cogent icon indicating copy to clipboard operation
cogent copied to clipboard

a constant must indeed be a constant

Open zilinc opened this issue 7 years ago • 4 comments

This is not enforced by the compiler. It causes troubles to the back-end.

zilinc avatar Jun 05 '18 02:06 zilinc

sort of a duplicate of #49.

zilinc avatar Jun 05 '18 02:06 zilinc

Should we not just evaluate the constant? I suppose that gets hard with C in the mix

liamoc avatar Jun 05 '18 06:06 liamoc

We don't evaluate them. We instead substitute the variable with the RHS of =. So when they're mistakenly not constants, we don't handle it properly in the code generator.

zilinc avatar Jun 05 '18 06:06 zilinc

I also think this could be potentially problematic if we had a proper refinement type system.

a : Int
a = 5

should probably be compiled to

a : {a : Int | a = 5}
a = _

If that's not a constant, I don't know how much sense it makes (esp. if we want make the SMT solver decidable)

zilinc avatar Jun 05 '18 06:06 zilinc