- some fixes regarding URIs of equality that now should be coherent with the

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

diff --git a/helm/software/components/tactics/paramodulation/indexing.ml b/helm/software/components/tactics/paramodulation/indexing.ml
index da76559e843f6f16ec80be9c78cb671b085aa647..7aafcbcd627927c66ced9577151dd61f2ef985ab 100644 (file)
--- a/helm/software/components/tactics/paramodulation/indexing.ml
+++ b/helm/software/components/tactics/paramodulation/indexing.ml
@@ -61,7 +61,7 @@ type retrieval_mode = Matching | Unification;;
 let string_of_res ?env =
   function
       None -> "None"
-    | Some (t, s, m, u, ((p,e), eq_URI)) ->
+    | Some (t, s, m, u, (p,e)) ->
         Printf.sprintf "Some: (%s, %s, %s)" 
           (Utils.string_of_pos p)
           (Equality.string_of_equality ?env e)
@@ -122,7 +122,7 @@ let check_for_duplicates metas msg =
 
 let check_res res msg =
   match res with
-      Some (t, subst, menv, ug, (eq_found, eq_URI)) ->
+      Some (t, subst, menv, ug, eq_found) ->
         let eqs = Equality.string_of_equality (snd eq_found) in
         check_disjoint_invariant subst menv msg;
         check_for_duplicates menv (msg ^ "\nchecking " ^ eqs);
@@ -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
 ;;
@@ -243,22 +252,21 @@ let rec find_matches metasenv context ugraph lift_amount term termty =
                                 ~metasenv context termty ty ugraph)) then (
           find_matches metasenv context ugraph lift_amount term termty tl
         ) else
-          let do_match c eq_URI =
+          let do_match c =
             let subst', metasenv', ugraph' =
               Inference.matching 
                 metasenv metas context term (S.lift lift_amount c) ugraph
             in
-            Some (Cic.Rel (1 + lift_amount), subst', metasenv', ugraph',
-                  (candidate, eq_URI))
+            Some (Cic.Rel(1+lift_amount),subst',metasenv',ugraph',candidate)
           in
-          let c, other, eq_URI =
-            if pos = Utils.Left then left, right, Utils.eq_ind_URI ()
-            else right, left, Utils.eq_ind_r_URI ()
+          let c, other =
+            if pos = Utils.Left then left, right
+            else right, left
           in
           if o <> U.Incomparable then
             let res =
               try
-                do_match c eq_URI
+                do_match c 
               with Inference.MatchingFailure ->
                 find_matches metasenv context ugraph lift_amount term termty tl
             in
@@ -266,7 +274,7 @@ let rec find_matches metasenv context ugraph lift_amount term termty =
               res
           else
             let res =
-              try do_match c eq_URI
+              try do_match c 
               with Inference.MatchingFailure -> None
             in
             if Utils.debug_res then ignore (check_res res "find2");
@@ -307,19 +315,19 @@ let rec find_all_matches ?(unif_fun=Inference.unification)
     | candidate::tl ->
         let pos, equality = candidate in 
         let (_,_,(ty,left,right,o),metas,_)=Equality.open_equality equality in
-        let do_match c eq_URI =
+        let do_match c =
           let subst', metasenv', ugraph' =
             unif_fun metasenv metas context term (S.lift lift_amount c) ugraph
           in
-          (C.Rel (1+lift_amount),subst',metasenv',ugraph',(candidate, eq_URI))
+          (C.Rel (1+lift_amount),subst',metasenv',ugraph',candidate)
         in
-        let c, other, eq_URI =
-          if pos = Utils.Left then left, right, Utils.eq_ind_URI ()
-          else right, left, Utils.eq_ind_r_URI ()
+        let c, other =
+          if pos = Utils.Left then left, right
+          else right, left
         in
         if o <> U.Incomparable then
           try
-            let res = do_match c eq_URI in
+            let res = do_match c in
             res::(find_all_matches ~unif_fun metasenv context ugraph
                     lift_amount term termty tl)
           with
@@ -330,7 +338,7 @@ let rec find_all_matches ?(unif_fun=Inference.unification)
                 lift_amount term termty tl
         else
           try
-            let res = do_match c eq_URI in
+            let res = do_match c in
             match res with
             | _, s, _, _, _ ->
                 let c' = apply_subst s c
@@ -388,7 +396,7 @@ let subsumption_aux use_unification env table target =
   in
   let rec ok what leftorright = function
     | [] -> None
-    | (_, subst, menv, ug, ((pos,equation),_))::tl ->
+    | (_, 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
@@ -399,7 +407,7 @@ let subsumption_aux use_unification env table target =
           in
           (match Subst.merge_subst_if_possible subst subst' with
           | None -> ok what leftorright tl
-          | Some s -> Some (s, equation, leftorright))
+          | Some s -> Some (s, equation, leftorright <> pos ))
         with 
         | Inference.MatchingFailure 
         | CicUnification.UnificationFailure _ -> ok what leftorright tl
@@ -528,7 +536,7 @@ let rec demodulation_aux ?from ?(typecheck=false)
 exception Foo
 
 (** demodulation, when target is an equality *)
-let rec demodulation_equality ?from newmeta env table sign target =
+let rec demodulation_equality ?from eq_uri newmeta env table sign target =
   let module C = Cic in
   let module S = CicSubstitution in
   let module M = CicMetaSubst in
@@ -550,7 +558,7 @@ let rec demodulation_equality ?from newmeta env table sign target =
   let metasenv' = (* metasenv @ *) metas in
   let maxmeta = ref newmeta in
   
-  let build_newtarget is_left (t, subst, menv, ug, (eq_found, eq_URI)) =
+  let build_newtarget is_left (t, subst, menv, ug, eq_found) =
     
     if Utils.debug_metas then
       begin
@@ -574,8 +582,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, []);
-                  S.lift 1 eq_ty; l; r]
+          C.Appl [C.MutInd (eq_uri, 0, []); S.lift 1 eq_ty; l; r]
       in
       if sign = Utils.Positive then
           (bo, (Equality.Step (subst,(Equality.Demodulation, id,(pos,id'),
@@ -684,7 +691,7 @@ let rec demodulation_equality ?from newmeta env table sign target =
             (Equality.meta_convertibility_eq target newtarget) then
               newmeta, newtarget
           else 
-            demodulation_equality ?from newmeta env table sign newtarget
+            demodulation_equality ?from eq_uri newmeta env table sign newtarget
     | None ->
         let res = demodulation_aux metasenv' context ugraph table 0 right in
         if Utils.debug_res then check_res res "demod result 1"; 
@@ -695,7 +702,7 @@ let rec demodulation_equality ?from newmeta env table sign target =
                   (Equality.meta_convertibility_eq target newtarget) then
                     newmeta, newtarget
                 else
-                   demodulation_equality ?from newmeta env table sign newtarget
+                   demodulation_equality ?from eq_uri newmeta env table sign newtarget
           | None ->
               newmeta, target
   in
@@ -719,6 +726,7 @@ let rec betaexpand_term
   let res, lifted_term = 
     match term with
     | C.Meta (i, l) ->
+        let l = [] in
         let l', lifted_l =
           List.fold_right
             (fun arg (res, lifted_tl) ->
@@ -841,8 +849,7 @@ let rec betaexpand_term
    index: its updated value is also returned
 *)
 let superposition_right 
-  ?(subterms_only=false) newmeta (metasenv, context, ugraph) table target 
-=
+  ?(subterms_only=false) eq_uri newmeta (metasenv, context, ugraph) table target=
   let module C = Cic in
   let module S = CicSubstitution in
   let module M = CicMetaSubst in
@@ -873,7 +880,7 @@ let superposition_right
         in
         (res left right), (res right left)
   in
-  let build_new ordering (bo, s, m, ug, (eq_found, eq_URI)) =
+  let build_new ordering (bo, s, m, ug, eq_found) =
     if Utils.debug_metas then 
       ignore (check_target context (snd eq_found) "buildnew1" );
     
@@ -891,8 +898,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, []);
-                S.lift 1 eq_ty; l; r]
+        C.Appl [C.MutInd (eq_uri, 0, []); S.lift 1 eq_ty; l; r]
       in
       bo',
         Equality.Step 
@@ -939,7 +945,7 @@ let rec demodulation_theorem newmeta env table theorem =
   let term, termty, metas = theorem in
   let metasenv' = metas in
   
-  let build_newtheorem (t, subst, menv, ug, (eq_found, eq_URI)) =
+  let build_newtheorem (t, subst, menv, ug, eq_found) =
     let pos, equality = eq_found in
     let (_, proof', (ty, what, other, _), menv',id) = 
       Equality.open_equality equality in
@@ -1018,7 +1024,7 @@ let fix_expansion goal posu (t, subst, menv, ug, eq_f) =
  * expansion builds a new goal *)
 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 (t,subst,menv,ug,eq_found) = fix_expansion goal posu expansion in
   let pos, equality = eq_found in
   let (_, proof', (ty, what, other, _), menv',id) = 
     Equality.open_equality equality in
@@ -1048,11 +1054,20 @@ let superposition_left (metasenv, context, ugraph) table goal =
     Utils.compare_weights ~normalize:true
       (Utils.weight_of_term l) (Utils.weight_of_term r)
   in
-  let big,small,possmall = 
-    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 Equality.SuperpositionLeft) expansions
+  
+  if c = Utils.Incomparable then
+    let expansionsl, _ = betaexpand_term menv context ugraph table 0 l in
+    let expansionsr, _ = betaexpand_term menv context ugraph table 0 r in
+    List.map (build_newgoal context goal Utils.Right Equality.SuperpositionLeft) expansionsl
+    @
+    List.map (build_newgoal context goal Utils.Left Equality.SuperpositionLeft) expansionsr
+
+  else
+    let big,small,possmall = 
+      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 Equality.SuperpositionLeft) expansions
 ;;
 
 (** demodulation, when the target is a goal *)