Support for [reassume]

[gmhwxi]

I have just finished adding support for [reassume].

Basically, [reassume] is used to make the implementation of an abstract type available in
another scope.

Here is a running example:

https://github.com/githwxi/ATS-Postiats/blob/master/doc/EXAMPLE/TESTATS/reassume.dats

In the following code, the implementation of int2_t0ype is made available
in the body of the function int2_add:

fun

int2_add

(

xy: int2

) : int =

xy.0 + xy.1 where

{

reassume int2_t0ype // making the implementation of int2_t0ype available

}

The feature of [reassume] comes especially handy when one wants to re-implement
function templates involving abstract types.

All the changes have been uploaded to the GitHub repo for ATS2. They will go into the
next release of ATS2 (ATS2-0.3.3).

[Yannick Duchêne]

Le mardi 28 février 2017 05:49:46 UTC+1, gmhwxi a écrit :

I have just finished adding support for [reassume].

Basically, [reassume] is used to make the implementation of an abstract type available in
another scope.

[…]

I tried this:

        abst@ype file

        local

           (* Scope #1 *)

           absimpl file = int

        in

        end

        local

           (* Scope #2 *)

           absreimpl file

           fn is_stdout(f:file): bool = (f = 1)

        in

        end

 

Scope #2 can see the implementation which was associated in scope #1. It seems to be the intent, but it still looks a bit strange. So it seems assume/absimpl works on the abstract definition like if it was a side‑effect.

[Hongwei Xi]

Yes, this is intended.

In theorem-proving, this is often referred to as selected use of definitions.

--
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-users+unsubscribe@googlegroups.com.
To post to this group, send email to ats-lang-users@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/2fa6f63a-ada2-4aae-b2df-737be6905944%40googlegroups.com.