goals after a superposition step are relocated

[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 6b3a1e0efabc8ab8271532715d6a38003ae85593..3ac57e6fe63ed2285b06722d7e7dd04853cf298f 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 =
@@ -463,9 +465,10 @@ let build_proof_step eq lift subst p1 p2 pos l r pred =
 ;;
 
 let parametrize_proof p l r ty = 
-  let parameters = 
-    CicUtil.metas_of_term p @ CicUtil.metas_of_term l @ CicUtil.metas_of_term r
-  in (* ?if they are under a lambda? *)
+  let uniq l = HExtlib.list_uniq (List.sort Pervasives.compare l) in
+  let mot = CicUtil.metas_of_term_set in
+  let parameters = uniq (mot p @ mot l @ mot r) in 
+  (* ?if they are under a lambda? *)
   let parameters = 
     HExtlib.list_uniq (List.sort Pervasives.compare parameters) 
   in
@@ -578,9 +581,12 @@ let rec find_deps m i =
 
 let topological_sort l = 
   (* build the partial order relation *)
-  let m = 
-    List.fold_left (fun m i -> find_deps m i)
-    M.empty l
+  let m = List.fold_left (fun m i -> find_deps m i) M.empty l in
+  let m = (* keep only deps inside l *) 
+    List.fold_left 
+      (fun m' i ->
+        M.add i (List.filter (fun x -> List.mem x l) (M.find i m)) m') 
+      M.empty l 
   in
   let m = M.map (fun x -> Some x) m in
   (* utils *)
@@ -601,7 +607,8 @@ let topological_sort l =
       let res = ok @ res in
       if ok = [] then res else aux m res
   in
-  aux m []
+  let rc = List.rev (aux m []) in
+  rc
 ;;
   
 
@@ -648,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
@@ -663,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);
@@ -728,7 +736,9 @@ let build_goal_proof eq l initial ty se =
           cic, p))
     lets (letsno-1,initial)
   in
-   canonical (contextualize_rewrites proof (CicSubstitution.lift letsno ty)),
+(*    canonical (contextualize_rewrites proof (CicSubstitution.lift letsno ty)),
+ *    *)
+proof,
    se 
 ;;
 
@@ -772,6 +782,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 =