{-# 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.Declarative 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.Algorithmic
import qualified MAlonzo.Code.Builtin
import qualified MAlonzo.Code.Builtin.Signature
import qualified MAlonzo.Code.Data.Fin.Base
import qualified MAlonzo.Code.Data.Vec.Base
import qualified MAlonzo.Code.Type
import qualified MAlonzo.Code.Type.BetaNBE
import qualified MAlonzo.Code.Type.Equality
import qualified MAlonzo.Code.Type.RenamingSubstitution
import qualified MAlonzo.Code.Utils
import qualified MAlonzo.Code.Utils.List
d_mkTy_6 ::
Integer ->
Integer ->
MAlonzo.Code.Builtin.Signature.T__'47'_'8866''8902'_22 ->
MAlonzo.Code.Type.T__'8866''8902'__20
d_mkTy_6 :: Integer
-> Integer -> T__'47'_'8866''8902'_22 -> T__'8866''8902'__20
d_mkTy_6
= ((T_Ctx'8902'_2 -> T_Kind_476 -> Any -> Any)
-> (Integer -> Integer -> T_Kind_476 -> T__'8715''8902'__14 -> Any)
-> (T_Ctx'8902'_2 -> T_Kind_476 -> T_Kind_476 -> Any -> Any -> Any)
-> (T_Ctx'8902'_2 -> T_Kind_476 -> T_TyCon_6 -> Any)
-> (T_Ctx'8902'_2 -> Any -> Any)
-> Integer
-> Integer
-> T__'47'_'8866''8902'_22
-> Any)
-> Any
-> Any
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> (Any -> Any -> Any)
-> Integer
-> Integer
-> T__'47'_'8866''8902'_22
-> T__'8866''8902'__20
forall a b. a -> b
coe
(T_Ctx'8902'_2 -> T_Kind_476 -> Any -> Any)
-> (Integer -> Integer -> T_Kind_476 -> T__'8715''8902'__14 -> Any)
-> (T_Ctx'8902'_2 -> T_Kind_476 -> T_Kind_476 -> Any -> Any -> Any)
-> (T_Ctx'8902'_2 -> T_Kind_476 -> T_TyCon_6 -> Any)
-> (T_Ctx'8902'_2 -> Any -> Any)
-> Integer
-> Integer
-> T__'47'_'8866''8902'_22
-> Any
MAlonzo.Code.Builtin.Signature.du_mkTy_198 ((Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v0 Any
v1 Any
v2 -> Any
v2))
((Any -> Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v0 Any
v1 Any
v2 Any
v3 -> (T__'8715''8902'__14 -> T__'8866''8902'__20) -> Any -> Any
forall a b. a -> b
coe T__'8715''8902'__14 -> T__'8866''8902'__20
MAlonzo.Code.Type.C_'96'_22 Any
v3))
(\ Any
v0 Any
v1 Any
v2 Any
v3 Any
v4 -> (T_Kind_476
-> T__'8866''8902'__20
-> T__'8866''8902'__20
-> T__'8866''8902'__20)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe T_Kind_476
-> T__'8866''8902'__20
-> T__'8866''8902'__20
-> T__'8866''8902'__20
MAlonzo.Code.Type.C__'183'__30 Any
v1 Any
v3 Any
v4)
((Any -> Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v0 Any
v1 -> (T_TyCon_6 -> T__'8866''8902'__20) -> Any
forall a b. a -> b
coe T_TyCon_6 -> T__'8866''8902'__20
MAlonzo.Code.Type.C_'94'_34))
(\ Any
v0 Any
v1 -> (T__'8866''8902'__20 -> T__'8866''8902'__20) -> Any -> Any
forall a b. a -> b
coe T__'8866''8902'__20 -> T__'8866''8902'__20
MAlonzo.Code.Type.C_con_36 Any
v1)
d_sig2type_8 ::
MAlonzo.Code.Builtin.Signature.T_Sig_68 ->
MAlonzo.Code.Type.T__'8866''8902'__20
d_sig2type_8 :: T_Sig_68 -> T__'8866''8902'__20
d_sig2type_8
= ((T_Ctx'8902'_2 -> T_Kind_476 -> Any -> Any)
-> (Integer -> Integer -> T_Kind_476 -> T__'8715''8902'__14 -> Any)
-> (T_Ctx'8902'_2 -> T_Kind_476 -> T_Kind_476 -> Any -> Any -> Any)
-> (T_Ctx'8902'_2 -> T_Kind_476 -> T_TyCon_6 -> Any)
-> (T_Ctx'8902'_2 -> Any -> Any)
-> (T_Ctx'8902'_2 -> Any -> Any -> Any)
-> (T_Ctx'8902'_2 -> T_Kind_476 -> Any -> Any)
-> T_Sig_68
-> Any)
-> Any
-> Any
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> (Any -> Any -> Any)
-> (Any -> Any -> Any -> Any)
-> (Any -> Any -> Any -> Any)
-> T_Sig_68
-> T__'8866''8902'__20
forall a b. a -> b
coe
(T_Ctx'8902'_2 -> T_Kind_476 -> Any -> Any)
-> (Integer -> Integer -> T_Kind_476 -> T__'8715''8902'__14 -> Any)
-> (T_Ctx'8902'_2 -> T_Kind_476 -> T_Kind_476 -> Any -> Any -> Any)
-> (T_Ctx'8902'_2 -> T_Kind_476 -> T_TyCon_6 -> Any)
-> (T_Ctx'8902'_2 -> Any -> Any)
-> (T_Ctx'8902'_2 -> Any -> Any -> Any)
-> (T_Ctx'8902'_2 -> T_Kind_476 -> Any -> Any)
-> T_Sig_68
-> Any
MAlonzo.Code.Builtin.Signature.du_sig2type_236
((Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v0 Any
v1 Any
v2 -> Any
v2))
((Any -> Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v0 Any
v1 Any
v2 Any
v3 -> (T__'8715''8902'__14 -> T__'8866''8902'__20) -> Any -> Any
forall a b. a -> b
coe T__'8715''8902'__14 -> T__'8866''8902'__20
MAlonzo.Code.Type.C_'96'_22 Any
v3))
(\ Any
v0 Any
v1 Any
v2 Any
v3 Any
v4 -> (T_Kind_476
-> T__'8866''8902'__20
-> T__'8866''8902'__20
-> T__'8866''8902'__20)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe T_Kind_476
-> T__'8866''8902'__20
-> T__'8866''8902'__20
-> T__'8866''8902'__20
MAlonzo.Code.Type.C__'183'__30 Any
v1 Any
v3 Any
v4)
((Any -> Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v0 Any
v1 -> (T_TyCon_6 -> T__'8866''8902'__20) -> Any
forall a b. a -> b
coe T_TyCon_6 -> T__'8866''8902'__20
MAlonzo.Code.Type.C_'94'_34))
(\ Any
v0 Any
v1 -> (T__'8866''8902'__20 -> T__'8866''8902'__20) -> Any -> Any
forall a b. a -> b
coe T__'8866''8902'__20 -> T__'8866''8902'__20
MAlonzo.Code.Type.C_con_36 Any
v1)
(\ Any
v0 Any
v1 Any
v2 -> (T__'8866''8902'__20 -> T__'8866''8902'__20 -> T__'8866''8902'__20)
-> Any -> Any -> Any
forall a b. a -> b
coe T__'8866''8902'__20 -> T__'8866''8902'__20 -> T__'8866''8902'__20
MAlonzo.Code.Type.C__'8658'__26 Any
v1 Any
v2)
(\ Any
v0 Any
v1 Any
v2 -> (T_Kind_476 -> T__'8866''8902'__20 -> T__'8866''8902'__20)
-> Any -> Any -> Any
forall a b. a -> b
coe T_Kind_476 -> T__'8866''8902'__20 -> T__'8866''8902'__20
MAlonzo.Code.Type.C_Π_24 Any
v1 Any
v2)
d_sig2typeΠ_10 ::
Integer ->
Integer ->
MAlonzo.Code.Type.T__'8866''8902'__20 ->
MAlonzo.Code.Type.T__'8866''8902'__20
d_sig2typeΠ_10 :: Integer -> Integer -> T__'8866''8902'__20 -> T__'8866''8902'__20
d_sig2typeΠ_10
= ((T_Ctx'8902'_2 -> T_Kind_476 -> Any -> Any)
-> Integer -> Integer -> Any -> Any)
-> (Any -> Any -> Any -> Any)
-> Integer
-> Integer
-> T__'8866''8902'__20
-> T__'8866''8902'__20
forall a b. a -> b
coe
(T_Ctx'8902'_2 -> T_Kind_476 -> Any -> Any)
-> Integer -> Integer -> Any -> Any
MAlonzo.Code.Builtin.Signature.du_sig2typeΠ_222
(\ Any
v0 Any
v1 Any
v2 -> (T_Kind_476 -> T__'8866''8902'__20 -> T__'8866''8902'__20)
-> Any -> Any -> Any
forall a b. a -> b
coe T_Kind_476 -> T__'8866''8902'__20 -> T__'8866''8902'__20
MAlonzo.Code.Type.C_Π_24 Any
v1 Any
v2)
d_sig2type'8658'_12 ::
Integer ->
Integer ->
[MAlonzo.Code.Builtin.Signature.T__'47'_'8866''8902'_22] ->
MAlonzo.Code.Type.T__'8866''8902'__20 ->
MAlonzo.Code.Type.T__'8866''8902'__20
d_sig2type'8658'_12 :: Integer
-> Integer
-> [T__'47'_'8866''8902'_22]
-> T__'8866''8902'__20
-> T__'8866''8902'__20
d_sig2type'8658'_12
= ((T_Ctx'8902'_2 -> T_Kind_476 -> Any -> Any)
-> (Integer -> Integer -> T_Kind_476 -> T__'8715''8902'__14 -> Any)
-> (T_Ctx'8902'_2 -> T_Kind_476 -> T_Kind_476 -> Any -> Any -> Any)
-> (T_Ctx'8902'_2 -> T_Kind_476 -> T_TyCon_6 -> Any)
-> (T_Ctx'8902'_2 -> Any -> Any)
-> (T_Ctx'8902'_2 -> Any -> Any -> Any)
-> Integer
-> Integer
-> [T__'47'_'8866''8902'_22]
-> Any
-> Any)
-> Any
-> Any
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> (Any -> Any -> Any)
-> (Any -> Any -> Any -> Any)
-> Integer
-> Integer
-> [T__'47'_'8866''8902'_22]
-> T__'8866''8902'__20
-> T__'8866''8902'__20
forall a b. a -> b
coe
(T_Ctx'8902'_2 -> T_Kind_476 -> Any -> Any)
-> (Integer -> Integer -> T_Kind_476 -> T__'8715''8902'__14 -> Any)
-> (T_Ctx'8902'_2 -> T_Kind_476 -> T_Kind_476 -> Any -> Any -> Any)
-> (T_Ctx'8902'_2 -> T_Kind_476 -> T_TyCon_6 -> Any)
-> (T_Ctx'8902'_2 -> Any -> Any)
-> (T_Ctx'8902'_2 -> Any -> Any -> Any)
-> Integer
-> Integer
-> [T__'47'_'8866''8902'_22]
-> Any
-> Any
MAlonzo.Code.Builtin.Signature.du_sig2type'8658'_208
((Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v0 Any
v1 Any
v2 -> Any
v2))
((Any -> Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v0 Any
v1 Any
v2 Any
v3 -> (T__'8715''8902'__14 -> T__'8866''8902'__20) -> Any -> Any
forall a b. a -> b
coe T__'8715''8902'__14 -> T__'8866''8902'__20
MAlonzo.Code.Type.C_'96'_22 Any
v3))
(\ Any
v0 Any
v1 Any
v2 Any
v3 Any
v4 -> (T_Kind_476
-> T__'8866''8902'__20
-> T__'8866''8902'__20
-> T__'8866''8902'__20)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe T_Kind_476
-> T__'8866''8902'__20
-> T__'8866''8902'__20
-> T__'8866''8902'__20
MAlonzo.Code.Type.C__'183'__30 Any
v1 Any
v3 Any
v4)
((Any -> Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v0 Any
v1 -> (T_TyCon_6 -> T__'8866''8902'__20) -> Any
forall a b. a -> b
coe T_TyCon_6 -> T__'8866''8902'__20
MAlonzo.Code.Type.C_'94'_34))
(\ Any
v0 Any
v1 -> (T__'8866''8902'__20 -> T__'8866''8902'__20) -> Any -> Any
forall a b. a -> b
coe T__'8866''8902'__20 -> T__'8866''8902'__20
MAlonzo.Code.Type.C_con_36 Any
v1)
(\ Any
v0 Any
v1 Any
v2 -> (T__'8866''8902'__20 -> T__'8866''8902'__20 -> T__'8866''8902'__20)
-> Any -> Any -> Any
forall a b. a -> b
coe T__'8866''8902'__20 -> T__'8866''8902'__20 -> T__'8866''8902'__20
MAlonzo.Code.Type.C__'8658'__26 Any
v1 Any
v2)
d_'8866''9839'2TyNe'9839'_14 ::
Integer ->
Integer ->
MAlonzo.Code.Builtin.Signature.T__'8866''9839'_4 ->
MAlonzo.Code.Type.T__'8866''8902'__20
d_'8866''9839'2TyNe'9839'_14 :: Integer -> Integer -> T__'8866''9839'_4 -> T__'8866''8902'__20
d_'8866''9839'2TyNe'9839'_14
= ((T_Ctx'8902'_2 -> T_Kind_476 -> Any -> Any)
-> (Integer -> Integer -> T_Kind_476 -> T__'8715''8902'__14 -> Any)
-> (T_Ctx'8902'_2 -> T_Kind_476 -> T_Kind_476 -> Any -> Any -> Any)
-> (T_Ctx'8902'_2 -> T_Kind_476 -> T_TyCon_6 -> Any)
-> Integer
-> Integer
-> T__'8866''9839'_4
-> Any)
-> Any
-> Any
-> (Any -> Any -> Any -> Any -> Any -> Any)
-> Any
-> Integer
-> Integer
-> T__'8866''9839'_4
-> T__'8866''8902'__20
forall a b. a -> b
coe
(T_Ctx'8902'_2 -> T_Kind_476 -> Any -> Any)
-> (Integer -> Integer -> T_Kind_476 -> T__'8715''8902'__14 -> Any)
-> (T_Ctx'8902'_2 -> T_Kind_476 -> T_Kind_476 -> Any -> Any -> Any)
-> (T_Ctx'8902'_2 -> T_Kind_476 -> T_TyCon_6 -> Any)
-> Integer
-> Integer
-> T__'8866''9839'_4
-> Any
MAlonzo.Code.Builtin.Signature.du_'8866''9839'2TyNe'9839'_182
((Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v0 Any
v1 Any
v2 -> Any
v2))
((Any -> Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v0 Any
v1 Any
v2 Any
v3 -> (T__'8715''8902'__14 -> T__'8866''8902'__20) -> Any -> Any
forall a b. a -> b
coe T__'8715''8902'__14 -> T__'8866''8902'__20
MAlonzo.Code.Type.C_'96'_22 Any
v3))
(\ Any
v0 Any
v1 Any
v2 Any
v3 Any
v4 -> (T_Kind_476
-> T__'8866''8902'__20
-> T__'8866''8902'__20
-> T__'8866''8902'__20)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe T_Kind_476
-> T__'8866''8902'__20
-> T__'8866''8902'__20
-> T__'8866''8902'__20
MAlonzo.Code.Type.C__'183'__30 Any
v1 Any
v3 Any
v4)
((Any -> Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v0 Any
v1 -> (T_TyCon_6 -> T__'8866''8902'__20) -> Any
forall a b. a -> b
coe T_TyCon_6 -> T__'8866''8902'__20
MAlonzo.Code.Type.C_'94'_34))
d_Ctx_16 :: p -> ()
d_Ctx_16 p
a0 = ()
data T_Ctx_16
= C_'8709'_18 | C__'44''8902'__22 T_Ctx_16 |
C__'44'__26 T_Ctx_16 MAlonzo.Code.Type.T__'8866''8902'__20
d__'8715'__34 :: p -> p -> p -> ()
d__'8715'__34 p
a0 p
a1 p
a2 = ()
data T__'8715'__34
= C_Z_36 | C_S_38 T__'8715'__34 |
C_T_40 MAlonzo.Code.Type.T__'8866''8902'__20 T__'8715'__34
d_btype_42 ::
MAlonzo.Code.Type.T_Ctx'8902'_2 ->
MAlonzo.Code.Builtin.T_Builtin_2 ->
MAlonzo.Code.Type.T__'8866''8902'__20
d_btype_42 :: T_Ctx'8902'_2 -> T_Builtin_2 -> T__'8866''8902'__20
d_btype_42 T_Ctx'8902'_2
v0 T_Builtin_2
v1
= (T_Ctx'8902'_2
-> T_Kind_476 -> T__'8866''8902'__20 -> T__'8866''8902'__20)
-> Any -> Any -> Any -> T__'8866''8902'__20
forall a b. a -> b
coe
T_Ctx'8902'_2
-> T_Kind_476 -> T__'8866''8902'__20 -> T__'8866''8902'__20
MAlonzo.Code.Type.RenamingSubstitution.d_sub'8709'_896 (T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
v0)
(T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
MAlonzo.Code.Utils.C_'42'_478)
(((T_Ctx'8902'_2 -> T_Kind_476 -> Any -> Any)
-> (Integer -> Integer -> T_Kind_476 -> T__'8715''8902'__14 -> Any)
-> (T_Ctx'8902'_2 -> T_Kind_476 -> T_Kind_476 -> Any -> Any -> Any)
-> (T_Ctx'8902'_2 -> T_Kind_476 -> T_TyCon_6 -> Any)
-> (T_Ctx'8902'_2 -> Any -> Any)
-> (T_Ctx'8902'_2 -> Any -> Any -> Any)
-> (T_Ctx'8902'_2 -> T_Kind_476 -> Any -> Any)
-> T_Sig_68
-> Any)
-> Any
-> Any
-> (Any -> Any -> Any -> 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_476 -> Any -> Any)
-> (Integer -> Integer -> T_Kind_476 -> T__'8715''8902'__14 -> Any)
-> (T_Ctx'8902'_2 -> T_Kind_476 -> T_Kind_476 -> Any -> Any -> Any)
-> (T_Ctx'8902'_2 -> T_Kind_476 -> T_TyCon_6 -> Any)
-> (T_Ctx'8902'_2 -> Any -> Any)
-> (T_Ctx'8902'_2 -> Any -> Any -> Any)
-> (T_Ctx'8902'_2 -> T_Kind_476 -> Any -> Any)
-> T_Sig_68
-> Any
MAlonzo.Code.Builtin.Signature.du_sig2type_236
((Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v2 Any
v3 Any
v4 -> Any
v4))
((Any -> Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v2 Any
v3 Any
v4 Any
v5 -> (T__'8715''8902'__14 -> T__'8866''8902'__20) -> Any -> Any
forall a b. a -> b
coe T__'8715''8902'__14 -> T__'8866''8902'__20
MAlonzo.Code.Type.C_'96'_22 Any
v5))
(\ Any
v2 Any
v3 Any
v4 Any
v5 Any
v6 -> (T_Kind_476
-> T__'8866''8902'__20
-> T__'8866''8902'__20
-> T__'8866''8902'__20)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe T_Kind_476
-> T__'8866''8902'__20
-> T__'8866''8902'__20
-> T__'8866''8902'__20
MAlonzo.Code.Type.C__'183'__30 Any
v3 Any
v5 Any
v6)
((Any -> Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v2 Any
v3 -> (T_TyCon_6 -> T__'8866''8902'__20) -> Any
forall a b. a -> b
coe T_TyCon_6 -> T__'8866''8902'__20
MAlonzo.Code.Type.C_'94'_34))
(\ Any
v2 Any
v3 -> (T__'8866''8902'__20 -> T__'8866''8902'__20) -> Any -> Any
forall a b. a -> b
coe T__'8866''8902'__20 -> T__'8866''8902'__20
MAlonzo.Code.Type.C_con_36 Any
v3)
(\ Any
v2 Any
v3 Any
v4 -> (T__'8866''8902'__20 -> T__'8866''8902'__20 -> T__'8866''8902'__20)
-> Any -> Any -> Any
forall a b. a -> b
coe T__'8866''8902'__20 -> T__'8866''8902'__20 -> T__'8866''8902'__20
MAlonzo.Code.Type.C__'8658'__26 Any
v3 Any
v4)
(\ Any
v2 Any
v3 Any
v4 -> (T_Kind_476 -> T__'8866''8902'__20 -> T__'8866''8902'__20)
-> Any -> Any -> Any
forall a b. a -> b
coe T_Kind_476 -> T__'8866''8902'__20 -> T__'8866''8902'__20
MAlonzo.Code.Type.C_Π_24 Any
v3 Any
v4)
((T_Builtin_2 -> T_Sig_68) -> Any -> Any
forall a b. a -> b
coe T_Builtin_2 -> T_Sig_68
MAlonzo.Code.Builtin.d_signature_278 (T_Builtin_2 -> Any
forall a b. a -> b
coe T_Builtin_2
v1)))
d_btype'45'ren_50 ::
MAlonzo.Code.Type.T_Ctx'8902'_2 ->
MAlonzo.Code.Type.T_Ctx'8902'_2 ->
MAlonzo.Code.Builtin.T_Builtin_2 ->
(MAlonzo.Code.Utils.T_Kind_476 ->
MAlonzo.Code.Type.T__'8715''8902'__14 ->
MAlonzo.Code.Type.T__'8715''8902'__14) ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_btype'45'ren_50 :: T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> T_Builtin_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> T__'8801'__12
d_btype'45'ren_50 = T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> T_Builtin_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> T__'8801'__12
forall a. a
erased
d_btype'45'sub_60 ::
MAlonzo.Code.Type.T_Ctx'8902'_2 ->
MAlonzo.Code.Type.T_Ctx'8902'_2 ->
MAlonzo.Code.Builtin.T_Builtin_2 ->
(MAlonzo.Code.Utils.T_Kind_476 ->
MAlonzo.Code.Type.T__'8715''8902'__14 ->
MAlonzo.Code.Type.T__'8866''8902'__20) ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_btype'45'sub_60 :: T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> T_Builtin_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20)
-> T__'8801'__12
d_btype'45'sub_60 = T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> T_Builtin_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20)
-> T__'8801'__12
forall a. a
erased
d_'10214'_'10215'd_68 ::
MAlonzo.Code.Type.T__'8866''8902'__20 -> ()
d_'10214'_'10215'd_68 :: T__'8866''8902'__20 -> ()
d_'10214'_'10215'd_68 = T__'8866''8902'__20 -> ()
forall a. a
erased
d_ty2TyTag_74 ::
MAlonzo.Code.Type.T__'8866''8902'__20 ->
MAlonzo.Code.Builtin.Signature.T__'8866''9839'_4
d_ty2TyTag_74 :: T__'8866''8902'__20 -> T__'8866''9839'_4
d_ty2TyTag_74 T__'8866''8902'__20
v0
= (T__'8866'Nf'8902'__4 -> T__'8866''9839'_4)
-> Any -> T__'8866''9839'_4
forall a b. a -> b
coe
T__'8866'Nf'8902'__4 -> T__'8866''9839'_4
MAlonzo.Code.Algorithmic.d_ty2sty_64
((T_Ctx'8902'_2
-> T_Kind_476 -> T__'8866''8902'__20 -> T__'8866'Nf'8902'__4)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
T_Ctx'8902'_2
-> T_Kind_476 -> T__'8866''8902'__20 -> T__'8866'Nf'8902'__4
MAlonzo.Code.Type.BetaNBE.d_nf_258
(T_Ctx'8902'_2 -> Any
forall a b. a -> b
coe T_Ctx'8902'_2
MAlonzo.Code.Type.C_'8709'_4)
(T_Kind_476 -> Any
forall a b. a -> b
coe T_Kind_476
MAlonzo.Code.Utils.C_'9839'_480) (T__'8866''8902'__20 -> Any
forall a b. a -> b
coe T__'8866''8902'__20
v0))
d_mkCaseType_82 ::
MAlonzo.Code.Type.T_Ctx'8902'_2 ->
MAlonzo.Code.Type.T__'8866''8902'__20 ->
[MAlonzo.Code.Type.T__'8866''8902'__20] ->
MAlonzo.Code.Type.T__'8866''8902'__20
d_mkCaseType_82 :: T_Ctx'8902'_2
-> T__'8866''8902'__20
-> [T__'8866''8902'__20]
-> T__'8866''8902'__20
d_mkCaseType_82 ~T_Ctx'8902'_2
v0 T__'8866''8902'__20
v1 [T__'8866''8902'__20]
v2 = T__'8866''8902'__20 -> [T__'8866''8902'__20] -> T__'8866''8902'__20
du_mkCaseType_82 T__'8866''8902'__20
v1 [T__'8866''8902'__20]
v2
du_mkCaseType_82 ::
MAlonzo.Code.Type.T__'8866''8902'__20 ->
[MAlonzo.Code.Type.T__'8866''8902'__20] ->
MAlonzo.Code.Type.T__'8866''8902'__20
du_mkCaseType_82 :: T__'8866''8902'__20 -> [T__'8866''8902'__20] -> T__'8866''8902'__20
du_mkCaseType_82 T__'8866''8902'__20
v0 [T__'8866''8902'__20]
v1
= case [T__'8866''8902'__20] -> [Any]
forall a b. a -> b
coe [T__'8866''8902'__20]
v1 of
[] -> T__'8866''8902'__20 -> T__'8866''8902'__20
forall a b. a -> b
coe T__'8866''8902'__20
v0
(:) Any
v2 [Any]
v3
-> (T__'8866''8902'__20 -> T__'8866''8902'__20 -> T__'8866''8902'__20)
-> Any -> Any -> T__'8866''8902'__20
forall a b. a -> b
coe
T__'8866''8902'__20 -> T__'8866''8902'__20 -> T__'8866''8902'__20
MAlonzo.Code.Type.C__'8658'__26 Any
v2
((T__'8866''8902'__20
-> [T__'8866''8902'__20] -> T__'8866''8902'__20)
-> Any -> Any -> Any
forall a b. a -> b
coe T__'8866''8902'__20 -> [T__'8866''8902'__20] -> T__'8866''8902'__20
du_mkCaseType_82 (T__'8866''8902'__20 -> Any
forall a b. a -> b
coe T__'8866''8902'__20
v0) ([Any] -> Any
forall a b. a -> b
coe [Any]
v3))
[Any]
_ -> T__'8866''8902'__20
forall a. a
MAlonzo.RTE.mazUnreachableError
d_ConstrArgs_94 ::
MAlonzo.Code.Type.T_Ctx'8902'_2 ->
T_Ctx_16 -> [MAlonzo.Code.Type.T__'8866''8902'__20] -> ()
d_ConstrArgs_94 :: T_Ctx'8902'_2 -> T_Ctx_16 -> [T__'8866''8902'__20] -> ()
d_ConstrArgs_94 = T_Ctx'8902'_2 -> T_Ctx_16 -> [T__'8866''8902'__20] -> ()
forall a. a
erased
d_Cases_104 :: p -> p -> p -> p -> p -> ()
d_Cases_104 p
a0 p
a1 p
a2 p
a3 p
a4 = ()
data T_Cases_104
= C_'91''93'_180 | C__'8759'__192 T__'8866'__110 T_Cases_104
d__'8866'__110 :: p -> p -> p -> ()
d__'8866'__110 p
a0 p
a1 p
a2 = ()
data T__'8866'__110
= C_'96'_114 T__'8715'__34 | C_ƛ_116 T__'8866'__110 |
C__'183'__118 MAlonzo.Code.Type.T__'8866''8902'__20 T__'8866'__110
T__'8866'__110 |
C_Λ_120 T__'8866'__110 |
C__'183''8902'__124 MAlonzo.Code.Utils.T_Kind_476
MAlonzo.Code.Type.T__'8866''8902'__20 T__'8866'__110
MAlonzo.Code.Type.T__'8866''8902'__20 |
C_wrap_130 T__'8866'__110 | C_unwrap_132 T__'8866'__110 |
C_constr_142 MAlonzo.Code.Data.Fin.Base.T_Fin_6
[MAlonzo.Code.Type.T__'8866''8902'__20]
MAlonzo.Code.Utils.List.T_IList_302 |
C_case_154 Integer MAlonzo.Code.Data.Vec.Base.T_Vec_24
T__'8866'__110 T_Cases_104 |
C_conv_156 MAlonzo.Code.Type.T__'8866''8902'__20
MAlonzo.Code.Type.Equality.T__'8801'β__10 T__'8866'__110 |
C_con_162 MAlonzo.Code.Type.T__'8866''8902'__20 AgdaAny
MAlonzo.Code.Type.Equality.T__'8801'β__10 |
C_builtin_166 MAlonzo.Code.Builtin.T_Builtin_2 | C_error_170
d_conv'8715'_194 ::
MAlonzo.Code.Type.T_Ctx'8902'_2 ->
T_Ctx_16 ->
T_Ctx_16 ->
MAlonzo.Code.Type.T__'8866''8902'__20 ->
MAlonzo.Code.Type.T__'8866''8902'__20 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
T__'8715'__34 -> T__'8715'__34
d_conv'8715'_194 :: T_Ctx'8902'_2
-> T_Ctx_16
-> T_Ctx_16
-> T__'8866''8902'__20
-> T__'8866''8902'__20
-> T__'8801'__12
-> T__'8801'__12
-> T__'8715'__34
-> T__'8715'__34
d_conv'8715'_194 ~T_Ctx'8902'_2
v0 ~T_Ctx_16
v1 ~T_Ctx_16
v2 ~T__'8866''8902'__20
v3 ~T__'8866''8902'__20
v4 ~T__'8801'__12
v5 ~T__'8801'__12
v6 T__'8715'__34
v7
= T__'8715'__34 -> T__'8715'__34
du_conv'8715'_194 T__'8715'__34
v7
du_conv'8715'_194 :: T__'8715'__34 -> T__'8715'__34
du_conv'8715'_194 :: T__'8715'__34 -> T__'8715'__34
du_conv'8715'_194 T__'8715'__34
v0 = T__'8715'__34 -> T__'8715'__34
forall a b. a -> b
coe T__'8715'__34
v0
d_conv'8866'_198 ::
MAlonzo.Code.Type.T_Ctx'8902'_2 ->
T_Ctx_16 ->
T_Ctx_16 ->
MAlonzo.Code.Type.T__'8866''8902'__20 ->
MAlonzo.Code.Type.T__'8866''8902'__20 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
T__'8866'__110 -> T__'8866'__110
d_conv'8866'_198 :: T_Ctx'8902'_2
-> T_Ctx_16
-> T_Ctx_16
-> T__'8866''8902'__20
-> T__'8866''8902'__20
-> T__'8801'__12
-> T__'8801'__12
-> T__'8866'__110
-> T__'8866'__110
d_conv'8866'_198 ~T_Ctx'8902'_2
v0 ~T_Ctx_16
v1 ~T_Ctx_16
v2 ~T__'8866''8902'__20
v3 ~T__'8866''8902'__20
v4 ~T__'8801'__12
v5 ~T__'8801'__12
v6 T__'8866'__110
v7
= T__'8866'__110 -> T__'8866'__110
du_conv'8866'_198 T__'8866'__110
v7
du_conv'8866'_198 :: T__'8866'__110 -> T__'8866'__110
du_conv'8866'_198 :: T__'8866'__110 -> T__'8866'__110
du_conv'8866'_198 T__'8866'__110
v0 = T__'8866'__110 -> T__'8866'__110
forall a b. a -> b
coe T__'8866'__110
v0
d_typeOf_204 ::
MAlonzo.Code.Type.T_Ctx'8902'_2 ->
MAlonzo.Code.Type.T__'8866''8902'__20 ->
T_Ctx_16 -> T__'8866'__110 -> MAlonzo.Code.Type.T__'8866''8902'__20
d_typeOf_204 :: T_Ctx'8902'_2
-> T__'8866''8902'__20
-> T_Ctx_16
-> T__'8866'__110
-> T__'8866''8902'__20
d_typeOf_204 ~T_Ctx'8902'_2
v0 T__'8866''8902'__20
v1 ~T_Ctx_16
v2 ~T__'8866'__110
v3 = T__'8866''8902'__20 -> T__'8866''8902'__20
du_typeOf_204 T__'8866''8902'__20
v1
du_typeOf_204 ::
MAlonzo.Code.Type.T__'8866''8902'__20 ->
MAlonzo.Code.Type.T__'8866''8902'__20
du_typeOf_204 :: T__'8866''8902'__20 -> T__'8866''8902'__20
du_typeOf_204 T__'8866''8902'__20
v0 = T__'8866''8902'__20 -> T__'8866''8902'__20
forall a b. a -> b
coe T__'8866''8902'__20
v0
d_typeOf'8715'_210 ::
MAlonzo.Code.Type.T_Ctx'8902'_2 ->
MAlonzo.Code.Type.T__'8866''8902'__20 ->
T_Ctx_16 -> T__'8715'__34 -> MAlonzo.Code.Type.T__'8866''8902'__20
d_typeOf'8715'_210 :: T_Ctx'8902'_2
-> T__'8866''8902'__20
-> T_Ctx_16
-> T__'8715'__34
-> T__'8866''8902'__20
d_typeOf'8715'_210 ~T_Ctx'8902'_2
v0 T__'8866''8902'__20
v1 ~T_Ctx_16
v2 ~T__'8715'__34
v3 = T__'8866''8902'__20 -> T__'8866''8902'__20
du_typeOf'8715'_210 T__'8866''8902'__20
v1
du_typeOf'8715'_210 ::
MAlonzo.Code.Type.T__'8866''8902'__20 ->
MAlonzo.Code.Type.T__'8866''8902'__20
du_typeOf'8715'_210 :: T__'8866''8902'__20 -> T__'8866''8902'__20
du_typeOf'8715'_210 T__'8866''8902'__20
v0 = T__'8866''8902'__20 -> T__'8866''8902'__20
forall a b. a -> b
coe T__'8866''8902'__20
v0
d_piBody_216 ::
MAlonzo.Code.Type.T_Ctx'8902'_2 ->
MAlonzo.Code.Utils.T_Kind_476 ->
T_Ctx_16 ->
MAlonzo.Code.Type.T__'8866''8902'__20 ->
T__'8866'__110 -> MAlonzo.Code.Type.T__'8866''8902'__20
d_piBody_216 :: T_Ctx'8902'_2
-> T_Kind_476
-> T_Ctx_16
-> T__'8866''8902'__20
-> T__'8866'__110
-> T__'8866''8902'__20
d_piBody_216 ~T_Ctx'8902'_2
v0 ~T_Kind_476
v1 ~T_Ctx_16
v2 T__'8866''8902'__20
v3 ~T__'8866'__110
v4 = T__'8866''8902'__20 -> T__'8866''8902'__20
du_piBody_216 T__'8866''8902'__20
v3
du_piBody_216 ::
MAlonzo.Code.Type.T__'8866''8902'__20 ->
MAlonzo.Code.Type.T__'8866''8902'__20
du_piBody_216 :: T__'8866''8902'__20 -> T__'8866''8902'__20
du_piBody_216 T__'8866''8902'__20
v0 = T__'8866''8902'__20 -> T__'8866''8902'__20
forall a b. a -> b
coe T__'8866''8902'__20
v0
d_muPat_222 ::
MAlonzo.Code.Type.T_Ctx'8902'_2 ->
MAlonzo.Code.Utils.T_Kind_476 ->
T_Ctx_16 ->
MAlonzo.Code.Type.T__'8866''8902'__20 ->
MAlonzo.Code.Type.T__'8866''8902'__20 ->
T__'8866'__110 -> MAlonzo.Code.Type.T__'8866''8902'__20
d_muPat_222 :: T_Ctx'8902'_2
-> T_Kind_476
-> T_Ctx_16
-> T__'8866''8902'__20
-> T__'8866''8902'__20
-> T__'8866'__110
-> T__'8866''8902'__20
d_muPat_222 ~T_Ctx'8902'_2
v0 ~T_Kind_476
v1 ~T_Ctx_16
v2 ~T__'8866''8902'__20
v3 T__'8866''8902'__20
v4 ~T__'8866'__110
v5 = T__'8866''8902'__20 -> T__'8866''8902'__20
du_muPat_222 T__'8866''8902'__20
v4
du_muPat_222 ::
MAlonzo.Code.Type.T__'8866''8902'__20 ->
MAlonzo.Code.Type.T__'8866''8902'__20
du_muPat_222 :: T__'8866''8902'__20 -> T__'8866''8902'__20
du_muPat_222 T__'8866''8902'__20
v0 = T__'8866''8902'__20 -> T__'8866''8902'__20
forall a b. a -> b
coe T__'8866''8902'__20
v0
d_muArg_228 ::
MAlonzo.Code.Type.T_Ctx'8902'_2 ->
MAlonzo.Code.Utils.T_Kind_476 ->
T_Ctx_16 ->
MAlonzo.Code.Type.T__'8866''8902'__20 ->
MAlonzo.Code.Type.T__'8866''8902'__20 ->
T__'8866'__110 -> MAlonzo.Code.Type.T__'8866''8902'__20
d_muArg_228 :: T_Ctx'8902'_2
-> T_Kind_476
-> T_Ctx_16
-> T__'8866''8902'__20
-> T__'8866''8902'__20
-> T__'8866'__110
-> T__'8866''8902'__20
d_muArg_228 ~T_Ctx'8902'_2
v0 ~T_Kind_476
v1 ~T_Ctx_16
v2 ~T__'8866''8902'__20
v3 T__'8866''8902'__20
v4 ~T__'8866'__110
v5 = T__'8866''8902'__20 -> T__'8866''8902'__20
du_muArg_228 T__'8866''8902'__20
v4
du_muArg_228 ::
MAlonzo.Code.Type.T__'8866''8902'__20 ->
MAlonzo.Code.Type.T__'8866''8902'__20
du_muArg_228 :: T__'8866''8902'__20 -> T__'8866''8902'__20
du_muArg_228 T__'8866''8902'__20
v0 = T__'8866''8902'__20 -> T__'8866''8902'__20
forall a b. a -> b
coe T__'8866''8902'__20
v0