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