Skip to content

Commit af91015

Browse files
committed
fix(metatheory): add LinearInXAndY constructor to RawModel
Add missing LinearInXAndY constructor to the Agda RawModel type and regenerate MAlonzo Haskell code. This constructor was added to the Haskell Model type but was missing from the Agda source, causing incomplete pattern match warnings during compilation. The LinearInXAndY model is used for valueContains costing as part of the const_above_diagonal approach.
1 parent c1204f8 commit af91015

File tree

6 files changed

+80
-74
lines changed

6 files changed

+80
-74
lines changed

plutus-metatheory/src/Cost/Raw.lagda.md

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -140,6 +140,7 @@ data RawModel : Set where
140140
LinearInU : LinearFunction → RawModel
141141
LiteralInYOrLinearInZ : LinearFunction → RawModel
142142
LinearInMaxYZ : LinearFunction → RawModel
143+
LinearInXAndY : TwoVariableLinearFunction → RawModel
143144
LinearInYAndZ : TwoVariableLinearFunction -> RawModel
144145
QuadraticInY : OneVariableQuadraticFunction → RawModel
145146
QuadraticInZ : OneVariableQuadraticFunction → RawModel
@@ -153,10 +154,10 @@ data RawModel : Set where
153154
154155
{-# COMPILE GHC RawModel = data Model (ConstantCost | AddedSizes |
155156
MultipliedSizes | MinSize | MaxSize | LinearInX | LinearInY | LinearInZ |
156-
LinearInU | LiteralInYOrLinearInZ | LinearInMaxYZ | LinearInYAndZ |
157-
QuadraticInY | QuadraticInZ | QuadraticInXAndY | WithInteractionInXAndY |
158-
SubtractedSizes | ConstAboveDiagonal | ConstBelowDiagonal |
159-
ConstOffDiagonal | ExpModCost) #-}
157+
LinearInU | LiteralInYOrLinearInZ | LinearInMaxYZ | LinearInXAndY |
158+
LinearInYAndZ | QuadraticInY | QuadraticInZ | QuadraticInXAndY |
159+
WithInteractionInXAndY | SubtractedSizes | ConstAboveDiagonal |
160+
ConstBelowDiagonal | ConstOffDiagonal | ExpModCost) #-}
160161
161162
record CpuAndMemoryModel : Set where
162163
constructor mkCpuAndMemoryModel

plutus-metatheory/src/MAlonzo/Code/Cost/Model.hs

Lines changed: 13 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -667,7 +667,7 @@ d_convertRawModel_292 v0 v1
667667
2 -> coe v2
668668
1 -> coe v2
669669
_ -> coe v2
670-
MAlonzo.Code.Cost.Raw.C_LinearInYAndZ_168 v3
670+
MAlonzo.Code.Cost.Raw.C_LinearInYAndZ_170 v3
671671
-> case coe v0 of
672672
3 -> case coe v3 of
673673
MAlonzo.Code.Cost.Raw.C_mkTwoVariableLinearFunction_74 v4 v5 v6
@@ -679,7 +679,7 @@ d_convertRawModel_292 v0 v1
679679
2 -> coe v2
680680
1 -> coe v2
681681
_ -> coe v2
682-
MAlonzo.Code.Cost.Raw.C_QuadraticInY_170 v3
682+
MAlonzo.Code.Cost.Raw.C_QuadraticInY_172 v3
683683
-> case coe v0 of
684684
_ | coe geqInt (coe v0) (coe (2 :: Integer)) ->
685685
case coe v3 of
@@ -695,7 +695,7 @@ d_convertRawModel_292 v0 v1
695695
_ -> MAlonzo.RTE.mazUnreachableError
696696
1 -> coe v2
697697
_ -> coe v2
698-
MAlonzo.Code.Cost.Raw.C_QuadraticInZ_172 v3
698+
MAlonzo.Code.Cost.Raw.C_QuadraticInZ_174 v3
699699
-> case coe v0 of
700700
_ | coe geqInt (coe v0) (coe (3 :: Integer)) ->
701701
case coe v3 of
@@ -714,7 +714,7 @@ d_convertRawModel_292 v0 v1
714714
2 -> coe v2
715715
1 -> coe v2
716716
_ -> coe v2
717-
MAlonzo.Code.Cost.Raw.C_QuadraticInXAndY_174 v3
717+
MAlonzo.Code.Cost.Raw.C_QuadraticInXAndY_176 v3
718718
-> case coe v0 of
719719
_ | coe geqInt (coe v0) (coe (2 :: Integer)) ->
720720
case coe v3 of
@@ -730,7 +730,7 @@ d_convertRawModel_292 v0 v1
730730
_ -> MAlonzo.RTE.mazUnreachableError
731731
1 -> coe v2
732732
_ -> coe v2
733-
MAlonzo.Code.Cost.Raw.C_SubtractedSizes_178 v3 v4
733+
MAlonzo.Code.Cost.Raw.C_SubtractedSizes_180 v3 v4
734734
-> case coe v0 of
735735
2 -> case coe v3 of
736736
MAlonzo.Code.Cost.Raw.C_mkLinearFunction_42 v5 v6
@@ -741,7 +741,7 @@ d_convertRawModel_292 v0 v1
741741
_ | coe geqInt (coe v0) (coe (2 :: Integer)) -> coe v2
742742
1 -> coe v2
743743
_ -> coe v2
744-
MAlonzo.Code.Cost.Raw.C_ConstAboveDiagonal_180 v3 v4
744+
MAlonzo.Code.Cost.Raw.C_ConstAboveDiagonal_182 v3 v4
745745
-> case coe v0 of
746746
2 -> coe
747747
MAlonzo.Code.Data.Maybe.Base.du_map_64
@@ -750,7 +750,7 @@ d_convertRawModel_292 v0 v1
750750
_ | coe geqInt (coe v0) (coe (2 :: Integer)) -> coe v2
751751
1 -> coe v2
752752
_ -> coe v2
753-
MAlonzo.Code.Cost.Raw.C_ConstBelowDiagonal_182 v3 v4
753+
MAlonzo.Code.Cost.Raw.C_ConstBelowDiagonal_184 v3 v4
754754
-> case coe v0 of
755755
2 -> coe
756756
MAlonzo.Code.Data.Maybe.Base.du_map_64
@@ -759,7 +759,7 @@ d_convertRawModel_292 v0 v1
759759
_ | coe geqInt (coe v0) (coe (2 :: Integer)) -> coe v2
760760
1 -> coe v2
761761
_ -> coe v2
762-
MAlonzo.Code.Cost.Raw.C_ConstOffDiagonal_184 v3 v4
762+
MAlonzo.Code.Cost.Raw.C_ConstOffDiagonal_186 v3 v4
763763
-> case coe v0 of
764764
2 -> coe
765765
MAlonzo.Code.Data.Maybe.Base.du_map_64
@@ -768,7 +768,7 @@ d_convertRawModel_292 v0 v1
768768
_ | coe geqInt (coe v0) (coe (2 :: Integer)) -> coe v2
769769
1 -> coe v2
770770
_ -> coe v2
771-
MAlonzo.Code.Cost.Raw.C_ExpModCost_186 v3
771+
MAlonzo.Code.Cost.Raw.C_ExpModCost_188 v3
772772
-> case coe v0 of
773773
3 -> case coe v3 of
774774
MAlonzo.Code.Cost.Raw.C_mkExpModCostingFunction_142 v4 v5 v6
@@ -784,11 +784,11 @@ d_convertRawModel_292 v0 v1
784784
-- Cost.Model.convertCpuAndMemoryModel
785785
d_convertCpuAndMemoryModel_408 ::
786786
Integer ->
787-
MAlonzo.Code.Cost.Raw.T_CpuAndMemoryModel_188 ->
787+
MAlonzo.Code.Cost.Raw.T_CpuAndMemoryModel_190 ->
788788
Maybe T_BuiltinModel_62
789789
d_convertCpuAndMemoryModel_408 v0 v1
790790
= case coe v1 of
791-
MAlonzo.Code.Cost.Raw.C_mkCpuAndMemoryModel_198 v2 v3
791+
MAlonzo.Code.Cost.Raw.C_mkCpuAndMemoryModel_200 v2 v3
792792
-> let v4 = d_convertRawModel_292 (coe v0) (coe v2) in
793793
coe
794794
(let v5 = d_convertRawModel_292 (coe v0) (coe v3) in
@@ -809,7 +809,7 @@ d_getModel_432 ::
809809
MAlonzo.Code.Utils.T_List_384
810810
(MAlonzo.Code.Utils.T__'215'__366
811811
MAlonzo.Code.Agda.Builtin.String.T_String_6
812-
MAlonzo.Code.Cost.Raw.T_CpuAndMemoryModel_188) ->
812+
MAlonzo.Code.Cost.Raw.T_CpuAndMemoryModel_190) ->
813813
Maybe MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
814814
d_getModel_432 v0 v1
815815
= case coe v1 of
@@ -919,7 +919,7 @@ d_createMap_536 ::
919919
MAlonzo.Code.Utils.T_List_384
920920
(MAlonzo.Code.Utils.T__'215'__366
921921
MAlonzo.Code.Agda.Builtin.String.T_String_6
922-
MAlonzo.Code.Cost.Raw.T_CpuAndMemoryModel_188) ->
922+
MAlonzo.Code.Cost.Raw.T_CpuAndMemoryModel_190) ->
923923
Maybe (MAlonzo.Code.Builtin.T_Builtin_2 -> T_BuiltinModel_62)
924924
d_createMap_536 v0
925925
= coe

plutus-metatheory/src/MAlonzo/Code/Cost/Raw.hs

Lines changed: 53 additions & 48 deletions
Original file line numberDiff line numberDiff line change
@@ -305,16 +305,17 @@ pattern C_LinearInZ_160 a0 = LinearInZ a0
305305
pattern C_LinearInU_162 a0 = LinearInU a0
306306
pattern C_LiteralInYOrLinearInZ_164 a0 = LiteralInYOrLinearInZ a0
307307
pattern C_LinearInMaxYZ_166 a0 = LinearInMaxYZ a0
308-
pattern C_LinearInYAndZ_168 a0 = LinearInYAndZ a0
309-
pattern C_QuadraticInY_170 a0 = QuadraticInY a0
310-
pattern C_QuadraticInZ_172 a0 = QuadraticInZ a0
311-
pattern C_QuadraticInXAndY_174 a0 = QuadraticInXAndY a0
312-
pattern C_WithInteractionInXAndY_176 a0 = WithInteractionInXAndY a0
313-
pattern C_SubtractedSizes_178 a0 a1 = SubtractedSizes a0 a1
314-
pattern C_ConstAboveDiagonal_180 a0 a1 = ConstAboveDiagonal a0 a1
315-
pattern C_ConstBelowDiagonal_182 a0 a1 = ConstBelowDiagonal a0 a1
316-
pattern C_ConstOffDiagonal_184 a0 a1 = ConstOffDiagonal a0 a1
317-
pattern C_ExpModCost_186 a0 = ExpModCost a0
308+
pattern C_LinearInXAndY_168 a0 = LinearInXAndY a0
309+
pattern C_LinearInYAndZ_170 a0 = LinearInYAndZ a0
310+
pattern C_QuadraticInY_172 a0 = QuadraticInY a0
311+
pattern C_QuadraticInZ_174 a0 = QuadraticInZ a0
312+
pattern C_QuadraticInXAndY_176 a0 = QuadraticInXAndY a0
313+
pattern C_WithInteractionInXAndY_178 a0 = WithInteractionInXAndY a0
314+
pattern C_SubtractedSizes_180 a0 a1 = SubtractedSizes a0 a1
315+
pattern C_ConstAboveDiagonal_182 a0 a1 = ConstAboveDiagonal a0 a1
316+
pattern C_ConstBelowDiagonal_184 a0 a1 = ConstBelowDiagonal a0 a1
317+
pattern C_ConstOffDiagonal_186 a0 a1 = ConstOffDiagonal a0 a1
318+
pattern C_ExpModCost_188 a0 = ExpModCost a0
318319
check_ConstantCost_146 :: Integer -> T_RawModel_144
319320
check_ConstantCost_146 = ConstantCost
320321
check_AddedSizes_148 :: T_LinearFunction_32 -> T_RawModel_144
@@ -338,36 +339,39 @@ check_LiteralInYOrLinearInZ_164 ::
338339
check_LiteralInYOrLinearInZ_164 = LiteralInYOrLinearInZ
339340
check_LinearInMaxYZ_166 :: T_LinearFunction_32 -> T_RawModel_144
340341
check_LinearInMaxYZ_166 = LinearInMaxYZ
341-
check_LinearInYAndZ_168 ::
342+
check_LinearInXAndY_168 ::
342343
T_TwoVariableLinearFunction_60 -> T_RawModel_144
343-
check_LinearInYAndZ_168 = LinearInYAndZ
344-
check_QuadraticInY_170 ::
344+
check_LinearInXAndY_168 = LinearInXAndY
345+
check_LinearInYAndZ_170 ::
346+
T_TwoVariableLinearFunction_60 -> T_RawModel_144
347+
check_LinearInYAndZ_170 = LinearInYAndZ
348+
check_QuadraticInY_172 ::
345349
T_OneVariableQuadraticFunction_44 -> T_RawModel_144
346-
check_QuadraticInY_170 = QuadraticInY
347-
check_QuadraticInZ_172 ::
350+
check_QuadraticInY_172 = QuadraticInY
351+
check_QuadraticInZ_174 ::
348352
T_OneVariableQuadraticFunction_44 -> T_RawModel_144
349-
check_QuadraticInZ_172 = QuadraticInZ
350-
check_QuadraticInXAndY_174 ::
353+
check_QuadraticInZ_174 = QuadraticInZ
354+
check_QuadraticInXAndY_176 ::
351355
T_TwoVariableQuadraticFunction_76 -> T_RawModel_144
352-
check_QuadraticInXAndY_174 = QuadraticInXAndY
353-
check_WithInteractionInXAndY_176 ::
356+
check_QuadraticInXAndY_176 = QuadraticInXAndY
357+
check_WithInteractionInXAndY_178 ::
354358
T_TwoVariableWithInteractionFunction_108 -> T_RawModel_144
355-
check_WithInteractionInXAndY_176 = WithInteractionInXAndY
356-
check_SubtractedSizes_178 ::
359+
check_WithInteractionInXAndY_178 = WithInteractionInXAndY
360+
check_SubtractedSizes_180 ::
357361
T_LinearFunction_32 -> Integer -> T_RawModel_144
358-
check_SubtractedSizes_178 = SubtractedSizes
359-
check_ConstAboveDiagonal_180 ::
362+
check_SubtractedSizes_180 = SubtractedSizes
363+
check_ConstAboveDiagonal_182 ::
360364
Integer -> T_RawModel_144 -> T_RawModel_144
361-
check_ConstAboveDiagonal_180 = ConstAboveDiagonal
362-
check_ConstBelowDiagonal_182 ::
365+
check_ConstAboveDiagonal_182 = ConstAboveDiagonal
366+
check_ConstBelowDiagonal_184 ::
363367
Integer -> T_RawModel_144 -> T_RawModel_144
364-
check_ConstBelowDiagonal_182 = ConstBelowDiagonal
365-
check_ConstOffDiagonal_184 ::
368+
check_ConstBelowDiagonal_184 = ConstBelowDiagonal
369+
check_ConstOffDiagonal_186 ::
366370
Integer -> T_RawModel_144 -> T_RawModel_144
367-
check_ConstOffDiagonal_184 = ConstOffDiagonal
368-
check_ExpModCost_186 ::
371+
check_ConstOffDiagonal_186 = ConstOffDiagonal
372+
check_ExpModCost_188 ::
369373
T_ExpModCostingFunction_128 -> T_RawModel_144
370-
check_ExpModCost_186 = ExpModCost
374+
check_ExpModCost_188 = ExpModCost
371375
cover_RawModel_144 :: Model -> ()
372376
cover_RawModel_144 x
373377
= case x of
@@ -382,6 +386,7 @@ cover_RawModel_144 x
382386
LinearInU _ -> ()
383387
LiteralInYOrLinearInZ _ -> ()
384388
LinearInMaxYZ _ -> ()
389+
LinearInXAndY _ -> ()
385390
LinearInYAndZ _ -> ()
386391
QuadraticInY _ -> ()
387392
QuadraticInZ _ -> ()
@@ -393,31 +398,31 @@ cover_RawModel_144 x
393398
ConstOffDiagonal _ _ -> ()
394399
ExpModCost _ -> ()
395400
-- Cost.Raw.CpuAndMemoryModel
396-
d_CpuAndMemoryModel_188 = ()
397-
type T_CpuAndMemoryModel_188 = CpuAndMemoryModel
398-
pattern C_mkCpuAndMemoryModel_198 a0 a1 = CpuAndMemoryModel a0 a1
399-
check_mkCpuAndMemoryModel_198 ::
400-
T_RawModel_144 -> T_RawModel_144 -> T_CpuAndMemoryModel_188
401-
check_mkCpuAndMemoryModel_198 = CpuAndMemoryModel
402-
cover_CpuAndMemoryModel_188 :: CpuAndMemoryModel -> ()
403-
cover_CpuAndMemoryModel_188 x
401+
d_CpuAndMemoryModel_190 = ()
402+
type T_CpuAndMemoryModel_190 = CpuAndMemoryModel
403+
pattern C_mkCpuAndMemoryModel_200 a0 a1 = CpuAndMemoryModel a0 a1
404+
check_mkCpuAndMemoryModel_200 ::
405+
T_RawModel_144 -> T_RawModel_144 -> T_CpuAndMemoryModel_190
406+
check_mkCpuAndMemoryModel_200 = CpuAndMemoryModel
407+
cover_CpuAndMemoryModel_190 :: CpuAndMemoryModel -> ()
408+
cover_CpuAndMemoryModel_190 x
404409
= case x of
405410
CpuAndMemoryModel _ _ -> ()
406411
-- Cost.Raw.CpuAndMemoryModel.cpuModel
407-
d_cpuModel_194 :: T_CpuAndMemoryModel_188 -> T_RawModel_144
408-
d_cpuModel_194 v0
412+
d_cpuModel_196 :: T_CpuAndMemoryModel_190 -> T_RawModel_144
413+
d_cpuModel_196 v0
409414
= case coe v0 of
410-
C_mkCpuAndMemoryModel_198 v1 v2 -> coe v1
415+
C_mkCpuAndMemoryModel_200 v1 v2 -> coe v1
411416
_ -> MAlonzo.RTE.mazUnreachableError
412417
-- Cost.Raw.CpuAndMemoryModel.memoryModel
413-
d_memoryModel_196 :: T_CpuAndMemoryModel_188 -> T_RawModel_144
414-
d_memoryModel_196 v0
418+
d_memoryModel_198 :: T_CpuAndMemoryModel_190 -> T_RawModel_144
419+
d_memoryModel_198 v0
415420
= case coe v0 of
416-
C_mkCpuAndMemoryModel_198 v1 v2 -> coe v2
421+
C_mkCpuAndMemoryModel_200 v1 v2 -> coe v2
417422
_ -> MAlonzo.RTE.mazUnreachableError
418423
-- Cost.Raw.BuiltinCostMap
419-
d_BuiltinCostMap_200 :: ()
420-
d_BuiltinCostMap_200 = erased
424+
d_BuiltinCostMap_202 :: ()
425+
d_BuiltinCostMap_202 = erased
421426
-- Cost.Raw.RawCostModel
422-
d_RawCostModel_202 :: ()
423-
d_RawCostModel_202 = erased
427+
d_RawCostModel_204 :: ()
428+
d_RawCostModel_204 = erased

plutus-metatheory/src/MAlonzo/Code/Evaluator/Program.hs

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -532,7 +532,7 @@ d_executeUPLCwithMP_144 ::
532532
(MAlonzo.Code.Utils.T_List_384
533533
(MAlonzo.Code.Utils.T__'215'__366
534534
MAlonzo.Code.Agda.Builtin.String.T_String_6
535-
MAlonzo.Code.Cost.Raw.T_CpuAndMemoryModel_188)) ->
535+
MAlonzo.Code.Cost.Raw.T_CpuAndMemoryModel_190)) ->
536536
(MAlonzo.Code.Utils.T__'215'__366
537537
MAlonzo.Code.Cost.Raw.T_HCekMachineCosts_4
538538
(MAlonzo.Code.Builtin.T_Builtin_2 ->
@@ -551,7 +551,7 @@ du_executeUPLCwithMP_144 ::
551551
(MAlonzo.Code.Utils.T_List_384
552552
(MAlonzo.Code.Utils.T__'215'__366
553553
MAlonzo.Code.Agda.Builtin.String.T_String_6
554-
MAlonzo.Code.Cost.Raw.T_CpuAndMemoryModel_188)) ->
554+
MAlonzo.Code.Cost.Raw.T_CpuAndMemoryModel_190)) ->
555555
(MAlonzo.Code.Utils.T__'215'__366
556556
MAlonzo.Code.Cost.Raw.T_HCekMachineCosts_4
557557
(MAlonzo.Code.Builtin.T_Builtin_2 ->
@@ -1013,7 +1013,7 @@ d_executeUPLC_192 ::
10131013
(MAlonzo.Code.Utils.T_List_384
10141014
(MAlonzo.Code.Utils.T__'215'__366
10151015
MAlonzo.Code.Agda.Builtin.String.T_String_6
1016-
MAlonzo.Code.Cost.Raw.T_CpuAndMemoryModel_188))) ->
1016+
MAlonzo.Code.Cost.Raw.T_CpuAndMemoryModel_190))) ->
10171017
MAlonzo.Code.Untyped.T__'8866'_14 ->
10181018
MAlonzo.Code.Utils.T_Either_6
10191019
MAlonzo.Code.Evaluator.Base.T_ERROR_12
@@ -1053,7 +1053,7 @@ d_evalProgramNU_204 ::
10531053
(MAlonzo.Code.Utils.T_List_384
10541054
(MAlonzo.Code.Utils.T__'215'__366
10551055
MAlonzo.Code.Agda.Builtin.String.T_String_6
1056-
MAlonzo.Code.Cost.Raw.T_CpuAndMemoryModel_188))) ->
1056+
MAlonzo.Code.Cost.Raw.T_CpuAndMemoryModel_190))) ->
10571057
T_ProgramNU_26 ->
10581058
MAlonzo.Code.Utils.T_Either_6
10591059
MAlonzo.Code.Evaluator.Base.T_ERROR_12

plutus-metatheory/src/MAlonzo/Code/Evaluator/Term.hs

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -881,7 +881,7 @@ runUCountingAgda ::
881881
(MAlonzo.Code.Utils.T_List_384
882882
(MAlonzo.Code.Utils.T__'215'__366
883883
MAlonzo.Code.Agda.Builtin.String.T_String_6
884-
MAlonzo.Code.Cost.Raw.T_CpuAndMemoryModel_188)) ->
884+
MAlonzo.Code.Cost.Raw.T_CpuAndMemoryModel_190)) ->
885885
T_TermU_24 ->
886886
MAlonzo.Code.Utils.T_Either_6
887887
MAlonzo.Code.Evaluator.Base.T_ERROR_12
@@ -894,7 +894,7 @@ d_runUCounting_202 ::
894894
(MAlonzo.Code.Utils.T_List_384
895895
(MAlonzo.Code.Utils.T__'215'__366
896896
MAlonzo.Code.Agda.Builtin.String.T_String_6
897-
MAlonzo.Code.Cost.Raw.T_CpuAndMemoryModel_188)) ->
897+
MAlonzo.Code.Cost.Raw.T_CpuAndMemoryModel_190)) ->
898898
T_TermU_24 ->
899899
MAlonzo.Code.Utils.T_Either_6
900900
MAlonzo.Code.Evaluator.Base.T_ERROR_12

plutus-metatheory/src/MAlonzo/Code/Main.hs

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -114,7 +114,7 @@ d_execP_44 ::
114114
(MAlonzo.Code.Utils.T_List_384
115115
(MAlonzo.Code.Utils.T__'215'__366
116116
MAlonzo.Code.Agda.Builtin.String.T_String_6
117-
MAlonzo.Code.Cost.Raw.T_CpuAndMemoryModel_188))))
117+
MAlonzo.Code.Cost.Raw.T_CpuAndMemoryModel_190))))
118118
d_execP_44 = execP
119119
-- Main.parse
120120
d_parse_46 ::
@@ -139,7 +139,7 @@ d_evalInput_50 ::
139139
(MAlonzo.Code.Utils.T_List_384
140140
(MAlonzo.Code.Utils.T__'215'__366
141141
MAlonzo.Code.Agda.Builtin.String.T_String_6
142-
MAlonzo.Code.Cost.Raw.T_CpuAndMemoryModel_188))) ->
142+
MAlonzo.Code.Cost.Raw.T_CpuAndMemoryModel_190))) ->
143143
MAlonzo.Code.Evaluator.Program.T_Format_14 ->
144144
MAlonzo.Code.Evaluator.Program.T_Input_16 ->
145145
MAlonzo.Code.Agda.Builtin.IO.T_IO_8
@@ -183,7 +183,7 @@ d_main''_70 ::
183183
(MAlonzo.Code.Utils.T_List_384
184184
(MAlonzo.Code.Utils.T__'215'__366
185185
MAlonzo.Code.Agda.Builtin.String.T_String_6
186-
MAlonzo.Code.Cost.Raw.T_CpuAndMemoryModel_188))) ->
186+
MAlonzo.Code.Cost.Raw.T_CpuAndMemoryModel_190))) ->
187187
MAlonzo.Code.Agda.Builtin.IO.T_IO_8
188188
AgdaAny MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6
189189
d_main''_70 v0

0 commit comments

Comments
 (0)