From: Alberto Griggio <griggio@fbk.eu>
Date: Thu, 19 May 2005 13:11:06 +0000 (+0000)
Subject: various optimizations (to paramodulation and passive clause selection)
X-Git-Tag: single_binding~34
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=975da98810a335a759a3b5e5f96b1beb96c932d2;p=helm.git

various optimizations (to paramodulation and passive clause selection)
---

diff --git a/helm/ocaml/paramodulation/inference.ml b/helm/ocaml/paramodulation/inference.ml
index 987c17cc8..999666bca 100644
--- a/helm/ocaml/paramodulation/inference.ml
+++ b/helm/ocaml/paramodulation/inference.ml
@@ -1,26 +1,87 @@
 open Utils;;
 
 
+let string_of_equality ?env =
+  match env with
+  | None -> (
+      function
+        | _, (ty, left, right), _, _ ->
+            Printf.sprintf "{%s}: %s = %s" (CicPp.ppterm ty)
+              (CicPp.ppterm left) (CicPp.ppterm right)
+    )
+  | Some (_, context, _) -> (
+      let names = names_of_context context in
+      function
+        | _, (ty, left, right), _, _ ->
+            Printf.sprintf "{%s}: %s = %s" (CicPp.pp ty names)
+              (CicPp.pp left names) (CicPp.pp right names)
+    )
+;;
+
+
+let rec metas_of_term = function
+  | Cic.Meta (i, c) -> [i]
+  | Cic.Var (_, ens) 
+  | Cic.Const (_, ens) 
+  | Cic.MutInd (_, _, ens) 
+  | Cic.MutConstruct (_, _, _, ens) ->
+      List.flatten (List.map (fun (u, t) -> metas_of_term t) ens)
+  | Cic.Cast (s, t)
+  | Cic.Prod (_, s, t)
+  | Cic.Lambda (_, s, t)
+  | Cic.LetIn (_, s, t) -> (metas_of_term s) @ (metas_of_term t)
+  | Cic.Appl l -> List.flatten (List.map metas_of_term l)
+  | Cic.MutCase (uri, i, s, t, l) ->
+      (metas_of_term s) @ (metas_of_term t) @
+        (List.flatten (List.map metas_of_term l))
+  | Cic.Fix (i, il) ->
+      List.flatten
+        (List.map (fun (s, i, t1, t2) ->
+                     (metas_of_term t1) @ (metas_of_term t2)) il)
+  | Cic.CoFix (i, il) ->
+      List.flatten
+        (List.map (fun (s, t1, t2) ->
+                     (metas_of_term t1) @ (metas_of_term t2)) il)
+  | _ -> []
+;;      
+
+
 exception NotMetaConvertible;;
 
 let meta_convertibility_aux table t1 t2 =
   let module C = Cic in
-  let rec aux table t1 t2 =
+  let print_table t =
+    String.concat ", "
+      (List.map
+         (fun (k, v) -> Printf.sprintf "(%d, %d)" k v) t)
+  in
+  let rec aux ((table_l, table_r) as table) t1 t2 =
+(*     Printf.printf "aux %s, %s\ntable_l: %s, table_r: %s\n" *)
+(*       (CicPp.ppterm t1) (CicPp.ppterm t2) *)
+(*       (print_table table_l) (print_table table_r); *)
     match t1, t2 with
-    | t1, t2 when t1 = t2 -> table
     | C.Meta (m1, tl1), C.Meta (m2, tl2) ->
-        let m1_binding, m2_binding, table =
-          let m1b, table = 
-            try List.assoc m1 table, table
-            with Not_found -> m2, (m1, m2)::table
-          in
-          let m2b, table = 
-            try List.assoc m2 table, table
-            with Not_found -> m1, (m2, m1)::table
-          in
-          m1b, m2b, table
+        let m1_binding, table_l =
+          try List.assoc m1 table_l, table_l
+          with Not_found -> m2, (m1, m2)::table_l
+        and m2_binding, table_r =
+          try List.assoc m2 table_r, table_r
+          with Not_found -> m1, (m2, m1)::table_r
         in
-        if m1_binding <> m2 || m2_binding <> m1 then
+(*         let m1_binding, m2_binding, table = *)
+(*           let m1b, table =  *)
+(*             try List.assoc m1 table, table *)
+(*             with Not_found -> m2, (m1, m2)::table *)
+(*           in *)
+(*           let m2b, table =  *)
+(*             try List.assoc m2 table, table *)
+(*             with Not_found -> m1, (m2, m1)::table *)
+(*           in *)
+(*           m1b, m2b, table *)
+(*         in *)
+(*         Printf.printf "table_l: %s\ntable_r: %s\n\n" *)
+(*           (print_table table_l) (print_table table_r); *)
+        if (m1_binding <> m2) || (m2_binding <> m1) then
           raise NotMetaConvertible
         else (
           try
@@ -30,7 +91,7 @@ let meta_convertibility_aux table t1 t2 =
                  | None, Some _ | Some _, None -> raise NotMetaConvertible
                  | None, None -> res
                  | Some t1, Some t2 -> (aux res t1 t2))
-              table tl1 tl2
+              (table_l, table_r) tl1 tl2
           with Invalid_argument _ ->
             raise NotMetaConvertible
         )
@@ -77,6 +138,7 @@ let meta_convertibility_aux table t1 t2 =
             table il1 il2
         with Invalid_argument _ -> raise NotMetaConvertible
       )
+    | t1, t2 when t1 = t2 -> table
     | _, _ -> raise NotMetaConvertible
         
   and aux_ens table ens1 ens2 =
@@ -102,28 +164,19 @@ let meta_convertibility_eq eq1 eq2 =
   and _, (ty', left', right'), _, _ = eq2 in
   if ty <> ty' then
     false
+  else if (left = left') && (right = right') then
+    true
+  else if (left = right') && (right = left') then
+    true
   else
-    let print_table t w =
-      Printf.printf "table %s is:\n" w;
-      List.iter
-        (fun (k, v) -> Printf.printf "?%d: ?%d\n" k v)
-        t;
-      print_newline ();
-    in
     try
-      let table = meta_convertibility_aux [] left left' in
+      let table = meta_convertibility_aux ([], []) left left' in
       let _ = meta_convertibility_aux table right right' in
-(*       Printf.printf "meta_convertibility_eq, ok:\n%s\n%s\n" *)
-(*         (string_of_equality eq1) (string_of_equality eq2); *)
-(*       print_newline (); *)
       true
     with NotMetaConvertible ->
       try
-        let table = meta_convertibility_aux [] left right' in
+        let table = meta_convertibility_aux ([], []) left right' in
         let _ = meta_convertibility_aux table right left' in
-(*         Printf.printf "meta_convertibility_eq, ok:\n%s\n%s\n" *)
-(*           (string_of_equality eq1) (string_of_equality eq2); *)
-(*         print_newline (); *)
         true
       with NotMetaConvertible ->
         false
@@ -131,18 +184,122 @@ let meta_convertibility_eq eq1 eq2 =
 
 
 let meta_convertibility t1 t2 =
-  try
-    let _ = meta_convertibility_aux [] t1 t2 in
+  let f t =
+    String.concat ", "
+      (List.map
+         (fun (k, v) -> Printf.sprintf "(%d, %d)" k v) t)
+  in
+  if t1 = t2 then
     true
-  with NotMetaConvertible ->
-    false
+  else
+    try
+      let l, r = meta_convertibility_aux ([], []) t1 t2 in
+      (*     Printf.printf "meta_convertibility:\n%s\n%s\n\n" (f l) (f r); *)
+      true
+    with NotMetaConvertible ->
+      false
 ;;
 
 
+let replace_metas (* context *) term =
+  let module C = Cic in
+  let rec aux = function
+    | C.Meta (i, c) ->
+(*         let irl = *)
+(*           CicMkImplicit.identity_relocation_list_for_metavariable context *)
+(*         in *)
+(*         if c = irl then *)
+(*           C.Implicit (Some (`MetaIndex i)) *)
+(*         else ( *)
+(*           Printf.printf "WARNING: c non e` un identity_relocation_list!\n%s\n" *)
+(*             (String.concat "\n" *)
+(*                (List.map *)
+(*                   (function None -> "" | Some t -> CicPp.ppterm t) c)); *)
+(*           C.Meta (i, c) *)
+(*         ) *)
+        C.Implicit (Some (`MetaInfo (i, c)))
+    | C.Var (u, ens) -> C.Var (u, aux_ens ens)
+    | C.Const (u, ens) -> C.Const (u, aux_ens ens)
+    | C.Cast (s, t) -> C.Cast (aux s, aux t)
+    | C.Prod (name, s, t) -> C.Prod (name, aux s, aux t)
+    | C.Lambda (name, s, t) -> C.Lambda (name, aux s, aux t)
+    | C.LetIn (name, s, t) -> C.LetIn (name, aux s, aux t)
+    | C.Appl l -> C.Appl (List.map aux l)
+    | C.MutInd (uri, i, ens) -> C.MutInd (uri, i, aux_ens ens)
+    | C.MutConstruct (uri, i, j, ens) -> C.MutConstruct (uri, i, j, aux_ens ens)
+    | C.MutCase (uri, i, s, t, l) ->
+        C.MutCase (uri, i, aux s, aux t, List.map aux l)
+    | C.Fix (i, il) ->
+        let il' =
+          List.map (fun (s, i, t1, t2) -> (s, i, aux t1, aux t2)) il in
+        C.Fix (i, il')
+    | C.CoFix (i, il) ->
+        let il' =
+          List.map (fun (s, t1, t2) -> (s, aux t1, aux t2)) il in
+        C.CoFix (i, il')
+    | t -> t
+  and aux_ens ens =
+    List.map (fun (u, t) -> (u, aux t)) ens
+  in
+  aux term
+;;
+
+
+let restore_metas (* context *) term =
+  let module C = Cic in
+  let rec aux = function
+    | C.Implicit (Some (`MetaInfo (i, c))) ->
+(*         let c = *)
+(*           CicMkImplicit.identity_relocation_list_for_metavariable context *)
+(*         in *)
+(*         C.Meta (i, c) *)
+(*         let local_context:(C.term option) list = *)
+(*           Marshal.from_string mc 0 *)
+(*         in *)
+(*         C.Meta (i, local_context) *)
+        C.Meta (i, c)
+    | C.Var (u, ens) -> C.Var (u, aux_ens ens)
+    | C.Const (u, ens) -> C.Const (u, aux_ens ens)
+    | C.Cast (s, t) -> C.Cast (aux s, aux t)
+    | C.Prod (name, s, t) -> C.Prod (name, aux s, aux t)
+    | C.Lambda (name, s, t) -> C.Lambda (name, aux s, aux t)
+    | C.LetIn (name, s, t) -> C.LetIn (name, aux s, aux t)
+    | C.Appl l -> C.Appl (List.map aux l)
+    | C.MutInd (uri, i, ens) -> C.MutInd (uri, i, aux_ens ens)
+    | C.MutConstruct (uri, i, j, ens) -> C.MutConstruct (uri, i, j, aux_ens ens)
+    | C.MutCase (uri, i, s, t, l) ->
+        C.MutCase (uri, i, aux s, aux t, List.map aux l)
+    | C.Fix (i, il) ->
+        let il' =
+          List.map (fun (s, i, t1, t2) -> (s, i, aux t1, aux t2)) il in
+        C.Fix (i, il')
+    | C.CoFix (i, il) ->
+        let il' =
+          List.map (fun (s, t1, t2) -> (s, aux t1, aux t2)) il in
+        C.CoFix (i, il')
+    | t -> t
+  and aux_ens ens =
+    List.map (fun (u, t) -> (u, aux t)) ens
+  in
+  aux term
+;;
+
+
+let rec restore_subst (* context *) subst =
+  List.map
+    (fun (i, (c, t, ty)) ->
+       i, (c, restore_metas (* context *) t, ty))
+    subst
+;;
+
+      
 let beta_expand ?(metas_ok=true) ?(match_only=false)
     what type_of_what where context metasenv ugraph = 
   let module S = CicSubstitution in
   let module C = Cic in
+
+  let print_info = false in
+  
 (*   let _ = *)
 (*     let names = names_of_context context in *)
 (*     Printf.printf "beta_expand:\nwhat: %s, %s\nwhere: %s, %s\n" *)
@@ -394,6 +551,10 @@ let beta_expand ?(metas_ok=true) ?(match_only=false)
       | C.Meta _ when (not metas_ok) ->
           res, lifted_term
       | _ ->
+(*           let term' = *)
+(*             if match_only then replace_metas context term *)
+(*             else term *)
+(*           in *)
           try
             let subst', metasenv', ugraph' =
 (*               Printf.printf "provo a unificare %s e %s\n" *)
@@ -409,19 +570,42 @@ let beta_expand ?(metas_ok=true) ?(match_only=false)
             if match_only then
               let t' = CicMetaSubst.apply_subst subst' term in
               if not (meta_convertibility term t') then (
-                let names = names_of_context context in
-(*                 Printf.printf "\nbeta_expand: term e t' sono diversi!:\n%s\n%s\n\n" *)
-(*                   (CicPp.pp term names) (CicPp.pp t' names); *)
+(*                 if print_info then ( *)
+(*                   let names = names_of_context context in *)
+(*                   Printf.printf *)
+(*                     "\nbeta_expand: term e t' sono diversi!:\n%s\n%s\n\n" *)
+(*                     (CicPp.pp term names) (CicPp.pp t' names) *)
+(*                 ); *)
                 res, lifted_term
-              )
-              else
+              ) else (
+                let metas = metas_of_term term in
+(*                 let ok = ref false in *)
+                let fix_subst = function
+                  | (i, (c, C.Meta (j, lc), ty)) when List.mem i metas ->
+(*                       Printf.printf "fix_subst: scambio ?%d e ?%d\n" i j; *)
+(*                       ok := true; *)
+                      (j, (c, C.Meta (i, lc), ty))
+                  | s -> s
+                in
+                let subst' = List.map fix_subst subst' in
+(*                 if !ok then ( *)
+(*                   Printf.printf "aaa:\nterm: %s\nt'%s\n term subst': %s\n" *)
+(*                     (CicPp.ppterm term) *)
+(*                     (CicPp.ppterm t') *)
+(*                     (CicPp.ppterm (CicMetaSubst.apply_subst subst' term)) *)
+(*                 ); *)
                 ((C.Rel (1 + lift_amount), subst', metasenv', ugraph')::res,
                  lifted_term)
+              )
+(*               ((C.Rel (1 + lift_amount), restore_subst context subst', *)
+(*                 metasenv', ugraph')::res, lifted_term) *)
             else
               ((C.Rel (1 + lift_amount), subst', metasenv', ugraph')::res,
                lifted_term)
           with e ->
-(*             print_endline ("beta_expand ERROR!: " ^ (Printexc.to_string e)); *)
+            if print_info then (
+              print_endline ("beta_expand ERROR!: " ^ (Printexc.to_string e));
+            );
             res, lifted_term
     in
 (*     Printf.printf "exit aux\n"; *)
@@ -455,14 +639,30 @@ let beta_expand ?(metas_ok=true) ?(match_only=false)
       ) exp_named_subst ([], [])
 
   in
-  let expansions, _ = aux 0 where context metasenv [] ugraph in
-  List.map
-    (fun (term, subst, metasenv, ugraph) ->
-       let term' = C.Lambda (C.Anonymous, type_of_what, term) in
-(*        Printf.printf "term is: %s\nsubst is:\n%s\n\n" *)
-(*          (CicPp.ppterm term') (print_subst subst); *)
-       (term', subst, metasenv, ugraph))
-    expansions
+  let expansions, _ =
+(*     let where = *)
+(*       if match_only then replace_metas (\* context *\) where *)
+(*       else where *)
+(*     in *)
+    if print_info then (
+      Printf.printf "searching %s inside %s\n"
+        (CicPp.ppterm what) (CicPp.ppterm where);
+    );
+    aux 0 where context metasenv [] ugraph
+  in
+  let mapfun =
+(*     if match_only then *)
+(*       (fun (term, subst, metasenv, ugraph) -> *)
+(*          let term' = *)
+(*            C.Lambda (C.Anonymous, type_of_what, restore_metas term) *)
+(*          and subst = restore_subst subst in *)
+(*          (term', subst, metasenv, ugraph)) *)
+(*     else *)
+      (fun (term, subst, metasenv, ugraph) ->
+         let term' = C.Lambda (C.Anonymous, type_of_what, term) in
+         (term', subst, metasenv, ugraph))
+  in
+  List.map mapfun expansions
 ;;
 
 
@@ -557,8 +757,17 @@ let fix_metas newmeta ((proof, (ty, left, right), menv, args) as equality) =
            (i, context, term)::menv)
       menv []
   in
+  let ty = repl ty
+  and left = repl left
+  and right = repl right in
+  let metas = (metas_of_term left) @ (metas_of_term right) in
+  let menv' = List.filter (fun (i, _, _) -> List.mem i metas) menv'
+  and newargs =
+    List.filter
+      (function Cic.Meta (i, _) -> List.mem i metas | _ -> assert false) newargs
+  in
   (newmeta + (List.length newargs) + 1,
-   (repl proof, (repl ty, repl left, repl right), menv', newargs))
+   (repl proof, (ty, left, right), menv', newargs))
 ;;
 
 
@@ -586,14 +795,13 @@ let superposition_left (metasenv, context, ugraph) target source =
   let proof, (eq_ty, left, right), _, _ = target in
   let eqproof, (ty, t1, t2), newmetas, args = source in
 
-  (* ALB: TODO check that ty and eq_ty are indeed equal... *)
-  (* assert (eq_ty = ty); *)
+  let compare_terms = !Utils.compare_terms in
 
   if eq_ty <> ty then
     []
   else    
     let where, is_left =
-      match nonrec_kbo left right with
+      match compare_terms left right with
       | Lt -> right, false
       | Gt -> left, true
       | _ -> (
@@ -604,16 +812,24 @@ let superposition_left (metasenv, context, ugraph) target source =
         )
     in
     let metasenv' = newmetas @ metasenv in
-    let res1 =
-      List.filter
-        (fun (t, s, m, ug) ->
-           nonrec_kbo (M.apply_subst s t1) (M.apply_subst s t2) = Gt)
-        (beta_expand t1 ty where context metasenv' ugraph)
-    and res2 =
-      List.filter
-        (fun (t, s, m, ug) ->
-           nonrec_kbo (M.apply_subst s t2) (M.apply_subst s t1) = Gt)
-        (beta_expand t2 ty where context metasenv' ugraph)
+    let result = compare_terms t1 t2 in
+    let res1, res2 = 
+      match result with
+      | Gt -> (beta_expand t1 ty where context metasenv' ugraph), []
+      | Lt -> [], (beta_expand t2 ty where context metasenv' ugraph)
+      | _ ->
+          let res1 =
+            List.filter
+              (fun (t, s, m, ug) ->
+                 compare_terms (M.apply_subst s t1) (M.apply_subst s t2) = Gt)
+              (beta_expand t1 ty where context metasenv' ugraph)
+          and res2 =
+            List.filter
+              (fun (t, s, m, ug) ->
+                 compare_terms (M.apply_subst s t2) (M.apply_subst s t1) = Gt)
+              (beta_expand t2 ty where context metasenv' ugraph)
+          in
+          res1, res2
     in
     (*   let what, other = *)
     (*     if is_left then left, right *)
@@ -660,8 +876,7 @@ let superposition_right newmeta (metasenv, context, ugraph) target source =
   let eqp', (ty', t1, t2), newm', args' = source in
   let maxmeta = ref newmeta in
 
-  (* TODO check if ty and ty' are equal... *)
-  (* assert (eq_ty = ty'); *)
+  let compare_terms = !Utils.compare_terms in
 
   if eq_ty <> ty' then
     newmeta, []
@@ -676,30 +891,53 @@ let superposition_right newmeta (metasenv, context, ugraph) target source =
     (*   in *)
     let condition left right what other (t, s, m, ug) =
       let subst = M.apply_subst s in
-      let cmp1 = nonrec_kbo (subst what) (subst other) in
-      let cmp2 = nonrec_kbo (subst left) (subst right) in
+      let cmp1 = compare_terms (subst what) (subst other) in
+      let cmp2 = compare_terms (subst left) (subst right) in
       (*     cmp1 = Gt && cmp2 = Gt *)
       cmp1 <> Lt && cmp1 <> Le && cmp2 <> Lt && cmp2 <> Le
         (*     && (ok t s other right ug) *)
     in
     let metasenv' = metasenv @ newmetas @ newm' in
     let beta_expand = beta_expand ~metas_ok:false in
-    let res1 =
-      List.filter
-        (condition left right t1 t2)
-        (beta_expand t1 eq_ty left context metasenv' ugraph)
-    and res2 =
-      List.filter
-        (condition left right t2 t1)
-        (beta_expand t2 eq_ty left context metasenv' ugraph)
-    and res3 =
-      List.filter
-        (condition right left t1 t2)
-        (beta_expand t1 eq_ty right context metasenv' ugraph)
-    and res4 =
-      List.filter
-        (condition right left t2 t1)
-        (beta_expand t2 eq_ty right context metasenv' ugraph)
+    let cmp1 = compare_terms left right
+    and cmp2 = compare_terms t1 t2 in
+    let res1, res2, res3, res4 =
+      let res l r s t =
+        List.filter
+          (condition l r s t)
+          (beta_expand s eq_ty l context metasenv' ugraph)
+      in
+      match cmp1, cmp2 with
+      | Gt, Gt ->
+          (beta_expand t1 eq_ty left context metasenv' ugraph), [], [], []
+      | Gt, Lt ->
+          [], (beta_expand t2 eq_ty left context metasenv' ugraph), [], []
+      | Lt, Gt ->
+          [], [], (beta_expand t1 eq_ty right context metasenv' ugraph), []
+      | Lt, Lt ->
+          [], [], [], (beta_expand t2 eq_ty right context metasenv' ugraph)
+      | Gt, _ ->
+          let res1 = res left right t1 t2
+          and res2 = res left right t2 t1 in
+          res1, res2, [], []
+      | Lt, _ ->
+          let res3 = res right left t1 t2
+          and res4 = res right left t2 t1 in
+          [], [], res3, res4
+      | _, Gt ->
+          let res1 = res left right t1 t2
+          and res3 = res right left t1 t2 in
+          res1, [], res3, []
+      | _, Lt ->
+          let res2 = res left right t2 t1
+          and res4 = res right left t2 t1 in
+          [], res2, [], res4
+      | _, _ ->
+          let res1 = res left right t1 t2
+          and res2 = res left right t2 t1
+          and res3 = res right left t1 t2
+          and res4 = res right left t2 t1 in
+          res1, res2, res3, res4
     in
     let newmetas = newmetas @ newm' in
     let newargs = args @ args' in
@@ -770,16 +1008,33 @@ let demodulation newmeta (metasenv, context, ugraph) target source =
 
   let proof, (eq_ty, left, right), metas, args = target
   and proof', (ty, t1, t2), metas', args' = source in
+
+  let compare_terms = !Utils.compare_terms in
+  
   if eq_ty <> ty then
     newmeta, target
   else
-    let get_params step =
-      match step with
-      | 3 -> true, t1, t2, HL.Logic.eq_ind_URI
-      | 2 -> false, t1, t2, HL.Logic.eq_ind_URI
-      | 1 -> true, t2, t1, HL.Logic.eq_ind_r_URI
-      | 0 -> false, t2, t1, HL.Logic.eq_ind_r_URI
-      | _ -> assert false
+    let first_step, get_params = 
+      match compare_terms t1 t2 with
+      | Gt -> 1, (function
+                    | 1 -> true, t1, t2, HL.Logic.eq_ind_URI
+                    | 0 -> false, t1, t2, HL.Logic.eq_ind_URI
+                    | _ -> assert false)
+      | Lt -> 1, (function
+                    | 1 -> true, t2, t1, HL.Logic.eq_ind_r_URI
+                    | 0 -> false, t2, t1, HL.Logic.eq_ind_r_URI
+                    | _ -> assert false)
+      | _ ->
+          let first_step = 3 in
+          let get_params step =
+            match step with
+            | 3 -> true, t1, t2, HL.Logic.eq_ind_URI
+            | 2 -> false, t1, t2, HL.Logic.eq_ind_URI
+            | 1 -> true, t2, t1, HL.Logic.eq_ind_r_URI
+            | 0 -> false, t2, t1, HL.Logic.eq_ind_r_URI
+            | _ -> assert false
+          in
+          first_step, get_params
     in
     let rec demodulate newmeta step metasenv target =
       let proof, (eq_ty, left, right), metas, args = target in
@@ -795,18 +1050,28 @@ let demodulation newmeta (metasenv, context, ugraph) target source =
 (*       print_newline (); *)
 
       let ok (t, s, m, ug) =
-        nonrec_kbo (M.apply_subst s what) (M.apply_subst s other) = Gt
+        compare_terms (M.apply_subst s what) (M.apply_subst s other) = Gt
       in
       let res =
         let r = (beta_expand ~metas_ok:false ~match_only:true
                    what ty (if is_left then left else right)
                    context (metasenv @ metas) ugraph) 
         in
-(*         print_endline "res:"; *)
-(*         List.iter (fun (t, s, m, ug) -> print_endline (CicPp.pp t names)) r; *)
-(*         print_newline (); *)
-(*         Printf.printf "metasenv:\n%s\n" (print_metasenv (metasenv @ metas)); *)
-(*         print_newline (); *)
+(*         let m' = metas_of_term what *)
+(*         and m'' = metas_of_term (if is_left then left else right) in *)
+(*         if (List.mem 527 m'') && (List.mem 6 m') then ( *)
+(*           Printf.printf *)
+(*             "demodulate\ntarget: %s\nwhat: %s\nother: %s\nis_left: %s\n" *)
+(*             (string_of_equality ~env target) (CicPp.pp what names) *)
+(*             (CicPp.pp other names) (string_of_bool is_left); *)
+(*           Printf.printf "step: %d" step; *)
+(*           print_newline (); *)
+(*           print_endline "res:"; *)
+(*           List.iter (fun (t, s, m, ug) -> print_endline (CicPp.pp t names)) r; *)
+(*           print_newline (); *)
+(*           Printf.printf "metasenv:\n%s\n" (print_metasenv (metasenv @ metas)); *)
+(*           print_newline (); *)
+(*         ); *)
         List.filter ok r
       in
       match res with
@@ -817,7 +1082,8 @@ let demodulation newmeta (metasenv, context, ugraph) target source =
           let newterm, newproof =
             match t with
             | C.Lambda (nn, ty, bo) ->
-                let bo' = M.apply_subst s (S.subst other bo) in
+(*                 let bo' = M.apply_subst s (S.subst other bo) in *)
+                let bo' = S.subst (M.apply_subst s other) bo in
                 let bo'' =
                   C.Appl (
                     [C.MutInd (HL.Logic.eq_URI, 0, []);
@@ -826,7 +1092,8 @@ let demodulation newmeta (metasenv, context, ugraph) target source =
                       else [S.lift 1 left; bo'])
                 in
                 let t' = C.Lambda (nn, ty, bo'') in
-                M.apply_subst s (S.subst other bo),
+(*                 M.apply_subst s (S.subst other bo), *)
+                bo', 
                 M.apply_subst s
                   (C.Appl [C.Const (eq_URI, []); ty; what; t';
                            proof; other; proof'])
@@ -834,24 +1101,39 @@ let demodulation newmeta (metasenv, context, ugraph) target source =
           in
           let newmeta, newtarget =
             let left, right =
-              if is_left then (newterm, M.apply_subst s right)
-              else (M.apply_subst s left, newterm) in
-            let newmetasenv = metasenv @ metas in
-            let newargs = args @ args' in
-            fix_metas newmeta
-              (newproof, (eq_ty, left, right), newmetasenv, newargs)
+(*               if is_left then (newterm, M.apply_subst s right) *)
+(*               else (M.apply_subst s left, newterm) in *)
+              if is_left then newterm, right
+              else left, newterm
+            in
+(*             let newmetasenv = metasenv @ metas in *)
+(*             let newargs = args @ args' in *)
+(*             fix_metas newmeta *)
+(*               (newproof, (eq_ty, left, right), newmetasenv, newargs) *)
+            let m = (metas_of_term left) @ (metas_of_term right) in
+            let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) metas
+            and newargs =
+              List.filter
+                (function C.Meta (i, _) -> List.mem i m | _ -> assert false)
+                args
+            in
+            newmeta, (newproof, (eq_ty, left, right), newmetasenv, newargs)
           in
-          Printf.printf
-            "demodulate, newtarget: %s\ntarget was: %s\n"
-            (string_of_equality ~env newtarget)
-            (string_of_equality ~env target);
-          print_newline ();
+(*           Printf.printf *)
+(*             "demodulate, newtarget: %s\ntarget was: %s\n" *)
+(*             (string_of_equality ~env newtarget) *)
+(*             (string_of_equality ~env target); *)
+(* (\*           let _, _, newm, newa = newtarget in *\) *)
+(* (\*           Printf.printf "newmetasenv:\n%s\nnewargs:\n%s\n" *\) *)
+(* (\*             (print_metasenv newm) *\) *)
+(* (\*             (String.concat "\n" (List.map CicPp.ppterm newa)); *\) *)
+(*           print_newline (); *)
           if is_identity env newtarget then
             newmeta, newtarget
           else
-            demodulate newmeta step metasenv newtarget
+            demodulate newmeta first_step metasenv newtarget
     in
-    demodulate newmeta 3 (metasenv @ metas') target
+    demodulate newmeta first_step (metasenv @ metas') target
 ;;
 
 
diff --git a/helm/ocaml/paramodulation/inference.mli b/helm/ocaml/paramodulation/inference.mli
index 4e1fe2c0a..bc37d1a64 100644
--- a/helm/ocaml/paramodulation/inference.mli
+++ b/helm/ocaml/paramodulation/inference.mli
@@ -63,4 +63,7 @@ val meta_convertibility_eq: equality -> equality -> bool
 
 val is_identity: environment -> equality -> bool
 
+val string_of_equality: ?env:environment -> equality -> string
+
+
 
diff --git a/helm/ocaml/paramodulation/saturation.ml b/helm/ocaml/paramodulation/saturation.ml
index a0148fb35..dbc85261b 100644
--- a/helm/ocaml/paramodulation/saturation.ml
+++ b/helm/ocaml/paramodulation/saturation.ml
@@ -15,6 +15,32 @@ let string_of_sign = function
 ;;
 
 
+(*
+let symbols_of_equality (_, (_, left, right), _, _) =
+  TermSet.union (symbols_of_term left) (symbols_of_term right)
+;;
+*)
+
+let symbols_of_equality ((_, (_, left, right), _, _) as equality) =
+  let m1 = symbols_of_term left in
+  let m = 
+    TermMap.fold
+      (fun k v res ->
+         try
+           let c = TermMap.find k res in
+           TermMap.add k (c+v) res
+         with Not_found ->
+           TermMap.add k v res)
+      (symbols_of_term right) m1
+  in
+(*   Printf.printf "symbols_of_equality %s:\n" *)
+(*     (string_of_equality equality); *)
+(*   TermMap.iter (fun k v -> Printf.printf "%s: %d\n" (CicPp.ppterm k) v) m; *)
+(*   print_newline (); *)
+  m
+;;
+
+
 module OrderedEquality =
 struct
   type t = Inference.equality
@@ -39,10 +65,15 @@ module EqualitySet = Set.Make(OrderedEquality);;
 let weight_age_ratio = ref 0;; (* settable by the user from the command line *)
 let weight_age_counter = ref !weight_age_ratio;;
 
-let set_selection = ref (fun set -> EqualitySet.min_elt set);;
+let symbols_ratio = ref 0;;
+let symbols_counter = ref 0;;
+
 
-let select env passive =
+let select env passive active =
   let (neg_list, neg_set), (pos_list, pos_set) = passive in
+  let remove eq l =
+    List.filter (fun e -> not (e = eq)) l
+  in
   if !weight_age_ratio > 0 then
     weight_age_counter := !weight_age_counter - 1;
   match !weight_age_counter with
@@ -55,19 +86,76 @@ let select env passive =
           (Positive, hd), (([], neg_set), (tl, EqualitySet.remove hd pos_set))
       | _, _ -> assert false
     )
-  | _ ->
-      let remove eq l =
-        List.filter (fun e -> not (e = eq)) l
+  | _ when (!symbols_counter > 0) && (EqualitySet.is_empty neg_set) -> (
+      symbols_counter := !symbols_counter - 1;
+      let cardinality map =
+        TermMap.fold (fun k v res -> res + v) map 0
       in
+      match active with
+      | (Negative, e)::_ ->
+          let symbols = symbols_of_equality e in
+          let card = cardinality symbols in
+          let f equality (i, e) =
+            let common, others =
+              TermMap.fold
+                (fun k v (r1, r2) ->
+                   if TermMap.mem k symbols then
+                     let c = TermMap.find k symbols in
+                     let c1 = abs (c - v) in
+                     let c2 = v - c1 in
+                     r1 + c2, r2 + c1
+                   else
+                     r1, r2 + v)
+                (symbols_of_equality equality) (0, 0)
+            in
+(*             Printf.printf "equality: %s, common: %d, others: %d\n" *)
+(*               (string_of_equality ~env equality) common others; *)
+            let c = others + (abs (common - card)) in
+            if c < i then (c, equality)
+            else (i, e)
+          in
+          let e1 = EqualitySet.min_elt pos_set in
+          let initial =
+            let common, others = 
+              TermMap.fold
+                (fun k v (r1, r2) ->
+                   if TermMap.mem k symbols then
+                     let c = TermMap.find k symbols in
+                     let c1 = abs (c - v) in
+                     let c2 = v - (abs (c - v)) in
+                     r1 + c1, r2 + c2
+                   else
+                     r1, r2 + v)
+                (symbols_of_equality e1) (0, 0)
+            in
+            (others + (abs (common - card))), e1
+          in
+          let _, current = EqualitySet.fold f pos_set initial in
+          Printf.printf "\nsymbols-based selection: %s\n\n"
+            (string_of_equality ~env current);
+          (Positive, current),
+          (([], neg_set),
+           (remove current pos_list, EqualitySet.remove current pos_set))
+      | _ ->
+            let current = EqualitySet.min_elt pos_set in
+          let passive =
+            (neg_list, neg_set),
+            (remove current pos_list, EqualitySet.remove current pos_set)
+          in
+          (Positive, current), passive
+    )
+  | _ ->
+      symbols_counter := !symbols_ratio;
+      let set_selection set = EqualitySet.min_elt set in
       if EqualitySet.is_empty neg_set then
-        let current = !set_selection pos_set in
+        let current = set_selection pos_set in
         let passive =
           (neg_list, neg_set),
           (remove current pos_list, EqualitySet.remove current pos_set)
         in
         (Positive, current), passive
       else
-        let current = !set_selection neg_set in
+        let current = set_selection neg_set in
         let passive =
           (remove current neg_list, EqualitySet.remove current neg_set),
           (pos_list, pos_set)
@@ -156,8 +244,16 @@ let contains_empty env (negative, positive) =
 ;;
 
 
-let forward_simplify env (sign, current) active =
+let forward_simplify env ?(active=[]) ?passive (sign, current) =
   (* first step, remove already present equalities *)
+  let pn, pp =
+    match passive with
+    | None -> [], []
+    | Some ((pn, _), (pp, _)) ->
+        (List.map (fun e -> Negative, e) pn),
+        (List.map (fun e -> Positive, e) pp)
+  in
+  let all = active @ pn @ pp in
   let duplicate =
     let rec aux = function
       | [] -> false
@@ -166,7 +262,7 @@ let forward_simplify env (sign, current) active =
           else aux tl
       | _::tl -> aux tl
     in
-    aux active
+    aux all
   in
   if duplicate then
     None
@@ -175,40 +271,61 @@ let forward_simplify env (sign, current) active =
       | [] -> Some (sign, current)
       | (Negative, _)::tl -> aux env (sign, current) tl
       | (Positive, equality)::tl ->
-          let newmeta, current =
+          let newmeta, newcurrent =
             demodulation !maxmeta env current equality in
           maxmeta := newmeta;
-          if is_identity env current then
+          if is_identity env newcurrent then
             None
+          else if newcurrent <> current then
+            aux env (sign, newcurrent) active
           else
-            aux env (sign, current) tl
+            aux env (sign, newcurrent) tl
     in
-    aux env (sign, current) active
+    aux env (sign, current) all
 ;;
 
 
-let forward_simplify_new env (new_neg, new_pos) active =
+let forward_simplify_new env ?(active=[]) ?passive (new_neg, new_pos) =
+  let pn, pp =
+    match passive with
+    | None -> [], []
+    | Some ((pn, _), (pp, _)) ->
+        (List.map (fun e -> Negative, e) pn),
+        (List.map (fun e -> Positive, e) pp)
+  in
+  let all = active @ pn @ pp in
   let remove_identities equalities =
     let ok eq = not (is_identity env eq) in
     List.filter ok equalities
   in
-  let rec simpl active target =
-    match active with
+  let rec simpl all' target =
+    match all' with
     | [] -> target
     | (Negative, _)::tl -> simpl tl target
     | (Positive, source)::tl ->
-        let newmeta, target = demodulation !maxmeta env target source in
+        let newmeta, newtarget = demodulation !maxmeta env target source in
         maxmeta := newmeta;
-        if is_identity env target then target
-        else simpl tl target
+        if is_identity env newtarget then newtarget
+        else if newtarget <> target then (
+(*           Printf.printf "OK:\n%s\n%s\n" *)
+(*             (string_of_equality ~env target) *)
+(*             (string_of_equality ~env newtarget); *)
+(*           print_newline (); *)
+          simpl all newtarget
+        )
+        else simpl tl newtarget
+  in
+  let new_neg = List.map (simpl all) new_neg
+  and new_pos = remove_identities (List.map (simpl all) new_pos) in
+  let new_pos_set =
+    List.fold_left (fun s e -> EqualitySet.add e s) EqualitySet.empty new_pos
   in
-  let new_neg = List.map (simpl active) new_neg
-  and new_pos = List.map (simpl active) new_pos in
-  new_neg, remove_identities new_pos
+  new_neg, EqualitySet.elements new_pos_set
 ;;
 
 
-let backward_simplify env (sign, current) active =
+(*
+let backward_simplify_active env (sign, current) active =
   match sign with
   | Negative -> active
   | Positive ->
@@ -234,17 +351,75 @@ let backward_simplify env (sign, current) active =
         (fun (s, eq) res -> if find eq res then res else (s, eq)::res)
         active []
 ;;
+*)
+
+
+let backward_simplify_active env (new_neg, new_pos) active =
+  let new_pos = List.map (fun e -> Positive, e) new_pos in
+  let active = 
+    List.fold_right
+      (fun (s, equality) res ->
+         match forward_simplify env ~active:new_pos (s, equality) with
+         | None -> res
+         | Some e -> e::res)
+      active []
+  in
+  let find eq1 where =
+    List.exists (fun (s, e) -> meta_convertibility_eq eq1 e) where
+  in
+  List.fold_right
+    (fun (s, eq) res ->
+       if (is_identity env eq) || (find eq res) then
+         res
+       else
+         (s, eq)::res)
+    active []
+;;
+
+
+let backward_simplify_passive env (new_neg, new_pos) passive =
+  let new_pos = List.map (fun e -> Positive, e) new_pos in
+  let (nl, ns), (pl, ps) = passive in
+  let f sign equality (resl, ress, newn) =
+    match forward_simplify env ~active:new_pos (sign, equality) with
+    | None -> resl, EqualitySet.remove equality ress, newn
+    | Some (s, e) ->
+        if equality = e then
+          equality::resl, ress, newn
+        else
+          let ress = EqualitySet.remove equality ress in
+          resl, ress, e::newn
+  in
+  let nl, ns, newn = List.fold_right (f Negative) nl ([], ns, [])
+  and pl, ps, newp = List.fold_right (f Positive) pl ([], ps, []) in
+  match newn, newp with
+  | [], [] -> ((nl, ns), (pl, ps)), None
+  | _, _ -> ((nl, ns), (pl, ps)), Some (newn, newp)
+;;
+
+
+let backward_simplify env ?(active=[]) ?passive new' =
+  let active = backward_simplify_active env new' active in
+  match passive with
+  | None ->
+      active, (([], EqualitySet.empty), ([], EqualitySet.empty)), None
+  | Some passive ->
+      let passive, new' =
+        backward_simplify_passive env new' passive in
+      active, passive, new'
+;;
 
 
+  
 let rec given_clause env passive active =
   match passive_is_empty passive with
   | true -> Failure
   | false ->
 (*       Printf.printf "before select\n"; *)
-      let (sign, current), passive = select env passive in
+      let (sign, current), passive = select env passive active in
 (*       Printf.printf "before simplification: sign: %s\ncurrent: %s\n\n" *)
 (*         (string_of_sign sign) (string_of_equality ~env current); *)
-      match forward_simplify env (sign, current) active with
+      match forward_simplify env (sign, current) ~active ~passive with
       | None when sign = Negative ->
           Printf.printf "OK!!! %s %s" (string_of_sign sign)
             (string_of_equality ~env current);
@@ -257,56 +432,148 @@ let rec given_clause env passive active =
 (*           print_newline (); *)
           given_clause env passive active
       | Some (sign, current) ->
-(*           Printf.printf "selected: %s %s" *)
-(*             (string_of_sign sign) (string_of_equality ~env current); *)
-(*           print_newline (); *)
+          print_endline "\n================================================";
+          Printf.printf "selected: %s %s"
+            (string_of_sign sign) (string_of_equality ~env current);
+          print_newline ();
 
           let new' = infer env sign current active in
 
-          let new' = forward_simplify_new env new' active in
-          
-          let active =
-            backward_simplify env (sign, current) active
-(*             match new' with *)
-(*             | [], [] -> backward_simplify env (sign, current) active *)
-(*             | _ -> active *)
-          in
+          let res, proof = contains_empty env new' in
+          if res then
+            Success (proof, env)
+          else
+            let new' = forward_simplify_new env new' ~active in
+            
+            (*           let active, passive, retained = *)
+            (*             backward_simplify env [(sign, current)] ~active ~passive *)
+            (*           in *)
+            let active =
+              match sign with
+              | Negative -> active
+              | Positive ->
+                  let active, _, _ =
+                    backward_simplify env ([], [current]) ~active
+                  in
+                  active
+            in
+            let _ =
+              Printf.printf "active:\n%s\n"
+                (String.concat "\n"
+                   ((List.map
+                       (fun (s, e) -> (string_of_sign s) ^ " " ^
+                          (string_of_equality ~env e)) active)));
+              print_newline ();
+            in
+            let _ =
+              match new' with
+              | neg, pos ->
+                  Printf.printf "new':\n%s\n"
+                    (String.concat "\n"
+                       ((List.map
+                           (fun e -> "Negative " ^
+                              (string_of_equality ~env e)) neg) @
+                          (List.map
+                             (fun e -> "Positive " ^
+                                (string_of_equality ~env e)) pos)));
+                  print_newline ();
+            in
+            match contains_empty env new' with
+            | false, _ -> 
+                let active =
+                  match sign with
+                  | Negative -> (sign, current)::active
+                  | Positive -> active @ [(sign, current)]
+                in
+                let passive = add_to_passive passive new' in
+                let (_, ns), (_, ps) = passive in
+                Printf.printf "passive:\n%s\n"
+                  (String.concat "\n"
+                     ((List.map (fun e -> "Negative " ^
+                                   (string_of_equality ~env e))
+                         (EqualitySet.elements ns)) @
+                        (List.map (fun e -> "Positive " ^
+                                     (string_of_equality ~env e))
+                           (EqualitySet.elements ps))));
+                print_newline ();
+                given_clause env passive active
+            | true, proof ->
+                Success (proof, env)
+;;
 
-          print_endline "\n================================================";
-          let _ =
-            Printf.printf "active:\n%s\n"
+
+(*
+let rec given_clause env passive active =
+  match passive_is_empty passive with
+  | true -> Failure
+  | false ->
+(*       Printf.printf "before select\n"; *)
+      let (sign, current), passive = select env passive active in
+(*       Printf.printf "before simplification: sign: %s\ncurrent: %s\n\n" *)
+(*         (string_of_sign sign) (string_of_equality ~env current); *)
+      print_endline "\n================================================";
+      Printf.printf "selected: %s %s"
+        (string_of_sign sign) (string_of_equality ~env current);
+      print_newline ();
+
+      let new' = infer env sign current active in
+
+      let rec simplify new' active passive =
+        let new' = forward_simplify_new env new' ~active ~passive in
+        let active, passive, retained =
+          backward_simplify env new' ~active ~passive
+        in
+        match retained with
+        | None -> active, passive, new'
+        | Some (rn, rp) ->
+            let nn, np = new' in
+            simplify (nn @ rn, np @ rp) active passive
+      in
+      let active, passive, new' = simplify new' active passive in
+      let _ =
+        Printf.printf "active:\n%s\n"
+          (String.concat "\n"
+             ((List.map
+                 (fun (s, e) -> (string_of_sign s) ^ " " ^
+                    (string_of_equality ~env e)) active)));
+        print_newline ();
+      in
+      let _ =
+        match new' with
+        | neg, pos ->
+            Printf.printf "new':\n%s\n"
               (String.concat "\n"
                  ((List.map
-                     (fun (s, e) -> (string_of_sign s) ^ " " ^
-                        (string_of_equality ~env e)) active)));
+                     (fun e -> "Negative " ^
+                        (string_of_equality ~env e)) neg) @
+                    (List.map
+                       (fun e -> "Positive " ^
+                          (string_of_equality ~env e)) pos)));
             print_newline ();
+      in
+      match contains_empty env new' with
+      | false, _ -> 
+          let active =
+            match sign with
+            | Negative -> (sign, current)::active
+            | Positive -> active @ [(sign, current)]
           in
-
-(*           let _ = *)
-(*             match new' with *)
-(*             | neg, pos -> *)
-(*                 Printf.printf "new':\n%s\n" *)
-(*                   (String.concat "\n" *)
-(*                      ((List.map *)
-(*                          (fun e -> "Negative " ^ *)
-(*                             (string_of_equality ~env e)) neg) @ *)
-(*                         (List.map *)
-(*                            (fun e -> "Positive " ^ *)
-(*                               (string_of_equality ~env e)) pos))); *)
-(*                 print_newline (); *)
-(*           in                 *)
-          match contains_empty env new' with
-          | false, _ -> 
-              let active =
-                match sign with
-                | Negative -> (sign, current)::active
-                | Positive -> active @ [(sign, current)]
-              in
-              let passive = add_to_passive passive new' in
-              given_clause env passive active
-          | true, proof ->
-              Success (proof, env)
+          let passive = add_to_passive passive new' in
+          let (_, ns), (_, ps) = passive in
+          Printf.printf "passive:\n%s\n"
+            (String.concat "\n"
+               ((List.map (fun e -> "Negative " ^
+                             (string_of_equality ~env e))
+                   (EqualitySet.elements ns)) @
+                  (List.map (fun e -> "Positive " ^
+                               (string_of_equality ~env e))
+                     (EqualitySet.elements ps))));
+          print_newline ();
+          given_clause env passive active
+      | true, proof ->
+          Success (proof, env)
 ;;
+*)
 
 
 let get_from_user () =
@@ -354,17 +621,17 @@ let main () =
       (function (_, (ty, t1, t2), _, _) ->
          let w1 = weight_of_term t1 in
          let w2 = weight_of_term t2 in
-         let res = nonrec_kbo t1 t2 in
+         let res = !compare_terms t1 t2 in
          Printf.printf "{%s}: %s<%s> %s %s<%s>\n" (PP.ppterm ty)
            (PP.ppterm t1) (string_of_weight w1)
            (string_of_comparison res)
            (PP.ppterm t2) (string_of_weight w2))
       equalities;
     print_endline "--------------------------------------------------";
-    let start = Sys.time () in
+    let start = Unix.gettimeofday () in
     print_endline "GO!";
     let res = given_clause env passive active in
-    let finish = Sys.time () in
+    let finish = Unix.gettimeofday () in
     match res with
     | Failure ->
         Printf.printf "NO proof found! :-(\n\n"
@@ -381,17 +648,23 @@ let main () =
 let configuration_file = ref "../../gTopLevel/gTopLevel.conf.xml";;
 
 let _ =
-  let set_ratio v = weight_age_ratio := v; weight_age_counter := v
-  and set_sel () = set_selection := (fun s -> EqualitySet.max_elt s)
+  let set_ratio v = weight_age_ratio := (v+1); weight_age_counter := (v+1)
+  and set_sel v = symbols_ratio := v; symbols_counter := v;
   and set_conf f = configuration_file := f
+  and set_lpo () = Utils.compare_terms := lpo
+  and set_kbo () = Utils.compare_terms := nonrec_kbo
   in
   Arg.parse [
-    "-r", Arg.Int set_ratio, "Weight-Age equality selection ratio";
+    "-r", Arg.Int set_ratio, "Weight-Age equality selection ratio (default: 0)";
 
-    "-i", Arg.Unit set_sel,
-    "Inverse selection (select heaviest equalities before)";
+    "-s", Arg.Int set_sel,
+    "symbols-based selection ratio (relative to the weight ratio)";
 
     "-c", Arg.String set_conf, "Configuration file (for the db connection)";
+
+    "-lpo", Arg.Unit set_lpo, "Use lpo term ordering";
+
+    "-kbo", Arg.Unit set_kbo, "Use (non-recursive) kbo term ordering (default)";
   ] (fun a -> ()) "Usage:"
 in
 Helm_registry.load_from !configuration_file;