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