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