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=1c3daffecf3fc1daff35973004d6d645e58fde74;hpb=b9d067ff0d66913b7ade9fadc79064dedb4aa86f;p=helm.git

diff --git a/helm/software/components/tactics/paramodulation/inference.ml b/helm/software/components/tactics/paramodulation/inference.ml
index 1c3daffec..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)
@@ -196,301 +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 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 (LibraryObjects.is_eq_URI 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 LibraryObjects.is_eq_URI 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 tty_of_u u = 
-  let _ = <:start<tty_of_u>> in
-  let t = CicUtil.term_of_uri u in
-  let ty, _ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in
-  let _ = <:stop<tty_of_u>> in
-  t, ty
-;;
-
-let utty_of_u u =
-  let t,ty = tty_of_u u in
-  u, t, ty
-;;
-
-let find_library_equalities dbd context status maxmeta = 
-  let module C = Cic in
-  let module S = CicSubstitution in
-  let module T = CicTypeChecker in
-  let _ = <:start<equations_for_goal>> in
-  let eqs = (MetadataQuery.equations_for_goal ~dbd status) in
-  let _ = <:stop<equations_for_goal>> in
-  let candidates =
-    List.fold_left
-      (fun l uri ->
-        if LibraryObjects.is_eq_refl_URI uri ||
-           LibraryObjects.is_sym_eq_URI uri ||
-           LibraryObjects.is_trans_eq_URI uri ||
-           LibraryObjects.is_eq_ind_URI uri ||
-           LibraryObjects.is_eq_ind_r_URI uri 
-         then 
-           l
-         else
-           (utty_of_u uri)::l)
-      [] eqs
-  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 (LibraryObjects.is_eq_URI uri ||
-                              LibraryObjects.is_eq_refl_URI 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 
-                (LibraryObjects.is_eq_URI uri || 
-                 LibraryObjects.is_eq_refl_URI 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 candidates =
-    List.fold_left
-      (fun l uri ->
-        if LibraryObjects.is_sym_eq_URI uri ||
-           LibraryObjects.is_trans_eq_URI uri ||
-           LibraryObjects.is_eq_ind_URI uri ||
-           LibraryObjects.is_eq_ind_r_URI uri 
-         then l
-         else
-           (let t,ty = tty_of_u uri in t, ty, [] )::l)
-      [] (MetadataQuery.signature_of_goal ~dbd status)
-  in
-  let refl_equal =
-    let eq = 
-      match LibraryObjects.eq_URI () with
-      | Some u -> u
-      | None -> 
-          raise 
-            (ProofEngineTypes.Fail 
-              (lazy "No default eq defined when running find_library_theorems"))
-    in
-    let t = CicUtil.term_of_uri (LibraryObjects.eq_refl_URI ~eq) in
-    let ty, _ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in
-    (t, ty, [])
-  in
-  let res = refl_equal::candidates in
-  res
-;;
-
-
-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.>>*) ;;