- patch to consider the symbols of the goal when computing the weight of an

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

diff --git a/helm/software/components/tactics/paramodulation/equality.ml b/helm/software/components/tactics/paramodulation/equality.ml
index 5a8e8863806a7a737efb072fdff5f789239391ad..91ed61cd5ea9426b7e111029a1e68cf84625f784 100644 (file)
--- a/helm/software/components/tactics/paramodulation/equality.ml
+++ b/helm/software/components/tactics/paramodulation/equality.ml
@@ -46,6 +46,8 @@ and proof =
 and goal_proof = (rule * Utils.pos * int * Subst.substitution * Cic.term) list
 ;;
 
+type goal = goal_proof * Cic.metasenv * Cic.term
+
 (* globals *)
 let maxid = ref 0;;
 let id_to_eq = Hashtbl.create 1024;;
@@ -432,7 +434,7 @@ let add_subst subst =
   function
     | Exact t -> Exact (Subst.apply_subst subst t)
     | Step (s,(rule, id1, (pos,id2), pred)) -> 
-       Step (Subst.concat subst s,(rule, id1, (pos,id2), pred))
+        Step (Subst.concat subst s,(rule, id1, (pos,id2), pred))
 ;;
        
 let build_proof_step eq lift subst p1 p2 pos l r pred =
@@ -653,7 +655,8 @@ let build_proof_term eq h lift proof =
     try List.assoc id h,l,r with Not_found -> aux p, l, r
   in
   let rec aux = function
-     | Exact term -> CicSubstitution.lift lift term
+     | Exact term -> 
+         CicSubstitution.lift lift term
      | Step (subst,(rule, id1, (pos,id2), pred)) ->
          let p1,_,_ = proof_of_id aux id1 in
          let p2,l,r = proof_of_id aux id2 in
@@ -668,7 +671,7 @@ let build_proof_term eq h lift proof =
            | Cic.Lambda (_,a,b) -> Cic.Lambda (varname,a,b)
            | _ -> assert false
          in
-         let p =   build_proof_step eq lift subst p1 p2 pos l r pred in
+         let p = build_proof_step eq lift subst p1 p2 pos l r pred in
 (*         let cond =  (not (List.mem 302 (Utils.metas_of_term p)) || id1 = 8 || id1 = 132) in
            if not cond then
              prerr_endline ("ERROR " ^ string_of_int id1 ^ " " ^ string_of_int id2);
@@ -777,6 +780,21 @@ let relocate newmeta menv to_be_relocated =
   let menv = Subst.apply_subst_metasenv subst menv @ newmetasenv in
   subst, menv, newmeta
 
+let fix_metas_goal newmeta goal =
+  let (proof, menv, ty) = goal in
+  let to_be_relocated = 
+    HExtlib.list_uniq (List.sort Pervasives.compare (Utils.metas_of_term ty))
+  in
+  let subst, menv, newmeta = relocate newmeta menv to_be_relocated in
+  let ty = Subst.apply_subst subst ty in
+  let proof = 
+    match proof with
+    | [] -> assert false (* is a nonsense to relocate the initial goal *)
+    | (r,pos,id,s,p) :: tl -> (r,pos,id,Subst.concat subst s,p) :: tl
+  in
+  newmeta+1,(proof, menv, ty)
+;;
+
 let fix_metas newmeta eq = 
   let w, p, (ty, left, right, o), menv,_ = open_equality eq in
   let to_be_relocated =