Template Instantiation in different file

[Mike Jones]

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?

[Hongwei Xi]

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.

--
You received this message because you are subscribed to the Google Groups "ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.
Visit this group at http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/61458336-3844-4cff-b4a1-9fd5e7e071ca%40googlegroups.com.