Les projets de syntaxe

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8161 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 255 insertions, 0 deletions

diff --git a/doc/discussion-syntaxe.txt b/doc/discussion-syntaxe.txt
new file mode 100644
index 0000000000..086f34fab3
--- /dev/null
+++ b/doc/discussion-syntaxe.txt
@@ -0,0 +1,255 @@
+
+  Synthèse des différentes propositions de "rénovation" de la syntaxe de Coq
+  --------------------------------------------------------------------------
+
+I) Constructions
+
+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.
+
+
+
+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
+