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