Is it possible to put a template instantiation in its own .dats file?
For example:
numbers.sats:
fun{} n7 (x: uint8): natLte(127)
numbers.dats:
implement{} n7 (x) = $UN.cast{natLte(127)}(x land u8(0x7F))
application.dats:
val n = n7(10)
The compiler is giving an error unless I put the implement in the
application.dats
I assume the answer is no, or it would compile. But I would like to know
the reason it does not work. I’m guessing it has to do with inlining and a
dats file is precompiled stuff. But, if so, one might want to put it in the
sats file, but implementations won’t compile. So is there some way to put
it in its own file such that application code can reference it so it does
not have to be declared in every application file that uses it?
You just need the following line in application.dats
staload “numbers.dats”
There is really no need for number.sats. Just do
extern
fun{} n7 (…): …
implement{} n7(…) = …
SATS files are just special kind of DATS files, and they are not really
needed
in practice.On Wed, Oct 28, 2015 at 10:03 AM, Mike Jones proc...@gmail.com wrote:
Is it possible to put a template instantiation in its own .dats file?
For example:
numbers.sats:
fun{} n7 (x: uint8): natLte(127)
numbers.dats:
implement{} n7 (x) = $UN.cast{natLte(127)}(x land u8(0x7F))
application.dats:
val n = n7(10)
The compiler is giving an error unless I put the implement in the
application.dats
I assume the answer is no, or it would compile. But I would like to know
the reason it does not work. I’m guessing it has to do with inlining and a
dats file is precompiled stuff. But, if so, one might want to put it in the
sats file, but implementations won’t compile. So is there some way to put
it in its own file such that application code can reference it so it does
not have to be declared in every application file that uses it?