Is it possible to write (proof) functions from datasorts to datasorts? For
example, if we have
datasort tlist =
| tnil
| tcons(t0ype, tlist)
it would be nice to write something equivalent to
tlist_append : (tlist, tlist) -> tlist
tlist_filter: (tlist, (tlist) -> bool) -> tlist
t
Could you show an example of intended use of tlist_append?
On Monday, April 9, 2018 at 1:35:44 AM UTC-4, Andrew Knapp wrote:
>
> Is it possible to write (proof) functions from datasorts to datasorts? For
> example, if we have
>
> datasort tlist =
> | tnil
> | tcons(t0ype
2018-04-09 11:35 GMT+06:00 Andrew Knapp :
> Is it possible to write (proof) functions from datasorts to datasorts? For
> example, if we have
>
> datasort tlist =
> | tnil
> | tcons(t0ype, tlist)
>
> it would be nice to write something equivalent to
>
> tlist_ap
My one example, serialization of nested records from a tlist of
@(string,t0ype), turned out to not need append. Anyhow, that's blocked for
now, since I don't think you can reflect a template-argument string literal
to the value level.
But more generally, a convenient way to write functions betw
I think I understand you mean here.
In ATS3, I plan to have an evaluator for evaluating
compile-time constant expressions. This evaluator
can evaluate an expression like tlist_append(constant1, constant2).
Of course tlist_append needs to be defined at the sort level first.
On Mon, Apr 9, 2018 at
