nandi.uk
This repository has no description
1import Mlang.Nickel
2import Mlang.Http
3import Mlang.NickelHost
4
5namespace Mlang
6
7open Nickel
8
9abbrev Name := String
10
11inductive Effect where
12 | error : Effect
13 | io : Effect
14 deriving Repr, Inhabited, BEq
15
16abbrev Effects := List Effect
17
18def Effects.contains (effects : Effects) (effect : Effect) : Bool :=
19 effects.any (· == effect)
20
21def Effects.insert (effects : Effects) (effect : Effect) : Effects :=
22 if effects.contains effect then effects else effect :: effects
23
24def Effects.union (lhs rhs : Effects) : Effects :=
25 rhs.foldl Effects.insert lhs
26
27def Effects.erase (effects : Effects) (target : Effect) : Effects :=
28 effects.filter (· != target)
29
30def Effects.render : Effects → String
31 | [] => "{}"
32 | effects =>
33 let names := effects.reverse.map (fun
34 | .error => "Error"
35 | .io => "IO")
36 "{" ++ String.intercalate ", " names ++ "}"
37
38inductive Ty where
39 | int : Ty
40 | bool : Ty
41 | string : Ty
42 | data : Ty
43 | dataInt : Ty
44 | dataBool : Ty
45 | dataString : Ty
46 | dataNull : Ty
47 | dataArray : Ty → Ty
48 | dataRecord : List (String × Ty) → Ty
49 | list : Ty
50 | result : Ty
51 | error : Ty
52 | funTy : Ty → Effects → Ty → Ty
53 deriving Repr, Inhabited, BEq
54
55inductive Data where
56 | null : Data
57 | bool : Bool → Data
58 | int : Int → Data
59 | string : String → Data
60 | array : List Data → Data
61 | record : List (String × Data) → Data
62 deriving Repr, Inhabited, BEq
63
64inductive Expr where
65 | int : Int → Expr
66 | bool : Bool → Expr
67 | string : String → Expr
68 | null : Expr
69 | var : Name → Expr
70 | arrayE : List Expr → Expr
71 | recordE : List (String × Expr) → Expr
72 | add : Expr → Expr → Expr
73 | sub : Expr → Expr → Expr
74 | mul : Expr → Expr → Expr
75 | div : Expr → Expr → Expr
76 | eq : Expr → Expr → Expr
77 | letE : Name → Expr → Expr → Expr
78 | ifE : Expr → Expr → Expr → Expr
79 | tryE : Expr → Name → Expr → Expr
80 | parMapE : Name → Expr → Expr → Expr
81 | lam : Name → Ty → Expr → Expr
82 | app : Expr → Expr → Expr
83 deriving Repr, Inhabited
84
85inductive Value where
86 | int : Int → Value
87 | bool : Bool → Value
88 | string : String → Value
89 | data : Data → Value
90 | list : List Value → Value
91 | resultOk : Value → Value
92 | resultErr : String → Value
93 | error : String → Value
94 | builtinReadFile : Value
95 | builtinHttpGet : Value
96 | builtinReadFileNickel : Value
97 | builtinParseNickel : Value
98 | builtinParseJson : Value
99 | builtinDataGet : Value
100 | builtinDataGetField : Data → Value
101 | builtinDataAt : Value
102 | builtinDataAtIndex : Data → Value
103 | builtinDataAsInt : Value
104 | builtinDataAsString : Value
105 | builtinDataAsBool : Value
106 | builtinDataToJson : Value
107 | builtinDataToNickel : Value
108 | closure : Name → Expr → List (Name × Value) → Value
109 deriving Repr, Inhabited
110
111abbrev Env := List (Name × Value)
112
113inductive RuntimeError where
114 | unboundVariable : Name → RuntimeError
115 | typeError : String → RuntimeError
116 | divisionByZero : RuntimeError
117 | ioError : String → RuntimeError
118 deriving Repr, Inhabited
119
120abbrev EvalM := EIO RuntimeError
121
122def Env.lookup (env : Env) (name : Name) : Option Value :=
123 match env with
124 | [] => none
125 | (n, v) :: rest => if n = name then some v else rest.lookup name
126
127def expectInt : Value → EvalM Int
128 | .int n => pure n
129 | _ => throw (.typeError "expected an integer")
130
131def expectBool : Value → EvalM Bool
132 | .bool b => pure b
133 | _ => throw (.typeError "expected a boolean")
134
135def expectString : Value → EvalM String
136 | .string s => pure s
137 | _ => throw (.typeError "expected a string")
138
139def expectData : Value → EvalM Data
140 | .data term => pure term
141 | _ => throw (.typeError "expected a data value")
142
143def valueToData : Value → EvalM Data
144 | .data term => pure term
145 | .int n => pure (.int n)
146 | .bool b => pure (.bool b)
147 | .string s => pure (.string s)
148 | _ => throw (.typeError "data literals only support Int, Bool, String, and Data values")
149
150partial def dataType : Data → Ty
151 | .null => .dataNull
152 | .bool _ => .dataBool
153 | .int _ => .dataInt
154 | .string _ => .dataString
155 | .array [] => .dataArray .data
156 | .array (x :: xs) =>
157 let itemTy := dataType x
158 if xs.all (fun item => dataType item == itemTy) then
159 .dataArray itemTy
160 else
161 .dataArray .data
162 | .record fields =>
163 .dataRecord (fields.map (fun (name, value) => (name, dataType value)))
164
165def dataRecordField? : List (String × Ty) → String → Option Ty
166 | [], _ => none
167 | (name, ty) :: rest, target =>
168 if name = target then some ty else dataRecordField? rest target
169
170def liftScalarDataTy : Ty → Ty
171 | .dataInt => .int
172 | .dataBool => .bool
173 | .dataString => .string
174 | ty => ty
175
176partial def refineKnownDataTy (ty : Ty) : Ty :=
177 match ty with
178 | .dataInt => .int
179 | .dataBool => .bool
180 | .dataString => .string
181 | .dataNull => .data
182 | .dataArray itemTy => .dataArray (refineKnownDataTy itemTy)
183 | .dataRecord fields =>
184 .dataRecord (fields.map (fun (name, fieldTy) => (name, refineKnownDataTy fieldTy)))
185 | other => other
186
187def dataArrayGet? : List Data → Nat → Option Data
188 | [], _ => none
189 | x :: _, 0 => some x
190 | _ :: xs, n + 1 => dataArrayGet? xs n
191
192def runtimeErrorToValue : RuntimeError → Value
193 | .unboundVariable name => .error s!"unbound variable: {name}"
194 | .typeError msg => .error s!"type error: {msg}"
195 | .divisionByZero => .error "division by zero"
196 | .ioError msg => .error s!"io error: {msg}"
197
198def runtimeErrorToMessage : RuntimeError → String
199 | .unboundVariable name => s!"unbound variable: {name}"
200 | .typeError msg => s!"type error: {msg}"
201 | .divisionByZero => "division by zero"
202 | .ioError msg => s!"io error: {msg}"
203
204partial def Data.ofNickel : Nickel.Term → Data
205 | .null => .null
206 | .bool b => .bool b
207 | .int n => .int n
208 | .string s => .string s
209 | .array xs => .array (xs.map Data.ofNickel)
210 | .record fields => .record (fields.map (fun (k, v) => (k, Data.ofNickel v)))
211
212def parseRenderedData (rendered : String) : EvalM Data := do
213 match Nickel.parse rendered with
214 | .ok term => pure (Data.ofNickel term)
215 | .error err => throw (.typeError s!"host Nickel render parse error: {err}")
216
217def encodeMapResult : Except RuntimeError Value → Value
218 | .ok value => .resultOk value
219 | .error err => .resultErr (runtimeErrorToMessage err)
220
221def escapeJsonChar : Char → String
222 | '"' => "\\\""
223 | '\\' => "\\\\"
224 | '\n' => "\\n"
225 | '\r' => "\\r"
226 | '\t' => "\\t"
227 | c => c.toString
228
229def renderJsonString (s : String) : String :=
230 "\"" ++ String.join (s.toList.map escapeJsonChar) ++ "\""
231
232def isNickelKeyStart (c : Char) : Bool :=
233 c.isAlpha || c = '_'
234
235def isNickelKeyContinue (c : Char) : Bool :=
236 c.isAlpha || c.isDigit || c = '_' || c = '-'
237
238def renderNickelKey (s : String) : String :=
239 match s.toList with
240 | [] => renderJsonString s
241 | c :: cs =>
242 if isNickelKeyStart c && cs.all isNickelKeyContinue then
243 s
244 else
245 renderJsonString s
246
247partial def renderNickelData : Data → String
248 | .null => "null"
249 | .bool b => toString b
250 | .int n => toString n
251 | .string s => renderJsonString s
252 | .array xs => "[" ++ String.intercalate ", " (xs.map renderNickelData) ++ "]"
253 | .record fields =>
254 let rendered := fields.map (fun (k, v) => s!"{renderNickelKey k} = {renderNickelData v}")
255 "{ " ++ String.intercalate ", " rendered ++ " }"
256
257partial def renderJsonData : Data → String
258 | .null => "null"
259 | .bool b => if b then "true" else "false"
260 | .int n => toString n
261 | .string s => renderJsonString s
262 | .array xs => "[" ++ String.intercalate ", " (xs.map renderJsonData) ++ "]"
263 | .record fields =>
264 let rendered := fields.map (fun (k, v) => s!"{renderJsonString k}: {renderJsonData v}")
265 "{" ++ String.intercalate ", " rendered ++ "}"
266
267def builtinType? (name : Name) : Option Ty :=
268 match name with
269 | "readFile" => some (.funTy .string [.error, .io] .string)
270 | "httpGet" => some (.funTy .string [.error, .io] .string)
271 | "readFileNickel" => some (.funTy .string [.error, .io] .data)
272 | "parseNickel" => some (.funTy .string [.error] .data)
273 | "parseJson" => some (.funTy .string [.error] .data)
274 | "get" => some (.funTy .data [] (.funTy .string [.error] .data))
275 | "at" => some (.funTy .data [] (.funTy .int [.error] .data))
276 | "asInt" => some (.funTy .data [.error] .int)
277 | "asString" => some (.funTy .data [.error] .string)
278 | "asBool" => some (.funTy .data [.error] .bool)
279 | "toJson" => some (.funTy .data [] .string)
280 | "toNickel" => some (.funTy .data [] .string)
281 | _ => none
282
283def builtinValue? (name : Name) : Option Value :=
284 match name with
285 | "readFile" => some .builtinReadFile
286 | "httpGet" => some .builtinHttpGet
287 | "readFileNickel" => some .builtinReadFileNickel
288 | "parseNickel" => some .builtinParseNickel
289 | "parseJson" => some .builtinParseJson
290 | "get" => some .builtinDataGet
291 | "at" => some .builtinDataAt
292 | "asInt" => some .builtinDataAsInt
293 | "asString" => some .builtinDataAsString
294 | "asBool" => some .builtinDataAsBool
295 | "toJson" => some .builtinDataToJson
296 | "toNickel" => some .builtinDataToNickel
297 | _ => none
298
299mutual
300 partial def applyValue (fnVal argVal : Value) : EvalM Value := do
301 match fnVal with
302 | .closure param body closureEnv =>
303 eval ((param, argVal) :: closureEnv) body
304 | .builtinReadFile => do
305 let path ← expectString argVal
306 let contents ← IO.toEIO (fun err => .ioError (toString err)) (IO.FS.readFile path)
307 pure (.string contents)
308 | .builtinHttpGet => do
309 let url ← expectString argVal
310 let body ← IO.toEIO (fun err => .ioError (toString err)) (Http.httpGet url)
311 pure (.string body)
312 | .builtinReadFileNickel => do
313 let path ← expectString argVal
314 let rendered ← IO.toEIO (fun err => .ioError (toString err)) (NickelHost.evalFile path)
315 pure (.data (← parseRenderedData rendered))
316 | .builtinParseNickel => do
317 let source ← expectString argVal
318 let rendered ← IO.toEIO (fun err => .ioError (toString err)) (NickelHost.evalString source)
319 pure (.data (← parseRenderedData rendered))
320 | .builtinParseJson => do
321 let source ← expectString argVal
322 let rendered ← IO.toEIO (fun err => .ioError (toString err)) (NickelHost.evalJsonString source)
323 pure (.data (← parseRenderedData rendered))
324 | .builtinDataGet => do
325 let term ← expectData argVal
326 pure (.builtinDataGetField term)
327 | .builtinDataGetField term => do
328 let key ← expectString argVal
329 match term with
330 | .record fields =>
331 match fields.find? (fun (name, _) => name = key) with
332 | some (_, value) => pure (.data value)
333 | none => throw (.typeError s!"missing field: {key}")
334 | _ => throw (.typeError "get expects a record")
335 | .builtinDataAt => do
336 let term ← expectData argVal
337 pure (.builtinDataAtIndex term)
338 | .builtinDataAtIndex term => do
339 let idx ← expectInt argVal
340 if idx < 0 then
341 throw (.typeError s!"negative index: {idx}")
342 else
343 match term with
344 | .array items =>
345 match dataArrayGet? items idx.toNat with
346 | some value => pure (.data value)
347 | none => throw (RuntimeError.typeError s!"index out of bounds: {idx}")
348 | _ => throw (.typeError "at expects an array")
349 | .builtinDataAsInt => do
350 let term ← expectData argVal
351 match term with
352 | .int n => pure (.int n)
353 | _ => throw (.typeError "asInt expects an integer")
354 | .builtinDataAsString => do
355 let term ← expectData argVal
356 match term with
357 | .string s => pure (.string s)
358 | _ => throw (.typeError "asString expects a string")
359 | .builtinDataAsBool => do
360 let term ← expectData argVal
361 match term with
362 | .bool b => pure (.bool b)
363 | _ => throw (.typeError "asBool expects a boolean")
364 | .builtinDataToJson => do
365 let term ← expectData argVal
366 pure (.string (renderJsonData term))
367 | .builtinDataToNickel => do
368 let term ← expectData argVal
369 pure (.string (renderNickelData term))
370 | _ =>
371 match fnVal, argVal with
372 | .data (.record fields), .string key =>
373 match fields.find? (fun (name, _) => name = key) with
374 | some (_, value) => pure (.data value)
375 | none => throw (.typeError s!"missing field: {key}")
376 | .data (.array items), .int idx =>
377 if idx < 0 then
378 throw (.typeError s!"negative index: {idx}")
379 else
380 match dataArrayGet? items idx.toNat with
381 | some value => pure (.data value)
382 | none => throw (RuntimeError.typeError s!"index out of bounds: {idx}")
383 | .data _, .string _ =>
384 throw (.typeError "string dispatch expects a record")
385 | .data _, .int _ =>
386 throw (.typeError "int dispatch expects an array")
387 | _, _ =>
388 throw (.typeError "expected a function")
389
390 partial def eval (env : Env) : Expr → EvalM Value
391 | .int n => pure (.int n)
392 | .bool b => pure (.bool b)
393 | .string s => pure (.string s)
394 | .null => pure (.data .null)
395 | .var name =>
396 match env.lookup name with
397 | some v => pure v
398 | none =>
399 match builtinValue? name with
400 | some v => pure v
401 | none => throw (.unboundVariable name)
402 | .arrayE items => do
403 let values ← items.mapM (eval env)
404 pure (.data (.array (← values.mapM valueToData)))
405 | .recordE fields => do
406 let fields' ← fields.mapM (fun (name, value) => do
407 let value' ← eval env value
408 pure (name, (← valueToData value')))
409 pure (.data (.record fields'))
410 | .add lhs rhs => do
411 let l ← expectInt (← eval env lhs)
412 let r ← expectInt (← eval env rhs)
413 pure (.int (l + r))
414 | .sub lhs rhs => do
415 let l ← expectInt (← eval env lhs)
416 let r ← expectInt (← eval env rhs)
417 pure (.int (l - r))
418 | .mul lhs rhs => do
419 let l ← expectInt (← eval env lhs)
420 let r ← expectInt (← eval env rhs)
421 pure (.int (l * r))
422 | .div lhs rhs => do
423 let l ← expectInt (← eval env lhs)
424 let r ← expectInt (← eval env rhs)
425 if r = 0 then
426 throw .divisionByZero
427 else
428 pure (.int (l / r))
429 | .eq lhs rhs => do
430 let l ← expectInt (← eval env lhs)
431 let r ← expectInt (← eval env rhs)
432 pure (.bool (l = r))
433 | .letE name value body => do
434 let value' ← eval env value
435 eval ((name, value') :: env) body
436 | .ifE cond thenBranch elseBranch => do
437 let c ← expectBool (← eval env cond)
438 if c then
439 eval env thenBranch
440 else
441 eval env elseBranch
442 | .tryE body errName handler => do
443 try
444 eval env body
445 catch err =>
446 eval ((errName, runtimeErrorToValue err) :: env) handler
447 | .parMapE itemName collection body => do
448 let source ← expectData (← eval env collection)
449 match source with
450 | .array items =>
451 let tasks ← items.mapM (fun item =>
452 EIO.asTask (prio := .dedicated) (eval ((itemName, .data item) :: env) body))
453 let results : List (Except RuntimeError Value) := List.map Task.get tasks
454 pure (.list (results.map encodeMapResult))
455 | _ =>
456 throw (.typeError "pmap expects an array value")
457 | .lam param _ body =>
458 pure (.closure param body env)
459 | .app fn arg => do
460 let fnVal ← eval env fn
461 let argVal ← eval env arg
462 applyValue fnVal argVal
463end
464
465def renderData : Data → String := renderNickelData
466
467def renderValue : Value → String
468 | .int n => toString n
469 | .bool b => toString b
470 | .string s => s!"\"{s}\""
471 | .data data => renderData data
472 | .list items => "[" ++ String.intercalate ", " (items.map renderValue) ++ "]"
473 | .resultOk value => s!"ok({renderValue value})"
474 | .resultErr msg => s!"err(\"{msg}\")"
475 | .error msg => s!"<error:{msg}>"
476 | .builtinReadFile => "<builtin:readFile>"
477 | .builtinHttpGet => "<builtin:httpGet>"
478 | .builtinReadFileNickel => "<builtin:readFileNickel>"
479 | .builtinParseNickel => "<builtin:parseNickel>"
480 | .builtinParseJson => "<builtin:parseJson>"
481 | .builtinDataGet => "<builtin:get>"
482 | .builtinDataGetField _ => "<builtin:getField>"
483 | .builtinDataAt => "<builtin:at>"
484 | .builtinDataAtIndex _ => "<builtin:atIndex>"
485 | .builtinDataAsInt => "<builtin:asInt>"
486 | .builtinDataAsString => "<builtin:asString>"
487 | .builtinDataAsBool => "<builtin:asBool>"
488 | .builtinDataToJson => "<builtin:toJson>"
489 | .builtinDataToNickel => "<builtin:toNickel>"
490 | .closure _ _ _ => "<closure>"
491
492abbrev TyEnv := List (Name × Ty)
493
494structure Judgment where
495 ty : Ty
496 effects : Effects
497 deriving Repr, Inhabited
498
499inductive TypeError where
500 | unboundVariable : Name → TypeError
501 | mismatch : Ty → Ty → TypeError
502 | expectedFunction : Ty → TypeError
503 deriving Repr, Inhabited
504
505abbrev CheckM := Except TypeError
506
507def TyEnv.lookup (env : TyEnv) (name : Name) : Option Ty :=
508 match env with
509 | [] => none
510 | (n, ty) :: rest => if n = name then some ty else rest.lookup name
511
512def ensureType (expected actual : Ty) : CheckM Unit :=
513 if expected == actual then
514 pure ()
515 else
516 throw (.mismatch expected actual)
517
518def pureJudgment (ty : Ty) : Judgment :=
519 { ty := ty, effects := [] }
520
521def eraseDataRefinement : Ty → Ty
522 | .dataInt | .dataBool | .dataString | .dataNull | .dataArray _ | .dataRecord _ => .data
523 | ty => ty
524
525def canFlowTo (actual expected : Ty) : Bool :=
526 if actual == expected then
527 true
528 else
529 match actual, expected with
530 | .dataInt, .data => true
531 | .dataBool, .data => true
532 | .dataString, .data => true
533 | .dataNull, .data => true
534 | .dataArray _, .data => true
535 | .dataRecord _, .data => true
536 | .dataArray _, .dataArray .data => true
537 | _, _ => false
538
539partial def constString? : Expr → Option String
540 | .string s => some s
541 | _ => none
542
543unsafe def evalConstData? (env : List (Name × Data)) : Expr → Option Data
544 | .null => some .null
545 | .string s => some (.string s)
546 | .int n => some (.int n)
547 | .bool b => some (.bool b)
548 | .var name => env.lookup name
549 | .arrayE items => do
550 some (.array (← items.mapM (evalConstData? env)))
551 | .recordE fields => do
552 some (.record (← fields.mapM (fun (name, value) => do
553 let value' ← evalConstData? env value
554 pure (name, value'))))
555 | .letE name value body => do
556 let value' ← evalConstData? env value
557 evalConstData? ((name, value') :: env) body
558 | .ifE cond thenBranch elseBranch => do
559 match (← evalConstData? env cond) with
560 | .bool true => evalConstData? env thenBranch
561 | .bool false => evalConstData? env elseBranch
562 | _ => none
563 | .app fn arg => do
564 match fn with
565 | .var "parseNickel" =>
566 let source ← evalConstData? env arg
567 match source with
568 | .string s =>
569 match unsafeIO (NickelHost.evalString s) with
570 | .ok rendered =>
571 match Nickel.parse rendered with
572 | .ok term => some (Data.ofNickel term)
573 | .error _ => none
574 | .error _ => none
575 | _ => none
576 | .var "parseJson" =>
577 let source ← evalConstData? env arg
578 match source with
579 | .string s =>
580 match unsafeIO (NickelHost.evalJsonString s) with
581 | .ok rendered =>
582 match Nickel.parse rendered with
583 | .ok term => some (Data.ofNickel term)
584 | .error _ => none
585 | .error _ => none
586 | _ => none
587 | .var "httpGet" =>
588 let url ← evalConstData? env arg
589 match url with
590 | .string s =>
591 match unsafeIO (Http.httpGet s) with
592 | .ok body => some (.string body)
593 | .error _ => none
594 | _ => none
595 | .var "readFileNickel" =>
596 let path ← evalConstData? env arg
597 match path with
598 | .string p =>
599 match unsafeIO (NickelHost.evalFile p) with
600 | .ok rendered =>
601 match Nickel.parse rendered with
602 | .ok term => some (Data.ofNickel term)
603 | .error _ => none
604 | .error _ => none
605 | _ => none
606 | .app (.var "get") base => do
607 let container ← evalConstData? env base
608 let key ← evalConstData? env arg
609 match container, key with
610 | .record fields, .string field =>
611 match fields.find? (fun (name, _) => name = field) with
612 | some (_, value) => some value
613 | none => none
614 | _, _ => none
615 | .app (.var "at") base => do
616 let container ← evalConstData? env base
617 let index ← evalConstData? env arg
618 match container, index with
619 | .array items, .int idx =>
620 if idx < 0 then none else dataArrayGet? items idx.toNat
621 | _, _ => none
622 | _ => none
623 | _ => none
624
625unsafe def inferType (env : TyEnv) : Expr → CheckM Judgment
626 | .int _ => pure (pureJudgment .int)
627 | .bool _ => pure (pureJudgment .bool)
628 | .string _ => pure (pureJudgment .string)
629 | .null => pure (pureJudgment .dataNull)
630 | .var name =>
631 match env.lookup name with
632 | some ty => pure (pureJudgment ty)
633 | none =>
634 match builtinType? name with
635 | some ty => pure (pureJudgment ty)
636 | none => throw (.unboundVariable name)
637 | .arrayE items => do
638 let itemJs ← items.mapM (inferType env)
639 let dataTys ← itemJs.mapM (fun j =>
640 match j.ty with
641 | .int => pure .dataInt
642 | .bool => pure .dataBool
643 | .string => pure .dataString
644 | .data => pure .data
645 | .dataInt => pure .dataInt
646 | .dataBool => pure .dataBool
647 | .dataString => pure .dataString
648 | .dataNull => pure .dataNull
649 | .dataArray ty => pure (.dataArray ty)
650 | .dataRecord fields => pure (.dataRecord fields)
651 | ty => throw (.mismatch .data ty))
652 let itemTy :=
653 match dataTys with
654 | [] => .data
655 | first :: rest => if rest.all (· == first) then first else .data
656 pure {
657 ty := .dataArray itemTy
658 effects := itemJs.foldl (fun acc j => acc.union j.effects) []
659 }
660 | .recordE fields => do
661 let fieldJs ← fields.mapM (fun (name, value) => do pure (name, ← inferType env value))
662 let fieldTys ← fieldJs.mapM (fun (name, j) => do
663 let ty ← match j.ty with
664 | .int => pure .dataInt
665 | .bool => pure .dataBool
666 | .string => pure .dataString
667 | .data => pure .data
668 | .dataInt => pure .dataInt
669 | .dataBool => pure .dataBool
670 | .dataString => pure .dataString
671 | .dataNull => pure .dataNull
672 | .dataArray ty => pure (.dataArray ty)
673 | .dataRecord fields => pure (.dataRecord fields)
674 | ty => throw (.mismatch .data ty)
675 pure (name, ty, j.effects))
676 pure {
677 ty := .dataRecord (fieldTys.map (fun (name, ty, _) => (name, ty)))
678 effects := fieldTys.foldl (fun acc (_, _, effects) => acc.union effects) []
679 }
680 | .add lhs rhs
681 | .sub lhs rhs
682 | .mul lhs rhs => do
683 let lhsJ ← inferType env lhs
684 let rhsJ ← inferType env rhs
685 ensureType .int lhsJ.ty
686 ensureType .int rhsJ.ty
687 pure { ty := .int, effects := lhsJ.effects.union rhsJ.effects }
688 | .div lhs rhs => do
689 let lhsJ ← inferType env lhs
690 let rhsJ ← inferType env rhs
691 ensureType .int lhsJ.ty
692 ensureType .int rhsJ.ty
693 pure {
694 ty := .int
695 effects := (lhsJ.effects.union rhsJ.effects).insert .error
696 }
697 | .eq lhs rhs => do
698 let lhsJ ← inferType env lhs
699 let rhsJ ← inferType env rhs
700 ensureType .int lhsJ.ty
701 ensureType .int rhsJ.ty
702 pure { ty := .bool, effects := lhsJ.effects.union rhsJ.effects }
703 | .letE name value body => do
704 let valueJ ← inferType env value
705 let bodyJ ← inferType ((name, valueJ.ty) :: env) body
706 pure {
707 ty := bodyJ.ty
708 effects := valueJ.effects.union bodyJ.effects
709 }
710 | .ifE cond thenBranch elseBranch => do
711 let condJ ← inferType env cond
712 ensureType .bool condJ.ty
713 let thenJ ← inferType env thenBranch
714 let elseJ ← inferType env elseBranch
715 ensureType thenJ.ty elseJ.ty
716 pure {
717 ty := thenJ.ty
718 effects := condJ.effects.union (thenJ.effects.union elseJ.effects)
719 }
720 | .tryE body errName handler => do
721 let bodyJ ← inferType env body
722 let handlerJ ← inferType ((errName, .error) :: env) handler
723 ensureType bodyJ.ty handlerJ.ty
724 pure {
725 ty := bodyJ.ty
726 effects := (bodyJ.effects.erase .error).union handlerJ.effects
727 }
728 | .parMapE itemName collection body => do
729 let collectionJ ← inferType env collection
730 match collectionJ.ty with
731 | .data
732 | .dataArray _ =>
733 let itemTy :=
734 match collectionJ.ty with
735 | .dataArray ty => ty
736 | _ => .data
737 let bodyJ ← inferType ((itemName, itemTy) :: env) body
738 pure {
739 ty := .list
740 effects := collectionJ.effects.union bodyJ.effects
741 }
742 | _ =>
743 throw (.mismatch .data collectionJ.ty)
744 | .lam param paramTy body => do
745 let bodyJ ← inferType ((param, paramTy) :: env) body
746 pure (pureJudgment (.funTy paramTy bodyJ.effects bodyJ.ty))
747 | .app fn arg => do
748 let fnJ ← inferType env fn
749 let argJ ← inferType env arg
750 match fnJ.ty with
751 | .funTy paramTy latentEffects resultTy =>
752 if canFlowTo argJ.ty paramTy then
753 let refinedResultTy :=
754 match fn, arg, resultTy with
755 | .app (.var "get") base, .string key, .data =>
756 match inferType env base with
757 | .ok baseJ =>
758 match baseJ.ty with
759 | .dataRecord fields =>
760 match dataRecordField? fields key with
761 | some ty => liftScalarDataTy ty
762 | none => .data
763 | _ =>
764 match evalConstData? [] (.app fn arg) with
765 | some data => liftScalarDataTy (dataType data)
766 | none => .data
767 | .error _ => .data
768 | .app (.var "at") base, _, .data =>
769 match evalConstData? [] (.app fn arg) with
770 | some data => liftScalarDataTy (dataType data)
771 | none =>
772 match inferType env base with
773 | .ok baseJ =>
774 match baseJ.ty with
775 | .dataArray itemTy => liftScalarDataTy itemTy
776 | _ => .data
777 | .error _ => .data
778 | .var "parseNickel", _, .data =>
779 match evalConstData? [] (.app fn arg) with
780 | some data => refineKnownDataTy (dataType data)
781 | none => .data
782 | .var "parseJson", _, .data =>
783 match evalConstData? [] (.app fn arg) with
784 | some data => refineKnownDataTy (dataType data)
785 | none => .data
786 | .var "readFileNickel", _, .data =>
787 match evalConstData? [] (.app fn arg) with
788 | some data => refineKnownDataTy (dataType data)
789 | none => .data
790 | .var "asInt", _, .int =>
791 match argJ.ty with
792 | .dataInt => .int
793 | _ => .int
794 | .var "asString", _, .string =>
795 match argJ.ty with
796 | .dataString => .string
797 | _ => .string
798 | .var "asBool", _, .bool =>
799 match argJ.ty with
800 | .dataBool => .bool
801 | _ => .bool
802 | _, _, _ => resultTy
803 pure {
804 ty := refinedResultTy
805 effects := fnJ.effects.union (argJ.effects.union latentEffects)
806 }
807 else
808 throw (.mismatch paramTy argJ.ty)
809 | _ =>
810 throw (.expectedFunction fnJ.ty)
811
812partial def renderType : Ty → String
813 | .int => "Int"
814 | .bool => "Bool"
815 | .string => "String"
816 | .data => "Data"
817 | .dataInt => "Data:Int"
818 | .dataBool => "Data:Bool"
819 | .dataString => "Data:String"
820 | .dataNull => "Data:Null"
821 | .dataArray itemTy => s!"Data:[{renderType itemTy}]"
822 | .dataRecord fields =>
823 let rendered := fields.map (fun (name, ty) => s!"{name}: {renderType ty}")
824 "Data:{" ++ String.intercalate ", " rendered ++ "}"
825 | .list => "List"
826 | .result => "Result"
827 | .error => "Error"
828 | .funTy lhs effects rhs => s!"({renderType lhs} -> {renderType rhs} ! {effects.render})"
829
830def renderJudgment (judgment : Judgment) : String :=
831 s!"{renderType judgment.ty} ! {judgment.effects.render}"
832
833def sampleProgram : Expr :=
834 .letE "inc" (.lam "x" .int (.add (.var "x") (.int 1)))
835 (.app (.var "inc") (.int 41))
836
837def lexicalScopeProgram : Expr :=
838 .letE "x" (.int 10)
839 (.letE "f" (.lam "y" .int (.add (.var "x") (.var "y")))
840 (.letE "x" (.int 100)
841 (.app (.var "f") (.int 5))))
842
843def conditionalProgram : Expr :=
844 .ifE (.eq (.mul (.int 6) (.int 7)) (.int 42))
845 (.int 1)
846 (.int 0)
847
848end Mlang