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 | ident : String → Token
9 | lparen : Token
10 | rparen : Token
11 | colon : Token
12 | plus : Token
13 | minus : Token
14 | star : Token
15 | slash : Token
16 | eq : Token
17 | thinArrow : Token
18 | fatArrow : Token
19 | kwLet : Token
20 | kwIn : Token
21 | kwIf : Token
22 | kwThen : Token
23 | kwElse : Token
24 | kwFun : Token
25 | kwTry : Token
26 | kwWith : Token
27 deriving Repr, BEq, Inhabited
28
29inductive ParseError where
30 | lexError : String → ParseError
31 | unexpectedEof : String → ParseError
32 | unexpectedToken : String → ParseError
33 | trailingTokens : List Token → ParseError
34 deriving Repr, Inhabited
35
36abbrev ParseM := Except ParseError
37
38def isDigit (c : Char) : Bool :=
39 '0' <= c && c <= '9'
40
41def isIdentStart (c : Char) : Bool :=
42 c.isAlpha || c = '_'
43
44def isIdentContinue (c : Char) : Bool :=
45 isIdentStart c || isDigit c
46
47def isAtomStart : Token → Bool
48 | .int _ | .bool _ | .ident _ | .lparen => true
49 | _ => false
50
51partial def spanChars (p : Char → Bool) : List Char → List Char × List Char
52 | [] => ([], [])
53 | c :: cs =>
54 if p c then
55 let (taken, rest) := spanChars p cs
56 (c :: taken, rest)
57 else
58 ([], c :: cs)
59
60def charsToString (chars : List Char) : String :=
61 String.ofList chars
62
63def lexIdent (chars : List Char) : Token × List Char :=
64 let (nameChars, rest) := spanChars isIdentContinue chars
65 let name := charsToString nameChars
66 let token :=
67 match name with
68 | "let" => .kwLet
69 | "in" => .kwIn
70 | "if" => .kwIf
71 | "then" => .kwThen
72 | "else" => .kwElse
73 | "fun" => .kwFun
74 | "try" => .kwTry
75 | "with" => .kwWith
76 | "true" => .bool true
77 | "false" => .bool false
78 | _ => .ident name
79 (token, rest)
80
81def lexNumber (chars : List Char) : ParseM (Token × List Char) := do
82 let (digits, rest) := spanChars isDigit chars
83 match String.toInt? (charsToString digits) with
84 | some n => pure (.int n, rest)
85 | none => throw (.lexError "invalid integer literal")
86
87partial def lexChars : List Char → ParseM (List Token)
88 | [] => pure []
89 | c :: cs =>
90 if c.isWhitespace then
91 lexChars cs
92 else if isDigit c then do
93 let (tok, rest) ← lexNumber (c :: cs)
94 let toks ← lexChars rest
95 pure (tok :: toks)
96 else if isIdentStart c then do
97 let (tok, rest) := lexIdent (c :: cs)
98 let toks ← lexChars rest
99 pure (tok :: toks)
100 else
101 match c, cs with
102 | '(', _ => do pure (.lparen :: (← lexChars cs))
103 | ')', _ => do pure (.rparen :: (← lexChars cs))
104 | ':', _ => do pure (.colon :: (← lexChars cs))
105 | '+', _ => do pure (.plus :: (← lexChars cs))
106 | '-', '>' :: rest => do pure (.thinArrow :: (← lexChars rest))
107 | '-', _ => do pure (.minus :: (← lexChars cs))
108 | '*', _ => do pure (.star :: (← lexChars cs))
109 | '/', _ => do pure (.slash :: (← lexChars cs))
110 | '=', '>' :: rest => do pure (.fatArrow :: (← lexChars rest))
111 | '=', _ => do pure (.eq :: (← lexChars cs))
112 | _, _ => throw (.lexError s!"unexpected character '{c}'")
113
114def lex (input : String) : ParseM (List Token) :=
115 lexChars input.toList
116
117abbrev ParserState := List Token
118
119def expectToken (expected : Token) : ParserState → ParseM ParserState
120 | tok :: rest =>
121 if tok == expected then
122 pure rest
123 else
124 throw (.unexpectedToken s!"expected {reprStr expected}, got {reprStr tok}")
125 | [] => throw (.unexpectedEof s!"expected {reprStr expected}")
126
127mutual
128 partial def parseTy (tokens : ParserState) : ParseM (Ty × ParserState) := do
129 let (lhs, rest) ← parseTyAtom tokens
130 match rest with
131 | .thinArrow :: rest =>
132 let (rhs, rest) ← parseTy rest
133 pure (.funTy lhs [] rhs, rest)
134 | _ => pure (lhs, rest)
135
136 partial def parseTyAtom : ParserState → ParseM (Ty × ParserState)
137 | .ident "Int" :: rest => pure (.int, rest)
138 | .ident "Bool" :: rest => pure (.bool, rest)
139 | .lparen :: rest => do
140 let (ty, rest) ← parseTy rest
141 let rest ← expectToken .rparen rest
142 pure (ty, rest)
143 | tok :: _ => throw (.unexpectedToken s!"expected type, got {reprStr tok}")
144 | [] => throw (.unexpectedEof "expected type")
145end
146
147mutual
148 partial def parseExpr (tokens : ParserState) : ParseM (Expr × ParserState) := do
149 match tokens with
150 | .kwLet :: .ident name :: .eq :: rest => do
151 let (value, rest) ← parseExpr rest
152 let rest ← expectToken .kwIn rest
153 let (body, rest) ← parseExpr rest
154 pure (.letE name value body, rest)
155 | .kwIf :: rest => do
156 let (cond, rest) ← parseExpr rest
157 let rest ← expectToken .kwThen rest
158 let (thenBranch, rest) ← parseExpr rest
159 let rest ← expectToken .kwElse rest
160 let (elseBranch, rest) ← parseExpr rest
161 pure (.ifE cond thenBranch elseBranch, rest)
162 | .kwTry :: rest => do
163 let (body, rest) ← parseExpr rest
164 let rest ← expectToken .kwWith rest
165 let (handler, rest) ← parseExpr rest
166 pure (.tryE body handler, rest)
167 | .kwFun :: .lparen :: .ident name :: .colon :: rest => do
168 let (paramTy, rest) ← parseTy rest
169 let rest ← expectToken .rparen rest
170 let rest ← expectToken .fatArrow rest
171 let (body, rest) ← parseExpr rest
172 pure (.lam name paramTy body, rest)
173 | _ =>
174 parseEq tokens
175
176 partial def parseEq (tokens : ParserState) : ParseM (Expr × ParserState) := do
177 let (lhs, rest) ← parseAddSub tokens
178 match rest with
179 | .eq :: rest =>
180 let (rhs, rest) ← parseEq rest
181 pure (Expr.eq lhs rhs, rest)
182 | _ => pure (lhs, rest)
183
184 partial def parseAddSub (tokens : ParserState) : ParseM (Expr × ParserState) := do
185 let (first, rest) ← parseMul tokens
186 parseAddSubTail first rest
187
188 partial def parseAddSubTail (lhs : Expr) (tokens : ParserState) : ParseM (Expr × ParserState) := do
189 match tokens with
190 | .plus :: rest => do
191 let (rhs, rest) ← parseMul rest
192 parseAddSubTail (.add lhs rhs) rest
193 | .minus :: rest => do
194 let (rhs, rest) ← parseMul rest
195 parseAddSubTail (.sub lhs rhs) rest
196 | _ => pure (lhs, tokens)
197
198 partial def parseMul (tokens : ParserState) : ParseM (Expr × ParserState) := do
199 let (first, rest) ← parseApp tokens
200 parseMulTail first rest
201
202 partial def parseMulTail (lhs : Expr) (tokens : ParserState) : ParseM (Expr × ParserState) := do
203 match tokens with
204 | .star :: rest => do
205 let (rhs, rest) ← parseApp rest
206 parseMulTail (.mul lhs rhs) rest
207 | .slash :: rest => do
208 let (rhs, rest) ← parseApp rest
209 parseMulTail (.div lhs rhs) rest
210 | _ => pure (lhs, tokens)
211
212 partial def parseApp (tokens : ParserState) : ParseM (Expr × ParserState) := do
213 let (fn, rest) ← parseAtom tokens
214 parseAppTail fn rest
215
216 partial def parseAppTail (fn : Expr) (tokens : ParserState) : ParseM (Expr × ParserState) := do
217 match tokens with
218 | tok :: _ =>
219 if isAtomStart tok then do
220 let (arg, rest) ← parseAtom tokens
221 parseAppTail (.app fn arg) rest
222 else
223 pure (fn, tokens)
224 | [] => pure (fn, [])
225
226 partial def parseAtom : ParserState → ParseM (Expr × ParserState)
227 | .int n :: rest => pure (.int n, rest)
228 | .bool b :: rest => pure (.bool b, rest)
229 | .ident name :: rest => pure (.var name, rest)
230 | .lparen :: rest => do
231 let (expr, rest) ← parseExpr rest
232 let rest ← expectToken .rparen rest
233 pure (expr, rest)
234 | tok :: _ => throw (.unexpectedToken s!"expected expression, got {reprStr tok}")
235 | [] => throw (.unexpectedEof "expected expression")
236end
237
238def parse (input : String) : ParseM Expr := do
239 let tokens ← lex input
240 let (expr, rest) ← parseExpr tokens
241 match rest with
242 | [] => pure expr
243 | _ => throw (.trailingTokens rest)
244
245end Mlang