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