Demodulate used to be a reduction_kind and it used to take a ~pattern.

Since demodulation is not a reduction kind, I changed it to a normal tactic.
Moreover, since the ~pattern was unused, I have temporarily removed it.
Doc changed accordingly.

diff --git a/components/grafite/grafiteAst.ml b/components/grafite/grafiteAst.ml
index 32625f39f108635b78f3790f5921abdb35738a61..5896e116fa6f17de2ff832c77c297578105e97bd 100644 (file)
--- a/components/grafite/grafiteAst.ml
+++ b/components/grafite/grafiteAst.ml
@@ -37,8 +37,7 @@ type ('term, 'ident) type_spec =
    | Type of UriManager.uri * int 
 
 type 'lazy_term reduction =
-  [ `Demodulate
-  | `Normalize
+  [ `Normalize
   | `Reduce
   | `Simpl
   | `Unfold of 'lazy_term option
@@ -57,6 +56,7 @@ type ('term, 'lazy_term, 'reduction, 'ident) tactic =
   | Contradiction of loc
   | Cut of loc * 'ident option * 'term
   | Decompose of loc * ('term, 'ident) type_spec list * 'ident option * 'ident list
+  | Demodulate of loc
   | Discriminate of loc * 'term
   | Elim of loc * 'term * 'term option * int option * 'ident list
   | ElimType of loc * 'term * 'term option * int option * 'ident list

diff --git a/components/grafite/grafiteAstPp.ml b/components/grafite/grafiteAstPp.ml
index 18f14c5ce99aefe1f96c1dcf3fc1e3339b9198d1..941f75d9d6dae352574be19861ddc79d1775f2c5 100644 (file)
--- a/components/grafite/grafiteAstPp.ml
+++ b/components/grafite/grafiteAstPp.ml
@@ -36,7 +36,6 @@ let command_terminator = tactical_terminator
 let pp_idents idents = "[" ^ String.concat "; " idents ^ "]"
 
 let pp_reduction_kind ~term_pp = function
-  | `Demodulate -> "demodulate"
   | `Normalize -> "normalize"
   | `Reduce -> "reduce"
   | `Simpl -> "simplify"
@@ -99,6 +98,7 @@ let rec pp_tactic ~term_pp ~lazy_term_pp =
       in
       let types = List.rev_map to_ident types in
       sprintf "decompose %s %s%s" (pp_idents types) (opt_string_pp what) (pp_intros_specs (None, names)) 
+  | Demodulate _ -> "demodulate"
   | Discriminate (_, term) -> "discriminate " ^ term_pp term
   | Elim (_, term, using, num, idents) ->
       sprintf "elim " ^ term_pp term ^

diff --git a/components/grafite_engine/grafiteEngine.ml b/components/grafite_engine/grafiteEngine.ml
index d7343c98c1447c5831ace4066798c6828e37fd09..b066b8ae09cafc5472a21c0bbc16b6a5625d7d21 100644 (file)
--- a/components/grafite_engine/grafiteEngine.ml
+++ b/components/grafite_engine/grafiteEngine.ml
@@ -83,6 +83,7 @@ let tactic_of_ast ast =
       let dbd = LibraryDb.instance () in
       let mk_fresh_name_callback = namer_of names in
       Tactics.decompose ~mk_fresh_name_callback ~dbd ~user_types ?what
+  | GrafiteAst.Demodulate _ -> Tactics.demodulate ~dbd:(LibraryDb.instance ())
   | GrafiteAst.Discriminate (_,term) -> Tactics.discriminate term
   | GrafiteAst.Elim (_, what, using, depth, names) ->
       Tactics.elim_intros ?using ?depth ~mk_fresh_name_callback:(namer_of names)
@@ -96,8 +97,6 @@ let tactic_of_ast ast =
   | GrafiteAst.Fold (_, reduction_kind, term, pattern) ->
       let reduction =
         match reduction_kind with
-        | `Demodulate -> 
-            GrafiteTypes.command_error "demodulation can't be folded"
         | `Normalize ->
             PET.const_lazy_reduction
               (CicReduction.normalize ~delta:false ~subst:[])
@@ -139,7 +138,6 @@ let tactic_of_ast ast =
       Tactics.letin term ~mk_fresh_name_callback:(namer_of [name])
   | GrafiteAst.Reduce (_, reduction_kind, pattern) ->
       (match reduction_kind with
-        | `Demodulate -> Tactics.demodulate ~dbd:(LibraryDb.instance ()) ~pattern
         | `Normalize -> Tactics.normalize ~pattern
         | `Reduce -> Tactics.reduce ~pattern  
         | `Simpl -> Tactics.simpl ~pattern 

diff --git a/components/grafite_parser/grafiteDisambiguate.ml b/components/grafite_parser/grafiteDisambiguate.ml
index 5babe3604b2478424cfc48c0ed27e5432a3ee0fb..6b7dd076bd68840453717b08e627405e7660cae6 100644 (file)
--- a/components/grafite_parser/grafiteDisambiguate.ml
+++ b/components/grafite_parser/grafiteDisambiguate.ml
@@ -98,7 +98,6 @@ let disambiguate_reduction_kind text prefix_len lexicon_status_ref = function
   | `Unfold (Some t) ->
       let t = disambiguate_lazy_term text prefix_len lexicon_status_ref t in
       `Unfold (Some t)
-  | `Demodulate
   | `Normalize
   | `Reduce
   | `Simpl
@@ -164,6 +163,8 @@ let disambiguate_tactic
          List.fold_left disambiguate (metasenv,[]) types
         in
          metasenv,GrafiteAst.Decompose (loc, types, what, names)
+    | GrafiteAst.Demodulate loc ->
+        metasenv,GrafiteAst.Demodulate loc
     | GrafiteAst.Discriminate (loc,term) ->
         let metasenv,term = disambiguate_term context metasenv term in
         metasenv,GrafiteAst.Discriminate(loc,term)

diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml
index ccff1fab1d3560cd46e2f2a4d3927259418ae747..f99573b30ccf3840f3444f8c509e1b98a751efc0 100644 (file)
--- a/components/grafite_parser/grafiteParser.ml
+++ b/components/grafite_parser/grafiteParser.ml
@@ -68,8 +68,7 @@ EXTEND
     [ tactic_terms = LIST1 tactic_term SEP SYMBOL "," -> tactic_terms ]
   ];
   reduction_kind: [
-    [ IDENT "demodulate" -> `Demodulate
-    | IDENT "normalize" -> `Normalize
+    [ IDENT "normalize" -> `Normalize
     | IDENT "reduce" -> `Reduce
     | IDENT "simplify" -> `Simpl
     | IDENT "unfold"; t = OPT tactic_term -> `Unfold t
@@ -154,6 +153,7 @@ EXTEND
        let idents = match idents with None -> [] | Some idents -> idents in
        let to_spec id = GrafiteAst.Ident id in
        GrafiteAst.Decompose (loc, List.rev_map to_spec types, what, idents)
+    | IDENT "demodulate" -> GrafiteAst.Demodulate loc
     | IDENT "discriminate"; t = tactic_term ->
         GrafiteAst.Discriminate (loc, t)
     | IDENT "elim"; what = tactic_term; using = using;

diff --git a/components/tactics/.depend b/components/tactics/.depend
index 743811ceb5d9d315e622ff08c7adffff53b62d5d..50083802753f2ac184c1e13d11d1a24ff04aa729 100644 (file)
--- a/components/tactics/.depend
+++ b/components/tactics/.depend
@@ -16,11 +16,11 @@ paramodulation/indexing.cmi: paramodulation/utils.cmi \
     paramodulation/equality.cmi 
 paramodulation/saturation.cmi: proofEngineTypes.cmi 
 variousTactics.cmi: proofEngineTypes.cmi 
-autoTactic.cmi: proofEngineTypes.cmi 
 introductionTactics.cmi: proofEngineTypes.cmi 
 eliminationTactics.cmi: proofEngineTypes.cmi 
 negationTactics.cmi: proofEngineTypes.cmi 
 equalityTactics.cmi: proofEngineTypes.cmi 
+autoTactic.cmi: proofEngineTypes.cmi 
 discriminationTactics.cmi: proofEngineTypes.cmi 
 inversion.cmi: proofEngineTypes.cmi 
 ring.cmi: proofEngineTypes.cmi 
@@ -102,12 +102,6 @@ variousTactics.cmo: tacticals.cmi proofEngineTypes.cmi \
 variousTactics.cmx: tacticals.cmx proofEngineTypes.cmx \
     proofEngineReduction.cmx proofEngineHelpers.cmx primitiveTactics.cmx \
     variousTactics.cmi 
-autoTactic.cmo: paramodulation/saturation.cmi proofEngineTypes.cmi \
-    proofEngineHelpers.cmi primitiveTactics.cmi metadataQuery.cmi \
-    paramodulation/equality.cmi autoTactic.cmi 
-autoTactic.cmx: paramodulation/saturation.cmx proofEngineTypes.cmx \
-    proofEngineHelpers.cmx primitiveTactics.cmx metadataQuery.cmx \
-    paramodulation/equality.cmx autoTactic.cmi 
 introductionTactics.cmo: proofEngineTypes.cmi primitiveTactics.cmi \
     introductionTactics.cmi 
 introductionTactics.cmx: proofEngineTypes.cmx primitiveTactics.cmx \
@@ -130,6 +124,14 @@ equalityTactics.cmx: tacticals.cmx reductionTactics.cmx proofEngineTypes.cmx \
     proofEngineStructuralRules.cmx proofEngineReduction.cmx \
     proofEngineHelpers.cmx primitiveTactics.cmx introductionTactics.cmx \
     equalityTactics.cmi 
+autoTactic.cmo: tacticals.cmi paramodulation/saturation.cmi \
+    proofEngineTypes.cmi proofEngineHelpers.cmi primitiveTactics.cmi \
+    metadataQuery.cmi equalityTactics.cmi paramodulation/equality.cmi \
+    autoTactic.cmi 
+autoTactic.cmx: tacticals.cmx paramodulation/saturation.cmx \
+    proofEngineTypes.cmx proofEngineHelpers.cmx primitiveTactics.cmx \
+    metadataQuery.cmx equalityTactics.cmx paramodulation/equality.cmx \
+    autoTactic.cmi 
 discriminationTactics.cmo: tacticals.cmi reductionTactics.cmi \
     proofEngineTypes.cmi primitiveTactics.cmi introductionTactics.cmi \
     equalityTactics.cmi eliminationTactics.cmi discriminationTactics.cmi 
@@ -150,6 +152,8 @@ ring.cmo: tacticals.cmi proofEngineTypes.cmi proofEngineStructuralRules.cmi \
     primitiveTactics.cmi equalityTactics.cmi eliminationTactics.cmi ring.cmi 
 ring.cmx: tacticals.cmx proofEngineTypes.cmx proofEngineStructuralRules.cmx \
     primitiveTactics.cmx equalityTactics.cmx eliminationTactics.cmx ring.cmi 
+setoids.cmo: proofEngineTypes.cmi setoids.cmi 
+setoids.cmx: proofEngineTypes.cmx setoids.cmi 
 fourier.cmo: fourier.cmi 
 fourier.cmx: fourier.cmi 
 fourierR.cmo: tacticals.cmi ring.cmi reductionTactics.cmi \

diff --git a/components/tactics/paramodulation/saturation.ml b/components/tactics/paramodulation/saturation.ml
index cbf15f0dfdad34e6e26a8f2ba4e532c713812f79..6cd2bcf4a8240813ef0bdf520902576d69369fb8 100644 (file)
--- a/components/tactics/paramodulation/saturation.ml
+++ b/components/tactics/paramodulation/saturation.ml
@@ -1873,7 +1873,7 @@ let main_demod_equalities dbd term metasenv ugraph =
 *)
 ;;
 
-let demodulate_tac ~dbd ~pattern ((proof,goal)(*s initialstatus*)) = 
+let demodulate_tac ~dbd ((proof,goal)(*s initialstatus*)) = 
   let curi,metasenv,pbo,pty = proof in
   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
   let eq_uri = eq_of_goal ty in 
@@ -1917,13 +1917,11 @@ let demodulate_tac ~dbd ~pattern ((proof,goal)(*s initialstatus*)) =
   else (* if newty = ty then *)
     raise (ProofEngineTypes.Fail (lazy "no progress"))
   (*else ProofEngineTypes.apply_tactic 
-    (ReductionTactics.simpl_tac ~pattern) 
-    initialstatus*)
+    (ReductionTactics.simpl_tac
+      ~pattern:(ProofEngineTypes.conclusion_pattern None)) initialstatus*)
 ;;
 
-let demodulate_tac ~dbd ~pattern = 
-  ProofEngineTypes.mk_tactic (demodulate_tac ~dbd ~pattern)
-;;
+let demodulate_tac ~dbd = ProofEngineTypes.mk_tactic (demodulate_tac ~dbd);;
 
 let rec find_in_ctx i name = function
   | [] -> raise (ProofEngineTypes.Fail (lazy ("Hypothesis not found: " ^ name)))

diff --git a/components/tactics/paramodulation/saturation.mli b/components/tactics/paramodulation/saturation.mli
index 8a03cd547a0be220daae305c3f44c379ca9b9524..d48dfc349ba77d007b9da65e564b618981b68028 100644 (file)
--- a/components/tactics/paramodulation/saturation.mli
+++ b/components/tactics/paramodulation/saturation.mli
@@ -48,9 +48,7 @@ val main_demod_equalities: HMysql.dbd ->
     Cic.term -> Cic.conjecture list -> CicUniv.universe_graph -> unit
 val main: HMysql.dbd ->
     bool -> Cic.term -> Cic.conjecture list -> CicUniv.universe_graph -> unit
-val demodulate_tac: 
-  dbd:HMysql.dbd ->  
-  pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic
+val demodulate_tac: dbd:HMysql.dbd ->  ProofEngineTypes.tactic
 
 val superposition_tac: 
   target:string -> table:string -> subterms_only:bool ->

diff --git a/components/tactics/tactics.mli b/components/tactics/tactics.mli
index 73d864e1dd7cbbc02e6b2c74ea672b76ea9e9004..d8a3959bffea0e0c538c20bd3b2b4c092b18e6a3 100644 (file)
--- a/components/tactics/tactics.mli
+++ b/components/tactics/tactics.mli
@@ -19,9 +19,7 @@ val decompose :
   ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
   ?user_types:(UriManager.uri * int) list ->
   ?what:string -> dbd:HMysql.dbd -> ProofEngineTypes.tactic
-val demodulate :
-  dbd:HMysql.dbd ->
-  pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic
+val demodulate : dbd:HMysql.dbd -> ProofEngineTypes.tactic
 val discriminate : term:Cic.term -> ProofEngineTypes.tactic
 val elim_intros :
   ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->

diff --git a/matita/help/C/sec_tactics.xml b/matita/help/C/sec_tactics.xml
index 130c08e56749cf2f08e9eb607fc3999e19781f83..56037dde56bf7d59f20b4efc6d6b1f848a2b643a 100644 (file)
--- a/matita/help/C/sec_tactics.xml
+++ b/matita/help/C/sec_tactics.xml
@@ -450,16 +450,16 @@
       </variablelist>
     </para>
   </sect1>
-  <sect1 id="tac_demodulation">
-    <title>demodulation</title>
-    <titleabbrev>demodulation</titleabbrev>
-    <para><userinput>demodulation patt</userinput></para>
+  <sect1 id="tac_demodulate">
+    <title>demodulate</title>
+    <titleabbrev>demodulate</titleabbrev>
+    <para><userinput>demodulate</userinput></para>
     <para>
       <variablelist>
         <varlistentry role="tactic.synopsis">
           <term>Synopsis:</term>
           <listitem>
-            <para><emphasis role="bold">demodulation</emphasis> &pattern;</para>
+            <para><emphasis role="bold">demodulate</emphasis></para>
           </listitem>
         </varlistentry>
         <varlistentry>

diff --git a/matita/help/C/sec_terms.xml b/matita/help/C/sec_terms.xml
index d521ac87060a6a2e0a462fd8ae079e2235184696..945a43837bcfb79db57081fbb359579a1ec12be3 100644 (file)
--- a/matita/help/C/sec_terms.xml
+++ b/matita/help/C/sec_terms.xml
@@ -643,11 +643,6 @@
        <row>
        <entry id="grammar.reduction-kind">&reduction-kind;</entry>
        <entry>::=</entry>
-        <entry><emphasis role="bold">demodulate</emphasis></entry>
-       </row>
-       <row>
-        <entry/>
-        <entry>|</entry>
         <entry><emphasis role="bold">normalize</emphasis></entry>
         <entry>Computes the βδιζ-normal form</entry>
        </row>

diff --git a/matita/help/C/tactic_quickref.xml b/matita/help/C/tactic_quickref.xml
index dd14d8a2685b15d99c9493b9bebeaf21a7de122a..58fd32afd506fb8fd67f87f80b9ddc3e0f2010a0 100644 (file)
--- a/matita/help/C/tactic_quickref.xml
+++ b/matita/help/C/tactic_quickref.xml
@@ -51,7 +51,11 @@
            </para>
   </listitem>
   <listitem>
-    <para><link linkend="tac_demodulation"><emphasis role="bold">demodulation</emphasis></link> <emphasis><link linkend="grammar.pattern">pattern</link></emphasis></para>
+    <para>
+      <link linkend="tac_demodulate">
+        <emphasis role="bold">demodulate</emphasis>
+      </link>
+    </para>
   </listitem>
   <listitem>
     <para><link linkend="tac_discriminate"><emphasis role="bold">discriminate</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></para>