X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Fsaturation.ml;h=bb1b3a853515d22c49fecc0e9b43e944e0b55d17;hb=a507a21ca97552dec5077667cf8433f24d7a45ae;hp=f81556c8f997e7088fbfe006b3552fdec48c8132;hpb=3b7bfb05e6fc1a2ac6864d8f7d959fcda0597d21;p=helm.git

diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml
index f81556c8f..bb1b3a853 100644
--- a/helm/software/components/tactics/paramodulation/saturation.ml
+++ b/helm/software/components/tactics/paramodulation/saturation.ml
@@ -1888,8 +1888,19 @@ let rec position_of i x = function
   | _ -> i
 ;;
 
-let superposition_tac ~what ~other ~subterms_only ~demodulate status = 
+(* Syntax: 
+ *   auto superposition target = NAME 
+ *     [table = NAME_LIST] [demod_table = NAME_LIST] [subterms_only]
+ *
+ *  - if table is omitted no superposition will be performed
+ *  - if demod_table is omitted no demodulation will be prformed
+ *  - subterms_only is passed to Indexing.superposition_right
+ *
+ *  lists are coded using _ (example: H_H1_H2)
+ *)
+let superposition_tac ~target ~table ~subterms_only ~demod_table status = 
   reset_refs();
+  Indexing.init_index ();
   let proof,goalno = status in 
   let curi,metasenv,pbo,pty = proof in
   let metano,context,ty = CicUtil.lookup_meta goalno metasenv in
@@ -1897,18 +1908,32 @@ let superposition_tac ~what ~other ~subterms_only ~demodulate status =
   let env = (metasenv, context, CicUniv.empty_ugraph) in
   let names = names_of_context context in
   let eq_index, equalities, maxm = find_equalities context proof in
-  let what = find_in_ctx 1 what context in
-  let other = find_in_ctx 1 other context in
-  let eq_what = List.nth equalities (position_of 0 what eq_index) in
-  let eq_other = List.nth equalities (position_of 0 other eq_index) in
-  let index = Indexing.index Indexing.empty eq_other in
+  let eq_what = 
+    let what = find_in_ctx 1 target context in
+    List.nth equalities (position_of 0 what eq_index)
+  in
+  let eq_other = 
+    if table <> "" then
+      let other = 
+        let others = Str.split (Str.regexp "_") table in 
+        List.map (fun other -> find_in_ctx 1 other context) others 
+      in
+      List.map 
+        (fun other -> List.nth equalities (position_of 0 other eq_index)) 
+        other 
+    else
+      []
+  in
+  let index = List.fold_left Indexing.index Indexing.empty eq_other in
   let maxm, eql = 
+    if table = "" then maxm,[eq_what] else 
     Indexing.superposition_right 
       ~subterms_only eq_uri maxm env index eq_what
   in
   prerr_endline ("Superposition right:");
   prerr_endline ("\n eq: " ^ Equality.string_of_equality eq_what ~env);
-  prerr_endline ("\n table: " ^ Equality.string_of_equality eq_other ~env);
+  prerr_endline ("\n table: ");
+  List.iter (fun e -> prerr_endline ("  " ^ Equality.string_of_equality e ~env)) eq_other;
   prerr_endline ("\n result: ");
   List.iter (fun e -> prerr_endline (Equality.string_of_equality e ~env)) eql;
   prerr_endline ("\n result (cut&paste): ");
@@ -1917,9 +1942,18 @@ let superposition_tac ~what ~other ~subterms_only ~demodulate status =
       let t = Equality.term_of_equality eq_uri e in
       prerr_endline (CicPp.pp t names)) 
   eql;
-  if demodulate then
+  if demod_table <> "" then
     begin
-      let table = List.fold_left Indexing.index Indexing.empty equalities in
+      let demod = 
+        let demod = Str.split (Str.regexp "_") demod_table in 
+        List.map (fun other -> find_in_ctx 1 other context) demod 
+      in
+      let eq_demod = 
+        List.map 
+          (fun demod -> List.nth equalities (position_of 0 demod eq_index)) 
+          demod 
+      in
+      let table = List.fold_left Indexing.index Indexing.empty eq_demod in
       let maxm,eql = 
         List.fold_left 
           (fun (maxm,acc) e -> 
@@ -1946,5 +1980,6 @@ let superposition_tac ~what ~other ~subterms_only ~demodulate status =
 
 let get_stats () = 
   <:show<Saturation.>> ^ Indexing.get_stats () ^ Inference.get_stats () ^
-  Equality.get_stats ();;
+  Equality.get_stats ()
+;;