removed abstractios for dummy metavariables when generating letins body

[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 4414d2f435f3af14a1d8cc1d32c131bd0b241db7..2634752e7aea7c65b818b7c7c1a5fd60c1b17496 100644 (file)
--- a/helm/software/components/tactics/paramodulation/equality.ml
+++ b/helm/software/components/tactics/paramodulation/equality.ml
@@ -67,6 +67,7 @@ let mk_equality (weight,p,(ty,l,r,o),m) =
   let id = freshid () in
   let eq = (uncomparable,weight,p,(ty,l,r,o),m,id) in
   Hashtbl.add id_to_eq id eq;
+
   eq
 ;;
 
@@ -108,6 +109,31 @@ let compare (_,_,_,s1,_,_) (_,_,_,s2,_,_) =
   Pervasives.compare s1 s2
 ;;
 
+let rec max_weight_in_proof current =
+  function
+   | Exact _ -> current
+   | Step (_, (_,id1,(_,id2),_)) ->
+       let eq1 = Hashtbl.find id_to_eq id1 in
+       let eq2 = Hashtbl.find id_to_eq id2 in  
+       let (w1,p1,(_,_,_,_),_,_) = open_equality eq1 in
+       let (w2,p2,(_,_,_,_),_,_) = open_equality eq2 in
+       let current = max current w1 in
+       let current = max_weight_in_proof current p1 in
+       let current = max current w2 in
+       max_weight_in_proof current p2
+
+let max_weight_in_goal_proof =
+  List.fold_left 
+    (fun current (_,_,id,_,_) ->
+       let eq = Hashtbl.find id_to_eq id in
+       let (w,p,(_,_,_,_),_,_) = open_equality eq in
+       let current = max current w in
+       max_weight_in_proof current p)
+
+let max_weight goal_proof proof =
+  let current = max_weight_in_proof 0 proof in
+  max_weight_in_goal_proof current goal_proof
+
 let proof_of_id id =
   try
     let (_,p,(_,l,r,_),_,_) = open_equality (Hashtbl.find id_to_eq id) in
@@ -536,7 +562,7 @@ let build_proof_step eq lift subst p1 p2 pos l r pred =
 let parametrize_proof p l r ty = 
   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 
+  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)