Alice de Berny pushed to branch alice at Stefan / Typer

Commits: e0c92648 by irradiee at 2020-07-01T18:33:36-04:00 check performance

- - - - -

6 changed files:

- GNUmakefile - src/REPL.ml - src/lexp.ml - src/lexp_type.ml - src/subst.ml - src/util.ml

Changes:

===================================== GNUmakefile ===================================== @@ -8,7 +8,8 @@ SRC_FILES := $(wildcard ./src/*.ml) CPL_FILES := $(wildcard ./$(BUILDDIR)/src/*.cmo) TEST_FILES := $(wildcard ./tests/*_test.ml)

-OBFLAGS = -tag debug -tag profile -lib str -build-dir $(BUILDDIR) -pkg zarith +# @TODO: remove -pkg unix +OBFLAGS = -tag debug -tag profile -lib str -build-dir $(BUILDDIR) -pkg zarith -pkg unix # OBFLAGS := -I $(SRCDIR) -build-dir $(BUILDDIR) -pkg str # OBFLAGS_DEBUG := -tag debug -tag profile -tag "warn(+20)" # OBFLAGS_RELEASE := -tag unsafe -tag inline @@ -45,6 +46,7 @@ debug: $(OCAMLBUILD) src/debug_util.$(COMPILE_MODE) -I src $(OBFLAGS) @$(MV) $(BUILDDIR)/src/debug_util.$(COMPILE_MODE) $(BUILDDIR)/debug_util

+ # interactive typer typer: # ============================

===================================== src/REPL.ml ===================================== @@ -203,10 +203,9 @@ let help_msg = %help (%h) : print help "

- -let readfiles files (i, lctx, rctx) prt = +let readfiles_aux files (i, lctx, rctx) prt = (* Read specified files *) - List.fold_left (fun (i, lctx, rctx) file -> + List.fold_left (fun (i, lctx, rctx) file ->

(if prt then ( print_string " In["; ralign_print_int i 2; print_string "] >> "; @@ -221,6 +220,9 @@ let readfiles files (i, lctx, rctx) prt = ) (i, lctx, rctx) files

+let readfiles files (i, lctx, rctx) prt = + let res = readfiles_aux files (i, lctx, rctx) prt in + (print_total_hctime !hc_total_time; res)

(* Specials commands %[command-name] [args] *) let rec repl i clxp rctx = @@ -232,8 +234,8 @@ 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 (WHC.stats hc_table) !lshrct !sshrct) - | "%scollisions" | "%scl" -> (get_stats (Subst.WHCSB.stats Subst.hcsb_table) !lshrct !sshrct) + | "%lcollisions" | "%cl" -> (get_stats_hashtbl (WHC.stats hc_table) !Subst.sshrct !Subst.nf_sshrct) + | "%scollisions" | "%scl" -> (get_stats_hashtbl (Subst.WHCSB.stats Subst.hcsb_table) !Subst.sshrct !Subst.nf_sshrct)

(* command with arguments *) | _ when (ipt.[0] = '%' && ipt.[1] != ' ') -> ( @@ -243,9 +245,16 @@ let rec repl i clxp rctx = try readfiles args (i, clxp, rctx) false with Log.Stop_Compilation msg -> - (handle_stopped_compilation msg; (i,clxp,rctx)) - in - repl clxp rctx; + (handle_stopped_compilation msg; (i,clxp,rctx)) in + repl clxp rctx + | "%readfiletime"::args -> + (time_process := true; + let (i, clxp, rctx) = + try + get_unix_stats_processtime (fun () -> (readfiles args (i, clxp, rctx) false)) + with Log.Stop_Compilation msg -> + (handle_stopped_compilation msg; (i,clxp,rctx)) in + repl clxp rctx) | "%who"::args | "%w"::args -> ( let _ = match args with | ["all"] -> dump_rte_ctx rctx @@ -287,6 +296,7 @@ let arg_defs = [ ("--verbosity", Arg.String Log.set_typer_log_level_str, "Set the logging level"); ("-v", Arg.Unit Log.increment_log_level, "Increment verbosity"); + ("--time", Arg.Set time_process, "Get time for process"); (* ("--debug", Arg.Set arg_debug, "Print the Elexp representation") *) (*"-I", Arg.String (fun f -> searchpath := f::!searchpath), @@ -310,9 +320,16 @@ let main () =

let (i, ectx, rctx) = ( try - let res = - readfiles (List.rev !arg_files) (1, ectx, rctx) (not !arg_batch) in - print_and_clear_log (); res + if !time_process + then + let res = + get_unix_stats_processtime (fun () -> (readfiles + (List.rev !arg_files) (1, ectx, rctx) (not !arg_batch))) in + (print_and_clear_log (); res) + else + let res = + readfiles_aux (List.rev !arg_files) (1, ectx, rctx) (not !arg_batch) in + (print_and_clear_log (); res) with | Log.Stop_Compilation msg -> handle_stopped_compilation msg; exit 1

===================================== src/lexp.ml ===================================== @@ -35,160 +35,115 @@ open Grammar

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

- (** hash-consing test ** - * with: Hashtbl.hash - lexp'_hash - * median bucket length: 7 - 7 - * biggest bucket length: 205 - 22 *) - - let lexp_lexp' (e, h) = e - -let rec apply_lxor (map : int list) : int = - match map with - | [] -> 31 - | e :: l -> (e * 31) lxor (apply_lxor l) - -let attributemap_combine_hash (k: (int * string)) (v: lexp) (p: int) : int = -shrct_inc lshrct 1; - (p * 31) lxor (((Hashtbl.hash k) * 31) lxor (lexp_hash v)) - -let ind_stringmap_combine_hash (k: string) (v: ((arg_kind * vname * ltype) list)) (p: int) : int = - (p * 31) lxor ((Hashtbl.hash k) * 31) lxor - (apply_lxor (List.map (fun e -> let (ak, n, lt) = e in - shrct_inc lshrct 1; - (U.combine_hash (Hashtbl.hash ak) - (U.combine_hash (Hashtbl.hash n) (lexp_hash lt)))) v)) - -let case_stringmap_combine_hash (k: string) (v: (U.location * (arg_kind * vname) list * lexp)) (p: int) : int = - shrct_inc lshrct 1; - let (loc, li, lp) = v in - (p * 31) lxor ((Hashtbl.hash k) * 31) lxor - (Hashtbl.hash loc) lxor (Hashtbl.hash li) lxor (lexp_hash lp) - - -(* Hashtbl.hash for not lexp types - * TODO: - find something else - * - extract the first arg of 2 arg types ? (SMap) *) - let lexp'_hash (expr : lexp') = +(** hash-consing test ** +* with: Hashtbl.hash - lexp'_hash +* median bucket length: 7 - 7 +* biggest bucket length: 205 - 22 *) + +let lexp_lexp' (e, h) = e + +let lexp'_hash (expr : lexp') = match expr 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 -> shrct_inc lshrct 1; lexp_hash lp - | SLlub (lp1, lp2) - -> shrct_inc lshrct 2; U.combine_hash (lexp_hash lp1) (lexp_hash lp2)) + -> 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 -> shrct_inc lshrct 1; lexp_hash lp + | Stype lp -> lexp_hash lp | StypeOmega -> Hashtbl.hash s | StypeLevel -> Hashtbl.hash s)) | Builtin (v, t, m) - -> shrct_inc lshrct 1; U.combine_hash 4 (U.combine_hash + -> U.combine_hash 4 (U.combine_hash (U.combine_hash (Hashtbl.hash v) (lexp_hash t)) (match m with - | Some m -> (AttributeMap.fold attributemap_combine_hash - m 31) - | None -> 404)) + | Some m -> Hashtbl.hash m + | None -> 404)) | Var v -> U.combine_hash 5 (Hashtbl.hash v) | Let (l, ds, e) - -> shrct_inc lshrct 1; - U.combine_hash 6 (U.combine_hash (Hashtbl.hash l) - (U.combine_hash (apply_lxor (List.map (fun e -> let (n, lp, lt) = e in - shrct_inc lshrct 2; - (U.combine_hash (Hashtbl.hash n) (U.combine_hash (lexp_hash lp) (lexp_hash lt)))) - ds)) (lexp_hash 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) - -> shrct_inc lshrct 2; - 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)))) + -> 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) - -> shrct_inc lshrct 2; - 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))) + -> 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 (apply_lxor (List.map (fun e -> let (ak, n, lt) = e in - shrct_inc lshrct 1; + (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)) - (SMap.fold ind_stringmap_combine_hash - cs 21))) - | Cons (t, n) -> shrct_inc lshrct 1; U.combine_hash 10 (U.combine_hash (lexp_hash t) (Hashtbl.hash n)) + (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) - -> shrct_inc lshrct 2; - 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 - (SMap.fold case_stringmap_combine_hash bs 21) - (match d with - | Some (n, lp) -> shrct_inc lshrct 1; U.combine_hash (Hashtbl.hash n) (lexp_hash lp) - | _ -> 0)))) + -> 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) - -> shrct_inc sshrct 1; - U.combine_hash 12 (U.combine_hash id - (U.combine_hash (S.subst_hash s) (Hashtbl.hash v))) + -> U.combine_hash 12 (U.combine_hash id + (U.combine_hash (S.subst_hash s) (Hashtbl.hash v))) | Call (e, args) - -> shrct_inc lshrct 1; U.combine_hash 13 (U.combine_hash (lexp_hash e) - (apply_lxor (List.map (fun e -> let (ak, lp) = e in - shrct_inc lshrct 1; + -> 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) - -> shrct_inc lshrct 1; shrct_inc sshrct 1; - U.combine_hash 14 (U.combine_hash (lexp_hash lp) (S.subst_hash subst)) + -> U.combine_hash 14 (U.combine_hash (lexp_hash lp) (S.subst_hash subst))

let hc_eq e1 e2 = 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 - (* TODO: == via hcs ? *) - | ((Susp (e1, s1) as e), _) -> compare e (lexp_lexp' e2) = 0 - | (_, (Susp (e2, s2) as e)) -> compare (lexp_lexp' e1) e = 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, cases1), Inductive (_, l2, as2, cases2)) - -> 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)) - cases1 cases2 - | (Cons (t1, (_, l1)), Cons (t2, (_, l2))) -> t1 == t2 && l1 = l2 - | (Case (_, e1, r1, cases1, def1), Case (_, e2, r2, cases2, def2)) - -> e1 == e2 && r1 == r2 - && SMap.equal (fun (_, fields1, e1) (_, fields2, e2) - -> e1 == e2 && List.for_all2 (fun (ak1, _) (ak2, _) - -> ak1 = ak2) - fields1 fields2) - cases1 cases2 - && (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 + | (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 && s1 == s2 + | (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, cases1), Inductive (_, l2, as2, cases2)) + -> 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)) cases1 cases2 + | (Cons (t1, (_, l1)), Cons (t2, (_, l2))) -> t1 == t2 && l1 = l2 + | (Case (_, e1, r1, cases1, def1), Case (_, e2, r2, cases2, def2)) + -> e1 == e2 && r1 == r2 && SMap.equal + (fun (_, fields1, e1) (_, fields2, e2) + -> e1 == e2 && List.for_all2 + (fun (ak1, _) (ak2, _) -> ak1 = ak2) fields1 fields2) cases1 cases2 + && (match (def1, def2) with + | (Some (_, e1), Some (_, e2)) -> e1 == e2 + | _ -> def1 = def2) + | (Metavar (i1, s1, _), Metavar (i2, s2, _)) + -> i1 = i2 && s1 == s2 + | _ -> false

module WHC = Weak.Make (struct type t = lexp (* Using (=) instead of `compare` results @@ -200,8 +155,16 @@ module WHC = Weak.Make (struct type t = lexp end)

let hc_table : WHC.t = WHC.create 1000 + +let hc_aux (e : lexp') : lexp = + let lp = (e, lexp'_hash e) in WHC.merge hc_table lp + let hc (e : lexp') : lexp = -let lp = (e, lexp'_hash e) in WHC.merge hc_table lp + if !U.time_process + then + U.inc_hc_total_time (fun () -> hc_aux e) + else + hc_aux e

let impossible = hc (Imm Sexp.dummy_epsilon)

@@ -220,9 +183,9 @@ let mkMetavar (n, s, v) = hc (Metavar (n, s, v)) let mkCall (f, es) = let f' = lexp_lexp' f in match f', es with - | Call (f'', es'), _ -> hc (Call (f'', es' @ es)) - | _, [] -> f - | _ -> hc (Call (f, es)) + | Call (f'', es'), _ -> hc (Call (f'', es' @ es)) + | _, [] -> f + | _ -> hc (Call (f, es))

and lexp_head e = let e' = lexp_lexp' e in @@ -831,128 +794,128 @@ and lexp_str ctx (exp : lexp) : string =

let e' = lexp_lexp' exp in match e' with - | Imm(value) -> (match value with - | String (_, s) -> tval (""" ^ s ^ """) - | Integer(_, s) -> tval (string_of_int s) - | Float (_, s) -> tval (string_of_float s) - | e -> sexp_string e) - - | Susp (e, s) -> lexp_str ctx (push_susp e s) - - | Var ((loc, name), idx) -> maybename name ^ (index idx) ; - - | Metavar (idx, subst, (loc, name)) - (* print metavar result if any *) - -> (match metavar_lookup idx with - | MVal e -> lexp_str ctx e - | _ -> "?" ^ maybename name ^ (subst_string subst) ^ (index idx)) - - | Let (_, decls, body) -> - (* Print first decls without indent *) - let h1, decls, idt_lvl = - match lexp_str_decls inter_ctx decls with - | h1::decls -> h1, decls, 2 - | _ -> "", [], 1 in - - let decls = List.fold_left (fun str elem -> - str ^ nl ^ (make_indent 1) ^ elem ^ " ") h1 decls in - - let n = String.length decls in - (* remove last newline *) - let decls = if (n > 0) then - String.sub decls 0 (n - 2) - else decls in - - (keyword "let ") ^ decls ^ (keyword " in ") ^ newline ^ - (make_indent idt_lvl) ^ (lexp_stri idt_lvl body) - - | Arrow(k, (_, Some name), tp, loc, expr) -> - "(" ^ name ^ " : " ^ (lexp_str' tp) ^ ") " ^ - (kind_str k) ^ " " ^ (lexp_str' expr) - - | Arrow(k, (_, None), tp, loc, expr) -> - "(" ^ (lexp_str' tp) ^ " " - ^ (kind_str k) ^ " " ^ (lexp_str' expr) ^ ")" - - | Lambda(k, (loc, name), ltype, lbody) -> - let arg = "(" ^ maybename name ^ " : " ^ (lexp_str' ltype) ^ ")" in - - (keyword "lambda ") ^ arg ^ " " ^ (kind_str k) ^ newline ^ - (make_indent 1) ^ (lexp_stri 1 lbody) - - | Cons(t, (_, ctor_name)) -> - (keyword "datacons ") ^ (lexp_str' t) ^ " " ^ ctor_name - - | Call(fname, args) -> - let name, idx = get_name fname in - let binop_str op (_, lhs) (_, rhs) = - "(" ^ (lexp_str' lhs) ^ op ^ (index idx) ^ " " ^ (lexp_str' rhs) ^ ")" in - - let print_arg str (arg_type, lxp) = - match arg_type with - | Aerasable when pp_erasable ctx -> str ^ " " ^ (lexp_str' lxp) - | Aimplicit when pp_implicit ctx -> str ^ " " ^ (lexp_str' lxp) - | Anormal -> str ^ " " ^ (lexp_str' lxp) - | _ -> str in ( - - match args with - | [lhs; rhs] when is_binary_op name -> - binop_str (" " ^ (get_binary_op_name name)) lhs rhs - - | _ -> let args = List.fold_left print_arg "" args in - "(" ^ (lexp_str' fname) ^ args ^ ")") - - | Inductive (_, (_, name), [], ctors) -> - (keyword "typecons") ^ " (" ^ name ^") " ^ newline ^ - (lexp_str_ctor ctx ctors) - - | Inductive (_, (_, name), args, ctors) - -> let args_str - = List.fold_left - (fun str (arg_kind, (_, name), ltype) - -> str ^ " (" ^ maybename name ^ " " ^ (kindp_str arg_kind) ^ " " - ^ (lexp_str' ltype) ^ ")") - "" args in - - (keyword "typecons") ^ " (" ^ name ^ args_str ^") " ^ + | Imm(value) -> (match value with + | String (_, s) -> tval (""" ^ s ^ """) + | Integer(_, s) -> tval (string_of_int s) + | Float (_, s) -> tval (string_of_float s) + | e -> sexp_string e) + + | Susp (e, s) -> lexp_str ctx (push_susp e s) + + | Var ((loc, name), idx) -> maybename name ^ (index idx) ; + + | Metavar (idx, subst, (loc, name)) + (* print metavar result if any *) + -> (match metavar_lookup idx with + | MVal e -> lexp_str ctx e + | _ -> "?" ^ maybename name ^ (subst_string subst) ^ (index idx)) + + | Let (_, decls, body) -> + (* Print first decls without indent *) + let h1, decls, idt_lvl = + match lexp_str_decls inter_ctx decls with + | h1::decls -> h1, decls, 2 + | _ -> "", [], 1 in + + let decls = List.fold_left (fun str elem -> + str ^ nl ^ (make_indent 1) ^ elem ^ " ") h1 decls in + + let n = String.length decls in + (* remove last newline *) + let decls = if (n > 0) then + String.sub decls 0 (n - 2) + else decls in + + (keyword "let ") ^ decls ^ (keyword " in ") ^ newline ^ + (make_indent idt_lvl) ^ (lexp_stri idt_lvl body) + + | Arrow(k, (_, Some name), tp, loc, expr) -> + "(" ^ name ^ " : " ^ (lexp_str' tp) ^ ") " ^ + (kind_str k) ^ " " ^ (lexp_str' expr) + + | Arrow(k, (_, None), tp, loc, expr) -> + "(" ^ (lexp_str' tp) ^ " " + ^ (kind_str k) ^ " " ^ (lexp_str' expr) ^ ")" + + | Lambda(k, (loc, name), ltype, lbody) -> + let arg = "(" ^ maybename name ^ " : " ^ (lexp_str' ltype) ^ ")" in + + (keyword "lambda ") ^ arg ^ " " ^ (kind_str k) ^ newline ^ + (make_indent 1) ^ (lexp_stri 1 lbody) + + | Cons(t, (_, ctor_name)) -> + (keyword "datacons ") ^ (lexp_str' t) ^ " " ^ ctor_name + + | Call(fname, args) -> + let name, idx = get_name fname in + let binop_str op (_, lhs) (_, rhs) = + "(" ^ (lexp_str' lhs) ^ op ^ (index idx) ^ " " ^ (lexp_str' rhs) ^ ")" in + + let print_arg str (arg_type, lxp) = + match arg_type with + | Aerasable when pp_erasable ctx -> str ^ " " ^ (lexp_str' lxp) + | Aimplicit when pp_implicit ctx -> str ^ " " ^ (lexp_str' lxp) + | Anormal -> str ^ " " ^ (lexp_str' lxp) + | _ -> str in ( + + match args with + | [lhs; rhs] when is_binary_op name -> + binop_str (" " ^ (get_binary_op_name name)) lhs rhs + + | _ -> let args = List.fold_left print_arg "" args in + "(" ^ (lexp_str' fname) ^ args ^ ")") + + | Inductive (_, (_, name), [], ctors) -> + (keyword "typecons") ^ " (" ^ name ^") " ^ newline ^ (lexp_str_ctor ctx ctors)

- | Case (_, target, _ret, map, dflt) ->( - let str = (keyword "case ") ^ (lexp_str' target) in - let arg_str arg - = List.fold_left (fun str v - -> match v with - | (_, (_, None)) -> str ^ " _" - | (_, (_, Some n)) -> str ^ " " ^ n) - "" arg in - - let str = SMap.fold (fun k (_, arg, exp) str -> - str ^ nl ^ (make_indent 1) ^ - "| " ^ (fun_call k) ^ (arg_str arg) ^ " => " ^ (lexp_stri 1 exp)) - map str in - - match dflt with - | None -> str - | Some (v, df) -> - str ^ nl ^ (make_indent 1) - ^ "| " ^ (match v with (_, None) -> "_" - | (_, Some name) -> name) - ^ " => " ^ (lexp_stri 1 df)) - - | 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_ω" - - | SortLevel (SLz) -> "##TypeLevel.z" - | SortLevel (SLsucc e) -> "(##TypeLevel.succ " ^ lexp_string e ^ ")" - | SortLevel (SLlub (e1, e2)) - -> "(##TypeLevel.∪ " ^ lexp_string e1 ^ " " ^ lexp_string e2 ^ ")" + | Inductive (_, (_, name), args, ctors) + -> let args_str + = List.fold_left + (fun str (arg_kind, (_, name), ltype) + -> str ^ " (" ^ maybename name ^ " " ^ (kindp_str arg_kind) ^ " " + ^ (lexp_str' ltype) ^ ")") + "" args in + + (keyword "typecons") ^ " (" ^ name ^ args_str ^") " ^ + (lexp_str_ctor ctx ctors) + + | Case (_, target, _ret, map, dflt) ->( + let str = (keyword "case ") ^ (lexp_str' target) in + let arg_str arg + = List.fold_left (fun str v + -> match v with + | (_, (_, None)) -> str ^ " _" + | (_, (_, Some n)) -> str ^ " " ^ n) + "" arg in + + let str = SMap.fold (fun k (_, arg, exp) str -> + str ^ nl ^ (make_indent 1) ^ + "| " ^ (fun_call k) ^ (arg_str arg) ^ " => " ^ (lexp_stri 1 exp)) + map str in + + match dflt with + | None -> str + | Some (v, df) -> + str ^ nl ^ (make_indent 1) + ^ "| " ^ (match v with (_, None) -> "_" + | (_, Some name) -> name) + ^ " => " ^ (lexp_stri 1 df)) + + | 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_ω" + + | SortLevel (SLz) -> "##TypeLevel.z" + | SortLevel (SLsucc e) -> "(##TypeLevel.succ " ^ lexp_string e ^ ")" + | SortLevel (SLlub (e1, e2)) + -> "(##TypeLevel.∪ " ^ lexp_string e1 ^ " " ^ lexp_string e2 ^ ")"

and lexp_str_ctor ctx ctors =

@@ -1005,34 +968,28 @@ let rec eq e1 e2 = | (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 + -> 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 + -> 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 | (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 + -> 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 && (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, _)) -> i1 = i2 && subst_eq s1 s2 | _ -> false

===================================== src/lexp_type.ml ===================================== @@ -103,43 +103,43 @@ type ltype = lexp * (Type ℓ, TypeOmega, TypeOmega), * (Type ℓ₁, Type ℓ₂, Type (max l₁ l₂) } *) - and sort = - | Stype of lexp - | StypeOmega - | StypeLevel - and sort_level = - | SLz - | SLsucc of lexp - | SLlub of lexp * lexp - - (* We define here substitutions which take a variable within a source context - * Δₛ and should return an expression valid in target context Δₜ. - * - * The current implementation only handles a very limited subset of such - * substitutions. One of the many limitations is that we can only encode - * substitutions which map variables to variables. - *) - - and db_index = int (* DeBruijn index. *) - and db_offset = int (* DeBruijn index offset. *) - - (* Substitution, i.e. a mapping from db_index to lexp *) - and subst = subst' * int - and subst' = - | Identity of db_offset (* Identity o ≡ id ∘ ↑ₒ *) - | Cons of lexp * subst * db_offset (* Cons (e, s, o) ≡ (e · s) ∘ ↑ₒ *) - (* Myers's extra pointers down the list: - * * int * lexp subst * db_offset *) - (* Lift (n,m) increases indices≥N by M. - * IOW, it takes variables from a source context Δₛ₁Δₛ₂ to a destination - * context Δₛ₁ΔₜΔₛ₂ where Δₛ₂ has size N and Δₜ has size M. *) - (* | Lift of db_index * db_offset *) - - (* Build Myers's "stack" element. *) - (* let mkCons e s o = match s with - * | Cons (_, _, _, sk1, Cons (_, _, _, sk2, s2, o2), o1) when sk1 >= sk2 - * -> Cons (e, s, o, sk1 + sk2 + 1, s2, o1 + o2 + o) - * | _ -> Cons (e, s, o, 1, s, o) *) +and sort = + | Stype of lexp + | StypeOmega + | StypeLevel +and sort_level = + | SLz + | SLsucc of lexp + | SLlub of lexp * lexp + +(* We define here substitutions which take a variable within a source context +* Δₛ and should return an expression valid in target context Δₜ. +* +* The current implementation only handles a very limited subset of such +* substitutions. One of the many limitations is that we can only encode +* substitutions which map variables to variables. +*) + +and db_index = int (* DeBruijn index. *) +and db_offset = int (* DeBruijn index offset. *) + +(* Substitution, i.e. a mapping from db_index to lexp *) +and subst = subst' * int + and subst' = + | Identity of db_offset (* Identity o ≡ id ∘ ↑ₒ *) + | Cons of lexp * subst * db_offset (* Cons (e, s, o) ≡ (e · s) ∘ ↑ₒ *) + (* Myers's extra pointers down the list: + * * int * lexp subst * db_offset *) +(* Lift (n,m) increases indices≥N by M. + * IOW, it takes variables from a source context Δₛ₁Δₛ₂ to a destination + * context Δₛ₁ΔₜΔₛ₂ where Δₛ₂ has size N and Δₜ has size M. *) + (* | Lift of db_index * db_offset *) + +(* Build Myers's "stack" element. *) +(* let mkCons e s o = match s with +* | Cons (_, _, _, sk1, Cons (_, _, _, sk2, s2, o2), o1) when sk1 >= sk2 +* -> Cons (e, s, o, sk1 + sk2 + 1, s2, o1 + o2 + o) +* | _ -> Cons (e, s, o, 1, s, o) *)

type varbind = @@ -147,7 +147,7 @@ type varbind = | ForwardRef | LetDef of U.db_offset * lexp

- let lexp_hash (e, h) = h +let lexp_hash (e, h) = h

(* For metavariables, we give each metavar a (hopefully) unique integer * and then we store its corresponding info into the `metavar_table` @@ -192,10 +192,3 @@ let metavar_lookup (id : meta_id) : metavar_info = try U.IMap.find id (!metavar_table) with Not_found -> Log.log_fatal ~section:"LEXP" "metavar lookup failure!" - -(* counter for lexp sharing *) -let lshrct = ref 0 - -(* counter for subst sharing *) -let sshrct = ref 0 -let shrct_inc e acc = e := !e + acc

===================================== src/subst.ml ===================================== @@ -104,43 +104,53 @@ open Lexp_type * *)

- (********************** Hash-consing **********************) - - (** hash-consing test ** - * with: subst'_hash - * median bucket length: 7 - * biggest bucket length: 22 *) - - let subst_hash (s, h) = h - let subst_subst' (s, h) = s - - let hcsb_eq sb1 sb2 = - sb1 == sb2 || - match (subst_subst' sb1, subst_subst' sb2) with - | (Identity off1, Identity off2) -> off1 = off2 - | (Cons (lp1, lps1, off1), Cons (lp2, lps2, off2)) - -> lp1 == lp2 && lps1 == lps2 && off1 = off2 - | _ -> false - - let subst'_hash (sb : subst') : int = - match sb with - | Identity off - -> U.combine_hash 1 (Hashtbl.hash off) - | Cons (lp, sb, off) - -> shrct_inc lshrct 1; shrct_inc sshrct 1; - U.combine_hash 2 +(********************** Hash-consing **********************) + +(** hash-consing test ** + * with: subst'_hash + * median bucket length: 7 + * biggest bucket length: 22 + * found/new subst entries: 7 *) + +let subst_hash (s, h) = h +let subst_subst' (s, h) = s + +(* counter for subst found in WHCSB *) +let sshrct = ref 0 + +(* counter for subst not found in WHCSB *) +let nf_sshrct = ref 0 + +let shrct_inc e acc = e := !e + acc + +let hcsb_eq sb1 sb2 = + sb1 == sb2 || + match (subst_subst' sb1, subst_subst' sb2) with + | (Identity off1, Identity off2) -> off1 = off2 + | (Cons (lp1, lps1, off1), Cons (lp2, lps2, off2)) + -> lp1 == lp2 && lps1 == lps2 && off1 = off2 + | _ -> false + +let subst'_hash (sb : subst') : int = + match sb with + | Identity off + -> U.combine_hash 1 (Hashtbl.hash off) + | Cons (lp, sb, off) + -> U.combine_hash 2 (U.combine_hash (U.combine_hash - (lexp_hash lp) (subst_hash sb)) (Hashtbl.hash off)) + (lexp_hash lp) (subst_hash sb)) (Hashtbl.hash off))

- module WHCSB = Weak.Make (struct type t = subst - let equal x y = hcsb_eq x y - let hash = subst_hash - end) +module WHCSB = Weak.Make (struct type t = subst + let equal x y = hcsb_eq x y + let hash = subst_hash + end)

- let hcsb_table : WHCSB.t = WHCSB.create 1000 +let hcsb_table : WHCSB.t = WHCSB.create 1000

- let hcsb (s : subst') : subst = - let sb = (s, subst'_hash s) in WHCSB.merge hcsb_table sb +let hcsb (s : subst') : subst = + let sb = (s, subst'_hash s) in + try let sb' = WHCSB.find hcsb_table sb in (shrct_inc sshrct 1; sb') + with Not_found -> (shrct_inc nf_sshrct 1; WHCSB.add hcsb_table sb; sb)

(* Apply a substitution to a single variable. *) let lookup (mkVar : 'b -> db_index -> 'a)

===================================== src/util.ml ===================================== @@ -51,6 +51,8 @@ let loc_string loc =

let loc_print loc = print_string (loc_string loc)

+let time_process = ref false + let string_implode chars = String.concat "" (List.map (String.make 1) chars) let string_sub str b e = String.sub str b (e - b)

@@ -117,9 +119,14 @@ let option_map (fn : 'a -> 'b) (opt : 'a option) : 'b option = | None -> None | Some x -> Some (fn x)

-let combine_hash (e1: int) (e2: int) : int = (e1 * 31) lxor e2 +let combine_hash e1 e2 = (e1 * 31) lxor e2 + +let rec combine_hashes map = + match map with + | [] -> 31 + | e :: l -> combine_hash (e * 31) (combine_hashes l)

-let get_stats stats lshrct sshrct = +let get_stats_hashtbl stats sshrct nf_sshrct = let (tl, ne, sumb, smallb, medianb, bigb) = stats in Printf.printf "\n\ttable length: %i\n number of entries: %i\n @@ -127,5 +134,27 @@ let get_stats stats lshrct sshrct = smallest bucket length: %i\n median bucket length: %i\n biggest bucket length: %i\n - lexp sharing counter: %i\n - subst sharing counter: %i\n" tl ne sumb smallb medianb bigb lshrct sshrct; + found/new subst entries: %i\n" + tl ne sumb smallb medianb bigb (sshrct / nf_sshrct) + +let get_total_unix_stats_processtime (times : Unix.process_times) = + Printf.printf "\n\tUser time for the process: %f\n + System time for the process: %f\n + User time for the children processes: %f\n + System time for the children processes: %f\n" + times.tms_utime times.tms_stime times.tms_cutime times.tms_cstime + +let hc_total_time = ref 0.0 + +let inc_hc_total_time f = + let t = Unix.gettimeofday () in + let res = f () in (hc_total_time := + !hc_total_time +. Unix.gettimeofday () -. t; res) + +let get_unix_stats_processtime f = + let t = Unix.gettimeofday () in + let res = f () in (Printf.printf "\t(Unix) process time: %f\n" + (Unix.gettimeofday () -. t); res) + +let print_total_hctime hctime = + Printf.printf "\t(Unix) total hc time: %f\n" hctime

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