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

pcp

parent 6ba3bce5
......@@ -65,22 +65,38 @@ let t_nil = tree_of_string s_nil
let s_isnil = "(/p.p (/x y.x))"
let t_isnil = tree_of_string s_isnil
(* STRINGS *)
let s_e = "(/x a b.x)"
let t_e = tree_of_string s_e
let s_a = "(/x a b.a x)"
let t_a = tree_of_string s_a
let s_b = "(/x a b.b x)"
let s_ab = "(/x a b.a (b x))"
let s_aa = "(/x a b.a (a x))"
let s_ba = "(/x a b.b (a x))"
let s_baba = "(/x a b.b (a (b (a x))))"
(* LIST with TUPLE (e,e) *)
let s_mktuple = "(/x y." ^ s_pair ^ " x y)"
let s_tuple_ee = "(" ^ s_mktuple ^ " " ^ s_empty ^ " " ^ s_empty ^ ")"
let s_mkpair = "(/x y." ^ s_pair ^ " x y)"
let t_mkpair = tree_of_string s_mkpair
let s_tuple_ee = "(" ^ s_mkpair ^ " " ^ s_e ^ " " ^ s_e ^ ")"
let s_listtuple_ee = "(" ^ s_cons ^ " " ^ s_tuple_ee ^ " " ^ s_nil ^ ")"
let t_listtuple_ee = tree_of_string s_listtuple_ee
(* LIST OF TILES *)
let s_t1_2 = "(/x a b.a x)"
let s_b1_2 = "(/x a b.a (b (b x)))"
let s_tile1 = "(" ^ s_mktuple ^ " " ^ s_t1_2 ^ " " ^ s_b1_2 ^ ")"
let s_tile1 = "(" ^ s_mkpair ^ " " ^ s_t1_2 ^ " " ^ s_b1_2 ^ ")"
let t_tile1 = tree_of_string s_tile1
let s_t2_2 = "(/x a b.b x)"
let s_b2_2 = "(/x a b.x)"
let s_tile2 = "(" ^ s_mktuple ^ " " ^ s_t2_2 ^ " " ^ s_b2_2 ^ ")"
let s_tile2 = "(" ^ s_mkpair ^ " " ^ s_t2_2 ^ " " ^ s_b2_2 ^ ")"
let t_tile2 = tree_of_string s_tile2
let s_tiles = "(" ^ s_cons ^ " " ^ s_tile2 ^ " (" ^ s_cons ^ " " ^ s_tile1 ^ " " ^ s_nil ^ "))"
(* let s_tiles = "(" ^ s_cons ^ " " ^ s_tile1 ^ " " ^ s_nil ^ ")" *)
let t_tiles = tree_of_string s_tiles
(* find if for (t1,t2), t1 = t2 in list of tuples *)
......@@ -91,17 +107,32 @@ let t_find_eq = tree_of_string s_find_eq
(* let tmp = Core.AApp(t_find_eq, t_tiles, UnT) *)
let s_concat_pairs = "(/p s."^s_mktuple^" ("^s_concat^" ("^s_first^" p) ("^s_first^" s)) ("^s_concat^" ("^s_second^" p) ("^s_second^" s)))"
let s_concat_pairs = "(/p s."^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
(* let tmp = Core.AApp(Core.AApp(t_concat_pairs, t_tile1, UnT), t_tile2, UnT) *)
let s__combine = "(/r x ys."^s_ite^" ("^s_isnil^" ys) ("^s_nil^") ("^s_cons^" ("^s_concat_pairs^" x ("^s_lhd^" ys)) (r x ("^s_ltl^" ys))))"
let s_combine = "(/x y."^s_ycomb^" "^s__combine^" x y)"
let s_combine = "(/x ys."^s_ycomb^" "^s__combine^" x ys)"
let t_combine = tree_of_string s_combine
let s__cross_append = "(/r xs ys."^s_ite^" ("^s_isnil^" xs) ("^s_nil^") ("^s_cons^" ("^s_combine^" ("^s_lhd^" xs) ys) (r ("^s_ltl^" xs) ys)))"
let s_cross_append = "(/xs ys."^s_ycomb^" "^s__cross_append^" xs ys)"
let s__append = "(/r xs ys."^s_ite^" ("^s_isnil^" xs) ys ("^s_cons^" ("^s_lhd^" xs) (r ("^s_ltl^" xs) ys)))"
let s_append = "(/xs ys."^s_ycomb^" "^s__append^" xs ys)"
(* let tmp = Core.AApp(Core.AApp(t_combine, t_tile1, UnT), t_listtuple_ee, UnT) *)
let s__cross_append = "(/r xs ys."^s_ite^" ("^s_isnil^" xs) ("^s_nil^") ("^s_append^" ("^s_combine^" ("^s_lhd^" xs) ys) (r ("^s_ltl^" xs) ys)))"
let s_cross_append = "(/xs ys."^s_ycomb^" "^s__cross_append^" xs ys)"
let t_cross_append = tree_of_string s_cross_append
(* let tmp = Core.AApp(Core.AApp(t_cross_append, t_listtuple_ee, UnT), t_tiles, UnT) *)
(* let tmp = Core.AApp(Core.AApp(t_cross_append, t_tiles, UnT), t_listtuple_ee, UnT) *)
(* let tmp = Core.AApp(Core.AApp(t_cross_append, Core.AApp(Core.AApp(t_cross_append, t_tiles, UnT), t_listtuple_ee, UnT), UnT),t_listtuple_ee,UnT) *)
(* let tmp = Core.AApp(Core.AApp(t_cross_append, Core.AApp(Core.AApp(t_cross_append, Core.AApp(Core.AApp(t_cross_append, t_tiles, UnT), t_listtuple_ee, UnT), UnT), t_listtuple_ee, UnT), UnT), t_listtuple_ee, UnT) *)
(* let tmp = t_tiles *)
(* 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) *)
(* let tmp = Core.AApp(t_lhd, Core.AApp(Core.AApp(t_cross_append, t_tiles, UnT), t_listtuple_ee, UnT), UnT) *)
let s__pcp = "(/r xs tiles."^s_ite^" ("^s_find_eq^" ("^s__cross_append^" xs tiles)) "^s_true^" (r ("^s__cross_append^" xs tiles) tiles))"
let s_pcp = "(/tiles."^s_ycomb^" "^s__pcp^" "^s_listtuple_ee^" tiles)"
......@@ -109,17 +140,6 @@ let t_pcp = tree_of_string s_pcp
let tmp = Core.AApp(t_pcp, t_tiles, UnT)
(* STRINGS *)
let s_e = tree_of_string "(/x a b.x)"
let s_a = tree_of_string "(/x a b.a x)"
let s_b = tree_of_string "(/x a b.b x)"
let s_ab = tree_of_string "(/x a b.a (b x))"
let s_aa = tree_of_string "(/x a b.a (a x))"
let s_ba = tree_of_string "(/x a b.b (a x))"
let s_baba = tree_of_string "(/x a b.b (a (b (a x))))"
(* 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