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