Typer Septembre 2019

typer@iro.umontreal.ca

2 participants
5 discussions

[Git][monnier/typer][simon-genier] 2 commits: Add eliminators for Pair in pervasive.typer.
by Simon Génier 29 Sep '19

29 Sep '19

Simon Génier pushed to branch simon-genier at Stefan / Typer Commits: 03f6a3b2 by Simon Génier at 2019-09-25T21:23:14Z Add eliminators for Pair in pervasive.typer. - - - - - a8096766 by Simon Génier at 2019-09-25T21:23:42Z Add datacons' for Decidable. - - - - - 1 changed file: - btl/pervasive.typer Changes: ===================================== btl/pervasive.typer ===================================== @@ -386,6 +386,12 @@ BoolMod = (##datacons Pair = typecons (Pair (a : Type) (b : Type)) (pair (fst : a) (snd : b)); pair = datacons Pair pair; +fst : (a : Type) ≡> (b : Type) ≡> Pair a b -> a; +fst p = case p | pair l _ => l; + +snd : (a : Type) ≡> (b : Type) ≡> Pair a b -> b; +snd p = case p | pair _ r => r; + __\.__ = let mksel o f = let constructor = Sexp_node (Sexp_symbol "##datacons") @@ -452,11 +458,10 @@ Not : Type -> Type; Not prop = prop -> False; %% Like Bool, except that it additionally carries the meaning of its value. -%% We don't use the `type` macro here because it would make these `true` -%% and `false` constructors ovrride `Bool`'s, and we currently don't -%% want that. -Decidable = typecons (Decidable (prop : Type)) - (true (p ::: prop)) (false (p ::: Not prop)); +type Decidable (prop : Type) + | yes (p ::: prop) + | no (p ::: Not prop) +; %% Testing generalization in inductive type constructors. LList : (a : Type) -> Int -> Type; %FIXME: `LList : ?` should be sufficient! View it on GitLab: https://gitlab.com/monnier/typer/compare/f64ab3da85ca3d8b8d8d7aa7cb2b75d37f… -- View it on GitLab: https://gitlab.com/monnier/typer/compare/f64ab3da85ca3d8b8d8d7aa7cb2b75d37f… You're receiving this email because of your account on gitlab.com.

2 1

[Git][monnier/typer][master] 2 commits: * lexp.ml (lexp): Typo
by Stefan 26 Sep '19

26 Sep '19

Stefan pushed to branch master at Stefan / Typer Commits: 25bb77ab by Stefan Monnier at 2019-09-26T20:51:26Z * lexp.ml (lexp): Typo - - - - - 5c7f8365 by Stefan Monnier at 2019-09-26T20:52:00Z Merge remote-tracking branch 'refs/remotes/gitlab/master' into trunk - - - - - 1 changed file: - src/lexp.ml Changes: ===================================== src/lexp.ml ===================================== @@ -69,7 +69,7 @@ type ltype = lexp | Susp of lexp * subst (* Lazy explicit substitution: e[σ]. *) (* This "Let" allows recursion. *) | Let of U.location * (vname * lexp * ltype) list * lexp - | Arrow of arg_kind * vname * ltype * U.location * lexp + | Arrow of arg_kind * vname * ltype * U.location * ltype | Lambda of arg_kind * vname * ltype * lexp | Call of lexp * (arg_kind * lexp) list (* Curried call. *) | Inductive of U.location * label View it on GitLab: https://gitlab.com/monnier/typer/compare/cf67844d6bda8effdde3e31e08b5cd7396… -- View it on GitLab: https://gitlab.com/monnier/typer/compare/cf67844d6bda8effdde3e31e08b5cd7396… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer] Pushed new branch simon-genier
by Simon Génier 25 Sep '19

25 Sep '19

Simon Génier pushed new branch simon-genier at Stefan / Typer -- View it on GitLab: https://gitlab.com/monnier/typer/tree/simon-genier You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][master] First tweak to try and handle parameterized inductives
by Stefan 13 Sep '19

13 Sep '19

Stefan pushed to branch master at Stefan / Typer Commits: cf67844d by Stefan Monnier at 2019-09-13T21:06:03Z First tweak to try and handle parameterized inductives * src/elab.ml (check_case.add_branch): Try and handle parameterized constructors. (elab_check_def): Slightly improve message. * src/unification.ml (unify_inductive): New function. (unify'): Use it. - - - - - 3 changed files: - src/elab.ml - src/lexp.ml - src/unification.ml Changes: ===================================== src/elab.ml ===================================== @@ -171,7 +171,8 @@ let elab_check_def (ctx : elab_context) var lxp ltype = elab_check_proper_type ctx ltype var else (EV.debug_messages fatal loc "Type check error: ¡¡ctx_define error!!" [ - lexp_string lxp ^ " !: " ^ lexp_string ltype; + (match var with (_, Some n) -> n | _ -> "<anon>") + ^ " = " ^ lexp_string lxp ^ " !: " ^ lexp_string ltype; " because"; lexp_string ltype' ^ " != " ^ lexp_string ltype]) @@ -650,7 +651,15 @@ and check_case rtype (loc, target, ppatterns) ctx = let add_branch pctor pargs = let loc = sexp_location pctor in let lctor, ct = infer pctor ctx in - match OL.lexp_whnf lctor (ectx_to_lctx ctx) with + let rec inst_args ctx e = match OL.lexp_whnf e (ectx_to_lctx ctx) with + | Lambda (Aerasable, v, t, body) + -> let arg = newMetavar (ectx_to_lctx ctx) (ectx_to_scope_level ctx) + v t in + let nctx = ctx_extend ctx v Variable t in + let body = inst_args nctx body in + mkSusp body (S.substitute arg) + | e -> e in + match nosusp (inst_args ctx lctor) with | Cons (it', (_, cons_name)) -> let _ = match Unif.unify it' it (ectx_to_lctx ctx) with | (None | Some (_::_)) @@ -676,7 +685,7 @@ and check_case rtype (loc, target, ppatterns) ctx = pargs (* Pattern arguments. *) cargs (* Constructor arguments. *) pe (* Pending explicit pattern args. *) - acc = (* Accumulated reult. *) + acc = (* Accumulated result. *) match (pargs, cargs) with | (_, []) when not (SMap.is_empty pe) -> let pending = SMap.bindings pe in ===================================== src/lexp.ml ===================================== @@ -281,8 +281,7 @@ let rec sunshift n = else (assert (n >= 0); S.cons impossible (sunshift (n - 1))) -let _ = assert (S.identity (* Sanity check! *) - = scompose (S.shift 5) (sunshift 5)) +let _ = assert (S.identity_p (scompose (S.shift 5) (sunshift 5))) (* The quick test below seemed to indicate that about 50% of the "sink"s * are applied on top of another "sink" and hence cound be combined into ===================================== src/unification.ml ===================================== @@ -1,6 +1,6 @@ (* unification.ml --- Unification of Lexp terms -Copyright (C) 2016-2018 Free Software Foundation, Inc. +Copyright (C) 2016-2019 Free Software Foundation, Inc. Author: Vincent Bonnevalle <tiv.crb(a)gmail.com> @@ -132,14 +132,16 @@ let rec unify (e1: lexp) (e2: lexp) and unify' (e1: lexp) (e2: lexp) (ctx : DB.lexp_context) (vs : OL.set_plexp) : return_type = + if e1 == e2 then Some [] else let e1' = OL.lexp_whnf e1 ctx in let e2' = OL.lexp_whnf e2 ctx in - let changed = not (e1 == e1' && e2 == e2') in + if e1' == e2' then Some [] else + let changed = true (* not (e1 == e1' && e2 == e2') *) in if changed && OL.set_member_p vs e1' e2' then Some [] 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 _) | (Inductive _, Inductive _)) + | (Var _, Var _)) -> if OL.conv_p ctx e1' e2' then Some [] else None | (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 @@ -152,7 +154,17 @@ and unify' (e1: lexp) (e2: lexp) (* | (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' - | _ -> Some (if OL.conv_p ctx e1' e2' then [] else [(e1, e2)]) + | (Inductive (_loc1, label1, args1, consts1), + Inductive (_loc2, label2, args2, consts2)) + -> (* print_string ("Unifying inductives " + * ^ snd label1 + * ^ " and " + * ^ snd label2 + * ^ "\n"); *) + unify_inductive ctx vs' args1 args2 consts1 consts2 + | _ -> Some (if OL.conv_p ctx e1' e2' then [] + else ((* print_string "Unification failure on default\n"; *) + [(e1, e2)])) (********************************* Type specific unify *******************************) @@ -401,6 +413,26 @@ and is_same arglist arglist2 = * | None -> test e subst) * ) None lst *) +and unify_inductive ctx vs args1 args2 consts1 consts2 = + let unif_formals ctx vs args1 args2 + = if not (List.length args1 == List.length args2) then (ctx, vs, None) else + List.fold_left (fun (ctx, vs, residue) ((ak1, v1, t1), (ak2, v2, t2)) + -> (DB.lexp_ctx_cons ctx v1 Variable t1, + OL.set_shift vs, + if not (ak1 == ak2) then None + else unify_and (unify' t1 t2 ctx vs) residue)) + (ctx, vs, Some []) + (List.combine args1 args2) in + let (ctx, vs, residue) = unif_formals ctx vs args1 args2 in + if not (SMap.cardinal consts1 == SMap.cardinal consts2) then None else + SMap.fold (fun cname args1 residue + -> match SMap.find cname consts2 with + | args2 -> let (_ctx, _vs, residue') + = unif_formals ctx vs args1 args2 in + unify_and residue' residue + | exception Not_found -> None) + consts1 residue + (** unify the SMap of list in Inductive *) (* and unify_induct_sub_list l1 l2 subst = * let test l1 l2 subst = View it on GitLab: https://gitlab.com/monnier/typer/commit/cf67844d6bda8effdde3e31e08b5cd73967… -- View it on GitLab: https://gitlab.com/monnier/typer/commit/cf67844d6bda8effdde3e31e08b5cd73967… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][master] Avoid using Inverse_subst in core type checking
by Stefan 13 Sep '19

13 Sep '19

Stefan pushed to branch master at Stefan / Typer Commits: e3a0fe68 by Stefan Monnier at 2019-09-13T18:31:03Z Avoid using Inverse_subst in core type checking * src/lexp.ml (mkSLlub', mkSLsucc): New constructors with sanity checks. (sunshift): New function. * src/opslexp.ml (check'', get_type): Use it instead of Inverse_subst. - - - - - 6 changed files: - src/debruijn.ml - src/elab.ml - src/inverse_subst.ml - src/lexp.ml - src/opslexp.ml - src/subst.ml Changes: ===================================== src/debruijn.ml ===================================== @@ -3,7 +3,7 @@ * * --------------------------------------------------------------------------- * - * Copyright (C) 2011-2018 Free Software Foundation, Inc. + * Copyright (C) 2011-2019 Free Software Foundation, Inc. * * Author: Pierre Delaunay <pierre.delaunay(a)hec.ca> * Keywords: languages, lisp, dependent types. @@ -85,8 +85,8 @@ let sort_level = mkSort (dloc, StypeLevel) let sort_omega = mkSort (dloc, StypeOmega) let type_level = mkBuiltin ((dloc, "TypeLevel"), sort_level, None) let level0 = mkSortLevel SLz -let level1 = mkSortLevel (SLsucc level0) -let level2 = mkSortLevel (SLsucc level1) +let level1 = mkSortLevel (mkSLsucc level0) +let level2 = mkSortLevel (mkSLsucc level1) let type0 = mkSort (dloc, Stype level0) let type1 = mkSort (dloc, Stype level1) let type2 = mkSort (dloc, Stype level2) ===================================== src/elab.ml ===================================== @@ -3,7 +3,7 @@ * * --------------------------------------------------------------------------- * - * Copyright (C) 2011-2018 Free Software Foundation, Inc. + * Copyright (C) 2011-2019 Free Software Foundation, Inc. * * Author: Pierre Delaunay <pierre.delaunay(a)hec.ca> * Keywords: languages, lisp, dependent types. @@ -297,8 +297,8 @@ let rec meta_to_var ids o (e : lexp) = let rec loop e = match e with | Imm _ -> e | SortLevel SLz -> e - | SortLevel (SLsucc e) -> mkSortLevel (SLsucc (loop e)) - | SortLevel (SLlub (e1, e2)) -> mkSortLevel (SLlub (loop e1, loop e2)) + | 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)) | Sort (_, (StypeOmega | StypeLevel)) -> e | Builtin _ -> e @@ -1526,7 +1526,7 @@ let sform_type ctx loc sargs ot = match sargs with | [l] -> let l, _ = infer l ctx in (mkSort (loc, Stype l), - Inferred (mkSort (loc, Stype (SortLevel (SLsucc l))))) + Inferred (mkSort (loc, Stype (SortLevel (mkSLsucc l))))) | _ -> sexp_error loc "##Type_ expects one argument"; sform_dummy_ret ctx loc ===================================== src/inverse_subst.ml ===================================== @@ -251,9 +251,10 @@ let rec compose_inv_subst (s' : subst) (s : subst) = match s' with and apply_inv_subst (e : lexp) (s : subst) : lexp = match e with | Imm _ -> e | SortLevel (SLz) -> e - | SortLevel (SLsucc e) -> mkSortLevel (SLsucc (apply_inv_subst e s)) + | SortLevel (SLsucc e) -> mkSortLevel (mkSLsucc (apply_inv_subst e s)) | SortLevel (SLlub (e1, e2)) - -> mkSortLevel (SLlub (apply_inv_subst e1 s, apply_inv_subst e2 s)) + (* Should we 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 | Builtin _ -> e ===================================== src/lexp.ml ===================================== @@ -205,6 +205,21 @@ let mkCall (f, es) | _, [] -> f | _ -> hc (Call (f, es)) +let mkSLlub' (e1, e2) = match (e1, e2) with + | (SortLevel SLz, _) | (_, SortLevel SLz) + -> U.msg_fatal "internal" U.dummy_location "lub of SLz" + | (SortLevel (SLsucc _), SortLevel (SLsucc _)) + -> U.msg_fatal "internal" U.dummy_location "lub of two SLsucc" + | ((SortLevel _ | Var _ | Metavar _ | Susp _), + (SortLevel _ | Var _ | Metavar _ | Susp _)) + -> SLlub (e1, e2) + | _ -> U.msg_fatal "internal" U.dummy_location "SLlub of non-level" + +let mkSLsucc e = match e with + | SortLevel _ | Var _ | Metavar _ | Susp _ + -> SLsucc e + | _ -> U.msg_fatal "internal" U.dummy_location "SLsucc of non-level" + (********* Helper functions to use the Subst operations *********) (* This basically "ties the knot" between Subst and Lexp. * Maybe it would be cleaner to just move subst.ml into lexp.ml @@ -260,6 +275,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)) +(* Shift by a negative amount! *) +let rec sunshift n = + if n = 0 then S.identity + else (assert (n >= 0); + S.cons impossible (sunshift (n - 1))) + +let _ = assert (S.identity (* Sanity check! *) + = scompose (S.shift 5) (sunshift 5)) + (* The quick test below seemed to indicate that about 50% of the "sink"s * are applied on top of another "sink" and hence cound be combined into * a single "Lift^n" constructor. Doesn't seem high enough to justify @@ -316,8 +340,9 @@ let rec push_susp e s = (* Push a suspension one level down. *) match e with | Imm _ -> e | SortLevel (SLz) -> e - | SortLevel (SLsucc e') -> mkSortLevel (SLsucc (mkSusp e' s)) - | SortLevel (SLlub (e1, e2)) -> mkSortLevel (SLlub (mkSusp e1 s, mkSusp e2 s)) + | SortLevel (SLsucc e') -> mkSortLevel (mkSLsucc (mkSusp e' s)) + | SortLevel (SLlub (e1, e2)) + -> mkSortLevel (mkSLlub' (mkSusp e1 s, mkSusp e2 s)) | Sort (l, Stype e) -> mkSort (l, Stype (mkSusp e s)) | Sort (l, _) -> e | Builtin _ -> e @@ -381,8 +406,10 @@ let clean e = let rec clean s e = match e with | Imm _ -> e | SortLevel (SLz) -> e - | SortLevel (SLsucc e) -> mkSortLevel (SLsucc (clean s e)) - | SortLevel (SLlub (e1, e2)) -> mkSortLevel (SLlub (clean s e1, clean s e2)) + | SortLevel (SLsucc e) -> mkSortLevel (mkSLsucc (clean s e)) + | SortLevel (SLlub (e1, e2)) + (* FIXME: The new SLlub could have `succ` on both sides! *) + -> mkSortLevel (mkSLlub' (clean s e1, clean s e2)) | Sort (l, Stype e) -> mkSort (l, Stype (clean s e)) | Sort (l, _) -> e | Builtin _ -> e ===================================== src/opslexp.ml ===================================== @@ -332,7 +332,7 @@ let rec mkSLlub ctx e1 e2 = let ce2 = level_canon (L.clean e2') in if level_leq ce1 ce2 then e1 else if level_leq ce2 ce1 then e2 - else mkSortLevel (SLlub (e1, e2)) + else mkSortLevel (mkSLlub' (e1, e2)) (* FIXME: Could be more canonical *) type sort_compose_result = SortResult of ltype @@ -535,10 +535,9 @@ let rec check'' erased ctx e = -> level | Sort (_, Stype level') -> mkSLlub ctx level - (* FIXME: We shouldn't use Inverse_subst - * in the plain `check` code! *) - (Inverse_subst.apply_inv_subst level' - (S.shift n)) + (* We need to unshift because the final type + * cannot refer to the fields! *) + (mkSusp level' (L.sunshift n)) | tt -> U.msg_error "TC" (lexp_location t) ("Field type " ^ lexp_string t @@ -789,7 +788,7 @@ let rec get_type ctx e = | Imm (Block (_, _, _) | Symbol _ | Node (_, _)) -> DB.type_int | Builtin (_, t, _) -> t | SortLevel _ -> DB.type_level - | Sort (l, Stype e) -> mkSort (l, Stype (mkSortLevel (SLsucc e))) + | Sort (l, Stype e) -> mkSort (l, Stype (mkSortLevel (mkSLsucc e))) | Sort (_, StypeLevel) -> DB.sort_omega | Sort (_, StypeOmega) -> DB.sort_omega | Var (((_, name), idx) as v) -> lookup_type ctx v @@ -835,9 +834,9 @@ let rec get_type ctx e = -> level | Sort (_, Stype level') -> mkSLlub ctx level - (try Inverse_subst.apply_inv_subst level' - (S.shift n) - with _ -> level) + (* We need to unshift because the final type + * cannot refer to the fields! *) + (mkSusp level' (L.sunshift n)) | tt -> level), DB.lctx_extend ictx v Variable t, n + 1)) ===================================== src/subst.ml ===================================== @@ -159,7 +159,7 @@ let mkShift s (m:db_offset) = * context ΔₛΔₜ where Δₜ has size M. *) let shift (m:db_offset) = Identity m -(* Return a substitution which replaces #0 with `e` and the applies `s` +(* Return a substitution which replaces #0 with `e` and then applies `s` * to the rest. *) let cons e s = Cons (e, s, 0) View it on GitLab: https://gitlab.com/monnier/typer/commit/e3a0fe68c47c151f0041137b33061a51e79… -- View it on GitLab: https://gitlab.com/monnier/typer/commit/e3a0fe68c47c151f0041137b33061a51e79… You're receiving this email because of your account on gitlab.com.

1 0

2024

2023

2022

2021

2020

2019

2018

2017

2016

Typer Septembre 2019