-
Notifications
You must be signed in to change notification settings - Fork 0
/
LedgerTypes.hs
1444 lines (1427 loc) · 50 KB
/
LedgerTypes.hs
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
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# OPTIONS_GHC -Wno-overlapping-patterns #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE EmptyDataDeriving #-}
module MAlonzo.Code.Ledger.Foreign.LedgerTypes where
import MAlonzo.RTE (coe, erased, AgdaAny, addInt, subInt, mulInt,
quotInt, remInt, geqInt, ltInt, eqInt, add64, sub64, mul64, quot64,
rem64, lt64, eq64, word64FromNat, word64ToNat)
import qualified MAlonzo.RTE
import qualified Data.Text
import qualified MAlonzo.Code.Agda.Builtin.List
import qualified MAlonzo.Code.Agda.Builtin.Maybe
import qualified MAlonzo.Code.Agda.Builtin.Unit
import qualified MAlonzo.Code.Foreign.Haskell.Either
import qualified MAlonzo.Code.Foreign.Haskell.Pair
import GHC.Generics (Generic)
import Data.TreeDiff
import Prelude hiding (Rational)
data AgdaEmpty deriving (Show, Generic)
data ComputationResult e a = Success a | Failure e
deriving (Functor, Eq, Show, Generic)
instance Applicative (ComputationResult e) where
pure = Success
(Success f) <*> x = f <$> x
(Failure e) <*> _ = Failure e
instance Monad (ComputationResult e) where
return = pure
(Success a) >>= m = m a
(Failure e) >>= _ = Failure e
type Rational = (Integer, Integer)
type Coin = Integer
type Addr = Integer
newtype TxId = MkTxId Integer
deriving (Generic, Show, Eq, Ord)
type Ix = Integer
type Epoch = Integer
type ScriptHash = Integer
type PParamsUpdate = Integer
type AuxiliaryData = ()
type DataHash = ()
type Datum = ()
type Redeemer = ()
type Anchor = ()
type Network = ()
type Script = ()
type TxIn = (TxId, Ix)
type TxOut = (Addr, (Coin, (Maybe (Either Datum DataHash), Maybe Script)))
type UTxO = [(TxIn, TxOut)]
type Hash = Integer
data Tag = Spend | Mint | Cert | Rewrd | Vote | Propose deriving (Show, Generic)
type RdmrPtr = (Tag, Ix)
type ExUnits = (Integer, Integer)
type ProtVer = (Integer, Integer)
type GovActionID = (TxId, Integer)
data Credential
= ScriptObj Integer
| KeyHashObj Integer
deriving (Show, Eq, Generic)
type PoolParams = Credential
type RwdAddr = (Network, Credential)
data GovRole
= CC
| DRep
| SPO
deriving (Show, Eq, Generic)
data VDeleg
= CredVoter GovRole Credential
| AbstainRep
| NoConfidenceRep
deriving (Show, Eq, Generic)
data TxCert
= Delegate Credential (Maybe VDeleg) (Maybe Credential) Coin
| Dereg Credential
| RegPool Credential PoolParams
| RetirePool Credential Epoch
| RegDRep Credential Coin Anchor
| DeRegDRep Credential
| CCRegHot Credential (Maybe Credential)
deriving (Show, Eq, Generic)
data TxBody = MkTxBody
{ txins :: [TxIn]
, refInputs :: [TxIn]
, txouts :: [(Ix, TxOut)]
, txfee :: Coin
, txvldt :: (Maybe Integer, Maybe Integer)
, txsize :: Integer
, txid :: TxId
, collateral :: [TxIn]
, reqSigHash :: [Hash]
, scriptIntHash :: Maybe Hash
, txcerts :: [TxCert]
} deriving (Show, Generic)
data TxWitnesses = MkTxWitnesses
{ vkSigs :: [(Integer, Integer)]
, scripts :: [AgdaEmpty]
, txdats :: [(DataHash, Datum)]
, txrdmrs :: [(RdmrPtr, (Redeemer, ExUnits))]
} deriving (Show, Generic)
data Tx = MkTx
{ body :: TxBody
, wits :: TxWitnesses
, txAD :: Maybe AuxiliaryData
} deriving (Show, Generic)
data PParams = MkPParams
{ a :: Integer
, b :: Integer
, maxBlockSize :: Integer
, maxTxSize :: Integer
, maxHeaderSize :: Integer
, maxValSize :: Integer
, minUTxOValue :: Coin
, poolDeposit :: Coin
, emax :: Epoch
, nopt :: Integer
, pv :: (Integer, Integer)
, votingThresholds :: ()
, govActionLifetime :: Integer
, govActionDeposit :: Coin
, drepDeposit :: Coin
, drepActivity :: Epoch
, ccMinSize :: Integer
, ccMaxTermLength :: Integer
, costmdls :: ()
, prices :: ()
, maxTxExUnits :: ExUnits
, maxBlockExUnits :: ExUnits
, coinsPerUTxOWord :: Coin
, maxCollateralInputs :: Integer
} deriving (Show, Generic)
data UTxOEnv = MkUTxOEnv
{ slot :: Integer
, pparams :: PParams
} deriving (Show, Generic)
data UTxOState = MkUTxOState
{ utxo :: UTxO
, fees :: Coin
} deriving (Show, Generic)
data EnactState = MkEnactState
{ esCC :: (Maybe ([(Credential, Epoch)], Rational), GovActionID)
, esConstitution :: ((DataHash, Maybe ScriptHash), GovActionID)
, esPV :: (ProtVer, GovActionID)
, esPParams :: (PParams, GovActionID)
, esWithdrawals :: [(RwdAddr, Coin)]
}
data GovEnv = MkGovEnv
{ geTxId :: TxId
, geEpoch :: Epoch
, gePParams :: PParams
, gePPolicy :: Maybe ScriptHash
, geEnactState :: EnactState
}
type Voter = (GovRole, Credential)
type GovState = [(GovActionID, GovActionState)]
data GovAction
= NoConfidence
| NewCommittee [(Credential, Epoch)] [Credential] Rational
| NewConstitution DataHash (Maybe ScriptHash)
| TriggerHF ProtVer
| ChangePParams PParamsUpdate
| TreasuryWdrl [(RwdAddr, Coin)]
| Info
data Vote
= VoteYes
| VoteNo
| VoteAbstain
data GovActionState = MkGovActionState
{ gasVotes :: [(Voter, Vote)]
, gasReturnAddr :: RwdAddr
, gasExpiresIn :: Epoch
, gasAction :: GovAction
, gasPrevAction :: GovActionID
}
data GovVote = MkGovVote
{ gvGid :: GovActionID
, gvVoter :: Voter
, gvVote :: Vote
, gvAnchor :: Maybe Anchor
}
data GovProposal = MkGovProposal
{ gpAction :: GovAction
, gpPrevAction :: GovActionID
, gpPolicy :: Maybe ScriptHash
, gpDeposit :: Coin
, gpReturnAddr :: RwdAddr
, gpAnchor :: Anchor
}
data GovSignal
= GovSignalVote GovVote
| GovSignalProposal GovProposal
-- Ledger.Foreign.LedgerTypes.Empty
d_Empty_6 = ()
type T_Empty_6 = AgdaEmpty
cover_Empty_6 :: AgdaEmpty -> ()
cover_Empty_6 x = case x of
-- Ledger.Foreign.LedgerTypes.ComputationResult
d_ComputationResult_12 a0 a1 = ()
type T_ComputationResult_12 a0 a1 = ComputationResult a0 a1
pattern C_Success_18 a0 = Success a0
pattern C_Failure_20 a0 = Failure a0
check_Success_18 ::
forall xE. forall xA. xA -> T_ComputationResult_12 xE xA
check_Success_18 = Success
check_Failure_20 ::
forall xE. forall xA. xE -> T_ComputationResult_12 xE xA
check_Failure_20 = Failure
cover_ComputationResult_12 :: ComputationResult a1 a2 -> ()
cover_ComputationResult_12 x
= case x of
Success _ -> ()
Failure _ -> ()
-- Ledger.Foreign.LedgerTypes.HSMap
d_HSMap_22 :: () -> () -> ()
d_HSMap_22 = erased
-- Ledger.Foreign.LedgerTypes.Rational
d_Rational_28 :: ()
d_Rational_28 = erased
-- Ledger.Foreign.LedgerTypes.TxId
d_TxId_30 = ()
type T_TxId_30 = TxId
pattern C_TxId'46'constructor_231 a0 = MkTxId a0
check_TxId'46'constructor_231 :: Integer -> T_TxId_30
check_TxId'46'constructor_231 = MkTxId
cover_TxId_30 :: TxId -> ()
cover_TxId_30 x
= case x of
MkTxId _ -> ()
-- Ledger.Foreign.LedgerTypes.TxId.txid
d_txid_34 :: T_TxId_30 -> Integer
d_txid_34 v0
= case coe v0 of
C_TxId'46'constructor_231 v1 -> coe v1
_ -> MAlonzo.RTE.mazUnreachableError
-- Ledger.Foreign.LedgerTypes.Coin
d_Coin_36 :: ()
d_Coin_36 = erased
-- Ledger.Foreign.LedgerTypes.Addr
d_Addr_38 :: ()
d_Addr_38 = erased
-- Ledger.Foreign.LedgerTypes.Ix
d_Ix_40 :: ()
d_Ix_40 = erased
-- Ledger.Foreign.LedgerTypes.Epoch
d_Epoch_42 :: ()
d_Epoch_42 = erased
-- Ledger.Foreign.LedgerTypes.ScriptHash
d_ScriptHash_44 :: ()
d_ScriptHash_44 = erased
-- Ledger.Foreign.LedgerTypes.AuxiliaryData
d_AuxiliaryData_46 :: ()
d_AuxiliaryData_46 = erased
-- Ledger.Foreign.LedgerTypes.DataHash
d_DataHash_48 :: ()
d_DataHash_48 = erased
-- Ledger.Foreign.LedgerTypes.Datum
d_Datum_50 :: ()
d_Datum_50 = erased
-- Ledger.Foreign.LedgerTypes.Redeemer
d_Redeemer_52 :: ()
d_Redeemer_52 = erased
-- Ledger.Foreign.LedgerTypes.Anchor
d_Anchor_54 :: ()
d_Anchor_54 = erased
-- Ledger.Foreign.LedgerTypes.Network
d_Network_56 :: ()
d_Network_56 = erased
-- Ledger.Foreign.LedgerTypes.PParamsUpdate
d_PParamsUpdate_58 :: ()
d_PParamsUpdate_58 = erased
-- Ledger.Foreign.LedgerTypes.Script
d_Script_60 :: ()
d_Script_60 = erased
-- Ledger.Foreign.LedgerTypes.TxIn
d_TxIn_62 :: ()
d_TxIn_62 = erased
-- Ledger.Foreign.LedgerTypes.TxOut
d_TxOut_64 :: ()
d_TxOut_64 = erased
-- Ledger.Foreign.LedgerTypes.UTxO
d_UTxO_66 :: ()
d_UTxO_66 = erased
-- Ledger.Foreign.LedgerTypes.Hash
d_Hash_68 :: ()
d_Hash_68 = erased
-- Ledger.Foreign.LedgerTypes.GovActionID
d_GovActionID_70 :: ()
d_GovActionID_70 = erased
-- Ledger.Foreign.LedgerTypes.HashProtected
d_HashProtected_72 :: () -> ()
d_HashProtected_72 = erased
-- Ledger.Foreign.LedgerTypes.Tag
d_Tag_76 = ()
type T_Tag_76 = Tag
pattern C_Spend_78 = Spend
pattern C_Mint_80 = Mint
pattern C_Cert_82 = Cert
pattern C_Rewrd_84 = Rewrd
pattern C_VoteTag_86 = Vote
pattern C_Propose_88 = Propose
check_Spend_78 :: T_Tag_76
check_Spend_78 = Spend
check_Mint_80 :: T_Tag_76
check_Mint_80 = Mint
check_Cert_82 :: T_Tag_76
check_Cert_82 = Cert
check_Rewrd_84 :: T_Tag_76
check_Rewrd_84 = Rewrd
check_VoteTag_86 :: T_Tag_76
check_VoteTag_86 = Vote
check_Propose_88 :: T_Tag_76
check_Propose_88 = Propose
cover_Tag_76 :: Tag -> ()
cover_Tag_76 x
= case x of
Spend -> ()
Mint -> ()
Cert -> ()
Rewrd -> ()
Vote -> ()
Propose -> ()
-- Ledger.Foreign.LedgerTypes.RdmrPtr
d_RdmrPtr_90 :: ()
d_RdmrPtr_90 = erased
-- Ledger.Foreign.LedgerTypes.ExUnits
d_ExUnits_92 :: ()
d_ExUnits_92 = erased
-- Ledger.Foreign.LedgerTypes.ProtVer
d_ProtVer_94 :: ()
d_ProtVer_94 = erased
-- Ledger.Foreign.LedgerTypes.Credential
d_Credential_96 = ()
type T_Credential_96 = Credential
pattern C_ScriptObj_98 a0 = ScriptObj a0
pattern C_KeyHashObj_100 a0 = KeyHashObj a0
check_ScriptObj_98 :: Integer -> T_Credential_96
check_ScriptObj_98 = ScriptObj
check_KeyHashObj_100 :: Integer -> T_Credential_96
check_KeyHashObj_100 = KeyHashObj
cover_Credential_96 :: Credential -> ()
cover_Credential_96 x
= case x of
ScriptObj _ -> ()
KeyHashObj _ -> ()
-- Ledger.Foreign.LedgerTypes.PoolParams
d_PoolParams_102 :: ()
d_PoolParams_102 = erased
-- Ledger.Foreign.LedgerTypes.RwdAddr
d_RwdAddr_104 :: ()
d_RwdAddr_104 = erased
-- Ledger.Foreign.LedgerTypes.GovRole
d_GovRole_106 = ()
type T_GovRole_106 = GovRole
pattern C_CC_108 = CC
pattern C_DRep_110 = DRep
pattern C_SPO_112 = SPO
check_CC_108 :: T_GovRole_106
check_CC_108 = CC
check_DRep_110 :: T_GovRole_106
check_DRep_110 = DRep
check_SPO_112 :: T_GovRole_106
check_SPO_112 = SPO
cover_GovRole_106 :: GovRole -> ()
cover_GovRole_106 x
= case x of
CC -> ()
DRep -> ()
SPO -> ()
-- Ledger.Foreign.LedgerTypes.VDeleg
d_VDeleg_114 = ()
type T_VDeleg_114 = VDeleg
pattern C_CredVoter_116 a0 a1 = CredVoter a0 a1
pattern C_AbstainRep_118 = AbstainRep
pattern C_NoConfidenceRep_120 = NoConfidenceRep
check_CredVoter_116 ::
T_GovRole_106 -> T_Credential_96 -> T_VDeleg_114
check_CredVoter_116 = CredVoter
check_AbstainRep_118 :: T_VDeleg_114
check_AbstainRep_118 = AbstainRep
check_NoConfidenceRep_120 :: T_VDeleg_114
check_NoConfidenceRep_120 = NoConfidenceRep
cover_VDeleg_114 :: VDeleg -> ()
cover_VDeleg_114 x
= case x of
CredVoter _ _ -> ()
AbstainRep -> ()
NoConfidenceRep -> ()
-- Ledger.Foreign.LedgerTypes.TxCert
d_TxCert_122 = ()
type T_TxCert_122 = TxCert
pattern C_Delegate_124 a0 a1 a2 a3 = Delegate a0 a1 a2 a3
pattern C_Dereg_126 a0 = Dereg a0
pattern C_RegPool_128 a0 a1 = RegPool a0 a1
pattern C_RetirePool_130 a0 a1 = RetirePool a0 a1
pattern C_RegDRep_132 a0 a1 a2 = RegDRep a0 a1 a2
pattern C_DeRegDRep_134 a0 = DeRegDRep a0
pattern C_CCRegHot_136 a0 a1 = CCRegHot a0 a1
check_Delegate_124 ::
T_Credential_96 ->
MAlonzo.Code.Agda.Builtin.Maybe.T_Maybe_10 () T_VDeleg_114 ->
MAlonzo.Code.Agda.Builtin.Maybe.T_Maybe_10 () T_Credential_96 ->
Integer -> T_TxCert_122
check_Delegate_124 = Delegate
check_Dereg_126 :: T_Credential_96 -> T_TxCert_122
check_Dereg_126 = Dereg
check_RegPool_128 ::
T_Credential_96 -> T_Credential_96 -> T_TxCert_122
check_RegPool_128 = RegPool
check_RetirePool_130 :: T_Credential_96 -> Integer -> T_TxCert_122
check_RetirePool_130 = RetirePool
check_RegDRep_132 ::
T_Credential_96 ->
Integer ->
MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6 -> T_TxCert_122
check_RegDRep_132 = RegDRep
check_DeRegDRep_134 :: T_Credential_96 -> T_TxCert_122
check_DeRegDRep_134 = DeRegDRep
check_CCRegHot_136 ::
T_Credential_96 ->
MAlonzo.Code.Agda.Builtin.Maybe.T_Maybe_10 () T_Credential_96 ->
T_TxCert_122
check_CCRegHot_136 = CCRegHot
cover_TxCert_122 :: TxCert -> ()
cover_TxCert_122 x
= case x of
Delegate _ _ _ _ -> ()
Dereg _ -> ()
RegPool _ _ -> ()
RetirePool _ _ -> ()
RegDRep _ _ _ -> ()
DeRegDRep _ -> ()
CCRegHot _ _ -> ()
-- Ledger.Foreign.LedgerTypes.TxBody
d_TxBody_138 = ()
type T_TxBody_138 = TxBody
pattern C_TxBody'46'constructor_1439 a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 = MkTxBody a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10
check_TxBody'46'constructor_1439 ::
MAlonzo.Code.Agda.Builtin.List.T_List_10
()
(MAlonzo.Code.Foreign.Haskell.Pair.T_Pair_22
() () T_TxId_30 Integer) ->
MAlonzo.Code.Agda.Builtin.List.T_List_10
()
(MAlonzo.Code.Foreign.Haskell.Pair.T_Pair_22
() () T_TxId_30 Integer) ->
MAlonzo.Code.Agda.Builtin.List.T_List_10
()
(MAlonzo.Code.Foreign.Haskell.Pair.T_Pair_22
() () Integer
(MAlonzo.Code.Foreign.Haskell.Pair.T_Pair_22
() () Integer
(MAlonzo.Code.Foreign.Haskell.Pair.T_Pair_22
() () Integer
(MAlonzo.Code.Foreign.Haskell.Pair.T_Pair_22
() ()
(MAlonzo.Code.Agda.Builtin.Maybe.T_Maybe_10
()
(MAlonzo.Code.Foreign.Haskell.Either.T_Either_22
() () MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6
MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6))
(MAlonzo.Code.Agda.Builtin.Maybe.T_Maybe_10
() MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6))))) ->
Integer ->
MAlonzo.Code.Foreign.Haskell.Pair.T_Pair_22
() () (MAlonzo.Code.Agda.Builtin.Maybe.T_Maybe_10 () Integer)
(MAlonzo.Code.Agda.Builtin.Maybe.T_Maybe_10 () Integer) ->
Integer ->
T_TxId_30 ->
MAlonzo.Code.Agda.Builtin.List.T_List_10
()
(MAlonzo.Code.Foreign.Haskell.Pair.T_Pair_22
() () T_TxId_30 Integer) ->
MAlonzo.Code.Agda.Builtin.List.T_List_10 () Integer ->
MAlonzo.Code.Agda.Builtin.Maybe.T_Maybe_10 () Integer ->
MAlonzo.Code.Agda.Builtin.List.T_List_10 () T_TxCert_122 ->
T_TxBody_138
check_TxBody'46'constructor_1439 = MkTxBody
cover_TxBody_138 :: TxBody -> ()
cover_TxBody_138 x
= case x of
MkTxBody _ _ _ _ _ _ _ _ _ _ _ -> ()
-- Ledger.Foreign.LedgerTypes.TxBody.txins
d_txins_162 ::
T_TxBody_138 ->
[MAlonzo.Code.Foreign.Haskell.Pair.T_Pair_22
AgdaAny AgdaAny T_TxId_30 Integer]
d_txins_162 v0
= case coe v0 of
C_TxBody'46'constructor_1439 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11
-> coe v1
_ -> MAlonzo.RTE.mazUnreachableError
-- Ledger.Foreign.LedgerTypes.TxBody.refInputs
d_refInputs_164 ::
T_TxBody_138 ->
[MAlonzo.Code.Foreign.Haskell.Pair.T_Pair_22
AgdaAny AgdaAny T_TxId_30 Integer]
d_refInputs_164 v0
= case coe v0 of
C_TxBody'46'constructor_1439 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11
-> coe v2
_ -> MAlonzo.RTE.mazUnreachableError
-- Ledger.Foreign.LedgerTypes.TxBody.txouts
d_txouts_166 ::
T_TxBody_138 ->
[MAlonzo.Code.Foreign.Haskell.Pair.T_Pair_22
AgdaAny AgdaAny Integer
(MAlonzo.Code.Foreign.Haskell.Pair.T_Pair_22
AgdaAny AgdaAny Integer
(MAlonzo.Code.Foreign.Haskell.Pair.T_Pair_22
AgdaAny AgdaAny Integer
(MAlonzo.Code.Foreign.Haskell.Pair.T_Pair_22
AgdaAny AgdaAny
(Maybe
(MAlonzo.Code.Foreign.Haskell.Either.T_Either_22
AgdaAny AgdaAny MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6
MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6))
(Maybe MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6))))]
d_txouts_166 v0
= case coe v0 of
C_TxBody'46'constructor_1439 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11
-> coe v3
_ -> MAlonzo.RTE.mazUnreachableError
-- Ledger.Foreign.LedgerTypes.TxBody.txfee
d_txfee_168 :: T_TxBody_138 -> Integer
d_txfee_168 v0
= case coe v0 of
C_TxBody'46'constructor_1439 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11
-> coe v4
_ -> MAlonzo.RTE.mazUnreachableError
-- Ledger.Foreign.LedgerTypes.TxBody.txvldt
d_txvldt_170 ::
T_TxBody_138 ->
MAlonzo.Code.Foreign.Haskell.Pair.T_Pair_22
AgdaAny AgdaAny (Maybe Integer) (Maybe Integer)
d_txvldt_170 v0
= case coe v0 of
C_TxBody'46'constructor_1439 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11
-> coe v5
_ -> MAlonzo.RTE.mazUnreachableError
-- Ledger.Foreign.LedgerTypes.TxBody.txsize
d_txsize_172 :: T_TxBody_138 -> Integer
d_txsize_172 v0
= case coe v0 of
C_TxBody'46'constructor_1439 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11
-> coe v6
_ -> MAlonzo.RTE.mazUnreachableError
-- Ledger.Foreign.LedgerTypes.TxBody.txid
d_txid_174 :: T_TxBody_138 -> T_TxId_30
d_txid_174 v0
= case coe v0 of
C_TxBody'46'constructor_1439 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11
-> coe v7
_ -> MAlonzo.RTE.mazUnreachableError
-- Ledger.Foreign.LedgerTypes.TxBody.collateral
d_collateral_176 ::
T_TxBody_138 ->
[MAlonzo.Code.Foreign.Haskell.Pair.T_Pair_22
AgdaAny AgdaAny T_TxId_30 Integer]
d_collateral_176 v0
= case coe v0 of
C_TxBody'46'constructor_1439 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11
-> coe v8
_ -> MAlonzo.RTE.mazUnreachableError
-- Ledger.Foreign.LedgerTypes.TxBody.reqSigHash
d_reqSigHash_178 :: T_TxBody_138 -> [Integer]
d_reqSigHash_178 v0
= case coe v0 of
C_TxBody'46'constructor_1439 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11
-> coe v9
_ -> MAlonzo.RTE.mazUnreachableError
-- Ledger.Foreign.LedgerTypes.TxBody.scriptIntHash
d_scriptIntHash_180 :: T_TxBody_138 -> Maybe Integer
d_scriptIntHash_180 v0
= case coe v0 of
C_TxBody'46'constructor_1439 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11
-> coe v10
_ -> MAlonzo.RTE.mazUnreachableError
-- Ledger.Foreign.LedgerTypes.TxBody.txcerts
d_txcerts_182 :: T_TxBody_138 -> [T_TxCert_122]
d_txcerts_182 v0
= case coe v0 of
C_TxBody'46'constructor_1439 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11
-> coe v11
_ -> MAlonzo.RTE.mazUnreachableError
-- Ledger.Foreign.LedgerTypes.TxWitnesses
d_TxWitnesses_184 = ()
type T_TxWitnesses_184 = TxWitnesses
pattern C_TxWitnesses'46'constructor_1805 a0 a1 a2 a3 = MkTxWitnesses a0 a1 a2 a3
check_TxWitnesses'46'constructor_1805 ::
MAlonzo.Code.Agda.Builtin.List.T_List_10
()
(MAlonzo.Code.Foreign.Haskell.Pair.T_Pair_22
() () Integer Integer) ->
MAlonzo.Code.Agda.Builtin.List.T_List_10 () T_Empty_6 ->
MAlonzo.Code.Agda.Builtin.List.T_List_10
()
(MAlonzo.Code.Foreign.Haskell.Pair.T_Pair_22
() () MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6
MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6) ->
MAlonzo.Code.Agda.Builtin.List.T_List_10
()
(MAlonzo.Code.Foreign.Haskell.Pair.T_Pair_22
() ()
(MAlonzo.Code.Foreign.Haskell.Pair.T_Pair_22
() () T_Tag_76 Integer)
(MAlonzo.Code.Foreign.Haskell.Pair.T_Pair_22
() () MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6
(MAlonzo.Code.Foreign.Haskell.Pair.T_Pair_22
() () Integer Integer))) ->
T_TxWitnesses_184
check_TxWitnesses'46'constructor_1805 = MkTxWitnesses
cover_TxWitnesses_184 :: TxWitnesses -> ()
cover_TxWitnesses_184 x
= case x of
MkTxWitnesses _ _ _ _ -> ()
-- Ledger.Foreign.LedgerTypes.TxWitnesses.vkSigs
d_vkSigs_194 ::
T_TxWitnesses_184 ->
[MAlonzo.Code.Foreign.Haskell.Pair.T_Pair_22
AgdaAny AgdaAny Integer Integer]
d_vkSigs_194 v0
= case coe v0 of
C_TxWitnesses'46'constructor_1805 v1 v2 v3 v4 -> coe v1
_ -> MAlonzo.RTE.mazUnreachableError
-- Ledger.Foreign.LedgerTypes.TxWitnesses.scripts
d_scripts_196 :: T_TxWitnesses_184 -> [T_Empty_6]
d_scripts_196 v0
= case coe v0 of
C_TxWitnesses'46'constructor_1805 v1 v2 v3 v4 -> coe v2
_ -> MAlonzo.RTE.mazUnreachableError
-- Ledger.Foreign.LedgerTypes.TxWitnesses.txdats
d_txdats_198 ::
T_TxWitnesses_184 ->
[MAlonzo.Code.Foreign.Haskell.Pair.T_Pair_22
AgdaAny AgdaAny MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6
MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6]
d_txdats_198 v0
= case coe v0 of
C_TxWitnesses'46'constructor_1805 v1 v2 v3 v4 -> coe v3
_ -> MAlonzo.RTE.mazUnreachableError
-- Ledger.Foreign.LedgerTypes.TxWitnesses.txrdmrs
d_txrdmrs_200 ::
T_TxWitnesses_184 ->
[MAlonzo.Code.Foreign.Haskell.Pair.T_Pair_22
AgdaAny AgdaAny
(MAlonzo.Code.Foreign.Haskell.Pair.T_Pair_22
AgdaAny AgdaAny T_Tag_76 Integer)
(MAlonzo.Code.Foreign.Haskell.Pair.T_Pair_22
AgdaAny AgdaAny MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6
(MAlonzo.Code.Foreign.Haskell.Pair.T_Pair_22
AgdaAny AgdaAny Integer Integer))]
d_txrdmrs_200 v0
= case coe v0 of
C_TxWitnesses'46'constructor_1805 v1 v2 v3 v4 -> coe v4
_ -> MAlonzo.RTE.mazUnreachableError
-- Ledger.Foreign.LedgerTypes.Tx
d_Tx_202 = ()
type T_Tx_202 = Tx
pattern C_Tx'46'constructor_1893 a0 a1 a2 = MkTx a0 a1 a2
check_Tx'46'constructor_1893 ::
T_TxBody_138 ->
T_TxWitnesses_184 ->
MAlonzo.Code.Agda.Builtin.Maybe.T_Maybe_10
() MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6 ->
T_Tx_202
check_Tx'46'constructor_1893 = MkTx
cover_Tx_202 :: Tx -> ()
cover_Tx_202 x
= case x of
MkTx _ _ _ -> ()
-- Ledger.Foreign.LedgerTypes.Tx.body
d_body_210 :: T_Tx_202 -> T_TxBody_138
d_body_210 v0
= case coe v0 of
C_Tx'46'constructor_1893 v1 v2 v3 -> coe v1
_ -> MAlonzo.RTE.mazUnreachableError
-- Ledger.Foreign.LedgerTypes.Tx.wits
d_wits_212 :: T_Tx_202 -> T_TxWitnesses_184
d_wits_212 v0
= case coe v0 of
C_Tx'46'constructor_1893 v1 v2 v3 -> coe v2
_ -> MAlonzo.RTE.mazUnreachableError
-- Ledger.Foreign.LedgerTypes.Tx.txAD
d_txAD_214 ::
T_Tx_202 -> Maybe MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6
d_txAD_214 v0
= case coe v0 of
C_Tx'46'constructor_1893 v1 v2 v3 -> coe v3
_ -> MAlonzo.RTE.mazUnreachableError
-- Ledger.Foreign.LedgerTypes.PParams
d_PParams_216 = ()
type T_PParams_216 = PParams
pattern C_PParams'46'constructor_2621 a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13 a14 a15 a16 a17 a18 a19 a20 a21 a22 a23 = MkPParams a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13 a14 a15 a16 a17 a18 a19 a20 a21 a22 a23
check_PParams'46'constructor_2621 ::
Integer ->
Integer ->
Integer ->
Integer ->
Integer ->
Integer ->
Integer ->
Integer ->
Integer ->
Integer ->
MAlonzo.Code.Foreign.Haskell.Pair.T_Pair_22
() () Integer Integer ->
MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6 ->
Integer ->
Integer ->
Integer ->
Integer ->
Integer ->
Integer ->
MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6 ->
MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6 ->
MAlonzo.Code.Foreign.Haskell.Pair.T_Pair_22
() () Integer Integer ->
MAlonzo.Code.Foreign.Haskell.Pair.T_Pair_22
() () Integer Integer ->
Integer -> Integer -> T_PParams_216
check_PParams'46'constructor_2621 = MkPParams
cover_PParams_216 :: PParams -> ()
cover_PParams_216 x
= case x of
MkPParams _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ -> ()
-- Ledger.Foreign.LedgerTypes.PParams.a
d_a_266 :: T_PParams_216 -> Integer
d_a_266 v0
= case coe v0 of
C_PParams'46'constructor_2621 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 v17 v18 v19 v20 v21 v22 v23 v24
-> coe v1
_ -> MAlonzo.RTE.mazUnreachableError
-- Ledger.Foreign.LedgerTypes.PParams.b
d_b_268 :: T_PParams_216 -> Integer
d_b_268 v0
= case coe v0 of
C_PParams'46'constructor_2621 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 v17 v18 v19 v20 v21 v22 v23 v24
-> coe v2
_ -> MAlonzo.RTE.mazUnreachableError
-- Ledger.Foreign.LedgerTypes.PParams.maxBlockSize
d_maxBlockSize_270 :: T_PParams_216 -> Integer
d_maxBlockSize_270 v0
= case coe v0 of
C_PParams'46'constructor_2621 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 v17 v18 v19 v20 v21 v22 v23 v24
-> coe v3
_ -> MAlonzo.RTE.mazUnreachableError
-- Ledger.Foreign.LedgerTypes.PParams.maxTxSize
d_maxTxSize_272 :: T_PParams_216 -> Integer
d_maxTxSize_272 v0
= case coe v0 of
C_PParams'46'constructor_2621 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 v17 v18 v19 v20 v21 v22 v23 v24
-> coe v4
_ -> MAlonzo.RTE.mazUnreachableError
-- Ledger.Foreign.LedgerTypes.PParams.maxHeaderSize
d_maxHeaderSize_274 :: T_PParams_216 -> Integer
d_maxHeaderSize_274 v0
= case coe v0 of
C_PParams'46'constructor_2621 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 v17 v18 v19 v20 v21 v22 v23 v24
-> coe v5
_ -> MAlonzo.RTE.mazUnreachableError
-- Ledger.Foreign.LedgerTypes.PParams.maxValSize
d_maxValSize_276 :: T_PParams_216 -> Integer
d_maxValSize_276 v0
= case coe v0 of
C_PParams'46'constructor_2621 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 v17 v18 v19 v20 v21 v22 v23 v24
-> coe v6
_ -> MAlonzo.RTE.mazUnreachableError
-- Ledger.Foreign.LedgerTypes.PParams.minUTxOValue
d_minUTxOValue_278 :: T_PParams_216 -> Integer
d_minUTxOValue_278 v0
= case coe v0 of
C_PParams'46'constructor_2621 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 v17 v18 v19 v20 v21 v22 v23 v24
-> coe v7
_ -> MAlonzo.RTE.mazUnreachableError
-- Ledger.Foreign.LedgerTypes.PParams.poolDeposit
d_poolDeposit_280 :: T_PParams_216 -> Integer
d_poolDeposit_280 v0
= case coe v0 of
C_PParams'46'constructor_2621 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 v17 v18 v19 v20 v21 v22 v23 v24
-> coe v8
_ -> MAlonzo.RTE.mazUnreachableError
-- Ledger.Foreign.LedgerTypes.PParams.Emax
d_Emax_282 :: T_PParams_216 -> Integer
d_Emax_282 v0
= case coe v0 of
C_PParams'46'constructor_2621 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 v17 v18 v19 v20 v21 v22 v23 v24
-> coe v9
_ -> MAlonzo.RTE.mazUnreachableError
-- Ledger.Foreign.LedgerTypes.PParams.nopt
d_nopt_284 :: T_PParams_216 -> Integer
d_nopt_284 v0
= case coe v0 of
C_PParams'46'constructor_2621 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 v17 v18 v19 v20 v21 v22 v23 v24
-> coe v10
_ -> MAlonzo.RTE.mazUnreachableError
-- Ledger.Foreign.LedgerTypes.PParams.pv
d_pv_286 ::
T_PParams_216 ->
MAlonzo.Code.Foreign.Haskell.Pair.T_Pair_22
AgdaAny AgdaAny Integer Integer
d_pv_286 v0
= case coe v0 of
C_PParams'46'constructor_2621 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 v17 v18 v19 v20 v21 v22 v23 v24
-> coe v11
_ -> MAlonzo.RTE.mazUnreachableError
-- Ledger.Foreign.LedgerTypes.PParams.votingThresholds
d_votingThresholds_288 ::
T_PParams_216 -> MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6
d_votingThresholds_288 v0
= case coe v0 of
C_PParams'46'constructor_2621 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 v17 v18 v19 v20 v21 v22 v23 v24
-> coe v12
_ -> MAlonzo.RTE.mazUnreachableError
-- Ledger.Foreign.LedgerTypes.PParams.govActionLifetime
d_govActionLifetime_290 :: T_PParams_216 -> Integer
d_govActionLifetime_290 v0
= case coe v0 of
C_PParams'46'constructor_2621 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 v17 v18 v19 v20 v21 v22 v23 v24
-> coe v13
_ -> MAlonzo.RTE.mazUnreachableError
-- Ledger.Foreign.LedgerTypes.PParams.govActionDeposit
d_govActionDeposit_292 :: T_PParams_216 -> Integer
d_govActionDeposit_292 v0
= case coe v0 of
C_PParams'46'constructor_2621 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 v17 v18 v19 v20 v21 v22 v23 v24
-> coe v14
_ -> MAlonzo.RTE.mazUnreachableError
-- Ledger.Foreign.LedgerTypes.PParams.drepDeposit
d_drepDeposit_294 :: T_PParams_216 -> Integer
d_drepDeposit_294 v0
= case coe v0 of
C_PParams'46'constructor_2621 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 v17 v18 v19 v20 v21 v22 v23 v24
-> coe v15
_ -> MAlonzo.RTE.mazUnreachableError
-- Ledger.Foreign.LedgerTypes.PParams.drepActivity
d_drepActivity_296 :: T_PParams_216 -> Integer
d_drepActivity_296 v0
= case coe v0 of
C_PParams'46'constructor_2621 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 v17 v18 v19 v20 v21 v22 v23 v24
-> coe v16
_ -> MAlonzo.RTE.mazUnreachableError
-- Ledger.Foreign.LedgerTypes.PParams.ccMinSize
d_ccMinSize_298 :: T_PParams_216 -> Integer
d_ccMinSize_298 v0
= case coe v0 of
C_PParams'46'constructor_2621 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 v17 v18 v19 v20 v21 v22 v23 v24
-> coe v17
_ -> MAlonzo.RTE.mazUnreachableError
-- Ledger.Foreign.LedgerTypes.PParams.ccMaxTermLength
d_ccMaxTermLength_300 :: T_PParams_216 -> Integer
d_ccMaxTermLength_300 v0
= case coe v0 of
C_PParams'46'constructor_2621 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 v17 v18 v19 v20 v21 v22 v23 v24
-> coe v18
_ -> MAlonzo.RTE.mazUnreachableError
-- Ledger.Foreign.LedgerTypes.PParams.costmdls
d_costmdls_302 ::
T_PParams_216 -> MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6
d_costmdls_302 v0
= case coe v0 of
C_PParams'46'constructor_2621 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 v17 v18 v19 v20 v21 v22 v23 v24
-> coe v19
_ -> MAlonzo.RTE.mazUnreachableError
-- Ledger.Foreign.LedgerTypes.PParams.prices
d_prices_304 ::
T_PParams_216 -> MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6
d_prices_304 v0
= case coe v0 of
C_PParams'46'constructor_2621 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 v17 v18 v19 v20 v21 v22 v23 v24
-> coe v20
_ -> MAlonzo.RTE.mazUnreachableError
-- Ledger.Foreign.LedgerTypes.PParams.maxTxExUnits
d_maxTxExUnits_306 ::
T_PParams_216 ->
MAlonzo.Code.Foreign.Haskell.Pair.T_Pair_22
AgdaAny AgdaAny Integer Integer
d_maxTxExUnits_306 v0
= case coe v0 of
C_PParams'46'constructor_2621 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 v17 v18 v19 v20 v21 v22 v23 v24
-> coe v21
_ -> MAlonzo.RTE.mazUnreachableError
-- Ledger.Foreign.LedgerTypes.PParams.maxBlockExUnits
d_maxBlockExUnits_308 ::
T_PParams_216 ->
MAlonzo.Code.Foreign.Haskell.Pair.T_Pair_22
AgdaAny AgdaAny Integer Integer
d_maxBlockExUnits_308 v0
= case coe v0 of
C_PParams'46'constructor_2621 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 v17 v18 v19 v20 v21 v22 v23 v24
-> coe v22
_ -> MAlonzo.RTE.mazUnreachableError
-- Ledger.Foreign.LedgerTypes.PParams.coinsPerUTxOWord
d_coinsPerUTxOWord_310 :: T_PParams_216 -> Integer
d_coinsPerUTxOWord_310 v0
= case coe v0 of
C_PParams'46'constructor_2621 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 v17 v18 v19 v20 v21 v22 v23 v24
-> coe v23
_ -> MAlonzo.RTE.mazUnreachableError
-- Ledger.Foreign.LedgerTypes.PParams.maxCollateralInputs
d_maxCollateralInputs_312 :: T_PParams_216 -> Integer
d_maxCollateralInputs_312 v0
= case coe v0 of
C_PParams'46'constructor_2621 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 v12 v13 v14 v15 v16 v17 v18 v19 v20 v21 v22 v23 v24
-> coe v24
_ -> MAlonzo.RTE.mazUnreachableError
-- Ledger.Foreign.LedgerTypes.UTxOEnv
d_UTxOEnv_314 = ()
type T_UTxOEnv_314 = UTxOEnv
pattern C_UTxOEnv'46'constructor_3851 a0 a1 = MkUTxOEnv a0 a1
check_UTxOEnv'46'constructor_3851 ::
Integer -> T_PParams_216 -> T_UTxOEnv_314
check_UTxOEnv'46'constructor_3851 = MkUTxOEnv
cover_UTxOEnv_314 :: UTxOEnv -> ()
cover_UTxOEnv_314 x
= case x of
MkUTxOEnv _ _ -> ()
-- Ledger.Foreign.LedgerTypes.UTxOEnv.slot
d_slot_320 :: T_UTxOEnv_314 -> Integer
d_slot_320 v0
= case coe v0 of
C_UTxOEnv'46'constructor_3851 v1 v2 -> coe v1
_ -> MAlonzo.RTE.mazUnreachableError
-- Ledger.Foreign.LedgerTypes.UTxOEnv.pparams
d_pparams_322 :: T_UTxOEnv_314 -> T_PParams_216
d_pparams_322 v0
= case coe v0 of
C_UTxOEnv'46'constructor_3851 v1 v2 -> coe v2
_ -> MAlonzo.RTE.mazUnreachableError
-- Ledger.Foreign.LedgerTypes.UTxOState
d_UTxOState_324 = ()
type T_UTxOState_324 = UTxOState
pattern C_UTxOState'46'constructor_3893 a0 a1 = MkUTxOState a0 a1
check_UTxOState'46'constructor_3893 ::
MAlonzo.Code.Agda.Builtin.List.T_List_10
()
(MAlonzo.Code.Foreign.Haskell.Pair.T_Pair_22
() ()
(MAlonzo.Code.Foreign.Haskell.Pair.T_Pair_22
() () T_TxId_30 Integer)
(MAlonzo.Code.Foreign.Haskell.Pair.T_Pair_22
() () Integer
(MAlonzo.Code.Foreign.Haskell.Pair.T_Pair_22
() () Integer
(MAlonzo.Code.Foreign.Haskell.Pair.T_Pair_22
() ()
(MAlonzo.Code.Agda.Builtin.Maybe.T_Maybe_10
()
(MAlonzo.Code.Foreign.Haskell.Either.T_Either_22
() () MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6
MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6))
(MAlonzo.Code.Agda.Builtin.Maybe.T_Maybe_10
() MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6))))) ->
Integer -> T_UTxOState_324
check_UTxOState'46'constructor_3893 = MkUTxOState
cover_UTxOState_324 :: UTxOState -> ()
cover_UTxOState_324 x
= case x of
MkUTxOState _ _ -> ()
-- Ledger.Foreign.LedgerTypes.UTxOState.utxo
d_utxo_330 ::
T_UTxOState_324 ->
[MAlonzo.Code.Foreign.Haskell.Pair.T_Pair_22
AgdaAny AgdaAny
(MAlonzo.Code.Foreign.Haskell.Pair.T_Pair_22
AgdaAny AgdaAny T_TxId_30 Integer)
(MAlonzo.Code.Foreign.Haskell.Pair.T_Pair_22
AgdaAny AgdaAny Integer
(MAlonzo.Code.Foreign.Haskell.Pair.T_Pair_22
AgdaAny AgdaAny Integer
(MAlonzo.Code.Foreign.Haskell.Pair.T_Pair_22
AgdaAny AgdaAny
(Maybe
(MAlonzo.Code.Foreign.Haskell.Either.T_Either_22
AgdaAny AgdaAny MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6
MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6))
(Maybe MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6))))]