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