components/tactics/paramodulation/indexing.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 (* $Id$ *)
  27
  28 module Index = Equality_indexing.DT (* discrimination tree based indexing *)
  29 (*
  30 module Index = Equality_indexing.DT (* path tree based indexing *)
  31 *)
  32
  33 let beta_expand_time = ref 0.;;
  34
  35 let debug_print = Utils.debug_print;;
  36
  37 (*
  38 for debugging
  39 let check_equation env equation msg =
  40   let w, proof, (eq_ty, left, right, order), metas, args = equation in
  41   let metasenv, context, ugraph = env
  42   let metasenv' = metasenv @ metas in
  43     try
  44       CicTypeChecker.type_of_aux' metasenv' context left ugraph;
  45       CicTypeChecker.type_of_aux' metasenv' context right ugraph;
  46       ()
  47     with
  48         CicUtil.Meta_not_found _ as exn ->
  49           begin
  50             prerr_endline msg;
  51             prerr_endline (CicPp.ppterm left);
  52             prerr_endline (CicPp.ppterm right);
  53             raise exn
  54           end
  55 *)
  56
  57 type retrieval_mode = Matching | Unification;;
  58
  59 let string_of_res ?env =
  60   function
  61       None -> "None"
  62     | Some (t, s, m, u, ((p,e), eq_URI)) ->
  63         Printf.sprintf "Some: (%s, %s, %s)"
  64           (Utils.string_of_pos p)
  65           (Inference.string_of_equality ?env e)
  66           (CicPp.ppterm t)
  67 ;;
  68
  69 let print_res ?env res =
  70   prerr_endline
  71     (String.concat "\n"
  72        (List.map (string_of_res ?env) res))
  73 ;;
  74
  75 let print_candidates ?env mode term res =
  76   let _ =
  77     match mode with
  78     | Matching ->
  79         prerr_endline ("| candidates Matching " ^ (CicPp.ppterm term))
  80     | Unification ->
  81         prerr_endline ("| candidates Unification " ^ (CicPp.ppterm term))
  82   in
  83   prerr_endline
  84     (String.concat "\n"
  85        (List.map
  86           (fun (p, e) ->
  87              Printf.sprintf "| (%s, %s)" (Utils.string_of_pos p)
  88                (Inference.string_of_equality ?env e))
  89           res));
  90 ;;
  91
  92
  93 let indexing_retrieval_time = ref 0.;;
  94
  95
  96 let apply_subst = CicMetaSubst.apply_subst
  97
  98 let index = Index.index
  99 let remove_index = Index.remove_index
 100 let in_index = Index.in_index
 101 let empty = Index.empty
 102 let init_index = Index.init_index
 103
 104 let check_disjoint_invariant subst metasenv msg =
 105   if (List.exists
 106         (fun (i,_,_) -> (List.exists (fun (j,_) -> i=j) subst)) metasenv)
 107   then
 108     begin
 109       prerr_endline ("not disjoint: " ^ msg);
 110       assert false
 111     end
 112 ;;
 113
 114 let check_for_duplicates metas msg =
 115   if List.length metas <>
 116   List.length (HExtlib.list_uniq (List.sort Pervasives.compare metas)) then
 117     begin
 118       prerr_endline ("DUPLICATI " ^ msg);
 119       prerr_endline (CicMetaSubst.ppmetasenv [] metas);
 120       assert false
 121     end
 122 ;;
 123
 124 let check_res res msg =
 125   match res with
 126       Some (t, subst, menv, ug, (eq_found, eq_URI)) ->
 127         let eqs = Inference.string_of_equality (snd eq_found) in
 128         check_disjoint_invariant subst menv msg;
 129         check_for_duplicates menv (msg ^ "\nchecking " ^ eqs);
 130     | None -> ()
 131 ;;
 132
 133 let check_target context target msg =
 134   let w, proof, (eq_ty, left, right, order), metas = target in
 135   (* check that metas does not contains duplicates *)
 136   let eqs = Inference.string_of_equality target in
 137   let _ = check_for_duplicates metas (msg ^ "\nchecking " ^ eqs) in
 138   let actual = (Inference.metas_of_term left)@(Inference.metas_of_term right)
 139     @(Inference.metas_of_term eq_ty)@(Inference.metas_of_proof proof) in
 140   let menv = List.filter (fun (i, _, _) -> List.mem i actual) metas in
 141   let _ = if menv <> metas then
 142     begin
 143       prerr_endline ("extra metas " ^ msg);
 144       prerr_endline (CicMetaSubst.ppmetasenv [] metas);
 145       prerr_endline "**********************";
 146       prerr_endline (CicMetaSubst.ppmetasenv [] menv);
 147       prerr_endline ("left: " ^ (CicPp.ppterm left));
 148       prerr_endline ("right: " ^ (CicPp.ppterm right));
 149       prerr_endline ("ty: " ^ (CicPp.ppterm eq_ty));
 150       assert false
 151     end
 152   else () in
 153   try
 154       CicTypeChecker.type_of_aux'
 155         metas context (Inference.build_proof_term proof) CicUniv.empty_ugraph
 156   with e ->
 157       prerr_endline msg;
 158       prerr_endline (Inference.string_of_proof proof);
 159       prerr_endline (CicPp.ppterm (Inference.build_proof_term proof));
 160       prerr_endline ("+++++++++++++left: " ^ (CicPp.ppterm left));
 161       prerr_endline ("+++++++++++++right: " ^ (CicPp.ppterm right));
 162       raise e
 163 ;;
 164
 165
 166 (* returns a list of all the equalities in the tree that are in relation
 167    "mode" with the given term, where mode can be either Matching or
 168    Unification.
 169
 170    Format of the return value: list of tuples in the form:
 171    (position - Left or Right - of the term that matched the given one in this
 172      equality,
 173     equality found)
 174
 175    Note that if equality is "left = right", if the ordering is left > right,
 176    the position will always be Left, and if the ordering is left < right,
 177    position will be Right.
 178 *)
 179 let local_max = ref 100;;
 180
 181 let make_variant (p,eq) =
 182   let maxmeta, eq = Inference.fix_metas !local_max eq in
 183   local_max := maxmeta;
 184   p, eq
 185 ;;
 186
 187 let get_candidates ?env mode tree term =
 188   let t1 = Unix.gettimeofday () in
 189   let res =
 190     let s =
 191       match mode with
 192       | Matching -> Index.retrieve_generalizations tree term
 193       | Unification -> Index.retrieve_unifiables tree term
 194     in
 195     Index.PosEqSet.elements s
 196   in
 197 (*   print_endline (Discrimination_tree.string_of_discrimination_tree tree); *)
 198 (*   print_newline (); *)
 199   let t2 = Unix.gettimeofday () in
 200   indexing_retrieval_time := !indexing_retrieval_time +. (t2 -. t1);
 201  (* make fresh instances *)
 202   res
 203 ;;
 204
 205 let profiler = HExtlib.profile "P/Indexing.get_candidates"
 206
 207 let get_candidates ?env mode tree term =
 208   profiler.HExtlib.profile (get_candidates ?env mode tree) term
 209
 210 let match_unif_time_ok = ref 0.;;
 211 let match_unif_time_no = ref 0.;;
 212
 213
 214 (*
 215   finds the first equality in the index that matches "term", of type "termty"
 216   termty can be Implicit if it is not needed. The result (one of the sides of
 217   the equality, actually) should be not greater (wrt the term ordering) than
 218   term
 219
 220   Format of the return value:
 221
 222   (term to substitute, [Cic.Rel 1 properly lifted - see the various
 223                         build_newtarget functions inside the various
 224                         demodulation_* functions]
 225    substitution used for the matching,
 226    metasenv,
 227    ugraph, [substitution, metasenv and ugraph have the same meaning as those
 228    returned by CicUnification.fo_unif]
 229    (equality where the matching term was found, [i.e. the equality to use as
 230                                                 rewrite rule]
 231     uri [either eq_ind_URI or eq_ind_r_URI, depending on the direction of
 232          the equality: this is used to build the proof term, again see one of
 233          the build_newtarget functions]
 234    ))
 235 *)
 236 let rec find_matches metasenv context ugraph lift_amount term termty =
 237   let module C = Cic in
 238   let module U = Utils in
 239   let module S = CicSubstitution in
 240   let module M = CicMetaSubst in
 241   let module HL = HelmLibraryObjects in
 242   let cmp = !Utils.compare_terms in
 243   let check = match termty with C.Implicit None -> false | _ -> true in
 244   function
 245     | [] -> None
 246     | candidate::tl ->
 247         let pos, (_, proof, (ty, left, right, o), metas) = candidate in
 248         if Utils.debug_metas then
 249           ignore(check_target context (snd candidate) "find_matches");
 250         if Utils.debug_res then
 251           begin
 252             let c = "eq = " ^ (Inference.string_of_equality (snd candidate)) ^ "\n"in
 253             let t = "t = " ^ (CicPp.ppterm term) ^ "\n" in
 254             let m = "metas = " ^ (CicMetaSubst.ppmetasenv [] metas) ^ "\n" in
 255             let p = "proof = " ^ (CicPp.ppterm (Inference.build_proof_term proof))  ^ "\n" in
 256               check_for_duplicates metas "gia nella metas";
 257               check_for_duplicates (metasenv @ metas) ("not disjoint" ^ c ^ t ^ m ^ p)
 258           end;
 259         if check && not (fst (CicReduction.are_convertible
 260                                 ~metasenv context termty ty ugraph)) then (
 261           find_matches metasenv context ugraph lift_amount term termty tl
 262         ) else
 263           let do_match c eq_URI =
 264             let subst', metasenv', ugraph' =
 265               let t1 = Unix.gettimeofday () in
 266               try
 267                 let r =
 268                   ( Inference.matching metasenv metas context
 269                     term (S.lift lift_amount c)) ugraph
 270                 in
 271                 let t2 = Unix.gettimeofday () in
 272                 match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
 273                 r
 274               with
 275                 | Inference.MatchingFailure as e ->
 276                 let t2 = Unix.gettimeofday () in
 277                 match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
 278                   raise e
 279                 | CicUtil.Meta_not_found _ as exn -> raise exn
 280             in
 281             Some (C.Rel (1 + lift_amount), subst', metasenv', ugraph',
 282                   (candidate, eq_URI))
 283           in
 284           let c, other, eq_URI =
 285             if pos = Utils.Left then left, right, Utils.eq_ind_URI ()
 286             else right, left, Utils.eq_ind_r_URI ()
 287           in
 288           if o <> U.Incomparable then
 289             let res =
 290               try
 291                 do_match c eq_URI
 292               with Inference.MatchingFailure ->
 293                 find_matches metasenv context ugraph lift_amount term termty tl
 294             in
 295               if Utils.debug_res then ignore (check_res res "find1");
 296               res
 297           else
 298             let res =
 299               try do_match c eq_URI
 300               with Inference.MatchingFailure -> None
 301             in
 302             if Utils.debug_res then ignore (check_res res "find2");
 303             match res with
 304             | Some (_, s, _, _, _) ->
 305                 let c' = apply_subst s c in
 306                 (*
 307              let other' = U.guarded_simpl context (apply_subst s other) in *)
 308                 let other' = apply_subst s other in
 309                 let order = cmp c' other' in
 310                 if order = U.Gt then
 311                   res
 312                 else
 313                   find_matches
 314                     metasenv context ugraph lift_amount term termty tl
 315             | None ->
 316                 find_matches metasenv context ugraph lift_amount term termty tl
 317 ;;
 318
 319 (*
 320   as above, but finds all the matching equalities, and the matching condition
 321   can be either Inference.matching or Inference.unification
 322 *)
 323 let rec find_all_matches ?(unif_fun=Inference.unification)
 324     metasenv context ugraph lift_amount term termty =
 325   let module C = Cic in
 326   let module U = Utils in
 327   let module S = CicSubstitution in
 328   let module M = CicMetaSubst in
 329   let module HL = HelmLibraryObjects in
 330   let cmp = !Utils.compare_terms in
 331   function
 332     | [] -> []
 333     | candidate::tl ->
 334         let pos, (_, _, (ty, left, right, o), metas) = candidate in
 335         let do_match c eq_URI =
 336           let subst', metasenv', ugraph' =
 337             let t1 = Unix.gettimeofday () in
 338             try
 339               let r =
 340                 unif_fun metasenv metas context
 341                   term (S.lift lift_amount c) ugraph in
 342               let t2 = Unix.gettimeofday () in
 343               match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
 344               r
 345             with
 346             | Inference.MatchingFailure
 347             | CicUnification.UnificationFailure _
 348             | CicUnification.Uncertain _ as e ->
 349                 let t2 = Unix.gettimeofday () in
 350                 match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
 351                 raise e
 352           in
 353           (C.Rel (1 + lift_amount), subst', metasenv', ugraph',
 354            (candidate, eq_URI))
 355         in
 356         let c, other, eq_URI =
 357           if pos = Utils.Left then left, right, Utils.eq_ind_URI ()
 358           else right, left, Utils.eq_ind_r_URI ()
 359         in
 360         if o <> U.Incomparable then
 361           try
 362             let res = do_match c eq_URI in
 363             res::(find_all_matches ~unif_fun metasenv context ugraph
 364                     lift_amount term termty tl)
 365           with
 366           | Inference.MatchingFailure
 367           | CicUnification.UnificationFailure _
 368           | CicUnification.Uncertain _ ->
 369               find_all_matches ~unif_fun metasenv context ugraph
 370                 lift_amount term termty tl
 371         else
 372           try
 373             let res = do_match c eq_URI in
 374             match res with
 375             | _, s, _, _, _ ->
 376                 let c' = apply_subst s c
 377                 and other' = apply_subst s other in
 378                 let order = cmp c' other' in
 379                 if order <> U.Lt && order <> U.Le then
 380                   res::(find_all_matches ~unif_fun metasenv context ugraph
 381                           lift_amount term termty tl)
 382                 else
 383                   find_all_matches ~unif_fun metasenv context ugraph
 384                     lift_amount term termty tl
 385           with
 386           | Inference.MatchingFailure
 387           | CicUnification.UnificationFailure _
 388           | CicUnification.Uncertain _ ->
 389               find_all_matches ~unif_fun metasenv context ugraph
 390                 lift_amount term termty tl
 391 ;;
 392
 393 let find_all_matches
 394   ?unif_fun metasenv context ugraph lift_amount term termty l
 395 =
 396   let rc =
 397     find_all_matches
 398       ?unif_fun metasenv context ugraph lift_amount term termty l
 399   in
 400   (*prerr_endline "CANDIDATES:";
 401   List.iter (fun (_,x)->prerr_endline (Inference.string_of_equality x)) l;
 402   prerr_endline ("MATCHING:" ^ CicPp.ppterm term ^ " are " ^ string_of_int
 403   (List.length rc));*)
 404   rc
 405
 406 (*
 407   returns true if target is subsumed by some equality in table
 408 *)
 409 let subsumption env table target =
 410   let _, _, (ty, left, right, _), tmetas = target in
 411   let metasenv, context, ugraph = env in
 412   let metasenv = metasenv @ tmetas in
 413   let samesubst subst subst' =
 414     let tbl = Hashtbl.create (List.length subst) in
 415     List.iter (fun (m, (c, t1, t2)) -> Hashtbl.add tbl m (c, t1, t2)) subst;
 416     List.for_all
 417       (fun (m, (c, t1, t2)) ->
 418          try
 419            let c', t1', t2' = Hashtbl.find tbl m in
 420            if (c = c') && (t1 = t1') && (t2 = t2') then true
 421            else false
 422          with Not_found ->
 423            true)
 424       subst'
 425   in
 426   let leftr =
 427     match left with
 428     | Cic.Meta _ -> []
 429     | _ ->
 430         let leftc = get_candidates Matching table left in
 431         find_all_matches ~unif_fun:Inference.matching
 432           metasenv context ugraph 0 left ty leftc
 433   in
 434   let rec ok what = function
 435     | [] -> false, []
 436     | (_, subst, menv, ug, ((pos, (_, _, (_, l, r, o), m)), _))::tl ->
 437         try
 438           let other = if pos = Utils.Left then r else l in
 439           let subst', menv', ug' =
 440             let t1 = Unix.gettimeofday () in
 441             try
 442               let r =
 443                 Inference.matching menv m context what other ugraph
 444               in
 445               let t2 = Unix.gettimeofday () in
 446               match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
 447               r
 448             with Inference.MatchingFailure as e ->
 449               let t2 = Unix.gettimeofday () in
 450               match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
 451               raise e
 452           in
 453           if samesubst subst subst' then
 454             true, subst
 455           else
 456             ok what tl
 457         with Inference.MatchingFailure ->
 458           ok what tl
 459   in
 460   let r, subst = ok right leftr in
 461   let r, s =
 462     if r then
 463       true, subst
 464     else
 465       let rightr =
 466         match right with
 467           | Cic.Meta _ -> []
 468           | _ ->
 469               let rightc = get_candidates Matching table right in
 470                 find_all_matches ~unif_fun:Inference.matching
 471                   metasenv context ugraph 0 right ty rightc
 472       in
 473         ok left rightr
 474   in
 475 (*     (if r then  *)
 476 (*        debug_print  *)
 477 (*          (lazy *)
 478 (*             (Printf.sprintf "SUBSUMPTION! %s\n%s\n" *)
 479 (*                (Inference.string_of_equality target) (Utils.print_subst s)))); *)
 480     r, s
 481 ;;
 482
 483 let rec demodulation_aux ?from ?(typecheck=false)
 484   metasenv context ugraph table lift_amount term =
 485   (* Printf.eprintf "term = %s\n" (CicPp.ppterm term); *)
 486   let module C = Cic in
 487   let module S = CicSubstitution in
 488   let module M = CicMetaSubst in
 489   let module HL = HelmLibraryObjects in
 490   let candidates =
 491     get_candidates ~env:(metasenv,context,ugraph) Matching table term in
 492 (*   let candidates = List.map make_variant candidates in *)
 493   let res =
 494     match term with
 495       | C.Meta _ -> None
 496       | term ->
 497           let termty, ugraph =
 498             if typecheck then
 499               CicTypeChecker.type_of_aux' metasenv context term ugraph
 500             else
 501               C.Implicit None, ugraph
 502           in
 503           let res =
 504             find_matches metasenv context ugraph lift_amount term termty candidates
 505           in
 506           if Utils.debug_res then ignore(check_res res "demod1");
 507             if res <> None then
 508               res
 509             else
 510               match term with
 511                 | C.Appl l ->
 512                     let res, ll =
 513                       List.fold_left
 514                         (fun (res, tl) t ->
 515                            if res <> None then
 516                              (res, tl @ [S.lift 1 t])
 517                            else
 518                              let r =
 519                                demodulation_aux ~from:"1" metasenv context ugraph table
 520                                  lift_amount t
 521                              in
 522                                match r with
 523                                  | None -> (None, tl @ [S.lift 1 t])
 524                                  | Some (rel, _, _, _, _) -> (r, tl @ [rel]))
 525                         (None, []) l
 526                     in (
 527                         match res with
 528                           | None -> None
 529                           | Some (_, subst, menv, ug, eq_found) ->
 530                               Some (C.Appl ll, subst, menv, ug, eq_found)
 531                       )
 532                 | C.Prod (nn, s, t) ->
 533                     let r1 =
 534                       demodulation_aux ~from:"2"
 535                         metasenv context ugraph table lift_amount s in (
 536                         match r1 with
 537                           | None ->
 538                               let r2 =
 539                                 demodulation_aux metasenv
 540                                   ((Some (nn, C.Decl s))::context) ugraph
 541                                   table (lift_amount+1) t
 542                               in (
 543                                   match r2 with
 544                                     | None -> None
 545                                     | Some (t', subst, menv, ug, eq_found) ->
 546                                         Some (C.Prod (nn, (S.lift 1 s), t'),
 547                                               subst, menv, ug, eq_found)
 548                                 )
 549                           | Some (s', subst, menv, ug, eq_found) ->
 550                               Some (C.Prod (nn, s', (S.lift 1 t)),
 551                                     subst, menv, ug, eq_found)
 552                       )
 553                 | C.Lambda (nn, s, t) ->
 554                     let r1 =
 555                       demodulation_aux
 556                         metasenv context ugraph table lift_amount s in (
 557                         match r1 with
 558                           | None ->
 559                               let r2 =
 560                                 demodulation_aux metasenv
 561                                   ((Some (nn, C.Decl s))::context) ugraph
 562                                   table (lift_amount+1) t
 563                               in (
 564                                   match r2 with
 565                                     | None -> None
 566                                     | Some (t', subst, menv, ug, eq_found) ->
 567                                         Some (C.Lambda (nn, (S.lift 1 s), t'),
 568                                               subst, menv, ug, eq_found)
 569                                 )
 570                           | Some (s', subst, menv, ug, eq_found) ->
 571                               Some (C.Lambda (nn, s', (S.lift 1 t)),
 572                                     subst, menv, ug, eq_found)
 573                       )
 574                 | t ->
 575                     None
 576   in
 577   if Utils.debug_res then ignore(check_res res "demod_aux output");
 578   res
 579 ;;
 580
 581
 582 let build_newtarget_time = ref 0.;;
 583
 584
 585 let demod_counter = ref 1;;
 586
 587 exception Foo
 588
 589 let profiler = HExtlib.profile "P/Indexing.demod_eq[build_new_target]"
 590
 591 (** demodulation, when target is an equality *)
 592 let rec demodulation_equality ?from newmeta env table sign target =
 593   let module C = Cic in
 594   let module S = CicSubstitution in
 595   let module M = CicMetaSubst in
 596   let module HL = HelmLibraryObjects in
 597   let module U = Utils in
 598   let metasenv, context, ugraph = env in
 599   let w, proof, (eq_ty, left, right, order), metas = target in
 600   (* first, we simplify *)
 601   let right = U.guarded_simpl context right in
 602   let left = U.guarded_simpl context left in
 603   let order = !Utils.compare_terms left right in
 604   let stat = (eq_ty, left, right, order) in
 605   let w = Utils.compute_equality_weight stat in
 606   let target = w, proof, stat, metas in
 607   if Utils.debug_metas then
 608     ignore(check_target context target "demod equalities input");
 609   let metasenv' = (* metasenv @ *) metas in
 610   let maxmeta = ref newmeta in
 611
 612   let build_newtarget is_left (t, subst, menv, ug, (eq_found, eq_URI)) =
 613     let time1 = Unix.gettimeofday () in
 614
 615     if Utils.debug_metas then
 616       begin
 617         ignore(check_for_duplicates menv "input1");
 618         ignore(check_disjoint_invariant subst menv "input2");
 619         let substs = CicMetaSubst.ppsubst subst in
 620         ignore(check_target context (snd eq_found) ("input3" ^ substs))
 621       end;
 622     let pos, (_, proof', (ty, what, other, _), menv') = eq_found in
 623     let ty =
 624     try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
 625       with CicUtil.Meta_not_found _ -> ty
 626     in
 627     let what, other = if pos = Utils.Left then what, other else other, what in
 628     let newterm, newproof =
 629       let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
 630       let name = C.Name ("x_Demod" ^ (string_of_int !demod_counter)) in
 631       incr demod_counter;
 632       let bo' =
 633         let l, r = if is_left then t, S.lift 1 right else S.lift 1 left, t in
 634           C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
 635                   S.lift 1 eq_ty; l; r]
 636       in
 637       if sign = Utils.Positive then
 638           (bo,
 639            Inference.ProofBlock (
 640              subst, eq_URI, (name, ty), bo'(* t' *), eq_found, proof))
 641       else
 642         let metaproof =
 643           incr maxmeta;
 644           let irl =
 645             CicMkImplicit.identity_relocation_list_for_metavariable context in
 646 (*           debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta)); *)
 647 (*           print_newline (); *)
 648           C.Meta (!maxmeta, irl)
 649         in
 650           let eq_found =
 651             let proof' =
 652               let termlist =
 653                 if pos = Utils.Left then [ty; what; other]
 654                 else [ty; other; what]
 655               in
 656               Inference.ProofSymBlock (termlist, proof')
 657             in
 658             let what, other =
 659               if pos = Utils.Left then what, other else other, what
 660             in
 661             pos, (0, proof', (ty, other, what, Utils.Incomparable),menv')
 662           in
 663           let target_proof =
 664             let pb =
 665               Inference.ProofBlock (subst, eq_URI, (name, ty), bo',
 666                                     eq_found, Inference.BasicProof metaproof)
 667             in
 668             match proof with
 669             | Inference.BasicProof _ ->
 670                 (* print_endline "replacing a BasicProof"; *)
 671                 pb
 672             | Inference.ProofGoalBlock (_, parent_proof) ->
 673
 674   (* print_endline "replacing another ProofGoalBlock"; *)
 675                 Inference.ProofGoalBlock (pb, parent_proof)
 676             | _ -> assert false
 677           in
 678         let refl =
 679           C.Appl [C.MutConstruct (* reflexivity *)
 680                     (LibraryObjects.eq_URI (), 0, 1, []);
 681                   eq_ty; if is_left then right else left]
 682         in
 683         (bo,
 684          Inference.ProofGoalBlock (Inference.BasicProof refl, target_proof))
 685     in
 686     let newmenv = (* Inference.filter subst *) menv in
 687     let _ =
 688       if Utils.debug_metas then
 689         try ignore(CicTypeChecker.type_of_aux'
 690           newmenv context (Inference.build_proof_term newproof) ugraph);
 691           ()
 692         with exc ->
 693           prerr_endline "sempre lui";
 694           prerr_endline (CicMetaSubst.ppsubst subst);
 695           prerr_endline (CicPp.ppterm (Inference.build_proof_term newproof));
 696           prerr_endline ("+++++++++++++termine: " ^ (CicPp.ppterm t));
 697           prerr_endline ("+++++++++++++what: " ^ (CicPp.ppterm what));
 698           prerr_endline ("+++++++++++++other: " ^ (CicPp.ppterm other));
 699           prerr_endline ("+++++++++++++subst: " ^ (CicMetaSubst.ppsubst subst));
 700           raise exc;
 701       else ()
 702     in
 703     let left, right = if is_left then newterm, right else left, newterm in
 704     let ordering = !Utils.compare_terms left right in
 705     let stat = (eq_ty, left, right, ordering) in
 706     let time2 = Unix.gettimeofday () in
 707     build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
 708     let res =
 709       let w = Utils.compute_equality_weight stat in
 710       (w, newproof, stat,newmenv) in
 711     if Utils.debug_metas then
 712       ignore(check_target context res "buildnew_target output");
 713     !maxmeta, res
 714   in
 715   let build_newtarget is_left x =
 716     profiler.HExtlib.profile (build_newtarget is_left) x
 717   in
 718
 719   let res = demodulation_aux ~from:"3" metasenv' context ugraph table 0 left in
 720   if Utils.debug_res then check_res res "demod result";
 721   let newmeta, newtarget =
 722     match res with
 723     | Some t ->
 724         let newmeta, newtarget = build_newtarget true t in
 725           if (Inference.is_weak_identity (metasenv', context, ugraph) newtarget) ||
 726             (Inference.meta_convertibility_eq target newtarget) then
 727               newmeta, newtarget
 728           else
 729             demodulation_equality newmeta env table sign newtarget
 730     | None ->
 731         let res = demodulation_aux metasenv' context ugraph table 0 right in
 732         if Utils.debug_res then check_res res "demod result 1";
 733           match res with
 734           | Some t ->
 735               let newmeta, newtarget = build_newtarget false t in
 736                 if (Inference.is_weak_identity (metasenv', context, ugraph) newtarget) ||
 737                   (Inference.meta_convertibility_eq target newtarget) then
 738                     newmeta, newtarget
 739                 else
 740                    demodulation_equality newmeta env table sign newtarget
 741           | None ->
 742               newmeta, target
 743   in
 744   (* newmeta, newtarget *)
 745   newmeta,newtarget
 746 ;;
 747
 748 (**
 749    Performs the beta expansion of the term "term" w.r.t. "table",
 750    i.e. returns the list of all the terms t s.t. "(t term) = t2", for some t2
 751    in table.
 752 *)
 753 let rec betaexpand_term metasenv context ugraph table lift_amount term =
 754   let module C = Cic in
 755   let module S = CicSubstitution in
 756   let module M = CicMetaSubst in
 757   let module HL = HelmLibraryObjects in
 758   let candidates = get_candidates Unification table term in
 759
 760   let res, lifted_term =
 761     match term with
 762     | C.Meta (i, l) ->
 763         let l', lifted_l =
 764           List.fold_right
 765             (fun arg (res, lifted_tl) ->
 766                match arg with
 767                | Some arg ->
 768                    let arg_res, lifted_arg =
 769                      betaexpand_term metasenv context ugraph table
 770                        lift_amount arg in
 771                    let l1 =
 772                      List.map
 773                        (fun (t, s, m, ug, eq_found) ->
 774                           (Some t)::lifted_tl, s, m, ug, eq_found)
 775                        arg_res
 776                    in
 777                    (l1 @
 778                       (List.map
 779                          (fun (l, s, m, ug, eq_found) ->
 780                             (Some lifted_arg)::l, s, m, ug, eq_found)
 781                          res),
 782                     (Some lifted_arg)::lifted_tl)
 783                | None ->
 784                    (List.map
 785                       (fun (r, s, m, ug, eq_found) ->
 786                          None::r, s, m, ug, eq_found) res,
 787                     None::lifted_tl)
 788             ) l ([], [])
 789         in
 790         let e =
 791           List.map
 792             (fun (l, s, m, ug, eq_found) ->
 793                (C.Meta (i, l), s, m, ug, eq_found)) l'
 794         in
 795         e, C.Meta (i, lifted_l)
 796
 797     | C.Rel m ->
 798         [], if m <= lift_amount then C.Rel m else C.Rel (m+1)
 799
 800     | C.Prod (nn, s, t) ->
 801         let l1, lifted_s =
 802           betaexpand_term metasenv context ugraph table lift_amount s in
 803         let l2, lifted_t =
 804           betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
 805             table (lift_amount+1) t in
 806         let l1' =
 807           List.map
 808             (fun (t, s, m, ug, eq_found) ->
 809                C.Prod (nn, t, lifted_t), s, m, ug, eq_found) l1
 810         and l2' =
 811           List.map
 812             (fun (t, s, m, ug, eq_found) ->
 813                C.Prod (nn, lifted_s, t), s, m, ug, eq_found) l2 in
 814         l1' @ l2', C.Prod (nn, lifted_s, lifted_t)
 815
 816     | C.Lambda (nn, s, t) ->
 817         let l1, lifted_s =
 818           betaexpand_term metasenv context ugraph table lift_amount s in
 819         let l2, lifted_t =
 820           betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
 821             table (lift_amount+1) t in
 822         let l1' =
 823           List.map
 824             (fun (t, s, m, ug, eq_found) ->
 825                C.Lambda (nn, t, lifted_t), s, m, ug, eq_found) l1
 826         and l2' =
 827           List.map
 828             (fun (t, s, m, ug, eq_found) ->
 829                C.Lambda (nn, lifted_s, t), s, m, ug, eq_found) l2 in
 830         l1' @ l2', C.Lambda (nn, lifted_s, lifted_t)
 831
 832     | C.Appl l ->
 833         let l', lifted_l =
 834           List.fold_right
 835             (fun arg (res, lifted_tl) ->
 836                let arg_res, lifted_arg =
 837                  betaexpand_term metasenv context ugraph table lift_amount arg
 838                in
 839                let l1 =
 840                  List.map
 841                    (fun (a, s, m, ug, eq_found) ->
 842                       a::lifted_tl, s, m, ug, eq_found)
 843                    arg_res
 844                in
 845                (l1 @
 846                   (List.map
 847                      (fun (r, s, m, ug, eq_found) ->
 848                         lifted_arg::r, s, m, ug, eq_found)
 849                      res),
 850                 lifted_arg::lifted_tl)
 851             ) l ([], [])
 852         in
 853         (List.map
 854            (fun (l, s, m, ug, eq_found) -> (C.Appl l, s, m, ug, eq_found)) l',
 855          C.Appl lifted_l)
 856
 857     | t -> [], (S.lift lift_amount t)
 858   in
 859   match term with
 860   | C.Meta (i, l) -> res, lifted_term
 861   | term ->
 862       let termty, ugraph =
 863         C.Implicit None, ugraph
 864 (*         CicTypeChecker.type_of_aux' metasenv context term ugraph *)
 865       in
 866       let r =
 867         find_all_matches
 868           metasenv context ugraph lift_amount term termty candidates
 869       in
 870       r @ res, lifted_term
 871 ;;
 872
 873 let profiler = HExtlib.profile "P/Indexing.betaexpand_term"
 874
 875 let betaexpand_term metasenv context ugraph table lift_amount term =
 876   profiler.HExtlib.profile
 877     (betaexpand_term metasenv context ugraph table lift_amount) term
 878
 879
 880 let sup_l_counter = ref 1;;
 881
 882 (**
 883    superposition_left
 884    returns a list of new clauses inferred with a left superposition step
 885    the negative equation "target" and one of the positive equations in "table"
 886 *)
 887 let superposition_left newmeta (metasenv, context, ugraph) table target =
 888   let module C = Cic in
 889   let module S = CicSubstitution in
 890   let module M = CicMetaSubst in
 891   let module HL = HelmLibraryObjects in
 892   let module CR = CicReduction in
 893   let module U = Utils in
 894   let weight, proof, (eq_ty, left, right, ordering), menv = target in
 895   if Utils.debug_metas then
 896     ignore(check_target context target "superpositionleft");
 897   let expansions, _ =
 898     let term = if ordering = U.Gt then left else right in
 899       begin
 900         let t1 = Unix.gettimeofday () in
 901         let res = betaexpand_term metasenv context ugraph table 0 term in
 902         let t2 = Unix.gettimeofday () in
 903           beta_expand_time := !beta_expand_time  +. (t2 -. t1);
 904         res
 905       end
 906   in
 907   let maxmeta = ref newmeta in
 908   let build_new (bo, s, m, ug, (eq_found, eq_URI)) =
 909 (*     debug_print (lazy "\nSUPERPOSITION LEFT\n"); *)
 910     let time1 = Unix.gettimeofday () in
 911
 912     let pos, (_, proof', (ty, what, other, _), menv') = eq_found in
 913     let what, other = if pos = Utils.Left then what, other else other, what in
 914     let newgoal, newproof =
 915       let bo' =  U.guarded_simpl context (apply_subst s (S.subst other bo)) in
 916       let name = C.Name ("x_SupL_" ^ (string_of_int !sup_l_counter)) in
 917       incr sup_l_counter;
 918       let bo'' =
 919         let l, r =
 920           if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
 921         C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
 922                 S.lift 1 eq_ty; l; r]
 923       in
 924       incr maxmeta;
 925       let metaproof =
 926         let irl =
 927           CicMkImplicit.identity_relocation_list_for_metavariable context in
 928         C.Meta (!maxmeta, irl)
 929       in
 930       let eq_found =
 931         let proof' =
 932           let termlist =
 933             if pos = Utils.Left then [ty; what; other]
 934             else [ty; other; what]
 935           in
 936           Inference.ProofSymBlock (termlist, proof')
 937         in
 938         let what, other =
 939           if pos = Utils.Left then what, other else other, what
 940         in
 941         pos, (0, proof', (ty, other, what, Utils.Incomparable), menv')
 942       in
 943       let target_proof =
 944         let pb =
 945           Inference.ProofBlock (s, eq_URI, (name, ty), bo'', eq_found,
 946                                 Inference.BasicProof metaproof)
 947         in
 948         match proof with
 949         | Inference.BasicProof _ ->
 950 (*             debug_print (lazy "replacing a BasicProof"); *)
 951             pb
 952         | Inference.ProofGoalBlock (_, parent_proof) ->
 953 (*             debug_print (lazy "replacing another ProofGoalBlock"); *)
 954             Inference.ProofGoalBlock (pb, parent_proof)
 955         | _ -> assert false
 956       in
 957       let refl =
 958         C.Appl [C.MutConstruct (* reflexivity *)
 959                   (LibraryObjects.eq_URI (), 0, 1, []);
 960                 eq_ty; if ordering = U.Gt then right else left]
 961       in
 962       (bo',
 963        Inference.ProofGoalBlock (Inference.BasicProof refl, target_proof))
 964     in
 965     let left, right =
 966       if ordering = U.Gt then newgoal, right else left, newgoal in
 967     let neworder = !Utils.compare_terms left right in
 968     let stat = (eq_ty, left, right, neworder) in
 969     let newmenv = (* Inference.filter s *) menv in
 970     let time2 = Unix.gettimeofday () in
 971     build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
 972
 973     let w = Utils.compute_equality_weight stat in
 974     (w, newproof, stat, newmenv)
 975
 976   in
 977   !maxmeta, List.map build_new expansions
 978 ;;
 979
 980
 981 let sup_r_counter = ref 1;;
 982
 983 (**
 984    superposition_right
 985    returns a list of new clauses inferred with a right superposition step
 986    between the positive equation "target" and one in the "table" "newmeta" is
 987    the first free meta index, i.e. the first number above the highest meta
 988    index: its updated value is also returned
 989 *)
 990 let superposition_right newmeta (metasenv, context, ugraph) table target =
 991   let module C = Cic in
 992   let module S = CicSubstitution in
 993   let module M = CicMetaSubst in
 994   let module HL = HelmLibraryObjects in
 995   let module CR = CicReduction in
 996   let module U = Utils in
 997   let w, eqproof, (eq_ty, left, right, ordering), newmetas = target in
 998   if Utils.debug_metas then
 999     ignore (check_target context target "superpositionright");
1000   let metasenv' = newmetas in
1001   let maxmeta = ref newmeta in
1002   let res1, res2 =
1003     let betaexpand_term metasenv context ugraph table d term =
1004       let t1 = Unix.gettimeofday () in
1005       let res = betaexpand_term metasenv context ugraph table d term in
1006       let t2 = Unix.gettimeofday () in
1007         beta_expand_time := !beta_expand_time  +. (t2 -. t1);
1008         res
1009     in
1010     match ordering with
1011     | U.Gt -> fst (betaexpand_term metasenv' context ugraph table 0 left), []
1012     | U.Lt -> [], fst (betaexpand_term metasenv' context ugraph table 0 right)
1013     | _ ->
1014         let res l r =
1015           List.filter
1016             (fun (_, subst, _, _, _) ->
1017                let subst = apply_subst subst in
1018                let o = !Utils.compare_terms (subst l) (subst r) in
1019                o <> U.Lt && o <> U.Le)
1020             (fst (betaexpand_term metasenv' context ugraph table 0 l))
1021         in
1022         (res left right), (res right left)
1023   in
1024   let build_new ordering (bo, s, m, ug, (eq_found, eq_URI)) =
1025     if Utils.debug_metas then
1026       ignore (check_target context (snd eq_found) "buildnew1" );
1027     let time1 = Unix.gettimeofday () in
1028
1029     let pos, (_, proof', (ty, what, other, _), menv') = eq_found in
1030     let what, other = if pos = Utils.Left then what, other else other, what in
1031     let newgoal, newproof =
1032       (* qua *)
1033       let bo' = Utils.guarded_simpl context (apply_subst s (S.subst other bo)) in
1034       let name = C.Name ("x_SupR_" ^ (string_of_int !sup_r_counter)) in
1035       incr sup_r_counter;
1036       let bo'' =
1037         let l, r =
1038           if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
1039         C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
1040                 S.lift 1 eq_ty; l; r]
1041       in
1042       bo',
1043       Inference.ProofBlock (s, eq_URI, (name, ty), bo'', eq_found, eqproof)
1044     in
1045     let newmeta, newequality =
1046       let left, right =
1047         if ordering = U.Gt then newgoal, apply_subst s right
1048         else apply_subst s left, newgoal in
1049       let neworder = !Utils.compare_terms left right in
1050       let newmenv = (* Inference.filter s *) m in
1051       let stat = (eq_ty, left, right, neworder) in
1052       let eq' =
1053         let w = Utils.compute_equality_weight stat in
1054         (w, newproof, stat, newmenv) in
1055       if Utils.debug_metas then
1056         ignore (check_target context eq' "buildnew3");
1057       let newm, eq' = Inference.fix_metas !maxmeta eq' in
1058       if Utils.debug_metas then
1059         ignore (check_target context eq' "buildnew4");
1060       newm, eq'
1061     in
1062     maxmeta := newmeta;
1063     let time2 = Unix.gettimeofday () in
1064     build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
1065     if Utils.debug_metas then
1066       ignore(check_target context newequality "buildnew2");
1067     newequality
1068   in
1069   let new1 = List.map (build_new U.Gt) res1
1070   and new2 = List.map (build_new U.Lt) res2 in
1071   let ok e = not (Inference.is_identity (metasenv', context, ugraph) e) in
1072   (!maxmeta,
1073    (List.filter ok (new1 @ new2)))
1074 ;;
1075
1076
1077 (** demodulation, when the target is a goal *)
1078 let rec demodulation_goal newmeta env table goal =
1079   let module C = Cic in
1080   let module S = CicSubstitution in
1081   let module M = CicMetaSubst in
1082   let module HL = HelmLibraryObjects in
1083   let metasenv, context, ugraph = env in
1084   let maxmeta = ref newmeta in
1085   let proof, metas, term = goal in
1086   let term = Utils.guarded_simpl (~debug:true) context term in
1087   let goal = proof, metas, term in
1088   let metasenv' = metas in
1089
1090   let build_newgoal (t, subst, menv, ug, (eq_found, eq_URI)) =
1091     let pos, (_, proof', (ty, what, other, _), menv') = eq_found in
1092     let what, other = if pos = Utils.Left then what, other else other, what in
1093     let ty =
1094       try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
1095       with CicUtil.Meta_not_found _ -> ty
1096     in
1097     let newterm, newproof =
1098       let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
1099       let bo' = apply_subst subst t in
1100       let name = C.Name ("x_DemodGoal_" ^ (string_of_int !demod_counter)) in
1101       incr demod_counter;
1102       let metaproof =
1103         incr maxmeta;
1104         let irl =
1105           CicMkImplicit.identity_relocation_list_for_metavariable context in
1106 (*         debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta)); *)
1107         C.Meta (!maxmeta, irl)
1108       in
1109       let eq_found =
1110         let proof' =
1111           let termlist =
1112             if pos = Utils.Left then [ty; what; other]
1113             else [ty; other; what]
1114           in
1115           Inference.ProofSymBlock (termlist, proof')
1116         in
1117         let what, other =
1118           if pos = Utils.Left then what, other else other, what
1119         in
1120         pos, (0, proof', (ty, other, what, Utils.Incomparable), menv')
1121       in
1122       let goal_proof =
1123         let pb =
1124           Inference.ProofBlock (subst, eq_URI, (name, ty), bo',
1125                                 eq_found, Inference.BasicProof metaproof)
1126         in
1127         let rec repl = function
1128           | Inference.NoProof ->
1129 (*               debug_print (lazy "replacing a NoProof"); *)
1130               pb
1131           | Inference.BasicProof _ ->
1132 (*               debug_print (lazy "replacing a BasicProof"); *)
1133               pb
1134           | Inference.ProofGoalBlock (_, parent_proof) ->
1135 (*               debug_print (lazy "replacing another ProofGoalBlock"); *)
1136               Inference.ProofGoalBlock (pb, parent_proof)
1137           | Inference.SubProof (term, meta_index, p)  ->
1138               Inference.SubProof (term, meta_index, repl p)
1139           | _ -> assert false
1140         in repl proof
1141       in
1142       bo, Inference.ProofGoalBlock (Inference.NoProof, goal_proof)
1143     in
1144     let newmetasenv = (* Inference.filter subst *) menv in
1145     !maxmeta, (newproof, newmetasenv, newterm)
1146   in
1147   let res =
1148     demodulation_aux (* ~typecheck:true *) metasenv' context ugraph table 0 term
1149   in
1150   match res with
1151   | Some t ->
1152       let newmeta, newgoal = build_newgoal t in
1153       let _, _, newg = newgoal in
1154       if Inference.meta_convertibility term newg then
1155         newmeta, newgoal
1156       else
1157         demodulation_goal newmeta env table newgoal
1158   | None ->
1159       newmeta, goal
1160 ;;
1161
1162 (** demodulation, when the target is a theorem *)
1163 let rec demodulation_theorem newmeta env table theorem =
1164   let module C = Cic in
1165   let module S = CicSubstitution in
1166   let module M = CicMetaSubst in
1167   let module HL = HelmLibraryObjects in
1168   let metasenv, context, ugraph = env in
1169   let maxmeta = ref newmeta in
1170   let term, termty, metas = theorem in
1171   let metasenv' = metas in
1172
1173   let build_newtheorem (t, subst, menv, ug, (eq_found, eq_URI)) =
1174     let pos, (_, proof', (ty, what, other, _), menv') = eq_found in
1175     let what, other = if pos = Utils.Left then what, other else other, what in
1176     let newterm, newty =
1177       let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
1178       let bo' = apply_subst subst t in
1179       let name = C.Name ("x_DemodThm_" ^ (string_of_int !demod_counter)) in
1180       incr demod_counter;
1181       let newproof =
1182         Inference.ProofBlock (subst, eq_URI, (name, ty), bo', eq_found,
1183                               Inference.BasicProof term)
1184       in
1185       (Inference.build_proof_term newproof, bo)
1186     in
1187
1188     (* let m = Inference.metas_of_term newterm in *)
1189     !maxmeta, (newterm, newty, menv)
1190   in
1191   let res =
1192     demodulation_aux (* ~typecheck:true *) metasenv' context ugraph table 0 termty
1193   in
1194   match res with
1195   | Some t ->
1196       let newmeta, newthm = build_newtheorem t in
1197       let newt, newty, _ = newthm in
1198       if Inference.meta_convertibility termty newty then
1199         newmeta, newthm
1200       else
1201         demodulation_theorem newmeta env table newthm
1202   | None ->
1203       newmeta, theorem
1204 ;;
1205