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