From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 31 May 2006 13:54:36 +0000 (+0000)
Subject: fixed proofs, contextualization should now work.
X-Git-Tag: 0.4.95@7852~1376
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f36b907612b05a95aba0f9e96030def1609bdadb;p=helm.git

fixed proofs, contextualization should now work.
the empty context is not a term with an open (Rel 1), but a
a term with a (Cic.Implicit(Some `Hole)) so that it can't bw confused with a
Rel to the last Hypothesis.
---

diff --git a/components/tactics/autoTactic.ml b/components/tactics/autoTactic.ml
index 7aabf9f33..a9505d739 100644
--- a/components/tactics/autoTactic.ml
+++ b/components/tactics/autoTactic.ml
@@ -340,7 +340,9 @@ let auto_tac ?(depth=default_depth) ?(width=default_width) ?paramodulation
       debug_print (lazy "USO PARAMODULATION...");
 (*       try *)
       try
-        Saturation.saturate dbd ~depth ~width ~full (proof, goal)
+        let rc = Saturation.saturate dbd ~depth ~width ~full (proof, goal) in
+        prerr_endline (Saturation.get_stats ());
+        rc
       with exn ->
         prerr_endline (Saturation.get_stats ());
         raise exn
diff --git a/components/tactics/paramodulation/equality.ml b/components/tactics/paramodulation/equality.ml
index bceb3ebc2..2561ea56f 100644
--- a/components/tactics/paramodulation/equality.ml
+++ b/components/tactics/paramodulation/equality.ml
@@ -305,12 +305,12 @@ let ty_of_lambda = function
 
 let compose_contexts ctx1 ctx2 = 
   ProofEngineReduction.replace_lifting 
-    ~equality:(=) ~what:[Cic.Rel 1] ~with_what:[ctx2] ~where:ctx1
+    ~equality:(=) ~what:[Cic.Implicit(Some `Hole)] ~with_what:[ctx2] ~where:ctx1
 ;;
 
 let put_in_ctx ctx t = 
   ProofEngineReduction.replace_lifting
-    ~equality:(=) ~what:[Cic.Rel 1] ~with_what:[t] ~where:ctx
+    ~equality:(=) ~what:[Cic.Implicit (Some `Hole)] ~with_what:[t] ~where:ctx
 ;;
 
 let mk_eq uri ty l r =
@@ -328,13 +328,14 @@ let open_eq = function
 ;;
 
 let contextualize uri ty left right t = 
+  let hole = Cic.Implicit (Some `Hole) in
   (* aux [uri] [ty] [left] [right] [ctx] [t] 
    * 
    * the parameters validate this invariant  
    *   t: eq(uri) ty left right
    * that is used only by the base case
    *
-   * ctx is a term with an open (Rel 1). (Rel 1) is the empty context
+   * ctx is a term with an hole. Cic.Implicit(Some `Hole) is the empty context
    *)
     let rec aux uri ty left right ctx_d = function
       | Cic.Appl ((Cic.Const(uri_sym,ens))::tl) 
@@ -358,7 +359,7 @@ let contextualize uri ty left right t =
             let m, ctx_c = if is_not_fixed_lp then rp,lp else lp,rp in
             (* they were under a lambda *)
             let m =  CicSubstitution.subst (Cic.Implicit None) m in
-            let ctx_c = CicSubstitution.subst (Cic.Rel 1) ctx_c in
+            let ctx_c = CicSubstitution.subst hole ctx_c in
             m, ctx_c          
           in
           (* create the compound context and put the terms under it *)
@@ -400,9 +401,11 @@ let contextualize uri ty left right t =
         let uri_ind = LibraryObjects.eq_ind_URI ~eq:uri in
         let pred = 
           (* ctx_d will go under a lambda, but put_in_ctx substitutes Rel 1 *)
-          let ctx_d = CicSubstitution.lift_from 2 1 ctx_d in (* bleah *)
-          let r = put_in_ctx ctx_d (CicSubstitution.lift 1 left) in
-          let l = ctx_d in
+          let r = CicSubstitution.lift 1 (put_in_ctx ctx_d left) in
+          let l = 
+            let ctx_d = CicSubstitution.lift 1 ctx_d in
+            put_in_ctx ctx_d (Cic.Rel 1)
+          in
           let lty = CicSubstitution.lift 1 ty in 
           Cic.Lambda (Cic.Name "foo",ty,(mk_eq uri lty l r))
         in
@@ -412,8 +415,7 @@ let contextualize uri ty left right t =
         mk_sym uri_sym ty d_right d_left
           (mk_eq_ind uri_ind ty left pred refl_eq right t)
   in
-  let empty_context = Cic.Rel 1 in
-  aux uri ty left right empty_context t
+  aux uri ty left right hole t
 ;;
 
 let contextualize_rewrites t ty =