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