diff --git a/plutus-metatheory/src/Builtin.lagda.md b/plutus-metatheory/src/Builtin.lagda.md index 3e34de9284c..a0ffcb9c1ac 100644 --- a/plutus-metatheory/src/Builtin.lagda.md +++ b/plutus-metatheory/src/Builtin.lagda.md @@ -42,7 +42,7 @@ open _⊢♯ renaming (pair to bpair; list to blist; array to barray) open _/_⊢⋆ open import Builtin.Constant.AtomicType -open import Utils.Reflection using (defDec;defShow;defEnum;defListConstructors) +open import Utils.Reflection using (defDec;defShow;defEnum;defFromEnum;defListConstructors) ``` ## Built-in functions @@ -688,15 +688,34 @@ Equality of Builtins is decidable. In order to prove equality we would have to p enumBuiltin : Builtin → ℕ unquoteDef enumBuiltin = defEnum (quote Builtin) enumBuiltin +fromEnumBuiltin : ℕ → Maybe Builtin +unquoteDef fromEnumBuiltin = defFromEnum (quote Builtin) fromEnumBuiltin + open import Agda.Builtin.Equality using (_≡_) open import Agda.Builtin.TrustMe using (primTrustMe) -open import Relation.Binary.PropositionalEquality using (cong) +open import Relation.Binary.PropositionalEquality using (cong; sym) open import Relation.Nullary using (Dec; yes; no; ¬_) +open import Data.Maybe.Properties using (just-injective) +open import Relation.Binary.Reasoning.Syntax +open import Function.Base using (id; _∘_) +open import Relation.Binary.PropositionalEquality.Core + using (_≡_; cong; refl; subst; trans; sym; subst₂; cong₂) + +-- TODO: this should be generated +decode-encode : ∀ x → fromEnumBuiltin (enumBuiltin x) ≡ just x +unquoteDef decode-encode = defDecodeEncode (quote Builtin) decode-encode --- TODO: this should be safe since enumBuiltin is generated; can it be proven without having to --- explicitly match on all n² cases? enumBuiltin-injective : (b1 b2 : Builtin) → enumBuiltin b1 ≡ enumBuiltin b2 → b1 ≡ b2 -enumBuiltin-injective b1 b2 b1≡b2 = primTrustMe +enumBuiltin-injective x y p = just-injective ( + begin + just x ≡⟨ sym (decode-encode x) ⟩ + fromEnumBuiltin (enumBuiltin x) ≡⟨ cong fromEnumBuiltin p ⟩ + fromEnumBuiltin (enumBuiltin y) ≡⟨ decode-encode y ⟩ + just y + ∎) + where + open Relation.Binary.PropositionalEquality.≡-Reasoning + decBuiltin : DecidableEquality Builtin decBuiltin b1 b2 with (enumBuiltin b1) Data.Nat.≟ (enumBuiltin b2) diff --git a/plutus-metatheory/src/MAlonzo/Code/Builtin.hs b/plutus-metatheory/src/MAlonzo/Code/Builtin.hs index 69cb7248585..d0891f07a71 100644 --- a/plutus-metatheory/src/MAlonzo/Code/Builtin.hs +++ b/plutus-metatheory/src/MAlonzo/Code/Builtin.hs @@ -2887,19 +2887,335 @@ d_enumBuiltin_426 v0 C_bls12'45'381'45'G1'45'multiScalarMul_188 -> coe (92 :: Integer) C_bls12'45'381'45'G2'45'multiScalarMul_190 -> coe (93 :: Integer) _ -> MAlonzo.RTE.mazUnreachableError +-- Builtin.fromEnumBuiltin +d_fromEnumBuiltin_428 :: Integer -> Maybe T_Builtin_2 +d_fromEnumBuiltin_428 v0 + = let v1 = coe MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18 in + coe + (case coe v0 of + 0 -> coe + MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 (coe C_addInteger_4) + 1 -> coe + MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 (coe C_subtractInteger_6) + 2 -> coe + MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 (coe C_multiplyInteger_8) + 3 -> coe + MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 (coe C_divideInteger_10) + 4 -> coe + MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 + (coe C_quotientInteger_12) + 5 -> coe + MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 + (coe C_remainderInteger_14) + 6 -> coe + MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 (coe C_modInteger_16) + 7 -> coe + MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 (coe C_equalsInteger_18) + 8 -> coe + MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 + (coe C_lessThanInteger_20) + 9 -> coe + MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 + (coe C_lessThanEqualsInteger_22) + 10 + -> coe + MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 + (coe C_appendByteString_24) + 11 + -> coe + MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 (coe C_consByteString_26) + 12 + -> coe + MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 + (coe C_sliceByteString_28) + 13 + -> coe + MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 + (coe C_lengthOfByteString_30) + 14 + -> coe + MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 + (coe C_indexByteString_32) + 15 + -> coe + MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 + (coe C_equalsByteString_34) + 16 + -> coe + MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 + (coe C_lessThanByteString_36) + 17 + -> coe + MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 + (coe C_lessThanEqualsByteString_38) + 18 + -> coe + MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 (coe C_sha2'45'256_40) + 19 + -> coe + MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 (coe C_sha3'45'256_42) + 20 + -> coe + MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 (coe C_blake2b'45'256_44) + 21 + -> coe + MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 + (coe C_verifyEd25519Signature_46) + 22 + -> coe + MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 + (coe C_verifyEcdsaSecp256k1Signature_48) + 23 + -> coe + MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 + (coe C_verifySchnorrSecp256k1Signature_50) + 24 + -> coe + MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 (coe C_appendString_52) + 25 + -> coe + MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 (coe C_equalsString_54) + 26 + -> coe + MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 (coe C_encodeUtf8_56) + 27 + -> coe + MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 (coe C_decodeUtf8_58) + 28 + -> coe + MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 (coe C_ifThenElse_60) + 29 + -> coe + MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 (coe C_chooseUnit_62) + 30 + -> coe MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 (coe C_trace_64) + 31 + -> coe MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 (coe C_fstPair_66) + 32 + -> coe MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 (coe C_sndPair_68) + 33 + -> coe + MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 (coe C_chooseList_70) + 34 + -> coe MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 (coe C_mkCons_72) + 35 + -> coe + MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 (coe C_headList_74) + 36 + -> coe + MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 (coe C_tailList_76) + 37 + -> coe + MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 (coe C_nullList_78) + 38 + -> coe + MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 (coe C_lengthOfArray_80) + 39 + -> coe + MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 (coe C_listToArray_82) + 40 + -> coe + MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 (coe C_indexArray_84) + 41 + -> coe + MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 (coe C_chooseData_86) + 42 + -> coe + MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 (coe C_constrData_88) + 43 + -> coe MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 (coe C_mapData_90) + 44 + -> coe + MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 (coe C_listData_92) + 45 + -> coe MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 (coe C_iData_94) + 46 + -> coe MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 (coe C_bData_96) + 47 + -> coe + MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 (coe C_unConstrData_98) + 48 + -> coe + MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 (coe C_unMapData_100) + 49 + -> coe + MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 (coe C_unListData_102) + 50 + -> coe + MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 (coe C_unIData_104) + 51 + -> coe + MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 (coe C_unBData_106) + 52 + -> coe + MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 (coe C_equalsData_108) + 53 + -> coe + MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 (coe C_serialiseData_110) + 54 + -> coe + MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 (coe C_mkPairData_112) + 55 + -> coe + MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 (coe C_mkNilData_114) + 56 + -> coe + MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 (coe C_mkNilPairData_116) + 57 + -> coe + MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 + (coe C_bls12'45'381'45'G1'45'add_118) + 58 + -> coe + MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 + (coe C_bls12'45'381'45'G1'45'neg_120) + 59 + -> coe + MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 + (coe C_bls12'45'381'45'G1'45'scalarMul_122) + 60 + -> coe + MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 + (coe C_bls12'45'381'45'G1'45'equal_124) + 61 + -> coe + MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 + (coe C_bls12'45'381'45'G1'45'hashToGroup_126) + 62 + -> coe + MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 + (coe C_bls12'45'381'45'G1'45'compress_128) + 63 + -> coe + MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 + (coe C_bls12'45'381'45'G1'45'uncompress_130) + 64 + -> coe + MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 + (coe C_bls12'45'381'45'G2'45'add_132) + 65 + -> coe + MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 + (coe C_bls12'45'381'45'G2'45'neg_134) + 66 + -> coe + MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 + (coe C_bls12'45'381'45'G2'45'scalarMul_136) + 67 + -> coe + MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 + (coe C_bls12'45'381'45'G2'45'equal_138) + 68 + -> coe + MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 + (coe C_bls12'45'381'45'G2'45'hashToGroup_140) + 69 + -> coe + MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 + (coe C_bls12'45'381'45'G2'45'compress_142) + 70 + -> coe + MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 + (coe C_bls12'45'381'45'G2'45'uncompress_144) + 71 + -> coe + MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 + (coe C_bls12'45'381'45'millerLoop_146) + 72 + -> coe + MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 + (coe C_bls12'45'381'45'mulMlResult_148) + 73 + -> coe + MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 + (coe C_bls12'45'381'45'finalVerify_150) + 74 + -> coe + MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 (coe C_keccak'45'256_152) + 75 + -> coe + MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 + (coe C_blake2b'45'224_154) + 76 + -> coe + MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 + (coe C_byteStringToInteger_156) + 77 + -> coe + MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 + (coe C_integerToByteString_158) + 78 + -> coe + MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 (coe C_andByteString_160) + 79 + -> coe + MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 (coe C_orByteString_162) + 80 + -> coe + MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 (coe C_xorByteString_164) + 81 + -> coe + MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 + (coe C_complementByteString_166) + 82 + -> coe + MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 (coe C_readBit_168) + 83 + -> coe + MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 (coe C_writeBits_170) + 84 + -> coe + MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 (coe C_replicateByte_172) + 85 + -> coe + MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 + (coe C_shiftByteString_174) + 86 + -> coe + MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 + (coe C_rotateByteString_176) + 87 + -> coe + MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 (coe C_countSetBits_178) + 88 + -> coe + MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 + (coe C_findFirstSetBit_180) + 89 + -> coe + MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 (coe C_ripemd'45'160_182) + 90 + -> coe + MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 (coe C_expModInteger_184) + 91 + -> coe + MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 (coe C_dropList_186) + 92 + -> coe + MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 + (coe C_bls12'45'381'45'G1'45'multiScalarMul_188) + 93 + -> coe + MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 + (coe C_bls12'45'381'45'G2'45'multiScalarMul_190) + _ -> coe v1) +-- Builtin.decode-encode +d_decode'45'encode_432 :: + T_Builtin_2 -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 +d_decode'45'encode_432 = erased -- Builtin.enumBuiltin-injective -d_enumBuiltin'45'injective_432 :: +d_enumBuiltin'45'injective_440 :: T_Builtin_2 -> T_Builtin_2 -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -d_enumBuiltin'45'injective_432 = erased +d_enumBuiltin'45'injective_440 = erased -- Builtin.decBuiltin -d_decBuiltin_440 :: +d_decBuiltin_472 :: T_Builtin_2 -> T_Builtin_2 -> MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 -d_decBuiltin_440 v0 v1 +d_decBuiltin_472 v0 v1 = let v2 = coe MAlonzo.Code.Relation.Nullary.Decidable.Core.du_map'8242'_178 @@ -2931,9 +3247,9 @@ d_decBuiltin_440 v0 v1 (coe MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)) _ -> MAlonzo.RTE.mazUnreachableError) -- Builtin.showBuiltin -d_showBuiltin_464 :: +d_showBuiltin_496 :: T_Builtin_2 -> MAlonzo.Code.Agda.Builtin.String.T_String_6 -d_showBuiltin_464 v0 +d_showBuiltin_496 v0 = case coe v0 of C_addInteger_4 -> coe ("addInteger" :: Data.Text.Text) C_subtractInteger_6 -> coe ("subtractInteger" :: Data.Text.Text) @@ -3061,8 +3377,8 @@ d_showBuiltin_464 v0 -> coe ("bls12-381-G2-multiScalarMul" :: Data.Text.Text) _ -> MAlonzo.RTE.mazUnreachableError -- Builtin.builtinList -d_builtinList_466 :: [T_Builtin_2] -d_builtinList_466 +d_builtinList_498 :: [T_Builtin_2] +d_builtinList_498 = coe MAlonzo.Code.Agda.Builtin.List.C__'8759'__22 (coe C_addInteger_4) (coe diff --git a/plutus-metatheory/src/MAlonzo/Code/Cost.hs b/plutus-metatheory/src/MAlonzo/Code/Cost.hs index f69d3569a7a..ab42cf2e8f0 100644 --- a/plutus-metatheory/src/MAlonzo/Code/Cost.hs +++ b/plutus-metatheory/src/MAlonzo/Code/Cost.hs @@ -486,7 +486,7 @@ d_mkKeyFromExBudgetCategory_150 v0 -> coe MAlonzo.Code.Data.String.Base.d__'43''43'__20 ("1" :: Data.Text.Text) - (MAlonzo.Code.Builtin.d_showBuiltin_464 (coe v1)) + (MAlonzo.Code.Builtin.d_showBuiltin_496 (coe v1)) MAlonzo.Code.Cost.Base.C_BStartup_42 -> coe ("2" :: Data.Text.Text) _ -> MAlonzo.RTE.mazUnreachableError -- Cost.TallyingBudget @@ -773,7 +773,7 @@ du_totalBuiltinCosts_236 v0 MAlonzo.Code.Builtin.Signature.C_atomic_12 (coe MAlonzo.Code.Builtin.Constant.AtomicType.C_aUnit_14)) (coe MAlonzo.Code.Agda.Builtin.Unit.C_tt_8)))))) - (coe MAlonzo.Code.Builtin.d_builtinList_466)) + (coe MAlonzo.Code.Builtin.d_builtinList_498)) -- Cost._.getCPU d_getCPU_244 :: MAlonzo.Code.Data.Tree.AVL.T_Tree_266 -> @@ -877,7 +877,7 @@ du_printBuiltinCost_268 v0 v1 MAlonzo.Code.Data.String.Base.d__'43''43'__20 (MAlonzo.Code.Data.String.Base.d_padRight_70 (coe ' ') (coe (22 :: Integer)) - (coe MAlonzo.Code.Builtin.d_showBuiltin_464 (coe v0))) + (coe MAlonzo.Code.Builtin.d_showBuiltin_496 (coe v0))) (coe MAlonzo.Code.Data.String.Base.d__'43''43'__20 (" " :: Data.Text.Text) @@ -924,7 +924,7 @@ du_printBuiltinReport_276 v0 (coe MAlonzo.Code.Builtin.Constant.AtomicType.C_aUnit_14)) (coe MAlonzo.Code.Agda.Builtin.Unit.C_tt_8)))))))) (coe ("" :: Data.Text.Text)) - (coe MAlonzo.Code.Builtin.d_builtinList_466) + (coe MAlonzo.Code.Builtin.d_builtinList_498) -- Cost._.formatTimePicoseconds d_formatTimePicoseconds_284 :: MAlonzo.Code.Data.Tree.AVL.T_Tree_266 -> diff --git a/plutus-metatheory/src/MAlonzo/Code/Cost/Model.hs b/plutus-metatheory/src/MAlonzo/Code/Cost/Model.hs index 14eab15270f..24edead5f30 100644 --- a/plutus-metatheory/src/MAlonzo/Code/Cost/Model.hs +++ b/plutus-metatheory/src/MAlonzo/Code/Cost/Model.hs @@ -910,13 +910,13 @@ d_getModel_480 v0 v1 (\ v6 -> coe MAlonzo.Code.Data.String.Properties.du_'8776''45'reflexive_8 - (coe MAlonzo.Code.Builtin.d_showBuiltin_464 (coe v0))) + (coe MAlonzo.Code.Builtin.d_showBuiltin_496 (coe v0))) (coe MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Properties.du_decidable_112 (coe MAlonzo.Code.Data.Char.Properties.d__'8799'__14) (coe MAlonzo.Code.Agda.Builtin.String.d_primStringToList_12 - (MAlonzo.Code.Builtin.d_showBuiltin_464 (coe v0))) + (MAlonzo.Code.Builtin.d_showBuiltin_496 (coe v0))) (coe MAlonzo.Code.Agda.Builtin.String.d_primStringToList_12 v4))) in coe @@ -1056,4 +1056,4 @@ d_createMap_584 v0 (coe MAlonzo.Code.Data.List.Base.du_map_22 (coe (\ v1 -> d_getModel_480 (coe v1) (coe v0))) - (coe MAlonzo.Code.Builtin.d_builtinList_466))) + (coe MAlonzo.Code.Builtin.d_builtinList_498))) diff --git a/plutus-metatheory/src/MAlonzo/Code/Raw.hs b/plutus-metatheory/src/MAlonzo/Code/Raw.hs index 7f0072e2549..8989ffc902b 100644 --- a/plutus-metatheory/src/MAlonzo/Code/Raw.hs +++ b/plutus-metatheory/src/MAlonzo/Code/Raw.hs @@ -386,7 +386,7 @@ d_decRTm_188 v0 v1 C_builtin_48 v4 -> coe MAlonzo.Code.Relation.Nullary.Decidable.Core.d_does_28 - (coe MAlonzo.Code.Builtin.d_decBuiltin_440 (coe v3) (coe v4)) + (coe MAlonzo.Code.Builtin.d_decBuiltin_472 (coe v3) (coe v4)) _ -> coe v2 C_wrap_50 v3 v4 v5 -> case coe v1 of diff --git a/plutus-metatheory/src/MAlonzo/Code/Untyped.hs b/plutus-metatheory/src/MAlonzo/Code/Untyped.hs index 3221586d027..eeaeee325a2 100644 --- a/plutus-metatheory/src/MAlonzo/Code/Untyped.hs +++ b/plutus-metatheory/src/MAlonzo/Code/Untyped.hs @@ -539,7 +539,7 @@ d_decUTm_284 v0 v1 MAlonzo.Code.RawU.C_UBuiltin_220 v4 -> coe MAlonzo.Code.Relation.Nullary.Decidable.Core.d_does_28 - (coe MAlonzo.Code.Builtin.d_decBuiltin_440 (coe v3) (coe v4)) + (coe MAlonzo.Code.Builtin.d_decBuiltin_472 (coe v3) (coe v4)) _ -> coe v2 MAlonzo.Code.RawU.C_UDelay_222 v3 -> case coe v1 of diff --git a/plutus-metatheory/src/MAlonzo/Code/Untyped/Equality.hs b/plutus-metatheory/src/MAlonzo/Code/Untyped/Equality.hs index cdd407bbba3..edfd7a143d1 100644 --- a/plutus-metatheory/src/MAlonzo/Code/Untyped/Equality.hs +++ b/plutus-metatheory/src/MAlonzo/Code/Untyped/Equality.hs @@ -1214,7 +1214,7 @@ du_DecEq'45'List_156 v0 -- Untyped.Equality.DecEq-Builtin d_DecEq'45'Builtin_160 :: T_DecEq_6 d_DecEq'45'Builtin_160 - = coe C_constructor_14 (coe MAlonzo.Code.Builtin.d_decBuiltin_440) + = coe C_constructor_14 (coe MAlonzo.Code.Builtin.d_decBuiltin_472) -- Untyped.Equality.DecEq-ℕ d_DecEq'45'ℕ_162 :: T_DecEq_6 d_DecEq'45'ℕ_162 diff --git a/plutus-metatheory/src/MAlonzo/Code/Utils/Reflection.hs b/plutus-metatheory/src/MAlonzo/Code/Utils/Reflection.hs index f6dfe80480b..6f61d51b68b 100644 --- a/plutus-metatheory/src/MAlonzo/Code/Utils/Reflection.hs +++ b/plutus-metatheory/src/MAlonzo/Code/Utils/Reflection.hs @@ -539,9 +539,152 @@ d_go_140 v0 v1 (coe MAlonzo.Code.Agda.Builtin.Reflection.C_nat_128 (coe v0)))) (coe d_go_140 (coe addInt (coe (1 :: Integer)) (coe v0)) (coe v3)) _ -> MAlonzo.RTE.mazUnreachableError +-- Utils.Reflection.natPat +d_natPat_148 :: + Integer -> MAlonzo.Code.Agda.Builtin.Reflection.T_Pattern_158 +d_natPat_148 v0 + = case coe v0 of + 0 -> coe + MAlonzo.Code.Agda.Builtin.Reflection.C_con_244 + (coe + (MAlonzo.RTE.QName + (8 :: Integer) (13537827747504913145 :: Integer) + "Agda.Builtin.Nat.Nat.zero" + (MAlonzo.RTE.Fixity MAlonzo.RTE.NonAssoc MAlonzo.RTE.Unrelated))) + (coe MAlonzo.Code.Agda.Builtin.List.C_'91''93'_16) + _ -> let v1 = subInt (coe v0) (coe (1 :: Integer)) in + coe + (coe + MAlonzo.Code.Agda.Builtin.Reflection.C_con_244 + (coe + (MAlonzo.RTE.QName + (12 :: Integer) (13537827747504913145 :: Integer) + "Agda.Builtin.Nat.Nat.suc" + (MAlonzo.RTE.Fixity MAlonzo.RTE.NonAssoc MAlonzo.RTE.Unrelated))) + (coe + MAlonzo.Code.Agda.Builtin.List.C__'8759'__22 + (coe + MAlonzo.Code.Agda.Builtin.Reflection.C_arg_98 + (coe + MAlonzo.Code.Agda.Builtin.Reflection.C_arg'45'info_82 + (coe MAlonzo.Code.Agda.Builtin.Reflection.C_visible_50) + (coe + MAlonzo.Code.Agda.Builtin.Reflection.C_modality_74 + (coe MAlonzo.Code.Agda.Builtin.Reflection.C_relevant_58) + (coe MAlonzo.Code.Agda.Builtin.Reflection.C_quantity'45'ω_66))) + (coe d_natPat_148 (coe v1))) + (coe MAlonzo.Code.Agda.Builtin.List.C_'91''93'_16))) +-- Utils.Reflection.mk-FromEnum +d_mk'45'FromEnum_152 :: + [AgdaAny] -> [MAlonzo.Code.Agda.Builtin.Reflection.T_Clause_160] +d_mk'45'FromEnum_152 v0 + = coe + MAlonzo.Code.Data.List.Base.du__'43''43'__32 + (coe du_go_160 (coe (0 :: Integer)) (coe v0)) + (coe + MAlonzo.Code.Data.List.Base.du_'91'_'93'_270 + (coe + MAlonzo.Code.Agda.Builtin.Reflection.C_clause_272 + (coe + MAlonzo.Code.Data.List.Base.du_'91'_'93'_270 + (coe + MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 + (coe ("_" :: Data.Text.Text)) + (coe + MAlonzo.Code.Agda.Builtin.Reflection.C_arg_98 + (coe + MAlonzo.Code.Agda.Builtin.Reflection.C_arg'45'info_82 + (coe MAlonzo.Code.Agda.Builtin.Reflection.C_visible_50) + (coe + MAlonzo.Code.Agda.Builtin.Reflection.C_modality_74 + (coe MAlonzo.Code.Agda.Builtin.Reflection.C_relevant_58) + (coe MAlonzo.Code.Agda.Builtin.Reflection.C_quantity'45'ω_66))) + (coe + MAlonzo.Code.Agda.Builtin.Reflection.C_def_184 + (coe + (MAlonzo.RTE.QName + (6 :: Integer) (13537827747504913145 :: Integer) + "Agda.Builtin.Nat.Nat" + (MAlonzo.RTE.Fixity MAlonzo.RTE.NonAssoc MAlonzo.RTE.Unrelated))) + (coe MAlonzo.Code.Agda.Builtin.List.C_'91''93'_16))))) + (coe + MAlonzo.Code.Data.List.Base.du_'91'_'93'_270 + (coe + MAlonzo.Code.Agda.Builtin.Reflection.C_arg_98 + (coe + MAlonzo.Code.Agda.Builtin.Reflection.C_arg'45'info_82 + (coe MAlonzo.Code.Agda.Builtin.Reflection.C_visible_50) + (coe + MAlonzo.Code.Agda.Builtin.Reflection.C_modality_74 + (coe MAlonzo.Code.Agda.Builtin.Reflection.C_relevant_58) + (coe MAlonzo.Code.Agda.Builtin.Reflection.C_quantity'45'ω_66))) + (coe + MAlonzo.Code.Agda.Builtin.Reflection.C_var_252 + (coe (0 :: Integer))))) + (coe + MAlonzo.Code.Agda.Builtin.Reflection.C_con_178 + (coe + (MAlonzo.RTE.QName + (18 :: Integer) (15412666033012224255 :: Integer) + "Agda.Builtin.Maybe.Maybe.nothing" + (MAlonzo.RTE.Fixity MAlonzo.RTE.NonAssoc MAlonzo.RTE.Unrelated))) + (coe MAlonzo.Code.Agda.Builtin.List.C_'91''93'_16)))) +-- Utils.Reflection._.go +d_go_160 :: + [AgdaAny] -> + Integer -> + [AgdaAny] -> [MAlonzo.Code.Agda.Builtin.Reflection.T_Clause_160] +d_go_160 ~v0 v1 v2 = du_go_160 v1 v2 +du_go_160 :: + Integer -> + [AgdaAny] -> [MAlonzo.Code.Agda.Builtin.Reflection.T_Clause_160] +du_go_160 v0 v1 + = case coe v1 of + [] -> coe v1 + (:) v2 v3 + -> coe + MAlonzo.Code.Agda.Builtin.List.C__'8759'__22 + (coe + MAlonzo.Code.Agda.Builtin.Reflection.C_clause_272 + (coe MAlonzo.Code.Agda.Builtin.List.C_'91''93'_16) + (coe + MAlonzo.Code.Data.List.Base.du_'91'_'93'_270 + (coe + MAlonzo.Code.Agda.Builtin.Reflection.C_arg_98 + (coe + MAlonzo.Code.Agda.Builtin.Reflection.C_arg'45'info_82 + (coe MAlonzo.Code.Agda.Builtin.Reflection.C_visible_50) + (coe + MAlonzo.Code.Agda.Builtin.Reflection.C_modality_74 + (coe MAlonzo.Code.Agda.Builtin.Reflection.C_relevant_58) + (coe MAlonzo.Code.Agda.Builtin.Reflection.C_quantity'45'ω_66))) + (coe d_natPat_148 (coe v0)))) + (coe + MAlonzo.Code.Agda.Builtin.Reflection.C_con_178 + (coe + (MAlonzo.RTE.QName + (16 :: Integer) (15412666033012224255 :: Integer) + "Agda.Builtin.Maybe.Maybe.just" + (MAlonzo.RTE.Fixity MAlonzo.RTE.NonAssoc MAlonzo.RTE.Unrelated))) + (coe + MAlonzo.Code.Data.List.Base.du_'91'_'93'_270 + (coe + MAlonzo.Code.Agda.Builtin.Reflection.C_arg_98 + (coe + MAlonzo.Code.Agda.Builtin.Reflection.C_arg'45'info_82 + (coe MAlonzo.Code.Agda.Builtin.Reflection.C_visible_50) + (coe + MAlonzo.Code.Agda.Builtin.Reflection.C_modality_74 + (coe MAlonzo.Code.Agda.Builtin.Reflection.C_relevant_58) + (coe MAlonzo.Code.Agda.Builtin.Reflection.C_quantity'45'ω_66))) + (coe + MAlonzo.Code.Agda.Builtin.Reflection.C_con_178 (coe v2) + (coe MAlonzo.Code.Agda.Builtin.List.C_'91''93'_16)))))) + (coe du_go_160 (coe addInt (coe (1 :: Integer)) (coe v0)) (coe v3)) + _ -> MAlonzo.RTE.mazUnreachableError -- Utils.Reflection.defEnum -d_defEnum_148 :: AgdaAny -> AgdaAny -> AgdaAny -d_defEnum_148 v0 v1 +d_defEnum_168 :: AgdaAny -> AgdaAny -> AgdaAny +d_defEnum_168 v0 v1 = coe MAlonzo.Code.Agda.Builtin.Reflection.d_bindTC_336 () () erased erased @@ -550,11 +693,22 @@ d_defEnum_148 v0 v1 coe MAlonzo.Code.Agda.Builtin.Reflection.d_defineFun_404 v1 (coe d_mk'45'Enum_134 (d_constructors_4 (coe v2)))) +-- Utils.Reflection.defFromEnum +d_defFromEnum_178 :: AgdaAny -> AgdaAny -> AgdaAny +d_defFromEnum_178 v0 v1 + = coe + MAlonzo.Code.Agda.Builtin.Reflection.d_bindTC_336 () () erased + erased + (coe MAlonzo.Code.Agda.Builtin.Reflection.d_getDefinition_408 v0) + (\ v2 -> + coe + MAlonzo.Code.Agda.Builtin.Reflection.d_defineFun_404 v1 + (d_mk'45'FromEnum_152 (coe d_constructors_4 (coe v2)))) -- Utils.Reflection.mkList -d_mkList_158 :: +d_mkList_188 :: [MAlonzo.Code.Agda.Builtin.Reflection.T_Term_154] -> MAlonzo.Code.Agda.Builtin.Reflection.T_Term_154 -d_mkList_158 v0 +d_mkList_188 v0 = case coe v0 of [] -> coe @@ -621,12 +775,12 @@ d_mkList_158 v0 MAlonzo.Code.Agda.Builtin.Reflection.C_modality_74 (coe MAlonzo.Code.Agda.Builtin.Reflection.C_relevant_58) (coe MAlonzo.Code.Agda.Builtin.Reflection.C_quantity'45'ω_66))) - (coe d_mkList_158 (coe v2))) + (coe d_mkList_188 (coe v2))) (coe MAlonzo.Code.Agda.Builtin.List.C_'91''93'_16))))) _ -> MAlonzo.RTE.mazUnreachableError -- Utils.Reflection.defListConstructors -d_defListConstructors_164 :: AgdaAny -> AgdaAny -> AgdaAny -d_defListConstructors_164 v0 v1 +d_defListConstructors_194 :: AgdaAny -> AgdaAny -> AgdaAny +d_defListConstructors_194 v0 v1 = coe MAlonzo.Code.Agda.Builtin.Reflection.d_bindTC_336 () () erased erased @@ -641,7 +795,7 @@ d_defListConstructors_164 v0 v1 (coe MAlonzo.Code.Agda.Builtin.List.C_'91''93'_16) (coe MAlonzo.Code.Agda.Builtin.List.C_'91''93'_16) (coe - d_mkList_158 + d_mkList_188 (coe MAlonzo.Code.Data.List.Base.du_map_22 (coe diff --git a/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/UCaseOfCase.hs b/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/UCaseOfCase.hs index d08b4b86363..5dba8bdb3ff 100644 --- a/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/UCaseOfCase.hs +++ b/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/UCaseOfCase.hs @@ -473,7 +473,7 @@ d_isCoCForce'63'_162 v0 v1 = coe MAlonzo.Code.Relation.Nullary.Decidable.Core.du__'215''45'dec__84 (coe - MAlonzo.Code.Builtin.d_decBuiltin_440 + MAlonzo.Code.Builtin.d_decBuiltin_472 (coe v30) (coe diff --git a/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/UForceDelay.hs b/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/UForceDelay.hs index b3d0a1c28ae..30618060ba5 100644 --- a/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/UForceDelay.hs +++ b/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/UForceDelay.hs @@ -1074,13 +1074,13 @@ d_isFD'63'_184 v0 v1 v2 v3 = coe MAlonzo.Code.Relation.Nullary.Decidable.Core.du__'215''45'dec__84 (coe - MAlonzo.Code.Builtin.d_decBuiltin_440 + MAlonzo.Code.Builtin.d_decBuiltin_472 (coe v53) (coe v69)) (coe - MAlonzo.Code.Builtin.d_decBuiltin_440 + MAlonzo.Code.Builtin.d_decBuiltin_472 (coe v53) (coe @@ -1811,13 +1811,13 @@ d_isFD'63'_184 v0 v1 v2 v3 = coe MAlonzo.Code.Relation.Nullary.Decidable.Core.du__'215''45'dec__84 (coe - MAlonzo.Code.Builtin.d_decBuiltin_440 + MAlonzo.Code.Builtin.d_decBuiltin_472 (coe v64) (coe v80)) (coe - MAlonzo.Code.Builtin.d_decBuiltin_440 + MAlonzo.Code.Builtin.d_decBuiltin_472 (coe v64) (coe diff --git a/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/UntypedViews.hs b/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/UntypedViews.hs index 8909eaaf35c..e5dea320946 100644 --- a/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/UntypedViews.hs +++ b/plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/UntypedViews.hs @@ -2141,7 +2141,7 @@ d_addComm'63'_2130 v0 v1 v2 (coe du_builtin'63'_1764 (coe - MAlonzo.Code.Builtin.d_decBuiltin_440 + MAlonzo.Code.Builtin.d_decBuiltin_472 (coe MAlonzo.Code.Builtin.C_addInteger_4))) (\ v3 -> coe du_'8943'_1880) in coe @@ -2215,7 +2215,7 @@ d_addComm'63'_2130 v0 v1 v2 (coe du_builtin'63'_1764 (coe - MAlonzo.Code.Builtin.d_decBuiltin_440 + MAlonzo.Code.Builtin.d_decBuiltin_472 (coe MAlonzo.Code.Builtin.C_addInteger_4))) (coe @@ -2440,7 +2440,7 @@ d_addComm'63'_2130 v0 v1 v2 (coe du_builtin'63'_1764 (coe - MAlonzo.Code.Builtin.d_decBuiltin_440 + MAlonzo.Code.Builtin.d_decBuiltin_472 (coe MAlonzo.Code.Builtin.C_addInteger_4))) (coe diff --git a/plutus-metatheory/src/Utils/Reflection.lagda.md b/plutus-metatheory/src/Utils/Reflection.lagda.md index b8a6149792f..2b30f7e100a 100644 --- a/plutus-metatheory/src/Utils/Reflection.lagda.md +++ b/plutus-metatheory/src/Utils/Reflection.lagda.md @@ -24,6 +24,7 @@ open import Agda.Builtin.Reflection open import Reflection open import Relation.Binary.PropositionalEquality using (refl) open import Relation.Nullary using (_because_;Reflects;ofʸ;ofⁿ) +open import Data.Maybe using (just) ``` Some definitions to help define functions by reflection @@ -124,11 +125,41 @@ mk-Enum = go 0 ((lit (nat acc))) ∷ go (suc acc) cs +natPat : ℕ → Pattern +natPat zero = con (quote zero) [] +natPat (suc n) = con (quote suc) (vArg (natPat n) ∷ []) + + +mk-FromEnum : List Name → List Clause +mk-FromEnum xs = go 0 xs ++ [ clause [ ("foo" , vArg (quoteTerm ℕ)) ] [ vArg (var zero) ] (con (quote nothing) []) ] + where + go : ℕ → List Name → List Clause + go _ [] = [] + go acc (c ∷ cs) = + clause + [] + [ vArg (natPat acc) ] + (con + (quote just) + [ vArg (con c []) ] + ) + ∷ go (suc acc) cs + defEnum : Name → Name → TC ⊤ defEnum T defName = do - d ← getDefinition T - let cls = mk-Enum (constructors d) - defineFun defName cls + d ← getDefinition T + let cls = mk-Enum (constructors d) + defineFun defName cls + +defFromEnum : Name → Name → TC ⊤ +defFromEnum type defName = do + d ← getDefinition type + let clauses = mk-FromEnum (constructors d) + defineFun defName clauses + +defDecodeEncode : Name → Name → TC ⊤ +defDecodeEncode T defName = {! !} + ```