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