Typer Avril 2020

typer@iro.umontreal.ca

2 participants
9 discussions

[Git][monnier/typer][ja-barszcz] [WIP] proof of Decidable (a < b)
by Jean-Alexandre Barszcz 14 Avr '20

14 Avr '20

Jean-Alexandre Barszcz pushed to branch ja-barszcz at Stefan / Typer Commits: b5f593a8 by Jean-Alexandre Barszcz at 2020-04-14T18:47:30-04:00 [WIP] proof of Decidable (a < b) - - - - - 1 changed file: - samples/decidable.typer Changes: ===================================== samples/decidable.typer ===================================== @@ -113,4 +113,25 @@ decideEven = type _<_ (a : Nat) (b : Nat) | ltZ (pa ::: Eq a zero) (pb ::: Eq b (succ ?b)) - | ltS (p : (?a < ?b)) (pa ::: Eq a (succ ?a)) (pb ::: Eq b (succ ?b)); + | ltS (p :: (?a < ?b)) (pa ::: Eq a (succ ?a)) (pb ::: Eq b (succ ?b)); + +decideLT : (a : Nat) => (b : Nat) => Decidable (a < b); +decideLT = + lambda a b => + case b + | zero => no (p := + lambda (p : (a < b)) -> + case p + | ltZ => absurd (Eq_trans b) (discriminate_nocheck zero (succ ?)) + | ltS => absurd (Eq_trans b) (discriminate_nocheck zero (succ ?))) + | succ b' => + case a + | zero => yes (p := ltZ) + | succ a' => + case (decideLT : (Decidable (a' < b'))) + | yes => yes (p := ltS) + | no => no (p := + lambda (p : (a < b)) -> + case p + | ltZ => absurd (Eq_trans a) (discriminate_nocheck zero (succ ?)) + | ltS => absurd (? : (a' < b')) (? : Not (a' < b'))); View it on GitLab: https://gitlab.com/monnier/typer/-/commit/b5f593a8a3cf403ce5e026840e4c54af4… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/b5f593a8a3cf403ce5e026840e4c54af4… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][ja-barszcz] 14 commits: * src/elab.ml (meta_to_var): Fix debruijn error.
by Jean-Alexandre Barszcz 13 Avr '20

13 Avr '20

Jean-Alexandre Barszcz pushed to branch ja-barszcz at Stefan / Typer Commits: f2b81386 by Stefan Monnier at 2020-04-02T19:31:41-04:00 * src/elab.ml (meta_to_var): Fix debruijn error. * btl/pervasive.typer (Decidable): Make it universe-polymorphic. * src/builtin.ml (register_builtin_csts): Fix Type0 typo. - - - - - 85d12bf5 by Stefan Monnier at 2020-04-07T22:21:39-04:00 * src/elab.ml (infer_and_generalize_type): Add more exceptions Don't generalize over the level of the final return type if it doesn't appear elsewhere. * btl/builtins.typer (Eq_cast): Give a name to the proof arg. - - - - - 4993afa5 by Stefan Monnier at 2020-04-07T23:15:21-04:00 * src/lexp.ml (srename): New function * src/unification.ml (unify): * src/opslexp.ml (conv_p'): * src/elab.ml (sform_lambda): Use it. - - - - - 63f7644b by Stefan Monnier at 2020-04-07T23:21:05-04:00 * src/elab.ml (meta_to_var): Rework to be able to infer universe levels (generalize): Adjust for new calling convention of `meta_to_var` and also for the fact that `meta_to_var` now takes care of the S.shift for us. - - - - - 886a3589 by Stefan Monnier at 2020-04-08T18:07:18-04:00 Remove most uses of L.clean * src/elab.ml (elab_check_sort, elab_check_def, infer_type): Skip `L.clean` since `lexp_string` already cleans up on the fly. (track_fv): Skip `L.clean` since `fv` already cleans up on the fly. (lexp_eval): Skip `L.clean` since `fv` and `erase_type` already clean up on the fly. (sform_new_attribute, sform_add_attribute, sform_built_in): Explicitly call `clean` now that `lexp_close` doesn't do it any more. * src/eval.ml (from_lctx): Skip `L.clean` since `fv` and `erase_type` already clean up on the fly. * src/lexp.ml (print_context_value): Remove `Expr` constructor. (pretty_ppctx): Remove unused `parent` and now unused `metavar`. (smap_lexp, pp_parent, pp_meta, set_parent, set_parent): Remove functions.. (lexp_str): Don't call `set_parent` any more. Rewrite metavar case to use `metavar_lookup` rather than `clean`. * src/opslexp.ml (lexp_close): Don't call `clean` any more. (conv_p', mkSLlub): Skip `L.clean` since `level_canon` already cleans up on the fly. (check''.assert_type): Skip `L.clean` since `lexp_string` already cleans up on the fly. (erase_type): Clean up metavars on the fly. * src/unification.ml (unify_metavar): Skip `L.clean` since `lexp_string` already cleans up on the fly. - - - - - bf3c818e by Jean-Alexandre Barszcz at 2020-04-12T02:05:40-04:00 Add a nix shell * shell.nix : When using nixpkgs/nixos, run `nix-shell` to get a shell with Typer's dependencies available. - - - - - c39ff3d5 by Jean-Alexandre Barszcz at 2020-04-12T02:05:40-04:00 Improve the implementation of Sexp.dispatch * src/elab.ml (sexp_dispatch) : Sexp.dispatch assumed that its arguments were closures. Instead, we use eval_call and also accept constructors, builtins, etc. - - - - - 7b623a26 by Jean-Alexandre Barszcz at 2020-04-12T02:05:40-04:00 Add the inductive type `Sexp_wrapper` to match on sexps * btl/pervasive.typer : Add the inductive type `Sexp_wrapper` to wrap the Sexp values in typer code, and the function `Sexp_wrap` to do the wrapping. This makes possible the use of pattern matching to destructure Sexps instead of the more verbose calls to `Sexp_dispatch`. - - - - - 8419c419 by Jean-Alexandre Barszcz at 2020-04-12T02:05:40-04:00 Fix lexp_whnf when the case scrutinee is a call * src/opslexp.ml (lexp_whnf) : Make sure that we take the WHNF of the function when the scrutinee of a case expression is a call, before checking that the function is a constructor. Otherwise, expressions like `case (let ... in (constructor ...))` fail to reduce, for example. - - - - - cc20d841 by Jean-Alexandre Barszcz at 2020-04-12T02:05:40-04:00 Fix some lexp constructor calls where hash-consing has been forgotten - - - - - 742049a9 by Jean-Alexandre Barszcz at 2020-04-12T02:05:40-04:00 [WIP] Make unification symmetric - - - - - 7bc1f309 by Jean-Alexandre Barszcz at 2020-04-12T02:05:40-04:00 [WIP] Handle variables earlier during unification - - - - - ef1aeb13 by Jean-Alexandre Barszcz at 2020-04-13T21:48:54-04:00 [WIP] experiments with Decidable and proofs - - - - - 3b72b8d2 by Jean-Alexandre Barszcz at 2020-04-13T21:48:54-04:00 [WIP] unify instead of conv_p in sform_lambda - - - - - 11 changed files: - btl/builtins.typer - btl/pervasive.typer - + samples/decidable.typer - + shell.nix - src/builtin.ml - src/elab.ml - src/eval.ml - src/inverse_subst.ml - src/lexp.ml - src/opslexp.ml - src/unification.ml Changes: ===================================== btl/builtins.typer ===================================== @@ -31,6 +31,9 @@ %%%% Base Types used in builtin functions +%% Box : Type_ ?ℓ₁ -> Type_ ?ℓ₂; +%% Box = lambda (ℓ₃ : TypeLevel) ≡> typecons (Box (t : Type_ ℓ₃)) (box t); + %% TypeLevel_succ = Built-in "TypeLevel.succ" : TypeLevel -> TypeLevel; %% TypeLevel_⊔ = Built-in "TypeLevel.⊔" : TypeLevel -> TypeLevel -> TypeLevel; @@ -48,7 +51,7 @@ Eq_refl : ((x : ?t) ≡> Eq x x); % FIXME: `Eq ?x ?x` causes an error! Eq_refl = Built-in "Eq.refl"; Eq_cast : (x : ?) ≡> (y : ?) - ≡> Eq x y + ≡> (p : Eq x y) ≡> (f : ? -> ?) ≡> f x -> f y; %% FIXME: I'd like to just say: ===================================== btl/pervasive.typer ===================================== @@ -358,6 +358,18 @@ type-impl = lambda (x : List Sexp) -> type_ = macro type-impl; +%%%% An inductive type to wrap Sexp + +type Sexp_wrapper + | node Sexp (List Sexp) + | symbol String + | string String + | integer Integer + | float Float + | block Sexp; + +Sexp_wrap s = Sexp_dispatch s node symbol string integer float block; + %%%% Tuples %% Sample tuple: a module holding Bool and its constructors. @@ -446,7 +458,8 @@ Not prop = prop -> False; %% We don't use the `type` macro here because it would make these `true` %% and `false` constructors override `Bool`'s, and we currently don't %% want that. -Decidable = typecons (Decidable (prop : Type)) +%% FIXME generalize typecons formal arguments +Decidable = typecons (Decidable (ℓ ::: TypeLevel) (prop : Type_ ℓ)) (true (p ::: prop)) (false (p ::: Not prop)); %% Testing generalization in inductive type constructors. ===================================== samples/decidable.typer ===================================== @@ -0,0 +1,116 @@ +False = Void; +True = Unit; + +% FIXME improved "case" fails with no branches +exfalso : False -> ?a; +exfalso f = ##case_ f; + +%type Decidable (prop : Type) +% | yes (p ::: prop) +% | no (p ::: Not prop); +yes = datacons Decidable true; +no = datacons Decidable false; + +Eq_trans : + (x : ?t) => (y : ?t) => (a : ?t) -> + (ax : Eq a x) => (ay : Eq a y) => Eq x y; +Eq_trans a = + lambda (ax : Eq a x) (ay : Eq a y) => + Eq_cast (f := lambda ax -> Eq ax y) ay; + +Eq_cong : % not sure about levels here + (t : (Type_ ?ℓ)) ≡> (r : (Type_ ?ℓ)) ≡> + (x : t) ≡> (y : t) ≡> (p : (Eq x y)) ≡> + (f : (t -> r)) -> (Eq (f x) (f y)); +Eq_cong f = + Eq_cast (p := p) (f := lambda xy -> Eq (f x) (f xy)) Eq_refl; + +discriminate_nocheck = + macro (lambda args -> + case args + | cons x (cons y nil) => + do { + sd <- gensym (); + sp <- gensym (); + IO_return + (quote ((lambda (uquote sp) -> + (Eq_cast (p := (uquote sp)) + (f := (lambda (uquote sd) -> + (case uquote sd + | (uquote x) => True + | _ => False))) + ())) : Not (Eq (uquote x) (uquote y)))) + } + | _ => IO_return Sexp_error); + +discriminate = + macro (lambda args -> + case args + | cons x (cons y nil) => + (case (Sexp_wrap x, Sexp_wrap y) + | (symbol sx, symbol sy) => % FIXME get the constructor even when its a call + do { + env <- Elab_getenv (); + if (and (Elab_isconstructor sx env) + (and (Elab_isconstructor sy env) + (not (Sexp_eq x y)))) + then + Macro_expand discriminate_nocheck args + else (IO_return Sexp_error) + } + | _ => IO_return Sexp_error) + | _ => IO_return Sexp_error); + +test : (Not (Eq true false)); +test = discriminate true false; + +absurd = + lambda (p : ?prop) -> + lambda (contra : (Not ?prop)) -> + contra p; + +% We can't (usefully) have a `Decidable Bool` because it's +% impossible to have a `Not Bool`. Instead, we can decide boolean +% equality: + +decideBoolEq : (a : Bool) => (b : Bool) => Decidable (Eq a b); +decideBoolEq = + lambda (a : Bool) (b : Bool) => + case (a, b) + | (false, false) => yes (p := Eq_trans false) + | (false, true) => no (p := lambda (p : Eq a b) -> + absurd (Eq_trans (ax := Eq_trans a) b) (discriminate false true)) + | (true, false) => no (p := lambda (p : Eq a b) -> + absurd (Eq_trans (ax := Eq_trans a) b) (discriminate true false)) + | (true, true) => yes (p := Eq_trans true); + +type Nat + | zero + | succ Nat; + +type even (a : Nat) + | eZ (p ::: Eq a zero) + | eSS (p :: even ?a) (pss ::: Eq a (succ (succ ?a))); + +decideEven : (a : Nat) => Decidable (even a); +decideEven = + lambda (a : Nat) => + case a + | zero => yes (p := eZ) + | succ zero => no (p := + lambda (p : even a) -> + case p + | eZ => absurd (Eq_trans a) (discriminate_nocheck zero (succ zero)) + | eSS => absurd (Eq_trans a) (discriminate_nocheck (succ (succ ?)) (succ zero))) + | succ (succ a') => + case (decideEven : Decidable (even a')) + | yes => yes (p := eSS) + | no => no (p := + lambda (p : even a) -> + case p + | eZ => absurd (Eq_trans a) (discriminate_nocheck zero (succ (succ ?))) + | eSS => absurd (? : even a') (? : Not (even a'))); + +type _<_ (a : Nat) (b : Nat) + | ltZ (pa ::: Eq a zero) (pb ::: Eq b (succ ?b)) + | ltS (p : (?a < ?b)) (pa ::: Eq a (succ ?a)) (pb ::: Eq b (succ ?b)); ===================================== shell.nix ===================================== @@ -0,0 +1,10 @@ +{ pkgs ? import <nixpkgs> {} }: +pkgs.mkShell { + name = "typer"; + buildInputs = + with pkgs.ocamlPackages; [ + pkgs.gnumake ocaml ocamlbuild findlib utop # tooling + zarith # ocaml libraries + merlin # for emacs + ]; +} ===================================== src/builtin.ml ===================================== @@ -155,7 +155,7 @@ let register_builtin_csts () = add_builtin_cst "TypeLevel" DB.type_level; add_builtin_cst "TypeLevel_z" DB.level0; add_builtin_cst "Type" DB.type0; - add_builtin_cst "Type0" DB.type1; + add_builtin_cst "Type0" DB.type0; add_builtin_cst "Type1" DB.type1; add_builtin_cst "Int" DB.type_int; add_builtin_cst "Integer" DB.type_integer; ===================================== src/elab.ml ===================================== @@ -128,8 +128,7 @@ let elab_check_sort (ctx : elab_context) lsort var ltp = "Exception during whnf of sort:"; raise e) with | Sort (_, _) -> () (* All clear! *) - | _ -> let lexp_string e = lexp_string (L.clean e) in - let typestr = lexp_string ltp ^ " : " ^ lexp_string lsort in + | _ -> let typestr = lexp_string ltp ^ " : " ^ lexp_string lsort in match var with | (l, None) -> lexp_error l ltp ("`" ^ typestr ^ "` is not a proper type") @@ -159,7 +158,6 @@ let elab_check_def (ctx : elab_context) var lxp ltype = let lctx = ectx_to_lctx ctx in let loc = lexp_location lxp in - let lexp_string e = lexp_string (L.clean e) in let ltype' = try OL.check lctx lxp with e -> match e with | Log.Stop_Compilation _ -> raise e @@ -311,39 +309,142 @@ let elab_varref ctx (loc, name) "` was not declared" ^ relateds); sform_dummy_ret ctx loc) -(* Turn metavar into plain vars after generalization. *) -let rec meta_to_var ids o (e : lexp) = - let rec loop e = match e with +(* Turn metavar into plain vars after generalization. + * ids: an IMap that maps metavars to their position as argument + * (first arg gets position 0). *) +let rec meta_to_var ids (e : lexp) = + + let count = IMap.cardinal ids in + + (* Yuck! Yuck! Yuck! + * This is very messy. What we need to do starts as follows: + * We have a `Γ ⊢ e : τ` and this `e` contains some metavars `m₁…mₙ : τ₁…τₙ` + * that we want to change into formal arguments, i.e. we want to turn `e` + * into something like + * + * Γ ⊢ λ x₁…xₙ ≡> e[x₁…xₙ/m₁…mₙ] : τ₁…τₙ ≡> τ + * + * The above substitution is not the usual capture-avoiding substitution + * since it replaces metavars with vars rather than vars with terms. + * It's more like *instanciation* of those metavars. + * And indeed, ideally it should be a simple matter of instanciating + * those metavars with temrs that are variable references. + * + * An important aspect here is that the rest of `e` also needs to be + * changed because it will now live in a new context: + * + * Γ,x₁:τ₁,…,xₙ:τₙ ⊢ e[x₁…xₙ/m₁…mₙ] : τ + * + * So we need to adjust all the variable references in `e` to account for + * that, which we normally do with a simple `S.shift n`. + * + * The first problem comes here: `S.shift n` takes a term from + * `Γ` to `Γ,x₁:τ₁,…,xₙ:τₙ`, making sure it still references the same + * bindings as before, i.e. it makes sure the result *cannot* refer to + * any `x₁…xₙ`! + * I first thought "it's OK, I'll first do the `S.shift n` and I only + * instanciate the metavars afterwards", but that does not help, + * because every reference to a metavar is properly wrapped in a + * pending application of the relevant substitution, so the `S.shift n` + * still applies to it. + * + * For this reason, we have a `loop` below which does the substitution + * of variable references for the metavars (since just instanciating + * the metavars doesn't work). + * + * The second problem comes with the other metavars in `e`. + * There are 3 kinds of metavars in `e`: + * + * A. Those that we want to replace with variable references. + * B. Those that live in some higher enclosing scope. + * C. The "others". + * + * Presumably, we have (A) under control. + * For (B) the situation is easy enough: since they live in a higher + * enlosing scope they can only refer to those variables that exist in + * some prefix of `Γ`, so we just need to apply `S.shift n` to them. + * + * For (C), we'd like those metavars (which originally could refer to + * any var in `Γ`) to now be a able to also refer to any of the + * new vars `x₁…xₙ`. So `S.shift n` is definitely not right for them. + * Instead, I ended up writing `adjust_subst` which hacks up + * the substitution attached to each metavar reference so it can + * now refer to its original context *and* to `x₁…xₙ`. + * + * Arguably, now that we handle (C), we could handle (A) by + * first treating them as (C) and then using instantiation. + * But the code for (A) was already written, and it doesn't seem like + * it would make things any simpler currently. + * + * Note: in the original HM algorithm (and in Twelf), (C) cannot occur + * because every metavariable that's not in (B) is generalized + * (i.e. will be in A). But here we need (C) for cases like: + * + * List : Type ? -> Type ?; + * + * Since the second `?` should not be generalized but should + * be inferred from the definition. I.e. the above should be + * generalized to: + * + * List : (ℓ : TypeLevel) ≡> Type ℓ -> Type ?; + * + * where the remaining `?` will be inferred by unification + * when type-checking the definition of `Box` where ti be unified with `ℓ`, + * the newly introduced variable! + *) + + (* `o` is the binding offset until the root. *) + let rec adjust_subst o s = match s with + | S.Identity n + -> let o' = o - n in + if o' < 0 then + (* This metavar's original context is outside of our scope + * (case (B) above), so don't let it refer to the new vars. *) + S.Identity (n + count) + else + Identity n + | S.Cons (e, s', n) + -> let o' = o - n in + if o' < 0 then + (* This metavar's original context is outside of our scope + * (case (B) above), so don't let it refer to the new vars. *) + S.Cons (e, s', n + count) + else + S.Cons (loop o' e, adjust_subst o' s', n) + + (* `o` is the binding depth at which we are relative to the "root" + * of the expression (i.e. where the new vars will be inserted). *) + and loop o e = match e with | Imm _ -> e | SortLevel SLz -> e - | SortLevel (SLsucc e) -> mkSortLevel (mkSLsucc (loop e)) - | SortLevel (SLlub (e1, e2)) -> mkSortLevel (mkSLlub' (loop e1, loop e2)) - | Sort (l, Stype e) -> mkSort (l, Stype (loop e)) + | SortLevel (SLsucc e) -> mkSortLevel (mkSLsucc (loop o e)) + | SortLevel (SLlub (e1, e2)) -> mkSortLevel (mkSLlub' (loop o e1, loop o e2)) + | Sort (l, Stype e) -> mkSort (l, Stype (loop o e)) | Sort (_, (StypeOmega | StypeLevel)) -> e | Builtin _ -> e - | Var _ -> e - | Susp (e, s) -> loop (push_susp e s) + | Var (n,i) -> if i < o then e else mkVar (n, i + count) + | Susp (e, s) -> loop o (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 ids (len + o) e, - meta_to_var ids (o' + o) t) :: defs)) + (o', (l, loop (len + o) e, + loop (o' + o) t) :: defs)) defs (len, []) in - mkLet (l, ndefs, meta_to_var ids (len + o) e) + mkLet (l, ndefs, loop (len + o) e) | Arrow (ak, v, t1, l, t2) - -> mkArrow (ak, v, loop t1, l, meta_to_var ids (1 + o) t2) + -> mkArrow (ak, v, loop o t1, l, loop (1 + o) t2) | Lambda (ak, v, t, e) - -> mkLambda (ak, v, loop t, meta_to_var ids (1 + o) e) + -> mkLambda (ak, v, loop o t, loop (1 + o) e) | Call (f, args) - -> mkCall (loop f, List.map (fun (ak, e) -> (ak, loop e)) args) + -> mkCall (loop o f, List.map (fun (ak, e) -> (ak, loop o 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 ids (o' + o) t) + (o', (ak, v, loop (o' + o) t) :: args)) args (alen, []) in let ncases @@ -354,28 +455,29 @@ let rec meta_to_var ids o (e : lexp) = = List.fold_right (fun (ak, v, t) (o', fields) -> let o' = o' - 1 in - (o', (ak, v, meta_to_var ids (o' + o) t) + (o', (ak, v, loop (o' + o) t) :: fields)) - fields (flen, []) in + fields (flen + alen, []) in nfields) cases in mkInductive (l, label, nargs, ncases) - | Cons (t, l) -> mkCons (loop t, l) + | Cons (t, l) -> mkCons (loop o t, l) | Case (l, e, t, cases, default) -> let ncases = SMap.map (fun (l, fields, e) - -> (l, fields, meta_to_var ids (o + List.length fields) e)) + -> (l, fields, loop (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)) + mkCase (l, loop o e, loop o t, ncases, + match default with None -> None + | Some (v, e) -> Some (v, loop (1 + o) e)) | Metavar (id, s, name) -> if IMap.mem id ids then - mkVar (name, o + IMap.find id ids) + mkVar (name, o + count - IMap.find id ids) else match metavar_lookup id with - | MVal e -> loop (push_susp e s) - | _ -> e - in loop e + | MVal e -> loop o (push_susp e s) + | _ -> mkMetavar (id, adjust_subst o s, name) + in loop 0 e let move_typelevel_to_front ctx mfvs = (* TypeLevel arguments have to come first, so move them accordingly. *) @@ -418,17 +520,17 @@ let generalize (nctx : elab_context) e = let len = List.length mfvs in let mfvs = move_typelevel_to_front (ectx_to_lctx nctx) mfvs in fun wrap e -> - let rec loop ids n mfvs = match mfvs with - | [] -> assert (n = 0); - let e = mkSusp e (S.shift len) in - meta_to_var ids 0 e + let rec loop ids n mfvs = + assert (n = IMap.cardinal ids); + match mfvs with + | [] -> assert (n = len); + meta_to_var ids 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 mt' = meta_to_var ids 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 + wrap (IMap.mem id nes) vname mt' l e' in + loop (IMap.empty) 0 mfvs let elab_p_id ((l,name) : symbol) : vname = (l, match name with "_" -> None | _ -> Some name) @@ -551,8 +653,7 @@ and infer_type pexp ectx var = s (ectx_to_lctx ectx) with | (_::_) - -> (let lexp_string e = lexp_string (L.clean e) in - let typestr = lexp_string t ^ " : " ^ lexp_string s in + -> (let typestr = lexp_string t ^ " : " ^ lexp_string s in match var with | (l, None) -> lexp_error l t ("`" ^ typestr ^ "` is not a proper type") @@ -938,13 +1039,12 @@ and track_fv rctx lctx e = name ^ " (" ^ track_fv (Myers.nthcdr drop rctx) (Myers.nthcdr drop lctx) - (L.clean e) + e ^ ")" | _ -> name in String.concat " " (List.map tfv nc) and lexp_eval ectx e = - let e = L.clean e in let ee = OL.erase_type e in let rctx = EV.from_ectx ectx in @@ -1034,10 +1134,10 @@ and lexp_check_decls (ectx : elab_context) (* External context. *) and infer_and_generalize_type (ctx : elab_context) se name = let nctx = ectx_new_scope ctx in let t = infer_type se nctx name in - (* FIXME: We should not generalize over metavars which only occur on the rightmost + (* We should not generalize over metavars which only occur on the rightmost * side of arrows in type annotations (aka declarations), since there's no * way for the callee to return something of the proper type if those - * metavar's don't also occur somewhere in the arguments. + * metavars don't also occur somewhere in the arguments. * E.g. for annotations like * * x : ?; @@ -1050,16 +1150,21 @@ and infer_and_generalize_type (ctx : elab_context) se name = * * since there can't be corresponding definitions. So replace the final * return type with some arbitrary closed constant before computing the - * set of free metavars. *) - 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 we can use `x : ?` to declare that - * `x` will be defined later without specifying its type yet. *) - | Metavar _ -> t - | _ -> let g = generalize nctx t in - g (fun _ne name t l e - -> mkArrow (Aerasable, name, t, l, e)) - t + * set of free metavars. + * The same argument holds for other *positive* positions, e.g. + * + * f : (? -> Int) -> Int; + * + * But we don't bother trying to catch all cases currently. + *) + let rec strip_rettype t = match t with + | Arrow (ak, v, t1, l, t2) -> Arrow (ak, v, t1, l, strip_rettype t2) + | Sort _ | Metavar _ -> type0 (* Abritrary closed constant. *) + | _ -> t in + let g = generalize nctx (strip_rettype t) in + g (fun _ne name t l e + -> mkArrow (Aerasable, name, t, l, e)) + t and infer_and_generalize_def (ctx : elab_context) se = let nctx = ectx_new_scope ctx in @@ -1225,7 +1330,7 @@ and sform_new_attribute ctx loc sargs ot = * is False, for example): Should be a type like `AttributeMap t` * instead. *) (mkBuiltin ((loc, "new-attribute"), - OL.lexp_close (ectx_to_lctx ctx) ltp, + L.clean (OL.lexp_close (ectx_to_lctx ctx) ltp), Some AttributeMap.empty), Lazy) | _ -> fatal ~loc "new-attribute expects a single Type argument" @@ -1241,7 +1346,7 @@ and sform_add_attribute ctx loc (sargs : sexp list) ot = | _ -> fatal ~loc "add-attribute expects a table as first argument" in (* FIXME: Type check (attr: type == attr_type) *) - let attr' = OL.lexp_close (ectx_to_lctx ctx) attr in + let attr' = L.clean (OL.lexp_close (ectx_to_lctx ctx) attr) in let table = AttributeMap.add var attr' map in (mkBuiltin ((loc, "add-attribute"), attr_type, Some table), Lazy) @@ -1302,7 +1407,11 @@ let sform_built_in ctx loc sargs ot = | true, [String (_, name)] -> (match ot with | Some ltp - -> let ltp' = OL.lexp_close (ectx_to_lctx ctx) ltp in + (* FIXME: This `L.clean` is basically the last remaining use of the + * function. It's not indispensible, tho it might still be useful for + * performance of type-inference (at least until we have proper + * memoization of push_susp and/or whnf). *) + -> let ltp' = L.clean (OL.lexp_close (ectx_to_lctx ctx) ltp) in let bi = mkBuiltin ((loc, name), ltp', None) in if not (SMap.mem name (!EV.builtin_functions)) then sexp_error loc ("Unknown built-in `" ^ name ^ "`"); @@ -1512,8 +1621,7 @@ let rec sform_lambda kind ctx loc sargs ot = * in order to account for the fact that `arg` and `v` * might not be the same name! *) | Some lt2 - -> let s = S.cons (mkVar (arg, 0)) (S.shift 1) in - Some (mkSusp lt2 s) in + -> Some (srename arg lt2) in let (lbody, alt) = elaborate nctx sbody olt2 in (mkLambda (kind, arg, lt1, lbody), match alt with @@ -1533,10 +1641,20 @@ let rec sform_lambda kind ctx loc sargs ot = -> (match olt1 with | None -> () | Some lt1' - -> if not (OL.conv_p (ectx_to_lctx ctx) lt1 lt1') - then lexp_error (lexp_location lt1') lt1' - ("Type mismatch! Context expected `" - ^ lexp_string lt1 ^ "`")); + -> (match Unif.unify lt1' lt1 (ectx_to_lctx ctx) with + | ((ck, _ctx, t1, t2)::_) + -> lexp_error (lexp_location lt1') lt1' + ("Type mismatch(" + ^ (match ck with | Unif.CKimpossible -> "impossible" + | Unif.CKresidual -> "residue") + ^ ")! Context expected:\n " + ^ lexp_string lt1 ^ "\nbut parameter has type:\n " + ^ lexp_string lt1' ^ "\ncan't unify:\n " + ^ lexp_string t1 + ^ "\nwith:\n " + ^ lexp_string t2); + assert (not (OL.conv_p (ectx_to_lctx ctx) lt1' lt1)) + | [] -> ())); mklam lt1 (Some lt2) | Arrow (ak2, v, lt1, _, lt2) when kind = Anormal ===================================== src/eval.ml ===================================== @@ -552,20 +552,11 @@ and eval_decls (decls: (vname * elexp) list) (String -> Sexp) -> (Int -> Sexp) -> (Float -> Sexp) -> (List Sexp -> Sexp) -> Sexp *) and sexp_dispatch loc depth args = - let eval a b = eval a b depth in - let sxp, nd, ctx_nd, - sym, ctx_sym, - str, ctx_str, - it, ctx_it, - flt, ctx_flt, - blk, ctx_blk = match args with - (* FIXME: Don't match against `Closure` to later use `eval`, instead - * pass the value to "funcall". *) - | [sxp; Closure(_, nd, ctx_nd); Closure(_, sym, ctx_sym); - Closure(_, str, ctx_str); Closure(_, it, ctx_it); - Closure(_, flt, ctx_flt); Closure(_, blk, ctx_blk)] -> - sxp, nd, ctx_nd, sym, ctx_sym, str, ctx_str, it, ctx_it, - flt, ctx_flt, blk, ctx_blk + let trace_dum = (Var ((loc, None), -1)) in + let eval_call a b = eval_call loc trace_dum depth a b in + let sxp, nd, sym, str, it, flt, blk = match args with + | [sxp; nd; sym; str; it; flt; blk] -> + sxp, nd, sym, str, it, flt, blk | _ -> error loc "sexp_dispatch expects 7 arguments" in let sxp = match sxp with @@ -573,34 +564,17 @@ and sexp_dispatch loc depth args = | _ -> value_fatal loc sxp "sexp_dispatch expects a Sexp as 1st arg" in match sxp with - | Node (op, s) ->( - let rctx = ctx_nd in - let rctx = add_rte_variable vdummy (Vsexp(op)) rctx in - let rctx = add_rte_variable vdummy (o2v_list s) rctx in - match eval nd rctx with - | Closure(_, nd, _) -> eval nd rctx - | _ -> error loc "Node has 2 arguments") - - | Symbol (_ , s) -> - let rctx = ctx_sym in - eval sym (add_rte_variable vdummy (Vstring s) rctx) - | String (_ , s) -> - let rctx = ctx_str in - eval str (add_rte_variable vdummy (Vstring s) rctx) - | Integer (_ , i) -> - let rctx = ctx_it in - eval it (add_rte_variable vdummy (Vinteger (BI.of_int i)) - rctx) - | Float (_ , f) -> - let rctx = ctx_flt in - eval flt (add_rte_variable vdummy (Vfloat f) rctx) + | Node (op, s) -> eval_call nd [Vsexp op; o2v_list s] + | Symbol (_ , s) -> eval_call sym [Vstring s] + | String (_ , s) -> eval_call str [Vstring s] + | Integer (_ , i) -> eval_call it [Vint i] + | Float (_ , f) -> eval_call flt [Vfloat f] | Block (_ , _, _) as b -> (* I think this code breaks what Blocks are. *) (* We delay parsing but parse with default_stt and default_grammar... *) (*let toks = Lexer.lex default_stt s in let s = sexp_parse_all_to_list default_grammar toks (Some ";") in*) - let rctx = ctx_blk in - eval blk (add_rte_variable vdummy (Vsexp b) rctx) + eval_call blk [Vsexp b] (* -------------------------------------------------------------------------- *) and print_eval_result i lxp = @@ -1113,16 +1087,15 @@ let from_lctx (lctx: lexp_context): runtime_env = Myers.cons (loname, ref (match def with | LetDef (_, e) - -> let e = L.clean e in - if closed_p rctx (OL.fv e) then - eval (OL.erase_type e) rctx - else Vundefined + -> if closed_p rctx (OL.fv e) then + eval (OL.erase_type e) rctx + else Vundefined | _ -> Vundefined)) rctx | CVfix (defs, lctx) -> let fvs = List.fold_left (fun fvs (_, e, _) - -> OL.fv_union fvs (OL.fv (L.clean e))) + -> OL.fv_union fvs (OL.fv e)) OL.fv_empty defs in let rctx = from_lctx lctx in ===================================== src/inverse_subst.ml ===================================== @@ -1,6 +1,6 @@ (* inverse_subst.ml --- Computing the inverse of a substitution -Copyright (C) 2016-2019 Free Software Foundation, Inc. +Copyright (C) 2016-2020 Free Software Foundation, Inc. Author: Vincent Bonnevalle <tiv.crb(a)gmail.com> @@ -253,7 +253,7 @@ and apply_inv_subst (e : lexp) (s : subst) : lexp = match e with | SortLevel (SLz) -> e | SortLevel (SLsucc e) -> mkSortLevel (mkSLsucc (apply_inv_subst e s)) | SortLevel (SLlub (e1, e2)) - (* Should we use mkSLlub? *) + (* FIXME: use mkSLlub? *) -> mkSortLevel (mkSLlub' (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 @@ -293,7 +293,7 @@ and apply_inv_subst (e : lexp) (s : subst) : lexp = match e with L.rev ncase) cases in mkInductive (l, label, nargs, ncases) - | Cons (it, name) -> Cons (apply_inv_subst it s, name) + | Cons (it, name) -> mkCons (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) ===================================== src/lexp.ml ===================================== @@ -295,6 +295,15 @@ and slookup s l v = S.lookup (fun l i -> mkVar (l, i)) s l v let ssink = S.sink (fun l i -> mkVar (l, i)) +(* Apply a "dummy" substitution which replace #0 with #0 + * in order to account for changes to a variable's name. + * This should probably be made into a no-op, but only after we get rid + * of the check in DB.lookup that a `Var` has the same name as the + * one stored in the lctx! + * Using DeBruijn *should* make α-renaming unnecessary + * so this is a real PITA! :-( *) +let srename name le = mkSusp le (S.cons (mkVar (name, 0)) (S.shift 1)) + (* Shift by a negative amount! *) let rec sunshift n = if n = 0 then S.identity @@ -393,7 +402,7 @@ let rec push_susp e s = (* Push a suspension one level down. *) L.rev ncase) cases in mkInductive (l, label, nargs, ncases) - | Cons (it, name) -> Cons (mkSusp it s, name) + | Cons (it, name) -> mkCons (mkSusp it s, name) | Case (l, e, ret, cases, default) -> mkCase (l, mkSusp e s, mkSusp ret s, SMap.map (fun (l, cargs, e) @@ -631,7 +640,6 @@ and lexp_name e = type print_context_value = | Bool of bool | Int of int - | Expr of lexp option | Predtl of grammar (* precedence table *) type print_context = print_context_value SMap.t @@ -646,8 +654,6 @@ let pretty_ppctx = ("color" , Bool (true) ); (* use console color to display hints *) ("separate_decl" , Bool (true) ); (* print newline between declarations *) ("indent_level" , Int (0) ); (* current indent level *) - ("parent" , Expr (None) ); (* parent expression *) - ("metavar" , Expr (None) ); (* metavar being printed *) ("col_max" , Int (80) ); (* col_size + col_ofsset <= col_max *) ("col_size" , Int (0) ); (* current column size *) ("col_ofsset" , Int (0) ); (* if col does not start at 0 *) @@ -669,8 +675,6 @@ let smap_bool s ctx = match SMap.find s ctx with Bool b -> b | _ -> failwith "Unreachable" and smap_int s ctx = match SMap.find s ctx with Int i -> i | _ -> failwith "Unreachable" -and smap_lexp s ctx = - match SMap.find s ctx with Expr e -> e | _ -> failwith "Unreachable" and smap_predtl s ctx = match SMap.find s ctx with Predtl tl -> tl | _ -> failwith "Unreachable" @@ -681,8 +685,6 @@ let pp_size = smap_int "indent_size" let pp_color = smap_bool "color" let pp_decl = smap_bool "separate_decl" let pp_indent = smap_int "indent_level" -let pp_parent = smap_lexp "parent" -let pp_meta = smap_lexp "metavar" let pp_grammar = smap_predtl "grammar" let pp_colsize = smap_int "col_size" let pp_colmax = smap_int "col_max" @@ -692,8 +694,6 @@ let pp_implicit = smap_bool "print_implicit" let set_col_size p ctx = SMap.add "col_size" (Int p) ctx let add_col_size p ctx = set_col_size ((pp_colsize ctx) + p) ctx let reset_col_size ctx = set_col_size 0 ctx -let set_parent p ctx = SMap.add "parent" (Expr (Some p)) ctx -let set_meta p ctx = SMap.add "metavar" (Expr (Some p)) ctx let add_indent ctx i = SMap.add "indent_level" (Int ((pp_indent ctx) + i)) ctx let pp_append_string buffer ctx str = @@ -743,7 +743,6 @@ and lexp_cstring ctx e = lexp_str ctx e (* Implementation *) and lexp_str ctx (exp : lexp) : string = - let ctx = set_parent exp ctx in let inter_ctx = add_indent ctx 1 in let lexp_str' = lexp_str ctx in let lexp_stri idt e = lexp_str (add_indent ctx idt) e in @@ -805,15 +804,9 @@ and lexp_str ctx (exp : lexp) : string = | Metavar (idx, subst, (loc, name)) (* print metavar result if any *) - -> (let print_meta exp = - let ctx = set_meta exp ctx in - lexp_str ctx (clean exp) in - - match pp_meta ctx with - | None -> print_meta exp - | Some e when e != exp -> print_meta exp - | _ -> - "?" ^ maybename name ^ (subst_string subst) ^ (index idx)) + -> (match metavar_lookup idx with + | MVal e -> lexp_str ctx e + | _ -> "?" ^ maybename name ^ (subst_string subst) ^ (index idx)) | Let (_, decls, body) -> (* Print first decls without indent *) ===================================== src/opslexp.ml ===================================== @@ -113,7 +113,7 @@ let lexp_close lctx e = * - It turns the lctx (of O(log N) access time) into a subst * (of O(N) access time) * Oh well! *) - L.clean (mkSusp e (lctx_to_subst lctx)) + mkSusp e (lctx_to_subst lctx) (** Reduce to weak head normal form. @@ -177,7 +177,10 @@ let lexp_whnf e (ctx : DB.lexp_context) : lexp = mkCase (l, e, rt, branches, default) in (match e' with | Cons (_, (_, name)) -> reduce name [] - | Call (Cons (_, (_, name)), aargs) -> reduce name aargs + | Call (f, aargs) -> + (match lexp_whnf f ctx with + | Cons (_, (_, name)) -> reduce name aargs + | _ -> mkCase (l, e, rt, branches, default)) | _ -> mkCase (l, e, rt, branches, default)) | Metavar (idx, s, _) -> (match metavar_lookup idx with @@ -231,6 +234,7 @@ let level_canon e = | SortLevel SLz -> if c < d then (d, m) else acc | SortLevel (SLsucc e) -> canon e (d + 1) acc | SortLevel (SLlub (e1, e2)) -> canon e1 d (canon e2 d acc) + (* FIXME: Apply substitutions from surrounding `Let` bindings. *) | Var (_, i) -> add_var_depth i d acc | Metavar (i, s, _) -> (match metavar_lookup i with @@ -263,8 +267,8 @@ let rec conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = -> (match (sl1, sl2) with | (SLz, SLz) -> true | (SLsucc sl1, SLsucc sl2) -> conv_p sl1 sl2 - | _ -> let ce1 = level_canon (L.clean e1') in - let ce2 = level_canon (L.clean e2') in + | _ -> let ce1 = level_canon e1' in + let ce2 = level_canon e2' in level_leq ce1 ce2 && level_leq ce2 ce1) | (Sort (_, s1), Sort (_, s2)) -> s1 == s2 @@ -277,7 +281,7 @@ let rec conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = -> ak1 == ak2 && conv_p t11 t21 && conv_p' (DB.lexp_ctx_cons ctx vd1 Variable t11) (set_shift vs') - t12 t22 + t12 (srename vd1 t22) | (Lambda (ak1, l1, t1, e1), Lambda (ak2, l2, t2, e2)) -> ak1 == ak2 && (conv_erase || conv_p t1 t2) && conv_p' (DB.lexp_ctx_cons ctx l1 Variable t1) @@ -334,8 +338,8 @@ let rec mkSLlub ctx e1 e2 = | (SortLevel (SLsucc e1), SortLevel (SLsucc e2)) -> mkSortLevel (SLsucc (mkSLlub ctx e1 e2)) | (e1', e2') - -> let ce1 = level_canon (L.clean e1') in - let ce2 = level_canon (L.clean e2') in + -> let ce1 = level_canon e1' in + let ce2 = level_canon e2' in if level_leq ce1 ce2 then e2 else if level_leq ce2 ce1 then e1 else mkSortLevel (mkSLlub' (e1, e2)) (* FIXME: Could be more canonical *) @@ -420,9 +424,9 @@ let rec check'' erased ctx e = if conv_p ctx t t' then () else (error_tc ~loc:(lexp_location e) ("Type mismatch for " - ^ lexp_string (L.clean e) ^ " : " - ^ lexp_string (L.clean t) ^ " != " - ^ lexp_string (L.clean t')); + ^ lexp_string e ^ " : " + ^ lexp_string t ^ " != " + ^ lexp_string t'); (* Log.internal_error "Type mismatch" *)) in let check_type erased ctx t = let s = check erased ctx t in @@ -939,7 +943,11 @@ let rec erase_type (lxp: L.lexp): E.elexp = | L.Sort _ -> E.Type lxp (* Still useful to some extent. *) | L.Inductive(l, label, _, _) -> E.Type lxp - | L.Metavar _ -> Log.internal_error "Metavar in erase_type" + | Metavar (idx, s, _) + -> (match metavar_lookup idx with + | MVal e -> erase_type (push_susp e s) + | MVar (_, t, _) + -> Log.internal_error "Metavar in erase_type") and filter_arg_list lst = let rec filter_arg_list lst acc = ===================================== src/unification.ml ===================================== @@ -190,20 +190,26 @@ and unify' (e1: lexp) (e2: lexp) if changed && OL.set_member_p vs e1' e2' then [] else let vs' = if changed then OL.set_add vs e1' e2' else vs in match (e1', e2') with - | ((Imm _, Imm _) | (Cons _, Cons _) | (Builtin _, Builtin _) - | (Var _, Var _)) + | ((Imm _, Imm _) | (Cons _, Cons _) | (Builtin _, Builtin _)) -> if OL.conv_p ctx e1' e2' then [] else [(CKimpossible, ctx, e1, e2)] | (l, (Metavar (idx, s, _) as r)) -> unify_metavar ctx idx s r l | ((Metavar (idx, s, _) as l), r) -> unify_metavar ctx idx s l r - | (l, (Call _ as r)) -> unify_call r l ctx vs' - (* | (l, (Case _ as r)) -> unify_case r l subst *) - | (Arrow _ as l, r) -> unify_arrow l r ctx vs' - | (Lambda _ as l, r) -> unify_lambda l r ctx vs' - | (Call _ as l, r) -> unify_call l r ctx vs' - (* | (Case _ as l, r) -> unify_case l r subst *) - (* | (Inductive _ as l, r) -> unify_induct l r subst *) - | (Sort _ as l, r) -> unify_sort l r ctx vs' - | (SortLevel _ as l, r) -> unify_sortlvl l r ctx vs' + | (l, (Call _ as r)) -> unify_call r l ctx vs' + | ((Call _ as l), r) -> unify_call l r ctx vs' + | (l, (Var _ as r)) -> unify_var r l ctx vs' + | ((Var _ as l), r) -> unify_var l r ctx vs' + | (l, (Arrow _ as r)) -> unify_arrow r l ctx vs' + | ((Arrow _ as l), r) -> unify_arrow l r ctx vs' + | (l, (Lambda _ as r)) -> unify_lambda r l ctx vs' + | ((Lambda _ as l), r) -> unify_lambda l r ctx vs' + (* | (l, (Case _ as r)) -> unify_case r l subst *) + (* | ((Case _ as l), r) -> unify_case l r subst *) + (* | (l, (Inductive _ as r)) -> unify_induct r l subst *) + (* | ((Inductive _ as l), r) -> unify_induct l r subst *) + | (l, (Sort _ as r)) -> unify_sort r l ctx vs' + | ((Sort _ as l), r) -> unify_sort l r ctx vs' + | (l, (SortLevel _ as r)) -> unify_sortlvl r l ctx vs' + | ((SortLevel _ as l), r) -> unify_sortlvl l r ctx vs' | (Inductive (_loc1, label1, args1, consts1), Inductive (_loc2, label2, args2, consts2)) -> (* print_string ("Unifying inductives " @@ -222,7 +228,6 @@ and unify' (e1: lexp) (e2: lexp) - (Arrow, Arrow) -> if var_kind = var_kind then unify ltype & lexp (Arrow (var_kind, _, ltype, lexp)) else None - - (Arrow, Var) -> Constraint - (_, _) -> None *) and unify_arrow (arrow: lexp) (lxp: lexp) ctx vs @@ -232,22 +237,16 @@ and unify_arrow (arrow: lexp) (lxp: lexp) ctx vs Arrow (var_kind2, _, ltype2, _, lexp2)) -> if var_kind1 = var_kind2 then (unify' ltype1 ltype2 ctx vs) - @(unify' lexp1 lexp2 + @(unify' lexp1 (srename v1 lexp2) (DB.lexp_ctx_cons ctx v1 Variable ltype1) (OL.set_shift vs)) - else [(CKimpossible, ctx, arrow, lxp)] - | (Arrow _, Imm _) -> [(CKimpossible, ctx, arrow, lxp)] - | (Arrow _, Var _) -> ([(CKresidual, ctx, arrow, lxp)]) - | (Arrow _, _) -> unify' lxp arrow ctx vs + else [(CKimpossible, ctx, arrow, lxp)] | (_, _) -> [(CKimpossible, ctx, arrow, lxp)] (** Unify a Lambda and a lexp if possible - - Lamda , Lambda -> if var_kind = var_kind + - Lambda , Lambda -> if var_kind = var_kind then UNIFY ltype & lxp else ERROR - - Lambda , Var -> CONSTRAINT - - Lambda , Call -> Constraint - - Lambda , Let -> Constraint - - Lambda , lexp -> unify lexp lambda subst + - Lambda , _ -> Impossible *) and unify_lambda (lambda: lexp) (lxp: lexp) ctx vs : return_type = match (lambda, lxp) with @@ -259,19 +258,12 @@ and unify_lambda (lambda: lexp) (lxp: lexp) ctx vs : return_type = (DB.lexp_ctx_cons ctx v1 Variable ltype1) (OL.set_shift vs)) else [(CKimpossible, ctx, lambda, lxp)] - | ((Lambda _, Var _) - | (Lambda _, Let _) - | (Lambda _, Call _)) -> [(CKresidual, ctx, lambda, lxp)] - | (Lambda _, Arrow _) - | (Lambda _, Imm _) -> [(CKimpossible, ctx, lambda, lxp)] - | (Lambda _, _) -> unify' lxp lambda ctx vs - | (_, _) -> [(CKimpossible, ctx, lambda, lxp)] + | (_, _) -> [(CKimpossible, ctx, lambda, lxp)] (** Unify a Metavar and a lexp if possible - - lexp , {metavar <-> none} -> UNIFY - - lexp , {metavar <-> lexp} -> UNFIFY lexp subst[metavar] - - metavar , metavar -> if Metavar = Metavar then OK else ERROR - - metavar , lexp -> OK + - metavar , metavar -> if Metavar = Metavar then intersect + - metavar , metavar -> inverse subst (both sides) + - metavar , lexp -> inverse subst *) and unify_metavar ctx idx s1 (lxp1: lexp) (lxp2: lexp) : return_type = @@ -296,8 +288,8 @@ and unify_metavar ctx idx s1 (lxp1: lexp) (lxp2: lexp) | _ -> log_info ?loc:None ("Unification of metavar type failed:\n " - ^ lexp_string (Lexp.clean t) ^ " != " - ^ lexp_string (Lexp.clean (OL.get_type ctx lxp)) + ^ lexp_string t ^ " != " + ^ lexp_string (OL.get_type ctx lxp) ^ "\n" ^ "for " ^ lexp_string lxp ^ "\n"); [(CKresidual, ctx, lxp1, lxp2)] in match lxp2 with @@ -364,6 +356,16 @@ and unify_metavar ctx idx s1 (lxp1: lexp) (lxp2: lexp) | _ -> unif idx2 s2 lxp1) | _ -> unif idx s1 lxp2 +(** Unify a Var (var) and a lexp (lxp) + - Var , Var -> IF same var THEN ok ELSE constraint + - Var , lexp -> Constraint +*) +and unify_var (var: lexp) (lxp: lexp) ctx vs + : return_type = + match (var, lxp) with + | (Var _, Var _) when OL.conv_p ctx var lxp -> [] + | (_, _) -> [(CKresidual, ctx, var, lxp)] + (** Unify a Call (call) and a lexp (lxp) - Call , Call -> UNIFY - Call , lexp -> CONSTRAINT @@ -452,7 +454,6 @@ and unify_sortlvl (sortlvl: lexp) (lxp: lexp) ctx vs : return_type = (** Unify a Sort and a lexp - Sort, Sort -> if Sort ~= Sort then OK else ERROR - - Sort, Var -> Constraint - Sort, lexp -> ERROR *) and unify_sort (sort_: lexp) (lxp: lexp) ctx vs : return_type = @@ -462,7 +463,6 @@ and unify_sort (sort_: lexp) (lxp: lexp) ctx vs : return_type = | StypeOmega, StypeOmega -> [] | StypeLevel, StypeLevel -> [] | _, _ -> [(CKimpossible, ctx, sort_, lxp)]) - | Sort _, Var _ -> [(CKresidual, ctx, sort_, lxp)] | _, _ -> [(CKimpossible, ctx, sort_, lxp)] (************************ Helper function ************************************) View it on GitLab: https://gitlab.com/monnier/typer/-/compare/386de0963b1b57e1ee89e36077294f1f… -- View it on GitLab: https://gitlab.com/monnier/typer/-/compare/386de0963b1b57e1ee89e36077294f1f… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer] Pushed new branch ja-barszcz
by Jean-Alexandre Barszcz 10 Avr '20

10 Avr '20

Jean-Alexandre Barszcz pushed new branch ja-barszcz at Stefan / Typer -- View it on GitLab: https://gitlab.com/monnier/typer/-/tree/ja-barszcz You're receiving this email because of your account on gitlab.com.

2 1

[Git][monnier/typer][master] Remove most uses of L.clean
by Stefan 08 Avr '20

08 Avr '20

Stefan pushed to branch master at Stefan / Typer Commits: 886a3589 by Stefan Monnier at 2020-04-08T18:07:18-04:00 Remove most uses of L.clean * src/elab.ml (elab_check_sort, elab_check_def, infer_type): Skip `L.clean` since `lexp_string` already cleans up on the fly. (track_fv): Skip `L.clean` since `fv` already cleans up on the fly. (lexp_eval): Skip `L.clean` since `fv` and `erase_type` already clean up on the fly. (sform_new_attribute, sform_add_attribute, sform_built_in): Explicitly call `clean` now that `lexp_close` doesn't do it any more. * src/eval.ml (from_lctx): Skip `L.clean` since `fv` and `erase_type` already clean up on the fly. * src/lexp.ml (print_context_value): Remove `Expr` constructor. (pretty_ppctx): Remove unused `parent` and now unused `metavar`. (smap_lexp, pp_parent, pp_meta, set_parent, set_parent): Remove functions. (lexp_str): Don't call `set_parent` any more. Rewrite metavar case to use `metavar_lookup` rather than `clean`. * src/opslexp.ml (lexp_close): Don't call `clean` any more. (conv_p', mkSLlub): Skip `L.clean` since `level_canon` already cleans up on the fly. (check''.assert_type): Skip `L.clean` since `lexp_string` already cleans up on the fly. (erase_type): Clean up metavars on the fly. * src/unification.ml (unify_metavar): Skip `L.clean` since `lexp_string` already cleans up on the fly. - - - - - 6 changed files: - src/elab.ml - src/eval.ml - src/inverse_subst.ml - src/lexp.ml - src/opslexp.ml - src/unification.ml Changes: ===================================== src/elab.ml ===================================== @@ -128,8 +128,7 @@ let elab_check_sort (ctx : elab_context) lsort var ltp = "Exception during whnf of sort:"; raise e) with | Sort (_, _) -> () (* All clear! *) - | _ -> let lexp_string e = lexp_string (L.clean e) in - let typestr = lexp_string ltp ^ " : " ^ lexp_string lsort in + | _ -> let typestr = lexp_string ltp ^ " : " ^ lexp_string lsort in match var with | (l, None) -> lexp_error l ltp ("`" ^ typestr ^ "` is not a proper type") @@ -159,7 +158,6 @@ let elab_check_def (ctx : elab_context) var lxp ltype = let lctx = ectx_to_lctx ctx in let loc = lexp_location lxp in - let lexp_string e = lexp_string (L.clean e) in let ltype' = try OL.check lctx lxp with e -> match e with | Log.Stop_Compilation _ -> raise e @@ -655,8 +653,7 @@ and infer_type pexp ectx var = s (ectx_to_lctx ectx) with | (_::_) - -> (let lexp_string e = lexp_string (L.clean e) in - let typestr = lexp_string t ^ " : " ^ lexp_string s in + -> (let typestr = lexp_string t ^ " : " ^ lexp_string s in match var with | (l, None) -> lexp_error l t ("`" ^ typestr ^ "` is not a proper type") @@ -1042,13 +1039,12 @@ and track_fv rctx lctx e = name ^ " (" ^ track_fv (Myers.nthcdr drop rctx) (Myers.nthcdr drop lctx) - (L.clean e) + e ^ ")" | _ -> name in String.concat " " (List.map tfv nc) and lexp_eval ectx e = - let e = L.clean e in let ee = OL.erase_type e in let rctx = EV.from_ectx ectx in @@ -1334,7 +1330,7 @@ and sform_new_attribute ctx loc sargs ot = * is False, for example): Should be a type like `AttributeMap t` * instead. *) (mkBuiltin ((loc, "new-attribute"), - OL.lexp_close (ectx_to_lctx ctx) ltp, + L.clean (OL.lexp_close (ectx_to_lctx ctx) ltp), Some AttributeMap.empty), Lazy) | _ -> fatal ~loc "new-attribute expects a single Type argument" @@ -1350,7 +1346,7 @@ and sform_add_attribute ctx loc (sargs : sexp list) ot = | _ -> fatal ~loc "add-attribute expects a table as first argument" in (* FIXME: Type check (attr: type == attr_type) *) - let attr' = OL.lexp_close (ectx_to_lctx ctx) attr in + let attr' = L.clean (OL.lexp_close (ectx_to_lctx ctx) attr) in let table = AttributeMap.add var attr' map in (mkBuiltin ((loc, "add-attribute"), attr_type, Some table), Lazy) @@ -1411,7 +1407,11 @@ let sform_built_in ctx loc sargs ot = | true, [String (_, name)] -> (match ot with | Some ltp - -> let ltp' = OL.lexp_close (ectx_to_lctx ctx) ltp in + (* FIXME: This `L.clean` is basically the last remaining use of the + * function. It's not indispensible, tho it might still be useful for + * performance of type-inference (at least until we have proper + * memoization of push_susp and/or whnf). *) + -> let ltp' = L.clean (OL.lexp_close (ectx_to_lctx ctx) ltp) in let bi = mkBuiltin ((loc, name), ltp', None) in if not (SMap.mem name (!EV.builtin_functions)) then sexp_error loc ("Unknown built-in `" ^ name ^ "`"); ===================================== src/eval.ml ===================================== @@ -1113,16 +1113,15 @@ let from_lctx (lctx: lexp_context): runtime_env = Myers.cons (loname, ref (match def with | LetDef (_, e) - -> let e = L.clean e in - if closed_p rctx (OL.fv e) then - eval (OL.erase_type e) rctx - else Vundefined + -> if closed_p rctx (OL.fv e) then + eval (OL.erase_type e) rctx + else Vundefined | _ -> Vundefined)) rctx | CVfix (defs, lctx) -> let fvs = List.fold_left (fun fvs (_, e, _) - -> OL.fv_union fvs (OL.fv (L.clean e))) + -> OL.fv_union fvs (OL.fv e)) OL.fv_empty defs in let rctx = from_lctx lctx in ===================================== src/inverse_subst.ml ===================================== @@ -1,6 +1,6 @@ (* inverse_subst.ml --- Computing the inverse of a substitution -Copyright (C) 2016-2019 Free Software Foundation, Inc. +Copyright (C) 2016-2020 Free Software Foundation, Inc. Author: Vincent Bonnevalle <tiv.crb(a)gmail.com> @@ -253,7 +253,7 @@ and apply_inv_subst (e : lexp) (s : subst) : lexp = match e with | SortLevel (SLz) -> e | SortLevel (SLsucc e) -> mkSortLevel (mkSLsucc (apply_inv_subst e s)) | SortLevel (SLlub (e1, e2)) - (* Should we use mkSLlub? *) + (* FIXME: use mkSLlub? *) -> mkSortLevel (mkSLlub' (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 ===================================== src/lexp.ml ===================================== @@ -640,7 +640,6 @@ and lexp_name e = type print_context_value = | Bool of bool | Int of int - | Expr of lexp option | Predtl of grammar (* precedence table *) type print_context = print_context_value SMap.t @@ -655,8 +654,6 @@ let pretty_ppctx = ("color" , Bool (true) ); (* use console color to display hints *) ("separate_decl" , Bool (true) ); (* print newline between declarations *) ("indent_level" , Int (0) ); (* current indent level *) - ("parent" , Expr (None) ); (* parent expression *) - ("metavar" , Expr (None) ); (* metavar being printed *) ("col_max" , Int (80) ); (* col_size + col_ofsset <= col_max *) ("col_size" , Int (0) ); (* current column size *) ("col_ofsset" , Int (0) ); (* if col does not start at 0 *) @@ -678,8 +675,6 @@ let smap_bool s ctx = match SMap.find s ctx with Bool b -> b | _ -> failwith "Unreachable" and smap_int s ctx = match SMap.find s ctx with Int i -> i | _ -> failwith "Unreachable" -and smap_lexp s ctx = - match SMap.find s ctx with Expr e -> e | _ -> failwith "Unreachable" and smap_predtl s ctx = match SMap.find s ctx with Predtl tl -> tl | _ -> failwith "Unreachable" @@ -690,8 +685,6 @@ let pp_size = smap_int "indent_size" let pp_color = smap_bool "color" let pp_decl = smap_bool "separate_decl" let pp_indent = smap_int "indent_level" -let pp_parent = smap_lexp "parent" -let pp_meta = smap_lexp "metavar" let pp_grammar = smap_predtl "grammar" let pp_colsize = smap_int "col_size" let pp_colmax = smap_int "col_max" @@ -701,8 +694,6 @@ let pp_implicit = smap_bool "print_implicit" let set_col_size p ctx = SMap.add "col_size" (Int p) ctx let add_col_size p ctx = set_col_size ((pp_colsize ctx) + p) ctx let reset_col_size ctx = set_col_size 0 ctx -let set_parent p ctx = SMap.add "parent" (Expr (Some p)) ctx -let set_meta p ctx = SMap.add "metavar" (Expr (Some p)) ctx let add_indent ctx i = SMap.add "indent_level" (Int ((pp_indent ctx) + i)) ctx let pp_append_string buffer ctx str = @@ -752,7 +743,6 @@ and lexp_cstring ctx e = lexp_str ctx e (* Implementation *) and lexp_str ctx (exp : lexp) : string = - let ctx = set_parent exp ctx in let inter_ctx = add_indent ctx 1 in let lexp_str' = lexp_str ctx in let lexp_stri idt e = lexp_str (add_indent ctx idt) e in @@ -814,15 +804,9 @@ and lexp_str ctx (exp : lexp) : string = | Metavar (idx, subst, (loc, name)) (* print metavar result if any *) - -> (let print_meta exp = - let ctx = set_meta exp ctx in - lexp_str ctx (clean exp) in - - match pp_meta ctx with - | None -> print_meta exp - | Some e when e != exp -> print_meta exp - | _ -> - "?" ^ maybename name ^ (subst_string subst) ^ (index idx)) + -> (match metavar_lookup idx with + | MVal e -> lexp_str ctx e + | _ -> "?" ^ maybename name ^ (subst_string subst) ^ (index idx)) | Let (_, decls, body) -> (* Print first decls without indent *) ===================================== src/opslexp.ml ===================================== @@ -113,7 +113,7 @@ let lexp_close lctx e = * - It turns the lctx (of O(log N) access time) into a subst * (of O(N) access time) * Oh well! *) - L.clean (mkSusp e (lctx_to_subst lctx)) + mkSusp e (lctx_to_subst lctx) (** Reduce to weak head normal form. @@ -231,6 +231,7 @@ let level_canon e = | SortLevel SLz -> if c < d then (d, m) else acc | SortLevel (SLsucc e) -> canon e (d + 1) acc | SortLevel (SLlub (e1, e2)) -> canon e1 d (canon e2 d acc) + (* FIXME: Apply substitutions from surrounding `Let` bindings. *) | Var (_, i) -> add_var_depth i d acc | Metavar (i, s, _) -> (match metavar_lookup i with @@ -263,8 +264,8 @@ let rec conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = -> (match (sl1, sl2) with | (SLz, SLz) -> true | (SLsucc sl1, SLsucc sl2) -> conv_p sl1 sl2 - | _ -> let ce1 = level_canon (L.clean e1') in - let ce2 = level_canon (L.clean e2') in + | _ -> let ce1 = level_canon e1' in + let ce2 = level_canon e2' in level_leq ce1 ce2 && level_leq ce2 ce1) | (Sort (_, s1), Sort (_, s2)) -> s1 == s2 @@ -334,8 +335,8 @@ let rec mkSLlub ctx e1 e2 = | (SortLevel (SLsucc e1), SortLevel (SLsucc e2)) -> mkSortLevel (SLsucc (mkSLlub ctx e1 e2)) | (e1', e2') - -> let ce1 = level_canon (L.clean e1') in - let ce2 = level_canon (L.clean e2') in + -> let ce1 = level_canon e1' in + let ce2 = level_canon e2' in if level_leq ce1 ce2 then e2 else if level_leq ce2 ce1 then e1 else mkSortLevel (mkSLlub' (e1, e2)) (* FIXME: Could be more canonical *) @@ -420,9 +421,9 @@ let rec check'' erased ctx e = if conv_p ctx t t' then () else (error_tc ~loc:(lexp_location e) ("Type mismatch for " - ^ lexp_string (L.clean e) ^ " : " - ^ lexp_string (L.clean t) ^ " != " - ^ lexp_string (L.clean t')); + ^ lexp_string e ^ " : " + ^ lexp_string t ^ " != " + ^ lexp_string t'); (* Log.internal_error "Type mismatch" *)) in let check_type erased ctx t = let s = check erased ctx t in @@ -939,7 +940,11 @@ let rec erase_type (lxp: L.lexp): E.elexp = | L.Sort _ -> E.Type lxp (* Still useful to some extent. *) | L.Inductive(l, label, _, _) -> E.Type lxp - | L.Metavar _ -> Log.internal_error "Metavar in erase_type" + | Metavar (idx, s, _) + -> (match metavar_lookup idx with + | MVal e -> erase_type (push_susp e s) + | MVar (_, t, _) + -> Log.internal_error "Metavar in erase_type") and filter_arg_list lst = let rec filter_arg_list lst acc = ===================================== src/unification.ml ===================================== @@ -296,8 +296,8 @@ and unify_metavar ctx idx s1 (lxp1: lexp) (lxp2: lexp) | _ -> log_info ?loc:None ("Unification of metavar type failed:\n " - ^ lexp_string (Lexp.clean t) ^ " != " - ^ lexp_string (Lexp.clean (OL.get_type ctx lxp)) + ^ lexp_string t ^ " != " + ^ lexp_string (OL.get_type ctx lxp) ^ "\n" ^ "for " ^ lexp_string lxp ^ "\n"); [(CKresidual, ctx, lxp1, lxp2)] in match lxp2 with View it on GitLab: https://gitlab.com/monnier/typer/-/commit/886a3589162b84e04cf63684239255054… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/886a3589162b84e04cf63684239255054… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][master] * src/elab.ml (meta_to_var): Rework to be able to infer universe levels
by Stefan 07 Avr '20

07 Avr '20

Stefan pushed to branch master at Stefan / Typer Commits: 63f7644b by Stefan Monnier at 2020-04-07T23:21:05-04:00 * src/elab.ml (meta_to_var): Rework to be able to infer universe levels (generalize): Adjust for new calling convention of `meta_to_var` and also for the fact that `meta_to_var` now takes care of the S.shift for us. - - - - - 2 changed files: - btl/builtins.typer - src/elab.ml Changes: ===================================== btl/builtins.typer ===================================== @@ -31,6 +31,9 @@ %%%% Base Types used in builtin functions +%% Box : Type_ ?ℓ₁ -> Type_ ?ℓ₂; +%% Box = lambda (ℓ₃ : TypeLevel) ≡> typecons (Box (t : Type_ ℓ₃)) (box t); + %% TypeLevel_succ = Built-in "TypeLevel.succ" : TypeLevel -> TypeLevel; %% TypeLevel_⊔ = Built-in "TypeLevel.⊔" : TypeLevel -> TypeLevel -> TypeLevel; ===================================== src/elab.ml ===================================== @@ -311,39 +311,142 @@ let elab_varref ctx (loc, name) "` was not declared" ^ relateds); sform_dummy_ret ctx loc) -(* Turn metavar into plain vars after generalization. *) -let rec meta_to_var ids o (e : lexp) = - let rec loop e = match e with +(* Turn metavar into plain vars after generalization. + * ids: an IMap that maps metavars to their position as argument + * (first arg gets position 0). *) +let rec meta_to_var ids (e : lexp) = + + let count = IMap.cardinal ids in + + (* Yuck! Yuck! Yuck! + * This is very messy. What we need to do starts as follows: + * We have a `Γ ⊢ e : τ` and this `e` contains some metavars `m₁…mₙ : τ₁…τₙ` + * that we want to change into formal arguments, i.e. we want to turn `e` + * into something like + * + * Γ ⊢ λ x₁…xₙ ≡> e[x₁…xₙ/m₁…mₙ] : τ₁…τₙ ≡> τ + * + * The above substitution is not the usual capture-avoiding substitution + * since it replaces metavars with vars rather than vars with terms. + * It's more like *instanciation* of those metavars. + * And indeed, ideally it should be a simple matter of instanciating + * those metavars with temrs that are variable references. + * + * An important aspect here is that the rest of `e` also needs to be + * changed because it will now live in a new context: + * + * Γ,x₁:τ₁,…,xₙ:τₙ ⊢ e[x₁…xₙ/m₁…mₙ] : τ + * + * So we need to adjust all the variable references in `e` to account for + * that, which we normally do with a simple `S.shift n`. + * + * The first problem comes here: `S.shift n` takes a term from + * `Γ` to `Γ,x₁:τ₁,…,xₙ:τₙ`, making sure it still references the same + * bindings as before, i.e. it makes sure the result *cannot* refer to + * any `x₁…xₙ`! + * I first thought "it's OK, I'll first do the `S.shift n` and I only + * instanciate the metavars afterwards", but that does not help, + * because every reference to a metavar is properly wrapped in a + * pending application of the relevant substitution, so the `S.shift n` + * still applies to it. + * + * For this reason, we have a `loop` below which does the substitution + * of variable references for the metavars (since just instanciating + * the metavars doesn't work). + * + * The second problem comes with the other metavars in `e`. + * There are 3 kinds of metavars in `e`: + * + * A. Those that we want to replace with variable references. + * B. Those that live in some higher enclosing scope. + * C. The "others". + * + * Presumably, we have (A) under control. + * For (B) the situation is easy enough: since they live in a higher + * enlosing scope they can only refer to those variables that exist in + * some prefix of `Γ`, so we just need to apply `S.shift n` to them. + * + * For (C), we'd like those metavars (which originally could refer to + * any var in `Γ`) to now be a able to also refer to any of the + * new vars `x₁…xₙ`. So `S.shift n` is definitely not right for them. + * Instead, I ended up writing `adjust_subst` which hacks up + * the substitution attached to each metavar reference so it can + * now refer to its original context *and* to `x₁…xₙ`. + * + * Arguably, now that we handle (C), we could handle (A) by + * first treating them as (C) and then using instantiation. + * But the code for (A) was already written, and it doesn't seem like + * it would make things any simpler currently. + * + * Note: in the original HM algorithm (and in Twelf), (C) cannot occur + * because every metavariable that's not in (B) is generalized + * (i.e. will be in A). But here we need (C) for cases like: + * + * List : Type ? -> Type ?; + * + * Since the second `?` should not be generalized but should + * be inferred from the definition. I.e. the above should be + * generalized to: + * + * List : (ℓ : TypeLevel) ≡> Type ℓ -> Type ?; + * + * where the remaining `?` will be inferred by unification + * when type-checking the definition of `Box` where ti be unified with `ℓ`, + * the newly introduced variable! + *) + + (* `o` is the binding offset until the root. *) + let rec adjust_subst o s = match s with + | S.Identity n + -> let o' = o - n in + if o' < 0 then + (* This metavar's original context is outside of our scope + * (case (B) above), so don't let it refer to the new vars. *) + S.Identity (n + count) + else + Identity n + | S.Cons (e, s', n) + -> let o' = o - n in + if o' < 0 then + (* This metavar's original context is outside of our scope + * (case (B) above), so don't let it refer to the new vars. *) + S.Cons (e, s', n + count) + else + S.Cons (loop o' e, adjust_subst o' s', n) + + (* `o` is the binding depth at which we are relative to the "root" + * of the expression (i.e. where the new vars will be inserted). *) + and loop o e = match e with | Imm _ -> e | SortLevel SLz -> e - | SortLevel (SLsucc e) -> mkSortLevel (mkSLsucc (loop e)) - | SortLevel (SLlub (e1, e2)) -> mkSortLevel (mkSLlub' (loop e1, loop e2)) - | Sort (l, Stype e) -> mkSort (l, Stype (loop e)) + | SortLevel (SLsucc e) -> mkSortLevel (mkSLsucc (loop o e)) + | SortLevel (SLlub (e1, e2)) -> mkSortLevel (mkSLlub' (loop o e1, loop o e2)) + | Sort (l, Stype e) -> mkSort (l, Stype (loop o e)) | Sort (_, (StypeOmega | StypeLevel)) -> e | Builtin _ -> e - | Var _ -> e - | Susp (e, s) -> loop (push_susp e s) + | Var (n,i) -> if i < o then e else mkVar (n, i + count) + | Susp (e, s) -> loop o (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 ids (len + o) e, - meta_to_var ids (o' + o) t) :: defs)) + (o', (l, loop (len + o) e, + loop (o' + o) t) :: defs)) defs (len, []) in - mkLet (l, ndefs, meta_to_var ids (len + o) e) + mkLet (l, ndefs, loop (len + o) e) | Arrow (ak, v, t1, l, t2) - -> mkArrow (ak, v, loop t1, l, meta_to_var ids (1 + o) t2) + -> mkArrow (ak, v, loop o t1, l, loop (1 + o) t2) | Lambda (ak, v, t, e) - -> mkLambda (ak, v, loop t, meta_to_var ids (1 + o) e) + -> mkLambda (ak, v, loop o t, loop (1 + o) e) | Call (f, args) - -> mkCall (loop f, List.map (fun (ak, e) -> (ak, loop e)) args) + -> mkCall (loop o f, List.map (fun (ak, e) -> (ak, loop o 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 ids (o' + o) t) + (o', (ak, v, loop (o' + o) t) :: args)) args (alen, []) in let ncases @@ -354,31 +457,29 @@ let rec meta_to_var ids o (e : lexp) = = List.fold_right (fun (ak, v, t) (o', fields) -> let o' = o' - 1 in - (o', (ak, v, meta_to_var ids (o' + o) t) + (o', (ak, v, loop (o' + o) t) :: fields)) fields (flen + alen, []) in nfields) cases in mkInductive (l, label, nargs, ncases) - | Cons (t, l) -> mkCons (loop t, l) + | Cons (t, l) -> mkCons (loop o t, l) | Case (l, e, t, cases, default) -> let ncases = SMap.map (fun (l, fields, e) - -> (l, fields, meta_to_var ids (o + List.length fields) e)) + -> (l, fields, loop (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)) + mkCase (l, loop o e, loop o t, ncases, + match default with None -> None + | Some (v, e) -> Some (v, loop (1 + o) e)) | Metavar (id, s, name) -> if IMap.mem id ids then - mkVar (name, o + IMap.find id ids) + mkVar (name, o + count - IMap.find id ids) else match metavar_lookup id with - | MVal e -> loop (push_susp e s) - (* FIXME: The substitution applied before calling `meta_to_var` - * make it impossible for the metavar to refer to the newly - * introduced variables. *) - | _ -> e - in loop e + | MVal e -> loop o (push_susp e s) + | _ -> mkMetavar (id, adjust_subst o s, name) + in loop 0 e let move_typelevel_to_front ctx mfvs = (* TypeLevel arguments have to come first, so move them accordingly. *) @@ -421,17 +522,17 @@ let generalize (nctx : elab_context) e = let len = List.length mfvs in let mfvs = move_typelevel_to_front (ectx_to_lctx nctx) mfvs in fun wrap e -> - let rec loop ids n mfvs = match mfvs with - | [] -> assert (n = 0); - let e = mkSusp e (S.shift len) in - meta_to_var ids 0 e + let rec loop ids n mfvs = + assert (n = IMap.cardinal ids); + match mfvs with + | [] -> assert (n = len); + meta_to_var ids 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 mt' = meta_to_var ids 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 + wrap (IMap.mem id nes) vname mt' l e' in + loop (IMap.empty) 0 mfvs let elab_p_id ((l,name) : symbol) : vname = (l, match name with "_" -> None | _ -> Some name) View it on GitLab: https://gitlab.com/monnier/typer/-/commit/63f7644b69db00b352c60e38bee5ec390… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/63f7644b69db00b352c60e38bee5ec390… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][master] * src/lexp.ml (srename): New function
by Stefan 07 Avr '20

07 Avr '20

Stefan pushed to branch master at Stefan / Typer Commits: 4993afa5 by Stefan Monnier at 2020-04-07T23:15:21-04:00 * src/lexp.ml (srename): New function * src/unification.ml (unify): * src/opslexp.ml (conv_p'): * src/elab.ml (sform_lambda): Use it. - - - - - 4 changed files: - src/elab.ml - src/lexp.ml - src/opslexp.ml - src/unification.ml Changes: ===================================== src/elab.ml ===================================== @@ -1520,8 +1520,7 @@ let rec sform_lambda kind ctx loc sargs ot = * in order to account for the fact that `arg` and `v` * might not be the same name! *) | Some lt2 - -> let s = S.cons (mkVar (arg, 0)) (S.shift 1) in - Some (mkSusp lt2 s) in + -> Some (srename arg lt2) in let (lbody, alt) = elaborate nctx sbody olt2 in (mkLambda (kind, arg, lt1, lbody), match alt with ===================================== src/lexp.ml ===================================== @@ -295,6 +295,15 @@ and slookup s l v = S.lookup (fun l i -> mkVar (l, i)) s l v let ssink = S.sink (fun l i -> mkVar (l, i)) +(* Apply a "dummy" substitution which replace #0 with #0 + * in order to account for changes to a variable's name. + * This should probably be made into a no-op, but only after we get rid + * of the check in DB.lookup that a `Var` has the same name as the + * one stored in the lctx! + * Using DeBruijn *should* make α-renaming unnecessary + * so this is a real PITA! :-( *) +let srename name le = mkSusp le (S.cons (mkVar (name, 0)) (S.shift 1)) + (* Shift by a negative amount! *) let rec sunshift n = if n = 0 then S.identity ===================================== src/opslexp.ml ===================================== @@ -277,7 +277,7 @@ let rec conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = -> ak1 == ak2 && conv_p t11 t21 && conv_p' (DB.lexp_ctx_cons ctx vd1 Variable t11) (set_shift vs') - t12 t22 + t12 (srename vd1 t22) | (Lambda (ak1, l1, t1, e1), Lambda (ak2, l2, t2, e2)) -> ak1 == ak2 && (conv_erase || conv_p t1 t2) && conv_p' (DB.lexp_ctx_cons ctx l1 Variable t1) ===================================== src/unification.ml ===================================== @@ -232,7 +232,7 @@ and unify_arrow (arrow: lexp) (lxp: lexp) ctx vs Arrow (var_kind2, _, ltype2, _, lexp2)) -> if var_kind1 = var_kind2 then (unify' ltype1 ltype2 ctx vs) - @(unify' lexp1 lexp2 + @(unify' lexp1 (srename v1 lexp2) (DB.lexp_ctx_cons ctx v1 Variable ltype1) (OL.set_shift vs)) else [(CKimpossible, ctx, arrow, lxp)] View it on GitLab: https://gitlab.com/monnier/typer/-/commit/4993afa507ca9bcea4cbf772984ca25be… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/4993afa507ca9bcea4cbf772984ca25be… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][master] * src/elab.ml (infer_and_generalize_type): Add more exceptions
by Stefan 07 Avr '20

07 Avr '20

Stefan pushed to branch master at Stefan / Typer Commits: 85d12bf5 by Stefan Monnier at 2020-04-07T22:21:39-04:00 * src/elab.ml (infer_and_generalize_type): Add more exceptions Don't generalize over the level of the final return type if it doesn't appear elsewhere. * btl/builtins.typer (Eq_cast): Give a name to the proof arg. - - - - - 2 changed files: - btl/builtins.typer - src/elab.ml Changes: ===================================== btl/builtins.typer ===================================== @@ -48,7 +48,7 @@ Eq_refl : ((x : ?t) ≡> Eq x x); % FIXME: `Eq ?x ?x` causes an error! Eq_refl = Built-in "Eq.refl"; Eq_cast : (x : ?) ≡> (y : ?) - ≡> Eq x y + ≡> (p : Eq x y) ≡> (f : ? -> ?) ≡> f x -> f y; %% FIXME: I'd like to just say: ===================================== src/elab.ml ===================================== @@ -374,6 +374,9 @@ let rec meta_to_var ids o (e : lexp) = mkVar (name, o + IMap.find id ids) else match metavar_lookup id with | MVal e -> loop (push_susp e s) + (* FIXME: The substitution applied before calling `meta_to_var` + * make it impossible for the metavar to refer to the newly + * introduced variables. *) | _ -> e in loop e @@ -1034,10 +1037,10 @@ and lexp_check_decls (ectx : elab_context) (* External context. *) and infer_and_generalize_type (ctx : elab_context) se name = let nctx = ectx_new_scope ctx in let t = infer_type se nctx name in - (* FIXME: We should not generalize over metavars which only occur on the rightmost + (* We should not generalize over metavars which only occur on the rightmost * side of arrows in type annotations (aka declarations), since there's no * way for the callee to return something of the proper type if those - * metavar's don't also occur somewhere in the arguments. + * metavars don't also occur somewhere in the arguments. * E.g. for annotations like * * x : ?; @@ -1050,16 +1053,21 @@ and infer_and_generalize_type (ctx : elab_context) se name = * * since there can't be corresponding definitions. So replace the final * return type with some arbitrary closed constant before computing the - * set of free metavars. *) - 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 we can use `x : ?` to declare that - * `x` will be defined later without specifying its type yet. *) - | Metavar _ -> t - | _ -> let g = generalize nctx t in - g (fun _ne name t l e - -> mkArrow (Aerasable, name, t, l, e)) - t + * set of free metavars. + * The same argument holds for other *positive* positions, e.g. + * + * f : (? -> Int) -> Int; + * + * But we don't bother trying to catch all cases currently. + *) + let rec strip_rettype t = match t with + | Arrow (ak, v, t1, l, t2) -> Arrow (ak, v, t1, l, strip_rettype t2) + | Sort _ | Metavar _ -> type0 (* Abritrary closed constant. *) + | _ -> t in + let g = generalize nctx (strip_rettype t) in + g (fun _ne name t l e + -> mkArrow (Aerasable, name, t, l, e)) + t and infer_and_generalize_def (ctx : elab_context) se = let nctx = ectx_new_scope ctx in View it on GitLab: https://gitlab.com/monnier/typer/-/commit/85d12bf59e470f20c8d866a33029c9f3c… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/85d12bf59e470f20c8d866a33029c9f3c… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][master] * src/elab.ml (meta_to_var): Fix debruijn error.
by Stefan 02 Avr '20

02 Avr '20

Stefan pushed to branch master at Stefan / Typer Commits: f2b81386 by Stefan Monnier at 2020-04-02T19:31:41-04:00 * src/elab.ml (meta_to_var): Fix debruijn error. * btl/pervasive.typer (Decidable): Make it universe-polymorphic. * src/builtin.ml (register_builtin_csts): Fix Type0 typo. - - - - - 3 changed files: - btl/pervasive.typer - src/builtin.ml - src/elab.ml Changes: ===================================== btl/pervasive.typer ===================================== @@ -446,7 +446,7 @@ Not prop = prop -> False; %% We don't use the `type` macro here because it would make these `true` %% and `false` constructors override `Bool`'s, and we currently don't %% want that. -Decidable = typecons (Decidable (prop : Type)) +Decidable = typecons (Decidable (prop : Type_ ?ℓ)) (true (p ::: prop)) (false (p ::: Not prop)); %% Testing generalization in inductive type constructors. ===================================== src/builtin.ml ===================================== @@ -155,7 +155,7 @@ let register_builtin_csts () = add_builtin_cst "TypeLevel" DB.type_level; add_builtin_cst "TypeLevel_z" DB.level0; add_builtin_cst "Type" DB.type0; - add_builtin_cst "Type0" DB.type1; + add_builtin_cst "Type0" DB.type0; add_builtin_cst "Type1" DB.type1; add_builtin_cst "Int" DB.type_int; add_builtin_cst "Integer" DB.type_integer; ===================================== src/elab.ml ===================================== @@ -356,7 +356,7 @@ let rec meta_to_var ids o (e : lexp) = -> let o' = o' - 1 in (o', (ak, v, meta_to_var ids (o' + o) t) :: fields)) - fields (flen, []) in + fields (flen + alen, []) in nfields) cases in mkInductive (l, label, nargs, ncases) View it on GitLab: https://gitlab.com/monnier/typer/-/commit/f2b81386a4aa31b49e0fd7e00ea7aea74… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/f2b81386a4aa31b49e0fd7e00ea7aea74… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][master] Misc tweaks; use a bit more universe polymorphism; improve some errors
by Stefan 02 Avr '20

02 Avr '20

Stefan pushed to branch master at Stefan / Typer Commits: 56ed1196 by Stefan Monnier at 2020-04-02T17:04:44-04:00 Misc tweaks; use a bit more universe polymorphism; improve some errors * btl/builtins.typer: Make better use of generalization to avoid `≡`. (List): * btl/pervasive.typer (Option, Not): Make them universe-polymorphic. * src/builtin.ml (register_builtin_csts): Add name `Type0`. * src/debruijn.ml (type_level_sort): Rename from `sort_level`. * src/elab.ml (check_inferred): Give more complete error info. (infer_level): Use `newMetalevel`. * src/lexp.ml (lexp_head): New function. (mkSLlub', lexp_name): Use it. (lexp_unparse, lexp_print): Fix printout of `type_level_sort`. * tests/eval_test.ml ("has-attribute", "Implicit Arguments"): Disable tests. - - - - - 8 changed files: - btl/builtins.typer - btl/pervasive.typer - src/builtin.ml - src/debruijn.ml - src/elab.ml - src/lexp.ml - src/opslexp.ml - tests/eval_test.ml Changes: ===================================== btl/builtins.typer ===================================== @@ -172,11 +172,11 @@ Sexp_debug_print = Built-in "Sexp.debug_print" : Sexp -> IO Sexp; %% ----------------------------------------------------- %% FIXME: "List : ?" should be sufficient but triggers -List : Type -> Type; +List : Type_ ?ℓ -> Type_ ?ℓ; %% List a = typecons List (nil) (cons a (List a)); %% nil = lambda a ≡> datacons (List a) nil; %% cons = lambda a ≡> datacons (List a) cons; -List = typecons (List (a : Type)) (nil) (cons a (List a)); +List = typecons (List (ℓ ::: TypeLevel) (a : Type_ ℓ)) (nil) (cons a (List a)); nil = datacons List nil; cons = datacons List cons; @@ -197,16 +197,15 @@ Macro_expand : Macro -> List Sexp -> IO Sexp; Macro_expand = lambda m -> lambda args -> case m | macro f => f args; -Sexp_dispatch = Built-in "Sexp.dispatch" - : (a : Type) ≡> - Sexp - -> (node : Sexp -> List Sexp -> a) - -> (symbol : String -> a) - -> (string : String -> a) - -> (int : Integer -> a) - -> (float : Float -> a) - -> (block : Sexp -> a) - -> a ; +Sexp_dispatch : Sexp + -> (node : Sexp -> List Sexp -> ?a) + -> (symbol : String -> ?a) + -> (string : String -> ?a) + -> (int : Integer -> ?a) + -> (float : Float -> ?a) + -> (block : Sexp -> ?a) + -> ?a ; +Sexp_dispatch = Built-in "Sexp.dispatch"; %% %% Parse a block using the grammar in the passed context @@ -222,7 +221,8 @@ Reader_parse = Built-in "Reader.parse" : Elab_Context -> Sexp -> List Sexp; %% %% Array_set is in O(N) where N is the length %% -Array_set = Built-in "Array.set" : (a : Type) ≡> Int -> a -> Array a -> Array a; +Array_set : Int -> ?a -> Array ?a -> Array ?a; +Array_set = Built-in "Array.set"; %% %% Takes an element and an array @@ -230,43 +230,47 @@ Array_set = Built-in "Array.set" : (a : Type) ≡> Int -> a -> Array a -> %% %% Array_append is in O(N) where N is the length %% -Array_append = Built-in "Array.append" : (a : Type) ≡> a -> Array a -> Array a; +Array_append : ?a -> Array ?a -> Array ?a; +Array_append = Built-in "Array.append"; %% %% Takes an Int (n) and a value %% Returns an array containing n times the value %% -Array_create = Built-in "Array.create" : (a : Type) ≡> Int -> a -> Array a; +Array_create : Int -> ?a -> Array ?a; +Array_create = Built-in "Array.create"; %% %% Takes an array %% Returns the number of element in the array %% -Array_length = Built-in "Array.length" : (a : Type) ≡> Array a -> Int; +Array_length : Array ?a -> Int; +Array_length = Built-in "Array.length"; %% %% Takes a default value, an index and an array %% Returns the value in the array at the specified index or %% the default value if the index is out of bounds %% -Array_get = Built-in "Array.get" : (a : Type) ≡> a -> Int -> Array a -> a; +Array_get : ?a -> Int -> Array ?a -> ?a; +Array_get = Built-in "Array.get"; %% %% It returns an empty array %% %% let Typer deduce the value of (a : Type) %% -Array_empty = Built-in "Array.empty" : (a : Type) ≡> Unit -> Array a; +Array_empty : Unit -> Array ?a; +Array_empty = Built-in "Array.empty"; %%%% Monads %% Builtin bind -IO_bind = Built-in "IO.bind" - : (a : Type) ≡> - (b : Type) ≡> - IO a -> (a -> IO b) -> (IO b); +IO_bind : IO ?a -> (?a -> IO ?b) -> IO ?b; +IO_bind = Built-in "IO.bind"; -IO_return = Built-in "IO.return" : (a : Type) ≡> a -> IO a; +IO_return : ?a -> IO ?a; +IO_return = Built-in "IO.return"; %% `runIO` should have type IO Unit -> b -> b %% or IO a -> b -> b, which means "run the IO, throw away the result, @@ -274,7 +278,8 @@ IO_return = Built-in "IO.return" : (a : Type) ≡> a -> IO a; %% is actually crucial to make sure the result of runIO is used, otherwise %% the whole call would look like a dead function call and could be %% optimized away! -IO_run = Built-in "IO.run" : (a : Type) ≡> IO Unit -> a -> a; +IO_run : IO Unit -> ?a -> ?a; +IO_run = Built-in "IO.run"; %% File monad @@ -300,20 +305,23 @@ Sys_exit = Built-in "Sys.exit" : Int -> IO Unit; %% Returns a value modifiable in the IO monad %% and which already contain the specified value %% -Ref_make = Built-in "Ref.make" : (a : Type) ≡> a -> IO (Ref a); +Ref_make : ?a -> IO (Ref ?a); +Ref_make = Built-in "Ref.make"; %% %% Takes a Ref %% Returns in the IO monad the value in the Ref %% -Ref_read = Built-in "Ref.read" : (a : Type) ≡> Ref a -> IO a; +Ref_read : Ref ?a -> IO ?a; +Ref_read = Built-in "Ref.read"; %% %% Takes a value and a Ref %% Returns the an empty command %% and set the Ref to contain specified value %% -Ref_write = Built-in "Ref.write" : (a : Type) ≡> a -> Ref a -> IO Unit; +Ref_write : ?a -> Ref ?a -> IO Unit; +Ref_write = Built-in "Ref.write"; %% %% gensym for macro @@ -431,12 +439,14 @@ Test_false = Built-in "Test.false" : String -> Bool -> IO Bool; %% Takes a message and two arbitrary value of the same type %% Returns true when the two value are equal %% -Test_eq = Built-in "Test.eq" : (a : Type) ≡> String -> a -> a -> IO Bool; +Test_eq : String -> ?a -> ?a -> IO Bool; +Test_eq = Built-in "Test.eq"; %% %% Takes a message and two arbitrary value of the same type %% Returns true when the two value are not equal %% -Test_neq = Built-in "Test.neq" : (a : Type) ≡> String -> a -> a -> IO Bool; +Test_neq : String -> ?a -> ?a -> IO Bool; +Test_neq = Built-in "Test.neq"; %%% builtins.typer ends here. ===================================== btl/pervasive.typer ===================================== @@ -32,7 +32,7 @@ %%%% `Option` type -Option = typecons (Option (a : Type)) (none) (some a); +Option = typecons (Option (ℓ ::: TypeLevel) (a : Type_ ℓ)) (none) (some a); some = datacons Option some; none = datacons Option none; @@ -334,6 +334,7 @@ type-impl = lambda (x : List Sexp) -> type-decl = quote ((uquote (get-name name)) : (uquote ( (List_foldl (lambda args arg -> Sexp_node (Sexp_symbol "_->_") (cons (get-type arg) (cons args nil))) + %% FIXME: Don't hardcode TypeLevel.z! (Sexp_symbol "Type") (List_reverse (get-args name) nil)) ))); @@ -439,18 +440,17 @@ in List_map mf xs; False = Void; True = Unit; -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 +%% and `false` constructors override `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! +LList : Type -> Int -> Type; %FIXME: `LList : ?` should be sufficient! type LList (a : Type) (n : Int) | vnil (p ::: Eq n 0) | vcons a (LList a ?n1) (p ::: Eq n (?n1 + 1)); %FIXME: Unsound wraparound! ===================================== src/builtin.ml ===================================== @@ -155,6 +155,7 @@ let register_builtin_csts () = add_builtin_cst "TypeLevel" DB.type_level; add_builtin_cst "TypeLevel_z" DB.level0; add_builtin_cst "Type" DB.type0; + add_builtin_cst "Type0" DB.type1; add_builtin_cst "Type1" DB.type1; add_builtin_cst "Int" DB.type_int; add_builtin_cst "Integer" DB.type_integer; ===================================== src/debruijn.ml ===================================== @@ -80,9 +80,9 @@ let fatal = Log.log_fatal ~section:"DEBRUIJN" * ---------------------------------- *) let dloc = dummy_location -let sort_level = mkSort (dloc, StypeLevel) +let type_level_sort = mkSort (dloc, StypeLevel) let sort_omega = mkSort (dloc, StypeOmega) -let type_level = mkBuiltin ((dloc, "TypeLevel"), sort_level, None) +let type_level = mkBuiltin ((dloc, "TypeLevel"), type_level_sort, None) let level0 = mkSortLevel SLz let level1 = mkSortLevel (mkSLsucc level0) let level2 = mkSortLevel (mkSLsucc level1) ===================================== src/elab.ml ===================================== @@ -602,11 +602,18 @@ and check_inferred ctx e inferred_t t = -> (e, inferred_t) | _ -> instantiate_implicit e inferred_t ctx in (match Unif.unify inferred_t t (ectx_to_lctx ctx) with - | ((_ck, _ctx, t1, t2)::_) + | ((ck, _ctx, t1, t2)::_) -> lexp_error (lexp_location e) e - ("Type mismatch! Context expected `" - ^ lexp_string t2 ^ "` but expression has type `" - ^ lexp_string t1 ^ "`") + ("Type mismatch(" + ^ (match ck with | Unif.CKimpossible -> "impossible" + | Unif.CKresidual -> "residue") + ^ ")! Context expected:\n " + ^ lexp_string t ^ "\nbut expression has type:\n " + ^ lexp_string inferred_t ^ "\ncan't unify:\n " + ^ lexp_string t1 + ^ "\nwith:\n " + ^ lexp_string t2); + assert (not (OL.conv_p (ectx_to_lctx ctx) inferred_t t)) | [] -> ()); e @@ -993,8 +1000,9 @@ and lexp_decls_macro (loc, mname) sargs ctx: sexp = (* Elaborate a bunch of mutually-recursive definitions. * FIXME: Currently, we never apply generalization to recursive definitions, - * which means we can't define `List_length` or `List_map` without adding - * explicit type annotations :-( *) + * which can leave "bogus" metavariables in the term (and it also means we + * can't define `List_length` or `List_map` without adding explicit type + * annotations :-( ). *) and lexp_check_decls (ectx : elab_context) (* External context. *) (nctx : elab_context) (* Context with type declarations. *) (defs : (symbol * sexp) list) @@ -1026,6 +1034,23 @@ and lexp_check_decls (ectx : elab_context) (* External context. *) and infer_and_generalize_type (ctx : elab_context) se name = let nctx = ectx_new_scope ctx in let t = infer_type se nctx name in + (* FIXME: We should not generalize over metavars which only occur on the rightmost + * side of arrows in type annotations (aka declarations), since there's no + * way for the callee to return something of the proper type if those + * metavar's don't also occur somewhere in the arguments. + * E.g. for annotations like + * + * x : ?; + * F : Type ? → Type ?; + * + * it makes no sense to generalize them to: + * + * x : (ℓ : TypeLevel) ≡> (t : Type ℓ) ≡> t; + * F : (ℓ₁ : TypeLevel) ≡> (ℓ₂ : TypeLevel) ≡> Type ℓ₁ → Type ℓ₂; + * + * since there can't be corresponding definitions. So replace the final + * return type with some arbitrary closed constant before computing the + * set of free metavars. *) 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 we can use `x : ?` to declare that @@ -1431,7 +1456,7 @@ let sform_identifier ctx loc sargs ot = * This is used so that in cases like "lambda t (y : ?) ... " * type inference can guess ? without having to wonder whether it * can refer to `t` or not. If the user wants ? to be able to refer - * to `t`, then she should explicitly write (y : ? t). *) + * to `t`, then they should explicitly write (y : ? t). *) let ctx_shift = ectx_local_scope_size ctx in let octx = Myers.nthcdr ctx_shift (ectx_to_lctx ctx) in let sl = ectx_to_scope_level ctx in @@ -1581,7 +1606,7 @@ let rec infer_level ctx se : lexp = -> OL.mkSLlub (ectx_to_lctx ctx) (infer_level ctx se1) (infer_level ctx se2) | _ -> let l = (sexp_location se) in (sexp_error l ("Unrecognized TypeLevel: " ^ sexp_string se); - newMetavar (ectx_to_lctx ctx) dummy_scope_level (l, None) type_level) + newMetalevel (ectx_to_lctx ctx) (ectx_to_scope_level ctx) l) (* Actually `Type_` could also be defined as a plain constant * Lambda("l", TypeLevel, Sort (Stype (Var "l"))) ===================================== src/lexp.ml ===================================== @@ -1,6 +1,6 @@ (* lexp.ml --- Lambda-expressions: the core language. -Copyright (C) 2011-2019 Free Software Foundation, Inc. +Copyright (C) 2011-2020 Free Software Foundation, Inc. Author: Stefan Monnier <monnier(a)iro.umontreal.ca> Keywords: languages, lisp, dependent types. @@ -204,6 +204,24 @@ let mkCall (f, es) | _, [] -> f | _ -> hc (Call (f, es)) +and lexp_head e = + match e with + | Imm s -> if e = impossible then "impossible" else "Imm" ^ sexp_string s + | Var _ -> "Var" + | Let _ -> "let" + | Arrow _ -> "Arrow" + | Lambda _ -> "lambda" + | Call _ -> "Call" + | Cons _ -> "datacons" + | Case _ -> "case" + | Inductive _ -> "typecons" + | Susp _ -> "Susp" + | Builtin (_, _, None) -> "Builtin" + | Builtin _ -> "AttributeTable" + | Metavar _ -> "Metavar" + | Sort _ -> "Sort" + | SortLevel _ -> "SortLevel" + let mkSLlub' (e1, e2) = match (e1, e2) with (* FIXME: This first case should be handled by calling `mkSLlub` instead! *) | (SortLevel SLz, SortLevel l) | (SortLevel l, SortLevel SLz) -> l @@ -214,7 +232,8 @@ let mkSLlub' (e1, e2) = match (e1, e2) with | ((SortLevel _ | Var _ | Metavar _ | Susp _), (SortLevel _ | Var _ | Metavar _ | Susp _)) -> SLlub (e1, e2) - | _ -> Log.log_fatal ~section:"internal" "SLlub of non-level" + | _ -> Log.log_fatal ~section:"internal" + ("SLlub of non-level: " ^ lexp_head e1 ^ " ∪ " ^ lexp_head e2) let mkSLsucc e = match e with | SortLevel _ | Var _ | Metavar _ | Susp _ @@ -583,7 +602,7 @@ let rec lexp_unparse lxp = -> Node (Symbol (lexp_location l1, "##TypeLevel.∪"), [lexp_unparse l1; lexp_unparse l2]) | Sort (l, StypeOmega) -> Symbol (l, "##Type_ω") - | Sort (l, StypeLevel) -> Symbol (l, "##TypeLevel") + | Sort (l, StypeLevel) -> Symbol (l, "##TypeLevel.Sort") | Sort (l, Stype sl) -> Node (Symbol (lexp_location sl, "##Type_"), [lexp_unparse sl]) @@ -601,19 +620,7 @@ and lexp_name e = match e with | Imm _ -> lexp_string e | Var _ -> lexp_string e - | Let _ -> "let" - | Arrow _ -> "Arrow" - | Lambda _ -> "lambda" - | Call _ -> "Call" - | Cons _ -> "datacons" - | Case _ -> "case" - | Inductive _ -> "typecons" - | Susp _ -> "Susp" - | Builtin (_, _, None) -> "Builtin" - | Builtin _ -> "AttributeTable" - | Metavar _ -> "Metavar" - | Sort _ -> "Sort" - | SortLevel _ -> "SortLevel" + | _ -> lexp_head e (* ------------------------------------------------------------------------- *) (* Printing *) @@ -905,7 +912,7 @@ and lexp_str ctx (exp : lexp) : string = | Sort (_, Stype (SortLevel SLz)) -> "##Type" | Sort (_, Stype (SortLevel (SLsucc (SortLevel SLz)))) -> "##Type1" | Sort (_, Stype l) -> "(##Type_ " ^ lexp_string l ^ ")" - | Sort (_, StypeLevel) -> "##TypeLevel" + | Sort (_, StypeLevel) -> "##TypeLevel.Sort" | Sort (_, StypeOmega) -> "##Type_ω" | SortLevel (SLz) -> "##TypeLevel.z" ===================================== src/opslexp.ml ===================================== @@ -556,6 +556,8 @@ let rec check'' erased ctx e = -> mkSLlub ctx level (* We need to unshift because the final type * cannot refer to the fields! *) + (* FIXME: If it does refer, + * we get an ugly error! *) (mkSusp level' (L.sunshift n)) | tt -> error_tc ~loc:(lexp_location t) ~print_action:(fun _ -> ===================================== tests/eval_test.ml ===================================== @@ -3,7 +3,7 @@ * * --------------------------------------------------------------------------- * - * Copyright (C) 2011-2018 Free Software Foundation, Inc. + * Copyright (C) 2011-2020 Free Software Foundation, Inc. * * Author: Pierre Delaunay <pierre.delaunay(a)hec.ca> * Keywords: languages, lisp, dependent types. @@ -276,20 +276,20 @@ let _ = test_eval_eqv_named let _ = test_eval_eqv "w = 2" "decltype w" "Int" let _ = test_eval_eqv "w = 2" "declexpr w" "2" -let attr_decl = " - w = 2; - greater-than = new-attribute (Int -> Int); - greater-than = add-attribute greater-than w (lambda (x : Int) -> x);" - -let _ = test_eval_eqv_named - "has-attribute" - - attr_decl - - "has-attribute greater-than w; - (get-attribute greater-than w) 3;" - - "true; 3" +(* let attr_decl = " + * w = 2; + * greater-than = new-attribute (Int -> Int); + * greater-than = add-attribute greater-than w (lambda (x : Int) -> x);" + * + * let _ = test_eval_eqv_named + * "has-attribute" + * + * attr_decl + * + * "has-attribute greater-than w; + * (get-attribute greater-than w) 3;" + * + * "true; 3" *) let _ = (add_test "EVAL" "Monads" (fun () -> @@ -350,21 +350,21 @@ let _ = test_eval_eqv_named "\"hello\"; 5.0; \"hello\"; 5.0; \"hello\"; 7" -let _ = test_eval_eqv_named - "Implicit Arguments" - - "default = new-attribute Macro; - default = add-attribute default Int (macro (lambda (lst : List Sexp) -> - (IO_return (Sexp_integer (Int->Integer 1))))); - - fun = lambda (x : Int) => - lambda (y : Int) -> - lambda (z : Int) -> x * y + z;" - - "fun 2 1; - fun 2 1" - - "3; 3" +(* let _ = test_eval_eqv_named + * "Implicit Arguments" + * + * "default = new-attribute Macro; + * default = add-attribute default Int (macro (lambda (lst : List Sexp) -> + * (IO_return (Sexp_integer (Int->Integer 1))))); + * + * fun = lambda (x : Int) => + * lambda (y : Int) -> + * lambda (z : Int) -> x * y + z;" + * + * "fun 2 1; + * fun 2 1" + * + * "3; 3" *) let _ = test_eval_eqv_named "Equalities" View it on GitLab: https://gitlab.com/monnier/typer/-/commit/56ed11967bf3b8160aaef90c3da5b996e… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/56ed11967bf3b8160aaef90c3da5b996e… You're receiving this email because of your account on gitlab.com.

1 0

2024

2023

2022

2021

2020

2019

2018

2017

2016

Typer Avril 2020