#define and macdef

[gmhwxi]

#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:

http://www.ats-lang.org/SERVER/MYCODE/Patsoptaas_serve.php?mycode_url=https://raw.githubusercontent.com/githwxi/ATS-Postiats/master/doc/EXAMPLE/ARITH/tally-of-powers.dats

The following old page contains some explanation on macdef:

http://ats-lang.sourceforge.net/htdocs-old/TUTORIAL/contents/macros.html

[Yannick Duchêne]

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.

[gmhwxi]

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.

...

[Yannick Duchêne]

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,

[Yannick Duchêne]

Le samedi 12 décembre 2015 03:59:46 UTC+1, Yannick Duchêne a écrit :

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.

[Yannick Duchêne]

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 :

[gmhwxi]


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.




[Yannick Duchêne]

Le samedi 12 décembre 2015 23:14:20 UTC+1, gmhwxi a écrit :


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.

[Yannick Duchêne]

Le samedi 12 décembre 2015 23:38:28 UTC+1, Yannick Duchêne a écrit :

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.

[Yannick Duchêne]

A macrodef is a bit like a closure whose application is pending, ins’t it?

[gmhwxi]

The main use of macrodef is to define recursive macros. This feature

is not extensively used at this point, though.