New approach to rewriting rules #899
Conversation
| private def safeBind(key: String, value: ArenaCell): RewritingComputation[Unit] = modify { s => | ||
| s.copy(binding = Binding(s.binding.toMap + (key -> value))) | ||
| } |
There was a problem hiding this comment.
I wonder if the body of this method might be situated as a method on the RewritingState object like
def bind(key: String, value: ArenaCell): RewritingStateor perhaps inlined. As is, seems like this method is "thin" and cases cases needless redirection when reading the code. I think I feel the same about the other safe helper methods. Perhaps this is just a matter of taste.
There was a problem hiding this comment.
Fair enough, the idea here was mostly to demonstrate the difference (and the relative ease of lifting to a "computation with possible exceptions"), but I agree that the "safe" methods don't add much.
tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rewriter2/NegationRule.scala
Show resolved
Hide resolved
shonfeder
changed the title
There was a problem hiding this comment.
This all looks good to me, with just a few minor change suggestion. I wonder if you should get input from Rodrigo or Igor before starting to migrate over the other rewriting stuff?
My principle question on this is what is the plan for integration? Do we have work scheduled to start porting over the rewriter into this new approach?
|
|
||
| type RewritingComputation[T] = State[RewritingState, T] | ||
|
|
||
| type StateCompWithExceptions[T] = EitherT[Exception, RewritingComputation, T] |
There was a problem hiding this comment.
How about something like this:
| type StateCompWithExceptions[T] = EitherT[Exception, RewritingComputation, T] | |
| type RewritingComputationExn[T] = EitherT[Exception, RewritingComputation, T] |
Otherwise its not clear from the name that this pertains to the RewritingComputation or that Comp is short for Computation rather than Comparison.
| // Shorthand for State[SymbStateInternal, T] { fn } | ||
| def cmp[T](fn: RewritingState => (RewritingState, T)): RewritingComputation[T] = | ||
| State[RewritingState, T] { fn } |
There was a problem hiding this comment.
If cmp is short for Computation than maybe use Comp since that's already appearing in the StateComptWithException type alias?
| } | ||
| } | ||
|
|
||
| // Shorthand for State[SymbStateInternal, T] { fn } |
There was a problem hiding this comment.
| // Shorthand for State[SymbStateInternal, T] { fn } | |
| // Shorthand for State[RewritingState, T] { fn } |
|
|
||
| /** | ||
| * A rule in the new rewriting system. It can be tested, or applied. In the latter case, it either returns | ||
| * a TlaEx (rewritten expression) or throws a RewritingException (represented by computation) |
There was a problem hiding this comment.
I don't understand this part: throws a RewritingException (represented by computation).
make fmt-fix(or had formatting run automatically on all files edited)Documentation added for any new functionalityEntry added to UNRELEASED.md for any new functionalityThis PR outlines a proof-of-concept alternative implementation of rewriting rules, using
scalaz.State. It should facilitate discussion regarding the new approach to rewriting, and is not intended to be integrated (in its current form) in the near future.