-- Type checker and interpreter for WHILE language.

module runwhile where

open import Library
open import WellTypedSyntax using (Program)
open import TypeChecker     using (checkProgram)

import AST as A
import Parser
open import Interpreter using (runProgram)

-- Other modules, not used here.
import Value
import UntypedInterpreter

-- Parse.

parse : String → IO A.Program
parse contents = do
  case Parser.parse contents of λ where
    (bad cs) → do
      putStrLn "SYNTAX ERROR"
      putStrLn (String.fromList cs)
      exitFailure
    (ok prg) → return prg
  where
  open Parser using (Err; ok; bad)

-- Type check.

check : A.Program → IO Program
check prg = do
  case checkProgram prg of λ where
    (fail err) → do
      putStrLn "TYPE ERROR"
      putStr   (print prg)
      putStrLn "The type error is:"
      putStrLn (print err)
      exitFailure
    (ok prg') → return prg'
  where
  open ErrorMonad using (fail; ok)

-- Interpret.

run : Program → IO ⊤
run prg' = putStrLn (print (runProgram prg'))

-- Display usage information and exit.

usage : IO ⊤
usage = do
  putStrLn "Usage: runwhile <SourceFile>"
  exitFailure

-- Parse command line argument and send file content through pipeline.

runwhile : IO ⊤
runwhile = do
  file ∷ [] ← getArgs where _ → usage
  run =<< check =<< parse =<< readFiniteFile file
  return _

main = runwhile


-- -}