search

zxcalc / quantomatic

Quantomatic is a tool for doing automated graph rewriting.
http://quantomatic.github.io
152 stars 22 forks source link

Bad match exception #152

Closed rossduncan closed 6 years ago

rossduncan commented 7 years ago

Repeatable bug in the latest integration. Matching falls over when using a pretty simple rule, which I'm pretty sure used to work, so I'm not sure what's going on. I have tried this with some simpler synthetic examples and it does work as it's supposed to, just not in this example where I actually need it....

In the attached project open the derivation: NEW/CCZ_Prop6.4/proofs/CCZ_BotherControlsHigh.qderive Then in the rewrite window add the inverse of the rule: NEW/MiscLemmas/unspider_green_pi_map.qrule In the console you will see:

[info] Exception trace for exception - bad_match_exp raised in :serial=1file=matching/bg_match.ML line 195 [info] [info] End of trace

And obviously it doesn't find the required match.

buggy.zip

rossduncan commented 7 years ago

Playing around a bit more, I suspect this is something to do with the fact the my graph has -\pi where the rule expects to see \pi.

rossduncan commented 7 years ago

Confirmed : \pi \neq -\pi is causing the problem here.