BONNEVALLE Vincent pushed to branch unification at Stefan / Typer

Commits: 57ff42c3 by n3f4s at 2016-06-29T22:48:00+02:00 add printing function for the lexp

- - - - - 107698ef by n3f4s at 2016-06-29T22:48:25+02:00 add printing function for debugging

- - - - - 476e08f2 by n3f4s at 2016-06-29T22:49:48+02:00 add print for debugging

- - - - - 490c9126 by n3f4s at 2016-06-29T22:50:06+02:00 change result of _unify_inner

_unify_inner returned None instead of non-error value, which caused the unification of the a let with himself to fail

- - - - - 48bc1748 by n3f4s at 2016-06-29T22:51:38+02:00 add test case for let

- - - - -

4 changed files:

- + src/debug_fun.ml - + src/fmt_lexp.ml - src/unification.ml - tests/unify_test.ml

Changes:

===================================== src/debug_fun.ml ===================================== --- /dev/null +++ b/src/debug_fun.ml @@ -0,0 +1,32 @@ + +open Fmt_lexp + +let _debug = true + +let indent = ref 0 + +let do_debug func = + if _debug then (func ()) else () + +let clear_indent () = + do_debug (fun () -> indent := 0; ()) + +let unindent () = + do_debug (fun () -> indent := (max 0 (!indent - 1)); ()) + +let debug_print_lexp lxp = + let str = colored_string_of_lxp lxp str_yellow str_magenta + in do_debug (fun () -> print_string str; ()) + +let debug_print_unify fn lhs rhs str = + let debug_print_unify fn lhs rhs str = + print_newline (); + print_string (padding_left fn 10 ' '); + print_string " : "; + print_string (String.make (!indent * 4) '-'); + debug_print_lexp lhs; + print_string " , "; + debug_print_lexp rhs; + print_string str; + indent := !indent + 1; + in do_debug (fun () -> debug_print_unify fn lhs rhs str; ())

===================================== src/fmt_lexp.ml ===================================== --- /dev/null +++ b/src/fmt_lexp.ml @@ -0,0 +1,68 @@ + +open Sexp +open Lexp +open Fmt + +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 rec 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 (_, _, a, _, b) -> "Arrow(" ^ (string_of_lxp a) ^ " => " ^ (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 _ -> ("Sort") ^ "(...)" + | SortLevel _ -> ("SortLevel") ^ "(...)" + | Case _ -> ("Case") ^ "(...)" + | Susp _ -> "Susp(...)" + | _ -> "Unidentified Lexp" + +let 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 _ -> (lcol "Sort") ^ "(...)" + | SortLevel _ -> (lcol "SortLevel") ^ "(...)" + | Susp _ -> (lcol "Susp") ^ "(...)" + | _ -> (lcol "Unidentified Lexp") + +let padding_right (str: string ) (dim: int ) (char_: char) : string = + let diff = (dim - String.length str) + 5 + in let rpad = diff + in str ^ (String.make rpad char_) + +let padding_left (str: string ) (dim: int ) (char_: char) : string = + let diff = (dim - String.length str) + 5 + in let lpad = diff + in (String.make lpad char_) ^ str + +let center (str: string ) (dim: int ) (char_: char) : string = + let diff = (dim - String.length str) + 5 + in let lpad, rpad = ((diff / 2 ), ((diff / 2) + (diff mod 2))) + in (String.make lpad char_) ^ str ^ (String.make lpad char_)

===================================== src/unification.ml ===================================== --- a/src/unification.ml +++ b/src/unification.ml @@ -2,25 +2,28 @@ open Lexp open Sexp

+open Debug_fun + module VMap = Map.Make (struct type t = int let compare = compare end)

type substitution = lexp VMap.t type constraints = (lexp * lexp) list + (* IMPROVEMENT For error handling : can carry location and name of type error *) -(*type 'a expected =*) -(*| Some of 'a*) -(*| Error of Util.location * string (*location * type name*)*) -(*| None*) +(*type 'a result =*) + (*| 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 0 let create_metavar = global_last_metavar := !global_last_metavar + 1; !global_last_metavar

-(*let expected_to_option (e: 'a expected) : ('a option) =*) -(*match e with*) -(*| Some elt -> Some elt*) -(*| Error _ -> None*) -(*| None -> None*) - (* For convenience *) type return_type = (substitution * constraints) option

@@ -78,6 +81,7 @@ let zip_fold list1 list2 f = *)

let rec unify (l: lexp) (r: lexp) (subst: substitution) : return_type = + debug_print_unify "unify" l r ""; match (l, r) with | (_, Metavar _) -> _unify_metavar r l subst | (_, Call _) -> _unify_call r l subst @@ -153,15 +157,16 @@ and _unify_builtin (bltin: lexp) (lxp: lexp) (subst: substitution) : return_type * Let , lexp -> constraint *) and _unify_let (let_: lexp) (lxp: lexp) (subst: substitution) : return_type = + debug_print_unify "_unify_let" let_ lxp ""; match (let_, lxp) with | (Let (_, m, lxp_), Let (_, m1, lxp2)) -> - let f = (fun (_, t, x) acc -> t::x::acc) + let f = (fun (_, lxp, lt) acc -> lxp::lt::acc) in let tail = zip_fold m m1 f in (match tail with - | [] -> None + | [] -> debug_print_unify "_unify_let" let_ lxp " -> No unification"; None | _ -> _unify_inner ((lxp_, lxp2)::(tail)) subst ) - | (Let _, _) -> Some (subst, [(let_, lxp)]) - | _, _ -> None + | (Let _, _) -> debug_print_unify "_unify_let" let_ lxp " -> Constraint"; Some (subst, [(let_, lxp)]) + | _, _ -> debug_print_unify "_unify_let" let_ lxp " -> No unification"; None

(** Unify a Var and a lexp, if possible * (Var, Var) -> unify if they have the same debruijn index FIXME : shift indexes @@ -281,7 +286,7 @@ and _unify_case (case: lexp) (lxp: lexp) (subst: substitution) : return_type = * Inductive, Var -> constraint * Inductive, Call/Metavar/Case/Let -> constraint * Inductive, _ -> None - *) +*) 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)) in match (induct, lxp) with @@ -348,7 +353,6 @@ and _unify_inner_case l s = | [] -> None | _ -> _unify_inner_case l s)

- (***** for Inductive *****) (** for _unify_induct : unify the formal arg*) and _unify_inner_induct lst subst : return_type = @@ -385,7 +389,7 @@ and _unify_inner (lxp_l: (lexp * lexp) list) (subst: substitution) : return_type let merge ((s, c): (substitution * constraints)) (lxp_list: (lexp * lexp) list) : return_type = match _unify_inner lxp_list s with - | None -> None (* Some (s, c) *) + | None -> Some (s, c) | Some (s_,c_) -> Some (s_, c@c_) in match lxp_l with @@ -393,3 +397,4 @@ and _unify_inner (lxp_l: (lexp * lexp) list) (subst: substitution) : return_type | Some (s, c) -> merge (s, c) tail | None -> None) | [] -> None +

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

open Debug

+open Fmt_lexp +open Debug_fun + type result = | Constraint | Unification @@ -27,27 +30,6 @@ type unif_res = (result * (substitution * constraints) option * lexp * lexp)

type triplet = string * string * string

-(* String & lexp formatting *) -let rec 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 (_, _, a, _, b) -> "Arrow(" ^ (string_of_lxp a) ^ " => " ^ (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 _ -> ("Sort") ^ "(...)" - | SortLevel _ -> ("SortLevel") ^ "(...)" - | Case _ -> ("Case") ^ "(...)" - | Susp _ -> "Susp(...)" - | _ -> "???" - let string_of_result r = match r with | Constraint -> "Constraint" @@ -62,11 +44,6 @@ let max_dim (lst: (string * string * string * string) list): (int * int * int *i (0, 0, 0, 0) lst

-let padding_right (str: string ) (dim: int ) (char_: char) : string = - let diff = (dim - String.length str) + 5 - in let rpad = diff - in str ^ (String.make rpad char_) - 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))) @@ -75,11 +52,11 @@ let fmt (lst: (lexp * lexp * result * result) list): string list = in List.map (fun (l1, l2, r1, r2) -> (padding_right l1 l ' ') ^ " , " ^ (padding_right l2 c1 ' ') - ^ " -> got :" + ^ " -> got : " ^ (padding_right r2 r ' ') ^ " expected : " ^ (padding_right r1 c2 ' ') - ) str_lst + ) str_lst

(* Inputs for the test *) let str_induct = "Nat = inductive_ (dNat) (zero) (succ Nat)" @@ -93,6 +70,7 @@ let str_case2 = "i = case 0 | 0 => 12 | 1 => 12 | _ => 12" +let str_let = "i = let a = 5 in a + 1"

let generate_ltype_from_str str = List.hd ((fun (lst, _) -> @@ -113,6 +91,7 @@ let input_int_4 = generate_lexp_from_str str_int_4 let input_int_3 = generate_lexp_from_str str_int_3 let input_case = generate_lexp_from_str str_case let input_case2 = generate_lexp_from_str str_case2 +let input_let = generate_lexp_from_str str_let

let generate_testable (_: lexp list) : ((lexp * lexp * result) list) = ( Builtin ((Util.dummy_location, "Int=3"), Imm (Integer (Util.dummy_location, 3))), @@ -152,13 +131,21 @@ let generate_testable (_: lexp list) : ((lexp * lexp * result) list) = Imm (Integer (Util.dummy_location, 3))), Nothing )

::(input_induct , input_induct , Equivalent) + ::(input_int_4 , input_int_4 , Equivalent) + ::(input_int_3 , input_int_4 , Nothing) + ::(input_case , input_int_4 , Constraint) ::(input_case , input_induct , Constraint) ::(input_case , input_case , Equivalent) ::(input_case , input_case2 , Nothing)

+ ::(input_let , input_induct , Constraint) + ::(input_let , input_int_4 , Constraint) + ::(input_let , input_case , Constraint) + ::(input_let , input_let , Equivalent) + ::(Let (Util.dummy_location, [], (*TODO : better tests*) Var ((Util.dummy_location, "x_let"), 9)) , @@ -170,6 +157,7 @@ let generate_testable (_: lexp list) : ((lexp * lexp * result) list) =

let test_input (lxp1: lexp) (lxp2: lexp) (subst: substitution): unif_res = (*do_debug (fun () -> print_string (fmt_unification_of lxp1 lxp2));*) + clear_indent (); let res = unify lxp1 lxp2 subst in match res with | Some (s, []) when s = empty_subst -> (Equivalent, res, lxp1, lxp2)

View it on GitLab: https://gitlab.com/monnier/typer/compare/46aab4745eeb6b8ae28c7e7e6ac1643aa8f...