X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Findexing.ml;h=d71e7c5a793702bbdd2210f40b9f44ebe5146699;hb=a060ed37101ce0e97bc26af8d49ce2491471c60c;hp=e6a2463c099a8a084e4ac83e42497eac382e3653;hpb=b1ec882fae6023000ff6076e0a45f9809a6210e4;p=helm.git

diff --git a/helm/software/components/tactics/paramodulation/indexing.ml b/helm/software/components/tactics/paramodulation/indexing.ml
index e6a2463c0..d71e7c5a7 100644
--- a/helm/software/components/tactics/paramodulation/indexing.ml
+++ b/helm/software/components/tactics/paramodulation/indexing.ml
@@ -62,7 +62,7 @@ let string_of_res ?env =
     | Some (t, s, m, u, ((p,e), eq_URI)) ->
         Printf.sprintf "Some: (%s, %s, %s)" 
           (Utils.string_of_pos p)
-          (Inference.string_of_equality ?env e)
+          (Equality.string_of_equality ?env e)
           (CicPp.ppterm t)
 ;;
 
@@ -85,7 +85,7 @@ let print_candidates ?env mode term res =
        (List.map
           (fun (p, e) ->
              Printf.sprintf "| (%s, %s)" (Utils.string_of_pos p)
-               (Inference.string_of_equality ?env e))
+               (Equality.string_of_equality ?env e))
           res));
 ;;
 
@@ -93,7 +93,7 @@ let print_candidates ?env mode term res =
 let indexing_retrieval_time = ref 0.;;
 
 
-let apply_subst = Inference.apply_subst
+let apply_subst = Equality.apply_subst
 
 let index = Index.index
 let remove_index = Index.remove_index
@@ -103,7 +103,7 @@ let init_index = Index.init_index
 
 let check_disjoint_invariant subst metasenv msg =
   if (List.exists 
-        (fun (i,_,_) -> (List.exists (fun (j,_) -> i=j) subst)) metasenv)
+        (fun (i,_,_) -> (Equality.is_in_subst i subst)) metasenv)
   then 
     begin 
       prerr_endline ("not disjoint: " ^ msg);
@@ -124,19 +124,20 @@ let check_for_duplicates metas msg =
 let check_res res msg =
   match res with
       Some (t, subst, menv, ug, (eq_found, eq_URI)) ->
-        let eqs = Inference.string_of_equality (snd eq_found) in
+        let eqs = Equality.string_of_equality (snd eq_found) in
         check_disjoint_invariant subst menv msg;
         check_for_duplicates menv (msg ^ "\nchecking " ^ eqs);
     | None -> ()
 ;;
 
 let check_target context target msg =
-  let w, proof, (eq_ty, left, right, order), metas = target in
+  let w, proof, (eq_ty, left, right, order), metas,_ = 
+    Equality.open_equality target in
   (* check that metas does not contains duplicates *)
-  let eqs = Inference.string_of_equality target in
+  let eqs = Equality.string_of_equality target in
   let _ = check_for_duplicates metas (msg ^ "\nchecking " ^ eqs) in
-  let actual = (Inference.metas_of_term left)@(Inference.metas_of_term right)
-    @(Inference.metas_of_term eq_ty)@(Inference.metas_of_proof proof)  in
+  let actual = (Utils.metas_of_term left)@(Utils.metas_of_term right)
+    @(Utils.metas_of_term eq_ty)@(Equality.metas_of_proof proof)  in
   let menv = List.filter (fun (i, _, _) -> List.mem i actual) metas in
   let _ = if menv <> metas then 
     begin 
@@ -177,13 +178,6 @@ let check_target context target msg =
    the position will always be Left, and if the ordering is left < right,
    position will be Right.
 *)
-let local_max = ref 100;;
-
-let make_variant (p,eq) =
-  let maxmeta, eq = Inference.fix_metas !local_max eq in
-  local_max := maxmeta;
-  p, eq
-;;
 
 let get_candidates ?env mode tree term =
   let t1 = Unix.gettimeofday () in
@@ -245,17 +239,21 @@ let rec find_matches metasenv context ugraph lift_amount term termty =
   function
     | [] -> None
     | candidate::tl ->
-        let pos, (_, proof, (ty, left, right, o), metas) = candidate in
+        let pos, equality = candidate in
+	let (_, proof, (ty, left, right, o), metas,_) = 
+	  Equality.open_equality equality in
         if Utils.debug_metas then 
           ignore(check_target context (snd candidate) "find_matches");
         if Utils.debug_res then 
           begin
-            let c = "eq = " ^ (Inference.string_of_equality (snd candidate)) ^ "\n"in
-            let t = "t = " ^ (CicPp.ppterm term) ^ "\n" in
-            let m = "metas = " ^ (CicMetaSubst.ppmetasenv [] metas) ^ "\n" in
-            let p = "proof = " ^ (CicPp.ppterm (Inference.build_proof_term proof))  ^ "\n" in
+            let c="eq = "^(Equality.string_of_equality (snd candidate)) ^ "\n"in
+            let t="t = " ^ (CicPp.ppterm term) ^ "\n" in
+            let m="metas = " ^ (CicMetaSubst.ppmetasenv [] metas) ^ "\n" in
+            let p="proof = "^
+              (CicPp.ppterm(Equality.build_proof_term_old (snd proof)))^"\n" 
+            in
               check_for_duplicates metas "gia nella metas";
-              check_for_duplicates (metasenv @ metas) ("not disjoint" ^ c ^ t ^ m ^ p)
+              check_for_duplicates (metasenv@metas) ("not disjoint"^c^t^m^p)
           end;
         if check && not (fst (CicReduction.are_convertible
                                 ~metasenv context termty ty ugraph)) then (
@@ -332,7 +330,8 @@ let rec find_all_matches ?(unif_fun=Inference.unification)
   function
     | [] -> []
     | candidate::tl ->
-        let pos, (_, _, (ty, left, right, o), metas) = candidate in
+        let pos, equality = candidate in 
+	let (_,_,(ty,left,right,o),metas,_)=Equality.open_equality equality in
         let do_match c eq_URI =
           let subst', metasenv', ugraph' =
             let t1 = Unix.gettimeofday () in
@@ -407,25 +406,16 @@ let find_all_matches
 (*
   returns true if target is subsumed by some equality in table
 *)
-let subsumption env table target =
-  let _, _, (ty, left, right, _), tmetas = target in
+let subsumption env table target = 
+  (* 
+  let print_res l =
+    prerr_endline (String.concat "\n" (List.map (fun (_, subst, menv, ug,
+    ((pos,equation),_)) -> Inference.string_of_equality equation)l))
+  in
+  *)
+  let _, _, (ty, left, right, _), tmetas, _ = Equality.open_equality target in
   let metasenv, context, ugraph = env in
   let metasenv = tmetas in
-  let merge_if_possible s1 s2 =
-    let already_in = Hashtbl.create 13 in
-    let rec aux acc = function
-      | ((i,x) as s)::tl ->
-          (try 
-            let x' = Hashtbl.find already_in i in
-            if x = x' then aux acc tl else None
-          with
-          | Not_found -> 
-              Hashtbl.add already_in i x;
-              aux (s::acc) tl)
-      | [] -> Some acc 
-    in  
-      aux [] (s1@s2)
-  in
   let leftr =
     match left with
     | Cic.Meta _ -> []   
@@ -434,16 +424,18 @@ let subsumption env table target =
         find_all_matches ~unif_fun:Inference.matching
           metasenv context ugraph 0 left ty leftc
   in
+(*  print_res leftr;*)
   let rec ok what = function
-    | [] -> false, []
-    | (_, subst, menv, ug, ((pos, (_, _, (_, l, r, o), m)), _))::tl ->
+    | [] -> None
+    | (_, subst, menv, ug, ((pos,equation),_))::tl ->
+        let _, _, (_, l, r, o), m,_ = Equality.open_equality equation in
         try
           let other = if pos = Utils.Left then r else l in
           let subst', menv', ug' =
             let t1 = Unix.gettimeofday () in
             try
               let r = 
-                Inference.matching metasenv menv context what other ugraph
+                Inference.matching metasenv m context what other ugraph
               in
               let t2 = Unix.gettimeofday () in
               match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
@@ -453,17 +445,15 @@ let subsumption env table target =
               match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
               raise e
           in
-          (match merge_if_possible subst subst' with
+          (match Equality.merge_subst_if_possible subst subst' with
           | None -> ok what tl
-          | Some s -> true, s)
+          | Some s -> Some (s, equation))
         with Inference.MatchingFailure ->
           ok what tl
   in
-  let r, subst = ok right leftr in
-  let r, s =
-    if r then
-      true, subst
-    else
+  match ok right leftr with
+  | Some _ as res -> res
+  | None -> 
       let rightr =
         match right with
           | Cic.Meta _ -> [] 
@@ -472,14 +462,13 @@ let subsumption env table target =
                 find_all_matches ~unif_fun:Inference.matching
                   metasenv context ugraph 0 right ty rightc
       in
+(*        print_res rightr;*)
         ok left rightr
-  in
 (*     (if r then  *)
 (*        debug_print  *)
 (*          (lazy *)
 (*             (Printf.sprintf "SUBSUMPTION! %s\n%s\n" *)
 (*                (Inference.string_of_equality target) (Utils.print_subst s)))); *)
-    r, s
 ;;
 
 let rec demodulation_aux ?from ?(typecheck=false) 
@@ -494,11 +483,10 @@ let rec demodulation_aux ?from ?(typecheck=false)
   if List.exists (fun (i,_,_) -> i = 2840) metasenv
   then
     (prerr_endline ("term: " ^(CicPp.ppterm term));
-     List.iter (fun (_,x) -> prerr_endline (Inference.string_of_equality  x))
+     List.iter (fun (_,x) -> prerr_endline (Equality.string_of_equality  x))
        candidates;
      prerr_endline ("-------");
      prerr_endline ("+++++++"));
-(*   let candidates = List.map make_variant candidates in *)
   let res =
     match term with
       | C.Meta _ -> None
@@ -605,14 +593,16 @@ let rec demodulation_equality ?from newmeta env table sign target =
   let module HL = HelmLibraryObjects in
   let module U = Utils in
   let metasenv, context, ugraph = env in
-  let w, proof, (eq_ty, left, right, order), metas = target in
+  let w, ((proof_new, proof_old) as proof), 
+     (eq_ty, left, right, order), metas, id = 
+    Equality.open_equality target in
   (* first, we simplify *)
   let right = U.guarded_simpl context right in
   let left = U.guarded_simpl context left in
   let order = !Utils.compare_terms left right in
   let stat = (eq_ty, left, right, order) in 
   let w = Utils.compute_equality_weight stat in
-  let target = w, proof, stat, metas in
+  let target = Equality.mk_equality (w, proof, stat, metas) in
   if Utils.debug_metas then 
     ignore(check_target context target "demod equalities input");
   let metasenv' = (* metasenv @ *) metas in
@@ -625,18 +615,22 @@ let rec demodulation_equality ?from newmeta env table sign target =
       begin
         ignore(check_for_duplicates menv "input1");
         ignore(check_disjoint_invariant subst menv "input2");
-        let substs = Inference.ppsubst subst in 
+        let substs = Equality.ppsubst subst in 
         ignore(check_target context (snd eq_found) ("input3" ^ substs))
       end;
-    let pos, (_, proof', (ty, what, other, _), menv') = eq_found in
+    let pos, equality = eq_found in
+    let (_, (proof'_new,proof'_old), 
+        (ty, what, other, _), menv',id') = Equality.open_equality equality in
     let ty =
-    try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
+      try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
       with CicUtil.Meta_not_found _ -> ty
     in
     let what, other = if pos = Utils.Left then what, other else other, what in
     let newterm, newproof =
-      let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
-      let name = C.Name ("x_Demod" ^ (string_of_int !demod_counter)) in
+      let bo = 
+        Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
+(*      let name = C.Name ("x_Demod" ^ (string_of_int !demod_counter)) in*)
+      let name = C.Name "x" in
       incr demod_counter;
       let bo' =
         let l, r = if is_left then t, S.lift 1 right else S.lift 1 left, t in
@@ -645,46 +639,55 @@ let rec demodulation_equality ?from newmeta env table sign target =
       in
       if sign = Utils.Positive then
           (bo,
-           Inference.ProofBlock (
-             subst, eq_URI, (name, ty), bo'(* t' *), eq_found, proof))
+           (Equality.Step (subst,(Equality.Demodulation,id,(pos,id'),
+			 (*apply_subst subst*) (Cic.Lambda (name, ty, bo')))),
+           Equality.ProofBlock (
+             subst, eq_URI, (name, ty), bo'(* t' *), eq_found, proof_old)))
       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 (); *)
+(*        debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta)); *)
+(*        print_newline (); *)
           C.Meta (!maxmeta, irl)
         in
           let eq_found =
-            let proof' =
+            let proof'_old' =
               let termlist =
                 if pos = Utils.Left then [ty; what; other]
                 else [ty; other; what]
               in
-              Inference.ProofSymBlock (termlist, proof')
+              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, (0, proof', (ty, other, what, Utils.Incomparable),menv')
+            pos, 
+              Equality.mk_equality 
+                (0, (proof'_new',proof'_old'), 
+                (ty, other, what, Utils.Incomparable),menv')
           in
           let target_proof =
             let pb =
-              Inference.ProofBlock 
+              Equality.ProofBlock 
 		(subst, eq_URI, (name, ty), bo',
-                 eq_found, Inference.BasicProof ([],metaproof))
+                 eq_found, Equality.BasicProof (Equality.empty_subst,metaproof))
             in
-            match proof with
-            | Inference.BasicProof _ ->
+            assert false, (* not implemented *)
+            (match snd proof with
+            | Equality.BasicProof _ ->
                 (* print_endline "replacing a BasicProof"; *)
                 pb
-            | Inference.ProofGoalBlock (_, parent_proof) ->
+            | Equality.ProofGoalBlock (_, parent_proof) ->
   (* print_endline "replacing another ProofGoalBlock"; *)
-                Inference.ProofGoalBlock (pb, parent_proof)
-            | _ -> assert false
+                Equality.ProofGoalBlock (pb, parent_proof)
+            | _ -> assert false)
           in
         let refl =
           C.Appl [C.MutConstruct (* reflexivity *)
@@ -692,23 +695,30 @@ let rec demodulation_equality ?from newmeta env table sign target =
                   eq_ty; if is_left then right else left]          
         in
         (bo,
-         Inference.ProofGoalBlock (Inference.BasicProof ([],refl), target_proof))
-	end
+         (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 (Inference.build_proof_term newproof) ugraph);
+          newmenv context 
+            (Equality.build_proof_term_old (snd newproof)) ugraph);
           () 
         with exc ->                   
           prerr_endline "sempre lui";
-          prerr_endline (Inference.ppsubst subst);
-          prerr_endline (CicPp.ppterm (Inference.build_proof_term newproof));
+          prerr_endline (Equality.ppsubst subst);
+          prerr_endline (CicPp.ppterm 
+            (Equality.build_proof_term_old (snd newproof)));
           prerr_endline ("+++++++++++++termine: " ^ (CicPp.ppterm t));
           prerr_endline ("+++++++++++++what: " ^ (CicPp.ppterm what));
           prerr_endline ("+++++++++++++other: " ^ (CicPp.ppterm other));
-          prerr_endline ("+++++++++++++subst: " ^ (Inference.ppsubst subst));
+          prerr_endline ("+++++++++++++subst: " ^ (Equality.ppsubst subst));
+          prerr_endline ("+++++++++++++newmenv: " ^ (CicMetaSubst.ppmetasenv []
+            newmenv));
           raise exc;
       else () 
     in
@@ -719,7 +729,8 @@ let rec demodulation_equality ?from newmeta env table sign target =
     build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
     let res =
       let w = Utils.compute_equality_weight stat in
-      (w, newproof, stat,newmenv) in
+      Equality.mk_equality (w, newproof, stat,newmenv) 
+    in
     if Utils.debug_metas then 
       ignore(check_target context res "buildnew_target output");
     !maxmeta, res 
@@ -734,8 +745,8 @@ let rec demodulation_equality ?from newmeta env table sign target =
     match res with
     | Some t ->
         let newmeta, newtarget = build_newtarget true t in
-          if (Inference.is_weak_identity (metasenv', context, ugraph) newtarget) ||
-            (Inference.meta_convertibility_eq target newtarget) then
+          if (Equality.is_weak_identity newtarget) ||
+            (Equality.meta_convertibility_eq target newtarget) then
               newmeta, newtarget
           else 
             demodulation_equality newmeta env table sign newtarget
@@ -745,8 +756,8 @@ let rec demodulation_equality ?from newmeta env table sign target =
           match res with
           | Some t ->
               let newmeta, newtarget = build_newtarget false t in
-                if (Inference.is_weak_identity (metasenv', context, ugraph) newtarget) ||
-                  (Inference.meta_convertibility_eq target newtarget) then
+                if (Equality.is_weak_identity newtarget) ||
+                  (Equality.meta_convertibility_eq target newtarget) then
                     newmeta, newtarget
                 else
                    demodulation_equality newmeta env table sign newtarget
@@ -896,6 +907,9 @@ let sup_l_counter = ref 1;;
    returns a list of new clauses inferred with a left superposition step
    the negative equation "target" and one of the positive equations in "table"
 *)
+let superposition_left newmeta (metasenv, context, ugraph) table target = 
+  assert false
+(*
 let superposition_left newmeta (metasenv, context, ugraph) table target =
   let module C = Cic in
   let module S = CicSubstitution in
@@ -903,25 +917,23 @@ let superposition_left newmeta (metasenv, context, ugraph) table target =
   let module HL = HelmLibraryObjects in
   let module CR = CicReduction in
   let module U = Utils in
-  let weight, proof, (eq_ty, left, right, ordering), menv = target in
+  let weight, proof, (eq_ty, left, right, ordering), menv, id = 
+    Equality.open_equality target 
+  in
   if Utils.debug_metas then
     ignore(check_target context target "superpositionleft");
   let expansions, _ =
     let term = if ordering = U.Gt then left else right in
-      begin 
-        let t1 = Unix.gettimeofday () in
-        let res = betaexpand_term metasenv context ugraph table 0 term in
-        let t2 = Unix.gettimeofday () in
-          beta_expand_time := !beta_expand_time  +. (t2 -. t1);
-        res
-      end
+    betaexpand_term metasenv context ugraph table 0 term
   in
   let maxmeta = ref newmeta in
   let build_new (bo, s, m, ug, (eq_found, eq_URI)) =
 (*     debug_print (lazy "\nSUPERPOSITION LEFT\n"); *)
     let time1 = Unix.gettimeofday () in
     
-    let pos, (_, proof', (ty, what, other, _), menv') = eq_found in
+    let pos, equality = eq_found in
+    let _,proof',(ty,what,other,_),menv',id'=Equality.open_equality equality in
+    let proof'_new, proof'_old = proof' in
     let what, other = if pos = Utils.Left then what, other else other, what in
     let newgoal, newproof =
       let bo' =  U.guarded_simpl context (apply_subst s (S.subst other bo)) in
@@ -945,26 +957,30 @@ let superposition_left newmeta (metasenv, context, ugraph) table target =
             if pos = Utils.Left then [ty; what; other]
             else [ty; other; what]
           in
-          Inference.ProofSymBlock (termlist, proof')
+          proof'_new, (* MAH????? *)
+          Equality.ProofSymBlock (termlist, proof'_old)
         in
         let what, other =
           if pos = Utils.Left then what, other else other, what
         in
-        pos, (0, proof', (ty, other, what, Utils.Incomparable), menv')
+        pos, 
+          Equality.mk_equality 
+            (0, proof', (ty, other, what, Utils.Incomparable), menv')
       in
-      let target_proof =
+      let target_proof = assert false (*
         let pb =
-          Inference.ProofBlock (s, eq_URI, (name, ty), bo'', eq_found,
-                                Inference.BasicProof ([],metaproof))
+          Equality.ProofBlock 
+            (s, eq_URI, (name, ty), bo'', eq_found,
+            Equality.BasicProof (Equality.empty_subst,metaproof))
         in
         match proof with
-        | Inference.BasicProof _ ->
+        | Equality.BasicProof _ ->
 (*             debug_print (lazy "replacing a BasicProof"); *)
             pb
-        | Inference.ProofGoalBlock (_, parent_proof) ->
+        | Equality.ProofGoalBlock (_, parent_proof) ->
 (*             debug_print (lazy "replacing another ProofGoalBlock"); *)
-            Inference.ProofGoalBlock (pb, parent_proof)
-        | _ -> assert false
+            Equality.ProofGoalBlock (pb, parent_proof)
+        | _ -> assert false*)
       in
       let refl =
         C.Appl [C.MutConstruct (* reflexivity *)
@@ -972,7 +988,10 @@ let superposition_left newmeta (metasenv, context, ugraph) table target =
                 eq_ty; if ordering = U.Gt then right else left]
       in
       (bo',
-       Inference.ProofGoalBlock (Inference.BasicProof ([],refl), target_proof))
+       (Equality.Step (Equality.SuperpositionLeft,id,(pos,id'),
+         assert false), (* il predicato della beta expand non viene tenuto? *) 
+       Equality.ProofGoalBlock 
+        (Equality.BasicProof (Equality.empty_subst,refl), target_proof)))
     in
     let left, right =
       if ordering = U.Gt then newgoal, right else left, newgoal in
@@ -983,12 +1002,12 @@ let superposition_left newmeta (metasenv, context, ugraph) table target =
     build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
 
     let w = Utils.compute_equality_weight stat in
-    (w, newproof, stat, newmenv) 
+    Equality.mk_equality (w, newproof, stat, newmenv) 
 
   in
   !maxmeta, List.map build_new expansions
 ;;
-
+*)
 
 let sup_r_counter = ref 1;;
 
@@ -1006,7 +1025,9 @@ let superposition_right newmeta (metasenv, context, ugraph) table target =
   let module HL = HelmLibraryObjects in
   let module CR = CicReduction in
   let module U = Utils in 
-  let w, eqproof, (eq_ty, left, right, ordering), newmetas = target in 
+  let w, (eqproof1,eqproof2), (eq_ty, left, right, ordering), newmetas,id = 
+    Equality.open_equality target 
+  in 
   if Utils.debug_metas then 
     ignore (check_target context target "superpositionright");
   let metasenv' = newmetas in
@@ -1038,12 +1059,15 @@ let superposition_right newmeta (metasenv, context, ugraph) table target =
       ignore (check_target context (snd eq_found) "buildnew1" );
     let time1 = Unix.gettimeofday () in
     
-    let pos, (_, proof', (ty, what, other, _), menv') = eq_found in
+    let pos, equality =  eq_found in
+    let (_, proof', (ty, what, other, _), menv',id') = 
+      Equality.open_equality  equality in
     let what, other = if pos = Utils.Left then what, other else other, what in
     let newgoal, newproof =
       (* qua *)
       let bo' = Utils.guarded_simpl context (apply_subst s (S.subst other bo)) in
-      let name = C.Name ("x_SupR_" ^ (string_of_int !sup_r_counter)) in
+(*      let name = C.Name ("x_SupR_" ^ (string_of_int !sup_r_counter)) in*)
+      let name = C.Name "x" in
       incr sup_r_counter;
       let bo'' =
         let l, r =
@@ -1052,7 +1076,10 @@ let superposition_right newmeta (metasenv, context, ugraph) table target =
                 S.lift 1 eq_ty; l; r]
       in
       bo',
-      Inference.ProofBlock (s, eq_URI, (name, ty), bo'', eq_found, eqproof)
+      ( Equality.Step (s,(Equality.SuperpositionRight,
+		      id,(pos,id'),(*apply_subst s*) (Cic.Lambda(name,ty,bo'')))),
+	Equality.ProofBlock (s, eq_URI, (name, ty), bo'', eq_found, eqproof2))
+       
     in
     let newmeta, newequality = 
       let left, right =
@@ -1063,10 +1090,10 @@ let superposition_right newmeta (metasenv, context, ugraph) table target =
       let stat = (eq_ty, left, right, neworder) in
       let eq' =
         let w = Utils.compute_equality_weight stat in
-        (w, newproof, stat, newmenv) in
+        Equality.mk_equality (w, newproof, stat, newmenv) in
       if Utils.debug_metas then 
         ignore (check_target context eq' "buildnew3");
-      let newm, eq' = Inference.fix_metas !maxmeta eq' in
+      let newm, eq' = Equality.fix_metas !maxmeta eq' in
       if Utils.debug_metas then 
         ignore (check_target context eq' "buildnew4");
       newm, eq'
@@ -1080,7 +1107,7 @@ let superposition_right newmeta (metasenv, context, ugraph) table target =
   in
   let new1 = List.map (build_new U.Gt) res1
   and new2 = List.map (build_new U.Lt) res2 in
-  let ok e = not (Inference.is_identity (metasenv', context, ugraph) e) in
+  let ok e = not (Equality.is_identity (metasenv', context, ugraph) e) in
   (!maxmeta,
    (List.filter ok (new1 @ new2)))
 ;;
@@ -1094,68 +1121,78 @@ let rec demodulation_goal newmeta env table goal =
   let module HL = HelmLibraryObjects in
   let metasenv, context, ugraph = env in
   let maxmeta = ref newmeta in
-  let proof, metas, term = goal in
+  let (cicproof,proof), metas, term = goal in
   let term = Utils.guarded_simpl (~debug:true) context term in
-  let goal = proof, metas, term in
+  let goal = (cicproof,proof), metas, term in
   let metasenv' = metas in
   
   let build_newgoal (t, subst, menv, ug, (eq_found, eq_URI)) =
-    let pos, (_, proof', (ty, what, other, _), menv') = eq_found in
+    let pos, equality = eq_found in
+    let (_, (proofnew',proof'), (ty, what, other, _), menv',id) = 
+      Equality.open_equality equality in
     let what, other = if pos = Utils.Left then what, other else other, what in
     let ty =
       try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
       with CicUtil.Meta_not_found _ -> ty
     in
-    let newterm, newproof =
-      let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
+    let newterm, newproof, newcicproof =
+      let bo = 
+	Utils.guarded_simpl context (apply_subst subst(S.subst other t)) 
+      in
       let bo' = apply_subst subst t in 
-      let name = C.Name ("x_DemodGoal_" ^ (string_of_int !demod_counter)) in
+(*      let name = C.Name ("x_DemodGoal_" ^ (string_of_int !demod_counter)) in*)
+      let name = C.Name "x" in
       incr demod_counter;
       let metaproof = 
         incr maxmeta;
-        let irl =
-          CicMkImplicit.identity_relocation_list_for_metavariable context in
+        let irl = [] (*
+          CicMkImplicit.identity_relocation_list_for_metavariable context *) in 
 (*         debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta)); *)
         C.Meta (!maxmeta, irl)
       in
       let eq_found =
-        let proof' =
+        let eq_found_proof =
           let termlist =
             if pos = Utils.Left then [ty; what; other]
             else [ty; other; what]
           in
-          Inference.ProofSymBlock (termlist, proof')
+          Equality.ProofSymBlock (termlist, proof')
         in
         let what, other =
           if pos = Utils.Left then what, other else other, what
         in
-        pos, (0, proof', (ty, other, what, Utils.Incomparable), menv')
+        pos, 
+	Equality.mk_equality 
+	  (0,(proofnew',eq_found_proof), (ty, other, what, Utils.Incomparable), menv')
       in
       let goal_proof =
         let pb =
-          Inference.ProofBlock (subst, eq_URI, (name, ty), bo',
-                                eq_found, Inference.BasicProof ([],metaproof))
+          Equality.ProofBlock 
+	    (subst, eq_URI, (name, ty), bo',
+             eq_found, Equality.BasicProof (Equality.empty_subst,metaproof))
         in
         let rec repl = function
-          | Inference.NoProof ->
+          | Equality.NoProof ->
 (*               debug_print (lazy "replacing a NoProof"); *)
               pb
-          | Inference.BasicProof _ ->
+          | Equality.BasicProof _ ->
 (*               debug_print (lazy "replacing a BasicProof"); *)
               pb
-          | Inference.ProofGoalBlock (_, parent_proof) ->
+          | Equality.ProofGoalBlock (_, parent_proof) ->
 (*               debug_print (lazy "replacing another ProofGoalBlock"); *)
-              Inference.ProofGoalBlock (pb, parent_proof)
-          | Inference.SubProof (term, meta_index, p)  ->
+              Equality.ProofGoalBlock (pb, parent_proof)
+          | Equality.SubProof (term, meta_index, p)  ->
               prerr_endline "subproof!";
-              Inference.SubProof (term, meta_index, repl p)
+              Equality.SubProof (term, meta_index, repl p)
           | _ -> assert false
         in repl proof
       in
-      bo, Inference.ProofGoalBlock (Inference.NoProof, goal_proof)
+      let newcicproofstep = (pos,id,subst,Cic.Lambda (name,ty,bo')) in
+      bo, Equality.ProofGoalBlock (Equality.NoProof, goal_proof),
+        (newcicproofstep::cicproof)
     in
     let newmetasenv = (* Inference.filter subst *) menv in
-    !maxmeta, (newproof, newmetasenv, newterm)
+    !maxmeta, ((newcicproof,newproof), newmetasenv, newterm)
   in  
   let res =
     demodulation_aux (* ~typecheck:true *) metasenv' context ugraph table 0 term
@@ -1164,12 +1201,12 @@ let rec demodulation_goal newmeta env table goal =
   | Some t ->
       let newmeta, newgoal = build_newgoal t in
       let _, _, newg = newgoal in
-      if Inference.meta_convertibility term newg then
-        newmeta, newgoal
+      if Equality.meta_convertibility term newg then
+        true, newmeta, newgoal
       else
         demodulation_goal newmeta env table newgoal
   | None ->
-      newmeta, goal
+      false, newmeta, goal
 ;;
 
 (** demodulation, when the target is a theorem *)
@@ -1184,18 +1221,20 @@ let rec demodulation_theorem newmeta env table theorem =
   let metasenv' = metas in
   
   let build_newtheorem (t, subst, menv, ug, (eq_found, eq_URI)) =
-    let pos, (_, proof', (ty, what, other, _), menv') = eq_found in
+    let pos, equality = eq_found in
+    let (_, proof', (ty, what, other, _), menv',id) = 
+      Equality.open_equality equality in
     let what, other = if pos = Utils.Left then what, other else other, what in
     let newterm, newty =
       let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
       let bo' = apply_subst subst t in 
       let name = C.Name ("x_DemodThm_" ^ (string_of_int !demod_counter)) in
       incr demod_counter;
-      let newproof =
-        Inference.ProofBlock (subst, eq_URI, (name, ty), bo', eq_found,
-                              Inference.BasicProof ([],term))
+      let newproofold =
+        Equality.ProofBlock (subst, eq_URI, (name, ty), bo', eq_found,
+                              Equality.BasicProof (Equality.empty_subst,term))
       in
-      (Inference.build_proof_term newproof, bo)
+      (Equality.build_proof_term_old newproofold, bo)
     in    
     !maxmeta, (newterm, newty, menv)
   in  
@@ -1206,7 +1245,7 @@ let rec demodulation_theorem newmeta env table theorem =
   | Some t ->
       let newmeta, newthm = build_newtheorem t in
       let newt, newty, _ = newthm in
-      if Inference.meta_convertibility termty newty then
+      if Equality.meta_convertibility termty newty then
         newmeta, newthm
       else
         demodulation_theorem newmeta env table newthm