au-ts / cogent

Cogent Project
https://trustworthy.systems/projects/TS/cogent.pml
Other
158 stars 26 forks source link

Error message for Integer type mismatch #41

Open zilinc opened 7 years ago

zilinc commented 7 years ago

Now it says something like:

Mismatch between
   U16
and
   U32
   from constraint U16 :< U32
   when checking that the expression at ("fail_large-code.cogent" (line 244, column 80))
      const_ext2Magic
   has type
      U32

Can be better.

liamoc commented 7 years ago

How can it be improved specifically?

zilinc commented 7 years ago

Suggest using upcast maybe? The constraint U16 :< U32 is actually satisfiable.

liamoc commented 7 years ago

Ah, if you use upcast, right. OK, I can add that.

zilinc commented 7 years ago

Oh btw, we still have functions like u16_to_u32 etc...in ext2 and bilbyfs; should use upcast instead...

zilinc commented 7 years ago

Ummm. let a : U32 = 1 doesn't upcast.

liamoc commented 7 years ago

It shouldn't... it should infer that 1 : U32.

zilinc commented 7 years ago

interestingly if I put 0 to a U32 field in a record, it seems ok

liamoc commented 7 years ago

The type of a numeric literal is inferred from context.. so of course that would work??

zilinc commented 7 years ago

Ah, I might have misunderstood you. Should let a : U32 = 1 typecheck?

liamoc commented 7 years ago

Yes.

zilinc commented 7 years ago

I see. upcast is only for variables (and constants).

liamoc commented 7 years ago

Yes, the literals are no longer given the smallest integer type possible. They are now given whatever integer type is inferred from context (so long as it's big enough to fit the literal).