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