PMVerr

[Mike Jones]

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.

[Hongwei Xi]

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.

--
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.

[Barry Schwartz]

Hongwei Xi <gmh...@gmail.com> skribis:

> 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.

The last time I had that, I had to make some functions templates that
probably should have been templates, anyway.

[Mike Jones]

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} .<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?

[Hongwei Xi]

Yes, this one looks rather mysterious :)

You can just do:

implement set_n{n0}(count) = ...

--
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.

[Mike Jones]

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)) ;

[Hongwei Xi]

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  + 1

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/9a7d9617-1edc-4c15-aa38-f024dadfd6fb%40googlegroups.com.

[Mike Jones]

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?

[Hongwei Xi]

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)

end

--

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.

[Mike Jones]

I knew there was secret sauce!