helm/software/components/tactics/paramodulation/saturation.ml

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