helm/ocaml/paramodulation/saturation.ml

   1 open Inference;;
   2 open Utils;;
   3
   4
   5 (* set to false to disable paramodulation inside auto_tac *)
   6 let connect_to_auto = true;;
   7
   8
   9 (* profiling statistics... *)
  10 let infer_time = ref 0.;;
  11 let forward_simpl_time = ref 0.;;
  12 let forward_simpl_new_time = ref 0.;;
  13 let backward_simpl_time = ref 0.;;
  14 let passive_maintainance_time = ref 0.;;
  15
  16 (* limited-resource-strategy related globals *)
  17 let processed_clauses = ref 0;; (* number of equalities selected so far... *)
  18 let time_limit = ref 0.;; (* in seconds, settable by the user... *)
  19 let start_time = ref 0.;; (* time at which the execution started *)
  20 let elapsed_time = ref 0.;;
  21 (* let maximal_weight = ref None;; *)
  22 let maximal_retained_equality = ref None;;
  23
  24 (* equality-selection related globals *)
  25 let use_fullred = ref true;;
  26 let weight_age_ratio = ref (* 5 *) 3;; (* settable by the user *)
  27 let weight_age_counter = ref !weight_age_ratio;;
  28 let symbols_ratio = ref (* 0 *) 2;;
  29 let symbols_counter = ref 0;;
  30
  31 (* non-recursive Knuth-Bendix term ordering by default *)
  32 Utils.compare_terms := Utils.nonrec_kbo;;
  33
  34 (* statistics... *)
  35 let derived_clauses = ref 0;;
  36 let kept_clauses = ref 0;;
  37
  38 (* index of the greatest Cic.Meta created - TODO: find a better way! *)
  39 let maxmeta = ref 0;;
  40
  41
  42 type result =
  43   | ParamodulationFailure
  44   | ParamodulationSuccess of Inference.equality option * environment
  45 ;;
  46
  47
  48 (*
  49 let symbols_of_equality (_, (_, left, right), _, _) =
  50   TermSet.union (symbols_of_term left) (symbols_of_term right)
  51 ;;
  52 *)
  53
  54 let symbols_of_equality ((_, _, (_, left, right, _), _, _) as equality) =
  55   let m1 = symbols_of_term left in
  56   let m =
  57     TermMap.fold
  58       (fun k v res ->
  59          try
  60            let c = TermMap.find k res in
  61            TermMap.add k (c+v) res
  62          with Not_found ->
  63            TermMap.add k v res)
  64       (symbols_of_term right) m1
  65   in
  66 (*   Printf.printf "symbols_of_equality %s:\n" *)
  67 (*     (string_of_equality equality); *)
  68 (*   TermMap.iter (fun k v -> Printf.printf "%s: %d\n" (CicPp.ppterm k) v) m; *)
  69 (*   print_newline (); *)
  70   m
  71 ;;
  72
  73
  74 module OrderedEquality = struct
  75   type t = Inference.equality
  76
  77   let compare eq1 eq2 =
  78     match meta_convertibility_eq eq1 eq2 with
  79     | true -> 0
  80     | false ->
  81         let w1, _, (ty, left, right, _), _, a = eq1
  82         and w2, _, (ty', left', right', _), _, a' = eq2 in
  83 (*         let weight_of t = fst (weight_of_term ~consider_metas:false t) in *)
  84 (*         let w1 = (weight_of ty) + (weight_of left) + (weight_of right) *)
  85 (*         and w2 = (weight_of ty') + (weight_of left') + (weight_of right') in *)
  86         match Pervasives.compare w1 w2 with
  87         | 0 ->
  88             let res = (List.length a) - (List.length a') in
  89             if res <> 0 then res else (
  90               try
  91                 let res = Pervasives.compare (List.hd a) (List.hd a') in
  92                 if res <> 0 then res else Pervasives.compare eq1 eq2
  93               with Failure "hd" -> Pervasives.compare eq1 eq2
  94 (*               match a, a' with *)
  95 (*               | (Cic.Meta (i, _)::_), (Cic.Meta (j, _)::_) -> *)
  96 (*                   let res = Pervasives.compare i j in *)
  97 (*                   if res <> 0 then res else Pervasives.compare eq1 eq2 *)
  98 (*               | _, _ -> Pervasives.compare eq1 eq2 *)
  99             )
 100         | res -> res
 101 end
 102
 103 module EqualitySet = Set.Make(OrderedEquality);;
 104
 105
 106 let select env passive (active, _) =
 107   processed_clauses := !processed_clauses + 1;
 108
 109   let (neg_list, neg_set), (pos_list, pos_set), passive_table = passive in
 110   let remove eq l =
 111     List.filter (fun e -> e <> eq) l
 112   in
 113   if !weight_age_ratio > 0 then
 114     weight_age_counter := !weight_age_counter - 1;
 115   match !weight_age_counter with
 116   | 0 -> (
 117       weight_age_counter := !weight_age_ratio;
 118       match neg_list, pos_list with
 119       | hd::tl, pos ->
 120           (* Negatives aren't indexed, no need to remove them... *)
 121           (Negative, hd),
 122           ((tl, EqualitySet.remove hd neg_set), (pos, pos_set), passive_table)
 123       | [], hd::tl ->
 124           let passive_table =
 125             Indexing.remove_index passive_table hd
 126 (*             if !use_fullred then Indexing.remove_index passive_table hd *)
 127 (*             else passive_table *)
 128           in
 129           (Positive, hd),
 130           (([], neg_set), (tl, EqualitySet.remove hd pos_set), passive_table)
 131       | _, _ -> assert false
 132     )
 133   | _ when (!symbols_counter > 0) && (EqualitySet.is_empty neg_set) -> (
 134       symbols_counter := !symbols_counter - 1;
 135       let cardinality map =
 136         TermMap.fold (fun k v res -> res + v) map 0
 137       in
 138       match active with
 139       | (Negative, e)::_ ->
 140           let symbols = symbols_of_equality e in
 141           let card = cardinality symbols in
 142           let foldfun k v (r1, r2) =
 143             if TermMap.mem k symbols then
 144               let c = TermMap.find k symbols in
 145               let c1 = abs (c - v) in
 146               let c2 = v - c1 in
 147               r1 + c2, r2 + c1
 148             else
 149               r1, r2 + v
 150           in
 151           let f equality (i, e) =
 152             let common, others =
 153               TermMap.fold foldfun (symbols_of_equality equality) (0, 0)
 154             in
 155             let c = others + (abs (common - card)) in
 156             if c < i then (c, equality)
 157 (*             else if c = i then *)
 158 (*               match OrderedEquality.compare equality e with *)
 159 (*               | -1 -> (c, equality) *)
 160 (*               | res -> (i, e) *)
 161             else (i, e)
 162           in
 163           let e1 = EqualitySet.min_elt pos_set in
 164           let initial =
 165             let common, others =
 166               TermMap.fold foldfun (symbols_of_equality e1) (0, 0)
 167             in
 168             (others + (abs (common - card))), e1
 169           in
 170           let _, current = EqualitySet.fold f pos_set initial in
 171 (*           Printf.printf "\nsymbols-based selection: %s\n\n" *)
 172 (*             (string_of_equality ~env current); *)
 173           let passive_table =
 174             Indexing.remove_index passive_table current
 175 (*             if !use_fullred then Indexing.remove_index passive_table current *)
 176 (*             else passive_table *)
 177           in
 178           (Positive, current),
 179           (([], neg_set),
 180            (remove current pos_list, EqualitySet.remove current pos_set),
 181            passive_table)
 182       | _ ->
 183           let current = EqualitySet.min_elt pos_set in
 184           let passive_table =
 185             Indexing.remove_index passive_table current
 186 (*             if !use_fullred then Indexing.remove_index passive_table current *)
 187 (*             else passive_table *)
 188           in
 189           let passive =
 190             (neg_list, neg_set),
 191             (remove current pos_list, EqualitySet.remove current pos_set),
 192             passive_table
 193           in
 194           (Positive, current), passive
 195     )
 196   | _ ->
 197       symbols_counter := !symbols_ratio;
 198       let set_selection set = EqualitySet.min_elt set in
 199       if EqualitySet.is_empty neg_set then
 200         let current = set_selection pos_set in
 201         let passive =
 202           (neg_list, neg_set),
 203           (remove current pos_list, EqualitySet.remove current pos_set),
 204           Indexing.remove_index passive_table current
 205 (*           if !use_fullred then Indexing.remove_index passive_table current *)
 206 (*           else passive_table *)
 207         in
 208         (Positive, current), passive
 209       else
 210         let current = set_selection neg_set in
 211         let passive =
 212           (remove current neg_list, EqualitySet.remove current neg_set),
 213           (pos_list, pos_set),
 214           passive_table
 215         in
 216         (Negative, current), passive
 217 ;;
 218
 219
 220 let make_passive neg pos =
 221   let set_of equalities =
 222     List.fold_left (fun s e -> EqualitySet.add e s) EqualitySet.empty equalities
 223   in
 224   let table =
 225       List.fold_left (fun tbl e -> Indexing.index tbl e)
 226         (Indexing.empty_table ()) pos
 227 (*     if !use_fullred then *)
 228 (*       List.fold_left (fun tbl e -> Indexing.index tbl e) *)
 229 (*         (Indexing.empty_table ()) pos *)
 230 (*     else *)
 231 (*       Indexing.empty_table () *)
 232   in
 233   (neg, set_of neg),
 234   (pos, set_of pos),
 235   table
 236 ;;
 237
 238
 239 let make_active () =
 240   [], Indexing.empty_table ()
 241 ;;
 242
 243
 244 let add_to_passive passive (new_neg, new_pos) =
 245   let (neg_list, neg_set), (pos_list, pos_set), table = passive in
 246   let ok set equality = not (EqualitySet.mem equality set) in
 247   let neg = List.filter (ok neg_set) new_neg
 248   and pos = List.filter (ok pos_set) new_pos in
 249   let table =
 250       List.fold_left (fun tbl e -> Indexing.index tbl e) table pos
 251 (*     if !use_fullred then *)
 252 (*       List.fold_left (fun tbl e -> Indexing.index tbl e) table pos *)
 253 (*     else *)
 254 (*       table *)
 255   in
 256   let add set equalities =
 257     List.fold_left (fun s e -> EqualitySet.add e s) set equalities
 258   in
 259   (neg @ neg_list, add neg_set neg),
 260   (pos_list @ pos, add pos_set pos),
 261   table
 262 ;;
 263
 264
 265 let passive_is_empty = function
 266   | ([], _), ([], _), _ -> true
 267   | _ -> false
 268 ;;
 269
 270
 271 let size_of_passive ((_, ns), (_, ps), _) =
 272   (EqualitySet.cardinal ns) + (EqualitySet.cardinal ps)
 273 ;;
 274
 275
 276 let size_of_active (active_list, _) =
 277   List.length active_list
 278 ;;
 279
 280
 281 let prune_passive howmany (active, _) passive =
 282   let (nl, ns), (pl, ps), tbl = passive in
 283   let howmany = float_of_int howmany
 284   and ratio = float_of_int !weight_age_ratio in
 285   let in_weight = int_of_float (howmany *. ratio /. (ratio +. 1.))
 286   and in_age = int_of_float (howmany /. (ratio +. 1.)) in
 287   debug_print (Printf.sprintf "in_weight: %d, in_age: %d\n" in_weight in_age);
 288   let symbols, card =
 289     match active with
 290     | (Negative, e)::_ ->
 291         let symbols = symbols_of_equality e in
 292         let card = TermMap.fold (fun k v res -> res + v) symbols 0 in
 293         Some symbols, card
 294     | _ -> None, 0
 295   in
 296   let counter = ref !symbols_ratio in
 297   let rec pickw w ns ps =
 298     if w > 0 then
 299       if not (EqualitySet.is_empty ns) then
 300         let e = EqualitySet.min_elt ns in
 301         let ns', ps = pickw (w-1) (EqualitySet.remove e ns) ps in
 302         EqualitySet.add e ns', ps
 303       else if !counter > 0 then
 304         let _ =
 305           counter := !counter - 1;
 306           if !counter = 0 then counter := !symbols_ratio
 307         in
 308         match symbols with
 309         | None ->
 310             let e = EqualitySet.min_elt ps in
 311             let ns, ps' = pickw (w-1) ns (EqualitySet.remove e ps) in
 312             ns, EqualitySet.add e ps'
 313         | Some symbols ->
 314             let foldfun k v (r1, r2) =
 315               if TermMap.mem k symbols then
 316                 let c = TermMap.find k symbols in
 317                 let c1 = abs (c - v) in
 318                 let c2 = v - c1 in
 319                 r1 + c2, r2 + c1
 320               else
 321                 r1, r2 + v
 322             in
 323             let f equality (i, e) =
 324               let common, others =
 325                 TermMap.fold foldfun (symbols_of_equality equality) (0, 0)
 326               in
 327               let c = others + (abs (common - card)) in
 328               if c < i then (c, equality)
 329               else (i, e)
 330             in
 331             let e1 = EqualitySet.min_elt ps in
 332             let initial =
 333               let common, others =
 334                 TermMap.fold foldfun (symbols_of_equality e1) (0, 0)
 335               in
 336               (others + (abs (common - card))), e1
 337             in
 338             let _, e = EqualitySet.fold f ps initial in
 339             let ns, ps' = pickw (w-1) ns (EqualitySet.remove e ps) in
 340             ns, EqualitySet.add e ps'
 341       else
 342         let e = EqualitySet.min_elt ps in
 343         let ns, ps' = pickw (w-1) ns (EqualitySet.remove e ps) in
 344         ns, EqualitySet.add e ps'
 345     else
 346       EqualitySet.empty, EqualitySet.empty
 347   in
 348 (*   let in_weight, ns = pickw in_weight ns in *)
 349 (*   let _, ps = pickw in_weight ps in *)
 350   let ns, ps = pickw in_weight ns ps in
 351   let rec picka w s l =
 352     if w > 0 then
 353       match l with
 354       | [] -> w, s, []
 355       | hd::tl when not (EqualitySet.mem hd s) ->
 356           let w, s, l = picka (w-1) s tl in
 357           w, EqualitySet.add hd s, hd::l
 358       | hd::tl ->
 359           let w, s, l = picka w s tl in
 360           w, s, hd::l
 361     else
 362       0, s, l
 363   in
 364   let in_age, ns, nl = picka in_age ns nl in
 365   let _, ps, pl = picka in_age ps pl in
 366   if not (EqualitySet.is_empty ps) then
 367 (*     maximal_weight := Some (weight_of_equality (EqualitySet.max_elt ps)); *)
 368     maximal_retained_equality := Some (EqualitySet.max_elt ps);
 369   let tbl =
 370     EqualitySet.fold
 371       (fun e tbl -> Indexing.index tbl e) ps (Indexing.empty_table ())
 372 (*     if !use_fullred then *)
 373 (*       EqualitySet.fold *)
 374 (*         (fun e tbl -> Indexing.index tbl e) ps (Indexing.empty_table ()) *)
 375 (*     else *)
 376 (*       tbl *)
 377   in
 378   (nl, ns), (pl, ps), tbl
 379 ;;
 380
 381
 382 let infer env sign current (active_list, active_table) =
 383   let new_neg, new_pos =
 384     match sign with
 385     | Negative ->
 386         let maxm, res =
 387           Indexing.superposition_left !maxmeta env active_table current in
 388         maxmeta := maxm;
 389         res, []
 390     | Positive ->
 391         let maxm, res =
 392           Indexing.superposition_right !maxmeta env active_table current in
 393         maxmeta := maxm;
 394         let rec infer_positive table = function
 395           | [] -> [], []
 396           | (Negative, equality)::tl ->
 397               let maxm, res =
 398                 Indexing.superposition_left !maxmeta env table equality in
 399               maxmeta := maxm;
 400               let neg, pos = infer_positive table tl in
 401               res @ neg, pos
 402           | (Positive, equality)::tl ->
 403               let maxm, res =
 404                 Indexing.superposition_right !maxmeta env table equality in
 405               maxmeta := maxm;
 406               let neg, pos = infer_positive table tl in
 407               neg, res @ pos
 408         in
 409         let curr_table = Indexing.index (Indexing.empty_table ()) current in
 410         let neg, pos = infer_positive curr_table active_list in
 411         neg, res @ pos
 412   in
 413   derived_clauses := !derived_clauses + (List.length new_neg) +
 414     (List.length new_pos);
 415   match (* !maximal_weight *)!maximal_retained_equality with
 416   | None -> new_neg, new_pos
 417   | Some (* w *) eq ->
 418       let new_pos =
 419         List.filter (fun e -> (* (weight_of_equality e) <= w *) OrderedEquality.compare e eq <= 0) new_pos in
 420       new_neg, new_pos
 421 ;;
 422
 423
 424 let contains_empty env (negative, positive) =
 425   let metasenv, context, ugraph = env in
 426   try
 427     let found =
 428       List.find
 429         (fun (w, proof, (ty, left, right, ordering), m, a) ->
 430            fst (CicReduction.are_convertible context left right ugraph))
 431         negative
 432     in
 433     true, Some found
 434   with Not_found ->
 435     false, None
 436 ;;
 437
 438
 439 let forward_simplify env (sign, current) ?passive (active_list, active_table) =
 440   let pl, passive_table =
 441     match passive with
 442     | None -> [], None
 443     | Some ((pn, _), (pp, _), pt) ->
 444         let pn = List.map (fun e -> (Negative, e)) pn
 445         and pp = List.map (fun e -> (Positive, e)) pp in
 446         pn @ pp, Some pt
 447   in
 448   let all = if pl = [] then active_list else active_list @ pl in
 449
 450 (*   let rec find_duplicate sign current = function *)
 451 (*     | [] -> false *)
 452 (*     | (s, eq)::tl when s = sign -> *)
 453 (*         if meta_convertibility_eq current eq then true *)
 454 (*         else find_duplicate sign current tl *)
 455 (*     | _::tl -> find_duplicate sign current tl *)
 456 (*   in *)
 457
 458 (*   let res =  *)
 459 (*     if sign = Positive then *)
 460 (*       Indexing.subsumption env active_table current *)
 461 (*     else *)
 462 (*       false *)
 463 (*   in *)
 464 (*   if res then *)
 465 (*     None *)
 466 (*   else *)
 467
 468   let demodulate table current =
 469     let newmeta, newcurrent =
 470       Indexing.demodulation !maxmeta env table sign current in
 471     maxmeta := newmeta;
 472     if is_identity env newcurrent then
 473       if sign = Negative then Some (sign, newcurrent)
 474       else None
 475     else
 476       Some (sign, newcurrent)
 477   in
 478   let res =
 479     let res = demodulate active_table current in
 480     match res with
 481     | None -> None
 482     | Some (sign, newcurrent) ->
 483         match passive_table with
 484         | None -> res
 485         | Some passive_table -> demodulate passive_table newcurrent
 486   in
 487   match res with
 488   | None -> None
 489   | Some (Negative, c) ->
 490       let ok = not (
 491         List.exists
 492           (fun (s, eq) -> s = Negative && meta_convertibility_eq eq c)
 493           all)
 494       in
 495       if ok then res else None
 496   | Some (Positive, c) ->
 497       if Indexing.in_index active_table c then
 498         None
 499       else
 500         match passive_table with
 501         | None -> res
 502         | Some passive_table ->
 503             if Indexing.in_index passive_table c then None
 504             else res
 505
 506 (*   | Some (s, c) -> if find_duplicate s c all then None else res *)
 507
 508 (*         if s = Utils.Negative then *)
 509 (*           res *)
 510 (*         else *)
 511 (*           if Indexing.subsumption env active_table c then *)
 512 (*             None *)
 513 (*           else ( *)
 514 (*             match passive_table with *)
 515 (*             | None -> res *)
 516 (*             | Some passive_table -> *)
 517 (*                 if Indexing.subsumption env passive_table c then *)
 518 (*                   None *)
 519 (*                 else *)
 520 (*                   res *)
 521 (*           ) *)
 522
 523 (*         let pred (sign, eq) = *)
 524 (*           if sign <> s then false *)
 525 (*           else subsumption env c eq *)
 526 (*         in *)
 527 (*         if List.exists pred all then None *)
 528 (*         else res *)
 529 ;;
 530
 531 type fs_time_info_t = {
 532   mutable build_all: float;
 533   mutable demodulate: float;
 534   mutable subsumption: float;
 535 };;
 536
 537 let fs_time_info = { build_all = 0.; demodulate = 0.; subsumption = 0. };;
 538
 539
 540 let forward_simplify_new env (new_neg, new_pos) ?passive active =
 541   let t1 = Unix.gettimeofday () in
 542
 543   let active_list, active_table = active in
 544   let pl, passive_table =
 545     match passive with
 546     | None -> [], None
 547     | Some ((pn, _), (pp, _), pt) ->
 548         let pn = List.map (fun e -> (Negative, e)) pn
 549         and pp = List.map (fun e -> (Positive, e)) pp in
 550         pn @ pp, Some pt
 551   in
 552   let all = active_list @ pl in
 553
 554   let t2 = Unix.gettimeofday () in
 555   fs_time_info.build_all <- fs_time_info.build_all +. (t2 -. t1);
 556
 557   let demodulate sign table target =
 558     let newmeta, newtarget =
 559       Indexing.demodulation !maxmeta env table sign target in
 560     maxmeta := newmeta;
 561     newtarget
 562   in
 563 (*   let f sign' target (sign, eq) = *)
 564 (*     if sign <> sign' then false *)
 565 (*     else subsumption env target eq  *)
 566 (*   in *)
 567
 568   let t1 = Unix.gettimeofday () in
 569
 570   let new_neg, new_pos =
 571     let new_neg = List.map (demodulate Negative active_table) new_neg
 572     and new_pos = List.map (demodulate Positive active_table) new_pos in
 573     match passive_table with
 574     | None -> new_neg, new_pos
 575     | Some passive_table ->
 576         List.map (demodulate Negative passive_table) new_neg,
 577         List.map (demodulate Positive passive_table) new_pos
 578   in
 579
 580   let t2 = Unix.gettimeofday () in
 581   fs_time_info.demodulate <- fs_time_info.demodulate +. (t2 -. t1);
 582
 583   let new_pos_set =
 584     List.fold_left
 585       (fun s e ->
 586          if not (Inference.is_identity env e) then
 587            if EqualitySet.mem e s then s
 588            else EqualitySet.add e s
 589          else s)
 590       EqualitySet.empty new_pos
 591   in
 592   let new_pos = EqualitySet.elements new_pos_set in
 593
 594   let subs =
 595     match passive_table with
 596     | None ->
 597         (fun e -> not (Indexing.subsumption env active_table e))
 598     | Some passive_table ->
 599         (fun e -> not ((Indexing.subsumption env active_table e) ||
 600                          (Indexing.subsumption env passive_table e)))
 601   in
 602
 603   let t1 = Unix.gettimeofday () in
 604
 605 (*   let new_neg, new_pos = *)
 606 (*     List.filter subs new_neg, *)
 607 (*     List.filter subs new_pos *)
 608 (*   in *)
 609
 610 (*   let new_neg, new_pos =  *)
 611 (*     (List.filter (fun e -> not (List.exists (f Negative e) all)) new_neg, *)
 612 (*      List.filter (fun e -> not (List.exists (f Positive e) all)) new_pos) *)
 613 (*   in *)
 614
 615   let t2 = Unix.gettimeofday () in
 616   fs_time_info.subsumption <- fs_time_info.subsumption +. (t2 -. t1);
 617
 618   let is_duplicate =
 619     match passive_table with
 620     | None ->
 621         (fun e -> not (Indexing.in_index active_table e))
 622     | Some passive_table ->
 623         (fun e ->
 624            not ((Indexing.in_index active_table e) ||
 625                   (Indexing.in_index passive_table e)))
 626   in
 627   new_neg, List.filter is_duplicate new_pos
 628
 629 (*   new_neg, new_pos *)
 630
 631 (*   let res = *)
 632 (*     (List.filter (fun e -> not (List.exists (f Negative e) all)) new_neg, *)
 633 (*      List.filter (fun e -> not (List.exists (f Positive e) all)) new_pos) *)
 634 (*   in *)
 635 (*   res *)
 636 ;;
 637
 638
 639 let backward_simplify_active env new_pos new_table min_weight active =
 640   let active_list, active_table = active in
 641   let active_list, newa =
 642     List.fold_right
 643       (fun (s, equality) (res, newn) ->
 644          let ew, _, _, _, _ = equality in
 645          if ew < min_weight then
 646            (s, equality)::res, newn
 647          else
 648            match forward_simplify env (s, equality) (new_pos, new_table) with
 649            | None -> res, newn
 650            | Some (s, e) ->
 651                if equality = e then
 652                  (s, e)::res, newn
 653                else
 654                  res, (s, e)::newn)
 655       active_list ([], [])
 656   in
 657   let find eq1 where =
 658     List.exists (fun (s, e) -> meta_convertibility_eq eq1 e) where
 659   in
 660   let active, newa =
 661     List.fold_right
 662       (fun (s, eq) (res, tbl) ->
 663          if List.mem (s, eq) res then
 664            res, tbl
 665          else if (is_identity env eq) || (find eq res) then (
 666            res, tbl
 667          ) (* else if (find eq res) then *)
 668 (*            res, tbl *)
 669          else
 670            (s, eq)::res, if s = Negative then tbl else Indexing.index tbl eq)
 671       active_list ([], Indexing.empty_table ()),
 672     List.fold_right
 673       (fun (s, eq) (n, p) ->
 674          if (s <> Negative) && (is_identity env eq) then (
 675            (n, p)
 676          ) else
 677            if s = Negative then eq::n, p
 678            else n, eq::p)
 679       newa ([], [])
 680   in
 681   match newa with
 682   | [], [] -> active, None
 683   | _ -> active, Some newa
 684 ;;
 685
 686
 687 let backward_simplify_passive env new_pos new_table min_weight passive =
 688   let (nl, ns), (pl, ps), passive_table = passive in
 689   let f sign equality (resl, ress, newn) =
 690     let ew, _, _, _, _ = equality in
 691     if ew < min_weight then
 692 (*       let _ = debug_print (Printf.sprintf "OK: %d %d" ew min_weight) in *)
 693       equality::resl, ress, newn
 694     else
 695       match forward_simplify env (sign, equality) (new_pos, new_table) with
 696       | None -> resl, EqualitySet.remove equality ress, newn
 697       | Some (s, e) ->
 698           if equality = e then
 699             equality::resl, ress, newn
 700           else
 701             let ress = EqualitySet.remove equality ress in
 702             resl, ress, e::newn
 703   in
 704   let nl, ns, newn = List.fold_right (f Negative) nl ([], ns, [])
 705   and pl, ps, newp = List.fold_right (f Positive) pl ([], ps, []) in
 706   let passive_table =
 707     List.fold_left
 708       (fun tbl e -> Indexing.index tbl e) (Indexing.empty_table ()) pl
 709   in
 710   match newn, newp with
 711   | [], [] -> ((nl, ns), (pl, ps), passive_table), None
 712   | _, _ -> ((nl, ns), (pl, ps), passive_table), Some (newn, newp)
 713 ;;
 714
 715
 716 let backward_simplify env new' ?passive active =
 717   let new_pos, new_table, min_weight =
 718     List.fold_left
 719       (fun (l, t, w) e ->
 720          let ew, _, _, _, _ = e in
 721          (Positive, e)::l, Indexing.index t e, min ew w)
 722       ([], Indexing.empty_table (), 1000000) (snd new')
 723   in
 724   let active, newa =
 725     backward_simplify_active env new_pos new_table min_weight active in
 726   match passive with
 727   | None ->
 728       active, (make_passive [] []), newa, None
 729   | Some passive ->
 730       let passive, newp =
 731         backward_simplify_passive env new_pos new_table min_weight passive in
 732       active, passive, newa, newp
 733 ;;
 734
 735
 736 let get_selection_estimate () =
 737   elapsed_time := (Unix.gettimeofday ()) -. !start_time;
 738 (*   !processed_clauses * (int_of_float (!time_limit /. !elapsed_time)) *)
 739   int_of_float (
 740     ceil ((float_of_int !processed_clauses) *.
 741             ((!time_limit (* *. 2. *)) /. !elapsed_time -. 1.)))
 742 ;;
 743
 744
 745 let rec given_clause env passive active =
 746   let time1 = Unix.gettimeofday () in
 747
 748   let selection_estimate = get_selection_estimate () in
 749   let kept = size_of_passive passive in
 750   let passive =
 751     if !time_limit = 0. || !processed_clauses = 0 then
 752       passive
 753     else if !elapsed_time > !time_limit then (
 754       debug_print (Printf.sprintf "Time limit (%.2f) reached: %.2f\n"
 755                      !time_limit !elapsed_time);
 756       make_passive [] []
 757     ) else if kept > selection_estimate then (
 758       debug_print (Printf.sprintf ("Too many passive equalities: pruning..." ^^
 759                                      "(kept: %d, selection_estimate: %d)\n")
 760                      kept selection_estimate);
 761       prune_passive selection_estimate active passive
 762     ) else
 763       passive
 764   in
 765
 766   let time2 = Unix.gettimeofday () in
 767   passive_maintainance_time := !passive_maintainance_time +. (time2 -. time1);
 768
 769   kept_clauses := (size_of_passive passive) + (size_of_active active);
 770
 771   match passive_is_empty passive with
 772   | true -> ParamodulationFailure
 773   | false ->
 774       let (sign, current), passive = select env passive active in
 775       let time1 = Unix.gettimeofday () in
 776       let res = forward_simplify env (sign, current) ~passive active in
 777       let time2 = Unix.gettimeofday () in
 778       forward_simpl_time := !forward_simpl_time +. (time2 -. time1);
 779       match res with
 780       | None ->
 781           given_clause env passive active
 782       | Some (sign, current) ->
 783           if (sign = Negative) && (is_identity env current) then (
 784             debug_print (Printf.sprintf "OK!!! %s %s" (string_of_sign sign)
 785                            (string_of_equality ~env current));
 786             ParamodulationSuccess (Some current, env)
 787           ) else (
 788             debug_print "\n================================================";
 789             debug_print (Printf.sprintf "selected: %s %s"
 790                            (string_of_sign sign)
 791                            (string_of_equality ~env current));
 792
 793             let t1 = Unix.gettimeofday () in
 794             let new' = infer env sign current active in
 795             let t2 = Unix.gettimeofday () in
 796             infer_time := !infer_time +. (t2 -. t1);
 797
 798             let res, goal = contains_empty env new' in
 799             if res then
 800               ParamodulationSuccess (goal, env)
 801             else
 802               let t1 = Unix.gettimeofday () in
 803               let new' = forward_simplify_new env new' (* ~passive *) active in
 804               let t2 = Unix.gettimeofday () in
 805               let _ =
 806                 forward_simpl_new_time := !forward_simpl_new_time +. (t2 -. t1)
 807               in
 808               let active =
 809                 match sign with
 810                 | Negative -> active
 811                 | Positive ->
 812                     let t1 = Unix.gettimeofday () in
 813                     let active, _, newa, _ =
 814                       backward_simplify env ([], [current]) active
 815                     in
 816                     let t2 = Unix.gettimeofday () in
 817                     backward_simpl_time := !backward_simpl_time +. (t2 -. t1);
 818                     match newa with
 819                     | None -> active
 820                     | Some (n, p) ->
 821                         let al, tbl = active in
 822                         let nn = List.map (fun e -> Negative, e) n in
 823                         let pp, tbl =
 824                           List.fold_right
 825                             (fun e (l, t) ->
 826                                (Positive, e)::l,
 827                                Indexing.index tbl e)
 828                             p ([], tbl)
 829                         in
 830                         nn @ al @ pp, tbl
 831               in
 832 (*               let _ = *)
 833 (*                 Printf.printf "active:\n%s\n" *)
 834 (*                   (String.concat "\n" *)
 835 (*                      ((List.map *)
 836 (*                          (fun (s, e) -> (string_of_sign s) ^ " " ^ *)
 837 (*                             (string_of_equality ~env e)) (fst active)))); *)
 838 (*                 print_newline (); *)
 839 (*               in *)
 840 (*               let _ = *)
 841 (*                 match new' with *)
 842 (*                 | neg, pos -> *)
 843 (*                     Printf.printf "new':\n%s\n" *)
 844 (*                       (String.concat "\n" *)
 845 (*                          ((List.map *)
 846 (*                              (fun e -> "Negative " ^ *)
 847 (*                                 (string_of_equality ~env e)) neg) @ *)
 848 (*                             (List.map *)
 849 (*                                (fun e -> "Positive " ^ *)
 850 (*                                   (string_of_equality ~env e)) pos))); *)
 851 (*                     print_newline (); *)
 852 (*               in *)
 853               match contains_empty env new' with
 854               | false, _ ->
 855                   let active =
 856                     let al, tbl = active in
 857                     match sign with
 858                     | Negative -> (sign, current)::al, tbl
 859                     | Positive ->
 860                         al @ [(sign, current)], Indexing.index tbl current
 861                   in
 862                   let passive = add_to_passive passive new' in
 863                   let (_, ns), (_, ps), _ = passive in
 864 (*                   Printf.printf "passive:\n%s\n" *)
 865 (*                     (String.concat "\n" *)
 866 (*                        ((List.map (fun e -> "Negative " ^ *)
 867 (*                                      (string_of_equality ~env e)) *)
 868 (*                            (EqualitySet.elements ns)) @ *)
 869 (*                           (List.map (fun e -> "Positive " ^ *)
 870 (*                                        (string_of_equality ~env e)) *)
 871 (*                              (EqualitySet.elements ps)))); *)
 872 (*                   print_newline (); *)
 873                   given_clause env passive active
 874               | true, goal ->
 875                   ParamodulationSuccess (goal, env)
 876           )
 877 ;;
 878
 879
 880 let rec given_clause_fullred env passive active =
 881   let time1 = Unix.gettimeofday () in
 882
 883   let selection_estimate = get_selection_estimate () in
 884   let kept = size_of_passive passive in
 885   let passive =
 886     if !time_limit = 0. || !processed_clauses = 0 then
 887       passive
 888     else if !elapsed_time > !time_limit then (
 889       debug_print (Printf.sprintf "Time limit (%.2f) reached: %.2f\n"
 890                      !time_limit !elapsed_time);
 891       make_passive [] []
 892     ) else if kept > selection_estimate then (
 893       debug_print (Printf.sprintf ("Too many passive equalities: pruning..." ^^
 894                                      "(kept: %d, selection_estimate: %d)\n")
 895                      kept selection_estimate);
 896       prune_passive selection_estimate active passive
 897     ) else
 898       passive
 899   in
 900
 901   let time2 = Unix.gettimeofday () in
 902   passive_maintainance_time := !passive_maintainance_time +. (time2 -. time1);
 903
 904   kept_clauses := (size_of_passive passive) + (size_of_active active);
 905
 906   match passive_is_empty passive with
 907   | true -> ParamodulationFailure
 908   | false ->
 909       let (sign, current), passive = select env passive active in
 910       let time1 = Unix.gettimeofday () in
 911       let res = forward_simplify env (sign, current) ~passive active in
 912       let time2 = Unix.gettimeofday () in
 913       forward_simpl_time := !forward_simpl_time +. (time2 -. time1);
 914       match res with
 915       | None ->
 916           given_clause_fullred env passive active
 917       | Some (sign, current) ->
 918           if (sign = Negative) && (is_identity env current) then (
 919             debug_print (Printf.sprintf "OK!!! %s %s" (string_of_sign sign)
 920                            (string_of_equality ~env current));
 921             ParamodulationSuccess (Some current, env)
 922           ) else (
 923             debug_print "\n================================================";
 924             debug_print (Printf.sprintf "selected: %s %s"
 925                            (string_of_sign sign)
 926                            (string_of_equality ~env current));
 927
 928             let t1 = Unix.gettimeofday () in
 929             let new' = infer env sign current active in
 930             let t2 = Unix.gettimeofday () in
 931             infer_time := !infer_time +. (t2 -. t1);
 932
 933             let active =
 934               if is_identity env current then active
 935               else
 936                 let al, tbl = active in
 937                 match sign with
 938                 | Negative -> (sign, current)::al, tbl
 939                 | Positive -> al @ [(sign, current)], Indexing.index tbl current
 940             in
 941             let rec simplify new' active passive =
 942               let t1 = Unix.gettimeofday () in
 943               let new' = forward_simplify_new env new' ~passive active in
 944               let t2 = Unix.gettimeofday () in
 945               forward_simpl_new_time := !forward_simpl_new_time +. (t2 -. t1);
 946               let t1 = Unix.gettimeofday () in
 947               let active, passive, newa, retained =
 948                 backward_simplify env new' ~passive active in
 949               let t2 = Unix.gettimeofday () in
 950               backward_simpl_time := !backward_simpl_time +. (t2 -. t1);
 951               match newa, retained with
 952               | None, None -> active, passive, new'
 953               | Some (n, p), None
 954               | None, Some (n, p) ->
 955                   let nn, np = new' in
 956                   simplify (nn @ n, np @ p) active passive
 957               | Some (n, p), Some (rn, rp) ->
 958                   let nn, np = new' in
 959                   simplify (nn @ n @ rn, np @ p @ rp) active passive
 960             in
 961             let active, passive, new' = simplify new' active passive in
 962
 963             let k = size_of_passive passive in
 964             if k < (kept - 1) then
 965               processed_clauses := !processed_clauses + (kept - 1 - k);
 966
 967             let _ =
 968               debug_print (
 969                 Printf.sprintf "active:\n%s\n"
 970                   (String.concat "\n"
 971                      ((List.map
 972                          (fun (s, e) -> (string_of_sign s) ^ " " ^
 973                             (string_of_equality ~env e)) (fst active)))))
 974             in
 975             let _ =
 976               match new' with
 977               | neg, pos ->
 978                   debug_print (
 979                     Printf.sprintf "new':\n%s\n"
 980                       (String.concat "\n"
 981                          ((List.map
 982                              (fun e -> "Negative " ^
 983                                 (string_of_equality ~env e)) neg) @
 984                             (List.map
 985                                (fun e -> "Positive " ^
 986                                   (string_of_equality ~env e)) pos))))
 987             in
 988             match contains_empty env new' with
 989             | false, _ ->
 990                 let passive = add_to_passive passive new' in
 991 (*                 let (_, ns), (_, ps), _ = passive in *)
 992 (*                 Printf.printf "passive:\n%s\n" *)
 993 (*                   (String.concat "\n" *)
 994 (*                      ((List.map (fun e -> "Negative " ^ *)
 995 (*                                    (string_of_equality ~env e)) *)
 996 (*                          (EqualitySet.elements ns)) @ *)
 997 (*                         (List.map (fun e -> "Positive " ^ *)
 998 (*                                      (string_of_equality ~env e)) *)
 999 (*                            (EqualitySet.elements ps)))); *)
1000 (*                 print_newline (); *)
1001                 given_clause_fullred env passive active
1002             | true, goal ->
1003                 ParamodulationSuccess (goal, env)
1004           )
1005 ;;
1006
1007
1008 let given_clause_ref = ref given_clause;;
1009
1010
1011 let main dbd term metasenv ugraph =
1012   let module C = Cic in
1013   let module T = CicTypeChecker in
1014   let module PET = ProofEngineTypes in
1015   let module PP = CicPp in
1016   let proof = None, (1, [], term)::metasenv, C.Meta (1, []), term in
1017   let status = PET.apply_tactic (PrimitiveTactics.intros_tac ()) (proof, 1) in
1018   let proof, goals = status in
1019   let goal' = List.nth goals 0 in
1020   let _, metasenv, meta_proof, _ = proof in
1021   let _, context, goal = CicUtil.lookup_meta goal' metasenv in
1022   let equalities, maxm = find_equalities context proof in
1023   let library_equalities, maxm =
1024     find_library_equalities ~dbd context (proof, goal') (maxm+2)
1025   in
1026   maxmeta := maxm+2; (* TODO ugly!! *)
1027   let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
1028   let new_meta_goal, metasenv, type_of_goal =
1029     let _, context, ty = CicUtil.lookup_meta goal' metasenv in
1030     Printf.printf "\n\nTIPO DEL GOAL: %s\n" (CicPp.ppterm ty);
1031     print_newline ();
1032     Cic.Meta (maxm+1, irl),
1033     (maxm+1, context, ty)::metasenv,
1034     ty
1035   in
1036 (*   let new_meta_goal = Cic.Meta (goal', irl) in *)
1037   let env = (metasenv, context, ugraph) in
1038   try
1039     let term_equality = equality_of_term new_meta_goal goal in
1040     let _, meta_proof, (eq_ty, left, right, ordering), _, _ = term_equality in
1041     if is_identity env term_equality then
1042       let proof =
1043         Cic.Appl [Cic.MutConstruct (* reflexivity *)
1044                     (HelmLibraryObjects.Logic.eq_URI, 0, 1, []);
1045                   eq_ty; left]
1046       in
1047       let _ =
1048         Printf.printf "OK, found a proof!\n";
1049         let names = names_of_context context in
1050         print_endline (PP.pp proof names)
1051       in
1052       ()
1053     else
1054       let equalities =
1055         let equalities = equalities @ library_equalities in
1056         debug_print (
1057           Printf.sprintf "equalities:\n%s\n"
1058             (String.concat "\n"
1059                (List.map string_of_equality equalities)));
1060         debug_print "SIMPLYFYING EQUALITIES...";
1061         let rec simpl e others others_simpl =
1062           let active = others @ others_simpl in
1063           let tbl =
1064             List.fold_left
1065               (fun t (_, e) -> Indexing.index t e)
1066               (Indexing.empty_table ()) active
1067           in
1068           let res = forward_simplify env e (active, tbl) in
1069           match others with
1070           | hd::tl -> (
1071               match res with
1072               | None -> simpl hd tl others_simpl
1073               | Some e -> simpl hd tl (e::others_simpl)
1074             )
1075           | [] -> (
1076               match res with
1077               | None -> others_simpl
1078               | Some e -> e::others_simpl
1079             )
1080         in
1081         match equalities with
1082         | [] -> []
1083         | hd::tl ->
1084             let others = List.map (fun e -> (Positive, e)) tl in
1085             let res =
1086               List.rev (List.map snd (simpl (Positive, hd) others []))
1087             in
1088             debug_print (
1089               Printf.sprintf "equalities AFTER:\n%s\n"
1090                 (String.concat "\n"
1091                    (List.map string_of_equality res)));
1092             res
1093       in
1094       let active = make_active () in
1095       let passive = make_passive [term_equality] equalities in
1096       Printf.printf "\ncurrent goal: %s\n"
1097         (string_of_equality ~env term_equality);
1098       Printf.printf "\ncontext:\n%s\n" (PP.ppcontext context);
1099       Printf.printf "\nmetasenv:\n%s\n" (print_metasenv metasenv);
1100       Printf.printf "\nequalities:\n%s\n"
1101         (String.concat "\n"
1102            (List.map
1103               (string_of_equality ~env)
1104               (equalities @ library_equalities)));
1105       print_endline "--------------------------------------------------";
1106       let start = Unix.gettimeofday () in
1107       print_endline "GO!";
1108       start_time := Unix.gettimeofday ();
1109       let res =
1110         (if !use_fullred then given_clause_fullred else given_clause)
1111           env passive active
1112       in
1113       let finish = Unix.gettimeofday () in
1114       let _ =
1115         match res with
1116         | ParamodulationFailure ->
1117             Printf.printf "NO proof found! :-(\n\n"
1118         | ParamodulationSuccess (Some goal, env) ->
1119             let proof = Inference.build_proof_term goal in
1120             let newmetasenv =
1121               List.fold_left
1122                 (fun m (_, _, _, menv, _) -> m @ menv) metasenv equalities
1123             in
1124             let _ =
1125               try
1126                 let ty, ug =
1127                   CicTypeChecker.type_of_aux' newmetasenv context proof ugraph
1128                 in
1129                 Printf.printf "OK, found a proof!\n";
1130                 (* REMEMBER: we have to instantiate meta_proof, we should use
1131                    apply  the "apply" tactic to proof and status
1132                 *)
1133                 let names = names_of_context context in
1134                 print_endline (PP.pp proof names);
1135                 (*           print_endline (PP.ppterm proof); *)
1136
1137                 print_endline (string_of_float (finish -. start));
1138                 Printf.printf
1139                   "\nGOAL was: %s\nPROOF has type: %s\nconvertible?: %s\n\n"
1140                   (CicPp.pp type_of_goal names) (CicPp.pp ty names)
1141                   (string_of_bool
1142                      (fst (CicReduction.are_convertible
1143                              context type_of_goal ty ug)));
1144               with e ->
1145                 Printf.printf "\nEXCEPTION!!! %s\n" (Printexc.to_string e);
1146                 Printf.printf "MAXMETA USED: %d\n" !maxmeta;
1147                 print_endline (string_of_float (finish -. start));
1148             in
1149             ()
1150
1151         | ParamodulationSuccess (None, env) ->
1152             Printf.printf "Success, but no proof?!?\n\n"
1153       in
1154       Printf.printf ("infer_time: %.9f\nforward_simpl_time: %.9f\n" ^^
1155                        "forward_simpl_new_time: %.9f\n" ^^
1156                        "backward_simpl_time: %.9f\n")
1157         !infer_time !forward_simpl_time !forward_simpl_new_time
1158         !backward_simpl_time;
1159       Printf.printf "passive_maintainance_time: %.9f\n"
1160         !passive_maintainance_time;
1161       Printf.printf "    successful unification/matching time: %.9f\n"
1162         !Indexing.match_unif_time_ok;
1163       Printf.printf "    failed unification/matching time: %.9f\n"
1164         !Indexing.match_unif_time_no;
1165       Printf.printf "    indexing retrieval time: %.9f\n"
1166         !Indexing.indexing_retrieval_time;
1167       Printf.printf "    demodulate_term.build_newtarget_time: %.9f\n"
1168         !Indexing.build_newtarget_time;
1169       Printf.printf "derived %d clauses, kept %d clauses.\n"
1170         !derived_clauses !kept_clauses;
1171   with exc ->
1172     print_endline ("EXCEPTION: " ^ (Printexc.to_string exc));
1173     raise exc
1174 ;;
1175
1176
1177 let saturate dbd (proof, goal) =
1178   let module C = Cic in
1179   maxmeta := 0;
1180   let goal' = goal in
1181   let uri, metasenv, meta_proof, term_to_prove = proof in
1182   let _, context, goal = CicUtil.lookup_meta goal' metasenv in
1183   let equalities, maxm = find_equalities context proof in
1184   let new_meta_goal, metasenv, type_of_goal =
1185     let irl =
1186       CicMkImplicit.identity_relocation_list_for_metavariable context in
1187     let _, context, ty = CicUtil.lookup_meta goal' metasenv in
1188     debug_print (Printf.sprintf "\n\nTIPO DEL GOAL: %s\n" (CicPp.ppterm ty));
1189     Cic.Meta (maxm+1, irl),
1190     (maxm+1, context, ty)::metasenv,
1191     ty
1192   in
1193   let ugraph = CicUniv.empty_ugraph in
1194   let env = (metasenv, context, ugraph) in
1195 (*   try *)
1196   let term_equality = equality_of_term new_meta_goal goal in
1197   let res, time =
1198     if is_identity env term_equality then
1199       let w, _, (eq_ty, left, right, o), m, a = term_equality in
1200       let proof =
1201         Cic.Appl [Cic.MutConstruct (* reflexivity *)
1202                     (HelmLibraryObjects.Logic.eq_URI, 0, 1, []);
1203                   eq_ty; left]
1204       in
1205       (ParamodulationSuccess
1206          (Some (0, Inference.BasicProof proof,
1207                 (eq_ty, left, right, o), m, a), env), 0.)
1208     else
1209       let library_equalities, maxm =
1210         find_library_equalities ~dbd context (proof, goal') (maxm+2)
1211       in
1212       maxmeta := maxm+2;
1213       let equalities =
1214         let equalities = equalities @ library_equalities in
1215         debug_print (
1216           Printf.sprintf "equalities:\n%s\n"
1217             (String.concat "\n"
1218                (List.map string_of_equality equalities)));
1219         debug_print "SIMPLYFYING EQUALITIES...";
1220         let rec simpl e others others_simpl =
1221           let active = others @ others_simpl in
1222           let tbl =
1223             List.fold_left
1224               (fun t (_, e) -> Indexing.index t e)
1225               (Indexing.empty_table ()) active
1226           in
1227           let res = forward_simplify env e (active, tbl) in
1228           match others with
1229           | hd::tl -> (
1230               match res with
1231               | None -> simpl hd tl others_simpl
1232               | Some e -> simpl hd tl (e::others_simpl)
1233             )
1234           | [] -> (
1235               match res with
1236               | None -> others_simpl
1237               | Some e -> e::others_simpl
1238             )
1239         in
1240         match equalities with
1241         | [] -> []
1242         | hd::tl ->
1243             let others = List.map (fun e -> (Positive, e)) tl in
1244             let res =
1245               List.rev (List.map snd (simpl (Positive, hd) others []))
1246             in
1247             debug_print (
1248               Printf.sprintf "equalities AFTER:\n%s\n"
1249                 (String.concat "\n"
1250                    (List.map string_of_equality res)));
1251             res
1252       in
1253       let active = make_active () in
1254       let passive = make_passive [term_equality] equalities in
1255       let start = Unix.gettimeofday () in
1256       let res = given_clause_fullred env passive active in
1257       let finish = Unix.gettimeofday () in
1258       (res, finish -. start)
1259   in
1260   match res with
1261   | ParamodulationSuccess (Some goal, env) ->
1262       debug_print "OK, found a proof!";
1263       let proof = Inference.build_proof_term goal in
1264       let names = names_of_context context in
1265       let newmetasenv =
1266         let i1 =
1267           match new_meta_goal with
1268           | C.Meta (i, _) -> i | _ -> assert false
1269         in
1270 (*           let i2 = *)
1271 (*             match meta_proof with *)
1272 (*             | C.Meta (i, _) -> i *)
1273 (*             | t -> *)
1274 (*                 Printf.printf "\nHMMM!!! meta_proof: %s\ngoal': %s" *)
1275 (*                   (CicPp.pp meta_proof names) (string_of_int goal'); *)
1276 (*                 print_newline (); *)
1277 (*                 assert false *)
1278 (*           in *)
1279         List.filter (fun (i, _, _) -> i <> i1 && i <> goal') metasenv
1280       in
1281       let newstatus =
1282         try
1283           let ty, ug =
1284             CicTypeChecker.type_of_aux' newmetasenv context proof ugraph
1285           in
1286           debug_print (CicPp.pp proof [](* names *));
1287           debug_print
1288             (Printf.sprintf
1289                "\nGOAL was: %s\nPROOF has type: %s\nconvertible?: %s\n"
1290                (CicPp.pp type_of_goal names) (CicPp.pp ty names)
1291                (string_of_bool
1292                   (fst (CicReduction.are_convertible
1293                           context type_of_goal ty ug))));
1294           let equality_for_replace i t1 =
1295             match t1 with
1296             | C.Meta (n, _) -> n = i
1297             | _ -> false
1298           in
1299           let real_proof =
1300             ProofEngineReduction.replace
1301               ~equality:equality_for_replace
1302               ~what:[goal'] ~with_what:[proof]
1303               ~where:meta_proof
1304           in
1305           debug_print (
1306             Printf.sprintf "status:\n%s\n%s\n%s\n%s\n"
1307               (match uri with Some uri -> UriManager.string_of_uri uri
1308                | None -> "")
1309               (print_metasenv newmetasenv)
1310               (CicPp.pp real_proof [](* names *))
1311               (CicPp.pp term_to_prove names));
1312           ((uri, newmetasenv, real_proof, term_to_prove), [])
1313         with CicTypeChecker.TypeCheckerFailure _ ->
1314           debug_print "THE PROOF DOESN'T TYPECHECK!!!";
1315           debug_print (CicPp.pp proof names);
1316           raise (ProofEngineTypes.Fail
1317                    "Found a proof, but it doesn't typecheck")
1318       in
1319       debug_print (Printf.sprintf "\nTIME NEEDED: %.9f" time);
1320       newstatus
1321   | _ ->
1322       raise (ProofEngineTypes.Fail "NO proof found")
1323 (*   with e -> *)
1324 (*     raise (Failure "saturation failed") *)
1325 ;;
1326
1327
1328 (* dummy function called within matita to trigger linkage *)
1329 let init () = ();;
1330
1331
1332 (* UGLY SIDE EFFECT... *)
1333 if connect_to_auto then (
1334   AutoTactic.paramodulation_tactic := saturate;
1335   AutoTactic.term_is_equality := Inference.term_is_equality;
1336 );;