ATerms vs String representation (forwarded from Mark van den Brand)

[Helene.Kirchner@loria.fr]

[Here is a first reaction from Mark van den Brand concerning the
output format for parsers. HK]

I have looked at the ATerm format and the string representation proposed
by Christophe and I want to point out the following main difference between
these representations. The abstract syntax rules are more or less 
explicit coded in the string format: (total-op-type (SORTS . SORT .))
whereas in ATerm this would be: total-op-type(. , .).
In fact the SORTS and SORT are redundant information because given
the unique identifier "total-op-type" this information can be reconstructed.

However it is possible to code this type information also in the ATerm format:
total-op-type(SORTS(.),SORT(.)). This may be information may be very
helpful when dealing with mappings from one format to another.

The example of note T3 would look like:
basic-spec(
 BASIC-ITEMS*([
  SIG-ITEMS(
   datatype-items(
    DATATYPE-DECL+([
     datatype-decl(
      SORT(mixid1(words([Nat]))),
      ALTERNATIVE+([
       total-construct(OP-NAME(mixid1(words([0]))),
                       COMPONENTS*([empty-components])),
       total-construct(
        OP-NAME(mixid1(words([suc]))),
        COMPONENTS*([total-select(OP-NAME+([mixid1(words([pre]))]),
                                  SORT(mixid1(words([Nat]))))]))]))]))),
  SIG-ITEMS(
   op-items(
    OP-ITEM+([
     op-decl(
      OP-NAME+([mixid4(mixid2(signs(+)))]),
      OP-TYPE(
       total-op-type(sorts([mixid1(words([Nat])),
                            mixid1(words([Nat]))]),
                     mixid1(words([Nat])))),
      OP-ATTR*([empty-op-attr]))]))),
  SIG-ITEMS(
   op-items(
    OP-ITEM+([
     op-defn(
      OP-NAME(mixid1(words([1]))),
      OP-HEAD(
       total-op-head(ARG-DECL*([empty-arg-decl]),
                     SORT(mixid1(words([Nat]))))),
      TERM(SIMPLE-TERM+([
       application(
        OP-SYMB(mixid1(words([suc]))),
        TERMS(terms(TERM*([SIMPLE-TERM+([SIMPLE-ID(words([0]))])]))))])))]))),
  var-items(
   VAR-DECL+([
    var-decl(
     VAR+([
      SIMPLE-ID(words([m])),
      SIMPLE-ID(words([n]))]),
     SORT(mixid1(words([Nat]))))])),
  axiom-items(
   FORMULA+([
    strong-equation(
     SIMPLE-TERM+([
      SIMPLE-ID(words([m])),
      toast-Var-Or-Const(+),
      SIMPLE-ID(words([0]))]),
     SIMPLE-TERM+([SIMPLE-ID(words([m]))])),
    strong-equation(
     SIMPLE-TERM+([
      SIMPLE-ID(words([m])),
      toast-Var-Or-Const(+),
      application(
       OP-SYMB(mixid1(words([suc]))),
       TERMS(terms(TERM*([SIMPLE-TERM+([SIMPLE-ID(words([n]))])]))))]),
     SIMPLE-TERM+([
      application(
       OP-SYMB(mixid1(words([suc]))),
       TERMS(
        terms(
         TERM*([
          SIMPLE-TERM+([SIMPLE-ID(words([m])),
          toast-Var-Or-Const(+),
          SIMPLE-ID(words([n]))])])))),
      SIMPLE-ID(words([end]))]))]))]))

I did not deal with the lexical syntax yet. Furthermore, the pretty printing
of the terms is performed manually. Finally, the SIMPLE-TERM+ is not in the
abstract syntax of Casl but is introduced to deal with the mixed fix operators.

To summarize I would be in favour of having just one formalism for checking
the correctness of the parsers and as exchange format. Because ATerms and
the string representation are so close I would suggest the extension described
above.

-- Mark


----------------------------------------------------------------
M.G.J. van den Brand,
Department of Software Engineering
CWI
Kruislaan 413, NL-1098 SJ AMSTERDAM, The Netherlands.

Tel___(+31) 20 5924103  WWW____http://adam.wins.uva.nl/~markvdb/
Fax___(+31) 20 5924199  Email__markvdb@cwi.nl         
----------------------------------------------------------------