MAJ

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

1 files changed, 297 insertions, 84 deletions

diff --git a/dev/translate.txt b/dev/translate.txt
index 9dfe9ca1bb..a7d9aabdef 100644
--- a/dev/translate.txt
+++ b/dev/translate.txt
@@ -1,32 +1,72 @@
 
-  Some hints for translation (DRAFT):
+                 How to use the translator
+                 =========================
+
+       (temporary version to be included in the official
+           TeX document describing the translator)
+
+The translator is a smart, robust and powerful tool to improve the
+readibility of your script. The current document describes the
+possibilities of the translator.
+
+I) Implicit Arguments
+ 1) Strict Implicit Arguments 
+ 2) Implicit Arguments in standard library
+
+II) Notations
+ 1) Translating a V7 notation as it was
+ 2) Translating a V7 notation which conflicts with the new syntax
+  a) Associativity conflicts
+  b) Conflicts with other notations
+   b1) A notation hides another notation 
+   b2) A notation conflicts with the V8 grammar
+   b3) My notation is already defined at another level
+  c) How to use V8only with Distfix ?
+  d) Can I overload a notation in V8, e.g. use "*" and "+" ?
+ 3) Using the translator to have simplest notations
+ 4) Setting the translator to automatically use new notations that
+    wasn't used in old syntax
+ 5) Defining a construction and its notation simultaneously
+
+III) Various pitfalls
+ 1) New keywords
+ 2) Old "Case" and "Match"
+ 3) Change of definition or theorem names
+
+---------------------------------------------------------------------
 
 I) Implicit Arguments
    ------------------
 
 1) Strict Implicit Arguments 
 
-  "Set Implicit Arguments" changes its meaning in v8: the default is
+  "Set Implicit Arguments" changes its meaning in V8: the default is
 to turn implicit only the arguments that are _strictly_ implicit (or
 rigid), i.e. that remains inferable whatever the other arguments
 are. E.g "x" inferable from "P x" is not strictly inferable since it
 can disappears if "P" is instanciated by a term which erase "x".
 
-  If you really wish to keep the old meaning of "Set Implicit
-Arguments", you have to replace every occurrence of it by
+  To respect the old semantics, the default behaviour of the
+translator is to replace each occurrence "Set Implicit Arguments" by
 
   Set Implicit Arguments.
   Unset Strict Implicits.
 
-  Warning: Changing the number of implicit arguments can break the notations.
-Then use the V8only modifier of Notations.
+  However, you may wish to adopt the new semantics of "Set Implicit
+Arguments" (for instance because you think that the choice of
+arguments it setsimplicit is more "natural" for you). In this case,
+add the option -strict-implicit to the translator.
+
+  Warning: Changing the number of implicit arguments can break the
+notations.  Then use the V8only modifier of Notations.
 
 2) Implicit Arguments in standard library
 
   Main definitions of standard library have now implicit
 arguments. These arguments are dropped in the translated files. This
 can exceptionally be a source of incompatibilities which has to be
-solved by hand.
+solved by hand (it typically happens for polymorphic functions applied
+to "nil" or "None").
 
 II) Notations
     ---------
@@ -34,44 +74,257 @@ II) Notations
   Grammar (on constr) and Syntax are no longer supported. Replace them by
 Notation before translation.
 
-  Precedence levels are now from 0 to 250. In V8, the precedence and
-associativity of an operator cannot be redefined. Typical level are:
+  Precedence levels are now from 0 to 200. In V8, the precedence and
+associativity of an operator cannot be redefined. Typical level are
+(refer to the chapter on notations in the Reference Manual for the
+full list):
+
+  <-> : 95                    (no associativity)
+  -> : 90                     (right associativity)
+  \/ : 85                     (right associativity)
+  /\ : 80                     (right associativity)
+  ~ : 75                      (right associativity)
+  =, <, >, <=, >=, <> : 70    (no associativity)
+  +, - : 50                   (left associativity)
+  *, / : 40                   (left associativity)
+  ^ : 30                      (right associativity)
+
+1) Translating a V7 notation as it was
+
+  By default, the translator keeps the associativity given in V7 while
+the levels are mapped according to the following table:
+ 
+  the V7 levels             [  0;  1;  2;  3;  4;  5;  6;  7;  8;  9;  10]
+  are resp. mapped in V8 to [  0; 20; 30; 40; 50; 70; 80; 85; 90; 95; 100]
+  with predefined assoc     [ No;  L;  R;  L;  L; No;  R;  R;  R; No;   L]
+
+  If this is OK for you, just simply apply the translator.
+
+2) Translating a V7 notation which conflicts with the new syntax
+
+a) Associativity conflict
+
+  Since the associativity of the levels obtained by translating a V7
+level (as shown on table above) cannot be changed, you have to choose
+another level with a compatible associativity.
+
+  You can choose any level between 0 and 200, knowing that the
+standard operators are already set at the levels shown on the list
+above. 
+
+Example 1: Assume you have a notation
+
+Infix NONA 2 "=_S" my_setoid_eq.
+
+By default, the translator moves it to level 30 which is right
+associative, hence a conflict with the expected no associativity.
+
+To solve the problem, just add the "V8only" modifier to reset the
+level and enforce the associativity as follows:
+
+Infix NONA 2 "=_S" my_setoid_eq V8only (at level 70, no associativity).
+
+The translator now knows that it has to translate "=_S" at level 70
+with no associativity.
+
+Rem: 70 is the "natural" level for relations, hence the choice of 70
+here, but any other level accepting a no-associativity would have been
+OK.
+
+Example 2: Assume you have a notation
+
+Infix RIGHTA 1 "o" my_comp.
+
+By default, the translator moves it to level 20 which is left
+associative, hence a conflict with the expected right associativity.
+
+To solve the problem, just add the "V8only" modifier to reset the
+level and enforce the associativity as follows:
+
+Infix RIGHTA 1 "o" my_comp V8only (at level 20, right associativity).
+
+The translator now knows that it has to translate "o" at level 20
+which has the correct "right associativity".
+
+Rem: We assumed here that the user wants a strong precedence for
+composition, in such a way, say, that "f o g + h" is parsed as
+"(f o g) + h". To get "o" binding less than the arithmetical operators,
+an appropriated level would have been close of 70, and below, e.g. 65.
+
+b) Conflicts with other notations
+
+Since the new syntax comes with new keywords and new predefined
+symbols, new conflicts can occur. Again, you can use the option V8only
+to inform the translator of the new syntax to use.
+
+b1) A notation hides another notation 
+
+Rem: use Print Grammar constr in V8 to diagnose the overlap and see the
+section on factorization in the chapter on notations of the Reference
+Manual for hints on how to factorize.
+
+Example:
+
+Notation "{ x }" := (my_embedding x) (at level 1).
+
+overlaps in V8 with notation "{ x : A & P }" at level 0 and with x at
+level 99. The conflicts can be solved by left-factorizing the notation
+as follows:
+
+Notation "{ x }" := (my_embedding x) (at level 1)
+  V8only (at level 0, x at level 99).
+
+b2) A notation conflicts with the V8 grammar.
+
+Again, use the V8only modifier to tell the translator to automatically
+take in charge the new syntax.
+
+Example:
+
+Infix 3 "@" app.
+
+Since "@" is used in the new syntax for deactivating the implicit
+arguments, another symbol has to be used, e.g. "@@". This is done via
+the V8only option as follows:
+
+Infix 3 "@" app V8only "@@" (at level 40, left associativity).
+
+or, alternatively by
+
+Notation "x @ y" := (app x y) (at level 3, left associativity)
+  V8only "x @@ y" (at level 40, left associativity).
+
+b3) My notation is already defined at another level (or with another
+associativity)
+
+In V8, the level and associativity of a given notation can no longer
+be changed. Then, either you adopt the standard reserved levels and
+associativity for this notation (as given on the list above) or you
+change your notation.
+
+- To change the notation, follow the directions in section b2.
+
+- To adopt the standard level, just use V8only without any argument.
+
+Example.
+
+Infix 6 "*" my_mult.
+
+is not accepted as such in V8. Write
+
+Infix 6 "*" my_mult V8only.
+
+to tell the translator to use "*" at the reserved level (i.e. 40 with
+left associativity). Even better, use interpretation scopes (look at
+the Reference Manual).
+
+c) How to use V8only with Distfix ?
+
+You can't, use Notation instead of Distfix.
+
+d) Can I overload a notation in V8, e.g. use "*" and "+" for my own
+algebraic operations ?
+
+Yes, using interpretation scopes (see the corresponding chapter in the
+Reference Manual).
+
+3) Using the translator to have simplest notations
+
+Thanks to the new syntax, * has now the expected left associativity,
+and the symbols <, >, <= and >= are now available.
+
+Thanks to the interpretation scopes, you can overload the
+interpretation of these operators with the default interpretation
+provided in Coq.
+
+This may be a motivation to use the translator to automatically change
+the notations while switching to the new syntax.
+
+See sections b) and d) above for examples.
+
+4) Setting the translator to automatically use new notations that
+wasn't used in old syntax
+
+Thanks to the "Notation" mechanism, defining symbolic notations is
+simpler than in the previous versions of Coq.
+
+Thanks to the new syntax and interpretation scopes, new symbols and
+overloading is available.
+
+This may be a motivation for using the translator to automatically change
+the notations while switching to the new syntax.
 
-  <-> : 80              (left associativity)
-  \/ : 70               (right associativity)
-  /\ : 60               (right associativity)
-  ~ : 55                (right associativity)
-  =, <=, >=, <> : 50    (no associativity)
-  +, - : 40             (left associativity)
-  *, / : 30             (left associativity)
+Use for that the commands V8Notation and V8Infix.
 
-  The new scale can induce incompatibilities. To set the level an
-operator should have after translation, use the V8only modifier of
-Infix or Notation in the v7 file (V8only is not supported for Distfix,
-use Notation instead), as e.g.:
+Examples:
 
-   Infix 6 "<=" le V8only (at level 50, no associativity).
-   Notation "( x , y )" := (pair ? ? x y)  V8only "x , y" (at level 0).
-   Infix 3 "*" mult : nat_scope  V8only (at level 30, left associativity).
+V8Infix "==>" my_relation (at level 65, right associativity).
 
-  The semantics of V8only is:
+tells the translator to write an infix "==>" instead of my_relation in
+the translated files.
 
-  - Without V8only, the associativity is as for V7 and the levels are
-  the V7 levels scaled by 10.
+V8Infix ">=" my_ge.
 
-  - If the syntactic parameters of the notation are already defined
-  (e.g. in theories/Init/Notations.v), then the V8only keyword alone
-  means that the levels and associativity will be inherited from the
-  reserved ones for this syntax. No levels and associativity will be
-  mentioned in the v8 files.
+tells the translator to write an infix ">=" instead of my_ge in the
+translated files and that the level and associativity are the standard
+one (as defined in the chart above).
 
-  - Otherwise, both associativity and levels must be mentioned after
-  the V8only keyword
+V8Infix ">=" my_ge : my_scope.
 
-  Notice that you can also change the syntax itself.
+tells the translator to write an infix ">=" instead of my_ge in the
+translated files, that the level and associativity are the standard
+one (as defined in the chart above), but only if scope my_scope is
+open or if a delimiting key is available for "my_scope" (see the
+Reference Manual).
 
-III) Main examples for new syntax
-     ----------------------------
+5) Defining a construction and its notation simultaneously
+
+This is permitted by the new syntax. Look at the Reference Manual for
+explanation. The translator is not fully able to take this in charge...
+
+III) Various pitfalls
+    ----------------
+
+1) New keywords
+
+  The following identifiers are new keywords
+
+  "forall"; "fun"; "match"; "fix"; "cofix"; "for"; "if"; "then";
+  "else"; "return"; "mod"; "at"; "let"; "_"; ".("
+
+  The translator automatically add a "_" to names clashing with a
+keyword, except for files. Hence users may need to rename the files
+whose name clashes with a keyword.
+
+  Remark: "in"; "with"; "end"; "as"; "Prop"; "Set"; "Type"
+  were already keywords
+
+2) Old "Case" and "Match"
+
+  "Case" and "Match" are normally automatically translated into
+  "match" or "match" and "fix", but sometimes it fails to do so. It
+  typically fails when the Case or Match is argument of a tactic whose
+  typing context is unknown because of a preceding Intro/Intros, as e.g. in 
+
+     Intros; Exists [m:nat](<quasiterm>Case m of t [p:nat](f m) end)
+
+  The solution is then to replace the invocation of the sequence of
+  tactics into several invocation of the elementary tactics as follows
+
+     Intros. Exists [m:nat](<quasiterm>Case m of t [p:nat](f m) end)
+          ^^^
+
+3) Change of definition or theorem names
+
+  Type "entier" from fast_integer.v is renamed into "N" by the
+translator. As a consequence, user-defined objects of same name "N"
+are systematically qualified even tough it may not be necessary.  The
+same apply for names "GREATER", "EQUAL", "LESS", etc... [COMPLETE LIST
+TO GIVE].
+
+======================================================================
+Main examples for new syntax
+----------------------------
 
 1) Constructions
 
@@ -131,15 +384,15 @@ this, the following renaming are applied:
 
   "NewDestruct" -> "destruct"
   "NewInduction" -> "induction"
-  "Induction" -> "oldinduction"
-  "Destruct" -> "olddestruct"
+  "Induction" -> "simple induction"
+  "Destruct" -> "simple destruct"
 
   For tactics with occurrences, the occurrences now comes after and
   repeated use is separated by comma as in
 
-  "Pattern 1 3 c d 4 e" -> "pattern c 3 1, d, e 4"
-  "Unfold 1 3 f 4 g" -> "unfold f 1 3, g 4"
-  "Simpl 1 3 e" -> "simpl e 1 3"
+  "Pattern 1 3 c d 4 e" -> "pattern c at 3 1, d, e at 4"
+  "Unfold 1 3 f 4 g" -> "unfold f at 1 3, g at 4"
+  "Simpl 1 3 e" -> "simpl e at 1 3"
 
 3) Tactic language
 
@@ -147,9 +400,10 @@ this, the following renaming are applied:
 "Tactic"/"Meta" "Definition") and are implicitly recursive
 ("Recursive" is no longer used).
 
-  The new rule for simple quotes is:
+  The new rule for distinguishing terms from ltac expressions is:
 
-  "Quote any tactic in argument position and any construction in head position"
+  Write "ltac:" in front of any tactic in argument position and
+  "constr:" in front of any construction in head position
 
 4) Vernacular language
 
@@ -221,44 +475,3 @@ ML-style notation as follows
 
   Inductive and (A B:Prop) : Prop as "A /\ B" := conj (a:A) (b:B).
   
-IV) Various pitfalls
-    ----------------
-
-1) New keywords
-
-  The following identifiers are new keywords
-
-  "forall"; "fun"; "match"; "fix"; "cofix"; "for"; "if"; "then";
-  "else"; "return"; "mod"
-
-  The translator automatically add a "_" to names clashing with a
-keyword, except for files. Hence users may need to rename the files
-whose name clashes with a keyword.
-
-  Remark: "in"; "with"; "end"; "as"; "let"; "Prop"; "Set"; "Type"
-  where already keywords
-
-2) Old "Case" and "Match"
-
-  "Case" and "Match" are normally automatically translated into
-  "match" or "match" and "fix", but sometimes it fails to do so. It
-  typically fails when the Case or Match is argument of a tactic whose
-  typing context is unknown because of a preceding Intro/Intros, as e.g. in 
-
-     Intros; Exists [m:nat](<quasiterm>Case m of t [p:nat](f m) end)
-
-  The solution is then to replace the invocation of the sequence of
-  tactics into several invocation of the elementary tactics as follows
-
-     Intros. Exists [m:nat](<quasiterm>Case m of t [p:nat](f m) end)
-          ^^^
-
-3) Renamed constructions
-
-  Type "entier" from fast_integer.v is renamed into "N" by the
-translator. As a consequence, user-defined objects of same name "N"
-can be hidden by the new "N" if the "Require ZArith" is not done soon
-enough. The solution is to move the "Require ZArith" before users
-modules. The same apply for names "GREATER", "EQUAL", "LESS",
-etc... [COMPLETE LIST TO GIVE].
-