helm/software/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 order = !Utils.compare_terms left right in
 593   let stat = (eq_ty, left, right, order) in
 594   let w = Utils.compute_equality_weight stat in
 595   let target = w, proof, stat, metas, args in
 596   if Utils.debug_metas then
 597     ignore(check_target context target "demod equalities input");
 598   let metasenv' = (* metasenv @ *) metas in
 599   let maxmeta = ref newmeta in
 600
 601   let build_newtarget is_left (t, subst, menv, ug, (eq_found, eq_URI)) =
 602     let time1 = Unix.gettimeofday () in
 603
 604     if Utils.debug_metas then
 605       begin
 606         ignore(check_for_duplicates menv "input1");
 607         ignore(check_disjoint_invariant subst menv "input2");
 608         let substs = CicMetaSubst.ppsubst subst in
 609         ignore(check_target context (snd eq_found) ("input3" ^ substs))
 610       end;
 611     let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
 612     let ty =
 613     try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
 614       with CicUtil.Meta_not_found _ -> ty
 615     in
 616     let what, other = if pos = Utils.Left then what, other else other, what in
 617     let newterm, newproof =
 618       let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
 619       let name = C.Name ("x_Demod" ^ (string_of_int !demod_counter)) in
 620       incr demod_counter;
 621       let bo' =
 622         let l, r = if is_left then t, S.lift 1 right else S.lift 1 left, t in
 623           C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
 624                   S.lift 1 eq_ty; l; r]
 625       in
 626       if sign = Utils.Positive then
 627           (bo,
 628            Inference.ProofBlock (
 629              subst, eq_URI, (name, ty), bo'(* t' *), eq_found, proof))
 630       else
 631         let metaproof =
 632           incr maxmeta;
 633           let irl =
 634             CicMkImplicit.identity_relocation_list_for_metavariable context in
 635 (*           debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta)); *)
 636 (*           print_newline (); *)
 637           C.Meta (!maxmeta, irl)
 638         in
 639           let eq_found =
 640             let proof' =
 641               let termlist =
 642                 if pos = Utils.Left then [ty; what; other]
 643                 else [ty; other; what]
 644               in
 645               Inference.ProofSymBlock (termlist, proof')
 646             in
 647             let what, other =
 648               if pos = Utils.Left then what, other else other, what
 649             in
 650             pos, (0, proof', (ty, other, what, Utils.Incomparable),
 651                   menv', args')
 652           in
 653           let target_proof =
 654             let pb =
 655               Inference.ProofBlock (subst, eq_URI, (name, ty), bo',
 656                                     eq_found, Inference.BasicProof metaproof)
 657             in
 658             match proof with
 659             | Inference.BasicProof _ ->
 660                 (* print_endline "replacing a BasicProof"; *)
 661                 pb
 662             | Inference.ProofGoalBlock (_, parent_proof) ->
 663
 664   (* print_endline "replacing another ProofGoalBlock"; *)
 665                 Inference.ProofGoalBlock (pb, parent_proof)
 666             | _ -> assert false
 667           in
 668         let refl =
 669           C.Appl [C.MutConstruct (* reflexivity *)
 670                     (LibraryObjects.eq_URI (), 0, 1, []);
 671                   eq_ty; if is_left then right else left]
 672         in
 673         (bo,
 674          Inference.ProofGoalBlock (Inference.BasicProof refl, target_proof))
 675     in
 676     let newmenv = (* Inference.filter subst *) menv in
 677     let _ =
 678       if Utils.debug_metas then
 679         try ignore(CicTypeChecker.type_of_aux'
 680           newmenv context (Inference.build_proof_term newproof) ugraph);
 681           ()
 682         with exc ->
 683           prerr_endline "sempre lui";
 684           prerr_endline (CicMetaSubst.ppsubst subst);
 685           prerr_endline (CicPp.ppterm (Inference.build_proof_term newproof));
 686           prerr_endline ("+++++++++++++termine: " ^ (CicPp.ppterm t));
 687           prerr_endline ("+++++++++++++what: " ^ (CicPp.ppterm what));
 688           prerr_endline ("+++++++++++++other: " ^ (CicPp.ppterm other));
 689           prerr_endline ("+++++++++++++subst: " ^ (CicMetaSubst.ppsubst subst));
 690           raise exc;
 691       else ()
 692     in
 693     let left, right = if is_left then newterm, right else left, newterm in
 694     let ordering = !Utils.compare_terms left right in
 695     let stat = (eq_ty, left, right, ordering) in
 696     let time2 = Unix.gettimeofday () in
 697     build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
 698     let res =
 699       let w = Utils.compute_equality_weight stat in
 700       (w, newproof, stat,newmenv,args) in
 701     if Utils.debug_metas then
 702       ignore(check_target context res "buildnew_target output");
 703     !maxmeta, res
 704   in
 705
 706   let res = demodulation_aux ~from:"3" metasenv' context ugraph table 0 left in
 707   if Utils.debug_res then check_res res "demod result";
 708   let newmeta, newtarget =
 709     match res with
 710     | Some t ->
 711         let newmeta, newtarget = build_newtarget true t in
 712           if (Inference.is_weak_identity (metasenv', context, ugraph) newtarget) ||
 713             (Inference.meta_convertibility_eq target newtarget) then
 714               newmeta, newtarget
 715           else
 716             demodulation_equality newmeta env table sign newtarget
 717     | None ->
 718         let res = demodulation_aux metasenv' context ugraph table 0 right in
 719         if Utils.debug_res then check_res res "demod result 1";
 720           match res with
 721           | Some t ->
 722               let newmeta, newtarget = build_newtarget false t in
 723                 if (Inference.is_weak_identity (metasenv', context, ugraph) newtarget) ||
 724                   (Inference.meta_convertibility_eq target newtarget) then
 725                     newmeta, newtarget
 726                 else
 727                    demodulation_equality newmeta env table sign newtarget
 728           | None ->
 729               newmeta, target
 730   in
 731   (* newmeta, newtarget *)
 732   newmeta,newtarget
 733 ;;
 734
 735
 736 (**
 737    Performs the beta expansion of the term "term" w.r.t. "table",
 738    i.e. returns the list of all the terms t s.t. "(t term) = t2", for some t2
 739    in table.
 740 *)
 741 let rec betaexpand_term metasenv context ugraph table lift_amount term =
 742   let module C = Cic in
 743   let module S = CicSubstitution in
 744   let module M = CicMetaSubst in
 745   let module HL = HelmLibraryObjects in
 746   let candidates = get_candidates Unification table term in
 747
 748   let res, lifted_term =
 749     match term with
 750     | C.Meta (i, l) ->
 751         let l', lifted_l =
 752           List.fold_right
 753             (fun arg (res, lifted_tl) ->
 754                match arg with
 755                | Some arg ->
 756                    let arg_res, lifted_arg =
 757                      betaexpand_term metasenv context ugraph table
 758                        lift_amount arg in
 759                    let l1 =
 760                      List.map
 761                        (fun (t, s, m, ug, eq_found) ->
 762                           (Some t)::lifted_tl, s, m, ug, eq_found)
 763                        arg_res
 764                    in
 765                    (l1 @
 766                       (List.map
 767                          (fun (l, s, m, ug, eq_found) ->
 768                             (Some lifted_arg)::l, s, m, ug, eq_found)
 769                          res),
 770                     (Some lifted_arg)::lifted_tl)
 771                | None ->
 772                    (List.map
 773                       (fun (r, s, m, ug, eq_found) ->
 774                          None::r, s, m, ug, eq_found) res,
 775                     None::lifted_tl)
 776             ) l ([], [])
 777         in
 778         let e =
 779           List.map
 780             (fun (l, s, m, ug, eq_found) ->
 781                (C.Meta (i, l), s, m, ug, eq_found)) l'
 782         in
 783         e, C.Meta (i, lifted_l)
 784
 785     | C.Rel m ->
 786         [], if m <= lift_amount then C.Rel m else C.Rel (m+1)
 787
 788     | C.Prod (nn, s, t) ->
 789         let l1, lifted_s =
 790           betaexpand_term metasenv context ugraph table lift_amount s in
 791         let l2, lifted_t =
 792           betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
 793             table (lift_amount+1) t in
 794         let l1' =
 795           List.map
 796             (fun (t, s, m, ug, eq_found) ->
 797                C.Prod (nn, t, lifted_t), s, m, ug, eq_found) l1
 798         and l2' =
 799           List.map
 800             (fun (t, s, m, ug, eq_found) ->
 801                C.Prod (nn, lifted_s, t), s, m, ug, eq_found) l2 in
 802         l1' @ l2', C.Prod (nn, lifted_s, lifted_t)
 803
 804     | C.Lambda (nn, s, t) ->
 805         let l1, lifted_s =
 806           betaexpand_term metasenv context ugraph table lift_amount s in
 807         let l2, lifted_t =
 808           betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
 809             table (lift_amount+1) t in
 810         let l1' =
 811           List.map
 812             (fun (t, s, m, ug, eq_found) ->
 813                C.Lambda (nn, t, lifted_t), s, m, ug, eq_found) l1
 814         and l2' =
 815           List.map
 816             (fun (t, s, m, ug, eq_found) ->
 817                C.Lambda (nn, lifted_s, t), s, m, ug, eq_found) l2 in
 818         l1' @ l2', C.Lambda (nn, lifted_s, lifted_t)
 819
 820     | C.Appl l ->
 821         let l', lifted_l =
 822           List.fold_right
 823             (fun arg (res, lifted_tl) ->
 824                let arg_res, lifted_arg =
 825                  betaexpand_term metasenv context ugraph table lift_amount arg
 826                in
 827                let l1 =
 828                  List.map
 829                    (fun (a, s, m, ug, eq_found) ->
 830                       a::lifted_tl, s, m, ug, eq_found)
 831                    arg_res
 832                in
 833                (l1 @
 834                   (List.map
 835                      (fun (r, s, m, ug, eq_found) ->
 836                         lifted_arg::r, s, m, ug, eq_found)
 837                      res),
 838                 lifted_arg::lifted_tl)
 839             ) l ([], [])
 840         in
 841         (List.map
 842            (fun (l, s, m, ug, eq_found) -> (C.Appl l, s, m, ug, eq_found)) l',
 843          C.Appl lifted_l)
 844
 845     | t -> [], (S.lift lift_amount t)
 846   in
 847   match term with
 848   | C.Meta (i, l) -> res, lifted_term
 849   | term ->
 850       let termty, ugraph =
 851         C.Implicit None, ugraph
 852 (*         CicTypeChecker.type_of_aux' metasenv context term ugraph *)
 853       in
 854       let r =
 855         find_all_matches
 856           metasenv context ugraph lift_amount term termty candidates
 857       in
 858       r @ res, lifted_term
 859 ;;
 860
 861
 862 let sup_l_counter = ref 1;;
 863
 864 (**
 865    superposition_left
 866    returns a list of new clauses inferred with a left superposition step
 867    the negative equation "target" and one of the positive equations in "table"
 868 *)
 869 let superposition_left newmeta (metasenv, context, ugraph) table target =
 870   let module C = Cic in
 871   let module S = CicSubstitution in
 872   let module M = CicMetaSubst in
 873   let module HL = HelmLibraryObjects in
 874   let module CR = CicReduction in
 875   let module U = Utils in
 876   let weight, proof, (eq_ty, left, right, ordering), menv, _ = target in
 877   if Utils.debug_metas then
 878     ignore(check_target context target "superpositionleft");
 879   let expansions, _ =
 880     let term = if ordering = U.Gt then left else right in
 881       begin
 882         let t1 = Unix.gettimeofday () in
 883         let res = betaexpand_term metasenv context ugraph table 0 term in
 884         let t2 = Unix.gettimeofday () in
 885           beta_expand_time := !beta_expand_time  +. (t2 -. t1);
 886         res
 887       end
 888   in
 889   let maxmeta = ref newmeta in
 890   let build_new (bo, s, m, ug, (eq_found, eq_URI)) =
 891 (*     debug_print (lazy "\nSUPERPOSITION LEFT\n"); *)
 892     let time1 = Unix.gettimeofday () in
 893
 894     let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
 895     let what, other = if pos = Utils.Left then what, other else other, what in
 896     let newgoal, newproof =
 897       let bo' =  U.guarded_simpl context (apply_subst s (S.subst other bo)) in
 898       let name = C.Name ("x_SupL_" ^ (string_of_int !sup_l_counter)) in
 899       incr sup_l_counter;
 900       let bo'' =
 901         let l, r =
 902           if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
 903         C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
 904                 S.lift 1 eq_ty; l; r]
 905       in
 906       incr maxmeta;
 907       let metaproof =
 908         let irl =
 909           CicMkImplicit.identity_relocation_list_for_metavariable context in
 910         C.Meta (!maxmeta, irl)
 911       in
 912       let eq_found =
 913         let proof' =
 914           let termlist =
 915             if pos = Utils.Left then [ty; what; other]
 916             else [ty; other; what]
 917           in
 918           Inference.ProofSymBlock (termlist, proof')
 919         in
 920         let what, other =
 921           if pos = Utils.Left then what, other else other, what
 922         in
 923         pos, (0, proof', (ty, other, what, Utils.Incomparable), menv', args')
 924       in
 925       let target_proof =
 926         let pb =
 927           Inference.ProofBlock (s, eq_URI, (name, ty), bo'', eq_found,
 928                                 Inference.BasicProof metaproof)
 929         in
 930         match proof with
 931         | Inference.BasicProof _ ->
 932 (*             debug_print (lazy "replacing a BasicProof"); *)
 933             pb
 934         | Inference.ProofGoalBlock (_, parent_proof) ->
 935 (*             debug_print (lazy "replacing another ProofGoalBlock"); *)
 936             Inference.ProofGoalBlock (pb, parent_proof)
 937         | _ -> assert false
 938       in
 939       let refl =
 940         C.Appl [C.MutConstruct (* reflexivity *)
 941                   (LibraryObjects.eq_URI (), 0, 1, []);
 942                 eq_ty; if ordering = U.Gt then right else left]
 943       in
 944       (bo',
 945        Inference.ProofGoalBlock (Inference.BasicProof refl, target_proof))
 946     in
 947     let left, right =
 948       if ordering = U.Gt then newgoal, right else left, newgoal in
 949     let neworder = !Utils.compare_terms left right in
 950     let stat = (eq_ty, left, right, neworder) in
 951     let newmenv = (* Inference.filter s *) menv in
 952     let time2 = Unix.gettimeofday () in
 953     build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
 954
 955     let w = Utils.compute_equality_weight stat in
 956     (w, newproof, stat, newmenv, [])
 957
 958   in
 959   !maxmeta, List.map build_new expansions
 960 ;;
 961
 962
 963 let sup_r_counter = ref 1;;
 964
 965 (**
 966    superposition_right
 967    returns a list of new clauses inferred with a right superposition step
 968    between the positive equation "target" and one in the "table" "newmeta" is
 969    the first free meta index, i.e. the first number above the highest meta
 970    index: its updated value is also returned
 971 *)
 972 let superposition_right newmeta (metasenv, context, ugraph) table target =
 973   let module C = Cic in
 974   let module S = CicSubstitution in
 975   let module M = CicMetaSubst in
 976   let module HL = HelmLibraryObjects in
 977   let module CR = CicReduction in
 978   let module U = Utils in
 979   let w, eqproof, (eq_ty, left, right, ordering), newmetas, args = target in
 980   if Utils.debug_metas then
 981     ignore (check_target context target "superpositionright");
 982   let metasenv' = newmetas in
 983   let maxmeta = ref newmeta in
 984   let res1, res2 =
 985     let betaexpand_term metasenv context ugraph table d term =
 986       let t1 = Unix.gettimeofday () in
 987       let res = betaexpand_term metasenv context ugraph table d term in
 988       let t2 = Unix.gettimeofday () in
 989         beta_expand_time := !beta_expand_time  +. (t2 -. t1);
 990         res
 991     in
 992     match ordering with
 993     | U.Gt -> fst (betaexpand_term metasenv' context ugraph table 0 left), []
 994     | U.Lt -> [], fst (betaexpand_term metasenv' context ugraph table 0 right)
 995     | _ ->
 996         let res l r =
 997           List.filter
 998             (fun (_, subst, _, _, _) ->
 999                let subst = apply_subst subst in
1000                let o = !Utils.compare_terms (subst l) (subst r) in
1001                o <> U.Lt && o <> U.Le)
1002             (fst (betaexpand_term metasenv' context ugraph table 0 l))
1003         in
1004         (res left right), (res right left)
1005   in
1006   let build_new ordering ((bo, s, m, ug, (eq_found, eq_URI)) as input) =
1007     if Utils.debug_metas then
1008       ignore (check_target context (snd eq_found) "buildnew1" );
1009     let time1 = Unix.gettimeofday () in
1010
1011     let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
1012     let what, other = if pos = Utils.Left then what, other else other, what in
1013     let newgoal, newproof =
1014       (* qua *)
1015       let bo' = Utils.guarded_simpl context (apply_subst s (S.subst other bo)) in
1016       let name = C.Name ("x_SupR_" ^ (string_of_int !sup_r_counter)) in
1017       incr sup_r_counter;
1018       let bo'' =
1019         let l, r =
1020           if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
1021         C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
1022                 S.lift 1 eq_ty; l; r]
1023       in
1024       bo',
1025       Inference.ProofBlock (s, eq_URI, (name, ty), bo'', eq_found, eqproof)
1026     in
1027     let newmeta, newequality =
1028       let left, right =
1029         if ordering = U.Gt then newgoal, apply_subst s right
1030         else apply_subst s left, newgoal in
1031       let neworder = !Utils.compare_terms left right in
1032       let newmenv = (* Inference.filter s *) m in
1033       let newargs = args @ args' in
1034       let stat = (eq_ty, left, right, neworder) in
1035       let eq' =
1036         let w = Utils.compute_equality_weight stat in
1037         (w, newproof, stat, newmenv, newargs) in
1038       if Utils.debug_metas then
1039         ignore (check_target context eq' "buildnew3");
1040       let newm, eq' = Inference.fix_metas !maxmeta eq' in
1041       if Utils.debug_metas then
1042         ignore (check_target context eq' "buildnew4");
1043       newm, eq'
1044     in
1045     maxmeta := newmeta;
1046     let time2 = Unix.gettimeofday () in
1047     build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
1048     if Utils.debug_metas then
1049       ignore(check_target context newequality "buildnew2");
1050     newequality
1051   in
1052   let new1 = List.map (build_new U.Gt) res1
1053   and new2 = List.map (build_new U.Lt) res2 in
1054   let ok e = not (Inference.is_identity (metasenv', context, ugraph) e) in
1055   (!maxmeta,
1056    (List.filter ok (new1 @ new2)))
1057 ;;
1058
1059
1060 (** demodulation, when the target is a goal *)
1061 let rec demodulation_goal newmeta env table goal =
1062   let module C = Cic in
1063   let module S = CicSubstitution in
1064   let module M = CicMetaSubst in
1065   let module HL = HelmLibraryObjects in
1066   let metasenv, context, ugraph = env in
1067   let maxmeta = ref newmeta in
1068   let proof, metas, term = goal in
1069   let term = Utils.guarded_simpl (~debug:true) context term in
1070   let goal = proof, metas, term in
1071   let metasenv' = metas in
1072
1073   let build_newgoal (t, subst, menv, ug, (eq_found, eq_URI)) =
1074     let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
1075     let what, other = if pos = Utils.Left then what, other else other, what in
1076     let ty =
1077       try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
1078       with CicUtil.Meta_not_found _ -> ty
1079     in
1080     let newterm, newproof =
1081       let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
1082       let bo' = apply_subst subst t in
1083       let name = C.Name ("x_DemodGoal_" ^ (string_of_int !demod_counter)) in
1084       incr demod_counter;
1085       let metaproof =
1086         incr maxmeta;
1087         let irl =
1088           CicMkImplicit.identity_relocation_list_for_metavariable context in
1089 (*         debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta)); *)
1090         C.Meta (!maxmeta, irl)
1091       in
1092       let eq_found =
1093         let proof' =
1094           let termlist =
1095             if pos = Utils.Left then [ty; what; other]
1096             else [ty; other; what]
1097           in
1098           Inference.ProofSymBlock (termlist, proof')
1099         in
1100         let what, other =
1101           if pos = Utils.Left then what, other else other, what
1102         in
1103         pos, (0, proof', (ty, other, what, Utils.Incomparable), menv', args')
1104       in
1105       let goal_proof =
1106         let pb =
1107           Inference.ProofBlock (subst, eq_URI, (name, ty), bo',
1108                                 eq_found, Inference.BasicProof metaproof)
1109         in
1110         let rec repl = function
1111           | Inference.NoProof ->
1112 (*               debug_print (lazy "replacing a NoProof"); *)
1113               pb
1114           | Inference.BasicProof _ ->
1115 (*               debug_print (lazy "replacing a BasicProof"); *)
1116               pb
1117           | Inference.ProofGoalBlock (_, parent_proof) ->
1118 (*               debug_print (lazy "replacing another ProofGoalBlock"); *)
1119               Inference.ProofGoalBlock (pb, parent_proof)
1120           | Inference.SubProof (term, meta_index, p)  ->
1121               Inference.SubProof (term, meta_index, repl p)
1122           | _ -> assert false
1123         in repl proof
1124       in
1125       bo, Inference.ProofGoalBlock (Inference.NoProof, goal_proof)
1126     in
1127     let newmetasenv = (* Inference.filter subst *) menv in
1128     !maxmeta, (newproof, newmetasenv, newterm)
1129   in
1130   let res =
1131     demodulation_aux (* ~typecheck:true *) metasenv' context ugraph table 0 term
1132   in
1133   match res with
1134   | Some t ->
1135       let newmeta, newgoal = build_newgoal t in
1136       let _, _, newg = newgoal in
1137       if Inference.meta_convertibility term newg then
1138         newmeta, newgoal
1139       else
1140         demodulation_goal newmeta env table newgoal
1141   | None ->
1142       newmeta, goal
1143 ;;
1144
1145
1146 (** demodulation, when the target is a theorem *)
1147 let rec demodulation_theorem newmeta env table theorem =
1148   let module C = Cic in
1149   let module S = CicSubstitution in
1150   let module M = CicMetaSubst in
1151   let module HL = HelmLibraryObjects in
1152   let metasenv, context, ugraph = env in
1153   let maxmeta = ref newmeta in
1154   let term, termty, metas = theorem in
1155   let metasenv' = metas in
1156
1157   let build_newtheorem (t, subst, menv, ug, (eq_found, eq_URI)) =
1158     let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
1159     let what, other = if pos = Utils.Left then what, other else other, what in
1160     let newterm, newty =
1161       let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
1162       let bo' = apply_subst subst t in
1163       let name = C.Name ("x_DemodThm_" ^ (string_of_int !demod_counter)) in
1164       incr demod_counter;
1165       let newproof =
1166         Inference.ProofBlock (subst, eq_URI, (name, ty), bo', eq_found,
1167                               Inference.BasicProof term)
1168       in
1169       (Inference.build_proof_term newproof, bo)
1170     in
1171
1172     let m = Inference.metas_of_term newterm in
1173     !maxmeta, (newterm, newty, menv)
1174   in
1175   let res =
1176     demodulation_aux (* ~typecheck:true *) metasenv' context ugraph table 0 termty
1177   in
1178   match res with
1179   | Some t ->
1180       let newmeta, newthm = build_newtheorem t in
1181       let newt, newty, _ = newthm in
1182       if Inference.meta_convertibility termty newty then
1183         newmeta, newthm
1184       else
1185         demodulation_theorem newmeta env table newthm
1186   | None ->
1187       newmeta, theorem
1188 ;;
1189