Commit 3582da47 authored by Frontull Samuel's avatar Frontull Samuel
Browse files

bugfix concatenation prepended instead of append

parent 0a661bd3
......@@ -24,10 +24,10 @@ let s_empty = "(/x a b.x)"
let t_empty = tree_of_string s_empty
let s_at = "(/z./x y.x)"
let t_af = tree_of_string s_at
let t_at = tree_of_string s_at
let s_af = "(/z./x y.y)"
(* let t_af = tree_of_string s_af *)
let t_af = tree_of_string s_af
let s_concat = "(/y z x a b.y (z x a b) a b)"
let t_concat = tree_of_string s_concat
......@@ -50,29 +50,20 @@ let t_and = tree_of_string s_and
let s_or = "(/x y.x x y)"
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 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 _eq_str = "(/r 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) (r ("^s_tl^" x) ("^s_tl^" y))))"
let s_eq_str = ("(/a b."^s_ycomb^" " ^_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 x)) ((/x a b.a x))") *)
let _isprefix = "(/r x y."^s_ite^" ("^s_isempty^" x) ("^s_true^") ("^s_and^" ("^s_hd_eq^" x y) (r ("^s_tl^" x) ("^s_tl^" y))))"
let s_isprefix = ("(/a b."^s_ycomb^" " ^_isprefix ^ " a b)")
let t_isprefix = tree_of_string s_isprefix
(* let tmp = tree_of_string (s_isprefix ^ " ((/x a b.x)) ((/x a b.x))") *)
(* LISTS *)
let s_cons = "(/x y.(/a b c.c a b) (/x y.y) ((/a b c.c a b) x y))"
......@@ -109,13 +100,13 @@ let s_mkpair = "(/x y." ^ s_pair ^ " x y)"
let t_mkpair = tree_of_string s_mkpair
(* LIST OF TILES *)
let s_tile1 = "(" ^ s_mkpair ^ " (/x a b.a x) (/x a b.b x))"
(* let s_tile1 = "(" ^ s_mkpair ^ " (/x a b.a (b x)) (/x a b.a x))"
let t_tile1 = tree_of_string s_tile1
let s_tile2 = "(" ^ s_mkpair ^ " (/x a b.a x) (/x a b.b x))"
let s_tile2 = "(" ^ s_mkpair ^ " (/x a b.a x) (/x a b.b (a x)))"
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_tile2 ^ " (" ^ s_cons ^ " " ^ s_tile1 ^ " " ^ s_nil ^ "))" *)
(* let s_tile1 = "(" ^ s_mkpair ^ " (/x a b.b (b (a x))) (/x a b.b x))"
let t_tile1 = tree_of_string s_tile1
......@@ -126,33 +117,25 @@ let t_tile2 = tree_of_string s_tile2
let s_tile3 = "(" ^ s_mkpair ^ " (/x a b.b x) (/x a b.a (b x)))"
let t_tile3 = tree_of_string s_tile3 *)
(* let s_tile1 = "(" ^ s_mkpair ^ " (/x a b.b x) (/x a b.b (b (b x))))"
let s_tile1 = "(" ^ s_mkpair ^ " (/x a b.b (a (a x))) (/x a b.b x))"
let t_tile1 = tree_of_string s_tile1
let s_tile2 = "(" ^ s_mkpair ^ " (/x a b.b (a (b (b (b x))))) (/x a b.b (a x)))"
let s_tile2 = "(" ^ s_mkpair ^ " (/x a b.a x) (/x a b.b (a (a x))))"
let t_tile2 = tree_of_string s_tile2
let s_tile3 = "(" ^ s_mkpair ^ " (/x a b.b (a x)) (/x a b.a x))"
let s_tile3 = "(" ^ s_mkpair ^ " (/x a b.b x) (/x a b.a (a x)))"
let t_tile3 = tree_of_string s_tile3
let s_tiles = "(" ^ s_cons ^ " " ^ s_tile3 ^ " (" ^ s_cons ^ " " ^ s_tile2 ^ " (" ^ s_cons ^ " " ^ s_tile1 ^ " " ^ s_nil ^ ")))" *)
let s_tiles = "(" ^ s_cons ^ " " ^ s_tile3 ^ " (" ^ s_cons ^ " " ^ s_tile2 ^ " (" ^ s_cons ^ " " ^ s_tile1 ^ " " ^ s_nil ^ ")))"
let t_tiles = tree_of_string s_tiles
(* let tmp = Core.AApp(Core.AApp(t_filter,t_pcppair,UnT),t_tiles,UnT) *)
(* find if for (t1,t2), t1 = t2 in list of tuples *)
(* "/r x.ite (isnil x) (false) (or (eq_str (fst (lhd x)) (snd (lhd x))) (r (tl x)))" *)
let s__find_eq = "(/r xs."^s_ite^" ("^s_isnil^" xs) "^s_false^" ("^s_or^" ("^s_eq_str^" ("^s_first^" ("^s_lhd^" xs)) ("^s_second^" ("^s_lhd^" xs))) (r ("^s_ltl^" xs))))"
let s_find_eq = "(/xs."^s_ycomb^" "^s__find_eq^" xs)"
let t_find_eq = tree_of_string s_find_eq
(* 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 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 ys."^s_ycomb^" "^s__combine^" x ys)"
let t_combine = tree_of_string s_combine
......@@ -160,40 +143,24 @@ let t_combine = tree_of_string s_combine
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_filter^" "^s_pcppair^" ("^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_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(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) *)
(* 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) *)
(* 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 ts."^s_ite^" ("^s_find_eq^" xs) ("^s_true^") (r ("^s_cross_append^" xs ts) ts))" *)
let s__pcp = "(/r xs ts."^s_ite^" ("^s_isnil^" xs) ("^s_false^") ("^s_ite^" ("^s_find_eq^" xs) ("^s_true^") (r ("^s_cross_append^" xs ts) ts)))"
let s_pcp = "(/ts."^s_ycomb^" "^s__pcp^" ts ts)"
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_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) *)
(* let tmp = Core.AApp(Core.AApp(t_cross_append,
Core.AApp(Core.AApp(t_filter, t_pcppair, UnT), Core.AApp(Core.AApp(t_cross_append, t_tiles, UnT), t_tiles, UnT), UnT),
UnT), t_tiles, UnT)
(* let tmp = Core.AApp(Core.AApp(t_cross_append, t_tiles, UnT), Core.AApp(Core.AApp(t_cross_append, t_tiles, UnT), t_tiles, UnT), UnT) *) *)
let pcpp = tree_of_string (s_pcp ^" "^s_tiles^" y")
let () =
Printf.printf "PCP file.\n";
(* Printf.printf "%s\n\n" (Core.a_term_to_string tmp); *)
Printf.printf "PCP\n";
Printf.printf "-----------------------------\n%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);
(* Printf.printf "pcp2: %s\n" (s_pcp2); *)
Printf.printf "res_pcp2: %s\n" (Core.a_term_to_string res_pcp2); *)
(* Printf.printf "pcpp: %s\n" (Core.a_term_to_string (Core.nf Core.casubst pcpp)); *)
Printf.printf "Alpha conversions: %d\n" (!Core.counter);
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