Stefan pushed to branch master at Stefan / Typer

Commits: fd033066 by Stefan Monnier at 2017-07-27T14:26:38-04:00 Don't pass meta_ctx as arg any more

Push the rest of last change, missed in last commit!

- - - - -

9 changed files:

- src/REPL.ml - src/builtin.ml - src/debug_util.ml - src/elab.ml - src/eval.ml - src/lexp.ml - src/opslexp.ml - src/unification.ml - tests/unify_test.ml

Changes:

===================================== src/REPL.ml ===================================== --- a/src/REPL.ml +++ b/src/REPL.ml @@ -132,8 +132,7 @@ let ilexp_parse pexps lctx: ((ldecl list list * lexpr list) * elab_context) = let pdecls, pexprs = pexps in let ldecls, lctx = Elab.lexp_p_decls pdecls lctx in let lexprs = Elab.lexp_parse_all pexprs lctx in - let meta_ctx, _ = !global_substitution in - List.iter (fun lxp -> ignore (OL.check meta_ctx (ectx_to_lctx lctx) lxp)) + List.iter (fun lxp -> ignore (OL.check (ectx_to_lctx lctx) lxp)) lexprs; (ldecls, lexprs), lctx

===================================== src/builtin.ml ===================================== --- a/src/builtin.ml +++ b/src/builtin.ml @@ -140,7 +140,7 @@ let lmap = ref (SMap.empty : (lexp * ltype) SMap.t) let add_builtin_cst (name : string) (e : lexp) = let map = !lmap in assert (not (SMap.mem name map)); - let t = OL.check VMap.empty Myers.nil e in + let t = OL.check Myers.nil e in lmap := SMap.add name (e, t) map

let new_builtin_type name kind =

===================================== src/debug_util.ml ===================================== --- a/src/debug_util.ml +++ b/src/debug_util.ml @@ -296,7 +296,7 @@ let main () = let cctx = ectx_to_lctx ctx in (* run type check *) List.iter (fun (_, lxp, _) - -> let _ = OL.check VMap.empty cctx lxp in ()) + -> let _ = OL.check cctx lxp in ()) flexps;

print_string (" " ^ (make_line '-' 76));

===================================== src/elab.ml ===================================== --- a/src/elab.ml +++ b/src/elab.ml @@ -114,15 +114,14 @@ let get_special_form name = * to errors in the user's code). *)

let elab_check_sort (ctx : elab_context) lsort var ltp = - let meta_ctx, _ = !global_substitution in - match (try OL.lexp_whnf lsort (ectx_to_lctx ctx) meta_ctx + match (try OL.lexp_whnf lsort (ectx_to_lctx ctx) with e -> print_string "Exception during whnf of "; lexp_print lsort; print_string "\n"; raise e) with | Sort (_, _) -> () (* All clear! *) - | _ -> let lexp_string e = lexp_string (L.clean meta_ctx e) in + | _ -> let lexp_string e = lexp_string (L.clean e) in let typestr = lexp_string ltp ^ " : " ^ lexp_string lsort in match var with | None -> lexp_error (lexp_location ltp) ltp @@ -133,8 +132,7 @@ let elab_check_sort (ctx : elab_context) lsort var ltp = ^ typestr)

let elab_check_proper_type (ctx : elab_context) ltp var = - let meta_ctx, _ = !global_substitution in - try elab_check_sort ctx (OL.check meta_ctx (ectx_to_lctx ctx) ltp) var ltp + try elab_check_sort ctx (OL.check (ectx_to_lctx ctx) ltp) var ltp with e -> print_string "Exception while checking type `"; lexp_print ltp; (match var with @@ -148,14 +146,13 @@ let elab_check_def (ctx : elab_context) var lxp ltype = let lctx = ectx_to_lctx ctx in let loc = lexp_location lxp in

- let meta_ctx, _ = !global_substitution in - let lexp_string e = lexp_string (L.clean meta_ctx e) in - let ltype' = try OL.check meta_ctx lctx lxp + let lexp_string e = lexp_string (L.clean e) in + let ltype' = try OL.check lctx lxp with e -> lexp_error loc lxp "Error while type-checking"; print_lexp_ctx (ectx_to_lctx ctx); raise e in - if (try OL.conv_p meta_ctx (ectx_to_lctx ctx) ltype ltype' + if (try OL.conv_p (ectx_to_lctx ctx) ltype ltype' with e -> print_string ("Exception while conversion-checking types:\n"); lexp_print ltype; @@ -287,10 +284,9 @@ let rec infer (p : sexp) (ctx : elab_context): lexp * ltype =

| Node (func, args) -> let (f, t) as ft = infer func ctx in - let meta_ctx, _ = !global_substitution in - if (OL.conv_p meta_ctx (ectx_to_lctx ctx) t type_special_form) then + if (OL.conv_p (ectx_to_lctx ctx) t type_special_form) then parse_special_form ctx f args None - else if (OL.conv_p meta_ctx (ectx_to_lctx ctx) t + else if (OL.conv_p (ectx_to_lctx ctx) t (BI.get_predef "Macro" ctx)) then let t = newMetatype (sexp_location func) in let lxp = handle_macro_call ctx f args t in @@ -317,8 +313,7 @@ let rec infer (p : sexp) (ctx : elab_context): lexp * ltype =

and parse_special_form ctx f args ot = let loc = lexp_location f in - let meta_ctx, _ = !global_substitution in - match OL.lexp_whnf f (ectx_to_lctx ctx) meta_ctx with + match OL.lexp_whnf f (ectx_to_lctx ctx) with | Builtin ((_, name), _, _) -> (* Special form. *) let (e, ot') = (get_special_form name) ctx loc args ot in @@ -327,20 +322,21 @@ and parse_special_form ctx f args ot = | (Some t, Checked) -> (e, t) | _ -> let inferred_t = match ot' with | Inferred t -> t - | _ -> let meta_ctx, _ = !global_substitution in - OL.get_type meta_ctx (ectx_to_lctx ctx) e in + | _ -> OL.get_type (ectx_to_lctx ctx) e in match ot with | None -> (e, inferred_t) | Some t -> let e = check_inferred ctx e inferred_t t in (e, t))

| _ -> lexp_error loc f ("Unknown special-form: " ^ lexp_string f); - let t = newMetatype loc in - (newMetavar loc "<dummy>" t, t) + mkDummy_infer loc

(* Make up an argument of type `t` when none is provided. *) and get_implicit_arg ctx loc name t = (* lookup default attribute of t. *) + (* FIXME: Don't lookup defaults/tactics here. Instead, just always + * generate a metavar at this point. The use of defaults/tactics should be + * postponed, probably to just before we do HM-style generalization. *) match try (* FIXME: We shouldn't hard code as popular a name as `default`. *) let pidx, pname = (senv_lookup "default" ctx), "default" in @@ -370,9 +366,8 @@ and get_implicit_arg ctx loc name t =

(* Build the list of implicit arguments to instantiate. *) and instantiate_implicit e t ctx = - let (meta_ctx, _) = !global_substitution in let rec instantiate t args = - match OL.lexp_whnf t (ectx_to_lctx ctx) meta_ctx with + match OL.lexp_whnf t (ectx_to_lctx ctx) with | Arrow ((Aerasable | Aimplicit) as ak, v, t1, _, t2) -> let arg = get_implicit_arg ctx (lexp_location e) @@ -387,18 +382,18 @@ and infer_type pexp ectx var = * Sort (?s), but in most cases the metavar would be allocated * unnecessarily. *) let t, s = infer pexp ectx in - (let meta_ctx, _ = !global_substitution in - match OL.lexp_whnf s (ectx_to_lctx ectx) meta_ctx with + (match OL.lexp_whnf s (ectx_to_lctx ectx) with | Sort (_, _) -> () (* All clear! *) (* FIXME: We could automatically coerce Type levels to Sorts, so we * could write `(a : TypeLevel) -> a -> a` instead of * `(a : TypeLevel) -> Type_ a -> Type_ a` *) | _ -> (* FIXME: Here we rule out TypeLevel/TypeOmega. *) - match Unif.unify (mkSort (lexp_location s, Stype (newMetalevel ()))) s - (ectx_to_lctx ectx) meta_ctx with - | (None | Some (_, _::_)) - -> (let lexp_string e = lexp_string (L.clean meta_ctx e) in + match + Unif.unify (mkSort (lexp_location s, Stype (newMetalevel ()))) 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 | None -> lexp_error (lexp_location t) t @@ -407,7 +402,7 @@ and infer_type pexp ectx var = -> lexp_error l t ("Type of `" ^ name ^ "` is not a proper type: " ^ typestr)) - | Some subst -> global_substitution := subst); + | Some [] -> ()); t

and lexp_let_decls declss (body: lexp) ctx = @@ -421,20 +416,19 @@ and unify_with_arrow ctx tloc lxp kind var aty = | Some laty -> laty in let l, _ = var in let arrow = mkArrow (kind, Some var, arg, l, body) in - let meta_ctx, _ = !global_substitution in - match Unif.unify arrow lxp (ectx_to_lctx ctx) meta_ctx with + 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)::_) + | 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 subst -> global_substitution := subst; arg, body + | Some [] -> arg, body

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

@@ -443,10 +437,9 @@ and check (p : sexp) (t : ltype) (ctx : elab_context): lexp =

| Node (func, args) -> let (f, ft) = infer func ctx in - let meta_ctx, _ = !global_substitution in - if (OL.conv_p meta_ctx (ectx_to_lctx ctx) ft type_special_form) then + if (OL.conv_p (ectx_to_lctx ctx) ft type_special_form) then let (e, _) = parse_special_form ctx f args (Some t) in e - else if (OL.conv_p meta_ctx (ectx_to_lctx ctx) ft + else if (OL.conv_p (ectx_to_lctx ctx) ft (BI.get_predef "Macro" ctx)) then handle_macro_call ctx f args t else @@ -477,23 +470,22 @@ and infer_and_check pexp ctx t = * we use is to instantiate implicit arguments when needed, but we could/should * do lots of other things. *) and check_inferred ctx e inferred_t t = - let subst, _ = !global_substitution in - let (e, inferred_t) = match OL.lexp_whnf t (ectx_to_lctx ctx) subst with + let (e, inferred_t) = match OL.lexp_whnf t (ectx_to_lctx ctx) with | Arrow ((Aerasable | Aimplicit), _, _, _, _) -> (e, inferred_t) | _ -> instantiate_implicit e inferred_t ctx in - (match Unif.unify inferred_t t (ectx_to_lctx ctx) subst with + (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)::_) + | Some ((t1,t2)::_) -> lexp_error (lexp_location e) e ("Type mismatch! Context expected `" ^ lexp_string t2 ^ "` but expression has type `" ^ lexp_string t1 ^ "`") - | Some subst -> global_substitution := subst); + | Some [] -> ()); e

(* Lexp.case can sometimes be inferred, but we prefer to always check. *) @@ -512,15 +504,14 @@ and check_case rtype (loc, target, ppatterns) ctx =

(* get target and its type *) let tlxp, tltp = infer target ctx in - let meta_ctx, _ = !global_substitution 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) meta_ctx) with + 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) meta_ctx with + 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. *) @@ -546,16 +537,15 @@ and check_case rtype (loc, target, ppatterns) ctx = let add_branch pctor pargs = let loc = sexp_location pctor in let lctor, ct = infer pctor ctx in - let meta_ctx, _ = !global_substitution in - match OL.lexp_whnf lctor (ectx_to_lctx ctx) meta_ctx with + match OL.lexp_whnf lctor (ectx_to_lctx ctx) with | Cons (it', (_, cons_name)) - -> let _ = match Unif.unify it' it (ectx_to_lctx ctx) meta_ctx with - | (None | Some (_, _::_)) + -> 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 subst -> global_substitution := subst in + | Some [] -> () in let _ = check_uniqueness pat cons_name lbranches in let cargs = try SMap.find cons_name constructors @@ -637,9 +627,8 @@ and check_case rtype (loc, target, ppatterns) ctx = | Ppatany _ -> add_default None | Ppatsym ((_, name) as var) -> (try let idx = senv_lookup name ctx in - let meta_ctx, _ = !global_substitution in match OL.lexp_whnf (mkVar (var, idx)) - (ectx_to_lctx ctx) meta_ctx with + (ectx_to_lctx ctx) with | Cons _ (* It's indeed a constructor! *) -> add_branch (Symbol var) [] | _ -> add_default (Some var) (* A named default branch. *) @@ -671,8 +660,7 @@ and infer_call ctx (func, ltp) (sargs: sexp list) = * Anonymous : lambda *)

let rec handle_fun_args largs sargs pending ltp = - let meta_ctx, _ = !global_substitution in - let ltp' = OL.lexp_whnf ltp (ectx_to_lctx ctx) meta_ctx in + let ltp' = OL.lexp_whnf ltp (ectx_to_lctx ctx) in match sargs, ltp' with | _, Arrow (ak, Some (_, aname), arg_type, _, ret_type) when SMap.mem aname pending @@ -763,7 +751,7 @@ and lexp_parse_inductive ctors ctx = SMap.add name (make_args args ctx) lctors) SMap.empty ctors

-and track_fv meta_ctx rctx lctx e = +and track_fv rctx lctx e = let (fvs, mvs) = OL.fv e in let nc = EV.not_closed rctx fvs in if nc = [] && not (VMap.is_empty mvs) then @@ -781,24 +769,22 @@ and track_fv meta_ctx rctx lctx e = "somevars[" ^ string_of_int i ^ "-" ^ string_of_int o ^ "]" else name ^ " (" - ^ track_fv meta_ctx - (Myers.nthcdr drop rctx) + ^ track_fv (Myers.nthcdr drop rctx) (Myers.nthcdr drop lctx) - (L.clean meta_ctx e) + (L.clean e) ^ ")" | _ -> name in String.concat " " (List.map tfv nc)

-and lexp_eval meta_ctx ectx e = - (* FIXME: Make erase_type take meta_ctx directly! *) - let e = L.clean meta_ctx e in +and lexp_eval ectx e = + let e = L.clean e in let ee = OL.erase_type e in - let rctx = EV.from_ectx meta_ctx ectx in + let rctx = EV.from_ectx ectx in

if not (EV.closed_p rctx (OL.fv e)) then lexp_error (lexp_location e) e ("Expression `" ^ lexp_string e ^ "` is not closed: " - ^ track_fv meta_ctx rctx (ectx_to_lctx ectx) e); + ^ track_fv rctx (ectx_to_lctx ectx) e);

try EV.eval ee rctx with exc -> EV.print_eval_trace None; raise exc @@ -807,13 +793,12 @@ and lexp_expand_macro loc macro_funct sargs ctx (ot : ltype option) : value_type =

(* Build the function to be called *) - let meta_ctx, _ = !global_substitution in let macro_expand = BI.get_predef "Macro_expand" ctx in (* FIXME: Rather than remember the lexp of "expand_macro" in predef, * we should remember its value so we don't have to re-eval it everytime. *) - let macro_expand = lexp_eval meta_ctx ctx macro_expand in + let macro_expand = lexp_eval ctx macro_expand in (* FIXME: provide `ot` (the optional expected type) for non-decl macros. *) - let macro = lexp_eval meta_ctx ctx macro_funct in + let macro = lexp_eval ctx macro_funct in let args = [macro; BI.o2v_list sargs] in

(* FIXME: Don't `mkCall + eval` but use eval_call instead! *) @@ -898,14 +883,13 @@ and lexp_decls_1 | (_, _, ForwardRef, t) -> push_susp t (S.shift (pt_idx + 1)) | _ -> U.internal_error "Var not found at its index!" in (* Unify it with the new one. *) - let meta_ctx, _ = !global_substitution in - let _ = match Unif.unify ltp pt (ectx_to_lctx nctx) meta_ctx with - | (None | Some (_, _::_)) + let _ = match Unif.unify ltp pt (ectx_to_lctx nctx) with + | (None | Some (_::_)) -> lexp_error l ltp ("New type annotation `" ^ lexp_string ltp ^ "` incompatible with previous `" ^ lexp_string pt ^ "`") - | Some subst -> global_substitution := subst in + | Some [] -> () in lexp_decls_1 sdecls ectx nctx pending_decls pending_defs else if List.exists (fun ((_, vname'), _) -> vname = vname') pending_defs then @@ -989,12 +973,11 @@ and lexp_parse_sexp (ctx: elab_context) (e : sexp) : lexp = and sform_new_attribute ctx loc sargs ot = match sargs with | [t] -> let ltp = infer_type t ctx None in - let meta_ctx, _ = !global_substitution in (* FIXME: This creates new values for type `ltp` (very wrong if `ltp` * is False, for example): Should be a type like `AttributeMap t` * instead. *) (mkBuiltin ((loc, "new-attribute"), - OL.lexp_close meta_ctx (ectx_to_lctx ctx) ltp, + OL.lexp_close (ectx_to_lctx ctx) ltp, Some AttributeMap.empty), Lazy) | _ -> fatal loc "new-attribute expects a single Type argument" @@ -1005,13 +988,12 @@ and sform_add_attribute ctx loc (sargs : sexp list) ot = | [table; Var((_, name), idx); attr] -> table, (n - idx, name), attr | _ -> fatal loc "add-attribute expects 3 arguments (table; var; attr)" in

- let meta_ctx, _ = !global_substitution in - let map, attr_type = match OL.lexp_whnf table (ectx_to_lctx ctx) meta_ctx with + let map, attr_type = match OL.lexp_whnf table (ectx_to_lctx ctx) with | Builtin (_, attr_type, Some map) -> map, attr_type | _ -> fatal loc "add-attribute expects a table as first argument" in

(* FIXME: Type check (attr: type == attr_type) *) - let attr' = OL.lexp_close meta_ctx (ectx_to_lctx ctx) attr in + let attr' = OL.lexp_close (ectx_to_lctx ctx) attr in let table = AttributeMap.add var attr' map in (mkBuiltin ((loc, "add-attribute"), attr_type, Some table), Lazy) @@ -1022,8 +1004,7 @@ and get_attribute ctx loc largs = | [table; Var((_, name), idx)] -> table, (ctx_n - idx, name) | _ -> fatal loc "get-attribute expects 2 arguments (table; var)" in

- let meta_ctx, _ = !global_substitution in - let map = match OL.lexp_whnf table (ectx_to_lctx ctx) meta_ctx with + let map = match OL.lexp_whnf table (ectx_to_lctx ctx) with | Builtin (_, attr_type, Some map) -> map | _ -> fatal loc "get-attribute expects a table as first argument" in

@@ -1045,8 +1026,7 @@ and sform_has_attribute ctx loc (sargs : sexp list) ot = | [table; Var((_, name), idx)] -> table, (n - idx, name) | _ -> fatal loc "get-attribute expects 2 arguments (table; var)" in

- let meta_ctx, _ = !global_substitution in - let map, attr_type = match OL.lexp_whnf table (ectx_to_lctx ctx) meta_ctx with + let map, attr_type = match OL.lexp_whnf table (ectx_to_lctx ctx) with | Builtin (_, attr_type, Some map) -> map, attr_type | lxp -> lexp_fatal loc lxp "get-attribute expects a table as first argument" in @@ -1077,8 +1057,7 @@ let sform_built_in ctx loc sargs ot = match !_parsing_internals, sargs with | true, [String (_, name); stp] -> let ltp = infer_type stp ctx None in - let meta_ctx, _ = !global_substitution in - let ltp' = OL.lexp_close meta_ctx (ectx_to_lctx ctx) ltp in + let ltp' = OL.lexp_close (ectx_to_lctx ctx) ltp in let bi = mkBuiltin ((loc, name), ltp', None) in if not (SMap.mem name (!EV.builtin_functions)) then sexp_error loc ("Unknown built-in `" ^ name ^ "`"); @@ -1209,13 +1188,12 @@ let rec sform_lambda kind ctx loc sargs ot = None (* Read var type from the provided type *) | Some t - -> let meta_ctx, _ = !global_substitution in - match OL.lexp_whnf t (ectx_to_lctx ctx) meta_ctx with + -> match OL.lexp_whnf t (ectx_to_lctx ctx) with | Arrow (ak2, _, lt1, _, lt2) when ak2 = kind -> (match olt1 with | None -> () | Some lt1' - -> if not (OL.conv_p meta_ctx (ectx_to_lctx ctx) lt1 lt1') + -> if not (OL.conv_p (ectx_to_lctx ctx) lt1 lt1') then lexp_error (lexp_location lt1') lt1' ("Type mismatch! Context expected `" ^ lexp_string lt1 ^ "`")); @@ -1390,9 +1368,7 @@ let default_ectx let lctx = read_file (btl_folder ^ "/pervasive.typer") lctx in lctx

-let default_rctx = - let meta_ctx, _ = !global_substitution in - EV.from_ectx meta_ctx default_ectx +let default_rctx = EV.from_ectx default_ectx

(* String Parsing * --------------------------------------------------------- *) @@ -1402,8 +1378,7 @@ let _lexp_expr_str (str: string) (tenv: token_env) (grm: grammar) (limit: string option) (ctx: elab_context) = let pxps = _pexp_expr_str str tenv grm limit in let lexps = lexp_parse_all pxps ctx in - let meta_ctx, _ = !global_substitution in - List.iter (fun lxp -> ignore (OL.check meta_ctx (ectx_to_lctx ctx) lxp)) + List.iter (fun lxp -> ignore (OL.check (ectx_to_lctx ctx) lxp)) lexps; lexps

===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -674,7 +674,7 @@ let closed_p rctx (fvs, mvs) = (* FIXME: Handle metavars! *) && VMap.is_empty mvs

-let from_lctx meta_ctx (lctx: lexp_context): runtime_env = +let from_lctx (lctx: lexp_context): runtime_env = (* FIXME: `eval` with a disabled IO.run. *) let rec from_lctx' (lctx: lexp_context): runtime_env = match lctx_view lctx with @@ -684,7 +684,7 @@ let from_lctx meta_ctx (lctx: lexp_context): runtime_env = Myers.cons (roname loname, ref (match def with | LetDef e - -> let e = L.clean meta_ctx e in + -> let e = L.clean e in if closed_p rctx (OL.fv e) then eval (OL.erase_type e) rctx else Vundefined @@ -695,7 +695,7 @@ let from_lctx meta_ctx (lctx: lexp_context): runtime_env = (fun fvs (_, odef, _) -> match odef with | LetDef e - -> OL.fv_union fvs (OL.fv (L.clean meta_ctx e)) + -> OL.fv_union fvs (OL.fv (L.clean e)) | _ -> fvs) OL.fv_empty defs in @@ -724,5 +724,5 @@ let from_lctx meta_ctx (lctx: lexp_context): runtime_env = in from_lctx lctx

(* build a rctx from a ectx. *) -let from_ectx meta_ctx (ctx: elab_context): runtime_env = - from_lctx meta_ctx (ectx_to_lctx ctx) +let from_ectx (ctx: elab_context): runtime_env = + from_lctx (ectx_to_lctx ctx)

===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -122,7 +122,25 @@ type varbind = | LetDef of lexp

module VMap = Map.Make (struct type t = int let compare = compare end) -type meta_subst = lexp VMap.t + +(* For metavariables, we give each metavar a (hopefully) unique integer + * and then we store its corresponding info into the `metavar_table` + * global map. + * + * Instead of this single ref-cell holding an IntMap, we could use many + * ref-cells, and do away with the unique integer. The reasons why we + * do it this way are: + * - for printing purposes, we want to have a printable unique identifier + * for each metavar. OCaml does not offer any way to turn a ref-cell + * into some kind of printable identifier (can't get a hash of the address, + * no `eq` hash-tables, ...). + * - Hashtbl.hash as well as `compare` happily follow ref-cell indirections: + * `compare (ref 0) (ref 0)` tells us they're equal! So we need the unique + * integer in order to procude a hash anyway (and we'd have to write the hash + * function by hand, tho that might be a good idea anyway). + *) +type metavar_info = lexp +type meta_subst = metavar_info VMap.t type constraints = (lexp * lexp) list

let empty_meta_subst : meta_subst = VMap.empty @@ -133,8 +151,8 @@ let impossible = Imm Sexp.dummy_epsilon

let builtin_size = ref 0

-(* :-( *) -let global_substitution = ref (empty_meta_subst, empty_constraint) +let metavar_table = ref (VMap.empty : meta_subst) +let metavar_lookup idx : metavar_info = VMap.find idx (!metavar_table)

(********************** Hash-consing **********************)

@@ -342,8 +360,7 @@ let clean e = else clean S.identity (mkSusp e s) | Metavar (idx, s', l, t) -> let s = (scompose s' s) in - let meta_ctx, _ = !global_substitution in - try clean s (VMap.find idx meta_ctx) + try clean s (metavar_lookup idx) with Not_found -> mkMetavar (idx, s, l, t) in clean S.identity e

===================================== src/opslexp.ml ===================================== --- a/src/opslexp.ml +++ b/src/opslexp.ml @@ -173,8 +173,7 @@ let lexp_whnf e (ctx : DB.lexp_context) : lexp = | Call (Cons (_, (_, name)), aargs) -> reduce name aargs | _ -> mkCase (l, e, rt, branches, default)) | Metavar (idx, s, _, _) - -> (let meta_ctx, _ = !global_substitution in - try lexp_whnf (mkSusp (L.VMap.find idx meta_ctx) s) ctx + -> (try lexp_whnf (mkSusp (metavar_lookup idx) s) ctx with Not_found -> e)

(* FIXME: I'd really prefer to use "native" recursive substitutions, using @@ -305,8 +304,7 @@ let level_canon e = | Var (_, i) -> let o = try VMap.find i m with Not_found -> -1 in if o < d then (c, VMap.add i d m) else acc | Metavar (i, _, _, _) - -> (let meta_ctx, _ = !global_substitution in - try canon (VMap.find i meta_ctx) d acc + -> (try canon (metavar_lookup i) d acc with Not_found -> let o = try VMap.find (- i) m with Not_found -> -1 in if o < d then (c, VMap.add (- i) d m) else acc) @@ -606,8 +604,7 @@ let rec check' erased ctx e = ^ lexp_string t); DB.type_int)) | Metavar (idx, s, _, t) - -> (try let meta_ctx, _ = !global_substitution in - let e = push_susp (L.VMap.find idx meta_ctx) s in + -> (try let e = push_susp (metavar_lookup idx) s in let t' = check erased ctx e in assert_type ctx e t' t with Not_found -> ());

===================================== src/unification.ml ===================================== --- a/src/unification.ml +++ b/src/unification.ml @@ -1,6 +1,6 @@ (* unification.ml --- Unification of Lexp terms

-Copyright (C) 2016 Free Software Foundation, Inc. +Copyright (C) 2016-2017 Free Software Foundation, Inc.

Author: Vincent Bonnevalle tiv.crb@gmail.com

@@ -40,24 +40,13 @@ let create_metavar () = global_last_metavar := !global_last_metavar + 1; !global_last_metavar

(* For convenience *) -type return_type = (meta_subst * constraints) option +type return_type = constraints option

(** Alias for VMap.add*) let associate (meta: int) (lxp: lexp) (subst: meta_subst) : meta_subst = (VMap.add meta lxp subst)

-(** If key is in map returns the value associated - else returns <code>None</code> -*) -let find_or_none (value: lexp) (map: meta_subst) : lexp option = - match value with - | Metavar (idx, _, _, _) - -> if VMap.mem idx map - then Some (VMap.find idx map) - else None - | _ -> None - (** lexp is equivalent to _ in ocaml (Let , lexp) == (lexp , Let) @@ -68,10 +57,10 @@ let find_or_none (value: lexp) (map: meta_subst) : lexp option =

let unify_and res op = match res with | None -> None - | Some (subst, constraints1) - -> match op subst with + | Some constraints1 + -> match op with | None -> None - | Some (subst, constraints2) -> Some (subst, constraints2@constraints1) + | Some constraints2 -> Some (constraints2@constraints1)

(****************************** Top level unify *************************************)

@@ -82,35 +71,34 @@ let unify_and res op = match res with The metavar unifyer is the end rule, it can't call unify with it's parameter (changing their order) *) let rec unify (e1: lexp) (e2: lexp) - (ctx : DB.lexp_context) (subst: meta_subst) + (ctx : DB.lexp_context) : return_type = - unify' e1 e2 ctx OL.set_empty subst + unify' e1 e2 ctx OL.set_empty

and unify' (e1: lexp) (e2: lexp) - (ctx : DB.lexp_context) (vs : OL.set_plexp) (subst: meta_subst) + (ctx : DB.lexp_context) (vs : OL.set_plexp) : return_type = - let e1' = OL.lexp_whnf e1 ctx subst in - let e2' = OL.lexp_whnf e2 ctx subst in + let e1' = OL.lexp_whnf e1 ctx in + let e2' = OL.lexp_whnf e2 ctx in let changed = not (e1 == e1' && e2 == e2') in - if changed && OL.set_member_p subst vs e1' e2' then Some (subst, []) else + if changed && OL.set_member_p vs e1' e2' then Some [] 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 _) | (Inductive _, Inductive _)) - -> if OL.conv_p subst ctx e1' e2' then Some (subst, []) else None - | (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 + -> 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, (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' subst - | (Lambda _ as l, r) -> _unify_lambda l r ctx vs' subst - | (Call _ as l, r) -> _unify_call l r ctx vs' subst + | (Arrow _ as l, r) -> _unify_arrow l r ctx vs' + | (Lambda _ as l, r) -> _unify_lambda l r ctx vs' + | (Call _ as l, r) -> _unify_call l r ctx vs' (* | (Case _ as l, r) -> _unify_case l r subst *) (* | (Inductive _ as l, r) -> _unify_induct l r subst *) - | (Sort _ as l, r) -> _unify_sort l r ctx vs' subst - | (SortLevel _ as l, r) -> _unify_sortlvl l r ctx vs' subst - | _ -> Some (subst, - if OL.conv_p subst ctx e1' e2' then [] else [(e1, e2)]) + | (Sort _ as l, r) -> _unify_sort l r ctx vs' + | (SortLevel _ as l, r) -> _unify_sortlvl l r ctx vs' + | _ -> Some (if OL.conv_p ctx e1' e2' then [] else [(e1, e2)])

(********************************* Type specific unify *******************************)

@@ -121,20 +109,20 @@ and unify' (e1: lexp) (e2: lexp) - (Arrow, Var) -> Constraint - (_, _) -> None *) -and _unify_arrow (arrow: lexp) (lxp: lexp) ctx vs (subst: meta_subst) +and _unify_arrow (arrow: lexp) (lxp: lexp) ctx vs : return_type = match (arrow, lxp) with | (Arrow (var_kind1, v1, ltype1, _, lexp1), Arrow (var_kind2, _, ltype2, _, lexp2)) -> if var_kind1 = var_kind2 - then unify_and (unify' ltype1 ltype2 ctx vs subst) + then unify_and (unify' ltype1 ltype2 ctx vs) (unify' lexp1 lexp2 (DB.lexp_ctx_cons ctx 0 v1 Variable ltype1) (OL.set_shift vs)) else None | (Arrow _, Imm _) -> None - | (Arrow _, Var _) -> Some (subst, [(arrow, lxp)]) - | (Arrow _, _) -> unify' lxp arrow ctx vs subst + | (Arrow _, Var _) -> Some ([(arrow, lxp)]) + | (Arrow _, _) -> unify' lxp arrow ctx vs | (_, _) -> None

(** Unify a Lambda and a lexp if possible @@ -145,22 +133,22 @@ and _unify_arrow (arrow: lexp) (lxp: lexp) ctx vs (subst: meta_subst) - Lambda , Let -> Constraint - Lambda , lexp -> unify lexp lambda subst *) -and _unify_lambda (lambda: lexp) (lxp: lexp) ctx vs (subst: meta_subst) : return_type = +and _unify_lambda (lambda: lexp) (lxp: lexp) ctx vs : return_type = match (lambda, lxp) with | (Lambda (var_kind1, v1, ltype1, lexp1), Lambda (var_kind2, _, ltype2, lexp2)) -> if var_kind1 = var_kind2 - then unify_and (unify' ltype1 ltype2 ctx vs subst) + then unify_and (unify' ltype1 ltype2 ctx vs) (unify' lexp1 lexp2 (DB.lexp_ctx_cons ctx 0 (Some v1) Variable ltype1) (OL.set_shift vs)) else None - | (Lambda _, Var _) -> Some ((subst, [(lambda, lxp)])) - | (Lambda _, Let _) -> Some ((subst, [(lambda, lxp)])) + | ((Lambda _, Var _) + | (Lambda _, Let _) + | (Lambda _, Call _)) -> Some [(lambda, lxp)] | (Lambda _, Arrow _) -> None - | (Lambda _, Call _) -> Some ((subst, [(lambda, lxp)])) | (Lambda _, Imm _) -> None - | (Lambda _, _) -> unify' lxp lambda ctx vs subst + | (Lambda _, _) -> unify' lxp lambda ctx vs | (_, _) -> None

(** Unify a Metavar and a lexp if possible @@ -169,26 +157,26 @@ 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 (subst: meta_subst) ctx idx s t (lxp1: lexp) (lxp2: lexp) +and _unify_metavar 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 + -> 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 subst t) ^ " != " - ^ lexp_string (Lexp.clean subst (OL.get_type subst ctx lxp)) ^ "\n" - ^ "for " ^ lexp_string lxp ^ "\n"); - Some (subst, []) in + ^ 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, _, t2) -> if idx = idx2 then (* FIXME: handle the case where s1 != s2 !! *) - Some ((subst, [])) + Some [] else (* If one of the two subst can't be inverted, try the other. * FIXME: There's probably a more general solution. *) @@ -204,19 +192,18 @@ and _unify_metavar (subst: meta_subst) ctx idx s t (lxp1: lexp) (lxp2: lexp) - Call , Call -> UNIFY - Call , lexp -> CONSTRAINT *) -and _unify_call (call: lexp) (lxp: lexp) ctx vs (subst: meta_subst) +and _unify_call (call: lexp) (lxp: lexp) ctx vs : return_type = match (call, lxp) with | (Call (lxp_left, lxp_list1), Call (lxp_right, lxp_list2)) - when OL.conv_p subst ctx lxp_left lxp_right - -> List.fold_left (fun op ((ak1, e1), (ak2, e2)) subst + 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 subst) op + unify_and (unify' e1 e2 ctx vs) op else None) - (fun subst -> Some (subst, [])) + (Some []) (List.combine lxp_list1 lxp_list2) - subst - | (Call _, _) -> Some ((subst, [(call, lxp)])) + | (Call _, _) -> Some [(call, lxp)] | (_, _) -> None

(** Unify a Case with a lexp @@ -276,11 +263,11 @@ and _unify_call (call: lexp) (lxp: lexp) ctx vs (subst: meta_subst) - SortLevel, SortLevel -> if SortLevel ~= SortLevel then OK else ERROR - SortLevel, _ -> ERROR *) -and _unify_sortlvl (sortlvl: lexp) (lxp: lexp) ctx vs (subst: meta_subst) : return_type = +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 (subst, []) - | SLsucc l1, SLsucc l2 -> unify' l1 l2 ctx vs subst + | SLz, SLz -> Some [] + | SLsucc l1, SLsucc l2 -> unify' l1 l2 ctx vs (* FIXME: Handle SLsub! *) | _, _ -> None) | _, _ -> None @@ -290,14 +277,14 @@ and _unify_sortlvl (sortlvl: lexp) (lxp: lexp) ctx vs (subst: meta_subst) : retu - Sort, Var -> Constraint - Sort, lexp -> ERROR *) -and _unify_sort (sort_: lexp) (lxp: lexp) ctx vs (subst: meta_subst) : return_type = +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 subst - | StypeOmega, StypeOmega -> Some (subst, []) - | StypeLevel, StypeLevel -> Some (subst, []) + | Stype lxp1, Stype lxp2 -> unify' lxp1 lxp2 ctx vs + | StypeOmega, StypeOmega -> Some [] + | StypeLevel, StypeLevel -> Some [] | _, _ -> None) - | Sort _, Var _ -> Some (subst, [(sort_, lxp)]) + | Sort _, Var _ -> Some [(sort_, lxp)] | _, _ -> None

(************************ Helper function **************************************)

===================================== tests/unify_test.ml ===================================== --- a/tests/unify_test.ml +++ b/tests/unify_test.ml @@ -43,7 +43,7 @@ type result = | Equivalent | Nothing

-type unif_res = (result * (meta_subst * constraints) option * lexp * lexp) +type unif_res = (result * (constraints) option * lexp * lexp)

type triplet = string * string * string

@@ -188,29 +188,32 @@ let generate_testable (_: lexp list) : ((lexp * lexp * result) list) =

::[]

-let test_input (lxp1: lexp) (lxp2: lexp) (subst: meta_subst): unif_res = - let res = unify lxp1 lxp2 Myers.nil subst in - let tmp = match res with - | Some (s, []) when s = empty_meta_subst -> (Equivalent, res, lxp1, lxp2) - | Some (_, []) -> (Unification, res, lxp1, lxp2) +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) - in tmp

-let check (lxp1: lexp) (lxp2: lexp) (res: result) (subst: meta_subst): bool = - let r, _, _, _ = test_input lxp1 lxp2 subst +let check (lxp1: lexp) (lxp2: lexp) (res: result): bool = + let r, _, _, _ = test_input lxp1 lxp2 in if r = res then true else false

let test_if (input: lexp list) sample_generator checker : bool = let rec test_if_ samples checker = match samples with - | (l1, l2, res)::t -> if checker l1 l2 res empty_meta_subst then test_if_ t checker else false + | (l1, l2, res)::t -> if checker l1 l2 res then test_if_ t checker else false | [] -> true in test_if_ (sample_generator input) checker

let unifications = List.map (fun (l1, l2, res) -> - let r, _, _, _ = test_input l1 l2 empty_meta_subst + let r, _, _, _ = test_input l1 l2 in (l1, l2, res, r)) (* FIXME: Skip failure for now. *) [] (* (generate_testable []) *)

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

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