Commit 408a4e34 authored by Frontull Samuel's avatar Frontull Samuel
Browse files

pcp done

parent d5d0840d
......@@ -848,7 +848,7 @@ let rec size term =
| AApp (e1, e2, t) -> 1 + size e1 + size e2
let rec nf subst term =
(* Printf.printf "%d\n" (size term); *)
(* Printf.printf "%d %s\n" (size term) (a_term_to_string term); *)
let new_term = reduce_lo subst term in
if new_term = term then term else nf subst new_term
......
......@@ -71,7 +71,7 @@ let _eq_str = "(/rec x y."^s_ite^" ("^s_or^" ("^s_isempty^" x) ("^s_isempty^" 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.b (b x))) ((/x a b.b (a x)))") *)
(* let tmp = tree_of_string (s_eq_str ^ " ((/x a b.a x)) ((/x a 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))"
......@@ -100,9 +100,6 @@ let s_baba = "(/x a b.b (a (b (a x))))"
(* LIST with TUPLE (e,e) *)
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_tile1 = "(" ^ s_mkpair ^ " (/x a b.a x) (/x a b.a (b (b x))))"
......@@ -131,35 +128,6 @@ 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))
(/c.(c (/c.(c (/x./a./b.b (b x)))
(/x./a./b.a (b (a (b x)))))) (/c.(c (/x./y.y))
(/c.(c (/c.(c (/x./a./b.a (b x)))
(/x./a./b.b (b (b (a (b x))))))) (/c.(c (/x./y.y))
(/c.(c (/c.(c (/x./a./b.b (b (a (b x)))))
(/x./a./b.b (a (b x))))) (/c.(c (/x./y.y))
(/c.(c (/c.(c (/x./a./b.b (a x)))
(/x./a./b.a (b (b (b (b x))))))) (/c.(c (/x./y.y))
(/c.(c (/c.(c (/x./a./b.a (a x)))
(/x./a./b.b (b (b (b (b (b x)))))))) (/c.(c (/x./y.y))
(/c.(c (/c.(c (/x./a./b.b (b (a (a x)))))
(/x./a./b.b (b (b (b x)))))) (/c.(c (/x./y.y))
(/c.(c (/c.(c (/x./a./b.b (b (b (a x)))))
(/x./a./b.a (b (b x))))) (/c.(c (/x./y.y))
(/c.(c (/c.(c (/x./a./b.a (b (b (a x)))))
(/x./a./b.b (b (b (b x)))))) (/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(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)))"
......@@ -182,7 +150,7 @@ let t_cross_append = tree_of_string s_cross_append
(* 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 = Core.AApp(t_find_eq, 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_tiles, UnT), UnT), t_tiles, UnT), UnT), t_tiles, UnT), UnT) *)
(* let tmp = t_tiles *)
(* let tmp = Core.AApp(t_first, Core.AApp(t_lhd, Core.AApp(Core.AApp(t_cross_append, t_tiles, UnT), t_tiles, UnT), UnT), UnT) *)
(* 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) *)
......@@ -194,24 +162,14 @@ let t_cross_append = tree_of_string s_cross_append
(* 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)"
(* 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 = "(/r xs tiles."^s_ite^" ("^s_find_eq^" xs) ("^s_true^") (r ("^s_cross_append^" xs tiles) tiles))"
let s_pcp = "(/tiles."^s_ycomb^" "^s__pcp^" tiles tiles)"
let t_pcp = tree_of_string s_pcp
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)"
let tmp = Core.AApp(all_a, s_baba, UnT)
let res_all_a = Core.nf (Core.casubst) tmp
let tmp = Core.AApp(Core.AApp(eq_str, s_baba, UnT), s_baba, UnT)
let res_eq_str = Core.nf (Core.casubst) tmp *)
(* let tmp = Core.AApp(t_find_eq, Core.AApp(Core.AApp(t_cross_append, Core.AApp(Core.AApp(t_cross_append, t_tiles, UnT), t_tiles, UnT), UnT), t_tiles, UnT), 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_listtuple_ee, UnT), t_tiles, UnT), UnT), t_tiles, UnT), UnT), t_tiles, UnT) *)
(* PCP2 *)
(* let s_t1_2 = "(/x a b.a x)"
......@@ -251,7 +209,7 @@ let res_pcp3 = Core.nf (Core.casubst) pcp3 *)
let () =
Printf.printf "PCP file.\n";
(* Printf.printf "%s\n\n" s_pcp; *)
(* Printf.printf "%s\n\n" (Core.a_term_to_string tmp); *)
Printf.printf "res_tmp: %s\n" (Core.a_term_to_string (Core.nf Core.casubst tmp));
(* Printf.printf "res_all_a: %s\n" (Core.a_term_to_string res_all_a);
Printf.printf "res_eq_str: %s\n" (Core.a_term_to_string res_eq_str);
......
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