X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fparamodulation%2Findexing.ml;h=c964e3a78c882f525df690c230ec60e18abd1eb4;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=0e5914b11320de8a39d79ad5957ab09ecdee1ed5;hpb=43c2a5068c1ff5f838e0558bb60c21e316cab852;p=helm.git

diff --git a/helm/ocaml/paramodulation/indexing.ml b/helm/ocaml/paramodulation/indexing.ml
index 0e5914b11..c964e3a78 100644
--- a/helm/ocaml/paramodulation/indexing.ml
+++ b/helm/ocaml/paramodulation/indexing.ml
@@ -51,53 +51,14 @@ let print_candidates mode term res =
 let indexing_retrieval_time = ref 0.;;
 
 
-(* let my_apply_subst subst term = *)
-(*   let module C = Cic in *)
-(*   let lookup lift_amount meta = *)
-(*     match meta with *)
-(*     | C.Meta (i, _) -> ( *)
-(*         try *)
-(*           let _, (_, t, _) = List.find (fun (m, _) -> m = i) subst in *)
-(*           (\* CicSubstitution.lift lift_amount  *\)t *)
-(*         with Not_found -> meta *)
-(*       ) *)
-(*     | _ -> assert false *)
-(*   in *)
-(*   let rec apply_aux lift_amount =  function *)
-(*     | C.Meta (i, l) as t -> lookup lift_amount t *)
-(*     | C.Appl l -> C.Appl (List.map (apply_aux lift_amount) l) *)
-(*     | C.Prod (nn, s, t) -> *)
-(*         C.Prod (nn, apply_aux lift_amount s, apply_aux (lift_amount+1) t) *)
-(*     | C.Lambda (nn, s, t) -> *)
-(*         C.Lambda (nn, apply_aux lift_amount s, apply_aux (lift_amount+1) t) *)
-(*     | t -> t *)
-(*   in *)
-(*   apply_aux 0 term *)
-(* ;; *)
-
-
-(* let apply_subst subst term = *)
-(*   Printf.printf "| apply_subst:\n| subst: %s\n| term: %s\n" *)
-(*     (Utils.print_subst ~prefix:" ; " subst) (CicPp.ppterm term); *)
-(*   let res = my_apply_subst subst term in *)
-(* (\*   let res = CicMetaSubst.apply_subst subst term in *\) *)
-(*   Printf.printf "| res: %s\n" (CicPp.ppterm res); *)
-(*   print_endline "|"; *)
-(*   res *)
-(* ;; *)
-
-(* let apply_subst = my_apply_subst *)
 let apply_subst = CicMetaSubst.apply_subst
 
 
-(* let apply_subst = *)
-(*   let profile = CicUtil.profile "apply_subst" in *)
-(*   (fun s a -> profile (apply_subst s) a) *)
-(* ;; *)
-
 
 (*
 (* NO INDEXING *)
+let init_index () = ()
+  
 let empty_table () = []
 
 let index table equality =
@@ -122,6 +83,8 @@ let get_candidates mode table term = table
 
 (*
 (* PATH INDEXING *)
+let init_index () = ()
+
 let empty_table () =
   Path_indexing.PSTrie.empty
 ;;
@@ -181,16 +144,16 @@ let get_candidates mode tree term =
 ;;
 
 
-(* let get_candidates = *)
-(*   let profile = CicUtil.profile "Indexing.get_candidates" in *)
-(*   (fun mode tree term -> profile.profile (get_candidates mode tree) term) *)
-(* ;; *)
-
-
 let match_unif_time_ok = ref 0.;;
 let match_unif_time_no = ref 0.;;
 
 
+(*
+  finds the first equality in the index that matches "term", of type "termty"
+  termty can be Implicit if it is not needed. The result (one of the sides of
+  the equality, actually) should be not greater (wrt the term ordering) than
+  term
+*)
 let rec find_matches metasenv context ugraph lift_amount term termty =
   let module C = Cic in
   let module U = Utils in
@@ -198,10 +161,6 @@ let rec find_matches metasenv context ugraph lift_amount term termty =
   let module M = CicMetaSubst in
   let module HL = HelmLibraryObjects in
   let cmp = !Utils.compare_terms in
-(*   let names = Utils.names_of_context context in *)
-(*   let termty, ugraph = *)
-(*     CicTypeChecker.type_of_aux' metasenv context term ugraph *)
-(*   in *)
   let check = match termty with C.Implicit None -> false | _ -> true in
   function
     | [] -> None
@@ -209,12 +168,9 @@ let rec find_matches metasenv context ugraph lift_amount term termty =
         let pos, (_, proof, (ty, left, right, o), metas, args) = candidate in
         if check && not (fst (CicReduction.are_convertible
                                 ~metasenv context termty ty ugraph)) then (
-(*           debug_print (lazy ( *)
-(*             Printf.sprintf "CANDIDATE HAS WRONG TYPE: %s required, %s found" *)
-(*               (CicPp.pp termty names) (CicPp.pp ty names))); *)
           find_matches metasenv context ugraph lift_amount term termty tl
         ) else
-          let do_match c (* other *) eq_URI =
+          let do_match c eq_URI =
             let subst', metasenv', ugraph' =
               let t1 = Unix.gettimeofday () in
               try
@@ -238,29 +194,20 @@ let rec find_matches metasenv context ugraph lift_amount term termty =
           in
           if o <> U.Incomparable then
             try
-              do_match c (* other *) eq_URI
+              do_match c eq_URI
             with Inference.MatchingFailure ->
               find_matches metasenv context ugraph lift_amount term termty tl
           else
             let res =
-              try do_match c (* other *) eq_URI
+              try do_match c eq_URI
               with Inference.MatchingFailure -> None
             in
             match res with
             | Some (_, s, _, _, _) ->
-                let c' = (* M. *)apply_subst s c
-                and other' = (* M. *)apply_subst s other in
+                let c' = apply_subst s c
+                and other' = apply_subst s other in
                 let order = cmp c' other' in
                 let names = U.names_of_context context in
-(*                 let _ = *)
-(*                   debug_print *)
-(*                     (Printf.sprintf "OK matching: %s and %s, order: %s" *)
-(*                        (CicPp.ppterm c') *)
-(*                        (CicPp.ppterm other') *)
-(*                        (Utils.string_of_comparison order)); *)
-(*                   debug_print *)
-(*                     (Printf.sprintf "subst:\n%s\n" (Utils.print_subst s)) *)
-(*                 in *)
                 if order = U.Gt then
                   res
                 else
@@ -271,6 +218,10 @@ let rec find_matches metasenv context ugraph lift_amount term termty =
 ;;
 
 
+(*
+  as above, but finds all the matching equalities, and the matching condition
+  can be either Inference.matching or Inference.unification
+*)
 let rec find_all_matches ?(unif_fun=Inference.unification)
     metasenv context ugraph lift_amount term termty =
   let module C = Cic in
@@ -279,89 +230,75 @@ let rec find_all_matches ?(unif_fun=Inference.unification)
   let module M = CicMetaSubst in
   let module HL = HelmLibraryObjects in
   let cmp = !Utils.compare_terms in
-(*   let names = Utils.names_of_context context in *)
-(*   let termty, ugraph = *)
-(*     CicTypeChecker.type_of_aux' metasenv context term ugraph *)
-(*   in *)
-(*   let _ = *)
-(*     match term with *)
-(*     | C.Meta _ -> assert false *)
-(*     | _ -> () *)
-(*   in *)
   function
     | [] -> []
     | candidate::tl ->
         let pos, (_, _, (ty, left, right, o), metas, args) = candidate in
-(*         if not (fst (CicReduction.are_convertible *)
-(*                        ~metasenv context termty ty ugraph)) then ( *)
-(* (\*           debug_print (lazy ( *\) *)
-(* (\*             Printf.sprintf "CANDIDATE HAS WRONG TYPE: %s required, %s found" *\) *)
-(* (\*               (CicPp.pp termty names) (CicPp.pp ty names))); *\) *)
-(*           find_all_matches ~unif_fun metasenv context ugraph *)
-(*             lift_amount term termty tl *)
-(*         ) else *)
-          let do_match c (* other *) eq_URI =
-            let subst', metasenv', ugraph' =
-              let t1 = Unix.gettimeofday () in
-              try
-                let r = 
-                  unif_fun (metasenv @ metas) context
-                    term (S.lift lift_amount c) ugraph in
-                let t2 = Unix.gettimeofday () in
-                match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
-                r
-              with
-              | Inference.MatchingFailure
-              | CicUnification.UnificationFailure _
-              | CicUnification.Uncertain _ as e ->
-                let t2 = Unix.gettimeofday () in
-                match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
-                raise e
-            in
-            (C.Rel (1 + lift_amount), subst', metasenv', ugraph',
-             (candidate, eq_URI))
-          in
-          let c, other, eq_URI =
-            if pos = Utils.Left then left, right, Utils.eq_ind_URI ()
-            else right, left, Utils.eq_ind_r_URI ()
-          in
-          if o <> U.Incomparable then
+        let do_match c eq_URI =
+          let subst', metasenv', ugraph' =
+            let t1 = Unix.gettimeofday () in
             try
-              let res = do_match c (* other *) eq_URI in
-              res::(find_all_matches ~unif_fun metasenv context ugraph
-                      lift_amount term termty tl)
+              let r = 
+                unif_fun (metasenv @ metas) context
+                  term (S.lift lift_amount c) ugraph in
+              let t2 = Unix.gettimeofday () in
+              match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
+              r
             with
             | Inference.MatchingFailure
             | CicUnification.UnificationFailure _
-            | CicUnification.Uncertain _ ->
+            | CicUnification.Uncertain _ as e ->
+                let t2 = Unix.gettimeofday () in
+                match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
+                raise e
+          in
+          (C.Rel (1 + lift_amount), subst', metasenv', ugraph',
+           (candidate, eq_URI))
+        in
+        let c, other, eq_URI =
+          if pos = Utils.Left then left, right, Utils.eq_ind_URI ()
+          else right, left, Utils.eq_ind_r_URI ()
+        in
+        if o <> U.Incomparable then
+          try
+            let res = do_match c eq_URI in
+            res::(find_all_matches ~unif_fun metasenv context ugraph
+                    lift_amount term termty tl)
+          with
+          | Inference.MatchingFailure
+          | CicUnification.UnificationFailure _
+          | CicUnification.Uncertain _ ->
+              find_all_matches ~unif_fun metasenv context ugraph
+                lift_amount term termty tl
+        else
+          try
+            let res = do_match c eq_URI in
+            match res with
+            | _, s, _, _, _ ->
+                let c' = apply_subst s c
+                and other' = apply_subst s other in
+                let order = cmp c' other' in
+                let names = U.names_of_context context in
+                if order <> U.Lt && order <> U.Le then
+                  res::(find_all_matches ~unif_fun metasenv context ugraph
+                          lift_amount term termty tl)
+                else
+                  find_all_matches ~unif_fun metasenv context ugraph
+                    lift_amount term termty tl
+          with
+          | Inference.MatchingFailure
+          | CicUnification.UnificationFailure _
+          | CicUnification.Uncertain _ ->
               find_all_matches ~unif_fun metasenv context ugraph
                 lift_amount term termty tl
-          else
-            try
-              let res = do_match c (* other *) eq_URI in
-              match res with
-              | _, s, _, _, _ ->
-                  let c' = (* M. *)apply_subst s c
-                  and other' = (* M. *)apply_subst s other in
-                  let order = cmp c' other' in
-                  let names = U.names_of_context context in
-                  if order <> U.Lt && order <> U.Le then
-                    res::(find_all_matches ~unif_fun metasenv context ugraph
-                            lift_amount term termty tl)
-                  else
-                    find_all_matches ~unif_fun metasenv context ugraph
-                      lift_amount term termty tl
-            with
-            | Inference.MatchingFailure
-            | CicUnification.UnificationFailure _
-            | CicUnification.Uncertain _ ->
-                find_all_matches ~unif_fun metasenv context ugraph
-                  lift_amount term termty tl
 ;;
 
 
+(*
+  returns true if target is subsumed by some equality in table
+*)
 let subsumption env table target =
-  let _, (ty, left, right, _), tmetas, _ = target in
+  let _, _, (ty, left, right, _), tmetas, _ = target in
   let metasenv, context, ugraph = env in
   let metasenv = metasenv @ tmetas in
   let samesubst subst subst' =
@@ -387,14 +324,15 @@ let subsumption env table target =
   in
   let rec ok what = function
     | [] -> false, []
-    | (_, subst, menv, ug, ((pos, (_, _, (_, l, r, o), _, _)), _))::tl ->
+    | (_, subst, menv, ug, ((pos, (_, _, (_, l, r, o), m, _)), _))::tl ->
         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 context what other ugraph in
+                Inference.matching (metasenv @ menv @ m) context what other ugraph
+	      in
               let t2 = Unix.gettimeofday () in
               match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
               r
@@ -411,18 +349,26 @@ let subsumption env table target =
           ok what tl
   in
   let r, subst = ok right leftr in
-  if r then
-    true, subst
-  else
-    let rightr =
-      match right with
-      | Cic.Meta _ -> []
-      | _ ->
-          let rightc = get_candidates Matching table right in
-          find_all_matches ~unif_fun:Inference.matching
-            metasenv context ugraph 0 right ty rightc
-    in
-    ok left rightr
+  let r, s =
+    if r then
+      true, subst
+    else
+      let rightr =
+	match right with
+	  | Cic.Meta _ -> []
+	  | _ ->
+              let rightc = get_candidates Matching table right in
+		find_all_matches ~unif_fun:Inference.matching
+		  metasenv context ugraph 0 right ty rightc
+      in
+	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
 ;;
 
 
@@ -520,6 +466,7 @@ let build_newtarget_time = ref 0.;;
 
 let demod_counter = ref 1;;
 
+(** demodulation, when target is an equality *)
 let rec demodulation_equality newmeta env table sign target =
   let module C = Cic in
   let module S = CicSubstitution in
@@ -541,14 +488,7 @@ let rec demodulation_equality newmeta env table sign target =
     in
     let what, other = if pos = Utils.Left then what, other else other, what in
     let newterm, newproof =
-      let bo = (* M. *)apply_subst subst (S.subst other t) in
-(*       let t' = *)
-(*         let name = C.Name ("x_Demod_" ^ (string_of_int !demod_counter)) in *)
-(*         incr demod_counter; *)
-(*         let l, r = *)
-(*           if is_left then t, S.lift 1 right else S.lift 1 left, t in *)
-(*         (name, ty, S.lift 1 eq_ty, l, r) *)
-(*       in *)
+      let bo = apply_subst subst (S.subst other t) in
       let name = C.Name ("x_Demod_" ^ (string_of_int !demod_counter)) in
       incr demod_counter;
       let bo' =
@@ -565,18 +505,12 @@ let rec demodulation_equality newmeta env table sign target =
           incr maxmeta;
           let irl =
             CicMkImplicit.identity_relocation_list_for_metavariable context in
-          Printf.printf "\nADDING META: %d\n" !maxmeta;
+          debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta));
           print_newline ();
           C.Meta (!maxmeta, irl)
         in
-(*         let target' = *)
           let eq_found =
             let proof' =
-(*               let ens = *)
-(*                 if pos = Utils.Left then *)
-(*                   build_ens_for_sym_eq ty what other *)
-(*                 else *)
-(*                   build_ens_for_sym_eq ty other what *)
               let termlist =
                 if pos = Utils.Left then [ty; what; other]
                 else [ty; other; what]
@@ -591,45 +525,30 @@ let rec demodulation_equality newmeta env table sign target =
           in
           let target_proof =
             let pb =
-              Inference.ProofBlock (subst, eq_URI, (name, ty), bo'(* t' *),
+              Inference.ProofBlock (subst, eq_URI, (name, ty), bo',
                                     eq_found, Inference.BasicProof metaproof)
             in
             match proof with
             | Inference.BasicProof _ ->
                 print_endline "replacing a BasicProof";
                 pb
-            | Inference.ProofGoalBlock (_, parent_proof(* parent_eq *)) ->
+            | Inference.ProofGoalBlock (_, parent_proof) ->
                 print_endline "replacing another ProofGoalBlock";
-                Inference.ProofGoalBlock (pb, parent_proof(* parent_eq *))
+                Inference.ProofGoalBlock (pb, parent_proof)
             | _ -> assert false
           in
-(*           (0, target_proof, (eq_ty, left, right, order), metas, args) *)
-(*         in *)
         let refl =
           C.Appl [C.MutConstruct (* reflexivity *)
                     (LibraryObjects.eq_URI (), 0, 1, []);
                   eq_ty; if is_left then right else left]          
         in
         (bo,
-         Inference.ProofGoalBlock (Inference.BasicProof refl, target_proof(* target' *)))
+         Inference.ProofGoalBlock (Inference.BasicProof refl, target_proof))
     in
     let left, right = if is_left then newterm, right else left, newterm in
     let m = (Inference.metas_of_term left) @ (Inference.metas_of_term right) in
     let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) metas
     and newargs = args
-(*       let a =  *)
-(*         List.filter *)
-(*           (function C.Meta (i, _) -> List.mem i m | _ -> assert false) args in *)
-(*       let delta = (List.length args) - (List.length a) in *)
-(*       if delta > 0 then *)
-(*         let first = List.hd a in *)
-(*         let rec aux l = function *)
-(*           | 0 -> l *)
-(*           | d -> let l = aux l (d-1) in l @ [first] *)
-(*         in *)
-(*         aux a delta *)
-(*       else *)
-(*         a *)
     in
     let ordering = !Utils.compare_terms left right in
 
@@ -643,35 +562,55 @@ let rec demodulation_equality newmeta env table sign target =
     !maxmeta, res
   in
   let res = demodulation_aux metasenv' context ugraph table 0 left in
-  match res with
-  | Some t ->
-      let newmeta, newtarget = build_newtarget true t in
-      if (Inference.is_identity (metasenv', context, ugraph) newtarget) ||
-        (Inference.meta_convertibility_eq target newtarget) then
-          newmeta, newtarget
-      else
-(*         if subsumption env table newtarget then *)
-(*           newmeta, build_identity newtarget *)
-(*         else *)
-        demodulation_equality newmeta env table sign newtarget
-  | None ->
-      let res = demodulation_aux metasenv' context ugraph table 0 right in
-      match res with
-      | Some t ->
-          let newmeta, newtarget = build_newtarget false t in
-          if (Inference.is_identity (metasenv', context, ugraph) newtarget) ||
+  let newmeta, newtarget = 
+    match res with
+    | Some t ->
+	let newmeta, newtarget = build_newtarget true t in
+	  if (Inference.is_identity (metasenv', context, ugraph) newtarget) ||
             (Inference.meta_convertibility_eq target newtarget) then
-              newmeta, newtarget
-          else
-(*             if subsumption env table newtarget then *)
-(*               newmeta, build_identity newtarget *)
-(*             else *)
-              demodulation_equality newmeta env table sign newtarget
-      | None ->
-          newmeta, target
+	      newmeta, newtarget
+	  else
+            demodulation_equality newmeta env table sign newtarget
+    | None ->
+	let res = demodulation_aux metasenv' context ugraph table 0 right in
+	  match res with
+	  | Some t ->
+	      let newmeta, newtarget = build_newtarget false t in
+		if (Inference.is_identity (metasenv', context, ugraph) newtarget) ||
+		  (Inference.meta_convertibility_eq target newtarget) then
+		    newmeta, newtarget
+		else
+		  demodulation_equality newmeta env table sign newtarget
+	  | None ->
+	      newmeta, target
+  in
+  (* newmeta, newtarget *)
+  (* tentiamo di ridurre usando CicReduction.normalize *)
+  let w, p, (ty, left, right, o), m, a = newtarget in
+  let left' = ProofEngineReduction.simpl context left in
+  let right' = ProofEngineReduction.simpl context right in
+  let newleft =
+    if !Utils.compare_terms left' left = Utils.Lt then left' else left in
+  let newright = 
+    if !Utils.compare_terms right' right = Utils.Lt then right' else right in
+  if newleft != left || newright != right then (
+    debug_print
+      (lazy
+	 (Printf.sprintf "left: %s, left': %s\nright: %s, right': %s\n"
+	    (CicPp.ppterm left) (CicPp.ppterm left') (CicPp.ppterm right)
+	    (CicPp.ppterm right')))
+  );
+  let w' = Utils.compute_equality_weight ty newleft newright in
+  let o' = !Utils.compare_terms newleft newright in
+  newmeta, (w', p, (ty, newleft, newright, o'), m, a)
 ;;
 
 
+(**
+   Performs the beta expansion of the term "term" w.r.t. "table",
+   i.e. returns the list of all the terms t s.t. "(t term) = t2", for some t2
+   in table.
+*)
 let rec betaexpand_term metasenv context ugraph table lift_amount term =
   let module C = Cic in
   let module S = CicSubstitution in
@@ -794,6 +733,11 @@ let rec betaexpand_term metasenv context ugraph table lift_amount term =
 
 let sup_l_counter = ref 1;;
 
+(**
+   superposition_left 
+   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 =
   let module C = Cic in
   let module S = CicSubstitution in
@@ -809,21 +753,14 @@ let superposition_left newmeta (metasenv, context, ugraph) table target =
   let maxmeta = ref newmeta in
   let build_new (bo, s, m, ug, (eq_found, eq_URI)) =
 
-    print_endline "\nSUPERPOSITION LEFT\n";
-    
+    debug_print (lazy "\nSUPERPOSITION LEFT\n");
+
     let time1 = Unix.gettimeofday () in
     
     let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
     let what, other = if pos = Utils.Left then what, other else other, what in
     let newgoal, newproof =
-      let bo' = (* M. *)apply_subst s (S.subst other bo) in
-(*       let t' = *)
-(*         let name = C.Name ("x_SupL_" ^ (string_of_int !sup_l_counter)) in *)
-(*         incr sup_l_counter; *)
-(*         let l, r = *)
-(*           if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in *)
-(*         (name, ty, S.lift 1 eq_ty, l, r) *)
-(*       in *)
+      let bo' = apply_subst s (S.subst other bo) in
       let name = C.Name ("x_SupL_" ^ (string_of_int !sup_l_counter)) in
       incr sup_l_counter;
       let bo'' = 
@@ -838,49 +775,40 @@ let superposition_left newmeta (metasenv, context, ugraph) table target =
           CicMkImplicit.identity_relocation_list_for_metavariable context in
         C.Meta (!maxmeta, irl)
       in
-(*       let target' = *)
-        let eq_found =
-          let proof' =
-(*             let ens = *)
-(*               if pos = Utils.Left then *)
-(*                 build_ens_for_sym_eq ty what other *)
-(*               else *)
-(*                 build_ens_for_sym_eq ty other what *)
-(*             in *)
-            let termlist =
-              if pos = Utils.Left then [ty; what; other]
-              else [ty; other; what]
-            in
-            Inference.ProofSymBlock (termlist, proof')
-          in
-          let what, other =
-            if pos = Utils.Left then what, other else other, what
+      let eq_found =
+        let proof' =
+          let termlist =
+            if pos = Utils.Left then [ty; what; other]
+            else [ty; other; what]
           in
-          pos, (0, proof', (ty, other, what, Utils.Incomparable), menv', args')
+          Inference.ProofSymBlock (termlist, proof')
         in
-        let target_proof =
-          let pb =
-            Inference.ProofBlock (s, eq_URI, (name, ty), bo''(* t' *), eq_found,
-                                  Inference.BasicProof metaproof)
-          in
-          match proof with
-          | Inference.BasicProof _ ->
-              print_endline "replacing a BasicProof";
-              pb
-          | Inference.ProofGoalBlock (_, parent_proof(* parent_eq *)) ->
-              print_endline "replacing another ProofGoalBlock";
-              Inference.ProofGoalBlock (pb, parent_proof(* parent_eq *))
-          | _ -> assert false
+        let what, other =
+          if pos = Utils.Left then what, other else other, what
+        in
+        pos, (0, proof', (ty, other, what, Utils.Incomparable), menv', args')
+      in
+      let target_proof =
+        let pb =
+          Inference.ProofBlock (s, eq_URI, (name, ty), bo'', eq_found,
+                                Inference.BasicProof metaproof)
         in
-(*         (weight, target_proof, (eq_ty, left, right, ordering), [], []) *)
-(*       in *)
+        match proof with
+        | Inference.BasicProof _ ->
+            debug_print (lazy "replacing a BasicProof");
+            pb
+        | Inference.ProofGoalBlock (_, parent_proof) ->
+            debug_print (lazy "replacing another ProofGoalBlock");
+            Inference.ProofGoalBlock (pb, parent_proof)
+        | _ -> assert false
+      in
       let refl =
         C.Appl [C.MutConstruct (* reflexivity *)
                   (LibraryObjects.eq_URI (), 0, 1, []);
                 eq_ty; if ordering = U.Gt then right else left]
       in
       (bo',
-       Inference.ProofGoalBlock (Inference.BasicProof refl, target_proof(* target' *)))
+       Inference.ProofGoalBlock (Inference.BasicProof refl, target_proof))
     in
     let left, right =
       if ordering = U.Gt then newgoal, right else left, newgoal in
@@ -901,6 +829,13 @@ let superposition_left newmeta (metasenv, context, ugraph) table target =
 
 let sup_r_counter = ref 1;;
 
+(**
+   superposition_right
+   returns a list of new clauses inferred with a right superposition step
+   between the positive equation "target" and one in the "table" "newmeta" is
+   the first free meta index, i.e. the first number above the highest meta
+   index: its updated value is also returned
+*)
 let superposition_right newmeta (metasenv, context, ugraph) table target =
   let module C = Cic in
   let module S = CicSubstitution in
@@ -919,7 +854,7 @@ let superposition_right newmeta (metasenv, context, ugraph) table target =
         let res l r =
           List.filter
             (fun (_, subst, _, _, _) ->
-               let subst = (* M. *)apply_subst subst in
+               let subst = apply_subst subst in
                let o = !Utils.compare_terms (subst l) (subst r) in
                o <> U.Lt && o <> U.Le)
             (fst (betaexpand_term metasenv' context ugraph table 0 l))
@@ -933,7 +868,7 @@ let superposition_right newmeta (metasenv, context, ugraph) table target =
     let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
     let what, other = if pos = Utils.Left then what, other else other, what in
     let newgoal, newproof =
-      let bo' = (* M. *)apply_subst s (S.subst other bo) in
+      let bo' = apply_subst s (S.subst other bo) in
       let t' =
         let name = C.Name ("x_SupR_" ^ (string_of_int !sup_r_counter)) in
         incr sup_r_counter;
@@ -950,34 +885,15 @@ 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''(* t' *), eq_found, eqproof)
+      Inference.ProofBlock (s, eq_URI, (name, ty), bo'', eq_found, eqproof)
     in
     let newmeta, newequality = 
       let left, right =
-        if ordering = U.Gt then newgoal, (* M. *)apply_subst s right
-        else (* M. *)apply_subst s left, newgoal in
+        if ordering = U.Gt then newgoal, apply_subst s right
+        else apply_subst s left, newgoal in
       let neworder = !Utils.compare_terms left right 
       and newmenv = newmetas @ menv'
       and newargs = args @ args' in
-(*         let m = *)
-(*           (Inference.metas_of_term left) @ (Inference.metas_of_term right) in *)
-(*         let a =  *)
-(*           List.filter *)
-(*             (function C.Meta (i, _) -> List.mem i m | _ -> assert false) *)
-(*             (args @ args') *)
-(*         in *)
-(*         let delta = (List.length args) - (List.length a) in *)
-(*         if delta > 0 then *)
-(*           let first = List.hd a in *)
-(*           let rec aux l = function *)
-(*             | 0 -> l *)
-(*             | d -> let l = aux l (d-1) in l @ [first] *)
-(*           in *)
-(*           aux a delta *)
-(*         else *)
-(*           a *)
-(*       in *)
       let eq' =
         let w = Utils.compute_equality_weight eq_ty left right in
         (w, newproof, (eq_ty, left, right, neworder), newmenv, newargs)
@@ -994,16 +910,13 @@ 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 = function *)
-(*     | _, _, (_, left, right, _), _, _ -> *)
-(*         not (fst (CR.are_convertible context left right ugraph)) *)
-(*   in *)
   let ok e = not (Inference.is_identity (metasenv, context, ugraph) e) in
   (!maxmeta,
    (List.filter ok (new1 @ new2)))
 ;;
 
 
+(** demodulation, when the target is a goal *)
 let rec demodulation_goal newmeta env table goal =
   let module C = Cic in
   let module S = CicSubstitution in
@@ -1022,7 +935,7 @@ let rec demodulation_goal newmeta env table goal =
       with CicUtil.Meta_not_found _ -> ty
     in
     let newterm, newproof =
-      let bo = (* M. *)apply_subst subst (S.subst other t) in
+      let bo = 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
       incr demod_counter;
@@ -1030,16 +943,11 @@ let rec demodulation_goal newmeta env table goal =
         incr maxmeta;
         let irl =
           CicMkImplicit.identity_relocation_list_for_metavariable context in
-        Printf.printf "\nADDING META: %d\n" !maxmeta;
-        print_newline ();
+        debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta));
         C.Meta (!maxmeta, irl)
       in
       let eq_found =
         let proof' =
-(*           let ens = *)
-(*             if pos = Utils.Left then build_ens_for_sym_eq ty what other *)
-(*             else build_ens_for_sym_eq ty other what *)
-(*           in *)
           let termlist =
             if pos = Utils.Left then [ty; what; other]
             else [ty; other; what]
@@ -1097,6 +1005,7 @@ let rec demodulation_goal newmeta env table goal =
 ;;
 
 
+(** demodulation, when the target is a theorem *)
 let rec demodulation_theorem newmeta env table theorem =
   let module C = Cic in
   let module S = CicSubstitution in