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/27fc552db4dc7ccc9c0a3f3cea5e3e9f5f1...