PiWare IO Runner

RunWithIO.agda

open import PiWare.Atom.Bool using (Atomic-B)
open import PiWare.Gates Atomic-B

module Test.RunWithIO (Gt : Gates) where
-- A = type of atoms

open import Data.Vec as Vec using (Vec)
open import Data.Nat as Nat using (ℕ; _≤?_; suc; _+_)
open import Data.Maybe as Maybe using (Maybe; just; nothing)
open import Data.String as String using (String; fromList; toList; Costring)
open import Data.Char using (Char; _≟_)
open import Data.List as List
open import Data.Bool using (Bool; if_then_else_; true; false)
open import Relation.Nullary
open import Relation.Nullary.Decidable using (True)
open import Relation.Binary.Core
open import Function
open import Data.Digit using (fromDigits; Digit)
open import Data.Fin using (Fin; zero; suc; fromℕ)
open import Category.Monad
open import Category.Monad.Indexed

split : Char → String → List String
split sep xs = reverse $ map (fromList ∘ reverse) $ split' (toList xs) []
  where split' : List Char -> List (List Char) -> List (List Char)
        split' [] ac = ac
        split' (x ∷ xs₁) ac with sep ≟ x
        split' (x ∷ xs₁) ac | yes p = split' xs₁ ([] ∷ ac)
        split' (x ∷ xs₁) [] | no ¬p = split' xs₁ [ [ x ] ]
        split' (x ∷ xs₁) (ac ∷ ac₁) | no ¬p = split' xs₁ ((x ∷ ac) ∷ ac₁)


{-
charToDigit : Char → Maybe (Digit 10)
charToDigit '0' = just zero
charToDigit '1' = just (suc zero)
charToDigit '2' = just (suc (suc zero))
charToDigit '3' = just (suc (suc (suc zero)))
charToDigit '4' = just (suc (suc (suc (suc zero))))
charToDigit '5' = just (suc (suc (suc (suc (suc zero)))))
charToDigit '6' = just (suc (suc (suc (suc (suc (suc zero))))))
charToDigit '7' = just (suc (suc (suc (suc (suc (suc (suc zero)))))))
charToDigit '8' = just (suc (suc (suc (suc (suc (suc (suc (suc zero))))))))
charToDigit '9' = just (suc (suc (suc (suc (suc (suc (suc (suc (suc zero)))))))))
charToDigit _   = nothing-}

module Read where

  open import Data.Unit
  open import Level
  open RawMonad {Level.zero} Maybe.monad

{-readNat : String → Maybe ℕ
readNat s = mapM Maybe.monad charToDigit (reverse $ toList s) >>= λ xs →
  return $ fromDigits xs-}

  readBool : String → Maybe Bool
  readBool "1" = just true
  readBool "0" = just false
  readBool _ = nothing

  readVec : {A : Set} (f : String → Maybe A) → (n : ℕ) -> String -> Maybe (Vec A n)
  readVec {A} f n s = mapM Maybe.monad f (split ',' s) >>= fromList'
    where fromList'' : ∀ {m k} → (m ≡ k) → Vec A m → Vec A k
          fromList'' refl xs = xs
          fromList' : List A → Maybe (Vec A n)
          fromList' xs with List.length xs Nat.≟ n
          fromList' xs | yes p = just (fromList'' p (Vec.fromList xs))
          fromList' xs | no ¬p = nothing

open Read

open import Level
open import PiWare.Circuit.Core Gt
open import PiWare.Simulation.Core Gt
module MMAybe = RawMonad {Level.zero} Maybe.monad

printBool : Bool → String
printBool true = "1"
printBool false = "0"

printVec : ∀ {n} {A : Set} → (A → String) → Vec A n → String
printVec f xs = foldr String._++_ "" $ intersperse "," $ List.map f $ Vec.toList xs

printMaybe : ∀ {A : Set} → (A → String) → Maybe A → String
printMaybe f (just x) = "just (" String.++ f x String.++ ")"
printMaybe f nothing = "nothing"

-- runs the circuit, returning the result
runCircuit : ∀ {i o} → ℂ' {σ} i o → String → Maybe String
runCircuit {i} {o} c inp = readVec readBool i inp MMAybe.>>= λ xs →
  just (printVec printBool (⟦ c ⟧' xs))
  where c' = ⟦ c ⟧'


-- actual test case - maybe split into a seperate file?
open import IO
open import Data.Unit
open import Coinduction
open import Relation.Nullary.Decidable
open import PiWare.Samples.BoolTrioComb
open import Data.Product
import PiWare.Circuit
open PiWare.Circuit.ℂ
open import PiWare.Gates.BoolTrio

-- we cheat by using String instead of Costring here...
import IO.Primitive

postulate
  getLine1 : IO.Primitive.IO String
{-# COMPILED getLine1 getLine #-}
{- -# COMPILED_CORE getLine1 System.IO.getLine #- -}

getLine : IO String
getLine = lift getLine1

loop : IO ⊤
loop = ♯ getLine >>= λ ln →
  ♯ (if ⌊ ln String.≟ "exit" ⌋ then
       return tt
     else let k = fadd in
       putStrLn (printMaybe id (runCircuit {{!!}} {{!!}} {!!} ln)))
  where k : PiWare.Circuit.ℂ BoolTrio (Bool × Bool) Bool {2} {1}
        k = ∧ℂ {σ}
--        g :  ℂ' {! !}
        g = base k

main = run loop