path: root/doc/discussion-syntaxe.txt

  Synth�se des diff�rentes propositions de "r�novation" de la syntaxe de Coq
  --------------------------------------------------------------------------

I) Constructions

   �l�ments de doctrine : 

   - choix de mots-cl�s en minuscule
   - proche de ml

A) Produit

  Consensus apparent pour remplacer la syntaxe actuelle � base de
parenth�ses par quelque chose de plus "simple". Les options retenues
sont "! x . P x", "Forall x . P x" ou "forall x . P x".

  A1) Choix du symbole de t�te

  "!" est court et expressif mais sans doute moins que "forall"
  surtout pour un d�butant. "!", c'est le choix d'HOL, "forall" (en
  majuscule), celui de PVS. Un inconv�nient de "forall" est qu'il
  n'est pas tr�s appropri� pour le produit fonctionnel d�pendant (ou
  alors, on propose � la fois "pi" et "forall" comme synonymes)

  Rem: Quelque soit le choix du symbole de t�te, un parseur/printeur
  unicode pourra substituer le symbole de t�te par le "\forall" (et le
  "\pi" dans l'option ou "pi" et "forall" coexistent)


  A2) Quantification sur plusieurs variables

  A2a) "! x y1 z. P x"

  Avantages : analogie avec la juxtaposition des arguments pour l'application,
  r�miniscent de la juxtaposition en math "\forall xyz.P(x)", c'est le
  choix d'HOL.

  A2b) "! x, y1, z. P x"

  Avantages : plus standard ?


  A3) Mention des types

  A3a) On a s�par� par des espaces

  A3a1) "! ( x x1 : A ) ( y1 y2 : f a ( g b ) ) z. P x"
  A3a2) "! x x1 : A, y1 y2 : f a ( g b ), z. P x"
  A3a3) "! x x1 : A; y1 y2 : f a ( g b ); z. P x"
  A3a4) "! x x1 : A. ! y1 y2 : f a ( g b ). ! z. P x"
    Rem: ici, un seul type explicite par quantificateur; mais incoh�rence
    avec "! x y. P x" o� x et y peuvent avoir des types diff�rente; en
    revanche, se comporte bien � l'�criture sur plusieurs lignes

  A3b) On a s�par� par des virgules

  A3b1) "! ( x, x1 : A ), ( y1, y2 : f a ( g b ) ), z. P x"
  A3b2) "! x, x1 : A, y1 y2 : f a ( g b ), z. P x"
  A3b3) "! x, x1 : A; y1 y2 : f a ( g b ); z. P x"
  A3b4) "! x, x1 : A. ! y1 y2 : f a ( g b ) . ! z. P x"

  Rem: si ";" voir section terminateur de phrase


B) Application

  Pas d'apparence de consensus

  B1) Principe que les parenth�ses font partie de la notation
  (appliqu� par une partie de la communaut� \-calcul et dans Lisp),

  B2) Principe que les parenth�ses ne servent qu'� grouper
  (appliqu� par une partie de la communaut� \-calcul et dans ML)

  Argument : notations plus l�g�res, coh�rence avec ML

  Ce choix implique-t-il de donner la plus grande pr�c�dence � l'application ?
  Exemple : comment comprendre ces expressions ?

  f 4 + x
  P A -> B
  ! x : f a = b c . h y 


C) Abstraction

  Tant qu'� faire, renoncement � la notation crochet pour obtenir une
meilleure coh�rence avec le reste.

  C1) "\ x. g y" ou "fun x. g y"  (analogie avec "!" ou "forall")
  C2) "fun x => g y" ou "Fun x => g y" (analogie avec caml et le filtrage)
  C3) "\ x => g y" (r�miniscent de Haskell)


D) Arithm�tique

  Consensus pour r�server 0, 1, 2, ... ainsi que +, -, *, /, < et > �
l'arithm�tique. Tant qu'� faire, >=, <= et <> aussi (l'usage en est
standard).

  Trois approches ont �t� propos�es pour distinguer l'alg�bre
concern�e (N, Z, R, ...).

  D1) Qualification des op�rateurs, qui ob�issent alors aux m�mes r�gles
que des identificateurs concernant la surcharge (c�d le dernier module
"import�" ("ouvert" au sens ML) impose ses noms et symboles. Ex:

  Require Arith.  (* + est l'addition sur les naturels *)
  Require ZArith. (* + devient l'addition sur les entiers relatifs mais
                     l'addition sur N reste accessible par Arith.+ *)

  Contraintes : 

  - les expressions style Arith.+ doivent �tre reconnues par
  l'analyseur lexicale (sinon la grammaire n'est plus LL1). Pour
  garder le "." dans le pour tout, on pourrait adopter ce principe: un
  "." imm�diatement suivi d'une lettre doit �tre compris comme un
  acc�s qualifi� et le "." se diff�rencie par le fait qu'il serait
  suivi d'un blanc, ce qui est conforme � la typographie usuelle.

  cf aussi E

  D2) Chaque module exporte 2 notations, "+" et une autre (typiquement
  "+_N" pour les naturels, "+_Z" pour les entiers relatifs, ...).
  Le dernier module "ouvert" impose son "+" mais les autres restent
  accessibles par le symbole index�.

  Cette option requiert des symboles mixtes (cf H)

  D3) ...

  Remarque suppl�mentaire sur les constantes num�riques: si on ne
  choisit pas l'option D1 (qualification style N.1), on doit pouvoir les
  mettre dans "positive" par d�faut et jouer avec les coercions pour
  qu'elles atterissent dans le type attendu (N, Z, ...).


E) Constructeurs de type de donn�es

  Propositions: utilisation de ** pour prod et ++ pour sum, rien pour
sumor et sumbool (qui pourrait �tre renomm� "dec" ou "decidable").

  Quid de sig ?


F) Egalit� et existentielle

  Consensus pour fusionner = et ==, c�d que = d�note eqT (c�d l'actuel ==)
et que la notation == disparaisse. La cumulativit� assure la compatibilit�.

  Mieux, id�e � explorer que = d�note l'�galit� de John Major. Tenants
et aboutissants ???

  Consensus pour avoir une existentielle unique (donc au niveau type
en jouant sur la cumulativit�). La notation serait naturellement
"? x. P x", "exists x. P x" ou "Exists x. P x".


G) Autres connecteurs

  Les choix actuels semblent convenir... (->, /\, \/ et ~) 


H) Extensibilit� de la syntaxe (tokens)

  H1) Une famille de token non extensible limit�e � l'avance,
  typiquement constitu�e des suites de symboles sp�ciaux (comme en Caml)

  Avantage : le lexeur peut �tre "camllex" (est-ce important ?)

  Inconv�nients :
    - Comment g�rer les tokens style "=_S" (cf D2)
      Dans l'option qualification des symboles (cf D1), cela pourrait 
      �tre "S.=", sinon... any ideas ?
    - Obligation de s�parer, comme dans ~~A, etc

  Rem: Les tokens compos�s uniquement de lettres, tel que "U" pour
  l'union pourrait �tre autoris�s � condition de les quoter par des � '
  �, � ` � ou � " �, ce qui d'ailleurs am�liore leur lisibilit�.

  H2) Famille de token extensible (comme en V6)
  
  Avantage : grande souplesse de choix de nouveaux symboles ce que
l'usage math�matique appr�cie


J) Extensibilit� de la syntaxe (r�gles)

  Consensus apparent pour limiter l'usage de Grammar et Syntax. Comme
de toutes fa�ons se sont essentiellement des infixes, ainsi que quelques
pr�fixes, postfixes et distfixes dont on a besoin !

  Prendre soin des combinaisons pr�c�dence/associativit� pour les
symboles � la fois pr�fixe/postfixe et infixe comme le "-".


K) Variables existentielles

  Si "?" est pris pour l'existentielle, "_", "_1", ... pourrait convenir.


L) Arguments implicites

  L1) Proposition (HH) d'unifier la notation "1!a" des arguments
implicites avec celle du "with" de Apply, et celle de "Intros Until",
sous une forme "f a b c with x:=d, 2:=H".

  Les index d�signeraient alors les arguments non nomm�s (qu'ils
soient implicites ou non).

  L2) Si "!" est pris pour le produit, "1!c" pourrait devenir "@1:=c"
  ou quelque chose comme cela.


M) Point fixe

  Quelques id�es... sachant que le cas est rare et que l'effort doit
porter d'abord sur Fixpoint.

  M1) "(let f a (b:B) c = ... and g d e f : A = ... in f) u v"
  M2) "(fun f a (b:B) c = ... and {h} x y = ... and g d e f = ...) u v"
    (ici, accolades pour dire que c'est h qui est projet�)
  M3) "(fix f where f a (b:B) c := ... and ... g d e f : A = ...) u v"

  + d�tection automatique des arguments gard�s et mention optionnelle
  du type r�sultat.


N) Filtrage

  N1) sans contrainte :

      "match t with p1 => t1 | ... | pn => tn end" 

  et pas de parenth�ses autour des pattern si pas autour de l'application

  N2) avec contrainte :

      "match t as x : I p1 .. pn y1 .. yq => T with
         p1 => t1
       | ...
       | pn => tn
       end" 

  N3) multiple

      "match t1, .., tq with
         p11, .., p1q => t1
       | .. 
       | pn1, .., pnq => tn
       end" 

  Probl�me avec le choix de la virgule : conflit avec la notation
  primitive des n-uplets si ceux-ci ne sont pas entour�es par des
  parenth�ses.

  Alternative : s�paration avec un "&" (pas d'ambigu�t� avec les
  paires) mais r�quisitionne le symbole, et pas tr�s standard (sauf
  latex...), quoique le symbole est intuitif.

  N4) multiple avec contrainte

      "match t1 as x : I p1 .. pn y1 .. yq, .., tq as ... => T with
         p11, .., p1q => t1
       | .. 
       | pn1, .., pnq => tn
       end"  

  Alternatives: case, cases, ...


II) Gallina

A) Terminateur de phrase

  Le "." �tant appr�ci� pour le pour tout, il conviendrait d'en
changer (pour la qualification on peut vivre avec en suivant le
principe mentionn� en I-D1).

  A1) ";;"

  Deux symboles donc peu d'interf�rence avec le reste, coh�rence avec
  caml, mais assez lourd
 
  A2) ";" 

  L�ger, comme en SML, mais oblige � changer la syntaxe du THEN
  (alternatives "," ou "THEN"), des records (alternative ",") et
  interdit dans le ";" dans les lieurs (I-A3a3 et I-A3b3).

B) Records

C) Point fixe (cf I-M)

  C1) "Fixpoint f a (b:B) c := ... and g d e f : A := ... ."
  C2) "Fixpoint f a (b:B) c := ... with g d e f : A := ... ."



III) Tactiques

Questions ouvertes :

- Incompatibilit� de prendre en compte dans ltad des arguments
  num�riques en conflit avec des ident, comme dans "Unfold 1 3 plus".

  Suggestion : "Unfold [1 3] plus".

- La syntaxe "Pattern -2 -1 x" est-elle claire ? Le "-" voulant dire
  sauf et non en partant de la fin.

  Suggestion de CP : on r��crit le but avec des _ � la place des occurrences
  souhait�es.

IV) Vernac

Mots-cles Variables/Hypotheses/Parameters ? Si oui, pourquoi pas Axioms ?

Int�grer Eval In � Constr ? Oui, mais avec une syntax plus l�g�re
Ou alors standardiser
Definition_kind id params := red_expr c : t.

Int�grer "with_binding" � Constr !

Faut-il s�parer command/gallina/gallina_ext/syntax, sachant que si
l'on s�pare, alors il ne faut plus partager de premier mot-cl� (ex:
Add et Print seront r�serv� pour command) ?

Virer theorem_body_line ?

Virer le Mutual old syntax ! Et m�me implanter le future style de
Christine avec param�tres engendr�s automatiquement et propre � chaque inductif

Scheme est-il Gallina ou pas ?
Require est-il gallina_ext ou commande ? Et faut-il garder specif ?
Utilite de RequireFrom ?

Faire des qualid un token ?

EVAL et CONTEXT dans constr: partout ou seulement en tete ?
Supprimer Specialize, supprimer with c (sans nom)

Ltac impose que "?" soit utilisable l� o� un identificateur ou un nom
long est attendu (p.ex. dans Clear). Accepte-t-on le principe ?

V) Biblioth�que standard

Zcompare_EGAL -> Zcompare_EQUAL