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), _, _)), _))::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 context what other ugraph in
 335               let t2 = Unix.gettimeofday () in
 336               match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
 337               r
 338             with Inference.MatchingFailure as e ->
 339               let t2 = Unix.gettimeofday () in
 340               match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
 341               raise e
 342           in
 343           if samesubst subst subst' then
 344             true, subst
 345           else
 346             ok what tl
 347         with Inference.MatchingFailure ->
 348           ok what tl
 349   in
 350   let r, subst = ok right leftr in
 351   if r then
 352     true, subst
 353   else
 354     let rightr =
 355       match right with
 356       | Cic.Meta _ -> []
 357       | _ ->
 358           let rightc = get_candidates Matching table right in
 359           find_all_matches ~unif_fun:Inference.matching
 360             metasenv context ugraph 0 right ty rightc
 361     in
 362     ok left rightr
 363 ;;
 364
 365
 366 let rec demodulation_aux ?(typecheck=false)
 367     metasenv context ugraph table lift_amount term =
 368   let module C = Cic in
 369   let module S = CicSubstitution in
 370   let module M = CicMetaSubst in
 371   let module HL = HelmLibraryObjects in
 372   let candidates = get_candidates Matching table term in
 373   match term with
 374   | C.Meta _ -> None
 375   | term ->
 376       let termty, ugraph =
 377         if typecheck then
 378           CicTypeChecker.type_of_aux' metasenv context term ugraph
 379         else
 380           C.Implicit None, ugraph
 381       in
 382       let res =
 383         find_matches metasenv context ugraph lift_amount term termty candidates
 384       in
 385       if res <> None then
 386         res
 387       else
 388         match term with
 389         | C.Appl l ->
 390             let res, ll =
 391               List.fold_left
 392                 (fun (res, tl) t ->
 393                    if res <> None then
 394                      (res, tl @ [S.lift 1 t])
 395                    else
 396                      let r =
 397                        demodulation_aux metasenv context ugraph table
 398                          lift_amount t
 399                      in
 400                      match r with
 401                      | None -> (None, tl @ [S.lift 1 t])
 402                      | Some (rel, _, _, _, _) -> (r, tl @ [rel]))
 403                 (None, []) l
 404             in (
 405               match res with
 406               | None -> None
 407               | Some (_, subst, menv, ug, eq_found) ->
 408                   Some (C.Appl ll, subst, menv, ug, eq_found)
 409             )
 410         | C.Prod (nn, s, t) ->
 411             let r1 =
 412               demodulation_aux metasenv context ugraph table lift_amount s in (
 413               match r1 with
 414               | None ->
 415                   let r2 =
 416                     demodulation_aux metasenv
 417                       ((Some (nn, C.Decl s))::context) ugraph
 418                       table (lift_amount+1) t
 419                   in (
 420                     match r2 with
 421                     | None -> None
 422                     | Some (t', subst, menv, ug, eq_found) ->
 423                         Some (C.Prod (nn, (S.lift 1 s), t'),
 424                               subst, menv, ug, eq_found)
 425                   )
 426               | Some (s', subst, menv, ug, eq_found) ->
 427                   Some (C.Prod (nn, s', (S.lift 1 t)),
 428                         subst, menv, ug, eq_found)
 429             )
 430         | C.Lambda (nn, s, t) ->
 431             let r1 =
 432               demodulation_aux metasenv context ugraph table lift_amount s in (
 433               match r1 with
 434               | None ->
 435                   let r2 =
 436                     demodulation_aux metasenv
 437                       ((Some (nn, C.Decl s))::context) ugraph
 438                       table (lift_amount+1) t
 439                   in (
 440                     match r2 with
 441                     | None -> None
 442                     | Some (t', subst, menv, ug, eq_found) ->
 443                         Some (C.Lambda (nn, (S.lift 1 s), t'),
 444                               subst, menv, ug, eq_found)
 445                   )
 446               | Some (s', subst, menv, ug, eq_found) ->
 447                   Some (C.Lambda (nn, s', (S.lift 1 t)),
 448                         subst, menv, ug, eq_found)
 449             )
 450         | t ->
 451             None
 452 ;;
 453
 454
 455 let build_newtarget_time = ref 0.;;
 456
 457
 458 let demod_counter = ref 1;;
 459
 460 (** demodulation, when target is an equality *)
 461 let rec demodulation_equality newmeta env table sign target =
 462   let module C = Cic in
 463   let module S = CicSubstitution in
 464   let module M = CicMetaSubst in
 465   let module HL = HelmLibraryObjects in
 466   let metasenv, context, ugraph = env in
 467   let _, proof, (eq_ty, left, right, order), metas, args = target in
 468   let metasenv' = metasenv @ metas in
 469
 470   let maxmeta = ref newmeta in
 471
 472   let build_newtarget is_left (t, subst, menv, ug, (eq_found, eq_URI)) =
 473     let time1 = Unix.gettimeofday () in
 474
 475     let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
 476     let ty =
 477       try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
 478       with CicUtil.Meta_not_found _ -> ty
 479     in
 480     let what, other = if pos = Utils.Left then what, other else other, what in
 481     let newterm, newproof =
 482       let bo = apply_subst subst (S.subst other t) in
 483       let name = C.Name ("x_Demod_" ^ (string_of_int !demod_counter)) in
 484       incr demod_counter;
 485       let bo' =
 486         let l, r = if is_left then t, S.lift 1 right else S.lift 1 left, t in
 487         C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
 488                 S.lift 1 eq_ty; l; r]
 489       in
 490       if sign = Utils.Positive then
 491         (bo,
 492          Inference.ProofBlock (
 493            subst, eq_URI, (name, ty), bo'(* t' *), eq_found, proof))
 494       else
 495         let metaproof =
 496           incr maxmeta;
 497           let irl =
 498             CicMkImplicit.identity_relocation_list_for_metavariable context in
 499           debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta));
 500           print_newline ();
 501           C.Meta (!maxmeta, irl)
 502         in
 503           let eq_found =
 504             let proof' =
 505               let termlist =
 506                 if pos = Utils.Left then [ty; what; other]
 507                 else [ty; other; what]
 508               in
 509               Inference.ProofSymBlock (termlist, proof')
 510             in
 511             let what, other =
 512               if pos = Utils.Left then what, other else other, what
 513             in
 514             pos, (0, proof', (ty, other, what, Utils.Incomparable),
 515                   menv', args')
 516           in
 517           let target_proof =
 518             let pb =
 519               Inference.ProofBlock (subst, eq_URI, (name, ty), bo',
 520                                     eq_found, Inference.BasicProof metaproof)
 521             in
 522             match proof with
 523             | Inference.BasicProof _ ->
 524                 print_endline "replacing a BasicProof";
 525                 pb
 526             | Inference.ProofGoalBlock (_, parent_proof) ->
 527                 print_endline "replacing another ProofGoalBlock";
 528                 Inference.ProofGoalBlock (pb, parent_proof)
 529             | _ -> assert false
 530           in
 531         let refl =
 532           C.Appl [C.MutConstruct (* reflexivity *)
 533                     (LibraryObjects.eq_URI (), 0, 1, []);
 534                   eq_ty; if is_left then right else left]
 535         in
 536         (bo,
 537          Inference.ProofGoalBlock (Inference.BasicProof refl, target_proof))
 538     in
 539     let left, right = if is_left then newterm, right else left, newterm in
 540     let m = (Inference.metas_of_term left) @ (Inference.metas_of_term right) in
 541     let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) metas
 542     and newargs = args
 543     in
 544     let ordering = !Utils.compare_terms left right in
 545
 546     let time2 = Unix.gettimeofday () in
 547     build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
 548
 549     let res =
 550       let w = Utils.compute_equality_weight eq_ty left right in
 551       (w, newproof, (eq_ty, left, right, ordering), newmetasenv, newargs)
 552     in
 553     !maxmeta, res
 554   in
 555   let res = demodulation_aux metasenv' context ugraph table 0 left in
 556   match res with
 557   | Some t ->
 558       let newmeta, newtarget = build_newtarget true t in
 559       if (Inference.is_identity (metasenv', context, ugraph) newtarget) ||
 560         (Inference.meta_convertibility_eq target newtarget) then
 561           newmeta, newtarget
 562       else
 563         demodulation_equality newmeta env table sign newtarget
 564   | None ->
 565       let res = demodulation_aux metasenv' context ugraph table 0 right in
 566       match res with
 567       | Some t ->
 568           let newmeta, newtarget = build_newtarget false 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           newmeta, target
 576 ;;
 577
 578
 579 (**
 580    Performs the beta expansion of the term "term" w.r.t. "table",
 581    i.e. returns the list of all the terms t s.t. "(t term) = t2", for some t2
 582    in table.
 583 *)
 584 let rec betaexpand_term metasenv context ugraph table lift_amount term =
 585   let module C = Cic in
 586   let module S = CicSubstitution in
 587   let module M = CicMetaSubst in
 588   let module HL = HelmLibraryObjects in
 589   let candidates = get_candidates Unification table term in
 590   let res, lifted_term =
 591     match term with
 592     | C.Meta (i, l) ->
 593         let l', lifted_l =
 594           List.fold_right
 595             (fun arg (res, lifted_tl) ->
 596                match arg with
 597                | Some arg ->
 598                    let arg_res, lifted_arg =
 599                      betaexpand_term metasenv context ugraph table
 600                        lift_amount arg in
 601                    let l1 =
 602                      List.map
 603                        (fun (t, s, m, ug, eq_found) ->
 604                           (Some t)::lifted_tl, s, m, ug, eq_found)
 605                        arg_res
 606                    in
 607                    (l1 @
 608                       (List.map
 609                          (fun (l, s, m, ug, eq_found) ->
 610                             (Some lifted_arg)::l, s, m, ug, eq_found)
 611                          res),
 612                     (Some lifted_arg)::lifted_tl)
 613                | None ->
 614                    (List.map
 615                       (fun (r, s, m, ug, eq_found) ->
 616                          None::r, s, m, ug, eq_found) res,
 617                     None::lifted_tl)
 618             ) l ([], [])
 619         in
 620         let e =
 621           List.map
 622             (fun (l, s, m, ug, eq_found) ->
 623                (C.Meta (i, l), s, m, ug, eq_found)) l'
 624         in
 625         e, C.Meta (i, lifted_l)
 626
 627     | C.Rel m ->
 628         [], if m <= lift_amount then C.Rel m else C.Rel (m+1)
 629
 630     | C.Prod (nn, s, t) ->
 631         let l1, lifted_s =
 632           betaexpand_term metasenv context ugraph table lift_amount s in
 633         let l2, lifted_t =
 634           betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
 635             table (lift_amount+1) t in
 636         let l1' =
 637           List.map
 638             (fun (t, s, m, ug, eq_found) ->
 639                C.Prod (nn, t, lifted_t), s, m, ug, eq_found) l1
 640         and l2' =
 641           List.map
 642             (fun (t, s, m, ug, eq_found) ->
 643                C.Prod (nn, lifted_s, t), s, m, ug, eq_found) l2 in
 644         l1' @ l2', C.Prod (nn, lifted_s, lifted_t)
 645
 646     | C.Lambda (nn, s, t) ->
 647         let l1, lifted_s =
 648           betaexpand_term metasenv context ugraph table lift_amount s in
 649         let l2, lifted_t =
 650           betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
 651             table (lift_amount+1) t in
 652         let l1' =
 653           List.map
 654             (fun (t, s, m, ug, eq_found) ->
 655                C.Lambda (nn, t, lifted_t), s, m, ug, eq_found) l1
 656         and l2' =
 657           List.map
 658             (fun (t, s, m, ug, eq_found) ->
 659                C.Lambda (nn, lifted_s, t), s, m, ug, eq_found) l2 in
 660         l1' @ l2', C.Lambda (nn, lifted_s, lifted_t)
 661
 662     | C.Appl l ->
 663         let l', lifted_l =
 664           List.fold_right
 665             (fun arg (res, lifted_tl) ->
 666                let arg_res, lifted_arg =
 667                  betaexpand_term metasenv context ugraph table lift_amount arg
 668                in
 669                let l1 =
 670                  List.map
 671                    (fun (a, s, m, ug, eq_found) ->
 672                       a::lifted_tl, s, m, ug, eq_found)
 673                    arg_res
 674                in
 675                (l1 @
 676                   (List.map
 677                      (fun (r, s, m, ug, eq_found) ->
 678                         lifted_arg::r, s, m, ug, eq_found)
 679                      res),
 680                 lifted_arg::lifted_tl)
 681             ) l ([], [])
 682         in
 683         (List.map
 684            (fun (l, s, m, ug, eq_found) -> (C.Appl l, s, m, ug, eq_found)) l',
 685          C.Appl lifted_l)
 686
 687     | t -> [], (S.lift lift_amount t)
 688   in
 689   match term with
 690   | C.Meta (i, l) -> res, lifted_term
 691   | term ->
 692       let termty, ugraph =
 693         C.Implicit None, ugraph
 694 (*         CicTypeChecker.type_of_aux' metasenv context term ugraph *)
 695       in
 696       let r =
 697         find_all_matches
 698           metasenv context ugraph lift_amount term termty candidates
 699       in
 700       r @ res, lifted_term
 701 ;;
 702
 703
 704 let sup_l_counter = ref 1;;
 705
 706 (**
 707    superposition_left
 708    returns a list of new clauses inferred with a left superposition step
 709    the negative equation "target" and one of the positive equations in "table"
 710 *)
 711 let superposition_left newmeta (metasenv, context, ugraph) table target =
 712   let module C = Cic in
 713   let module S = CicSubstitution in
 714   let module M = CicMetaSubst in
 715   let module HL = HelmLibraryObjects in
 716   let module CR = CicReduction in
 717   let module U = Utils in
 718   let weight, proof, (eq_ty, left, right, ordering), _, _ = target in
 719   let expansions, _ =
 720     let term = if ordering = U.Gt then left else right in
 721     betaexpand_term metasenv context ugraph table 0 term
 722   in
 723   let maxmeta = ref newmeta in
 724   let build_new (bo, s, m, ug, (eq_found, eq_URI)) =
 725
 726     debug_print (lazy "\nSUPERPOSITION LEFT\n");
 727
 728     let time1 = Unix.gettimeofday () in
 729
 730     let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
 731     let what, other = if pos = Utils.Left then what, other else other, what in
 732     let newgoal, newproof =
 733       let bo' = apply_subst s (S.subst other bo) in
 734       let name = C.Name ("x_SupL_" ^ (string_of_int !sup_l_counter)) in
 735       incr sup_l_counter;
 736       let bo'' =
 737         let l, r =
 738           if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
 739         C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
 740                 S.lift 1 eq_ty; l; r]
 741       in
 742       incr maxmeta;
 743       let metaproof =
 744         let irl =
 745           CicMkImplicit.identity_relocation_list_for_metavariable context in
 746         C.Meta (!maxmeta, irl)
 747       in
 748       let eq_found =
 749         let proof' =
 750           let termlist =
 751             if pos = Utils.Left then [ty; what; other]
 752             else [ty; other; what]
 753           in
 754           Inference.ProofSymBlock (termlist, proof')
 755         in
 756         let what, other =
 757           if pos = Utils.Left then what, other else other, what
 758         in
 759         pos, (0, proof', (ty, other, what, Utils.Incomparable), menv', args')
 760       in
 761       let target_proof =
 762         let pb =
 763           Inference.ProofBlock (s, eq_URI, (name, ty), bo'', eq_found,
 764                                 Inference.BasicProof metaproof)
 765         in
 766         match proof with
 767         | Inference.BasicProof _ ->
 768             debug_print (lazy "replacing a BasicProof");
 769             pb
 770         | Inference.ProofGoalBlock (_, parent_proof) ->
 771             debug_print (lazy "replacing another ProofGoalBlock");
 772             Inference.ProofGoalBlock (pb, parent_proof)
 773         | _ -> assert false
 774       in
 775       let refl =
 776         C.Appl [C.MutConstruct (* reflexivity *)
 777                   (LibraryObjects.eq_URI (), 0, 1, []);
 778                 eq_ty; if ordering = U.Gt then right else left]
 779       in
 780       (bo',
 781        Inference.ProofGoalBlock (Inference.BasicProof refl, target_proof))
 782     in
 783     let left, right =
 784       if ordering = U.Gt then newgoal, right else left, newgoal in
 785     let neworder = !Utils.compare_terms left right in
 786
 787     let time2 = Unix.gettimeofday () in
 788     build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
 789
 790     let res =
 791       let w = Utils.compute_equality_weight eq_ty left right in
 792       (w, newproof, (eq_ty, left, right, neworder), [], [])
 793     in
 794     res
 795   in
 796   !maxmeta, List.map build_new expansions
 797 ;;
 798
 799
 800 let sup_r_counter = ref 1;;
 801
 802 (**
 803    superposition_right
 804    returns a list of new clauses inferred with a right superposition step
 805    between the positive equation "target" and one in the "table" "newmeta" is
 806    the first free meta index, i.e. the first number above the highest meta
 807    index: its updated value is also returned
 808 *)
 809 let superposition_right newmeta (metasenv, context, ugraph) table target =
 810   let module C = Cic in
 811   let module S = CicSubstitution in
 812   let module M = CicMetaSubst in
 813   let module HL = HelmLibraryObjects in
 814   let module CR = CicReduction in
 815   let module U = Utils in
 816   let _, eqproof, (eq_ty, left, right, ordering), newmetas, args = target in
 817   let metasenv' = metasenv @ newmetas in
 818   let maxmeta = ref newmeta in
 819   let res1, res2 =
 820     match ordering with
 821     | U.Gt -> fst (betaexpand_term metasenv' context ugraph table 0 left), []
 822     | U.Lt -> [], fst (betaexpand_term metasenv' context ugraph table 0 right)
 823     | _ ->
 824         let res l r =
 825           List.filter
 826             (fun (_, subst, _, _, _) ->
 827                let subst = apply_subst subst in
 828                let o = !Utils.compare_terms (subst l) (subst r) in
 829                o <> U.Lt && o <> U.Le)
 830             (fst (betaexpand_term metasenv' context ugraph table 0 l))
 831         in
 832         (res left right), (res right left)
 833   in
 834   let build_new ordering (bo, s, m, ug, (eq_found, eq_URI)) =
 835
 836     let time1 = Unix.gettimeofday () in
 837
 838     let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
 839     let what, other = if pos = Utils.Left then what, other else other, what in
 840     let newgoal, newproof =
 841       let bo' = apply_subst s (S.subst other bo) in
 842       let t' =
 843         let name = C.Name ("x_SupR_" ^ (string_of_int !sup_r_counter)) in
 844         incr sup_r_counter;
 845         let l, r =
 846           if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
 847         (name, ty, S.lift 1 eq_ty, l, r)
 848       in
 849       let name = C.Name ("x_SupR_" ^ (string_of_int !sup_r_counter)) in
 850       incr sup_r_counter;
 851       let bo'' =
 852         let l, r =
 853           if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
 854         C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
 855                 S.lift 1 eq_ty; l; r]
 856       in
 857       bo',
 858       Inference.ProofBlock (s, eq_URI, (name, ty), bo'', eq_found, eqproof)
 859     in
 860     let newmeta, newequality =
 861       let left, right =
 862         if ordering = U.Gt then newgoal, apply_subst s right
 863         else apply_subst s left, newgoal in
 864       let neworder = !Utils.compare_terms left right
 865       and newmenv = newmetas @ menv'
 866       and newargs = args @ args' in
 867       let eq' =
 868         let w = Utils.compute_equality_weight eq_ty left right in
 869         (w, newproof, (eq_ty, left, right, neworder), newmenv, newargs)
 870       and env = (metasenv, context, ugraph) in
 871       let newm, eq' = Inference.fix_metas !maxmeta eq' in
 872       newm, eq'
 873     in
 874     maxmeta := newmeta;
 875
 876     let time2 = Unix.gettimeofday () in
 877     build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
 878
 879     newequality
 880   in
 881   let new1 = List.map (build_new U.Gt) res1
 882   and new2 = List.map (build_new U.Lt) res2 in
 883   let ok e = not (Inference.is_identity (metasenv, context, ugraph) e) in
 884   (!maxmeta,
 885    (List.filter ok (new1 @ new2)))
 886 ;;
 887
 888
 889 (** demodulation, when the target is a goal *)
 890 let rec demodulation_goal newmeta env table goal =
 891   let module C = Cic in
 892   let module S = CicSubstitution in
 893   let module M = CicMetaSubst in
 894   let module HL = HelmLibraryObjects in
 895   let metasenv, context, ugraph = env in
 896   let maxmeta = ref newmeta in
 897   let proof, metas, term = goal in
 898   let metasenv' = metasenv @ metas in
 899
 900   let build_newgoal (t, subst, menv, ug, (eq_found, eq_URI)) =
 901     let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
 902     let what, other = if pos = Utils.Left then what, other else other, what in
 903     let ty =
 904       try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
 905       with CicUtil.Meta_not_found _ -> ty
 906     in
 907     let newterm, newproof =
 908       let bo = apply_subst subst (S.subst other t) in
 909       let bo' = apply_subst subst t in
 910       let name = C.Name ("x_DemodGoal_" ^ (string_of_int !demod_counter)) in
 911       incr demod_counter;
 912       let metaproof =
 913         incr maxmeta;
 914         let irl =
 915           CicMkImplicit.identity_relocation_list_for_metavariable context in
 916         debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta));
 917         C.Meta (!maxmeta, irl)
 918       in
 919       let eq_found =
 920         let proof' =
 921           let termlist =
 922             if pos = Utils.Left then [ty; what; other]
 923             else [ty; other; what]
 924           in
 925           Inference.ProofSymBlock (termlist, proof')
 926         in
 927         let what, other =
 928           if pos = Utils.Left then what, other else other, what
 929         in
 930         pos, (0, proof', (ty, other, what, Utils.Incomparable), menv', args')
 931       in
 932       let goal_proof =
 933         let pb =
 934           Inference.ProofBlock (subst, eq_URI, (name, ty), bo',
 935                                 eq_found, Inference.BasicProof metaproof)
 936         in
 937         let rec repl = function
 938           | Inference.NoProof ->
 939               debug_print (lazy "replacing a NoProof");
 940               pb
 941           | Inference.BasicProof _ ->
 942               debug_print (lazy "replacing a BasicProof");
 943               pb
 944           | Inference.ProofGoalBlock (_, parent_proof) ->
 945               debug_print (lazy "replacing another ProofGoalBlock");
 946               Inference.ProofGoalBlock (pb, parent_proof)
 947           | (Inference.SubProof (term, meta_index, p) as subproof) ->
 948               debug_print
 949                 (lazy
 950                    (Printf.sprintf "replacing %s"
 951                       (Inference.string_of_proof subproof)));
 952               Inference.SubProof (term, meta_index, repl p)
 953           | _ -> assert false
 954         in repl proof
 955       in
 956       bo, Inference.ProofGoalBlock (Inference.NoProof, goal_proof)
 957     in
 958     let m = Inference.metas_of_term newterm in
 959     let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) metas in
 960     !maxmeta, (newproof, newmetasenv, newterm)
 961   in
 962   let res =
 963     demodulation_aux ~typecheck:true metasenv' context ugraph table 0 term
 964   in
 965   match res with
 966   | Some t ->
 967       let newmeta, newgoal = build_newgoal t in
 968       let _, _, newg = newgoal in
 969       if Inference.meta_convertibility term newg then
 970         newmeta, newgoal
 971       else
 972         demodulation_goal newmeta env table newgoal
 973   | None ->
 974       newmeta, goal
 975 ;;
 976
 977
 978 (** demodulation, when the target is a theorem *)
 979 let rec demodulation_theorem newmeta env table theorem =
 980   let module C = Cic in
 981   let module S = CicSubstitution in
 982   let module M = CicMetaSubst in
 983   let module HL = HelmLibraryObjects in
 984   let metasenv, context, ugraph = env in
 985   let maxmeta = ref newmeta in
 986   let proof, metas, term = theorem in
 987   let term, termty, metas = theorem in
 988   let metasenv' = metasenv @ metas in
 989
 990   let build_newtheorem (t, subst, menv, ug, (eq_found, eq_URI)) =
 991     let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
 992     let what, other = if pos = Utils.Left then what, other else other, what in
 993     let newterm, newty =
 994       let bo = apply_subst subst (S.subst other t) in
 995       let bo' = apply_subst subst t in
 996       let name = C.Name ("x_DemodThm_" ^ (string_of_int !demod_counter)) in
 997       incr demod_counter;
 998       let newproof =
 999         Inference.ProofBlock (subst, eq_URI, (name, ty), bo', eq_found,
1000                               Inference.BasicProof term)
1001       in
1002       (Inference.build_proof_term newproof, bo)
1003     in
1004     let m = Inference.metas_of_term newterm in
1005     let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) metas in
1006     !maxmeta, (newterm, newty, newmetasenv)
1007   in
1008   let res =
1009     demodulation_aux ~typecheck:true metasenv' context ugraph table 0 termty
1010   in
1011   match res with
1012   | Some t ->
1013       let newmeta, newthm = build_newtheorem t in
1014       let newt, newty, _ = newthm in
1015       if Inference.meta_convertibility termty newty then
1016         newmeta, newthm
1017       else
1018         demodulation_theorem newmeta env table newthm
1019   | None ->
1020       newmeta, theorem
1021 ;;