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/0461e108945d89232822e1b44a244765c7c...