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 (sign, current) ?passive active =
 248   let pn, pp =
 249     match passive with
 250     | None -> [], []
 251     | Some ((pn, _), (pp, _)) ->
 252         (List.map (fun e -> Negative, e) pn),
 253         (List.map (fun e -> Positive, e) pp)
 254   in
 255   let all = active @ pn @ pp in
 256   let rec find_duplicate sign current = function
 257     | [] -> false
 258     | (s, eq)::tl when s = sign ->
 259         if meta_convertibility_eq current eq then true
 260         else find_duplicate sign current tl
 261     | _::tl -> find_duplicate sign current tl
 262   in
 263 (*   let duplicate = find_duplicate sign current all in *)
 264 (*   if duplicate then *)
 265 (*     None *)
 266 (*   else *)
 267   let rec aux env (sign, current) = function
 268     | [] -> Some (sign, current)
 269     | (Negative, _)::tl -> aux env (sign, current) tl
 270     | (Positive, equality)::tl ->
 271         let newmeta, newcurrent =
 272           demodulation !maxmeta env current equality in
 273         maxmeta := newmeta;
 274         if is_identity env newcurrent then
 275           if sign = Negative then
 276             Some (sign, current)
 277           else
 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   let res = aux env (sign, current) all in
 285   match res with
 286   | None -> None
 287   | Some (s, c) ->
 288       if find_duplicate s c all then
 289         None
 290       else
 291         let pred (sign, eq) =
 292           if sign <> s then false
 293           else subsumption env c eq
 294         in
 295         if List.exists pred all then None
 296         else res
 297 ;;
 298
 299
 300 let forward_simplify_new env (new_neg, new_pos) ?passive active =
 301   let pn, pp =
 302     match passive with
 303     | None -> [], []
 304     | Some ((pn, _), (pp, _)) ->
 305         (List.map (fun e -> Negative, e) pn),
 306         (List.map (fun e -> Positive, e) pp)
 307   in
 308   let all = active @ pn @ pp in
 309   let remove_identities equalities =
 310     let ok eq = not (is_identity env eq) in
 311     List.filter ok equalities
 312   in
 313   let rec simpl all' target =
 314     match all' with
 315     | [] -> target
 316     | (Negative, _)::tl -> simpl tl target
 317     | (Positive, source)::tl ->
 318         let newmeta, newtarget = demodulation !maxmeta env target source in
 319         maxmeta := newmeta;
 320         if is_identity env newtarget then newtarget
 321         else if newtarget <> target then (
 322 (*           Printf.printf "OK:\n%s\n%s\n" *)
 323 (*             (string_of_equality ~env target) *)
 324 (*             (string_of_equality ~env newtarget); *)
 325 (*           print_newline (); *)
 326           simpl all newtarget
 327         )
 328         else simpl tl newtarget
 329   in
 330   let new_neg = List.map (simpl all) new_neg
 331   and new_pos = remove_identities (List.map (simpl all) new_pos) in
 332   let new_pos_set =
 333     List.fold_left (fun s e -> EqualitySet.add e s) EqualitySet.empty new_pos
 334   in
 335   let new_pos = EqualitySet.elements new_pos_set in
 336   let f sign' target (sign, eq) =
 337 (*     Printf.printf "f %s <%s> (%s, <%s>)\n" *)
 338 (*       (string_of_sign sign') (string_of_equality ~env target) *)
 339 (*       (string_of_sign sign) (string_of_equality ~env eq); *)
 340     if sign <> sign' then false
 341     else subsumption env target eq
 342   in
 343 (*   new_neg, new_pos *)
 344   (List.filter (fun e -> not (List.exists (f Negative e) all)) new_neg,
 345    List.filter (fun e -> not (List.exists (f Positive e) all)) new_pos)
 346 ;;
 347
 348
 349 let backward_simplify_active env (new_neg, new_pos) active =
 350   let new_pos = List.map (fun e -> Positive, e) new_pos in
 351   let active, newa =
 352     List.fold_right
 353       (fun (s, equality) (res, newn) ->
 354          match forward_simplify env (s, equality) new_pos with
 355          | None when s = Negative ->
 356              Printf.printf "\nECCO QUI: %s\n"
 357                (string_of_equality ~env equality);
 358              print_newline ();
 359              res, newn
 360          | None -> res, newn
 361          | Some (s, e) ->
 362              if equality = e then
 363                (s, e)::res, newn
 364              else
 365                res, (s, e)::newn)
 366       active ([], [])
 367   in
 368   let find eq1 where =
 369     List.exists (fun (s, e) -> meta_convertibility_eq eq1 e) where
 370   in
 371   let active, newa =
 372     let f (s, eq) res =
 373       if (is_identity env eq) || (find eq res) then res else (s, eq)::res
 374     in
 375     List.fold_right
 376       (fun (s, eq) res ->
 377          if (is_identity env eq) || (find eq res) then res else (s, eq)::res)
 378       active [],
 379     List.fold_right
 380       (fun (s, eq) (n, p) ->
 381          if (s <> Negative) && (is_identity env eq) then
 382            (n, p)
 383          else
 384            if s = Negative then eq::n, p
 385            else n, eq::p)
 386       newa ([], [])
 387   in
 388   match newa with
 389   | [], [] -> active, None
 390   | _ -> active, Some newa
 391 ;;
 392
 393
 394 let backward_simplify_passive env (new_neg, new_pos) passive =
 395   let new_pos = List.map (fun e -> Positive, e) new_pos in
 396   let (nl, ns), (pl, ps) = passive in
 397   let f sign equality (resl, ress, newn) =
 398     match forward_simplify env (sign, equality) new_pos with
 399     | None -> resl, EqualitySet.remove equality ress, newn
 400     | Some (s, e) ->
 401         if equality = e then
 402           equality::resl, ress, newn
 403         else
 404           let ress = EqualitySet.remove equality ress in
 405           resl, ress, e::newn
 406   in
 407   let nl, ns, newn = List.fold_right (f Negative) nl ([], ns, [])
 408   and pl, ps, newp = List.fold_right (f Positive) pl ([], ps, []) in
 409   match newn, newp with
 410   | [], [] -> ((nl, ns), (pl, ps)), None
 411   | _, _ -> ((nl, ns), (pl, ps)), Some (newn, newp)
 412 ;;
 413
 414
 415 let backward_simplify env new' ?passive active =
 416   let active, newa = backward_simplify_active env new' active in
 417   match passive with
 418   | None ->
 419       active, (([], EqualitySet.empty), ([], EqualitySet.empty)), newa, None
 420   | Some passive ->
 421       let passive, newp =
 422         backward_simplify_passive env new' passive in
 423       active, passive, newa, newp
 424 ;;
 425
 426
 427
 428 let rec given_clause env passive active =
 429   match passive_is_empty passive with
 430   | true -> Failure
 431   | false ->
 432 (*       Printf.printf "before select\n"; *)
 433       let (sign, current), passive = select env passive active in
 434 (*       Printf.printf "before simplification: sign: %s\ncurrent: %s\n\n" *)
 435 (*         (string_of_sign sign) (string_of_equality ~env current); *)
 436       match forward_simplify env (sign, current) ~passive active with
 437 (*       | None when sign = Negative -> *)
 438 (*           Printf.printf "OK!!! %s %s" (string_of_sign sign) *)
 439 (*             (string_of_equality ~env current); *)
 440 (*           print_newline (); *)
 441 (*           let proof, _, _, _ = current in *)
 442 (*           Success (Some proof, env) *)
 443       | None ->
 444 (*           Printf.printf "avanti... %s %s" (string_of_sign sign) *)
 445 (*             (string_of_equality ~env current); *)
 446 (*           print_newline (); *)
 447           given_clause env passive active
 448       | Some (sign, current) ->
 449           if (sign = Negative) && (is_identity env current) then (
 450             Printf.printf "OK!!! %s %s" (string_of_sign sign)
 451               (string_of_equality ~env current);
 452             print_newline ();
 453             let proof, _, _, _ = current in
 454             Success (Some proof, env)
 455           ) else (
 456             print_endline "\n================================================";
 457             Printf.printf "selected: %s %s"
 458               (string_of_sign sign) (string_of_equality ~env current);
 459             print_newline ();
 460
 461             let new' = infer env sign current active in
 462             let res, proof = contains_empty env new' in
 463             if res then
 464               Success (proof, env)
 465             else
 466               let new' = forward_simplify_new env new' active in
 467               let active =
 468                 match sign with
 469                 | Negative -> active
 470                 | Positive ->
 471                     let active, _, newa, _ =
 472                       backward_simplify env ([], [current]) active
 473                     in
 474                     match newa with
 475                     | None -> active
 476                     | Some (n, p) ->
 477                         let nn = List.map (fun e -> Negative, e) n
 478                         and pp = List.map (fun e -> Positive, e) p in
 479                         nn @ active @ pp
 480               in
 481               let _ =
 482                 Printf.printf "active:\n%s\n"
 483                   (String.concat "\n"
 484                      ((List.map
 485                          (fun (s, e) -> (string_of_sign s) ^ " " ^
 486                             (string_of_equality ~env e)) active)));
 487                 print_newline ();
 488               in
 489               let _ =
 490                 match new' with
 491                 | neg, pos ->
 492                     Printf.printf "new':\n%s\n"
 493                       (String.concat "\n"
 494                          ((List.map
 495                              (fun e -> "Negative " ^
 496                                 (string_of_equality ~env e)) neg) @
 497                             (List.map
 498                                (fun e -> "Positive " ^
 499                                   (string_of_equality ~env e)) pos)));
 500                     print_newline ();
 501               in
 502               match contains_empty env new' with
 503               | false, _ ->
 504                   let active =
 505                     match sign with
 506                     | Negative -> (sign, current)::active
 507                     | Positive -> active @ [(sign, current)]
 508                   in
 509                   let passive = add_to_passive passive new' in
 510                   let (_, ns), (_, ps) = passive in
 511                   Printf.printf "passive:\n%s\n"
 512                     (String.concat "\n"
 513                        ((List.map (fun e -> "Negative " ^
 514                                      (string_of_equality ~env e))
 515                            (EqualitySet.elements ns)) @
 516                           (List.map (fun e -> "Positive " ^
 517                                        (string_of_equality ~env e))
 518                              (EqualitySet.elements ps))));
 519                   print_newline ();
 520                   given_clause env passive active
 521               | true, proof ->
 522                   Success (proof, env)
 523           )
 524 ;;
 525
 526
 527 let rec given_clause_fullred env passive active =
 528   match passive_is_empty passive with
 529   | true -> Failure
 530   | false ->
 531 (*       Printf.printf "before select\n"; *)
 532       let (sign, current), passive = select env passive active in
 533 (*       Printf.printf "before simplification: sign: %s\ncurrent: %s\n\n" *)
 534 (*         (string_of_sign sign) (string_of_equality ~env current); *)
 535       match forward_simplify env (sign, current) ~passive active with
 536       | None ->
 537           given_clause_fullred env passive active
 538       | Some (sign, current) ->
 539           if (sign = Negative) && (is_identity env current) then (
 540             Printf.printf "OK!!! %s %s" (string_of_sign sign)
 541               (string_of_equality ~env current);
 542             print_newline ();
 543             let proof, _, _, _ = current in
 544             Success (Some proof, env)
 545           ) else (
 546             print_endline "\n================================================";
 547             Printf.printf "selected: %s %s"
 548               (string_of_sign sign) (string_of_equality ~env current);
 549             print_newline ();
 550
 551             let new' = infer env sign current active in
 552
 553             let active =
 554               if is_identity env current then active
 555               else
 556                 match sign with
 557                 | Negative -> (sign, current)::active
 558                 | Positive -> active @ [(sign, current)]
 559             in
 560 (*             let _ = *)
 561 (*               match new' with *)
 562 (*               | neg, pos -> *)
 563 (*                   Printf.printf "new' before simpl:\n%s\n" *)
 564 (*                     (String.concat "\n" *)
 565 (*                        ((List.map *)
 566 (*                            (fun e -> "Negative " ^ *)
 567 (*                               (string_of_equality ~env e)) neg) @ *)
 568 (*                           (List.map *)
 569 (*                              (fun e -> "Positive " ^ *)
 570 (*                                 (string_of_equality ~env e)) pos))); *)
 571 (*                   print_newline (); *)
 572 (*             in *)
 573             let rec simplify new' active passive =
 574               let new' = forward_simplify_new env new' ~passive active in
 575               let active, passive, newa, retained =
 576                 backward_simplify env new' ~passive active
 577               in
 578               match newa, retained with
 579               | None, None -> active, passive, new'
 580               | Some (n, p), None
 581               | None, Some (n, p) ->
 582                   let nn, np = new' in
 583                   simplify (nn @ n, np @ p) active passive
 584               | Some (n, p), Some (rn, rp) ->
 585                   let nn, np = new' in
 586                   simplify (nn @ n @ rn, np @ p @ rp) active passive
 587             in
 588             let active, passive, new' = simplify new' active passive in
 589             let _ =
 590               Printf.printf "active:\n%s\n"
 591                 (String.concat "\n"
 592                    ((List.map
 593                        (fun (s, e) -> (string_of_sign s) ^ " " ^
 594                           (string_of_equality ~env e)) active)));
 595               print_newline ();
 596             in
 597             let _ =
 598               match new' with
 599               | neg, pos ->
 600                   Printf.printf "new':\n%s\n"
 601                     (String.concat "\n"
 602                        ((List.map
 603                            (fun e -> "Negative " ^
 604                               (string_of_equality ~env e)) neg) @
 605                           (List.map
 606                              (fun e -> "Positive " ^
 607                                 (string_of_equality ~env e)) pos)));
 608                   print_newline ();
 609             in
 610             match contains_empty env new' with
 611             | false, _ ->
 612                 let passive = add_to_passive passive new' in
 613 (*                 let (_, ns), (_, ps) = passive in *)
 614 (*                 Printf.printf "passive:\n%s\n" *)
 615 (*                   (String.concat "\n" *)
 616 (*                      ((List.map (fun e -> "Negative " ^ *)
 617 (*                                    (string_of_equality ~env e)) *)
 618 (*                          (EqualitySet.elements ns)) @ *)
 619 (*                         (List.map (fun e -> "Positive " ^ *)
 620 (*                                      (string_of_equality ~env e)) *)
 621 (*                            (EqualitySet.elements ps)))); *)
 622 (*                 print_newline (); *)
 623                 given_clause_fullred env passive active
 624             | true, proof ->
 625                 Success (proof, env)
 626           )
 627 ;;
 628
 629
 630 let get_from_user () =
 631   let dbd = Mysql.quick_connect
 632     ~host:"localhost" ~user:"helm" ~database:"mowgli" () in
 633   let rec get () =
 634     match read_line () with
 635     | "" -> []
 636     | t -> t::(get ())
 637   in
 638   let term_string = String.concat "\n" (get ()) in
 639   let env, metasenv, term, ugraph =
 640     List.nth (Disambiguate.Trivial.disambiguate_string dbd term_string) 0
 641   in
 642   term, metasenv, ugraph
 643 ;;
 644
 645
 646 let given_clause_ref = ref given_clause;;
 647
 648
 649 let main () =
 650   let module C = Cic in
 651   let module T = CicTypeChecker in
 652   let module PET = ProofEngineTypes in
 653   let module PP = CicPp in
 654   let term, metasenv, ugraph = get_from_user () in
 655   let proof = None, (1, [], term)::metasenv, C.Meta (1, []), term in
 656   let proof, goals =
 657     PET.apply_tactic (PrimitiveTactics.intros_tac ()) (proof, 1) in
 658   let goal = List.nth goals 0 in
 659   let _, metasenv, meta_proof, _ = proof in
 660   let _, context, goal = CicUtil.lookup_meta goal metasenv in
 661   let equalities, maxm = find_equalities context proof in
 662   maxmeta := maxm; (* TODO ugly!! *)
 663   let env = (metasenv, context, ugraph) in
 664   try
 665     let term_equality = equality_of_term meta_proof goal in
 666     let meta_proof, (eq_ty, left, right), _, _ = term_equality in
 667     let active = [] in
 668     let passive = make_passive [term_equality] equalities in
 669     Printf.printf "\ncurrent goal: %s ={%s} %s\n"
 670       (PP.ppterm left) (PP.ppterm eq_ty) (PP.ppterm right);
 671     Printf.printf "\ncontext:\n%s\n" (PP.ppcontext context);
 672     Printf.printf "\nmetasenv:\n%s\n" (print_metasenv metasenv);
 673     Printf.printf "\nequalities:\n";
 674     List.iter
 675       (function (_, (ty, t1, t2), _, _) ->
 676          let w1 = weight_of_term t1 in
 677          let w2 = weight_of_term t2 in
 678          let res = !compare_terms t1 t2 in
 679          Printf.printf "{%s}: %s<%s> %s %s<%s>\n" (PP.ppterm ty)
 680            (PP.ppterm t1) (string_of_weight w1)
 681            (string_of_comparison res)
 682            (PP.ppterm t2) (string_of_weight w2))
 683       equalities;
 684     print_endline "--------------------------------------------------";
 685     let start = Unix.gettimeofday () in
 686     print_endline "GO!";
 687     let res = !given_clause_ref env passive active in
 688     let finish = Unix.gettimeofday () in
 689     match res with
 690     | Failure ->
 691         Printf.printf "NO proof found! :-(\n\n"
 692     | Success (Some proof, env) ->
 693         Printf.printf "OK, found a proof!:\n%s\n%.9f\n" (PP.ppterm proof)
 694           (finish -. start);
 695     | Success (None, env) ->
 696         Printf.printf "Success, but no proof?!?\n\n"
 697   with exc ->
 698     print_endline ("EXCEPTION: " ^ (Printexc.to_string exc));
 699 ;;
 700
 701
 702 let configuration_file = ref "../../gTopLevel/gTopLevel.conf.xml";;
 703
 704 let _ =
 705   let set_ratio v = weight_age_ratio := (v+1); weight_age_counter := (v+1)
 706   and set_sel v = symbols_ratio := v; symbols_counter := v;
 707   and set_conf f = configuration_file := f
 708   and set_lpo () = Utils.compare_terms := lpo
 709   and set_kbo () = Utils.compare_terms := nonrec_kbo
 710   and set_fullred () = given_clause_ref := given_clause_fullred
 711   in
 712   Arg.parse [
 713     "-f", Arg.Unit set_fullred, "Use full-reduction strategy";
 714
 715     "-r", Arg.Int set_ratio, "Weight-Age equality selection ratio (default: 0)";
 716
 717     "-s", Arg.Int set_sel,
 718     "symbols-based selection ratio (relative to the weight ratio)";
 719
 720     "-c", Arg.String set_conf, "Configuration file (for the db connection)";
 721
 722     "-lpo", Arg.Unit set_lpo, "Use lpo term ordering";
 723
 724     "-kbo", Arg.Unit set_kbo, "Use (non-recursive) kbo term ordering (default)";
 725   ] (fun a -> ()) "Usage:"
 726 in
 727 Helm_registry.load_from !configuration_file;
 728 main ()