{-# Language LambdaCase, Strict #-}

module Interpreter.Self where

import Chi
import Interpreter.Haskell

-- Task 3

mapExp :: Exp
mapExp = parse
  "\\f. rec map = \\xs. case xs of \
  \ { Nil() -> Nil() \
  \ ; Cons(x,xs) -> Cons(f x, map xs)\
  \ }"

equalExp :: Exp
equalExp = parse
  "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 }\
  \ }"

elemExp :: Exp
elemExp =
  subst (Variable "equal") equalExp $ parse
  "\\x. rec elem = \\l. case l of \
  \ { Nil() -> False() \
  \ ; Cons(v,vs) -> case (equal x v) of { True() -> True(); False() -> (elem vs) } \
  \ }"

substBrExp :: Exp
substBrExp =
  subst (Variable "elem") elemExp $ parse
  "\\subst. \\var. \\b. case b of \
  \ { Branch(c,vs,e') -> case (elem var vs) of \
  \   { True() -> Branch(c,vs,e') \
  \   ; False() -> Branch(c,vs, subst e') \
  \   } \
  \ }"

substExp :: Exp
substExp =
  subst (Variable "equal") equalExp .
  subst (Variable "substBr") substBrExp .
  subst (Variable "map") mapExp $ parse
        "\\var. \\e. rec subst = \\x. case x of\
        \ { Apply(e1,e2) -> Apply(subst e1, subst e2) \
        \ ; Lambda(x,y) -> case (equal x var) of \
        \     { True() -> Lambda(x,y) \
        \     ; False() -> Lambda(x,subst y) \
        \     } \
        \ ; Var(x) -> case (equal x var) of {True() -> e; False() -> Var(x)} \
        \ ; Const(c,es) -> Const(c, map subst es) \
        \ ; Rec(x, e') -> case (equal x var) of {True() -> Rec(x,e'); False() -> Rec(x,subst e')}\
        \ ; Case(e',bs) -> Case(subst e', map (substBr subst var) bs) \
        \ }"

-- Task 4

lookupExp :: Exp
lookupExp =
  subst (Variable "equal") equalExp $ parse
  "\\c. rec lookup = \\xs. case xs of \
  \ { Cons(b,bs) -> \
  \     case b of \
  \       { Branch(c', xs, e') -> case (equal c c') of \
  \         { True() -> Pair(xs,e') \
  \         ; False() -> lookup bs \
  \         } \
  \       } \
  \ }"

substsExp :: Exp
substsExp =
  subst (Variable "subst") substExp $ parse
  "rec substs = \\xs. \\vs. \\e'. case xs of \
  \ { Nil() -> case vs of { Nil() -> e' } \
  \ ; Cons(x,xs) -> case vs of { Cons(v,vs) -> subst x v (substs xs vs e') }\
  \ }"

evalExp :: Exp
evalExp =
  subst (Variable "map") mapExp .
  subst (Variable "lookup") lookupExp .
  subst (Variable "substs") substsExp .
  subst (Variable "subst") substExp $ parse
  "rec eval = \\e. case e of \
  \ { Lambda(x,e) -> Lambda(x,e) \
  \ ; Apply(e1,e2) -> case eval e1 of \
  \    { Lambda(x,e) -> eval (subst x (eval e2) e) } \
  \ ; Rec(x,e) -> eval (subst x Rec(x,e) e) \
  \ ; Const(c,es) -> Const(c, map eval es) \
  \ ; Case(e,bs) -> case eval e of \
  \     { Const(c,vs) -> case lookup c bs of \
  \        { Pair(xs,e') -> eval (substs xs vs e') } \
  \     } \
  \ ; Var(x) -> Var(x) \
  \ }"