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