X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fparamodulation%2Findexing.ml;h=2d9076ad5fd1e389d5d94f5fce3230d9b972d862;hb=803959f90ae806a62746efe7f557ecd4b70c16ee;hp=85ee885cb969755c55bb551b85ea88d6e6a09550;hpb=439cb54c906ae03dc5f88e907ce2577fe5d6fcf7;p=helm.git

diff --git a/helm/ocaml/paramodulation/indexing.ml b/helm/ocaml/paramodulation/indexing.ml
index 85ee885cb..2d9076ad5 100644
--- a/helm/ocaml/paramodulation/indexing.ml
+++ b/helm/ocaml/paramodulation/indexing.ml
@@ -23,12 +23,18 @@
  * http://cs.unibo.it/helm/.
  *)
 
+(* $Id$ *)
+
+module Index = Equality_indexing.DT (* discrimination tree based indexing *)
+(*
+module Index = Equality_indexing.DT (* path tree based indexing *)
+*)
+
 let debug_print = Utils.debug_print;;
 
 
 type retrieval_mode = Matching | Unification;;
 
-
 let print_candidates mode term res =
   let _ =
     match mode with
@@ -51,128 +57,38 @@ 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 empty_table () = []
-
-let index table equality =
-  let _, _, (_, l, r, ordering), _, _ = equality in
-  match ordering with
-  | Utils.Gt -> (Utils.Left, equality)::table
-  | Utils.Lt -> (Utils.Right, equality)::table
-  | _ -> (Utils.Left, equality)::(Utils.Right, equality)::table
-;;
-
-let remove_index table equality =
-  List.filter (fun (p, e) -> e != equality) table
-;;
-
-let in_index table equality =
-  List.exists (fun (p, e) -> e == equality) table
-;;
-
-let get_candidates mode table term = table
-*)
-
-
-(*
-(* PATH INDEXING *)
-let empty_table () =
-  Path_indexing.PSTrie.empty
-;;
-
-let index = Path_indexing.index
-and remove_index = Path_indexing.remove_index
-and in_index = Path_indexing.in_index;;
-  
-let get_candidates mode trie term =
-  let t1 = Unix.gettimeofday () in
-  let res = 
-    let s = 
-      match mode with
-      | Matching -> Path_indexing.retrieve_generalizations trie term
-      | Unification -> Path_indexing.retrieve_unifiables trie term
-(*       Path_indexing.retrieve_all trie term *)
-    in
-    Path_indexing.PosEqSet.elements s
-  in
-(*   print_candidates mode term res; *)
-  let t2 = Unix.gettimeofday () in
-  indexing_retrieval_time := !indexing_retrieval_time +. (t2 -. t1);
-  res
-;;
+let index = Index.index
+let remove_index = Index.remove_index
+let in_index = Index.in_index
+let empty = Index.empty 
+let init_index = Index.init_index
+
+(* returns a list of all the equalities in the tree that are in relation
+   "mode" with the given term, where mode can be either Matching or
+   Unification.
+
+   Format of the return value: list of tuples in the form:
+   (position - Left or Right - of the term that matched the given one in this
+     equality,
+    equality found)
+   
+   Note that if equality is "left = right", if the ordering is left > right,
+   the position will always be Left, and if the ordering is left < right,
+   position will be Right.
 *)
-
-
-(* DISCRIMINATION TREES *)
-let init_index () =
-  Hashtbl.clear Discrimination_tree.arities;
-;;
-
-let empty_table () =
-  Discrimination_tree.DiscriminationTree.empty
-;;
-
-let index = Discrimination_tree.index
-and remove_index = Discrimination_tree.remove_index
-and in_index = Discrimination_tree.in_index;;
-
 let get_candidates mode tree term =
   let t1 = Unix.gettimeofday () in
   let res =
     let s = 
       match mode with
-      | Matching -> Discrimination_tree.retrieve_generalizations tree term
-      | Unification -> Discrimination_tree.retrieve_unifiables tree term
+      | Matching -> Index.retrieve_generalizations tree term
+      | Unification -> Index.retrieve_unifiables tree term
     in
-    Discrimination_tree.PosEqSet.elements s
+    Index.PosEqSet.elements s
   in
-(*   print_candidates mode term res; *)
+  (*   print_candidates mode term res; *)
 (*   print_endline (Discrimination_tree.string_of_discrimination_tree tree); *)
 (*   print_newline (); *)
   let t2 = Unix.gettimeofday () in
@@ -181,16 +97,32 @@ 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
+
+  Format of the return value:
+
+  (term to substitute, [Cic.Rel 1 properly lifted - see the various
+                        build_newtarget functions inside the various
+                        demodulation_* functions]
+   substitution used for the matching,
+   metasenv,
+   ugraph, [substitution, metasenv and ugraph have the same meaning as those
+   returned by CicUnification.fo_unif]
+   (equality where the matching term was found, [i.e. the equality to use as
+                                                rewrite rule]
+    uri [either eq_ind_URI or eq_ind_r_URI, depending on the direction of
+         the equality: this is used to build the proof term, again see one of
+         the build_newtarget functions]
+   ))
+*)
 let rec find_matches metasenv context ugraph lift_amount term termty =
   let module C = Cic in
   let module U = Utils in
@@ -198,10 +130,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 +137,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 +163,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 in
+                let other' = U.guarded_simpl context (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 +187,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 +199,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 +293,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 +318,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,11 +435,13 @@ 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
   let module M = CicMetaSubst in
   let module HL = HelmLibraryObjects in
+  let module U = Utils in
   let metasenv, context, ugraph = env in
   let _, proof, (eq_ty, left, right, order), metas, args = target in
   let metasenv' = metasenv @ metas in
@@ -541,14 +458,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 = U.guarded_simpl context (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 +475,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;
-          print_newline ();
+(*           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 +495,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 +532,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 +703,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 +723,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' =  U.guarded_simpl context (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 +745,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 +799,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 +824,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 +838,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 +855,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,26 +880,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 _ =
-    let env = metasenv, context, ugraph in
-    debug_print
-      (lazy
-         (Printf.sprintf "end of superposition_right:\n%s\n"
-            (String.concat "\n"
-               ((List.map
-                   (fun e -> "Positive " ^
-                      (Inference.string_of_equality ~env e)) (new1 @ new2))))))
-  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
@@ -1032,7 +905,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;
@@ -1040,16 +913,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]
@@ -1068,19 +936,19 @@ let rec demodulation_goal newmeta env table goal =
         in
         let rec repl = function
           | Inference.NoProof ->
-              debug_print (lazy "replacing a NoProof");
+(*               debug_print (lazy "replacing a NoProof"); *)
               pb
           | Inference.BasicProof _ ->
-              debug_print (lazy "replacing a BasicProof");
+(*               debug_print (lazy "replacing a BasicProof"); *)
               pb
           | Inference.ProofGoalBlock (_, parent_proof) ->
-              debug_print (lazy "replacing another ProofGoalBlock");
+(*               debug_print (lazy "replacing another ProofGoalBlock"); *)
               Inference.ProofGoalBlock (pb, parent_proof)
           | (Inference.SubProof (term, meta_index, p) as subproof) ->
-              debug_print
-                (lazy
-                   (Printf.sprintf "replacing %s"
-                      (Inference.string_of_proof subproof)));
+(*               debug_print *)
+(*                 (lazy *)
+(*                    (Printf.sprintf "replacing %s" *)
+(*                       (Inference.string_of_proof subproof))); *)
               Inference.SubProof (term, meta_index, repl p)
           | _ -> assert false
         in repl proof
@@ -1107,6 +975,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