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