X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Findexing.ml;h=b535119ed2df5702e9c8a3f2f0a99ce4d0bd7b80;hb=b4da5c84ca7fa4c028ef70875aa79cc7bc279ee9;hp=ff5bf23cbbaae16548a4dd6a643fa089856ec96c;hpb=bd4a73c6f758bd39254178dd7b313af321a5cd4b;p=helm.git

diff --git a/helm/software/components/tactics/paramodulation/indexing.ml b/helm/software/components/tactics/paramodulation/indexing.ml
index ff5bf23cb..b535119ed 100644
--- a/helm/software/components/tactics/paramodulation/indexing.ml
+++ b/helm/software/components/tactics/paramodulation/indexing.ml
@@ -404,7 +404,7 @@ let subsumption_aux use_unification env table target =
         | Founif.MatchingFailure 
         | CicUnification.UnificationFailure _ -> ok what leftorright tl
   in
-  match ok right Utils.Left  leftr with
+  match ok right Utils.Left leftr with
   | Some _ as res -> res
   | None -> 
       let rightr =
@@ -426,6 +426,61 @@ let unification x y z =
   subsumption_aux true x y z
 ;;
 
+let subsumption_aux_all use_unification env table target = 
+  let _, _, (ty, left, right, _), tmetas, _ = Equality.open_equality target in
+  let _, context, ugraph = env in
+  let metasenv = tmetas in
+  let predicate, unif_fun = 
+    if use_unification then
+      Unification, Founif.unification
+    else
+      Matching, Founif.matching
+  in
+  let leftr =
+    match left with
+    | Cic.Meta _ when not use_unification -> []   
+    | _ ->
+        let leftc = get_candidates predicate table left in
+        find_all_matches ~unif_fun
+          metasenv context ugraph 0 left ty leftc
+  in
+  let rightr =
+        match right with
+          | Cic.Meta _ when not use_unification -> [] 
+          | _ ->
+              let rightc = get_candidates predicate table right in
+                find_all_matches ~unif_fun
+                  metasenv context ugraph 0 right ty rightc
+  in
+  let rec ok_all what leftorright = function
+    | [] -> []
+    | (_, subst, menv, ug, (pos,equation))::tl ->
+        let _, _, (_, l, r, o), m,_ = Equality.open_equality equation in
+        try
+          let other = if pos = Utils.Left then r else l in
+          let what' = Subst.apply_subst subst what in
+          let other' = Subst.apply_subst subst other in
+          let subst', menv', ug' =
+            unif_fun metasenv m context what' other' ugraph
+          in
+          (match Subst.merge_subst_if_possible subst subst' with
+          | None -> ok_all what leftorright tl
+          | Some s -> 
+	      (s, equation, leftorright <> pos )::(ok_all what leftorright tl))
+        with 
+        | Founif.MatchingFailure 
+        | CicUnification.UnificationFailure _ -> (ok_all what leftorright tl)
+  in
+  (ok_all right Utils.Left leftr)@(ok_all left Utils.Right rightr )
+;;
+
+let subsumption_all x y z =
+  subsumption_aux_all false x y z
+;;
+
+let unification_all x y z = 
+  subsumption_aux_all true x y z
+;;
 let rec demodulation_aux bag ?from ?(typecheck=false) 
   metasenv context ugraph table lift_amount term =
 (*  Printf.eprintf "term = %s\n" (CicPp.ppterm term);*)
@@ -600,7 +655,7 @@ let rec demodulation_equality bag ?from eq_uri newmeta env table target =
     match res with
     | Some t ->
         let newmeta, newtarget = build_newtarget true t in
-          assert (not (Equality.meta_convertibility_eq target newtarget));
+          (* assert (not (Equality.meta_convertibility_eq target newtarget)); *)
           if (Equality.is_weak_identity newtarget) (* || *)
             (*Equality.meta_convertibility_eq target newtarget*) then
               newmeta, newtarget
@@ -843,7 +898,7 @@ let superposition_right bag
   in
   let new1 = List.map (build_new U.Gt) res1
   and new2 = List.map (build_new U.Lt) res2 in
-  let ok e = not (Equality.is_weak_identity (*metasenv', context, ugraph*) e) in
+  let ok e = not (Equality.is_identity (metasenv', context, ugraph) e) in
   (!maxmeta,
    (List.filter ok (new1 @ new2)))
 ;;
@@ -904,7 +959,7 @@ let rec demodulation_theorem bag newmeta env table theorem =
 let open_goal g =
   match g with
   | (proof,menv,Cic.Appl[(Cic.MutInd(uri,0,_)) as eq;ty;l;r]) -> 
-      assert (LibraryObjects.is_eq_URI uri);
+      (* assert (LibraryObjects.is_eq_URI uri); *)
       proof,menv,eq,ty,l,r
   | _ -> assert false
 ;;
@@ -948,8 +1003,11 @@ let build_newgoal bag context goal posu rule expansion =
       Utils.guarded_simpl context 
         (apply_subst subst (CicSubstitution.subst other t)) 
     in
-    let bo' = (*apply_subst subst*) t in 
-    let name = Cic.Name "x" in
+    let bo' = (*apply_subst subst*) t in
+    (* patch?? 
+    let bo' = t in
+    let ty = apply_subst subst ty in *)
+    let name = Cic.Name "x" in 
     let newgoalproofstep = (rule,pos,id,subst,Cic.Lambda (name,ty,bo')) in
     bo, (newgoalproofstep::goalproof)
   in