X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2FnCicProof.ml;h=c5290694bfd96a4c5179b70eaeb665d8a742d3d7;hb=72e835f5e6848c09faf6343fb7e276c88bfc1f2e;hp=781b6bf08316b42efbff3365fe47c3eb8a919333;hpb=8c678be0b7ee11a60f21b002553cc414f1d18267;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/nCicProof.ml b/helm/software/components/ng_paramodulation/nCicProof.ml
index 781b6bf08..c5290694b 100644
--- 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,6 @@ let debug c _ = c;;
     in aux ft (List.rev pl)
     ;;
 
-  (* we should better split forward and backard rewriting *)
   let mk_proof ?(demod=false) (bag : NCic.term Terms.bag) mp subst steps =
     let module NCicBlob = 
        NCicBlob.NCicBlob(
@@ -254,7 +253,7 @@ let debug c _ = c;;
     let get_literal id =
       let (_, lit, vl, proof),_,_ = Terms.get_from_bag id bag in
       let lit =match lit with 
-          | Terms.Predicate t -> assert false 
+          | Terms.Predicate t -> t (* assert false *) 
           | Terms.Equation (l,r,ty,_) -> 
               Terms.Node [ Terms.Leaf eqP(); ty; l; r]
       in
@@ -264,6 +263,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 +324,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 +409,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