~ubuntu-branches/ubuntu/wily/agda/wily-proposed

« back to all changes in this revision

Viewing changes to src/prototyping/eval/Main.hs

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2014-08-05 06:38:12 UTC
  • mfrom: (1.1.6)
  • Revision ID: package-import@ubuntu.com-20140805063812-io8e77niomivhd49
Tags: 2.4.0.2-1
* [6e140ac] Imported Upstream version 2.4.0.2
* [2049fc8] Update Build-Depends to match control
* [93dc4d4] Install the new primitives
* [e48f40f] Fix typo dev→doc

Show diffs side-by-side

added added

removed removed

Lines of Context:
1
 
 
2
 
module Main where
3
 
 
4
 
import Prelude hiding (catch)
5
 
import Control.Exception
6
 
import System.Environment
7
 
import System.Console.Readline
8
 
 
9
 
import Syntax
10
 
import Pretty
11
 
import Parse
12
 
 
13
 
import qualified DeBruijnCBN
14
 
import qualified DeBruijnCBN2
15
 
import qualified DeBruijnCBN3
16
 
import qualified DeBruijnCBN4
17
 
import qualified DeBruijnCBN5
18
 
import qualified DeBruijnCBN6
19
 
import qualified DeBruijnCBN7
20
 
import qualified DeBruijnLazy1
21
 
import qualified DeBruijnLazy2
22
 
import qualified DeBruijnLazy3
23
 
import qualified DeBruijnLazy4
24
 
import qualified DeBruijnLazy5
25
 
import qualified DeBruijnLazy6
26
 
import qualified DeBruijnLazy7
27
 
 
28
 
eval "dbCBN"   = DeBruijnCBN.eval
29
 
eval "dbCBN2"  = DeBruijnCBN2.eval
30
 
eval "dbCBN3"  = DeBruijnCBN3.eval
31
 
eval "dbCBN4"  = DeBruijnCBN4.eval
32
 
eval "dbCBN5"  = DeBruijnCBN5.eval
33
 
eval "dbCBN6"  = DeBruijnCBN6.eval
34
 
eval "dbCBN7"  = DeBruijnCBN7.eval
35
 
eval "dbLazy1" = DeBruijnLazy1.eval
36
 
eval "dbLazy2" = DeBruijnLazy2.eval
37
 
eval "dbLazy3" = DeBruijnLazy3.eval
38
 
eval "dbLazy4" = DeBruijnLazy4.eval
39
 
eval "dbLazy5" = DeBruijnLazy5.eval
40
 
eval "dbLazy6" = DeBruijnLazy6.eval
41
 
eval "dbLazy7" = DeBruijnLazy7.eval
42
 
eval s         = error $ "no such implementation: " ++ s
43
 
 
44
 
evalD = DeBruijnLazy7.eval
45
 
 
46
 
main = do
47
 
    args <- getArgs
48
 
    case args of
49
 
        [file] -> do
50
 
            sig <- parseFile file
51
 
            print $ evalD sig $ Def "main"
52
 
        [file, "-n", s] -> do
53
 
            sig <- parseFile file
54
 
            print $ eval s sig $ Def "main"
55
 
        ["-i", file] -> do
56
 
            sig <- parseFile file
57
 
            loop file sig
58
 
        _   -> putStrLn "Bad args"
59
 
 
60
 
loop file sig = do
61
 
    ms <- readline "> "
62
 
    case ms of
63
 
        Nothing   -> return ()
64
 
        Just ":q" -> return ()
65
 
        Just ":r" -> do
66
 
            addHistory ":r"
67
 
            sig <- parseFile file
68
 
            loop file sig
69
 
        Just s    -> do
70
 
            addHistory s
71
 
            print $ evalD sig (parseTerm sig s)
72
 
            loop file sig
73
 
    `catch` \err -> do
74
 
        print err
75
 
        loop file sig