Skip to content

Commit 86ec713

Browse files
ana-pantilieana-pantilie
committed
Force-Case-Delay final version
1 parent 2744281 commit 86ec713

9 files changed

Lines changed: 9374 additions & 2972 deletions

File tree

‎plutus-metatheory/plutus-metatheory.cabal‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -374,6 +374,7 @@ library
374374
MAlonzo.Code.VerifiedCompilation.UCaseReduce
375375
MAlonzo.Code.VerifiedCompilation.UCSE
376376
MAlonzo.Code.VerifiedCompilation.UFloatDelay
377+
MAlonzo.Code.VerifiedCompilation.UForceCaseDelay
377378
MAlonzo.Code.VerifiedCompilation.UForceDelay
378379
MAlonzo.Code.VerifiedCompilation.UInline
379380
MAlonzo.Code.VerifiedCompilation.UntypedTranslation

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

Lines changed: 8359 additions & 2828 deletions
Large diffs are not rendered by default.

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

Lines changed: 56 additions & 34 deletions
Original file line numberDiff line numberDiff line change
@@ -20,6 +20,7 @@ import qualified Data.Text
2020
import qualified MAlonzo.Code.Agda.Builtin.Bool
2121
import qualified MAlonzo.Code.Agda.Builtin.List
2222
import qualified MAlonzo.Code.Agda.Primitive
23+
import qualified MAlonzo.Code.Data.Bool.Base
2324
import qualified MAlonzo.Code.Data.Irrelevant
2425
import qualified MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base
2526
import qualified MAlonzo.Code.Relation.Nullary.Decidable.Core
@@ -144,40 +145,61 @@ data T_CertResult_60
144145
d_ProofOrCE_86 a0 a1 = ()
145146
data T_ProofOrCE_86
146147
= C_proof_92 AgdaAny | C_ce_100 T_SimplifierTag_4 AgdaAny AgdaAny
148+
-- VerifiedCompilation.Certificate.isProof?
149+
d_isProof'63'_104 ::
150+
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
151+
() -> T_ProofOrCE_86 -> Bool
152+
d_isProof'63'_104 ~v0 ~v1 v2 = du_isProof'63'_104 v2
153+
du_isProof'63'_104 :: T_ProofOrCE_86 -> Bool
154+
du_isProof'63'_104 v0
155+
= case coe v0 of
156+
C_proof_92 v1 -> coe MAlonzo.Code.Agda.Builtin.Bool.C_true_10
157+
C_ce_100 v4 v5 v6 -> coe MAlonzo.Code.Agda.Builtin.Bool.C_false_8
158+
_ -> MAlonzo.RTE.mazUnreachableError
159+
-- VerifiedCompilation.Certificate.isCE?
160+
d_isCE'63'_108 ::
161+
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
162+
() -> T_ProofOrCE_86 -> Bool
163+
d_isCE'63'_108 ~v0 ~v1 v2 = du_isCE'63'_108 v2
164+
du_isCE'63'_108 :: T_ProofOrCE_86 -> Bool
165+
du_isCE'63'_108 v0
166+
= coe
167+
MAlonzo.Code.Data.Bool.Base.d_not_22
168+
(coe du_isProof'63'_104 (coe v0))
147169
-- VerifiedCompilation.Certificate.Proof?
148-
d_Proof'63'_106 a0 a1 = ()
149-
data T_Proof'63'_106
150-
= C_proof_112 AgdaAny |
151-
C_abort_118 T_SimplifierTag_4 AgdaAny AgdaAny
170+
d_Proof'63'_114 a0 a1 = ()
171+
data T_Proof'63'_114
172+
= C_proof_120 AgdaAny |
173+
C_abort_126 T_SimplifierTag_4 AgdaAny AgdaAny
152174
-- VerifiedCompilation.Certificate._>>=_
153-
d__'62''62''61'__128 ::
175+
d__'62''62''61'__136 ::
154176
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
155177
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
156178
() ->
157179
() ->
158-
T_Proof'63'_106 -> (AgdaAny -> T_Proof'63'_106) -> T_Proof'63'_106
159-
d__'62''62''61'__128 ~v0 ~v1 ~v2 ~v3 v4 v5
160-
= du__'62''62''61'__128 v4 v5
161-
du__'62''62''61'__128 ::
162-
T_Proof'63'_106 -> (AgdaAny -> T_Proof'63'_106) -> T_Proof'63'_106
163-
du__'62''62''61'__128 v0 v1
180+
T_Proof'63'_114 -> (AgdaAny -> T_Proof'63'_114) -> T_Proof'63'_114
181+
d__'62''62''61'__136 ~v0 ~v1 ~v2 ~v3 v4 v5
182+
= du__'62''62''61'__136 v4 v5
183+
du__'62''62''61'__136 ::
184+
T_Proof'63'_114 -> (AgdaAny -> T_Proof'63'_114) -> T_Proof'63'_114
185+
du__'62''62''61'__136 v0 v1
164186
= case coe v0 of
165-
C_proof_112 v2 -> coe v1 v2
166-
C_abort_118 v4 v5 v6 -> coe C_abort_118 v4 v5 v6
187+
C_proof_120 v2 -> coe v1 v2
188+
C_abort_126 v4 v5 v6 -> coe C_abort_126 v4 v5 v6
167189
_ -> MAlonzo.RTE.mazUnreachableError
168190
-- VerifiedCompilation.Certificate.decToPCE
169-
d_decToPCE_148 ::
191+
d_decToPCE_156 ::
170192
() ->
171193
() ->
172194
T_SimplifierTag_4 ->
173195
MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
174196
AgdaAny -> AgdaAny -> T_ProofOrCE_86
175-
d_decToPCE_148 ~v0 ~v1 v2 v3 v4 v5 = du_decToPCE_148 v2 v3 v4 v5
176-
du_decToPCE_148 ::
197+
d_decToPCE_156 ~v0 ~v1 v2 v3 v4 v5 = du_decToPCE_156 v2 v3 v4 v5
198+
du_decToPCE_156 ::
177199
T_SimplifierTag_4 ->
178200
MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
179201
AgdaAny -> AgdaAny -> T_ProofOrCE_86
180-
du_decToPCE_148 v0 v1 v2 v3
202+
du_decToPCE_156 v0 v1 v2 v3
181203
= case coe v1 of
182204
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 v4 v5
183205
-> if coe v4
@@ -188,15 +210,15 @@ du_decToPCE_148 v0 v1 v2 v3
188210
else coe seq (coe v5) (coe C_ce_100 v0 v2 v3)
189211
_ -> MAlonzo.RTE.mazUnreachableError
190212
-- VerifiedCompilation.Certificate.pceToDec
191-
d_pceToDec_162 ::
213+
d_pceToDec_170 ::
192214
() ->
193215
T_ProofOrCE_86 ->
194216
MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
195-
d_pceToDec_162 ~v0 v1 = du_pceToDec_162 v1
196-
du_pceToDec_162 ::
217+
d_pceToDec_170 ~v0 v1 = du_pceToDec_170 v1
218+
du_pceToDec_170 ::
197219
T_ProofOrCE_86 ->
198220
MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
199-
du_pceToDec_162 v0
221+
du_pceToDec_170 v0
200222
= case coe v0 of
201223
C_proof_92 v1
202224
-> coe
@@ -210,14 +232,14 @@ du_pceToDec_162 v0
210232
(coe MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
211233
_ -> MAlonzo.RTE.mazUnreachableError
212234
-- VerifiedCompilation.Certificate.MatchOrCE
213-
d_MatchOrCE_176 ::
235+
d_MatchOrCE_184 ::
214236
() ->
215237
() ->
216238
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
217239
(AgdaAny -> AgdaAny -> ()) -> ()
218-
d_MatchOrCE_176 = erased
240+
d_MatchOrCE_184 = erased
219241
-- VerifiedCompilation.Certificate.matchOrCE
220-
d_matchOrCE_196 ::
242+
d_matchOrCE_204 ::
221243
() ->
222244
() ->
223245
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
@@ -227,15 +249,15 @@ d_matchOrCE_196 ::
227249
AgdaAny ->
228250
MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
229251
AgdaAny -> AgdaAny -> T_ProofOrCE_86
230-
d_matchOrCE_196 ~v0 ~v1 ~v2 ~v3 v4 v5 v6 v7
231-
= du_matchOrCE_196 v4 v5 v6 v7
232-
du_matchOrCE_196 ::
252+
d_matchOrCE_204 ~v0 ~v1 ~v2 ~v3 v4 v5 v6 v7
253+
= du_matchOrCE_204 v4 v5 v6 v7
254+
du_matchOrCE_204 ::
233255
T_SimplifierTag_4 ->
234256
(AgdaAny ->
235257
AgdaAny ->
236258
MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
237259
AgdaAny -> AgdaAny -> T_ProofOrCE_86
238-
du_matchOrCE_196 v0 v1 v2 v3
260+
du_matchOrCE_204 v0 v1 v2 v3
239261
= let v4 = coe v1 v2 v3 in
240262
coe
241263
(case coe v4 of
@@ -248,21 +270,21 @@ du_matchOrCE_196 v0 v1 v2 v3
248270
else coe seq (coe v6) (coe C_ce_100 v0 v2 v3)
249271
_ -> MAlonzo.RTE.mazUnreachableError)
250272
-- VerifiedCompilation.Certificate.pcePointwise
251-
d_pcePointwise_238 ::
273+
d_pcePointwise_246 ::
252274
() ->
253275
() ->
254276
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
255277
(AgdaAny -> AgdaAny -> ()) ->
256278
T_SimplifierTag_4 ->
257279
(AgdaAny -> AgdaAny -> T_ProofOrCE_86) ->
258280
[AgdaAny] -> [AgdaAny] -> T_ProofOrCE_86
259-
d_pcePointwise_238 ~v0 ~v1 ~v2 ~v3 v4 v5 v6 v7
260-
= du_pcePointwise_238 v4 v5 v6 v7
261-
du_pcePointwise_238 ::
281+
d_pcePointwise_246 ~v0 ~v1 ~v2 ~v3 v4 v5 v6 v7
282+
= du_pcePointwise_246 v4 v5 v6 v7
283+
du_pcePointwise_246 ::
262284
T_SimplifierTag_4 ->
263285
(AgdaAny -> AgdaAny -> T_ProofOrCE_86) ->
264286
[AgdaAny] -> [AgdaAny] -> T_ProofOrCE_86
265-
du_pcePointwise_238 v0 v1 v2 v3
287+
du_pcePointwise_246 v0 v1 v2 v3
266288
= case coe v2 of
267289
[]
268290
-> case coe v3 of
@@ -282,7 +304,7 @@ du_pcePointwise_238 v0 v1 v2 v3
282304
(case coe v8 of
283305
C_proof_92 v9
284306
-> let v10
285-
= coe du_pcePointwise_238 (coe v0) (coe v1) (coe v5) (coe v7) in
307+
= coe du_pcePointwise_246 (coe v0) (coe v1) (coe v5) (coe v7) in
286308
coe
287309
(case coe v10 of
288310
C_proof_92 v11

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

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -581,7 +581,7 @@ d_isCoC'63'_264 v0 v1 v2
581581
v43)
582582
(let v44
583583
= coe
584-
MAlonzo.Code.VerifiedCompilation.Certificate.du_pcePointwise_238
584+
MAlonzo.Code.VerifiedCompilation.Certificate.du_pcePointwise_246
585585
(coe
586586
MAlonzo.Code.VerifiedCompilation.Certificate.C_caseOfCaseT_12)
587587
(coe
@@ -598,7 +598,7 @@ d_isCoC'63'_264 v0 v1 v2
598598
MAlonzo.Code.VerifiedCompilation.Certificate.C_proof_92 v45
599599
-> let v46
600600
= coe
601-
MAlonzo.Code.VerifiedCompilation.Certificate.du_pcePointwise_238
601+
MAlonzo.Code.VerifiedCompilation.Certificate.du_pcePointwise_246
602602
(coe
603603
MAlonzo.Code.VerifiedCompilation.Certificate.C_caseOfCaseT_12)
604604
(coe
@@ -615,7 +615,7 @@ d_isCoC'63'_264 v0 v1 v2
615615
MAlonzo.Code.VerifiedCompilation.Certificate.C_proof_92 v47
616616
-> let v48
617617
= coe
618-
MAlonzo.Code.VerifiedCompilation.Certificate.du_pcePointwise_238
618+
MAlonzo.Code.VerifiedCompilation.Certificate.du_pcePointwise_246
619619
(coe
620620
MAlonzo.Code.VerifiedCompilation.Certificate.C_caseOfCaseT_12)
621621
(coe

0 commit comments

Comments
 (0)