Stefan pushed to branch unification at Stefan / Typer

Commits: 6cb1661b by Stefan Monnier at 2016-10-17T23:38:03-04:00 Gut Fmt_lexp. Use lexp_string and lexp_print instead

* src/debug_fun.ml: Don't open Fmt_lexp. Don't enable debugging trace by default. Use lexp_string.

* src/fmt_lexp.ml: Strip it down to just the two padding functions.

* src/lexp.ml (subst_string): New function.

- - - - -

8 changed files:

- src/debug_fun.ml - src/fmt_lexp.ml - src/lexp.ml - src/lparse.ml - src/opslexp.ml - tests/inverse_test.ml - tests/lparse_test.ml - tests/unify_test.ml

Changes:

===================================== src/debug_fun.ml ===================================== --- a/src/debug_fun.ml +++ b/src/debug_fun.ml @@ -1,8 +1,6 @@

-open Fmt_lexp - -let _debug = true -(* let _debug = false *) +(* let _debug = true *) +let _debug = false

let logs = ref []

@@ -12,7 +10,7 @@ let do_debug func =

(** print the two string parameter (buffered print) *) let debug_print str1 str2 = - logs := ((padding_left str1 20 ' ')^" : ", (str2^"\n"))::(!logs); () + logs := ((Fmt_lexp.padding_left str1 20 ' ')^" : ", (str2^"\n"))::(!logs); ()

let clear_indent () = let indent = ref 0 @@ -34,17 +32,17 @@ let debug_print_no_buff str =

(** Print a lxp when _debug = true. No buffer *) let debug_print_lexp lxp = - let str = colored_string_of_lxp lxp str_yellow str_magenta + 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 = ((padding_left fn 20 ' ') ^ " : ", - (colored_string_of_lxp lhs str_yellow str_magenta) - ^ " , " - ^ colored_string_of_lxp rhs str_yellow str_magenta - ^ str ^ "\n") + 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/fmt_lexp.ml ===================================== --- a/src/fmt_lexp.ml +++ b/src/fmt_lexp.ml @@ -1,97 +1,4 @@

-module L = Lexp -module S = Subst - -let _color = true - -let str_red str = if _color then Fmt.red ^ str ^ Fmt.reset else str -let str_green str = if _color then Fmt.green ^ str ^ Fmt.reset else str -let str_magenta str = if _color then Fmt.magenta ^ str ^ Fmt.reset else str -let str_yellow str = if _color then Fmt.yellow ^ str ^ Fmt.reset else str -let str_cyan str = if _color then Fmt.cyan ^ str ^ Fmt.reset else str - -let rec string_of_subst s = - match s with - | S.Cons (L.Var(_, idx), s2) -> (* "a" ^ *) string_of_int idx ^ " · " ^ string_of_subst s2 - | S.Cons (l, s2) -> string_of_lxp l ^ " · " ^ string_of_subst s2 - | S.Shift (s2, shift) -> "(" ^ string_of_subst s2 ^ ") ↑^" ^ string_of_int shift - | S.Identity -> "Id" - -(* result look more like ocaml code *) -and ocaml_string_of_subst s = - match s with - | S.Cons (l, s2) -> "Cons(" ^ string_of_lxp l ^ ", " ^ ocaml_string_of_subst s2 ^ ")" - | S.Shift (s2, shift) -> "Shift(" ^ ocaml_string_of_subst s2 ^ ", " ^ string_of_int shift ^ ")" - | S.Identity -> "Identity" - -(* Same as ocaml_string_of_subst but prettier *) -and pp_ocaml_string_of_subst s = - let rec pp_ocaml_string_of_subst s i = - match s with - | S.Cons (l, s2) -> "Cons(" ^ string_of_lxp l ^ ",\n" - ^ (String.make (4 * i) ' ') ^ pp_ocaml_string_of_subst s2 (i + 1) ^ ")" - | S.Shift (s2, shift) -> "Shift(" ^ string_of_int shift ^ ",\n" - ^ (String.make (4 * i) ' ') ^ pp_ocaml_string_of_subst s2 (i + 1)^ ")" - | S.Identity -> "Identity" - in pp_ocaml_string_of_subst s 1 - -and string_of_lxp lxp = - match lxp with - | L.Imm (Sexp.Integer (_, value)) -> "Integer(" ^ (string_of_int value) ^ ")" - | L.Imm (Sexp.String (_, value)) -> "String(" ^ value ^ ")" - | L.Imm (Sexp.Float (_, value)) -> "Float(" ^ (string_of_float value) ^ ")" - | L.Cons (it, (_, cname)) -> "Cons(" ^ string_of_lxp it ^ ", " ^ cname ^")" - | L.Builtin ((_, name), _) -> "Builtin(" ^ name ^ ")" - | L.Let (_) -> "Let(..)" - | L.Var ((_, name), idx) -> "Var(" ^ name ^ ", #" ^(string_of_int idx) ^ ")" - | L.Arrow (kind, Some(_, name), a, _, b) -> name ^ ":Arrow(" ^ (string_of_lxp a) ^ ":" ^ string_of_kind kind ^ " => " ^ (string_of_lxp b) ^ ")" - | L.Arrow (kind, _, a, _, b) -> "Arrow(" ^ (string_of_lxp a) ^ ":" ^ string_of_kind kind ^ " => " ^ (string_of_lxp b) ^ ")" - | L.Lambda (_,(_, name), dcl, body) -> "Lambda(" ^ name ^ ": " ^ (string_of_lxp dcl) ^ " => (" ^ (string_of_lxp body) ^ "))" - | L.Metavar (value, _, (_, name)) -> "Metavar(" ^ (string_of_int value) ^ ", " ^ name ^ ")" - | L.Call (_) -> "Call(...)" - | L.Inductive _ -> ("Inductive") ^ "(...)" - | L.Sort (_, s) -> ("Sort") ^ "(" ^ string_of_sort s ^ ")" - | L.SortLevel l -> ("SortLevel") ^ "(" ^ string_of_sort_level l ^ ")" - | L.Case _ -> ("Case") ^ "(...)" - | L.Susp (v, s) -> "Susp(" ^ (string_of_lxp v) ^ ", " ^ (string_of_subst s) ^ ")" - | _ -> "Unidentified Lexp" - -and string_of_kind = function - | Pexp.Aexplicit -> "Aexplicit" - | Pexp.Aimplicit -> "Aimplicit" - | Pexp.Aerasable -> "Aerasable" - -and string_of_sort_level lvl = - match lvl with - | L.SLz -> "SLz" - | L.SLsucc l -> "SLsucc(" ^ string_of_lxp l ^ ")" - -and string_of_sort sort = - match sort with - | L.Stype lxp -> "Stype(" ^ string_of_lxp lxp ^ ")" - | L.StypeOmega -> "StypeOmega" - | L.StypeLevel -> "StypeLevel" - -let rec colored_string_of_lxp lxp lcol vcol = - match lxp with - | L.Imm (Sexp.Integer (_, value)) -> (lcol "Integer") ^ "(" ^ (vcol (string_of_int value)) ^ ")" - | L.Imm (Sexp.String (_, value)) -> (lcol "String") ^ "(" ^ (vcol value ) ^ ")" - | L.Imm (Sexp.Float (_, value)) -> (lcol "Float" ) ^ "(" ^ (vcol (string_of_float value)) ^ ")" - | L.Cons (it, _) -> (lcol "Cons" ) ^ "(" ^ (colored_string_of_lxp it lcol vcol) ^ ")" - | L.Builtin ((_, name), _) -> (lcol "Builtin") ^ "(" ^ (vcol name) ^ ")" - | L.Let (_) -> (lcol "Let(..)") - | L.Var ((_, name), idx) -> (lcol "Var" ) ^ "(" ^ (vcol name ) ^ ", " ^ (vcol ("#" ^ (string_of_int idx))) ^ ")" - | L.Arrow (_, _, a, _, b) -> (lcol "Arrow(") ^ (vcol (string_of_lxp a)) ^ " => " ^ (vcol (string_of_lxp b)) ^ ")" - | L.Lambda (_,(_, name), dcl, body) -> (lcol "Lambda") ^ "(" ^ (vcol name) ^ " : " ^ (vcol (string_of_lxp dcl)) - | L.Metavar (value, _, (_, name)) -> (lcol "Metavar" ) ^ "(" ^ (vcol (string_of_int value)) ^ ", " ^ (vcol name) ^ ")" - | L.Call (_) -> (lcol "Call(...)" ) - | L.Case _ -> (lcol "Case") ^ "(...)" - | L.Inductive _ -> (lcol "Inductive") ^ "(...)" - | L.Sort (_, s) -> (lcol "Sort") ^ "(" ^ vcol (string_of_sort s)^ ")" - | L.SortLevel l -> (lcol "SortLevel") ^ "(" ^ vcol (string_of_sort_level l) ^ ")" - | L.Susp (v, s) -> (lcol "Susp") ^ "(" ^ colored_string_of_lxp v lcol vcol ^ ", " ^ vcol (string_of_subst s) ^")" - | _ -> (lcol "Unidentified Lexp") - let padding_right (str: string ) (dim: int ) (char_: char) : string = let diff = (dim - String.length str) in let rpad = max diff 0 @@ -101,72 +8,3 @@ 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 - -let center (str: string ) (dim: int ) (char_: char) : string = - let diff = max (dim - String.length str) 0 - in let lpad, rpad = ((diff / 2), ((diff / 2) + (diff mod 2))) - in (String.make lpad char_) ^ str ^ (String.make rpad char_) - - -let rec string_of_pexp pxp = - match pxp with - | Pexp.Pimm (Sexp.Integer (_, i)) -> "Pimm( Integer (" ^ string_of_int i ^ "))" - | Pexp.Pimm (Sexp.Float (_, f)) -> "Pimm( Float (" ^ string_of_float f ^ "))" - | Pexp.Pimm (Sexp.String (_, s)) -> "Pimm (String (" ^ s ^ "))" - | Pexp.Pvar (_, s) -> "Pvar (" ^ s ^ ")" - | Pexp.Phastype (_, p1, p2) -> "Phastype (" ^ string_of_pexp p1 ^ ", " ^ string_of_pexp p2 ^ ")" - | Pexp.Pmetavar (_, s) -> "Pmetavar (" ^ s ^ ")" - | Pexp.Plet (_, _, p) -> "Plet (_, " ^ string_of_pexp p ^ ")" - | Pexp.Parrow (_, _, _, _, _) -> "Parrow (...)" - | Pexp.Plambda _ -> "Plambda (...)" - | Pexp.Pcall _ -> "Pcall (...)" - | Pexp.Pinductive _ -> "Pinductive (...)" - | Pexp.Pcons (it, (_, s2)) -> "Pcons (" ^ string_of_pexp it - ^ ", " ^ s2 ^ ")" - | Pexp.Pcase _ -> "Pcase (...)" - | _ -> "Pexp not handled" - -let print_meta_ctx ((subst: L.substitution), (const: L.constraints)) = - let print_const c = - let strs = List.map (fun (c1, c2) -> (string_of_lxp c1, string_of_lxp c2)) c - in let strs = ("left lexp", "right lexp")::strs - in let (max_size_left, max_size_right) = List.fold_right - (fun (s1, s2) (l1, l2) -> ( - (max (String.length s1) l1), - (max (String.length s2) l2) - )) strs (0, 0) - in let head, tail = (List.hd strs), (List.tl strs) - in let strs = head::(String.make (max_size_left) '=', String.make (max_size_right) '=')::tail - in print_endline (center " Constraints " (max_size_left + max_size_right + 7) '='); - List.iter - (fun (s1, s2) -> - print_endline ( "| " - ^ padding_right s1 (max_size_left) ' ' - ^ " | " - ^ padding_right s2 (max_size_right) ' ' - ^ " |") - ) strs; - print_endline (center "=" (max_size_left + max_size_right + 7) '='); - and print_meta m = - let strs = List.map (fun (k, v) -> (string_of_int k, string_of_lxp v)) (L.VMap.bindings m) - in let strs = ("Metavar index", "Lexp")::strs - in let (max_size_left, max_size_right) = List.fold_right - (fun (s1, s2) (l1, l2) -> ( - (max (String.length s1) l1), - (max (String.length s2) l2) - )) strs (0, 0) - in let head, tail = (List.hd strs), (List.tl strs) - in let strs = head::(String.make (max_size_left) '=', String.make (max_size_right) '=')::tail - in print_endline (center " Metavar Context " (max_size_left + max_size_right + 7) '='); - List.iter - (fun (s1, s2) -> - print_endline ( "| " - ^ padding_right s1 (max_size_left) ' ' - ^ " | " - ^ padding_right s2 (max_size_right) ' ' - ^ " |") - ) strs; - print_endline (center "=" (max_size_left + max_size_right + 7) '='); - in print_meta subst; - print_const const -

===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -574,7 +574,13 @@ let rec lexp_unparse lxp =

| _ as e -> Pimm (Symbol(lexp_location e, "Type"))

-let lexp_string lxp = sexp_string (pexp_unparse (lexp_unparse lxp)) +let rec subst_string s = match s with + | S.Identity -> "Id" + | S.Shift (s, n) -> "(" ^ subst_string s ^ "↑" ^ string_of_int n ^ ")" + | S.Cons (l, s) -> lexp_string l ^ " · " ^ subst_string s + +(* FIXME: ¡Unify lexp_print and lexp_string! *) +and lexp_string lxp = sexp_string (pexp_unparse (lexp_unparse lxp)) (* * Printing * --------------------- *)

===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -202,7 +202,7 @@ and _lexp_p_infer (p : pexp) (ctx : elab_context) i: lexp * ltype = Debug_fun.do_debug (fun () -> prerr_endline ("[StackTrace] ------------------------------------------"); prerr_endline ("[StackTrace] let _lexp_p_infer p ctx i"); - prerr_endline ("[StackTrace] p = " ^ Fmt_lexp.string_of_pexp p); + prerr_endline ("[StackTrace] p = " ^ pexp_string p); prerr_endline ("[StackTrace] ctx = ???"); prerr_endline ("[StackTrace] i = " ^ string_of_int i); (* prerr_endline (Printexc.raw_backtrace_to_string (Printexc.get_callstack 20)); *) @@ -302,7 +302,9 @@ and _lexp_p_infer (p : pexp) (ctx : elab_context) i: lexp * ltype =

| _ -> lexp_error loc "Not an Inductive Type"; Debug_fun.do_debug (fun () -> - print_string ("idt : " ^ Fmt_lexp.string_of_lxp (nosusp idt) ^ ", p : " ^ (Fmt_lexp.string_of_pexp p)); + print_string "idt : "; + lexp_print (nosusp idt); + print_string (", p : " ^ (pexp_string p)); print_newline (); ()); [], [] in

@@ -364,8 +366,8 @@ and _lexp_p_check (p : pexp) (t : ltype) (ctx : elab_context) i: lexp = Debug_fun.do_debug (fun () -> prerr_endline ("[StackTrace] ------------------------------------------"); prerr_endline ("[StackTrace] let _lexp_p_check p t ctx i"); - prerr_endline ("[StackTrace] p = " ^ Fmt_lexp.string_of_pexp p); - prerr_endline ("[StackTrace] t = " ^ Fmt_lexp.string_of_lxp t); + 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 i); prerr_endline ("[StackTrace] ------------------------------------------"); @@ -381,9 +383,9 @@ and _lexp_p_check (p : pexp) (t : ltype) (ctx : elab_context) i: lexp = in let arrow = Arrow (kind, None, arg, Util.dummy_location, body) in match Unif.unify arrow lxp subst with | Some(subst) -> global_substitution := subst; arg, body - | None -> lexp_error tloc ("Type " ^ Fmt_lexp.string_of_lxp lxp + | None -> lexp_error tloc ("Type " ^ lexp_string lxp ^ " and " - ^ Fmt_lexp.string_of_lxp arrow + ^ lexp_string arrow ^ " does not match"); dltype, dltype

in @@ -435,15 +437,13 @@ and lexp_p_infer_and_check pexp ctx t i = | None -> debug_msg ( let print_lxp str = - print_string (Fmt_lexp.colored_string_of_lxp - str Fmt_lexp.str_yellow - Fmt_lexp.str_magenta) in + print_string (lexp_string str) in Debug_fun.do_debug (fun () -> - prerr_endline ("0 pxp " ^ Fmt_lexp.string_of_pexp pexp); + prerr_endline ("0 pxp " ^ pexp_string pexp); ()); - print_string ("1 exp " ^ lexp_string e ^ "\n"); - print_string ("2 inf " ^ lexp_string inferred_t ^ "\n"); - print_string ("3 ann " ^ lexp_string t ^ "\n"); + print_string "1 exp "; lexp_print e; print_string "\n"; + print_string "2 inf "; lexp_print inferred_t; print_string "\n"; + print_string "3 ann "; lexp_print t; print_string "\n"; lexp_warning (pexp_location pexp) "Type Mismatch inferred != Annotation")); e @@ -516,7 +516,7 @@ 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 = " ^ Fmt_lexp.string_of_pexp func); + prerr_endline ("[StackTrace] func = " ^ pexp_string func); prerr_endline ("[StackTrace] sargs = ???"); prerr_endline ("[StackTrace] ctx = ???"); prerr_endline ("[StackTrace] i = " ^ string_of_int i); @@ -606,9 +606,9 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i = | e -> (* Process Arguments *) let largs, ret_type = try handle_fun_args [] sargs ltp - with Internal_error m -> print_string ( ( Fmt_lexp.string_of_lxp e ) ^ "---\n" ); + with Internal_error m -> print_string ( ( lexp_string e ) ^ "---\n" ); List.iter (fun s -> Sexp.sexp_print s; print_newline () ) sargs; - print_endline (">>>" ^ Fmt_lexp.string_of_lxp ltp); + print_endline (">>>" ^ lexp_string ltp); raise (Internal_error m) in Call (body, List.rev largs), ret_type in

===================================== src/opslexp.ml ===================================== --- a/src/opslexp.ml +++ b/src/opslexp.ml @@ -134,7 +134,7 @@ let rec lexp_whnf e (ctx : DB.lexp_context) meta_ctx : lexp = Debug_fun.do_debug (fun () -> prerr_endline ("[StackTrace] ------------------------------------------"); prerr_endline ("[StackTrace] let lexp_whnf e ctx meta_ctx"); - prerr_endline ("[StackTrace] e = " ^ Fmt_lexp.string_of_lxp e); + prerr_endline ("[StackTrace] e = " ^ lexp_string e); prerr_endline ("[StackTrace] ctx = ???"); prerr_endline ("[StackTrace] meta_ctx = ???"); prerr_endline ("[StackTrace] ------------------------------------------");

===================================== tests/inverse_test.ml ===================================== --- a/tests/inverse_test.ml +++ b/tests/inverse_test.ml @@ -126,10 +126,11 @@ let _ = generate_tests "INVERSION" fmt_res (fun (s, b) -> ( match inverse s with | Some (s') -> (let comp = scompose s s' in - let ret = (is_identity comp) - in let str = ((string_of_subst s), (string_of_subst s'), (string_of_subst comp)) - in (str, ret)) - | None -> ((string_of_subst s, "None", "None"), not b) + let ret = (is_identity comp) in + let str = (subst_string s, subst_string s', + subst_string comp) in + (str, ret)) + | None -> ((subst_string s, "None", "None"), not b) ) )

@@ -144,10 +145,12 @@ let _ = generate_tests "INVERSION-RAND" fmt_res (fun (s) -> ( match inverse s with | Some (s') -> (let comp = scompose s s' in - let ret = (is_identity comp) - in let str = ((string_of_subst s), (string_of_subst s'), (string_of_subst comp)) - in (str, ret)) - | None -> ((string_of_subst s , "None" , "None") , false) + let ret = (is_identity comp) in + let str = (subst_string s, + subst_string s', + subst_string comp) in + (str, ret)) + | None -> ((subst_string s , "None" , "None") , false) ))

let _ = run_all ()

===================================== tests/lparse_test.ml ===================================== --- a/tests/lparse_test.ml +++ b/tests/lparse_test.ml @@ -43,7 +43,7 @@ let generate_lexp_from_str str = let _ = generate_tests "TYPECHECK" (fun () -> [generate_lexp_from_str input]) - (fun x -> List.map string_of_lxp x) + (fun x -> List.map lexp_string x) (fun x -> (x, true))

let lctx = default_lctx

===================================== tests/unify_test.ml ===================================== --- a/tests/unify_test.ml +++ b/tests/unify_test.ml @@ -17,7 +17,6 @@ open Str

open Debug

-open Fmt_lexp open Debug_fun

type result = @@ -46,16 +45,16 @@ let max_dim (lst: (string * string * string * string) list): (int * int * int *i

let fmt (lst: (lexp * lexp * result * result) list): string list = let str_lst = List.map - (fun (l1, l2, r1, r2) -> ((string_of_lxp l1), (string_of_lxp l2), (string_of_result r1), (string_of_result r2))) + (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) -> (padding_right l1 l ' ') + in List.map (fun (l1, l2, r1, r2) -> (Fmt_lexp.padding_right l1 l ' ') ^ ", " - ^ (padding_right l2 c1 ' ') + ^ (Fmt_lexp.padding_right l2 c1 ' ') ^ " -> got: " - ^ (padding_right r2 r ' ') + ^ (Fmt_lexp.padding_right r2 r ' ') ^ " expected: " - ^ (padding_right r1 c2 ' ') + ^ (Fmt_lexp.padding_right r1 c2 ' ') ) str_lst

(* Inputs for the test *)

View it on GitLab: https://gitlab.com/monnier/typer/commit/6cb1661b329dde683650afd8ec30efeef4be...