BONNEVALLE Vincent pushed to branch unification at Stefan / Typer
Commits: af770325 by n3f4s at 2016-06-23T19:15:13+02:00 add test case to unify_test
- - - - - d1706192 by n3f4s at 2016-06-23T23:36:54+02:00 add printing of lexp type in _unify_test
- - - - - f2c80dc6 by n3f4s at 2016-06-24T20:44:39+02:00 add _unify_case and correct _unify_inner
make suer _unify_inner fail when one unification fail
- - - - - 674cb642 by n3f4s at 2016-06-24T20:54:29+02:00 add check of default in _unify_case
- - - - -
2 changed files:
- src/unification.ml - tests/unify_test.ml
Changes:
===================================== src/unification.ml ===================================== --- a/src/unification.ml +++ b/src/unification.ml @@ -80,6 +80,8 @@ let empty_subst = (VMap.empty) * Inductive , lexp -> ERROR (???)
(*TODO*) + * Sort , lexp -> + * SortLevel , lexp -> * lexp , lexp ->
* lexp is equivalent to _ in ocaml @@ -108,10 +110,49 @@ let rec unify (l: lexp) (r: lexp) (subst: substitution) : return_type = | (Metavar _, _) -> _unify_metavar l r subst | (Call _, _) -> _unify_call l r subst | (Susp _, _) -> _unify_susp l r subst - | (Case _, _) -> None (* Maybe Constraint instead ?*) + | (Case _, _) -> _unify_case l r subst | (Inductive _, _) -> _unfiy_induct l r subst | (_, _) -> None
+(** Check arg_king in (arg_kind * vdef option) list in Case *) +and is_same arglist arglist2 = + match arglist, arglist2 with + | (akind, _)::t1, (akind2, _)::t2 when akind = akind2 -> is_same t1 t2 + | [], [] -> true + | _, _ -> false + +(** try to unify the SMap part of the case *) +and _unify_inner_case l s = + let rec _unify_inner_case l s = + match l with + | ((key, (_, arglist, lxp)), (key2, (_, arglist2, lxp2)))::t when key = key2 -> + (if is_same arglist arglist2 then ( match unify lxp lxp2 s with + | Some (s', c) -> (match _unify_inner_case l s' with + | Some (s_, c_) -> Some (s_, c@c_) + | None -> None) + | None -> None) + else None) + | [] -> Some (s, []) + | _ -> None + in _unify_inner_case l s + +(** Unify a Case with a lexp + * Case, Var -> constraint (if the variable type and the type of the return value is equivalent, it should be unifiable) + * Case, Case -> try to unify + * Case, _ -> None + *) +and _unify_case (case: lexp) (lxp: lexp) (subst: substitution) : return_type = +(* Maybe Constraint instead ?*) + match case, lxp with + | (Case (_, lxp, lt11, lt12, smap, lxpopt), Case (_, lxp2, lt21, lt22, smap2, lxopt2)) + -> ( match lxpopt, lxopt2 with + | Some l1, Some l2 -> (match _unify_inner ((lxp, lxp2)::(lt11, lt21)::(lt12, lt22)::(l1, l2)::[]) subst with + | Some (s, c) -> _unify_inner_case (List.combine (SMap.bindings smap) (SMap.bindings smap2)) s (* TODO match on result *) + | None -> None) + | _, _ -> None) + | (Case _, Var _) -> Some (subst, [(case, lxp)]) (* ??? *) + | (_, _) -> None + (* Those part of Inductive : * ((arg_kind * vdef * ltype) list) (* formal Args *) @@ -323,7 +364,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 -> Some (s, c) + | None -> None (* Some (s, c) *) | Some (s_,c_) -> Some (s_, c@c_) in match lxp_l with
===================================== tests/unify_test.ml ===================================== --- a/tests/unify_test.ml +++ b/tests/unify_test.ml @@ -1,5 +1,6 @@
open Sexp +open Pexp open Lexp open Unification
@@ -45,6 +46,11 @@ let rec string_of_lxp lxp = | 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 _color = false @@ -68,6 +74,11 @@ let colored_string_of_lxp lxp lcol vcol = ^ " => (" ^ (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") ^ "(...)" | _ -> "???"
let padding_right (str: string ) (dim: int ) (char_: char) : string = @@ -122,6 +133,9 @@ let fmt_title l1 l2 r = string_of_lxp l1 ^ ", " ^ string_of_lxp l2 ^ " -> " ^ st
(* Inputs for the test *) let input_, _ = lexp_decl_str " + sqr = lambda (x : Int) -> x * x; + cube = lambda (x : Int) -> x * (sqr x); + mult = lambda (x : Int) -> lambda (y : Int) -> x * y;
twice = (mult 2); @@ -130,7 +144,7 @@ let input_, _ = lexp_decl_str " let a = (twice x); b = (mult 2 x); in a + b;" default_lctx
-let input = List.map (fun (_, l, _)-> l) (List.flatten input_) +let input = List.flatten (List.map (fun (_, l, l2)-> l::l2::[]) (List.flatten input_))
let man_input = Imm (Integer (Util.dummy_location, 3)) @@ -178,11 +192,47 @@ let tests (input: lexp list) sample_generator formatter : (string list) = in formatter res
let generate_testable (_: lexp list) : ((lexp * lexp * result) list) = - ( Imm (Integer (Util.dummy_location, 3)) , Imm (Integer (Util.dummy_location, 3)) , Equivalent) - ::( Imm (Integer (Util.dummy_location, 4)) , Imm (Integer (Util.dummy_location, 3)) , Nothing ) - ::( 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 ) + ( Imm (Integer (Util.dummy_location, 3)) , + Imm (Integer (Util.dummy_location, 3)) , Equivalent) + + ::( Imm (Integer (Util.dummy_location, 4)) , + Imm (Integer (Util.dummy_location, 3)) , Nothing ) + + ::( 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 ) + + ::( Lambda ((Aexplicit), + (Util.dummy_location, "L1"), + Var((Util.dummy_location, "z"), 3), + Imm (Integer (Util.dummy_location, 3))), + Lambda ((Aexplicit), + (Util.dummy_location, "L2"), + 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 ) ::[]
let check (lxp1: lexp ) (lxp2: lexp ) (res: result) (subst: substitution ): bool = @@ -196,15 +246,13 @@ let test_if (input: lexp list) sample_generator checker : bool = | [] -> true in test_if_ (sample_generator input) checker
-let print_as_json (input: lexp list) = - let str = tests input (generate_couples) (fmt_all) - in let s = "[\n" ^ (List.fold_right (fun e a -> a ^ e ^ ",\n") str "") ^ "]\n" - in print_string s +(*let print_as_json (input: lexp list) =*) + (*let h::t = tests input (generate_couples) (fmt_all)*) + (*in let s = "[\n" ^ (List.fold_right (fun e a -> a ^ e ^ ",\n") t "") ^ h ^ "\n]\n"*) + (*in print_string s*)
(*let () = print_as_json (input@man_input)*)
-(*let () = (fun () -> if test_if [] generate_testable check then () else ()) ()*) - let _ = List.map (fun (l1, l2, r) -> add_test "UNIFICATION" @@ -213,3 +261,5 @@ let _ = List.map (generate_testable [])
let _ = run_all () + +
View it on GitLab: https://gitlab.com/monnier/typer/compare/2c96fe0015c94a11ec0c1344d057a090a91...