Agda decision tracing #6957
Agda decision tracing #6957
Conversation
|
At this moment this "works" in the sense that it produces counter examples, but it highlights that some of our decision procedures return "no" so it shouldn't be merged until we can decide which is wrong: the Agda relations or the compiler. |
There was a problem hiding this comment.
What I'm not convinced about is the fact that we're not constructing the negative proofs anymore. Since we're in an intuitionistic setting here, if we don't have evidence for the "false" case, we can't say that it is really "false", right? I mean, even from a practical perspective, Agda will definitely complain if someone ever needs to use the negative result in a proof.
| isFD : {X : Set}{{_ : DecEq X}} → {ast ast' : X ⊢} → UFD.ForceDelay ast ast' → Transformation SimplifierTag.forceDelayT ast ast' | ||
| isFlD : {X : Set}{{_ : DecEq X}} → {ast ast' : X ⊢} → UFlD.FloatDelay ast ast' → Transformation SimplifierTag.floatDelayT ast ast' | ||
| isCSE : {X : Set}{{_ : DecEq X}} → {ast ast' : X ⊢} → UCSE.UntypedCSE ast ast' → Transformation SimplifierTag.cseT ast ast' | ||
| inlineNotImplemented : {X : Set}{{_ : DecEq X}} → {ast ast' : X ⊢} → Transformation SimplifierTag.inlineT ast ast' |
There was a problem hiding this comment.
I think you removed the comment here accidentally
|
|
||
| runCertifier : List (SimplifierTag × Untyped × Untyped) → Maybe Proof | ||
| runCertifier : (t : List (SimplifierTag × Untyped × Untyped)) → Maybe Cert |
There was a problem hiding this comment.
Why do you need to bind t here?
| ## Semantic Equivalence | ||
|
|
||
| ``` | ||
| open import Untyped.CEK using (stepper; step) | ||
| open import Builtin using (Builtin; addInteger; subtractInteger) | ||
|
|
||
| ex1 : ⊥ ⊢ | ||
| ex1 = (((ƛ (ƛ (((builtin subtractInteger) · (` nothing)) · (` (just nothing)))))) · (con-integer 2)) · (con-integer 3) --- \× . \y . x - y ==> 2 - 3 | ||
|
|
||
| ex2 : ⊥ ⊢ | ||
| ex2 = (((ƛ (ƛ (((builtin subtractInteger) · (` (just nothing))) · (` nothing))))) · (con-integer 3)) · (con-integer 2) --- \x . \y . y - x ==> 2 - 3 | ||
|
|
||
| ``` |
There was a problem hiding this comment.
I guess you didn't want to add this to this PR?
There was a problem hiding this comment.
I did but I had weird merge conflicts. I thought I solved them sensibly but maybe not here! :)
There was a problem hiding this comment.
Oh, I missread that - no, this shouldn't be here!
| data ProofOrCE (P : Set 𝓁) : Set (suc 𝓁) where | ||
| proof : P → ProofOrCE P | ||
| ce : {X X' : Set} → SimplifierTag → X → X' → ProofOrCE P |
There was a problem hiding this comment.
Are we 100% certain that we won't want the proof of the negation?
There was a problem hiding this comment.
The negation isn't used anywhere, we only look at the no response. These Counter Examples should at least be vaguely useful - although I'm not sure they are currently as minimal as they could be.
There was a problem hiding this comment.
Copying my Slack comment verbatim.
The whole approach to counterexamples doesn't make sense to me. You're just returning a small part of the AST, how is that a counterexample? It's at best a small bit of debugging info. Optimizations are inherently non-local, how is it useful to know that, say, a single variable is different to another variable after a certain pass? It's a single discrepancy within two potentially wildly different ASTs, it's not even necessarily representative of what went wrong, might be just a by-product.
The right approach is to return both the ASTs and to shrink the original one while the mismatch persists (i.e. running the certifier each time) until you've got an actual minimal counterexample.
But I'm happy to be proven wrong. Could you show some of the counterexamples that you get and interpret them meaningfully?
|
|
||
| data ProofOrCE (P : Set 𝓁) : Set (suc 𝓁) where | ||
| proof : (p : P) → ProofOrCE P | ||
| ce : (¬p : ¬ P) → {X X' : Set} → SimplifierTag → X → X' → ProofOrCE P |
There was a problem hiding this comment.
Why are X and X' arbitrary types? Not that I mind, just wanna know.
There was a problem hiding this comment.
Precisely because they are sub-trees so might be completely different scope from the trees - and from each other, if the optimisation does something really weird. Making them just different scopes didn't work for ... reasons (There was something very weird with Universe Levels that happened when I tried that?)
Add Counter Examples to the return type of the certifier, rather than the "negative proofs".
Ideally, this will produce "minimal" counter examples, returning two ASTs that are the smallest sub-trees of the program which exhibit the problem.