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