BF.agda

module BF where

data Token : Set where
  Plus : Token
  Minus : Token
  Less : Token
  More : Token
  Period : Token
  Comma : Token
  Open : Token
  Close : Token

module Lexer where
  open import Data.Char using (Char)
  open import Data.List using (List; gfilter)
  open import Data.Maybe using (Maybe; just; nothing)

  lex₁ : Char → Maybe Token
  lex₁ '+' = just Plus
  lex₁ '-' = just Minus
  lex₁ '<' = just Less
  lex₁ '>' = just More
  lex₁ '.' = just Period
  lex₁ ',' = just Comma
  lex₁ '[' = just Open
  lex₁ ']' = just Close
  lex₁ _ = nothing

  lex : List Char → List Token
  lex = gfilter lex₁

open import Data.List using (List)

data Instruction : Set where
  Up : Instruction
  Down : Instruction
  Left : Instruction
  Right : Instruction
  Out : Instruction
  In : Instruction
  Loop : List Instruction → Instruction

module Parser where
  -- TODO this is probably quadratic, please make better
  open import Data.List using (List; []; _∷_; _∷ʳ_)
  open import Data.Maybe using (Maybe; just; nothing; map)

  parse′ : List Token → List (List Instruction) → List Instruction → Maybe (List Instruction)
  parse′ [] [] r = just r
  parse′ [] _ _ = nothing
  parse′ (Plus ∷ p) d r = parse′ p d (r ∷ʳ Up)
  parse′ (Minus ∷ p) d r = parse′ p d (r ∷ʳ Down)
  parse′ (Less ∷ p) d r = parse′ p d (r ∷ʳ Left)
  parse′ (More ∷ p) d r = parse′ p d (r ∷ʳ Right)
  parse′ (Period ∷ p) d r = parse′ p d (r ∷ʳ Out)
  parse′ (Comma ∷ p) d r = parse′ p d (r ∷ʳ In)
  parse′ (Open ∷ p) d r = parse′ p (r ∷ d) []
  parse′ (Close ∷ p) [] r = nothing
  parse′ (Close ∷ p) (d ∷ ds) r = parse′ p ds (d ∷ʳ Loop r)

  parse : List Token → Maybe (List Instruction)
  parse p = parse′ p [] []

module Interpreter₁ where
  open import Coinduction using (♯_; ♭)
  open import Data.Stream using (Stream; _∷_; repeat)
  open import Data.Integer using (ℤ; +_; ∣_∣; suc; pred)

  record Machine : Set where
    constructor _<_>_
    field
      leftward : Stream ℤ
      tapehead : ℤ
      rightward : Stream ℤ

  initial : Machine
  initial = repeat (+ 0) < + 0 > repeat (+ 0)

  left : Machine → Machine
  left ((x ∷ xs) < tapehead > rightward) = ♭ xs < x > (tapehead ∷ ♯ rightward)

  right : Machine → Machine
  right (leftward < tapehead > (x ∷ xs)) = (tapehead ∷ ♯ leftward) < x > ♭ xs

  up : Machine → Machine
  up (leftward < tapehead > rightward) = leftward < suc tapehead > rightward

  down : Machine → Machine
  down (leftward < tapehead > rightward) = leftward < pred tapehead > rightward

  open import Data.Char using (Char; toNat)
  open import Agda.Builtin.Char using () renaming (primNatToChar to natToChar)
  open import Data.Colist using (Colist; []; _∷_; _++_)
  open import Data.Product using (_×_; _,_; proj₂; map)

  in′ : Machine × Colist Char → Machine × Colist Char
  in′ ((leftward < tapehead > rightward) , []) = leftward < + 0 > rightward , []
  in′ ((leftward < tapehead > rightward) , (x ∷ xs)) = leftward < + toNat x > rightward , ♭ xs

  out : Machine → Machine × Char
  out (leftward < tapehead > rightward) = leftward < tapehead > rightward , natToChar ∣ tapehead ∣

  open import Function using (_∘_; id; _$_)

  lift₁ : (Machine → Machine) → Machine × Colist Char → (Machine × Colist Char) × Colist Char
  lift₁ f = (_, []) ∘ map f id

  lift₃ : (Machine → Machine × Char) → Machine × Colist Char → (Machine × Colist Char) × Colist Char
  lift₃ f (x , y) with f x
  ... | (x′ , c) = (x′ , y) , c ∷ ♯ []
  
  _⊝_ : (Machine × Colist Char → (Machine × Colist Char) × Colist Char) →
        (Machine × Colist Char → (Machine × Colist Char) × Colist Char) →
        Machine × Colist Char →
        (Machine × Colist Char) × Colist Char
  (f ⊝ g) x with g x
  ... | y , o₁ with f y
  ... | z , o₂ = z , o₁ ++ o₂

  open import Data.List using (List; []; _∷_)

  {-# NON_TERMINATING #-}
  interpret′ : List Instruction → Machine × Colist Char → (Machine × Colist Char) × Colist Char
  interpret′ [] = _, []
  interpret′ (Up ∷ is) = interpret′ is ⊝ lift₁ up
  interpret′ (Down ∷ is) = interpret′ is ⊝ lift₁ down
  interpret′ (Left ∷ is) = interpret′ is ⊝ lift₁ left
  interpret′ (Right ∷ is) = interpret′ is ⊝ lift₁ right
  interpret′ (Out ∷ is) = interpret′ is ⊝ (lift₃ out)
  interpret′ (In ∷ is) = interpret′ is ∘ in′
  interpret′ (Loop x ∷ is) ((leftward < + 0 > rightward) , io) = interpret′ is (leftward < + 0 > rightward , io)
  interpret′ (Loop x ∷ is) ((leftward < tapehead > rightward) , io) = interpret′ (Loop x ∷ is) ⊝ interpret′ x $ (leftward < tapehead > rightward , io)

  interpret : List Instruction → Colist Char → Colist Char
  interpret p i = proj₂ $ interpret′ p (initial , i)

module Main where
  open import Coinduction using (♯_)
  open import Data.Maybe using (just; nothing)
  open import Data.Unit using (⊤)
  open import Data.String using (toList)
  open import Function using (_$_; _∘_; case_of_)
  open import IO using (run; _>>=_; putStrLn; getContents; putStrLn∞; readFiniteFile)
  open import IO.Primitive using (IO)
  
  open Lexer using (lex)
  open Parser using (parse)
  open Interpreter₁ using (interpret)

  main : IO ⊤
  main = run $ ♯ readFiniteFile "in.bf" >>= λ program →
               ♯ (case (parse ∘ lex ∘ toList $ program) of λ {
                       nothing → putStrLn "Parse Error";
                       (just program) → ♯ getContents >>= λ in′ → ♯ putStrLn∞ (interpret program in′)
                 })

open Main using (main)