BONNEVALLE Vincent pushed to branch unification at Stefan / Typer
Commits: ddece110 by n3f4s at 2016-06-22T18:16:07+02:00 add _unify_susp
- - - - - d92aa7f7 by n3f4s at 2016-06-22T22:54:54+02:00 swtich from _unify_inner_arrow to _unify_inner
_unify_inner is a generalized version of _unify_inner_arrow
- - - - - cabefe09 by n3f4s at 2016-06-23T00:10:43+02:00 add _unify_induction for induction -> induction
- - - - - 92c144b1 by n3f4s at 2016-06-23T18:20:25+02:00 add test for unification
- - - - - 2c96fe00 by n3f4s at 2016-06-23T18:20:59+02:00 add doc _unfiy_induct & refactoring
- - - - -
2 changed files:
- src/unification.ml - + tests/unify_test.ml
Changes:
===================================== src/unification.ml ===================================== --- a/src/unification.ml +++ b/src/unification.ml @@ -7,19 +7,19 @@ 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 expected =*) +(*| Some of 'a*) +(*| Error of Util.location * string (*location * type name*)*) +(*| 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 +(*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 @@ -35,8 +35,8 @@ let associate (meta: int) (lxp: lexp) (subst: substitution) let find_or_none (value: lexp) (map: substitution) : lexp option = match value with | Metavar (idx, _) -> (if VMap.mem idx map - then Some (VMap.find idx map) - else None) + then Some (VMap.find idx map) + else None) | _ -> None
let empty_subst = (VMap.empty) @@ -50,11 +50,12 @@ let empty_subst = (VMap.empty) then ERROR else OK * Builtin , lexp -> UNIFY lexp of Builtin with lexp
- * Let , lexp -> UNIFY right part of Let 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 -> ERROR + * Var , lexp -> CONSTRAINT
* Arrow , Arrow -> if var_kind = var_kind then UNIFY ltype & lexp else ERROR @@ -64,24 +65,21 @@ let empty_subst = (VMap.empty) * lexp , {metavar <-> none} -> UNIFY * lexp , {metavar <-> lexp} -> UNFIFY lexp subst[metavar] * metavar , metavar -> if Metavar = Metavar then OK else ERROR - * metavar , lexp -> ERROR + * metavar , lexp -> OK
* Lamda , Lambda -> if var_kind = var_kind - then unify ltype & lxp else ERROR - * Lambda , Var -> constraints + then UNIFY ltype & lxp else ERROR + * Lambda , Var -> CONSTRAINT * Lambda , lexp -> ERROR - * Call , Imm -> CONSTRAINT - * Call , Cons -> ERROR - * Call , Buitin -> ERROR - * Call , Var -> CONSTRAINT - * Call , Let -> ERROR - * Call , Arrow -> ERROR - * Call , Call -> CONSTRAINT - * Case , lexp -> ERROR + + * Call , lexp -> CONSTRAINT + + * Case , lexp -> ERROR (or CONSTRAINT ?) + * Susp , lexp -> UNIFY (unsusp Susp) lexp + * Inductive , Inductive -> UNIFY + * Inductive , lexp -> ERROR (???)
(*TODO*) - * Inductive , lexp -> - * Susp , lexp -> * lexp , lexp ->
* lexp is equivalent to _ in ocaml @@ -98,19 +96,81 @@ let empty_subst = (VMap.empty)
let rec unify (l: lexp) (r: lexp) (subst: substitution) : return_type = match (l, r) with - | (_, Metavar _) -> _unify_metavar r l subst - | (_, Call _) -> _unify_call r l subst - | (Imm _, _) -> _unify_imm l r subst - | (Cons _, _) -> _unify_cons l r subst - | (Builtin _, _) -> _unify_builtin l r subst - | (Let _, _) -> _unify_let l r subst - | (Var _, _) -> _unify_var l r subst - | (Arrow _, _) -> _unify_arrow l r subst - | (Lambda _, _) -> _unify_lambda l r subst - | (Metavar _, _) -> _unify_metavar l r subst - | (Call _, _) -> _unify_call l r subst - | (Case _, _) -> None - | (_, _) -> None + | (_, Metavar _) -> _unify_metavar r l subst + | (_, Call _) -> _unify_call r l subst + | (Imm _, _) -> _unify_imm l r subst + | (Cons _, _) -> _unify_cons l r subst + | (Builtin _, _) -> _unify_builtin l r subst + | (Let _, _) -> _unify_let l r subst + | (Var _, _) -> _unify_var l r subst + | (Arrow _, _) -> _unify_arrow l r subst + | (Lambda _, _) -> _unify_lambda l r subst + | (Metavar _, _) -> _unify_metavar l r subst + | (Call _, _) -> _unify_call l r subst + | (Susp _, _) -> _unify_susp l r subst + | (Case _, _) -> None (* Maybe Constraint instead ?*) + | (Inductive _, _) -> _unfiy_induct l r subst + | (_, _) -> None + +(* + 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 = + 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 + +(** 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 + | Some (s, c) -> (match (_unify_induct_sub_list t1 t2 s) with + | Some (s1, c1) -> Some (s1, c1@c) + | None -> Some (s, c)) + | None -> (_unify_induct_sub_list t1 t2 subst)) + | _, _ -> None + in test l1 l2 subst + +(** Unify a Inductive and a lexp + * Inductive, Inductive -> try t unify + * Inductive, _ -> None*) +and _unfiy_induct (induct: lexp) (lxp: lexp) (subst: substitution) : return_type = + 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 + | None -> None + | Some (s, c) -> _unify_induct_sub_list (SMap.bindings m1) (SMap.bindings m2) s) + | (_, _) -> None + +and _unify_susp (susp_: lexp) (lxp: lexp) (subst: substitution) : return_type = + match susp_ with + | Susp _ -> unify (unsusp_all susp_) lxp subst + | _ -> None
and _unify_cons (cons: lexp) (lxp: lexp) (subst: substitution) : return_type = (* symbol = (location * string)*) @@ -118,14 +178,14 @@ and _unify_cons (cons: lexp) (lxp: lexp) (subst: substitution) : return_type = (*FIXME which parameter of Cons is it's name ?*) | (Cons ((_, idx), (_, name)), Cons ((_, idx2), (_, name2))) when name = name2 -> - if idx = idx2 then Some (subst, []) (*TODO shift indexes ?*) - else None + if idx = idx2 then Some (subst, []) (*TODO shift indexes ?*) + else None | (_, _) -> None
and _unify_call (call: lexp) (lxp: lexp) (subst: substitution) : return_type = let combine list1 list2 = - let l1 = List.fold_left (fun acc (_, x) -> x::acc) [] list1 - and l2 = List.fold_left (fun acc (_, x) -> x::acc) [] list2 + let l1 = List.fold_right (fun (_, x) acc -> x::acc) list1 [] + and l2 = List.fold_right (fun (_, x) acc -> x::acc) list2 [] in List.combine l1 l2 in match (call, lxp) with | (Call (lxp1, lxp_list1), Call (lxp2, lxp_list2)) -> @@ -140,7 +200,8 @@ and _unify_lambda (lambda: lexp) (lxp: lexp) (subst: substitution) : return_type match (lambda, lxp) with | (Lambda (var_kind1, _, ltype1, lexp1), Lambda (var_kind2, _, ltype2, lexp2)) -> if var_kind1 = var_kind2 - then _unify_inner_arrow ltype1 lexp1 ltype2 lexp2 subst + then _unify_inner ((ltype1, ltype2)::(lexp1, lexp2)::[]) subst + (*then _unify_inner_arrow ltype1 lexp1 ltype2 lexp2 subst*) else None | (Lambda _, Var _) -> Some ((subst, [(lambda, lxp)])) | (Lambda _, Let _) -> Some ((subst, [(lambda, lxp)])) @@ -175,7 +236,8 @@ and _unify_arrow (arrow: lexp) (lxp: lexp) (subst: substitution) match (arrow, lxp) with | (Arrow (var_kind1, _, ltype1, _, lexp1), Arrow (var_kind2, _, ltype2, _, lexp2)) -> if var_kind1 = var_kind2 - then _unify_inner_arrow ltype1 lexp1 ltype2 lexp2 subst + then _unify_inner ((ltype1, ltype2)::(lexp1, lexp2)::[]) subst + (* _unify_inner_arrow ltype1 lexp1 ltype2 lexp2 subst *) else None | (Arrow _, Imm _) -> None | (Arrow _, Var _) -> Some (subst, [(arrow, lxp)]) (* FIXME Var can contain type ???*) @@ -237,7 +299,8 @@ and _unify_builtin (bltin: lexp) (lxp: lexp) (subst: substitution) : return_type | (_, _) -> None
(** Unify a Let (let_) and a lexp (lxp), if possible - * Unify the left lexp part of the Let (Let (_, _, lxp)) with the lexp + * Let , Let -> check the 'inside' of the let + * Let , lexp -> constraint *) and _unify_let (let_: lexp) (lxp: lexp) (subst: substitution) : return_type = match (let_, lxp) with @@ -252,8 +315,8 @@ and _unify_let (let_: lexp) (lxp: lexp) (subst: substitution) : return_type = [(ltype * ltype), (lexp * lexp), (ltype2 * ltype2), (lexp2 * lexp2), ...] *) and combine list1 list2 = - let l1 = List.fold_left (fun acc (_, t, x) -> t::x::acc) [] list1 - and l2 = List.fold_left (fun acc (_, t, x) -> t::x::acc) [] list2 + let l1 = List.fold_right (fun (_, t, x) acc -> t::x::acc) list1 [] + and l2 = List.fold_right (fun (_, t, x) acc -> t::x::acc) list2 [] in List.combine l1 l2
and _unify_inner (lxp_l: (lexp * lexp) list) (subst: substitution) : return_type =
===================================== tests/unify_test.ml ===================================== --- /dev/null +++ b/tests/unify_test.ml @@ -0,0 +1,215 @@ + +open Sexp +open Lexp +open Unification + +open Lparse (* add_def *) + +open Utest_lib + +open Fmt + +open Builtin +open Env + +open Str + +open Debug + +type result = + | Constraint + | Unification + | Equivalent + | Nothing + +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 + | 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(...)" + | _ -> "???" + +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(...)" ) + | _ -> "???" + +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" + | Unification -> "Unification" + | 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 " + 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.map (fun (_, l, _)-> l) (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 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 + +(* Testing the inputs *) + +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 + +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 ) + ::[] + +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 + +let test_if (input: lexp list) sample_generator checker : bool = + let rec test_if_ samples checker = + match samples with + | (l1, l2, res)::t -> if checker l1 l2 res empty_subst then test_if_ t checker else false + | [] -> 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@man_input)*) + +(*let () = (fun () -> if test_if [] generate_testable check then () else ()) ()*) + +let _ = List.map + (fun (l1, l2, r) -> + add_test "UNIFICATION" + (fmt_title l1 l2 r) + (fun () -> if test_if [] (fun _ -> [(l1, l2, r)]) check then success () else failure ())) + (generate_testable []) + +let _ = run_all ()
View it on GitLab: https://gitlab.com/monnier/typer/compare/4943fc4f9f4324e77980e41f2d9857ecfa7...