Skip to content
This repository has been archived by the owner on Jun 9, 2021. It is now read-only.

Switch Lambda and Pi constructors to use Text instead of String. #119

Merged
merged 3 commits into from
Jan 19, 2021

Conversation

brianhuffman
Copy link
Contributor

We introduce a type synonym LocalName = Text for this purpose.

This is a step toward removing all uses of String in saw-core (#44).

See also #111.

@brianhuffman
Copy link
Contributor Author

This patch will require some small changes to the saw-core-coq and saw-script packages as well.

@brianhuffman brianhuffman linked an issue Jan 18, 2021 that may be closed by this pull request
@brianhuffman
Copy link
Contributor Author

While there are still uses of String in the saw-core API, I believe this PR completely removes String from the term representation. So upon merging I think we can close #44.

Copy link
Contributor

@robdockins robdockins left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Glad to see these kinds of changes coming along. Only question is about pushing Text into the untyped AST as well.

saw-core/src/Verifier/SAW/Typechecker.hs Show resolved Hide resolved
Brian Huffman added 3 commits January 19, 2021 06:31
We introduce a type synonym `LocalName = Text` for this purpose.

This is a step toward removing all uses of `String` in saw-core
(#44).
@brianhuffman brianhuffman merged commit 0aee352 into master Jan 19, 2021
@brianhuffman brianhuffman deleted the text-lambda branch January 19, 2021 14:39
brianhuffman pushed a commit to GaloisInc/saw-core-coq that referenced this pull request Jan 19, 2021
This switched lambda and pi binders in the saw-core AST from
String to Text (introducing a new type synonym LocalName).
brianhuffman pushed a commit to GaloisInc/crucible that referenced this pull request Jan 19, 2021
Some occurrences of `String` in the saw-core term AST have changed
to `Text`.
brianhuffman pushed a commit to GaloisInc/crucible that referenced this pull request Jan 19, 2021
brianhuffman pushed a commit to GaloisInc/saw-script that referenced this pull request Jan 19, 2021
The saw-core term AST has changed some uses of `String` to `Text`.
brianhuffman pushed a commit to GaloisInc/saw-core-coq that referenced this pull request Jan 19, 2021
brianhuffman pushed a commit to GaloisInc/saw-script that referenced this pull request Jan 19, 2021
The saw-core term AST has changed some uses of `String` to `Text`.
brianhuffman pushed a commit to GaloisInc/saw-script that referenced this pull request Jan 20, 2021
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Avoid using type String in saw-core term representation
2 participants