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