helm/ocaml/paramodulation/saturation.ml

   1 open Inference;;
   2 open Utils;;
   3
   4 type result =
   5   | Failure
   6   | Success of Cic.term option * environment
   7 ;;
   8
   9
  10 type equality_sign = Negative | Positive;;
  11
  12 let string_of_sign = function
  13   | Negative -> "Negative"
  14   | Positive -> "Positive"
  15 ;;
  16
  17
  18 (*
  19 let symbols_of_equality (_, (_, left, right), _, _) =
  20   TermSet.union (symbols_of_term left) (symbols_of_term right)
  21 ;;
  22 *)
  23
  24 let symbols_of_equality ((_, (_, left, right), _, _) as equality) =
  25   let m1 = symbols_of_term left in
  26   let m =
  27     TermMap.fold
  28       (fun k v res ->
  29          try
  30            let c = TermMap.find k res in
  31            TermMap.add k (c+v) res
  32          with Not_found ->
  33            TermMap.add k v res)
  34       (symbols_of_term right) m1
  35   in
  36 (*   Printf.printf "symbols_of_equality %s:\n" *)
  37 (*     (string_of_equality equality); *)
  38 (*   TermMap.iter (fun k v -> Printf.printf "%s: %d\n" (CicPp.ppterm k) v) m; *)
  39 (*   print_newline (); *)
  40   m
  41 ;;
  42
  43
  44 module OrderedEquality =
  45 struct
  46   type t = Inference.equality
  47
  48   let compare eq1 eq2 =
  49     match meta_convertibility_eq eq1 eq2 with
  50     | true -> 0
  51     | false ->
  52         let _, (ty, left, right), _, _ = eq1
  53         and _, (ty', left', right'), _, _ = eq2 in
  54         let weight_of t = fst (weight_of_term ~consider_metas:false t) in
  55         let w1 = (weight_of ty) + (weight_of left) + (weight_of right)
  56         and w2 = (weight_of ty') + (weight_of left') + (weight_of right') in
  57         match Pervasives.compare w1 w2 with
  58         | 0 -> Pervasives.compare eq1 eq2
  59         | res -> res
  60 end
  61
  62 module EqualitySet = Set.Make(OrderedEquality);;
  63
  64
  65 let weight_age_ratio = ref 0;; (* settable by the user from the command line *)
  66 let weight_age_counter = ref !weight_age_ratio;;
  67
  68 let symbols_ratio = ref 0;;
  69 let symbols_counter = ref 0;;
  70
  71
  72 let select env passive active =
  73   let (neg_list, neg_set), (pos_list, pos_set) = passive in
  74   let remove eq l =
  75     List.filter (fun e -> not (e = eq)) l
  76   in
  77   if !weight_age_ratio > 0 then
  78     weight_age_counter := !weight_age_counter - 1;
  79   match !weight_age_counter with
  80   | 0 -> (
  81       weight_age_counter := !weight_age_ratio;
  82       match neg_list, pos_list with
  83       | hd::tl, pos ->
  84           (Negative, hd), ((tl, EqualitySet.remove hd neg_set), (pos, pos_set))
  85       | [], hd::tl ->
  86           (Positive, hd), (([], neg_set), (tl, EqualitySet.remove hd pos_set))
  87       | _, _ -> assert false
  88     )
  89   | _ when (!symbols_counter > 0) && (EqualitySet.is_empty neg_set) -> (
  90       symbols_counter := !symbols_counter - 1;
  91       let cardinality map =
  92         TermMap.fold (fun k v res -> res + v) map 0
  93       in
  94       match active with
  95       | (Negative, e)::_ ->
  96           let symbols = symbols_of_equality e in
  97           let card = cardinality symbols in
  98           let f equality (i, e) =
  99             let common, others =
 100               TermMap.fold
 101                 (fun k v (r1, r2) ->
 102                    if TermMap.mem k symbols then
 103                      let c = TermMap.find k symbols in
 104                      let c1 = abs (c - v) in
 105                      let c2 = v - c1 in
 106                      r1 + c2, r2 + c1
 107                    else
 108                      r1, r2 + v)
 109                 (symbols_of_equality equality) (0, 0)
 110             in
 111 (*             Printf.printf "equality: %s, common: %d, others: %d\n" *)
 112 (*               (string_of_equality ~env equality) common others; *)
 113             let c = others + (abs (common - card)) in
 114             if c < i then (c, equality)
 115             else (i, e)
 116           in
 117           let e1 = EqualitySet.min_elt pos_set in
 118           let initial =
 119             let common, others =
 120               TermMap.fold
 121                 (fun k v (r1, r2) ->
 122                    if TermMap.mem k symbols then
 123                      let c = TermMap.find k symbols in
 124                      let c1 = abs (c - v) in
 125                      let c2 = v - (abs (c - v)) in
 126                      r1 + c1, r2 + c2
 127                    else
 128                      r1, r2 + v)
 129                 (symbols_of_equality e1) (0, 0)
 130             in
 131             (others + (abs (common - card))), e1
 132           in
 133           let _, current = EqualitySet.fold f pos_set initial in
 134           Printf.printf "\nsymbols-based selection: %s\n\n"
 135             (string_of_equality ~env current);
 136           (Positive, current),
 137           (([], neg_set),
 138            (remove current pos_list, EqualitySet.remove current pos_set))
 139       | _ ->
 140             let current = EqualitySet.min_elt pos_set in
 141           let passive =
 142             (neg_list, neg_set),
 143             (remove current pos_list, EqualitySet.remove current pos_set)
 144           in
 145           (Positive, current), passive
 146     )
 147   | _ ->
 148       symbols_counter := !symbols_ratio;
 149       let set_selection set = EqualitySet.min_elt set in
 150       if EqualitySet.is_empty neg_set then
 151         let current = set_selection pos_set in
 152         let passive =
 153           (neg_list, neg_set),
 154           (remove current pos_list, EqualitySet.remove current pos_set)
 155         in
 156         (Positive, current), passive
 157       else
 158         let current = set_selection neg_set in
 159         let passive =
 160           (remove current neg_list, EqualitySet.remove current neg_set),
 161           (pos_list, pos_set)
 162         in
 163         (Negative, current), passive
 164 ;;
 165
 166
 167 let make_passive neg pos =
 168   let set_of equalities =
 169     List.fold_left (fun s e -> EqualitySet.add e s) EqualitySet.empty equalities
 170   in
 171   (neg, set_of neg), (pos, set_of pos)
 172 ;;
 173
 174
 175 let add_to_passive passive (new_neg, new_pos) =
 176   let (neg_list, neg_set), (pos_list, pos_set) = passive in
 177   let ok set equality = not (EqualitySet.mem equality set) in
 178   let neg = List.filter (ok neg_set) new_neg
 179   and pos = List.filter (ok pos_set) new_pos in
 180   let add set equalities =
 181     List.fold_left (fun s e -> EqualitySet.add e s) set equalities
 182   in
 183   (neg @ neg_list, add neg_set neg), (pos_list @ pos, add pos_set pos)
 184 ;;
 185
 186
 187 let passive_is_empty = function
 188   | ([], _), ([], _) -> true
 189   | _ -> false
 190 ;;
 191
 192
 193 (* TODO: find a better way! *)
 194 let maxmeta = ref 0;;
 195
 196 let infer env sign current active =
 197   let rec infer_negative current = function
 198     | [] -> [], []
 199     | (Negative, _)::tl -> infer_negative current tl
 200     | (Positive, equality)::tl ->
 201         let res = superposition_left env current equality in
 202         let neg, pos = infer_negative current tl in
 203         res @ neg, pos
 204
 205   and infer_positive current = function
 206     | [] -> [], []
 207     | (Negative, equality)::tl ->
 208         let res = superposition_left env equality current in
 209         let neg, pos = infer_positive current tl in
 210         res @ neg, pos
 211     | (Positive, equality)::tl ->
 212         let maxm, res = superposition_right !maxmeta env current equality in
 213         let maxm, res' = superposition_right maxm env equality current in
 214         maxmeta := maxm;
 215         let neg, pos = infer_positive current tl in
 216
 217 (*         Printf.printf "risultato di superposition_right: %s %s\n%s\n\n" *)
 218 (*           (string_of_equality ~env current) (string_of_equality ~env equality) *)
 219 (*           (String.concat "\n" (List.map (string_of_equality ~env) res)); *)
 220 (*         Printf.printf "risultato di superposition_right: %s %s\n%s\n\n" *)
 221 (*           (string_of_equality ~env equality) (string_of_equality ~env current) *)
 222 (*           (String.concat "\n" (List.map (string_of_equality ~env) res')); *)
 223
 224         neg, res @ res' @ pos
 225   in
 226   match sign with
 227   | Negative -> infer_negative current active
 228   | Positive -> infer_positive current active
 229 ;;
 230
 231
 232 let contains_empty env (negative, positive) =
 233   let metasenv, context, ugraph = env in
 234   try
 235     let (proof, _, _, _) =
 236       List.find
 237         (fun (proof, (ty, left, right), m, a) ->
 238            fst (CicReduction.are_convertible context left right ugraph))
 239         negative
 240     in
 241     true, Some proof
 242   with Not_found ->
 243     false, None
 244 ;;
 245
 246
 247 let forward_simplify env ?(active=[]) ?passive (sign, current) =
 248   (* first step, remove already present equalities *)
 249   let pn, pp =
 250     match passive with
 251     | None -> [], []
 252     | Some ((pn, _), (pp, _)) ->
 253         (List.map (fun e -> Negative, e) pn),
 254         (List.map (fun e -> Positive, e) pp)
 255   in
 256   let all = active @ pn @ pp in
 257   let duplicate =
 258     let rec aux = function
 259       | [] -> false
 260       | (s, eq)::tl when s = sign ->
 261           if meta_convertibility_eq current eq then true
 262           else aux tl
 263       | _::tl -> aux tl
 264     in
 265     aux all
 266   in
 267   if duplicate then
 268     None
 269   else
 270     let rec aux env (sign, current) = function
 271       | [] -> Some (sign, current)
 272       | (Negative, _)::tl -> aux env (sign, current) tl
 273       | (Positive, equality)::tl ->
 274           let newmeta, newcurrent =
 275             demodulation !maxmeta env current equality in
 276           maxmeta := newmeta;
 277           if is_identity env newcurrent then
 278             None
 279           else if newcurrent <> current then
 280             aux env (sign, newcurrent) active
 281           else
 282             aux env (sign, newcurrent) tl
 283     in
 284     aux env (sign, current) all
 285 ;;
 286
 287
 288 let forward_simplify_new env ?(active=[]) ?passive (new_neg, new_pos) =
 289   let pn, pp =
 290     match passive with
 291     | None -> [], []
 292     | Some ((pn, _), (pp, _)) ->
 293         (List.map (fun e -> Negative, e) pn),
 294         (List.map (fun e -> Positive, e) pp)
 295   in
 296   let all = active @ pn @ pp in
 297   let remove_identities equalities =
 298     let ok eq = not (is_identity env eq) in
 299     List.filter ok equalities
 300   in
 301   let rec simpl all' target =
 302     match all' with
 303     | [] -> target
 304     | (Negative, _)::tl -> simpl tl target
 305     | (Positive, source)::tl ->
 306         let newmeta, newtarget = demodulation !maxmeta env target source in
 307         maxmeta := newmeta;
 308         if is_identity env newtarget then newtarget
 309         else if newtarget <> target then (
 310 (*           Printf.printf "OK:\n%s\n%s\n" *)
 311 (*             (string_of_equality ~env target) *)
 312 (*             (string_of_equality ~env newtarget); *)
 313 (*           print_newline (); *)
 314           simpl all newtarget
 315         )
 316         else simpl tl newtarget
 317   in
 318   let new_neg = List.map (simpl all) new_neg
 319   and new_pos = remove_identities (List.map (simpl all) new_pos) in
 320   let new_pos_set =
 321     List.fold_left (fun s e -> EqualitySet.add e s) EqualitySet.empty new_pos
 322   in
 323   new_neg, EqualitySet.elements new_pos_set
 324 ;;
 325
 326
 327 (*
 328 let backward_simplify_active env (sign, current) active =
 329   match sign with
 330   | Negative -> active
 331   | Positive ->
 332       let active =
 333         List.map
 334           (fun (s, equality) ->
 335              (*            match s with *)
 336              (*            | Negative -> s, equality *)
 337              (*            | Positive -> *)
 338              let newmeta, equality =
 339                demodulation !maxmeta env equality current in
 340              maxmeta := newmeta;
 341              s, equality)
 342           active
 343       in
 344       let active =
 345         List.filter (fun (s, eq) -> not (is_identity env eq)) active
 346       in
 347       let find eq1 where =
 348         List.exists (fun (s, e) -> meta_convertibility_eq eq1 e) where
 349       in
 350       List.fold_right
 351         (fun (s, eq) res -> if find eq res then res else (s, eq)::res)
 352         active []
 353 ;;
 354 *)
 355
 356
 357 let backward_simplify_active env (new_neg, new_pos) active =
 358   let new_pos = List.map (fun e -> Positive, e) new_pos in
 359   let active =
 360     List.fold_right
 361       (fun (s, equality) res ->
 362          match forward_simplify env ~active:new_pos (s, equality) with
 363          | None -> res
 364          | Some e -> e::res)
 365       active []
 366   in
 367   let find eq1 where =
 368     List.exists (fun (s, e) -> meta_convertibility_eq eq1 e) where
 369   in
 370   List.fold_right
 371     (fun (s, eq) res ->
 372        if (is_identity env eq) || (find eq res) then
 373          res
 374        else
 375          (s, eq)::res)
 376     active []
 377 ;;
 378
 379
 380 let backward_simplify_passive env (new_neg, new_pos) passive =
 381   let new_pos = List.map (fun e -> Positive, e) new_pos in
 382   let (nl, ns), (pl, ps) = passive in
 383   let f sign equality (resl, ress, newn) =
 384     match forward_simplify env ~active:new_pos (sign, equality) with
 385     | None -> resl, EqualitySet.remove equality ress, newn
 386     | Some (s, e) ->
 387         if equality = e then
 388           equality::resl, ress, newn
 389         else
 390           let ress = EqualitySet.remove equality ress in
 391           resl, ress, e::newn
 392   in
 393   let nl, ns, newn = List.fold_right (f Negative) nl ([], ns, [])
 394   and pl, ps, newp = List.fold_right (f Positive) pl ([], ps, []) in
 395   match newn, newp with
 396   | [], [] -> ((nl, ns), (pl, ps)), None
 397   | _, _ -> ((nl, ns), (pl, ps)), Some (newn, newp)
 398 ;;
 399
 400
 401 let backward_simplify env ?(active=[]) ?passive new' =
 402   let active = backward_simplify_active env new' active in
 403   match passive with
 404   | None ->
 405       active, (([], EqualitySet.empty), ([], EqualitySet.empty)), None
 406   | Some passive ->
 407       let passive, new' =
 408         backward_simplify_passive env new' passive in
 409       active, passive, new'
 410 ;;
 411
 412
 413
 414 let rec given_clause env passive active =
 415   match passive_is_empty passive with
 416   | true -> Failure
 417   | false ->
 418 (*       Printf.printf "before select\n"; *)
 419       let (sign, current), passive = select env passive active in
 420 (*       Printf.printf "before simplification: sign: %s\ncurrent: %s\n\n" *)
 421 (*         (string_of_sign sign) (string_of_equality ~env current); *)
 422       match forward_simplify env (sign, current) ~active ~passive with
 423       | None when sign = Negative ->
 424           Printf.printf "OK!!! %s %s" (string_of_sign sign)
 425             (string_of_equality ~env current);
 426           print_newline ();
 427           let proof, _, _, _ = current in
 428           Success (Some proof, env)
 429       | None ->
 430 (*           Printf.printf "avanti... %s %s" (string_of_sign sign) *)
 431 (*             (string_of_equality ~env current); *)
 432 (*           print_newline (); *)
 433           given_clause env passive active
 434       | Some (sign, current) ->
 435           print_endline "\n================================================";
 436           Printf.printf "selected: %s %s"
 437             (string_of_sign sign) (string_of_equality ~env current);
 438           print_newline ();
 439
 440           let new' = infer env sign current active in
 441
 442           let res, proof = contains_empty env new' in
 443           if res then
 444             Success (proof, env)
 445           else
 446             let new' = forward_simplify_new env new' ~active in
 447
 448             (*           let active, passive, retained = *)
 449             (*             backward_simplify env [(sign, current)] ~active ~passive *)
 450             (*           in *)
 451             let active =
 452               match sign with
 453               | Negative -> active
 454               | Positive ->
 455                   let active, _, _ =
 456                     backward_simplify env ([], [current]) ~active
 457                   in
 458                   active
 459             in
 460             let _ =
 461               Printf.printf "active:\n%s\n"
 462                 (String.concat "\n"
 463                    ((List.map
 464                        (fun (s, e) -> (string_of_sign s) ^ " " ^
 465                           (string_of_equality ~env e)) active)));
 466               print_newline ();
 467             in
 468             let _ =
 469               match new' with
 470               | neg, pos ->
 471                   Printf.printf "new':\n%s\n"
 472                     (String.concat "\n"
 473                        ((List.map
 474                            (fun e -> "Negative " ^
 475                               (string_of_equality ~env e)) neg) @
 476                           (List.map
 477                              (fun e -> "Positive " ^
 478                                 (string_of_equality ~env e)) pos)));
 479                   print_newline ();
 480             in
 481             match contains_empty env new' with
 482             | false, _ ->
 483                 let active =
 484                   match sign with
 485                   | Negative -> (sign, current)::active
 486                   | Positive -> active @ [(sign, current)]
 487                 in
 488                 let passive = add_to_passive passive new' in
 489                 let (_, ns), (_, ps) = passive in
 490                 Printf.printf "passive:\n%s\n"
 491                   (String.concat "\n"
 492                      ((List.map (fun e -> "Negative " ^
 493                                    (string_of_equality ~env e))
 494                          (EqualitySet.elements ns)) @
 495                         (List.map (fun e -> "Positive " ^
 496                                      (string_of_equality ~env e))
 497                            (EqualitySet.elements ps))));
 498                 print_newline ();
 499                 given_clause env passive active
 500             | true, proof ->
 501                 Success (proof, env)
 502 ;;
 503
 504
 505 (*
 506 let rec given_clause env passive active =
 507   match passive_is_empty passive with
 508   | true -> Failure
 509   | false ->
 510 (*       Printf.printf "before select\n"; *)
 511       let (sign, current), passive = select env passive active in
 512 (*       Printf.printf "before simplification: sign: %s\ncurrent: %s\n\n" *)
 513 (*         (string_of_sign sign) (string_of_equality ~env current); *)
 514       print_endline "\n================================================";
 515       Printf.printf "selected: %s %s"
 516         (string_of_sign sign) (string_of_equality ~env current);
 517       print_newline ();
 518
 519       let new' = infer env sign current active in
 520
 521       let rec simplify new' active passive =
 522         let new' = forward_simplify_new env new' ~active ~passive in
 523         let active, passive, retained =
 524           backward_simplify env new' ~active ~passive
 525         in
 526         match retained with
 527         | None -> active, passive, new'
 528         | Some (rn, rp) ->
 529             let nn, np = new' in
 530             simplify (nn @ rn, np @ rp) active passive
 531       in
 532       let active, passive, new' = simplify new' active passive in
 533       let _ =
 534         Printf.printf "active:\n%s\n"
 535           (String.concat "\n"
 536              ((List.map
 537                  (fun (s, e) -> (string_of_sign s) ^ " " ^
 538                     (string_of_equality ~env e)) active)));
 539         print_newline ();
 540       in
 541       let _ =
 542         match new' with
 543         | neg, pos ->
 544             Printf.printf "new':\n%s\n"
 545               (String.concat "\n"
 546                  ((List.map
 547                      (fun e -> "Negative " ^
 548                         (string_of_equality ~env e)) neg) @
 549                     (List.map
 550                        (fun e -> "Positive " ^
 551                           (string_of_equality ~env e)) pos)));
 552             print_newline ();
 553       in
 554       match contains_empty env new' with
 555       | false, _ ->
 556           let active =
 557             match sign with
 558             | Negative -> (sign, current)::active
 559             | Positive -> active @ [(sign, current)]
 560           in
 561           let passive = add_to_passive passive new' in
 562           let (_, ns), (_, ps) = passive in
 563           Printf.printf "passive:\n%s\n"
 564             (String.concat "\n"
 565                ((List.map (fun e -> "Negative " ^
 566                              (string_of_equality ~env e))
 567                    (EqualitySet.elements ns)) @
 568                   (List.map (fun e -> "Positive " ^
 569                                (string_of_equality ~env e))
 570                      (EqualitySet.elements ps))));
 571           print_newline ();
 572           given_clause env passive active
 573       | true, proof ->
 574           Success (proof, env)
 575 ;;
 576 *)
 577
 578
 579 let get_from_user () =
 580   let dbd = Mysql.quick_connect
 581     ~host:"localhost" ~user:"helm" ~database:"mowgli" () in
 582   let rec get () =
 583     match read_line () with
 584     | "" -> []
 585     | t -> t::(get ())
 586   in
 587   let term_string = String.concat "\n" (get ()) in
 588   let env, metasenv, term, ugraph =
 589     List.nth (Disambiguate.Trivial.disambiguate_string dbd term_string) 0
 590   in
 591   term, metasenv, ugraph
 592 ;;
 593
 594
 595 let main () =
 596   let module C = Cic in
 597   let module T = CicTypeChecker in
 598   let module PET = ProofEngineTypes in
 599   let module PP = CicPp in
 600   let term, metasenv, ugraph = get_from_user () in
 601   let proof = None, (1, [], term)::metasenv, C.Meta (1, []), term in
 602   let proof, goals =
 603     PET.apply_tactic (PrimitiveTactics.intros_tac ()) (proof, 1) in
 604   let goal = List.nth goals 0 in
 605   let _, metasenv, meta_proof, _ = proof in
 606   let _, context, goal = CicUtil.lookup_meta goal metasenv in
 607   let equalities, maxm = find_equalities context proof in
 608   maxmeta := maxm; (* TODO ugly!! *)
 609   let env = (metasenv, context, ugraph) in
 610   try
 611     let term_equality = equality_of_term meta_proof goal in
 612     let meta_proof, (eq_ty, left, right), _, _ = term_equality in
 613     let active = [] in
 614     let passive = make_passive [term_equality] equalities in
 615     Printf.printf "\ncurrent goal: %s ={%s} %s\n"
 616       (PP.ppterm left) (PP.ppterm eq_ty) (PP.ppterm right);
 617     Printf.printf "\ncontext:\n%s\n" (PP.ppcontext context);
 618     Printf.printf "\nmetasenv:\n%s\n" (print_metasenv metasenv);
 619     Printf.printf "\nequalities:\n";
 620     List.iter
 621       (function (_, (ty, t1, t2), _, _) ->
 622          let w1 = weight_of_term t1 in
 623          let w2 = weight_of_term t2 in
 624          let res = !compare_terms t1 t2 in
 625          Printf.printf "{%s}: %s<%s> %s %s<%s>\n" (PP.ppterm ty)
 626            (PP.ppterm t1) (string_of_weight w1)
 627            (string_of_comparison res)
 628            (PP.ppterm t2) (string_of_weight w2))
 629       equalities;
 630     print_endline "--------------------------------------------------";
 631     let start = Unix.gettimeofday () in
 632     print_endline "GO!";
 633     let res = given_clause env passive active in
 634     let finish = Unix.gettimeofday () in
 635     match res with
 636     | Failure ->
 637         Printf.printf "NO proof found! :-(\n\n"
 638     | Success (Some proof, env) ->
 639         Printf.printf "OK, found a proof!:\n%s\n%.9f\n" (PP.ppterm proof)
 640           (finish -. start);
 641     | Success (None, env) ->
 642         Printf.printf "Success, but no proof?!?\n\n"
 643   with exc ->
 644     print_endline ("EXCEPTION: " ^ (Printexc.to_string exc));
 645 ;;
 646
 647
 648 let configuration_file = ref "../../gTopLevel/gTopLevel.conf.xml";;
 649
 650 let _ =
 651   let set_ratio v = weight_age_ratio := (v+1); weight_age_counter := (v+1)
 652   and set_sel v = symbols_ratio := v; symbols_counter := v;
 653   and set_conf f = configuration_file := f
 654   and set_lpo () = Utils.compare_terms := lpo
 655   and set_kbo () = Utils.compare_terms := nonrec_kbo
 656   in
 657   Arg.parse [
 658     "-r", Arg.Int set_ratio, "Weight-Age equality selection ratio (default: 0)";
 659
 660     "-s", Arg.Int set_sel,
 661     "symbols-based selection ratio (relative to the weight ratio)";
 662
 663     "-c", Arg.String set_conf, "Configuration file (for the db connection)";
 664
 665     "-lpo", Arg.Unit set_lpo, "Use lpo term ordering";
 666
 667     "-kbo", Arg.Unit set_kbo, "Use (non-recursive) kbo term ordering (default)";
 668   ] (fun a -> ()) "Usage:"
 669 in
 670 Helm_registry.load_from !configuration_file;
 671 main ()