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
84
85
86
87
88
89
90
91
92
93
94
95
96
|
module Main
import CC.Name
import CC.Term
import CC.Term.Elaborate
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-check [--help|nf|type]",
" --help : display this message",
" nf : read & typecheck expression from stdin, print its normal form and type",
" type : read & typecheck expression from stdin, print its type"
]
mainWith : IO (List String) -> IO RawTerm -> IO ()
mainWith getOpt getTerm = do
opts <- getOpt
case opts of
[_, "--help"] => putStrLn helpMsg
[_, "nf"] => do
rawTerm <- getTerm
let Right (t, ty) = runElabError $ inferTerm rawTerm
| Left errs => for_ errs putErr >> exitFailure
let nf : Term [<] = normalise [<] t
let ty = quote ty
putDoc (group $ pretty nf <++> colon <+> line <+> pretty ty)
[_, "type"] => do
rawTerm <- getTerm
let Right (t, ty) = runElabError $ inferTerm rawTerm
| Left errs => for_ errs putErr >> exitFailure
putDoc (group $ pretty $ quote ty)
_ => putErrLn helpMsg >> exitFailure
where
putErr : Either Name (String, Maybe Bounds) -> IO ()
putErr (Left n) = putBoundErrLn (bounds n) "undefined name: \{n}"
putErr (Right (s, bounds)) = putBoundErrLn bounds s
partial
main : IO ()
main = mainWith getArgs parseStdin
main' : String -> String -> IO ()
main' mode src = mainWith (pure [mode]) (parse src)
|
