From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Thu, 4 Mar 2010 07:52:45 +0000 (+0000)
Subject: Corrected a bug relative to the application of substs in the "on goal"
X-Git-Tag: make_still_working~3018
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c471db7f3e949af87d9206861d9b36a13dfce45a;p=helm.git

Corrected a bug relative to the application of substs in the "on goal"
case.
---

diff --git a/helm/software/components/ng_paramodulation/nCicProof.ml b/helm/software/components/ng_paramodulation/nCicProof.ml
index b80ac7e9c..b5f4af9d6 100644
--- a/helm/software/components/ng_paramodulation/nCicProof.ml
+++ b/helm/software/components/ng_paramodulation/nCicProof.ml
@@ -12,7 +12,7 @@
 (* $Id: orderings.ml 9869 2009-06-11 22:52:38Z denes $ *)
 
 type eq_sig_type = Eq | EqInd_l | EqInd_r | Refl
-
+              
 let eqsig = ref (fun _ -> assert false);;
 let set_sig f = eqsig:= f;;
 let get_sig = fun x -> !eqsig x;;
@@ -219,6 +219,14 @@ let debug c _ = c;;
     ;;
 
   let mk_proof (bag : NCic.term Terms.bag) mp subst steps =
+    let module NCicBlob = 
+       NCicBlob.NCicBlob(
+	 struct
+	   let metasenv = [] let subst = [] let context = []
+	 end)
+     in
+     let  module Pp = Pp.Pp(NCicBlob) 
+     in
     let module Subst = FoSubst in
     let position i l = 
       let rec aux = function
@@ -261,11 +269,11 @@ let debug c _ = c;;
           let amount = List.length seen in
           let lit,vl,proof = get_literal id in
           if not ongoal && id = mp then
-            let lit = Subst.apply_subst subst lit in
+            let lit = Subst.apply_subst subst lit in 
             let eq_ty = extract amount [] lit in
             let refl = mk_refl eq_ty in
-             (*prerr_endline ("Reached m point, id=" ^ (string_of_int id));*)
-             (* (NCic.LetIn ("clause_" ^ string_of_int id, eq_ty, refl,
+             (* prerr_endline ("Reached m point, id=" ^ (string_of_int id));
+                (NCic.LetIn ("clause_" ^ string_of_int id, eq_ty, refl,
                 aux true ((id,([],lit))::seen) (id::tl))) *)
               NCicSubstitution.subst 
                 ~avoid_beta_redexes:true ~no_implicit:false refl
@@ -277,8 +285,8 @@ let debug c _ = c;;
               aux ongoal seen tl
           | Terms.Step _ when tl=[] -> assert false
           | Terms.Exact ft ->
-              (* prerr_endline ("Exact for " ^ (string_of_int id));*)
-              (*
+	      (*
+               prerr_endline ("Exact for " ^ (string_of_int id));
                NCic.LetIn ("clause_" ^ string_of_int id, 
                  close_with_forall vl (extract amount vl lit),
                  close_with_lambdas vl (extract amount vl ft),
@@ -292,10 +300,12 @@ let debug c _ = c;;
                    ((id,(List.map (fun x -> Terms.Var x) vl,lit))::seen) tl)
           | Terms.Step (_, id1, id2, dir, pos, subst) ->
               let id, id1,(lit,vl,proof) =
-                if ongoal then id1,id,get_literal id1
-                else id,id1,(lit,vl,proof)
-              in
-              let vl = if ongoal then [](*Subst.filter subst vl*) else vl in
+                if ongoal then
+		  let lit,vl,proof = get_literal id1 in
+		  id1,id,(Subst.apply_subst subst lit, 
+			  Subst.filter subst vl, proof)
+                else id,id1,(lit,vl,proof) in
+              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
@@ -347,12 +357,15 @@ let debug c _ = c;;
                       extract amount vl (Subst.apply_subst subst r)
                   | _ -> assert false
                 in
-                  (*prerr_endline "mk_predicate :";
+		  (*
+                  prerr_endline "mk_predicate :";
                   if ongoal then prerr_endline "ongoal=true"
                   else prerr_endline "ongoal=false";
                   prerr_endline ("id=" ^ string_of_int id);
-                  prerr_endline ("id1=" ^ string_of_int id1);
-                  prerr_endline ("id2=" ^ string_of_int id2);
+                  prerr_endline ("id1=" ^ string_of_int id1 
+				 ^": " ^ Pp.pp_foterm id1_ty);
+                  prerr_endline ("id2=" ^ string_of_int id2
+				 ^ ": " ^ NCicPp.ppterm [][][] id2_ty);
                   prerr_endline ("Positions :" ^
                                    (String.concat ", "
                                       (List.map string_of_int pos)));*)