-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathCore.lean
More file actions
7580 lines (7438 loc) · 393 KB
/
Copy pathCore.lean
File metadata and controls
7580 lines (7438 loc) · 393 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
import Lean
import Init.Data.ByteArray.Extra
import LeanExe.Extract.Env
import LeanExe.Extract.ReleaseCheck
import LeanExe.Extract.StructuralRec
import LeanExe.IR.Core
import LeanExe.Runtime
open Lean
namespace LeanExe.Extract.Core
structure ExtractedForInStepBody where
bodyTargets : List Nat
bodyValues : List IRExpr
bodyLets : List LeanExe.IR.LocalLet
bodyDone : IRExpr
nextLocal : Nat
def releaseForInStepTemporaries (ctx : Context) (ty : Ty)
(step : ExtractedForInStepBody) : ExtractedForInStepBody :=
let released := addLiveSlots (localLetsReleasedSlots step.bodyLets) (exprReleasedSlots step.bodyDone)
let owners := (localLetsOwnedNonrecursiveHeapSlots ctx step.bodyLets).filter fun slot =>
!released.contains slot
if owners.isEmpty then step else
let protectedSlots := (tyReleaseOwnerSlotOffsets ty).filterMap fun offset => step.bodyTargets[offset]?
let doneSlot := step.nextLocal
let releaseSlot := doneSlot + 1
let cleanup := owners.foldl (fun (prior, lets) slot =>
let cond := prior.foldl
(fun cond other => .and cond (.not (.eqU64 (.local slot) (.local other))))
(.not (.eqU64 (.local slot) (.u64 0)))
(slot :: prior, lets ++ [.branch cond [.expr releaseSlot (.release (.local slot))] []]))
(protectedSlots, [])
{ step with
bodyLets := step.bodyLets ++ [.expr doneSlot step.bodyDone] ++ cleanup.snd
bodyDone := .local doneSlot
nextLocal := releaseSlot + 1 }
def valueIteConst
(cond : IRCond)
(thenValue elseValue : ExtractedValue) :
Except String ExtractedValue :=
match condConst? cond with
| some true => .ok thenValue
| some false => .ok elseValue
| none => valueIte cond thenValue elseValue
def boolExprConst (cond : IRCond) : IRExpr :=
match condConst? cond with
| some true => .u64 1
| some false => .u64 0
| none => boolExpr cond
def uint64OfNatLTName : Name := .str (.str .anonymous "UInt64") "ofNatLT"
def uint32OfNatLTName : Name := .str (.str .anonymous "UInt32") "ofNatLT"
def uint8OfNatLTName : Name := .str (.str .anonymous "UInt8") "ofNatLT"
def generatedBEqMethodName : Name → Bool
| .str _ "beq" => true
| _ => false
def structuralBEqMethod? (expr : Expr) : Bool :=
match appFnArgs expr with
| (.const name _, []) => generatedBEqMethodName name
| _ => false
partial def structuralBEqEvidence? (env : Environment) (fuel : Nat) (expr : Expr) : Bool :=
match fuel with
| 0 => false
| fuel + 1 =>
match appFnArgs expr with
| (.const ``instBEqOfDecidableEq _, _) => true
| (.const ``Option.instBEq _, args) =>
match args.reverse with
| evidence :: _ => structuralBEqEvidence? env fuel evidence
| _ => false
| (.const ``Array.instBEq _, args) =>
match args.reverse with
| evidence :: _ => structuralBEqEvidence? env fuel evidence
| _ => false
| (.const ``BEq.mk _, args) =>
match args.reverse with
| method :: _ => structuralBEqMethod? method
| _ => false
| (.const name levels, args) =>
match env.find? name with
| some info =>
match info.value? with
| some value =>
structuralBEqEvidence? env fuel
(rebuildApp
(value.instantiateLevelParamsArray info.levelParams.toArray levels.toArray)
args)
| none => false
| none => false
| _ => false
def structuralBEqApplication? (env : Environment) (name : Name) (expr : Expr) : Bool :=
name == ``BEq.beq &&
match appFnArgs expr with
| (_, _type :: evidence :: _left :: _right :: []) => structuralBEqEvidence? env 16 evidence
| _ => false
def directPrimitiveClassProjection (name : Name) : Bool :=
name == ``OfNat.ofNat || name == ``HAdd.hAdd || name == ``HSub.hSub ||
name == ``HMul.hMul || name == ``HDiv.hDiv || name == ``HMod.hMod ||
name == ``LT.lt || name == ``LE.le || name == ``GT.gt || name == ``GE.ge ||
name == ``Min.min || name == ``Max.max
def classEvidenceNormalizedApp? (env : Environment) (name : Name) (expr : Expr) : Option Expr :=
if structuralBEqApplication? env name expr || directPrimitiveClassProjection name then
none
else if isEvidenceProjectionFunction env name || classEvidenceApplication? env expr then
let normalized := normalizeClassEvidenceExpr env 64 expr
let (fn, _) := appFnArgs normalized
match fn.consumeMData with
| .const normalizedName _ => if normalizedName == name then none else some normalized
| _ => some normalized
else
none
def directScalarLtPrimitive (name : Name) : Bool :=
name == ``Nat.lt || name == ``UInt64.lt || name == ``UInt32.lt ||
name == ``UInt8.lt
def directScalarLePrimitive (name : Name) : Bool :=
name == ``Nat.le || name == ``UInt64.le || name == ``UInt32.le ||
name == ``UInt8.le
mutual
partial def extractStructuralRecCallValueFrom
(ctx : Context)
(locals : List Binding)
(nextLocal : Nat)
(functionName : Name)
(arg : ExtractedValue)
(capturedArgs : List ExtractedValue)
(extraArgs : List Expr) :
Except String (ExtractedValue × Nat) := do
let index ←
match functionIndex? ctx functionName with
| some index => .ok index
| none => .error s!"structural recursive function is not compiled: {functionName}"
let sig ←
match functionSignature? ctx functionName with
| some sig => .ok sig
| none => .error s!"unsupported function type or declaration: {functionName}"
let paramTy ←
match sig.params with
| paramTy :: _ => .ok paramTy
| _ => .error s!"unsupported structural recursion arity: {functionName}"
let argSlots ← materializeStrictInternalSlotsWithSummaries ctx.freshResultOwnerOffsets paramTy arg nextLocal
let bound := bindStrictSlots argSlots.slots argSlots.nextLocal
let expectedExtra := sig.params.drop 1
let extraResult ←
if extraArgs.isEmpty && !capturedArgs.isEmpty then
materializeCapturedStructuralArgs expectedExtra capturedArgs bound.nextLocal
else
let dynamicExtraArgs ← dynamicStructuralExtraArgs expectedExtra extraArgs
extractCallArgsFrom ctx locals bound.nextLocal expectedExtra dynamicExtraArgs
let slotCount := internalSlots sig.result
let slotStart := extraResult.nextLocal
let slots := (List.range slotCount).map (fun offset => slotStart + offset)
let value := valueFromInternalSlots sig.result fun offset => .local (slotStart + offset)
.ok
(wrapValueLets (argSlots.lets ++ bound.lets ++ extraResult.lets)
(.letCall slots index (bound.slots ++ extraResult.args) value),
slotStart + slotCount)
partial def extractWfRecursorCallValueFrom
(ctx : Context)
(locals : List Binding)
(nextLocal : Nat)
(functionName : Name)
(args : List Expr) :
Except String (ExtractedValue × Nat) := do
match args with
| arg :: _proof :: extraArgs =>
let argResult ← extractValueFrom ctx locals nextLocal arg
extractStructuralRecCallValueFrom ctx locals argResult.snd functionName argResult.fst []
extraArgs
| _ => .error s!"unsupported well-founded recursive call: {functionName}"
partial def extractNatRecursorCallValueFrom
(ctx : Context)
(locals : List Binding)
(nextLocal : Nat)
(functionName : Name)
(args : List Expr) :
Except String (ExtractedValue × Nat) := do
let index ←
match functionIndex? ctx functionName with
| some index => .ok index
| none => .error s!"Nat recursive function is not compiled: {functionName}"
let sig ←
match functionSignature? ctx functionName with
| some sig => .ok sig
| none => .error s!"unsupported function type or declaration: {functionName}"
let carriedParams ←
match sig.params with
| .nat :: carried => .ok carried
| _ => .error s!"unsupported Nat recursive function arity: {functionName}"
if args.length != carriedParams.length then
.error s!"Nat recursive call arity mismatch: {functionName}"
else
strictCallMaterializationCheck ctx functionName carriedParams args
let argsResult ← extractCallArgsFrom ctx locals nextLocal carriedParams args
let slotCount := internalSlots sig.result
let slotStart := argsResult.nextLocal
let slots := (List.range slotCount).map (fun offset => slotStart + offset)
let value := valueFromInternalSlots sig.result fun offset => .local (slotStart + offset)
let fuelArg : IRExpr := .u64Bin .sub (.local 0) (.u64 1)
.ok
(wrapValueLets argsResult.lets
(.letCall slots index (fuelArg :: argsResult.args) value),
slotStart + slotCount)
partial def extractClosedStructuralPredicateExprFrom
(ctx : Context)
(locals : List Binding)
(nextLocal : Nat)
(expr : Expr) :
Except String (Option (IRExpr × Nat)) := do
match closedStructuralPredicateShape? ctx.env expr with
| none => .ok none
| some shape =>
let layout ←
match recursiveVariantLayout? ctx.env shape.typeName shape.typeParams with
| some layout => .ok layout
| none => .error s!"unsupported closed structural predicate type: {shape.typeName}"
let stepInfo ←
structuralRecStepMatcher? ctx.env shape.typeName shape.typeParams 1 shape.step
if stepInfo.layout != layout then
.error s!"closed structural predicate matcher type mismatch: {shape.typeName}"
else if stepInfo.arms.length != layout.ctors.length then
.error s!"inductive matcher arity mismatch: {layout.name}"
else if stepInfo.prePostArgCount > 1 then
.error s!"unsupported closed structural predicate arguments: {shape.typeName}"
else
let ctorInfos :=
enumerate layout.ctors |>.map fun item =>
({
index := item.fst,
ctor := item.snd,
recursiveOffsets :=
directRecursiveFieldOffsets shape.typeName shape.typeParams item.snd.fields
} : ClosedFoldCtorInfo)
let continueInfos := ctorInfos.filter fun info => info.recursiveOffsets.length == 1
let terminalInfos := ctorInfos.filter fun info => info.recursiveOffsets.isEmpty
let continueInfo ←
match continueInfos with
| [info] => .ok info
| _ => .error s!"closed structural predicate requires one recursive constructor: {shape.typeName}"
if terminalInfos.length + 1 != ctorInfos.length then
.error s!"closed structural predicate requires list-shaped recursive constructors: {shape.typeName}"
else
let recursiveFieldOffset ←
match continueInfo.recursiveOffsets with
| [offset] => .ok offset
| _ => .error s!"closed structural predicate requires one recursive field: {shape.typeName}"
let scrutineeResult ← extractValueFrom ctx locals nextLocal shape.scrutinee
let ptrExpr ←
match heapVariantPtrWithLets? layout.name scrutineeResult.fst with
| some parts => .ok (wrapExprLets parts.fst parts.snd)
| none =>
match ← flattenInternalValue
(.recVariant shape.typeName shape.typeParams)
scrutineeResult.fst
ctx.freshResultOwnerOffsets with
| [ptr] => .ok ptr
| _ => .error s!"recursive predicate scrutinee shape mismatch: {shape.typeName}"
let fieldSlotCount := runtimeFieldSlotCount continueInfo.ctor.fields
let fieldStart := scrutineeResult.snd
let runtimeFields := localRuntimeFieldsFromKinds continueInfo.ctor.fields fieldStart
let sourceBindings ←
sourceFieldBindingsFromKinds layout.name continueInfo.ctor.fields runtimeFields
let fieldBinders :=
(continueInfo.ctor.fields.zip sourceBindings).map fun item =>
StructuralArmBinder.runtime item.fst item.snd
let postBinders := [StructuralArmBinder.staticLambda shape.predicate]
let belowBinding ←
structuralBelowBinding layout.name [] layout.name shape.typeParams
continueInfo.ctor.name continueInfo.ctor.fields runtimeFields
let continueArm ←
match stepInfo.arms[continueInfo.index]? with
| some arm => .ok arm
| none => .error s!"inductive matcher arity mismatch: {layout.name}"
let parsedContinue ←
consumeStructuralCtorArm ctx layout.name stepInfo.prePostArgCount postBinders fieldBinders
continueInfo.ctor belowBinding continueArm
let (predicateExpr, recExpr, stopWhenTrue, terminalValue) ←
match appFnArgs parsedContinue.fst with
| (.const ``Bool.or _, [predicateExpr, recExpr]) =>
.ok (predicateExpr, recExpr, true, false)
| (.const ``Bool.and _, [predicateExpr, recExpr]) =>
.ok (predicateExpr, recExpr, false, true)
| _ =>
.error s!"unsupported closed structural predicate step: {shape.typeName}"
let recCall ←
match ← structuralRecCallTarget? parsedContinue.snd recExpr with
| some recCall => .ok recCall
| none =>
.error
s!"closed structural predicate step must call the recursive field: {shape.typeName}"
if recCall.fst != layout.name then
.error s!"closed structural predicate recursive target mismatch: {shape.typeName}"
else
let recArg := recCall.snd.fst
let recCapturedArgs := recCall.snd.snd.fst
let recExtraArgs := recCall.snd.snd.snd
let recursiveFieldValue := valueFromInternalSlots
(.recVariant shape.typeName shape.typeParams)
(fun _ => .local (fieldStart + recursiveFieldOffset))
if recArg != recursiveFieldValue then
.error s!"closed structural predicate recursive field mismatch: {shape.typeName}"
else if !recCapturedArgs.isEmpty || !(recExtraArgs.all isDirectLambda) then
.error s!"closed structural predicate recursive argument mismatch: {shape.typeName}"
else
let predicateResult ←
extractExprFrom ctx (parsedContinue.snd ++ locals)
(fieldStart + fieldSlotCount) predicateExpr
let rec parseTerminalArms : List ClosedFoldCtorInfo → Except String Unit
| [] => .ok ()
| info :: rest => do
let arm ←
match stepInfo.arms[info.index]? with
| some arm => .ok arm
| none => .error s!"inductive matcher arity mismatch: {layout.name}"
let runtimeFields ← runtimeTypesFromKinds info.ctor.fields |>.mapM defaultValue
let sourceBindings ←
sourceFieldBindingsFromKinds layout.name info.ctor.fields runtimeFields
let fieldBinders :=
(info.ctor.fields.zip sourceBindings).map fun item =>
StructuralArmBinder.runtime item.fst item.snd
let belowBinding ←
structuralBelowBinding layout.name [] layout.name shape.typeParams
info.ctor.name info.ctor.fields runtimeFields
let parsedArm ←
consumeStructuralCtorArm ctx layout.name stepInfo.prePostArgCount postBinders
fieldBinders info.ctor belowBinding arm
let armResult ←
extractExprFrom ctx (parsedArm.snd ++ locals) predicateResult.snd parsedArm.fst
let expected := if terminalValue then .u64 1 else .u64 0
if armResult.fst == expected then
parseTerminalArms rest
else
.error
s!"closed structural predicate terminal arm mismatch: {shape.typeName}"
parseTerminalArms terminalInfos
.ok (some
(.heapLinearPredicate ptrExpr continueInfo.index fieldSlotCount recursiveFieldOffset
fieldStart predicateResult.fst stopWhenTrue terminalValue,
predicateResult.snd))
partial def extractForInStepBody
(ctx : Context)
(locals : List Binding)
(nextLocal : Nat)
(resultTy : Ty)
(body : Expr) :
Except String ExtractedForInStepBody := do
let resultWidth := internalSlots resultTy
match forInStepBody? resultTy body with
| .ok parsedStep =>
let bodyResult ← extractValueFrom ctx locals nextLocal parsedStep.value
let bodyTargets :=
(List.range resultWidth).map fun offset => bodyResult.snd + offset
let bodyLets ←
materializeInternalValueLets resultTy bodyResult.fst bodyTargets
ctx.freshResultOwnerOffsets
let doneResult ←
extractExprFrom ctx locals (bodyResult.snd + resultWidth) parsedStep.done
.ok {
bodyTargets := bodyTargets,
bodyValues := bodyTargets.map fun slot => (.local slot : IRExpr),
bodyLets := bodyLets,
bodyDone := doneResult.fst,
nextLocal := doneResult.snd
}
| .error _ =>
match body.consumeMData with
| .letE _ type value letBody _ =>
if !containsBVar 0 letBody then
match runtimeReleaseArgs? value with
| some args =>
let releaseResult ←
extractPrimitiveApplicationFrom ctx locals nextLocal
``LeanExe.Runtime.release args
let releaseSlot := releaseResult.snd
let step ←
extractForInStepBody ctx (.recursor :: locals) (releaseSlot + 1)
resultTy letBody
return { step with
bodyLets := .expr releaseSlot releaseResult.fst :: step.bodyLets
}
| none =>
return ← extractForInStepBody ctx (.recursor :: locals) nextLocal resultTy letBody
else if isStringType type then
return ← extractForInStepBody ctx (.thunk locals ctx.inlineStack value :: locals) nextLocal resultTy letBody
else
match value.consumeMData with
| .lam _ _ _ _ =>
return ← extractForInStepBody ctx locals nextLocal resultTy
(betaReduceLocalExpr 32 (letBody.instantiateRev #[value]))
| _ =>
match typeAtom? ctx.env type with
| some ty =>
if supportedLocalType ty then
let valueResult ← extractValueFrom ctx locals nextLocal value
let width := internalSlots ty
let targets := (List.range width).map fun offset => valueResult.snd + offset
let lets ←
materializeInternalValueLets ty valueResult.fst targets
ctx.freshResultOwnerOffsets
let localValue :=
valueFromInternalSlots ty (fun offset => .local (valueResult.snd + offset))
let step ←
extractForInStepBody ctx (.value localValue :: locals)
(valueResult.snd + width) resultTy letBody
return { step with bodyLets := lets ++ step.bodyLets }
else
.error s!"unsupported for-in step let-bound type: {type}"
| none => .error s!"unsupported for-in step let-bound type: {type}"
| _ =>
match appFnArgs body with
| (.const ``ite _, [_ty, condExpr, _, thenExpr, elseExpr]) =>
let condResult ← extractCondFrom ctx locals nextLocal condExpr
let thenStep ←
extractForInStepBody ctx locals condResult.snd resultTy thenExpr
let elseStep ←
extractForInStepBody ctx locals thenStep.nextLocal resultTy elseExpr
let bodyTargetStart := elseStep.nextLocal
let bodyTargets :=
(List.range resultWidth).map fun offset => bodyTargetStart + offset
let doneSlot := bodyTargetStart + resultWidth
let thenLets :=
thenStep.bodyLets ++
[.slots bodyTargets thenStep.bodyValues, .expr doneSlot thenStep.bodyDone]
let elseLets :=
elseStep.bodyLets ++
[.slots bodyTargets elseStep.bodyValues, .expr doneSlot elseStep.bodyDone]
return {
bodyTargets := bodyTargets,
bodyValues := bodyTargets.map fun slot => (.local slot : IRExpr),
bodyLets := [.branch condResult.fst thenLets elseLets],
bodyDone := .local doneSlot,
nextLocal := doneSlot + 1
}
| _ => pure ()
let stepTy : Ty := .variant ``ForInStep [resultTy] [[resultTy], [resultTy]]
let stepResult ←
match extractValueFrom ctx locals nextLocal body with
| .ok result => .ok result
| .error message =>
.error s!"unsupported for-in step value extraction: {message}; body: {body}"
let stepWidth := internalSlots stepTy
let stepTargets :=
(List.range stepWidth).map fun offset => stepResult.snd + offset
let stepLets ←
materializeInternalValueLets stepTy stepResult.fst stepTargets
ctx.freshResultOwnerOffsets
let tagSlot := stepResult.snd
let donePayloadStart := tagSlot + 1
let yieldPayloadStart := donePayloadStart + resultWidth
let doneValue :=
valueFromInternalSlots resultTy
(fun offset => .local (donePayloadStart + offset))
let yieldValue :=
valueFromInternalSlots resultTy
(fun offset => .local (yieldPayloadStart + offset))
let doneCond := .eqU64 (.local tagSlot) (.u64 0)
let selectedValue ← valueIte doneCond doneValue yieldValue
let bodyTargetStart := stepResult.snd + stepWidth
let bodyTargets :=
(List.range resultWidth).map fun offset => bodyTargetStart + offset
let bodyLets ←
materializeInternalValueLets resultTy selectedValue bodyTargets
ctx.freshResultOwnerOffsets
.ok {
bodyTargets := bodyTargets,
bodyValues := bodyTargets.map fun slot => (.local slot : IRExpr),
bodyLets := stepLets ++ bodyLets,
bodyDone := boolExpr doneCond,
nextLocal := bodyTargetStart + resultWidth
}
partial def monadPayloadResultType
(monad : SupportedMonad)
(payloadTy : Ty) :
Except String Ty :=
match monad with
| .option => .ok (.variant ``Option [payloadTy] [[], [payloadTy]])
| .except errorTy => .ok (.variant ``Except [errorTy, payloadTy] [[errorTy], [payloadTy]])
| .id => .error "Id foldlM is unsupported; use foldl"
partial def mkMonadPureValue
(monad : SupportedMonad)
(payload : ExtractedValue) :
Except String ExtractedValue := do
match monad with
| .option => .ok (mkOptionValue (.u64 1) payload)
| .except errorTy =>
.ok (mkExceptValue (.u64 1) (← defaultValue errorTy) payload)
| .id => .error "Id foldlM is unsupported; use foldl"
partial def monadFoldAccumulatorParts
(monad : SupportedMonad)
(value : ExtractedValue) :
Except String (IRExpr × ExtractedValue) := do
match monad with
| .option =>
let parts ← optionPartsWithLets value
.ok (wrapExprLets parts.fst parts.snd.fst,
wrapValueLets parts.fst parts.snd.snd)
| .except _ =>
let parts ← exceptPartsWithLets value
.ok (wrapExprLets parts.fst parts.snd.fst,
wrapValueLets parts.fst parts.snd.snd.snd)
| .id => .error "Id foldlM is unsupported; use foldl"
partial def extractMonadicForInStepBody
(ctx : Context)
(nextLocal : Nat)
(monad : SupportedMonad)
(payloadTy : Ty)
(accStart : Nat)
(bodyLocalPrefix : List Binding)
(bodyLocalSuffix : List Binding)
(bodyExpr : Expr) :
Except String ExtractedForInStepBody := do
let resultTy ← monadPayloadResultType monad payloadTy
let resultWidth := internalSlots resultTy
let accValue :=
valueFromInternalSlots resultTy (fun offset => .local (accStart + offset))
let accParts ← monadFoldAccumulatorParts monad accValue
let payload := accParts.snd
let stepTy : Ty := .variant ``ForInStep [payloadTy] [[payloadTy], [payloadTy]]
let bodyResult ←
extractValueFrom ctx
(bodyLocalPrefix ++ [.value payload] ++ bodyLocalSuffix)
nextLocal
bodyExpr
let stepWidth := internalSlots stepTy
let stepTargetStart := bodyResult.snd
let stepTargets :=
(List.range stepWidth).map fun offset => stepTargetStart + offset
let bodyTargetStart := stepTargetStart + stepWidth
let bodyTargets :=
(List.range resultWidth).map fun offset => bodyTargetStart + offset
let doneSlot := bodyTargetStart + resultWidth
let pairTy : Ty := .product resultTy .bool
let pairTargets := bodyTargets ++ [doneSlot]
let defaultPayload ← defaultValue payloadTy
let computedPair ←
match monad with
| .option =>
let parts ← optionPartsWithLets bodyResult.fst
let bodyTag := parts.snd.fst
let bodyFailed := .eqU64 bodyTag (.u64 0)
let rawStepParts ← variantPartsWithLets ``ForInStep parts.snd.snd
let rawStepDone :=
.eqU64 (wrapExprLets rawStepParts.fst rawStepParts.snd.fst) (.u64 0)
let stepLets ←
materializeInternalValueLets stepTy parts.snd.snd stepTargets
ctx.freshResultOwnerOffsets
let stepTag := .local stepTargetStart
let donePayloadStart := stepTargetStart + 1
let yieldPayloadStart := donePayloadStart + internalSlots payloadTy
let doneValue :=
valueFromInternalSlots payloadTy
(fun offset => .local (donePayloadStart + offset))
let yieldValue :=
valueFromInternalSlots payloadTy
(fun offset => .local (yieldPayloadStart + offset))
let stepDone :=
match condConst? rawStepDone with
| some true => .true
| some false => .false
| none => .eqU64 stepTag (.u64 0)
let selectedPayload ← valueIteConst stepDone doneValue yieldValue
let failedResult := mkOptionValue (.u64 0) defaultPayload
let okResult := mkOptionValue (.u64 1) selectedPayload
let nextValue ← valueIteConst bodyFailed failedResult okResult
let doneValue := boolExprConst (.or bodyFailed stepDone)
.ok
(wrapValueLets parts.fst
(wrapValueLocalLets stepLets
(.product nextValue (.scalar doneValue))))
| .except errorTy =>
let parts ← exceptPartsWithLets bodyResult.fst
let bodyTag := parts.snd.fst
let bodyFailed := .eqU64 bodyTag (.u64 0)
let errorPayload := parts.snd.snd.fst
let stepPayload := parts.snd.snd.snd
let rawStepParts ← variantPartsWithLets ``ForInStep stepPayload
let rawStepDone :=
.eqU64 (wrapExprLets rawStepParts.fst rawStepParts.snd.fst) (.u64 0)
let stepLets ←
materializeInternalValueLets stepTy stepPayload stepTargets
ctx.freshResultOwnerOffsets
let stepTag := .local stepTargetStart
let donePayloadStart := stepTargetStart + 1
let yieldPayloadStart := donePayloadStart + internalSlots payloadTy
let doneValue :=
valueFromInternalSlots payloadTy
(fun offset => .local (donePayloadStart + offset))
let yieldValue :=
valueFromInternalSlots payloadTy
(fun offset => .local (yieldPayloadStart + offset))
let stepDone :=
match condConst? rawStepDone with
| some true => .true
| some false => .false
| none => .eqU64 stepTag (.u64 0)
let selectedPayload ← valueIteConst stepDone doneValue yieldValue
let failedResult := mkExceptValue (.u64 0) errorPayload defaultPayload
let okResult :=
mkExceptValue (.u64 1) (← defaultValue errorTy) selectedPayload
let nextValue ← valueIteConst bodyFailed failedResult okResult
let doneValue := boolExprConst (.or bodyFailed stepDone)
.ok
(wrapValueLets parts.fst
(wrapValueLocalLets stepLets
(.product nextValue (.scalar doneValue))))
| .id => .error "Id for-in is handled by extractForInStepBody"
let bodyLets ←
materializeInternalValueLets pairTy computedPair pairTargets
ctx.freshResultOwnerOffsets
.ok {
bodyTargets := bodyTargets,
bodyValues := bodyTargets.map fun slot => (.local slot : IRExpr),
bodyLets := bodyLets,
bodyDone := .local doneSlot,
nextLocal := doneSlot + 1
}
partial def forInAccumulatorType
(monad : SupportedMonad)
(payloadTy : Ty) :
Except String Ty :=
match monad with
| .id => .ok payloadTy
| .option => monadPayloadResultType monad payloadTy
| .except _ => monadPayloadResultType monad payloadTy
partial def mkForInInitialAccumulatorValue
(monad : SupportedMonad)
(payload : ExtractedValue) :
Except String ExtractedValue :=
match monad with
| .id => .ok payload
| .option => mkMonadPureValue monad payload
| .except _ => mkMonadPureValue monad payload
partial def extractForInStepForMonad
(ctx : Context)
(nextLocal : Nat)
(monad : SupportedMonad)
(payloadTy : Ty)
(accStart : Nat)
(itemLocals : List Binding)
(bodyExpr : Expr) :
Except String ExtractedForInStepBody := do
let step ← match monad with
| .id =>
let accValue :=
valueFromInternalSlots payloadTy (fun offset => .local (accStart + offset))
extractForInStepBody ctx (.value accValue :: itemLocals) nextLocal payloadTy bodyExpr
| .option =>
extractMonadicForInStepBody ctx nextLocal monad payloadTy accStart []
itemLocals bodyExpr
| .except _ =>
extractMonadicForInStepBody ctx nextLocal monad payloadTy accStart []
itemLocals bodyExpr
let accumulatorTy ← forInAccumulatorType monad payloadTy
.ok (releaseForInStepTemporaries ctx accumulatorTy step)
partial def extractMonadicFoldStep
(ctx : Context)
(nextLocal : Nat)
(monad : SupportedMonad)
(resultTy : Ty)
(accStart : Nat)
(bodyLocalPrefix : List Binding)
(bodyLocalSuffix : List Binding)
(bodyExpr : Expr) :
Except String ExtractedForInStepBody := do
let resultWidth := internalSlots resultTy
let accValue :=
valueFromInternalSlots resultTy (fun offset => .local (accStart + offset))
let parts ← monadFoldAccumulatorParts monad accValue
let payload := parts.snd
let bodyResult ←
extractValueFrom ctx
(bodyLocalPrefix ++ [.value payload] ++ bodyLocalSuffix)
nextLocal
bodyExpr
let bodyTargets :=
(List.range resultWidth).map fun offset => bodyResult.snd + offset
let bodyLets ←
materializeInternalValueLets resultTy bodyResult.fst bodyTargets
ctx.freshResultOwnerOffsets
match bodyTargets with
| tagTarget :: _ =>
.ok {
bodyTargets := bodyTargets,
bodyValues := bodyTargets.map fun slot => (.local slot : IRExpr),
bodyLets := bodyLets,
bodyDone := boolExpr (.eqU64 (.local tagTarget) (.u64 0)),
nextLocal := bodyResult.snd + resultWidth
}
| [] => .error "monadic fold result has no tag slot"
partial def extractArrayFoldMValueFrom
(ctx : Context)
(locals : List Binding)
(nextLocal : Nat)
(args : List Expr) :
Except String (ExtractedValue × Nat) := do
match args with
| sourceTyExpr :: payloadTyExpr :: monadTyExpr :: _inst :: foldFn :: init :: array :: rest =>
let attached? := arrayAttachValue? ctx.env array
let sourceTy? :=
match attached? with
| some item => some item.fst
| none => typeAtom? ctx.env sourceTyExpr
match sourceTy?, typeAtom? ctx.env payloadTyExpr, supportedMonadType? ctx.env monadTyExpr with
| some sourceTy, some payloadTy, some monad =>
let resultTy ← monadPayloadResultType monad payloadTy
if !supportedLoopAccumulatorType resultTy then
.error s!"unsupported Array.foldlM result type: {reprStr resultTy}"
else
match arrayElementSlots? sourceTy with
| some sourceWidth =>
let arrayExpr :=
match attached? with
| some item => item.snd
| none => array
let arrayResult ← extractExprFrom ctx locals nextLocal arrayExpr
let initResult ← extractValueFrom ctx locals arrayResult.snd init
let initValue ← mkMonadPureValue monad initResult.fst
let startStop ←
match rest with
| [] => .ok ((.u64 0, .arraySize arrayResult.fst), initResult.snd)
| [start] =>
let startResult ← extractExprFrom ctx locals initResult.snd start
.ok ((startResult.fst, .arraySize arrayResult.fst), startResult.snd)
| [start, stop] =>
let startResult ← extractExprFrom ctx locals initResult.snd start
match attached?, arrayAttachSize? ctx.env stop with
| some _, some _ =>
.ok ((startResult.fst, .arraySize arrayResult.fst), startResult.snd)
| _, _ =>
let stopResult ← extractExprFrom ctx locals startResult.snd stop
.ok ((startResult.fst, stopResult.fst), stopResult.snd)
| _ => .error "unsupported Array.foldlM application"
let resultWidth := internalSlots resultTy
let initSlots ← flattenInternalValue resultTy initValue ctx.freshResultOwnerOffsets
if initSlots.length != resultWidth then
.error "Array.foldlM accumulator initial value shape mismatch"
else
let accStart := startStop.snd
let itemStart := accStart + resultWidth
let foldBody ←
match collectLambdas foldFn 2 with
| some body => .ok body
| none => .error "unsupported Array.foldlM function"
let itemValue ← arrayLocalValue sourceTy itemStart
let bodyExpr ←
match attached? with
| some _ =>
match arrayAttachUnwrapBody? ctx.env foldBody with
| some body => .ok body
| none => .error "unsupported Array.attach foldlM body"
| none => .ok foldBody
let step ←
match attached? with
| some _ =>
extractMonadicFoldStep ctx (itemStart + sourceWidth)
monad resultTy accStart
[.recursor, .value itemValue, .recursor]
locals
bodyExpr
| none =>
extractMonadicFoldStep ctx (itemStart + sourceWidth) monad
resultTy accStart [.value itemValue] locals bodyExpr
let releaseOffsets :=
foldAccumulatorReleaseOffsets ctx.freshResultOwnerOffsets resultTy
accStart step.bodyLets step.bodyDone step.bodyTargets
let resultValue :=
valueFromInternalSlots resultTy
(fun offset =>
.arrayFoldMultiSlot
sourceWidth
resultWidth
false
arrayResult.fst
startStop.fst.fst
startStop.fst.snd
initSlots
accStart
itemStart
step.bodyValues
step.bodyLets
step.bodyDone
releaseOffsets
offset)
.ok (resultValue, step.nextLocal)
| none => .error s!"unsupported Array.foldlM item type: {reprStr sourceTy}"
| _, _, _ => .error "unsupported Array.foldlM application"
| _ => .error "unsupported Array.foldlM application"
partial def extractArrayFoldValueFrom
(ctx : Context)
(locals : List Binding)
(nextLocal : Nat)
(reverse : Bool)
(args : List Expr) :
Except String (ExtractedValue × Nat) := do
let foldName := if reverse then "foldr" else "foldl"
match args with
| sourceTyExpr :: resultTyExpr :: foldFn :: init :: array :: rest =>
let attached? := arrayAttachValue? ctx.env array
let sourceTy? :=
match attached? with
| some item => some item.fst
| none => typeAtom? ctx.env sourceTyExpr
match sourceTy?, typeAtom? ctx.env resultTyExpr with
| some sourceTy, some resultTy =>
if !supportedLoopAccumulatorType resultTy then
.error s!"unsupported Array.{foldName} accumulator type: {reprStr resultTy}"
else
match arrayElementSlots? sourceTy with
| some sourceWidth =>
let arrayExpr :=
match attached? with
| some item => item.snd
| none => array
let arrayResult ← extractExprFrom ctx locals nextLocal arrayExpr
let (arrayIR, arrayBind?, afterArray) :=
match arrayResult.fst with
| .local index => ((.local index : IRExpr), none, arrayResult.snd)
| bound =>
((.local arrayResult.snd : IRExpr),
some (arrayResult.snd, bound),
arrayResult.snd + 1)
let initResult ← extractValueFrom ctx locals afterArray init
let arraySizeExpr : IRExpr := .arraySize arrayIR
let sameArraySize? (expr : Expr) : Bool :=
match appFnArgs expr with
| (.const ``Array.size _, sizeArgs) =>
match sizeArgs.reverse with
| sized :: _ => sized == arrayExpr
| _ => false
| _ => false
let extractArraySizeBound (next : Nat) (expr : Expr) :
Except String (IRExpr × Nat) :=
match attached?, arrayAttachSize? ctx.env expr with
| some _, some _ => .ok (arraySizeExpr, next)
| _, _ =>
if sameArraySize? expr then
.ok (arraySizeExpr, next)
else
extractExprFrom ctx locals next expr
let startStop ←
if reverse then
match rest with
| [] => .ok ((arraySizeExpr, .u64 0), initResult.snd)
| [start] =>
let startResult ← extractArraySizeBound initResult.snd start
.ok ((startResult.fst, .u64 0), startResult.snd)
| [start, stop] =>
let startResult ← extractArraySizeBound initResult.snd start
let stopResult ← extractExprFrom ctx locals startResult.snd stop
.ok ((startResult.fst, stopResult.fst), stopResult.snd)
| _ => .error s!"unsupported Array.{foldName} application"
else
match rest with
| [] => .ok ((.u64 0, arraySizeExpr), initResult.snd)
| [start] =>
let startResult ← extractExprFrom ctx locals initResult.snd start
.ok ((startResult.fst, arraySizeExpr), startResult.snd)
| [start, stop] =>
let startResult ← extractExprFrom ctx locals initResult.snd start
let stopResult ← extractArraySizeBound startResult.snd stop
.ok ((startResult.fst, stopResult.fst), stopResult.snd)
| _ => .error s!"unsupported Array.{foldName} application"
let resultWidth := internalSlots resultTy
let initSlots ←
flattenInternalValue resultTy initResult.fst ctx.freshResultOwnerOffsets
if initSlots.length != resultWidth then
.error s!"Array.{foldName} accumulator initial value shape mismatch"
else
let accStart := startStop.snd
let itemStart := accStart + resultWidth
let foldBody ←
match collectLambdas foldFn 2 with
| some body => .ok body
| none => .error s!"unsupported Array.{foldName} function"
let itemValue ← arrayLocalValue sourceTy itemStart
let accValue :=
valueFromInternalSlots resultTy
(fun offset => .local (accStart + offset))
let bodyExpr ←
match attached?, reverse with
| some _, true => .error "unsupported Array.attach foldr body"
| some _, false =>
match arrayAttachUnwrapBody? ctx.env foldBody with
| some body => .ok body
| none => .error s!"unsupported Array.attach {foldName} body"
| none, _ => .ok foldBody
let bodyLocals :=
match attached? with
| some _ =>
.recursor :: .value itemValue :: .recursor ::
.value accValue :: locals
| none =>
if reverse then
.value accValue :: .value itemValue :: locals
else
.value itemValue :: .value accValue :: locals
let bodyResult ←
extractValueFrom ctx bodyLocals (itemStart + sourceWidth) bodyExpr
let bodyTargets :=
(List.range resultWidth).map fun offset => bodyResult.snd + offset
let bodyLets ←
materializeInternalValueLets resultTy bodyResult.fst bodyTargets
ctx.freshResultOwnerOffsets
if bodyTargets.length != resultWidth then
.error s!"Array.{foldName} accumulator body value shape mismatch"
else
let releaseOffsets :=
foldAccumulatorReleaseOffsets ctx.freshResultOwnerOffsets resultTy
accStart bodyLets (.u64 0) bodyTargets
let resultValue :=
valueFromInternalSlots resultTy
(fun offset =>
let fold : IRExpr :=
.arrayFoldMultiSlot
sourceWidth
resultWidth
reverse
arrayIR
startStop.fst.fst
startStop.fst.snd
initSlots
accStart
itemStart
(bodyTargets.map fun slot => (.local slot : IRExpr))
bodyLets
(.u64 0)
releaseOffsets
offset
match arrayBind? with
| some (slot, bound) => .letE slot bound fold
| none => fold)
.ok (resultValue, bodyResult.snd + resultWidth)
| none => .error s!"unsupported Array.{foldName} item type: {reprStr sourceTy}"
| _, _ => .error s!"unsupported Array.{foldName} application"
| _ => .error s!"unsupported Array.{foldName} application"
partial def extractByteArrayFoldMValueFrom
(ctx : Context)
(locals : List Binding)
(nextLocal : Nat)
(args : List Expr) :
Except String (ExtractedValue × Nat) := do
match args with
| payloadTyExpr :: monadTyExpr :: _inst :: foldFn :: init :: array :: rest =>
match typeAtom? ctx.env payloadTyExpr, supportedMonadType? ctx.env monadTyExpr with
| some payloadTy, some monad =>
let resultTy ← monadPayloadResultType monad payloadTy
if !supportedLoopAccumulatorType resultTy then
.error s!"unsupported ByteArray.foldlM result type: {reprStr resultTy}"
else
let arrayResult ← extractValueFrom ctx locals nextLocal array
let parts ← byteArrayPartsWithLets arrayResult.fst
let ptr := parts.snd.fst
let len := parts.snd.snd
let initResult ← extractValueFrom ctx locals arrayResult.snd init
let initValue ← mkMonadPureValue monad initResult.fst
let sameByteSize? (expr : Expr) : Bool :=
match appFnArgs expr with
| (.const ``ByteArray.size _, sizeArgs) =>
match sizeArgs.reverse with
| sized :: _ => sized == array
| _ => false
| _ => false
let startStop ←
match rest with
| [] => .ok ((.u64 0, len), initResult.snd)
| [start] =>
let startResult ← extractExprFrom ctx locals initResult.snd start
.ok ((startResult.fst, len), startResult.snd)
| [start, stop] =>
let startResult ← extractExprFrom ctx locals initResult.snd start
if sameByteSize? stop then
.ok ((startResult.fst, len), startResult.snd)
else