helm/software/components/tactics/paramodulation/indexing.ml

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