helm/software/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 (* let _profiler = <:profiler<_profiler>>;; *)
  27
  28 (* $Id$ *)
  29
  30 (* set to false to disable paramodulation inside auto_tac *)
  31
  32 let connect_to_auto = true;;
  33
  34 let debug_print = Utils.debug_print;;
  35
  36 (* profiling statistics... *)
  37 let infer_time = ref 0.;;
  38 let forward_simpl_time = ref 0.;;
  39 let forward_simpl_new_time = ref 0.;;
  40 let backward_simpl_time = ref 0.;;
  41 let passive_maintainance_time = ref 0.;;
  42
  43 (* limited-resource-strategy related globals *)
  44 let processed_clauses = ref 0;; (* number of equalities selected so far... *)
  45 let time_limit = ref 0.;; (* in seconds, settable by the user... *)
  46 let start_time = ref 0.;; (* time at which the execution started *)
  47 let elapsed_time = ref 0.;;
  48 (* let maximal_weight = ref None;; *)
  49 let maximal_retained_equality = ref None;;
  50
  51 (* equality-selection related globals *)
  52 let use_fullred = ref true;;
  53 let weight_age_ratio = ref 6 (* 5 *);; (* settable by the user *)
  54 let weight_age_counter = ref !weight_age_ratio ;;
  55 let symbols_ratio = ref 0 (* 3 *);;
  56 let symbols_counter = ref 0;;
  57
  58 (* non-recursive Knuth-Bendix term ordering by default *)
  59 (* Utils.compare_terms := Utils.rpo;; *)
  60 (* Utils.compare_terms := Utils.nonrec_kbo;; *)
  61 (* Utils.compare_terms := Utils.ao;; *)
  62
  63 (* statistics... *)
  64 let derived_clauses = ref 0;;
  65 let kept_clauses = ref 0;;
  66
  67 (* varbiables controlling the search-space *)
  68 let maxdepth = ref 3;;
  69 let maxwidth = ref 3;;
  70
  71 type theorem = Cic.term * Cic.term * Cic.metasenv;;
  72
  73 let symbols_of_equality equality =
  74   let (_, _, (_, left, right, _), _,_) = Equality.open_equality equality in
  75   let m1 = Utils.symbols_of_term left in
  76   let m =
  77     Utils.TermMap.fold
  78       (fun k v res ->
  79          try
  80            let c = Utils.TermMap.find k res in
  81            Utils.TermMap.add k (c+v) res
  82          with Not_found ->
  83            Utils.TermMap.add k v res)
  84       (Utils.symbols_of_term right) m1
  85   in
  86   m
  87 ;;
  88
  89 (* griggio *)
  90 module OrderedEquality = struct
  91   type t = Equality.equality
  92
  93   let compare eq1 eq2 =
  94     match Equality.meta_convertibility_eq eq1 eq2 with
  95     | true -> 0
  96     | false ->
  97         let w1, _, (ty,left, right, _), m1,_ = Equality.open_equality eq1 in
  98         let w2, _, (ty',left', right', _), m2,_ = Equality.open_equality eq2 in
  99         match Pervasives.compare w1 w2 with
 100         | 0 ->
 101             let res = (List.length m1) - (List.length m2) in
 102             if res <> 0 then res else
 103               Equality.compare eq1 eq2
 104         | res -> res
 105 end
 106
 107 module EqualitySet = Set.Make(OrderedEquality);;
 108
 109 type passive_table = Equality.equality list * EqualitySet.t
 110 type active_table = Equality.equality list * Indexing.Index.t
 111 type new_proof =
 112   Equality.goal_proof * Equality.proof * int * Subst.substitution * Cic.metasenv
 113 type result =
 114   | ParamodulationFailure of
 115       string * active_table * passive_table * Equality.equality_bag
 116   | ParamodulationSuccess of
 117       new_proof * active_table * passive_table * Equality.equality_bag
 118 ;;
 119
 120 let list_of_passive (l,s) = l ;;
 121 let list_of_active (l,s) = l ;;
 122
 123 let make_passive eq_list =
 124   let set =
 125     List.fold_left (fun s e -> EqualitySet.add e s) EqualitySet.empty eq_list
 126   in
 127   (* we have the invariant that the list and the set have the same
 128    * cardinality *)
 129   EqualitySet.elements set, set
 130 ;;
 131
 132 let make_empty_active () = [], Indexing.empty ;;
 133 let make_active eq_list =
 134   eq_list, List.fold_left Indexing.index Indexing.empty eq_list
 135 ;;
 136
 137 let size_of_passive (passive_list, _) = List.length passive_list;;
 138 let size_of_active (active_list, _) = List.length active_list;;
 139
 140 let passive_is_empty = function
 141   | [], s when EqualitySet.is_empty s -> true
 142   | [], s -> assert false (* the set and the list should be in sync *)
 143   | _ -> false
 144 ;;
 145
 146 type goals = Equality.goal list * Equality.goal list
 147
 148 let no_more_passive_goals g = match g with | _,[] -> true | _ -> false;;
 149
 150
 151 let age_factor = 0.01;;
 152
 153 (**
 154    selects one equality from passive. The selection strategy is a combination
 155    of weight, age and goal-similarity
 156 *)
 157
 158 let rec select env g passive =
 159   processed_clauses := !processed_clauses + 1;
 160 (*
 161   let goal =
 162     match (List.rev goals) with goal::_ -> goal | _ -> assert false
 163   in
 164 *)
 165   let pos_list, pos_set = passive in
 166   let remove eq l = List.filter (fun e -> Equality.compare e eq <> 0) l in
 167   if !weight_age_ratio > 0 then
 168     weight_age_counter := !weight_age_counter - 1;
 169   match !weight_age_counter with
 170   | 0 -> (
 171       weight_age_counter := !weight_age_ratio;
 172       let skip_giant pos_list pos_set =
 173         match pos_list with
 174           | (hd:EqualitySet.elt)::tl ->
 175               let w,_,_,_,_ = Equality.open_equality hd in
 176                 if w < 30 then
 177                   hd, (tl, EqualitySet.remove hd pos_set)
 178                 else
 179 (*
 180                   (prerr_endline
 181                     ("+++ skipping giant of size "^string_of_int w^" +++");
 182 *)
 183                   select env g (tl@[hd],pos_set)
 184           | _ -> assert false
 185                    in
 186                     skip_giant pos_list pos_set)
 187
 188 (*
 189       let rec skip_giant pos_list pos_set =
 190         match pos_list with
 191           | (hd:EqualitySet.elt)::tl ->
 192               let w,_,_,_,_ = Equality.open_equality hd in
 193               let pos_set = EqualitySet.remove hd pos_set in
 194                 if w < 30 then
 195                   hd, (tl, pos_set)
 196                 else
 197                   (prerr_endline
 198                     ("+++ skipping giant of size "^string_of_int w^" +++");
 199                   skip_giant tl pos_set)
 200           | _ -> assert false
 201       in
 202   skip_giant pos_list pos_set)
 203
 204 *)
 205 (*
 206   | _ when (!symbols_counter > 0) ->
 207      (symbols_counter := !symbols_counter - 1;
 208       let cardinality map =
 209         Utils.TermMap.fold (fun k v res -> res + v) map 0
 210       in
 211       let symbols =
 212         let _, _, term = goal in
 213         Utils.symbols_of_term term
 214       in
 215       let card = cardinality symbols in
 216       let foldfun k v (r1, r2) =
 217         if Utils.TermMap.mem k symbols then
 218           let c = Utils.TermMap.find k symbols in
 219           let c1 = abs (c - v) in
 220           let c2 = v - c1 in
 221           r1 + c2, r2 + c1
 222         else
 223           r1, r2 + v
 224       in
 225       let f equality (i, e) =
 226         let common, others =
 227           Utils.TermMap.fold foldfun (symbols_of_equality equality) (0, 0)
 228         in
 229         let c = others + (abs (common - card)) in
 230         if c < i then (c, equality)
 231         else (i, e)
 232       in
 233       let e1 = EqualitySet.min_elt pos_set in
 234       let initial =
 235         let common, others =
 236           Utils.TermMap.fold foldfun (symbols_of_equality e1) (0, 0)
 237         in
 238         (others + (abs (common - card))), e1
 239       in
 240       let _, current = EqualitySet.fold f pos_set initial in
 241         current,
 242       (remove current pos_list, EqualitySet.remove current pos_set))
 243 *)
 244   | _ ->
 245       symbols_counter := !symbols_ratio;
 246       let my_min e1 e2 =
 247         let w1,_,_,_,_ = Equality.open_equality e1 in
 248         let w2,_,_,_,_ = Equality.open_equality e2 in
 249         if w1 < w2 then e1 else e2
 250       in
 251       let rec my_min_elt min = function
 252         | [] -> min
 253         | hd::tl -> my_min_elt (my_min hd min) tl
 254       in
 255 (*     let current = EqualitySet.min_elt pos_set in  *)
 256        let current = my_min_elt (List.hd pos_list) (List.tl pos_list) in
 257        current,(remove current pos_list, EqualitySet.remove current pos_set)
 258 ;;
 259
 260
 261 let filter_dependent bag passive id =
 262   let pos_list, pos_set = passive in
 263   let passive,no_pruned =
 264     List.fold_right
 265       (fun eq ((list,set),no) ->
 266          if Equality.depend bag eq id then
 267            (list, EqualitySet.remove eq set), no + 1
 268          else
 269            (eq::list, set), no)
 270       pos_list (([],pos_set),0)
 271   in
 272 (*
 273   if no_pruned > 0 then
 274     prerr_endline ("+++ pruning "^ string_of_int no_pruned ^" passives +++");
 275 *)
 276   passive
 277 ;;
 278
 279
 280 (* adds to passive a list of equalities new_pos *)
 281 let add_to_passive passive new_pos preferred =
 282   let pos_list, pos_set = passive in
 283   let ok set equality = not (EqualitySet.mem equality set) in
 284   let pos = List.filter (ok pos_set) new_pos in
 285   let add set equalities =
 286     List.fold_left (fun s e -> EqualitySet.add e s) set equalities
 287   in
 288   let pos_head, pos_tail =
 289     List.partition
 290       (fun e -> List.exists (fun x -> Equality.compare x e = 0) preferred)
 291       pos
 292   in
 293   pos_head @ pos_list @ pos_tail, add pos_set pos
 294 ;;
 295
 296 (* TODO *)
 297 (* removes from passive equalities that are estimated impossible to activate
 298    within the current time limit *)
 299 let prune_passive howmany (active, _) passive =
 300   let (pl, ps), tbl = passive in
 301   let howmany = float_of_int howmany
 302   and ratio = float_of_int !weight_age_ratio in
 303   let round v =
 304     let t = ceil v in
 305     int_of_float (if t -. v < 0.5 then t else v)
 306   in
 307   let in_weight = round (howmany *. ratio /. (ratio +. 1.))
 308   and in_age = round (howmany /. (ratio +. 1.)) in
 309   Utils.debug_print
 310     (lazy (Printf.sprintf "in_weight: %d, in_age: %d\n" in_weight in_age));
 311   let counter = ref !symbols_ratio in
 312   let rec pickw w ps =
 313     if w > 0 then
 314       if !counter > 0 then
 315         let _ =
 316           counter := !counter - 1;
 317           if !counter = 0 then counter := !symbols_ratio in
 318         let e = EqualitySet.min_elt ps in
 319         let ps' = pickw (w-1) (EqualitySet.remove e ps) in
 320           EqualitySet.add e ps'
 321       else
 322         let e = EqualitySet.min_elt ps in
 323         let ps' = pickw (w-1) (EqualitySet.remove e ps) in
 324         EqualitySet.add e ps'
 325     else
 326       EqualitySet.empty
 327   in
 328   let ps = pickw in_weight ps in
 329   let rec picka w s l =
 330     if w > 0 then
 331       match l with
 332       | [] -> w, s, []
 333       | hd::tl when not (EqualitySet.mem hd s) ->
 334           let w, s, l = picka (w-1) s tl in
 335           w, EqualitySet.add hd s, hd::l
 336       | hd::tl ->
 337           let w, s, l = picka w s tl in
 338           w, s, hd::l
 339     else
 340       0, s, l
 341   in
 342   let _, ps, pl = picka in_age ps pl in
 343   if not (EqualitySet.is_empty ps) then
 344     maximal_retained_equality := Some (EqualitySet.max_elt ps);
 345   let tbl =
 346     EqualitySet.fold
 347       (fun e tbl -> Indexing.index tbl e) ps Indexing.empty
 348   in
 349   (pl, ps), tbl
 350 ;;
 351
 352
 353 (** inference of new equalities between current and some in active *)
 354 let infer bag eq_uri env current (active_list, active_table) =
 355   let (_,c,_) = env in
 356   if Utils.debug_metas then
 357     (ignore(Indexing.check_target bag c current "infer1");
 358      ignore(List.map (function current -> Indexing.check_target bag c current "infer2") active_list));
 359   let bag, new_pos =
 360       let bag, copy_of_current = Equality.fix_metas bag current in
 361       let active_table =  Indexing.index active_table copy_of_current in
 362 (*       let _ = <:start<current contro active>> in *)
 363       let bag, res =
 364         Indexing.superposition_right bag eq_uri env active_table current
 365       in
 366 (*       let _ = <:stop<current contro active>> in *)
 367       if Utils.debug_metas then
 368         ignore(List.map
 369                  (function current ->
 370                     Indexing.check_target bag c current "sup0") res);
 371       let rec infer_positive bag table = function
 372         | [] -> bag, []
 373         | equality::tl ->
 374             let bag, res =
 375               Indexing.superposition_right bag
 376                 ~subterms_only:true eq_uri env table equality
 377             in
 378               if Utils.debug_metas then
 379                 ignore
 380                   (List.map
 381                      (function current ->
 382                         Indexing.check_target bag c current "sup2") res);
 383               let bag, pos = infer_positive bag table tl in
 384               bag, res @ pos
 385       in
 386       let curr_table = Indexing.index Indexing.empty current in
 387       let bag, pos = infer_positive bag curr_table ((*copy_of_current::*)active_list) in
 388       if Utils.debug_metas then
 389         ignore(List.map
 390                  (function current ->
 391                     Indexing.check_target bag c current "sup3") pos);
 392       bag, res @ pos
 393   in
 394   derived_clauses := !derived_clauses + (List.length new_pos);
 395   match !maximal_retained_equality with
 396     | None -> bag, new_pos
 397     | Some eq ->
 398       ignore(assert false);
 399       (* if we have a maximal_retained_equality, we can discard all equalities
 400          "greater" than it, as they will never be reached...  An equality is
 401          greater than maximal_retained_equality if it is bigger
 402          wrt. OrderedEquality.compare and it is less similar than
 403          maximal_retained_equality to the current goal *)
 404         bag, List.filter (fun e -> OrderedEquality.compare e eq <= 0) new_pos
 405 ;;
 406
 407 let check_for_deep_subsumption env active_table eq =
 408   let _,_,(eq_ty, left, right, order),metas,id = Equality.open_equality eq in
 409   let check_subsumed deep l r =
 410     let eqtmp =
 411       Equality.mk_tmp_equality(0,(eq_ty,l,r,Utils.Incomparable),metas)in
 412     match Indexing.subsumption env active_table eqtmp with
 413     | None -> false
 414     | Some _ -> true
 415   in
 416   let rec aux b (ok_so_far, subsumption_used) t1 t2  =
 417     match t1,t2 with
 418       | t1, t2 when not ok_so_far -> ok_so_far, subsumption_used
 419       | t1, t2 when subsumption_used -> t1 = t2, subsumption_used
 420       | Cic.Appl (h1::l),Cic.Appl (h2::l') ->
 421           let rc = check_subsumed b t1 t2 in
 422             if rc then
 423               true, true
 424             else if h1 = h2 then
 425               (try
 426                  List.fold_left2
 427                    (fun (ok_so_far, subsumption_used) t t' ->
 428                       aux true (ok_so_far, subsumption_used) t t')
 429                    (ok_so_far, subsumption_used) l l'
 430                with Invalid_argument _ -> false,subsumption_used)
 431             else
 432               false, subsumption_used
 433     | _ -> false, subsumption_used
 434   in
 435   fst (aux false (true,false) left right)
 436 ;;
 437
 438 (** simplifies current using active and passive *)
 439 let forward_simplify bag eq_uri env current (active_list, active_table) =
 440   let _, context, _ = env in
 441   let demodulate bag table current =
 442     let bag, newcurrent =
 443       Indexing.demodulation_equality bag eq_uri env table current
 444     in
 445     bag, if Equality.is_identity env newcurrent then None else Some newcurrent
 446   in
 447   let demod bag current =
 448     if Utils.debug_metas then
 449       ignore (Indexing.check_target bag context current "demod0");
 450     let bag, res = demodulate bag active_table current in
 451     if Utils.debug_metas then
 452       ignore ((function None -> () | Some x ->
 453       ignore (Indexing.check_target bag context x "demod1");()) res);
 454     bag, res
 455   in
 456   let bag, res = demod bag current in
 457   match res with
 458   | None -> bag, None
 459   | Some c ->
 460       if Indexing.in_index active_table c ||
 461          check_for_deep_subsumption env active_table c
 462       then
 463         bag, None
 464       else
 465         bag, res
 466 ;;
 467
 468 (** simplifies new using active and passive *)
 469 let forward_simplify_new bag eq_uri env new_pos active =
 470   if Utils.debug_metas then
 471     begin
 472       let m,c,u = env in
 473         ignore(List.map
 474         (fun current -> Indexing.check_target bag c current "forward new pos")
 475       new_pos;)
 476     end;
 477   let active_list, active_table = active in
 478   let demodulate bag table target =
 479     let bag, newtarget =
 480       Indexing.demodulation_equality bag eq_uri env table target
 481     in
 482     bag, newtarget
 483   in
 484   (* we could also demodulate using passive. Currently we don't *)
 485   let bag, new_pos =
 486     List.fold_right (fun x (bag,acc) ->
 487        let bag, y = demodulate bag active_table x in
 488        bag, y::acc)
 489     new_pos (bag,[])
 490   in
 491   let new_pos_set =
 492     List.fold_left
 493       (fun s e ->
 494          if not (Equality.is_identity env e) then
 495            EqualitySet.add e s
 496          else s)
 497       EqualitySet.empty new_pos
 498   in
 499   let new_pos = EqualitySet.elements new_pos_set in
 500   let subs e = Indexing.subsumption env active_table e = None in
 501   let is_duplicate e = not (Indexing.in_index active_table e) in
 502   bag, List.filter subs (List.filter is_duplicate new_pos)
 503 ;;
 504
 505
 506 (** simplifies a goal with equalities in active and passive *)
 507 let rec simplify_goal bag env goal (active_list, active_table) =
 508   let demodulate table goal = Indexing.demodulation_goal bag env table goal in
 509   let changed, goal = demodulate active_table goal in
 510   changed,
 511   if not changed then
 512     goal
 513   else
 514     snd (simplify_goal bag env goal (active_list, active_table))
 515 ;;
 516
 517
 518 let simplify_goals bag env goals active =
 519   let a_goals, p_goals = goals in
 520   let p_goals = List.map (fun g -> snd (simplify_goal bag env g active)) p_goals in
 521   let a_goals = List.map (fun g -> snd (simplify_goal bag env g active)) a_goals in
 522   a_goals, p_goals
 523 ;;
 524
 525
 526 (** simplifies active usign new *)
 527 let backward_simplify_active
 528   bag eq_uri env new_pos new_table min_weight active
 529 =
 530   let active_list, active_table = active in
 531   let bag, active_list, newa, pruned =
 532     List.fold_right
 533       (fun equality (bag, res, newn,pruned) ->
 534          let ew, _, _, _,id = Equality.open_equality equality in
 535          if ew < min_weight then
 536            bag, equality::res, newn,pruned
 537          else
 538            match
 539              forward_simplify bag eq_uri env equality (new_pos, new_table)
 540            with
 541            | bag, None -> bag, res, newn, id::pruned
 542            | bag, Some e ->
 543                if Equality.compare equality e = 0 then
 544                  bag, e::res, newn, pruned
 545                else
 546                  bag, res, e::newn, pruned)
 547       active_list (bag, [], [],[])
 548   in
 549   let find eq1 where =
 550     List.exists (Equality.meta_convertibility_eq eq1) where
 551   in
 552   let id_of_eq eq =
 553     let _, _, _, _,id = Equality.open_equality eq in id
 554   in
 555   let ((active1,pruned),tbl), newa =
 556     List.fold_right
 557       (fun eq ((res,pruned), tbl) ->
 558          if List.mem eq res then
 559            (res, (id_of_eq eq)::pruned),tbl
 560          else if (Equality.is_identity env eq) || (find eq res) then (
 561            (res, (id_of_eq eq)::pruned),tbl
 562          )
 563          else
 564            (eq::res,pruned), Indexing.index tbl eq)
 565       active_list (([],pruned), Indexing.empty),
 566     List.fold_right
 567       (fun eq p ->
 568          if (Equality.is_identity env eq) then p
 569          else eq::p)
 570       newa []
 571   in
 572   match newa with
 573   | [] -> bag, (active1,tbl), None, pruned
 574   | _ -> bag, (active1,tbl), Some newa, pruned
 575 ;;
 576
 577
 578 (** simplifies passive using new *)
 579 let backward_simplify_passive
 580   bag eq_uri env new_pos new_table min_weight passive
 581 =
 582   let (pl, ps), passive_table = passive in
 583   let f bag equality (resl, ress, newn) =
 584     let ew, _, _, _ , _ = Equality.open_equality equality in
 585     if ew < min_weight then
 586       bag, (equality::resl, ress, newn)
 587     else
 588       match
 589         forward_simplify bag eq_uri env equality (new_pos, new_table)
 590       with
 591       | bag, None ->
 592           bag, (resl, EqualitySet.remove equality ress, newn)
 593       | bag, Some e ->
 594           if equality = e then
 595             bag, (equality::resl, ress, newn)
 596           else
 597             let ress = EqualitySet.remove equality ress in
 598             bag, (resl, ress, e::newn)
 599   in
 600   let bag, (pl, ps, newp) =
 601     List.fold_right (fun x (bag,acc) -> f bag x acc) pl (bag,([], ps, [])) in
 602   let passive_table =
 603     List.fold_left
 604       (fun tbl e -> Indexing.index tbl e) Indexing.empty pl
 605   in
 606   match newp with
 607   | [] -> bag, ((pl, ps), passive_table), None
 608   |  _ -> bag, ((pl, ps), passive_table), Some (newp)
 609 ;;
 610
 611 let build_table equations =
 612     List.fold_left
 613       (fun (l, t, w) e ->
 614          let ew, _, _, _ , _ = Equality.open_equality e in
 615          e::l, Indexing.index t e, min ew w)
 616       ([], Indexing.empty, 1000000) equations
 617 ;;
 618
 619
 620 let backward_simplify bag eq_uri env new' active =
 621   let new_pos, new_table, min_weight = build_table new' in
 622   let bag, active, newa, pruned =
 623     backward_simplify_active bag eq_uri env new_pos new_table min_weight active
 624   in
 625   bag, active, newa, pruned
 626 ;;
 627
 628 let close bag eq_uri env new' given =
 629   let new_pos, new_table, min_weight =
 630     List.fold_left
 631       (fun (l, t, w) e ->
 632          let ew, _, _, _ , _ = Equality.open_equality e in
 633          e::l, Indexing.index t e, min ew w)
 634       ([], Indexing.empty, 1000000) (snd new')
 635   in
 636   List.fold_left
 637     (fun (bag,p) c ->
 638        let bag, pos = infer bag eq_uri env c (new_pos,new_table) in
 639        bag, pos@p)
 640     (bag,[]) given
 641 ;;
 642
 643 let is_commutative_law eq =
 644   let w, proof, (eq_ty, left, right, order), metas , _ =
 645     Equality.open_equality eq
 646   in
 647     match left,right with
 648         Cic.Appl[f1;Cic.Meta _ as a1;Cic.Meta _ as b1],
 649         Cic.Appl[f2;Cic.Meta _ as a2;Cic.Meta _ as b2] ->
 650           f1 = f2 && a1 = b2 && a2 = b1
 651       | _ -> false
 652 ;;
 653
 654 let prova bag eq_uri env new' active =
 655   let given = List.filter is_commutative_law (fst active) in
 656   let _ =
 657     Utils.debug_print
 658       (lazy
 659          (Printf.sprintf "symmetric:\n%s\n"
 660             (String.concat "\n"
 661                (List.map
 662                   (fun e -> Equality.string_of_equality ~env e)
 663                    given)))) in
 664     close bag eq_uri env new' given
 665 ;;
 666
 667 (* returns an estimation of how many equalities in passive can be activated
 668    within the current time limit *)
 669 let get_selection_estimate () =
 670   elapsed_time := (Unix.gettimeofday ()) -. !start_time;
 671   (*   !processed_clauses * (int_of_float (!time_limit /. !elapsed_time)) *)
 672   int_of_float (
 673     ceil ((float_of_int !processed_clauses) *.
 674             ((!time_limit (* *. 2. *)) /. !elapsed_time -. 1.)))
 675 ;;
 676
 677
 678 (** initializes the set of goals *)
 679 let make_goals goal =
 680   let active = []
 681   and passive = [0, [goal]] in
 682   active, passive
 683 ;;
 684
 685 let make_goal_set goal =
 686   ([],[goal])
 687 ;;
 688
 689 (** initializes the set of theorems *)
 690 let make_theorems theorems =
 691   theorems, []
 692 ;;
 693
 694
 695 let activate_goal (active, passive) =
 696   if active = [] then
 697     match passive with
 698     | goal_conj::tl -> true, (goal_conj::active, tl)
 699     | [] -> false, (active, passive)
 700   else
 701     true, (active,passive)
 702 ;;
 703
 704
 705 let activate_theorem (active, passive) =
 706   match passive with
 707   | theorem::tl -> true, (theorem::active, tl)
 708   | [] -> false, (active, passive)
 709 ;;
 710
 711 let rec simpl bag eq_uri env e others others_simpl =
 712   let active = others @ others_simpl in
 713   let tbl =
 714     List.fold_left
 715       (fun t e ->
 716          if Equality.is_identity env e then t else Indexing.index t e)
 717       Indexing.empty active
 718   in
 719   let bag, res =
 720     forward_simplify bag eq_uri env e (active, tbl)
 721   in
 722     match others with
 723       | hd::tl -> (
 724           match res with
 725             | None -> simpl bag eq_uri env hd tl others_simpl
 726             | Some e -> simpl bag eq_uri env hd tl (e::others_simpl)
 727         )
 728       | [] -> (
 729           match res with
 730             | None -> bag, others_simpl
 731             | Some e -> bag, e::others_simpl
 732         )
 733 ;;
 734
 735 let simplify_equalities bag eq_uri env equalities =
 736   Utils.debug_print
 737     (lazy
 738        (Printf.sprintf "equalities:\n%s\n"
 739           (String.concat "\n"
 740              (List.map Equality.string_of_equality equalities))));
 741 Utils.debug_print (lazy "SIMPLYFYING EQUALITIES...");
 742   match equalities with
 743     | [] -> bag, []
 744     | hd::tl ->
 745         let bag, res = simpl bag eq_uri env hd tl [] in
 746         let res = List.rev res in
 747           Utils.debug_print
 748             (lazy
 749                (Printf.sprintf "equalities AFTER:\n%s\n"
 750                   (String.concat "\n"
 751                      (List.map Equality.string_of_equality res))));
 752        bag, res
 753 ;;
 754
 755 let print_goals goals =
 756   (String.concat "\n"
 757      (List.map
 758         (fun (d, gl) ->
 759            let gl' =
 760              List.map
 761                (fun (p, _, t) ->
 762                   (* (string_of_proof p) ^ ", " ^ *) (CicPp.ppterm t)) gl
 763            in
 764            Printf.sprintf "%d: %s" d (String.concat "; " gl')) goals))
 765 ;;
 766
 767 let pp_goal_set msg goals names =
 768   let active_goals, passive_goals = goals in
 769   debug_print (lazy ("////" ^ msg));
 770   debug_print (lazy ("ACTIVE G: " ^
 771     (String.concat "\n " (List.map (fun (_,_,g) -> CicPp.pp g names)
 772     active_goals))));
 773   debug_print (lazy ("PASSIVE G: " ^
 774     (String.concat "\n " (List.map (fun (_,_,g) -> CicPp.pp g names)
 775     passive_goals))))
 776 ;;
 777
 778 let check_if_goal_is_subsumed bag ((_,ctx,_) as env) table (goalproof,menv,ty) =
 779 (*   let names = Utils.names_of_context ctx in *)
 780   match ty with
 781   | Cic.Appl[Cic.MutInd(uri,_,_);eq_ty;left;right]
 782     when LibraryObjects.is_eq_URI uri ->
 783       (let bag, goal_equation =
 784          Equality.mk_equality bag
 785            (0,Equality.Exact (Cic.Implicit None),(eq_ty,left,right,Utils.Eq),menv)
 786       in
 787        match Indexing.subsumption env table goal_equation with
 788        (* match Indexing.unification env table goal_equation with *)
 789         | Some (subst, equality, swapped ) ->
 790 (*
 791             prerr_endline
 792              ("GOAL SUBSUMED IS: "^Equality.string_of_equality goal_equation ~env);
 793             prerr_endline
 794              ("GOAL IS SUBSUMED BY: "^Equality.string_of_equality equality ~env);
 795             prerr_endline ("SUBST:"^Subst.ppsubst ~names subst);
 796 *)
 797             let (_,p,(ty,l,r,_),m,id) = Equality.open_equality equality in
 798             let cicmenv = Subst.apply_subst_metasenv subst (m @ menv) in
 799             let bag, p =
 800               if swapped then
 801                 Equality.symmetric bag eq_ty l id uri m
 802               else
 803                 bag, p
 804             in
 805             bag, Some (goalproof, p, id, subst, cicmenv)
 806         | None ->
 807                         bag, None)
 808   | _ -> bag, None
 809 ;;
 810
 811 let find_all_subsumed bag env table (goalproof,menv,ty) =
 812   match ty with
 813   | Cic.Appl[Cic.MutInd(uri,_,_);eq_ty;left;right]
 814     when LibraryObjects.is_eq_URI uri ->
 815       let bag, goal_equation =
 816         (Equality.mk_equality bag
 817           (0,Equality.Exact (Cic.Implicit None),(eq_ty,left,right,Utils.Eq),menv))
 818       in
 819       List.fold_right
 820           (fun (subst, equality, swapped) (bag,acc) ->
 821              let (_,p,(ty,l,r,_),m,id) = Equality.open_equality equality in
 822              let cicmenv = Subst.apply_subst_metasenv subst (m @ menv) in
 823              Indexing.check_for_duplicates cicmenv "from subsumption";
 824              let bag, p =
 825                if swapped then
 826                  Equality.symmetric bag eq_ty l id uri m
 827                else
 828                  bag, p
 829              in
 830               bag, (goalproof, p, id, subst, cicmenv)::acc)
 831          (Indexing.subsumption_all env table goal_equation) (bag,[])
 832           (* (Indexing.unification_all env table goal_equation) *)
 833   | _ -> assert false
 834 ;;
 835
 836
 837 let check_if_goal_is_identity env = function
 838   | (goalproof,m,Cic.Appl[Cic.MutInd(uri,_,ens);eq_ty;left;right])
 839     when left = right && LibraryObjects.is_eq_URI uri ->
 840       let reflproof = Equality.Exact (Equality.refl_proof uri eq_ty left) in
 841       Some (goalproof, reflproof, 0, Subst.empty_subst,m)
 842   | (goalproof,m,Cic.Appl[Cic.MutInd(uri,_,ens);eq_ty;left;right])
 843     when LibraryObjects.is_eq_URI uri ->
 844     (let _,context,_ = env in
 845     try
 846      let s,m,_ =
 847        Founif.unification [] m context left right CicUniv.empty_ugraph
 848      in
 849       let reflproof = Equality.Exact (Equality.refl_proof uri eq_ty left) in
 850       let m = Subst.apply_subst_metasenv s m in
 851       Some (goalproof, reflproof, 0, s,m)
 852     with CicUnification.UnificationFailure _ -> None)
 853   | _ -> None
 854 ;;
 855
 856 let rec check b goal = function
 857   | [] -> b, None
 858   | f::tl ->
 859       match f b goal with
 860       | b, None -> check b goal tl
 861       | b, (Some _ as ok)  -> b, ok
 862 ;;
 863
 864 let simplify_goal_set bag env goals active =
 865   let active_goals, passive_goals = goals in
 866   let find (_,_,g) where =
 867     List.exists (fun (_,_,g1) -> Equality.meta_convertibility g g1) where
 868   in
 869     (* prova:tengo le passive semplificate
 870   let passive_goals =
 871     List.map (fun g -> snd (simplify_goal env g active)) passive_goals
 872   in *)
 873     List.fold_left
 874       (fun (acc_a,acc_p) goal ->
 875         match simplify_goal bag env goal active with
 876         | changed, g ->
 877             if changed then
 878               if find g acc_p then acc_a,acc_p else acc_a,g::acc_p
 879             else
 880               if find g acc_a then acc_a,acc_p else g::acc_a,acc_p)
 881       ([],passive_goals) active_goals
 882 ;;
 883
 884 let check_if_goals_set_is_solved bag env active goals =
 885   let active_goals, passive_goals = goals in
 886   List.fold_left
 887     (fun (bag, proof) goal ->
 888       match proof with
 889       | Some p -> bag, proof
 890       | None ->
 891           check bag goal [
 892             (fun b x -> b, check_if_goal_is_identity env x);
 893             (fun bag -> check_if_goal_is_subsumed bag env (snd active))])
 894 (* provare active and passive?*)
 895     (bag,None) active_goals
 896 ;;
 897
 898 let infer_goal_set bag env active goals =
 899   let active_goals, passive_goals = goals in
 900   let rec aux bag = function
 901     | [] -> bag, (active_goals, [])
 902     | hd::tl ->
 903         let changed, selected = simplify_goal bag env hd active in
 904         let (_,m1,t1) = selected in
 905         let already_in =
 906           List.exists (fun (_,_,t) -> Equality.meta_convertibility t t1)
 907               active_goals
 908         in
 909         if already_in then
 910              aux bag tl
 911           else
 912             let passive_goals = tl in
 913             let bag, new_passive_goals =
 914               if Utils.metas_of_term t1 = [] then
 915                 bag, passive_goals
 916               else
 917                 let bag, new' =
 918                    Indexing.superposition_left bag env (snd active) selected
 919                 in
 920                 bag, passive_goals @ new'
 921             in
 922             bag, (selected::active_goals, new_passive_goals)
 923   in
 924    aux bag passive_goals
 925 ;;
 926
 927 let infer_goal_set_with_current bag env current goals active =
 928   let active_goals, passive_goals = simplify_goal_set bag env goals active in
 929   let l,table,_  = build_table [current] in
 930   let bag, passive_goals =
 931    List.fold_left
 932     (fun (bag, acc) g ->
 933       let bag, new' = Indexing.superposition_left bag env table g in
 934       bag, acc @ new')
 935     (bag, passive_goals) active_goals
 936   in
 937   bag, active_goals, passive_goals
 938 ;;
 939
 940 let ids_of_goal g =
 941   let p,_,_ = g in
 942   let ids = List.map (fun _,_,i,_,_ -> i) p in
 943   ids
 944 ;;
 945
 946 let ids_of_goal_set (ga,gp) =
 947   List.flatten (List.map ids_of_goal ga) @
 948   List.flatten (List.map ids_of_goal gp)
 949 ;;
 950
 951 let size_of_goal_set_a (l,_) = List.length l;;
 952 let size_of_goal_set_p (_,l) = List.length l;;
 953
 954 let pp_goals label goals context =
 955   let names = Utils.names_of_context context in
 956   List.iter
 957     (fun _,_,g ->
 958       debug_print (lazy
 959         (Printf.sprintf  "Current goal: %s = %s\n" label (CicPp.pp g names))))
 960     (fst goals);
 961   List.iter
 962     (fun _,_,g ->
 963       debug_print (lazy
 964         (Printf.sprintf  "PASSIVE goal: %s = %s\n" label (CicPp.pp g names))))
 965       (snd goals);
 966 ;;
 967
 968 let print_status iterno goals active passive =
 969   debug_print (lazy
 970     (Printf.sprintf "\n%d #ACTIVES: %d #PASSIVES: %d #GOALSET: %d(%d)"
 971       iterno (size_of_active active) (size_of_passive passive)
 972       (size_of_goal_set_a goals) (size_of_goal_set_p goals)))
 973 ;;
 974
 975 let add_to_active_aux bag active passive env eq_uri current =
 976   debug_print (lazy ("Adding to actives : " ^
 977     Equality.string_of_equality ~env  current));
 978   match forward_simplify bag eq_uri env current active with
 979   | bag, None -> None, active, passive, bag
 980   | bag, Some current ->
 981       let bag, new' = infer bag eq_uri env current active in
 982       let active =
 983         let al, tbl = active in
 984         al @ [current], Indexing.index tbl current
 985       in
 986       let rec simplify bag new' active passive =
 987         let bag, new' =
 988           forward_simplify_new bag eq_uri env new' active
 989         in
 990         let bag, active, newa, pruned =
 991           backward_simplify bag eq_uri env new' active
 992         in
 993         let passive =
 994           List.fold_left (filter_dependent bag) passive pruned
 995         in
 996         match newa with
 997         | None -> bag, active, passive, new'
 998         | Some p -> simplify bag (new' @ p) active passive
 999       in
1000       let bag, active, passive, new' =
1001         simplify bag new' active passive
1002       in
1003       let passive = add_to_passive passive new' [] in
1004       Some new', active, passive, bag
1005 ;;
1006
1007 (** given-clause algorithm with full reduction strategy: NEW implementation *)
1008 (* here goals is a set of goals in OR *)
1009 let given_clause
1010   bag eq_uri ((_,context,_) as env) goals passive active
1011   goal_steps saturation_steps max_time
1012 =
1013   let initial_time = Unix.gettimeofday () in
1014   let iterations_left iterno =
1015     let now = Unix.gettimeofday () in
1016     let time_left = max_time -. now in
1017     let time_spent_until_now = now -. initial_time in
1018     let iteration_medium_cost =
1019       time_spent_until_now /. (float_of_int iterno)
1020     in
1021     let iterations_left = time_left /. iteration_medium_cost in
1022     int_of_float iterations_left
1023   in
1024   let rec step bag goals passive active g_iterno s_iterno =
1025     if g_iterno > goal_steps && s_iterno > saturation_steps then
1026       (ParamodulationFailure ("No more iterations to spend",active,passive,bag))
1027     else if Unix.gettimeofday () > max_time then
1028       (ParamodulationFailure ("No more time to spend",active,passive,bag))
1029     else
1030       let _ =
1031          print_status (max g_iterno s_iterno) goals active passive
1032 (*         Printf.eprintf ".%!"; *)
1033       in
1034       (* PRUNING OF PASSIVE THAT WILL NEVER BE PROCESSED *)
1035       let passive =
1036         let selection_estimate = iterations_left (max g_iterno s_iterno) in
1037         let kept = size_of_passive passive in
1038         if kept > selection_estimate then
1039           begin
1040             (*Printf.eprintf "Too many passive equalities: pruning...";
1041             prune_passive selection_estimate active*) passive
1042           end
1043         else
1044           passive
1045       in
1046       kept_clauses := (size_of_passive passive) + (size_of_active active);
1047       let bag, goals =
1048         if g_iterno < goal_steps then
1049           infer_goal_set bag env active goals
1050         else
1051           bag, goals
1052       in
1053       match check_if_goals_set_is_solved bag env active goals with
1054       | bag, Some p ->
1055           debug_print (lazy
1056             (Printf.sprintf "\nFound a proof in: %f\n"
1057               (Unix.gettimeofday() -. initial_time)));
1058           ParamodulationSuccess (p,active,passive,bag)
1059       | bag, None ->
1060           (* SELECTION *)
1061           if passive_is_empty passive then
1062             if no_more_passive_goals goals then
1063               ParamodulationFailure
1064                 ("No more passive equations/goals",active,passive,bag)
1065               (*maybe this is a success! *)
1066             else
1067               step bag goals passive active (g_iterno+1) (s_iterno+1)
1068           else
1069             begin
1070               (* COLLECTION OF GARBAGED EQUALITIES *)
1071               let bag =
1072                 if max g_iterno s_iterno mod 40 = 0 then
1073                   (print_status (max g_iterno s_iterno) goals active passive;
1074                   let active = List.map Equality.id_of (fst active) in
1075                   let passive = List.map Equality.id_of (fst passive) in
1076                   let goal = ids_of_goal_set goals in
1077                   Equality.collect bag active passive goal)
1078                 else
1079                   bag
1080               in
1081               if s_iterno > saturation_steps then
1082                 ParamodulationFailure ("max saturation steps",active,passive,bag)
1083               else
1084                 let current, passive = select env goals passive in
1085                   match add_to_active_aux bag active passive env eq_uri current with
1086                   | None, active, passive, bag ->
1087                       step bag goals passive active (g_iterno+1) (s_iterno+1)
1088                   | Some new', active, passive, bag ->
1089                       let bag, active_goals, passive_goals =
1090                         infer_goal_set_with_current bag env current goals active
1091                       in
1092                       let goals =
1093                         let a,b,_ = build_table new' in
1094                         let rc =
1095                           simplify_goal_set bag env (active_goals,passive_goals) (a,b)
1096                         in
1097                         rc
1098                       in
1099                       step bag goals passive active (g_iterno+1) (s_iterno+1)
1100             end
1101   in
1102     step bag goals passive active 1 1
1103 ;;
1104
1105 let rec saturate_equations bag eq_uri env goal accept_fun passive active =
1106   elapsed_time := Unix.gettimeofday () -. !start_time;
1107   if !elapsed_time > !time_limit then
1108     bag, active, passive
1109   else
1110     let current, passive = select env ([goal],[]) passive in
1111     let bag, res = forward_simplify bag eq_uri env current active in
1112     match res with
1113     | None ->
1114         saturate_equations bag eq_uri env goal accept_fun passive active
1115     | Some current ->
1116         Utils.debug_print (lazy (Printf.sprintf "selected: %s"
1117                              (Equality.string_of_equality ~env current)));
1118         let bag, new' = infer bag eq_uri env current active in
1119         let active =
1120           if Equality.is_identity env current then active
1121           else
1122             let al, tbl = active in
1123             al @ [current], Indexing.index tbl current
1124         in
1125         (* alla fine new' contiene anche le attive semplificate!
1126          * quindi le aggiungo alle passive insieme alle new *)
1127         let rec simplify bag new' active passive =
1128           let bag, new' = forward_simplify_new bag eq_uri env new' active in
1129           let bag, active, newa, pruned =
1130             backward_simplify bag eq_uri env new' active in
1131           let passive =
1132             List.fold_left (filter_dependent bag) passive pruned in
1133           match newa with
1134           | None -> bag, active, passive, new'
1135           | Some p -> simplify bag (new' @ p) active passive
1136         in
1137         let bag, active, passive, new' = simplify bag new' active passive in
1138         let _ =
1139           Utils.debug_print
1140             (lazy
1141                (Printf.sprintf "active:\n%s\n"
1142                   (String.concat "\n"
1143                      (List.map
1144                          (fun e -> Equality.string_of_equality ~env e)
1145                          (fst active)))))
1146         in
1147         let _ =
1148           Utils.debug_print
1149             (lazy
1150                (Printf.sprintf "new':\n%s\n"
1151                   (String.concat "\n"
1152                      (List.map
1153                          (fun e -> "Negative " ^
1154                             (Equality.string_of_equality ~env e)) new'))))
1155         in
1156         let new' = List.filter accept_fun new' in
1157         let passive = add_to_passive passive new' [] in
1158         saturate_equations bag eq_uri env goal accept_fun passive active
1159 ;;
1160
1161 let default_depth = !maxdepth
1162 and default_width = !maxwidth;;
1163
1164 let reset_refs () =
1165   symbols_counter := 0;
1166   weight_age_counter := !weight_age_ratio;
1167   processed_clauses := 0;
1168   start_time := 0.;
1169   elapsed_time := 0.;
1170   maximal_retained_equality := None;
1171   infer_time := 0.;
1172   forward_simpl_time := 0.;
1173   forward_simpl_new_time := 0.;
1174   backward_simpl_time := 0.;
1175   passive_maintainance_time := 0.;
1176   derived_clauses := 0;
1177   kept_clauses := 0;
1178 ;;
1179
1180 let add_to_active bag active passive env ty term newmetas =
1181    reset_refs ();
1182    match LibraryObjects.eq_URI () with
1183    | None -> active, passive, bag
1184    | Some eq_uri ->
1185        try
1186          let bag, current = Equality.equality_of_term bag term ty newmetas in
1187          let bag, current = Equality.fix_metas bag current in
1188          match add_to_active_aux bag active passive env eq_uri current with
1189          | _,a,p,b -> a,p,b
1190        with
1191        | Equality.TermIsNotAnEquality -> active, passive, bag
1192 ;;
1193
1194
1195 let eq_of_goal = function
1196   | Cic.Appl [Cic.MutInd(uri,0,_);_;_;_] when LibraryObjects.is_eq_URI uri ->
1197       uri
1198   | _ -> raise (ProofEngineTypes.Fail (lazy ("The goal is not an equality ")))
1199 ;;
1200
1201 let eq_and_ty_of_goal = function
1202   | Cic.Appl [Cic.MutInd(uri,0,_);t;_;_] when LibraryObjects.is_eq_URI uri ->
1203       uri,t
1204   | _ -> raise (ProofEngineTypes.Fail (lazy ("The goal is not an equality ")))
1205 ;;
1206
1207 (* fix proof takes in input a term and try to build a metasenv for it *)
1208
1209 let fix_proof metasenv context all_implicits p =
1210   let rec aux metasenv n p =
1211     match p with
1212       | Cic.Meta (i,_) ->
1213           if all_implicits then
1214             metasenv,Cic.Implicit None
1215           else
1216           let irl =
1217             CicMkImplicit.identity_relocation_list_for_metavariable context
1218           in
1219           let meta = CicSubstitution.lift n (Cic.Meta (i,irl)) in
1220           let metasenv =
1221             try
1222             let _ = CicUtil.lookup_meta i metasenv in metasenv
1223             with CicUtil.Meta_not_found _ ->
1224             debug_print (lazy ("not found: "^(string_of_int i)));
1225             let metasenv,j = CicMkImplicit.mk_implicit_type metasenv [] context in
1226               (i,context,Cic.Meta(j,irl))::metasenv
1227           in
1228             metasenv,meta
1229       | Cic.Appl l ->
1230           let metasenv,l=
1231             List.fold_right
1232               (fun a (metasenv,l) ->
1233                  let metasenv,a' = aux metasenv n a in
1234                    metasenv,a'::l)
1235               l (metasenv,[])
1236           in metasenv,Cic.Appl l
1237       | Cic.Lambda(name,s,t) ->
1238           let metasenv,s = aux metasenv n s in
1239           let metasenv,t = aux metasenv (n+1) t in
1240             metasenv,Cic.Lambda(name,s,t)
1241       | Cic.Prod(name,s,t) ->
1242           let metasenv,s = aux metasenv n s in
1243           let metasenv,t = aux metasenv (n+1) t in
1244             metasenv,Cic.Prod(name,s,t)
1245       | Cic.LetIn(name,s,ty,t) ->
1246           let metasenv,s = aux metasenv n s in
1247           let metasenv,ty = aux metasenv n ty in
1248           let metasenv,t = aux metasenv (n+1) t in
1249             metasenv,Cic.LetIn(name,s,ty,t)
1250       | Cic.Const(uri,ens) ->
1251           let metasenv,ens =
1252             List.fold_right
1253               (fun (v,a) (metasenv,ens) ->
1254                  let metasenv,a' = aux metasenv n a in
1255                    metasenv,(v,a')::ens)
1256               ens (metasenv,[])
1257           in
1258           metasenv,Cic.Const(uri,ens)
1259       | t -> metasenv,t
1260   in
1261   aux metasenv 0 p
1262 ;;
1263
1264 let fix_metasenv context metasenv =
1265   List.fold_left
1266     (fun m (i,c,t) ->
1267        let m,t = fix_proof m context false t in
1268        let m = List.filter (fun (j,_,_) -> j<>i) m in
1269          (i,context,t)::m)
1270     metasenv metasenv
1271 ;;
1272
1273
1274 (* status: input proof status
1275  * goalproof: forward steps on goal
1276  * newproof: backward steps
1277  * subsumption_id: the equation used if goal is closed by subsumption
1278  *   (0 if not closed by subsumption) (DEBUGGING: can be safely removed)
1279  * subsumption_subst: subst to make newproof and goalproof match
1280  * proof_menv: final metasenv
1281  *)
1282
1283 let build_proof
1284   bag status
1285   goalproof newproof subsumption_id subsumption_subst proof_menv
1286 =
1287   if proof_menv = [] then debug_print (lazy "+++++++++++++++VUOTA")
1288   else debug_print (lazy (CicMetaSubst.ppmetasenv [] proof_menv));
1289   let proof, goalno = status in
1290   let uri, metasenv, _subst, meta_proof, term_to_prove, attrs = proof in
1291   let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in
1292   let eq_uri = eq_of_goal type_of_goal in
1293   let names = Utils.names_of_context context in
1294   debug_print (lazy "Proof:");
1295   debug_print (lazy
1296     (Equality.pp_proof bag names goalproof newproof subsumption_subst
1297        subsumption_id type_of_goal));
1298 (*
1299       prerr_endline ("max weight: " ^
1300         (string_of_int (Equality.max_weight goalproof newproof)));
1301 *)
1302   (* generation of the CIC proof *)
1303   (* let metasenv' = List.filter (fun i,_,_ -> i<>goalno) metasenv in *)
1304   let side_effects =
1305     List.filter (fun i -> i <> goalno)
1306       (ProofEngineHelpers.compare_metasenvs
1307          ~newmetasenv:metasenv ~oldmetasenv:proof_menv) in
1308   let goal_proof, side_effects_t =
1309     let initial = Equality.add_subst subsumption_subst newproof in
1310       Equality.build_goal_proof bag
1311         eq_uri goalproof initial type_of_goal side_effects
1312         context proof_menv
1313   in
1314 (*   Equality.draw_proof bag names goalproof newproof subsumption_id; *)
1315   let goal_proof = Subst.apply_subst subsumption_subst goal_proof in
1316   (* assert (metasenv=[]); *)
1317   let real_menv =  fix_metasenv context (proof_menv@metasenv) in
1318   let real_menv,goal_proof =
1319     fix_proof real_menv context false goal_proof in
1320 (*
1321   let real_menv,fixed_proof = fix_proof proof_menv context false goal_proof in
1322     (* prerr_endline ("PROOF: " ^ CicPp.pp goal_proof names); *)
1323 *)
1324   let pp_error goal_proof names error exn =
1325     prerr_endline "THE PROOF DOES NOT TYPECHECK! <begin>";
1326     prerr_endline (CicPp.pp goal_proof names);
1327     prerr_endline "THE PROOF DOES NOT TYPECHECK!";
1328     prerr_endline error;
1329     prerr_endline "THE PROOF DOES NOT TYPECHECK! <end>";
1330     raise exn
1331   in
1332   let old_insert_coercions = !CicRefine.insert_coercions in
1333   let goal_proof,goal_ty,real_menv,_ =
1334     (* prerr_endline ("parte la refine per: " ^ (CicPp.pp goal_proof names)); *)
1335     try
1336             debug_print (lazy (CicPp.ppterm goal_proof));
1337             CicRefine.insert_coercions := false;
1338             let res =
1339               CicRefine.type_of_aux'
1340                 real_menv context goal_proof CicUniv.empty_ugraph
1341             in
1342             CicRefine.insert_coercions := old_insert_coercions;
1343             res
1344     with
1345       | CicRefine.RefineFailure s
1346       | CicRefine.Uncertain s
1347       | CicRefine.AssertFailure s as exn ->
1348           CicRefine.insert_coercions := old_insert_coercions;
1349           pp_error goal_proof names (Lazy.force s) exn
1350       | CicUtil.Meta_not_found i as exn ->
1351           CicRefine.insert_coercions := old_insert_coercions;
1352           pp_error goal_proof names ("META NOT FOUND: "^string_of_int i) exn
1353       | Invalid_argument "list_fold_left2" as exn ->
1354           CicRefine.insert_coercions := old_insert_coercions;
1355           pp_error goal_proof names "Invalid_argument: list_fold_left2" exn
1356       | exn ->
1357           CicRefine.insert_coercions := old_insert_coercions;
1358           raise exn
1359   in
1360   let subst_side_effects,real_menv,_ =
1361     try
1362       CicUnification.fo_unif_subst [] context real_menv
1363         goal_ty type_of_goal CicUniv.empty_ugraph
1364     with
1365       | CicUnification.UnificationFailure s
1366       | CicUnification.Uncertain s
1367       | CicUnification.AssertFailure s -> assert false
1368           (*            fail "Maybe the local context of metas in the goal was not an IRL" s *)
1369   in
1370   Utils.debug_print (lazy "+++++++++++++ FINE UNIF");
1371   let final_subst =
1372     (goalno,(context,goal_proof,type_of_goal))::subst_side_effects
1373   in
1374 (*
1375       let metas_of_proof = Utils.metas_of_term goal_proof in
1376 *)
1377   let proof, real_metasenv =
1378     ProofEngineHelpers.subst_meta_and_metasenv_in_proof
1379       proof goalno final_subst
1380       (List.filter (fun i,_,_ -> i<>goalno ) real_menv)
1381   in
1382   let open_goals =
1383     (ProofEngineHelpers.compare_metasenvs
1384        ~oldmetasenv:metasenv ~newmetasenv:real_metasenv) in
1385 (*
1386   let open_goals =
1387     List.map (fun i,_,_ -> i) real_metasenv in
1388 *)
1389   final_subst, proof, open_goals
1390
1391
1392 (*
1393
1394       let metas_still_open_in_proof = Utils.metas_of_term goal_proof in
1395       (* prerr_endline (CicPp.pp goal_proof names); *)
1396       let goal_proof = (* Subst.apply_subst subsumption_subst *) goal_proof in
1397       let side_effects_t =
1398         List.map (Subst.apply_subst subsumption_subst) side_effects_t
1399       in
1400       (* replacing fake mets with real ones *)
1401       (* prerr_endline "replacing metas..."; *)
1402       let irl=CicMkImplicit.identity_relocation_list_for_metavariable context in
1403       CicMetaSubst.ppmetasenv [] proof_menv;
1404       let what, with_what =
1405         List.fold_left
1406           (fun (acc1,acc2) i ->
1407              (Cic.Meta(i,[]))::acc1, (Cic.Implicit None)::acc2)
1408           ([],[])
1409           metas_still_open_in_proof
1410 (*
1411           (List.filter
1412            (fun (i,_,_) ->
1413              List.mem i metas_still_open_in_proof
1414              (*&& not(List.mem i metas_still_open_in_goal)*))
1415            proof_menv)
1416 *)
1417       in
1418       let goal_proof_menv =
1419         List.filter
1420           (fun (i,_,_) -> List.mem i metas_still_open_in_proof)
1421              proof_menv
1422       in
1423       let replace where =
1424         (* we need this fake equality since the metas of the hypothesis may be
1425          * with a real local context *)
1426         ProofEngineReduction.replace_lifting
1427           ~equality:(fun x y ->
1428             match x,y with Cic.Meta(i,_),Cic.Meta(j,_) -> i=j | _-> false)
1429           ~what ~with_what ~where
1430       in
1431       let goal_proof = replace goal_proof in
1432         (* ok per le meta libere... ma per quelle che c'erano e sono rimaste?
1433          * what mi pare buono, sostituisce solo le meta farlocche *)
1434       let side_effects_t = List.map replace side_effects_t in
1435       let free_metas =
1436         List.filter (fun i -> i <> goalno)
1437           (ProofEngineHelpers.compare_metasenvs
1438             ~oldmetasenv:metasenv ~newmetasenv:goal_proof_menv)
1439       in
1440       (* prerr_endline
1441        *   ("freemetas: " ^
1442        *   String.concat "," (List.map string_of_int free_metas) ); *)
1443       (* check/refine/... build the new proof *)
1444       let replaced_goal =
1445         ProofEngineReduction.replace
1446           ~what:side_effects ~with_what:side_effects_t
1447           ~equality:(fun i t -> match t with Cic.Meta(j,_)->j=i|_->false)
1448           ~where:type_of_goal
1449       in
1450       let goal_proof,goal_ty,real_menv,_ =
1451         try
1452           CicRefine.type_of_aux' metasenv context goal_proof
1453             CicUniv.empty_ugraph
1454         with
1455         | CicUtil.Meta_not_found _
1456         | CicRefine.RefineFailure _
1457         | CicRefine.Uncertain _
1458         | CicRefine.AssertFailure _
1459         | Invalid_argument "list_fold_left2" as exn ->
1460             prerr_endline "THE PROOF DOES NOT TYPECHECK!";
1461             prerr_endline (CicPp.pp goal_proof names);
1462             prerr_endline "THE PROOF DOES NOT TYPECHECK!";
1463             raise exn
1464       in
1465       prerr_endline "+++++++++++++ METASENV";
1466       prerr_endline
1467        (CicMetaSubst.ppmetasenv [] real_menv);
1468       let subst_side_effects,real_menv,_ =
1469 (*
1470         prerr_endline ("XX type_of_goal  " ^ CicPp.ppterm type_of_goal);
1471         prerr_endline ("XX replaced_goal " ^ CicPp.ppterm replaced_goal);
1472         prerr_endline ("XX metasenv      " ^
1473         CicMetaSubst.ppmetasenv [] (metasenv @ free_metas_menv));
1474 *)
1475         try
1476           CicUnification.fo_unif_subst [] context real_menv
1477            goal_ty type_of_goal CicUniv.empty_ugraph
1478         with
1479         | CicUnification.UnificationFailure s
1480         | CicUnification.Uncertain s
1481         | CicUnification.AssertFailure s -> assert false
1482 (*            fail "Maybe the local context of metas in the goal was not an IRL" s *)
1483       in
1484       let final_subst =
1485         (goalno,(context,goal_proof,type_of_goal))::subst_side_effects
1486       in
1487 (*
1488       let metas_of_proof = Utils.metas_of_term goal_proof in
1489 *)
1490       let proof, real_metasenv =
1491         ProofEngineHelpers.subst_meta_and_metasenv_in_proof
1492           proof goalno (CicMetaSubst.apply_subst final_subst)
1493           (List.filter (fun i,_,_ -> i<>goalno ) real_menv)
1494       in
1495       let open_goals =
1496         List.map (fun i,_,_ -> i) real_metasenv in
1497
1498 (*
1499         HExtlib.list_uniq (List.sort Pervasives.compare metas_of_proof)
1500       in *)
1501 (*
1502         match free_meta with Some(Cic.Meta(m,_)) when m<>goalno ->[m] | _ ->[]
1503       in
1504 *)
1505 (*
1506       Printf.eprintf
1507         "GOALS APERTI: %s\nMETASENV PRIMA:\n%s\nMETASENV DOPO:\n%s\n"
1508           (String.concat ", " (List.map string_of_int open_goals))
1509           (CicMetaSubst.ppmetasenv [] metasenv)
1510           (CicMetaSubst.ppmetasenv [] real_metasenv);
1511 *)
1512       final_subst, proof, open_goals
1513 ;;
1514 *)
1515
1516 (* **************** HERE ENDS THE PARAMODULATION STUFF ******************** *)
1517
1518 (* exported functions  *)
1519
1520 let pump_actives context bag active passive saturation_steps max_time =
1521   reset_refs();
1522 (*
1523   let max_l l =
1524     List.fold_left
1525      (fun acc e -> let _,_,_,menv,_ = Equality.open_equality e in
1526       List.fold_left (fun acc (i,_,_) -> max i acc) acc menv)
1527      0 l in
1528 *)
1529 (*   let active_l = fst active in *)
1530 (*   let passive_l = fst passive in *)
1531 (*   let ma = max_l active_l in *)
1532 (*   let mp = max_l passive_l in *)
1533   match LibraryObjects.eq_URI () with
1534     | None -> active, passive, bag
1535     | Some eq_uri ->
1536         let env = [],context,CicUniv.empty_ugraph in
1537           (match
1538              given_clause bag eq_uri env ([],[])
1539                passive active 0 saturation_steps max_time
1540            with
1541            | ParamodulationFailure (_,a,p,b) ->
1542                  a, p, b
1543              | ParamodulationSuccess _ ->
1544                  assert false)
1545 ;;
1546
1547 let all_subsumed bag status active passive =
1548   let proof, goalno = status in
1549   let uri, metasenv, _subst, meta_proof, term_to_prove, attrs = proof in
1550   let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in
1551   let env = metasenv,context,CicUniv.empty_ugraph in
1552   let cleaned_goal = Utils.remove_local_context type_of_goal in
1553   let canonical_menv,other_menv =
1554     List.partition (fun (_,c,_) -> c = context)  metasenv in
1555   (* prerr_endline ("other menv = " ^ (CicMetaSubst.ppmetasenv [] other_menv));   *)
1556   let metasenv = List.map (fun (i,_,ty)-> (i,[],ty)) canonical_menv in
1557   let goal = [], List.filter (fun (i,_,_)->i<>goalno) metasenv, cleaned_goal in
1558   debug_print (lazy (string_of_int (List.length (fst active))));
1559    (* we simplify using both actives passives *)
1560   let table =
1561     List.fold_left
1562       (fun (l,tbl) eq -> eq::l,(Indexing.index tbl eq))
1563       active (list_of_passive passive) in
1564   let (_,_,ty) = goal in
1565   debug_print (lazy ("prima " ^ CicPp.ppterm ty));
1566   let _,goal = simplify_goal bag env goal table in
1567   let (_,_,ty) = goal in
1568   debug_print (lazy ("in mezzo " ^ CicPp.ppterm ty));
1569   let bag, subsumed = find_all_subsumed bag env (snd table) goal in
1570   debug_print (lazy ("dopo " ^ CicPp.ppterm ty));
1571   let subsumed_or_id =
1572     match (check_if_goal_is_identity env goal) with
1573         None -> subsumed
1574       | Some id -> id::subsumed in
1575   debug_print (lazy "dopo subsumed");
1576   let res =
1577     List.map
1578       (fun
1579          (goalproof,newproof,subsumption_id,subsumption_subst, proof_menv) ->
1580            let subst, proof, gl =
1581              build_proof bag
1582                status goalproof newproof subsumption_id subsumption_subst proof_menv
1583            in
1584            let uri, metasenv, subst, meta_proof, term_to_prove, attrs = proof in
1585            let newmetasenv =
1586              other_menv @
1587              List.filter
1588                (fun x,_,_ -> not (List.exists (fun y,_,_ -> x=y) other_menv)) metasenv
1589            in
1590            let proof = uri, newmetasenv, subst, meta_proof, term_to_prove, attrs in
1591              (subst, proof,gl)) subsumed_or_id
1592   in
1593   res
1594 ;;
1595
1596
1597 let given_clause
1598   bag status active passive goal_steps saturation_steps max_time
1599 =
1600   reset_refs();
1601   let active_l = fst active in
1602   let proof, goalno = status in
1603   let uri, metasenv, _subst, meta_proof, term_to_prove, attrs = proof in
1604   let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in
1605   let eq_uri = eq_of_goal type_of_goal in
1606   let cleaned_goal = Utils.remove_local_context type_of_goal in
1607   let metas_occurring_in_goal = CicUtil.metas_of_term cleaned_goal in
1608   let canonical_menv,other_menv =
1609     List.partition (fun (_,c,_) -> c = context)  metasenv in
1610   Utils.set_goal_symbols cleaned_goal; (* DISACTIVATED *)
1611   let canonical_menv =
1612     List.map
1613      (fun (i,_,ty)-> (i,[],Utils.remove_local_context ty)) canonical_menv
1614   in
1615   let metasenv' =
1616     List.filter
1617       (fun (i,_,_)-> i<>goalno && List.mem_assoc i metas_occurring_in_goal)
1618       canonical_menv
1619   in
1620   let goal = [], metasenv', cleaned_goal in
1621   let env = metasenv,context,CicUniv.empty_ugraph in
1622   debug_print (lazy ">>>>>> ACTIVES >>>>>>>>");
1623   List.iter (fun e -> debug_print (lazy (Equality.string_of_equality ~env e)))
1624   active_l;
1625   debug_print (lazy ">>>>>>>>>>>>>>");
1626   let goals = make_goal_set goal in
1627   match
1628     given_clause bag eq_uri env goals passive active
1629       goal_steps saturation_steps max_time
1630   with
1631   | ParamodulationFailure (_,a,p,b) ->
1632       None, a, p, b
1633   | ParamodulationSuccess
1634     ((goalproof,newproof,subsumption_id,subsumption_subst, proof_menv),a,p,b) ->
1635     let subst, proof, gl =
1636       build_proof b
1637         status goalproof newproof subsumption_id subsumption_subst proof_menv
1638     in
1639     let uri, metasenv, subst, meta_proof, term_to_prove, attrs = proof in
1640     let proof = uri, other_menv@metasenv, subst, meta_proof, term_to_prove, attrs in
1641     Some (subst, proof,gl),a,p, b
1642 ;;
1643
1644
1645 let add_to_passive eql passives =
1646   add_to_passive passives eql eql
1647 ;;
1648
1649