Comments on CASL concrete syntax

[Till Mossakowski <till@informatik.uni-bremen.de>]

Dear Peter,

Thank you and the others for finding a good compromise.

I have some rather technical comments, most of which arose during
the attempt (together with Kolyang) to implement an encoding 
of CASL basic specs within Isabelle-HOL (we will give
a demo of this on Friday).

[It should be stressed that the concrete syntax proposal may well need
 some adjustments to facilitate/allow deterministic implementations
 of parsers using standard tools.  Such adjustments will hopefully not
 affect the appearance of formatted specifications too much!  
--PDM]


AXIOMs
------
I think the examples PATH, LIST_WITH_ORDER and others
are not covered by the current syntax (I wonder how they
go through Mark's parser...).

The current syntax requires the keyword "axiom(s)" in front of
each individual axiom, except for atoms and quantifications.
I would propose to have something like
	AXIOM-S ::= axiom AXIOM | axioms AXIOM;... | QUANTIFICATION
instead.

[Ah, I see that the grammar in CASL/SyntaxIssues didn't get completely
 updated to match the ASF+SDF grammar in CASL/SyntaxExamples/ASF+SDF, 
 which is:
    AXIOM-S ";" {FORMULA ";"}+   -> AXIOM-ITEMS
    AXIOM-S                      -> AXIOM-ITEMS
    "axiom" AXIOM  -> AXIOM-S
    "axioms" AXIOM -> AXIOM-S
    QUANTIFICATION -> AXIOM-S
 With this grammar, the PATH and LIST_WITH_ORDER examples parse OK.
 Thanks for pointing out the mistake.  However, my proposal for the
 corrected grammar would probably be
 ! AXIOM-ITEMS      ::=  AXIOM-S; AXIOM;... |  AXIOM-S;  |  AXIOM-S
 ! AXIOM-S          ::=  axiom AXIOM  |  axioms AXIOM  |  QUANTIFICATION
 (We may experiment with the ASF+SDF version when Bjarke Wedemeijer and
 I give a short demo of it on Friday.)  
--PDM]


Variables, constants, and qualifications
----------------------------------------
A context-free parser cannot distinguish constants and variables
(we always parse them as constants, and later on replace those
that are declared as variables by constants).

Moreover, a qualified constant c:s cannot be distinguished from
a sort qualifications c:s with an unqualified constant c.
Note that both may have a different semantics: Given

spec sorted_or_qualified =
sorts  s,t;
       s < t;
ops    c:s
axiom  defined (c:t)

then defined (c:t) is ill-formed if c:t is a qualified constant,
but well-formed if it is a sort qualification of an
unqualified constant.
I interpret the third-last paragraph on p.7 in such a way 
that qualified constant function application has a higher
precedence than sort qualification (btw, I do not understand
any other meaning of this sentence: which other ambiguities
could arise?).  [I see now that there are none.  Perhaps I was
thinking of a HO extension, where parentheses wouldn't be obligatory
in function application... --PDM]
In particular, if we want to have all institution sentences
directly represented in CASL, then we need this precedence
to be able to select profiles of constants (a sort
qualification does not select a particular profile,
since implicit injections may be inserted inside it).

This complicates things for context free parsers:
Now c:t is parsed as a qualified constant application,
but if later on c happens to be a variable, c:t has
to be considered to be a sort qualification.

[This suggests that we might revert to Bernd's original idea (if I
 recall correctly) of using "TERM as SORT" both for SORTED-TERM and
 CAST.  I regard this as a very minor issue, as (we hope that) it will
 seldom be necessary to use SORTED-TERM in practice.  Does anyone see
 any drawbacks to this change?  
--PDM]

ISO-DECLs
---------
The current syntax is similar to that of SUBSORT-DECLs:
	ISO-DECL ::= SORT,...,SORT = SORT
The last sort is singled out, but this has no semantical meaning.
Wouldn't it better fit with the semantics to have
	ISO-DECL ::= SORT=...=SORT = SORT
?

[The intention was that, as in SUBSORT-DECL, the last SORT was to be
 declared elsewhere, so it was a bit special.  But perhaps it would be
 better to let SUBSORT-DECL and ISO-DECL declare *all* the sorts
 mentioned (irrespective of whether they are declared elsewhere or
 not - recalling that redeclaration is semantically irrelevant).  Then
   sort Int; subsort Nat < Int
 could be abbreviated to 
   subsorts Nat < Int
 Would this be an improvemement or not, e.g., methodologically?  See
 also some of the points made in Language Design Note of Dissent L-4;
 the well-formedness of DATATYPE-DECL, however, is really a separate
 issue.
--PDM]

Greetings,
Till