{-# 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.Builtin.Integer.Base 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.Maybe
import qualified MAlonzo.Code.Agda.Builtin.Sigma
import qualified MAlonzo.Code.Data.Integer.Base
import qualified MAlonzo.Code.Data.Integer.Properties
import qualified MAlonzo.Code.Data.Maybe.Base
import qualified MAlonzo.Code.Data.Nat.Base
import qualified MAlonzo.Code.Data.Sign.Base
import qualified MAlonzo.Code.Relation.Nullary.Decidable.Core
d_quot_12 ::
Integer ->
Integer -> MAlonzo.Code.Data.Nat.Base.T_NonZero_112 -> Integer
d_quot_12 :: Integer -> Integer -> T_NonZero_112 -> Integer
d_quot_12 Integer
v0 Integer
v1 ~T_NonZero_112
v2 = Integer -> Integer -> Integer
du_quot_12 Integer
v0 Integer
v1
du_quot_12 :: Integer -> Integer -> Integer
du_quot_12 :: Integer -> Integer -> Integer
du_quot_12 Integer
v0 Integer
v1
= (T_Sign_6 -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe
T_Sign_6 -> Integer -> Integer
MAlonzo.Code.Data.Integer.Base.d__'9667'__238
((T_Sign_6 -> T_Sign_6 -> T_Sign_6) -> Any -> Any -> Any
forall a b. a -> b
coe
T_Sign_6 -> T_Sign_6 -> T_Sign_6
MAlonzo.Code.Data.Sign.Base.d__'42'__14
((Integer -> T_Sign_6) -> Any -> Any
forall a b. a -> b
coe Integer -> T_Sign_6
MAlonzo.Code.Data.Integer.Base.d_sign_24 (Integer -> Any
forall a b. a -> b
coe Integer
v0))
((Integer -> T_Sign_6) -> Any -> Any
forall a b. a -> b
coe Integer -> T_Sign_6
MAlonzo.Code.Data.Integer.Base.d_sign_24 (Integer -> Any
forall a b. a -> b
coe Integer
v1)))
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'47'__318
((Integer -> Integer) -> Any -> Any
forall a b. a -> b
coe Integer -> Integer
MAlonzo.Code.Data.Integer.Base.d_'8739'_'8739'_18 (Integer -> Any
forall a b. a -> b
coe Integer
v0))
((Integer -> Integer) -> Any -> Any
forall a b. a -> b
coe Integer -> Integer
MAlonzo.Code.Data.Integer.Base.d_'8739'_'8739'_18 (Integer -> Any
forall a b. a -> b
coe Integer
v1)))
d_rem_24 ::
Integer ->
Integer -> MAlonzo.Code.Data.Nat.Base.T_NonZero_112 -> Integer
d_rem_24 :: Integer -> Integer -> T_NonZero_112 -> Integer
d_rem_24 Integer
v0 Integer
v1 ~T_NonZero_112
v2 = Integer -> Integer -> Integer
du_rem_24 Integer
v0 Integer
v1
du_rem_24 :: Integer -> Integer -> Integer
du_rem_24 :: Integer -> Integer -> Integer
du_rem_24 Integer
v0 Integer
v1
= (T_Sign_6 -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe
T_Sign_6 -> Integer -> Integer
MAlonzo.Code.Data.Integer.Base.d__'9667'__238
((Integer -> T_Sign_6) -> Any -> Any
forall a b. a -> b
coe Integer -> T_Sign_6
MAlonzo.Code.Data.Integer.Base.d_sign_24 (Integer -> Any
forall a b. a -> b
coe Integer
v0))
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer
MAlonzo.Code.Data.Nat.Base.du__'37'__330
((Integer -> Integer) -> Any -> Any
forall a b. a -> b
coe Integer -> Integer
MAlonzo.Code.Data.Integer.Base.d_'8739'_'8739'_18 (Integer -> Any
forall a b. a -> b
coe Integer
v0))
((Integer -> Integer) -> Any -> Any
forall a b. a -> b
coe Integer -> Integer
MAlonzo.Code.Data.Integer.Base.d_'8739'_'8739'_18 (Integer -> Any
forall a b. a -> b
coe Integer
v1)))
d_divModFixup_38 ::
Integer ->
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_divModFixup_38 :: Integer -> Integer -> Integer -> T_NonZero_112 -> T_Σ_14
d_divModFixup_38 Integer
v0 Integer
v1 Integer
v2 ~T_NonZero_112
v3 = Integer -> Integer -> Integer -> T_Σ_14
du_divModFixup_38 Integer
v0 Integer
v1 Integer
v2
du_divModFixup_38 ::
Integer ->
Integer -> Integer -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_divModFixup_38 :: Integer -> Integer -> Integer -> T_Σ_14
du_divModFixup_38 Integer
v0 Integer
v1 Integer
v2
= let v3 :: Any
v3
= (Any -> Any -> T_Σ_14) -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> Any -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1) in
Any -> T_Σ_14
forall a b. a -> b
coe
(case Integer -> Integer
forall a b. a -> b
coe Integer
v1 of
Integer
_ | (Integer -> Integer -> Bool) -> Any -> Any -> Bool
forall a b. a -> b
coe Integer -> Integer -> Bool
geqInt (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer)) ->
case Integer -> Any
forall a b. a -> b
coe Integer
v2 of
Any
_ | (Integer -> Integer -> Bool) -> Any -> Any -> Bool
forall a b. a -> b
coe Integer -> Integer -> Bool
ltInt (Integer -> Any
forall a b. a -> b
coe Integer
v2) (Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer)) ->
(Any -> Any -> T_Σ_14) -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> Any -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
((Integer -> Integer) -> Any -> Any
forall a b. a -> b
coe Integer -> Integer
MAlonzo.Code.Data.Integer.Base.d_pred_312 (Integer -> Any
forall a b. a -> b
coe Integer
v0))
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Data.Integer.Base.d__'43'__284 (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe Integer
v2))
Any
_ -> Any -> Any
forall a b. a -> b
coe Any
v3
Integer
0 -> Any -> Any
forall a b. a -> b
coe Any
v3
Integer
_ -> case Integer -> Any
forall a b. a -> b
coe Integer
v2 of
Any
_ | (Integer -> Integer -> Bool) -> Any -> Any -> Bool
forall a b. a -> b
coe Integer -> Integer -> Bool
geqInt (Integer -> Any
forall a b. a -> b
coe Integer
v2) (Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer)) ->
(Any -> Any -> T_Σ_14) -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> Any -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
((Integer -> Integer) -> Any -> Any
forall a b. a -> b
coe Integer -> Integer
MAlonzo.Code.Data.Integer.Base.d_pred_312 (Integer -> Any
forall a b. a -> b
coe Integer
v0))
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
MAlonzo.Code.Data.Integer.Base.d__'43'__284 (Integer -> Any
forall a b. a -> b
coe Integer
v1) (Integer -> Any
forall a b. a -> b
coe Integer
v2))
Any
_ -> Any -> Any
forall a b. a -> b
coe Any
v3)
d_divMod_64 ::
Integer ->
Integer ->
MAlonzo.Code.Data.Nat.Base.T_NonZero_112 ->
MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_divMod_64 :: Integer -> Integer -> T_NonZero_112 -> T_Σ_14
d_divMod_64 Integer
v0 Integer
v1 ~T_NonZero_112
v2 = Integer -> Integer -> T_Σ_14
du_divMod_64 Integer
v0 Integer
v1
du_divMod_64 ::
Integer -> Integer -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_divMod_64 :: Integer -> Integer -> T_Σ_14
du_divMod_64 Integer
v0 Integer
v1
= (Integer -> Integer -> Integer -> T_Σ_14)
-> Any -> Any -> Any -> T_Σ_14
forall a b. a -> b
coe
Integer -> Integer -> Integer -> T_Σ_14
du_divModFixup_38 ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
du_quot_12 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1))
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
du_rem_24 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1)) (Integer -> Any
forall a b. a -> b
coe Integer
v1)
d_div_76 ::
Integer ->
Integer -> MAlonzo.Code.Data.Nat.Base.T_NonZero_112 -> Integer
d_div_76 :: Integer -> Integer -> T_NonZero_112 -> Integer
d_div_76 Integer
v0 Integer
v1 ~T_NonZero_112
v2 = Integer -> Integer -> Integer
du_div_76 Integer
v0 Integer
v1
du_div_76 :: Integer -> Integer -> Integer
du_div_76 :: Integer -> Integer -> Integer
du_div_76 Integer
v0 Integer
v1
= (T_Σ_14 -> Any) -> Any -> Integer
forall a b. a -> b
coe
T_Σ_14 -> Any
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28
((Integer -> Integer -> T_Σ_14) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> T_Σ_14
du_divMod_64 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1))
d_mod_88 ::
Integer ->
Integer -> MAlonzo.Code.Data.Nat.Base.T_NonZero_112 -> Integer
d_mod_88 :: Integer -> Integer -> T_NonZero_112 -> Integer
d_mod_88 Integer
v0 Integer
v1 ~T_NonZero_112
v2 = Integer -> Integer -> Integer
du_mod_88 Integer
v0 Integer
v1
du_mod_88 :: Integer -> Integer -> Integer
du_mod_88 :: Integer -> Integer -> Integer
du_mod_88 Integer
v0 Integer
v1
= (T_Σ_14 -> Any) -> Any -> Integer
forall a b. a -> b
coe
T_Σ_14 -> Any
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30
((Integer -> Integer -> T_Σ_14) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> T_Σ_14
du_divMod_64 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1))
agdaQuotientInteger ::
Integer ->
Integer -> MAlonzo.Code.Agda.Builtin.Maybe.T_Maybe_10 () Integer
agdaQuotientInteger :: Integer -> Integer -> T_Maybe_10 () Integer
agdaQuotientInteger = (Integer -> Integer -> T_Maybe_10 () Integer)
-> Integer -> Integer -> T_Maybe_10 () Integer
forall a b. a -> b
coe Integer -> Integer -> T_Maybe_10 () Integer
d_quotMaybe_94
d_quotMaybe_94 :: Integer -> Integer -> Maybe Integer
d_quotMaybe_94 :: Integer -> Integer -> T_Maybe_10 () Integer
d_quotMaybe_94 Integer
v0 Integer
v1
= let v2 :: T_Dec_20
v2
= Integer -> Integer -> T_Dec_20
MAlonzo.Code.Data.Integer.Properties.d__'8799'__2800
(Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe Integer
MAlonzo.Code.Data.Integer.Base.d_0ℤ_12) in
Any -> T_Maybe_10 () Integer
forall a b. a -> b
coe
(case T_Dec_20 -> T_Dec_20
forall a b. a -> b
coe T_Dec_20
v2 of
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v3 T_Reflects_16
v4
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v3
then (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> Any -> Any
forall a b. a -> b -> b
seq (T_Reflects_16 -> Any
forall a b. a -> b
coe T_Reflects_16
v4) (Maybe Any -> Any
forall a b. a -> b
coe Maybe Any
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18)
else (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> Any -> Any
forall a b. a -> b -> b
seq (T_Reflects_16 -> Any
forall a b. a -> b
coe T_Reflects_16
v4)
((Any -> Maybe Any) -> Any -> Any
forall a b. a -> b
coe
Any -> Maybe Any
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
du_quot_12 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1)))
T_Dec_20
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
agdaRemainderInteger ::
Integer ->
Integer -> MAlonzo.Code.Agda.Builtin.Maybe.T_Maybe_10 () Integer
agdaRemainderInteger :: Integer -> Integer -> T_Maybe_10 () Integer
agdaRemainderInteger = (Integer -> Integer -> T_Maybe_10 () Integer)
-> Integer -> Integer -> T_Maybe_10 () Integer
forall a b. a -> b
coe Integer -> Integer -> T_Maybe_10 () Integer
d_remMaybe_120
d_remMaybe_120 :: Integer -> Integer -> Maybe Integer
d_remMaybe_120 :: Integer -> Integer -> T_Maybe_10 () Integer
d_remMaybe_120 Integer
v0 Integer
v1
= let v2 :: T_Dec_20
v2
= Integer -> Integer -> T_Dec_20
MAlonzo.Code.Data.Integer.Properties.d__'8799'__2800
(Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe Integer
MAlonzo.Code.Data.Integer.Base.d_0ℤ_12) in
Any -> T_Maybe_10 () Integer
forall a b. a -> b
coe
(case T_Dec_20 -> T_Dec_20
forall a b. a -> b
coe T_Dec_20
v2 of
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v3 T_Reflects_16
v4
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v3
then (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> Any -> Any
forall a b. a -> b -> b
seq (T_Reflects_16 -> Any
forall a b. a -> b
coe T_Reflects_16
v4) (Maybe Any -> Any
forall a b. a -> b
coe Maybe Any
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18)
else (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> Any -> Any
forall a b. a -> b -> b
seq (T_Reflects_16 -> Any
forall a b. a -> b
coe T_Reflects_16
v4)
((Any -> Maybe Any) -> Any -> Any
forall a b. a -> b
coe
Any -> Maybe Any
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
du_rem_24 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1)))
T_Dec_20
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
d_divModMaybe_146 ::
Integer -> Integer -> Maybe MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_divModMaybe_146 :: Integer -> Integer -> Maybe T_Σ_14
d_divModMaybe_146 Integer
v0 Integer
v1
= let v2 :: T_Dec_20
v2
= Integer -> Integer -> T_Dec_20
MAlonzo.Code.Data.Integer.Properties.d__'8799'__2800
(Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe Integer
MAlonzo.Code.Data.Integer.Base.d_0ℤ_12) in
Any -> Maybe T_Σ_14
forall a b. a -> b
coe
(case T_Dec_20 -> T_Dec_20
forall a b. a -> b
coe T_Dec_20
v2 of
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v3 T_Reflects_16
v4
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v3
then (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> Any -> Any
forall a b. a -> b -> b
seq (T_Reflects_16 -> Any
forall a b. a -> b
coe T_Reflects_16
v4) (Maybe Any -> Any
forall a b. a -> b
coe Maybe Any
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18)
else (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> Any -> Any
forall a b. a -> b -> b
seq (T_Reflects_16 -> Any
forall a b. a -> b
coe T_Reflects_16
v4)
((Any -> Maybe Any) -> Any -> Any
forall a b. a -> b
coe
Any -> Maybe Any
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
((Integer -> Integer -> T_Σ_14) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> T_Σ_14
du_divMod_64 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Integer -> Any
forall a b. a -> b
coe Integer
v1)))
T_Dec_20
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
agdaDivideInteger ::
Integer ->
Integer -> MAlonzo.Code.Agda.Builtin.Maybe.T_Maybe_10 () Integer
agdaDivideInteger :: Integer -> Integer -> T_Maybe_10 () Integer
agdaDivideInteger = (Integer -> Integer -> T_Maybe_10 () Integer)
-> Integer -> Integer -> T_Maybe_10 () Integer
forall a b. a -> b
coe Integer -> Integer -> T_Maybe_10 () Integer
d_divMaybe_172
d_divMaybe_172 :: Integer -> Integer -> Maybe Integer
d_divMaybe_172 :: Integer -> Integer -> T_Maybe_10 () Integer
d_divMaybe_172 Integer
v0 Integer
v1
= ((Any -> Any) -> Maybe Any -> Maybe Any)
-> (Any -> Any) -> Maybe T_Σ_14 -> T_Maybe_10 () Integer
forall a b. a -> b
coe
(Any -> Any) -> Maybe Any -> Maybe Any
MAlonzo.Code.Data.Maybe.Base.du_map_64
(\ Any
v2 -> T_Σ_14 -> Any
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28 (Any -> T_Σ_14
forall a b. a -> b
coe Any
v2))
(Integer -> Integer -> Maybe T_Σ_14
d_divModMaybe_146 (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (Integer -> Integer
forall a b. a -> b
coe Integer
v1))
agdaModInteger ::
Integer ->
Integer -> MAlonzo.Code.Agda.Builtin.Maybe.T_Maybe_10 () Integer
agdaModInteger :: Integer -> Integer -> T_Maybe_10 () Integer
agdaModInteger = (Integer -> Integer -> T_Maybe_10 () Integer)
-> Integer -> Integer -> T_Maybe_10 () Integer
forall a b. a -> b
coe Integer -> Integer -> T_Maybe_10 () Integer
d_modMaybe_178
d_modMaybe_178 :: Integer -> Integer -> Maybe Integer
d_modMaybe_178 :: Integer -> Integer -> T_Maybe_10 () Integer
d_modMaybe_178 Integer
v0 Integer
v1
= ((Any -> Any) -> Maybe Any -> Maybe Any)
-> (Any -> Any) -> Maybe T_Σ_14 -> T_Maybe_10 () Integer
forall a b. a -> b
coe
(Any -> Any) -> Maybe Any -> Maybe Any
MAlonzo.Code.Data.Maybe.Base.du_map_64
(\ Any
v2 -> T_Σ_14 -> Any
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30 (Any -> T_Σ_14
forall a b. a -> b
coe Any
v2))
(Integer -> Integer -> Maybe T_Σ_14
d_divModMaybe_146 (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (Integer -> Integer
forall a b. a -> b
coe Integer
v1))