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

Exclusive enumeration #1085

Merged
merged 4 commits into from
Mar 3, 2021
Merged

Exclusive enumeration #1085

merged 4 commits into from
Mar 3, 2021

Conversation

robdockins
Copy link
Contributor

Add support for enumerations with exclusive upper bounds. This allows us to capture two different boundary conditions: empty sequences and infinite sequences.

Cryptol> :t [ 0:Integer .. <0 ]
[0 : Integer .. < 0] : [0]Integer
Cryptol> :t [ 0:Integer .. <inf ]
[0 : Integer .. < inf] : [inf]Integer

As a result, we can redefine generate in a way that allows LHS indexing to likewise produce infinite and empty sequences

generate : {n, a, ix} (Integral ix, LiteralLessThan n ix) => (ix -> a) -> [n]a
generate f = [ f i | i <- [0 .. <n] ]

Fixes #1063
Fixes #973

There are still some questions we need to answer regarding #1062.

@weaversa
Copy link
Collaborator

@robdockins #973 contains a good suggestion by you about setting the stride. Are you planning to tackle that here as well?

@robdockins
Copy link
Contributor Author

I haven't thought about it much since I made that suggestion. Is that something you think people would find useful?

@weaversa
Copy link
Collaborator

Yes, and I didn't want to comment to disappear -- I see this PR is labeled "Fixes #973". Would you be willing to capture your idea in a new issue?

@robdockins
Copy link
Contributor Author

CF #1087

This allows us to express enumerations with exclusive upper bounds.
In contrast with the `Literal` constraint, `LiteralLessThan n a`
express that `a` contains all the literals strictly less than `n`,
and explicitly allows `n` to be `inf` for unbounded types like
`Integer` and `Rational`.

It is possible to define `Literal n a` as
`(fin n, LiteralLessThan (n+1) a)` instead of leaving it primitve.
However, this makes infered types and error messages worse, IMO.
As it stands, the typechecker has no real knowledge of the connection
between `Literal` and `LiteralLessThan`.
`[ x   .. < y ]` --> ``fromToLessThan`{first=x, bound=y}``
`[ x:t .. < y ]` --> ``fromToLessThan`{first=x, bound=y, a=t}``
@robdockins robdockins force-pushed the exclusive-enumeration branch from c856d49 to eb9d3e9 Compare March 3, 2021 01:25
@robdockins robdockins merged commit 48443b5 into master Mar 3, 2021
brianhuffman pushed a commit to GaloisInc/saw-script that referenced this pull request Apr 7, 2021
…ons.

This includes the following submodule PRs:
- GaloisInc/cryptol#1085 "exclusive-enumeration"
- GaloisInc/saw-core#188 "PLiteralLessThan"
@RyanGlScott RyanGlScott deleted the exclusive-enumeration branch March 22, 2024 14:47
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Make generate and lhs-indexing work for infinite sequences indexed by Integer. Base case for enumerations
3 participants