Huh?
This commit is contained in:
@@ -47,41 +47,18 @@ substBrExp =
|
|||||||
|
|
||||||
substExp :: Exp
|
substExp :: Exp
|
||||||
substExp =
|
substExp =
|
||||||
parse
|
subst (Variable "if") ifExp .
|
||||||
"( \\map. \\substBr. \\elem. \\equal. \\if. \\var. \\e. rec subst = \\x. case x of\
|
subst (Variable "equal") equalExp .
|
||||||
\ { Apply(e1,e2) -> Apply(subst e1, subst e2) \
|
subst (Variable "substBr") substBrExp .
|
||||||
\ ; Lambda(x,y) -> if (equal x var) Lambda(x,y) Lambda(x,subst y) \
|
subst (Variable "map") mapExp $ parse
|
||||||
\ ; Var(x) -> if (equal x var) e Var(x) \
|
"\\var. \\e. rec subst = \\x. case x of\
|
||||||
\ ; Const(c,es) -> Const(c, map subst es) \
|
\ { Apply(e1,e2) -> Apply(subst e1, subst e2) \
|
||||||
\ ; Rec(x, e') -> if (equal x var) Rec(x,e') Rec(x,subst e')\
|
\ ; Lambda(x,y) -> if (equal x var) Lambda(x,y) Lambda(x,subst y) \
|
||||||
\ ; Case(e',bs) -> Case(subst e', map (substBr subst var) bs) \
|
\ ; Var(x) -> if (equal x var) e Var(x) \
|
||||||
\ }) \
|
\ ; Const(c,es) -> Const(c, map subst es) \
|
||||||
\ \
|
\ ; Rec(x, e') -> if (equal x var) Rec(x,e') Rec(x,subst e')\
|
||||||
\ -- map \
|
\ ; Case(e',bs) -> Case(subst e', map (substBr subst var) bs) \
|
||||||
\ (\\f. rec map = \\xs. case xs of \
|
\ }"
|
||||||
\ { Nil() -> Nil() \
|
|
||||||
\ ; Cons(x,xs) -> Cons(f x, map xs)\
|
|
||||||
\ }) \
|
|
||||||
\ -- substBr \
|
|
||||||
\ (\\subst. \\var. \\b. case b of \
|
|
||||||
\ { Branch(c,vs,e') -> if (elem var vs) Branch(c,vs,e') Branch(c,vs, subst e') \
|
|
||||||
\ }) \
|
|
||||||
\ -- elem \
|
|
||||||
\ (\\x. rec elem = \\l. case l of \
|
|
||||||
\ { Nil() -> False() \
|
|
||||||
\ ; Cons(v,vs) -> if (equal x v) True() (elem vs)\
|
|
||||||
\ }) \
|
|
||||||
\ -- equal \
|
|
||||||
\ (rec equal = \\m. \\n. case m of \
|
|
||||||
\ { Zero() -> case n of { Zero() -> True(); Suc(n) -> False() } \
|
|
||||||
\ ; Suc(m) -> case n of { Zero() -> False(); Suc(n) -> equal m n }\
|
|
||||||
\ }) \
|
|
||||||
\ -- if \
|
|
||||||
\ (\\b. \\t. \\f. case b of \
|
|
||||||
\ { True() -> t \
|
|
||||||
\ ; False() -> f \
|
|
||||||
\ }) \
|
|
||||||
\"
|
|
||||||
|
|
||||||
-- Task 4
|
-- Task 4
|
||||||
|
|
||||||
|
|||||||
Reference in New Issue
Block a user