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

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