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