Alice de Berny pushed to branch alice at Stefan / Typer

Commits: 47cb679f by irradiee at 2020-07-10T06:43:41-04:00 add time & profiling

- - - - -

8 changed files:

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

Changes:

===================================== .gitignore ===================================== @@ -34,8 +34,12 @@ _tags # Files generated by profilers gmon.out ocamlprof.dump +profiling

# Files auto-generated for ELPA packaging and other Emacs stuff emacs/*-autoloads.el emacs/*-pkg.el emacs/*.elc + +# Dependencies +.depend

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

-# @TODO: remove -pkg unix -OBFLAGS = -tag debug -tag profile -lib str -build-dir $(BUILDDIR) -pkg zarith -pkg unix +OBFLAGS = -tag debug -tag e -lib str -build-dir $(BUILDDIR) -pkg zarith # OBFLAGS := -I $(SRCDIR) -build-dir $(BUILDDIR) -pkg str -# OBFLAGS_DEBUG := -tag debug -tag profile -tag "warn(+20)" +# OBFLAGS_DEBUG := -tag debug -tag e -tag "warn(+20)" # OBFLAGS_RELEASE := -tag unsafe -tag inline COMPILE_MODE = byte # COMPILE_MODE = native @@ -19,6 +18,15 @@ COMPILE_MODE = byte # DEBUG ?= 1 # VERBOSE ?= 1

+OCAMLCP := ocamlcp +OCAMLOPTP := ocamloptp +OCAMLOPT := ocamlopt +OCAMLDEP := ocamldep + +OCAMLFLAGS := -I src +SRC_NO_DEBUG := $(filter-out ./src/debug_util.ml, $(SRC_FILES)) +DEPSORT_FILES := $(shell ocamldep -sort -I src $(SRC_NO_DEBUG)) + all: typer debug tests-build

# ifeq ($(OS), Windows_NT) @@ -46,13 +54,12 @@ debug: $(OCAMLBUILD) src/debug_util.$(COMPILE_MODE) -I src $(OBFLAGS) @$(MV) $(BUILDDIR)/src/debug_util.$(COMPILE_MODE) $(BUILDDIR)/debug_util

- # interactive typer typer: # ============================ # Build typer # ============================ - $(OCAMLBUILD) src/REPL.$(COMPILE_MODE) -I src $(OBFLAGS) + $(OCAMLBUILD) src/REPL.$(COMPILE_MODE) -I src $(OBFLAGS) @$(MV) $(BUILDDIR)/src/REPL.$(COMPILE_MODE) $(BUILDDIR)/typer

tests-build: @@ -78,6 +85,14 @@ install: tests

tests: tests-build tests-run

+# @TODO: delete +test: + $(OCAMLBUILD) tests/lexp_test.$(COMPILE_MODE) -I src $(OBFLAGS) + @$(OCAMLBUILD) tests/utest_main.$(COMPILE_MODE) -I src $(OBFLAGS) + @$(MV) $(BUILDDIR)/tests/utest_main.$(COMPILE_MODE) \ + $(BUILDDIR)/tests/utests + @./$(BUILDDIR)/tests/utests --verbose= 3 + # Make language doc doc-tex: texi2pdf ./doc/manual.texi --pdf --build=clean @@ -110,3 +125,36 @@ run/typer-file:

run/test-file: @./$(BUILDDIR)/test + +profiling-cp: + # ============================ + # profiling bytecode + # ============================ + ocamlfind $(OCAMLCP) -o profiling -linkpkg -package zarith \ + $(OCAMLFLAGS) str.cma -P f $(DEPSORT_FILES) + +profiling-optp: + # ============================ + # profiling native + # ============================ + ocamlfind $(OCAMLOPTP) -o profiling -linkpkg -package zarith \ + $(OCAMLFLAGS) str.cmxa -P f $(DEPSORT_FILES) + +time: + # ============================ + # time native + # ============================ + ocamlfind $(OCAMLOPT) -p -o profiling -linkpkg -package zarith \ + $(OCAMLFLAGS) str.cmxa $(DEPSORT_FILES) + +# Clean up +clean-profiling: + -rm -rf profiling + -rm -rf src/*.cm[iox] src/*.o + -rm -rf ocamlprof.dump + -rm -rf .depend + -rm -rf gmon.out + +# Dependencies +depend: + $(OCAMLDEP) -sort $(OCAMLFLAGS) src/*.ml > .depend

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

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

@@ -220,10 +220,6 @@ let readfiles_aux 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 = let repl = repl (i + 1) in @@ -234,8 +230,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_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) + | "%lcollisions" | "%cl" -> (get_stats_hashtbl (WHC.stats hc_table) !lshrct !nf_lshrct !Subst.sshrct !Subst.nf_sshrct) + | "%scollisions" | "%scl" -> (get_stats_hashtbl (Subst.WHCSB.stats Subst.hcsb_table) !lshrct !nf_lshrct !Subst.sshrct !Subst.nf_sshrct)

(* command with arguments *) | _ when (ipt.[0] = '%' && ipt.[1] != ' ') -> ( @@ -251,7 +247,7 @@ let rec repl i clxp rctx = (time_process := true; let (i, clxp, rctx) = try - get_unix_stats_processtime (fun () -> (readfiles args (i, clxp, rctx) false)) + readfiles args (i, clxp, rctx) false with Log.Stop_Compilation msg -> (handle_stopped_compilation msg; (i,clxp,rctx)) in repl clxp rctx) @@ -323,12 +319,11 @@ let main () = if !time_process then let res = - get_unix_stats_processtime (fun () -> (readfiles - (List.rev !arg_files) (1, ectx, rctx) (not !arg_batch))) in + 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 + readfiles (List.rev !arg_files) (1, ectx, rctx) (not !arg_batch) in (print_and_clear_log (); res) with | Log.Stop_Compilation msg ->

===================================== src/debug_util.ml ===================================== @@ -29,7 +29,6 @@ * print out each compilation' steps * * --------------------------------------------------------------------------- *) - (* Utilities *) open Util open Fmt @@ -38,6 +37,7 @@ open Debug (* ASTs *) open Sexp open Pexp +open Lexp_type open Lexp

(* AST reader *)

===================================== src/lexp.ml ===================================== @@ -154,17 +154,18 @@ module WHC = Weak.Make (struct type t = lexp let hash = lexp_hash end)

-let hc_table : WHC.t = WHC.create 1000 +(* counter for lexp found in WHC *) +let lshrct = ref 0 + +(* counter for lexp not found in WHC *) +let nf_lshrct = ref 0

-let hc_aux (e : lexp') : lexp = - let lp = (e, lexp'_hash e) in WHC.merge hc_table lp +let hc_table : WHC.t = WHC.create 1000

-let hc (e : lexp') : lexp = - if !U.time_process - then - U.inc_hc_total_time (fun () -> hc_aux e) - else - hc_aux e +let hc (s : lexp') : lexp = + let lp = (s, lexp'_hash s) in + try let lp' = WHC.find hc_table lp in (U.shrct_inc lshrct 1; lp') + with Not_found -> (U.shrct_inc nf_lshrct 1; WHC.add hc_table lp; lp)

let impossible = hc (Imm Sexp.dummy_epsilon)

===================================== src/lexp_type.ml ===================================== @@ -124,6 +124,7 @@ and db_index = int (* DeBruijn index. *) and db_offset = int (* DeBruijn index offset. *)

(* Substitution, i.e. a mapping from db_index to lexp *) +(* @TODO: change Cons name *) and subst = subst' * int and subst' = | Identity of db_offset (* Identity o ≡ id ∘ ↑ₒ *)

===================================== src/subst.ml ===================================== @@ -121,8 +121,6 @@ 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 @@ -149,8 +147,8 @@ let hcsb_table : WHCSB.t = WHCSB.create 1000

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) + try let sb' = WHCSB.find hcsb_table sb in (U.shrct_inc sshrct 1; sb') + with Not_found -> (U.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 ===================================== @@ -126,7 +126,7 @@ let rec combine_hashes map = | [] -> 31 | e :: l -> combine_hash (e * 31) (combine_hashes l)

-let get_stats_hashtbl stats sshrct nf_sshrct = +let get_stats_hashtbl stats lshrct nf_lshrct sshrct nf_sshrct = let (tl, ne, sumb, smallb, medianb, bigb) = stats in Printf.printf "\n\ttable length: %i\n number of entries: %i\n @@ -134,27 +134,8 @@ let get_stats_hashtbl stats sshrct nf_sshrct = smallest bucket length: %i\n median bucket length: %i\n biggest bucket length: %i\n + found/new lexp entries: %i\n found/new subst entries: %i\n" - tl ne sumb smallb medianb bigb (sshrct / nf_sshrct) + tl ne sumb smallb medianb bigb (lshrct / nf_lshrct) (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 +let shrct_inc e acc = e := !e + acc

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