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

Parameterize prims by their numeric type and endianness #481

Closed
wants to merge 3 commits into from

Conversation

Kmeakin
Copy link
Contributor

@Kmeakin Kmeakin commented Jan 27, 2023

Reduce some duplication in core::Prim by adding fields determining a prim's int/float type and endianness where necessary

eg FormatU64Be becomes FormatInt(IntType::Unsigned(UintType::U64, Endianness::Big))

Allows removing a lot of repeated match arms all over the place. Still not as concise as I would like, but an improvement.

@Kmeakin Kmeakin changed the title Parameterise prims by their numeric type and endianness Parameterize prims by their numeric type and endianness Jan 27, 2023
@brendanzab
Copy link
Member

brendanzab commented Feb 2, 2023

Yeah I have been pondering this and have experimented locally with similar stuff it in the past: but more in the direction of defining stuff directly in the core AST, rather than as Prims. Like FormatType, FormatRepr, etc. Not sure about of adding more data to the prims though… I was more hoping this type would remain a simple prim name? But yeah unsure. Primitives are always rather frustrating :(

Eventually we might want to look at making the numeric types refinements on Int (see #258), which could simplify things?

Curious why F* has specific numeric types when they have access to refinement types: https://github.com/FStarLang/FStar/blob/3ec3078dffa8cb249b2743ef41863cf580f8e65f/src/typechecker/FStar.TypeChecker.TcTerm.fst#L1818-L1826

@Kmeakin
Copy link
Contributor Author

Kmeakin commented Feb 2, 2023

Curious why F* has specific numeric types when they have access to refinement types: https://github.com/FStarLang/FStar/blob/3ec3078dffa8cb249b2743ef41863cf580f8e65f/src/typechecker/FStar.TypeChecker.TcTerm.fst#L1818-L1826

I would guess its so that they can have types that are guaranteed to compile to uint8_t/uint16_t/uint32_t/uint64_t. I wonder how easy/reliable it would be to optimize types like { x : Int | x <= 256 } to U8

@Kmeakin Kmeakin closed this Feb 10, 2023
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.

None yet

2 participants