PMVerr

Google Group
1

I put a function in a dats file, then did an staload of it in a main.dats,
but I can’t link due to a missing definition of PMVerr(string)

PMVerr seems to be part of pats_ccomp.sats

Is there some standard way to hook this? staload fails.

2

I knew there was secret sauce!

3

I see.

But if foo has an quantifier and an inner loop has a quantifier that
references the one in foo, so far, I have not been able to separate the
fun/impl.

Is there any way to solve that problem?

4

PMVerr indicates that some kind of error occurred at compile-time.
One needs to take a look at the source code to figure what went wrong.On Wed, Oct 28, 2015 at 1:10 PM, Mike Jones proc...@gmail.com wrote:

I put a function in a dats file, then did an staload of it in a main.dats,
but I can’t link due to a missing definition of PMVerr(string)

PMVerr seems to be part of pats_ccomp.sats

Is there some standard way to hook this? staload fails.

–
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/bbaebb86-8424-429c-a4c5-45ed9f446155%40googlegroups.com
https://groups.google.com/d/msgid/ats-lang-users/bbaebb86-8424-429c-a4c5-45ed9f446155%40googlegroups.com?utm_medium=email&utm_source=footer
.

5

extern
fun foo{n:nat}(x: int(n)): int(n+1)

implement foo{n}(x) = let
fun add1(x: int(n)): int(n+1) = x + 1
in
add1(x)
endOn Wed, Oct 28, 2015 at 6:58 PM, Mike Jones proc...@gmail.com wrote:

I see.

But if foo has an quantifier and an inner loop has a quantifier that
references the one in foo, so far, I have not been able to separate the
fun/impl.

Is there any way to solve that problem?

–
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/8d632d28-d9e2-4d62-939b-d97f0edd9cb9%40googlegroups.com
https://groups.google.com/d/msgid/ats-lang-users/8d632d28-d9e2-4d62-939b-d97f0edd9cb9%40googlegroups.com?utm_medium=email&utm_source=footer
.

6

In this case:

in frames.dats:

fun set_n {n0: nat | n0 >= 3 && n0 <= 127} (count: int(n0)): void = let

in main.dats

staload “frames.dats”

val v = set_n(…)

gives an error the v =

There is no definition in a .sats file

I suspect I need an extern fun + implement like this:

extern fun set_n {n0: nat | n0 >= 3 && n0 <= 127} (count: int(n0)): void
implement set_n (count) = let
val () = !packetOutCount := u8(count) // Not setting multi-frame bit
val () = !packetOutHeader := (!packetInHeader land u8(0xFE)) // No error
fun loop {n: nat | n0 - 1 >= n} .. (cnt: int(n), p: uint8): uint8 =
if cnt > 0
then loop(cnt - 1, pec_add(p, packetOut[count - cnt - 1]))
else p
in packetOut[count - 1] := loop(count - 1, u8(0)) end

but this won’t compile because n0 is outside the implementation.

Is there a proper way to specify a function that is staloaded from a dats?
Is there a way to split the fun from impl between two files and still
manage the universal constraint that is referenced by the embedded loop?

7

Say you do:

fun foo(x:int): int = x + 1

Then foo is a static function (in the sense of C); it cannot be used
outside the file where it is defined.

To use it outside the file, do

extern fun foo(x:int): int
implement foo(x) = x + 1On Wed, Oct 28, 2015 at 5:51 PM, Mike Jones proc...@gmail.com wrote:

Does the error below offer a clue to the problem?

Note: I get these errors any time I put a function in a dats and then
staload the dats file. Meaning, fun foo():void, etc.

When I split a function between sats/dats, I don’t have any errors. I
performed the experiment with the same sats/dats, so I am assuming no
general compile problems as I can mix working and un-working in the same
files.

/*
emit_instr: loc0 = /home/mike/linti/linti-avr/DATS/main.dats:
11298(line=250, offs=53) – 11314(line=250, offs=69)
*/
ATSINSmove_void(tmpret231,
ATSfunclo_fun(PMVerr(“/home/mike/linti/linti-avr/DATS/main.dats:
11298(line=250, offs=53) – 11303(line=250, offs=58)”),
(atstkind_t0ype(atstype_int)), atsvoid_t0ype)(tmp253)) ;

On Wednesday, October 28, 2015 at 11:37:09 AM UTC-6, gmhwxi wrote:

Yes, this one looks rather mysterious :slight_smile:

You can just do:

implement set_n{n0}(count) = …

On Wed, Oct 28, 2015 at 1:34 PM, Mike Jones pro...@gmail.com wrote:

In this case:

in frames.dats:

fun set_n {n0: nat | n0 >= 3 && n0 <= 127} (count: int(n0)): void = let

in main.dats

staload “frames.dats”

val v = set_n(…)

gives an error the v =

There is no definition in a .sats file

I suspect I need an extern fun + implement like this:

extern fun set_n {n0: nat | n0 >= 3 && n0 <= 127} (count: int(n0)):
void
implement set_n (count) = let
val () = !packetOutCount := u8(count) // Not setting multi-frame bit
val () = !packetOutHeader := (!packetInHeader land u8(0xFE)) // No
error
fun loop {n: nat | n0 - 1 >= n} .. (cnt: int(n), p: uint8): uint8

  if cnt > 0
  then loop(cnt - 1, pec_add(p, packetOut[count - cnt - 1]))
  else p

in packetOut[count - 1] := loop(count - 1, u8(0)) end

but this won’t compile because n0 is outside the implementation.

Is there a proper way to specify a function that is staloaded from a
dats?
Is there a way to split the fun from impl between two files and still
manage the universal constraint that is referenced by the embedded loop?

–
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...@googlegroups.com.
To post to this group, send email to ats-l...@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/3cab69a0-365c-4555-bd7a-e23b3e973ebb%40googlegroups.com
https://groups.google.com/d/msgid/ats-lang-users/3cab69a0-365c-4555-bd7a-e23b3e973ebb%40googlegroups.com?utm_medium=email&utm_source=footer
.

–
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/9a7d9617-1edc-4c15-aa38-f024dadfd6fb%40googlegroups.com
https://groups.google.com/d/msgid/ats-lang-users/9a7d9617-1edc-4c15-aa38-f024dadfd6fb%40googlegroups.com?utm_medium=email&utm_source=footer
.

8

Yes, this one looks rather mysterious :slight_smile:

You can just do:

implement set_n{n0}(count) = …On Wed, Oct 28, 2015 at 1:34 PM, Mike Jones proc...@gmail.com wrote:

In this case:

in frames.dats:

fun set_n {n0: nat | n0 >= 3 && n0 <= 127} (count: int(n0)): void = let

in main.dats

staload “frames.dats”

val v = set_n(…)

gives an error the v =

There is no definition in a .sats file

I suspect I need an extern fun + implement like this:

extern fun set_n {n0: nat | n0 >= 3 && n0 <= 127} (count: int(n0)): void
implement set_n (count) = let
val () = !packetOutCount := u8(count) // Not setting multi-frame bit
val () = !packetOutHeader := (!packetInHeader land u8(0xFE)) // No
error
fun loop {n: nat | n0 - 1 >= n} .. (cnt: int(n), p: uint8): uint8 =
if cnt > 0
then loop(cnt - 1, pec_add(p, packetOut[count - cnt - 1]))
else p
in packetOut[count - 1] := loop(count - 1, u8(0)) end

but this won’t compile because n0 is outside the implementation.

Is there a proper way to specify a function that is staloaded from a dats?
Is there a way to split the fun from impl between two files and still
manage the universal constraint that is referenced by the embedded loop?

–
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/3cab69a0-365c-4555-bd7a-e23b3e973ebb%40googlegroups.com
https://groups.google.com/d/msgid/ats-lang-users/3cab69a0-365c-4555-bd7a-e23b3e973ebb%40googlegroups.com?utm_medium=email&utm_source=footer
.

9

Does the error below offer a clue to the problem?

Note: I get these errors any time I put a function in a dats and then
staload the dats file. Meaning, fun foo():void, etc.

When I split a function between sats/dats, I don’t have any errors. I
performed the experiment with the same sats/dats, so I am assuming no
general compile problems as I can mix working and un-working in the same
files.

/*
emit_instr: loc0 = /home/mike/linti/linti-avr/DATS/main.dats:
11298(line=250, offs=53) – 11314(line=250, offs=69)
*/
ATSINSmove_void(tmpret231,
ATSfunclo_fun(PMVerr(“/home/mike/linti/linti-avr/DATS/main.dats:
11298(line=250, offs=53) – 11303(line=250, offs=58)”),
(atstkind_t0ype(atstype_int)), atsvoid_t0ype)(tmp253)) ;On Wednesday, October 28, 2015 at 11:37:09 AM UTC-6, gmhwxi wrote:

Yes, this one looks rather mysterious :slight_smile:

You can just do:

implement set_n{n0}(count) = …

On Wed, Oct 28, 2015 at 1:34 PM, Mike Jones <pro...@gmail.com <javascript:>> wrote:

In this case:

in frames.dats:

fun set_n {n0: nat | n0 >= 3 && n0 <= 127} (count: int(n0)): void = let

in main.dats

staload “frames.dats”

val v = set_n(…)

gives an error the v =

There is no definition in a .sats file

I suspect I need an extern fun + implement like this:

extern fun set_n {n0: nat | n0 >= 3 && n0 <= 127} (count: int(n0)): void
implement set_n (count) = let
val () = !packetOutCount := u8(count) // Not setting multi-frame bit
val () = !packetOutHeader := (!packetInHeader land u8(0xFE)) // No
error
fun loop {n: nat | n0 - 1 >= n} .. (cnt: int(n), p: uint8): uint8 =
if cnt > 0
then loop(cnt - 1, pec_add(p, packetOut[count - cnt - 1]))
else p
in packetOut[count - 1] := loop(count - 1, u8(0)) end

but this won’t compile because n0 is outside the implementation.

Is there a proper way to specify a function that is staloaded from a dats?
Is there a way to split the fun from impl between two files and still
manage the universal constraint that is referenced by the embedded loop?

–
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...@googlegroups.com <javascript:>.
To post to this group, send email to ats-l...@googlegroups.com
<javascript:>.
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/3cab69a0-365c-4555-bd7a-e23b3e973ebb%40googlegroups.com
https://groups.google.com/d/msgid/ats-lang-users/3cab69a0-365c-4555-bd7a-e23b3e973ebb%40googlegroups.com?utm_medium=email&utm_source=footer
.