#define and macdef are largely undocumented.
#define is similar to its counterpart in C. At the beginning of the
following page, there
are some interesting cases of using #define:
The following old page contains some explanation on macdef:
http://ats-lang.sourceforge.net/htdocs-old/TUTORIAL/contents/macros.html
Yes, the behavior is expected.
If macro TAIL is used, then UTF8_C2_2 is a unary constructor
taking only one argument; the argument is a pair of proofs:| UTF8_C2_2 (pf12) => … // pf12.0 for pf1 and pf12.1 for pf2
I did not knew this one (not tried, as not good for direct destructuring).
So ATS’s #define are really real syntactical constructs. That’s important
to know.
Or you can write
| UTF8_C2_2 (@(pf1, pf2)) => …
Checked! This one’s fine.
You may be able to write
| UTF8_C2_2((pf1, pf2)) => … // I am not sure about this one.
That’s the one I tried, and it complained “the tuple/record pattern is
ill-typed”.
So either using @(…) or pf.N where N is a decimal, depending on the use
case.
These additional requirements on writing, are to be balanced with the
benefits of using #define.
As said above, I’m not used to defines/macro and had bad experiences with
C macros, thus my question for comments
Well, finally, there is no far less reasons to be afraid for #define in ATS
than in C; it’s a lot safer in ATS: one can’t do anything too much
unreadable with #define and #define are scoped.
Sample showing #define can’t do anything too much silly, as a consequence
of it being handled as an AST node:
val a = (1)
#define FOO (
#define BAR )
val b = FOO 1 BAR
It complains a closing parenthesis is missing next to #define FOO (
Sample showing #define are scoped:
#define FOO 1
val a = FOO
val () =
let
val b = FOO
#define BAR 1
val c = BAR
in ()
end
val d = FOO
val e = BAR // It complains! That’s pretty!
On the last line, it complains “the dynamic identifier [BAR] is
unrecognized” and it’s good it complains.
I like ATS’s #define more than C #define.
These additional requirements on writing, are to be balanced with the
benefits of using #define.
Seems a good trade‑off, is to use #define for simple expressions, not
tuples (while there may be tuple in the expression, which is a different
case). It can be enough to help readability, and may be even more, as it’s
easier to not lose track of what a “sentence” stands for (the “sentences”
structure is not altered). Added doing so avoids the use of @(…) and
P.n , it looks a good recommendation in using #define.
Yes, the behavior is expected.
If macro TAIL is used, then UTF8_C2_2 is a unary constructor
taking only one argument; the argument is a pair of proofs:
| UTF8_C2_2 (pf12) => … // pf12.0 for pf1 and pf12.1 for pf2
Or you can write
| UTF8_C2_2 (@(pf1, pf2)) => …
You may be able to write
| UTF8_C2_2((pf1, pf2)) => … // I am not sure about this one.On Saturday, December 12, 2015 at 3:38:41 PM UTC-5, Yannick Duchêne wrote:
Based on the previous example, I encountered an issue with #define. I
don’t know if it’s expected or not. It’s related to when and how it
expands, and it came as a surprise to me.Given this, without using the #define:
dataprop UTF8_C2 (i:int, c:int) =
| {b:hb_C2; i == 1} UTF8_C2_1(i, b - 0xC0) of HEAD
| {b:tb_80; i == 2} UTF8_C2_2(i, added(c, b)) of (UTF8_C2(i-1, c), DATA(i,
b))I can try this (unsolved constraint, but OK otherwise):
prfn utf8_c2_lower {c:int} (pf:UTF8_C2(2, c)): [c >= 128] void =
case+ pf of
| UTF8_C2_2(pf1, pf2) =>
let (* Pending )
in ( Pending *)
endHowever, given this, using #define TAIL:
dataprop UTF8_C2 (i:int, c:int) =
| {b:hb_C2; i == 1} UTF8_C2_1(i, b - 0xC0) of HEAD
| {b:tb_80; i == 2} UTF8_C2_2(i, added(c, b)) of TAIL(UTF8_C2)If I try the same:
prfn utf8_c2_lower {c:int} (pf:UTF8_C2(2, c)): [c >= 128] void =
case+ pf of
| UTF8_C2_2(pf1, pf2) =>
let (* Pending )
in ( Pending *)
endI get this error about
UTF8_C2_2(pf1, pf2): “constructor arity mismatch:
fewer arguments are expected.”When using the #define, the checker believes the proof gets a single
argument. Is this expected?Le mardi 12 mai 2015 20:00:03 UTC+2, gmhwxi a écrit :
#define and macdef are largely undocumented.
#define is similar to its counterpart in C. At the beginning of the
following page, there
are some interesting cases of using #define:The following old page contains some explanation on macdef:
http://ats-lang.sourceforge.net/htdocs-old/TUTORIAL/contents/macros.html
Based on the previous example, I encountered an issue with #define. I don’t
know if it’s expected or not. It’s related to when and how it expands, and
it came as a surprise to me.
Given this, without using the #define:
dataprop UTF8_C2 (i:int, c:int) =
| {b:hb_C2; i == 1} UTF8_C2_1(i, b - 0xC0) of HEAD
| {b:tb_80; i == 2} UTF8_C2_2(i, added(c, b)) of (UTF8_C2(i-1, c), DATA(i, b
))
I can try this (unsolved constraint, but OK otherwise):
prfn utf8_c2_lower {c:int} (pf:UTF8_C2(2, c)): [c >= 128] void =
case+ pf of
| UTF8_C2_2(pf1, pf2) =>
let (* Pending )
in ( Pending *)
end
However, given this, using #define TAIL:
dataprop UTF8_C2 (i:int, c:int) =
| {b:hb_C2; i == 1} UTF8_C2_1(i, b - 0xC0) of HEAD
| {b:tb_80; i == 2} UTF8_C2_2(i, added(c, b)) of TAIL(UTF8_C2)
If I try the same:
prfn utf8_c2_lower {c:int} (pf:UTF8_C2(2, c)): [c >= 128] void =
case+ pf of
| UTF8_C2_2(pf1, pf2) =>
let (* Pending )
in ( Pending *)
end
I get this error about UTF8_C2_2(pf1, pf2): “constructor arity mismatch:
fewer arguments are expected.”
When using the #define, the checker believes the proof gets a single
argument. Is this expected?Le mardi 12 mai 2015 20:00:03 UTC+2, gmhwxi a écrit :
#define and macdef are largely undocumented.
#define is similar to its counterpart in C. At the beginning of the
following page, there
are some interesting cases of using #define:The following old page contains some explanation on macdef:
http://ats-lang.sourceforge.net/htdocs-old/TUTORIAL/contents/macros.html
I’m coming from the Ada world, where macros are far from being advertised,
so may be I’m biased being a bit afraid of macro. There are more check with
macdef than with #define, as I recall, but it seems macdef only wants
dynamic identifiers in the expression it introduces, so I’m talking here
about #define, as my question came in the static.
Is this kind of thing, which follows, rather OK or not, and also, is there
another way to do, without #define?
As they were many repetitions, I turned this:
dataprop UTF8_00 (i:int, c:int) =
| {b:hb00; i == 1} UTF8_00_1(i, b) of INPUT(i, b)
dataprop UTF8_C2 (i:int, c:int) =
| {b:hbC2; i == 1} UTF8_C2_1(i, b - 0xC0) of INPUT(i, b)
| {b:tb80; i == 2} UTF8_C2_2(i, added(c, b)) of (UTF8_C2(i-1, c), INPUT(i, b
))
| {b:tb80; i == 2} UTF8_C2_2(i, added(c, b)) of (UTF8_C2(i-1, c), INPUT(i, b
))
dataprop UTF8_E0 (i:int, c:int) =
| {b:hbE0; i == 1} UTF8_E0_1(i, b - 0xE0) of INPUT(i, b)
| {b:tbA0; i == 2} UTF8_E0_2(i, added(c, b)) of (UTF8_E0(i-1, c), INPUT(i, b
))
| {b:tb80; i == 3} UTF8_E0_3(i, added(c, b)) of (UTF8_E0(i-1, c), INPUT(i, b
))
dataprop UTF8_E1 (i:int, c:int) =
| {b:hbE1; i == 1} UTF8_E1_1(i, b - 0xE0) of INPUT(i, b)
| {b:tb80; i == 2} UTF8_E1_2(i, added(c, b)) of (UTF8_E1(i-1, c), INPUT(i, b
))
| {b:tb80; i == 3} UTF8_E1_3(i, added(c, b)) of (UTF8_E1(i-1, c), INPUT(i, b
))
/* more of the like */
Into this, using a #define:
#define NEXT(UTF8_XX) (UTF8_XX(i-1, c), INPUT(i, b))
dataprop UTF8_00 (i:int, c:int) =
| {b:hb00; i == 1} UTF8_00_1(i, b) of INPUT(i, b)
dataprop UTF8_C2 (i:int, c:int) =
| {b:hbC2; i == 1} UTF8_C2_1(i, b - 0xC0) of INPUT(i, b)
| {b:tb80; i == 2} UTF8_C2_2(i, added(c, b)) of NEXT(UTF8_C2)
| {b:tb80; i == 2} UTF8_C2_2(i, added(c, b)) of NEXT(UTF8_C2)
dataprop UTF8_E0 (i:int, c:int) =
| {b:hbE0; i == 1} UTF8_E0_1(i, b - 0xE0) of INPUT(i, b)
| {b:tbA0; i == 2} UTF8_E0_2(i, added(c, b)) of NEXT(UTF8_E0)
| {b:tb80; i == 3} UTF8_E0_3(i, added(c, b)) of NEXT(UTF8_E0)
dataprop UTF8_E1 (i:int, c:int) =
| {b:hbE1; i == 1} UTF8_E1_1(i, b - 0xE0) of INPUT(i, b)
| {b:tb80; i == 2} UTF8_E1_2(i, added(c, b)) of NEXT(UTF8_E1)
| {b:tb80; i == 3} UTF8_E1_3(i, added(c, b)) of NEXT(UTF8_E1)
/* more of the like */
#undef NEXT
Writing things this way helps readability and maintenance (as it is
terser), but is there a risk to face issues, in the large? If there are
people who use #defines a lot in ATS2, what’s your overall feelings and
opinions?
Or is there a better way to do? (for a previous case, I could use a
stadef, but this won’t work here) As said above, I’m not used to
defines/macro and had bad experiences with C macros, thus my question for
comments, or better (if possible), another track.Le mardi 12 mai 2015 20:00:03 UTC+2, gmhwxi a écrit :
#define and macdef are largely undocumented.
#define is similar to its counterpart in C. At the beginning of the
following page, there
are some interesting cases of using #define:The following old page contains some explanation on macdef:
http://ats-lang.sourceforge.net/htdocs-old/TUTORIAL/contents/macros.html
I myself do not really use ‘#define’ to do anything “fancy”.
I am actually a bit surprised that you could do what you did using
#define. I mostly use #define to introduce constants:
#define XYZ 1
#define XYZ1 (XYZ+1)
Constants introduced in this way can be used in both statics and dynamics.On Friday, December 11, 2015 at 9:59:46 PM UTC-5, Yannick Duchêne wrote:
I’m coming from the Ada world, where macros are far from being advertised,
so may be I’m biased being a bit afraid of macro. There are more check with
macdef than with #define, as I recall, but it seems macdef only wants
dynamic identifiers in the expression it introduces, so I’m talking here
about #define, as my question came in the static.Is this kind of thing, which follows, rather OK or not, and also, is there
another way to do, without #define?As they were many repetitions, I turned this:
dataprop UTF8_00 (i:int, c:int) =
| {b:hb00; i == 1} UTF8_00_1(i, b) of INPUT(i, b)dataprop UTF8_C2 (i:int, c:int) =
| {b:hbC2; i == 1} UTF8_C2_1(i, b - 0xC0) of INPUT(i, b)
| {b:tb80; i == 2} UTF8_C2_2(i, added(c, b)) of (UTF8_C2(i-1, c), INPUT(i,
b))
| {b:tb80; i == 2} UTF8_C2_2(i, added(c, b)) of (UTF8_C2(i-1, c), INPUT(i,
b))dataprop UTF8_E0 (i:int, c:int) =
| {b:hbE0; i == 1} UTF8_E0_1(i, b - 0xE0) of INPUT(i, b)
| {b:tbA0; i == 2} UTF8_E0_2(i, added(c, b)) of (UTF8_E0(i-1, c), INPUT(i,
b))
| {b:tb80; i == 3} UTF8_E0_3(i, added(c, b)) of (UTF8_E0(i-1, c), INPUT(i,
b))dataprop UTF8_E1 (i:int, c:int) =
| {b:hbE1; i == 1} UTF8_E1_1(i, b - 0xE0) of INPUT(i, b)
| {b:tb80; i == 2} UTF8_E1_2(i, added(c, b)) of (UTF8_E1(i-1, c), INPUT(i,
b))
| {b:tb80; i == 3} UTF8_E1_3(i, added(c, b)) of (UTF8_E1(i-1, c), INPUT(i,
b))/* more of the like */
Into this, using a #define:
#define NEXT(UTF8_XX) (UTF8_XX(i-1, c), INPUT(i, b))
dataprop UTF8_00 (i:int, c:int) =
| {b:hb00; i == 1} UTF8_00_1(i, b) of INPUT(i, b)dataprop UTF8_C2 (i:int, c:int) =
| {b:hbC2; i == 1} UTF8_C2_1(i, b - 0xC0) of INPUT(i, b)
| {b:tb80; i == 2} UTF8_C2_2(i, added(c, b)) of NEXT(UTF8_C2)
| {b:tb80; i == 2} UTF8_C2_2(i, added(c, b)) of NEXT(UTF8_C2)dataprop UTF8_E0 (i:int, c:int) =
| {b:hbE0; i == 1} UTF8_E0_1(i, b - 0xE0) of INPUT(i, b)
| {b:tbA0; i == 2} UTF8_E0_2(i, added(c, b)) of NEXT(UTF8_E0)
…
May I’m going too easily too far with it… (time will say).
That said, I feel if references to defines was syntactically
distinguishable, this would be nice. Ex. with a character prefix which
would clearly makes visible it’s a reference to a define,Le samedi 12 décembre 2015 04:33:14 UTC+1, gmhwxi a écrit :
I myself do not really use ‘#define’ to do anything “fancy”.
I am actually a bit surprised that you could do what you did using
#define. I mostly use #define to introduce constants:#define XYZ 1
#define XYZ1 (XYZ+1)Constants introduced in this way can be used in both statics and dynamics.