- partial implementation of pattern for case documented

- notation partially documented
- omitting the precedence level in a notation declaration is no longer allowed

diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index 6ce615091a5203602f6195221d48e2b0b62f4911..18c30d4ecbddcfa141c229131223d6c8149f3761 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -55,7 +55,6 @@ let statement = Grammar.Entry.create grammar "statement"
 
 let add_raw_attribute ~text t = Ast.AttributedTerm (`Raw text, t)
 
-let default_precedence = 50
 let default_associativity = Gramext.NonA
         
 let mk_rec_corec ind_kind defs loc = 
@@ -575,7 +574,7 @@ EXTEND
   ];
   notation: [
     [ dir = OPT direction; s = QSTRING;
-      assoc = OPT associativity; prec = OPT precedence;
+      assoc = OPT associativity; prec = precedence;
       IDENT "for";
       p2 = 
         [ blob = UNPARSED_AST ->
@@ -592,11 +591,6 @@ EXTEND
             | None -> default_associativity
             | Some assoc -> assoc
           in
-          let prec =
-            match prec with
-            | None -> default_precedence
-            | Some prec -> prec
-          in
           let p1 =
             add_raw_attribute ~text:s
               (CicNotationParser.parse_level1_pattern

diff --git a/helm/software/matita/help/C/matita.xml b/helm/software/matita/help/C/matita.xml
index cb94d108cd9e8d69b768d8b65d033cce80d710d4..21dd9bc7ba44204d3fee272b22484744998f9c48 100644 (file)
--- a/helm/software/matita/help/C/matita.xml
+++ b/helm/software/matita/help/C/matita.xml
@@ -58,6 +58,10 @@
   <!ENTITY interpretation_argument "<emphasis><link linkend='grammar.interpretation_argument'>interpretation_argument</link></emphasis>">
   <!ENTITY interpretation_rhs "<emphasis><link linkend='grammar.interpretation_rhs'>interpretation_rhs</link></emphasis>">
   <!ENTITY csymbol "<emphasis><link linkend='grammar.csymbol'>csymbol</link></emphasis>">
+  <!ENTITY usage "<emphasis><link linkend='grammar.usage'>usage</link></emphasis>">
+  <!ENTITY notation_lhs "<emphasis><link linkend='grammar.notation_lhs'>notation_lhs</link></emphasis>">
+  <!ENTITY notation_rhs "<emphasis><link linkend='grammar.notation_rhs'>notation_rhs</link></emphasis>">
+  <!ENTITY associativity "<emphasis><link linkend='grammar.associativity'>associativity</link></emphasis>">
 ]>
 
 <?yelp:chunk-depth 3?>

diff --git a/helm/software/matita/help/C/sec_tactics.xml b/helm/software/matita/help/C/sec_tactics.xml
index 0205ce8a896f286f0f75154f2eaa4764c9c85ebb..ebd100a26c408c5a242e0b87d221d43838e78692 100644 (file)
--- a/helm/software/matita/help/C/sec_tactics.xml
+++ b/helm/software/matita/help/C/sec_tactics.xml
@@ -221,7 +221,7 @@
     <title>cases</title>
     <titleabbrev>cases</titleabbrev>
     <para><userinput>
-     cases t hyps
+     cases t pattern hyps
     </userinput></para>
     <para>
       <variablelist>
@@ -230,7 +230,7 @@
           <listitem>
             <para>
             <emphasis role="bold">cases</emphasis>
-            &term; [<emphasis role="bold">(</emphasis>[&id;]…<emphasis role="bold">)</emphasis>]
+            &term; &pattern; [<emphasis role="bold">(</emphasis>[&id;]…<emphasis role="bold">)</emphasis>]
            </para>
           </listitem>
         </varlistentry>
@@ -249,6 +249,12 @@
             It proceed by cases on <command>t</command>. The new generated
              hypothesis in each branch are named according to
              <command>hyps</command>.
+             The elimintation predicate is restricted by
+             <command>pattern</command>. In particular, if some hypothesis
+             is listed in <command>pattern</command>, the hypothesis is
+             generalized and cleared before proceeding by cases on
+             <command>t</command>. Currently, we only support patterns of the
+             form <command>H<subscript>1</subscript> … H<subscript>n</subscript> ⊢ %</command>. This limitation will be lifted in the future.
            </para>
           </listitem>
         </varlistentry>

diff --git a/helm/software/matita/help/C/sec_usernotation.xml b/helm/software/matita/help/C/sec_usernotation.xml
index f4b3cc4112380d01948a31c6d24b110324ade597..46bf146c97d684bafb5c180a9fd648917484ac02 100644 (file)
--- a/helm/software/matita/help/C/sec_usernotation.xml
+++ b/helm/software/matita/help/C/sec_usernotation.xml
@@ -2,12 +2,132 @@
 <!-- ============ User Notation ====================== -->
 <chapter id="sec_usernotation">
  <title>Extending the syntax</title>
-  Introduction: TODO
+  Introduction: &TODO;
  <sect1>
   <title>notation</title>
   <titleabbrev>notation</titleabbrev>
+   <para><userinput>notation usage &quot;presentation&quot; associativity with precedence p for content</userinput></para>
   <para id="notation">
-    notation: &TODO;
+    <variablelist>
+      <varlistentry role="tactic.synopsis">
+        <term>Synopsis:</term>
+        <listitem>
+          <para><emphasis role="bold">notation</emphasis>
+           [&usage;] <emphasis role="bold">&quot;</emphasis>&notation_lhs;<emphasis role="bold">&quot;</emphasis> [&associativity;] <emphasis role="bold">with</emphasis> <emphasis role="bold">precedence</emphasis> &nat;
+           <emphasis role="bold">for</emphasis>
+           &notation_rhs;
+          </para>
+        </listitem>
+      </varlistentry>
+      <varlistentry>
+       <term>Action:</term>
+       <listitem>
+         <para>Declares a mapping between the presentation
+          AST <command>presentation</command> and the content AST
+          <command>content</command>. The declared presentation AST fragment
+          <command>presentation</command> is at precedence level
+          <command>p</command>. The precedence level is used to determine where
+          parentheses must be inserted. In particular, the content AST fragment
+          <command>content</command> is actually a pattern, since it contains
+          placeholders (variables) for sub-ASTs. Every placeholder for a term
+          is given an expected precedence level. Parentheses must be inserted
+          around sub-ASTs having a precedence level strictly smaller than the
+          expected one.</para>
+          <para>If <command>presentation</command> describes a binary
+          infix operator and if no precedence level is explicitly given for the
+          operator arguments, an <command>associativity</command> declaration
+          can be given to automatically choose the right level for the operands.
+          Otherwise, no <command>associativity</command> can be given.</para>
+         <para>If <command>direction</command> is
+          omitted, the mapping is bi-directional and is used both during
+          parsing and pretty-printing of terms. If <command>direction</command>
+          is <command>&gt;</command>, the mapping is used only during parsing;
+          if it is <command>&lt;</command>, it is used only during
+          pretty-printing. Thus it is possible to use simple notations to type
+          for writing the term, and nicer ones for rendering it.</para>
+       </listitem>
+      </varlistentry>
+      <varlistentry>
+        <term>Notation arguments:</term>
+        <listitem>
+
+    <table frame="topbot" rowsep="0" colsep="0" role="grammar">
+      <title>usage</title>
+      <tgroup cols="4">
+      <tbody>
+       <row>
+        <entry id="grammar.usage">&usage;</entry>
+        <entry>::=</entry>
+        <entry><emphasis role="bold">&lt;</emphasis></entry>
+        <entry>Only for pretty-printing</entry>
+       </row>
+       <row>
+        <entry/>
+        <entry>|</entry>
+        <entry><emphasis role="bold">&gt;</emphasis></entry>
+        <entry>Only for parsing</entry>
+       </row>
+      </tbody>
+      </tgroup>
+     </table>
+
+    <table frame="topbot" rowsep="0" colsep="0" role="grammar">
+      <title>associativity</title>
+      <tgroup cols="4">
+      <tbody>
+       <row>
+        <entry id="grammar.associativity">&associativity;</entry>
+        <entry>::=</entry>
+        <entry><emphasis role="bold">left</emphasis> <emphasis role="bold">associative</emphasis></entry>
+        <entry>Left associative</entry>
+       </row>
+       <row>
+        <entry/>
+        <entry>|</entry>
+        <entry><emphasis role="bold">left</emphasis> <emphasis role="bold">associative</emphasis></entry>
+        <entry>Right associative</entry>
+       </row>
+       <row>
+        <entry/>
+        <entry>|</entry>
+        <entry><emphasis role="bold">non</emphasis> <emphasis role="bold">associative</emphasis></entry>
+        <entry>Non associative (default)</entry>
+       </row>
+      </tbody>
+      </tgroup>
+     </table>
+
+    <table frame="topbot" rowsep="0" colsep="0" role="grammar">
+      <title>notation_rhs</title>
+      <tgroup cols="4">
+      <tbody>
+       <row>
+        <entry id="grammar.notation_rhs">&notation_rhs;</entry>
+        <entry>::=</entry>
+        <entry>&TODO;</entry>
+        <entry>&TODO;</entry>
+       </row>
+      </tbody>
+      </tgroup>
+     </table>
+
+    <table frame="topbot" rowsep="0" colsep="0" role="grammar">
+      <title>notation_lhs</title>
+      <tgroup cols="4">
+      <tbody>
+       <row>
+        <entry id="grammar.notation_lhs">&notation_lhs;</entry>
+        <entry>::=</entry>
+        <entry>&TODO;</entry>
+        <entry>&TODO;</entry>
+       </row>
+      </tbody>
+      </tgroup>
+     </table>
+
+        </listitem>
+      </varlistentry>
+    </variablelist>
   </para>
  </sect1>
  <sect1>
@@ -22,7 +142,7 @@
         <listitem>
           <para><emphasis role="bold">interpretation</emphasis>
            &qstring; &csymbol; [&interpretation_argument;]…
-           <emphasis role="bol">=</emphasis>
+           <emphasis role="bold">=</emphasis>
            &interpretation_rhs;
           </para>
         </listitem>

diff --git a/helm/software/matita/help/C/tactics_quickref.xml b/helm/software/matita/help/C/tactics_quickref.xml
index ba7020c10247d40ddf1136c90f87511ca05a45cb..c7a789c1a32ed246648eb8577e80afb34aa77862 100644 (file)
--- a/helm/software/matita/help/C/tactics_quickref.xml
+++ b/helm/software/matita/help/C/tactics_quickref.xml
@@ -36,7 +36,7 @@
         <entry>|</entry>
         <entry>
             <link linkend="tac_cases"><emphasis role="bold">cases</emphasis></link>
-            <emphasis><link linkend="grammar.term">term</link></emphasis> [<emphasis role="bold">(</emphasis>[<emphasis><link linkend="grammar.id">id</link></emphasis>]…<emphasis role="bold">)</emphasis>]
+            <emphasis><link linkend="grammar.term">term</link></emphasis> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis> [<emphasis role="bold">(</emphasis>[<emphasis><link linkend="grammar.id">id</link></emphasis>]…<emphasis role="bold">)</emphasis>]
            </entry>
       </row>
       <row>