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, Utils.eq_ind_URI ()
 232             else right, left, Utils.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, Utils.eq_ind_URI ()
 321             else right, left, Utils.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_newtarget_time = ref 0.;;
 511
 512
 513 let demod_counter = ref 1;;
 514
 515 let rec demodulation_equality newmeta env table sign target =
 516   let module C = Cic in
 517   let module S = CicSubstitution in
 518   let module M = CicMetaSubst in
 519   let module HL = HelmLibraryObjects in
 520   let metasenv, context, ugraph = env in
 521   let _, proof, (eq_ty, left, right, order), metas, args = target in
 522   let metasenv' = metasenv @ metas in
 523
 524   let maxmeta = ref newmeta in
 525
 526   let build_newtarget is_left (t, subst, menv, ug, (eq_found, eq_URI)) =
 527     let time1 = Unix.gettimeofday () in
 528
 529     let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
 530     let ty =
 531       try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
 532       with CicUtil.Meta_not_found _ -> ty
 533     in
 534     let what, other = if pos = Utils.Left then what, other else other, what in
 535     let newterm, newproof =
 536       let bo = (* M. *)apply_subst subst (S.subst other t) in
 537 (*       let t' = *)
 538 (*         let name = C.Name ("x_Demod_" ^ (string_of_int !demod_counter)) in *)
 539 (*         incr demod_counter; *)
 540 (*         let l, r = *)
 541 (*           if is_left then t, S.lift 1 right else S.lift 1 left, t in *)
 542 (*         (name, ty, S.lift 1 eq_ty, l, r) *)
 543 (*       in *)
 544       let name = C.Name ("x_Demod_" ^ (string_of_int !demod_counter)) in
 545       incr demod_counter;
 546       let bo' =
 547         let l, r = if is_left then t, S.lift 1 right else S.lift 1 left, t in
 548         C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
 549                 S.lift 1 eq_ty; l; r]
 550       in
 551       if sign = Utils.Positive then
 552         (bo,
 553          Inference.ProofBlock (
 554            subst, eq_URI, (name, ty), bo'(* t' *), eq_found, proof))
 555       else
 556         let metaproof =
 557           incr maxmeta;
 558           let irl =
 559             CicMkImplicit.identity_relocation_list_for_metavariable context in
 560           Printf.printf "\nADDING META: %d\n" !maxmeta;
 561           print_newline ();
 562           C.Meta (!maxmeta, irl)
 563         in
 564 (*         let target' = *)
 565           let eq_found =
 566             let proof' =
 567 (*               let ens = *)
 568 (*                 if pos = Utils.Left then *)
 569 (*                   build_ens_for_sym_eq ty what other *)
 570 (*                 else *)
 571 (*                   build_ens_for_sym_eq ty other what *)
 572               let termlist =
 573                 if pos = Utils.Left then [ty; what; other]
 574                 else [ty; other; what]
 575               in
 576               Inference.ProofSymBlock (termlist, proof')
 577             in
 578             let what, other =
 579               if pos = Utils.Left then what, other else other, what
 580             in
 581             pos, (0, proof', (ty, other, what, Utils.Incomparable),
 582                   menv', args')
 583           in
 584           let target_proof =
 585             let pb =
 586               Inference.ProofBlock (subst, eq_URI, (name, ty), bo'(* t' *),
 587                                     eq_found, Inference.BasicProof metaproof)
 588             in
 589             match proof with
 590             | Inference.BasicProof _ ->
 591                 print_endline "replacing a BasicProof";
 592                 pb
 593             | Inference.ProofGoalBlock (_, parent_proof(* parent_eq *)) ->
 594                 print_endline "replacing another ProofGoalBlock";
 595                 Inference.ProofGoalBlock (pb, parent_proof(* parent_eq *))
 596             | _ -> assert false
 597           in
 598 (*           (0, target_proof, (eq_ty, left, right, order), metas, args) *)
 599 (*         in *)
 600         let refl =
 601           C.Appl [C.MutConstruct (* reflexivity *)
 602                     (LibraryObjects.eq_URI (), 0, 1, []);
 603                   eq_ty; if is_left then right else left]
 604         in
 605         (bo,
 606          Inference.ProofGoalBlock (Inference.BasicProof refl, target_proof(* target' *)))
 607     in
 608     let left, right = if is_left then newterm, right else left, newterm in
 609     let m = (Inference.metas_of_term left) @ (Inference.metas_of_term right) in
 610     let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) metas
 611     and newargs = args
 612 (*       let a =  *)
 613 (*         List.filter *)
 614 (*           (function C.Meta (i, _) -> List.mem i m | _ -> assert false) args in *)
 615 (*       let delta = (List.length args) - (List.length a) in *)
 616 (*       if delta > 0 then *)
 617 (*         let first = List.hd a in *)
 618 (*         let rec aux l = function *)
 619 (*           | 0 -> l *)
 620 (*           | d -> let l = aux l (d-1) in l @ [first] *)
 621 (*         in *)
 622 (*         aux a delta *)
 623 (*       else *)
 624 (*         a *)
 625     in
 626     let ordering = !Utils.compare_terms left right in
 627
 628     let time2 = Unix.gettimeofday () in
 629     build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
 630
 631     let res =
 632       let w = Utils.compute_equality_weight eq_ty left right in
 633       (w, newproof, (eq_ty, left, right, ordering), newmetasenv, newargs)
 634     in
 635     !maxmeta, res
 636   in
 637   let res = demodulation_aux metasenv' context ugraph table 0 left in
 638   match res with
 639   | Some t ->
 640       let newmeta, newtarget = build_newtarget true t in
 641       if (Inference.is_identity (metasenv', context, ugraph) newtarget) ||
 642         (Inference.meta_convertibility_eq target newtarget) then
 643           newmeta, newtarget
 644       else
 645 (*         if subsumption env table newtarget then *)
 646 (*           newmeta, build_identity newtarget *)
 647 (*         else *)
 648         demodulation_equality newmeta env table sign newtarget
 649   | None ->
 650       let res = demodulation_aux metasenv' context ugraph table 0 right in
 651       match res with
 652       | Some t ->
 653           let newmeta, newtarget = build_newtarget false t in
 654           if (Inference.is_identity (metasenv', context, ugraph) newtarget) ||
 655             (Inference.meta_convertibility_eq target newtarget) then
 656               newmeta, newtarget
 657           else
 658 (*             if subsumption env table newtarget then *)
 659 (*               newmeta, build_identity newtarget *)
 660 (*             else *)
 661               demodulation_equality newmeta env table sign newtarget
 662       | None ->
 663           newmeta, target
 664 ;;
 665
 666
 667 let rec betaexpand_term metasenv context ugraph table lift_amount term =
 668   let module C = Cic in
 669   let module S = CicSubstitution in
 670   let module M = CicMetaSubst in
 671   let module HL = HelmLibraryObjects in
 672   let candidates = get_candidates Unification table term in
 673   let res, lifted_term =
 674     match term with
 675     | C.Meta (i, l) ->
 676         let l', lifted_l =
 677           List.fold_right
 678             (fun arg (res, lifted_tl) ->
 679                match arg with
 680                | Some arg ->
 681                    let arg_res, lifted_arg =
 682                      betaexpand_term metasenv context ugraph table
 683                        lift_amount arg in
 684                    let l1 =
 685                      List.map
 686                        (fun (t, s, m, ug, eq_found) ->
 687                           (Some t)::lifted_tl, s, m, ug, eq_found)
 688                        arg_res
 689                    in
 690                    (l1 @
 691                       (List.map
 692                          (fun (l, s, m, ug, eq_found) ->
 693                             (Some lifted_arg)::l, s, m, ug, eq_found)
 694                          res),
 695                     (Some lifted_arg)::lifted_tl)
 696                | None ->
 697                    (List.map
 698                       (fun (r, s, m, ug, eq_found) ->
 699                          None::r, s, m, ug, eq_found) res,
 700                     None::lifted_tl)
 701             ) l ([], [])
 702         in
 703         let e =
 704           List.map
 705             (fun (l, s, m, ug, eq_found) ->
 706                (C.Meta (i, l), s, m, ug, eq_found)) l'
 707         in
 708         e, C.Meta (i, lifted_l)
 709
 710     | C.Rel m ->
 711         [], if m <= lift_amount then C.Rel m else C.Rel (m+1)
 712
 713     | C.Prod (nn, s, t) ->
 714         let l1, lifted_s =
 715           betaexpand_term metasenv context ugraph table lift_amount s in
 716         let l2, lifted_t =
 717           betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
 718             table (lift_amount+1) t in
 719         let l1' =
 720           List.map
 721             (fun (t, s, m, ug, eq_found) ->
 722                C.Prod (nn, t, lifted_t), s, m, ug, eq_found) l1
 723         and l2' =
 724           List.map
 725             (fun (t, s, m, ug, eq_found) ->
 726                C.Prod (nn, lifted_s, t), s, m, ug, eq_found) l2 in
 727         l1' @ l2', C.Prod (nn, lifted_s, lifted_t)
 728
 729     | C.Lambda (nn, s, t) ->
 730         let l1, lifted_s =
 731           betaexpand_term metasenv context ugraph table lift_amount s in
 732         let l2, lifted_t =
 733           betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
 734             table (lift_amount+1) t in
 735         let l1' =
 736           List.map
 737             (fun (t, s, m, ug, eq_found) ->
 738                C.Lambda (nn, t, lifted_t), s, m, ug, eq_found) l1
 739         and l2' =
 740           List.map
 741             (fun (t, s, m, ug, eq_found) ->
 742                C.Lambda (nn, lifted_s, t), s, m, ug, eq_found) l2 in
 743         l1' @ l2', C.Lambda (nn, lifted_s, lifted_t)
 744
 745     | C.Appl l ->
 746         let l', lifted_l =
 747           List.fold_right
 748             (fun arg (res, lifted_tl) ->
 749                let arg_res, lifted_arg =
 750                  betaexpand_term metasenv context ugraph table lift_amount arg
 751                in
 752                let l1 =
 753                  List.map
 754                    (fun (a, s, m, ug, eq_found) ->
 755                       a::lifted_tl, s, m, ug, eq_found)
 756                    arg_res
 757                in
 758                (l1 @
 759                   (List.map
 760                      (fun (r, s, m, ug, eq_found) ->
 761                         lifted_arg::r, s, m, ug, eq_found)
 762                      res),
 763                 lifted_arg::lifted_tl)
 764             ) l ([], [])
 765         in
 766         (List.map
 767            (fun (l, s, m, ug, eq_found) -> (C.Appl l, s, m, ug, eq_found)) l',
 768          C.Appl lifted_l)
 769
 770     | t -> [], (S.lift lift_amount t)
 771   in
 772   match term with
 773   | C.Meta (i, l) -> res, lifted_term
 774   | term ->
 775       let termty, ugraph =
 776         C.Implicit None, ugraph
 777 (*         CicTypeChecker.type_of_aux' metasenv context term ugraph *)
 778       in
 779       let r =
 780         find_all_matches
 781           metasenv context ugraph lift_amount term termty candidates
 782       in
 783       r @ res, lifted_term
 784 ;;
 785
 786
 787 let sup_l_counter = ref 1;;
 788
 789 let superposition_left newmeta (metasenv, context, ugraph) table target =
 790   let module C = Cic in
 791   let module S = CicSubstitution in
 792   let module M = CicMetaSubst in
 793   let module HL = HelmLibraryObjects in
 794   let module CR = CicReduction in
 795   let module U = Utils in
 796   let weight, proof, (eq_ty, left, right, ordering), _, _ = target in
 797   let expansions, _ =
 798     let term = if ordering = U.Gt then left else right in
 799     betaexpand_term metasenv context ugraph table 0 term
 800   in
 801   let maxmeta = ref newmeta in
 802   let build_new (bo, s, m, ug, (eq_found, eq_URI)) =
 803
 804     print_endline "\nSUPERPOSITION LEFT\n";
 805
 806     let time1 = Unix.gettimeofday () in
 807
 808     let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
 809     let what, other = if pos = Utils.Left then what, other else other, what in
 810     let newgoal, newproof =
 811       let bo' = (* M. *)apply_subst s (S.subst other bo) in
 812 (*       let t' = *)
 813 (*         let name = C.Name ("x_SupL_" ^ (string_of_int !sup_l_counter)) in *)
 814 (*         incr sup_l_counter; *)
 815 (*         let l, r = *)
 816 (*           if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in *)
 817 (*         (name, ty, S.lift 1 eq_ty, l, r) *)
 818 (*       in *)
 819       let name = C.Name ("x_SupL_" ^ (string_of_int !sup_l_counter)) in
 820       incr sup_l_counter;
 821       let bo'' =
 822         let l, r =
 823           if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
 824         C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
 825                 S.lift 1 eq_ty; l; r]
 826       in
 827       incr maxmeta;
 828       let metaproof =
 829         let irl =
 830           CicMkImplicit.identity_relocation_list_for_metavariable context in
 831         C.Meta (!maxmeta, irl)
 832       in
 833 (*       let target' = *)
 834         let eq_found =
 835           let proof' =
 836 (*             let ens = *)
 837 (*               if pos = Utils.Left then *)
 838 (*                 build_ens_for_sym_eq ty what other *)
 839 (*               else *)
 840 (*                 build_ens_for_sym_eq ty other what *)
 841 (*             in *)
 842             let termlist =
 843               if pos = Utils.Left then [ty; what; other]
 844               else [ty; other; what]
 845             in
 846             Inference.ProofSymBlock (termlist, proof')
 847           in
 848           let what, other =
 849             if pos = Utils.Left then what, other else other, what
 850           in
 851           pos, (0, proof', (ty, other, what, Utils.Incomparable), menv', args')
 852         in
 853         let target_proof =
 854           let pb =
 855             Inference.ProofBlock (s, eq_URI, (name, ty), bo''(* t' *), eq_found,
 856                                   Inference.BasicProof metaproof)
 857           in
 858           match proof with
 859           | Inference.BasicProof _ ->
 860               print_endline "replacing a BasicProof";
 861               pb
 862           | Inference.ProofGoalBlock (_, parent_proof(* parent_eq *)) ->
 863               print_endline "replacing another ProofGoalBlock";
 864               Inference.ProofGoalBlock (pb, parent_proof(* parent_eq *))
 865           | _ -> assert false
 866         in
 867 (*         (weight, target_proof, (eq_ty, left, right, ordering), [], []) *)
 868 (*       in *)
 869       let refl =
 870         C.Appl [C.MutConstruct (* reflexivity *)
 871                   (LibraryObjects.eq_URI (), 0, 1, []);
 872                 eq_ty; if ordering = U.Gt then right else left]
 873       in
 874       (bo',
 875        Inference.ProofGoalBlock (Inference.BasicProof refl, target_proof(* target' *)))
 876     in
 877     let left, right =
 878       if ordering = U.Gt then newgoal, right else left, newgoal in
 879     let neworder = !Utils.compare_terms left right in
 880
 881     let time2 = Unix.gettimeofday () in
 882     build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
 883
 884     let res =
 885       let w = Utils.compute_equality_weight eq_ty left right in
 886       (w, newproof, (eq_ty, left, right, neworder), [], [])
 887     in
 888     res
 889   in
 890   !maxmeta, List.map build_new expansions
 891 ;;
 892
 893
 894 let sup_r_counter = ref 1;;
 895
 896 let superposition_right newmeta (metasenv, context, ugraph) table target =
 897   let module C = Cic in
 898   let module S = CicSubstitution in
 899   let module M = CicMetaSubst in
 900   let module HL = HelmLibraryObjects in
 901   let module CR = CicReduction in
 902   let module U = Utils in
 903   let _, eqproof, (eq_ty, left, right, ordering), newmetas, args = target in
 904   let metasenv' = metasenv @ newmetas in
 905   let maxmeta = ref newmeta in
 906   let res1, res2 =
 907     match ordering with
 908     | U.Gt -> fst (betaexpand_term metasenv' context ugraph table 0 left), []
 909     | U.Lt -> [], fst (betaexpand_term metasenv' context ugraph table 0 right)
 910     | _ ->
 911         let res l r =
 912           List.filter
 913             (fun (_, subst, _, _, _) ->
 914                let subst = (* M. *)apply_subst subst in
 915                let o = !Utils.compare_terms (subst l) (subst r) in
 916                o <> U.Lt && o <> U.Le)
 917             (fst (betaexpand_term metasenv' context ugraph table 0 l))
 918         in
 919         (res left right), (res right left)
 920   in
 921   let build_new ordering (bo, s, m, ug, (eq_found, eq_URI)) =
 922
 923     let time1 = Unix.gettimeofday () in
 924
 925     let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
 926     let what, other = if pos = Utils.Left then what, other else other, what in
 927     let newgoal, newproof =
 928       let bo' = (* M. *)apply_subst s (S.subst other bo) in
 929       let t' =
 930         let name = C.Name ("x_SupR_" ^ (string_of_int !sup_r_counter)) in
 931         incr sup_r_counter;
 932         let l, r =
 933           if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
 934         (name, ty, S.lift 1 eq_ty, l, r)
 935       in
 936       let name = C.Name ("x_SupR_" ^ (string_of_int !sup_r_counter)) in
 937       incr sup_r_counter;
 938       let bo'' =
 939         let l, r =
 940           if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
 941         C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
 942                 S.lift 1 eq_ty; l; r]
 943       in
 944       bo',
 945       Inference.ProofBlock (
 946         s, eq_URI, (name, ty), bo''(* t' *), eq_found, eqproof)
 947     in
 948     let newmeta, newequality =
 949       let left, right =
 950         if ordering = U.Gt then newgoal, (* M. *)apply_subst s right
 951         else (* M. *)apply_subst s left, newgoal in
 952       let neworder = !Utils.compare_terms left right
 953       and newmenv = newmetas @ menv'
 954       and newargs = args @ args' in
 955 (*         let m = *)
 956 (*           (Inference.metas_of_term left) @ (Inference.metas_of_term right) in *)
 957 (*         let a =  *)
 958 (*           List.filter *)
 959 (*             (function C.Meta (i, _) -> List.mem i m | _ -> assert false) *)
 960 (*             (args @ args') *)
 961 (*         in *)
 962 (*         let delta = (List.length args) - (List.length a) in *)
 963 (*         if delta > 0 then *)
 964 (*           let first = List.hd a in *)
 965 (*           let rec aux l = function *)
 966 (*             | 0 -> l *)
 967 (*             | d -> let l = aux l (d-1) in l @ [first] *)
 968 (*           in *)
 969 (*           aux a delta *)
 970 (*         else *)
 971 (*           a *)
 972 (*       in *)
 973       let eq' =
 974         let w = Utils.compute_equality_weight eq_ty left right in
 975         (w, newproof, (eq_ty, left, right, neworder), newmenv, newargs)
 976       and env = (metasenv, context, ugraph) in
 977       let newm, eq' = Inference.fix_metas !maxmeta eq' in
 978       newm, eq'
 979     in
 980     maxmeta := newmeta;
 981
 982     let time2 = Unix.gettimeofday () in
 983     build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
 984
 985     newequality
 986   in
 987   let new1 = List.map (build_new U.Gt) res1
 988   and new2 = List.map (build_new U.Lt) res2 in
 989 (*   let ok = function *)
 990 (*     | _, _, (_, left, right, _), _, _ -> *)
 991 (*         not (fst (CR.are_convertible context left right ugraph)) *)
 992 (*   in *)
 993   let ok e = not (Inference.is_identity (metasenv, context, ugraph) e) in
 994   (!maxmeta,
 995    (List.filter ok (new1 @ new2)))
 996 ;;
 997
 998
 999 let rec demodulation_goal newmeta env table goal =
1000   let module C = Cic in
1001   let module S = CicSubstitution in
1002   let module M = CicMetaSubst in
1003   let module HL = HelmLibraryObjects in
1004   let metasenv, context, ugraph = env in
1005   let maxmeta = ref newmeta in
1006   let proof, metas, term = goal in
1007   let metasenv' = metasenv @ metas in
1008
1009   let build_newgoal (t, subst, menv, ug, (eq_found, eq_URI)) =
1010     let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
1011     let what, other = if pos = Utils.Left then what, other else other, what in
1012     let ty =
1013       try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
1014       with CicUtil.Meta_not_found _ -> ty
1015     in
1016     let newterm, newproof =
1017       let bo = (* M. *)apply_subst subst (S.subst other t) in
1018       let bo' = apply_subst subst t in
1019       let name = C.Name ("x_DemodGoal_" ^ (string_of_int !demod_counter)) in
1020       incr demod_counter;
1021       let metaproof =
1022         incr maxmeta;
1023         let irl =
1024           CicMkImplicit.identity_relocation_list_for_metavariable context in
1025         Printf.printf "\nADDING META: %d\n" !maxmeta;
1026         print_newline ();
1027         C.Meta (!maxmeta, irl)
1028       in
1029       let eq_found =
1030         let proof' =
1031 (*           let ens = *)
1032 (*             if pos = Utils.Left then build_ens_for_sym_eq ty what other *)
1033 (*             else build_ens_for_sym_eq ty other what *)
1034 (*           in *)
1035           let termlist =
1036             if pos = Utils.Left then [ty; what; other]
1037             else [ty; other; what]
1038           in
1039           Inference.ProofSymBlock (termlist, proof')
1040         in
1041         let what, other =
1042           if pos = Utils.Left then what, other else other, what
1043         in
1044         pos, (0, proof', (ty, other, what, Utils.Incomparable), menv', args')
1045       in
1046       let goal_proof =
1047         let pb =
1048           Inference.ProofBlock (subst, eq_URI, (name, ty), bo',
1049                                 eq_found, Inference.BasicProof metaproof)
1050         in
1051         let rec repl = function
1052           | Inference.NoProof ->
1053               debug_print (lazy "replacing a NoProof");
1054               pb
1055           | Inference.BasicProof _ ->
1056               debug_print (lazy "replacing a BasicProof");
1057               pb
1058           | Inference.ProofGoalBlock (_, parent_proof) ->
1059               debug_print (lazy "replacing another ProofGoalBlock");
1060               Inference.ProofGoalBlock (pb, parent_proof)
1061           | (Inference.SubProof (term, meta_index, p) as subproof) ->
1062               debug_print
1063                 (lazy
1064                    (Printf.sprintf "replacing %s"
1065                       (Inference.string_of_proof subproof)));
1066               Inference.SubProof (term, meta_index, repl p)
1067           | _ -> assert false
1068         in repl proof
1069       in
1070       bo, Inference.ProofGoalBlock (Inference.NoProof, goal_proof)
1071     in
1072     let m = Inference.metas_of_term newterm in
1073     let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) metas in
1074     !maxmeta, (newproof, newmetasenv, newterm)
1075   in
1076   let res = demodulation_aux metasenv' context ugraph table 0 term in
1077   match res with
1078   | Some t ->
1079       let newmeta, newgoal = build_newgoal t in
1080       let _, _, newg = newgoal in
1081       if Inference.meta_convertibility term newg then
1082         newmeta, newgoal
1083       else
1084         demodulation_goal newmeta env table newgoal
1085   | None ->
1086       newmeta, goal
1087 ;;
1088
1089
1090 let rec demodulation_theorem newmeta env table theorem =
1091   let module C = Cic in
1092   let module S = CicSubstitution in
1093   let module M = CicMetaSubst in
1094   let module HL = HelmLibraryObjects in
1095   let metasenv, context, ugraph = env in
1096   let maxmeta = ref newmeta in
1097   let proof, metas, term = theorem in
1098   let term, termty, metas = theorem in
1099   let metasenv' = metasenv @ metas in
1100
1101   let build_newtheorem (t, subst, menv, ug, (eq_found, eq_URI)) =
1102     let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
1103     let what, other = if pos = Utils.Left then what, other else other, what in
1104     let newterm, newty =
1105       let bo = apply_subst subst (S.subst other t) in
1106       let bo' = apply_subst subst t in
1107       let name = C.Name ("x_DemodThm_" ^ (string_of_int !demod_counter)) in
1108       incr demod_counter;
1109       let newproof =
1110         Inference.ProofBlock (subst, eq_URI, (name, ty), bo', eq_found,
1111                               Inference.BasicProof term)
1112       in
1113       (Inference.build_proof_term newproof, bo)
1114     in
1115     let m = Inference.metas_of_term newterm in
1116     let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) metas in
1117     !maxmeta, (newterm, newty, newmetasenv)
1118   in
1119   let res = demodulation_aux metasenv' context ugraph table 0 termty in
1120   match res with
1121   | Some t ->
1122       let newmeta, newthm = build_newtheorem t in
1123       let newt, newty, _ = newthm in
1124       if Inference.meta_convertibility termty newty then
1125         newmeta, newthm
1126       else
1127         demodulation_theorem newmeta env table newthm
1128   | None ->
1129       newmeta, theorem
1130 ;;