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         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 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 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 metasenv context ugraph lift_amount term termty tl
 246         ) else
 247           let do_match c =
 248             let subst', metasenv', ugraph' =
 249               Inference.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 Inference.MatchingFailure ->
 263                 find_matches metasenv context ugraph lift_amount term termty tl
 264             in
 265               if Utils.debug_res then ignore (check_res res "find1");
 266               res
 267           else
 268             let res =
 269               try do_match c
 270               with Inference.MatchingFailure -> None
 271             in
 272             if Utils.debug_res then ignore (check_res res "find2");
 273             match res with
 274             | Some (_, s, _, _, _) ->
 275                 let c' = apply_subst s c in
 276                 (*
 277              let other' = U.guarded_simpl context (apply_subst s other) in *)
 278                 let other' = apply_subst s other in
 279                 let order = cmp c' other' in
 280                 if order = U.Gt then
 281                   res
 282                 else
 283                   find_matches
 284                     metasenv context ugraph lift_amount term termty tl
 285             | None ->
 286                 find_matches metasenv context ugraph lift_amount term termty tl
 287 ;;
 288
 289 let find_matches metasenv context ugraph lift_amount term termty =
 290   find_matches metasenv context ugraph lift_amount term termty
 291 ;;
 292
 293 (*
 294   as above, but finds all the matching equalities, and the matching condition
 295   can be either Inference.matching or Inference.unification
 296 *)
 297 let rec find_all_matches ?(unif_fun=Inference.unification)
 298     metasenv context ugraph lift_amount term termty =
 299   let module C = Cic in
 300   let module U = Utils in
 301   let module S = CicSubstitution in
 302   let module M = CicMetaSubst in
 303   let module HL = HelmLibraryObjects in
 304   let cmp = !Utils.compare_terms in
 305   function
 306     | [] -> []
 307     | candidate::tl ->
 308         let pos, equality = candidate in
 309         let (_,_,(ty,left,right,o),metas,_)=Equality.open_equality equality in
 310         let do_match c =
 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           | Inference.MatchingFailure
 327           | CicUnification.UnificationFailure _
 328           | CicUnification.Uncertain _ ->
 329               find_all_matches ~unif_fun metasenv context ugraph
 330                 lift_amount term termty tl
 331         else
 332           try
 333             let res = do_match c in
 334             match res with
 335             | _, s, _, _, _ ->
 336                 let c' = apply_subst s c
 337                 and other' = apply_subst s other in
 338                 let order = cmp c' other' in
 339                 if order <> U.Lt && order <> U.Le then
 340                   res::(find_all_matches ~unif_fun metasenv context ugraph
 341                           lift_amount term termty tl)
 342                 else
 343                   find_all_matches ~unif_fun metasenv context ugraph
 344                     lift_amount term termty tl
 345           with
 346           | Inference.MatchingFailure
 347           | CicUnification.UnificationFailure _
 348           | CicUnification.Uncertain _ ->
 349               find_all_matches ~unif_fun metasenv context ugraph
 350                 lift_amount term termty tl
 351 ;;
 352
 353 let find_all_matches
 354   ?unif_fun metasenv context ugraph lift_amount term termty l
 355 =
 356     find_all_matches
 357       ?unif_fun metasenv context ugraph lift_amount term termty l
 358   (*prerr_endline "CANDIDATES:";
 359   List.iter (fun (_,x)->prerr_endline (Inference.string_of_equality x)) l;
 360   prerr_endline ("MATCHING:" ^ CicPp.ppterm term ^ " are " ^ string_of_int
 361   (List.length rc));*)
 362 ;;
 363 (*
 364   returns true if target is subsumed by some equality in table
 365 *)
 366 let print_res l =
 367   prerr_endline (String.concat "\n" (List.map (fun (_, subst, menv, ug,
 368     ((pos,equation),_)) -> Equality.string_of_equality equation)l))
 369 ;;
 370
 371 let subsumption_aux use_unification env table target =
 372   let _, _, (ty, left, right, _), tmetas, _ = Equality.open_equality target in
 373   let metasenv, context, ugraph = env in
 374   let metasenv = tmetas in
 375   let predicate, unif_fun =
 376     if use_unification then
 377       Unification, Inference.unification
 378     else
 379       Matching, Inference.matching
 380   in
 381   let leftr =
 382     match left with
 383     | Cic.Meta _ when not use_unification -> []
 384     | _ ->
 385         let leftc = get_candidates predicate table left in
 386         find_all_matches ~unif_fun
 387           metasenv context ugraph 0 left ty leftc
 388   in
 389   let rec ok what 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         | Inference.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 ?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 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 ~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 ~from:"2"
 482                         metasenv context ugraph table lift_amount s in (
 483                         match r1 with
 484                           | None ->
 485                               let r2 =
 486                                 demodulation_aux 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
 503                         metasenv context ugraph table lift_amount s in (
 504                         match r1 with
 505                           | None ->
 506                               let r2 =
 507                                 demodulation_aux 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 ?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 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 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 (w, newproof, stat,newmenv))
 589     in
 590     if Utils.debug_metas then
 591       ignore(check_target context res "buildnew_target output");
 592     !maxmeta, res
 593   in
 594
 595   let res = demodulation_aux ~from:"3" metasenv' context ugraph table 0 left in
 596   if Utils.debug_res then check_res res "demod result";
 597   let newmeta, newtarget =
 598     match res with
 599     | Some t ->
 600         let newmeta, newtarget = build_newtarget true t in
 601           assert (not (Equality.meta_convertibility_eq target newtarget));
 602           if (Equality.is_weak_identity newtarget) ||
 603             (Equality.meta_convertibility_eq target newtarget) then
 604               newmeta, newtarget
 605           else
 606             demodulation_equality ?from eq_uri newmeta env table newtarget
 607     | None ->
 608         let res = demodulation_aux metasenv' context ugraph table 0 right in
 609         if Utils.debug_res then check_res res "demod result 1";
 610           match res with
 611           | Some t ->
 612               let newmeta, newtarget = build_newtarget false t in
 613                 if (Equality.is_weak_identity newtarget) ||
 614                   (Equality.meta_convertibility_eq target newtarget) then
 615                     newmeta, newtarget
 616                 else
 617                    demodulation_equality ?from eq_uri newmeta env table newtarget
 618           | None ->
 619               newmeta, target
 620   in
 621   (* newmeta, newtarget *)
 622   newmeta,newtarget
 623 ;;
 624
 625 (**
 626    Performs the beta expansion of the term "term" w.r.t. "table",
 627    i.e. returns the list of all the terms t s.t. "(t term) = t2", for some t2
 628    in table.
 629 *)
 630 let rec betaexpand_term
 631   ?(subterms_only=false) metasenv context ugraph table lift_amount term
 632 =
 633   let module C = Cic in
 634   let module S = CicSubstitution in
 635   let module M = CicMetaSubst in
 636   let module HL = HelmLibraryObjects in
 637
 638   let res, lifted_term =
 639     match term with
 640     | C.Meta (i, l) ->
 641         let l = [] in
 642         let l', lifted_l =
 643           List.fold_right
 644             (fun arg (res, lifted_tl) ->
 645                match arg with
 646                | Some arg ->
 647                    let arg_res, lifted_arg =
 648                      betaexpand_term metasenv context ugraph table
 649                        lift_amount arg in
 650                    let l1 =
 651                      List.map
 652                        (fun (t, s, m, ug, eq_found) ->
 653                           (Some t)::lifted_tl, s, m, ug, eq_found)
 654                        arg_res
 655                    in
 656                    (l1 @
 657                       (List.map
 658                          (fun (l, s, m, ug, eq_found) ->
 659                             (Some lifted_arg)::l, s, m, ug, eq_found)
 660                          res),
 661                     (Some lifted_arg)::lifted_tl)
 662                | None ->
 663                    (List.map
 664                       (fun (r, s, m, ug, eq_found) ->
 665                          None::r, s, m, ug, eq_found) res,
 666                     None::lifted_tl)
 667             ) l ([], [])
 668         in
 669         let e =
 670           List.map
 671             (fun (l, s, m, ug, eq_found) ->
 672                (C.Meta (i, l), s, m, ug, eq_found)) l'
 673         in
 674         e, C.Meta (i, lifted_l)
 675
 676     | C.Rel m ->
 677         [], if m <= lift_amount then C.Rel m else C.Rel (m+1)
 678
 679     | C.Prod (nn, s, t) ->
 680         let l1, lifted_s =
 681           betaexpand_term metasenv context ugraph table lift_amount s in
 682         let l2, lifted_t =
 683           betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
 684             table (lift_amount+1) t in
 685         let l1' =
 686           List.map
 687             (fun (t, s, m, ug, eq_found) ->
 688                C.Prod (nn, t, lifted_t), s, m, ug, eq_found) l1
 689         and l2' =
 690           List.map
 691             (fun (t, s, m, ug, eq_found) ->
 692                C.Prod (nn, lifted_s, t), s, m, ug, eq_found) l2 in
 693         l1' @ l2', C.Prod (nn, lifted_s, lifted_t)
 694
 695     | C.Lambda (nn, s, t) ->
 696         let l1, lifted_s =
 697           betaexpand_term metasenv context ugraph table lift_amount s in
 698         let l2, lifted_t =
 699           betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
 700             table (lift_amount+1) t in
 701         let l1' =
 702           List.map
 703             (fun (t, s, m, ug, eq_found) ->
 704                C.Lambda (nn, t, lifted_t), s, m, ug, eq_found) l1
 705         and l2' =
 706           List.map
 707             (fun (t, s, m, ug, eq_found) ->
 708                C.Lambda (nn, lifted_s, t), s, m, ug, eq_found) l2 in
 709         l1' @ l2', C.Lambda (nn, lifted_s, lifted_t)
 710
 711     | C.Appl l ->
 712         let l', lifted_l =
 713           List.fold_left
 714             (fun (res, lifted_tl) arg ->
 715                let arg_res, lifted_arg =
 716                  betaexpand_term metasenv context ugraph table lift_amount arg
 717                in
 718                let l1 =
 719                  List.map
 720                    (fun (a, s, m, ug, eq_found) ->
 721                       a::lifted_tl, s, m, ug, eq_found)
 722                    arg_res
 723                in
 724                (l1 @
 725                   (List.map
 726                      (fun (r, s, m, ug, eq_found) ->
 727                         lifted_arg::r, s, m, ug, eq_found)
 728                      res),
 729                 lifted_arg::lifted_tl)
 730             ) ([], []) (List.rev l)
 731         in
 732         (List.map
 733            (fun (l, s, m, ug, eq_found) -> (C.Appl l, s, m, ug, eq_found)) l',
 734          C.Appl lifted_l)
 735
 736     | t -> [], (S.lift lift_amount t)
 737   in
 738   match term with
 739   | C.Meta (i, l) -> res, lifted_term
 740   | term ->
 741       let termty, ugraph =
 742         C.Implicit None, ugraph
 743 (*         CicTypeChecker.type_of_aux' metasenv context term ugraph *)
 744       in
 745       let candidates = get_candidates Unification table term in
 746       let r =
 747         if subterms_only then
 748           []
 749         else
 750           find_all_matches
 751             metasenv context ugraph lift_amount term termty candidates
 752       in
 753       r @ res, lifted_term
 754 ;;
 755
 756 (**
 757    superposition_right
 758    returns a list of new clauses inferred with a right superposition step
 759    between the positive equation "target" and one in the "table" "newmeta" is
 760    the first free meta index, i.e. the first number above the highest meta
 761    index: its updated value is also returned
 762 *)
 763 let superposition_right
 764   ?(subterms_only=false) eq_uri newmeta (metasenv, context, ugraph) table target=
 765   let module C = Cic in
 766   let module S = CicSubstitution in
 767   let module M = CicMetaSubst in
 768   let module HL = HelmLibraryObjects in
 769   let module CR = CicReduction in
 770   let module U = Utils in
 771   let w, eqproof, (eq_ty, left, right, ordering), newmetas,id =
 772     Equality.open_equality target
 773   in
 774   if Utils.debug_metas then
 775     ignore (check_target context target "superpositionright");
 776   let metasenv' = newmetas in
 777   let maxmeta = ref newmeta in
 778   let res1, res2 =
 779     match ordering with
 780     | U.Gt ->
 781         fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 left), []
 782     | U.Lt ->
 783         [], fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 right)
 784     | _ ->
 785         let res l r =
 786           List.filter
 787             (fun (_, subst, _, _, _) ->
 788                let subst = apply_subst subst in
 789                let o = !Utils.compare_terms (subst l) (subst r) in
 790                o <> U.Lt && o <> U.Le)
 791             (fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 l))
 792         in
 793         (res left right), (res right left)
 794   in
 795   let build_new ordering (bo, s, m, ug, eq_found) =
 796     if Utils.debug_metas then
 797       ignore (check_target context (snd eq_found) "buildnew1" );
 798
 799     let pos, equality =  eq_found in
 800     let (_, proof', (ty, what, other, _), menv',id') =
 801       Equality.open_equality  equality in
 802     let what, other = if pos = Utils.Left then what, other else other, what in
 803
 804     let newgoal, newproof =
 805       (* qua *)
 806       let bo' =
 807         Utils.guarded_simpl context (apply_subst s (S.subst other bo))
 808       in
 809       let name = C.Name "x" in
 810       let bo'' =
 811         let l, r =
 812           if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
 813         C.Appl [C.MutInd (eq_uri, 0, []); S.lift 1 eq_ty; l; r]
 814       in
 815       bo',
 816         Equality.Step
 817           (s,(Equality.SuperpositionRight,
 818                id,(pos,id'),(Cic.Lambda(name,ty,bo''))))
 819     in
 820     let newmeta, newequality =
 821       let left, right =
 822         if ordering = U.Gt then newgoal, apply_subst s right
 823         else apply_subst s left, newgoal in
 824       let neworder = !Utils.compare_terms left right in
 825       let newmenv = (* Inference.filter s *) m in
 826       let stat = (eq_ty, left, right, neworder) in
 827       let eq' =
 828         let w = Utils.compute_equality_weight stat in
 829         Equality.mk_equality (w, newproof, stat, newmenv) in
 830       if Utils.debug_metas then
 831         ignore (check_target context eq' "buildnew3");
 832       let newm, eq' = Equality.fix_metas !maxmeta eq' in
 833       if Utils.debug_metas then
 834         ignore (check_target context eq' "buildnew4");
 835       newm, eq'
 836     in
 837     maxmeta := newmeta;
 838     if Utils.debug_metas then
 839       ignore(check_target context newequality "buildnew2");
 840     newequality
 841   in
 842   let new1 = List.map (build_new U.Gt) res1
 843   and new2 = List.map (build_new U.Lt) res2 in
 844   let ok e = not (Equality.is_identity (metasenv', context, ugraph) e) in
 845   (!maxmeta,
 846    (List.filter ok (new1 @ new2)))
 847 ;;
 848
 849 (** demodulation, when the target is a theorem *)
 850 let rec demodulation_theorem newmeta env table theorem =
 851   let module C = Cic in
 852   let module S = CicSubstitution in
 853   let module M = CicMetaSubst in
 854   let module HL = HelmLibraryObjects in
 855   let metasenv, context, ugraph = env in
 856   let maxmeta = ref newmeta in
 857   let term, termty, metas = theorem in
 858   let metasenv' = metas in
 859
 860   let build_newtheorem (t, subst, menv, ug, eq_found) =
 861     let pos, equality = eq_found in
 862     let (_, proof', (ty, what, other, _), menv',id) =
 863       Equality.open_equality equality in
 864     let what, other = if pos = Utils.Left then what, other else other, what in
 865     let newterm, newty =
 866       let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
 867 (*      let bo' = apply_subst subst t in *)
 868 (*      let name = C.Name ("x_DemodThm_" ^ (string_of_int !demod_counter)) in*)
 869 (*
 870       let newproofold =
 871         Equality.ProofBlock (subst, eq_URI, (name, ty), bo', eq_found,
 872                               Equality.BasicProof (Equality.empty_subst,term))
 873       in
 874       (Equality.build_proof_term_old newproofold, bo)
 875 *)
 876       (* TODO, not ported to the new proofs *)
 877       if true then assert false; term, bo
 878     in
 879     !maxmeta, (newterm, newty, menv)
 880   in
 881   let res =
 882     demodulation_aux (* ~typecheck:true *) metasenv' context ugraph table 0 termty
 883   in
 884   match res with
 885   | Some t ->
 886       let newmeta, newthm = build_newtheorem t in
 887       let newt, newty, _ = newthm in
 888       if Equality.meta_convertibility termty newty then
 889         newmeta, newthm
 890       else
 891         demodulation_theorem newmeta env table newthm
 892   | None ->
 893       newmeta, theorem
 894 ;;
 895
 896 (*****************************************************************************)
 897 (**                         OPERATIONS ON GOALS                             **)
 898 (**                                                                         **)
 899 (**                DEMODULATION_GOAL & SUPERPOSITION_LEFT                   **)
 900 (*****************************************************************************)
 901
 902 let open_goal g =
 903   match g with
 904   | (proof,menv,Cic.Appl[(Cic.MutInd(uri,0,_)) as eq;ty;l;r]) ->
 905       assert (LibraryObjects.is_eq_URI uri);
 906       proof,menv,eq,ty,l,r
 907   | _ -> assert false
 908 ;;
 909
 910 let ty_of_goal (_,_,ty) = ty ;;
 911
 912 (* checks if two goals are metaconvertible *)
 913 let goal_metaconvertibility_eq g1 g2 =
 914   Equality.meta_convertibility (ty_of_goal g1) (ty_of_goal g2)
 915 ;;
 916
 917 (* when the betaexpand_term function is called on the left/right side of the
 918  * goal, the predicate has to be fixed
 919  * C[x] ---> (eq ty unchanged C[x])
 920  * [posu] is the side of the [unchanged] term in the original goal
 921  *)
 922 let fix_expansion goal posu (t, subst, menv, ug, eq_f) =
 923   let _,_,eq,ty,l,r = open_goal goal in
 924   let unchanged = if posu = Utils.Left then l else r in
 925   let unchanged = CicSubstitution.lift 1 unchanged in
 926   let ty = CicSubstitution.lift 1 ty in
 927   let pred =
 928     match posu with
 929     | Utils.Left -> Cic.Appl [eq;ty;unchanged;t]
 930     | Utils.Right -> Cic.Appl [eq;ty;t;unchanged]
 931   in
 932   (pred, subst, menv, ug, eq_f)
 933 ;;
 934
 935 (* ginve the old [goal], the side that has not changed [posu] and the
 936  * expansion builds a new goal *)
 937 let build_newgoal context goal posu rule expansion =
 938   let goalproof,_,_,_,_,_ = open_goal goal in
 939   let (t,subst,menv,ug,eq_found) = fix_expansion goal posu expansion in
 940   let pos, equality = eq_found in
 941   let (_, proof', (ty, what, other, _), menv',id) =
 942     Equality.open_equality equality in
 943   let what, other = if pos = Utils.Left then what, other else other, what in
 944   let newterm, newgoalproof =
 945     let bo =
 946       Utils.guarded_simpl context
 947         (apply_subst subst (CicSubstitution.subst other t))
 948     in
 949     let bo' = (*apply_subst subst*) t in
 950     let name = Cic.Name "x" in
 951     let newgoalproofstep = (rule,pos,id,subst,Cic.Lambda (name,ty,bo')) in
 952     bo, (newgoalproofstep::goalproof)
 953   in
 954   let newmetasenv = (* Inference.filter subst *) menv in
 955   (newgoalproof, newmetasenv, newterm)
 956 ;;
 957
 958 (**
 959    superposition_left
 960    returns a list of new clauses inferred with a left superposition step
 961    the negative equation "target" and one of the positive equations in "table"
 962 *)
 963 let superposition_left (metasenv, context, ugraph) table goal maxmeta =
 964   let names = Utils.names_of_context context in
 965   let proof,menv,eq,ty,l,r = open_goal goal in
 966   let c = !Utils.compare_terms l r in
 967   let newgoals =
 968     if c = Utils.Incomparable then
 969       begin
 970       let expansionsl, _ = betaexpand_term menv context ugraph table 0 l in
 971       let expansionsr, _ = betaexpand_term menv context ugraph table 0 r in
 972       (* prerr_endline "incomparable";
 973       prerr_endline (string_of_int (List.length expansionsl));
 974       prerr_endline (string_of_int (List.length expansionsr));
 975       *)
 976       List.map (build_newgoal context goal Utils.Right Equality.SuperpositionLeft) expansionsl
 977       @
 978       List.map (build_newgoal context goal Utils.Left Equality.SuperpositionLeft) expansionsr
 979       end
 980     else
 981         match c with
 982         | Utils.Gt -> (* prerr_endline "GT"; *)
 983             let big,small,possmall = l,r,Utils.Right in
 984             let expansions, _ = betaexpand_term menv context ugraph table 0 big in
 985             List.map
 986               (build_newgoal context goal possmall Equality.SuperpositionLeft)
 987               expansions
 988         | Utils.Lt -> (* prerr_endline "LT"; *)
 989             let big,small,possmall = r,l,Utils.Left 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.Eq -> []
 995         | _ ->
 996             prerr_endline
 997               ("NOT GT, LT NOR EQ : "^CicPp.pp l names^" - "^CicPp.pp r names);
 998             assert false
 999   in
1000   (* rinfresco le meta *)
1001   List.fold_right
1002     (fun g (max,acc) ->
1003        let max,g = Equality.fix_metas_goal max g in max,g::acc)
1004     newgoals (maxmeta,[])
1005 ;;
1006
1007 (** demodulation, when the target is a goal *)
1008 let rec demodulation_goal env table goal =
1009   let goalproof,menv,_,_,left,right = open_goal goal in
1010   let _, context, ugraph = env in
1011 (*  let term = Utils.guarded_simpl (~debug:true) context term in*)
1012   let do_right () =
1013       let resright = demodulation_aux menv context ugraph table 0 right in
1014       match resright with
1015       | Some t ->
1016           let newg =
1017             build_newgoal context goal Utils.Left Equality.Demodulation t
1018           in
1019           if goal_metaconvertibility_eq goal newg then
1020             false, goal
1021           else
1022             true, snd (demodulation_goal env table newg)
1023       | None -> false, goal
1024   in
1025   let resleft = demodulation_aux menv context ugraph table 0 left in
1026   match resleft with
1027   | Some t ->
1028       let newg = build_newgoal context goal Utils.Right Equality.Demodulation t in
1029       if goal_metaconvertibility_eq goal newg then
1030         do_right ()
1031       else
1032         true, snd (demodulation_goal env table newg)
1033   | None -> do_right ()
1034 ;;
1035
1036 let get_stats () = "" ;;