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/65bbe6d12d2c516eeccd061436c50dae129...