[CoFI] (Minor) Comments on v0.99

[cerioli@disi.unige.it (Maura Cerioli)]

Anonymous mixfix operators
===========================
There is (just) one common situation where anonymous mixfix operators are
used, imho, that is to describe positional notation for numbers.
I think that it is mandatory to be able to use standard notation for
numbers in CASL. Thus, either we have a bunch of "basic data types"
(incuding naturals and integers) predefined using an extended syntax or we
do allow anonymous mixfix operators in basic CASL and then we can require
that the "basic data types" are simply (predefined) basic specifications.

[It might seem attractive to use `__ __' for this purpose - but
 presumably you wouldn't want it to be associative, so iterations
 of it, e.g. 102, would need explicit grouping, e.g. (10)2; recall
 that grouping is supposed to be determined independently of
 argument and result sorts...  Note that if 02=2 then 1(02)=12...
 But maybe you had something else in mind?

 My proposal would be to introduce constants `0', ..., `9', and
 postfix ops `__0', ..., `__9', so that e.g. 102 is unambiguously
 grouped.  This does not require anonymous ops, although the
 signature is admittedly somewhat messier.  --PDM]

A couple of comments on possible changes
=========================================

1 Bernd Krieg-Brueckner wrote:
  > imports
  > -------
  > I seem to remember from some email that
  >       imports SP
  >       spec S [PAR1] [Par2] = ...
  > was regarded (more?) favourably by someone.
  > [I.e., instead of "spec S [PAR1] [Par2] imports SP = ..." --PDM]

  I personnally favour the current version, as the "imports"
  are for me a (fixed) part of the body; thus, I prefer to have
  them listed near the body itself.


2 Bernd Krieg-Brueckner wrote:
  > Arrows in morphisms
  > -------------------
  > I find it very confusing for the beginner that the arrows |-> go one way
  > in renamings and the other in fitting morphisms. I know abstractly from
  > the theoretical background that the fitting morphisms go "the other way
  > round", but regard this rather as a technical detail. I am afraid that
  > this only occurred to me late last week when discussing with Till;
  > indeed there are some special cases when fitting can be replaced by
  > renaming. [I thought that this was actually the general case?  --PDM]
  > When both are next to each other it is particularly confusing;
  > see e.g. the example in SyntaxExamples:
  > spec PATH
  >       NON_EMPTY_LIST_OF[NAME fitting Item |-> Name]
  >               renaming List[Name] |-> Path, ...
  > My suggestion: regard "|->" as a symbol for substitution, and change the
  > direction in fittings.

  > [The fitting applies to the implicit parameter spec, e.g., spec ITEM =
  > sort Item.  The induced renaming is applied to NON_EMPTY_LIST_OF[ITEM],
  > and the fitting seems to me to go in the right direction for
  > consistency with renaming.  Please would those who have opinions on
  > this issue send them to cofi-language@brics.dk as soon as possible.
  >  --PDM]

  Maybe I'm missing something, but it seems to me that the current
  version is consistent in using the symbol |-> to mean "becomes".
  So we have (in both cases of the example) on the left-hand side the
  symbol to be renamed and on the right-hand side the new name we will
  use in the result.
  Therefore, I prefer not to have changes.
  (Possibly the keyword "fitting" is confusing, because it suggest
  that the actual parameter is the object of the action, but I have no
  better suggestion)

TERMs, MIXED-TERMs and SIMPLE-TERMs
====================================
I'm a bit lost.
I understand that
FORMULA ::= SIMPLE-TERM SIMPLE-TERM...
is the production corresponding to the application of a predicate in mixfix
notation (?correct?).  [Yes. --PDM]
In this case, I find the proposal at the same time too restrictive and too
general (again, *if* I'm getting it right)
Indeed, on one side the distinction between terms and atomic formulae
disappeared (I suppose that there are static checks in order here?)

[Apart from some minor differences (concerning qualified symbols,
 casts, and sorted terms), atomic formulae and terms do indeed have
 the same appearance regarding mixfix applications. --PDM]

On the other side, if I want, for instance, specify a simple "rewriting
machine" for natural numbers, with an (infix) arrow predicate denoting a
(hopefully) simplification step
        pred __ -->__: nat nat;
then the axiom
        axiom forall a:nat.a+zero --> a
is incorrect and I should write instead
        axiom forall a:nat.(a+zero) --> a
This is not a terrible drawback, of course, but I'm missing why should we
restrict the syntax of "operands" for mixfix predicates. Is the restriction
drastically improving parsers?

[Perhaps the main issue here is whether or not we should rely on
 the distinction between operation and predicate symbols when
 disambiguating the grouping.  If __-->__  and __+__ were two infix
 operations, we'd have to group their composition explicitly; it
 seemed more uniform to do this also when one was a predicate.
 But it would be easy enough to generalize the syntax above, taking
 TERM instead of SIMPLE-TERM, and letting the grouping parentheses be
 omitted.  --PDM]

(BTW I wasn't able to find PRED-SYMB and OP-SYMB in the concrete syntax,
though I assume they are as in the abstract one)  [Right.  --PDM]

Maura