{-# OPTIONS --type-in-type --no-termination-check #-}
module Interaction where
open import Data.Unit
open import Function
open import Data.Product
open import Data.Nat
open import Data.List
open import Data.Bool
{-# IMPORT System.IO #-}
open import System.IO
open import Foreign.Haskell
open import WS-Syn
open import WS-Sem
open import IOWS
open import WS-Annot
open import WS-Exp
open import WS-Comp
open import WS-Tex
open import WS-SCIL-Consts
open import RunStrategy
open import ParsePrintLoop
open import GenericPrompt
runprf : ∀ {p}{Γ : Seq p} → ⊢ Γ → IO Unit
runprf { - } {Γ} prf = Ask ⟦ prf ⟧⊢ (anotate $ Γ F) (prFml ∘ proj₂)
runprf { + } {Γ} prf = Tell ⟦ prf ⟧⊢ (anotate $ Γ F) (prFml ∘ proj₂)
askRunPrf : IO Unit
askRunPrf = prompt (text "Proof") parsePrf cont where
cont : Prf → IO Unit
cont (Γ ⊣: prf) =
putDocLn (sep (text "Proof parsed: " ∷ prPrf (Γ ⊣: prf) ∷ []) $$
text "-------------------------------------------" ) >>
runprf prf
test1 = askShowSeq
3cell = cell 3 true
test2 = runprf 3cell
test3 = putDocLn (prf2tex 3cell)
test4 = putDocLn (prAnnFml (! 3 Fvar))
n3cell = nbe 3cell
test5 = runprf n3cell
test6 = putDocLn (prf2tex n3cell)
test7 = runprf notPrf
main = hSetBuffering stdout NoBuffering >>
test2