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