1. the default for the default equality/absurd/true/false URIs used to be

[helm.git] / components / tactics / paramodulation / indexing.ml

diff --git a/components/tactics/paramodulation/indexing.ml b/components/tactics/paramodulation/indexing.ml
index a2e6eda07443be5d7e644136861f7520e14d3121..e72ed64dad3c37c9620a97ec7576784bf3cb80ae 100644 (file)
--- a/components/tactics/paramodulation/indexing.ml
+++ b/components/tactics/paramodulation/indexing.ml
@@ -181,8 +181,17 @@ let check_target context target msg =
 let get_candidates ?env mode tree term =
   let s = 
     match mode with
-    | Matching -> Index.retrieve_generalizations tree term
-    | Unification -> Index.retrieve_unifiables tree term
+    | Matching -> 
+        let _ = <:start<retrieve_generalizations>> in
+        <:stop<retrieve_generalizations
+        Index.retrieve_generalizations tree term
+        >>
+    | Unification -> 
+        let _ = <:start<retrieve_unifiables>> in
+        <:stop<retrieve_unifiables
+        Index.retrieve_unifiables tree term
+        >>
+        
   in
   Index.PosEqSet.elements s
 ;;
@@ -386,24 +395,25 @@ let subsumption_aux use_unification env table target =
         find_all_matches ~unif_fun
           metasenv context ugraph 0 left ty leftc
   in
-  let rec ok what = function
+  let rec ok what leftorright = function
     | [] -> None
     | (_, 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
+            unif_fun metasenv m context what' other' ugraph
           in
           (match Subst.merge_subst_if_possible subst subst' with
-          | None -> ok what tl
-          | Some s -> Some (s, equation))
+          | None -> ok what leftorright tl
+          | Some s -> Some (s, equation, leftorright <> pos ))
         with 
         | Inference.MatchingFailure 
-        | CicUnification.UnificationFailure _ -> ok what tl
+        | CicUnification.UnificationFailure _ -> ok what leftorright tl
   in
-  match ok right leftr with
+  match ok right Utils.Left  leftr with
   | Some _ as res -> res
   | None -> 
       let rightr =
@@ -414,7 +424,7 @@ let subsumption_aux use_unification env table target =
                 find_all_matches ~unif_fun
                   metasenv context ugraph 0 right ty rightc
       in
-        ok left rightr
+        ok left Utils.Right rightr 
 ;;
 
 let subsumption x y z =
@@ -573,7 +583,7 @@ let rec demodulation_equality ?from newmeta env table sign target =
       let name = C.Name "x" in
       let bo' =
         let l, r = if is_left then t, S.lift 1 right else S.lift 1 left, t in
-          C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
+          C.Appl [C.MutInd (Utils.eq_URI (), 0, []);
                   S.lift 1 eq_ty; l; r]
       in
       if sign = Utils.Positive then
@@ -890,7 +900,7 @@ let superposition_right
       let bo'' =
         let l, r =
           if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
-        C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
+        C.Appl [C.MutInd (Utils.eq_URI (), 0, []);
                 S.lift 1 eq_ty; l; r]
       in
       bo',
@@ -1015,7 +1025,7 @@ let fix_expansion goal posu (t, subst, menv, ug, eq_f) =
 
 (* ginve the old [goal], the side that has not changed [posu] and the 
  * expansion builds a new goal *)
-let build_newgoal context goal posu expansion =
+let build_newgoal context goal posu rule expansion =
   let goalproof,_,_,_,_,_ = open_goal goal in
   let (t,subst,menv,ug,(eq_found,eq_URI)) = fix_expansion goal posu expansion in
   let pos, equality = eq_found in
@@ -1029,7 +1039,7 @@ let build_newgoal context goal posu expansion =
     in
     let bo' = (*apply_subst subst*) t in 
     let name = Cic.Name "x" in
-    let newgoalproofstep = (pos,id,subst,Cic.Lambda (name,ty,bo')) in
+    let newgoalproofstep = (rule,pos,id,subst,Cic.Lambda (name,ty,bo')) in
     bo, (newgoalproofstep::goalproof)
   in
   let newmetasenv = (* Inference.filter subst *) menv in
@@ -1051,19 +1061,21 @@ let superposition_left (metasenv, context, ugraph) table goal =
     match c with Utils.Gt -> l,r,Utils.Right | _ -> r,l,Utils.Left
   in
   let expansions, _ = betaexpand_term menv context ugraph table 0 big in
-  List.map (build_newgoal context goal possmall) expansions
+  List.map (build_newgoal context goal possmall Equality.SuperpositionLeft) expansions
 ;;
 
 (** demodulation, when the target is a goal *)
 let rec demodulation_goal env table goal =
   let goalproof,menv,_,_,left,right = open_goal goal in
-  let metasenv, context, ugraph = env in
+  let _, context, ugraph = env in
 (*  let term = Utils.guarded_simpl (~debug:true) context term in*)
   let do_right () = 
       let resright = demodulation_aux menv context ugraph table 0 right in
       match resright with
       | Some t ->
-          let newg = build_newgoal context goal Utils.Left t in
+          let newg = 
+            build_newgoal context goal Utils.Left Equality.Demodulation t 
+          in
           if goal_metaconvertibility_eq goal newg then
             false, goal
           else
@@ -1073,7 +1085,7 @@ let rec demodulation_goal env table goal =
   let resleft = demodulation_aux menv context ugraph table 0 left in
   match resleft with
   | Some t ->
-      let newg = build_newgoal context goal Utils.Right t in
+      let newg = build_newgoal context goal Utils.Right Equality.Demodulation t in
       if goal_metaconvertibility_eq goal newg then
         do_right ()
       else