Review changes #2

Author: jfehrle

doc/sphinx/addendum/generalized-rewriting.rst

@@ -713,13 +713,11 @@ Definitions
 ~~~~~~~~~~~
 
 The generalized rewriting tactic is based on a set of strategies that can be
-combined to obtain custom rewriting procedures. Its set of strategies is based
+combined to create custom rewriting procedures. Its set of strategies is based
 on the programmable rewriting strategies with generic traversals by Visser et al.
 :cite:`Luttik97specificationof` :cite:`Visser98`, which formed the core of
 the Stratego transformation language :cite:`Visser01`. Rewriting strategies
-are applied using the tactic :n:`rewrite_strat @rewstrategy` where :n:`@rewstrategy` is a
-strategy expression. Strategies are defined inductively as described by the
-following grammar:
+are applied using the tactic :n:`rewrite_strat @rewstrategy`.
 
 .. insertprodn rewstrategy rewstrategy
 
@@ -732,6 +730,7 @@ following grammar:
    | progress @rewstrategy
    | try @rewstrategy
    | @rewstrategy ; @rewstrategy
+   | choice @rewstrategy @rewstrategy
    | repeat @rewstrategy
    | any @rewstrategy
    | subterm @rewstrategy
@@ -745,10 +744,79 @@ following grammar:
    | eval @red_expr
    | fold @term1_extended
    | ( @rewstrategy )
-   | choice @rewstrategy @rewstrategy
    | old_hints @ident
 
-Actually a few of these are defined in terms of the others using a
+:n:`@term1_extended`
+   lemma, left to right
+
+:n:`<- @term1_extended`
+   lemma, right to left
+
+:n:`fail`
+   failure
+
+:n:`id`
+  identity
+
+:n:`refl`
+   reflexivity
+
+:n:`progress rewstrategy`
+   progress
+
+:n:`try rewstrategy`
+   try catch
+
+:n:`rewstrategy` ; `@rewstrategy`
+   composition
+
+:n:`choice @rewstrategy @rewstrategy`
+   left_biased_choice
+
+:n:`repeat @rewstrategy`
+   one or more
+
+:n:`any @rewstrategy`
+   zero or more
+
+:n:`subterm @rewstrategy`
+   one subterm
+
+:n:`subterms @rewstrategy`
+   all subterms
+
+:n:`innermost @rewstrategy`
+   innermost first
+
+:n:`outermost @rewstrategy`
+   outermost first
+
+:n:`bottomup @rewstrategy`
+   bottom-up
+
+:n:`topdown @rewstrategy`
+   top-down
+
+:n:`hints @ident`
+   apply hints from hint database
+
+:n:`terms {* @term1_extended }`
+   any of the terms
+
+:n:`eval @red_expr`
+   apply reduction
+
+:n:`fold @term`
+   unify
+
+:n:`( @rewstrategy )`
+   to be documented
+
+:n:`old_hints @ident`
+   to be documented
+
+
+A few of these are defined in terms of the others using a
 primitive fixpoint operator:
 
 - :n:`try @rewstrategy := choice @rewstrategy id`

doc/sphinx/addendum/implicit-coercions.rst

@@ -25,13 +25,6 @@ typed modulo insertion of appropriate coercions. We allow to write:
 Classes
 -------
 
-   .. insertprodn class class
-
-   .. prodn::
-      class ::= Funclass
-      | Sortclass
-      | @smart_global
-
 A class with :math:`n` parameters is any defined name with a type
 :n:`forall (@ident__1 : @type__1)..(@ident__n:@type__n), @sort`.  Thus a class with
 parameters is considered as a single class and not as a family of
@@ -44,7 +37,13 @@ In addition to these user-defined classes, we have two built-in classes:
   * ``Funclass``, the class of functions; its objects are all the terms with a functional
     type, i.e. of form :g:`forall x:A,B`.
 
-Formally, the syntax of classes is defined here: :n:`@class`.
+   .. insertprodn class class
+
+   .. prodn::
+      class ::= Funclass
+      | Sortclass
+      | @smart_global
+
 
 
 Coercions
@@ -188,10 +187,10 @@ Declaring Coercions
      This defines :token:`ident` just like :n:`Let @ident := @term  {? @type }`,
      and then declares :token:`ident` as a coercion between it source and its target.
 
-Assumptions can be declared as coercions.
 Use :n:`:>` before the :n:`@type` of the assumption
 to declare the assumption as a coercion.
 See :ref:`gallina-assumptions`.
+
 ..
   FIXME:
    \comindex{Variable \mbox{\rm (and coercions)}}

doc/sphinx/addendum/ring.rst

@@ -360,6 +360,7 @@ The syntax for adding a new ring is
       preliminary step for :tacn:`ring` and :tacn:`ring_simplify`. It can be used to
       transform a goal so that it is better recognized. For instance, ``S n``
       can be changed to ``plus 1 n``.
+
    :n:`postprocess [ @ltac_expr ]`
       specifies a tactic :n:`@tactic` that is applied as a final
       step for :tacn:`ring_simplify`. For instance, it can be used to undo
@@ -368,7 +369,6 @@ The syntax for adding a new ring is
    :n:`power @term1_extended [ {+ @qualid } ]`
       to be documented
 
-
    :n:`power_tac @term1_extended @ltac_expr ]`
       allows :tacn:`ring` and :tacn:`ring_simplify` to recognize
       power expressions with a constant positive integer exponent (example:

doc/sphinx/proof-engine/tactics.rst

@@ -460,14 +460,22 @@ Examples:
 Occurrence sets and occurrence clauses
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-An occurrence clause (:n:`at @occurrences`) is a modifier to some tactics that obeys the
+An occurrence clause (:n:`in @in_clause`) is a modifier to some tactics that obeys the
 following syntax:
 
-  .. insertprodn occurrences occurrences
+  .. insertprodn in_clause hypident
 
   .. prodn::
-     occurrences ::= {+ @int }
-     | @ident
+     in_clause ::= @in_clause
+     | * {? at @occs_nums }
+     | * |- {? @concl_occ }
+     | {*, @hypident_occ } |- {? @concl_occ }
+     | {*, @hypident_occ }
+     concl_occ ::= * {? at @occs_nums }
+     hypident_occ ::= @hypident {? at @occs_nums }
+     hypident ::= @ident
+     | ( type of @ident )
+     | ( value of @ident )
 
 The role of an occurrence clause is to select a set of occurrences of a term
 in a goal. In the first case, the :n:`@ident {? at {* num}}` parts indicate
@@ -1274,6 +1282,12 @@ Managing the local context
 
    .. tacv:: set (@ident := @term) in @occurrences
 
+      .. insertprodn occurrences occurrences
+
+      .. prodn::
+         occurrences ::= {+ @int }
+         | @ident
+
       This notation allows specifying which occurrences of :token:`term` have
       to be substituted in the context. The :n:`in @occurrences` clause
       is an occurrence clause whose syntax and behavior are described in

doc/tools/docgram/common.edit_mlg

@@ -807,6 +807,10 @@ record_binder: [
 | DELETE name
 ]
 
+concl_occ: [
+| OPTINREF
+]
+
 SPLICE: [
 | noedit_mode
 | command_entry

doc/tools/docgram/orderedGrammar

@@ -1648,11 +1648,25 @@ by_arg_tac: [
 in_clause: [
 | in_clause
 | "*" OPT ( "at" occs_nums )
-| "*" "|-" concl_occ
-| LIST0 hypident_occ SEP "," "|-" concl_occ
+| "*" "|-" OPT concl_occ
+| LIST0 hypident_occ SEP "," "|-" OPT concl_occ
 | LIST0 hypident_occ SEP ","
 ]
 
+concl_occ: [
+| "*" OPT ( "at" occs_nums )
+]
+
+hypident_occ: [
+| hypident OPT ( "at" occs_nums )
+]
+
+hypident: [
+| ident
+| "(" "type" "of" ident ")"
+| "(" "value" "of" ident ")"
+]
+
 as_ipat: [
 | "as" simple_intropattern
 |
@@ -1783,16 +1797,6 @@ bindings_with_parameters: [
 | "(" ident LIST0 simple_binder ":=" term ")"
 ]
 
-hypident: [
-| ident
-| "(" "type" "of" ident ")"
-| "(" "value" "of" ident ")"
-]
-
-hypident_occ: [
-| hypident OPT ( "at" occs_nums )
-]
-
 clause_dft_concl: [
 | "in" in_clause
 | OPT ( "at" occs_nums )
@@ -1810,11 +1814,6 @@ opt_clause: [
 |
 ]
 
-concl_occ: [
-| "*" OPT ( "at" occs_nums )
-|
-]
-
 in_hyp_list: [
 | "in" LIST1 ident
 |
@@ -1905,6 +1904,7 @@ rewstrategy: [
 | "progress" rewstrategy
 | "try" rewstrategy
 | rewstrategy ";" rewstrategy
+| "choice" rewstrategy rewstrategy
 | "repeat" rewstrategy
 | "any" rewstrategy
 | "subterm" rewstrategy
@@ -1918,7 +1918,6 @@ rewstrategy: [
 | "eval" red_expr
 | "fold" term1_extended
 | "(" rewstrategy ")"
-| "choice" rewstrategy rewstrategy
 | "old_hints" ident
 ]