Initial work on setoids:

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

diff --git a/helm/software/components/tactics/paramodulation/indexing.ml b/helm/software/components/tactics/paramodulation/indexing.ml
index 7b545dd47c5b72a1cec282bc92f40c25b57c60b7..f3af1b482e8afb2eece8d1ce79d3e10af7812ec7 100644 (file)
--- a/helm/software/components/tactics/paramodulation/indexing.ml
+++ b/helm/software/components/tactics/paramodulation/indexing.ml
@@ -23,7 +23,7 @@
  * http://cs.unibo.it/helm/.
  *)
 
-let _profiler = <:profiler<_profiler>>;;
+(* let _profiler = <:profiler<_profiler>>;; *)
 
 (* $Id$ *)
 
@@ -180,15 +180,9 @@ let get_candidates ?env mode tree term =
   let s = 
     match mode with
     | Matching -> 
-        let _ = <:start<retrieve_generalizations>> in
-        <:stop<retrieve_generalizations
         Index.retrieve_generalizations tree term
-        >>
     | Unification -> 
-        let _ = <:start<retrieve_unifiables>> in
-        <:stop<retrieve_unifiables
         Index.retrieve_unifiables tree term
-        >>
         
   in
   Index.PosEqSet.elements s
@@ -534,7 +528,7 @@ let rec demodulation_aux ?from ?(typecheck=false)
 exception Foo
 
 (** demodulation, when target is an equality *)
-let rec demodulation_equality ?from eq_uri newmeta env table sign target =
+let rec demodulation_equality ?from eq_uri newmeta env table target =
   let module C = Cic in
   let module S = CicSubstitution in
   let module M = CicMetaSubst in
@@ -582,90 +576,10 @@ let rec demodulation_equality ?from eq_uri newmeta env table sign target =
         let l, r = if is_left then t, S.lift 1 right else S.lift 1 left, t in
           C.Appl [C.MutInd (eq_uri, 0, []); S.lift 1 eq_ty; l; r]
       in
-      if sign = Utils.Positive then
           (bo, (Equality.Step (subst,(Equality.Demodulation, id,(pos,id'),
           (Cic.Lambda (name, ty, bo'))))))
-      else
-        assert false
-(*
-        begin
-        prerr_endline "***************************************negative";
-        let metaproof = 
-          incr maxmeta;
-          let irl =
-            CicMkImplicit.identity_relocation_list_for_metavariable context in
-(*        debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta)); *)
-(*        print_newline (); *)
-          C.Meta (!maxmeta, irl)
-        in
-          let eq_found =
-            let proof'_old' =
-              let termlist =
-                if pos = Utils.Left then [ty; what; other]
-                else [ty; other; what]
-              in
-              Equality.ProofSymBlock (termlist, proof'_old)
-            in
-            let proof'_new' = assert false (* not implemented *) in
-            let what, other =
-              if pos = Utils.Left then what, other else other, what
-            in
-            pos, 
-              Equality.mk_equality 
-                (0, (proof'_new',proof'_old'), 
-                (ty, other, what, Utils.Incomparable),menv')
-          in
-          let target_proof =
-            let pb =
-              Equality.ProofBlock 
-                (subst, eq_URI, (name, ty), bo',
-                 eq_found, Equality.BasicProof (Equality.empty_subst,metaproof))
-            in
-            assert false, (* not implemented *)
-            (match snd proof with
-            | Equality.BasicProof _ ->
-                (* print_endline "replacing a BasicProof"; *)
-                pb
-            | Equality.ProofGoalBlock (_, parent_proof) ->
-  (* print_endline "replacing another ProofGoalBlock"; *)
-                Equality.ProofGoalBlock (pb, parent_proof)
-            | _ -> assert false)
-          in
-        let refl =
-          C.Appl [C.MutConstruct (* reflexivity *)
-                    (LibraryObjects.eq_URI (), 0, 1, []);
-                  eq_ty; if is_left then right else left]          
-        in
-        (bo,
-         (assert false, (* not implemented *)
-         Equality.ProofGoalBlock 
-           (Equality.BasicProof (Equality.empty_subst,refl), snd target_proof)))
-      end
-*)
     in
-    let newmenv = (* Inference.filter subst *) menv in
-(*
-    let _ = 
-      if Utils.debug_metas then 
-        try ignore(CicTypeChecker.type_of_aux'
-          newmenv context 
-            (Equality.build_proof_term newproof) ugraph);
-          () 
-        with exc ->                   
-          prerr_endline "sempre lui";
-          prerr_endline (Subst.ppsubst subst);
-          prerr_endline (CicPp.ppterm 
-            (Equality.build_proof_term newproof));
-          prerr_endline ("+++++++++++++termine: " ^ (CicPp.ppterm t));
-          prerr_endline ("+++++++++++++what: " ^ (CicPp.ppterm what));
-          prerr_endline ("+++++++++++++other: " ^ (CicPp.ppterm other));
-          prerr_endline ("+++++++++++++subst: " ^ (Subst.ppsubst subst));
-          prerr_endline ("+++++++++++++newmenv: " ^ (CicMetaSubst.ppmetasenv []
-            newmenv));
-          raise exc;
-      else () 
-    in
-*)
+    let newmenv = menv in
     let left, right = if is_left then newterm, right else left, newterm in
     let ordering = !Utils.compare_terms left right in
     let stat = (eq_ty, left, right, ordering) in
@@ -689,7 +603,7 @@ let rec demodulation_equality ?from eq_uri newmeta env table sign target =
             (Equality.meta_convertibility_eq target newtarget) then
               newmeta, newtarget
           else 
-            demodulation_equality ?from eq_uri newmeta env table sign newtarget
+            demodulation_equality ?from eq_uri newmeta env table newtarget
     | None ->
         let res = demodulation_aux metasenv' context ugraph table 0 right in
         if Utils.debug_res then check_res res "demod result 1"; 
@@ -700,7 +614,7 @@ let rec demodulation_equality ?from eq_uri newmeta env table sign target =
                   (Equality.meta_convertibility_eq target newtarget) then
                     newmeta, newtarget
                 else
-                   demodulation_equality ?from eq_uri newmeta env table sign newtarget
+                   demodulation_equality ?from eq_uri newmeta env table newtarget
           | None ->
               newmeta, target
   in
@@ -1119,4 +1033,4 @@ let rec demodulation_goal env table goal =
   | None -> do_right ()
 ;;
 
-let get_stats () = <:show<Indexing.>> ;;
+let get_stats () = "" ;;