removed no longer used METAs

[helm.git] / helm / ocaml / tactics / paramodulation / inference.ml

diff --git a/helm/ocaml/tactics/paramodulation/inference.ml b/helm/ocaml/tactics/paramodulation/inference.ml
index f22b49ceedfbb1e15345f37a1594b546a14a6a81..dfb67583ec6836c6ddbb3aca8910f2dd1a8a3965 100644 (file)
--- a/helm/ocaml/tactics/paramodulation/inference.ml
+++ b/helm/ocaml/tactics/paramodulation/inference.ml
@@ -500,7 +500,7 @@ let matching metasenv context t1 t2 ugraph =
 try
           unification metasenv context t1 t2 ugraph
 with CicUtil.Meta_not_found _ as exn ->
- Printf.eprintf "t1 = %s\nt2 = %s\nmetasenv = %s\n%!"
+ Printf.eprintf "t1 == %s\nt2 = %s\nmetasenv == %s\n%!"
   (CicPp.ppterm t1) (CicPp.ppterm t2) (CicMetaSubst.ppmetasenv [] metasenv);
  raise exn
       in
@@ -574,7 +574,9 @@ let find_equalities context proof =
           match do_find context term with
           | Some p, newmeta ->
               let tl, newmeta' = (aux (index+1) newmeta tl) in
-              (index, p)::tl, max newmeta newmeta'
+             if newmeta' < newmeta then 
+               prerr_endline "big trouble";
+              (index, p)::tl, newmeta' (* max???? *)
           | None, _ ->
               aux (index+1) newmeta tl
         )
@@ -716,7 +718,9 @@ let find_library_equalities dbd context status maxmeta =
         match res with
         | Some e ->
             let tl, newmeta' = aux newmeta tl in
-            (uri, e)::tl, max newmeta newmeta'
+             if newmeta' < newmeta then 
+               prerr_endline "big trouble";
+              (uri, e)::tl, newmeta' (* max???? *)
         | None ->
             aux newmeta tl
   in
@@ -795,8 +799,9 @@ let find_context_hypotheses env equalities_indexes =
 ;;
 
 
-let fix_metas newmeta (w, p, (ty, left, right, o), menv, args) =
+let fix_metas_old newmeta (w, p, (ty, left, right, o), menv, args) =
   let table = Hashtbl.create (List.length args) in
+
   let newargs, newmeta =
     List.fold_right
       (fun t (newargs, index) ->
@@ -811,6 +816,7 @@ let fix_metas newmeta (w, p, (ty, left, right, o), menv, args) =
          | _ -> assert false)
       args ([], newmeta+1)
   in
+
   let repl where =
     ProofEngineReduction.replace ~equality:(=) ~what:args ~with_what:newargs
       ~where
@@ -828,7 +834,7 @@ let fix_metas newmeta (w, p, (ty, left, right, o), menv, args) =
   let ty = repl ty
   and left = repl left
   and right = repl right in
-  let metas = (metas_of_term left) @ (metas_of_term right) in
+  let metas = (metas_of_term left) @ (metas_of_term right) @ (metas_of_term ty) in
   let menv' = List.filter (fun (i, _, _) -> List.mem i metas) menv' in
   let newargs =
     List.filter
@@ -880,10 +886,54 @@ let fix_metas newmeta (w, p, (ty, left, right, o), menv, args) =
     | p -> assert false
   in
   let neweq = (w, fix_proof p, (ty, left, right, o), menv', newargs) in
-  (newmeta + 1, neweq)
+  (newmeta +1, neweq)
 ;;
 
 
+let relocate newmeta menv =
+  let subst, metasenv, newmeta = 
+    List.fold_right 
+      (fun (i, context, ty) (subst, menv, maxmeta) -> 
+        let irl=CicMkImplicit.identity_relocation_list_for_metavariable context in
+        let newsubst = (i, (context, (Cic.Meta (maxmeta, irl)), ty)) in
+        let newmeta = maxmeta, context, ty in
+        newsubst::subst, newmeta::menv, maxmeta+1) 
+      menv ([], [], newmeta+1)
+  in
+  let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
+  let subst =
+    List.map
+      (fun (i, (context, term, ty)) ->
+        let context = CicMetaSubst.apply_subst_context subst context in
+        let term = CicMetaSubst.apply_subst subst term in
+        let ty = CicMetaSubst.apply_subst subst ty in  
+        (i, (context, term, ty))) subst in
+  subst, metasenv, newmeta
+
+
+let fix_metas newmeta (w, p, (ty, left, right, o), menv, args) =
+  (* debug 
+  let _ , eq = 
+    fix_metas_old newmeta (w, p, (ty, left, right, o), menv, args) in
+  prerr_endline (string_of_equality eq); *)
+  let subst, metasenv, newmeta = relocate newmeta menv in
+  let ty = CicMetaSubst.apply_subst subst ty in
+  let left = CicMetaSubst.apply_subst subst left in
+  let right = CicMetaSubst.apply_subst subst right in
+  let args = List.map (CicMetaSubst.apply_subst subst) args in
+  let rec fix_proof = function
+    | NoProof -> NoProof 
+    | BasicProof term -> BasicProof (CicMetaSubst.apply_subst subst term)
+    | ProofBlock (subst', eq_URI, namety, bo, (pos, eq), p) ->
+        ProofBlock (subst' @ subst, eq_URI, namety, bo, (pos, eq), p)
+    | p -> assert false
+  in
+  let metas = (metas_of_term left)@(metas_of_term right)@(metas_of_term ty) in
+  let metasenv = List.filter (fun (i, _, _) -> List.mem i metas) metasenv in
+  let eq = (w, fix_proof p, (ty, left, right, o), metasenv, args) in
+  (* debug prerr_endline (string_of_equality eq); *)
+  newmeta, eq  
+
 let term_is_equality term =
   let iseq uri = UriManager.eq uri (LibraryObjects.eq_URI ()) in
   match term with
@@ -910,12 +960,21 @@ let equality_of_term proof term =
 
 type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph;;
 
+let is_weak_identity (metasenv, context, ugraph) = function
+  | (_, _, (ty, left, right, _), menv, _) -> 
+       (left = right ||
+          (meta_convertibility left right)) 
+          (* the test below is not a good idea since it stops
+             demodulation too early *)
+           (* (fst (CicReduction.are_convertible 
+                 ~metasenv:(metasenv @ menv) context left right ugraph)))*)
+;;
 
 let is_identity (metasenv, context, ugraph) = function
   | (_, _, (ty, left, right, _), menv, _) ->
        (left = right ||
-          (* (meta_convertibility left right) || *)
-          (fst (CicReduction.are_convertible 
+          (* (meta_convertibility left right)) *)
+           (fst (CicReduction.are_convertible 
                  ~metasenv:(metasenv @ menv) context left right ugraph)))
 ;;