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