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