Stefan pushed to branch master at Stefan / Typer

Commits: 1fd2d612 by Stefan Monnier at 2016-12-19T13:34:24-05:00 * src/opslexp.ml (check'): Check Metavar's type annotation.

* src/opslexp.ml (conv_p'): Add partial support for SortLevel's SLlub.

* src/lparse.ml (newMetalevel, newMetatype): Fix thinko's. (lexp_decls_macro): Use pexp_p_decls.

* src/unification.ml (_unify_metavar): Also unify the var's type. Furthermore, when unifying two metavars, try it both ways.

- - - - -

3 changed files:

- src/lparse.ml - src/opslexp.ml - src/unification.ml

Changes:

===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -238,9 +238,9 @@ let newMetavar l name t = mkMetavar (meta, S.Identity, (l, name), t)

let newMetalevel () = - newMetavar Util.dummy_location "l" (mkSort (dummy_location, StypeLevel)) + newMetavar Util.dummy_location "l" type_level

-let newMetatype loc = newMetavar loc "t" (newMetalevel ()) +let newMetatype loc = newMetavar loc "t" (mkSort (loc, Stype (newMetalevel ())))

(* Functions used when we need to return some lexp/ltype but * an error makes it impossible to return "the right one". *) @@ -901,7 +901,7 @@ and lexp_decls_macro (loc, mname) sargs ctx: (pdecl list * elab_context) = | _ -> fatal loc ("Macro `" ^ mname ^ "` should return a sexp") in

(* read as pexp_declaraton *) - (try pexp_decls_all [decls], ctx + (try pexp_p_decls decls, ctx (* if an error occur print generated code to ease debugging *) with e -> error loc "An error occurred while expanding a macro";

===================================== src/opslexp.ml ===================================== --- a/src/opslexp.ml +++ b/src/opslexp.ml @@ -224,7 +224,17 @@ let rec conv_p' meta_ctx (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = | (Imm (Integer (_, i1)), Imm (Integer (_, i2))) -> i1 = i2 | (Imm (Float (_, i1)), Imm (Float (_, i2))) -> i1 = i2 | (Imm (String (_, i1)), Imm (String (_, i2))) -> i1 = i2 - | (SortLevel sl1, SortLevel sl2) -> sl1 = sl2 + | (SortLevel sl1, SortLevel sl2) + -> (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) | (Sort (_, s1), Sort (_, s2)) -> s1 == s2 || (match (s1, s2) with @@ -342,8 +352,9 @@ let rec check' meta_ctx erased ctx e = if conv_p meta_ctx ctx t t' then () else (U.msg_error "TC" (lexp_location e) ("Type mismatch for " - ^ lexp_string e ^ " : " - ^ lexp_string t ^ " != " ^ lexp_string t'); + ^ lexp_string (L.clean meta_ctx e) ^ " : " + ^ lexp_string (L.clean meta_ctx t) ^ " != " + ^ lexp_string (L.clean meta_ctx t')); (* U.internal_error "Type mismatch" *)) in let check_type erased ctx t = let s = check erased ctx t in @@ -589,8 +600,11 @@ let rec check' meta_ctx erased ctx e = ^ lexp_string t); DB.type_int)) | Metavar (idx, s, _, t) - -> try check erased ctx (push_susp (L.VMap.find idx meta_ctx) s) - with Not_found -> t + -> (try let e = push_susp (L.VMap.find idx meta_ctx) s in + let t' = check erased ctx e in + assert_type ctx e t' t + with Not_found -> ()); + t

let check meta_ctx = check' meta_ctx DB.set_empty

===================================== src/unification.ml ===================================== --- a/src/unification.ml +++ b/src/unification.ml @@ -98,12 +98,12 @@ and unify' (e1: lexp) (e2: lexp) | ((Imm _, Imm _) | (Cons _, Cons _) | (Builtin _, Builtin _) | (Var _, Var _) | (Inductive _, Inductive _)) -> if OL.conv_p subst ctx e1' e2' then Some (subst, []) else None - | (l, (Metavar _ as r)) -> _unify_metavar r l subst + | (l, (Metavar (idx, s, _, t) as r)) -> _unify_metavar subst ctx idx s t r l + | ((Metavar (idx, s, _, t) as l), r) -> _unify_metavar subst ctx idx s t l r | (l, (Call _ as r)) -> _unify_call r l ctx vs' subst (* | (l, (Case _ as r)) -> _unify_case r l subst *) | (Arrow _ as l, r) -> _unify_arrow l r ctx vs' subst | (Lambda _ as l, r) -> _unify_lambda l r ctx vs' subst - | (Metavar _ as l, r) -> _unify_metavar l r subst | (Call _ as l, r) -> _unify_call l r ctx vs' subst (* | (Case _ as l, r) -> _unify_case l r subst *) (* | (Inductive _ as l, r) -> _unify_induct l r subst *) @@ -169,22 +169,36 @@ and _unify_lambda (lambda: lexp) (lxp: lexp) ctx vs (subst: meta_subst) : return - metavar , metavar -> if Metavar = Metavar then OK else ERROR - metavar , lexp -> OK *) -and _unify_metavar (meta: lexp) (lxp: lexp) (subst: meta_subst) : return_type = - let find_or_unify metavar value lxp s = - match find_or_none metavar s with - | Some (lxp_) -> assert false - | None -> (match metavar with - | Metavar (_, subst_, _, _) -> (match Inverse_subst.inverse subst_ with - | Some s' -> Some (associate value (mkSusp lxp s') s, []) +and _unify_metavar (subst: meta_subst) ctx idx s t (lxp1: lexp) (lxp2: lexp) + : return_type = + let unif idx s t lxp = match Inverse_subst.inverse s with + | None -> None + | Some s' + -> let subst = associate idx (mkSusp lxp s') subst in + match unify t (OL.get_type subst ctx lxp) ctx subst with + | Some (subst, []) as r -> r + (* FIXME: Let's ignore the error for now. *) + | _ + -> print_string ("Unification of metavar type failed:\n " + ^ lexp_string (Lexp.clean subst t) ^ " != " + ^ lexp_string (Lexp.clean subst (OL.get_type subst ctx lxp)) ^ "\n" + ^ "for " ^ lexp_string lxp ^ "\n"); + Some (subst, []) in + match lxp2 with + | Metavar (idx2, s2, _, t2) + -> if idx = idx2 then + (* FIXME: handle the case where s1 != s2 !! *) + Some ((subst, [])) + 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 + | Some s -> Some s + | None -> + match unif idx2 s2 t2 lxp1 with + | Some s -> Some s | None -> None) - | _ -> None) - in - match (meta, lxp) with - | (Metavar (val1, s1, _, _), Metavar (val2, s2, _, _)) when val1 = val2 - (* FIXME: handle the case where s1 != s2 !! *) - -> Some ((subst, [])) - | (Metavar (v, s1, _, _), _) -> find_or_unify meta v lxp subst - | (_, _) -> None + | _ -> unif idx s t lxp2

(** Unify a Call (call) and a lexp (lxp) - Call , Call -> UNIFY @@ -267,6 +281,7 @@ and _unify_sortlvl (sortlvl: lexp) (lxp: lexp) ctx vs (subst: meta_subst) : retu | (SortLevel s, SortLevel s2) -> (match s, s2 with | SLz, SLz -> Some (subst, []) | SLsucc l1, SLsucc l2 -> unify' l1 l2 ctx vs subst + (* FIXME: Handle SLsub! *) | _, _ -> None) | _, _ -> None

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