Typer
Discussions par mois
- ----- 2026 -----
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2025 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2024 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2023 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2022 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2021 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2020 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2019 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2018 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2017 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
- janvier
- ----- 2016 -----
- décembre
- novembre
- octobre
- septembre
- août
- juillet
- juin
- mai
- avril
- mars
- février
Juillet 2016
- 1 participants
- 14 discussions
[Git][monnier/typer][unification] 13 commits: fix non termination of test
by BONNEVALLE Vincent 29 Jul '16
by BONNEVALLE Vincent 29 Jul '16
29 Jul '16
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/293f20f65d551488bcf599af7c2bd8536c…
1
0
[Git][monnier/typer][unification] * tests/inverse_test.ml (is_identity.is_identity): Forget it
by Stefan 28 Jul '16
by Stefan 28 Jul '16
28 Jul '16
Stefan pushed to branch unification at Stefan / Typer
Commits:
293f20f6 by Stefan Monnier at 2016-07-28T14:15:34-04:00
* tests/inverse_test.ml (is_identity.is_identity): Forget it
* src/lexp.ml (push_susp): Don't be so picky.
- - - - -
2 changed files:
- src/lexp.ml
- tests/inverse_test.ml
Changes:
=====================================
src/lexp.ml
=====================================
--- a/src/lexp.ml
+++ b/src/lexp.ml
@@ -328,10 +328,10 @@ let rec push_susp e s = (* Push a suspension one level down. *)
* pushes the subst into them eagerly. IOW if there's a Susp(Var..)
* or Susp(Metavar..) it's because some chunk of code should use mkSusp
* rather than Susp. *)
- | Susp (e,s') -> U.msg_error "SUSP" (lexp_location e) "¡Susp(Susp)!";
+ | Susp (e,s') -> (* U.msg_error "SUSP" (lexp_location e) "¡Susp(Susp)!"; *)
push_susp e (scompose s' s)
| (Var _ | Metavar _)
- -> U.msg_error "SUSP" (lexp_location e) "¡Susp((meta)var)!";
+ -> (* U.msg_error "SUSP" (lexp_location e) "¡Susp((meta)var)!"; *)
push_susp (mkSusp e s) S.identity
let nosusp e = (* Return `e` without `Susp`. *)
=====================================
tests/inverse_test.ml
=====================================
--- a/tests/inverse_test.ml
+++ b/tests/inverse_test.ml
@@ -56,7 +56,7 @@ let is_identity s =
let rec is_identity s acc =
match s with
| S.Cons(Var(_, idx), s1) when idx = acc -> is_identity s1 (acc + 1)
- | S.Shift(S.Identity, shift) -> (0 = shift)
+ | S.Shift(S.Identity, shift) -> (acc = shift)
| S.Identity -> true
| _ -> false
in is_identity s 0
View it on GitLab: https://gitlab.com/monnier/typer/commit/293f20f65d551488bcf599af7c2bd8536c7…
1
0
[Git][monnier/typer][unification] * tests/inverse_test.ml (is_identity.is_identity): Only shift 0 is identity.
by Stefan 28 Jul '16
by Stefan 28 Jul '16
28 Jul '16
Stefan pushed to branch unification at Stefan / Typer
Commits:
93626d8b by Stefan Monnier at 2016-07-28T14:12:26-04:00
* tests/inverse_test.ml (is_identity.is_identity): Only shift 0 is identity.
- - - - -
1 changed file:
- tests/inverse_test.ml
Changes:
=====================================
tests/inverse_test.ml
=====================================
--- a/tests/inverse_test.ml
+++ b/tests/inverse_test.ml
@@ -56,7 +56,7 @@ let is_identity s =
let rec is_identity s acc =
match s with
| S.Cons(Var(_, idx), s1) when idx = acc -> is_identity s1 (acc + 1)
- | S.Shift(S.Identity, shift) -> (acc = shift)
+ | S.Shift(S.Identity, shift) -> (0 = shift)
| S.Identity -> true
| _ -> false
in is_identity s 0
View it on GitLab: https://gitlab.com/monnier/typer/commit/93626d8b8c6017bcd04b49b3e4b698bfcb1…
1
0
28 Jul '16
Stefan pushed to branch unification at Stefan / Typer
Commits:
4e504963 by Stefan Monnier at 2016-07-28T12:42:23-04:00
Tweak use of substitutions and unsusp
* src/inverse_subst.ml (mkFinalShift): Remove; use S.shift instead.
(toIr): Use S.mkShift.
(flattenIr.flattenCons): Remove unused `offset' arg. Simplify.
* src/lexp.ml (subst): Newtype.
(mkSusp): Also apply eagerly to Metavar.
(push_susp): Rename from unsusp.
(nosusp): Rename from ususp_all.
(_lexp_to_str): Use push_susp.
* src/unification.ml (unify.tmp): Use nosusp.
(_unify_susp): Remove.
* tests/inverse_test.ml: Use S.shift/cons and friends.
- - - - -
8 changed files:
- src/elexp.ml
- src/inverse_subst.ml
- src/lexp.ml
- src/lparse.ml
- src/subst.ml
- src/typecheck.ml
- src/unification.ml
- tests/inverse_test.ml
Changes:
=====================================
src/elexp.ml
=====================================
--- a/src/elexp.ml
+++ b/src/elexp.ml
@@ -86,7 +86,7 @@ let rec erase_type (lxp: L.lexp): elexp =
Case(l, (erase_type target), (clean_map cases),
(clean_maybe default))
- | L.Susp(l, s) -> erase_type (L.unsusp l s)
+ | L.Susp(l, s) -> erase_type (L.push_susp l s)
(* To be thrown out *)
| L.Arrow _ -> Type
=====================================
src/inverse_subst.ml
=====================================
--- a/src/inverse_subst.ml
+++ b/src/inverse_subst.ml
@@ -12,28 +12,27 @@ type inter_subst = lexp list (* Intermediate between "tree"-like substitution an
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':
+(** Transform a subst into a more linear 'intermediate representation':
- - a1.↑^\{x1\}(a2.↑^\{x2\}(a3.↑^\{x3\}id)) -> a1.(↑^\{x1\}a2).(↑^\{x2\}a3).↑^\{x3\}id
+ - 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
+ - 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 =
+ let rec toIr s total_offset =
match s with
- | 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 ))]
+ | 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
@@ -46,15 +45,14 @@ let toIr (s: lexp S.subst) : inter_subst =
- <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 offset =
+ let rec flattenCons s =
match s with
- | 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))
+ | 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 0
+ in flattenCons s
(** Flatten a "tree"-like substitution:
@@ -156,9 +154,9 @@ let to_list (s: lexp S.subst) : (((int * int) list) * int) =
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))
+ | Some s -> Some (S.cons (mkVar i) s)
| None -> None)
- | [] -> Some (mkFinalShift shift)
+ | [] -> Some (S.shift shift)
(** Compute the inverse, if there is one, of the substitution.
=====================================
src/lexp.ml
=====================================
--- a/src/lexp.ml
+++ b/src/lexp.ml
@@ -53,13 +53,14 @@ type label = symbol
(* Pour la propagation des types bidirectionnelle, tout va dans `infer`,
* sauf Lambda et Case qui vont dans `check`. Je crois. *)
type ltype = lexp
+ and subst = lexp S.subst
and lexp =
| Imm of sexp (* Used for strings, ... *)
| SortLevel of sort_level
| Sort of U.location * sort
| Builtin of vdef * ltype
| Var of vref
- | Susp of lexp * lexp S.subst (* Lazy explicit substitution: e[σ]. *)
+ | Susp of lexp * subst (* Lazy explicit substitution: e[σ]. *)
(* This "Let" allows recursion. *)
| Let of U.location * (vdef * lexp * ltype) list * lexp
| Arrow of arg_kind * vdef option * ltype * U.location * lexp
@@ -74,7 +75,7 @@ type ltype = lexp
* ltype (* The type of the return value of all branches *)
* (U.location * (arg_kind * vdef option) list * lexp) SMap.t
* lexp option (* Default. *)
- | Metavar of int * (lexp S.subst) * vdef (*idx * S.subst * (name * location)*)
+ | Metavar of int * subst * vdef
(* (\* For logical metavars, there's no substitution. *\)
* | Metavar of (U.location * string) * metakind * metavar ref
* and metavar =
@@ -110,9 +111,13 @@ type varbind =
let rec mkSusp e s =
if S.identity_p s then e else
+ (* We apply the substitution eagerly to some terms.
+ * There's no deep technical rason for that:
+ * it just seemed like a good idea to do it eagerly when it's easy. *)
match e with
| Susp (e, s') -> mkSusp e (scompose s' s)
- | Var (l,v) -> slookup s l v (* Apply the substitution eagerly. *)
+ | Var (l,v) -> slookup s l v
+ | Metavar (vn, s', vd) -> Metavar (vn, scompose s' s, vd)
| _ -> Susp (e, s)
and scompose s1 s2 = S.compose mkSusp s1 s2
and slookup s l v = S.lookup (fun l i -> Var (l, i))
@@ -272,16 +277,13 @@ let rec lexp_location e =
let vdummy = (U.dummy_location, "dummy")
let maybev mv = match mv with None -> vdummy | Some v -> v
-let rec unsusp e s = (* Push a suspension one level down. *)
+let rec push_susp e s = (* Push a suspension one level down. *)
match e with
| Imm _ -> e
| SortLevel _ -> e
| Sort (l, Stype e) -> Sort (l, Stype (mkSusp e s))
| Sort (l, _) -> e
| Builtin _ -> e
- | Var ((l,_) as lv,v) -> U.msg_error "SUSP" l "¡Susp(Var)!"; slookup s lv v
- | Susp (e,s') -> U.msg_error "SUSP" (lexp_location e) "¡Susp(Susp)!";
- mkSusp e (scompose s' s)
| Let (l, defs, e)
-> let s' = L.fold_left (fun s (v, _, _) -> ssink v s) s defs in
let (_,ndefs) = L.fold_left (fun (s,ndefs) (v, def, ty)
@@ -322,11 +324,19 @@ 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.compose (mkSusp) s s'), vdef_)
+ (* Susp should never appear around Var/Susp/Metavar because mkSusp
+ * pushes the subst into them eagerly. IOW if there's a Susp(Var..)
+ * or Susp(Metavar..) it's because some chunk of code should use mkSusp
+ * rather than Susp. *)
+ | Susp (e,s') -> U.msg_error "SUSP" (lexp_location e) "¡Susp(Susp)!";
+ push_susp e (scompose s' s)
+ | (Var _ | Metavar _)
+ -> U.msg_error "SUSP" (lexp_location e) "¡Susp((meta)var)!";
+ push_susp (mkSusp e s) S.identity
-let unsusp_all e =
+let nosusp e = (* Return `e` without `Susp`. *)
match e with
- | Susp(e, s) -> unsusp e s
+ | Susp(e, s) -> push_susp e s
| _ -> e
let lexp_to_string e =
@@ -670,7 +680,7 @@ and _lexp_to_str ctx exp =
| Float (_, s) -> tval (string_of_float s)
| e -> sexp_to_str e)
- | Susp _ -> _lexp_to_str ctx (unsusp_all exp)
+ | Susp (e, s) -> _lexp_to_str ctx (push_susp e s)
| Var ((loc, name), idx) -> name ^ (index idx) ;
=====================================
src/lparse.ml
=====================================
--- a/src/lparse.ml
+++ b/src/lparse.ml
@@ -241,7 +241,7 @@ and _lexp_p_infer (p : pexp) (ctx : lexp_context) i: lexp * ltype =
let inductive_type = Var((loc, type_name), idx) in
(* Get constructor args *)
- let formal, args = match unsusp_all idt with
+ let formal, args = match nosusp idt with
| Inductive(_, _, formal, ctor_def) -> (
try formal, (SMap.find cname ctor_def)
with Not_found ->
@@ -297,7 +297,7 @@ and _lexp_p_check (p : pexp) (t : ltype) (ctx : lexp_context) i: lexp =
(* This case cannot be inferred *)
| Plambda (kind, var, None, body) ->(
(* Read var type from the provided type *)
- let ltp, lbtp = match unsusp_all t with
+ let ltp, lbtp = match nosusp t with
| Arrow(kind, _, ltp, _, lbtp) -> ltp, lbtp
| _ -> lexp_error tloc "Type does not match"; dltype, dltype in
@@ -402,7 +402,7 @@ and lexp_call (fun_name: pexp) (sargs: sexp list) ctx i =
(* consume Arrows and args together *)
let rec get_return_type name i ltp args =
- match (unsusp_all ltp), args with
+ match (nosusp ltp), args with
| _, [] -> ltp
| Arrow(_, _, _, _, ltp), hd::tl -> (get_return_type name (i + 1) ltp tl)
| _, _ -> lexp_warning loc
@@ -416,7 +416,7 @@ and lexp_call (fun_name: pexp) (sargs: sexp list) ctx i =
(* retrieve function's body *)
let body, ltp = _lexp_p_infer fun_name ctx (i + 1) in
- let ltp = unsusp_all ltp in
+ let ltp = nosusp ltp in
let handle_named_call (loc, name) =
(* Process Arguments *)
@@ -428,7 +428,7 @@ and lexp_call (fun_name: pexp) (sargs: sexp list) ctx i =
let idx = senv_lookup name ctx in
let vf = (make_var name idx loc) in
- match unsusp_all (env_lookup_expr ctx ((loc, name), idx)) with
+ match nosusp (env_lookup_expr ctx ((loc, name), idx)) with
| Builtin((_, "Built-in"), _) ->(
(* ------ SPECIAL ------ *)
match !_parsing_internals, largs with
@@ -476,7 +476,7 @@ and lexp_call (fun_name: pexp) (sargs: sexp list) ctx i =
lexp_fatal loc (name ^ " was found but " ^ (string_of_int idx) ^
" is not a correct index.") in
- let lxp = match unsusp_all lxp with
+ let lxp = match nosusp lxp with
| Call(Var((_, "Macro_"), _), [(_, fct)]) -> fct
| _ ->
print_string "\n";
@@ -555,7 +555,7 @@ and lexp_read_pattern pattern exp target ctx:
| Ppatvar ((loc, name) as var) ->(
try(
let idx = senv_lookup name ctx in
- match unsusp_all (env_lookup_expr ctx ((loc, name), idx)) with
+ match nosusp (env_lookup_expr ctx ((loc, name), idx)) with
(* We are matching a constructor *)
| Cons _ -> (name, loc, []), ctx
@@ -641,7 +641,7 @@ and lexp_decls_macro (loc, mname) sargs ctx: (pdecl list * lexp_context) =
" is not a correct index.") in
(* get stored function *)
- let lxp = match unsusp_all lxp with
+ let lxp = match nosusp lxp with
| Call(Var((_, "Macro_"), _), [(_, fct)]) -> fct
| _ -> print_string "\n";
print_string (lexp_to_string lxp); print_string "\n";
=====================================
src/subst.ml
=====================================
--- a/src/subst.ml
+++ b/src/subst.ml
@@ -21,6 +21,28 @@ this program. If not, see <http://www.gnu.org/licenses/>. *)
module U = Util
+(* Implementation of the subsitution calculus.
+ *
+ * As a general rule, try not to use the constructors of the `subst'
+ * datatype, but use the following entry points instead.
+ * Constructor functions:
+ * - S.identity
+ * - S.cons
+ * - S.mkShift
+ * - S.shift
+ * - S.compose
+ * - S.substitute
+ * - S.sink
+ * Destructor functions:
+ * - S.identity_p
+ * - S.lookup
+ *
+ * This implementation is generic (i.e. can be with various datatypes
+ * implementing the associated lambda-calculus), which is the reason for
+ * the added complexity of arguments like `mkVar` and `mkShift` to `S.lookup`.
+ * So in general, you'll want to use Lexp.scompose and Lexp.slookup
+ * for those functions.
+ *)
(* Suspensions definitions.
*
@@ -236,6 +258,7 @@ let shift (m:db_offset) = mkShift Identity m
(* The trivial substitution which doesn't do anything. *)
let identity = Identity
+(* Test if a substitution is trivial. The "_p" stands for "predicate". *)
let identity_p s = match s with | Identity -> true | _ -> false
(* Compose two substitutions. This implements the merging rules.
=====================================
src/typecheck.ml
=====================================
--- a/src/typecheck.ml
+++ b/src/typecheck.ml
@@ -110,7 +110,7 @@ let lookup_type ctx vref =
let lookup_value ctx vref =
let (_, i) = vref in
match Myers.nth i ctx with
- | (o, _, LetDef v, _) -> Some (unsusp v (S.shift (i + 1 - o)))
+ | (o, _, LetDef v, _) -> Some (push_susp v (S.shift (i + 1 - o)))
| _ -> None
let assert_type e t t' =
@@ -151,7 +151,7 @@ let rec check ctx e =
| Builtin (_, t) -> t
(* FIXME: Check recursive references. *)
| Var v -> lookup_type ctx v
- | Susp (e, s) -> check ctx (unsusp e s)
+ | Susp (e, s) -> check ctx (push_susp e s)
| Let (_, defs, e)
-> let tmp_ctx =
L.fold_left (fun ctx (v, e, t)
=====================================
src/unification.ml
=====================================
--- a/src/unification.ml
+++ b/src/unification.ml
@@ -81,11 +81,11 @@ let zip_fold list1 list2 f =
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
+ let tmp = match (nosusp l, nosusp r) with
| (_, Metavar _) -> _unify_metavar r l subst
| (_, Call _) -> _unify_call r l subst
| (_, Case _) -> _unify_case r l subst
- | (_, Susp _) -> _unify_susp r l subst
+ | (_, Susp _) -> assert false
| (_, Let _) -> _unify_let r l subst
| (Imm _, _) -> _unify_imm l r subst
| (Cons _, _) -> _unify_cons l r subst
@@ -96,7 +96,7 @@ let rec unify (l: lexp) (r: lexp) (subst: substitution) : return_type =
| (Lambda _, _) -> _unify_lambda l r subst
| (Metavar _, _) -> _unify_metavar l r subst
| (Call _, _) -> _unify_call l r subst
- | (Susp _, _) -> _unify_susp l r subst
+ | (Susp _, _) -> assert false
| (Case _, _) -> _unify_case l r subst
| (Inductive _, _) -> _unfiy_induct l r subst
| (Sort _, _) -> _unify_sort l r subst
@@ -271,13 +271,6 @@ and _unify_call (call: lexp) (lxp: lexp) (subst: substitution) : return_type =
| None -> Debug_fun.debug_print_unify "_unify_call" call lxp " -> unification failed"; tmp
| Some _ -> Debug_fun.debug_print_unify "_unify_call" call lxp " -> unification success"; tmp
-(** Apply unsusp to the Susp and unify the result with the lexp
-*)
-and _unify_susp (susp_: lexp) (lxp: lexp) (subst: substitution) : return_type =
- match susp_ with
- | Susp _ -> unify (unsusp_all susp_) lxp subst
- | _ -> None
-
(** Unify a Case with a lexp
- Case, Case -> try to unify
- Case, _ -> Constraint
=====================================
tests/inverse_test.ml
=====================================
--- a/tests/inverse_test.ml
+++ b/tests/inverse_test.ml
@@ -21,13 +21,13 @@ open Fmt_lexp
open Debug_fun
let mkShift2 shift subst =
- S.Shift (subst, shift)
+ S.mkShift subst shift
let rec mkTestSubst lst =
match lst with
- | (var, shift)::tail -> S.Cons (mkVar var,
- mkShift2 shift (mkTestSubst tail))
- | [] -> S.Identity
+ | (var, shift)::tail -> S.cons (mkVar var)
+ (mkShift2 shift (mkTestSubst tail))
+ | [] -> S.identity
type result_type =
| Ok
@@ -42,10 +42,10 @@ let input =
((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(S.Identity, 3))), Ok)::
- ((S.Cons (mkVar 1, S.Cons (mkVar 3, S.Identity))), TransfoFail)::
- ((S.Shift (S.Shift (S.Identity, 3), 4)), Ok)::
- ((S.Shift (S.Cons (mkVar 1, S.Identity), 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)::
@@ -59,10 +59,7 @@ let is_identity s =
| S.Shift(S.Identity, shift) -> (acc = shift)
| S.Identity -> true
| _ -> false
- in match s with
- | S.Shift(S.Identity, _) -> true
- | S.Identity -> true
- | _ -> is_identity s 0
+ in is_identity s 0
let generateRandInput shiftMax numberOfTest =
Random.self_init ();
@@ -184,8 +181,8 @@ let _ = generate_tests "TRANSFORMATION"
(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)
+ | None, TransfoFail -> ((subst, S.identity), true)
| Some (s), _ -> ((subst, s), false)
- | None, _ -> ((subst, S.Identity), false))
+ | None, _ -> ((subst, S.identity), false))
let _ = run_all ()
View it on GitLab: https://gitlab.com/monnier/typer/commit/4e5049638ef74bcaa83598d6a10ca91dfe0…
1
0
BONNEVALLE Vincent pushed to branch unification at Stefan / Typer
Commits:
b291e84b by n3f4s at 2016-07-28T00:11:34+02:00
random (passing) test
- - - - -
1 changed file:
- tests/inverse_test.ml
Changes:
=====================================
tests/inverse_test.ml
=====================================
--- a/tests/inverse_test.ml
+++ b/tests/inverse_test.ml
@@ -64,20 +64,22 @@ let is_identity s =
| S.Identity -> true
| _ -> is_identity s 0
-let generateRandInput n m =
+let generateRandInput shiftMax numberOfTest =
Random.self_init ();
- let rec generateList n m =
- let rec generateRandInput n i =
- if n > i
+ let rec generateList shiftMax numberOfTest =
+ let rec generateRandInput shiftMax idx acc =
+ if idx < shiftMax
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))
+ then ( let r = Random.int shiftMax in
+ let shift = (min (r + idx + 1) (shiftMax))
+ in let shift = shift + (max 0 ((idx + shift) - acc))
+ in (idx, shift)::(generateRandInput shiftMax (idx + 1) (shift + acc)) )
+ else generateRandInput shiftMax (idx + 1) acc)
else []
- in if m >= 0
- then (mkTestSubst (generateRandInput n 0))::(generateList n (m - 1))
+ in if numberOfTest >= 0
+ then (mkTestSubst (generateRandInput shiftMax 0 0))::(generateList shiftMax (numberOfTest - 1))
else []
- in generateList n m
+ in generateList shiftMax numberOfTest
let lxp = mkVar 3
@@ -154,6 +156,20 @@ let _ = generate_tests "INVERSION"
| _ -> true)))
)
+(* 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)
+ ))
+
let _ = generate_tests "TRANSFORMATION"
(fun () -> input)
(fun subst ->
View it on GitLab: https://gitlab.com/monnier/typer/commit/b291e84bae35b15e0ed5a75c095abbff21b…
1
0
[Git][monnier/typer][unification] 3 commits: add error in inverse for subst with same index
by BONNEVALLE Vincent 27 Jul '16
by BONNEVALLE Vincent 27 Jul '16
27 Jul '16
BONNEVALLE Vincent pushed to branch unification at Stefan / Typer
Commits:
03221c91 by n3f4s at 2016-07-27T23:25:05+02:00
add error in inverse for subst with same index
- - - - -
ead6631f by n3f4s at 2016-07-27T23:26:20+02:00
better comparison against Id in tests
- - - - -
523c1f4d by n3f4s at 2016-07-27T23:26:58+02:00
better testing for INVERSE & TRANSFORMATION
- - - - -
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
@@ -72,8 +72,8 @@ let flatten (s: lexp S.subst): lexp S.subst option =
| 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)
+ | None -> None
+ | Some o -> if idx >= o then None else Some o)
| _ -> assert false
in
match flattenIr (toIr s) with
@@ -112,7 +112,7 @@ 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 =
+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)
in
let rec fill_before (l: (int * int) list): (int * int) list =
@@ -120,8 +120,9 @@ let fill (l: (int * int) list) (size: int) (acc: (int * int) list): (int * int)
| [] -> []
| (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 =
+ and fill_after (l: (int * int) list) (size: int) (acc: (int * int) list): (int * int) list 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
@@ -129,9 +130,9 @@ let fill (l: (int * int) list) (size: int) (acc: (int * int) list): (int * int)
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
+ 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
@@ -171,6 +172,7 @@ let rec inverse (subst: lexp S.subst ) : lexp S.subst option =
| 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
+ in match fill (sort cons_lst) shift_val [] with
+ | None -> None
+ | Some cons_lst -> to_cons cons_lst size
=====================================
tests/inverse_test.ml
=====================================
--- a/tests/inverse_test.ml
+++ b/tests/inverse_test.ml
@@ -29,22 +29,41 @@ 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)::[]))::
- (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)))::
- (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 ?*)
+ ((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(S.Identity, 3))), Ok)::
+ ((S.Cons (mkVar 1, S.Cons (mkVar 3, S.Identity))), TransfoFail)::
+ ((S.Shift (S.Shift (S.Identity, 3), 4)), Ok)::
+ ((S.Shift (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)::
[]
+let is_identity s =
+ let rec is_identity s acc =
+ match s with
+ | S.Cons(Var(_, idx), s1) when idx = acc -> is_identity s1 (acc + 1)
+ | S.Shift(S.Identity, shift) -> (acc = shift)
+ | S.Identity -> true
+ | _ -> false
+ in match s with
+ | S.Shift(S.Identity, _) -> true
+ | S.Identity -> true
+ | _ -> is_identity s 0
+
let generateRandInput n m =
Random.self_init ();
let rec generateList n m =
@@ -116,19 +135,23 @@ let get_dim lst =
let _ = generate_tests "INVERSION"
(fun () -> input)
fmt_res
- (fun s -> ( match inverse s, flatten s with
+ (fun (s, b) -> ( 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)
+ 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"),
- false )
- | None, Some(sf) -> ((string_of_subst s, string_of_subst sf, "None", "None"),
- false )
- | _ -> ((string_of_subst s, "None", "None", "None"),
- false ))
+ | 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)))
)
let _ = generate_tests "TRANSFORMATION"
@@ -142,8 +165,11 @@ let _ = generate_tests "TRANSFORMATION"
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, S.Identity), false))
+ (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 ()
View it on GitLab: https://gitlab.com/monnier/typer/compare/65bbe6d12d2c516eeccd061436c50dae12…
1
0
[Git][monnier/typer][unification] 6 commits: apply the Shift on Id instead of the whole subst
by BONNEVALLE Vincent 27 Jul '16
by BONNEVALLE Vincent 27 Jul '16
27 Jul '16
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/4282321b68032b4ecc2496164905fcadc5…
1
0
26 Jul '16
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/629fa172c788c3bc0cf590f3c854955746…
1
0
[Git][monnier/typer][unification] 5 commits: better output for subst
by BONNEVALLE Vincent 21 Jul '16
by BONNEVALLE Vincent 21 Jul '16
21 Jul '16
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/0461e108945d89232822e1b44a244765c7…
1
0
[Git][monnier/typer][unification] 2 commits: Dummy variable have index shift+1 instead of -1
by BONNEVALLE Vincent 20 Jul '16
by BONNEVALLE Vincent 20 Jul '16
20 Jul '16
BONNEVALLE Vincent pushed to branch unification at Stefan / Typer
Commits:
37f21f32 by n3f4s at 2016-07-20T16:58:41+02:00
Dummy variable have index shift+1 instead of -1
- - - - -
0461e108 by n3f4s at 2016-07-20T17:01:45+02:00
add generation of random test
- - - - -
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
@@ -2,11 +2,6 @@
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
*)
@@ -41,7 +36,7 @@ let toIr (s: lexp S.subst) : inter_subst =
or in ocaml-ish representation :
- - S.Cons(var, S.Shift(S.Identity, offset))::...::Identity -> S.Shift(S.Cons(var, S.Cons(...)), x1+x2+x3...)
+ - <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 rec flattenCons s =
@@ -62,7 +57,7 @@ let flattenIr (s: inter_subst) =
or in ocaml-ish representation :
- - S.Cons(var, S.Shift(..., offset)) -> S.Shift(S.Cons(var, S.Cons(...)), x1+x2+x3...)
+ - <code>S.Cons(var, S.Shift(..., offset)) -> S.Shift(S.Cons(var, S.Cons(...)), x1+x2+x3...)</code>
*)
let flatten (s: lexp S.subst) = flattenIr (toIr s)
@@ -100,9 +95,9 @@ let rec nthOf s i =
let idxOf (_, idx) = idx
(** Returns a list of couple (X, -1) where X go from beg_ to end_*)
-let rec genDummyVar beg_ end_ =
+let rec genDummyVar beg_ end_ idx =
if beg_ < end_
- then (beg_, -1)::(genDummyVar (beg_ + 1) end_)
+ then (beg_, idx)::(genDummyVar (beg_ + 1) end_ idx)
else []
(** Returns a dummy variable with the db_index idx
@@ -117,7 +112,7 @@ let rec generate_s l =
| [] -> S.Identity
(* With the exemple of the article :
- should return (1,1)::(3,2)::(4,3)::[]
+ should return <code>(1,1)::(3,2)::(4,3)::[]</code>
*)
let rec genCons s i =
match s with
@@ -125,9 +120,11 @@ let rec genCons s i =
| S.Identity -> []
(* With the exemple of the article :
- should return (1,1)::(2, X)::(3,2)::(4,3)::(5, Z)::[]
+ should return <code>(1,1)::(2, X)::(3,2)::(4,3)::(5, Z)::[]</code>
*)
let fill l size acc =
+ let genDummyVar beg_ end_ = genDummyVar beg_ end_ (size + 1)
+ in
let rec fill_before l =
match l with
| [] -> []
@@ -151,7 +148,9 @@ let fill l size acc =
*)
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 *)
+(** <code>s:S.subst -> l:lexp -> s':S.subst</code> where <code>l[s][s'] = l</code>
+ Return undefined result for bad input
+*)
let rec inverse (subst: lexp S.subst ) : lexp S.subst option =
match flatten subst with
| Some(S.Shift(flattened, shift)) ->
=====================================
tests/inverse_test.ml
=====================================
--- a/tests/inverse_test.ml
+++ b/tests/inverse_test.ml
@@ -29,33 +29,96 @@ 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)::(5, 0)::[]))::
+ (mkTestSubst ((0, 3)::(1, 2)::(4, 1)::(9, 0)::[])):: (* Erroneous result -> normal ?*)
(S.Cons (mkVar 1, S.Shift(S.Identity, 3)))::
[]
+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))
+ else []
+ in generateList n m
+
let lxp = mkVar 3
-let inputs = List.map (fun s ->
+let test input = 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")))
+ | 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 inputs = test 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 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 ()))
- inputs
+ 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 _ = run_all ()
View it on GitLab: https://gitlab.com/monnier/typer/compare/27fc552db4dc7ccc9c0a3f3cea5e3e9f5f…
1
0