Axioms were not indexed.

[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 b80ac7e9ce7007aa8c83c1da55c8d4a477b9021a..df6f949b603c867128b5d31634cf72091199ab9e 100644 (file)
--- 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;;
@@ -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,16 @@ let debug c _ = c;;
     in aux ft (List.rev pl)
     ;;
 
-  let mk_proof (bag : NCic.term Terms.bag) mp subst steps =
+  (* 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(
+        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
@@ -255,17 +264,39 @@ 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 ->
           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,
+            let refl = 
+             if demod then NCic.Implicit `Term 
+             else 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,
                 aux true ((id,([],lit))::seen) (id::tl))) *)
               NCicSubstitution.subst 
                 ~avoid_beta_redexes:true ~no_implicit:false refl
@@ -277,8 +308,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 +323,14 @@ 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 res_subst lit, 
+                         Subst.filter res_subst vl, proof)
+                else id,id1,(lit,vl,proof) 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
@@ -347,12 +382,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)));*)
@@ -372,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