helm/software/components/tactics/paramodulation/indexing.ml

   1 (* Copyright (C) 2005, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://cs.unibo.it/helm/.
  24  *)
  25
  26 (* $Id$ *)
  27
  28 type goal = Equality.goal_proof * Cic.metasenv * Cic.term
  29
  30 module Index = Equality_indexing.DT (* discrimination tree based indexing *)
  31 (*
  32 module Index = Equality_indexing.DT (* path tree based indexing *)
  33 *)
  34
  35 let beta_expand_time = ref 0.;;
  36
  37 let debug_print = Utils.debug_print;;
  38
  39 (*
  40 for debugging
  41 let check_equation env equation msg =
  42   let w, proof, (eq_ty, left, right, order), metas, args = equation in
  43   let metasenv, context, ugraph = env
  44   let metasenv' = metasenv @ metas in
  45     try
  46       CicTypeChecker.type_of_aux' metasenv' context left ugraph;
  47       CicTypeChecker.type_of_aux' metasenv' context right ugraph;
  48       ()
  49     with
  50         CicUtil.Meta_not_found _ as exn ->
  51           begin
  52             prerr_endline msg;
  53             prerr_endline (CicPp.ppterm left);
  54             prerr_endline (CicPp.ppterm right);
  55             raise exn
  56           end
  57 *)
  58
  59 type retrieval_mode = Matching | Unification;;
  60
  61 let string_of_res ?env =
  62   function
  63       None -> "None"
  64     | Some (t, s, m, u, ((p,e), eq_URI)) ->
  65         Printf.sprintf "Some: (%s, %s, %s)"
  66           (Utils.string_of_pos p)
  67           (Equality.string_of_equality ?env e)
  68           (CicPp.ppterm t)
  69 ;;
  70
  71 let print_res ?env res =
  72   prerr_endline
  73     (String.concat "\n"
  74        (List.map (string_of_res ?env) res))
  75 ;;
  76
  77 let print_candidates ?env mode term res =
  78   let _ =
  79     match mode with
  80     | Matching ->
  81         prerr_endline ("| candidates Matching " ^ (CicPp.ppterm term))
  82     | Unification ->
  83         prerr_endline ("| candidates Unification " ^ (CicPp.ppterm term))
  84   in
  85   prerr_endline
  86     (String.concat "\n"
  87        (List.map
  88           (fun (p, e) ->
  89              Printf.sprintf "| (%s, %s)" (Utils.string_of_pos p)
  90                (Equality.string_of_equality ?env e))
  91           res));
  92 ;;
  93
  94
  95 let indexing_retrieval_time = ref 0.;;
  96
  97
  98 let apply_subst = Subst.apply_subst
  99
 100 let index = Index.index
 101 let remove_index = Index.remove_index
 102 let in_index = Index.in_index
 103 let empty = Index.empty
 104 let init_index = Index.init_index
 105
 106 let check_disjoint_invariant subst metasenv msg =
 107   if (List.exists
 108         (fun (i,_,_) -> (Subst.is_in_subst i subst)) metasenv)
 109   then
 110     begin
 111       prerr_endline ("not disjoint: " ^ msg);
 112       assert false
 113     end
 114 ;;
 115
 116 let check_for_duplicates metas msg =
 117   if List.length metas <>
 118   List.length (HExtlib.list_uniq (List.sort Pervasives.compare metas)) then
 119     begin
 120       prerr_endline ("DUPLICATI " ^ msg);
 121       prerr_endline (CicMetaSubst.ppmetasenv [] metas);
 122       assert false
 123     end
 124 ;;
 125
 126 let check_res res msg =
 127   match res with
 128       Some (t, subst, menv, ug, (eq_found, eq_URI)) ->
 129         let eqs = Equality.string_of_equality (snd eq_found) in
 130         check_disjoint_invariant subst menv msg;
 131         check_for_duplicates menv (msg ^ "\nchecking " ^ eqs);
 132     | None -> ()
 133 ;;
 134
 135 let check_target context target msg =
 136   let w, proof, (eq_ty, left, right, order), metas,_ =
 137     Equality.open_equality target in
 138   (* check that metas does not contains duplicates *)
 139   let eqs = Equality.string_of_equality target in
 140   let _ = check_for_duplicates metas (msg ^ "\nchecking " ^ eqs) in
 141   let actual = (Utils.metas_of_term left)@(Utils.metas_of_term right)
 142     @(Utils.metas_of_term eq_ty)@(Equality.metas_of_proof proof)  in
 143   let menv = List.filter (fun (i, _, _) -> List.mem i actual) metas in
 144   let _ = if menv <> metas then
 145     begin
 146       prerr_endline ("extra metas " ^ msg);
 147       prerr_endline (CicMetaSubst.ppmetasenv [] metas);
 148       prerr_endline "**********************";
 149       prerr_endline (CicMetaSubst.ppmetasenv [] menv);
 150       prerr_endline ("left: " ^ (CicPp.ppterm left));
 151       prerr_endline ("right: " ^ (CicPp.ppterm right));
 152       prerr_endline ("ty: " ^ (CicPp.ppterm eq_ty));
 153       assert false
 154     end
 155   else () in ()
 156 (*
 157   try
 158       ignore(CicTypeChecker.type_of_aux'
 159         metas context (Inference.build_proof_term proof) CicUniv.empty_ugraph)
 160   with e ->
 161       prerr_endline msg;
 162       prerr_endline (Inference.string_of_proof proof);
 163       prerr_endline (CicPp.ppterm (Inference.build_proof_term proof));
 164       prerr_endline ("+++++++++++++left: " ^ (CicPp.ppterm left));
 165       prerr_endline ("+++++++++++++right: " ^ (CicPp.ppterm right));
 166       raise e
 167 *)
 168
 169
 170 (* returns a list of all the equalities in the tree that are in relation
 171    "mode" with the given term, where mode can be either Matching or
 172    Unification.
 173
 174    Format of the return value: list of tuples in the form:
 175    (position - Left or Right - of the term that matched the given one in this
 176      equality,
 177     equality found)
 178
 179    Note that if equality is "left = right", if the ordering is left > right,
 180    the position will always be Left, and if the ordering is left < right,
 181    position will be Right.
 182 *)
 183
 184 let get_candidates ?env mode tree term =
 185   let t1 = Unix.gettimeofday () in
 186   let res =
 187     let s =
 188       match mode with
 189       | Matching -> Index.retrieve_generalizations tree term
 190       | Unification -> Index.retrieve_unifiables tree term
 191     in
 192     Index.PosEqSet.elements s
 193   in
 194 (*   print_endline (Discrimination_tree.string_of_discrimination_tree tree); *)
 195 (*   print_newline (); *)
 196   let t2 = Unix.gettimeofday () in
 197   indexing_retrieval_time := !indexing_retrieval_time +. (t2 -. t1);
 198  (* make fresh instances *)
 199   res
 200 ;;
 201
 202 let profiler = HExtlib.profile "P/Indexing.get_candidates"
 203
 204 let get_candidates ?env mode tree term =
 205   profiler.HExtlib.profile (get_candidates ?env mode tree) term
 206
 207 let match_unif_time_ok = ref 0.;;
 208 let match_unif_time_no = ref 0.;;
 209
 210
 211 (*
 212   finds the first equality in the index that matches "term", of type "termty"
 213   termty can be Implicit if it is not needed. The result (one of the sides of
 214   the equality, actually) should be not greater (wrt the term ordering) than
 215   term
 216
 217   Format of the return value:
 218
 219   (term to substitute, [Cic.Rel 1 properly lifted - see the various
 220                         build_newtarget functions inside the various
 221                         demodulation_* functions]
 222    substitution used for the matching,
 223    metasenv,
 224    ugraph, [substitution, metasenv and ugraph have the same meaning as those
 225    returned by CicUnification.fo_unif]
 226    (equality where the matching term was found, [i.e. the equality to use as
 227                                                 rewrite rule]
 228     uri [either eq_ind_URI or eq_ind_r_URI, depending on the direction of
 229          the equality: this is used to build the proof term, again see one of
 230          the build_newtarget functions]
 231    ))
 232 *)
 233 let rec find_matches metasenv context ugraph lift_amount term termty =
 234   let module C = Cic in
 235   let module U = Utils in
 236   let module S = CicSubstitution in
 237   let module M = CicMetaSubst in
 238   let module HL = HelmLibraryObjects in
 239   let cmp = !Utils.compare_terms in
 240   let check = match termty with C.Implicit None -> false | _ -> true in
 241   function
 242     | [] -> None
 243     | candidate::tl ->
 244         let pos, equality = candidate in
 245         let (_, proof, (ty, left, right, o), metas,_) =
 246           Equality.open_equality equality in
 247         if Utils.debug_metas then
 248           ignore(check_target context (snd candidate) "find_matches");
 249         if Utils.debug_res then
 250           begin
 251             let c="eq = "^(Equality.string_of_equality (snd candidate)) ^ "\n"in
 252             let t="t = " ^ (CicPp.ppterm term) ^ "\n" in
 253             let m="metas = " ^ (CicMetaSubst.ppmetasenv [] metas) ^ "\n" in
 254             let p="proof = "^
 255               (CicPp.ppterm(Equality.build_proof_term proof))^"\n"
 256             in
 257               check_for_duplicates metas "gia nella metas";
 258               check_for_duplicates (metasenv@metas) ("not disjoint"^c^t^m^p)
 259           end;
 260         if check && not (fst (CicReduction.are_convertible
 261                                 ~metasenv context termty ty ugraph)) then (
 262           find_matches metasenv context ugraph lift_amount term termty tl
 263         ) else
 264           let do_match c eq_URI =
 265             let subst', metasenv', ugraph' =
 266               let t1 = Unix.gettimeofday () in
 267               try
 268                 let r =
 269                   ( Inference.matching metasenv metas context
 270                     term (S.lift lift_amount c)) ugraph
 271                 in
 272                 let t2 = Unix.gettimeofday () in
 273                 match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
 274                 r
 275               with
 276                 | Inference.MatchingFailure as e ->
 277                 let t2 = Unix.gettimeofday () in
 278                 match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
 279                   raise e
 280                 | CicUtil.Meta_not_found _ as exn -> raise exn
 281             in
 282             Some (C.Rel (1 + lift_amount), subst', metasenv', ugraph',
 283                   (candidate, eq_URI))
 284           in
 285           let c, other, eq_URI =
 286             if pos = Utils.Left then left, right, Utils.eq_ind_URI ()
 287             else right, left, Utils.eq_ind_r_URI ()
 288           in
 289           if o <> U.Incomparable then
 290             let res =
 291               try
 292                 do_match c eq_URI
 293               with Inference.MatchingFailure ->
 294                 find_matches metasenv context ugraph lift_amount term termty tl
 295             in
 296               if Utils.debug_res then ignore (check_res res "find1");
 297               res
 298           else
 299             let res =
 300               try do_match c eq_URI
 301               with Inference.MatchingFailure -> None
 302             in
 303             if Utils.debug_res then ignore (check_res res "find2");
 304             match res with
 305             | Some (_, s, _, _, _) ->
 306                 let c' = apply_subst s c in
 307                 (*
 308              let other' = U.guarded_simpl context (apply_subst s other) in *)
 309                 let other' = apply_subst s other in
 310                 let order = cmp c' other' in
 311                 if order = U.Gt then
 312                   res
 313                 else
 314                   find_matches
 315                     metasenv context ugraph lift_amount term termty tl
 316             | None ->
 317                 find_matches metasenv context ugraph lift_amount term termty tl
 318 ;;
 319
 320 (*
 321   as above, but finds all the matching equalities, and the matching condition
 322   can be either Inference.matching or Inference.unification
 323 *)
 324 let rec find_all_matches ?(unif_fun=Inference.unification)
 325     metasenv context ugraph lift_amount term termty =
 326   let module C = Cic in
 327   let module U = Utils in
 328   let module S = CicSubstitution in
 329   let module M = CicMetaSubst in
 330   let module HL = HelmLibraryObjects in
 331   let cmp = !Utils.compare_terms in
 332   function
 333     | [] -> []
 334     | candidate::tl ->
 335         let pos, equality = candidate in
 336         let (_,_,(ty,left,right,o),metas,_)=Equality.open_equality equality in
 337         let do_match c eq_URI =
 338           let subst', metasenv', ugraph' =
 339             let t1 = Unix.gettimeofday () in
 340             try
 341               let r =
 342                 unif_fun metasenv metas context
 343                   term (S.lift lift_amount c) ugraph in
 344               let t2 = Unix.gettimeofday () in
 345               match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
 346               r
 347             with
 348             | Inference.MatchingFailure
 349             | CicUnification.UnificationFailure _
 350             | CicUnification.Uncertain _ as e ->
 351                 let t2 = Unix.gettimeofday () in
 352                 match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
 353                 raise e
 354           in
 355           (C.Rel (1 + lift_amount), subst', metasenv', ugraph',
 356            (candidate, eq_URI))
 357         in
 358         let c, other, eq_URI =
 359           if pos = Utils.Left then left, right, Utils.eq_ind_URI ()
 360           else right, left, Utils.eq_ind_r_URI ()
 361         in
 362         if o <> U.Incomparable then
 363           try
 364             let res = do_match c eq_URI in
 365             res::(find_all_matches ~unif_fun metasenv context ugraph
 366                     lift_amount term termty tl)
 367           with
 368           | Inference.MatchingFailure
 369           | CicUnification.UnificationFailure _
 370           | CicUnification.Uncertain _ ->
 371               find_all_matches ~unif_fun metasenv context ugraph
 372                 lift_amount term termty tl
 373         else
 374           try
 375             let res = do_match c eq_URI in
 376             match res with
 377             | _, s, _, _, _ ->
 378                 let c' = apply_subst s c
 379                 and other' = apply_subst s other in
 380                 let order = cmp c' other' in
 381                 if order <> U.Lt && order <> U.Le then
 382                   res::(find_all_matches ~unif_fun metasenv context ugraph
 383                           lift_amount term termty tl)
 384                 else
 385                   find_all_matches ~unif_fun metasenv context ugraph
 386                     lift_amount term termty tl
 387           with
 388           | Inference.MatchingFailure
 389           | CicUnification.UnificationFailure _
 390           | CicUnification.Uncertain _ ->
 391               find_all_matches ~unif_fun metasenv context ugraph
 392                 lift_amount term termty tl
 393 ;;
 394
 395 let find_all_matches
 396   ?unif_fun metasenv context ugraph lift_amount term termty l
 397 =
 398   let rc =
 399     find_all_matches
 400       ?unif_fun metasenv context ugraph lift_amount term termty l
 401   in
 402   (*prerr_endline "CANDIDATES:";
 403   List.iter (fun (_,x)->prerr_endline (Inference.string_of_equality x)) l;
 404   prerr_endline ("MATCHING:" ^ CicPp.ppterm term ^ " are " ^ string_of_int
 405   (List.length rc));*)
 406   rc
 407
 408 (*
 409   returns true if target is subsumed by some equality in table
 410 *)
 411 let subsumption_aux use_unification env table target =
 412   (*
 413   let print_res l =
 414     prerr_endline (String.concat "\n" (List.map (fun (_, subst, menv, ug,
 415     ((pos,equation),_)) -> Inference.string_of_equality equation)l))
 416   in
 417   *)
 418   let _, _, (ty, left, right, _), tmetas, _ = Equality.open_equality target in
 419   let metasenv, context, ugraph = env in
 420   let metasenv = tmetas in
 421   let leftr =
 422     match left with
 423     | Cic.Meta _ -> []
 424     | _ ->
 425         let leftc = get_candidates Matching table left in
 426         find_all_matches ~unif_fun:Inference.matching
 427           metasenv context ugraph 0 left ty leftc
 428   in
 429 (*  print_res leftr;*)
 430   let rec ok what = function
 431     | [] -> None
 432     | (_, subst, menv, ug, ((pos,equation),_))::tl ->
 433         let _, _, (_, l, r, o), m,_ = Equality.open_equality equation in
 434         try
 435           let other = if pos = Utils.Left then r else l in
 436           let subst', menv', ug' =
 437             let t1 = Unix.gettimeofday () in
 438             try
 439               let r =
 440                 if use_unification then
 441                   Inference.unification metasenv m context what other ugraph
 442                 else
 443                   Inference.matching metasenv m context what other ugraph
 444               in
 445               let t2 = Unix.gettimeofday () in
 446               match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
 447               r
 448             with Inference.MatchingFailure as e ->
 449               let t2 = Unix.gettimeofday () in
 450               match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
 451               raise e
 452           in
 453           (match Subst.merge_subst_if_possible subst subst' with
 454           | None -> ok what tl
 455           | Some s -> Some (s, equation))
 456         with Inference.MatchingFailure ->
 457           ok what tl
 458   in
 459   match ok right leftr with
 460   | Some _ as res -> res
 461   | None ->
 462       let rightr =
 463         match right with
 464           | Cic.Meta _ -> []
 465           | _ ->
 466               let rightc = get_candidates Matching table right in
 467                 find_all_matches ~unif_fun:Inference.matching
 468                   metasenv context ugraph 0 right ty rightc
 469       in
 470 (*        print_res rightr;*)
 471         ok left rightr
 472 (*     (if r then  *)
 473 (*        debug_print  *)
 474 (*          (lazy *)
 475 (*             (Printf.sprintf "SUBSUMPTION! %s\n%s\n" *)
 476 (*                (Inference.string_of_equality target) (Utils.print_subst s)))); *)
 477 ;;
 478
 479 let subsumption = subsumption_aux false;;
 480 let unification = subsumption_aux true;;
 481
 482 let rec demodulation_aux ?from ?(typecheck=false)
 483   metasenv context ugraph table lift_amount term =
 484   (* Printf.eprintf "term = %s\n" (CicPp.ppterm term); *)
 485   let module C = Cic in
 486   let module S = CicSubstitution in
 487   let module M = CicMetaSubst in
 488   let module HL = HelmLibraryObjects in
 489   let candidates =
 490     get_candidates ~env:(metasenv,context,ugraph) (* Unification *) Matching table term in
 491   if List.exists (fun (i,_,_) -> i = 2840) metasenv
 492   then
 493     (prerr_endline ("term: " ^(CicPp.ppterm term));
 494      List.iter (fun (_,x) -> prerr_endline (Equality.string_of_equality  x))
 495        candidates;
 496      prerr_endline ("-------");
 497      prerr_endline ("+++++++"));
 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
 917 let build_newgoal context goalproof (t, subst, menv, ug, (eq_found, eq_URI)) =
 918   let pos, equality = eq_found in
 919   let (_, proof', (ty, what, other, _), menv',id) =
 920     Equality.open_equality equality in
 921   let what, other = if pos = Utils.Left then what, other else other, what in
 922   let newterm, newgoalproof =
 923     let bo =
 924       Utils.guarded_simpl context
 925         (apply_subst subst (CicSubstitution.subst other t))
 926     in
 927     let bo' = (*apply_subst subst*) t in
 928     let name = Cic.Name "x" in
 929     let newgoalproofstep = (pos,id,subst,Cic.Lambda (name,ty,bo')) in
 930     bo, (newgoalproofstep::goalproof)
 931   in
 932   let newmetasenv = (* Inference.filter subst *) menv in
 933   (newgoalproof, newmetasenv, newterm)
 934 ;;
 935
 936 let superposition_left
 937   (metasenv, context, ugraph) table (proof,menv,ty)
 938 =
 939   let module C = Cic in
 940   let module S = CicSubstitution in
 941   let module M = CicMetaSubst in
 942   let module HL = HelmLibraryObjects in
 943   let module CR = CicReduction in
 944   let module U = Utils in
 945   let big,small,pos,eq,ty =
 946     match ty with
 947     | Cic.Appl [eq;ty;l;r] ->
 948        let c =
 949          Utils.compare_weights ~normalize:true
 950            (Utils.weight_of_term l) (Utils.weight_of_term r)
 951        in
 952        (match c with
 953        | Utils.Gt -> l,r,Utils.Right,eq,ty
 954        | _ -> r,l,Utils.Left,eq,ty)
 955     | _ -> assert false
 956   in
 957   let small = CicSubstitution.lift 1 small in
 958   let ty = CicSubstitution.lift 1 ty in
 959   let expansions, _ = betaexpand_term menv context ugraph table 0 big in
 960   let fix_preds (t, subst, menv, ug, (eq_found, eq_URI)) =
 961     let pred =
 962       match pos with
 963       | Utils.Left ->
 964           Cic.Appl [eq;ty;small;t]
 965       | Utils.Right ->
 966           Cic.Appl [eq;ty;t;small]
 967     in
 968     (pred, subst, menv, ug, (eq_found, eq_URI))
 969   in
 970   List.map (build_newgoal context proof)
 971     (List.map fix_preds expansions)
 972 ;;
 973
 974 let sup_r_counter = ref 1;;
 975
 976 (**
 977    superposition_right
 978    returns a list of new clauses inferred with a right superposition step
 979    between the positive equation "target" and one in the "table" "newmeta" is
 980    the first free meta index, i.e. the first number above the highest meta
 981    index: its updated value is also returned
 982 *)
 983 let superposition_right newmeta (metasenv, context, ugraph) table target =
 984   let module C = Cic in
 985   let module S = CicSubstitution in
 986   let module M = CicMetaSubst in
 987   let module HL = HelmLibraryObjects in
 988   let module CR = CicReduction in
 989   let module U = Utils in
 990   let w, eqproof, (eq_ty, left, right, ordering), newmetas,id =
 991     Equality.open_equality target
 992   in
 993   if Utils.debug_metas then
 994     ignore (check_target context target "superpositionright");
 995   let metasenv' = newmetas in
 996   let maxmeta = ref newmeta in
 997   let res1, res2 =
 998     let betaexpand_term metasenv context ugraph table d term =
 999       let t1 = Unix.gettimeofday () in
1000       let res = betaexpand_term metasenv context ugraph table d term in
1001       let t2 = Unix.gettimeofday () in
1002         beta_expand_time := !beta_expand_time  +. (t2 -. t1);
1003         res
1004     in
1005     match ordering with
1006     | U.Gt -> fst (betaexpand_term metasenv' context ugraph table 0 left), []
1007     | U.Lt -> [], fst (betaexpand_term metasenv' context ugraph table 0 right)
1008     | _ ->
1009         let res l r =
1010           List.filter
1011             (fun (_, subst, _, _, _) ->
1012                let subst = apply_subst subst in
1013                let o = !Utils.compare_terms (subst l) (subst r) in
1014                o <> U.Lt && o <> U.Le)
1015             (fst (betaexpand_term metasenv' context ugraph table 0 l))
1016         in
1017         (res left right), (res right left)
1018   in
1019   let build_new ordering (bo, s, m, ug, (eq_found, eq_URI)) =
1020     if Utils.debug_metas then
1021       ignore (check_target context (snd eq_found) "buildnew1" );
1022     let time1 = Unix.gettimeofday () in
1023
1024     let pos, equality =  eq_found in
1025     let (_, proof', (ty, what, other, _), menv',id') =
1026       Equality.open_equality  equality in
1027     let what, other = if pos = Utils.Left then what, other else other, what in
1028     let newgoal, newproof =
1029       (* qua *)
1030       let bo' =
1031         Utils.guarded_simpl context (apply_subst s (S.subst other bo))
1032       in
1033       let name = C.Name "x" in
1034       incr sup_r_counter;
1035       let bo'' =
1036         let l, r =
1037           if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
1038         C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
1039                 S.lift 1 eq_ty; l; r]
1040       in
1041       bo',
1042         Equality.Step
1043           (s,(Equality.SuperpositionRight,
1044                id,(pos,id'),(Cic.Lambda(name,ty,bo''))))
1045     in
1046     let newmeta, newequality =
1047       let left, right =
1048         if ordering = U.Gt then newgoal, apply_subst s right
1049         else apply_subst s left, newgoal in
1050       let neworder = !Utils.compare_terms left right in
1051       let newmenv = (* Inference.filter s *) m in
1052       let stat = (eq_ty, left, right, neworder) in
1053       let eq' =
1054         let w = Utils.compute_equality_weight stat in
1055         Equality.mk_equality (w, newproof, stat, newmenv) in
1056       if Utils.debug_metas then
1057         ignore (check_target context eq' "buildnew3");
1058       let newm, eq' = Equality.fix_metas !maxmeta eq' in
1059       if Utils.debug_metas then
1060         ignore (check_target context eq' "buildnew4");
1061       newm, eq'
1062     in
1063     maxmeta := newmeta;
1064     let time2 = Unix.gettimeofday () in
1065     build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
1066     if Utils.debug_metas then
1067       ignore(check_target context newequality "buildnew2");
1068     newequality
1069   in
1070   let new1 = List.map (build_new U.Gt) res1
1071   and new2 = List.map (build_new U.Lt) res2 in
1072   let ok e = not (Equality.is_identity (metasenv', context, ugraph) e) in
1073   (!maxmeta,
1074    (List.filter ok (new1 @ new2)))
1075 ;;
1076
1077
1078 (** demodulation, when the target is a goal *)
1079 let rec demodulation_goal newmeta env table goal =
1080   let module C = Cic in
1081   let module S = CicSubstitution in
1082   let module M = CicMetaSubst in
1083   let module HL = HelmLibraryObjects in
1084   let metasenv, context, ugraph = env in
1085   let maxmeta = ref newmeta in
1086   let goalproof, metas, term = goal in
1087   let term = Utils.guarded_simpl (~debug:true) context term in
1088   let goal = goalproof, metas, term in
1089   let metasenv' = metas in
1090
1091   let build_newgoal (t, subst, menv, ug, (eq_found, eq_URI)) =
1092     let pos, equality = eq_found in
1093     let (_, proof', (ty, what, other, _), menv',id) =
1094       Equality.open_equality equality in
1095     let what, other = if pos = Utils.Left then what, other else other, what in
1096     let ty =
1097       try fst (CicTypeChecker.type_of_aux' menv' context what ugraph)
1098       with
1099       | CicUtil.Meta_not_found _
1100       | Invalid_argument("List.fold_left2") -> ty
1101     in
1102     let newterm, newgoalproof =
1103       let bo =
1104         Utils.guarded_simpl context (apply_subst subst(S.subst other t))
1105       in
1106       let bo' = (*apply_subst subst*) t in
1107       let name = C.Name "x" in
1108       incr demod_counter;
1109       let newgoalproofstep = (pos,id,subst,Cic.Lambda (name,ty,bo')) in
1110       bo, (newgoalproofstep::goalproof)
1111     in
1112     let newmetasenv = (* Inference.filter subst *) menv in
1113     !maxmeta, (newgoalproof, newmetasenv, newterm)
1114   in
1115   let res =
1116     demodulation_aux (* ~typecheck:true *) metasenv' context ugraph table 0 term
1117   in
1118   match res with
1119   | Some t ->
1120       let newmeta, newgoal = build_newgoal t in
1121       let _, _, newg = newgoal in
1122       if Equality.meta_convertibility term newg then
1123         false, newmeta, newgoal
1124       else
1125         let changed, newmeta, newgoal =
1126           demodulation_goal newmeta env table newgoal
1127         in
1128         true, newmeta, newgoal
1129   | None ->
1130       false, newmeta, goal
1131 ;;
1132
1133 (** demodulation, when the target is a theorem *)
1134 let rec demodulation_theorem newmeta env table theorem =
1135   let module C = Cic in
1136   let module S = CicSubstitution in
1137   let module M = CicMetaSubst in
1138   let module HL = HelmLibraryObjects in
1139   let metasenv, context, ugraph = env in
1140   let maxmeta = ref newmeta in
1141   let term, termty, metas = theorem in
1142   let metasenv' = metas in
1143
1144   let build_newtheorem (t, subst, menv, ug, (eq_found, eq_URI)) =
1145     let pos, equality = eq_found in
1146     let (_, proof', (ty, what, other, _), menv',id) =
1147       Equality.open_equality equality in
1148     let what, other = if pos = Utils.Left then what, other else other, what in
1149     let newterm, newty =
1150       let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
1151 (*      let bo' = apply_subst subst t in *)
1152 (*      let name = C.Name ("x_DemodThm_" ^ (string_of_int !demod_counter)) in*)
1153       incr demod_counter;
1154 (*
1155       let newproofold =
1156         Equality.ProofBlock (subst, eq_URI, (name, ty), bo', eq_found,
1157                               Equality.BasicProof (Equality.empty_subst,term))
1158       in
1159       (Equality.build_proof_term_old newproofold, bo)
1160 *)
1161       (* TODO, not ported to the new proofs *)
1162       if true then assert false; term, bo
1163     in
1164     !maxmeta, (newterm, newty, menv)
1165   in
1166   let res =
1167     demodulation_aux (* ~typecheck:true *) metasenv' context ugraph table 0 termty
1168   in
1169   match res with
1170   | Some t ->
1171       let newmeta, newthm = build_newtheorem t in
1172       let newt, newty, _ = newthm in
1173       if Equality.meta_convertibility termty newty then
1174         newmeta, newthm
1175       else
1176         demodulation_theorem newmeta env table newthm
1177   | None ->
1178       newmeta, theorem
1179 ;;
1180