Alice de Berny pushed to branch alice at Stefan / Typer

Commits: ff5ad4d5 by irradiee at 2020-05-30T13:45:44-04:00 add lexp_lexp' for genericity

- - - - -

7 changed files:

- src/debug.ml - src/elab.ml - src/eval.ml - src/inverse_subst.ml - src/lexp.ml - src/opslexp.ml - src/unification.ml

Changes:

===================================== src/debug.ml ===================================== @@ -157,7 +157,7 @@ let debug_lexp_decls decls =

) decls

-let print_hc_table = WHC.iter (fun e -> print_int (Hashtbl.hash e); +(* let print_hc_table table = WHC.iter (fun e -> print_int (Hashtbl.hash e); print_string "\t"; lexp_print e; - print_string "\n") hc_table + print_string "\n") table *)

===================================== src/elab.ml ===================================== @@ -121,7 +121,7 @@ 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 = - let (lp, h) = (try OL.lexp_whnf lsort (ectx_to_lctx ctx) + let lp = lexp_lexp' (try OL.lexp_whnf lsort (ectx_to_lctx ctx) with e -> info ~print_action:(fun _ -> lexp_print lsort; print_newline ()) ~loc:(lexp_location lsort) @@ -416,7 +416,7 @@ 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 = - let (e', h) = e in + let e' = lexp_lexp' e in match e' with | Imm _ -> e | SortLevel SLz -> e @@ -579,7 +579,7 @@ and infer (p : sexp) (ctx : elab_context): lexp * ltype =

and elab_special_form ctx f args ot = let loc = lexp_location f in - let (lp, h) = OL.lexp_whnf f (ectx_to_lctx ctx) in + let lp = lexp_lexp' (OL.lexp_whnf f (ectx_to_lctx ctx)) in match lp with | Builtin ((_, name), _, _) -> (* Special form. *) @@ -628,7 +628,7 @@ 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 = - let (lp, h) = OL.lexp_whnf t (ectx_to_lctx ctx) in + let lp = lexp_lexp' (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 @@ -641,7 +641,7 @@ 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 (lp, h) = OL.lexp_whnf s (ectx_to_lctx ectx) in + (let lp = lexp_lexp' (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 @@ -705,7 +705,7 @@ and check (p : sexp) (t : ltype) (ctx : elab_context): lexp = * do lots of other things. *) and check_inferred ctx e inferred_t t = let (e, inferred_t) = - let (lp, h) = OL.lexp_whnf t (ectx_to_lctx ctx) in + let lp = lexp_lexp' (OL.lexp_whnf t (ectx_to_lctx ctx)) in match lp with | Arrow ((Aerasable | Aimplicit), _, _, _, _) -> (e, inferred_t) @@ -757,7 +757,7 @@ and check_case rtype (loc, target, ppatterns) ctx = | [] -> () in (cs, args) | None - -> let (lp, h) = OL.lexp_whnf it' (ectx_to_lctx ctx) in + -> let lp = lexp_lexp' (OL.lexp_whnf it' (ectx_to_lctx ctx)) in match lp with | Inductive (_, _, fargs, constructors) -> let (s, targs) = List.fold_left @@ -774,13 +774,13 @@ and check_case rtype (loc, target, ppatterns) ctx = it_cs_as := Some (it', cs, args); (cs, args) | _ -> let call_split e = - let (lp, h) = OL.lexp_whnf e (ectx_to_lctx ctx) in + let lp = lexp_lexp' (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 = - let (lp, h) = OL.lexp_whnf it (ectx_to_lctx ctx) in + let lp = lexp_lexp' (OL.lexp_whnf it (ectx_to_lctx ctx)) in match lp with | Inductive (_, _, fargs, constructors) -> assert (List.length fargs = List.length targs); @@ -806,16 +806,16 @@ and check_case rtype (loc, target, ppatterns) ctx = let loc = sexp_location pctor in let lctor, ct = infer pctor ctx in let rec inst_args ctx e = - let (lp, h) = OL.lexp_whnf e (ectx_to_lctx ctx) in - match lp with + let lp = OL.lexp_whnf e (ectx_to_lctx ctx) in + match lexp_lexp' 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, h) in - let (lp, h') = nosusp (inst_args ctx lctor) in + | e -> lp in + let lp = lexp_lexp' (nosusp (inst_args ctx lctor)) in match lp with | Cons (it', (_, cons_name)) -> let _ = check_uniqueness pat cons_name lbranches in @@ -927,8 +927,8 @@ 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', h) = OL.lexp_whnf ltp (ectx_to_lctx ctx) in - match sargs, ltp' with + let ltp' = OL.lexp_whnf ltp (ectx_to_lctx ctx) in + match sargs, lexp_lexp' ltp' with | _, Arrow (ak, (_, Some aname), arg_type, _, ret_type) when SMap.mem aname pending -> let sarg = SMap.find aname pending in @@ -982,12 +982,12 @@ and elab_call ctx (func, ltp) (sargs: sexp list) = ^ "` have no matching formal args")); largs, ltp

- | sarg :: sargs, _ - -> let (arg_type, ret_type) = match ltp' with + | sarg :: sargs, _ (* verifier ltp' *) + -> let (arg_type, ret_type) = match lexp_lexp' ltp' with | Arrow (ak, _, arg_type, _, ret_type) -> assert (ak = Anormal); (arg_type, ret_type) | _ -> unify_with_arrow ctx (sexp_location sarg) - (ltp', h) Anormal (dloc, None) None in + ltp' 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 @@ -1010,22 +1010,20 @@ and lexp_parse_inductive ctors ctx = * things like `fv` and `meta_to_var`. *) let altacc = List.fold_right (fun (ak, n, t) aa - -> let lp = - Arrow (ak, n, t, dummy_location, aa) - in (lp, lexp'_hash lp)) + -> + hc (Arrow (ak, n, t, dummy_location, aa))) acc impossible in let g = generalize nctx altacc in let altacc' = g (fun _ne vname t l e - -> let lp = - Arrow (Aerasable, vname, t, l, e) - in (lp, lexp'_hash lp)) + -> + hc (Arrow (Aerasable, vname, t, l, e))) altacc in if altacc' == altacc then acc (* No generalization! *) else (* Convert the Lexp back into a list of fields. *) let rec loop e = - let (e', h) = e in + let e' = lexp_lexp' e in match e' with | Arrow (ak, n, t, _, e) -> (ak, n, t)::(loop e) | _ -> assert (e = impossible); [] in @@ -1180,11 +1178,10 @@ 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 = - let (t', h) = t in + let t' = lexp_lexp' 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) + -> hc (Arrow (ak, v, t1, l, strip_rettype t2)) | Sort _ | Metavar _ -> type0 (* Abritrary closed constant. *) | _ -> t in let g = generalize nctx (strip_rettype t) in @@ -1368,7 +1365,7 @@ and sform_add_attribute ctx loc (sargs : sexp list) ot = | _ -> fatal ~loc "add-attribute expects 3 arguments (table; var; attr)" in

let map, attr_type = - let (lp, h) = OL.lexp_whnf table (ectx_to_lctx ctx) in + let lp = lexp_lexp' (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 @@ -1386,7 +1383,7 @@ and get_attribute ctx loc largs = | _ -> fatal ~loc "get-attribute expects 2 arguments (table; var)" in

let map = - let (lp, h) = OL.lexp_whnf table (ectx_to_lctx ctx) in + let lp = lexp_lexp' (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 @@ -1406,10 +1403,10 @@ and sform_has_attribute ctx loc (sargs : sexp list) ot = | _ -> fatal ~loc "get-attribute expects 2 arguments (table; var)" in

let map, attr_type = - let (lp, h) = OL.lexp_whnf table (ectx_to_lctx ctx) in - match lp with + let lp = OL.lexp_whnf table (ectx_to_lctx ctx) in + match lexp_lexp' lp with | Builtin (_, attr_type, Some map) -> map, attr_type - | lxp -> lexp_fatal loc (lxp, h) + | lxp -> lexp_fatal loc lp "get-attribute expects a table as first argument" in

(BI.o2l_bool ctx (AttributeMap.mem var map), Lazy) @@ -1614,7 +1611,7 @@ let sform_identifier ctx loc sargs ot = let mv = newMetavar octx sl (loc, Some name) t in (if not (name = "") then let idx = - let (mv', h) = mv in + let mv' = lexp_lexp' mv in match mv' with | Metavar (idx, _, _) -> idx | _ -> fatal ~loc "newMetavar returned a non-Metavar" in @@ -1670,8 +1667,8 @@ let rec sform_lambda kind ctx loc sargs ot = None (* Read var type from the provided type *) | Some t - -> let (lp, h) = OL.lexp_whnf t (ectx_to_lctx ctx) in - match lp with + -> let lp = OL.lexp_whnf t (ectx_to_lctx ctx) in + match lexp_lexp' lp with | Arrow (ak2, _, lt1, _, lt2) when ak2 = kind -> (match olt1 with | None -> () @@ -1699,7 +1696,7 @@ let rec sform_lambda kind ctx loc sargs ot = | _ -> alt)

| lt - -> let (lt1, lt2) = unify_with_arrow ctx loc (lt, h) kind arg olt1 + -> let (lt1, lt2) = unify_with_arrow ctx loc lp kind arg olt1 in mklam lt1 (Some lt2))

| _ -> sexp_error loc ("##lambda_"^(match kind with Anormal -> "->"

===================================== src/eval.ml ===================================== @@ -738,8 +738,8 @@ 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 | ...` *) - let (lwhnf, h) = OL.lexp_whnf (mkVar ((dummy_location, Some name), idx)) - (ectx_to_lctx ectx) in + let lwhnf = lexp_lexp' (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 @@ -754,8 +754,8 @@ let erasable_p name nth ectx = else false | _ -> false in try let idx = senv_lookup name ectx in - let (lwhnf, h) = OL.lexp_whnf (mkVar ((dummy_location, Some name), idx)) - (ectx_to_lctx ectx) in + let lwhnf = lexp_lexp' (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), _) -> @@ -775,8 +775,8 @@ let erasable_p2 t name ectx = args) | _ -> false in try let idx = senv_lookup t ectx in - let (lwhnf, h) = OL.lexp_whnf (mkVar ((dummy_location, Some t), idx)) - (ectx_to_lctx ectx) in + let lwhnf = lexp_lexp' (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), _) -> @@ -794,8 +794,8 @@ let nth_ctor_arg name nth ectx = | exception (Failure _) -> "_" ) | _ -> "_" in try let idx = senv_lookup name ectx in - let (lwhnf, h) = OL.lexp_whnf (mkVar ((dummy_location, Some name), idx)) - (ectx_to_lctx ectx) in + let lwhnf = lexp_lexp' (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), _) -> @@ -816,8 +816,8 @@ let ctor_arg_pos name arg ectx = | Some n -> n ) | _ -> (-1) in try let idx = senv_lookup name ectx in - let (lwhnf, h) = OL.lexp_whnf (mkVar ((dummy_location, Some name), idx)) - (ectx_to_lctx ectx) in + let lwhnf = lexp_lexp' (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), _) ->

===================================== src/inverse_subst.ml ===================================== @@ -60,7 +60,7 @@ 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 *) - let (v', h) = v in + let v' = lexp_lexp' v in match v' with | Var (_, v) -> v | _ -> assert false @@ -184,7 +184,7 @@ let inverse (s: Lexp.subst) : Lexp.subst option = let rec invertible (s: subst) : bool = match s with | S.Identity _ -> true | S.Cons (e, s, _) - -> (let (e', h) = e in + -> (let e' = lexp_lexp' e in match e' with Var _ -> true | _ -> e = impossible) && invertible s

@@ -203,7 +203,7 @@ let rec lookup_inv_subst (i : db_index) (s : subst) : db_index with Not_invertible -> 0) | S.Cons (e, s, o) -> assert - (let (e', h) = e in + (let e' = lexp_lexp' e in match e' with Var _ -> true | _ -> e = impossible); 1 + lookup_inv_subst (i - o) s

@@ -254,7 +254,7 @@ let rec compose_inv_subst (s' : subst) (s : subst) = match s' with * 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 = - let (e', h) = e in + let e' = lexp_lexp' e in match e' with | Imm _ -> e | SortLevel (SLz) -> e

===================================== src/lexp.ml ===================================== @@ -176,15 +176,21 @@ 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 + +(* == depends on implementation when it involves non mutable types + * do not use (e, h) directly to "construct" a lexp ? + * in this case we had: ref lexp1' = ref lexp2' but not lexp1' == lexp2' ... *) + let lexp_lexp' (e, h) = e

let rec apply_lxor (map : int list) : int = match map with | [] -> 0 | e :: l -> e lxor (apply_lxor l)

+let combine_hash e1 e2 = e1 lxor e2 (* Hashtbl.hash for not lexp types - * TODO: find something else *) + * TODO: - find something else + * - extract the first arg of 2 arg types ? (SMap)*) let lexp'_hash (expr : lexp') = match expr with | Imm s -> Hashtbl.hash s @@ -192,9 +198,9 @@ let metavar_lookup (id : meta_id) : metavar_info -> (match l with | SLz -> Hashtbl.hash l | SLsucc lp -> lexp_hash lp - | SLlub (lp1, lp2) -> (lexp_hash lp1) lxor (lexp_hash lp2)) + | SLlub (lp1, lp2) -> combine_hash (lexp_hash lp1) (lexp_hash lp2)) | Sort (l, s) - -> (Hashtbl.hash l) lxor + -> combine_hash (Hashtbl.hash l) (match s with | Stype lp -> lexp_hash lp | StypeOmega -> Hashtbl.hash s @@ -202,49 +208,56 @@ let metavar_lookup (id : meta_id) : metavar_info | Builtin (v, t, m) as e -> Hashtbl.hash e | Var v -> Hashtbl.hash v | Let (l, ds, e) - -> (Hashtbl.hash l) lxor - ((apply_lxor (List.map (fun e -> let (n, lp, lt) = e in - ((Hashtbl.hash n) lxor ((lexp_hash lp) lxor (lexp_hash lt)))) - ds)) lxor (lexp_hash e)) + -> combine_hash (Hashtbl.hash l) + (combine_hash (apply_lxor (List.map (fun e -> let (n, lp, lt) = e in + (combine_hash (Hashtbl.hash n) (combine_hash (lexp_hash lp) (lexp_hash lt)))) + ds)) (lexp_hash e)) | Arrow (k, v, t1, l, t2) - -> ((Hashtbl.hash k) lxor (Hashtbl.hash v)) lxor - ((lexp_hash t1) lxor ((Hashtbl.hash l) lxor (lexp_hash t2))) + -> combine_hash (combine_hash (Hashtbl.hash k) (Hashtbl.hash v)) + (combine_hash (lexp_hash t1) (combine_hash (Hashtbl.hash l) (lexp_hash t2))) | Lambda (k, v, t, e) - -> ((Hashtbl.hash k) lxor (Hashtbl.hash v)) lxor - ((lexp_hash t) lxor (lexp_hash e)) + -> combine_hash (combine_hash (Hashtbl.hash k) (Hashtbl.hash v)) + (combine_hash (lexp_hash t) (lexp_hash e)) | Inductive (l, n, a, cs) - -> ((Hashtbl.hash l) lxor (Hashtbl.hash n)) lxor - ((apply_lxor (List.map (fun e -> let (ak, n, lt) = e in - ((Hashtbl.hash ak) lxor ((Hashtbl.hash n) lxor (lexp_hash lt)))) a)) - lxor Hashtbl.hash cs) - | Cons (t, n) -> (lexp_hash t) lxor (Hashtbl.hash n) + -> combine_hash (combine_hash (Hashtbl.hash l) (Hashtbl.hash n)) + (combine_hash (apply_lxor (List.map (fun e -> let (ak, n, lt) = e in + (combine_hash (Hashtbl.hash ak) + (combine_hash (Hashtbl.hash n) (lexp_hash lt)))) a)) + (Hashtbl.hash cs)) (* here *) + | Cons (t, n) -> combine_hash (lexp_hash t) (Hashtbl.hash n) | Case (l, e, rt, bs, d) - -> ((Hashtbl.hash l) lxor (lexp_hash e)) lxor - ((lexp_hash rt) lxor ((Hashtbl.hash bs) lxor + -> combine_hash (combine_hash (Hashtbl.hash l) (lexp_hash e)) + (combine_hash (lexp_hash rt) (combine_hash (Hashtbl.hash bs) (match d with - | Some (n, lp) -> (Hashtbl.hash n) lxor (lexp_hash lp) + | Some (n, lp) -> combine_hash (Hashtbl.hash n) (lexp_hash lp) | _ -> 0))) | Metavar (id, s, v) -> Hashtbl.hash expr - | Call (e, args) -> (lexp_hash e) lxor + | Call (e, args) -> combine_hash (lexp_hash e) (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) + (combine_hash (Hashtbl.hash ak) (lexp_hash lp))) args)) + | Susp (lp, subst) -> combine_hash (lexp_hash lp) (Hashtbl.hash subst)

let impossible = (let imp = Imm Sexp.dummy_epsilon in (imp, dummy_hash))

+let compare_hash x y = + let (x', h1) = x in + let (y', h2) = y in + compare h1 h2 = 0 + +(* May be a tree ? *) module WHC = Weak.Make (struct type t = lexp (* Using (=) instead of `compare` results * in an *enormous* slowdown. Apparently * `compare` checks == before recursing * but (=) doesn't? *) - let equal x y = (compare x y = 0) + let equal x y = (compare (lexp_lexp' x) (lexp_lexp' y) = 0) let hash = lexp_hash end)

-(* TODO: maybe just a table ? *) let hc_table : WHC.t = WHC.create 1000 -let hc (e : lexp') : lexp = let h = lexp'_hash e in WHC.merge hc_table (e, h) +let hc (e : lexp') : lexp = +let lp = (e, lexp'_hash e) in WHC.merge hc_table lp

let mkImm s = hc (Imm s) let mkSortLevel l = hc (SortLevel l) @@ -259,14 +272,14 @@ 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) - = let (f', h) = f in + = let f' = lexp_lexp' f in match f', es with | Call (f'', es'), _ -> hc (Call (f'', es' @ es)) | _, [] -> f | _ -> hc (Call (f, es))

and lexp_head e = - let (e', h) = e in + let e' = lexp_lexp' e in match e' with | Imm s -> if e = impossible then "impossible" else "Imm" ^ sexp_string s | Var _ -> "Var" @@ -285,8 +298,8 @@ and lexp_head e = | SortLevel _ -> "SortLevel"

let mkSLlub' (e1, e2) = - let (e1', h1) = e1 in - let (e2', h2) = e2 in + let e1' = lexp_lexp' e1 in + let e2' = lexp_lexp' 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 @@ -301,7 +314,7 @@ let mkSLlub' (e1, e2) = ("SLlub of non-level: " ^ lexp_head e1 ^ " ∪ " ^ lexp_head e2)

let mkSLsucc e = - let (e', h) = e in + let e' = lexp_lexp' e in match e' with | SortLevel _ | Var _ | Metavar _ | Susp _ -> SLsucc e @@ -338,11 +351,8 @@ let hcs_table : ((lexp * subst), lexp) Hashtbl.t = Hashtbl.create 1000 * ... *)

-(* let mkSusp e s = let susp = mkSusp_aux e s in (susp, lexp'_hash susp) *) - -(* argh *) let rec mkSusp e s = - let (e', h) = e in + let e' = lexp_lexp' e in if S.identity_p s then e else (* We apply the substitution eagerly to some terms. * There's no deep technical rason for that: @@ -409,7 +419,7 @@ let _ = assert (S.identity_p (scompose (S.shift 5) (sunshift 5)))

let rec lexp_location e = - let (e', h) = e in + let e' = lexp_lexp' e in match e' with | Sort (l,_) -> l | SortLevel (SLsucc e) -> lexp_location e @@ -437,7 +447,7 @@ 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. *) - let (e', h) = e in + let e' = lexp_lexp' e in match e' with | Imm _ -> e | SortLevel (SLz) -> e @@ -497,7 +507,7 @@ 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`. *) - let (e', h) = e in + let e' = lexp_lexp' e in match e' with | Susp(e, s) -> push_susp e s | _ -> e @@ -506,7 +516,7 @@ and nosusp e = (* Return `e` with no outermost `Susp`. *) (* Get rid of `Susp`ensions and instantiated `Metavar`s. *) let clean e = let rec clean s e = - let (e', h) = e in + let e' = lexp_lexp' e in match e' with | Imm _ -> e | SortLevel (SLz) -> e @@ -544,7 +554,7 @@ let clean e = L.rev ncase) cases in mkInductive (l, label, nargs, ncases) - | Cons (it, name) -> (let lp = Cons (clean s it, name) in (lp, lexp'_hash lp)) + | Cons (it, name) -> hc (Cons (clean s it, name)) | Case (l, e, ret, cases, default) -> mkCase (l, clean s e, clean s ret, SMap.map (fun (l, cargs, e) @@ -571,9 +581,9 @@ let stypecons = Symbol (U.dummy_location, "##typecons")

(* ugly printing (sexp_print (pexp_unparse (lexp_unparse e))) *) let rec lexp_unparse lxp = - let (lxp', h) = lxp in + let lxp' = lexp_lexp' lxp in match lxp' with - | Susp _ as e -> lexp_unparse (nosusp (e, lexp'_hash e)) + | Susp _ as e -> lexp_unparse (nosusp (hc e)) | Imm (sexp) -> sexp | Builtin ((l,name), _, _) -> Symbol (l, "##" ^ name) (* FIXME: Add a Sexp syntax for debindex references. *) @@ -703,7 +713,7 @@ and subst_string s = match s with -> "(↑"^ string_of_int o ^ " " ^ subst_string (S.cons l s) ^ ")"

and lexp_name e = - let (e', h) = e in + let e' = lexp_lexp' e in match e' with | Imm _ -> lexp_string e | Var _ -> lexp_string e @@ -794,7 +804,7 @@ let get_binary_op_name name =

let rec get_precedence expr ctx = let lkp name = SMap.find name (pp_grammar ctx) in - let (e', h) = expr in + let e' = lexp_lexp' expr in match e' with | Lambda _ -> lkp "lambda" | Case _ -> lkp "case" @@ -864,7 +874,7 @@ and lexp_str ctx (exp : lexp) : string = | Anormal -> ":" | Aimplicit -> "::" | Aerasable -> ":::" in

let get_name fname = - let (fn, h) = fname in + let fn = lexp_lexp' fname in match fn with | Builtin ((_, name), _, _) -> name, 0 | Var((_, Some name), idx) -> name, idx @@ -872,7 +882,7 @@ and lexp_str ctx (exp : lexp) : string = | Cons _ -> "__", 0 | _ -> "__", -1 in

- let (e', h) = exp in + let e' = lexp_lexp' exp in match e' with | Imm(value) -> (match value with | String (_, s) -> tval (""" ^ s ^ """) @@ -1029,59 +1039,54 @@ and lexp_str_decls ctx decls =

(** Syntactic equality (i.e. without β). *******)

-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 +let rec eq e1 e2 = + let e1' = lexp_lexp' e1 in + let e2' = lexp_lexp' e2 in + e1' == e2' || + match (e1', e2') with | (Imm (Integer (_, i1)), Imm (Integer (_, i2))) -> i1 = i2 | (Imm (Float (_, x1)), Imm (Float (_, x2))) -> x1 = x2 | (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), _) -> eq (push_susp e1 s1) e2 + | (_, 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 @@ -1093,15 +1098,13 @@ 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,7 @@ 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 = - let (le', h) = e in + let le' = lexp_lexp' e in match le' with | Var v -> (match lookup_value ctx v with | None -> e @@ -145,7 +145,7 @@ 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)) -> - (let (lwhnf', h) = lexp_whnf f ctx in + (let lwhnf' = lexp_lexp' (lexp_whnf f ctx) in match lwhnf' with | Lambda (_, _, _, body) -> (* Here we apply whnf to the arg eagerly to kind of stay closer @@ -177,11 +177,11 @@ let lexp_whnf e (ctx : DB.lexp_context) : lexp = ("Unhandled constructor " ^ name ^ "in case expression"); mkCase (l, e, rt, branches, default) in - (let (e'', h) = e' in + (let e'' = lexp_lexp' e' in match e'' with | Cons (_, (_, name)) -> reduce name [] | Call (f, aargs) -> - (let (lwhnf, h) = lexp_whnf f ctx in + (let lwhnf = lexp_lexp' (lexp_whnf f ctx) in match lwhnf with | Cons (_, (_, name)) -> reduce name aargs | _ -> mkCase (l, e, rt, branches, default)) @@ -196,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, h) + | elem -> e

in lexp_whnf e ctx

@@ -205,10 +205,8 @@ 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 - = 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'))); + = assert (lexp_lexp' e1 == lexp_lexp' (Lexp.hc (lexp_lexp' e1))); + assert (lexp_lexp' e2 == lexp_lexp' (Lexp.hc (lexp_lexp' e2))); try let _ = List.find (fun (e1', e2') -> L.eq e1 e1' && L.eq e2 e2') s @@ -237,7 +235,7 @@ let level_canon e = if o < d then (c, IMap.add v d m) else acc in

let rec canon e d ((c,m) as acc) = - let (e', h) = e in + let e' = lexp_lexp' e in match e' with | SortLevel SLz -> if c < d then (d, m) else acc | SortLevel (SLsucc e) -> canon e (d + 1) acc @@ -262,13 +260,13 @@ let level_leq (c1, m1) (c2, m2) = let rec conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = let e1' = lexp_whnf e1 ctx in let e2' = lexp_whnf e2 ctx in - e1' == e2' || - let changed = not (e1 == e1' && e2 == e2') in + let e1''= lexp_lexp' e1' in + let e2'' = lexp_lexp' e2' in + e1'' == e2'' || + let changed = not (lexp_lexp' e1 == e1'' && lexp_lexp' e2 == e2'') in 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 - 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 @@ -342,16 +340,16 @@ let conv_p (ctx : DB.lexp_context) e1 e2 (********* Testing if a lexp is properly typed *********)

let rec mkSLlub ctx e1 e2 = - let (lwhnf1, h1) = lexp_whnf e1 ctx in - let (lwhnf2, h2) = lexp_whnf e2 ctx in - match (lwhnf1, lwhnf2) with + let lwhnf1 = lexp_whnf e1 ctx in + let lwhnf2 = lexp_whnf e2 ctx in + match (lexp_lexp' lwhnf1, lexp_lexp' 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', h1) in - let ce2 = level_canon (e2', h2) in + -> let ce1 = level_canon lwhnf1 in + let ce2 = level_canon lwhnf2 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 *) @@ -365,8 +363,8 @@ 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. *) - let (lwhnf1, h1) = lexp_whnf k1 ctx1 in - let (lwhnf2, h2) = lexp_whnf k2 ctx2 in + let lwhnf1 = lexp_lexp' (lexp_whnf k1 ctx1) in + let lwhnf2 = lexp_lexp' (lexp_whnf k2 ctx2) in match (lwhnf1, lwhnf2) with | (Sort (_, s1), Sort (_, s2)) -> (match s1, s2 with @@ -422,7 +420,7 @@ 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`. *) - let (e', h) = e in + let e' = lexp_lexp' e in match e' with Var (_, idx) -> DB.set_mem idx nerased | _ -> false) defs in @@ -445,14 +443,14 @@ 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 - (let (lwhnf, h) = lexp_whnf s ctx in + (let lwhnf = lexp_lexp' (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 + let e' = lexp_lexp' e in match e' with | Imm (Float (_, _)) -> DB.type_float | Imm (Integer (_, _)) -> DB.type_int @@ -544,7 +542,7 @@ 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 - let (lwhnf, h) = lexp_whnf ft ctx in + let lwhnf = lexp_lexp' (lexp_whnf ft ctx) in match lwhnf with | Arrow (ak', v, t1, l, t2) -> if not (ak == ak') then @@ -568,9 +566,8 @@ let rec check'' erased ctx e = let (level, _, _, _) = List.fold_left (fun (level, ictx, erased, n) (ak, v, t) -> - ((let (lwhnf, h) = - lexp_whnf (check_type erased ictx t) ictx in - match lwhnf with + ((let lwhnf = lexp_whnf (check_type erased ictx t) ictx in + match lexp_lexp' lwhnf with | Sort (_, Stype _) when ak == P.Aerasable && impredicative_erase -> level @@ -588,7 +585,7 @@ let rec check'' erased ctx e = ("Field type " ^ lexp_string t ^ " is not a Type! (" - ^ lexp_string (tt, h) ^")"); + ^ lexp_string lwhnf ^")"); level), DB.lctx_extend ictx v Variable t, DB.set_sink 1 erased, @@ -609,13 +606,13 @@ let rec check'' erased ctx e = | Case (l, e, ret, branches, default) (* FIXME: Check that the return type isn't TypeLevel. *) -> let call_split e = - let (e', h) = e in + let e' = lexp_lexp' 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 - (let (lwhnf, h) = lexp_whnf it ctx in + (let lwhnf = lexp_lexp' (lexp_whnf it ctx) in match lwhnf, aargs with | Inductive (_, _, fargs, constructors), aargs -> let rec mksubst s fargs aargs = @@ -665,7 +662,7 @@ let rec check'' erased ctx e = | _,_ -> error_tc ~loc:l "Case on a non-inductive type!"); ret | Cons (t, (l, name)) - -> (let (lwhnf, h) = lexp_whnf t ctx in + -> (let lwhnf = lexp_lexp' (lexp_whnf t ctx) in match lwhnf with | Inductive (l, _, fargs, constructors) -> (try @@ -755,7 +752,7 @@ let fv_erase (fvs, mvs) = (fvs, mv_set_erase mvs)

let rec fv (e : lexp) : (DB.set * mv_set) = let fv' e = - let (e', h) = e in + let e' = lexp_lexp' e in match e' with | Imm _ -> fv_empty | SortLevel SLz -> fv_empty @@ -831,7 +828,7 @@ let rec fv (e : lexp) : (DB.set * mv_set) = (* This should never signal any warning/error. *)

let rec get_type ctx e = - let (e', h) = e in + let e' = lexp_lexp' e in match e' with | Imm (Float (_, _)) -> DB.type_float | Imm (Integer (_, _)) -> DB.type_int @@ -863,7 +860,7 @@ let rec get_type ctx e = -> let ft = get_type ctx f in List.fold_left (fun ft (ak,arg) - -> let (lwhnf, h) = lexp_whnf ft ctx in + -> let lwhnf = lexp_lexp' (lexp_whnf ft ctx) in match lwhnf with | Arrow (ak', v, t1, l, t2) -> mkSusp t2 (S.substitute arg) @@ -880,7 +877,7 @@ let rec get_type ctx e = let (level, _, _) = List.fold_left (fun (level, ictx, n) (ak, v, t) -> - ((let (lwhnf, h) = lexp_whnf (get_type ictx t) ictx in + ((let lwhnf = lexp_lexp' (lexp_whnf (get_type ictx t) ictx) in match lwhnf with | Sort (_, Stype _) when ak == P.Aerasable && impredicative_erase @@ -905,7 +902,7 @@ let rec get_type ctx e = tct | Case (l, e, ret, branches, default) -> ret | Cons (t, (l, name)) - -> (let (lwhnf, h) = lexp_whnf t ctx in + -> (let lwhnf = lexp_lexp' (lexp_whnf t ctx) in match lwhnf with | Inductive (l, _, fargs, constructors) -> (try @@ -940,7 +937,7 @@ let rec get_type ctx e = (*********** Type erasure, before evaluation. *****************)

let rec erase_type (lxp: L.lexp): E.elexp = - let (lxp', h) = lxp in + let lxp' = lexp_lexp' lxp in match lxp' with | L.Imm(s) -> E.Imm(s) | L.Builtin(v, _, _) -> E.Builtin(v) @@ -1032,12 +1029,8 @@ 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");*) - let lexp = - Call - ((let lexp' = - Cons ( - ((let lexp'' = - Inductive (loc, type_label, [], + + hc (Call (hc (Cons (hc (Inductive (loc, type_label, [], SMap.add cons_name (List.map (fun (oname, t) -> (P.Aimplicit, oname, @@ -1051,24 +1044,22 @@ let ctx2tup ctx nctx = * equivalent and preferable). *) mkSusp t (S.shift offset))) types) - SMap.empty) in (lexp'', lexp'_hash lexp'')), - cons_label)) in (lexp', lexp'_hash lexp')), + SMap.empty)), + cons_label)), List.mapi (fun i (oname, t) -> (P.Aimplicit, mkVar (oname, offset - i - 1))) - types) in (lexp, lexp'_hash lexp) + types)) | (DB.CVlet (name, LetDef (_, e), t, _) :: blocs) - -> let lp = - Let (loc, [(name, mkSusp e (S.shift 1), t)], - mk_lets_and_tup blocs ((name, t) :: types)) in (lp, lexp'_hash lp) + -> hc (Let (loc, [(name, mkSusp e (S.shift 1), t)], + mk_lets_and_tup blocs ((name, t) :: types))) | (DB.CVfix (defs, _) :: blocs) - -> let lp = - Let (loc, defs, + -> hc (Let (loc, defs, mk_lets_and_tup blocs (List.append (List.rev (List.map (fun (oname, _, t) -> (oname, t)) defs)) - types)) in (lp, lexp'_hash lp) + types))) | _ -> assert false in mk_lets_and_tup (get_blocs nctx []) []

===================================== src/unification.ml ===================================== @@ -62,7 +62,7 @@ let occurs_in (id: meta_id) (e : lexp) : bool = match metavar_lookup id with "Checking occurrence of an instantiated metavar!!" | MVar (sl, _, _) -> let rec oi e = - let (e', h) = e in + let e' = lexp_lexp' e in match e' with | Imm _ -> false | SortLevel SLz -> false @@ -191,8 +191,8 @@ 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 - let (e1'', h1) = e1' in - let (e2'', h2) = e2' in + let e1'' = lexp_lexp' e1' in + let e2'' = lexp_lexp' e2' in match (e1'', e2'') with | ((Imm _, Imm _) | (Cons _, Cons _) | (Builtin _, Builtin _) | (Var _, Var _)) @@ -231,8 +231,8 @@ and unify' (e1: lexp) (e2: lexp) *) and unify_arrow (arrow: lexp) (lxp: lexp) ctx vs : return_type = - let (arrow', h1) = arrow in - let (lxp', h2) = lxp in + let arrow' = lexp_lexp' arrow in + let lxp' = lexp_lexp' lxp in match (arrow', lxp') with | (Arrow (var_kind1, v1, ltype1, _, lexp1), Arrow (var_kind2, _, ltype2, _, lexp2)) @@ -256,8 +256,8 @@ 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 = - let (lambda', h1) = lambda in - let (lxp', h2) = lxp in + let lambda' = lexp_lexp' lambda in + let lxp' = lexp_lexp' lxp in match (lambda', lxp') with | (Lambda (var_kind1, v1, ltype1, lexp1), Lambda (var_kind2, _, ltype2, lexp2)) @@ -308,7 +308,7 @@ 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 - let (lxp2', h) = lxp2 in + let lxp2' = lexp_lexp' lxp2 in match lxp2' with | Metavar (idx2, s2, name) -> if idx = idx2 then @@ -379,8 +379,8 @@ and unify_metavar ctx idx s1 (lxp1: lexp) (lxp2: lexp) *) and unify_call (call: lexp) (lxp: lexp) ctx vs : return_type = - let (call', h1) = call in - let (lxp', h2) = lxp in + let call' = lexp_lexp' call in + let lxp' = lexp_lexp' 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 @@ -450,8 +450,8 @@ and unify_call (call: lexp) (lxp: lexp) ctx vs - SortLevel, _ -> ERROR *) and unify_sortlvl (sortlvl: lexp) (lxp: lexp) ctx vs : return_type = - let (sortlvl', h1) = sortlvl in - let (lxp', h2) = lxp in + let sortlvl' = lexp_lexp' sortlvl in + let lxp' = lexp_lexp' lxp in match sortlvl', lxp' with | (SortLevel s, SortLevel s2) -> (match s, s2 with | SLz, SLz -> [] @@ -469,8 +469,8 @@ 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 = - let (sort_', h1) = sort_ in - let (lxp', h2) = lxp in + let sort_' = lexp_lexp' sort_ in + let lxp' = lexp_lexp' lxp in match sort_', lxp' with | (Sort (_, srt), Sort (_, srt2)) -> (match srt, srt2 with | Stype lxp1, Stype lxp2 -> unify' lxp1 lxp2 ctx vs

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