-
-
Notifications
You must be signed in to change notification settings - Fork 40
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Make records as they are work in the arrays encoding #1419
Changes from all commits
5d3f30f
3a7b380
6869af9
c46a828
c0c71b8
dce272d
e181f4d
42ff7a3
e2db7ab
5a2d262
f6c0f06
09d4fc7
58b0e6c
36059fb
195f8a0
93a5942
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -2,7 +2,7 @@ package at.forsyte.apalache.tla.bmcmt.rules | |
|
||
import at.forsyte.apalache.tla.bmcmt.{RewriterException, SymbState, SymbStateRewriter} | ||
import at.forsyte.apalache.tla.bmcmt.caches.IntRangeCache | ||
import at.forsyte.apalache.tla.bmcmt.types.FunT | ||
import at.forsyte.apalache.tla.bmcmt.types.{FunT, RecordT, SeqT, TupleT} | ||
import at.forsyte.apalache.tla.lir.OperEx | ||
import at.forsyte.apalache.tla.lir.oper.TlaFunOper | ||
|
||
|
@@ -21,14 +21,25 @@ class DomainRuleWithArrays(rewriter: SymbStateRewriter, intRangeCache: IntRangeC | |
val funState = rewriter.rewriteUntilDone(state.setRex(funEx)) | ||
val funCell = funState.asCell | ||
|
||
// TODO: consider records, tuples, and sequences in the arrays encoding | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. is this TODO obsolete? There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Not really. It is there as a reminder of what was not touched for when we decide to encode these features differently. |
||
funCell.cellType match { | ||
case RecordT(_) => | ||
val dom = funState.arena.getDom(funCell) | ||
funState.setRex(dom.toNameEx) | ||
|
||
case TupleT(_) => | ||
mkTupleDomain(funState, funCell) | ||
|
||
case SeqT(_) => | ||
mkSeqDomain(funState, funCell) | ||
|
||
case FunT(_, _) => | ||
val dom = funState.arena.getDom(funCell) | ||
funState.setRex(dom.toNameEx) | ||
|
||
case _ => | ||
// TODO: consider records, tuples, and sequences in the arrays encoding | ||
super.apply(state) | ||
throw new RewriterException("DOMAIN x where type(x) = %s is not implemented".format(funCell.cellType), | ||
state.ex) | ||
} | ||
|
||
case _ => | ||
|
This file was deleted.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This is a very old piece of code. Let's replace it with an assertion that both
left.cellType
andright.cellType
areFinSetT(_)
.There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
See #1430.