components/tactics/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 (* $Id$ *)
  27
  28 module Index = Equality_indexing.DT (* discrimination tree based indexing *)
  29 (*
  30 module Index = Equality_indexing.DT (* path tree based indexing *)
  31 *)
  32
  33 let beta_expand_time = ref 0.;;
  34
  35 let debug_print = Utils.debug_print;;
  36
  37 (*
  38 for debugging
  39 let check_equation env equation msg =
  40   let w, proof, (eq_ty, left, right, order), metas, args = equation in
  41   let metasenv, context, ugraph = env
  42   let metasenv' = metasenv @ metas in
  43     try
  44       CicTypeChecker.type_of_aux' metasenv' context left ugraph;
  45       CicTypeChecker.type_of_aux' metasenv' context right ugraph;
  46       ()
  47     with
  48         CicUtil.Meta_not_found _ as exn ->
  49           begin
  50             prerr_endline msg;
  51             prerr_endline (CicPp.ppterm left);
  52             prerr_endline (CicPp.ppterm right);
  53             raise exn
  54           end
  55 *)
  56
  57 type retrieval_mode = Matching | Unification;;
  58
  59 let string_of_res ?env =
  60   function
  61       None -> "None"
  62     | Some (t, s, m, u, ((p,e), eq_URI)) ->
  63         Printf.sprintf "Some: (%s, %s, %s)"
  64           (Utils.string_of_pos p)
  65           (Inference.string_of_equality ?env e)
  66           (CicPp.ppterm t)
  67 ;;
  68
  69 let print_res ?env res =
  70   prerr_endline
  71     (String.concat "\n"
  72        (List.map (string_of_res ?env) res))
  73 ;;
  74
  75 let print_candidates ?env mode term res =
  76   let _ =
  77     match mode with
  78     | Matching ->
  79         prerr_endline ("| candidates Matching " ^ (CicPp.ppterm term))
  80     | Unification ->
  81         prerr_endline ("| candidates Unification " ^ (CicPp.ppterm term))
  82   in
  83   prerr_endline
  84     (String.concat "\n"
  85        (List.map
  86           (fun (p, e) ->
  87              Printf.sprintf "| (%s, %s)" (Utils.string_of_pos p)
  88                (Inference.string_of_equality ?env e))
  89           res));
  90 ;;
  91
  92
  93 let indexing_retrieval_time = ref 0.;;
  94
  95
  96 let apply_subst = CicMetaSubst.apply_subst
  97
  98 let index = Index.index
  99 let remove_index = Index.remove_index
 100 let in_index = Index.in_index
 101 let empty = Index.empty
 102 let init_index = Index.init_index
 103
 104 let check_disjoint_invariant subst metasenv msg =
 105   if (List.exists
 106         (fun (i,_,_) -> (List.exists (fun (j,_) -> i=j) subst)) metasenv)
 107   then
 108     begin
 109       prerr_endline ("not disjoint: " ^ msg);
 110       assert false
 111     end
 112 ;;
 113
 114 let check_for_duplicates metas msg =
 115 let _ =
 116     try
 117       ignore(CicUtil.lookup_meta 190 metas);
 118       prerr_endline ("eccoci in " ^ msg);
 119     with
 120         CicUtil.Meta_not_found _ -> () in
 121 if List.length metas <>
 122   List.length (HExtlib.list_uniq (List.sort Pervasives.compare metas)) then
 123     begin
 124       prerr_endline ("DUPLICATI " ^ msg);
 125       prerr_endline (CicMetaSubst.ppmetasenv [] metas);
 126       assert false
 127     end
 128 ;;
 129
 130 let check_res res msg =
 131   match res with
 132       Some (t, subst, menv, ug, (eq_found, eq_URI)) ->
 133         let eqs = Inference.string_of_equality (snd eq_found) in
 134         check_disjoint_invariant subst menv msg;
 135         check_for_duplicates menv (msg ^ "\nchecking " ^ eqs);
 136     | None -> ()
 137 ;;
 138
 139 let check_target context target msg =
 140   let w, proof, (eq_ty, left, right, order), metas, args = target in
 141   (* check that metas does not contains duplicates *)
 142   let eqs = Inference.string_of_equality target in
 143   let _ = check_for_duplicates metas (msg ^ "\nchecking " ^ eqs) in
 144   let actual = (Inference.metas_of_term left)@(Inference.metas_of_term right)
 145     @(Inference.metas_of_term eq_ty)@(Inference.metas_of_proof proof) in
 146   let menv = List.filter (fun (i, _, _) -> List.mem i actual) metas in
 147   let _ = if menv <> metas then
 148     begin
 149       prerr_endline ("extra metas " ^ msg);
 150       prerr_endline (CicMetaSubst.ppmetasenv [] metas);
 151       prerr_endline "**********************";
 152       prerr_endline (CicMetaSubst.ppmetasenv [] menv);
 153       prerr_endline ("left: " ^ (CicPp.ppterm left));
 154       prerr_endline ("right: " ^ (CicPp.ppterm right));
 155       prerr_endline ("ty: " ^ (CicPp.ppterm eq_ty));
 156       assert false
 157     end
 158   else () in
 159   try
 160       CicTypeChecker.type_of_aux'
 161         metas context (Inference.build_proof_term proof) CicUniv.empty_ugraph
 162   with e ->
 163       prerr_endline msg;
 164       prerr_endline (Inference.string_of_proof proof);
 165       prerr_endline (CicPp.ppterm (Inference.build_proof_term proof));
 166       prerr_endline ("+++++++++++++left: " ^ (CicPp.ppterm left));
 167       prerr_endline ("+++++++++++++right: " ^ (CicPp.ppterm right));
 168       raise e
 169 ;;
 170
 171
 172 (* returns a list of all the equalities in the tree that are in relation
 173    "mode" with the given term, where mode can be either Matching or
 174    Unification.
 175
 176    Format of the return value: list of tuples in the form:
 177    (position - Left or Right - of the term that matched the given one in this
 178      equality,
 179     equality found)
 180
 181    Note that if equality is "left = right", if the ordering is left > right,
 182    the position will always be Left, and if the ordering is left < right,
 183    position will be Right.
 184 *)
 185 let local_max = ref 100;;
 186
 187 let make_variant (p,eq) =
 188   let maxmeta, eq = Inference.fix_metas !local_max eq in
 189   local_max := maxmeta;
 190   p, eq
 191 ;;
 192
 193 let get_candidates ?env mode tree term =
 194   let t1 = Unix.gettimeofday () in
 195   let res =
 196     let s =
 197       match mode with
 198       | Matching -> Index.retrieve_generalizations tree term
 199       | Unification -> Index.retrieve_unifiables tree term
 200     in
 201     Index.PosEqSet.elements s
 202   in
 203 (*   print_endline (Discrimination_tree.string_of_discrimination_tree tree); *)
 204 (*   print_newline (); *)
 205   let t2 = Unix.gettimeofday () in
 206   indexing_retrieval_time := !indexing_retrieval_time +. (t2 -. t1);
 207  (* make fresh instances *)
 208   res
 209 ;;
 210
 211
 212 let match_unif_time_ok = ref 0.;;
 213 let match_unif_time_no = ref 0.;;
 214
 215
 216 (*
 217   finds the first equality in the index that matches "term", of type "termty"
 218   termty can be Implicit if it is not needed. The result (one of the sides of
 219   the equality, actually) should be not greater (wrt the term ordering) than
 220   term
 221
 222   Format of the return value:
 223
 224   (term to substitute, [Cic.Rel 1 properly lifted - see the various
 225                         build_newtarget functions inside the various
 226                         demodulation_* functions]
 227    substitution used for the matching,
 228    metasenv,
 229    ugraph, [substitution, metasenv and ugraph have the same meaning as those
 230    returned by CicUnification.fo_unif]
 231    (equality where the matching term was found, [i.e. the equality to use as
 232                                                 rewrite rule]
 233     uri [either eq_ind_URI or eq_ind_r_URI, depending on the direction of
 234          the equality: this is used to build the proof term, again see one of
 235          the build_newtarget functions]
 236    ))
 237 *)
 238 let rec find_matches metasenv context ugraph lift_amount term termty =
 239   let module C = Cic in
 240   let module U = Utils in
 241   let module S = CicSubstitution in
 242   let module M = CicMetaSubst in
 243   let module HL = HelmLibraryObjects in
 244   let cmp = !Utils.compare_terms in
 245   let check = match termty with C.Implicit None -> false | _ -> true in
 246   function
 247     | [] -> None
 248     | candidate::tl ->
 249         let pos, (_, proof, (ty, left, right, o), metas, args) = candidate in
 250         if Utils.debug_metas then
 251           ignore(check_target context (snd candidate) "find_matches");
 252         if Utils.debug_res then
 253           begin
 254             let c = "eq = " ^ (Inference.string_of_equality (snd candidate)) ^ "\n"in
 255             let t = "t = " ^ (CicPp.ppterm term) ^ "\n" in
 256             let m = "metas = " ^ (CicMetaSubst.ppmetasenv [] metas) ^ "\n" in
 257             let p = "proof = " ^ (CicPp.ppterm (Inference.build_proof_term proof))  ^ "\n" in
 258               check_for_duplicates metas "gia nella metas";
 259               check_for_duplicates (metasenv @ metas) ("not disjoint" ^ c ^ t ^ m ^ p)
 260           end;
 261         if check && not (fst (CicReduction.are_convertible
 262                                 ~metasenv context termty ty ugraph)) then (
 263           find_matches metasenv context ugraph lift_amount term termty tl
 264         ) else
 265           let do_match c eq_URI =
 266             let subst', metasenv', ugraph' =
 267               let t1 = Unix.gettimeofday () in
 268               try
 269                 let r =
 270                   ( Inference.matching metasenv metas context
 271                     term (S.lift lift_amount c)) ugraph
 272                 in
 273                 let t2 = Unix.gettimeofday () in
 274                 match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
 275                 r
 276               with
 277                 | Inference.MatchingFailure as e ->
 278                 let t2 = Unix.gettimeofday () in
 279                 match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
 280                   raise e
 281                 | CicUtil.Meta_not_found _ as exn -> raise exn
 282             in
 283             Some (C.Rel (1 + lift_amount), subst', metasenv', ugraph',
 284                   (candidate, eq_URI))
 285           in
 286           let c, other, eq_URI =
 287             if pos = Utils.Left then left, right, Utils.eq_ind_URI ()
 288             else right, left, Utils.eq_ind_r_URI ()
 289           in
 290           if o <> U.Incomparable then
 291             let res =
 292               try
 293                 do_match c eq_URI
 294               with Inference.MatchingFailure ->
 295                 find_matches metasenv context ugraph lift_amount term termty tl
 296             in
 297               if Utils.debug_res then ignore (check_res res "find1");
 298               res
 299           else
 300             let res =
 301               try do_match c eq_URI
 302               with Inference.MatchingFailure -> None
 303             in
 304             if Utils.debug_res then ignore (check_res res "find2");
 305             match res with
 306             | Some (_, s, _, _, _) ->
 307                 let c' = apply_subst s c in
 308                 (*
 309              let other' = U.guarded_simpl context (apply_subst s other) in *)
 310                 let other' = apply_subst s other in
 311                 let order = cmp c' other' in
 312                 if order = U.Gt then
 313                   res
 314                 else
 315                   find_matches
 316                     metasenv context ugraph lift_amount term termty tl
 317             | None ->
 318                 find_matches metasenv context ugraph lift_amount term termty tl
 319 ;;
 320
 321
 322 (*
 323   as above, but finds all the matching equalities, and the matching condition
 324   can be either Inference.matching or Inference.unification
 325 *)
 326 let rec find_all_matches ?(unif_fun=Inference.unification)
 327     metasenv context ugraph lift_amount term termty =
 328   let module C = Cic in
 329   let module U = Utils in
 330   let module S = CicSubstitution in
 331   let module M = CicMetaSubst in
 332   let module HL = HelmLibraryObjects in
 333   let cmp = !Utils.compare_terms in
 334   function
 335     | [] -> []
 336     | candidate::tl ->
 337         let pos, (_, _, (ty, left, right, o), metas, args) = candidate in
 338         let do_match c eq_URI =
 339           let subst', metasenv', ugraph' =
 340             let t1 = Unix.gettimeofday () in
 341             try
 342               let r =
 343                 unif_fun metasenv metas context
 344                   term (S.lift lift_amount c) ugraph in
 345               let t2 = Unix.gettimeofday () in
 346               match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
 347               r
 348             with
 349             | Inference.MatchingFailure
 350             | CicUnification.UnificationFailure _
 351             | CicUnification.Uncertain _ as e ->
 352                 let t2 = Unix.gettimeofday () in
 353                 match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
 354                 raise e
 355           in
 356           (C.Rel (1 + lift_amount), subst', metasenv', ugraph',
 357            (candidate, eq_URI))
 358         in
 359         let c, other, eq_URI =
 360           if pos = Utils.Left then left, right, Utils.eq_ind_URI ()
 361           else right, left, Utils.eq_ind_r_URI ()
 362         in
 363         if o <> U.Incomparable then
 364           try
 365             let res = do_match c eq_URI in
 366             res::(find_all_matches ~unif_fun metasenv context ugraph
 367                     lift_amount term termty tl)
 368           with
 369           | Inference.MatchingFailure
 370           | CicUnification.UnificationFailure _
 371           | CicUnification.Uncertain _ ->
 372               find_all_matches ~unif_fun metasenv context ugraph
 373                 lift_amount term termty tl
 374         else
 375           try
 376             let res = do_match c eq_URI in
 377             match res with
 378             | _, s, _, _, _ ->
 379                 let c' = apply_subst s c
 380                 and other' = apply_subst s other in
 381                 let order = cmp c' other' in
 382                 if order <> U.Lt && order <> U.Le then
 383                   res::(find_all_matches ~unif_fun metasenv context ugraph
 384                           lift_amount term termty tl)
 385                 else
 386                   find_all_matches ~unif_fun metasenv context ugraph
 387                     lift_amount term termty tl
 388           with
 389           | Inference.MatchingFailure
 390           | CicUnification.UnificationFailure _
 391           | CicUnification.Uncertain _ ->
 392               find_all_matches ~unif_fun metasenv context ugraph
 393                 lift_amount term termty tl
 394 ;;
 395
 396
 397 (*
 398   returns true if target is subsumed by some equality in table
 399 *)
 400 let subsumption env table target =
 401   let _, _, (ty, left, right, _), tmetas, _ = target in
 402   let metasenv, context, ugraph = env in
 403   let metasenv = metasenv @ tmetas in
 404   let samesubst subst subst' =
 405     let tbl = Hashtbl.create (List.length subst) in
 406     List.iter (fun (m, (c, t1, t2)) -> Hashtbl.add tbl m (c, t1, t2)) subst;
 407     List.for_all
 408       (fun (m, (c, t1, t2)) ->
 409          try
 410            let c', t1', t2' = Hashtbl.find tbl m in
 411            if (c = c') && (t1 = t1') && (t2 = t2') then true
 412            else false
 413          with Not_found ->
 414            true)
 415       subst'
 416   in
 417   let leftr =
 418     match left with
 419     | Cic.Meta _ -> []
 420     | _ ->
 421         let leftc = get_candidates Matching table left in
 422         find_all_matches ~unif_fun:Inference.matching
 423           metasenv context ugraph 0 left ty leftc
 424   in
 425   let rec ok what = function
 426     | [] -> false, []
 427     | (_, subst, menv, ug, ((pos, (_, _, (_, l, r, o), m, _)), _))::tl ->
 428         try
 429           let other = if pos = Utils.Left then r else l in
 430           let subst', menv', ug' =
 431             let t1 = Unix.gettimeofday () in
 432             try
 433               let r =
 434                 Inference.matching menv m context what other ugraph
 435               in
 436               let t2 = Unix.gettimeofday () in
 437               match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
 438               r
 439             with Inference.MatchingFailure as e ->
 440               let t2 = Unix.gettimeofday () in
 441               match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
 442               raise e
 443           in
 444           if samesubst subst subst' then
 445             true, subst
 446           else
 447             ok what tl
 448         with Inference.MatchingFailure ->
 449           ok what tl
 450   in
 451   let r, subst = ok right leftr in
 452   let r, s =
 453     if r then
 454       true, subst
 455     else
 456       let rightr =
 457         match right with
 458           | Cic.Meta _ -> []
 459           | _ ->
 460               let rightc = get_candidates Matching table right in
 461                 find_all_matches ~unif_fun:Inference.matching
 462                   metasenv context ugraph 0 right ty rightc
 463       in
 464         ok left rightr
 465   in
 466 (*     (if r then  *)
 467 (*        debug_print  *)
 468 (*       (lazy *)
 469 (*          (Printf.sprintf "SUBSUMPTION! %s\n%s\n" *)
 470 (*             (Inference.string_of_equality target) (Utils.print_subst s)))); *)
 471     r, s
 472 ;;
 473
 474 let rec demodulation_aux ?from ?(typecheck=false)
 475   metasenv context ugraph table lift_amount term =
 476   (* Printf.eprintf "term = %s\n" (CicPp.ppterm term); *)
 477   let module C = Cic in
 478   let module S = CicSubstitution in
 479   let module M = CicMetaSubst in
 480   let module HL = HelmLibraryObjects in
 481   let candidates =
 482     get_candidates ~env:(metasenv,context,ugraph) Matching table term in
 483 (*   let candidates = List.map make_variant candidates in *)
 484   let res =
 485     match term with
 486       | C.Meta _ -> None
 487       | term ->
 488           let termty, ugraph =
 489             if typecheck then
 490               CicTypeChecker.type_of_aux' metasenv context term ugraph
 491             else
 492               C.Implicit None, ugraph
 493           in
 494           let res =
 495             find_matches metasenv context ugraph lift_amount term termty candidates
 496           in
 497           if Utils.debug_res then ignore(check_res res "demod1");
 498             if res <> None then
 499               res
 500             else
 501               match term with
 502                 | C.Appl l ->
 503                     let res, ll =
 504                       List.fold_left
 505                         (fun (res, tl) t ->
 506                            if res <> None then
 507                              (res, tl @ [S.lift 1 t])
 508                            else
 509                              let r =
 510                                demodulation_aux ~from:"1" metasenv context ugraph table
 511                                  lift_amount t
 512                              in
 513                                match r with
 514                                  | None -> (None, tl @ [S.lift 1 t])
 515                                  | Some (rel, _, _, _, _) -> (r, tl @ [rel]))
 516                         (None, []) l
 517                     in (
 518                         match res with
 519                           | None -> None
 520                           | Some (_, subst, menv, ug, eq_found) ->
 521                               Some (C.Appl ll, subst, menv, ug, eq_found)
 522                       )
 523                 | C.Prod (nn, s, t) ->
 524                     let r1 =
 525                       demodulation_aux ~from:"2"
 526                         metasenv context ugraph table lift_amount s in (
 527                         match r1 with
 528                           | None ->
 529                               let r2 =
 530                                 demodulation_aux metasenv
 531                                   ((Some (nn, C.Decl s))::context) ugraph
 532                                   table (lift_amount+1) t
 533                               in (
 534                                   match r2 with
 535                                     | None -> None
 536                                     | Some (t', subst, menv, ug, eq_found) ->
 537                                         Some (C.Prod (nn, (S.lift 1 s), t'),
 538                                               subst, menv, ug, eq_found)
 539                                 )
 540                           | Some (s', subst, menv, ug, eq_found) ->
 541                               Some (C.Prod (nn, s', (S.lift 1 t)),
 542                                     subst, menv, ug, eq_found)
 543                       )
 544                 | C.Lambda (nn, s, t) ->
 545                     let r1 =
 546                       demodulation_aux
 547                         metasenv context ugraph table lift_amount s in (
 548                         match r1 with
 549                           | None ->
 550                               let r2 =
 551                                 demodulation_aux metasenv
 552                                   ((Some (nn, C.Decl s))::context) ugraph
 553                                   table (lift_amount+1) t
 554                               in (
 555                                   match r2 with
 556                                     | None -> None
 557                                     | Some (t', subst, menv, ug, eq_found) ->
 558                                         Some (C.Lambda (nn, (S.lift 1 s), t'),
 559                                               subst, menv, ug, eq_found)
 560                                 )
 561                           | Some (s', subst, menv, ug, eq_found) ->
 562                               Some (C.Lambda (nn, s', (S.lift 1 t)),
 563                                     subst, menv, ug, eq_found)
 564                       )
 565                 | t ->
 566                     None
 567   in
 568   if Utils.debug_res then ignore(check_res res "demod_aux output");
 569   res
 570 ;;
 571
 572
 573 let build_newtarget_time = ref 0.;;
 574
 575
 576 let demod_counter = ref 1;;
 577
 578 exception Foo
 579
 580 (** demodulation, when target is an equality *)
 581 let rec demodulation_equality ?from newmeta env table sign target =
 582   let module C = Cic in
 583   let module S = CicSubstitution in
 584   let module M = CicMetaSubst in
 585   let module HL = HelmLibraryObjects in
 586   let module U = Utils in
 587   let metasenv, context, ugraph = env in
 588   let w, proof, (eq_ty, left, right, order), metas, args = target in
 589   (* first, we simplify *)
 590   let right = U.guarded_simpl context right in
 591   let left = U.guarded_simpl context left in
 592   let w = Utils.compute_equality_weight eq_ty left right in
 593   let order = !Utils.compare_terms left right in
 594   let target = w, proof, (eq_ty, left, right, order), metas, args in
 595   if Utils.debug_metas then
 596     ignore(check_target context target "demod equalities input");
 597   let metasenv' = (* metasenv @ *) metas in
 598   let maxmeta = ref newmeta in
 599
 600   let build_newtarget is_left (t, subst, menv, ug, (eq_found, eq_URI)) =
 601     let time1 = Unix.gettimeofday () in
 602
 603     if Utils.debug_metas then
 604       begin
 605         ignore(check_for_duplicates menv "input1");
 606         ignore(check_disjoint_invariant subst menv "input2");
 607         let substs = CicMetaSubst.ppsubst subst in
 608         ignore(check_target context (snd eq_found) ("input3" ^ substs))
 609       end;
 610     let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
 611     let ty =
 612     try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
 613       with CicUtil.Meta_not_found _ -> ty
 614     in
 615     let what, other = if pos = Utils.Left then what, other else other, what in
 616     let newterm, newproof =
 617       let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
 618       let name = C.Name ("x_Demod" ^ (string_of_int !demod_counter)) in
 619       incr demod_counter;
 620       let bo' =
 621         let l, r = if is_left then t, S.lift 1 right else S.lift 1 left, t in
 622           C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
 623                   S.lift 1 eq_ty; l; r]
 624       in
 625       if sign = Utils.Positive then
 626           (bo,
 627            Inference.ProofBlock (
 628              subst, eq_URI, (name, ty), bo'(* t' *), eq_found, proof))
 629       else
 630         let metaproof =
 631           incr maxmeta;
 632           let irl =
 633             CicMkImplicit.identity_relocation_list_for_metavariable context in
 634 (*           debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta)); *)
 635 (*           print_newline (); *)
 636           C.Meta (!maxmeta, irl)
 637         in
 638           let eq_found =
 639             let proof' =
 640               let termlist =
 641                 if pos = Utils.Left then [ty; what; other]
 642                 else [ty; other; what]
 643               in
 644               Inference.ProofSymBlock (termlist, proof')
 645             in
 646             let what, other =
 647               if pos = Utils.Left then what, other else other, what
 648             in
 649             pos, (0, proof', (ty, other, what, Utils.Incomparable),
 650                   menv', args')
 651           in
 652           let target_proof =
 653             let pb =
 654               Inference.ProofBlock (subst, eq_URI, (name, ty), bo',
 655                                     eq_found, Inference.BasicProof metaproof)
 656             in
 657             match proof with
 658             | Inference.BasicProof _ ->
 659                 (* print_endline "replacing a BasicProof"; *)
 660                 pb
 661             | Inference.ProofGoalBlock (_, parent_proof) ->
 662
 663   (* print_endline "replacing another ProofGoalBlock"; *)
 664                 Inference.ProofGoalBlock (pb, parent_proof)
 665             | _ -> assert false
 666           in
 667         let refl =
 668           C.Appl [C.MutConstruct (* reflexivity *)
 669                     (LibraryObjects.eq_URI (), 0, 1, []);
 670                   eq_ty; if is_left then right else left]
 671         in
 672         (bo,
 673          Inference.ProofGoalBlock (Inference.BasicProof refl, target_proof))
 674     in
 675     let newmenv = (* Inference.filter subst *) menv in
 676     let _ =
 677       if Utils.debug_metas then
 678         try ignore(CicTypeChecker.type_of_aux'
 679           newmenv context (Inference.build_proof_term newproof) ugraph);
 680           ()
 681         with exc ->
 682           prerr_endline "sempre lui";
 683           prerr_endline (CicMetaSubst.ppsubst subst);
 684           prerr_endline (CicPp.ppterm (Inference.build_proof_term newproof));
 685           prerr_endline ("+++++++++++++termine: " ^ (CicPp.ppterm t));
 686           prerr_endline ("+++++++++++++what: " ^ (CicPp.ppterm what));
 687           prerr_endline ("+++++++++++++other: " ^ (CicPp.ppterm other));
 688           prerr_endline ("+++++++++++++subst: " ^ (CicMetaSubst.ppsubst subst));
 689           raise exc;
 690       else ()
 691     in
 692     let left, right = if is_left then newterm, right else left, newterm in
 693     let ordering = !Utils.compare_terms left right in
 694     let time2 = Unix.gettimeofday () in
 695     build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
 696     let res =
 697       let w = Utils.compute_equality_weight eq_ty left right in
 698       (w, newproof, (eq_ty, left, right, ordering),newmenv,args) in
 699     if Utils.debug_metas then
 700       ignore(check_target context res "buildnew_target output");
 701     !maxmeta, res
 702   in
 703
 704   let res = demodulation_aux ~from:"3" metasenv' context ugraph table 0 left in
 705   if Utils.debug_res then check_res res "demod result";
 706   let newmeta, newtarget =
 707     match res with
 708     | Some t ->
 709         let newmeta, newtarget = build_newtarget true t in
 710           if (Inference.is_weak_identity (metasenv', context, ugraph) newtarget) ||
 711             (Inference.meta_convertibility_eq target newtarget) then
 712               newmeta, newtarget
 713           else
 714             demodulation_equality newmeta env table sign newtarget
 715     | None ->
 716         let res = demodulation_aux metasenv' context ugraph table 0 right in
 717         if Utils.debug_res then check_res res "demod result 1";
 718           match res with
 719           | Some t ->
 720               let newmeta, newtarget = build_newtarget false t in
 721                 if (Inference.is_weak_identity (metasenv', context, ugraph) newtarget) ||
 722                   (Inference.meta_convertibility_eq target newtarget) then
 723                     newmeta, newtarget
 724                 else
 725                    demodulation_equality newmeta env table sign newtarget
 726           | None ->
 727               newmeta, target
 728   in
 729   (* newmeta, newtarget *)
 730   newmeta,newtarget
 731 ;;
 732
 733
 734 (**
 735    Performs the beta expansion of the term "term" w.r.t. "table",
 736    i.e. returns the list of all the terms t s.t. "(t term) = t2", for some t2
 737    in table.
 738 *)
 739 let rec betaexpand_term metasenv context ugraph table lift_amount term =
 740   let module C = Cic in
 741   let module S = CicSubstitution in
 742   let module M = CicMetaSubst in
 743   let module HL = HelmLibraryObjects in
 744   let candidates = get_candidates Unification table term in
 745
 746   let res, lifted_term =
 747     match term with
 748     | C.Meta (i, l) ->
 749         let l', lifted_l =
 750           List.fold_right
 751             (fun arg (res, lifted_tl) ->
 752                match arg with
 753                | Some arg ->
 754                    let arg_res, lifted_arg =
 755                      betaexpand_term metasenv context ugraph table
 756                        lift_amount arg in
 757                    let l1 =
 758                      List.map
 759                        (fun (t, s, m, ug, eq_found) ->
 760                           (Some t)::lifted_tl, s, m, ug, eq_found)
 761                        arg_res
 762                    in
 763                    (l1 @
 764                       (List.map
 765                          (fun (l, s, m, ug, eq_found) ->
 766                             (Some lifted_arg)::l, s, m, ug, eq_found)
 767                          res),
 768                     (Some lifted_arg)::lifted_tl)
 769                | None ->
 770                    (List.map
 771                       (fun (r, s, m, ug, eq_found) ->
 772                          None::r, s, m, ug, eq_found) res,
 773                     None::lifted_tl)
 774             ) l ([], [])
 775         in
 776         let e =
 777           List.map
 778             (fun (l, s, m, ug, eq_found) ->
 779                (C.Meta (i, l), s, m, ug, eq_found)) l'
 780         in
 781         e, C.Meta (i, lifted_l)
 782
 783     | C.Rel m ->
 784         [], if m <= lift_amount then C.Rel m else C.Rel (m+1)
 785
 786     | C.Prod (nn, s, t) ->
 787         let l1, lifted_s =
 788           betaexpand_term metasenv context ugraph table lift_amount s in
 789         let l2, lifted_t =
 790           betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
 791             table (lift_amount+1) t in
 792         let l1' =
 793           List.map
 794             (fun (t, s, m, ug, eq_found) ->
 795                C.Prod (nn, t, lifted_t), s, m, ug, eq_found) l1
 796         and l2' =
 797           List.map
 798             (fun (t, s, m, ug, eq_found) ->
 799                C.Prod (nn, lifted_s, t), s, m, ug, eq_found) l2 in
 800         l1' @ l2', C.Prod (nn, lifted_s, lifted_t)
 801
 802     | C.Lambda (nn, s, t) ->
 803         let l1, lifted_s =
 804           betaexpand_term metasenv context ugraph table lift_amount s in
 805         let l2, lifted_t =
 806           betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
 807             table (lift_amount+1) t in
 808         let l1' =
 809           List.map
 810             (fun (t, s, m, ug, eq_found) ->
 811                C.Lambda (nn, t, lifted_t), s, m, ug, eq_found) l1
 812         and l2' =
 813           List.map
 814             (fun (t, s, m, ug, eq_found) ->
 815                C.Lambda (nn, lifted_s, t), s, m, ug, eq_found) l2 in
 816         l1' @ l2', C.Lambda (nn, lifted_s, lifted_t)
 817
 818     | C.Appl l ->
 819         let l', lifted_l =
 820           List.fold_right
 821             (fun arg (res, lifted_tl) ->
 822                let arg_res, lifted_arg =
 823                  betaexpand_term metasenv context ugraph table lift_amount arg
 824                in
 825                let l1 =
 826                  List.map
 827                    (fun (a, s, m, ug, eq_found) ->
 828                       a::lifted_tl, s, m, ug, eq_found)
 829                    arg_res
 830                in
 831                (l1 @
 832                   (List.map
 833                      (fun (r, s, m, ug, eq_found) ->
 834                         lifted_arg::r, s, m, ug, eq_found)
 835                      res),
 836                 lifted_arg::lifted_tl)
 837             ) l ([], [])
 838         in
 839         (List.map
 840            (fun (l, s, m, ug, eq_found) -> (C.Appl l, s, m, ug, eq_found)) l',
 841          C.Appl lifted_l)
 842
 843     | t -> [], (S.lift lift_amount t)
 844   in
 845   match term with
 846   | C.Meta (i, l) -> res, lifted_term
 847   | term ->
 848       let termty, ugraph =
 849         C.Implicit None, ugraph
 850 (*         CicTypeChecker.type_of_aux' metasenv context term ugraph *)
 851       in
 852       let r =
 853         find_all_matches
 854           metasenv context ugraph lift_amount term termty candidates
 855       in
 856       r @ res, lifted_term
 857 ;;
 858
 859
 860 let sup_l_counter = ref 1;;
 861
 862 (**
 863    superposition_left
 864    returns a list of new clauses inferred with a left superposition step
 865    the negative equation "target" and one of the positive equations in "table"
 866 *)
 867 let superposition_left newmeta (metasenv, context, ugraph) table target =
 868   let module C = Cic in
 869   let module S = CicSubstitution in
 870   let module M = CicMetaSubst in
 871   let module HL = HelmLibraryObjects in
 872   let module CR = CicReduction in
 873   let module U = Utils in
 874   let weight, proof, (eq_ty, left, right, ordering), menv, _ = target in
 875   if Utils.debug_metas then
 876     ignore(check_target context target "superpositionleft");
 877   let expansions, _ =
 878     let term = if ordering = U.Gt then left else right in
 879       begin
 880         let t1 = Unix.gettimeofday () in
 881         let res = betaexpand_term metasenv context ugraph table 0 term in
 882         let t2 = Unix.gettimeofday () in
 883           beta_expand_time := !beta_expand_time  +. (t2 -. t1);
 884         res
 885       end
 886   in
 887   let maxmeta = ref newmeta in
 888   let build_new (bo, s, m, ug, (eq_found, eq_URI)) =
 889 (*     debug_print (lazy "\nSUPERPOSITION LEFT\n"); *)
 890     let time1 = Unix.gettimeofday () in
 891
 892     let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
 893     let what, other = if pos = Utils.Left then what, other else other, what in
 894     let newgoal, newproof =
 895       let bo' =  U.guarded_simpl context (apply_subst s (S.subst other bo)) in
 896       let name = C.Name ("x_SupL_" ^ (string_of_int !sup_l_counter)) in
 897       incr sup_l_counter;
 898       let bo'' =
 899         let l, r =
 900           if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
 901         C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
 902                 S.lift 1 eq_ty; l; r]
 903       in
 904       incr maxmeta;
 905       let metaproof =
 906         let irl =
 907           CicMkImplicit.identity_relocation_list_for_metavariable context in
 908         C.Meta (!maxmeta, irl)
 909       in
 910       let eq_found =
 911         let proof' =
 912           let termlist =
 913             if pos = Utils.Left then [ty; what; other]
 914             else [ty; other; what]
 915           in
 916           Inference.ProofSymBlock (termlist, proof')
 917         in
 918         let what, other =
 919           if pos = Utils.Left then what, other else other, what
 920         in
 921         pos, (0, proof', (ty, other, what, Utils.Incomparable), menv', args')
 922       in
 923       let target_proof =
 924         let pb =
 925           Inference.ProofBlock (s, eq_URI, (name, ty), bo'', eq_found,
 926                                 Inference.BasicProof metaproof)
 927         in
 928         match proof with
 929         | Inference.BasicProof _ ->
 930 (*             debug_print (lazy "replacing a BasicProof"); *)
 931             pb
 932         | Inference.ProofGoalBlock (_, parent_proof) ->
 933 (*             debug_print (lazy "replacing another ProofGoalBlock"); *)
 934             Inference.ProofGoalBlock (pb, parent_proof)
 935         | _ -> assert false
 936       in
 937       let refl =
 938         C.Appl [C.MutConstruct (* reflexivity *)
 939                   (LibraryObjects.eq_URI (), 0, 1, []);
 940                 eq_ty; if ordering = U.Gt then right else left]
 941       in
 942       (bo',
 943        Inference.ProofGoalBlock (Inference.BasicProof refl, target_proof))
 944     in
 945     let left, right =
 946       if ordering = U.Gt then newgoal, right else left, newgoal in
 947     let neworder = !Utils.compare_terms left right in
 948     let newmenv = (* Inference.filter s *) menv in
 949     let time2 = Unix.gettimeofday () in
 950     build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
 951
 952     let w = Utils.compute_equality_weight eq_ty left right in
 953     (w, newproof, (eq_ty, left, right, neworder), newmenv, [])
 954
 955   in
 956   !maxmeta, List.map build_new expansions
 957 ;;
 958
 959
 960 let sup_r_counter = ref 1;;
 961
 962 (**
 963    superposition_right
 964    returns a list of new clauses inferred with a right superposition step
 965    between the positive equation "target" and one in the "table" "newmeta" is
 966    the first free meta index, i.e. the first number above the highest meta
 967    index: its updated value is also returned
 968 *)
 969 let superposition_right newmeta (metasenv, context, ugraph) table target =
 970   let module C = Cic in
 971   let module S = CicSubstitution in
 972   let module M = CicMetaSubst in
 973   let module HL = HelmLibraryObjects in
 974   let module CR = CicReduction in
 975   let module U = Utils in
 976   let w, eqproof, (eq_ty, left, right, ordering), newmetas, args = target in
 977   if Utils.debug_metas then
 978     ignore (check_target context target "superpositionright");
 979   let metasenv' = newmetas in
 980   let maxmeta = ref newmeta in
 981   let res1, res2 =
 982     let betaexpand_term metasenv context ugraph table d term =
 983       let t1 = Unix.gettimeofday () in
 984       let res = betaexpand_term metasenv context ugraph table d term in
 985       let t2 = Unix.gettimeofday () in
 986         beta_expand_time := !beta_expand_time  +. (t2 -. t1);
 987         res
 988     in
 989     match ordering with
 990     | U.Gt -> fst (betaexpand_term metasenv' context ugraph table 0 left), []
 991     | U.Lt -> [], fst (betaexpand_term metasenv' context ugraph table 0 right)
 992     | _ ->
 993         let res l r =
 994           List.filter
 995             (fun (_, subst, _, _, _) ->
 996                let subst = apply_subst subst in
 997                let o = !Utils.compare_terms (subst l) (subst r) in
 998                o <> U.Lt && o <> U.Le)
 999             (fst (betaexpand_term metasenv' context ugraph table 0 l))
1000         in
1001         (res left right), (res right left)
1002   in
1003   let build_new ordering ((bo, s, m, ug, (eq_found, eq_URI)) as input) =
1004     if Utils.debug_metas then
1005       ignore (check_target context (snd eq_found) "buildnew1" );
1006     let time1 = Unix.gettimeofday () in
1007
1008     let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
1009     let what, other = if pos = Utils.Left then what, other else other, what in
1010     let newgoal, newproof =
1011       (* qua *)
1012       let bo' = Utils.guarded_simpl context (apply_subst s (S.subst other bo)) in
1013       let name = C.Name ("x_SupR_" ^ (string_of_int !sup_r_counter)) in
1014       incr sup_r_counter;
1015       let bo'' =
1016         let l, r =
1017           if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
1018         C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
1019                 S.lift 1 eq_ty; l; r]
1020       in
1021       bo',
1022       Inference.ProofBlock (s, eq_URI, (name, ty), bo'', eq_found, eqproof)
1023     in
1024     let newmeta, newequality =
1025       let left, right =
1026         if ordering = U.Gt then newgoal, apply_subst s right
1027         else apply_subst s left, newgoal in
1028       let neworder = !Utils.compare_terms left right in
1029       let newmenv = (* Inference.filter s *) m in
1030       let newargs = args @ args' in
1031       let eq' =
1032         let w = Utils.compute_equality_weight eq_ty left right in
1033         (w, newproof, (eq_ty, left, right, neworder), newmenv, newargs) in
1034       if Utils.debug_metas then
1035         ignore (check_target context eq' "buildnew3");
1036       let newm, eq' = Inference.fix_metas !maxmeta eq' in
1037       if Utils.debug_metas then
1038         ignore (check_target context eq' "buildnew4");
1039       newm, eq'
1040     in
1041     maxmeta := newmeta;
1042     let time2 = Unix.gettimeofday () in
1043     build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
1044     if Utils.debug_metas then
1045       ignore(check_target context newequality "buildnew2");
1046     newequality
1047   in
1048   let new1 = List.map (build_new U.Gt) res1
1049   and new2 = List.map (build_new U.Lt) res2 in
1050   let ok e = not (Inference.is_identity (metasenv', context, ugraph) e) in
1051   (!maxmeta,
1052    (List.filter ok (new1 @ new2)))
1053 ;;
1054
1055
1056 (** demodulation, when the target is a goal *)
1057 let rec demodulation_goal newmeta env table goal =
1058   let module C = Cic in
1059   let module S = CicSubstitution in
1060   let module M = CicMetaSubst in
1061   let module HL = HelmLibraryObjects in
1062   let metasenv, context, ugraph = env in
1063   let maxmeta = ref newmeta in
1064   let proof, metas, term = goal in
1065   let term = Utils.guarded_simpl (~debug:true) context term in
1066   let goal = proof, metas, term in
1067   let metasenv' = metas in
1068
1069   let build_newgoal (t, subst, menv, ug, (eq_found, eq_URI)) =
1070     let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
1071     let what, other = if pos = Utils.Left then what, other else other, what in
1072     let ty =
1073       try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
1074       with CicUtil.Meta_not_found _ -> ty
1075     in
1076     let newterm, newproof =
1077       let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
1078       let bo' = apply_subst subst t in
1079       let name = C.Name ("x_DemodGoal_" ^ (string_of_int !demod_counter)) in
1080       incr demod_counter;
1081       let metaproof =
1082         incr maxmeta;
1083         let irl =
1084           CicMkImplicit.identity_relocation_list_for_metavariable context in
1085 (*         debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta)); *)
1086         C.Meta (!maxmeta, irl)
1087       in
1088       let eq_found =
1089         let proof' =
1090           let termlist =
1091             if pos = Utils.Left then [ty; what; other]
1092             else [ty; other; what]
1093           in
1094           Inference.ProofSymBlock (termlist, proof')
1095         in
1096         let what, other =
1097           if pos = Utils.Left then what, other else other, what
1098         in
1099         pos, (0, proof', (ty, other, what, Utils.Incomparable), menv', args')
1100       in
1101       let goal_proof =
1102         let pb =
1103           Inference.ProofBlock (subst, eq_URI, (name, ty), bo',
1104                                 eq_found, Inference.BasicProof metaproof)
1105         in
1106         let rec repl = function
1107           | Inference.NoProof ->
1108 (*               debug_print (lazy "replacing a NoProof"); *)
1109               pb
1110           | Inference.BasicProof _ ->
1111 (*               debug_print (lazy "replacing a BasicProof"); *)
1112               pb
1113           | Inference.ProofGoalBlock (_, parent_proof) ->
1114 (*               debug_print (lazy "replacing another ProofGoalBlock"); *)
1115               Inference.ProofGoalBlock (pb, parent_proof)
1116           | Inference.SubProof (term, meta_index, p)  ->
1117               Inference.SubProof (term, meta_index, repl p)
1118           | _ -> assert false
1119         in repl proof
1120       in
1121       bo, Inference.ProofGoalBlock (Inference.NoProof, goal_proof)
1122     in
1123     let newmetasenv = (* Inference.filter subst *) menv in
1124     !maxmeta, (newproof, newmetasenv, newterm)
1125   in
1126   let res =
1127     demodulation_aux (* ~typecheck:true *) metasenv' context ugraph table 0 term
1128   in
1129   match res with
1130   | Some t ->
1131       let newmeta, newgoal = build_newgoal t in
1132       let _, _, newg = newgoal in
1133       if Inference.meta_convertibility term newg then
1134         newmeta, newgoal
1135       else
1136         demodulation_goal newmeta env table newgoal
1137   | None ->
1138       newmeta, goal
1139 ;;
1140
1141
1142 (** demodulation, when the target is a theorem *)
1143 let rec demodulation_theorem newmeta env table theorem =
1144   let module C = Cic in
1145   let module S = CicSubstitution in
1146   let module M = CicMetaSubst in
1147   let module HL = HelmLibraryObjects in
1148   let metasenv, context, ugraph = env in
1149   let maxmeta = ref newmeta in
1150   let term, termty, metas = theorem in
1151   let metasenv' = metas in
1152
1153   let build_newtheorem (t, subst, menv, ug, (eq_found, eq_URI)) =
1154     let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
1155     let what, other = if pos = Utils.Left then what, other else other, what in
1156     let newterm, newty =
1157       let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
1158       let bo' = apply_subst subst t in
1159       let name = C.Name ("x_DemodThm_" ^ (string_of_int !demod_counter)) in
1160       incr demod_counter;
1161       let newproof =
1162         Inference.ProofBlock (subst, eq_URI, (name, ty), bo', eq_found,
1163                               Inference.BasicProof term)
1164       in
1165       (Inference.build_proof_term newproof, bo)
1166     in
1167
1168     let m = Inference.metas_of_term newterm in
1169     !maxmeta, (newterm, newty, menv)
1170   in
1171   let res =
1172     demodulation_aux (* ~typecheck:true *) metasenv' context ugraph table 0 termty
1173   in
1174   match res with
1175   | Some t ->
1176       let newmeta, newthm = build_newtheorem t in
1177       let newt, newty, _ = newthm in
1178       if Inference.meta_convertibility termty newty then
1179         newmeta, newthm
1180       else
1181         demodulation_theorem newmeta env table newthm
1182   | None ->
1183       newmeta, theorem
1184 ;;
1185