Add casing on builtins to the metatheory - #7895
Conversation
kwxm
left a comment
kwxm
left a comment
There was a problem hiding this comment.
Looks good: I was expecting it to be a lot more complicated.
| runUplcEvalTests | ||
| (agdaEvalUplcProg WithCosting) | ||
| (flip elem failingEvaluationTests) | ||
| (const False) -- no evaluation tests are expected to fail |
There was a problem hiding this comment.
I'd suggest leaving it as it is here but having failingEvaluationTests = []. If we later add more conformance tests that the Agda code can't handle that would make it easier to turn them off until we update the Agda.
5027289 to
3c2ff74
Compare
| caseCon s ρ bool true (_ ∷ t ∷ []) = s ; ρ ▻ t | ||
| caseCon s ρ integer (ℤ.pos n) ts = maybe (s ; ρ ▻_) ◆ (lookup? n ts) | ||
| caseCon s ρ (list ty) (x ∷ xs) (t ∷ []) = pushValueFrames s ((ε , V-con ty x) , V-con (list ty) xs) ; ρ ▻ t | ||
| caseCon s ρ (list ty) (x ∷ xs) (t ∷ _ ∷ []) = pushValueFrames s ((ε , V-con ty x) , V-con (list ty) xs) ; ρ ▻ t |
There was a problem hiding this comment.
It might be more readable to not use pushValueFrames in these cases, since we can construct the new stack directly:
caseCon s ρ (list ty) (x ∷ xs) (t ∷ []) =
((s , -·v (V-con (list ty) xs)) , -·v (V-con ty x)) ; ρ ▻ t
I find pushValueFrames particularly confusing because it reverses its second stack, e.g.
pushValueFrames ((ε , a) , b) ((ε , c) , d) = (((((ε , a) , b) , -·v d) , -·v c)
so the direct style makes it obvious what the order in the new stack is.
(it would be useful to have an infixl for , to avoid all those parentheses).
|
Nice how this change was only a few lines! |
3 participants
Fixes https://github.com/IntersectMBO/plutus-private/issues/2331, since the only thing that needs to be done for
BuiltinBoolis to support casing on it.