Typer Mars 2020

typer@iro.umontreal.ca

1 participants
7 discussions

[Git][monnier/typer][master] Infer type of `case` target from patterns
by Stefan 27 Mar '20

27 Mar '20

Stefan pushed to branch master at Stefan / Typer Commits: 402bdbe0 by Stefan Monnier at 2020-03-27T16:04:24-04:00 Infer type of `case` target from patterns * src/elab.ml (check_case): Infer the type of the target from the patterns when applicable. * src/opslexp.ml (check''): Be careful to always pass the inferred type and the expected type in the same order. * src/unification.ml (create_metavar_1): New function extracted from create_metavar. (create_metavar): Use it. (common_subset, s_offset): New functions. (unify_metavar): Use them to properly handle the case of unifying a metavar with itself where the two substitutions are different. * btl/builtins.typer (Eq_comm): Simplify type annotation a bit. * btl/pervasive.typer (List_head1, List_head, List_tail, List_concat) (I, List_map-fst, List_map-snd): Remove unnecessary type annotation. - - - - - 6 changed files: - btl/builtins.typer - btl/pervasive.typer - samples/hott.typer - src/elab.ml - src/opslexp.ml - src/unification.ml Changes: ===================================== btl/builtins.typer ===================================== @@ -1,6 +1,6 @@ %%% builtins.typer --- Initialize the builtin functions -%% 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. @@ -48,18 +48,18 @@ Eq_refl : ((x : ?t) ≡> Eq x x); % FIXME: `Eq ?x ?x` causes an error! Eq_refl = Built-in "Eq.refl"; Eq_cast : (x : ?) ≡> (y : ?) - ≡> (p : Eq x y) + ≡> Eq x y ≡> (f : ? -> ?) ≡> f x -> f y; %% FIXME: I'd like to just say: -%% Eq_cast : (p : Eq ?x ?y) ≡> ?f ?x -> ?f ?y; +%% Eq_cast : Eq ?x ?y ≡> ?f ?x -> ?f ?y; Eq_cast = Built-in "Eq.cast"; %% Commutativity of equality! %% FIXME: I'd like to just say: -%% Eq_comm : (p : Eq ?x ?y) -> Eq ?y ?x`; -Eq_comm : (x : ?t) ≡> (y : ?t) ≡> (p : Eq x y) -> Eq (t := ?t) y x; -Eq_comm p = Eq_cast (f := lambda xy -> Eq (t := t) xy x) +%% Eq_comm : Eq ?x ?y -> Eq ?y ?x`; +Eq_comm : (x : ?t) ≡> (y : ?t) ≡> Eq x y -> Eq y x; +Eq_comm p = Eq_cast (f := lambda xy -> Eq xy x) %% FIXME: I can't figure out how `(p := p)` %% gets inferred here, yet it seems to work!?! Eq_refl; ===================================== btl/pervasive.typer ===================================== @@ -1,6 +1,6 @@ %%% pervasive --- Always available definitions -%% 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. @@ -38,7 +38,7 @@ none = datacons Option none; %%%% List functions -List_length : List ?a -> Int; +List_length : List ?a -> Int; % Recursive defs aren't generalized :-( List_length xs = case xs | nil => 0 | cons hd tl => @@ -49,18 +49,15 @@ List_length xs = case xs %% - Provide a default value : `a -> List a -> a`; %% - Disallow problem case : `(l : List a) -> (l != nil) -> a`; %% - Return an Option/Error -List_head1 : List ?a -> Option ?a; -List_head1 : (a : Type) ≡> List a -> Option a; List_head1 xs = case xs | nil => none | cons hd tl => some hd; -List_head x = lambda xs -> case (xs : List ?a) - %% FIXME: We shouldn't need to annotate `xs` above! +List_head x = lambda xs -> case xs | cons x _ => x | nil => x; -List_tail xs = case (xs : List ?a) % FIXME: Same here. +List_tail xs = case xs | nil => nil | cons hd tl => tl; @@ -146,7 +143,6 @@ List_reverse l t = case l | nil => t | cons hd tl => List_reverse tl (cons hd t); -List_concat : List ?a -> List ?a -> List ?a; List_concat l t = List_reverse (List_reverse l nil) t; List_foldl : (?a -> ?b -> ?a) -> ?a -> List ?b -> ?a; @@ -183,7 +179,6 @@ List_empty xs = Int_eq (List_length xs) 0; %%% Good 'ol combinators -I : ?a -> ?a; I x = x; %% Use explicit erasable annotations since with an annotation like @@ -429,15 +424,11 @@ List_merge xs ys = case xs %% `Unmerge` a List of Pair %% The two functions name said it all -List_map-fst : List (Pair ?a ?b) -> List ?a; List_map-fst xs = let - mf : Pair ?a ?b -> ?a; mf p = case p | pair x _ => x; in List_map mf xs; -List_map-snd : List (Pair ?a ?b) -> List ?b; List_map-snd xs = let - mf : Pair ?a ?b -> ?b; mf p = case p | pair _ y => y; in List_map mf xs; ===================================== samples/hott.typer ===================================== @@ -106,6 +106,9 @@ Equiv_function f (g : (x : ?A) -> ?B) = ((x : ?A) -> Eq (f x) (g x)); %% similarly restrict the univalent universes so they're always erased %% before runtime (so we don't need to have the non-nop form of "cast" %% at run-time). +%% This can be thought of as adding a new equality to some universes, +%% aka making a "quotient universe", which, like HIT, requires proving +%% that every time we use types from this universe we obey those equalities. %%%% Propositions, resizing, etc... ===================================== src/elab.ml ===================================== @@ -240,7 +240,7 @@ let ctx_define_rec (ctx: elab_context) decls = * infer the types and perform macro-expansion. * * More specifically, we do it with 2 mutually recursive functions: - * - `check` takes a Pexp along with its expected type and return an Lexp + * - `check` takes a Pexp along with its expected type and returns an Lexp * of that type (hopefully) * - `infer` takes a Pexp and infers its type (which it returns along with * the Lexp). @@ -251,8 +251,8 @@ let ctx_define_rec (ctx: elab_context) decls = * metavars we create/instantiate/dereference as well as the number of call to * the unification algorithm. * Basically guessing/annotations is only needed at those few places where the - * code is not fully-normalized, which in normal programs is only in "let" - * definitions. + * code is not fully-normalized (which in normal programs is only in "let" + * definitions) as well as when we fill implicit arguments. *) let newMetavar (ctx : lexp_context) sl name t = @@ -462,8 +462,8 @@ let rec elaborate ctx se ot = * elaborate ctx (Node (Symbol (l, "typer-funcall"), func::args)) ot * but that forces `typer-funcall` to elaborate `func` a second time! * Maybe I should only elaborate `func` above if it's a symbol - * (and maybe even use `elaborate_varref` rather than indirecting - * through `typr-identifier`)? *) + * (and maybe even use `elab_varref` rather than indirecting + * through `typer-identifier`)? *) elab_call ctx ft args and infer (p : sexp) (ctx : elab_context): lexp * ltype = @@ -626,24 +626,49 @@ and check_case rtype (loc, target, ppatterns) ctx = (* get target and its type *) let tlxp, tltp = infer target ctx in - (* FIXME: We need to be careful with whnf: while the output is "equivalent" - * to the input, it's not necessarily as readable/efficient. - * So try to reuse the "non-whnf" form whenever possible. *) - let call_split e = match (OL.lexp_whnf e (ectx_to_lctx ctx)) with - | Call (f, args) -> (f, args) - | _ -> (e,[]) in - let it, targs = call_split tltp in - let constructors = match OL.lexp_whnf it (ectx_to_lctx ctx) with - (* FIXME: Check that it's `Inductive' only after performing Unif.unify - * with the various branches, so that we can infer the type - * of the target from the type of the patterns. *) - | Inductive (_, _, fargs, constructors) - -> assert (List.length fargs = List.length targs); - constructors - | _ -> lexp_error (sexp_location target) tlxp - ("Can't `case` on objects of this type: " - ^ lexp_string tltp); - SMap.empty in + let it_cs_as = ref None in + let ltarget = ref tlxp in + + let get_cs_as it' lctor = + match !it_cs_as with + | Some (it, cs, args) + -> let _ = match Unif.unify it' it (ectx_to_lctx ctx) with + | (_::_) + -> lexp_error loc lctor + ("Expected pattern of type `" + ^ lexp_string it ^ "` but got `" + ^ lexp_string it' ^ "`") + | [] -> () in + (cs, args) + | None + -> match OL.lexp_whnf it' (ectx_to_lctx ctx) with + | Inductive (_, _, fargs, constructors) + -> let (s, targs) = List.fold_left + (fun (s, targs) (ak, name, t) + -> let arg = newMetavar + (ectx_to_lctx ctx) + (ectx_to_scope_level ctx) + name (mkSusp t s) in + (S.cons arg s, (ak, arg) :: targs)) + (S.identity, []) + fargs in + let (cs, args) = (constructors, List.rev targs) in + ltarget := check_inferred ctx tlxp tltp (mkCall (it', args)); + it_cs_as := Some (it', cs, args); + (cs, args) + | _ -> let call_split e = match (OL.lexp_whnf e (ectx_to_lctx ctx)) + with | Call (f, args) -> (f, args) + | _ -> (e,[]) in + let (it, targs) = call_split tltp in + let constructors = match OL.lexp_whnf it (ectx_to_lctx ctx) with + | Inductive (_, _, fargs, constructors) + -> assert (List.length fargs = List.length targs); + constructors + | _ -> lexp_error (sexp_location target) tlxp + ("Can't `case` on objects of this type: " + ^ lexp_string tltp); + SMap.empty in + (constructors, targs) in (* Read patterns one by one *) let fold_fun (lbranches, dflt) (pat, pexp) = @@ -669,19 +694,13 @@ and check_case rtype (loc, target, ppatterns) ctx = | 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 - | (_::_) - -> lexp_error loc lctor - ("Expected pattern of type `" - ^ lexp_string it ^ "` but got `" - ^ lexp_string it' ^ "`") - | [] -> () in - let _ = check_uniqueness pat cons_name lbranches in + -> let _ = check_uniqueness pat cons_name lbranches in + let (constructors, targs) = get_cs_as it' lctor in let cargs = try SMap.find cons_name constructors with Not_found -> lexp_error loc lctor - ("`" ^ (lexp_string it) + ("`" ^ (lexp_string it') ^ "` does not have a `" ^ cons_name ^ "` constructor"); [] in @@ -972,10 +991,16 @@ and lexp_decls_macro (loc, mname) sargs ctx: sexp = with e -> fatal ~loc ("Macro `" ^ mname ^ "` not found") +(* 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 :-( *) and lexp_check_decls (ectx : elab_context) (* External context. *) (nctx : elab_context) (* Context with type declarations. *) (defs : (symbol * sexp) list) : (vname * lexp * ltype) list * elab_context = + (* FIXME: Generalize when/where possible, so things like `map` can be + defined without type annotations! *) (* Preserve the new operators added to nctx. *) let ectx = let (_, a, b, c) = ectx in let (grm, _, _, _) = nctx in ===================================== src/opslexp.ml ===================================== @@ -486,11 +486,11 @@ let rec check'' erased ctx e = let _ = List.fold_left (fun n (v, e, t) -> assert_type nctx e - (push_susp t (S.shift n)) (check (if DB.set_mem (n - 1) nerased then DB.set_empty else nerased) - nctx e); + nctx e) + (push_susp t (S.shift n)); n - 1) (List.length defs) defs in mkSusp (check nerased nctx e) @@ -530,7 +530,7 @@ let rec check'' erased ctx e = (error_tc ~loc:(lexp_location arg) "arg kind mismatch"; ()) else (); - assert_type ctx arg t1 at; + assert_type ctx arg at t1; mkSusp t2 (S.substitute arg) | _ -> (error_tc ~loc:(lexp_location arg) ("Calling a non function (type = " @@ -620,8 +620,8 @@ let rec check'' erased ctx e = (erased, ctx)) in let (nerased, nctx) = mkctx erased ctx s vdefs fieldtypes in assert_type nctx branch - (mkSusp ret (S.shift (List.length fieldtypes))) - (check nerased nctx branch)) + (check nerased nctx branch) + (mkSusp ret (S.shift (List.length fieldtypes)))) branches; let diff = SMap.cardinal constructors - SMap.cardinal branches in (match default with @@ -629,8 +629,8 @@ let rec check'' erased ctx e = -> if diff <= 0 then warning_tc ~loc:l "Redundant default clause"; let nctx = (DB.lctx_extend ctx v (LetDef (0, e)) etype) in - assert_type nctx d (mkSusp ret (S.shift 1)) - (check (DB.set_sink 1 erased) nctx d) + assert_type nctx d (check (DB.set_sink 1 erased) nctx d) + (mkSusp ret (S.shift 1)) | None -> if diff > 0 then error_tc ~loc:l ("Non-exhaustive match: " ===================================== src/unification.ml ===================================== @@ -32,13 +32,16 @@ let log_info = Log.log_info ~section:"UNIF" (* :-( *) let global_last_metavar = ref (-1) (*The first metavar is 0*) -let create_metavar (ctx : DB.lexp_context) (sl : scope_level) (t : ltype) +let create_metavar_1 (sl : scope_level) (t : ltype) (clen : int) = let idx = !global_last_metavar + 1 in global_last_metavar := idx; - metavar_table := U.IMap.add idx (MVar (sl, t, Myers.length ctx)) + metavar_table := U.IMap.add idx (MVar (sl, t, clen)) (!metavar_table); idx +let create_metavar (ctx : DB.lexp_context) (sl : scope_level) (t : ltype) + = create_metavar_1 sl t (Myers.length ctx) + (* For convenience *) type constraint_kind = | CKimpossible (* Unification is simply impossible. *) @@ -110,8 +113,60 @@ let occurs_in (id: meta_id) (e : lexp) : bool = match metavar_lookup id with var after all! *) (metavar_table := old_mvt; true) else false - -(****************************** Top level unify *************************************) + +(* When unifying a metavar with itself, if the two metavars don't + * have the same substitution applied, then we should take the "common subset" + * of those two substitutions: e.g. + * + * ?a[0 => x, 1 => y, 2 => z, ...] =?= ?a[0 => x, 1 => b, 2 => z, ...] + * + * then we know `?a` can't use variable #1 since if it did then the two + * substitutions would result in different terms. + * We can do that by instantiating `?a` with a new metavar: + * + * ?a = ?b[0 => 0, 1 => 2, ...] + * aka + * ?a = ?b[0 => 0 · ↑1] + *) +let common_subset ctx s1 s2 = + let rec loop s1 s2 o1 o2 o = + match (s1, s2) with + | (S.Cons (le1, s1', o1'), S.Cons (le2, s2', o2')) + -> let o1 = o1 + o1' in + let o2 = o2 + o2' in + (* FIXME: We should check if le1 and le2 are *unifiable* instead! *) + if not (le1 = impossible || le1 = impossible) + && OL.conv_p ctx (mkSusp le1 (S.shift o1)) (mkSusp le2 (S.shift o2)) + then match loop s1' s2' o1 o2 1 with + | S.Identity 1 -> S.Identity o (* Optimization! *) + | s' -> S.Cons (mkVar ((lexp_location le1, None), 0), + s', o) + else loop s1' s2' o1 o2 (o + 1) + (* If one of them reached `Identity`, unroll it, knowing that + * + * Identity 0 = #0 · #1 · #2 ... = #0 · (Identity 1) + *) + | (S.Cons _, S.Identity o2') + -> loop s1 (S.Cons (mkVar ((U.dummy_location, None), 0), + S.Identity 1, o2')) + o1 o2 o + | (S.Identity o1', S.Cons _) + -> loop (S.Cons (mkVar ((U.dummy_location, None), 0), + S.Identity 1, o1')) + s2 o1 o2 o + | (S.Identity o1', S.Identity o2') + -> assert (o1 + o1' = o2 + o2'); + S.Identity o + in loop s1 s2 0 0 0 + +(* Return the number of vars difference between input and output context. * + * Could be returned directly by `common_subset`, but it's pretty easy to + * compute it here instead. *) +let rec s_offset s = match s with + | S.Identity o -> o + | S.Cons (_, s', o) -> o - 1 + s_offset s' + +(************************** Top level unify **********************************) (** Dispatch to the right unifier. @@ -161,7 +216,7 @@ and unify' (e1: lexp) (e2: lexp) else ((* print_string "Unification failure on default\n"; *) [(CKresidual, ctx, e1, e2)])) -(********************************* Type specific unify *******************************) +(************************* Type specific unify *******************************) (** Unify a Arrow and a lexp if possible - (Arrow, Arrow) -> if var_kind = var_kind @@ -218,7 +273,7 @@ and unify_lambda (lambda: lexp) (lxp: lexp) ctx vs : return_type = - metavar , metavar -> if Metavar = Metavar then OK else ERROR - metavar , lexp -> OK *) -and unify_metavar ctx idx s (lxp1: lexp) (lxp2: lexp) +and unify_metavar ctx idx s1 (lxp1: lexp) (lxp2: lexp) : return_type = let unif idx s lxp = let t = match metavar_lookup idx with @@ -246,17 +301,68 @@ and unify_metavar ctx idx s (lxp1: lexp) (lxp2: lexp) ^ "\n" ^ "for " ^ lexp_string lxp ^ "\n"); [(CKresidual, ctx, lxp1, lxp2)] in match lxp2 with - | Metavar (idx2, s2, _) + | Metavar (idx2, s2, name) -> if idx = idx2 then - (* FIXME: handle the case where s1 != s2 !! *) - [] + match common_subset ctx s1 s2 with + | S.Identity 0 -> [] (* Optimization! *) + (* ¡ s1 != s2 ! + * Create a new metavar that can only refer to those vars + * which are mapped identically by `s1` and `s2` + * (as found by `common_subset`). + * This metavar doesn't necessarily live exactly in `ctx` + * nor even a proper prefix of it, tho :-( !! + *) + | s -> + (* print_string "Metavar idx-idx s1!=s2\n"; *) + assert (not (OL.conv_p ctx lxp1 lxp2)); + match (Inverse_subst.inverse s, + metavar_lookup idx) with + | (None, _) + -> Log.internal_error + "Can't inverse subst returned by common_subset!" + | (_, MVal _) + -> Log.internal_error + "`lexp_whnf` returned an instantiated metavar!!" + | (Some s_inv, MVar (sl, t, clen)) + -> let clen' = clen - s_offset s in + let t' = mkSusp t s_inv in + let newmv = create_metavar_1 sl t' clen' in + let lexp = mkMetavar (newmv, s, name) in + assert (sl <= clen); + assert (sl <= clen'); + assert (OL.conv_p ctx (mkSusp t' s) t); + (* if (OL.conv_p ctx (mkSusp lexp s1) (mkSusp lexp s2)) then + * print_string ("common_subset successful:\n " + * ^ subst_string s + * ^ "\n =\n " + * ^ subst_string s1 + * ^ "\n ∩\n " + * ^ subst_string s2 + * ^ "\n") + * else + * print_string ("common_subset failed:\n " + * ^ subst_string s + * ^ "\n ∘\n " + * ^ subst_string s1 + * ^ "\n =\n " + * ^ subst_string (scompose s s1) + * ^ "\n!=\n " + * ^ subst_string s + * ^ "\n ∘\n " + * ^ subst_string s2 + * ^ "\n =\n " + * ^ subst_string (scompose s s2) + * ^ "\n"); *) + metavar_table := associate idx lexp (!metavar_table); + assert (OL.conv_p ctx lxp1 lxp2); + [] else (* If one of the two subst can't be inverted, try the other. * FIXME: There's probably a more general solution. *) - (match unif idx s lxp2 with + (match unif idx s1 lxp2 with | [] -> [] | _ -> unif idx2 s2 lxp1) - | _ -> unif idx s lxp2 + | _ -> unif idx s1 lxp2 (** Unify a Call (call) and a lexp (lxp) - Call , Call -> UNIFY @@ -359,7 +465,7 @@ and unify_sort (sort_: lexp) (lxp: lexp) ctx vs : return_type = | Sort _, Var _ -> [(CKresidual, ctx, sort_, lxp)] | _, _ -> [(CKimpossible, ctx, sort_, lxp)] -(************************ Helper function **************************************) +(************************ Helper function ************************************) (***** for Case *****) (** Check arg_king in <code>(arg_kind * vdef option) list </code> in Case *) View it on GitLab: https://gitlab.com/monnier/typer/-/commit/402bdbe074bfa0149141759cb37733846… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/402bdbe074bfa0149141759cb37733846… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][master] * unification.ml: Return just a list rather than an list option
by Stefan 21 Mar '20

21 Mar '20

Stefan pushed to branch master at Stefan / Typer Commits: 86d4a83d by Stefan Monnier at 2020-03-21T18:02:02-04:00 * unification.ml: Return just a list rather than an list option Additionally, keep track of the ctx and annotate whether there's a possibility unification could succeed at some other time. * src/lexp.ml (constraints): Move to unification.ml * src/unification.ml (constraint_kind): New type. (constraints): Rewrite. (unify_and): Remove, use `@` instead. - - - - - 5 changed files: - src/debruijn.ml - src/elab.ml - src/lexp.ml - src/unification.ml - tests/unify_test.ml Changes: ===================================== src/debruijn.ml ===================================== @@ -3,7 +3,7 @@ * * --------------------------------------------------------------------------- * - * Copyright (C) 2011-2019 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. ===================================== src/elab.ml ===================================== @@ -550,7 +550,7 @@ and infer_type pexp ectx var = l))) s (ectx_to_lctx ectx) with - | (None | Some (_::_)) + | (_::_) -> (let lexp_string e = lexp_string (L.clean e) in let typestr = lexp_string t ^ " : " ^ lexp_string s in match var with @@ -560,7 +560,7 @@ and infer_type pexp ectx var = -> lexp_error l t ("Type of `" ^ name ^ "` is not a proper type: " ^ typestr)) - | Some [] -> ()); + | [] -> ()); t and lexp_let_decls declss (body: lexp) ctx = @@ -576,18 +576,13 @@ and unify_with_arrow ctx tloc lxp kind var aty let (l, _) = var in let arrow = mkArrow (kind, var, arg, l, body) in match Unif.unify arrow lxp (ectx_to_lctx ctx) with - | None -> lexp_error tloc lxp ("Type " ^ lexp_string lxp - ^ " and " - ^ lexp_string arrow - ^ " does not match"); - (mkDummy_type ctx l, mkDummy_type nctx l) - | Some ((t1,t2)::_) + | ((_ck, _ctx, t1, t2)::_) -> lexp_error tloc lxp ("Types:\n " ^ lexp_string t1 ^ "\n and:\n " ^ lexp_string t2 ^ "\n do not match!"); (mkDummy_type ctx l, mkDummy_type nctx l) - | Some [] -> arg, body + | [] -> arg, body and check (p : sexp) (t : ltype) (ctx : elab_context): lexp = let (e, ot) = elaborate ctx p (Some t) in @@ -607,17 +602,12 @@ 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 - | None - -> lexp_error (lexp_location e) e - ("Type mismatch! Context expected `" - ^ lexp_string t ^ "` but expression has type `" - ^ lexp_string inferred_t ^ "`") - | Some ((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 ^ "`") - | Some [] -> ()); + | [] -> ()); e (* Lexp.case can sometimes be inferred, but we prefer to always check. *) @@ -680,12 +670,12 @@ and check_case rtype (loc, target, ppatterns) ctx = match nosusp (inst_args ctx lctor) with | Cons (it', (_, cons_name)) -> let _ = match Unif.unify it' it (ectx_to_lctx ctx) with - | (None | Some (_::_)) + | (_::_) -> lexp_error loc lctor ("Expected pattern of type `" ^ lexp_string it ^ "` but got `" ^ lexp_string it' ^ "`") - | Some [] -> () in + | [] -> () in let _ = check_uniqueness pat cons_name lbranches in let cargs = try SMap.find cons_name constructors @@ -1073,12 +1063,12 @@ and lexp_decls_1 | _ -> Log.internal_error "Var not found at its index!" in (* Unify it with the new one. *) let _ = match Unif.unify ltp pt (ectx_to_lctx nctx) with - | (None | Some (_::_)) + | (_::_) -> lexp_error loc ltp ("New type annotation `" ^ lexp_string ltp ^ "` incompatible with previous `" ^ lexp_string pt ^ "`") - | Some [] -> () in + | [] -> () in lexp_decls_1 sdecls ectx nctx pending_decls pending_defs else if List.exists (fun ((_, vname'), _) -> vname = vname') pending_defs then ===================================== src/lexp.ml ===================================== @@ -155,7 +155,6 @@ type metavar_info = * so we just keep the length of the lexp_context. *) * ctx_length type meta_subst = metavar_info U.IMap.t -type constraints = (lexp * lexp) list let dummy_scope_level = 0 let impossible = Imm Sexp.dummy_epsilon ===================================== src/unification.ml ===================================== @@ -40,7 +40,15 @@ let create_metavar (ctx : DB.lexp_context) (sl : scope_level) (t : ltype) idx (* For convenience *) -type return_type = constraints option +type constraint_kind = + | CKimpossible (* Unification is simply impossible. *) + | CKresidual (* We failed to find a unifier. *) +(* FIXME: Each constraint should additionally come with a description of how + it relates to its "top-level" or some other info which might let us + fix the problem (e.g. by introducing coercions). *) +type constraints = (constraint_kind * DB.lexp_context * lexp * lexp) list + +type return_type = constraints (** Alias for VMap.add*) let associate (id: meta_id) (lxp: lexp) (subst: meta_subst) : meta_subst @@ -103,21 +111,6 @@ let occurs_in (id: meta_id) (e : lexp) : bool = match metavar_lookup id with (metavar_table := old_mvt; true) else false -(** - lexp is equivalent to _ in ocaml - (Let , lexp) == (lexp , Let) - UNIFY -> recursive call or dispatching - OK -> add a substituion to the list of substitution - CONSTRAINT -> returns a constraint -*) - -let unify_and res op = match res with - | None -> None - | Some constraints1 - -> match op with - | None -> None - | Some constraints2 -> Some (constraints2@constraints1) - (****************************** Top level unify *************************************) (** Dispatch to the right unifier. @@ -134,17 +127,17 @@ 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 + if e1 == e2 then [] else let e1' = OL.lexp_whnf e1 ctx in let e2' = OL.lexp_whnf e2 ctx in - if e1' == e2' then Some [] else + if e1' == e2' then [] else let changed = true (* not (e1 == e1' && e2 == e2') *) in - if changed && OL.set_member_p vs e1' e2' then Some [] else + 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 _)) - -> if OL.conv_p ctx e1' e2' then Some [] else None + -> 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' @@ -163,10 +156,10 @@ and unify' (e1: lexp) (e2: lexp) * ^ " 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)])) + unify_inductive ctx vs' args1 args2 consts1 consts2 e1 e2 + | _ -> (if OL.conv_p ctx e1' e2' then [] + else ((* print_string "Unification failure on default\n"; *) + [(CKresidual, ctx, e1, e2)])) (********************************* Type specific unify *******************************) @@ -183,15 +176,15 @@ and unify_arrow (arrow: lexp) (lxp: lexp) ctx vs | (Arrow (var_kind1, v1, ltype1, _, lexp1), Arrow (var_kind2, _, ltype2, _, lexp2)) -> if var_kind1 = var_kind2 - then unify_and (unify' ltype1 ltype2 ctx vs) - (unify' lexp1 lexp2 - (DB.lexp_ctx_cons ctx v1 Variable ltype1) - (OL.set_shift vs)) - else None - | (Arrow _, Imm _) -> None - | (Arrow _, Var _) -> Some ([(arrow, lxp)]) + then (unify' ltype1 ltype2 ctx vs) + @(unify' lexp1 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 - | (_, _) -> None + | (_, _) -> [(CKimpossible, ctx, arrow, lxp)] (** Unify a Lambda and a lexp if possible - Lamda , Lambda -> if var_kind = var_kind @@ -206,18 +199,18 @@ and unify_lambda (lambda: lexp) (lxp: lexp) ctx vs : return_type = | (Lambda (var_kind1, v1, ltype1, lexp1), Lambda (var_kind2, _, ltype2, lexp2)) -> if var_kind1 = var_kind2 - then unify_and (unify' ltype1 ltype2 ctx vs) - (unify' lexp1 lexp2 - (DB.lexp_ctx_cons ctx v1 Variable ltype1) - (OL.set_shift vs)) - else None + then (unify' ltype1 ltype2 ctx vs) + @(unify' lexp1 lexp2 + (DB.lexp_ctx_cons ctx v1 Variable ltype1) + (OL.set_shift vs)) + else [(CKimpossible, ctx, lambda, lxp)] | ((Lambda _, Var _) | (Lambda _, Let _) - | (Lambda _, Call _)) -> Some [(lambda, lxp)] - | (Lambda _, Arrow _) -> None - | (Lambda _, Imm _) -> None + | (Lambda _, Call _)) -> [(CKresidual, ctx, lambda, lxp)] + | (Lambda _, Arrow _) + | (Lambda _, Imm _) -> [(CKimpossible, ctx, lambda, lxp)] | (Lambda _, _) -> unify' lxp lambda ctx vs - | (_, _) -> None + | (_, _) -> [(CKimpossible, ctx, lambda, lxp)] (** Unify a Metavar and a lexp if possible - lexp , {metavar <-> none} -> UNIFY @@ -235,15 +228,15 @@ and unify_metavar ctx idx s (lxp1: lexp) (lxp2: lexp) match Inverse_subst.apply_inv_subst lxp s with | exception Inverse_subst.Not_invertible -> log_info ?loc:None ("Unification of metavar failed:\n " - ^ "?[" ^ subst_string s ^ "]" - ^ "\nAgainst:\n " - ^ lexp_string lxp ^ "\n"); - None - | lxp' when occurs_in idx lxp' -> None + ^ "?[" ^ subst_string s ^ "]" + ^ "\nAgainst:\n " + ^ lexp_string lxp ^ "\n"); + [(CKresidual, ctx, lxp1, lxp2)] + | lxp' when occurs_in idx lxp' -> [(CKimpossible, ctx, lxp1, lxp2)] | lxp' -> metavar_table := associate idx lxp' (!metavar_table); match unify t (OL.get_type ctx lxp) ctx with - | Some [] as r -> r + | [] as r -> r (* FIXME: Let's ignore the error for now. *) | _ -> log_info ?loc:None @@ -251,21 +244,18 @@ and unify_metavar ctx idx s (lxp1: lexp) (lxp2: lexp) ^ lexp_string (Lexp.clean t) ^ " != " ^ lexp_string (Lexp.clean (OL.get_type ctx lxp)) ^ "\n" ^ "for " ^ lexp_string lxp ^ "\n"); - Some [] in + [(CKresidual, ctx, lxp1, lxp2)] in match lxp2 with | Metavar (idx2, s2, _) -> if idx = idx2 then (* FIXME: handle the case where s1 != s2 !! *) - Some [] + [] else (* If one of the two subst can't be inverted, try the other. * FIXME: There's probably a more general solution. *) (match unif idx s lxp2 with - | Some s -> Some s - | None -> - match unif idx2 s2 lxp1 with - | Some s -> Some s - | None -> None) + | [] -> [] + | _ -> unif idx2 s2 lxp1) | _ -> unif idx s lxp2 (** Unify a Call (call) and a lexp (lxp) @@ -279,12 +269,11 @@ and unify_call (call: lexp) (lxp: lexp) ctx vs when OL.conv_p ctx lxp_left lxp_right -> List.fold_left (fun op ((ak1, e1), (ak2, e2)) -> if ak1 == ak2 then - unify_and (unify' e1 e2 ctx vs) op - else None) - (Some []) + (unify' e1 e2 ctx vs)@op + else [(CKimpossible, ctx, call, lxp)]) + [] (List.combine lxp_list1 lxp_list2) - | (Call _, _) -> Some [(call, lxp)] - | (_, _) -> None + | (_, _) -> [(CKresidual, ctx, call, lxp)] (** Unify a Case with a lexp - Case, Case -> try to unify @@ -346,16 +335,14 @@ and unify_call (call: lexp) (lxp: lexp) ctx vs and unify_sortlvl (sortlvl: lexp) (lxp: lexp) ctx vs : return_type = match sortlvl, lxp with | (SortLevel s, SortLevel s2) -> (match s, s2 with - | SLz, SLz -> Some [] + | SLz, SLz -> [] | SLsucc l1, SLsucc l2 -> unify' l1 l2 ctx vs | SLlub (l11, l12), SLlub (l21, l22) -> (* FIXME: This SLlub representation needs to be * more "canonicalized" otherwise it's too restrictive! *) - (match (unify' l11 l21 ctx vs, unify' l12 l22 ctx vs) with - | (Some cs1, Some cs2) -> Some (cs1 @ cs2) - | _ -> None) - | _, _ -> None) - | _, _ -> None + (unify' l11 l21 ctx vs)@(unify' l12 l22 ctx vs) + | _, _ -> [(CKimpossible, ctx, sortlvl, lxp)]) + | _, _ -> [(CKresidual, ctx, sortlvl, lxp)] (** Unify a Sort and a lexp - Sort, Sort -> if Sort ~= Sort then OK else ERROR @@ -366,11 +353,11 @@ and unify_sort (sort_: lexp) (lxp: lexp) ctx vs : return_type = match sort_, lxp with | (Sort (_, srt), Sort (_, srt2)) -> (match srt, srt2 with | Stype lxp1, Stype lxp2 -> unify' lxp1 lxp2 ctx vs - | StypeOmega, StypeOmega -> Some [] - | StypeLevel, StypeLevel -> Some [] - | _, _ -> None) - | Sort _, Var _ -> Some [(sort_, lxp)] - | _, _ -> None + | StypeOmega, StypeOmega -> [] + | StypeLevel, StypeLevel -> [] + | _, _ -> [(CKimpossible, ctx, sort_, lxp)]) + | Sort _, Var _ -> [(CKresidual, ctx, sort_, lxp)] + | _, _ -> [(CKimpossible, ctx, sort_, lxp)] (************************ Helper function **************************************) @@ -420,24 +407,28 @@ and is_same arglist arglist2 = * | None -> test e subst) * ) None lst *) -and unify_inductive ctx vs args1 args2 consts1 consts2 = +and unify_inductive ctx vs args1 args2 consts1 consts2 e1 e2 = let unif_formals ctx vs args1 args2 - = if not (List.length args1 == List.length args2) then (ctx, vs, None) else + = if not (List.length args1 == List.length args2) then + (ctx, vs, [(CKimpossible, ctx, e1, e2)]) + 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 []) + if not (ak1 == ak2) then [(CKimpossible, ctx, e1, e2)] + else (unify' t1 t2 ctx vs) @ residue)) + (ctx, vs, []) (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 + if not (SMap.cardinal consts1 == SMap.cardinal consts2) then + [(CKimpossible, ctx, e1, e2)] + 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) + residue' @ residue + | exception Not_found -> [(CKimpossible, ctx, e1, e2)]) consts1 residue (** unify the SMap of list in Inductive *) ===================================== tests/unify_test.ml ===================================== @@ -1,6 +1,6 @@ (* unify_test.ml --- Test the unification algorithm * - * Copyright (C) 2016-2019 Free Software Foundation, Inc. + * Copyright (C) 2016-2020 Free Software Foundation, Inc. * * Author: Vincent Bonnevalle <tiv.crb(a)gmail.com> * @@ -43,7 +43,7 @@ type result = | Equivalent | Nothing -type unif_res = (result * (constraints) option * lexp * lexp) +type unif_res = (result * (constraints) * lexp * lexp) type triplet = string * string * string @@ -192,13 +192,13 @@ let test_input (lxp1: lexp) (lxp2: lexp): unif_res = let orig_subst = !metavar_table in let res = unify lxp1 lxp2 Myers.nil in match res with - | Some [] + | [] -> let new_subst = !metavar_table in if orig_subst == new_subst then (Equivalent, res, lxp1, lxp2) else (Unification, res, lxp1, lxp2) - | Some _ -> (Constraint, res, lxp1, lxp2) - | None -> (Nothing, res, lxp1, lxp2) + | (CKresidual, _, _, _)::_ -> (Constraint, res, lxp1, lxp2) + | (CKimpossible, _, _, _)::_ -> (Nothing, res, lxp1, lxp2) let check (lxp1: lexp) (lxp2: lexp) (res: result): bool = let r, _, _, _ = test_input lxp1 lxp2 View it on GitLab: https://gitlab.com/monnier/typer/-/commit/86d4a83db13b23cac91152ae7bff6858d… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/86d4a83db13b23cac91152ae7bff6858d… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][master] -
by Stefan 20 Mar '20

20 Mar '20

Stefan pushed to branch master at Stefan / Typer Commits: c081c586 by Stefan Monnier at 2020-03-20T11:28:31-04:00 - - - - - - 1 changed file: - samples/hott.typer Changes: ===================================== samples/hott.typer ===================================== @@ -47,8 +47,8 @@ %% We additionally need some kind of elimination on paths like: %% %% Eq_call : Eq(_ := ?t) ?x ?y ≡> I ≡> ?t; -%% Eq_call _ i₀ ↝ ?x -%% Eq_call _ i₁ ↝ ?y +%% Eq_call (_ : Eq x y) i₀ ↝ x +%% Eq_call (_ : Eq x y) i₁ ↝ y %% %% Heterogenous equality could look like: %% @@ -81,7 +81,7 @@ Equiv_function f (g : (x : ?A) -> ?B) = ((x : ?A) -> Eq (f x) (g x)); %% %% It'd be great to support univalence without losing `Eq_cast`, but %% it's not at all clear how: -%% - One way is to make it a non-axiom and replace it with a system that +%% - One way is to make it a non-axiom and implement it as a system that %% proves it directly on a case-by-case basis, as in the paper %% "Equivalence for Free!". %% - Another is to make `Eq_cast` take a proof of `isSet T`, @@ -95,6 +95,17 @@ Equiv_function f (g : (x : ?A) -> ?B) = ((x : ?A) -> Eq (f x) (g x)); %% %% but that begs the question: how could we prevent "promoting" %% a non-erasable proof to an erasable one? +%% - Another is to distinguish univalent universes, as done in the paper +%% "Extending Homotopy Type Theory with Strict Equality". +%% E.g. Our sorts `Type ℓ` would be refined to `Type k ℓ` where `k` +%% would be a boolean indicating if the universe admits univalence or not, +%% and then the J (aka "cast") rule would be restricted so that a proof +%% about equality between univalent types can only be used to coerce +%% between univalent types. +%% This is reminiscent of the confinement of Prop in Coq, so we could +%% similarly restrict the univalent universes so they're always erased +%% before runtime (so we don't need to have the non-nop form of "cast" +%% at run-time). %%%% Propositions, resizing, etc... View it on GitLab: https://gitlab.com/monnier/typer/-/commit/c081c5869f90f7f00b87a1ac179557bb1… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/c081c5869f90f7f00b87a1ac179557bb1… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][master] Fix up various issues with universe levels
by Stefan 18 Mar '20

18 Mar '20

Stefan pushed to branch master at Stefan / Typer Commits: 93cb1223 by Stefan Monnier at 2020-03-18T23:30:00-04:00 Fix up various issues with universe levels * src/builtin.ml (type_eq): Use `mkVar`. * src/elab.ml (elaborate): Use `mkVar`. (infer_level): Add suport for ∪ in type level expressions. * src/lexp.ml (mkSLlub'): Add a crutch. (lexp_unparse, lexp_print): Clarify output of TypeLevel. * src/opslexp.ml (level_canon, level_leq): Move earlier. (conv_p'): Use to fix handling of `SLlub`. (mkSLlub): Fix thinko. (check'', get_type): Use `mkVar`. * src/unification.ml (unify): Improve unification of SLlub. - - - - - 5 changed files: - src/builtin.ml - src/elab.ml - src/lexp.ml - src/opslexp.ml - src/unification.ml Changes: ===================================== src/builtin.ml ===================================== @@ -1,6 +1,6 @@ (* builtin.ml --- Infrastructure to define built-in primitives * - * Copyright (C) 2016-2019 Free Software Foundation, Inc. + * Copyright (C) 2016-2020 Free Software Foundation, Inc. * * Author: Pierre Delaunay <pierre.delaunay(a)hec.ca> * Keywords: languages, lisp, dependent types. @@ -105,12 +105,12 @@ let type_eq = mkArrow (Aerasable, lv, DB.type_level, dloc, mkArrow (Aerasable, tv, - mkSort (dloc, Stype (Var (lv, 0))), dloc, + mkSort (dloc, Stype (mkVar (lv, 0))), dloc, mkArrow (Anormal, (dloc, None), - Var (tv, 0), dloc, + mkVar (tv, 0), dloc, mkArrow (Anormal, (dloc, None), mkVar (tv, 1), dloc, - mkSort (dloc, Stype (Var (lv, 3))))))) + mkSort (dloc, Stype (mkVar (lv, 3))))))) let o2l_bool ctx b = get_predef (if b then "true" else "false") ctx ===================================== src/elab.ml ===================================== @@ -3,7 +3,7 @@ * * --------------------------------------------------------------------------- * - * Copyright (C) 2011-2019 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. @@ -491,7 +491,7 @@ and get_implicit_arg ctx loc oname t = match try (* FIXME: We shouldn't hard code as popular a name as `default`. *) let pidx, pname = (senv_lookup "default" ctx), "default" in - let default = Var ((dloc, Some pname), pidx) in + let default = mkVar ((dloc, Some pname), pidx) in get_attribute ctx loc [default; t] with e -> None with | Some attr @@ -1562,6 +1562,8 @@ let rec infer_level ctx se : lexp = | Symbol _ -> check se type_level ctx | Node (Symbol (_, "s"), [se]) -> mkSortLevel (SLsucc (infer_level ctx se)) + | Node (Symbol (_, "_∪_"), [se1; se2]) + -> 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) ===================================== src/lexp.ml ===================================== @@ -206,6 +206,8 @@ let mkCall (f, es) | _ -> hc (Call (f, es)) 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 | (SortLevel SLz, _) | (_, SortLevel SLz) -> Log.log_fatal ~section:"internal" "lub of SLz" | (SortLevel (SLsucc _), SortLevel (SLsucc _)) @@ -582,7 +584,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, "##Type_ℓ") + | Sort (l, StypeLevel) -> Symbol (l, "##TypeLevel") | Sort (l, Stype sl) -> Node (Symbol (lexp_location sl, "##Type_"), [lexp_unparse sl]) @@ -904,13 +906,13 @@ 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) -> "##Type_ℓ" + | Sort (_, StypeLevel) -> "##TypeLevel" | Sort (_, StypeOmega) -> "##Type_ω" | SortLevel (SLz) -> "##TypeLevel.z" | SortLevel (SLsucc e) -> "(##TypeLevel.succ " ^ lexp_string e ^ ")" | SortLevel (SLlub (e1, e2)) - -> "(##TypeLevel.∪ " ^ lexp_string e1 ^ " " ^ lexp_string e1 ^ ")" + -> "(##TypeLevel.∪ " ^ lexp_string e1 ^ " " ^ lexp_string e2 ^ ")" and lexp_str_ctor ctx ctors = ===================================== src/opslexp.ml ===================================== @@ -216,6 +216,36 @@ let set_shift s : set_plexp = set_shift_n s 1 (********* Testing if two types are "convertible" aka "equivalent" *********) +(* Turn e (presumably of type TypeLevel) into a canonical representation, + * which is basically the set of vars it references along with the number of + * `succ` applied to them. + * `c` is the maximum "constant" level that occurs in `e` + * and `m` maps variable indices to the maxmimum depth at which they were + * found. *) +let level_canon e = + let add_var_depth v d ((c,m) as acc) = + let o = try IMap.find v m with Not_found -> -1 in + if o < d then (c, IMap.add v d m) else acc in + + let rec canon e d ((c,m) as acc) = match e with + | 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) + | Var (_, i) -> add_var_depth i d acc + | Metavar (i, s, _) + -> (match metavar_lookup i with + | MVal e -> canon (push_susp e s) d acc + | _ -> add_var_depth (- i) d acc) + | Susp (e, s) -> canon (push_susp e s) d acc + | _ -> (max_int, m) + in canon e 0 (0,IMap.empty) + +let level_leq (c1, m1) (c2, m2) = + c1 <= c2 + && c1 != max_int + && IMap.for_all (fun i d -> try d <= IMap.find i m2 with Not_found -> false) + m1 + (* Returns true if e₁ and e₂ are equal (upto alpha/beta/...). *) let rec conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = let e1' = lexp_whnf e1 ctx in @@ -233,13 +263,9 @@ 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 - | (SLlub (sl11, sl12), sl2) - (* FIXME: This should be "<=" rather than equality! *) - -> conv_p sl11 e2' && conv_p sl12 e2' - | (sl1, SLlub (sl21, sl22)) - (* FIXME: This should be "<=" rather than equality! *) - -> conv_p e1' sl21 && conv_p e1' sl22 - | _ -> false) + | _ -> let ce1 = level_canon (L.clean e1') in + let ce2 = level_canon (L.clean e2') in + level_leq ce1 ce2 && level_leq ce2 ce1) | (Sort (_, s1), Sort (_, s2)) -> s1 == s2 || (match (s1, s2) with @@ -301,47 +327,17 @@ let conv_p (ctx : DB.lexp_context) e1 e2 (********* Testing if a lexp is properly typed *********) -(* Turn e (presumably of type TypeLevel) into its canonical representation, - * which is basically the set of vars it references along with the number of - * `succ` applied to them. - * `c` is the maximum "constant" level that occurs in `e` - * and `m` maps variable indices to the maxmimum depth at which they were - * found. *) -let level_canon e = - let add_var_depth v d ((c,m) as acc) = - let o = try IMap.find v m with Not_found -> -1 in - if o < d then (c, IMap.add v d m) else acc in - - let rec canon e d ((c,m) as acc) = match e with - | 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) - | Var (_, i) -> add_var_depth i d acc - | Metavar (i, s, _) - -> (match metavar_lookup i with - | MVal e -> canon (push_susp e s) d acc - | _ -> add_var_depth (- i) d acc) - | Susp (e, s) -> canon (push_susp e s) d acc - | _ -> (max_int, m) - in canon e 0 (0,IMap.empty) - -let level_leq (c1, m1) (c2, m2) = - c1 <= c2 - && c1 != max_int - && IMap.for_all (fun i d -> try d <= IMap.find i m2 with Not_found -> false) - m1 - let rec mkSLlub ctx e1 e2 = match (lexp_whnf e1 ctx, lexp_whnf e2 ctx) with - | (SortLevel SLz, e2) -> e2 - | (e1, SortLevel SLz) -> e1 + | (SortLevel SLz, _) -> e2 + | (_, SortLevel SLz) -> e1 | (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 - if level_leq ce1 ce2 then e1 - else if level_leq ce2 ce1 then e2 + 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 *) type sort_compose_result @@ -360,6 +356,10 @@ let sort_compose ctx1 ctx2 l ak k1 k2 = -> if ak == P.Aerasable && impredicative_erase then SortResult (mkSusp k2 (S.substitute impossible)) else let l2' = (mkSusp l2 (S.substitute impossible)) in + (* print_string ("Normal: " ^ lexp_string l1 ^ " -> " + * ^ lexp_string l2' ^ " ==> " + * ^ lexp_string (mkSort (l, Stype (mkSLlub ctx1 l1 l2'))) + * ^ "\n"); *) SortResult (mkSort (l, Stype (mkSLlub ctx1 l1 l2'))) | (StypeLevel, Stype l2) when ak == P.Aerasable && impredicative_universe_poly @@ -367,7 +367,11 @@ let sort_compose ctx1 ctx2 l ak k1 k2 = * It's pretty powerful, e.g. allows tuples containing * level-polymorphic functions, and makes impredicative-encoding * of data types almost(just?) as flexible as inductive types. *) - -> SortResult (mkSusp k2 (S.substitute DB.level0)) + -> (* print_string ("ImpUniv: " ^ lexp_string k1 ^ " ≡> " + * ^ lexp_string k2 ^ " ==> " + * ^ lexp_string (mkSusp k2 (S.substitute DB.level0)) + * ^ "\n"); *) + SortResult (mkSusp k2 (S.substitute DB.level0)) | (StypeLevel, Stype _) | (StypeLevel, StypeOmega) (* This might be safe, but I don't think it adds much power. @@ -608,7 +612,7 @@ let rec check'' erased ctx e = | (ak, vdef)::vdefs, (ak', vdef', ftype)::fieldtypes -> mkctx (dbset_push ak erased) (DB.lexp_ctx_cons ctx vdef Variable (mkSusp ftype s)) - (S.cons (Var (vdef, 0)) + (S.cons (mkVar (vdef, 0)) (S.mkShift s 1)) vdefs fieldtypes | _,_ -> (error_tc ~loc:l @@ -641,7 +645,7 @@ let rec check'' erased ctx e = let rec indtype fargs start_index = match fargs with | [] -> [] - | (ak, vd, _)::fargs -> (ak, Var (vd, start_index)) + | (ak, vd, _)::fargs -> (ak, mkVar (vd, start_index)) :: indtype fargs (start_index - 1) in let rec fieldargs ftypes = match ftypes with @@ -875,7 +879,7 @@ let rec get_type ctx e = let rec indtype fargs start_index = match fargs with | [] -> [] - | (ak, vd, _)::fargs -> (ak, Var (vd, start_index)) + | (ak, vd, _)::fargs -> (ak, mkVar (vd, start_index)) :: indtype fargs (start_index - 1) in let rec fieldargs ftypes = match ftypes with @@ -1007,7 +1011,7 @@ let ctx2tup ctx nctx = SMap.empty), cons_label), List.mapi (fun i (oname, t) - -> (P.Aimplicit, Var (oname, offset - i - 1))) + -> (P.Aimplicit, mkVar (oname, offset - i - 1))) types) | (DB.CVlet (name, LetDef (_, e), t, _) :: blocs) -> Let (loc, [(name, mkSusp e (S.shift 1), t)], ===================================== src/unification.ml ===================================== @@ -1,6 +1,6 @@ (* unification.ml --- Unification of Lexp terms -Copyright (C) 2016-2019 Free Software Foundation, Inc. +Copyright (C) 2016-2020 Free Software Foundation, Inc. Author: Vincent Bonnevalle <tiv.crb(a)gmail.com> @@ -348,8 +348,13 @@ and unify_sortlvl (sortlvl: lexp) (lxp: lexp) ctx vs : return_type = | (SortLevel s, SortLevel s2) -> (match s, s2 with | SLz, SLz -> Some [] | SLsucc l1, SLsucc l2 -> unify' l1 l2 ctx vs - (* FIXME: Handle SLsub! *) - | _, _ -> None) + | SLlub (l11, l12), SLlub (l21, l22) + -> (* FIXME: This SLlub representation needs to be + * more "canonicalized" otherwise it's too restrictive! *) + (match (unify' l11 l21 ctx vs, unify' l12 l22 ctx vs) with + | (Some cs1, Some cs2) -> Some (cs1 @ cs2) + | _ -> None) + | _, _ -> None) | _, _ -> None (** Unify a Sort and a lexp View it on GitLab: https://gitlab.com/monnier/typer/-/commit/93cb1223b53de871422205d2635b24a1e… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/93cb1223b53de871422205d2635b24a1e… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][master] * src/opslexp.ml (impredicative_erase): Disable it
by Stefan 17 Mar '20

17 Mar '20

Stefan pushed to branch master at Stefan / Typer Commits: b4bacaf0 by Stefan Monnier at 2020-03-17T14:26:41-04:00 * src/opslexp.ml (impredicative_erase): Disable it (impredicative_universe_poly): Rename from deep_universe_poly. - - - - - 1 changed file: - src/opslexp.ml Changes: ===================================== src/opslexp.ml ===================================== @@ -1,6 +1,6 @@ (* opslexp.ml --- Operations on Lexps -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. @@ -46,11 +46,13 @@ let conv_erase = true (* Makes conv ignore erased terms. *) (* `impredicative_erase` is inconsistent: as shown in samples/hurkens.typer * it allows the definition of an inf-looping expression of type ⊥. *) -let impredicative_erase = true (* Allows erasable args to be impredicative. *) +let impredicative_erase = false (* Allows erasable args to be impredicative. *) -(* The safety of `deep_universe_poly` is unknown. - * But I also like the idea. *) -let deep_universe_poly = true (* Assume arg is TypeLevel.z when erasable. *) +(* The safety of `impredicative_universe_poly` is unknown. + * But I also like the idea. + * Furthermore it is sufficient to be able to encode System-F (tho + * I haven't been able to generalize this result to Fω). *) +let impredicative_universe_poly = true (* Assume arg is TypeLevel.z when erasable. *) (* Lexp context *) @@ -360,7 +362,7 @@ let sort_compose ctx1 ctx2 l ak k1 k2 = else let l2' = (mkSusp l2 (S.substitute impossible)) in SortResult (mkSort (l, Stype (mkSLlub ctx1 l1 l2'))) | (StypeLevel, Stype l2) - when ak == P.Aerasable && deep_universe_poly + when ak == P.Aerasable && impredicative_universe_poly (* The safety/soundness of this rule is completely unknown. * It's pretty powerful, e.g. allows tuples containing * level-polymorphic functions, and makes impredicative-encoding View it on GitLab: https://gitlab.com/monnier/typer/-/commit/b4bacaf063bc0fbdd54347c6f9e8b9068… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/b4bacaf063bc0fbdd54347c6f9e8b9068… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][master] * samples/hott.typer: New file
by Stefan 17 Mar '20

17 Mar '20

Stefan pushed to branch master at Stefan / Typer Commits: 93c051db by Stefan Monnier at 2020-03-17T14:06:01-04:00 * samples/hott.typer: New file - - - - - 1 changed file: - + samples/hott.typer Changes: ===================================== samples/hott.typer ===================================== @@ -0,0 +1,132 @@ +%%% HoTT -- Homotopy Type-Theory + +%% Copyright (C) 2020 Free Software Foundation, Inc. +%% +%% Author: Stefan Monnier <monnier(a)iro.umontreal.ca> +%% +%% This file is part of Typer. +%% +%% Typer is free software; you can redistribute it and/or modify it under the +%% terms of the GNU General Public License as published by the Free Software +%% Foundation, either version 3 of the License, or (at your option) any +%% later version. +%% +%% Typer is distributed in the hope that it will be useful, but WITHOUT ANY +%% WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS +%% FOR A PARTICULAR PURPOSE. See the GNU General Public License for +%% more details. +%% +%% You should have received a copy of the GNU General Public License along +%% with this program. If not, see <http://www.gnu.org/licenses/>. + +%%% Commentary: + +%% Various definitions inspired from the HoTT book. + +%%% Code: + +%%%% Paths + +%% Cubical interval type `I` +%% Path type: +%% +%% I : Type0? +%% i₀ : I; +%% i₁ : I; +%% +%% Note: while one cannot eliminate (no `if`) on `I`, one can use +%% `∨`, `∧`, and `¬` on values of this type, and maybe one could do +%% `type I | i₀ | i₁` and allow elimination with the simple restriction +%% that you can only eliminate an `I` to another `I` (so one could define +%% `∨` by hand). Better yet, maybe instead of a special `I` we could simply +%% use a normal `Bool`, since the `≡>` already prevents elimination? +%% +%% Eq : (t : Type) ≡> t → t → Type; +%% path : (p : I ≡> t) → Eq (p(_ := i₀)) (p(_ := i₁)); +%% +%% We additionally need some kind of elimination on paths like: +%% +%% Eq_call : Eq(_ := ?t) ?x ?y ≡> I ≡> ?t; +%% Eq_call _ i₀ ↝ ?x +%% Eq_call _ i₁ ↝ ?y +%% +%% Heterogenous equality could look like: +%% +%% HEq (t₁ : Type) ≡> (t₂ : Type) ≡> t₁ → t₂ → Type; +%% type HEq x₁ x₂ +%% | Hrefl (p : Eq t₁ t₂) (Eq (coe p x₁) x₂); +%% type HEq (t : (i : I) ≡> Type) +%% (x₁ : t(i := i₀)) (x₂ : t(i := i₁)) +%% | Hrefl (p : Eq t₁ t₂) (Eq (coe p x₁) x₂); + +%%%% Univalence + +%% type Equiv_function (f : ?A -> ?B) (g : ?A -> ?B) +%% | equiv_function ((x : ?) -> Eq (f x) (g x)); +Equiv_function f (g : (x : ?A) -> ?B) = ((x : ?A) -> Eq (f x) (g x)); +%% Equiv_function_axiom : Equiv_function ?f ?g -> Eq ?f ?g; + +%% type HoTT_IsEquiv (f : ?A -> ?B) +%% | hott_isequiv (Equiv_function (compose f ?g) identity) +%% (Equiv_function (compose ?h f) identity); + +%% type Equiv_type (A : Type) (B : Type) +%% | equiv_type (f : A -> B) (HoTT_Isequiv f); +%% univalence_axiom : Equiv_type A B -> Eq A B; + +%% FIXME: Univalence is incompatible with Typer's `Eq_cast` because +%% it allows casting between, say, `Nat` and `BinNat` which is not +%% a no-op. Cubical Agda supports it by making its "Eq elimination" into a +%% non-trivial operation whose `Eq` proof is very much non-erasable. +%% +%% It'd be great to support univalence without losing `Eq_cast`, but +%% it's not at all clear how: +%% - One way is to make it a non-axiom and replace it with a system that +%% proves it directly on a case-by-case basis, as in the paper +%% "Equivalence for Free!". +%% - Another is to make `Eq_cast` take a proof of `isSet T`, +%% but that prevents use of `Eq_cast` between `Nat` and `α` +%% since `isSet Type` is not true. +%% It would also prevent use of `Eq_cast` on HIT. +%% - Ideally another would be to require `Eq_cast` to take an additional +%% proof that the equality proof is equal to `eq_refl` or more generally: +%% +%% Eq_cast: (eq: Eq ?x ?y) ≡> Eq_erasable eq ≡> .... +%% +%% but that begs the question: how could we prevent "promoting" +%% a non-erasable proof to an erasable one? + +%%%% Propositions, resizing, etc... + +HoTT_isSet A = (x : A) -> (y : A) -> (p : Eq x y) -> (q : Eq x y) -> Eq p q; +%% `isProp` basically implies proof irrelevance. +%% So it also implies erasability. Note that if we use the double-negation +%% encoding of classical `or` in type-theory, then it preserves `isProp`! +HoTT_isProp P = (x : P) -> (y : P) -> Eq x y; + +%% Provable without axioms: +%% +%% ¬¬¬A -> ¬A + +Inverse_double_negation : ?A -> Not (Not ?A); +Inverse_double_negation a na = na a; + +Weak_double_negation : Not (Not (Not ?A)) -> Not ?A; +Weak_double_negation nnna a = nnna (lambda na -> na a); + +%% BEWARE: univalence_axiom incompatible with general LEM! +%% HoTT_LEM_axiom : HoTT_isProp A -> ¬¬A -> A; + +%% "mere propositions" can be treated impredicatively!! +%% HoTT_propositional_resizing_axiom : +%% Equiv_type { A : Type l | isProp A} { A : Type (l + 1) | isProp A} + +%% Propositional truncation: ||A|| is equivalent to A but is a mere proposition. +%% One way to approximate could be: +Propositional_truncation A = (P : ?) ≡> HoTT_isProp P ≡> (A -> P) -> P; +propositional_truncation : ?A -> Propositional_truncation ?A; +propositional_truncation a f = f a; + + + +%%% hott.typer ends here. View it on GitLab: https://gitlab.com/monnier/typer/-/commit/93c051dbed31e0ccc2969fea85ca5d25f… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/93c051dbed31e0ccc2969fea85ca5d25f… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][master] * src/env.ml (BI): Use `Z` rather than `Big_int`
by Stefan 17 Mar '20

17 Mar '20

Stefan pushed to branch master at Stefan / Typer Commits: 4bcb4b11 by Stefan Monnier at 2020-03-17T13:59:49-04:00 * src/env.ml (BI): Use `Z` rather than `Big_int` * GNUmakefile (OBFLAGS): Use Zarith rather than Num - - - - - 3 changed files: - GNUmakefile - src/env.ml - src/eval.ml Changes: ===================================== GNUmakefile ===================================== @@ -8,7 +8,7 @@ SRC_FILES := $(wildcard ./src/*.ml) CPL_FILES := $(wildcard ./$(BUILDDIR)/src/*.cmo) TEST_FILES := $(wildcard ./tests/*_test.ml) -OBFLAGS = -tag debug -tag profile -lib str -build-dir $(BUILDDIR) -pkg num +OBFLAGS = -tag debug -tag profile -lib str -build-dir $(BUILDDIR) -pkg zarith # OBFLAGS := -I $(SRCDIR) -build-dir $(BUILDDIR) -pkg str # OBFLAGS_DEBUG := -tag debug -tag profile -tag "warn(+20)" # OBFLAGS_RELEASE := -tag unsafe -tag inline ===================================== src/env.ml ===================================== @@ -3,7 +3,7 @@ * * --------------------------------------------------------------------------- * - * Copyright (C) 2011-2018 Free Software Foundation, Inc. + * Copyright (C) 2011-2018, 2020 Free Software Foundation, Inc. * * Author: Pierre Delaunay <pierre.delaunay(a)hec.ca> * Keywords: languages, lisp, dependent types. @@ -37,7 +37,7 @@ open Sexp open Elexp module M = Myers module L = Lexp -module BI = Big_int +module BI = Z (* Was Big_int *) module DB = Debruijn let dloc = Util.dummy_location @@ -49,7 +49,7 @@ let str_idx idx = "[" ^ (string_of_int idx) ^ "]" type value_type = | Vint of int - | Vinteger of BI.big_int + | Vinteger of BI.t | Vstring of string | Vcons of symbol * value_type list | Vbuiltin of string @@ -72,7 +72,7 @@ type value_type = let rec value_equal a b = match a, b with | Vint (i1), Vint (i2) -> i1 = i2 - | Vinteger (i1), Vinteger (i2) -> BI.eq_big_int i1 i2 + | Vinteger (i1), Vinteger (i2) -> i1 = i2 | Vstring (s1), Vstring (s2) -> s1 = s2 | Vbuiltin (s1), Vbuiltin (s2) -> s1 = s2 | Vfloat (f1), Vfloat (f2) -> f1 = f2 @@ -142,7 +142,7 @@ let rec value_string v = | Vstring s -> "\"" ^ s ^ "\"" | Vbuiltin s -> s | Vint i -> string_of_int i - | Vinteger i -> BI.string_of_big_int i + | Vinteger i -> BI.to_string i | Vfloat f -> string_of_float f | Vsexp s -> sexp_string s | Vtype e -> L.lexp_string e ===================================== src/eval.ml ===================================== @@ -3,7 +3,7 @@ * * --------------------------------------------------------------------------- * - * Copyright (C) 2011-2018 Free Software Foundation, Inc. + * Copyright (C) 2011-2018, 2020 Free Software Foundation, Inc. * * Author: Pierre Delaunay <pierre.delaunay(a)hec.ca> * Keywords: languages, lisp, dependent types. @@ -196,10 +196,10 @@ let add_binary_biop name f = | _ -> error loc ("`" ^ name ^ "` expects 2 Integer arguments") in add_builtin_function name f 2 -let _ = add_binary_biop "+" BI.add_big_int; - add_binary_biop "-" BI.sub_big_int; - add_binary_biop "*" BI.mult_big_int; - add_binary_biop "/" BI.div_big_int +let _ = add_binary_biop "+" BI.add; + add_binary_biop "-" BI.sub; + add_binary_biop "*" BI.mul; + add_binary_biop "/" BI.div let add_binary_bool_biop name f = let name = "Integer." ^ name in @@ -209,17 +209,17 @@ let add_binary_bool_biop name f = | _ -> error loc ("`" ^ name ^ "` expects 2 Integer arguments") in add_builtin_function name f 2 -let _ = add_binary_bool_biop "<" BI.lt_big_int; - add_binary_bool_biop ">" BI.gt_big_int; - add_binary_bool_biop "=" BI.eq_big_int; - add_binary_bool_biop ">=" BI.ge_big_int; - add_binary_bool_biop "<=" BI.le_big_int; +let _ = add_binary_bool_biop "<" BI.lt; + add_binary_bool_biop ">" BI.gt; + add_binary_bool_biop "=" BI.equal; + add_binary_bool_biop ">=" BI.geq; + add_binary_bool_biop "<=" BI.leq; let name = "Int->Integer" in add_builtin_function name (fun loc (depth : eval_debug_info) (args_val: value_type list) -> match args_val with - | [Vint v] -> Vinteger (BI.big_int_of_int v) + | [Vint v] -> Vinteger (BI.of_int v) | _ -> error loc ("`" ^ name ^ "` expects 1 Int argument")) 1 @@ -283,7 +283,7 @@ let make_string loc depth args_val = match args_val with | _ -> error loc "Sexp.string expects one string as argument" let make_integer loc depth args_val = match args_val with - | [Vinteger n] -> Vsexp (Integer (loc, BI.int_of_big_int n)) + | [Vinteger n] -> Vsexp (Integer (loc, BI.to_int n)) | _ -> error loc "Sexp.integer expects one integer as argument" let make_float loc depth args_val = match args_val with @@ -589,7 +589,7 @@ and sexp_dispatch loc depth args = eval str (add_rte_variable vdummy (Vstring s) rctx) | Integer (_ , i) -> let rctx = ctx_it in - eval it (add_rte_variable vdummy (Vinteger (BI.big_int_of_int i)) + eval it (add_rte_variable vdummy (Vinteger (BI.of_int i)) rctx) | Float (_ , f) -> let rctx = ctx_flt in @@ -691,7 +691,7 @@ let int_to_string loc depth args_val = match args_val with | _ -> error loc "Int->String expects one Int argument" let integer_to_string loc depth args_val = match args_val with - | [Vinteger x] -> Vstring (BI.string_of_big_int x) + | [Vinteger x] -> Vstring (BI.to_string x) | _ -> error loc "Integer->String expects one Integer argument" let sys_exit loc depth args_val = match args_val with View it on GitLab: https://gitlab.com/monnier/typer/-/commit/4bcb4b11c4467ed7e5859436caa46fb1b… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/4bcb4b11c4467ed7e5859436caa46fb1b… You're receiving this email because of your account on gitlab.com.

1 0

2024

2023

2022

2021

2020

2019

2018

2017

2016

Typer Mars 2020