nandi.uk
This repository has no description
Initial commit
author
nandi
date
(May 30, 2026, 10:48 PM -0700)
commit
1a0b9186
1a0b91868716375c17c623b90a5357f0df0203ce
+812
+13
.gitignore
+13
.gitignore
+85
Main.lean
+85
Main.lean
···
1
+
import Mlang
2
+
3
+
open Mlang
4
+
5
+
def checkAndEval (source : String) : Except String (Value × Judgment) := do
6
+
match parse source with
7
+
| .error err =>
8
+
throw s!"parse error: {reprStr err}"
9
+
| .ok expr =>
10
+
match inferType [] expr with
11
+
| .error err =>
12
+
throw s!"type error: {reprStr err}"
13
+
| .ok judgment =>
14
+
match eval [] expr with
15
+
| .ok value =>
16
+
pure (value, judgment)
17
+
| .error err =>
18
+
throw s!"runtime error: {reprStr err}"
19
+
20
+
def printResult (label : String) (source : String) : IO Unit := do
21
+
match checkAndEval source with
22
+
| .ok (value, judgment) =>
23
+
IO.println s!"{label}: {renderValue value} : {renderJudgment judgment}"
24
+
| .error msg =>
25
+
IO.println s!"{label}: {msg}"
26
+
27
+
def runFile (path : String) : IO UInt32 := do
28
+
let source ← IO.FS.readFile path
29
+
match checkAndEval source with
30
+
| .ok (value, judgment) =>
31
+
IO.println s!"{renderValue value} : {renderJudgment judgment}"
32
+
pure 0
33
+
| .error msg =>
34
+
IO.eprintln s!"{path}: {msg}"
35
+
pure 1
36
+
37
+
partial def repl : IO UInt32 := do
38
+
let stdin ← IO.getStdin
39
+
let line ← stdin.getLine
40
+
let input := (String.trimAscii line).toString
41
+
if input.isEmpty then
42
+
repl
43
+
else if input = ":quit" || input = ":q" then
44
+
pure 0
45
+
else do
46
+
match checkAndEval input with
47
+
| .ok (value, judgment) =>
48
+
IO.println s!"{renderValue value} : {renderJudgment judgment}"
49
+
| .error msg =>
50
+
IO.eprintln msg
51
+
repl
52
+
53
+
def printUsage : IO Unit := do
54
+
IO.println "usage:"
55
+
IO.println " mlang # start REPL"
56
+
IO.println " mlang <file> # run a source file"
57
+
IO.println " mlang --demo # run built-in examples"
58
+
IO.println " mlang :quit # not valid; use inside REPL"
59
+
60
+
def runDemo : IO UInt32 := do
61
+
printResult "sample" "let inc = fun (x : Int) => x + 1 in inc 41"
62
+
printResult "lexical-scope" "let x = 10 in let f = fun (y : Int) => x + y in let x = 100 in f 5"
63
+
printResult "conditional" "if 6 * 7 = 42 then 1 else 0"
64
+
printResult "effectful" "10 / 2"
65
+
printResult "handled" "try 10 / 0 with 99"
66
+
printResult "handled-nested" "1 + (try 10 / 0 with 4)"
67
+
printResult "runtime-error" "10 / 0"
68
+
printResult "type-error" "let inc = fun (x : Int) => x + 1 in inc true"
69
+
pure 0
70
+
71
+
def main (args : List String) : IO UInt32 := do
72
+
match args with
73
+
| [] =>
74
+
IO.println "mlang REPL. enter :quit to exit."
75
+
repl
76
+
| ["--demo"] =>
77
+
runDemo
78
+
| ["-h"] | ["--help"] =>
79
+
printUsage
80
+
pure 0
81
+
| [path] =>
82
+
runFile path
83
+
| _ =>
84
+
printUsage
85
+
pure 1
+263
Mlang/Interpreter.lean
+263
Mlang/Interpreter.lean
···
1
+
namespace Mlang
2
+
3
+
abbrev Name := String
4
+
5
+
inductive Effect where
6
+
| error : Effect
7
+
deriving Repr, Inhabited, BEq
8
+
9
+
abbrev Effects := List Effect
10
+
11
+
def Effects.contains (effects : Effects) (effect : Effect) : Bool :=
12
+
effects.any (· == effect)
13
+
14
+
def Effects.insert (effects : Effects) (effect : Effect) : Effects :=
15
+
if effects.contains effect then effects else effect :: effects
16
+
17
+
def Effects.union (lhs rhs : Effects) : Effects :=
18
+
rhs.foldl Effects.insert lhs
19
+
20
+
def Effects.erase (effects : Effects) (target : Effect) : Effects :=
21
+
effects.filter (· != target)
22
+
23
+
def Effects.render : Effects → String
24
+
| [] => "{}"
25
+
| effects =>
26
+
let names := effects.reverse.map (fun
27
+
| .error => "Error")
28
+
"{" ++ String.intercalate ", " names ++ "}"
29
+
30
+
inductive Ty where
31
+
| int : Ty
32
+
| bool : Ty
33
+
| funTy : Ty → Effects → Ty → Ty
34
+
deriving Repr, Inhabited, BEq
35
+
36
+
inductive Expr where
37
+
| int : Int → Expr
38
+
| bool : Bool → Expr
39
+
| var : Name → Expr
40
+
| add : Expr → Expr → Expr
41
+
| sub : Expr → Expr → Expr
42
+
| mul : Expr → Expr → Expr
43
+
| div : Expr → Expr → Expr
44
+
| eq : Expr → Expr → Expr
45
+
| letE : Name → Expr → Expr → Expr
46
+
| ifE : Expr → Expr → Expr → Expr
47
+
| tryE : Expr → Expr → Expr
48
+
| lam : Name → Ty → Expr → Expr
49
+
| app : Expr → Expr → Expr
50
+
deriving Repr, Inhabited
51
+
52
+
inductive Value where
53
+
| int : Int → Value
54
+
| bool : Bool → Value
55
+
| closure : Name → Expr → List (Name × Value) → Value
56
+
deriving Repr, Inhabited
57
+
58
+
abbrev Env := List (Name × Value)
59
+
60
+
inductive RuntimeError where
61
+
| unboundVariable : Name → RuntimeError
62
+
| typeError : String → RuntimeError
63
+
| divisionByZero : RuntimeError
64
+
deriving Repr, Inhabited
65
+
66
+
abbrev EvalM := Except RuntimeError
67
+
68
+
def Env.lookup (env : Env) (name : Name) : Option Value :=
69
+
match env with
70
+
| [] => none
71
+
| (n, v) :: rest => if n = name then some v else rest.lookup name
72
+
73
+
def expectInt : Value → EvalM Int
74
+
| .int n => .ok n
75
+
| _ => .error (.typeError "expected an integer")
76
+
77
+
def expectBool : Value → EvalM Bool
78
+
| .bool b => .ok b
79
+
| _ => .error (.typeError "expected a boolean")
80
+
81
+
partial def eval (env : Env) : Expr → EvalM Value
82
+
| .int n => .ok (.int n)
83
+
| .bool b => .ok (.bool b)
84
+
| .var name =>
85
+
match env.lookup name with
86
+
| some v => .ok v
87
+
| none => .error (.unboundVariable name)
88
+
| .add lhs rhs => do
89
+
let l ← expectInt (← eval env lhs)
90
+
let r ← expectInt (← eval env rhs)
91
+
pure (.int (l + r))
92
+
| .sub lhs rhs => do
93
+
let l ← expectInt (← eval env lhs)
94
+
let r ← expectInt (← eval env rhs)
95
+
pure (.int (l - r))
96
+
| .mul lhs rhs => do
97
+
let l ← expectInt (← eval env lhs)
98
+
let r ← expectInt (← eval env rhs)
99
+
pure (.int (l * r))
100
+
| .div lhs rhs => do
101
+
let l ← expectInt (← eval env lhs)
102
+
let r ← expectInt (← eval env rhs)
103
+
if r = 0 then
104
+
.error .divisionByZero
105
+
else
106
+
pure (.int (l / r))
107
+
| .eq lhs rhs => do
108
+
let l ← expectInt (← eval env lhs)
109
+
let r ← expectInt (← eval env rhs)
110
+
pure (.bool (l = r))
111
+
| .letE name value body => do
112
+
let value' ← eval env value
113
+
eval ((name, value') :: env) body
114
+
| .ifE cond thenBranch elseBranch => do
115
+
let c ← expectBool (← eval env cond)
116
+
if c then
117
+
eval env thenBranch
118
+
else
119
+
eval env elseBranch
120
+
| .tryE body handler =>
121
+
match eval env body with
122
+
| .ok value => .ok value
123
+
| .error _ => eval env handler
124
+
| .lam param _ body =>
125
+
pure (.closure param body env)
126
+
| .app fn arg => do
127
+
let fnVal ← eval env fn
128
+
let argVal ← eval env arg
129
+
match fnVal with
130
+
| .closure param body closureEnv =>
131
+
eval ((param, argVal) :: closureEnv) body
132
+
| _ =>
133
+
.error (.typeError "expected a function")
134
+
135
+
def renderValue : Value → String
136
+
| .int n => toString n
137
+
| .bool b => toString b
138
+
| .closure _ _ _ => "<closure>"
139
+
140
+
abbrev TyEnv := List (Name × Ty)
141
+
142
+
structure Judgment where
143
+
ty : Ty
144
+
effects : Effects
145
+
deriving Repr, Inhabited
146
+
147
+
inductive TypeError where
148
+
| unboundVariable : Name → TypeError
149
+
| mismatch : Ty → Ty → TypeError
150
+
| expectedFunction : Ty → TypeError
151
+
deriving Repr, Inhabited
152
+
153
+
abbrev CheckM := Except TypeError
154
+
155
+
def TyEnv.lookup (env : TyEnv) (name : Name) : Option Ty :=
156
+
match env with
157
+
| [] => none
158
+
| (n, ty) :: rest => if n = name then some ty else rest.lookup name
159
+
160
+
def ensureType (expected actual : Ty) : CheckM Unit :=
161
+
if expected == actual then
162
+
pure ()
163
+
else
164
+
throw (.mismatch expected actual)
165
+
166
+
def pureJudgment (ty : Ty) : Judgment :=
167
+
{ ty := ty, effects := [] }
168
+
169
+
partial def inferType (env : TyEnv) : Expr → CheckM Judgment
170
+
| .int _ => pure (pureJudgment .int)
171
+
| .bool _ => pure (pureJudgment .bool)
172
+
| .var name =>
173
+
match env.lookup name with
174
+
| some ty => pure (pureJudgment ty)
175
+
| none => throw (.unboundVariable name)
176
+
| .add lhs rhs
177
+
| .sub lhs rhs
178
+
| .mul lhs rhs => do
179
+
let lhsJ ← inferType env lhs
180
+
let rhsJ ← inferType env rhs
181
+
ensureType .int lhsJ.ty
182
+
ensureType .int rhsJ.ty
183
+
pure { ty := .int, effects := lhsJ.effects.union rhsJ.effects }
184
+
| .div lhs rhs => do
185
+
let lhsJ ← inferType env lhs
186
+
let rhsJ ← inferType env rhs
187
+
ensureType .int lhsJ.ty
188
+
ensureType .int rhsJ.ty
189
+
pure {
190
+
ty := .int
191
+
effects := (lhsJ.effects.union rhsJ.effects).insert .error
192
+
}
193
+
| .eq lhs rhs => do
194
+
let lhsJ ← inferType env lhs
195
+
let rhsJ ← inferType env rhs
196
+
ensureType .int lhsJ.ty
197
+
ensureType .int rhsJ.ty
198
+
pure { ty := .bool, effects := lhsJ.effects.union rhsJ.effects }
199
+
| .letE name value body => do
200
+
let valueJ ← inferType env value
201
+
let bodyJ ← inferType ((name, valueJ.ty) :: env) body
202
+
pure {
203
+
ty := bodyJ.ty
204
+
effects := valueJ.effects.union bodyJ.effects
205
+
}
206
+
| .ifE cond thenBranch elseBranch => do
207
+
let condJ ← inferType env cond
208
+
ensureType .bool condJ.ty
209
+
let thenJ ← inferType env thenBranch
210
+
let elseJ ← inferType env elseBranch
211
+
ensureType thenJ.ty elseJ.ty
212
+
pure {
213
+
ty := thenJ.ty
214
+
effects := condJ.effects.union (thenJ.effects.union elseJ.effects)
215
+
}
216
+
| .tryE body handler => do
217
+
let bodyJ ← inferType env body
218
+
let handlerJ ← inferType env handler
219
+
ensureType bodyJ.ty handlerJ.ty
220
+
pure {
221
+
ty := bodyJ.ty
222
+
effects := (bodyJ.effects.erase .error).union handlerJ.effects
223
+
}
224
+
| .lam param paramTy body => do
225
+
let bodyJ ← inferType ((param, paramTy) :: env) body
226
+
pure (pureJudgment (.funTy paramTy bodyJ.effects bodyJ.ty))
227
+
| .app fn arg => do
228
+
let fnJ ← inferType env fn
229
+
let argJ ← inferType env arg
230
+
match fnJ.ty with
231
+
| .funTy paramTy latentEffects resultTy =>
232
+
ensureType paramTy argJ.ty
233
+
pure {
234
+
ty := resultTy
235
+
effects := fnJ.effects.union (argJ.effects.union latentEffects)
236
+
}
237
+
| _ =>
238
+
throw (.expectedFunction fnJ.ty)
239
+
240
+
def renderType : Ty → String
241
+
| .int => "Int"
242
+
| .bool => "Bool"
243
+
| .funTy lhs effects rhs => s!"({renderType lhs} -> {renderType rhs} ! {effects.render})"
244
+
245
+
def renderJudgment (judgment : Judgment) : String :=
246
+
s!"{renderType judgment.ty} ! {judgment.effects.render}"
247
+
248
+
def sampleProgram : Expr :=
249
+
.letE "inc" (.lam "x" .int (.add (.var "x") (.int 1)))
250
+
(.app (.var "inc") (.int 41))
251
+
252
+
def lexicalScopeProgram : Expr :=
253
+
.letE "x" (.int 10)
254
+
(.letE "f" (.lam "y" .int (.add (.var "x") (.var "y")))
255
+
(.letE "x" (.int 100)
256
+
(.app (.var "f") (.int 5))))
257
+
258
+
def conditionalProgram : Expr :=
259
+
.ifE (.eq (.mul (.int 6) (.int 7)) (.int 42))
260
+
(.int 1)
261
+
(.int 0)
262
+
263
+
end Mlang
+245
Mlang/Parser.lean
+245
Mlang/Parser.lean
···
1
+
import Mlang.Interpreter
2
+
3
+
namespace Mlang
4
+
5
+
inductive 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
+
29
+
inductive ParseError where
30
+
| lexError : String → ParseError
31
+
| unexpectedEof : String → ParseError
32
+
| unexpectedToken : String → ParseError
33
+
| trailingTokens : List Token → ParseError
34
+
deriving Repr, Inhabited
35
+
36
+
abbrev ParseM := Except ParseError
37
+
38
+
def isDigit (c : Char) : Bool :=
39
+
'0' <= c && c <= '9'
40
+
41
+
def isIdentStart (c : Char) : Bool :=
42
+
c.isAlpha || c = '_'
43
+
44
+
def isIdentContinue (c : Char) : Bool :=
45
+
isIdentStart c || isDigit c
46
+
47
+
def isAtomStart : Token → Bool
48
+
| .int _ | .bool _ | .ident _ | .lparen => true
49
+
| _ => false
50
+
51
+
partial 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
+
60
+
def charsToString (chars : List Char) : String :=
61
+
String.ofList chars
62
+
63
+
def 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
+
81
+
def 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
+
87
+
partial 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
+
114
+
def lex (input : String) : ParseM (List Token) :=
115
+
lexChars input.toList
116
+
117
+
abbrev ParserState := List Token
118
+
119
+
def 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
+
127
+
mutual
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")
145
+
end
146
+
147
+
mutual
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")
236
+
end
237
+
238
+
def 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
+
245
+
end Mlang
+76
README.md
+76
README.md
···
1
+
# mlang
2
+
3
+
A small functional language prototype written in Lean 4.
4
+
5
+
Current scope:
6
+
7
+
- integer and boolean literals
8
+
- variables
9
+
- `let`
10
+
- `if`
11
+
- typed lambdas
12
+
- function application
13
+
- integer arithmetic
14
+
- integer division
15
+
- lexical closures
16
+
- hand-written lexer and parser
17
+
- static type checker
18
+
- implicit effect tracking
19
+
20
+
The interpreter lives in [Mlang/Interpreter.lean](/home/nandi/code/mlang/Mlang/Interpreter.lean:1).
21
+
The parser lives in [Mlang/Parser.lean](/home/nandi/code/mlang/Mlang/Parser.lean:1).
22
+
23
+
## Run
24
+
25
+
With `devenv` installed:
26
+
27
+
```bash
28
+
devenv shell
29
+
build
30
+
run
31
+
```
32
+
33
+
You can also run commands directly without entering the shell:
34
+
35
+
```bash
36
+
devenv test
37
+
devenv shell -- build
38
+
devenv shell -- run
39
+
```
40
+
41
+
The executable supports a REPL and file execution:
42
+
43
+
```bash
44
+
devenv shell -- lake exe mlang
45
+
devenv shell -- lake exe mlang examples/samples.mlg
46
+
devenv shell -- lake exe mlang --demo
47
+
```
48
+
49
+
Current syntax:
50
+
51
+
```text
52
+
expr ::= let name = expr in expr
53
+
| if expr then expr else expr
54
+
| try expr with expr
55
+
| fun (name : type) => expr
56
+
| expr = expr
57
+
| expr + expr
58
+
| expr - expr
59
+
| expr * expr
60
+
| expr expr
61
+
| (expr)
62
+
| true | false | 123 | name
63
+
64
+
type ::= Int | Bool | type -> type | (type)
65
+
```
66
+
67
+
Expressions are checked as `Type ! Effects`. Pure expressions get `{}`; division carries `{Error}` implicitly. `try ... with ...` handles `Error` and removes it from the resulting effect set when recovered locally.
68
+
69
+
The REPL parses, typechecks, and evaluates one expression per line. Use `:quit` to exit.
70
+
71
+
## Next steps
72
+
73
+
- persist top-level bindings across REPL entries
74
+
- add recursive functions
75
+
- add algebraic data types and pattern matching
76
+
- compile to a bytecode VM or another backend
+65
devenv.lock
+65
devenv.lock
···
1
+
{
2
+
"nodes": {
3
+
"devenv": {
4
+
"locked": {
5
+
"dir": "src/modules",
6
+
"lastModified": 1780091591,
7
+
"narHash": "sha256-07KVQbmtDbtTU9DlbOQiIXXS+UA+t+/aQ65iY311bSc=",
8
+
"owner": "cachix",
9
+
"repo": "devenv",
10
+
"rev": "21d68a204558895af93ad82014f8fa83f9c9a51e",
11
+
"type": "github"
12
+
},
13
+
"original": {
14
+
"dir": "src/modules",
15
+
"owner": "cachix",
16
+
"repo": "devenv",
17
+
"type": "github"
18
+
}
19
+
},
20
+
"nixpkgs": {
21
+
"inputs": {
22
+
"nixpkgs-src": "nixpkgs-src"
23
+
},
24
+
"locked": {
25
+
"lastModified": 1778507786,
26
+
"narHash": "sha256-HzSQCKMsMr8r55LwM1JuzIOB+8bzk0FEv6sItKvsfoY=",
27
+
"owner": "cachix",
28
+
"repo": "devenv-nixpkgs",
29
+
"rev": "8f24a228a782e24576b155d1e39f0d914b380691",
30
+
"type": "github"
31
+
},
32
+
"original": {
33
+
"owner": "cachix",
34
+
"ref": "rolling",
35
+
"repo": "devenv-nixpkgs",
36
+
"type": "github"
37
+
}
38
+
},
39
+
"nixpkgs-src": {
40
+
"flake": false,
41
+
"locked": {
42
+
"lastModified": 1778274207,
43
+
"narHash": "sha256-I4puXmX1iovcCHZlRmztO3vW0mAbbRvq4F8wgIMQ1MM=",
44
+
"owner": "NixOS",
45
+
"repo": "nixpkgs",
46
+
"rev": "b3da656039dc7a6240f27b2ef8cc6a3ef3bccae7",
47
+
"type": "github"
48
+
},
49
+
"original": {
50
+
"owner": "NixOS",
51
+
"ref": "nixpkgs-unstable",
52
+
"repo": "nixpkgs",
53
+
"type": "github"
54
+
}
55
+
},
56
+
"root": {
57
+
"inputs": {
58
+
"devenv": "devenv",
59
+
"nixpkgs": "nixpkgs"
60
+
}
61
+
}
62
+
},
63
+
"root": "root",
64
+
"version": 7
65
+
}
+27
devenv.nix
+27
devenv.nix
···
1
+
{ pkgs, lib, config, inputs, ... }:
2
+
3
+
{
4
+
packages = with pkgs; [
5
+
git
6
+
lean4
7
+
];
8
+
9
+
scripts.build.exec = ''
10
+
lake build
11
+
'';
12
+
13
+
scripts.run.exec = ''
14
+
lake exe mlang
15
+
'';
16
+
17
+
enterShell = ''
18
+
echo "mlang devenv ready"
19
+
lean --version
20
+
lake --version
21
+
'';
22
+
23
+
enterTest = ''
24
+
lean --version
25
+
lake --version
26
+
'';
27
+
}
+18
devenv.yaml
+18
devenv.yaml
···
1
+
# yaml-language-server: $schema=https://devenv.sh/devenv.schema.json
2
+
inputs:
3
+
nixpkgs:
4
+
url: github:cachix/devenv-nixpkgs/rolling
5
+
6
+
# If you're using non-OSS software, you can set allow_unfree to true.
7
+
# allow_unfree: true
8
+
9
+
# If you're not willing to allow unsupported packages:
10
+
# allow_unsupported_system: false
11
+
12
+
# If you're willing to use a package that's vulnerable
13
+
# permitted_insecure_packages:
14
+
# - "openssl-1.1.1w"
15
+
16
+
# If you have more than one devenv you can merge them
17
+
#imports:
18
+
# - ./backend
+1
examples/samples.mlg
+1
examples/samples.mlg
···
1
+
try 10 / 0 with 42
+5
lake-manifest.json
+5
lake-manifest.json
+11
lakefile.lean
+11
lakefile.lean
+1
lean-toolchain
+1
lean-toolchain
···
1
+
leanprover/lean4:stable