components/tactics/paramodulation/indexing.ml

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