helm/ocaml/tactics/paramodulation/saturation.ml

   1 (* Copyright (C) 2005, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://cs.unibo.it/helm/.
  24  *)
  25
  26 (* $Id$ *)
  27
  28 open Inference;;
  29 open Utils;;
  30
  31
  32 (* set to false to disable paramodulation inside auto_tac *)
  33 let connect_to_auto = true;;
  34
  35
  36 (* profiling statistics... *)
  37 let infer_time = ref 0.;;
  38 let forward_simpl_time = ref 0.;;
  39 let forward_simpl_new_time = ref 0.;;
  40 let backward_simpl_time = ref 0.;;
  41 let passive_maintainance_time = ref 0.;;
  42
  43 (* limited-resource-strategy related globals *)
  44 let processed_clauses = ref 0;; (* number of equalities selected so far... *)
  45 let time_limit = ref 0.;; (* in seconds, settable by the user... *)
  46 let start_time = ref 0.;; (* time at which the execution started *)
  47 let elapsed_time = ref 0.;;
  48 (* let maximal_weight = ref None;; *)
  49 let maximal_retained_equality = ref None;;
  50
  51 (* equality-selection related globals *)
  52 let use_fullred = ref true;;
  53 let weight_age_ratio = ref (* 5 *) 4;; (* settable by the user *)
  54 let weight_age_counter = ref !weight_age_ratio;;
  55 let symbols_ratio = ref (* 0 *) 3;;
  56 let symbols_counter = ref 0;;
  57
  58 (* non-recursive Knuth-Bendix term ordering by default *)
  59 (* Utils.compare_terms := Utils.rpo;; *)
  60 (* Utils.compare_terms := Utils.nonrec_kbo;; *)
  61 (* Utils.compare_terms := Utils.ao;; *)
  62
  63 (* statistics... *)
  64 let derived_clauses = ref 0;;
  65 let kept_clauses = ref 0;;
  66
  67 (* index of the greatest Cic.Meta created - TODO: find a better way! *)
  68 let maxmeta = ref 0;;
  69
  70 (* varbiables controlling the search-space *)
  71 let maxdepth = ref 3;;
  72 let maxwidth = ref 3;;
  73
  74
  75 type result =
  76   | ParamodulationFailure
  77   | ParamodulationSuccess of Inference.proof option * environment
  78 ;;
  79
  80 type goal = proof * Cic.metasenv * Cic.term;;
  81
  82 type theorem = Cic.term * Cic.term * Cic.metasenv;;
  83
  84 let symbols_of_equality (_, _, (_, left, right, _), _, _) =
  85   let m1 = symbols_of_term left in
  86   let m =
  87     TermMap.fold
  88       (fun k v res ->
  89          try
  90            let c = TermMap.find k res in
  91            TermMap.add k (c+v) res
  92          with Not_found ->
  93            TermMap.add k v res)
  94       (symbols_of_term right) m1
  95   in
  96   m
  97 ;;
  98
  99 module OrderedEquality = struct
 100   type t = Inference.equality
 101
 102   let compare eq1 eq2 =
 103     match meta_convertibility_eq eq1 eq2 with
 104     | true -> 0
 105     | false ->
 106         let w1, _, (ty, left, right, _), _, a = eq1
 107         and w2, _, (ty', left', right', _), _, a' = eq2 in
 108         match Pervasives.compare w1 w2 with
 109         | 0 ->
 110             let res = (List.length a) - (List.length a') in
 111             if res <> 0 then res else (
 112               try
 113                 let res = Pervasives.compare (List.hd a) (List.hd a') in
 114                 if res <> 0 then res else Pervasives.compare eq1 eq2
 115               with Failure "hd" -> Pervasives.compare eq1 eq2
 116             )
 117         | res -> res
 118 end
 119
 120 module EqualitySet = Set.Make(OrderedEquality);;
 121
 122
 123 (**
 124    selects one equality from passive. The selection strategy is a combination
 125    of weight, age and goal-similarity
 126 *)
 127 let select env goals passive (active, _) =
 128   processed_clauses := !processed_clauses + 1;
 129   let goal =
 130     match (List.rev goals) with (_, goal::_)::_ -> goal | _ -> assert false
 131   in
 132   let (neg_list, neg_set), (pos_list, pos_set), passive_table = passive in
 133   let remove eq l =
 134     List.filter (fun e -> e <> eq) l
 135   in
 136   if !weight_age_ratio > 0 then
 137     weight_age_counter := !weight_age_counter - 1;
 138   match !weight_age_counter with
 139   | 0 -> (
 140       weight_age_counter := !weight_age_ratio;
 141       match neg_list, pos_list with
 142       | hd::tl, pos ->
 143           (* Negatives aren't indexed, no need to remove them... *)
 144           (Negative, hd),
 145           ((tl, EqualitySet.remove hd neg_set), (pos, pos_set), passive_table)
 146       | [], (hd:EqualitySet.elt)::tl ->
 147           let passive_table =
 148             Indexing.remove_index passive_table hd
 149           in
 150           (Positive, hd),
 151           (([], neg_set), (tl, EqualitySet.remove hd pos_set), passive_table)
 152       | _, _ -> assert false
 153     )
 154   | _ when (!symbols_counter > 0) && (EqualitySet.is_empty neg_set) -> (
 155       symbols_counter := !symbols_counter - 1;
 156       let cardinality map =
 157         TermMap.fold (fun k v res -> res + v) map 0
 158       in
 159       let symbols =
 160         let _, _, term = goal in
 161         symbols_of_term term
 162       in
 163       let card = cardinality symbols in
 164       let foldfun k v (r1, r2) =
 165         if TermMap.mem k symbols then
 166           let c = TermMap.find k symbols in
 167           let c1 = abs (c - v) in
 168           let c2 = v - c1 in
 169           r1 + c2, r2 + c1
 170         else
 171           r1, r2 + v
 172       in
 173       let f equality (i, e) =
 174         let common, others =
 175           TermMap.fold foldfun (symbols_of_equality equality) (0, 0)
 176         in
 177         let c = others + (abs (common - card)) in
 178         if c < i then (c, equality)
 179         else (i, e)
 180       in
 181       let e1 = EqualitySet.min_elt pos_set in
 182       let initial =
 183         let common, others =
 184           TermMap.fold foldfun (symbols_of_equality e1) (0, 0)
 185         in
 186         (others + (abs (common - card))), e1
 187       in
 188       let _, current = EqualitySet.fold f pos_set initial in
 189       let passive_table =
 190         Indexing.remove_index passive_table current
 191       in
 192       (Positive, current),
 193       (([], neg_set),
 194        (remove current pos_list, EqualitySet.remove current pos_set),
 195        passive_table)
 196     )
 197   | _ ->
 198       symbols_counter := !symbols_ratio;
 199       let set_selection set = EqualitySet.min_elt set in
 200       if EqualitySet.is_empty neg_set then
 201         let current = set_selection pos_set in
 202         let passive =
 203           (neg_list, neg_set),
 204           (remove current pos_list, EqualitySet.remove current pos_set),
 205           Indexing.remove_index passive_table current
 206         in
 207         (Positive, current), passive
 208       else
 209         let current = set_selection neg_set in
 210         let passive =
 211           (remove current neg_list, EqualitySet.remove current neg_set),
 212           (pos_list, pos_set),
 213           passive_table
 214         in
 215         (Negative, current), passive
 216 ;;
 217
 218
 219 (* initializes the passive set of equalities *)
 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) Indexing.empty pos
 226   in
 227   (neg, set_of neg),
 228   (pos, set_of pos),
 229   table
 230 ;;
 231
 232
 233 let make_active () =
 234   [], Indexing.empty
 235 ;;
 236
 237
 238 (* adds to passive a list of equalities: new_neg is a list of negative
 239    equalities, new_pos a list of positive equalities *)
 240 let add_to_passive passive (new_neg, new_pos) =
 241   let (neg_list, neg_set), (pos_list, pos_set), table = passive in
 242   let ok set equality = not (EqualitySet.mem equality set) in
 243   let neg = List.filter (ok neg_set) new_neg
 244   and pos = List.filter (ok pos_set) new_pos in
 245   let table =
 246     List.fold_left (fun tbl e -> Indexing.index tbl e) table pos
 247   in
 248   let add set equalities =
 249     List.fold_left (fun s e -> EqualitySet.add e s) set equalities
 250   in
 251   (neg @ neg_list, add neg_set neg),
 252   (pos_list @ pos, add pos_set pos),
 253   table
 254 ;;
 255
 256
 257 let passive_is_empty = function
 258   | ([], _), ([], _), _ -> true
 259   | _ -> false
 260 ;;
 261
 262
 263 let size_of_passive ((_, ns), (_, ps), _) =
 264   (EqualitySet.cardinal ns) + (EqualitySet.cardinal ps)
 265 ;;
 266
 267
 268 let size_of_active (active_list, _) =
 269   List.length active_list
 270 ;;
 271
 272
 273 (* removes from passive equalities that are estimated impossible to activate
 274    within the current time limit *)
 275 let prune_passive howmany (active, _) passive =
 276   let (nl, ns), (pl, ps), tbl = passive in
 277   let howmany = float_of_int howmany
 278   and ratio = float_of_int !weight_age_ratio in
 279   let round v =
 280     let t = ceil v in
 281     int_of_float (if t -. v < 0.5 then t else v)
 282   in
 283   let in_weight = round (howmany *. ratio /. (ratio +. 1.))
 284   and in_age = round (howmany /. (ratio +. 1.)) in
 285   debug_print
 286     (lazy (Printf.sprintf "in_weight: %d, in_age: %d\n" in_weight in_age));
 287   let symbols, card =
 288     match active with
 289     | (Negative, e)::_ ->
 290         let symbols = symbols_of_equality e in
 291         let card = TermMap.fold (fun k v res -> res + v) symbols 0 in
 292         Some symbols, card
 293     | _ -> None, 0
 294   in
 295   let counter = ref !symbols_ratio in
 296   let rec pickw w ns ps =
 297     if w > 0 then
 298       if not (EqualitySet.is_empty ns) then
 299         let e = EqualitySet.min_elt ns in
 300         let ns', ps = pickw (w-1) (EqualitySet.remove e ns) ps in
 301         EqualitySet.add e ns', ps
 302       else if !counter > 0 then
 303         let _ =
 304           counter := !counter - 1;
 305           if !counter = 0 then counter := !symbols_ratio
 306         in
 307         match symbols with
 308         | None ->
 309             let e = EqualitySet.min_elt ps in
 310             let ns, ps' = pickw (w-1) ns (EqualitySet.remove e ps) in
 311             ns, EqualitySet.add e ps'
 312         | Some symbols ->
 313             let foldfun k v (r1, r2) =
 314               if TermMap.mem k symbols then
 315                 let c = TermMap.find k symbols in
 316                 let c1 = abs (c - v) in
 317                 let c2 = v - c1 in
 318                 r1 + c2, r2 + c1
 319               else
 320                 r1, r2 + v
 321             in
 322             let f equality (i, e) =
 323               let common, others =
 324                 TermMap.fold foldfun (symbols_of_equality equality) (0, 0)
 325               in
 326               let c = others + (abs (common - card)) in
 327               if c < i then (c, equality)
 328               else (i, e)
 329             in
 330             let e1 = EqualitySet.min_elt ps in
 331             let initial =
 332               let common, others =
 333                 TermMap.fold foldfun (symbols_of_equality e1) (0, 0)
 334               in
 335               (others + (abs (common - card))), e1
 336             in
 337             let _, e = EqualitySet.fold f ps initial in
 338             let ns, ps' = pickw (w-1) ns (EqualitySet.remove e ps) in
 339             ns, EqualitySet.add e ps'
 340       else
 341         let e = EqualitySet.min_elt ps in
 342         let ns, ps' = pickw (w-1) ns (EqualitySet.remove e ps) in
 343         ns, EqualitySet.add e ps'
 344     else
 345       EqualitySet.empty, EqualitySet.empty
 346   in
 347   let ns, ps = pickw in_weight ns ps in
 348   let rec picka w s l =
 349     if w > 0 then
 350       match l with
 351       | [] -> w, s, []
 352       | hd::tl when not (EqualitySet.mem hd s) ->
 353           let w, s, l = picka (w-1) s tl in
 354           w, EqualitySet.add hd s, hd::l
 355       | hd::tl ->
 356           let w, s, l = picka w s tl in
 357           w, s, hd::l
 358     else
 359       0, s, l
 360   in
 361   let in_age, ns, nl = picka in_age ns nl in
 362   let _, ps, pl = picka in_age ps pl in
 363   if not (EqualitySet.is_empty ps) then
 364     maximal_retained_equality := Some (EqualitySet.max_elt ps);
 365   let tbl =
 366     EqualitySet.fold
 367       (fun e tbl -> Indexing.index tbl e) ps Indexing.empty
 368   in
 369   (nl, ns), (pl, ps), tbl
 370 ;;
 371
 372
 373 (** inference of new equalities between current and some in active *)
 374 let infer env sign current (active_list, active_table) =
 375   let new_neg, new_pos =
 376     match sign with
 377     | Negative ->
 378         let maxm, res =
 379           Indexing.superposition_left !maxmeta env active_table current in
 380         maxmeta := maxm;
 381         res, []
 382     | Positive ->
 383         let maxm, res =
 384           Indexing.superposition_right !maxmeta env active_table current in
 385         maxmeta := maxm;
 386         let rec infer_positive table = function
 387           | [] -> [], []
 388           | (Negative, equality)::tl ->
 389               let maxm, res =
 390                 Indexing.superposition_left !maxmeta env table equality in
 391               maxmeta := maxm;
 392               let neg, pos = infer_positive table tl in
 393               res @ neg, pos
 394           | (Positive, equality)::tl ->
 395               let maxm, res =
 396                 Indexing.superposition_right !maxmeta env table equality in
 397               maxmeta := maxm;
 398               let neg, pos = infer_positive table tl in
 399               neg, res @ pos
 400         in
 401         let curr_table = Indexing.index Indexing.empty current in
 402         let neg, pos = infer_positive curr_table active_list in
 403         neg, res @ pos
 404   in
 405   derived_clauses := !derived_clauses + (List.length new_neg) +
 406     (List.length new_pos);
 407   match !maximal_retained_equality with
 408   | None -> new_neg, new_pos
 409   | Some eq ->
 410       (* if we have a maximal_retained_equality, we can discard all equalities
 411          "greater" than it, as they will never be reached...  An equality is
 412          greater than maximal_retained_equality if it is bigger
 413          wrt. OrderedEquality.compare and it is less similar than
 414          maximal_retained_equality to the current goal *)
 415       let symbols, card =
 416         match active_list with
 417         | (Negative, e)::_ ->
 418             let symbols = symbols_of_equality e in
 419             let card = TermMap.fold (fun k v res -> res + v) symbols 0 in
 420             Some symbols, card
 421         | _ -> None, 0
 422       in
 423       let new_pos =
 424         match symbols with
 425         | None ->
 426             List.filter (fun e -> OrderedEquality.compare e eq <= 0) new_pos
 427         | Some symbols ->
 428             let filterfun e =
 429               if OrderedEquality.compare e eq <= 0 then
 430                 true
 431               else
 432                 let foldfun k v (r1, r2) =
 433                   if TermMap.mem k symbols then
 434                     let c = TermMap.find k symbols in
 435                     let c1 = abs (c - v) in
 436                     let c2 = v - c1 in
 437                     r1 + c2, r2 + c1
 438                   else
 439                     r1, r2 + v
 440                 in
 441                 let initial =
 442                   let common, others =
 443                     TermMap.fold foldfun (symbols_of_equality eq) (0, 0) in
 444                   others + (abs (common - card))
 445                 in
 446                 let common, others =
 447                   TermMap.fold foldfun (symbols_of_equality e) (0, 0) in
 448                 let c = others + (abs (common - card)) in
 449                 if c < initial then true else false
 450             in
 451             List.filter filterfun new_pos
 452       in
 453       new_neg, new_pos
 454 ;;
 455
 456
 457 let contains_empty env (negative, positive) =
 458   let metasenv, context, ugraph = env in
 459   try
 460     let found =
 461       List.find
 462         (fun (w, proof, (ty, left, right, ordering), m, a) ->
 463            fst (CicReduction.are_convertible context left right ugraph))
 464         negative
 465     in
 466     true, Some found
 467   with Not_found ->
 468     false, None
 469 ;;
 470
 471
 472 (** simplifies current using active and passive *)
 473 let forward_simplify env (sign, current) ?passive (active_list, active_table) =
 474   let pl, passive_table =
 475     match passive with
 476     | None -> [], None
 477     | Some ((pn, _), (pp, _), pt) ->
 478         let pn = List.map (fun e -> (Negative, e)) pn
 479         and pp = List.map (fun e -> (Positive, e)) pp in
 480         pn @ pp, Some pt
 481   in
 482   let all = if pl = [] then active_list else active_list @ pl in
 483
 484   let demodulate table current =
 485     let newmeta, newcurrent =
 486       let _ =
 487         let w, proof, (eq_ty, left, right, order), metas, args = current in
 488         let metasenv, context, ugraph = env in
 489         let metasenv' = metasenv @ metas in
 490         try
 491           CicTypeChecker.type_of_aux' metasenv' context left ugraph;
 492           CicTypeChecker.type_of_aux' metasenv' context right ugraph;
 493         with
 494             CicUtil.Meta_not_found _ as exn ->
 495               begin
 496                 prerr_endline "siamo in forward_simplify";
 497                 prerr_endline (CicPp.ppterm left);
 498                 prerr_endline (CicPp.ppterm right);
 499                 raise exn
 500               end
 501       in
 502       Indexing.demodulation_equality !maxmeta env table sign current in
 503     maxmeta := newmeta;
 504     if is_identity env newcurrent then
 505       if sign = Negative then Some (sign, newcurrent)
 506       else (
 507 (*      debug_print  *)
 508 (*        (lazy *)
 509 (*           (Printf.sprintf "\ncurrent was: %s\nnewcurrent is: %s\n" *)
 510 (*              (string_of_equality current) *)
 511 (*              (string_of_equality newcurrent))); *)
 512 (*      debug_print *)
 513 (*        (lazy *)
 514 (*           (Printf.sprintf "active is: %s" *)
 515 (*              (String.concat "\n"  *)
 516 (*                 (List.map (fun (_, e) -> (string_of_equality e)) active_list)))); *)
 517         None
 518       )
 519     else
 520       Some (sign, newcurrent)
 521   in
 522   let res =
 523     let res = demodulate active_table current in
 524     match res with
 525     | None -> None
 526     | Some (sign, newcurrent) ->
 527         match passive_table with
 528         | None -> res
 529         | Some passive_table -> demodulate passive_table newcurrent
 530   in
 531   match res with
 532   | None -> None
 533   | Some (Negative, c) ->
 534       let ok = not (
 535         List.exists
 536           (fun (s, eq) -> s = Negative && meta_convertibility_eq eq c)
 537           all)
 538       in
 539       if ok then res else None
 540   | Some (Positive, c) ->
 541       if Indexing.in_index active_table c then
 542         None
 543       else
 544         match passive_table with
 545         | None ->
 546             if fst (Indexing.subsumption env active_table c) then
 547               None
 548             else
 549               res
 550         | Some passive_table ->
 551             if Indexing.in_index passive_table c then None
 552             else
 553               let r1, _ = Indexing.subsumption env active_table c in
 554               if r1 then None else
 555                 let r2, _ = Indexing.subsumption env passive_table c in
 556                 if r2 then None else res
 557 ;;
 558
 559 type fs_time_info_t = {
 560   mutable build_all: float;
 561   mutable demodulate: float;
 562   mutable subsumption: float;
 563 };;
 564
 565 let fs_time_info = { build_all = 0.; demodulate = 0.; subsumption = 0. };;
 566
 567
 568 (** simplifies new using active and passive *)
 569 let forward_simplify_new env (new_neg, new_pos) ?passive active =
 570   let t1 = Unix.gettimeofday () in
 571
 572   let active_list, active_table = active in
 573   let pl, passive_table =
 574     match passive with
 575     | None -> [], None
 576     | Some ((pn, _), (pp, _), pt) ->
 577         let pn = List.map (fun e -> (Negative, e)) pn
 578         and pp = List.map (fun e -> (Positive, e)) pp in
 579         pn @ pp, Some pt
 580   in
 581
 582   let t2 = Unix.gettimeofday () in
 583   fs_time_info.build_all <- fs_time_info.build_all +. (t2 -. t1);
 584
 585   let demodulate sign table target =
 586     let newmeta, newtarget =
 587       let _ =
 588         let w, proof, (eq_ty, left, right, order), metas, args = target in
 589         let metasenv, context, ugraph = env in
 590         let metasenv' = metasenv @ metas in
 591         try
 592           CicTypeChecker.type_of_aux' metasenv' context left ugraph;
 593           CicTypeChecker.type_of_aux' metasenv' context right ugraph;
 594         with
 595             CicUtil.Meta_not_found _ as exn ->
 596               begin
 597                 prerr_endline "siamo in forward_simplify_new";
 598                 prerr_endline (CicPp.ppterm left);
 599                 prerr_endline (CicPp.ppterm right);
 600                 raise exn
 601               end
 602       in
 603       Indexing.demodulation_equality !maxmeta env table sign target in
 604     maxmeta := newmeta;
 605     newtarget
 606   in
 607   let t1 = Unix.gettimeofday () in
 608
 609   let new_neg, new_pos =
 610     let new_neg = List.map (demodulate Negative active_table) new_neg
 611     and new_pos = List.map (demodulate Positive active_table) new_pos in
 612     match passive_table with
 613     | None -> new_neg, new_pos
 614     | Some passive_table ->
 615         List.map (demodulate Negative passive_table) new_neg,
 616         List.map (demodulate Positive passive_table) new_pos
 617   in
 618
 619   let t2 = Unix.gettimeofday () in
 620   fs_time_info.demodulate <- fs_time_info.demodulate +. (t2 -. t1);
 621
 622   let new_pos_set =
 623     List.fold_left
 624       (fun s e ->
 625          if not (Inference.is_identity env e) then
 626            if EqualitySet.mem e s then s
 627            else EqualitySet.add e s
 628          else s)
 629       EqualitySet.empty new_pos
 630   in
 631   let new_pos = EqualitySet.elements new_pos_set in
 632
 633   let subs =
 634     match passive_table with
 635     | None ->
 636         (fun e -> not (fst (Indexing.subsumption env active_table e)))
 637     | Some passive_table ->
 638         (fun e -> not ((fst (Indexing.subsumption env active_table e)) ||
 639                          (fst (Indexing.subsumption env passive_table e))))
 640   in
 641 (*   let t1 = Unix.gettimeofday () in *)
 642 (*   let t2 = Unix.gettimeofday () in *)
 643 (*   fs_time_info.subsumption <- fs_time_info.subsumption +. (t2 -. t1); *)
 644   let is_duplicate =
 645     match passive_table with
 646     | None ->
 647         (fun e -> not (Indexing.in_index active_table e))
 648     | Some passive_table ->
 649         (fun e ->
 650            not ((Indexing.in_index active_table e) ||
 651                   (Indexing.in_index passive_table e)))
 652   in
 653   new_neg, List.filter subs (List.filter is_duplicate new_pos)
 654 ;;
 655
 656
 657 (** simplifies active usign new *)
 658 let backward_simplify_active env new_pos new_table min_weight active =
 659   let active_list, active_table = active in
 660   let active_list, newa =
 661     List.fold_right
 662       (fun (s, equality) (res, newn) ->
 663          let ew, _, _, _, _ = equality in
 664          if ew < min_weight then
 665            (s, equality)::res, newn
 666          else
 667            match forward_simplify env (s, equality) (new_pos, new_table) with
 668            | None -> res, newn
 669            | Some (s, e) ->
 670                if equality = e then
 671                  (s, e)::res, newn
 672                else
 673                  res, (s, e)::newn)
 674       active_list ([], [])
 675   in
 676   let find eq1 where =
 677     List.exists (fun (s, e) -> meta_convertibility_eq eq1 e) where
 678   in
 679   let active, newa =
 680     List.fold_right
 681       (fun (s, eq) (res, tbl) ->
 682          if List.mem (s, eq) res then
 683            res, tbl
 684          else if (is_identity env eq) || (find eq res) then (
 685            res, tbl
 686          )
 687          else
 688            (s, eq)::res, if s = Negative then tbl else Indexing.index tbl eq)
 689       active_list ([], Indexing.empty),
 690     List.fold_right
 691       (fun (s, eq) (n, p) ->
 692          if (s <> Negative) && (is_identity env eq) then (
 693            (n, p)
 694          ) else
 695            if s = Negative then eq::n, p
 696            else n, eq::p)
 697       newa ([], [])
 698   in
 699   match newa with
 700   | [], [] -> active, None
 701   | _ -> active, Some newa
 702 ;;
 703
 704
 705 (** simplifies passive using new *)
 706 let backward_simplify_passive env new_pos new_table min_weight passive =
 707   let (nl, ns), (pl, ps), passive_table = passive in
 708   let f sign equality (resl, ress, newn) =
 709     let ew, _, _, _, _ = equality in
 710     if ew < min_weight then
 711       equality::resl, ress, newn
 712     else
 713       match forward_simplify env (sign, equality) (new_pos, new_table) with
 714       | None -> resl, EqualitySet.remove equality ress, newn
 715       | Some (s, e) ->
 716           if equality = e then
 717             equality::resl, ress, newn
 718           else
 719             let ress = EqualitySet.remove equality ress in
 720             resl, ress, e::newn
 721   in
 722   let nl, ns, newn = List.fold_right (f Negative) nl ([], ns, [])
 723   and pl, ps, newp = List.fold_right (f Positive) pl ([], ps, []) in
 724   let passive_table =
 725     List.fold_left
 726       (fun tbl e -> Indexing.index tbl e) Indexing.empty pl
 727   in
 728   match newn, newp with
 729   | [], [] -> ((nl, ns), (pl, ps), passive_table), None
 730   | _, _ -> ((nl, ns), (pl, ps), passive_table), Some (newn, newp)
 731 ;;
 732
 733
 734 let backward_simplify env new' ?passive active =
 735   let new_pos, new_table, min_weight =
 736     List.fold_left
 737       (fun (l, t, w) e ->
 738          let ew, _, _, _, _ = e in
 739          (Positive, e)::l, Indexing.index t e, min ew w)
 740       ([], Indexing.empty, 1000000) (snd new')
 741   in
 742   let active, newa =
 743     backward_simplify_active env new_pos new_table min_weight active in
 744   match passive with
 745   | None ->
 746       active, (make_passive [] []), newa, None
 747   | Some passive ->
 748       let passive, newp =
 749         backward_simplify_passive env new_pos new_table min_weight passive in
 750       active, passive, newa, newp
 751 ;;
 752
 753
 754 (* returns an estimation of how many equalities in passive can be activated
 755    within the current time limit *)
 756 let get_selection_estimate () =
 757   elapsed_time := (Unix.gettimeofday ()) -. !start_time;
 758   (*   !processed_clauses * (int_of_float (!time_limit /. !elapsed_time)) *)
 759   int_of_float (
 760     ceil ((float_of_int !processed_clauses) *.
 761             ((!time_limit (* *. 2. *)) /. !elapsed_time -. 1.)))
 762 ;;
 763
 764
 765 (** initializes the set of goals *)
 766 let make_goals goal =
 767   let active = []
 768   and passive = [0, [goal]] in
 769   active, passive
 770 ;;
 771
 772
 773 (** initializes the set of theorems *)
 774 let make_theorems theorems =
 775   theorems, []
 776 ;;
 777
 778
 779 let activate_goal (active, passive) =
 780   match passive with
 781   | goal_conj::tl -> true, (goal_conj::active, tl)
 782   | [] -> false, (active, passive)
 783 ;;
 784
 785
 786 let activate_theorem (active, passive) =
 787   match passive with
 788   | theorem::tl -> true, (theorem::active, tl)
 789   | [] -> false, (active, passive)
 790 ;;
 791
 792
 793 (** simplifies a goal with equalities in active and passive *)
 794 let simplify_goal env goal ?passive (active_list, active_table) =
 795   let pl, passive_table =
 796     match passive with
 797     | None -> [], None
 798     | Some ((pn, _), (pp, _), pt) ->
 799         let pn = List.map (fun e -> (Negative, e)) pn
 800         and pp = List.map (fun e -> (Positive, e)) pp in
 801         pn @ pp, Some pt
 802   in
 803
 804   let demodulate table goal =
 805     let newmeta, newgoal =
 806       Indexing.demodulation_goal !maxmeta env table goal in
 807     maxmeta := newmeta;
 808     goal != newgoal, newgoal
 809   in
 810   let changed, goal =
 811     match passive_table with
 812     | None -> demodulate active_table goal
 813     | Some passive_table ->
 814         let changed, goal = demodulate active_table goal in
 815         let changed', goal = demodulate passive_table goal in
 816         (changed || changed'), goal
 817   in
 818   changed, goal
 819 ;;
 820
 821
 822 let simplify_goals env goals ?passive active =
 823   let a_goals, p_goals = goals in
 824   let p_goals =
 825     List.map
 826       (fun (d, gl) ->
 827          let gl =
 828            List.map (fun g -> snd (simplify_goal env g ?passive active)) gl in
 829          d, gl)
 830       p_goals
 831   in
 832   let goals =
 833     List.fold_left
 834       (fun (a, p) (d, gl) ->
 835          let changed = ref false in
 836          let gl =
 837            List.map
 838              (fun g ->
 839                 let c, g = simplify_goal env g ?passive active in
 840                 changed := !changed || c; g) gl in
 841          if !changed then (a, (d, gl)::p) else ((d, gl)::a, p))
 842       ([], p_goals) a_goals
 843   in
 844   goals
 845 ;;
 846
 847
 848 let simplify_theorems env theorems ?passive (active_list, active_table) =
 849   let pl, passive_table =
 850     match passive with
 851     | None -> [], None
 852     | Some ((pn, _), (pp, _), pt) ->
 853         let pn = List.map (fun e -> (Negative, e)) pn
 854         and pp = List.map (fun e -> (Positive, e)) pp in
 855         pn @ pp, Some pt
 856   in
 857   let a_theorems, p_theorems = theorems in
 858   let demodulate table theorem =
 859     let newmeta, newthm =
 860       Indexing.demodulation_theorem !maxmeta env table theorem in
 861     maxmeta := newmeta;
 862     theorem != newthm, newthm
 863   in
 864   let foldfun table (a, p) theorem =
 865     let changed, theorem = demodulate table theorem in
 866     if changed then (a, theorem::p) else (theorem::a, p)
 867   in
 868   let mapfun table theorem = snd (demodulate table theorem) in
 869   match passive_table with
 870   | None ->
 871       let p_theorems = List.map (mapfun active_table) p_theorems in
 872       List.fold_left (foldfun active_table) ([], p_theorems) a_theorems
 873   | Some passive_table ->
 874       let p_theorems = List.map (mapfun active_table) p_theorems in
 875       let p_theorems, a_theorems =
 876         List.fold_left (foldfun active_table) ([], p_theorems) a_theorems in
 877       let p_theorems = List.map (mapfun passive_table) p_theorems in
 878       List.fold_left (foldfun passive_table) ([], p_theorems) a_theorems
 879 ;;
 880
 881
 882 let rec simpl env e others others_simpl =
 883   let active = others @ others_simpl in
 884   let tbl =
 885     List.fold_left
 886       (fun t (_, e) -> Indexing.index t e)
 887       Indexing.empty active
 888   in
 889   let res = forward_simplify env e (active, tbl) in
 890     match others with
 891       | hd::tl -> (
 892           match res with
 893             | None -> simpl env hd tl others_simpl
 894             | Some e -> simpl env hd tl (e::others_simpl)
 895         )
 896       | [] -> (
 897           match res with
 898             | None -> others_simpl
 899             | Some e -> e::others_simpl
 900         )
 901 ;;
 902
 903 let simplify_equalities env equalities =
 904   debug_print
 905     (lazy
 906        (Printf.sprintf "equalities:\n%s\n"
 907           (String.concat "\n"
 908              (List.map string_of_equality equalities))));
 909   debug_print (lazy "SIMPLYFYING EQUALITIES...");
 910   match equalities with
 911     | [] -> []
 912     | hd::tl ->
 913         let others = List.map (fun e -> (Positive, e)) tl in
 914         let res =
 915           List.rev (List.map snd (simpl env (Positive, hd) others []))
 916         in
 917           debug_print
 918             (lazy
 919                (Printf.sprintf "equalities AFTER:\n%s\n"
 920                   (String.concat "\n"
 921                      (List.map string_of_equality res))));
 922           res
 923 ;;
 924
 925 (* applies equality to goal to see if the goal can be closed *)
 926 let apply_equality_to_goal env equality goal =
 927   let module C = Cic in
 928   let module HL = HelmLibraryObjects in
 929   let module I = Inference in
 930   let metasenv, context, ugraph = env in
 931   let _, proof, (ty, left, right, _), metas, args = equality in
 932   let eqterm =
 933     C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []); ty; left; right] in
 934   let gproof, gmetas, gterm = goal in
 935 (*   debug_print *)
 936 (*     (lazy *)
 937 (*        (Printf.sprintf "APPLY EQUALITY TO GOAL: %s, %s" *)
 938 (*           (string_of_equality equality) (CicPp.ppterm gterm))); *)
 939   try
 940     let subst, metasenv', _ =
 941       let menv = metasenv @ metas @ gmetas in
 942       Inference.unification menv context eqterm gterm ugraph
 943     in
 944     let newproof =
 945       match proof with
 946       | I.BasicProof t -> I.BasicProof (CicMetaSubst.apply_subst subst t)
 947       | I.ProofBlock (s, uri, nt, t, pe, p) ->
 948           I.ProofBlock (subst @ s, uri, nt, t, pe, p)
 949       | _ -> assert false
 950     in
 951     let newgproof =
 952       let rec repl = function
 953         | I.ProofGoalBlock (_, gp) -> I.ProofGoalBlock (newproof, gp)
 954         | I.NoProof -> newproof
 955         | I.BasicProof p -> newproof
 956         | I.SubProof (t, i, p) -> I.SubProof (t, i, repl p)
 957         | _ -> assert false
 958       in
 959       repl gproof
 960     in
 961     true, subst, newgproof
 962   with CicUnification.UnificationFailure _ ->
 963     false, [], I.NoProof
 964 ;;
 965
 966
 967
 968 let new_meta metasenv =
 969   let m = CicMkImplicit.new_meta metasenv [] in
 970   incr maxmeta;
 971   while !maxmeta <= m do incr maxmeta done;
 972   !maxmeta
 973 ;;
 974
 975
 976 (* applies a theorem or an equality to goal, returning a list of subgoals or
 977    an indication of failure *)
 978 let apply_to_goal env theorems ?passive active goal =
 979   let metasenv, context, ugraph = env in
 980   let proof, metas, term = goal in
 981   (*   debug_print *)
 982   (*     (lazy *)
 983   (*        (Printf.sprintf "apply_to_goal with goal: %s" *)
 984   (*           (\* (string_of_proof proof)  *\)(CicPp.ppterm term))); *)
 985   let status =
 986     let irl =
 987       CicMkImplicit.identity_relocation_list_for_metavariable context in
 988     let proof', newmeta =
 989       let rec get_meta = function
 990         | SubProof (t, i, p) ->
 991             let t', i' = get_meta p in
 992             if i' = -1 then t, i else t', i'
 993         | ProofGoalBlock (_, p) -> get_meta p
 994         | _ -> Cic.Implicit None, -1
 995       in
 996       let p, m = get_meta proof in
 997       if m = -1 then
 998         let n = new_meta (metasenv @ metas) in
 999         Cic.Meta (n, irl), n
1000       else
1001         p, m
1002     in
1003     let metasenv = (newmeta, context, term)::metasenv @ metas in
1004     let bit = new_meta metasenv, context, term in
1005     let metasenv' = bit::metasenv in
1006     ((None, metasenv', Cic.Meta (newmeta, irl), term), newmeta)
1007   in
1008   let rec aux = function
1009     | [] -> `No
1010     | (theorem, thmty, _)::tl ->
1011         try
1012           let subst, (newproof, newgoals) =
1013             PrimitiveTactics.apply_tac_verbose_with_subst ~term:theorem status
1014           in
1015           if newgoals = [] then
1016             let _, _, p, _ = newproof in
1017             let newp =
1018               let rec repl = function
1019                 | Inference.ProofGoalBlock (_, gp) ->
1020                     Inference.ProofGoalBlock (Inference.BasicProof p, gp)
1021                 | Inference.NoProof -> Inference.BasicProof p
1022                 | Inference.BasicProof _ -> Inference.BasicProof p
1023                 | Inference.SubProof (t, i, p2) ->
1024                     Inference.SubProof (t, i, repl p2)
1025                 | _ -> assert false
1026               in
1027               repl proof
1028             in
1029             let _, m = status in
1030             let subst = List.filter (fun (i, _) -> i = m) subst in
1031             `Ok (subst, [newp, metas, term])
1032           else
1033             let _, menv, p, _ = newproof in
1034             let irl =
1035               CicMkImplicit.identity_relocation_list_for_metavariable context
1036             in
1037             let goals =
1038               List.map
1039                 (fun i ->
1040                    let _, _, ty = CicUtil.lookup_meta i menv in
1041                    let p' =
1042                      let rec gp = function
1043                        | SubProof (t, i, p) ->
1044                            SubProof (t, i, gp p)
1045                        | ProofGoalBlock (sp1, sp2) ->
1046                            ProofGoalBlock (sp1, gp sp2)
1047                        | BasicProof _
1048                        | NoProof ->
1049                            SubProof (p, i, BasicProof (Cic.Meta (i, irl)))
1050                        | ProofSymBlock (s, sp) ->
1051                            ProofSymBlock (s, gp sp)
1052                        | ProofBlock (s, u, nt, t, pe, sp) ->
1053                            ProofBlock (s, u, nt, t, pe, gp sp)
1054                      in gp proof
1055                    in
1056                    (p', menv, ty))
1057                 newgoals
1058             in
1059             let goals =
1060               let weight t =
1061                 let w, m = weight_of_term t in
1062                 w + 2 * (List.length m)
1063               in
1064               List.sort
1065                 (fun (_, _, t1) (_, _, t2) ->
1066                    Pervasives.compare (weight t1) (weight t2))
1067                 goals
1068             in
1069             let best = aux tl in
1070             match best with
1071             | `Ok (_, _) -> best
1072             | `No -> `GoOn ([subst, goals])
1073             | `GoOn sl -> `GoOn ((subst, goals)::sl)
1074         with ProofEngineTypes.Fail msg ->
1075           aux tl
1076   in
1077   let r, s, l =
1078     if Inference.term_is_equality term then
1079       let rec appleq_a = function
1080         | [] -> false, [], []
1081         | (Positive, equality)::tl ->
1082             let ok, s, newproof = apply_equality_to_goal env equality goal in
1083             if ok then true, s, [newproof, metas, term] else appleq_a tl
1084         | _::tl -> appleq_a tl
1085       in
1086       let rec appleq_p = function
1087         | [] -> false, [], []
1088         | equality::tl ->
1089             let ok, s, newproof = apply_equality_to_goal env equality goal in
1090             if ok then true, s, [newproof, metas, term] else appleq_p tl
1091       in
1092       let al, _ = active in
1093       match passive with
1094       | None -> appleq_a al
1095       | Some (_, (pl, _), _) ->
1096           let r, s, l = appleq_a al in if r then r, s, l else appleq_p pl
1097     else
1098       false, [], []
1099   in
1100   if r = true then `Ok (s, l) else aux theorems
1101 ;;
1102
1103
1104 (* sorts a conjunction of goals in order to detect earlier if it is
1105    unsatisfiable. Non-predicate goals are placed at the end of the list *)
1106 let sort_goal_conj (metasenv, context, ugraph) (depth, gl) =
1107   let gl =
1108     List.stable_sort
1109       (fun (_, e1, g1) (_, e2, g2) ->
1110          let ty1, _ =
1111            CicTypeChecker.type_of_aux' (e1 @ metasenv) context g1 ugraph
1112          and ty2, _ =
1113            CicTypeChecker.type_of_aux' (e2 @ metasenv) context g2 ugraph
1114          in
1115          let prop1 =
1116            let b, _ =
1117              CicReduction.are_convertible context (Cic.Sort Cic.Prop) ty1 ugraph
1118            in
1119            if b then 0 else 1
1120          and prop2 =
1121            let b, _ =
1122              CicReduction.are_convertible context (Cic.Sort Cic.Prop) ty2 ugraph
1123            in
1124            if b then 0 else 1
1125          in
1126          if prop1 = 0 && prop2 = 0 then
1127            let e1 = if Inference.term_is_equality g1 then 0 else 1
1128            and e2 = if Inference.term_is_equality g2 then 0 else 1 in
1129            e1 - e2
1130          else
1131            prop1 - prop2)
1132       gl
1133   in
1134   (depth, gl)
1135 ;;
1136
1137
1138 let is_meta_closed goals =
1139   List.for_all (fun (_, _, g) -> CicUtil.is_meta_closed g) goals
1140 ;;
1141
1142
1143 (* applies a series of theorems/equalities to a conjunction of goals *)
1144 let rec apply_to_goal_conj env theorems ?passive active (depth, goals) =
1145   let aux (goal, r) tl =
1146     let propagate_subst subst (proof, metas, term) =
1147       let rec repl = function
1148         | NoProof -> NoProof
1149         | BasicProof t ->
1150             BasicProof (CicMetaSubst.apply_subst subst t)
1151         | ProofGoalBlock (p, pb) ->
1152             let pb' = repl pb in
1153             ProofGoalBlock (p, pb')
1154         | SubProof (t, i, p) ->
1155             let t' = CicMetaSubst.apply_subst subst t in
1156             let p = repl p in
1157             SubProof (t', i, p)
1158         | ProofSymBlock (ens, p) -> ProofSymBlock (ens, repl p)
1159         | ProofBlock (s, u, nty, t, pe, p) ->
1160             ProofBlock (subst @ s, u, nty, t, pe, p)
1161       in (repl proof, metas, term)
1162     in
1163     (* let r = apply_to_goal env theorems ?passive active goal in *) (
1164       match r with
1165       | `No -> `No (depth, goals)
1166       | `GoOn sl ->
1167           let l =
1168             List.map
1169               (fun (s, gl) ->
1170                  let tl = List.map (propagate_subst s) tl in
1171                  sort_goal_conj env (depth+1, gl @ tl)) sl
1172           in
1173           `GoOn l
1174       | `Ok (subst, gl) ->
1175           if tl = [] then
1176             `Ok (depth, gl)
1177           else
1178             let p, _, _ = List.hd gl in
1179             let subproof =
1180               let rec repl = function
1181                 | SubProof (_, _, p) -> repl p
1182                 | ProofGoalBlock (p1, p2) ->
1183                     ProofGoalBlock (repl p1, repl p2)
1184                 | p -> p
1185               in
1186               build_proof_term (repl p)
1187             in
1188             let i =
1189               let rec get_meta = function
1190                 | SubProof (_, i, p) ->
1191                     let i' = get_meta p in
1192                     if i' = -1 then i else i'
1193 (*                         max i (get_meta p) *)
1194                 | ProofGoalBlock (_, p) -> get_meta p
1195                 | _ -> -1
1196               in
1197               get_meta p
1198             in
1199             let subst =
1200               let _, (context, _, _) = List.hd subst in
1201               [i, (context, subproof, Cic.Implicit None)]
1202             in
1203             let tl = List.map (propagate_subst subst) tl in
1204             let conj = sort_goal_conj env (depth(* +1 *), tl) in
1205             `GoOn ([conj])
1206     )
1207   in
1208   if depth > !maxdepth || (List.length goals) > !maxwidth then
1209     `No (depth, goals)
1210   else
1211     let rec search_best res = function
1212       | [] -> res
1213       | goal::tl ->
1214           let r = apply_to_goal env theorems ?passive active goal in
1215           match r with
1216           | `Ok _ -> (goal, r)
1217           | `No -> search_best res tl
1218           | `GoOn l ->
1219               let newres =
1220                 match res with
1221                 | _, `Ok _ -> assert false
1222                 | _, `No -> goal, r
1223                 | _, `GoOn l2 ->
1224                     if (List.length l) < (List.length l2) then goal, r else res
1225               in
1226               search_best newres tl
1227     in
1228     let hd = List.hd goals in
1229     let res = hd, (apply_to_goal env theorems ?passive active hd) in
1230     let best =
1231       match res with
1232       | _, `Ok _ -> res
1233       | _, _ -> search_best res (List.tl goals)
1234     in
1235     let res = aux best (List.filter (fun g -> g != (fst best)) goals) in
1236     match res with
1237     | `GoOn ([conj]) when is_meta_closed (snd conj) &&
1238         (List.length (snd conj)) < (List.length goals)->
1239         apply_to_goal_conj env theorems ?passive active conj
1240     | _ -> res
1241 ;;
1242
1243
1244 (*
1245 module OrderedGoals = struct
1246   type t = int * (Inference.proof * Cic.metasenv * Cic.term) list
1247
1248   let compare g1 g2 =
1249     let d1, l1 = g1
1250     and d2, l2 = g2 in
1251     let r = d2 - d1 in
1252     if r <> 0 then r
1253     else let r = (List.length l1) - (List.length l2) in
1254     if r <> 0 then r
1255     else
1256       let res = ref 0 in
1257       let _ =
1258         List.exists2
1259           (fun (_, _, t1) (_, _, t2) ->
1260              let r = Pervasives.compare t1 t2 in
1261              if r <> 0 then (
1262                res := r;
1263                true
1264              ) else
1265                false) l1 l2
1266       in !res
1267 end
1268
1269 module GoalsSet = Set.Make(OrderedGoals);;
1270
1271
1272 exception SearchSpaceOver;;
1273 *)
1274
1275
1276 (*
1277 let apply_to_goals env is_passive_empty theorems active goals =
1278   debug_print (lazy "\n\n\tapply_to_goals\n\n");
1279   let add_to set goals =
1280     List.fold_left (fun s g -> GoalsSet.add g s) set goals
1281   in
1282   let rec aux set = function
1283     | [] ->
1284         debug_print (lazy "HERE!!!");
1285         if is_passive_empty then raise SearchSpaceOver else false, set
1286     | goals::tl ->
1287         let res = apply_to_goal_conj env theorems active goals in
1288         match res with
1289         | `Ok newgoals ->
1290             let _ =
1291               let d, p, t =
1292                 match newgoals with
1293                 | (d, (p, _, t)::_) -> d, p, t
1294                 | _ -> assert false
1295               in
1296               debug_print
1297                 (lazy
1298                    (Printf.sprintf "\nOK!!!!\ndepth: %d\nProof: %s\ngoal: %s\n"
1299                       d (string_of_proof p) (CicPp.ppterm t)))
1300             in
1301             true, GoalsSet.singleton newgoals
1302         | `GoOn newgoals ->
1303             let set' = add_to set (goals::tl) in
1304             let set' = add_to set' newgoals in
1305             false, set'
1306         | `No newgoals ->
1307             aux set tl
1308   in
1309   let n = List.length goals in
1310   let res, goals = aux (add_to GoalsSet.empty goals) goals in
1311   let goals = GoalsSet.elements goals in
1312   debug_print (lazy "\n\tapply_to_goals end\n");
1313   let m = List.length goals in
1314   if m = n && is_passive_empty then
1315     raise SearchSpaceOver
1316   else
1317     res, goals
1318 ;;
1319 *)
1320
1321
1322 (* sorts the list of passive goals to minimize the search for a proof (doesn't
1323    work that well yet...) *)
1324 let sort_passive_goals goals =
1325   List.stable_sort
1326     (fun (d1, l1) (d2, l2) ->
1327        let r1 = d2 - d1
1328        and r2 = (List.length l1) - (List.length l2) in
1329        let foldfun ht (_, _, t) =
1330          let _ = List.map (fun i -> Hashtbl.replace ht i 1) (metas_of_term t)
1331          in ht
1332        in
1333        let m1 = Hashtbl.length (List.fold_left foldfun (Hashtbl.create 3) l1)
1334        and m2 = Hashtbl.length (List.fold_left foldfun (Hashtbl.create 3) l2)
1335        in let r3 = m1 - m2 in
1336        if r3 <> 0 then r3
1337        else if r2 <> 0 then r2
1338        else r1)
1339     (*          let _, _, g1 = List.hd l1 *)
1340 (*          and _, _, g2 = List.hd l2 in *)
1341 (*          let e1 = if Inference.term_is_equality g1 then 0 else 1 *)
1342 (*          and e2 = if Inference.term_is_equality g2 then 0 else 1 *)
1343 (*          in let r4 = e1 - e2 in *)
1344 (*          if r4 <> 0 then r3 else r1) *)
1345     goals
1346 ;;
1347
1348
1349 let print_goals goals =
1350   (String.concat "\n"
1351      (List.map
1352         (fun (d, gl) ->
1353            let gl' =
1354              List.map
1355                (fun (p, _, t) ->
1356                   (* (string_of_proof p) ^ ", " ^ *) (CicPp.ppterm t)) gl
1357            in
1358            Printf.sprintf "%d: %s" d (String.concat "; " gl')) goals))
1359 ;;
1360
1361
1362 (* tries to prove the first conjunction in goals with applications of
1363    theorems/equalities, returning new sub-goals or an indication of success *)
1364 let apply_goal_to_theorems dbd env theorems ?passive active goals =
1365   let theorems, _ = theorems in
1366   let a_goals, p_goals = goals in
1367   let goal = List.hd a_goals in
1368   let not_in_active gl =
1369     not
1370       (List.exists
1371          (fun (_, gl') ->
1372             if (List.length gl) = (List.length gl') then
1373               List.for_all2 (fun (_, _, g1) (_, _, g2) -> g1 = g2) gl gl'
1374             else
1375               false)
1376          a_goals)
1377   in
1378   let aux theorems =
1379     let res = apply_to_goal_conj env theorems ?passive active goal in
1380     match res with
1381     | `Ok newgoals ->
1382         true, ([newgoals], [])
1383     | `No _ ->
1384         false, (a_goals, p_goals)
1385     | `GoOn newgoals ->
1386         let newgoals =
1387           List.filter
1388             (fun (d, gl) ->
1389                (d <= !maxdepth) && (List.length gl) <= !maxwidth &&
1390                  not_in_active gl)
1391             newgoals in
1392         let p_goals = newgoals @ p_goals in
1393         let p_goals = sort_passive_goals p_goals in
1394         false, (a_goals, p_goals)
1395   in
1396   aux theorems
1397 ;;
1398
1399
1400 let apply_theorem_to_goals env theorems active goals =
1401   let a_goals, p_goals = goals in
1402   let theorem = List.hd (fst theorems) in
1403   let theorems = [theorem] in
1404   let rec aux p = function
1405     | [] -> false, ([], p)
1406     | goal::tl ->
1407         let res = apply_to_goal_conj env theorems active goal in
1408         match res with
1409         | `Ok newgoals -> true, ([newgoals], [])
1410         | `No _ -> aux p tl
1411         | `GoOn newgoals -> aux (newgoals @ p) tl
1412   in
1413   let ok, (a, p) = aux p_goals a_goals in
1414   if ok then
1415     ok, (a, p)
1416   else
1417     let p_goals =
1418       List.stable_sort
1419         (fun (d1, l1) (d2, l2) ->
1420            let r = d2 - d1 in
1421            if r <> 0 then r
1422            else let r = (List.length l1) - (List.length l2) in
1423            if r <> 0 then r
1424            else
1425              let res = ref 0 in
1426              let _ =
1427                List.exists2
1428                  (fun (_, _, t1) (_, _, t2) ->
1429                     let r = Pervasives.compare t1 t2 in
1430                     if r <> 0 then (res := r; true) else false) l1 l2
1431              in !res)
1432         p
1433     in
1434     ok, (a_goals, p_goals)
1435 ;;
1436
1437
1438 (* given-clause algorithm with lazy reduction strategy *)
1439 let rec given_clause dbd env goals theorems passive active =
1440   let goals = simplify_goals env goals active in
1441   let ok, goals = activate_goal goals in
1442   (*   let theorems = simplify_theorems env theorems active in *)
1443   if ok then
1444     let ok, goals = apply_goal_to_theorems dbd env theorems active goals in
1445     if ok then
1446       let proof =
1447         match (fst goals) with
1448         | (_, [proof, _, _])::_ -> Some proof
1449         | _ -> assert false
1450       in
1451       ParamodulationSuccess (proof, env)
1452     else
1453       given_clause_aux dbd env goals theorems passive active
1454   else
1455 (*     let ok', theorems = activate_theorem theorems in *)
1456     let ok', theorems = false, theorems in
1457     if ok' then
1458       let ok, goals = apply_theorem_to_goals env theorems active goals in
1459       if ok then
1460         let proof =
1461           match (fst goals) with
1462           | (_, [proof, _, _])::_ -> Some proof
1463           | _ -> assert false
1464         in
1465         ParamodulationSuccess (proof, env)
1466       else
1467         given_clause_aux dbd env goals theorems passive active
1468     else
1469       if (passive_is_empty passive) then ParamodulationFailure
1470       else given_clause_aux dbd env goals theorems passive active
1471
1472 and given_clause_aux dbd env goals theorems passive active =
1473   let time1 = Unix.gettimeofday () in
1474
1475   let selection_estimate = get_selection_estimate () in
1476   let kept = size_of_passive passive in
1477   let passive =
1478     if !time_limit = 0. || !processed_clauses = 0 then
1479       passive
1480     else if !elapsed_time > !time_limit then (
1481       debug_print (lazy (Printf.sprintf "Time limit (%.2f) reached: %.2f\n"
1482                            !time_limit !elapsed_time));
1483       make_passive [] []
1484     ) else if kept > selection_estimate then (
1485       debug_print
1486         (lazy (Printf.sprintf ("Too many passive equalities: pruning..." ^^
1487                                  "(kept: %d, selection_estimate: %d)\n")
1488                  kept selection_estimate));
1489       prune_passive selection_estimate active passive
1490     ) else
1491       passive
1492   in
1493
1494   let time2 = Unix.gettimeofday () in
1495   passive_maintainance_time := !passive_maintainance_time +. (time2 -. time1);
1496
1497   kept_clauses := (size_of_passive passive) + (size_of_active active);
1498   match passive_is_empty passive with
1499   | true -> (* ParamodulationFailure *)
1500       given_clause dbd env goals theorems passive active
1501   | false ->
1502       let (sign, current), passive = select env (fst goals) passive active in
1503       let time1 = Unix.gettimeofday () in
1504       let res = forward_simplify env (sign, current) ~passive active in
1505       let time2 = Unix.gettimeofday () in
1506       forward_simpl_time := !forward_simpl_time +. (time2 -. time1);
1507       match res with
1508       | None ->
1509           given_clause dbd env goals theorems passive active
1510       | Some (sign, current) ->
1511           if (sign = Negative) && (is_identity env current) then (
1512             debug_print
1513               (lazy (Printf.sprintf "OK!!! %s %s" (string_of_sign sign)
1514                        (string_of_equality ~env current)));
1515             let _, proof, _, _, _  = current in
1516             ParamodulationSuccess (Some proof, env)
1517           ) else (
1518             debug_print
1519               (lazy "\n================================================");
1520             debug_print (lazy (Printf.sprintf "selected: %s %s"
1521                                  (string_of_sign sign)
1522                                  (string_of_equality ~env current)));
1523
1524             let t1 = Unix.gettimeofday () in
1525             let new' = infer env sign current active in
1526             let t2 = Unix.gettimeofday () in
1527             infer_time := !infer_time +. (t2 -. t1);
1528
1529             let res, goal' = contains_empty env new' in
1530             if res then
1531               let proof =
1532                 match goal' with
1533                 | Some goal -> let _, proof, _, _, _ = goal in Some proof
1534                 | None -> None
1535               in
1536               ParamodulationSuccess (proof, env)
1537             else
1538               let t1 = Unix.gettimeofday () in
1539               let new' = forward_simplify_new env new' active in
1540               let t2 = Unix.gettimeofday () in
1541               let _ =
1542                 forward_simpl_new_time :=
1543                   !forward_simpl_new_time +. (t2 -. t1)
1544               in
1545               let active =
1546                 match sign with
1547                 | Negative -> active
1548                 | Positive ->
1549                     let t1 = Unix.gettimeofday () in
1550                     let active, _, newa, _ =
1551                       backward_simplify env ([], [current]) active
1552                     in
1553                     let t2 = Unix.gettimeofday () in
1554                     backward_simpl_time :=
1555                       !backward_simpl_time +. (t2 -. t1);
1556                     match newa with
1557                     | None -> active
1558                     | Some (n, p) ->
1559                         let al, tbl = active in
1560                         let nn = List.map (fun e -> Negative, e) n in
1561                         let pp, tbl =
1562                           List.fold_right
1563                             (fun e (l, t) ->
1564                                (Positive, e)::l,
1565                                Indexing.index tbl e)
1566                             p ([], tbl)
1567                         in
1568                         nn @ al @ pp, tbl
1569               in
1570               match contains_empty env new' with
1571               | false, _ ->
1572                   let active =
1573                     let al, tbl = active in
1574                     match sign with
1575                     | Negative -> (sign, current)::al, tbl
1576                     | Positive ->
1577                         al @ [(sign, current)], Indexing.index tbl current
1578                   in
1579                   let passive = add_to_passive passive new' in
1580                   given_clause dbd env goals theorems passive active
1581               | true, goal ->
1582                   let proof =
1583                     match goal with
1584                     | Some goal ->
1585                         let _, proof, _, _, _ = goal in Some proof
1586                     | None -> None
1587                   in
1588                   ParamodulationSuccess (proof, env)
1589           )
1590 ;;
1591
1592
1593 (** given-clause algorithm with full reduction strategy *)
1594 let rec given_clause_fullred dbd env goals theorems passive active =
1595   let goals = simplify_goals env goals ~passive active in
1596   let ok, goals = activate_goal goals in
1597 (*   let theorems = simplify_theorems env theorems ~passive active in *)
1598   if ok then
1599 (*     let _ = *)
1600 (*       debug_print *)
1601 (*         (lazy *)
1602 (*            (Printf.sprintf "\ngoals = \nactive\n%s\npassive\n%s\n" *)
1603 (*               (print_goals (fst goals)) (print_goals (snd goals)))); *)
1604 (*       let current = List.hd (fst goals) in *)
1605 (*       let p, _, t = List.hd (snd current) in *)
1606 (*       debug_print *)
1607 (*         (lazy *)
1608 (*            (Printf.sprintf "goal activated:\n%s\n%s\n" *)
1609 (*               (CicPp.ppterm t) (string_of_proof p))); *)
1610 (*     in *)
1611     let ok, goals =
1612       apply_goal_to_theorems dbd env theorems ~passive active goals
1613     in
1614     if ok then
1615       let proof =
1616         match (fst goals) with
1617         | (_, [proof, _, _])::_ -> Some proof
1618         | _ -> assert false
1619       in
1620       ParamodulationSuccess (proof, env)
1621     else
1622       given_clause_fullred_aux dbd env goals theorems passive active
1623   else
1624 (*     let ok', theorems = activate_theorem theorems in *)
1625 (*     if ok' then *)
1626 (*       let ok, goals = apply_theorem_to_goals env theorems active goals in *)
1627 (*       if ok then *)
1628 (*         let proof = *)
1629 (*           match (fst goals) with *)
1630 (*           | (_, [proof, _, _])::_ -> Some proof *)
1631 (*           | _ -> assert false *)
1632 (*         in *)
1633 (*         ParamodulationSuccess (proof, env) *)
1634 (*       else *)
1635 (*         given_clause_fullred_aux env goals theorems passive active *)
1636 (*     else *)
1637       if (passive_is_empty passive) then ParamodulationFailure
1638       else given_clause_fullred_aux dbd env goals theorems passive active
1639
1640 and given_clause_fullred_aux dbd env goals theorems passive active =
1641   let time1 = Unix.gettimeofday () in
1642
1643   let selection_estimate = get_selection_estimate () in
1644   let kept = size_of_passive passive in
1645   let passive =
1646     if !time_limit = 0. || !processed_clauses = 0 then
1647       passive
1648     else if !elapsed_time > !time_limit then (
1649       debug_print (lazy (Printf.sprintf "Time limit (%.2f) reached: %.2f\n"
1650                            !time_limit !elapsed_time));
1651       make_passive [] []
1652     ) else if kept > selection_estimate then (
1653       debug_print
1654         (lazy (Printf.sprintf ("Too many passive equalities: pruning..." ^^
1655                                  "(kept: %d, selection_estimate: %d)\n")
1656                  kept selection_estimate));
1657       prune_passive selection_estimate active passive
1658     ) else
1659       passive
1660   in
1661
1662   let time2 = Unix.gettimeofday () in
1663   passive_maintainance_time := !passive_maintainance_time +. (time2 -. time1);
1664
1665   kept_clauses := (size_of_passive passive) + (size_of_active active);
1666   match passive_is_empty passive with
1667   | true -> (* ParamodulationFailure *)
1668       given_clause_fullred dbd env goals theorems passive active
1669   | false ->
1670       let (sign, current), passive = select env (fst goals) passive active in
1671       let time1 = Unix.gettimeofday () in
1672       let res = forward_simplify env (sign, current) ~passive active in
1673       let time2 = Unix.gettimeofday () in
1674       forward_simpl_time := !forward_simpl_time +. (time2 -. time1);
1675       match res with
1676       | None ->
1677           given_clause_fullred dbd env goals theorems passive active
1678       | Some (sign, current) ->
1679           if (sign = Negative) && (is_identity env current) then (
1680             debug_print
1681               (lazy (Printf.sprintf "OK!!! %s %s" (string_of_sign sign)
1682                        (string_of_equality ~env current)));
1683             let _, proof, _, _, _ = current in
1684             ParamodulationSuccess (Some proof, env)
1685           ) else (
1686             debug_print
1687               (lazy "\n================================================");
1688             debug_print (lazy (Printf.sprintf "selected: %s %s"
1689                                  (string_of_sign sign)
1690                                  (string_of_equality ~env current)));
1691
1692             let t1 = Unix.gettimeofday () in
1693             let new' = infer env sign current active in
1694             let t2 = Unix.gettimeofday () in
1695             infer_time := !infer_time +. (t2 -. t1);
1696
1697             let active =
1698               if is_identity env current then active
1699               else
1700                 let al, tbl = active in
1701                 match sign with
1702                 | Negative -> (sign, current)::al, tbl
1703                 | Positive ->
1704                     al @ [(sign, current)], Indexing.index tbl current
1705             in
1706             let rec simplify new' active passive =
1707               let t1 = Unix.gettimeofday () in
1708               let new' = forward_simplify_new env new' ~passive active in
1709               let t2 = Unix.gettimeofday () in
1710               forward_simpl_new_time :=
1711                 !forward_simpl_new_time +. (t2 -. t1);
1712               let t1 = Unix.gettimeofday () in
1713               let active, passive, newa, retained =
1714                 backward_simplify env new' ~passive active in
1715               let t2 = Unix.gettimeofday () in
1716               backward_simpl_time := !backward_simpl_time +. (t2 -. t1);
1717               match newa, retained with
1718               | None, None -> active, passive, new'
1719               | Some (n, p), None
1720               | None, Some (n, p) ->
1721                   let nn, np = new' in
1722                   simplify (nn @ n, np @ p) active passive
1723               | Some (n, p), Some (rn, rp) ->
1724                   let nn, np = new' in
1725                   simplify (nn @ n @ rn, np @ p @ rp) active passive
1726             in
1727             let active, passive, new' = simplify new' active passive in
1728
1729             let k = size_of_passive passive in
1730             if k < (kept - 1) then
1731               processed_clauses := !processed_clauses + (kept - 1 - k);
1732
1733             let _ =
1734               debug_print
1735                 (lazy
1736                    (Printf.sprintf "active:\n%s\n"
1737                       (String.concat "\n"
1738                          ((List.map
1739                              (fun (s, e) -> (string_of_sign s) ^ " " ^
1740                                 (string_of_equality ~env e))
1741                              (fst active))))))
1742             in
1743             let _ =
1744               match new' with
1745               | neg, pos ->
1746                   debug_print
1747                     (lazy
1748                        (Printf.sprintf "new':\n%s\n"
1749                           (String.concat "\n"
1750                              ((List.map
1751                                  (fun e -> "Negative " ^
1752                                     (string_of_equality ~env e)) neg) @
1753                                 (List.map
1754                                    (fun e -> "Positive " ^
1755                                       (string_of_equality ~env e)) pos)))))
1756             in
1757             match contains_empty env new' with
1758             | false, _ ->
1759                 let passive = add_to_passive passive new' in
1760                 given_clause_fullred dbd env goals theorems passive active
1761             | true, goal ->
1762                 let proof =
1763                   match goal with
1764                   | Some goal -> let _, proof, _, _, _ = goal in Some proof
1765                   | None -> None
1766                 in
1767                 ParamodulationSuccess (proof, env)
1768           )
1769 ;;
1770
1771
1772 let rec saturate_equations env goal accept_fun passive active =
1773   elapsed_time := Unix.gettimeofday () -. !start_time;
1774   if !elapsed_time > !time_limit then
1775     (active, passive)
1776   else
1777     let (sign, current), passive = select env [1, [goal]] passive active in
1778     let res = forward_simplify env (sign, current) ~passive active in
1779     match res with
1780     | None ->
1781         saturate_equations env goal accept_fun passive active
1782     | Some (sign, current) ->
1783         assert (sign = Positive);
1784         debug_print
1785           (lazy "\n================================================");
1786         debug_print (lazy (Printf.sprintf "selected: %s %s"
1787                              (string_of_sign sign)
1788                              (string_of_equality ~env current)));
1789         let new' = infer env sign current active in
1790         let active =
1791           if is_identity env current then active
1792           else
1793             let al, tbl = active in
1794             al @ [(sign, current)], Indexing.index tbl current
1795         in
1796         let rec simplify new' active passive =
1797           let new' = forward_simplify_new env new' ~passive active in
1798           let active, passive, newa, retained =
1799             backward_simplify env new' ~passive active in
1800           match newa, retained with
1801           | None, None -> active, passive, new'
1802           | Some (n, p), None
1803           | None, Some (n, p) ->
1804               let nn, np = new' in
1805               simplify (nn @ n, np @ p) active passive
1806           | Some (n, p), Some (rn, rp) ->
1807               let nn, np = new' in
1808               simplify (nn @ n @ rn, np @ p @ rp) active passive
1809         in
1810         let active, passive, new' = simplify new' active passive in
1811         let _ =
1812           debug_print
1813             (lazy
1814                (Printf.sprintf "active:\n%s\n"
1815                   (String.concat "\n"
1816                      ((List.map
1817                          (fun (s, e) -> (string_of_sign s) ^ " " ^
1818                             (string_of_equality ~env e))
1819                          (fst active))))))
1820         in
1821         let _ =
1822           match new' with
1823           | neg, pos ->
1824               debug_print
1825                 (lazy
1826                    (Printf.sprintf "new':\n%s\n"
1827                       (String.concat "\n"
1828                          ((List.map
1829                              (fun e -> "Negative " ^
1830                                 (string_of_equality ~env e)) neg) @
1831                             (List.map
1832                                (fun e -> "Positive " ^
1833                                   (string_of_equality ~env e)) pos)))))
1834         in
1835         let new' = match new' with _, pos -> [], List.filter accept_fun pos in
1836         let passive = add_to_passive passive new' in
1837         saturate_equations env goal accept_fun passive active
1838 ;;
1839
1840
1841
1842
1843 let main dbd full term metasenv ugraph =
1844   let module C = Cic in
1845   let module T = CicTypeChecker in
1846   let module PET = ProofEngineTypes in
1847   let module PP = CicPp in
1848   let proof = None, (1, [], term)::metasenv, C.Meta (1, []), term in
1849   let status = PET.apply_tactic (PrimitiveTactics.intros_tac ()) (proof, 1) in
1850   let proof, goals = status in
1851   let goal' = List.nth goals 0 in
1852   let _, metasenv, meta_proof, _ = proof in
1853   let _, context, goal = CicUtil.lookup_meta goal' metasenv in
1854   let eq_indexes, equalities, maxm = find_equalities context proof in
1855   let lib_eq_uris, library_equalities, maxm =
1856     find_library_equalities dbd context (proof, goal') (maxm+2)
1857   in
1858   let library_equalities = List.map snd library_equalities in
1859   maxmeta := maxm+2; (* TODO ugly!! *)
1860   let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
1861   let new_meta_goal, metasenv, type_of_goal =
1862     let _, context, ty = CicUtil.lookup_meta goal' metasenv in
1863     debug_print
1864       (lazy
1865          (Printf.sprintf "\n\nTIPO DEL GOAL: %s\n\n" (CicPp.ppterm ty)));
1866     Cic.Meta (maxm+1, irl),
1867     (maxm+1, context, ty)::metasenv,
1868     ty
1869   in
1870   let env = (metasenv, context, ugraph) in
1871   let t1 = Unix.gettimeofday () in
1872   let theorems =
1873     if full then
1874       let theorems = find_library_theorems dbd env (proof, goal') lib_eq_uris in
1875       let context_hyp = find_context_hypotheses env eq_indexes in
1876       context_hyp @ theorems, []
1877     else
1878       let refl_equal =
1879         let us = UriManager.string_of_uri (LibraryObjects.eq_URI ()) in
1880         UriManager.uri_of_string (us ^ "#xpointer(1/1/1)")
1881       in
1882       let t = CicUtil.term_of_uri refl_equal in
1883       let ty, _ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in
1884       [(t, ty, [])], []
1885   in
1886   let t2 = Unix.gettimeofday () in
1887   debug_print
1888     (lazy
1889        (Printf.sprintf "Time to retrieve theorems: %.9f\n" (t2 -. t1)));
1890   let _ =
1891     debug_print
1892       (lazy
1893          (Printf.sprintf
1894             "Theorems:\n-------------------------------------\n%s\n"
1895             (String.concat "\n"
1896                (List.map
1897                   (fun (t, ty, _) ->
1898                      Printf.sprintf
1899                        "Term: %s, type: %s" (CicPp.ppterm t) (CicPp.ppterm ty))
1900                   (fst theorems)))))
1901   in
1902   (*try*)
1903     let goal = Inference.BasicProof new_meta_goal, [], goal in
1904     let equalities = simplify_equalities env (equalities@library_equalities) in
1905     let active = make_active () in
1906     let passive = make_passive [] equalities in
1907     Printf.printf "\ncurrent goal: %s\n"
1908       (let _, _, g = goal in CicPp.ppterm g);
1909     Printf.printf "\ncontext:\n%s\n" (PP.ppcontext context);
1910     Printf.printf "\nmetasenv:\n%s\n" (print_metasenv metasenv);
1911     Printf.printf "\nequalities:\n%s\n"
1912       (String.concat "\n"
1913          (List.map
1914             (string_of_equality ~env) equalities));
1915 (*             (equalities @ library_equalities))); *)
1916       print_endline "--------------------------------------------------";
1917       let start = Unix.gettimeofday () in
1918       print_endline "GO!";
1919       start_time := Unix.gettimeofday ();
1920       let res =
1921         let goals = make_goals goal in
1922         (if !use_fullred then given_clause_fullred else given_clause)
1923           dbd env goals theorems passive active
1924       in
1925       let finish = Unix.gettimeofday () in
1926       let _ =
1927         match res with
1928         | ParamodulationFailure ->
1929             Printf.printf "NO proof found! :-(\n\n"
1930         | ParamodulationSuccess (Some proof, env) ->
1931             let proof = Inference.build_proof_term proof in
1932             Printf.printf "OK, found a proof!\n";
1933             (* REMEMBER: we have to instantiate meta_proof, we should use
1934                apply  the "apply" tactic to proof and status
1935             *)
1936             let names = names_of_context context in
1937             print_endline (PP.pp proof names);
1938             let newmetasenv =
1939               List.fold_left
1940                 (fun m (_, _, _, menv, _) -> m @ menv) metasenv equalities
1941             in
1942             let _ =
1943               (*try*)
1944                 let ty, ug =
1945                   CicTypeChecker.type_of_aux' newmetasenv context proof ugraph
1946                 in
1947                 print_endline (string_of_float (finish -. start));
1948                 Printf.printf
1949                   "\nGOAL was: %s\nPROOF has type: %s\nconvertible?: %s\n\n"
1950                   (CicPp.pp type_of_goal names) (CicPp.pp ty names)
1951                   (string_of_bool
1952                      (fst (CicReduction.are_convertible
1953                              context type_of_goal ty ug)));
1954               (*with e ->
1955                 Printf.printf "\nEXCEPTION!!! %s\n" (Printexc.to_string e);
1956                 Printf.printf "MAXMETA USED: %d\n" !maxmeta;
1957                 print_endline (string_of_float (finish -. start));*)
1958             in
1959             ()
1960
1961         | ParamodulationSuccess (None, env) ->
1962             Printf.printf "Success, but no proof?!?\n\n"
1963       in
1964       Printf.printf ("infer_time: %.9f\nforward_simpl_time: %.9f\n" ^^
1965                        "forward_simpl_new_time: %.9f\n" ^^
1966                        "backward_simpl_time: %.9f\n")
1967         !infer_time !forward_simpl_time !forward_simpl_new_time
1968         !backward_simpl_time;
1969       Printf.printf "passive_maintainance_time: %.9f\n"
1970         !passive_maintainance_time;
1971       Printf.printf "    successful unification/matching time: %.9f\n"
1972         !Indexing.match_unif_time_ok;
1973       Printf.printf "    failed unification/matching time: %.9f\n"
1974         !Indexing.match_unif_time_no;
1975       Printf.printf "    indexing retrieval time: %.9f\n"
1976         !Indexing.indexing_retrieval_time;
1977       Printf.printf "    demodulate_term.build_newtarget_time: %.9f\n"
1978         !Indexing.build_newtarget_time;
1979       Printf.printf "derived %d clauses, kept %d clauses.\n"
1980         !derived_clauses !kept_clauses;
1981 (*
1982   with exc ->
1983     print_endline ("EXCEPTION: " ^ (Printexc.to_string exc));
1984     raise exc
1985 *)
1986 ;;
1987
1988
1989 let default_depth = !maxdepth
1990 and default_width = !maxwidth;;
1991
1992 let reset_refs () =
1993   maxmeta := 0;
1994   symbols_counter := 0;
1995   weight_age_counter := !weight_age_ratio;
1996   processed_clauses := 0;
1997   start_time := 0.;
1998   elapsed_time := 0.;
1999   maximal_retained_equality := None;
2000   infer_time := 0.;
2001   forward_simpl_time := 0.;
2002   forward_simpl_new_time := 0.;
2003   backward_simpl_time := 0.;
2004   passive_maintainance_time := 0.;
2005   derived_clauses := 0;
2006   kept_clauses := 0;
2007 ;;
2008
2009 let saturate
2010     dbd ?(full=false) ?(depth=default_depth) ?(width=default_width) status =
2011   let module C = Cic in
2012   reset_refs ();
2013   Indexing.init_index ();
2014   maxdepth := depth;
2015   maxwidth := width;
2016   let proof, goal = status in
2017   let goal' = goal in
2018   let uri, metasenv, meta_proof, term_to_prove = proof in
2019   let _, context, goal = CicUtil.lookup_meta goal' metasenv in
2020   let eq_indexes, equalities, maxm = find_equalities context proof in
2021   let new_meta_goal, metasenv, type_of_goal =
2022     let irl =
2023       CicMkImplicit.identity_relocation_list_for_metavariable context in
2024     let _, context, ty = CicUtil.lookup_meta goal' metasenv in
2025     debug_print
2026       (lazy (Printf.sprintf "\n\nTIPO DEL GOAL: %s\n" (CicPp.ppterm ty)));
2027     Cic.Meta (maxm+1, irl),
2028     (maxm+1, context, ty)::metasenv,
2029     ty
2030   in
2031   let ugraph = CicUniv.empty_ugraph in
2032   let env = (metasenv, context, ugraph) in
2033   let goal = Inference.BasicProof new_meta_goal, [], goal in
2034   let res, time =
2035     let t1 = Unix.gettimeofday () in
2036     let lib_eq_uris, library_equalities, maxm =
2037       find_library_equalities dbd context (proof, goal') (maxm+2)
2038     in
2039     let library_equalities = List.map snd library_equalities in
2040     let t2 = Unix.gettimeofday () in
2041     maxmeta := maxm+2;
2042     let equalities = simplify_equalities env (equalities@library_equalities) in
2043     debug_print
2044       (lazy
2045          (Printf.sprintf "Time to retrieve equalities: %.9f\n" (t2 -. t1)));
2046     let t1 = Unix.gettimeofday () in
2047     let theorems =
2048       if full then
2049         let thms = find_library_theorems dbd env (proof, goal') lib_eq_uris in
2050         let context_hyp = find_context_hypotheses env eq_indexes in
2051         context_hyp @ thms, []
2052       else
2053         let refl_equal =
2054           let us = UriManager.string_of_uri (LibraryObjects.eq_URI ()) in
2055           UriManager.uri_of_string (us ^ "#xpointer(1/1/1)")
2056         in
2057         let t = CicUtil.term_of_uri refl_equal in
2058         let ty, _ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in
2059         [(t, ty, [])], []
2060     in
2061     let t2 = Unix.gettimeofday () in
2062     let _ =
2063       debug_print
2064         (lazy
2065            (Printf.sprintf
2066               "Theorems:\n-------------------------------------\n%s\n"
2067               (String.concat "\n"
2068                  (List.map
2069                     (fun (t, ty, _) ->
2070                        Printf.sprintf
2071                          "Term: %s, type: %s"
2072                          (CicPp.ppterm t) (CicPp.ppterm ty))
2073                     (fst theorems)))));
2074       debug_print
2075         (lazy
2076            (Printf.sprintf "Time to retrieve theorems: %.9f\n" (t2 -. t1)));
2077     in
2078     let active = make_active () in
2079     let passive = make_passive [] equalities in
2080     let start = Unix.gettimeofday () in
2081     let res =
2082       let goals = make_goals goal in
2083       given_clause_fullred dbd env goals theorems passive active
2084     in
2085     let finish = Unix.gettimeofday () in
2086     (res, finish -. start)
2087   in
2088   match res with
2089   | ParamodulationSuccess (Some proof, env) ->
2090       debug_print (lazy "OK, found a proof!");
2091       let proof = Inference.build_proof_term proof in
2092       let names = names_of_context context in
2093       let newmetasenv =
2094         let i1 =
2095           match new_meta_goal with
2096           | C.Meta (i, _) -> i | _ -> assert false
2097         in
2098         List.filter (fun (i, _, _) -> i <> i1 && i <> goal') metasenv
2099       in
2100       let newstatus =
2101         try
2102           let ty, ug =
2103             CicTypeChecker.type_of_aux' newmetasenv context proof ugraph
2104           in
2105           debug_print (lazy (CicPp.pp proof [](* names *)));
2106           debug_print
2107             (lazy
2108                (Printf.sprintf
2109                   "\nGOAL was: %s\nPROOF has type: %s\nconvertible?: %s\n"
2110                   (CicPp.pp type_of_goal names) (CicPp.pp ty names)
2111                   (string_of_bool
2112                      (fst (CicReduction.are_convertible
2113                              context type_of_goal ty ug)))));
2114           let equality_for_replace i t1 =
2115             match t1 with
2116             | C.Meta (n, _) -> n = i
2117             | _ -> false
2118           in
2119           let real_proof =
2120             ProofEngineReduction.replace
2121               ~equality:equality_for_replace
2122               ~what:[goal'] ~with_what:[proof]
2123               ~where:meta_proof
2124           in
2125           debug_print
2126             (lazy
2127                (Printf.sprintf "status:\n%s\n%s\n%s\n%s\n"
2128                   (match uri with Some uri -> UriManager.string_of_uri uri
2129                    | None -> "")
2130                   (print_metasenv newmetasenv)
2131                   (CicPp.pp real_proof [](* names *))
2132                   (CicPp.pp term_to_prove names)));
2133           ((uri, newmetasenv, real_proof, term_to_prove), [])
2134         with CicTypeChecker.TypeCheckerFailure _ ->
2135           debug_print (lazy "THE PROOF DOESN'T TYPECHECK!!!");
2136           debug_print (lazy (CicPp.pp proof names));
2137           raise (ProofEngineTypes.Fail
2138                   (lazy "Found a proof, but it doesn't typecheck"))
2139       in
2140       debug_print (lazy (Printf.sprintf "\nTIME NEEDED: %.9f" time));
2141       newstatus
2142   | _ ->
2143       raise (ProofEngineTypes.Fail (lazy "NO proof found"))
2144 ;;
2145
2146 (* dummy function called within matita to trigger linkage *)
2147 let init () = ();;
2148
2149
2150 let retrieve_and_print dbd term metasenv ugraph =
2151   let module C = Cic in
2152   let module T = CicTypeChecker in
2153   let module PET = ProofEngineTypes in
2154   let module PP = CicPp in
2155   let proof = None, (1, [], term)::metasenv, C.Meta (1, []), term in
2156   let status = PET.apply_tactic (PrimitiveTactics.intros_tac ()) (proof, 1) in
2157   let proof, goals = status in
2158   let goal' = List.nth goals 0 in
2159   let uri, metasenv, meta_proof, term_to_prove = proof in
2160   let _, context, goal = CicUtil.lookup_meta goal' metasenv in
2161   let eq_indexes, equalities, maxm = find_equalities context proof in
2162   let new_meta_goal, metasenv, type_of_goal =
2163     let irl =
2164       CicMkImplicit.identity_relocation_list_for_metavariable context in
2165     let _, context, ty = CicUtil.lookup_meta goal' metasenv in
2166     debug_print
2167       (lazy (Printf.sprintf "\n\nTIPO DEL GOAL: %s\n" (CicPp.ppterm ty)));
2168     Cic.Meta (maxm+1, irl),
2169     (maxm+1, context, ty)::metasenv,
2170     ty
2171   in
2172   let ugraph = CicUniv.empty_ugraph in
2173   let env = (metasenv, context, ugraph) in
2174   let t1 = Unix.gettimeofday () in
2175   let lib_eq_uris, library_equalities, maxm =
2176     find_library_equalities dbd context (proof, goal') (maxm+2) in
2177   let t2 = Unix.gettimeofday () in
2178   maxmeta := maxm+2;
2179   let equalities = (* equalities @ *) library_equalities in
2180   debug_print
2181      (lazy
2182         (Printf.sprintf "\n\nequalities:\n%s\n"
2183            (String.concat "\n"
2184               (List.map
2185           (fun (u, e) ->
2186 (*               Printf.sprintf "%s: %s" *)
2187                    (UriManager.string_of_uri u)
2188 (*                 (string_of_equality e) *)
2189                      )
2190           equalities))));
2191   debug_print (lazy "SIMPLYFYING EQUALITIES...");
2192   let rec simpl e others others_simpl =
2193     let (u, e) = e in
2194     let active = List.map (fun (u, e) -> (Positive, e))
2195       (others @ others_simpl) in
2196     let tbl =
2197       List.fold_left
2198         (fun t (_, e) -> Indexing.index t e)
2199         Indexing.empty active
2200     in
2201     let res = forward_simplify env (Positive, e) (active, tbl) in
2202     match others with
2203         | hd::tl -> (
2204             match res with
2205               | None -> simpl hd tl others_simpl
2206               | Some e -> simpl hd tl ((u, (snd e))::others_simpl)
2207           )
2208         | [] -> (
2209             match res with
2210               | None -> others_simpl
2211               | Some e -> (u, (snd e))::others_simpl
2212           )
2213   in
2214   let _equalities =
2215     match equalities with
2216       | [] -> []
2217       | hd::tl ->
2218           let others = tl in (* List.map (fun e -> (Positive, e)) tl in *)
2219           let res =
2220             List.rev (simpl (*(Positive,*) hd others [])
2221           in
2222             debug_print
2223               (lazy
2224                  (Printf.sprintf "\nequalities AFTER:\n%s\n"
2225                     (String.concat "\n"
2226                        (List.map
2227                           (fun (u, e) ->
2228                              Printf.sprintf "%s: %s"
2229                                (UriManager.string_of_uri u)
2230                                (string_of_equality e)
2231                           )
2232                           res))));
2233             res in
2234     debug_print
2235       (lazy
2236          (Printf.sprintf "Time to retrieve equalities: %.9f\n" (t2 -. t1)))
2237 ;;
2238
2239
2240 let main_demod_equalities dbd term metasenv ugraph =
2241   let module C = Cic in
2242   let module T = CicTypeChecker in
2243   let module PET = ProofEngineTypes in
2244   let module PP = CicPp in
2245   let proof = None, (1, [], term)::metasenv, C.Meta (1, []), term in
2246   let status = PET.apply_tactic (PrimitiveTactics.intros_tac ()) (proof, 1) in
2247   let proof, goals = status in
2248   let goal' = List.nth goals 0 in
2249   let _, metasenv, meta_proof, _ = proof in
2250   let _, context, goal = CicUtil.lookup_meta goal' metasenv in
2251   let eq_indexes, equalities, maxm = find_equalities context proof in
2252   let lib_eq_uris, library_equalities, maxm =
2253     find_library_equalities dbd context (proof, goal') (maxm+2)
2254   in
2255   let library_equalities = List.map snd library_equalities in
2256   maxmeta := maxm+2; (* TODO ugly!! *)
2257   let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
2258   let new_meta_goal, metasenv, type_of_goal =
2259     let _, context, ty = CicUtil.lookup_meta goal' metasenv in
2260     debug_print
2261       (lazy
2262          (Printf.sprintf "\n\nTRYING TO INFER EQUALITIES MATCHING: %s\n\n"
2263             (CicPp.ppterm ty)));
2264     Cic.Meta (maxm+1, irl),
2265     (maxm+1, context, ty)::metasenv,
2266     ty
2267   in
2268   let env = (metasenv, context, ugraph) in
2269   (*try*)
2270     let goal = Inference.BasicProof new_meta_goal, [], goal in
2271     let equalities = simplify_equalities env (equalities@library_equalities) in
2272     let active = make_active () in
2273     let passive = make_passive [] equalities in
2274     Printf.printf "\ncontext:\n%s\n" (PP.ppcontext context);
2275     Printf.printf "\nmetasenv:\n%s\n" (print_metasenv metasenv);
2276     Printf.printf "\nequalities:\n%s\n"
2277       (String.concat "\n"
2278          (List.map
2279             (string_of_equality ~env) equalities));
2280     print_endline "--------------------------------------------------";
2281     print_endline "GO!";
2282     start_time := Unix.gettimeofday ();
2283     if !time_limit < 1. then time_limit := 60.;
2284     let ra, rp =
2285       saturate_equations env goal (fun e -> true) passive active
2286     in
2287
2288     let initial =
2289       List.fold_left (fun s e -> EqualitySet.add e s)
2290         EqualitySet.empty equalities
2291     in
2292     let addfun s e =
2293       if not (EqualitySet.mem e initial) then EqualitySet.add e s else s
2294     in
2295
2296     let passive =
2297       match rp with
2298       | (n, _), (p, _), _ ->
2299           EqualitySet.elements (List.fold_left addfun EqualitySet.empty p)
2300     in
2301     let active =
2302       let l = List.map snd (fst ra) in
2303       EqualitySet.elements (List.fold_left addfun EqualitySet.empty l)
2304     in
2305     Printf.printf "\n\nRESULTS:\nActive:\n%s\n\nPassive:\n%s\n"
2306        (String.concat "\n" (List.map (string_of_equality ~env) active))
2307      (*  (String.concat "\n"
2308          (List.map (fun e -> CicPp.ppterm (term_of_equality e)) active)) *)
2309 (*       (String.concat "\n" (List.map (string_of_equality ~env) passive)); *)
2310       (String.concat "\n"
2311          (List.map (fun e -> CicPp.ppterm (term_of_equality e)) passive));
2312     print_newline ();
2313 (*
2314   with e ->
2315     debug_print (lazy ("EXCEPTION: " ^ (Printexc.to_string e)))
2316 *)
2317 ;;
2318
2319 let demodulate_tac ~dbd ~pattern ((proof,goal) as initialstatus) =
2320   let module I = Inference in
2321   let curi,metasenv,pbo,pty = proof in
2322   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
2323   let eq_indexes, equalities, maxm = I.find_equalities context proof in
2324   let lib_eq_uris, library_equalities, maxm =
2325     I.find_library_equalities dbd context (proof, goal) (maxm+2) in
2326   if library_equalities = [] then prerr_endline "VUOTA!!!";
2327   let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
2328   let library_equalities = List.map snd library_equalities in
2329   let goalterm = Cic.Meta (metano,irl) in
2330   let initgoal = Inference.BasicProof goalterm, [], ty in
2331   let env = (metasenv, context, CicUniv.empty_ugraph) in
2332   let equalities = simplify_equalities env (equalities@library_equalities) in
2333   let table =
2334     List.fold_left
2335       (fun tbl eq -> Indexing.index tbl eq)
2336       Indexing.empty equalities
2337   in
2338   let newmeta,(newproof,newmetasenv, newty) = Indexing.demodulation_goal
2339     maxm (metasenv,context,CicUniv.empty_ugraph) table initgoal
2340   in
2341   if newmeta != maxm then
2342     begin
2343       let opengoal = Cic.Meta(maxm,irl) in
2344       let proofterm =
2345         Inference.build_proof_term ~noproof:opengoal newproof in
2346         let extended_metasenv = (maxm,context,newty)::metasenv in
2347         let extended_status =
2348           (curi,extended_metasenv,pbo,pty),goal in
2349         let (status,newgoals) =
2350           ProofEngineTypes.apply_tactic
2351             (PrimitiveTactics.apply_tac ~term:proofterm)
2352             extended_status in
2353         (status,maxm::newgoals)
2354     end
2355   else if newty = ty then
2356     raise (ProofEngineTypes.Fail (lazy "no progress"))
2357   else ProofEngineTypes.apply_tactic
2358     (ReductionTactics.simpl_tac ~pattern)
2359     initialstatus
2360 ;;
2361
2362 let demodulate_tac ~dbd ~pattern =
2363   ProofEngineTypes.mk_tactic (demodulate_tac ~dbd ~pattern)
2364 ;;