{-# 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.VerifiedCompilation 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.IO
import qualified MAlonzo.Code.Agda.Builtin.String
import qualified MAlonzo.Code.Agda.Builtin.Unit
import qualified MAlonzo.Code.Data.String.Base
import qualified MAlonzo.Code.RawU
import qualified MAlonzo.Code.Relation.Nullary
import qualified MAlonzo.Code.Scoped
import qualified MAlonzo.Code.Untyped
import qualified MAlonzo.Code.Utils
import qualified MAlonzo.Code.VerifiedCompilation.Equality
import qualified MAlonzo.Code.VerifiedCompilation.UCaseOfCase
import qualified MAlonzo.Code.VerifiedCompilation.UForceDelay
import qualified MAlonzo.Code.VerifiedCompilation.UntypedTranslation
import qualified Data.Text.IO as TextIO
import qualified System.IO as IO
import qualified Data.Text as Text
d_Trace_6 :: p -> p -> p -> ()
d_Trace_6 p
a0 p
a1 p
a2 = ()
data T_Trace_6 = C_empty_12 | C_cons_22 AgdaAny T_Trace_6
d_IsTransformation_24 :: p -> p -> p -> ()
d_IsTransformation_24 p
a0 p
a1 p
a2 = ()
data T_IsTransformation_24
= C_isCoC_32 MAlonzo.Code.VerifiedCompilation.UCaseOfCase.T_CoC_4 |
C_isFD_40 MAlonzo.Code.VerifiedCompilation.UForceDelay.T_FD_48
d_isTrace'63'_46 ::
() ->
(() ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Untyped.T__'8866'_14 -> ()) ->
(MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
MAlonzo.Code.Utils.T_List_382
(MAlonzo.Code.Utils.T__'215'__364
MAlonzo.Code.Untyped.T__'8866'_14
MAlonzo.Code.Untyped.T__'8866'_14) ->
MAlonzo.Code.Relation.Nullary.T_Dec_32
d_isTrace'63'_46 :: ()
-> (() -> T__'8866'_14 -> T__'8866'_14 -> ())
-> (T__'8866'_14 -> T__'8866'_14 -> T_Dec_32)
-> T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
-> T_Dec_32
d_isTrace'63'_46 ~()
v0 ~() -> T__'8866'_14 -> T__'8866'_14 -> ()
v1 T__'8866'_14 -> T__'8866'_14 -> T_Dec_32
v2 T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
v3 = (T__'8866'_14 -> T__'8866'_14 -> T_Dec_32)
-> T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14) -> T_Dec_32
du_isTrace'63'_46 T__'8866'_14 -> T__'8866'_14 -> T_Dec_32
v2 T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
v3
du_isTrace'63'_46 ::
(MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
MAlonzo.Code.Utils.T_List_382
(MAlonzo.Code.Utils.T__'215'__364
MAlonzo.Code.Untyped.T__'8866'_14
MAlonzo.Code.Untyped.T__'8866'_14) ->
MAlonzo.Code.Relation.Nullary.T_Dec_32
du_isTrace'63'_46 :: (T__'8866'_14 -> T__'8866'_14 -> T_Dec_32)
-> T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14) -> T_Dec_32
du_isTrace'63'_46 T__'8866'_14 -> T__'8866'_14 -> T_Dec_32
v0 T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
v1
= case T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14) -> [Any]
forall a b. a -> b
coe T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
v1 of
[Any]
MAlonzo.Code.Utils.C_'91''93'_386
-> (Bool -> T_Reflects_14 -> T_Dec_32) -> Any -> Any -> T_Dec_32
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> Any
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10)
((Any -> T_Reflects_14) -> Any -> Any
forall a b. a -> b
coe Any -> T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'696'_22 (T_Trace_6 -> Any
forall a b. a -> b
coe T_Trace_6
C_empty_12))
MAlonzo.Code.Utils.C__'8759'__388 Any
v2 [Any]
v3
-> case Any -> (Any, Any)
forall a b. a -> b
coe Any
v2 of
MAlonzo.Code.Utils.C__'44'__378 Any
v4 Any
v5
-> let v6 :: t
v6 = ((T__'8866'_14 -> T__'8866'_14 -> T_Dec_32)
-> T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
-> T_Dec_32)
-> Any -> Any -> t
forall a b. a -> b
coe (T__'8866'_14 -> T__'8866'_14 -> T_Dec_32)
-> T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14) -> T_Dec_32
du_isTrace'63'_46 ((T__'8866'_14 -> T__'8866'_14 -> T_Dec_32) -> Any
forall a b. a -> b
coe T__'8866'_14 -> T__'8866'_14 -> T_Dec_32
v0) ([Any] -> Any
forall a b. a -> b
coe [Any]
v3) in
Any -> T_Dec_32
forall a b. a -> b
coe
(case Any -> T_Dec_32
forall a b. a -> b
coe Any
forall {t}. t
v6 of
MAlonzo.Code.Relation.Nullary.C__because__46 Bool
v7 T_Reflects_14
v8
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v7
then case T_Reflects_14 -> T_Reflects_14
forall a b. a -> b
coe T_Reflects_14
v8 of
MAlonzo.Code.Relation.Nullary.C_of'696'_22 Any
v9
-> let v10 :: t
v10 = (T__'8866'_14 -> T__'8866'_14 -> T_Dec_32) -> Any -> Any -> t
forall a b. a -> b
coe T__'8866'_14 -> T__'8866'_14 -> T_Dec_32
v0 Any
v4 Any
v5 in
Any -> Any
forall a b. a -> b
coe
(case Any -> T_Dec_32
forall a b. a -> b
coe Any
forall {t}. t
v10 of
MAlonzo.Code.Relation.Nullary.C__because__46 Bool
v11 T_Reflects_14
v12
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v11
then case T_Reflects_14 -> T_Reflects_14
forall a b. a -> b
coe T_Reflects_14
v12 of
MAlonzo.Code.Relation.Nullary.C_of'696'_22 Any
v13
-> (Bool -> T_Reflects_14 -> T_Dec_32) -> Any -> Any -> Any
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> Any
forall a b. a -> b
coe Bool
v11)
((Any -> T_Reflects_14) -> Any -> Any
forall a b. a -> b
coe
Any -> T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'696'_22
((Any -> T_Trace_6 -> T_Trace_6) -> Any -> Any -> Any
forall a b. a -> b
coe Any -> T_Trace_6 -> T_Trace_6
C_cons_22 Any
v13 Any
v9))
T_Reflects_14
_ -> Any
forall {t}. t
MAlonzo.RTE.mazUnreachableError
else (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> Any -> Any
forall a b. a -> b -> b
seq (T_Reflects_14 -> Any
forall a b. a -> b
coe T_Reflects_14
v12)
((Bool -> T_Reflects_14 -> T_Dec_32) -> Any -> Any -> Any
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> Any
forall a b. a -> b
coe Bool
v11)
(T_Reflects_14 -> Any
forall a b. a -> b
coe
T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26))
T_Dec_32
_ -> Any
forall {t}. t
MAlonzo.RTE.mazUnreachableError)
T_Reflects_14
_ -> Any
forall {t}. t
MAlonzo.RTE.mazUnreachableError
else (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> Any -> Any
forall a b. a -> b -> b
seq (T_Reflects_14 -> Any
forall a b. a -> b
coe T_Reflects_14
v8)
((Bool -> T_Reflects_14 -> T_Dec_32) -> Any -> Any -> Any
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46 (Bool -> Any
forall a b. a -> b
coe Bool
v7)
(T_Reflects_14 -> Any
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26))
T_Dec_32
_ -> Any
forall {t}. t
MAlonzo.RTE.mazUnreachableError)
(Any, Any)
_ -> T_Dec_32
forall {t}. t
MAlonzo.RTE.mazUnreachableError
[Any]
_ -> T_Dec_32
forall {t}. t
MAlonzo.RTE.mazUnreachableError
d_isTransformation'63'_150 ::
() ->
MAlonzo.Code.VerifiedCompilation.Equality.T_DecEq_6 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Relation.Nullary.T_Dec_32
d_isTransformation'63'_150 :: () -> T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_32
d_isTransformation'63'_150 ~()
v0 T_DecEq_6
v1 T__'8866'_14
v2 T__'8866'_14
v3
= T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_32
du_isTransformation'63'_150 T_DecEq_6
v1 T__'8866'_14
v2 T__'8866'_14
v3
du_isTransformation'63'_150 ::
MAlonzo.Code.VerifiedCompilation.Equality.T_DecEq_6 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Relation.Nullary.T_Dec_32
du_isTransformation'63'_150 :: T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_32
du_isTransformation'63'_150 T_DecEq_6
v0 T__'8866'_14
v1 T__'8866'_14
v2
= let v3 :: t
v3
= (T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_32)
-> Any -> Any -> Any -> t
forall a b. a -> b
coe
T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_32
MAlonzo.Code.VerifiedCompilation.UCaseOfCase.du_isCoC'63'_264
(T_DecEq_6 -> Any
forall a b. a -> b
coe T_DecEq_6
v0) (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v1) (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v2) in
Any -> T_Dec_32
forall a b. a -> b
coe
(let v4 :: t
v4
= (T_DecEq_6
-> Integer -> Integer -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_32)
-> Any -> Any -> Any -> Any -> Any -> t
forall a b. a -> b
coe
T_DecEq_6
-> Integer -> Integer -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_32
MAlonzo.Code.VerifiedCompilation.UForceDelay.du_isFD'63'_138
(T_DecEq_6 -> Any
forall a b. a -> b
coe T_DecEq_6
v0) (Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer)) (Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer)) (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v1)
(T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v2) in
Any -> Any
forall a b. a -> b
coe
(case Any -> T_Dec_32
forall a b. a -> b
coe Any
forall {t}. t
v4 of
MAlonzo.Code.Relation.Nullary.C__because__46 Bool
v5 T_Reflects_14
v6
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v5
then case T_Reflects_14 -> T_Reflects_14
forall a b. a -> b
coe T_Reflects_14
v6 of
MAlonzo.Code.Relation.Nullary.C_of'696'_22 Any
v7
-> case Any -> T_Dec_32
forall a b. a -> b
coe Any
forall {t}. t
v3 of
MAlonzo.Code.Relation.Nullary.C__because__46 Bool
v8 T_Reflects_14
v9
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v8
then case T_Reflects_14 -> T_Reflects_14
forall a b. a -> b
coe T_Reflects_14
v9 of
MAlonzo.Code.Relation.Nullary.C_of'696'_22 Any
v10
-> (Bool -> T_Reflects_14 -> T_Dec_32) -> Any -> Any -> Any
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> Any
forall a b. a -> b
coe Bool
v8)
((Any -> T_Reflects_14) -> Any -> Any
forall a b. a -> b
coe
Any -> T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'696'_22
((T_CoC_4 -> T_IsTransformation_24) -> Any -> Any
forall a b. a -> b
coe T_CoC_4 -> T_IsTransformation_24
C_isCoC_32 Any
v10))
T_Reflects_14
_ -> Any
forall {t}. t
MAlonzo.RTE.mazUnreachableError
else (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> Any -> Any
forall a b. a -> b -> b
seq (T_Reflects_14 -> Any
forall a b. a -> b
coe T_Reflects_14
v9)
((Bool -> T_Reflects_14 -> T_Dec_32) -> Any -> Any -> Any
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> Any
forall a b. a -> b
coe Bool
v5)
((Any -> T_Reflects_14) -> Any -> Any
forall a b. a -> b
coe
Any -> T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'696'_22
((T_FD_48 -> T_IsTransformation_24) -> Any -> Any
forall a b. a -> b
coe T_FD_48 -> T_IsTransformation_24
C_isFD_40 Any
v7)))
T_Dec_32
_ -> Any
forall {t}. t
MAlonzo.RTE.mazUnreachableError
T_Reflects_14
_ -> Any
forall {t}. t
MAlonzo.RTE.mazUnreachableError
else (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> Any -> Any
forall a b. a -> b -> b
seq (T_Reflects_14 -> Any
forall a b. a -> b
coe T_Reflects_14
v6)
(case Any -> T_Dec_32
forall a b. a -> b
coe Any
forall {t}. t
v3 of
MAlonzo.Code.Relation.Nullary.C__because__46 Bool
v7 T_Reflects_14
v8
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v7
then case T_Reflects_14 -> T_Reflects_14
forall a b. a -> b
coe T_Reflects_14
v8 of
MAlonzo.Code.Relation.Nullary.C_of'696'_22 Any
v9
-> (Bool -> T_Reflects_14 -> T_Dec_32) -> Any -> Any -> Any
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
(Bool -> Any
forall a b. a -> b
coe Bool
v7)
((Any -> T_Reflects_14) -> Any -> Any
forall a b. a -> b
coe
Any -> T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'696'_22
((T_CoC_4 -> T_IsTransformation_24) -> Any -> Any
forall a b. a -> b
coe T_CoC_4 -> T_IsTransformation_24
C_isCoC_32 Any
v9))
T_Reflects_14
_ -> Any
forall {t}. t
MAlonzo.RTE.mazUnreachableError
else (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
Any -> Any -> Any
forall a b. a -> b -> b
seq (T_Reflects_14 -> Any
forall a b. a -> b
coe T_Reflects_14
v8)
((Bool -> T_Reflects_14 -> T_Dec_32) -> Any -> Any -> Any
forall a b. a -> b
coe
Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46 (Bool -> Any
forall a b. a -> b
coe Bool
v7)
(T_Reflects_14 -> Any
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26))
T_Dec_32
_ -> Any
forall {t}. t
MAlonzo.RTE.mazUnreachableError)
T_Dec_32
_ -> Any
forall {t}. t
MAlonzo.RTE.mazUnreachableError))
d_showTranslation_214 ::
() ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.VerifiedCompilation.UntypedTranslation.T_Translation_12 ->
MAlonzo.Code.Agda.Builtin.String.T_String_6
d_showTranslation_214 :: () -> T__'8866'_14 -> T__'8866'_14 -> T_Translation_12 -> Text
d_showTranslation_214 ~()
v0 T__'8866'_14
v1 T__'8866'_14
v2 T_Translation_12
v3
= T__'8866'_14 -> T__'8866'_14 -> T_Translation_12 -> Text
du_showTranslation_214 T__'8866'_14
v1 T__'8866'_14
v2 T_Translation_12
v3
du_showTranslation_214 ::
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.VerifiedCompilation.UntypedTranslation.T_Translation_12 ->
MAlonzo.Code.Agda.Builtin.String.T_String_6
du_showTranslation_214 :: T__'8866'_14 -> T__'8866'_14 -> T_Translation_12 -> Text
du_showTranslation_214 T__'8866'_14
v0 T__'8866'_14
v1 T_Translation_12
v2
= case T_Translation_12 -> T_Translation_12
forall a b. a -> b
coe T_Translation_12
v2 of
MAlonzo.Code.VerifiedCompilation.UntypedTranslation.C_istranslation_22 Any
v6
-> Text -> Text
forall a b. a -> b
coe (Text
"istranslation TODO" :: Data.Text.Text)
T_Translation_12
MAlonzo.Code.VerifiedCompilation.UntypedTranslation.C_var_28
-> Text -> Text
forall a b. a -> b
coe (Text
"var" :: Data.Text.Text)
MAlonzo.Code.VerifiedCompilation.UntypedTranslation.C_ƛ_36 T_Translation_12
v6
-> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v0 of
MAlonzo.Code.Untyped.C_ƛ_20 T__'8866'_14
v7
-> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v1 of
MAlonzo.Code.Untyped.C_ƛ_20 T__'8866'_14
v8
-> (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) -> Any -> Text -> Any
forall a b. a -> b
coe
Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
((T__'8866'_14 -> T__'8866'_14 -> T_Translation_12 -> Text)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe T__'8866'_14 -> T__'8866'_14 -> T_Translation_12 -> Text
du_showTranslation_214 (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v7) (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v8) (T_Translation_12 -> Any
forall a b. a -> b
coe T_Translation_12
v6))
(Text
")" :: Data.Text.Text))
T__'8866'_14
_ -> Text
forall {t}. t
MAlonzo.RTE.mazUnreachableError
T__'8866'_14
_ -> Text
forall {t}. t
MAlonzo.RTE.mazUnreachableError
MAlonzo.Code.VerifiedCompilation.UntypedTranslation.C_app_48 T_Translation_12
v8 T_Translation_12
v9
-> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v0 of
MAlonzo.Code.Untyped.C__'183'__22 T__'8866'_14
v10 T__'8866'_14
v11
-> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v1 of
MAlonzo.Code.Untyped.C__'183'__22 T__'8866'_14
v12 T__'8866'_14
v13
-> (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
"(app " :: Data.Text.Text)
((Text -> Text -> Text) -> Any -> Any -> Any
forall a b. a -> b
coe
Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
((T__'8866'_14 -> T__'8866'_14 -> T_Translation_12 -> Text)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe T__'8866'_14 -> T__'8866'_14 -> T_Translation_12 -> Text
du_showTranslation_214 (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v10) (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v12) (T_Translation_12 -> Any
forall a b. a -> b
coe T_Translation_12
v8))
((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) -> Any -> Text -> Any
forall a b. a -> b
coe
Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
((T__'8866'_14 -> T__'8866'_14 -> T_Translation_12 -> Text)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe T__'8866'_14 -> T__'8866'_14 -> T_Translation_12 -> Text
du_showTranslation_214 (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v11) (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v13) (T_Translation_12 -> Any
forall a b. a -> b
coe T_Translation_12
v9))
(Text
")" :: Data.Text.Text))))
T__'8866'_14
_ -> Text
forall {t}. t
MAlonzo.RTE.mazUnreachableError
T__'8866'_14
_ -> Text
forall {t}. t
MAlonzo.RTE.mazUnreachableError
MAlonzo.Code.VerifiedCompilation.UntypedTranslation.C_force_56 T_Translation_12
v6
-> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v0 of
MAlonzo.Code.Untyped.C_force_24 T__'8866'_14
v7
-> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v1 of
MAlonzo.Code.Untyped.C_force_24 T__'8866'_14
v8
-> (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
"(force " :: Data.Text.Text)
((Text -> Text -> Text) -> Any -> Text -> Any
forall a b. a -> b
coe
Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
((T__'8866'_14 -> T__'8866'_14 -> T_Translation_12 -> Text)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe T__'8866'_14 -> T__'8866'_14 -> T_Translation_12 -> Text
du_showTranslation_214 (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v7) (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v8) (T_Translation_12 -> Any
forall a b. a -> b
coe T_Translation_12
v6))
(Text
")" :: Data.Text.Text))
T__'8866'_14
_ -> Text
forall {t}. t
MAlonzo.RTE.mazUnreachableError
T__'8866'_14
_ -> Text
forall {t}. t
MAlonzo.RTE.mazUnreachableError
MAlonzo.Code.VerifiedCompilation.UntypedTranslation.C_delay_64 T_Translation_12
v6
-> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v0 of
MAlonzo.Code.Untyped.C_delay_26 T__'8866'_14
v7
-> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v1 of
MAlonzo.Code.Untyped.C_delay_26 T__'8866'_14
v8
-> (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
"(delay " :: Data.Text.Text)
((Text -> Text -> Text) -> Any -> Text -> Any
forall a b. a -> b
coe
Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
((T__'8866'_14 -> T__'8866'_14 -> T_Translation_12 -> Text)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe T__'8866'_14 -> T__'8866'_14 -> T_Translation_12 -> Text
du_showTranslation_214 (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v7) (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v8) (T_Translation_12 -> Any
forall a b. a -> b
coe T_Translation_12
v6))
(Text
")" :: Data.Text.Text))
T__'8866'_14
_ -> Text
forall {t}. t
MAlonzo.RTE.mazUnreachableError
T__'8866'_14
_ -> Text
forall {t}. t
MAlonzo.RTE.mazUnreachableError
T_Translation_12
MAlonzo.Code.VerifiedCompilation.UntypedTranslation.C_con_70
-> Text -> Text
forall a b. a -> b
coe (Text
"con" :: Data.Text.Text)
MAlonzo.Code.VerifiedCompilation.UntypedTranslation.C_constr_80 T_Pointwise_48
v7
-> Text -> Text
forall a b. a -> b
coe (Text
"(constr TODO)" :: Data.Text.Text)
MAlonzo.Code.VerifiedCompilation.UntypedTranslation.C_case_92 T_Pointwise_48
v8 T_Translation_12
v9
-> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v0 of
MAlonzo.Code.Untyped.C_case_40 T__'8866'_14
v10 [T__'8866'_14]
v11
-> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v1 of
MAlonzo.Code.Untyped.C_case_40 T__'8866'_14
v12 [T__'8866'_14]
v13
-> (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 TODO " :: Data.Text.Text)
((Text -> Text -> Text) -> Any -> Text -> Any
forall a b. a -> b
coe
Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
((T__'8866'_14 -> T__'8866'_14 -> T_Translation_12 -> Text)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe T__'8866'_14 -> T__'8866'_14 -> T_Translation_12 -> Text
du_showTranslation_214 (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v10) (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v12) (T_Translation_12 -> Any
forall a b. a -> b
coe T_Translation_12
v9))
(Text
")" :: Data.Text.Text))
T__'8866'_14
_ -> Text
forall {t}. t
MAlonzo.RTE.mazUnreachableError
T__'8866'_14
_ -> Text
forall {t}. t
MAlonzo.RTE.mazUnreachableError
T_Translation_12
MAlonzo.Code.VerifiedCompilation.UntypedTranslation.C_builtin_98
-> Text -> Text
forall a b. a -> b
coe (Text
"builtin" :: Data.Text.Text)
T_Translation_12
MAlonzo.Code.VerifiedCompilation.UntypedTranslation.C_error_102
-> Text -> Text
forall a b. a -> b
coe (Text
"error" :: Data.Text.Text)
T_Translation_12
_ -> Text
forall {t}. t
MAlonzo.RTE.mazUnreachableError
d_showTrace_238 ::
() ->
MAlonzo.Code.Utils.T_List_382
(MAlonzo.Code.Utils.T__'215'__364
MAlonzo.Code.Untyped.T__'8866'_14
MAlonzo.Code.Untyped.T__'8866'_14) ->
T_Trace_6 -> MAlonzo.Code.Agda.Builtin.String.T_String_6
d_showTrace_238 :: ()
-> T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
-> T_Trace_6
-> Text
d_showTrace_238 ~()
v0 T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
v1 T_Trace_6
v2 = T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
-> T_Trace_6 -> Text
du_showTrace_238 T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
v1 T_Trace_6
v2
du_showTrace_238 ::
MAlonzo.Code.Utils.T_List_382
(MAlonzo.Code.Utils.T__'215'__364
MAlonzo.Code.Untyped.T__'8866'_14
MAlonzo.Code.Untyped.T__'8866'_14) ->
T_Trace_6 -> MAlonzo.Code.Agda.Builtin.String.T_String_6
du_showTrace_238 :: T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
-> T_Trace_6 -> Text
du_showTrace_238 T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
v0 T_Trace_6
v1
= case T_Trace_6 -> T_Trace_6
forall a b. a -> b
coe T_Trace_6
v1 of
T_Trace_6
C_empty_12 -> Text -> Text
forall a b. a -> b
coe (Text
"empty" :: Data.Text.Text)
C_cons_22 Any
v6 T_Trace_6
v7
-> case T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14) -> [Any]
forall a b. a -> b
coe T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
v0 of
MAlonzo.Code.Utils.C__'8759'__388 Any
v8 [Any]
v9
-> case Any -> (Any, Any)
forall a b. a -> b
coe Any
v8 of
MAlonzo.Code.Utils.C__'44'__378 Any
v10 Any
v11
-> (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
"(cons " :: Data.Text.Text)
((Text -> Text -> Text) -> Any -> Any -> Any
forall a b. a -> b
coe
Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
((T__'8866'_14 -> T__'8866'_14 -> T_Translation_12 -> Text)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe T__'8866'_14 -> T__'8866'_14 -> T_Translation_12 -> Text
du_showTranslation_214 (Any -> Any
forall a b. a -> b
coe Any
v10) (Any -> Any
forall a b. a -> b
coe Any
v11) (Any -> Any
forall a b. a -> b
coe Any
v6))
((Text -> Text -> Text) -> Any -> Text -> Any
forall a b. a -> b
coe
Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
((T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
-> T_Trace_6 -> Text)
-> Any -> Any -> Any
forall a b. a -> b
coe T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
-> T_Trace_6 -> Text
du_showTrace_238 ([Any] -> Any
forall a b. a -> b
coe [Any]
v9) (T_Trace_6 -> Any
forall a b. a -> b
coe T_Trace_6
v7)) (Text
")" :: Data.Text.Text)))
(Any, Any)
_ -> Text
forall {t}. t
MAlonzo.RTE.mazUnreachableError
[Any]
_ -> Text
forall {t}. t
MAlonzo.RTE.mazUnreachableError
T_Trace_6
_ -> Text
forall {t}. t
MAlonzo.RTE.mazUnreachableError
d_serializeTraceProof_248 ::
() ->
MAlonzo.Code.Utils.T_List_382
(MAlonzo.Code.Utils.T__'215'__364
MAlonzo.Code.Untyped.T__'8866'_14
MAlonzo.Code.Untyped.T__'8866'_14) ->
MAlonzo.Code.Relation.Nullary.T_Dec_32 ->
MAlonzo.Code.Agda.Builtin.String.T_String_6
d_serializeTraceProof_248 :: ()
-> T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
-> T_Dec_32
-> Text
d_serializeTraceProof_248 ~()
v0 T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
v1 T_Dec_32
v2
= T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
-> T_Dec_32 -> Text
du_serializeTraceProof_248 T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
v1 T_Dec_32
v2
du_serializeTraceProof_248 ::
MAlonzo.Code.Utils.T_List_382
(MAlonzo.Code.Utils.T__'215'__364
MAlonzo.Code.Untyped.T__'8866'_14
MAlonzo.Code.Untyped.T__'8866'_14) ->
MAlonzo.Code.Relation.Nullary.T_Dec_32 ->
MAlonzo.Code.Agda.Builtin.String.T_String_6
du_serializeTraceProof_248 :: T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
-> T_Dec_32 -> Text
du_serializeTraceProof_248 T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
v0 T_Dec_32
v1
= case T_Dec_32 -> T_Dec_32
forall a b. a -> b
coe T_Dec_32
v1 of
MAlonzo.Code.Relation.Nullary.C__because__46 Bool
v2 T_Reflects_14
v3
-> if Bool -> Bool
forall a b. a -> b
coe Bool
v2
then case T_Reflects_14 -> T_Reflects_14
forall a b. a -> b
coe T_Reflects_14
v3 of
MAlonzo.Code.Relation.Nullary.C_of'696'_22 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
"yes " :: Data.Text.Text) ((T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
-> T_Trace_6 -> Text)
-> Any -> Any -> Any
forall a b. a -> b
coe T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
-> T_Trace_6 -> Text
du_showTrace_238 (T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14) -> Any
forall a b. a -> b
coe T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
v0) (Any -> Any
forall a b. a -> b
coe Any
v4))
T_Reflects_14
_ -> Text
forall {t}. t
MAlonzo.RTE.mazUnreachableError
else (Any -> Any -> Any) -> Any -> Any -> Text
forall a b. a -> b
coe Any -> Any -> Any
forall a b. a -> b -> b
seq (T_Reflects_14 -> Any
forall a b. a -> b
coe T_Reflects_14
v3) (Text -> Any
forall a b. a -> b
coe (Text
"no" :: Data.Text.Text))
T_Dec_32
_ -> Text
forall {t}. t
MAlonzo.RTE.mazUnreachableError
type T_FileHandle_254 = IO.Handle
d_FileHandle_254 :: a
d_FileHandle_254
= [Char] -> a
forall a. HasCallStack => [Char] -> a
error
[Char]
"MAlonzo Runtime Error: postulate evaluated: VerifiedCompilation.FileHandle"
d_writeFile_256 ::
MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
MAlonzo.Code.Agda.Builtin.IO.T_IO_8
() MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6
d_writeFile_256 :: Text -> Text -> T_IO_8 () ()
d_writeFile_256 = \Text
f -> [Char] -> Text -> T_IO_8 () ()
TextIO.writeFile (Text -> [Char]
Text.unpack Text
f)
d_stderr_258 :: T_FileHandle_254
d_stderr_258 :: T_FileHandle_254
d_stderr_258 = T_FileHandle_254
IO.stderr
d_hPutStrLn_260 ::
T_FileHandle_254 ->
MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
MAlonzo.Code.Agda.Builtin.IO.T_IO_8
() MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6
d_hPutStrLn_260 :: T_FileHandle_254 -> Text -> T_IO_8 () ()
d_hPutStrLn_260 = T_FileHandle_254 -> Text -> T_IO_8 () ()
TextIO.hPutStr
d_buildPairs_264 ::
() ->
MAlonzo.Code.Utils.T_List_382 MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Utils.T_List_382
(MAlonzo.Code.Utils.T__'215'__364
MAlonzo.Code.Untyped.T__'8866'_14
MAlonzo.Code.Untyped.T__'8866'_14)
d_buildPairs_264 :: ()
-> [T__'8866'_14]
-> T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
d_buildPairs_264 ~()
v0 [T__'8866'_14]
v1 = [T__'8866'_14]
-> T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
du_buildPairs_264 [T__'8866'_14]
v1
du_buildPairs_264 ::
MAlonzo.Code.Utils.T_List_382 MAlonzo.Code.Untyped.T__'8866'_14 ->
MAlonzo.Code.Utils.T_List_382
(MAlonzo.Code.Utils.T__'215'__364
MAlonzo.Code.Untyped.T__'8866'_14
MAlonzo.Code.Untyped.T__'8866'_14)
du_buildPairs_264 :: [T__'8866'_14]
-> T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
du_buildPairs_264 [T__'8866'_14]
v0
= case [T__'8866'_14] -> [Any]
forall a b. a -> b
coe [T__'8866'_14]
v0 of
[Any]
MAlonzo.Code.Utils.C_'91''93'_386 -> [T__'8866'_14]
-> T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
forall a b. a -> b
coe [T__'8866'_14]
v0
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
-> (Any -> [Any] -> [Any])
-> Any
-> Any
-> T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
forall a b. a -> b
coe
Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Utils.C__'8759'__388
((Any -> Any -> (Any, Any)) -> Any -> Any -> Any
forall a b. a -> b
coe Any -> Any -> (Any, Any)
forall {a} {b}. a -> b -> (a, b)
MAlonzo.Code.Utils.C__'44'__378 (Any -> Any
forall a b. a -> b
coe Any
v1) (Any -> Any
forall a b. a -> b
coe Any
v1)) ([Any] -> Any
forall a b. a -> b
coe [Any]
v2)
MAlonzo.Code.Utils.C__'8759'__388 Any
v3 [Any]
v4
-> (Any -> [Any] -> [Any])
-> Any
-> Any
-> T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
forall a b. a -> b
coe
Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Utils.C__'8759'__388
((Any -> Any -> (Any, Any)) -> Any -> Any -> Any
forall a b. a -> b
coe Any -> Any -> (Any, Any)
forall {a} {b}. a -> b -> (a, b)
MAlonzo.Code.Utils.C__'44'__378 (Any -> Any
forall a b. a -> b
coe Any
v1) (Any -> Any
forall a b. a -> b
coe Any
v3))
(([T__'8866'_14]
-> T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14))
-> Any -> Any
forall a b. a -> b
coe [T__'8866'_14]
-> T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
du_buildPairs_264 ([Any] -> Any
forall a b. a -> b
coe [Any]
v2))
[Any]
_ -> T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
forall {t}. t
MAlonzo.RTE.mazUnreachableError
[Any]
_ -> T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
forall {t}. t
MAlonzo.RTE.mazUnreachableError
d_traverseEitherList_280 ::
() ->
() ->
() ->
(AgdaAny -> MAlonzo.Code.Utils.T_Either_6 AgdaAny AgdaAny) ->
MAlonzo.Code.Utils.T_List_382 AgdaAny ->
MAlonzo.Code.Utils.T_Either_6
AgdaAny (MAlonzo.Code.Utils.T_List_382 AgdaAny)
d_traverseEitherList_280 :: ()
-> ()
-> ()
-> (Any -> T_Either_6 Any Any)
-> [Any]
-> T_Either_6 Any [Any]
d_traverseEitherList_280 ~()
v0 ~()
v1 ~()
v2 Any -> T_Either_6 Any Any
v3 [Any]
v4
= (Any -> T_Either_6 Any Any) -> [Any] -> T_Either_6 Any [Any]
du_traverseEitherList_280 Any -> T_Either_6 Any Any
v3 [Any]
v4
du_traverseEitherList_280 ::
(AgdaAny -> MAlonzo.Code.Utils.T_Either_6 AgdaAny AgdaAny) ->
MAlonzo.Code.Utils.T_List_382 AgdaAny ->
MAlonzo.Code.Utils.T_Either_6
AgdaAny (MAlonzo.Code.Utils.T_List_382 AgdaAny)
du_traverseEitherList_280 :: (Any -> T_Either_6 Any Any) -> [Any] -> T_Either_6 Any [Any]
du_traverseEitherList_280 Any -> T_Either_6 Any Any
v0 [Any]
v1
= case [Any] -> [Any]
forall a b. a -> b
coe [Any]
v1 of
[Any]
MAlonzo.Code.Utils.C_'91''93'_386
-> (Any -> T_Either_6 Any Any) -> Any -> T_Either_6 Any [Any]
forall a b. a -> b
coe Any -> T_Either_6 Any Any
forall {a} {b}. b -> Either a b
MAlonzo.Code.Utils.C_inj'8322'_14 ([Any] -> Any
forall a b. a -> b
coe [Any]
v1)
MAlonzo.Code.Utils.C__'8759'__388 Any
v2 [Any]
v3
-> let v4 :: t
v4 = (Any -> T_Either_6 Any Any) -> Any -> t
forall a b. a -> b
coe Any -> T_Either_6 Any Any
v0 Any
v2 in
Any -> T_Either_6 Any [Any]
forall a b. a -> b
coe
(case Any -> T_Either_6 Any Any
forall a b. a -> b
coe Any
forall {t}. t
v4 of
MAlonzo.Code.Utils.C_inj'8321'_12 Any
v5 -> Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v4
MAlonzo.Code.Utils.C_inj'8322'_14 Any
v5
-> let v6 :: t
v6 = ((Any -> T_Either_6 Any Any) -> [Any] -> T_Either_6 Any [Any])
-> Any -> Any -> t
forall a b. a -> b
coe (Any -> T_Either_6 Any Any) -> [Any] -> T_Either_6 Any [Any]
du_traverseEitherList_280 ((Any -> T_Either_6 Any Any) -> Any
forall a b. a -> b
coe Any -> T_Either_6 Any Any
v0) ([Any] -> Any
forall a b. a -> b
coe [Any]
v3) in
Any -> Any
forall a b. a -> b
coe
(case Any -> T_Either_6 Any Any
forall a b. a -> b
coe Any
forall {t}. t
v6 of
MAlonzo.Code.Utils.C_inj'8321'_12 Any
v7 -> Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v6
MAlonzo.Code.Utils.C_inj'8322'_14 Any
v7
-> (Any -> T_Either_6 Any Any) -> Any -> Any
forall a b. a -> b
coe
Any -> T_Either_6 Any Any
forall {a} {b}. b -> Either a b
MAlonzo.Code.Utils.C_inj'8322'_14
((Any -> [Any] -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe Any -> [Any] -> [Any]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Utils.C__'8759'__388 (Any -> Any
forall a b. a -> b
coe Any
v5) (Any -> Any
forall a b. a -> b
coe Any
v7))
T_Either_6 Any Any
_ -> Any
forall {t}. t
MAlonzo.RTE.mazUnreachableError)
T_Either_6 Any Any
_ -> Any
forall {t}. t
MAlonzo.RTE.mazUnreachableError)
[Any]
_ -> T_Either_6 Any [Any]
forall {t}. t
MAlonzo.RTE.mazUnreachableError
d_certifier_334 ::
() ->
MAlonzo.Code.Utils.T_List_382 MAlonzo.Code.RawU.T_Untyped_146 ->
(MAlonzo.Code.Utils.T_List_382
(MAlonzo.Code.Utils.T__'215'__364
MAlonzo.Code.Untyped.T__'8866'_14
MAlonzo.Code.Untyped.T__'8866'_14) ->
MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
MAlonzo.Code.Utils.T_Either_6
MAlonzo.Code.Scoped.T_ScopeError_576
MAlonzo.Code.Agda.Builtin.String.T_String_6
d_certifier_334 :: ()
-> T_List_382 T_Untyped_146
-> (T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
-> T_Dec_32)
-> T_Either_6 T_ScopeError_576 Text
d_certifier_334 ~()
v0 T_List_382 T_Untyped_146
v1 T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14) -> T_Dec_32
v2 = T_List_382 T_Untyped_146
-> (T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
-> T_Dec_32)
-> T_Either_6 T_ScopeError_576 Text
du_certifier_334 T_List_382 T_Untyped_146
v1 T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14) -> T_Dec_32
v2
du_certifier_334 ::
MAlonzo.Code.Utils.T_List_382 MAlonzo.Code.RawU.T_Untyped_146 ->
(MAlonzo.Code.Utils.T_List_382
(MAlonzo.Code.Utils.T__'215'__364
MAlonzo.Code.Untyped.T__'8866'_14
MAlonzo.Code.Untyped.T__'8866'_14) ->
MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
MAlonzo.Code.Utils.T_Either_6
MAlonzo.Code.Scoped.T_ScopeError_576
MAlonzo.Code.Agda.Builtin.String.T_String_6
du_certifier_334 :: T_List_382 T_Untyped_146
-> (T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
-> T_Dec_32)
-> T_Either_6 T_ScopeError_576 Text
du_certifier_334 T_List_382 T_Untyped_146
v0 T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14) -> T_Dec_32
v1
= let v2 :: t
v2
= ((Any -> T_Either_6 Any Any) -> [Any] -> T_Either_6 Any [Any])
-> Any -> Any -> t
forall a b. a -> b
coe
(Any -> T_Either_6 Any Any) -> [Any] -> T_Either_6 Any [Any]
du_traverseEitherList_280
((T_Untyped_146 -> T_Either_6 T_ScopeError_576 T__'8866'_14) -> Any
forall a b. a -> b
coe T_Untyped_146 -> T_Either_6 T_ScopeError_576 T__'8866'_14
MAlonzo.Code.Untyped.du_toWellScoped_358) (T_List_382 T_Untyped_146 -> Any
forall a b. a -> b
coe T_List_382 T_Untyped_146
v0) in
Any -> T_Either_6 T_ScopeError_576 Text
forall a b. a -> b
coe
(case Any -> T_Either_6 Any Any
forall a b. a -> b
coe Any
forall {t}. t
v2 of
MAlonzo.Code.Utils.C_inj'8321'_12 Any
v3 -> Any -> Any
forall a b. a -> b
coe Any
forall {t}. t
v2
MAlonzo.Code.Utils.C_inj'8322'_14 Any
v3
-> (Any -> T_Either_6 Any Any) -> Any -> Any
forall a b. a -> b
coe
Any -> T_Either_6 Any Any
forall {a} {b}. b -> Either a b
MAlonzo.Code.Utils.C_inj'8322'_14
((T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
-> T_Dec_32 -> Text)
-> Any -> Any -> Any
forall a b. a -> b
coe
T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
-> T_Dec_32 -> Text
du_serializeTraceProof_248 (([T__'8866'_14]
-> T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14))
-> Any -> Any
forall a b. a -> b
coe [T__'8866'_14]
-> T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
du_buildPairs_264 (Any -> Any
forall a b. a -> b
coe Any
v3))
((T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14) -> T_Dec_32)
-> Any -> Any
forall a b. a -> b
coe T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14) -> T_Dec_32
v1 (([T__'8866'_14]
-> T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14))
-> Any -> Any
forall a b. a -> b
coe [T__'8866'_14]
-> T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
du_buildPairs_264 (Any -> Any
forall a b. a -> b
coe Any
v3))))
T_Either_6 Any Any
_ -> Any
forall {t}. t
MAlonzo.RTE.mazUnreachableError)
runCertifier ::
MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
MAlonzo.Code.Utils.T_List_382 MAlonzo.Code.RawU.T_Untyped_146 ->
MAlonzo.Code.Agda.Builtin.IO.T_IO_8
() MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6
runCertifier :: Text -> T_List_382 T_Untyped_146 -> T_IO_8 () ()
runCertifier = (Text -> T_List_382 T_Untyped_146 -> T_IO_8 () ())
-> Text -> T_List_382 T_Untyped_146 -> T_IO_8 () ()
forall a b. a -> b
coe Text -> T_List_382 T_Untyped_146 -> T_IO_8 () ()
d_runCertifier_364
d_runCertifier_364 ::
MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
MAlonzo.Code.Utils.T_List_382 MAlonzo.Code.RawU.T_Untyped_146 ->
MAlonzo.Code.Agda.Builtin.IO.T_IO_8
AgdaAny MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6
d_runCertifier_364 :: Text -> T_List_382 T_Untyped_146 -> T_IO_8 () ()
d_runCertifier_364 Text
v0 T_List_382 T_Untyped_146
v1
= let v2 :: t
v2
= (T_List_382 T_Untyped_146
-> (T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
-> T_Dec_32)
-> T_Either_6 T_ScopeError_576 Text)
-> Any -> Any -> t
forall a b. a -> b
coe
T_List_382 T_Untyped_146
-> (T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
-> T_Dec_32)
-> T_Either_6 T_ScopeError_576 Text
du_certifier_334 (T_List_382 T_Untyped_146 -> Any
forall a b. a -> b
coe T_List_382 T_Untyped_146
v1)
(((T__'8866'_14 -> T__'8866'_14 -> T_Dec_32)
-> T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14)
-> T_Dec_32)
-> Any -> Any
forall a b. a -> b
coe
(T__'8866'_14 -> T__'8866'_14 -> T_Dec_32)
-> T_List_382 (T__'215'__364 T__'8866'_14 T__'8866'_14) -> T_Dec_32
du_isTrace'63'_46
((()
-> T_DecEq_6
-> (() -> T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_32)
-> T__'8866'_14
-> T__'8866'_14
-> T_Dec_32)
-> Any -> Any -> (Any -> Any -> Any -> Any -> Any) -> Any
forall a b. a -> b
coe
()
-> T_DecEq_6
-> (() -> T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_32)
-> T__'8866'_14
-> T__'8866'_14
-> T_Dec_32
MAlonzo.Code.VerifiedCompilation.UntypedTranslation.du_translation'63'_114
Any
forall {t}. t
erased
((T_DecEq_6 -> T_DecEq_6) -> Any -> Any
forall a b. a -> b
coe
T_DecEq_6 -> T_DecEq_6
MAlonzo.Code.VerifiedCompilation.Equality.du_DecEq'45'Maybe_122
(T_DecEq_6 -> Any
forall a b. a -> b
coe T_DecEq_6
MAlonzo.Code.VerifiedCompilation.Equality.d_EmptyEq_128))
(\ Any
v2 Any
v3 Any
v4 Any
v5 -> (T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_32)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_Dec_32
du_isTransformation'63'_150 Any
v3 Any
v4 Any
v5))) in
Any -> T_IO_8 () ()
forall a b. a -> b
coe
(case Any -> T_Either_6 Any Any
forall a b. a -> b
coe Any
forall {t}. t
v2 of
MAlonzo.Code.Utils.C_inj'8321'_12 Any
v3
-> (T_FileHandle_254 -> Text -> T_IO_8 () ())
-> T_FileHandle_254 -> Text -> Any
forall a b. a -> b
coe T_FileHandle_254 -> Text -> T_IO_8 () ()
d_hPutStrLn_260 T_FileHandle_254
d_stderr_258 (Text
"error" :: Data.Text.Text)
MAlonzo.Code.Utils.C_inj'8322'_14 Any
v3
-> (Text -> Text -> T_IO_8 () ()) -> Any -> Any -> Any
forall a b. a -> b
coe
Text -> Text -> T_IO_8 () ()
d_writeFile_256
((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
".agda" :: Data.Text.Text))
Any
v3
T_Either_6 Any Any
_ -> Any
forall {t}. t
MAlonzo.RTE.mazUnreachableError)