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 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 ty, eq_ty = apply_subst subst ty, apply_subst subst eq_ty in
 625     let what, other = if pos = Utils.Left then what, other else other, what in
 626     let newterm, newproof =
 627       let bo =
 628         Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
 629 (*      let name = C.Name ("x_Demod" ^ (string_of_int !demod_counter)) in*)
 630       let name = C.Name "x" in
 631       let bo' =
 632         let l, r = if is_left then t, S.lift 1 right else S.lift 1 left, t in
 633           C.Appl [C.MutInd (eq_uri, 0, []); S.lift 1 eq_ty; l; r]
 634       in
 635           (bo, (Equality.Step (subst,(Equality.Demodulation, id,(pos,id'),
 636           (Cic.Lambda (name, ty, bo'))))))
 637     in
 638     let newmenv = menv in
 639     let left, right = if is_left then newterm, right else left, newterm in
 640     let ordering = !Utils.compare_terms left right in
 641     let stat = (eq_ty, left, right, ordering) in
 642     let res =
 643       let w = Utils.compute_equality_weight stat in
 644           (Equality.mk_equality bag (w, newproof, stat,newmenv))
 645     in
 646     if Utils.debug_metas then
 647       ignore(check_target bag context res "buildnew_target output");
 648     !maxmeta, res
 649   in
 650
 651   let res =
 652     demodulation_aux bag ~from:"3" metasenv' context ugraph table 0 left
 653   in
 654   if Utils.debug_res then check_res res "demod result";
 655   let newmeta, newtarget =
 656     match res with
 657     | Some t ->
 658         let newmeta, newtarget = build_newtarget true t in
 659           (* assert (not (Equality.meta_convertibility_eq target newtarget)); *)
 660           if (Equality.is_weak_identity newtarget) (* || *)
 661             (*Equality.meta_convertibility_eq target newtarget*) then
 662               newmeta, newtarget
 663           else
 664             demodulation_equality bag ?from eq_uri newmeta env table newtarget
 665     | None ->
 666         let res = demodulation_aux bag metasenv' context ugraph table 0 right in
 667         if Utils.debug_res then check_res res "demod result 1";
 668           match res with
 669           | Some t ->
 670               let newmeta, newtarget = build_newtarget false t in
 671                 if (Equality.is_weak_identity newtarget) ||
 672                   (Equality.meta_convertibility_eq target newtarget) then
 673                     newmeta, newtarget
 674                 else
 675                    demodulation_equality bag ?from eq_uri newmeta env table newtarget
 676           | None ->
 677               newmeta, target
 678   in
 679   (* newmeta, newtarget *)
 680   newmeta,newtarget
 681 ;;
 682
 683 (**
 684    Performs the beta expansion of the term "term" w.r.t. "table",
 685    i.e. returns the list of all the terms t s.t. "(t term) = t2", for some t2
 686    in table.
 687 *)
 688 let rec betaexpand_term
 689   ?(subterms_only=false) metasenv context ugraph table lift_amount term
 690 =
 691   let module C = Cic in
 692   let module S = CicSubstitution in
 693   let module M = CicMetaSubst in
 694   let module HL = HelmLibraryObjects in
 695
 696   let res, lifted_term =
 697     match term with
 698     | C.Meta (i, l) ->
 699         let l = [] in
 700         let l', lifted_l =
 701           List.fold_right
 702             (fun arg (res, lifted_tl) ->
 703                match arg with
 704                | Some arg ->
 705                    let arg_res, lifted_arg =
 706                      betaexpand_term metasenv context ugraph table
 707                        lift_amount arg in
 708                    let l1 =
 709                      List.map
 710                        (fun (t, s, m, ug, eq_found) ->
 711                           (Some t)::lifted_tl, s, m, ug, eq_found)
 712                        arg_res
 713                    in
 714                    (l1 @
 715                       (List.map
 716                          (fun (l, s, m, ug, eq_found) ->
 717                             (Some lifted_arg)::l, s, m, ug, eq_found)
 718                          res),
 719                     (Some lifted_arg)::lifted_tl)
 720                | None ->
 721                    (List.map
 722                       (fun (r, s, m, ug, eq_found) ->
 723                          None::r, s, m, ug, eq_found) res,
 724                     None::lifted_tl)
 725             ) l ([], [])
 726         in
 727         let e =
 728           List.map
 729             (fun (l, s, m, ug, eq_found) ->
 730                (C.Meta (i, l), s, m, ug, eq_found)) l'
 731         in
 732         e, C.Meta (i, lifted_l)
 733
 734     | C.Rel m ->
 735         [], if m <= lift_amount then C.Rel m else C.Rel (m+1)
 736
 737     | C.Prod (nn, s, t) ->
 738         let l1, lifted_s =
 739           betaexpand_term metasenv context ugraph table lift_amount s in
 740         let l2, lifted_t =
 741           betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
 742             table (lift_amount+1) t in
 743         let l1' =
 744           List.map
 745             (fun (t, s, m, ug, eq_found) ->
 746                C.Prod (nn, t, lifted_t), s, m, ug, eq_found) l1
 747         and l2' =
 748           List.map
 749             (fun (t, s, m, ug, eq_found) ->
 750                C.Prod (nn, lifted_s, t), s, m, ug, eq_found) l2 in
 751         l1' @ l2', C.Prod (nn, lifted_s, lifted_t)
 752
 753     | C.Lambda (nn, s, t) ->
 754         let l1, lifted_s =
 755           betaexpand_term metasenv context ugraph table lift_amount s in
 756         let l2, lifted_t =
 757           betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
 758             table (lift_amount+1) t in
 759         let l1' =
 760           List.map
 761             (fun (t, s, m, ug, eq_found) ->
 762                C.Lambda (nn, t, lifted_t), s, m, ug, eq_found) l1
 763         and l2' =
 764           List.map
 765             (fun (t, s, m, ug, eq_found) ->
 766                C.Lambda (nn, lifted_s, t), s, m, ug, eq_found) l2 in
 767         l1' @ l2', C.Lambda (nn, lifted_s, lifted_t)
 768
 769     | C.Appl l ->
 770         let l', lifted_l =
 771           List.fold_left
 772             (fun (res, lifted_tl) arg ->
 773                let arg_res, lifted_arg =
 774                  betaexpand_term metasenv context ugraph table lift_amount arg
 775                in
 776                let l1 =
 777                  List.map
 778                    (fun (a, s, m, ug, eq_found) ->
 779                       a::lifted_tl, s, m, ug, eq_found)
 780                    arg_res
 781                in
 782                (l1 @
 783                   (List.map
 784                      (fun (r, s, m, ug, eq_found) ->
 785                         lifted_arg::r, s, m, ug, eq_found)
 786                      res),
 787                 lifted_arg::lifted_tl)
 788             ) ([], []) (List.rev l)
 789         in
 790         (List.map
 791            (fun (l, s, m, ug, eq_found) -> (C.Appl l, s, m, ug, eq_found)) l',
 792          C.Appl lifted_l)
 793
 794     | t -> [], (S.lift lift_amount t)
 795   in
 796   match term with
 797   | C.Meta (i, l) -> res, lifted_term
 798   | term ->
 799       let termty, ugraph =
 800         C.Implicit None, ugraph
 801 (*         CicTypeChecker.type_of_aux' metasenv context term ugraph *)
 802       in
 803       let candidates = get_candidates Unification table term in
 804       let r =
 805         if subterms_only then
 806           []
 807         else
 808           find_all_matches
 809             metasenv context ugraph lift_amount term termty candidates
 810       in
 811       r @ res, lifted_term
 812 ;;
 813
 814 (**
 815    superposition_right
 816    returns a list of new clauses inferred with a right superposition step
 817    between the positive equation "target" and one in the "table" "newmeta" is
 818    the first free meta index, i.e. the first number above the highest meta
 819    index: its updated value is also returned
 820 *)
 821 let superposition_right bag
 822   ?(subterms_only=false) eq_uri newmeta (metasenv, context, ugraph) table target=
 823   let module C = Cic in
 824   let module S = CicSubstitution in
 825   let module M = CicMetaSubst in
 826   let module HL = HelmLibraryObjects in
 827   let module CR = CicReduction in
 828   let module U = Utils in
 829   let w, eqproof, (eq_ty, left, right, ordering), newmetas,id =
 830     Equality.open_equality target
 831   in
 832   if Utils.debug_metas then
 833     ignore (check_target bag context target "superpositionright");
 834   let metasenv' = newmetas in
 835   let maxmeta = ref newmeta in
 836   let res1, res2 =
 837     match ordering with
 838     | U.Gt ->
 839         fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 left), []
 840     | U.Lt ->
 841         [], fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 right)
 842     | _ ->
 843         let res l r =
 844           List.filter
 845             (fun (_, subst, _, _, _) ->
 846                let subst = apply_subst subst in
 847                let o = !Utils.compare_terms (subst l) (subst r) in
 848                o <> U.Lt && o <> U.Le)
 849             (fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 l))
 850         in
 851         (res left right), (res right left)
 852   in
 853   let build_new ordering (bo, s, m, ug, eq_found) =
 854     if Utils.debug_metas then
 855       ignore (check_target bag context (snd eq_found) "buildnew1" );
 856
 857     let pos, equality =  eq_found in
 858     let (_, proof', (ty, what, other, _), menv',id') =
 859       Equality.open_equality  equality in
 860     let what, other = if pos = Utils.Left then what, other else other, what in
 861
 862     let ty, eq_ty = apply_subst s ty, apply_subst s eq_ty in
 863     let newgoal, newproof =
 864       (* qua *)
 865       let bo' =
 866         Utils.guarded_simpl context (apply_subst s (S.subst other bo))
 867       in
 868       let name = C.Name "x" in
 869       let bo'' =
 870         let l, r =
 871           if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
 872         C.Appl [C.MutInd (eq_uri, 0, []); S.lift 1 eq_ty; l; r]
 873       in
 874       bo',
 875         Equality.Step
 876           (s,(Equality.SuperpositionRight,
 877                id,(pos,id'),(Cic.Lambda(name,ty,bo''))))
 878     in
 879     let newmeta, newequality =
 880       let left, right =
 881         if ordering = U.Gt then newgoal, apply_subst s right
 882         else apply_subst s left, newgoal in
 883       let neworder = !Utils.compare_terms left right in
 884       let newmenv = (* Founif.filter s *) m in
 885       let stat = (eq_ty, left, right, neworder) in
 886       let eq' =
 887         let w = Utils.compute_equality_weight stat in
 888         Equality.mk_equality bag (w, newproof, stat, newmenv) in
 889       if Utils.debug_metas then
 890         ignore (check_target bag context eq' "buildnew3");
 891       let newm, eq' = Equality.fix_metas bag !maxmeta eq' in
 892       if Utils.debug_metas then
 893         ignore (check_target bag context eq' "buildnew4");
 894       newm, eq'
 895     in
 896     maxmeta := newmeta;
 897     if Utils.debug_metas then
 898       ignore(check_target bag context newequality "buildnew2");
 899     newequality
 900   in
 901   let new1 = List.map (build_new U.Gt) res1
 902   and new2 = List.map (build_new U.Lt) res2 in
 903   let ok e = not (Equality.is_identity (metasenv', context, ugraph) e) in
 904   (!maxmeta,
 905    (List.filter ok (new1 @ new2)))
 906 ;;
 907
 908 (** demodulation, when the target is a theorem *)
 909 let rec demodulation_theorem bag newmeta env table theorem =
 910   let module C = Cic in
 911   let module S = CicSubstitution in
 912   let module M = CicMetaSubst in
 913   let module HL = HelmLibraryObjects in
 914   let metasenv, context, ugraph = env in
 915   let maxmeta = ref newmeta in
 916   let term, termty, metas = theorem in
 917   let metasenv' = metas in
 918
 919   let build_newtheorem (t, subst, menv, ug, eq_found) =
 920     let pos, equality = eq_found in
 921     let (_, proof', (ty, what, other, _), menv',id) =
 922       Equality.open_equality equality in
 923     let what, other = if pos = Utils.Left then what, other else other, what in
 924     let newterm, newty =
 925       let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
 926 (*      let bo' = apply_subst subst t in *)
 927 (*      let name = C.Name ("x_DemodThm_" ^ (string_of_int !demod_counter)) in*)
 928 (*
 929       let newproofold =
 930         Equality.ProofBlock (subst, eq_URI, (name, ty), bo', eq_found,
 931                               Equality.BasicProof (Equality.empty_subst,term))
 932       in
 933       (Equality.build_proof_term_old newproofold, bo)
 934 *)
 935       (* TODO, not ported to the new proofs *)
 936       if true then assert false; term, bo
 937     in
 938     !maxmeta, (newterm, newty, menv)
 939   in
 940   let res =
 941     demodulation_aux bag (* ~typecheck:true *) metasenv' context ugraph table 0 termty
 942   in
 943   match res with
 944   | Some t ->
 945       let newmeta, newthm = build_newtheorem t in
 946       let newt, newty, _ = newthm in
 947       if Equality.meta_convertibility termty newty then
 948         newmeta, newthm
 949       else
 950         demodulation_theorem bag newmeta env table newthm
 951   | None ->
 952       newmeta, theorem
 953 ;;
 954
 955 (*****************************************************************************)
 956 (**                         OPERATIONS ON GOALS                             **)
 957 (**                                                                         **)
 958 (**                DEMODULATION_GOAL & SUPERPOSITION_LEFT                   **)
 959 (*****************************************************************************)
 960
 961 let open_goal g =
 962   match g with
 963   | (proof,menv,Cic.Appl[(Cic.MutInd(uri,0,_)) as eq;ty;l;r]) ->
 964       (* assert (LibraryObjects.is_eq_URI uri); *)
 965       proof,menv,eq,ty,l,r
 966   | _ -> assert false
 967 ;;
 968
 969 let ty_of_goal (_,_,ty) = ty ;;
 970
 971 (* checks if two goals are metaconvertible *)
 972 let goal_metaconvertibility_eq g1 g2 =
 973   Equality.meta_convertibility (ty_of_goal g1) (ty_of_goal g2)
 974 ;;
 975
 976 (* when the betaexpand_term function is called on the left/right side of the
 977  * goal, the predicate has to be fixed
 978  * C[x] ---> (eq ty unchanged C[x])
 979  * [posu] is the side of the [unchanged] term in the original goal
 980  *)
 981 let fix_expansion goal posu (t, subst, menv, ug, eq_f) =
 982   let _,_,eq,ty,l,r = open_goal goal in
 983   let unchanged = if posu = Utils.Left then l else r in
 984   let unchanged = CicSubstitution.lift 1 unchanged in
 985   let ty = CicSubstitution.lift 1 ty in
 986   let pred =
 987     match posu with
 988     | Utils.Left -> Cic.Appl [eq;ty;unchanged;t]
 989     | Utils.Right -> Cic.Appl [eq;ty;t;unchanged]
 990   in
 991   (pred, subst, menv, ug, eq_f)
 992 ;;
 993
 994 (* ginve the old [goal], the side that has not changed [posu] and the
 995  * expansion builds a new goal *)
 996 let build_newgoal bag context goal posu rule expansion =
 997   let goalproof,_,_,_,_,_ = open_goal goal in
 998   let (t,subst,menv,ug,eq_found) = fix_expansion goal posu expansion in
 999   let pos, equality = eq_found in
1000   let (_, proof', (ty, what, other, _), menv',id) =
1001     Equality.open_equality equality in
1002   let what, other = if pos = Utils.Left then what, other else other, what in
1003   let newterm, newgoalproof =
1004     let bo =
1005       Utils.guarded_simpl context
1006         (apply_subst subst (CicSubstitution.subst other t))
1007     in
1008     let bo' = apply_subst subst 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 () = "" ;;