BONNEVALLE Vincent pushed to branch unification at Stefan / Typer

Commits: 1fbfe683 by n3f4s at 2016-06-30T22:24:57+02:00 debug recursion on wrong lexp in _unify_call

- - - - - 3f93815b by n3f4s at 2016-06-30T22:26:01+02:00 better printing for debugging & test

- - - - - c520b3e9 by n3f4s at 2016-06-30T22:26:16+02:00 add test case

- - - - -

4 changed files:

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

Changes:

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

open Fmt_lexp

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

let logs = ref []

@@ -22,6 +23,7 @@ let clear_indent () = indent := !indent + 1; ) (!logs); logs := []; + print_newline (); ())

let debug_print_lexp lxp =

===================================== src/fmt_lexp.ml ===================================== --- a/src/fmt_lexp.ml +++ b/src/fmt_lexp.ml @@ -21,7 +21,7 @@ let rec string_of_lxp lxp = | 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) ^ ") )" + | 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") ^ "(...)"

===================================== src/unification.ml ===================================== --- a/src/unification.ml +++ b/src/unification.ml @@ -252,10 +252,13 @@ and _unify_call (call: lexp) (lxp: lexp) (subst: substitution) : return_type = | None -> None | Some tail -> _unify_inner ((lxp1, lxp2)::(tail)) subst) in - match (call, lxp) with - | (Call (lxp1, lxp_list1), Call (lxp2, lxp_list2)) -> try_zip_fold lxp_list1 lxp_list2 lxp lxp2 subst + let tmp = 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

(** Apply unsusp to the Susp and unify the result with the lexp *) @@ -416,12 +419,19 @@ and _unify_inner (lxp_l: (lexp * lexp) list) (subst: substitution) : return_type (lxp_list: (lexp * lexp) list) : return_type = match _unify_inner lxp_list s with (*| None -> Some (s, c)*) - | None -> Debug_fun.debug_print "_unify_inner.merge" "unification failed"; None - | Some (s_,c_) -> Debug_fun.debug_print "_unify_inner.merge" "unification success"; Some (s_, c@c_) + | None -> None + | Some (s_,c_) -> Some (s_, c@c_) in - match lxp_l with + let tmp = match lxp_l with | (lxp1, lxp2)::tail -> ( match unify lxp1 lxp2 subst with | Some (s, c) -> merge (s, c) tail - | None -> Debug_fun.debug_print "_unify_inner" "unification failed"; None) - | [] -> Debug_fun.debug_print "_unify_inner" "unification success : list empty"; Some (subst, []) + | None -> None) + | [] -> 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 ) + | 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 )

===================================== tests/unify_test.ml ===================================== --- a/tests/unify_test.ml +++ b/tests/unify_test.ml @@ -50,11 +50,11 @@ let fmt (lst: (lexp * lexp * result * result) list): string list = lst in let l, c1, c2, r = max_dim str_lst in List.map (fun (l1, l2, r1, r2) -> (padding_right l1 l ' ') - ^ " , " + ^ "," ^ (padding_right l2 c1 ' ') - ^ " -> got : " + ^ "-> got: " ^ (padding_right r2 r ' ') - ^ " expected : " + ^ "expected: " ^ (padding_right r1 c2 ' ') ) str_lst

@@ -70,6 +70,10 @@ let str_case2 = "i = case 0 | 0 => 12 | _ => 12" let str_let = "i = let a = 5 in a + 1" +let str_let2 = "j = let b = 5 in b" +let str_lambda = "sqr = lambda (x : Int) -> x * x;" +let str_lambda2 = "sqr = lambda (x : Int) -> x * x;" +let str_lambda3 = "sqr = lambda (x : Int) -> lambda (y : Int) -> x * y;"

let generate_ltype_from_str str = List.hd ((fun (lst, _) -> @@ -85,22 +89,25 @@ let generate_lexp_from_str str = (List.flatten lst)) (lexp_decl_str str default_lctx))

-let input_induct = generate_lexp_from_str str_induct -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 input_induct = generate_lexp_from_str str_induct +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 input_let2 = generate_lexp_from_str str_let +let input_lambda = generate_lexp_from_str str_lambda +let input_lambda2 = generate_lexp_from_str str_lambda2 +let input_lambda3 = generate_lexp_from_str str_lambda3

let generate_testable (_: lexp list) : ((lexp * lexp * result) list) = - ( Builtin ((Util.dummy_location, "Int=3"), Imm (Integer (Util.dummy_location, 3))), - Imm (Integer (Util.dummy_location, 3)), Equivalent) - - ::( Var ((Util.dummy_location, "x"), 3), - Var ((Util.dummy_location, "y"), 4), Nothing ) - - ::( Var ((Util.dummy_location, "x"), 3), - Metavar (0, (Util.dummy_location, "M")), Unification ) + (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)

::( Lambda ((Aexplicit), (Util.dummy_location, "L1"), @@ -111,58 +118,42 @@ let generate_testable (_: lexp list) : ((lexp * lexp * result) list) = Var((Util.dummy_location, "z"), 4), Imm (Integer (Util.dummy_location, 3))), Unification )

- ::( Cons (((Util.dummy_location, "Cons"), 3), (Util.dummy_location, "Cons")) , - Imm (Integer (Util.dummy_location, 3)) , Nothing ) - - ::( Cons (((Util.dummy_location, "Cons"), 3), (Util.dummy_location, "Cons")) , - Imm (Integer (Util.dummy_location, 3)), Nothing) - - ::( Cons (((Util.dummy_location, "Cons"), 3), (Util.dummy_location, "Cons")) , - Var ((Util.dummy_location, "y"), 4), Nothing ) - - ::( Cons (((Util.dummy_location, "Cons"), 3), (Util.dummy_location, "Cons")) , - Metavar (0, (Util.dummy_location, "M")), Unification ) - - ::( Cons (((Util.dummy_location, "Cons"), 3), (Util.dummy_location, "Cons")) , - Lambda ((Aexplicit), - (Util.dummy_location, "L2"), - Var((Util.dummy_location, "z"), 4), - 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) + ::(input_let , input_induct , Constraint) + ::(input_let , input_int_4 , Constraint) + ::(input_let , input_case , Constraint) + ::(input_let , input_let , Equivalent) + ::(input_let2 , input_let , Equivalent) + ::(input_let2 , input_let2 , Equivalent) + + ::(input_lambda , input_int_4 , Nothing) + ::(input_lambda , input_induct , Nothing) + ::(input_lambda , input_case , Constraint) + ::(input_lambda , input_case2 , Constraint) + ::(input_lambda , input_let , Constraint) + ::(input_lambda , input_induct , Nothing) + ::(input_lambda , input_lambda , Equivalent) + + ::(input_lambda2 , input_int_4 , Nothing) + ::(input_lambda2 , input_induct , Nothing) + ::(input_lambda2 , input_case , Constraint) + ::(input_lambda2 , input_case2 , Constraint) + ::(input_lambda2 , input_let , Constraint) + ::(input_lambda2 , input_induct , Nothing) + ::(input_lambda2 , input_lambda , Equivalent) + ::(input_lambda2 , input_lambda2 , Equivalent) + ::(input_lambda2 , input_lambda3 , Constraint) + ::(input_lambda3 , input_lambda3 , Equivalent)

- ::(Let (Util.dummy_location, - [], (*TODO : better tests*) - Var ((Util.dummy_location, "x_let"), 9)) , - Lambda ((Aexplicit), - (Util.dummy_location, "L2"), - Var((Util.dummy_location, "z"), 4), - Imm (Integer (Util.dummy_location, 3))), Constraint ) ::[]

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 + let tmp = match res with | Some (s, []) when s = empty_subst -> (Equivalent, res, lxp1, lxp2) | Some (_, []) -> (Unification, res, lxp1, lxp2) | Some _ -> (Constraint, res, lxp1, lxp2) | None -> (Nothing, res, lxp1, lxp2) + in clear_indent (); tmp

let check (lxp1: lexp ) (lxp2: lexp ) (res: result) (subst: substitution ): bool = let r, _, _, _ = test_input lxp1 lxp2 subst @@ -181,10 +172,12 @@ let unifications = List.map in (l1, l2, res, r)) (generate_testable [])

+let idx = ref 0 let _ = List.map (fun (str, (l1, l2, expected, res)) -> + idx := !idx + 1; add_test "UNIFICATION" - (str) + ((if !idx < 10 then "0" else "") ^ (string_of_int !idx) ^ " " ^ str ) (fun () -> if expected = res then success () else failure ())) (List.combine (fmt unifications) unifications )

View it on GitLab: https://gitlab.com/monnier/typer/compare/239ce52674b8835de01bc1836510f70cee4...