Alice de Berny pushed to branch master at Stefan / Typer

Commits: 28d16874 by irradiee at 2020-08-14T05:59:20-04:00 Add hash in Lexp's type (hash-consing). Lexp: type lexp is now a pair int * lexp' (interchangeable), profiling: add compilation with ocamlc & ocamlopt, collisions: add %cl command to get stats of hash-consing, Lexp tests: add tests and getters for some Lexp

- - - - - 68f25184 by irradiee at 2020-08-24T13:11:01-04:00 Add hash in Lexp's type (hash-consing). Lexp: type lexp is now a pair int * lexp' (interchangeable), profiling: add compilation with ocamlc & ocamlopt, collisions: add %cl command to get stats of hash-consing, Lexp tests: add tests and getters for some Lexp

- - - - -

13 changed files:

- GNUmakefile - src/REPL.ml - src/builtin.ml - src/debruijn.ml - src/elab.ml - src/eval.ml - src/inverse_subst.ml - src/lexp.ml - src/opslexp.ml - src/sexp.ml - src/unification.ml - src/util.ml - tests/unify_test.ml

Changes:

===================================== GNUmakefile ===================================== @@ -4,9 +4,13 @@ OCAMLBUILD=ocamlbuild

BUILDDIR := _build

+OCAMLCP := ocamlcp +OCAMLOPT := ocamlopt +OCAMLDEP := ocamldep + SRC_FILES := $(wildcard ./src/*.ml) -CPL_FILES := $(wildcard ./$(BUILDDIR)/src/*.cmo) TEST_FILES := $(wildcard ./tests/*_test.ml) +DEPSORT_FILES := $(shell ocamldep -sort -I src $(SRC_NO_DEBUG))

OBFLAGS = -tag debug -tag profile -lib str -build-dir $(BUILDDIR) -pkg zarith # OBFLAGS := -I $(SRCDIR) -build-dir $(BUILDDIR) -pkg str @@ -108,3 +112,30 @@ run/typer-file:

run/test-file: @./$(BUILDDIR)/test + +# Compile into bytecode using ocamlc in profiling mode. +# Generate a ocamlprof.dump file. +profiling-cp: + # ============================ + # profiling bytecode + # ============================ + ocamlfind $(OCAMLCP) -o profiling -linkpkg -package zarith \ + -I src str.cma -P f $(DEPSORT_FILES) + +# Compile into native code using ocamlopt in profiling mode. +# Generate a gmon.out file. +profiling-optp: + # ============================ + # profiling native code + # ============================ + ocamlfind $(OCAMLOPTP) -o profiling -linkpkg -package zarith \ + -I src str.cmxa -P f $(DEPSORT_FILES) + +# Clean profiling +# FIXME: We prefer generate files in the "./$(BUILDDIR)/" folder but how ? +# No -build-dir option found for ocamlc and ocamlopt. +clean-profiling: + -rm -rf profiling + -rm -rf src/*.cm[iox] src/*.o + -rm -rf ocamlprof.dump + -rm -rf gmon.out

===================================== src/REPL.ml ===================================== @@ -232,6 +232,7 @@ let rec repl i clxp rctx = | "%help" | "%h" -> (print_string help_msg; repl clxp rctx) | "%calltrace" | "%ct" -> (print_eval_trace None; repl clxp rctx) | "%typertrace" | "%tt" -> (print_typer_trace None; repl clxp rctx) + | "%lcollisions" | "%cl" -> (get_stats_hashtbl (WHC.stats hc_table))

(* command with arguments *) | _ when (ipt.[0] = '%' && ipt.[1] != ' ') -> (

===================================== src/builtin.ml ===================================== @@ -57,7 +57,7 @@ open Util

open Sexp (* Integer/Float *) open Pexp (* arg_kind *) -module L = Lexp + module OL = Opslexp open Lexp

===================================== src/debruijn.ml ===================================== @@ -35,8 +35,10 @@ module Str = Str

open Util + + open Lexp -module L = Lexp + module M = Myers open Fmt

@@ -300,7 +302,7 @@ let print_lexp_ctx_n (ctx : lexp_context) start =

(* Only print user defined variables *) let print_lexp_ctx (ctx : lexp_context) = - print_lexp_ctx_n ctx !L.builtin_size + print_lexp_ctx_n ctx !builtin_size

(* Dump the whole context *) let dump_lexp_ctx (ctx : lexp_context) =

===================================== 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 = - match (try OL.lexp_whnf lsort (ectx_to_lctx ctx) + match (try OL.lexp'_whnf lsort (ectx_to_lctx ctx) with e -> info ~print_action:(fun _ -> lexp_print lsort; print_newline ()) ~loc:(lexp_location lsort) @@ -323,7 +323,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. @@ -402,7 +402,7 @@ let rec meta_to_var ids (e : lexp) = * (case (B) above), so don't let it refer to the new vars. *) S.Identity (n + count) else - Identity n + S.Identity n | S.Cons (e, s', n) -> let o' = o - n in if o' < 0 then @@ -414,7 +414,8 @@ 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 = + match lexp_lexp' e with | Imm _ -> e | SortLevel SLz -> e | SortLevel (SLsucc e) -> mkSortLevel (mkSLsucc (loop o e)) @@ -576,7 +577,7 @@ 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 + match (OL.lexp'_whnf f (ectx_to_lctx ctx)) with | Builtin ((_, name), _, _) -> (* Special form. *) (get_special_form name) ctx loc args ot @@ -624,7 +625,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 = - match OL.lexp_whnf t (ectx_to_lctx 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) v t1 in instantiate (mkSusp t2 (S.substitute arg)) ((ak, arg)::args) @@ -636,7 +637,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 - (match OL.lexp_whnf s (ectx_to_lctx ectx) 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 @@ -698,7 +699,8 @@ 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) = + match OL.lexp'_whnf t (ectx_to_lctx ctx) with | Arrow ((Aerasable | Aimplicit), _, _, _, _) -> (e, inferred_t) | _ -> instantiate_implicit e inferred_t ctx in @@ -749,7 +751,7 @@ and check_case rtype (loc, target, ppatterns) ctx = | [] -> () in (cs, args) | None - -> match OL.lexp_whnf it' (ectx_to_lctx ctx) with + -> match OL.lexp'_whnf it' (ectx_to_lctx ctx) with | Inductive (_, _, fargs, constructors) -> let (s, targs) = List.fold_left (fun (s, targs) (ak, name, t) @@ -764,11 +766,13 @@ 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 = + 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) with + let constructors = + match OL.lexp'_whnf it (ectx_to_lctx ctx) with | Inductive (_, _, fargs, constructors) -> assert (List.length fargs = List.length targs); constructors @@ -792,15 +796,17 @@ 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 lxp = OL.lexp_whnf e (ectx_to_lctx ctx) in + match lexp_lexp' lxp 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 -> lxp in + match lexp_lexp' (nosusp (inst_args ctx lctor)) with | Cons (it', (_, cons_name)) -> let _ = check_uniqueness pat cons_name lbranches in let (constructors, targs) = get_cs_as it' lctor in @@ -912,7 +918,7 @@ and elab_call ctx (func, ltp) (sargs: sexp list) =

let rec handle_fun_args largs sargs pending ltp = let ltp' = OL.lexp_whnf ltp (ectx_to_lctx ctx) in - match sargs, ltp' with + 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 @@ -967,7 +973,7 @@ and elab_call ctx (func, ltp) (sargs: sexp list) = largs, ltp

| sarg :: sargs, _ - -> let (arg_type, ret_type) = match ltp' with + -> 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) @@ -994,17 +1000,18 @@ 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)) + -> mkArrow (ak, n, t, dummy_location, aa)) acc impossible in let g = generalize nctx altacc in let altacc' = g (fun _ne vname t l e - -> Arrow (Aerasable, vname, t, l, e)) + -> mkArrow (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 = match e with + let rec loop e = + match lexp_lexp' e with | Arrow (ak, n, t, _, e) -> (ak, n, t)::(loop e) | _ -> assert (e = impossible); [] in loop altacc' @@ -1157,8 +1164,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 = match t with - | Arrow (ak, v, t1, l, t2) -> Arrow (ak, v, t1, l, strip_rettype t2) + let rec strip_rettype t = + match lexp_lexp' t with + | Arrow (ak, v, t1, l, t2) + -> mkArrow (ak, v, t1, l, strip_rettype t2) | Sort _ | Metavar _ -> type0 (* Abritrary closed constant. *) | _ -> t in let g = generalize nctx (strip_rettype t) in @@ -1354,10 +1363,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; e; attr] when is_var e + -> table, (n - (get_var_db_index (get_var e)), U.get_vname_name (get_var_vname (get_var e))), 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 = + 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

@@ -1367,13 +1378,17 @@ and sform_add_attribute ctx loc (sargs : sexp list) ot = (mkBuiltin ((loc, "add-attribute"), attr_type, Some table), Lazy)

-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) - | _ -> fatal ~loc "get-attribute expects 2 arguments (table; var)" in

- let map = match OL.lexp_whnf table (ectx_to_lctx ctx) with + and get_attribute ctx loc largs = + let ctx_n = get_size ctx in + let table, var = match largs with + | [table; e] when is_var e + -> table, (ctx_n - get_var_db_index (get_var e), U.get_vname_name (get_var_vname (get_var e))) + | _ -> fatal ~loc "get-attribute expects 2 arguments (table; var)" in + + + 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

@@ -1388,33 +1403,39 @@ 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; e] when is_var e + -> table, (n - get_var_db_index (get_var e), U.get_vname_name (get_var_vname (get_var e))) | _ -> 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 = 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 + | lxp -> lexp_fatal loc table "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)] - -> (match DB.env_lookup_expr ctx ((loc, vn), vi) with - | Some lxp -> (lxp, Lazy) - | None -> error ~loc "no expr available"; - sform_dummy_ret ctx loc) - | _ -> error ~loc "declexpr expects one argument"; - sform_dummy_ret ctx loc + and sform_declexpr ctx loc sargs ot = + match List.map (lexp_parse_sexp ctx) sargs with + | [e] when is_var e + -> (match DB.env_lookup_expr ctx ((loc, U.get_vname_name_option (get_var_vname (get_var e))), get_var_db_index (get_var e)) with + | Some lxp -> (lxp, Lazy) + | None -> error ~loc "no expr available"; + sform_dummy_ret ctx loc) + | _ -> error ~loc "declexpr expects one argument"; + sform_dummy_ret ctx loc + + + let sform_decltype ctx loc sargs ot = + match List.map (lexp_parse_sexp ctx) sargs with + | [e] when is_var e + -> (DB.env_lookup_type ctx ((loc, U.get_vname_name_option (get_var_vname (get_var e))), get_var_db_index (get_var e)), Lazy) + | _ -> error ~loc "decltype expects one argument"; + sform_dummy_ret ctx loc

-let sform_decltype ctx loc sargs ot = - match List.map (lexp_parse_sexp ctx) sargs with - | [Var((_, vn), vi)] - -> (DB.env_lookup_type ctx ((loc, vn), vi), Lazy) - | _ -> error ~loc "decltype expects one argument"; - sform_dummy_ret ctx loc

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

@@ -1597,7 +1618,8 @@ 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 = + match lexp_lexp' mv with | Metavar (idx, _, _) -> idx | _ -> fatal ~loc "newMetavar returned a non-Metavar" in rmmap := SMap.add name idx (!rmmap)); @@ -1652,7 +1674,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 = 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 -> () @@ -1680,7 +1703,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 lp kind arg olt1 in mklam lt1 (Some lt2))

| _ -> sexp_error loc ("##lambda_"^(match kind with Anormal -> "->" @@ -1956,4 +1979,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, mkVar (vdummy, -1))])) | _ -> value_fatal loc f "Trying to call a non-function!"

and eval_case ctx i loc target pat dflt = @@ -738,10 +738,9 @@ 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 + match OL.lexp'_whnf (mkVar ((dummy_location, Some name), idx)) (ectx_to_lctx ectx) with + | Cons _ -> true (* It's indeed a constructor! *) + | _ -> false with Senv_Lookup_Fail _ -> false

let erasable_p name nth ectx = @@ -753,32 +752,33 @@ 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)) -> - is_erasable ctors - | _ -> false ) + match OL.lexp'_whnf (mkVar ((dummy_location, Some name), idx)) (ectx_to_lctx ectx) with + | Cons (e, _) when is_var e + -> (match (env_lookup_expr ectx (get_var e)) with + | Some i when is_inductive i + -> is_erasable (get_inductive_ctor (get_inductive i)) + | _ -> false) | _ -> false with Senv_Lookup_Fail _ -> false

let erasable_p2 t name ectx = - let is_erasable ctors = match (smap_find_opt t ctors) with - | Some args -> - (List.exists - (fun (k, oname, _) - -> match oname with - | (_, Some n) -> (n = name && k = Aerasable) - | _ -> false) - args) - | _ -> false in + let is_erasable ctors = + match (smap_find_opt t ctors) with + | Some args + -> (List.exists + (fun (k, oname, _) + -> match oname with + | (_, Some n) -> (n = name && k = Aerasable) + | _ -> false) + 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)) -> - is_erasable ctors - | _ -> false ) + match OL.lexp'_whnf (mkVar ((dummy_location, Some t), idx)) (ectx_to_lctx ectx) with + | Cons (e, _) when is_var e + -> (match (env_lookup_expr ectx (get_var e)) with + | Some i when is_inductive i + -> is_erasable (get_inductive_ctor (get_inductive i)) + | _ -> false) | _ -> false with Senv_Lookup_Fail _ -> false

@@ -791,12 +791,12 @@ 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)) -> - find_nth ctors - | _ -> "_" ) + match OL.lexp'_whnf (mkVar ((dummy_location, Some name), idx)) (ectx_to_lctx ectx) with + | Cons (e, _) when is_var e + -> (match (env_lookup_expr ectx (get_var e)) with + | Some i when is_inductive i + -> find_nth (get_inductive_ctor (get_inductive i)) + | _ -> "_") | _ -> "_" with Senv_Lookup_Fail _ -> "_"

@@ -812,12 +812,12 @@ 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)) -> - find_arg ctors - | _ -> (-1) ) + match OL.lexp'_whnf (mkVar ((dummy_location, Some name), idx)) (ectx_to_lctx ectx) with + | Cons (e, _) when is_var e + -> (match (env_lookup_expr ectx (get_var e)) with + | Some i when is_inductive i + -> find_arg (get_inductive_ctor (get_inductive i)) + | _ -> (-1)) | _ -> (-1) with Senv_Lookup_Fail _ -> (-1)

===================================== src/inverse_subst.ml ===================================== @@ -56,11 +56,11 @@ type substIR = ((int * int) list * int * int) (** Transform a substitution to a more linear substitution * makes the inversion easier * Example of result : ((new_idx, old_position)::..., shift)*) -let transfo (s: Lexp.subst) : substIR option = - let rec transfo (s: Lexp.subst) (off_acc: int) (idx: int) (imp_cnt : int) +let transfo (s: subst) : substIR option = + let rec transfo (s: 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 + match lexp_lexp' v with | Var (_, v) -> v | _ -> assert false in @@ -68,15 +68,16 @@ 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) -> - let off_acc = off_acc + o in + | S.Cons (e, s, o) when is_var e + -> 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 e off_acc in if newVar >= off then None (* Error *) - else Some (((shiftVar v off_acc), idx)::tail, off, imp) + else Some (((shiftVar e off_acc), idx)::tail, off, imp) | None -> None) - | S.Cons (Imm (Sexp.Symbol (_, "")), s, o) + | S.Cons (e, s, o) + when pred_imm e (fun s -> Sexp.pred_symbol s (fun n -> n = "")) -> transfo s (o + off_acc) (idx + 1) (imp_cnt + 1) | S.Identity o -> Some ([], (o + off_acc), imp_cnt) | _ -> None (* Error *) @@ -93,7 +94,7 @@ let rec sizeOf (s: (int * int) list): int = List.length s let counter = ref 0 let mkVar (idx: int) : lexp = counter := !counter + 1; - Lexp.mkVar ((U.dummy_location, None), idx) + mkVar ((U.dummy_location, None), idx)

(** Fill the gap between e_i in the list of couple (e_i, i) by adding dummy variables. @@ -104,18 +105,18 @@ let mkVar (idx: int) : lexp = @param size size of the list to return @param acc recursion accumulator *) -let fill (l: (int * int) list) (nbVar: int) (shift: int): Lexp.subst option = - let rec genDummyVar (beg_: int) (end_: int) (l: Lexp.subst): Lexp.subst = (* Create the filler variables *) +let fill (l: (int * int) list) (nbVar: int) (shift: int): subst option = + let rec genDummyVar (beg_: int) (end_: int) (l: subst): subst = (* Create the filler variables *) if beg_ < end_ then S.cons impossible (genDummyVar (beg_ + 1) end_ l) else l in - let fill_before (l: (int * int) list) (s: Lexp.subst) (nbVar: int): Lexp.subst option = (* Fill if the first var is not 0 *) + let fill_before (l: (int * int) list) (s: subst) (nbVar: int): subst option = (* Fill if the first var is not 0 *) match l with | [] -> Some (genDummyVar 0 nbVar s) | (i1, v1)::_ when i1 > 0 -> Some (genDummyVar 0 i1 s) | _ -> Some s - in let rec fill_after (l: (int * int) list) (nbVar: int) (shift: int): Lexp.subst option = (* Fill gaps *) + in let rec fill_after (l: (int * int) list) (nbVar: int) (shift: int): subst option = (* Fill gaps *) match l with | (idx1, val1)::(idx2, val2)::tail when (idx1 = idx2) -> None

@@ -145,7 +146,8 @@ 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(e, s1, 0) when pred_var e (fun e -> get_var_db_index e = acc) + -> is_identity s1 (acc + 1) | S.Identity o -> acc = o | _ -> S.identity_p s in is_identity s 0 @@ -154,7 +156,7 @@ let is_identity s =

<code>s:S.subst, l:lexp, s':S.subst</code> where <code>l[s][s'] = l</code> and <code> inverse s = s' </code> *) -let inverse (s: Lexp.subst) : Lexp.subst option = +let inverse (s: subst) : subst option = let sort = List.sort (fun (ei1, _) (ei2, _) -> compare ei1 ei2) in match transfo s with | None -> None @@ -182,7 +184,8 @@ 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, _) + -> (match lexp_lexp' e with Var _ -> true | _ -> e = impossible) && invertible s

exception Not_invertible @@ -193,13 +196,13 @@ 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 - -> (try let i'' = lookup_inv_subst i' s in + | S.Cons (e, s, o) when pred_var e (fun e -> get_var_db_index e = i - o) + -> (try let i'' = lookup_inv_subst (get_var_db_index (get_var e)) 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 (match lexp_lexp' e with Var _ -> true | _ -> e = impossible); 1 + lookup_inv_subst (i - o) s

(* When going under a binder, we have the rule @@ -248,7 +251,8 @@ 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 = + match lexp_lexp' e with | Imm _ -> e | SortLevel (SLz) -> e | SortLevel (SLsucc e) -> mkSortLevel (mkSLsucc (apply_inv_subst e s))

===================================== src/lexp.ml ===================================== @@ -60,7 +60,9 @@ module AttributeMap = Map.Make (struct type t = attribute_key let compare = comp

type ltype = lexp and subst = lexp S.subst - and lexp = +(* Here we want a pair of `Lexp` and its hash value to avoid re-hashing "sub-Lexp". *) + and lexp = lexp' * int + and lexp' = | Imm of sexp (* Used for strings, ... *) | SortLevel of sort_level | Sort of U.location * sort @@ -157,7 +159,6 @@ type metavar_info = type meta_subst = metavar_info U.IMap.t

let dummy_scope_level = 0 -let impossible = Imm Sexp.dummy_epsilon

let builtin_size = ref 0

@@ -169,22 +170,140 @@ let metavar_lookup (id : meta_id) : metavar_info

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

-(* let hc_table : (lexp, lexp) Hashtbl.t = Hashtbl.create 1000 - * let hc (e : lexp) : lexp = - * try Hashtbl.find hc_table e - * with Not_found -> Hashtbl.add hc_table e e; e *) +(** Hash-consing test ** +* with: Hashtbl.hash / lexp'_hash +* median bucket length: 7 / 7 +* biggest bucket length: 205 / 36 +* found/new lexp entries: - / 2 *) + +let lexp_lexp' (e, h) = e +let lexp_hash (e, h) = h + +(* Hash `Lexp` using combine_hash (lxor) with hash of "sub-lexp". *) +let lexp'_hash (lp : lexp') = + match lp with + | Imm s -> U.combine_hash 1 (Hashtbl.hash s) + | SortLevel l + -> U.combine_hash 2 + (match l with + | SLz -> Hashtbl.hash l + | SLsucc lp -> lexp_hash lp + | SLlub (lp1, lp2) + -> U.combine_hash (lexp_hash lp1) (lexp_hash lp2)) + | Sort (l, s) + -> U.combine_hash 3 (U.combine_hash (Hashtbl.hash l) + (match s with + | Stype lp -> lexp_hash lp + | StypeOmega -> Hashtbl.hash s + | StypeLevel -> Hashtbl.hash s)) + | Builtin (v, t, m) + -> U.combine_hash 4 (U.combine_hash + (U.combine_hash (Hashtbl.hash v) (lexp_hash t)) + (match m with + | Some m -> Hashtbl.hash m + | None -> 404)) + | Var v -> U.combine_hash 5 (Hashtbl.hash v) + | Let (l, ds, e) + -> U.combine_hash 6 (U.combine_hash (Hashtbl.hash l) + (U.combine_hash (U.combine_hashes + (List.map (fun e -> let (n, lp, lt) = e in + (U.combine_hash (Hashtbl.hash n) + (U.combine_hash (lexp_hash lp) (lexp_hash lt)))) + ds)) + (lexp_hash e))) + | Arrow (k, v, t1, l, t2) + -> U.combine_hash 7 (U.combine_hash + (U.combine_hash (Hashtbl.hash k) (Hashtbl.hash v)) + (U.combine_hash (lexp_hash t1) + (U.combine_hash (Hashtbl.hash l) (lexp_hash t2)))) + | Lambda (k, v, t, e) + -> U.combine_hash 8 (U.combine_hash + (U.combine_hash (Hashtbl.hash k) (Hashtbl.hash v)) + (U.combine_hash (lexp_hash t) (lexp_hash e))) + | Inductive (l, n, a, cs) + -> U.combine_hash 9 (U.combine_hash + (U.combine_hash (Hashtbl.hash l) (Hashtbl.hash n)) + (U.combine_hash (U.combine_hashes + (List.map (fun e -> let (ak, n, lt) = e in + (U.combine_hash (Hashtbl.hash ak) + (U.combine_hash (Hashtbl.hash n) (lexp_hash lt)))) + a)) + (Hashtbl.hash cs))) + | Cons (t, n) -> U.combine_hash 10 (U.combine_hash (lexp_hash t) (Hashtbl.hash n)) + | Case (l, e, rt, bs, d) + -> U.combine_hash 11 (U.combine_hash + (U.combine_hash (Hashtbl.hash l) (lexp_hash e)) + (U.combine_hash (lexp_hash rt) (U.combine_hash + (Hashtbl.hash bs) + (match d with + | Some (n, lp) -> U.combine_hash (Hashtbl.hash n) (lexp_hash lp) + | _ -> 0)))) + | Metavar (id, s, v) + -> U.combine_hash 12 (U.combine_hash id + (U.combine_hash (Hashtbl.hash s) (Hashtbl.hash v))) + | Call (e, args) + -> U.combine_hash 13 (U.combine_hash (lexp_hash e) + (U.combine_hashes (List.map (fun e -> let (ak, lp) = e in + (U.combine_hash (Hashtbl.hash ak) (lexp_hash lp))) + args))) + | Susp (lp, subst) + -> U.combine_hash 14 (U.combine_hash (lexp_hash lp) (Hashtbl.hash subst)) + +(* Equality function for hash table + * using physical equality for "sub-lexp" and compare for `subst`. *) +let hc_eq e1 e2 = + match (lexp_lexp' e1, lexp_lexp' 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)) -> e1 == e2 + | (SortLevel (SLlub (e11, e21)), SortLevel (SLlub (e12, e22))) + -> e11 == e12 && e21 == e22 + | (Sort (_, StypeOmega), Sort (_, StypeOmega)) -> true + | (Sort (_, StypeLevel), Sort (_, StypeLevel)) -> true + | (Sort (_, Stype e1), Sort (_, Stype e2)) -> e1 == e2 + | (Builtin ((_, name1), _, _), Builtin ((_, name2), _, _)) -> name1 = name2 + | (Var (_, i1), Var (_, i2)) -> i1 = i2 + | (Susp (e1, s1), Susp (e2, s2)) -> e1 == e2 && compare s1 s2 = 0 + | (Let (_, defs1, e1), Let (_, defs2, e2)) + -> e1 == e2 && List.for_all2 + (fun (_, e1, t1) (_, e2, t2) -> t1 == t2 && e1 == e2) defs1 defs2 + | (Arrow (ak1, _, t11, _, t21), Arrow (ak2, _, t12, _, t22)) + -> ak1 = ak2 && t11 == t12 && t21 == t22 + | (Lambda (ak1, _, t1, e1), Lambda (ak2, _, t2, e2)) + -> ak1 = ak2 && t1 == t2 && e1 == e2 + | (Call (e1, as1), Call (e2, as2)) + -> e1 == e2 && List.for_all2 + (fun (ak1, e1) (ak2, e2) -> ak1 = ak2 && e1 == e2) as1 as2 + | (Inductive (_, l1, as1, ctor1), Inductive (_, l2, as2, ctor2)) + -> l1 = l2 && List.for_all2 + (fun (ak1, _, e1) (ak2, _, e2) -> ak1 = ak2 && e1 == e2) as1 as2 + && SMap.equal (List.for_all2 + (fun (ak1, _, e1) (ak2, _, e2) -> ak1 = ak2 && e1 == e2)) ctor1 ctor2 + | (Cons (t1, (_, l1)), Cons (t2, (_, l2))) -> t1 == t2 && l1 = l2 + | (Case (_, e1, r1, ctor1, def1), Case (_, e2, r2, ctor2, def2)) + -> e1 == e2 && r1 == r2 && SMap.equal + (fun (_, fields1, e1) (_, fields2, e2) + -> e1 == e2 && List.for_all2 + (fun (ak1, _) (ak2, _) -> ak1 = ak2) fields1 fields2) ctor1 ctor2 + && (match (def1, def2) with + | (Some (_, e1), Some (_, e2)) -> e1 == e2 + | _ -> def1 = def2) + | (Metavar (i1, s1, _), Metavar (i2, s2, _)) + -> i1 = i2 && compare s1 s2 = 0 + | _ -> false

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 hash = Hashtbl.hash - end) + let equal x y = hc_eq x y + let hash = lexp_hash + end) + let hc_table : WHC.t = WHC.create 1000 -let hc : lexp -> lexp = WHC.merge hc_table

+let hc (l : lexp') : lexp = + WHC.merge hc_table (l, lexp'_hash l)

let mkImm s = hc (Imm s) let mkSortLevel l = hc (SortLevel l) @@ -198,14 +317,16 @@ let mkInductive (l, n, a, cs) = hc (Inductive (l, n, a, cs)) let mkCons (t, n) = hc (Cons (t, n)) let mkCase (l, e, rt, bs, d) = hc (Case (l, e, rt, bs, d)) let mkMetavar (n, s, v) = hc (Metavar (n, s, v)) -let mkCall (f, es) - = 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 mkCall (f, es) = + match lexp_lexp' f, es with + | Call (f', es'), _ -> hc (Call (f', es' @ es)) + | _, [] -> f + | _ -> hc (Call (f, es)) + +let impossible = mkImm Sexp.dummy_epsilon + +let lexp_head e = + match lexp_lexp' e with | Imm s -> if e = impossible then "impossible" else "Imm" ^ sexp_string s | Var _ -> "Var" | Let _ -> "let" @@ -222,7 +343,8 @@ and lexp_head e = | Sort _ -> "Sort" | SortLevel _ -> "SortLevel"

-let mkSLlub' (e1, e2) = match (e1, e2) with +let mkSLlub' (e1, e2) = + match (lexp_lexp' e1, lexp_lexp' 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) @@ -235,11 +357,54 @@ let mkSLlub' (e1, e2) = match (e1, e2) with | _ -> 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 - | _ -> Log.log_fatal ~section:"internal" "SLsucc of non-level " - +let mkSLsucc e = + match lexp_lexp' e with + | SortLevel _ | Var _ | Metavar _ | Susp _ + -> SLsucc e + | _ -> Log.log_fatal ~section:"internal" "SLsucc of non-level " + +(********************** Lexp tests ************************) + +let pred_imm l pred = + match lexp_lexp' l with + | Imm s -> pred s + | _ -> false + +let is_imm l = pred_imm l (fun e -> true) + +let pred_var l pred = + match lexp_lexp' l with + | Var v -> pred v + | _ -> false + +let is_var l = pred_var l (fun e -> true) + +let get_var l = + match lexp_lexp' l with + | Var v -> v + | _ -> Log.log_fatal ~section:"internal" "Lexp is not Var " + +let get_var_db_index v = + let (n, idx) = v in idx + +let get_var_vname v = + let (n, idx) = v in n + +let pred_inductive l pred = + match lexp_lexp' l with + | Inductive (l, n, a, cs) -> pred (l, n, a, cs) + | _ -> false + +let get_inductive l = +match lexp_lexp' l with + | Inductive (l, n, a, cs) -> (l, n, a, cs) + | _ -> Log.log_fatal ~section:"internal" "Lexp is not Inductive " + +let get_inductive_ctor i = + let (l, n, a, cs) = i in cs + +let is_inductive l = pred_inductive l (fun e -> true) + (********* Helper functions to use the Subst operations *********) (* This basically "ties the knot" between Subst and Lexp. * Maybe it would be cleaner to just move subst.ml into lexp.ml @@ -276,7 +441,7 @@ let rec mkSusp e s = (* We apply the substitution eagerly to some terms. * There's no deep technical reason for that: * it just seemed like a good idea to do it eagerly when it's easy. *) - match e with + match lexp_lexp' e with | Imm _ -> e | Builtin _ -> e | Susp (e, s') -> mkSusp_memo e (scompose s' s) @@ -338,7 +503,7 @@ let _ = assert (S.identity_p (scompose (S.shift 5) (sunshift 5)))

let rec lexp_location e = - match e with + match lexp_lexp' e with | Sort (l,_) -> l | SortLevel (SLsucc e) -> lexp_location e | SortLevel (SLlub (e, _)) -> lexp_location e @@ -365,10 +530,10 @@ 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 + match lexp_lexp' 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)) @@ -424,14 +589,15 @@ 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 + match lexp_lexp' 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 = + match lexp_lexp' e with | Imm _ -> e | SortLevel (SLz) -> e | SortLevel (SLsucc e) -> mkSortLevel (mkSLsucc (clean s e)) @@ -468,7 +634,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) -> mkCons (clean s it, name) | Case (l, e, ret, cases, default) -> mkCase (l, clean s e, clean s ret, SMap.map (fun (l, cargs, e) @@ -495,8 +661,8 @@ 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) + match lexp_lexp' lxp with + | Susp _ -> lexp_unparse (nosusp lxp) | Imm (sexp) -> sexp | Builtin ((l,name), _, _) -> Symbol (l, "##" ^ name) (* FIXME: Add a Sexp syntax for debindex references. *) @@ -626,7 +792,7 @@ and subst_string s = match s with -> "(↑"^ string_of_int o ^ " " ^ subst_string (S.cons l s) ^ ")"

and lexp_name e = - match e with + match lexp_lexp' e with | Imm _ -> lexp_string e | Var _ -> lexp_string e | _ -> lexp_head e @@ -716,7 +882,7 @@ 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 + match lexp_lexp' expr with | Lambda _ -> lkp "lambda" | Case _ -> lkp "case" | Let _ -> lkp "let" @@ -784,14 +950,15 @@ 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 = + match lexp_lexp' fname with | Builtin ((_, name), _, _) -> name, 0 | Var((_, Some name), idx) -> name, idx | Lambda _ -> "__", 0 | Cons _ -> "__", 0 | _ -> "__", -1 in

- match exp with + match lexp_lexp' exp with | Imm(value) -> (match value with | String (_, s) -> tval (""" ^ s ^ """) | Integer(_, s) -> tval (string_of_int s) @@ -902,9 +1069,6 @@ and lexp_str ctx (exp : lexp) : string =

| Builtin ((_, name), _, _) -> "##" ^ name

- | 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_ω"

@@ -913,6 +1077,14 @@ and lexp_str ctx (exp : lexp) : string = | SortLevel (SLlub (e1, e2)) -> "(##TypeLevel.∪ " ^ lexp_string e1 ^ " " ^ lexp_string e2 ^ ")"

+ | Sort (_, Stype l) + -> match lexp_lexp' l with + | SortLevel SLz -> "##Type" + | SortLevel (SLsucc lp) + when (match lexp_lexp' lp with SortLevel SLz -> true | _ -> false) + -> "##Type1" + | _ -> "(##Type_ " ^ lexp_string l ^ ")" + and lexp_str_ctor ctx ctors =

let pretty = pp_pretty ctx in @@ -947,11 +1119,8 @@ and lexp_str_decls ctx decls =

let rec eq e1 e2 = 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 + match (lexp_lexp' e1, lexp_lexp' e2) with + | (Imm s1, Imm s2) -> sexp_equal s1 s2 | (SortLevel SLz, SortLevel SLz) -> true | (SortLevel (SLsucc e1), SortLevel (SLsucc e2)) -> eq e1 e2 | (SortLevel (SLlub (e11, e21)), SortLevel (SLlub (e12, e22))) @@ -961,37 +1130,31 @@ let rec 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) - defs1 defs2 + -> 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 | (Lambda (ak1, _, t1, e1), Lambda (ak2, _, t2, 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) - 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) - as1 as2 - && SMap.equal (List.for_all2 (fun (ak1, _, e1) (ak2, _, e2) - -> ak1 = ak2 && eq e1 e2)) - cases1 cases2 + -> eq e1 e2 && List.for_all2 + (fun (ak1, e1) (ak2, e2) -> ak1 = ak2 && eq e1 e2) as1 as2 + | (Inductive (_, l1, as1, ctor1), Inductive (_, l2, as2, ctor2)) + -> l1 = l2 && 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)) ctor1 ctor2 | (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 - && SMap.equal (fun (_, fields1, e1) (_, fields2, e2) - -> eq e1 e2 && List.for_all2 (fun (ak1, _) (ak2, _) - -> ak1 = ak2) - fields1 fields2) - cases1 cases2 + | (Case (_, e1, r1, ctor1, def1), Case (_, e2, r2, ctor2, def2)) + -> eq e1 e2 && eq r1 r2 && SMap.equal + (fun (_, fields1, e1) (_, fields2, e2) -> eq e1 e2 && List.for_all2 + (fun (ak1, _) (ak2, _) -> ak1 = ak2) fields1 fields2) ctor1 ctor2 && (match (def1, def2) with - | (Some (_, e1), Some (_, e2)) -> eq e1 e2 - | _ -> def1 = def2) + | (Some (_, e1), Some (_, e2)) -> eq e1 e2 + | _ -> def1 = def2) | (Metavar (i1, s1, _), Metavar (i2, s2, _)) -> if i1 == i2 then subst_eq s1 s2 else (match (metavar_lookup i1, metavar_lookup i2) with @@ -1024,4 +1187,3 @@ and subst_eq s1 s2 = eq e1 (mkSusp e2 (S.shift o)) && subst_eq s1 (S.mkShift s2 o) | _ -> false -

===================================== src/opslexp.ml ===================================== @@ -132,78 +132,82 @@ let lexp_close lctx e = * but only on *types*. If you must use it on code, be sure to use its * return value as little as possible since WHNF will inherently introduce * 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 lexp_whnf_aux e (ctx : DB.lexp_context) : lexp = +let rec lexp_whnf_aux e (ctx : DB.lexp_context) : lexp = + match lexp_lexp' e with | Var v -> (match lookup_value ctx v with | None -> e (* We can do this blindly even for recursive definitions! * IOW the risk of inf-looping should only show up when doing * things like full normalization (e.g. lexp_conv_p). *) - | Some e' -> lexp_whnf e' ctx) - | Susp (e, s) -> lexp_whnf (push_susp e s) ctx - | Call (e, []) -> lexp_whnf e ctx + | Some e' -> lexp_whnf_aux e' ctx) + | Susp (e, s) -> lexp_whnf_aux (push_susp e s) ctx + | Call (e, []) -> lexp_whnf_aux e ctx | Call (f, (((_, arg)::args) as xs)) -> - (match lexp_whnf f ctx with + (match lexp_lexp' (lexp_whnf_aux f ctx) 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 * we can't really make sure we always reduce the arg to a value. *) - lexp_whnf (mkCall (push_susp body (S.substitute (lexp_whnf arg ctx)), + lexp_whnf_aux (mkCall (push_susp body (S.substitute (lexp_whnf_aux arg ctx)), args)) ctx | Call (f', xs1) -> mkCall (f', List.append xs1 xs) | _ -> e) (* Keep `e`, assuming it's more readable! *) | Case (l, e, rt, branches, default) -> - let e' = lexp_whnf e ctx in + let e' = lexp_whnf_aux e ctx in let reduce name aargs = try let (_, _, branch) = SMap.find name branches in let (subst, _) = List.fold_left (fun (s,d) (_, arg) -> - (S.cons (L.mkSusp (lexp_whnf arg ctx) (S.shift d)) s, + (S.cons (L.mkSusp (lexp_whnf_aux arg ctx) (S.shift d)) s, d + 1)) (S.identity, 0) aargs in - lexp_whnf (push_susp branch subst) ctx + lexp_whnf_aux (push_susp branch subst) ctx with Not_found -> match default with | Some (v,default) - -> lexp_whnf (push_susp default (S.substitute e')) ctx + -> lexp_whnf_aux (push_susp default (S.substitute e')) ctx | _ -> Log.log_error ~section:"WHNF" ~loc:l ("Unhandled constructor " ^ name ^ "in case expression"); mkCase (l, e, rt, branches, default) in - (match e' with + (match lexp_lexp' e' with | Cons (_, (_, name)) -> reduce name [] | Call (f, aargs) -> - (match lexp_whnf f ctx with + (match lexp_lexp' (lexp_whnf_aux f ctx) with | Cons (_, (_, name)) -> reduce name aargs | _ -> mkCase (l, e, rt, branches, default)) | _ -> mkCase (l, e, rt, branches, default)) | Metavar (idx, s, _) -> (match metavar_lookup idx with - | MVal e -> lexp_whnf (push_susp e s) ctx + | MVal e -> lexp_whnf_aux (push_susp e s) ctx | _ -> e)

(* FIXME: I'd really prefer to use "native" recursive substitutions, using * ideally a trick similar to the db_offsets in lexp_context! *) | Let (l, defs, body) - -> lexp_whnf (push_susp body (lexp_defs_subst l S.identity defs)) ctx + -> lexp_whnf_aux (push_susp body (lexp_defs_subst l S.identity defs)) ctx

- | e -> e + | elem -> e

- in lexp_whnf e ctx + in lexp_whnf_aux e ctx

+let lexp'_whnf e (ctx : DB.lexp_context) : lexp' = + lexp_lexp' (lexp_whnf_aux e ctx) + +let lexp_whnf e (ctx : DB.lexp_context) : lexp = + lexp_whnf_aux e ctx

(** A very naive implementation of sets of pairs of lexps. *) 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); - try let _ = List.find (fun (e1', e2') + = try let _ = List.find (fun (e1', e2') -> L.eq e1 e1' && L.eq e2 e2') s in true @@ -230,7 +234,8 @@ 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) = + match lexp_lexp' 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 +264,7 @@ 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 + match (lexp_lexp' e1', lexp_lexp' 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 +337,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 = 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' in - let ce2 = level_canon e2' 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 *) @@ -353,7 +360,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 = lexp'_whnf k1 ctx1 in + let lwhnf2 = lexp'_whnf k2 ctx2 in + match (lwhnf1, lwhnf2) with | (Sort (_, s1), Sort (_, s2)) -> (match s1, s2 with | (Stype l1, Stype l2) @@ -408,7 +417,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`. *) - match e with Var (_, idx) -> DB.set_mem idx nerased + match lexp_lexp' e with Var (_, idx) -> DB.set_mem idx nerased | _ -> false) defs in if not (List.mem true es) then nerased else @@ -430,14 +439,13 @@ 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 + (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 lexp_lexp' e with | Imm (Float (_, _)) -> DB.type_float | Imm (Integer (_, _)) -> DB.type_int | Imm (String (_, _)) -> DB.type_string @@ -528,7 +536,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 - match lexp_whnf ft ctx with + match lexp'_whnf ft ctx with | Arrow (ak', v, t1, l, t2) -> if not (ak == ak') then (error_tc ~loc:(lexp_location arg) @@ -551,8 +559,8 @@ 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 = lexp_whnf (check_type erased ictx t) ictx in + match lexp_lexp' lwhnf with | Sort (_, Stype _) when ak == P.Aerasable && impredicative_erase -> level @@ -570,7 +578,7 @@ let rec check'' erased ctx e = ("Field type " ^ lexp_string t ^ " is not a Type! (" - ^ lexp_string tt ^")"); + ^ lexp_string lwhnf ^")"); level), DB.lctx_extend ictx v Variable t, DB.set_sink 1 erased, @@ -590,12 +598,13 @@ 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 = + match lexp_lexp' 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 + (match lexp'_whnf it ctx, aargs with | Inductive (_, _, fargs, constructors), aargs -> let rec mksubst s fargs aargs = match fargs, aargs with @@ -644,8 +653,8 @@ 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) + -> (match lexp'_whnf t ctx with + | Inductive (l, _, fargs, constructors) -> (try let fieldtypes = SMap.find name constructors in let rec indtype fargs start_index = @@ -732,7 +741,8 @@ 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 = + match lexp_lexp' e with | Imm _ -> fv_empty | SortLevel SLz -> fv_empty | SortLevel (SLsucc e) -> fv e @@ -807,7 +817,7 @@ 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 + match lexp_lexp' e with | Imm (Float (_, _)) -> DB.type_float | Imm (Integer (_, _)) -> DB.type_int | Imm (String (_, _)) -> DB.type_string @@ -838,7 +848,7 @@ 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 + -> match lexp'_whnf ft ctx with | Arrow (ak', v, t1, l, t2) -> mkSusp t2 (S.substitute arg) | _ -> ft) @@ -854,7 +864,7 @@ 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 + ((match lexp'_whnf (get_type ictx t) ictx with | Sort (_, Stype _) when ak == P.Aerasable && impredicative_erase -> level @@ -878,7 +888,7 @@ let rec get_type ctx e = tct | Case (l, e, ret, branches, default) -> ret | Cons (t, (l, name)) - -> (match lexp_whnf t ctx with + -> (match lexp'_whnf t ctx with | Inductive (l, _, fargs, constructors) -> (try let fieldtypes = SMap.find name constructors in @@ -911,9 +921,8 @@ let rec get_type ctx e =

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

-let rec erase_type (lxp: L.lexp): E.elexp = - - match lxp with +let rec erase_type (lxp: lexp): E.elexp = + match lexp_lexp' lxp with | L.Imm(s) -> E.Imm(s) | L.Builtin(v, _, _) -> E.Builtin(v) | L.Var(v) -> E.Var(v) @@ -943,7 +952,7 @@ let rec erase_type (lxp: L.lexp): E.elexp = | L.Sort _ -> E.Type lxp (* Still useful to some extent. *) | L.Inductive(l, label, _, _) -> E.Type lxp - | Metavar (idx, s, _) + | L.Metavar (idx, s, _) -> (match metavar_lookup idx with | MVal e -> erase_type (push_susp e s) | MVar (_, t, _) @@ -1004,7 +1013,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");*) - Call (Cons (Inductive (loc, type_label, [], + + mkCall (mkCons (mkInductive (loc, type_label, [], SMap.add cons_name (List.map (fun (oname, t) -> (P.Aimplicit, oname, @@ -1024,10 +1034,10 @@ let ctx2tup ctx nctx = -> (P.Aimplicit, mkVar (oname, offset - i - 1))) types) | (DB.CVlet (name, LetDef (_, e), t, _) :: blocs) - -> Let (loc, [(name, mkSusp e (S.shift 1), t)], + -> mkLet (loc, [(name, mkSusp e (S.shift 1), t)], mk_lets_and_tup blocs ((name, t) :: types)) | (DB.CVfix (defs, _) :: blocs) - -> Let (loc, defs, + -> mkLet (loc, defs, mk_lets_and_tup blocs (List.append (List.rev (List.map (fun (oname, _, t)

===================================== src/sexp.ml ===================================== @@ -45,6 +45,15 @@ type token = sexp let epsilon l = Symbol (l, "") let dummy_epsilon = epsilon dummy_location

+(********************** Sexp tests **********************) + +let pred_symbol s pred = + match s with + | Symbol (_, n) -> pred n + | _ -> false + +let is_symbol e = pred_symbol e (fun e -> true) + (**************** Hash-consing symbols *********************)

module SHash = Hashtbl.Make (struct type t = string

===================================== src/unification.ml ===================================== @@ -61,7 +61,8 @@ 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 = + match lexp_lexp' e with | Imm _ -> false | SortLevel SLz -> false | SortLevel (SLsucc e) -> oi e @@ -189,21 +190,21 @@ 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 + match (lexp_lexp' e1', lexp_lexp' 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' + | (_, Metavar (idx, s, _)) -> unify_metavar ctx idx s e2' e1' + | (Metavar (idx, s, _), _) -> unify_metavar ctx idx s e1' e2' + | (_, Call _) -> 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 _ , _) -> unify_arrow e1' e2' ctx vs' + | (Lambda _, _) -> unify_lambda e1' e2' ctx vs' + | (Call _, _) -> 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 _, _) -> unify_sort e1' e2' ctx vs' + | (SortLevel _, _) -> unify_sortlvl e1' e2' ctx vs' | (Inductive (_loc1, label1, args1, consts1), Inductive (_loc2, label2, args2, consts2)) -> (* print_string ("Unifying inductives " @@ -227,7 +228,7 @@ and unify' (e1: lexp) (e2: lexp) *) and unify_arrow (arrow: lexp) (lxp: lexp) ctx vs : return_type = - match (arrow, lxp) with + match (lexp_lexp' arrow, lexp_lexp' lxp) with | (Arrow (var_kind1, v1, ltype1, _, lexp1), Arrow (var_kind2, _, ltype2, _, lexp2)) -> if var_kind1 = var_kind2 @@ -250,7 +251,7 @@ 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 + match (lexp_lexp' lambda, lexp_lexp' lxp) with | (Lambda (var_kind1, v1, ltype1, lexp1), Lambda (var_kind2, _, ltype2, lexp2)) -> if var_kind1 = var_kind2 @@ -300,7 +301,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 - match lxp2 with + match lexp_lexp' lxp2 with | Metavar (idx2, s2, name) -> if idx = idx2 then match common_subset ctx s1 s2 with @@ -370,7 +371,7 @@ 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 + match (lexp_lexp' call, lexp_lexp' 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 +440,7 @@ 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 + match lexp_lexp' sortlvl, lexp_lexp' lxp with | (SortLevel s, SortLevel s2) -> (match s, s2 with | SLz, SLz -> [] | SLsucc l1, SLsucc l2 -> unify' l1 l2 ctx vs @@ -456,7 +457,7 @@ 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 + match lexp_lexp' sort_, lexp_lexp' lxp with | (Sort (_, srt), Sort (_, srt2)) -> (match srt, srt2 with | Stype lxp1, Stype lxp2 -> unify' lxp1 lxp2 ctx vs | StypeOmega, StypeOmega -> []

===================================== src/util.ml ===================================== @@ -45,6 +45,15 @@ type vref = vname * db_index

type bottom = | B_o_t_t_o_m_ of bottom

+let get_vname_name_option vname = + let (loc, name) = vname in name + +let get_vname_name vname = + let (loc, name) = vname in + match name with + | Some n -> n + | _ -> "" (* FIXME: Replace with dummy_name ? *) + (* print debug info *) let loc_string loc = "Ln " ^ (Fmt.ralign_int loc.line 3) ^ ", cl " ^ (Fmt.ralign_int loc.column 3) @@ -116,3 +125,22 @@ let option_map (fn : 'a -> 'b) (opt : 'a option) : 'b option = match opt with | None -> None | Some x -> Some (fn x) + +(* It seemed good to use the prime number 31. + * FIXME: Pick another one ? *) +let combine_hash e1 e2 = (e1 * 31) lxor e2 + +let rec combine_hashes li = + match li with + | [] -> 31 + | e :: l -> combine_hash (e * 31) (combine_hashes l) + +let get_stats_hashtbl stats = + let (tl, ne, sumb, smallb, medianb, bigb) = stats in + Printf.printf "\n\ttable length: %i\n + number of entries: %i\n + sum of bucket lengths: %i\n + smallest bucket length: %i\n + median bucket length: %i\n + biggest bucket length: %i\n" + tl ne sumb smallb medianb bigb

===================================== tests/unify_test.ml ===================================== @@ -125,14 +125,14 @@ let input_type_t = generate_ltype_from_str str_type2

let generate_testable (_: lexp list) : ((lexp * lexp * result) list) =

- ( Lambda ((Anormal), + ( mkLambda ((Anormal), (Util.dummy_location, Some "L1"), - Var((Util.dummy_location, Some "z"), 3), - Imm (Integer (Util.dummy_location, 3))), - Lambda ((Anormal), + mkVar((Util.dummy_location, Some "z"), 3), + mkImm (Integer (Util.dummy_location, 3))), + mkLambda ((Anormal), (Util.dummy_location, Some "L2"), - Var((Util.dummy_location, Some "z"), 4), - Imm (Integer (Util.dummy_location, 3))), Nothing ) + mkVar((Util.dummy_location, Some "z"), 4), + mkImm (Integer (Util.dummy_location, 3))), Nothing )

::(input_induct , input_induct , Equivalent) (* 2 *) ::(input_int_4 , input_int_4 , Equivalent) (* 3 *) @@ -183,8 +183,8 @@ let generate_testable (_: lexp list) : ((lexp * lexp * result) list) =

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

- ::(Metavar (0, S.identity, (Util.dummy_location, Some "M")), - Var ((Util.dummy_location, Some "x"), 3), Unification) (* 45 *) + ::(mkMetavar (0, S.identity, (Util.dummy_location, Some "M")), + mkVar ((Util.dummy_location, Some "x"), 3), Unification) (* 45 *)

::[]

View it on GitLab: https://gitlab.com/monnier/typer/-/compare/f0b33b284588b1cc628f0b482bb00afe5...