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   ignore(CicTypeChecker.type_of_aux' metasenv context term);
 134   let check = match termty with C.Implicit None -> false | _ -> true in
 135   function
 136     | [] -> None
 137     | candidate::tl ->
 138         let pos, (_, proof, (ty, left, right, o), metas, args) = candidate in
 139         if check && not (fst (CicReduction.are_convertible
 140                                 ~metasenv context termty ty ugraph)) then (
 141           find_matches metasenv context ugraph lift_amount term termty tl
 142         ) else
 143           let do_match c eq_URI =
 144             let subst', metasenv', ugraph' =
 145               let t1 = Unix.gettimeofday () in
 146               try
 147                 let r =
 148                   Inference.matching (metasenv @ metas) context
 149                     term (S.lift lift_amount c) ugraph
 150                 in
 151                 let t2 = Unix.gettimeofday () in
 152                 match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
 153                 r
 154               with
 155                 | Inference.MatchingFailure as e ->
 156                 let t2 = Unix.gettimeofday () in
 157                 match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
 158                   raise e
 159                 | CicUtil.Meta_not_found _ as exn ->
 160                     prerr_endline "siam qua"; 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 res = demodulation_aux metasenv' context ugraph table 0 left in
 550   let newmeta, newtarget =
 551     match res with
 552     | Some t ->
 553         let newmeta, newtarget = build_newtarget true t in
 554           if (Inference.is_weak_identity (metasenv', context, ugraph) newtarget) ||
 555             (Inference.meta_convertibility_eq target newtarget) then
 556               newmeta, newtarget
 557           else
 558             demodulation_equality newmeta env table sign newtarget
 559     | None ->
 560         let res = demodulation_aux metasenv' context ugraph table 0 right in
 561           match res with
 562           | Some t ->
 563               let newmeta, newtarget = build_newtarget false t in
 564                 if (Inference.is_weak_identity (metasenv', context, ugraph) newtarget) ||
 565                   (Inference.meta_convertibility_eq target newtarget) then
 566                     newmeta, newtarget
 567                 else
 568                   demodulation_equality newmeta env table sign newtarget
 569           | None ->
 570               newmeta, target
 571   in
 572   (* newmeta, newtarget *)
 573   newmeta,newtarget
 574 ;;
 575
 576
 577 (**
 578    Performs the beta expansion of the term "term" w.r.t. "table",
 579    i.e. returns the list of all the terms t s.t. "(t term) = t2", for some t2
 580    in table.
 581 *)
 582 let rec betaexpand_term metasenv context ugraph table lift_amount term =
 583   let module C = Cic in
 584   let module S = CicSubstitution in
 585   let module M = CicMetaSubst in
 586   let module HL = HelmLibraryObjects in
 587   let candidates = get_candidates Unification table term in
 588   let res, lifted_term =
 589     match term with
 590     | C.Meta (i, l) ->
 591         let l', lifted_l =
 592           List.fold_right
 593             (fun arg (res, lifted_tl) ->
 594                match arg with
 595                | Some arg ->
 596                    let arg_res, lifted_arg =
 597                      betaexpand_term metasenv context ugraph table
 598                        lift_amount arg in
 599                    let l1 =
 600                      List.map
 601                        (fun (t, s, m, ug, eq_found) ->
 602                           (Some t)::lifted_tl, s, m, ug, eq_found)
 603                        arg_res
 604                    in
 605                    (l1 @
 606                       (List.map
 607                          (fun (l, s, m, ug, eq_found) ->
 608                             (Some lifted_arg)::l, s, m, ug, eq_found)
 609                          res),
 610                     (Some lifted_arg)::lifted_tl)
 611                | None ->
 612                    (List.map
 613                       (fun (r, s, m, ug, eq_found) ->
 614                          None::r, s, m, ug, eq_found) res,
 615                     None::lifted_tl)
 616             ) l ([], [])
 617         in
 618         let e =
 619           List.map
 620             (fun (l, s, m, ug, eq_found) ->
 621                (C.Meta (i, l), s, m, ug, eq_found)) l'
 622         in
 623         e, C.Meta (i, lifted_l)
 624
 625     | C.Rel m ->
 626         [], if m <= lift_amount then C.Rel m else C.Rel (m+1)
 627
 628     | C.Prod (nn, s, t) ->
 629         let l1, lifted_s =
 630           betaexpand_term metasenv context ugraph table lift_amount s in
 631         let l2, lifted_t =
 632           betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
 633             table (lift_amount+1) t in
 634         let l1' =
 635           List.map
 636             (fun (t, s, m, ug, eq_found) ->
 637                C.Prod (nn, t, lifted_t), s, m, ug, eq_found) l1
 638         and l2' =
 639           List.map
 640             (fun (t, s, m, ug, eq_found) ->
 641                C.Prod (nn, lifted_s, t), s, m, ug, eq_found) l2 in
 642         l1' @ l2', C.Prod (nn, lifted_s, lifted_t)
 643
 644     | C.Lambda (nn, s, t) ->
 645         let l1, lifted_s =
 646           betaexpand_term metasenv context ugraph table lift_amount s in
 647         let l2, lifted_t =
 648           betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
 649             table (lift_amount+1) t in
 650         let l1' =
 651           List.map
 652             (fun (t, s, m, ug, eq_found) ->
 653                C.Lambda (nn, t, lifted_t), s, m, ug, eq_found) l1
 654         and l2' =
 655           List.map
 656             (fun (t, s, m, ug, eq_found) ->
 657                C.Lambda (nn, lifted_s, t), s, m, ug, eq_found) l2 in
 658         l1' @ l2', C.Lambda (nn, lifted_s, lifted_t)
 659
 660     | C.Appl l ->
 661         let l', lifted_l =
 662           List.fold_right
 663             (fun arg (res, lifted_tl) ->
 664                let arg_res, lifted_arg =
 665                  betaexpand_term metasenv context ugraph table lift_amount arg
 666                in
 667                let l1 =
 668                  List.map
 669                    (fun (a, s, m, ug, eq_found) ->
 670                       a::lifted_tl, s, m, ug, eq_found)
 671                    arg_res
 672                in
 673                (l1 @
 674                   (List.map
 675                      (fun (r, s, m, ug, eq_found) ->
 676                         lifted_arg::r, s, m, ug, eq_found)
 677                      res),
 678                 lifted_arg::lifted_tl)
 679             ) l ([], [])
 680         in
 681         (List.map
 682            (fun (l, s, m, ug, eq_found) -> (C.Appl l, s, m, ug, eq_found)) l',
 683          C.Appl lifted_l)
 684
 685     | t -> [], (S.lift lift_amount t)
 686   in
 687   match term with
 688   | C.Meta (i, l) -> res, lifted_term
 689   | term ->
 690       let termty, ugraph =
 691         C.Implicit None, ugraph
 692 (*         CicTypeChecker.type_of_aux' metasenv context term ugraph *)
 693       in
 694       let r =
 695         find_all_matches
 696           metasenv context ugraph lift_amount term termty candidates
 697       in
 698       r @ res, lifted_term
 699 ;;
 700
 701
 702 let sup_l_counter = ref 1;;
 703
 704 (**
 705    superposition_left
 706    returns a list of new clauses inferred with a left superposition step
 707    the negative equation "target" and one of the positive equations in "table"
 708 *)
 709 let superposition_left newmeta (metasenv, context, ugraph) table target =
 710   let module C = Cic in
 711   let module S = CicSubstitution in
 712   let module M = CicMetaSubst in
 713   let module HL = HelmLibraryObjects in
 714   let module CR = CicReduction in
 715   let module U = Utils in
 716   let weight, proof, (eq_ty, left, right, ordering), _, _ = target in
 717   let expansions, _ =
 718     let term = if ordering = U.Gt then left else right in
 719     betaexpand_term metasenv context ugraph table 0 term
 720   in
 721   let maxmeta = ref newmeta in
 722   let build_new (bo, s, m, ug, (eq_found, eq_URI)) =
 723
 724 (*     debug_print (lazy "\nSUPERPOSITION LEFT\n"); *)
 725
 726     let time1 = Unix.gettimeofday () in
 727
 728     let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
 729     let what, other = if pos = Utils.Left then what, other else other, what in
 730     let newgoal, newproof =
 731       let bo' =  U.guarded_simpl context (apply_subst s (S.subst other bo)) in
 732       let name = C.Name ("x_SupL_" ^ (string_of_int !sup_l_counter)) in
 733       incr sup_l_counter;
 734       let bo'' =
 735         let l, r =
 736           if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
 737         C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
 738                 S.lift 1 eq_ty; l; r]
 739       in
 740       incr maxmeta;
 741       let metaproof =
 742         let irl =
 743           CicMkImplicit.identity_relocation_list_for_metavariable context in
 744         C.Meta (!maxmeta, irl)
 745       in
 746       let eq_found =
 747         let proof' =
 748           let termlist =
 749             if pos = Utils.Left then [ty; what; other]
 750             else [ty; other; what]
 751           in
 752           Inference.ProofSymBlock (termlist, proof')
 753         in
 754         let what, other =
 755           if pos = Utils.Left then what, other else other, what
 756         in
 757         pos, (0, proof', (ty, other, what, Utils.Incomparable), menv', args')
 758       in
 759       let target_proof =
 760         let pb =
 761           Inference.ProofBlock (s, eq_URI, (name, ty), bo'', eq_found,
 762                                 Inference.BasicProof metaproof)
 763         in
 764         match proof with
 765         | Inference.BasicProof _ ->
 766 (*             debug_print (lazy "replacing a BasicProof"); *)
 767             pb
 768         | Inference.ProofGoalBlock (_, parent_proof) ->
 769 (*             debug_print (lazy "replacing another ProofGoalBlock"); *)
 770             Inference.ProofGoalBlock (pb, parent_proof)
 771         | _ -> assert false
 772       in
 773       let refl =
 774         C.Appl [C.MutConstruct (* reflexivity *)
 775                   (LibraryObjects.eq_URI (), 0, 1, []);
 776                 eq_ty; if ordering = U.Gt then right else left]
 777       in
 778       (bo',
 779        Inference.ProofGoalBlock (Inference.BasicProof refl, target_proof))
 780     in
 781     let left, right =
 782       if ordering = U.Gt then newgoal, right else left, newgoal in
 783     let neworder = !Utils.compare_terms left right in
 784
 785     let time2 = Unix.gettimeofday () in
 786     build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
 787
 788     let res =
 789       let w = Utils.compute_equality_weight eq_ty left right in
 790       (w, newproof, (eq_ty, left, right, neworder), [], [])
 791     in
 792     res
 793   in
 794   !maxmeta, List.map build_new expansions
 795 ;;
 796
 797
 798 let sup_r_counter = ref 1;;
 799
 800 (**
 801    superposition_right
 802    returns a list of new clauses inferred with a right superposition step
 803    between the positive equation "target" and one in the "table" "newmeta" is
 804    the first free meta index, i.e. the first number above the highest meta
 805    index: its updated value is also returned
 806 *)
 807 let superposition_right newmeta (metasenv, context, ugraph) table target =
 808   let module C = Cic in
 809   let module S = CicSubstitution in
 810   let module M = CicMetaSubst in
 811   let module HL = HelmLibraryObjects in
 812   let module CR = CicReduction in
 813   let module U = Utils in
 814   let _, eqproof, (eq_ty, left, right, ordering), newmetas, args = target in
 815   let metasenv' = metasenv @ newmetas in
 816   let maxmeta = ref newmeta in
 817   let res1, res2 =
 818     match ordering with
 819     | U.Gt -> fst (betaexpand_term metasenv' context ugraph table 0 left), []
 820     | U.Lt -> [], fst (betaexpand_term metasenv' context ugraph table 0 right)
 821     | _ ->
 822         let res l r =
 823           List.filter
 824             (fun (_, subst, _, _, _) ->
 825                let subst = apply_subst subst in
 826                let o = !Utils.compare_terms (subst l) (subst r) in
 827                o <> U.Lt && o <> U.Le)
 828             (fst (betaexpand_term metasenv' context ugraph table 0 l))
 829         in
 830         (res left right), (res right left)
 831   in
 832   let build_new ordering (bo, s, m, ug, (eq_found, eq_URI)) =
 833
 834     let time1 = Unix.gettimeofday () in
 835
 836     let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
 837     let what, other = if pos = Utils.Left then what, other else other, what in
 838     let newgoal, newproof =
 839       (* qua *)
 840       let bo' = Utils.guarded_simpl context (apply_subst s (S.subst other bo)) in
 841       let name = C.Name ("x_SupR_" ^ (string_of_int !sup_r_counter)) in
 842       incr sup_r_counter;
 843       let bo'' =
 844         let l, r =
 845           if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
 846         C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
 847                 S.lift 1 eq_ty; l; r]
 848       in
 849       bo',
 850       Inference.ProofBlock (s, eq_URI, (name, ty), bo'', eq_found, eqproof)
 851     in
 852     let newmeta, newequality =
 853       let left, right =
 854         if ordering = U.Gt then newgoal, apply_subst s right
 855         else apply_subst s left, newgoal in
 856       let neworder = !Utils.compare_terms left right
 857       and newmenv = newmetas @ menv'
 858       and newargs = args @ args' in
 859       let eq' =
 860         let w = Utils.compute_equality_weight eq_ty left right in
 861         (w, newproof, (eq_ty, left, right, neworder), newmenv, newargs) in
 862       let newm, eq' = Inference.fix_metas !maxmeta eq' in
 863       newm, eq'
 864     in
 865     maxmeta := newmeta;
 866
 867     let time2 = Unix.gettimeofday () in
 868     build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
 869
 870     newequality
 871   in
 872   let new1 = List.map (build_new U.Gt) res1
 873   and new2 = List.map (build_new U.Lt) res2 in
 874 (*
 875   let ok e = not (Inference.is_identity (metasenv, context, ugraph) e) in
 876 *)
 877   let ok e = not (Inference.is_identity (metasenv', context, ugraph) e) in
 878   (!maxmeta,
 879    (List.filter ok (new1 @ new2)))
 880 ;;
 881
 882
 883 (** demodulation, when the target is a goal *)
 884 let rec demodulation_goal newmeta env table goal =
 885   let module C = Cic in
 886   let module S = CicSubstitution in
 887   let module M = CicMetaSubst in
 888   let module HL = HelmLibraryObjects in
 889   let metasenv, context, ugraph = env in
 890   let maxmeta = ref newmeta in
 891   let proof, metas, term = goal in
 892   let term = Utils.guarded_simpl (~debug:true) context term in
 893   let goal = proof, metas, term in
 894   let metasenv' = metasenv @ metas in
 895
 896   let build_newgoal (t, subst, menv, ug, (eq_found, eq_URI)) =
 897     let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
 898     let what, other = if pos = Utils.Left then what, other else other, what in
 899     let ty =
 900       try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
 901       with CicUtil.Meta_not_found _ -> ty
 902     in
 903     let newterm, newproof =
 904       (* qua *)
 905       let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
 906       let bo' = apply_subst subst t in
 907       let name = C.Name ("x_DemodGoal_" ^ (string_of_int !demod_counter)) in
 908       incr demod_counter;
 909       let metaproof =
 910         incr maxmeta;
 911         let irl =
 912           CicMkImplicit.identity_relocation_list_for_metavariable context in
 913 (*         debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta)); *)
 914         C.Meta (!maxmeta, irl)
 915       in
 916       let eq_found =
 917         let proof' =
 918           let termlist =
 919             if pos = Utils.Left then [ty; what; other]
 920             else [ty; other; what]
 921           in
 922           Inference.ProofSymBlock (termlist, proof')
 923         in
 924         let what, other =
 925           if pos = Utils.Left then what, other else other, what
 926         in
 927         pos, (0, proof', (ty, other, what, Utils.Incomparable), menv', args')
 928       in
 929       let goal_proof =
 930         let pb =
 931           Inference.ProofBlock (subst, eq_URI, (name, ty), bo',
 932                                 eq_found, Inference.BasicProof metaproof)
 933         in
 934         let rec repl = function
 935           | Inference.NoProof ->
 936 (*               debug_print (lazy "replacing a NoProof"); *)
 937               pb
 938           | Inference.BasicProof _ ->
 939 (*               debug_print (lazy "replacing a BasicProof"); *)
 940               pb
 941           | Inference.ProofGoalBlock (_, parent_proof) ->
 942 (*               debug_print (lazy "replacing another ProofGoalBlock"); *)
 943               Inference.ProofGoalBlock (pb, parent_proof)
 944           | Inference.SubProof (term, meta_index, p)  ->
 945               Inference.SubProof (term, meta_index, repl p)
 946           | _ -> assert false
 947         in repl proof
 948       in
 949       bo, Inference.ProofGoalBlock (Inference.NoProof, goal_proof)
 950     in
 951     let m = Inference.metas_of_term newterm in
 952     let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) (metas @ menv')in
 953     !maxmeta, (newproof, newmetasenv, newterm)
 954   in
 955   let res =
 956     demodulation_aux ~typecheck:true metasenv' context ugraph table 0 term
 957   in
 958   match res with
 959   | Some t ->
 960       let newmeta, newgoal = build_newgoal t in
 961       let _, _, newg = newgoal in
 962       if Inference.meta_convertibility term newg then
 963         newmeta, newgoal
 964       else
 965         demodulation_goal newmeta env table newgoal
 966   | None ->
 967       newmeta, goal
 968 ;;
 969
 970
 971 (** demodulation, when the target is a theorem *)
 972 let rec demodulation_theorem newmeta env table theorem =
 973   let module C = Cic in
 974   let module S = CicSubstitution in
 975   let module M = CicMetaSubst in
 976   let module HL = HelmLibraryObjects in
 977   let metasenv, context, ugraph = env in
 978   let maxmeta = ref newmeta in
 979   let term, termty, metas = theorem in
 980   let metasenv' = metasenv @ metas in
 981
 982   let build_newtheorem (t, subst, menv, ug, (eq_found, eq_URI)) =
 983     let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
 984     let what, other = if pos = Utils.Left then what, other else other, what in
 985     let newterm, newty =
 986       (* qua *)
 987       let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
 988       let bo' = apply_subst subst t in
 989       let name = C.Name ("x_DemodThm_" ^ (string_of_int !demod_counter)) in
 990       incr demod_counter;
 991       let newproof =
 992         Inference.ProofBlock (subst, eq_URI, (name, ty), bo', eq_found,
 993                               Inference.BasicProof term)
 994       in
 995       (Inference.build_proof_term newproof, bo)
 996     in
 997
 998     let m = Inference.metas_of_term newterm in
 999     let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) (metas @ menv') in
1000     !maxmeta, (newterm, newty, newmetasenv)
1001   in
1002   let res =
1003     demodulation_aux ~typecheck:true metasenv' context ugraph table 0 termty
1004   in
1005   match res with
1006   | Some t ->
1007       let newmeta, newthm = build_newtheorem t in
1008       let newt, newty, _ = newthm in
1009       if Inference.meta_convertibility termty newty then
1010         newmeta, newthm
1011       else
1012         demodulation_theorem newmeta env table newthm
1013   | None ->
1014       newmeta, theorem
1015 ;;
1016