Commit 13956d87 authored by Frontull Samuel's avatar Frontull Samuel
Browse files

pcp done

parent cf5b4d2b
......@@ -132,10 +132,10 @@ is_nil :: LCList a -> LCBool
is_nil = \l -> unList l (\h t -> false) true
-- -- List Head
-- hd_l :: LCList a -> a
-- hd_l = \x -> unList x true nil
hd_l = \l -> l (\h t -> h) nil
-- hd_l = \l -> unList l (\h t -> h) nil
hd_l :: (LCList a) -> a
unit = ()
diverge = \u -> ycomb (\x -> x)
hd_l = \l -> (unList l (\h t u -> h) (diverge)) unit
-- List Tail
next_l = \h p -> pair (cons h (first p)) (first p)
......@@ -143,8 +143,34 @@ next_l = \h p -> pair (cons h (first p)) (first p)
tl_l :: LCList a -> LCList a
tl_l = \l -> second (unList l next_l (pair nil nil))
lent = ycomb (\f x -> ite (is_nil x) 0 (1 + (f (tl_l x))))
-- flat = ycomb (\f x -> ite (is_nil x) "" ((hd_l x) ++ (f (tl_l x))))
append :: LCList a -> LCList a -> LCList a
append = \x y -> LCList $ \c n -> unList x c (unList y c n)
-- lent = ycomb (\f x -> ite (is_nil x) 0 (1 + (f (tl_l x))))
--
-- flat :: LCList String -> String
-- flat = (ycomb (\f x -> ite (is_nil x) "" ((hd_l x) ++ (f (tl_l x))))) (cons "as" nil)
-- PCP
simp' :: (LCStr -> LCStr -> (LCStr -> LCStr -> a) -> a)
-> LCStr -> LCStr -> (LCStr -> LCStr -> a) -> a
simp' = \f x y -> ite (lor (isempty x) (isempty y)) (pair x y) (f (tl x) (tl y))
simp :: ((a1 -> a1 -> a1) -> LCStr) -> (LCStr -> LCStr -> a) -> a
simp = \p -> ycomb simp' (first p) (second p)
pvalid = \p -> lor (prefix (first p) (second p)) (prefix (second p) (first p))
find_eq = ycomb (\f x -> ite (is_nil x) false (lor (eq (first (hd_l x)) (second (hd_l x))) (f (tl_l x))))
cmb = \p s -> pair (conc (first p) (first s)) (conc (second p) (second s))
map_cmb = ycomb (\f x y -> ite (is_nil y) nil (ite (pvalid (cmb x (hd_l y))) (cons (simp (cmb x (hd_l y))) (f x (tl_l y))) (f x (tl_l y))))
cross_cmb = ycomb (\f x y -> ite (is_nil x) nil (append (map_cmb (hd_l x) y) (f (tl_l x) y)))
pcp' = \f x y -> ite (is_nil x) false (ite (find_eq x) true (f (cross_cmb x y) y))
pcp = \x -> ycomb pcp' x x
lcstr_tostr :: LCStr -> String
lcstr_tostr = \s -> unChurch s ("") (\a -> "a" ++ a) (\b -> "b" ++ b)
......
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