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 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         (*
 591           prerr_endline ("demodulation_eq:\n");
 592         Index.iter table (fun l ->
 593           let l = Index.PosEqSet.elements l in
 594           let l =
 595             List.map (fun (p,e) ->
 596               Utils.string_of_pos p ^ Equality.string_of_equality e) l in
 597           prerr_endline (String.concat "\n" l)
 598           );
 599           *)
 600   let module C = Cic in
 601   let module S = CicSubstitution in
 602   let module M = CicMetaSubst in
 603   let module HL = HelmLibraryObjects in
 604   let module U = Utils in
 605   let metasenv, context, ugraph = env in
 606   let w, proof, (eq_ty, left, right, order), metas, id =
 607     Equality.open_equality target
 608   in
 609   (* first, we simplify *)
 610 (*   let right = U.guarded_simpl context right in *)
 611 (*   let left = U.guarded_simpl context left in *)
 612 (*   let order = !Utils.compare_terms left right in *)
 613 (*   let stat = (eq_ty, left, right, order) in  *)
 614 (*  let w = Utils.compute_equality_weight stat in*)
 615   (* let target = Equality.mk_equality (w, proof, stat, metas) in *)
 616   if Utils.debug_metas then
 617     ignore(check_target bag context target "demod equalities input");
 618   let metasenv' = (* metasenv @ *) metas in
 619   let maxmeta = ref newmeta in
 620
 621   let build_newtarget is_left (t, subst, menv, ug, eq_found) =
 622
 623     if Utils.debug_metas then
 624       begin
 625         ignore(check_for_duplicates menv "input1");
 626         ignore(check_disjoint_invariant subst menv "input2");
 627         let substs = Subst.ppsubst subst in
 628         ignore(check_target bag context (snd eq_found) ("input3" ^ substs))
 629       end;
 630     let pos, equality = eq_found in
 631     let (_, proof',
 632         (ty, what, other, _), menv',id') = Equality.open_equality equality in
 633     let ty =
 634       try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
 635       with CicUtil.Meta_not_found _ -> ty
 636     in
 637     let ty, eq_ty = apply_subst subst ty, apply_subst subst eq_ty in
 638     let what, other = if pos = Utils.Left then what, other else other, what in
 639     let newterm, newproof =
 640       let bo =
 641         Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
 642 (*      let name = C.Name ("x_Demod" ^ (string_of_int !demod_counter)) in*)
 643       let name = C.Name "x" in
 644       let bo' =
 645         let l, r = if is_left then t, S.lift 1 right else S.lift 1 left, t in
 646           C.Appl [C.MutInd (eq_uri, 0, []); S.lift 1 eq_ty; l; r]
 647       in
 648           (bo, (Equality.Step (subst,(Equality.Demodulation, id,(pos,id'),
 649           (Cic.Lambda (name, ty, bo'))))))
 650     in
 651     let newmenv = menv in
 652     let left, right = if is_left then newterm, right else left, newterm in
 653     let ordering = !Utils.compare_terms left right in
 654     let stat = (eq_ty, left, right, ordering) in
 655     let res =
 656       let w = Utils.compute_equality_weight stat in
 657           (Equality.mk_equality bag (w, newproof, stat,newmenv))
 658     in
 659     if Utils.debug_metas then
 660       ignore(check_target bag context res "buildnew_target output");
 661     !maxmeta, res
 662   in
 663
 664   let res =
 665     demodulation_aux bag ~from:"3" metasenv' context ugraph table 0 left
 666   in
 667   if Utils.debug_res then check_res res "demod result";
 668   let newmeta, newtarget =
 669     match res with
 670     | Some t ->
 671         let newmeta, newtarget = build_newtarget true t in
 672           (* assert (not (Equality.meta_convertibility_eq target newtarget)); *)
 673           if (Equality.is_weak_identity newtarget) (* || *)
 674             (*Equality.meta_convertibility_eq target newtarget*) then
 675               newmeta, newtarget
 676           else
 677             demodulation_equality bag ?from eq_uri newmeta env table newtarget
 678     | None ->
 679         let res = demodulation_aux bag metasenv' context ugraph table 0 right in
 680         if Utils.debug_res then check_res res "demod result 1";
 681           match res with
 682           | Some t ->
 683               let newmeta, newtarget = build_newtarget false t in
 684                 if (Equality.is_weak_identity newtarget) ||
 685                   (Equality.meta_convertibility_eq target newtarget) then
 686                     newmeta, newtarget
 687                 else
 688                    demodulation_equality bag ?from eq_uri newmeta env table newtarget
 689           | None ->
 690               newmeta, target
 691   in
 692   (* newmeta, newtarget *)
 693   newmeta,newtarget
 694 ;;
 695
 696 (**
 697    Performs the beta expansion of the term "term" w.r.t. "table",
 698    i.e. returns the list of all the terms t s.t. "(t term) = t2", for some t2
 699    in table.
 700 *)
 701 let rec betaexpand_term
 702   ?(subterms_only=false) metasenv context ugraph table lift_amount term
 703 =
 704   let module C = Cic in
 705   let module S = CicSubstitution in
 706   let module M = CicMetaSubst in
 707   let module HL = HelmLibraryObjects in
 708
 709   let res, lifted_term =
 710     match term with
 711     | C.Meta (i, l) ->
 712         let l = [] in
 713         let l', lifted_l =
 714           List.fold_right
 715             (fun arg (res, lifted_tl) ->
 716                match arg with
 717                | Some arg ->
 718                    let arg_res, lifted_arg =
 719                      betaexpand_term metasenv context ugraph table
 720                        lift_amount arg in
 721                    let l1 =
 722                      List.map
 723                        (fun (t, s, m, ug, eq_found) ->
 724                           (Some t)::lifted_tl, s, m, ug, eq_found)
 725                        arg_res
 726                    in
 727                    (l1 @
 728                       (List.map
 729                          (fun (l, s, m, ug, eq_found) ->
 730                             (Some lifted_arg)::l, s, m, ug, eq_found)
 731                          res),
 732                     (Some lifted_arg)::lifted_tl)
 733                | None ->
 734                    (List.map
 735                       (fun (r, s, m, ug, eq_found) ->
 736                          None::r, s, m, ug, eq_found) res,
 737                     None::lifted_tl)
 738             ) l ([], [])
 739         in
 740         let e =
 741           List.map
 742             (fun (l, s, m, ug, eq_found) ->
 743                (C.Meta (i, l), s, m, ug, eq_found)) l'
 744         in
 745         e, C.Meta (i, lifted_l)
 746
 747     | C.Rel m ->
 748         [], if m <= lift_amount then C.Rel m else C.Rel (m+1)
 749
 750     | C.Prod (nn, s, t) ->
 751         let l1, lifted_s =
 752           betaexpand_term metasenv context ugraph table lift_amount s in
 753         let l2, lifted_t =
 754           betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
 755             table (lift_amount+1) t in
 756         let l1' =
 757           List.map
 758             (fun (t, s, m, ug, eq_found) ->
 759                C.Prod (nn, t, lifted_t), s, m, ug, eq_found) l1
 760         and l2' =
 761           List.map
 762             (fun (t, s, m, ug, eq_found) ->
 763                C.Prod (nn, lifted_s, t), s, m, ug, eq_found) l2 in
 764         l1' @ l2', C.Prod (nn, lifted_s, lifted_t)
 765
 766     | C.Lambda (nn, s, t) ->
 767         let l1, lifted_s =
 768           betaexpand_term metasenv context ugraph table lift_amount s in
 769         let l2, lifted_t =
 770           betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
 771             table (lift_amount+1) t in
 772         let l1' =
 773           List.map
 774             (fun (t, s, m, ug, eq_found) ->
 775                C.Lambda (nn, t, lifted_t), s, m, ug, eq_found) l1
 776         and l2' =
 777           List.map
 778             (fun (t, s, m, ug, eq_found) ->
 779                C.Lambda (nn, lifted_s, t), s, m, ug, eq_found) l2 in
 780         l1' @ l2', C.Lambda (nn, lifted_s, lifted_t)
 781
 782     | C.Appl l ->
 783         let l', lifted_l =
 784           List.fold_left
 785             (fun (res, lifted_tl) arg ->
 786                let arg_res, lifted_arg =
 787                  betaexpand_term metasenv context ugraph table lift_amount arg
 788                in
 789                let l1 =
 790                  List.map
 791                    (fun (a, s, m, ug, eq_found) ->
 792                       a::lifted_tl, s, m, ug, eq_found)
 793                    arg_res
 794                in
 795                (l1 @
 796                   (List.map
 797                      (fun (r, s, m, ug, eq_found) ->
 798                         lifted_arg::r, s, m, ug, eq_found)
 799                      res),
 800                 lifted_arg::lifted_tl)
 801             ) ([], []) (List.rev l)
 802         in
 803         (List.map
 804            (fun (l, s, m, ug, eq_found) -> (C.Appl l, s, m, ug, eq_found)) l',
 805          C.Appl lifted_l)
 806
 807     | t -> [], (S.lift lift_amount t)
 808   in
 809   match term with
 810   | C.Meta (i, l) -> res, lifted_term
 811   | term ->
 812       let termty, ugraph =
 813         C.Implicit None, ugraph
 814 (*         CicTypeChecker.type_of_aux' metasenv context term ugraph *)
 815       in
 816       let candidates = get_candidates Unification table term in
 817       let r =
 818         if subterms_only then
 819           []
 820         else
 821           find_all_matches
 822             metasenv context ugraph lift_amount term termty candidates
 823       in
 824       r @ res, lifted_term
 825 ;;
 826
 827 (**
 828    superposition_right
 829    returns a list of new clauses inferred with a right superposition step
 830    between the positive equation "target" and one in the "table" "newmeta" is
 831    the first free meta index, i.e. the first number above the highest meta
 832    index: its updated value is also returned
 833 *)
 834 let superposition_right bag
 835   ?(subterms_only=false) eq_uri newmeta (metasenv, context, ugraph) table target=
 836   let module C = Cic in
 837   let module S = CicSubstitution in
 838   let module M = CicMetaSubst in
 839   let module HL = HelmLibraryObjects in
 840   let module CR = CicReduction in
 841   let module U = Utils in
 842   let w, eqproof, (eq_ty, left, right, ordering), newmetas,id =
 843     Equality.open_equality target
 844   in
 845   if Utils.debug_metas then
 846     ignore (check_target bag context target "superpositionright");
 847   let metasenv' = newmetas in
 848   let maxmeta = ref newmeta in
 849   let res1, res2 =
 850     match ordering with
 851     | U.Gt ->
 852         fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 left), []
 853     | U.Lt ->
 854         [], fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 right)
 855     | _ ->
 856         let res l r =
 857           List.filter
 858             (fun (_, subst, _, _, _) ->
 859                let subst = apply_subst subst in
 860                let o = !Utils.compare_terms (subst l) (subst r) in
 861                o <> U.Lt && o <> U.Le)
 862             (fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 l))
 863         in
 864         (res left right), (res right left)
 865   in
 866   let build_new ordering (bo, s, m, ug, eq_found) =
 867     if Utils.debug_metas then
 868       ignore (check_target bag context (snd eq_found) "buildnew1" );
 869
 870     let pos, equality =  eq_found in
 871     let (_, proof', (ty, what, other, _), menv',id') =
 872       Equality.open_equality  equality in
 873     let what, other = if pos = Utils.Left then what, other else other, what in
 874
 875     let ty, eq_ty = apply_subst s ty, apply_subst s eq_ty in
 876     let newgoal, newproof =
 877       (* qua *)
 878       let bo' =
 879         Utils.guarded_simpl context (apply_subst s (S.subst other bo))
 880       in
 881       let name = C.Name "x" in
 882       let bo'' =
 883         let l, r =
 884           if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
 885         C.Appl [C.MutInd (eq_uri, 0, []); S.lift 1 eq_ty; l; r]
 886       in
 887       bo',
 888         Equality.Step
 889           (s,(Equality.SuperpositionRight,
 890                id,(pos,id'),(Cic.Lambda(name,ty,bo''))))
 891     in
 892     let newmeta, newequality =
 893       let left, right =
 894         if ordering = U.Gt then newgoal, apply_subst s right
 895         else apply_subst s left, newgoal in
 896       let neworder = !Utils.compare_terms left right in
 897       let newmenv = (* Founif.filter s *) m in
 898       let stat = (eq_ty, left, right, neworder) in
 899       let eq' =
 900         let w = Utils.compute_equality_weight stat in
 901         Equality.mk_equality bag (w, newproof, stat, newmenv) in
 902       if Utils.debug_metas then
 903         ignore (check_target bag context eq' "buildnew3");
 904       let newm, eq' = Equality.fix_metas bag !maxmeta eq' in
 905       if Utils.debug_metas then
 906         ignore (check_target bag context eq' "buildnew4");
 907       newm, eq'
 908     in
 909     maxmeta := newmeta;
 910     if Utils.debug_metas then
 911       ignore(check_target bag context newequality "buildnew2");
 912     newequality
 913   in
 914   let new1 = List.map (build_new U.Gt) res1
 915   and new2 = List.map (build_new U.Lt) res2 in
 916   let ok e = not (Equality.is_identity (metasenv', context, ugraph) e) in
 917   (!maxmeta,
 918    (List.filter ok (new1 @ new2)))
 919 ;;
 920
 921 (** demodulation, when the target is a theorem *)
 922 let rec demodulation_theorem bag env table theorem =
 923   let module C = Cic in
 924   let module S = CicSubstitution in
 925   let module M = CicMetaSubst in
 926   let module HL = HelmLibraryObjects in
 927   let eq_uri =
 928     match LibraryObjects.eq_URI() with
 929     | Some u -> u
 930     | None -> assert false in
 931   let metasenv, context, ugraph = env in
 932   let proof, theo, metas = theorem in
 933   let build_newtheorem (t, subst, menv, ug, eq_found) =
 934     let pos, equality = eq_found in
 935     let (_, proof', (ty, what, other, _), menv',id) =
 936       Equality.open_equality equality in
 937     let peq =
 938       match proof' with
 939       | Equality.Exact p -> p
 940       | _ -> assert false in
 941     let what, other =
 942       if pos = Utils.Left then what, other else other, what in
 943     let newtheo = apply_subst subst (S.subst other t) in
 944     let name = C.Name "x" in
 945     let body = apply_subst subst t in
 946     let pred = C.Lambda(name,ty,body) in
 947     let newproof =
 948       match pos with
 949         | Utils.Left ->
 950           Equality.mk_eq_ind eq_uri ty what pred proof other peq
 951         | Utils.Right ->
 952           Equality.mk_eq_ind eq_uri ty what pred proof other peq
 953     in
 954     newproof,newtheo
 955   in
 956   let res = demodulation_aux bag metas context ugraph table 0 theo in
 957   match res with
 958   | Some t ->
 959       let newproof, newtheo = build_newtheorem t in
 960       if Equality.meta_convertibility theo newtheo then
 961         newproof, newtheo
 962       else
 963         demodulation_theorem bag env table (newproof,newtheo,[])
 964   | None ->
 965       proof,theo
 966 ;;
 967
 968 (*****************************************************************************)
 969 (**                         OPERATIONS ON GOALS                             **)
 970 (**                                                                         **)
 971 (**                DEMODULATION_GOAL & SUPERPOSITION_LEFT                   **)
 972 (*****************************************************************************)
 973
 974 let open_goal g =
 975   match g with
 976   | (proof,menv,Cic.Appl[(Cic.MutInd(uri,0,_)) as eq;ty;l;r]) ->
 977       (* assert (LibraryObjects.is_eq_URI uri); *)
 978       proof,menv,eq,ty,l,r
 979   | _ -> assert false
 980 ;;
 981
 982 let ty_of_goal (_,_,ty) = ty ;;
 983
 984 (* checks if two goals are metaconvertible *)
 985 let goal_metaconvertibility_eq g1 g2 =
 986   Equality.meta_convertibility (ty_of_goal g1) (ty_of_goal g2)
 987 ;;
 988
 989 (* when the betaexpand_term function is called on the left/right side of the
 990  * goal, the predicate has to be fixed
 991  * C[x] ---> (eq ty unchanged C[x])
 992  * [posu] is the side of the [unchanged] term in the original goal
 993  *)
 994 let fix_expansion goal posu (t, subst, menv, ug, eq_f) =
 995   let _,_,eq,ty,l,r = open_goal goal in
 996   let unchanged = if posu = Utils.Left then l else r in
 997   let unchanged = CicSubstitution.lift 1 unchanged in
 998   let ty = CicSubstitution.lift 1 ty in
 999   let pred =
1000     match posu with
1001     | Utils.Left -> Cic.Appl [eq;ty;unchanged;t]
1002     | Utils.Right -> Cic.Appl [eq;ty;t;unchanged]
1003   in
1004   (pred, subst, menv, ug, eq_f)
1005 ;;
1006
1007 (* ginve the old [goal], the side that has not changed [posu] and the
1008  * expansion builds a new goal *)
1009 let build_newgoal bag context goal posu rule expansion =
1010   let goalproof,_,_,_,_,_ = open_goal goal in
1011   let (t,subst,menv,ug,eq_found) = fix_expansion goal posu expansion in
1012   let pos, equality = eq_found in
1013   let (_, proof', (ty, what, other, _), menv',id) =
1014     Equality.open_equality equality in
1015   let what, other = if pos = Utils.Left then what, other else other, what in
1016   let newterm, newgoalproof =
1017     let bo =
1018       Utils.guarded_simpl context
1019         (apply_subst subst (CicSubstitution.subst other t))
1020     in
1021     let bo' = apply_subst subst t in
1022     let ty = apply_subst subst ty in
1023     let name = Cic.Name "x" in
1024     let newgoalproofstep = (rule,pos,id,subst,Cic.Lambda (name,ty,bo')) in
1025     bo, (newgoalproofstep::goalproof)
1026   in
1027   let newmetasenv = (* Founif.filter subst *) menv in
1028   (newgoalproof, newmetasenv, newterm)
1029 ;;
1030
1031 (**
1032    superposition_left
1033    returns a list of new clauses inferred with a left superposition step
1034    the negative equation "target" and one of the positive equations in "table"
1035 *)
1036 let superposition_left bag (metasenv, context, ugraph) table goal maxmeta =
1037   let names = Utils.names_of_context context in
1038   let proof,menv,eq,ty,l,r = open_goal goal in
1039   let c = !Utils.compare_terms l r in
1040   let newgoals =
1041     if c = Utils.Incomparable then
1042       begin
1043       let expansionsl, _ = betaexpand_term menv context ugraph table 0 l in
1044       let expansionsr, _ = betaexpand_term menv context ugraph table 0 r in
1045       (* prerr_endline "incomparable";
1046       prerr_endline (string_of_int (List.length expansionsl));
1047       prerr_endline (string_of_int (List.length expansionsr));
1048       *)
1049       List.map (build_newgoal bag context goal Utils.Right Equality.SuperpositionLeft) expansionsl
1050       @
1051       List.map (build_newgoal bag context goal Utils.Left Equality.SuperpositionLeft) expansionsr
1052       end
1053     else
1054         match c with
1055         | Utils.Gt -> (* prerr_endline "GT"; *)
1056             let big,small,possmall = l,r,Utils.Right in
1057             let expansions, _ = betaexpand_term menv context ugraph table 0 big in
1058             List.map
1059               (build_newgoal bag context goal possmall Equality.SuperpositionLeft)
1060               expansions
1061         | Utils.Lt -> (* prerr_endline "LT"; *)
1062             let big,small,possmall = r,l,Utils.Left in
1063             let expansions, _ = betaexpand_term menv context ugraph table 0 big in
1064             List.map
1065               (build_newgoal bag context goal possmall Equality.SuperpositionLeft)
1066               expansions
1067         | Utils.Eq -> []
1068         | _ ->
1069             prerr_endline
1070               ("NOT GT, LT NOR EQ : "^CicPp.pp l names^" - "^CicPp.pp r names);
1071             assert false
1072   in
1073   (* rinfresco le meta *)
1074   List.fold_right
1075     (fun g (max,acc) ->
1076        let max,g = Equality.fix_metas_goal max g in max,g::acc)
1077     newgoals (maxmeta,[])
1078 ;;
1079
1080 (** demodulation, when the target is a goal *)
1081 let rec demodulation_goal bag env table goal =
1082   let goalproof,menv,_,_,left,right = open_goal goal in
1083   let _, context, ugraph = env in
1084 (*  let term = Utils.guarded_simpl (~debug:true) context term in*)
1085   let do_right () =
1086       let resright = demodulation_aux bag menv context ugraph table 0 right in
1087       match resright with
1088       | Some t ->
1089           let newg =
1090             build_newgoal bag context goal Utils.Left Equality.Demodulation t
1091           in
1092           if goal_metaconvertibility_eq goal newg then
1093             false, goal
1094           else
1095             true, snd (demodulation_goal bag env table newg)
1096       | None -> false, goal
1097   in
1098   let resleft = demodulation_aux bag menv context ugraph table 0 left in
1099   match resleft with
1100   | Some t ->
1101       let newg = build_newgoal bag context goal Utils.Right Equality.Demodulation t in
1102       if goal_metaconvertibility_eq goal newg then
1103         do_right ()
1104       else
1105         true, snd (demodulation_goal bag env table newg)
1106   | None -> do_right ()
1107 ;;
1108
1109 type next = L | R
1110 type solved = Yes of Equality.goal | No of Equality.goal list
1111
1112 (* returns all the 1 step demodulations *)
1113 module C = Cic;;
1114 module S = CicSubstitution;;
1115 let rec demodulation_all_aux
1116   metasenv context ugraph table lift_amount term
1117 =
1118   let candidates =
1119     get_candidates ~env:(metasenv,context,ugraph) Matching table term
1120   in
1121   match term with
1122   | C.Meta _ -> []
1123   | _ ->
1124       let termty, ugraph = C.Implicit None, ugraph in
1125       let res =
1126         find_all_matches
1127           metasenv context ugraph lift_amount term termty candidates
1128       in
1129       match term with
1130       | C.Appl l ->
1131          let res, _, _ =
1132            List.fold_left
1133             (fun (res,l,r) t ->
1134                res @
1135                List.map
1136                  (fun (rel, s, m, ug, c) ->
1137                    (Cic.Appl (l@[rel]@List.tl r), s, m, ug, c))
1138                  (demodulation_all_aux
1139                    metasenv context ugraph table lift_amount t),
1140                l@[List.hd r], List.tl r)
1141             (res, [], List.map (S.lift 1) l) l
1142          in
1143          res
1144       | C.Prod (nn, s, t)
1145       | C.Lambda (nn, s, t) ->
1146           let context = (Some (nn, C.Decl s))::context in
1147           let mk s t =
1148             match term with
1149             | Cic.Prod _ -> Cic.Prod (nn,s,t) | _ -> Cic.Lambda (nn,s,t)
1150           in
1151           res @
1152           List.map
1153             (fun (rel, subst, m, ug, c) ->
1154                mk (S.lift 1 s) rel, subst, m, ug, c)
1155             (demodulation_all_aux
1156               metasenv context ugraph table (lift_amount+1) t)
1157               (* we could demodulate also in s, but then t may be badly
1158                * typed... *)
1159       | t -> res
1160 ;;
1161
1162 let solve_demodulating bag env table initgoal steps =
1163   let _, context, ugraph = env in
1164   let solved goal res side =
1165     let newg = build_newgoal bag context goal side Equality.Demodulation res in
1166     match newg with
1167     | (goalproof,m,Cic.Appl[Cic.MutInd(uri,n,ens);eq_ty;left;right])
1168       when LibraryObjects.is_eq_URI uri ->
1169         (try
1170           let _ =
1171             Founif.unification m m context left right CicUniv.empty_ugraph
1172           in
1173           Yes newg
1174         with CicUnification.UnificationFailure _ -> No [newg])
1175     | _ -> No [newg]
1176   in
1177   let solved goal res_list side =
1178     let newg = List.map (fun x -> solved goal x side) res_list in
1179     try
1180       List.find (function Yes _ -> true | _ -> false) newg
1181     with Not_found ->
1182       No (List.flatten (List.map (function No s -> s | _-> assert false) newg))
1183   in
1184   let rec first f l =
1185     match l with
1186     | [] -> None
1187     | x::tl ->
1188        match f x with
1189        | None -> first f tl
1190        | Some x as ok -> ok
1191   in
1192   let rec aux steps next goal =
1193     if steps = 0 then None else
1194     let goalproof,menv,_,_,left,right = open_goal goal in
1195     let do_step t =
1196       demodulation_all_aux menv context ugraph table 0 t
1197     in
1198     match next with
1199     | L ->
1200         (match do_step left with
1201         | _::_ as res ->
1202             (match solved goal res Utils.Right with
1203             | No newgoals ->
1204                  (match first (aux (steps - 1) L) newgoals with
1205                  | Some g as success -> success
1206                  | None -> aux steps R goal)
1207             | Yes newgoal -> Some newgoal)
1208         | [] -> aux steps R goal)
1209     | R ->
1210         (match do_step right with
1211         | _::_ as res ->
1212             (match solved goal res Utils.Left with
1213             | No newgoals ->
1214                  (match first (aux (steps - 1) L) newgoals with
1215                  | Some g as success -> success
1216                  | None -> None)
1217             | Yes newgoal -> Some newgoal)
1218         | [] -> None)
1219   in
1220   aux steps L initgoal
1221 ;;
1222
1223 let get_stats () = "" ;;