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