BONNEVALLE Vincent pushed to branch unification at Stefan / Typer
Commits: 406ac0da by n3f4s at 2016-09-09T03:50:02+02:00 clean unification.ml
- better variable naming - unify formatting - move types to lexp.ml
- - - - - 1b57485f by n3f4s at 2016-09-09T03:52:55+02:00 add metavar context printing and clean code
- - - - - 59a7efc6 by n3f4s at 2016-09-09T03:54:41+02:00 add doc
- - - - - a7136734 by n3f4s at 2016-09-09T04:08:37+02:00 clean code and add doc
- - - - - 13b6dba7 by n3f4s at 2016-09-09T17:32:30+02:00 add doc
- - - - - c2e85c1e by n3f4s at 2016-09-09T18:12:36+02:00 add debug output
- - - - - ea747f75 by n3f4s at 2016-09-09T18:13:11+02:00 clean code && correct moved function
- - - - -
11 changed files:
- src/debruijn.ml - src/debug_fun.ml - src/env.ml - src/eval.ml - src/fmt_lexp.ml - src/inverse_subst.ml - src/lexp.ml - src/lparse.ml - src/opslexp.ml - src/unification.ml - tests/unify_test.ml
Changes:
===================================== src/debruijn.ml ===================================== --- a/src/debruijn.ml +++ b/src/debruijn.ml @@ -145,7 +145,7 @@ let env_lookup_expr ctx (v : vref): lexp option = match lxp with | LetDef lxp -> Some (L.push_susp lxp (S.shift (idx + 1 - r))) (* FIXME: why Sort here? *) - | _ -> None + | _ -> None
let env_lookup_by_index index (ctx: lexp_context): env_elem = (Myers.nth index (_get_env ctx))
===================================== src/debug_fun.ml ===================================== --- a/src/debug_fun.ml +++ b/src/debug_fun.ml @@ -6,9 +6,11 @@ let _debug = true
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 := ((padding_left str1 20 ' ')^" : ", (str2^"\n"))::(!logs); ()
@@ -26,13 +28,16 @@ let clear_indent () = 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 = colored_string_of_lxp lxp str_yellow str_magenta 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 ' ') ^ " : ",
===================================== src/env.ml ===================================== --- a/src/env.ml +++ b/src/env.ml @@ -129,6 +129,17 @@ 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 ();();); env_error dloc ("Variable lookup failure. Expected: "" ^ n2 ^ "[" ^ (string_of_int idx) ^ "]" ^ "" got "" ^ n1 ^ """))) @@ -143,6 +154,8 @@ let rte_shift vref ctx = let (_, (osize, _)) = ctx in (* number of variable declared outside *) let csize = get_rte_size ctx in (* current size *) let offset = csize - osize in + Debug_fun.do_debug (fun () -> + prerr_endline (">>> offset " ^ (string_of_int offset) ^ " (" ^ (string_of_int csize)^ " - " ^ (string_of_int osize) ^ ")"); ()); let ((loc, name), idx) = vref in (* check if variable is free *) let offset = if idx > offset then offset else 0 in
===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -65,6 +65,14 @@ let _builtin_lookup = ref SMap.empty (* This is an internal definition * 'i' is the recursion depth used to print the call trace *) let rec _eval lxp ctx i: (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_str lxp); + prerr_endline ("[StackTrace] ctx = ???"); + prerr_endline ("[StackTrace] i = " ^ (string_of_int i)); + prerr_endline ("[StackTrace] ------------------------------------------"); + ()); let tloc = elexp_location lxp in
(if i > (!_eval_max_recursion_depth) then @@ -111,6 +119,20 @@ 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_str 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 ("index shifted " ^ (string_of_int (rte_shift v ctx))); + prerr_endline ("ctx size " ^ (string_of_int (get_rte_size ctx))); + () + ); try get_rte_variable (Some name) (idx) ctx with e -> eval_error loc ("Variable: " ^ name ^ (str_idx idx) ^ " was not found ") @@ -357,6 +379,13 @@ let eval lxp ctx = _eval lxp ctx 1
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_str lxp); + prerr_endline ("[StackTrace] ctx = ???"); + prerr_endline ("[StackTrace] ------------------------------------------"); + ()); try _global_eval_trace := []; eval lxp ctx @@ -367,6 +396,14 @@ let debug_eval lxp 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 ===================================== --- a/src/fmt_lexp.ml +++ b/src/fmt_lexp.ml @@ -1,30 +1,30 @@
-open Sexp -open Pexp -open Lexp -open Fmt +module L = Lexp +module S = Subst
let _color = true
-let str_red str = if _color then red ^ str ^ reset else str -let str_green str = if _color then green ^ str ^ reset else str -let str_magenta str = if _color then magenta ^ str ^ reset else str -let str_yellow str = if _color then yellow ^ str ^ reset else str -let str_cyan str = if _color then cyan ^ str ^ reset else str +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 (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" + | 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 @@ -37,61 +37,60 @@ and pp_ocaml_string_of_subst s =
and string_of_lxp lxp = match lxp with - | Imm (Integer (_, value)) -> "Integer(" ^ (string_of_int value) ^ ")" - | Imm (String (_, value)) -> "String(" ^ value ^ ")" - | Imm (Float (_, value)) -> "Float(" ^ (string_of_float value) ^ ")" - | Cons (((_,name),_),_) -> "Cons(" ^ name ^ ")" - | Builtin ((_, name), _) -> "Builtin(" ^ name ^ ")" - | Let (_) -> "Let(..)" - | Var ((_, name), idx) -> "Var(" ^ name ^ ", #" ^(string_of_int idx) ^ ")" - | Arrow (kind, Some(_, name), a, _, b) -> name ^ ":Arrow(" ^ (string_of_lxp a) ^ ":" ^ string_of_kind kind ^ " => " ^ (string_of_lxp b) ^ ")" - | Arrow (kind, _, a, _, b) -> "Arrow(" ^ (string_of_lxp a) ^ ":" ^ string_of_kind kind ^ " => " ^ (string_of_lxp b) ^ ")" - | Lambda (_,(_, name), dcl, body) -> "Lambda(" ^ name ^ ": " ^ (string_of_lxp dcl) ^ " => (" ^ (string_of_lxp body) ^ "))" - | Metavar (value, _, (_, name)) -> "Metavar(" ^ (string_of_int value) ^ ", " ^ name ^ ")" - | Call (_) -> "Call(...)" - | Inductive _ -> ("Inductive") ^ "(...)" - | Sort (_, s) -> ("Sort") ^ "(" ^ string_of_sort s ^ ")" - | SortLevel l -> ("SortLevel") ^ "(" ^ string_of_sort_level l ^ ")" - | Case _ -> ("Case") ^ "(...)" - | Susp (v, s) -> "Susp(" ^ (string_of_lxp v) ^ ", " ^ (string_of_subst s) ^ ")" - | _ -> "Unidentified Lexp" + | 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 (((_,tname),_),(_, cname)) -> "Cons(" ^ tname ^ ", " ^ 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 - | Aexplicit -> "Aexplicit" - | Aimplicit -> "Aimplicit" - | Aerasable -> "Aerasable" + | Pexp.Aexplicit -> "Aexplicit" + | Pexp.Aimplicit -> "Aimplicit" + | Pexp.Aerasable -> "Aerasable"
and string_of_sort_level lvl = match lvl with - | SLn i -> "SLn(" ^ string_of_int i ^ ")" - | SLsucc l -> "SLsucc(" ^ string_of_lxp l^ ")" + | L.SLn i -> "SLn(" ^ string_of_int i ^ ")" + | L.SLsucc l -> "SLsucc(" ^ string_of_lxp l^ ")"
and string_of_sort sort = match sort with - | Stype lxp -> "Stype(" ^ string_of_lxp lxp ^ ")" - | StypeOmega -> "StypeOmega" - | StypeLevel -> "StypeLevel" + | 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 - | Imm (Integer (_, value)) -> (lcol "Integer") ^ "(" ^ (vcol (string_of_int value)) ^ ")" - | Imm (String (_, value)) -> (lcol "String") ^ "(" ^ (vcol value ) ^ ")" - | Imm (Float (_, value)) -> (lcol "Float" ) ^ "(" ^ (vcol (string_of_float value)) ^ ")" - | Cons (((_,name),_),_) -> (lcol "Cons" ) ^ "(" ^ (vcol name) ^ ")" - | Builtin ((_, name), _) -> (lcol "Builtin") ^ "(" ^ (vcol name) ^ ")" - | Let (_) -> (lcol "Let(..)") - | Var ((_, name), idx) -> (lcol "Var" ) ^ "(" ^ (vcol name ) ^ ", " ^ (vcol ("#" ^ (string_of_int idx))) ^ ")" - | Arrow (_, _, a, _, b) -> (lcol "Arrow(") ^ (vcol (string_of_lxp a)) ^ " => " ^ (vcol (string_of_lxp b)) ^ ")" - | Lambda (_,(_, name), dcl, body) -> (lcol "Lambda") ^ "(" ^ (vcol name) ^ " : " ^ (vcol (string_of_lxp dcl)) - ^ " => (" ^ (vcol (string_of_lxp body)) ^ "))" - | Metavar (value, _, (_, name)) -> (lcol "Metavar" ) ^ "(" ^ (vcol (string_of_int value)) ^ ", " ^ (vcol name) ^ ")" - | Call (_) -> (lcol "Call(...)" ) - | Case _ -> (lcol "Case") ^ "(...)" - | Inductive _ -> (lcol "Inductive") ^ "(...)" - | Sort (_, s) -> (lcol "Sort") ^ "(" ^ vcol (string_of_sort s)^ ")" - | SortLevel l -> (lcol "SortLevel") ^ "(" ^ vcol (string_of_sort_level l) ^ ")" - | Susp (v, s) -> (lcol "Susp") ^ "(" ^ colored_string_of_lxp v lcol vcol ^ ", " ^ vcol (string_of_subst s) ^")" - | _ -> (lcol "Unidentified Lexp") + | 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 (((_,name),_),_) -> (lcol "Cons" ) ^ "(" ^ (vcol name) ^ ")" + | 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) @@ -105,36 +104,68 @@ let padding_left (str: string ) (dim: int ) (char_: char) : string =
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 lpad char_) + 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 - (* | Psort of location * sort *) - | Pimm (Integer (_, i)) -> "Pimm( Integer (" ^ string_of_int i ^ "))" - | Pimm (Float (_, f)) -> "Pimm( Float (" ^ string_of_float f ^ "))" - | Pimm (String (_, s)) -> "Pimm (String (" ^ s ^ "))" - | Pvar (_, s) -> "Pvar (" ^ s ^ ")" - | Phastype (_, p1, p2) -> "Phastype (" ^ string_of_pexp p1 ^ ", " ^ string_of_pexp p2 ^ ")" - | Pmetavar (_, s) -> "Pmetavar (" ^ s ^ ")" - | Plet (_, _, p) -> "Plet (_, " ^ string_of_pexp p ^ ")" - | Parrow (_, _, _, _, _) -> "Parrow (...)" - | Plambda _ -> "Plambda (...)" - | Pcall _ -> "Pcall (...)" - | Pinductive _ -> "Pinductive (...)" - | Pcons ( (_, s), (_, s2) ) -> "Pcons (" ^ s ^ ", " ^ s2 ^ ")" - | Pcase _ -> "Pcase (...)" - | _ -> "Pexp not handled" - - -(* let rec string_of_lexp_ctx (senv, env, prop) = *) - (* "(" ^ (string_of_senv senv) ^ "\n" ^ (string_of_env env) ^ "\n" ^ (string_of_prop prop) ^ ")" *) -(* and string_of_senv (len, sc) = *) - (* "(" ^ string_of_int len ^ ",\n " ^ (string_of_scope sc) ^ ")" *) -(* and string_of_scope sc = *) - (* "(" ^ *) - (* Debruijn.StringMap.fold (fun key value acc -> acc ^ ", (" ^ key ^ string_of_int value ^ ")") sc "" *) - (* ^ ")" *) -(* and string_of_env env = *) + | 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 ( (_, s), (_, s2) ) -> "Pcons (" ^ s ^ ", " ^ 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/inverse_subst.ml ===================================== --- a/src/inverse_subst.ml +++ b/src/inverse_subst.ml @@ -3,36 +3,41 @@ open Lexp open Util module S = Subst
-(** Provide inverse function for computing the inverse of a substitution -*) +(** Provide inverse function for computing the inverse of a substitution *)
(* Transformation *)
+(** Convenience types and variables *) + type inter_subst = lexp list (* Intermediate between "tree"-like substitution and fully flattened subsitution *)
let dummy_var = Var((dummy_location, "DummyVar"), -1)
type substIR = ((int * int) list * int)
-(* toIr + flattenIr + to_list *) -(* TODO : find better name ?*) +(** Transform a substitution to a more linear substitution + * makes the inversion easier + * Example of result : ((new_idx, old_position)::..., shift)*) let transfo (s: lexp S.subst) : substIR option = let rec transfo (s: lexp S.subst) (off_acc: int) (idx: int): substIR option = - let valueOf (v: lexp): int = + let indexOf (v: lexp): int = (* Helper : return the index of a variabble *) match v with | Var (_, v) -> v | _ -> assert false - in let shiftVar (var: lexp) (offset: int): int = valueOf (mkSusp var (S.shift offset)) - in match s with + in + let shiftVar (var: lexp) (offset: int): int = + indexOf (mkSusp var (S.shift offset)) (* Helper : shift the index of a var *) + in + match s with | S.Cons (Var _ as v, s) -> (match transfo s off_acc (idx + 1) with | Some (tail, off) -> let newVar = shiftVar v off_acc - in if newVar >= off then None + in if newVar >= off then None (* Error *) else Some (((shiftVar v off_acc), idx)::tail, off) | None -> None) | S.Shift (s, offset) -> transfo s (offset + off_acc) idx - | S.Identity -> Some ([], off_acc) - | _ -> None + | S.Identity -> Some ([], off_acc) (* End of recursion *) + | _ -> None (* Error *) in transfo s 0 0
(* Inverse *) @@ -55,17 +60,17 @@ let mkVar (idx: int): lexp = Var((U.dummy_location, ""), idx) @param acc recursion accumulator *) let fill (l: (int * int) list) (nbVar: int) (shift: int): lexp S.subst option = - let rec genDummyVar (beg_: int) (end_: int) (l: lexp S.subst): lexp S.subst = + let rec genDummyVar (beg_: int) (end_: int) (l: lexp S.subst): lexp S.subst = (* Create the filler variables *) if beg_ < end_ then S.cons (mkVar (nbVar + 1)) (genDummyVar (beg_ + 1) end_ l) else l in - let fill_before (l: (int * int) list) (s: lexp S.subst) (nbVar: int): lexp S.subst option = + let fill_before (l: (int * int) list) (s: lexp S.subst) (nbVar: int): lexp S.subst option = (* Fill if the first var is not 0 *) match l with | [] -> Some (genDummyVar 0 nbVar S.identity) | (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 S.subst option = + in let rec fill_after (l: (int * int) list) (nbVar: int) (shift: int): lexp S.subst option = (* Fill gaps *) match l with | (idx1, val1)::(idx2, val2)::tail when (idx1 = idx2) -> None
===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -95,6 +95,11 @@ type varbind = | ForwardRef | LetDef of lexp
+module VMap = Map.Make (struct type t = int let compare = compare end) +type substitution = lexp VMap.t +type constraints = (lexp * lexp) list +let empty_subst = (VMap.empty) + (********* 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
===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -131,7 +131,7 @@ let get_type0 ctx = build_var "Type" ctx let get_int ctx = build_var "Int" ctx
(* :-( *) -let global_substitution = ref (Unif.empty_subst, []) +let global_substitution = ref (empty_subst, [])
let mkMetavar () = let meta = Unif.create_metavar () in let name = "__Metavar_" ^ (string_of_int meta) @@ -441,15 +441,15 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i = (* retrieve function's body *) let body, ltp = _lexp_p_infer func ctx (i + 1) in let ltp = nosusp ltp in + + let rec handle_fun_args largs sargs ltp = Debug_fun.do_debug (fun () -> - prerr_endline ">>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>"; - prerr_endline ("ltp : " ^ Fmt_lexp.string_of_lxp ltp); - prerr_endline ("body : " ^ Fmt_lexp.string_of_lxp body); - prerr_endline (string_of_int (List.length sargs) ^ " args"); + print_endline ">>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>"; + print_lexp_ctx ctx; + flush stdout; prerr_endline "<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<"; - prerr_newline ();();); - - let rec handle_fun_args largs sargs ltp = match sargs with + print_newline ();();); + match sargs with | [] -> largs, ltp | (Node (Symbol (_, "_:=_"), [Symbol (_, aname); sarg])) :: sargs (* Explicit-implicit argument. *) @@ -460,8 +460,12 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i = let larg = _lexp_p_check parg arg_type ctx i in handle_fun_args ((ak, larg) :: largs) sargs (L.mkSusp ret_type (S.substitute larg)) - | _ -> lexp_fatal (sexp_location sarg) - "Explicit arg to non-function") + | e -> Debug_fun.do_debug (fun () -> + print_endline ("<>explicit arg : " ^ Fmt_lexp.string_of_lxp ltp); + print_endline ("<>explicit res : " ^ Fmt_lexp.string_of_lxp e); + ()); + lexp_fatal (sexp_location sarg) + ("Explicit-implicit arg " ^ aname ^ " to non-function")) | sarg :: sargs (* Process Argument *) -> (match OL.lexp_whnf ltp ctx meta_ctx with @@ -507,7 +511,12 @@ and lexp_call (func: pexp) (sargs: sexp list) ctx i =
| e -> (* Process Arguments *) - let largs, ret_type = handle_fun_args [] sargs ltp in + let largs, ret_type = try handle_fun_args [] sargs ltp + with Internal_error m -> print_string ( ( Fmt_lexp.string_of_lxp e ) ^ "---\n" ); + List.iter (fun s -> Sexp.sexp_print s; print_newline () ) sargs; + print_endline (">>>" ^ Fmt_lexp.string_of_lxp ltp); + raise (Internal_error m) + in Call (body, List.rev largs), ret_type in
let handle_macro_call () = @@ -1060,6 +1069,15 @@ 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 @@ -118,7 +118,16 @@ and conv_p e1 e2 = conv_p' S.identity S.identity e1 e2 * 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 rec lexp_whnf e ctx meta_ctx = match e with +let rec lexp_whnf e ctx meta_ctx = + 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] ctx = ???"); + prerr_endline ("[StackTrace] meta_ctx = ???"); + prerr_endline ("[StackTrace] ------------------------------------------"); + ()); + match e with (* | Let (_, defs, body) -> FIXME!! Need recursive substitutions! *) | Var v -> (match DB.env_lookup_expr ctx v with | None -> e @@ -162,7 +171,7 @@ let rec lexp_whnf e ctx meta_ctx = match e with | Cons (_, (_, name)) -> reduce name [] | Call (Cons (_, (_, name)), aargs) -> reduce name aargs | e' -> Case (l, e', bt, rt, branches, default)) - | Metavar (idx, _, _) -> lexp_whnf (Unification.VMap.find idx meta_ctx) ctx meta_ctx + | Metavar (idx, _, _) -> lexp_whnf (L.VMap.find idx meta_ctx) ctx meta_ctx | e -> e
===================================== src/unification.ml ===================================== --- a/src/unification.ml +++ b/src/unification.ml @@ -3,26 +3,12 @@ open Lexp open Sexp open Inverse_subst
-module VMap = Map.Make (struct type t = int let compare = compare end) - -type substitution = lexp VMap.t -type constraints = (lexp * lexp) list
(** Provide unify function for unifying two Lambda-Expression *)
-(* IMPROVEMENT For error handling : can carry location and name of type error *) -(*type 'a result =*) (* use std result type*) -(*| Some of 'a*) -(*| Error of Util.location * string (*location * type name*)*) -(*| Nil*) - -(*let result_to_option (e: 'a result) : ('a option) =*) -(*match e with*) -(*| Some elt -> Some elt*) -(*| Error _ -> None*) -(*| Nil -> None*) - +(* :-( *) let global_last_metavar = ref (-1) (*The first metavar is 0*) + let create_metavar () = global_last_metavar := !global_last_metavar + 1; !global_last_metavar let mkMetavar subst vdef = Metavar (create_metavar (), subst, vdef)
@@ -44,8 +30,6 @@ let find_or_none (value: lexp) (map: substitution) : lexp option = else None) | _ -> None
-let empty_subst = (VMap.empty) - (** Zip while applying a function, returns <code>None</code> list if l1 & l2 have different size*) let zip_map (l1: 'a list ) (l2: 'b list ) (f: ('a -> 'b -> 'c)): 'c list option = let rec zip_ ll1 ll2 f = @@ -82,7 +66,7 @@ let zip_fold list1 list2 f = The metavar unifyer is the end rule, it can't call unify with it's parameter (changing their order) *) let rec unify (l: lexp) (r: lexp) (subst: substitution) : return_type = - let tmp = match (nosusp l, nosusp r) with + match (nosusp l, nosusp r) with | (_, Metavar _) -> _unify_metavar r l subst | (_, Call _) -> _unify_call r l subst | (_, Case _) -> _unify_case r l subst @@ -102,9 +86,6 @@ let rec unify (l: lexp) (r: lexp) (subst: substitution) : return_type = | (Inductive _, _) -> _unfiy_induct l r subst | (Sort _, _) -> _unify_sort l r subst | (SortLevel _, _) -> _unify_sortlvl l r subst - in match tmp with - | Some _ -> Debug_fun.debug_print_unify "unify" l r " -> unification success"; tmp - | None -> Debug_fun.debug_print_unify "unify" l r " -> unification failed"; tmp
(********************************* Type specific unify *******************************)
@@ -132,9 +113,6 @@ and _unify_imm (l: lexp) (r: lexp) (subst: substitution) : return_type = - Cons, Cons -> if Cons ~= Cons then OK else ERROR - Cons, _ -> ERROR *) -(*FIXME which parameter of Cons is it's name ?*) -(* symbol = (location * string)*) -(*TODO in index comparison : shift indexes ?*) and _unify_cons (cons: lexp) (lxp: lexp) (subst: substitution) : return_type = match (cons, lxp) with | (Cons ((_, idx), (_, name)), @@ -162,25 +140,22 @@ and _unify_builtin (bltin: lexp) (lxp: lexp) (subst: substitution) : return_type and _unify_let (let_: lexp) (lxp: lexp) (subst: substitution) : return_type = let concat = (fun (_, lxp, lt) acc -> lxp::lt::acc) in - let try_zip_fold m m1 f lxp_ lxp2 subst = match zip_fold m m1 f with - | Some [] -> Some (subst, []) (* ??? *) + let try_zip_fold body1 body2 func lxp_ lxp2 subst = + match zip_fold body1 body2 func with + | Some [] -> Some (subst, []) | None -> None | Some tail -> _unify_inner ((lxp_, lxp2)::(tail)) subst in - let tmp = match (let_, lxp) with + match (let_, lxp) with | (Let (_, m, lxp_), Let (_, m1, lxp2)) -> try_zip_fold m m1 concat lxp_ lxp2 subst | (Let _, _) -> Some (subst, [(let_, lxp)]) | _, _ -> None - in match tmp with - | Some _ -> Debug_fun.debug_print_unify "_unify_let" let_ lxp " -> unification success"; tmp - | None -> Debug_fun.debug_print_unify "_unify_let" let_ lxp " -> unification failed"; tmp
(** Unify a Var and a lexp, if possible - - (Var, Var) -> unify if they have the same debruijn index FIXME : shift indexes + - (Var, Var) -> unify if they have the same debruijn index - (Var, Metavar) -> unify_metavar Metavar var subst - (Var _, _) -> unfiy lexp Var subst *) -(*FIXME : check for the value of Var -> need context ?*) and _unify_var (var: lexp) (r: lexp) (subst: substitution) : return_type = match (var, r) with | (Var (_, idx1), Var (_, idx2)) @@ -264,39 +239,35 @@ and _unify_call (call: lexp) (lxp: lexp) (subst: substitution) : return_type = | None -> None | Some tail -> _unify_inner ((lxp1, lxp2)::(tail)) subst) in - let tmp = match (call, lxp) with + match (call, lxp) with | (Call (lxp_left, lxp_list1), Call (lxp_right, lxp_list2)) -> try_zip_fold lxp_list1 lxp_list2 lxp_left lxp_right subst | (Call _, _) -> Some ((subst, [(call, lxp)])) | (_, _) -> None - in match tmp with - | None -> Debug_fun.debug_print_unify "_unify_call" call lxp " -> unification failed"; tmp - | Some _ -> Debug_fun.debug_print_unify "_unify_call" call lxp " -> unification success"; tmp
(** Unify a Case with a lexp - Case, Case -> try to unify - Case, _ -> Constraint *) and _unify_case (case: lexp) (lxp: lexp) (subst: substitution) : return_type = - let merge (_, c) r2 = match r2 with + let merge (_, const) subst_res = match subst_res with | None -> None - | Some (s', c') -> Some (s', c@c') + | Some (s', c') -> Some (s', const@c') in - let match_unify_inner lst sm1 sm2 s = match _unify_inner lst s with + let match_unify_inner lst smap1 smap2 subst = + match _unify_inner lst subst with | None -> None - | Some (s, c) -> merge (s, c) (_unify_inner_case (zip (SMap.bindings sm1) (SMap.bindings sm2)) s) + | Some (s, c) -> merge (s, c) (_unify_inner_case (zip (SMap.bindings smap1) (SMap.bindings smap2)) s) in - let match_lxp_opt lo1 lo2 tail sm1 sm2 s = match lo1, lo2 with - | Some lxp1, Some lxp2 -> match_unify_inner ((lxp1, lxp2)::tail) sm1 sm2 s + let match_lxp_opt lxp_opt1 lxp_opt2 tail smap1 smap2 subst = + match lxp_opt1, lxp_opt2 with + | Some lxp1, Some lxp2 -> match_unify_inner ((lxp1, lxp2)::tail) smap1 smap2 subst | _, _ -> None in - let tmp = match case, lxp with + match (case, lxp) with | (Case (_, lxp, lt11, lt12, smap, lxpopt), Case (_, lxp2, lt21, lt22, smap2, lxopt2)) -> match_lxp_opt lxpopt lxopt2 ((lt11, lt21)::(lt12, lt22)::[]) smap smap2 subst | (Case _, _) -> Some (subst, [(case, lxp)]) | (_, _) -> None - in match tmp with - | Some _ -> Debug_fun.debug_print_unify "_unify_case" case lxp " -> unification success"; tmp - | None -> Debug_fun.debug_print_unify "_unify_case" case lxp " -> unification failed"; tmp
(** Unify a Inductive and a lexp - Inductive, Inductive -> try unify @@ -306,13 +277,15 @@ and _unify_case (case: lexp) (lxp: lexp) (subst: substitution) : return_type = *) and _unfiy_induct (induct: lexp) (lxp: lexp) (subst: substitution) : return_type = let transform (a, b, c) (d, e, f) = ((a, Some b, c), (d, Some e, f)) - and merge m1 m2 (s, c) : return_type = match (_unify_induct_sub_list (SMap.bindings m1) (SMap.bindings m2) s) with - | Some (s', c') -> Some (s', c@c') + and merge map1 map2 (subst, const) : return_type = + match (_unify_induct_sub_list (SMap.bindings map1) (SMap.bindings map2) subst) with + | Some (s', c') -> Some (s', const@c') | None -> None in - let zip_unify lst subst m1 m2 : return_type = match _unify_inner_induct lst subst with + let zip_unify lst subst map1 map2 : return_type = + match _unify_inner_induct lst subst with | None -> None - | Some (s, c) -> merge m1 m2 (s, c) + | Some (s, c) -> merge map1 map2 (s, c) in match (induct, lxp) with | (Inductive (_, lbl1, farg1, m1), Inductive (_, lbl2, farg2, m2)) when lbl1 = lbl2 -> @@ -353,33 +326,34 @@ and _unify_sort (sort_: lexp) (lxp: lexp) (subst: substitution) : return_type = (************************ Helper function **************************************)
(***** for Case *****) -(** Check arg_king in (arg_kind * vdef option) list in Case *) +(** Check arg_king in <code>(arg_kind * vdef option) list </code> in Case *) and is_same arglist arglist2 = match arglist, arglist2 with | (akind, _)::t1, (akind2, _)::t2 when akind = akind2 -> is_same t1 t2 - | [], [] -> Debug_fun.debug_print "is_same" " unification success"; true - | _, _ -> Debug_fun.debug_print "is_same" " unification failed"; false + | [], [] -> true + | _, _ -> false
(** try to unify the SMap part of the case *) -and _unify_inner_case l s = - let merge (_, c) res = match res with +and _unify_inner_case lst subst = + let merge (_, c) res = + match res with | Some (s', c') -> Some (s', c@c') - | None -> None + | None -> None in - let rec _unify_inner_case list_ s = + let rec _unify_inner_case list_ subst = match list_ with | ((key, (_, arglist, lxp)), (key2, (_, arglist2, lxp2)))::tail when key = key2 -> (if is_same arglist arglist2 - then ( match unify lxp lxp2 s with + then ( match unify lxp lxp2 subst with | Some (s', c) -> merge (s', c) (_unify_inner_case tail s') - | None -> Debug_fun.debug_print "_unify_inner_case" "unification failed"; None) + | None -> None) else None) - | [] -> Debug_fun.debug_print "_unify_inner_lxp" "unification success"; Some (s, []) - | _ -> Debug_fun.debug_print "_unify_inner_case" "unification failed"; None - in (match l with - | Some [] -> Some (s, []) + | [] -> Some (subst, []) + | _ -> None + in (match lst with + | Some [] -> Some (subst, []) | None -> None - | Some l -> _unify_inner_case l s) + | Some l -> _unify_inner_case l subst)
(***** for Inductive *****) (** for _unify_induct : unify the formal arg*) @@ -388,17 +362,20 @@ and _unify_inner_induct lst subst : return_type = if a1 = a2 then unify l1 l2 subst else None in - List.fold_left (fun a e -> (match a with - | Some (s, c) -> (match test e s with + List.fold_left (fun a e -> + (match a with + | Some (s, c) -> + (match test e s with | Some (s1, c1) -> Some (s1, c1@c) | None -> Some (s, c)) - | None -> test e subst) + | None -> test e subst) ) None lst
(** unify the SMap of list in Inductive *) and _unify_induct_sub_list l1 l2 subst = let test l1 l2 subst = - let merge l1 l2 subst (s, c) = match (_unify_induct_sub_list l1 l2 subst) with + let merge l1 l2 subst (s, c) = + match (_unify_induct_sub_list l1 l2 subst) with | Some (s1, c1) -> Some (s1, c1@c) | None -> Some (s, c) in @@ -437,9 +414,9 @@ and _unify_inner (lxp_l: (lexp * lexp) list) (subst: substitution) : return_type | [] -> Some (subst, []) in match tmp with | None -> ( match lxp_l with - | [] -> Debug_fun.debug_print "_unify_inner" " -> list empty"; tmp - | (l1, l2)::_ -> Debug_fun.debug_print_unify "_unify_inner" l1 l2 " -> unification failed"; tmp ) + | [] -> tmp + | (l1, l2)::_ -> tmp ) | Some _ -> ( match lxp_l with - | [] -> Debug_fun.debug_print "_unify_inner" " -> list empty"; tmp - | (l1, l2)::_ -> Debug_fun.debug_print_unify "_unify_inner" l1 l2 " -> unification success"; tmp ) + | [] -> tmp + | (l1, l2)::_ -> tmp )
===================================== tests/unify_test.ml ===================================== --- a/tests/unify_test.ml +++ b/tests/unify_test.ml @@ -152,9 +152,9 @@ let generate_testable (_: lexp list) : ((lexp * lexp * result) list) = ::(input_lambda2 , input_lambda3 , Constraint) ::(input_lambda3 , input_lambda3 , Equivalent)
- ::(input_arrow2 , input_int_4 , Unification) (* changes in lexp_p_infer & lexp_p_check *) - ::(input_arrow2 , input_induct , Unification) (* changed the "output" of lexp_decl_str*) - ::(input_arrow2 , input_case , Constraint) (* which changed the type of the Lexp*) + ::(input_arrow2 , input_int_4 , Unification) + ::(input_arrow2 , input_induct , Unification) + ::(input_arrow2 , input_case , Constraint) ::(input_arrow2 , input_case2 , Constraint) ::(input_arrow2 , input_let , Constraint) ::(input_arrow2 , input_induct , Unification) @@ -178,7 +178,7 @@ let test_input (lxp1: lexp) (lxp2: lexp) (subst: substitution): unif_res = | Some (_, []) -> (Unification, res, lxp1, lxp2) | Some _ -> (Constraint, res, lxp1, lxp2) | None -> (Nothing, res, lxp1, lxp2) - in clear_indent (); tmp + in tmp
let check (lxp1: lexp ) (lxp2: lexp ) (res: result) (subst: substitution ): bool = let r, _, _, _ = test_input lxp1 lxp2 subst
View it on GitLab: https://gitlab.com/monnier/typer/compare/cd2691062d8d973994d8ff8afdb2b7d9e81...