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