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
|
module CC.Term.Parse
import CC.Name
import CC.Term
import CC.Term.Raw
import Data.List
import Text.Lexer
import Text.Parser
-- Tokens ----------------------------------------------------------------------
data CCTokenKind
= TIgnore
| TIdent
-- Keywords
| TLet
-- Symbols
| TLambda
| TPOpen
| TPClose
| TComma
| TFatArrow
| TDef
| TSemi
%name CCTokenKind k
Eq CCTokenKind where
TIgnore == TIgnore = True
TIdent == TIdent = True
TLet == TLet = True
TLambda == TLambda = True
TPOpen == TPOpen = True
TPClose == TPClose = True
TComma == TComma = True
TFatArrow == TFatArrow = True
TDef == TDef = True
TSemi == TSemi = True
_ == _ = False
TokenKind CCTokenKind where
TokType TIdent = String
TokType _ = ()
tokValue TIgnore s = ()
tokValue TIdent s = s
tokValue TLet s = ()
tokValue TLambda s = ()
tokValue TPOpen s = ()
tokValue TPClose s = ()
tokValue TComma s = ()
tokValue TFatArrow s = ()
tokValue TDef s = ()
tokValue TSemi s = ()
export
CCToken : Type
CCToken = Token CCTokenKind
-- Lexer -----------------------------------------------------------------------
ignored : List Lexer
ignored = [spaces, lineComment (exact "--"), blockComment (exact "{-") (exact "-}")]
identifier : Lexer
identifier = alpha <+> many alphaNum
keywords : List (String, CCTokenKind)
keywords = [("let", TLet)]
tokenMap : TokenMap CCToken
tokenMap =
toTokenMap (map (, TIgnore) ignored) ++
[(identifier, \s =>
case lookup s keywords of
Just kind => Tok kind s
Nothing => Tok TIdent s)
] ++ toTokenMap [
(exact "\\", TLambda),
(exact "\x03BB", TLambda),
(exact "(", TPOpen),
(exact ")", TPClose),
(exact ",", TComma),
(exact "=>", TFatArrow),
(exact "=", TDef),
(exact ";", TSemi)
]
-- Parser ----------------------------------------------------------------------
%tcinline
parens : {b : Bool} -> Grammar state CCToken b ty -> Grammar state CCToken True ty
parens p = match TPOpen >> commit >> p >>= (\t => match TPClose *> commit *> pure t)
parseTerm : Grammar state CCToken True RawTerm
parseLambda : Grammar state CCToken True RawTerm
parseLet : Grammar state CCToken True RawTerm
parseSpine : Grammar state CCToken True RawTerm
parseAtom : Grammar state CCToken True RawTerm
parseTerm = parseLambda <|> parseLet <|> parseSpine
parseLambda = do
match TLambda
commit
names <- sepBy1 (match TComma >> commit) (MkName <$> (bounds $ match TIdent))
commit
match TFatArrow
commit
t <- parseTerm
pure $ foldr1By RAbs (flip RAbs t) names
parseLet = do
match TLet
commit
n <- bounds $ match TIdent
commit
match TDef
commit
t <- parseTerm
match TSemi
commit
u <- parseTerm
pure $ RLet (MkName n) t u
parseSpine = foldl1 RApp <$> some parseAtom
parseAtom =
(RVar <$> MkName <$> (bounds $ match TIdent <* commit)) <|>
(parens parseTerm)
parseSrc : Grammar state CCToken True RawTerm
parseSrc = parseTerm <* eof
export
parseString : String -> Either (List1 (ParsingError CCToken)) RawTerm
parseString str = do
let (tokens, _, _, "") = lex tokenMap str
| (_, line, col, rest) =>
let bounds = MkBounds { startCol = col, startLine = line, endCol = col, endLine = line } in
Left (Error "failed to lex input" (Just bounds) ::: [])
(val, []) <- parse parseSrc $ filter (\tok => tok.val.kind /= TIgnore) tokens
| (_, fst :: rest) => Left (Error "unexpected token" (Just fst.bounds) ::: [])
pure val
|
