nandi.uk
This repository has no description
1import Mlang.Interpreter
2
3namespace Mlang
4
5inductive Token where
6 | int : Int → Token
7 | decimal : Decimal → Token
8 | bool : Bool → Token
9 | string : String → Token
10 | ident : String → Token
11 | lparen : Token
12 | rparen : Token
13 | lbracket : Token
14 | rbracket : Token
15 | lbrace : Token
16 | rbrace : Token
17 | semicolon : Token
18 | comma : Token
19 | colon : Token
20 | plus : Token
21 | minus : Token
22 | star : Token
23 | slash : Token
24 | eq : Token
25 | thinArrow : Token
26 | fatArrow : Token
27 | kwLet : Token
28 | kwIn : Token
29 | kwIf : Token
30 | kwThen : Token
31 | kwElse : Token
32 | kwFun : Token
33 | kwTry : Token
34 | kwWith : Token
35 | kwPmap : Token
36 | kwNull : Token
37 deriving Repr, BEq, Inhabited
38
39inductive ParseError where
40 | lexError : String → ParseError
41 | unexpectedEof : String → ParseError
42 | unexpectedToken : String → ParseError
43 | trailingTokens : List Token → ParseError
44 deriving Repr, Inhabited
45
46abbrev ParseM := Except ParseError
47
48def isDigit (c : Char) : Bool :=
49 '0' <= c && c <= '9'
50
51def isIdentStart (c : Char) : Bool :=
52 c.isAlpha || c = '_'
53
54def isIdentContinue (c : Char) : Bool :=
55 isIdentStart c || isDigit c
56
57def isAtomStart : Token → Bool
58 | .int _ | .decimal _ | .bool _ | .string _ | .ident _ | .lparen | .lbracket | .lbrace | .kwNull => true
59 | _ => false
60
61partial def spanChars (p : Char → Bool) : List Char → List Char × List Char
62 | [] => ([], [])
63 | c :: cs =>
64 if p c then
65 let (taken, rest) := spanChars p cs
66 (c :: taken, rest)
67 else
68 ([], c :: cs)
69
70def charsToString (chars : List Char) : String :=
71 String.ofList chars
72
73def lexIdent (chars : List Char) : Token × List Char :=
74 let (nameChars, rest) := spanChars isIdentContinue chars
75 let name := charsToString nameChars
76 let token :=
77 match name with
78 | "let" => .kwLet
79 | "in" => .kwIn
80 | "if" => .kwIf
81 | "then" => .kwThen
82 | "else" => .kwElse
83 | "fun" => .kwFun
84 | "try" => .kwTry
85 | "with" => .kwWith
86 | "pmap" => .kwPmap
87 | "null" => .kwNull
88 | "true" => .bool true
89 | "false" => .bool false
90 | _ => .ident name
91 (token, rest)
92
93def lexNumber (chars : List Char) : ParseM (Token × List Char) := do
94 let (digits, rest) := spanChars isDigit chars
95 match rest with
96 | '.' :: fracRest =>
97 let (fracDigits, tail) := spanChars isDigit fracRest
98 if fracDigits.isEmpty then
99 throw (.lexError "invalid decimal literal")
100 else
101 pure (.decimal (parseDecimal (charsToString digits ++ "." ++ charsToString fracDigits)), tail)
102 | _ =>
103 match String.toInt? (charsToString digits) with
104 | some n => pure (.int n, rest)
105 | none => throw (.lexError "invalid integer literal")
106
107partial def takeStringChars : List Char → ParseM (List Char × List Char)
108 | [] => throw (.lexError "unterminated string literal")
109 | '"' :: rest => pure ([], rest)
110 | '\\' :: '"' :: rest => do
111 let (chars, tail) ← takeStringChars rest
112 pure ('"' :: chars, tail)
113 | '\\' :: 'n' :: rest => do
114 let (chars, tail) ← takeStringChars rest
115 pure ('\n' :: chars, tail)
116 | c :: rest => do
117 let (chars, tail) ← takeStringChars rest
118 pure (c :: chars, tail)
119
120def lexString (chars : List Char) : ParseM (Token × List Char) := do
121 let (content, rest) ← takeStringChars chars
122 pure (.string (charsToString content), rest)
123
124partial def lexChars : List Char → ParseM (List Token)
125 | [] => pure []
126 | c :: cs =>
127 if c.isWhitespace then
128 lexChars cs
129 else if isDigit c then do
130 let (tok, rest) ← lexNumber (c :: cs)
131 let toks ← lexChars rest
132 pure (tok :: toks)
133 else if isIdentStart c then do
134 let (tok, rest) := lexIdent (c :: cs)
135 let toks ← lexChars rest
136 pure (tok :: toks)
137 else
138 match c, cs with
139 | '"', _ => do
140 let (tok, rest) ← lexString cs
141 let toks ← lexChars rest
142 pure (tok :: toks)
143 | '(', _ => do pure (.lparen :: (← lexChars cs))
144 | ')', _ => do pure (.rparen :: (← lexChars cs))
145 | '[', _ => do pure (.lbracket :: (← lexChars cs))
146 | ']', _ => do pure (.rbracket :: (← lexChars cs))
147 | '{', _ => do pure (.lbrace :: (← lexChars cs))
148 | '}', _ => do pure (.rbrace :: (← lexChars cs))
149 | ';', _ => do pure (.semicolon :: (← lexChars cs))
150 | ',', _ => do pure (.comma :: (← lexChars cs))
151 | ':', _ => do pure (.colon :: (← lexChars cs))
152 | '+', _ => do pure (.plus :: (← lexChars cs))
153 | '-', '>' :: rest => do pure (.thinArrow :: (← lexChars rest))
154 | '-', _ => do pure (.minus :: (← lexChars cs))
155 | '*', _ => do pure (.star :: (← lexChars cs))
156 | '/', _ => do pure (.slash :: (← lexChars cs))
157 | '=', '>' :: rest => do pure (.fatArrow :: (← lexChars rest))
158 | '=', _ => do pure (.eq :: (← lexChars cs))
159 | _, _ => throw (.lexError s!"unexpected character '{c}'")
160
161def lex (input : String) : ParseM (List Token) :=
162 lexChars input.toList
163
164abbrev ParserState := List Token
165
166inductive ReplCommand where
167 | bind : Name → Expr → ReplCommand
168 | evalProgram : List Expr → ReplCommand
169 deriving Repr, Inhabited
170
171def expectToken (expected : Token) : ParserState → ParseM ParserState
172 | tok :: rest =>
173 if tok == expected then
174 pure rest
175 else
176 throw (.unexpectedToken s!"expected {reprStr expected}, got {reprStr tok}")
177 | [] => throw (.unexpectedEof s!"expected {reprStr expected}")
178
179def threadStep (current : Expr) (stepName : Name) : Expr :=
180 .app (.var stepName) current
181
182def threadTemplateStep (current : Expr) (step : Expr) : Expr :=
183 match step with
184 | .app fn arg => .app (.app fn current) arg
185 | .var _ => .app step current
186 | _ => .app step current
187
188mutual
189 partial def parseTy (tokens : ParserState) : ParseM (Ty × ParserState) := do
190 let (lhs, rest) ← parseTyAtom tokens
191 match rest with
192 | .thinArrow :: rest =>
193 let (rhs, rest) ← parseTy rest
194 pure (.funTy lhs [] rhs, rest)
195 | _ => pure (lhs, rest)
196
197 partial def parseTyAtom : ParserState → ParseM (Ty × ParserState)
198 | .ident "Number" :: rest => pure (.number, rest)
199 | .ident "Int" :: rest => pure (.int, rest)
200 | .ident "Decimal" :: rest => pure (.decimal, rest)
201 | .ident "Rational" :: rest => pure (.number, rest)
202 | .ident "Stability" :: rest => pure (.stability, rest)
203 | .ident "Bool" :: rest => pure (.bool, rest)
204 | .ident "LazyReal" :: rest => pure (.number, rest)
205 | .ident "String" :: rest => pure (.string, rest)
206 | .ident "Data" :: rest => pure (.data, rest)
207 | .ident "List" :: rest => pure (.list, rest)
208 | .ident "Result" :: rest => pure (.result, rest)
209 | .ident "Error" :: rest => pure (.error, rest)
210 | .lparen :: rest => do
211 let (ty, rest) ← parseTy rest
212 let rest ← expectToken .rparen rest
213 pure (ty, rest)
214 | tok :: _ => throw (.unexpectedToken s!"expected type, got {reprStr tok}")
215 | [] => throw (.unexpectedEof "expected type")
216end
217
218mutual
219 partial def parseExpr (tokens : ParserState) : ParseM (Expr × ParserState) := do
220 match tokens with
221 | .thinArrow :: rest => do
222 let (start, rest) ← parseThreadSeed rest
223 parseThreadTail start rest
224 | .kwLet :: .ident name :: .eq :: rest => do
225 let (value, rest) ← parseExpr rest
226 let rest ← expectToken .kwIn rest
227 let (body, rest) ← parseExpr rest
228 pure (.letE name value body, rest)
229 | .kwIf :: rest => do
230 let (cond, rest) ← parseExpr rest
231 let rest ← expectToken .kwThen rest
232 let (thenBranch, rest) ← parseExpr rest
233 let rest ← expectToken .kwElse rest
234 let (elseBranch, rest) ← parseExpr rest
235 pure (.ifE cond thenBranch elseBranch, rest)
236 | .kwTry :: rest => do
237 let (body, rest) ← parseExpr rest
238 let rest ← expectToken .kwWith rest
239 match rest with
240 | .ident errName :: .fatArrow :: rest => do
241 let (handler, rest) ← parseExpr rest
242 pure (.tryE body errName handler, rest)
243 | tok :: _ =>
244 throw (.unexpectedToken s!"expected handler binder, got {reprStr tok}")
245 | [] =>
246 throw (.unexpectedEof "expected handler binder")
247 | .kwPmap :: .ident itemName :: .kwIn :: rest => do
248 let (collection, rest) ← parseExpr rest
249 let rest ← expectToken .fatArrow rest
250 let (body, rest) ← parseExpr rest
251 pure (.parMapE itemName collection body, rest)
252 | .kwFun :: .lparen :: .ident name :: .colon :: rest => do
253 let (paramTy, rest) ← parseTy rest
254 let rest ← expectToken .rparen rest
255 let rest ← expectToken .fatArrow rest
256 let (body, rest) ← parseExpr rest
257 pure (.lam name paramTy body, rest)
258 | _ =>
259 parseEq tokens
260
261 partial def parseThreadTail (current : Expr) (tokens : ParserState) : ParseM (Expr × ParserState) := do
262 match tokens with
263 | .ident stepName :: rest =>
264 parseThreadTail (threadStep current stepName) rest
265 | .lparen :: _ => do
266 let (step, rest) ← parseAtom tokens
267 parseThreadTail (threadTemplateStep current step) rest
268 | _ =>
269 pure (current, tokens)
270
271 partial def parseThreadSeed (tokens : ParserState) : ParseM (Expr × ParserState) := do
272 parseAtom tokens
273
274 partial def parseEq (tokens : ParserState) : ParseM (Expr × ParserState) := do
275 let (lhs, rest) ← parseAddSub tokens
276 match rest with
277 | .eq :: rest =>
278 let (rhs, rest) ← parseEq rest
279 pure (Expr.eq lhs rhs, rest)
280 | _ => pure (lhs, rest)
281
282 partial def parseAddSub (tokens : ParserState) : ParseM (Expr × ParserState) := do
283 let (first, rest) ← parseMul tokens
284 parseAddSubTail first rest
285
286 partial def parseAddSubTail (lhs : Expr) (tokens : ParserState) : ParseM (Expr × ParserState) := do
287 match tokens with
288 | .plus :: rest => do
289 let (rhs, rest) ← parseMul rest
290 parseAddSubTail (.add lhs rhs) rest
291 | .minus :: rest => do
292 let (rhs, rest) ← parseMul rest
293 parseAddSubTail (.sub lhs rhs) rest
294 | _ => pure (lhs, tokens)
295
296 partial def parseMul (tokens : ParserState) : ParseM (Expr × ParserState) := do
297 let (first, rest) ← parseApp tokens
298 parseMulTail first rest
299
300 partial def parseMulTail (lhs : Expr) (tokens : ParserState) : ParseM (Expr × ParserState) := do
301 match tokens with
302 | .star :: rest => do
303 let (rhs, rest) ← parseApp rest
304 parseMulTail (.mul lhs rhs) rest
305 | .slash :: rest => do
306 let (rhs, rest) ← parseApp rest
307 parseMulTail (.div lhs rhs) rest
308 | _ => pure (lhs, tokens)
309
310 partial def parseApp (tokens : ParserState) : ParseM (Expr × ParserState) := do
311 let (fn, rest) ← parseAtom tokens
312 parseAppTail fn rest
313
314 partial def parseAppTail (fn : Expr) (tokens : ParserState) : ParseM (Expr × ParserState) := do
315 match tokens with
316 | tok :: _ =>
317 if isAtomStart tok then do
318 let (arg, rest) ← parseAtom tokens
319 parseAppTail (.app fn arg) rest
320 else
321 pure (fn, tokens)
322 | [] => pure (fn, [])
323
324 partial def parseArrayItems (items : List Expr) : ParserState → ParseM (Expr × ParserState)
325 | .rbracket :: rest => pure (.arrayE items.reverse, rest)
326 | .comma :: rest => do
327 let (item, rest) ← parseExpr rest
328 parseArrayItems (item :: items) rest
329 | tok :: _ => throw (.unexpectedToken s!"expected ',' or ']', got {reprStr tok}")
330 | [] => throw (.unexpectedEof "unterminated array")
331
332 partial def parseArray : ParserState → ParseM (Expr × ParserState)
333 | .rbracket :: rest => pure (.arrayE [], rest)
334 | tokens => do
335 let (first, rest) ← parseExpr tokens
336 parseArrayItems [first] rest
337
338 partial def parseFieldKey : ParserState → ParseM (String × ParserState)
339 | .ident name :: rest => pure (name, rest)
340 | .string name :: rest => pure (name, rest)
341 | tok :: _ => throw (.unexpectedToken s!"expected field key, got {reprStr tok}")
342 | [] => throw (.unexpectedEof "expected field key")
343
344 partial def parseRecordFields (fields : List (String × Expr)) : ParserState → ParseM (Expr × ParserState)
345 | .rbrace :: rest => pure (.recordE fields.reverse, rest)
346 | .comma :: rest => do
347 let (name, rest) ← parseFieldKey rest
348 let rest ← expectToken .eq rest
349 let (value, rest) ← parseExpr rest
350 parseRecordFields ((name, value) :: fields) rest
351 | tok :: _ => throw (.unexpectedToken s!"expected ',' or '}}', got {reprStr tok}")
352 | [] => throw (.unexpectedEof "unterminated record")
353
354 partial def parseRecord : ParserState → ParseM (Expr × ParserState)
355 | .rbrace :: rest => pure (.recordE [], rest)
356 | tokens => do
357 let (name, rest) ← parseFieldKey tokens
358 let rest ← expectToken .eq rest
359 let (value, rest) ← parseExpr rest
360 parseRecordFields [(name, value)] rest
361
362 partial def parseAtom : ParserState → ParseM (Expr × ParserState)
363 | .int n :: rest => pure (.int n, rest)
364 | .decimal d :: rest => pure (.decimal d, rest)
365 | .bool b :: rest => pure (.bool b, rest)
366 | .string s :: rest => pure (.string s, rest)
367 | .kwNull :: rest => pure (.null, rest)
368 | .ident name :: rest => pure (.var name, rest)
369 | .lbracket :: rest => parseArray rest
370 | .lbrace :: rest => parseRecord rest
371 | .lparen :: rest => do
372 let (expr, rest) ← parseExpr rest
373 let rest ← expectToken .rparen rest
374 pure (expr, rest)
375 | tok :: _ => throw (.unexpectedToken s!"expected expression, got {reprStr tok}")
376 | [] => throw (.unexpectedEof "expected expression")
377end
378
379partial def parseProgramTokens : ParserState → ParseM (List Expr)
380 | [] => pure []
381 | .semicolon :: rest => parseProgramTokens rest
382 | tokens => do
383 let (expr, rest) ← parseExpr tokens
384 match rest with
385 | [] => pure [expr]
386 | .semicolon :: more =>
387 let tail ← parseProgramTokens more
388 pure (expr :: tail)
389 | _ => throw (.trailingTokens rest)
390
391def parseProgram (input : String) : ParseM (List Expr) := do
392 let tokens ← lex input
393 parseProgramTokens tokens
394
395def parseReplCommand (input : String) : ParseM ReplCommand := do
396 let tokens ← lex input
397 match tokens with
398 | .kwLet :: .ident name :: .eq :: rest =>
399 match parseExpr rest with
400 | .ok (value, []) => pure (.bind name value)
401 | _ =>
402 let program ← parseProgramTokens tokens
403 pure (.evalProgram program)
404 | _ =>
405 let program ← parseProgramTokens tokens
406 pure (.evalProgram program)
407
408def parse (input : String) : ParseM Expr := do
409 let program ← parseProgram input
410 match program with
411 | [expr] => pure expr
412 | [] => throw (ParseError.unexpectedEof "expected expression")
413 | _ => throw (ParseError.unexpectedToken "expected a single expression")
414
415end Mlang