[CoFI] Re: Concrete Syntax

[Christine.Choppy@irin.univ-nantes.fr (Christine Choppy)]

Dear all,

This mail tries to reflect our common reaction (Michel, Frederic and myself)
to the concrete syntax for basic specifications (of October 6th).

Since Peter asked for positive reactions I'd like to add that there are
lots of things we like !!

Now, more comments:

** Section 2: Input Syntax
page 3
CONSTRAINT ::= > | = | freely
Some of us find this a bit strange, we propose
 ::= instead of >, gen_by instead of =, freely gen_by instead of freely

page 4:  
FUN-ATTRS: we support Frederic and Peter's proposals

PRED-TYPE:
-- in order to prevent from some old ghosts return, we would like to avoid
   ->  truth
-- we would prefer to have predicates introduced by a keywords as for sorts,
 ops, etc.

AXIOM-S:
.AXIOM may be ambiguous when there is an id . for an operator
For sake of homogeneity, we think it is better to ask for the keyword axiom:
AXIOM-S ::= axiom AXIOM | axioms AXIOM
(allowing several AXIOM after the keyword as in examples by Peter sec 2,
e.g. PATH)

IMPLICATION ::= FORMULA => FORMULA | FORMULA if FORMULA
We like this and think that <= instead of if might be misleading.

PRED-SYMB and FUN-SYMB:
We still prefer " " instead of ( ), and
"f __ __: sort1 sort2 -> sort"(t1,t2) instead of 
(f __ __: sort1 sort2 -> sort)(t1,t2)

Using parentheses may look strange within terms, renamings, etc.

EXISTL-EQUATION
Given that =! is ambiguous (see below) we suggest to use =e=
how to parse !x=!y given that !__ is an operator ?

**Section 3: Display Format
Identifiers: we would prefer that the display format for compound ids
mmore closely reflect the input format, and therefore we are not in 
favor of using subscripts.

Symbols: probably we want to add exists1 and . 

**Section 4: Disambiguation
- page 6
We are not sure that f(x):S is not ambiguous.
(i) f x : S may be parsed as f (x:S) or as (f x):S
[we do not take into consideration here the fact that f is prefix,
which is a particular case]
(ii) parentheses may be added anywhere or x may stand for a big term,
so f x : S may be written also f (x) : S
and may be parsed as f ((x):S) or as (f (x)):S

**Section 6: Comments and Annotations
- section 6.1 page 8
Do we want to reserve </> on some occasions to prevent:
%% fancy comment using <latex>$</>$<other></></>

page 9: it may be safer to end %%ignore by </ignore>

- section 6.2 page 9
Do we want to reserve %! on some occasions to prevent:
%! <<<latex>$<<$<other>%!%!

page 10: sum__ to__ : it may be useful to keep the #1 #2 convention
to allow for potential change on the order of argts.

** Appendix A page 11
Mixfix notation: we would like to have invisible symbols since we found
them very useful.

Precedence in terms: we think we should not have fixed precedence for
symbols starting with particular characters, as told before this may be
really akward.

** Miscellaneous: display with bold
There is a possibility that we end up with a lot of bold characters
in a given spec. In our proposal, we made a lighter use of bolds
(but this may be worked out later).

Cheers,

Christine.