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