How to use use option_v and pointer?

[Kiwamu Okabe]

Hi all,

I try to use option_v.

extern fun user_get_super (dev: dev_t): [l:addr]
(option_v(super_block_t@l, l > null) | ptr(l)) = "mac#"
extern fun vfs_ustat_ats (dev: dev_t): Option_vt(@(uint64_t, uint64_t)) = "sta#"

implement vfs_ustat_ats (dev) = r where {
var sbuf: kstatfs_t
val (pfopt | p) = user_get_super(dev)
val r = if (p > null) then let // <= Error occurs here!
prval Some_v (pf) = pfopt
val () = drop_super(pf | p)
in
end else let
prval None_v () = pfopt
in
None_vt()
end
}

However this catches an error...

/home/kiwamu/src/ATS-Postiats/bin/patsopt -o fs/statfs_dats.c -d
metasepi/fs/DATS/statfs.dats
/home/kiwamu/src/linux-bohai-s2/metasepi/fs/DATS/statfs.dats:
1090(line=28, offs=19) -- 1094(line=28, offs=23): error(2): the
dynamic identifier [null] is unrecognized.
patsopt(TRANS2): there are [1] errors in total.
exit(ATS): uncaught exception:
_2home_2kiwamu_2src_2ATS_2dPostiats_2src_2pats_error_2esats__FatalErrorExn(1025)
metasepi/scripts/Makefile.ats:13: recipe for target 'fs/statfs_dats.c' failed

I see this pattern at ATS-Postiats/utils/atsynmark/DATS/pats2xhtml_main.dats:

val [l:addr] (pfopt | p) =
$STDIO.fopen_err (basename, file_mode_w)
// end of [val]
in
//
if p > null then let
prval Some_v (pf) = pfopt
val filp = __cast (pf | p) where {
extern castfn __cast (pf: FILE w @ l | p: ptr l):<> FILEref
} // end of [val]
in
cmdstate_set_outchan (state, OUTCHANptr (filp))
end else let
prval None_v () = pfopt
val () = state.nerror := state.nerror + 1
in
cmdstate_set_outchan (state, OUTCHANref (stderr_ref))
end // end of [if]

How to use dynamic identifier [null]?

Best regards,
--
Kiwamu Okabe at METASEPI DESIGN

[Artyom Shalkhakov]

Hello Kiwamu,

the_null_ptr is the dynamic constant of type ptr null

(I recently tripped over this while porting some ATS1 code to ATS2)

[Kiwamu Okabe]

Hi Artyom,

On Sun, Feb 22, 2015 at 10:05 PM, Artyom Shalkhakov
<artyom.s...@gmail.com> wrote:
> the_null_ptr is the dynamic constant of type ptr null

Thank's! Following code is ready to be compiled:

extern fun vfs_ustat_ats (dev: dev_t): Option_vt(@(uint64_t, uint64_t)) = "sta#"
implement vfs_ustat_ats (dev) = r where {
var sbuf: kstatfs_t
val (pfopt | p) = user_get_super(dev)

val () = if (p > the_null_ptr) then {

prval Some_v (pf) = pfopt
val () = drop_super(pf | p)
}

else {

prval None_v () = pfopt
}

val r = None_vt() (* xxx Not correct *)
}

Thank's for your advice,

[Hongwei Xi]

You can write p > 0 as well. Or use isneqz(p).

--
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/CAEvX6dm4yV9bhL-WNNO30LeMafF2c_hLQLE3FWM5KOAd2NYw-Q%40mail.gmail.com.

[Hongwei Xi]

>>extern fun vfs_ustat_ats (dev: dev_t): Option_vt(@(uint64_t, uint64_t)) = "sta#"

Using option_vt causes memory allocation. Using 'opt' does not:

typedef res = @(uint64_t, uint64_t)
extern fun vfs_ustat_ats (dev: dev_t, res? >> opt(res, b)): #[b:bool] bool(b) = "sta#"

[Kiwamu Okabe]

Hi Hongwei,

On Sun, Feb 22, 2015 at 11:28 PM, Hongwei Xi <gmh...@gmail.com> wrote:
> You can write p > 0 as well. Or use isneqz(p).

Thank's. I think "p > 0" is better than "the_null_ptr" to be easy to remember.

[Kiwamu Okabe]

Hi Hongwei,

On Sun, Feb 22, 2015 at 11:36 PM, Hongwei Xi <gmh...@gmail.com> wrote:
>>>extern fun vfs_ustat_ats (dev: dev_t): Option_vt(@(uint64_t, uint64_t)) =
>>> "sta#"
>
> Using option_vt causes memory allocation. Using 'opt' does not:
>
> typedef res = @(uint64_t, uint64_t)
> extern fun vfs_ustat_ats (dev: dev_t, res? >> opt(res, b)): #[b:bool] bool(b) = "sta#"

I try to use opt at following code.

https://github.com/metasepi/linux-bohai-s2/blob/774767d22125f39b3eb6f1aa3290707029dfa679/metasepi/fs/DATS/statfs.dats#L27

```
extern fun vfs_ustat
(dev: dev_t, sbuf: &kstatfs_t? >> opt (kstatfs_t, i==0)): #[i:int | i
!= 0] int(i) = "mac#"

extern fun syscall_ustat_ats (dev: dev_t, ubuf: ustat_t_p): int = "sta#"
implement syscall_ustat_ats (dev, ubuf) = r where {
fun copy_tmp (sbuf: &kstatfs_t): int = r where {
var tmp: ustat_t
val _ = memset0(addr@tmp, 0, sizeof<ustat_t>)
val () = tmp.f_tfree := $UN.cast(sbuf.f_bfree)
val () = tmp.f_tinode := $UN.cast(sbuf.f_ffree)
val r = if copy_to_user0($UN.cast ubuf, addr@tmp, $UN.cast
sizeof<ustat_t>) != 0
then (~ EFAULT) else 0
}
var sbuf: kstatfs_t
val e = vfs_ustat(new_decode_dev(dev), sbuf)
val r = (if e != 0 then let
prval () = opt_unnone(sbuf)
in
e:int
end else let
prval () = opt_unsome(sbuf)
in
copy_tmp(sbuf)
end):int
}
```

However it cause following compile error:

https://travis-ci.org/metasepi/linux-bohai-s2/builds/52234547#L1937

/home/kiwamu/src/ATS-Postiats/bin/patsopt -o fs/statfs_dats.c -d
metasepi/fs/DATS/statfs.dats
/home/kiwamu/src/linux-bohai-s2/metasepi/fs/DATS/statfs.dats:

1570(line=39, offs=27) -- 1634(line=43, offs=8): error(3): mismatch of
static terms (tyleq):
The actual term is: S2Etop(knd=0; S2Eapp(S2Ecst(g0int_t0ype);
S2Ecst(lint_kind)))
The needed term is: S2Eapp(S2Ecst(g0int_t0ype); S2Ecst(lint_kind))
/home/kiwamu/src/linux-bohai-s2/metasepi/fs/DATS/statfs.dats:
1570(line=39, offs=27) -- 1634(line=43, offs=8): error(3): mismatch of
static terms (tyleq):
--snip--

How to fix it?

Best regards,

[Hongwei Xi]

Try to change

var sbuf: kstatfs_t

into

var sbuf: kstatfs_t?

--
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/CAEvX6d%3DR8Gn4WjbJHA-kYTDsEDbKda2E4z%2BHn9y%2BWH-HKaDxgA%40mail.gmail.com.

[Shea Levy]

On Feb 22, 2015, at 9:36 AM, Hongwei Xi <gmh...@gmail.com> wrote:

>>extern fun vfs_ustat_ats (dev: dev_t): Option_vt(@(uint64_t, uint64_t)) = "sta#"

Using option_vt causes memory allocation. Using 'opt' does not:

typedef res = @(uint64_t, uint64_t)

extern fun vfs_ustat_ats (dev: dev_t, res? >> opt(res, b)): #[b:bool] bool(b) = "sta#”

What does the # before [b:bool] mean here?

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLqXddtp%3DcKiar%3DPXTTHgEp%3DrB4V18vfRLtO5TQYEsonqg%40mail.gmail.com.

[Hongwei Xi]

It means that the scope of [b:bool] contains the b to its left.

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/934B4C61-9870-4534-8FD9-415C5B235CF9%40shealevy.com.

[Kiwamu Okabe]

Hi Hongwei,

On Thu, Feb 26, 2015 at 11:38 PM, Hongwei Xi <gmh...@gmail.com> wrote:
> Try to change
>
> var sbuf: kstatfs_t
>
> into
>
> var sbuf: kstatfs_t?

I got compilable code.

However, I think the compile error doesn't explain "?" missing.

/home/kiwamu/src/ATS-Postiats/bin/patsopt -o fs/statfs_dats.c -d
metasepi/fs/DATS/statfs.dats
/home/kiwamu/src/linux-bohai-s2/metasepi/fs/DATS/statfs.dats:
1570(line=39, offs=27) -- 1634(line=43, offs=8): error(3): mismatch of
static terms (tyleq):
The actual term is: S2Etop(knd=0; S2Eapp(S2Ecst(g0int_t0ype);
S2Ecst(lint_kind)))
The needed term is: S2Eapp(S2Ecst(g0int_t0ype); S2Ecst(lint_kind))
/home/kiwamu/src/linux-bohai-s2/metasepi/fs/DATS/statfs.dats:
1570(line=39, offs=27) -- 1634(line=43, offs=8): error(3): mismatch of
static terms (tyleq):
The actual term is: S2Etop(knd=0; S2Eapp(S2Ecst(g0int_t0ype);
S2Ecst(lint_kind)))
The needed term is: S2Eapp(S2Ecst(g0int_t0ype); S2Ecst(lint_kind))

They point let binding...

var sbuf: kstatfs_t
val e = vfs_ustat(new_decode_dev(dev), sbuf)

val r = (if e != 0 then let // <= Line 39

prval () = opt_unnone(sbuf)
in
e:int
end else let
prval () = opt_unsome(sbuf)
in
copy_tmp(sbuf)
end):int

How do you understand the error?

Thank's,

[gmhwxi]

To me, it does explain :)

Typechecking if-expressions in ATS uses a strategy
explained in the following paper:

http://www.ats-lang.org/Papers.html#Xanadu-lics2000

Basically, each 'var' is given a so-called *master* type.
In your example, the master type for sbuf is kstatfs_t.
When the if-expression is being typechecked, sbuf is
assumed to have the type kstatfs_t at the end of both
then-branch and else-branch. But this is not true in your code.

To put it differently, your code would have leaked a resource
if kstatfs_t were a linear type.