BONNEVALLE Vincent pushed to branch unification at Stefan / Typer

Commits: 79f26644 by n3f4s at 2016-07-28T23:28:58+02:00 fix non termination of test

- - - - - 2a02a1fb by n3f4s at 2016-07-28T23:48:06+02:00 add metavar in lexp_p_infer for default case

- - - - - ec33b98a by n3f4s at 2016-07-28T23:49:49+02:00 remove padding for random test

- - - - - 3b5313eb by n3f4s at 2016-07-28T23:50:48+02:00 add test for type checking

- - - - - 42608955 by n3f4s at 2016-07-29T18:22:00+02:00 debug inversion for Id ↑^X

- - - - - 05af83ee by n3f4s at 2016-07-29T20:44:49+02:00 begining of adding unification in type check

- - - - - 5d99315b by n3f4s at 2016-07-29T21:16:28+02:00 try to remove iteration

- - - - - a0b5b8d0 by n3f4s at 2016-07-29T21:23:55+02:00 fix transformation : change shift value in transfo

merge toIr, flattenIr and to_list in transfo

- - - - - 7798134b by n3f4s at 2016-07-29T21:47:14+02:00 add check for deBruijn indices >= shift offset

- - - - - 5acc8450 by n3f4s at 2016-07-29T21:48:22+02:00 remove useless code

- - - - - 946063a6 by n3f4s at 2016-07-29T21:48:36+02:00 adapt tests

- - - - - 8b249028 by n3f4s at 2016-07-29T23:18:37+02:00 merge fill with to_cons

- - - - - 304245b6 by n3f4s at 2016-07-29T23:20:23+02:00 remove useless code

- - - - -

5 changed files:

- src/inverse_subst.ml - src/lparse.ml - src/unification.ml - tests/inverse_test.ml - + tests/lparse_test.ml

Changes:

===================================== src/inverse_subst.ml ===================================== --- a/src/inverse_subst.ml +++ b/src/inverse_subst.ml @@ -12,74 +12,28 @@ type inter_subst = lexp list (* Intermediate between "tree"-like substitution an

let dummy_var = Var((dummy_location, "DummyVar"), -1)

-(** Transform a subst into a more linear 'intermediate representation': - - - a₁ · ↑n₁ (a₂ · ↑n₂ (a₃ · ↑n₃ id)) - ⇒ a₁' · a₂' · a₃' · ↑n₃ id - - or in ocaml-ish representation : - - - S.Cons(var, S.Shift(..., offset)) - ⇒ S.Cons(var, S.Shift(S.Identity, offset))::...::Identity -*) -let toIr (s: lexp S.subst) : inter_subst = - let rec toIr s total_offset = - match s with - | S.Shift (s_1, offset) -> toIr s_1 (total_offset + offset) - (* FIXME: A Cons with something else than a Var is not an error. - * It might mean that we can't invert this substitution, but that's - * no justification for "assert false". *) - | S.Cons(Var _ as v, s_1) - (* FIXME: Why not L.mkSusp? *) - -> Susp (v, S.shift total_offset)::(toIr s_1 total_offset) - | S.Identity -> [Susp (dummy_var, S.shift total_offset)] - | _ -> assert false - 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.(id ↑^{x1+x2+x3}) - - or in ocaml-ish representation : - - - <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 = - match s with - | Susp (_dummy_var, s)::[] -> Some s - | susp::tail -> (match flattenCons tail with - | Some (s1) -> Some (S.cons (nosusp susp) s1) - | None -> None) - | _ -> None - in flattenCons s - -(** Flatten a "tree"-like substitution: - - - a1.↑^{x1}(a2.↑^{x2}(a3.↑^{x3}id)) -> a1.(↑^{x1}a2).(↑^{x2}a3).↑^{x3}id -> a1.a2.a3 ↑^{x1+x2+x3} - - or in ocaml-ish representation : - - - <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): 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 - +type substIR = ((int * int) list * int) + +(* toIr + flattenIr + to_list *) +(* TODO : find better name ?*) +let transfo (s: lexp S.subst) : substIR option = + let rec transfo (s: lexp S.subst) (off_acc: int) (idx: int): substIR option = + let valueOf (v: lexp): int = + match v with + | Var (_, v) -> v + | _ -> assert false + in let shiftVar (var: lexp) (offset: int): int = valueOf (mkSusp var (S.shift offset)) + in match s with + | S.Cons (Var _ as v, s) -> + (match transfo s off_acc (idx + 1) with + | Some (tail, off) -> let newVar = shiftVar v off_acc + in if newVar >= off then None + else Some (((shiftVar v off_acc), idx)::tail, off) + | None -> None) + | S.Shift (s, offset) -> transfo s (offset + off_acc) idx + | S.Identity -> Some ([], off_acc) + | _ -> None + in transfo s 0 0

(* Inverse *)

@@ -87,16 +41,6 @@ let flatten (s: lexp S.subst): lexp S.subst option = *) 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_: 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: int): lexp = Var((U.dummy_location, ""), idx) @@ -110,67 +54,51 @@ 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 option = - let genDummyVar beg_ end_ = genDummyVar beg_ end_ (size + 1) +let fill (l: (int * int) list) (nbVar: int) (shift: int): lexp S.subst option = + let rec genDummyVar (beg_: int) (end_: int) (l: lexp S.subst): lexp S.subst = + if beg_ < end_ + then S.cons (mkVar (nbVar + 1)) (genDummyVar (beg_ + 1) end_ l) + else l in - let rec fill_before (l: (int * int) list): (int * int) list = + let fill_before (l: (int * int) list) (s: lexp S.subst) (nbVar: int): lexp S.subst option = match l with - | [] -> [] - | (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 option = + | [] -> Some (genDummyVar 0 nbVar S.identity) + | (i1, v1)::_ when i1 > 0 -> Some (genDummyVar 0 i1 s) + | _ -> Some s + in let rec fill_after (l: (int * int) list) (nbVar: int) (shift: int): lexp S.subst 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 - then (acc@[(idx1, val1)]@(genDummyVar (idx1 + 1) idx2)) - else (acc@(idx1, val1)::[]) - in fill_after tail size accu - | (idx1, val1)::[] -> if (idx1 + 1) < size - 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 - in the debuijn index sequence -*) -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 - -(** 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 (S.shift shift) + | (idx1, val1)::(idx2, val2)::tail when (idx1 = idx2) -> None + + | (idx1, val1)::(idx2, val2)::tail when (idx2 - idx1) > 1 -> + (match fill_after ((idx2, val2)::tail) nbVar shift with + | None -> None + | Some s -> Some (S.cons (mkVar val1) (genDummyVar (idx1 + 1) idx2 s))) + + | (idx1, val1)::(idx2, val2)::tail -> + (match fill_after ((idx2, val2)::tail) nbVar shift with + | None -> None + | Some s -> Some (S.cons (mkVar val1) s)) + + | (idx1, val1)::[] when (idx1 + 1) < nbVar -> + Some (S.cons (mkVar val1) (genDummyVar (idx1 + 1) nbVar (S.shift shift))) + + | (idx1, val1)::[] -> + Some (S.cons (mkVar val1) (S.shift shift)) + + | [] -> + Some (S.shift shift) + in match fill_after l nbVar shift with + | None -> None + | Some s -> fill_before l s nbVar

(** 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 inverse (s: lexp S.subst) : lexp S.subst option = let sort = List.sort (fun (ei1, _) (ei2, _) -> compare ei1 ei2) - in - match flatten subst with - | None -> None - | Some (s) -> - let cons_lst, shift_val = to_list s - in let size = sizeOf cons_lst - in match fill (sort cons_lst) shift_val [] with - | None -> None - | Some cons_lst -> to_cons cons_lst size - + in match transfo s with + | None -> None + | Some (cons_lst, shift_val) -> + let size = sizeOf cons_lst + in fill (sort cons_lst) shift_val size

===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -48,6 +48,8 @@ open Eval open Grammar open Builtin

+module Unif = Unification + module TC = Typecheck module EL = Elexp module SU = Subst @@ -274,8 +276,9 @@ and _lexp_p_infer (p : pexp) (ctx : lexp_context) i: lexp * ltype = let ltp, _ = lexp_infer ptp ctx in (_lexp_p_check pxp ltp ctx (i + 1)), ltp

- | _ -> pexp_print p; print_string "\n"; - lexp_fatal tloc "Unhandled Pexp" + (*FIXME right thing to do*) + | _ -> let meta = Unif.mkMetavar S.Identity (Util.dummy_location, "") (*???*) + in (meta, lexp_p_check p meta ctx)

and lexp_let_decls decls (body: lexp) ctx i = @@ -287,6 +290,8 @@ and lexp_let_decls decls (body: lexp) ctx i = and lexp_p_check (p : pexp) (t : ltype) (ctx : lexp_context): lexp = _lexp_p_check p t ctx 1

+(*TODO : - add substitution parameter for unification + - try to unify in default case *) and _lexp_p_check (p : pexp) (t : ltype) (ctx : lexp_context) i: lexp = let tloc = pexp_location p in

@@ -312,18 +317,21 @@ and _lexp_p_check (p : pexp) (t : ltype) (ctx : lexp_context) i: lexp = lxp

| _ -> let (e, inferred_t) = _lexp_p_infer p ctx (i + 1) in - e (* + (* e *) match e with (* Built-in is a dummy function with no type. We cannot check * Built-in *) | Builtin _ -> e | _ -> - (if TC.conv_p inferred_t t then () else debug_msg ( + (* (if TC.conv_p inferred_t t then () else debug_msg ( *) + (match Unif.unify inferred_t t Unif.empty_subst with + | Some _ -> () + | None -> debug_msg ( print_string "1 exp "; lexp_print e; print_string "\n"; print_string "2 inf "; lexp_print inferred_t; print_string "\n"; print_string "3 Ann "; lexp_print t; print_string "\n"; lexp_warning tloc "Type Mismatch inferred != Annotation")); - e*) + e

(* Lexp.case cam be checked and inferred *) and lexp_case (rtype: lexp option) (loc, target, patterns) ctx i =

===================================== src/unification.ml ===================================== --- a/src/unification.ml +++ b/src/unification.ml @@ -22,8 +22,9 @@ type constraints = (lexp * lexp) list (*| Error _ -> None*) (*| Nil -> None*)

-let global_last_metavar = ref 0 -let create_metavar = global_last_metavar := !global_last_metavar + 1; !global_last_metavar +let global_last_metavar = ref (-1) (*The first metavar is 0*) +let create_metavar () = global_last_metavar := !global_last_metavar + 1; !global_last_metavar +let mkMetavar subst vdef = Metavar (create_metavar (), subst, vdef)

(* For convenience *) type return_type = (substitution * constraints) option

===================================== tests/inverse_test.ml ===================================== --- a/tests/inverse_test.ml +++ b/tests/inverse_test.ml @@ -29,27 +29,22 @@ 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)::[])), 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 3)), Ok):: - ((S.cons (mkVar 1) (S.cons (mkVar 3) (S.identity))), TransfoFail):: - ((S.mkShift (S.shift 3) 4), Ok):: - ((S.mkShift (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):: + ((mkTestSubst ((0, 3)::(2, 2)::(3, 5)::[])), true):: + ((mkTestSubst ((1, 3)::(2, 2)::(3, 5)::[])), true):: + ((mkTestSubst ((1, 3)::(2, 2)::(4, 5)::[])), true):: + ((mkTestSubst ((0, 3)::(2, 2)::(4, 5)::[])), true):: + ((mkTestSubst ((0, 3)::(1, 2)::(4, 5)::[])), true):: + ((mkTestSubst ((0, 3)::(1, 2)::(4, 1)::(5, 5)::[])), false):: + ((S.cons (mkVar 1) (S.shift 3)), true):: + ((S.cons (mkVar 1) (S.cons (mkVar 3) (S.identity))), false):: + ((S.mkShift (S.shift 3) 4), true):: + ((S.mkShift (S.cons (mkVar 1) (S.identity)) 5), false):: + ((mkTestSubst ((4, 0)::(2, 2)::(3, 5)::[])), true):: + ((mkTestSubst ((1, 2)::(5, 1)::(3, 5)::[])), true):: + ((mkTestSubst ((1, 2)::(5, 2)::(3, 5)::[])), false):: + ((mkTestSubst ((0, 3)::(1, 2)::(4, 1)::(9, 5)::[])), false):: []

let is_identity s = @@ -106,83 +101,53 @@ 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) + (fun (acs, acs', acc) (s, s', comp) -> ((max acs s), (max acs' s'), (max acc comp))) + (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' ' ') ^ " = " ^ - (com) + let (ds, ds', dcomp) = get_dim str + in List.map (fun (s, s', com) -> (padding_right s ds ' ') ^ " -> " ^ + (padding_right s' ds' ' ') ^ " = " ^ + (com) ) str

-(* 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) 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) + (fun (acs, acs', acc) (s, s', comp) -> ((max acs s), (max acs' s'), (max acc comp))) + (0,0,0) lst

+ let _ = generate_tests "INVERSION" (fun () -> input) fmt_res - (fun (s, b) -> ( match inverse s, flatten s with - | Some (s'), Some (sf) -> (let comp = scompose sf s' in - 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"),(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))) + (fun (s, b) -> ( match inverse s with + | Some (s') -> (let comp = scompose s s' in + let ret = (is_identity comp) + in let str = ((string_of_subst s), (string_of_subst s'), (string_of_subst comp)) + in (str, ret)) + | None -> ((string_of_subst s, "None", "None"), not b) + ) )

+let fmt_res str = + List.map (fun (s, s', com) -> (s) ^ " -> " ^ + (s') ^ " = " ^ + (com) ) str + (* TODO find a better way to check test*) let _ = generate_tests "INVERSION-RAND" (fun () -> generateRandInput 5 10) fmt_res - (fun (s) -> ( match inverse s, flatten s with - | Some (s'), Some (sf) -> (let comp = scompose sf s' in - let ret = (is_identity comp) - 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) + (fun (s) -> ( match inverse s with + | Some (s') -> (let comp = scompose s s' in + let ret = (is_identity comp) + in let str = ((string_of_subst s), (string_of_subst s'), (string_of_subst comp)) + in (str, ret)) + | None -> ((string_of_subst s , "None" , "None") , false) ))

-let _ = generate_tests "TRANSFORMATION" - (fun () -> input) - (fun 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) - 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, 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 ()

===================================== tests/lparse_test.ml ===================================== --- /dev/null +++ b/tests/lparse_test.ml @@ -0,0 +1,42 @@ + +open Lparse +open Fmt_lexp +open Utest_lib + +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 input = "x = lambda x -> x;" + +let generate_lexp_from_str str = + List.hd ((fun (lst, _) -> + (List.map + (fun (_, lxp, _) -> lxp)) + (List.flatten lst)) + (lexp_decl_str str default_lctx)) + +let _ = generate_tests + "TYPECHECK" + (fun () -> [generate_lexp_from_str input]) + (fun x -> List.map string_of_lxp x) + (fun x -> (x, false)) + +let _ = run_all ()

View it on GitLab: https://gitlab.com/monnier/typer/compare/293f20f65d551488bcf599af7c2bd8536c7...