-- Type checker and interpreter for WHILE language.

module V1.runwhile where

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

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

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

-- Parse.

parse : String  IO A.Program
parse contents = 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 = 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


-- -}