[Typer] [Git][monnier/typer][unification] 4 commits: move doc, error management with List.combine

BONNEVALLE Vincent pushed to branch unification at Stefan / Typer

Commits: 3950fd86 by n3f4s at 2016-06-28T20:48:58+02:00 move doc, error management with List.combine

switch from List.combine to zip to handle case where the two list have different size

- - - - - ee113a9e by n3f4s at 2016-06-28T21:43:38+02:00 add test case

- - - - - ddfe6931 by n3f4s at 2016-06-28T22:39:03+02:00 debug recursion on wrong variable

- - - - - 46aab474 by n3f4s at 2016-06-29T20:51:49+02:00 remove useless code & add test from typer code

add lexp generation from typer code in unification test add better printing system for unification test

- - - - -

2 changed files:

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

Changes:

===================================== src/unification.ml ===================================== --- a/src/unification.ml +++ b/src/unification.ml @@ -41,49 +41,28 @@ let find_or_none (value: lexp) (map: substitution) : lexp option =

let empty_subst = (VMap.empty)

-(** - * Imm , Imm -> if Imm =/= Imm then ERROR else OK - - * Cons , Cons -> ERROR - - * Builtin , Builtin -> if Builtin =/= Buitin - then ERROR else OK - * Builtin , lexp -> UNIFY lexp of Builtin with lexp - - * Let , Let -> UNIFY inside of Let - * Let , lexp -> CONSTRAINT - - * Var , Var -> if db_index ~= db_index UNIFY else ERROR - * Var , MetaVar -> UNIFY Metavar - * Var , lexp -> CONSTRAINT - - * Arrow , Arrow -> if var_kind = var_kind - then UNIFY ltype & lexp else ERROR - * Arrow , Imm -> ERROR - * Arrow , Var -> CONSTRAINT - - * lexp , {metavar <-> none} -> UNIFY - * lexp , {metavar <-> lexp} -> UNFIFY lexp subst[metavar] - * metavar , metavar -> if Metavar = Metavar then OK else ERROR - * metavar , lexp -> OK - - * Lamda , Lambda -> if var_kind = var_kind - then UNIFY ltype & lxp else ERROR - * Lambda , Var -> CONSTRAINT - * Lambda , lexp -> ERROR - - * Call , lexp -> CONSTRAINT - - * Case , lexp -> ERROR (or CONSTRAINT ?) - * Susp , lexp -> UNIFY (unsusp Susp) lexp - * Inductive , Inductive -> UNIFY - * Inductive , lexp -> ERROR (???) - - (*TODO*) - * Sort , lexp -> - * SortLevel , lexp -> - * lexp , lexp -> +(* Zip while applying a function, returns empty list if l1 & l2 have different size*) +let zip_map (l1: 'a list ) (l2: 'b list ) (f: ('a -> 'b -> 'c)): 'c list= + let rec zip_ ll1 ll2 f = + match ll1, ll2 with + | (h1::t1, h2::t2) -> (match zip_ t1 t2 f with + | None -> None + | Some t -> Some ((f h1 h2)::t)) + | ([], []) -> Some [] + | ([], _) -> None + | (_, []) -> None + in match zip_ l1 l2 f with + | None -> [] + | Some l -> l + +let zip (l1: 'a list) (l2: 'b list): (('a * 'b) list) = zip_map l1 l2 (fun x z -> (x, z)) + +let zip_fold list1 list2 f = + let l1 = List.fold_right (f) list1 [] + and l2 = List.fold_right (f) list2 [] + in zip l1 l2

+(** * lexp is equivalent to _ in ocaml * (Let , lexp) == (lexp , Let) * UNIFY -> recursive call or dispatching @@ -119,7 +98,7 @@ 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 -(*| (_, _) -> None*) +(* | (_, _) -> None*)

(********************************* Type specific unify *******************************)

@@ -143,6 +122,10 @@ and _unify_imm (l: lexp) (r: lexp) (subst: substitution) : return_type = | (Imm _, _) -> unify r l subst | (_, _) -> None

+(** Unify a Cons and a lexp + * Cons, Cons -> if Cons ~= Cons then OK else ERROR + * Cons, _ -> ERROR +*) and _unify_cons (cons: lexp) (lxp: lexp) (subst: substitution) : return_type = (* symbol = (location * string)*) match (cons, lxp) with @@ -170,21 +153,20 @@ 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 = - let combine list1 list2 f = - let l1 = List.fold_right (f) list1 [] - and l2 = List.fold_right (f) list2 [] - in List.combine l1 l2 - in match (let_, lxp) with + match (let_, lxp) with | (Let (_, m, lxp_), Let (_, m1, lxp2)) -> let f = (fun (_, t, x) acc -> t::x::acc) - in _unify_inner ((lxp_, lxp2)::(combine m m1 f)) subst + in let tail = zip_fold m m1 f + in (match tail with + | [] -> None + | _ -> _unify_inner ((lxp_, lxp2)::(tail)) subst ) | (Let _, _) -> Some (subst, [(let_, lxp)]) | _, _ -> None

(** Unify a Var and a lexp, if possible * (Var, Var) -> unify if they have the same debruijn index FIXME : shift indexes * (Var, Metavar) -> unify_metavar Metavar var subst - * (_, _) -> None + * (Var _, _) -> unfiy lexp Var subst *) and _unify_var (var: lexp) (r: lexp) (subst: substitution) : return_type = match (var, r) with @@ -199,6 +181,7 @@ and _unify_var (var: lexp) (r: lexp) (subst: substitution) : return_type = * (Arrow, Arrow) -> if var_kind = var_kind then unify ltype & lexp (Arrow (var_kind, _, ltype, lexp)) else None + * (Arrow, Var) -> Constraint * (_, _) -> None *) and _unify_arrow (arrow: lexp) (lxp: lexp) (subst: substitution) @@ -216,7 +199,12 @@ and _unify_arrow (arrow: lexp) (lxp: lexp) (subst: substitution) | (_, _) -> None

(** Unify a Lambda and a lexp if possible - * See above for result + * Lamda , Lambda -> if var_kind = var_kind + then UNIFY ltype & lxp else ERROR + * Lambda , Var -> CONSTRAINT + * Lambda , Call -> Constraint + * Lambda , Let -> Constraint + * Lambda , lexp -> unify lexp lambda subst *) and _unify_lambda (lambda: lexp) (lxp: lexp) (subst: substitution) : return_type = match (lambda, lxp) with @@ -234,8 +222,10 @@ and _unify_lambda (lambda: lexp) (lxp: lexp) (subst: substitution) : return_type | (_, _) -> None

(** Unify a Metavar and a lexp if possible - * See above for result - * Metavar is the 'end' of the rules i.e. : it can call unify with his argument (re-ordered) + * lexp , {metavar <-> none} -> UNIFY + * lexp , {metavar <-> lexp} -> UNFIFY lexp subst[metavar] + * metavar , metavar -> if Metavar = Metavar then OK else ERROR + * metavar , lexp -> OK *) and _unify_metavar (meta: lexp) (lxp: lexp) (subst: substitution) : return_type = match (meta, lxp) with @@ -247,18 +237,23 @@ and _unify_metavar (meta: lexp) (lxp: lexp) (subst: substitution) : return_type | Some (lxp_) -> unify lxp_ lxp subst) | (_, _) -> None

+(** Unify a Call (call) and a lexp (lxp) + * Call , Call -> UNIFY + * Call , lexp -> CONSTRAINT +*) and _unify_call (call: lexp) (lxp: lexp) (subst: substitution) : return_type = - let combine list1 list2 f = - let l1 = List.fold_right (f) list1 [] - and l2 = List.fold_right (f) list2 [] - in List.combine l1 l2 - in match (call, lxp) with + match (call, lxp) with | (Call (lxp1, lxp_list1), Call (lxp2, lxp_list2)) -> let f = (fun (_, x) acc -> x::acc) - in _unify_inner ((lxp1, lxp2)::(combine lxp_list1 lxp_list2 f)) subst + in let tail = zip_fold lxp_list1 lxp_list2 f + in (match tail with + | [] -> None + | _ -> _unify_inner ((lxp1, lxp2)::(tail)) subst) | (Call _, _) -> Some ((subst, [(call, lxp)])) | (_, _) -> None

+(** Apply unsusp to the Susp and unify the result with the lexp +*) and _unify_susp (susp_: lexp) (lxp: lexp) (subst: substitution) : return_type = match susp_ with | Susp _ -> unify (unsusp_all susp_) lxp subst @@ -273,7 +268,7 @@ and _unify_case (case: lexp) (lxp: lexp) (subst: substitution) : return_type = | (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) -> (match _unify_inner_case (List.combine (SMap.bindings smap) (SMap.bindings smap2)) s with + | Some (s, c) -> (match _unify_inner_case (zip (SMap.bindings smap) (SMap.bindings smap2)) s with | Some (s', c') -> Some (s', c@c') | None -> None) | None -> None) @@ -285,11 +280,13 @@ and _unify_case (case: lexp) (lxp: lexp) (subst: substitution) : return_type = * Inductive, Inductive -> try unify * Inductive, Var -> constraint * Inductive, Call/Metavar/Case/Let -> constraint - * Inductive, _ -> None*) + * Inductive, _ -> None + *) and _unfiy_induct (induct: lexp) (lxp: lexp) (subst: substitution) : return_type = - match (induct, lxp) with + let transform (a, b, c) (d, e, f) = ((a, Some b, c), (d, Some e, f)) + in match (induct, lxp) with | (Inductive (_, lbl1, farg1, m1), Inductive (_, lbl2, farg2, m2)) when lbl1 = lbl2 -> - (match _unify_inner_induct_1 (List.combine farg1 farg2) subst with + (match _unify_inner_induct (zip_map farg1 farg2 transform) subst with | None -> None | Some (s, c) -> (match (_unify_induct_sub_list (SMap.bindings m1) (SMap.bindings m2) s) with | Some (s', c') -> Some (s', c@c') @@ -297,6 +294,10 @@ and _unfiy_induct (induct: lexp) (lxp: lexp) (subst: substitution) : return_type | (Inductive _, Var _) -> Some (subst, [(induct, lxp)]) | (_, _) -> None

+(** Unify a SortLevel with a lexp + * SortLevel, SortLevel -> if SortLevel ~= SortLevel then OK else ERROR + * SortLevel, _ -> ERROR +*) and _unify_sortlvl (sortlvl: lexp) (lxp: lexp) (subst: substitution) : return_type = match sortlvl, lxp with | (SortLevel s, SortLevel s2) -> (match s, s2 with @@ -305,6 +306,11 @@ and _unify_sortlvl (sortlvl: lexp) (lxp: lexp) (subst: substitution) : return_ty | _, _ -> None) | _, _ -> None

+(** Unify a Sort and a lexp + * Sort, Sort -> if Sort ~= Sort then OK else ERROR + * Sort, Var -> Constraint + * Sort, lexp -> ERROR +*) and _unify_sort (sort_: lexp) (lxp: lexp) (subst: substitution) : return_type = match sort_, lxp with | (Sort (_, srt), Sort (_, srt2)) -> (match srt, srt2 with @@ -312,8 +318,8 @@ and _unify_sort (sort_: lexp) (lxp: lexp) (subst: substitution) : return_type = | StypeOmega, StypeOmega -> Some (subst, []) | StypeLevel, StypeLevel -> Some (subst, []) | _, _ -> None) - | Sort _, Var _ -> Some (subst, [(sort_, lxp)]) - | _, _ -> None + | Sort _, Var _ -> Some (subst, [(sort_, lxp)]) + | _, _ -> None

(************************ Helper function **************************************)

@@ -327,43 +333,25 @@ and is_same arglist arglist2 =

(** 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 -> + let rec _unify_inner_case list_ s = + 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 - | Some (s', c) -> (match _unify_inner_case l s' with + | Some (s', c) -> (match _unify_inner_case tail s' with | Some (s_, c_) -> Some (s_, c@c_) | None -> None) | None -> None) else None) | [] -> Some (s, []) | _ -> None - in _unify_inner_case l s + in (match l with + | [] -> None + | _ -> _unify_inner_case l s)

(***** for Inductive *****) -(* - Those part of Inductive : - * ((arg_kind * vdef * ltype) list) (* formal Args *) - * ((arg_kind * vdef option * ltype) list) - are almost identical except for the 'vdef option' (which is ignored) so the same function (_unify_inner_induct) should - work for those part, but it don't work because of 'vdef option' -*) -(** for _unfiy_induct_sub_list*) -and _unify_inner_induct_2 lst subst : return_type = - let test ((a1, _, l1), (a2, _, l2)) 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 - | Some (s1, c1) -> Some (s1, c1@c) - | None -> Some (s, c)) - | None -> test e subst) - ) None lst - (** for _unify_induct : unify the formal arg*) -and _unify_inner_induct_1 lst subst : return_type = +and _unify_inner_induct lst subst : return_type = let test ((a1, _, l1), (a2, _, l2)) subst : return_type = if a1 = a2 then unify l1 l2 subst else None @@ -378,7 +366,7 @@ and _unify_inner_induct_1 lst subst : return_type = (** unify the SMap of list in Inductive *) and _unify_induct_sub_list l1 l2 subst = let test l1 l2 subst = match l1, l2 with - | (k1, v1)::t1, (k2, v2)::t2 when k1 = k2 -> (match _unify_inner_induct_2 (List.combine v1 v2) subst with + | (k1, v1)::t1, (k2, v2)::t2 when k1 = k2 -> (match _unify_inner_induct (zip v1 v2) subst with | Some (s, c) -> (match (_unify_induct_sub_list t1 t2 s) with | Some (s1, c1) -> Some (s1, c1@c) | None -> Some (s, c)) @@ -405,5 +393,3 @@ 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 @@ -27,11 +27,6 @@ type unif_res = (result * (substitution * constraints) option * lexp * lexp)

type triplet = string * string * string

-let _debug = false - -let do_debug func = - if _debug then (func ()) else () - (* String & lexp formatting *) let rec string_of_lxp lxp = match lxp with @@ -53,75 +48,6 @@ let rec string_of_lxp lxp = | Susp _ -> "Susp(...)" | _ -> "???"

-let _color = false -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 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") ^ "(...)" - | _ -> "???" - -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_) - -let get_max_dim (str_list : triplet list ) : (int * int * int) = - let max_ i s = max i (String.length s) - in (List.fold_left - (fun (al,ac,ar) (el, ec, er) -> ((max_ al el), (max_ ac ec), (max_ ar er))) - (0, 0, 0) str_list) - -let fmt_unification_result (l: unif_res): string = - match l with - | (Constraint, _, lxp1, lxp2) -> - "{ "result" : " ^ (str_yellow ""Constraint"") ^ ", "lexp_left" : "" ^ (str_yellow (string_of_lxp lxp1)) ^ "", "lexp_right" : "" ^ (str_yellow (string_of_lxp lxp2)) ^ ""}" - | (Unification, _, lxp1, lxp2) -> - "{ "result" : " ^ (str_yellow ""Unification"") ^ ", "lexp_left" : "" ^ (str_yellow (string_of_lxp lxp1)) ^ "", "lexp_right" : "" ^ (str_yellow (string_of_lxp lxp2)) ^ ""}" - | (Equivalent, _, lxp1, lxp2) -> - "{ "result" : " ^ (str_yellow ""Equivalent"") ^ ", "lexp_left" : "" ^ (str_yellow (string_of_lxp lxp1)) ^ "", "lexp_right" : "" ^ (str_yellow (string_of_lxp lxp2)) ^ ""}" - | (Nothing, _, lxp1, lxp2) -> - "{ "result" : " ^ (str_yellow ""Nothing"") ^ ", "lexp_left" : "" ^ (str_yellow (string_of_lxp lxp1)) ^ "", "lexp_right" : "" ^ (str_yellow (string_of_lxp lxp2)) ^ ""}" - -let fmt_all (r: unif_res list) = - List.map fmt_unification_result r - -let fmt_unification_of lxp1 lxp2 = - "Unifying " ^ (colored_string_of_lxp lxp1 str_yellow str_cyan) - ^ " -> " - ^ (colored_string_of_lxp lxp2 str_yellow str_cyan) - ^ "\n" - let string_of_result r = match r with | Constraint -> "Constraint" @@ -129,77 +55,68 @@ let string_of_result r = | Equivalent -> "Equivalent" | Nothing -> "Nothing"

-let fmt_title l1 l2 r = string_of_lxp l1 ^ ", " ^ string_of_lxp l2 ^ " -> " ^ string_of_result r - -(* 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); - - let_fun = lambda (x : Int) -> - let a = (twice x); b = (mult 2 x); in - a + b;" default_lctx - -let input = List.flatten (List.map (fun (_, l, l2)-> l::l2::[]) (List.flatten input_)) - -let man_input = - Imm (Integer (Util.dummy_location, 3)) - ::Imm (Integer (Util.dummy_location, 4)) - ::Builtin ((Util.dummy_location, "Int=3"), Imm (Integer (Util.dummy_location, 3))) - ::Var ((Util.dummy_location, "x"), 3) - ::Var ((Util.dummy_location, "y"), 4) - ::Metavar (0, (Util.dummy_location, "M")) - ::[] - - -(* Test sample generation *) -let rec range (begin_: int) (end_: int) : (int list) = - if begin_ >= end_ - then [] - else begin_::(range (begin_+1) end_) - -let generate_combination (r: int list) (input: lexp list) : ((lexp * lexp) list) = - let begin_ = List.hd r - in List.map (fun idx -> ((List.nth input begin_ ), (List.nth input idx)) ) r - -let generate_couples (input: lexp list) : ((lexp * lexp) list) = - let length = List.length input - in List.fold_left (fun acc elt -> (generate_combination (range elt length) input)@acc) [] (range 0 length) - -(* Testing the sample *) +let max_dim (lst: (string * string * string * string) list): (int * int * int *int) = + let max i l = max i (String.length l) + in List.fold_left + (fun (la, ca1, ca2, ra) (l, c1, c2, r) -> ((max la l), (max ca1 c1), (max ca2 c2), (max ra r))) + (0, 0, 0, 0) + lst

-let test_input (lxp1: lexp) (lxp2: lexp) (subst: substitution): unif_res = - do_debug (fun () -> print_string (fmt_unification_of lxp1 lxp2)); - let res = unify lxp1 lxp2 subst in - 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) - -let test_samples (samples: (lexp * lexp) list) (subst: substitution): (unif_res list) = - List.map (fun (l1, l2) -> test_input l1 l2 subst) samples +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_)

-(* Testing the inputs *) +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))) + 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 :" + ^ (padding_right r2 r ' ') + ^ " expected : " + ^ (padding_right r1 c2 ' ') + ) str_lst

-let tests (input: lexp list) sample_generator formatter : (string list) = - let samples = sample_generator input - in let res = test_samples samples empty_subst - in formatter res +(* Inputs for the test *) +let str_induct = "Nat = inductive_ (dNat) (zero) (succ Nat)" +let str_int_3 = "i = 3" +let str_int_4 = "i = 4" +let str_case = "i = case 0 +| 1 => 2 +| 0 => 42 +| _ => 5" +let str_case2 = "i = case 0 +| 0 => 12 +| 1 => 12 +| _ => 12" + +let generate_ltype_from_str str = + List.hd ((fun (lst, _) -> + (List.map + (fun (_, _, ltype) -> ltype)) + (List.flatten lst)) + (lexp_decl_str str default_lctx)) + +let generate_lexp_from_str str = + List.hd ((fun (lst, _) -> + (List.map + (fun (_, lxp, _) -> lxp)) + (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 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) + ( 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 ) @@ -233,8 +150,33 @@ let generate_testable (_: lexp list) : ((lexp * lexp * result) list) = (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) + + ::(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));*) + let res = unify lxp1 lxp2 subst in + 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) + let check (lxp1: lexp ) (lxp2: lexp ) (res: result) (subst: substitution ): bool = let r, _, _, _ = test_input lxp1 lxp2 subst in if r = res then true else false @@ -246,19 +188,18 @@ 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 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 unifications = List.map + (fun (l1, l2, res) -> + let r, _, _, _ = test_input l1 l2 empty_subst + in (l1, l2, res, r)) + (generate_testable [])

let _ = List.map - (fun (l1, l2, r) -> + (fun (str, (l1, l2, expected, res)) -> add_test "UNIFICATION" - (fmt_title l1 l2 r) - (fun () -> if test_if [] (fun _ -> [(l1, l2, r)]) check then success () else failure ())) - (generate_testable []) + (str) + (fun () -> if expected = res then success () else failure ())) + (List.combine (fmt unifications) unifications )

let _ = run_all ()

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