Stefan pushed to branch master at Stefan / Typer

Commits: 494d60da by Stefan Monnier at 2017-09-19T20:30:58Z Auto-generalize variable's type declarations

* btl/pervasive.typer: Simplify declarations, relying on generalization.

* src/debruijn.ml (scope): Remove. (meta_scope): New type alias. (elab_context): Use it to add a map of known metavar names. (empty_elab_context, ectx_new_scope): Handle the new metavar map. (get_size): Add sanity check.

* src/elab.ml (meta_to_var, infer_and_generalize_type): New functions. (lexp_decls_1): Use them to generalize var declarations. (sform_identifier): Use new metavar map to handle names metavars.

* src/inverse_subst.ml (invertible, lookup_inv_subst) (shift_inv_subst, compose_inv_subst, apply_inv_subst): New functions.

* src/lexp.ml (meta_id): New type alias. (lexp): Use it.

* src/opslexp.ml (mv_set): Keep track of types, names, and (meta)scope. (mv_set_union): Adjust accordingly.

* src/unification.ml (_unify_metavar): Use apply_inv_subst!

- - - - -

7 changed files:

- btl/pervasive.typer - src/debruijn.ml - src/elab.ml - src/inverse_subst.ml - src/lexp.ml - src/opslexp.ml - src/unification.ml

Changes:

===================================== btl/pervasive.typer ===================================== --- a/btl/pervasive.typer +++ b/btl/pervasive.typer @@ -38,7 +38,7 @@ none = datacons Option none;

%%%% List functions

-List_length : (a : Type) ≡> List a -> Int; +List_length : List ?a -> Int; List_length xs = case xs | nil => 0 | cons hd tl => @@ -49,37 +49,40 @@ List_length xs = case xs %% - Provide a default value : `a -> List a -> a`; %% - Disallow problem case : `(l : List a) -> (l != nil) -> a`; %% - Return an Option/Error +List_head1 : List ?a -> Option ?a; List_head1 : (a : Type) ≡> List a -> Option a; List_head1 xs = case xs | nil => none | cons hd tl => some hd;

-List_head : (a : Type) ≡> a -> List a -> a; +List_head : ?a -> List ?a -> ?a; List_head x = lambda xs -> case xs | cons x _ => x | nil => x;

-List_tail : (a : Type) ≡> List a -> List a; +List_tail : List ?a -> List ?a; List_tail xs = case xs | nil => nil | cons hd tl => tl;

-List_map : (a : Type) ≡> (b : Type) ≡> (a -> b) -> List a -> List b; +List_map : (?a -> ?b) -> List ?a -> List ?b; List_map f = lambda xs -> case xs | nil => nil | cons x xs => cons (f x) (List_map f xs);

-List_foldr : (a : Type) ≡> (b : Type) ≡> (b -> a -> a) -> List b -> a -> a; +List_foldr : (?b -> ?a -> ?a) -> List ?b -> ?a -> ?a; +List_foldr : (l : TypeLevel) ≡> (a : Type_ l) ≡> (b : Type) + ≡> (b -> a -> a) -> List b -> a -> a; List_foldr f = lambda xs -> lambda i -> case xs | nil => i | cons x xs => f x (List_foldr f xs i);

-List_find : (a : Type) ≡> (a -> Bool) -> List a -> Option a; +List_find : (?a -> Bool) -> List ?a -> Option ?a; List_find f = lambda xs -> case xs | nil => none | cons x xs => case f x | true => some x | false => List_find f xs;

-List_nth : (a : Type) ≡> Int -> List a -> a -> a; +List_nth : Int -> List ?a -> ?a -> ?a; List_nth = lambda n -> lambda xs -> lambda d -> case xs | nil => d | cons x xs @@ -139,24 +142,29 @@ lambda_≡>_ = macro (multiarg_lambda "##lambda_≡>_");

%%%% More list functions

-List_reverse : (a : Type) ≡> List a -> List a -> List a; +List_reverse : List ?a -> List ?a -> List ?a; List_reverse l t = case l | nil => t | cons hd tl => List_reverse tl (cons hd t);

-List_concat : (a : Type) ≡> List a -> List a -> List a; +List_concat : List ?a -> List ?a -> List ?a; List_concat l t = List_reverse (List_reverse l nil) t;

-List_foldl : (a : Type) ≡> (b : Type) ≡> (a -> b -> a) -> a -> List b -> a; +List_foldl : (?a -> ?b -> ?a) -> ?a -> List ?b -> ?a; List_foldl f i xs = case xs | nil => i | cons x xs => List_foldl f (f i x) xs;

%%% Good 'ol combinators

-I : (a : Type) ≡> a -> a; +I : ?a -> ?a; I x = x;

+%% Use explicit erasable annotations since with an annotation like +%% K : ?a -> ?b -> ?a; +%% Typer generalizes to +%% K : (a : Type) ≡> (b : Type) ≡> a -> b -> a; +%% Which is less general. K : (a : Type) ≡> a -> (b : Type) ≡> b -> a; K x y = x;

===================================== src/debruijn.ml ===================================== --- a/src/debruijn.ml +++ b/src/debruijn.ml @@ -98,21 +98,25 @@ type lexp_context = env_elem M.myers

type db_ridx = int (* DeBruijn reverse index (i.e. counting from the root). *)

-(* Map matching variable name and its distance in the current scope *) -type scope = db_ridx SMap.t (* Map<String, db_ridx>*) - +(* Map variable name to its distance in the context *) type senv_length = int (* it is not the map true length *) -type senv_type = senv_length * scope +type senv_type = senv_length * (db_ridx SMap.t)

type lctx_length = db_ridx

+type meta_scope + = scope_level (* Integer identifying a level. *) + * lctx_length (* Length of ctx when the scope is added. *) + * (meta_id SMap.t ref) (* Metavars already known in this scope. *) + (* This is the *elaboration context* (i.e. a context that holds * a lexp context plus some side info. *) type elab_context - = Grammar.grammar * senv_type * lexp_context * (scope_level * lctx_length) + = Grammar.grammar * senv_type * lexp_context * meta_scope

-let get_size ctx = let (_, (n, _), lctx, _) = ctx in - assert (n = M.length lctx); n +let get_size (ctx : elab_context) + = let (_, (n, _), lctx, _) = ctx in + assert (n = M.length lctx); n

let ectx_to_grm (ectx : elab_context) : Grammar.grammar = let (grm,_, _, _) = ectx in grm @@ -121,9 +125,10 @@ let ectx_to_grm (ectx : elab_context) : Grammar.grammar = let ectx_to_lctx (ectx : elab_context) : lexp_context = let (_,_, lctx, _) = ectx in lctx

-let ectx_to_scope_level ((_, _, _, (sl, _)) : elab_context) : scope_level = sl +let ectx_to_scope_level ((_, _, _, (sl, _, _)) : elab_context) : scope_level + = sl

-let ectx_local_scope_size ((_, (n, _), _, (_, slen)) as ectx: elab_context) : int +let ectx_local_scope_size ((_, (n, _), _, (_, slen, _)) as ectx) : int = get_size ectx - slen

(* internal definitions @@ -137,7 +142,8 @@ let _make_myers = M.nil * ---------------------------------- *)

let empty_elab_context : elab_context - = (Grammar.default_grammar, _make_senv_type, _make_myers, (0, 0)) + = (Grammar.default_grammar, _make_senv_type, _make_myers, + (0, 0, ref SMap.empty))

(* return its current DeBruijn index *) let rec senv_lookup (name: string) (ctx: elab_context): int = @@ -193,11 +199,11 @@ let ectx_extend_rec (ctx: elab_context) (defs: (vname * lexp * ltype) list) = (senv, n) defs in (grm, (n + List.length defs, senv'), lctx_extend_rec lctx defs, sl)

-let ectx_new_scope ectx : elab_context = - let (grm, senv, lctx, (scope, _)) = ectx in - (grm, senv, lctx, (scope + 1, Myers.length lctx)) +let ectx_new_scope (ectx : elab_context) : elab_context = + let (grm, senv, lctx, (scope, _, rmmap)) = ectx in + (grm, senv, lctx, (scope + 1, Myers.length lctx, ref (!rmmap)))

-let ectx_get_scope (ectx : elab_context) : (scope_level * lctx_length) = +let ectx_get_scope (ectx : elab_context) : meta_scope = let (_, _, _, sl) = ectx in sl

let ectx_get_grammar (ectx : elab_context) : Grammar.grammar =

===================================== src/elab.ml ===================================== --- a/src/elab.ml +++ b/src/elab.ml @@ -271,6 +271,72 @@ let elab_varref ctx ((loc, name) as id) let ltp = env_lookup_type ctx (id, idx) in (lxp, Inferred ltp)

+(* Turn metavar into plain vars after generalization. *) +let rec meta_to_var idxs o (e : lexp) = + let rec loop e = match e with + | Imm _ -> e + | SortLevel SLz -> e + | SortLevel (SLsucc e) -> mkSortLevel (SLsucc (loop e)) + | SortLevel (SLlub (e1, e2)) -> mkSortLevel (SLlub (loop e1, loop e2)) + | Sort (l, Stype e) -> mkSort (l, Stype (loop e)) + | Sort (_, (StypeOmega | StypeLevel)) -> e + | Builtin _ -> e + | Var _ -> e + | Susp (e, s) -> loop (push_susp e s) + | Let (l, defs, e) + -> let len = List.length defs in + let (_, ndefs) + = List.fold_right (fun (l,e,t) (o', defs) + -> let o' = o' - 1 in + (o', (l, meta_to_var idxs (len + o) e, + meta_to_var idxs (o' + o) t) :: defs)) + defs (len, []) in + mkLet (l, ndefs, meta_to_var idxs (len + o) e) + | Arrow (ak, v, t1, l, t2) + -> mkArrow (ak, v, loop t1, l, meta_to_var idxs (1 + o) t2) + | Lambda (ak, v, t, e) + -> mkLambda (ak, v, loop t, meta_to_var idxs (1 + o) e) + | Call (f, args) + -> mkCall (loop f, List.map (fun (ak, e) -> (ak, loop e)) args) + | Inductive (l, label, args, cases) + -> let alen = List.length args in + let (_, nargs) + = List.fold_right (fun (ak, v, t) (o', args) + -> let o' = o' - 1 in + (o', (ak, v, meta_to_var idxs (o' + o) t) + :: args)) + args (alen, []) in + let ncases + = SMap.map + (fun fields + -> let flen = List.length fields in + let (_, nfields) + = List.fold_right + (fun (ak, v, t) (o', fields) + -> let o' = o' - 1 in + (o', (ak, v, meta_to_var idxs (o' + o) t) + :: fields)) + fields (flen, []) in + nfields) + cases in + mkInductive (l, label, nargs, ncases) + | Cons (t, l) -> mkCons (loop t, l) + | Case (l, e, t, cases, default) + -> let ncases + = SMap.map + (fun (l, fields, e) + -> (l, fields, meta_to_var idxs (o + List.length fields) e)) + cases in + mkCase (l, loop e, loop t, ncases, + match default with None -> None | Some (v, e) -> Some (v, loop e)) + | Metavar (id, s, name) + -> if IMap.mem id idxs then + mkVar (name, o + IMap.find id idxs) + else match metavar_lookup id with + | MVal e -> loop (push_susp e s) + | _ -> e + in loop e + (* Infer or check, as the case may be. *) let rec elaborate ctx se ot = match se with @@ -816,6 +882,49 @@ and lexp_check_decls (ectx : elab_context) (* External context. *) let decls = List.rev (List.map (fun (_, d) -> d) (IMap.bindings declmap)) in decls, ctx_define_rec ectx decls

+and infer_and_generalize_type (ctx : elab_context) se oname = + let l = sexp_location se in + let nctx = ectx_new_scope ctx in + let sl = ectx_to_scope_level nctx in + let cl = Myers.length (ectx_to_lctx nctx) in + let t = infer_type se nctx oname in + match OL.lexp_whnf t (ectx_to_lctx ctx) with + (* There's no point generalizing a single metavar, and it's useful + * to keep it ungeneralized so you can use `x : ?` to declare that + * `x` will be defined later. *) + | Metavar _ -> t + | _ + -> let (_, mfvs) = OL.fv t in + if mfvs = IMap.empty then t else ( + let mfvs = IMap.fold (fun idx (sl', mt, cl', vname) fvs + -> if sl' < sl then + (* This metavar appears in the context, + * so we can't generalize over it. *) + fvs + else ( + assert (cl' >= cl); + (idx, vname, + if cl' > cl then + Inverse_subst.apply_inv_subst + mt (S.shift (cl' - cl)) + else + mt) + :: fvs)) + mfvs [] in + (* FIXME: Sort `mvfs' topologically! *) + let len = List.length mfvs in + let t = mkSusp t (S.shift len) in + let rec loop idxs n mfvs = match mfvs with + | [] -> assert (n = 0); meta_to_var idxs 0 t + | ((idx, vname, mt) :: mfvs) + -> let mt' = mkSusp mt (S.shift (len - n)) in + let mt'' = meta_to_var idxs (- n) mt' in + let n = n - 1 in + let t' = loop (IMap.add idx n idxs) n mfvs in + mkArrow (Aerasable, Some vname, mt'', l, + t') in + loop (IMap.empty) len mfvs) +

and lexp_decls_1 (sdecls : sexp list) @@ -844,7 +953,7 @@ and lexp_decls_1 (* FIXME: Move this to a "special form"! *) -> (match args with | [Symbol ((l, vname) as v); stp] - -> let ltp = infer_type stp (ectx_new_scope nctx) (Some v) in + -> let ltp = infer_and_generalize_type nctx stp (Some v) in if SMap.mem vname pending_decls then (* Don't burp: take'em all and unify! *) let pt_idx = senv_lookup vname nctx in @@ -1161,8 +1270,7 @@ let sform_identifier ctx loc sargs ot = when String.length name >= 1 && String.get name 0 = '?' -> assert (String.length name >= 1 && String.get name 0 = '?'); let name = if name = "?" then "" else - (sexp_error loc "Named metavars not supported (yet)"; - String.sub name 1 (String.length name)) in + string_sub name 1 (String.length name) in (* Shift the var so it can't refer to the local vars. * This is used so that in cases like "lambda t (y : ?) ... " * type inference can guess ? without having to wonder whether it @@ -1172,14 +1280,23 @@ let sform_identifier ctx loc sargs ot = let octx = Myers.nthcdr ctx_shift (ectx_to_lctx ctx) in let sl = ectx_to_scope_level ctx in let subst = S.shift ctx_shift in - let t = match ot with - | None -> newMetatype octx sl loc - (* FIXME: `t` is defined in ctx instead of octx. - * We need something like: - * let t = push_inv_subst t (S.shift ctx_shift) in *) - | Some t -> t in - (mkSusp (newMetavar octx sl loc name t) subst, - match ot with Some _ -> Checked | None -> Lazy) + let (_, _, rmmap) = ectx_get_scope ctx in + if not (name = "") && SMap.mem name (!rmmap) then + (mkMetavar (SMap.find name (!rmmap), subst, (loc, name)), Lazy) + else + let t = match ot with + | None -> newMetatype octx sl loc + | Some t + (* `t` is defined in ctx instead of octx. *) + -> Inverse_subst.apply_inv_subst t subst in + let mv = newMetavar octx sl loc name t in + (if not (name = "") then + let idx = match mv with + | Metavar (idx, _, _) -> idx + | _ -> fatal loc "newMetavar returned a non-Metavar" in + rmmap := SMap.add name idx (!rmmap)); + (mkSusp mv subst, + match ot with Some _ -> Checked | None -> Lazy)

(* Normal identifier. *) | [Symbol id]

===================================== src/inverse_subst.ml ===================================== --- a/src/inverse_subst.ml +++ b/src/inverse_subst.ml @@ -56,8 +56,8 @@ type substIR = ((int * int) list * int * int) (** Transform a substitution to a more linear substitution * makes the inversion easier * Example of result : ((new_idx, old_position)::..., shift)*) -let transfo (s: lexp S.subst) : substIR option = - let rec transfo (s: lexp S.subst) (off_acc: int) (idx: int) (imp_cnt : int) +let transfo (s: Lexp.subst) : substIR option = + let rec transfo (s: Lexp.subst) (off_acc: int) (idx: int) (imp_cnt : int) : substIR option = let indexOf (v: lexp): int = (* Helper : return the index of a variabble *) match v with @@ -92,7 +92,7 @@ let rec sizeOf (s: (int * int) list): int = List.length s let counter = ref 0 let mkVar (idx: int) : lexp = counter := !counter + 1; - Var((U.dummy_location, "<anon" ^ string_of_int idx ^ ">"), idx) + Lexp.mkVar ((U.dummy_location, "<anon" ^ string_of_int idx ^ ">"), idx)

(** Fill the gap between e_i in the list of couple (e_i, i) by adding dummy variables. @@ -103,18 +103,18 @@ let mkVar (idx: int) : lexp = @param size size of the list to return @param acc recursion accumulator *) -let fill (l: (int * int) list) (nbVar: int) (shift: int): lexp S.subst option = - let rec genDummyVar (beg_: int) (end_: int) (l: lexp S.subst): lexp S.subst = (* Create the filler variables *) +let fill (l: (int * int) list) (nbVar: int) (shift: int): Lexp.subst option = + let rec genDummyVar (beg_: int) (end_: int) (l: Lexp.subst): Lexp.subst = (* Create the filler variables *) if beg_ < end_ then S.cons impossible (genDummyVar (beg_ + 1) end_ l) else l in - let fill_before (l: (int * int) list) (s: lexp S.subst) (nbVar: int): lexp S.subst option = (* Fill if the first var is not 0 *) + let fill_before (l: (int * int) list) (s: Lexp.subst) (nbVar: int): Lexp.subst option = (* Fill if the first var is not 0 *) match l with | [] -> Some (genDummyVar 0 nbVar s) | (i1, v1)::_ when i1 > 0 -> Some (genDummyVar 0 i1 s) | _ -> Some s - in let rec fill_after (l: (int * int) list) (nbVar: int) (shift: int): lexp S.subst option = (* Fill gaps *) + in let rec fill_after (l: (int * int) list) (nbVar: int) (shift: int): Lexp.subst option = (* Fill gaps *) match l with | (idx1, val1)::(idx2, val2)::tail when (idx1 = idx2) -> None

@@ -153,7 +153,7 @@ let is_identity s =

<code>s:S.subst, l:lexp, s':S.subst</code> where <code>l[s][s'] = l</code> and <code> inverse s = s' </code> *) -let inverse (s: lexp S.subst) : lexp S.subst option = +let inverse (s: Lexp.subst) : Lexp.subst option = let sort = List.sort (fun (ei1, _) (ei2, _) -> compare ei1 ei2) in match transfo s with | None -> None @@ -175,3 +175,136 @@ let inverse (s: lexp S.subst) : lexp S.subst option = ^ " !!\n")) | _ -> ()); res + +(* Returns false if the application of the inverse substitution is not + * possible. This happens when the substitution replaces some variables + * with non-variables, in which case the "inverse" is ambiguous. *) +let rec invertible (s: subst) : bool = match s with + | S.Identity -> true + | S.Shift (s, _) -> invertible s + | S.Cons (e, s) -> (match e with Var _ -> true | _ -> e = impossible) + && invertible s + +exception Not_invertible +exception Ambiguous + +(* Lookup variable i in s⁻¹ *) +let rec lookup_inv_subst (i : db_index) (s : subst) : db_index + = match s with + | S.Identity -> i + | S.Shift (s, n) -> if i < n then + raise Not_invertible + else lookup_inv_subst (i - n) s + | S.Cons (Var (_, i'), s) when i' = i + -> (try let i'' = lookup_inv_subst i s in + assert (i'' != 0); + raise Ambiguous + with Not_invertible -> 0) + | S.Cons (e, s) + -> assert (match e with Var _ -> true | _ -> e = impossible); + 1 + lookup_inv_subst i s + +(* When going under a binder, we have the rule + * (λe)[s] ==> λ(e[lift s]) + * where `lift s` is (#0 · (s ↑1)) + * + * Here, we want to construct a substitution s' such that + * + * (λe)[s⁻¹] ==> λ(e[s'⁻¹]) + * + * So (lift_inv_subst s) is morally equivalent to ((lift (s⁻¹))⁻¹). + * And it turns out that ((lift (s⁻¹))⁻¹) = lift s: + *) + +(* Return a substitution s' = (↑n ∘ (s⁻¹))⁻¹ = ((s⁻¹)⁻¹ ∘ (↑n)⁻¹) = (s ∘ (↑n)⁻¹) + * ↑n is a substitution of type Γ → Γ,x₁,…,xₙ + * So `s⁻¹` should be a substitution Γ,x₁,…,xₙ → Γ' + * Hence `s` should be a substitution Γ' → Γ,x₁,…,xₙ + * and we need to return a substitution Γ' → Γ + *) +let shift_inv_subst n s + (* We could define it as: + * = compose_inv_subst s (S.shift n) + * But this can fail if an element of `s` maps to a var with index < n *) + = let shift_n = match inverse (S.shift n) with + | Some s -> s + | _ -> assert (false) in + Lexp.scompose s shift_n + +(* For metavars, we need to compute: s' ∘ s⁻¹ + * One way to do it is to compute s⁻¹ and then pass it to `compose`. + * But we can try and do it more directly. + *) +let rec compose_inv_subst (s' : subst) (s : subst) = match s' with + | S.Cons (e, s') -> S.Cons (apply_inv_subst e s, compose_inv_subst s' s) + | S.Identity -> (match inverse s with + | Some s -> s + (* FIXME: could also be Ambiguous, depending on `s`. *) + | None -> raise Not_invertible) + | S.Shift (s', n) + -> compose_inv_subst s' (shift_inv_subst n s) + +(* Apply s⁻¹ to e. + * The function presumes that `invertible s` was true. + * This can be used like mkSusp/push_susp, but it's not lazy. + * This is because it can signal errors Not_invertible or Ambiguous. *) +and apply_inv_subst (e : lexp) (s : subst) : lexp = match e with + | Imm _ -> e + | SortLevel (SLz) -> e + | SortLevel (SLsucc e) -> mkSortLevel (SLsucc (apply_inv_subst e s)) + | SortLevel (SLlub (e1, e2)) + -> mkSortLevel (SLlub (apply_inv_subst e1 s, apply_inv_subst e2 s)) + | Sort (l, Stype e) -> mkSort (l, Stype (apply_inv_subst e s)) + | Sort (l, (StypeOmega | StypeLevel)) -> e + | Builtin _ -> e + | Var (name, i) -> Lexp.mkVar (name, lookup_inv_subst i s) + | Susp (e, s') -> apply_inv_subst (push_susp e s') s + | Let (l, defs, e) + -> let s' = L.fold_left (fun s (v, _, _) -> ssink v s) s defs in + let (_,ndefs) + = L.fold_left (fun (s,ndefs) (v, def, ty) + -> (ssink v s, + (v, apply_inv_subst def s', apply_inv_subst ty s) + :: ndefs)) + (s, []) defs in + mkLet (l, ndefs, apply_inv_subst e s') + | Arrow (ak, v, t1, l, t2) + -> mkArrow (ak, v, apply_inv_subst t1 s, l, + apply_inv_subst t2 (ssink (maybev v) s)) + | Lambda (ak, v, t, e) + -> mkLambda (ak, v, apply_inv_subst t s, apply_inv_subst e (ssink v s)) + | Call (f, args) + -> mkCall (apply_inv_subst f s, + L.map (fun (ak, arg) -> (ak, apply_inv_subst arg s)) args) + | Inductive (l, label, args, cases) + -> let (s, nargs) + = L.fold_left (fun (s, nargs) (ak, v, t) + -> (ssink v s, (ak, v, apply_inv_subst t s) :: nargs)) + (s, []) args in + let nargs = List.rev nargs in + let ncases = SMap.map (fun args + -> let (_, ncase) + = L.fold_left (fun (s, nargs) (ak, v, t) + -> (ssink (maybev v) s, + (ak, v, apply_inv_subst t s) + :: nargs)) + (s, []) args in + L.rev ncase) + cases in + mkInductive (l, label, nargs, ncases) + | Cons (it, name) -> Cons (apply_inv_subst it s, name) + | Case (l, e, ret, cases, default) + -> mkCase (l, apply_inv_subst e s, apply_inv_subst ret s, + SMap.map (fun (l, cargs, e) + -> let s' = L.fold_left + (fun s (_,ov) -> ssink (maybev ov) s) + s cargs in + (l, cargs, apply_inv_subst e s')) + cases, + match default with + | None -> default + | Some (v,e) -> Some (v, apply_inv_subst e (ssink (maybev v) s))) + | Metavar (id, s', name) + -> match metavar_lookup id with + | MVal e -> apply_inv_subst (push_susp e s') s + | MVar _ -> mkMetavar (id, compose_inv_subst s' s, name)

===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -36,6 +36,7 @@ module S = Subst

type vname = U.vname type vref = U.vref +type meta_id = int (* Identifier of a meta variable. *)

type label = symbol

@@ -81,7 +82,7 @@ type ltype = lexp * (vname option * lexp) option (* Default. *) (* The `subst` only applies to the lexp associated * with the metavar's "value", not to the ltype. *) - | Metavar of int * subst * vname + | Metavar of meta_id * subst * vname (* (* For logical metavars, there's no substitution. *) * | Metavar of (U.location * string) * metakind * metavar ref * and metavar = @@ -162,8 +163,8 @@ let impossible = Imm Sexp.dummy_epsilon let builtin_size = ref 0

let metavar_table = ref (U.IMap.empty : meta_subst) -let metavar_lookup idx : metavar_info - = try U.IMap.find idx (!metavar_table) +let metavar_lookup (id : meta_id) : metavar_info + = try U.IMap.find id (!metavar_table) with Not_found -> U.msg_fatal "LEXP" U.dummy_location "metavar lookup failure!"

===================================== src/opslexp.ml ===================================== --- a/src/opslexp.ml +++ b/src/opslexp.ml @@ -623,19 +623,23 @@ let rec list_union l1 l2 = match l1 with | [] -> l2 | (x::l1) -> list_union l1 (if List.mem x l2 then l2 else (x::l2))

-type mv_set = subst list IMap.t +type mv_set = (scope_level * ltype * scope_length * vname) IMap.t let mv_set_empty = IMap.empty -let mv_set_add ms m s - = let ss = try IMap.find m ms with Not_found -> [] in - if List.mem s ss then ms - else IMap.add m (s::ss) ms +let mv_set_add ms m x = IMap.add m x ms let mv_set_union : mv_set -> mv_set -> mv_set = IMap.merge (fun m oss1 oss2 -> match (oss1, oss2) with | (None, _) -> oss2 | (_, None) -> oss1 | (Some ss1, Some ss2) - -> Some (list_union ss1 ss2)) + -> (let ((sl1, t1, len1, (_, name1)), + (sl2, t2, len2, (_, name2))) + = (ss1, ss2) in + assert (sl1 = sl2); + assert (t1 = t2); + assert (len1 = len2); + assert (name2 = name1)); + Some ss1)

module LMap (* Memoization table. FIXME: Ideally the keys should be "weak", but @@ -702,12 +706,12 @@ let rec fv (e : lexp) : (DB.set * mv_set) = SMap.fold (fun _ (_, fields, e) s -> fv_union s (fv_hoist (List.length fields) (fv e))) cases s - | Metavar (m, s, _) + | Metavar (m, s, name) -> (match metavar_lookup m with | MVal e -> fv (push_susp e s) - | MVar (_, t, _) + | MVar (sl, t, cl) -> let (fvs, mvs) = fv (push_susp t s) in - (fvs, mv_set_add mvs m s)) + (fvs, mv_set_add mvs m (sl, t, cl, name))) in try LMap.find fv_memo e with Not_found

===================================== src/unification.ml ===================================== --- a/src/unification.ml +++ b/src/unification.ml @@ -162,23 +162,29 @@ and _unify_lambda (lambda: lexp) (lxp: lexp) ctx vs : return_type = *) and _unify_metavar ctx idx s (lxp1: lexp) (lxp2: lexp) : return_type = - let unif idx s lxp = match Inverse_subst.inverse s with - | None -> None - | Some s' - -> let t = match metavar_lookup idx with - | MVal _ -> U.internal_error - "`lexp_whnf` returned an instantiated metavar!!" - | MVar (_, t, _) -> push_susp t s in - metavar_table := associate idx (mkSusp lxp s') (!metavar_table); - match unify t (OL.get_type ctx lxp) ctx with - | Some [] as r -> r - (* FIXME: Let's ignore the error for now. *) - | _ - -> print_string ("Unification of metavar type failed:\n " - ^ lexp_string (Lexp.clean t) ^ " != " - ^ lexp_string (Lexp.clean (OL.get_type ctx lxp)) - ^ "\n" ^ "for " ^ lexp_string lxp ^ "\n"); - Some [] in + let unif idx s lxp = + let t = match metavar_lookup idx with + | MVal _ -> U.internal_error + "`lexp_whnf` returned an instantiated metavar!!" + | MVar (_, t, _) -> push_susp t s in + let lxp' = try Inverse_subst.apply_inv_subst lxp s with + | Inverse_subst.Not_invertible + -> print_string "Not_invertible:\n "; + lexp_print lxp; + print_string "\nAgainst:\n "; + print_string (subst_string s); + print_string "\n"; + lxp in + metavar_table := associate idx lxp' (!metavar_table); + match unify t (OL.get_type ctx lxp) ctx with + | Some [] as r -> r + (* FIXME: Let's ignore the error for now. *) + | _ + -> print_string ("Unification of metavar type failed:\n " + ^ lexp_string (Lexp.clean t) ^ " != " + ^ lexp_string (Lexp.clean (OL.get_type ctx lxp)) + ^ "\n" ^ "for " ^ lexp_string lxp ^ "\n"); + Some [] in match lxp2 with | Metavar (idx2, s2, _) -> if idx = idx2 then

View it on GitLab: https://gitlab.com/monnier/typer/commit/494d60dac1042a643bb6a4d99f3bd7e6469a...

--- View it on GitLab: https://gitlab.com/monnier/typer/commit/494d60dac1042a643bb6a4d99f3bd7e6469a... You're receiving this email because of your account on gitlab.com.