{-# 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.Algorithmic 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.Equality
import qualified MAlonzo.Code.Builtin
import qualified MAlonzo.Code.Builtin.Constant.Type
import qualified MAlonzo.Code.Builtin.Signature
import qualified MAlonzo.Code.Data.Fin.Base
import qualified MAlonzo.Code.Data.Irrelevant
import qualified MAlonzo.Code.Data.List.Base
import qualified MAlonzo.Code.Data.Vec.Base
import qualified MAlonzo.Code.Type
import qualified MAlonzo.Code.Type.BetaNormal
import qualified MAlonzo.Code.Utils
import qualified MAlonzo.Code.Utils.List
d_Ctx_2 :: p -> ()
d_Ctx_2 p
a0 = ()
data T_Ctx_2
= C_'8709'_4 | C__'44''8902'__8 T_Ctx_2 |
C__'44'__12 T_Ctx_2
MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4
d__'8715'__16 :: p -> p -> p -> ()
d__'8715'__16 p
a0 p
a1 p
a2 = ()
data T__'8715'__16
= C_Z_22 | C_S_30 T__'8715'__16 |
C_T_38 MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4
T__'8715'__16
d_'9839'Kinded_40 :: p -> ()
d_'9839'Kinded_40 p
a0 = ()
data T_'9839'Kinded_40
= C_'9839'_42 | C_K'9839'_48 T_'9839'Kinded_40
d_lemma'9839'Kinded_58 ::
MAlonzo.Code.Utils.T_Kind_652 ->
MAlonzo.Code.Utils.T_Kind_652 ->
MAlonzo.Code.Utils.T_Kind_652 ->
MAlonzo.Code.Utils.T_Kind_652 ->
T_'9839'Kinded_40 ->
MAlonzo.Code.Type.BetaNormal.T__'8866'Ne'8902'__6 ->
MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_lemma'9839'Kinded_58 :: T_Kind_652
-> T_Kind_652
-> T_Kind_652
-> T_Kind_652
-> T_'9839'Kinded_40
-> T__'8866'Ne'8902'__6
-> T_Irrelevant_20
d_lemma'9839'Kinded_58 = T_Kind_652
-> T_Kind_652
-> T_Kind_652
-> T_Kind_652
-> T_'9839'Kinded_40
-> T__'8866'Ne'8902'__6
-> T_Irrelevant_20
forall a. a
erased
d_ty2sty_64 ::
MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
MAlonzo.Code.Builtin.Signature.T__'8866''9839'_4
d_ty2sty_64 :: T__'8866'Nf'8902'__4 -> T__'8866''9839'_4
d_ty2sty_64 T__'8866'Nf'8902'__4
v0
= case T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4
forall a b. a -> b
coe T__'8866'Nf'8902'__4
v0 of
MAlonzo.Code.Type.BetaNormal.C_ne_20 T__'8866'Ne'8902'__6
v3
-> case T__'8866'Ne'8902'__6 -> T__'8866'Ne'8902'__6
forall a b. a -> b
coe T__'8866'Ne'8902'__6
v3 of
MAlonzo.Code.Type.BetaNormal.C__'183'__10 T_Kind_652
v5 T__'8866'Ne'8902'__6
v7 T__'8866'Nf'8902'__4
v8
-> case T__'8866'Ne'8902'__6 -> T__'8866'Ne'8902'__6
forall a b. a -> b
coe T__'8866'Ne'8902'__6
v7 of
MAlonzo.Code.Type.BetaNormal.C__'183'__10 T_Kind_652
v10 T__'8866'Ne'8902'__6
v12 T__'8866'Nf'8902'__4
v13
-> case T__'8866'Ne'8902'__6 -> T__'8866'Ne'8902'__6
forall a b. a -> b
coe T__'8866'Ne'8902'__6
v12 of
MAlonzo.Code.Type.BetaNormal.C_'94'_12 T_TyCon_6
v16
-> (Any -> Any -> Any) -> Any -> Any -> T__'8866''9839'_4
forall a b. a -> b
coe
Any -> Any -> Any
forall a b. a -> b -> b
seq (T_TyCon_6 -> Any
forall a b. a -> b
coe T_TyCon_6
v16)
((T__'8866''9839'_4 -> T__'8866''9839'_4 -> T__'8866''9839'_4)
-> T__'8866''9839'_4 -> T__'8866''9839'_4 -> Any
forall a b. a -> b
coe
T__'8866''9839'_4 -> T__'8866''9839'_4 -> T__'8866''9839'_4
MAlonzo.Code.Builtin.Signature.C_pair_24
(T__'8866'Nf'8902'__4 -> T__'8866''9839'_4
d_ty2sty_64 (T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4
forall a b. a -> b
coe T__'8866'Nf'8902'__4
v13)) (T__'8866'Nf'8902'__4 -> T__'8866''9839'_4
d_ty2sty_64 (T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4
forall a b. a -> b
coe T__'8866'Nf'8902'__4
v8)))
T__'8866'Ne'8902'__6
_ -> T__'8866''9839'_4
forall a. a
MAlonzo.RTE.mazUnreachableError
MAlonzo.Code.Type.BetaNormal.C_'94'_12 T_TyCon_6
v11
-> case T_TyCon_6 -> T_TyCon_6
forall a b. a -> b
coe T_TyCon_6
v11 of
T_TyCon_6
MAlonzo.Code.Builtin.Constant.Type.C_list_10
-> (T__'8866''9839'_4 -> T__'8866''9839'_4)
-> T__'8866''9839'_4 -> T__'8866''9839'_4
forall a b. a -> b
coe
T__'8866''9839'_4 -> T__'8866''9839'_4
MAlonzo.Code.Builtin.Signature.C_list_16 (T__'8866'Nf'8902'__4 -> T__'8866''9839'_4
d_ty2sty_64 (T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4
forall a b. a -> b
coe T__'8866'Nf'8902'__4
v8))
T_TyCon_6
MAlonzo.Code.Builtin.Constant.Type.C_array_12
-> (T__'8866''9839'_4 -> T__'8866''9839'_4)
-> T__'8866''9839'_4 -> T__'8866''9839'_4
forall a b. a -> b
coe
T__'8866''9839'_4 -> T__'8866''9839'_4
MAlonzo.Code.Builtin.Signature.C_array_20 (T__'8866'Nf'8902'__4 -> T__'8866''9839'_4
d_ty2sty_64 (T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4
forall a b. a -> b
coe T__'8866'Nf'8902'__4
v8))
T_TyCon_6
_ -> T__'8866''9839'_4
forall a. a
MAlonzo.RTE.mazUnreachableError
T__'8866'Ne'8902'__6
_ -> T__'8866''9839'_4
forall a. a
MAlonzo.RTE.mazUnreachableError
MAlonzo.Code.Type.BetaNormal.C_'94'_12 T_TyCon_6
v6
-> case T_TyCon_6 -> T_TyCon_6
forall a b. a -> b
coe T_TyCon_6
v6 of
MAlonzo.Code.Builtin.Constant.Type.C_atomic_8 T_AtomicTyCon_6
v7
-> (T_AtomicTyCon_6 -> T__'8866''9839'_4)
-> T_AtomicTyCon_6 -> T__'8866''9839'_4
forall a b. a -> b
coe T_AtomicTyCon_6 -> T__'8866''9839'_4
MAlonzo.Code.Builtin.Signature.C_atomic_12 T_AtomicTyCon_6
v7
T_TyCon_6
_ -> T__'8866''9839'_4
forall a. a
MAlonzo.RTE.mazUnreachableError
T__'8866'Ne'8902'__6
_ -> T__'8866''9839'_4
forall a. a
MAlonzo.RTE.mazUnreachableError
T__'8866'Nf'8902'__4
_ -> T__'8866''9839'_4
forall a. a
MAlonzo.RTE.mazUnreachableError
d_sty2ty_84 ::
MAlonzo.Code.Builtin.Signature.T__'8866''9839'_4 ->
MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4
d_sty2ty_84 :: T__'8866''9839'_4 -> T__'8866'Nf'8902'__4
d_sty2ty_84 T__'8866''9839'_4
v0
= (T__'8866'Ne'8902'__6 -> T__'8866'Nf'8902'__4)
-> Any -> T__'8866'Nf'8902'__4
forall a b. a -> b
coe
T__'8866'Ne'8902'__6 -> T__'8866'Nf'8902'__4
MAlonzo.Code.Type.BetaNormal.C_ne_20
(((T_Ctx'8902'_2 -> T_Kind_652 -> Any -> Any)
-> (Integer -> Integer -> T_Kind_652 -> T__'8715''8902'__14 -> Any)
-> (T_Ctx'8902'_2 -> T_Kind_652 -> T_Kind_652 -> Any -> Any -> Any)
-> (T_Ctx'8902'_2 -> T_Kind_652 -> T_TyCon_6 -> Any)
-> Integer
-> Integer
-> T__'8866''9839'_4
-> Any)
-> (Any -> Any -> Any -> Any)
-> Any
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Any
-> Any
-> Any
-> Any
forall a b. a -> b
coe
(T_Ctx'8902'_2 -> T_Kind_652 -> Any -> Any)
-> (Integer -> Integer -> T_Kind_652 -> T__'8715''8902'__14 -> Any)
-> (T_Ctx'8902'_2 -> T_Kind_652 -> T_Kind_652 -> Any -> Any -> Any)
-> (T_Ctx'8902'_2 -> T_Kind_652 -> T_TyCon_6 -> Any)
-> Integer
-> Integer
-> T__'8866''9839'_4
-> Any
MAlonzo.Code.Builtin.Signature.du_'8866''9839'2TyNe'9839'_186
(\ Any
v1 Any
v2 Any
v3 -> (T__'8866'Ne'8902'__6 -> T__'8866'Nf'8902'__4) -> Any -> Any
forall a b. a -> b
coe T__'8866'Ne'8902'__6 -> T__'8866'Nf'8902'__4
MAlonzo.Code.Type.BetaNormal.C_ne_20 Any
v3)
((Any -> Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe
(\ Any
v1 Any
v2 Any
v3 Any
v4 -> (T__'8715''8902'__14 -> T__'8866'Ne'8902'__6) -> Any -> Any
forall a b. a -> b
coe T__'8715''8902'__14 -> T__'8866'Ne'8902'__6
MAlonzo.Code.Type.BetaNormal.C_'96'_8 Any
v4))
(\ Any
v1 Any
v2 Any
v3 Any
v4 Any
v5 ->
(T_Kind_652
-> T__'8866'Ne'8902'__6
-> T__'8866'Nf'8902'__4
-> T__'8866'Ne'8902'__6)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe T_Kind_652
-> T__'8866'Ne'8902'__6
-> T__'8866'Nf'8902'__4
-> T__'8866'Ne'8902'__6
MAlonzo.Code.Type.BetaNormal.C__'183'__10 Any
v2 Any
v4 Any
v5)
((Any -> Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v1 Any
v2 -> (T_TyCon_6 -> T__'8866'Ne'8902'__6) -> Any
forall a b. a -> b
coe T_TyCon_6 -> T__'8866'Ne'8902'__6
MAlonzo.Code.Type.BetaNormal.C_'94'_12))
(Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer)) (Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer)) (T__'8866''9839'_4 -> Any
forall a b. a -> b
coe T__'8866''9839'_4
v0))
d_ty'8773'sty'8321'_90 ::
MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_ty'8773'sty'8321'_90 :: T__'8866'Nf'8902'__4 -> T__'8801'__12
d_ty'8773'sty'8321'_90 = T__'8866'Nf'8902'__4 -> T__'8801'__12
forall a. a
erased
d_ty'8773'sty'8322'_118 ::
MAlonzo.Code.Builtin.Signature.T__'8866''9839'_4 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_ty'8773'sty'8322'_118 :: T__'8866''9839'_4 -> T__'8801'__12
d_ty'8773'sty'8322'_118 = T__'8866''9839'_4 -> T__'8801'__12
forall a. a
erased
d_'10214'_'10215'_132 ::
MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 -> ()
d_'10214'_'10215'_132 :: T__'8866'Nf'8902'__4 -> ()
d_'10214'_'10215'_132 = T__'8866'Nf'8902'__4 -> ()
forall a. a
erased
d_mkCaseType_156 ::
MAlonzo.Code.Type.T_Ctx'8902'_2 ->
MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
[MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4] ->
MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4
d_mkCaseType_156 :: T_Ctx'8902'_2
-> T__'8866'Nf'8902'__4
-> [T__'8866'Nf'8902'__4]
-> T__'8866'Nf'8902'__4
d_mkCaseType_156 ~T_Ctx'8902'_2
v0 T__'8866'Nf'8902'__4
v1 = T__'8866'Nf'8902'__4
-> [T__'8866'Nf'8902'__4] -> T__'8866'Nf'8902'__4
du_mkCaseType_156 T__'8866'Nf'8902'__4
v1
du_mkCaseType_156 ::
MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
[MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4] ->
MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4
du_mkCaseType_156 :: T__'8866'Nf'8902'__4
-> [T__'8866'Nf'8902'__4] -> T__'8866'Nf'8902'__4
du_mkCaseType_156 T__'8866'Nf'8902'__4
v0
= ((Any -> Any -> Any) -> Any -> [Any] -> Any)
-> Any -> Any -> [T__'8866'Nf'8902'__4] -> T__'8866'Nf'8902'__4
forall a b. a -> b
coe
(Any -> Any -> Any) -> Any -> [Any] -> Any
MAlonzo.Code.Data.List.Base.du_foldr_216
((T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4)
-> Any
forall a b. a -> b
coe T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4
MAlonzo.Code.Type.BetaNormal.C__'8658'__16) (T__'8866'Nf'8902'__4 -> Any
forall a b. a -> b
coe T__'8866'Nf'8902'__4
v0)
d_ConstrArgs_162 ::
MAlonzo.Code.Type.T_Ctx'8902'_2 ->
T_Ctx_2 ->
[MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4] -> ()
d_ConstrArgs_162 :: T_Ctx'8902'_2 -> T_Ctx_2 -> [T__'8866'Nf'8902'__4] -> ()
d_ConstrArgs_162 = T_Ctx'8902'_2 -> T_Ctx_2 -> [T__'8866'Nf'8902'__4] -> ()
forall a. a
erased
d_Cases_172 :: p -> p -> p -> p -> p -> ()
d_Cases_172 p
a0 p
a1 p
a2 p
a3 p
a4 = ()
data T_Cases_172
= C_'91''93'_278 | C__'8759'__290 T__'8866'__178 T_Cases_172
d__'8866'__178 :: p -> p -> p -> ()
d__'8866'__178 p
a0 p
a1 p
a2 = ()
data T__'8866'__178
= C_'96'_184 T__'8715'__16 | C_ƛ_190 T__'8866'__178 |
C__'183'__196 MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4
T__'8866'__178 T__'8866'__178 |
C_Λ_202 T__'8866'__178 |
C__'183''8902'_'47'__212 MAlonzo.Code.Utils.T_Kind_652
MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 T__'8866'__178
MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 |
C_wrap_220 T__'8866'__178 |
C_unwrap_230 MAlonzo.Code.Utils.T_Kind_652
MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4
MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 T__'8866'__178 |
C_constr_240 MAlonzo.Code.Data.Fin.Base.T_Fin_10
[MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4]
MAlonzo.Code.Utils.List.T_IList_302 |
C_case_252 Integer MAlonzo.Code.Data.Vec.Base.T_Vec_28
T__'8866'__178 T_Cases_172 |
C_con_258 MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4
AgdaAny |
C_builtin_'47'__264 MAlonzo.Code.Builtin.T_Builtin_2 | C_error_268
d_conv'8715'_300 ::
MAlonzo.Code.Type.T_Ctx'8902'_2 ->
T_Ctx_2 ->
T_Ctx_2 ->
MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
T__'8715'__16 -> T__'8715'__16
d_conv'8715'_300 :: T_Ctx'8902'_2
-> T_Ctx_2
-> T_Ctx_2
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
-> T__'8801'__12
-> T__'8801'__12
-> T__'8715'__16
-> T__'8715'__16
d_conv'8715'_300 ~T_Ctx'8902'_2
v0 ~T_Ctx_2
v1 ~T_Ctx_2
v2 ~T__'8866'Nf'8902'__4
v3 ~T__'8866'Nf'8902'__4
v4 ~T__'8801'__12
v5 ~T__'8801'__12
v6 T__'8715'__16
v7
= T__'8715'__16 -> T__'8715'__16
du_conv'8715'_300 T__'8715'__16
v7
du_conv'8715'_300 :: T__'8715'__16 -> T__'8715'__16
du_conv'8715'_300 :: T__'8715'__16 -> T__'8715'__16
du_conv'8715'_300 T__'8715'__16
v0 = T__'8715'__16 -> T__'8715'__16
forall a b. a -> b
coe T__'8715'__16
v0
d_conv'8866'_312 ::
MAlonzo.Code.Type.T_Ctx'8902'_2 ->
T_Ctx_2 ->
T_Ctx_2 ->
MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
T__'8866'__178 -> T__'8866'__178
d_conv'8866'_312 :: T_Ctx'8902'_2
-> T_Ctx_2
-> T_Ctx_2
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
-> T__'8801'__12
-> T__'8801'__12
-> T__'8866'__178
-> T__'8866'__178
d_conv'8866'_312 ~T_Ctx'8902'_2
v0 ~T_Ctx_2
v1 ~T_Ctx_2
v2 ~T__'8866'Nf'8902'__4
v3 ~T__'8866'Nf'8902'__4
v4 ~T__'8801'__12
v5 ~T__'8801'__12
v6 T__'8866'__178
v7
= T__'8866'__178 -> T__'8866'__178
du_conv'8866'_312 T__'8866'__178
v7
du_conv'8866'_312 :: T__'8866'__178 -> T__'8866'__178
du_conv'8866'_312 :: T__'8866'__178 -> T__'8866'__178
du_conv'8866'_312 T__'8866'__178
v0 = T__'8866'__178 -> T__'8866'__178
forall a b. a -> b
coe T__'8866'__178
v0
d_lookupCase_328 ::
Integer ->
MAlonzo.Code.Type.T_Ctx'8902'_2 ->
T_Ctx_2 ->
MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
MAlonzo.Code.Data.Fin.Base.T_Fin_10 ->
T_Cases_172 -> T__'8866'__178
d_lookupCase_328 :: Integer
-> T_Ctx'8902'_2
-> T_Ctx_2
-> T__'8866'Nf'8902'__4
-> T_Vec_28
-> T_Fin_10
-> T_Cases_172
-> T__'8866'__178
d_lookupCase_328 ~Integer
v0 ~T_Ctx'8902'_2
v1 ~T_Ctx_2
v2 ~T__'8866'Nf'8902'__4
v3 T_Vec_28
v4 T_Fin_10
v5 T_Cases_172
v6
= T_Vec_28 -> T_Fin_10 -> T_Cases_172 -> T__'8866'__178
du_lookupCase_328 T_Vec_28
v4 T_Fin_10
v5 T_Cases_172
v6
du_lookupCase_328 ::
MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
MAlonzo.Code.Data.Fin.Base.T_Fin_10 ->
T_Cases_172 -> T__'8866'__178
du_lookupCase_328 :: T_Vec_28 -> T_Fin_10 -> T_Cases_172 -> T__'8866'__178
du_lookupCase_328 T_Vec_28
v0 T_Fin_10
v1 T_Cases_172
v2
= case T_Fin_10 -> T_Fin_10
forall a b. a -> b
coe T_Fin_10
v1 of
T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12
-> case T_Cases_172 -> T_Cases_172
forall a b. a -> b
coe T_Cases_172
v2 of
C__'8759'__290 T__'8866'__178
v7 T_Cases_172
v8 -> T__'8866'__178 -> T__'8866'__178
forall a b. a -> b
coe T__'8866'__178
v7
T_Cases_172
_ -> T__'8866'__178
forall a. a
MAlonzo.RTE.mazUnreachableError
MAlonzo.Code.Data.Fin.Base.C_suc_16 T_Fin_10
v4
-> case T_Cases_172 -> T_Cases_172
forall a b. a -> b
coe T_Cases_172
v2 of
C__'8759'__290 T__'8866'__178
v8 T_Cases_172
v9
-> case T_Vec_28 -> T_Vec_28
forall a b. a -> b
coe T_Vec_28
v0 of
MAlonzo.Code.Data.Vec.Base.C__'8759'__38 Any
v11 T_Vec_28
v12
-> (T_Vec_28 -> T_Fin_10 -> T_Cases_172 -> T__'8866'__178)
-> Any -> Any -> Any -> T__'8866'__178
forall a b. a -> b
coe T_Vec_28 -> T_Fin_10 -> T_Cases_172 -> T__'8866'__178
du_lookupCase_328 (T_Vec_28 -> Any
forall a b. a -> b
coe T_Vec_28
v12) (T_Fin_10 -> Any
forall a b. a -> b
coe T_Fin_10
v4) (T_Cases_172 -> Any
forall a b. a -> b
coe T_Cases_172
v9)
T_Vec_28
_ -> T__'8866'__178
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Cases_172
_ -> T__'8866'__178
forall a. a
MAlonzo.RTE.mazUnreachableError
T_Fin_10
_ -> T__'8866'__178
forall a. a
MAlonzo.RTE.mazUnreachableError
d_bwdMkCaseType_344 ::
MAlonzo.Code.Type.T_Ctx'8902'_2 ->
MAlonzo.Code.Utils.List.T_Bwd_6 ->
MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4
d_bwdMkCaseType_344 :: T_Ctx'8902'_2
-> T_Bwd_6 -> T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4
d_bwdMkCaseType_344 ~T_Ctx'8902'_2
v0 T_Bwd_6
v1 T__'8866'Nf'8902'__4
v2 = T_Bwd_6 -> T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4
du_bwdMkCaseType_344 T_Bwd_6
v1 T__'8866'Nf'8902'__4
v2
du_bwdMkCaseType_344 ::
MAlonzo.Code.Utils.List.T_Bwd_6 ->
MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4
du_bwdMkCaseType_344 :: T_Bwd_6 -> T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4
du_bwdMkCaseType_344 T_Bwd_6
v0 T__'8866'Nf'8902'__4
v1
= ((Any -> Any -> Any) -> Any -> T_Bwd_6 -> Any)
-> Any -> Any -> Any -> T__'8866'Nf'8902'__4
forall a b. a -> b
coe
(Any -> Any -> Any) -> Any -> T_Bwd_6 -> Any
MAlonzo.Code.Utils.List.du_bwd'45'foldr_26
((T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4)
-> Any
forall a b. a -> b
coe T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4
MAlonzo.Code.Type.BetaNormal.C__'8658'__16) (T__'8866'Nf'8902'__4 -> Any
forall a b. a -> b
coe T__'8866'Nf'8902'__4
v1) (T_Bwd_6 -> Any
forall a b. a -> b
coe T_Bwd_6
v0)
d_lemma'45'bwdfwdfunction''_356 ::
MAlonzo.Code.Type.T_Ctx'8902'_2 ->
MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
[MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4] ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_lemma'45'bwdfwdfunction''_356 :: T_Ctx'8902'_2
-> T__'8866'Nf'8902'__4 -> [T__'8866'Nf'8902'__4] -> T__'8801'__12
d_lemma'45'bwdfwdfunction''_356 = T_Ctx'8902'_2
-> T__'8866'Nf'8902'__4 -> [T__'8866'Nf'8902'__4] -> T__'8801'__12
forall a. a
erased
d_constr'45'cong_382 ::
MAlonzo.Code.Type.T_Ctx'8902'_2 ->
T_Ctx_2 ->
Integer ->
MAlonzo.Code.Data.Fin.Base.T_Fin_10 ->
MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
[MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4] ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Utils.List.T_IList_302 ->
MAlonzo.Code.Utils.List.T_IList_302 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_constr'45'cong_382 :: T_Ctx'8902'_2
-> T_Ctx_2
-> Integer
-> T_Fin_10
-> T_Vec_28
-> [T__'8866'Nf'8902'__4]
-> T__'8801'__12
-> T_IList_302
-> T_IList_302
-> T__'8801'__12
-> T__'8801'__12
d_constr'45'cong_382 = T_Ctx'8902'_2
-> T_Ctx_2
-> Integer
-> T_Fin_10
-> T_Vec_28
-> [T__'8866'Nf'8902'__4]
-> T__'8801'__12
-> T_IList_302
-> T_IList_302
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
d_constr'45'cong''_410 ::
MAlonzo.Code.Type.T_Ctx'8902'_2 ->
T_Ctx_2 ->
Integer ->
MAlonzo.Code.Data.Fin.Base.T_Fin_10 ->
MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
[MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4] ->
[MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4] ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Utils.List.T_IList_302 ->
MAlonzo.Code.Utils.List.T_IList_302 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_constr'45'cong''_410 :: T_Ctx'8902'_2
-> T_Ctx_2
-> Integer
-> T_Fin_10
-> T_Vec_28
-> [T__'8866'Nf'8902'__4]
-> [T__'8866'Nf'8902'__4]
-> T__'8801'__12
-> T__'8801'__12
-> T_IList_302
-> T_IList_302
-> T__'8801'__12
-> T__'8801'__12
d_constr'45'cong''_410 = T_Ctx'8902'_2
-> T_Ctx_2
-> Integer
-> T_Fin_10
-> T_Vec_28
-> [T__'8866'Nf'8902'__4]
-> [T__'8866'Nf'8902'__4]
-> T__'8801'__12
-> T__'8801'__12
-> T_IList_302
-> T_IList_302
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased