Lambda.mtcr

"xi : (a -> a -> b) -> a -> b"
[define xi (x i)]

"pass : a -> (a -> b) -> b"
[define pass (c (s (k i)))]

"and-pred : Predicate -> Predicate -> Predicate"
[define and-pred (b (b (s pass)) (b (b (pass (k false))) (b (b c) c)))]

"if-pred : Predicate -> (Struct -> Struct) -> (Struct -> Struct) -> Struct -> Struct"
[define if-pred (b (b (b xi)) (b (b c) c))]

"hard-parse : String -> Any"
[define hard-parse (b (get-field 0) parse)]

"one-two-same? : Struct -> Boolean"
[define one-two-same? (s (b symbol-eq? (get-field 0)) (get-field 1))]

"lambda-tag? : Struct -> Boolean"
[define lambda-tag? (b (symbol-eq? [quote lambda]) tag-of)]

"lambda? : Struct -> Boolean"
[define lambda? (and-pred lambda-tag? (b (nat-eq? 2) struct-size))]

"pair? : Struct -> Boolean"
[define pair? (b (symbol-eq? [quote pair]) type-of)]

"is-id? : Struct -> Boolean"
[define is-id? (and-pred lambda? one-two-same?)]

"rec-ap : Struct -> Struct"
"[define rec-ap (s (b pair (b abstr-elim _1)) (b abstr-elim _2))]"
[define rec-ap (s (b pair _1) _2)]

"ap-to-ap : (Struct -> Struct) -> Struct -> Struct"
[define ap-to-ap (if-pred pair? rec-ap)]

"id-to-i : (Struct -> Struct) -> Struct -> Struct"
[define id-to-i (if-pred is-id? (k [quote i]))]

"abstr-elim : Struct -> Struct"
[define abstr-elim (id-to-i (ap-to-ap i))]

"parse-+-elim : String -> Any"
[define parse-+-elim (b abstr-elim hard-parse)]

(parse-+-elim "[lambda x y]")
(parse-+-elim "([lambda x x] [lambda x x])")