packages feed

Agda-2.3.2.2: src/prototyping/eval/Main.hs

module Main where

import Prelude hiding (catch)
import Control.Exception
import System.Environment
import System.Console.Readline

import Syntax
import Pretty
import Parse

import qualified DeBruijnCBN
import qualified DeBruijnCBN2
import qualified DeBruijnCBN3
import qualified DeBruijnCBN4
import qualified DeBruijnCBN5
import qualified DeBruijnCBN6
import qualified DeBruijnCBN7
import qualified DeBruijnLazy1
import qualified DeBruijnLazy2
import qualified DeBruijnLazy3
import qualified DeBruijnLazy4
import qualified DeBruijnLazy5
import qualified DeBruijnLazy6
import qualified DeBruijnLazy7

eval "dbCBN"   = DeBruijnCBN.eval
eval "dbCBN2"  = DeBruijnCBN2.eval
eval "dbCBN3"  = DeBruijnCBN3.eval
eval "dbCBN4"  = DeBruijnCBN4.eval
eval "dbCBN5"  = DeBruijnCBN5.eval
eval "dbCBN6"  = DeBruijnCBN6.eval
eval "dbCBN7"  = DeBruijnCBN7.eval
eval "dbLazy1" = DeBruijnLazy1.eval
eval "dbLazy2" = DeBruijnLazy2.eval
eval "dbLazy3" = DeBruijnLazy3.eval
eval "dbLazy4" = DeBruijnLazy4.eval
eval "dbLazy5" = DeBruijnLazy5.eval
eval "dbLazy6" = DeBruijnLazy6.eval
eval "dbLazy7" = DeBruijnLazy7.eval
eval s	       = error $ "no such implementation: " ++ s

evalD = DeBruijnLazy7.eval

main = do
    args <- getArgs
    case args of
	[file] -> do
	    sig <- parseFile file
	    print $ evalD sig $ Def "main"
	[file, "-n", s]	-> do
	    sig <- parseFile file
	    print $ eval s sig $ Def "main"
	["-i", file] -> do
	    sig <- parseFile file
	    loop file sig
	_   -> putStrLn "Bad args"

loop file sig = do
    ms <- readline "> "
    case ms of
	Nothing   -> return ()
	Just ":q" -> return ()
	Just ":r" -> do
	    addHistory ":r"
	    sig <- parseFile file
	    loop file sig
	Just s	  -> do
	    addHistory s
	    print $ evalD sig (parseTerm sig s)
	    loop file sig
    `catch` \err -> do
	print err
	loop file sig