added the geniric

[helm.git] / helm / software / components / tactics / paramodulation / saturation.ml

diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml
index ca9dc194bd8f0af487c3c0faafb13e82080ec5ee..f81556c8f997e7088fbfe006b3552fdec48c8132 100644 (file)
--- a/helm/software/components/tactics/paramodulation/saturation.ml
+++ b/helm/software/components/tactics/paramodulation/saturation.ml
@@ -1454,6 +1454,12 @@ let eq_of_goal = function
   | _ -> raise (ProofEngineTypes.Fail (lazy ("The goal is not an equality ")))
 ;;
 
+let eq_and_ty_of_goal = function
+  | Cic.Appl [Cic.MutInd(uri,0,_);t;_;_] when LibraryObjects.is_eq_URI uri ->
+      uri,t
+  | _ -> raise (ProofEngineTypes.Fail (lazy ("The goal is not an equality ")))
+;;
+
 let saturate 
     dbd ?(full=false) ?(depth=default_depth) ?(width=default_width) status = 
   let module C = Cic in
@@ -1819,7 +1825,6 @@ let main_demod_equalities dbd term metasenv ugraph =
 ;;
 
 let demodulate_tac ~dbd ~pattern ((proof,goal)(*s initialstatus*)) = 
-  let module I = Inference in
   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 
@@ -1827,7 +1832,7 @@ let demodulate_tac ~dbd ~pattern ((proof,goal)(*s initialstatus*)) =
     Inference.find_equalities context proof 
   in
   let lib_eq_uris, library_equalities, maxm =
-    I.find_library_equalities dbd context (proof, goal) (maxm+2) in
+    Inference.find_library_equalities dbd context (proof, goal) (maxm+2) in
   if library_equalities = [] then prerr_endline "VUOTA!!!";
   let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
   let library_equalities = List.map snd library_equalities in
@@ -1871,6 +1876,74 @@ let demodulate_tac ~dbd ~pattern =
   ProofEngineTypes.mk_tactic (demodulate_tac ~dbd ~pattern)
 ;;
 
+let rec find_in_ctx i name = function
+  | [] -> raise (ProofEngineTypes.Fail (lazy ("Hypothesis not found: " ^ name)))
+  | Some (Cic.Name name', _)::tl when name = name' -> i
+  | _::tl -> find_in_ctx (i+1) name tl
+;;
+
+let rec position_of i x = function
+  | [] -> assert false
+  | j::tl when j <> x -> position_of (i+1) x tl
+  | _ -> i
+;;
+
+let superposition_tac ~what ~other ~subterms_only ~demodulate status = 
+  reset_refs();
+  let proof,goalno = status in 
+  let curi,metasenv,pbo,pty = proof in
+  let metano,context,ty = CicUtil.lookup_meta goalno metasenv in
+  let eq_uri,tty = eq_and_ty_of_goal ty in
+  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 maxm, eql = 
+    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 result: ");
+  List.iter (fun e -> prerr_endline (Equality.string_of_equality e ~env)) eql;
+  prerr_endline ("\n result (cut&paste): ");
+  List.iter 
+    (fun e -> 
+      let t = Equality.term_of_equality eq_uri e in
+      prerr_endline (CicPp.pp t names)) 
+  eql;
+  if demodulate then
+    begin
+      let table = List.fold_left Indexing.index Indexing.empty equalities in
+      let maxm,eql = 
+        List.fold_left 
+          (fun (maxm,acc) e -> 
+            let maxm,eq = 
+              Indexing.demodulation_equality 
+                eq_uri maxm env table Utils.Positive e
+            in
+            maxm,eq::acc) 
+          (maxm,[]) eql
+      in
+      let eql = List.rev eql in
+      prerr_endline ("\n result [demod]: ");
+      List.iter 
+        (fun e -> prerr_endline (Equality.string_of_equality e ~env)) eql;
+      prerr_endline ("\n result [demod] (cut&paste): ");
+      List.iter 
+        (fun e -> 
+          let t = Equality.term_of_equality eq_uri e in
+          prerr_endline (CicPp.pp t names)) 
+      eql;
+    end;
+  proof,[goalno]
+;;
+
 let get_stats () = 
   <:show<Saturation.>> ^ Indexing.get_stats () ^ Inference.get_stats () ^
   Equality.get_stats ();;