At various times we have talked about introducing literal quantifiers
into BitC. I am now fairly convinced that they should be introduced.
A literal quantifier looks something like:
(forall (intlit:int32)
(define (proc i:intlit) ...))
with the meaning that the actual parameter passed to "i" must be an
integer literal of type int32.
Until today, I had not noticed that literal quantification is a very
specialized form of match type. Consider:
(forall (intlit:int32)
(define (proc i: intlit
array (by-ref (array intlit 'a))) ...)
which captures the notion of type-safe by-reference array passing with a
separately passed index. This procedure does not need to be
polyinstantiated.
If the sole consideration was "what is good for BitC", I wouldn't really
care about this. It does let us implement ARRAY-LENGTH as a non-builtin
procedure, but that isn't really enough to justify introducing it.
What this construct *does* do is increase the amount of C code that has
a direct translation to BitC, because it will let us deal with many
cases of C's implicit by-pointer array passing. Right now we have to do
those with by-ref, and if multiple distinct array types get passed to
the receiver we end up with that procedure polyinstantiated.
What other cases, if any, would be assisted by literal quantification of
this form? Does it give us any beginning of a way to express range
types?
shap
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
