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