{-# Language LambdaCase, Strict #-}

module Interpreter.Turing where

import Chi
import Interpreter.Haskell -- from assignment 3

equalExp :: Exp
equalExp = parse
  "rec equal = \\m. \\n. case m of \
  \ { Zero()  -> case n of { Blank() -> False(); Zero() -> True();  Suc(n) -> False() } \
  \ ; Suc(m)  -> case n of { Blank() -> False(); Zero() -> False(); Suc(n) -> equal m n } \
  \ ; Blank() -> case n of { Blank() -> True();  Zero() -> False(); Suc(n) -> False() } \
  \ }"

lookupExp :: Exp
lookupExp =
  subst (Variable "equal") equalExp $ parse
  "\\s. \\head. rec lookup = \\rules. case rules of \
  \ { Nil() -> Done() \
  \ ; Cons(x,xs) -> case x of \
  \   { Rule(s1, x1, s2, x2, d) -> case equal s s1 of \
  \     { True()  -> case equal head x1 of \
  \       { True()  -> Trip(s2,x2,d)\
  \       ; False() -> lookup xs \
  \       } \
  \     ; False() -> lookup xs \
  \     } \
  \   }\
  \ } \
  \ "

joinExp :: Exp
joinExp = parse
  "rec join = \\xs. \\ys. case xs of \
  \ { Nil() -> ys \
  \ ; Cons(x,xs) -> join xs Cons(x,ys) \
  \ }"

appendExp :: Exp
appendExp = parse
  "rec append = \\xs. \\ys. case xs of \
  \ { Nil() -> ys \
  \ ; Cons(x,xs) -> Cons(x,append xs ys) \
  \ }"

reverseExp :: Exp
reverseExp =
  subst (Variable "append") appendExp $ parse
  "rec reverse = \\xs. case xs of \
  \ { Nil() -> Nil() \
  \ ; Cons(x,xs) -> append xs Cons(x,Nil())\
  \ }"

removeLastBlanksExp :: Exp
removeLastBlanksExp = parse
  "rec removeLastBlanks = \\xs. case xs of \
  \ { Nil() -> Nil() \
  \ ; Cons(x,xs) -> case x of \
  \   { Blank() -> removeLastBlanks xs \
  \   ; Zero()  -> Cons(x,xs) \
  \   ; Suc(n)  -> Cons(x,xs) \
  \   } \
  \ }\
  \ "

runExp :: Exp
runExp =
  subst (Variable "removeLastBlanks") removeLastBlanksExp .
  subst (Variable "reverse") reverseExp .
  subst (Variable "join") joinExp .
  subst (Variable "lookup") lookupExp $ parse
  "(rec run = \\rev. \\tm. \\tape. case tm of \
  \ { TM(state,deltas) -> case tape of \
  \   { Nil() -> run rev TM(state,deltas) Cons(Blank(), Nil()) \
  \   ; Cons(head,xs) -> case lookup state head deltas of \
  \     { Done() -> join rev (reverse (removeLastBlanks (reverse tape))) \
  \     ; Trip(s2, x2, d) -> case d of \
  \       { L() -> case rev of \
  \         { Nil() -> run Nil() TM(s2,deltas) Cons(x2,xs) \
  \         ; Cons(y,ys) -> run ys TM(s2,deltas) Cons(y,Cons(x2,xs)) \
  \         } \
  \       ; R() -> run Cons(x2,rev) TM(s2,deltas) xs \
  \       } \
  \     } \
  \   } \
  \ }) Nil()"