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