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 = [] in
 732         let l', lifted_l =
 733           List.fold_right
 734             (fun arg (res, lifted_tl) ->
 735                match arg with
 736                | Some arg ->
 737                    let arg_res, lifted_arg =
 738                      betaexpand_term metasenv context ugraph table
 739                        lift_amount arg in
 740                    let l1 =
 741                      List.map
 742                        (fun (t, s, m, ug, eq_found) ->
 743                           (Some t)::lifted_tl, s, m, ug, eq_found)
 744                        arg_res
 745                    in
 746                    (l1 @
 747                       (List.map
 748                          (fun (l, s, m, ug, eq_found) ->
 749                             (Some lifted_arg)::l, s, m, ug, eq_found)
 750                          res),
 751                     (Some lifted_arg)::lifted_tl)
 752                | None ->
 753                    (List.map
 754                       (fun (r, s, m, ug, eq_found) ->
 755                          None::r, s, m, ug, eq_found) res,
 756                     None::lifted_tl)
 757             ) l ([], [])
 758         in
 759         let e =
 760           List.map
 761             (fun (l, s, m, ug, eq_found) ->
 762                (C.Meta (i, l), s, m, ug, eq_found)) l'
 763         in
 764         e, C.Meta (i, lifted_l)
 765
 766     | C.Rel m ->
 767         [], if m <= lift_amount then C.Rel m else C.Rel (m+1)
 768
 769     | C.Prod (nn, s, t) ->
 770         let l1, lifted_s =
 771           betaexpand_term metasenv context ugraph table lift_amount s in
 772         let l2, lifted_t =
 773           betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
 774             table (lift_amount+1) t in
 775         let l1' =
 776           List.map
 777             (fun (t, s, m, ug, eq_found) ->
 778                C.Prod (nn, t, lifted_t), s, m, ug, eq_found) l1
 779         and l2' =
 780           List.map
 781             (fun (t, s, m, ug, eq_found) ->
 782                C.Prod (nn, lifted_s, t), s, m, ug, eq_found) l2 in
 783         l1' @ l2', C.Prod (nn, lifted_s, lifted_t)
 784
 785     | C.Lambda (nn, s, t) ->
 786         let l1, lifted_s =
 787           betaexpand_term metasenv context ugraph table lift_amount s in
 788         let l2, lifted_t =
 789           betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
 790             table (lift_amount+1) t in
 791         let l1' =
 792           List.map
 793             (fun (t, s, m, ug, eq_found) ->
 794                C.Lambda (nn, t, lifted_t), s, m, ug, eq_found) l1
 795         and l2' =
 796           List.map
 797             (fun (t, s, m, ug, eq_found) ->
 798                C.Lambda (nn, lifted_s, t), s, m, ug, eq_found) l2 in
 799         l1' @ l2', C.Lambda (nn, lifted_s, lifted_t)
 800
 801     | C.Appl l ->
 802         let l', lifted_l =
 803           List.fold_right
 804             (fun arg (res, lifted_tl) ->
 805                let arg_res, lifted_arg =
 806                  betaexpand_term metasenv context ugraph table lift_amount arg
 807                in
 808                let l1 =
 809                  List.map
 810                    (fun (a, s, m, ug, eq_found) ->
 811                       a::lifted_tl, s, m, ug, eq_found)
 812                    arg_res
 813                in
 814                (l1 @
 815                   (List.map
 816                      (fun (r, s, m, ug, eq_found) ->
 817                         lifted_arg::r, s, m, ug, eq_found)
 818                      res),
 819                 lifted_arg::lifted_tl)
 820             ) l ([], [])
 821         in
 822         (List.map
 823            (fun (l, s, m, ug, eq_found) -> (C.Appl l, s, m, ug, eq_found)) l',
 824          C.Appl lifted_l)
 825
 826     | t -> [], (S.lift lift_amount t)
 827   in
 828   match term with
 829   | C.Meta (i, l) -> res, lifted_term
 830   | term ->
 831       let termty, ugraph =
 832         C.Implicit None, ugraph
 833 (*         CicTypeChecker.type_of_aux' metasenv context term ugraph *)
 834       in
 835       let candidates = get_candidates Unification table term in
 836       let r =
 837         if subterms_only then
 838           []
 839         else
 840           find_all_matches
 841             metasenv context ugraph lift_amount term termty candidates
 842       in
 843       r @ res, lifted_term
 844 ;;
 845
 846 (**
 847    superposition_right
 848    returns a list of new clauses inferred with a right superposition step
 849    between the positive equation "target" and one in the "table" "newmeta" is
 850    the first free meta index, i.e. the first number above the highest meta
 851    index: its updated value is also returned
 852 *)
 853 let superposition_right
 854   ?(subterms_only=false) newmeta (metasenv, context, ugraph) table target
 855 =
 856   let module C = Cic in
 857   let module S = CicSubstitution in
 858   let module M = CicMetaSubst in
 859   let module HL = HelmLibraryObjects in
 860   let module CR = CicReduction in
 861   let module U = Utils in
 862   let w, eqproof, (eq_ty, left, right, ordering), newmetas,id =
 863     Equality.open_equality target
 864   in
 865   if Utils.debug_metas then
 866     ignore (check_target context target "superpositionright");
 867   let metasenv' = newmetas in
 868   let maxmeta = ref newmeta in
 869   let res1, res2 =
 870     match ordering with
 871     | U.Gt ->
 872         fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 left), []
 873     | U.Lt ->
 874         [], fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 right)
 875     | _ ->
 876         let res l r =
 877           List.filter
 878             (fun (_, subst, _, _, _) ->
 879                let subst = apply_subst subst in
 880                let o = !Utils.compare_terms (subst l) (subst r) in
 881                o <> U.Lt && o <> U.Le)
 882             (fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 l))
 883         in
 884         (res left right), (res right left)
 885   in
 886   let build_new ordering (bo, s, m, ug, (eq_found, eq_URI)) =
 887     if Utils.debug_metas then
 888       ignore (check_target context (snd eq_found) "buildnew1" );
 889
 890     let pos, equality =  eq_found in
 891     let (_, proof', (ty, what, other, _), menv',id') =
 892       Equality.open_equality  equality in
 893     let what, other = if pos = Utils.Left then what, other else other, what in
 894
 895     let newgoal, newproof =
 896       (* qua *)
 897       let bo' =
 898         Utils.guarded_simpl context (apply_subst s (S.subst other bo))
 899       in
 900       let name = C.Name "x" in
 901       let bo'' =
 902         let l, r =
 903           if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
 904         C.Appl [C.MutInd (Utils.eq_URI (), 0, []);
 905                 S.lift 1 eq_ty; l; r]
 906       in
 907       bo',
 908         Equality.Step
 909           (s,(Equality.SuperpositionRight,
 910                id,(pos,id'),(Cic.Lambda(name,ty,bo''))))
 911     in
 912     let newmeta, newequality =
 913       let left, right =
 914         if ordering = U.Gt then newgoal, apply_subst s right
 915         else apply_subst s left, newgoal in
 916       let neworder = !Utils.compare_terms left right in
 917       let newmenv = (* Inference.filter s *) m in
 918       let stat = (eq_ty, left, right, neworder) in
 919       let eq' =
 920         let w = Utils.compute_equality_weight stat in
 921         Equality.mk_equality (w, newproof, stat, newmenv) in
 922       if Utils.debug_metas then
 923         ignore (check_target context eq' "buildnew3");
 924       let newm, eq' = Equality.fix_metas !maxmeta eq' in
 925       if Utils.debug_metas then
 926         ignore (check_target context eq' "buildnew4");
 927       newm, eq'
 928     in
 929     maxmeta := newmeta;
 930     if Utils.debug_metas then
 931       ignore(check_target context newequality "buildnew2");
 932     newequality
 933   in
 934   let new1 = List.map (build_new U.Gt) res1
 935   and new2 = List.map (build_new U.Lt) res2 in
 936   let ok e = not (Equality.is_identity (metasenv', context, ugraph) e) in
 937   (!maxmeta,
 938    (List.filter ok (new1 @ new2)))
 939 ;;
 940
 941 (** demodulation, when the target is a theorem *)
 942 let rec demodulation_theorem newmeta env table theorem =
 943   let module C = Cic in
 944   let module S = CicSubstitution in
 945   let module M = CicMetaSubst in
 946   let module HL = HelmLibraryObjects in
 947   let metasenv, context, ugraph = env in
 948   let maxmeta = ref newmeta in
 949   let term, termty, metas = theorem in
 950   let metasenv' = metas in
 951
 952   let build_newtheorem (t, subst, menv, ug, (eq_found, eq_URI)) =
 953     let pos, equality = eq_found in
 954     let (_, proof', (ty, what, other, _), menv',id) =
 955       Equality.open_equality equality in
 956     let what, other = if pos = Utils.Left then what, other else other, what in
 957     let newterm, newty =
 958       let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
 959 (*      let bo' = apply_subst subst t in *)
 960 (*      let name = C.Name ("x_DemodThm_" ^ (string_of_int !demod_counter)) in*)
 961 (*
 962       let newproofold =
 963         Equality.ProofBlock (subst, eq_URI, (name, ty), bo', eq_found,
 964                               Equality.BasicProof (Equality.empty_subst,term))
 965       in
 966       (Equality.build_proof_term_old newproofold, bo)
 967 *)
 968       (* TODO, not ported to the new proofs *)
 969       if true then assert false; term, bo
 970     in
 971     !maxmeta, (newterm, newty, menv)
 972   in
 973   let res =
 974     demodulation_aux (* ~typecheck:true *) metasenv' context ugraph table 0 termty
 975   in
 976   match res with
 977   | Some t ->
 978       let newmeta, newthm = build_newtheorem t in
 979       let newt, newty, _ = newthm in
 980       if Equality.meta_convertibility termty newty then
 981         newmeta, newthm
 982       else
 983         demodulation_theorem newmeta env table newthm
 984   | None ->
 985       newmeta, theorem
 986 ;;
 987
 988 (*****************************************************************************)
 989 (**                         OPERATIONS ON GOALS                             **)
 990 (**                                                                         **)
 991 (**                DEMODULATION_GOAL & SUPERPOSITION_LEFT                   **)
 992 (*****************************************************************************)
 993
 994 let open_goal g =
 995   match g with
 996   | (proof,menv,Cic.Appl[(Cic.MutInd(uri,0,_)) as eq;ty;l;r]) ->
 997       assert (LibraryObjects.is_eq_URI uri);
 998       proof,menv,eq,ty,l,r
 999   | _ -> assert false
1000 ;;
1001
1002 let ty_of_goal (_,_,ty) = ty ;;
1003
1004 (* checks if two goals are metaconvertible *)
1005 let goal_metaconvertibility_eq g1 g2 =
1006   Equality.meta_convertibility (ty_of_goal g1) (ty_of_goal g2)
1007 ;;
1008
1009 (* when the betaexpand_term function is called on the left/right side of the
1010  * goal, the predicate has to be fixed
1011  * C[x] ---> (eq ty unchanged C[x])
1012  * [posu] is the side of the [unchanged] term in the original goal
1013  *)
1014 let fix_expansion goal posu (t, subst, menv, ug, eq_f) =
1015   let _,_,eq,ty,l,r = open_goal goal in
1016   let unchanged = if posu = Utils.Left then l else r in
1017   let unchanged = CicSubstitution.lift 1 unchanged in
1018   let ty = CicSubstitution.lift 1 ty in
1019   let pred =
1020     match posu with
1021     | Utils.Left -> Cic.Appl [eq;ty;unchanged;t]
1022     | Utils.Right -> Cic.Appl [eq;ty;t;unchanged]
1023   in
1024   (pred, subst, menv, ug, eq_f)
1025 ;;
1026
1027 (* ginve the old [goal], the side that has not changed [posu] and the
1028  * expansion builds a new goal *)
1029 let build_newgoal context goal posu rule expansion =
1030   let goalproof,_,_,_,_,_ = open_goal goal in
1031   let (t,subst,menv,ug,(eq_found,eq_URI)) = fix_expansion goal posu expansion in
1032   let pos, equality = eq_found in
1033   let (_, proof', (ty, what, other, _), menv',id) =
1034     Equality.open_equality equality in
1035   let what, other = if pos = Utils.Left then what, other else other, what in
1036   let newterm, newgoalproof =
1037     let bo =
1038       Utils.guarded_simpl context
1039         (apply_subst subst (CicSubstitution.subst other t))
1040     in
1041     let bo' = (*apply_subst subst*) t in
1042     let name = Cic.Name "x" in
1043     let newgoalproofstep = (rule,pos,id,subst,Cic.Lambda (name,ty,bo')) in
1044     bo, (newgoalproofstep::goalproof)
1045   in
1046   let newmetasenv = (* Inference.filter subst *) menv in
1047   (newgoalproof, newmetasenv, newterm)
1048 ;;
1049
1050 (**
1051    superposition_left
1052    returns a list of new clauses inferred with a left superposition step
1053    the negative equation "target" and one of the positive equations in "table"
1054 *)
1055 let superposition_left (metasenv, context, ugraph) table goal =
1056   let proof,menv,eq,ty,l,r = open_goal goal in
1057   let c =
1058     Utils.compare_weights ~normalize:true
1059       (Utils.weight_of_term l) (Utils.weight_of_term r)
1060   in
1061
1062   if c = Utils.Incomparable then
1063     let expansionsl, _ = betaexpand_term menv context ugraph table 0 l in
1064     let expansionsr, _ = betaexpand_term menv context ugraph table 0 r in
1065     prerr_endline "ZZZ";
1066     prerr_endline (string_of_int (List.length expansionsl));
1067     prerr_endline (string_of_int (List.length expansionsr));
1068     List.map (build_newgoal context goal Utils.Right Equality.SuperpositionLeft) expansionsl
1069     @
1070     List.map (build_newgoal context goal Utils.Left Equality.SuperpositionLeft) expansionsr
1071
1072   else
1073     let big,small,possmall =
1074       match c with Utils.Gt -> l,r,Utils.Right | _ -> r,l,Utils.Left
1075     in
1076     let expansions, _ = betaexpand_term menv context ugraph table 0 big in
1077     List.map (build_newgoal context goal possmall Equality.SuperpositionLeft) expansions
1078 ;;
1079
1080 (** demodulation, when the target is a goal *)
1081 let rec demodulation_goal env table goal =
1082   let goalproof,menv,_,_,left,right = open_goal goal in
1083   let _, context, ugraph = env in
1084 (*  let term = Utils.guarded_simpl (~debug:true) context term in*)
1085   let do_right () =
1086       let resright = demodulation_aux menv context ugraph table 0 right in
1087       match resright with
1088       | Some t ->
1089           let newg =
1090             build_newgoal context goal Utils.Left Equality.Demodulation t
1091           in
1092           if goal_metaconvertibility_eq goal newg then
1093             false, goal
1094           else
1095             true, snd (demodulation_goal env table newg)
1096       | None -> false, goal
1097   in
1098   let resleft = demodulation_aux menv context ugraph table 0 left in
1099   match resleft with
1100   | Some t ->
1101       let newg = build_newgoal context goal Utils.Right Equality.Demodulation t in
1102       if goal_metaconvertibility_eq goal newg then
1103         do_right ()
1104       else
1105         true, snd (demodulation_goal env table newg)
1106   | None -> do_right ()
1107 ;;
1108
1109 let get_stats () = <:show<Indexing.>> ;;