blob: 2f05ccf2a7b4356452fdc12ef256101040509a40 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
|
module Main
import CC.Name
import CC.Term
import CC.Term.Eval
import CC.Term.Parse
import CC.Term.Pretty
import CC.Term.Raw
import Data.String
import System
import System.File.ReadWrite
import System.File.Virtual
import Text.Parser
import Text.PrettyPrint.Prettyprinter
import Text.PrettyPrint.Prettyprinter.Render.Terminal
--- Error Reporting ------------------------------------------------------------
putErrLn : HasIO io => String -> io ()
putErrLn str = do
Right () <- fPutStrLn stderr str
| Left e => pure ()
pure ()
putBoundErrLn : HasIO io => Maybe Bounds -> String -> io ()
putBoundErrLn Nothing str = putErrLn str
putBoundErrLn (Just bounds) str =
let startLine = padLeft 3 '0' $ show (1 + bounds.startLine) in
let startCol = padLeft 2 '0' $ show bounds.startCol in
let endLine = padLeft 3 '0' $ show (1 + bounds.endLine) in
let endCol = padLeft 2 '0' $ show bounds.endCol in
putErrLn "\{startLine}:\{startCol}--\{endLine}:\{endCol}: \{str}"
-- Parsing ---------------------------------------------------------------------
parse : String -> IO RawTerm
parse str =
case parseString str of
Left errs => for_ errs putErr >> exitFailure
Right v => pure v
where
putErr : ParsingError CCToken -> IO ()
putErr (Error str bounds) = putBoundErrLn bounds ("parse error: \{str}" )
partial
parseStdin : IO RawTerm
parseStdin = do
Right str <- fRead stdin
| Left err => putErrLn "failed to read input: \{show err}" >> exitFailure
parse str
-- Main Function ---------------------------------------------------------------
helpMsg : String
helpMsg = unlines [
"usage: cc-eval [--help|nf]",
" --help : display this message",
" nf : read expression from stdin, print its normal form"
]
mainWith : IO (List String) -> IO RawTerm -> IO ()
mainWith getOpt getTerm = do
[_, "nf"] <- getOpt
| [_, "--help"] => putStrLn helpMsg
| _ => putErrLn helpMsg >> exitFailure
rawTerm <- getTerm
let Right term = runNameError $ translate [<] rawTerm
| Left errs => for_ errs putErr >> exitFailure
let nf : Term [<] = normalise [<] term
putDoc (pretty nf)
where
putErr : Name -> IO ()
putErr n = putBoundErrLn (bounds n) "undefined name: \{n}"
partial
main : IO ()
main = mainWith getArgs parseStdin
main' : String -> String -> IO ()
main' mode src = mainWith (pure [mode]) (parse src)
|
