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