X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Finference.ml;h=ac80099b06b3602b3905330949f37cbd37896994;hb=2eaee49a7ff3ed74598a0db84ce4dbc5bca92380;hp=6004de44ceb29ef815daf390b824678aa8863ef3;hpb=3df775cea96aae2d25dd9b47f9491711abc1c8fb;p=helm.git

diff --git a/helm/software/components/tactics/paramodulation/inference.ml b/helm/software/components/tactics/paramodulation/inference.ml
index 6004de44c..ac80099b0 100644
--- a/helm/software/components/tactics/paramodulation/inference.ml
+++ b/helm/software/components/tactics/paramodulation/inference.ml
@@ -23,13 +23,15 @@
  * http://cs.unibo.it/helm/.
  *)
 
-let _profiler = <:profiler<_profiler>>;;
+(* let _profiler = <:profiler<_profiler>>;; *)
 
 (* $Id$ *)
 
 open Utils;;
 open Printf;;
 
+let debug_print s = ();;(*prerr_endline (Lazy.force s);;*)
+
 let check_disjoint_invariant subst metasenv msg =
   if (List.exists 
         (fun (i,_,_) -> (Subst.is_in_subst i subst)) metasenv)
@@ -70,7 +72,7 @@ let unification_simple locked_menv metasenv context t1 t2 ugraph =
   let lookup = Subst.lookup_subst in
   let rec occurs_check subst what where =
     match where with
-    | t when what = t -> true
+    | Cic.Meta(i,_) when i = what -> true
     | C.Appl l -> List.exists (occurs_check subst what) l
     | C.Meta _ ->
         let t = lookup where subst in
@@ -84,6 +86,9 @@ let unification_simple locked_menv metasenv context t1 t2 ugraph =
     in
     match s, t with
     | s, t when s = t -> subst, menv
+    (* sometimes the same meta has different local contexts; this
+       could create "cyclic" substitutions *)
+    | C.Meta (i, _), C.Meta (j, _) when i=j ->  subst, menv
     | C.Meta (i, _), C.Meta (j, _) 
         when (locked locked_menv i) &&(locked locked_menv j) ->
         raise
@@ -92,7 +97,7 @@ let unification_simple locked_menv metasenv context t1 t2 ugraph =
         unif subst menv t s
     | C.Meta (i, _), C.Meta (j, _) when (i > j) && not (locked locked_menv j) ->
         unif subst menv t s
-    | C.Meta _, t when occurs_check subst s t ->
+    | C.Meta (i,_), t when occurs_check subst i t ->
         raise
           (U.UnificationFailure (lazy "Inference.unification.unif"))
     | C.Meta (i, l), t when (locked locked_menv i) -> 
@@ -193,303 +198,4 @@ let unification m1 m2 c t1 t2 ug =
     raise exn
 ;;
 
-
-let check_eq context msg eq =
-  let w, proof, (eq_ty, left, right, order), metas = eq in
-  if not (fst (CicReduction.are_convertible ~metasenv:metas context eq_ty
-   (fst (CicTypeChecker.type_of_aux' metas context  left CicUniv.empty_ugraph))
-   CicUniv.empty_ugraph))
-  then
-    begin
-      prerr_endline msg;
-      assert false;
-    end
-  else ()
-;;
-
-let find_equalities context proof =
-  let module C = Cic in
-  let module S = CicSubstitution in
-  let module T = CicTypeChecker in
-  let eq_uri = Utils.eq_URI () in
-  let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in
-  let ok_types ty menv =
-    List.for_all (fun (_, _, mt) -> mt = ty) menv
-  in
-  let rec aux index newmeta = function
-    | [] -> [], newmeta
-    | (Some (_, C.Decl (term)))::tl ->
-        let do_find context term =
-          match term with
-          | C.Prod (name, s, t) ->
-              let (head, newmetas, args, newmeta) =
-                ProofEngineHelpers.saturate_term newmeta []
-                  context (S.lift index term) 0
-              in
-              let p =
-                if List.length args = 0 then
-                  C.Rel index
-                else
-                  C.Appl ((C.Rel index)::args)
-              in (
-                match head with
-                | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
-                    when (UriManager.eq uri eq_uri) && (ok_types ty newmetas) ->
-                    debug_print
-                      (lazy
-                         (Printf.sprintf "OK: %s" (CicPp.ppterm term)));
-                    let o = !Utils.compare_terms t1 t2 in
-                    let stat = (ty,t1,t2,o) in
-                    let w = compute_equality_weight stat in
-                    let proof = Equality.Exact p in
-                    let e = Equality.mk_equality (w, proof, stat, newmetas) in
-                    Some e, (newmeta+1)
-                | _ -> None, newmeta
-              )
-          | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
-              when UriManager.eq uri eq_uri ->
-              let ty = S.lift index ty in
-              let t1 = S.lift index t1 in
-              let t2 = S.lift index t2 in
-              let o = !Utils.compare_terms t1 t2 in
-              let stat = (ty,t1,t2,o) in
-              let w = compute_equality_weight stat in
-              let p = C.Rel index in
-              let proof = Equality.Exact p in
-              let e = Equality.mk_equality (w, proof,stat,[]) in
-              Some e, (newmeta+1)
-          | _ -> None, newmeta
-        in (
-          match do_find context term with
-          | Some p, newmeta ->
-              let tl, newmeta' = (aux (index+1) newmeta tl) in
-              if newmeta' < newmeta then 
-                prerr_endline "big trouble";
-              (index, p)::tl, newmeta' (* max???? *)
-          | None, _ ->
-              aux (index+1) newmeta tl
-        )
-    | _::tl ->
-        aux (index+1) newmeta tl
-  in
-  let il, maxm = aux 1 newmeta context in
-  let indexes, equalities = List.split il in
-  (* ignore (List.iter (check_eq context "find") equalities); *)
-  indexes, equalities, maxm
-;;
-
-
-(*
-let equations_blacklist =
-  List.fold_left
-    (fun s u -> UriManager.UriSet.add (UriManager.uri_of_string u) s)
-    UriManager.UriSet.empty [
-      "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)";
-      "cic:/Coq/Init/Logic/trans_eq.con";
-      "cic:/Coq/Init/Logic/f_equal.con";
-      "cic:/Coq/Init/Logic/f_equal2.con";
-      "cic:/Coq/Init/Logic/f_equal3.con";
-      "cic:/Coq/Init/Logic/f_equal4.con";
-      "cic:/Coq/Init/Logic/f_equal5.con";
-      "cic:/Coq/Init/Logic/sym_eq.con";
-      "cic:/Coq/Init/Logic/eq_ind.con";
-      "cic:/Coq/Init/Logic/eq_ind_r.con";
-      "cic:/Coq/Init/Logic/eq_rec.con";
-      "cic:/Coq/Init/Logic/eq_rec_r.con";
-      "cic:/Coq/Init/Logic/eq_rect.con";
-      "cic:/Coq/Init/Logic/eq_rect_r.con";
-      "cic:/Coq/Logic/Eqdep/UIP.con";
-      "cic:/Coq/Logic/Eqdep/UIP_refl.con";
-      "cic:/Coq/Logic/Eqdep_dec/eq2eqT.con";
-      "cic:/Coq/ZArith/Zcompare/rename.con";
-      (* ALB !!!! questo e` imbrogliare, ma x ora lo lasciamo cosi`...
-         perche' questo cacchio di teorema rompe le scatole :'( *)
-      "cic:/Rocq/SUBST/comparith/mult_n_2.con";
-
-      "cic:/matita/logic/equality/eq_f.con";
-      "cic:/matita/logic/equality/eq_f2.con";
-      "cic:/matita/logic/equality/eq_rec.con";
-      "cic:/matita/logic/equality/eq_rect.con";
-    ]
-;;
-*)
-let equations_blacklist = UriManager.UriSet.empty;;
-
-
-let find_library_equalities dbd context status maxmeta = 
-  let module C = Cic in
-  let module S = CicSubstitution in
-  let module T = CicTypeChecker in
-  let blacklist =
-    List.fold_left
-      (fun s u -> UriManager.UriSet.add u s)
-      equations_blacklist
-      [eq_XURI (); sym_eq_URI (); trans_eq_URI (); eq_ind_URI ();
-       eq_ind_r_URI ()]
-  in
-  let candidates =
-    List.fold_left
-      (fun l uri ->
-         if UriManager.UriSet.mem uri blacklist then
-           l
-         else
-           let t = CicUtil.term_of_uri uri in
-           let ty, _ =
-             CicTypeChecker.type_of_aux' [] context t CicUniv.empty_ugraph
-           in
-           (uri, t, ty)::l)
-      []
-      (let t1 = Unix.gettimeofday () in
-       let eqs = (MetadataQuery.equations_for_goal ~dbd status) in
-       let t2 = Unix.gettimeofday () in
-       (debug_print
-          (lazy
-             (Printf.sprintf "Tempo di MetadataQuery.equations_for_goal: %.9f\n"
-                (t2 -. t1))));
-       eqs)
-  in
-  let eq_uri1 = eq_XURI ()
-  and eq_uri2 = Utils.eq_URI () in
-  let iseq uri =
-    (UriManager.eq uri eq_uri1) || (UriManager.eq uri eq_uri2)
-  in
-  let ok_types ty menv =
-    List.for_all (fun (_, _, mt) -> mt = ty) menv
-  in
-  let rec has_vars = function
-    | C.Meta _ | C.Rel _ | C.Const _ -> false
-    | C.Var _ -> true
-    | C.Appl l -> List.exists has_vars l
-    | C.Prod (_, s, t) | C.Lambda (_, s, t)
-    | C.LetIn (_, s, t) | C.Cast (s, t) ->
-        (has_vars s) || (has_vars t)
-    | _ -> false
- in
-  let rec aux newmeta = function
-    | [] -> [], newmeta
-    | (uri, term, termty)::tl ->
-        debug_print
-          (lazy
-             (Printf.sprintf "Examining: %s (%s)"
-                (CicPp.ppterm term) (CicPp.ppterm termty)));
-        let res, newmeta = 
-          match termty with
-          | C.Prod (name, s, t) when not (has_vars termty) ->
-              let head, newmetas, args, newmeta =
-                ProofEngineHelpers.saturate_term newmeta [] context termty 0
-              in
-              let p =
-                if List.length args = 0 then
-                  term
-                else
-                  C.Appl (term::args)
-              in (
-                  match head with
-                    | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
-                        when (iseq uri) && (ok_types ty newmetas) ->
-                    debug_print
-                      (lazy
-                         (Printf.sprintf "OK: %s" (CicPp.ppterm term)));
-                    let o = !Utils.compare_terms t1 t2 in
-                    let stat = (ty,t1,t2,o) in
-                    let w = compute_equality_weight stat in
-                    let proof = Equality.Exact p in
-                    let e = Equality.mk_equality (w, proof, stat, newmetas) in
-                    Some e, (newmeta+1)
-                | _ -> None, newmeta
-              )
-          | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
-              when iseq uri && not (has_vars termty) ->
-              let o = !Utils.compare_terms t1 t2 in
-              let stat = (ty,t1,t2,o) in
-              let w = compute_equality_weight stat in
-              let proof = Equality.Exact term in 
-              let e = Equality.mk_equality (w, proof, stat, []) in
-              Some e, (newmeta+1)
-          | _ -> None, newmeta
-        in
-        match res with
-        | Some e ->
-            let tl, newmeta' = aux newmeta tl in
-              if newmeta' < newmeta then 
-                prerr_endline "big trouble";
-              (uri, e)::tl, newmeta' (* max???? *)
-        | None ->
-            aux newmeta tl
-  in
-  let found, maxm = aux maxmeta candidates in
-  let uriset, eqlist = 
-    let mceq = Equality.meta_convertibility_eq in
-    (List.fold_left
-       (fun (s, l) (u, e) ->
-          if List.exists (mceq e) (List.map snd l) then (
-            debug_print
-              (lazy
-                 (Printf.sprintf "NO!! %s already there!"
-                    (Equality.string_of_equality e)));
-            (UriManager.UriSet.add u s, l)
-          ) else (UriManager.UriSet.add u s, (u, e)::l))
-       (UriManager.UriSet.empty, []) found)
-  in
-  uriset, eqlist, maxm
-;;
-
-
-let find_library_theorems dbd env status equalities_uris =
-  let module C = Cic in
-  let module S = CicSubstitution in
-  let module T = CicTypeChecker in
-  let blacklist =
-    let refl_equal =
-      UriManager.uri_of_string "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)" in
-    let s =
-      UriManager.UriSet.remove refl_equal
-        (UriManager.UriSet.union equalities_uris equations_blacklist)
-    in
-    List.fold_left
-      (fun s u -> UriManager.UriSet.add u s)
-      s [eq_XURI () ;sym_eq_URI (); trans_eq_URI (); eq_ind_URI ();
-         eq_ind_r_URI ()]
-  in
-  let metasenv, context, ugraph = env in
-  let candidates =
-    List.fold_left
-      (fun l uri ->
-         if UriManager.UriSet.mem uri blacklist then l
-         else
-           let t = CicUtil.term_of_uri uri in
-           let ty, _ = CicTypeChecker.type_of_aux' metasenv context t ugraph in
-           (t, ty, [])::l)
-      [] (MetadataQuery.signature_of_goal ~dbd status)
-  in
-  let refl_equal =
-    let u = eq_XURI () in
-    let t = CicUtil.term_of_uri u in
-    let ty, _ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in
-    (t, ty, [])
-  in
-  refl_equal::candidates
-;;
-
-
-let find_context_hypotheses env equalities_indexes =
-  let metasenv, context, ugraph = env in
-  let _, res = 
-    List.fold_left
-      (fun (n, l) entry ->
-         match entry with
-         | None -> (n+1, l)
-         | Some _ ->
-             if List.mem n equalities_indexes then
-               (n+1, l)
-             else
-               let t = Cic.Rel n in
-               let ty, _ =
-                 CicTypeChecker.type_of_aux' metasenv context t ugraph in 
-               (n+1, (t, ty, [])::l))
-      (1, []) context
-  in
-  res
-;;
-
-let get_stats () = <:show<Inference.>> ;;
+let get_stats () = "" (*<:show<Inference.>>*) ;;