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/4282321b68032b4ecc2496164905fcadc50...