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@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@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/402bdbe074bfa0149141759cb377338467...