BONNEVALLE Vincent pushed to branch unification at Stefan / Typer

Commits: d3a880af by n3f4s at 2016-10-11T16:11:56+02:00 fix nosusp bug in unfiy

result of nosusp wasn't used when dispatching to specialized unify functions.

- - - - - 117a72f7 by n3f4s at 2016-10-11T16:13:32+02:00 remove default case hiding "coding" error

- - - - - 521cad46 by n3f4s at 2016-10-11T16:13:59+02:00 add test number(in comment) in unification tests

- - - - -

2 changed files:

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

Changes:

===================================== src/unification.ml ===================================== --- a/src/unification.ml +++ b/src/unification.ml @@ -66,7 +66,8 @@ 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 = - match (nosusp l, nosusp r) with + let l, r = (nosusp l, nosusp r) in + match (l, r) with | (_, Metavar _) -> _unify_metavar r l subst | (_, Call _) -> _unify_call r l subst | (_, Case _) -> _unify_case r l subst @@ -107,7 +108,6 @@ and _unify_imm (l: lexp) (r: lexp) (subst: substitution) : return_type = else None | (Imm _, Imm _) -> None | (Imm _, _) -> unify r l subst - | (_, _) -> None

(** Unify a Cons and a lexp - Cons, Cons -> if Cons ~= Cons then OK else ERROR

===================================== tests/unify_test.ml ===================================== --- a/tests/unify_test.ml +++ b/tests/unify_test.ml @@ -118,56 +118,56 @@ let generate_testable (_: lexp list) : ((lexp * lexp * result) list) = 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_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) - - ::(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) - ::(input_arrow2 , input_lambda , Unification) - ::(input_arrow2 , input_lambda2 , Unification) - ::(input_arrow2 , input_arrow3 , Unification) - ::(input_arrow3 , input_arrow , Unification) - ::(input_arrow2 , input_arrow , Unification) - ::(input_arrow3 , input_arrow3 , Equivalent) - - ::(input_type , input_type_t , Equivalent) - - ::(Metavar (0, S.Identity, (Util.dummy_location, "M")), Var ((Util.dummy_location, "x"), 3), Unification) + ::(input_induct , input_induct , Equivalent) (* 2 *) + ::(input_int_4 , input_int_4 , Equivalent) (* 3 *) + ::(input_int_3 , input_int_4 , Nothing) (* 4 *) + ::(input_case , input_int_4 , Constraint) (* 5 *) + ::(input_case , input_induct , Constraint) (* 6 *) + ::(input_case , input_case , Equivalent) (* 7 *) + ::(input_case , input_case2 , Nothing) (* 8 *) + + ::(input_let , input_induct , Constraint) (* 9 *) + ::(input_let , input_int_4 , Constraint) (* 10 *) + ::(input_let , input_case , Constraint) (* 11 *) + ::(input_let , input_let , Equivalent) (* 12 *) + ::(input_let2 , input_let , Equivalent) (* 13 *) + ::(input_let2 , input_let2 , Equivalent) (* 14 *) + + ::(input_lambda , input_int_4 , Nothing) (* 15 *) + ::(input_lambda , input_induct , Nothing) (* 16 *) + ::(input_lambda , input_case , Constraint) (* 17 *) + ::(input_lambda , input_case2 , Constraint) (* 18 *) + ::(input_lambda , input_let , Constraint) (* 19 *) + ::(input_lambda , input_induct , Nothing) (* 20 *) + ::(input_lambda , input_lambda , Equivalent) (* 21 *) + + ::(input_lambda2 , input_int_4 , Nothing) (* 22 *) + ::(input_lambda2 , input_induct , Nothing) (* 23 *) + ::(input_lambda2 , input_case , Constraint) (* 24 *) + ::(input_lambda2 , input_case2 , Constraint) (* 25 *) + ::(input_lambda2 , input_let , Constraint) (* 26 *) + ::(input_lambda2 , input_induct , Nothing) (* 27 *) + ::(input_lambda2 , input_lambda , Equivalent) (* 28 *) + ::(input_lambda2 , input_lambda2 , Equivalent) (* 29 *) + ::(input_lambda2 , input_lambda3 , Constraint) (* 30 *) + ::(input_lambda3 , input_lambda3 , Equivalent) (* 31 *) + + ::(input_arrow2 , input_int_4 , Unification) (* 32 *) + ::(input_arrow2 , input_induct , Unification) (* 33 *) + ::(input_arrow2 , input_case , Constraint) (* 34 *) + ::(input_arrow2 , input_case2 , Constraint) (* 35 *) + ::(input_arrow2 , input_let , Constraint) (* 36 *) + ::(input_arrow2 , input_induct , Unification) (* 37 *) + ::(input_arrow2 , input_lambda , Unification) (* 38 *) + ::(input_arrow2 , input_lambda2 , Unification) (* 39 *) + ::(input_arrow2 , input_arrow3 , Unification) (* 40 *) + ::(input_arrow3 , input_arrow , Unification) (* 41 *) + ::(input_arrow2 , input_arrow , Unification) (* 42 *) + ::(input_arrow3 , input_arrow3 , Equivalent) (* 43 *) + + ::(input_type , input_type_t , Equivalent) (* 44 *) + + ::(Metavar (0, S.Identity, (Util.dummy_location, "M")), Var ((Util.dummy_location, "x"), 3), Unification) (* 45 *)

::[]

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