Skip to content

Commit 47a0318

Browse files
SeungheonOhSeungheonOh
committed
Add CaseApply to metatheory
1 parent 57ce342 commit 47a0318

File tree

12 files changed

+50508
-50490
lines changed

12 files changed

+50508
-50490
lines changed

‎plutus-metatheory/src/FFI/AgdaUnparse.hs‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -46,6 +46,7 @@ instance AgdaUnparse UPLC.DefaultFun where
4646
agdaUnparse = usToHyphen . lowerInitialChar . show
4747

4848
instance AgdaUnparse SimplifierStage where
49+
agdaUnparse CaseApply = "caseApplyT"
4950
agdaUnparse FloatDelay = "floatDelayT"
5051
agdaUnparse ForceDelay = "forceDelayT"
5152
agdaUnparse ForceCaseDelay = "forceCaseDelayT"

‎plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation.hs‎

Lines changed: 49704 additions & 49694 deletions
Large diffs are not rendered by default.

‎plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/Certificate.hs‎

Lines changed: 73 additions & 69 deletions
Original file line numberDiff line numberDiff line change
@@ -28,27 +28,30 @@ import UntypedPlutusCore.Transform.Simplifier
2828
-- VerifiedCompilation.Certificate.SimplifierTag
2929
d_SimplifierTag_4 = ()
3030
type T_SimplifierTag_4 = SimplifierStage
31-
pattern C_floatDelayT_6 = FloatDelay
32-
pattern C_forceDelayT_8 = ForceDelay
33-
pattern C_forceCaseDelayT_10 = ForceCaseDelay
34-
pattern C_caseOfCaseT_12 = CaseOfCase
35-
pattern C_caseReduceT_14 = CaseReduce
36-
pattern C_inlineT_16 = Inline
37-
pattern C_cseT_18 = CSE
38-
check_floatDelayT_6 :: T_SimplifierTag_4
39-
check_floatDelayT_6 = FloatDelay
40-
check_forceDelayT_8 :: T_SimplifierTag_4
41-
check_forceDelayT_8 = ForceDelay
42-
check_forceCaseDelayT_10 :: T_SimplifierTag_4
43-
check_forceCaseDelayT_10 = ForceCaseDelay
44-
check_caseOfCaseT_12 :: T_SimplifierTag_4
45-
check_caseOfCaseT_12 = CaseOfCase
46-
check_caseReduceT_14 :: T_SimplifierTag_4
47-
check_caseReduceT_14 = CaseReduce
48-
check_inlineT_16 :: T_SimplifierTag_4
49-
check_inlineT_16 = Inline
50-
check_cseT_18 :: T_SimplifierTag_4
51-
check_cseT_18 = CSE
31+
pattern C_caseApplyT_6 = FloatDelay
32+
pattern C_floatDelayT_8 = ForceDelay
33+
pattern C_forceDelayT_10 = ForceCaseDelay
34+
pattern C_forceCaseDelayT_12 = CaseOfCase
35+
pattern C_caseOfCaseT_14 = CaseReduce
36+
pattern C_caseReduceT_16 = Inline
37+
pattern C_inlineT_18 = CSE
38+
pattern C_cseT_20 = CaseApply
39+
check_caseApplyT_6 :: T_SimplifierTag_4
40+
check_caseApplyT_6 = FloatDelay
41+
check_floatDelayT_8 :: T_SimplifierTag_4
42+
check_floatDelayT_8 = ForceDelay
43+
check_forceDelayT_10 :: T_SimplifierTag_4
44+
check_forceDelayT_10 = ForceCaseDelay
45+
check_forceCaseDelayT_12 :: T_SimplifierTag_4
46+
check_forceCaseDelayT_12 = CaseOfCase
47+
check_caseOfCaseT_14 :: T_SimplifierTag_4
48+
check_caseOfCaseT_14 = CaseReduce
49+
check_caseReduceT_16 :: T_SimplifierTag_4
50+
check_caseReduceT_16 = Inline
51+
check_inlineT_18 :: T_SimplifierTag_4
52+
check_inlineT_18 = CSE
53+
check_cseT_20 :: T_SimplifierTag_4
54+
check_cseT_20 = CaseApply
5255
cover_SimplifierTag_4 :: SimplifierStage -> ()
5356
cover_SimplifierTag_4 x
5457
= case x of
@@ -59,63 +62,64 @@ cover_SimplifierTag_4 x
5962
CaseReduce -> ()
6063
Inline -> ()
6164
CSE -> ()
65+
CaseApply -> ()
6266
-- VerifiedCompilation.Certificate.ProofOrCE
63-
d_ProofOrCE_28 a0 a1 = ()
64-
data T_ProofOrCE_28
65-
= C_proof_34 AgdaAny | C_ce_42 T_SimplifierTag_4 AgdaAny AgdaAny
67+
d_ProofOrCE_30 a0 a1 = ()
68+
data T_ProofOrCE_30
69+
= C_proof_36 AgdaAny | C_ce_44 T_SimplifierTag_4 AgdaAny AgdaAny
6670
-- VerifiedCompilation.Certificate.decToPCE
67-
d_decToPCE_52 ::
71+
d_decToPCE_54 ::
6872
() ->
6973
() ->
7074
T_SimplifierTag_4 ->
7175
MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
72-
AgdaAny -> AgdaAny -> T_ProofOrCE_28
73-
d_decToPCE_52 ~v0 ~v1 v2 v3 v4 v5 = du_decToPCE_52 v2 v3 v4 v5
74-
du_decToPCE_52 ::
76+
AgdaAny -> AgdaAny -> T_ProofOrCE_30
77+
d_decToPCE_54 ~v0 ~v1 v2 v3 v4 v5 = du_decToPCE_54 v2 v3 v4 v5
78+
du_decToPCE_54 ::
7579
T_SimplifierTag_4 ->
7680
MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
77-
AgdaAny -> AgdaAny -> T_ProofOrCE_28
78-
du_decToPCE_52 v0 v1 v2 v3
81+
AgdaAny -> AgdaAny -> T_ProofOrCE_30
82+
du_decToPCE_54 v0 v1 v2 v3
7983
= case coe v1 of
8084
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 v4 v5
8185
-> if coe v4
8286
then case coe v5 of
8387
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 v6
84-
-> coe C_proof_34 (coe v6)
88+
-> coe C_proof_36 (coe v6)
8589
_ -> MAlonzo.RTE.mazUnreachableError
86-
else coe seq (coe v5) (coe C_ce_42 v0 v2 v3)
90+
else coe seq (coe v5) (coe C_ce_44 v0 v2 v3)
8791
_ -> MAlonzo.RTE.mazUnreachableError
8892
-- VerifiedCompilation.Certificate.pceToDec
89-
d_pceToDec_66 ::
93+
d_pceToDec_68 ::
9094
() ->
91-
T_ProofOrCE_28 ->
95+
T_ProofOrCE_30 ->
9296
MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
93-
d_pceToDec_66 ~v0 v1 = du_pceToDec_66 v1
94-
du_pceToDec_66 ::
95-
T_ProofOrCE_28 ->
97+
d_pceToDec_68 ~v0 v1 = du_pceToDec_68 v1
98+
du_pceToDec_68 ::
99+
T_ProofOrCE_30 ->
96100
MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
97-
du_pceToDec_66 v0
101+
du_pceToDec_68 v0
98102
= case coe v0 of
99-
C_proof_34 v1
103+
C_proof_36 v1
100104
-> coe
101105
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
102106
(coe MAlonzo.Code.Agda.Builtin.Bool.C_true_10)
103107
(coe MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 (coe v1))
104-
C_ce_42 v4 v5 v6
108+
C_ce_44 v4 v5 v6
105109
-> coe
106110
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
107111
(coe MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
108112
(coe MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
109113
_ -> MAlonzo.RTE.mazUnreachableError
110114
-- VerifiedCompilation.Certificate.MatchOrCE
111-
d_MatchOrCE_80 ::
115+
d_MatchOrCE_82 ::
112116
() ->
113117
() ->
114118
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
115119
(AgdaAny -> AgdaAny -> ()) -> ()
116-
d_MatchOrCE_80 = erased
120+
d_MatchOrCE_82 = erased
117121
-- VerifiedCompilation.Certificate.matchOrCE
118-
d_matchOrCE_100 ::
122+
d_matchOrCE_102 ::
119123
() ->
120124
() ->
121125
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
@@ -124,74 +128,74 @@ d_matchOrCE_100 ::
124128
(AgdaAny ->
125129
AgdaAny ->
126130
MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
127-
AgdaAny -> AgdaAny -> T_ProofOrCE_28
128-
d_matchOrCE_100 ~v0 ~v1 ~v2 ~v3 v4 v5 v6 v7
129-
= du_matchOrCE_100 v4 v5 v6 v7
130-
du_matchOrCE_100 ::
131+
AgdaAny -> AgdaAny -> T_ProofOrCE_30
132+
d_matchOrCE_102 ~v0 ~v1 ~v2 ~v3 v4 v5 v6 v7
133+
= du_matchOrCE_102 v4 v5 v6 v7
134+
du_matchOrCE_102 ::
131135
T_SimplifierTag_4 ->
132136
(AgdaAny ->
133137
AgdaAny ->
134138
MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
135-
AgdaAny -> AgdaAny -> T_ProofOrCE_28
136-
du_matchOrCE_100 v0 v1 v2 v3
139+
AgdaAny -> AgdaAny -> T_ProofOrCE_30
140+
du_matchOrCE_102 v0 v1 v2 v3
137141
= let v4 = coe v1 v2 v3 in
138142
coe
139143
(case coe v4 of
140144
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 v5 v6
141145
-> if coe v5
142146
then case coe v6 of
143147
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 v7
144-
-> coe C_proof_34 (coe v7)
148+
-> coe C_proof_36 (coe v7)
145149
_ -> MAlonzo.RTE.mazUnreachableError
146-
else coe seq (coe v6) (coe C_ce_42 v0 v2 v3)
150+
else coe seq (coe v6) (coe C_ce_44 v0 v2 v3)
147151
_ -> MAlonzo.RTE.mazUnreachableError)
148152
-- VerifiedCompilation.Certificate.pcePointwise
149-
d_pcePointwise_142 ::
153+
d_pcePointwise_144 ::
150154
() ->
151155
() ->
152156
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
153157
(AgdaAny -> AgdaAny -> ()) ->
154158
T_SimplifierTag_4 ->
155-
(AgdaAny -> AgdaAny -> T_ProofOrCE_28) ->
156-
[AgdaAny] -> [AgdaAny] -> T_ProofOrCE_28
157-
d_pcePointwise_142 ~v0 ~v1 ~v2 ~v3 v4 v5 v6 v7
158-
= du_pcePointwise_142 v4 v5 v6 v7
159-
du_pcePointwise_142 ::
159+
(AgdaAny -> AgdaAny -> T_ProofOrCE_30) ->
160+
[AgdaAny] -> [AgdaAny] -> T_ProofOrCE_30
161+
d_pcePointwise_144 ~v0 ~v1 ~v2 ~v3 v4 v5 v6 v7
162+
= du_pcePointwise_144 v4 v5 v6 v7
163+
du_pcePointwise_144 ::
160164
T_SimplifierTag_4 ->
161-
(AgdaAny -> AgdaAny -> T_ProofOrCE_28) ->
162-
[AgdaAny] -> [AgdaAny] -> T_ProofOrCE_28
163-
du_pcePointwise_142 v0 v1 v2 v3
165+
(AgdaAny -> AgdaAny -> T_ProofOrCE_30) ->
166+
[AgdaAny] -> [AgdaAny] -> T_ProofOrCE_30
167+
du_pcePointwise_144 v0 v1 v2 v3
164168
= case coe v2 of
165169
[]
166170
-> case coe v3 of
167171
[]
168172
-> coe
169-
C_proof_34
173+
C_proof_36
170174
(coe
171175
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C_'91''93'_56)
172-
(:) v4 v5 -> coe C_ce_42 v0 v2 v5
176+
(:) v4 v5 -> coe C_ce_44 v0 v2 v5
173177
_ -> MAlonzo.RTE.mazUnreachableError
174178
(:) v4 v5
175179
-> case coe v3 of
176-
[] -> coe C_ce_42 v0 v5 v3
180+
[] -> coe C_ce_44 v0 v5 v3
177181
(:) v6 v7
178182
-> let v8 = coe v1 v4 v6 in
179183
coe
180184
(case coe v8 of
181-
C_proof_34 v9
185+
C_proof_36 v9
182186
-> let v10
183-
= coe du_pcePointwise_142 (coe v0) (coe v1) (coe v5) (coe v7) in
187+
= coe du_pcePointwise_144 (coe v0) (coe v1) (coe v5) (coe v7) in
184188
coe
185189
(case coe v10 of
186-
C_proof_34 v11
190+
C_proof_36 v11
187191
-> coe
188-
C_proof_34
192+
C_proof_36
189193
(coe
190194
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C__'8759'__62
191195
v9 v11)
192-
C_ce_42 v14 v15 v16 -> coe C_ce_42 v14 v15 v16
196+
C_ce_44 v14 v15 v16 -> coe C_ce_44 v14 v15 v16
193197
_ -> MAlonzo.RTE.mazUnreachableError)
194-
C_ce_42 v12 v13 v14 -> coe C_ce_42 v12 v13 v14
198+
C_ce_44 v12 v13 v14 -> coe C_ce_44 v12 v13 v14
195199
_ -> MAlonzo.RTE.mazUnreachableError)
196200
_ -> MAlonzo.RTE.mazUnreachableError
197201
_ -> MAlonzo.RTE.mazUnreachableError

‎plutus-metatheory/src/MAlonzo/Code/VerifiedCompilation/UCSE.hs‎

Lines changed: 11 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -44,32 +44,32 @@ d_isUntypedCSE'63'_32 ::
4444
MAlonzo.Code.Untyped.Equality.T_DecEq_6 ->
4545
MAlonzo.Code.Untyped.T__'8866'_14 ->
4646
MAlonzo.Code.Untyped.T__'8866'_14 ->
47-
MAlonzo.Code.VerifiedCompilation.Certificate.T_ProofOrCE_28
47+
MAlonzo.Code.VerifiedCompilation.Certificate.T_ProofOrCE_30
4848
d_isUntypedCSE'63'_32 ~v0 v1 = du_isUntypedCSE'63'_32 v1
4949
du_isUntypedCSE'63'_32 ::
5050
MAlonzo.Code.Untyped.Equality.T_DecEq_6 ->
5151
MAlonzo.Code.Untyped.T__'8866'_14 ->
5252
MAlonzo.Code.Untyped.T__'8866'_14 ->
53-
MAlonzo.Code.VerifiedCompilation.Certificate.T_ProofOrCE_28
53+
MAlonzo.Code.VerifiedCompilation.Certificate.T_ProofOrCE_30
5454
du_isUntypedCSE'63'_32 v0
5555
= coe
5656
MAlonzo.Code.VerifiedCompilation.UntypedTranslation.du_translation'63'_178
5757
erased (coe v0)
58-
(coe MAlonzo.Code.VerifiedCompilation.Certificate.C_cseT_18)
58+
(coe MAlonzo.Code.VerifiedCompilation.Certificate.C_cseT_20)
5959
(\ v1 v2 v3 v4 -> coe du_isUCSE'63'_38 v2 v3 v4)
6060
-- VerifiedCompilation.UCSE.isUCSE?
6161
d_isUCSE'63'_38 ::
6262
() ->
6363
MAlonzo.Code.Untyped.Equality.T_DecEq_6 ->
6464
MAlonzo.Code.Untyped.T__'8866'_14 ->
6565
MAlonzo.Code.Untyped.T__'8866'_14 ->
66-
MAlonzo.Code.VerifiedCompilation.Certificate.T_ProofOrCE_28
66+
MAlonzo.Code.VerifiedCompilation.Certificate.T_ProofOrCE_30
6767
d_isUCSE'63'_38 ~v0 v1 v2 v3 = du_isUCSE'63'_38 v1 v2 v3
6868
du_isUCSE'63'_38 ::
6969
MAlonzo.Code.Untyped.Equality.T_DecEq_6 ->
7070
MAlonzo.Code.Untyped.T__'8866'_14 ->
7171
MAlonzo.Code.Untyped.T__'8866'_14 ->
72-
MAlonzo.Code.VerifiedCompilation.Certificate.T_ProofOrCE_28
72+
MAlonzo.Code.VerifiedCompilation.Certificate.T_ProofOrCE_30
7373
du_isUCSE'63'_38 v0 v1 v2
7474
= let v3
7575
= coe
@@ -112,13 +112,13 @@ du_isUCSE'63'_38 v0 v1 v2
112112
(coe v15) (coe v12)) in
113113
coe
114114
(case coe v16 of
115-
MAlonzo.Code.VerifiedCompilation.Certificate.C_proof_34 v17
115+
MAlonzo.Code.VerifiedCompilation.Certificate.C_proof_36 v17
116116
-> coe
117-
MAlonzo.Code.VerifiedCompilation.Certificate.C_proof_34
117+
MAlonzo.Code.VerifiedCompilation.Certificate.C_proof_36
118118
(coe C_cse_16 v17)
119-
MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_42 v20 v21 v22
119+
MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_44 v20 v21 v22
120120
-> coe
121-
MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_42
121+
MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_44
122122
v20 v21 v22
123123
_ -> MAlonzo.RTE.mazUnreachableError)))
124124
_ -> MAlonzo.RTE.mazUnreachableError
@@ -129,8 +129,8 @@ du_isUCSE'63'_38 v0 v1 v2
129129
else coe
130130
seq (coe v5)
131131
(coe
132-
MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_42
133-
(coe MAlonzo.Code.VerifiedCompilation.Certificate.C_cseT_18) v1 v2)
132+
MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_44
133+
(coe MAlonzo.Code.VerifiedCompilation.Certificate.C_cseT_20) v1 v2)
134134
_ -> MAlonzo.RTE.mazUnreachableError)
135135
-- VerifiedCompilation.UCSE..extendedlambda0
136136
d_'46'extendedlambda0_54 ::

0 commit comments

Comments
 (0)