Fixed a few bugs

[helm.git] / helm / software / components / ng_paramodulation / nCicProof.ml

diff --git a/helm/software/components/ng_paramodulation/nCicProof.ml b/helm/software/components/ng_paramodulation/nCicProof.ml
index 781b6bf08316b42efbff3365fe47c3eb8a919333..df6f949b603c867128b5d31634cf72091199ab9e 100644 (file)
--- a/helm/software/components/ng_paramodulation/nCicProof.ml
+++ b/helm/software/components/ng_paramodulation/nCicProof.ml
@@ -207,7 +207,7 @@ let debug c _ = c;;
               List.fold_left
                (fun (i,acc) t ->
                  i+1,
-                             let f = extract amount vl f in
+                      let f = extract amount vl f in
                   if i = n then
                    let imp = NCic.Implicit `Term in
                     NCic.Appl (dag::imp::imp::imp(* f *)::imp::imp::
@@ -218,7 +218,7 @@ let debug c _ = c;;
     in aux ft (List.rev pl)
     ;;
 
-  (* we should better split forward and backard rewriting *)
+  (* we should better split forward and backward rewriting *)
   let mk_proof ?(demod=false) (bag : NCic.term Terms.bag) mp subst steps =
     let module NCicBlob = 
        NCicBlob.NCicBlob(
@@ -264,6 +264,26 @@ let debug c _ = c;;
       let lit,_,_ = get_literal mp in
       let lit = Subst.apply_subst subst lit in
         extract 0 [] lit in
+    (* composition of all subst acting on goal *)
+    let res_subst =
+      let rec rsaux ongoal acc = 
+       function
+         | [] -> acc (* is the final subst for refl *)
+         | id::tl when ongoal ->
+            let lit,vl,proof = get_literal id in
+             (match proof with
+               | Terms.Exact _ -> rsaux ongoal acc tl
+               | Terms.Step (_, _, _, _, _, s) ->
+                   rsaux ongoal (s@acc) tl)
+         | id::tl -> 
+           (* subst is the the substitution for refl *)
+           rsaux (id=mp) subst tl
+      in 
+      let r = rsaux false [] steps in
+       (* prerr_endline ("res substitution: " ^ Pp.pp_substitution r);
+           prerr_endline ("\n" ^ "subst: " ^ Pp.pp_substitution subst); *)
+      r
+    in
     let rec aux ongoal seen = function
       | [] -> NCic.Rel 1
       | id :: tl ->
@@ -305,10 +325,12 @@ let debug c _ = c;;
               let id, id1,(lit,vl,proof) =
                 if ongoal then
                  let lit,vl,proof = get_literal id1 in
-                 id1,id,(Subst.apply_subst subst lit, 
-                         Subst.filter subst vl, proof)
+                 id1,id,(Subst.apply_subst res_subst lit, 
+                         Subst.filter res_subst vl, proof)
                 else id,id1,(lit,vl,proof) in
-              let vl = if ongoal then [] else vl in
+              (* free variables remaining in the goal should not
+                 be abstracted: we do not want to prove a generalization *)
+              let vl = if ongoal then [] else vl in 
               let proof_of_id id = 
                 let vars = List.rev (vars_of id seen) in
                 let args = List.map (Subst.apply_subst subst) vars in
@@ -388,7 +410,8 @@ let debug c _ = c;;
               let body = aux ongoal 
                 ((id,(List.map (fun x -> Terms.Var x) vl,lit))::seen) tl 
               in 
-                if NCicUntrusted.count_occurrences [] 0 body <= 1 then
+             let occ= NCicUntrusted.count_occurrences [] 1 body in
+               if occ <= 1 then
                   NCicSubstitution.subst 
                     ~avoid_beta_redexes:true ~no_implicit:false
                     (close_with_lambdas vl rewrite_step) body