Commit d5d0840d authored by Frontull Samuel's avatar Frontull Samuel
Browse files

error found?

parent ad4a88bc
......@@ -37,10 +37,13 @@ let t_prepa = tree_of_string "(/s x a b.a (s x a b))"
let t_prepb = tree_of_string "(/s x a b.b (s x a b))"
let t_nexta = tree_of_string "(/x.(/a b c.c a b) ((/s x a b.a (s x a b)) ((/p.p (/x y.x)) x)) ((/p.p (/x y.x)) x))"
let t_nextb = tree_of_string "(/x.(/a b c.c a b) ((/s x a b.b (s x a b)) ((/p.p (/x y.x)) x)) ((/p.p (/x y.x)) x))"
let t_tl = tree_of_string "(/s.(/p.p (/x y.y)) (s ((/a b c.c a b) (/x a b.x) (/x a b.x)) (/x.(/a b c.c a b) ((/s x a b.a (s x a b)) ((/p.p (/x y.x)) x)) ((/p.p (/x y.x)) x)) (/x.(/a b c.c a b) ((/s x a b.b (s x a b)) ((/p.p (/x y.x)) x)) ((/p.p (/x y.x)) x))))"
let s_tl = "(/s.(/p.p (/x y.y)) (s ((/a b c.c a b) (/x a b.x) (/x a b.x)) (/x.(/a b c.c a b) ((/s x a b.a (s x a b)) ((/p.p (/x y.x)) x)) ((/p.p (/x y.x)) x)) (/x.(/a b c.c a b) ((/s x a b.b (s x a b)) ((/p.p (/x y.x)) x)) ((/p.p (/x y.x)) x))))"
let t_tl = tree_of_string s_tl
let t_hd = tree_of_string "(/s x a b.s x (/y.a x) (/y.b x))"
let t_hd_a = tree_of_string "(/s.s (/x y.y) (/x./x y.x) (/x./x y.y))"
let t_hd_b = tree_of_string "(/s.s (/x y.y) (/x./x y.x) (/x./x y.x))"
let s_hd_a = "(/s.s (/x y.y) (/x./x y.x) (/x./x y.y))"
let t_hd_a = tree_of_string s_hd_a
let s_hd_b = "(/s.s (/x y.y) (/x./x y.y) (/x./x y.x))"
let t_hd_b = tree_of_string s_hd_b
let t_is_e = tree_of_string "(/s.s (/x y.x) (/x./x y.y) (/x./x y.y))"
let s_and = "(/x y.x y x)"
let t_and = tree_of_string s_and
......@@ -50,18 +53,25 @@ let t_or = tree_of_string s_or
(* let tmp = tree_of_string (s_or ^ " (/x y.x) (/x y.y)") *)
(* let tmp = tree_of_string ("(/x y.x y x) (" ^ s_isempty ^ " (/x a b.x)) (" ^ s_isempty ^ " (/x a b.a x))") *)
let t_hd_eq = tree_of_string "(/x y.(/x y.x x y) ((/x y.x y x) ((/s.s (/x y.y) (/x./x y.x) (/x./x y.y)) x) ((/s.s (/x y.y) (/x./x y.x) (/x./x y.y)) y)) ((/x y.x y x) ((/s.s (/x y.y) (/x./x y.x) (/x./x y.x)) x) ((/s.s (/x y.y) (/x./x y.x) (/x./x y.x)) y)))"
(* let s_hd_eq = "(/x y.(/x y.x x y) ((/x y.x y x) ((/s.s (/x y.y) (/x./x y.x) (/x./x y.y)) x) ((/s.s (/x y.y) (/x./x y.x) (/x./x y.y)) y)) ((/x y.x y x) ((/s.s (/x y.y) (/x./x y.x) (/x./x y.x)) x) ((/s.s (/x y.y) (/x./x y.x) (/x./x y.x)) y)))" *)
let s_hd_eq = "(/x y."^s_or^" ("^s_and^" ("^s_hd_a^" x) ("^s_hd_a^" y)) ("^s_and^" ("^s_hd_b^" x) ("^s_hd_b^" y)))"
let t_hd_eq = tree_of_string s_hd_eq
(* let tmp = tree_of_string (s_hd_a ^ " ((/x a b.(b x)))") *)
(* let tmp = tree_of_string (s_hd_b ^ " ((/x a b.(a x)))") *)
(* let tmp = tree_of_string (s_hd_eq ^ " ((/x a b.(b x))) ((/x a b.(a x)))") *)
let s_ycomb = "(/f.(/x.f (x x)) (/x.f (x x)))"
let t_ycomb = tree_of_string s_ycomb
let s_zcomb = "(/f.(/x.f (/y.x x y)) (/x.f (/y.x x y)))"
let t_zcomb = tree_of_string s_zcomb
let _eq_str = "(/rec x y.(/c a b.c a b) ((/x y.x x y) ((/s.(s (/x y.x)) (/x./x y.y) (/x./x y.y)) x) ((/s.(s (/x y.x)) (/x./x y.y) (/x./x y.y)) y)) ((/x y.x y x) ((/s.(s (/x y.x)) (/x./x y.y) (/x./x y.y)) x) ((/s.(s (/x y.x)) (/x./x y.y) (/x./x y.y)) y)) ((/x y.x y x) ((/x y.(/x y.x x y) ((/x y.x y x) ((/s.s (/x y.y) (/x./x y.x) (/x./x y.y)) x) ((/s.s (/x y.y) (/x./x y.x) (/x./x y.y)) y)) ((/x y.x y x) ((/s.s (/x y.y) (/x./x y.x) (/x./x y.x)) x) ((/s.s (/x y.y) (/x./x y.x) (/x./x y.x)) y))) x y) (rec ((/s.(/p.p (/x y.y)) (s ((/a b c.c a b) (/x a b.x) (/x a b.x)) (/x.(/a b c.c a b) ((/s x a b.a (s x a b)) ((/p.p (/x y.x)) x)) ((/p.p (/x y.x)) x)) (/x.(/a b c.c a b) ((/s x a b.b (s x a b)) ((/p.p (/x y.x)) x)) ((/p.p (/x y.x)) x)))) x) ((/s.(/p.p (/x y.y)) (s ((/a b c.c a b) (/x a b.x) (/x a b.x)) (/x.(/a b c.c a b) ((/s x a b.a (s x a b)) ((/p.p (/x y.x)) x)) ((/p.p (/x y.x)) x)) (/x.(/a b c.c a b) ((/s x a b.b (s x a b)) ((/p.p (/x y.x)) x)) ((/p.p (/x y.x)) x)))) y))))";;
let _eq_str = "(/rec x y."^s_ite^" ("^s_or^" ("^s_isempty^" x) ("^s_isempty^" y)) ("^s_and^" ("^s_isempty^" x) ("^s_isempty^" y)) ("^s_and^" ("^s_hd_eq^" x y) (rec ("^s_tl^" x) ("^s_tl^" y))))";;
let s_eq_str = ("(/a b.(/f.(/x.f (x x)) (/x.f (x x))) " ^_eq_str ^ " a b)");;
let eq_str = tree_of_string s_eq_str;;
(* let tmp = tree_of_string (s_eq_str ^ " ((/x a b.a (b x))) ((/x a b.a (b x)))") *)
(* let tmp = tree_of_string (s_eq_str ^ " ((/x a b.b (b x))) ((/x a b.b (a x)))") *)
(* LISTS *)
let s_cons = "(/x y.(/a b c.c a b) (/x y.y) ((/a b c.c a b) x y))"
......@@ -121,7 +131,7 @@ let s__find_eq = "(/r xs."^s_ite^" ("^s_isnil^" xs) "^s_false^" ("^s_or^" ("^s_e
let s_find_eq = "(/xs."^s_ycomb^" "^s__find_eq^" xs)"
let t_find_eq = tree_of_string s_find_eq
let ttt = "/c.(c (/x./y.y))
(* let ttt = "/c.(c (/x./y.y))
(/c.(c (/c.(c (/x./a./b.b (b x)))
(/x./a./b.a (b (a (b x)))))) (/c.(c (/x./y.y))
......@@ -149,8 +159,8 @@ let ttt = "/c.(c (/x./y.y))
(/c.(c (/c.(c (/x./a./b.b (b (a (b (b (a x)))))))
(/x./a./b.b (b x)))) (/x.x))))))))))))))))))
"
let tmp = Core.AApp(Core.AApp(eq_str,(tree_of_string "(/x./a./b.b (b (a (a x))))"),UnT),(tree_of_string "(/x./a./b.b (b (b (b x))))"),UnT)
(* let tmp = Core.AApp(t_find_eq, (tree_of_string ttt), UnT) *)
let tmp = Core.AApp(t_find_eq, (tree_of_string ttt), UnT) *)
(* let tmp = Core.AApp(Core.AApp(eq_str,(tree_of_string "(/x./a./b.b (b (a (a x))))"),UnT),(tree_of_string "(/x./a./b.b (b (b (b x))))"),UnT) *)
let s_concat_pairs = "(/s p."^s_mkpair^" ("^s_concat^" ("^s_first^" p) ("^s_first^" s)) ("^s_concat^" ("^s_second^" p) ("^s_second^" s)))"
let t_concat_pairs = tree_of_string s_concat_pairs
......@@ -178,6 +188,7 @@ let t_cross_append = tree_of_string s_cross_append
(* let tmp = Core.AApp(t_second, Core.AApp(t_lhd, Core.AApp(Core.AApp(t_cross_append, t_tiles, UnT), t_tiles, UnT), UnT), UnT) *)
(* let tmp = Core.AApp(t_lhd,Core.AApp(t_ltl,Core.AApp(t_ltl,Core.AApp(t_ltl,Core.AApp(t_ltl,Core.AApp(t_ltl,Core.AApp(t_ltl,Core.AApp(t_ltl,Core.AApp(t_ltl,Core.AApp(t_ltl,Core.AApp(Core.AApp(t_cross_append, t_tiles, UnT), t_tiles, UnT), UnT), UnT), UnT), UnT), UnT), UnT), UnT), UnT), UnT), UnT) *)
(* let tmp = Core.AApp(t_find_eq,Core.AApp(Core.AApp(t_cross_append, t_listtuple_ee, UnT), t_listtuple_ee, UnT),UnT) *)
(* let tmp = Core.AApp(t_find_eq,Core.AApp(Core.AApp(t_cross_append, t_tiles, UnT), t_tiles, UnT),UnT) *)
(* let tmp = t_tiles *)
(* let tmp = Core.AApp(Core.AApp(t_mkpair,t_a,UnT),(Core.AApp(Core.AApp(t_concat,t_a,UnT),t_a,UnT)),UnT) *)
......@@ -187,7 +198,7 @@ let s__pcp = "(/r xs tiles."^s_ite^" ("^s_find_eq^" ("^s__cross_append^" xs tile
let s_pcp = "(/tiles."^s_ycomb^" "^s__pcp^" "^s_listtuple_ee^" tiles)"
let t_pcp = tree_of_string s_pcp
(* let tmp = Core.AApp(t_pcp, t_tiles, UnT) *)
let tmp = Core.AApp(t_pcp, t_tiles, UnT)
(* let tmp = Core.AApp(t_find_eq, Core.AApp(Core.AApp(t_cross_append, Core.AApp(Core.AApp(t_cross_append, t_listtuple_ee, UnT), t_tiles, UnT), UnT), t_tiles, UnT), UnT) *)
(* let _all_a = tree_of_string "(/f x.(/c a b.c a b) ((/s.(s (/x y.x)) (/x./x y.y) (/x./x y.y)) x) (/x y.x) ((/x y.x y x) ((/s.s (/x y.y) (/x./x y.x) (/x./x y.y)) x) (f ((/s.(/p.p (/x y.y)) (s ((/a b c.c a b) (/x a b.x) (/x a b.x)) (/x.(/a b c.c a b) ((/s x a b.a (s x a b)) ((/p.p (/x y.x)) x)) ((/p.p (/x y.x)) x)) (/x.(/a b c.c a b) ((/s x a b.b (s x a b)) ((/p.p (/x y.x)) x)) ((/p.p (/x y.x)) x)))) x))))"
let all_a = tree_of_string "(/a.(/f.(/x.f (x x)) (/x.f (x x))) (/f x.(/c a b.c a b) ((/s.(s (/x y.x)) (/x./x y.y) (/x./x y.y)) x) (/x y.x) ((/x y.x y x) ((/s.s (/x y.y) (/x./x y.x) (/x./x y.y)) x) (f ((/s.(/p.p (/x y.y)) (s ((/a b c.c a b) (/x a b.x) (/x a b.x)) (/x.(/a b c.c a b) ((/s x a b.a (s x a b)) ((/p.p (/x y.x)) x)) ((/p.p (/x y.x)) x)) (/x.(/a b c.c a b) ((/s x a b.b (s x a b)) ((/p.p (/x y.x)) x)) ((/p.p (/x y.x)) x)))) x)))) a)"
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment