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