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 -> bag, None)
 807   | _ -> bag, None
 808 ;;
 809
 810 let find_all_subsumed bag env table (goalproof,menv,ty) =
 811   match ty with
 812   | Cic.Appl[Cic.MutInd(uri,_,_);eq_ty;left;right]
 813     when LibraryObjects.is_eq_URI uri ->
 814       let bag, goal_equation =
 815         (Equality.mk_equality bag
 816           (0,Equality.Exact (Cic.Implicit None),(eq_ty,left,right,Utils.Eq),menv))
 817       in
 818       List.fold_right
 819           (fun (subst, equality, swapped) (bag,acc) ->
 820              let (_,p,(ty,l,r,_),m,id) = Equality.open_equality equality in
 821              let cicmenv = Subst.apply_subst_metasenv subst (m @ menv) in
 822              Indexing.check_for_duplicates cicmenv "from subsumption";
 823              let bag, p =
 824                if swapped then
 825                  Equality.symmetric bag eq_ty l id uri m
 826                else
 827                  bag, p
 828              in
 829               bag, (goalproof, p, id, subst, cicmenv)::acc)
 830          (Indexing.subsumption_all env table goal_equation) (bag,[])
 831           (* (Indexing.unification_all env table goal_equation) *)
 832   | _ -> assert false
 833 ;;
 834
 835
 836 let check_if_goal_is_identity env = function
 837   | (goalproof,m,Cic.Appl[Cic.MutInd(uri,_,ens);eq_ty;left;right])
 838     when left = right && LibraryObjects.is_eq_URI uri ->
 839       let reflproof = Equality.Exact (Equality.refl_proof uri eq_ty left) in
 840       Some (goalproof, reflproof, 0, Subst.empty_subst,m)
 841   | (goalproof,m,Cic.Appl[Cic.MutInd(uri,_,ens);eq_ty;left;right])
 842     when LibraryObjects.is_eq_URI uri ->
 843     (let _,context,_ = env in
 844     try
 845      let s,m,_ =
 846        Founif.unification [] m context left right CicUniv.empty_ugraph
 847      in
 848       let reflproof = Equality.Exact (Equality.refl_proof uri eq_ty left) in
 849       let m = Subst.apply_subst_metasenv s m in
 850       Some (goalproof, reflproof, 0, s,m)
 851     with CicUnification.UnificationFailure _ -> None)
 852   | _ -> None
 853 ;;
 854
 855 let rec check b goal = function
 856   | [] -> b, None
 857   | f::tl ->
 858       match f b goal with
 859       | b, None -> check b goal tl
 860       | b, (Some _ as ok)  -> b, ok
 861 ;;
 862
 863 let simplify_goal_set bag env goals active =
 864   let active_goals, passive_goals = goals in
 865   let find (_,_,g) where =
 866     List.exists (fun (_,_,g1) -> Equality.meta_convertibility g g1) where
 867   in
 868     (* prova:tengo le passive semplificate
 869   let passive_goals =
 870     List.map (fun g -> snd (simplify_goal env g active)) passive_goals
 871   in *)
 872     List.fold_left
 873       (fun (acc_a,acc_p) goal ->
 874         match simplify_goal bag env goal active with
 875         | changed, g ->
 876             if changed then
 877               if find g acc_p then acc_a,acc_p else acc_a,g::acc_p
 878             else
 879               if find g acc_a then acc_a,acc_p else g::acc_a,acc_p)
 880       ([],passive_goals) active_goals
 881 ;;
 882
 883 let check_if_goals_set_is_solved bag env active goals =
 884   let active_goals, passive_goals = goals in
 885   List.fold_left
 886     (fun (bag, proof) goal ->
 887       match proof with
 888       | Some p -> bag, proof
 889       | None ->
 890           check bag goal [
 891             (fun b x -> b, check_if_goal_is_identity env x);
 892             (fun bag -> check_if_goal_is_subsumed bag env (snd active))])
 893 (* provare active and passive?*)
 894     (bag,None) active_goals
 895 ;;
 896
 897 let infer_goal_set bag env active goals =
 898   let active_goals, passive_goals = goals in
 899   let rec aux bag = function
 900     | [] -> bag, (active_goals, [])
 901     | hd::tl ->
 902         let changed, selected = simplify_goal bag env hd active in
 903         let (_,_,t1) = selected in
 904         let already_in =
 905           List.exists (fun (_,_,t) -> Equality.meta_convertibility t t1)
 906               active_goals
 907         in
 908         if already_in then
 909              aux bag tl
 910           else
 911             let passive_goals = tl in
 912             let bag, new_passive_goals =
 913               if Utils.metas_of_term t1 = [] then
 914                 bag, passive_goals
 915               else
 916                 let bag, new' =
 917                    Indexing.superposition_left bag env (snd active) selected
 918                 in
 919                 bag, passive_goals @ new'
 920             in
 921             bag, (selected::active_goals, new_passive_goals)
 922   in
 923    aux bag passive_goals
 924 ;;
 925
 926 let infer_goal_set_with_current bag env current goals active =
 927   let active_goals, passive_goals = simplify_goal_set bag env goals active in
 928   let l,table,_  = build_table [current] in
 929   let bag, passive_goals =
 930    List.fold_left
 931     (fun (bag, acc) g ->
 932       let bag, new' = Indexing.superposition_left bag env table g in
 933       bag, acc @ new')
 934     (bag, passive_goals) active_goals
 935   in
 936   bag, active_goals, passive_goals
 937 ;;
 938
 939 let ids_of_goal g =
 940   let p,_,_ = g in
 941   let ids = List.map (fun _,_,i,_,_ -> i) p in
 942   ids
 943 ;;
 944
 945 let ids_of_goal_set (ga,gp) =
 946   List.flatten (List.map ids_of_goal ga) @
 947   List.flatten (List.map ids_of_goal gp)
 948 ;;
 949
 950 let size_of_goal_set_a (l,_) = List.length l;;
 951 let size_of_goal_set_p (_,l) = List.length l;;
 952
 953 let pp_goals label goals context =
 954   let names = Utils.names_of_context context in
 955   List.iter
 956     (fun _,_,g ->
 957       debug_print (lazy
 958         (Printf.sprintf  "Current goal: %s = %s\n" label (CicPp.pp g names))))
 959     (fst goals);
 960   List.iter
 961     (fun _,_,g ->
 962       debug_print (lazy
 963         (Printf.sprintf  "PASSIVE goal: %s = %s\n" label (CicPp.pp g names))))
 964       (snd goals);
 965 ;;
 966
 967 let print_status iterno goals active passive =
 968   debug_print (lazy
 969     (Printf.sprintf "\n%d #ACTIVES: %d #PASSIVES: %d #GOALSET: %d(%d)"
 970       iterno (size_of_active active) (size_of_passive passive)
 971       (size_of_goal_set_a goals) (size_of_goal_set_p goals)))
 972 ;;
 973
 974 let add_to_active_aux bag active passive env eq_uri current =
 975   debug_print (lazy ("Adding to actives : " ^
 976     Equality.string_of_equality ~env  current));
 977   match forward_simplify bag eq_uri env current active with
 978   | bag, None -> None, active, passive, bag
 979   | bag, Some current ->
 980       let bag, new' = infer bag eq_uri env current active in
 981       let active =
 982         let al, tbl = active in
 983         al @ [current], Indexing.index tbl current
 984       in
 985       let rec simplify bag new' active passive =
 986         let bag, new' =
 987           forward_simplify_new bag eq_uri env new' active
 988         in
 989         let bag, active, newa, pruned =
 990           backward_simplify bag eq_uri env new' active
 991         in
 992         let passive =
 993           List.fold_left (filter_dependent bag) passive pruned
 994         in
 995         match newa with
 996         | None -> bag, active, passive, new'
 997         | Some p -> simplify bag (new' @ p) active passive
 998       in
 999       let bag, active, passive, new' =
1000         simplify bag new' active passive
1001       in
1002       let passive = add_to_passive passive new' [] in
1003       Some new', active, passive, bag
1004 ;;
1005
1006 (** given-clause algorithm with full reduction strategy: NEW implementation *)
1007 (* here goals is a set of goals in OR *)
1008 let given_clause
1009   bag eq_uri ((_,context,_) as env) goals passive active
1010   goal_steps saturation_steps max_time
1011 =
1012   let initial_time = Unix.gettimeofday () in
1013   let iterations_left iterno =
1014     let now = Unix.gettimeofday () in
1015     let time_left = max_time -. now in
1016     let time_spent_until_now = now -. initial_time in
1017     let iteration_medium_cost =
1018       time_spent_until_now /. (float_of_int iterno)
1019     in
1020     let iterations_left = time_left /. iteration_medium_cost in
1021     int_of_float iterations_left
1022   in
1023   let rec step bag goals passive active g_iterno s_iterno =
1024     if g_iterno > goal_steps && s_iterno > saturation_steps then
1025       (ParamodulationFailure ("No more iterations to spend",active,passive,bag))
1026     else if Unix.gettimeofday () > max_time then
1027       (ParamodulationFailure ("No more time to spend",active,passive,bag))
1028     else
1029       let _ =
1030          print_status (max g_iterno s_iterno) goals active passive
1031 (*         Printf.eprintf ".%!"; *)
1032       in
1033       (* PRUNING OF PASSIVE THAT WILL NEVER BE PROCESSED *)
1034       let passive =
1035         let selection_estimate = iterations_left (max g_iterno s_iterno) in
1036         let kept = size_of_passive passive in
1037         if kept > selection_estimate then
1038           begin
1039             (*Printf.eprintf "Too many passive equalities: pruning...";
1040             prune_passive selection_estimate active*) passive
1041           end
1042         else
1043           passive
1044       in
1045       kept_clauses := (size_of_passive passive) + (size_of_active active);
1046       let bag, goals =
1047         if g_iterno < goal_steps then
1048           infer_goal_set bag env active goals
1049         else
1050           bag, goals
1051       in
1052       match check_if_goals_set_is_solved bag env active goals with
1053       | bag, Some p ->
1054           debug_print (lazy
1055             (Printf.sprintf "\nFound a proof in: %f\n"
1056               (Unix.gettimeofday() -. initial_time)));
1057           ParamodulationSuccess (p,active,passive,bag)
1058       | bag, None ->
1059           (* SELECTION *)
1060           if passive_is_empty passive then
1061             if no_more_passive_goals goals then
1062               ParamodulationFailure
1063                 ("No more passive equations/goals",active,passive,bag)
1064               (*maybe this is a success! *)
1065             else
1066               step bag goals passive active (g_iterno+1) (s_iterno+1)
1067           else
1068             begin
1069               (* COLLECTION OF GARBAGED EQUALITIES *)
1070               let bag =
1071                 if max g_iterno s_iterno mod 40 = 0 then
1072                   (print_status (max g_iterno s_iterno) goals active passive;
1073                   let active = List.map Equality.id_of (fst active) in
1074                   let passive = List.map Equality.id_of (fst passive) in
1075                   let goal = ids_of_goal_set goals in
1076                   Equality.collect bag active passive goal)
1077                 else
1078                   bag
1079               in
1080               if s_iterno > saturation_steps then
1081                 ParamodulationFailure ("max saturation steps",active,passive,bag)
1082               else
1083                 let current, passive = select env goals passive in
1084                   match add_to_active_aux bag active passive env eq_uri current with
1085                   | None, active, passive, bag ->
1086                       step bag goals passive active (g_iterno+1) (s_iterno+1)
1087                   | Some new', active, passive, bag ->
1088                       let bag, active_goals, passive_goals =
1089                         infer_goal_set_with_current bag env current goals active
1090                       in
1091                       let goals =
1092                         let a,b,_ = build_table new' in
1093                         let rc =
1094                           simplify_goal_set bag env (active_goals,passive_goals) (a,b)
1095                         in
1096                         rc
1097                       in
1098                       step bag goals passive active (g_iterno+1) (s_iterno+1)
1099             end
1100   in
1101     step bag goals passive active 1 1
1102 ;;
1103
1104 let rec saturate_equations bag eq_uri env goal accept_fun passive active =
1105   elapsed_time := Unix.gettimeofday () -. !start_time;
1106   if !elapsed_time > !time_limit then
1107     bag, active, passive
1108   else
1109     let current, passive = select env ([goal],[]) passive in
1110     let bag, res = forward_simplify bag eq_uri env current active in
1111     match res with
1112     | None ->
1113         saturate_equations bag eq_uri env goal accept_fun passive active
1114     | Some current ->
1115         Utils.debug_print (lazy (Printf.sprintf "selected: %s"
1116                              (Equality.string_of_equality ~env current)));
1117         let bag, new' = infer bag eq_uri env current active in
1118         let active =
1119           if Equality.is_identity env current then active
1120           else
1121             let al, tbl = active in
1122             al @ [current], Indexing.index tbl current
1123         in
1124         (* alla fine new' contiene anche le attive semplificate!
1125          * quindi le aggiungo alle passive insieme alle new *)
1126         let rec simplify bag new' active passive =
1127           let bag, new' = forward_simplify_new bag eq_uri env new' active in
1128           let bag, active, newa, pruned =
1129             backward_simplify bag eq_uri env new' active in
1130           let passive =
1131             List.fold_left (filter_dependent bag) passive pruned in
1132           match newa with
1133           | None -> bag, active, passive, new'
1134           | Some p -> simplify bag (new' @ p) active passive
1135         in
1136         let bag, active, passive, new' = simplify bag new' active passive in
1137         let _ =
1138           Utils.debug_print
1139             (lazy
1140                (Printf.sprintf "active:\n%s\n"
1141                   (String.concat "\n"
1142                      (List.map
1143                          (fun e -> Equality.string_of_equality ~env e)
1144                          (fst active)))))
1145         in
1146         let _ =
1147           Utils.debug_print
1148             (lazy
1149                (Printf.sprintf "new':\n%s\n"
1150                   (String.concat "\n"
1151                      (List.map
1152                          (fun e -> "Negative " ^
1153                             (Equality.string_of_equality ~env e)) new'))))
1154         in
1155         let new' = List.filter accept_fun new' in
1156         let passive = add_to_passive passive new' [] in
1157         saturate_equations bag eq_uri env goal accept_fun passive active
1158 ;;
1159
1160 let default_depth = !maxdepth
1161 and default_width = !maxwidth;;
1162
1163 let reset_refs () =
1164   symbols_counter := 0;
1165   weight_age_counter := !weight_age_ratio;
1166   processed_clauses := 0;
1167   start_time := 0.;
1168   elapsed_time := 0.;
1169   maximal_retained_equality := None;
1170   infer_time := 0.;
1171   forward_simpl_time := 0.;
1172   forward_simpl_new_time := 0.;
1173   backward_simpl_time := 0.;
1174   passive_maintainance_time := 0.;
1175   derived_clauses := 0;
1176   kept_clauses := 0;
1177 ;;
1178
1179 let add_to_active bag active passive env ty term newmetas =
1180    reset_refs ();
1181    match LibraryObjects.eq_URI () with
1182    | None -> active, passive, bag
1183    | Some eq_uri ->
1184        try
1185          let bag, current = Equality.equality_of_term bag term ty newmetas in
1186          let bag, current = Equality.fix_metas bag current in
1187          match add_to_active_aux bag active passive env eq_uri current with
1188          | _,a,p,b -> a,p,b
1189        with
1190        | Equality.TermIsNotAnEquality -> active, passive, bag
1191 ;;
1192
1193
1194 let eq_of_goal = function
1195   | Cic.Appl [Cic.MutInd(uri,0,_);_;_;_] when LibraryObjects.is_eq_URI uri ->
1196       uri
1197   | _ -> raise (ProofEngineTypes.Fail (lazy ("The goal is not an equality ")))
1198 ;;
1199
1200 let eq_and_ty_of_goal = function
1201   | Cic.Appl [Cic.MutInd(uri,0,_);t;_;_] when LibraryObjects.is_eq_URI uri ->
1202       uri,t
1203   | _ -> raise (ProofEngineTypes.Fail (lazy ("The goal is not an equality ")))
1204 ;;
1205
1206 (* fix proof takes in input a term and try to build a metasenv for it *)
1207
1208 let fix_proof metasenv context all_implicits p =
1209   let rec aux metasenv n p =
1210     match p with
1211       | Cic.Meta (i,_) ->
1212           if all_implicits then
1213             metasenv,Cic.Implicit None
1214           else
1215           let irl =
1216             CicMkImplicit.identity_relocation_list_for_metavariable context
1217           in
1218           let meta = CicSubstitution.lift n (Cic.Meta (i,irl)) in
1219           let metasenv =
1220             try
1221             let _ = CicUtil.lookup_meta i metasenv in metasenv
1222             with CicUtil.Meta_not_found _ ->
1223             debug_print (lazy ("not found: "^(string_of_int i)));
1224             let metasenv,j = CicMkImplicit.mk_implicit_type metasenv [] context in
1225               (i,context,Cic.Meta(j,irl))::metasenv
1226           in
1227             metasenv,meta
1228       | Cic.Appl l ->
1229           let metasenv,l=
1230             List.fold_right
1231               (fun a (metasenv,l) ->
1232                  let metasenv,a' = aux metasenv n a in
1233                    metasenv,a'::l)
1234               l (metasenv,[])
1235           in metasenv,Cic.Appl l
1236       | Cic.Lambda(name,s,t) ->
1237           let metasenv,s = aux metasenv n s in
1238           let metasenv,t = aux metasenv (n+1) t in
1239             metasenv,Cic.Lambda(name,s,t)
1240       | Cic.Prod(name,s,t) ->
1241           let metasenv,s = aux metasenv n s in
1242           let metasenv,t = aux metasenv (n+1) t in
1243             metasenv,Cic.Prod(name,s,t)
1244       | Cic.LetIn(name,s,ty,t) ->
1245           let metasenv,s = aux metasenv n s in
1246           let metasenv,ty = aux metasenv n ty in
1247           let metasenv,t = aux metasenv (n+1) t in
1248             metasenv,Cic.LetIn(name,s,ty,t)
1249       | Cic.Const(uri,ens) ->
1250           let metasenv,ens =
1251             List.fold_right
1252               (fun (v,a) (metasenv,ens) ->
1253                  let metasenv,a' = aux metasenv n a in
1254                    metasenv,(v,a')::ens)
1255               ens (metasenv,[])
1256           in
1257           metasenv,Cic.Const(uri,ens)
1258       | t -> metasenv,t
1259   in
1260   aux metasenv 0 p
1261 ;;
1262
1263 let fix_metasenv context metasenv =
1264   List.fold_left
1265     (fun m (i,c,t) ->
1266        let m,t = fix_proof m context false t in
1267        let m = List.filter (fun (j,_,_) -> j<>i) m in
1268          (i,context,t)::m)
1269     metasenv metasenv
1270 ;;
1271
1272
1273 (* status: input proof status
1274  * goalproof: forward steps on goal
1275  * newproof: backward steps
1276  * subsumption_id: the equation used if goal is closed by subsumption
1277  *   (0 if not closed by subsumption) (DEBUGGING: can be safely removed)
1278  * subsumption_subst: subst to make newproof and goalproof match
1279  * proof_menv: final metasenv
1280  *)
1281
1282 let build_proof
1283   bag status
1284   goalproof newproof subsumption_id subsumption_subst proof_menv
1285 =
1286   if proof_menv = [] then debug_print (lazy "+++++++++++++++VUOTA")
1287   else debug_print (lazy (CicMetaSubst.ppmetasenv [] proof_menv));
1288   let proof, goalno = status in
1289   let uri, metasenv, _subst, meta_proof, term_to_prove, attrs = proof in
1290   let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in
1291   let eq_uri = eq_of_goal type_of_goal in
1292   let names = Utils.names_of_context context in
1293   debug_print (lazy "Proof:");
1294   debug_print (lazy
1295     (Equality.pp_proof bag names goalproof newproof subsumption_subst
1296        subsumption_id type_of_goal));
1297 (*
1298       prerr_endline ("max weight: " ^
1299         (string_of_int (Equality.max_weight goalproof newproof)));
1300 *)
1301   (* generation of the CIC proof *)
1302   (* let metasenv' = List.filter (fun i,_,_ -> i<>goalno) metasenv in *)
1303   let side_effects =
1304     List.filter (fun i -> i <> goalno)
1305       (ProofEngineHelpers.compare_metasenvs
1306          ~newmetasenv:metasenv ~oldmetasenv:proof_menv) in
1307   let goal_proof, side_effects_t =
1308     let initial = Equality.add_subst subsumption_subst newproof in
1309       Equality.build_goal_proof bag
1310         eq_uri goalproof initial type_of_goal side_effects
1311         context proof_menv
1312   in
1313 (*   Equality.draw_proof bag names goalproof newproof subsumption_id; *)
1314   let goal_proof = Subst.apply_subst subsumption_subst goal_proof in
1315   (* assert (metasenv=[]); *)
1316   let real_menv =  fix_metasenv context (proof_menv@metasenv) in
1317   let real_menv,goal_proof =
1318     fix_proof real_menv context false goal_proof in
1319 (*
1320   let real_menv,fixed_proof = fix_proof proof_menv context false goal_proof in
1321     (* prerr_endline ("PROOF: " ^ CicPp.pp goal_proof names); *)
1322 *)
1323   let pp_error goal_proof names error exn =
1324     prerr_endline "THE PROOF DOES NOT TYPECHECK! <begin>";
1325     prerr_endline (CicPp.pp goal_proof names);
1326     prerr_endline "THE PROOF DOES NOT TYPECHECK!";
1327     prerr_endline error;
1328     prerr_endline "THE PROOF DOES NOT TYPECHECK! <end>";
1329     raise exn
1330   in
1331   let old_insert_coercions = !CicRefine.insert_coercions in
1332   let goal_proof,goal_ty,real_menv,_ =
1333     (* prerr_endline ("parte la refine per: " ^ (CicPp.pp goal_proof names)); *)
1334     try
1335             debug_print (lazy (CicPp.ppterm goal_proof));
1336             CicRefine.insert_coercions := false;
1337             let res =
1338               CicRefine.type_of_aux'
1339                 real_menv context goal_proof CicUniv.empty_ugraph
1340             in
1341             CicRefine.insert_coercions := old_insert_coercions;
1342             res
1343     with
1344       | CicRefine.RefineFailure s
1345       | CicRefine.Uncertain s
1346       | CicRefine.AssertFailure s as exn ->
1347           CicRefine.insert_coercions := old_insert_coercions;
1348           pp_error goal_proof names (Lazy.force s) exn
1349       | CicUtil.Meta_not_found i as exn ->
1350           CicRefine.insert_coercions := old_insert_coercions;
1351           pp_error goal_proof names ("META NOT FOUND: "^string_of_int i) exn
1352       | Invalid_argument "list_fold_left2" as exn ->
1353           CicRefine.insert_coercions := old_insert_coercions;
1354           pp_error goal_proof names "Invalid_argument: list_fold_left2" exn
1355       | exn ->
1356           CicRefine.insert_coercions := old_insert_coercions;
1357           raise exn
1358   in
1359   let subst_side_effects,real_menv,_ =
1360     try
1361       CicUnification.fo_unif_subst [] context real_menv
1362         goal_ty type_of_goal CicUniv.empty_ugraph
1363     with
1364       | CicUnification.UnificationFailure s
1365       | CicUnification.Uncertain s
1366       | CicUnification.AssertFailure s -> assert false
1367           (*            fail "Maybe the local context of metas in the goal was not an IRL" s *)
1368   in
1369   Utils.debug_print (lazy "+++++++++++++ FINE UNIF");
1370   let final_subst =
1371     (goalno,(context,goal_proof,type_of_goal))::subst_side_effects
1372   in
1373 (*
1374       let metas_of_proof = Utils.metas_of_term goal_proof in
1375 *)
1376   let proof, real_metasenv =
1377     ProofEngineHelpers.subst_meta_and_metasenv_in_proof
1378       proof goalno final_subst
1379       (List.filter (fun i,_,_ -> i<>goalno ) real_menv)
1380   in
1381   let open_goals =
1382     (ProofEngineHelpers.compare_metasenvs
1383        ~oldmetasenv:metasenv ~newmetasenv:real_metasenv) in
1384 (*
1385   let open_goals =
1386     List.map (fun i,_,_ -> i) real_metasenv in
1387 *)
1388   final_subst, proof, open_goals
1389
1390
1391 (*
1392
1393       let metas_still_open_in_proof = Utils.metas_of_term goal_proof in
1394       (* prerr_endline (CicPp.pp goal_proof names); *)
1395       let goal_proof = (* Subst.apply_subst subsumption_subst *) goal_proof in
1396       let side_effects_t =
1397         List.map (Subst.apply_subst subsumption_subst) side_effects_t
1398       in
1399       (* replacing fake mets with real ones *)
1400       (* prerr_endline "replacing metas..."; *)
1401       let irl=CicMkImplicit.identity_relocation_list_for_metavariable context in
1402       CicMetaSubst.ppmetasenv [] proof_menv;
1403       let what, with_what =
1404         List.fold_left
1405           (fun (acc1,acc2) i ->
1406              (Cic.Meta(i,[]))::acc1, (Cic.Implicit None)::acc2)
1407           ([],[])
1408           metas_still_open_in_proof
1409 (*
1410           (List.filter
1411            (fun (i,_,_) ->
1412              List.mem i metas_still_open_in_proof
1413              (*&& not(List.mem i metas_still_open_in_goal)*))
1414            proof_menv)
1415 *)
1416       in
1417       let goal_proof_menv =
1418         List.filter
1419           (fun (i,_,_) -> List.mem i metas_still_open_in_proof)
1420              proof_menv
1421       in
1422       let replace where =
1423         (* we need this fake equality since the metas of the hypothesis may be
1424          * with a real local context *)
1425         ProofEngineReduction.replace_lifting
1426           ~equality:(fun x y ->
1427             match x,y with Cic.Meta(i,_),Cic.Meta(j,_) -> i=j | _-> false)
1428           ~what ~with_what ~where
1429       in
1430       let goal_proof = replace goal_proof in
1431         (* ok per le meta libere... ma per quelle che c'erano e sono rimaste?
1432          * what mi pare buono, sostituisce solo le meta farlocche *)
1433       let side_effects_t = List.map replace side_effects_t in
1434       let free_metas =
1435         List.filter (fun i -> i <> goalno)
1436           (ProofEngineHelpers.compare_metasenvs
1437             ~oldmetasenv:metasenv ~newmetasenv:goal_proof_menv)
1438       in
1439       (* prerr_endline
1440        *   ("freemetas: " ^
1441        *   String.concat "," (List.map string_of_int free_metas) ); *)
1442       (* check/refine/... build the new proof *)
1443       let replaced_goal =
1444         ProofEngineReduction.replace
1445           ~what:side_effects ~with_what:side_effects_t
1446           ~equality:(fun i t -> match t with Cic.Meta(j,_)->j=i|_->false)
1447           ~where:type_of_goal
1448       in
1449       let goal_proof,goal_ty,real_menv,_ =
1450         try
1451           CicRefine.type_of_aux' metasenv context goal_proof
1452             CicUniv.empty_ugraph
1453         with
1454         | CicUtil.Meta_not_found _
1455         | CicRefine.RefineFailure _
1456         | CicRefine.Uncertain _
1457         | CicRefine.AssertFailure _
1458         | Invalid_argument "list_fold_left2" as exn ->
1459             prerr_endline "THE PROOF DOES NOT TYPECHECK!";
1460             prerr_endline (CicPp.pp goal_proof names);
1461             prerr_endline "THE PROOF DOES NOT TYPECHECK!";
1462             raise exn
1463       in
1464       prerr_endline "+++++++++++++ METASENV";
1465       prerr_endline
1466        (CicMetaSubst.ppmetasenv [] real_menv);
1467       let subst_side_effects,real_menv,_ =
1468 (*
1469         prerr_endline ("XX type_of_goal  " ^ CicPp.ppterm type_of_goal);
1470         prerr_endline ("XX replaced_goal " ^ CicPp.ppterm replaced_goal);
1471         prerr_endline ("XX metasenv      " ^
1472         CicMetaSubst.ppmetasenv [] (metasenv @ free_metas_menv));
1473 *)
1474         try
1475           CicUnification.fo_unif_subst [] context real_menv
1476            goal_ty type_of_goal CicUniv.empty_ugraph
1477         with
1478         | CicUnification.UnificationFailure s
1479         | CicUnification.Uncertain s
1480         | CicUnification.AssertFailure s -> assert false
1481 (*            fail "Maybe the local context of metas in the goal was not an IRL" s *)
1482       in
1483       let final_subst =
1484         (goalno,(context,goal_proof,type_of_goal))::subst_side_effects
1485       in
1486 (*
1487       let metas_of_proof = Utils.metas_of_term goal_proof in
1488 *)
1489       let proof, real_metasenv =
1490         ProofEngineHelpers.subst_meta_and_metasenv_in_proof
1491           proof goalno (CicMetaSubst.apply_subst final_subst)
1492           (List.filter (fun i,_,_ -> i<>goalno ) real_menv)
1493       in
1494       let open_goals =
1495         List.map (fun i,_,_ -> i) real_metasenv in
1496
1497 (*
1498         HExtlib.list_uniq (List.sort Pervasives.compare metas_of_proof)
1499       in *)
1500 (*
1501         match free_meta with Some(Cic.Meta(m,_)) when m<>goalno ->[m] | _ ->[]
1502       in
1503 *)
1504 (*
1505       Printf.eprintf
1506         "GOALS APERTI: %s\nMETASENV PRIMA:\n%s\nMETASENV DOPO:\n%s\n"
1507           (String.concat ", " (List.map string_of_int open_goals))
1508           (CicMetaSubst.ppmetasenv [] metasenv)
1509           (CicMetaSubst.ppmetasenv [] real_metasenv);
1510 *)
1511       final_subst, proof, open_goals
1512 ;;
1513 *)
1514
1515 (* **************** HERE ENDS THE PARAMODULATION STUFF ******************** *)
1516
1517 (* exported functions  *)
1518
1519 let pump_actives context bag active passive saturation_steps max_time =
1520   reset_refs();
1521 (*
1522   let max_l l =
1523     List.fold_left
1524      (fun acc e -> let _,_,_,menv,_ = Equality.open_equality e in
1525       List.fold_left (fun acc (i,_,_) -> max i acc) acc menv)
1526      0 l in
1527 *)
1528 (*   let active_l = fst active in *)
1529 (*   let passive_l = fst passive in *)
1530 (*   let ma = max_l active_l in *)
1531 (*   let mp = max_l passive_l in *)
1532   match LibraryObjects.eq_URI () with
1533     | None -> active, passive, bag
1534     | Some eq_uri ->
1535         let env = [],context,CicUniv.empty_ugraph in
1536           (match
1537              given_clause bag eq_uri env ([],[])
1538                passive active 0 saturation_steps max_time
1539            with
1540            | ParamodulationFailure (_,a,p,b) ->
1541                  a, p, b
1542              | ParamodulationSuccess _ ->
1543                  assert false)
1544 ;;
1545
1546 let all_subsumed bag status active passive =
1547   let proof, goalno = status in
1548   let uri, metasenv, _subst, meta_proof, term_to_prove, attrs = proof in
1549   let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in
1550   let env = metasenv,context,CicUniv.empty_ugraph in
1551   let cleaned_goal = Utils.remove_local_context type_of_goal in
1552   let canonical_menv,other_menv =
1553     List.partition (fun (_,c,_) -> c = context)  metasenv in
1554   (* prerr_endline ("other menv = " ^ (CicMetaSubst.ppmetasenv [] other_menv));   *)
1555   let metasenv = List.map (fun (i,_,ty)-> (i,[],ty)) canonical_menv in
1556   let goal = [], List.filter (fun (i,_,_)->i<>goalno) metasenv, cleaned_goal in
1557   debug_print (lazy (string_of_int (List.length (fst active))));
1558    (* we simplify using both actives passives *)
1559   let table =
1560     List.fold_left
1561       (fun (l,tbl) eq -> eq::l,(Indexing.index tbl eq))
1562       active (list_of_passive passive) in
1563   let (_,_,ty) = goal in
1564   debug_print (lazy ("prima " ^ CicPp.ppterm ty));
1565   let _,goal = simplify_goal bag env goal table in
1566   let (_,_,ty) = goal in
1567   debug_print (lazy ("in mezzo " ^ CicPp.ppterm ty));
1568   let bag, subsumed = find_all_subsumed bag env (snd table) goal in
1569   debug_print (lazy ("dopo " ^ CicPp.ppterm ty));
1570   let subsumed_or_id =
1571     match (check_if_goal_is_identity env goal) with
1572         None -> subsumed
1573       | Some id -> id::subsumed in
1574   debug_print (lazy "dopo subsumed");
1575   let res =
1576     List.map
1577       (fun
1578          (goalproof,newproof,subsumption_id,subsumption_subst, proof_menv) ->
1579            let subst, proof, gl =
1580              build_proof bag
1581                status goalproof newproof subsumption_id subsumption_subst proof_menv
1582            in
1583            let uri, metasenv, subst, meta_proof, term_to_prove, attrs = proof in
1584            let newmetasenv =
1585              other_menv @
1586              List.filter
1587                (fun x,_,_ -> not (List.exists (fun y,_,_ -> x=y) other_menv)) metasenv
1588            in
1589            let proof = uri, newmetasenv, subst, meta_proof, term_to_prove, attrs in
1590              (subst, proof,gl)) subsumed_or_id
1591   in
1592   res
1593 ;;
1594
1595
1596 let given_clause
1597   bag status active passive goal_steps saturation_steps max_time
1598 =
1599   reset_refs();
1600   let active_l = fst active in
1601   let proof, goalno = status in
1602   let uri, metasenv, _subst, meta_proof, term_to_prove, attrs = proof in
1603   let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in
1604   let eq_uri = eq_of_goal type_of_goal in
1605   let cleaned_goal = Utils.remove_local_context type_of_goal in
1606   let metas_occurring_in_goal = CicUtil.metas_of_term cleaned_goal in
1607   let canonical_menv,other_menv =
1608     List.partition (fun (_,c,_) -> c = context)  metasenv in
1609   Utils.set_goal_symbols cleaned_goal; (* DISACTIVATED *)
1610   let canonical_menv =
1611     List.map
1612      (fun (i,_,ty)-> (i,[],Utils.remove_local_context ty)) canonical_menv
1613   in
1614   let metasenv' =
1615     List.filter
1616       (fun (i,_,_)-> i<>goalno && List.mem_assoc i metas_occurring_in_goal)
1617       canonical_menv
1618   in
1619   let goal = [], metasenv', cleaned_goal in
1620   let env = metasenv,context,CicUniv.empty_ugraph in
1621   debug_print (lazy ">>>>>> ACTIVES >>>>>>>>");
1622   List.iter (fun e -> debug_print (lazy (Equality.string_of_equality ~env e)))
1623   active_l;
1624   debug_print (lazy ">>>>>>>>>>>>>>");
1625   let goals = make_goal_set goal in
1626   match
1627     given_clause bag eq_uri env goals passive active
1628       goal_steps saturation_steps max_time
1629   with
1630   | ParamodulationFailure (_,a,p,b) ->
1631       None, a, p, b
1632   | ParamodulationSuccess
1633     ((goalproof,newproof,subsumption_id,subsumption_subst, proof_menv),a,p,b) ->
1634     let subst, proof, gl =
1635       build_proof b
1636         status goalproof newproof subsumption_id subsumption_subst proof_menv
1637     in
1638     let uri, metasenv, subst, meta_proof, term_to_prove, attrs = proof in
1639     let proof = uri, other_menv@metasenv, subst, meta_proof, term_to_prove, attrs in
1640     Some (subst, proof,gl),a,p, b
1641 ;;
1642
1643
1644 let add_to_passive eql passives =
1645   add_to_passive passives eql eql
1646 ;;
1647
1648