helm/software/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 subst', menv', ug' =
 441             let t1 = Unix.gettimeofday () in
 442             try
 443               let other = Subst.apply_subst subst other in
 444               let r = unif_fun metasenv m context what other ugraph in
 445               let t2 = Unix.gettimeofday () in
 446               match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
 447               r
 448             with
 449               | Inference.MatchingFailure
 450               | CicUnification.UnificationFailure _ as e ->
 451               let t2 = Unix.gettimeofday () in
 452               match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
 453               raise e
 454           in
 455           (match Subst.merge_subst_if_possible subst subst' with
 456           | None -> ok what tl
 457           | Some s -> Some (s, equation))
 458         with
 459         | Inference.MatchingFailure
 460         | CicUnification.UnificationFailure _ -> ok what tl
 461   in
 462   match ok right leftr with
 463   | Some _ as res -> res
 464   | None ->
 465       let rightr =
 466         match right with
 467           | Cic.Meta _ when not use_unification -> []
 468           | _ ->
 469               let rightc = get_candidates predicate table right in
 470                 find_all_matches ~unif_fun
 471                   metasenv context ugraph 0 right ty rightc
 472       in
 473 (*        print_res rightr;*)
 474         ok left rightr
 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 ;;
 481
 482 let subsumption = subsumption_aux false;;
 483 let unification = subsumption_aux true;;
 484
 485 let rec demodulation_aux ?from ?(typecheck=false)
 486   metasenv context ugraph table lift_amount term =
 487   (* Printf.eprintf "term = %s\n" (CicPp.ppterm term); *)
 488   let module C = Cic in
 489   let module S = CicSubstitution in
 490   let module M = CicMetaSubst in
 491   let module HL = HelmLibraryObjects in
 492   let candidates =
 493     get_candidates ~env:(metasenv,context,ugraph) (* Unification *) Matching table term in
 494   if List.exists (fun (i,_,_) -> i = 2840) metasenv
 495   then
 496     (prerr_endline ("term: " ^(CicPp.ppterm term));
 497      List.iter (fun (_,x) -> prerr_endline (Equality.string_of_equality  x))
 498        candidates;
 499      prerr_endline ("-------");
 500      prerr_endline ("+++++++"));
 501   let res =
 502     match term with
 503       | C.Meta _ -> None
 504       | term ->
 505           let termty, ugraph =
 506             if typecheck then
 507               CicTypeChecker.type_of_aux' metasenv context term ugraph
 508             else
 509               C.Implicit None, ugraph
 510           in
 511           let res =
 512             find_matches metasenv context ugraph lift_amount term termty candidates
 513           in
 514           if Utils.debug_res then ignore(check_res res "demod1");
 515             if res <> None then
 516               res
 517             else
 518               match term with
 519                 | C.Appl l ->
 520                     let res, ll =
 521                       List.fold_left
 522                         (fun (res, tl) t ->
 523                            if res <> None then
 524                              (res, tl @ [S.lift 1 t])
 525                            else
 526                              let r =
 527                                demodulation_aux ~from:"1" metasenv context ugraph table
 528                                  lift_amount t
 529                              in
 530                                match r with
 531                                  | None -> (None, tl @ [S.lift 1 t])
 532                                  | Some (rel, _, _, _, _) -> (r, tl @ [rel]))
 533                         (None, []) l
 534                     in (
 535                         match res with
 536                           | None -> None
 537                           | Some (_, subst, menv, ug, eq_found) ->
 538                               Some (C.Appl ll, subst, menv, ug, eq_found)
 539                       )
 540                 | C.Prod (nn, s, t) ->
 541                     let r1 =
 542                       demodulation_aux ~from:"2"
 543                         metasenv context ugraph table lift_amount s in (
 544                         match r1 with
 545                           | None ->
 546                               let r2 =
 547                                 demodulation_aux metasenv
 548                                   ((Some (nn, C.Decl s))::context) ugraph
 549                                   table (lift_amount+1) t
 550                               in (
 551                                   match r2 with
 552                                     | None -> None
 553                                     | Some (t', subst, menv, ug, eq_found) ->
 554                                         Some (C.Prod (nn, (S.lift 1 s), t'),
 555                                               subst, menv, ug, eq_found)
 556                                 )
 557                           | Some (s', subst, menv, ug, eq_found) ->
 558                               Some (C.Prod (nn, s', (S.lift 1 t)),
 559                                     subst, menv, ug, eq_found)
 560                       )
 561                 | C.Lambda (nn, s, t) ->
 562                     let r1 =
 563                       demodulation_aux
 564                         metasenv context ugraph table lift_amount s in (
 565                         match r1 with
 566                           | None ->
 567                               let r2 =
 568                                 demodulation_aux metasenv
 569                                   ((Some (nn, C.Decl s))::context) ugraph
 570                                   table (lift_amount+1) t
 571                               in (
 572                                   match r2 with
 573                                     | None -> None
 574                                     | Some (t', subst, menv, ug, eq_found) ->
 575                                         Some (C.Lambda (nn, (S.lift 1 s), t'),
 576                                               subst, menv, ug, eq_found)
 577                                 )
 578                           | Some (s', subst, menv, ug, eq_found) ->
 579                               Some (C.Lambda (nn, s', (S.lift 1 t)),
 580                                     subst, menv, ug, eq_found)
 581                       )
 582                 | t ->
 583                     None
 584   in
 585   if Utils.debug_res then ignore(check_res res "demod_aux output");
 586   res
 587 ;;
 588
 589
 590 let build_newtarget_time = ref 0.;;
 591
 592
 593 let demod_counter = ref 1;;
 594
 595 exception Foo
 596
 597 let profiler = HExtlib.profile "P/Indexing.demod_eq[build_new_target]"
 598
 599 (** demodulation, when target is an equality *)
 600 let rec demodulation_equality ?from newmeta env table sign target =
 601   let module C = Cic in
 602   let module S = CicSubstitution in
 603   let module M = CicMetaSubst in
 604   let module HL = HelmLibraryObjects in
 605   let module U = Utils in
 606   let metasenv, context, ugraph = env in
 607   let w, proof, (eq_ty, left, right, order), metas, id =
 608     Equality.open_equality target
 609   in
 610   (* first, we simplify *)
 611 (*   let right = U.guarded_simpl context right in *)
 612 (*   let left = U.guarded_simpl context left in *)
 613 (*   let order = !Utils.compare_terms left right in *)
 614 (*   let stat = (eq_ty, left, right, order) in  *)
 615 (*  let w = Utils.compute_equality_weight stat in*)
 616   (* let target = Equality.mk_equality (w, proof, stat, metas) in *)
 617   if Utils.debug_metas then
 618     ignore(check_target context target "demod equalities input");
 619   let metasenv' = (* metasenv @ *) metas in
 620   let maxmeta = ref newmeta in
 621
 622   let build_newtarget is_left (t, subst, menv, ug, (eq_found, eq_URI)) =
 623     let time1 = Unix.gettimeofday () in
 624
 625     if Utils.debug_metas then
 626       begin
 627         ignore(check_for_duplicates menv "input1");
 628         ignore(check_disjoint_invariant subst menv "input2");
 629         let substs = Subst.ppsubst subst in
 630         ignore(check_target context (snd eq_found) ("input3" ^ substs))
 631       end;
 632     let pos, equality = eq_found in
 633     let (_, proof',
 634         (ty, what, other, _), menv',id') = Equality.open_equality equality in
 635     let ty =
 636       try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
 637       with CicUtil.Meta_not_found _ -> ty
 638     in
 639     let what, other = if pos = Utils.Left then what, other else other, what in
 640     let newterm, newproof =
 641       let bo =
 642         Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
 643 (*      let name = C.Name ("x_Demod" ^ (string_of_int !demod_counter)) in*)
 644       let name = C.Name "x" in
 645       incr demod_counter;
 646       let bo' =
 647         let l, r = if is_left then t, S.lift 1 right else S.lift 1 left, t in
 648           C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
 649                   S.lift 1 eq_ty; l; r]
 650       in
 651       if sign = Utils.Positive then
 652           (bo, (Equality.Step (subst,(Equality.Demodulation, id,(pos,id'),
 653           (Cic.Lambda (name, ty, bo'))))))
 654       else
 655         assert false
 656 (*
 657         begin
 658         prerr_endline "***************************************negative";
 659         let metaproof =
 660           incr maxmeta;
 661           let irl =
 662             CicMkImplicit.identity_relocation_list_for_metavariable context in
 663 (*        debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta)); *)
 664 (*        print_newline (); *)
 665           C.Meta (!maxmeta, irl)
 666         in
 667           let eq_found =
 668             let proof'_old' =
 669               let termlist =
 670                 if pos = Utils.Left then [ty; what; other]
 671                 else [ty; other; what]
 672               in
 673               Equality.ProofSymBlock (termlist, proof'_old)
 674             in
 675             let proof'_new' = assert false (* not implemented *) in
 676             let what, other =
 677               if pos = Utils.Left then what, other else other, what
 678             in
 679             pos,
 680               Equality.mk_equality
 681                 (0, (proof'_new',proof'_old'),
 682                 (ty, other, what, Utils.Incomparable),menv')
 683           in
 684           let target_proof =
 685             let pb =
 686               Equality.ProofBlock
 687                 (subst, eq_URI, (name, ty), bo',
 688                  eq_found, Equality.BasicProof (Equality.empty_subst,metaproof))
 689             in
 690             assert false, (* not implemented *)
 691             (match snd proof with
 692             | Equality.BasicProof _ ->
 693                 (* print_endline "replacing a BasicProof"; *)
 694                 pb
 695             | Equality.ProofGoalBlock (_, parent_proof) ->
 696   (* print_endline "replacing another ProofGoalBlock"; *)
 697                 Equality.ProofGoalBlock (pb, parent_proof)
 698             | _ -> assert false)
 699           in
 700         let refl =
 701           C.Appl [C.MutConstruct (* reflexivity *)
 702                     (LibraryObjects.eq_URI (), 0, 1, []);
 703                   eq_ty; if is_left then right else left]
 704         in
 705         (bo,
 706          (assert false, (* not implemented *)
 707          Equality.ProofGoalBlock
 708            (Equality.BasicProof (Equality.empty_subst,refl), snd target_proof)))
 709       end
 710 *)
 711     in
 712     let newmenv = (* Inference.filter subst *) menv in
 713     let _ =
 714       if Utils.debug_metas then
 715         try ignore(CicTypeChecker.type_of_aux'
 716           newmenv context
 717             (Equality.build_proof_term newproof) ugraph);
 718           ()
 719         with exc ->
 720           prerr_endline "sempre lui";
 721           prerr_endline (Subst.ppsubst subst);
 722           prerr_endline (CicPp.ppterm
 723             (Equality.build_proof_term newproof));
 724           prerr_endline ("+++++++++++++termine: " ^ (CicPp.ppterm t));
 725           prerr_endline ("+++++++++++++what: " ^ (CicPp.ppterm what));
 726           prerr_endline ("+++++++++++++other: " ^ (CicPp.ppterm other));
 727           prerr_endline ("+++++++++++++subst: " ^ (Subst.ppsubst subst));
 728           prerr_endline ("+++++++++++++newmenv: " ^ (CicMetaSubst.ppmetasenv []
 729             newmenv));
 730           raise exc;
 731       else ()
 732     in
 733     let left, right = if is_left then newterm, right else left, newterm in
 734     let ordering = !Utils.compare_terms left right in
 735     let stat = (eq_ty, left, right, ordering) in
 736     let time2 = Unix.gettimeofday () in
 737     build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
 738     let res =
 739       let w = Utils.compute_equality_weight stat in
 740       Equality.mk_equality (w, newproof, stat,newmenv)
 741     in
 742     if Utils.debug_metas then
 743       ignore(check_target context res "buildnew_target output");
 744     !maxmeta, res
 745   in
 746   let build_newtarget is_left x =
 747     profiler.HExtlib.profile (build_newtarget is_left) x
 748   in
 749
 750   let res = demodulation_aux ~from:"3" metasenv' context ugraph table 0 left in
 751   if Utils.debug_res then check_res res "demod result";
 752   let newmeta, newtarget =
 753     match res with
 754     | Some t ->
 755         let newmeta, newtarget = build_newtarget true t in
 756           assert (not (Equality.meta_convertibility_eq target newtarget));
 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         let res = demodulation_aux metasenv' context ugraph table 0 right in
 764         if Utils.debug_res then check_res res "demod result 1";
 765           match res with
 766           | Some t ->
 767               let newmeta, newtarget = build_newtarget false t in
 768                 if (Equality.is_weak_identity newtarget) ||
 769                   (Equality.meta_convertibility_eq target newtarget) then
 770                     newmeta, newtarget
 771                 else
 772                    demodulation_equality ?from newmeta env table sign newtarget
 773           | None ->
 774               newmeta, target
 775   in
 776   (* newmeta, newtarget *)
 777   newmeta,newtarget
 778 ;;
 779
 780 (**
 781    Performs the beta expansion of the term "term" w.r.t. "table",
 782    i.e. returns the list of all the terms t s.t. "(t term) = t2", for some t2
 783    in table.
 784 *)
 785 let rec betaexpand_term metasenv context ugraph table lift_amount term =
 786   let module C = Cic in
 787   let module S = CicSubstitution in
 788   let module M = CicMetaSubst in
 789   let module HL = HelmLibraryObjects in
 790   let candidates = get_candidates Unification table term in
 791
 792   let res, lifted_term =
 793     match term with
 794     | C.Meta (i, l) ->
 795         let l', lifted_l =
 796           List.fold_right
 797             (fun arg (res, lifted_tl) ->
 798                match arg with
 799                | Some arg ->
 800                    let arg_res, lifted_arg =
 801                      betaexpand_term metasenv context ugraph table
 802                        lift_amount arg in
 803                    let l1 =
 804                      List.map
 805                        (fun (t, s, m, ug, eq_found) ->
 806                           (Some t)::lifted_tl, s, m, ug, eq_found)
 807                        arg_res
 808                    in
 809                    (l1 @
 810                       (List.map
 811                          (fun (l, s, m, ug, eq_found) ->
 812                             (Some lifted_arg)::l, s, m, ug, eq_found)
 813                          res),
 814                     (Some lifted_arg)::lifted_tl)
 815                | None ->
 816                    (List.map
 817                       (fun (r, s, m, ug, eq_found) ->
 818                          None::r, s, m, ug, eq_found) res,
 819                     None::lifted_tl)
 820             ) l ([], [])
 821         in
 822         let e =
 823           List.map
 824             (fun (l, s, m, ug, eq_found) ->
 825                (C.Meta (i, l), s, m, ug, eq_found)) l'
 826         in
 827         e, C.Meta (i, lifted_l)
 828
 829     | C.Rel m ->
 830         [], if m <= lift_amount then C.Rel m else C.Rel (m+1)
 831
 832     | C.Prod (nn, s, t) ->
 833         let l1, lifted_s =
 834           betaexpand_term metasenv context ugraph table lift_amount s in
 835         let l2, lifted_t =
 836           betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
 837             table (lift_amount+1) t in
 838         let l1' =
 839           List.map
 840             (fun (t, s, m, ug, eq_found) ->
 841                C.Prod (nn, t, lifted_t), s, m, ug, eq_found) l1
 842         and l2' =
 843           List.map
 844             (fun (t, s, m, ug, eq_found) ->
 845                C.Prod (nn, lifted_s, t), s, m, ug, eq_found) l2 in
 846         l1' @ l2', C.Prod (nn, lifted_s, lifted_t)
 847
 848     | C.Lambda (nn, s, t) ->
 849         let l1, lifted_s =
 850           betaexpand_term metasenv context ugraph table lift_amount s in
 851         let l2, lifted_t =
 852           betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
 853             table (lift_amount+1) t in
 854         let l1' =
 855           List.map
 856             (fun (t, s, m, ug, eq_found) ->
 857                C.Lambda (nn, t, lifted_t), s, m, ug, eq_found) l1
 858         and l2' =
 859           List.map
 860             (fun (t, s, m, ug, eq_found) ->
 861                C.Lambda (nn, lifted_s, t), s, m, ug, eq_found) l2 in
 862         l1' @ l2', C.Lambda (nn, lifted_s, lifted_t)
 863
 864     | C.Appl l ->
 865         let l', lifted_l =
 866           List.fold_right
 867             (fun arg (res, lifted_tl) ->
 868                let arg_res, lifted_arg =
 869                  betaexpand_term metasenv context ugraph table lift_amount arg
 870                in
 871                let l1 =
 872                  List.map
 873                    (fun (a, s, m, ug, eq_found) ->
 874                       a::lifted_tl, s, m, ug, eq_found)
 875                    arg_res
 876                in
 877                (l1 @
 878                   (List.map
 879                      (fun (r, s, m, ug, eq_found) ->
 880                         lifted_arg::r, s, m, ug, eq_found)
 881                      res),
 882                 lifted_arg::lifted_tl)
 883             ) l ([], [])
 884         in
 885         (List.map
 886            (fun (l, s, m, ug, eq_found) -> (C.Appl l, s, m, ug, eq_found)) l',
 887          C.Appl lifted_l)
 888
 889     | t -> [], (S.lift lift_amount t)
 890   in
 891   match term with
 892   | C.Meta (i, l) -> res, lifted_term
 893   | term ->
 894       let termty, ugraph =
 895         C.Implicit None, ugraph
 896 (*         CicTypeChecker.type_of_aux' metasenv context term ugraph *)
 897       in
 898       let r =
 899         find_all_matches
 900           metasenv context ugraph lift_amount term termty candidates
 901       in
 902       r @ res, lifted_term
 903 ;;
 904
 905 let profiler = HExtlib.profile "P/Indexing.betaexpand_term"
 906
 907 let betaexpand_term metasenv context ugraph table lift_amount term =
 908   profiler.HExtlib.profile
 909     (betaexpand_term metasenv context ugraph table lift_amount) term
 910
 911
 912 let sup_l_counter = ref 1;;
 913
 914 (**
 915    superposition_left
 916    returns a list of new clauses inferred with a left superposition step
 917    the negative equation "target" and one of the positive equations in "table"
 918 *)
 919
 920 let build_newgoal context goalproof (t, subst, menv, ug, (eq_found, eq_URI)) =
 921   let pos, equality = eq_found in
 922   let (_, proof', (ty, what, other, _), menv',id) =
 923     Equality.open_equality equality in
 924   let what, other = if pos = Utils.Left then what, other else other, what in
 925   let newterm, newgoalproof =
 926     let bo =
 927       Utils.guarded_simpl context
 928         (apply_subst subst (CicSubstitution.subst other t))
 929     in
 930     let bo' = (*apply_subst subst*) t in
 931     let name = Cic.Name "x" in
 932     let newgoalproofstep = (pos,id,subst,Cic.Lambda (name,ty,bo')) in
 933     bo, (newgoalproofstep::goalproof)
 934   in
 935   let newmetasenv = (* Inference.filter subst *) menv in
 936   (newgoalproof, newmetasenv, newterm)
 937 ;;
 938
 939 let superposition_left
 940   (metasenv, context, ugraph) table (proof,menv,ty)
 941 =
 942   let module C = Cic in
 943   let module S = CicSubstitution in
 944   let module M = CicMetaSubst in
 945   let module HL = HelmLibraryObjects in
 946   let module CR = CicReduction in
 947   let module U = Utils in
 948   let big,small,pos,eq,ty =
 949     match ty with
 950     | Cic.Appl [eq;ty;l;r] ->
 951        let c =
 952          Utils.compare_weights ~normalize:true
 953            (Utils.weight_of_term l) (Utils.weight_of_term r)
 954        in
 955        (match c with
 956        | Utils.Gt -> l,r,Utils.Right,eq,ty
 957        | _ -> r,l,Utils.Left,eq,ty)
 958     | _ -> assert false
 959   in
 960   let small = CicSubstitution.lift 1 small in
 961   let ty = CicSubstitution.lift 1 ty in
 962   let expansions, _ = betaexpand_term menv context ugraph table 0 big in
 963   let fix_preds (t, subst, menv, ug, (eq_found, eq_URI)) =
 964     let pred =
 965       match pos with
 966       | Utils.Left ->
 967           Cic.Appl [eq;ty;small;t]
 968       | Utils.Right ->
 969           Cic.Appl [eq;ty;t;small]
 970     in
 971     (pred, subst, menv, ug, (eq_found, eq_URI))
 972   in
 973   List.map (build_newgoal context proof)
 974     (List.map fix_preds expansions)
 975 ;;
 976
 977 let sup_r_counter = ref 1;;
 978
 979 (**
 980    superposition_right
 981    returns a list of new clauses inferred with a right superposition step
 982    between the positive equation "target" and one in the "table" "newmeta" is
 983    the first free meta index, i.e. the first number above the highest meta
 984    index: its updated value is also returned
 985 *)
 986 let superposition_right newmeta (metasenv, context, ugraph) table target =
 987   let module C = Cic in
 988   let module S = CicSubstitution in
 989   let module M = CicMetaSubst in
 990   let module HL = HelmLibraryObjects in
 991   let module CR = CicReduction in
 992   let module U = Utils in
 993   let w, eqproof, (eq_ty, left, right, ordering), newmetas,id =
 994     Equality.open_equality target
 995   in
 996   if Utils.debug_metas then
 997     ignore (check_target context target "superpositionright");
 998   let metasenv' = newmetas in
 999   let maxmeta = ref newmeta in
1000   let res1, res2 =
1001     let betaexpand_term metasenv context ugraph table d term =
1002       let t1 = Unix.gettimeofday () in
1003       let res = betaexpand_term metasenv context ugraph table d term in
1004       let t2 = Unix.gettimeofday () in
1005         beta_expand_time := !beta_expand_time  +. (t2 -. t1);
1006         res
1007     in
1008     match ordering with
1009     | U.Gt -> fst (betaexpand_term metasenv' context ugraph table 0 left), []
1010     | U.Lt -> [], fst (betaexpand_term metasenv' context ugraph table 0 right)
1011     | _ ->
1012         let res l r =
1013           List.filter
1014             (fun (_, subst, _, _, _) ->
1015                let subst = apply_subst subst in
1016                let o = !Utils.compare_terms (subst l) (subst r) in
1017                o <> U.Lt && o <> U.Le)
1018             (fst (betaexpand_term metasenv' context ugraph table 0 l))
1019         in
1020         (res left right), (res right left)
1021   in
1022   let build_new ordering (bo, s, m, ug, (eq_found, eq_URI)) =
1023     if Utils.debug_metas then
1024       ignore (check_target context (snd eq_found) "buildnew1" );
1025     let time1 = Unix.gettimeofday () in
1026
1027     let pos, equality =  eq_found in
1028     let (_, proof', (ty, what, other, _), menv',id') =
1029       Equality.open_equality  equality in
1030     let what, other = if pos = Utils.Left then what, other else other, what in
1031     let newgoal, newproof =
1032       (* qua *)
1033       let bo' =
1034         Utils.guarded_simpl context (apply_subst s (S.subst other bo))
1035       in
1036       let name = C.Name "x" in
1037       incr sup_r_counter;
1038       let bo'' =
1039         let l, r =
1040           if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
1041         C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
1042                 S.lift 1 eq_ty; l; r]
1043       in
1044       bo',
1045         Equality.Step
1046           (s,(Equality.SuperpositionRight,
1047                id,(pos,id'),(Cic.Lambda(name,ty,bo''))))
1048     in
1049     let newmeta, newequality =
1050       let left, right =
1051         if ordering = U.Gt then newgoal, apply_subst s right
1052         else apply_subst s left, newgoal in
1053       let neworder = !Utils.compare_terms left right in
1054       let newmenv = (* Inference.filter s *) m in
1055       let stat = (eq_ty, left, right, neworder) in
1056       let eq' =
1057         let w = Utils.compute_equality_weight stat in
1058         Equality.mk_equality (w, newproof, stat, newmenv) in
1059       if Utils.debug_metas then
1060         ignore (check_target context eq' "buildnew3");
1061       let newm, eq' = Equality.fix_metas !maxmeta eq' in
1062       if Utils.debug_metas then
1063         ignore (check_target context eq' "buildnew4");
1064       newm, eq'
1065     in
1066     maxmeta := newmeta;
1067     let time2 = Unix.gettimeofday () in
1068     build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
1069     if Utils.debug_metas then
1070       ignore(check_target context newequality "buildnew2");
1071     newequality
1072   in
1073   let new1 = List.map (build_new U.Gt) res1
1074   and new2 = List.map (build_new U.Lt) res2 in
1075   let ok e = not (Equality.is_identity (metasenv', context, ugraph) e) in
1076   (!maxmeta,
1077    (List.filter ok (new1 @ new2)))
1078 ;;
1079
1080
1081 (** demodulation, when the target is a goal *)
1082 let rec demodulation_goal newmeta env table goal =
1083   let module C = Cic in
1084   let module S = CicSubstitution in
1085   let module M = CicMetaSubst in
1086   let module HL = HelmLibraryObjects in
1087   let metasenv, context, ugraph = env in
1088   let maxmeta = ref newmeta in
1089   let goalproof, metas, term = goal in
1090   let term = Utils.guarded_simpl (~debug:true) context term in
1091   let goal = goalproof, metas, term in
1092   let metasenv' = metas in
1093
1094   let build_newgoal (t, subst, menv, ug, (eq_found, eq_URI)) =
1095     let pos, equality = eq_found in
1096     let (_, proof', (ty, what, other, _), menv',id) =
1097       Equality.open_equality equality in
1098     let what, other = if pos = Utils.Left then what, other else other, what in
1099     let ty =
1100       try fst (CicTypeChecker.type_of_aux' menv' context what ugraph)
1101       with
1102       | CicUtil.Meta_not_found _
1103       | Invalid_argument("List.fold_left2") -> ty
1104     in
1105     let newterm, newgoalproof =
1106       let bo =
1107         Utils.guarded_simpl context (apply_subst subst(S.subst other t))
1108       in
1109       let bo' = (*apply_subst subst*) t in
1110       let name = C.Name "x" in
1111       incr demod_counter;
1112       let newgoalproofstep = (pos,id,subst,Cic.Lambda (name,ty,bo')) in
1113       bo, (newgoalproofstep::goalproof)
1114     in
1115     let newmetasenv = (* Inference.filter subst *) menv in
1116     !maxmeta, (newgoalproof, newmetasenv, newterm)
1117   in
1118   let res =
1119     demodulation_aux (* ~typecheck:true *) metasenv' context ugraph table 0 term
1120   in
1121   match res with
1122   | Some t ->
1123       let newmeta, newgoal = build_newgoal t in
1124       let _, _, newg = newgoal in
1125       if Equality.meta_convertibility term newg then
1126         false, newmeta, newgoal
1127       else
1128         let changed, newmeta, newgoal =
1129           demodulation_goal newmeta env table newgoal
1130         in
1131         true, newmeta, newgoal
1132   | None ->
1133       false, newmeta, goal
1134 ;;
1135
1136 (** demodulation, when the target is a theorem *)
1137 let rec demodulation_theorem newmeta env table theorem =
1138   let module C = Cic in
1139   let module S = CicSubstitution in
1140   let module M = CicMetaSubst in
1141   let module HL = HelmLibraryObjects in
1142   let metasenv, context, ugraph = env in
1143   let maxmeta = ref newmeta in
1144   let term, termty, metas = theorem in
1145   let metasenv' = metas in
1146
1147   let build_newtheorem (t, subst, menv, ug, (eq_found, eq_URI)) =
1148     let pos, equality = eq_found in
1149     let (_, proof', (ty, what, other, _), menv',id) =
1150       Equality.open_equality equality in
1151     let what, other = if pos = Utils.Left then what, other else other, what in
1152     let newterm, newty =
1153       let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
1154 (*      let bo' = apply_subst subst t in *)
1155 (*      let name = C.Name ("x_DemodThm_" ^ (string_of_int !demod_counter)) in*)
1156       incr demod_counter;
1157 (*
1158       let newproofold =
1159         Equality.ProofBlock (subst, eq_URI, (name, ty), bo', eq_found,
1160                               Equality.BasicProof (Equality.empty_subst,term))
1161       in
1162       (Equality.build_proof_term_old newproofold, bo)
1163 *)
1164       (* TODO, not ported to the new proofs *)
1165       if true then assert false; term, bo
1166     in
1167     !maxmeta, (newterm, newty, menv)
1168   in
1169   let res =
1170     demodulation_aux (* ~typecheck:true *) metasenv' context ugraph table 0 termty
1171   in
1172   match res with
1173   | Some t ->
1174       let newmeta, newthm = build_newtheorem t in
1175       let newt, newty, _ = newthm in
1176       if Equality.meta_convertibility termty newty then
1177         newmeta, newthm
1178       else
1179         demodulation_theorem newmeta env table newthm
1180   | None ->
1181       newmeta, theorem
1182 ;;
1183