{-# 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.Untyped.Purity 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.Bool
import qualified MAlonzo.Code.Agda.Builtin.Equality
import qualified MAlonzo.Code.Agda.Builtin.Maybe
import qualified MAlonzo.Code.Agda.Builtin.Sigma
import qualified MAlonzo.Code.Builtin
import qualified MAlonzo.Code.Data.Fin.Base
import qualified MAlonzo.Code.Data.Irrelevant
import qualified MAlonzo.Code.Data.List.Relation.Unary.All
import qualified MAlonzo.Code.RawU
import qualified MAlonzo.Code.Relation.Nullary.Decidable.Core
import qualified MAlonzo.Code.Relation.Nullary.Reflects
import qualified MAlonzo.Code.Untyped
import qualified MAlonzo.Code.Untyped.CEK
import qualified MAlonzo.Code.Untyped.Reduction
import qualified MAlonzo.Code.VerifiedCompilation.UntypedViews
d_Pure_6 :: p -> p -> ()
d_Pure_6 p
a0 p
a1 = ()
data T_Pure_6
= C_force_12 T_Pure_6 |
C_constr_18 MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 |
C_case_28 MAlonzo.Code.Untyped.T__'8866'_14 T_Pure_6 |
C_builtin_32 |
C_unsat'45'builtin'8320'_40 Integer Integer T_Pure_6 |
C_unsat'45'builtin'8320''8331''8321'_46 Integer T_Pure_6 |
C_unsat'45'builtin'8321'_54 Integer T_Pure_6 T_Pure_6 |
C_app_60 T_Pure_6 T_Pure_6 | C_var_64 | C_delay_68 | C_ƛ_72 |
C_con_76
d_isPure'63'_82 ::
Integer ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d_isPure'63'_82 :: Integer -> T__'8866'_14 -> T_Dec_20
d_isPure'63'_82 Integer
v0 T__'8866'_14
v1
= case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v1 of
MAlonzo.Code.Untyped.C_'96'_18 T_Fin_10
v2
-> (Bool -> T_Reflects_16 -> T_Dec_20) -> Any -> Any -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> Any
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10)
((Any -> T_Reflects_16) -> Any -> Any
forall a b. a -> b
coe
Any -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 (T_Pure_6 -> Any
forall a b. a -> b
coe T_Pure_6
C_var_64))
MAlonzo.Code.Untyped.C_ƛ_20 T__'8866'_14
v2
-> (Bool -> T_Reflects_16 -> T_Dec_20) -> Any -> Any -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> Any
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10)
((Any -> T_Reflects_16) -> Any -> Any
forall a b. a -> b
coe
Any -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 (T_Pure_6 -> Any
forall a b. a -> b
coe T_Pure_6
C_ƛ_72))
MAlonzo.Code.Untyped.C__'183'__22 T__'8866'_14
v2 T__'8866'_14
v3
-> let v4 :: Any
v4
= (Integer
-> (Integer -> T__'8866'_14 -> T_Dec_20)
-> T__'8866'_14
-> T_Dec_20)
-> Any -> (Any -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe
Integer
-> (Integer -> T__'8866'_14 -> T_Dec_20)
-> T__'8866'_14
-> T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_isLambda'63'_70
(Integer -> Any
forall a b. a -> b
coe Integer
v0)
(\ Any
v4 Any
v5 ->
T_Dec_20 -> Any
forall a b. a -> b
coe
T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_isTerm'63'_782)
(T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v2) in
Any -> T_Dec_20
forall a b. a -> b
coe
(case Any -> T_Dec_20
forall a b. a -> b
coe Any
v4 of
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v5 T_Reflects_16
v6
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v5
then case T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe T_Reflects_16
v6 of
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 Any
v7
-> case Any -> T_isLambda_54
forall a b. a -> b
coe Any
v7 of
MAlonzo.Code.VerifiedCompilation.UntypedViews.C_islambda_62 Any
v9
-> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v2 of
MAlonzo.Code.Untyped.C_ƛ_20 T__'8866'_14
v10
-> (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> Any -> Any
forall a b. a -> b -> b
seq (Any -> Any
forall a b. a -> b
coe Any
v9)
(let v11 :: Any
v11
= (T_Dec_20 -> T_Dec_20 -> T_Dec_20) -> Any -> Any -> Any
forall a b. a -> b
coe
T_Dec_20 -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.du__'215''45'dec__76
((Integer -> T__'8866'_14 -> T_Dec_20) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> T__'8866'_14 -> T_Dec_20
d_isPure'63'_82
((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer))
(Integer -> Any
forall a b. a -> b
coe Integer
v0))
(T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v10))
((Integer -> T__'8866'_14 -> T_Dec_20) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> T__'8866'_14 -> T_Dec_20
d_isPure'63'_82 (Integer -> Any
forall a b. a -> b
coe Integer
v0)
(T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v3)) in
Any -> Any
forall a b. a -> b
coe
(case Any -> T_Dec_20
forall a b. a -> b
coe Any
v11 of
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v12 T_Reflects_16
v13
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v12
then case T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe T_Reflects_16
v13 of
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 Any
v14
-> case Any -> T_Σ_14
forall a b. a -> b
coe Any
v14 of
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 Any
v15 Any
v16
-> (Bool -> T_Reflects_16 -> T_Dec_20) -> Any -> Any -> Any
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> Any
forall a b. a -> b
coe Bool
v12)
((Any -> T_Reflects_16) -> Any -> Any
forall a b. a -> b
coe
Any -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22
((T_Pure_6 -> T_Pure_6 -> T_Pure_6) -> Any -> Any -> Any
forall a b. a -> b
coe
T_Pure_6 -> T_Pure_6 -> T_Pure_6
C_app_60
Any
v15 Any
v16))
T_Σ_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Reflects_16
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
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
v13)
((Bool -> T_Reflects_16 -> T_Dec_20) -> Any -> Any -> Any
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> Any
forall a b. a -> b
coe Bool
v12)
(T_Reflects_16 -> Any
forall a b. a -> b
coe
T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26))
T_Dec_20
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError))
T__'8866'_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
T_isLambda_54
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Reflects_16
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
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
v6)
(let v7 :: Any
v7 = (T__'8866'_14 -> T_Arity_4) -> Any -> Any
forall a b. a -> b
coe T__'8866'_14 -> T_Arity_4
MAlonzo.Code.Untyped.Reduction.du_sat_36 (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v2) in
Any -> Any
forall a b. a -> b
coe
(case Any -> T_Arity_4
forall a b. a -> b
coe Any
v7 of
T_Arity_4
MAlonzo.Code.Untyped.Reduction.C_no'45'builtin_6
-> (Bool -> T_Reflects_16 -> T_Dec_20) -> Any -> Any -> Any
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> Any
forall a b. a -> b
coe Bool
v5)
(T_Reflects_16 -> Any
forall a b. a -> b
coe
T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
MAlonzo.Code.Untyped.Reduction.C_want_8 Integer
v8 Integer
v9
-> case Integer -> Integer
forall a b. a -> b
coe Integer
v8 of
Integer
0 -> case Integer -> Integer
forall a b. a -> b
coe Integer
v9 of
Integer
0 -> (Bool -> T_Reflects_16 -> T_Dec_20) -> Any -> Any -> Any
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> Any
forall a b. a -> b
coe Bool
v5)
(T_Reflects_16 -> Any
forall a b. a -> b
coe
T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
Integer
1 -> (Bool -> T_Reflects_16 -> T_Dec_20) -> Any -> Any -> Any
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> Any
forall a b. a -> b
coe Bool
v5)
(T_Reflects_16 -> Any
forall a b. a -> b
coe
T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
Integer
_ -> let v10 :: Integer
v10
= Integer -> Integer -> Integer
subInt
(Integer -> Integer
forall a b. a -> b
coe Integer
v9) (Integer -> Integer
forall a b. a -> b
coe (Integer
2 :: Integer)) in
Any -> Any
forall a b. a -> b
coe
(let v11 :: Any
v11
= (T_Dec_20 -> T_Dec_20 -> T_Dec_20) -> Any -> Any -> Any
forall a b. a -> b
coe
T_Dec_20 -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.du__'215''45'dec__76
((Integer -> T__'8866'_14 -> T_Dec_20) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> T__'8866'_14 -> T_Dec_20
d_isPure'63'_82 (Integer -> Any
forall a b. a -> b
coe Integer
v0)
(T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v2))
((Integer -> T__'8866'_14 -> T_Dec_20) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> T__'8866'_14 -> T_Dec_20
d_isPure'63'_82 (Integer -> Any
forall a b. a -> b
coe Integer
v0)
(T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v3)) in
Any -> Any
forall a b. a -> b
coe
(case Any -> T_Dec_20
forall a b. a -> b
coe Any
v11 of
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v12 T_Reflects_16
v13
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v12
then case T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe T_Reflects_16
v13 of
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 Any
v14
-> case Any -> T_Σ_14
forall a b. a -> b
coe Any
v14 of
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 Any
v15 Any
v16
-> (Bool -> T_Reflects_16 -> T_Dec_20) -> Any -> Any -> Any
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> Any
forall a b. a -> b
coe Bool
v12)
((Any -> T_Reflects_16) -> Any -> Any
forall a b. a -> b
coe
Any -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22
((Integer -> T_Pure_6 -> T_Pure_6 -> T_Pure_6)
-> Integer -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> T_Pure_6 -> T_Pure_6 -> T_Pure_6
C_unsat'45'builtin'8321'_54
Integer
v10
Any
v15
Any
v16))
T_Σ_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Reflects_16
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
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
v13)
((Bool -> T_Reflects_16 -> T_Dec_20) -> Any -> Any -> Any
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> Any
forall a b. a -> b
coe Bool
v12)
(T_Reflects_16 -> Any
forall a b. a -> b
coe
T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26))
T_Dec_20
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError))
Integer
_ -> (Bool -> T_Reflects_16 -> T_Dec_20) -> Any -> Any -> Any
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> Any
forall a b. a -> b
coe Bool
v5)
(T_Reflects_16 -> Any
forall a b. a -> b
coe
T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
T_Arity_4
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError))
T_Dec_20
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
MAlonzo.Code.Untyped.C_force_24 T__'8866'_14
v2
-> let v3 :: Any
v3
= (Integer
-> (Integer -> T__'8866'_14 -> T_Dec_20)
-> T__'8866'_14
-> T_Dec_20)
-> Any -> (Any -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe
Integer
-> (Integer -> T__'8866'_14 -> T_Dec_20)
-> T__'8866'_14
-> T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_isDelay'63'_370
(Integer -> Any
forall a b. a -> b
coe Integer
v0)
(\ Any
v3 Any
v4 ->
T_Dec_20 -> Any
forall a b. a -> b
coe
T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_isTerm'63'_782)
(T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v2) in
Any -> T_Dec_20
forall a b. a -> b
coe
(case Any -> T_Dec_20
forall a b. a -> b
coe Any
v3 of
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v4 T_Reflects_16
v5
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v4
then case T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe T_Reflects_16
v5 of
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 Any
v6
-> case Any -> T_isDelay_354
forall a b. a -> b
coe Any
v6 of
MAlonzo.Code.VerifiedCompilation.UntypedViews.C_isdelay_362 Any
v8
-> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v2 of
MAlonzo.Code.Untyped.C_delay_26 T__'8866'_14
v9
-> (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> Any -> Any
forall a b. a -> b -> b
seq (Any -> Any
forall a b. a -> b
coe Any
v8)
(let v10 :: T_Dec_20
v10 = Integer -> T__'8866'_14 -> T_Dec_20
d_isPure'63'_82 (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v9) in
Any -> Any
forall a b. a -> b
coe
(case T_Dec_20 -> T_Dec_20
forall a b. a -> b
coe T_Dec_20
v10 of
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v11 T_Reflects_16
v12
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v11
then case T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe T_Reflects_16
v12 of
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 Any
v13
-> (Bool -> T_Reflects_16 -> T_Dec_20) -> Any -> Any -> Any
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> Any
forall a b. a -> b
coe Bool
v11)
((Any -> T_Reflects_16) -> Any -> Any
forall a b. a -> b
coe
Any -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22
((T_Pure_6 -> T_Pure_6) -> Any -> Any
forall a b. a -> b
coe
T_Pure_6 -> T_Pure_6
C_force_12 Any
v13))
T_Reflects_16
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
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
v12)
((Bool -> T_Reflects_16 -> T_Dec_20) -> Any -> Any -> Any
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> Any
forall a b. a -> b
coe Bool
v11)
(T_Reflects_16 -> Any
forall a b. a -> b
coe
T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26))
T_Dec_20
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError))
T__'8866'_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
T_isDelay_354
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Reflects_16
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
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
v5)
(let v6 :: Any
v6 = (T__'8866'_14 -> T_Arity_4) -> Any -> Any
forall a b. a -> b
coe T__'8866'_14 -> T_Arity_4
MAlonzo.Code.Untyped.Reduction.du_sat_36 (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v2) in
Any -> Any
forall a b. a -> b
coe
(case Any -> T_Arity_4
forall a b. a -> b
coe Any
v6 of
T_Arity_4
MAlonzo.Code.Untyped.Reduction.C_no'45'builtin_6
-> (Bool -> T_Reflects_16 -> T_Dec_20) -> Any -> Any -> Any
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> Any
forall a b. a -> b
coe Bool
v4)
(T_Reflects_16 -> Any
forall a b. a -> b
coe
T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
MAlonzo.Code.Untyped.Reduction.C_want_8 Integer
v7 Integer
v8
-> case Integer -> Integer
forall a b. a -> b
coe Integer
v7 of
Integer
0 -> (Bool -> T_Reflects_16 -> T_Dec_20) -> Any -> Any -> Any
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> Any
forall a b. a -> b
coe Bool
v4)
(T_Reflects_16 -> Any
forall a b. a -> b
coe
T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
Integer
1 -> case Integer -> Integer
forall a b. a -> b
coe Integer
v8 of
Integer
0 -> (Bool -> T_Reflects_16 -> T_Dec_20) -> Any -> Any -> Any
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> Any
forall a b. a -> b
coe Bool
v4)
(T_Reflects_16 -> Any
forall a b. a -> b
coe
T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
Integer
_ -> let v9 :: Integer
v9
= Integer -> Integer -> Integer
subInt
(Integer -> Integer
forall a b. a -> b
coe Integer
v8) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
Any -> Any
forall a b. a -> b
coe
(let v10 :: T_Dec_20
v10
= Integer -> T__'8866'_14 -> T_Dec_20
d_isPure'63'_82
(Integer -> Integer
forall a b. a -> b
coe Integer
v0) (T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v2) in
Any -> Any
forall a b. a -> b
coe
(case T_Dec_20 -> T_Dec_20
forall a b. a -> b
coe T_Dec_20
v10 of
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v11 T_Reflects_16
v12
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v11
then case T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe T_Reflects_16
v12 of
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 Any
v13
-> (Bool -> T_Reflects_16 -> T_Dec_20) -> Any -> Any -> Any
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> Any
forall a b. a -> b
coe Bool
v11)
((Any -> T_Reflects_16) -> Any -> Any
forall a b. a -> b
coe
Any -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22
((Integer -> T_Pure_6 -> T_Pure_6) -> Integer -> Any -> Any
forall a b. a -> b
coe
Integer -> T_Pure_6 -> T_Pure_6
C_unsat'45'builtin'8320''8331''8321'_46
Integer
v9 Any
v13))
T_Reflects_16
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
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
v12)
((Bool -> T_Reflects_16 -> T_Dec_20) -> Any -> Any -> Any
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> Any
forall a b. a -> b
coe Bool
v11)
(T_Reflects_16 -> Any
forall a b. a -> b
coe
T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26))
T_Dec_20
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError))
Integer
_ -> let v9 :: Integer
v9 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v7) (Integer -> Integer
forall a b. a -> b
coe (Integer
2 :: Integer)) in
Any -> Any
forall a b. a -> b
coe
(let v10 :: T_Dec_20
v10 = Integer -> T__'8866'_14 -> T_Dec_20
d_isPure'63'_82 (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v2) in
Any -> Any
forall a b. a -> b
coe
(case T_Dec_20 -> T_Dec_20
forall a b. a -> b
coe T_Dec_20
v10 of
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v11 T_Reflects_16
v12
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v11
then case T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe T_Reflects_16
v12 of
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 Any
v13
-> (Bool -> T_Reflects_16 -> T_Dec_20) -> Any -> Any -> Any
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> Any
forall a b. a -> b
coe Bool
v11)
((Any -> T_Reflects_16) -> Any -> Any
forall a b. a -> b
coe
Any -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22
((Integer -> Integer -> T_Pure_6 -> T_Pure_6)
-> Integer -> Integer -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> T_Pure_6 -> T_Pure_6
C_unsat'45'builtin'8320'_40
Integer
v9 Integer
v8 Any
v13))
T_Reflects_16
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
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
v12)
((Bool -> T_Reflects_16 -> T_Dec_20) -> Any -> Any -> Any
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> Any
forall a b. a -> b
coe Bool
v11)
(T_Reflects_16 -> Any
forall a b. a -> b
coe
T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26))
T_Dec_20
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError))
T_Arity_4
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError))
T_Dec_20
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
MAlonzo.Code.Untyped.C_delay_26 T__'8866'_14
v2
-> (Bool -> T_Reflects_16 -> T_Dec_20) -> Any -> Any -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> Any
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10)
((Any -> T_Reflects_16) -> Any -> Any
forall a b. a -> b
coe
Any -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22
(T_Pure_6 -> Any
forall a b. a -> b
coe T_Pure_6
C_delay_68))
MAlonzo.Code.Untyped.C_con_28 T_TmCon_202
v2
-> (Bool -> T_Reflects_16 -> T_Dec_20) -> Any -> Any -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> Any
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10)
((Any -> T_Reflects_16) -> Any -> Any
forall a b. a -> b
coe
Any -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 (T_Pure_6 -> Any
forall a b. a -> b
coe T_Pure_6
C_con_76))
MAlonzo.Code.Untyped.C_constr_34 Integer
v2 [T__'8866'_14]
v3
-> let v4 :: T_Dec_20
v4 = Integer -> [T__'8866'_14] -> T_Dec_20
d_allPure'63'_88 (Integer -> Integer
forall a b. a -> b
coe Integer
v0) ([T__'8866'_14] -> [T__'8866'_14]
forall a b. a -> b
coe [T__'8866'_14]
v3) in
Any -> T_Dec_20
forall a b. a -> b
coe
(case T_Dec_20 -> T_Dec_20
forall a b. a -> b
coe T_Dec_20
v4 of
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v5 T_Reflects_16
v6
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v5
then case T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe T_Reflects_16
v6 of
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 Any
v7
-> (Bool -> T_Reflects_16 -> T_Dec_20) -> Any -> Any -> Any
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> Any
forall a b. a -> b
coe Bool
v5)
((Any -> T_Reflects_16) -> Any -> Any
forall a b. a -> b
coe
Any -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22
((T_All_44 -> T_Pure_6) -> Any -> Any
forall a b. a -> b
coe T_All_44 -> T_Pure_6
C_constr_18 Any
v7))
T_Reflects_16
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
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
v6)
((Bool -> T_Reflects_16 -> T_Dec_20) -> Any -> Any -> Any
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> Any
forall a b. a -> b
coe Bool
v5)
(T_Reflects_16 -> Any
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26))
T_Dec_20
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
MAlonzo.Code.Untyped.C_case_40 T__'8866'_14
v2 [T__'8866'_14]
v3
-> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v2 of
MAlonzo.Code.Untyped.C_'96'_18 T_Fin_10
v4
-> (Bool -> T_Reflects_16 -> T_Dec_20) -> Any -> Any -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> Any
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> Any
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
MAlonzo.Code.Untyped.C_ƛ_20 T__'8866'_14
v4
-> (Bool -> T_Reflects_16 -> T_Dec_20) -> Any -> Any -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> Any
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> Any
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
MAlonzo.Code.Untyped.C__'183'__22 T__'8866'_14
v4 T__'8866'_14
v5
-> (Bool -> T_Reflects_16 -> T_Dec_20) -> Any -> Any -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> Any
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> Any
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
MAlonzo.Code.Untyped.C_force_24 T__'8866'_14
v4
-> (Bool -> T_Reflects_16 -> T_Dec_20) -> Any -> Any -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> Any
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> Any
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
MAlonzo.Code.Untyped.C_delay_26 T__'8866'_14
v4
-> (Bool -> T_Reflects_16 -> T_Dec_20) -> Any -> Any -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> Any
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> Any
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
MAlonzo.Code.Untyped.C_con_28 T_TmCon_202
v4
-> (Bool -> T_Reflects_16 -> T_Dec_20) -> Any -> Any -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> Any
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> Any
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
MAlonzo.Code.Untyped.C_constr_34 Integer
v4 [T__'8866'_14]
v5
-> let v6 :: Any
v6
= (Integer -> [Any] -> Maybe Any) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> [Any] -> Maybe Any
MAlonzo.Code.Untyped.CEK.du_lookup'63'_996 (Integer -> Any
forall a b. a -> b
coe Integer
v4) ([T__'8866'_14] -> Any
forall a b. a -> b
coe [T__'8866'_14]
v3) in
Any -> T_Dec_20
forall a b. a -> b
coe
(case Any -> Maybe Any
forall a b. a -> b
coe Any
v6 of
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 Any
v7
-> let v8 :: T_Dec_20
v8
= Integer -> T__'8866'_14 -> T_Dec_20
d_isPure'63'_82
(Integer -> Integer
forall a b. a -> b
coe Integer
v0)
((T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14)
-> Any -> Any -> T__'8866'_14
forall a b. a -> b
coe
T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14
MAlonzo.Code.Untyped.Reduction.du_iterApp_242 (Any -> Any
forall a b. a -> b
coe Any
v7)
([T__'8866'_14] -> Any
forall a b. a -> b
coe [T__'8866'_14]
v5)) in
Any -> Any
forall a b. a -> b
coe
(case T_Dec_20 -> T_Dec_20
forall a b. a -> b
coe T_Dec_20
v8 of
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v9 T_Reflects_16
v10
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v9
then case T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe T_Reflects_16
v10 of
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 Any
v11
-> (Bool -> T_Reflects_16 -> T_Dec_20) -> Any -> Any -> Any
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> Any
forall a b. a -> b
coe Bool
v9)
((Any -> T_Reflects_16) -> Any -> Any
forall a b. a -> b
coe
Any -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22
((T__'8866'_14 -> T_Pure_6 -> T_Pure_6) -> Any -> Any -> Any
forall a b. a -> b
coe T__'8866'_14 -> T_Pure_6 -> T_Pure_6
C_case_28 Any
v7 Any
v11))
T_Reflects_16
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
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
v10)
((Bool -> T_Reflects_16 -> T_Dec_20) -> Any -> Any -> Any
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> Any
forall a b. a -> b
coe Bool
v9)
(T_Reflects_16 -> Any
forall a b. a -> b
coe
T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26))
T_Dec_20
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
Maybe Any
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18
-> (Bool -> T_Reflects_16 -> T_Dec_20) -> Any -> Any -> Any
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> Any
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> Any
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
Maybe Any
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
MAlonzo.Code.Untyped.C_case_40 T__'8866'_14
v4 [T__'8866'_14]
v5
-> (Bool -> T_Reflects_16 -> T_Dec_20) -> Any -> Any -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> Any
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> Any
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
MAlonzo.Code.Untyped.C_builtin_44 T_Builtin_2
v4
-> (Bool -> T_Reflects_16 -> T_Dec_20) -> Any -> Any -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> Any
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> Any
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
T__'8866'_14
MAlonzo.Code.Untyped.C_error_46
-> (Bool -> T_Reflects_16 -> T_Dec_20) -> Any -> Any -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> Any
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> Any
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
T__'8866'_14
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
MAlonzo.Code.Untyped.C_builtin_44 T_Builtin_2
v2
-> (Bool -> T_Reflects_16 -> T_Dec_20) -> Any -> Any -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> Any
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10)
((Any -> T_Reflects_16) -> Any -> Any
forall a b. a -> b
coe
Any -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22
(T_Pure_6 -> Any
forall a b. a -> b
coe T_Pure_6
C_builtin_32))
T__'8866'_14
MAlonzo.Code.Untyped.C_error_46
-> (Bool -> T_Reflects_16 -> T_Dec_20) -> Any -> Any -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> Any
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
(T_Reflects_16 -> Any
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
T__'8866'_14
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
d_allPure'63'_88 ::
Integer ->
[MAlonzo.Code.Untyped.T__'8866'_14] ->
MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d_allPure'63'_88 :: Integer -> [T__'8866'_14] -> T_Dec_20
d_allPure'63'_88 Integer
v0 [T__'8866'_14]
v1
= case [T__'8866'_14] -> [Any]
forall a b. a -> b
coe [T__'8866'_14]
v1 of
[]
-> (Bool -> T_Reflects_16 -> T_Dec_20) -> Any -> Any -> T_Dec_20
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> Any
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10)
((Any -> T_Reflects_16) -> Any -> Any
forall a b. a -> b
coe
Any -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22
(T_All_44 -> Any
forall a b. a -> b
coe T_All_44
MAlonzo.Code.Data.List.Relation.Unary.All.C_'91''93'_50))
(:) Any
v2 [Any]
v3
-> let v4 :: Any
v4
= (T_Dec_20 -> T_Dec_20 -> T_Dec_20) -> Any -> Any -> Any
forall a b. a -> b
coe
T_Dec_20 -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.du__'215''45'dec__76
((Integer -> T__'8866'_14 -> T_Dec_20) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> T__'8866'_14 -> T_Dec_20
d_isPure'63'_82 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Any -> Any
forall a b. a -> b
coe Any
v2))
((Integer -> [T__'8866'_14] -> T_Dec_20) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> [T__'8866'_14] -> T_Dec_20
d_allPure'63'_88 (Integer -> Any
forall a b. a -> b
coe Integer
v0) ([Any] -> Any
forall a b. a -> b
coe [Any]
v3)) in
Any -> T_Dec_20
forall a b. a -> b
coe
(case Any -> T_Dec_20
forall a b. a -> b
coe Any
v4 of
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v5 T_Reflects_16
v6
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v5
then case T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe T_Reflects_16
v6 of
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 Any
v7
-> case Any -> T_Σ_14
forall a b. a -> b
coe Any
v7 of
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 Any
v8 Any
v9
-> (Bool -> T_Reflects_16 -> T_Dec_20) -> Any -> Any -> Any
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> Any
forall a b. a -> b
coe Bool
v5)
((Any -> T_Reflects_16) -> Any -> Any
forall a b. a -> b
coe
Any -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22
((Any -> T_All_44 -> T_All_44) -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> T_All_44 -> T_All_44
MAlonzo.Code.Data.List.Relation.Unary.All.C__'8759'__60
Any
v8 Any
v9))
T_Σ_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Reflects_16
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
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
v6)
((Bool -> T_Reflects_16 -> T_Dec_20) -> Any -> Any -> Any
forall a b. a -> b
coe
Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
(Bool -> Any
forall a b. a -> b
coe Bool
v5)
(T_Reflects_16 -> Any
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26))
T_Dec_20
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
[Any]
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
d_'46'extendedlambda0_112 ::
Integer ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
[MAlonzo.Code.Untyped.T__'8866'_14] ->
(MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'46'extendedlambda0_112 :: Integer
-> T__'8866'_14
-> [T__'8866'_14]
-> (T_Σ_14 -> T_Irrelevant_20)
-> T_All_44
-> T_Irrelevant_20
d_'46'extendedlambda0_112 = Integer
-> T__'8866'_14
-> [T__'8866'_14]
-> (T_Σ_14 -> T_Irrelevant_20)
-> T_All_44
-> T_Irrelevant_20
forall a. a
erased
d_'46'extendedlambda1_158 ::
Integer ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
(MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
T_Pure_6 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'46'extendedlambda1_158 :: Integer
-> T__'8866'_14
-> T__'8866'_14
-> (T_Σ_14 -> T_Irrelevant_20)
-> T_Pure_6
-> T_Irrelevant_20
d_'46'extendedlambda1_158 = Integer
-> T__'8866'_14
-> T__'8866'_14
-> (T_Σ_14 -> T_Irrelevant_20)
-> T_Pure_6
-> T_Irrelevant_20
forall a. a
erased
d_'46'extendedlambda2_182 ::
Integer ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
(MAlonzo.Code.VerifiedCompilation.UntypedViews.T_isLambda_54 ->
MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
T_Pure_6 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'46'extendedlambda2_182 :: Integer
-> T__'8866'_14
-> T__'8801'__12
-> (T_isLambda_54 -> T_Irrelevant_20)
-> T__'8866'_14
-> T_Pure_6
-> T_Irrelevant_20
d_'46'extendedlambda2_182 = Integer
-> T__'8866'_14
-> T__'8801'__12
-> (T_isLambda_54 -> T_Irrelevant_20)
-> T__'8866'_14
-> T_Pure_6
-> T_Irrelevant_20
forall a. a
erased
d_'46'extendedlambda3_200 ::
Integer ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
(MAlonzo.Code.VerifiedCompilation.UntypedViews.T_isLambda_54 ->
MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
T_Pure_6 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'46'extendedlambda3_200 :: Integer
-> T__'8866'_14
-> T__'8801'__12
-> (T_isLambda_54 -> T_Irrelevant_20)
-> T__'8866'_14
-> T_Pure_6
-> T_Irrelevant_20
d_'46'extendedlambda3_200 = Integer
-> T__'8866'_14
-> T__'8801'__12
-> (T_isLambda_54 -> T_Irrelevant_20)
-> T__'8866'_14
-> T_Pure_6
-> T_Irrelevant_20
forall a. a
erased
d_'46'extendedlambda4_214 ::
Integer ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
(MAlonzo.Code.VerifiedCompilation.UntypedViews.T_isLambda_54 ->
MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
T_Pure_6 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'46'extendedlambda4_214 :: Integer
-> T__'8866'_14
-> T__'8801'__12
-> (T_isLambda_54 -> T_Irrelevant_20)
-> T__'8866'_14
-> T_Pure_6
-> T_Irrelevant_20
d_'46'extendedlambda4_214 = Integer
-> T__'8866'_14
-> T__'8801'__12
-> (T_isLambda_54 -> T_Irrelevant_20)
-> T__'8866'_14
-> T_Pure_6
-> T_Irrelevant_20
forall a. a
erased
d_'46'extendedlambda5_232 ::
Integer ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
Integer ->
Integer ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
(MAlonzo.Code.VerifiedCompilation.UntypedViews.T_isLambda_54 ->
MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
T_Pure_6 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'46'extendedlambda5_232 :: Integer
-> T__'8866'_14
-> Integer
-> Integer
-> T__'8801'__12
-> (T_isLambda_54 -> T_Irrelevant_20)
-> T__'8866'_14
-> T_Pure_6
-> T_Irrelevant_20
d_'46'extendedlambda5_232 = Integer
-> T__'8866'_14
-> Integer
-> Integer
-> T__'8801'__12
-> (T_isLambda_54 -> T_Irrelevant_20)
-> T__'8866'_14
-> T_Pure_6
-> T_Irrelevant_20
forall a. a
erased
d_'46'extendedlambda6_274 ::
Integer ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
(MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
Integer ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
(MAlonzo.Code.VerifiedCompilation.UntypedViews.T_isLambda_54 ->
MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
T_Pure_6 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'46'extendedlambda6_274 :: Integer
-> T__'8866'_14
-> T__'8866'_14
-> (T_Σ_14 -> T_Irrelevant_20)
-> Integer
-> T__'8801'__12
-> (T_isLambda_54 -> T_Irrelevant_20)
-> T_Pure_6
-> T_Irrelevant_20
d_'46'extendedlambda6_274 = Integer
-> T__'8866'_14
-> T__'8866'_14
-> (T_Σ_14 -> T_Irrelevant_20)
-> Integer
-> T__'8801'__12
-> (T_isLambda_54 -> T_Irrelevant_20)
-> T_Pure_6
-> T_Irrelevant_20
forall a. a
erased
d_'46'extendedlambda7_302 ::
Integer ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
(MAlonzo.Code.VerifiedCompilation.UntypedViews.T_isDelay_354 ->
MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
T_Pure_6 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'46'extendedlambda7_302 :: Integer
-> T__'8866'_14
-> T__'8801'__12
-> (T_isDelay_354 -> T_Irrelevant_20)
-> T_Pure_6
-> T_Irrelevant_20
d_'46'extendedlambda7_302 = Integer
-> T__'8866'_14
-> T__'8801'__12
-> (T_isDelay_354 -> T_Irrelevant_20)
-> T_Pure_6
-> T_Irrelevant_20
forall a. a
erased
d_'46'extendedlambda8_320 ::
Integer ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
Integer ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
(MAlonzo.Code.VerifiedCompilation.UntypedViews.T_isDelay_354 ->
MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
T_Pure_6 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'46'extendedlambda8_320 :: Integer
-> T__'8866'_14
-> Integer
-> T__'8801'__12
-> (T_isDelay_354 -> T_Irrelevant_20)
-> T_Pure_6
-> T_Irrelevant_20
d_'46'extendedlambda8_320 = Integer
-> T__'8866'_14
-> Integer
-> T__'8801'__12
-> (T_isDelay_354 -> T_Irrelevant_20)
-> T_Pure_6
-> T_Irrelevant_20
forall a. a
erased
d_'46'extendedlambda9_334 ::
Integer ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
(MAlonzo.Code.VerifiedCompilation.UntypedViews.T_isDelay_354 ->
MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
T_Pure_6 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'46'extendedlambda9_334 :: Integer
-> T__'8866'_14
-> T__'8801'__12
-> (T_isDelay_354 -> T_Irrelevant_20)
-> T_Pure_6
-> T_Irrelevant_20
d_'46'extendedlambda9_334 = Integer
-> T__'8866'_14
-> T__'8801'__12
-> (T_isDelay_354 -> T_Irrelevant_20)
-> T_Pure_6
-> T_Irrelevant_20
forall a. a
erased
d_'46'extendedlambda10_362 ::
Integer ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
(T_Pure_6 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
Integer ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
(MAlonzo.Code.VerifiedCompilation.UntypedViews.T_isDelay_354 ->
MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
T_Pure_6 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'46'extendedlambda10_362 :: Integer
-> T__'8866'_14
-> (T_Pure_6 -> T_Irrelevant_20)
-> Integer
-> T__'8801'__12
-> (T_isDelay_354 -> T_Irrelevant_20)
-> T_Pure_6
-> T_Irrelevant_20
d_'46'extendedlambda10_362 = Integer
-> T__'8866'_14
-> (T_Pure_6 -> T_Irrelevant_20)
-> Integer
-> T__'8801'__12
-> (T_isDelay_354 -> T_Irrelevant_20)
-> T_Pure_6
-> T_Irrelevant_20
forall a. a
erased
d_'46'extendedlambda11_402 ::
Integer ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
(T_Pure_6 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
Integer ->
Integer ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
(MAlonzo.Code.VerifiedCompilation.UntypedViews.T_isDelay_354 ->
MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
T_Pure_6 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'46'extendedlambda11_402 :: Integer
-> T__'8866'_14
-> (T_Pure_6 -> T_Irrelevant_20)
-> Integer
-> Integer
-> T__'8801'__12
-> (T_isDelay_354 -> T_Irrelevant_20)
-> T_Pure_6
-> T_Irrelevant_20
d_'46'extendedlambda11_402 = Integer
-> T__'8866'_14
-> (T_Pure_6 -> T_Irrelevant_20)
-> Integer
-> Integer
-> T__'8801'__12
-> (T_isDelay_354 -> T_Irrelevant_20)
-> T_Pure_6
-> T_Irrelevant_20
forall a. a
erased
d_'46'extendedlambda12_442 ::
Integer ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
(T_Pure_6 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
T_Pure_6 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'46'extendedlambda12_442 :: Integer
-> T__'8866'_14
-> (T_Pure_6 -> T_Irrelevant_20)
-> T_Pure_6
-> T_Irrelevant_20
d_'46'extendedlambda12_442 = Integer
-> T__'8866'_14
-> (T_Pure_6 -> T_Irrelevant_20)
-> T_Pure_6
-> T_Irrelevant_20
forall a. a
erased
d_'46'extendedlambda13_470 ::
Integer ->
[MAlonzo.Code.Untyped.T__'8866'_14] ->
(MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
Integer -> T_Pure_6 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'46'extendedlambda13_470 :: Integer
-> [T__'8866'_14]
-> (T_All_44 -> T_Irrelevant_20)
-> Integer
-> T_Pure_6
-> T_Irrelevant_20
d_'46'extendedlambda13_470 = Integer
-> [T__'8866'_14]
-> (T_All_44 -> T_Irrelevant_20)
-> Integer
-> T_Pure_6
-> T_Irrelevant_20
forall a. a
erased
d_'46'extendedlambda14_518 ::
Integer ->
Integer ->
[MAlonzo.Code.Untyped.T__'8866'_14] ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
[MAlonzo.Code.Untyped.T__'8866'_14] ->
T_Pure_6 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'46'extendedlambda14_518 :: Integer
-> Integer
-> [T__'8866'_14]
-> T__'8801'__12
-> [T__'8866'_14]
-> T_Pure_6
-> T_Irrelevant_20
d_'46'extendedlambda14_518 = Integer
-> Integer
-> [T__'8866'_14]
-> T__'8801'__12
-> [T__'8866'_14]
-> T_Pure_6
-> T_Irrelevant_20
forall a. a
erased
d_'46'extendedlambda15_556 ::
Integer ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
[MAlonzo.Code.Untyped.T__'8866'_14] ->
(T_Pure_6 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
Integer ->
[MAlonzo.Code.Untyped.T__'8866'_14] ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
T_Pure_6 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'46'extendedlambda15_556 :: Integer
-> T__'8866'_14
-> [T__'8866'_14]
-> (T_Pure_6 -> T_Irrelevant_20)
-> Integer
-> [T__'8866'_14]
-> T__'8801'__12
-> T_Pure_6
-> T_Irrelevant_20
d_'46'extendedlambda15_556 = Integer
-> T__'8866'_14
-> [T__'8866'_14]
-> (T_Pure_6 -> T_Irrelevant_20)
-> Integer
-> [T__'8866'_14]
-> T__'8801'__12
-> T_Pure_6
-> T_Irrelevant_20
forall a. a
erased