Skip to content
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 type constructors strict #1224

Closed
robdockins opened this issue May 27, 2015 · 1 comment
Closed

Make type constructors strict #1224

robdockins opened this issue May 27, 2015 · 1 comment
Labels
subsystem: saw-core Issues related to the saw-core representation or the saw-core subsystem

Comments

@robdockins
Copy link
Contributor

I don't recall the context for this action item, but probably it has to do with squashing space leaks.

brianhuffman referenced this issue in GaloisInc/saw-core Jul 23, 2020
* Add SMT Array primitives.

* Use panic instead of fail.
brianhuffman referenced this issue in GaloisInc/saw-core Aug 6, 2020
Remove uses of `fail` and use `panic` or throw exceptions instead
@brianhuffman brianhuffman transferred this issue from GaloisInc/saw-core Apr 27, 2021
@brianhuffman brianhuffman added the subsystem: saw-core Issues related to the saw-core representation or the saw-core subsystem label Apr 27, 2021
@brianhuffman
Copy link
Contributor

The various type constructors are interpreted as strict in the saw-core simulator backends, and have been for some time. We can see this in the definition of the TValue type, where the arguments for vectors, arrays, pairs, and records are themselves fully-evaluated TValues rather than thunks.

data TValue l
= VVecType !Natural !(TValue l)
| VBoolType
| VIntType
| VIntModType !Natural
| VArrayType !(TValue l) !(TValue l)
| VPiType !(TValue l) !(Thunk l -> EvalM l (TValue l))
| VUnitType
| VPairType !(TValue l) !(TValue l)
| VDataType !Ident ![Value l]
| VRecordType ![(FieldName, TValue l)]
| VSort !Sort

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
subsystem: saw-core Issues related to the saw-core representation or the saw-core subsystem
Projects
None yet
Development

No branches or pull requests

2 participants