diff --git a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Transform/Certify/Trace.hs b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Transform/Certify/Trace.hs index 8539c3e9a51..506400fa167 100644 --- a/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Transform/Certify/Trace.hs +++ b/plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Transform/Certify/Trace.hs @@ -28,6 +28,7 @@ data CertifiedOptStage | ApplyToCase | CaseReduce | LetFloatOut + | PolyBuiltin deriving stock (Show, Generic) deriving anyclass (NFData) @@ -44,7 +45,6 @@ at https://github.com/IntersectMBO/plutus/issues. -} data UncertifiedOptStage = CaseOfCase | ConstantFolding - | PolyBuiltin deriving stock (Show, Generic) deriving anyclass (NFData) @@ -81,7 +81,7 @@ pattern ConstantFoldingStage :: OptStage pattern ConstantFoldingStage = Left ConstantFolding pattern PolyBuiltinStage :: OptStage -pattern PolyBuiltinStage = Left PolyBuiltin +pattern PolyBuiltinStage = Right PolyBuiltin {-# COMPLETE FloatDelayStage diff --git a/plutus-metatheory/src/CertifierReport.lagda.md b/plutus-metatheory/src/CertifierReport.lagda.md index e9ff18e009b..6d7c286d042 100644 --- a/plutus-metatheory/src/CertifierReport.lagda.md +++ b/plutus-metatheory/src/CertifierReport.lagda.md @@ -13,6 +13,7 @@ open import VerifiedCompilation.UntypedTranslation open import VerifiedCompilation.UInline open import VerifiedCompilation.UCaseReduce as CR import VerifiedCompilation.FloatOut as FloatOut +open import VerifiedCompilation.UCSE as CSE open import Untyped.Relation.Binary.Modular open import Untyped.Relation.Binary.Core renaming (Pointwise to PW) open import Untyped @@ -48,11 +49,11 @@ showCertifiedOptTag cseT = "Common Subexpression Elimination" showCertifiedOptTag applyToCaseT = "Transform multi-argument applications into case-constr form" showCertifiedOptTag caseReduceT = "Case-Constr and Case-Constant Cancellation" showCertifiedOptTag letFloatOutT = "Float bindings outwards" +showCertifiedOptTag polyBuiltinT = "Hoist Polymorphic Builtins" showUncertifiedOptTag : UncertifiedOptTag → String showUncertifiedOptTag caseOfCaseT = "Case-of-Case" showUncertifiedOptTag constantFoldingT = "Constant Folding" -showUncertifiedOptTag polyBuiltinT = "Hoist Polymorphic Builtins" showTag : OptTag → String showTag (inj₁ tag) = showUncertifiedOptTag tag ++ " ⚠ (certifier unavailable)" @@ -129,6 +130,7 @@ numSites forceCaseDelayT p = numSites′ p numSites applyToCaseT p = numSites′ p numSites {M = M} caseReduceT p = numSitesCaseReduce (CR.sound {M = M} p) numSites letFloatOutT p = FloatOut.numSites p +numSites polyBuiltinT p = CSE.polyNumSites p showSites : {M N : 0 ⊢} → (tag : OptTag) → RelationOf tag M N → String showSites (inj₁ _) _ = "" diff --git a/plutus-metatheory/src/FFI/AgdaUnparse.hs b/plutus-metatheory/src/FFI/AgdaUnparse.hs index 69a864614c4..2596f260e05 100644 --- a/plutus-metatheory/src/FFI/AgdaUnparse.hs +++ b/plutus-metatheory/src/FFI/AgdaUnparse.hs @@ -74,11 +74,11 @@ instance AgdaUnparse CertifiedOptStage where agdaUnparse ApplyToCase = "applyToCaseT" agdaUnparse CaseReduce = "caseReduceT" agdaUnparse LetFloatOut = "letFloatOutT" + agdaUnparse PolyBuiltin = "polyBuiltinT" instance AgdaUnparse UncertifiedOptStage where agdaUnparse CaseOfCase = "caseOfCaseT" agdaUnparse ConstantFolding = "constantFoldingT" - agdaUnparse PolyBuiltin = "polyBuiltinT" instance AgdaUnparse Hints.Hints where agdaUnparse = \case diff --git a/plutus-metatheory/src/MAlonzo/Code/Certifier.hs b/plutus-metatheory/src/MAlonzo/Code/Certifier.hs index 477421728cb..8381f44de56 100644 --- a/plutus-metatheory/src/MAlonzo/Code/Certifier.hs +++ b/plutus-metatheory/src/MAlonzo/Code/Certifier.hs @@ -34,7 +34,7 @@ d_runCertifier_2 :: (MAlonzo.Code.Utils.T__'215'__436 (MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_12) + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10) MAlonzo.Code.VerifiedCompilation.Trace.T_Hints_80) MAlonzo.Code.RawU.T_Untyped_210 -> MAlonzo.Code.Utils.T_Either_6 @@ -65,7 +65,7 @@ runCertifierMain :: (MAlonzo.Code.Utils.T__'215'__436 (MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_12) + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10) MAlonzo.Code.VerifiedCompilation.Trace.T_Hints_80) MAlonzo.Code.RawU.T_Untyped_210 -> MAlonzo.Code.Agda.Builtin.List.T_List_10 @@ -80,7 +80,7 @@ d_runCertifierMain_10 :: (MAlonzo.Code.Utils.T__'215'__436 (MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_12) + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10) MAlonzo.Code.VerifiedCompilation.Trace.T_Hints_80) MAlonzo.Code.RawU.T_Untyped_210 -> [MAlonzo.Code.VerifiedCompilation.Trace.T_EvalResult_122] -> @@ -104,7 +104,7 @@ d_runCertifierMain_10 v0 v1 MAlonzo.Code.Utils.C__'44'__450 (coe MAlonzo.Code.Agda.Builtin.Bool.C_false_8) (coe - MAlonzo.Code.CertifierReport.d_makeReport_290 (coe v2) (coe v1))) + MAlonzo.Code.CertifierReport.d_makeReport_292 (coe v2) (coe v1))) MAlonzo.Code.VerifiedCompilation.C_abort_10 v4 -> coe MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 @@ -112,7 +112,7 @@ d_runCertifierMain_10 v0 v1 MAlonzo.Code.Utils.C__'44'__450 (coe MAlonzo.Code.Agda.Builtin.Bool.C_false_8) (coe - MAlonzo.Code.CertifierReport.d_makeReport_290 (coe v2) (coe v1))) + MAlonzo.Code.CertifierReport.d_makeReport_292 (coe v2) (coe v1))) _ -> MAlonzo.RTE.mazUnreachableError MAlonzo.Code.Utils.C_inj'8322'_14 v3 -> coe @@ -123,5 +123,5 @@ d_runCertifierMain_10 v0 v1 MAlonzo.Code.Utils.C__'44'__450 (coe MAlonzo.Code.Agda.Builtin.Bool.C_true_10) (coe - MAlonzo.Code.CertifierReport.d_makeReport_290 (coe v2) (coe v1)))) + MAlonzo.Code.CertifierReport.d_makeReport_292 (coe v2) (coe v1)))) _ -> MAlonzo.RTE.mazUnreachableError) diff --git a/plutus-metatheory/src/MAlonzo/Code/CertifierReport.hs b/plutus-metatheory/src/MAlonzo/Code/CertifierReport.hs index dea2d0e132c..811cb47ed8a 100644 --- a/plutus-metatheory/src/MAlonzo/Code/CertifierReport.hs +++ b/plutus-metatheory/src/MAlonzo/Code/CertifierReport.hs @@ -29,6 +29,7 @@ import qualified MAlonzo.Code.Utils import qualified MAlonzo.Code.VerifiedCompilation import qualified MAlonzo.Code.VerifiedCompilation.FloatOut import qualified MAlonzo.Code.VerifiedCompilation.Trace +import qualified MAlonzo.Code.VerifiedCompilation.UCSE import qualified MAlonzo.Code.VerifiedCompilation.UCaseReduce import qualified MAlonzo.Code.VerifiedCompilation.UInline import qualified MAlonzo.Code.VerifiedCompilation.UntypedTranslation @@ -53,30 +54,32 @@ d_hl_8 Data.Text.Text) -- CertifierReport.showCertifiedOptTag d_showCertifiedOptTag_10 :: - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_12 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> MAlonzo.Code.Agda.Builtin.String.T_String_6 d_showCertifiedOptTag_10 v0 = case coe v0 of - MAlonzo.Code.VerifiedCompilation.Trace.C_floatDelayT_14 + MAlonzo.Code.VerifiedCompilation.Trace.C_floatDelayT_12 -> coe ("Float Delay" :: Data.Text.Text) - MAlonzo.Code.VerifiedCompilation.Trace.C_forceDelayT_16 + MAlonzo.Code.VerifiedCompilation.Trace.C_forceDelayT_14 -> coe ("Force-Delay Cancellation" :: Data.Text.Text) - MAlonzo.Code.VerifiedCompilation.Trace.C_forceCaseDelayT_18 + MAlonzo.Code.VerifiedCompilation.Trace.C_forceCaseDelayT_16 -> coe ("Float Force into Case Branches" :: Data.Text.Text) - MAlonzo.Code.VerifiedCompilation.Trace.C_inlineT_20 + MAlonzo.Code.VerifiedCompilation.Trace.C_inlineT_18 -> coe ("Inlining" :: Data.Text.Text) - MAlonzo.Code.VerifiedCompilation.Trace.C_cseT_22 + MAlonzo.Code.VerifiedCompilation.Trace.C_cseT_20 -> coe ("Common Subexpression Elimination" :: Data.Text.Text) - MAlonzo.Code.VerifiedCompilation.Trace.C_applyToCaseT_24 + MAlonzo.Code.VerifiedCompilation.Trace.C_applyToCaseT_22 -> coe ("Transform multi-argument applications into case-constr form" :: Data.Text.Text) - MAlonzo.Code.VerifiedCompilation.Trace.C_caseReduceT_26 + MAlonzo.Code.VerifiedCompilation.Trace.C_caseReduceT_24 -> coe ("Case-Constr and Case-Constant Cancellation" :: Data.Text.Text) - MAlonzo.Code.VerifiedCompilation.Trace.C_letFloatOutT_28 + MAlonzo.Code.VerifiedCompilation.Trace.C_letFloatOutT_26 -> coe ("Float bindings outwards" :: Data.Text.Text) + MAlonzo.Code.VerifiedCompilation.Trace.C_polyBuiltinT_28 + -> coe ("Hoist Polymorphic Builtins" :: Data.Text.Text) _ -> MAlonzo.RTE.mazUnreachableError -- CertifierReport.showUncertifiedOptTag d_showUncertifiedOptTag_12 :: @@ -88,14 +91,12 @@ d_showUncertifiedOptTag_12 v0 -> coe ("Case-of-Case" :: Data.Text.Text) MAlonzo.Code.VerifiedCompilation.Trace.C_constantFoldingT_8 -> coe ("Constant Folding" :: Data.Text.Text) - MAlonzo.Code.VerifiedCompilation.Trace.C_polyBuiltinT_10 - -> coe ("Hoist Polymorphic Builtins" :: Data.Text.Text) _ -> MAlonzo.RTE.mazUnreachableError -- CertifierReport.showTag d_showTag_14 :: MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_12 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> MAlonzo.Code.Agda.Builtin.String.T_String_6 d_showTag_14 v0 = case coe v0 of @@ -565,48 +566,52 @@ d_numSitesInline_140 v0 v1 v2 v3 v4 v5 v6 v7 d_numSites_178 :: MAlonzo.Code.Untyped.T__'8866'_14 -> MAlonzo.Code.Untyped.T__'8866'_14 -> - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_12 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> AgdaAny -> Integer d_numSites_178 v0 v1 v2 v3 = case coe v2 of - MAlonzo.Code.VerifiedCompilation.Trace.C_floatDelayT_14 + MAlonzo.Code.VerifiedCompilation.Trace.C_floatDelayT_12 -> coe du_numSites'8242'_26 v0 v1 v3 - MAlonzo.Code.VerifiedCompilation.Trace.C_forceDelayT_16 + MAlonzo.Code.VerifiedCompilation.Trace.C_forceDelayT_14 -> coe du_numSites'8242'_26 v0 v1 v3 - MAlonzo.Code.VerifiedCompilation.Trace.C_forceCaseDelayT_18 + MAlonzo.Code.VerifiedCompilation.Trace.C_forceCaseDelayT_16 -> coe du_numSites'8242'_26 v0 v1 v3 - MAlonzo.Code.VerifiedCompilation.Trace.C_inlineT_20 + MAlonzo.Code.VerifiedCompilation.Trace.C_inlineT_18 -> coe d_numSitesInline_140 (coe (0 :: Integer)) erased (coe MAlonzo.Code.VerifiedCompilation.UInline.C_'9633'_32) (coe MAlonzo.Code.VerifiedCompilation.UInline.C_'9633'_32) (coe MAlonzo.Code.VerifiedCompilation.UInline.C_'9633'_106) (coe v0) (coe v1) (coe v3) - MAlonzo.Code.VerifiedCompilation.Trace.C_cseT_22 + MAlonzo.Code.VerifiedCompilation.Trace.C_cseT_20 -> coe du_numSites'8242'_26 v0 v1 v3 - MAlonzo.Code.VerifiedCompilation.Trace.C_applyToCaseT_24 + MAlonzo.Code.VerifiedCompilation.Trace.C_applyToCaseT_22 -> coe du_numSites'8242'_26 v0 v1 v3 - MAlonzo.Code.VerifiedCompilation.Trace.C_caseReduceT_26 + MAlonzo.Code.VerifiedCompilation.Trace.C_caseReduceT_24 -> coe MAlonzo.Code.VerifiedCompilation.UCaseReduce.d_numSitesCaseReduce_578 (coe (0 :: Integer)) (coe v0) (coe v1) (coe MAlonzo.Code.VerifiedCompilation.UCaseReduce.du_sound_568 (coe (0 :: Integer)) (coe v0)) - MAlonzo.Code.VerifiedCompilation.Trace.C_letFloatOutT_28 + MAlonzo.Code.VerifiedCompilation.Trace.C_letFloatOutT_26 -> coe MAlonzo.Code.VerifiedCompilation.FloatOut.d_numSites_330 (coe (0 :: Integer)) (coe v0) (coe v1) (coe v3) + MAlonzo.Code.VerifiedCompilation.Trace.C_polyBuiltinT_28 + -> coe + MAlonzo.Code.VerifiedCompilation.UCSE.du_polyNumSites_400 (coe v1) + (coe v3) _ -> MAlonzo.RTE.mazUnreachableError -- CertifierReport.showSites -d_showSites_204 :: +d_showSites_206 :: MAlonzo.Code.Untyped.T__'8866'_14 -> MAlonzo.Code.Untyped.T__'8866'_14 -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_12 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> AgdaAny -> MAlonzo.Code.Agda.Builtin.String.T_String_6 -d_showSites_204 v0 v1 v2 v3 +d_showSites_206 v0 v1 v2 v3 = case coe v2 of MAlonzo.Code.Utils.C_inj'8321'_12 v4 -> coe ("" :: Data.Text.Text) MAlonzo.Code.Utils.C_inj'8322'_14 v4 @@ -620,59 +625,59 @@ d_showSites_204 v0 v1 v2 v3 (d_numSites_178 (coe v0) (coe v1) (coe v4) (coe v3)))) _ -> MAlonzo.RTE.mazUnreachableError -- CertifierReport.termSize -d_termSize_212 :: +d_termSize_214 :: Integer -> MAlonzo.Code.Untyped.T__'8866'_14 -> Integer -d_termSize_212 v0 v1 +d_termSize_214 v0 v1 = case coe v1 of MAlonzo.Code.Untyped.C_'96'_18 v2 -> coe (1 :: Integer) MAlonzo.Code.Untyped.C_ƛ_20 v2 -> coe addInt (coe (1 :: Integer)) (coe - d_termSize_212 (coe addInt (coe (1 :: Integer)) (coe v0)) (coe v2)) + d_termSize_214 (coe addInt (coe (1 :: Integer)) (coe v0)) (coe v2)) MAlonzo.Code.Untyped.C__'183'__22 v2 v3 -> coe addInt (coe - addInt (coe (1 :: Integer)) (coe d_termSize_212 (coe v0) (coe v2))) - (coe d_termSize_212 (coe v0) (coe v3)) + addInt (coe (1 :: Integer)) (coe d_termSize_214 (coe v0) (coe v2))) + (coe d_termSize_214 (coe v0) (coe v3)) MAlonzo.Code.Untyped.C_force_24 v2 -> coe - addInt (coe (1 :: Integer)) (coe d_termSize_212 (coe v0) (coe v2)) + addInt (coe (1 :: Integer)) (coe d_termSize_214 (coe v0) (coe v2)) MAlonzo.Code.Untyped.C_delay_26 v2 -> coe - addInt (coe (1 :: Integer)) (coe d_termSize_212 (coe v0) (coe v2)) + addInt (coe (1 :: Integer)) (coe d_termSize_214 (coe v0) (coe v2)) MAlonzo.Code.Untyped.C_con_28 v2 -> coe (1 :: Integer) MAlonzo.Code.Untyped.C_constr_34 v2 v3 -> coe addInt (coe (1 :: Integer)) - (coe d_termSize'7510''695'_216 (coe v0) (coe v3)) + (coe d_termSize'7510''695'_218 (coe v0) (coe v3)) MAlonzo.Code.Untyped.C_case_40 v2 v3 -> coe addInt (coe addInt (coe (1 :: Integer)) - (coe d_termSize'7510''695'_216 (coe v0) (coe v3))) - (coe d_termSize_212 (coe v0) (coe v2)) + (coe d_termSize'7510''695'_218 (coe v0) (coe v3))) + (coe d_termSize_214 (coe v0) (coe v2)) MAlonzo.Code.Untyped.C_builtin_44 v2 -> coe (1 :: Integer) MAlonzo.Code.Untyped.C_error_46 -> coe (1 :: Integer) _ -> MAlonzo.RTE.mazUnreachableError -- CertifierReport.termSizeᵖʷ -d_termSize'7510''695'_216 :: +d_termSize'7510''695'_218 :: Integer -> [MAlonzo.Code.Untyped.T__'8866'_14] -> Integer -d_termSize'7510''695'_216 v0 v1 +d_termSize'7510''695'_218 v0 v1 = case coe v1 of [] -> coe (0 :: Integer) (:) v2 v3 -> coe - addInt (coe d_termSize'7510''695'_216 (coe v0) (coe v3)) - (coe d_termSize_212 (coe v0) (coe v2)) + addInt (coe d_termSize'7510''695'_218 (coe v0) (coe v3)) + (coe d_termSize_214 (coe v0) (coe v2)) _ -> MAlonzo.RTE.mazUnreachableError -- CertifierReport.showEvalResult -d_showEvalResult_238 :: +d_showEvalResult_240 :: MAlonzo.Code.VerifiedCompilation.Trace.T_EvalResult_122 -> MAlonzo.Code.Agda.Builtin.String.T_String_6 -d_showEvalResult_238 v0 +d_showEvalResult_240 v0 = case coe v0 of MAlonzo.Code.VerifiedCompilation.Trace.C_success_124 v1 v2 -> coe @@ -705,10 +710,10 @@ d_showEvalResult_238 v0 (coe MAlonzo.Code.Data.Nat.Show.d_show_56 v3)))))) _ -> MAlonzo.RTE.mazUnreachableError -- CertifierReport.showCostPair -d_showCostPair_250 :: +d_showCostPair_252 :: [MAlonzo.Code.VerifiedCompilation.Trace.T_EvalResult_122] -> MAlonzo.Code.Agda.Builtin.String.T_String_6 -d_showCostPair_250 v0 +d_showCostPair_252 v0 = let v1 = "" :: Data.Text.Text in coe (case coe v0 of @@ -717,7 +722,7 @@ d_showCostPair_250 v0 (:) v4 v5 -> coe MAlonzo.Code.Data.String.Base.d__'43''43'__20 - (d_showEvalResult_238 (coe v2)) + (d_showEvalResult_240 (coe v2)) (coe MAlonzo.Code.Data.String.Base.d__'43''43'__20 (" (before)" :: Data.Text.Text) @@ -725,32 +730,32 @@ d_showCostPair_250 v0 MAlonzo.Code.Data.String.Base.d__'43''43'__20 d_nl_6 (coe MAlonzo.Code.Data.String.Base.d__'43''43'__20 - (d_showEvalResult_238 (coe v4)) (" (after)" :: Data.Text.Text)))) + (d_showEvalResult_240 (coe v4)) (" (after)" :: Data.Text.Text)))) _ -> coe v1 _ -> coe v1) -- CertifierReport.tail -d_tail_258 :: () -> [AgdaAny] -> [AgdaAny] -d_tail_258 ~v0 v1 = du_tail_258 v1 -du_tail_258 :: [AgdaAny] -> [AgdaAny] -du_tail_258 v0 +d_tail_260 :: () -> [AgdaAny] -> [AgdaAny] +d_tail_260 ~v0 v1 = du_tail_260 v1 +du_tail_260 :: [AgdaAny] -> [AgdaAny] +du_tail_260 v0 = case coe v0 of [] -> coe v0 (:) v1 v2 -> coe v2 _ -> MAlonzo.RTE.mazUnreachableError -- CertifierReport.reportPasses -d_reportPasses_268 :: +d_reportPasses_270 :: Integer -> MAlonzo.Code.VerifiedCompilation.Trace.T_NonEmptySep_90 (MAlonzo.Code.Utils.T__'215'__436 (MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_12) + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10) MAlonzo.Code.VerifiedCompilation.Trace.T_Hints_80) MAlonzo.Code.Untyped.T__'8866'_14 -> AgdaAny -> [MAlonzo.Code.VerifiedCompilation.Trace.T_EvalResult_122] -> MAlonzo.Code.Agda.Builtin.String.T_String_6 -d_reportPasses_268 v0 v1 v2 v3 +d_reportPasses_270 v0 v1 v2 v3 = case coe v1 of MAlonzo.Code.VerifiedCompilation.Trace.C_cons_96 v4 v5 v6 -> case coe v5 of @@ -781,7 +786,7 @@ d_reportPasses_268 v0 v1 v2 v3 MAlonzo.Code.Data.String.Base.d__'43''43'__20 (coe MAlonzo.Code.Data.Nat.Show.d_show_56 - (d_termSize_212 (coe (0 :: Integer)) (coe v4))) + (d_termSize_214 (coe (0 :: Integer)) (coe v4))) (coe MAlonzo.Code.Data.String.Base.d__'43''43'__20 (" (before)" :: Data.Text.Text) @@ -799,7 +804,7 @@ d_reportPasses_268 v0 v1 v2 v3 MAlonzo.Code.Data.String.Base.d__'43''43'__20 (coe MAlonzo.Code.Data.Nat.Show.d_show_56 - (d_termSize_212 + (d_termSize_214 (coe (0 :: Integer)) (coe MAlonzo.Code.VerifiedCompilation.Trace.d_head_112 @@ -812,13 +817,13 @@ d_reportPasses_268 v0 v1 v2 v3 d_nl_6 (coe MAlonzo.Code.Data.String.Base.d__'43''43'__20 - (d_showCostPair_250 (coe v3)) + (d_showCostPair_252 (coe v3)) (coe MAlonzo.Code.Data.String.Base.d__'43''43'__20 d_nl_6 (coe MAlonzo.Code.Data.String.Base.d__'43''43'__20 - (d_showSites_204 + (d_showSites_206 (coe v4) (coe MAlonzo.Code.VerifiedCompilation.Trace.d_head_112 @@ -827,7 +832,7 @@ d_reportPasses_268 v0 v1 v2 v3 (coe MAlonzo.Code.Data.String.Base.d__'43''43'__20 d_nl_6 - (d_reportPasses_268 + (d_reportPasses_270 (coe addInt (coe @@ -836,7 +841,7 @@ d_reportPasses_268 v0 v1 v2 v3 (coe v0)) (coe v6) (coe v10) (coe - du_tail_258 + du_tail_260 (coe v3)))))))))))))))))))) _ -> MAlonzo.RTE.mazUnreachableError @@ -845,10 +850,10 @@ d_reportPasses_268 v0 v1 v2 v3 -> coe ("" :: Data.Text.Text) _ -> MAlonzo.RTE.mazUnreachableError -- CertifierReport.reportFailure -d_reportFailure_284 :: +d_reportFailure_286 :: MAlonzo.Code.VerifiedCompilation.T_Error_2 -> MAlonzo.Code.Agda.Builtin.String.T_String_6 -d_reportFailure_284 v0 +d_reportFailure_286 v0 = case coe v0 of MAlonzo.Code.VerifiedCompilation.C_emptyDump_4 -> coe @@ -892,24 +897,24 @@ d_reportFailure_284 v0 (" \10060 FAILED" :: Data.Text.Text) d_hl_8))) _ -> MAlonzo.RTE.mazUnreachableError -- CertifierReport.makeReport -d_makeReport_290 :: +d_makeReport_292 :: MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.T_Error_2 MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> [MAlonzo.Code.VerifiedCompilation.Trace.T_EvalResult_122] -> MAlonzo.Code.Agda.Builtin.String.T_String_6 -d_makeReport_290 v0 v1 +d_makeReport_292 v0 v1 = coe MAlonzo.Code.Data.String.Base.d__'43''43'__20 ("UPLC OPTIMIZATION: CERTIFIER REPORT" :: Data.Text.Text) (coe MAlonzo.Code.Data.String.Base.d__'43''43'__20 d_nl_6 (coe - MAlonzo.Code.Utils.du_either_22 (coe v0) (coe d_reportFailure_284) + MAlonzo.Code.Utils.du_either_22 (coe v0) (coe d_reportFailure_286) (coe (\ v2 -> case coe v2 of MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 v3 v4 -> coe - d_reportPasses_268 (coe (1 :: Integer)) (coe v3) (coe v4) (coe v1) + d_reportPasses_270 (coe (1 :: Integer)) (coe v3) (coe v4) (coe v1) _ -> MAlonzo.RTE.mazUnreachableError)))) diff --git a/plutus-metatheory/src/MAlonzo/Code/Evaluator/Program.hs b/plutus-metatheory/src/MAlonzo/Code/Evaluator/Program.hs index 2a473628262..cc1a786834e 100644 --- a/plutus-metatheory/src/MAlonzo/Code/Evaluator/Program.hs +++ b/plutus-metatheory/src/MAlonzo/Code/Evaluator/Program.hs @@ -205,7 +205,7 @@ d_parseUPLC_62 v0 MAlonzo.Code.Utils.du_withE_352 (coe MAlonzo.Code.Evaluator.Base.C_scopeError_18) (coe - MAlonzo.Code.Untyped.d_scopeCheckU0_290 (coe d_convPU_32 v1)))) + MAlonzo.Code.Untyped.d_scopeCheckU0_410 (coe d_convPU_32 v1)))) -- Evaluator.Program.typeCheckPLC d_typeCheckPLC_70 :: MAlonzo.Code.Scoped.T_ScopedTm_522 -> @@ -297,7 +297,7 @@ d_executePLC_80 v0 v1 MAlonzo.Code.Utils.C_inj'8322'_14 (coe MAlonzo.Code.Evaluator.Base.d_prettyPrintUTm_10 - (MAlonzo.Code.Untyped.d_extricateU0_228 + (MAlonzo.Code.Untyped.d_extricateU0_348 (coe MAlonzo.Code.Untyped.CEK.d_discharge_126 (coe v7)))) @@ -516,7 +516,7 @@ d_showUPLCResult_138 v0 MAlonzo.Code.Utils.C_inj'8322'_14 (coe MAlonzo.Code.Evaluator.Base.d_prettyPrintUTm_10 - (MAlonzo.Code.Untyped.d_extricateU0_228 + (MAlonzo.Code.Untyped.d_extricateU0_348 (coe MAlonzo.Code.Untyped.CEK.d_discharge_126 (coe v2)))) MAlonzo.Code.Untyped.CEK.C_'9670'_228 -> coe diff --git a/plutus-metatheory/src/MAlonzo/Code/Evaluator/Term.hs b/plutus-metatheory/src/MAlonzo/Code/Evaluator/Term.hs index 2d49670e0b4..3c28f1bd095 100644 --- a/plutus-metatheory/src/MAlonzo/Code/Evaluator/Term.hs +++ b/plutus-metatheory/src/MAlonzo/Code/Evaluator/Term.hs @@ -861,7 +861,7 @@ d_runU_194 v0 MAlonzo.Code.Utils.du_withE_352 (coe MAlonzo.Code.Evaluator.Base.C_scopeError_18) (coe - MAlonzo.Code.Untyped.d_scopeCheckU0_290 (coe d_convTmU_46 v0))) + MAlonzo.Code.Untyped.d_scopeCheckU0_410 (coe d_convTmU_46 v0))) (coe (\ v1 -> coe @@ -872,7 +872,7 @@ d_runU_194 v0 MAlonzo.Code.Utils.C_inj'8322'_14 (coe d_unconvTmU_48 - (MAlonzo.Code.Untyped.d_extricateU0_228 + (MAlonzo.Code.Untyped.d_extricateU0_348 (coe MAlonzo.Code.Untyped.CEK.d_discharge_126 (coe v2)))))))) -- Evaluator.Term.runUCounting runUCountingAgda :: @@ -1327,7 +1327,7 @@ d_runUCounting_202 v0 v1 MAlonzo.Code.Utils.du_withE_352 (coe MAlonzo.Code.Evaluator.Base.C_scopeError_18) (coe - MAlonzo.Code.Untyped.d_scopeCheckU0_290 (coe d_convTmU_46 v1))) + MAlonzo.Code.Untyped.d_scopeCheckU0_410 (coe d_convTmU_46 v1))) (coe (\ v6 -> coe @@ -1365,7 +1365,7 @@ d_runUCounting_202 v0 v1 MAlonzo.Code.Utils.C__'44'__450 (coe d_unconvTmU_48 - (MAlonzo.Code.Untyped.d_extricateU0_228 + (MAlonzo.Code.Untyped.d_extricateU0_348 (coe MAlonzo.Code.Untyped.CEK.d_discharge_126 (coe v9)))) @@ -1582,7 +1582,7 @@ d_alphaU_406 v0 v1 -> case coe v7 of MAlonzo.Code.Utils.C_inj'8322'_14 v9 -> coe - MAlonzo.Code.Untyped.d_decUTm_298 + MAlonzo.Code.Untyped.d_decUTm_418 (coe d_convTmU_46 v8) (coe d_convTmU_46 v9) _ -> coe MAlonzo.Code.Agda.Builtin.Bool.C_false_8 _ -> coe MAlonzo.Code.Agda.Builtin.Bool.C_false_8)) diff --git a/plutus-metatheory/src/MAlonzo/Code/Untyped.hs b/plutus-metatheory/src/MAlonzo/Code/Untyped.hs index a657946a43e..aabd74db097 100644 --- a/plutus-metatheory/src/MAlonzo/Code/Untyped.hs +++ b/plutus-metatheory/src/MAlonzo/Code/Untyped.hs @@ -48,17 +48,17 @@ data T__'8866'_14 C_case_40 T__'8866'_14 [T__'8866'_14] | C_builtin_44 MAlonzo.Code.Builtin.T_Builtin_2 | C_error_46 -- Untyped.uglyDATA -d_uglyDATA_76 :: +d_uglyDATA_196 :: MAlonzo.Code.Utils.T_DATA_618 -> MAlonzo.Code.Agda.Builtin.String.T_String_6 -d_uglyDATA_76 ~v0 = du_uglyDATA_76 -du_uglyDATA_76 :: MAlonzo.Code.Agda.Builtin.String.T_String_6 -du_uglyDATA_76 = coe ("(DATA)" :: Data.Text.Text) +d_uglyDATA_196 ~v0 = du_uglyDATA_196 +du_uglyDATA_196 :: MAlonzo.Code.Agda.Builtin.String.T_String_6 +du_uglyDATA_196 = coe ("(DATA)" :: Data.Text.Text) -- Untyped.uglyTmCon -d_uglyTmCon_80 :: +d_uglyTmCon_200 :: MAlonzo.Code.RawU.T_TmCon_204 -> MAlonzo.Code.Agda.Builtin.String.T_String_6 -d_uglyTmCon_80 v0 +d_uglyTmCon_200 v0 = case coe v0 of MAlonzo.Code.RawU.C_tmCon_208 v1 v2 -> case coe v1 of @@ -88,7 +88,7 @@ d_uglyTmCon_80 v0 then coe ("(bool true)" :: Data.Text.Text) else coe ("(bool false)" :: Data.Text.Text) MAlonzo.Code.Builtin.Constant.AtomicType.C_aData_18 - -> coe du_uglyDATA_76 + -> coe du_uglyDATA_196 MAlonzo.Code.Builtin.Constant.AtomicType.C_aValue_20 -> coe ("(value ???)" :: Data.Text.Text) MAlonzo.Code.Builtin.Constant.AtomicType.C_aBls12'45'381'45'g1'45'element_22 @@ -104,7 +104,7 @@ d_uglyTmCon_80 v0 ("(list [ " :: Data.Text.Text) (coe MAlonzo.Code.Data.String.Base.d__'43''43'__20 - (d_uglyTmConList_84 (coe v4) (coe v2)) (" ])" :: Data.Text.Text)) + (d_uglyTmConList_204 (coe v4) (coe v2)) (" ])" :: Data.Text.Text)) MAlonzo.Code.Builtin.Signature.C_array_20 v4 -> coe ("(array [ something ])" :: Data.Text.Text) MAlonzo.Code.Builtin.Signature.C_pair_24 v4 v5 @@ -115,52 +115,52 @@ d_uglyTmCon_80 v0 ("(pair (" :: Data.Text.Text) (coe MAlonzo.Code.Data.String.Base.d__'43''43'__20 - (d_uglyTmCon_80 + (d_uglyTmCon_200 (coe MAlonzo.Code.RawU.C_tmCon_208 (coe v4) (coe v6))) (coe MAlonzo.Code.Data.String.Base.d__'43''43'__20 (" , " :: Data.Text.Text) (coe MAlonzo.Code.Data.String.Base.d__'43''43'__20 - (d_uglyTmCon_80 + (d_uglyTmCon_200 (coe MAlonzo.Code.RawU.C_tmCon_208 (coe v5) (coe v7))) (") )" :: Data.Text.Text)))) _ -> MAlonzo.RTE.mazUnreachableError _ -> MAlonzo.RTE.mazUnreachableError _ -> MAlonzo.RTE.mazUnreachableError -- Untyped.uglyTmConList -d_uglyTmConList_84 :: +d_uglyTmConList_204 :: MAlonzo.Code.Builtin.Signature.T__'8866''9839'_4 -> MAlonzo.Code.Utils.T_List_454 AgdaAny -> MAlonzo.Code.Agda.Builtin.String.T_String_6 -d_uglyTmConList_84 v0 v1 +d_uglyTmConList_204 v0 v1 = case coe v1 of MAlonzo.Code.Utils.C_'91''93'_458 -> coe ("" :: Data.Text.Text) MAlonzo.Code.Utils.C__'8759'__460 v2 v3 -> case coe v3 of MAlonzo.Code.Utils.C_'91''93'_458 -> coe - d_uglyTmCon_80 + d_uglyTmCon_200 (coe MAlonzo.Code.RawU.C_tmCon_208 (coe v0) (coe v2)) MAlonzo.Code.Utils.C__'8759'__460 v4 v5 -> coe MAlonzo.Code.Data.String.Base.d__'43''43'__20 - (d_uglyTmCon_80 + (d_uglyTmCon_200 (coe MAlonzo.Code.RawU.C_tmCon_208 (coe v0) (coe v2))) (coe MAlonzo.Code.Data.String.Base.d__'43''43'__20 - (" , " :: Data.Text.Text) (d_uglyTmConList_84 (coe v0) (coe v3))) + (" , " :: Data.Text.Text) (d_uglyTmConList_204 (coe v0) (coe v3))) _ -> MAlonzo.RTE.mazUnreachableError _ -> MAlonzo.RTE.mazUnreachableError -- Untyped.showNat -d_showNat_132 :: +d_showNat_252 :: Integer -> MAlonzo.Code.Agda.Builtin.String.T_String_6 -d_showNat_132 = T.pack . show +d_showNat_252 = T.pack . show -- Untyped.uglyBuiltin -d_uglyBuiltin_134 :: +d_uglyBuiltin_254 :: MAlonzo.Code.Builtin.T_Builtin_2 -> MAlonzo.Code.Agda.Builtin.String.T_String_6 -d_uglyBuiltin_134 v0 +d_uglyBuiltin_254 v0 = let v1 = "other" :: Data.Text.Text in coe (case coe v0 of @@ -168,36 +168,36 @@ d_uglyBuiltin_134 v0 -> coe ("addInteger" :: Data.Text.Text) _ -> coe v1) -- Untyped.uglyList -d_uglyList_138 :: +d_uglyList_258 :: Integer -> [T__'8866'_14] -> MAlonzo.Code.Agda.Builtin.String.T_String_6 -d_uglyList_138 v0 v1 +d_uglyList_258 v0 v1 = coe MAlonzo.Code.Data.String.Base.d__'43''43'__20 ("[" :: Data.Text.Text) (coe MAlonzo.Code.Data.String.Base.d__'43''43'__20 - (d_uglyList''_142 (coe v0) (coe v1)) ("]" :: Data.Text.Text)) + (d_uglyList''_262 (coe v0) (coe v1)) ("]" :: Data.Text.Text)) -- Untyped.uglyList' -d_uglyList''_142 :: +d_uglyList''_262 :: Integer -> [T__'8866'_14] -> MAlonzo.Code.Agda.Builtin.String.T_String_6 -d_uglyList''_142 v0 v1 +d_uglyList''_262 v0 v1 = case coe v1 of [] -> coe ("" :: Data.Text.Text) (:) v2 v3 -> coe MAlonzo.Code.Data.String.Base.d__'43''43'__20 - (d_ugly_146 (coe v0) (coe v2)) + (d_ugly_266 (coe v0) (coe v2)) (coe MAlonzo.Code.Data.String.Base.d__'43''43'__20 - (" , " :: Data.Text.Text) (d_uglyList''_142 (coe v0) (coe v3))) + (" , " :: Data.Text.Text) (d_uglyList''_262 (coe v0) (coe v3))) _ -> MAlonzo.RTE.mazUnreachableError -- Untyped.ugly -d_ugly_146 :: +d_ugly_266 :: Integer -> T__'8866'_14 -> MAlonzo.Code.Agda.Builtin.String.T_String_6 -d_ugly_146 v0 v1 +d_ugly_266 v0 v1 = case coe v1 of C_'96'_18 v2 -> coe ("(` var )" :: Data.Text.Text) C_ƛ_20 v2 @@ -206,7 +206,7 @@ d_ugly_146 v0 v1 ("(\411 " :: Data.Text.Text) (coe MAlonzo.Code.Data.String.Base.d__'43''43'__20 - (d_ugly_146 (coe addInt (coe (1 :: Integer)) (coe v0)) (coe v2)) + (d_ugly_266 (coe addInt (coe (1 :: Integer)) (coe v0)) (coe v2)) (")" :: Data.Text.Text)) C__'183'__22 v2 v3 -> coe @@ -214,34 +214,34 @@ d_ugly_146 v0 v1 ("( " :: Data.Text.Text) (coe MAlonzo.Code.Data.String.Base.d__'43''43'__20 - (d_ugly_146 (coe v0) (coe v2)) + (d_ugly_266 (coe v0) (coe v2)) (coe MAlonzo.Code.Data.String.Base.d__'43''43'__20 (" \183 " :: Data.Text.Text) (coe MAlonzo.Code.Data.String.Base.d__'43''43'__20 - (d_ugly_146 (coe v0) (coe v3)) (")" :: Data.Text.Text)))) + (d_ugly_266 (coe v0) (coe v3)) (")" :: Data.Text.Text)))) C_force_24 v2 -> coe MAlonzo.Code.Data.String.Base.d__'43''43'__20 ("(force " :: Data.Text.Text) (coe MAlonzo.Code.Data.String.Base.d__'43''43'__20 - (d_ugly_146 (coe v0) (coe v2)) (")" :: Data.Text.Text)) + (d_ugly_266 (coe v0) (coe v2)) (")" :: Data.Text.Text)) C_delay_26 v2 -> coe MAlonzo.Code.Data.String.Base.d__'43''43'__20 ("(delay " :: Data.Text.Text) (coe MAlonzo.Code.Data.String.Base.d__'43''43'__20 - (d_ugly_146 (coe v0) (coe v2)) (")" :: Data.Text.Text)) + (d_ugly_266 (coe v0) (coe v2)) (")" :: Data.Text.Text)) C_con_28 v2 -> coe MAlonzo.Code.Data.String.Base.d__'43''43'__20 ("(con " :: Data.Text.Text) (coe MAlonzo.Code.Data.String.Base.d__'43''43'__20 - (d_uglyTmCon_80 (coe v2)) (")" :: Data.Text.Text)) + (d_uglyTmCon_200 (coe v2)) (")" :: Data.Text.Text)) C_constr_34 v2 v3 -> coe MAlonzo.Code.Data.String.Base.d__'43''43'__20 @@ -251,58 +251,58 @@ d_ugly_146 v0 v1 (coe MAlonzo.Code.Data.Nat.Show.d_show_56 v2) (coe MAlonzo.Code.Data.String.Base.d__'43''43'__20 - (d_uglyList_138 (coe v0) (coe v3)) (")" :: Data.Text.Text))) + (d_uglyList_258 (coe v0) (coe v3)) (")" :: Data.Text.Text))) C_case_40 v2 v3 -> coe MAlonzo.Code.Data.String.Base.d__'43''43'__20 ("(case " :: Data.Text.Text) (coe MAlonzo.Code.Data.String.Base.d__'43''43'__20 - (d_ugly_146 (coe v0) (coe v2)) + (d_ugly_266 (coe v0) (coe v2)) (coe MAlonzo.Code.Data.String.Base.d__'43''43'__20 (" " :: Data.Text.Text) (coe MAlonzo.Code.Data.String.Base.d__'43''43'__20 - (d_uglyList_138 (coe v0) (coe v3)) (")" :: Data.Text.Text)))) + (d_uglyList_258 (coe v0) (coe v3)) (")" :: Data.Text.Text)))) C_builtin_44 v2 -> coe MAlonzo.Code.Data.String.Base.d__'43''43'__20 ("(builtin " :: Data.Text.Text) (coe MAlonzo.Code.Data.String.Base.d__'43''43'__20 - (d_uglyBuiltin_134 (coe v2)) (")" :: Data.Text.Text)) + (d_uglyBuiltin_254 (coe v2)) (")" :: Data.Text.Text)) C_error_46 -> coe ("error" :: Data.Text.Text) _ -> MAlonzo.RTE.mazUnreachableError -- Untyped.extG -d_extG_180 :: +d_extG_300 :: () -> (AgdaAny -> Integer) -> Maybe AgdaAny -> Integer -d_extG_180 ~v0 v1 v2 = du_extG_180 v1 v2 -du_extG_180 :: (AgdaAny -> Integer) -> Maybe AgdaAny -> Integer -du_extG_180 v0 v1 +d_extG_300 ~v0 v1 v2 = du_extG_300 v1 v2 +du_extG_300 :: (AgdaAny -> Integer) -> Maybe AgdaAny -> Integer +du_extG_300 v0 v1 = case coe v1 of MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 v2 -> coe addInt (coe (1 :: Integer)) (coe v0 v2) MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18 -> coe (0 :: Integer) _ -> MAlonzo.RTE.mazUnreachableError -- Untyped.extricateUList -d_extricateUList_190 :: +d_extricateUList_310 :: Integer -> [T__'8866'_14] -> MAlonzo.Code.Utils.T_List_454 MAlonzo.Code.RawU.T_Untyped_210 -d_extricateUList_190 v0 v1 +d_extricateUList_310 v0 v1 = case coe v1 of [] -> coe MAlonzo.Code.Utils.C_'91''93'_458 (:) v2 v3 -> coe MAlonzo.Code.Utils.C__'8759'__460 - (coe d_extricateU_194 (coe v0) (coe v2)) - (coe d_extricateUList_190 (coe v0) (coe v3)) + (coe d_extricateU_314 (coe v0) (coe v2)) + (coe d_extricateUList_310 (coe v0) (coe v3)) _ -> MAlonzo.RTE.mazUnreachableError -- Untyped.extricateU -d_extricateU_194 :: +d_extricateU_314 :: Integer -> T__'8866'_14 -> MAlonzo.Code.RawU.T_Untyped_210 -d_extricateU_194 v0 v1 +d_extricateU_314 v0 v1 = case coe v1 of C_'96'_18 v2 -> coe @@ -312,21 +312,21 @@ d_extricateU_194 v0 v1 -> coe MAlonzo.Code.RawU.C_ULambda_214 (coe - d_extricateU_194 (coe addInt (coe (1 :: Integer)) (coe v0)) + d_extricateU_314 (coe addInt (coe (1 :: Integer)) (coe v0)) (coe v2)) C__'183'__22 v2 v3 -> coe MAlonzo.Code.RawU.C_UApp_216 - (coe d_extricateU_194 (coe v0) (coe v2)) - (coe d_extricateU_194 (coe v0) (coe v3)) + (coe d_extricateU_314 (coe v0) (coe v2)) + (coe d_extricateU_314 (coe v0) (coe v3)) C_force_24 v2 -> coe MAlonzo.Code.RawU.C_UForce_226 - (coe d_extricateU_194 (coe v0) (coe v2)) + (coe d_extricateU_314 (coe v0) (coe v2)) C_delay_26 v2 -> coe MAlonzo.Code.RawU.C_UDelay_224 - (coe d_extricateU_194 (coe v0) (coe v2)) + (coe d_extricateU_314 (coe v0) (coe v2)) C_con_28 v2 -> coe MAlonzo.Code.RawU.C_UCon_218 @@ -342,24 +342,24 @@ d_extricateU_194 v0 v1 MAlonzo.Code.RawU.C_UConstr_228 (coe v2) (coe MAlonzo.Code.Utils.C__'8759'__460 - (coe d_extricateU_194 (coe v0) (coe v4)) - (coe d_extricateUList_190 (coe v0) (coe v5))) + (coe d_extricateU_314 (coe v0) (coe v4)) + (coe d_extricateUList_310 (coe v0) (coe v5))) _ -> MAlonzo.RTE.mazUnreachableError C_case_40 v2 v3 -> coe MAlonzo.Code.RawU.C_UCase_230 - (coe d_extricateU_194 (coe v0) (coe v2)) - (coe d_extricateUList_190 (coe v0) (coe v3)) + (coe d_extricateU_314 (coe v0) (coe v2)) + (coe d_extricateUList_310 (coe v0) (coe v3)) C_builtin_44 v2 -> coe MAlonzo.Code.RawU.C_UBuiltin_222 (coe v2) C_error_46 -> coe MAlonzo.Code.RawU.C_UError_220 _ -> MAlonzo.RTE.mazUnreachableError -- Untyped.extricateU0 -d_extricateU0_228 :: +d_extricateU0_348 :: T__'8866'_14 -> MAlonzo.Code.RawU.T_Untyped_210 -d_extricateU0_228 v0 - = coe d_extricateU_194 (coe (0 :: Integer)) (coe v0) +d_extricateU0_348 v0 + = coe d_extricateU_314 (coe (0 :: Integer)) (coe v0) -- Untyped.extG' -d_extG''_234 :: +d_extG''_354 :: () -> (Integer -> MAlonzo.Code.Utils.T_Either_6 @@ -367,15 +367,15 @@ d_extG''_234 :: Integer -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.Scoped.T_ScopeError_576 (Maybe AgdaAny) -d_extG''_234 ~v0 v1 v2 = du_extG''_234 v1 v2 -du_extG''_234 :: +d_extG''_354 ~v0 v1 v2 = du_extG''_354 v1 v2 +du_extG''_354 :: (Integer -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.Scoped.T_ScopeError_576 AgdaAny) -> Integer -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.Scoped.T_ScopeError_576 (Maybe AgdaAny) -du_extG''_234 v0 v1 +du_extG''_354 v0 v1 = case coe v1 of 0 -> coe MAlonzo.Code.Utils.C_inj'8322'_14 @@ -387,12 +387,12 @@ du_extG''_234 v0 v1 (coe MAlonzo.Code.Utils.du_EitherP_344) (coe MAlonzo.Code.Agda.Builtin.Maybe.C_just_16) (coe v0 v2)) -- Untyped.scopeCheckUList -d_scopeCheckUList_244 :: +d_scopeCheckUList_364 :: Integer -> MAlonzo.Code.Utils.T_List_454 MAlonzo.Code.RawU.T_Untyped_210 -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.Scoped.T_ScopeError_576 [T__'8866'_14] -d_scopeCheckUList_244 v0 v1 +d_scopeCheckUList_364 v0 v1 = case coe v1 of MAlonzo.Code.Utils.C_'91''93'_458 -> coe @@ -401,12 +401,12 @@ d_scopeCheckUList_244 v0 v1 MAlonzo.Code.Utils.C__'8759'__460 v2 v3 -> coe MAlonzo.Code.Utils.du_eitherBind_54 - (coe d_scopeCheckU_248 (coe v0) (coe v2)) + (coe d_scopeCheckU_368 (coe v0) (coe v2)) (coe (\ v4 -> coe MAlonzo.Code.Utils.du_eitherBind_54 - (coe d_scopeCheckUList_244 (coe v0) (coe v3)) + (coe d_scopeCheckUList_364 (coe v0) (coe v3)) (coe (\ v5 -> coe @@ -415,12 +415,12 @@ d_scopeCheckUList_244 v0 v1 MAlonzo.Code.Agda.Builtin.List.C__'8759'__22 (coe v4) (coe v5)))))) _ -> MAlonzo.RTE.mazUnreachableError -- Untyped.scopeCheckU -d_scopeCheckU_248 :: +d_scopeCheckU_368 :: Integer -> MAlonzo.Code.RawU.T_Untyped_210 -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.Scoped.T_ScopeError_576 T__'8866'_14 -d_scopeCheckU_248 v0 v1 +d_scopeCheckU_368 v0 v1 = case coe v1 of MAlonzo.Code.RawU.C_UVar_212 v2 -> coe @@ -435,17 +435,17 @@ d_scopeCheckU_248 v0 v1 MAlonzo.Code.Utils.du_fmap_292 (coe MAlonzo.Code.Utils.du_EitherP_344) (coe C_ƛ_20) (coe - d_scopeCheckU_248 (coe addInt (coe (1 :: Integer)) (coe v0)) + d_scopeCheckU_368 (coe addInt (coe (1 :: Integer)) (coe v0)) (coe v2)) MAlonzo.Code.RawU.C_UApp_216 v2 v3 -> coe MAlonzo.Code.Utils.du_eitherBind_54 - (coe d_scopeCheckU_248 (coe v0) (coe v2)) + (coe d_scopeCheckU_368 (coe v0) (coe v2)) (coe (\ v4 -> coe MAlonzo.Code.Utils.du_eitherBind_54 - (coe d_scopeCheckU_248 (coe v0) (coe v3)) + (coe d_scopeCheckU_368 (coe v0) (coe v3)) (coe (\ v5 -> coe @@ -464,26 +464,26 @@ d_scopeCheckU_248 v0 v1 -> coe MAlonzo.Code.Utils.du_fmap_292 (coe MAlonzo.Code.Utils.du_EitherP_344) (coe C_delay_26) - (coe d_scopeCheckU_248 (coe v0) (coe v2)) + (coe d_scopeCheckU_368 (coe v0) (coe v2)) MAlonzo.Code.RawU.C_UForce_226 v2 -> coe MAlonzo.Code.Utils.du_fmap_292 (coe MAlonzo.Code.Utils.du_EitherP_344) (coe C_force_24) - (coe d_scopeCheckU_248 (coe v0) (coe v2)) + (coe d_scopeCheckU_368 (coe v0) (coe v2)) MAlonzo.Code.RawU.C_UConstr_228 v2 v3 -> coe MAlonzo.Code.Utils.du_fmap_292 (coe MAlonzo.Code.Utils.du_EitherP_344) (coe C_constr_34 (coe v2)) - (coe d_scopeCheckUList_244 (coe v0) (coe v3)) + (coe d_scopeCheckUList_364 (coe v0) (coe v3)) MAlonzo.Code.RawU.C_UCase_230 v2 v3 -> coe MAlonzo.Code.Utils.du_eitherBind_54 - (coe d_scopeCheckU_248 (coe v0) (coe v2)) + (coe d_scopeCheckU_368 (coe v0) (coe v2)) (coe (\ v4 -> coe MAlonzo.Code.Utils.du_eitherBind_54 - (coe d_scopeCheckUList_244 (coe v0) (coe v3)) + (coe d_scopeCheckUList_364 (coe v0) (coe v3)) (coe (\ v5 -> coe @@ -491,17 +491,17 @@ d_scopeCheckU_248 v0 v1 (coe C_case_40 (coe v4) (coe v5)))))) _ -> MAlonzo.RTE.mazUnreachableError -- Untyped.scopeCheckU0 -d_scopeCheckU0_290 :: +d_scopeCheckU0_410 :: MAlonzo.Code.RawU.T_Untyped_210 -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.Scoped.T_ScopeError_576 T__'8866'_14 -d_scopeCheckU0_290 v0 - = coe d_scopeCheckU_248 (coe (0 :: Integer)) (coe v0) +d_scopeCheckU0_410 v0 + = coe d_scopeCheckU_368 (coe (0 :: Integer)) (coe v0) -- Untyped.decUTm -d_decUTm_298 :: +d_decUTm_418 :: MAlonzo.Code.RawU.T_Untyped_210 -> MAlonzo.Code.RawU.T_Untyped_210 -> Bool -d_decUTm_298 v0 v1 +d_decUTm_418 v0 v1 = let v2 = coe MAlonzo.Code.Agda.Builtin.Bool.C_false_8 in coe (case coe v0 of @@ -516,15 +516,15 @@ d_decUTm_298 v0 v1 MAlonzo.Code.RawU.C_ULambda_214 v3 -> case coe v1 of MAlonzo.Code.RawU.C_ULambda_214 v4 - -> coe d_decUTm_298 (coe v3) (coe v4) + -> coe d_decUTm_418 (coe v3) (coe v4) _ -> coe v2 MAlonzo.Code.RawU.C_UApp_216 v3 v4 -> case coe v1 of MAlonzo.Code.RawU.C_UApp_216 v5 v6 -> coe MAlonzo.Code.Data.Bool.Base.d__'8743'__24 - (coe d_decUTm_298 (coe v3) (coe v5)) - (coe d_decUTm_298 (coe v4) (coe v6)) + (coe d_decUTm_418 (coe v3) (coe v5)) + (coe d_decUTm_418 (coe v4) (coe v6)) _ -> coe v2 MAlonzo.Code.RawU.C_UCon_218 v3 -> case coe v1 of @@ -546,29 +546,29 @@ d_decUTm_298 v0 v1 MAlonzo.Code.RawU.C_UDelay_224 v3 -> case coe v1 of MAlonzo.Code.RawU.C_UDelay_224 v4 - -> coe d_decUTm_298 (coe v3) (coe v4) + -> coe d_decUTm_418 (coe v3) (coe v4) _ -> coe v2 MAlonzo.Code.RawU.C_UForce_226 v3 -> case coe v1 of MAlonzo.Code.RawU.C_UForce_226 v4 - -> coe d_decUTm_298 (coe v3) (coe v4) + -> coe d_decUTm_418 (coe v3) (coe v4) _ -> coe v2 _ -> coe v2) -- Untyped.buildDebruijnEncoding -d_buildDebruijnEncoding_334 :: +d_buildDebruijnEncoding_454 :: () -> Integer -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.Scoped.T_ScopeError_576 (Maybe AgdaAny) -d_buildDebruijnEncoding_334 ~v0 v1 - = du_buildDebruijnEncoding_334 v1 -du_buildDebruijnEncoding_334 :: +d_buildDebruijnEncoding_454 ~v0 v1 + = du_buildDebruijnEncoding_454 v1 +du_buildDebruijnEncoding_454 :: Integer -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.Scoped.T_ScopeError_576 (Maybe AgdaAny) -du_buildDebruijnEncoding_334 v0 +du_buildDebruijnEncoding_454 v0 = coe - du_extG''_234 + du_extG''_354 (coe (\ v1 -> coe @@ -576,18 +576,18 @@ du_buildDebruijnEncoding_334 v0 (coe MAlonzo.Code.Scoped.C_deBError_578))) (coe v0) -- Untyped.make-integer -d_make'45'integer_340 :: +d_make'45'integer_460 :: MAlonzo.Code.Builtin.Signature.T__'8866''9839'_4 -d_make'45'integer_340 +d_make'45'integer_460 = coe MAlonzo.Code.RawU.du_tag2TyTag_234 (coe MAlonzo.Code.RawU.C_integer_30) -- Untyped.con-integer -d_con'45'integer_344 :: Integer -> Integer -> T__'8866'_14 -d_con'45'integer_344 ~v0 v1 = du_con'45'integer_344 v1 -du_con'45'integer_344 :: Integer -> T__'8866'_14 -du_con'45'integer_344 v0 +d_con'45'integer_464 :: Integer -> Integer -> T__'8866'_14 +d_con'45'integer_464 ~v0 v1 = du_con'45'integer_464 v1 +du_con'45'integer_464 :: Integer -> T__'8866'_14 +du_con'45'integer_464 v0 = coe C_con_28 (coe - MAlonzo.Code.RawU.C_tmCon_208 (coe d_make'45'integer_340) (coe v0)) + MAlonzo.Code.RawU.C_tmCon_208 (coe d_make'45'integer_460) (coe v0)) diff --git a/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation.hs b/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation.hs index 520d7a1380c..3bdcd3fba00 100644 --- a/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation.hs +++ b/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation.hs @@ -17,6 +17,7 @@ import MAlonzo.RTE (coe, erased, AgdaAny, addInt, subInt, mulInt, rem64, lt64, eq64, word64FromNat, word64ToNat) import qualified MAlonzo.RTE import qualified Data.Text +import qualified MAlonzo.Code.Agda.Builtin.List import qualified MAlonzo.Code.Agda.Builtin.Maybe import qualified MAlonzo.Code.Agda.Builtin.Unit import qualified MAlonzo.Code.Data.Maybe.Base @@ -41,13 +42,13 @@ data T_Error_2 = C_emptyDump_4 | C_illScoped_6 | C_counterExample_8 (MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_12) | + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10) | C_abort_10 (MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_12) + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10) -- VerifiedCompilation.tagToRelation d_tagToRelation_12 :: - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_12 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> MAlonzo.Code.Untyped.T__'8866'_14 -> MAlonzo.Code.Untyped.T__'8866'_14 -> () d_tagToRelation_12 = erased @@ -55,7 +56,7 @@ d_tagToRelation_12 = erased d_RelationOf_14 :: MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_12 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> MAlonzo.Code.Untyped.T__'8866'_14 -> MAlonzo.Code.Untyped.T__'8866'_14 -> () d_RelationOf_14 = erased @@ -63,14 +64,14 @@ d_RelationOf_14 = erased d_hasRelation_18 :: MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_12 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> Bool d_hasRelation_18 = coe MAlonzo.Code.Utils.du_is'45'inj'8322'_46 -- VerifiedCompilation.certifyPass d_certifyPass_26 :: MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_12 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> MAlonzo.Code.VerifiedCompilation.Trace.T_Hints_80 -> MAlonzo.Code.Untyped.T__'8866'_14 -> MAlonzo.Code.Untyped.T__'8866'_14 -> @@ -84,25 +85,25 @@ d_certifyPass_26 v0 v1 MAlonzo.Code.VerifiedCompilation.NotImplemented.du_certNotImplemented_22) MAlonzo.Code.Utils.C_inj'8322'_14 v2 -> case coe v2 of - MAlonzo.Code.VerifiedCompilation.Trace.C_floatDelayT_14 + MAlonzo.Code.VerifiedCompilation.Trace.C_floatDelayT_12 -> coe MAlonzo.Code.VerifiedCompilation.Certificate.du_decider_204 (coe MAlonzo.Code.VerifiedCompilation.UFloatDelay.d_isFloatDelay'63'_102 (coe (0 :: Integer))) - MAlonzo.Code.VerifiedCompilation.Trace.C_forceDelayT_16 + MAlonzo.Code.VerifiedCompilation.Trace.C_forceDelayT_14 -> coe MAlonzo.Code.VerifiedCompilation.Certificate.du_decider_204 (coe MAlonzo.Code.VerifiedCompilation.UForceDelay.d_isForceDelay'63'_178 (coe (0 :: Integer))) - MAlonzo.Code.VerifiedCompilation.Trace.C_forceCaseDelayT_18 + MAlonzo.Code.VerifiedCompilation.Trace.C_forceCaseDelayT_16 -> coe MAlonzo.Code.VerifiedCompilation.Certificate.du_decider_204 (coe MAlonzo.Code.VerifiedCompilation.UForceCaseDelay.d_isForceCaseDelay'63'_94 (coe (0 :: Integer))) - MAlonzo.Code.VerifiedCompilation.Trace.C_inlineT_20 + MAlonzo.Code.VerifiedCompilation.Trace.C_inlineT_18 -> case coe v1 of MAlonzo.Code.VerifiedCompilation.Trace.C_inline_82 v3 -> coe @@ -115,30 +116,38 @@ d_certifyPass_26 v0 v1 MAlonzo.Code.VerifiedCompilation.Certificate.C_abort_32 (coe MAlonzo.Code.VerifiedCompilation.Trace.d_InlineT_38) _ -> MAlonzo.RTE.mazUnreachableError - MAlonzo.Code.VerifiedCompilation.Trace.C_cseT_22 + MAlonzo.Code.VerifiedCompilation.Trace.C_cseT_20 -> coe MAlonzo.Code.VerifiedCompilation.Certificate.du_decider_204 (coe MAlonzo.Code.VerifiedCompilation.UCSE.d_isUntypedCSE'63'_22 (coe (0 :: Integer))) - MAlonzo.Code.VerifiedCompilation.Trace.C_applyToCaseT_24 + MAlonzo.Code.VerifiedCompilation.Trace.C_applyToCaseT_22 -> coe MAlonzo.Code.VerifiedCompilation.Certificate.du_decider_204 (coe MAlonzo.Code.VerifiedCompilation.UApplyToCase.d_a2c'63''7580''7580'_24 (coe (0 :: Integer))) - MAlonzo.Code.VerifiedCompilation.Trace.C_caseReduceT_26 + MAlonzo.Code.VerifiedCompilation.Trace.C_caseReduceT_24 -> coe MAlonzo.Code.VerifiedCompilation.Certificate.du_decider_204 (coe MAlonzo.Code.VerifiedCompilation.UCaseReduce.d_decide_526 (coe (0 :: Integer))) - MAlonzo.Code.VerifiedCompilation.Trace.C_letFloatOutT_28 + MAlonzo.Code.VerifiedCompilation.Trace.C_letFloatOutT_26 -> coe MAlonzo.Code.VerifiedCompilation.Certificate.du_decider_204 (coe MAlonzo.Code.VerifiedCompilation.FloatOut.d_decide_312 (coe (0 :: Integer))) + MAlonzo.Code.VerifiedCompilation.Trace.C_polyBuiltinT_28 + -> coe + MAlonzo.Code.VerifiedCompilation.Certificate.du_decider''_242 + (coe v0) + (coe + MAlonzo.Code.VerifiedCompilation.UCSE.d_dec'45'hoist_178 + (coe (0 :: Integer)) + (coe MAlonzo.Code.Agda.Builtin.List.C_'91''93'_16)) _ -> MAlonzo.RTE.mazUnreachableError _ -> MAlonzo.RTE.mazUnreachableError -- VerifiedCompilation.Certificate @@ -147,7 +156,7 @@ d_Certificate_34 :: (MAlonzo.Code.Utils.T__'215'__436 (MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_12) + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10) MAlonzo.Code.VerifiedCompilation.Trace.T_Hints_80) MAlonzo.Code.Untyped.T__'8866'_14 -> () @@ -158,7 +167,7 @@ d_certify_46 :: (MAlonzo.Code.Utils.T__'215'__436 (MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_12) + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10) MAlonzo.Code.VerifiedCompilation.Trace.T_Hints_80) MAlonzo.Code.Untyped.T__'8866'_14 -> MAlonzo.Code.Utils.T_Either_6 T_Error_2 AgdaAny @@ -200,7 +209,7 @@ d_cert_96 :: (MAlonzo.Code.Utils.T__'215'__436 (MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_12) + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10) MAlonzo.Code.VerifiedCompilation.Trace.T_Hints_80) MAlonzo.Code.Untyped.T__'8866'_14 -> MAlonzo.Code.Utils.T_Either_6 T_Error_2 AgdaAny -> @@ -220,14 +229,14 @@ d_checkScope_100 :: d_checkScope_100 v0 = coe MAlonzo.Code.Utils.du_eitherToMaybe_112 - (coe MAlonzo.Code.Untyped.d_scopeCheckU0_290 (coe v0)) + (coe MAlonzo.Code.Untyped.d_scopeCheckU0_410 (coe v0)) -- VerifiedCompilation.checkScopeᵗ d_checkScope'7511'_102 :: MAlonzo.Code.VerifiedCompilation.Trace.T_NonEmptySep_90 (MAlonzo.Code.Utils.T__'215'__436 (MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_12) + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10) MAlonzo.Code.VerifiedCompilation.Trace.T_Hints_80) MAlonzo.Code.RawU.T_Untyped_210 -> Maybe @@ -235,7 +244,7 @@ d_checkScope'7511'_102 :: (MAlonzo.Code.Utils.T__'215'__436 (MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_12) + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10) MAlonzo.Code.VerifiedCompilation.Trace.T_Hints_80) MAlonzo.Code.Untyped.T__'8866'_14) d_checkScope'7511'_102 v0 diff --git a/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/Certificate.hs b/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/Certificate.hs index 15abb9f1a03..a727672ccf0 100644 --- a/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/Certificate.hs +++ b/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/Certificate.hs @@ -33,11 +33,11 @@ data T_CertResult_12 = C_proof_18 AgdaAny | C_ce_26 (MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_12) + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10) AgdaAny AgdaAny | C_abort_32 (MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_12) + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10) AgdaAny AgdaAny -- VerifiedCompilation.Certificate.is-proof d_is'45'proof_36 :: @@ -68,7 +68,7 @@ data T_ProofOrCE_50 = C_proof_56 AgdaAny | C_ce_64 (MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_12) + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10) AgdaAny AgdaAny -- VerifiedCompilation.Certificate.isProof? d_isProof'63'_68 :: @@ -97,7 +97,7 @@ data T_Proof'63'_78 = C_proof_84 AgdaAny | C_abort_90 (MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_12) + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10) AgdaAny AgdaAny -- VerifiedCompilation.Certificate._>>=_ d__'62''62''61'__100 :: @@ -162,23 +162,55 @@ du_decider_204 v0 v1 v2 C_proof_56 v4 -> coe C_proof_18 (coe v4) C_ce_64 v7 v8 v9 -> coe C_ce_26 v7 v8 v9 _ -> MAlonzo.RTE.mazUnreachableError) +-- VerifiedCompilation.Certificate.decider' +d_decider''_242 :: + () -> + (AgdaAny -> AgdaAny -> ()) -> + MAlonzo.Code.Utils.T_Either_6 + MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> + (AgdaAny -> + AgdaAny -> + MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) -> + AgdaAny -> AgdaAny -> T_CertResult_12 +d_decider''_242 ~v0 ~v1 v2 v3 v4 v5 = du_decider''_242 v2 v3 v4 v5 +du_decider''_242 :: + MAlonzo.Code.Utils.T_Either_6 + MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> + (AgdaAny -> + AgdaAny -> + MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) -> + AgdaAny -> AgdaAny -> T_CertResult_12 +du_decider''_242 v0 v1 v2 v3 + = let v4 = coe v1 v2 v3 in + coe + (case coe v4 of + MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 v5 v6 + -> if coe v5 + then case coe v6 of + MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 v7 + -> coe C_proof_18 (coe v7) + _ -> MAlonzo.RTE.mazUnreachableError + else coe seq (coe v6) (coe C_ce_26 v0 v2 v3) + _ -> MAlonzo.RTE.mazUnreachableError) -- VerifiedCompilation.Certificate.decToPCE -d_decToPCE_246 :: +d_decToPCE_284 :: () -> () -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_12 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 -> AgdaAny -> AgdaAny -> T_ProofOrCE_50 -d_decToPCE_246 ~v0 ~v1 v2 v3 v4 v5 = du_decToPCE_246 v2 v3 v4 v5 -du_decToPCE_246 :: +d_decToPCE_284 ~v0 ~v1 v2 v3 v4 v5 = du_decToPCE_284 v2 v3 v4 v5 +du_decToPCE_284 :: MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_12 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 -> AgdaAny -> AgdaAny -> T_ProofOrCE_50 -du_decToPCE_246 v0 v1 v2 v3 +du_decToPCE_284 v0 v1 v2 v3 = case coe v1 of MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 v4 v5 -> if coe v4 @@ -189,15 +221,15 @@ du_decToPCE_246 v0 v1 v2 v3 else coe seq (coe v5) (coe C_ce_64 v0 v2 v3) _ -> MAlonzo.RTE.mazUnreachableError -- VerifiedCompilation.Certificate.pceToDec -d_pceToDec_260 :: +d_pceToDec_298 :: () -> T_ProofOrCE_50 -> MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 -d_pceToDec_260 ~v0 v1 = du_pceToDec_260 v1 -du_pceToDec_260 :: +d_pceToDec_298 ~v0 v1 = du_pceToDec_298 v1 +du_pceToDec_298 :: T_ProofOrCE_50 -> MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 -du_pceToDec_260 v0 +du_pceToDec_298 v0 = case coe v0 of C_proof_56 v1 -> coe @@ -211,29 +243,29 @@ du_pceToDec_260 v0 (coe MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26) _ -> MAlonzo.RTE.mazUnreachableError -- VerifiedCompilation.Certificate.matchOrCE -d_matchOrCE_274 :: +d_matchOrCE_312 :: () -> () -> MAlonzo.Code.Agda.Primitive.T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_12 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> (AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) -> AgdaAny -> AgdaAny -> T_ProofOrCE_50 -d_matchOrCE_274 ~v0 ~v1 ~v2 ~v3 v4 v5 v6 v7 - = du_matchOrCE_274 v4 v5 v6 v7 -du_matchOrCE_274 :: +d_matchOrCE_312 ~v0 ~v1 ~v2 ~v3 v4 v5 v6 v7 + = du_matchOrCE_312 v4 v5 v6 v7 +du_matchOrCE_312 :: MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_12 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> (AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) -> AgdaAny -> AgdaAny -> T_ProofOrCE_50 -du_matchOrCE_274 v0 v1 v2 v3 +du_matchOrCE_312 v0 v1 v2 v3 = let v4 = coe v1 v2 v3 in coe (case coe v4 of @@ -246,25 +278,25 @@ du_matchOrCE_274 v0 v1 v2 v3 else coe seq (coe v6) (coe C_ce_64 v0 v2 v3) _ -> MAlonzo.RTE.mazUnreachableError) -- VerifiedCompilation.Certificate.pcePointwise -d_pcePointwise_316 :: +d_pcePointwise_354 :: () -> () -> MAlonzo.Code.Agda.Primitive.T_Level_18 -> (AgdaAny -> AgdaAny -> ()) -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_12 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> (AgdaAny -> AgdaAny -> T_ProofOrCE_50) -> [AgdaAny] -> [AgdaAny] -> T_ProofOrCE_50 -d_pcePointwise_316 ~v0 ~v1 ~v2 ~v3 v4 v5 v6 v7 - = du_pcePointwise_316 v4 v5 v6 v7 -du_pcePointwise_316 :: +d_pcePointwise_354 ~v0 ~v1 ~v2 ~v3 v4 v5 v6 v7 + = du_pcePointwise_354 v4 v5 v6 v7 +du_pcePointwise_354 :: MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_12 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> (AgdaAny -> AgdaAny -> T_ProofOrCE_50) -> [AgdaAny] -> [AgdaAny] -> T_ProofOrCE_50 -du_pcePointwise_316 v0 v1 v2 v3 +du_pcePointwise_354 v0 v1 v2 v3 = case coe v2 of [] -> case coe v3 of @@ -284,7 +316,7 @@ du_pcePointwise_316 v0 v1 v2 v3 (case coe v8 of C_proof_56 v9 -> let v10 - = coe du_pcePointwise_316 (coe v0) (coe v1) (coe v5) (coe v7) in + = coe du_pcePointwise_354 (coe v0) (coe v1) (coe v5) (coe v7) in coe (case coe v10 of C_proof_56 v11 diff --git a/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/FloatOut.hs b/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/FloatOut.hs index f29dcffd0ac..beec008a7c4 100644 --- a/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/FloatOut.hs +++ b/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/FloatOut.hs @@ -81,7 +81,7 @@ du_apply'45'dec_62 v0 v1 v2 v3 coe MAlonzo.Code.VerifiedCompilation.UntypedViews.du_'8943'_2404) (coe v2)) (coe - MAlonzo.Code.VerifiedCompilation.UntypedViews.du_let'''63'_2390 + MAlonzo.Code.VerifiedCompilation.UntypedViews.du_let'8321''63'_2390 (\ v4 -> coe MAlonzo.Code.VerifiedCompilation.UntypedViews.du_'8943'_2404) (coe @@ -243,7 +243,7 @@ du_case'45'dec_148 v0 v1 v2 v3 coe MAlonzo.Code.VerifiedCompilation.UntypedViews.du_'8943'_2404) (coe v2)) (coe - MAlonzo.Code.VerifiedCompilation.UntypedViews.du_let'''63'_2390 + MAlonzo.Code.VerifiedCompilation.UntypedViews.du_let'8321''63'_2390 (\ v4 -> coe MAlonzo.Code.VerifiedCompilation.UntypedViews.du_'8943'_2404) (coe @@ -411,7 +411,7 @@ du_force'45'dec_234 v0 v1 v2 v3 coe MAlonzo.Code.VerifiedCompilation.UntypedViews.du_'8943'_2404) (coe v2)) (coe - MAlonzo.Code.VerifiedCompilation.UntypedViews.du_let'''63'_2390 + MAlonzo.Code.VerifiedCompilation.UntypedViews.du_let'8321''63'_2390 (\ v4 -> coe MAlonzo.Code.VerifiedCompilation.UntypedViews.du_'8943'_2404) (coe diff --git a/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/Trace.hs b/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/Trace.hs index da8ebbcb61a..022c89c609e 100644 --- a/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/Trace.hs +++ b/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/Trace.hs @@ -30,48 +30,47 @@ d_UncertifiedOptTag_4 = () type T_UncertifiedOptTag_4 = UncertifiedOptStage pattern C_caseOfCaseT_6 = CaseOfCase pattern C_constantFoldingT_8 = ConstantFolding -pattern C_polyBuiltinT_10 = PolyBuiltin check_caseOfCaseT_6 :: T_UncertifiedOptTag_4 check_caseOfCaseT_6 = CaseOfCase check_constantFoldingT_8 :: T_UncertifiedOptTag_4 check_constantFoldingT_8 = ConstantFolding -check_polyBuiltinT_10 :: T_UncertifiedOptTag_4 -check_polyBuiltinT_10 = PolyBuiltin cover_UncertifiedOptTag_4 :: UncertifiedOptStage -> () cover_UncertifiedOptTag_4 x = case x of CaseOfCase -> () ConstantFolding -> () - PolyBuiltin -> () -- VerifiedCompilation.Trace.CertifiedOptTag -d_CertifiedOptTag_12 = () -type T_CertifiedOptTag_12 = CertifiedOptStage -pattern C_floatDelayT_14 = FloatDelay -pattern C_forceDelayT_16 = ForceDelay -pattern C_forceCaseDelayT_18 = ForceCaseDelay -pattern C_inlineT_20 = Inline -pattern C_cseT_22 = CSE -pattern C_applyToCaseT_24 = ApplyToCase -pattern C_caseReduceT_26 = CaseReduce -pattern C_letFloatOutT_28 = LetFloatOut -check_floatDelayT_14 :: T_CertifiedOptTag_12 -check_floatDelayT_14 = FloatDelay -check_forceDelayT_16 :: T_CertifiedOptTag_12 -check_forceDelayT_16 = ForceDelay -check_forceCaseDelayT_18 :: T_CertifiedOptTag_12 -check_forceCaseDelayT_18 = ForceCaseDelay -check_inlineT_20 :: T_CertifiedOptTag_12 -check_inlineT_20 = Inline -check_cseT_22 :: T_CertifiedOptTag_12 -check_cseT_22 = CSE -check_applyToCaseT_24 :: T_CertifiedOptTag_12 -check_applyToCaseT_24 = ApplyToCase -check_caseReduceT_26 :: T_CertifiedOptTag_12 -check_caseReduceT_26 = CaseReduce -check_letFloatOutT_28 :: T_CertifiedOptTag_12 -check_letFloatOutT_28 = LetFloatOut -cover_CertifiedOptTag_12 :: CertifiedOptStage -> () -cover_CertifiedOptTag_12 x +d_CertifiedOptTag_10 = () +type T_CertifiedOptTag_10 = CertifiedOptStage +pattern C_floatDelayT_12 = FloatDelay +pattern C_forceDelayT_14 = ForceDelay +pattern C_forceCaseDelayT_16 = ForceCaseDelay +pattern C_inlineT_18 = Inline +pattern C_cseT_20 = CSE +pattern C_applyToCaseT_22 = ApplyToCase +pattern C_caseReduceT_24 = CaseReduce +pattern C_letFloatOutT_26 = LetFloatOut +pattern C_polyBuiltinT_28 = PolyBuiltin +check_floatDelayT_12 :: T_CertifiedOptTag_10 +check_floatDelayT_12 = FloatDelay +check_forceDelayT_14 :: T_CertifiedOptTag_10 +check_forceDelayT_14 = ForceDelay +check_forceCaseDelayT_16 :: T_CertifiedOptTag_10 +check_forceCaseDelayT_16 = ForceCaseDelay +check_inlineT_18 :: T_CertifiedOptTag_10 +check_inlineT_18 = Inline +check_cseT_20 :: T_CertifiedOptTag_10 +check_cseT_20 = CSE +check_applyToCaseT_22 :: T_CertifiedOptTag_10 +check_applyToCaseT_22 = ApplyToCase +check_caseReduceT_24 :: T_CertifiedOptTag_10 +check_caseReduceT_24 = CaseReduce +check_letFloatOutT_26 :: T_CertifiedOptTag_10 +check_letFloatOutT_26 = LetFloatOut +check_polyBuiltinT_28 :: T_CertifiedOptTag_10 +check_polyBuiltinT_28 = PolyBuiltin +cover_CertifiedOptTag_10 :: CertifiedOptStage -> () +cover_CertifiedOptTag_10 x = case x of FloatDelay -> () ForceDelay -> () @@ -81,74 +80,75 @@ cover_CertifiedOptTag_12 x ApplyToCase -> () CaseReduce -> () LetFloatOut -> () + PolyBuiltin -> () -- VerifiedCompilation.Trace.OptTag d_OptTag_30 :: () d_OptTag_30 = erased -- VerifiedCompilation.Trace.FloatDelayT d_FloatDelayT_32 :: MAlonzo.Code.Utils.T_Either_6 - T_UncertifiedOptTag_4 T_CertifiedOptTag_12 + T_UncertifiedOptTag_4 T_CertifiedOptTag_10 d_FloatDelayT_32 - = coe MAlonzo.Code.Utils.C_inj'8322'_14 (coe C_floatDelayT_14) + = coe MAlonzo.Code.Utils.C_inj'8322'_14 (coe C_floatDelayT_12) -- VerifiedCompilation.Trace.ForceDelayT d_ForceDelayT_34 :: MAlonzo.Code.Utils.T_Either_6 - T_UncertifiedOptTag_4 T_CertifiedOptTag_12 + T_UncertifiedOptTag_4 T_CertifiedOptTag_10 d_ForceDelayT_34 - = coe MAlonzo.Code.Utils.C_inj'8322'_14 (coe C_forceDelayT_16) + = coe MAlonzo.Code.Utils.C_inj'8322'_14 (coe C_forceDelayT_14) -- VerifiedCompilation.Trace.ForceCaseDelayT d_ForceCaseDelayT_36 :: MAlonzo.Code.Utils.T_Either_6 - T_UncertifiedOptTag_4 T_CertifiedOptTag_12 + T_UncertifiedOptTag_4 T_CertifiedOptTag_10 d_ForceCaseDelayT_36 - = coe MAlonzo.Code.Utils.C_inj'8322'_14 (coe C_forceCaseDelayT_18) + = coe MAlonzo.Code.Utils.C_inj'8322'_14 (coe C_forceCaseDelayT_16) -- VerifiedCompilation.Trace.InlineT d_InlineT_38 :: MAlonzo.Code.Utils.T_Either_6 - T_UncertifiedOptTag_4 T_CertifiedOptTag_12 + T_UncertifiedOptTag_4 T_CertifiedOptTag_10 d_InlineT_38 - = coe MAlonzo.Code.Utils.C_inj'8322'_14 (coe C_inlineT_20) + = coe MAlonzo.Code.Utils.C_inj'8322'_14 (coe C_inlineT_18) -- VerifiedCompilation.Trace.CseT d_CseT_40 :: MAlonzo.Code.Utils.T_Either_6 - T_UncertifiedOptTag_4 T_CertifiedOptTag_12 -d_CseT_40 = coe MAlonzo.Code.Utils.C_inj'8322'_14 (coe C_cseT_22) + T_UncertifiedOptTag_4 T_CertifiedOptTag_10 +d_CseT_40 = coe MAlonzo.Code.Utils.C_inj'8322'_14 (coe C_cseT_20) -- VerifiedCompilation.Trace.ApplyToCaseT d_ApplyToCaseT_42 :: MAlonzo.Code.Utils.T_Either_6 - T_UncertifiedOptTag_4 T_CertifiedOptTag_12 + T_UncertifiedOptTag_4 T_CertifiedOptTag_10 d_ApplyToCaseT_42 - = coe MAlonzo.Code.Utils.C_inj'8322'_14 (coe C_applyToCaseT_24) + = coe MAlonzo.Code.Utils.C_inj'8322'_14 (coe C_applyToCaseT_22) -- VerifiedCompilation.Trace.LetFloatOutT d_LetFloatOutT_44 :: MAlonzo.Code.Utils.T_Either_6 - T_UncertifiedOptTag_4 T_CertifiedOptTag_12 + T_UncertifiedOptTag_4 T_CertifiedOptTag_10 d_LetFloatOutT_44 - = coe MAlonzo.Code.Utils.C_inj'8322'_14 (coe C_letFloatOutT_28) + = coe MAlonzo.Code.Utils.C_inj'8322'_14 (coe C_letFloatOutT_26) -- VerifiedCompilation.Trace.CaseReduceT d_CaseReduceT_46 :: MAlonzo.Code.Utils.T_Either_6 - T_UncertifiedOptTag_4 T_CertifiedOptTag_12 + T_UncertifiedOptTag_4 T_CertifiedOptTag_10 d_CaseReduceT_46 - = coe MAlonzo.Code.Utils.C_inj'8322'_14 (coe C_caseReduceT_26) + = coe MAlonzo.Code.Utils.C_inj'8322'_14 (coe C_caseReduceT_24) -- VerifiedCompilation.Trace.CaseOfCaseT d_CaseOfCaseT_48 :: MAlonzo.Code.Utils.T_Either_6 - T_UncertifiedOptTag_4 T_CertifiedOptTag_12 + T_UncertifiedOptTag_4 T_CertifiedOptTag_10 d_CaseOfCaseT_48 = coe MAlonzo.Code.Utils.C_inj'8321'_12 (coe C_caseOfCaseT_6) -- VerifiedCompilation.Trace.ConstantFoldingT d_ConstantFoldingT_50 :: MAlonzo.Code.Utils.T_Either_6 - T_UncertifiedOptTag_4 T_CertifiedOptTag_12 + T_UncertifiedOptTag_4 T_CertifiedOptTag_10 d_ConstantFoldingT_50 = coe MAlonzo.Code.Utils.C_inj'8321'_12 (coe C_constantFoldingT_8) -- VerifiedCompilation.Trace.PolyBuiltinT d_PolyBuiltinT_52 :: MAlonzo.Code.Utils.T_Either_6 - T_UncertifiedOptTag_4 T_CertifiedOptTag_12 + T_UncertifiedOptTag_4 T_CertifiedOptTag_10 d_PolyBuiltinT_52 - = coe MAlonzo.Code.Utils.C_inj'8321'_12 (coe C_polyBuiltinT_10) + = coe MAlonzo.Code.Utils.C_inj'8322'_14 (coe C_polyBuiltinT_28) -- VerifiedCompilation.Trace.InlineHints d_InlineHints_54 = () type T_InlineHints_54 = Hints.Inline diff --git a/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/UApplyToCase.hs b/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/UApplyToCase.hs index 0500f8416b0..22a4d06c2ea 100644 --- a/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/UApplyToCase.hs +++ b/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/UApplyToCase.hs @@ -276,7 +276,7 @@ d_'46'extendedlambda1_94 :: () -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_12 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> AgdaAny -> AgdaAny -> T_ApplyToCase_4 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20 diff --git a/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/UCSE.hs b/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/UCSE.hs index 27d7d1b20d7..0786d0cdc3a 100644 --- a/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/UCSE.hs +++ b/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/UCSE.hs @@ -18,6 +18,7 @@ import MAlonzo.RTE (coe, erased, AgdaAny, addInt, subInt, mulInt, import qualified MAlonzo.RTE import qualified Data.Text import qualified MAlonzo.Code.Agda.Builtin.Bool +import qualified MAlonzo.Code.Agda.Builtin.Equality import qualified MAlonzo.Code.Agda.Builtin.List import qualified MAlonzo.Code.Agda.Builtin.Sigma import qualified MAlonzo.Code.Data.Fin.Base @@ -26,6 +27,8 @@ import qualified MAlonzo.Code.Data.Irrelevant import qualified MAlonzo.Code.Relation.Nullary.Decidable.Core import qualified MAlonzo.Code.Relation.Nullary.Reflects import qualified MAlonzo.Code.Untyped +import qualified MAlonzo.Code.Untyped.Equality +import qualified MAlonzo.Code.Untyped.Purity import qualified MAlonzo.Code.Untyped.RenamingSubstitution import qualified MAlonzo.Code.Untyped.Strictness import qualified MAlonzo.Code.Utils @@ -12127,81 +12130,679 @@ d_'46'extendedlambda2_106 :: () -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_12 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> AgdaAny -> AgdaAny -> MAlonzo.Code.Untyped.Strictness.T__'8712''8595'__10 -> T_UCSE_6 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20 d_'46'extendedlambda2_106 = erased --- VerifiedCompilation.UCSE.M₁ -d_M'8321'_124 :: MAlonzo.Code.Untyped.T__'8866'_14 -d_M'8321'_124 - = coe - MAlonzo.Code.Untyped.C__'183'__22 - (coe - MAlonzo.Code.Untyped.C_constr_34 (coe (0 :: Integer)) - (coe MAlonzo.Code.Agda.Builtin.List.C_'91''93'_16)) - (coe - MAlonzo.Code.Untyped.C_constr_34 (coe (0 :: Integer)) - (coe MAlonzo.Code.Agda.Builtin.List.C_'91''93'_16)) --- VerifiedCompilation.UCSE.N₁ -d_N'8321'_126 :: MAlonzo.Code.Untyped.T__'8866'_14 -d_N'8321'_126 - = coe - MAlonzo.Code.Untyped.C__'183'__22 - (coe - MAlonzo.Code.Untyped.C_ƛ_20 - (coe - MAlonzo.Code.Untyped.C__'183'__22 - (coe - MAlonzo.Code.Untyped.C_'96'_18 - (coe MAlonzo.Code.Data.Fin.Base.C_zero_12)) - (coe - MAlonzo.Code.Untyped.C_'96'_18 - (coe MAlonzo.Code.Data.Fin.Base.C_zero_12)))) - (coe - MAlonzo.Code.Untyped.C_constr_34 (coe (0 :: Integer)) - (coe MAlonzo.Code.Agda.Builtin.List.C_'91''93'_16)) --- VerifiedCompilation.UCSE.M₂ -d_M'8322'_130 :: MAlonzo.Code.Untyped.T__'8866'_14 -d_M'8322'_130 - = coe - MAlonzo.Code.Untyped.C__'183'__22 - (coe - MAlonzo.Code.Untyped.C_ƛ_20 - (coe - MAlonzo.Code.Untyped.C_'96'_18 - (coe MAlonzo.Code.Data.Fin.Base.C_zero_12))) - (coe - MAlonzo.Code.Untyped.C_constr_34 (coe (0 :: Integer)) - (coe MAlonzo.Code.Agda.Builtin.List.C_'91''93'_16)) --- VerifiedCompilation.UCSE.N₂ -d_N'8322'_132 :: MAlonzo.Code.Untyped.T__'8866'_14 -d_N'8322'_132 - = coe - MAlonzo.Code.Untyped.C__'183'__22 - (coe - MAlonzo.Code.Untyped.C_ƛ_20 - (coe - MAlonzo.Code.Untyped.C_'96'_18 - (coe MAlonzo.Code.Data.Fin.Base.C_zero_12))) - (coe - MAlonzo.Code.Untyped.C_constr_34 (coe (0 :: Integer)) - (coe MAlonzo.Code.Agda.Builtin.List.C_'91''93'_16)) --- VerifiedCompilation.UCSE.M₃ -d_M'8323'_136 :: MAlonzo.Code.Untyped.T__'8866'_14 -d_M'8323'_136 - = coe - MAlonzo.Code.Untyped.C_constr_34 (coe (0 :: Integer)) - (coe MAlonzo.Code.Agda.Builtin.List.C_'91''93'_16) --- VerifiedCompilation.UCSE.N₃ -d_N'8323'_138 :: MAlonzo.Code.Untyped.T__'8866'_14 -d_N'8323'_138 - = coe - MAlonzo.Code.Untyped.C__'183'__22 - (coe - MAlonzo.Code.Untyped.C_ƛ_20 - (coe - MAlonzo.Code.Untyped.C_constr_34 (coe (0 :: Integer)) - (coe MAlonzo.Code.Agda.Builtin.List.C_'91''93'_16))) - (coe MAlonzo.Code.Untyped.C_error_46) +-- VerifiedCompilation.UCSE.applyN +d_applyN_126 :: + Integer -> + MAlonzo.Code.Untyped.T__'8866'_14 -> + [MAlonzo.Code.Untyped.T__'8866'_14] -> + MAlonzo.Code.Untyped.T__'8866'_14 +d_applyN_126 ~v0 v1 v2 = du_applyN_126 v1 v2 +du_applyN_126 :: + MAlonzo.Code.Untyped.T__'8866'_14 -> + [MAlonzo.Code.Untyped.T__'8866'_14] -> + MAlonzo.Code.Untyped.T__'8866'_14 +du_applyN_126 v0 v1 + = case coe v1 of + [] -> coe v0 + (:) v2 v3 + -> coe + du_applyN_126 + (coe MAlonzo.Code.Untyped.C__'183'__22 (coe v0) (coe v2)) (coe v3) + _ -> MAlonzo.RTE.mazUnreachableError +-- VerifiedCompilation.UCSE.HoistPoly +d_HoistPoly_138 a0 a1 a2 a3 = () +data T_HoistPoly_138 + = C_let'45''183'_150 T_HoistPoly_138 | + C_let'45'ƛ_160 MAlonzo.Code.Untyped.Purity.T_Pure_6 + T_HoistPoly_138 | + C_refl_168 +-- VerifiedCompilation.UCSE.dec-hoist +d_dec'45'hoist_178 :: + Integer -> + [MAlonzo.Code.Untyped.T__'8866'_14] -> + MAlonzo.Code.Untyped.T__'8866'_14 -> + MAlonzo.Code.Untyped.T__'8866'_14 -> + MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 +d_dec'45'hoist_178 v0 v1 v2 v3 + = let v4 + = coe + MAlonzo.Code.Relation.Nullary.Decidable.Core.du__'215''45'dec__84 + (coe + MAlonzo.Code.VerifiedCompilation.UntypedViews.du_ƛ'63'_1158 + (\ v4 -> + coe MAlonzo.Code.VerifiedCompilation.UntypedViews.du_'8943'_2404) + (coe v3)) + (coe + MAlonzo.Code.VerifiedCompilation.UntypedViews.du__'8759''63'__2434 + (\ v4 -> + coe MAlonzo.Code.VerifiedCompilation.UntypedViews.du_'8943'_2404) + (\ v4 -> + coe MAlonzo.Code.VerifiedCompilation.UntypedViews.du_'8943'_2404) + (coe v1)) in + coe + (case coe v4 of + MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 v5 v6 + -> if coe v5 + then case coe v6 of + MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 v7 + -> case coe v7 of + MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 v8 v9 + -> case coe v8 of + MAlonzo.Code.VerifiedCompilation.UntypedViews.C_ƛ'33'_876 v11 + -> case coe v3 of + MAlonzo.Code.Untyped.C_ƛ_20 v12 + -> coe + seq (coe v11) + (case coe v9 of + MAlonzo.Code.VerifiedCompilation.UntypedViews.C__'8759''33'__2426 v15 v16 + -> case coe v1 of + (:) v17 v18 + -> coe + seq (coe v15) + (coe + seq (coe v16) + (let v19 + = coe + MAlonzo.Code.Relation.Nullary.Decidable.Core.du__'215''45'dec__84 + (coe + MAlonzo.Code.Untyped.Purity.d_isPure'63'_72 + (coe v0) + (coe v17)) + (coe + d_dec'45'hoist_178 + (coe v0) + (coe v18) + (coe v2) + (coe + MAlonzo.Code.Untyped.RenamingSubstitution.d__'91'_'93'_478 + (coe v0) + (coe v12) + (coe + v17))) in + coe + (case coe v19 of + MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 v20 v21 + -> if coe v20 + then case coe + v21 of + MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 v22 + -> case coe + v22 of + MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 v23 v24 + -> coe + MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 + (coe + v20) + (coe + MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 + (coe + C_let'45'ƛ_160 + v23 + v24)) + _ -> MAlonzo.RTE.mazUnreachableError + _ -> MAlonzo.RTE.mazUnreachableError + else coe + seq + (coe v21) + (let v22 + = MAlonzo.Code.Untyped.Equality.d_decEq'45''8866'_56 + (coe + v0) + (coe + v2) + (coe + du_applyN_126 + (coe + v3) + (coe + v1)) in + coe + (case coe + v22 of + MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 v23 v24 + -> if coe + v23 + then coe + seq + (coe + v24) + (coe + MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 + (coe + v23) + (coe + MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 + (coe + C_refl_168))) + else coe + seq + (coe + v24) + (coe + MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 + (coe + v23) + (coe + MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)) + _ -> MAlonzo.RTE.mazUnreachableError)) + _ -> MAlonzo.RTE.mazUnreachableError))) + _ -> MAlonzo.RTE.mazUnreachableError + _ -> MAlonzo.RTE.mazUnreachableError) + _ -> MAlonzo.RTE.mazUnreachableError + _ -> MAlonzo.RTE.mazUnreachableError + _ -> MAlonzo.RTE.mazUnreachableError + _ -> MAlonzo.RTE.mazUnreachableError + else coe + seq (coe v6) + (case coe v3 of + MAlonzo.Code.Untyped.C_'96'_18 v7 + -> let v8 + = MAlonzo.Code.Untyped.Equality.d_decEq'45''8866'_56 + (coe v0) (coe v2) (coe du_applyN_126 (coe v3) (coe v1)) in + coe + (case coe v8 of + MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 v9 v10 + -> if coe v9 + then coe + seq (coe v10) + (coe + MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 + (coe v9) + (coe + MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 + (coe C_refl_168))) + else coe + seq (coe v10) + (coe + MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 + (coe v9) + (coe + MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)) + _ -> MAlonzo.RTE.mazUnreachableError) + MAlonzo.Code.Untyped.C_ƛ_20 v7 + -> let v8 + = MAlonzo.Code.Untyped.Equality.d_decEq'45''8866'_56 + (coe v0) (coe v2) (coe du_applyN_126 (coe v3) (coe v1)) in + coe + (case coe v8 of + MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 v9 v10 + -> if coe v9 + then coe + seq (coe v10) + (coe + MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 + (coe v9) + (coe + MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 + (coe C_refl_168))) + else coe + seq (coe v10) + (coe + MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 + (coe v9) + (coe + MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)) + _ -> MAlonzo.RTE.mazUnreachableError) + MAlonzo.Code.Untyped.C__'183'__22 v7 v8 + -> let v9 + = coe + MAlonzo.Code.Relation.Nullary.Decidable.Core.du__'215''45'dec__84 + (coe + MAlonzo.Code.VerifiedCompilation.UntypedViews.du_'8943'_2404) + (coe + MAlonzo.Code.VerifiedCompilation.UntypedViews.du_'8943'_2404) in + coe + (case coe v9 of + MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 v10 v11 + -> if coe v10 + then case coe v11 of + MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 v12 + -> case coe v12 of + MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 v13 v14 + -> coe + seq (coe v13) + (coe + seq (coe v14) + (let v15 + = d_dec'45'hoist_178 + (coe v0) + (coe + MAlonzo.Code.Agda.Builtin.List.C__'8759'__22 + (coe v8) (coe v1)) + (coe v2) (coe v7) in + coe + (case coe v15 of + MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 v16 v17 + -> if coe v16 + then case coe v17 of + MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 v18 + -> coe + MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 + (coe + v16) + (coe + MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 + (coe + C_let'45''183'_150 + v18)) + _ -> MAlonzo.RTE.mazUnreachableError + else coe + seq (coe v17) + (let v18 + = MAlonzo.Code.Untyped.Equality.d_decEq'45''8866'_56 + (coe + v0) + (coe + v2) + (coe + du_applyN_126 + (coe + v3) + (coe + v1)) in + coe + (case coe + v18 of + MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 v19 v20 + -> if coe + v19 + then coe + seq + (coe + v20) + (coe + MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 + (coe + v19) + (coe + MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 + (coe + C_refl_168))) + else coe + seq + (coe + v20) + (coe + MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 + (coe + v19) + (coe + MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)) + _ -> MAlonzo.RTE.mazUnreachableError)) + _ -> MAlonzo.RTE.mazUnreachableError))) + _ -> MAlonzo.RTE.mazUnreachableError + _ -> MAlonzo.RTE.mazUnreachableError + else (let v12 + = seq + (coe v11) + (coe + MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 + (coe v10) + (coe + MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)) in + coe + (case coe v12 of + MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 v13 v14 + -> if coe v13 + then case coe v14 of + MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 v15 + -> case coe v15 of + MAlonzo.Code.VerifiedCompilation.UntypedViews.C__'183''33'__894 v18 v19 + -> coe + seq (coe v18) + (coe + seq (coe v19) + (let v20 + = d_dec'45'hoist_178 + (coe + v0) + (coe + MAlonzo.Code.Agda.Builtin.List.C__'8759'__22 + (coe + v8) + (coe + v1)) + (coe + v2) + (coe + v7) in + coe + (case coe + v20 of + MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 v21 v22 + -> if coe + v21 + then case coe + v22 of + MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 v23 + -> coe + MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 + (coe + v21) + (coe + MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 + (coe + C_let'45''183'_150 + v23)) + _ -> MAlonzo.RTE.mazUnreachableError + else coe + seq + (coe + v22) + (let v23 + = MAlonzo.Code.Untyped.Equality.d_decEq'45''8866'_56 + (coe + v0) + (coe + v2) + (coe + du_applyN_126 + (coe + v3) + (coe + v1)) in + coe + (case coe + v23 of + MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 v24 v25 + -> if coe + v24 + then coe + seq + (coe + v25) + (coe + MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 + (coe + v24) + (coe + MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 + (coe + C_refl_168))) + else coe + seq + (coe + v25) + (coe + MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 + (coe + v24) + (coe + MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)) + _ -> MAlonzo.RTE.mazUnreachableError)) + _ -> MAlonzo.RTE.mazUnreachableError))) + _ -> MAlonzo.RTE.mazUnreachableError + _ -> MAlonzo.RTE.mazUnreachableError + else coe + seq (coe v14) + (let v15 + = MAlonzo.Code.Untyped.Equality.d_decEq'45''8866'_56 + (coe v0) (coe v2) + (coe + du_applyN_126 + (coe v3) + (coe v1)) in + coe + (case coe v15 of + MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 v16 v17 + -> if coe v16 + then coe + seq + (coe v17) + (coe + MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 + (coe v16) + (coe + MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 + (coe + C_refl_168))) + else coe + seq + (coe v17) + (coe + MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 + (coe v16) + (coe + MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)) + _ -> MAlonzo.RTE.mazUnreachableError)) + _ -> MAlonzo.RTE.mazUnreachableError)) + _ -> MAlonzo.RTE.mazUnreachableError) + MAlonzo.Code.Untyped.C_force_24 v7 + -> let v8 + = MAlonzo.Code.Untyped.Equality.d_decEq'45''8866'_56 + (coe v0) (coe v2) (coe du_applyN_126 (coe v3) (coe v1)) in + coe + (case coe v8 of + MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 v9 v10 + -> if coe v9 + then coe + seq (coe v10) + (coe + MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 + (coe v9) + (coe + MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 + (coe C_refl_168))) + else coe + seq (coe v10) + (coe + MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 + (coe v9) + (coe + MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)) + _ -> MAlonzo.RTE.mazUnreachableError) + MAlonzo.Code.Untyped.C_delay_26 v7 + -> let v8 + = MAlonzo.Code.Untyped.Equality.d_decEq'45''8866'_56 + (coe v0) (coe v2) (coe du_applyN_126 (coe v3) (coe v1)) in + coe + (case coe v8 of + MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 v9 v10 + -> if coe v9 + then coe + seq (coe v10) + (coe + MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 + (coe v9) + (coe + MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 + (coe C_refl_168))) + else coe + seq (coe v10) + (coe + MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 + (coe v9) + (coe + MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)) + _ -> MAlonzo.RTE.mazUnreachableError) + MAlonzo.Code.Untyped.C_con_28 v7 + -> let v8 + = MAlonzo.Code.Untyped.Equality.d_decEq'45''8866'_56 + (coe v0) (coe v2) (coe du_applyN_126 (coe v3) (coe v1)) in + coe + (case coe v8 of + MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 v9 v10 + -> if coe v9 + then coe + seq (coe v10) + (coe + MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 + (coe v9) + (coe + MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 + (coe C_refl_168))) + else coe + seq (coe v10) + (coe + MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 + (coe v9) + (coe + MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)) + _ -> MAlonzo.RTE.mazUnreachableError) + MAlonzo.Code.Untyped.C_constr_34 v7 v8 + -> let v9 + = MAlonzo.Code.Untyped.Equality.d_decEq'45''8866'_56 + (coe v0) (coe v2) (coe du_applyN_126 (coe v3) (coe v1)) in + coe + (case coe v9 of + MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 v10 v11 + -> if coe v10 + then coe + seq (coe v11) + (coe + MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 + (coe v10) + (coe + MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 + (coe C_refl_168))) + else coe + seq (coe v11) + (coe + MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 + (coe v10) + (coe + MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)) + _ -> MAlonzo.RTE.mazUnreachableError) + MAlonzo.Code.Untyped.C_case_40 v7 v8 + -> let v9 + = MAlonzo.Code.Untyped.Equality.d_decEq'45''8866'_56 + (coe v0) (coe v2) (coe du_applyN_126 (coe v3) (coe v1)) in + coe + (case coe v9 of + MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 v10 v11 + -> if coe v10 + then coe + seq (coe v11) + (coe + MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 + (coe v10) + (coe + MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 + (coe C_refl_168))) + else coe + seq (coe v11) + (coe + MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 + (coe v10) + (coe + MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)) + _ -> MAlonzo.RTE.mazUnreachableError) + MAlonzo.Code.Untyped.C_builtin_44 v7 + -> let v8 + = MAlonzo.Code.Untyped.Equality.d_decEq'45''8866'_56 + (coe v0) (coe v2) (coe du_applyN_126 (coe v3) (coe v1)) in + coe + (case coe v8 of + MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 v9 v10 + -> if coe v9 + then coe + seq (coe v10) + (coe + MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 + (coe v9) + (coe + MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 + (coe C_refl_168))) + else coe + seq (coe v10) + (coe + MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 + (coe v9) + (coe + MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)) + _ -> MAlonzo.RTE.mazUnreachableError) + MAlonzo.Code.Untyped.C_error_46 + -> let v7 + = MAlonzo.Code.Untyped.Equality.d_decEq'45''8866'_56 + (coe v0) (coe v2) (coe du_applyN_126 (coe v3) (coe v1)) in + coe + (case coe v7 of + MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 v8 v9 + -> if coe v8 + then coe + seq (coe v9) + (coe + MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 + (coe v8) + (coe + MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 + (coe C_refl_168))) + else coe + seq (coe v9) + (coe + MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 + (coe v8) + (coe + MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)) + _ -> MAlonzo.RTE.mazUnreachableError) + _ -> MAlonzo.RTE.mazUnreachableError) + _ -> MAlonzo.RTE.mazUnreachableError) +-- VerifiedCompilation.UCSE..extendedlambda3 +d_'46'extendedlambda3_250 :: + Integer -> + 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.Agda.Builtin.Equality.T__'8801'__12 -> + MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) -> + (MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> + MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) -> + T_HoistPoly_138 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20 +d_'46'extendedlambda3_250 = erased +-- VerifiedCompilation.UCSE..extendedlambda4 +d_'46'extendedlambda4_346 :: + Integer -> + 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.Agda.Builtin.Equality.T__'8801'__12 -> + MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) -> + (T_HoistPoly_138 -> + MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) -> + (MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> + MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) -> + T_HoistPoly_138 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20 +d_'46'extendedlambda4_346 = erased +-- VerifiedCompilation.UCSE..extendedlambda5 +d_'46'extendedlambda5_386 :: + Integer -> + MAlonzo.Code.Untyped.T__'8866'_14 -> + [MAlonzo.Code.Untyped.T__'8866'_14] -> + MAlonzo.Code.Untyped.T__'8866'_14 -> + (MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> + MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) -> + (MAlonzo.Code.VerifiedCompilation.UntypedViews.T__'183''7510'__884 -> + MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) -> + (MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> + MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) -> + T_HoistPoly_138 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20 +d_'46'extendedlambda5_386 = erased +-- VerifiedCompilation.UCSE.polyNumSites +d_polyNumSites_400 :: + Integer -> + [MAlonzo.Code.Untyped.T__'8866'_14] -> + MAlonzo.Code.Untyped.T__'8866'_14 -> + MAlonzo.Code.Untyped.T__'8866'_14 -> T_HoistPoly_138 -> Integer +d_polyNumSites_400 ~v0 ~v1 ~v2 v3 v4 = du_polyNumSites_400 v3 v4 +du_polyNumSites_400 :: + MAlonzo.Code.Untyped.T__'8866'_14 -> T_HoistPoly_138 -> Integer +du_polyNumSites_400 v0 v1 + = case coe v1 of + C_let'45''183'_150 v6 + -> case coe v0 of + MAlonzo.Code.Untyped.C__'183'__22 v7 v8 + -> coe + addInt (coe (1 :: Integer)) + (coe du_polyNumSites_400 (coe v7) (coe v6)) + _ -> MAlonzo.RTE.mazUnreachableError + C_let'45'ƛ_160 v6 v7 -> coe (0 :: Integer) + C_refl_168 -> coe (0 :: Integer) + _ -> MAlonzo.RTE.mazUnreachableError diff --git a/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/UCaseOfCase.hs b/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/UCaseOfCase.hs index bcbc4eb275d..07b11231e21 100644 --- a/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/UCaseOfCase.hs +++ b/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/UCaseOfCase.hs @@ -671,7 +671,7 @@ d_isCoC'63'_264 v0 v1 v2 v43) (let v44 = coe - MAlonzo.Code.VerifiedCompilation.Certificate.du_pcePointwise_316 + MAlonzo.Code.VerifiedCompilation.Certificate.du_pcePointwise_354 (coe MAlonzo.Code.VerifiedCompilation.Trace.d_CaseOfCaseT_48) (coe @@ -688,7 +688,7 @@ d_isCoC'63'_264 v0 v1 v2 MAlonzo.Code.VerifiedCompilation.Certificate.C_proof_56 v45 -> let v46 = coe - MAlonzo.Code.VerifiedCompilation.Certificate.du_pcePointwise_316 + MAlonzo.Code.VerifiedCompilation.Certificate.du_pcePointwise_354 (coe MAlonzo.Code.VerifiedCompilation.Trace.d_CaseOfCaseT_48) (coe @@ -705,7 +705,7 @@ d_isCoC'63'_264 v0 v1 v2 MAlonzo.Code.VerifiedCompilation.Certificate.C_proof_56 v47 -> let v48 = coe - MAlonzo.Code.VerifiedCompilation.Certificate.du_pcePointwise_316 + MAlonzo.Code.VerifiedCompilation.Certificate.du_pcePointwise_354 (coe MAlonzo.Code.VerifiedCompilation.Trace.d_CaseOfCaseT_48) (coe @@ -869,7 +869,7 @@ d_'46'extendedlambda6_444 :: () -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_12 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> AgdaAny -> AgdaAny -> MAlonzo.Code.Untyped.T__'8866'_14 -> @@ -892,7 +892,7 @@ d_'46'extendedlambda7_524 :: () -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_12 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> AgdaAny -> AgdaAny -> [MAlonzo.Code.Untyped.T__'8866'_14] -> @@ -916,7 +916,7 @@ d_'46'extendedlambda8_608 :: () -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_12 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> AgdaAny -> AgdaAny -> [MAlonzo.Code.Untyped.T__'8866'_14] -> diff --git a/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/UFloatDelay.hs b/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/UFloatDelay.hs index a894616f7c8..e0466a5eba4 100644 --- a/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/UFloatDelay.hs +++ b/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/UFloatDelay.hs @@ -350,7 +350,7 @@ d_'46'extendedlambda2_196 :: () -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_12 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> AgdaAny -> AgdaAny -> MAlonzo.Code.Untyped.T__'8866'_14 -> @@ -368,7 +368,7 @@ d_'46'extendedlambda3_244 :: () -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_12 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> AgdaAny -> AgdaAny -> MAlonzo.Code.Untyped.T__'8866'_14 -> diff --git a/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/UForceCaseDelay.hs b/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/UForceCaseDelay.hs index 7ef4296a014..6c492d10eaf 100644 --- a/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/UForceCaseDelay.hs +++ b/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/UForceCaseDelay.hs @@ -269,7 +269,7 @@ d_isFCD'63'_96 v0 v1 v2 MAlonzo.Code.VerifiedCompilation.Certificate.C_proof_56 v31 -> let v32 = coe - MAlonzo.Code.VerifiedCompilation.Certificate.du_pcePointwise_316 + MAlonzo.Code.VerifiedCompilation.Certificate.du_pcePointwise_354 (coe MAlonzo.Code.VerifiedCompilation.Trace.d_ForceCaseDelayT_36) (coe @@ -382,7 +382,7 @@ d_'46'extendedlambda4_228 :: () -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_12 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> AgdaAny -> AgdaAny -> [MAlonzo.Code.Untyped.T__'8866'_14] -> @@ -401,7 +401,7 @@ d_'46'extendedlambda5_280 :: () -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_12 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> AgdaAny -> AgdaAny -> MAlonzo.Code.Untyped.T__'8866'_14 -> diff --git a/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/UForceDelay.hs b/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/UForceDelay.hs index 18c4985d265..45bd84644c4 100644 --- a/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/UForceDelay.hs +++ b/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/UForceDelay.hs @@ -421,11 +421,11 @@ d_forceDelaySimpleBefore_144 MAlonzo.Code.Untyped.C_'96'_18 (coe MAlonzo.Code.Data.Fin.Base.C_zero_12))))))))) (coe - MAlonzo.Code.Untyped.du_con'45'integer_344 (coe (1 :: Integer))))) + MAlonzo.Code.Untyped.du_con'45'integer_464 (coe (1 :: Integer))))) (coe - MAlonzo.Code.Untyped.du_con'45'integer_344 (coe (2 :: Integer))))) + MAlonzo.Code.Untyped.du_con'45'integer_464 (coe (2 :: Integer))))) (coe - MAlonzo.Code.Untyped.du_con'45'integer_344 (coe (3 :: Integer))) + MAlonzo.Code.Untyped.du_con'45'integer_464 (coe (3 :: Integer))) -- VerifiedCompilation.UForceDelay.forceDelaySimpleAfter d_forceDelaySimpleAfter_146 :: MAlonzo.Code.Untyped.T__'8866'_14 d_forceDelaySimpleAfter_146 @@ -445,11 +445,11 @@ d_forceDelaySimpleAfter_146 MAlonzo.Code.Untyped.C_'96'_18 (coe MAlonzo.Code.Data.Fin.Base.C_zero_12))))) (coe - MAlonzo.Code.Untyped.du_con'45'integer_344 (coe (1 :: Integer)))) + MAlonzo.Code.Untyped.du_con'45'integer_464 (coe (1 :: Integer)))) (coe - MAlonzo.Code.Untyped.du_con'45'integer_344 (coe (2 :: Integer)))) + MAlonzo.Code.Untyped.du_con'45'integer_464 (coe (2 :: Integer)))) (coe - MAlonzo.Code.Untyped.du_con'45'integer_344 (coe (3 :: Integer))) + MAlonzo.Code.Untyped.du_con'45'integer_464 (coe (3 :: Integer))) -- VerifiedCompilation.UForceDelay.forceDelaySimple d_forceDelaySimple_148 :: T_FD_112 d_forceDelaySimple_148 @@ -485,17 +485,17 @@ d_forceDelaySimple_148 MAlonzo.Code.VerifiedCompilation.UntypedTranslation.du_reflexive_1596 (coe (0 :: Integer)) (coe - MAlonzo.Code.Untyped.du_con'45'integer_344 (coe (1 :: Integer)))))) + MAlonzo.Code.Untyped.du_con'45'integer_464 (coe (1 :: Integer)))))) (coe MAlonzo.Code.VerifiedCompilation.UntypedTranslation.du_reflexive_1596 (coe (0 :: Integer)) (coe - MAlonzo.Code.Untyped.du_con'45'integer_344 (coe (2 :: Integer)))))) + MAlonzo.Code.Untyped.du_con'45'integer_464 (coe (2 :: Integer)))))) (coe MAlonzo.Code.VerifiedCompilation.UntypedTranslation.du_reflexive_1596 (coe (0 :: Integer)) (coe - MAlonzo.Code.Untyped.du_con'45'integer_344 (coe (3 :: Integer)))) + MAlonzo.Code.Untyped.du_con'45'integer_464 (coe (3 :: Integer)))) -- VerifiedCompilation.UForceDelay.lastDelayBreak d_lastDelayBreak_150 :: T_FD_112 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20 @@ -521,15 +521,15 @@ d_ast0_170 MAlonzo.Code.Untyped.C_builtin_44 (coe MAlonzo.Code.Builtin.C_ifThenElse_60))) (coe - MAlonzo.Code.Untyped.du_con'45'integer_344 (coe (1 :: Integer)))) + MAlonzo.Code.Untyped.du_con'45'integer_464 (coe (1 :: Integer)))) (coe MAlonzo.Code.Untyped.C_delay_26 (coe - MAlonzo.Code.Untyped.du_con'45'integer_344 (coe (1 :: Integer))))) + MAlonzo.Code.Untyped.du_con'45'integer_464 (coe (1 :: Integer))))) (coe MAlonzo.Code.Untyped.C_delay_26 (coe - MAlonzo.Code.Untyped.du_con'45'integer_344 (coe (2 :: Integer))))) + MAlonzo.Code.Untyped.du_con'45'integer_464 (coe (2 :: Integer))))) -- VerifiedCompilation.UForceDelay.ast1 d_ast1_172 :: MAlonzo.Code.Untyped.T__'8866'_14 d_ast1_172 @@ -545,11 +545,11 @@ d_ast1_172 MAlonzo.Code.Untyped.C_builtin_44 (coe MAlonzo.Code.Builtin.C_ifThenElse_60))) (coe - MAlonzo.Code.Untyped.du_con'45'integer_344 (coe (1 :: Integer)))) + MAlonzo.Code.Untyped.du_con'45'integer_464 (coe (1 :: Integer)))) (coe - MAlonzo.Code.Untyped.du_con'45'integer_344 (coe (1 :: Integer)))) + MAlonzo.Code.Untyped.du_con'45'integer_464 (coe (1 :: Integer)))) (coe - MAlonzo.Code.Untyped.du_con'45'integer_344 (coe (2 :: Integer))) + MAlonzo.Code.Untyped.du_con'45'integer_464 (coe (2 :: Integer))) -- VerifiedCompilation.UForceDelay.ifThenElseProof d_ifThenElseProof_174 :: T_FD_112 d_ifThenElseProof_174 @@ -2255,7 +2255,7 @@ d_'46'extendedlambda2_246 :: () -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_12 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> AgdaAny -> AgdaAny -> T_FD_112 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20 d_'46'extendedlambda2_246 = erased @@ -2273,7 +2273,7 @@ d_'46'extendedlambda3_320 :: () -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_12 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> AgdaAny -> AgdaAny -> (MAlonzo.Code.VerifiedCompilation.UntypedViews.T_isForce_270 -> @@ -2292,7 +2292,7 @@ d_'46'extendedlambda4_348 :: () -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_12 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> AgdaAny -> AgdaAny -> MAlonzo.Code.VerifiedCompilation.Certificate.T_ProofOrCE_50 -> @@ -2322,7 +2322,7 @@ d_'46'extendedlambda6_476 :: () -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_12 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> AgdaAny -> AgdaAny -> MAlonzo.Code.Untyped.T__'8866'_14 -> @@ -2334,7 +2334,7 @@ d_'46'extendedlambda6_476 :: () -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_12 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> AgdaAny -> AgdaAny -> T_FD_112 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20 d_'46'extendedlambda6_476 = erased @@ -2354,7 +2354,7 @@ d_'46'extendedlambda7_518 :: () -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_12 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> AgdaAny -> AgdaAny -> T_FD_112 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20 d_'46'extendedlambda7_518 = erased @@ -2381,7 +2381,7 @@ d_'46'extendedlambda8_634 :: () -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_12 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> AgdaAny -> AgdaAny -> MAlonzo.Code.VerifiedCompilation.Certificate.T_ProofOrCE_50 -> @@ -2410,7 +2410,7 @@ d_'46'extendedlambda9_688 :: () -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_12 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> AgdaAny -> AgdaAny -> MAlonzo.Code.VerifiedCompilation.Certificate.T_ProofOrCE_50 -> @@ -2434,7 +2434,7 @@ d_'46'extendedlambda10_750 :: () -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_12 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> AgdaAny -> AgdaAny -> MAlonzo.Code.VerifiedCompilation.Certificate.T_ProofOrCE_50 -> @@ -2446,7 +2446,7 @@ d_'46'extendedlambda10_750 :: () -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_12 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> AgdaAny -> AgdaAny -> MAlonzo.Code.VerifiedCompilation.Certificate.T_ProofOrCE_50 -> @@ -2470,7 +2470,7 @@ d_'46'extendedlambda11_814 :: () -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_12 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> AgdaAny -> AgdaAny -> MAlonzo.Code.VerifiedCompilation.Certificate.T_ProofOrCE_50 -> @@ -2481,7 +2481,7 @@ d_'46'extendedlambda11_814 :: () -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_12 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> AgdaAny -> AgdaAny -> MAlonzo.Code.VerifiedCompilation.Certificate.T_ProofOrCE_50 -> @@ -2506,7 +2506,7 @@ d_'46'extendedlambda12_880 :: () -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_12 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> AgdaAny -> AgdaAny -> MAlonzo.Code.Builtin.T_Builtin_2 -> @@ -2516,7 +2516,7 @@ d_'46'extendedlambda12_880 :: () -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_12 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> AgdaAny -> AgdaAny -> MAlonzo.Code.VerifiedCompilation.Certificate.T_ProofOrCE_50 -> @@ -2546,7 +2546,7 @@ d_'46'extendedlambda13_1034 :: () -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_12 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> AgdaAny -> AgdaAny -> MAlonzo.Code.VerifiedCompilation.Certificate.T_ProofOrCE_50 -> @@ -2567,7 +2567,7 @@ d_'46'extendedlambda14_1074 :: () -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_12 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> AgdaAny -> AgdaAny -> MAlonzo.Code.VerifiedCompilation.Certificate.T_ProofOrCE_50 -> @@ -2584,7 +2584,7 @@ d_'46'extendedlambda15_1190 :: () -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_12 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> AgdaAny -> AgdaAny -> (T_FD_112 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) -> @@ -2592,7 +2592,7 @@ d_'46'extendedlambda15_1190 :: () -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_12 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> AgdaAny -> AgdaAny -> (MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> @@ -2610,7 +2610,7 @@ d_'46'extendedlambda16_1214 :: () -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_12 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> AgdaAny -> AgdaAny -> (MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> @@ -2629,7 +2629,7 @@ d_'46'extendedlambda17_1238 :: () -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_12 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> AgdaAny -> AgdaAny -> (MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> @@ -2661,7 +2661,7 @@ d_'46'extendedlambda19_1340 :: () -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_12 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> AgdaAny -> AgdaAny -> (MAlonzo.Code.VerifiedCompilation.UntypedViews.T_isDelay_356 -> @@ -2681,7 +2681,7 @@ d_'46'extendedlambda20_1454 :: () -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_12 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> AgdaAny -> AgdaAny -> (T_FD_112 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) -> @@ -2689,7 +2689,7 @@ d_'46'extendedlambda20_1454 :: () -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_12 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> AgdaAny -> AgdaAny -> MAlonzo.Code.Untyped.T__'8866'_14 -> @@ -2706,7 +2706,7 @@ d_'46'extendedlambda21_1480 :: () -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_12 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> AgdaAny -> AgdaAny -> MAlonzo.Code.Untyped.T__'8866'_14 -> @@ -2724,7 +2724,7 @@ d_'46'extendedlambda22_1506 :: () -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_12 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> AgdaAny -> AgdaAny -> MAlonzo.Code.Untyped.T__'8866'_14 -> @@ -2742,7 +2742,7 @@ d_'46'extendedlambda23_1574 :: () -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_12 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> AgdaAny -> AgdaAny -> (MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> @@ -2780,7 +2780,7 @@ d_'46'extendedlambda25_1698 :: () -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_12 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> AgdaAny -> AgdaAny -> (MAlonzo.Code.VerifiedCompilation.UntypedViews.T_isForce_270 -> @@ -2803,7 +2803,7 @@ d_'46'extendedlambda26_1732 :: () -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_12 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> AgdaAny -> AgdaAny -> MAlonzo.Code.VerifiedCompilation.Certificate.T_ProofOrCE_50 -> diff --git a/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/UntypedTranslation.hs b/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/UntypedTranslation.hs index 42635c42aca..4e6ecdd4e25 100644 --- a/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/UntypedTranslation.hs +++ b/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/UntypedTranslation.hs @@ -84,7 +84,7 @@ d_translation'63'_160 :: MAlonzo.Code.Untyped.T__'8866'_14 -> ()) -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_12 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> (Integer -> MAlonzo.Code.Untyped.T__'8866'_14 -> MAlonzo.Code.Untyped.T__'8866'_14 -> @@ -98,7 +98,7 @@ du_translation'63'_160 :: Integer -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_12 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> (Integer -> MAlonzo.Code.Untyped.T__'8866'_14 -> MAlonzo.Code.Untyped.T__'8866'_14 -> @@ -1897,7 +1897,7 @@ du_translation'63'_160 v0 v1 v2 v3 v4 MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 v14 -> let v15 = coe - MAlonzo.Code.VerifiedCompilation.Certificate.du_decToPCE_246 + MAlonzo.Code.VerifiedCompilation.Certificate.du_decToPCE_284 (coe v1) (coe MAlonzo.Code.Relation.Nullary.Decidable.Core.du_map'8242'_178 @@ -2924,7 +2924,7 @@ d_decPointwiseTranslation'63'_172 :: MAlonzo.Code.Untyped.T__'8866'_14 -> ()) -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_12 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> (Integer -> MAlonzo.Code.Untyped.T__'8866'_14 -> MAlonzo.Code.Untyped.T__'8866'_14 -> @@ -2938,7 +2938,7 @@ du_decPointwiseTranslation'63'_172 :: Integer -> MAlonzo.Code.Utils.T_Either_6 MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4 - MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_12 -> + MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_10 -> (Integer -> MAlonzo.Code.Untyped.T__'8866'_14 -> MAlonzo.Code.Untyped.T__'8866'_14 -> diff --git a/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/UntypedViews.hs b/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/UntypedViews.hs index 99c6222cefb..73195e26edb 100644 --- a/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/UntypedViews.hs +++ b/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/UntypedViews.hs @@ -1002,13 +1002,13 @@ newtype T_tmCon'45'pair'7510'_1014 d_Let'7510'_In'7510'__1032 a0 a1 a2 a3 = () data T_Let'7510'_In'7510'__1032 = C_Let'33'_In'33'__1042 AgdaAny AgdaAny --- VerifiedCompilation.UntypedViews.let'ᵖ -d_let'''7510'_1048 :: +-- VerifiedCompilation.UntypedViews.let₁ᵖ +d_let'8321''7510'_1048 :: Integer -> (MAlonzo.Code.Untyped.T__'8866'_14 -> ()) -> (MAlonzo.Code.Untyped.T__'8866'_14 -> ()) -> MAlonzo.Code.Untyped.T__'8866'_14 -> () -d_let'''7510'_1048 = erased +d_let'8321''7510'_1048 = erased -- VerifiedCompilation.UntypedViews.`? d_'96''63'_1058 :: Integer -> @@ -2256,8 +2256,8 @@ du_Let'63'_In'63'__2180 v0 v1 v2 (coe MAlonzo.Code.Agda.Builtin.Bool.C_false_8) (coe MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26) _ -> MAlonzo.RTE.mazUnreachableError --- VerifiedCompilation.UntypedViews.let'? -d_let'''63'_2390 :: +-- VerifiedCompilation.UntypedViews.let₁? +d_let'8321''63'_2390 :: Integer -> (MAlonzo.Code.Untyped.T__'8866'_14 -> ()) -> (MAlonzo.Code.Untyped.T__'8866'_14 -> ()) -> @@ -2267,15 +2267,15 @@ d_let'''63'_2390 :: MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) -> MAlonzo.Code.Untyped.T__'8866'_14 -> MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 -d_let'''63'_2390 ~v0 ~v1 ~v2 = du_let'''63'_2390 -du_let'''63'_2390 :: +d_let'8321''63'_2390 ~v0 ~v1 ~v2 = du_let'8321''63'_2390 +du_let'8321''63'_2390 :: (MAlonzo.Code.Untyped.T__'8866'_14 -> MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) -> (MAlonzo.Code.Untyped.T__'8866'_14 -> MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) -> MAlonzo.Code.Untyped.T__'8866'_14 -> MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 -du_let'''63'_2390 = coe du_Let'63'_In'63'__2180 +du_let'8321''63'_2390 = coe du_Let'63'_In'63'__2180 -- VerifiedCompilation.UntypedViews.match d_match_2394 a0 a1 = () data T_match_2394 = C_match'33'_2400 diff --git a/plutus-metatheory/src/Untyped.lagda.md b/plutus-metatheory/src/Untyped.lagda.md index befa59c357e..9bc7f5aae64 100644 --- a/plutus-metatheory/src/Untyped.lagda.md +++ b/plutus-metatheory/src/Untyped.lagda.md @@ -72,8 +72,20 @@ data _⊢ (n : ℕ) : Set where pattern Let_In_ rhs body = ƛ body · rhs infix 2 Let_In_ +``` + +Convenient pattern synonyms for nested lets -pattern let' rhs body = ƛ body · rhs +``` +pattern let₁ M₁ N = ƛ N · M₁ +pattern let₂ M₁ M₂ N = (ƛ (ƛ N)) · M₁ · M₂ +pattern let₃ M₁ M₂ M₃ N = (ƛ (ƛ (ƛ N))) · M₁ · M₂ · M₃ +pattern let₄ M₁ M₂ M₃ M₄ N = (ƛ (ƛ (ƛ (ƛ N)))) · M₁ · M₂ · M₃ · M₄ +pattern let₅ M₁ M₂ M₃ M₄ M₅ N = (ƛ (ƛ (ƛ (ƛ (ƛ N))))) · M₁ · M₂ · M₃ · M₄ · M₅ +pattern let₆ M₁ M₂ M₃ M₄ M₅ M₆ N = (ƛ (ƛ (ƛ (ƛ (ƛ (ƛ N)))))) · M₁ · M₂ · M₃ · M₄ · M₅ · M₆ +pattern let₇ M₁ M₂ M₃ M₄ M₅ M₆ M₇ N = (ƛ (ƛ (ƛ (ƛ (ƛ (ƛ (ƛ N))))))) · M₁ · M₂ · M₃ · M₄ · M₅ · M₆ · M₇ +pattern let₈ M₁ M₂ M₃ M₄ M₅ M₆ M₇ M₈ N = (ƛ (ƛ (ƛ (ƛ (ƛ (ƛ (ƛ (ƛ N)))))))) · M₁ · M₂ · M₃ · M₄ · M₅ · M₆ · M₇ · M₈ +pattern let₉ M₁ M₂ M₃ M₄ M₅ M₆ M₇ M₈ M₉ N = (ƛ (ƛ (ƛ (ƛ (ƛ (ƛ (ƛ (ƛ (ƛ N))))))))) · M₁ · M₂ · M₃ · M₄ · M₅ · M₆ · M₇ · M₈ · M₉ ``` ``` diff --git a/plutus-metatheory/src/VerifiedCompilation.lagda.md b/plutus-metatheory/src/VerifiedCompilation.lagda.md index 3fc1e0c5650..430d7ad7e1d 100644 --- a/plutus-metatheory/src/VerifiedCompilation.lagda.md +++ b/plutus-metatheory/src/VerifiedCompilation.lagda.md @@ -35,6 +35,7 @@ module VerifiedCompilation where ``` open import Function using (_∘_) open import Data.Bool.Base +open import Data.List using ([]) open import Data.Maybe using (is-just ; fromMaybe) open import Agda.Builtin.Sigma using (Σ; _,_) open import Agda.Builtin.Unit using (⊤; tt) @@ -82,6 +83,7 @@ tagToRelation cseT = UCSE.UntypedCSE tagToRelation applyToCaseT = UA2C.UApplyToCase tagToRelation caseReduceT = UCR.CaseReduce tagToRelation letFloatOutT = FO.FloatOut +tagToRelation polyBuiltinT = UCSE.HoistPoly [] ``` We default to the `NotImplemented` relation to give each `OptTag` a relation: @@ -109,6 +111,7 @@ certifyPass (inj₂ cseT) _ = decider UCSE.isUntypedCSE? certifyPass (inj₂ applyToCaseT) _ = decider UA2C.a2c?ᶜᶜ certifyPass (inj₂ caseReduceT) _ = decider UCR.decide certifyPass (inj₂ letFloatOutT) _ = decider FO.decide +certifyPass (inj₂ polyBuiltinT) _ = decider' (inj₂ polyBuiltinT) (UCSE.dec-hoist []) ``` A `Certificate t` states the main theorem of a trace `t`: a sequence (product) diff --git a/plutus-metatheory/src/VerifiedCompilation/Certificate.lagda.md b/plutus-metatheory/src/VerifiedCompilation/Certificate.lagda.md index ce052ef54d7..4638ec05b43 100644 --- a/plutus-metatheory/src/VerifiedCompilation/Certificate.lagda.md +++ b/plutus-metatheory/src/VerifiedCompilation/Certificate.lagda.md @@ -103,6 +103,11 @@ decider f x y with f x y ... | proof p = proof p ... | ce ¬p tag a b = ce ¬p tag a b +decider' : ∀ {X} {P : X → X → Set} → OptTag → Binary.Decidable P → Certifiable P +decider' tag f x y with f x y +... | yes p = proof p +... | no ¬p = ce ¬p tag x y + decToPCE : {X : Set} {P : Set} → OptTag → Dec P → {before after : X} → ProofOrCE P decToPCE _ (yes p) = proof p decToPCE tag (no ¬p) {before} {after} = ce ¬p tag before after diff --git a/plutus-metatheory/src/VerifiedCompilation/FloatOut.lagda.md b/plutus-metatheory/src/VerifiedCompilation/FloatOut.lagda.md index 47e3b65ba24..568939c4b62 100644 --- a/plutus-metatheory/src/VerifiedCompilation/FloatOut.lagda.md +++ b/plutus-metatheory/src/VerifiedCompilation/FloatOut.lagda.md @@ -29,25 +29,25 @@ open import VerifiedCompilation.Certificate using (ProofOrCE; ce; proof; LetFloa data FloatApply (@++ R : Relation) : Relation where float-apply : ∀ {n} {M N K : n ⊢} {L N' : suc n ⊢} - → R M (let' K L) + → R M (let₁ K L) → R (weaken N) N' ---------------------------------------- - → FloatApply R (M · N) (let' K (L · N')) + → FloatApply R (M · N) (let₁ K (L · N')) data FloatCase (@++ R : Relation) : Relation where float-case : ∀ {n} {M N : n ⊢} {L : suc n ⊢} {Ms Ms'} - → R M (let' N L) + → R M (let₁ N L) → Pointwise R (map weaken Ms) Ms' ----------------------------------------------- - → FloatCase R (case M Ms) (let' N (case L Ms')) + → FloatCase R (case M Ms) (let₁ N (case L Ms')) data FloatForce (@++ R : Relation) : Relation where float-force : ∀ {n} {M N : n ⊢} {L : suc n ⊢} - → R M (let' N L) + → R M (let₁ N L) ------------------------------------------- - → FloatForce R (force M) (let' N (force L)) + → FloatForce R (force M) (let₁ N (force L)) ``` ## Full relation @@ -65,32 +65,32 @@ FloatOut = Fix (CompatTerm ⊕ FloatApply ⊕ FloatCase ⊕ FloatForce ⊕ Empty apply-dec : DecidableT FloatApply apply-dec R? x y with (⋯ ·? ⋯) x - ×-dec (let'? ⋯ (⋯ ·? ⋯)) y + ×-dec (let₁? ⋯ (⋯ ·? ⋯)) y ... | no ¬P = no λ {(float-apply _ _) → ¬P inhabitant} -... | yes (match! M ·! match! N , let'! (match! K) (match! L ·! match! N')) - with R? M (let' K L) ×-dec R? (weaken N) N' +... | yes (match! M ·! match! N , let₁! (match! K) (match! L ·! match! N')) + with R? M (let₁ K L) ×-dec R? (weaken N) N' ... | no ¬P = no λ {(float-apply RMM' RNN') → ¬P (RMM' , RNN') } ... | yes (RMM' , RNN') = yes (float-apply RMM' RNN') case-dec : DecidableT FloatCase case-dec R? x y with (case? ⋯ ⋯) x - ×-dec (let'? ⋯ (case? ⋯ ⋯)) y + ×-dec (let₁? ⋯ (case? ⋯ ⋯)) y ... | no ¬P×Q = no λ {(float-case _ _) → ¬P×Q inhabitant} ... | yes ( case! (match! M) (match! Ms) - , let'! (match! N) (case! (match! L) (match! Ms')) + , let₁! (match! N) (case! (match! L) (match! Ms')) ) - with R? M (let' N L) + with R? M (let₁ N L) ×-dec (pointwise? R? (map weaken Ms) Ms') ... | no ¬P×Q = no λ {(float-case RMM' RMsMs') → ¬P×Q (RMM' , RMsMs')} ... | yes (RMM' , RMsMs') = yes (float-case RMM' RMsMs') force-dec : DecidableT FloatForce force-dec R? x y - with (force? ⋯) x ×-dec (let'? ⋯ (force? ⋯)) y + with (force? ⋯) x ×-dec (let₁? ⋯ (force? ⋯)) y ... | no ¬P×Q = no λ {(float-force _) → ¬P×Q inhabitant} -... | yes (force! (match! M) , let'! (match! M') (force! (match! N'))) - with R? M (let' M' N') +... | yes (force! (match! M) , let₁! (match! M') (force! (match! N'))) + with R? M (let₁ M' N') ... | no ¬P = no λ {(float-force RMM') → ¬P RMM'} ... | yes RNN' = yes (float-force RNN') ``` @@ -161,8 +161,8 @@ Basic behaviour: ``` M M' : 1 ⊢ - M = (let' id c) · c - M' = let' id (c · c) + M = (let₁ id c) · c + M' = let₁ id (c · c) _ : does (dec M M') ≡ true _ = refl @@ -171,8 +171,8 @@ Basic behaviour: _ = refl N N' : 0 ⊢ - N = force (let' id c) - N' = let' id (force c ) + N = force (let₁ id c) + N' = let₁ id (force c ) _ : does (dec N N') ≡ true _ = refl @@ -182,15 +182,15 @@ Floating out multiple levels: ``` L L' : 0 ⊢ - L = force ( force (let' id c)) - L' = let' (ƛ (` zero)) (force (force (constr 0 []))) + L = force ( force (let₁ id c)) + L' = let₁ (ƛ (` zero)) (force (force (constr 0 []))) LL' : does (dec L L') ≡ true LL' = refl H H' : 0 ⊢ - H = ((let' id c) · c) · c - H' = let' id (c · c · c) + H = ((let₁ id c) · c) · c + H' = let₁ id (c · c · c) HH' : does (dec H H') ≡ true HH' = refl @@ -200,8 +200,8 @@ Floating in multiple places ``` K K' : 0 ⊢ - K = force (let' id M) - K' = let' id (force M') + K = force (let₁ id M) + K' = let₁ id (force M') _ : does (dec K K') ≡ true _ = refl diff --git a/plutus-metatheory/src/VerifiedCompilation/Trace.lagda.md b/plutus-metatheory/src/VerifiedCompilation/Trace.lagda.md index 64d1eff30c7..eadcc30d3b5 100644 --- a/plutus-metatheory/src/VerifiedCompilation/Trace.lagda.md +++ b/plutus-metatheory/src/VerifiedCompilation/Trace.lagda.md @@ -32,7 +32,6 @@ pragmas MUST be the same as the order of their counterparts in data UncertifiedOptTag : Set where caseOfCaseT : UncertifiedOptTag constantFoldingT : UncertifiedOptTag - polyBuiltinT : UncertifiedOptTag data CertifiedOptTag : Set where floatDelayT : CertifiedOptTag @@ -43,6 +42,7 @@ data CertifiedOptTag : Set where applyToCaseT : CertifiedOptTag caseReduceT : CertifiedOptTag letFloatOutT : CertifiedOptTag + polyBuiltinT : CertifiedOptTag OptTag = Utils.Either UncertifiedOptTag CertifiedOptTag @@ -68,7 +68,7 @@ CaseOfCaseT = Utils.inj₁ caseOfCaseT ConstantFoldingT : OptTag ConstantFoldingT = Utils.inj₁ constantFoldingT PolyBuiltinT : OptTag -PolyBuiltinT = Utils.inj₁ polyBuiltinT +PolyBuiltinT = Utils.inj₂ polyBuiltinT {-# COMPILE GHC CertifiedOptTag @@ -81,6 +81,7 @@ PolyBuiltinT = Utils.inj₁ polyBuiltinT | ApplyToCase | CaseReduce | LetFloatOut + | PolyBuiltin ) #-} {-# COMPILE GHC @@ -88,7 +89,6 @@ PolyBuiltinT = Utils.inj₁ polyBuiltinT = data UncertifiedOptStage ( CaseOfCase | ConstantFolding - | PolyBuiltin ) #-} ``` diff --git a/plutus-metatheory/src/VerifiedCompilation/UCSE.lagda.md b/plutus-metatheory/src/VerifiedCompilation/UCSE.lagda.md index 3c85a0153ac..ac02e0ad37a 100644 --- a/plutus-metatheory/src/VerifiedCompilation/UCSE.lagda.md +++ b/plutus-metatheory/src/VerifiedCompilation/UCSE.lagda.md @@ -3,7 +3,7 @@ title: VerifiedCompilation.UCSE layout: page --- -# Common Subexpression Elimination Translation Phase +# CSE and Hoist Polymorphic Builtins ``` module VerifiedCompilation.UCSE where @@ -13,18 +13,28 @@ module VerifiedCompilation.UCSE where ``` open import VerifiedCompilation.UntypedViews open import VerifiedCompilation.UntypedTranslation using (Translation; TransMatch; translation?; Relation) +open import VerifiedCompilation.UntypedViews import Relation.Binary as Binary using (Decidable) -open import Relation.Nullary using (Dec; yes; no; ¬_) -open import Untyped using (_⊢; case; builtin; _·_; force; `; ƛ; delay; con; constr; error; Let_In_) +open import Relation.Nullary using (Dec; yes; no; ¬_; from-yes) +open import Untyped using (_⊢; case; builtin; _·_; force; `; ƛ; delay; con; constr; error; Let_In_; let₂) +open import Builtin +open import Untyped.RenamingSubstitution +open import Untyped.Strictness +open import Untyped.Purity using (Pure; isPure?) import Relation.Binary.PropositionalEquality as Eq open Eq using (_≡_; refl) -open import Data.Nat using (ℕ; suc) -open import Data.Fin using (Fin; suc; zero) +open import Data.Nat using (ℕ; suc; _+_) +open import Data.Fin using (Fin; suc; zero; #_) open import Untyped.RenamingSubstitution using (_[_]) open import VerifiedCompilation.Certificate using (ProofOrCE; ce; proof; pcePointwise; DecidableCE; CseT; isProof?) open import Data.Bool.Base using (Bool; false; true) open import Data.List hiding ([_]) -open import Untyped.Strictness +open import Data.Product using (_×_; _,_) +open import Relation.Nullary using (_×-dec_) +open import Data.Unit using (⊤) +open import Data.Empty using (⊥) +open import Data.Product using (∃ ; _,_) +open import Untyped.Equality using (_≟_) ``` ## Description @@ -84,6 +94,118 @@ isUCSE? ast₁ ast₂ with (Let? ⋯ In? ⋯) ast₂ isUntypedCSE? = translation? CseT isUCSE? ``` +## Hoisting polymorphic built-ins + +This pass differs slightly from CSE in two ways: + +1. it produces multi-lets, i.e. + + (λ (λ (...)) · M₀ · ... · Mₙ + +2. all produced lets appear at the very top of the post-term. + +3. Only partially applied built-ins are lifted (always pure) + + +### Application contexts + +For describing the nested let structure we need to keep track of an application +context, represented as a list of terms. We sometimes need to apply a function +to those arguments. + +``` +applyN : ∀ {X} → X ⊢ → List (X ⊢) → X ⊢ +applyN M [] = M +applyN M (N ∷ Ns) = applyN (M · N) Ns +``` + +The relation keeps a list of function arguments as extra index, similar to the +zipper of the inliner relation: + +``` +data HoistPoly {X : ℕ} : List (X ⊢) → X ⊢ → X ⊢ → Set where + let-· + : {Ls : List (X ⊢)} + → {M N L : X ⊢} + → HoistPoly (L ∷ Ls) M N + ------------------------ + → HoistPoly Ls M (N · L) + + let-ƛ + : {Ls : List (X ⊢)} + → {M L : X ⊢} + → {N : suc X ⊢} + → Pure L + → HoistPoly Ls M (N [ L ]) + ---------------------------- + → HoistPoly (L ∷ Ls) M (ƛ N) + + refl + : {Ls : List (X ⊢)} + → {M N : X ⊢} + → M ≡ applyN N Ls + → HoistPoly Ls M N +``` + +The first two rules traverse the structure of nested lets, by collecting the +arguments and traversing the corresponding lambdas. At each lambda, we +substitute the bound term. Once we traversed the lets, we simply require terms +to be equal. + +### Decision procedure + +Termination argument: we traverse a finite amount of lets on the top-level this +would be easier to prove if we keep a substitution environment in the relation +instead of directly susbtituting having a rule for the variable case that looks +in that environment. That way, size(M) + size(N) decreases in every rule. + +``` +{-# TERMINATING #-} +dec-hoist : {X : ℕ} (Ls : List (X ⊢)) (M N : X ⊢) → Dec (HoistPoly Ls M N) +dec-hoist Ls M N + with (ƛ? ⋯) N ×-dec (⋯ ∷? ⋯) Ls +dec-hoist _ M _ | yes (ƛ! (match! N) , (match! L) ∷! (match! Ls) ) + with isPure? L ×-dec dec-hoist Ls M (N [ L ]) +... | yes (pure , hoist) = yes (let-ƛ pure hoist) +... | no ¬pure-hoist + with M ≟ applyN (ƛ N) (L ∷ Ls) +... | yes refl = yes (refl refl) +... | no ¬refl = no λ { (let-ƛ pure M~N[L]) → ¬pure-hoist (pure , M~N[L]) + ; (refl refl) → ¬refl refl + } +dec-hoist Ls M N | no ¬ƛ∷ + with (⋯ ·? ⋯) N +... | yes (match! N ·! match! L) + with dec-hoist (L ∷ Ls) M N +... | yes M~N = yes (let-· M~N) +... | no ¬M~N + with M ≟ applyN (N · L) Ls +... | yes refl = yes (refl refl) +... | no ¬refl = no λ { (let-· M~N) → ¬M~N M~N + ; (refl refl) → ¬refl refl} + +dec-hoist Ls M N | no ¬ƛ∷ | no ¬· + with M ≟ (applyN N Ls) +... | yes refl = yes (refl refl) + +... | no ¬refl = no λ { (let-ƛ pure M~N[L]) → ¬ƛ∷ inhabitant + ; (let-· _) → ¬· inhabitant + ; (refl refl) → ¬refl refl + } + +``` + +### Counting optimization sites + +The amount of expressions that appear hoisted in the post-term: + +``` +polyNumSites : ∀ {X} {Ls : List (X ⊢)} {M N : X ⊢} → HoistPoly Ls M N → ℕ +polyNumSites (let-· p) = 1 + polyNumSites p +polyNumSites (let-ƛ x p) = 0 +polyNumSites (refl x) = 0 +``` + ## Tests A few unit tests which check that the decision procedure works as expected. @@ -92,31 +214,73 @@ The third test shows that the strictness condition catches an unsound transforma ``` -M₁ : 1 ⊢ -M₁ = constr 0 [] · constr 0 [] +private -N₁ : 1 ⊢ -N₁ = Let constr 0 [] In ` zero · ` zero + M₁ : 1 ⊢ + M₁ = constr 0 [] · constr 0 [] -_ : isProof? (isUntypedCSE? M₁ N₁) ≡ true -_ = refl + N₁ : 1 ⊢ + N₁ = Let constr 0 [] In ` zero · ` zero -M₂ : 1 ⊢ -M₂ = Let constr 0 [] In ` zero + _ : isProof? (isUntypedCSE? M₁ N₁) ≡ true + _ = refl -N₂ : 1 ⊢ -N₂ = Let constr 0 [] In ` zero + M₂ : 1 ⊢ + M₂ = Let constr 0 [] In ` zero -_ : isProof? (isUntypedCSE? M₂ N₂) ≡ true -_ = refl + N₂ : 1 ⊢ + N₂ = Let constr 0 [] In ` zero -M₃ : 1 ⊢ -M₃ = constr 0 [] + _ : isProof? (isUntypedCSE? M₂ N₂) ≡ true + _ = refl -N₃ : 1 ⊢ -N₃ = Let error In constr 0 [] + M₃ : 1 ⊢ + M₃ = constr 0 [] -_ : isProof? (isUntypedCSE? M₃ N₃) ≡ false -_ = refl + N₃ : 1 ⊢ + N₃ = Let error In constr 0 [] + _ : isProof? (isUntypedCSE? M₃ N₃) ≡ false + _ = refl +``` + +Tests for HoistPoly + +``` +private + pre : 2 ⊢ + pre = force (builtin ifThenElse) + · (` (# 0)) + · (constr 0 []) + · (force (builtin trace) + · (` (# 1)) + · (constr 1 []) + ) + + post : 2 ⊢ + post = let₂ + (force (builtin ifThenElse)) + (force (builtin trace)) + ( ` (# 1) -- ifThenElse + · ` (# 2) + · constr 0 [] + · ( ` (# 0) -- trace + · ` (# 3) + · constr 1 [] + ) + ) + + open Pure + pure₁ : Pure {2} (force (builtin ifThenElse)) + pure₁ = unsat-builtin₀₋₁ refl builtin + pure₂ : Pure {2} (force (builtin trace)) + pure₂ = unsat-builtin₀₋₁ refl builtin + + -- manual derivation + pre-post : HoistPoly [] pre post + pre-post = let-· (let-· (let-ƛ pure₁ (let-ƛ pure₂ (refl refl)))) + + -- decision procedure + pre-post' : HoistPoly [] pre post + pre-post' = from-yes (dec-hoist [] pre post) ``` diff --git a/plutus-metatheory/src/VerifiedCompilation/UntypedViews.lagda.md b/plutus-metatheory/src/VerifiedCompilation/UntypedViews.lagda.md index 592f6ffb87b..a76dbe18fd2 100644 --- a/plutus-metatheory/src/VerifiedCompilation/UntypedViews.lagda.md +++ b/plutus-metatheory/src/VerifiedCompilation/UntypedViews.lagda.md @@ -300,10 +300,10 @@ data Letᵖ_Inᵖ_ (P : Pr (n ⊢)) (Q : Pr (suc n ⊢)) : Pr (n ⊢) where infix 0 Letᵖ_Inᵖ_ infix 0 Let!_In!_ -let'ᵖ : (P : Pr (n ⊢)) (Q : Pr (suc n ⊢)) → Pr (n ⊢) -let'ᵖ = Letᵖ_Inᵖ_ +let₁ᵖ : (P : Pr (n ⊢)) (Q : Pr (suc n ⊢)) → Pr (n ⊢) +let₁ᵖ = Letᵖ_Inᵖ_ -pattern let'! P Q = Let! P In! Q +pattern let₁! P Q = Let! P In! Q ``` Each predicate is decidable if the predicates on sub-terms are decidable. @@ -530,8 +530,8 @@ Let?_In?_ : {P : Pr (n ⊢)} {Q : Pr (suc n ⊢)} → Decidable P → Decidable ... | yes (PN , QM) = yes (Let! PN In! QM) ... | no ¬PN×QM = no λ { (Let! PN In! QM) → ¬PN×QM (PN , QM)} -let'? : {P : Pr (n ⊢)} {Q : Pr (suc n ⊢)} → Decidable P → Decidable Q → Decidable (let'ᵖ P Q) -let'? = Let?_In?_ +let₁? : {P : Pr (n ⊢)} {Q : Pr (suc n ⊢)} → Decidable P → Decidable Q → Decidable (let₁ᵖ P Q) +let₁? = Let?_In?_ ``` `match` is the trivial predicate that always holds: