From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 9 Oct 2006 17:48:45 +0000 (+0000)
Subject: applyS now receives the same parameters that auto receives.
X-Git-Tag: 0.4.95@7852~918
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=76917216be769918258c90e486bb7c06d81b70b4;p=helm.git

applyS now receives the same parameters that auto receives.
The parameters are not used yet.
---

diff --git a/components/grafite/grafiteAst.ml b/components/grafite/grafiteAst.ml
index e4b2cf24d..8816f2efa 100644
--- a/components/grafite/grafiteAst.ml
+++ b/components/grafite/grafiteAst.ml
@@ -46,7 +46,7 @@ type 'lazy_term reduction =
 type ('term, 'lazy_term, 'reduction, 'ident) tactic =
   | Absurd of loc * 'term
   | Apply of loc * 'term
-  | ApplyS of loc * 'term
+  | ApplyS of loc * 'term * (string * string) list
   | Assumption of loc
   | Auto of loc * (string * string) list
   | Change of loc * ('term, 'lazy_term, 'ident) pattern * 'lazy_term
diff --git a/components/grafite/grafiteAstPp.ml b/components/grafite/grafiteAstPp.ml
index 5644d33d3..13a4690dd 100644
--- a/components/grafite/grafiteAstPp.ml
+++ b/components/grafite/grafiteAstPp.ml
@@ -75,7 +75,10 @@ let rec pp_tactic ~term_pp ~lazy_term_pp =
   function
   | Absurd (_, term) -> "absurd" ^ term_pp term
   | Apply (_, term) -> "apply " ^ term_pp term
-  | ApplyS (_, term) -> "applyS " ^ term_pp term
+  | ApplyS (_, term, params) ->
+     "applyS " ^ term_pp term ^
+      String.concat " " 
+        (List.map (fun (k,v) -> if v <> "" then k ^ "=" ^ v else k) params)
   | Auto (_,params) -> "auto " ^ 
       String.concat " " 
         (List.map (fun (k,v) -> if v <> "" then k ^ "=" ^ v else k) params)
diff --git a/components/grafite_engine/grafiteEngine.ml b/components/grafite_engine/grafiteEngine.ml
index 2d0d691f1..4539029af 100644
--- a/components/grafite_engine/grafiteEngine.ml
+++ b/components/grafite_engine/grafiteEngine.ml
@@ -61,8 +61,8 @@ let tactic_of_ast ast =
   match ast with
   | GrafiteAst.Absurd (_, term) -> Tactics.absurd term
   | GrafiteAst.Apply (_, term) -> Tactics.apply term
-  | GrafiteAst.ApplyS (_, term) ->
-     Tactics.applyS ~term ~dbd:(LibraryDb.instance ())
+  | GrafiteAst.ApplyS (_, term, params) ->
+     Tactics.applyS ~term ~params ~dbd:(LibraryDb.instance ())
   | GrafiteAst.Assumption _ -> Tactics.assumption
   | GrafiteAst.Auto (_,params) ->
       AutoTactic.auto_tac ~params ~dbd:(LibraryDb.instance ()) 
diff --git a/components/grafite_parser/grafiteDisambiguate.ml b/components/grafite_parser/grafiteDisambiguate.ml
index 134a16895..9528d45e1 100644
--- a/components/grafite_parser/grafiteDisambiguate.ml
+++ b/components/grafite_parser/grafiteDisambiguate.ml
@@ -123,9 +123,9 @@ let disambiguate_tactic
     | GrafiteAst.Apply (loc, term) ->
         let metasenv,cic = disambiguate_term context metasenv term in
         metasenv,GrafiteAst.Apply (loc, cic)
-    | GrafiteAst.ApplyS (loc, term) ->
+    | GrafiteAst.ApplyS (loc, term, params) ->
         let metasenv,cic = disambiguate_term context metasenv term in
-        metasenv,GrafiteAst.ApplyS (loc, cic)
+        metasenv,GrafiteAst.ApplyS (loc, cic, params)
     | GrafiteAst.Assumption loc ->
         metasenv,GrafiteAst.Assumption loc
     | GrafiteAst.Auto (loc,params) ->
diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml
index 6e108ce04..af185a63e 100644
--- a/components/grafite_parser/grafiteParser.ml
+++ b/components/grafite_parser/grafiteParser.ml
@@ -133,8 +133,10 @@ EXTEND
         GrafiteAst.Absurd (loc, t)
     | IDENT "apply"; t = tactic_term ->
         GrafiteAst.Apply (loc, t)
-    | IDENT "applyS"; t = tactic_term ->
-        GrafiteAst.ApplyS (loc, t)
+    | IDENT "applyS"; t = tactic_term ; params = 
+        LIST0 [ i = IDENT -> i,"" | i = IDENT ; SYMBOL "="; v = [ v = int ->
+          string_of_int v | v = IDENT -> v ] -> i,v ] ->
+        GrafiteAst.ApplyS (loc, t, params)
     | IDENT "assumption" ->
         GrafiteAst.Assumption loc
     | IDENT "auto"; params = 
diff --git a/components/tactics/auto.ml b/components/tactics/auto.ml
index 1e99c9b64..117978d8c 100644
--- a/components/tactics/auto.ml
+++ b/components/tactics/auto.ml
@@ -533,7 +533,7 @@ let auto dbd cache context metasenv gl flags =
   | Fail s,tables,cache,maxm -> None,cache
 ;;
 
-let applyS_tac ~dbd ~term =
+let applyS_tac ~dbd ~term ~params =
  ProofEngineTypes.mk_tactic
   (fun status ->
     try 
diff --git a/components/tactics/auto.mli b/components/tactics/auto.mli
index 5883f0bf2..c9f3b9b09 100644
--- a/components/tactics/auto.mli
+++ b/components/tactics/auto.mli
@@ -42,5 +42,6 @@ val auto_all_solutions:
   AutoTypes.flags ->
     (Cic.substitution * Cic.metasenv) list * AutoCache.cache
 
-val applyS_tac: dbd:HMysql.dbd -> term: Cic.term -> ProofEngineTypes.tactic
-
+val applyS_tac:
+ dbd:HMysql.dbd -> term: Cic.term -> params:(string * string) list ->
+  ProofEngineTypes.tactic
diff --git a/components/tactics/tactics.mli b/components/tactics/tactics.mli
index c49303555..7a7d92fdc 100644
--- a/components/tactics/tactics.mli
+++ b/components/tactics/tactics.mli
@@ -1,7 +1,8 @@
 (* GENERATED FILE, DO NOT EDIT. STAMP:Thu Sep 28 10:29:58 CEST 2006 *)
 val absurd : term:Cic.term -> ProofEngineTypes.tactic
 val apply : term:Cic.term -> ProofEngineTypes.tactic
-val applyS : dbd:HMysql.dbd -> term:Cic.term -> ProofEngineTypes.tactic
+val applyS :
+  dbd:HMysql.dbd -> term:Cic.term -> params:(string * string) list -> ProofEngineTypes.tactic
 val assumption : ProofEngineTypes.tactic
 val auto :
   params:(string * string) list -> dbd:HMysql.dbd -> ProofEngineTypes.tactic
diff --git a/matita/help/C/matita.xml b/matita/help/C/matita.xml
index c3ea1da84..bb281ac67 100644
--- a/matita/help/C/matita.xml
+++ b/matita/help/C/matita.xml
@@ -48,6 +48,7 @@
   <!ENTITY LCFtactical "<emphasis><link linkend='grammar.LCFtactical'>LCF-tactical</link></emphasis>">
   <!ENTITY qstring "<emphasis><link linkend='grammar.qstring'>qstring</link></emphasis>">
   <!ENTITY interpretation "<emphasis><link linkend='grammar.interpretation'>interpretation</link></emphasis>">
+  <!ENTITY autoparams "<emphasis><link linkend='grammar.autoparams'>auto_params</link></emphasis>">
 ]>
 
 <?yelp:chunk-depth 3?>
diff --git a/matita/help/C/sec_tactics.xml b/matita/help/C/sec_tactics.xml
index 468a27695..ff8d099c0 100644
--- a/matita/help/C/sec_tactics.xml
+++ b/matita/help/C/sec_tactics.xml
@@ -89,13 +89,13 @@
   <sect1 id="tac_applyS">
     <title>applyS</title>
     <titleabbrev>applyS</titleabbrev>
-    <para><userinput>applyS t</userinput></para>
+    <para><userinput>applyS t auto_params</userinput></para>
     <para>
       <variablelist>
         <varlistentry role="tactic.synopsis">
           <term>Synopsis:</term>
           <listitem>
-            <para><emphasis role="bold">applyS</emphasis> &sterm;</para>
+            <para><emphasis role="bold">applyS</emphasis> &sterm; &autoparams;</para>
           </listitem>
         </varlistentry>
         <varlistentry>
@@ -123,6 +123,8 @@
              Then it closes the current sequent by applying
              <command>t</command> to <command>n</command>
              implicit arguments (that become new sequents).
+             The <command>auto_params</command> parameters are passed
+             directly to <command>auto paramodulation</command>.
             </para>
           </listitem>
         </varlistentry>
@@ -176,13 +178,13 @@
   <sect1 id="tac_auto">
     <title>auto</title>
     <titleabbrev>auto</titleabbrev>
-    <para><userinput>auto depth=d width=w paramodulation full</userinput></para>
+    <para><userinput>auto params</userinput></para>
     <para>
       <variablelist>
         <varlistentry role="tactic.synopsis">
           <term>Synopsis:</term>
           <listitem>
-            <para><emphasis role="bold">auto</emphasis> [<emphasis role="bold">depth=</emphasis>&nat;] [<emphasis role="bold">width=</emphasis>&nat;] [<emphasis role="bold">paramodulation</emphasis>] [<emphasis role="bold">full</emphasis>]</para>
+            <para><emphasis role="bold">auto</emphasis> &autoparams;</para>
           </listitem>
         </varlistentry>
         <varlistentry>
@@ -190,10 +192,10 @@
           <listitem>
             <para>None, but the tactic may fail finding a proof if every
              proof is in the search space that is pruned away. Pruning is
-             controlled by <command>d</command> and <command>w</command>.
+             controlled by the optional <command>params</command>.
              Moreover, only lemmas whose type signature is a subset of the
              signature of the current sequent are considered. The signature of
-             a sequent is ...TODO</para>
+             a sequent is ...&TODO;</para>
           </listitem>
         </varlistentry>
         <varlistentry>
diff --git a/matita/help/C/sec_terms.xml b/matita/help/C/sec_terms.xml
index add3ba750..f5ac2b3ec 100644
--- a/matita/help/C/sec_terms.xml
+++ b/matita/help/C/sec_terms.xml
@@ -687,6 +687,36 @@
      </tgroup>
     </table>
     </sect2>
+
+    <sect2 id="auto-params">
+    <title>auto-params</title>
+    <para>&TODO;</para>
+    <table frame="topbot" rowsep="0" colsep="0" role="grammar">
+      <title>reduction-kind</title>
+      <tgroup cols="4">
+      <tbody>
+       <row>
+	<entry id="grammar.autoparams">&autoparams;</entry>
+	<entry>::=</entry>
+        <entry><emphasis role="bold">depth=&nat;</emphasis></entry>
+        <entry>&TODO;</entry>
+       </row>
+       <row>
+        <entry/>
+        <entry>|</entry>
+        <entry><emphasis role="bold">width=&nat;</emphasis></entry>
+        <entry>&TODO;</entry>
+       </row>
+       <row>
+        <entry/>
+        <entry>|</entry>
+        <entry><emphasis role="bold">&TODO;</emphasis></entry>
+        <entry>&TODO;</entry>
+       </row>
+      </tbody>
+     </tgroup>
+    </table>
+    </sect2>
   </sect1>
 
 </chapter>