{-# 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.Raw 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.String
import qualified MAlonzo.Code.Builtin
import qualified MAlonzo.Code.Builtin.Constant.AtomicType
import qualified MAlonzo.Code.Data.Bool.Base
import qualified MAlonzo.Code.Data.Integer.Show
import qualified MAlonzo.Code.Data.Nat.Properties
import qualified MAlonzo.Code.Data.String.Base
import qualified MAlonzo.Code.RawU
import qualified MAlonzo.Code.Relation.Nullary.Decidable.Core
import qualified MAlonzo.Code.Utils
import Raw
d_RawTy_2 :: ()
d_RawTy_2 = ()
type T_RawTy_2 = RType
pattern $mC_'96'_6 :: forall {r}. RType -> (Integer -> r) -> ((# #) -> r) -> r
$bC_'96'_6 :: Integer -> RType
C_'96'_6 a0 = RTyVar a0
pattern $mC__'8658'__8 :: forall {r}. RType -> (RType -> RType -> r) -> ((# #) -> r) -> r
$bC__'8658'__8 :: RType -> RType -> RType
C__'8658'__8 a0 a1 = RTyFun a0 a1
pattern $mC_Π_10 :: forall {r}. RType -> (KIND -> RType -> r) -> ((# #) -> r) -> r
$bC_Π_10 :: KIND -> RType -> RType
C_Π_10 a0 a1 = RTyPi a0 a1
pattern $mC_ƛ_12 :: forall {r}. RType -> (KIND -> RType -> r) -> ((# #) -> r) -> r
$bC_ƛ_12 :: KIND -> RType -> RType
C_ƛ_12 a0 a1 = RTyLambda a0 a1
pattern $mC__'183'__14 :: forall {r}. RType -> (RType -> RType -> r) -> ((# #) -> r) -> r
$bC__'183'__14 :: RType -> RType -> RType
C__'183'__14 a0 a1 = RTyApp a0 a1
pattern $mC_con_16 :: forall {r}. RType -> (RTyCon -> r) -> ((# #) -> r) -> r
$bC_con_16 :: RTyCon -> RType
C_con_16 a0 = RTyCon a0
pattern $mC_μ_18 :: forall {r}. RType -> (RType -> RType -> r) -> ((# #) -> r) -> r
$bC_μ_18 :: RType -> RType -> RType
C_μ_18 a0 a1 = RTyMu a0 a1
pattern $mC_SOP_22 :: forall {r}. RType -> ([[RType]] -> r) -> ((# #) -> r) -> r
$bC_SOP_22 :: [[RType]] -> RType
C_SOP_22 a0 = RTySOP a0
check_'96'_6 :: Integer -> T_RawTy_2
check_'96'_6 :: Integer -> RType
check_'96'_6 = Integer -> RType
RTyVar
check__'8658'__8 :: T_RawTy_2 -> T_RawTy_2 -> T_RawTy_2
check__'8658'__8 :: RType -> RType -> RType
check__'8658'__8 = RType -> RType -> RType
RTyFun
check_Π_10 ::
MAlonzo.Code.Utils.T_Kind_476 -> T_RawTy_2 -> T_RawTy_2
check_Π_10 :: KIND -> RType -> RType
check_Π_10 = KIND -> RType -> RType
RTyPi
check_ƛ_12 ::
MAlonzo.Code.Utils.T_Kind_476 -> T_RawTy_2 -> T_RawTy_2
check_ƛ_12 :: KIND -> RType -> RType
check_ƛ_12 = KIND -> RType -> RType
RTyLambda
check__'183'__14 :: T_RawTy_2 -> T_RawTy_2 -> T_RawTy_2
check__'183'__14 :: RType -> RType -> RType
check__'183'__14 = RType -> RType -> RType
RTyApp
check_con_16 :: T_RawTyCon_4 -> T_RawTy_2
check_con_16 :: RTyCon -> RType
check_con_16 = RTyCon -> RType
RTyCon
check_μ_18 :: T_RawTy_2 -> T_RawTy_2 -> T_RawTy_2
check_μ_18 :: RType -> RType -> RType
check_μ_18 = RType -> RType -> RType
RTyMu
check_SOP_22 ::
MAlonzo.Code.Utils.T_List_382
(MAlonzo.Code.Utils.T_List_382 T_RawTy_2) ->
T_RawTy_2
check_SOP_22 :: [[RType]] -> RType
check_SOP_22 = [[RType]] -> RType
RTySOP
cover_RawTy_2 :: RType -> ()
cover_RawTy_2 :: RType -> ()
cover_RawTy_2 RType
x
= case RType
x of
RTyVar Integer
_ -> ()
RTyFun RType
_ RType
_ -> ()
RTyPi KIND
_ RType
_ -> ()
RTyLambda KIND
_ RType
_ -> ()
RTyApp RType
_ RType
_ -> ()
RTyCon RTyCon
_ -> ()
RTyMu RType
_ RType
_ -> ()
RTySOP [[RType]]
_ -> ()
d_RawTyCon_4 :: ()
d_RawTyCon_4 = ()
type T_RawTyCon_4 = RTyCon
pattern $mC_atomic_24 :: forall {r}. RTyCon -> (AtomicTyCon -> r) -> ((# #) -> r) -> r
$bC_atomic_24 :: AtomicTyCon -> RTyCon
C_atomic_24 a0 = RTyConAtom a0
pattern $mC_list_26 :: forall {r}. RTyCon -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_list_26 :: RTyCon
C_list_26 = RTyConList
pattern $mC_pair_28 :: forall {r}. RTyCon -> ((# #) -> r) -> ((# #) -> r) -> r
$bC_pair_28 :: RTyCon
C_pair_28 = RTyConPair
check_atomic_24 ::
MAlonzo.Code.Builtin.Constant.AtomicType.T_AtomicTyCon_6 ->
T_RawTyCon_4
check_atomic_24 :: AtomicTyCon -> RTyCon
check_atomic_24 = AtomicTyCon -> RTyCon
RTyConAtom
check_list_26 :: T_RawTyCon_4
check_list_26 :: RTyCon
check_list_26 = RTyCon
RTyConList
check_pair_28 :: T_RawTyCon_4
check_pair_28 :: RTyCon
check_pair_28 = RTyCon
RTyConPair
cover_RawTyCon_4 :: RTyCon -> ()
cover_RawTyCon_4 :: RTyCon -> ()
cover_RawTyCon_4 RTyCon
x
= case RTyCon
x of
RTyConAtom AtomicTyCon
_ -> ()
RTyCon
RTyConList -> ()
RTyCon
RTyConPair -> ()
d_RawTm_30 :: ()
d_RawTm_30 = ()
type T_RawTm_30 = RTerm
pattern $mC_'96'_32 :: forall {r}. RTerm -> (Integer -> r) -> ((# #) -> r) -> r
$bC_'96'_32 :: Integer -> RTerm
C_'96'_32 a0 = RVar a0
pattern $mC_Λ_34 :: forall {r}. RTerm -> (KIND -> RTerm -> r) -> ((# #) -> r) -> r
$bC_Λ_34 :: KIND -> RTerm -> RTerm
C_Λ_34 a0 a1 = RTLambda a0 a1
pattern $mC__'183''8902'__36 :: forall {r}. RTerm -> (RTerm -> RType -> r) -> ((# #) -> r) -> r
$bC__'183''8902'__36 :: RTerm -> RType -> RTerm
C__'183''8902'__36 a0 a1 = RTApp a0 a1
pattern $mC_ƛ_38 :: forall {r}. RTerm -> (RType -> RTerm -> r) -> ((# #) -> r) -> r
$bC_ƛ_38 :: RType -> RTerm -> RTerm
C_ƛ_38 a0 a1 = RLambda a0 a1
pattern $mC__'183'__40 :: forall {r}. RTerm -> (RTerm -> RTerm -> r) -> ((# #) -> r) -> r
$bC__'183'__40 :: RTerm -> RTerm -> RTerm
C__'183'__40 a0 a1 = RApp a0 a1
pattern $mC_con_42 :: forall {r}.
RTerm -> (Some (ValueOf DefaultUni) -> r) -> ((# #) -> r) -> r
$bC_con_42 :: Some (ValueOf DefaultUni) -> RTerm
C_con_42 a0 = RCon a0
pattern $mC_error_44 :: forall {r}. RTerm -> (RType -> r) -> ((# #) -> r) -> r
$bC_error_44 :: RType -> RTerm
C_error_44 a0 = RError a0
pattern $mC_builtin_46 :: forall {r}. RTerm -> (DefaultFun -> r) -> ((# #) -> r) -> r
$bC_builtin_46 :: DefaultFun -> RTerm
C_builtin_46 a0 = RBuiltin a0
pattern $mC_wrap_48 :: forall {r}.
RTerm -> (RType -> RType -> RTerm -> r) -> ((# #) -> r) -> r
$bC_wrap_48 :: RType -> RType -> RTerm -> RTerm
C_wrap_48 a0 a1 a2 = RWrap a0 a1 a2
pattern $mC_unwrap_50 :: forall {r}. RTerm -> (RTerm -> r) -> ((# #) -> r) -> r
$bC_unwrap_50 :: RTerm -> RTerm
C_unwrap_50 a0 = RUnWrap a0
pattern $mC_constr_58 :: forall {r}.
RTerm -> (RType -> Integer -> [RTerm] -> r) -> ((# #) -> r) -> r
$bC_constr_58 :: RType -> Integer -> [RTerm] -> RTerm
C_constr_58 a0 a1 a2 = RConstr a0 a1 a2
pattern $mC_case_66 :: forall {r}.
RTerm -> (RType -> RTerm -> [RTerm] -> r) -> ((# #) -> r) -> r
$bC_case_66 :: RType -> RTerm -> [RTerm] -> RTerm
C_case_66 a0 a1 a2 = RCase a0 a1 a2
check_'96'_32 :: Integer -> T_RawTm_30
check_'96'_32 :: Integer -> RTerm
check_'96'_32 = Integer -> RTerm
RVar
check_Λ_34 ::
MAlonzo.Code.Utils.T_Kind_476 -> T_RawTm_30 -> T_RawTm_30
check_Λ_34 :: KIND -> RTerm -> RTerm
check_Λ_34 = KIND -> RTerm -> RTerm
RTLambda
check__'183''8902'__36 :: T_RawTm_30 -> T_RawTy_2 -> T_RawTm_30
check__'183''8902'__36 :: RTerm -> RType -> RTerm
check__'183''8902'__36 = RTerm -> RType -> RTerm
RTApp
check_ƛ_38 :: T_RawTy_2 -> T_RawTm_30 -> T_RawTm_30
check_ƛ_38 :: RType -> RTerm -> RTerm
check_ƛ_38 = RType -> RTerm -> RTerm
RLambda
check__'183'__40 :: T_RawTm_30 -> T_RawTm_30 -> T_RawTm_30
check__'183'__40 :: RTerm -> RTerm -> RTerm
check__'183'__40 = RTerm -> RTerm -> RTerm
RApp
check_con_42 :: MAlonzo.Code.RawU.T_TagCon_58 -> T_RawTm_30
check_con_42 :: Some (ValueOf DefaultUni) -> RTerm
check_con_42 = Some (ValueOf DefaultUni) -> RTerm
RCon
check_error_44 :: T_RawTy_2 -> T_RawTm_30
check_error_44 :: RType -> RTerm
check_error_44 = RType -> RTerm
RError
check_builtin_46 :: MAlonzo.Code.Builtin.T_Builtin_2 -> T_RawTm_30
check_builtin_46 :: DefaultFun -> RTerm
check_builtin_46 = DefaultFun -> RTerm
RBuiltin
check_wrap_48 :: T_RawTy_2 -> T_RawTy_2 -> T_RawTm_30 -> T_RawTm_30
check_wrap_48 :: RType -> RType -> RTerm -> RTerm
check_wrap_48 = RType -> RType -> RTerm -> RTerm
RWrap
check_unwrap_50 :: T_RawTm_30 -> T_RawTm_30
check_unwrap_50 :: RTerm -> RTerm
check_unwrap_50 = RTerm -> RTerm
RUnWrap
check_constr_58 ::
T_RawTy_2 ->
Integer -> MAlonzo.Code.Utils.T_List_382 T_RawTm_30 -> T_RawTm_30
check_constr_58 :: RType -> Integer -> [RTerm] -> RTerm
check_constr_58 = RType -> Integer -> [RTerm] -> RTerm
RConstr
check_case_66 ::
T_RawTy_2 ->
T_RawTm_30 ->
MAlonzo.Code.Utils.T_List_382 T_RawTm_30 -> T_RawTm_30
check_case_66 :: RType -> RTerm -> [RTerm] -> RTerm
check_case_66 = RType -> RTerm -> [RTerm] -> RTerm
RCase
cover_RawTm_30 :: RTerm -> ()
cover_RawTm_30 :: RTerm -> ()
cover_RawTm_30 RTerm
x
= case RTerm
x of
RVar Integer
_ -> ()
RTLambda KIND
_ RTerm
_ -> ()
RTApp RTerm
_ RType
_ -> ()
RLambda RType
_ RTerm
_ -> ()
RApp RTerm
_ RTerm
_ -> ()
RCon Some (ValueOf DefaultUni)
_ -> ()
RError RType
_ -> ()
RBuiltin DefaultFun
_ -> ()
RWrap RType
_ RType
_ RTerm
_ -> ()
RUnWrap RTerm
_ -> ()
RConstr RType
_ Integer
_ [RTerm]
_ -> ()
RCase RType
_ RTerm
_ [RTerm]
_ -> ()
d_decRTyCon_72 :: T_RawTyCon_4 -> T_RawTyCon_4 -> Bool
d_decRTyCon_72 :: RTyCon -> RTyCon -> Bool
d_decRTyCon_72 RTyCon
v0 RTyCon
v1
= let v2 :: b
v2 = Bool -> b
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8 in
Any -> Bool
forall a b. a -> b
coe
(case RTyCon -> RTyCon
forall a b. a -> b
coe RTyCon
v0 of
C_atomic_24 AtomicTyCon
v3
-> case RTyCon -> RTyCon
forall a b. a -> b
coe RTyCon
v1 of
C_atomic_24 AtomicTyCon
v4
-> (T_Dec_20 -> Bool) -> Any -> Any
forall a b. a -> b
coe
T_Dec_20 -> Bool
MAlonzo.Code.Relation.Nullary.Decidable.Core.d_does_28
((AtomicTyCon -> AtomicTyCon -> T_Dec_20) -> Any -> Any -> Any
forall a b. a -> b
coe
AtomicTyCon -> AtomicTyCon -> T_Dec_20
MAlonzo.Code.Builtin.Constant.AtomicType.d_decAtomicTyCon_26
(AtomicTyCon -> Any
forall a b. a -> b
coe AtomicTyCon
v3) (AtomicTyCon -> Any
forall a b. a -> b
coe AtomicTyCon
v4))
RTyCon
_ -> Any -> Any
forall a b. a -> b
coe Any
forall {b}. b
v2
RTyCon
C_list_26
-> case RTyCon -> RTyCon
forall a b. a -> b
coe RTyCon
v1 of
RTyCon
C_list_26 -> Bool -> Any
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10
RTyCon
_ -> Any -> Any
forall a b. a -> b
coe Any
forall {b}. b
v2
RTyCon
C_pair_28
-> case RTyCon -> RTyCon
forall a b. a -> b
coe RTyCon
v1 of
RTyCon
C_pair_28 -> Bool -> Any
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10
RTyCon
_ -> Any -> Any
forall a b. a -> b
coe Any
forall {b}. b
v2
RTyCon
_ -> Any
forall {b}. b
MAlonzo.RTE.mazUnreachableError)
d_decRKi_82 ::
MAlonzo.Code.Utils.T_Kind_476 ->
MAlonzo.Code.Utils.T_Kind_476 -> Bool
d_decRKi_82 :: KIND -> KIND -> Bool
d_decRKi_82 KIND
v0 KIND
v1
= case KIND -> KIND
forall a b. a -> b
coe KIND
v0 of
KIND
MAlonzo.Code.Utils.C_'42'_478
-> let v2 :: b
v2 = Bool -> b
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8 in
Any -> Bool
forall a b. a -> b
coe
(case KIND -> KIND
forall a b. a -> b
coe KIND
v1 of
KIND
MAlonzo.Code.Utils.C_'42'_478
-> Bool -> Any
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10
KIND
_ -> Any -> Any
forall a b. a -> b
coe Any
forall {b}. b
v2)
KIND
MAlonzo.Code.Utils.C_'9839'_480
-> let v2 :: b
v2 = Bool -> b
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8 in
Any -> Bool
forall a b. a -> b
coe
(case KIND -> KIND
forall a b. a -> b
coe KIND
v1 of
KIND
MAlonzo.Code.Utils.C_'9839'_480
-> Bool -> Any
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10
KIND
_ -> Any -> Any
forall a b. a -> b
coe Any
forall {b}. b
v2)
MAlonzo.Code.Utils.C__'8658'__482 KIND
v2 KIND
v3
-> let v4 :: b
v4 = Bool -> b
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8 in
Any -> Bool
forall a b. a -> b
coe
(case KIND -> KIND
forall a b. a -> b
coe KIND
v1 of
MAlonzo.Code.Utils.C__'8658'__482 KIND
v5 KIND
v6
-> (Bool -> Bool -> Bool) -> Any -> Any -> Any
forall a b. a -> b
coe
Bool -> Bool -> Bool
MAlonzo.Code.Data.Bool.Base.d__'8743'__24
((KIND -> KIND -> Bool) -> Any -> Any -> Any
forall a b. a -> b
coe KIND -> KIND -> Bool
d_decRKi_82 (KIND -> Any
forall a b. a -> b
coe KIND
v2) (KIND -> Any
forall a b. a -> b
coe KIND
v5))
((KIND -> KIND -> Bool) -> Any -> Any -> Any
forall a b. a -> b
coe KIND -> KIND -> Bool
d_decRKi_82 (KIND -> Any
forall a b. a -> b
coe KIND
v3) (KIND -> Any
forall a b. a -> b
coe KIND
v6))
KIND
_ -> Any -> Any
forall a b. a -> b
coe Any
forall {b}. b
v4)
KIND
_ -> Bool
forall {b}. b
MAlonzo.RTE.mazUnreachableError
d_decRTy_100 :: T_RawTy_2 -> T_RawTy_2 -> Bool
d_decRTy_100 :: RType -> RType -> Bool
d_decRTy_100 RType
v0 RType
v1
= let v2 :: b
v2 = Bool -> b
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8 in
Any -> Bool
forall a b. a -> b
coe
(case RType -> RType
forall a b. a -> b
coe RType
v0 of
C_'96'_6 Integer
v3
-> case RType -> RType
forall a b. a -> b
coe RType
v1 of
C_'96'_6 Integer
v4
-> (T_Dec_20 -> Bool) -> Any -> Any
forall a b. a -> b
coe
T_Dec_20 -> Bool
MAlonzo.Code.Relation.Nullary.Decidable.Core.d_does_28
((Integer -> Integer -> T_Dec_20) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> T_Dec_20
MAlonzo.Code.Data.Nat.Properties.d__'8799'__2688 (Integer -> Any
forall a b. a -> b
coe Integer
v3) (Integer -> Any
forall a b. a -> b
coe Integer
v4))
RType
_ -> Any -> Any
forall a b. a -> b
coe Any
forall {b}. b
v2
C__'8658'__8 RType
v3 RType
v4
-> case RType -> RType
forall a b. a -> b
coe RType
v1 of
C__'8658'__8 RType
v5 RType
v6
-> (Bool -> Bool -> Bool) -> Any -> Any -> Any
forall a b. a -> b
coe
Bool -> Bool -> Bool
MAlonzo.Code.Data.Bool.Base.d__'8743'__24
((RType -> RType -> Bool) -> Any -> Any -> Any
forall a b. a -> b
coe RType -> RType -> Bool
d_decRTy_100 (RType -> Any
forall a b. a -> b
coe RType
v3) (RType -> Any
forall a b. a -> b
coe RType
v5))
((RType -> RType -> Bool) -> Any -> Any -> Any
forall a b. a -> b
coe RType -> RType -> Bool
d_decRTy_100 (RType -> Any
forall a b. a -> b
coe RType
v4) (RType -> Any
forall a b. a -> b
coe RType
v6))
RType
_ -> Any -> Any
forall a b. a -> b
coe Any
forall {b}. b
v2
C_Π_10 KIND
v3 RType
v4
-> case RType -> RType
forall a b. a -> b
coe RType
v1 of
C_Π_10 KIND
v5 RType
v6
-> (Bool -> Bool -> Bool) -> Any -> Any -> Any
forall a b. a -> b
coe
Bool -> Bool -> Bool
MAlonzo.Code.Data.Bool.Base.d__'8743'__24
((KIND -> KIND -> Bool) -> Any -> Any -> Any
forall a b. a -> b
coe KIND -> KIND -> Bool
d_decRKi_82 (KIND -> Any
forall a b. a -> b
coe KIND
v3) (KIND -> Any
forall a b. a -> b
coe KIND
v5))
((RType -> RType -> Bool) -> Any -> Any -> Any
forall a b. a -> b
coe RType -> RType -> Bool
d_decRTy_100 (RType -> Any
forall a b. a -> b
coe RType
v4) (RType -> Any
forall a b. a -> b
coe RType
v6))
RType
_ -> Any -> Any
forall a b. a -> b
coe Any
forall {b}. b
v2
C_ƛ_12 KIND
v3 RType
v4
-> case RType -> RType
forall a b. a -> b
coe RType
v1 of
C_ƛ_12 KIND
v5 RType
v6
-> (Bool -> Bool -> Bool) -> Any -> Any -> Any
forall a b. a -> b
coe
Bool -> Bool -> Bool
MAlonzo.Code.Data.Bool.Base.d__'8743'__24
((KIND -> KIND -> Bool) -> Any -> Any -> Any
forall a b. a -> b
coe KIND -> KIND -> Bool
d_decRKi_82 (KIND -> Any
forall a b. a -> b
coe KIND
v3) (KIND -> Any
forall a b. a -> b
coe KIND
v5))
((RType -> RType -> Bool) -> Any -> Any -> Any
forall a b. a -> b
coe RType -> RType -> Bool
d_decRTy_100 (RType -> Any
forall a b. a -> b
coe RType
v4) (RType -> Any
forall a b. a -> b
coe RType
v6))
RType
_ -> Any -> Any
forall a b. a -> b
coe Any
forall {b}. b
v2
C__'183'__14 RType
v3 RType
v4
-> case RType -> RType
forall a b. a -> b
coe RType
v1 of
C__'183'__14 RType
v5 RType
v6
-> (Bool -> Bool -> Bool) -> Any -> Any -> Any
forall a b. a -> b
coe
Bool -> Bool -> Bool
MAlonzo.Code.Data.Bool.Base.d__'8743'__24
((RType -> RType -> Bool) -> Any -> Any -> Any
forall a b. a -> b
coe RType -> RType -> Bool
d_decRTy_100 (RType -> Any
forall a b. a -> b
coe RType
v3) (RType -> Any
forall a b. a -> b
coe RType
v5))
((RType -> RType -> Bool) -> Any -> Any -> Any
forall a b. a -> b
coe RType -> RType -> Bool
d_decRTy_100 (RType -> Any
forall a b. a -> b
coe RType
v4) (RType -> Any
forall a b. a -> b
coe RType
v6))
RType
_ -> Any -> Any
forall a b. a -> b
coe Any
forall {b}. b
v2
C_con_16 RTyCon
v3
-> case RType -> RType
forall a b. a -> b
coe RType
v1 of
C_con_16 RTyCon
v4 -> (RTyCon -> RTyCon -> Bool) -> Any -> Any -> Any
forall a b. a -> b
coe RTyCon -> RTyCon -> Bool
d_decRTyCon_72 (RTyCon -> Any
forall a b. a -> b
coe RTyCon
v3) (RTyCon -> Any
forall a b. a -> b
coe RTyCon
v4)
RType
_ -> Any -> Any
forall a b. a -> b
coe Any
forall {b}. b
v2
C_μ_18 RType
v3 RType
v4
-> case RType -> RType
forall a b. a -> b
coe RType
v1 of
C_μ_18 RType
v5 RType
v6
-> (Bool -> Bool -> Bool) -> Any -> Any -> Any
forall a b. a -> b
coe
Bool -> Bool -> Bool
MAlonzo.Code.Data.Bool.Base.d__'8743'__24
((RType -> RType -> Bool) -> Any -> Any -> Any
forall a b. a -> b
coe RType -> RType -> Bool
d_decRTy_100 (RType -> Any
forall a b. a -> b
coe RType
v3) (RType -> Any
forall a b. a -> b
coe RType
v5))
((RType -> RType -> Bool) -> Any -> Any -> Any
forall a b. a -> b
coe RType -> RType -> Bool
d_decRTy_100 (RType -> Any
forall a b. a -> b
coe RType
v4) (RType -> Any
forall a b. a -> b
coe RType
v6))
RType
_ -> Any -> Any
forall a b. a -> b
coe Any
forall {b}. b
v2
C_SOP_22 [[RType]]
v3
-> case RType -> RType
forall a b. a -> b
coe RType
v1 of
C_SOP_22 [[RType]]
v4 -> ([[RType]] -> [[RType]] -> Bool) -> Any -> Any -> Any
forall a b. a -> b
coe [[RType]] -> [[RType]] -> Bool
d_decRTyListList_112 ([[RType]] -> Any
forall a b. a -> b
coe [[RType]]
v3) ([[RType]] -> Any
forall a b. a -> b
coe [[RType]]
v4)
RType
_ -> Any -> Any
forall a b. a -> b
coe Any
forall {b}. b
v2
RType
_ -> Any
forall {b}. b
MAlonzo.RTE.mazUnreachableError)
d_decRTyList_106 ::
MAlonzo.Code.Utils.T_List_382 T_RawTy_2 ->
MAlonzo.Code.Utils.T_List_382 T_RawTy_2 -> Bool
d_decRTyList_106 :: [RType] -> [RType] -> Bool
d_decRTyList_106 [RType]
v0 [RType]
v1
= let v2 :: b
v2 = Bool -> b
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8 in
Any -> Bool
forall a b. a -> b
coe
(case [RType] -> [Any]
forall a b. a -> b
coe [RType]
v0 of
[Any]
MAlonzo.Code.Utils.C_'91''93'_386
-> case [RType] -> [Any]
forall a b. a -> b
coe [RType]
v1 of
[Any]
MAlonzo.Code.Utils.C_'91''93'_386
-> Bool -> Any
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10
[Any]
_ -> Any -> Any
forall a b. a -> b
coe Any
forall {b}. b
v2
MAlonzo.Code.Utils.C__'8759'__388 Any
v3 [Any]
v4
-> case [RType] -> [Any]
forall a b. a -> b
coe [RType]
v1 of
MAlonzo.Code.Utils.C__'8759'__388 Any
v5 [Any]
v6
-> (Bool -> Bool -> Bool) -> Any -> Any -> Any
forall a b. a -> b
coe
Bool -> Bool -> Bool
MAlonzo.Code.Data.Bool.Base.d__'8743'__24
((RType -> RType -> Bool) -> Any -> Any -> Any
forall a b. a -> b
coe RType -> RType -> Bool
d_decRTy_100 (Any -> Any
forall a b. a -> b
coe Any
v3) (Any -> Any
forall a b. a -> b
coe Any
v5))
(([RType] -> [RType] -> Bool) -> Any -> Any -> Any
forall a b. a -> b
coe [RType] -> [RType] -> Bool
d_decRTyList_106 ([Any] -> Any
forall a b. a -> b
coe [Any]
v4) ([Any] -> Any
forall a b. a -> b
coe [Any]
v6))
[Any]
_ -> Any -> Any
forall a b. a -> b
coe Any
forall {b}. b
v2
[Any]
_ -> Any
forall {b}. b
MAlonzo.RTE.mazUnreachableError)
d_decRTyListList_112 ::
MAlonzo.Code.Utils.T_List_382
(MAlonzo.Code.Utils.T_List_382 T_RawTy_2) ->
MAlonzo.Code.Utils.T_List_382
(MAlonzo.Code.Utils.T_List_382 T_RawTy_2) ->
Bool
d_decRTyListList_112 :: [[RType]] -> [[RType]] -> Bool
d_decRTyListList_112 [[RType]]
v0 [[RType]]
v1
= let v2 :: b
v2 = Bool -> b
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8 in
Any -> Bool
forall a b. a -> b
coe
(case [[RType]] -> [Any]
forall a b. a -> b
coe [[RType]]
v0 of
[Any]
MAlonzo.Code.Utils.C_'91''93'_386
-> case [[RType]] -> [Any]
forall a b. a -> b
coe [[RType]]
v1 of
[Any]
MAlonzo.Code.Utils.C_'91''93'_386
-> Bool -> Any
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10
[Any]
_ -> Any -> Any
forall a b. a -> b
coe Any
forall {b}. b
v2
MAlonzo.Code.Utils.C__'8759'__388 Any
v3 [Any]
v4
-> case [[RType]] -> [Any]
forall a b. a -> b
coe [[RType]]
v1 of
MAlonzo.Code.Utils.C__'8759'__388 Any
v5 [Any]
v6
-> (Bool -> Bool -> Bool) -> Any -> Any -> Any
forall a b. a -> b
coe
Bool -> Bool -> Bool
MAlonzo.Code.Data.Bool.Base.d__'8743'__24
(([RType] -> [RType] -> Bool) -> Any -> Any -> Any
forall a b. a -> b
coe [RType] -> [RType] -> Bool
d_decRTyList_106 (Any -> Any
forall a b. a -> b
coe Any
v3) (Any -> Any
forall a b. a -> b
coe Any
v5))
(([[RType]] -> [[RType]] -> Bool) -> Any -> Any -> Any
forall a b. a -> b
coe [[RType]] -> [[RType]] -> Bool
d_decRTyListList_112 ([Any] -> Any
forall a b. a -> b
coe [Any]
v4) ([Any] -> Any
forall a b. a -> b
coe [Any]
v6))
[Any]
_ -> Any -> Any
forall a b. a -> b
coe Any
forall {b}. b
v2
[Any]
_ -> Any
forall {b}. b
MAlonzo.RTE.mazUnreachableError)
d_decRTm_186 :: T_RawTm_30 -> T_RawTm_30 -> Bool
d_decRTm_186 :: RTerm -> RTerm -> Bool
d_decRTm_186 RTerm
v0 RTerm
v1
= let v2 :: b
v2 = Bool -> b
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8 in
Any -> Bool
forall a b. a -> b
coe
(case RTerm -> RTerm
forall a b. a -> b
coe RTerm
v0 of
C_'96'_32 Integer
v3
-> case RTerm -> RTerm
forall a b. a -> b
coe RTerm
v1 of
C_'96'_32 Integer
v4
-> (T_Dec_20 -> Bool) -> Any -> Any
forall a b. a -> b
coe
T_Dec_20 -> Bool
MAlonzo.Code.Relation.Nullary.Decidable.Core.d_does_28
((Integer -> Integer -> T_Dec_20) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> T_Dec_20
MAlonzo.Code.Data.Nat.Properties.d__'8799'__2688 (Integer -> Any
forall a b. a -> b
coe Integer
v3) (Integer -> Any
forall a b. a -> b
coe Integer
v4))
RTerm
_ -> Any -> Any
forall a b. a -> b
coe Any
forall {b}. b
v2
C_Λ_34 KIND
v3 RTerm
v4
-> case RTerm -> RTerm
forall a b. a -> b
coe RTerm
v1 of
C_Λ_34 KIND
v5 RTerm
v6
-> (Bool -> Bool -> Bool) -> Any -> Any -> Any
forall a b. a -> b
coe
Bool -> Bool -> Bool
MAlonzo.Code.Data.Bool.Base.d__'8743'__24
((KIND -> KIND -> Bool) -> Any -> Any -> Any
forall a b. a -> b
coe KIND -> KIND -> Bool
d_decRKi_82 (KIND -> Any
forall a b. a -> b
coe KIND
v3) (KIND -> Any
forall a b. a -> b
coe KIND
v5))
((RTerm -> RTerm -> Bool) -> Any -> Any -> Any
forall a b. a -> b
coe RTerm -> RTerm -> Bool
d_decRTm_186 (RTerm -> Any
forall a b. a -> b
coe RTerm
v4) (RTerm -> Any
forall a b. a -> b
coe RTerm
v6))
RTerm
_ -> Any -> Any
forall a b. a -> b
coe Any
forall {b}. b
v2
C__'183''8902'__36 RTerm
v3 RType
v4
-> case RTerm -> RTerm
forall a b. a -> b
coe RTerm
v1 of
C__'183''8902'__36 RTerm
v5 RType
v6
-> (Bool -> Bool -> Bool) -> Any -> Any -> Any
forall a b. a -> b
coe
Bool -> Bool -> Bool
MAlonzo.Code.Data.Bool.Base.d__'8743'__24
((RTerm -> RTerm -> Bool) -> Any -> Any -> Any
forall a b. a -> b
coe RTerm -> RTerm -> Bool
d_decRTm_186 (RTerm -> Any
forall a b. a -> b
coe RTerm
v3) (RTerm -> Any
forall a b. a -> b
coe RTerm
v5))
((RType -> RType -> Bool) -> Any -> Any -> Any
forall a b. a -> b
coe RType -> RType -> Bool
d_decRTy_100 (RType -> Any
forall a b. a -> b
coe RType
v4) (RType -> Any
forall a b. a -> b
coe RType
v6))
RTerm
_ -> Any -> Any
forall a b. a -> b
coe Any
forall {b}. b
v2
C_ƛ_38 RType
v3 RTerm
v4
-> case RTerm -> RTerm
forall a b. a -> b
coe RTerm
v1 of
C_ƛ_38 RType
v5 RTerm
v6
-> (Bool -> Bool -> Bool) -> Any -> Any -> Any
forall a b. a -> b
coe
Bool -> Bool -> Bool
MAlonzo.Code.Data.Bool.Base.d__'8743'__24
((RType -> RType -> Bool) -> Any -> Any -> Any
forall a b. a -> b
coe RType -> RType -> Bool
d_decRTy_100 (RType -> Any
forall a b. a -> b
coe RType
v3) (RType -> Any
forall a b. a -> b
coe RType
v5))
((RTerm -> RTerm -> Bool) -> Any -> Any -> Any
forall a b. a -> b
coe RTerm -> RTerm -> Bool
d_decRTm_186 (RTerm -> Any
forall a b. a -> b
coe RTerm
v4) (RTerm -> Any
forall a b. a -> b
coe RTerm
v6))
RTerm
_ -> Any -> Any
forall a b. a -> b
coe Any
forall {b}. b
v2
C__'183'__40 RTerm
v3 RTerm
v4
-> case RTerm -> RTerm
forall a b. a -> b
coe RTerm
v1 of
C__'183'__40 RTerm
v5 RTerm
v6
-> (Bool -> Bool -> Bool) -> Any -> Any -> Any
forall a b. a -> b
coe
Bool -> Bool -> Bool
MAlonzo.Code.Data.Bool.Base.d__'8743'__24
((RTerm -> RTerm -> Bool) -> Any -> Any -> Any
forall a b. a -> b
coe RTerm -> RTerm -> Bool
d_decRTm_186 (RTerm -> Any
forall a b. a -> b
coe RTerm
v3) (RTerm -> Any
forall a b. a -> b
coe RTerm
v5))
((RTerm -> RTerm -> Bool) -> Any -> Any -> Any
forall a b. a -> b
coe RTerm -> RTerm -> Bool
d_decRTm_186 (RTerm -> Any
forall a b. a -> b
coe RTerm
v4) (RTerm -> Any
forall a b. a -> b
coe RTerm
v6))
RTerm
_ -> Any -> Any
forall a b. a -> b
coe Any
forall {b}. b
v2
C_con_42 Some (ValueOf DefaultUni)
v3
-> case RTerm -> RTerm
forall a b. a -> b
coe RTerm
v1 of
C_con_42 Some (ValueOf DefaultUni)
v4
-> (Some (ValueOf DefaultUni) -> Some (ValueOf DefaultUni) -> Bool)
-> Any -> Any -> Any
forall a b. a -> b
coe Some (ValueOf DefaultUni) -> Some (ValueOf DefaultUni) -> Bool
MAlonzo.Code.RawU.d_decTagCon_136 (Some (ValueOf DefaultUni) -> Any
forall a b. a -> b
coe Some (ValueOf DefaultUni)
v3) (Some (ValueOf DefaultUni) -> Any
forall a b. a -> b
coe Some (ValueOf DefaultUni)
v4)
RTerm
_ -> Any -> Any
forall a b. a -> b
coe Any
forall {b}. b
v2
C_error_44 RType
v3
-> case RTerm -> RTerm
forall a b. a -> b
coe RTerm
v1 of
C_error_44 RType
v4 -> (RType -> RType -> Bool) -> Any -> Any -> Any
forall a b. a -> b
coe RType -> RType -> Bool
d_decRTy_100 (RType -> Any
forall a b. a -> b
coe RType
v3) (RType -> Any
forall a b. a -> b
coe RType
v4)
RTerm
_ -> Any -> Any
forall a b. a -> b
coe Any
forall {b}. b
v2
C_builtin_46 DefaultFun
v3
-> case RTerm -> RTerm
forall a b. a -> b
coe RTerm
v1 of
C_builtin_46 DefaultFun
v4
-> (T_Dec_20 -> Bool) -> Any -> Any
forall a b. a -> b
coe
T_Dec_20 -> Bool
MAlonzo.Code.Relation.Nullary.Decidable.Core.d_does_28
((DefaultFun -> DefaultFun -> T_Dec_20) -> Any -> Any -> Any
forall a b. a -> b
coe DefaultFun -> DefaultFun -> T_Dec_20
MAlonzo.Code.Builtin.d_decBuiltin_398 (DefaultFun -> Any
forall a b. a -> b
coe DefaultFun
v3) (DefaultFun -> Any
forall a b. a -> b
coe DefaultFun
v4))
RTerm
_ -> Any -> Any
forall a b. a -> b
coe Any
forall {b}. b
v2
C_wrap_48 RType
v3 RType
v4 RTerm
v5
-> case RTerm -> RTerm
forall a b. a -> b
coe RTerm
v1 of
C_wrap_48 RType
v6 RType
v7 RTerm
v8
-> (Bool -> Bool -> Bool) -> Any -> Any -> Any
forall a b. a -> b
coe
Bool -> Bool -> Bool
MAlonzo.Code.Data.Bool.Base.d__'8743'__24
((RType -> RType -> Bool) -> Any -> Any -> Any
forall a b. a -> b
coe RType -> RType -> Bool
d_decRTy_100 (RType -> Any
forall a b. a -> b
coe RType
v3) (RType -> Any
forall a b. a -> b
coe RType
v6))
((Bool -> Bool -> Bool) -> Any -> Any -> Any
forall a b. a -> b
coe
Bool -> Bool -> Bool
MAlonzo.Code.Data.Bool.Base.d__'8743'__24
((RType -> RType -> Bool) -> Any -> Any -> Any
forall a b. a -> b
coe RType -> RType -> Bool
d_decRTy_100 (RType -> Any
forall a b. a -> b
coe RType
v4) (RType -> Any
forall a b. a -> b
coe RType
v7))
((RTerm -> RTerm -> Bool) -> Any -> Any -> Any
forall a b. a -> b
coe RTerm -> RTerm -> Bool
d_decRTm_186 (RTerm -> Any
forall a b. a -> b
coe RTerm
v5) (RTerm -> Any
forall a b. a -> b
coe RTerm
v8)))
RTerm
_ -> Any -> Any
forall a b. a -> b
coe Any
forall {b}. b
v2
C_unwrap_50 RTerm
v3
-> case RTerm -> RTerm
forall a b. a -> b
coe RTerm
v1 of
C_unwrap_50 RTerm
v4 -> (RTerm -> RTerm -> Bool) -> Any -> Any -> Any
forall a b. a -> b
coe RTerm -> RTerm -> Bool
d_decRTm_186 (RTerm -> Any
forall a b. a -> b
coe RTerm
v3) (RTerm -> Any
forall a b. a -> b
coe RTerm
v4)
RTerm
_ -> Any -> Any
forall a b. a -> b
coe Any
forall {b}. b
v2
C_constr_58 RType
v3 Integer
v4 [RTerm]
v5
-> case RTerm -> RTerm
forall a b. a -> b
coe RTerm
v1 of
C_constr_58 RType
v6 Integer
v7 [RTerm]
v8
-> (Bool -> Bool -> Bool) -> Any -> Any -> Any
forall a b. a -> b
coe
Bool -> Bool -> Bool
MAlonzo.Code.Data.Bool.Base.d__'8743'__24
((RType -> RType -> Bool) -> Any -> Any -> Any
forall a b. a -> b
coe RType -> RType -> Bool
d_decRTy_100 (RType -> Any
forall a b. a -> b
coe RType
v3) (RType -> Any
forall a b. a -> b
coe RType
v6))
((Bool -> Bool -> Bool) -> Any -> Any -> Any
forall a b. a -> b
coe
Bool -> Bool -> Bool
MAlonzo.Code.Data.Bool.Base.d__'8743'__24
((T_Dec_20 -> Bool) -> Any -> Any
forall a b. a -> b
coe
T_Dec_20 -> Bool
MAlonzo.Code.Relation.Nullary.Decidable.Core.d_does_28
((Integer -> Integer -> T_Dec_20) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Integer -> T_Dec_20
MAlonzo.Code.Data.Nat.Properties.d__'8799'__2688 (Integer -> Any
forall a b. a -> b
coe Integer
v4)
(Integer -> Any
forall a b. a -> b
coe Integer
v7)))
(([RTerm] -> [RTerm] -> Bool) -> Any -> Any -> Any
forall a b. a -> b
coe [RTerm] -> [RTerm] -> Bool
d_decRTmList_192 ([RTerm] -> Any
forall a b. a -> b
coe [RTerm]
v5) ([RTerm] -> Any
forall a b. a -> b
coe [RTerm]
v8)))
RTerm
_ -> Any -> Any
forall a b. a -> b
coe Any
forall {b}. b
v2
C_case_66 RType
v3 RTerm
v4 [RTerm]
v5
-> case RTerm -> RTerm
forall a b. a -> b
coe RTerm
v1 of
C_case_66 RType
v6 RTerm
v7 [RTerm]
v8
-> (Bool -> Bool -> Bool) -> Any -> Any -> Any
forall a b. a -> b
coe
Bool -> Bool -> Bool
MAlonzo.Code.Data.Bool.Base.d__'8743'__24
((RType -> RType -> Bool) -> Any -> Any -> Any
forall a b. a -> b
coe RType -> RType -> Bool
d_decRTy_100 (RType -> Any
forall a b. a -> b
coe RType
v3) (RType -> Any
forall a b. a -> b
coe RType
v6))
((Bool -> Bool -> Bool) -> Any -> Any -> Any
forall a b. a -> b
coe
Bool -> Bool -> Bool
MAlonzo.Code.Data.Bool.Base.d__'8743'__24
((RTerm -> RTerm -> Bool) -> Any -> Any -> Any
forall a b. a -> b
coe RTerm -> RTerm -> Bool
d_decRTm_186 (RTerm -> Any
forall a b. a -> b
coe RTerm
v4) (RTerm -> Any
forall a b. a -> b
coe RTerm
v7))
(([RTerm] -> [RTerm] -> Bool) -> Any -> Any -> Any
forall a b. a -> b
coe [RTerm] -> [RTerm] -> Bool
d_decRTmList_192 ([RTerm] -> Any
forall a b. a -> b
coe [RTerm]
v5) ([RTerm] -> Any
forall a b. a -> b
coe [RTerm]
v8)))
RTerm
_ -> Any -> Any
forall a b. a -> b
coe Any
forall {b}. b
v2
RTerm
_ -> Any
forall {b}. b
MAlonzo.RTE.mazUnreachableError)
d_decRTmList_192 ::
MAlonzo.Code.Utils.T_List_382 T_RawTm_30 ->
MAlonzo.Code.Utils.T_List_382 T_RawTm_30 -> Bool
d_decRTmList_192 :: [RTerm] -> [RTerm] -> Bool
d_decRTmList_192 [RTerm]
v0 [RTerm]
v1
= let v2 :: b
v2 = Bool -> b
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8 in
Any -> Bool
forall a b. a -> b
coe
(case [RTerm] -> [Any]
forall a b. a -> b
coe [RTerm]
v0 of
[Any]
MAlonzo.Code.Utils.C_'91''93'_386
-> case [RTerm] -> [Any]
forall a b. a -> b
coe [RTerm]
v1 of
[Any]
MAlonzo.Code.Utils.C_'91''93'_386
-> Bool -> Any
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10
[Any]
_ -> Any -> Any
forall a b. a -> b
coe Any
forall {b}. b
v2
MAlonzo.Code.Utils.C__'8759'__388 Any
v3 [Any]
v4
-> case [RTerm] -> [Any]
forall a b. a -> b
coe [RTerm]
v1 of
MAlonzo.Code.Utils.C__'8759'__388 Any
v5 [Any]
v6
-> (Bool -> Bool -> Bool) -> Any -> Any -> Any
forall a b. a -> b
coe
Bool -> Bool -> Bool
MAlonzo.Code.Data.Bool.Base.d__'8743'__24
((RTerm -> RTerm -> Bool) -> Any -> Any -> Any
forall a b. a -> b
coe RTerm -> RTerm -> Bool
d_decRTm_186 (Any -> Any
forall a b. a -> b
coe Any
v3) (Any -> Any
forall a b. a -> b
coe Any
v5))
(([RTerm] -> [RTerm] -> Bool) -> Any -> Any -> Any
forall a b. a -> b
coe [RTerm] -> [RTerm] -> Bool
d_decRTmList_192 ([Any] -> Any
forall a b. a -> b
coe [Any]
v4) ([Any] -> Any
forall a b. a -> b
coe [Any]
v6))
[Any]
_ -> Any -> Any
forall a b. a -> b
coe Any
forall {b}. b
v2
[Any]
_ -> Any
forall {b}. b
MAlonzo.RTE.mazUnreachableError)
d_addBrackets_290 ::
MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
MAlonzo.Code.Agda.Builtin.String.T_String_6
d_addBrackets_290 :: Text -> Text
d_addBrackets_290 Text
v0
= (Text -> Text -> Text) -> Text -> Any -> Text
forall a b. a -> b
coe
Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
(Text
"[" :: Data.Text.Text)
((Text -> Text -> Text) -> Text -> Text -> Any
forall a b. a -> b
coe
Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20 Text
v0
(Text
"]" :: Data.Text.Text))
d_rawTyPrinter_294 ::
T_RawTy_2 -> MAlonzo.Code.Agda.Builtin.String.T_String_6
d_rawTyPrinter_294 :: RType -> Text
d_rawTyPrinter_294 RType
v0
= case RType -> RType
forall a b. a -> b
coe RType
v0 of
C_'96'_6 Integer
v1 -> (Integer -> Text) -> Any -> Text
forall a b. a -> b
coe Integer -> Text
MAlonzo.Code.Data.Integer.Show.d_show_6 (Integer -> Any
forall a b. a -> b
coe Integer
v1)
C__'8658'__8 RType
v1 RType
v2
-> (Text -> Text -> Text) -> Text -> Any -> Text
forall a b. a -> b
coe
Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
(Text
"(" :: Data.Text.Text)
((Text -> Text -> Text) -> Text -> Any -> Any
forall a b. a -> b
coe
Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
(RType -> Text
d_rawTyPrinter_294 (RType -> RType
forall a b. a -> b
coe RType
v1))
((Text -> Text -> Text) -> Text -> Any -> Any
forall a b. a -> b
coe
Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
(Text
"\8658" :: Data.Text.Text)
((Text -> Text -> Text) -> Text -> Text -> Any
forall a b. a -> b
coe
Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
(RType -> Text
d_rawTyPrinter_294 (RType -> RType
forall a b. a -> b
coe RType
v2)) (Text
")" :: Data.Text.Text))))
C_Π_10 KIND
v1 RType
v2
-> (Text -> Text -> Text) -> Text -> Any -> Text
forall a b. a -> b
coe
Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
(Text
"(\928" :: Data.Text.Text)
((Text -> Text -> Text) -> Text -> Any -> Any
forall a b. a -> b
coe
Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
(Text
"kind" :: Data.Text.Text)
((Text -> Text -> Text) -> Text -> Text -> Any
forall a b. a -> b
coe
Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
(RType -> Text
d_rawTyPrinter_294 (RType -> RType
forall a b. a -> b
coe RType
v2)) (Text
")" :: Data.Text.Text)))
C_ƛ_12 KIND
v1 RType
v2
-> (Text -> Text -> Text) -> Text -> Any -> Text
forall a b. a -> b
coe
Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
(Text
"(\411" :: Data.Text.Text)
((Text -> Text -> Text) -> Text -> Any -> Any
forall a b. a -> b
coe
Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
(Text
"kind" :: Data.Text.Text)
((Text -> Text -> Text) -> Text -> Text -> Any
forall a b. a -> b
coe
Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
(RType -> Text
d_rawTyPrinter_294 (RType -> RType
forall a b. a -> b
coe RType
v2)) (Text
")" :: Data.Text.Text)))
C__'183'__14 RType
v1 RType
v2
-> (Text -> Text -> Text) -> Text -> Any -> Text
forall a b. a -> b
coe
Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
(Text
"(" :: Data.Text.Text)
((Text -> Text -> Text) -> Text -> Any -> Any
forall a b. a -> b
coe
Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
(RType -> Text
d_rawTyPrinter_294 (RType -> RType
forall a b. a -> b
coe RType
v1))
((Text -> Text -> Text) -> Text -> Any -> Any
forall a b. a -> b
coe
Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
(Text
"\183" :: Data.Text.Text)
((Text -> Text -> Text) -> Text -> Text -> Any
forall a b. a -> b
coe
Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
(RType -> Text
d_rawTyPrinter_294 (RType -> RType
forall a b. a -> b
coe RType
v2)) (Text
")" :: Data.Text.Text))))
C_con_16 RTyCon
v1 -> Text -> Text
forall a b. a -> b
coe (Text
"(con)" :: Data.Text.Text)
C_μ_18 RType
v1 RType
v2
-> (Text -> Text -> Text) -> Text -> Any -> Text
forall a b. a -> b
coe
Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
(Text
"(\956" :: Data.Text.Text)
((Text -> Text -> Text) -> Text -> Any -> Any
forall a b. a -> b
coe
Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
(RType -> Text
d_rawTyPrinter_294 (RType -> RType
forall a b. a -> b
coe RType
v1))
((Text -> Text -> Text) -> Text -> Text -> Any
forall a b. a -> b
coe
Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
(RType -> Text
d_rawTyPrinter_294 (RType -> RType
forall a b. a -> b
coe RType
v2)) (Text
")" :: Data.Text.Text)))
C_SOP_22 [[RType]]
v1
-> (Text -> Text) -> Any -> Text
forall a b. a -> b
coe Text -> Text
d_addBrackets_290 (([[RType]] -> Text) -> Any -> Any
forall a b. a -> b
coe [[RType]] -> Text
d_rawTyListListPrinter_298 ([[RType]] -> Any
forall a b. a -> b
coe [[RType]]
v1))
RType
_ -> Text
forall {b}. b
MAlonzo.RTE.mazUnreachableError
d_rawTyListPrinter_296 ::
MAlonzo.Code.Utils.T_List_382 T_RawTy_2 ->
MAlonzo.Code.Agda.Builtin.String.T_String_6
d_rawTyListPrinter_296 :: [RType] -> Text
d_rawTyListPrinter_296 [RType]
v0
= case [RType] -> [Any]
forall a b. a -> b
coe [RType]
v0 of
[Any]
MAlonzo.Code.Utils.C_'91''93'_386 -> Text -> Text
forall a b. a -> b
coe (Text
"" :: Data.Text.Text)
MAlonzo.Code.Utils.C__'8759'__388 Any
v1 [Any]
v2
-> case [Any] -> [Any]
forall a b. a -> b
coe [Any]
v2 of
[Any]
MAlonzo.Code.Utils.C_'91''93'_386
-> (RType -> Text) -> Any -> Text
forall a b. a -> b
coe RType -> Text
d_rawTyPrinter_294 (Any -> Any
forall a b. a -> b
coe Any
v1)
MAlonzo.Code.Utils.C__'8759'__388 Any
v3 [Any]
v4
-> (Text -> Text -> Text) -> Text -> Any -> Text
forall a b. a -> b
coe
Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
(RType -> Text
d_rawTyPrinter_294 (Any -> RType
forall a b. a -> b
coe Any
v1))
((Text -> Text -> Text) -> Text -> Text -> Any
forall a b. a -> b
coe
Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
(Text
" , " :: Data.Text.Text) ([RType] -> Text
d_rawTyListPrinter_296 ([Any] -> [RType]
forall a b. a -> b
coe [Any]
v2)))
[Any]
_ -> Text
forall {b}. b
MAlonzo.RTE.mazUnreachableError
[Any]
_ -> Text
forall {b}. b
MAlonzo.RTE.mazUnreachableError
d_rawTyListListPrinter_298 ::
MAlonzo.Code.Utils.T_List_382
(MAlonzo.Code.Utils.T_List_382 T_RawTy_2) ->
MAlonzo.Code.Agda.Builtin.String.T_String_6
d_rawTyListListPrinter_298 :: [[RType]] -> Text
d_rawTyListListPrinter_298 [[RType]]
v0
= case [[RType]] -> [Any]
forall a b. a -> b
coe [[RType]]
v0 of
[Any]
MAlonzo.Code.Utils.C_'91''93'_386 -> Text -> Text
forall a b. a -> b
coe (Text
"" :: Data.Text.Text)
MAlonzo.Code.Utils.C__'8759'__388 Any
v1 [Any]
v2
-> case [Any] -> [Any]
forall a b. a -> b
coe [Any]
v2 of
[Any]
MAlonzo.Code.Utils.C_'91''93'_386
-> (Text -> Text) -> Any -> Text
forall a b. a -> b
coe Text -> Text
d_addBrackets_290 (([RType] -> Text) -> Any -> Any
forall a b. a -> b
coe [RType] -> Text
d_rawTyListPrinter_296 (Any -> Any
forall a b. a -> b
coe Any
v1))
MAlonzo.Code.Utils.C__'8759'__388 Any
v3 [Any]
v4
-> (Text -> Text -> Text) -> Text -> Any -> Text
forall a b. a -> b
coe
Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
(Text -> Text
d_addBrackets_290 (([RType] -> Text) -> Any -> Text
forall a b. a -> b
coe [RType] -> Text
d_rawTyListPrinter_296 (Any -> Any
forall a b. a -> b
coe Any
v1)))
((Text -> Text -> Text) -> Text -> Text -> Any
forall a b. a -> b
coe
Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
(Text
" , " :: Data.Text.Text) ([[RType]] -> Text
d_rawTyListListPrinter_298 ([Any] -> [[RType]]
forall a b. a -> b
coe [Any]
v2)))
[Any]
_ -> Text
forall {b}. b
MAlonzo.RTE.mazUnreachableError
[Any]
_ -> Text
forall {b}. b
MAlonzo.RTE.mazUnreachableError
d_rawListPrinter_342 ::
MAlonzo.Code.Utils.T_List_382 T_RawTm_30 ->
MAlonzo.Code.Agda.Builtin.String.T_String_6
d_rawListPrinter_342 :: [RTerm] -> Text
d_rawListPrinter_342 [RTerm]
v0
= case [RTerm] -> [Any]
forall a b. a -> b
coe [RTerm]
v0 of
[Any]
MAlonzo.Code.Utils.C_'91''93'_386 -> Text -> Text
forall a b. a -> b
coe (Text
"" :: Data.Text.Text)
MAlonzo.Code.Utils.C__'8759'__388 Any
v1 [Any]
v2
-> case [Any] -> [Any]
forall a b. a -> b
coe [Any]
v2 of
[Any]
MAlonzo.Code.Utils.C_'91''93'_386 -> (RTerm -> Text) -> Any -> Text
forall a b. a -> b
coe RTerm -> Text
d_rawPrinter_344 (Any -> Any
forall a b. a -> b
coe Any
v1)
MAlonzo.Code.Utils.C__'8759'__388 Any
v3 [Any]
v4
-> (Text -> Text -> Text) -> Text -> Any -> Text
forall a b. a -> b
coe
Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
(RTerm -> Text
d_rawPrinter_344 (Any -> RTerm
forall a b. a -> b
coe Any
v1))
((Text -> Text -> Text) -> Text -> Text -> Any
forall a b. a -> b
coe
Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
(Text
" , " :: Data.Text.Text) ([RTerm] -> Text
d_rawListPrinter_342 ([Any] -> [RTerm]
forall a b. a -> b
coe [Any]
v2)))
[Any]
_ -> Text
forall {b}. b
MAlonzo.RTE.mazUnreachableError
[Any]
_ -> Text
forall {b}. b
MAlonzo.RTE.mazUnreachableError
d_rawPrinter_344 ::
T_RawTm_30 -> MAlonzo.Code.Agda.Builtin.String.T_String_6
d_rawPrinter_344 :: RTerm -> Text
d_rawPrinter_344 RTerm
v0
= case RTerm -> RTerm
forall a b. a -> b
coe RTerm
v0 of
C_'96'_32 Integer
v1
-> (Integer -> Text) -> Any -> Text
forall a b. a -> b
coe Integer -> Text
MAlonzo.Code.Data.Integer.Show.d_show_6 (Integer -> Any
forall a b. a -> b
coe Integer
v1)
C_Λ_34 KIND
v1 RTerm
v2
-> (Text -> Text -> Text) -> Text -> Any -> Text
forall a b. a -> b
coe
Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
(Text
"(" :: Data.Text.Text)
((Text -> Text -> Text) -> Text -> Any -> Any
forall a b. a -> b
coe
Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
(Text
"\923" :: Data.Text.Text)
((Text -> Text -> Text) -> Text -> Any -> Any
forall a b. a -> b
coe
Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
(Text
"kind" :: Data.Text.Text)
((Text -> Text -> Text) -> Text -> Text -> Any
forall a b. a -> b
coe
Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
(RTerm -> Text
d_rawPrinter_344 (RTerm -> RTerm
forall a b. a -> b
coe RTerm
v2)) (Text
")" :: Data.Text.Text))))
C__'183''8902'__36 RTerm
v1 RType
v2
-> (Text -> Text -> Text) -> Text -> Any -> Text
forall a b. a -> b
coe
Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
(Text
"(" :: Data.Text.Text)
((Text -> Text -> Text) -> Text -> Any -> Any
forall a b. a -> b
coe
Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
(RTerm -> Text
d_rawPrinter_344 (RTerm -> RTerm
forall a b. a -> b
coe RTerm
v1))
((Text -> Text -> Text) -> Text -> Any -> Any
forall a b. a -> b
coe
Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
(Text
"\183\8902" :: Data.Text.Text)
((Text -> Text -> Text) -> Text -> Text -> Any
forall a b. a -> b
coe
Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
(RType -> Text
d_rawTyPrinter_294 (RType -> RType
forall a b. a -> b
coe RType
v2)) (Text
")" :: Data.Text.Text))))
C_ƛ_38 RType
v1 RTerm
v2
-> (Text -> Text -> Text) -> Text -> Any -> Text
forall a b. a -> b
coe
Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
(Text
"(" :: Data.Text.Text)
((Text -> Text -> Text) -> Text -> Any -> Any
forall a b. a -> b
coe
Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
(Text
"\411" :: Data.Text.Text)
((Text -> Text -> Text) -> Text -> Any -> Any
forall a b. a -> b
coe
Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
(RType -> Text
d_rawTyPrinter_294 (RType -> RType
forall a b. a -> b
coe RType
v1))
((Text -> Text -> Text) -> Text -> Text -> Any
forall a b. a -> b
coe
Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
(RTerm -> Text
d_rawPrinter_344 (RTerm -> RTerm
forall a b. a -> b
coe RTerm
v2)) (Text
")" :: Data.Text.Text))))
C__'183'__40 RTerm
v1 RTerm
v2
-> (Text -> Text -> Text) -> Text -> Any -> Text
forall a b. a -> b
coe
Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
(Text
"(" :: Data.Text.Text)
((Text -> Text -> Text) -> Text -> Any -> Any
forall a b. a -> b
coe
Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
(RTerm -> Text
d_rawPrinter_344 (RTerm -> RTerm
forall a b. a -> b
coe RTerm
v1))
((Text -> Text -> Text) -> Text -> Any -> Any
forall a b. a -> b
coe
Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
(Text
"\183" :: Data.Text.Text)
((Text -> Text -> Text) -> Text -> Text -> Any
forall a b. a -> b
coe
Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
(RTerm -> Text
d_rawPrinter_344 (RTerm -> RTerm
forall a b. a -> b
coe RTerm
v2)) (Text
")" :: Data.Text.Text))))
C_con_42 Some (ValueOf DefaultUni)
v1 -> Text -> Text
forall a b. a -> b
coe (Text
"(con)" :: Data.Text.Text)
C_error_44 RType
v1
-> (Text -> Text -> Text) -> Text -> Any -> Text
forall a b. a -> b
coe
Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
(Text
"(error" :: Data.Text.Text)
((Text -> Text -> Text) -> Text -> Text -> Any
forall a b. a -> b
coe
Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
(RType -> Text
d_rawTyPrinter_294 (RType -> RType
forall a b. a -> b
coe RType
v1)) (Text
")" :: Data.Text.Text))
C_builtin_46 DefaultFun
v1 -> Text -> Text
forall a b. a -> b
coe (Text
"(builtin)" :: Data.Text.Text)
C_wrap_48 RType
v1 RType
v2 RTerm
v3
-> (Text -> Text -> Text) -> Text -> Text -> Text
forall a b. a -> b
coe
Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
(Text
"(wrap" :: Data.Text.Text) (Text
")" :: Data.Text.Text)
C_unwrap_50 RTerm
v1
-> (Text -> Text -> Text) -> Text -> Any -> Text
forall a b. a -> b
coe
Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
(Text
"(unwrap" :: Data.Text.Text)
((Text -> Text -> Text) -> Text -> Text -> Any
forall a b. a -> b
coe
Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
(RTerm -> Text
d_rawPrinter_344 (RTerm -> RTerm
forall a b. a -> b
coe RTerm
v1)) (Text
")" :: Data.Text.Text))
C_constr_58 RType
v1 Integer
v2 [RTerm]
v3
-> (Text -> Text -> Text) -> Text -> Any -> Text
forall a b. a -> b
coe
Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
(Text
"(const" :: Data.Text.Text)
((Text -> Text -> Text) -> Text -> Any -> Any
forall a b. a -> b
coe
Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
(RType -> Text
d_rawTyPrinter_294 (RType -> RType
forall a b. a -> b
coe RType
v1))
((Text -> Text -> Text) -> Text -> Any -> Any
forall a b. a -> b
coe
Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
(Text
" " :: Data.Text.Text)
((Text -> Text -> Text) -> Text -> Any -> Any
forall a b. a -> b
coe
Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
(Integer -> Text
MAlonzo.Code.Data.Integer.Show.d_show_6 (Integer -> Integer
forall a b. a -> b
coe Integer
v2))
((Text -> Text -> Text) -> Text -> Any -> Any
forall a b. a -> b
coe
Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
(Text
" [" :: Data.Text.Text)
((Text -> Text -> Text) -> Text -> Text -> Any
forall a b. a -> b
coe
Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
([RTerm] -> Text
d_rawListPrinter_342 ([RTerm] -> [RTerm]
forall a b. a -> b
coe [RTerm]
v3)) (Text
"])" :: Data.Text.Text))))))
C_case_66 RType
v1 RTerm
v2 [RTerm]
v3
-> (Text -> Text -> Text) -> Text -> Any -> Text
forall a b. a -> b
coe
Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
(Text
"(case" :: Data.Text.Text)
((Text -> Text -> Text) -> Text -> Any -> Any
forall a b. a -> b
coe
Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
(RType -> Text
d_rawTyPrinter_294 (RType -> RType
forall a b. a -> b
coe RType
v1))
((Text -> Text -> Text) -> Text -> Any -> Any
forall a b. a -> b
coe
Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
(Text
" " :: Data.Text.Text)
((Text -> Text -> Text) -> Text -> Any -> Any
forall a b. a -> b
coe
Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
(RTerm -> Text
d_rawPrinter_344 (RTerm -> RTerm
forall a b. a -> b
coe RTerm
v2))
((Text -> Text -> Text) -> Text -> Any -> Any
forall a b. a -> b
coe
Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
(Text
" [" :: Data.Text.Text)
((Text -> Text -> Text) -> Text -> Text -> Any
forall a b. a -> b
coe
Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
([RTerm] -> Text
d_rawListPrinter_342 ([RTerm] -> [RTerm]
forall a b. a -> b
coe [RTerm]
v3)) (Text
"])" :: Data.Text.Text))))))
RTerm
_ -> Text
forall {b}. b
MAlonzo.RTE.mazUnreachableError