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 6c2a9b9dccfa83788706545862bc82c86690c8ba..dfb67583ec6836c6ddbb3aca8910f2dd1a8a3965 100644 (file)
--- a/helm/ocaml/tactics/paramodulation/inference.ml
+++ b/helm/ocaml/tactics/paramodulation/inference.ml
@@ -39,7 +39,7 @@ type equality =
     Cic.term list        (* arguments *)
 
 and proof =
-  | NoProof
+  | NoProof (* term is the goal missing a proof *)
   | BasicProof of Cic.term
   | ProofBlock of
       Cic.substitution * UriManager.uri *
@@ -70,7 +70,7 @@ let string_of_equality ?env =
 
 
 let rec string_of_proof = function
-  | NoProof -> "NoProof"
+  | NoProof -> "NoProof " 
   | BasicProof t -> "BasicProof " ^ (CicPp.ppterm t)
   | SubProof (t, i, p) ->
       Printf.sprintf "SubProof(%s, %s, %s)"
@@ -101,12 +101,12 @@ let build_ens_for_sym_eq sym_eq_URI termlist =
 ;;
 
 
-let build_proof_term proof =
+let build_proof_term ?(noproof=Cic.Implicit None) proof =
   let rec do_build_proof proof = 
     match proof with
     | NoProof ->
         Printf.fprintf stderr "WARNING: no proof!\n";
-        Cic.Implicit None
+        noproof
     | BasicProof term -> term
     | ProofGoalBlock (proofbit, proof) ->
         print_endline "found ProofGoalBlock, going up...";
@@ -191,11 +191,6 @@ exception NotMetaConvertible;;
 
 let meta_convertibility_aux table t1 t2 =
   let module C = Cic in
-  let print_table t =
-    String.concat ", "
-      (List.map
-         (fun (k, v) -> Printf.sprintf "(%d, %d)" k v) t)
-  in
   let rec aux ((table_l, table_r) as table) t1 t2 =
     match t1, t2 with
     | C.Meta (m1, tl1), C.Meta (m2, tl2) ->
@@ -309,16 +304,11 @@ let meta_convertibility_eq eq1 eq2 =
 
 
 let meta_convertibility t1 t2 =
-  let f t =
-    String.concat ", "
-      (List.map
-         (fun (k, v) -> Printf.sprintf "(%d, %d)" k v) t)
-  in
   if t1 = t2 then
     true
   else
     try
-      let l, r = meta_convertibility_aux ([], []) t1 t2 in
+      ignore(meta_convertibility_aux ([], []) t1 t2);
       true
     with NotMetaConvertible ->
       false
@@ -510,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
@@ -584,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
         )
@@ -648,7 +640,6 @@ let find_library_equalities dbd context status maxmeta =
   let candidates =
     List.fold_left
       (fun l uri ->
-       let suri = UriManager.string_of_uri uri in
          if UriManager.UriSet.mem uri blacklist then
            l
          else
@@ -727,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
@@ -806,8 +799,9 @@ let find_context_hypotheses env equalities_indexes =
 ;;
 
 
-let fix_metas newmeta ((w, p, (ty, left, right, o), menv, args) as equality) =
+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) ->
@@ -822,6 +816,7 @@ let fix_metas newmeta ((w, p, (ty, left, right, o), menv, args) as equality) =
          | _ -> assert false)
       args ([], newmeta+1)
   in
+
   let repl where =
     ProofEngineReduction.replace ~equality:(=) ~what:args ~with_what:newargs
       ~where
@@ -839,7 +834,7 @@ let fix_metas newmeta ((w, p, (ty, left, right, o), menv, args) as equality) =
   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
@@ -866,7 +861,7 @@ let fix_metas newmeta ((w, p, (ty, left, right, o), menv, args) as equality) =
         (Hashtbl.copy table)
   in
   let rec fix_proof = function
-    | NoProof -> NoProof
+    | NoProof -> NoProof 
     | BasicProof term -> BasicProof (repl term)
     | ProofBlock (subst, eq_URI, namety, bo, (pos, eq), p) ->
         let subst' =
@@ -891,10 +886,54 @@ let fix_metas newmeta ((w, p, (ty, left, right, o), menv, args) as equality) =
     | 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
@@ -921,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) as env) = function
-  | ((_, _, (ty, left, right, _), menv, _) as equality) ->
+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)))
 ;;