diff options
Diffstat (limited to 'doc/discussion-syntaxe.txt')
| -rw-r--r-- | doc/discussion-syntaxe.txt | 349 |
1 files changed, 0 insertions, 349 deletions
diff --git a/doc/discussion-syntaxe.txt b/doc/discussion-syntaxe.txt deleted file mode 100644 index 658c67c72..000000000 --- a/doc/discussion-syntaxe.txt +++ /dev/null @@ -1,349 +0,0 @@ - - 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 |