Juillet 2016 - Typer - mailman.iro.umontreal.ca

[Git][monnier/typer][unification] 13 commits: fix non termination of test
by BONNEVALLE Vincent 29 Jul '16

29 Jul '16

BONNEVALLE Vincent pushed to branch unification at Stefan / Typer Commits: 79f26644 by n3f4s at 2016-07-28T23:28:58+02:00 fix non termination of test - - - - - 2a02a1fb by n3f4s at 2016-07-28T23:48:06+02:00 add metavar in lexp_p_infer for default case - - - - - ec33b98a by n3f4s at 2016-07-28T23:49:49+02:00 remove padding for random test - - - - - 3b5313eb by n3f4s at 2016-07-28T23:50:48+02:00 add test for type checking - - - - - 42608955 by n3f4s at 2016-07-29T18:22:00+02:00 debug inversion for Id ↑^X - - - - - 05af83ee by n3f4s at 2016-07-29T20:44:49+02:00 begining of adding unification in type check - - - - - 5d99315b by n3f4s at 2016-07-29T21:16:28+02:00 try to remove iteration - - - - - a0b5b8d0 by n3f4s at 2016-07-29T21:23:55+02:00 fix transformation : change shift value in transfo merge toIr, flattenIr and to_list in transfo - - - - - 7798134b by n3f4s at 2016-07-29T21:47:14+02:00 add check for deBruijn indices >= shift offset - - - - - 5acc8450 by n3f4s at 2016-07-29T21:48:22+02:00 remove useless code - - - - - 946063a6 by n3f4s at 2016-07-29T21:48:36+02:00 adapt tests - - - - - 8b249028 by n3f4s at 2016-07-29T23:18:37+02:00 merge fill with to_cons - - - - - 304245b6 by n3f4s at 2016-07-29T23:20:23+02:00 remove useless code - - - - - 5 changed files: - src/inverse_subst.ml - src/lparse.ml - src/unification.ml - tests/inverse_test.ml - + tests/lparse_test.ml Changes: ===================================== src/inverse_subst.ml ===================================== --- a/src/inverse_subst.ml +++ b/src/inverse_subst.ml @@ -12,74 +12,28 @@ type inter_subst = lexp list (* Intermediate between "tree"-like substitution an let dummy_var = Var((dummy_location, "DummyVar"), -1) -(** Transform a subst into a more linear 'intermediate representation': - - - a₁ · ↑n₁ (a₂ · ↑n₂ (a₃ · ↑n₃ id)) - ⇒ a₁' · a₂' · a₃' · ↑n₃ id - - or in ocaml-ish representation : - - - S.Cons(var, S.Shift(..., offset)) - ⇒ S.Cons(var, S.Shift(S.Identity, offset))::...::Identity -*) -let toIr (s: lexp S.subst) : inter_subst = - let rec toIr s total_offset = - match s with - | S.Shift (s_1, offset) -> toIr s_1 (total_offset + offset) - (* FIXME: A Cons with something else than a Var is not an error. - * It might mean that we can't invert this substitution, but that's - * no justification for "assert false". *) - | S.Cons(Var _ as v, s_1) - (* FIXME: Why not L.mkSusp? *) - -> Susp (v, S.shift total_offset)::(toIr s_1 total_offset) - | S.Identity -> [Susp (dummy_var, S.shift total_offset)] - | _ -> assert false - in toIr s 0 - -(** Transform an 'intermediate representation' into a sequence of cons followed by a shift - - - a1.(↑^\{x1\}a2).(↑^\{x2\}a3).↑^\{x3\}id -> a1.a2.a3.(id ↑^\{x1+x2+x3\}) - - or in ocaml-ish representation : - - - <code>S.Cons(var, S.Shift(S.Identity, offset))::...::Identity -> S.Cons(var, S.Cons(...S.Shift(S.Identity, x1+x2+x3...)))</code> -*) -let flattenIr (s: inter_subst): lexp S.subst option = - let rec flattenCons s = - match s with - | Susp (_dummy_var, s)::[] -> Some s - | susp::tail -> (match flattenCons tail with - | Some (s1) -> Some (S.cons (nosusp susp) s1) - | None -> None) - | _ -> None - in flattenCons s - -(** Flatten a "tree"-like substitution: - - - a1.↑^\{x1\}(a2.↑^\{x2\}(a3.↑^\{x3\}id)) -> a1.(↑^\{x1\}a2).(↑^\{x2\}a3).↑^\{x3\}id -> a1.a2.a3 ↑^\{x1+x2+x3\} - - or in ocaml-ish representation : - - - <code>S.Cons(var, S.Shift(S.Identity, offset))::...::Identity -> S.Cons(var, S.Cons(...S.Shift(S.Identity, x1+x2+x3...)))</code> -*) -let flatten (s: lexp S.subst): lexp S.subst option = - let rec check (sf: lexp S.subst): int option = - match sf with - | S.Identity -> Some 0 - | S.Shift(sf, o) -> (match check sf with - | None -> None - | Some o2 -> Some (o + o2)) - | S.Cons (Var(_, idx), sf) -> (match check sf with - | None -> None - | Some o -> if idx >= o then None else Some o) - | _ -> assert false - in - match flattenIr (toIr s) with - | None -> None - | Some (sf2) as sf -> match check sf2 with - | Some _ -> sf - | None -> None - +type substIR = ((int * int) list * int) + +(* toIr + flattenIr + to_list *) +(* TODO : find better name ?*) +let transfo (s: lexp S.subst) : substIR option = + let rec transfo (s: lexp S.subst) (off_acc: int) (idx: int): substIR option = + let valueOf (v: lexp): int = + match v with + | Var (_, v) -> v + | _ -> assert false + in let shiftVar (var: lexp) (offset: int): int = valueOf (mkSusp var (S.shift offset)) + in match s with + | S.Cons (Var _ as v, s) -> + (match transfo s off_acc (idx + 1) with + | Some (tail, off) -> let newVar = shiftVar v off_acc + in if newVar >= off then None + else Some (((shiftVar v off_acc), idx)::tail, off) + | None -> None) + | S.Shift (s, offset) -> transfo s (offset + off_acc) idx + | S.Identity -> Some ([], off_acc) + | _ -> None + in transfo s 0 0 (* Inverse *) @@ -87,16 +41,6 @@ let flatten (s: lexp S.subst): lexp S.subst option = *) let rec sizeOf (s: (int * int) list): int = List.length s -(** Returns the db_index of the "inside" of a Var -*) -let idxOf (_, idx) = idx - -(** Returns a list of couple (X, idx) where X go from beg_ to end_*) -let rec genDummyVar (beg_: int) (end_: int) (idx: int): (int * int) list = - if beg_ < end_ - then (beg_, idx)::(genDummyVar (beg_ + 1) end_ idx) - else [] - (** Returns a dummy variable with the db_index idx *) let mkVar (idx: int): lexp = Var((U.dummy_location, ""), idx) @@ -110,67 +54,51 @@ let mkVar (idx: int): lexp = Var((U.dummy_location, ""), idx) @param size size of the list to return @param acc recursion accumulator *) -let fill (l: (int * int) list) (size: int) (acc: (int * int) list): (int * int) list option = - let genDummyVar beg_ end_ = genDummyVar beg_ end_ (size + 1) +let fill (l: (int * int) list) (nbVar: int) (shift: int): lexp S.subst option = + let rec genDummyVar (beg_: int) (end_: int) (l: lexp S.subst): lexp S.subst = + if beg_ < end_ + then S.cons (mkVar (nbVar + 1)) (genDummyVar (beg_ + 1) end_ l) + else l in - let rec fill_before (l: (int * int) list): (int * int) list = + let fill_before (l: (int * int) list) (s: lexp S.subst) (nbVar: int): lexp S.subst option = match l with - | [] -> [] - | (idx, val_)::tail -> (if idx > 0 then (genDummyVar 0 idx)@l - else l) - and fill_after (l: (int * int) list) (size: int) (acc: (int * int) list): (int * int) list option = + | [] -> Some (genDummyVar 0 nbVar S.identity) + | (i1, v1)::_ when i1 > 0 -> Some (genDummyVar 0 i1 s) + | _ -> Some s + in let rec fill_after (l: (int * int) list) (nbVar: int) (shift: int): lexp S.subst option = match l with - | (idx1, val1)::(idx2, val2)::tail when (idx1 = idx2) -> None - | (idx1, val1)::(idx2, val2)::tail -> - let tail = (idx2, val2)::tail in - let accu = if (idx2 - idx1) > 1 - then (acc@[(idx1, val1)]@(genDummyVar (idx1 + 1) idx2)) - else (acc@(idx1, val1)::[]) - in fill_after tail size accu - | (idx1, val1)::[] -> if (idx1 + 1) < size - then Some (acc@((idx1, val1)::(genDummyVar (idx1 + 1) size))) - else Some (acc@[(idx1, val1)]) - | [] -> Some acc - in fill_after (fill_before l) size acc - -(** Transform a L-exp to a list of (e_i, i) where e_i is the position of the debuijn index i - in the debuijn index sequence -*) -let to_list (s: lexp S.subst) : (((int * int) list) * int) = - let rec as_list (s: lexp S.subst) (i: int) : (((int * int) list) * int) = - match s with - | S.Cons (Var(v), s1) -> let tail, o = as_list s1 (i + 1) in ((((idxOf v), i)::tail ), o) - | S.Shift (S.Identity, shift) -> ([], shift) - | S.Identity -> ([], 0) - | _ -> assert false; - in as_list s 0 - -(** Transform a (e_i, i) list to a substitution by transforming the list into Cons and - adding a Shift. - - @param lst list of couple (ei_, i) to transform - @param shift value of the shift -*) -let rec to_cons (lst: (int * int) list) (shift: int) : lexp S.subst option = - match lst with - | (_, i)::tail -> (match (to_cons tail shift) with - | Some s -> Some (S.cons (mkVar i) s) - | None -> None) - | [] -> Some (S.shift shift) + | (idx1, val1)::(idx2, val2)::tail when (idx1 = idx2) -> None + + | (idx1, val1)::(idx2, val2)::tail when (idx2 - idx1) > 1 -> + (match fill_after ((idx2, val2)::tail) nbVar shift with + | None -> None + | Some s -> Some (S.cons (mkVar val1) (genDummyVar (idx1 + 1) idx2 s))) + + | (idx1, val1)::(idx2, val2)::tail -> + (match fill_after ((idx2, val2)::tail) nbVar shift with + | None -> None + | Some s -> Some (S.cons (mkVar val1) s)) + + | (idx1, val1)::[] when (idx1 + 1) < nbVar -> + Some (S.cons (mkVar val1) (genDummyVar (idx1 + 1) nbVar (S.shift shift))) + + | (idx1, val1)::[] -> + Some (S.cons (mkVar val1) (S.shift shift)) + + | [] -> + Some (S.shift shift) + in match fill_after l nbVar shift with + | None -> None + | Some s -> fill_before l s nbVar (** Compute the inverse, if there is one, of the substitution. <code>s:S.subst, l:lexp, s':S.subst</code> where <code>l[s][s'] = l</code> and <code> inverse s = s' </code> *) -let rec inverse (subst: lexp S.subst ) : lexp S.subst option = +let inverse (s: lexp S.subst) : lexp S.subst option = let sort = List.sort (fun (ei1, _) (ei2, _) -> compare ei1 ei2) - in - match flatten subst with - | None -> None - | Some (s) -> - let cons_lst, shift_val = to_list s - in let size = sizeOf cons_lst - in match fill (sort cons_lst) shift_val [] with - | None -> None - | Some cons_lst -> to_cons cons_lst size - + in match transfo s with + | None -> None + | Some (cons_lst, shift_val) -> + let size = sizeOf cons_lst + in fill (sort cons_lst) shift_val size ===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -48,6 +48,8 @@ open Eval open Grammar open Builtin +module Unif = Unification + module TC = Typecheck module EL = Elexp module SU = Subst @@ -274,8 +276,9 @@ and _lexp_p_infer (p : pexp) (ctx : lexp_context) i: lexp * ltype = let ltp, _ = lexp_infer ptp ctx in (_lexp_p_check pxp ltp ctx (i + 1)), ltp - | _ -> pexp_print p; print_string "\n"; - lexp_fatal tloc "Unhandled Pexp" + (*FIXME right thing to do*) + | _ -> let meta = Unif.mkMetavar S.Identity (Util.dummy_location, "") (*???*) + in (meta, lexp_p_check p meta ctx) and lexp_let_decls decls (body: lexp) ctx i = @@ -287,6 +290,8 @@ and lexp_let_decls decls (body: lexp) ctx i = and lexp_p_check (p : pexp) (t : ltype) (ctx : lexp_context): lexp = _lexp_p_check p t ctx 1 +(*TODO : - add substitution parameter for unification + - try to unify in default case *) and _lexp_p_check (p : pexp) (t : ltype) (ctx : lexp_context) i: lexp = let tloc = pexp_location p in @@ -312,18 +317,21 @@ and _lexp_p_check (p : pexp) (t : ltype) (ctx : lexp_context) i: lexp = lxp | _ -> let (e, inferred_t) = _lexp_p_infer p ctx (i + 1) in - e (* + (* e *) match e with (* Built-in is a dummy function with no type. We cannot check * Built-in *) | Builtin _ -> e | _ -> - (if TC.conv_p inferred_t t then () else debug_msg ( + (* (if TC.conv_p inferred_t t then () else debug_msg ( *) + (match Unif.unify inferred_t t Unif.empty_subst with + | Some _ -> () + | None -> debug_msg ( print_string "1 exp "; lexp_print e; print_string "\n"; print_string "2 inf "; lexp_print inferred_t; print_string "\n"; print_string "3 Ann "; lexp_print t; print_string "\n"; lexp_warning tloc "Type Mismatch inferred != Annotation")); - e*) + e (* Lexp.case cam be checked and inferred *) and lexp_case (rtype: lexp option) (loc, target, patterns) ctx i = ===================================== src/unification.ml ===================================== --- a/src/unification.ml +++ b/src/unification.ml @@ -22,8 +22,9 @@ type constraints = (lexp * lexp) list (*| Error _ -> None*) (*| Nil -> None*) -let global_last_metavar = ref 0 -let create_metavar = global_last_metavar := !global_last_metavar + 1; !global_last_metavar +let global_last_metavar = ref (-1) (*The first metavar is 0*) +let create_metavar () = global_last_metavar := !global_last_metavar + 1; !global_last_metavar +let mkMetavar subst vdef = Metavar (create_metavar (), subst, vdef) (* For convenience *) type return_type = (substitution * constraints) option ===================================== tests/inverse_test.ml ===================================== --- a/tests/inverse_test.ml +++ b/tests/inverse_test.ml @@ -29,27 +29,22 @@ let rec mkTestSubst lst = (mkShift2 shift (mkTestSubst tail)) | [] -> S.identity -type result_type = - | Ok - | TransfoFail - | InverseFail - (*TODO better checking of where it should fail*) let input = - ((mkTestSubst ((0, 3)::(2, 2)::(3, 5)::[])), Ok):: - ((mkTestSubst ((1, 3)::(2, 2)::(3, 5)::[])), Ok):: - ((mkTestSubst ((1, 3)::(2, 2)::(4, 5)::[])), Ok):: - ((mkTestSubst ((0, 3)::(2, 2)::(4, 5)::[])), Ok):: - ((mkTestSubst ((0, 3)::(1, 2)::(4, 5)::[])), Ok):: - ((mkTestSubst ((0, 3)::(1, 2)::(4, 1)::(5, 5)::[])), TransfoFail):: - ((S.cons (mkVar 1) (S.shift 3)), Ok):: - ((S.cons (mkVar 1) (S.cons (mkVar 3) (S.identity))), TransfoFail):: - ((S.mkShift (S.shift 3) 4), Ok):: - ((S.mkShift (S.cons (mkVar 1) (S.identity)) 5), TransfoFail):: - ((mkTestSubst ((4, 0)::(2, 2)::(3, 5)::[])), Ok):: - ((mkTestSubst ((1, 2)::(5, 1)::(3, 5)::[])), Ok):: - ((mkTestSubst ((1, 2)::(5, 2)::(3, 5)::[])), InverseFail):: - ((mkTestSubst ((0, 3)::(1, 2)::(4, 1)::(9, 5)::[])), TransfoFail):: + ((mkTestSubst ((0, 3)::(2, 2)::(3, 5)::[])), true):: + ((mkTestSubst ((1, 3)::(2, 2)::(3, 5)::[])), true):: + ((mkTestSubst ((1, 3)::(2, 2)::(4, 5)::[])), true):: + ((mkTestSubst ((0, 3)::(2, 2)::(4, 5)::[])), true):: + ((mkTestSubst ((0, 3)::(1, 2)::(4, 5)::[])), true):: + ((mkTestSubst ((0, 3)::(1, 2)::(4, 1)::(5, 5)::[])), false):: + ((S.cons (mkVar 1) (S.shift 3)), true):: + ((S.cons (mkVar 1) (S.cons (mkVar 3) (S.identity))), false):: + ((S.mkShift (S.shift 3) 4), true):: + ((S.mkShift (S.cons (mkVar 1) (S.identity)) 5), false):: + ((mkTestSubst ((4, 0)::(2, 2)::(3, 5)::[])), true):: + ((mkTestSubst ((1, 2)::(5, 1)::(3, 5)::[])), true):: + ((mkTestSubst ((1, 2)::(5, 2)::(3, 5)::[])), false):: + ((mkTestSubst ((0, 3)::(1, 2)::(4, 1)::(9, 5)::[])), false):: [] let is_identity s = @@ -106,83 +101,53 @@ let get_dim lst = let max i s = max i (String.length s) in List.fold_left - (fun (acs, acsf, acs', acc) (s, sf, s', comp) -> ((max acs s), (max acsf sf), (max acs' s'), (max acc comp))) - (0,0,0,0) + (fun (acs, acs', acc) (s, s', comp) -> ((max acs s), (max acs' s'), (max acc comp))) + (0,0,0) lst let fmt_res str = - let (ds, dsf, ds', dcomp) = get_dim str - in List.map (fun (s, sf, s', com) -> "[ " ^ - (padding_right s ds ' ') ^ " -> " ^ - (padding_right (sf ^ " ]") dsf ' ') ^ " ∘ " ^ - (padding_right s' ds' ' ') ^ " = " ^ - (com) + let (ds, ds', dcomp) = get_dim str + in List.map (fun (s, s', com) -> (padding_right s ds ' ') ^ " -> " ^ + (padding_right s' ds' ' ') ^ " = " ^ + (com) ) str -(* let string_of_subst = ocaml_string_of_subst *) -(* let fmt_res str = *) -(* List.map (fun (_, sf, s', com) -> sf ^ " ∘ " ^ s' ^ " = " ^ com ) str *) - let get_dim lst = let max i s = max i (String.length s) in List.fold_left - (fun (acs, acsf, acs', acc) (s, sf, s', comp) -> ((max acs s), (max acsf sf), (max acs' s'), (max acc comp))) - (0,0,0,0) + (fun (acs, acs', acc) (s, s', comp) -> ((max acs s), (max acs' s'), (max acc comp))) + (0,0,0) lst + let _ = generate_tests "INVERSION" (fun () -> input) fmt_res - (fun (s, b) -> ( match inverse s, flatten s with - | Some (s'), Some (sf) -> (let comp = scompose sf s' in - let ret = (match (is_identity comp), b with - | true, Ok -> true (*if we are here, the result of the composition should be Id*) - | false, Ok -> false - | _, _ -> false) - in let str = ((string_of_subst s), (string_of_subst sf), (string_of_subst s'), (string_of_subst comp)) - in (str, ret)) - | Some (s'), None -> ((string_of_subst s, "None", string_of_subst s', "None"),(match b with - | TransfoFail -> true - | _ -> false)) - | None, Some(sf) -> ((string_of_subst s, string_of_subst sf, "None", "None"), (match b with - | InverseFail -> true - | _ -> false)) - | _ -> ((string_of_subst s, "None", "None", "None"), (match b with - | Ok -> false - | _ -> true))) + (fun (s, b) -> ( match inverse s with + | Some (s') -> (let comp = scompose s s' in + let ret = (is_identity comp) + in let str = ((string_of_subst s), (string_of_subst s'), (string_of_subst comp)) + in (str, ret)) + | None -> ((string_of_subst s, "None", "None"), not b) + ) ) +let fmt_res str = + List.map (fun (s, s', com) -> (s) ^ " -> " ^ + (s') ^ " = " ^ + (com) ) str + (* TODO find a better way to check test*) let _ = generate_tests "INVERSION-RAND" (fun () -> generateRandInput 5 10) fmt_res - (fun (s) -> ( match inverse s, flatten s with - | Some (s'), Some (sf) -> (let comp = scompose sf s' in - let ret = (is_identity comp) - in let str = ((string_of_subst s), (string_of_subst sf), (string_of_subst s'), (string_of_subst comp)) - in (str, ret)) - | Some (s'), None -> ((string_of_subst s, "None", string_of_subst s', "None"),false) - | None, Some(sf) -> ((string_of_subst s, string_of_subst sf, "None", "None"), false) - | _ -> ((string_of_subst s, "None", "None", "None"), false) + (fun (s) -> ( match inverse s with + | Some (s') -> (let comp = scompose s s' in + let ret = (is_identity comp) + in let str = ((string_of_subst s), (string_of_subst s'), (string_of_subst comp)) + in (str, ret)) + | None -> ((string_of_subst s , "None" , "None") , false) )) -let _ = generate_tests "TRANSFORMATION" - (fun () -> input) - (fun subst -> - let padding_right s d c = "\n" ^ s ^ "\n" - in let string_of_subst = pp_ocaml_string_of_subst - in let subst = List.map (fun (s,fs) -> (string_of_subst s, string_of_subst fs)) subst - in let get_dim lst = - let max i s = max i (String.length s) - in List.fold_left (fun (acs, acsf) (s, sf) -> ((max acs s), (max acsf sf))) (0,0) lst - in let (ds, dsf) = get_dim subst - in List.map (fun (s,sf) -> (padding_right s ds ' ') ^ " -> " ^ (padding_right sf dsf ' ')) subst) - (fun (subst, b) -> match flatten subst, b with - | Some(s), Ok -> ((subst, (s)), true) - | Some(s), InverseFail -> ((subst, (s)), true) - | None, TransfoFail -> ((subst, S.identity), true) - | Some (s), _ -> ((subst, s), false) - | None, _ -> ((subst, S.identity), false)) - let _ = run_all () ===================================== tests/lparse_test.ml ===================================== --- /dev/null +++ b/tests/lparse_test.ml @@ -0,0 +1,42 @@ + +open Lparse +open Fmt_lexp +open Utest_lib + +let test + (input_gen: (unit -> 'a list)) + (fmt: 'b list -> string list) + (tester: 'a -> ('b * bool)): (string * bool) list = + let input = List.map tester (input_gen ()) + in let str = List.map (fun (s, _) -> s ) input + in let b = List.map (fun (_, b) -> b) input + in List.combine (fmt str) b + +let generate_tests (name: string) + (input_gen: (unit -> 'a list)) + (fmt: 'b list -> string list) + (tester: 'a -> ('b * bool)) = + let idx = (ref 0) + in List.map (fun (sub, res) -> + idx := !idx + 1; + add_test name + ((padding_left (string_of_int (!idx)) 2 '0') ^ " - " ^ sub) + (fun () -> if res then success () else failure ())) + (test input_gen fmt tester) + +let input = "x = lambda x -> x;" + +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 _ = generate_tests + "TYPECHECK" + (fun () -> [generate_lexp_from_str input]) + (fun x -> List.map string_of_lxp x) + (fun x -> (x, false)) + +let _ = run_all () View it on GitLab: https://gitlab.com/monnier/typer/compare/293f20f65d551488bcf599af7c2bd8536c…

1 0

[Git][monnier/typer][unification] * tests/inverse_test.ml (is_identity.is_identity): Forget it
by Stefan 28 Jul '16

28 Jul '16

Stefan pushed to branch unification at Stefan / Typer Commits: 293f20f6 by Stefan Monnier at 2016-07-28T14:15:34-04:00 * tests/inverse_test.ml (is_identity.is_identity): Forget it * src/lexp.ml (push_susp): Don't be so picky. - - - - - 2 changed files: - src/lexp.ml - tests/inverse_test.ml Changes: ===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -328,10 +328,10 @@ let rec push_susp e s = (* Push a suspension one level down. *) * pushes the subst into them eagerly. IOW if there's a Susp(Var..) * or Susp(Metavar..) it's because some chunk of code should use mkSusp * rather than Susp. *) - | Susp (e,s') -> U.msg_error "SUSP" (lexp_location e) "¡Susp(Susp)!"; + | Susp (e,s') -> (* U.msg_error "SUSP" (lexp_location e) "¡Susp(Susp)!"; *) push_susp e (scompose s' s) | (Var _ | Metavar _) - -> U.msg_error "SUSP" (lexp_location e) "¡Susp((meta)var)!"; + -> (* U.msg_error "SUSP" (lexp_location e) "¡Susp((meta)var)!"; *) push_susp (mkSusp e s) S.identity let nosusp e = (* Return `e` without `Susp`. *) ===================================== tests/inverse_test.ml ===================================== --- a/tests/inverse_test.ml +++ b/tests/inverse_test.ml @@ -56,7 +56,7 @@ let is_identity s = let rec is_identity s acc = match s with | S.Cons(Var(_, idx), s1) when idx = acc -> is_identity s1 (acc + 1) - | S.Shift(S.Identity, shift) -> (0 = shift) + | S.Shift(S.Identity, shift) -> (acc = shift) | S.Identity -> true | _ -> false in is_identity s 0 View it on GitLab: https://gitlab.com/monnier/typer/commit/293f20f65d551488bcf599af7c2bd8536c7…

1 0

[Git][monnier/typer][unification] * tests/inverse_test.ml (is_identity.is_identity): Only shift 0 is identity.
by Stefan 28 Jul '16

28 Jul '16

Stefan pushed to branch unification at Stefan / Typer Commits: 93626d8b by Stefan Monnier at 2016-07-28T14:12:26-04:00 * tests/inverse_test.ml (is_identity.is_identity): Only shift 0 is identity. - - - - - 1 changed file: - tests/inverse_test.ml Changes: ===================================== tests/inverse_test.ml ===================================== --- a/tests/inverse_test.ml +++ b/tests/inverse_test.ml @@ -56,7 +56,7 @@ let is_identity s = let rec is_identity s acc = match s with | S.Cons(Var(_, idx), s1) when idx = acc -> is_identity s1 (acc + 1) - | S.Shift(S.Identity, shift) -> (acc = shift) + | S.Shift(S.Identity, shift) -> (0 = shift) | S.Identity -> true | _ -> false in is_identity s 0 View it on GitLab: https://gitlab.com/monnier/typer/commit/93626d8b8c6017bcd04b49b3e4b698bfcb1…

1 0

[Git][monnier/typer][unification] Tweak use of substitutions and unsusp
by Stefan 28 Jul '16

28 Jul '16

Stefan pushed to branch unification at Stefan / Typer Commits: 4e504963 by Stefan Monnier at 2016-07-28T12:42:23-04:00 Tweak use of substitutions and unsusp * src/inverse_subst.ml (mkFinalShift): Remove; use S.shift instead. (toIr): Use S.mkShift. (flattenIr.flattenCons): Remove unused `offset' arg. Simplify. * src/lexp.ml (subst): Newtype. (mkSusp): Also apply eagerly to Metavar. (push_susp): Rename from unsusp. (nosusp): Rename from ususp_all. (_lexp_to_str): Use push_susp. * src/unification.ml (unify.tmp): Use nosusp. (_unify_susp): Remove. * tests/inverse_test.ml: Use S.shift/cons and friends. - - - - - 8 changed files: - src/elexp.ml - src/inverse_subst.ml - src/lexp.ml - src/lparse.ml - src/subst.ml - src/typecheck.ml - src/unification.ml - tests/inverse_test.ml Changes: ===================================== src/elexp.ml ===================================== --- a/src/elexp.ml +++ b/src/elexp.ml @@ -86,7 +86,7 @@ let rec erase_type (lxp: L.lexp): elexp = Case(l, (erase_type target), (clean_map cases), (clean_maybe default)) - | L.Susp(l, s) -> erase_type (L.unsusp l s) + | L.Susp(l, s) -> erase_type (L.push_susp l s) (* To be thrown out *) | L.Arrow _ -> Type ===================================== src/inverse_subst.ml ===================================== --- a/src/inverse_subst.ml +++ b/src/inverse_subst.ml @@ -12,28 +12,27 @@ type inter_subst = lexp list (* Intermediate between "tree"-like substitution an let dummy_var = Var((dummy_location, "DummyVar"), -1) -(** Make a Shift with Identity as "inner" substitution. - Returns Identity if the Shift offset is lower or equal to 0 -*) -let mkFinalShift (value: int): lexp S.subst = - if value > 0 - then S.Shift (S.Identity, value) - else S.Identity - -(** Transform a subst into a more linear 'intermdiate representation': +(** Transform a subst into a more linear 'intermediate representation': - - a1.↑^\{x1\}(a2.↑^\{x2\}(a3.↑^\{x3\}id)) -> a1.(↑^\{x1\}a2).(↑^\{x2\}a3).↑^\{x3\}id + - a₁ · ↑n₁ (a₂ · ↑n₂ (a₃ · ↑n₃ id)) + ⇒ a₁' · a₂' · a₃' · ↑n₃ id or in ocaml-ish representation : - - S.Cons(var, S.Shift(..., offset)) -> S.Cons(var, S.Shift(S.Identity, offset))::...::Identity + - S.Cons(var, S.Shift(..., offset)) + ⇒ S.Cons(var, S.Shift(S.Identity, offset))::...::Identity *) let toIr (s: lexp S.subst) : inter_subst = - let rec toIr s last_offset = + let rec toIr s total_offset = match s with - | S.Shift (s_1, offset) -> toIr s_1 (last_offset + offset) - | S.Cons(Var _ as v, s_1) -> Susp(v, (S.mkShift S.Identity last_offset))::(toIr s_1 last_offset) - | S.Identity -> [Susp(dummy_var, (S.mkShift S.Identity last_offset ))] + | S.Shift (s_1, offset) -> toIr s_1 (total_offset + offset) + (* FIXME: A Cons with something else than a Var is not an error. + * It might mean that we can't invert this substitution, but that's + * no justification for "assert false". *) + | S.Cons(Var _ as v, s_1) + (* FIXME: Why not L.mkSusp? *) + -> Susp (v, S.shift total_offset)::(toIr s_1 total_offset) + | S.Identity -> [Susp (dummy_var, S.shift total_offset)] | _ -> assert false in toIr s 0 @@ -46,15 +45,14 @@ let toIr (s: lexp S.subst) : inter_subst = - <code>S.Cons(var, S.Shift(S.Identity, offset))::...::Identity -> S.Cons(var, S.Cons(...S.Shift(S.Identity, x1+x2+x3...)))</code> *) let flattenIr (s: inter_subst): lexp S.subst option = - let rec flattenCons s offset = + let rec flattenCons s = match s with - | Susp (_, S.Shift (S.Identity, o))::[] -> Some (S.Shift(S.Identity, o + offset)) - | Susp (_, S.Identity)::[] -> Some (mkFinalShift offset) - | susp::tail -> (match flattenCons tail offset with - | Some (s1) -> Some (S.Cons (unsusp_all susp, s1)) + | Susp (_dummy_var, s)::[] -> Some s + | susp::tail -> (match flattenCons tail with + | Some (s1) -> Some (S.cons (nosusp susp) s1) | None -> None) | _ -> None - in flattenCons s 0 + in flattenCons s (** Flatten a "tree"-like substitution: @@ -156,9 +154,9 @@ let to_list (s: lexp S.subst) : (((int * int) list) * int) = let rec to_cons (lst: (int * int) list) (shift: int) : lexp S.subst option = match lst with | (_, i)::tail -> (match (to_cons tail shift) with - | Some s -> Some (S.Cons (mkVar i, s)) + | Some s -> Some (S.cons (mkVar i) s) | None -> None) - | [] -> Some (mkFinalShift shift) + | [] -> Some (S.shift shift) (** Compute the inverse, if there is one, of the substitution. ===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -53,13 +53,14 @@ type label = symbol (* Pour la propagation des types bidirectionnelle, tout va dans `infer`, * sauf Lambda et Case qui vont dans `check`. Je crois. *) type ltype = lexp + and subst = lexp S.subst and lexp = | Imm of sexp (* Used for strings, ... *) | SortLevel of sort_level | Sort of U.location * sort | Builtin of vdef * ltype | Var of vref - | Susp of lexp * lexp S.subst (* Lazy explicit substitution: e[σ]. *) + | Susp of lexp * subst (* Lazy explicit substitution: e[σ]. *) (* This "Let" allows recursion. *) | Let of U.location * (vdef * lexp * ltype) list * lexp | Arrow of arg_kind * vdef option * ltype * U.location * lexp @@ -74,7 +75,7 @@ type ltype = lexp * ltype (* The type of the return value of all branches *) * (U.location * (arg_kind * vdef option) list * lexp) SMap.t * lexp option (* Default. *) - | Metavar of int * (lexp S.subst) * vdef (*idx * S.subst * (name * location)*) + | Metavar of int * subst * vdef (* (\* For logical metavars, there's no substitution. *\) * | Metavar of (U.location * string) * metakind * metavar ref * and metavar = @@ -110,9 +111,13 @@ type varbind = let rec mkSusp e s = if S.identity_p s then e else + (* We apply the substitution eagerly to some terms. + * There's no deep technical rason for that: + * it just seemed like a good idea to do it eagerly when it's easy. *) match e with | Susp (e, s') -> mkSusp e (scompose s' s) - | Var (l,v) -> slookup s l v (* Apply the substitution eagerly. *) + | Var (l,v) -> slookup s l v + | Metavar (vn, s', vd) -> Metavar (vn, scompose s' s, vd) | _ -> Susp (e, s) and scompose s1 s2 = S.compose mkSusp s1 s2 and slookup s l v = S.lookup (fun l i -> Var (l, i)) @@ -272,16 +277,13 @@ let rec lexp_location e = let vdummy = (U.dummy_location, "dummy") let maybev mv = match mv with None -> vdummy | Some v -> v -let rec unsusp e s = (* Push a suspension one level down. *) +let rec push_susp e s = (* Push a suspension one level down. *) match e with | Imm _ -> e | SortLevel _ -> e | Sort (l, Stype e) -> Sort (l, Stype (mkSusp e s)) | Sort (l, _) -> e | Builtin _ -> e - | Var ((l,_) as lv,v) -> U.msg_error "SUSP" l "¡Susp(Var)!"; slookup s lv v - | Susp (e,s') -> U.msg_error "SUSP" (lexp_location e) "¡Susp(Susp)!"; - mkSusp e (scompose s' s) | Let (l, defs, e) -> let s' = L.fold_left (fun s (v, _, _) -> ssink v s) s defs in let (_,ndefs) = L.fold_left (fun (s,ndefs) (v, def, ty) @@ -322,11 +324,19 @@ let rec unsusp e s = (* Push a suspension one level down. *) match default with | None -> default | Some e -> Some (mkSusp e s)) - | Metavar (idx, s', vdef_) -> Metavar(idx, (S.compose (mkSusp) s s'), vdef_) + (* Susp should never appear around Var/Susp/Metavar because mkSusp + * pushes the subst into them eagerly. IOW if there's a Susp(Var..) + * or Susp(Metavar..) it's because some chunk of code should use mkSusp + * rather than Susp. *) + | Susp (e,s') -> U.msg_error "SUSP" (lexp_location e) "¡Susp(Susp)!"; + push_susp e (scompose s' s) + | (Var _ | Metavar _) + -> U.msg_error "SUSP" (lexp_location e) "¡Susp((meta)var)!"; + push_susp (mkSusp e s) S.identity -let unsusp_all e = +let nosusp e = (* Return `e` without `Susp`. *) match e with - | Susp(e, s) -> unsusp e s + | Susp(e, s) -> push_susp e s | _ -> e let lexp_to_string e = @@ -670,7 +680,7 @@ and _lexp_to_str ctx exp = | Float (_, s) -> tval (string_of_float s) | e -> sexp_to_str e) - | Susp _ -> _lexp_to_str ctx (unsusp_all exp) + | Susp (e, s) -> _lexp_to_str ctx (push_susp e s) | Var ((loc, name), idx) -> name ^ (index idx) ; ===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -241,7 +241,7 @@ and _lexp_p_infer (p : pexp) (ctx : lexp_context) i: lexp * ltype = let inductive_type = Var((loc, type_name), idx) in (* Get constructor args *) - let formal, args = match unsusp_all idt with + let formal, args = match nosusp idt with | Inductive(_, _, formal, ctor_def) -> ( try formal, (SMap.find cname ctor_def) with Not_found -> @@ -297,7 +297,7 @@ and _lexp_p_check (p : pexp) (t : ltype) (ctx : lexp_context) i: lexp = (* This case cannot be inferred *) | Plambda (kind, var, None, body) ->( (* Read var type from the provided type *) - let ltp, lbtp = match unsusp_all t with + let ltp, lbtp = match nosusp t with | Arrow(kind, _, ltp, _, lbtp) -> ltp, lbtp | _ -> lexp_error tloc "Type does not match"; dltype, dltype in @@ -402,7 +402,7 @@ and lexp_call (fun_name: pexp) (sargs: sexp list) ctx i = (* consume Arrows and args together *) let rec get_return_type name i ltp args = - match (unsusp_all ltp), args with + match (nosusp ltp), args with | _, [] -> ltp | Arrow(_, _, _, _, ltp), hd::tl -> (get_return_type name (i + 1) ltp tl) | _, _ -> lexp_warning loc @@ -416,7 +416,7 @@ and lexp_call (fun_name: pexp) (sargs: sexp list) ctx i = (* retrieve function's body *) let body, ltp = _lexp_p_infer fun_name ctx (i + 1) in - let ltp = unsusp_all ltp in + let ltp = nosusp ltp in let handle_named_call (loc, name) = (* Process Arguments *) @@ -428,7 +428,7 @@ and lexp_call (fun_name: pexp) (sargs: sexp list) ctx i = let idx = senv_lookup name ctx in let vf = (make_var name idx loc) in - match unsusp_all (env_lookup_expr ctx ((loc, name), idx)) with + match nosusp (env_lookup_expr ctx ((loc, name), idx)) with | Builtin((_, "Built-in"), _) ->( (* ------ SPECIAL ------ *) match !_parsing_internals, largs with @@ -476,7 +476,7 @@ and lexp_call (fun_name: pexp) (sargs: sexp list) ctx i = lexp_fatal loc (name ^ " was found but " ^ (string_of_int idx) ^ " is not a correct index.") in - let lxp = match unsusp_all lxp with + let lxp = match nosusp lxp with | Call(Var((_, "Macro_"), _), [(_, fct)]) -> fct | _ -> print_string "\n"; @@ -555,7 +555,7 @@ and lexp_read_pattern pattern exp target ctx: | Ppatvar ((loc, name) as var) ->( try( let idx = senv_lookup name ctx in - match unsusp_all (env_lookup_expr ctx ((loc, name), idx)) with + match nosusp (env_lookup_expr ctx ((loc, name), idx)) with (* We are matching a constructor *) | Cons _ -> (name, loc, []), ctx @@ -641,7 +641,7 @@ and lexp_decls_macro (loc, mname) sargs ctx: (pdecl list * lexp_context) = " is not a correct index.") in (* get stored function *) - let lxp = match unsusp_all lxp with + let lxp = match nosusp lxp with | Call(Var((_, "Macro_"), _), [(_, fct)]) -> fct | _ -> print_string "\n"; print_string (lexp_to_string lxp); print_string "\n"; ===================================== src/subst.ml ===================================== --- a/src/subst.ml +++ b/src/subst.ml @@ -21,6 +21,28 @@ this program. If not, see <http://www.gnu.org/licenses/>. *) module U = Util +(* Implementation of the subsitution calculus. + * + * As a general rule, try not to use the constructors of the `subst' + * datatype, but use the following entry points instead. + * Constructor functions: + * - S.identity + * - S.cons + * - S.mkShift + * - S.shift + * - S.compose + * - S.substitute + * - S.sink + * Destructor functions: + * - S.identity_p + * - S.lookup + * + * This implementation is generic (i.e. can be with various datatypes + * implementing the associated lambda-calculus), which is the reason for + * the added complexity of arguments like `mkVar` and `mkShift` to `S.lookup`. + * So in general, you'll want to use Lexp.scompose and Lexp.slookup + * for those functions. + *) (* Suspensions definitions. * @@ -236,6 +258,7 @@ let shift (m:db_offset) = mkShift Identity m (* The trivial substitution which doesn't do anything. *) let identity = Identity +(* Test if a substitution is trivial. The "_p" stands for "predicate". *) let identity_p s = match s with | Identity -> true | _ -> false (* Compose two substitutions. This implements the merging rules. ===================================== src/typecheck.ml ===================================== --- a/src/typecheck.ml +++ b/src/typecheck.ml @@ -110,7 +110,7 @@ let lookup_type ctx vref = let lookup_value ctx vref = let (_, i) = vref in match Myers.nth i ctx with - | (o, _, LetDef v, _) -> Some (unsusp v (S.shift (i + 1 - o))) + | (o, _, LetDef v, _) -> Some (push_susp v (S.shift (i + 1 - o))) | _ -> None let assert_type e t t' = @@ -151,7 +151,7 @@ let rec check ctx e = | Builtin (_, t) -> t (* FIXME: Check recursive references. *) | Var v -> lookup_type ctx v - | Susp (e, s) -> check ctx (unsusp e s) + | Susp (e, s) -> check ctx (push_susp e s) | Let (_, defs, e) -> let tmp_ctx = L.fold_left (fun ctx (v, e, t) ===================================== src/unification.ml ===================================== --- a/src/unification.ml +++ b/src/unification.ml @@ -81,11 +81,11 @@ 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 = - let tmp = match (l, r) with + let tmp = match (nosusp l, nosusp r) with | (_, Metavar _) -> _unify_metavar r l subst | (_, Call _) -> _unify_call r l subst | (_, Case _) -> _unify_case r l subst - | (_, Susp _) -> _unify_susp r l subst + | (_, Susp _) -> assert false | (_, Let _) -> _unify_let r l subst | (Imm _, _) -> _unify_imm l r subst | (Cons _, _) -> _unify_cons l r subst @@ -96,7 +96,7 @@ let rec unify (l: lexp) (r: lexp) (subst: substitution) : return_type = | (Lambda _, _) -> _unify_lambda l r subst | (Metavar _, _) -> _unify_metavar l r subst | (Call _, _) -> _unify_call l r subst - | (Susp _, _) -> _unify_susp l r subst + | (Susp _, _) -> assert false | (Case _, _) -> _unify_case l r subst | (Inductive _, _) -> _unfiy_induct l r subst | (Sort _, _) -> _unify_sort l r subst @@ -271,13 +271,6 @@ and _unify_call (call: lexp) (lxp: lexp) (subst: substitution) : return_type = | 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 -*) -and _unify_susp (susp_: lexp) (lxp: lexp) (subst: substitution) : return_type = - match susp_ with - | Susp _ -> unify (unsusp_all susp_) lxp subst - | _ -> None - (** Unify a Case with a lexp - Case, Case -> try to unify - Case, _ -> Constraint ===================================== tests/inverse_test.ml ===================================== --- a/tests/inverse_test.ml +++ b/tests/inverse_test.ml @@ -21,13 +21,13 @@ open Fmt_lexp open Debug_fun let mkShift2 shift subst = - S.Shift (subst, shift) + S.mkShift subst shift let rec mkTestSubst lst = match lst with - | (var, shift)::tail -> S.Cons (mkVar var, - mkShift2 shift (mkTestSubst tail)) - | [] -> S.Identity + | (var, shift)::tail -> S.cons (mkVar var) + (mkShift2 shift (mkTestSubst tail)) + | [] -> S.identity type result_type = | Ok @@ -42,10 +42,10 @@ let input = ((mkTestSubst ((0, 3)::(2, 2)::(4, 5)::[])), Ok):: ((mkTestSubst ((0, 3)::(1, 2)::(4, 5)::[])), Ok):: ((mkTestSubst ((0, 3)::(1, 2)::(4, 1)::(5, 5)::[])), TransfoFail):: - ((S.Cons (mkVar 1, S.Shift(S.Identity, 3))), Ok):: - ((S.Cons (mkVar 1, S.Cons (mkVar 3, S.Identity))), TransfoFail):: - ((S.Shift (S.Shift (S.Identity, 3), 4)), Ok):: - ((S.Shift (S.Cons (mkVar 1, S.Identity), 5)), TransfoFail):: + ((S.cons (mkVar 1) (S.shift 3)), Ok):: + ((S.cons (mkVar 1) (S.cons (mkVar 3) (S.identity))), TransfoFail):: + ((S.mkShift (S.shift 3) 4), Ok):: + ((S.mkShift (S.cons (mkVar 1) (S.identity)) 5), TransfoFail):: ((mkTestSubst ((4, 0)::(2, 2)::(3, 5)::[])), Ok):: ((mkTestSubst ((1, 2)::(5, 1)::(3, 5)::[])), Ok):: ((mkTestSubst ((1, 2)::(5, 2)::(3, 5)::[])), InverseFail):: @@ -59,10 +59,7 @@ let is_identity s = | S.Shift(S.Identity, shift) -> (acc = shift) | S.Identity -> true | _ -> false - in match s with - | S.Shift(S.Identity, _) -> true - | S.Identity -> true - | _ -> is_identity s 0 + in is_identity s 0 let generateRandInput shiftMax numberOfTest = Random.self_init (); @@ -184,8 +181,8 @@ let _ = generate_tests "TRANSFORMATION" (fun (subst, b) -> match flatten subst, b with | Some(s), Ok -> ((subst, (s)), true) | Some(s), InverseFail -> ((subst, (s)), true) - | None, TransfoFail -> ((subst, S.Identity), true) + | None, TransfoFail -> ((subst, S.identity), true) | Some (s), _ -> ((subst, s), false) - | None, _ -> ((subst, S.Identity), false)) + | None, _ -> ((subst, S.identity), false)) let _ = run_all () View it on GitLab: https://gitlab.com/monnier/typer/commit/4e5049638ef74bcaa83598d6a10ca91dfe0…

1 0

[Git][monnier/typer][unification] random (passing) test
by BONNEVALLE Vincent 28 Jul '16

28 Jul '16

BONNEVALLE Vincent pushed to branch unification at Stefan / Typer Commits: b291e84b by n3f4s at 2016-07-28T00:11:34+02:00 random (passing) test - - - - - 1 changed file: - tests/inverse_test.ml Changes: ===================================== tests/inverse_test.ml ===================================== --- a/tests/inverse_test.ml +++ b/tests/inverse_test.ml @@ -64,20 +64,22 @@ let is_identity s = | S.Identity -> true | _ -> is_identity s 0 -let generateRandInput n m = +let generateRandInput shiftMax numberOfTest = Random.self_init (); - let rec generateList n m = - let rec generateRandInput n i = - if n > i + let rec generateList shiftMax numberOfTest = + let rec generateRandInput shiftMax idx acc = + if idx < shiftMax then (if Random.bool () - then ( let r = Random.int n in - (i, (min (r + i) n))::(generateRandInput n (i + 1)) ) - else generateRandInput n (i + 1)) + then ( let r = Random.int shiftMax in + let shift = (min (r + idx + 1) (shiftMax)) + in let shift = shift + (max 0 ((idx + shift) - acc)) + in (idx, shift)::(generateRandInput shiftMax (idx + 1) (shift + acc)) ) + else generateRandInput shiftMax (idx + 1) acc) else [] - in if m >= 0 - then (mkTestSubst (generateRandInput n 0))::(generateList n (m - 1)) + in if numberOfTest >= 0 + then (mkTestSubst (generateRandInput shiftMax 0 0))::(generateList shiftMax (numberOfTest - 1)) else [] - in generateList n m + in generateList shiftMax numberOfTest let lxp = mkVar 3 @@ -154,6 +156,20 @@ let _ = generate_tests "INVERSION" | _ -> true))) ) +(* TODO find a better way to check test*) +let _ = generate_tests "INVERSION-RAND" + (fun () -> generateRandInput 5 10) + fmt_res + (fun (s) -> ( match inverse s, flatten s with + | Some (s'), Some (sf) -> (let comp = scompose sf s' in + let ret = (is_identity comp) + in let str = ((string_of_subst s), (string_of_subst sf), (string_of_subst s'), (string_of_subst comp)) + in (str, ret)) + | Some (s'), None -> ((string_of_subst s, "None", string_of_subst s', "None"),false) + | None, Some(sf) -> ((string_of_subst s, string_of_subst sf, "None", "None"), false) + | _ -> ((string_of_subst s, "None", "None", "None"), false) + )) + let _ = generate_tests "TRANSFORMATION" (fun () -> input) (fun subst -> View it on GitLab: https://gitlab.com/monnier/typer/commit/b291e84bae35b15e0ed5a75c095abbff21b…

1 0

[Git][monnier/typer][unification] 3 commits: add error in inverse for subst with same index
by BONNEVALLE Vincent 27 Jul '16

27 Jul '16

BONNEVALLE Vincent pushed to branch unification at Stefan / Typer Commits: 03221c91 by n3f4s at 2016-07-27T23:25:05+02:00 add error in inverse for subst with same index - - - - - ead6631f by n3f4s at 2016-07-27T23:26:20+02:00 better comparison against Id in tests - - - - - 523c1f4d by n3f4s at 2016-07-27T23:26:58+02:00 better testing for INVERSE & TRANSFORMATION - - - - - 2 changed files: - src/inverse_subst.ml - tests/inverse_test.ml Changes: ===================================== src/inverse_subst.ml ===================================== --- a/src/inverse_subst.ml +++ b/src/inverse_subst.ml @@ -72,8 +72,8 @@ let flatten (s: lexp S.subst): lexp S.subst option = | None -> None | Some o2 -> Some (o + o2)) | S.Cons (Var(_, idx), sf) -> (match check sf with - | None -> None - | Some o -> if idx >= o then None else Some o) + | None -> None + | Some o -> if idx >= o then None else Some o) | _ -> assert false in match flattenIr (toIr s) with @@ -112,7 +112,7 @@ let mkVar (idx: int): lexp = Var((U.dummy_location, ""), idx) @param size size of the list to return @param acc recursion accumulator *) -let fill (l: (int * int) list) (size: int) (acc: (int * int) list): (int * int) list = +let fill (l: (int * int) list) (size: int) (acc: (int * int) list): (int * int) list option = let genDummyVar beg_ end_ = genDummyVar beg_ end_ (size + 1) in let rec fill_before (l: (int * int) list): (int * int) list = @@ -120,8 +120,9 @@ let fill (l: (int * int) list) (size: int) (acc: (int * int) list): (int * int) | [] -> [] | (idx, val_)::tail -> (if idx > 0 then (genDummyVar 0 idx)@l else l) - and fill_after (l: (int * int) list) (size: int) (acc: (int * int) list): (int * int) list = + and fill_after (l: (int * int) list) (size: int) (acc: (int * int) list): (int * int) list option = match l with + | (idx1, val1)::(idx2, val2)::tail when (idx1 = idx2) -> None | (idx1, val1)::(idx2, val2)::tail -> let tail = (idx2, val2)::tail in let accu = if (idx2 - idx1) > 1 @@ -129,9 +130,9 @@ let fill (l: (int * int) list) (size: int) (acc: (int * int) list): (int * int) else (acc@(idx1, val1)::[]) in fill_after tail size accu | (idx1, val1)::[] -> if (idx1 + 1) < size - then acc@((idx1, val1)::(genDummyVar (idx1 + 1) size)) - else acc@[(idx1, val1)] - | [] -> acc + then Some (acc@((idx1, val1)::(genDummyVar (idx1 + 1) size))) + else Some (acc@[(idx1, val1)]) + | [] -> Some acc in fill_after (fill_before l) size acc (** Transform a L-exp to a list of (e_i, i) where e_i is the position of the debuijn index i @@ -171,6 +172,7 @@ let rec inverse (subst: lexp S.subst ) : lexp S.subst option = | Some (s) -> let cons_lst, shift_val = to_list s in let size = sizeOf cons_lst - in let cons_lst = fill (sort cons_lst) shift_val [] - in to_cons cons_lst size + in match fill (sort cons_lst) shift_val [] with + | None -> None + | Some cons_lst -> to_cons cons_lst size ===================================== tests/inverse_test.ml ===================================== --- a/tests/inverse_test.ml +++ b/tests/inverse_test.ml @@ -29,22 +29,41 @@ let rec mkTestSubst lst = mkShift2 shift (mkTestSubst tail)) | [] -> S.Identity +type result_type = + | Ok + | TransfoFail + | InverseFail + +(*TODO better checking of where it should fail*) let input = - (mkTestSubst ((0, 3)::(2, 2)::(3, 5)::[])):: - (mkTestSubst ((1, 3)::(2, 2)::(3, 5)::[])):: - (mkTestSubst ((1, 3)::(2, 2)::(4, 5)::[])):: - (mkTestSubst ((0, 3)::(2, 2)::(4, 5)::[])):: - (mkTestSubst ((0, 3)::(1, 2)::(4, 5)::[])):: - (mkTestSubst ((0, 3)::(1, 2)::(4, 1)::(5, 5)::[])):: - (S.Cons (mkVar 1, S.Shift(S.Identity, 3))):: - (S.Cons (mkVar 1, S.Cons (mkVar 3, S.Identity))):: - (S.Shift (S.Shift (S.Identity, 3), 4)):: - (S.Shift (S.Cons (mkVar 1, S.Identity), 5)):: - (mkTestSubst ((4, 0)::(2, 2)::(3, 5)::[])):: - (mkTestSubst ((1, 2)::(5, 2)::(3, 5)::[])):: - (mkTestSubst ((0, 3)::(1, 2)::(4, 1)::(9, 5)::[])):: (* Erroneous result -> normal ?*) + ((mkTestSubst ((0, 3)::(2, 2)::(3, 5)::[])), Ok):: + ((mkTestSubst ((1, 3)::(2, 2)::(3, 5)::[])), Ok):: + ((mkTestSubst ((1, 3)::(2, 2)::(4, 5)::[])), Ok):: + ((mkTestSubst ((0, 3)::(2, 2)::(4, 5)::[])), Ok):: + ((mkTestSubst ((0, 3)::(1, 2)::(4, 5)::[])), Ok):: + ((mkTestSubst ((0, 3)::(1, 2)::(4, 1)::(5, 5)::[])), TransfoFail):: + ((S.Cons (mkVar 1, S.Shift(S.Identity, 3))), Ok):: + ((S.Cons (mkVar 1, S.Cons (mkVar 3, S.Identity))), TransfoFail):: + ((S.Shift (S.Shift (S.Identity, 3), 4)), Ok):: + ((S.Shift (S.Cons (mkVar 1, S.Identity), 5)), TransfoFail):: + ((mkTestSubst ((4, 0)::(2, 2)::(3, 5)::[])), Ok):: + ((mkTestSubst ((1, 2)::(5, 1)::(3, 5)::[])), Ok):: + ((mkTestSubst ((1, 2)::(5, 2)::(3, 5)::[])), InverseFail):: + ((mkTestSubst ((0, 3)::(1, 2)::(4, 1)::(9, 5)::[])), TransfoFail):: [] +let is_identity s = + let rec is_identity s acc = + match s with + | S.Cons(Var(_, idx), s1) when idx = acc -> is_identity s1 (acc + 1) + | S.Shift(S.Identity, shift) -> (acc = shift) + | S.Identity -> true + | _ -> false + in match s with + | S.Shift(S.Identity, _) -> true + | S.Identity -> true + | _ -> is_identity s 0 + let generateRandInput n m = Random.self_init (); let rec generateList n m = @@ -116,19 +135,23 @@ let get_dim lst = let _ = generate_tests "INVERSION" (fun () -> input) fmt_res - (fun s -> ( match inverse s, flatten s with + (fun (s, b) -> ( match inverse s, flatten s with | Some (s'), Some (sf) -> (let comp = scompose sf s' in - let ret = (match comp with - | S.Identity -> true - | _ -> false) + let ret = (match (is_identity comp), b with + | true, Ok -> true (*if we are here, the result of the composition should be Id*) + | false, Ok -> false + | _, _ -> false) in let str = ((string_of_subst s), (string_of_subst sf), (string_of_subst s'), (string_of_subst comp)) in (str, ret)) - | Some (s'), None -> ((string_of_subst s, "None", string_of_subst s', "None"), - false ) - | None, Some(sf) -> ((string_of_subst s, string_of_subst sf, "None", "None"), - false ) - | _ -> ((string_of_subst s, "None", "None", "None"), - false )) + | Some (s'), None -> ((string_of_subst s, "None", string_of_subst s', "None"),(match b with + | TransfoFail -> true + | _ -> false)) + | None, Some(sf) -> ((string_of_subst s, string_of_subst sf, "None", "None"), (match b with + | InverseFail -> true + | _ -> false)) + | _ -> ((string_of_subst s, "None", "None", "None"), (match b with + | Ok -> false + | _ -> true))) ) let _ = generate_tests "TRANSFORMATION" @@ -142,8 +165,11 @@ let _ = generate_tests "TRANSFORMATION" in List.fold_left (fun (acs, acsf) (s, sf) -> ((max acs s), (max acsf sf))) (0,0) lst in let (ds, dsf) = get_dim subst in List.map (fun (s,sf) -> (padding_right s ds ' ') ^ " -> " ^ (padding_right sf dsf ' ')) subst) - (fun subst -> match flatten subst with - |Some s -> ((subst, (s)), true) - | None -> ((subst, S.Identity), false)) + (fun (subst, b) -> match flatten subst, b with + | Some(s), Ok -> ((subst, (s)), true) + | Some(s), InverseFail -> ((subst, (s)), true) + | None, TransfoFail -> ((subst, S.Identity), true) + | Some (s), _ -> ((subst, s), false) + | None, _ -> ((subst, S.Identity), false)) let _ = run_all () View it on GitLab: https://gitlab.com/monnier/typer/compare/65bbe6d12d2c516eeccd061436c50dae12…

1 0

[Git][monnier/typer][unification] 6 commits: apply the Shift on Id instead of the whole subst
by BONNEVALLE Vincent 27 Jul '16

27 Jul '16

BONNEVALLE Vincent pushed to branch unification at Stefan / Typer Commits: 3226d35e by n3f4s at 2016-07-26T21:51:37+02:00 apply the Shift on Id instead of the whole subst - - - - - f4086ee1 by n3f4s at 2016-07-26T21:58:37+02:00 change implementation of sizeOf - - - - - b1f5bca2 by n3f4s at 2016-07-26T21:59:15+02:00 add check for de Bruijn index - - - - - f2514bb5 by n3f4s at 2016-07-27T18:08:04+02:00 sort (e_i, i) couples during inversion - - - - - 18f3261b by n3f4s at 2016-07-27T18:09:45+02:00 remove dead code, add type hint and update doc - - - - - 65bbe6d1 by n3f4s at 2016-07-27T18:37:49+02:00 update doc - - - - - 2 changed files: - src/inverse_subst.ml - tests/inverse_test.ml Changes: ===================================== src/inverse_subst.ml ===================================== --- a/src/inverse_subst.ml +++ b/src/inverse_subst.ml @@ -8,15 +8,18 @@ module S = Subst (* Transformation *) -(** a_0 . ↑^x1 (a_2 . ↑x2 ... ) . ↑^xn . id*) -(* type inter_subst = lexp S.subst list (* Intermediate between "tree"-like substitution and fully flattened subsitution *) *) type inter_subst = lexp list (* Intermediate between "tree"-like substitution and fully flattened subsitution *) -(** Helper function that create a Cons(_, Shift(_)) *) -(* let mkSubstNode var offset = S.Cons (var, S.Shift(S.Identity, offset)) *) - let dummy_var = Var((dummy_location, "DummyVar"), -1) +(** Make a Shift with Identity as "inner" substitution. + Returns Identity if the Shift offset is lower or equal to 0 +*) +let mkFinalShift (value: int): lexp S.subst = + if value > 0 + then S.Shift (S.Identity, value) + else S.Identity + (** Transform a subst into a more linear 'intermdiate representation': - a1.↑^\{x1\}(a2.↑^\{x2\}(a3.↑^\{x3\}id)) -> a1.(↑^\{x1\}a2).(↑^\{x2\}a3).↑^\{x3\}id @@ -32,40 +35,26 @@ let toIr (s: lexp S.subst) : inter_subst = | S.Cons(Var _ as v, s_1) -> Susp(v, (S.mkShift S.Identity last_offset))::(toIr s_1 last_offset) | S.Identity -> [Susp(dummy_var, (S.mkShift S.Identity last_offset ))] | _ -> assert false - in let res = toIr s 0 - in Debug_fun.do_debug ( fun () -> - List.iter (fun i -> - print_string (Fmt_lexp.string_of_lxp i); print_string "::"; - match i with - | Susp _ -> assert true - | _ -> assert false) res; - print_newline(); print_newline(); ); res + in toIr s 0 (** Transform an 'intermediate representation' into a sequence of cons followed by a shift - - a1.(↑^\{x1\}a2).(↑^\{x2\}a3).↑^\{x3\}id -> a1.a2.a3 ↑^\{x1+x2+x3\} + - a1.(↑^\{x1\}a2).(↑^\{x2\}a3).↑^\{x3\}id -> a1.a2.a3.(id ↑^\{x1+x2+x3\}) or in ocaml-ish representation : - - <code>S.Cons(var, S.Shift(S.Identity, offset))::...::Identity -> S.Shift(S.Cons(var, S.Cons(...)), x1+x2+x3...)</code> + - <code>S.Cons(var, S.Shift(S.Identity, offset))::...::Identity -> S.Cons(var, S.Cons(...S.Shift(S.Identity, x1+x2+x3...)))</code> *) let flattenIr (s: inter_subst): lexp S.subst option = - let rec flattenCons s = + let rec flattenCons s offset = match s with - | Susp (_, S.Shift (S.Identity, o))::[] -> Some (o, S.Identity) - | Susp (_, S.Identity)::[] -> Some (0, S.Identity) - | susp::tail -> (match flattenCons tail with - | Some (o, s1) -> Some (o, (S.Cons (unsusp_all susp, s1))) + | Susp (_, S.Shift (S.Identity, o))::[] -> Some (S.Shift(S.Identity, o + offset)) + | Susp (_, S.Identity)::[] -> Some (mkFinalShift offset) + | susp::tail -> (match flattenCons tail offset with + | Some (s1) -> Some (S.Cons (unsusp_all susp, s1)) | None -> None) | _ -> None - in Debug_fun.do_debug ( fun () -> - List.iter (fun i -> - match i with - | Susp _ -> assert true - | _ -> assert false) s); - match flattenCons s with - | Some(offset, cons) -> Some(S.Shift(cons, offset)) - | None -> None + in flattenCons s 0 (** Flatten a "tree"-like substitution: @@ -73,81 +62,65 @@ let flattenIr (s: inter_subst): lexp S.subst option = or in ocaml-ish representation : - - <code>S.Cons(var, S.Shift(..., offset)) -> S.Shift(S.Cons(var, S.Cons(...)), x1+x2+x3...)</code> + - <code>S.Cons(var, S.Shift(S.Identity, offset))::...::Identity -> S.Cons(var, S.Cons(...S.Shift(S.Identity, x1+x2+x3...)))</code> *) -let flatten (s: lexp S.subst) = flattenIr (toIr s) +let flatten (s: lexp S.subst): lexp S.subst option = + let rec check (sf: lexp S.subst): int option = + match sf with + | S.Identity -> Some 0 + | S.Shift(sf, o) -> (match check sf with + | None -> None + | Some o2 -> Some (o + o2)) + | S.Cons (Var(_, idx), sf) -> (match check sf with + | None -> None + | Some o -> if idx >= o then None else Some o) + | _ -> assert false + in + match flattenIr (toIr s) with + | None -> None + | Some (sf2) as sf -> match check sf2 with + | Some _ -> sf + | None -> None (* Inverse *) -(** Returns the value of the shift of a S.Shift -*) -let shiftOf s = - match s with - | S.Shift (_, o) -> o - | _ -> 0 - (** Returns the number of element in a sequence of S.Cons *) -let rec sizeOf s = - match s with - | S.Cons(_, s1) -> 1 + sizeOf s1 - | S.Shift(s1, _) -> sizeOf s1 - | S.Identity -> 0 - -(** Returns the nth of a susbstitution, - returns S.Identity if i > number_of_element(s) -*) -let rec nthOf s i = - match s, i with - | S.Cons _, 0 -> s - | S.Shift _, 0 -> s - | S.Identity, _ -> s - | S.Cons(_, s1), _ -> nthOf s1 (i - 1) - | S.Shift(s1, _), _ -> nthOf s1 (i - 1) +let rec sizeOf (s: (int * int) list): int = List.length s (** Returns the db_index of the "inside" of a Var *) let idxOf (_, idx) = idx (** Returns a list of couple (X, idx) where X go from beg_ to end_*) -let rec genDummyVar beg_ end_ idx = +let rec genDummyVar (beg_: int) (end_: int) (idx: int): (int * int) list = if beg_ < end_ then (beg_, idx)::(genDummyVar (beg_ + 1) end_ idx) else [] (** Returns a dummy variable with the db_index idx *) -let mkVar idx = Var((U.dummy_location, ""), idx) +let mkVar (idx: int): lexp = Var((U.dummy_location, ""), idx) -(** Map a list of tuple to a sequence of S.Cons -*) -let rec generate_s l = - match l with - | (_, i)::tail -> S.Cons(mkVar i, (generate_s tail)) - | [] -> S.Identity +(** Fill the gap between e_i in the list of couple (e_i, i) by adding + dummy variables. + With the exemple of the article : + should return <code>(1,1)::(2, X)::(3,2)::(4,3)::(5, Z)::[]</code> -(* With the exemple of the article : - should return <code>(1,1)::(3,2)::(4,3)::[]</code> -*) -let rec genCons s i = - match s with - | S.Cons(Var(v), s1) -> ((idxOf v), i)::(genCons s1 (i + 1)) (* e_{idx_of v} = i *) - | S.Identity -> [] - | _ -> assert false - -(* With the exemple of the article : - should return <code>(1,1)::(2, X)::(3,2)::(4,3)::(5, Z)::[]</code> + @param l list of (e_i, i) couples with gap between e_i + @param size size of the list to return + @param acc recursion accumulator *) -let fill l size acc = +let fill (l: (int * int) list) (size: int) (acc: (int * int) list): (int * int) list = let genDummyVar beg_ end_ = genDummyVar beg_ end_ (size + 1) in - let rec fill_before l = + let rec fill_before (l: (int * int) list): (int * int) list = match l with | [] -> [] | (idx, val_)::tail -> (if idx > 0 then (genDummyVar 0 idx)@l else l) - and fill_after l size acc = + and fill_after (l: (int * int) list) (size: int) (acc: (int * int) list): (int * int) list = match l with | (idx1, val1)::(idx2, val2)::tail -> let tail = (idx2, val2)::tail in @@ -161,21 +134,43 @@ let fill l size acc = | [] -> acc in fill_after (fill_before l) size acc -(** Take a "flattened" substitution and returns the inverse of the Cons +(** Transform a L-exp to a list of (e_i, i) where e_i is the position of the debuijn index i + in the debuijn index sequence *) -let generateCons s _size shift = - let sort = List.sort (fun (ei1, _) (ei2, _) -> compare ei1 ei2) - in - generate_s (fill (sort (genCons s 0)) shift []) +let to_list (s: lexp S.subst) : (((int * int) list) * int) = + let rec as_list (s: lexp S.subst) (i: int) : (((int * int) list) * int) = + match s with + | S.Cons (Var(v), s1) -> let tail, o = as_list s1 (i + 1) in ((((idxOf v), i)::tail ), o) + | S.Shift (S.Identity, shift) -> ([], shift) + | S.Identity -> ([], 0) + | _ -> assert false; + in as_list s 0 -(** <code>s:S.subst -> l:lexp -> s':S.subst</code> where <code>l[s][s'] = l</code> - Return undefined result for bad input +(** Transform a (e_i, i) list to a substitution by transforming the list into Cons and + adding a Shift. + + @param lst list of couple (ei_, i) to transform + @param shift value of the shift +*) +let rec to_cons (lst: (int * int) list) (shift: int) : lexp S.subst option = + match lst with + | (_, i)::tail -> (match (to_cons tail shift) with + | Some s -> Some (S.Cons (mkVar i, s)) + | None -> None) + | [] -> Some (mkFinalShift shift) + +(** Compute the inverse, if there is one, of the substitution. + + <code>s:S.subst, l:lexp, s':S.subst</code> where <code>l[s][s'] = l</code> and <code> inverse s = s' </code> *) let rec inverse (subst: lexp S.subst ) : lexp S.subst option = + let sort = List.sort (fun (ei1, _) (ei2, _) -> compare ei1 ei2) + in match flatten subst with - | Some(S.Shift(flattened, shift)) -> - let size = sizeOf flattened - in Some(S.Shift((generateCons flattened size shift), size)) - | None -> None - | _ -> assert false + | None -> None + | Some (s) -> + let cons_lst, shift_val = to_list s + in let size = sizeOf cons_lst + in let cons_lst = fill (sort cons_lst) shift_val [] + in to_cons cons_lst size ===================================== tests/inverse_test.ml ===================================== --- a/tests/inverse_test.ml +++ b/tests/inverse_test.ml @@ -98,7 +98,7 @@ let fmt_res str = (padding_right s ds ' ') ^ " -> " ^ (padding_right (sf ^ " ]") dsf ' ') ^ " ∘ " ^ (padding_right s' ds' ' ') ^ " = " ^ - (padding_right com dcomp ' ') + (com) ) str (* let string_of_subst = ocaml_string_of_subst *) @@ -123,7 +123,11 @@ let _ = generate_tests "INVERSION" | _ -> false) in let str = ((string_of_subst s), (string_of_subst sf), (string_of_subst s'), (string_of_subst comp)) in (str, ret)) - | _ -> ((string_of_subst s, string_of_subst S.Identity, string_of_subst S.Identity, string_of_subst S.Identity), + | Some (s'), None -> ((string_of_subst s, "None", string_of_subst s', "None"), + false ) + | None, Some(sf) -> ((string_of_subst s, string_of_subst sf, "None", "None"), + false ) + | _ -> ((string_of_subst s, "None", "None", "None"), false )) ) View it on GitLab: https://gitlab.com/monnier/typer/compare/4282321b68032b4ecc2496164905fcadc5…

1 0

[Git][monnier/typer][unification] 3 commits: better test output
by BONNEVALLE Vincent 26 Jul '16

26 Jul '16

BONNEVALLE Vincent pushed to branch unification at Stefan / Typer Commits: 77068263 by n3f4s at 2016-07-25T17:02:43+02:00 better test output - - - - - b72ea611 by n3f4s at 2016-07-25T17:03:08+02:00 debug substitution composed only with Cons - - - - - 4282321b by n3f4s at 2016-07-26T17:50:38+02:00 sort substitutions during inversion prevent inversion of substitution from returning an invalid substitution - - - - - 4 changed files: - src/debug_fun.ml - src/fmt_lexp.ml - src/inverse_subst.ml - tests/inverse_test.ml Changes: ===================================== src/debug_fun.ml ===================================== --- a/src/debug_fun.ml +++ b/src/debug_fun.ml @@ -1,7 +1,7 @@ open Fmt_lexp -(*let _debug = true*) +(* let _debug = true *) let _debug = false let logs = ref [] ===================================== src/fmt_lexp.ml ===================================== --- a/src/fmt_lexp.ml +++ b/src/fmt_lexp.ml @@ -13,7 +13,7 @@ let str_cyan str = if _color then cyan ^ str ^ reset else str let rec string_of_subst s = match s with - | S.Cons (Var(_, idx), s2) -> "a" ^ string_of_int idx ^ " · " ^ string_of_subst s2 + | S.Cons (Var(_, idx), s2) -> (* "a" ^ *) string_of_int idx ^ " · " ^ string_of_subst s2 | S.Cons (l, s2) -> string_of_lxp l ^ " · " ^ string_of_subst s2 | S.Shift (s2, shift) -> "(" ^ string_of_subst s2 ^ ") ↑^" ^ string_of_int shift | S.Identity -> "Id" @@ -24,6 +24,16 @@ and ocaml_string_of_subst s = | S.Shift (s2, shift) -> "Shift(" ^ ocaml_string_of_subst s2 ^ ", " ^ string_of_int shift ^ ")" | S.Identity -> "Identity" +and pp_ocaml_string_of_subst s = + let rec pp_ocaml_string_of_subst s i = + match s with + | S.Cons (l, s2) -> "Cons(" ^ string_of_lxp l ^ ",\n" + ^ (String.make (4 * i) ' ') ^ pp_ocaml_string_of_subst s2 (i + 1) ^ ")" + | S.Shift (s2, shift) -> "Shift(" ^ string_of_int shift ^ ",\n" + ^ (String.make (4 * i) ' ') ^ pp_ocaml_string_of_subst s2 (i + 1)^ ")" + | S.Identity -> "Identity" + in pp_ocaml_string_of_subst s 1 + and string_of_lxp lxp = match lxp with | Imm (Integer (_, value)) -> "Integer(" ^ (string_of_int value) ^ ")" @@ -51,9 +61,9 @@ and string_of_sort_level lvl = and string_of_sort sort = match sort with - | Stype lxp -> "Stype(" ^ string_of_lxp lxp ^ ")" - | StypeOmega -> "StypeOmega" - | StypeLevel -> "StypeLevel" + | Stype lxp -> "Stype(" ^ string_of_lxp lxp ^ ")" + | StypeOmega -> "StypeOmega" + | StypeLevel -> "StypeLevel" let colored_string_of_lxp lxp lcol vcol = match lxp with ===================================== src/inverse_subst.ml ===================================== --- a/src/inverse_subst.ml +++ b/src/inverse_subst.ml @@ -15,7 +15,7 @@ type inter_subst = lexp list (* Intermediate between "tree"-like substitution an (** Helper function that create a Cons(_, Shift(_)) *) (* let mkSubstNode var offset = S.Cons (var, S.Shift(S.Identity, offset)) *) -let dummy_var = Var((dummy_location, ""), -1) +let dummy_var = Var((dummy_location, "DummyVar"), -1) (** Transform a subst into a more linear 'intermdiate representation': @@ -32,8 +32,14 @@ let toIr (s: lexp S.subst) : inter_subst = | S.Cons(Var _ as v, s_1) -> Susp(v, (S.mkShift S.Identity last_offset))::(toIr s_1 last_offset) | S.Identity -> [Susp(dummy_var, (S.mkShift S.Identity last_offset ))] | _ -> assert false - (* Assuming that a Shift always follow Cons, the case Shift should never arise *) - in toIr s 0 + in let res = toIr s 0 + in Debug_fun.do_debug ( fun () -> + List.iter (fun i -> + print_string (Fmt_lexp.string_of_lxp i); print_string "::"; + match i with + | Susp _ -> assert true + | _ -> assert false) res; + print_newline(); print_newline(); ); res (** Transform an 'intermediate representation' into a sequence of cons followed by a shift @@ -46,12 +52,18 @@ let toIr (s: lexp S.subst) : inter_subst = let flattenIr (s: inter_subst): lexp S.subst option = let rec flattenCons s = match s with - | Susp (dv, S.Shift (S.Identity, o))::[] -> Some (o, S.Identity) + | Susp (_, S.Shift (S.Identity, o))::[] -> Some (o, S.Identity) + | Susp (_, S.Identity)::[] -> Some (0, S.Identity) | susp::tail -> (match flattenCons tail with | Some (o, s1) -> Some (o, (S.Cons (unsusp_all susp, s1))) | None -> None) | _ -> None - in match flattenCons s with + in Debug_fun.do_debug ( fun () -> + List.iter (fun i -> + match i with + | Susp _ -> assert true + | _ -> assert false) s); + match flattenCons s with | Some(offset, cons) -> Some(S.Shift(cons, offset)) | None -> None @@ -98,7 +110,7 @@ let rec nthOf s i = *) let idxOf (_, idx) = idx -(** Returns a list of couple (X, -1) where X go from beg_ to end_*) +(** Returns a list of couple (X, idx) where X go from beg_ to end_*) let rec genDummyVar beg_ end_ idx = if beg_ < end_ then (beg_, idx)::(genDummyVar (beg_ + 1) end_ idx) @@ -106,7 +118,7 @@ let rec genDummyVar beg_ end_ idx = (** Returns a dummy variable with the db_index idx *) -let mkVar idx = Var((U.dummy_location, ""), idx) (* not sure how to fill vdef *) +let mkVar idx = Var((U.dummy_location, ""), idx) (** Map a list of tuple to a sequence of S.Cons *) @@ -151,7 +163,10 @@ let fill l size acc = (** Take a "flattened" substitution and returns the inverse of the Cons *) -let generateCons s _size shift = generate_s (fill (genCons s 0) shift []) +let generateCons s _size shift = + let sort = List.sort (fun (ei1, _) (ei2, _) -> compare ei1 ei2) + in + generate_s (fill (sort (genCons s 0)) shift []) (** <code>s:S.subst -> l:lexp -> s':S.subst</code> where <code>l[s][s'] = l</code> Return undefined result for bad input @@ -162,4 +177,5 @@ let rec inverse (subst: lexp S.subst ) : lexp S.subst option = let size = sizeOf flattened in Some(S.Shift((generateCons flattened size shift), size)) | None -> None + | _ -> assert false ===================================== tests/inverse_test.ml ===================================== --- a/tests/inverse_test.ml +++ b/tests/inverse_test.ml @@ -30,15 +30,18 @@ let rec mkTestSubst lst = | [] -> S.Identity let input = - (mkTestSubst ((0, 3)::(2, 2)::(3, 5)::[])):: (* Seems to work *) - (mkTestSubst ((1, 3)::(2, 2)::(3, 5)::[])):: (* Seems to work *) - (mkTestSubst ((1, 3)::(2, 2)::(4, 5)::[])):: (* Seems to work *) - (mkTestSubst ((0, 3)::(2, 2)::(4, 5)::[])):: (* Seems to work *) - (mkTestSubst ((0, 3)::(1, 2)::(4, 5)::[])):: (* Seems to work *) + (mkTestSubst ((0, 3)::(2, 2)::(3, 5)::[])):: + (mkTestSubst ((1, 3)::(2, 2)::(3, 5)::[])):: + (mkTestSubst ((1, 3)::(2, 2)::(4, 5)::[])):: + (mkTestSubst ((0, 3)::(2, 2)::(4, 5)::[])):: + (mkTestSubst ((0, 3)::(1, 2)::(4, 5)::[])):: (mkTestSubst ((0, 3)::(1, 2)::(4, 1)::(5, 5)::[])):: (S.Cons (mkVar 1, S.Shift(S.Identity, 3))):: - (mkTestSubst ((4, 2)::(2, 2)::(3, 5)::[])):: (* Go completly wrong -> indices not in order -> should fail ?*) - (mkTestSubst ((1, 2)::(5, 2)::(3, 5)::[])):: (* Go completly wrong -> indices not in order -> should fail ?*) + (S.Cons (mkVar 1, S.Cons (mkVar 3, S.Identity))):: + (S.Shift (S.Shift (S.Identity, 3), 4)):: + (S.Shift (S.Cons (mkVar 1, S.Identity), 5)):: + (mkTestSubst ((4, 0)::(2, 2)::(3, 5)::[])):: + (mkTestSubst ((1, 2)::(5, 2)::(3, 5)::[])):: (mkTestSubst ((0, 3)::(1, 2)::(4, 1)::(9, 5)::[])):: (* Erroneous result -> normal ?*) [] @@ -81,8 +84,6 @@ let generate_tests (name: string) (test input_gen fmt tester) -(* let inputs = test_inverse input *) - let get_dim lst = let max i s = max i (String.length s) in @@ -129,7 +130,8 @@ let _ = generate_tests "INVERSION" let _ = generate_tests "TRANSFORMATION" (fun () -> input) (fun subst -> - let string_of_subst = ocaml_string_of_subst + let padding_right s d c = "\n" ^ s ^ "\n" + in let string_of_subst = pp_ocaml_string_of_subst in let subst = List.map (fun (s,fs) -> (string_of_subst s, string_of_subst fs)) subst in let get_dim lst = let max i s = max i (String.length s) @@ -138,6 +140,6 @@ let _ = generate_tests "TRANSFORMATION" in List.map (fun (s,sf) -> (padding_right s ds ' ') ^ " -> " ^ (padding_right sf dsf ' ')) subst) (fun subst -> match flatten subst with |Some s -> ((subst, (s)), true) - | None -> ((subst, subst), false)) + | None -> ((subst, S.Identity), false)) let _ = run_all () View it on GitLab: https://gitlab.com/monnier/typer/compare/629fa172c788c3bc0cf590f3c854955746…

1 0

[Git][monnier/typer][unification] 5 commits: better output for subst
by BONNEVALLE Vincent 21 Jul '16

21 Jul '16

BONNEVALLE Vincent pushed to branch unification at Stefan / Typer Commits: 2f8b27cf by n3f4s at 2016-07-21T21:36:56+02:00 better output for subst - - - - - 692dd5bb by n3f4s at 2016-07-21T21:38:01+02:00 change subst transformation algo - - - - - bf59e3c0 by n3f4s at 2016-07-21T21:38:58+02:00 re-indentation - - - - - 28a0a1d9 by n3f4s at 2016-07-21T21:39:13+02:00 add better testing - - - - - 629fa172 by n3f4s at 2016-07-21T23:54:36+02:00 better testing of inversion & tranformation - - - - - 5 changed files: - src/fmt_lexp.ml - src/inverse_subst.ml - src/unification.ml - tests/inverse_test.ml - tests/unify_test.ml Changes: ===================================== src/fmt_lexp.ml ===================================== --- a/src/fmt_lexp.ml +++ b/src/fmt_lexp.ml @@ -11,7 +11,20 @@ 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 rec string_of_lxp lxp = +let rec string_of_subst s = + match s with + | S.Cons (Var(_, idx), s2) -> "a" ^ string_of_int idx ^ " · " ^ string_of_subst s2 + | S.Cons (l, s2) -> string_of_lxp l ^ " · " ^ string_of_subst s2 + | S.Shift (s2, shift) -> "(" ^ string_of_subst s2 ^ ") ↑^" ^ string_of_int shift + | S.Identity -> "Id" + +and ocaml_string_of_subst s = + match s with + | S.Cons (l, s2) -> "Cons(" ^ string_of_lxp l ^ ", " ^ ocaml_string_of_subst s2 ^ ")" + | S.Shift (s2, shift) -> "Shift(" ^ ocaml_string_of_subst s2 ^ ", " ^ string_of_int shift ^ ")" + | S.Identity -> "Identity" + +and string_of_lxp lxp = match lxp with | Imm (Integer (_, value)) -> "Integer(" ^ (string_of_int value) ^ ")" | Imm (String (_, value)) -> "String(" ^ value ^ ")" @@ -28,7 +41,7 @@ let rec string_of_lxp lxp = | Sort (_, s) -> ("Sort") ^ "(" ^ string_of_sort s ^ ")" | SortLevel l -> ("SortLevel") ^ "(" ^ string_of_sort_level l ^ ")" | Case _ -> ("Case") ^ "(...)" - | Susp _ -> "Susp(...)" + | Susp (v, s) -> "Susp(" ^ (string_of_lxp v) ^ ", " ^ (string_of_subst s) ^ ")" | _ -> "Unidentified Lexp" and string_of_sort_level lvl = @@ -64,25 +77,18 @@ let colored_string_of_lxp lxp lcol vcol = | _ -> (lcol "Unidentified Lexp") let padding_right (str: string ) (dim: int ) (char_: char) : string = - let diff = (dim - String.length str) + 5 - in let rpad = diff + let diff = (dim - String.length str) + in let rpad = max diff 0 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 + let diff = (dim - String.length str) + in let lpad = max diff 0 in (String.make lpad char_) ^ str let center (str: string ) (dim: int ) (char_: char) : string = - let diff = (dim - String.length str) + 5 + let diff = max (dim - String.length str) 0 in let lpad, rpad = ((diff / 2 ), ((diff / 2) + (diff mod 2))) in (String.make lpad char_) ^ str ^ (String.make lpad char_) -let rec string_of_subst s = - match s with - | S.Cons (Var(_, idx), s2) -> "a" ^ string_of_int idx ^ " · " ^ string_of_subst s2 - | S.Cons (l, s2) -> string_of_lxp l ^ " · " ^ string_of_subst s2 - | S.Shift (s2, shift) -> "(" ^ string_of_subst s2 ^ ") ↑^" ^ string_of_int shift - | S.Identity -> "Id" - ===================================== src/inverse_subst.ml ===================================== --- a/src/inverse_subst.ml +++ b/src/inverse_subst.ml @@ -1,5 +1,6 @@ open Lexp +open Util module S = Subst (** Provide inverse function for computing the inverse of a substitution @@ -8,10 +9,13 @@ module S = Subst (* Transformation *) (** a_0 . ↑^x1 (a_2 . ↑x2 ... ) . ↑^xn . id*) -type inter_subst = lexp S.subst list (* Intermediate between "tree"-like substitution and fully flattened subsitution *) +(* type inter_subst = lexp S.subst list (* Intermediate between "tree"-like substitution and fully flattened subsitution *) *) +type inter_subst = lexp list (* Intermediate between "tree"-like substitution and fully flattened subsitution *) (** Helper function that create a Cons(_, Shift(_)) *) -let mkSubstNode var offset = S.Cons (var, S.Shift(S.Identity, offset)) +(* let mkSubstNode var offset = S.Cons (var, S.Shift(S.Identity, offset)) *) + +let dummy_var = Var((dummy_location, ""), -1) (** Transform a subst into a more linear 'intermdiate representation': @@ -24,9 +28,10 @@ let mkSubstNode var offset = S.Cons (var, S.Shift(S.Identity, offset)) let toIr (s: lexp S.subst) : inter_subst = let rec toIr s last_offset = match s with - | S.Cons(Var _ as v, S.Shift (s_1, offset)) -> - (mkSubstNode v last_offset)::(toIr s_1 offset) - | S.Identity -> [S.Shift (S.Identity, last_offset )] + | S.Shift (s_1, offset) -> toIr s_1 (last_offset + offset) + | S.Cons(Var _ as v, s_1) -> Susp(v, (S.mkShift S.Identity last_offset))::(toIr s_1 last_offset) + | S.Identity -> [Susp(dummy_var, (S.mkShift S.Identity last_offset ))] + | _ -> assert false (* Assuming that a Shift always follow Cons, the case Shift should never arise *) in toIr s 0 @@ -38,15 +43,14 @@ let toIr (s: lexp S.subst) : inter_subst = - <code>S.Cons(var, S.Shift(S.Identity, offset))::...::Identity -> S.Shift(S.Cons(var, S.Cons(...)), x1+x2+x3...)</code> *) -let flattenIr (s: inter_subst) = +let flattenIr (s: inter_subst): lexp S.subst option = let rec flattenCons s = match s with - | S.Cons(Var _ as v, S.Shift(S.Identity, offset))::tail -> - (match flattenCons tail with - | Some (o, s1) -> Some (o + offset, S.Cons(v, s1)) - | None -> None) - | (S.Shift(S.Identity, o))::[] -> Some (o, S.Identity) - | [] -> None + | Susp (dv, S.Shift (S.Identity, o))::[] -> Some (o, S.Identity) + | susp::tail -> (match flattenCons tail with + | Some (o, s1) -> Some (o, (S.Cons (unsusp_all susp, s1))) + | None -> None) + | _ -> None in match flattenCons s with | Some(offset, cons) -> Some(S.Shift(cons, offset)) | None -> None @@ -118,6 +122,7 @@ let rec genCons s i = match s with | S.Cons(Var(v), s1) -> ((idxOf v), i)::(genCons s1 (i + 1)) (* e_{idx_of v} = i *) | S.Identity -> [] + | _ -> assert false (* With the exemple of the article : should return <code>(1,1)::(2, X)::(3,2)::(4,3)::(5, Z)::[]</code> ===================================== src/unification.ml ===================================== --- a/src/unification.ml +++ b/src/unification.ml @@ -11,7 +11,7 @@ type constraints = (lexp * lexp) list (** Provide unify function for unifying two Lambda-Expression *) (* IMPROVEMENT For error handling : can carry location and name of type error *) -(*type 'a result =*) +(*type 'a result =*) (* use std result type*) (*| Some of 'a*) (*| Error of Util.location * string (*location * type name*)*) (*| Nil*) ===================================== tests/inverse_test.ml ===================================== --- a/tests/inverse_test.ml +++ b/tests/inverse_test.ml @@ -29,56 +29,80 @@ let rec mkTestSubst lst = mkShift2 shift (mkTestSubst tail)) | [] -> S.Identity -(* FIXME : tests fail but yield a seemingly good result *) -(* FIXME : is a_0 ... a_p ↑^n when p > n an error case ? *) -(* TODO : Generate random input *) let input = - (mkTestSubst ((0, 3)::(2, 2)::(3, 0)::[])):: (* Seems to work *) - (mkTestSubst ((1, 3)::(2, 2)::(3, 0)::[])):: (* Seems to work *) - (mkTestSubst ((4, 2)::(2, 2)::(3, 0)::[])):: (* Go completly wrong -> indices not in order -> should fail ?*) - (mkTestSubst ((1, 2)::(5, 2)::(3, 0)::[])):: (* Go completly wrong -> indices not in order -> should fail ?*) - (mkTestSubst ((1, 3)::(2, 2)::(4, 0)::[])):: (* Seems to work *) - (mkTestSubst ((0, 3)::(2, 2)::(4, 0)::[])):: (* Seems to work *) - (mkTestSubst ((0, 3)::(1, 2)::(4, 0)::[])):: (* Seems to work *) - (mkTestSubst ((0, 3)::(1, 2)::(4, 1)::(5, 0)::[])):: - (mkTestSubst ((0, 3)::(1, 2)::(4, 1)::(9, 0)::[])):: (* Erroneous result -> normal ?*) + (mkTestSubst ((0, 3)::(2, 2)::(3, 5)::[])):: (* Seems to work *) + (mkTestSubst ((1, 3)::(2, 2)::(3, 5)::[])):: (* Seems to work *) + (mkTestSubst ((1, 3)::(2, 2)::(4, 5)::[])):: (* Seems to work *) + (mkTestSubst ((0, 3)::(2, 2)::(4, 5)::[])):: (* Seems to work *) + (mkTestSubst ((0, 3)::(1, 2)::(4, 5)::[])):: (* Seems to work *) + (mkTestSubst ((0, 3)::(1, 2)::(4, 1)::(5, 5)::[])):: (S.Cons (mkVar 1, S.Shift(S.Identity, 3))):: + (mkTestSubst ((4, 2)::(2, 2)::(3, 5)::[])):: (* Go completly wrong -> indices not in order -> should fail ?*) + (mkTestSubst ((1, 2)::(5, 2)::(3, 5)::[])):: (* Go completly wrong -> indices not in order -> should fail ?*) + (mkTestSubst ((0, 3)::(1, 2)::(4, 1)::(9, 5)::[])):: (* Erroneous result -> normal ?*) [] let generateRandInput n m = Random.self_init (); let rec generateList n m = - let rec generateRandInput n i = - if n > i - then (if Random.bool () - then ( let r = Random.int n in - (i, (min (r + i) n))::(generateRandInput n (i + 1)) ) - else generateRandInput n (i + 1)) - else [] - in if m >= 0 - then (mkTestSubst (generateRandInput n 0))::(generateList n (m - 1)) + let rec generateRandInput n i = + if n > i + then (if Random.bool () + then ( let r = Random.int n in + (i, (min (r + i) n))::(generateRandInput n (i + 1)) ) + else generateRandInput n (i + 1)) else [] + in if m >= 0 + then (mkTestSubst (generateRandInput n 0))::(generateList n (m - 1)) + else [] in generateList n m let lxp = mkVar 3 -let test input = List.map (fun s -> - match inverse s, flatten s with - | Some(s'), Some(sf) -> (let comp = scompose sf s' in - let ret = (match comp with - | S.Identity -> true - | _ -> false) - in let str = ( - (string_of_subst s), - (string_of_subst sf), - (string_of_subst s'), - (string_of_subst comp)) - in (ret, str)) - | _ -> (false, (string_of_subst s, string_of_subst S.Identity,string_of_subst S.Identity, string_of_subst S.Identity))) - input +let test + (input_gen: (unit -> 'a list)) + (fmt: 'b list -> string list) + (tester: 'a -> ('b * bool)): (string * bool) list = + let input = List.map tester (input_gen ()) + in let str = List.map (fun (s, _) -> s ) input + in let b = List.map (fun (_, b) -> b) input + in List.combine (fmt str) b + +let generate_tests (name: string) + (input_gen: (unit -> 'a list)) + (fmt: 'b list -> string list) + (tester: 'a -> ('b * bool)) = + let idx = (ref 0) + in List.map (fun (sub, res) -> + idx := !idx + 1; + add_test name + ((padding_left (string_of_int (!idx)) 2 '0') ^ " - " ^ sub) + (fun () -> if res then success () else failure ())) + (test input_gen fmt tester) + + +(* let inputs = test_inverse input *) +let get_dim lst = + let max i s = max i (String.length s) + in + List.fold_left + (fun (acs, acsf, acs', acc) (s, sf, s', comp) -> ((max acs s), (max acsf sf), (max acs' s'), (max acc comp))) + (0,0,0,0) + lst + +let fmt_res str = + let (ds, dsf, ds', dcomp) = get_dim str + in List.map (fun (s, sf, s', com) -> "[ " ^ + (padding_right s ds ' ') ^ " -> " ^ + (padding_right (sf ^ " ]") dsf ' ') ^ " ∘ " ^ + (padding_right s' ds' ' ') ^ " = " ^ + (padding_right com dcomp ' ') + ) str -let inputs = test input +(* let string_of_subst = ocaml_string_of_subst *) +(* let fmt_res str = *) +(* List.map (fun (_, sf, s', com) -> sf ^ " ∘ " ^ s' ^ " = " ^ com ) str *) let get_dim lst = let max i s = max i (String.length s) @@ -88,37 +112,32 @@ let get_dim lst = (0,0,0,0) lst -let fmt_res lst = - let str = List.map (fun (_, s) -> s) lst - and res = List.map (fun (r, _) -> r) lst - in - let (ds, dsf, ds', dcomp) = get_dim str - in let str' = List.map (fun (s, sf, s', com) -> "[ " ^ - (padding_right s ds ' ') ^ " -> " ^ - (padding_right (sf ^ " ]") dsf ' ') ^ " ∘ " ^ - (padding_right s' ds' ' ') ^ " = " ^ - (padding_right com dcomp ' ') - ) str - in match zip res str' with - | None -> [] - | Some (s) -> s - -let fmt_res2 lst = - let str = List.map (fun (_, s) -> s) lst - and res = List.map (fun (r, _) -> r) lst - in let str' = List.map (fun (s, sf, s', com) -> - sf ^ " ∘ " ^ s' - ) str - in match zip res str' with - | None -> [] - | Some (s) -> s - -let fmt_inputs = fmt_res inputs - -let _ = List.map (fun (res, str) -> add_test "INVERSE" str (fun () -> if res then success () else failure ())) - fmt_inputs - -let _ = List.map (fun (res, str) -> add_test "INVERSE (RAND)" str (fun () -> if res then success () else failure ())) - (fmt_res2 (test (generateRandInput 5 15))) +let _ = generate_tests "INVERSION" + (fun () -> input) + fmt_res + (fun s -> ( match inverse s, flatten s with + | Some (s'), Some (sf) -> (let comp = scompose sf s' in + let ret = (match comp with + | S.Identity -> true + | _ -> false) + in let str = ((string_of_subst s), (string_of_subst sf), (string_of_subst s'), (string_of_subst comp)) + in (str, ret)) + | _ -> ((string_of_subst s, string_of_subst S.Identity, string_of_subst S.Identity, string_of_subst S.Identity), + false )) + ) + +let _ = generate_tests "TRANSFORMATION" + (fun () -> input) + (fun subst -> + let string_of_subst = ocaml_string_of_subst + in let subst = List.map (fun (s,fs) -> (string_of_subst s, string_of_subst fs)) subst + in let get_dim lst = + let max i s = max i (String.length s) + in List.fold_left (fun (acs, acsf) (s, sf) -> ((max acs s), (max acsf sf))) (0,0) lst + in let (ds, dsf) = get_dim subst + in List.map (fun (s,sf) -> (padding_right s ds ' ') ^ " -> " ^ (padding_right sf dsf ' ')) subst) + (fun subst -> match flatten subst with + |Some s -> ((subst, (s)), true) + | None -> ((subst, subst), false)) let _ = run_all () ===================================== tests/unify_test.ml ===================================== --- a/tests/unify_test.ml +++ b/tests/unify_test.ml @@ -52,9 +52,9 @@ let fmt (lst: (lexp * lexp * result * result) list): string list = 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 View it on GitLab: https://gitlab.com/monnier/typer/compare/0461e108945d89232822e1b44a244765c7…

1 0

[Git][monnier/typer][unification] 2 commits: Dummy variable have index shift+1 instead of -1
by BONNEVALLE Vincent 20 Jul '16

20 Jul '16

BONNEVALLE Vincent pushed to branch unification at Stefan / Typer Commits: 37f21f32 by n3f4s at 2016-07-20T16:58:41+02:00 Dummy variable have index shift+1 instead of -1 - - - - - 0461e108 by n3f4s at 2016-07-20T17:01:45+02:00 add generation of random test - - - - - 2 changed files: - src/inverse_subst.ml - tests/inverse_test.ml Changes: ===================================== src/inverse_subst.ml ===================================== --- a/src/inverse_subst.ml +++ b/src/inverse_subst.ml @@ -2,11 +2,6 @@ open Lexp module S = Subst -(* FIXME : fail when the inversion have to create the first variable - i.e. : a1 · ↑3 -> a-1 · a0 · ↑^1 (expected result) - -> a-1 · a0 · ↑^1 (current result) -*) - (** Provide inverse function for computing the inverse of a substitution *) @@ -41,7 +36,7 @@ let toIr (s: lexp S.subst) : inter_subst = or in ocaml-ish representation : - - S.Cons(var, S.Shift(S.Identity, offset))::...::Identity -> S.Shift(S.Cons(var, S.Cons(...)), x1+x2+x3...) + - <code>S.Cons(var, S.Shift(S.Identity, offset))::...::Identity -> S.Shift(S.Cons(var, S.Cons(...)), x1+x2+x3...)</code> *) let flattenIr (s: inter_subst) = let rec flattenCons s = @@ -62,7 +57,7 @@ let flattenIr (s: inter_subst) = or in ocaml-ish representation : - - S.Cons(var, S.Shift(..., offset)) -> S.Shift(S.Cons(var, S.Cons(...)), x1+x2+x3...) + - <code>S.Cons(var, S.Shift(..., offset)) -> S.Shift(S.Cons(var, S.Cons(...)), x1+x2+x3...)</code> *) let flatten (s: lexp S.subst) = flattenIr (toIr s) @@ -100,9 +95,9 @@ let rec nthOf s i = let idxOf (_, idx) = idx (** Returns a list of couple (X, -1) where X go from beg_ to end_*) -let rec genDummyVar beg_ end_ = +let rec genDummyVar beg_ end_ idx = if beg_ < end_ - then (beg_, -1)::(genDummyVar (beg_ + 1) end_) + then (beg_, idx)::(genDummyVar (beg_ + 1) end_ idx) else [] (** Returns a dummy variable with the db_index idx @@ -117,7 +112,7 @@ let rec generate_s l = | [] -> S.Identity (* With the exemple of the article : - should return (1,1)::(3,2)::(4,3)::[] + should return <code>(1,1)::(3,2)::(4,3)::[]</code> *) let rec genCons s i = match s with @@ -125,9 +120,11 @@ let rec genCons s i = | S.Identity -> [] (* With the exemple of the article : - should return (1,1)::(2, X)::(3,2)::(4,3)::(5, Z)::[] + should return <code>(1,1)::(2, X)::(3,2)::(4,3)::(5, Z)::[]</code> *) let fill l size acc = + let genDummyVar beg_ end_ = genDummyVar beg_ end_ (size + 1) + in let rec fill_before l = match l with | [] -> [] @@ -151,7 +148,9 @@ let fill l size acc = *) let generateCons s _size shift = generate_s (fill (genCons s 0) shift []) -(** s:S.subst -> l:lexp -> s':S.subst where l[s][s'] = l *) +(** <code>s:S.subst -> l:lexp -> s':S.subst</code> where <code>l[s][s'] = l</code> + Return undefined result for bad input +*) let rec inverse (subst: lexp S.subst ) : lexp S.subst option = match flatten subst with | Some(S.Shift(flattened, shift)) -> ===================================== tests/inverse_test.ml ===================================== --- a/tests/inverse_test.ml +++ b/tests/inverse_test.ml @@ -29,33 +29,96 @@ let rec mkTestSubst lst = mkShift2 shift (mkTestSubst tail)) | [] -> S.Identity +(* FIXME : tests fail but yield a seemingly good result *) +(* FIXME : is a_0 ... a_p ↑^n when p > n an error case ? *) +(* TODO : Generate random input *) let input = (mkTestSubst ((0, 3)::(2, 2)::(3, 0)::[])):: (* Seems to work *) (mkTestSubst ((1, 3)::(2, 2)::(3, 0)::[])):: (* Seems to work *) (mkTestSubst ((4, 2)::(2, 2)::(3, 0)::[])):: (* Go completly wrong -> indices not in order -> should fail ?*) + (mkTestSubst ((1, 2)::(5, 2)::(3, 0)::[])):: (* Go completly wrong -> indices not in order -> should fail ?*) (mkTestSubst ((1, 3)::(2, 2)::(4, 0)::[])):: (* Seems to work *) (mkTestSubst ((0, 3)::(2, 2)::(4, 0)::[])):: (* Seems to work *) (mkTestSubst ((0, 3)::(1, 2)::(4, 0)::[])):: (* Seems to work *) (mkTestSubst ((0, 3)::(1, 2)::(4, 1)::(5, 0)::[])):: - (mkTestSubst ((0, 3)::(1, 2)::(4, 1)::(5, 0)::[])):: + (mkTestSubst ((0, 3)::(1, 2)::(4, 1)::(9, 0)::[])):: (* Erroneous result -> normal ?*) (S.Cons (mkVar 1, S.Shift(S.Identity, 3))):: [] +let generateRandInput n m = + Random.self_init (); + let rec generateList n m = + let rec generateRandInput n i = + if n > i + then (if Random.bool () + then ( let r = Random.int n in + (i, (min (r + i) n))::(generateRandInput n (i + 1)) ) + else generateRandInput n (i + 1)) + else [] + in if m >= 0 + then (mkTestSubst (generateRandInput n 0))::(generateList n (m - 1)) + else [] + in generateList n m + let lxp = mkVar 3 -let inputs = List.map (fun s -> +let test input = List.map (fun s -> match inverse s, flatten s with - | Some(s'), Some(sf) -> (let lxp_inv = mkSusp lxp s' - in let ret = (match unify lxp lxp_inv empty_subst with - | Some (_) -> true - | _ -> false) - in let str = (string_of_subst sf) ^ (String.make (50 - String.length (string_of_subst sf)) ' ') - ^ " -> " ^ (string_of_subst s') - in (ret, str)) - | _ -> (false, ((string_of_subst s) ^ " -> Non inversable"))) + | Some(s'), Some(sf) -> (let comp = scompose sf s' in + let ret = (match comp with + | S.Identity -> true + | _ -> false) + in let str = ( + (string_of_subst s), + (string_of_subst sf), + (string_of_subst s'), + (string_of_subst comp)) + in (ret, str)) + | _ -> (false, (string_of_subst s, string_of_subst S.Identity,string_of_subst S.Identity, string_of_subst S.Identity))) input + +let inputs = test input + +let get_dim lst = + let max i s = max i (String.length s) + in + List.fold_left + (fun (acs, acsf, acs', acc) (s, sf, s', comp) -> ((max acs s), (max acsf sf), (max acs' s'), (max acc comp))) + (0,0,0,0) + lst + +let fmt_res lst = + let str = List.map (fun (_, s) -> s) lst + and res = List.map (fun (r, _) -> r) lst + in + let (ds, dsf, ds', dcomp) = get_dim str + in let str' = List.map (fun (s, sf, s', com) -> "[ " ^ + (padding_right s ds ' ') ^ " -> " ^ + (padding_right (sf ^ " ]") dsf ' ') ^ " ∘ " ^ + (padding_right s' ds' ' ') ^ " = " ^ + (padding_right com dcomp ' ') + ) str + in match zip res str' with + | None -> [] + | Some (s) -> s + +let fmt_res2 lst = + let str = List.map (fun (_, s) -> s) lst + and res = List.map (fun (r, _) -> r) lst + in let str' = List.map (fun (s, sf, s', com) -> + sf ^ " ∘ " ^ s' + ) str + in match zip res str' with + | None -> [] + | Some (s) -> s + +let fmt_inputs = fmt_res inputs + let _ = List.map (fun (res, str) -> add_test "INVERSE" str (fun () -> if res then success () else failure ())) - inputs + fmt_inputs + +let _ = List.map (fun (res, str) -> add_test "INVERSE (RAND)" str (fun () -> if res then success () else failure ())) + (fmt_res2 (test (generateRandInput 5 15))) let _ = run_all () View it on GitLab: https://gitlab.com/monnier/typer/compare/27fc552db4dc7ccc9c0a3f3cea5e3e9f5f…

1 0

2024

2023

2022

2021

2020

2019

2018

2017

2016

Typer Juillet 2016