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