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         prerr_endline (". " ^ Equality.string_of_equality equality);
 246         let (_, proof, (ty, left, right, o), metas,_) =
 247           Equality.open_equality equality
 248         in
 249         if Utils.debug_metas then
 250           ignore(check_target context (snd candidate) "find_matches");
 251         if Utils.debug_res then
 252           begin
 253             let c="eq = "^(Equality.string_of_equality (snd candidate)) ^ "\n"in
 254             let t="t = " ^ (CicPp.ppterm term) ^ "\n" in
 255             let m="metas = " ^ (CicMetaSubst.ppmetasenv [] metas) ^ "\n" in
 256             let p="proof = "^
 257               (CicPp.ppterm(Equality.build_proof_term proof))^"\n"
 258             in
 259               check_for_duplicates metas "gia nella metas";
 260               check_for_duplicates (metasenv@metas) ("not disjoint"^c^t^m^p)
 261           end;
 262         if check && not (fst (CicReduction.are_convertible
 263                                 ~metasenv context termty ty ugraph)) then (
 264           find_matches metasenv context ugraph lift_amount term termty tl
 265         ) else
 266           let do_match c eq_URI =
 267             let subst', metasenv', ugraph' =
 268               let t1 = Unix.gettimeofday () in
 269               try
 270                 let r =
 271                   ( Inference.matching metasenv metas context
 272                     term (S.lift lift_amount c)) ugraph
 273                 in
 274                 let t2 = Unix.gettimeofday () in
 275                 match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
 276                 r
 277               with
 278                 | Inference.MatchingFailure as e ->
 279                 let t2 = Unix.gettimeofday () in
 280                 match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
 281                   raise e
 282                 | CicUtil.Meta_not_found _ as exn -> raise exn
 283             in
 284             Some (Cic.Rel (1 + lift_amount), subst', metasenv', ugraph',
 285                   (candidate, eq_URI))
 286           in
 287           let c, other, eq_URI =
 288             if pos = Utils.Left then left, right, Utils.eq_ind_URI ()
 289             else right, left, Utils.eq_ind_r_URI ()
 290           in
 291           if o <> U.Incomparable then
 292             let res =
 293               try
 294                 do_match c eq_URI
 295               with Inference.MatchingFailure ->
 296                 find_matches metasenv context ugraph lift_amount term termty tl
 297             in
 298               if Utils.debug_res then ignore (check_res res "find1");
 299               res
 300           else
 301             let res =
 302               try do_match c eq_URI
 303               with Inference.MatchingFailure -> None
 304             in
 305             if Utils.debug_res then ignore (check_res res "find2");
 306             match res with
 307             | Some (_, s, _, _, _) ->
 308                 let c' = apply_subst s c in
 309                 (*
 310              let other' = U.guarded_simpl context (apply_subst s other) in *)
 311                 let other' = apply_subst s other in
 312                 let order = cmp c' other' in
 313                 if order = U.Gt then
 314                   res
 315                 else
 316                   find_matches
 317                     metasenv context ugraph lift_amount term termty tl
 318             | None ->
 319                 find_matches metasenv context ugraph lift_amount term termty tl
 320 ;;
 321
 322 (*
 323   as above, but finds all the matching equalities, and the matching condition
 324   can be either Inference.matching or Inference.unification
 325 *)
 326 let rec find_all_matches ?(unif_fun=Inference.unification)
 327     metasenv context ugraph lift_amount term termty =
 328   let module C = Cic in
 329   let module U = Utils in
 330   let module S = CicSubstitution in
 331   let module M = CicMetaSubst in
 332   let module HL = HelmLibraryObjects in
 333   let cmp = !Utils.compare_terms in
 334   function
 335     | [] -> []
 336     | candidate::tl ->
 337         let pos, equality = candidate in
 338         let (_,_,(ty,left,right,o),metas,_)=Equality.open_equality equality in
 339         let do_match c eq_URI =
 340           let subst', metasenv', ugraph' =
 341             let t1 = Unix.gettimeofday () in
 342             try
 343                 let term =
 344                   match c,term with
 345                   | Cic.Meta _, Cic.Appl[Cic.MutInd(u,0,_);_;l;r]
 346                     when  LibraryObjects.is_eq_URI u -> l
 347 (*
 348                       if Utils.compare_weights (Utils.weight_of_term l)
 349                          (Utils.weight_of_term r) = Utils.Gt
 350                       then l else r
 351 *)
 352                   | _ -> term
 353                 in
 354
 355               let r =
 356                 unif_fun metasenv metas context
 357                   term (S.lift lift_amount c) ugraph in
 358               let t2 = Unix.gettimeofday () in
 359               match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
 360               r
 361             with
 362             | Inference.MatchingFailure
 363             | CicUnification.UnificationFailure _
 364             | CicUnification.Uncertain _ as e ->
 365                 let t2 = Unix.gettimeofday () in
 366                 match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
 367                 raise e
 368           in
 369           (C.Rel (1 + lift_amount), subst', metasenv', ugraph',
 370            (candidate, eq_URI))
 371         in
 372         let c, other, eq_URI =
 373           if pos = Utils.Left then left, right, Utils.eq_ind_URI ()
 374           else right, left, Utils.eq_ind_r_URI ()
 375         in
 376         if o <> U.Incomparable then
 377           try
 378             let res = do_match c eq_URI in
 379             res::(find_all_matches ~unif_fun metasenv context ugraph
 380                     lift_amount term termty tl)
 381           with
 382           | Inference.MatchingFailure
 383           | CicUnification.UnificationFailure _
 384           | CicUnification.Uncertain _ ->
 385               find_all_matches ~unif_fun metasenv context ugraph
 386                 lift_amount term termty tl
 387         else
 388           try
 389             let res = do_match c eq_URI in
 390             match res with
 391             | _, s, _, _, _ ->
 392                 let c' = apply_subst s c
 393                 and other' = apply_subst s other in
 394                 let order = cmp c' other' in
 395                 if order <> U.Lt && order <> U.Le then
 396                   res::(find_all_matches ~unif_fun metasenv context ugraph
 397                           lift_amount term termty tl)
 398                 else
 399                   find_all_matches ~unif_fun metasenv context ugraph
 400                     lift_amount term termty tl
 401           with
 402           | Inference.MatchingFailure
 403           | CicUnification.UnificationFailure _
 404           | CicUnification.Uncertain _ ->
 405               find_all_matches ~unif_fun metasenv context ugraph
 406                 lift_amount term termty tl
 407 ;;
 408
 409 let find_all_matches
 410   ?unif_fun metasenv context ugraph lift_amount term termty l
 411 =
 412   let rc =
 413     find_all_matches
 414       ?unif_fun metasenv context ugraph lift_amount term termty l
 415   in
 416   (*prerr_endline "CANDIDATES:";
 417   List.iter (fun (_,x)->prerr_endline (Inference.string_of_equality x)) l;
 418   prerr_endline ("MATCHING:" ^ CicPp.ppterm term ^ " are " ^ string_of_int
 419   (List.length rc));*)
 420   rc
 421
 422 (*
 423   returns true if target is subsumed by some equality in table
 424 *)
 425 let subsumption_aux use_unification env table target =
 426 (*  let print_res l =*)
 427 (*    prerr_endline (String.concat "\n" (List.map (fun (_, subst, menv, ug,*)
 428 (*    ((pos,equation),_)) -> Equality.string_of_equality equation)l))*)
 429 (*  in*)
 430   let _, _, (ty, left, right, _), tmetas, _ = Equality.open_equality target in
 431   let metasenv, context, ugraph = env in
 432   let metasenv = tmetas in
 433   let predicate, unif_fun =
 434     if use_unification then
 435       Unification, Inference.unification
 436     else
 437       Matching, Inference.matching
 438   in
 439   let leftr =
 440     match left with
 441     | Cic.Meta _ when not use_unification -> []
 442     | _ ->
 443         let leftc = get_candidates predicate table left in
 444         find_all_matches ~unif_fun
 445           metasenv context ugraph 0 left ty leftc
 446   in
 447 (*  print_res leftr;*)
 448   let rec ok what = function
 449     | [] -> None
 450     | (_, subst, menv, ug, ((pos,equation),_))::tl ->
 451         let _, _, (_, l, r, o), m,_ = Equality.open_equality equation in
 452         try
 453           let other = if pos = Utils.Left then r else l in
 454           let what' = Subst.apply_subst subst what in
 455           let subst', menv', ug' =
 456             unif_fun metasenv m context what' other ugraph
 457           in
 458           (match Subst.merge_subst_if_possible subst subst' with
 459           | None -> ok what tl
 460           | Some s -> Some (s, equation))
 461         with
 462         | Inference.MatchingFailure
 463         | CicUnification.UnificationFailure _ -> ok what tl
 464   in
 465   match ok right leftr with
 466   | Some _ as res -> res
 467   | None ->
 468       let rightr =
 469         match right with
 470           | Cic.Meta _ when not use_unification -> []
 471           | _ ->
 472               let rightc = get_candidates predicate table right in
 473                 find_all_matches ~unif_fun
 474                   metasenv context ugraph 0 right ty rightc
 475       in
 476 (*        print_res rightr;*)
 477         ok left rightr
 478 (*     (if r then  *)
 479 (*        debug_print  *)
 480 (*          (lazy *)
 481 (*             (Printf.sprintf "SUBSUMPTION! %s\n%s\n" *)
 482 (*                (Inference.string_of_equality target) (Utils.print_subst s)))); *)
 483 ;;
 484
 485 let subsumption = subsumption_aux false;;
 486 let unification = subsumption_aux true;;
 487
 488 let rec demodulation_aux ?from ?(typecheck=false)
 489   metasenv context ugraph table lift_amount term =
 490 (*  Printf.eprintf "term = %s\n" (CicPp.ppterm term);*)
 491   let module C = Cic in
 492   let module S = CicSubstitution in
 493   let module M = CicMetaSubst in
 494   let module HL = HelmLibraryObjects in
 495   let candidates =
 496     get_candidates
 497       ~env:(metasenv,context,ugraph) (* Unification *) Matching table term
 498   in
 499   let res =
 500     match term with
 501       | C.Meta _ -> None
 502       | term ->
 503           let termty, ugraph =
 504             if typecheck then
 505               CicTypeChecker.type_of_aux' metasenv context term ugraph
 506             else
 507               C.Implicit None, ugraph
 508           in
 509           let res =
 510             find_matches metasenv context ugraph lift_amount term termty candidates
 511           in
 512           if Utils.debug_res then ignore(check_res res "demod1");
 513             if res <> None then
 514               res
 515             else
 516               match term with
 517                 | C.Appl l ->
 518                     let res, ll =
 519                       List.fold_left
 520                         (fun (res, tl) t ->
 521                            if res <> None then
 522                              (res, tl @ [S.lift 1 t])
 523                            else
 524                              let r =
 525                                demodulation_aux ~from:"1" metasenv context ugraph table
 526                                  lift_amount t
 527                              in
 528                                match r with
 529                                  | None -> (None, tl @ [S.lift 1 t])
 530                                  | Some (rel, _, _, _, _) -> (r, tl @ [rel]))
 531                         (None, []) l
 532                     in (
 533                         match res with
 534                           | None -> None
 535                           | Some (_, subst, menv, ug, eq_found) ->
 536                               Some (C.Appl ll, subst, menv, ug, eq_found)
 537                       )
 538                 | C.Prod (nn, s, t) ->
 539                     let r1 =
 540                       demodulation_aux ~from:"2"
 541                         metasenv context ugraph table lift_amount s in (
 542                         match r1 with
 543                           | None ->
 544                               let r2 =
 545                                 demodulation_aux metasenv
 546                                   ((Some (nn, C.Decl s))::context) ugraph
 547                                   table (lift_amount+1) t
 548                               in (
 549                                   match r2 with
 550                                     | None -> None
 551                                     | Some (t', subst, menv, ug, eq_found) ->
 552                                         Some (C.Prod (nn, (S.lift 1 s), t'),
 553                                               subst, menv, ug, eq_found)
 554                                 )
 555                           | Some (s', subst, menv, ug, eq_found) ->
 556                               Some (C.Prod (nn, s', (S.lift 1 t)),
 557                                     subst, menv, ug, eq_found)
 558                       )
 559                 | C.Lambda (nn, s, t) ->
 560                     let r1 =
 561                       demodulation_aux
 562                         metasenv context ugraph table lift_amount s in (
 563                         match r1 with
 564                           | None ->
 565                               let r2 =
 566                                 demodulation_aux metasenv
 567                                   ((Some (nn, C.Decl s))::context) ugraph
 568                                   table (lift_amount+1) t
 569                               in (
 570                                   match r2 with
 571                                     | None -> None
 572                                     | Some (t', subst, menv, ug, eq_found) ->
 573                                         Some (C.Lambda (nn, (S.lift 1 s), t'),
 574                                               subst, menv, ug, eq_found)
 575                                 )
 576                           | Some (s', subst, menv, ug, eq_found) ->
 577                               Some (C.Lambda (nn, s', (S.lift 1 t)),
 578                                     subst, menv, ug, eq_found)
 579                       )
 580                 | t ->
 581                     None
 582   in
 583   if Utils.debug_res then ignore(check_res res "demod_aux output");
 584   res
 585 ;;
 586
 587
 588 let build_newtarget_time = ref 0.;;
 589
 590
 591 let demod_counter = ref 1;;
 592
 593 exception Foo
 594
 595 let profiler = HExtlib.profile "P/Indexing.demod_eq[build_new_target]"
 596
 597 (** demodulation, when target is an equality *)
 598 let rec demodulation_equality ?from newmeta env table sign target =
 599   let module C = Cic in
 600   let module S = CicSubstitution in
 601   let module M = CicMetaSubst in
 602   let module HL = HelmLibraryObjects in
 603   let module U = Utils in
 604   let metasenv, context, ugraph = env in
 605   let w, proof, (eq_ty, left, right, order), metas, id =
 606     Equality.open_equality target
 607   in
 608   (* first, we simplify *)
 609 (*   let right = U.guarded_simpl context right in *)
 610 (*   let left = U.guarded_simpl context left in *)
 611 (*   let order = !Utils.compare_terms left right in *)
 612 (*   let stat = (eq_ty, left, right, order) in  *)
 613 (*  let w = Utils.compute_equality_weight stat in*)
 614   (* let target = Equality.mk_equality (w, proof, stat, metas) in *)
 615   if Utils.debug_metas then
 616     ignore(check_target context target "demod equalities input");
 617   let metasenv' = (* metasenv @ *) metas in
 618   let maxmeta = ref newmeta in
 619
 620   let build_newtarget is_left (t, subst, menv, ug, (eq_found, eq_URI)) =
 621     let time1 = Unix.gettimeofday () in
 622
 623     if Utils.debug_metas then
 624       begin
 625         ignore(check_for_duplicates menv "input1");
 626         ignore(check_disjoint_invariant subst menv "input2");
 627         let substs = Subst.ppsubst subst in
 628         ignore(check_target context (snd eq_found) ("input3" ^ substs))
 629       end;
 630     let pos, equality = eq_found in
 631     let (_, proof',
 632         (ty, what, other, _), menv',id') = Equality.open_equality equality in
 633     let ty =
 634       try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
 635       with CicUtil.Meta_not_found _ -> ty
 636     in
 637     let what, other = if pos = Utils.Left then what, other else other, what in
 638     let newterm, newproof =
 639       let bo =
 640         Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
 641 (*      let name = C.Name ("x_Demod" ^ (string_of_int !demod_counter)) in*)
 642       let name = C.Name "x" in
 643       incr demod_counter;
 644       let bo' =
 645         let l, r = if is_left then t, S.lift 1 right else S.lift 1 left, t in
 646           C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
 647                   S.lift 1 eq_ty; l; r]
 648       in
 649       if sign = Utils.Positive then
 650           (bo, (Equality.Step (subst,(Equality.Demodulation, id,(pos,id'),
 651           (Cic.Lambda (name, ty, bo'))))))
 652       else
 653         assert false
 654 (*
 655         begin
 656         prerr_endline "***************************************negative";
 657         let metaproof =
 658           incr maxmeta;
 659           let irl =
 660             CicMkImplicit.identity_relocation_list_for_metavariable context in
 661 (*        debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta)); *)
 662 (*        print_newline (); *)
 663           C.Meta (!maxmeta, irl)
 664         in
 665           let eq_found =
 666             let proof'_old' =
 667               let termlist =
 668                 if pos = Utils.Left then [ty; what; other]
 669                 else [ty; other; what]
 670               in
 671               Equality.ProofSymBlock (termlist, proof'_old)
 672             in
 673             let proof'_new' = assert false (* not implemented *) in
 674             let what, other =
 675               if pos = Utils.Left then what, other else other, what
 676             in
 677             pos,
 678               Equality.mk_equality
 679                 (0, (proof'_new',proof'_old'),
 680                 (ty, other, what, Utils.Incomparable),menv')
 681           in
 682           let target_proof =
 683             let pb =
 684               Equality.ProofBlock
 685                 (subst, eq_URI, (name, ty), bo',
 686                  eq_found, Equality.BasicProof (Equality.empty_subst,metaproof))
 687             in
 688             assert false, (* not implemented *)
 689             (match snd proof with
 690             | Equality.BasicProof _ ->
 691                 (* print_endline "replacing a BasicProof"; *)
 692                 pb
 693             | Equality.ProofGoalBlock (_, parent_proof) ->
 694   (* print_endline "replacing another ProofGoalBlock"; *)
 695                 Equality.ProofGoalBlock (pb, parent_proof)
 696             | _ -> assert false)
 697           in
 698         let refl =
 699           C.Appl [C.MutConstruct (* reflexivity *)
 700                     (LibraryObjects.eq_URI (), 0, 1, []);
 701                   eq_ty; if is_left then right else left]
 702         in
 703         (bo,
 704          (assert false, (* not implemented *)
 705          Equality.ProofGoalBlock
 706            (Equality.BasicProof (Equality.empty_subst,refl), snd target_proof)))
 707       end
 708 *)
 709     in
 710     let newmenv = (* Inference.filter subst *) menv in
 711     let _ =
 712       if Utils.debug_metas then
 713         try ignore(CicTypeChecker.type_of_aux'
 714           newmenv context
 715             (Equality.build_proof_term newproof) ugraph);
 716           ()
 717         with exc ->
 718           prerr_endline "sempre lui";
 719           prerr_endline (Subst.ppsubst subst);
 720           prerr_endline (CicPp.ppterm
 721             (Equality.build_proof_term newproof));
 722           prerr_endline ("+++++++++++++termine: " ^ (CicPp.ppterm t));
 723           prerr_endline ("+++++++++++++what: " ^ (CicPp.ppterm what));
 724           prerr_endline ("+++++++++++++other: " ^ (CicPp.ppterm other));
 725           prerr_endline ("+++++++++++++subst: " ^ (Subst.ppsubst subst));
 726           prerr_endline ("+++++++++++++newmenv: " ^ (CicMetaSubst.ppmetasenv []
 727             newmenv));
 728           raise exc;
 729       else ()
 730     in
 731     let left, right = if is_left then newterm, right else left, newterm in
 732     let ordering = !Utils.compare_terms left right in
 733     let stat = (eq_ty, left, right, ordering) in
 734     let time2 = Unix.gettimeofday () in
 735     build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
 736     let res =
 737       let w = Utils.compute_equality_weight stat in
 738       Equality.mk_equality (w, newproof, stat,newmenv)
 739     in
 740     if Utils.debug_metas then
 741       ignore(check_target context res "buildnew_target output");
 742     !maxmeta, res
 743   in
 744   let build_newtarget is_left x =
 745     profiler.HExtlib.profile (build_newtarget is_left) x
 746   in
 747
 748   let res = demodulation_aux ~from:"3" metasenv' context ugraph table 0 left in
 749   if Utils.debug_res then check_res res "demod result";
 750   let newmeta, newtarget =
 751     match res with
 752     | Some t ->
 753         let newmeta, newtarget = build_newtarget true t in
 754           assert (not (Equality.meta_convertibility_eq target newtarget));
 755           if (Equality.is_weak_identity newtarget) ||
 756             (Equality.meta_convertibility_eq target newtarget) then
 757               newmeta, newtarget
 758           else
 759             demodulation_equality ?from newmeta env table sign newtarget
 760     | None ->
 761         let res = demodulation_aux metasenv' context ugraph table 0 right in
 762         if Utils.debug_res then check_res res "demod result 1";
 763           match res with
 764           | Some t ->
 765               let newmeta, newtarget = build_newtarget false t in
 766                 if (Equality.is_weak_identity newtarget) ||
 767                   (Equality.meta_convertibility_eq target newtarget) then
 768                     newmeta, newtarget
 769                 else
 770                    demodulation_equality ?from newmeta env table sign newtarget
 771           | None ->
 772               newmeta, target
 773   in
 774   (* newmeta, newtarget *)
 775   newmeta,newtarget
 776 ;;
 777
 778 (**
 779    Performs the beta expansion of the term "term" w.r.t. "table",
 780    i.e. returns the list of all the terms t s.t. "(t term) = t2", for some t2
 781    in table.
 782 *)
 783 let rec betaexpand_term metasenv context ugraph table lift_amount term =
 784   let module C = Cic in
 785   let module S = CicSubstitution in
 786   let module M = CicMetaSubst in
 787   let module HL = HelmLibraryObjects in
 788   let candidates = get_candidates Unification table term in
 789
 790   let res, lifted_term =
 791     match term with
 792     | C.Meta (i, l) ->
 793         let l', lifted_l =
 794           List.fold_right
 795             (fun arg (res, lifted_tl) ->
 796                match arg with
 797                | Some arg ->
 798                    let arg_res, lifted_arg =
 799                      betaexpand_term metasenv context ugraph table
 800                        lift_amount arg in
 801                    let l1 =
 802                      List.map
 803                        (fun (t, s, m, ug, eq_found) ->
 804                           (Some t)::lifted_tl, s, m, ug, eq_found)
 805                        arg_res
 806                    in
 807                    (l1 @
 808                       (List.map
 809                          (fun (l, s, m, ug, eq_found) ->
 810                             (Some lifted_arg)::l, s, m, ug, eq_found)
 811                          res),
 812                     (Some lifted_arg)::lifted_tl)
 813                | None ->
 814                    (List.map
 815                       (fun (r, s, m, ug, eq_found) ->
 816                          None::r, s, m, ug, eq_found) res,
 817                     None::lifted_tl)
 818             ) l ([], [])
 819         in
 820         let e =
 821           List.map
 822             (fun (l, s, m, ug, eq_found) ->
 823                (C.Meta (i, l), s, m, ug, eq_found)) l'
 824         in
 825         e, C.Meta (i, lifted_l)
 826
 827     | C.Rel m ->
 828         [], if m <= lift_amount then C.Rel m else C.Rel (m+1)
 829
 830     | C.Prod (nn, s, t) ->
 831         let l1, lifted_s =
 832           betaexpand_term metasenv context ugraph table lift_amount s in
 833         let l2, lifted_t =
 834           betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
 835             table (lift_amount+1) t in
 836         let l1' =
 837           List.map
 838             (fun (t, s, m, ug, eq_found) ->
 839                C.Prod (nn, t, lifted_t), s, m, ug, eq_found) l1
 840         and l2' =
 841           List.map
 842             (fun (t, s, m, ug, eq_found) ->
 843                C.Prod (nn, lifted_s, t), s, m, ug, eq_found) l2 in
 844         l1' @ l2', C.Prod (nn, lifted_s, lifted_t)
 845
 846     | C.Lambda (nn, s, t) ->
 847         let l1, lifted_s =
 848           betaexpand_term metasenv context ugraph table lift_amount s in
 849         let l2, lifted_t =
 850           betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
 851             table (lift_amount+1) t in
 852         let l1' =
 853           List.map
 854             (fun (t, s, m, ug, eq_found) ->
 855                C.Lambda (nn, t, lifted_t), s, m, ug, eq_found) l1
 856         and l2' =
 857           List.map
 858             (fun (t, s, m, ug, eq_found) ->
 859                C.Lambda (nn, lifted_s, t), s, m, ug, eq_found) l2 in
 860         l1' @ l2', C.Lambda (nn, lifted_s, lifted_t)
 861
 862     | C.Appl l ->
 863         let l', lifted_l =
 864           List.fold_right
 865             (fun arg (res, lifted_tl) ->
 866                let arg_res, lifted_arg =
 867                  betaexpand_term metasenv context ugraph table lift_amount arg
 868                in
 869                let l1 =
 870                  List.map
 871                    (fun (a, s, m, ug, eq_found) ->
 872                       a::lifted_tl, s, m, ug, eq_found)
 873                    arg_res
 874                in
 875                (l1 @
 876                   (List.map
 877                      (fun (r, s, m, ug, eq_found) ->
 878                         lifted_arg::r, s, m, ug, eq_found)
 879                      res),
 880                 lifted_arg::lifted_tl)
 881             ) l ([], [])
 882         in
 883         (List.map
 884            (fun (l, s, m, ug, eq_found) -> (C.Appl l, s, m, ug, eq_found)) l',
 885          C.Appl lifted_l)
 886
 887     | t -> [], (S.lift lift_amount t)
 888   in
 889   match term with
 890   | C.Meta (i, l) -> res, lifted_term
 891   | term ->
 892       let termty, ugraph =
 893         C.Implicit None, ugraph
 894 (*         CicTypeChecker.type_of_aux' metasenv context term ugraph *)
 895       in
 896       let r =
 897         find_all_matches
 898           metasenv context ugraph lift_amount term termty candidates
 899       in
 900       r @ res, lifted_term
 901 ;;
 902
 903 let profiler = HExtlib.profile "P/Indexing.betaexpand_term"
 904
 905 let betaexpand_term metasenv context ugraph table lift_amount term =
 906   profiler.HExtlib.profile
 907     (betaexpand_term metasenv context ugraph table lift_amount) term
 908
 909
 910 let sup_l_counter = ref 1;;
 911
 912 (**
 913    superposition_left
 914    returns a list of new clauses inferred with a left superposition step
 915    the negative equation "target" and one of the positive equations in "table"
 916 *)
 917 let fix_expansion (eq,ty,unchanged,posu) (t, subst, menv, ug, eq_f) =
 918   let unchanged = CicSubstitution.lift 1 unchanged in
 919   let ty = CicSubstitution.lift 1 ty in
 920   let pred =
 921     match posu with
 922     | Utils.Left -> Cic.Appl [eq;ty;unchanged;t]
 923     | Utils.Right -> Cic.Appl [eq;ty;t;unchanged]
 924   in
 925   (pred, subst, menv, ug, eq_f)
 926 ;;
 927
 928 let build_newgoal context goalproof goal_info expansion =
 929   let (t,subst,menv,ug,(eq_found,eq_URI)) = fix_expansion goal_info expansion in
 930   let pos, equality = eq_found in
 931   let (_, proof', (ty, what, other, _), menv',id) =
 932     Equality.open_equality equality in
 933   let what, other = if pos = Utils.Left then what, other else other, what in
 934   let newterm, newgoalproof =
 935     let bo =
 936       Utils.guarded_simpl context
 937         (apply_subst subst (CicSubstitution.subst other t))
 938     in
 939     let bo' = (*apply_subst subst*) t in
 940     let name = Cic.Name "x" in
 941     let newgoalproofstep = (pos,id,subst,Cic.Lambda (name,ty,bo')) in
 942     bo, (newgoalproofstep::goalproof)
 943   in
 944   let newmetasenv = (* Inference.filter subst *) menv in
 945   (newgoalproof, newmetasenv, newterm)
 946 ;;
 947
 948 let superposition_left
 949   (metasenv, context, ugraph) table (proof,menv,ty)
 950 =
 951   let module C = Cic in
 952   let module S = CicSubstitution in
 953   let module M = CicMetaSubst in
 954   let module HL = HelmLibraryObjects in
 955   let module CR = CicReduction in
 956   let module U = Utils in
 957   let big,small,pos,eq,ty =
 958     match ty with
 959     | Cic.Appl [eq;ty;l;r] ->
 960        let c =
 961          Utils.compare_weights ~normalize:true
 962            (Utils.weight_of_term l) (Utils.weight_of_term r)
 963        in
 964        (match c with
 965        | Utils.Gt -> l,r,Utils.Right,eq,ty
 966        | _ -> r,l,Utils.Left,eq,ty)
 967     | _ ->
 968         let names = Utils.names_of_context context in
 969         prerr_endline ("NON TROVO UN EQ: " ^ CicPp.pp ty names);
 970         assert false
 971   in
 972   let expansions, _ = betaexpand_term menv context ugraph table 0 big in
 973   List.map (build_newgoal context proof (eq,ty,small,pos)) expansions
 974 ;;
 975
 976 let sup_r_counter = ref 1;;
 977
 978 (**
 979    superposition_right
 980    returns a list of new clauses inferred with a right superposition step
 981    between the positive equation "target" and one in the "table" "newmeta" is
 982    the first free meta index, i.e. the first number above the highest meta
 983    index: its updated value is also returned
 984 *)
 985 let superposition_right newmeta (metasenv, context, ugraph) table target =
 986   let module C = Cic in
 987   let module S = CicSubstitution in
 988   let module M = CicMetaSubst in
 989   let module HL = HelmLibraryObjects in
 990   let module CR = CicReduction in
 991   let module U = Utils in
 992   let w, eqproof, (eq_ty, left, right, ordering), newmetas,id =
 993     Equality.open_equality target
 994   in
 995   if Utils.debug_metas then
 996     ignore (check_target context target "superpositionright");
 997   let metasenv' = newmetas in
 998   let maxmeta = ref newmeta in
 999   let res1, res2 =
1000     let betaexpand_term metasenv context ugraph table d term =
1001       let t1 = Unix.gettimeofday () in
1002       let res = betaexpand_term metasenv context ugraph table d term in
1003       let t2 = Unix.gettimeofday () in
1004         beta_expand_time := !beta_expand_time  +. (t2 -. t1);
1005         res
1006     in
1007     match ordering with
1008     | U.Gt ->
1009         fst (betaexpand_term metasenv' context ugraph table 0 left), []
1010     | U.Lt ->
1011         [], fst (betaexpand_term metasenv' context ugraph table 0 right)
1012     | _ ->
1013         let res l r =
1014           List.filter
1015             (fun (_, subst, _, _, _) ->
1016                let subst = apply_subst subst in
1017                let o = !Utils.compare_terms (subst l) (subst r) in
1018                o <> U.Lt && o <> U.Le)
1019             (fst (betaexpand_term metasenv' context ugraph table 0 l))
1020         in
1021         (res left right), (res right left)
1022   in
1023   let build_new ordering (bo, s, m, ug, (eq_found, eq_URI)) =
1024     if Utils.debug_metas then
1025       ignore (check_target context (snd eq_found) "buildnew1" );
1026     let time1 = Unix.gettimeofday () in
1027
1028     let pos, equality =  eq_found in
1029     let (_, proof', (ty, what, other, _), menv',id') =
1030       Equality.open_equality  equality in
1031     let what, other = if pos = Utils.Left then what, other else other, what in
1032
1033     let newgoal, newproof =
1034       (* qua *)
1035       let bo' =
1036         Utils.guarded_simpl context (apply_subst s (S.subst other bo))
1037       in
1038       let name = C.Name "x" in
1039       incr sup_r_counter;
1040       let bo'' =
1041         let l, r =
1042           if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
1043         C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
1044                 S.lift 1 eq_ty; l; r]
1045       in
1046       bo',
1047         Equality.Step
1048           (s,(Equality.SuperpositionRight,
1049                id,(pos,id'),(Cic.Lambda(name,ty,bo''))))
1050     in
1051     let newmeta, newequality =
1052       let left, right =
1053         if ordering = U.Gt then newgoal, apply_subst s right
1054         else apply_subst s left, newgoal in
1055       let neworder = !Utils.compare_terms left right in
1056       let newmenv = (* Inference.filter s *) m in
1057       let stat = (eq_ty, left, right, neworder) in
1058       let eq' =
1059         let w = Utils.compute_equality_weight stat in
1060         Equality.mk_equality (w, newproof, stat, newmenv) in
1061       if Utils.debug_metas then
1062         ignore (check_target context eq' "buildnew3");
1063       let newm, eq' = Equality.fix_metas !maxmeta eq' in
1064       if Utils.debug_metas then
1065         ignore (check_target context eq' "buildnew4");
1066       newm, eq'
1067     in
1068     maxmeta := newmeta;
1069     let time2 = Unix.gettimeofday () in
1070     build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
1071     if Utils.debug_metas then
1072       ignore(check_target context newequality "buildnew2");
1073     newequality
1074   in
1075   let new1 = List.map (build_new U.Gt) res1
1076   and new2 = List.map (build_new U.Lt) res2 in
1077   let ok e = not (Equality.is_identity (metasenv', context, ugraph) e) in
1078   (!maxmeta,
1079    (List.filter ok (new1 @ new2)))
1080 ;;
1081
1082 (** demodulation, when the target is a goal *)
1083 let goal_metaconvertibility_eq (_,_,g1) (_,_,g2) =
1084   Equality.meta_convertibility g1 g2
1085 ;;
1086
1087 let rec demodulation_goal env table goal =
1088   let metasenv, context, ugraph = env 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 left,right,eq,ty =
1095     match term with
1096     | Cic.Appl [eq;ty;l;r] -> l,r,eq,ty
1097     | _ -> assert false
1098   in
1099   let do_right () =
1100       let resright = demodulation_aux metasenv' context ugraph table 0 right in
1101       match resright with
1102       | Some t ->
1103           let newg=build_newgoal context goalproof (eq,ty,left,Utils.Left) t in
1104           if goal_metaconvertibility_eq goal newg then
1105             false, goal
1106           else
1107             true, snd (demodulation_goal env table newg)
1108       | None -> false, goal
1109   in
1110   let resleft =
1111     demodulation_aux (*~typecheck:true*) metasenv' context ugraph table 0 left
1112   in
1113   match resleft with
1114   | Some t ->
1115       let newg = build_newgoal context goalproof (eq,ty,right,Utils.Right) t in
1116       if goal_metaconvertibility_eq goal newg then
1117         do_right ()
1118       else
1119         true, snd (demodulation_goal env table newg)
1120   | None -> do_right ()
1121 ;;
1122
1123 (** demodulation, when the target is a theorem *)
1124 let rec demodulation_theorem newmeta env table theorem =
1125   let module C = Cic in
1126   let module S = CicSubstitution in
1127   let module M = CicMetaSubst in
1128   let module HL = HelmLibraryObjects in
1129   let metasenv, context, ugraph = env in
1130   let maxmeta = ref newmeta in
1131   let term, termty, metas = theorem in
1132   let metasenv' = metas in
1133
1134   let build_newtheorem (t, subst, menv, ug, (eq_found, eq_URI)) =
1135     let pos, equality = eq_found in
1136     let (_, proof', (ty, what, other, _), menv',id) =
1137       Equality.open_equality equality in
1138     let what, other = if pos = Utils.Left then what, other else other, what in
1139     let newterm, newty =
1140       let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
1141 (*      let bo' = apply_subst subst t in *)
1142 (*      let name = C.Name ("x_DemodThm_" ^ (string_of_int !demod_counter)) in*)
1143       incr demod_counter;
1144 (*
1145       let newproofold =
1146         Equality.ProofBlock (subst, eq_URI, (name, ty), bo', eq_found,
1147                               Equality.BasicProof (Equality.empty_subst,term))
1148       in
1149       (Equality.build_proof_term_old newproofold, bo)
1150 *)
1151       (* TODO, not ported to the new proofs *)
1152       if true then assert false; term, bo
1153     in
1154     !maxmeta, (newterm, newty, menv)
1155   in
1156   let res =
1157     demodulation_aux (* ~typecheck:true *) metasenv' context ugraph table 0 termty
1158   in
1159   match res with
1160   | Some t ->
1161       let newmeta, newthm = build_newtheorem t in
1162       let newt, newty, _ = newthm in
1163       if Equality.meta_convertibility termty newty then
1164         newmeta, newthm
1165       else
1166         demodulation_theorem newmeta env table newthm
1167   | None ->
1168       newmeta, theorem
1169 ;;
1170