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/helm/software/components/tactics/autoTactic.ml b/helm/software/components/tactics/autoTactic.ml
index 7aabf9f3378321e8de1e1737d17afef25d421329..a9505d73919f1d33a929599b5741c59a930f4efb 100644 (file)
--- a/helm/software/components/tactics/autoTactic.ml
+++ b/helm/software/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/helm/software/components/tactics/paramodulation/equality.ml b/helm/software/components/tactics/paramodulation/equality.ml
index bceb3ebc2b150f6b6b27722f58f0b23277177a08..2561ea56f5a587549fdc89f6fb55fc56ecc8aece 100644 (file)
--- a/helm/software/components/tactics/paramodulation/equality.ml
+++ b/helm/software/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 =