-
Notifications
You must be signed in to change notification settings - Fork 13
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
1 parent
413ec83
commit a9ca34e
Showing
569 changed files
with
2,121,648 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,17 @@ | ||
module Lib | ||
( module X | ||
) where | ||
|
||
import MAlonzo.Code.Ledger.Foreign.LedgerTypes as X | ||
|
||
import MAlonzo.Code.Ledger.Foreign.HSLedger.Cert as X (certStep, certsStep) | ||
import MAlonzo.Code.Ledger.Foreign.HSLedger.Chain as X (chainStep) | ||
import MAlonzo.Code.Ledger.Foreign.HSLedger.Certs as X (delegStep, govCertStep, poolStep) | ||
import MAlonzo.Code.Ledger.Foreign.HSLedger.Enact as X (enactStep) | ||
import MAlonzo.Code.Ledger.Foreign.HSLedger.Epoch as X (epochStep) | ||
import MAlonzo.Code.Ledger.Foreign.HSLedger.Gov as X (govStep) | ||
import MAlonzo.Code.Ledger.Foreign.HSLedger.Ledger as X (ledgerStep) | ||
import MAlonzo.Code.Ledger.Foreign.HSLedger.NewEpoch as X (newEpochStep) | ||
import MAlonzo.Code.Ledger.Foreign.HSLedger.Ratify as X (ratifyStep) | ||
import MAlonzo.Code.Ledger.Foreign.HSLedger.Utxo as X (utxoStep, utxowStep) | ||
|
25 changes: 25 additions & 0 deletions
25
ledgerSrc/haskell/Ledger/MAlonzo/Code/Agda/Builtin/Bool.hs
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,25 @@ | ||
{-# LANGUAGE BangPatterns #-} | ||
{-# LANGUAGE EmptyCase #-} | ||
{-# LANGUAGE EmptyDataDecls #-} | ||
{-# LANGUAGE ExistentialQuantification #-} | ||
{-# LANGUAGE NoMonomorphismRestriction #-} | ||
{-# LANGUAGE OverloadedStrings #-} | ||
{-# LANGUAGE PatternSynonyms #-} | ||
{-# LANGUAGE RankNTypes #-} | ||
{-# LANGUAGE ScopedTypeVariables #-} | ||
|
||
{-# OPTIONS_GHC -Wno-overlapping-patterns #-} | ||
|
||
module MAlonzo.Code.Agda.Builtin.Bool 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 | ||
|
||
-- Agda.Builtin.Bool.Bool | ||
type T_Bool_6 = Bool | ||
d_Bool_6 = () | ||
pattern C_false_8 = False | ||
pattern C_true_10 = True |
53 changes: 53 additions & 0 deletions
53
ledgerSrc/haskell/Ledger/MAlonzo/Code/Agda/Builtin/Char.hs
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,53 @@ | ||
{-# LANGUAGE BangPatterns #-} | ||
{-# LANGUAGE EmptyCase #-} | ||
{-# LANGUAGE EmptyDataDecls #-} | ||
{-# LANGUAGE ExistentialQuantification #-} | ||
{-# LANGUAGE NoMonomorphismRestriction #-} | ||
{-# LANGUAGE OverloadedStrings #-} | ||
{-# LANGUAGE PatternSynonyms #-} | ||
{-# LANGUAGE RankNTypes #-} | ||
{-# LANGUAGE ScopedTypeVariables #-} | ||
|
||
{-# OPTIONS_GHC -Wno-overlapping-patterns #-} | ||
|
||
module MAlonzo.Code.Agda.Builtin.Char 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.Char | ||
import qualified Data.Text | ||
|
||
-- Agda.Builtin.Char.Char | ||
type T_Char_6 = Char | ||
d_Char_6 | ||
= error | ||
"MAlonzo Runtime Error: postulate evaluated: Agda.Builtin.Char.Char" | ||
-- Agda.Builtin.Char.primIsLower | ||
d_primIsLower_8 = Data.Char.isLower | ||
-- Agda.Builtin.Char.primIsDigit | ||
d_primIsDigit_10 = Data.Char.isDigit | ||
-- Agda.Builtin.Char.primIsAlpha | ||
d_primIsAlpha_12 = Data.Char.isAlpha | ||
-- Agda.Builtin.Char.primIsSpace | ||
d_primIsSpace_14 = Data.Char.isSpace | ||
-- Agda.Builtin.Char.primIsAscii | ||
d_primIsAscii_16 = Data.Char.isAscii | ||
-- Agda.Builtin.Char.primIsLatin1 | ||
d_primIsLatin1_18 = Data.Char.isLatin1 | ||
-- Agda.Builtin.Char.primIsPrint | ||
d_primIsPrint_20 = Data.Char.isPrint | ||
-- Agda.Builtin.Char.primIsHexDigit | ||
d_primIsHexDigit_22 = Data.Char.isHexDigit | ||
-- Agda.Builtin.Char.primToUpper | ||
d_primToUpper_24 = Data.Char.toUpper | ||
-- Agda.Builtin.Char.primToLower | ||
d_primToLower_26 = Data.Char.toLower | ||
-- Agda.Builtin.Char.primCharToNat | ||
d_primCharToNat_28 = (fromIntegral . fromEnum :: Char -> Integer) | ||
-- Agda.Builtin.Char.primNatToChar | ||
d_primNatToChar_30 = MAlonzo.RTE.natToChar | ||
-- Agda.Builtin.Char.primCharEquality | ||
d_primCharEquality_32 | ||
= (\ x y -> ((==) :: Char -> Char -> Bool) ( x) ( y)) |
22 changes: 22 additions & 0 deletions
22
ledgerSrc/haskell/Ledger/MAlonzo/Code/Agda/Builtin/Char/Properties.hs
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,22 @@ | ||
{-# LANGUAGE BangPatterns #-} | ||
{-# LANGUAGE EmptyCase #-} | ||
{-# LANGUAGE EmptyDataDecls #-} | ||
{-# LANGUAGE ExistentialQuantification #-} | ||
{-# LANGUAGE NoMonomorphismRestriction #-} | ||
{-# LANGUAGE OverloadedStrings #-} | ||
{-# LANGUAGE PatternSynonyms #-} | ||
{-# LANGUAGE RankNTypes #-} | ||
{-# LANGUAGE ScopedTypeVariables #-} | ||
|
||
{-# OPTIONS_GHC -Wno-overlapping-patterns #-} | ||
|
||
module MAlonzo.Code.Agda.Builtin.Char.Properties 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 | ||
|
||
-- Agda.Builtin.Char.Properties.primCharToNatInjective | ||
d_primCharToNatInjective_12 = erased |
24 changes: 24 additions & 0 deletions
24
ledgerSrc/haskell/Ledger/MAlonzo/Code/Agda/Builtin/Equality.hs
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,24 @@ | ||
{-# LANGUAGE BangPatterns #-} | ||
{-# LANGUAGE EmptyCase #-} | ||
{-# LANGUAGE EmptyDataDecls #-} | ||
{-# LANGUAGE ExistentialQuantification #-} | ||
{-# LANGUAGE NoMonomorphismRestriction #-} | ||
{-# LANGUAGE OverloadedStrings #-} | ||
{-# LANGUAGE PatternSynonyms #-} | ||
{-# LANGUAGE RankNTypes #-} | ||
{-# LANGUAGE ScopedTypeVariables #-} | ||
|
||
{-# OPTIONS_GHC -Wno-overlapping-patterns #-} | ||
|
||
module MAlonzo.Code.Agda.Builtin.Equality 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.Primitive | ||
|
||
-- Agda.Builtin.Equality._≡_ | ||
d__'8801'__12 a0 a1 a2 a3 = () | ||
data T__'8801'__12 = C_refl_20 |
151 changes: 151 additions & 0 deletions
151
ledgerSrc/haskell/Ledger/MAlonzo/Code/Agda/Builtin/Float.hs
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,151 @@ | ||
{-# LANGUAGE BangPatterns #-} | ||
{-# LANGUAGE EmptyCase #-} | ||
{-# LANGUAGE EmptyDataDecls #-} | ||
{-# LANGUAGE ExistentialQuantification #-} | ||
{-# LANGUAGE NoMonomorphismRestriction #-} | ||
{-# LANGUAGE OverloadedStrings #-} | ||
{-# LANGUAGE PatternSynonyms #-} | ||
{-# LANGUAGE RankNTypes #-} | ||
{-# LANGUAGE ScopedTypeVariables #-} | ||
|
||
{-# OPTIONS_GHC -Wno-overlapping-patterns #-} | ||
|
||
module MAlonzo.Code.Agda.Builtin.Float 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.RTE.Float | ||
|
||
-- Agda.Builtin.Float.Float | ||
type T_Float_6 = Double | ||
d_Float_6 | ||
= error | ||
"MAlonzo Runtime Error: postulate evaluated: Agda.Builtin.Float.Float" | ||
-- Agda.Builtin.Float.primFloatInequality | ||
d_primFloatInequality_8 = MAlonzo.RTE.Float.doubleLe | ||
-- Agda.Builtin.Float.primFloatEquality | ||
d_primFloatEquality_10 = MAlonzo.RTE.Float.doubleEq | ||
-- Agda.Builtin.Float.primFloatLess | ||
d_primFloatLess_12 = MAlonzo.RTE.Float.doubleLt | ||
-- Agda.Builtin.Float.primFloatIsInfinite | ||
d_primFloatIsInfinite_14 = (isInfinite :: Double -> Bool) | ||
-- Agda.Builtin.Float.primFloatIsNaN | ||
d_primFloatIsNaN_16 = (isNaN :: Double -> Bool) | ||
-- Agda.Builtin.Float.primFloatIsNegativeZero | ||
d_primFloatIsNegativeZero_18 = (isNegativeZero :: Double -> Bool) | ||
-- Agda.Builtin.Float.primFloatIsSafeInteger | ||
d_primFloatIsSafeInteger_20 = MAlonzo.RTE.Float.isSafeInteger | ||
-- Agda.Builtin.Float.primFloatToWord64 | ||
d_primFloatToWord64_22 = MAlonzo.RTE.Float.doubleToWord64 | ||
-- Agda.Builtin.Float.primNatToFloat | ||
d_primNatToFloat_24 | ||
= (MAlonzo.RTE.Float.intToDouble :: Integer -> Double) | ||
-- Agda.Builtin.Float.primIntToFloat | ||
d_primIntToFloat_26 | ||
= (MAlonzo.RTE.Float.intToDouble :: Integer -> Double) | ||
-- Agda.Builtin.Float.primFloatRound | ||
d_primFloatRound_28 = MAlonzo.RTE.Float.doubleRound | ||
-- Agda.Builtin.Float.primFloatFloor | ||
d_primFloatFloor_30 = MAlonzo.RTE.Float.doubleFloor | ||
-- Agda.Builtin.Float.primFloatCeiling | ||
d_primFloatCeiling_32 = MAlonzo.RTE.Float.doubleCeiling | ||
-- Agda.Builtin.Float.primFloatToRatio | ||
d_primFloatToRatio_36 = MAlonzo.RTE.Float.doubleToRatio | ||
-- Agda.Builtin.Float.primRatioToFloat | ||
d_primRatioToFloat_38 = MAlonzo.RTE.Float.ratioToDouble | ||
-- Agda.Builtin.Float.primFloatDecode | ||
d_primFloatDecode_42 = MAlonzo.RTE.Float.doubleDecode | ||
-- Agda.Builtin.Float.primFloatEncode | ||
d_primFloatEncode_44 = MAlonzo.RTE.Float.doubleEncode | ||
-- Agda.Builtin.Float.primShowFloat | ||
d_primShowFloat_46 | ||
= (Data.Text.pack . show :: Double -> Data.Text.Text) | ||
-- Agda.Builtin.Float.primFloatPlus | ||
d_primFloatPlus_48 = MAlonzo.RTE.Float.doublePlus | ||
-- Agda.Builtin.Float.primFloatMinus | ||
d_primFloatMinus_50 = MAlonzo.RTE.Float.doubleMinus | ||
-- Agda.Builtin.Float.primFloatTimes | ||
d_primFloatTimes_52 = MAlonzo.RTE.Float.doubleTimes | ||
-- Agda.Builtin.Float.primFloatDiv | ||
d_primFloatDiv_54 = MAlonzo.RTE.Float.doubleDiv | ||
-- Agda.Builtin.Float.primFloatPow | ||
d_primFloatPow_56 = MAlonzo.RTE.Float.doublePow | ||
-- Agda.Builtin.Float.primFloatNegate | ||
d_primFloatNegate_58 = MAlonzo.RTE.Float.doubleNegate | ||
-- Agda.Builtin.Float.primFloatSqrt | ||
d_primFloatSqrt_60 = MAlonzo.RTE.Float.doubleSqrt | ||
-- Agda.Builtin.Float.primFloatExp | ||
d_primFloatExp_62 = MAlonzo.RTE.Float.doubleExp | ||
-- Agda.Builtin.Float.primFloatLog | ||
d_primFloatLog_64 = MAlonzo.RTE.Float.doubleLog | ||
-- Agda.Builtin.Float.primFloatSin | ||
d_primFloatSin_66 = MAlonzo.RTE.Float.doubleSin | ||
-- Agda.Builtin.Float.primFloatCos | ||
d_primFloatCos_68 = MAlonzo.RTE.Float.doubleCos | ||
-- Agda.Builtin.Float.primFloatTan | ||
d_primFloatTan_70 = MAlonzo.RTE.Float.doubleTan | ||
-- Agda.Builtin.Float.primFloatASin | ||
d_primFloatASin_72 = MAlonzo.RTE.Float.doubleASin | ||
-- Agda.Builtin.Float.primFloatACos | ||
d_primFloatACos_74 = MAlonzo.RTE.Float.doubleACos | ||
-- Agda.Builtin.Float.primFloatATan | ||
d_primFloatATan_76 = MAlonzo.RTE.Float.doubleATan | ||
-- Agda.Builtin.Float.primFloatATan2 | ||
d_primFloatATan2_78 = MAlonzo.RTE.Float.doubleATan2 | ||
-- Agda.Builtin.Float.primFloatSinh | ||
d_primFloatSinh_80 = MAlonzo.RTE.Float.doubleSinh | ||
-- Agda.Builtin.Float.primFloatCosh | ||
d_primFloatCosh_82 = MAlonzo.RTE.Float.doubleCosh | ||
-- Agda.Builtin.Float.primFloatTanh | ||
d_primFloatTanh_84 = MAlonzo.RTE.Float.doubleTanh | ||
-- Agda.Builtin.Float.primFloatASinh | ||
d_primFloatASinh_86 = MAlonzo.RTE.Float.doubleASinh | ||
-- Agda.Builtin.Float.primFloatACosh | ||
d_primFloatACosh_88 = MAlonzo.RTE.Float.doubleACosh | ||
-- Agda.Builtin.Float.primFloatATanh | ||
d_primFloatATanh_90 = MAlonzo.RTE.Float.doubleATanh | ||
-- Agda.Builtin.Float.primFloatNumericalEquality | ||
d_primFloatNumericalEquality_92 :: T_Float_6 -> T_Float_6 -> Bool | ||
d_primFloatNumericalEquality_92 = coe d_primFloatEquality_10 | ||
-- Agda.Builtin.Float.primFloatNumericalLess | ||
d_primFloatNumericalLess_94 :: T_Float_6 -> T_Float_6 -> Bool | ||
d_primFloatNumericalLess_94 = coe d_primFloatLess_12 | ||
-- Agda.Builtin.Float.primRound | ||
d_primRound_96 :: T_Float_6 -> Maybe Integer | ||
d_primRound_96 = coe d_primFloatRound_28 | ||
-- Agda.Builtin.Float.primFloor | ||
d_primFloor_98 :: T_Float_6 -> Maybe Integer | ||
d_primFloor_98 = coe d_primFloatFloor_30 | ||
-- Agda.Builtin.Float.primCeiling | ||
d_primCeiling_100 :: T_Float_6 -> Maybe Integer | ||
d_primCeiling_100 = coe d_primFloatCeiling_32 | ||
-- Agda.Builtin.Float.primExp | ||
d_primExp_102 :: T_Float_6 -> T_Float_6 | ||
d_primExp_102 = coe d_primFloatExp_62 | ||
-- Agda.Builtin.Float.primLog | ||
d_primLog_104 :: T_Float_6 -> T_Float_6 | ||
d_primLog_104 = coe d_primFloatLog_64 | ||
-- Agda.Builtin.Float.primSin | ||
d_primSin_106 :: T_Float_6 -> T_Float_6 | ||
d_primSin_106 = coe d_primFloatSin_66 | ||
-- Agda.Builtin.Float.primCos | ||
d_primCos_108 :: T_Float_6 -> T_Float_6 | ||
d_primCos_108 = coe d_primFloatCos_68 | ||
-- Agda.Builtin.Float.primTan | ||
d_primTan_110 :: T_Float_6 -> T_Float_6 | ||
d_primTan_110 = coe d_primFloatTan_70 | ||
-- Agda.Builtin.Float.primASin | ||
d_primASin_112 :: T_Float_6 -> T_Float_6 | ||
d_primASin_112 = coe d_primFloatASin_72 | ||
-- Agda.Builtin.Float.primACos | ||
d_primACos_114 :: T_Float_6 -> T_Float_6 | ||
d_primACos_114 = coe d_primFloatACos_74 | ||
-- Agda.Builtin.Float.primATan | ||
d_primATan_116 :: T_Float_6 -> T_Float_6 | ||
d_primATan_116 = coe d_primFloatATan_76 | ||
-- Agda.Builtin.Float.primATan2 | ||
d_primATan2_118 :: T_Float_6 -> T_Float_6 -> T_Float_6 | ||
d_primATan2_118 = coe d_primFloatATan2_78 |
22 changes: 22 additions & 0 deletions
22
ledgerSrc/haskell/Ledger/MAlonzo/Code/Agda/Builtin/Float/Properties.hs
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,22 @@ | ||
{-# LANGUAGE BangPatterns #-} | ||
{-# LANGUAGE EmptyCase #-} | ||
{-# LANGUAGE EmptyDataDecls #-} | ||
{-# LANGUAGE ExistentialQuantification #-} | ||
{-# LANGUAGE NoMonomorphismRestriction #-} | ||
{-# LANGUAGE OverloadedStrings #-} | ||
{-# LANGUAGE PatternSynonyms #-} | ||
{-# LANGUAGE RankNTypes #-} | ||
{-# LANGUAGE ScopedTypeVariables #-} | ||
|
||
{-# OPTIONS_GHC -Wno-overlapping-patterns #-} | ||
|
||
module MAlonzo.Code.Agda.Builtin.Float.Properties 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 | ||
|
||
-- Agda.Builtin.Float.Properties.primFloatToWord64Injective | ||
d_primFloatToWord64Injective_12 = erased |
37 changes: 37 additions & 0 deletions
37
ledgerSrc/haskell/Ledger/MAlonzo/Code/Agda/Builtin/FromNat.hs
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,37 @@ | ||
{-# LANGUAGE BangPatterns #-} | ||
{-# LANGUAGE EmptyCase #-} | ||
{-# LANGUAGE EmptyDataDecls #-} | ||
{-# LANGUAGE ExistentialQuantification #-} | ||
{-# LANGUAGE NoMonomorphismRestriction #-} | ||
{-# LANGUAGE OverloadedStrings #-} | ||
{-# LANGUAGE PatternSynonyms #-} | ||
{-# LANGUAGE RankNTypes #-} | ||
{-# LANGUAGE ScopedTypeVariables #-} | ||
|
||
{-# OPTIONS_GHC -Wno-overlapping-patterns #-} | ||
|
||
module MAlonzo.Code.Agda.Builtin.FromNat 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.Primitive | ||
|
||
-- Agda.Builtin.FromNat.Number | ||
d_Number_10 a0 a1 = () | ||
newtype T_Number_10 | ||
= C_Number'46'constructor_55 (Integer -> AgdaAny -> AgdaAny) | ||
-- Agda.Builtin.FromNat.Number.Constraint | ||
d_Constraint_24 :: T_Number_10 -> Integer -> () | ||
d_Constraint_24 = erased | ||
-- Agda.Builtin.FromNat.Number.fromNat | ||
d_fromNat_30 :: T_Number_10 -> Integer -> AgdaAny -> AgdaAny | ||
d_fromNat_30 v0 | ||
= case coe v0 of | ||
C_Number'46'constructor_55 v2 -> coe v2 | ||
_ -> MAlonzo.RTE.mazUnreachableError | ||
-- Agda.Builtin.FromNat._.fromNat | ||
d_fromNat_34 :: T_Number_10 -> Integer -> AgdaAny -> AgdaAny | ||
d_fromNat_34 v0 = coe d_fromNat_30 (coe v0) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,26 @@ | ||
{-# LANGUAGE BangPatterns #-} | ||
{-# LANGUAGE EmptyCase #-} | ||
{-# LANGUAGE EmptyDataDecls #-} | ||
{-# LANGUAGE ExistentialQuantification #-} | ||
{-# LANGUAGE NoMonomorphismRestriction #-} | ||
{-# LANGUAGE OverloadedStrings #-} | ||
{-# LANGUAGE PatternSynonyms #-} | ||
{-# LANGUAGE RankNTypes #-} | ||
{-# LANGUAGE ScopedTypeVariables #-} | ||
|
||
{-# OPTIONS_GHC -Wno-overlapping-patterns #-} | ||
|
||
module MAlonzo.Code.Agda.Builtin.IO 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 | ||
|
||
type AgdaIO a b = IO b | ||
-- Agda.Builtin.IO.IO | ||
type T_IO_8 a0 a1 = AgdaIO a0 a1 | ||
d_IO_8 | ||
= error | ||
"MAlonzo Runtime Error: postulate evaluated: Agda.Builtin.IO.IO" |
Oops, something went wrong.