fixed LetIn proofs

diff --git a/components/tactics/paramodulation/equality.ml b/components/tactics/paramodulation/equality.ml
index c31538bda7595dd0b223311d8ee2bc7049dfd262..57c440860a78dc3016ba1b3c11917861d9b13a5b 100644 (file)
--- a/components/tactics/paramodulation/equality.ml
+++ b/components/tactics/paramodulation/equality.ml
@@ -422,8 +422,11 @@ let build_proof_step lift subst p1 p2 pos l r pred =
         mk_eq_ind (Utils.eq_ind_r_URI ()) ty what pred p1 other p2
 ;;
 
-let parametrize_proof p ty = 
-  let parameters = CicUtil.metas_of_term p in (* ?if they are under a lambda? *)
+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 parameters = 
     HExtlib.list_uniq (List.sort Pervasives.compare parameters) 
   in
@@ -434,7 +437,7 @@ let parametrize_proof p ty =
   let p = CicSubstitution.lift (lift_no-1) p in
   let p = 
     ProofEngineReduction.replace_lifting
-    ~equality:(=) ~what ~with_what ~where:p
+    ~equality:(fun t1 t2 -> match t1,t2 with Cic.Meta (i,_),Cic.Meta(j,_) -> i=j | _ -> false) ~what ~with_what ~where:p
   in
   let ty_of_m _ = ty (*function 
     | Cic.Meta (i,_) -> List.assoc i menv 
@@ -502,17 +505,19 @@ let get_duplicate_step_in_wfo l p =
   let add i n = 
     let p,_,_ = proof_of_id i in 
     match p with 
-    | Exact _ -> ()
+    | Exact _ -> true
     | _ -> 
-        try let (pos,no) = Hashtbl.find h i in Hashtbl.replace h i (pos,no+1)
-        with Not_found -> Hashtbl.add h i (n,1)
+        try let (pos,no) = Hashtbl.find h i in Hashtbl.replace h i (pos,no+1);false
+        with Not_found -> Hashtbl.add h i (n,1);true
   in
   let rec aux n = function
     | Exact _ -> n
     | Step (_,(_,i1,(_,i2),_)) -> 
-        add i1 n;add i2 n;
-        max (aux (n+1) (let p,_,_ = proof_of_id i1 in p))
-          (aux (n+1) (let p,_,_ = proof_of_id i2 in p))
+       let go_on_1 = add i1 n in
+       let go_on_2 = add i2 n in
+        max 
+         (if go_on_1 then aux (n+1) (let p,_,_ = proof_of_id i1 in p) else n+1)
+         (if go_on_2 then aux (n+1) (let p,_,_ = proof_of_id i2 in p) else n+1)
   in
   let i = aux 0 p in 
   let _ = 
@@ -537,9 +542,6 @@ let build_proof_term h lift proof =
   let rec aux = function
      | Exact term -> CicSubstitution.lift lift term
      | Step (subst,(_, id1, (pos,id2), pred)) ->
-         if Subst.is_in_subst 9 subst then
-           prerr_endline (Printf.sprintf "ID %d-%d has: %s\n" id1 id2 (Subst.ppsubst
-           subst));
          let p1,_,_ = proof_of_id aux id1 in
          let p2,l,r = proof_of_id aux id2 in
            build_proof_step lift subst p1 p2 pos l r pred
@@ -557,10 +559,10 @@ let build_goal_proof l initial ty se =
   let lets,_,h = 
     List.fold_left
       (fun (acc,n,h) id -> 
-        let p,_,_ = proof_of_id id in
+        let p,l,r = proof_of_id id in
         let cic = build_proof_term h n p in
         let real_cic,instance = 
-          parametrize_proof cic (CicSubstitution.lift n mty)
+          parametrize_proof cic l r (CicSubstitution.lift n mty)
         in
         let h = (id, instance)::lift_list h in
         acc@[id,real_cic],n+1,h) 

diff --git a/components/tactics/paramodulation/inference.ml b/components/tactics/paramodulation/inference.ml
index ccc73c351e3d8f422b33a90007f4f9db44095e07..ab27f8a314b13e4b75cce13afbd272a7f9440475 100644 (file)
--- a/components/tactics/paramodulation/inference.ml
+++ b/components/tactics/paramodulation/inference.ml
@@ -488,4 +488,5 @@ let find_context_hypotheses env equalities_indexes =
   in
   res
 ;;
+
 let get_stats () = <:show<Inference.>> ;;

diff --git a/components/tactics/paramodulation/saturation.ml b/components/tactics/paramodulation/saturation.ml
index b5b727b4d42d55554dc05e70969ba667f500e205..445eccdbc2f217565c67b5f319cb2652c105066e 100644 (file)
--- a/components/tactics/paramodulation/saturation.ml
+++ b/components/tactics/paramodulation/saturation.ml
@@ -1771,6 +1771,7 @@ let saturate
         let initial = newproof in
         Equality.build_goal_proof goalproof initial type_of_goal side_effects
       in
+prerr_endline (CicPp.pp goal_proof names);
       let goal_proof = Subst.apply_subst subsumption_subst goal_proof in
       let side_effects_t = 
         List.map (Subst.apply_subst subsumption_subst) side_effects_t