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