Update saw-core submodule to fix addsimp crash.
#965
Conversation
brianhuffman
force-pushed
the
issue319
branch
from
a9f4656 to
51a6c3c
Compare
| addsimp :: Theorem -> Simpset -> TopLevel Simpset | ||
| addsimp (Theorem (Prop t) _stats) ss = | ||
| case ruleOfProp t of | ||
| Nothing -> fail "addsimp: theorem not an equation" |
There was a problem hiding this comment.
I'm not entirely settled on the right answer here, but I've been using throwTopLevel in some code recently when working in the TopLevel monad. It doesn't hugely matter, because fail calls throwTopLevel in this case, but I do slightly like the idea of avoiding having calls to fail in the codebase, even if we know they're well-behaved.
There was a problem hiding this comment.
I totally agree that fail is not the way to go in the long term. However there are already lots of other TopLevel primitives that use fail in their implementations right now, so I just used fail for consistency. I was thinking that we could remove all the uses of fail in the TopLevel monad in a separate PR.
There was a problem hiding this comment.
Yeah, I think that makes sense. The same question will come up shortly when I merge the external ABC interaction branch. I did modify some code to use throwTopLevel, but there's a bunch more refactoring to do.
There was a problem hiding this comment.
I just opened #966, which I imagine would be reasonable to address in a single PR.
This patch includes PR GaloisInc/saw-core#112, which implements error handling using the Maybe monad for the creation of rewrite rules from equational theorems. Fixes #319.
brianhuffman
force-pushed
the
issue319
branch
from
51a6c3c to
c2e9888
Compare
This patch includes PR GaloisInc/saw-core#112, which
implements error handling using the Maybe monad for
the creation of rewrite rules from equational theorems.
Fixes #319.