helm/ocaml/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 debug_print = Utils.debug_print;;
  34
  35 (*
  36 for debugging
  37 let check_equation env equation msg =
  38   let w, proof, (eq_ty, left, right, order), metas, args = equation in
  39   let metasenv, context, ugraph = env in
  40   let metasenv' = metasenv @ metas in
  41     try
  42       CicTypeChecker.type_of_aux' metasenv' context left ugraph;
  43       CicTypeChecker.type_of_aux' metasenv' context right ugraph;
  44       ()
  45     with
  46         CicUtil.Meta_not_found _ as exn ->
  47           begin
  48             prerr_endline msg;
  49             prerr_endline (CicPp.ppterm left);
  50             prerr_endline (CicPp.ppterm right);
  51             raise exn
  52           end
  53 *)
  54
  55 type retrieval_mode = Matching | Unification;;
  56
  57 let print_candidates mode term res =
  58   let _ =
  59     match mode with
  60     | Matching ->
  61         Printf.printf "| candidates Matching %s\n" (CicPp.ppterm term)
  62     | Unification ->
  63         Printf.printf "| candidates Unification %s\n" (CicPp.ppterm term)
  64   in
  65   print_endline
  66     (String.concat "\n"
  67        (List.map
  68           (fun (p, e) ->
  69              Printf.sprintf "| (%s, %s)" (Utils.string_of_pos p)
  70                (Inference.string_of_equality e))
  71           res));
  72   print_endline "|";
  73 ;;
  74
  75
  76 let indexing_retrieval_time = ref 0.;;
  77
  78
  79 let apply_subst = CicMetaSubst.apply_subst
  80
  81 let index = Index.index
  82 let remove_index = Index.remove_index
  83 let in_index = Index.in_index
  84 let empty = Index.empty
  85 let init_index = Index.init_index
  86
  87 (* returns a list of all the equalities in the tree that are in relation
  88    "mode" with the given term, where mode can be either Matching or
  89    Unification.
  90
  91    Format of the return value: list of tuples in the form:
  92    (position - Left or Right - of the term that matched the given one in this
  93      equality,
  94     equality found)
  95
  96    Note that if equality is "left = right", if the ordering is left > right,
  97    the position will always be Left, and if the ordering is left < right,
  98    position will be Right.
  99 *)
 100 let get_candidates mode tree term =
 101   let t1 = Unix.gettimeofday () in
 102   let res =
 103     let s =
 104       match mode with
 105       | Matching -> Index.retrieve_generalizations tree term
 106       | Unification -> Index.retrieve_unifiables tree term
 107     in
 108     Index.PosEqSet.elements s
 109   in
 110   (*   print_candidates mode term res; *)
 111 (*   print_endline (Discrimination_tree.string_of_discrimination_tree tree); *)
 112 (*   print_newline (); *)
 113   let t2 = Unix.gettimeofday () in
 114   indexing_retrieval_time := !indexing_retrieval_time +. (t2 -. t1);
 115   res
 116 ;;
 117
 118
 119 let match_unif_time_ok = ref 0.;;
 120 let match_unif_time_no = ref 0.;;
 121
 122
 123 (*
 124   finds the first equality in the index that matches "term", of type "termty"
 125   termty can be Implicit if it is not needed. The result (one of the sides of
 126   the equality, actually) should be not greater (wrt the term ordering) than
 127   term
 128
 129   Format of the return value:
 130
 131   (term to substitute, [Cic.Rel 1 properly lifted - see the various
 132                         build_newtarget functions inside the various
 133                         demodulation_* functions]
 134    substitution used for the matching,
 135    metasenv,
 136    ugraph, [substitution, metasenv and ugraph have the same meaning as those
 137    returned by CicUnification.fo_unif]
 138    (equality where the matching term was found, [i.e. the equality to use as
 139                                                 rewrite rule]
 140     uri [either eq_ind_URI or eq_ind_r_URI, depending on the direction of
 141          the equality: this is used to build the proof term, again see one of
 142          the build_newtarget functions]
 143    ))
 144 *)
 145 let rec find_matches metasenv context ugraph lift_amount term termty =
 146   let module C = Cic in
 147   let module U = Utils in
 148   let module S = CicSubstitution in
 149   let module M = CicMetaSubst in
 150   let module HL = HelmLibraryObjects in
 151   let cmp = !Utils.compare_terms in
 152   let check = match termty with C.Implicit None -> false | _ -> true in
 153   function
 154     | [] -> None
 155     | candidate::tl ->
 156         let pos, (_, proof, (ty, left, right, o), metas, args) = candidate in
 157         if check && not (fst (CicReduction.are_convertible
 158                                 ~metasenv context termty ty ugraph)) then (
 159           find_matches metasenv context ugraph lift_amount term termty tl
 160         ) else
 161           let do_match c eq_URI =
 162             let subst', metasenv', ugraph' =
 163               let t1 = Unix.gettimeofday () in
 164               try
 165                 let r =
 166                   Inference.matching (metasenv @ metas) context
 167                     term (S.lift lift_amount c) ugraph
 168                 in
 169                 let t2 = Unix.gettimeofday () in
 170                 match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
 171                 r
 172               with
 173                 | Inference.MatchingFailure as e ->
 174                 let t2 = Unix.gettimeofday () in
 175                 match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
 176                   raise e
 177                 | CicUtil.Meta_not_found _ as exn ->
 178                     prerr_endline "zurg";
 179                     raise exn
 180             in
 181             Some (C.Rel (1 + lift_amount), subst', metasenv', ugraph',
 182                   (candidate, eq_URI))
 183           in
 184           let c, other, eq_URI =
 185             if pos = Utils.Left then left, right, Utils.eq_ind_URI ()
 186             else right, left, Utils.eq_ind_r_URI ()
 187           in
 188           if o <> U.Incomparable then
 189             try
 190               do_match c eq_URI
 191             with Inference.MatchingFailure ->
 192               find_matches metasenv context ugraph lift_amount term termty tl
 193           else
 194             let res =
 195               try do_match c eq_URI
 196               with Inference.MatchingFailure -> None
 197             in
 198             match res with
 199             | Some (_, s, _, _, _) ->
 200                 let c' = apply_subst s c in
 201                 (*
 202              let other' = U.guarded_simpl context (apply_subst s other) in *)
 203                 let other' = apply_subst s other in
 204                 let order = cmp c' other' in
 205                 if order = U.Gt then
 206                   res
 207                 else
 208                   find_matches
 209                     metasenv context ugraph lift_amount term termty tl
 210             | None ->
 211                 find_matches metasenv context ugraph lift_amount term termty tl
 212 ;;
 213
 214
 215 (*
 216   as above, but finds all the matching equalities, and the matching condition
 217   can be either Inference.matching or Inference.unification
 218 *)
 219 let rec find_all_matches ?(unif_fun=Inference.unification)
 220     metasenv context ugraph lift_amount term termty =
 221   let module C = Cic in
 222   let module U = Utils in
 223   let module S = CicSubstitution in
 224   let module M = CicMetaSubst in
 225   let module HL = HelmLibraryObjects in
 226   let cmp = !Utils.compare_terms in
 227   function
 228     | [] -> []
 229     | candidate::tl ->
 230         let pos, (_, _, (ty, left, right, o), metas, args) = candidate in
 231         let do_match c eq_URI =
 232           let subst', metasenv', ugraph' =
 233             let t1 = Unix.gettimeofday () in
 234             try
 235               let r =
 236                 unif_fun (metasenv @ metas) context
 237                   term (S.lift lift_amount c) ugraph in
 238               let t2 = Unix.gettimeofday () in
 239               match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
 240               r
 241             with
 242             | Inference.MatchingFailure
 243             | CicUnification.UnificationFailure _
 244             | CicUnification.Uncertain _ as e ->
 245                 let t2 = Unix.gettimeofday () in
 246                 match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
 247                 raise e
 248           in
 249           (C.Rel (1 + lift_amount), subst', metasenv', ugraph',
 250            (candidate, eq_URI))
 251         in
 252         let c, other, eq_URI =
 253           if pos = Utils.Left then left, right, Utils.eq_ind_URI ()
 254           else right, left, Utils.eq_ind_r_URI ()
 255         in
 256         if o <> U.Incomparable then
 257           try
 258             let res = do_match c eq_URI in
 259             res::(find_all_matches ~unif_fun metasenv context ugraph
 260                     lift_amount term termty tl)
 261           with
 262           | Inference.MatchingFailure
 263           | CicUnification.UnificationFailure _
 264           | CicUnification.Uncertain _ ->
 265               find_all_matches ~unif_fun metasenv context ugraph
 266                 lift_amount term termty tl
 267         else
 268           try
 269             let res = do_match c eq_URI in
 270             match res with
 271             | _, s, _, _, _ ->
 272                 let c' = apply_subst s c
 273                 and other' = apply_subst s other in
 274                 let order = cmp c' other' in
 275                 if order <> U.Lt && order <> U.Le then
 276                   res::(find_all_matches ~unif_fun metasenv context ugraph
 277                           lift_amount term termty tl)
 278                 else
 279                   find_all_matches ~unif_fun metasenv context ugraph
 280                     lift_amount term termty tl
 281           with
 282           | Inference.MatchingFailure
 283           | CicUnification.UnificationFailure _
 284           | CicUnification.Uncertain _ ->
 285               find_all_matches ~unif_fun metasenv context ugraph
 286                 lift_amount term termty tl
 287 ;;
 288
 289
 290 (*
 291   returns true if target is subsumed by some equality in table
 292 *)
 293 let subsumption env table target =
 294   let _, _, (ty, left, right, _), tmetas, _ = target in
 295   let metasenv, context, ugraph = env in
 296   let metasenv = metasenv @ tmetas in
 297   let samesubst subst subst' =
 298     let tbl = Hashtbl.create (List.length subst) in
 299     List.iter (fun (m, (c, t1, t2)) -> Hashtbl.add tbl m (c, t1, t2)) subst;
 300     List.for_all
 301       (fun (m, (c, t1, t2)) ->
 302          try
 303            let c', t1', t2' = Hashtbl.find tbl m in
 304            if (c = c') && (t1 = t1') && (t2 = t2') then true
 305            else false
 306          with Not_found ->
 307            true)
 308       subst'
 309   in
 310   let leftr =
 311     match left with
 312     | Cic.Meta _ -> []
 313     | _ ->
 314         let leftc = get_candidates Matching table left in
 315         find_all_matches ~unif_fun:Inference.matching
 316           metasenv context ugraph 0 left ty leftc
 317   in
 318   let rec ok what = function
 319     | [] -> false, []
 320     | (_, subst, menv, ug, ((pos, (_, _, (_, l, r, o), m, _)), _))::tl ->
 321         try
 322           let other = if pos = Utils.Left then r else l in
 323           let subst', menv', ug' =
 324             let t1 = Unix.gettimeofday () in
 325             try
 326               let r =
 327                 Inference.matching (metasenv @ menv @ m) context what other ugraph
 328               in
 329               let t2 = Unix.gettimeofday () in
 330               match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
 331               r
 332             with Inference.MatchingFailure as e ->
 333               let t2 = Unix.gettimeofday () in
 334               match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
 335               raise e
 336           in
 337           if samesubst subst subst' then
 338             true, subst
 339           else
 340             ok what tl
 341         with Inference.MatchingFailure ->
 342           ok what tl
 343   in
 344   let r, subst = ok right leftr in
 345   let r, s =
 346     if r then
 347       true, subst
 348     else
 349       let rightr =
 350         match right with
 351           | Cic.Meta _ -> []
 352           | _ ->
 353               let rightc = get_candidates Matching table right in
 354                 find_all_matches ~unif_fun:Inference.matching
 355                   metasenv context ugraph 0 right ty rightc
 356       in
 357         ok left rightr
 358   in
 359 (*     (if r then  *)
 360 (*        debug_print  *)
 361 (*       (lazy *)
 362 (*          (Printf.sprintf "SUBSUMPTION! %s\n%s\n" *)
 363 (*             (Inference.string_of_equality target) (Utils.print_subst s)))); *)
 364     r, s
 365 ;;
 366
 367
 368 let rec demodulation_aux ?(typecheck=false)
 369     metasenv context ugraph table lift_amount term =
 370   (* Printf.eprintf "term = %s\n" (CicPp.ppterm term); *)
 371
 372   let module C = Cic in
 373   let module S = CicSubstitution in
 374   let module M = CicMetaSubst in
 375   let module HL = HelmLibraryObjects in
 376   let candidates = get_candidates Matching table term  in
 377   match term with
 378   | C.Meta _ -> None
 379   | term ->
 380       let termty, ugraph =
 381         if typecheck then
 382           CicTypeChecker.type_of_aux' metasenv context term ugraph
 383         else
 384           C.Implicit None, ugraph
 385       in
 386       let res =
 387         find_matches metasenv context ugraph lift_amount term termty candidates
 388       in
 389       if res <> None then
 390         res
 391       else
 392         match term with
 393         | C.Appl l ->
 394             let res, ll =
 395               List.fold_left
 396                 (fun (res, tl) t ->
 397                    if res <> None then
 398                      (res, tl @ [S.lift 1 t])
 399                    else
 400                      let r =
 401                        demodulation_aux metasenv context ugraph table
 402                          lift_amount t
 403                      in
 404                      match r with
 405                      | None -> (None, tl @ [S.lift 1 t])
 406                      | Some (rel, _, _, _, _) -> (r, tl @ [rel]))
 407                 (None, []) l
 408             in (
 409               match res with
 410               | None -> None
 411               | Some (_, subst, menv, ug, eq_found) ->
 412                   Some (C.Appl ll, subst, menv, ug, eq_found)
 413             )
 414         | C.Prod (nn, s, t) ->
 415             let r1 =
 416               demodulation_aux metasenv context ugraph table lift_amount s in (
 417               match r1 with
 418               | None ->
 419                   let r2 =
 420                     demodulation_aux metasenv
 421                       ((Some (nn, C.Decl s))::context) ugraph
 422                       table (lift_amount+1) t
 423                   in (
 424                     match r2 with
 425                     | None -> None
 426                     | Some (t', subst, menv, ug, eq_found) ->
 427                         Some (C.Prod (nn, (S.lift 1 s), t'),
 428                               subst, menv, ug, eq_found)
 429                   )
 430               | Some (s', subst, menv, ug, eq_found) ->
 431                   Some (C.Prod (nn, s', (S.lift 1 t)),
 432                         subst, menv, ug, eq_found)
 433             )
 434         | C.Lambda (nn, s, t) ->
 435             let r1 =
 436               demodulation_aux metasenv context ugraph table lift_amount s in (
 437               match r1 with
 438               | None ->
 439                   let r2 =
 440                     demodulation_aux metasenv
 441                       ((Some (nn, C.Decl s))::context) ugraph
 442                       table (lift_amount+1) t
 443                   in (
 444                     match r2 with
 445                     | None -> None
 446                     | Some (t', subst, menv, ug, eq_found) ->
 447                         Some (C.Lambda (nn, (S.lift 1 s), t'),
 448                               subst, menv, ug, eq_found)
 449                   )
 450               | Some (s', subst, menv, ug, eq_found) ->
 451                   Some (C.Lambda (nn, s', (S.lift 1 t)),
 452                         subst, menv, ug, eq_found)
 453             )
 454         | t ->
 455             None
 456 ;;
 457
 458
 459 let build_newtarget_time = ref 0.;;
 460
 461
 462 let demod_counter = ref 1;;
 463
 464 (** demodulation, when target is an equality *)
 465 let rec demodulation_equality newmeta env table sign target =
 466   let module C = Cic in
 467   let module S = CicSubstitution in
 468   let module M = CicMetaSubst in
 469   let module HL = HelmLibraryObjects in
 470   let module U = Utils in
 471   let metasenv, context, ugraph = env in
 472   let w, proof, (eq_ty, left, right, order), metas, args = target in
 473   (* first, we simplify *)
 474   let right = U.guarded_simpl context right in
 475   let left = U.guarded_simpl context left in
 476   let w = Utils.compute_equality_weight eq_ty left right in
 477   let order = !Utils.compare_terms left right in
 478   let target = w, proof, (eq_ty, left, right, order), metas, args in
 479
 480   let metasenv' = metasenv @ metas in
 481
 482   let maxmeta = ref newmeta in
 483
 484   let build_newtarget is_left (t, subst, menv, ug, (eq_found, eq_URI)) =
 485     let time1 = Unix.gettimeofday () in
 486
 487     let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
 488     let ty =
 489       try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
 490       with CicUtil.Meta_not_found _ -> ty
 491     in
 492     let what, other = if pos = Utils.Left then what, other else other, what in
 493     let newterm, newproof =
 494       let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
 495       let name = C.Name ("x_Demod_" ^ (string_of_int !demod_counter)) in
 496       incr demod_counter;
 497       let bo' =
 498         let l, r = if is_left then t, S.lift 1 right else S.lift 1 left, t in
 499         C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
 500                 S.lift 1 eq_ty; l; r]
 501       in
 502       if sign = Utils.Positive then
 503         (bo,
 504          Inference.ProofBlock (
 505            subst, eq_URI, (name, ty), bo'(* t' *), eq_found, proof))
 506       else
 507         let metaproof =
 508           incr maxmeta;
 509           let irl =
 510             CicMkImplicit.identity_relocation_list_for_metavariable context in
 511 (*           debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta)); *)
 512 (*           print_newline (); *)
 513           C.Meta (!maxmeta, irl)
 514         in
 515           let eq_found =
 516             let proof' =
 517               let termlist =
 518                 if pos = Utils.Left then [ty; what; other]
 519                 else [ty; other; what]
 520               in
 521               Inference.ProofSymBlock (termlist, proof')
 522             in
 523             let what, other =
 524               if pos = Utils.Left then what, other else other, what
 525             in
 526             pos, (0, proof', (ty, other, what, Utils.Incomparable),
 527                   menv', args')
 528           in
 529           let target_proof =
 530             let pb =
 531               Inference.ProofBlock (subst, eq_URI, (name, ty), bo',
 532                                     eq_found, Inference.BasicProof metaproof)
 533             in
 534             match proof with
 535             | Inference.BasicProof _ ->
 536                 print_endline "replacing a BasicProof";
 537                 pb
 538             | Inference.ProofGoalBlock (_, parent_proof) ->
 539                 print_endline "replacing another ProofGoalBlock";
 540                 Inference.ProofGoalBlock (pb, parent_proof)
 541             | _ -> assert false
 542           in
 543         let refl =
 544           C.Appl [C.MutConstruct (* reflexivity *)
 545                     (LibraryObjects.eq_URI (), 0, 1, []);
 546                   eq_ty; if is_left then right else left]
 547         in
 548         (bo,
 549          Inference.ProofGoalBlock (Inference.BasicProof refl, target_proof))
 550     in
 551     let left, right = if is_left then newterm, right else left, newterm in
 552     let m =
 553       (Inference.metas_of_term left)
 554       @ (Inference.metas_of_term right)
 555       @ (Inference.metas_of_term eq_ty) in
 556     (* let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) (metas @ menv') *)
 557     let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) (metasenv' @ menv')
 558     and newargs = args
 559     in
 560     let ordering = !Utils.compare_terms left right in
 561
 562     let time2 = Unix.gettimeofday () in
 563     build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
 564
 565     let res =
 566       let w = Utils.compute_equality_weight eq_ty left right in
 567       (w, newproof, (eq_ty, left, right, ordering), newmetasenv, newargs)
 568     in
 569     !maxmeta, res
 570   in
 571   let _ =
 572     try
 573       CicTypeChecker.type_of_aux' metasenv' context left ugraph;
 574       CicTypeChecker.type_of_aux' metasenv' context right ugraph;
 575     with
 576         CicUtil.Meta_not_found _ as exn ->
 577           begin
 578             prerr_endline "siamo in demodulation_equality 1";
 579             prerr_endline (CicPp.ppterm left);
 580             prerr_endline (CicPp.ppterm right);
 581             raise exn
 582           end
 583   in
 584   let res = demodulation_aux metasenv' context ugraph table 0 left in
 585   let newmeta, newtarget =
 586     match res with
 587     | Some t ->
 588         let newmeta, newtarget = build_newtarget true t in
 589           if (Inference.is_weak_identity (metasenv', context, ugraph) newtarget) ||
 590             (Inference.meta_convertibility_eq target newtarget) then
 591               newmeta, newtarget
 592           else
 593             demodulation_equality newmeta env table sign newtarget
 594     | None ->
 595         let res = demodulation_aux metasenv' context ugraph table 0 right in
 596           match res with
 597           | Some t ->
 598               let newmeta, newtarget = build_newtarget false t in
 599                 if (Inference.is_weak_identity (metasenv', context, ugraph) newtarget) ||
 600                   (Inference.meta_convertibility_eq target newtarget) then
 601                     newmeta, newtarget
 602                 else
 603                   demodulation_equality newmeta env table sign newtarget
 604           | None ->
 605               newmeta, target
 606   in
 607   (* newmeta, newtarget *)
 608   newmeta,newtarget
 609 ;;
 610
 611
 612 (**
 613    Performs the beta expansion of the term "term" w.r.t. "table",
 614    i.e. returns the list of all the terms t s.t. "(t term) = t2", for some t2
 615    in table.
 616 *)
 617 let rec betaexpand_term metasenv context ugraph table lift_amount term =
 618   let module C = Cic in
 619   let module S = CicSubstitution in
 620   let module M = CicMetaSubst in
 621   let module HL = HelmLibraryObjects in
 622   let candidates = get_candidates Unification table term in
 623   let res, lifted_term =
 624     match term with
 625     | C.Meta (i, l) ->
 626         let l', lifted_l =
 627           List.fold_right
 628             (fun arg (res, lifted_tl) ->
 629                match arg with
 630                | Some arg ->
 631                    let arg_res, lifted_arg =
 632                      betaexpand_term metasenv context ugraph table
 633                        lift_amount arg in
 634                    let l1 =
 635                      List.map
 636                        (fun (t, s, m, ug, eq_found) ->
 637                           (Some t)::lifted_tl, s, m, ug, eq_found)
 638                        arg_res
 639                    in
 640                    (l1 @
 641                       (List.map
 642                          (fun (l, s, m, ug, eq_found) ->
 643                             (Some lifted_arg)::l, s, m, ug, eq_found)
 644                          res),
 645                     (Some lifted_arg)::lifted_tl)
 646                | None ->
 647                    (List.map
 648                       (fun (r, s, m, ug, eq_found) ->
 649                          None::r, s, m, ug, eq_found) res,
 650                     None::lifted_tl)
 651             ) l ([], [])
 652         in
 653         let e =
 654           List.map
 655             (fun (l, s, m, ug, eq_found) ->
 656                (C.Meta (i, l), s, m, ug, eq_found)) l'
 657         in
 658         e, C.Meta (i, lifted_l)
 659
 660     | C.Rel m ->
 661         [], if m <= lift_amount then C.Rel m else C.Rel (m+1)
 662
 663     | C.Prod (nn, s, t) ->
 664         let l1, lifted_s =
 665           betaexpand_term metasenv context ugraph table lift_amount s in
 666         let l2, lifted_t =
 667           betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
 668             table (lift_amount+1) t in
 669         let l1' =
 670           List.map
 671             (fun (t, s, m, ug, eq_found) ->
 672                C.Prod (nn, t, lifted_t), s, m, ug, eq_found) l1
 673         and l2' =
 674           List.map
 675             (fun (t, s, m, ug, eq_found) ->
 676                C.Prod (nn, lifted_s, t), s, m, ug, eq_found) l2 in
 677         l1' @ l2', C.Prod (nn, lifted_s, lifted_t)
 678
 679     | C.Lambda (nn, s, t) ->
 680         let l1, lifted_s =
 681           betaexpand_term metasenv context ugraph table lift_amount s in
 682         let l2, lifted_t =
 683           betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
 684             table (lift_amount+1) t in
 685         let l1' =
 686           List.map
 687             (fun (t, s, m, ug, eq_found) ->
 688                C.Lambda (nn, t, lifted_t), s, m, ug, eq_found) l1
 689         and l2' =
 690           List.map
 691             (fun (t, s, m, ug, eq_found) ->
 692                C.Lambda (nn, lifted_s, t), s, m, ug, eq_found) l2 in
 693         l1' @ l2', C.Lambda (nn, lifted_s, lifted_t)
 694
 695     | C.Appl l ->
 696         let l', lifted_l =
 697           List.fold_right
 698             (fun arg (res, lifted_tl) ->
 699                let arg_res, lifted_arg =
 700                  betaexpand_term metasenv context ugraph table lift_amount arg
 701                in
 702                let l1 =
 703                  List.map
 704                    (fun (a, s, m, ug, eq_found) ->
 705                       a::lifted_tl, s, m, ug, eq_found)
 706                    arg_res
 707                in
 708                (l1 @
 709                   (List.map
 710                      (fun (r, s, m, ug, eq_found) ->
 711                         lifted_arg::r, s, m, ug, eq_found)
 712                      res),
 713                 lifted_arg::lifted_tl)
 714             ) l ([], [])
 715         in
 716         (List.map
 717            (fun (l, s, m, ug, eq_found) -> (C.Appl l, s, m, ug, eq_found)) l',
 718          C.Appl lifted_l)
 719
 720     | t -> [], (S.lift lift_amount t)
 721   in
 722   match term with
 723   | C.Meta (i, l) -> res, lifted_term
 724   | term ->
 725       let termty, ugraph =
 726         C.Implicit None, ugraph
 727 (*         CicTypeChecker.type_of_aux' metasenv context term ugraph *)
 728       in
 729       let r =
 730         find_all_matches
 731           metasenv context ugraph lift_amount term termty candidates
 732       in
 733       r @ res, lifted_term
 734 ;;
 735
 736
 737 let sup_l_counter = ref 1;;
 738
 739 (**
 740    superposition_left
 741    returns a list of new clauses inferred with a left superposition step
 742    the negative equation "target" and one of the positive equations in "table"
 743 *)
 744 let superposition_left newmeta (metasenv, context, ugraph) table target =
 745   let module C = Cic in
 746   let module S = CicSubstitution in
 747   let module M = CicMetaSubst in
 748   let module HL = HelmLibraryObjects in
 749   let module CR = CicReduction in
 750   let module U = Utils in
 751   let weight, proof, (eq_ty, left, right, ordering), menv, _ = target in
 752   let expansions, _ =
 753     let term = if ordering = U.Gt then left else right in
 754     betaexpand_term metasenv context ugraph table 0 term
 755   in
 756   let maxmeta = ref newmeta in
 757   let build_new (bo, s, m, ug, (eq_found, eq_URI)) =
 758
 759 (*     debug_print (lazy "\nSUPERPOSITION LEFT\n"); *)
 760
 761     let time1 = Unix.gettimeofday () in
 762
 763     let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
 764     let what, other = if pos = Utils.Left then what, other else other, what in
 765     let newgoal, newproof =
 766       let bo' =  U.guarded_simpl context (apply_subst s (S.subst other bo)) in
 767       let name = C.Name ("x_SupL_" ^ (string_of_int !sup_l_counter)) in
 768       incr sup_l_counter;
 769       let bo'' =
 770         let l, r =
 771           if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
 772         C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
 773                 S.lift 1 eq_ty; l; r]
 774       in
 775       incr maxmeta;
 776       let metaproof =
 777         let irl =
 778           CicMkImplicit.identity_relocation_list_for_metavariable context in
 779         C.Meta (!maxmeta, irl)
 780       in
 781       let eq_found =
 782         let proof' =
 783           let termlist =
 784             if pos = Utils.Left then [ty; what; other]
 785             else [ty; other; what]
 786           in
 787           Inference.ProofSymBlock (termlist, proof')
 788         in
 789         let what, other =
 790           if pos = Utils.Left then what, other else other, what
 791         in
 792         pos, (0, proof', (ty, other, what, Utils.Incomparable), menv', args')
 793       in
 794       let target_proof =
 795         let pb =
 796           Inference.ProofBlock (s, eq_URI, (name, ty), bo'', eq_found,
 797                                 Inference.BasicProof metaproof)
 798         in
 799         match proof with
 800         | Inference.BasicProof _ ->
 801 (*             debug_print (lazy "replacing a BasicProof"); *)
 802             pb
 803         | Inference.ProofGoalBlock (_, parent_proof) ->
 804 (*             debug_print (lazy "replacing another ProofGoalBlock"); *)
 805             Inference.ProofGoalBlock (pb, parent_proof)
 806         | _ -> assert false
 807       in
 808       let refl =
 809         C.Appl [C.MutConstruct (* reflexivity *)
 810                   (LibraryObjects.eq_URI (), 0, 1, []);
 811                 eq_ty; if ordering = U.Gt then right else left]
 812       in
 813       (bo',
 814        Inference.ProofGoalBlock (Inference.BasicProof refl, target_proof))
 815     in
 816     let left, right =
 817       if ordering = U.Gt then newgoal, right else left, newgoal in
 818     let neworder = !Utils.compare_terms left right in
 819
 820     let time2 = Unix.gettimeofday () in
 821     build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
 822
 823     let res =
 824       let w = Utils.compute_equality_weight eq_ty left right in
 825       (w, newproof, (eq_ty, left, right, neworder), menv @ menv', [])
 826     in
 827     res
 828   in
 829   !maxmeta, List.map build_new expansions
 830 ;;
 831
 832
 833 let sup_r_counter = ref 1;;
 834
 835 (**
 836    superposition_right
 837    returns a list of new clauses inferred with a right superposition step
 838    between the positive equation "target" and one in the "table" "newmeta" is
 839    the first free meta index, i.e. the first number above the highest meta
 840    index: its updated value is also returned
 841 *)
 842 let superposition_right newmeta (metasenv, context, ugraph) table target =
 843   let module C = Cic in
 844   let module S = CicSubstitution in
 845   let module M = CicMetaSubst in
 846   let module HL = HelmLibraryObjects in
 847   let module CR = CicReduction in
 848   let module U = Utils in
 849   let _, eqproof, (eq_ty, left, right, ordering), newmetas, args = target in
 850   let metasenv' = metasenv @ newmetas in
 851   let maxmeta = ref newmeta in
 852   let res1, res2 =
 853     match ordering with
 854     | U.Gt -> fst (betaexpand_term metasenv' context ugraph table 0 left), []
 855     | U.Lt -> [], fst (betaexpand_term metasenv' context ugraph table 0 right)
 856     | _ ->
 857         let res l r =
 858           List.filter
 859             (fun (_, subst, _, _, _) ->
 860                let subst = apply_subst subst in
 861                let o = !Utils.compare_terms (subst l) (subst r) in
 862                o <> U.Lt && o <> U.Le)
 863             (fst (betaexpand_term metasenv' context ugraph table 0 l))
 864         in
 865         (res left right), (res right left)
 866   in
 867   let build_new ordering (bo, s, m, ug, (eq_found, eq_URI)) =
 868
 869     let time1 = Unix.gettimeofday () in
 870
 871     let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
 872     let what, other = if pos = Utils.Left then what, other else other, what in
 873     let newgoal, newproof =
 874       (* qua *)
 875       let bo' = Utils.guarded_simpl context (apply_subst s (S.subst other bo)) in
 876       let name = C.Name ("x_SupR_" ^ (string_of_int !sup_r_counter)) in
 877       incr sup_r_counter;
 878       let bo'' =
 879         let l, r =
 880           if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
 881         C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
 882                 S.lift 1 eq_ty; l; r]
 883       in
 884       bo',
 885       Inference.ProofBlock (s, eq_URI, (name, ty), bo'', eq_found, eqproof)
 886     in
 887     let newmeta, newequality =
 888       let left, right =
 889         if ordering = U.Gt then newgoal, apply_subst s right
 890         else apply_subst s left, newgoal in
 891       let neworder = !Utils.compare_terms left right
 892       and newmenv = newmetas @ menv'
 893       and newargs = args @ args' in
 894       let eq' =
 895         let w = Utils.compute_equality_weight eq_ty left right in
 896         (w, newproof, (eq_ty, left, right, neworder), newmenv, newargs) in
 897       let newm, eq' = Inference.fix_metas !maxmeta eq' in
 898       newm, eq'
 899     in
 900     maxmeta := newmeta;
 901
 902     let time2 = Unix.gettimeofday () in
 903     build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
 904
 905     newequality
 906   in
 907   let new1 = List.map (build_new U.Gt) res1
 908   and new2 = List.map (build_new U.Lt) res2 in
 909 (*
 910   let ok e = not (Inference.is_identity (metasenv, context, ugraph) e) in
 911 *)
 912   let ok e = not (Inference.is_identity (metasenv', context, ugraph) e) in
 913   (!maxmeta,
 914    (List.filter ok (new1 @ new2)))
 915 ;;
 916
 917
 918 (** demodulation, when the target is a goal *)
 919 let rec demodulation_goal newmeta env table goal =
 920   let module C = Cic in
 921   let module S = CicSubstitution in
 922   let module M = CicMetaSubst in
 923   let module HL = HelmLibraryObjects in
 924   let metasenv, context, ugraph = env in
 925   let maxmeta = ref newmeta in
 926   let proof, metas, term = goal in
 927   let term = Utils.guarded_simpl (~debug:true) context term in
 928   let goal = proof, metas, term in
 929   let metasenv' = metasenv @ metas in
 930
 931   let build_newgoal (t, subst, menv, ug, (eq_found, eq_URI)) =
 932     let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
 933     let what, other = if pos = Utils.Left then what, other else other, what in
 934     let ty =
 935       try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
 936       with CicUtil.Meta_not_found _ -> ty
 937     in
 938     let newterm, newproof =
 939       (* qua *)
 940       let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
 941       let bo' = apply_subst subst t in
 942       let name = C.Name ("x_DemodGoal_" ^ (string_of_int !demod_counter)) in
 943       incr demod_counter;
 944       let metaproof =
 945         incr maxmeta;
 946         let irl =
 947           CicMkImplicit.identity_relocation_list_for_metavariable context in
 948 (*         debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta)); *)
 949         C.Meta (!maxmeta, irl)
 950       in
 951       let eq_found =
 952         let proof' =
 953           let termlist =
 954             if pos = Utils.Left then [ty; what; other]
 955             else [ty; other; what]
 956           in
 957           Inference.ProofSymBlock (termlist, proof')
 958         in
 959         let what, other =
 960           if pos = Utils.Left then what, other else other, what
 961         in
 962         pos, (0, proof', (ty, other, what, Utils.Incomparable), menv', args')
 963       in
 964       let goal_proof =
 965         let pb =
 966           Inference.ProofBlock (subst, eq_URI, (name, ty), bo',
 967                                 eq_found, Inference.BasicProof metaproof)
 968         in
 969         let rec repl = function
 970           | Inference.NoProof ->
 971 (*               debug_print (lazy "replacing a NoProof"); *)
 972               pb
 973           | Inference.BasicProof _ ->
 974 (*               debug_print (lazy "replacing a BasicProof"); *)
 975               pb
 976           | Inference.ProofGoalBlock (_, parent_proof) ->
 977 (*               debug_print (lazy "replacing another ProofGoalBlock"); *)
 978               Inference.ProofGoalBlock (pb, parent_proof)
 979           | Inference.SubProof (term, meta_index, p)  ->
 980               Inference.SubProof (term, meta_index, repl p)
 981           | _ -> assert false
 982         in repl proof
 983       in
 984       bo, Inference.ProofGoalBlock (Inference.NoProof, goal_proof)
 985     in
 986     let m = Inference.metas_of_term newterm in
 987     (* QUA *)
 988     let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) (menv @ menv')in
 989     !maxmeta, (newproof, newmetasenv, newterm)
 990   in
 991   let res =
 992     demodulation_aux ~typecheck:true metasenv' context ugraph table 0 term
 993   in
 994   match res with
 995   | Some t ->
 996       let newmeta, newgoal = build_newgoal t in
 997       let _, _, newg = newgoal in
 998       if Inference.meta_convertibility term newg then
 999         newmeta, newgoal
1000       else
1001         demodulation_goal newmeta env table newgoal
1002   | None ->
1003       newmeta, goal
1004 ;;
1005
1006
1007 (** demodulation, when the target is a theorem *)
1008 let rec demodulation_theorem newmeta env table theorem =
1009   let module C = Cic in
1010   let module S = CicSubstitution in
1011   let module M = CicMetaSubst in
1012   let module HL = HelmLibraryObjects in
1013   let metasenv, context, ugraph = env in
1014   let maxmeta = ref newmeta in
1015   let term, termty, metas = theorem in
1016   let metasenv' = metasenv @ metas in
1017
1018   let build_newtheorem (t, subst, menv, ug, (eq_found, eq_URI)) =
1019     let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
1020     let what, other = if pos = Utils.Left then what, other else other, what in
1021     let newterm, newty =
1022       (* qua *)
1023       let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
1024       let bo' = apply_subst subst t in
1025       let name = C.Name ("x_DemodThm_" ^ (string_of_int !demod_counter)) in
1026       incr demod_counter;
1027       let newproof =
1028         Inference.ProofBlock (subst, eq_URI, (name, ty), bo', eq_found,
1029                               Inference.BasicProof term)
1030       in
1031       (Inference.build_proof_term newproof, bo)
1032     in
1033
1034     let m = Inference.metas_of_term newterm in
1035     let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) (metas @ menv') in
1036     !maxmeta, (newterm, newty, newmetasenv)
1037   in
1038   let res =
1039     demodulation_aux ~typecheck:true metasenv' context ugraph table 0 termty
1040   in
1041   match res with
1042   | Some t ->
1043       let newmeta, newthm = build_newtheorem t in
1044       let newt, newty, _ = newthm in
1045       if Inference.meta_convertibility termty newty then
1046         newmeta, newthm
1047       else
1048         demodulation_theorem newmeta env table newthm
1049   | None ->
1050       newmeta, theorem
1051 ;;
1052