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