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