Stefan pushed to branch master at Stefan / Typer

Commits: c9eae130 by Stefan Monnier at 2017-07-29T22:43:16-04:00 * src/lexp.ml: Move the type info of metavars from lexp to metavar_info

(lexp): Don't carry the type of metavars any more. (scope_length): New type. (metavar_info): Rename MLevel to MVar and add type and ctx information.

- - - - -

5 changed files:

- src/elab.ml - src/lexp.ml - src/opslexp.ml - src/unification.ml - tests/unify_test.ml

Changes:

===================================== src/elab.ml ===================================== --- a/src/elab.ml +++ b/src/elab.ml @@ -232,22 +232,24 @@ let ctx_define_rec (ctx: elab_context) decls = * definitions. *)

-let newMetavar sl l name t = - let meta = Unif.create_metavar sl in - mkMetavar (meta, S.Identity, (l, name), t) +let newMetavar (ctx : lexp_context) sl l name t= + let meta = Unif.create_metavar ctx sl t in + mkMetavar (meta, S.Identity, (l, name))

-let newMetalevel sl = - newMetavar sl Util.dummy_location "l" type_level +let newMetalevel (ctx : elab_context) sl = + newMetavar (ectx_to_lctx ctx) sl Util.dummy_location "l" type_level

-let newMetatype sl loc - = newMetavar sl loc "t" (mkSort (loc, Stype (newMetalevel sl))) +let newMetatype (ctx : elab_context) sl loc + = newMetavar (ectx_to_lctx ctx) sl loc + "t" (mkSort (loc, Stype (newMetalevel ctx sl)))

(* Functions used when we need to return some lexp/ltype but * an error makes it impossible to return "the right one". *) -let mkDummy_type loc = newMetatype dummy_scope_level loc -let mkDummy_check loc t = newMetavar dummy_scope_level loc "dummy" t -let mkDummy_infer loc = - let t = newMetatype dummy_scope_level loc in (mkDummy_check loc t, t) +let mkDummy_type ctx loc = newMetatype ctx dummy_scope_level loc +let mkDummy_check ctx loc t = newMetavar (ectx_to_lctx ctx) dummy_scope_level + loc "dummy" t +let mkDummy_infer ctx loc = + let t = newMetatype ctx dummy_scope_level loc in (mkDummy_check ctx loc t, t)

let rec infer (p : sexp) (ctx : elab_context): lexp * ltype =

@@ -261,9 +263,9 @@ let rec infer (p : sexp) (ctx : elab_context): lexp * ltype = try SMap.find name (! BI.lmap) with Not_found -> sexp_error l ("Unknown builtin `" ^ name ^ "`"); - mkDummy_infer l + mkDummy_infer ctx l else (sexp_error l ("Invalid special identifier `" ^ name ^ "`"); - mkDummy_infer l) + mkDummy_infer ctx l)

(* Symbol i.e identifier. *) | Symbol (loc, name) @@ -278,7 +280,7 @@ let rec infer (p : sexp) (ctx : elab_context): lexp * ltype =

with Not_found -> (sexp_error loc ("The variable: `" ^ name ^ "` was not declared"); - mkDummy_infer loc)) + mkDummy_infer ctx loc))

| Node (se, []) -> infer se ctx

@@ -288,7 +290,8 @@ let rec infer (p : sexp) (ctx : elab_context): lexp * ltype = parse_special_form ctx f args None else if (OL.conv_p (ectx_to_lctx ctx) t (BI.get_predef "Macro" ctx)) then - let t = newMetatype (ectx_to_scope_level ctx) (sexp_location func) in + let t = newMetatype ctx (ectx_to_scope_level ctx) + (sexp_location func) in let lxp = handle_macro_call ctx f args t in (lxp, t) else @@ -296,7 +299,7 @@ let rec infer (p : sexp) (ctx : elab_context): lexp * ltype =

| Symbol (_, name) -> assert (String.length name >= 1 || String.get name 0 = '?'); - let t = newMetatype (ectx_to_scope_level ctx) (sexp_location p) in + let t = newMetatype ctx (ectx_to_scope_level ctx) (sexp_location p) in let lxp = check p t ctx in (lxp, t)

@@ -308,7 +311,7 @@ let rec infer (p : sexp) (ctx : elab_context): lexp * ltype = | Float _ -> DB.type_float | String _ -> DB.type_string; | _ -> sexp_error tloc "Could not find type"; - mkDummy_type tloc) + mkDummy_type ctx tloc)

and parse_special_form ctx f args ot = @@ -329,7 +332,7 @@ and parse_special_form ctx f args ot = (e, t))

| _ -> lexp_error loc f ("Unknown special-form: " ^ lexp_string f); - mkDummy_infer loc + mkDummy_infer ctx loc

(* Make up an argument of type `t` when none is provided. *) and get_implicit_arg ctx loc name t = @@ -362,7 +365,7 @@ and get_implicit_arg ctx loc name t =

(* Elaborate the argument *) check lsarg t ctx - | None -> newMetavar (ectx_to_scope_level ctx) loc name t + | None -> newMetavar (ectx_to_lctx ctx) (ectx_to_scope_level ctx) loc name t

(* Build the list of implicit arguments to instantiate. *) and instantiate_implicit e t ctx = @@ -391,7 +394,8 @@ and infer_type pexp ectx var = (* FIXME: Here we rule out TypeLevel/TypeOmega. *) match Unif.unify (mkSort (lexp_location s, - Stype (newMetalevel (ectx_to_scope_level ectx)))) + Stype (newMetalevel + ectx (ectx_to_scope_level ectx)))) s (ectx_to_lctx ectx) with | (None | Some (_::_)) @@ -411,26 +415,27 @@ and lexp_let_decls declss (body: lexp) ctx = List.fold_right (fun decls lxp -> mkLet (dloc, decls, lxp)) declss body

-and unify_with_arrow ctx tloc lxp kind var aty = - let body = newMetatype (ectx_to_scope_level ctx) tloc in - let arg = match aty with - | None -> newMetatype (ectx_to_scope_level ctx) tloc - | Some laty -> laty in - let l, _ = var in - let arrow = mkArrow (kind, Some 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 l, mkDummy_type l) - | Some ((t1,t2)::_) - -> lexp_error tloc lxp ("Types `" ^ lexp_string t1 - ^ " and " - ^ lexp_string t2 - ^ " do not match"); - (mkDummy_type l, mkDummy_type l) - | Some [] -> arg, body +and unify_with_arrow ctx tloc lxp kind var aty + = let arg = match aty with + | None -> newMetatype ctx (ectx_to_scope_level ctx) tloc + | Some laty -> laty in + let nctx = ectx_extend ctx (Some var) Variable arg in + let body = newMetatype nctx (ectx_to_scope_level ctx) tloc in + let (l, _) = var in + let arrow = mkArrow (kind, Some 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)::_) + -> lexp_error tloc lxp ("Types `" ^ lexp_string t1 + ^ " and " + ^ lexp_string t2 + ^ " do not match"); + (mkDummy_type ctx l, mkDummy_type nctx l) + | Some [] -> arg, body

and check (p : sexp) (t : ltype) (ctx : elab_context): lexp =

@@ -456,10 +461,15 @@ and check (p : sexp) (t : ltype) (ctx : elab_context): lexp = (* 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 - * can refer `t` or not. If the user wants ? to be able to refer to - * `t`, then she should explicitly write (y : ? t). *) - mkSusp (newMetavar (ectx_to_scope_level ctx) l name t) - (S.shift (ectx_local_scope_size ctx)) + * can refer to `t` or not. If the user wants ? to be able to refer + * to `t`, then she should explicitly write (y : ? t). *) + let ctx_shift = ectx_local_scope_size ctx in + let octx = Myers.nthcdr ctx_shift (ectx_to_lctx ctx) in + (* FIXME: `t` is defined in ctx instead of octx. + * We need something like: + * let t = push_inv_subst t (S.shift ctx_shift) in *) + mkSusp (newMetavar octx (ectx_to_scope_level ctx) l name t) + (S.shift ctx_shift)

| _ -> infer_and_check p ctx t

@@ -1013,14 +1023,15 @@ and get_attribute ctx loc largs = try Some (AttributeMap.find var map) with Not_found -> None

-and sform_dummy_ret loc = - let t = newMetatype dummy_scope_level loc in - (newMetavar dummy_scope_level loc "special-form-error" t, Inferred t) +and sform_dummy_ret ctx loc = + let t = newMetatype ctx dummy_scope_level loc in + (newMetavar (ectx_to_lctx ctx) dummy_scope_level loc "special-form-error" t, + Inferred t)

and sform_get_attribute ctx loc (sargs : sexp list) ot = match get_attribute ctx loc (List.map (lexp_parse_sexp ctx) sargs) with | Some e -> (e, Lazy) - | None -> sexp_error loc "No attribute found"; sform_dummy_ret loc + | None -> sexp_error loc "No attribute found"; sform_dummy_ret ctx loc

and sform_has_attribute ctx loc (sargs : sexp list) ot = let n = get_size ctx in @@ -1041,9 +1052,9 @@ and sform_declexpr ctx loc sargs ot = -> (match DB.env_lookup_expr ctx ((loc, vn), vi) with | Some lxp -> (lxp, Lazy) | None -> error loc "no expr available"; - sform_dummy_ret loc) + sform_dummy_ret ctx loc) | _ -> error loc "declexpr expects one argument"; - sform_dummy_ret loc + sform_dummy_ret ctx loc

let sform_decltype ctx loc sargs ot = @@ -1051,7 +1062,7 @@ let sform_decltype ctx loc sargs ot = | [Var((_, vn), vi)] -> (DB.env_lookup_type ctx ((loc, vn), vi), Lazy) | _ -> error loc "decltype expects one argument"; - sform_dummy_ret loc + sform_dummy_ret ctx loc

let builtin_value_types : ltype option SMap.t ref = ref SMap.empty

@@ -1067,10 +1078,10 @@ let sform_built_in ctx loc sargs ot = (bi, Inferred ltp')

| true, _ -> error loc "Wrong Usage of `Built-in`"; - sform_dummy_ret loc + sform_dummy_ret ctx loc

| false, _ -> error loc "Use of `Built-in` in user code"; - sform_dummy_ret loc + sform_dummy_ret ctx loc

let sform_datacons ctx loc sargs ot = match sargs with @@ -1079,13 +1090,13 @@ let sform_datacons ctx loc sargs ot = (mkCons (idt, sym), Lazy)

| [_;_] -> sexp_error loc "Second arg of ##constr should be a symbol"; - sform_dummy_ret loc + sform_dummy_ret ctx loc | _ -> sexp_error loc "##constr requires two arguments"; - sform_dummy_ret loc + sform_dummy_ret ctx loc

let sform_typecons ctx loc sargs ot = match sargs with - | [] -> sexp_error loc "No arg to ##typecons!"; (mkDummy_type loc, Lazy) + | [] -> sexp_error loc "No arg to ##typecons!"; (mkDummy_type ctx loc, Lazy) | formals :: constrs -> let (label, formals) = match formals with | Node (label, formals) -> (label, formals) @@ -1103,7 +1114,7 @@ let sform_typecons ctx loc sargs ot = let ltp = match opxp with | Some pxp -> let (l,_) = infer pxp ctx in l | None -> let (l,_) = var in - newMetatype (ectx_to_scope_level ctx) l in + newMetatype ctx (ectx_to_scope_level ctx) l in

parse_formals sformals ((kind, var, ltp) :: rformals) (env_extend ctx var Variable ltp) in @@ -1134,7 +1145,7 @@ let sform_hastype ctx loc sargs ot = let le = check se lt ctx in (le, Inferred lt) | _ -> sexp_error loc "##_:_ takes two arguments"; - sform_dummy_ret loc + sform_dummy_ret ctx loc

let sform_arrow kind ctx loc sargs ot = match sargs with @@ -1147,7 +1158,7 @@ let sform_arrow kind ctx loc sargs ot = let lt2 = infer_type st2 nctx None in (mkArrow (kind, v, lt1, loc, lt2), Lazy) | _ -> sexp_error loc "##_->_ takes two arguments"; - sform_dummy_ret loc + sform_dummy_ret ctx loc

(* Infer or check, as the case may be. *) let elaborate ctx pe ot = @@ -1187,7 +1198,7 @@ let rec sform_lambda kind ctx loc sargs ot = (match ot with | None -> mklam (match olt1 with | Some lt1 -> lt1 - | None -> newMetatype (ectx_to_scope_level ctx) loc) + | None -> newMetatype ctx (ectx_to_scope_level ctx) loc) None (* Read var type from the provided type *) | Some t @@ -1225,7 +1236,7 @@ let rec sform_lambda kind ctx loc sargs ot = | Aimplicit -> "=>" | Aerasable -> "≡>") ^"_ takes two arguments"); - sform_dummy_ret loc + sform_dummy_ret ctx loc

let rec sform_case ctx loc sargs ot = match sargs with | [Node (Symbol (_, "_|_"), se :: scases)] @@ -1236,15 +1247,16 @@ let rec sform_case ctx loc sargs ot = match sargs with sexp_error l "Unrecognized simple case branch"; (Ppatany l, Symbol (l, "?")) in let pcases = List.map parse_case scases in - let t = match ot with Some t -> t - | None -> newMetatype (ectx_to_scope_level ctx) loc in + let t = match ot with + | Some t -> t + | None -> newMetatype ctx (ectx_to_scope_level ctx) loc in let le = check_case t (loc, se, pcases) ctx in (le, match ot with Some _ -> Checked | None -> Inferred t)

(* In case there are no branches, pretend there was a | anyway. *) | [e] -> sform_case ctx loc [Node (Symbol (loc, "_|_"), sargs)] ot | _ -> sexp_error loc "Unrecognized case expression"; - sform_dummy_ret loc + sform_dummy_ret ctx loc

let sform_letin ctx loc sargs ot = match sargs with | [sdecls; sbody] @@ -1255,7 +1267,7 @@ let sform_letin ctx loc sargs ot = match sargs with (lexp_let_decls declss bdy nctx, Inferred (mkSusp ltp s)) | _ -> sexp_error loc "Unrecognized let_in_ expression"; - sform_dummy_ret loc + sform_dummy_ret ctx loc

(* Actually `Type_` could also be defined as a plain constant * Lambda("l", TypeLevel, Sort (Stype (Var "l"))) @@ -1269,7 +1281,7 @@ let sform_type ctx loc sargs ot = (mkSort (loc, Stype l), Inferred (mkSort (loc, Stype (SortLevel (SLsucc l))))) | _ -> sexp_error loc "##Type_ expects one argument"; - sform_dummy_ret loc + sform_dummy_ret ctx loc

(* Only print var info *) and lexp_print_var_info ctx =

===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -81,7 +81,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 * ltype + | Metavar of int * subst * vname (* (* For logical metavars, there's no substitution. *) * | Metavar of (U.location * string) * metakind * metavar ref * and metavar = @@ -143,10 +143,16 @@ type varbind = * The lctx_length keeps track of the lctx's length when that scope level was * entered in order to know by how much to shift metavars. *) type scope_level = int +type scope_length = int

type metavar_info = | MVal of lexp (* Exp to which the var is instantiated. *) - | MLevel of scope_level (* Outermost scope in which the var appears. *) + | MVar of scope_level (* Outermost scope in which the var appears. *) + * ltype (* Expected type. *) + (* We'd like to keep the lexp_content in which the type is to be + * understood, but lexp_context is not yet defined here, + * so we just keep the length of the lexp_context. *) + * scope_length type meta_subst = metavar_info U.IMap.t type constraints = (lexp * lexp) list

@@ -191,7 +197,7 @@ let mkLambda (k, v, t, e) = hc (Lambda (k, v, t, e)) let mkInductive (l, n, a, cs) = hc (Inductive (l, n, a, cs)) let mkCons (t, n) = hc (Cons (t, n)) let mkCase (l, e, rt, bs, d) = hc (Case (l, e, rt, bs, d)) -let mkMetavar (n, s, v, t) = hc (Metavar (n, s, v, t)) +let mkMetavar (n, s, v) = hc (Metavar (n, s, v)) let mkCall (f, es) = match f, es with | Call (f', es'), _ -> hc (Call (f', es' @ es)) @@ -214,7 +220,7 @@ let rec mkSusp e s = | Builtin _ -> e | Susp (e, s') -> mkSusp e (scompose s' s) | Var (l,v) -> slookup s l v - | Metavar (vn, s', vd, t) -> mkMetavar (vn, scompose s' s, vd, mkSusp t s) + | Metavar (vn, s', vd) -> mkMetavar (vn, scompose s' s, vd) | _ -> hc (Susp (e, s)) and scompose s1 s2 = S.compose mkSusp s1 s2 and slookup s l v = S.lookup (fun l i -> mkVar (l, i)) @@ -241,7 +247,7 @@ let rec lexp_location e = | Case (l,_,_,_,_) -> l | Susp (e, _) -> lexp_location e (* | Susp (_, e) -> lexp_location e *) - | Metavar (_,_,(l,_), _) -> l + | Metavar (_,_,(l,_)) -> l

(********* Normalizing a term *********) @@ -365,11 +371,11 @@ let clean e = | Susp (e, s') -> clean (scompose s' s) e | Var _ -> if S.identity_p s then e else clean S.identity (mkSusp e s) - | Metavar (idx, s', name, t) + | Metavar (idx, s', name) -> let s = scompose s' s in match metavar_lookup idx with | MVal e -> clean s e - | _ -> mkMetavar (idx, s, name, t) + | _ -> mkMetavar (idx, s, name) in clean S.identity e

let sdatacons = Symbol (U.dummy_location, "##datacons") @@ -479,7 +485,7 @@ let rec lexp_unparse lxp = pbranch)

(* FIXME: The cases below are all broken! *) - | Metavar (idx, subst, (loc, name), _) + | Metavar (idx, subst, (loc, name)) -> Symbol (loc, "?" ^ name ^ "-" ^ string_of_int idx ^ "[" ^ subst_string subst ^ "]")

@@ -690,17 +696,17 @@ and _lexp_str ctx (exp : lexp) : string =

| Var ((loc, name), idx) -> name ^ (index idx) ;

- | Metavar (idx, subst, (loc, name), _) ->( + | Metavar (idx, subst, (loc, name)) (* print metavar result if any *) - let print_meta exp = - let ctx = set_meta exp ctx in - _lexp_str ctx (clean exp) in + -> (let print_meta exp = + let ctx = set_meta exp ctx in + _lexp_str ctx (clean exp) in

- match pp_meta ctx with - | None -> print_meta exp - | Some e when e != exp -> print_meta exp - | _ -> - "?" ^ name ^ (subst_string subst) ^ (index idx)) + match pp_meta ctx with + | None -> print_meta exp + | Some e when e != exp -> print_meta exp + | _ -> + "?" ^ name ^ (subst_string subst) ^ (index idx))

| Let (_, decls, body) -> (* Print first decls without indent *) @@ -882,8 +888,8 @@ let rec eq e1 e2 = && (match (def1, def2) with | (Some (_, e1), Some (_, e2)) -> eq e1 e2 | _ -> def1 = def2) - | (Metavar (i1, s1, _, t1), Metavar (i2, s2, _, t2)) - -> i1 = i2 && eq t1 t2 && subst_eq s1 s2 + | (Metavar (i1, s1, _), Metavar (i2, s2, _)) + -> i1 = i2 && subst_eq s1 s2 | _ -> false

and subst_eq s1 s2 =

===================================== src/opslexp.ml ===================================== --- a/src/opslexp.ml +++ b/src/opslexp.ml @@ -173,7 +173,7 @@ let lexp_whnf e (ctx : DB.lexp_context) : lexp = | Cons (_, (_, name)) -> reduce name [] | Call (Cons (_, (_, name)), aargs) -> reduce name aargs | _ -> mkCase (l, e, rt, branches, default)) - | Metavar (idx, s, _, _) + | Metavar (idx, s, _) -> (match metavar_lookup idx with | MVal e -> lexp_whnf (push_susp e s) ctx | _ -> e) @@ -308,7 +308,7 @@ let level_canon e = | 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, _, _) + | Metavar (i, s, _) -> (match metavar_lookup i with | MVal e -> canon (push_susp e s) d acc | _ -> add_var_depth (- i) d acc) @@ -608,13 +608,11 @@ let rec check' erased ctx e = ("Cons of a non-inductive type: " ^ lexp_string t); DB.type_int)) - | Metavar (idx, s, _, t) + | Metavar (idx, s, _) -> (match metavar_lookup idx with | MVal e -> let e = push_susp e s in - let t' = check erased ctx e in - assert_type ctx e t' t - | _ -> ()); - t + check erased ctx e + | MVar (_, t, _) -> push_susp t s)

let check = check' DB.set_empty

@@ -703,9 +701,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, _, t) - -> let (fvs, mvs) = fv t in - (fvs, mv_set_add mvs m s) + | Metavar (m, s, _) + -> (match metavar_lookup m with + | MVal e -> fv (push_susp e s) + | MVar (_, t, _) + -> let (fvs, mvs) = fv (push_susp t s) in + (fvs, mv_set_add mvs m s)) in try LMap.find fv_memo e with Not_found @@ -818,7 +819,10 @@ let rec get_type ctx e = buildtype fargs with Not_found -> DB.type_int) | _ -> DB.type_int) - | Metavar (idx, s, _, t) -> t + | Metavar (idx, s, _) + -> (match metavar_lookup idx with + | MVal e -> get_type ctx (push_susp e s) + | MVar (_, t, _) -> push_susp t s)

(*********** Type erasure, before evaluation. *****************)

===================================== src/unification.ml ===================================== --- a/src/unification.ml +++ b/src/unification.ml @@ -36,10 +36,11 @@ module DB = Debruijn (* :-( *) let global_last_metavar = ref (-1) (*The first metavar is 0*)

-let create_metavar (sl : scope_level) +let create_metavar (ctx : DB.lexp_context) (sl : scope_level) (t : ltype) = let idx = !global_last_metavar + 1 in global_last_metavar := idx; - metavar_table := U.IMap.add idx (MLevel sl) (!metavar_table); + metavar_table := U.IMap.add idx (MVar (sl, t, Myers.length ctx)) + (!metavar_table); idx

(* For convenience *) @@ -89,8 +90,8 @@ and unify' (e1: lexp) (e2: lexp) | ((Imm _, Imm _) | (Cons _, Cons _) | (Builtin _, Builtin _) | (Var _, Var _) | (Inductive _, Inductive _)) -> if OL.conv_p ctx e1' e2' then Some [] else None - | (l, (Metavar (idx, s, _, t) as r)) -> _unify_metavar ctx idx s t r l - | ((Metavar (idx, s, _, t) as l), r) -> _unify_metavar ctx idx s t l r + | (l, (Metavar (idx, s, _) as r)) -> _unify_metavar ctx idx s r l + | ((Metavar (idx, s, _) as l), r) -> _unify_metavar ctx idx s l r | (l, (Call _ as r)) -> _unify_call r l ctx vs' (* | (l, (Case _ as r)) -> _unify_case r l subst *) | (Arrow _ as l, r) -> _unify_arrow l r ctx vs' @@ -159,12 +160,16 @@ 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 t (lxp1: lexp) (lxp2: lexp) +and _unify_metavar ctx idx s (lxp1: lexp) (lxp2: lexp) : return_type = - let unif idx s t lxp = match Inverse_subst.inverse s with + let unif idx s lxp = match Inverse_subst.inverse s with | None -> None | Some s' - -> metavar_table := associate idx (mkSusp lxp s') (!metavar_table); + -> 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. *) @@ -175,20 +180,20 @@ and _unify_metavar ctx idx s t (lxp1: lexp) (lxp2: lexp) ^ "\n" ^ "for " ^ lexp_string lxp ^ "\n"); Some [] in match lxp2 with - | Metavar (idx2, s2, _, t2) + | 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 t lxp2 with + (match unif idx s lxp2 with | Some s -> Some s | None -> - match unif idx2 s2 t2 lxp1 with + match unif idx2 s2 lxp1 with | Some s -> Some s | None -> None) - | _ -> unif idx s t lxp2 + | _ -> unif idx s lxp2

(** Unify a Call (call) and a lexp (lxp) - Call , Call -> UNIFY

===================================== tests/unify_test.ml ===================================== --- a/tests/unify_test.ml +++ b/tests/unify_test.ml @@ -183,7 +183,7 @@ let generate_testable (_: lexp list) : ((lexp * lexp * result) list) =

::(input_type , input_type_t , Equivalent) (* 44 *)

- ::(Metavar (0, S.Identity, (Util.dummy_location, "M"), DB.type0), + ::(Metavar (0, S.Identity, (Util.dummy_location, "M")), Var ((Util.dummy_location, "x"), 3), Unification) (* 45 *)

::[]

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

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