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
|
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)
parseIdent : Grammar state CCToken True Name
parseIdent = MkName <$> (bounds $ match TIdent)
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) parseIdent
commit
match TFatArrow
commit
t <- parseTerm
pure $ foldr1By Abs (flip Abs t) names
parseLet = do
match TLet
commit
n <- parseIdent
commit
match TDef
commit
t <- parseTerm
match TSemi
commit
u <- parseTerm
pure $ Let n t u
parseSpine = foldl1 App <$> some parseAtom
parseAtom =
(Var <$> parseIdent <* 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
|
