path: root/dev/translate.txt

  Some hints for translation (DRAFT):

I) Implicit Arguments
   ------------------

1) Strict Implicit Arguments 

  "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

  Set Implicit Arguments.
  Unset Strict Implicits.

  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.

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:

  <-> : 80              (left associativity)
  \/ : 70               (right associativity)
  /\ : 60               (right associativity)
  ~ : 55                (right associativity)
  =, <=, >=, <> : 50    (no associativity)
  +, - : 40             (left associativity)
  *, / : 30             (left associativity)

  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.:

   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).

  The semantics of V8only is:

  - Without V8only, the associativity is as for V7 and the levels are
  the V7 levels scaled by 10.

  - 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.

  - Otherwise, both associativity and levels must be mentioned after
  the V8only keyword

  Notice that you can also change the syntax itself.

III) Main examples for new syntax
     ----------------------------

1) Constructions

  Applicative terms don't any longer require to be surrounded by parentheses as
e.g in

  "x = f y -> S x = S (f y)"


  Product is written

     "forall x y : T, U"
     "forall x y, U"
     "forall (x y : T) z (v w : V), U"
     etc.

  Abstraction is written

     "fun x y : T, U"
     "fun x y, U"
     "fun (x y : T) z (v w : V), U"
     etc.

  Pattern-matching is written

     "match x with c1 x1 x2 => t | c2 y as z => u end"
     "match v1, v2 with c1 x1 x2, _ => t | c2 y, d z => u end"
     "match v1 as y in le _ n, v2 as z in I p q return P n y p q z with
         c1 x1 x2, _ => t | c2 y, d z => u end"

     The last example is the new form of what was written

    "<[n;y:(le ? n);p;q;z:(I p q)](P n y p q z)>Cases v1 v2 of
         (c1 x1 x2) _ => t | (c2 y) (d z) => u end"

  Pattern-matching of type with one constructors and no dependencies
of the arguments in the resulting type can be written

    "let (x,y,z) as u return P u := t in v"
     
  Local fixpoints are written

    "fix f (n m:nat) z (x : X) {struct m} : nat := ...
     with ..."

    and "struct" tells which argument is structurally decreasing.

  Explicitation of implicit arguments is written

     "f @1:=u v @3:=w t"
     "@f u v w t"

2) Tactics

  The main change is that tactics names are now lowercase. Besides
this, the following renaming are applied:

  "NewDestruct" -> "destruct"
  "NewInduction" -> "induction"
  "Induction" -> "oldinduction"
  "Destruct" -> "olddestruct"

  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"

3) Tactic language

  Definitions are now introduced with keyword "Ltac" (instead of
"Tactic"/"Meta" "Definition") and are implicitly recursive
("Recursive" is no longer used).

  The new rule for simple quotes is:

  "Quote any tactic in argument position and any construction in head position"

4) Vernacular language

a) Assumptions

  The syntax for commands is mainly unchanged. Declaration of
assumptions is now done as follows

  Variable m : t.
  Variables m n p : t.
  Variables (m n : t) (u v : s) (w : r).
  
b) Definitions

  Definitions are done as follows

  Definition f m n : t := ... .
  Definition f m n := ... .
  Definition f m n := ... : t.
  Definition f (m n : u) : t := ... .
  Definition f (m n : u) := ... : t.
  Definition f (m n : u) := ... .
  Definition f a b (p q : v) r s (m n : t) : t := ... .
  Definition f a b (p q : v) r s (m n : t) := ... .
  Definition f a b (p q : v) r s (m n : t) := ... : t.

c) Fixpoints

  Fixpoints are done this way
  
  Fixpoint f x (y : t) z a (b c : u) {struct z} : v := ... with ... .
  Fixpoint f x : v := ... .
  Fixpoint f (x : t) : v := ... .

  It is possible to give a concrete notation to a fixpoint as follows

  Fixpoint plus (n m:nat) {struct n} : nat as "n + m" :=
    match n with
    | O => m
    | S p => S (p + m)
    end.

d) Inductive types

  The syntax for inductive types is as follows

  Inductive t (a b : u) (d : e) : v :=
     c1 : w1 | c2 : w2 | ... .

  Inductive t (a b : u) (d : e) : v :=
     c1 : w1 | c2 : w2 | ... .

  Inductive t (a b : u) (d : e) : v :=
     c1 (x y : t) : w1 | c2 (z : r) : w2 | ... .

  As seen in the last example, arguments of the constructors can be
given before the colon. If the type itself is omitted (allowed only in
case the inductive type has no real arguments), this yields an
ML-style notation as follows

  Inductive nat : Set := O | S (n:nat).
  Inductive bool : Set := true | false.

  It is even possible to define a syntax at the same time, as follows:

  Inductive or (A B:Prop) : Prop as "A \/ B":=
    | or_introl (a:A) : A \/ B 
    | or_intror (b:B) : A \/ B.

  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].