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