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       Indexing.demodulation_equality !maxmeta env table sign current in
 487     maxmeta := newmeta;
 488     if is_identity env newcurrent then
 489       if sign = Negative then Some (sign, newcurrent)
 490       else (
 491 (*      debug_print  *)
 492 (*        (lazy *)
 493 (*           (Printf.sprintf "\ncurrent was: %s\nnewcurrent is: %s\n" *)
 494 (*              (string_of_equality current) *)
 495 (*              (string_of_equality newcurrent))); *)
 496 (*      debug_print *)
 497 (*        (lazy *)
 498 (*           (Printf.sprintf "active is: %s" *)
 499 (*              (String.concat "\n"  *)
 500 (*                 (List.map (fun (_, e) -> (string_of_equality e)) active_list)))); *)
 501         None
 502       )
 503     else
 504       Some (sign, newcurrent)
 505   in
 506   let res =
 507     let res = demodulate active_table current in
 508     match res with
 509     | None -> None
 510     | Some (sign, newcurrent) ->
 511         match passive_table with
 512         | None -> res
 513         | Some passive_table -> demodulate passive_table newcurrent
 514   in
 515   match res with
 516   | None -> None
 517   | Some (Negative, c) ->
 518       let ok = not (
 519         List.exists
 520           (fun (s, eq) -> s = Negative && meta_convertibility_eq eq c)
 521           all)
 522       in
 523       if ok then res else None
 524   | Some (Positive, c) ->
 525       if Indexing.in_index active_table c then
 526         None
 527       else
 528         match passive_table with
 529         | None ->
 530             if fst (Indexing.subsumption env active_table c) then
 531               None
 532             else
 533               res
 534         | Some passive_table ->
 535             if Indexing.in_index passive_table c then None
 536             else
 537               let r1, _ = Indexing.subsumption env active_table c in
 538               if r1 then None else
 539                 let r2, _ = Indexing.subsumption env passive_table c in
 540                 if r2 then None else res
 541 ;;
 542
 543 type fs_time_info_t = {
 544   mutable build_all: float;
 545   mutable demodulate: float;
 546   mutable subsumption: float;
 547 };;
 548
 549 let fs_time_info = { build_all = 0.; demodulate = 0.; subsumption = 0. };;
 550
 551
 552 (** simplifies new using active and passive *)
 553 let forward_simplify_new env (new_neg, new_pos) ?passive active =
 554   let t1 = Unix.gettimeofday () in
 555
 556   let active_list, active_table = active in
 557   let pl, passive_table =
 558     match passive with
 559     | None -> [], None
 560     | Some ((pn, _), (pp, _), pt) ->
 561         let pn = List.map (fun e -> (Negative, e)) pn
 562         and pp = List.map (fun e -> (Positive, e)) pp in
 563         pn @ pp, Some pt
 564   in
 565
 566   let t2 = Unix.gettimeofday () in
 567   fs_time_info.build_all <- fs_time_info.build_all +. (t2 -. t1);
 568
 569   let demodulate sign table target =
 570     let newmeta, newtarget =
 571       Indexing.demodulation_equality !maxmeta env table sign target in
 572     maxmeta := newmeta;
 573     newtarget
 574   in
 575   let t1 = Unix.gettimeofday () in
 576
 577   let new_neg, new_pos =
 578     let new_neg = List.map (demodulate Negative active_table) new_neg
 579     and new_pos = List.map (demodulate Positive active_table) new_pos in
 580     match passive_table with
 581     | None -> new_neg, new_pos
 582     | Some passive_table ->
 583         List.map (demodulate Negative passive_table) new_neg,
 584         List.map (demodulate Positive passive_table) new_pos
 585   in
 586
 587   let t2 = Unix.gettimeofday () in
 588   fs_time_info.demodulate <- fs_time_info.demodulate +. (t2 -. t1);
 589
 590   let new_pos_set =
 591     List.fold_left
 592       (fun s e ->
 593          if not (Inference.is_identity env e) then
 594            if EqualitySet.mem e s then s
 595            else EqualitySet.add e s
 596          else s)
 597       EqualitySet.empty new_pos
 598   in
 599   let new_pos = EqualitySet.elements new_pos_set in
 600
 601   let subs =
 602     match passive_table with
 603     | None ->
 604         (fun e -> not (fst (Indexing.subsumption env active_table e)))
 605     | Some passive_table ->
 606         (fun e -> not ((fst (Indexing.subsumption env active_table e)) ||
 607                          (fst (Indexing.subsumption env passive_table e))))
 608   in
 609 (*   let t1 = Unix.gettimeofday () in *)
 610 (*   let t2 = Unix.gettimeofday () in *)
 611 (*   fs_time_info.subsumption <- fs_time_info.subsumption +. (t2 -. t1); *)
 612   let is_duplicate =
 613     match passive_table with
 614     | None ->
 615         (fun e -> not (Indexing.in_index active_table e))
 616     | Some passive_table ->
 617         (fun e ->
 618            not ((Indexing.in_index active_table e) ||
 619                   (Indexing.in_index passive_table e)))
 620   in
 621   new_neg, List.filter subs (List.filter is_duplicate new_pos)
 622 ;;
 623
 624
 625 (** simplifies active usign new *)
 626 let backward_simplify_active env new_pos new_table min_weight active =
 627   let active_list, active_table = active in
 628   let active_list, newa =
 629     List.fold_right
 630       (fun (s, equality) (res, newn) ->
 631          let ew, _, _, _, _ = equality in
 632          if ew < min_weight then
 633            (s, equality)::res, newn
 634          else
 635            match forward_simplify env (s, equality) (new_pos, new_table) with
 636            | None -> res, newn
 637            | Some (s, e) ->
 638                if equality = e then
 639                  (s, e)::res, newn
 640                else
 641                  res, (s, e)::newn)
 642       active_list ([], [])
 643   in
 644   let find eq1 where =
 645     List.exists (fun (s, e) -> meta_convertibility_eq eq1 e) where
 646   in
 647   let active, newa =
 648     List.fold_right
 649       (fun (s, eq) (res, tbl) ->
 650          if List.mem (s, eq) res then
 651            res, tbl
 652          else if (is_identity env eq) || (find eq res) then (
 653            res, tbl
 654          )
 655          else
 656            (s, eq)::res, if s = Negative then tbl else Indexing.index tbl eq)
 657       active_list ([], Indexing.empty),
 658     List.fold_right
 659       (fun (s, eq) (n, p) ->
 660          if (s <> Negative) && (is_identity env eq) then (
 661            (n, p)
 662          ) else
 663            if s = Negative then eq::n, p
 664            else n, eq::p)
 665       newa ([], [])
 666   in
 667   match newa with
 668   | [], [] -> active, None
 669   | _ -> active, Some newa
 670 ;;
 671
 672
 673 (** simplifies passive using new *)
 674 let backward_simplify_passive env new_pos new_table min_weight passive =
 675   let (nl, ns), (pl, ps), passive_table = passive in
 676   let f sign equality (resl, ress, newn) =
 677     let ew, _, _, _, _ = equality in
 678     if ew < min_weight then
 679       equality::resl, ress, newn
 680     else
 681       match forward_simplify env (sign, equality) (new_pos, new_table) with
 682       | None -> resl, EqualitySet.remove equality ress, newn
 683       | Some (s, e) ->
 684           if equality = e then
 685             equality::resl, ress, newn
 686           else
 687             let ress = EqualitySet.remove equality ress in
 688             resl, ress, e::newn
 689   in
 690   let nl, ns, newn = List.fold_right (f Negative) nl ([], ns, [])
 691   and pl, ps, newp = List.fold_right (f Positive) pl ([], ps, []) in
 692   let passive_table =
 693     List.fold_left
 694       (fun tbl e -> Indexing.index tbl e) Indexing.empty pl
 695   in
 696   match newn, newp with
 697   | [], [] -> ((nl, ns), (pl, ps), passive_table), None
 698   | _, _ -> ((nl, ns), (pl, ps), passive_table), Some (newn, newp)
 699 ;;
 700
 701
 702 let backward_simplify env new' ?passive active =
 703   let new_pos, new_table, min_weight =
 704     List.fold_left
 705       (fun (l, t, w) e ->
 706          let ew, _, _, _, _ = e in
 707          (Positive, e)::l, Indexing.index t e, min ew w)
 708       ([], Indexing.empty, 1000000) (snd new')
 709   in
 710   let active, newa =
 711     backward_simplify_active env new_pos new_table min_weight active in
 712   match passive with
 713   | None ->
 714       active, (make_passive [] []), newa, None
 715   | Some passive ->
 716       let passive, newp =
 717         backward_simplify_passive env new_pos new_table min_weight passive in
 718       active, passive, newa, newp
 719 ;;
 720
 721
 722 (* returns an estimation of how many equalities in passive can be activated
 723    within the current time limit *)
 724 let get_selection_estimate () =
 725   elapsed_time := (Unix.gettimeofday ()) -. !start_time;
 726   (*   !processed_clauses * (int_of_float (!time_limit /. !elapsed_time)) *)
 727   int_of_float (
 728     ceil ((float_of_int !processed_clauses) *.
 729             ((!time_limit (* *. 2. *)) /. !elapsed_time -. 1.)))
 730 ;;
 731
 732
 733 (** initializes the set of goals *)
 734 let make_goals goal =
 735   let active = []
 736   and passive = [0, [goal]] in
 737   active, passive
 738 ;;
 739
 740
 741 (** initializes the set of theorems *)
 742 let make_theorems theorems =
 743   theorems, []
 744 ;;
 745
 746
 747 let activate_goal (active, passive) =
 748   match passive with
 749   | goal_conj::tl -> true, (goal_conj::active, tl)
 750   | [] -> false, (active, passive)
 751 ;;
 752
 753
 754 let activate_theorem (active, passive) =
 755   match passive with
 756   | theorem::tl -> true, (theorem::active, tl)
 757   | [] -> false, (active, passive)
 758 ;;
 759
 760
 761 (** simplifies a goal with equalities in active and passive *)
 762 let simplify_goal env goal ?passive (active_list, active_table) =
 763   let pl, passive_table =
 764     match passive with
 765     | None -> [], None
 766     | Some ((pn, _), (pp, _), pt) ->
 767         let pn = List.map (fun e -> (Negative, e)) pn
 768         and pp = List.map (fun e -> (Positive, e)) pp in
 769         pn @ pp, Some pt
 770   in
 771
 772   let demodulate table goal =
 773     let newmeta, newgoal =
 774       Indexing.demodulation_goal !maxmeta env table goal in
 775     maxmeta := newmeta;
 776     goal != newgoal, newgoal
 777   in
 778   let changed, goal =
 779     match passive_table with
 780     | None -> demodulate active_table goal
 781     | Some passive_table ->
 782         let changed, goal = demodulate active_table goal in
 783         let changed', goal = demodulate passive_table goal in
 784         (changed || changed'), goal
 785   in
 786   changed, goal
 787 ;;
 788
 789
 790 let simplify_goals env goals ?passive active =
 791   let a_goals, p_goals = goals in
 792   let p_goals =
 793     List.map
 794       (fun (d, gl) ->
 795          let gl =
 796            List.map (fun g -> snd (simplify_goal env g ?passive active)) gl in
 797          d, gl)
 798       p_goals
 799   in
 800   let goals =
 801     List.fold_left
 802       (fun (a, p) (d, gl) ->
 803          let changed = ref false in
 804          let gl =
 805            List.map
 806              (fun g ->
 807                 let c, g = simplify_goal env g ?passive active in
 808                 changed := !changed || c; g) gl in
 809          if !changed then (a, (d, gl)::p) else ((d, gl)::a, p))
 810       ([], p_goals) a_goals
 811   in
 812   goals
 813 ;;
 814
 815
 816 let simplify_theorems env theorems ?passive (active_list, active_table) =
 817   let pl, passive_table =
 818     match passive with
 819     | None -> [], None
 820     | Some ((pn, _), (pp, _), pt) ->
 821         let pn = List.map (fun e -> (Negative, e)) pn
 822         and pp = List.map (fun e -> (Positive, e)) pp in
 823         pn @ pp, Some pt
 824   in
 825   let a_theorems, p_theorems = theorems in
 826   let demodulate table theorem =
 827     let newmeta, newthm =
 828       Indexing.demodulation_theorem !maxmeta env table theorem in
 829     maxmeta := newmeta;
 830     theorem != newthm, newthm
 831   in
 832   let foldfun table (a, p) theorem =
 833     let changed, theorem = demodulate table theorem in
 834     if changed then (a, theorem::p) else (theorem::a, p)
 835   in
 836   let mapfun table theorem = snd (demodulate table theorem) in
 837   match passive_table with
 838   | None ->
 839       let p_theorems = List.map (mapfun active_table) p_theorems in
 840       List.fold_left (foldfun active_table) ([], p_theorems) a_theorems
 841   | Some passive_table ->
 842       let p_theorems = List.map (mapfun active_table) p_theorems in
 843       let p_theorems, a_theorems =
 844         List.fold_left (foldfun active_table) ([], p_theorems) a_theorems in
 845       let p_theorems = List.map (mapfun passive_table) p_theorems in
 846       List.fold_left (foldfun passive_table) ([], p_theorems) a_theorems
 847 ;;
 848
 849
 850 (* applies equality to goal to see if the goal can be closed *)
 851 let apply_equality_to_goal env equality goal =
 852   let module C = Cic in
 853   let module HL = HelmLibraryObjects in
 854   let module I = Inference in
 855   let metasenv, context, ugraph = env in
 856   let _, proof, (ty, left, right, _), metas, args = equality in
 857   let eqterm =
 858     C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []); ty; left; right] in
 859   let gproof, gmetas, gterm = goal in
 860 (*   debug_print *)
 861 (*     (lazy *)
 862 (*        (Printf.sprintf "APPLY EQUALITY TO GOAL: %s, %s" *)
 863 (*           (string_of_equality equality) (CicPp.ppterm gterm))); *)
 864   try
 865     let subst, metasenv', _ =
 866       let menv = metasenv @ metas @ gmetas in
 867       Inference.unification menv context eqterm gterm ugraph
 868     in
 869     let newproof =
 870       match proof with
 871       | I.BasicProof t -> I.BasicProof (CicMetaSubst.apply_subst subst t)
 872       | I.ProofBlock (s, uri, nt, t, pe, p) ->
 873           I.ProofBlock (subst @ s, uri, nt, t, pe, p)
 874       | _ -> assert false
 875     in
 876     let newgproof =
 877       let rec repl = function
 878         | I.ProofGoalBlock (_, gp) -> I.ProofGoalBlock (newproof, gp)
 879         | I.NoProof -> newproof
 880         | I.BasicProof p -> newproof
 881         | I.SubProof (t, i, p) -> I.SubProof (t, i, repl p)
 882         | _ -> assert false
 883       in
 884       repl gproof
 885     in
 886     true, subst, newgproof
 887   with CicUnification.UnificationFailure _ ->
 888     false, [], I.NoProof
 889 ;;
 890
 891
 892
 893 let new_meta metasenv =
 894   let m = CicMkImplicit.new_meta metasenv [] in
 895   incr maxmeta;
 896   while !maxmeta <= m do incr maxmeta done;
 897   !maxmeta
 898 ;;
 899
 900
 901 (* applies a theorem or an equality to goal, returning a list of subgoals or
 902    an indication of failure *)
 903 let apply_to_goal env theorems ?passive active goal =
 904   let metasenv, context, ugraph = env in
 905   let proof, metas, term = goal in
 906   (*   debug_print *)
 907   (*     (lazy *)
 908   (*        (Printf.sprintf "apply_to_goal with goal: %s" *)
 909   (*           (\* (string_of_proof proof)  *\)(CicPp.ppterm term))); *)
 910   let status =
 911     let irl =
 912       CicMkImplicit.identity_relocation_list_for_metavariable context in
 913     let proof', newmeta =
 914       let rec get_meta = function
 915         | SubProof (t, i, p) ->
 916             let t', i' = get_meta p in
 917             if i' = -1 then t, i else t', i'
 918         | ProofGoalBlock (_, p) -> get_meta p
 919         | _ -> Cic.Implicit None, -1
 920       in
 921       let p, m = get_meta proof in
 922       if m = -1 then
 923         let n = new_meta (metasenv @ metas) in
 924         Cic.Meta (n, irl), n
 925       else
 926         p, m
 927     in
 928     let metasenv = (newmeta, context, term)::metasenv @ metas in
 929     let bit = new_meta metasenv, context, term in
 930     let metasenv' = bit::metasenv in
 931     ((None, metasenv', Cic.Meta (newmeta, irl), term), newmeta)
 932   in
 933   let rec aux = function
 934     | [] -> `No
 935     | (theorem, thmty, _)::tl ->
 936         try
 937           let subst, (newproof, newgoals) =
 938             PrimitiveTactics.apply_tac_verbose_with_subst ~term:theorem status
 939           in
 940           if newgoals = [] then
 941             let _, _, p, _ = newproof in
 942             let newp =
 943               let rec repl = function
 944                 | Inference.ProofGoalBlock (_, gp) ->
 945                     Inference.ProofGoalBlock (Inference.BasicProof p, gp)
 946                 | Inference.NoProof -> Inference.BasicProof p
 947                 | Inference.BasicProof _ -> Inference.BasicProof p
 948                 | Inference.SubProof (t, i, p2) ->
 949                     Inference.SubProof (t, i, repl p2)
 950                 | _ -> assert false
 951               in
 952               repl proof
 953             in
 954             let _, m = status in
 955             let subst = List.filter (fun (i, _) -> i = m) subst in
 956             `Ok (subst, [newp, metas, term])
 957           else
 958             let _, menv, p, _ = newproof in
 959             let irl =
 960               CicMkImplicit.identity_relocation_list_for_metavariable context
 961             in
 962             let goals =
 963               List.map
 964                 (fun i ->
 965                    let _, _, ty = CicUtil.lookup_meta i menv in
 966                    let p' =
 967                      let rec gp = function
 968                        | SubProof (t, i, p) ->
 969                            SubProof (t, i, gp p)
 970                        | ProofGoalBlock (sp1, sp2) ->
 971                            ProofGoalBlock (sp1, gp sp2)
 972                        | BasicProof _
 973                        | NoProof ->
 974                            SubProof (p, i, BasicProof (Cic.Meta (i, irl)))
 975                        | ProofSymBlock (s, sp) ->
 976                            ProofSymBlock (s, gp sp)
 977                        | ProofBlock (s, u, nt, t, pe, sp) ->
 978                            ProofBlock (s, u, nt, t, pe, gp sp)
 979                      in gp proof
 980                    in
 981                    (p', menv, ty))
 982                 newgoals
 983             in
 984             let goals =
 985               let weight t =
 986                 let w, m = weight_of_term t in
 987                 w + 2 * (List.length m)
 988               in
 989               List.sort
 990                 (fun (_, _, t1) (_, _, t2) ->
 991                    Pervasives.compare (weight t1) (weight t2))
 992                 goals
 993             in
 994             let best = aux tl in
 995             match best with
 996             | `Ok (_, _) -> best
 997             | `No -> `GoOn ([subst, goals])
 998             | `GoOn sl -> `GoOn ((subst, goals)::sl)
 999         with ProofEngineTypes.Fail msg ->
1000           aux tl
1001   in
1002   let r, s, l =
1003     if Inference.term_is_equality term then
1004       let rec appleq_a = function
1005         | [] -> false, [], []
1006         | (Positive, equality)::tl ->
1007             let ok, s, newproof = apply_equality_to_goal env equality goal in
1008             if ok then true, s, [newproof, metas, term] else appleq_a tl
1009         | _::tl -> appleq_a tl
1010       in
1011       let rec appleq_p = function
1012         | [] -> false, [], []
1013         | equality::tl ->
1014             let ok, s, newproof = apply_equality_to_goal env equality goal in
1015             if ok then true, s, [newproof, metas, term] else appleq_p tl
1016       in
1017       let al, _ = active in
1018       match passive with
1019       | None -> appleq_a al
1020       | Some (_, (pl, _), _) ->
1021           let r, s, l = appleq_a al in if r then r, s, l else appleq_p pl
1022     else
1023       false, [], []
1024   in
1025   if r = true then `Ok (s, l) else aux theorems
1026 ;;
1027
1028
1029 (* sorts a conjunction of goals in order to detect earlier if it is
1030    unsatisfiable. Non-predicate goals are placed at the end of the list *)
1031 let sort_goal_conj (metasenv, context, ugraph) (depth, gl) =
1032   let gl =
1033     List.stable_sort
1034       (fun (_, e1, g1) (_, e2, g2) ->
1035          let ty1, _ =
1036            CicTypeChecker.type_of_aux' (e1 @ metasenv) context g1 ugraph
1037          and ty2, _ =
1038            CicTypeChecker.type_of_aux' (e2 @ metasenv) context g2 ugraph
1039          in
1040          let prop1 =
1041            let b, _ =
1042              CicReduction.are_convertible context (Cic.Sort Cic.Prop) ty1 ugraph
1043            in
1044            if b then 0 else 1
1045          and prop2 =
1046            let b, _ =
1047              CicReduction.are_convertible context (Cic.Sort Cic.Prop) ty2 ugraph
1048            in
1049            if b then 0 else 1
1050          in
1051          if prop1 = 0 && prop2 = 0 then
1052            let e1 = if Inference.term_is_equality g1 then 0 else 1
1053            and e2 = if Inference.term_is_equality g2 then 0 else 1 in
1054            e1 - e2
1055          else
1056            prop1 - prop2)
1057       gl
1058   in
1059   (depth, gl)
1060 ;;
1061
1062
1063 let is_meta_closed goals =
1064   List.for_all (fun (_, _, g) -> CicUtil.is_meta_closed g) goals
1065 ;;
1066
1067
1068 (* applies a series of theorems/equalities to a conjunction of goals *)
1069 let rec apply_to_goal_conj env theorems ?passive active (depth, goals) =
1070   let aux (goal, r) tl =
1071     let propagate_subst subst (proof, metas, term) =
1072       let rec repl = function
1073         | NoProof -> NoProof
1074         | BasicProof t ->
1075             BasicProof (CicMetaSubst.apply_subst subst t)
1076         | ProofGoalBlock (p, pb) ->
1077             let pb' = repl pb in
1078             ProofGoalBlock (p, pb')
1079         | SubProof (t, i, p) ->
1080             let t' = CicMetaSubst.apply_subst subst t in
1081             let p = repl p in
1082             SubProof (t', i, p)
1083         | ProofSymBlock (ens, p) -> ProofSymBlock (ens, repl p)
1084         | ProofBlock (s, u, nty, t, pe, p) ->
1085             ProofBlock (subst @ s, u, nty, t, pe, p)
1086       in (repl proof, metas, term)
1087     in
1088     (* let r = apply_to_goal env theorems ?passive active goal in *) (
1089       match r with
1090       | `No -> `No (depth, goals)
1091       | `GoOn sl ->
1092           let l =
1093             List.map
1094               (fun (s, gl) ->
1095                  let tl = List.map (propagate_subst s) tl in
1096                  sort_goal_conj env (depth+1, gl @ tl)) sl
1097           in
1098           `GoOn l
1099       | `Ok (subst, gl) ->
1100           if tl = [] then
1101             `Ok (depth, gl)
1102           else
1103             let p, _, _ = List.hd gl in
1104             let subproof =
1105               let rec repl = function
1106                 | SubProof (_, _, p) -> repl p
1107                 | ProofGoalBlock (p1, p2) ->
1108                     ProofGoalBlock (repl p1, repl p2)
1109                 | p -> p
1110               in
1111               build_proof_term (repl p)
1112             in
1113             let i =
1114               let rec get_meta = function
1115                 | SubProof (_, i, p) ->
1116                     let i' = get_meta p in
1117                     if i' = -1 then i else i'
1118 (*                         max i (get_meta p) *)
1119                 | ProofGoalBlock (_, p) -> get_meta p
1120                 | _ -> -1
1121               in
1122               get_meta p
1123             in
1124             let subst =
1125               let _, (context, _, _) = List.hd subst in
1126               [i, (context, subproof, Cic.Implicit None)]
1127             in
1128             let tl = List.map (propagate_subst subst) tl in
1129             let conj = sort_goal_conj env (depth(* +1 *), tl) in
1130             `GoOn ([conj])
1131     )
1132   in
1133   if depth > !maxdepth || (List.length goals) > !maxwidth then
1134     `No (depth, goals)
1135   else
1136     let rec search_best res = function
1137       | [] -> res
1138       | goal::tl ->
1139           let r = apply_to_goal env theorems ?passive active goal in
1140           match r with
1141           | `Ok _ -> (goal, r)
1142           | `No -> search_best res tl
1143           | `GoOn l ->
1144               let newres =
1145                 match res with
1146                 | _, `Ok _ -> assert false
1147                 | _, `No -> goal, r
1148                 | _, `GoOn l2 ->
1149                     if (List.length l) < (List.length l2) then goal, r else res
1150               in
1151               search_best newres tl
1152     in
1153     let hd = List.hd goals in
1154     let res = hd, (apply_to_goal env theorems ?passive active hd) in
1155     let best =
1156       match res with
1157       | _, `Ok _ -> res
1158       | _, _ -> search_best res (List.tl goals)
1159     in
1160     let res = aux best (List.filter (fun g -> g != (fst best)) goals) in
1161     match res with
1162     | `GoOn ([conj]) when is_meta_closed (snd conj) &&
1163         (List.length (snd conj)) < (List.length goals)->
1164         apply_to_goal_conj env theorems ?passive active conj
1165     | _ -> res
1166 ;;
1167
1168
1169 (*
1170 module OrderedGoals = struct
1171   type t = int * (Inference.proof * Cic.metasenv * Cic.term) list
1172
1173   let compare g1 g2 =
1174     let d1, l1 = g1
1175     and d2, l2 = g2 in
1176     let r = d2 - d1 in
1177     if r <> 0 then r
1178     else let r = (List.length l1) - (List.length l2) in
1179     if r <> 0 then r
1180     else
1181       let res = ref 0 in
1182       let _ =
1183         List.exists2
1184           (fun (_, _, t1) (_, _, t2) ->
1185              let r = Pervasives.compare t1 t2 in
1186              if r <> 0 then (
1187                res := r;
1188                true
1189              ) else
1190                false) l1 l2
1191       in !res
1192 end
1193
1194 module GoalsSet = Set.Make(OrderedGoals);;
1195
1196
1197 exception SearchSpaceOver;;
1198 *)
1199
1200
1201 (*
1202 let apply_to_goals env is_passive_empty theorems active goals =
1203   debug_print (lazy "\n\n\tapply_to_goals\n\n");
1204   let add_to set goals =
1205     List.fold_left (fun s g -> GoalsSet.add g s) set goals
1206   in
1207   let rec aux set = function
1208     | [] ->
1209         debug_print (lazy "HERE!!!");
1210         if is_passive_empty then raise SearchSpaceOver else false, set
1211     | goals::tl ->
1212         let res = apply_to_goal_conj env theorems active goals in
1213         match res with
1214         | `Ok newgoals ->
1215             let _ =
1216               let d, p, t =
1217                 match newgoals with
1218                 | (d, (p, _, t)::_) -> d, p, t
1219                 | _ -> assert false
1220               in
1221               debug_print
1222                 (lazy
1223                    (Printf.sprintf "\nOK!!!!\ndepth: %d\nProof: %s\ngoal: %s\n"
1224                       d (string_of_proof p) (CicPp.ppterm t)))
1225             in
1226             true, GoalsSet.singleton newgoals
1227         | `GoOn newgoals ->
1228             let set' = add_to set (goals::tl) in
1229             let set' = add_to set' newgoals in
1230             false, set'
1231         | `No newgoals ->
1232             aux set tl
1233   in
1234   let n = List.length goals in
1235   let res, goals = aux (add_to GoalsSet.empty goals) goals in
1236   let goals = GoalsSet.elements goals in
1237   debug_print (lazy "\n\tapply_to_goals end\n");
1238   let m = List.length goals in
1239   if m = n && is_passive_empty then
1240     raise SearchSpaceOver
1241   else
1242     res, goals
1243 ;;
1244 *)
1245
1246
1247 (* sorts the list of passive goals to minimize the search for a proof (doesn't
1248    work that well yet...) *)
1249 let sort_passive_goals goals =
1250   List.stable_sort
1251     (fun (d1, l1) (d2, l2) ->
1252        let r1 = d2 - d1
1253        and r2 = (List.length l1) - (List.length l2) in
1254        let foldfun ht (_, _, t) =
1255          let _ = List.map (fun i -> Hashtbl.replace ht i 1) (metas_of_term t)
1256          in ht
1257        in
1258        let m1 = Hashtbl.length (List.fold_left foldfun (Hashtbl.create 3) l1)
1259        and m2 = Hashtbl.length (List.fold_left foldfun (Hashtbl.create 3) l2)
1260        in let r3 = m1 - m2 in
1261        if r3 <> 0 then r3
1262        else if r2 <> 0 then r2
1263        else r1)
1264     (*          let _, _, g1 = List.hd l1 *)
1265 (*          and _, _, g2 = List.hd l2 in *)
1266 (*          let e1 = if Inference.term_is_equality g1 then 0 else 1 *)
1267 (*          and e2 = if Inference.term_is_equality g2 then 0 else 1 *)
1268 (*          in let r4 = e1 - e2 in *)
1269 (*          if r4 <> 0 then r3 else r1) *)
1270     goals
1271 ;;
1272
1273
1274 let print_goals goals =
1275   (String.concat "\n"
1276      (List.map
1277         (fun (d, gl) ->
1278            let gl' =
1279              List.map
1280                (fun (p, _, t) ->
1281                   (* (string_of_proof p) ^ ", " ^ *) (CicPp.ppterm t)) gl
1282            in
1283            Printf.sprintf "%d: %s" d (String.concat "; " gl')) goals))
1284 ;;
1285
1286
1287 (* tries to prove the first conjunction in goals with applications of
1288    theorems/equalities, returning new sub-goals or an indication of success *)
1289 let apply_goal_to_theorems dbd env theorems ?passive active goals =
1290   let theorems, _ = theorems in
1291   let a_goals, p_goals = goals in
1292   let goal = List.hd a_goals in
1293   let not_in_active gl =
1294     not
1295       (List.exists
1296          (fun (_, gl') ->
1297             if (List.length gl) = (List.length gl') then
1298               List.for_all2 (fun (_, _, g1) (_, _, g2) -> g1 = g2) gl gl'
1299             else
1300               false)
1301          a_goals)
1302   in
1303   let aux theorems =
1304     let res = apply_to_goal_conj env theorems ?passive active goal in
1305     match res with
1306     | `Ok newgoals ->
1307         true, ([newgoals], [])
1308     | `No _ ->
1309         false, (a_goals, p_goals)
1310     | `GoOn newgoals ->
1311         let newgoals =
1312           List.filter
1313             (fun (d, gl) ->
1314                (d <= !maxdepth) && (List.length gl) <= !maxwidth &&
1315                  not_in_active gl)
1316             newgoals in
1317         let p_goals = newgoals @ p_goals in
1318         let p_goals = sort_passive_goals p_goals in
1319         false, (a_goals, p_goals)
1320   in
1321   aux theorems
1322 ;;
1323
1324
1325 let apply_theorem_to_goals env theorems active goals =
1326   let a_goals, p_goals = goals in
1327   let theorem = List.hd (fst theorems) in
1328   let theorems = [theorem] in
1329   let rec aux p = function
1330     | [] -> false, ([], p)
1331     | goal::tl ->
1332         let res = apply_to_goal_conj env theorems active goal in
1333         match res with
1334         | `Ok newgoals -> true, ([newgoals], [])
1335         | `No _ -> aux p tl
1336         | `GoOn newgoals -> aux (newgoals @ p) tl
1337   in
1338   let ok, (a, p) = aux p_goals a_goals in
1339   if ok then
1340     ok, (a, p)
1341   else
1342     let p_goals =
1343       List.stable_sort
1344         (fun (d1, l1) (d2, l2) ->
1345            let r = d2 - d1 in
1346            if r <> 0 then r
1347            else let r = (List.length l1) - (List.length l2) in
1348            if r <> 0 then r
1349            else
1350              let res = ref 0 in
1351              let _ =
1352                List.exists2
1353                  (fun (_, _, t1) (_, _, t2) ->
1354                     let r = Pervasives.compare t1 t2 in
1355                     if r <> 0 then (res := r; true) else false) l1 l2
1356              in !res)
1357         p
1358     in
1359     ok, (a_goals, p_goals)
1360 ;;
1361
1362
1363 (* given-clause algorithm with lazy reduction strategy *)
1364 let rec given_clause dbd env goals theorems passive active =
1365   let goals = simplify_goals env goals active in
1366   let ok, goals = activate_goal goals in
1367   (*   let theorems = simplify_theorems env theorems active in *)
1368   if ok then
1369     let ok, goals = apply_goal_to_theorems dbd env theorems active goals in
1370     if ok then
1371       let proof =
1372         match (fst goals) with
1373         | (_, [proof, _, _])::_ -> Some proof
1374         | _ -> assert false
1375       in
1376       ParamodulationSuccess (proof, env)
1377     else
1378       given_clause_aux dbd env goals theorems passive active
1379   else
1380 (*     let ok', theorems = activate_theorem theorems in *)
1381     let ok', theorems = false, theorems in
1382     if ok' then
1383       let ok, goals = apply_theorem_to_goals env theorems active goals in
1384       if ok then
1385         let proof =
1386           match (fst goals) with
1387           | (_, [proof, _, _])::_ -> Some proof
1388           | _ -> assert false
1389         in
1390         ParamodulationSuccess (proof, env)
1391       else
1392         given_clause_aux dbd env goals theorems passive active
1393     else
1394       if (passive_is_empty passive) then ParamodulationFailure
1395       else given_clause_aux dbd env goals theorems passive active
1396
1397 and given_clause_aux dbd env goals theorems passive active =
1398   let time1 = Unix.gettimeofday () in
1399
1400   let selection_estimate = get_selection_estimate () in
1401   let kept = size_of_passive passive in
1402   let passive =
1403     if !time_limit = 0. || !processed_clauses = 0 then
1404       passive
1405     else if !elapsed_time > !time_limit then (
1406       debug_print (lazy (Printf.sprintf "Time limit (%.2f) reached: %.2f\n"
1407                            !time_limit !elapsed_time));
1408       make_passive [] []
1409     ) else if kept > selection_estimate then (
1410       debug_print
1411         (lazy (Printf.sprintf ("Too many passive equalities: pruning..." ^^
1412                                  "(kept: %d, selection_estimate: %d)\n")
1413                  kept selection_estimate));
1414       prune_passive selection_estimate active passive
1415     ) else
1416       passive
1417   in
1418
1419   let time2 = Unix.gettimeofday () in
1420   passive_maintainance_time := !passive_maintainance_time +. (time2 -. time1);
1421
1422   kept_clauses := (size_of_passive passive) + (size_of_active active);
1423   match passive_is_empty passive with
1424   | true -> (* ParamodulationFailure *)
1425       given_clause dbd env goals theorems passive active
1426   | false ->
1427       let (sign, current), passive = select env (fst goals) passive active in
1428       let time1 = Unix.gettimeofday () in
1429       let res = forward_simplify env (sign, current) ~passive active in
1430       let time2 = Unix.gettimeofday () in
1431       forward_simpl_time := !forward_simpl_time +. (time2 -. time1);
1432       match res with
1433       | None ->
1434           given_clause dbd env goals theorems passive active
1435       | Some (sign, current) ->
1436           if (sign = Negative) && (is_identity env current) then (
1437             debug_print
1438               (lazy (Printf.sprintf "OK!!! %s %s" (string_of_sign sign)
1439                        (string_of_equality ~env current)));
1440             let _, proof, _, _, _  = current in
1441             ParamodulationSuccess (Some proof, env)
1442           ) else (
1443             debug_print
1444               (lazy "\n================================================");
1445             debug_print (lazy (Printf.sprintf "selected: %s %s"
1446                                  (string_of_sign sign)
1447                                  (string_of_equality ~env current)));
1448
1449             let t1 = Unix.gettimeofday () in
1450             let new' = infer env sign current active in
1451             let t2 = Unix.gettimeofday () in
1452             infer_time := !infer_time +. (t2 -. t1);
1453
1454             let res, goal' = contains_empty env new' in
1455             if res then
1456               let proof =
1457                 match goal' with
1458                 | Some goal -> let _, proof, _, _, _ = goal in Some proof
1459                 | None -> None
1460               in
1461               ParamodulationSuccess (proof, env)
1462             else
1463               let t1 = Unix.gettimeofday () in
1464               let new' = forward_simplify_new env new' active in
1465               let t2 = Unix.gettimeofday () in
1466               let _ =
1467                 forward_simpl_new_time :=
1468                   !forward_simpl_new_time +. (t2 -. t1)
1469               in
1470               let active =
1471                 match sign with
1472                 | Negative -> active
1473                 | Positive ->
1474                     let t1 = Unix.gettimeofday () in
1475                     let active, _, newa, _ =
1476                       backward_simplify env ([], [current]) active
1477                     in
1478                     let t2 = Unix.gettimeofday () in
1479                     backward_simpl_time :=
1480                       !backward_simpl_time +. (t2 -. t1);
1481                     match newa with
1482                     | None -> active
1483                     | Some (n, p) ->
1484                         let al, tbl = active in
1485                         let nn = List.map (fun e -> Negative, e) n in
1486                         let pp, tbl =
1487                           List.fold_right
1488                             (fun e (l, t) ->
1489                                (Positive, e)::l,
1490                                Indexing.index tbl e)
1491                             p ([], tbl)
1492                         in
1493                         nn @ al @ pp, tbl
1494               in
1495               match contains_empty env new' with
1496               | false, _ ->
1497                   let active =
1498                     let al, tbl = active in
1499                     match sign with
1500                     | Negative -> (sign, current)::al, tbl
1501                     | Positive ->
1502                         al @ [(sign, current)], Indexing.index tbl current
1503                   in
1504                   let passive = add_to_passive passive new' in
1505                   given_clause dbd env goals theorems passive active
1506               | true, goal ->
1507                   let proof =
1508                     match goal with
1509                     | Some goal ->
1510                         let _, proof, _, _, _ = goal in Some proof
1511                     | None -> None
1512                   in
1513                   ParamodulationSuccess (proof, env)
1514           )
1515 ;;
1516
1517
1518 (** given-clause algorithm with full reduction strategy *)
1519 let rec given_clause_fullred dbd env goals theorems passive active =
1520   let goals = simplify_goals env goals ~passive active in
1521   let ok, goals = activate_goal goals in
1522 (*   let theorems = simplify_theorems env theorems ~passive active in *)
1523   if ok then
1524 (*     let _ = *)
1525 (*       debug_print *)
1526 (*         (lazy *)
1527 (*            (Printf.sprintf "\ngoals = \nactive\n%s\npassive\n%s\n" *)
1528 (*               (print_goals (fst goals)) (print_goals (snd goals)))); *)
1529 (*       let current = List.hd (fst goals) in *)
1530 (*       let p, _, t = List.hd (snd current) in *)
1531 (*       debug_print *)
1532 (*         (lazy *)
1533 (*            (Printf.sprintf "goal activated:\n%s\n%s\n" *)
1534 (*               (CicPp.ppterm t) (string_of_proof p))); *)
1535 (*     in *)
1536     let ok, goals =
1537       apply_goal_to_theorems dbd env theorems ~passive active goals
1538     in
1539     if ok then
1540       let proof =
1541         match (fst goals) with
1542         | (_, [proof, _, _])::_ -> Some proof
1543         | _ -> assert false
1544       in
1545       ParamodulationSuccess (proof, env)
1546     else
1547       given_clause_fullred_aux dbd env goals theorems passive active
1548   else
1549 (*     let ok', theorems = activate_theorem theorems in *)
1550 (*     if ok' then *)
1551 (*       let ok, goals = apply_theorem_to_goals env theorems active goals in *)
1552 (*       if ok then *)
1553 (*         let proof = *)
1554 (*           match (fst goals) with *)
1555 (*           | (_, [proof, _, _])::_ -> Some proof *)
1556 (*           | _ -> assert false *)
1557 (*         in *)
1558 (*         ParamodulationSuccess (proof, env) *)
1559 (*       else *)
1560 (*         given_clause_fullred_aux env goals theorems passive active *)
1561 (*     else *)
1562       if (passive_is_empty passive) then ParamodulationFailure
1563       else given_clause_fullred_aux dbd env goals theorems passive active
1564
1565 and given_clause_fullred_aux dbd env goals theorems passive active =
1566   let time1 = Unix.gettimeofday () in
1567
1568   let selection_estimate = get_selection_estimate () in
1569   let kept = size_of_passive passive in
1570   let passive =
1571     if !time_limit = 0. || !processed_clauses = 0 then
1572       passive
1573     else if !elapsed_time > !time_limit then (
1574       debug_print (lazy (Printf.sprintf "Time limit (%.2f) reached: %.2f\n"
1575                            !time_limit !elapsed_time));
1576       make_passive [] []
1577     ) else if kept > selection_estimate then (
1578       debug_print
1579         (lazy (Printf.sprintf ("Too many passive equalities: pruning..." ^^
1580                                  "(kept: %d, selection_estimate: %d)\n")
1581                  kept selection_estimate));
1582       prune_passive selection_estimate active passive
1583     ) else
1584       passive
1585   in
1586
1587   let time2 = Unix.gettimeofday () in
1588   passive_maintainance_time := !passive_maintainance_time +. (time2 -. time1);
1589
1590   kept_clauses := (size_of_passive passive) + (size_of_active active);
1591   match passive_is_empty passive with
1592   | true -> (* ParamodulationFailure *)
1593       given_clause_fullred dbd env goals theorems passive active
1594   | false ->
1595       let (sign, current), passive = select env (fst goals) passive active in
1596       let time1 = Unix.gettimeofday () in
1597       let res = forward_simplify env (sign, current) ~passive active in
1598       let time2 = Unix.gettimeofday () in
1599       forward_simpl_time := !forward_simpl_time +. (time2 -. time1);
1600       match res with
1601       | None ->
1602           given_clause_fullred dbd env goals theorems passive active
1603       | Some (sign, current) ->
1604           if (sign = Negative) && (is_identity env current) then (
1605             debug_print
1606               (lazy (Printf.sprintf "OK!!! %s %s" (string_of_sign sign)
1607                        (string_of_equality ~env current)));
1608             let _, proof, _, _, _ = current in
1609             ParamodulationSuccess (Some proof, env)
1610           ) else (
1611             debug_print
1612               (lazy "\n================================================");
1613             debug_print (lazy (Printf.sprintf "selected: %s %s"
1614                                  (string_of_sign sign)
1615                                  (string_of_equality ~env current)));
1616
1617             let t1 = Unix.gettimeofday () in
1618             let new' = infer env sign current active in
1619             let t2 = Unix.gettimeofday () in
1620             infer_time := !infer_time +. (t2 -. t1);
1621
1622             let active =
1623               if is_identity env current then active
1624               else
1625                 let al, tbl = active in
1626                 match sign with
1627                 | Negative -> (sign, current)::al, tbl
1628                 | Positive ->
1629                     al @ [(sign, current)], Indexing.index tbl current
1630             in
1631             let rec simplify new' active passive =
1632               let t1 = Unix.gettimeofday () in
1633               let new' = forward_simplify_new env new' ~passive active in
1634               let t2 = Unix.gettimeofday () in
1635               forward_simpl_new_time :=
1636                 !forward_simpl_new_time +. (t2 -. t1);
1637               let t1 = Unix.gettimeofday () in
1638               let active, passive, newa, retained =
1639                 backward_simplify env new' ~passive active in
1640               let t2 = Unix.gettimeofday () in
1641               backward_simpl_time := !backward_simpl_time +. (t2 -. t1);
1642               match newa, retained with
1643               | None, None -> active, passive, new'
1644               | Some (n, p), None
1645               | None, Some (n, p) ->
1646                   let nn, np = new' in
1647                   simplify (nn @ n, np @ p) active passive
1648               | Some (n, p), Some (rn, rp) ->
1649                   let nn, np = new' in
1650                   simplify (nn @ n @ rn, np @ p @ rp) active passive
1651             in
1652             let active, passive, new' = simplify new' active passive in
1653
1654             let k = size_of_passive passive in
1655             if k < (kept - 1) then
1656               processed_clauses := !processed_clauses + (kept - 1 - k);
1657
1658             let _ =
1659               debug_print
1660                 (lazy
1661                    (Printf.sprintf "active:\n%s\n"
1662                       (String.concat "\n"
1663                          ((List.map
1664                              (fun (s, e) -> (string_of_sign s) ^ " " ^
1665                                 (string_of_equality ~env e))
1666                              (fst active))))))
1667             in
1668             let _ =
1669               match new' with
1670               | neg, pos ->
1671                   debug_print
1672                     (lazy
1673                        (Printf.sprintf "new':\n%s\n"
1674                           (String.concat "\n"
1675                              ((List.map
1676                                  (fun e -> "Negative " ^
1677                                     (string_of_equality ~env e)) neg) @
1678                                 (List.map
1679                                    (fun e -> "Positive " ^
1680                                       (string_of_equality ~env e)) pos)))))
1681             in
1682             match contains_empty env new' with
1683             | false, _ ->
1684                 let passive = add_to_passive passive new' in
1685                 given_clause_fullred dbd env goals theorems passive active
1686             | true, goal ->
1687                 let proof =
1688                   match goal with
1689                   | Some goal -> let _, proof, _, _, _ = goal in Some proof
1690                   | None -> None
1691                 in
1692                 ParamodulationSuccess (proof, env)
1693           )
1694 ;;
1695
1696
1697 let rec saturate_equations env goal accept_fun passive active =
1698   elapsed_time := Unix.gettimeofday () -. !start_time;
1699   if !elapsed_time > !time_limit then
1700     (active, passive)
1701   else
1702     let (sign, current), passive = select env [1, [goal]] passive active in
1703     let res = forward_simplify env (sign, current) ~passive active in
1704     match res with
1705     | None ->
1706         saturate_equations env goal accept_fun passive active
1707     | Some (sign, current) ->
1708         assert (sign = Positive);
1709         debug_print
1710           (lazy "\n================================================");
1711         debug_print (lazy (Printf.sprintf "selected: %s %s"
1712                              (string_of_sign sign)
1713                              (string_of_equality ~env current)));
1714         let new' = infer env sign current active in
1715         let active =
1716           if is_identity env current then active
1717           else
1718             let al, tbl = active in
1719             al @ [(sign, current)], Indexing.index tbl current
1720         in
1721         let rec simplify new' active passive =
1722           let new' = forward_simplify_new env new' ~passive active in
1723           let active, passive, newa, retained =
1724             backward_simplify env new' ~passive active in
1725           match newa, retained with
1726           | None, None -> active, passive, new'
1727           | Some (n, p), None
1728           | None, Some (n, p) ->
1729               let nn, np = new' in
1730               simplify (nn @ n, np @ p) active passive
1731           | Some (n, p), Some (rn, rp) ->
1732               let nn, np = new' in
1733               simplify (nn @ n @ rn, np @ p @ rp) active passive
1734         in
1735         let active, passive, new' = simplify new' active passive in
1736         let _ =
1737           debug_print
1738             (lazy
1739                (Printf.sprintf "active:\n%s\n"
1740                   (String.concat "\n"
1741                      ((List.map
1742                          (fun (s, e) -> (string_of_sign s) ^ " " ^
1743                             (string_of_equality ~env e))
1744                          (fst active))))))
1745         in
1746         let _ =
1747           match new' with
1748           | neg, pos ->
1749               debug_print
1750                 (lazy
1751                    (Printf.sprintf "new':\n%s\n"
1752                       (String.concat "\n"
1753                          ((List.map
1754                              (fun e -> "Negative " ^
1755                                 (string_of_equality ~env e)) neg) @
1756                             (List.map
1757                                (fun e -> "Positive " ^
1758                                   (string_of_equality ~env e)) pos)))))
1759         in
1760         let new' = match new' with _, pos -> [], List.filter accept_fun pos in
1761         let passive = add_to_passive passive new' in
1762         saturate_equations env goal accept_fun passive active
1763 ;;
1764
1765
1766
1767
1768 let main dbd full term metasenv ugraph =
1769   let module C = Cic in
1770   let module T = CicTypeChecker in
1771   let module PET = ProofEngineTypes in
1772   let module PP = CicPp in
1773   let proof = None, (1, [], term)::metasenv, C.Meta (1, []), term in
1774   let status = PET.apply_tactic (PrimitiveTactics.intros_tac ()) (proof, 1) in
1775   let proof, goals = status in
1776   let goal' = List.nth goals 0 in
1777   let _, metasenv, meta_proof, _ = proof in
1778   let _, context, goal = CicUtil.lookup_meta goal' metasenv in
1779   let eq_indexes, equalities, maxm = find_equalities context proof in
1780   let lib_eq_uris, library_equalities, maxm =
1781     find_library_equalities dbd context (proof, goal') (maxm+2)
1782   in
1783   let library_equalities = List.map snd library_equalities in
1784   maxmeta := maxm+2; (* TODO ugly!! *)
1785   let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
1786   let new_meta_goal, metasenv, type_of_goal =
1787     let _, context, ty = CicUtil.lookup_meta goal' metasenv in
1788     debug_print
1789       (lazy
1790          (Printf.sprintf "\n\nTIPO DEL GOAL: %s\n\n" (CicPp.ppterm ty)));
1791     Cic.Meta (maxm+1, irl),
1792     (maxm+1, context, ty)::metasenv,
1793     ty
1794   in
1795   let env = (metasenv, context, ugraph) in
1796   let t1 = Unix.gettimeofday () in
1797   let theorems =
1798     if full then
1799       let theorems = find_library_theorems dbd env (proof, goal') lib_eq_uris in
1800       let context_hyp = find_context_hypotheses env eq_indexes in
1801       context_hyp @ theorems, []
1802     else
1803       let refl_equal =
1804         let us = UriManager.string_of_uri (LibraryObjects.eq_URI ()) in
1805         UriManager.uri_of_string (us ^ "#xpointer(1/1/1)")
1806       in
1807       let t = CicUtil.term_of_uri refl_equal in
1808       let ty, _ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in
1809       [(t, ty, [])], []
1810   in
1811   let t2 = Unix.gettimeofday () in
1812   debug_print
1813     (lazy
1814        (Printf.sprintf "Time to retrieve theorems: %.9f\n" (t2 -. t1)));
1815   let _ =
1816     debug_print
1817       (lazy
1818          (Printf.sprintf
1819             "Theorems:\n-------------------------------------\n%s\n"
1820             (String.concat "\n"
1821                (List.map
1822                   (fun (t, ty, _) ->
1823                      Printf.sprintf
1824                        "Term: %s, type: %s" (CicPp.ppterm t) (CicPp.ppterm ty))
1825                   (fst theorems)))))
1826   in
1827   (*try*)
1828     let goal = Inference.BasicProof new_meta_goal, [], goal in
1829     let equalities =
1830       let equalities = equalities @ library_equalities in
1831       debug_print
1832         (lazy
1833            (Printf.sprintf "equalities:\n%s\n"
1834               (String.concat "\n"
1835                  (List.map string_of_equality equalities))));
1836       debug_print (lazy "SIMPLYFYING EQUALITIES...");
1837       let rec simpl e others others_simpl =
1838         let active = others @ others_simpl in
1839         let tbl =
1840           List.fold_left
1841             (fun t (_, e) -> Indexing.index t e)
1842              Indexing.empty active
1843         in
1844         let res = forward_simplify env e (active, tbl) in
1845         match others with
1846         | hd::tl -> (
1847             match res with
1848             | None -> simpl hd tl others_simpl
1849             | Some e -> simpl hd tl (e::others_simpl)
1850           )
1851         | [] -> (
1852             match res with
1853             | None -> others_simpl
1854             | Some e -> e::others_simpl
1855           )
1856       in
1857       match equalities with
1858       | [] -> []
1859       | hd::tl ->
1860           let others = List.map (fun e -> (Positive, e)) tl in
1861           let res =
1862             List.rev (List.map snd (simpl (Positive, hd) others []))
1863           in
1864           debug_print
1865             (lazy
1866                (Printf.sprintf "equalities AFTER:\n%s\n"
1867                   (String.concat "\n"
1868                      (List.map string_of_equality res))));
1869           res
1870     in
1871     let active = make_active () in
1872     let passive = make_passive [] equalities in
1873     Printf.printf "\ncurrent goal: %s\n"
1874       (let _, _, g = goal in CicPp.ppterm g);
1875     Printf.printf "\ncontext:\n%s\n" (PP.ppcontext context);
1876     Printf.printf "\nmetasenv:\n%s\n" (print_metasenv metasenv);
1877     Printf.printf "\nequalities:\n%s\n"
1878       (String.concat "\n"
1879          (List.map
1880             (string_of_equality ~env) equalities));
1881 (*             (equalities @ library_equalities))); *)
1882       print_endline "--------------------------------------------------";
1883       let start = Unix.gettimeofday () in
1884       print_endline "GO!";
1885       start_time := Unix.gettimeofday ();
1886       let res =
1887         let goals = make_goals goal in
1888         (if !use_fullred then given_clause_fullred else given_clause)
1889           dbd env goals theorems passive active
1890       in
1891       let finish = Unix.gettimeofday () in
1892       let _ =
1893         match res with
1894         | ParamodulationFailure ->
1895             Printf.printf "NO proof found! :-(\n\n"
1896         | ParamodulationSuccess (Some proof, env) ->
1897             let proof = Inference.build_proof_term proof in
1898             Printf.printf "OK, found a proof!\n";
1899             (* REMEMBER: we have to instantiate meta_proof, we should use
1900                apply  the "apply" tactic to proof and status
1901             *)
1902             let names = names_of_context context in
1903             print_endline (PP.pp proof names);
1904             let newmetasenv =
1905               List.fold_left
1906                 (fun m (_, _, _, menv, _) -> m @ menv) metasenv equalities
1907             in
1908             let _ =
1909               (*try*)
1910                 let ty, ug =
1911                   CicTypeChecker.type_of_aux' newmetasenv context proof ugraph
1912                 in
1913                 print_endline (string_of_float (finish -. start));
1914                 Printf.printf
1915                   "\nGOAL was: %s\nPROOF has type: %s\nconvertible?: %s\n\n"
1916                   (CicPp.pp type_of_goal names) (CicPp.pp ty names)
1917                   (string_of_bool
1918                      (fst (CicReduction.are_convertible
1919                              context type_of_goal ty ug)));
1920               (*with e ->
1921                 Printf.printf "\nEXCEPTION!!! %s\n" (Printexc.to_string e);
1922                 Printf.printf "MAXMETA USED: %d\n" !maxmeta;
1923                 print_endline (string_of_float (finish -. start));*)
1924             in
1925             ()
1926
1927         | ParamodulationSuccess (None, env) ->
1928             Printf.printf "Success, but no proof?!?\n\n"
1929       in
1930       Printf.printf ("infer_time: %.9f\nforward_simpl_time: %.9f\n" ^^
1931                        "forward_simpl_new_time: %.9f\n" ^^
1932                        "backward_simpl_time: %.9f\n")
1933         !infer_time !forward_simpl_time !forward_simpl_new_time
1934         !backward_simpl_time;
1935       Printf.printf "passive_maintainance_time: %.9f\n"
1936         !passive_maintainance_time;
1937       Printf.printf "    successful unification/matching time: %.9f\n"
1938         !Indexing.match_unif_time_ok;
1939       Printf.printf "    failed unification/matching time: %.9f\n"
1940         !Indexing.match_unif_time_no;
1941       Printf.printf "    indexing retrieval time: %.9f\n"
1942         !Indexing.indexing_retrieval_time;
1943       Printf.printf "    demodulate_term.build_newtarget_time: %.9f\n"
1944         !Indexing.build_newtarget_time;
1945       Printf.printf "derived %d clauses, kept %d clauses.\n"
1946         !derived_clauses !kept_clauses;
1947 (*
1948   with exc ->
1949     print_endline ("EXCEPTION: " ^ (Printexc.to_string exc));
1950     raise exc
1951 *)
1952 ;;
1953
1954
1955 let default_depth = !maxdepth
1956 and default_width = !maxwidth;;
1957
1958 let reset_refs () =
1959   maxmeta := 0;
1960   symbols_counter := 0;
1961   weight_age_counter := !weight_age_ratio;
1962   processed_clauses := 0;
1963   start_time := 0.;
1964   elapsed_time := 0.;
1965   maximal_retained_equality := None;
1966   infer_time := 0.;
1967   forward_simpl_time := 0.;
1968   forward_simpl_new_time := 0.;
1969   backward_simpl_time := 0.;
1970   passive_maintainance_time := 0.;
1971   derived_clauses := 0;
1972   kept_clauses := 0;
1973 ;;
1974
1975 let saturate
1976     dbd ?(full=false) ?(depth=default_depth) ?(width=default_width) status =
1977   let module C = Cic in
1978   reset_refs ();
1979   Indexing.init_index ();
1980   maxdepth := depth;
1981   maxwidth := width;
1982   let proof, goal = status in
1983   let goal' = goal in
1984   let uri, metasenv, meta_proof, term_to_prove = proof in
1985   let _, context, goal = CicUtil.lookup_meta goal' metasenv in
1986   let eq_indexes, equalities, maxm = find_equalities context proof in
1987   let new_meta_goal, metasenv, type_of_goal =
1988     let irl =
1989       CicMkImplicit.identity_relocation_list_for_metavariable context in
1990     let _, context, ty = CicUtil.lookup_meta goal' metasenv in
1991     debug_print
1992       (lazy (Printf.sprintf "\n\nTIPO DEL GOAL: %s\n" (CicPp.ppterm ty)));
1993     Cic.Meta (maxm+1, irl),
1994     (maxm+1, context, ty)::metasenv,
1995     ty
1996   in
1997   let ugraph = CicUniv.empty_ugraph in
1998   let env = (metasenv, context, ugraph) in
1999   let goal = Inference.BasicProof new_meta_goal, [], goal in
2000   let res, time =
2001     let t1 = Unix.gettimeofday () in
2002     let lib_eq_uris, library_equalities, maxm =
2003       find_library_equalities dbd context (proof, goal') (maxm+2)
2004     in
2005     let library_equalities = List.map snd library_equalities in
2006     let t2 = Unix.gettimeofday () in
2007     maxmeta := maxm+2;
2008     let equalities =
2009       let equalities = equalities @ library_equalities in
2010       debug_print
2011         (lazy
2012            (Printf.sprintf "equalities:\n%s\n"
2013               (String.concat "\n"
2014                  (List.map string_of_equality equalities))));
2015       debug_print (lazy "SIMPLYFYING EQUALITIES...");
2016       let rec simpl e others others_simpl =
2017         let active = others @ others_simpl in
2018         let tbl =
2019           List.fold_left
2020             (fun t (_, e) -> Indexing.index t e)
2021              Indexing.empty active
2022         in
2023         let res = forward_simplify env e (active, tbl) in
2024         match others with
2025         | hd::tl -> (
2026             match res with
2027             | None -> simpl hd tl others_simpl
2028             | Some e -> simpl hd tl (e::others_simpl)
2029           )
2030         | [] -> (
2031             match res with
2032             | None -> others_simpl
2033             | Some e -> e::others_simpl
2034           )
2035       in
2036       match equalities with
2037       | [] -> []
2038       | hd::tl ->
2039           let others = List.map (fun e -> (Positive, e)) tl in
2040           let res =
2041             List.rev (List.map snd (simpl (Positive, hd) others []))
2042           in
2043           debug_print
2044             (lazy
2045                (Printf.sprintf "equalities AFTER:\n%s\n"
2046                   (String.concat "\n"
2047                      (List.map string_of_equality res))));
2048           res
2049     in
2050     debug_print
2051       (lazy
2052          (Printf.sprintf "Time to retrieve equalities: %.9f\n" (t2 -. t1)));
2053     let t1 = Unix.gettimeofday () in
2054     let theorems =
2055       if full then
2056         let thms = find_library_theorems dbd env (proof, goal') lib_eq_uris in
2057         let context_hyp = find_context_hypotheses env eq_indexes in
2058         context_hyp @ thms, []
2059       else
2060         let refl_equal =
2061           let us = UriManager.string_of_uri (LibraryObjects.eq_URI ()) in
2062           UriManager.uri_of_string (us ^ "#xpointer(1/1/1)")
2063         in
2064         let t = CicUtil.term_of_uri refl_equal in
2065         let ty, _ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in
2066         [(t, ty, [])], []
2067     in
2068     let t2 = Unix.gettimeofday () in
2069     let _ =
2070       debug_print
2071         (lazy
2072            (Printf.sprintf
2073               "Theorems:\n-------------------------------------\n%s\n"
2074               (String.concat "\n"
2075                  (List.map
2076                     (fun (t, ty, _) ->
2077                        Printf.sprintf
2078                          "Term: %s, type: %s"
2079                          (CicPp.ppterm t) (CicPp.ppterm ty))
2080                     (fst theorems)))));
2081       debug_print
2082         (lazy
2083            (Printf.sprintf "Time to retrieve theorems: %.9f\n" (t2 -. t1)));
2084     in
2085     let active = make_active () in
2086     let passive = make_passive [] equalities in
2087     let start = Unix.gettimeofday () in
2088     let res =
2089       let goals = make_goals goal in
2090       given_clause_fullred dbd env goals theorems passive active
2091     in
2092     let finish = Unix.gettimeofday () in
2093     (res, finish -. start)
2094   in
2095   match res with
2096   | ParamodulationSuccess (Some proof, env) ->
2097       debug_print (lazy "OK, found a proof!");
2098       let proof = Inference.build_proof_term proof in
2099       let names = names_of_context context in
2100       let newmetasenv =
2101         let i1 =
2102           match new_meta_goal with
2103           | C.Meta (i, _) -> i | _ -> assert false
2104         in
2105         List.filter (fun (i, _, _) -> i <> i1 && i <> goal') metasenv
2106       in
2107       let newstatus =
2108         try
2109           let ty, ug =
2110             CicTypeChecker.type_of_aux' newmetasenv context proof ugraph
2111           in
2112           debug_print (lazy (CicPp.pp proof [](* names *)));
2113           debug_print
2114             (lazy
2115                (Printf.sprintf
2116                   "\nGOAL was: %s\nPROOF has type: %s\nconvertible?: %s\n"
2117                   (CicPp.pp type_of_goal names) (CicPp.pp ty names)
2118                   (string_of_bool
2119                      (fst (CicReduction.are_convertible
2120                              context type_of_goal ty ug)))));
2121           let equality_for_replace i t1 =
2122             match t1 with
2123             | C.Meta (n, _) -> n = i
2124             | _ -> false
2125           in
2126           let real_proof =
2127             ProofEngineReduction.replace
2128               ~equality:equality_for_replace
2129               ~what:[goal'] ~with_what:[proof]
2130               ~where:meta_proof
2131           in
2132           debug_print
2133             (lazy
2134                (Printf.sprintf "status:\n%s\n%s\n%s\n%s\n"
2135                   (match uri with Some uri -> UriManager.string_of_uri uri
2136                    | None -> "")
2137                   (print_metasenv newmetasenv)
2138                   (CicPp.pp real_proof [](* names *))
2139                   (CicPp.pp term_to_prove names)));
2140           ((uri, newmetasenv, real_proof, term_to_prove), [])
2141         with CicTypeChecker.TypeCheckerFailure _ ->
2142           debug_print (lazy "THE PROOF DOESN'T TYPECHECK!!!");
2143           debug_print (lazy (CicPp.pp proof names));
2144           raise (ProofEngineTypes.Fail
2145                   (lazy "Found a proof, but it doesn't typecheck"))
2146       in
2147       debug_print (lazy (Printf.sprintf "\nTIME NEEDED: %.9f" time));
2148       newstatus
2149   | _ ->
2150       raise (ProofEngineTypes.Fail (lazy "NO proof found"))
2151 ;;
2152
2153 (* dummy function called within matita to trigger linkage *)
2154 let init () = ();;
2155
2156
2157 let retrieve_and_print dbd term metasenv ugraph =
2158   let module C = Cic in
2159   let module T = CicTypeChecker in
2160   let module PET = ProofEngineTypes in
2161   let module PP = CicPp in
2162   let proof = None, (1, [], term)::metasenv, C.Meta (1, []), term in
2163   let status = PET.apply_tactic (PrimitiveTactics.intros_tac ()) (proof, 1) in
2164   let proof, goals = status in
2165   let goal' = List.nth goals 0 in
2166   let uri, metasenv, meta_proof, term_to_prove = proof in
2167   let _, context, goal = CicUtil.lookup_meta goal' metasenv in
2168   let eq_indexes, equalities, maxm = find_equalities context proof in
2169   let new_meta_goal, metasenv, type_of_goal =
2170     let irl =
2171       CicMkImplicit.identity_relocation_list_for_metavariable context in
2172     let _, context, ty = CicUtil.lookup_meta goal' metasenv in
2173     debug_print
2174       (lazy (Printf.sprintf "\n\nTIPO DEL GOAL: %s\n" (CicPp.ppterm ty)));
2175     Cic.Meta (maxm+1, irl),
2176     (maxm+1, context, ty)::metasenv,
2177     ty
2178   in
2179   let ugraph = CicUniv.empty_ugraph in
2180   let env = (metasenv, context, ugraph) in
2181   let t1 = Unix.gettimeofday () in
2182   let lib_eq_uris, library_equalities, maxm =
2183     find_library_equalities dbd context (proof, goal') (maxm+2) in
2184   let t2 = Unix.gettimeofday () in
2185   maxmeta := maxm+2;
2186   let equalities = (* equalities @ *) library_equalities in
2187   debug_print
2188      (lazy
2189         (Printf.sprintf "\n\nequalities:\n%s\n"
2190            (String.concat "\n"
2191               (List.map
2192           (fun (u, e) ->
2193 (*               Printf.sprintf "%s: %s" *)
2194                    (UriManager.string_of_uri u)
2195 (*                 (string_of_equality e) *)
2196                      )
2197           equalities))));
2198   debug_print (lazy "SIMPLYFYING EQUALITIES...");
2199   let rec simpl e others others_simpl =
2200     let (u, e) = e in
2201     let active = List.map (fun (u, e) -> (Positive, e))
2202       (others @ others_simpl) in
2203     let tbl =
2204       List.fold_left
2205         (fun t (_, e) -> Indexing.index t e)
2206         Indexing.empty active
2207     in
2208     let res = forward_simplify env (Positive, e) (active, tbl) in
2209     match others with
2210         | hd::tl -> (
2211             match res with
2212               | None -> simpl hd tl others_simpl
2213               | Some e -> simpl hd tl ((u, (snd e))::others_simpl)
2214           )
2215         | [] -> (
2216             match res with
2217               | None -> others_simpl
2218               | Some e -> (u, (snd e))::others_simpl
2219           )
2220   in
2221   let _equalities =
2222     match equalities with
2223       | [] -> []
2224       | hd::tl ->
2225           let others = tl in (* List.map (fun e -> (Positive, e)) tl in *)
2226           let res =
2227             List.rev (simpl (*(Positive,*) hd others [])
2228           in
2229             debug_print
2230               (lazy
2231                  (Printf.sprintf "\nequalities AFTER:\n%s\n"
2232                     (String.concat "\n"
2233                        (List.map
2234                           (fun (u, e) ->
2235                              Printf.sprintf "%s: %s"
2236                                (UriManager.string_of_uri u)
2237                                (string_of_equality e)
2238                           )
2239                           res))));
2240             res in
2241     debug_print
2242       (lazy
2243          (Printf.sprintf "Time to retrieve equalities: %.9f\n" (t2 -. t1)))
2244 ;;
2245
2246
2247 let main_demod_equalities dbd term metasenv ugraph =
2248   let module C = Cic in
2249   let module T = CicTypeChecker in
2250   let module PET = ProofEngineTypes in
2251   let module PP = CicPp in
2252   let proof = None, (1, [], term)::metasenv, C.Meta (1, []), term in
2253   let status = PET.apply_tactic (PrimitiveTactics.intros_tac ()) (proof, 1) in
2254   let proof, goals = status in
2255   let goal' = List.nth goals 0 in
2256   let _, metasenv, meta_proof, _ = proof in
2257   let _, context, goal = CicUtil.lookup_meta goal' metasenv in
2258   let eq_indexes, equalities, maxm = find_equalities context proof in
2259   let lib_eq_uris, library_equalities, maxm =
2260     find_library_equalities dbd context (proof, goal') (maxm+2)
2261   in
2262   let library_equalities = List.map snd library_equalities in
2263   maxmeta := maxm+2; (* TODO ugly!! *)
2264   let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
2265   let new_meta_goal, metasenv, type_of_goal =
2266     let _, context, ty = CicUtil.lookup_meta goal' metasenv in
2267     debug_print
2268       (lazy
2269          (Printf.sprintf "\n\nTRYING TO INFER EQUALITIES MATCHING: %s\n\n"
2270             (CicPp.ppterm ty)));
2271     Cic.Meta (maxm+1, irl),
2272     (maxm+1, context, ty)::metasenv,
2273     ty
2274   in
2275   let env = (metasenv, context, ugraph) in
2276   (*try*)
2277     let goal = Inference.BasicProof new_meta_goal, [], goal in
2278     let equalities =
2279       let equalities = equalities @ library_equalities in
2280       debug_print
2281         (lazy
2282            (Printf.sprintf "equalities:\n%s\n"
2283               (String.concat "\n"
2284                  (List.map string_of_equality equalities))));
2285       debug_print (lazy "SIMPLYFYING EQUALITIES...");
2286       let rec simpl e others others_simpl =
2287         let active = others @ others_simpl in
2288         let tbl =
2289           List.fold_left
2290             (fun t (_, e) -> Indexing.index t e)
2291             Indexing.empty active
2292         in
2293         let res = forward_simplify env e (active, tbl) in
2294         match others with
2295         | hd::tl -> (
2296             match res with
2297             | None -> simpl hd tl others_simpl
2298             | Some e -> simpl hd tl (e::others_simpl)
2299           )
2300         | [] -> (
2301             match res with
2302             | None -> others_simpl
2303             | Some e -> e::others_simpl
2304           )
2305       in
2306       match equalities with
2307       | [] -> []
2308       | hd::tl ->
2309           let others = List.map (fun e -> (Positive, e)) tl in
2310           let res =
2311             List.rev (List.map snd (simpl (Positive, hd) others []))
2312           in
2313           debug_print
2314             (lazy
2315                (Printf.sprintf "equalities AFTER:\n%s\n"
2316                   (String.concat "\n"
2317                      (List.map string_of_equality res))));
2318           res
2319     in
2320     let active = make_active () in
2321     let passive = make_passive [] equalities in
2322     Printf.printf "\ncontext:\n%s\n" (PP.ppcontext context);
2323     Printf.printf "\nmetasenv:\n%s\n" (print_metasenv metasenv);
2324     Printf.printf "\nequalities:\n%s\n"
2325       (String.concat "\n"
2326          (List.map
2327             (string_of_equality ~env) equalities));
2328     print_endline "--------------------------------------------------";
2329     print_endline "GO!";
2330     start_time := Unix.gettimeofday ();
2331     if !time_limit < 1. then time_limit := 60.;
2332     let ra, rp =
2333       saturate_equations env goal (fun e -> true) passive active
2334     in
2335
2336     let initial =
2337       List.fold_left (fun s e -> EqualitySet.add e s)
2338         EqualitySet.empty equalities
2339     in
2340     let addfun s e =
2341       if not (EqualitySet.mem e initial) then EqualitySet.add e s else s
2342     in
2343
2344     let passive =
2345       match rp with
2346       | (n, _), (p, _), _ ->
2347           EqualitySet.elements (List.fold_left addfun EqualitySet.empty p)
2348     in
2349     let active =
2350       let l = List.map snd (fst ra) in
2351       EqualitySet.elements (List.fold_left addfun EqualitySet.empty l)
2352     in
2353     Printf.printf "\n\nRESULTS:\nActive:\n%s\n\nPassive:\n%s\n"
2354        (String.concat "\n" (List.map (string_of_equality ~env) active))
2355      (*  (String.concat "\n"
2356          (List.map (fun e -> CicPp.ppterm (term_of_equality e)) active)) *)
2357 (*       (String.concat "\n" (List.map (string_of_equality ~env) passive)); *)
2358       (String.concat "\n"
2359          (List.map (fun e -> CicPp.ppterm (term_of_equality e)) passive));
2360     print_newline ();
2361 (*
2362   with e ->
2363     debug_print (lazy ("EXCEPTION: " ^ (Printexc.to_string e)))
2364 *)
2365 ;;