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