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