Stefan pushed to branch master at Stefan / Typer

Commits: c17b5a1f by Stefan Monnier at 2016-08-26T23:47:10-04:00 Tweak use of substitutions and unsusp

* src/lexp.ml (subst): Newtype. (mkSusp): Also apply eagerly to Metavar. (push_susp): Rename from unsusp. (nosusp): Rename from ususp_all. (_lexp_to_str): Use push_susp.

- - - - - 536bba67 by Stefan Monnier at 2016-08-26T23:51:29-04:00 * src/lexp.ml (push_susp): Don't be so picky.

- - - - -

5 changed files:

- src/elexp.ml - src/lexp.ml - src/lparse.ml - src/subst.ml - src/typecheck.ml

Changes:

===================================== src/elexp.ml ===================================== --- a/src/elexp.ml +++ b/src/elexp.ml @@ -86,7 +86,7 @@ let rec erase_type (lxp: L.lexp): elexp = Case(l, (erase_type target), (clean_map cases), (clean_maybe default))

- | L.Susp(l, s) -> erase_type (L.unsusp l s) + | L.Susp(l, s) -> erase_type (L.push_susp l s)

(* To be thrown out *) | L.Arrow _ -> Type

===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -53,13 +53,14 @@ type label = symbol (* Pour la propagation des types bidirectionnelle, tout va dans `infer`, * sauf Lambda et Case qui vont dans `check`. Je crois. *) type ltype = lexp + and subst = lexp S.subst and lexp = | Imm of sexp (* Used for strings, ... *) | SortLevel of sort_level | Sort of U.location * sort | Builtin of vdef * ltype | Var of vref - | Susp of lexp * lexp S.subst (* Lazy explicit substitution: e[σ]. *) + | Susp of lexp * subst (* Lazy explicit substitution: e[σ]. *) (* This "Let" allows recursion. *) | Let of U.location * (vdef * lexp * ltype) list * lexp | Arrow of arg_kind * vdef option * ltype * U.location * lexp @@ -109,9 +110,12 @@ type varbind =

let rec mkSusp e s = if S.identity_p s then e else + (* We apply the substitution eagerly to some terms. + * There's no deep technical rason for that: + * it just seemed like a good idea to do it eagerly when it's easy. *) match e with | Susp (e, s') -> mkSusp e (scompose s' s) - | Var (l,v) -> slookup s l v (* Apply the substitution eagerly. *) + | Var (l,v) -> slookup s l v | _ -> Susp (e, s) and scompose s1 s2 = S.compose mkSusp s1 s2 and slookup s l v = S.lookup (fun l i -> Var (l, i)) @@ -271,16 +275,13 @@ let rec lexp_location e = let vdummy = (U.dummy_location, "dummy") let maybev mv = match mv with None -> vdummy | Some v -> v

-let rec unsusp e s = (* Push a suspension one level down. *) +let rec push_susp e s = (* Push a suspension one level down. *) match e with | Imm _ -> e | SortLevel _ -> e | Sort (l, Stype e) -> Sort (l, Stype (mkSusp e s)) | Sort (l, _) -> e | Builtin _ -> e - | Var ((l,_) as lv,v) -> U.msg_error "SUSP" l "¡Susp(Var)!"; slookup s lv v - | Susp (e,s') -> U.msg_error "SUSP" (lexp_location e) "¡Susp(Susp)!"; - mkSusp e (scompose s' s) | Let (l, defs, e) -> let s' = L.fold_left (fun s (v, _, _) -> ssink v s) s defs in let (_,ndefs) = L.fold_left (fun (s,ndefs) (v, def, ty) @@ -321,10 +322,19 @@ let rec unsusp e s = (* Push a suspension one level down. *) match default with | None -> default | Some e -> Some (mkSusp e s)) - -let unsusp_all e = + (* Susp should never appear around Var/Susp/Metavar because mkSusp + * pushes the subst into them eagerly. IOW if there's a Susp(Var..) + * or Susp(Metavar..) it's because some chunk of code should use mkSusp + * rather than Susp. *) + | Susp (e,s') -> (* U.msg_error "SUSP" (lexp_location e) "¡Susp(Susp)!"; *) + push_susp e (scompose s' s) + | (Var _) + -> (* U.msg_error "SUSP" (lexp_location e) "¡Susp((meta)var)!"; *) + push_susp (mkSusp e s) S.identity + +let nosusp e = (* Return `e` without `Susp`. *) match e with - | Susp(e, s) -> unsusp e s + | Susp(e, s) -> push_susp e s | _ -> e

let lexp_to_string e = @@ -668,7 +678,7 @@ and _lexp_to_str ctx exp = | Float (_, s) -> tval (string_of_float s) | e -> sexp_to_str e)

- | Susp _ -> _lexp_to_str ctx (unsusp_all exp) + | Susp (e, s) -> _lexp_to_str ctx (push_susp e s)

| Var ((loc, name), idx) -> name ^ (index idx) ;

===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -241,7 +241,7 @@ and _lexp_p_infer (p : pexp) (ctx : lexp_context) i: lexp * ltype = let inductive_type = Var((loc, type_name), idx) in

(* Get constructor args *) - let formal, args = match unsusp_all idt with + let formal, args = match nosusp idt with | Inductive(_, _, formal, ctor_def) -> ( try formal, (SMap.find cname ctor_def) with Not_found -> @@ -297,7 +297,7 @@ and _lexp_p_check (p : pexp) (t : ltype) (ctx : lexp_context) i: lexp = (* This case cannot be inferred *) | Plambda (kind, var, None, body) ->( (* Read var type from the provided type *) - let ltp, lbtp = match unsusp_all t with + let ltp, lbtp = match nosusp t with | Arrow(kind, _, ltp, _, lbtp) -> ltp, lbtp | _ -> lexp_error tloc "Type does not match"; dltype, dltype in

@@ -402,7 +402,7 @@ and lexp_call (fun_name: pexp) (sargs: sexp list) ctx i =

(* consume Arrows and args together *) let rec get_return_type name i ltp args = - match (unsusp_all ltp), args with + match (nosusp ltp), args with | _, [] -> ltp | Arrow(_, _, _, _, ltp), hd::tl -> (get_return_type name (i + 1) ltp tl) | _, _ -> lexp_warning loc @@ -416,7 +416,7 @@ and lexp_call (fun_name: pexp) (sargs: sexp list) ctx i =

(* retrieve function's body *) let body, ltp = _lexp_p_infer fun_name ctx (i + 1) in - let ltp = unsusp_all ltp in + let ltp = nosusp ltp in

let handle_named_call (loc, name) = (* Process Arguments *) @@ -428,7 +428,7 @@ and lexp_call (fun_name: pexp) (sargs: sexp list) ctx i = let idx = senv_lookup name ctx in let vf = (make_var name idx loc) in

- match unsusp_all (env_lookup_expr ctx ((loc, name), idx)) with + match nosusp (env_lookup_expr ctx ((loc, name), idx)) with | Builtin((_, "Built-in"), _) ->( (* ------ SPECIAL ------ *) match !_parsing_internals, largs with @@ -476,7 +476,7 @@ and lexp_call (fun_name: pexp) (sargs: sexp list) ctx i = lexp_fatal loc (name ^ " was found but " ^ (string_of_int idx) ^ " is not a correct index.") in

- let lxp = match unsusp_all lxp with + let lxp = match nosusp lxp with | Call(Var((_, "Macro_"), _), [(_, fct)]) -> fct | _ -> print_string "\n"; @@ -555,7 +555,7 @@ and lexp_read_pattern pattern exp target ctx: | Ppatvar ((loc, name) as var) ->( try( let idx = senv_lookup name ctx in - match unsusp_all (env_lookup_expr ctx ((loc, name), idx)) with + match nosusp (env_lookup_expr ctx ((loc, name), idx)) with (* We are matching a constructor *) | Cons _ -> (name, loc, []), ctx

@@ -641,7 +641,7 @@ and lexp_decls_macro (loc, mname) sargs ctx: (pdecl list * lexp_context) = " is not a correct index.") in

(* get stored function *) - let lxp = match unsusp_all lxp with + let lxp = match nosusp lxp with | Call(Var((_, "Macro_"), _), [(_, fct)]) -> fct | _ -> print_string "\n"; print_string (lexp_to_string lxp); print_string "\n";

===================================== src/subst.ml ===================================== --- a/src/subst.ml +++ b/src/subst.ml @@ -21,6 +21,28 @@ this program. If not, see http://www.gnu.org/licenses/. *)

module U = Util

+(* Implementation of the subsitution calculus. + * + * As a general rule, try not to use the constructors of the `subst' + * datatype, but use the following entry points instead. + * Constructor functions: + * - S.identity + * - S.cons + * - S.mkShift + * - S.shift + * - S.compose + * - S.substitute + * - S.sink + * Destructor functions: + * - S.identity_p + * - S.lookup + * + * This implementation is generic (i.e. can be with various datatypes + * implementing the associated lambda-calculus), which is the reason for + * the added complexity of arguments like `mkVar` and `mkShift` to `S.lookup`. + * So in general, you'll want to use Lexp.scompose and Lexp.slookup + * for those functions. + *)

(* Suspensions definitions. * @@ -236,6 +258,7 @@ let shift (m:db_offset) = mkShift Identity m (* The trivial substitution which doesn't do anything. *) let identity = Identity

+(* Test if a substitution is trivial. The "_p" stands for "predicate". *) let identity_p s = match s with | Identity -> true | _ -> false

(* Compose two substitutions. This implements the merging rules.

===================================== src/typecheck.ml ===================================== --- a/src/typecheck.ml +++ b/src/typecheck.ml @@ -110,7 +110,7 @@ let lookup_type ctx vref = let lookup_value ctx vref = let (_, i) = vref in match Myers.nth i ctx with - | (o, _, LetDef v, _) -> Some (unsusp v (S.shift (i + 1 - o))) + | (o, _, LetDef v, _) -> Some (push_susp v (S.shift (i + 1 - o))) | _ -> None

let assert_type e t t' = @@ -151,7 +151,7 @@ let rec check ctx e = | Builtin (_, t) -> t (* FIXME: Check recursive references. *) | Var v -> lookup_type ctx v - | Susp (e, s) -> check ctx (unsusp e s) + | Susp (e, s) -> check ctx (push_susp e s) | Let (_, defs, e) -> let tmp_ctx = L.fold_left (fun ctx (v, e, t)

View it on GitLab: https://gitlab.com/monnier/typer/compare/e54bbd6d3f50ce539b9669e07cec546057c...