Closed Kmeakin closed 1 year ago
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 Prim
s. 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
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
Reduce some duplication in
core::Prim
by adding fields determining a prim's int/float type and endianness where necessaryeg
FormatU64Be
becomesFormatInt(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.