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