1. the default for the default equality/absurd/true/false URIs used to be

[helm.git] / helm / software / components / tactics / paramodulation / equality.ml

diff --git a/helm/software/components/tactics/paramodulation/equality.ml b/helm/software/components/tactics/paramodulation/equality.ml
index bceb3ebc2b150f6b6b27722f58f0b23277177a08..3bff5b57460bc4decc952b913a83f4c410fb4d29 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,15 +415,21 @@ 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 = 
   let eq,ty,l,r = open_eq ty in
   contextualize eq ty l r t
 ;;
-  
+
+let add_subst subst =
+  function
+    | Exact t -> Exact (Subst.apply_subst subst t)
+    | Step (s,(rule, id1, (pos,id2), pred)) -> 
+       Step (Subst.concat subst s,(rule, id1, (pos,id2), pred))
+;;
+       
 let build_proof_step ?(sym=false) lift subst p1 p2 pos l r pred =
   let p1 = Subst.apply_subst_lift lift subst p1 in
   let p2 = Subst.apply_subst_lift lift subst p2 in
@@ -720,14 +729,15 @@ let build_goal_proof l initial ty se =
           cic, p))
     lets (letsno-1,initial)
   in
-  canonical (contextualize_rewrites proof (CicSubstitution.lift letsno ty)), 
-   se
+    (proof,se)
+  (* canonical (contextualize_rewrites proof (CicSubstitution.lift letsno ty)),
+   se *)
 ;;
 
 let refl_proof ty term = 
   Cic.Appl 
     [Cic.MutConstruct 
-       (LibraryObjects.eq_URI (), 0, 1, []);
+       (Utils.eq_URI (), 0, 1, []);
        ty; term]
 ;;
 
@@ -754,6 +764,7 @@ let relocate newmeta menv to_be_relocated =
 let fix_metas newmeta eq = 
   let w, p, (ty, left, right, o), menv,_ = open_equality eq in
   let to_be_relocated = 
+(* List.map (fun i ,_,_ -> i) menv *)
     HExtlib.list_uniq 
       (List.sort Pervasives.compare 
          (Utils.metas_of_term left @ Utils.metas_of_term right)) 
@@ -901,14 +912,14 @@ let meta_convertibility t1 t2 =
 exception TermIsNotAnEquality;;
 
 let term_is_equality term =
-  let iseq uri = UriManager.eq uri (LibraryObjects.eq_URI ()) in
+  let iseq uri = UriManager.eq uri (Utils.eq_URI ()) in
   match term with
   | Cic.Appl [Cic.MutInd (uri, _, _); _; _; _] when iseq uri -> true
   | _ -> false
 ;;
 
 let equality_of_term proof term =
-  let eq_uri = LibraryObjects.eq_URI () in
+  let eq_uri = Utils.eq_URI () in
   let iseq uri = UriManager.eq uri eq_uri in
   match term with
   | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] when iseq uri ->
@@ -940,7 +951,7 @@ let term_of_equality equality =
   let argsno = List.length menv in
   let t =
     CicSubstitution.lift argsno
-      (Cic.Appl [Cic.MutInd (LibraryObjects.eq_URI (), 0, []); ty; left; right])
+      (Cic.Appl [Cic.MutInd (Utils.eq_URI (), 0, []); ty; left; right])
   in
   snd (
     List.fold_right