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