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
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
|
module Obs.Parser
import Data.String
import Obs.Sort
import Obs.Syntax
import System
import System.File
import Text.Lexer
import Text.Parser
%default total
Error : Type -> Type -> Type
Error tok = Either (List1 (ParsingError tok))
report : List1 (ParsingError tok) -> Error tok a
report = Left
data ObsTokenKind
= OTNewline
| OTIgnore
| OTIdent
-- Keywords
| OTProp
| OTSet
| OTNat
-- Special symbols
| OTUnit
| OTPoint
-- Grouping symbols
| OTPOpen
| OTPClose
-- Definition characters
| OTEqual
| OTColon
Eq ObsTokenKind where
OTNewline == OTNewline = True
OTIgnore == OTIgnore = True
OTIdent == OTIdent = True
OTProp == OTProp = True
OTSet == OTSet = True
OTNat == OTNat = True
OTUnit == OTUnit = True
OTPoint == OTPoint = True
OTPOpen == OTPOpen = True
OTPClose == OTPClose = True
OTEqual == OTEqual = True
OTColon == OTColon = True
_ == _ = False
TokenKind ObsTokenKind where
TokType OTIdent = String
TokType OTNat = Nat
TokType _ = ()
tokValue OTNewline s = ()
tokValue OTIgnore s = ()
tokValue OTIdent s = s
tokValue OTProp s = ()
tokValue OTSet s = ()
tokValue OTNat s = stringToNatOrZ s
tokValue OTUnit s = ()
tokValue OTPoint s = ()
tokValue OTPOpen s = ()
tokValue OTPClose s = ()
tokValue OTEqual s = ()
tokValue OTColon s = ()
ObsToken : Type
ObsToken = Token ObsTokenKind
ignored : WithBounds ObsToken -> Bool
ignored (MkBounded (Tok OTIgnore _) _ _) = True
ignored _ = False
identifier : Lexer
identifier = alpha <+> many alphaNum
keywords : List (String, ObsTokenKind)
keywords =
[ ("Set", OTSet)
, ("Prop", OTProp)
]
obsTokenMap : TokenMap ObsToken
obsTokenMap = toTokenMap [(newline, OTNewline), (spaces, OTIgnore)] ++
[ (identifier, \s =>
case lookup s keywords of
(Just kind) => Tok kind s
Nothing => Tok OTIdent s)
] ++ toTokenMap
[ (digits, OTNat)
, (exact "_", OTPoint)
, (exact "(", OTPOpen)
, (exact ")", OTPClose)
, (exact "=", OTEqual)
, (exact ":", OTColon)
]
parens : {c : _} -> Grammar state ObsToken c a -> Grammar state ObsToken True a
parens g =
match OTPOpen *>
many (match OTNewline) *>
g <*
many (match OTNewline) <*
match OTPClose
ident : Grammar state ObsToken True (WithBounds String)
ident = bounds $ match OTIdent
var : Grammar state ObsToken True Syntax
var = do
id <- ident
pure (Var id.bounds id.val)
prop : Grammar state ObsToken True (WithBounds Sort)
prop = do
p <- bounds $ match OTProp
pure (map (\_ => Prop) p)
set : Grammar state ObsToken True (WithBounds Sort)
set = do
s <- bounds $ match OTSet
i <- bounds $ option 0 (match OTNat)
pure (map Set $ mergeBounds s i)
sort : Grammar state ObsToken True Syntax
sort = do
sort <- prop <|> set
pure (Sort sort.bounds sort.val)
top : Grammar state ObsToken True Syntax
top = map (\v => Top v.bounds) $ bounds $ match OTUnit
point : Grammar state ObsToken True Syntax
point = map (\v => Point v.bounds) $ bounds $ match OTPoint
partial
exp : Grammar state ObsToken True Syntax
partial
term : Grammar state ObsToken True Syntax
exp = term
term = var <|> sort <|> top <|> point <|> parens exp
partial
decl : Grammar state ObsToken True (WithBounds String, Syntax)
decl = [| MkPair ident (match OTColon *> exp) |]
partial
def : Grammar state ObsToken True (WithBounds String, Syntax)
def = [| MkPair ident (match OTEqual *> exp) |]
partial
fullDef : Grammar state ObsToken True Definition
fullDef =
seq
[| MkPair decl (match OTNewline *> def) |]
(\((name, ty), (name', tm)) =>
if name.val == name'.val
then pure (MkDefinition {bounds = name.bounds, name = name.val, ty, tm})
else fatalLoc name.bounds "name mismatch for declaration and definition")
partial
file : Grammar state ObsToken False (List Definition)
file = many (match OTNewline) *> sepEndBy (some (match OTNewline)) fullDef
postprocess : List (WithBounds ObsToken) -> List (WithBounds ObsToken)
postprocess [] = []
postprocess [tok] = if ignored tok then [] else [tok]
postprocess (tok :: tail@(tok' :: toks)) = case (tok.val.kind, tok'.val.kind) of
(OTPOpen, OTPClose) => map (\_ => Tok OTUnit "()") (mergeBounds tok tok') :: postprocess toks
_ => if ignored tok then postprocess tail else tok :: postprocess tail
partial
export
parse : String -> Error ObsToken (List Definition)
parse str = do
let (toks, _, _, "") = lex obsTokenMap str
| (_, l, c, rem) => report (Error "failed to lex input" (Just $ MkBounds { startLine = l, startCol = c, endLine = l, endCol = c }) ::: [])
(defs, []) <- parse file $ postprocess toks
| (_, (t :: _)) => report (Error "unparsed tokens" (Just t.bounds) ::: [])
pure defs
printErr : ParsingError tok -> IO ()
printErr (Error str Nothing) = putStrLn "error: \{str}"
printErr (Error str (Just b)) = putStrLn
"error: \{show b.startLine}:\{show b.startCol}-\{show b.endLine}:\{show b.endCol}: \{str}"
reportErrs : List (ParsingError tok) -> IO a
reportErrs [] = exitFailure
reportErrs (e :: errs) = do
() <- printErr e
reportErrs errs
partial
export
parseFile : (fname : String) -> IO (List Definition)
parseFile fname = do
Right str <- readFile fname
| Left err => do
() <- putStrLn "error: \{show err}"
exitFailure
let Right defs = parse str
| Left err => reportErrs (forget err)
pure defs
|
