andrew-johnson-4 / lambda-mountain

Compiler Backend for LSTS (Typed Macro Assembler)
https://andrew-johnson-4.github.io/lambda-mountain/
MIT License
20 stars 1 forks source link

Auto Coerce for slice indexes with Quick Prop #996

Closed andrew-johnson-4 closed 4 hours ago

andrew-johnson-4 commented 4 hours ago

This is a modelling problem for quick prop, how can we do this.

[:] : (x[], I64,I64) -> x[];
as : U64 -> I64;

"abc"[1:2]

What annotations or quick props need to be added to make this happen? Inferring I64 for all U64 would cause big problems. What is the right tradeoff between localization vs generalization of coercion.

andrew-johnson-4 commented 4 hours ago

I am sort of feeling like puns are best?

defines casts for
[:] : (x[], U64,U64) -> x[];
[:] : (x[], U64,I64) -> x[];
[:] : (x[], I64,U64) -> x[];
andrew-johnson-4 commented 4 hours ago

Connecting calls to casts in any general way is going to cause a lot of bugs. This is "too smart".