Stefan pushed to branch unification at Stefan / Typer
Commits: 29925bc1 by Stefan Monnier at 2016-11-08T18:24:24-05:00 * src/debug_fun.ml, src/fmt_lexp.ml: Remove
* src/util.ml (padding_right, padding_left): Move from fmt_lexp.ml. (utf8_head_p, string_width): New functions. * src/prelexer.ml (inc_cp): Use them.
- - - - -
11 changed files:
- − src/debug_fun.ml - src/env.ml - src/eval.ml - − src/fmt_lexp.ml - src/lparse.ml - src/opslexp.ml - src/prelexer.ml - src/util.ml - tests/inverse_test.ml - tests/lparse_test.ml - tests/unify_test.ml
Changes:
===================================== src/debug_fun.ml deleted ===================================== --- a/src/debug_fun.ml +++ /dev/null @@ -1,49 +0,0 @@ - -(* let _debug = true *) -let _debug = false - -let logs = ref [] - -(** Execute the function if _debug = true*) -let do_debug func = - if _debug then (func ()) else () - -(** print the two string parameter (buffered print) *) -let debug_print str1 str2 = - logs := ((Fmt_lexp.padding_left str1 20 ' ')^" : ", (str2^"\n"))::(!logs); () - -let clear_indent () = - let indent = ref 0 - in - do_debug (fun () -> - List.iter (fun (s1, s2) -> - prerr_string s1; - prerr_string (String.make (!indent * 2) '-'); - prerr_string s2; - indent := !indent + 1; - ) (!logs); - logs := []; - prerr_newline (); - ()) - -(** Print when _debug = true. No buffer *) -let debug_print_no_buff str = - do_debug (fun () -> prerr_string str; ()) - -(** Print a lxp when _debug = true. No buffer *) -let debug_print_lexp lxp = - let str = Lexp.lexp_string lxp - in do_debug (fun () -> prerr_string str; ()) - -(** Helper for printing in a unify* function. Buffered *) -let debug_print_unify fn lhs rhs str = - let debug_print_unify fn lhs rhs str = - let tmp = ((Fmt_lexp.padding_left fn 20 ' ') ^ " : ", - Lexp.lexp_string lhs - ^ " , " - ^ Lexp.lexp_string rhs - ^ str ^ "\n") - in - logs := tmp::(!logs); - in do_debug (fun () -> debug_print_unify fn lhs rhs str; ()) -
===================================== src/env.ml ===================================== --- a/src/env.ml +++ b/src/env.ml @@ -148,17 +148,6 @@ let get_rte_variable (name: string option) (idx: int) if n1 = n2 then x else ( - Debug_fun.do_debug (fun () -> - prerr_endline ">>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>"; - prerr_endline "get_rte_variable"; - prerr_endline ("idx = " ^ (string_of_int idx)); - prerr_endline ("rte_size = " ^ (string_of_int (get_rte_size ctx))); - prerr_endline ("name = " ^ n2); - prerr_endline ("tname = " ^ n1); - prerr_endline "Callstack"; - prerr_endline (Printexc.raw_backtrace_to_string (Printexc.get_callstack 20)); - prerr_endline "<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<"; - prerr_newline ();();); error dloc ("Variable lookup failure. Expected: "" ^ n2 ^ "[" ^ (string_of_int idx) ^ "]" ^ "" got "" ^ n1 ^ """)))
===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -245,14 +245,6 @@ let write_impl loc depth args_val ctx = (* This is an internal definition * 'i' is the recursion depth used to print the call trace *) let rec _eval lxp (ctx : Env.runtime_env) (trace : eval_debug_info): (value_type) = - Debug_fun.do_debug (fun () -> - prerr_endline ("[StackTrace] ------------------------------------------"); - prerr_endline ("[StackTrace] let rec _eval lxp ctx i"); - prerr_endline ("[StackTrace] lxp = " ^ Elexp.elexp_string lxp); - prerr_endline ("[StackTrace] ctx = ???"); - (* prerr_endline ("[StackTrace] i = " ^ (string_of_int trace)); *) - prerr_endline ("[StackTrace] ------------------------------------------"); - ());
let trace = append_eval_trace trace lxp in let tloc = elexp_location lxp in @@ -305,19 +297,6 @@ and get_predef_eval name ctx =
and eval_var ctx lxp v = let ((loc, name), idx) = v in - Debug_fun.do_debug (fun () -> - prerr_endline ("[StackTrace] ------------------------------------------"); - prerr_endline ("[StackTrace] let eval_var ctx lxp v"); - prerr_endline ("[StackTrace] lxp = " ^ Elexp.elexp_string lxp); - prerr_endline ("[StackTrace] ctx = ???"); - prerr_endline ("[StackTrace] v = ((?loc?, " ^ name ^ "), " ^ (string_of_int idx) ^ ")"); - prerr_endline ("[StackTrace] ------------------------------------------"); - ()); - Debug_fun.do_debug (fun () -> - prerr_endline ("index not shifted " ^ (string_of_int idx)); - prerr_endline ("ctx size " ^ (string_of_int (get_rte_size ctx))); - () - ); try get_rte_variable (Some name) (idx) ctx with e -> elexp_fatal loc lxp @@ -606,13 +585,6 @@ and print_eval_trace trace = let eval lxp ctx = _eval lxp ctx ([], [])
let debug_eval lxp ctx = - Debug_fun.do_debug (fun () -> - prerr_endline ("[StackTrace] ------------------------------------------"); - prerr_endline ("[StackTrace] let debug_eval lxps rctx silent"); - prerr_endline ("[StackTrace] lxp = " ^ Elexp.elexp_string lxp); - prerr_endline ("[StackTrace] ctx = ???"); - prerr_endline ("[StackTrace] ------------------------------------------"); - ()); try eval lxp ctx with e -> ( print_rte_ctx (!_global_eval_ctx); @@ -629,14 +601,6 @@ let eval_decls_toplevel (decls: (vdef * elexp) list list) ctx =
(* Eval a list of lexp *) let eval_all lxps rctx silent = - Debug_fun.do_debug (fun () -> - prerr_endline ("[StackTrace] ------------------------------------------"); - prerr_endline ("[StackTrace] let eval_all lxps rctx silent"); - prerr_endline ("[StackTrace] lxps = ???"); - prerr_endline ("[StackTrace] rctx = ???"); - prerr_endline ("[StackTrace] silent = " ^ string_of_bool silent); - prerr_endline ("[StackTrace] ------------------------------------------"); - ()); let evalfun = if silent then eval else debug_eval in List.map (fun g -> evalfun g rctx) lxps
===================================== src/fmt_lexp.ml deleted ===================================== --- a/src/fmt_lexp.ml +++ /dev/null @@ -1,10 +0,0 @@ - -let padding_right (str: string ) (dim: int ) (char_: char) : string = - let diff = (dim - String.length str) - in let rpad = max diff 0 - in str ^ (String.make rpad char_) - -let padding_left (str: string ) (dim: int ) (char_: char) : string = - let diff = (dim - String.length str) - in let lpad = max diff 0 - in (String.make lpad char_) ^ str
===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -211,15 +211,6 @@ let newMetalevel () = let newMetatype () = newMetavar (newMetalevel ())
let rec _lexp_p_infer (p : pexp) (ctx : elab_context) trace: lexp * ltype = - Debug_fun.do_debug (fun () -> - prerr_endline ("[StackTrace] ------------------------------------------"); - prerr_endline ("[StackTrace] let _lexp_p_infer p ctx i"); - prerr_endline ("[StackTrace] p = " ^ pexp_string p); - prerr_endline ("[StackTrace] ctx = ???"); - (* prerr_endline ("[StackTrace] i = " ^ string_of_int trace); *) - (* prerr_endline (Printexc.raw_backtrace_to_string (Printexc.get_callstack 20)); *) - prerr_endline ("[StackTrace] ------------------------------------------"); - ());
let trace = ((OL.Pexp p)::trace) in let tloc = pexp_location p in @@ -382,15 +373,6 @@ and lexp_let_decls declss (body: lexp) ctx i = and _lexp_p_check (p : pexp) (t : ltype) (ctx : elab_context) trace: lexp =
let trace = ((OL.Pexp p)::trace) in - Debug_fun.do_debug (fun () -> - prerr_endline ("[StackTrace] ------------------------------------------"); - prerr_endline ("[StackTrace] let _lexp_p_check p t ctx i"); - prerr_endline ("[StackTrace] p = " ^ pexp_string p); - prerr_endline ("[StackTrace] t = " ^ lexp_string t); - prerr_endline ("[StackTrace] ctx = ???"); - (* prerr_endline ("[StackTrace] i = " ^ string_of_int trace); *) - prerr_endline ("[StackTrace] ------------------------------------------"); - ()); let tloc = pexp_location p in let lexp_infer p ctx = _lexp_p_infer p ctx trace in @@ -597,15 +579,6 @@ and lexp_case rtype (loc, target, ppatterns) ctx i =
(* Identify Call Type and return processed call *) and lexp_call (func: pexp) (sargs: sexp list) ctx i = - Debug_fun.do_debug (fun () -> - prerr_endline ("[StackTrace] ------------------------------------------"); - prerr_endline ("[StackTrace] let lexp_call func sargs ctx i"); - prerr_endline ("[StackTrace] func = " ^ pexp_string func); - prerr_endline ("[StackTrace] sargs = ???"); - prerr_endline ("[StackTrace] ctx = ???"); - (* prerr_endline ("[StackTrace] i = " ^ string_of_int trace); *) - prerr_endline ("[StackTrace] ------------------------------------------"); - ()); let loc = pexp_location func in let meta_ctx, _ = !global_substitution in
@@ -622,12 +595,6 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i = let ltp = nosusp ltp in
let rec handle_fun_args largs sargs ltp = - Debug_fun.do_debug (fun () -> - print_endline ">>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>"; - print_lexp_ctx (ectx_to_lctx ctx); - flush stdout; - prerr_endline "<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<"; - print_newline ();();); match sargs with | [] -> largs, ltp | (Node (Symbol (_, "_:=_"), [Symbol (_, aname); sarg])) :: sargs @@ -810,14 +777,6 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i =
(* Parse inductive type definition. *) and lexp_parse_inductive ctors ctx i = - Debug_fun.do_debug (fun () -> - prerr_endline ("[StackTrace] ------------------------------------------"); - prerr_endline ("[StackTrace] let lexp_parse_inductive ctors ctx i"); - prerr_endline ("[StackTrace] ctors = ???"); - prerr_endline ("[StackTrace] ctx = ???"); - (* prerr_endline ("[StackTrace] i = " ^ string_of_int trace); *) - prerr_endline ("[StackTrace] ------------------------------------------"); - ()); let lexp_parse p ctx = _lexp_p_infer p ctx i in
let make_args (args:(arg_kind * pvar option * pexp) list) ctx @@ -1129,15 +1088,6 @@ let lexp_decl_str str lctx = (* Because we cant include lparse in eval.ml *)
let _eval_expr_str str lctx rctx silent = - Debug_fun.do_debug (fun () -> - prerr_endline ("[StackTrace] ------------------------------------------"); - prerr_endline ("[StackTrace] let _eval_expr_str str lctx rctx silent"); - prerr_endline ("[StackTrace] str = " ^ str); - prerr_endline ("[StackTrace] lctx = ???"); - prerr_endline ("[StackTrace] rctx = ???"); - prerr_endline ("[StackTrace] silent = " ^ string_of_bool silent); - prerr_endline ("[StackTrace] ------------------------------------------"); - ()); let lxps = lexp_expr_str str lctx in let elxps = List.map OL.erase_type lxps in (eval_all elxps rctx silent)
===================================== src/opslexp.ml ===================================== --- a/src/opslexp.ml +++ b/src/opslexp.ml @@ -87,14 +87,6 @@ let rec lexp_defs_subst l s defs = match defs with * call-by-name behavior. *) let lexp_whnf e (ctx : DB.lexp_context) meta_ctx : lexp = let rec lexp_whnf e (ctx : DB.lexp_context) : lexp = - Debug_fun.do_debug (fun () -> - prerr_endline ("[StackTrace] ------------------------------------------"); - prerr_endline ("[StackTrace] let lexp_whnf e ctx meta_ctx"); - prerr_endline ("[StackTrace] e = " ^ lexp_string e); - prerr_endline ("[StackTrace] ctx = ???"); - prerr_endline ("[StackTrace] meta_ctx = ???"); - prerr_endline ("[StackTrace] ------------------------------------------"); - ()); match e with | Var v -> (match lookup_value ctx v with | None -> e
===================================== src/prelexer.ml ===================================== --- a/src/prelexer.ml +++ b/src/prelexer.ml @@ -50,7 +50,7 @@ let string_sub str b e = String.sub str b (e - b)
let inc_cp (cp:charpos) (c:char) = (* Count char positions in utf-8: don't count the non-leading bytes. *) - if (Char.code c < 128 || Char.code c >= 192) then cp+1 else cp + if utf8_head_p c then cp+1 else cp
let rec prelex (file : string) (getline : unit -> string) ln ctx acc : pretoken list =
===================================== src/util.ml ===================================== --- a/src/util.ml +++ b/src/util.ml @@ -118,3 +118,27 @@ let str_split str sep = ret := (Buffer.contents buffer)::(!ret));
List.rev (!ret)) + +let utf8_head_p (c : char) : bool + = Char.code c < 128 || Char.code c >= 192 + +(* Display size of `str`, assuming the byte-sequence is UTF-8. + * Very naive: doesn't pay attention to LF, TABs, double-width chars, ... *) +let string_width (s : string) : int = + let rec width i w = + if i < 0 then w + else width (i - 1) + (if utf8_head_p (String.get s i) + then w + 1 + else w) in + width (String.length s - 1) 0 + +let padding_right (str: string ) (dim: int ) (char_: char) : string = + let diff = (dim - string_width str) + in let rpad = max diff 0 + in str ^ (String.make rpad char_) + +let padding_left (str: string ) (dim: int ) (char_: char) : string = + let diff = (dim - string_width str) + in let lpad = max diff 0 + in (String.make lpad char_) ^ str
===================================== tests/inverse_test.ml ===================================== --- a/tests/inverse_test.ml +++ b/tests/inverse_test.ml @@ -17,9 +17,6 @@ open Str
open Debug
-open Fmt_lexp -open Debug_fun - let mkShift2 shift subst = S.mkShift subst shift
@@ -92,7 +89,7 @@ let generate_tests (name: string) in List.map (fun (sub, res) -> idx := !idx + 1; add_test name - ((padding_left (string_of_int (!idx)) 2 '0') ^ " - " ^ sub) + ((U.padding_left (string_of_int (!idx)) 2 '0') ^ " - " ^ sub) (fun () -> if res then success () else failure ())) (test input_gen fmt tester)
@@ -107,10 +104,10 @@ let get_dim lst =
let fmt_res str = let (ds, ds', dcomp) = get_dim str - in List.map (fun (s, s', com) -> (padding_right s ds ' ') ^ " -> " ^ - (padding_right s' ds' ' ') ^ " = " ^ - (com) - ) str + in List.map (fun (s, s', com) -> (U.padding_right s ds ' ') ^ " -> " + ^ (U.padding_right s' ds' ' ') ^ " = " + ^ com) + str
let get_dim lst = let max i s = max i (String.length s)
===================================== tests/lparse_test.ml ===================================== --- a/tests/lparse_test.ml +++ b/tests/lparse_test.ml @@ -1,6 +1,5 @@
open Lparse -open Fmt_lexp open Utest_lib
open Pexp @@ -25,7 +24,7 @@ let generate_tests (name: string) in List.map (fun (sub, res) -> idx := !idx + 1; add_test name - ((padding_left (string_of_int (!idx)) 2 '0') ^ " - " ^ sub) + ((U.padding_left (string_of_int (!idx)) 2 '0') ^ " - " ^ sub) (fun () -> if res then success () else failure ())) (test input_gen fmt tester)
===================================== tests/unify_test.ml ===================================== --- a/tests/unify_test.ml +++ b/tests/unify_test.ml @@ -17,8 +17,6 @@ open Str
open Debug
-open Debug_fun - type result = | Constraint | Unification @@ -48,13 +46,13 @@ let fmt (lst: (lexp * lexp * result * result) list): string list = (fun (l1, l2, r1, r2) -> ((lexp_string l1), (lexp_string l2), (string_of_result r1), (string_of_result r2))) lst in let l, c1, c2, r = max_dim str_lst - in List.map (fun (l1, l2, r1, r2) -> (Fmt_lexp.padding_right l1 l ' ') + in List.map (fun (l1, l2, r1, r2) -> (U.padding_right l1 l ' ') ^ ", " - ^ (Fmt_lexp.padding_right l2 c1 ' ') + ^ (U.padding_right l2 c1 ' ') ^ " -> got: " - ^ (Fmt_lexp.padding_right r2 r ' ') + ^ (U.padding_right r2 r ' ') ^ " expected: " - ^ (Fmt_lexp.padding_right r1 c2 ' ') + ^ (U.padding_right r1 c2 ' ') ) str_lst
(* Inputs for the test *)
View it on GitLab: https://gitlab.com/monnier/typer/commit/29925bc187745a333cd15f55e969bb59c378...