Septembre 2017 - Typer - mailman.iro.umontreal.ca

Datatypes and tuples
by Stefan Monnier 02 Oct '18

02 Oct '18

Hi guys, Wondering if you might have an idea: In Typer, the basic datastructure is the "algebraic datatype" (which combines a sum, product, and recursion), and the basic eliminator is the "pattern matching case". It works OK, but is unsatisfactory: 1- both of those are fairly large/complex. 2- it means that extracting a record field is a "case" operation that discards all but the required field, so it's an O(n) operation (where n is the size of the record), if not in the final code, at least in intermediate code. 3- it means the choice of representation of datatype tags is hardcoded in the blackbox compiler. While point n°2 might seem irrelevant, it is a pain with large records, such as those you might get when records are used to represent modules: the encoding of the simple "String.concat" reference ends up taking space proportional to the number of primitives exported from the "String" module, which can be rather large. I'd like to find another option and was thinking of something along the following lines: - provide a separate product primitive. - provide a "union" type, i.e. an *untagged* sum. - provide primitive discrimination operations, such as "dispatch on an Int". then the Either type could look like Either a b = union (Singleton(1), a) (Singleton(2), b) and case e | Left x => ... | Right y => ... would turn into switch (e.0 <withmagicproof>) | 1 => let e' = cast (Singleton(1), a) e; x = e'.1 in ... | 2 => let e' = cast (Singleton(2), b) e; y = e'.1 in ... Obviously, we'd still want to have "case", but written as a macro. The `magicproof` is needed to convince Typer that all union members have a field 0. And of course, each `cast` would also need to provide a proof (constructed from a proof provided by `switch`) that indeed we know that `e` is this specific member of the union. The way I presented it is fairly general, but pretty heavyweight to define and to use: every "case" will be compiled to that big switch-with-proofs and the definition of a "record selection out of a union" (such as the "e.0 <withmagicproof>") seems fairly complex as well. Does anyone here have another approach to suggest? Stefan

5 7

[Git][monnier/typer][master] Also apply generalization to inductive type constructors
by Stefan 29 Sep '17

29 Sep '17

Stefan pushed to branch master at Stefan / Typer Commits: 06c37fc5 by Stefan Monnier at 2017-09-29T00:53:28-04:00 Also apply generalization to inductive type constructors * src/elab.ml (generalize): Change calling convention. (infer_and_generalize_type, infer_and_generalize_def): Adjust accordingly. (lexp_parse_inductive.make_args): Generalize constructors. (var_of_ovar): Move to lexp.ml. * src/opslexp.ml (check', get_type): Fix scoping of `level` in Inductive. * btl/builtins.typer (Eq_comm): Take advantage of improvements in gneralization and unification. * btl/pervasive.typer (BoolMod): Avoid `typecons`'s generalizing. (LList): New type, to test typecons's generalization. * src/lexp.ml (var_of_ovar): Move from elab.ml. (lexp_unparse): Simplify. * src/pexp.ml (pexp_u_ind_arg): Remove. - - - - - 6 changed files: - btl/builtins.typer - btl/pervasive.typer - src/elab.ml - src/lexp.ml - src/opslexp.ml - src/pexp.ml Changes: ===================================== btl/builtins.typer ===================================== --- a/btl/builtins.typer +++ b/btl/builtins.typer @@ -52,10 +52,12 @@ Eq_cast = Built-in "Eq.cast" ≡> f x -> f y); %% Commutativity of equality! -Eq_comm : (l : TypeLevel) ≡> (t : Type_ l) ≡> (x : t) ≡> (y : t) - ≡> (p : Eq (t := t) x y) -> Eq (t := t) y x; +%% FIXME: I'd like to just say: +%% Eq_comm : (p : Eq ?x ?y) -> Eq ?y ?x`; +Eq_comm : (x : ?t) ≡> (y : ?t) ≡> (p : Eq x y) -> Eq (t := ?t) y x; Eq_comm p = Eq_cast (f := lambda xy -> Eq (t := t) xy x) - (p := p) + %% FIXME: I can't figure out how `(p := p)` + %% gets inferred here, yet it seems to work!?! Eq_refl; %% General recursion!! ===================================== btl/pervasive.typer ===================================== --- a/btl/pervasive.typer +++ b/btl/pervasive.typer @@ -70,8 +70,6 @@ List_map f = lambda xs -> case xs | cons x xs => cons (f x) (List_map f xs); List_foldr : (?b -> ?a -> ?a) -> List ?b -> ?a -> ?a; -%% List_foldr : (l : TypeLevel) ≡> (a : Type_ l) ≡> (b : Type) -%% ≡> (b -> a -> a) -> List b -> a -> a; List_foldr f = lambda xs -> lambda i -> case xs | nil => i | cons x xs => f x (List_foldr f xs i); @@ -164,7 +162,9 @@ I x = x; %% Typer generalizes to %% K : (a : Type) ≡> (b : Type) ≡> a -> b -> a; %% Which is less general. -K : (a : Type) ≡> a -> (b : Type) ≡> b -> a; +%% FIXME: Change the generalizer to insert the `(b : Type) ≡>` +%% more lazily (i.e. after the `a` argument). +K : ?a -> (b : Type) ≡> b -> ?a; K x y = x; %%%% Quasi-Quote macro @@ -308,8 +308,22 @@ tail = List_tail; %%%% Tuples %% Sample tuple: a module holding Bool and its constructors. -BoolMod = (##datacons (typecons _ (cons (t :: ?) (true :: ?) (false :: ?))) - cons) +BoolMod = (##datacons + %% We need the `?` metavars to be lexically outside of the + %% `typecons` expression, otherwise they end up generalized, so + %% we end up with a type constructor like + %% + %% typecons _ (cons (τ₁ : Type) (t : τ₁) + %% (τ₂ : Type) (true : τ₂) + %% (τ₃ : Type) (false : τ₃) + %% + %% And it's actually even worse because it tries to generalize + %% over the level of those `Type`s, so we end up with an invalid + %% inductive type. + ((lambda t1 t2 t3 + -> typecons _ (cons (t :: t1) (true :: t2) (false :: t3))) + ? ? ?) + cons) (_ := Bool) (_ := true) (_ := false); Pair = typecons (Pair (a : Type) (b : Type)) (cons (x :: a) (y :: b)); @@ -350,9 +364,17 @@ Not : Type -> Type; Not prop = prop -> False; %% Like Bool, except that it additionally carries the meaning of its value. +%% We don't use the `type` macro here because it would make these `true` +%% and `false` constructors ovrride `Bool`'s, and we currently don't +%% want that. Decidable = typecons (Decidable (prop : Type)) (true (p ::: prop)) (false (p ::: Not prop)); +%% Testing generalization in inductive type constructors. +LList : (a : Type) -> Int -> Type; %FIXME: `LList : ?` should be sufficient! +type LList (a : Type) n + | vnil (p ::: Eq n 0) + | vcons a (LList a ?n1) (p ::: Eq n (?n1 + 1)); %FIXME: Unsound wraparound! %%%% If ===================================== src/elab.ml ===================================== --- a/src/elab.ml +++ b/src/elab.ml @@ -340,12 +340,14 @@ let rec meta_to_var ids o (e : lexp) = (* Generalize expression `e` with respect to its uninstantiated metavars. * `wrap` is the function that adds the relevant quantification, typically * either mkArrow or mkLambda. *) -let generalize wrap (nctx : elab_context) e = +let generalize (nctx : elab_context) e = let l = lexp_location e in let sl = ectx_to_scope_level nctx in let cl = Myers.length (ectx_to_lctx nctx) in let (_, (mfvs, nes)) = OL.fv e in - if mfvs = IMap.empty then e else ( + if mfvs = IMap.empty + then (fun wrap e -> e) (* Nothing to generalize, yay! *) + else let mfvs = IMap.fold (fun idx (sl', mt, cl', vname) fvs -> if sl' < sl then (* This metavar appears in the context, @@ -363,16 +365,18 @@ let generalize wrap (nctx : elab_context) e = mfvs [] in (* FIXME: Sort `mvfs' topologically! *) let len = List.length mfvs in - let e = mkSusp e (S.shift len) in + fun wrap e -> let rec loop ids n mfvs = match mfvs with - | [] -> assert (n = 0); meta_to_var ids 0 e + | [] -> assert (n = 0); + let e = mkSusp e (S.shift len) in + meta_to_var ids 0 e | ((id, vname, mt) :: mfvs) -> let mt' = mkSusp mt (S.shift (len - n)) in let mt'' = meta_to_var ids (- n) mt' in let n = n - 1 in let e' = loop (IMap.add id n ids) n mfvs in wrap (IMap.mem id nes) vname mt'' l e' in - loop (IMap.empty) len mfvs) + loop (IMap.empty) len mfvs (* Infer or check, as the case may be. *) let rec elaborate ctx se ot = @@ -803,24 +807,45 @@ and elab_call ctx (func, ltp) (sargs: sexp list) = (* Parse inductive type definition. *) and lexp_parse_inductive ctors ctx = - let make_args (args:(arg_kind * pvar option * sexp) list) ctx - : (arg_kind * vname option * ltype) list = - let rec loop args acc ctx = - match args with - | [] -> (List.rev acc) - | hd::tl -> begin - match hd with - | (kind, var, exp) -> - let lxp = infer_type exp ctx var in - let nctx = ectx_extend ctx var Variable lxp in - loop tl ((kind, var, lxp)::acc) nctx - end in - loop args [] ctx in - - List.fold_left - (fun lctors ((_, name), args) -> - SMap.add name (make_args args ctx) lctors) - SMap.empty ctors + let make_args (args:(arg_kind * pvar option * sexp) list) ctx + : (arg_kind * vname option * ltype) list = + let nctx = ectx_new_scope ctx in + let rec loop args acc ctx = + match args with + | [] -> let acc = List.rev acc in + (* Convert the list of fields into a Lexp expression. + * The actual expression doesn't matter, as long as its + * scoping is right: we only use it so we can pass it to + * things like `fv` and `meta_to_var`. *) + let altacc = List.fold_right + (fun (ak, n, t) aa + -> Arrow (ak, n, t, dummy_location, aa)) + acc impossible in + let g = generalize nctx altacc in + let altacc' = g (fun _ne vname t l e + -> Arrow (Aerasable, Some vname, t, l, e)) + altacc in + if altacc' == altacc + then acc (* No generalization! *) + else + (* Convert the Lexp back into a list of fields. *) + let rec loop e = match e with + | Arrow (ak, n, t, _, e) -> (ak, n, t)::(loop e) + | _ -> assert (e = impossible); [] in + loop altacc' + | hd::tl -> begin + match hd with + | (kind, var, exp) -> + let lxp = infer_type exp ctx var in + let nctx = ectx_extend ctx var Variable lxp in + loop tl ((kind, var, lxp)::acc) nctx + end in + loop args [] nctx in + + List.fold_left + (fun lctors ((_, name), args) -> + SMap.add name (make_args args ctx) lctors) + SMap.empty ctors and track_fv rctx lctx e = let (fvs, (mvs, _)) = OL.fv e in @@ -925,24 +950,27 @@ and infer_and_generalize_type (ctx : elab_context) se oname = let t = infer_type se nctx oname in match OL.lexp_whnf t (ectx_to_lctx ctx) with (* There's no point generalizing a single metavar, and it's useful - * to keep it ungeneralized so you can use `x : ?` to declare that - * `x` will be defined later. *) + * to keep it ungeneralized so we can use `x : ?` to declare that + * `x` will be defined later without specifying its type yet. *) | Metavar _ -> t - | _ -> generalize (fun _ne vname t l e - -> mkArrow (Aerasable, Some vname, t, l, e)) - nctx t + | _ -> let g = generalize nctx t in + g (fun _ne vname t l e + -> mkArrow (Aerasable, Some vname, t, l, e)) + t and infer_and_generalize_def (ctx : elab_context) se = let nctx = ectx_new_scope ctx in let (e,t) = infer se nctx in - let e' = generalize (fun ne vname t l e - -> mkLambda ((if ne then Aimplicit else Aerasable), - vname, t, e)) - nctx e in - if e == e' - then (e, t) - (* FIXME: Compute type directly instead of going through `e'`. *) - else (e', OL.get_type (ectx_to_lctx ctx) e') + let g = generalize nctx e in + let e' = g (fun ne vname t l e + -> mkLambda ((if ne then Aimplicit else Aerasable), + vname, t, e)) + e in + let t' = g (fun ne vname t l e + -> mkArrow ((if ne then Aimplicit else Aerasable), + Some vname, t, sexp_location se, e)) + t in + (e', t') and lexp_decls_1 (sdecls : sexp list) @@ -1332,10 +1360,6 @@ let sform_identifier ctx loc sargs ot = -> (sexp_error loc ("Too many args to ##typer-identifier"); sform_dummy_ret ctx loc) -let var_of_ovar l ov = match ov with - | None -> (l, "<anon>") - | Some v -> v - let rec sform_lambda kind ctx loc sargs ot = match sargs with | [sarg; sbody] ===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -205,6 +205,10 @@ let mkCall (f, es) | _, [] -> f | _ -> hc (Call (f, es)) +let var_of_ovar l ov = match ov with + | None -> (l, "<anon>") + | Some v -> v + (********* Helper functions to use the Subst operations *********) (* This basically "ties the knot" between Subst and Lexp. * Maybe it would be cleaner to just move subst.ml into lexp.ml @@ -435,21 +439,24 @@ let rec lexp_unparse lxp = let pfargs = List.map (fun (kind, vdef, ltp) -> (kind, vdef, Some (lexp_unparse ltp))) lfargs in - (* ((arg_kind * vdef option * ltype) list) SMap.t *) - (* (symbol * (arg_kind * pvar option * pexp) list) list *) - let ctors = List.map (fun (str, largs) -> - let pargs = List.map (fun (kind, var, ltp) -> - match var with - | Some (loc, name) -> (kind, Some (loc, name), lexp_unparse ltp) - | None -> (kind, None, lexp_unparse ltp)) largs - in ((loc, str), pargs) - ) (SMap.bindings ctors) in Node (stypecons, Node (Symbol label, List.map pexp_u_formal_arg pfargs) - :: List.map (fun ((l,name) as s, types) - -> Node (Symbol s, - List.map pexp_u_ind_arg types)) - ctors) + :: List.map + (fun (name, types) + -> Node (Symbol (loc, name), + List.map + (fun arg -> + match arg with + | (Aexplicit, None, t) -> lexp_unparse t + | (ak, s, t) + -> let (l,_) as id = pexp_u_id s in + Node (Symbol (l, match ak with + | Aexplicit -> "_:_" + | Aimplicit -> "_::_" + | Aerasable -> "_:::_"), + [Symbol id; lexp_unparse t])) + types)) + (SMap.bindings ctors)) | Case (loc, target, bltp, branches, default) -> let bt = lexp_unparse bltp in ===================================== src/opslexp.ml ===================================== --- a/src/opslexp.ml +++ b/src/opslexp.ml @@ -484,18 +484,18 @@ let rec check' erased ctx e = -> let level = SMap.fold (fun _ case level -> - let level, _, _ = + let (level, _, _, _) = List.fold_left - (fun (level, ctx, erased) (ak, v, t) -> - (* FIXME: DB.set_empty seems wrong! *) + (fun (level, ctx, erased, n) (ak, v, t) -> ((match lexp_whnf (check_type erased ctx t) ctx with | Sort (_, Stype _) when ak == P.Aerasable && impredicative_erase -> level | Sort (_, Stype level') - (* FIXME: scoping of level vars! *) - -> mkSLlub ctx level level' + -> mkSLlub ctx level + (Inverse_subst.apply_inv_subst level' + (S.shift n)) | tt -> U.msg_error "TC" (lexp_location t) ("Field type " ^ lexp_string t @@ -505,8 +505,9 @@ let rec check' erased ctx e = (* U.internal_error "Oops"; *) level), DB.lctx_extend ctx v Variable t, - DB.set_sink 1 erased)) - (level, ctx, erased) + DB.set_sink 1 erased, + n + 1)) + (level, ctx, erased, 0) case in level) cases (mkSortLevel SLz) in @@ -788,19 +789,22 @@ let rec get_type ctx e = -> let level = SMap.fold (fun _ case level -> - let level, _ = + let (level, _, _) = List.fold_left - (fun (level, ctx) (ak, v, t) -> - (match lexp_whnf (get_type ctx t) ctx with - | Sort (_, Stype _) - when ak == P.Aerasable && impredicative_erase - -> level - | Sort (_, Stype level') - (* FIXME: scoping of level vars! *) - -> mkSLlub ctx level level' - | tt -> level), - DB.lctx_extend ctx v Variable t) - (level, ctx) + (fun (level, ctx, n) (ak, v, t) -> + ((match lexp_whnf (get_type ctx t) ctx with + | Sort (_, Stype _) + when ak == P.Aerasable && impredicative_erase + -> level + | Sort (_, Stype level') + -> mkSLlub ctx level + (try Inverse_subst.apply_inv_subst level' + (S.shift n) + with _ -> level) + | tt -> level), + DB.lctx_extend ctx v Variable t, + n + 1)) + (level, ctx, 0) case in level) cases (mkSortLevel SLz) in ===================================== src/pexp.ml ===================================== --- a/src/pexp.ml +++ b/src/pexp.ml @@ -90,15 +90,6 @@ and pexp_p_ind_arg s = match s with -> (Aerasable, pexp_p_id s, t) | _ -> (Aexplicit, None, s) -and pexp_u_ind_arg arg = match arg with - | (Aexplicit, None, t) -> t - | (k, s, t) - -> let (l,_) as id = pexp_u_id s in - Node (Symbol (l, match k with Aexplicit -> "_:_" - | Aimplicit -> "_::_" - | Aerasable -> "_:::_"), - [Symbol id; t]) - and pexp_p_pat_arg (s : sexp) = match s with | Symbol _ -> (None, pexp_p_pat s) | Node (Symbol (_, "_:=_"), [Symbol f; Symbol s]) View it on GitLab: https://gitlab.com/monnier/typer/commit/06c37fc5c1d4d8b79394b90bcd05f9f26df… --- View it on GitLab: https://gitlab.com/monnier/typer/commit/06c37fc5c1d4d8b79394b90bcd05f9f26df… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][master] Finally implement the occurs check (and scope_level propagation)
by Stefan 26 Sep '17

26 Sep '17

Stefan pushed to branch master at Stefan / Typer Commits: 17853dd7 by Stefan Monnier at 2017-09-26T09:08:22-04:00 Finally implement the occurs check (and scope_level propagation) * src/lexp.ml (ctx_length): Rename from scope_length. * src/unification.ml (occurs_in): New function. (_unify_metavar.unif): Use it to avoid circular types and inconsistent generalization! - - - - - 3 changed files: - src/lexp.ml - src/opslexp.ml - src/unification.ml Changes: ===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -141,10 +141,10 @@ type varbind = (* Scope level is used to detect "out of scope" metavars. * See http://okmij.org/ftp/ML/generalization.html - * The lctx_length keeps track of the lctx's length when that scope level was - * entered in order to know by how much to shift metavars. *) + * The ctx_length keeps track of the length of the lctx in which the + * metavar is meant to be defined. *) type scope_level = int -type scope_length = int +type ctx_length = int type metavar_info = | MVal of lexp (* Exp to which the var is instantiated. *) @@ -153,7 +153,7 @@ type metavar_info = (* We'd like to keep the lexp_content in which the type is to be * understood, but lexp_context is not yet defined here, * so we just keep the length of the lexp_context. *) - * scope_length + * ctx_length type meta_subst = metavar_info U.IMap.t type constraints = (lexp * lexp) list ===================================== src/opslexp.ml ===================================== --- a/src/opslexp.ml +++ b/src/opslexp.ml @@ -624,7 +624,7 @@ let rec list_union l1 l2 = match l1 with | [] -> l2 | (x::l1) -> list_union l1 (if List.mem x l2 then l2 else (x::l2)) -type mv_set = (scope_level * ltype * scope_length * vname) IMap.t +type mv_set = (scope_level * ltype * ctx_length * vname) IMap.t (* Metavars that appear in non-erasable positions. *) * unit IMap.t let mv_set_empty : mv_set = (IMap.empty, IMap.empty) ===================================== src/unification.ml ===================================== --- a/src/unification.ml +++ b/src/unification.ml @@ -19,12 +19,6 @@ more details. You should have received a copy of the GNU General Public License along with this program. If not, see <http://www.gnu.org/licenses/>. *) -(* FIXME: Needs occurs-check. - * Also needs to add a notion of scope-level, as described in - * http://okmij.org/ftp/ML/generalization.html (aka ranks in - * ftp://ftp.inria.fr/INRIA/Projects/cristal/Didier.Remy/eq-theory-on-types.ps.gz) - *) - open Lexp (* open Sexp *) (* open Inverse_subst *) @@ -47,9 +41,66 @@ let create_metavar (ctx : DB.lexp_context) (sl : scope_level) (t : ltype) type return_type = constraints option (** Alias for VMap.add*) -let associate (meta: int) (lxp: lexp) (subst: meta_subst) : meta_subst - = U.IMap.add meta (MVal lxp) subst - +let associate (id: meta_id) (lxp: lexp) (subst: meta_subst) : meta_subst + = U.IMap.add id (MVal lxp) subst + +let occurs_in (id: meta_id) (e : lexp) : bool = match metavar_lookup id with + | MVal _ -> U.internal_error + "Checking occurrence of an instantiated metavar!!" + | MVar (sl, _, _) + -> let rec oi e = match e with + | Imm _ -> false + | SortLevel SLz -> false + | SortLevel (SLsucc e) -> oi e + | SortLevel (SLlub (e1, e2)) -> oi e1 || oi e2 + | Sort (_, Stype e) -> oi e + | Sort (_, (StypeOmega | StypeLevel)) -> false + | Builtin _ -> false + | Var (_, i) -> false + | Susp (e, s) -> U.internal_error "`e` should be \"clean\" here!?" + (* ; oi (push_susp e s) *) + | Let (_, defs, e) + -> List.fold_left (fun o (_, e, t) -> o || oi e || oi t) (oi e) defs + | Arrow (_, _, t1, _, t2) -> oi t1 || oi t2 + | Lambda (_, _, t, e) -> oi t || oi e + | Call (f, args) + -> List.fold_left (fun o (_, arg) -> o || oi arg) (oi f) args + | Inductive (_, _, args, cases) + -> SMap.fold + (fun _ fields o + -> List.fold_left (fun o (_, _, t) -> o || oi t) + o fields) + cases + (List.fold_left (fun o (_, _, t) -> o || oi t) false args) + | Cons (t, _) -> oi t + | Case (_, e, t, cases, def) + -> let o = oi e || oi t in + let o = match def with | None -> o | Some (_, e) -> o || oi e in + SMap.fold (fun _ (_, _, e) o -> o || oi e) + cases o + | Metavar (id', _, name) when id' = id -> true + | Metavar (id', _, _) + -> (match metavar_lookup id' with + | MVal e -> U.internal_error "`e` should be \"clean\" here!?" + (* ; oi e *) + | MVar (sl', t, cl) + -> if sl' > sl then + (* id' will now appear in id's scope, so if id's scope is + * higher than id', we need to make sure id' won't be + * generalized in sl' but only in sl! + * This is the trick mentioned in + * http://okmij.org/ftp/ML/generalization.html + * to avoid computing `fv lctx` when generalizing! *) + metavar_table := U.IMap.add id' (MVar (sl, t, cl)) + (!metavar_table); + false) in + let old_mvt = (!metavar_table) in + if oi e then + (* Undo the side-effects since we're not going to instantiate the + var after all! *) + (metavar_table := old_mvt; true) + else false + (** lexp is equivalent to _ in ocaml (Let , lexp) == (lexp , Let) @@ -175,6 +226,7 @@ and _unify_metavar ctx idx s (lxp1: lexp) (lxp2: lexp) lexp_print lxp; print_string "\n"; None + | lxp' when occurs_in idx lxp' -> None | lxp' -> metavar_table := associate idx lxp' (!metavar_table); match unify t (OL.get_type ctx lxp) ctx with View it on GitLab: https://gitlab.com/monnier/typer/commit/17853dd7385dc60938a31aeee474bc28f63… --- View it on GitLab: https://gitlab.com/monnier/typer/commit/17853dd7385dc60938a31aeee474bc28f63… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][master] Pretend we use bigints for Sexp integers
by Stefan 25 Sep '17

25 Sep '17

Stefan pushed to branch master at Stefan / Typer Commits: 098ca889 by Stefan Monnier at 2017-09-26T02:15:31Z Pretend we use bigints for Sexp integers * btl/builtins.typer: Slight reorganisation. (Float->string): Rename from Float_to_string. (Int->Integer): Give it a type. (Sexp_integer): Change its type to be `Integer`. (Sexp_dispatch): Make matching change. * src/eval.ml: Add new "Int->Integer" primitive. (make_integer): Make it take a bigint. (sexp_dispatch): Make it use a bigint for the integer case. - - - - - 6 changed files: - btl/builtins.typer - src/eval.ml - src/opslexp.ml - src/sexp.ml - tests/eval_test.ml - tests/macro_test.ml Changes: ===================================== btl/builtins.typer ===================================== --- a/btl/builtins.typer +++ b/btl/builtins.typer @@ -86,32 +86,27 @@ Eq_comm p = Eq_cast (f := lambda xy -> Eq (t := t) xy x) Y = Built-in "Y" ((a : Type) ≡> (b : Type) ≡> (witness : a -> b) ≡> ((a -> b) -> (a -> b)) -> (a -> b)); +Bool = typecons (Bool) (true) (false); +true = datacons Bool true; +false = datacons Bool false; + %% Basic operators _+_ = Built-in "Int.+" (Int -> Int -> Int); _-_ = Built-in "Int.-" (Int -> Int -> Int); _*_ = Built-in "Int.*" (Int -> Int -> Int); _/_ = Built-in "Int./" (Int -> Int -> Int); -Integer_+ = Built-in "Integer.+" (Integer -> Integer -> Integer); -Integer_- = Built-in "Integer.-" (Integer -> Integer -> Integer); -Integer_* = Built-in "Integer.*" (Integer -> Integer -> Integer); -Integer_/ = Built-in "Integer./" (Integer -> Integer -> Integer); - -Float_+ = Built-in "Float.+" (Float -> Float -> Float); -Float_- = Built-in "Float.-" (Float -> Float -> Float); -Float_* = Built-in "Float.*" (Float -> Float -> Float); -Float_/ = Built-in "Float./" (Float -> Float -> Float); -Float_to_string = Built-in "Float.to_string" (Float -> String); - -Bool = typecons (Bool) (true) (false); -true = datacons Bool true; -false = datacons Bool false; - Int_< = Built-in "Int.<" (Int -> Int -> Bool); Int_> = Built-in "Int.>" (Int -> Int -> Bool); Int_eq = Built-in "Int.=" (Int -> Int -> Bool); Int_<= = Built-in "Int.<=" (Int -> Int -> Bool); Int_>= = Built-in "Int.>=" (Int -> Int -> Bool); +Int->Integer = Built-in "Int->Integer" (Int -> Integer); + +Integer_+ = Built-in "Integer.+" (Integer -> Integer -> Integer); +Integer_- = Built-in "Integer.-" (Integer -> Integer -> Integer); +Integer_* = Built-in "Integer.*" (Integer -> Integer -> Integer); +Integer_/ = Built-in "Integer./" (Integer -> Integer -> Integer); Integer_< = Built-in "Integer.<" (Integer -> Integer -> Bool); Integer_> = Built-in "Integer.>" (Integer -> Integer -> Bool); @@ -119,6 +114,12 @@ Integer_eq = Built-in "Integer.=" (Integer -> Integer -> Bool); Integer_<= = Built-in "Integer.<=" (Integer -> Integer -> Bool); Integer_>= = Built-in "Integer.>=" (Integer -> Integer -> Bool); +Float_+ = Built-in "Float.+" (Float -> Float -> Float); +Float_- = Built-in "Float.-" (Float -> Float -> Float); +Float_* = Built-in "Float.*" (Float -> Float -> Float); +Float_/ = Built-in "Float./" (Float -> Float -> Float); +Float->String = Built-in "Float->String" (Float -> String); + String_eq = Built-in "String.=" (String -> String -> Bool); Sexp_eq = Built-in "Sexp.=" (Sexp -> Sexp -> Bool); @@ -127,9 +128,6 @@ Sexp_eq = Built-in "Sexp.=" (Sexp -> Sexp -> Bool); %% ----------------------------------------------------- %% FIXME: "List : ?" should be sufficient but triggers -%% [!] Error ELAB `(List[2] a[1]) : ?ta · Id[18]` is not a proper type -%% > Call: (List[2] a[1]) -%% "Subst-inversion-bug: <anon> · (↑2 () · () · () · Id) ∘ <anon0> · () · (↑4 Id) == <anon> · () · (↑2 Id) !!" List : Type -> Type; %% List a = typecons List (nil) (cons a (List a)); %% nil = lambda a ≡> datacons (List a) nil; @@ -144,7 +142,7 @@ cons = datacons List cons; Sexp_symbol = Built-in "Sexp.symbol" (String -> Sexp); Sexp_string = Built-in "Sexp.string" (String -> Sexp); Sexp_node = Built-in "Sexp.node" (Sexp -> List Sexp -> Sexp); -Sexp_integer = Built-in "Sexp.integer" (Int -> Sexp); +Sexp_integer = Built-in "Sexp.integer" (Integer -> Sexp); Sexp_float = Built-in "Sexp.float" (Float -> Sexp); Macro = typecons (Macro) @@ -161,7 +159,7 @@ Sexp_dispatch = Built-in "Sexp.dispatch" ( -> (node : Sexp -> List Sexp -> a) -> (symbol : String -> a) -> (string : String -> a) - -> (int : Int -> a) + -> (int : Integer -> a) -> (float : Float -> a) -> (block : List Sexp -> a) -> a ===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -147,7 +147,7 @@ let add_binary_bool_iop name f = let name = "Int." ^ name in let f loc (depth : eval_debug_info) (args_val: value_type list) = match args_val with - | [Vint (v); Vint (w)] -> o2v_bool (f v w) + | [Vint v; Vint w] -> o2v_bool (f v w) | _ -> error loc ("`" ^ name ^ "` expects 2 Int arguments") in add_builtin_function name f 2 @@ -157,11 +157,13 @@ let _ = add_binary_bool_iop "<" (<); add_binary_bool_iop ">=" (>=); add_binary_bool_iop "<=" (<=) +(* True integers (aka Z). *) + let add_binary_biop name f = let name = "Integer." ^ name in let f loc (depth : eval_debug_info) (args_val: value_type list) = match args_val with - | [Vinteger (v); Vinteger (w)] -> Vinteger (f v w) + | [Vinteger v; Vinteger w] -> Vinteger (f v w) | _ -> error loc ("`" ^ name ^ "` expects 2 Integer arguments") in add_builtin_function name f 2 @@ -174,7 +176,7 @@ let add_binary_bool_biop name f = let name = "Integer." ^ name in let f loc (depth : eval_debug_info) (args_val: value_type list) = match args_val with - | [Vinteger (v); Vinteger (w)] -> o2v_bool (f v w) + | [Vinteger v; Vinteger w] -> o2v_bool (f v w) | _ -> error loc ("`" ^ name ^ "` expects 2 Integer arguments") in add_builtin_function name f 2 @@ -182,13 +184,23 @@ let _ = add_binary_bool_biop "<" BI.lt_big_int; add_binary_bool_biop ">" BI.gt_big_int; add_binary_bool_biop "=" BI.eq_big_int; add_binary_bool_biop ">=" BI.ge_big_int; - add_binary_bool_biop "<=" BI.le_big_int + add_binary_bool_biop "<=" BI.le_big_int; + let name = "Int->Integer" in + add_builtin_function + name + (fun loc (depth : eval_debug_info) (args_val: value_type list) + -> match args_val with + | [Vint v] -> Vinteger (BI.big_int_of_int v) + | _ -> error loc ("`" ^ name ^ "` expects 1 Int argument")) + 1 + +(* Floating point numers. *) let add_binary_fop name f = let name = "Float." ^ name in let f loc (depth : eval_debug_info) (args_val: value_type list) = match args_val with - | [Vfloat (v); Vfloat (w)] -> Vfloat (f v w) + | [Vfloat v; Vfloat w] -> Vfloat (f v w) | _ -> error loc ("`" ^ name ^ "` expects 2 Float arguments") in add_builtin_function name f 2 @@ -221,10 +233,9 @@ let make_string loc depth args_val = match args_val with | _ -> error loc "Sexp.string expects one string as argument" let make_integer loc depth args_val = match args_val with - | [Vint (str)] -> Vsexp (Integer (loc, str)) + | [Vinteger n] -> Vsexp (Integer (loc, BI.int_of_big_int n)) | _ -> error loc "Sexp.integer expects one integer as argument" - let make_float loc depth args_val = match args_val with | [Vfloat x] -> Vsexp (Float (loc, x)) | _ -> error loc "Sexp.float expects one float as argument" @@ -285,13 +296,13 @@ let rec _eval lxp (ctx : Env.runtime_env) (trace : eval_debug_info): (value_type match lxp with (* Leafs *) (* ---------------- *) - | Imm(Integer (_, i)) -> Vint (i) - | Imm(String (_, s)) -> Vstring (s) - | Imm(Float (_, n)) -> Vfloat (n) - | Imm(sxp) -> Vsexp (sxp) + | Imm(Integer (_, i)) -> Vint i + | Imm(String (_, s)) -> Vstring s + | Imm(Float (_, n)) -> Vfloat n + | Imm(sxp) -> Vsexp sxp | Cons (label) -> Vcons (label, []) | Lambda ((_, n), lxp) -> Closure (n, lxp, ctx) - | Builtin ((_, str)) -> Vbuiltin (str) + | Builtin ((_, str)) -> Vbuiltin str (* Return a value stored in env *) | Var((loc, name), idx) as e @@ -490,16 +501,17 @@ and sexp_dispatch loc depth args = | Symbol (_ , s) -> let rctx = ctx_sym in - eval sym (add_rte_variable None (Vstring(s)) rctx) + eval sym (add_rte_variable None (Vstring s) rctx) | String (_ , s) -> let rctx = ctx_str in - eval str (add_rte_variable None (Vstring(s)) rctx) + eval str (add_rte_variable None (Vstring s) rctx) | Integer (_ , i) -> let rctx = ctx_it in - eval it (add_rte_variable None (Vint(i)) rctx) + eval it (add_rte_variable None (Vinteger (BI.big_int_of_int i)) + rctx) | Float (_ , f) -> let rctx = ctx_flt in - eval flt (add_rte_variable None (Vfloat(f)) rctx) (* + eval flt (add_rte_variable None (Vfloat f) rctx) (* | Block (_ , s, _) -> eval blk (add_rte_variable None (o2v_list s)) *) | _ -> @@ -588,7 +600,7 @@ let io_return loc depth args_val = match args_val with let float_to_string loc depth args_val = match args_val with | [Vfloat x] -> Vstring (string_of_float x) - | _ -> error loc "Float.to_string expects one Float arg" + | _ -> error loc "Float->string expects one Float arg" let sys_exit loc depth args_val = match args_val with | [Vint n] -> Vcommand (fun _ -> exit n) @@ -626,7 +638,7 @@ let register_builtin_functions () = ("Sexp.dispatch" , sexp_dispatch, 7); ("String.=" , string_eq, 2); ("Sexp.=" , sexp_eq, 2); - ("Float.to_string", float_to_string, 1); + ("Float->String", float_to_string, 1); ("IO.bind" , io_bind, 2); ("IO.return" , io_return, 1); ("IO.run" , io_run, 2); ===================================== src/opslexp.ml ===================================== --- a/src/opslexp.ml +++ b/src/opslexp.ml @@ -420,6 +420,7 @@ let rec check' erased ctx e = -> (let _ = check_type DB.set_empty ctx t in DB.lctx_extend ctx (Some v) ForwardRef t)) ctx defs in + (* FIXME: Allow erasable let-bindings! *) let nerased = DB.set_sink (List.length defs) erased in let nctx = DB.lctx_extend_rec ctx defs in (* FIXME: Termination checking! Positivity-checker! *) ===================================== src/sexp.ml ===================================== --- a/src/sexp.ml +++ b/src/sexp.ml @@ -33,6 +33,9 @@ type sexp = (* Syntactic expression, kind of like Lisp. *) | Block of location * pretoken list * location | Symbol of symbol | String of location * string + (* FIXME: It would make a lof of sense to use a bigint here, but `compare` + * burps on Big_int objects, and `compare` is used for hash-consing of lexp + * objects which contain sexp objects as well. *) | Integer of location * integer | Float of location * float | Node of sexp * sexp list ===================================== tests/eval_test.ml ===================================== --- a/tests/eval_test.ml +++ b/tests/eval_test.ml @@ -343,7 +343,7 @@ let _ = test_eval_eqv_named "Implicit Arguments" "default = new-attribute Macro; - default = add-attribute default Int (macro (lambda (lst : List Sexp) -> Sexp_integer 1)); + default = add-attribute default Int (macro (lambda (lst : List Sexp) -> Sexp_integer (Int->Integer 1))); fun = lambda (x : Int) => lambda (y : Int) -> ===================================== tests/macro_test.ml ===================================== --- a/tests/macro_test.ml +++ b/tests/macro_test.ml @@ -75,7 +75,7 @@ let _ = (add_test "MACROS" "macros decls" (fun () -> let make-decl : String -> Int -> Sexp; make-decl name val = - (Sexp_node (Sexp_symbol \"_=_\") (cons (Sexp_symbol name) (cons (Sexp_integer val) nil))) in + (Sexp_node (Sexp_symbol \"_=_\") (cons (Sexp_symbol name) (cons (Sexp_integer (Int->Integer val)) nil))) in let d1 = make-decl \"a\" 1 in let d2 = make-decl \"b\" 2 in View it on GitLab: https://gitlab.com/monnier/typer/commit/098ca889df9159b692dc6f8896ffb59588e… --- View it on GitLab: https://gitlab.com/monnier/typer/commit/098ca889df9159b692dc6f8896ffb59588e… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][master] * src/util.ml (msg_message): Use GNU standard format.
by Stefan 25 Sep '17

25 Sep '17

Stefan pushed to branch master at Stefan / Typer Commits: befa5609 by Stefan Monnier at 2017-09-25T17:46:34Z * src/util.ml (msg_message): Use GNU standard format. - - - - - 2 changed files: - src/env.ml - src/util.ml Changes: ===================================== src/env.ml ===================================== --- a/src/env.ml +++ b/src/env.ml @@ -124,12 +124,13 @@ let value_name v = let rec value_string v = match v with | Vin _ -> "in_channel" - | Vout _ -> "out_channe;" + | Vout _ -> "out_channel" | Vundefined -> "<undefined!>" | Vcommand _ -> "command" | Vstring s -> "\"" ^ s ^ "\"" | Vbuiltin s -> s | Vint i -> string_of_int i + | Vinteger i -> BI.string_of_big_int i | Vfloat f -> string_of_float f | Vsexp s -> sexp_string s | Vtype e -> L.lexp_string e ===================================== src/util.ml ===================================== --- a/src/util.ml +++ b/src/util.ml @@ -66,20 +66,23 @@ let typer_unreachable s = raise (Unreachable_error s) (* Section is the name of the compilation step [for debugging] *) (* 'prerr' output is ugly *) let msg_message lvl kind section (loc: location) msg = - if lvl <= !_typer_verbose then( - let info = - " [" ^ loc_string loc ^ "] " ^ loc.file ^ "\n" ^ - " " ^ kind ^ " " ^ (Fmt.lalign_string section 8) ^ " " ^ msg ^ "\n" in - print_string info) else () + if lvl <= !_typer_verbose then + print_string (loc.file + ^ ":" ^ string_of_int loc.line + ^ ":" ^ string_of_int loc.column + ^ ":" ^ kind + ^ (if section = "" then " " else "(" ^ section ^ ") ") + ^ msg ^ "\n") + else () let msg_fatal s l m = msg_message 0 "[X] Fatal " s l m; flush stdout; internal_error "Compiler Fatal Error" -let msg_error = msg_message 1 "[!] Error " -let msg_warning = msg_message 2 "/!\\ Warning " -let msg_info = msg_message 3 "[?] Info " +let msg_error = msg_message 1 "Error:" +let msg_warning = msg_message 2 "Warning:" +let msg_info = msg_message 3 "Info:" (* Compiler Internal Debug print *) let debug_msg expr = View it on GitLab: https://gitlab.com/monnier/typer/commit/befa5609dc00c08f9ae466e92d14b1783bd… --- View it on GitLab: https://gitlab.com/monnier/typer/commit/befa5609dc00c08f9ae466e92d14b1783bd… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][master] Add preliminary support for big-ints
by Stefan 25 Sep '17

25 Sep '17

Stefan pushed to branch master at Stefan / Typer Commits: 9ae0cbe3 by Stefan Monnier at 2017-09-25T15:30:10Z Add preliminary support for big-ints * GNUmakefile (OBFLAGS): Add `nums`. * src/debruijn.ml (type_integer): New type. * src/builtin.ml (register_builtin_csts): Register it. * src/env.ml (value_type): Add big-int constructor. * src/eval.ml (add_binary_biop, add_binary_bool_biop): New functions. Use them to setup new primitives. * btl/builtins.typer (Integer_*): Give them types. - - - - - 6 changed files: - GNUmakefile - btl/builtins.typer - src/builtin.ml - src/debruijn.ml - src/env.ml - src/eval.ml Changes: ===================================== GNUmakefile ===================================== --- a/GNUmakefile +++ b/GNUmakefile @@ -8,7 +8,7 @@ SRC_FILES := $(wildcard ./src/*.ml) CPL_FILES := $(wildcard ./$(BUILDDIR)/src/*.cmo) TEST_FILES := $(wildcard ./tests/*_test.ml) -OBFLAGS = -tag debug -tag profile -build-dir $(BUILDDIR) +OBFLAGS = -tag debug -tag profile -lib nums -build-dir $(BUILDDIR) # OBFLAGS := -I $(SRCDIR) -build-dir $(BUILDDIR) -pkg str # OBFLAGS_DEBUG := -tag debug -tag profile -tag "warn(+20)" # OBFLAGS_RELEASE := -tag unsafe -tag inline ===================================== btl/builtins.typer ===================================== --- a/btl/builtins.typer +++ b/btl/builtins.typer @@ -59,7 +59,7 @@ Eq_comm p = Eq_cast (f := lambda xy -> Eq (t := t) xy x) Eq_refl; %% General recursion!! -%% Whether this breaks onsistency or not is a good question. +%% Whether this breaks consistency or not is a good question. %% The basic idea is the following: %% %% The `witness` argument presumably makes sure that "Y f" can only @@ -92,6 +92,11 @@ _-_ = Built-in "Int.-" (Int -> Int -> Int); _*_ = Built-in "Int.*" (Int -> Int -> Int); _/_ = Built-in "Int./" (Int -> Int -> Int); +Integer_+ = Built-in "Integer.+" (Integer -> Integer -> Integer); +Integer_- = Built-in "Integer.-" (Integer -> Integer -> Integer); +Integer_* = Built-in "Integer.*" (Integer -> Integer -> Integer); +Integer_/ = Built-in "Integer./" (Integer -> Integer -> Integer); + Float_+ = Built-in "Float.+" (Float -> Float -> Float); Float_- = Built-in "Float.-" (Float -> Float -> Float); Float_* = Built-in "Float.*" (Float -> Float -> Float); @@ -108,6 +113,12 @@ Int_eq = Built-in "Int.=" (Int -> Int -> Bool); Int_<= = Built-in "Int.<=" (Int -> Int -> Bool); Int_>= = Built-in "Int.>=" (Int -> Int -> Bool); +Integer_< = Built-in "Integer.<" (Integer -> Integer -> Bool); +Integer_> = Built-in "Integer.>" (Integer -> Integer -> Bool); +Integer_eq = Built-in "Integer.=" (Integer -> Integer -> Bool); +Integer_<= = Built-in "Integer.<=" (Integer -> Integer -> Bool); +Integer_>= = Built-in "Integer.>=" (Integer -> Integer -> Bool); + String_eq = Built-in "String.=" (String -> String -> Bool); Sexp_eq = Built-in "Sexp.=" (Sexp -> Sexp -> Bool); ===================================== src/builtin.ml ===================================== --- a/src/builtin.ml +++ b/src/builtin.ml @@ -154,6 +154,7 @@ let register_builtin_csts () = add_builtin_cst "Type" DB.type0; add_builtin_cst "Type1" DB.type1; add_builtin_cst "Int" DB.type_int; + add_builtin_cst "Integer" DB.type_integer; add_builtin_cst "Float" DB.type_float; add_builtin_cst "String" DB.type_string ===================================== src/debruijn.ml ===================================== --- a/src/debruijn.ml +++ b/src/debruijn.ml @@ -89,6 +89,7 @@ let type0 = mkSort (dloc, Stype level0) let type1 = mkSort (dloc, Stype level1) let type2 = mkSort (dloc, Stype level2) let type_int = mkBuiltin ((dloc, "Int"), type0, None) +let type_integer = mkBuiltin ((dloc, "Integer"), type0, None) let type_float = mkBuiltin ((dloc, "Float"), type0, None) let type_string = mkBuiltin ((dloc, "String"), type0, None) ===================================== src/env.ml ===================================== --- a/src/env.ml +++ b/src/env.ml @@ -38,6 +38,7 @@ open Sexp open Elexp module M = Myers module L = Lexp +module BI = Big_int let dloc = dummy_location @@ -48,6 +49,7 @@ let str_idx idx = "[" ^ (string_of_int idx) ^ "]" type value_type = | Vint of int + | Vinteger of BI.big_int | Vstring of string | Vcons of symbol * value_type list | Vbuiltin of string @@ -67,6 +69,7 @@ type value_type = let rec value_equal a b = match a, b with | Vint (i1), Vint (i2) -> i1 = i2 + | Vinteger (i1), Vinteger (i2) -> BI.eq_big_int i1 i2 | Vstring (s1), Vstring (s2) -> s1 = s2 | Vbuiltin (s1), Vbuiltin (s2) -> s1 = s2 | Vfloat (f1), Vfloat (f2) -> f1 = f2 @@ -107,6 +110,7 @@ let value_name v = | Vin _ -> "Vin" | Vout _ -> "Vout" | Vint _ -> "Vint" + | Vinteger _ -> "Vinteger" | Vsexp _ -> "Vsexp" | Vtype _ -> "Vtype" | Vcons _ -> "Vcons" ===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -157,6 +157,33 @@ let _ = add_binary_bool_iop "<" (<); add_binary_bool_iop ">=" (>=); add_binary_bool_iop "<=" (<=) +let add_binary_biop name f = + let name = "Integer." ^ name in + let f loc (depth : eval_debug_info) (args_val: value_type list) = + match args_val with + | [Vinteger (v); Vinteger (w)] -> Vinteger (f v w) + | _ -> error loc ("`" ^ name ^ "` expects 2 Integer arguments") in + add_builtin_function name f 2 + +let _ = add_binary_biop "+" BI.add_big_int; + add_binary_biop "-" BI.sub_big_int; + add_binary_biop "*" BI.mult_big_int; + add_binary_biop "/" BI.div_big_int + +let add_binary_bool_biop name f = + let name = "Integer." ^ name in + let f loc (depth : eval_debug_info) (args_val: value_type list) = + match args_val with + | [Vinteger (v); Vinteger (w)] -> o2v_bool (f v w) + | _ -> error loc ("`" ^ name ^ "` expects 2 Integer arguments") in + add_builtin_function name f 2 + +let _ = add_binary_bool_biop "<" BI.lt_big_int; + add_binary_bool_biop ">" BI.gt_big_int; + add_binary_bool_biop "=" BI.eq_big_int; + add_binary_bool_biop ">=" BI.ge_big_int; + add_binary_bool_biop "<=" BI.le_big_int + let add_binary_fop name f = let name = "Float." ^ name in let f loc (depth : eval_debug_info) (args_val: value_type list) = View it on GitLab: https://gitlab.com/monnier/typer/commit/9ae0cbe3c74ea3a1965ba2cd48a076fb4e9… --- View it on GitLab: https://gitlab.com/monnier/typer/commit/9ae0cbe3c74ea3a1965ba2cd48a076fb4e9… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][master] Generalize non-recursive let-definitions
by Stefan 24 Sep '17

24 Sep '17

Stefan pushed to branch master at Stefan / Typer Commits: ee53e868 by Stefan Monnier at 2017-09-25T02:21:00Z Generalize non-recursive let-definitions * btl/pervasive.typer (List_head, List_tail, Sexp_to_list.singleton): Let Typer generalize the definition's type. * src/elab.ml (newMetalevel): Add a `loc` argument. (generalize): New function, extracted from infer_and_generalize_type. (track_fv): Adjust to new output of `OL.fv`. (infer_and_generalize_type): Use `generalize`. (infer_and_generalize_def): New function. (lexp_decls_1): Use it for non-recursive definitions. * src/eval.ml (closed_p): Adjust to new output of `OL.fv`. * src/opslexp.ml (mv_set): Add info to keep track of erasability. (mv_set_erase, fv_erase): New functions. (fv): Use them. * src/unification.ml (_unify_metavar.unif): Return None in case of failure of inversion. - - - - - 5 changed files: - btl/pervasive.typer - src/elab.ml - src/eval.ml - src/opslexp.ml - src/unification.ml Changes: ===================================== btl/pervasive.typer ===================================== --- a/btl/pervasive.typer +++ b/btl/pervasive.typer @@ -55,13 +55,12 @@ List_head1 xs = case xs | nil => none | cons hd tl => some hd; -List_head : ?a -> List ?a -> ?a; -List_head x = lambda xs -> case xs +List_head x = lambda xs -> case (xs : List ?a) + %% FIXME: We shouldn't need to annotate `xs` above! | cons x _ => x | nil => x; -List_tail : List ?a -> List ?a; -List_tail xs = case xs +List_tail xs = case (xs : List ?a) % FIXME: Same here. | nil => nil | cons hd tl => tl; @@ -71,8 +70,8 @@ List_map f = lambda xs -> case xs | cons x xs => cons (f x) (List_map f xs); List_foldr : (?b -> ?a -> ?a) -> List ?b -> ?a -> ?a; -List_foldr : (l : TypeLevel) ≡> (a : Type_ l) ≡> (b : Type) - ≡> (b -> a -> a) -> List b -> a -> a; +%% List_foldr : (l : TypeLevel) ≡> (a : Type_ l) ≡> (b : Type) +%% ≡> (b -> a -> a) -> List b -> a -> a; List_foldr f = lambda xs -> lambda i -> case xs | nil => i | cons x xs => f x (List_foldr f xs i); @@ -95,9 +94,9 @@ List_nth = lambda n -> lambda xs -> lambda d -> case xs %% An `Sexp` which we use to represents an *error*. Sexp_error = Sexp_symbol "<error>"; -Sexp_to_list : Sexp -> List Sexp -> List Sexp; +%% Sexp_to_list : Sexp -> List Sexp -> List Sexp; Sexp_to_list s = lambda exceptions -> - let singleton = lambda (a : Type) ≡> lambda (_ : a) -> cons s nil in + let singleton (_ : ?) = cons s nil in %FIXME: Get rid of ": ?"! Sexp_dispatch s (node := lambda head -> lambda tail ===================================== src/elab.ml ===================================== --- a/src/elab.ml +++ b/src/elab.ml @@ -236,11 +236,11 @@ let newMetavar (ctx : lexp_context) sl l name t= let meta = Unif.create_metavar ctx sl t in mkMetavar (meta, S.Identity, (l, name)) -let newMetalevel (ctx : lexp_context) sl = - newMetavar ctx sl Util.dummy_location "l" type_level +let newMetalevel (ctx : lexp_context) sl loc = + newMetavar ctx sl Util.dummy_location "ℓ" type_level let newMetatype (ctx : lexp_context) sl loc - = newMetavar ctx sl loc "t" (mkSort (loc, Stype (newMetalevel ctx sl))) + = newMetavar ctx sl loc "τ" (mkSort (loc, Stype (newMetalevel ctx sl loc))) (* Functions used when we need to return some lexp/ltype but * an error makes it impossible to return "the right one". *) @@ -272,7 +272,7 @@ let elab_varref ctx ((loc, name) as id) (lxp, Inferred ltp) (* Turn metavar into plain vars after generalization. *) -let rec meta_to_var idxs o (e : lexp) = +let rec meta_to_var ids o (e : lexp) = let rec loop e = match e with | Imm _ -> e | SortLevel SLz -> e @@ -288,14 +288,14 @@ let rec meta_to_var idxs o (e : lexp) = let (_, ndefs) = List.fold_right (fun (l,e,t) (o', defs) -> let o' = o' - 1 in - (o', (l, meta_to_var idxs (len + o) e, - meta_to_var idxs (o' + o) t) :: defs)) + (o', (l, meta_to_var ids (len + o) e, + meta_to_var ids (o' + o) t) :: defs)) defs (len, []) in - mkLet (l, ndefs, meta_to_var idxs (len + o) e) + mkLet (l, ndefs, meta_to_var ids (len + o) e) | Arrow (ak, v, t1, l, t2) - -> mkArrow (ak, v, loop t1, l, meta_to_var idxs (1 + o) t2) + -> mkArrow (ak, v, loop t1, l, meta_to_var ids (1 + o) t2) | Lambda (ak, v, t, e) - -> mkLambda (ak, v, loop t, meta_to_var idxs (1 + o) e) + -> mkLambda (ak, v, loop t, meta_to_var ids (1 + o) e) | Call (f, args) -> mkCall (loop f, List.map (fun (ak, e) -> (ak, loop e)) args) | Inductive (l, label, args, cases) @@ -303,7 +303,7 @@ let rec meta_to_var idxs o (e : lexp) = let (_, nargs) = List.fold_right (fun (ak, v, t) (o', args) -> let o' = o' - 1 in - (o', (ak, v, meta_to_var idxs (o' + o) t) + (o', (ak, v, meta_to_var ids (o' + o) t) :: args)) args (alen, []) in let ncases @@ -314,7 +314,7 @@ let rec meta_to_var idxs o (e : lexp) = = List.fold_right (fun (ak, v, t) (o', fields) -> let o' = o' - 1 in - (o', (ak, v, meta_to_var idxs (o' + o) t) + (o', (ak, v, meta_to_var ids (o' + o) t) :: fields)) fields (flen, []) in nfields) @@ -325,18 +325,55 @@ let rec meta_to_var idxs o (e : lexp) = -> let ncases = SMap.map (fun (l, fields, e) - -> (l, fields, meta_to_var idxs (o + List.length fields) e)) + -> (l, fields, meta_to_var ids (o + List.length fields) e)) cases in mkCase (l, loop e, loop t, ncases, match default with None -> None | Some (v, e) -> Some (v, loop e)) | Metavar (id, s, name) - -> if IMap.mem id idxs then - mkVar (name, o + IMap.find id idxs) + -> if IMap.mem id ids then + mkVar (name, o + IMap.find id ids) else match metavar_lookup id with | MVal e -> loop (push_susp e s) | _ -> e in loop e +(* Generalize expression `e` with respect to its uninstantiated metavars. + * `wrap` is the function that adds the relevant quantification, typically + * either mkArrow or mkLambda. *) +let generalize wrap (nctx : elab_context) e = + let l = lexp_location e in + let sl = ectx_to_scope_level nctx in + let cl = Myers.length (ectx_to_lctx nctx) in + let (_, (mfvs, nes)) = OL.fv e in + if mfvs = IMap.empty then e else ( + let mfvs = IMap.fold (fun idx (sl', mt, cl', vname) fvs + -> if sl' < sl then + (* This metavar appears in the context, + * so we can't generalize over it. *) + fvs + else ( + assert (cl' >= cl); + (idx, vname, + if cl' > cl then + Inverse_subst.apply_inv_subst + mt (S.shift (cl' - cl)) + else + mt) + :: fvs)) + mfvs [] in + (* FIXME: Sort `mvfs' topologically! *) + let len = List.length mfvs in + let e = mkSusp e (S.shift len) in + let rec loop ids n mfvs = match mfvs with + | [] -> assert (n = 0); meta_to_var ids 0 e + | ((id, vname, mt) :: mfvs) + -> let mt' = mkSusp mt (S.shift (len - n)) in + let mt'' = meta_to_var ids (- n) mt' in + let n = n - 1 in + let e' = loop (IMap.add id n ids) n mfvs in + wrap (IMap.mem id nes) vname mt'' l e' in + loop (IMap.empty) len mfvs) + (* Infer or check, as the case may be. *) let rec elaborate ctx se ot = match se with @@ -445,11 +482,12 @@ and infer_type pexp ectx var = | _ -> (* FIXME: Here we rule out TypeLevel/TypeOmega. * Maybe it's actually correct?! *) + let l = lexp_location s in match - Unif.unify (mkSort (lexp_location s, - Stype (newMetalevel - (ectx_to_lctx ectx) - (ectx_to_scope_level ectx)))) + Unif.unify (mkSort (l, Stype (newMetalevel + (ectx_to_lctx ectx) + (ectx_to_scope_level ectx) + l))) s (ectx_to_lctx ectx) with | (None | Some (_::_)) @@ -484,10 +522,10 @@ and unify_with_arrow ctx tloc lxp kind var aty ^ " does not match"); (mkDummy_type ctx l, mkDummy_type nctx l) | Some ((t1,t2)::_) - -> lexp_error tloc lxp ("Types `" ^ lexp_string t1 - ^ " and " + -> lexp_error tloc lxp ("Types:\n " ^ lexp_string t1 + ^ "\n and:\n " ^ lexp_string t2 - ^ " do not match"); + ^ "\n do not match!"); (mkDummy_type ctx l, mkDummy_type nctx l) | Some [] -> arg, body @@ -785,7 +823,7 @@ and lexp_parse_inductive ctors ctx = SMap.empty ctors and track_fv rctx lctx e = - let (fvs, mvs) = OL.fv e in + let (fvs, (mvs, _)) = OL.fv e in let nc = EV.not_closed rctx fvs in if nc = [] && not (IMap.is_empty mvs) then "metavars" @@ -883,48 +921,28 @@ and lexp_check_decls (ectx : elab_context) (* External context. *) decls, ctx_define_rec ectx decls and infer_and_generalize_type (ctx : elab_context) se oname = - let l = sexp_location se in let nctx = ectx_new_scope ctx in - let sl = ectx_to_scope_level nctx in - let cl = Myers.length (ectx_to_lctx nctx) in let t = infer_type se nctx oname in match OL.lexp_whnf t (ectx_to_lctx ctx) with (* There's no point generalizing a single metavar, and it's useful * to keep it ungeneralized so you can use `x : ?` to declare that * `x` will be defined later. *) | Metavar _ -> t - | _ - -> let (_, mfvs) = OL.fv t in - if mfvs = IMap.empty then t else ( - let mfvs = IMap.fold (fun idx (sl', mt, cl', vname) fvs - -> if sl' < sl then - (* This metavar appears in the context, - * so we can't generalize over it. *) - fvs - else ( - assert (cl' >= cl); - (idx, vname, - if cl' > cl then - Inverse_subst.apply_inv_subst - mt (S.shift (cl' - cl)) - else - mt) - :: fvs)) - mfvs [] in - (* FIXME: Sort `mvfs' topologically! *) - let len = List.length mfvs in - let t = mkSusp t (S.shift len) in - let rec loop idxs n mfvs = match mfvs with - | [] -> assert (n = 0); meta_to_var idxs 0 t - | ((idx, vname, mt) :: mfvs) - -> let mt' = mkSusp mt (S.shift (len - n)) in - let mt'' = meta_to_var idxs (- n) mt' in - let n = n - 1 in - let t' = loop (IMap.add idx n idxs) n mfvs in - mkArrow (Aerasable, Some vname, mt'', l, - t') in - loop (IMap.empty) len mfvs) + | _ -> generalize (fun _ne vname t l e + -> mkArrow (Aerasable, Some vname, t, l, e)) + nctx t +and infer_and_generalize_def (ctx : elab_context) se = + let nctx = ectx_new_scope ctx in + let (e,t) = infer se nctx in + let e' = generalize (fun ne vname t l e + -> mkLambda ((if ne then Aimplicit else Aerasable), + vname, t, e)) + nctx e in + if e == e' + then (e, t) + (* FIXME: Compute type directly instead of going through `e'`. *) + else (e', OL.get_type (ectx_to_lctx ctx) e') and lexp_decls_1 (sdecls : sexp list) @@ -989,7 +1007,7 @@ and lexp_decls_1 -> assert (pending_defs == []); (* Used to be true before we added define-operator. *) (* assert (ectx == nctx); *) - let (lexp, ltp) = infer sexp (ectx_new_scope nctx) in + let (lexp, ltp) = infer_and_generalize_def nctx sexp in (* Lexp decls are always recursive, so we have to shift by 1 to * account for the extra var (ourselves). *) [(v, mkSusp lexp (S.shift 1), ltp)], sdecls, ===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -670,7 +670,7 @@ let not_closed rctx ((o, vm) : DB.set) = match !rc with Vundefined -> i::nc | _ -> nc) vm [] -let closed_p rctx (fvs, mvs) = +let closed_p rctx (fvs, (mvs, _)) = not_closed rctx fvs = [] (* FIXME: Handle metavars! *) && IMap.is_empty mvs ===================================== src/opslexp.ml ===================================== --- a/src/opslexp.ml +++ b/src/opslexp.ml @@ -624,10 +624,12 @@ let rec list_union l1 l2 = match l1 with | (x::l1) -> list_union l1 (if List.mem x l2 then l2 else (x::l2)) type mv_set = (scope_level * ltype * scope_length * vname) IMap.t -let mv_set_empty = IMap.empty -let mv_set_add ms m x = IMap.add m x ms -let mv_set_union : mv_set -> mv_set -> mv_set - = IMap.merge (fun m oss1 oss2 + (* Metavars that appear in non-erasable positions. *) + * unit IMap.t +let mv_set_empty : mv_set = (IMap.empty, IMap.empty) +let mv_set_add (ms, nes) id x : mv_set = (IMap.add id x ms, IMap.add id () nes) +let mv_set_union ((ms1, nes1) : mv_set) ((ms2, nes2) : mv_set) : mv_set + = (IMap.merge (fun _m oss1 oss2 -> match (oss1, oss2) with | (None, _) -> oss2 | (_, None) -> oss1 @@ -640,6 +642,9 @@ let mv_set_union : mv_set -> mv_set -> mv_set assert (len1 = len2); assert (name2 = name1)); Some ss1) + ms1 ms2, + IMap.merge (fun _m _o1 _o2 -> Some ()) nes1 nes2) +let mv_set_erase (ms, _nes) = (ms, IMap.empty) module LMap (* Memoization table. FIXME: Ideally the keys should be "weak", but @@ -653,6 +658,7 @@ let fv_union (fv1, mv1) (fv2, mv2) = (DB.set_union fv1 fv2, mv_set_union mv1 mv2) let fv_sink n (fvs, mvs) = (DB.set_sink n fvs, mvs) let fv_hoist n (fvs, mvs) = (DB.set_hoist n fvs, mvs) +let fv_erase (fvs, mvs) = (fvs, mv_set_erase mvs) let rec fv (e : lexp) : (DB.set * mv_set) = let fv' e = match e with @@ -667,18 +673,23 @@ let rec fv (e : lexp) : (DB.set * mv_set) = | Susp (e, s) -> fv (push_susp e s) | Let (_, defs, e) -> let len = List.length defs in - let (s, _) - = List.fold_left (fun (s, o) (_, e, t) - -> (fv_union s (fv_union (fv_sink o (fv t)) - (fv e)), + let (fvs, _) + = List.fold_left (fun (fvs, o) (_, e, t) + -> (fv_union fvs (fv_union (fv_erase + (fv_sink o (fv t))) + (fv e)), o - 1)) (fv e, len) defs in - fv_hoist len s + fv_hoist len fvs | Arrow (_, _, t1, _, t2) -> fv_union (fv t1) (fv_hoist 1 (fv t2)) - | Lambda (_, _, t, e) -> fv_union (fv t) (fv_hoist 1 (fv e)) + | Lambda (_, _, t, e) -> fv_union (fv_erase (fv t)) (fv_hoist 1 (fv e)) | Call (f, args) - -> List.fold_left (fun s (_, arg) - -> fv_union s (fv arg)) + -> List.fold_left (fun fvs (ak, arg) + -> let afvs = fv arg in + fv_union fvs + (if ak = P.Aerasable + then fv_erase afvs + else afvs)) (fv f) args | Inductive (_, _, args, cases) -> let alen = List.length args in @@ -697,22 +708,24 @@ let rec fv (e : lexp) : (DB.set * mv_set) = fv_empty fields))) cases s in fv_hoist alen s - | Cons (t, _) -> fv t + | Cons (t, _) -> fv_erase (fv t) | Case (_, e, t, cases, def) - -> let s = fv_union (fv e) (fv t) in + -> let s = fv_union (fv e) (fv_erase (fv t)) in let s = match def with | None -> s | Some (_, e) -> fv_union s (fv_hoist 1 (fv e)) in SMap.fold (fun _ (_, fields, e) s -> fv_union s (fv_hoist (List.length fields) (fv e))) cases s - | Metavar (m, s, name) - -> (match metavar_lookup m with + | Metavar (id, s, name) + -> (match metavar_lookup id with | MVal e -> fv (push_susp e s) | MVar (sl, t, cl) - -> let (fvs, mvs) = fv (push_susp t s) in - (fvs, mv_set_add mvs m (sl, t, cl, name))) + -> let (fvs, mvs) = fv_erase (fv (push_susp t s)) in + (fvs, mv_set_add mvs id (sl, t, cl, name))) in + (* FIXME: Flush the memoization table whenever the metavar table + * is modified, since that can affect the output of `fv`. *) try LMap.find fv_memo e with Not_found -> let r = fv' e in ===================================== src/unification.ml ===================================== --- a/src/unification.ml +++ b/src/unification.ml @@ -167,24 +167,25 @@ and _unify_metavar ctx idx s (lxp1: lexp) (lxp2: lexp) | MVal _ -> U.internal_error "`lexp_whnf` returned an instantiated metavar!!" | MVar (_, t, _) -> push_susp t s in - let lxp' = try Inverse_subst.apply_inv_subst lxp s with - | Inverse_subst.Not_invertible - -> print_string "Not_invertible:\n "; - lexp_print lxp; + match Inverse_subst.apply_inv_subst lxp s with + | exception Inverse_subst.Not_invertible + -> print_string "Unification of metavar failed:\n "; + print_string ("?[" ^ subst_string s ^ "]"); print_string "\nAgainst:\n "; - print_string (subst_string s); + lexp_print lxp; print_string "\n"; - lxp in - metavar_table := associate idx lxp' (!metavar_table); - match unify t (OL.get_type ctx lxp) ctx with - | Some [] as r -> r - (* FIXME: Let's ignore the error for now. *) - | _ - -> print_string ("Unification of metavar type failed:\n " - ^ lexp_string (Lexp.clean t) ^ " != " - ^ lexp_string (Lexp.clean (OL.get_type ctx lxp)) - ^ "\n" ^ "for " ^ lexp_string lxp ^ "\n"); - Some [] in + None + | lxp' + -> metavar_table := associate idx lxp' (!metavar_table); + match unify t (OL.get_type ctx lxp) ctx with + | Some [] as r -> r + (* FIXME: Let's ignore the error for now. *) + | _ + -> print_string ("Unification of metavar type failed:\n " + ^ lexp_string (Lexp.clean t) ^ " != " + ^ lexp_string (Lexp.clean (OL.get_type ctx lxp)) + ^ "\n" ^ "for " ^ lexp_string lxp ^ "\n"); + Some [] in match lxp2 with | Metavar (idx2, s2, _) -> if idx = idx2 then View it on GitLab: https://gitlab.com/monnier/typer/commit/ee53e86819ca2da07ec4d91725276406c9c… --- View it on GitLab: https://gitlab.com/monnier/typer/commit/ee53e86819ca2da07ec4d91725276406c9c… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][master] Auto-generalize variable's type declarations
by Stefan 19 Sep '17

19 Sep '17

Stefan pushed to branch master at Stefan / Typer Commits: 494d60da by Stefan Monnier at 2017-09-19T20:30:58Z Auto-generalize variable's type declarations * btl/pervasive.typer: Simplify declarations, relying on generalization. * src/debruijn.ml (scope): Remove. (meta_scope): New type alias. (elab_context): Use it to add a map of known metavar names. (empty_elab_context, ectx_new_scope): Handle the new metavar map. (get_size): Add sanity check. * src/elab.ml (meta_to_var, infer_and_generalize_type): New functions. (lexp_decls_1): Use them to generalize var declarations. (sform_identifier): Use new metavar map to handle names metavars. * src/inverse_subst.ml (invertible, lookup_inv_subst) (shift_inv_subst, compose_inv_subst, apply_inv_subst): New functions. * src/lexp.ml (meta_id): New type alias. (lexp): Use it. * src/opslexp.ml (mv_set): Keep track of types, names, and (meta)scope. (mv_set_union): Adjust accordingly. * src/unification.ml (_unify_metavar): Use apply_inv_subst! - - - - - 7 changed files: - btl/pervasive.typer - src/debruijn.ml - src/elab.ml - src/inverse_subst.ml - src/lexp.ml - src/opslexp.ml - src/unification.ml Changes: ===================================== btl/pervasive.typer ===================================== --- a/btl/pervasive.typer +++ b/btl/pervasive.typer @@ -38,7 +38,7 @@ none = datacons Option none; %%%% List functions -List_length : (a : Type) ≡> List a -> Int; +List_length : List ?a -> Int; List_length xs = case xs | nil => 0 | cons hd tl => @@ -49,37 +49,40 @@ List_length xs = case xs %% - Provide a default value : `a -> List a -> a`; %% - Disallow problem case : `(l : List a) -> (l != nil) -> a`; %% - Return an Option/Error +List_head1 : List ?a -> Option ?a; List_head1 : (a : Type) ≡> List a -> Option a; List_head1 xs = case xs | nil => none | cons hd tl => some hd; -List_head : (a : Type) ≡> a -> List a -> a; +List_head : ?a -> List ?a -> ?a; List_head x = lambda xs -> case xs | cons x _ => x | nil => x; -List_tail : (a : Type) ≡> List a -> List a; +List_tail : List ?a -> List ?a; List_tail xs = case xs | nil => nil | cons hd tl => tl; -List_map : (a : Type) ≡> (b : Type) ≡> (a -> b) -> List a -> List b; +List_map : (?a -> ?b) -> List ?a -> List ?b; List_map f = lambda xs -> case xs | nil => nil | cons x xs => cons (f x) (List_map f xs); -List_foldr : (a : Type) ≡> (b : Type) ≡> (b -> a -> a) -> List b -> a -> a; +List_foldr : (?b -> ?a -> ?a) -> List ?b -> ?a -> ?a; +List_foldr : (l : TypeLevel) ≡> (a : Type_ l) ≡> (b : Type) + ≡> (b -> a -> a) -> List b -> a -> a; List_foldr f = lambda xs -> lambda i -> case xs | nil => i | cons x xs => f x (List_foldr f xs i); -List_find : (a : Type) ≡> (a -> Bool) -> List a -> Option a; +List_find : (?a -> Bool) -> List ?a -> Option ?a; List_find f = lambda xs -> case xs | nil => none | cons x xs => case f x | true => some x | false => List_find f xs; -List_nth : (a : Type) ≡> Int -> List a -> a -> a; +List_nth : Int -> List ?a -> ?a -> ?a; List_nth = lambda n -> lambda xs -> lambda d -> case xs | nil => d | cons x xs @@ -139,24 +142,29 @@ lambda_≡>_ = macro (multiarg_lambda "##lambda_≡>_"); %%%% More list functions -List_reverse : (a : Type) ≡> List a -> List a -> List a; +List_reverse : List ?a -> List ?a -> List ?a; List_reverse l t = case l | nil => t | cons hd tl => List_reverse tl (cons hd t); -List_concat : (a : Type) ≡> List a -> List a -> List a; +List_concat : List ?a -> List ?a -> List ?a; List_concat l t = List_reverse (List_reverse l nil) t; -List_foldl : (a : Type) ≡> (b : Type) ≡> (a -> b -> a) -> a -> List b -> a; +List_foldl : (?a -> ?b -> ?a) -> ?a -> List ?b -> ?a; List_foldl f i xs = case xs | nil => i | cons x xs => List_foldl f (f i x) xs; %%% Good 'ol combinators -I : (a : Type) ≡> a -> a; +I : ?a -> ?a; I x = x; +%% Use explicit erasable annotations since with an annotation like +%% K : ?a -> ?b -> ?a; +%% Typer generalizes to +%% K : (a : Type) ≡> (b : Type) ≡> a -> b -> a; +%% Which is less general. K : (a : Type) ≡> a -> (b : Type) ≡> b -> a; K x y = x; ===================================== src/debruijn.ml ===================================== --- a/src/debruijn.ml +++ b/src/debruijn.ml @@ -98,21 +98,25 @@ type lexp_context = env_elem M.myers type db_ridx = int (* DeBruijn reverse index (i.e. counting from the root). *) -(* Map matching variable name and its distance in the current scope *) -type scope = db_ridx SMap.t (* Map<String, db_ridx>*) - +(* Map variable name to its distance in the context *) type senv_length = int (* it is not the map true length *) -type senv_type = senv_length * scope +type senv_type = senv_length * (db_ridx SMap.t) type lctx_length = db_ridx +type meta_scope + = scope_level (* Integer identifying a level. *) + * lctx_length (* Length of ctx when the scope is added. *) + * (meta_id SMap.t ref) (* Metavars already known in this scope. *) + (* This is the *elaboration context* (i.e. a context that holds * a lexp context plus some side info. *) type elab_context - = Grammar.grammar * senv_type * lexp_context * (scope_level * lctx_length) + = Grammar.grammar * senv_type * lexp_context * meta_scope -let get_size ctx = let (_, (n, _), lctx, _) = ctx in - assert (n = M.length lctx); n +let get_size (ctx : elab_context) + = let (_, (n, _), lctx, _) = ctx in + assert (n = M.length lctx); n let ectx_to_grm (ectx : elab_context) : Grammar.grammar = let (grm,_, _, _) = ectx in grm @@ -121,9 +125,10 @@ let ectx_to_grm (ectx : elab_context) : Grammar.grammar = let ectx_to_lctx (ectx : elab_context) : lexp_context = let (_,_, lctx, _) = ectx in lctx -let ectx_to_scope_level ((_, _, _, (sl, _)) : elab_context) : scope_level = sl +let ectx_to_scope_level ((_, _, _, (sl, _, _)) : elab_context) : scope_level + = sl -let ectx_local_scope_size ((_, (n, _), _, (_, slen)) as ectx: elab_context) : int +let ectx_local_scope_size ((_, (n, _), _, (_, slen, _)) as ectx) : int = get_size ectx - slen (* internal definitions @@ -137,7 +142,8 @@ let _make_myers = M.nil * ---------------------------------- *) let empty_elab_context : elab_context - = (Grammar.default_grammar, _make_senv_type, _make_myers, (0, 0)) + = (Grammar.default_grammar, _make_senv_type, _make_myers, + (0, 0, ref SMap.empty)) (* return its current DeBruijn index *) let rec senv_lookup (name: string) (ctx: elab_context): int = @@ -193,11 +199,11 @@ let ectx_extend_rec (ctx: elab_context) (defs: (vname * lexp * ltype) list) = (senv, n) defs in (grm, (n + List.length defs, senv'), lctx_extend_rec lctx defs, sl) -let ectx_new_scope ectx : elab_context = - let (grm, senv, lctx, (scope, _)) = ectx in - (grm, senv, lctx, (scope + 1, Myers.length lctx)) +let ectx_new_scope (ectx : elab_context) : elab_context = + let (grm, senv, lctx, (scope, _, rmmap)) = ectx in + (grm, senv, lctx, (scope + 1, Myers.length lctx, ref (!rmmap))) -let ectx_get_scope (ectx : elab_context) : (scope_level * lctx_length) = +let ectx_get_scope (ectx : elab_context) : meta_scope = let (_, _, _, sl) = ectx in sl let ectx_get_grammar (ectx : elab_context) : Grammar.grammar = ===================================== src/elab.ml ===================================== --- a/src/elab.ml +++ b/src/elab.ml @@ -271,6 +271,72 @@ let elab_varref ctx ((loc, name) as id) let ltp = env_lookup_type ctx (id, idx) in (lxp, Inferred ltp) +(* Turn metavar into plain vars after generalization. *) +let rec meta_to_var idxs o (e : lexp) = + let rec loop e = match e with + | Imm _ -> e + | SortLevel SLz -> e + | SortLevel (SLsucc e) -> mkSortLevel (SLsucc (loop e)) + | SortLevel (SLlub (e1, e2)) -> mkSortLevel (SLlub (loop e1, loop e2)) + | Sort (l, Stype e) -> mkSort (l, Stype (loop e)) + | Sort (_, (StypeOmega | StypeLevel)) -> e + | Builtin _ -> e + | Var _ -> e + | Susp (e, s) -> loop (push_susp e s) + | Let (l, defs, e) + -> let len = List.length defs in + let (_, ndefs) + = List.fold_right (fun (l,e,t) (o', defs) + -> let o' = o' - 1 in + (o', (l, meta_to_var idxs (len + o) e, + meta_to_var idxs (o' + o) t) :: defs)) + defs (len, []) in + mkLet (l, ndefs, meta_to_var idxs (len + o) e) + | Arrow (ak, v, t1, l, t2) + -> mkArrow (ak, v, loop t1, l, meta_to_var idxs (1 + o) t2) + | Lambda (ak, v, t, e) + -> mkLambda (ak, v, loop t, meta_to_var idxs (1 + o) e) + | Call (f, args) + -> mkCall (loop f, List.map (fun (ak, e) -> (ak, loop e)) args) + | Inductive (l, label, args, cases) + -> let alen = List.length args in + let (_, nargs) + = List.fold_right (fun (ak, v, t) (o', args) + -> let o' = o' - 1 in + (o', (ak, v, meta_to_var idxs (o' + o) t) + :: args)) + args (alen, []) in + let ncases + = SMap.map + (fun fields + -> let flen = List.length fields in + let (_, nfields) + = List.fold_right + (fun (ak, v, t) (o', fields) + -> let o' = o' - 1 in + (o', (ak, v, meta_to_var idxs (o' + o) t) + :: fields)) + fields (flen, []) in + nfields) + cases in + mkInductive (l, label, nargs, ncases) + | Cons (t, l) -> mkCons (loop t, l) + | Case (l, e, t, cases, default) + -> let ncases + = SMap.map + (fun (l, fields, e) + -> (l, fields, meta_to_var idxs (o + List.length fields) e)) + cases in + mkCase (l, loop e, loop t, ncases, + match default with None -> None | Some (v, e) -> Some (v, loop e)) + | Metavar (id, s, name) + -> if IMap.mem id idxs then + mkVar (name, o + IMap.find id idxs) + else match metavar_lookup id with + | MVal e -> loop (push_susp e s) + | _ -> e + in loop e + (* Infer or check, as the case may be. *) let rec elaborate ctx se ot = match se with @@ -816,6 +882,49 @@ and lexp_check_decls (ectx : elab_context) (* External context. *) let decls = List.rev (List.map (fun (_, d) -> d) (IMap.bindings declmap)) in decls, ctx_define_rec ectx decls +and infer_and_generalize_type (ctx : elab_context) se oname = + let l = sexp_location se in + let nctx = ectx_new_scope ctx in + let sl = ectx_to_scope_level nctx in + let cl = Myers.length (ectx_to_lctx nctx) in + let t = infer_type se nctx oname in + match OL.lexp_whnf t (ectx_to_lctx ctx) with + (* There's no point generalizing a single metavar, and it's useful + * to keep it ungeneralized so you can use `x : ?` to declare that + * `x` will be defined later. *) + | Metavar _ -> t + | _ + -> let (_, mfvs) = OL.fv t in + if mfvs = IMap.empty then t else ( + let mfvs = IMap.fold (fun idx (sl', mt, cl', vname) fvs + -> if sl' < sl then + (* This metavar appears in the context, + * so we can't generalize over it. *) + fvs + else ( + assert (cl' >= cl); + (idx, vname, + if cl' > cl then + Inverse_subst.apply_inv_subst + mt (S.shift (cl' - cl)) + else + mt) + :: fvs)) + mfvs [] in + (* FIXME: Sort `mvfs' topologically! *) + let len = List.length mfvs in + let t = mkSusp t (S.shift len) in + let rec loop idxs n mfvs = match mfvs with + | [] -> assert (n = 0); meta_to_var idxs 0 t + | ((idx, vname, mt) :: mfvs) + -> let mt' = mkSusp mt (S.shift (len - n)) in + let mt'' = meta_to_var idxs (- n) mt' in + let n = n - 1 in + let t' = loop (IMap.add idx n idxs) n mfvs in + mkArrow (Aerasable, Some vname, mt'', l, + t') in + loop (IMap.empty) len mfvs) + and lexp_decls_1 (sdecls : sexp list) @@ -844,7 +953,7 @@ and lexp_decls_1 (* FIXME: Move this to a "special form"! *) -> (match args with | [Symbol ((l, vname) as v); stp] - -> let ltp = infer_type stp (ectx_new_scope nctx) (Some v) in + -> let ltp = infer_and_generalize_type nctx stp (Some v) in if SMap.mem vname pending_decls then (* Don't burp: take'em all and unify! *) let pt_idx = senv_lookup vname nctx in @@ -1161,8 +1270,7 @@ let sform_identifier ctx loc sargs ot = when String.length name >= 1 && String.get name 0 = '?' -> assert (String.length name >= 1 && String.get name 0 = '?'); let name = if name = "?" then "" else - (sexp_error loc "Named metavars not supported (yet)"; - String.sub name 1 (String.length name)) in + string_sub name 1 (String.length name) in (* Shift the var so it can't refer to the local vars. * This is used so that in cases like "lambda t (y : ?) ... " * type inference can guess ? without having to wonder whether it @@ -1172,14 +1280,23 @@ let sform_identifier ctx loc sargs ot = let octx = Myers.nthcdr ctx_shift (ectx_to_lctx ctx) in let sl = ectx_to_scope_level ctx in let subst = S.shift ctx_shift in - let t = match ot with - | None -> newMetatype octx sl loc - (* FIXME: `t` is defined in ctx instead of octx. - * We need something like: - * let t = push_inv_subst t (S.shift ctx_shift) in *) - | Some t -> t in - (mkSusp (newMetavar octx sl loc name t) subst, - match ot with Some _ -> Checked | None -> Lazy) + let (_, _, rmmap) = ectx_get_scope ctx in + if not (name = "") && SMap.mem name (!rmmap) then + (mkMetavar (SMap.find name (!rmmap), subst, (loc, name)), Lazy) + else + let t = match ot with + | None -> newMetatype octx sl loc + | Some t + (* `t` is defined in ctx instead of octx. *) + -> Inverse_subst.apply_inv_subst t subst in + let mv = newMetavar octx sl loc name t in + (if not (name = "") then + let idx = match mv with + | Metavar (idx, _, _) -> idx + | _ -> fatal loc "newMetavar returned a non-Metavar" in + rmmap := SMap.add name idx (!rmmap)); + (mkSusp mv subst, + match ot with Some _ -> Checked | None -> Lazy) (* Normal identifier. *) | [Symbol id] ===================================== src/inverse_subst.ml ===================================== --- a/src/inverse_subst.ml +++ b/src/inverse_subst.ml @@ -56,8 +56,8 @@ type substIR = ((int * int) list * int * int) (** Transform a substitution to a more linear substitution * makes the inversion easier * Example of result : ((new_idx, old_position)::..., shift)*) -let transfo (s: lexp S.subst) : substIR option = - let rec transfo (s: lexp S.subst) (off_acc: int) (idx: int) (imp_cnt : int) +let transfo (s: Lexp.subst) : substIR option = + let rec transfo (s: Lexp.subst) (off_acc: int) (idx: int) (imp_cnt : int) : substIR option = let indexOf (v: lexp): int = (* Helper : return the index of a variabble *) match v with @@ -92,7 +92,7 @@ let rec sizeOf (s: (int * int) list): int = List.length s let counter = ref 0 let mkVar (idx: int) : lexp = counter := !counter + 1; - Var((U.dummy_location, "<anon" ^ string_of_int idx ^ ">"), idx) + Lexp.mkVar ((U.dummy_location, "<anon" ^ string_of_int idx ^ ">"), idx) (** Fill the gap between e_i in the list of couple (e_i, i) by adding dummy variables. @@ -103,18 +103,18 @@ let mkVar (idx: int) : lexp = @param size size of the list to return @param acc recursion accumulator *) -let fill (l: (int * int) list) (nbVar: int) (shift: int): lexp S.subst option = - let rec genDummyVar (beg_: int) (end_: int) (l: lexp S.subst): lexp S.subst = (* Create the filler variables *) +let fill (l: (int * int) list) (nbVar: int) (shift: int): Lexp.subst option = + let rec genDummyVar (beg_: int) (end_: int) (l: Lexp.subst): Lexp.subst = (* Create the filler variables *) if beg_ < end_ then S.cons impossible (genDummyVar (beg_ + 1) end_ l) else l in - let fill_before (l: (int * int) list) (s: lexp S.subst) (nbVar: int): lexp S.subst option = (* Fill if the first var is not 0 *) + let fill_before (l: (int * int) list) (s: Lexp.subst) (nbVar: int): Lexp.subst option = (* Fill if the first var is not 0 *) match l with | [] -> Some (genDummyVar 0 nbVar s) | (i1, v1)::_ when i1 > 0 -> Some (genDummyVar 0 i1 s) | _ -> Some s - in let rec fill_after (l: (int * int) list) (nbVar: int) (shift: int): lexp S.subst option = (* Fill gaps *) + in let rec fill_after (l: (int * int) list) (nbVar: int) (shift: int): Lexp.subst option = (* Fill gaps *) match l with | (idx1, val1)::(idx2, val2)::tail when (idx1 = idx2) -> None @@ -153,7 +153,7 @@ let is_identity s = <code>s:S.subst, l:lexp, s':S.subst</code> where <code>l[s][s'] = l</code> and <code> inverse s = s' </code> *) -let inverse (s: lexp S.subst) : lexp S.subst option = +let inverse (s: Lexp.subst) : Lexp.subst option = let sort = List.sort (fun (ei1, _) (ei2, _) -> compare ei1 ei2) in match transfo s with | None -> None @@ -175,3 +175,136 @@ let inverse (s: lexp S.subst) : lexp S.subst option = ^ " !!\n")) | _ -> ()); res + +(* Returns false if the application of the inverse substitution is not + * possible. This happens when the substitution replaces some variables + * with non-variables, in which case the "inverse" is ambiguous. *) +let rec invertible (s: subst) : bool = match s with + | S.Identity -> true + | S.Shift (s, _) -> invertible s + | S.Cons (e, s) -> (match e with Var _ -> true | _ -> e = impossible) + && invertible s + +exception Not_invertible +exception Ambiguous + +(* Lookup variable i in s⁻¹ *) +let rec lookup_inv_subst (i : db_index) (s : subst) : db_index + = match s with + | S.Identity -> i + | S.Shift (s, n) -> if i < n then + raise Not_invertible + else lookup_inv_subst (i - n) s + | S.Cons (Var (_, i'), s) when i' = i + -> (try let i'' = lookup_inv_subst i s in + assert (i'' != 0); + raise Ambiguous + with Not_invertible -> 0) + | S.Cons (e, s) + -> assert (match e with Var _ -> true | _ -> e = impossible); + 1 + lookup_inv_subst i s + +(* When going under a binder, we have the rule + * (λe)[s] ==> λ(e[lift s]) + * where `lift s` is (#0 · (s ↑1)) + * + * Here, we want to construct a substitution s' such that + * + * (λe)[s⁻¹] ==> λ(e[s'⁻¹]) + * + * So (lift_inv_subst s) is morally equivalent to ((lift (s⁻¹))⁻¹). + * And it turns out that ((lift (s⁻¹))⁻¹) = lift s: + *) + +(* Return a substitution s' = (↑n ∘ (s⁻¹))⁻¹ = ((s⁻¹)⁻¹ ∘ (↑n)⁻¹) = (s ∘ (↑n)⁻¹) + * ↑n is a substitution of type Γ → Γ,x₁,…,xₙ + * So `s⁻¹` should be a substitution Γ,x₁,…,xₙ → Γ' + * Hence `s` should be a substitution Γ' → Γ,x₁,…,xₙ + * and we need to return a substitution Γ' → Γ + *) +let shift_inv_subst n s + (* We could define it as: + * = compose_inv_subst s (S.shift n) + * But this can fail if an element of `s` maps to a var with index < n *) + = let shift_n = match inverse (S.shift n) with + | Some s -> s + | _ -> assert (false) in + Lexp.scompose s shift_n + +(* For metavars, we need to compute: s' ∘ s⁻¹ + * One way to do it is to compute s⁻¹ and then pass it to `compose`. + * But we can try and do it more directly. + *) +let rec compose_inv_subst (s' : subst) (s : subst) = match s' with + | S.Cons (e, s') -> S.Cons (apply_inv_subst e s, compose_inv_subst s' s) + | S.Identity -> (match inverse s with + | Some s -> s + (* FIXME: could also be Ambiguous, depending on `s`. *) + | None -> raise Not_invertible) + | S.Shift (s', n) + -> compose_inv_subst s' (shift_inv_subst n s) + +(* Apply s⁻¹ to e. + * The function presumes that `invertible s` was true. + * This can be used like mkSusp/push_susp, but it's not lazy. + * This is because it can signal errors Not_invertible or Ambiguous. *) +and apply_inv_subst (e : lexp) (s : subst) : lexp = match e with + | Imm _ -> e + | SortLevel (SLz) -> e + | SortLevel (SLsucc e) -> mkSortLevel (SLsucc (apply_inv_subst e s)) + | SortLevel (SLlub (e1, e2)) + -> mkSortLevel (SLlub (apply_inv_subst e1 s, apply_inv_subst e2 s)) + | Sort (l, Stype e) -> mkSort (l, Stype (apply_inv_subst e s)) + | Sort (l, (StypeOmega | StypeLevel)) -> e + | Builtin _ -> e + | Var (name, i) -> Lexp.mkVar (name, lookup_inv_subst i s) + | Susp (e, s') -> apply_inv_subst (push_susp e 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) + -> (ssink v s, + (v, apply_inv_subst def s', apply_inv_subst ty s) + :: ndefs)) + (s, []) defs in + mkLet (l, ndefs, apply_inv_subst e s') + | Arrow (ak, v, t1, l, t2) + -> mkArrow (ak, v, apply_inv_subst t1 s, l, + apply_inv_subst t2 (ssink (maybev v) s)) + | Lambda (ak, v, t, e) + -> mkLambda (ak, v, apply_inv_subst t s, apply_inv_subst e (ssink v s)) + | Call (f, args) + -> mkCall (apply_inv_subst f s, + L.map (fun (ak, arg) -> (ak, apply_inv_subst arg s)) args) + | Inductive (l, label, args, cases) + -> let (s, nargs) + = L.fold_left (fun (s, nargs) (ak, v, t) + -> (ssink v s, (ak, v, apply_inv_subst t s) :: nargs)) + (s, []) args in + let nargs = List.rev nargs in + let ncases = SMap.map (fun args + -> let (_, ncase) + = L.fold_left (fun (s, nargs) (ak, v, t) + -> (ssink (maybev v) s, + (ak, v, apply_inv_subst t s) + :: nargs)) + (s, []) args in + L.rev ncase) + cases in + mkInductive (l, label, nargs, ncases) + | Cons (it, name) -> Cons (apply_inv_subst it s, name) + | Case (l, e, ret, cases, default) + -> mkCase (l, apply_inv_subst e s, apply_inv_subst ret s, + SMap.map (fun (l, cargs, e) + -> let s' = L.fold_left + (fun s (_,ov) -> ssink (maybev ov) s) + s cargs in + (l, cargs, apply_inv_subst e s')) + cases, + match default with + | None -> default + | Some (v,e) -> Some (v, apply_inv_subst e (ssink (maybev v) s))) + | Metavar (id, s', name) + -> match metavar_lookup id with + | MVal e -> apply_inv_subst (push_susp e s') s + | MVar _ -> mkMetavar (id, compose_inv_subst s' s, name) ===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -36,6 +36,7 @@ module S = Subst type vname = U.vname type vref = U.vref +type meta_id = int (* Identifier of a meta variable. *) type label = symbol @@ -81,7 +82,7 @@ type ltype = lexp * (vname option * lexp) option (* Default. *) (* The `subst` only applies to the lexp associated * with the metavar's "value", not to the ltype. *) - | Metavar of int * subst * vname + | Metavar of meta_id * subst * vname (* (\* For logical metavars, there's no substitution. *\) * | Metavar of (U.location * string) * metakind * metavar ref * and metavar = @@ -162,8 +163,8 @@ let impossible = Imm Sexp.dummy_epsilon let builtin_size = ref 0 let metavar_table = ref (U.IMap.empty : meta_subst) -let metavar_lookup idx : metavar_info - = try U.IMap.find idx (!metavar_table) +let metavar_lookup (id : meta_id) : metavar_info + = try U.IMap.find id (!metavar_table) with Not_found -> U.msg_fatal "LEXP" U.dummy_location "metavar lookup failure!" ===================================== src/opslexp.ml ===================================== --- a/src/opslexp.ml +++ b/src/opslexp.ml @@ -623,19 +623,23 @@ let rec list_union l1 l2 = match l1 with | [] -> l2 | (x::l1) -> list_union l1 (if List.mem x l2 then l2 else (x::l2)) -type mv_set = subst list IMap.t +type mv_set = (scope_level * ltype * scope_length * vname) IMap.t let mv_set_empty = IMap.empty -let mv_set_add ms m s - = let ss = try IMap.find m ms with Not_found -> [] in - if List.mem s ss then ms - else IMap.add m (s::ss) ms +let mv_set_add ms m x = IMap.add m x ms let mv_set_union : mv_set -> mv_set -> mv_set = IMap.merge (fun m oss1 oss2 -> match (oss1, oss2) with | (None, _) -> oss2 | (_, None) -> oss1 | (Some ss1, Some ss2) - -> Some (list_union ss1 ss2)) + -> (let ((sl1, t1, len1, (_, name1)), + (sl2, t2, len2, (_, name2))) + = (ss1, ss2) in + assert (sl1 = sl2); + assert (t1 = t2); + assert (len1 = len2); + assert (name2 = name1)); + Some ss1) module LMap (* Memoization table. FIXME: Ideally the keys should be "weak", but @@ -702,12 +706,12 @@ let rec fv (e : lexp) : (DB.set * mv_set) = SMap.fold (fun _ (_, fields, e) s -> fv_union s (fv_hoist (List.length fields) (fv e))) cases s - | Metavar (m, s, _) + | Metavar (m, s, name) -> (match metavar_lookup m with | MVal e -> fv (push_susp e s) - | MVar (_, t, _) + | MVar (sl, t, cl) -> let (fvs, mvs) = fv (push_susp t s) in - (fvs, mv_set_add mvs m s)) + (fvs, mv_set_add mvs m (sl, t, cl, name))) in try LMap.find fv_memo e with Not_found ===================================== src/unification.ml ===================================== --- a/src/unification.ml +++ b/src/unification.ml @@ -162,23 +162,29 @@ and _unify_lambda (lambda: lexp) (lxp: lexp) ctx vs : return_type = *) and _unify_metavar ctx idx s (lxp1: lexp) (lxp2: lexp) : return_type = - let unif idx s lxp = match Inverse_subst.inverse s with - | None -> None - | Some s' - -> let t = match metavar_lookup idx with - | MVal _ -> U.internal_error - "`lexp_whnf` returned an instantiated metavar!!" - | MVar (_, t, _) -> push_susp t s in - metavar_table := associate idx (mkSusp lxp s') (!metavar_table); - match unify t (OL.get_type ctx lxp) ctx with - | Some [] as r -> r - (* FIXME: Let's ignore the error for now. *) - | _ - -> print_string ("Unification of metavar type failed:\n " - ^ lexp_string (Lexp.clean t) ^ " != " - ^ lexp_string (Lexp.clean (OL.get_type ctx lxp)) - ^ "\n" ^ "for " ^ lexp_string lxp ^ "\n"); - Some [] in + let unif idx s lxp = + let t = match metavar_lookup idx with + | MVal _ -> U.internal_error + "`lexp_whnf` returned an instantiated metavar!!" + | MVar (_, t, _) -> push_susp t s in + let lxp' = try Inverse_subst.apply_inv_subst lxp s with + | Inverse_subst.Not_invertible + -> print_string "Not_invertible:\n "; + lexp_print lxp; + print_string "\nAgainst:\n "; + print_string (subst_string s); + print_string "\n"; + lxp in + metavar_table := associate idx lxp' (!metavar_table); + match unify t (OL.get_type ctx lxp) ctx with + | Some [] as r -> r + (* FIXME: Let's ignore the error for now. *) + | _ + -> print_string ("Unification of metavar type failed:\n " + ^ lexp_string (Lexp.clean t) ^ " != " + ^ lexp_string (Lexp.clean (OL.get_type ctx lxp)) + ^ "\n" ^ "for " ^ lexp_string lxp ^ "\n"); + Some [] in match lxp2 with | Metavar (idx2, s2, _) -> if idx = idx2 then View it on GitLab: https://gitlab.com/monnier/typer/commit/494d60dac1042a643bb6a4d99f3bd7e6469… --- View it on GitLab: https://gitlab.com/monnier/typer/commit/494d60dac1042a643bb6a4d99f3bd7e6469… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][master] Make define-operator's effect "immediately" visible
by Stefan 19 Sep '17

19 Sep '17

Stefan pushed to branch master at Stefan / Typer Commits: 91395fc2 by Stefan Monnier at 2017-09-19T20:07:58Z Make define-operator's effect "immediately" visible * src/debruijn.ml (ectx_get_grammar): New function. * src/elab.ml (sform_immediate, default_ectx.read_file, lexp_expr_str) (lexp_decl_str)): Use it. (lexp_p_decls): Make new scope for body of `let`. * tests/eval_test.ml (define-operator): No need for workaround any more. * src/lexer.ml (unescape.split): Use string_sub. * src/lexp.ml (_lexp_str): Avoid corner case bug. (get_binary_op_name): Catch corner case bug. * src/opslexp.ml (clean_map): Prefer `map` when the `i` is not used. * src/prelexer.ml (prelex_string.getline): Use string_sub. - - - - - 9 changed files: - src/debruijn.ml - src/elab.ml - src/eval.ml - src/inverse_subst.ml - src/lexer.ml - src/lexp.ml - src/opslexp.ml - src/prelexer.ml - tests/eval_test.ml Changes: ===================================== src/debruijn.ml ===================================== --- a/src/debruijn.ml +++ b/src/debruijn.ml @@ -200,6 +200,9 @@ let ectx_new_scope ectx : elab_context = let ectx_get_scope (ectx : elab_context) : (scope_level * lctx_length) = let (_, _, _, sl) = ectx in sl +let ectx_get_grammar (ectx : elab_context) : Grammar.grammar = + let (grm, _, _, _) = ectx in grm + let env_lookup_by_index index (ctx: lexp_context): env_elem = Myers.nth index ctx ===================================== src/elab.ml ===================================== --- a/src/elab.ml +++ b/src/elab.ml @@ -377,7 +377,8 @@ and infer_type pexp ectx var = * could write `(a : TypeLevel) -> a -> a` instead of * `(a : TypeLevel) -> Type_ a -> Type_ a` *) | _ -> - (* FIXME: Here we rule out TypeLevel/TypeOmega. *) + (* FIXME: Here we rule out TypeLevel/TypeOmega. + * Maybe it's actually correct?! *) match Unif.unify (mkSort (lexp_location s, Stype (newMetalevel @@ -724,10 +725,10 @@ and track_fv rctx lctx e = "metavars" else if nc = [] then "a bug" - else let rec tfv i = + else let tfv i = let name = match Myers.nth i rctx with - | (Some n,_) -> n - | _ -> "<anon>" in + | (Some n,_) -> n + | _ -> "<anon>" in match Myers.nth i lctx with | (o, _, LetDef e, _) -> let drop = i + 1 - o in @@ -930,7 +931,7 @@ and lexp_decls_1 and lexp_p_decls (sdecls : sexp list) (ctx : elab_context) : ((vname * lexp * ltype) list list * elab_context) = match sdecls with - | [] -> [], ctx + | [] -> [], ectx_new_scope ctx | _ -> let decls, sdecls, nctx = lexp_decls_1 sdecls ctx ctx SMap.empty [] in let declss, nnctx = lexp_p_decls sdecls nctx in decls :: declss, nnctx @@ -1130,7 +1131,7 @@ let sform_immediate ctx loc sargs ot = | [(Integer _) as se] -> mkImm (se), Inferred DB.type_int | [(Float _) as se] -> mkImm (se), Inferred DB.type_float | [Block (sl, pts, el)] - -> let (grm, _, _, _) = ctx in + -> let grm = ectx_get_grammar ctx in let tokens = lex default_stt pts in let (se, _) = sexp_parse_all grm tokens None in elaborate ctx se ot @@ -1257,7 +1258,7 @@ let rec sform_lambda kind ctx loc sargs ot = match alt with | Inferred lt2' -> Inferred (mkArrow (ak2, ov, lt1, loc, lt2')) | _ -> alt) - + | lt -> let (lt1, lt2) = unify_with_arrow ctx loc lt kind arg olt1 in mklam lt1 (Some lt2)) @@ -1379,7 +1380,8 @@ let default_ectx let read_file file_name elctx = let pres = prelex_file file_name in let sxps = lex default_stt pres in - let nods = sexp_parse_all_to_list default_grammar sxps (Some ";") in + let nods = sexp_parse_all_to_list (ectx_get_grammar elctx) + sxps (Some ";") in let _, lctx = lexp_p_decls nods elctx in lctx in @@ -1432,16 +1434,16 @@ let _lexp_expr_str (str: string) (tenv: token_env) (* specialized version *) -let lexp_expr_str str lctx = - _lexp_expr_str str default_stt default_grammar (Some ";") lctx +let lexp_expr_str str ctx = + _lexp_expr_str str default_stt (ectx_get_grammar ctx) (Some ";") ctx -let _lexp_decl_str (str: string) tenv grm limit ctx = +let _lexp_decl_str (str: string) tenv grm limit (ctx : elab_context) = let sdecls = _sexp_parse_str str tenv grm limit in - lexp_p_decls sdecls ctx + lexp_p_decls sdecls ctx (* specialized version *) -let lexp_decl_str str lctx = - _lexp_decl_str str default_stt default_grammar (Some ";") lctx +let lexp_decl_str str ctx = + _lexp_decl_str str default_stt (ectx_get_grammar ctx) (Some ";") ctx (* Eval String ===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -372,7 +372,8 @@ and eval_case ctx i loc target pat dflt = (* extract constructor name and arguments *) let ctor_name, args = match v with | Vcons((_, cname), args) -> cname, args - | _ -> elexp_fatal loc target "Target is not a Constructor" in + | _ -> value_error loc v ("Target `" ^ elexp_string target + ^ "` is not a Constructor") in (* Get working pattern *) try let (_, pat_args, exp) = SMap.find ctor_name pat in ===================================== src/inverse_subst.ml ===================================== --- a/src/inverse_subst.ml +++ b/src/inverse_subst.ml @@ -34,7 +34,7 @@ this program. If not, see <http://www.gnu.org/licenses/>. *) * * X[σ] = e ==> X[σ][σ⁻¹] = e[σ⁻¹] * - * so if we can find a σ⁻¹ such that σ ∘ σ⁻¹ = Id, e have X = e[σ⁻¹] + * so if we can find a σ⁻¹ such that σ ∘ σ⁻¹ = Id, we have X = e[σ⁻¹] * * So either left or right inverse can be used! *) ===================================== src/lexer.ml ===================================== --- a/src/lexer.ml +++ b/src/lexer.ml @@ -38,7 +38,7 @@ let unescape str = if b >= String.length str then [] else let e = try String.index_from str b '\\' with Not_found -> String.length str in - String.sub str b (e - b) :: split (e + 1) + string_sub str b e :: split (e + 1) in String.concat "" (split 0) let nexttoken (stt : token_env) (pts : pretoken list) bpos cpos ===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -607,6 +607,7 @@ let is_binary_op str = if (c1 = '_') && (cn = '_') then true else false let get_binary_op_name name = + assert (((String.length name) - 2) >= 1); String.sub name 1 ((String.length name) - 2) let rec get_precedence expr ctx = @@ -718,9 +719,11 @@ and _lexp_str ctx (exp : lexp) : string = let decls = List.fold_left (fun str elem -> str ^ nl ^ (make_indent 1) ^ elem ^ " ") h1 decls in - let n = String.length decls - 2 in + let n = String.length decls in (* remove last newline *) - let decls = (String.sub decls 0 n) in + let decls = if (n > 0) then + String.sub decls 0 (n - 2) + else decls in (keyword "let ") ^ decls ^ (keyword " in ") ^ newline ^ (make_indent idt_lvl) ^ (lexp_stri idt_lvl body) ===================================== src/opslexp.ml ===================================== --- a/src/opslexp.ml +++ b/src/opslexp.ml @@ -108,7 +108,7 @@ let lexp_close lctx e = * (of O(N) access time) * Oh well! *) L.clean (mkSusp e (lctx_to_subst lctx)) - + (** Reduce to weak head normal form. * WHNF implies: @@ -890,5 +890,6 @@ and clean_map cases = | [] -> List.rev acc in clean_arg_list lst [] in - SMap.mapi (fun key (l, args, expr) -> - (l, (clean_arg_list args), (erase_type expr))) cases + SMap.map (fun (l, args, expr) + -> (l, (clean_arg_list args), (erase_type expr))) + cases ===================================== src/prelexer.ml ===================================== --- a/src/prelexer.ml +++ b/src/prelexer.ml @@ -1,6 +1,6 @@ (* prelexer.ml --- First half of lexical analysis of Typer. -Copyright (C) 2011-2012, 2016 Free Software Foundation, Inc. +Copyright (C) 2011-2017 Free Software Foundation, Inc. Author: Stefan Monnier <monnier(a)iro.umontreal.ca> Keywords: languages, lisp, dependent types. @@ -152,7 +152,7 @@ let prelex_string str = with Not_found -> String.length str - 1 in let npos = i + 1 in pos := npos; - let line = String.sub str start (npos - start) in + let line = string_sub str start npos in (* print_string ("Read line: " ^ line); *) line in prelex "<string>" getline 1 [] [] ===================================== tests/eval_test.ml ===================================== --- a/tests/eval_test.ml +++ b/tests/eval_test.ml @@ -389,6 +389,7 @@ let _ = test_eval_eqv_named "Y" "length_y = lambda t ≡> + %% FIXME: The `a` argument should be inferred! Y (a := List t) (witness := (lambda l -> 0)) (lambda length l -> case l @@ -415,10 +416,8 @@ let _ = test_eval_eqv_named define-operator \"ELSE\" 1 66; IF_THEN_ELSE_ = if_then_else_;" - "{IF true THEN 2 ELSE 3};" - (* FIXME: the new grammar is not used at top-level yet! *) - (* "if true then 2 else 3;" *) - "{if true then 2 else 3};" + "IF true THEN 2 ELSE 3;" + "if true then 2 else 3;" let _ = test_eval_eqv_named "Type Alias" "ListInt = List Int;" "" (* == *) "" View it on GitLab: https://gitlab.com/monnier/typer/commit/91395fc27ad104a1ed95b64a1ec0c32998e… --- View it on GitLab: https://gitlab.com/monnier/typer/commit/91395fc27ad104a1ed95b64a1ec0c32998e… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][master] * emacs/typer-mode.el: Render comments as markdown
by Stefan 19 Sep '17

19 Sep '17

Stefan pushed to branch master at Stefan / Typer Commits: 756bdbdf by Stefan Monnier at 2017-09-19T17:26:13Z * emacs/typer-mode.el: Render comments as markdown (typer--markdown-verbatim-block-re, typer--markdown-verbatim-face): New consts. (typer--markdown-p): New function. (typer-markdown-blockquote): New face. (typer-markdown-keywords): New var. (typer-font-lock-keywords): Use it. (typer-mode): Setup use of `invisible' property. * btl/pervasive.typer: Make use of new comment style. * src/subst.ml: Rework top-level comment. - - - - - 5 changed files: - btl/pervasive.typer - doc/manual.texi - emacs/typer-mode.el - src/subst.ml - tests/elab_test.ml Changes: ===================================== btl/pervasive.typer ===================================== --- a/btl/pervasive.typer +++ b/btl/pervasive.typer @@ -1,4 +1,4 @@ -%%% pervasive.typer --- Always available definitions +%%% pervasive --- Always available definitions %% Copyright (C) 2011-2017 Free Software Foundation, Inc. %% @@ -23,10 +23,10 @@ %%% Commentary: %% This file includes all kinds of predefined types and functions that are -%% generally useful. It plays a similar role to builtins.typer and is read -%% right after that one. The main reason for the separation into +%% generally useful. It plays a similar role to `builtins.typer` and is +%% read right after that one. The main reason for the separation into %% 2 different files, is that for technical reasons, one cannot use macros -%% in builtins.typer. +%% in `builtins.typer`. %%% Code: @@ -46,9 +46,9 @@ List_length xs = case xs %% ML's typical `head` function is not total, so can't be defined %% as-is in Typer. There are several workarounds: -%% - Provide a default value : (a : Type) ≡> a -> List a -> a; -%% - Disallow problem case : (a : Type) ≡> (l : List a) -> (l != nil) -> a; -%% - Return an Option/Error. +%% - Provide a default value : `a -> List a -> a`; +%% - Disallow problem case : `(l : List a) -> (l != nil) -> a`; +%% - Return an Option/Error List_head1 : (a : Type) ≡> List a -> Option a; List_head1 xs = case xs | nil => none @@ -89,7 +89,7 @@ List_nth = lambda n -> lambda xs -> lambda d -> case xs %%%% A more flexible `lambda` -%% An Sexp which we use to represents an error. +%% An `Sexp` which we use to represents an *error*. Sexp_error = Sexp_symbol "<error>"; Sexp_to_list : Sexp -> List Sexp -> List Sexp; @@ -108,10 +108,12 @@ Sexp_to_list s = lambda exceptions -> singleton singleton singleton singleton; multiarg_lambda = - %% This macro lets `lambda_->_` (and siblings) accept multiplke arguments. + %% This macro lets `lambda_->_` (and siblings) accept multiple arguments. %% TODO: We could additionally turn - %% `lambda (x :: t) y -> e` into `lambda (x : t) => lambda y -> e` - %% thus providing an alternate syntax for lambdas which doesn't use + %% lambda (x :: t) y -> e + %% into + %% lambda (x : t) => lambda y -> e` + %% thus providing an alternate syntax for lambdas which don't use %% => and ≡>. let exceptions = List_map Sexp_symbol (cons "_:_" (cons "_::_" (cons "_:::_" nil))) in @@ -168,7 +170,7 @@ K x y = x; %% Takes an Sexp `x` as argument and return an Sexp which represents code %% which will construct an Sexp equivalent to `x` at run-time. -%% This is basically "cross stage persistence" for Sexp. +%% This is basically *cross stage persistence* for Sexp. quote1 : Sexp -> Sexp; quote1 x = let k = K x; qlist : List Sexp -> Sexp; @@ -191,8 +193,8 @@ quote = macro (lambda x -> quote1 (List_head Sexp_error x)); %%%% The `type` declaration macro -%% build a declaration -%% var-name = value-expr; +%% Build a declaration: +%% var-name = value-expr; make-decl : Sexp -> Sexp -> Sexp; make-decl var-name value-expr = Sexp_node (Sexp_symbol "_=_") @@ -203,8 +205,8 @@ chain-decl : Sexp -> Sexp -> Sexp; chain-decl a b = Sexp_node (Sexp_symbol "_;_") (cons a (cons b nil)); -%% build datacons -%% ctor-name = datacons type-name ctor-name; +%% Build datacons: +%% ctor-name = datacons type-name ctor-name; make-cons : Sexp -> Sexp -> Sexp; make-cons ctor-name type-name = make-decl ctor-name @@ -212,8 +214,8 @@ make-cons ctor-name type-name = (cons type-name (cons ctor-name nil))); -%% buil type annotation -%% var-name : type-expr; +%% Build type annotation: +%% var-name : type-expr; make-ann : Sexp -> Sexp -> Sexp; make-ann var-name type-expr = Sexp_node (Sexp_symbol "_:_") @@ -221,10 +223,11 @@ make-ann var-name type-expr = (cons type-expr nil)); type-impl = lambda (x : List Sexp) -> - %% x follow the mask -> (_|_ Nat zero (succ Nat)) - %% Type name --^ ^------^ constructors + %% `x` follow the mask -> + %% (_|_ Nat zero (succ Nat)) + %% Type name --^ ^------^ constructors - %% Return a list contained inside a node sexp + %% Return a list contained inside a node sexp. let knil = K nil; kerr = K Sexp_error; @@ -252,7 +255,7 @@ type-impl = lambda (x : List Sexp) -> get-head = List_head Sexp_error; - %% Get expression + %% Get expression. expr = get-head x; %% Expression is Sexp_node (Sexp_symbol "|") (list) @@ -265,13 +268,13 @@ type-impl = lambda (x : List Sexp) -> type-name = get-name name; - %% Create the inductive type definition + %% Create the inductive type definition. inductive = Sexp_node (Sexp_symbol "typecons") (cons name ctor); decl = make-decl type-name inductive; - %% Add constructors + %% Add constructors. ctors = let for-each : List Sexp -> Sexp -> Sexp; for-each ctr acc = case ctr | cons hd tl => @@ -331,8 +334,8 @@ __\.__ = %%%% Logic -%% False should be one of the many empty types. -%% Other common choices are False = ∀a.a and True = ∃a.a. +%% `False` should be one of the many empty types. +%% Other popular choices are False = ∀a.a and True = ∃a.a. False = Void; True = Unit; @@ -360,15 +363,18 @@ if_then_else_ | false => uquote e3)); %%%% Test -test1 : Option Int; +test1 : ?; test2 : Option Int; test3 : Option Int; test1 = test2; -test4 : Option ?; +%% In earlier versions of Typer, we could use `?` in declarations +%% to mean "fill this for me by unifying with later type information", +%% but this is incompatible with the use of generalization to introduce +%% implicit arguments. +%% test4 : Option ?; test2 = none; test4 : Option Int; -test4 = test1; +test4 = test1 : Option ?; test3 = test4; - %%% pervasive.typer ends here. ===================================== doc/manual.texi ===================================== --- a/doc/manual.texi +++ b/doc/manual.texi @@ -206,7 +206,7 @@ A = { TypeLevel : SortL, TypeLevel.z : TypeLevel TypeLevel.s : TypeLevel → TypeLevel, TypeLevel.∪ : TypeLevel → TypeLevel → TypeLevel. - Type l : Type (TypeLevel.s l), ∀ l : TypeLevel + Type : (l : TypeLevel) → Type (TypeLevel.s l) } R = { (SortL, Type l, Sortω), ∀ l : TypeLevel (SortL, Sortω, Sortω), ===================================== emacs/typer-mode.el ===================================== --- a/emacs/typer-mode.el +++ b/emacs/typer-mode.el @@ -55,15 +55,82 @@ st) "Syntax table for `typer-mode'.") +;;;; Support for markdown-style rendering in comments + +(defconst typer--markdown-verbatim-block-re "^[ \t]*%+\$?: *\t\\| \$") + +(defconst typer--markdown-verbatim-face + (if (facep 'fixed-pitch-serif) 'fixed-pitch-serif 'fixed-pitch)) + +(defun typer--markdown-p () + (and (save-excursion (nth 4 (syntax-ppss))) + (let ((prop (get-text-property (1- (point)) 'face))) + (not (and (consp prop) + (memq typer--markdown-verbatim-face prop)))))) + +(defface typer-markdown-blockquote + '((t :background "grey95")) + "Face used for blocks quoted with `>' in comments.") + +(defvar typer-markdown-keywords + `((,(concat "\$?:\\`%%\\(%+\$[ \t]+\$.*?\$[ \t]+---" ;First line + "\\|^%%\$?1:%+\$" ;Other header lines + "\\)[ \t]+\$.*\$") + (2 typer--markdown-verbatim-face prepend t) + (3 (typer--section-face (- (match-end 1) (match-beginning 1))) prepend)) + (,(concat typer--markdown-verbatim-block-re "[ \t]*\$.*\$") + (1 (when (save-excursion + (forward-line -1) + (looking-at (concat typer--markdown-verbatim-block-re + "[ \t]*\$.*\$" + "\\|[ \t]*%+\$?:[ \t]*$\\| ?[^ \t]\$"))) + typer--markdown-verbatim-face) + append)) + ("^[ \t]*%+[ \t]+>\$[ \t]+.*\$" + (1 'typer-markdown-blockquote append)) + (,(concat typer--markdown-verbatim-block-re "[ \t]*\$.*\$") + (1 (when (save-excursion + (forward-line -1) + (looking-at (concat typer--markdown-verbatim-block-re + "[ \t]*\$.*\$" + "\\|[ \t]*%+[ \t]*$"))) + typer--markdown-verbatim-face) + append)) + ("`\$[^`\n]+\$`" + (1 (if (typer--markdown-p) typer--markdown-verbatim-face) + prepend)) + ("\\*\\*\$.+?\$\\*\\*" + (1 (let ((p0 (match-beginning 0)) + (p1 (match-beginning 1)) + (p2 (match-end 1)) + (p3 (match-end 0))) + (when (typer--markdown-p) + ;; FIXME: Completely hiding the ** is evil! + (put-text-property p0 p1 'invisible 'typer-markdown) + (put-text-property p2 p3 'invisible 'typer-markdown) + 'bold)) + prepend)) + ("\\*\$[^*\n]+\$\\*" + (1 (unless (or (eq ?* (char-before (match-beginning 0))) + (eq ?* (char-after (match-end 0)))) + (let ((p0 (match-beginning 0)) + (p1 (match-beginning 1)) + (p2 (match-end 1)) + (p3 (match-end 0))) + (when (typer--markdown-p) + ;; FIXME: Completely hiding the ** is evil! + (put-text-property p0 p1 'invisible 'typer-markdown) + (put-text-property p2 p3 'invisible 'typer-markdown) + 'italic))) + prepend)))) + (defvar typer-font-lock-keywords `(("deftoken[ \t]+\$[^ \t\n]+\$" (1 font-lock-function-name-face)) (,(concat "\\_<" (regexp-opt '("type" "case" "lambda" "let" "in")) "\\_>") (0 font-lock-keyword-face)) ("\\_<type[ \t]+\$[^ \t\n]+\$" (1 font-lock-function-name-face)) ("^\$[^() \t]+\$[ \t]" (1 font-lock-function-name-face)) - ("^%%\$%+\$\$?:.* ---\$?\$.*\$" - (2 (typer--section-face (- (match-end 1) (match-beginning 1))) prepend)) - ) + ,@typer-markdown-keywords) "Keyword highlighting specification for `typer-mode'.") (defun typer--section-face (length) @@ -202,6 +269,8 @@ (concat "./typer " (shell-quote-argument (file-relative-name buffer-file-name))))) (smie-setup typer-smie-grammar #'typer-smie-rules) + (add-to-invisibility-spec '(typer-markdown . nil)) + (push 'invisible font-lock-extra-managed-props) ;; (set (make-local-variable 'compilation-first-column) 0) (set (make-local-variable 'compilation-error-screen-columns) nil) (set (make-local-variable 'imenu-generic-expression) ===================================== src/subst.ml ===================================== --- a/src/subst.ml +++ b/src/subst.ml @@ -1,6 +1,6 @@ (* subst.ml --- Substitutions for Lexp -Copyright (C) 2016 Free Software Foundation, Inc. +Copyright (C) 2016-2017 Free Software Foundation, Inc. Author: Stefan Monnier <monnier(a)iro.umontreal.ca> @@ -37,174 +37,70 @@ module U = Util * - S.identity_p * - S.lookup * - * This implementation is generic (i.e. can be with various datatypes + * This implementation is generic (i.e. can be used 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. +(* There are many different ways to do an explicit substitution system. + * See for example: + * Implementation of Explicit Substitutions: + * from λσ to the Suspension Calculus. + * Vincent Archambault-Bouffard and Stefan Monnier. HOR'2016. + * http://www.iro.umontreal.ca/~monnier/HOR-2016.pdf * - * ol: old embedding level ('associate' level, length with environement) - * nl: new .... + * We mostly follow the above article, which we summarize here. + * We start from Abadi's calculs which looks like: * - * n: A Natural Number - * i: A positive integer + * e ::= #0 % Reference to dbi_index 0 + * e₁ e₂ + * (λ e) + * e[s] % Application of a substitution * - * t ::= c : - * #i : Debruijn Index variable bound by the ith abstraction - * (t, t) : Applications - * (λ t) : Abstractions - * [t, n, n, e] : Suspensions + * s ::= id % identity substitution + * e . s % replace #0 with `e` and use `s` for the rest + * s₁ ∘ s₂ % Composition (apply s₁ *first* and then s₂!). + * ↑ % dbi_index = dbi_index + 1 * - * length level - * e ::= nil : 0 : 0 - * (t, n)::e : n + len(e) : n - * {e1, nl, ol, e2} : len(e1) + len(e2) - nl : lev(e1) + nl - ol + * But we make it more practical by using instead: * - * level is the dbi index ? + * e ::= #i % Reference to dbi_index `i` + * e₁ e₂ + * (λ e) + * e[s] % Application of a substitution * - * Substitutions Compositions definitions. + * s ::= id % identity substitution + * e . s % replace #0 by `e` and use `s` for the rest + * s ↑n % like Abadi's "s ∘ (↑ⁿ)" * - * a ::= 1 - * a b - * (λ a) : - * a[s] : + * And the composition ∘ is defined as a function rather than a constructor. * - * s ::= id : identity - * a . s : cons replace dbi_idx = 0 by a use s for the rest - * s o t : Composition - * shift : dbi_index + 1 - *) -(* Substitutions. - * - * There are many different ways to implement a calculus with explicit - * substitutions, with tradeoffs between complexity of implementation, - * performance etc... - * - * The "fine-grained notation" version of the suspension calculus uses - * The following special rules: - * - * (λ [t₁, ol+1, nl+1, @nl::e]) t₂ ==> [t₁, ol+1, nl, (t₂,nl)::e] - * [[t, ol, nl, e], 0, nl', nil] ==> [t, ol, nl+nl', e] - * - * Alternate rules: - * - * [(λ t₁), ol, nl, e]) t₂ ==> [t₁, ol+1, nl, (t₂,nl)::e] - * - * The normal beta rule is: - * - * (λ t₁) t₂ ==> [t₁, 1, 0, (t₂,0) :: nil] - * - * which would be instantiated to - * - * (λ [t₁, ol, nl, e]) t₂ ==> [[t₁, ol, nl, e], 1, 0, (t₂,0) :: nil] - * - * So we could do it as follows: - * - * (λ [t₁ σ₁]) t₂ ==> [t₁ ((1, 0, (t₂::nil)) ∘ σ₁)] - * ((1, 0, (t₂::nil)) ∘ (ol+1, nl+1, e) ==> (ol₁, nl, (t₂,nl)::e) - * - * Rules used in the "no merging" version: - * - * (λ t₁) t₂ ==> [t₁, 1, 0, (t₂,0) :: nil] - * (λ [t₁, ol+1, nl+1, @nl::e]) t₂ ==> [t₁, ol+1, nl, (t₂,nl)::e] - * [t, 0, 0, nil] ==> t - * [#i, ol, nl, e] ==> #(i-ol+nl) if i>ol - * [#i, ol, nl, e] ==> #(nl - j) if e.i = @j' - * [#i, ol, nl, e] ==> [t, 0, nl - j, nil] if e.i = (t,j) - * [λt, ol, nl, e] ==> λ[t, ol+1, nl+1, @nl :: e] - * [[t, ol, nl, e], 0, nl', nil] ==> [t, ol, nl+nl', e] - * - * First simplification: get rid of `ol`! - * - * (λ t₁) t₂ ==> [t₁, 0, (t₂,0)::nil] - * [#i, nl, e] ==> [t, nl - j, nil] if e.i = (t,j) - * [λt, nl, e] ==> λ[t, nl+1, @nl::e] + * And we have the propagation rules: * - * (λ [t₁, nl+1, @nl::e]) t₂ ==> [t₁, nl, (t₂,nl)::e] - * [(λ t₁), nl, e]) t₂ ==> [t₁, nl, (t₂,nl)::e] - * [[t, nl, e], nl', nil] ==> [t, nl+nl', e] + * #i[s] ==> lookup i s + * (e₁ e₂)[s] ==> (e₁[s]) (e₂[s]) + * (λ e)[s] ==> λ(e[#0 · (s ↑1)]) + * e[s₁][s₂] ==> e[s₁ ∘ s₂] * - * [t, 0, nil] ==> t - * [#i, nl, e] ==> #(i-len(e)+nl) if i>len(e) - * [#i, nl, e] ==> #(nl - j) if e.i = @j' + * We also have beta rules: * - * Re-introduce subst-merging. So we currently have two merging rules: + * (λ e₁) e₂ ==> e₁[e₂·id] * - * ((0, (t₂::nil)) ∘ (nl+1, e) ==> (nl, (t₂,nl)::e) if e≠nil - * (nl, e) ∘ (nl', nil) ==> (nl+nl', e) + * To which we can add (as an optimisation to avoid using `compose`): * - * What do these substitutions mean? - * - * (N, nil) == shift N - * (0, e) == replace nearest N vars with values from `e` - * (nl+1, @nl::e) == lift e - * (nl, e) == shift (nl - ol) (ol, e) if ol = lvl(e) - * - * Another way to look at it: - * - * (λ t₁) t₂ ==> [t₁, t₂::nil] - * [λt, σ] ==> λ[t, lift σ] - * - * (λ [t₁, lift σ]) t₂ ==> [t₁, t₂::σ] - * [(λ t₁), σ]) t₂ ==> [t₁, t₂::σ] - * [[t, σ], shift n nil] ==> [t, shift n σ] - * - * [t, id] ==> t - * [#0, t::σ] ==> t - * [#i, t::σ] ==> [#i-1, σ] - * [#0, lift σ] ==> #0 - * [#i, lift σ] ==> [[#i-1, σ], shift 1 nil] - * [#i, shift N σ] ==> [[#i, σ], shift N nil] - * - * I guess I'm leaning towards a kind of λσ, but with - * - * σ = id | σ ↑n | a·σ - * - * where σ ↑n == (σ ∘ ↑n) - * and lift σ == #0·(σ ↑) - * and #n == [#0, ↑n] - * - * (λt₁)t₂ ==> [t₁, t₂·nil] - * [λt, σ] ==> λ[t, lift σ] - * [t, id] ==> t - * [#0, t·σ] ==> t - * [#i+1, t·σ] ==> [#i, σ] (because => [[#i, ↑] t·σ] => [#i, ↑ ∘ t·σ]) - * [#i, σ ↑n] ==> [[#i, σ], ↑n] + * (λ e₁)[s] e₂ ==> e₁[e₂·s] * * Merging rules: * - * (σ ↑n₂) ↑n₁ ==> σ ↑(n₁+n₂) {part of m1} - * σ₁ ∘ id ==> σ₁ {m2} - * σ₁ ∘ σ₂ ↑n ==> (σ₁ ∘ σ₂) ↑n {part of m1} - * id ∘ σ ==> σ {m3} - * σ₁ ↑n ∘ a·σ₂ ==> σ₁ ↑(n-1) ∘ σ₂ {m4 & m5} - * a·σ₁ ∘ σ₂ ==> [a, σ₂]·(σ₁ ∘ σ₂) {m6} - * - * The optimisations used in FLINT would translate to: - * - * [λt₁, σ] t₂ ==> (λ[t₁, lift σ]) t₂ - * ==> [t₁, (lift σ) ∘ t₂·nil] - * ==> [t₁, #0·(σ ↑) ∘ t₂·nil] - * ==> [t₁, [#0, t₂·nil]·(σ ↑ ∘ t₂·nil)] - * ==> [t₁, t₂·σ] - * [[t, σ], id ↑n] ==> [t, σ ∘ id ↑n] - * ==> [t, σ ↑n] - * - * Confluence: - * - * a·σ₁ ∘ σ₂ ↑n ==> (a·σ₁ ∘ σ₂) ↑n - * a·σ₁ ∘ σ₂ ↑n ==> [a, σ₂ ↑n]·(σ₁ ∘ σ₂ ↑n) - * - * so we might also need to make sure that - * - * (a·σ₁ ∘ σ₂) ↑n <==> [a, σ₂ ↑n]·(σ₁ ∘ σ₂ ↑n) - * - * for confluence. Which might boild down to adding a rule like + * (s ↑n₂) ↑n₁ ==> s ↑(n₁+n₂) {part of m1} + * s₁ ∘ id ==> s₁ {m2} + * s₁ ∘ s₂ ↑n ==> (s₁ ∘ s₂) ↑n {part of m1} + * id ∘ s ==> s {m3} + * s₁ ↑n ∘ e·s₂ ==> s₁ ↑(n-1) ∘ s₂ {m4 & m5} + * e·s₁ ∘ s₂ ==> (e[s₂])·(s₁ ∘ s₂) {m6} * - * (a·σ₁) ↑n <==> [a, id ↑n]·(σ₁ ↑n) *) (* We define here substitutions which take a variable within a source context @@ -219,7 +115,7 @@ type db_index = int (* DeBruijn index. *) type db_offset = int (* DeBruijn index offset. *) (* Substitution, i.e. a mapping from db_index to 'a - * In practice, 'a is always lexp, but we keep it as a paramter: + * In practice, 'a is always lexp, but we keep it as a parameter: * - for better modularity of the code. * - to break a mutual dependency between the Lexp and the Subst modules. *) type 'a subst = (* lexp subst *) ===================================== tests/elab_test.ml ===================================== --- a/tests/elab_test.ml +++ b/tests/elab_test.ml @@ -1,4 +1,4 @@ -(* lparse_test.ml --- +(* elab_test.ml --- * * Copyright (C) 2016-2017 Free Software Foundation, Inc. * View it on GitLab: https://gitlab.com/monnier/typer/commit/756bdbdfa94cf2d683e2e9b67a73661dece… --- View it on GitLab: https://gitlab.com/monnier/typer/commit/756bdbdfa94cf2d683e2e9b67a73661dece… You're receiving this email because of your account on gitlab.com.

1 0

2024

2023

2022

2021

2020

2019

2018

2017

2016

Typer Septembre 2017