1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
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
|
