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
10structure Rational where
11 num : Int
12 den : Nat
13 deriving Repr, Inhabited, BEq
14
15abbrev Decimal := Rational
16
17mutual
18 inductive Generator where
19 | exactRatio : Rational → Generator
20 | exactDecimal : Decimal → Generator
21 | rationalRefiner : LazyReal → Generator
22 | decimalRefiner : LazyReal → Generator
23 | piChudnovsky : Generator
24 | sqrt : Decimal → Generator
25 | add : Generator → Generator → Generator
26 | sub : Generator → Generator → Generator
27 | mul : Generator → Generator → Generator
28 | div : Generator → Generator → Generator
29 deriving Repr, Inhabited, BEq
30
31 inductive LazyReal where
32 | exact : Decimal → LazyReal
33 | ratioProcess : Rational → LazyReal
34 | decimalProcess : Decimal → LazyReal
35 | pi : LazyReal
36 | sqrt : Decimal → LazyReal
37 | add : LazyReal → LazyReal → LazyReal
38 | sub : LazyReal → LazyReal → LazyReal
39 | mul : LazyReal → LazyReal → LazyReal
40 | div : LazyReal → LazyReal → LazyReal
41 | generated : Generator → LazyReal
42 deriving Repr, Inhabited, BEq
43end
44
45def normalizeDecimalParts (negative : Bool) (whole frac : String) : String :=
46 let wholeChars := whole.toList.dropWhile (· = '0')
47 let whole' := if wholeChars.isEmpty then "0" else String.ofList wholeChars
48 let fracChars := frac.toList.reverse.dropWhile (· = '0') |>.reverse
49 let frac' := if fracChars.isEmpty then "0" else String.ofList fracChars
50 let sign := if negative && !(whole' = "0" && frac' = "0") then "-" else ""
51 sign ++ whole' ++ "." ++ frac'
52
53def parseDecimalParts (repr : String) : Bool × String × String :=
54 let chars := repr.toList
55 let (negative, chars) :=
56 match chars with
57 | '-' :: rest => (true, rest)
58 | _ => (false, chars)
59 let rec split (acc : List Char) : List Char → List Char × List Char
60 | [] => (acc.reverse, [])
61 | '.' :: rest => (acc.reverse, rest)
62 | c :: rest => split (c :: acc) rest
63 let (wholeChars, fracChars) := split [] chars
64 (negative, String.ofList wholeChars, String.ofList fracChars)
65
66def pow10 : Nat → Int
67 | 0 => 1
68 | n + 1 => 10 * pow10 n
69
70def powNat (base : Nat) : Nat → Nat
71 | 0 => 1
72 | n + 1 => base * powNat base n
73
74def mkRational (num : Int) (den : Nat) : Rational :=
75 if den = 0 then
76 { num := 0, den := 1 }
77 else if num = 0 then
78 { num := 0, den := 1 }
79 else
80 let g := Nat.gcd num.natAbs den
81 { num := num / Int.ofNat g, den := den / g }
82
83def parseDecimal (repr : String) : Decimal :=
84 let (negative, whole, frac) := parseDecimalParts repr
85 let digits := whole ++ frac
86 let magnitude := String.toInt? digits |>.getD 0
87 let signed := if negative then -magnitude else magnitude
88 mkRational signed (powNat 10 frac.length)
89
90def renderDecimalScaled (scaled : Int) (scale : Nat) : String :=
91 let negative := scaled < 0
92 let mag := scaled.natAbs
93 let digits := toString mag
94 if scale = 0 then
95 normalizeDecimalParts negative digits "0"
96 else if digits.length <= scale then
97 let zeros := String.ofList (List.replicate (scale - digits.length + 1) '0')
98 let padded := zeros ++ digits
99 let wholeLen := padded.length - scale
100 normalizeDecimalParts negative (padded.take wholeLen |>.toString) (padded.drop wholeLen |>.toString)
101 else
102 let wholeLen := digits.length - scale
103 normalizeDecimalParts negative (digits.take wholeLen |>.toString) (digits.drop wholeLen |>.toString)
104
105def decimalOfInt (n : Int) : Decimal :=
106 mkRational n 1
107
108def addDecimals (lhs rhs : Decimal) : Decimal :=
109 mkRational (lhs.num * Int.ofNat rhs.den + rhs.num * Int.ofNat lhs.den) (lhs.den * rhs.den)
110
111def subDecimals (lhs rhs : Decimal) : Decimal :=
112 mkRational (lhs.num * Int.ofNat rhs.den - rhs.num * Int.ofNat lhs.den) (lhs.den * rhs.den)
113
114def mulDecimals (lhs rhs : Decimal) : Decimal :=
115 mkRational (lhs.num * rhs.num) (lhs.den * rhs.den)
116
117def rationalEq (lhs rhs : Decimal) : Bool :=
118 lhs.num == rhs.num && lhs.den == rhs.den
119
120partial def countFactor (factor : Nat) (n : Nat) : Nat :=
121 let rec loop (count current : Nat) :=
122 if current = 0 then count
123 else if current % factor = 0 then loop (count + 1) (current / factor)
124 else count
125 loop 0 n
126
127partial def stripFactor (factor : Nat) (n : Nat) : Nat :=
128 let rec loop (current : Nat) :=
129 if current = 0 then 0
130 else if current % factor = 0 then loop (current / factor)
131 else current
132 loop n
133
134def renderDecimal (d : Decimal) : String :=
135 if d.den = 1 then
136 renderDecimalScaled d.num 0
137 else
138 let twos := countFactor 2 d.den
139 let withoutTwos := stripFactor 2 d.den
140 let fives := countFactor 5 withoutTwos
141 let rest := stripFactor 5 withoutTwos
142 if rest = 1 then
143 let scale := max twos fives
144 let mult2 := powNat 2 (scale - twos)
145 let mult5 := powNat 5 (scale - fives)
146 let scaledNum := d.num * Int.ofNat (mult2 * mult5)
147 renderDecimalScaled scaledNum scale
148 else
149 s!"{d.num}/{d.den}"
150
151def isTerminatingDecimal (q : Rational) : Bool :=
152 if q.den = 1 then
153 true
154 else
155 let withoutTwos := stripFactor 2 q.den
156 let withoutFives := stripFactor 5 withoutTwos
157 withoutFives = 1
158
159inductive Effect where
160 | error : Effect
161 | io : Effect
162 deriving Repr, Inhabited, BEq
163
164abbrev Effects := List Effect
165
166def Effects.contains (effects : Effects) (effect : Effect) : Bool :=
167 effects.any (· == effect)
168
169def Effects.insert (effects : Effects) (effect : Effect) : Effects :=
170 if effects.contains effect then effects else effect :: effects
171
172def Effects.union (lhs rhs : Effects) : Effects :=
173 rhs.foldl Effects.insert lhs
174
175def Effects.erase (effects : Effects) (target : Effect) : Effects :=
176 effects.filter (· != target)
177
178def Effects.render : Effects → String
179 | [] => "{}"
180 | effects =>
181 let names := effects.reverse.map (fun
182 | .error => "Error"
183 | .io => "IO")
184 "{" ++ String.intercalate ", " names ++ "}"
185
186inductive Ty where
187 | number : Ty
188 | int : Ty
189 | decimal : Ty
190 | rational : Ty
191 | lazyReal : Ty
192 | stability : Ty
193 | bool : Ty
194 | string : Ty
195 | data : Ty
196 | dataInt : Ty
197 | dataDecimal : Ty
198 | dataRational : Ty
199 | dataBool : Ty
200 | dataString : Ty
201 | dataNull : Ty
202 | dataArray : Ty → Ty
203 | dataRecord : List (String × Ty) → Ty
204 | list : Ty
205 | result : Ty
206 | error : Ty
207 | funTy : Ty → Effects → Ty → Ty
208 deriving Repr, Inhabited, BEq
209
210inductive Data where
211 | null : Data
212 | bool : Bool → Data
213 | int : Int → Data
214 | decimal : Decimal → Data
215 | string : String → Data
216 | array : List Data → Data
217 | record : List (String × Data) → Data
218 deriving Repr, Inhabited, BEq
219
220inductive Expr where
221 | int : Int → Expr
222 | decimal : Decimal → Expr
223 | bool : Bool → Expr
224 | string : String → Expr
225 | null : Expr
226 | var : Name → Expr
227 | arrayE : List Expr → Expr
228 | recordE : List (String × Expr) → Expr
229 | add : Expr → Expr → Expr
230 | sub : Expr → Expr → Expr
231 | mul : Expr → Expr → Expr
232 | div : Expr → Expr → Expr
233 | eq : Expr → Expr → Expr
234 | letE : Name → Expr → Expr → Expr
235 | ifE : Expr → Expr → Expr → Expr
236 | tryE : Expr → Name → Expr → Expr
237 | parMapE : Name → Expr → Expr → Expr
238 | lam : Name → Ty → Expr → Expr
239 | app : Expr → Expr → Expr
240 deriving Repr, Inhabited
241
242inductive Numeric where
243 | exact : Rational → Numeric
244 | composite : LazyReal → Numeric
245 deriving Repr, Inhabited, BEq
246
247inductive Value where
248 | number : Numeric → Value
249 | stability : String → Value
250 | bool : Bool → Value
251 | string : String → Value
252 | data : Data → Value
253 | list : List Value → Value
254 | resultOk : Value → Value
255 | resultErr : String → Value
256 | error : String → Value
257 | builtinReadFile : Value
258 | builtinHttpGet : Value
259 | builtinReadFileNickel : Value
260 | builtinParseNickel : Value
261 | builtinParseJson : Value
262 | builtinGetAturi : Value
263 | builtinDataGet : Value
264 | builtinDataGetField : Value → Value
265 | builtinDataAt : Value
266 | builtinDataAtIndex : Value → Value
267 | builtinDataAsInt : Value
268 | builtinDataAsDecimal : Value
269 | builtinRationalToInt : Value
270 | builtinRationalToDecimal : Value
271 | builtinDataAsString : Value
272 | builtinDataAsBool : Value
273 | builtinDataToJson : Value
274 | builtinDataToNickel : Value
275 | builtinSqrt : Value
276 | builtinProcess : Value
277 | builtinSynthesize : Value
278 | builtinFormula : Value
279 | builtinApprox : Value
280 | builtinApproxStep : Value → Value
281 | builtinStabilize : Value
282 | builtinStabilizeStep : Value → Value
283 | builtinBounds : Value
284 | builtinBoundsStep : Value → Value
285 | builtinRationalStability : Value
286 | builtinDecimalStability : Value
287 | closure : Name → Expr → List (Name × Value) → Value
288 deriving Repr, Inhabited
289
290abbrev Env := List (Name × Value)
291
292inductive Observation where
293 | asRational : Observation
294 | asDecimal : Observation
295 | asInt : Observation
296 | rationalStability : Observation
297 | decimalStability : Observation
298 | getField : String → Observation
299 | atIndex : Nat → Observation
300 | approx : Nat → Observation
301 | bounds : Nat → Observation
302 deriving Repr, Inhabited
303
304inductive ObservationResult where
305 | rational : Rational → ObservationResult
306 | decimal : Decimal → ObservationResult
307 | int : Int → ObservationResult
308 | stability : String → ObservationResult
309 | data : Data → ObservationResult
310 | bounds : Decimal → Decimal → ObservationResult
311 deriving Repr, Inhabited
312
313inductive RuntimeError where
314 | unboundVariable : Name → RuntimeError
315 | typeError : String → RuntimeError
316 | divisionByZero : RuntimeError
317 | ioError : String → RuntimeError
318 deriving Repr, Inhabited
319
320abbrev EvalM := EIO RuntimeError
321
322def numericOfInt (n : Int) : Numeric :=
323 .exact (decimalOfInt n)
324
325def numericOfDecimal (d : Decimal) : Numeric :=
326 .exact d
327
328def valueToDecimal : Value → EvalM Decimal
329 | .number (.exact q) => pure q
330 | _ => throw (.typeError "expected a numeric value")
331
332def divDecimals (lhs rhs : Decimal) : EvalM Decimal := do
333 if rhs.num = 0 then
334 throw .divisionByZero
335 else
336 pure (mkRational (lhs.num * Int.ofNat rhs.den) (lhs.den * rhs.num.natAbs) |>
337 fun q => if rhs.num < 0 then { q with num := -q.num } else q)
338
339def valueToLazyReal : Value → EvalM LazyReal
340 | .number (.composite r) => pure r
341 | .number (.exact q) => pure (.exact q)
342 | _ => throw (.typeError "expected a numeric or LazyReal value")
343
344def generatorComplexity : Generator → Nat
345 | .exactRatio _ => 1
346 | .exactDecimal _ => 1
347 | .rationalRefiner _ => 2
348 | .decimalRefiner _ => 2
349 | .piChudnovsky => 3
350 | .sqrt _ => 2
351 | .add lhs rhs => 1 + generatorComplexity lhs + generatorComplexity rhs
352 | .sub lhs rhs => 1 + generatorComplexity lhs + generatorComplexity rhs
353 | .mul lhs rhs => 1 + generatorComplexity lhs + generatorComplexity rhs
354 | .div lhs rhs => 1 + generatorComplexity lhs + generatorComplexity rhs
355
356def selectFirstGoodEnough [Inhabited α] (candidates : List α) (goodEnough : α → Bool) : α :=
357 match candidates.find? goodEnough with
358 | some candidate => candidate
359 | none =>
360 match candidates with
361 | candidate :: _ => candidate
362 | [] => default
363
364def generatorGoodEnough : Generator → Bool
365 | .exactRatio _ => true
366 | .exactDecimal _ => true
367 | .rationalRefiner _ => true
368 | .decimalRefiner _ => true
369 | .piChudnovsky => true
370 | .sqrt _ => true
371 | .add lhs rhs => generatorGoodEnough lhs && generatorGoodEnough rhs
372 | .sub lhs rhs => generatorGoodEnough lhs && generatorGoodEnough rhs
373 | .mul lhs rhs => generatorGoodEnough lhs && generatorGoodEnough rhs
374 | .div lhs rhs => generatorGoodEnough lhs && generatorGoodEnough rhs
375
376partial def synthesizedCandidates (r : LazyReal) : List Generator :=
377 match r with
378 | .exact q =>
379 if isTerminatingDecimal q then
380 [.exactDecimal q, .exactRatio q]
381 else
382 [.exactRatio q, .decimalRefiner (.exact q)]
383 | .ratioProcess q =>
384 if isTerminatingDecimal q then
385 [.exactDecimal q, .exactRatio q]
386 else
387 [.exactRatio q, .decimalRefiner (.ratioProcess q)]
388 | .decimalProcess d =>
389 [.exactDecimal d, .exactRatio d]
390 | .generated g =>
391 [g, .decimalRefiner (.generated g), .rationalRefiner (.generated g)]
392 | .pi =>
393 [.decimalRefiner .pi, .rationalRefiner .pi, .piChudnovsky]
394 | .sqrt d =>
395 [.decimalRefiner (.sqrt d), .rationalRefiner (.sqrt d), .sqrt d]
396 | .add lhs rhs =>
397 let lhsGen := selectFirstGoodEnough (synthesizedCandidates lhs) generatorGoodEnough
398 let rhsGen := selectFirstGoodEnough (synthesizedCandidates rhs) generatorGoodEnough
399 [.add lhsGen rhsGen, .decimalRefiner (.add lhs rhs), .rationalRefiner (.add lhs rhs)]
400 | .sub lhs rhs =>
401 let lhsGen := selectFirstGoodEnough (synthesizedCandidates lhs) generatorGoodEnough
402 let rhsGen := selectFirstGoodEnough (synthesizedCandidates rhs) generatorGoodEnough
403 [.sub lhsGen rhsGen, .decimalRefiner (.sub lhs rhs), .rationalRefiner (.sub lhs rhs)]
404 | .mul lhs rhs =>
405 let lhsGen := selectFirstGoodEnough (synthesizedCandidates lhs) generatorGoodEnough
406 let rhsGen := selectFirstGoodEnough (synthesizedCandidates rhs) generatorGoodEnough
407 [.mul lhsGen rhsGen, .decimalRefiner (.mul lhs rhs), .rationalRefiner (.mul lhs rhs)]
408 | .div lhs rhs =>
409 let lhsGen := selectFirstGoodEnough (synthesizedCandidates lhs) generatorGoodEnough
410 let rhsGen := selectFirstGoodEnough (synthesizedCandidates rhs) generatorGoodEnough
411 [.div lhsGen rhsGen, .decimalRefiner (.div lhs rhs), .rationalRefiner (.div lhs rhs)]
412
413def chooseSynthesizedGenerator (r : LazyReal) : Generator :=
414 selectFirstGoodEnough (synthesizedCandidates r) generatorGoodEnough
415
416mutual
417 partial def renderGeneratorFormula : Generator → String
418 | .exactRatio q => s!"{q.num}/{q.den}"
419 | .exactDecimal d => renderDecimal d
420 | .rationalRefiner r => s!"rationalRefine({renderLazyFormula r})"
421 | .decimalRefiner r => s!"decimalRefine({renderLazyFormula r})"
422 | .piChudnovsky =>
423 "426880 * sqrt(10005) / sum(k => ((-1)^k * (6k)! * (13591409 + 545140134k)) / ((3k)! * (k!)^3 * 640320^(3k)), k = 0..inf)"
424 | .sqrt d => s!"sqrt({renderDecimal d})"
425 | .add lhs rhs => s!"({renderGeneratorFormula lhs}) + ({renderGeneratorFormula rhs})"
426 | .sub lhs rhs => s!"({renderGeneratorFormula lhs}) - ({renderGeneratorFormula rhs})"
427 | .mul lhs rhs => s!"({renderGeneratorFormula lhs}) * ({renderGeneratorFormula rhs})"
428 | .div lhs rhs => s!"({renderGeneratorFormula lhs}) / ({renderGeneratorFormula rhs})"
429
430 partial def renderLazyFormula : LazyReal → String
431 | .exact q => renderDecimal q
432 | .ratioProcess q => s!"ratio({q.num}/{q.den})"
433 | .decimalProcess d => s!"decimal({renderDecimal d})"
434 | .pi => "pi"
435 | .sqrt d => s!"sqrt({renderDecimal d})"
436 | .add lhs rhs => s!"({renderLazyFormula lhs}) + ({renderLazyFormula rhs})"
437 | .sub lhs rhs => s!"({renderLazyFormula lhs}) - ({renderLazyFormula rhs})"
438 | .mul lhs rhs => s!"({renderLazyFormula lhs}) * ({renderLazyFormula rhs})"
439 | .div lhs rhs => s!"({renderLazyFormula lhs}) / ({renderLazyFormula rhs})"
440 | .generated g => renderGeneratorFormula g
441end
442
443def formulaOfValue (value : Value) : EvalM String := do
444 match value with
445 | .number (.exact q) =>
446 pure (renderGeneratorFormula (chooseSynthesizedGenerator (.exact q)))
447 | .number (.composite r) =>
448 pure (renderGeneratorFormula (chooseSynthesizedGenerator r))
449 | _ =>
450 let q ← valueToDecimal value
451 pure (renderGeneratorFormula (chooseSynthesizedGenerator (.exact q)))
452
453def synthesizeNumeric (value : Value) : EvalM Numeric := do
454 match value with
455 | .number (.exact q) =>
456 pure (.composite (.generated (chooseSynthesizedGenerator (.exact q))))
457 | .number (.composite r) =>
458 pure (.composite (.generated (chooseSynthesizedGenerator r)))
459 | _ =>
460 let q ← valueToDecimal value
461 pure (.composite (.generated (chooseSynthesizedGenerator (.exact q))))
462
463partial def natSqrtSearch (target lo hi : Nat) : Nat :=
464 if lo + 1 >= hi then
465 lo
466 else
467 let mid := lo + (hi - lo) / 2
468 if mid * mid ≤ target then
469 natSqrtSearch target mid hi
470 else
471 natSqrtSearch target lo mid
472
473def natSqrtFloor (target : Nat) : Nat :=
474 natSqrtSearch target 0 (target + 1)
475
476def sqrtBoundsOfDecimal (d : Decimal) (steps : Nat) : EvalM (Decimal × Decimal) := do
477 if d.num < 0 then
478 throw (.typeError "sqrt expects a non-negative decimal")
479 else
480 let scale := steps
481 let scaledTarget := d.num.natAbs * powNat 10 (2 * scale) / d.den
482 let loNat := natSqrtFloor scaledTarget
483 let lo := mkRational (Int.ofNat loNat) (powNat 10 scale)
484 let step := mkRational 1 (powNat 10 scale)
485 pure (lo, addDecimals lo step)
486
487def natFactorial : Nat → Nat
488 | 0 => 1
489 | n + 1 => (n + 1) * natFactorial n
490
491def chudnovskyTermMag (k : Nat) : Decimal :=
492 let sixFact := natFactorial (6 * k)
493 let threeFact := natFactorial (3 * k)
494 let kFact := natFactorial k
495 let coeff : Int := 13591409 + 545140134 * Int.ofNat k
496 let num := Int.ofNat sixFact * coeff
497 let den := threeFact * kFact * kFact * kFact * powNat 640320 (3 * k)
498 mkRational num den
499
500def chudnovskySignedTerm (k : Nat) : Decimal :=
501 let mag := chudnovskyTermMag k
502 if k % 2 = 0 then mag else { mag with num := -mag.num }
503
504def chudnovskySum (terms : Nat) : Decimal :=
505 let rec loop (k : Nat) (acc : Decimal) :=
506 if k < terms then
507 loop (k + 1) (addDecimals acc (chudnovskySignedTerm k))
508 else
509 acc
510 loop 0 (decimalOfInt 0)
511
512def piBounds (steps : Nat) : EvalM (Decimal × Decimal) := do
513 let terms := steps / 14 + 1
514 let sum := chudnovskySum terms
515 let tail := chudnovskyTermMag terms
516 let sumLo := subDecimals sum tail
517 let sumHi := addDecimals sum tail
518 let (sqrtLo, sqrtHi) ← sqrtBoundsOfDecimal (decimalOfInt 10005) (steps + 2)
519 let coeff := decimalOfInt 426880
520 let cLo := mulDecimals coeff sqrtLo
521 let cHi := mulDecimals coeff sqrtHi
522 let lo ← divDecimals cLo sumHi
523 let hi ← divDecimals cHi sumLo
524 pure (lo, hi)
525
526def minDecimal (a b : Decimal) : Decimal :=
527 if a.num * Int.ofNat b.den <= b.num * Int.ofNat a.den then a else b
528
529def maxDecimal (a b : Decimal) : Decimal :=
530 if a.num * Int.ofNat b.den >= b.num * Int.ofNat a.den then a else b
531
532def roundRationalToScale (q : Rational) (scale : Nat) : Rational :=
533 let factor := powNat 10 scale
534 let scaledNum := q.num * Int.ofNat factor
535 let denInt := Int.ofNat q.den
536 let adjust := Int.ofNat (q.den / 2)
537 let rounded :=
538 if scaledNum < 0 then
539 (scaledNum - adjust) / denInt
540 else
541 (scaledNum + adjust) / denInt
542 mkRational rounded factor
543
544def mulBounds (lo1 hi1 lo2 hi2 : Decimal) : Decimal × Decimal :=
545 let p1 := mulDecimals lo1 lo2
546 let p2 := mulDecimals lo1 hi2
547 let p3 := mulDecimals hi1 lo2
548 let p4 := mulDecimals hi1 hi2
549 let lo := minDecimal (minDecimal p1 p2) (minDecimal p3 p4)
550 let hi := maxDecimal (maxDecimal p1 p2) (maxDecimal p3 p4)
551 (lo, hi)
552
553mutual
554 partial def boundsGenerator (g : Generator) (steps : Nat) : EvalM (Decimal × Decimal) := do
555 match g with
556 | .exactRatio q => pure (q, q)
557 | .exactDecimal d => pure (d, d)
558 | .rationalRefiner r =>
559 let q ← approxLazyReal r steps
560 pure (q, q)
561 | .decimalRefiner r =>
562 let q ← approxLazyReal r steps
563 pure (roundRationalToScale q steps, roundRationalToScale q steps)
564 | .piChudnovsky => piBounds steps
565 | .sqrt d => sqrtBoundsOfDecimal d steps
566 | .add lhs rhs =>
567 let (llo, lhi) ← boundsGenerator lhs steps
568 let (rlo, rhi) ← boundsGenerator rhs steps
569 pure (addDecimals llo rlo, addDecimals lhi rhi)
570 | .sub lhs rhs =>
571 let (llo, lhi) ← boundsGenerator lhs steps
572 let (rlo, rhi) ← boundsGenerator rhs steps
573 pure (subDecimals llo rhi, subDecimals lhi rlo)
574 | .mul lhs rhs =>
575 let (llo, lhi) ← boundsGenerator lhs steps
576 let (rlo, rhi) ← boundsGenerator rhs steps
577 pure (mulBounds llo lhi rlo rhi)
578 | .div lhs rhs =>
579 let (llo, lhi) ← boundsGenerator lhs steps
580 let (rlo, rhi) ← boundsGenerator rhs steps
581 if rlo.num <= 0 && 0 <= rhi.num then
582 throw (.typeError "generated division interval crosses zero")
583 else
584 let invLo ← divDecimals (decimalOfInt 1) rhi
585 let invHi ← divDecimals (decimalOfInt 1) rlo
586 pure (mulBounds llo lhi invLo invHi)
587
588 partial def approxGenerator (g : Generator) (steps : Nat) : EvalM Decimal := do
589 match g with
590 | .exactRatio q => pure q
591 | .exactDecimal d => pure d
592 | .rationalRefiner r => approxLazyReal r steps
593 | .decimalRefiner r =>
594 let q ← approxLazyReal r steps
595 pure (roundRationalToScale q steps)
596 | .piChudnovsky =>
597 let (lo, hi) ← piBounds steps
598 divDecimals (addDecimals lo hi) (decimalOfInt 2)
599 | .sqrt d =>
600 let (lo, hi) ← sqrtBoundsOfDecimal d steps
601 divDecimals (addDecimals lo hi) (decimalOfInt 2)
602 | .add _ _ | .sub _ _ | .mul _ _ | .div _ _ =>
603 let (lo, hi) ← boundsGenerator g steps
604 divDecimals (addDecimals lo hi) (decimalOfInt 2)
605
606 partial def boundsLazyReal (r : LazyReal) (steps : Nat) : EvalM (Decimal × Decimal) := do
607 match r with
608 | .exact d => pure (d, d)
609 | .ratioProcess q => pure (q, q)
610 | .decimalProcess d => pure (d, d)
611 | .generated g => boundsGenerator g steps
612 | .pi => piBounds steps
613 | .sqrt d => sqrtBoundsOfDecimal d steps
614 | .add lhs rhs =>
615 let (llo, lhi) ← boundsLazyReal lhs steps
616 let (rlo, rhi) ← boundsLazyReal rhs steps
617 pure (addDecimals llo rlo, addDecimals lhi rhi)
618 | .sub lhs rhs =>
619 let (llo, lhi) ← boundsLazyReal lhs steps
620 let (rlo, rhi) ← boundsLazyReal rhs steps
621 pure (subDecimals llo rhi, subDecimals lhi rlo)
622 | .mul lhs rhs =>
623 let (llo, lhi) ← boundsLazyReal lhs steps
624 let (rlo, rhi) ← boundsLazyReal rhs steps
625 pure (mulBounds llo lhi rlo rhi)
626 | .div lhs rhs =>
627 let (llo, lhi) ← boundsLazyReal lhs steps
628 let (rlo, rhi) ← boundsLazyReal rhs steps
629 if rlo.num <= 0 && 0 <= rhi.num then
630 throw (.typeError "lazy division interval crosses zero")
631 else
632 let invLo ← divDecimals (decimalOfInt 1) rhi
633 let invHi ← divDecimals (decimalOfInt 1) rlo
634 pure (mulBounds llo lhi invLo invHi)
635
636 partial def approxLazyReal (r : LazyReal) (steps : Nat) : EvalM Decimal := do
637 match r with
638 | .exact d => pure d
639 | .ratioProcess q => pure q
640 | .decimalProcess d => pure d
641 | .generated g => approxGenerator g steps
642 | .pi =>
643 let (lo, hi) ← piBounds steps
644 divDecimals (addDecimals lo hi) (decimalOfInt 2)
645 | .sqrt d =>
646 let (lo, hi) ← sqrtBoundsOfDecimal d steps
647 divDecimals (addDecimals lo hi) (decimalOfInt 2)
648 | .add _ _ | .sub _ _ | .mul _ _ | .div _ _ =>
649 let (lo, hi) ← boundsLazyReal r steps
650 divDecimals (addDecimals lo hi) (decimalOfInt 2)
651end
652
653def stabilizeNumeric (value : Value) (steps : Nat) : EvalM Rational := do
654 match value with
655 | .number (.exact q) => pure (roundRationalToScale q steps)
656 | .number (.composite r) =>
657 let q ← approxLazyReal r steps
658 pure (roundRationalToScale q steps)
659 | _ =>
660 let q ← valueToDecimal value
661 pure (roundRationalToScale q steps)
662
663def Env.lookup (env : Env) (name : Name) : Option Value :=
664 match env with
665 | [] => none
666 | (n, v) :: rest => if n = name then some v else rest.lookup name
667
668def expectInt : Value → EvalM Int
669 | .number (.exact q) =>
670 if q.den = 1 then pure q.num else throw (.typeError "expected an integer")
671 | _ => throw (.typeError "expected an integer")
672
673def expectDecimal : Value → EvalM Decimal
674 | .number (.exact q) => pure q
675 | _ => throw (.typeError "expected a decimal")
676
677def expectLazyReal : Value → EvalM LazyReal
678 | .number (.composite r) => pure r
679 | _ => throw (.typeError "expected a LazyReal")
680
681def expectBool : Value → EvalM Bool
682 | .bool b => pure b
683 | _ => throw (.typeError "expected a boolean")
684
685def expectString : Value → EvalM String
686 | .string s => pure s
687 | _ => throw (.typeError "expected a string")
688
689def expectData : Value → EvalM Data
690 | .data term => pure term
691 | _ => throw (.typeError "expected a data value")
692
693def expectWholeNat (value : Value) : EvalM Nat := do
694 let q ← valueToDecimal value
695 if q.den ≠ 1 then
696 throw (.typeError "expected a whole rational")
697 else if q.num < 0 then
698 throw (.typeError "expected a non-negative whole rational")
699 else
700 pure q.num.toNat
701
702def rationalStabilityOfValue (value : Value) : String :=
703 match value with
704 | .number (.composite (.ratioProcess _)) => "Immediate"
705 | .number (.composite (.decimalProcess _)) => "Immediate"
706 | .number (.composite (.generated (.exactRatio _))) => "Immediate"
707 | .number (.composite (.generated (.exactDecimal _))) => "Immediate"
708 | .number (.exact _) => "Immediate"
709 | .number (.composite _) => "Refining"
710 | _ => "Unavailable"
711
712def decimalStabilityOfRational (q : Rational) : String :=
713 if isTerminatingDecimal q then "Terminating" else "Periodic"
714
715def decimalStabilityOfValue (value : Value) : String :=
716 match value with
717 | .number (.composite (.ratioProcess q)) => decimalStabilityOfRational q
718 | .number (.composite (.decimalProcess d)) => decimalStabilityOfRational d
719 | .number (.composite (.generated (.exactRatio q))) => decimalStabilityOfRational q
720 | .number (.composite (.generated (.exactDecimal d))) => decimalStabilityOfRational d
721 | .number (.exact q) => decimalStabilityOfRational q
722 | .number (.composite _) => "Refining"
723 | _ => "Unavailable"
724
725def observeValue (value : Value) (obs : Observation) : EvalM ObservationResult := do
726 match obs with
727 | .asRational =>
728 match value with
729 | .number (.exact q) => pure (.rational q)
730 | .number (.composite _) =>
731 throw (.typeError s!"rational observation failed: number is {rationalStabilityOfValue value}, not Immediate")
732 | _ =>
733 pure (.rational (← valueToDecimal value))
734 | .asDecimal =>
735 match value with
736 | .number (.exact q) =>
737 if isTerminatingDecimal q then
738 pure (.decimal q)
739 else
740 throw (.typeError s!"decimal observation failed: number is {decimalStabilityOfValue value}, not Terminating")
741 | .number (.composite _) =>
742 throw (.typeError s!"decimal observation failed: number is {decimalStabilityOfValue value}, not Terminating")
743 | _ =>
744 let q ← valueToDecimal value
745 if isTerminatingDecimal q then
746 pure (.decimal q)
747 else
748 throw (.typeError s!"decimal observation failed: number is {decimalStabilityOfValue value}, not Terminating")
749 | .asInt =>
750 match value with
751 | .number (.exact q) =>
752 if q.den = 1 then
753 pure (.int q.num)
754 else
755 throw (.typeError "integer observation failed: number is not whole")
756 | .number (.composite _) =>
757 throw (.typeError s!"integer observation failed: number is {rationalStabilityOfValue value}, not Immediate")
758 | _ =>
759 let q ← valueToDecimal value
760 if q.den = 1 then
761 pure (.int q.num)
762 else
763 throw (.typeError "integer observation failed: number is not whole")
764 | .rationalStability =>
765 pure (.stability (rationalStabilityOfValue value))
766 | .decimalStability =>
767 pure (.stability (decimalStabilityOfValue value))
768 | .getField key =>
769 match value with
770 | .data (.record fields) =>
771 match fields.find? (fun (name, _) => name = key) with
772 | some (_, field) => pure (.data field)
773 | none => throw (.typeError s!"missing field: {key}")
774 | _ => throw (.typeError "get expects a record")
775 | .atIndex idx =>
776 let rec arrayGet? : List Data → Nat → Option Data
777 | [], _ => none
778 | x :: _, 0 => some x
779 | _ :: xs, n + 1 => arrayGet? xs n
780 match value with
781 | .data (.array items) =>
782 match arrayGet? items idx with
783 | some item => pure (.data item)
784 | none => throw (RuntimeError.typeError s!"index out of bounds: {idx}")
785 | _ => throw (RuntimeError.typeError "at expects an array")
786 | .approx steps =>
787 let r ← valueToLazyReal value
788 pure (.rational (← approxLazyReal r steps))
789 | .bounds steps =>
790 let r ← valueToLazyReal value
791 let (lo, hi) ← boundsLazyReal r steps
792 pure (.bounds lo hi)
793
794def valueToData : Value → EvalM Data
795 | .data term => pure term
796 | .number (.exact q) => pure (.decimal q)
797 | .bool b => pure (.bool b)
798 | .string s => pure (.string s)
799 | _ => throw (.typeError "data literals only support Int, Decimal, Bool, String, and Data values")
800
801partial def dataType : Data → Ty
802 | .null => .dataNull
803 | .bool _ => .dataBool
804 | .int _ => .dataInt
805 | .decimal _ => .dataRational
806 | .string _ => .dataString
807 | .array [] => .dataArray .data
808 | .array (x :: xs) =>
809 let itemTy := dataType x
810 if xs.all (fun item => dataType item == itemTy) then
811 .dataArray itemTy
812 else
813 .dataArray .data
814 | .record fields =>
815 .dataRecord (fields.map (fun (name, value) => (name, dataType value)))
816
817def dataRecordField? : List (String × Ty) → String → Option Ty
818 | [], _ => none
819 | (name, ty) :: rest, target =>
820 if name = target then some ty else dataRecordField? rest target
821
822def liftScalarDataTy : Ty → Ty
823 | .dataInt => .int
824 | .dataDecimal => .decimal
825 | .dataRational => .rational
826 | .dataBool => .bool
827 | .dataString => .string
828 | ty => ty
829
830partial def refineKnownDataTy (ty : Ty) : Ty :=
831 match ty with
832 | .dataInt => .int
833 | .dataDecimal => .decimal
834 | .dataRational => .rational
835 | .dataBool => .bool
836 | .dataString => .string
837 | .dataNull => .data
838 | .dataArray itemTy => .dataArray (refineKnownDataTy itemTy)
839 | .dataRecord fields =>
840 .dataRecord (fields.map (fun (name, fieldTy) => (name, refineKnownDataTy fieldTy)))
841 | other => other
842
843def dataArrayGet? : List Data → Nat → Option Data
844 | [], _ => none
845 | x :: _, 0 => some x
846 | _ :: xs, n + 1 => dataArrayGet? xs n
847
848def runtimeErrorToValue : RuntimeError → Value
849 | .unboundVariable name => .error s!"unbound variable: {name}"
850 | .typeError msg => .error s!"type error: {msg}"
851 | .divisionByZero => .error "division by zero"
852 | .ioError msg => .error s!"io error: {msg}"
853
854def runtimeErrorToMessage : RuntimeError → String
855 | .unboundVariable name => s!"unbound variable: {name}"
856 | .typeError msg => s!"type error: {msg}"
857 | .divisionByZero => "division by zero"
858 | .ioError msg => s!"io error: {msg}"
859
860partial def Data.ofNickel : Nickel.Term → Data
861 | .null => .null
862 | .bool b => .bool b
863 | .int n => .int n
864 | .decimal d => .decimal (parseDecimal d)
865 | .string s => .string s
866 | .array xs => .array (xs.map Data.ofNickel)
867 | .record fields => .record (fields.map (fun (k, v) => (k, Data.ofNickel v)))
868
869def parseRenderedData (rendered : String) : EvalM Data := do
870 match Nickel.parse rendered with
871 | .ok term => pure (Data.ofNickel term)
872 | .error err => throw (.typeError s!"host Nickel render parse error: {err}")
873
874def encodeMapResult : Except RuntimeError Value → Value
875 | .ok value => .resultOk value
876 | .error err => .resultErr (runtimeErrorToMessage err)
877
878def escapeJsonChar : Char → String
879 | '"' => "\\\""
880 | '\\' => "\\\\"
881 | '\n' => "\\n"
882 | '\r' => "\\r"
883 | '\t' => "\\t"
884 | c => c.toString
885
886def renderJsonString (s : String) : String :=
887 "\"" ++ String.join (s.toList.map escapeJsonChar) ++ "\""
888
889def isNickelKeyStart (c : Char) : Bool :=
890 c.isAlpha || c = '_'
891
892def isNickelKeyContinue (c : Char) : Bool :=
893 c.isAlpha || c.isDigit || c = '_' || c = '-'
894
895def renderNickelKey (s : String) : String :=
896 match s.toList with
897 | [] => renderJsonString s
898 | c :: cs =>
899 if isNickelKeyStart c && cs.all isNickelKeyContinue then
900 s
901 else
902 renderJsonString s
903
904partial def renderNickelData : Data → String
905 | .null => "null"
906 | .bool b => toString b
907 | .int n => toString n
908 | .decimal d => renderDecimal d
909 | .string s => renderJsonString s
910 | .array xs => "[" ++ String.intercalate ", " (xs.map renderNickelData) ++ "]"
911 | .record fields =>
912 let rendered := fields.map (fun (k, v) => s!"{renderNickelKey k} = {renderNickelData v}")
913 "{ " ++ String.intercalate ", " rendered ++ " }"
914
915partial def renderJsonData : Data → String
916 | .null => "null"
917 | .bool b => if b then "true" else "false"
918 | .int n => toString n
919 | .decimal d => renderDecimal d
920 | .string s => renderJsonString s
921 | .array xs => "[" ++ String.intercalate ", " (xs.map renderJsonData) ++ "]"
922 | .record fields =>
923 let rendered := fields.map (fun (k, v) => s!"{renderJsonString k}: {renderJsonData v}")
924 "{" ++ String.intercalate ", " rendered ++ "}"
925
926def builtinType? (name : Name) : Option Ty :=
927 match name with
928 | "readFile" => some (.funTy .string [.error, .io] .string)
929 | "httpGet" => some (.funTy .string [.error, .io] .string)
930 | "readFileNickel" => some (.funTy .string [.error, .io] .data)
931 | "parseNickel" => some (.funTy .string [.error] .data)
932 | "parseJson" => some (.funTy .string [.error] .data)
933 | "getAturi" => some (.funTy .string [.error, .io] .data)
934 | "get" => some (.funTy .data [] (.funTy .string [.error] .data))
935 | "at" => some (.funTy .data [] (.funTy .number [.error] .data))
936 | "asInt" => some (.funTy .data [.error] .int)
937 | "asDecimal" => some (.funTy .data [.error] .decimal)
938 | "toInt" => some (.funTy .number [.error] .int)
939 | "toDecimal" => some (.funTy .number [.error] .decimal)
940 | "asString" => some (.funTy .data [.error] .string)
941 | "asBool" => some (.funTy .data [.error] .bool)
942 | "toJson" => some (.funTy .data [] .string)
943 | "toNickel" => some (.funTy .data [] .string)
944 | "rationalStability" => some (.funTy .number [] .stability)
945 | "decimalStability" => some (.funTy .number [] .stability)
946 | "pi" => some .number
947 | "sqrt" => some (.funTy .number [.error] .number)
948 | "process" => some (.funTy .number [] .number)
949 | "synthesize" => some (.funTy .number [.error] .number)
950 | "formula" => some (.funTy .number [.error] .string)
951 | "lazyRationalStability" => some (.funTy .number [] .stability)
952 | "lazyDecimalStability" => some (.funTy .number [] .stability)
953 | "stabilize" => some (.funTy .number [] (.funTy .number [.error] .number))
954 | "approx" => some (.funTy .number [] (.funTy .number [.error] .number))
955 | "bounds" => some (.funTy .number [] (.funTy .number [.error] .data))
956 | _ => none
957
958def builtinValue? (name : Name) : Option Value :=
959 match name with
960 | "readFile" => some .builtinReadFile
961 | "httpGet" => some .builtinHttpGet
962 | "readFileNickel" => some .builtinReadFileNickel
963 | "parseNickel" => some .builtinParseNickel
964 | "parseJson" => some .builtinParseJson
965 | "getAturi" => some .builtinGetAturi
966 | "get" => some .builtinDataGet
967 | "at" => some .builtinDataAt
968 | "asInt" => some .builtinDataAsInt
969 | "asDecimal" => some .builtinDataAsDecimal
970 | "toInt" => some .builtinRationalToInt
971 | "toDecimal" => some .builtinRationalToDecimal
972 | "asString" => some .builtinDataAsString
973 | "asBool" => some .builtinDataAsBool
974 | "toJson" => some .builtinDataToJson
975 | "toNickel" => some .builtinDataToNickel
976 | "rationalStability" => some .builtinRationalStability
977 | "decimalStability" => some .builtinDecimalStability
978 | "pi" => some (.number (.composite .pi))
979 | "sqrt" => some .builtinSqrt
980 | "process" => some .builtinProcess
981 | "synthesize" => some .builtinSynthesize
982 | "formula" => some .builtinFormula
983 | "lazyRationalStability" => some .builtinRationalStability
984 | "lazyDecimalStability" => some .builtinDecimalStability
985 | "stabilize" => some .builtinStabilize
986 | "approx" => some .builtinApprox
987 | "bounds" => some .builtinBounds
988 | _ => none
989
990mutual
991 partial def applyValue (fnVal argVal : Value) : EvalM Value := do
992 match fnVal with
993 | .closure param body closureEnv =>
994 eval ((param, argVal) :: closureEnv) body
995 | .builtinReadFile => do
996 let path ← expectString argVal
997 let contents ← IO.toEIO (fun err => .ioError (toString err)) (IO.FS.readFile path)
998 pure (.string contents)
999 | .builtinHttpGet => do
1000 let url ← expectString argVal
1001 let body ← IO.toEIO (fun err => .ioError (toString err)) (Http.httpGet url)
1002 pure (.string body)
1003 | .builtinReadFileNickel => do
1004 let path ← expectString argVal
1005 let rendered ← IO.toEIO (fun err => .ioError (toString err)) (NickelHost.evalFile path)
1006 pure (.data (← parseRenderedData rendered))
1007 | .builtinParseNickel => do
1008 let source ← expectString argVal
1009 let rendered ← IO.toEIO (fun err => .ioError (toString err)) (NickelHost.evalString source)
1010 pure (.data (← parseRenderedData rendered))
1011 | .builtinParseJson => do
1012 let source ← expectString argVal
1013 let rendered ← IO.toEIO (fun err => .ioError (toString err)) (NickelHost.evalJsonString source)
1014 pure (.data (← parseRenderedData rendered))
1015 | .builtinGetAturi => do
1016 let source ← expectString argVal
1017 let rendered ← IO.toEIO (fun err => .ioError (toString err)) (Http.parseAturi source)
1018 pure (.data (← parseRenderedData rendered))
1019 | .builtinDataGet => pure (.builtinDataGetField argVal)
1020 | .builtinDataGetField target => do
1021 let key ← expectString argVal
1022 match (← observeValue target (.getField key)) with
1023 | .data value => pure (.data value)
1024 | _ => throw (.typeError "get observation returned non-data")
1025 | .builtinDataAt => pure (.builtinDataAtIndex argVal)
1026 | .builtinDataAtIndex target => do
1027 let idx ← expectWholeNat argVal
1028 match (← observeValue target (.atIndex idx)) with
1029 | .data value => pure (.data value)
1030 | _ => throw (.typeError "at observation returned non-data")
1031 | .builtinDataAsInt => do
1032 let term ← expectData argVal
1033 match term with
1034 | .int n => pure (.number (numericOfInt n))
1035 | _ => throw (.typeError "asInt expects an integer")
1036 | .builtinDataAsDecimal => do
1037 let term ← expectData argVal
1038 match term with
1039 | .decimal d => pure (.number (numericOfDecimal d))
1040 | _ => throw (.typeError "asDecimal expects a decimal")
1041 | .builtinRationalToInt => do
1042 match (← observeValue argVal .asInt) with
1043 | .int n => pure (.number (numericOfInt n))
1044 | _ => throw (.typeError "toInt observation returned non-int")
1045 | .builtinRationalToDecimal => do
1046 match (← observeValue argVal .asDecimal) with
1047 | .decimal d => pure (.number (numericOfDecimal d))
1048 | _ => throw (.typeError "toDecimal observation returned non-decimal")
1049 | .builtinDataAsString => do
1050 let term ← expectData argVal
1051 match term with
1052 | .string s => pure (.string s)
1053 | _ => throw (.typeError "asString expects a string")
1054 | .builtinDataAsBool => do
1055 let term ← expectData argVal
1056 match term with
1057 | .bool b => pure (.bool b)
1058 | _ => throw (.typeError "asBool expects a boolean")
1059 | .builtinDataToJson => do
1060 let term ← expectData argVal
1061 pure (.string (renderJsonData term))
1062 | .builtinDataToNickel => do
1063 let term ← expectData argVal
1064 pure (.string (renderNickelData term))
1065 | .builtinRationalStability => do
1066 match (← observeValue argVal .rationalStability) with
1067 | .stability label => pure (.stability label)
1068 | _ => throw (.typeError "rationalStability observation returned non-stability")
1069 | .builtinDecimalStability => do
1070 match (← observeValue argVal .decimalStability) with
1071 | .stability label => pure (.stability label)
1072 | _ => throw (.typeError "decimalStability observation returned non-stability")
1073 | .builtinSqrt => do
1074 let d ← valueToDecimal argVal
1075 if d.num < 0 then
1076 throw (.typeError "sqrt expects a non-negative decimal")
1077 else
1078 pure (.number (.composite (.sqrt d)))
1079 | .builtinProcess => do
1080 match argVal with
1081 | .number (.exact q) => pure (.number (.composite (.exact q)))
1082 | .number (.composite r) => pure (.number (.composite r))
1083 | _ => throw (.typeError "process expects a number")
1084 | .builtinSynthesize => do
1085 pure (.number (← synthesizeNumeric argVal))
1086 | .builtinFormula => do
1087 pure (.string (← formulaOfValue argVal))
1088 | .builtinStabilize => pure (.builtinStabilizeStep argVal)
1089 | .builtinStabilizeStep target => do
1090 let steps ← expectWholeNat argVal
1091 pure (.number (.exact (← stabilizeNumeric target steps)))
1092 | .builtinApprox => pure (.builtinApproxStep argVal)
1093 | .builtinApproxStep target => do
1094 let steps ← expectWholeNat argVal
1095 match (← observeValue target (.approx steps)) with
1096 | .rational q => pure (.number (.exact q))
1097 | _ => throw (.typeError "approx observation returned non-rational")
1098 | .builtinBounds => pure (.builtinBoundsStep argVal)
1099 | .builtinBoundsStep target => do
1100 let steps ← expectWholeNat argVal
1101 match (← observeValue target (.bounds steps)) with
1102 | .bounds lo hi => pure (.data (.record [("lo", .decimal lo), ("hi", .decimal hi)]))
1103 | _ => throw (.typeError "bounds observation returned non-bounds")
1104 | .data (.record fields) =>
1105 let key ← expectString argVal
1106 match fields.find? (fun (name, _) => name = key) with
1107 | some (_, value) => pure (.data value)
1108 | none => throw (.typeError s!"missing field: {key}")
1109 | .data (.array items) =>
1110 let idx ← expectWholeNat argVal
1111 match dataArrayGet? items idx with
1112 | some value => pure (.data value)
1113 | none => throw (RuntimeError.typeError s!"index out of bounds: {idx}")
1114 | .data _ =>
1115 throw (.typeError "data value is not callable with this argument")
1116 | _ =>
1117 throw (.typeError "expected a function")
1118
1119 partial def eval (env : Env) : Expr → EvalM Value
1120 | .int n => pure (.number (numericOfInt n))
1121 | .decimal d => pure (.number (numericOfDecimal d))
1122 | .bool b => pure (.bool b)
1123 | .string s => pure (.string s)
1124 | .null => pure (.data .null)
1125 | .var name =>
1126 match env.lookup name with
1127 | some v => pure v
1128 | none =>
1129 match builtinValue? name with
1130 | some v => pure v
1131 | none => throw (.unboundVariable name)
1132 | .arrayE items => do
1133 let values ← items.mapM (eval env)
1134 pure (.data (.array (← values.mapM valueToData)))
1135 | .recordE fields => do
1136 let fields' ← fields.mapM (fun (name, value) => do
1137 let value' ← eval env value
1138 pure (name, (← valueToData value')))
1139 pure (.data (.record fields'))
1140 | .add lhs rhs => do
1141 let lVal ← eval env lhs
1142 let rVal ← eval env rhs
1143 match lVal, rVal with
1144 | .number (.composite _), _ | _, .number (.composite _) =>
1145 pure (.number (.composite (.add (← valueToLazyReal lVal) (← valueToLazyReal rVal))))
1146 | _, _ =>
1147 pure (.number (.exact (addDecimals (← valueToDecimal lVal) (← valueToDecimal rVal))))
1148 | .sub lhs rhs => do
1149 let lVal ← eval env lhs
1150 let rVal ← eval env rhs
1151 match lVal, rVal with
1152 | .number (.composite _), _ | _, .number (.composite _) =>
1153 pure (.number (.composite (.sub (← valueToLazyReal lVal) (← valueToLazyReal rVal))))
1154 | _, _ =>
1155 pure (.number (.exact (subDecimals (← valueToDecimal lVal) (← valueToDecimal rVal))))
1156 | .mul lhs rhs => do
1157 let lVal ← eval env lhs
1158 let rVal ← eval env rhs
1159 match lVal, rVal with
1160 | .number (.composite _), _ | _, .number (.composite _) =>
1161 pure (.number (.composite (.mul (← valueToLazyReal lVal) (← valueToLazyReal rVal))))
1162 | _, _ =>
1163 pure (.number (.exact (mulDecimals (← valueToDecimal lVal) (← valueToDecimal rVal))))
1164 | .div lhs rhs => do
1165 let lVal ← eval env lhs
1166 let rVal ← eval env rhs
1167 match lVal, rVal with
1168 | .number (.composite _), _ | _, .number (.composite _) =>
1169 pure (.number (.composite (.div (← valueToLazyReal lVal) (← valueToLazyReal rVal))))
1170 | _, _ =>
1171 pure (.number (.exact (← divDecimals (← valueToDecimal lVal) (← valueToDecimal rVal))))
1172 | .eq lhs rhs => do
1173 let l ← eval env lhs
1174 let r ← eval env rhs
1175 match l, r with
1176 | .number _, .number _ => pure (.bool (rationalEq (← valueToDecimal l) (← valueToDecimal r)))
1177 | _, _ => throw (.typeError "equality expects matching Int or Decimal operands")
1178 | .letE name value body => do
1179 let value' ← eval env value
1180 eval ((name, value') :: env) body
1181 | .ifE cond thenBranch elseBranch => do
1182 let c ← expectBool (← eval env cond)
1183 if c then
1184 eval env thenBranch
1185 else
1186 eval env elseBranch
1187 | .tryE body errName handler => do
1188 try
1189 eval env body
1190 catch err =>
1191 eval ((errName, runtimeErrorToValue err) :: env) handler
1192 | .parMapE itemName collection body => do
1193 let source ← expectData (← eval env collection)
1194 match source with
1195 | .array items =>
1196 let tasks ← items.mapM (fun item =>
1197 EIO.asTask (prio := .dedicated) (eval ((itemName, .data item) :: env) body))
1198 let results : List (Except RuntimeError Value) := List.map Task.get tasks
1199 pure (.list (results.map encodeMapResult))
1200 | _ =>
1201 throw (.typeError "pmap expects an array value")
1202 | .lam param _ body =>
1203 pure (.closure param body env)
1204 | .app fn arg => do
1205 let fnVal ← eval env fn
1206 let argVal ← eval env arg
1207 applyValue fnVal argVal
1208end
1209
1210def renderData : Data → String := renderNickelData
1211
1212def renderObservedScalar (value : Value) : Option String :=
1213 match value with
1214 | .number (.exact q) => some s!"{q.num}/{q.den}"
1215 | _ => none
1216
1217def renderValue : Value → String
1218 | value@(.number (.exact _)) =>
1219 match renderObservedScalar value with
1220 | some rendered => rendered
1221 | none => "<number>"
1222 | .stability label => label
1223 | .number (.composite (.ratioProcess q)) => s!"<process:ratio({q.num}/{q.den})>"
1224 | .number (.composite (.decimalProcess d)) => s!"<process:decimal({renderDecimal d})>"
1225 | .number (.composite (.generated (.exactRatio q))) => s!"<generator:ratio({q.num}/{q.den})>"
1226 | .number (.composite (.generated (.exactDecimal d))) => s!"<generator:decimal({renderDecimal d})>"
1227 | .number (.composite (.generated (.rationalRefiner _))) => "<generator:rational-refiner>"
1228 | .number (.composite (.generated (.decimalRefiner _))) => "<generator:decimal-refiner>"
1229 | .number (.composite (.generated .piChudnovsky)) => "<generator:pi[chudnovsky]>"
1230 | .number (.composite (.generated (.sqrt d))) => s!"<generator:sqrt({renderDecimal d})>"
1231 | .number (.composite (.generated (.add _ _))) => "<generator:add>"
1232 | .number (.composite (.generated (.sub _ _))) => "<generator:sub>"
1233 | .number (.composite (.generated (.mul _ _))) => "<generator:mul>"
1234 | .number (.composite (.generated (.div _ _))) => "<generator:div>"
1235 | .number (.composite (.exact d)) => s!"<lazy:{renderDecimal d}>"
1236 | .number (.composite .pi) => "<lazy:pi>"
1237 | .number (.composite (.sqrt d)) => s!"<lazy:sqrt({renderDecimal d})>"
1238 | .number (.composite (.add _ _)) => "<lazy:add>"
1239 | .number (.composite (.sub _ _)) => "<lazy:sub>"
1240 | .number (.composite (.mul _ _)) => "<lazy:mul>"
1241 | .number (.composite (.div _ _)) => "<lazy:div>"
1242 | .bool b => toString b
1243 | .string s => s!"\"{s}\""
1244 | .data data => renderData data
1245 | .list items => "[" ++ String.intercalate ", " (items.map renderValue) ++ "]"
1246 | .resultOk value => s!"ok({renderValue value})"
1247 | .resultErr msg => s!"err(\"{msg}\")"
1248 | .error msg => s!"<error:{msg}>"
1249 | .builtinReadFile => "<builtin:readFile>"
1250 | .builtinHttpGet => "<builtin:httpGet>"
1251 | .builtinReadFileNickel => "<builtin:readFileNickel>"
1252 | .builtinParseNickel => "<builtin:parseNickel>"
1253 | .builtinParseJson => "<builtin:parseJson>"
1254 | .builtinGetAturi => "<builtin:getAturi>"
1255 | .builtinDataGet => "<builtin:get>"
1256 | .builtinDataGetField _ => "<builtin:getField>"
1257 | .builtinDataAt => "<builtin:at>"
1258 | .builtinDataAtIndex _ => "<builtin:atIndex>"
1259 | .builtinDataAsInt => "<builtin:asInt>"
1260 | .builtinDataAsDecimal => "<builtin:asDecimal>"
1261 | .builtinRationalToInt => "<builtin:toInt>"
1262 | .builtinRationalToDecimal => "<builtin:toDecimal>"
1263 | .builtinDataAsString => "<builtin:asString>"
1264 | .builtinDataAsBool => "<builtin:asBool>"
1265 | .builtinDataToJson => "<builtin:toJson>"
1266 | .builtinDataToNickel => "<builtin:toNickel>"
1267 | .builtinRationalStability => "<builtin:rationalStability>"
1268 | .builtinDecimalStability => "<builtin:decimalStability>"
1269 | .builtinSqrt => "<builtin:sqrt>"
1270 | .builtinProcess => "<builtin:process>"
1271 | .builtinSynthesize => "<builtin:synthesize>"
1272 | .builtinFormula => "<builtin:formula>"
1273 | .builtinStabilize => "<builtin:stabilize>"
1274 | .builtinStabilizeStep _ => "<builtin:stabilizeStep>"
1275 | .builtinApprox => "<builtin:approx>"
1276 | .builtinApproxStep _ => "<builtin:approxStep>"
1277 | .builtinBounds => "<builtin:bounds>"
1278 | .builtinBoundsStep _ => "<builtin:boundsStep>"
1279 | .closure _ _ _ => "<closure>"
1280
1281abbrev TyEnv := List (Name × Ty)
1282
1283structure Judgment where
1284 ty : Ty
1285 effects : Effects
1286 deriving Repr, Inhabited
1287
1288inductive TypeError where
1289 | unboundVariable : Name → TypeError
1290 | mismatch : Ty → Ty → TypeError
1291 | expectedFunction : Ty → TypeError
1292 deriving Repr, Inhabited
1293
1294abbrev CheckM := Except TypeError
1295
1296def TyEnv.lookup (env : TyEnv) (name : Name) : Option Ty :=
1297 match env with
1298 | [] => none
1299 | (n, ty) :: rest => if n = name then some ty else rest.lookup name
1300
1301def ensureType (expected actual : Ty) : CheckM Unit :=
1302 if expected == actual then
1303 pure ()
1304 else
1305 throw (.mismatch expected actual)
1306
1307def isNumericTy : Ty → Bool
1308 | .number | .int | .decimal | .rational | .lazyReal => true
1309 | _ => false
1310
1311def pureJudgment (ty : Ty) : Judgment :=
1312 { ty := ty, effects := [] }
1313
1314def eraseDataRefinement : Ty → Ty
1315 | .dataInt | .dataDecimal | .dataRational | .dataBool | .dataString | .dataNull | .dataArray _ | .dataRecord _ => .data
1316 | ty => ty
1317
1318def canFlowTo (actual expected : Ty) : Bool :=
1319 if actual == expected then
1320 true
1321 else
1322 match actual, expected with
1323 | .number, .number => true
1324 | .int, .number => true
1325 | .decimal, .number => true
1326 | .rational, .number => true
1327 | .lazyReal, .number => true
1328 | .number, .decimal => true
1329 | .number, .rational => true
1330 | .int, .decimal => true
1331 | .int, .rational => true
1332 | .decimal, .rational => true
1333 | .rational, .decimal => true
1334 | .dataInt, .data => true
1335 | .dataDecimal, .data => true
1336 | .dataRational, .data => true
1337 | .dataBool, .data => true
1338 | .dataString, .data => true
1339 | .dataNull, .data => true
1340 | .dataArray _, .data => true
1341 | .dataRecord _, .data => true
1342 | .dataArray _, .dataArray .data => true
1343 | _, _ => false
1344
1345partial def constString? : Expr → Option String
1346 | .string s => some s
1347 | _ => none
1348
1349unsafe def evalConstData? (env : List (Name × Data)) : Expr → Option Data
1350 | .null => some .null
1351 | .string s => some (.string s)
1352 | .int n => some (.int n)
1353 | .decimal d => some (.decimal d)
1354 | .bool b => some (.bool b)
1355 | .var name => env.lookup name
1356 | .arrayE items => do
1357 some (.array (← items.mapM (evalConstData? env)))
1358 | .recordE fields => do
1359 some (.record (← fields.mapM (fun (name, value) => do
1360 let value' ← evalConstData? env value
1361 pure (name, value'))))
1362 | .letE name value body => do
1363 let value' ← evalConstData? env value
1364 evalConstData? ((name, value') :: env) body
1365 | .ifE cond thenBranch elseBranch => do
1366 match (← evalConstData? env cond) with
1367 | .bool true => evalConstData? env thenBranch
1368 | .bool false => evalConstData? env elseBranch
1369 | _ => none
1370 | .app fn arg => do
1371 match fn with
1372 | .var "parseNickel" =>
1373 let source ← evalConstData? env arg
1374 match source with
1375 | .string s =>
1376 match unsafeIO (NickelHost.evalString s) with
1377 | .ok rendered =>
1378 match Nickel.parse rendered with
1379 | .ok term => some (Data.ofNickel term)
1380 | .error _ => none
1381 | .error _ => none
1382 | _ => none
1383 | .var "parseJson" =>
1384 let source ← evalConstData? env arg
1385 match source with
1386 | .string s =>
1387 match unsafeIO (NickelHost.evalJsonString s) with
1388 | .ok rendered =>
1389 match Nickel.parse rendered with
1390 | .ok term => some (Data.ofNickel term)
1391 | .error _ => none
1392 | .error _ => none
1393 | _ => none
1394 | .var "httpGet" =>
1395 let url ← evalConstData? env arg
1396 match url with
1397 | .string s =>
1398 match unsafeIO (Http.httpGet s) with
1399 | .ok body => some (.string body)
1400 | .error _ => none
1401 | _ => none
1402 | .var "getAturi" =>
1403 let source ← evalConstData? env arg
1404 match source with
1405 | .string s =>
1406 match unsafeIO (Http.parseAturi s) with
1407 | .ok rendered =>
1408 match Nickel.parse rendered with
1409 | .ok term => some (Data.ofNickel term)
1410 | .error _ => none
1411 | .error _ => none
1412 | _ => none
1413 | .var "readFileNickel" =>
1414 let path ← evalConstData? env arg
1415 match path with
1416 | .string p =>
1417 match unsafeIO (NickelHost.evalFile p) with
1418 | .ok rendered =>
1419 match Nickel.parse rendered with
1420 | .ok term => some (Data.ofNickel term)
1421 | .error _ => none
1422 | .error _ => none
1423 | _ => none
1424 | .app (.var "get") base => do
1425 let container ← evalConstData? env base
1426 let key ← evalConstData? env arg
1427 match container, key with
1428 | .record fields, .string field =>
1429 match fields.find? (fun (name, _) => name = field) with
1430 | some (_, value) => some value
1431 | none => none
1432 | _, _ => none
1433 | .app (.var "at") base => do
1434 let container ← evalConstData? env base
1435 let index ← evalConstData? env arg
1436 match container, index with
1437 | .array items, .int idx =>
1438 if idx < 0 then none else dataArrayGet? items idx.toNat
1439 | _, _ => none
1440 | _ => none
1441 | _ => none
1442
1443unsafe def inferType (env : TyEnv) : Expr → CheckM Judgment
1444 | .int _ => pure (pureJudgment .number)
1445 | .decimal _ => pure (pureJudgment .number)
1446 | .bool _ => pure (pureJudgment .bool)
1447 | .string _ => pure (pureJudgment .string)
1448 | .null => pure (pureJudgment .dataNull)
1449 | .var name =>
1450 match env.lookup name with
1451 | some ty => pure (pureJudgment ty)
1452 | none =>
1453 match builtinType? name with
1454 | some ty => pure (pureJudgment ty)
1455 | none => throw (.unboundVariable name)
1456 | .arrayE items => do
1457 let itemJs ← items.mapM (inferType env)
1458 let dataTys ← itemJs.mapM (fun j =>
1459 match j.ty with
1460 | .number => pure .dataRational
1461 | .int => pure .dataInt
1462 | .decimal => pure .dataDecimal
1463 | .rational => pure .dataRational
1464 | .bool => pure .dataBool
1465 | .string => pure .dataString
1466 | .data => pure .data
1467 | .dataInt => pure .dataInt
1468 | .dataDecimal => pure .dataDecimal
1469 | .dataRational => pure .dataRational
1470 | .dataBool => pure .dataBool
1471 | .dataString => pure .dataString
1472 | .dataNull => pure .dataNull
1473 | .dataArray ty => pure (.dataArray ty)
1474 | .dataRecord fields => pure (.dataRecord fields)
1475 | ty => throw (.mismatch .data ty))
1476 let itemTy :=
1477 match dataTys with
1478 | [] => .data
1479 | first :: rest => if rest.all (· == first) then first else .data
1480 pure {
1481 ty := .dataArray itemTy
1482 effects := itemJs.foldl (fun acc j => acc.union j.effects) []
1483 }
1484 | .recordE fields => do
1485 let fieldJs ← fields.mapM (fun (name, value) => do pure (name, ← inferType env value))
1486 let fieldTys ← fieldJs.mapM (fun (name, j) => do
1487 let ty ← match j.ty with
1488 | .number => pure .dataRational
1489 | .int => pure .dataInt
1490 | .decimal => pure .dataDecimal
1491 | .rational => pure .dataRational
1492 | .bool => pure .dataBool
1493 | .string => pure .dataString
1494 | .data => pure .data
1495 | .dataInt => pure .dataInt
1496 | .dataDecimal => pure .dataDecimal
1497 | .dataRational => pure .dataRational
1498 | .dataBool => pure .dataBool
1499 | .dataString => pure .dataString
1500 | .dataNull => pure .dataNull
1501 | .dataArray ty => pure (.dataArray ty)
1502 | .dataRecord fields => pure (.dataRecord fields)
1503 | ty => throw (.mismatch .data ty)
1504 pure (name, ty, j.effects))
1505 pure {
1506 ty := .dataRecord (fieldTys.map (fun (name, ty, _) => (name, ty)))
1507 effects := fieldTys.foldl (fun acc (_, _, effects) => acc.union effects) []
1508 }
1509 | .add lhs rhs
1510 | .sub lhs rhs
1511 | .mul lhs rhs => do
1512 let lhsJ ← inferType env lhs
1513 let rhsJ ← inferType env rhs
1514 if isNumericTy lhsJ.ty && isNumericTy rhsJ.ty then
1515 pure {
1516 ty := .number
1517 effects := lhsJ.effects.union rhsJ.effects
1518 }
1519 else
1520 throw (.mismatch lhsJ.ty rhsJ.ty)
1521 | .div lhs rhs => do
1522 let lhsJ ← inferType env lhs
1523 let rhsJ ← inferType env rhs
1524 if isNumericTy lhsJ.ty && isNumericTy rhsJ.ty then
1525 pure {
1526 ty := .number
1527 effects := (lhsJ.effects.union rhsJ.effects).insert .error
1528 }
1529 else
1530 throw (.mismatch lhsJ.ty rhsJ.ty)
1531 | .eq lhs rhs => do
1532 let lhsJ ← inferType env lhs
1533 let rhsJ ← inferType env rhs
1534 if isNumericTy lhsJ.ty && isNumericTy rhsJ.ty then
1535 pure { ty := .bool, effects := lhsJ.effects.union rhsJ.effects }
1536 else
1537 throw (.mismatch lhsJ.ty rhsJ.ty)
1538 | .letE name value body => do
1539 let valueJ ← inferType env value
1540 let bodyJ ← inferType ((name, valueJ.ty) :: env) body
1541 pure {
1542 ty := bodyJ.ty
1543 effects := valueJ.effects.union bodyJ.effects
1544 }
1545 | .ifE cond thenBranch elseBranch => do
1546 let condJ ← inferType env cond
1547 ensureType .bool condJ.ty
1548 let thenJ ← inferType env thenBranch
1549 let elseJ ← inferType env elseBranch
1550 ensureType thenJ.ty elseJ.ty
1551 pure {
1552 ty := thenJ.ty
1553 effects := condJ.effects.union (thenJ.effects.union elseJ.effects)
1554 }
1555 | .tryE body errName handler => do
1556 let bodyJ ← inferType env body
1557 let handlerJ ← inferType ((errName, .error) :: env) handler
1558 ensureType bodyJ.ty handlerJ.ty
1559 pure {
1560 ty := bodyJ.ty
1561 effects := (bodyJ.effects.erase .error).union handlerJ.effects
1562 }
1563 | .parMapE itemName collection body => do
1564 let collectionJ ← inferType env collection
1565 match collectionJ.ty with
1566 | .data
1567 | .dataArray _ =>
1568 let itemTy :=
1569 match collectionJ.ty with
1570 | .dataArray ty => ty
1571 | _ => .data
1572 let bodyJ ← inferType ((itemName, itemTy) :: env) body
1573 pure {
1574 ty := .list
1575 effects := collectionJ.effects.union bodyJ.effects
1576 }
1577 | _ =>
1578 throw (.mismatch .data collectionJ.ty)
1579 | .lam param paramTy body => do
1580 let bodyJ ← inferType ((param, paramTy) :: env) body
1581 pure (pureJudgment (.funTy paramTy bodyJ.effects bodyJ.ty))
1582 | .app fn arg => do
1583 let fnJ ← inferType env fn
1584 let argJ ← inferType env arg
1585 match fnJ.ty with
1586 | .funTy paramTy latentEffects resultTy =>
1587 if canFlowTo argJ.ty paramTy then
1588 let refinedResultTy :=
1589 match fn, arg, resultTy with
1590 | .app (.var "get") base, .string key, .data =>
1591 match inferType env base with
1592 | .ok baseJ =>
1593 match baseJ.ty with
1594 | .dataRecord fields =>
1595 match dataRecordField? fields key with
1596 | some ty => liftScalarDataTy ty
1597 | none => .data
1598 | _ =>
1599 match evalConstData? [] (.app fn arg) with
1600 | some data => liftScalarDataTy (dataType data)
1601 | none => .data
1602 | .error _ => .data
1603 | .app (.var "at") base, _, .data =>
1604 match evalConstData? [] (.app fn arg) with
1605 | some data => liftScalarDataTy (dataType data)
1606 | none =>
1607 match inferType env base with
1608 | .ok baseJ =>
1609 match baseJ.ty with
1610 | .dataArray itemTy => liftScalarDataTy itemTy
1611 | _ => .data
1612 | .error _ => .data
1613 | .var "parseNickel", _, .data =>
1614 match evalConstData? [] (.app fn arg) with
1615 | some data => refineKnownDataTy (dataType data)
1616 | none => .data
1617 | .var "parseJson", _, .data =>
1618 match evalConstData? [] (.app fn arg) with
1619 | some data => refineKnownDataTy (dataType data)
1620 | none => .data
1621 | .var "readFileNickel", _, .data =>
1622 match evalConstData? [] (.app fn arg) with
1623 | some data => refineKnownDataTy (dataType data)
1624 | none => .data
1625 | .var "asInt", _, .int =>
1626 match argJ.ty with
1627 | .dataInt => .int
1628 | _ => .int
1629 | .var "asDecimal", _, .decimal =>
1630 match argJ.ty with
1631 | .dataDecimal => .decimal
1632 | _ => .decimal
1633 | .var "toInt", _, .int =>
1634 .int
1635 | .var "toDecimal", _, .decimal =>
1636 .decimal
1637 | .var "asString", _, .string =>
1638 match argJ.ty with
1639 | .dataString => .string
1640 | _ => .string
1641 | .var "asBool", _, .bool =>
1642 match argJ.ty with
1643 | .dataBool => .bool
1644 | _ => .bool
1645 | .app (.var "approx") _, _, .number =>
1646 .number
1647 | .app (.var "stabilize") _, _, .number =>
1648 .number
1649 | .app (.var "bounds") _, _, .data =>
1650 .data
1651 | _, _, _ => resultTy
1652 pure {
1653 ty := refinedResultTy
1654 effects := fnJ.effects.union (argJ.effects.union latentEffects)
1655 }
1656 else
1657 throw (.mismatch paramTy argJ.ty)
1658 | _ =>
1659 throw (.expectedFunction fnJ.ty)
1660
1661partial def renderType : Ty → String
1662 | .number => "Number"
1663 | .int => "Int"
1664 | .decimal => "Decimal"
1665 | .rational => "Number"
1666 | .lazyReal => "Number"
1667 | .stability => "Stability"
1668 | .bool => "Bool"
1669 | .string => "String"
1670 | .data => "Data"
1671 | .dataInt => "Data:Int"
1672 | .dataDecimal => "Data:Decimal"
1673 | .dataRational => "Data:Rational"
1674 | .dataBool => "Data:Bool"
1675 | .dataString => "Data:String"
1676 | .dataNull => "Data:Null"
1677 | .dataArray itemTy => s!"Data:[{renderType itemTy}]"
1678 | .dataRecord fields =>
1679 let rendered := fields.map (fun (name, ty) => s!"{name}: {renderType ty}")
1680 "Data:{" ++ String.intercalate ", " rendered ++ "}"
1681 | .list => "List"
1682 | .result => "Result"
1683 | .error => "Error"
1684 | .funTy lhs effects rhs => s!"({renderType lhs} -> {renderType rhs} ! {effects.render})"
1685
1686def renderTypeError : TypeError → String
1687 | .unboundVariable name => s!"unbound variable {name}"
1688 | .mismatch expected actual => s!"expected {renderType expected}, got {renderType actual}"
1689 | .expectedFunction actual => s!"expected function, got {renderType actual}"
1690
1691def renderJudgment (judgment : Judgment) : String :=
1692 s!"{renderType judgment.ty} ! {judgment.effects.render}"
1693
1694def sampleProgram : Expr :=
1695 .letE "inc" (.lam "x" .int (.add (.var "x") (.int 1)))
1696 (.app (.var "inc") (.int 41))
1697
1698def lexicalScopeProgram : Expr :=
1699 .letE "x" (.int 10)
1700 (.letE "f" (.lam "y" .int (.add (.var "x") (.var "y")))
1701 (.letE "x" (.int 100)
1702 (.app (.var "f") (.int 5))))
1703
1704def conditionalProgram : Expr :=
1705 .ifE (.eq (.mul (.int 6) (.int 7)) (.int 42))
1706 (.int 1)
1707 (.int 0)
1708
1709end Mlang