Alice de Berny pushed to branch alice at Stefan / Typer
Commits: 63089e95 by irradiee at 2020-05-26T14:53:16-04:00 fix des repercussions du changement des lexp
- - - - -
6 changed files:
- src/elab.ml - src/eval.ml - src/inverse_subst.ml - src/lexp.ml - src/opslexp.ml - src/unification.ml
Changes:
===================================== src/elab.ml ===================================== @@ -121,12 +121,13 @@ let sform_default_ectx = ref empty_elab_context * to errors in the user's code). *)
let elab_check_sort (ctx : elab_context) lsort var ltp = - match (try OL.lexp_whnf lsort (ectx_to_lctx ctx) + let (lp, h) = (try OL.lexp_whnf lsort (ectx_to_lctx ctx) with e -> info ~print_action:(fun _ -> lexp_print lsort; print_newline ()) ~loc:(lexp_location lsort) "Exception during whnf of sort:"; - raise e) with + raise e) in + match lp with | Sort (_, _) -> () (* All clear! *) | _ -> let typestr = lexp_string ltp ^ " : " ^ lexp_string lsort in match var with @@ -323,7 +324,7 @@ let rec meta_to_var ids (e : lexp) = * into something like * * Γ ⊢ λ x₁…xₙ ≡> e[x₁…xₙ/m₁…mₙ] : τ₁…τₙ ≡> τ - * + * * The above substitution is not the usual capture-avoiding substitution * since it replaces metavars with vars rather than vars with terms. * It's more like *instanciation* of those metavars. @@ -414,7 +415,9 @@ let rec meta_to_var ids (e : lexp) =
(* `o` is the binding depth at which we are relative to the "root" * of the expression (i.e. where the new vars will be inserted). *) - and loop o e = match e with + and loop o e = + let (e', h) = e in + match e' with | Imm _ -> e | SortLevel SLz -> e | SortLevel (SLsucc e) -> mkSortLevel (mkSLsucc (loop o e)) @@ -576,7 +579,8 @@ and infer (p : sexp) (ctx : elab_context): lexp * ltype =
and elab_special_form ctx f args ot = let loc = lexp_location f in - match OL.lexp_whnf f (ectx_to_lctx ctx) with + let (lp, h) = OL.lexp_whnf f (ectx_to_lctx ctx) in + match lp with | Builtin ((_, name), _, _) -> (* Special form. *) (get_special_form name) ctx loc args ot @@ -624,7 +628,8 @@ and get_implicit_arg ctx loc oname t = (* Build the list of implicit arguments to instantiate. *) and instantiate_implicit e t ctx = let rec instantiate t args = - match OL.lexp_whnf t (ectx_to_lctx ctx) with + let (lp, h) = OL.lexp_whnf t (ectx_to_lctx ctx) in + match lp with | Arrow ((Aerasable | Aimplicit) as ak, (_, v), t1, _, t2) -> let arg = get_implicit_arg ctx (lexp_location e) v t1 in instantiate (mkSusp t2 (S.substitute arg)) ((ak, arg)::args) @@ -636,7 +641,8 @@ 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 - (match OL.lexp_whnf s (ectx_to_lctx ectx) with + (let (lp, h) = OL.lexp_whnf s (ectx_to_lctx ectx) in + match lp with | Sort (_, _) -> () (* All clear! *) (* FIXME: We could automatically coerce Type levels to Sorts, so we * could write `(a : TypeLevel) -> a -> a` instead of @@ -698,7 +704,9 @@ and check (p : sexp) (t : ltype) (ctx : elab_context): lexp = * 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 (e, inferred_t) = match OL.lexp_whnf t (ectx_to_lctx ctx) with + let (e, inferred_t) = + let (lp, h) = OL.lexp_whnf t (ectx_to_lctx ctx) in + match lp with | Arrow ((Aerasable | Aimplicit), _, _, _, _) -> (e, inferred_t) | _ -> instantiate_implicit e inferred_t ctx in @@ -749,7 +757,8 @@ and check_case rtype (loc, target, ppatterns) ctx = | [] -> () in (cs, args) | None - -> match OL.lexp_whnf it' (ectx_to_lctx ctx) with + -> let (lp, h) = OL.lexp_whnf it' (ectx_to_lctx ctx) in + match lp with | Inductive (_, _, fargs, constructors) -> let (s, targs) = List.fold_left (fun (s, targs) (ak, name, t) @@ -764,11 +773,15 @@ and check_case rtype (loc, target, ppatterns) ctx = 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) + | _ -> let call_split e = + let (lp, h) = OL.lexp_whnf e (ectx_to_lctx ctx) in + match lp 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 + let constructors = + let (lp, h) = OL.lexp_whnf it (ectx_to_lctx ctx) in + match lp with | Inductive (_, _, fargs, constructors) -> assert (List.length fargs = List.length targs); constructors @@ -792,15 +805,18 @@ 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 rec inst_args ctx e = match OL.lexp_whnf e (ectx_to_lctx ctx) with + let rec inst_args ctx e = + let (lp, h) = OL.lexp_whnf e (ectx_to_lctx ctx) in + match lp with | Lambda (Aerasable, v, t, body) -> let arg = newMetavar (ectx_to_lctx ctx) (ectx_to_scope_level ctx) v t in let nctx = ctx_extend ctx v Variable t in let body = inst_args nctx body in mkSusp body (S.substitute arg) - | e -> e in - match nosusp (inst_args ctx lctor) with + | e -> (e, h) in + let (lp, h') = nosusp (inst_args ctx lctor) in + match lp with | Cons (it', (_, cons_name)) -> let _ = check_uniqueness pat cons_name lbranches in let (constructors, targs) = get_cs_as it' lctor in @@ -911,7 +927,7 @@ and elab_call ctx (func, ltp) (sargs: sexp list) = let loc = lexp_location func in
let rec handle_fun_args largs sargs pending ltp = - let ltp' = OL.lexp_whnf ltp (ectx_to_lctx ctx) in + let (ltp', h) = 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 @@ -971,7 +987,7 @@ and elab_call ctx (func, ltp) (sargs: sexp list) = | Arrow (ak, _, arg_type, _, ret_type) -> assert (ak = Anormal); (arg_type, ret_type) | _ -> unify_with_arrow ctx (sexp_location sarg) - ltp' Anormal (dloc, None) None in + (ltp', h) Anormal (dloc, None) None in let larg = check sarg arg_type ctx in handle_fun_args ((Anormal, larg) :: largs) sargs pending (L.mkSusp ret_type (S.substitute larg)) in @@ -994,17 +1010,23 @@ and lexp_parse_inductive ctors ctx = * things like `fv` and `meta_to_var`. *) let altacc = List.fold_right (fun (ak, n, t) aa - -> Arrow (ak, n, t, dummy_location, aa)) + -> let lp = + Arrow (ak, n, t, dummy_location, aa) + in (lp, lexp'_hash lp)) acc impossible in let g = generalize nctx altacc in let altacc' = g (fun _ne vname t l e - -> Arrow (Aerasable, vname, t, l, e)) + -> let lp = + Arrow (Aerasable, vname, t, l, e) + in (lp, lexp'_hash lp)) altacc in if altacc' == altacc then acc (* No generalization! *) else (* Convert the Lexp back into a list of fields. *) - let rec loop e = match e with + let rec loop e = + let (e', h) = e in + match e' with | Arrow (ak, n, t, _, e) -> (ak, n, t)::(loop e) | _ -> assert (e = impossible); [] in loop altacc' @@ -1157,8 +1179,12 @@ and infer_and_generalize_type (ctx : elab_context) se name = * * But we don't bother trying to catch all cases currently. *) - let rec strip_rettype t = match t with - | Arrow (ak, v, t1, l, t2) -> Arrow (ak, v, t1, l, strip_rettype t2) + let rec strip_rettype t = + let (t', h) = t in + match t' with + | Arrow (ak, v, t1, l, t2) + -> let lp = Arrow (ak, v, t1, l, strip_rettype t2) + in (lp, lexp'_hash lp) | Sort _ | Metavar _ -> type0 (* Abritrary closed constant. *) | _ -> t in let g = generalize nctx (strip_rettype t) in @@ -1338,10 +1364,12 @@ and sform_new_attribute ctx loc sargs ot = and sform_add_attribute ctx loc (sargs : sexp list) ot = let n = get_size ctx in let table, var, attr = match List.map (lexp_parse_sexp ctx) sargs with - | [table; Var((_, Some name), idx); attr] -> table, (n - idx, name), attr + | [table; (Var((_, Some name), idx), _); attr] -> table, (n - idx, name), attr | _ -> fatal ~loc "add-attribute expects 3 arguments (table; var; attr)" in
- let map, attr_type = match OL.lexp_whnf table (ectx_to_lctx ctx) with + let map, attr_type = + let (lp, h) = OL.lexp_whnf table (ectx_to_lctx ctx) in + match lp with | Builtin (_, attr_type, Some map) -> map, attr_type | _ -> fatal ~loc "add-attribute expects a table as first argument" in
@@ -1354,10 +1382,12 @@ and sform_add_attribute ctx loc (sargs : sexp list) ot = and get_attribute ctx loc largs = let ctx_n = get_size ctx in let table, var = match largs with - | [table; Var((_, Some name), idx)] -> table, (ctx_n - idx, name) + | [table; (Var((_, Some name), _), idx)] -> table, (ctx_n - idx, name) | _ -> fatal ~loc "get-attribute expects 2 arguments (table; var)" in
- let map = match OL.lexp_whnf table (ectx_to_lctx ctx) with + let map = + let (lp, h) = OL.lexp_whnf table (ectx_to_lctx ctx) in + match lp with | Builtin (_, attr_type, Some map) -> map | _ -> fatal ~loc "get-attribute expects a table as first argument" in
@@ -1372,19 +1402,21 @@ and sform_get_attribute ctx loc (sargs : sexp list) ot = and sform_has_attribute ctx loc (sargs : sexp list) ot = let n = get_size ctx in let table, var = match List.map (lexp_parse_sexp ctx) sargs with - | [table; Var((_, Some name), idx)] -> table, (n - idx, name) + | [table; (Var((_, Some name), _), idx)] -> table, (n - idx, name) | _ -> fatal ~loc "get-attribute expects 2 arguments (table; var)" in
- let map, attr_type = match OL.lexp_whnf table (ectx_to_lctx ctx) with + let map, attr_type = + let (lp, h) = OL.lexp_whnf table (ectx_to_lctx ctx) in + match lp with | Builtin (_, attr_type, Some map) -> map, attr_type - | lxp -> lexp_fatal loc lxp + | lxp -> lexp_fatal loc (lxp, h) "get-attribute expects a table as first argument" in
(BI.o2l_bool ctx (AttributeMap.mem var map), Lazy)
and sform_declexpr ctx loc sargs ot = match List.map (lexp_parse_sexp ctx) sargs with - | [Var((_, vn), vi)] + | [(Var((_, vn), _), vi)] -> (match DB.env_lookup_expr ctx ((loc, vn), vi) with | Some lxp -> (lxp, Lazy) | None -> error ~loc "no expr available"; @@ -1395,7 +1427,7 @@ and sform_declexpr ctx loc sargs ot =
let sform_decltype ctx loc sargs ot = match List.map (lexp_parse_sexp ctx) sargs with - | [Var((_, vn), vi)] + | [(Var((_, vn), _), vi)] -> (DB.env_lookup_type ctx ((loc, vn), vi), Lazy) | _ -> error ~loc "decltype expects one argument"; sform_dummy_ret ctx loc @@ -1581,7 +1613,9 @@ let sform_identifier ctx loc sargs ot = -> Inverse_subst.apply_inv_subst t subst in let mv = newMetavar octx sl (loc, Some name) t in (if not (name = "") then - let idx = match mv with + let idx = + let (mv', h) = mv in + match mv' with | Metavar (idx, _, _) -> idx | _ -> fatal ~loc "newMetavar returned a non-Metavar" in rmmap := SMap.add name idx (!rmmap)); @@ -1636,7 +1670,8 @@ let rec sform_lambda kind ctx loc sargs ot = None (* Read var type from the provided type *) | Some t - -> match OL.lexp_whnf t (ectx_to_lctx ctx) with + -> let (lp, h) = OL.lexp_whnf t (ectx_to_lctx ctx) in + match lp with | Arrow (ak2, _, lt1, _, lt2) when ak2 = kind -> (match olt1 with | None -> () @@ -1664,7 +1699,7 @@ let rec sform_lambda kind ctx loc sargs ot = | _ -> alt)
| lt - -> let (lt1, lt2) = unify_with_arrow ctx loc lt kind arg olt1 + -> let (lt1, lt2) = unify_with_arrow ctx loc (lt, h) kind arg olt1 in mklam lt1 (Some lt2))
| _ -> sexp_error loc ("##lambda_"^(match kind with Anormal -> "->" @@ -1946,4 +1981,3 @@ let eval_decl_str str lctx rctx = let elxps = (List.map OL.clean_decls lxps) in (EV.eval_decls_toplevel elxps rctx), lctx with Log.Stop_Compilation s -> (prev_rctx, prev_lctx) -
===================================== src/eval.ml ===================================== @@ -484,7 +484,7 @@ and eval_call loc unef i f args = (* We may call a Vlexp e.g. for "x = Map Int String". * FIXME: The arg will sometimes be a Vlexp but not always, so this is * really just broken! *) - -> Vtype (L.mkCall (e, [(Anormal, Var (vdummy, -1))])) + -> Vtype (L.mkCall (e, [(Anormal, (Var (vdummy, -1), dummy_hash))])) | _ -> value_fatal loc f "Trying to call a non-function!"
and eval_case ctx i loc target pat dflt = @@ -738,10 +738,11 @@ let constructor_p name ectx = (* Use `lexp_whnf` so that `name` can be indirectly * defined as a constructor * (e.g. as in `let foo = cons in case foo x xs | ...` *) - match OL.lexp_whnf (mkVar ((dummy_location, Some name), idx)) - (ectx_to_lctx ectx) with - | Cons _ -> true (* It's indeed a constructor! *) - | _ -> false + let (lwhnf, h) = OL.lexp_whnf (mkVar ((dummy_location, Some name), idx)) + (ectx_to_lctx ectx) in + match lwhnf with + | Cons _ -> true (* It's indeed a constructor! *) + | _ -> false with Senv_Lookup_Fail _ -> false
let erasable_p name nth ectx = @@ -753,10 +754,11 @@ let erasable_p name nth ectx = else false | _ -> false in try let idx = senv_lookup name ectx in - match OL.lexp_whnf (mkVar ((dummy_location, Some name), idx)) - (ectx_to_lctx ectx) with - | Cons (Var v, _) -> ( match (env_lookup_expr ectx v) with - | Some (Inductive (_, _, _, ctors)) -> + let (lwhnf, h) = OL.lexp_whnf (mkVar ((dummy_location, Some name), idx)) + (ectx_to_lctx ectx) in + match lwhnf with + | Cons ((Var v, _), _) -> ( match (env_lookup_expr ectx v) with + | Some (Inductive (_, _, _, ctors), _) -> is_erasable ctors | _ -> false ) | _ -> false @@ -773,10 +775,11 @@ let erasable_p2 t name ectx = args) | _ -> false in try let idx = senv_lookup t ectx in - match OL.lexp_whnf (mkVar ((dummy_location, Some t), idx)) - (ectx_to_lctx ectx) with - | Cons (Var v, _) -> ( match (env_lookup_expr ectx v) with - | Some (Inductive (_, _, _, ctors)) -> + let (lwhnf, h) = OL.lexp_whnf (mkVar ((dummy_location, Some t), idx)) + (ectx_to_lctx ectx) in + match lwhnf with + | Cons ((Var v, _), _) -> ( match (env_lookup_expr ectx v) with + | Some (Inductive (_, _, _, ctors), _) -> is_erasable ctors | _ -> false ) | _ -> false @@ -791,10 +794,11 @@ let nth_ctor_arg name nth ectx = | exception (Failure _) -> "_" ) | _ -> "_" in try let idx = senv_lookup name ectx in - match OL.lexp_whnf (mkVar ((dummy_location, Some name), idx)) - (ectx_to_lctx ectx) with - | Cons (Var v, _) -> ( match (env_lookup_expr ectx v) with - | Some (Inductive (_, _, _, ctors)) -> + let (lwhnf, h) = OL.lexp_whnf (mkVar ((dummy_location, Some name), idx)) + (ectx_to_lctx ectx) in + match lwhnf with + | Cons ((Var v, _), _) -> ( match (env_lookup_expr ectx v) with + | Some (Inductive (_, _, _, ctors), _) -> find_nth ctors | _ -> "_" ) | _ -> "_" @@ -812,10 +816,11 @@ let ctor_arg_pos name arg ectx = | Some n -> n ) | _ -> (-1) in try let idx = senv_lookup name ectx in - match OL.lexp_whnf (mkVar ((dummy_location, Some name), idx)) - (ectx_to_lctx ectx) with - | Cons (Var v, _) -> ( match (env_lookup_expr ectx v) with - | Some (Inductive (_, _, _, ctors)) -> + let (lwhnf, h) = OL.lexp_whnf (mkVar ((dummy_location, Some name), idx)) + (ectx_to_lctx ectx) in + match lwhnf with + | Cons ((Var v, _), _) -> ( match (env_lookup_expr ectx v) with + | Some (Inductive (_, _, _, ctors), _) -> find_arg ctors | _ -> (-1) ) | _ -> (-1)
===================================== src/inverse_subst.ml ===================================== @@ -60,7 +60,8 @@ 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 + let (v', h) = v in + match v' with | Var (_, v) -> v | _ -> assert false in @@ -68,15 +69,15 @@ let transfo (s: Lexp.subst) : substIR option = indexOf (mkSusp var (S.shift offset)) (* Helper : shift the index of a var *) in match s with - | S.Cons (Var _ as v, s, o) -> + | S.Cons ((Var _ as v, h), s, o) -> let off_acc = off_acc + o in (match transfo s off_acc (idx + 1) imp_cnt with | Some (tail, off, imp) - -> let newVar = shiftVar v off_acc + -> let newVar = shiftVar (v, h) off_acc in if newVar >= off then None (* Error *) - else Some (((shiftVar v off_acc), idx)::tail, off, imp) + else Some (((shiftVar (v, h) off_acc), idx)::tail, off, imp) | None -> None) - | S.Cons (Imm (Sexp.Symbol (_, "")), s, o) + | S.Cons ((Imm (Sexp.Symbol (_, "")), _), s, o) -> transfo s (o + off_acc) (idx + 1) (imp_cnt + 1) | S.Identity o -> Some ([], (o + off_acc), imp_cnt) | _ -> None (* Error *) @@ -145,7 +146,7 @@ let fill (l: (int * int) list) (nbVar: int) (shift: int): Lexp.subst option = let is_identity s = let rec is_identity s acc = match s with - | S.Cons(Var(_, idx), s1, 0) when idx = acc -> is_identity s1 (acc + 1) + | S.Cons((Var(_, idx), _), s1, 0) when idx = acc -> is_identity s1 (acc + 1) | S.Identity o -> acc = o | _ -> S.identity_p s in is_identity s 0 @@ -182,7 +183,9 @@ let inverse (s: Lexp.subst) : Lexp.subst option = * with non-variables, in which case the "inverse" is ambiguous. *) let rec invertible (s: subst) : bool = match s with | S.Identity _ -> true - | S.Cons (e, s, _) -> (match e with Var _ -> true | _ -> e = impossible) + | S.Cons (e, s, _) + -> (let (e', h) = e in + match e' with Var _ -> true | _ -> e = impossible) && invertible s
exception Not_invertible @@ -193,13 +196,15 @@ let rec lookup_inv_subst (i : db_index) (s : subst) : db_index = match s with | (S.Identity o | S.Cons (_, _, o)) when i < o -> raise Not_invertible | S.Identity o -> i - o - | S.Cons (Var (_, i'), s, o) when i' = i - o + | S.Cons ((Var (_, i'), _), s, o) when i' = i - o -> (try let i'' = lookup_inv_subst i' s in assert (i'' != 0); raise Ambiguous with Not_invertible -> 0) | S.Cons (e, s, o) - -> assert (match e with Var _ -> true | _ -> e = impossible); + -> assert + (let (e', h) = e in + match e' with Var _ -> true | _ -> e = impossible); 1 + lookup_inv_subst (i - o) s
(* When going under a binder, we have the rule @@ -248,7 +253,9 @@ let rec compose_inv_subst (s' : subst) (s : subst) = match s' with * 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 +and apply_inv_subst (e : lexp) (s : subst) : lexp = + let (e', h) = e in + match e' with | Imm _ -> e | SortLevel (SLz) -> e | SortLevel (SLsucc e) -> mkSortLevel (mkSLsucc (apply_inv_subst e s))
===================================== src/lexp.ml ===================================== @@ -158,7 +158,8 @@ type metavar_info = type meta_subst = metavar_info U.IMap.t
let dummy_scope_level = 0 -let impossible = Imm Sexp.dummy_epsilon + +let dummy_hash = 0
let builtin_size = ref 0
@@ -175,6 +176,7 @@ let metavar_lookup (id : meta_id) : metavar_info * try Hashtbl.find hc_table e * with Not_found -> Hashtbl.add hc_table e e; e *) let lexp_hash (e, h) = h + let lexp_to_lexp' (e, h) = e
let rec apply_lxor (map : int list) : int = match map with @@ -183,7 +185,7 @@ let metavar_lookup (id : meta_id) : metavar_info
(* Hashtbl.hash for not lexp types * TODO: find something else *) - let lexp'_hash expr = + let lexp'_hash (expr : lexp') = match expr with | Imm s -> Hashtbl.hash s | SortLevel l @@ -227,7 +229,9 @@ let metavar_lookup (id : meta_id) : metavar_info | Call (e, args) -> (lexp_hash e) lxor (apply_lxor (List.map (fun e -> let (ak, lp) = e in ((Hashtbl.hash ak) lxor (lexp_hash lp))) args)) -(* | Susp (lp, subst) -> (lexp_hash lp) lxor (Hashtbl.hash subst) *) + | Susp (lp, subst) -> (lexp_hash lp) lxor (Hashtbl.hash subst) + +let impossible = (let imp = Imm Sexp.dummy_epsilon in (imp, dummy_hash))
module WHC = Weak.Make (struct type t = lexp (* Using (=) instead of `compare` results @@ -255,13 +259,15 @@ 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) = hc (Metavar (n, s, v)) let mkCall (f, es) - = match f, es with - | Call (f', es'), _ -> hc (Call (f', es' @ es)) - | _, [] -> (f, lexp'_hash f) - | _ -> hc (Call ((f, lexp'_hash f), es)) + = let (f', h) = f in + match f', es with + | Call (f'', es'), _ -> hc (Call (f'', es' @ es)) + | _, [] -> f + | _ -> hc (Call (f, es))
and lexp_head e = - match e with + let (e', h) = e in + match e' with | Imm s -> if e = impossible then "impossible" else "Imm" ^ sexp_string s | Var _ -> "Var" | Let _ -> "let" @@ -278,7 +284,10 @@ and lexp_head e = | Sort _ -> "Sort" | SortLevel _ -> "SortLevel"
-let mkSLlub' (e1, e2) = match (e1, e2) with +let mkSLlub' (e1, e2) = + let (e1', h1) = e1 in + let (e2', h2) = e2 in + match (e1', e2') with (* FIXME: This first case should be handled by calling `mkSLlub` instead! *) | (SortLevel SLz, SortLevel l) | (SortLevel l, SortLevel SLz) -> l | (SortLevel SLz, _) | (_, SortLevel SLz) @@ -287,14 +296,16 @@ let mkSLlub' (e1, e2) = match (e1, e2) with -> Log.log_fatal ~section:"internal" "lub of two SLsucc" | ((SortLevel _ | Var _ | Metavar _ | Susp _), (SortLevel _ | Var _ | Metavar _ | Susp _)) - -> SLlub ((e1, lexp'_hash e1), (e2, lexp'_hash e2)) + -> SLlub (e1, e2) | _ -> Log.log_fatal ~section:"internal" ("SLlub of non-level: " ^ lexp_head e1 ^ " ∪ " ^ lexp_head e2)
-let mkSLsucc e = match e with - | SortLevel _ | Var _ | Metavar _ | Susp _ - -> SLsucc (e, lexp'_hash e) - | _ -> Log.log_fatal ~section:"internal" "SLsucc of non-level " +let mkSLsucc e = + let (e', h) = e in + match e' with + | SortLevel _ | Var _ | Metavar _ | Susp _ + -> SLsucc e + | _ -> Log.log_fatal ~section:"internal" "SLsucc of non-level "
(********* Helper functions to use the Subst operations *********) (* This basically "ties the knot" between Subst and Lexp. @@ -398,7 +409,8 @@ let _ = assert (S.identity_p (scompose (S.shift 5) (sunshift 5)))
let rec lexp_location e = - match e with + let (e', h) = e in + match e' with | Sort (l,_) -> l | SortLevel (SLsucc e) -> lexp_location e | SortLevel (SLlub (e, _)) -> lexp_location e @@ -425,10 +437,11 @@ let maybename n = match n with None -> "<anon>" | Some v -> v let sname (l,n) = (l, maybename n)
let rec push_susp e s = (* Push a suspension one level down. *) - match e with + let (e', h) = e in + match e' with | Imm _ -> e | SortLevel (SLz) -> e - | SortLevel (SLsucc e') -> mkSortLevel (mkSLsucc (mkSusp e' s)) + | SortLevel (SLsucc e'') -> mkSortLevel (mkSLsucc (mkSusp e'' s)) | SortLevel (SLlub (e1, e2)) -> mkSortLevel (mkSLlub' (mkSusp e1 s, mkSusp e2 s)) | Sort (l, Stype e) -> mkSort (l, Stype (mkSusp e s)) @@ -484,14 +497,17 @@ let rec push_susp e s = (* Push a suspension one level down. *) | (Var _ | Metavar _) -> nosusp (mkSusp e s)
and nosusp e = (* Return `e` with no outermost `Susp`. *) - match e with + let (e', h) = e in + match e' with | Susp(e, s) -> push_susp e s | _ -> e
(* Get rid of `Susp`ensions and instantiated `Metavar`s. *) let clean e = - let rec clean s e = match e with + let rec clean s e = + let (e', h) = e in + match e' with | Imm _ -> e | SortLevel (SLz) -> e | SortLevel (SLsucc e) -> mkSortLevel (mkSLsucc (clean s e)) @@ -528,7 +544,7 @@ let clean e = L.rev ncase) cases in mkInductive (l, label, nargs, ncases) - | Cons (it, name) -> Cons (clean s it, name) + | Cons (it, name) -> (let lp = Cons (clean s it, name) in (lp, lexp'_hash lp)) | Case (l, e, ret, cases, default) -> mkCase (l, clean s e, clean s ret, SMap.map (fun (l, cargs, e) @@ -555,8 +571,9 @@ let stypecons = Symbol (U.dummy_location, "##typecons")
(* ugly printing (sexp_print (pexp_unparse (lexp_unparse e))) *) let rec lexp_unparse lxp = - match lxp with - | Susp _ as e -> lexp_unparse (nosusp e) + let (lxp', h) = lxp in + match lxp' with + | Susp _ as e -> lexp_unparse (nosusp (e, lexp'_hash e)) | Imm (sexp) -> sexp | Builtin ((l,name), _, _) -> Symbol (l, "##" ^ name) (* FIXME: Add a Sexp syntax for debindex references. *) @@ -686,7 +703,8 @@ and subst_string s = match s with -> "(↑"^ string_of_int o ^ " " ^ subst_string (S.cons l s) ^ ")"
and lexp_name e = - match e with + let (e', h) = e in + match e' with | Imm _ -> lexp_string e | Var _ -> lexp_string e | _ -> lexp_head e @@ -776,7 +794,8 @@ let get_binary_op_name name =
let rec get_precedence expr ctx = let lkp name = SMap.find name (pp_grammar ctx) in - match expr with + let (e', h) = expr in + match e' with | Lambda _ -> lkp "lambda" | Case _ -> lkp "case" | Let _ -> lkp "let" @@ -844,14 +863,17 @@ and lexp_str ctx (exp : lexp) : string = let kindp_str k = match k with | Anormal -> ":" | Aimplicit -> "::" | Aerasable -> ":::" in
- let get_name fname = match fname with + let get_name fname = + let (fn, h) = fname in + match fn with | Builtin ((_, name), _, _) -> name, 0 | Var((_, Some name), idx) -> name, idx | Lambda _ -> "__", 0 | Cons _ -> "__", 0 | _ -> "__", -1 in
- match exp with + let (e', h) = exp in + match e' with | Imm(value) -> (match value with | String (_, s) -> tval (""" ^ s ^ """) | Integer(_, s) -> tval (string_of_int s) @@ -962,8 +984,10 @@ and lexp_str ctx (exp : lexp) : string =
| Builtin ((_, name), _, _) -> "##" ^ name
- | Sort (_, Stype (SortLevel SLz)) -> "##Type" - | Sort (_, Stype (SortLevel (SLsucc (SortLevel SLz)))) -> "##Type1" + | Sort (_, Stype ((SortLevel SLz), _)) -> "##Type" + | Sort (_, Stype ((SortLevel + (SLsucc + (SortLevel SLz, _))), _)) -> "##Type1" | Sort (_, Stype l) -> "(##Type_ " ^ lexp_string l ^ ")" | Sort (_, StypeLevel) -> "##TypeLevel.Sort" | Sort (_, StypeOmega) -> "##Type_ω" @@ -1005,7 +1029,14 @@ and lexp_str_decls ctx decls =
(** Syntactic equality (i.e. without β). *******)
-let rec eq e1 e2 = +let eq (e1 : lexp) (e2 : lexp) : bool = + let (e1', h1) = e1 in + let (e2', h2) = e2 in + compare h1 h2 == 0 + +(* + +let rec eq' e1 e2 = e1 == e2 || match (e1, e2) with | (Imm (Integer (_, i1)), Imm (Integer (_, i2))) -> i1 = i2 @@ -1013,44 +1044,44 @@ let rec eq e1 e2 = | (Imm (String (_, s1)), Imm (String (_, s2))) -> s1 = s2 | (Imm s1, Imm s2) -> s1 = s2 | (SortLevel SLz, SortLevel SLz) -> true - | (SortLevel (SLsucc e1), SortLevel (SLsucc e2)) -> eq e1 e2 + | (SortLevel (SLsucc e1), SortLevel (SLsucc e2)) -> eq' e1 e2 | (SortLevel (SLlub (e11, e21)), SortLevel (SLlub (e12, e22))) - -> eq e11 e12 && eq e21 e22 + -> eq' e11 e12 && eq' e21 e22 | (Sort (_, StypeOmega), Sort (_, StypeOmega)) -> true | (Sort (_, StypeLevel), Sort (_, StypeLevel)) -> true - | (Sort (_, Stype e1), Sort (_, Stype e2)) -> eq e1 e2 + | (Sort (_, Stype e1), Sort (_, Stype e2)) -> eq' e1 e2 | (Builtin ((_, name1), _, _), Builtin ((_, name2), _, _)) -> name1 = name2 | (Var (_, i1), Var (_, i2)) -> i1 = i2 - | (Susp (e1, s1), e2) -> eq (push_susp e1 s1) e2 - | (e1, Susp (e2, s2)) -> eq e1 (push_susp e2 s2) + | (Susp (e1, s1), e2) -> eq' (push_susp e1 s1) e2 + | (e1, Susp (e2, s2)) -> eq' e1 (push_susp e2 s2) | (Let (_, defs1, e1), Let (_, defs2, e2)) - -> eq e1 e2 && List.for_all2 (fun (_, e1, t1) (_, e2, t2) - -> eq t1 t2 && eq e1 e2) + -> eq' e1 e2 && List.for_all2 (fun (_, e1, t1) (_, e2, t2) + -> eq' t1 t2 && eq' e1 e2) defs1 defs2 | (Arrow (ak1, _, t11, _, t21), Arrow (ak2, _, t12, _, t22)) - -> ak1 = ak2 && eq t11 t12 && eq t21 t22 + -> ak1 = ak2 && eq' t11 t12 && eq' t21 t22 | (Lambda (ak1, _, t1, e1), Lambda (ak2, _, t2, e2)) - -> ak1 = ak2 && eq t1 t2 && eq e1 e2 + -> ak1 = ak2 && eq' t1 t2 && eq' e1 e2 | (Call (e1, as1), Call (e2, as2)) - -> eq e1 e2 && List.for_all2 (fun (ak1, e1) (ak2, e2) -> ak1 = ak2 && eq e1 e2) + -> eq' e1 e2 && List.for_all2 (fun (ak1, e1) (ak2, e2) -> ak1 = ak2 && eq' e1 e2) as1 as2 | (Inductive (_, l1, as1, cases1), Inductive (_, l2, as2, cases2)) -> l1 = l2 - && List.for_all2 (fun (ak1, _, e1) (ak2, _, e2) -> ak1 = ak2 && eq e1 e2) + && List.for_all2 (fun (ak1, _, e1) (ak2, _, e2) -> ak1 = ak2 && eq' e1 e2) as1 as2 && SMap.equal (List.for_all2 (fun (ak1, _, e1) (ak2, _, e2) - -> ak1 = ak2 && eq e1 e2)) + -> ak1 = ak2 && eq' e1 e2)) cases1 cases2 - | (Cons (t1, (_, l1)), Cons (t2, (_, l2))) -> eq t1 t2 && l1 = l2 + | (Cons (t1, (_, l1)), Cons (t2, (_, l2))) -> eq' t1 t2 && l1 = l2 | (Case (_, e1, r1, cases1, def1), Case (_, e2, r2, cases2, def2)) - -> eq e1 e2 && eq r1 r2 + -> eq' e1 e2 && eq' r1 r2 && SMap.equal (fun (_, fields1, e1) (_, fields2, e2) - -> eq e1 e2 && List.for_all2 (fun (ak1, _) (ak2, _) + -> eq' e1 e2 && List.for_all2 (fun (ak1, _) (ak2, _) -> ak1 = ak2) fields1 fields2) cases1 cases2 && (match (def1, def2) with - | (Some (_, e1), Some (_, e2)) -> eq e1 e2 + | (Some (_, e1), Some (_, e2)) -> eq' e1 e2 | _ -> def1 = def2) | (Metavar (i1, s1, _), Metavar (i2, s2, _)) -> i1 = i2 && subst_eq s1 s2 @@ -1062,13 +1093,15 @@ and subst_eq s1 s2 = | (S.Identity o1, S.Identity o2) -> o1 = o2 | (S.Cons (e1, s1, o1), S.Cons (e2, s2, o2)) -> if o1 = o2 then - eq e1 e2 && subst_eq s1 s2 + eq' e1 e2 && subst_eq s1 s2 else if o1 > o2 then let o = o1 - o2 in - eq (mkSusp e1 (S.shift o)) e2 + eq' (mkSusp e1 (S.shift o)) e2 && subst_eq (S.mkShift s1 o) s2 else let o = o2 - o1 in - eq e1 (mkSusp e2 (S.shift o)) + eq' e1 (mkSusp e2 (S.shift o)) && subst_eq s1 (S.mkShift s2 o) | _ -> false + +*)
===================================== src/opslexp.ml ===================================== @@ -134,7 +134,8 @@ let lexp_close lctx e = * call-by-name behavior. *) let lexp_whnf e (ctx : DB.lexp_context) : lexp = let rec lexp_whnf e (ctx : DB.lexp_context) : lexp = - match e with + let (le', h) = e in + match le' with | Var v -> (match lookup_value ctx v with | None -> e (* We can do this blindly even for recursive definitions! @@ -144,7 +145,8 @@ let lexp_whnf e (ctx : DB.lexp_context) : lexp = | Susp (e, s) -> lexp_whnf (push_susp e s) ctx | Call (e, []) -> lexp_whnf e ctx | Call (f, (((_, arg)::args) as xs)) -> - (match lexp_whnf f ctx with + (let (lwhnf', h) = lexp_whnf f ctx in + match lwhnf' with | Lambda (_, _, _, body) -> (* Here we apply whnf to the arg eagerly to kind of stay closer * to the idea of call-by-value, although in this context @@ -175,10 +177,12 @@ let lexp_whnf e (ctx : DB.lexp_context) : lexp = ("Unhandled constructor " ^ name ^ "in case expression"); mkCase (l, e, rt, branches, default) in - (match e' with + (let (e'', h) = e' in + match e'' with | Cons (_, (_, name)) -> reduce name [] | Call (f, aargs) -> - (match lexp_whnf f ctx with + (let (lwhnf, h) = lexp_whnf f ctx in + match lwhnf with | Cons (_, (_, name)) -> reduce name aargs | _ -> mkCase (l, e, rt, branches, default)) | _ -> mkCase (l, e, rt, branches, default)) @@ -192,7 +196,7 @@ let lexp_whnf e (ctx : DB.lexp_context) : lexp = | Let (l, defs, body) -> lexp_whnf (push_susp body (lexp_defs_subst l S.identity defs)) ctx
- | e -> e + | e -> (e, h)
in lexp_whnf e ctx
@@ -201,8 +205,10 @@ let lexp_whnf e (ctx : DB.lexp_context) : lexp = type set_plexp = (lexp * lexp) list let set_empty : set_plexp = [] let set_member_p (s : set_plexp) (e1 : lexp) (e2 : lexp) : bool - = assert (e1 == Lexp.hc e1); - assert (e2 == Lexp.hc e2); + = lexp_print e2 ; print_string "\n" ; + lexp_print (Lexp.hc (let (e2', h) = e2 in e2')); + assert (lexp_hash e1 == lexp_hash (Lexp.hc (let (e1', h) = e1 in e1'))); + assert (lexp_hash e2 == lexp_hash (Lexp.hc (let (e2', h) = e2 in e2'))); try let _ = List.find (fun (e1', e2') -> L.eq e1 e1' && L.eq e2 e2') s @@ -230,7 +236,9 @@ let level_canon e = let o = try IMap.find v m with Not_found -> -1 in if o < d then (c, IMap.add v d m) else acc in
- let rec canon e d ((c,m) as acc) = match e with + let rec canon e d ((c,m) as acc) = + let (e', h) = e in + match e' with | SortLevel SLz -> if c < d then (d, m) else acc | SortLevel (SLsucc e) -> canon e (d + 1) acc | SortLevel (SLlub (e1, e2)) -> canon e1 d (canon e2 d acc) @@ -259,7 +267,9 @@ let rec conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = if changed && set_member_p vs e1' e2' then true else let vs' = if changed then set_add vs e1' e2' else vs in let conv_p = conv_p' ctx vs' in - match (e1', e2') with + let (e1'', h1) = e1' in + let (e2'', h1) = e2' in + match (e1'', e2'') with | (Imm (Integer (_, i1)), Imm (Integer (_, i2))) -> i1 = i2 | (Imm (Float (_, i1)), Imm (Float (_, i2))) -> i1 = i2 | (Imm (String (_, i1)), Imm (String (_, i2))) -> i1 = i2 @@ -332,14 +342,16 @@ let conv_p (ctx : DB.lexp_context) e1 e2 (********* Testing if a lexp is properly typed *********)
let rec mkSLlub ctx e1 e2 = - match (lexp_whnf e1 ctx, lexp_whnf e2 ctx) with + let (lwhnf1, h1) = lexp_whnf e1 ctx in + let (lwhnf2, h2) = lexp_whnf e2 ctx in + match (lwhnf1, lwhnf2) with | (SortLevel SLz, _) -> e2 | (_, SortLevel SLz) -> e1 | (SortLevel (SLsucc e1), SortLevel (SLsucc e2)) -> mkSortLevel (SLsucc (mkSLlub ctx e1 e2)) | (e1', e2') - -> let ce1 = level_canon e1' in - let ce2 = level_canon e2' in + -> let ce1 = level_canon (e1', h1) in + let ce2 = level_canon (e2', h2) in if level_leq ce1 ce2 then e2 else if level_leq ce2 ce1 then e1 else mkSortLevel (mkSLlub' (e1, e2)) (* FIXME: Could be more canonical *) @@ -353,7 +365,9 @@ type sort_compose_result let sort_compose ctx1 ctx2 l ak k1 k2 = (* BEWARE! Technically `k2` can refer to `v`, but this should only happen * if `v` is a TypeLevel. *) - match (lexp_whnf k1 ctx1, lexp_whnf k2 ctx2) with + let (lwhnf1, h1) = lexp_whnf k1 ctx1 in + let (lwhnf2, h2) = lexp_whnf k2 ctx2 in + match (lwhnf1, lwhnf2) with | (Sort (_, s1), Sort (_, s2)) -> (match s1, s2 with | (Stype l1, Stype l2) @@ -408,7 +422,8 @@ let nerased_let defs erased = * will be non-erasable, so in `let x = z; y = x ...` * where `z` is erasable, `x` will be found * to be erasable, but not `y`. *) - match e with Var (_, idx) -> DB.set_mem idx nerased + let (e', h) = e in + match e' with Var (_, idx) -> DB.set_mem idx nerased | _ -> false) defs in if not (List.mem true es) then nerased else @@ -430,14 +445,15 @@ let rec check'' erased ctx e = (* Log.internal_error "Type mismatch" *)) in let check_type erased ctx t = let s = check erased ctx t in - (match lexp_whnf s ctx with - | Sort _ -> () - | _ -> error_tc ~loc:(lexp_location t) - ("Not a proper type: " ^ lexp_string t)); - (* FIXME: return the `sort` rather than the surrounding `lexp`! *) - s in - - match e with + (let (lwhnf, h) = lexp_whnf s ctx in + match lwhnf with + | Sort _ -> () + | _ -> error_tc ~loc:(lexp_location t) + ("Not a proper type: " ^ lexp_string t)); + (* FIXME: return the `sort` rather than the surrounding `lexp`! *) + s in + let (e', h) = e in + match e' with | Imm (Float (_, _)) -> DB.type_float | Imm (Integer (_, _)) -> DB.type_int | Imm (String (_, _)) -> DB.type_string @@ -528,7 +544,8 @@ let rec check'' erased ctx e = (fun ft (ak,arg) -> let at = check (if ak = P.Aerasable then DB.set_empty else erased) ctx arg in - match lexp_whnf ft ctx with + let (lwhnf, h) = lexp_whnf ft ctx in + match lwhnf with | Arrow (ak', v, t1, l, t2) -> if not (ak == ak') then (error_tc ~loc:(lexp_location arg) @@ -551,8 +568,9 @@ let rec check'' erased ctx e = let (level, _, _, _) = List.fold_left (fun (level, ictx, erased, n) (ak, v, t) -> - ((match lexp_whnf (check_type erased ictx t) - ictx with + ((let (lwhnf, h) = + lexp_whnf (check_type erased ictx t) ictx in + match lwhnf with | Sort (_, Stype _) when ak == P.Aerasable && impredicative_erase -> level @@ -570,7 +588,7 @@ let rec check'' erased ctx e = ("Field type " ^ lexp_string t ^ " is not a Type! (" - ^ lexp_string tt ^")"); + ^ lexp_string (tt, h) ^")"); level), DB.lctx_extend ictx v Variable t, DB.set_sink 1 erased, @@ -590,12 +608,15 @@ let rec check'' erased ctx e = tct | Case (l, e, ret, branches, default) (* FIXME: Check that the return type isn't TypeLevel. *) - -> let call_split e = match e with + -> let call_split e = + let (e', h) = e in + match e' with | Call (f, args) -> (f, args) | _ -> (e,[]) in let etype = lexp_whnf (check erased ctx e) ctx in let it, aargs = call_split etype in - (match lexp_whnf it ctx, aargs with + (let (lwhnf, h) = lexp_whnf it ctx in + match lwhnf, aargs with | Inductive (_, _, fargs, constructors), aargs -> let rec mksubst s fargs aargs = match fargs, aargs with @@ -644,8 +665,9 @@ let rec check'' erased ctx e = | _,_ -> error_tc ~loc:l "Case on a non-inductive type!"); ret | Cons (t, (l, name)) - -> (match lexp_whnf t ctx with - | Inductive (l, _, fargs, constructors) + -> (let (lwhnf, h) = lexp_whnf t ctx in + match lwhnf with + | Inductive (l, _, fargs, constructors) -> (try let fieldtypes = SMap.find name constructors in let rec indtype fargs start_index = @@ -732,7 +754,9 @@ let fv_hoist n (fvs, mvs) = (DB.set_hoist n fvs, mvs) let fv_erase (fvs, mvs) = (fvs, mv_set_erase mvs)
let rec fv (e : lexp) : (DB.set * mv_set) = - let fv' e = match e with + let fv' e = + let (e', h) = e in + match e' with | Imm _ -> fv_empty | SortLevel SLz -> fv_empty | SortLevel (SLsucc e) -> fv e @@ -807,7 +831,8 @@ let rec fv (e : lexp) : (DB.set * mv_set) = (* This should never signal any warning/error. *)
let rec get_type ctx e = - match e with + let (e', h) = e in + match e' with | Imm (Float (_, _)) -> DB.type_float | Imm (Integer (_, _)) -> DB.type_int | Imm (String (_, _)) -> DB.type_string @@ -838,7 +863,8 @@ let rec get_type ctx e = -> let ft = get_type ctx f in List.fold_left (fun ft (ak,arg) - -> match lexp_whnf ft ctx with + -> let (lwhnf, h) = lexp_whnf ft ctx in + match lwhnf with | Arrow (ak', v, t1, l, t2) -> mkSusp t2 (S.substitute arg) | _ -> ft) @@ -854,7 +880,8 @@ let rec get_type ctx e = let (level, _, _) = List.fold_left (fun (level, ictx, n) (ak, v, t) -> - ((match lexp_whnf (get_type ictx t) ictx with + ((let (lwhnf, h) = lexp_whnf (get_type ictx t) ictx in + match lwhnf with | Sort (_, Stype _) when ak == P.Aerasable && impredicative_erase -> level @@ -878,7 +905,8 @@ let rec get_type ctx e = tct | Case (l, e, ret, branches, default) -> ret | Cons (t, (l, name)) - -> (match lexp_whnf t ctx with + -> (let (lwhnf, h) = lexp_whnf t ctx in + match lwhnf with | Inductive (l, _, fargs, constructors) -> (try let fieldtypes = SMap.find name constructors in @@ -912,8 +940,8 @@ let rec get_type ctx e = (*********** Type erasure, before evaluation. *****************)
let rec erase_type (lxp: L.lexp): E.elexp = - - match lxp with + let (lxp', h) = lxp in + match lxp' with | L.Imm(s) -> E.Imm(s) | L.Builtin(v, _, _) -> E.Builtin(v) | L.Var(v) -> E.Var(v) @@ -1004,7 +1032,12 @@ let ctx2tup ctx nctx = let offset = List.length types in let types = List.rev types in (*Log.debug_msg ("Building tuple of size " ^ string_of_int offset ^ "\n");*) - Call (Cons (Inductive (loc, type_label, [], + let lexp = + Call + ((let lexp' = + Cons ( + ((let lexp'' = + Inductive (loc, type_label, [], SMap.add cons_name (List.map (fun (oname, t) -> (P.Aimplicit, oname, @@ -1018,22 +1051,24 @@ let ctx2tup ctx nctx = * equivalent and preferable). *) mkSusp t (S.shift offset))) types) - SMap.empty), - cons_label), + SMap.empty) in (lexp'', lexp'_hash lexp'')), + cons_label)) in (lexp', lexp'_hash lexp')), List.mapi (fun i (oname, t) -> (P.Aimplicit, mkVar (oname, offset - i - 1))) - types) + types) in (lexp, lexp'_hash lexp) | (DB.CVlet (name, LetDef (_, e), t, _) :: blocs) - -> Let (loc, [(name, mkSusp e (S.shift 1), t)], - mk_lets_and_tup blocs ((name, t) :: types)) + -> let lp = + Let (loc, [(name, mkSusp e (S.shift 1), t)], + mk_lets_and_tup blocs ((name, t) :: types)) in (lp, lexp'_hash lp) | (DB.CVfix (defs, _) :: blocs) - -> Let (loc, defs, + -> let lp = + Let (loc, defs, mk_lets_and_tup blocs (List.append (List.rev (List.map (fun (oname, _, t) -> (oname, t)) defs)) - types)) + types)) in (lp, lexp'_hash lp) | _ -> assert false in mk_lets_and_tup (get_blocs nctx []) []
===================================== src/unification.ml ===================================== @@ -61,7 +61,9 @@ let occurs_in (id: meta_id) (e : lexp) : bool = match metavar_lookup id with | MVal _ -> Log.internal_error "Checking occurrence of an instantiated metavar!!" | MVar (sl, _, _) - -> let rec oi e = match e with + -> let rec oi e = + let (e', h) = e in + match e' with | Imm _ -> false | SortLevel SLz -> false | SortLevel (SLsucc e) -> oi e @@ -189,21 +191,23 @@ and unify' (e1: lexp) (e2: lexp) let changed = true (* not (e1 == e1' && e2 == e2') *) in if changed && OL.set_member_p vs e1' e2' then [] else let vs' = if changed then OL.set_add vs e1' e2' else vs in - match (e1', e2') with + let (e1'', h1) = e1' in + let (e2'', h2) = e2' in + match (e1'', e2'') with | ((Imm _, Imm _) | (Cons _, Cons _) | (Builtin _, Builtin _) | (Var _, Var _)) -> if OL.conv_p ctx e1' e2' then [] else [(CKimpossible, ctx, e1, e2)] - | (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, (Metavar (idx, s, _) as r)) -> unify_metavar ctx idx s e2' e1' + | ((Metavar (idx, s, _) as l), r) -> unify_metavar ctx idx s e1' e2' + | (l, (Call _ as r)) -> unify_call e2' e1' ctx vs' (* | (l, (Case _ as r)) -> unify_case r l 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' + | (Arrow _ as l, r) -> unify_arrow e1' e2' ctx vs' + | (Lambda _ as l, r) -> unify_lambda e1' e2' ctx vs' + | (Call _ as l, r) -> unify_call e1' e2' 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' - | (SortLevel _ as l, r) -> unify_sortlvl l r ctx vs' + | (Sort _ as l, r) -> unify_sort e1' e2' ctx vs' + | (SortLevel _ as l, r) -> unify_sortlvl e1' e2' ctx vs' | (Inductive (_loc1, label1, args1, consts1), Inductive (_loc2, label2, args2, consts2)) -> (* print_string ("Unifying inductives " @@ -227,7 +231,9 @@ and unify' (e1: lexp) (e2: lexp) *) and unify_arrow (arrow: lexp) (lxp: lexp) ctx vs : return_type = - match (arrow, lxp) with + let (arrow', h1) = arrow in + let (lxp', h2) = lxp in + match (arrow', lxp') with | (Arrow (var_kind1, v1, ltype1, _, lexp1), Arrow (var_kind2, _, ltype2, _, lexp2)) -> if var_kind1 = var_kind2 @@ -250,7 +256,9 @@ and unify_arrow (arrow: lexp) (lxp: lexp) ctx vs - Lambda , lexp -> unify lexp lambda subst *) and unify_lambda (lambda: lexp) (lxp: lexp) ctx vs : return_type = - match (lambda, lxp) with + let (lambda', h1) = lambda in + let (lxp', h2) = lxp in + match (lambda', lxp') with | (Lambda (var_kind1, v1, ltype1, lexp1), Lambda (var_kind2, _, ltype2, lexp2)) -> if var_kind1 = var_kind2 @@ -300,7 +308,8 @@ and unify_metavar ctx idx s1 (lxp1: lexp) (lxp2: lexp) ^ lexp_string (OL.get_type ctx lxp) ^ "\n" ^ "for " ^ lexp_string lxp ^ "\n"); [(CKresidual, ctx, lxp1, lxp2)] in - match lxp2 with + let (lxp2', h) = lxp2 in + match lxp2' with | Metavar (idx2, s2, name) -> if idx = idx2 then match common_subset ctx s1 s2 with @@ -370,7 +379,9 @@ and unify_metavar ctx idx s1 (lxp1: lexp) (lxp2: lexp) *) and unify_call (call: lexp) (lxp: lexp) ctx vs : return_type = - match (call, lxp) with + let (call', h1) = call in + let (lxp', h2) = lxp in + match (call', lxp') with | (Call (lxp_left, lxp_list1), Call (lxp_right, lxp_list2)) when OL.conv_p ctx lxp_left lxp_right -> List.fold_left (fun op ((ak1, e1), (ak2, e2)) @@ -439,7 +450,9 @@ and unify_call (call: lexp) (lxp: lexp) ctx vs - SortLevel, _ -> ERROR *) and unify_sortlvl (sortlvl: lexp) (lxp: lexp) ctx vs : return_type = - match sortlvl, lxp with + let (sortlvl', h1) = sortlvl in + let (lxp', h2) = lxp in + match sortlvl', lxp' with | (SortLevel s, SortLevel s2) -> (match s, s2 with | SLz, SLz -> [] | SLsucc l1, SLsucc l2 -> unify' l1 l2 ctx vs @@ -456,7 +469,9 @@ and unify_sortlvl (sortlvl: lexp) (lxp: lexp) ctx vs : return_type = - Sort, lexp -> ERROR *) and unify_sort (sort_: lexp) (lxp: lexp) ctx vs : return_type = - match sort_, lxp with + let (sort_', h1) = sort_ in + let (lxp', h2) = lxp in + match sort_', lxp' with | (Sort (_, srt), Sort (_, srt2)) -> (match srt, srt2 with | Stype lxp1, Stype lxp2 -> unify' lxp1 lxp2 ctx vs | StypeOmega, StypeOmega -> [] @@ -557,4 +572,3 @@ and unify_inductive ctx vs args1 args2 consts1 consts2 e1 e2 = * | None -> None) * | _, _ -> None * in test l1 l2 subst *) -
View it on GitLab: https://gitlab.com/monnier/typer/-/commit/63089e95553de312dab7a21757a65cc5fe...
-
Alice de Berny -
Stefan Monnier