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