BONNEVALLE Vincent pushed to branch unification at Stefan / Typer

Commits: d9a44f1b by n3f4s at 2016-07-06T21:52:44+02:00 add first idea of finding inverse of substitution

- - - - - 357c3f5e by n3f4s at 2016-07-06T23:07:32+02:00 better printing for sort(level)

- - - - - f771c1f5 by n3f4s at 2016-07-06T23:08:03+02:00 add test for sort

- - - - - dcf7fce4 by n3f4s at 2016-07-06T23:08:19+02:00 add lexp_loc for metavar

- - - - - 8d0ea3b7 by n3f4s at 2016-07-07T16:36:11+02:00 compose s & s' in unsusp for metavar

- - - - - 81a12842 by n3f4s at 2016-07-07T16:36:40+02:00 use mkSusp instead of Susp(_, _) in _unify_metavar

- - - - - d18fac93 by n3f4s at 2016-07-14T22:24:26+02:00 add begining flattening function

- - - - - 9d83a8d4 by n3f4s at 2016-07-14T22:25:41+02:00 move inversion function out of unification

- - - - - 98dde635 by n3f4s at 2016-07-18T23:30:52+02:00 add test for substituttion inversion

- - - - - b8267fd7 by n3f4s at 2016-07-18T23:31:41+02:00 better output & first version of inversion

- - - - - 73772928 by n3f4s at 2016-07-18T23:58:57+02:00 add test

Inversion fail when the first variable is generated

- - - - - 93eb0302 by n3f4s at 2016-07-19T00:51:47+02:00 debug case where the first variable is generated

- - - - - e9223a23 by n3f4s at 2016-07-19T18:11:41+02:00 ocamldoc compliant documentation

- - - - - 8b9352ac by n3f4s at 2016-07-19T21:06:46+02:00 better printing for substitution

- - - - - ff8660c0 by n3f4s at 2016-07-19T21:12:30+02:00 better indentation for doc

- - - - - 801db020 by n3f4s at 2016-07-19T21:13:44+02:00 refactoring in fill function for readability

- - - - - 31a0d0d0 by n3f4s at 2016-07-19T21:14:13+02:00 add test for substitution inversion

- - - - - 27fc552d by n3f4s at 2016-07-19T22:13:47+02:00 Add function for creating test input

- - - - -

6 changed files:

- src/fmt_lexp.ml - + src/inverse_subst.ml - src/lexp.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 @@ -25,12 +25,23 @@ let rec string_of_lxp lxp = | Metavar (value, _, (_, name)) -> "Metavar(" ^ (string_of_int value) ^ ", " ^ name ^ ")" | Call (_) -> "Call(...)" | Inductive _ -> ("Inductive") ^ "(...)" - | Sort _ -> ("Sort") ^ "(...)" - | SortLevel _ -> ("SortLevel") ^ "(...)" + | Sort (_, s) -> ("Sort") ^ "(" ^ string_of_sort s ^ ")" + | SortLevel l -> ("SortLevel") ^ "(" ^ string_of_sort_level l ^ ")" | Case _ -> ("Case") ^ "(...)" | Susp _ -> "Susp(...)" | _ -> "Unidentified Lexp"

+and string_of_sort_level lvl = + match lvl with + | SLn i -> "SLn(" ^ string_of_int i ^ ")" + | SLsucc l -> "SLsucc(" ^ string_of_lxp l^ ")" + +and string_of_sort sort = + match sort with + | Stype lxp -> "Stype(" ^ string_of_lxp lxp ^ ")" + | StypeOmega -> "StypeOmega" + | StypeLevel -> "StypeLevel" + let colored_string_of_lxp lxp lcol vcol = match lxp with | Imm (Integer (_, value)) -> (lcol "Integer") ^ "(" ^ (vcol (string_of_int value)) ^ ")" @@ -66,3 +77,12 @@ let center (str: string ) (dim: int ) (char_: char) : string = let diff = (dim - String.length str) + 5 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 ===================================== --- /dev/null +++ b/src/inverse_subst.ml @@ -0,0 +1,161 @@ + +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 +*) + +(* 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 *) + +(** Helper function that create a Cons(_, Shift(_)) *) +let mkSubstNode var offset = S.Cons (var, S.Shift(S.Identity, offset)) + +(** Transform a subst into a more linear 'intermdiate representation': + + - a1.↑^{x1}(a2.↑^{x2}(a3.↑^{x3}id)) -> a1.(↑^{x1}a2).(↑^{x2}a3).↑^{x3}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 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 )] + (* Assuming that a Shift always follow Cons, the case Shift should never arise *) + 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} + + or in ocaml-ish representation : + + - S.Cons(var, S.Shift(S.Identity, offset))::...::Identity -> S.Shift(S.Cons(var, S.Cons(...)), x1+x2+x3...) +*) +let flattenIr (s: inter_subst) = + 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 + in match flattenCons s with + | Some(offset, cons) -> Some(S.Shift(cons, offset)) + | None -> None + +(** 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 : + + - S.Cons(var, S.Shift(..., offset)) -> S.Shift(S.Cons(var, S.Cons(...)), x1+x2+x3...) +*) +let flatten (s: lexp S.subst) = flattenIr (toIr s) + + +(* 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) + +(** Returns the db_index of the "inside" of a Var +*) +let idxOf (_, idx) = idx + +(** Returns a list of couple (X, -1) where X go from beg_ to end_*) +let rec genDummyVar beg_ end_ = + if beg_ < end_ + then (beg_, -1)::(genDummyVar (beg_ + 1) end_) + else [] + +(** Returns a dummy variable with the db_index idx +*) +let mkVar idx = Var((U.dummy_location, ""), idx) (* not sure how to fill vdef *) + +(** 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 + +(* With the exemple of the article : + should return (1,1)::(3,2)::(4,3)::[] +*) +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 -> [] + +(* With the exemple of the article : + should return (1,1)::(2, X)::(3,2)::(4,3)::(5, Z)::[] +*) +let fill l size acc = + let rec fill_before l = + match l with + | [] -> [] + | (idx, val_)::tail -> (if idx > 0 then (genDummyVar 0 idx)@l + else l) + and fill_after l size acc = + match l with + | (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 acc@((idx1, val1)::(genDummyVar (idx1 + 1) size)) + else acc@[(idx1, val1)] + | [] -> acc + in fill_after (fill_before 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 []) + +(** s:S.subst -> l:lexp -> s':S.subst where l[s][s'] = l *) +let rec inverse (subst: lexp S.subst ) : lexp S.subst option = + match flatten subst with + | Some(S.Shift(flattened, shift)) -> + let size = sizeOf flattened + in Some(S.Shift((generateCons flattened size shift), size)) + | None -> None +

===================================== src/lexp.ml ===================================== --- a/src/lexp.ml +++ b/src/lexp.ml @@ -263,8 +263,8 @@ let rec lexp_location e = | Cons (_,(l,_)) -> l | Case (l,_,_,_,_,_) -> l | Susp (e, _) -> lexp_location e - (* | Susp (_, e) -> lexp_location e - * | Metavar ((l,_),_,_) -> l *) + (* | Susp (_, e) -> lexp_location e *) + | Metavar (_,_,(l,_)) -> l

(********* Normalizing a term *********) @@ -322,7 +322,7 @@ let rec unsusp e s = (* Push a suspension one level down. *) match default with | None -> default | Some e -> Some (mkSusp e s)) - | Metavar (idx, s', vdef_) -> Metavar(idx, s, vdef_) + | Metavar (idx, s', vdef_) -> Metavar(idx, (S.compose (mkSusp) s s'), vdef_)

let unsusp_all e = match e with

===================================== src/unification.ml ===================================== --- a/src/unification.ml +++ b/src/unification.ml @@ -1,12 +1,15 @@

open Lexp open Sexp +open Inverse_subst

module VMap = Map.Make (struct type t = int let compare = compare end)

type substitution = lexp VMap.t 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 =*) (*| Some of 'a*) @@ -31,7 +34,7 @@ let associate (meta: int) (lxp: lexp) (subst: substitution) (VMap.add meta lxp subst)

(** If key is in map returns the value associated - * else returns None + else returns <code>None</code> *) let find_or_none (value: lexp) (map: substitution) : lexp option = match value with @@ -42,7 +45,7 @@ let find_or_none (value: lexp) (map: substitution) : lexp option =

let empty_subst = (VMap.empty)

-(* Zip while applying a function, returns empty list if l1 & l2 have different size*) +(** Zip while applying a function, returns <code>None</code> list if l1 & l2 have different size*) let zip_map (l1: 'a list ) (l2: 'b list ) (f: ('a -> 'b -> 'c)): 'c list option = let rec zip_ ll1 ll2 f = match ll1, ll2 with @@ -51,26 +54,31 @@ let zip_map (l1: 'a list ) (l2: 'b list ) (f: ('a -> 'b -> 'c)): 'c list option | _, _ -> [] (* Should never happen since we check length before actually calling the recursion but without this case, the compiler complains*) in if List.length l1 = List.length l2 then Some (zip_ l1 l2 f) else None

+(** Custom zip (<i>List.combine</i>), return a list of couple if the two list have the same size, +return <code>None</code> if not*) let zip (l1: 'a list) (l2: 'b list): (('a * 'b) list option) = zip_map l1 l2 (fun x z -> (x, z))

+(** Fold the two lists, and zip the result *) let zip_fold list1 list2 f = let l1 = List.fold_right (f) list1 [] and l2 = List.fold_right (f) list2 [] in zip l1 l2

(** - * lexp is equivalent to _ in ocaml - * (Let , lexp) == (lexp , Let) - * UNIFY -> recursive call or dispatching - * OK -> add a substituion to the list of substitution - * CONSTRAINT -> returns a constraint + lexp is equivalent to _ in ocaml + (Let , lexp) == (lexp , Let) + UNIFY -> recursive call or dispatching + OK -> add a substituion to the list of substitution + CONSTRAINT -> returns a constraint *)

(****************************** Top level unify *************************************)

(** Dispatch to the right unifyer. - * If (_unify_X X Y) don't handle the case (X, Y), it call (unify Y X) - * The metavar unifyer is the end rule, it can't call unify with it's parameter (changing their order) + + If (<code>_unify_X X Y</code>) don't handle the case <b>(X, Y)</b>, it call (<code>unify Y X</code>) + + The metavar unifyer is the end rule, it can't call unify with it's parameter (changing their order) *) let rec unify (l: lexp) (r: lexp) (subst: substitution) : return_type = let tmp = match (l, r) with @@ -93,7 +101,6 @@ let rec unify (l: lexp) (r: lexp) (subst: substitution) : return_type = | (Inductive _, _) -> _unfiy_induct l r subst | (Sort _, _) -> _unify_sort l r subst | (SortLevel _, _) -> _unify_sortlvl l r subst - (* | (_, _) -> None*) in match tmp with | Some _ -> Debug_fun.debug_print_unify "unify" l r " -> unification success"; tmp | None -> Debug_fun.debug_print_unify "unify" l r " -> unification failed"; tmp @@ -101,9 +108,9 @@ let rec unify (l: lexp) (r: lexp) (subst: substitution) : return_type = (********************************* Type specific unify *******************************)

(** Unify two Imm if they match <=> Same type and same value - * Add one of the Imm (the first arguement) to the substitution - * Imm, Imm -> if Imm =/= Imm then ERROR else OK - * Imm, lexp -> unify lexp Imm + - Add one of the Imm (the first arguement) to the substitution + - Imm, Imm -> if Imm =/= Imm then ERROR else OK + - Imm, lexp -> unify lexp Imm *) and _unify_imm (l: lexp) (r: lexp) (subst: substitution) : return_type = match (l, r) with @@ -121,8 +128,8 @@ and _unify_imm (l: lexp) (r: lexp) (subst: substitution) : return_type = | (_, _) -> None

(** Unify a Cons and a lexp - * Cons, Cons -> if Cons ~= Cons then OK else ERROR - * Cons, _ -> ERROR + - Cons, Cons -> if Cons ~= Cons then OK else ERROR + - Cons, _ -> ERROR *) (*FIXME which parameter of Cons is it's name ?*) (* symbol = (location * string)*) @@ -136,8 +143,8 @@ and _unify_cons (cons: lexp) (lxp: lexp) (subst: substitution) : return_type = | (_, _) -> None

(** Unify a builtin (bltin) and a lexp (lxp) if it is possible - * If the two arguments are builtin, unify based on name - * If it's a Builtin and an other lexp, unify lexp part of Builtin with the lexp + - If the two arguments are builtin, unify based on name + - If it's a Builtin and an other lexp, unify lexp part of Builtin with the lexp *) and _unify_builtin (bltin: lexp) (lxp: lexp) (subst: substitution) : return_type = match (bltin, lxp) with @@ -148,8 +155,8 @@ and _unify_builtin (bltin: lexp) (lxp: lexp) (subst: substitution) : return_type | (_, _) -> None

(** Unify a Let (let_) and a lexp (lxp), if possible - * Let , Let -> check the 'inside' of the let - * Let , lexp -> constraint + - Let , Let -> check the 'inside' of the let + - Let , lexp -> constraint *) and _unify_let (let_: lexp) (lxp: lexp) (subst: substitution) : return_type = let concat = (fun (_, lxp, lt) acc -> lxp::lt::acc) @@ -168,9 +175,9 @@ and _unify_let (let_: lexp) (lxp: lexp) (subst: substitution) : return_type = | None -> Debug_fun.debug_print_unify "_unify_let" let_ lxp " -> unification failed"; tmp

(** Unify a Var and a lexp, if possible - * (Var, Var) -> unify if they have the same debruijn index FIXME : shift indexes - * (Var, Metavar) -> unify_metavar Metavar var subst - * (Var _, _) -> unfiy lexp Var subst + - (Var, Var) -> unify if they have the same debruijn index FIXME : shift indexes + - (Var, Metavar) -> unify_metavar Metavar var subst + - (Var _, _) -> unfiy lexp Var subst *) (*FIXME : check for the value of Var -> need context ?*) and _unify_var (var: lexp) (r: lexp) (subst: substitution) : return_type = @@ -183,11 +190,11 @@ and _unify_var (var: lexp) (r: lexp) (subst: substitution) : return_type = | (_, _) -> None

(** Unify a Arrow and a lexp if possible - * (Arrow, Arrow) -> if var_kind = var_kind + - (Arrow, Arrow) -> if var_kind = var_kind then unify ltype & lexp (Arrow (var_kind, _, ltype, lexp)) else None - * (Arrow, Var) -> Constraint - * (_, _) -> None + - (Arrow, Var) -> Constraint + - (_, _) -> None *) and _unify_arrow (arrow: lexp) (lxp: lexp) (subst: substitution) : return_type = @@ -202,12 +209,12 @@ and _unify_arrow (arrow: lexp) (lxp: lexp) (subst: substitution) | (_, _) -> None

(** Unify a Lambda and a lexp if possible - * Lamda , Lambda -> if var_kind = var_kind + - Lamda , Lambda -> if var_kind = var_kind then UNIFY ltype & lxp else ERROR - * Lambda , Var -> CONSTRAINT - * Lambda , Call -> Constraint - * Lambda , Let -> Constraint - * Lambda , lexp -> unify lexp lambda subst + - Lambda , Var -> CONSTRAINT + - Lambda , Call -> Constraint + - Lambda , Let -> Constraint + - Lambda , lexp -> unify lexp lambda subst *) and _unify_lambda (lambda: lexp) (lxp: lexp) (subst: substitution) : return_type = match (lambda, lxp) with @@ -224,21 +231,18 @@ and _unify_lambda (lambda: lexp) (lxp: lexp) (subst: substitution) : return_type | (_, _) -> None

(** Unify a Metavar and a lexp if possible - * lexp , {metavar <-> none} -> UNIFY - * lexp , {metavar <-> lexp} -> UNFIFY lexp subst[metavar] - * metavar , metavar -> if Metavar = Metavar then OK else ERROR - * metavar , lexp -> OK + - lexp , {metavar <-> none} -> UNIFY + - lexp , {metavar <-> lexp} -> UNFIFY lexp subst[metavar] + - metavar , metavar -> if Metavar = Metavar then OK else ERROR + - metavar , lexp -> OK *) and _unify_metavar (meta: lexp) (lxp: lexp) (subst: substitution) : return_type = - (** s:S.subst -> l:lexp -> s':S.subst where l[s][s'] = l *) - let rec inverse subst = Some S.Identity - in let find_or_unify metavar value lxp s = match find_or_none metavar s with | Some (lxp_) -> unify lxp_ lxp s | None -> (match metavar with | Metavar (_, subst_, _) -> (match inverse subst_ with - | Some s' -> Some (associate value (Susp (lxp, s')) s, []) + | Some s' -> Some (associate value (mkSusp lxp s') s, []) | None -> None) | _ -> None) in @@ -249,8 +253,8 @@ and _unify_metavar (meta: lexp) (lxp: lexp) (subst: substitution) : return_type | (_, _) -> None

(** Unify a Call (call) and a lexp (lxp) - * Call , Call -> UNIFY - * Call , lexp -> CONSTRAINT + - Call , Call -> UNIFY + - Call , lexp -> CONSTRAINT *) and _unify_call (call: lexp) (lxp: lexp) (subst: substitution) : return_type = let f = (fun (_, x) acc -> x::acc) @@ -275,8 +279,8 @@ and _unify_susp (susp_: lexp) (lxp: lexp) (subst: substitution) : return_type = | _ -> None

(** Unify a Case with a lexp - * Case, Case -> try to unify - * Case, _ -> Constraint + - Case, Case -> try to unify + - Case, _ -> Constraint *) and _unify_case (case: lexp) (lxp: lexp) (subst: substitution) : return_type = let merge (_, c) r2 = match r2 with @@ -301,10 +305,10 @@ and _unify_case (case: lexp) (lxp: lexp) (subst: substitution) : return_type = | None -> Debug_fun.debug_print_unify "_unify_case" case lxp " -> unification failed"; tmp

(** Unify a Inductive and a lexp - * Inductive, Inductive -> try unify - * Inductive, Var -> constraint - * Inductive, Call/Metavar/Case/Let -> constraint - * Inductive, _ -> None + - Inductive, Inductive -> try unify + - Inductive, Var -> constraint + - Inductive, Call/Metavar/Case/Let -> constraint + - Inductive, _ -> None *) and _unfiy_induct (induct: lexp) (lxp: lexp) (subst: substitution) : return_type = let transform (a, b, c) (d, e, f) = ((a, Some b, c), (d, Some e, f)) @@ -326,8 +330,8 @@ and _unfiy_induct (induct: lexp) (lxp: lexp) (subst: substitution) : return_type | (_, _) -> None

(** Unify a SortLevel with a lexp - * SortLevel, SortLevel -> if SortLevel ~= SortLevel then OK else ERROR - * SortLevel, _ -> ERROR + - SortLevel, SortLevel -> if SortLevel ~= SortLevel then OK else ERROR + - SortLevel, _ -> ERROR *) and _unify_sortlvl (sortlvl: lexp) (lxp: lexp) (subst: substitution) : return_type = match sortlvl, lxp with @@ -338,9 +342,9 @@ and _unify_sortlvl (sortlvl: lexp) (lxp: lexp) (subst: substitution) : return_ty | _, _ -> None

(** Unify a Sort and a lexp - * Sort, Sort -> if Sort ~= Sort then OK else ERROR - * Sort, Var -> Constraint - * Sort, lexp -> ERROR + - Sort, Sort -> if Sort ~= Sort then OK else ERROR + - Sort, Var -> Constraint + - Sort, lexp -> ERROR *) and _unify_sort (sort_: lexp) (lxp: lexp) (subst: substitution) : return_type = match sort_, lxp with

===================================== tests/inverse_test.ml ===================================== --- /dev/null +++ b/tests/inverse_test.ml @@ -0,0 +1,61 @@ +open Sexp +open Pexp +open Lexp +open Unification +open Inverse_subst + +open Lparse (* add_def *) + +open Utest_lib + +open Fmt + +open Builtin +open Env + +open Str + +open Debug + +open Fmt_lexp +open Debug_fun + +let mkShift2 shift subst = + S.Shift (subst, shift) + +let rec mkTestSubst lst = + match lst with + | (var, shift)::tail -> S.Cons (mkVar var, + mkShift2 shift (mkTestSubst tail)) + | [] -> S.Identity + +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, 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)::[])):: + (S.Cons (mkVar 1, S.Shift(S.Identity, 3))):: + [] + +let lxp = mkVar 3 + +let inputs = 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"))) + input + +let _ = List.map (fun (res, str) -> add_test "INVERSE" str (fun () -> if res then success () else failure ())) + inputs + +let _ = run_all ()

===================================== tests/unify_test.ml ===================================== --- a/tests/unify_test.ml +++ b/tests/unify_test.ml @@ -50,7 +50,7 @@ let fmt (lst: (lexp * lexp * result * result) list): string list = lst in let l, c1, c2, r = max_dim str_lst in List.map (fun (l1, l2, r1, r2) -> (padding_right l1 l ' ') - ^ "," + ^ ", " ^ (padding_right l2 c1 ' ') ^ "-> got: " ^ (padding_right r2 r ' ') @@ -74,6 +74,8 @@ let str_let2 = "j = let b = 5 in b" let str_lambda = "sqr = lambda (x : Int) -> x * x;" let str_lambda2 = "sqr = lambda (x : Int) -> x * x;" let str_lambda3 = "sqr = lambda (x : Int) -> lambda (y : Int) -> x * y;" +let str_type = "i = let j = decltype(Type) in decltype(j);" +let str_type2 = "j = let i = Int -> Int in decltype(i);"

let generate_ltype_from_str str = List.hd ((fun (lst, _) -> @@ -102,6 +104,8 @@ let input_lambda3 = generate_lexp_from_str str_lambda3 let input_arrow = generate_ltype_from_str str_lambda let input_arrow2 = generate_ltype_from_str str_lambda2 let input_arrow3 = generate_ltype_from_str str_lambda3 +let input_type = generate_ltype_from_str str_type +let input_type_t = generate_ltype_from_str str_type2

let generate_testable (_: lexp list) : ((lexp * lexp * result) list) =

@@ -160,6 +164,9 @@ let generate_testable (_: lexp list) : ((lexp * lexp * result) list) = ::(input_arrow3 , input_arrow , Constraint) (* of the var inside the arrow *) ::(input_arrow2 , input_arrow , Equivalent) ::(input_arrow3 , input_arrow3 , Equivalent) + + ::(input_type , input_type_t , Equivalent) + ::(Metavar (0, S.Identity, (Util.dummy_location, "M")), Var ((Util.dummy_location, "x"), 3), Unification)

::[]

View it on GitLab: https://gitlab.com/monnier/typer/compare/6bc9f1f9eda89148c692155709647b4f26b...