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/629fa172c788c3bc0cf590f3c854955746a...