BFStrType.agda

module _ where

open import Core.Nat
open import Core.Int
open import Core.List
open import Core.String
open import Core.Maybe
open import Core.Operators
open import Core.Pair
open import Core.Unit
open import Core.Equality

record Tape : Set where
  field
    value : Nat
    left : List Nat
    right : List Nat

moveRight : Tape -> Tape
moveRight tape = record
  { value = headOr 0 (Tape.left tape);
    left = tail (Tape.left tape);
    right = Tape.value tape :: Tape.right tape }

moveLeft : Tape -> Tape
moveLeft tape = record
  { value = headOr 0 (Tape.right tape);
    left = Tape.value tape :: Tape.left tape;
    right = tail (Tape.right tape) }

emptyTape : Tape
emptyTape = record
  { value = 0;
    left = [];
    right = [] }

increment : Tape -> Tape
increment tape = record tape { value = 1+ (Tape.value tape) }

decrement : Tape -> Tape
decrement tape with Tape.value tape
... | zero = tape
... | suc n = record tape { value = n }

data Inst : Set where
  :fin : Inst
  :+_ :-_ :<_ :>_ :i_ :o_ : Inst -> Inst
  :[_]_ : Inst -> Inst -> Inst

parse' : (Inst -> Inst) -> List (Inst -> Inst) -> List Char -> Inst
parse' prev stack [] = prev :fin
parse' prev stack ('+' :: next) = parse' (\x -> prev (:+ x)) stack next
parse' prev stack ('-' :: next) = parse' (\x -> prev (:- x)) stack next
parse' prev stack ('<' :: next) = parse' (\x -> prev (:< x)) stack next
parse' prev stack ('>' :: next) = parse' (\x -> prev (:> x)) stack next
parse' prev stack (',' :: next) = parse' (\x -> prev (:i x)) stack next
parse' prev stack ('.' :: next) = parse' (\x -> prev (:o x)) stack next
parse' prev [] (']' :: next) = parse' prev [] next -- Just skip orphaned ]
parse' prev (h :: t) (']' :: next) = parse' (\x -> h (:[ (prev :fin) ] x)) t next
parse' prev stack ('[' :: next) = parse' (\x -> x) (prev :: stack) next
parse' prev stack (_ :: next) = parse' prev stack next

parse : String -> Inst
parse code = parse' (\x -> x) [] [ code ]

record State : Set where
  field
    inst : Inst
    tape : Tape
    stack : List Inst
    input : List Nat
    output : List Nat

stateValue : State -> Nat
stateValue state = Tape.value (State.tape state)

step : State -> Maybe State
step state with State.inst state
... | :fin with State.stack state
... | [] = nothing
... | (loop :: stack) = just (record state { inst = loop; stack = stack })
step state | (:+ next) = just (record state { inst = next; tape = increment (State.tape state) })
step state | (:- next) = just (record state { inst = next; tape = decrement (State.tape state) })
step state | (:< next) = just (record state { inst = next; tape = moveRight (State.tape state) })
step state | (:> next) = just (record state { inst = next; tape = moveLeft (State.tape state) })
step state | (:i next) with State.input state
... | [] = just (record state { inst = next; tape = record (State.tape state) { value = 0 } })
... | c :: cs = just (record state { inst = next; tape = record (State.tape state) { value = c }; input = cs })
step state | (:o next) = just (record state { inst = next; output = stateValue state :: State.output state })
step state | loop@(:[ body ] next) with stateValue state
... | zero = just (record state { inst = next })
... | suc _ = just (record state { inst = body; stack = loop :: State.stack state })

stepn : Nat -> State -> State
stepn 0 state = state
stepn (suc n) state with step state
... | nothing = state
... | just next = stepn n next

run' : Inst -> List Nat -> List Nat
run' inst input = reverse (State.output (stepn 100000000000 (record { inst = inst; tape = emptyTape; stack = []; input = input; output = [] })))

stringToNatList : String -> List Nat
stringToNatList s = map charToNat (stringToChars s)

natListToString : List Nat -> String
natListToString l = charsToString (map natToChar l)

runBF : String -> String -> String
runBF code input = natListToString (run' (parse code) (stringToNatList input))

StrType' : List Set -> List Char -> Set
StrType' (t :: []) [] = t
StrType' s ('n' :: n) = StrType' (Nat :: s) n
StrType' s ('s' :: n) = StrType' (String :: s) n
StrType' (b :: a :: s) ('p' :: n) = StrType' (Pair a b :: s) n
StrType' (a :: s) ('l' :: n) = StrType' (List a :: s) n
StrType' _ _ = Never

-- Turns a string into a type, for example "nsp" becomes Pair Nat String.
StrType : String -> Set
StrType code = StrType' [] (stringToChars code)

-- Run some brainfuck code that prints "nspl" and use StrType to turn that into List (Nat * String).
Foo : StrType (runBF ">++>++>+[>+[-<++++>]<<]>.+++++.---.----." "")
Foo = [ (69 , "Sixty Nine") , (420 , "Four Twenty") ]