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