ATS programing on ChibiOS/RT and Arduino

gmhwxi · May 9, 2014, 2:16pm

First, some minor issues:

you can write 1000u or 1000U for i2u(1000).

Also, I suggest

abst@ype SerialDriver = $extype"SerialDriver"

Then SerialDriver_p can be replaced with cPtr1(SerialDriver) (or
cPtr0(SerialDriver)).On Friday, May 9, 2014 9:53:01 AM UTC-4, Kiwamu Okabe wrote:

Hi all.

Second trying is ATS programing on ChibiOS/RT and Arduino.

GitHub - fpiot/chibios-ats: ATS programing on ChibiOS/RT

ChibiOS/RT is very small RTOS that has good API.

ChibiOS free embedded RTOS - ChibiOS Homepage
http://chibios.sourceforge.net/html/index.html

ATS application source code is found at following.

https://github.com/fpiot/chibios-ats/blob/ats/demos/AVR-ArduinoMega2560-GCC-ats/main.dats#L7

But it has some C language code yet…
I would like to have no more C code!!!

Do you have any idea?

Best regards,

Kiwamu Okabe at METASEPI DESIGN

gmhwxi · May 9, 2014, 4:16pm

I also suggest the following style of sequencing:

val () = do_this (…)
val () = do_that (…)

This style will make it very easy to add proofs into your code.

By the way, people often criticize the syntax of ATS for being verbose.
But in this case, the above style of sequencing is a lot more flexible than
the following very restricted form:

do_this (…); do_that (…);

For instance, we can later add proofs as follows:

val (pf | ()) = do_this (…)
val ((void)) = do_that (pf | …)On Friday, May 9, 2014 10:44:14 AM UTC-4, Kiwamu Okabe wrote:

Hi Hongwei.

On Fri, May 9, 2014 at 11:16 PM, gmhwxi <gmh...@gmail.com <javascript:>> wrote:

you can write 1000u or 1000U for i2u(1000).

Also, I suggest

abst@ype SerialDriver = $extype"SerialDriver"

Then SerialDriver_p can be replaced with cPtr1(SerialDriver) (or
cPtr0(SerialDriver)).

The code is more readable.
I should learn linear type…

Thank’s for your advice.

Kiwamu Okabe at METASEPI DESIGN

gmhwxi · May 10, 2014, 4:01pm

atstype_var is not supposed to be used by the compiler.

I have now introduced a flag as follows to control its size:

//
// HX-2014-05:
// making it not usable!!!
//
#ifndef _ATSTYPE_VAR_SIZE
#define _ATSTYPE_VAR_SIZE 0X10000
#endif // end of [#ifndef]
//
// HX-2014-05:
// for 8-bit or 16-bit march,
// _ATSTYPE_VAR_SIZE can be set to 0x100
//
typedef
struct{char _[_ATSTYPE_VAR_SIZE];} atstype_var[0] ;
//On Sat, May 10, 2014 at 3:23 AM, Kiwamu Okabe kiw...@debian.or.jp wrote:

Hi Hongwei.

BTW.
The ccomp/runtime/pats_ccomp_typedefs.h file has a big array.
// HX: making it not usable!!!
//
typedef
struct{char _[0XFFFF];} atstype_var[0] ;
64KiB is too big for 8-bit or 16-bit microcontroller.

Sometime 32-bit arch also: LPC812M101JDH20 :: NXP

LPC81X-LPC83X | NXP Semiconductors

I have escaped it with dirty hack.

https://github.com/fpiot/chibios-ats/blob/ats/demos/AVR-ArduinoMega2560-GCC-ats/Makefile#L639
pats_ccomp_typedefs.h:
        sed -e 's/_\[0XFFFF\]/_\[0X00FF\]/g' ${PATSHOME}/ccomp/runtime/$@
> $@
Is it needed for ATS language today?

Thank’s,

Kiwamu Okabe at METASEPI DESIGN

–
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.
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/CAEvX6dnEV7rwx9%2BFFFeuNV2zzJ6fkN%2BGeifRP9mv2pUojdoSUA%40mail.gmail.com
.

Brandon_Barker · May 17, 2014, 3:33pm

So I’m probably missing several points here, including how to properly use
proofs and even what is meant by parallel. But I never saw any parallelism
in these concrete examples:

(* ****** ****** )
//
#include
“share/atspre_define.hats”
#include
“share/atspre_staload.hats”
//
( ****** ****** *)

%{^
int do_adding() {
volatile unsigned int i = 1;
while(i >= 0) {
i = i + 1;
}
return -1;
}
%}

extern
fun do_adding():int = “mac#”
// Now with proofs:
dataprop TESTPROP =
| TEST of ()
extern
fun do_adding_usepf(pf: TESTPROP | ):int = “mac#do_adding”
//

implement main0() = let

// val x = do_adding() and y = do_adding()
// same cpu usage as:
// val x = do_adding()

prval apf = TEST()
prval bpf = TEST()

// The cpu usage is the same again
val x = do_adding_usepf(apf | ) and y = do_adding_usepf(bpf | )

in
println!(x)
endOn Friday, May 9, 2014 8:24:52 PM UTC-4, gmhwxi wrote:

In ATS, a pure function can write but it can only write
to the memory it owns. The design in ATS goes like this:

If I want to indicate to the compiler that that do_this and do_that
can be evaluated in parallel, I use the following syntax:

prval (pf1, pf2) = … // [pf1] and [pf2] are separated
val … = do_this (pf1 | …) // do_this is checked to be pure
and … = do_that (pf2 | …) // do_that is checked to be pure

Basically, the requirement is that (1) do_this and do_that can
only manipulate resources they own and (2) they do not share
any resources between them.

On Friday, May 9, 2014 6:44:17 PM UTC-4, John Skaller wrote:

On 10/05/2014, at 3:04 AM, gmhwxi wrote:

is actually the erasure of

val (pf | ()) = do_this (…)
val ((void)) = do_that (pf | …)

Clearly, we cannot call ‘do_that’ first because ‘do_that’
needs a proof returned by a call to ‘do_this’. This explains why,
sometimes, sequencing order, is significant (and, sometimes, it
is insignificant).

And when it is insignificant and we can evaluate in parallel,
how is that indicated?

–
john skaller
ska...@users.sourceforge.net
http://felix-lang.org

gmhwxi · May 17, 2014, 4:14pm

This is parallel-let binding.

It was actually supported in ATS at one-point as an
experiment:

http://www.cs.bu.edu/~hwxi/academic/papers/sblp09.pdfOn Saturday, May 17, 2014 12:04:55 PM UTC-4, Brandon Barker wrote:

It seems that it would be a very convenient syntax. Anyone could make a
simple wrapper function requiring a proof if they want to call something in
a parallel context.

Brandon Barker
brand...@gmail.com <javascript:>

On Sat, May 17, 2014 at 11:55 AM, gmhwxi <gmh...@gmail.com <javascript:>>wrote:

The compiler does to support it right now

On Saturday, May 17, 2014 11:33:09 AM UTC-4, Brandon Barker wrote:

So I’m probably missing several points here, including how to properly
use proofs and even what is meant by parallel. But I never saw any
parallelism in these concrete examples:

(* ****** ****** )
//
#include
“share/atspre_define.hats”
#include
“share/atspre_staload.hats”
//
( ****** ****** *)

%{^
int do_adding() {
volatile unsigned int i = 1;
while(i >= 0) {
i = i + 1;
}
return -1;
}
%}

extern
fun do_adding():int = “mac#”
// Now with proofs:
dataprop TESTPROP =
| TEST of ()
extern
fun do_adding_usepf(pf: TESTPROP | ):int = “mac#do_adding”
//

implement main0() = let

// val x = do_adding() and y = do_adding()
// same cpu usage as:
// val x = do_adding()

prval apf = TEST()
prval bpf = TEST()

// The cpu usage is the same again
val x = do_adding_usepf(apf | ) and y = do_adding_usepf(bpf | )

in
println!(x)
end

On Friday, May 9, 2014 8:24:52 PM UTC-4, gmhwxi wrote:

In ATS, a pure function can write but it can only write
to the memory it owns. The design in ATS goes like this:

If I want to indicate to the compiler that that do_this and do_that
can be evaluated in parallel, I use the following syntax:

prval (pf1, pf2) = … // [pf1] and [pf2] are separated
val … = do_this (pf1 | …) // do_this is checked to be pure
and … = do_that (pf2 | …) // do_that is checked to be pure

Basically, the requirement is that (1) do_this and do_that can
only manipulate resources they own and (2) they do not share
any resources between them.

On Friday, May 9, 2014 6:44:17 PM UTC-4, John Skaller wrote:

On 10/05/2014, at 3:04 AM, gmhwxi wrote:

is actually the erasure of

val (pf | ()) = do_this (…)
val ((void)) = do_that (pf | …)

Clearly, we cannot call ‘do_that’ first because ‘do_that’
needs a proof returned by a call to ‘do_this’. This explains why,
sometimes, sequencing order, is significant (and, sometimes, it
is insignificant).

And when it is insignificant and we can evaluate in parallel,
how is that indicated?

–
john skaller
ska...@users.sourceforge.net
http://felix-lang.org

–
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:>
.
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/48b9400b-cf43-4a36-a8b3-d60c27711484%40googlegroups.com https://groups.google.com/d/msgid/ats-lang-users/48b9400b-cf43-4a36-a8b3-d60c27711484%40googlegroups.com?utm_medium=email&utm_source=footer
.

john_skaller · May 9, 2014, 10:44pm

is actually the erasure of

val (pf | ()) = do_this (…)
val ((void)) = do_that (pf | …)

Clearly, we cannot call ‘do_that’ first because ‘do_that’
needs a proof returned by a call to ‘do_this’. This explains why,
sometimes, sequencing order, is significant (and, sometimes, it
is insignificant).

And when it is insignificant and we can evaluate in parallel,
how is that indicated?

john skaller
ska...@users.sourceforge.net
http://felix-lang.org

Brandon_Barker · May 17, 2014, 4:04pm

It seems that it would be a very convenient syntax. Anyone could make a
simple wrapper function requiring a proof if they want to call something in
a parallel context.

Brandon Barker
brandon…@gmail.comOn Sat, May 17, 2014 at 11:55 AM, gmhwxi gmh...@gmail.com wrote:

The compiler does to support it right now

On Saturday, May 17, 2014 11:33:09 AM UTC-4, Brandon Barker wrote:

So I’m probably missing several points here, including how to properly
use proofs and even what is meant by parallel. But I never saw any
parallelism in these concrete examples:

(* ****** ****** )
//
#include
“share/atspre_define.hats”
#include
“share/atspre_staload.hats”
//
( ****** ****** *)

%{^
int do_adding() {
volatile unsigned int i = 1;
while(i >= 0) {
i = i + 1;
}
return -1;
}
%}

extern
fun do_adding():int = “mac#”
// Now with proofs:
dataprop TESTPROP =
| TEST of ()
extern
fun do_adding_usepf(pf: TESTPROP | ):int = “mac#do_adding”
//

implement main0() = let

// val x = do_adding() and y = do_adding()
// same cpu usage as:
// val x = do_adding()

prval apf = TEST()
prval bpf = TEST()

// The cpu usage is the same again
val x = do_adding_usepf(apf | ) and y = do_adding_usepf(bpf | )

in
println!(x)
end

On Friday, May 9, 2014 8:24:52 PM UTC-4, gmhwxi wrote:

In ATS, a pure function can write but it can only write
to the memory it owns. The design in ATS goes like this:

If I want to indicate to the compiler that that do_this and do_that
can be evaluated in parallel, I use the following syntax:

prval (pf1, pf2) = … // [pf1] and [pf2] are separated
val … = do_this (pf1 | …) // do_this is checked to be pure
and … = do_that (pf2 | …) // do_that is checked to be pure

Basically, the requirement is that (1) do_this and do_that can
only manipulate resources they own and (2) they do not share
any resources between them.

On Friday, May 9, 2014 6:44:17 PM UTC-4, John Skaller wrote:

On 10/05/2014, at 3:04 AM, gmhwxi wrote:

is actually the erasure of

val (pf | ()) = do_this (…)
val ((void)) = do_that (pf | …)

Clearly, we cannot call ‘do_that’ first because ‘do_that’
needs a proof returned by a call to ‘do_this’. This explains why,
sometimes, sequencing order, is significant (and, sometimes, it
is insignificant).

And when it is insignificant and we can evaluate in parallel,
how is that indicated?

–
john skaller
ska...@users.sourceforge.net
http://felix-lang.org

–
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.
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/48b9400b-cf43-4a36-a8b3-d60c27711484%40googlegroups.com https://groups.google.com/d/msgid/ats-lang-users/48b9400b-cf43-4a36-a8b3-d60c27711484%40googlegroups.com?utm_medium=email&utm_source=footer
.

gmhwxi · May 9, 2014, 5:04pm

When I see the following code:

do_this(…); do_that(…);

My first question is always: Why can’t we write

do_that(…); do_this(…);

To many people, this sounds like a “stupid” question. But if you think
about it, this is actually a very profound question.

In Ocaml, this question is ignored. In other words, this question
can only be answered externally.

In Haskell, monads are introduced to support sequencing.

In ATS, you can think that the following code:

do_this (…); do_that (…);

is actually the erasure of

val (pf | ()) = do_this (…)
val ((void)) = do_that (pf | …)

Clearly, we cannot call ‘do_that’ first because ‘do_that’
needs a proof returned by a call to ‘do_this’. This explains why,
sometimes, sequencing order, is significant (and, sometimes, it
is insignificant).On Friday, May 9, 2014 12:22:05 PM UTC-4, Kiwamu Okabe wrote:

Hi Hongwei.

On Sat, May 10, 2014 at 1:16 AM, gmhwxi <gmh...@gmail.com <javascript:>> wrote:

I also suggest the following style of sequencing:

val () = do_this (…)
val () = do_that (…)

This style will make it very easy to add proofs into your code.

By the way, people often criticize the syntax of ATS for being verbose.
But in this case, the above style of sequencing is a lot more flexible
than
the following very restricted form:

do_this (…); do_that (…);

I like OCaml style. But…

For instance, we can later add proofs as follows:

val (pf | ()) = do_this (…)
val ((void)) = do_that (pf | …)

It makes sense.
“When in Rome, do as the Romans do.”

Thank’s,

Kiwamu Okabe at METASEPI DESIGN

gmhwxi · May 10, 2014, 12:24am

In ATS, a pure function can write but it can only write
to the memory it owns. The design in ATS goes like this:

If I want to indicate to the compiler that that do_this and do_that
can be evaluated in parallel, I use the following syntax:

prval (pf1, pf2) = … // [pf1] and [pf2] are separated
val … = do_this (pf1 | …) // do_this is checked to be pure
and … = do_that (pf2 | …) // do_that is checked to be pure

Basically, the requirement is that (1) do_this and do_that can
only manipulate resources they own and (2) they do not share
any resources between them.On Friday, May 9, 2014 6:44:17 PM UTC-4, John Skaller wrote:

On 10/05/2014, at 3:04 AM, gmhwxi wrote:

is actually the erasure of

val (pf | ()) = do_this (…)
val ((void)) = do_that (pf | …)

Clearly, we cannot call ‘do_that’ first because ‘do_that’
needs a proof returned by a call to ‘do_this’. This explains why,
sometimes, sequencing order, is significant (and, sometimes, it
is insignificant).

And when it is insignificant and we can evaluate in parallel,
how is that indicated?

–
john skaller
ska...@users.sourceforge.net <javascript:>
http://felix-lang.org

Topic		Replies	Views
ATS for Arduino Google Group	6	473	November 11, 2014
Functional programming on Arduino Uno Google Group	0	307	October 19, 2014
ATS-par-emit: labels for instructions Google Group	10	502	August 19, 2014
ATS for AVR programming Google Group	0	277	November 8, 2014
ATS support in Pure Google Group	1	322	October 15, 2014

ATS programing on ChibiOS/RT and Arduino

Best regards,

Thank’s for your advice.

Sometime 32-bit arch also: LPC812M101JDH20 :: NXP

Thank’s,

Thank’s,

Related Topics