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 module Index = Equality_indexing.DT (* discrimination tree based indexing *)
  27 (*
  28 module Index = Equality_indexing.DT (* path tree based indexing *)
  29 *)
  30
  31 let debug_print = Utils.debug_print;;
  32
  33
  34 type retrieval_mode = Matching | Unification;;
  35
  36 let print_candidates mode term res =
  37   let _ =
  38     match mode with
  39     | Matching ->
  40         Printf.printf "| candidates Matching %s\n" (CicPp.ppterm term)
  41     | Unification ->
  42         Printf.printf "| candidates Unification %s\n" (CicPp.ppterm term)
  43   in
  44   print_endline
  45     (String.concat "\n"
  46        (List.map
  47           (fun (p, e) ->
  48              Printf.sprintf "| (%s, %s)" (Utils.string_of_pos p)
  49                (Inference.string_of_equality e))
  50           res));
  51   print_endline "|";
  52 ;;
  53
  54
  55 let indexing_retrieval_time = ref 0.;;
  56
  57
  58 let apply_subst = CicMetaSubst.apply_subst
  59
  60 let index = Index.index
  61 let remove_index = Index.remove_index
  62 let in_index = Index.in_index
  63 let empty = Index.empty
  64 let init_index = Index.init_index
  65
  66 (* returns a list of all the equalities in the tree that are in relation
  67    "mode" with the given term, where mode can be either Matching or
  68    Unification.
  69
  70    Format of the return value: list of tuples in the form:
  71    (position - Left or Right - of the term that matched the given one in this
  72      equality,
  73     equality found)
  74
  75    Note that if equality is "left = right", if the ordering is left > right,
  76    the position will always be Left, and if the ordering is left < right,
  77    position will be Right.
  78 *)
  79 let get_candidates mode tree term =
  80   let t1 = Unix.gettimeofday () in
  81   let res =
  82     let s =
  83       match mode with
  84       | Matching -> Index.retrieve_generalizations tree term
  85       | Unification -> Index.retrieve_unifiables tree term
  86     in
  87     Index.PosEqSet.elements s
  88   in
  89   (*   print_candidates mode term res; *)
  90 (*   print_endline (Discrimination_tree.string_of_discrimination_tree tree); *)
  91 (*   print_newline (); *)
  92   let t2 = Unix.gettimeofday () in
  93   indexing_retrieval_time := !indexing_retrieval_time +. (t2 -. t1);
  94   res
  95 ;;
  96
  97
  98 let match_unif_time_ok = ref 0.;;
  99 let match_unif_time_no = ref 0.;;
 100
 101
 102 (*
 103   finds the first equality in the index that matches "term", of type "termty"
 104   termty can be Implicit if it is not needed. The result (one of the sides of
 105   the equality, actually) should be not greater (wrt the term ordering) than
 106   term
 107
 108   Format of the return value:
 109
 110   (term to substitute, [Cic.Rel 1 properly lifted - see the various
 111                         build_newtarget functions inside the various
 112                         demodulation_* functions]
 113    substitution used for the matching,
 114    metasenv,
 115    ugraph, [substitution, metasenv and ugraph have the same meaning as those
 116    returned by CicUnification.fo_unif]
 117    (equality where the matching term was found, [i.e. the equality to use as
 118                                                 rewrite rule]
 119     uri [either eq_ind_URI or eq_ind_r_URI, depending on the direction of
 120          the equality: this is used to build the proof term, again see one of
 121          the build_newtarget functions]
 122    ))
 123 *)
 124 let rec find_matches metasenv context ugraph lift_amount term termty =
 125   let module C = Cic in
 126   let module U = Utils in
 127   let module S = CicSubstitution in
 128   let module M = CicMetaSubst in
 129   let module HL = HelmLibraryObjects in
 130   let cmp = !Utils.compare_terms in
 131   let check = match termty with C.Implicit None -> false | _ -> true in
 132   function
 133     | [] -> None
 134     | candidate::tl ->
 135         let pos, (_, proof, (ty, left, right, o), metas, args) = candidate in
 136         if check && not (fst (CicReduction.are_convertible
 137                                 ~metasenv context termty ty ugraph)) then (
 138           find_matches metasenv context ugraph lift_amount term termty tl
 139         ) else
 140           let do_match c eq_URI =
 141             let subst', metasenv', ugraph' =
 142               let t1 = Unix.gettimeofday () in
 143               try
 144                 let r =
 145                   Inference.matching (metasenv @ metas) context
 146                     term (S.lift lift_amount c) ugraph in
 147                 let t2 = Unix.gettimeofday () in
 148                 match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
 149                 r
 150               with Inference.MatchingFailure as e ->
 151                 let t2 = Unix.gettimeofday () in
 152                 match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
 153                 raise e
 154             in
 155             Some (C.Rel (1 + lift_amount), subst', metasenv', ugraph',
 156                   (candidate, eq_URI))
 157           in
 158           let c, other, eq_URI =
 159             if pos = Utils.Left then left, right, Utils.eq_ind_URI ()
 160             else right, left, Utils.eq_ind_r_URI ()
 161           in
 162           if o <> U.Incomparable then
 163             try
 164               do_match c eq_URI
 165             with Inference.MatchingFailure ->
 166               find_matches metasenv context ugraph lift_amount term termty tl
 167           else
 168             let res =
 169               try do_match c eq_URI
 170               with Inference.MatchingFailure -> None
 171             in
 172             match res with
 173             | Some (_, s, _, _, _) ->
 174                 let c' = apply_subst s c in
 175                 let other' = U.guarded_simpl context (apply_subst s other) in
 176                 let order = cmp c' other' in
 177                 let names = U.names_of_context context in
 178                 if order = U.Gt then
 179                   res
 180                 else
 181                   find_matches
 182                     metasenv context ugraph lift_amount term termty tl
 183             | None ->
 184                 find_matches metasenv context ugraph lift_amount term termty tl
 185 ;;
 186
 187
 188 (*
 189   as above, but finds all the matching equalities, and the matching condition
 190   can be either Inference.matching or Inference.unification
 191 *)
 192 let rec find_all_matches ?(unif_fun=Inference.unification)
 193     metasenv context ugraph lift_amount term termty =
 194   let module C = Cic in
 195   let module U = Utils in
 196   let module S = CicSubstitution in
 197   let module M = CicMetaSubst in
 198   let module HL = HelmLibraryObjects in
 199   let cmp = !Utils.compare_terms in
 200   function
 201     | [] -> []
 202     | candidate::tl ->
 203         let pos, (_, _, (ty, left, right, o), metas, args) = candidate in
 204         let do_match c eq_URI =
 205           let subst', metasenv', ugraph' =
 206             let t1 = Unix.gettimeofday () in
 207             try
 208               let r =
 209                 unif_fun (metasenv @ metas) context
 210                   term (S.lift lift_amount c) ugraph in
 211               let t2 = Unix.gettimeofday () in
 212               match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
 213               r
 214             with
 215             | Inference.MatchingFailure
 216             | CicUnification.UnificationFailure _
 217             | CicUnification.Uncertain _ as e ->
 218                 let t2 = Unix.gettimeofday () in
 219                 match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
 220                 raise e
 221           in
 222           (C.Rel (1 + lift_amount), subst', metasenv', ugraph',
 223            (candidate, eq_URI))
 224         in
 225         let c, other, eq_URI =
 226           if pos = Utils.Left then left, right, Utils.eq_ind_URI ()
 227           else right, left, Utils.eq_ind_r_URI ()
 228         in
 229         if o <> U.Incomparable then
 230           try
 231             let res = do_match c eq_URI in
 232             res::(find_all_matches ~unif_fun metasenv context ugraph
 233                     lift_amount term termty tl)
 234           with
 235           | Inference.MatchingFailure
 236           | CicUnification.UnificationFailure _
 237           | CicUnification.Uncertain _ ->
 238               find_all_matches ~unif_fun metasenv context ugraph
 239                 lift_amount term termty tl
 240         else
 241           try
 242             let res = do_match c eq_URI in
 243             match res with
 244             | _, s, _, _, _ ->
 245                 let c' = apply_subst s c
 246                 and other' = apply_subst s other in
 247                 let order = cmp c' other' in
 248                 let names = U.names_of_context context in
 249                 if order <> U.Lt && order <> U.Le then
 250                   res::(find_all_matches ~unif_fun metasenv context ugraph
 251                           lift_amount term termty tl)
 252                 else
 253                   find_all_matches ~unif_fun metasenv context ugraph
 254                     lift_amount term termty tl
 255           with
 256           | Inference.MatchingFailure
 257           | CicUnification.UnificationFailure _
 258           | CicUnification.Uncertain _ ->
 259               find_all_matches ~unif_fun metasenv context ugraph
 260                 lift_amount term termty tl
 261 ;;
 262
 263
 264 (*
 265   returns true if target is subsumed by some equality in table
 266 *)
 267 let subsumption env table target =
 268   let _, _, (ty, left, right, _), tmetas, _ = target in
 269   let metasenv, context, ugraph = env in
 270   let metasenv = metasenv @ tmetas in
 271   let samesubst subst subst' =
 272     let tbl = Hashtbl.create (List.length subst) in
 273     List.iter (fun (m, (c, t1, t2)) -> Hashtbl.add tbl m (c, t1, t2)) subst;
 274     List.for_all
 275       (fun (m, (c, t1, t2)) ->
 276          try
 277            let c', t1', t2' = Hashtbl.find tbl m in
 278            if (c = c') && (t1 = t1') && (t2 = t2') then true
 279            else false
 280          with Not_found ->
 281            true)
 282       subst'
 283   in
 284   let leftr =
 285     match left with
 286     | Cic.Meta _ -> []
 287     | _ ->
 288         let leftc = get_candidates Matching table left in
 289         find_all_matches ~unif_fun:Inference.matching
 290           metasenv context ugraph 0 left ty leftc
 291   in
 292   let rec ok what = function
 293     | [] -> false, []
 294     | (_, subst, menv, ug, ((pos, (_, _, (_, l, r, o), m, _)), _))::tl ->
 295         try
 296           let other = if pos = Utils.Left then r else l in
 297           let subst', menv', ug' =
 298             let t1 = Unix.gettimeofday () in
 299             try
 300               let r =
 301                 Inference.matching (metasenv @ menv @ m) context what other ugraph
 302               in
 303               let t2 = Unix.gettimeofday () in
 304               match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
 305               r
 306             with Inference.MatchingFailure as e ->
 307               let t2 = Unix.gettimeofday () in
 308               match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
 309               raise e
 310           in
 311           if samesubst subst subst' then
 312             true, subst
 313           else
 314             ok what tl
 315         with Inference.MatchingFailure ->
 316           ok what tl
 317   in
 318   let r, subst = ok right leftr in
 319   let r, s =
 320     if r then
 321       true, subst
 322     else
 323       let rightr =
 324         match right with
 325           | Cic.Meta _ -> []
 326           | _ ->
 327               let rightc = get_candidates Matching table right in
 328                 find_all_matches ~unif_fun:Inference.matching
 329                   metasenv context ugraph 0 right ty rightc
 330       in
 331         ok left rightr
 332   in
 333 (*     (if r then  *)
 334 (*        debug_print  *)
 335 (*       (lazy *)
 336 (*          (Printf.sprintf "SUBSUMPTION! %s\n%s\n" *)
 337 (*             (Inference.string_of_equality target) (Utils.print_subst s)))); *)
 338     r, s
 339 ;;
 340
 341
 342 let rec demodulation_aux ?(typecheck=false)
 343     metasenv context ugraph table lift_amount term =
 344   let module C = Cic in
 345   let module S = CicSubstitution in
 346   let module M = CicMetaSubst in
 347   let module HL = HelmLibraryObjects in
 348   let candidates = get_candidates Matching table term in
 349   match term with
 350   | C.Meta _ -> None
 351   | term ->
 352       let termty, ugraph =
 353         if typecheck then
 354           CicTypeChecker.type_of_aux' metasenv context term ugraph
 355         else
 356           C.Implicit None, ugraph
 357       in
 358       let res =
 359         find_matches metasenv context ugraph lift_amount term termty candidates
 360       in
 361       if res <> None then
 362         res
 363       else
 364         match term with
 365         | C.Appl l ->
 366             let res, ll =
 367               List.fold_left
 368                 (fun (res, tl) t ->
 369                    if res <> None then
 370                      (res, tl @ [S.lift 1 t])
 371                    else
 372                      let r =
 373                        demodulation_aux metasenv context ugraph table
 374                          lift_amount t
 375                      in
 376                      match r with
 377                      | None -> (None, tl @ [S.lift 1 t])
 378                      | Some (rel, _, _, _, _) -> (r, tl @ [rel]))
 379                 (None, []) l
 380             in (
 381               match res with
 382               | None -> None
 383               | Some (_, subst, menv, ug, eq_found) ->
 384                   Some (C.Appl ll, subst, menv, ug, eq_found)
 385             )
 386         | C.Prod (nn, s, t) ->
 387             let r1 =
 388               demodulation_aux metasenv context ugraph table lift_amount s in (
 389               match r1 with
 390               | None ->
 391                   let r2 =
 392                     demodulation_aux metasenv
 393                       ((Some (nn, C.Decl s))::context) ugraph
 394                       table (lift_amount+1) t
 395                   in (
 396                     match r2 with
 397                     | None -> None
 398                     | Some (t', subst, menv, ug, eq_found) ->
 399                         Some (C.Prod (nn, (S.lift 1 s), t'),
 400                               subst, menv, ug, eq_found)
 401                   )
 402               | Some (s', subst, menv, ug, eq_found) ->
 403                   Some (C.Prod (nn, s', (S.lift 1 t)),
 404                         subst, menv, ug, eq_found)
 405             )
 406         | C.Lambda (nn, s, t) ->
 407             let r1 =
 408               demodulation_aux metasenv context ugraph table lift_amount s in (
 409               match r1 with
 410               | None ->
 411                   let r2 =
 412                     demodulation_aux metasenv
 413                       ((Some (nn, C.Decl s))::context) ugraph
 414                       table (lift_amount+1) t
 415                   in (
 416                     match r2 with
 417                     | None -> None
 418                     | Some (t', subst, menv, ug, eq_found) ->
 419                         Some (C.Lambda (nn, (S.lift 1 s), t'),
 420                               subst, menv, ug, eq_found)
 421                   )
 422               | Some (s', subst, menv, ug, eq_found) ->
 423                   Some (C.Lambda (nn, s', (S.lift 1 t)),
 424                         subst, menv, ug, eq_found)
 425             )
 426         | t ->
 427             None
 428 ;;
 429
 430
 431 let build_newtarget_time = ref 0.;;
 432
 433
 434 let demod_counter = ref 1;;
 435
 436 (** demodulation, when target is an equality *)
 437 let rec demodulation_equality newmeta env table sign target =
 438   let module C = Cic in
 439   let module S = CicSubstitution in
 440   let module M = CicMetaSubst in
 441   let module HL = HelmLibraryObjects in
 442   let module U = Utils in
 443   let metasenv, context, ugraph = env in
 444   let _, proof, (eq_ty, left, right, order), metas, args = target in
 445   let metasenv' = metasenv @ metas in
 446
 447   let maxmeta = ref newmeta in
 448
 449   let build_newtarget is_left (t, subst, menv, ug, (eq_found, eq_URI)) =
 450     let time1 = Unix.gettimeofday () in
 451
 452     let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
 453     let ty =
 454       try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
 455       with CicUtil.Meta_not_found _ -> ty
 456     in
 457     let what, other = if pos = Utils.Left then what, other else other, what in
 458     let newterm, newproof =
 459       let bo = U.guarded_simpl context (apply_subst subst (S.subst other t)) in
 460       let name = C.Name ("x_Demod_" ^ (string_of_int !demod_counter)) in
 461       incr demod_counter;
 462       let bo' =
 463         let l, r = if is_left then t, S.lift 1 right else S.lift 1 left, t in
 464         C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
 465                 S.lift 1 eq_ty; l; r]
 466       in
 467       if sign = Utils.Positive then
 468         (bo,
 469          Inference.ProofBlock (
 470            subst, eq_URI, (name, ty), bo'(* t' *), eq_found, proof))
 471       else
 472         let metaproof =
 473           incr maxmeta;
 474           let irl =
 475             CicMkImplicit.identity_relocation_list_for_metavariable context in
 476 (*           debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta)); *)
 477 (*           print_newline (); *)
 478           C.Meta (!maxmeta, irl)
 479         in
 480           let eq_found =
 481             let proof' =
 482               let termlist =
 483                 if pos = Utils.Left then [ty; what; other]
 484                 else [ty; other; what]
 485               in
 486               Inference.ProofSymBlock (termlist, proof')
 487             in
 488             let what, other =
 489               if pos = Utils.Left then what, other else other, what
 490             in
 491             pos, (0, proof', (ty, other, what, Utils.Incomparable),
 492                   menv', args')
 493           in
 494           let target_proof =
 495             let pb =
 496               Inference.ProofBlock (subst, eq_URI, (name, ty), bo',
 497                                     eq_found, Inference.BasicProof metaproof)
 498             in
 499             match proof with
 500             | Inference.BasicProof _ ->
 501                 print_endline "replacing a BasicProof";
 502                 pb
 503             | Inference.ProofGoalBlock (_, parent_proof) ->
 504                 print_endline "replacing another ProofGoalBlock";
 505                 Inference.ProofGoalBlock (pb, parent_proof)
 506             | _ -> assert false
 507           in
 508         let refl =
 509           C.Appl [C.MutConstruct (* reflexivity *)
 510                     (LibraryObjects.eq_URI (), 0, 1, []);
 511                   eq_ty; if is_left then right else left]
 512         in
 513         (bo,
 514          Inference.ProofGoalBlock (Inference.BasicProof refl, target_proof))
 515     in
 516     let left, right = if is_left then newterm, right else left, newterm in
 517     let m = (Inference.metas_of_term left) @ (Inference.metas_of_term right) in
 518     let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) metas
 519     and newargs = args
 520     in
 521     let ordering = !Utils.compare_terms left right in
 522
 523     let time2 = Unix.gettimeofday () in
 524     build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
 525
 526     let res =
 527       let w = Utils.compute_equality_weight eq_ty left right in
 528       (w, newproof, (eq_ty, left, right, ordering), newmetasenv, newargs)
 529     in
 530     !maxmeta, res
 531   in
 532   let res = demodulation_aux metasenv' context ugraph table 0 left in
 533   let newmeta, newtarget =
 534     match res with
 535     | Some t ->
 536         let newmeta, newtarget = build_newtarget true t in
 537           if (Inference.is_identity (metasenv', context, ugraph) newtarget) ||
 538             (Inference.meta_convertibility_eq target newtarget) then
 539               newmeta, newtarget
 540           else
 541             demodulation_equality newmeta env table sign newtarget
 542     | None ->
 543         let res = demodulation_aux metasenv' context ugraph table 0 right in
 544           match res with
 545           | Some t ->
 546               let newmeta, newtarget = build_newtarget false t in
 547                 if (Inference.is_identity (metasenv', context, ugraph) newtarget) ||
 548                   (Inference.meta_convertibility_eq target newtarget) then
 549                     newmeta, newtarget
 550                 else
 551                   demodulation_equality newmeta env table sign newtarget
 552           | None ->
 553               newmeta, target
 554   in
 555   (* newmeta, newtarget *)
 556   (* tentiamo di ridurre usando CicReduction.normalize *)
 557   let w, p, (ty, left, right, o), m, a = newtarget in
 558   let left' = ProofEngineReduction.simpl context left in
 559   let right' = ProofEngineReduction.simpl context right in
 560   let newleft =
 561     if !Utils.compare_terms left' left = Utils.Lt then left' else left in
 562   let newright =
 563     if !Utils.compare_terms right' right = Utils.Lt then right' else right in
 564 (*   if newleft != left || newright != right then ( *)
 565 (*     debug_print *)
 566 (*       (lazy *)
 567 (*       (Printf.sprintf "left: %s, left': %s\nright: %s, right': %s\n" *)
 568 (*          (CicPp.ppterm left) (CicPp.ppterm left') (CicPp.ppterm right) *)
 569 (*          (CicPp.ppterm right'))) *)
 570 (*   ); *)
 571   let w' = Utils.compute_equality_weight ty newleft newright in
 572   let o' = !Utils.compare_terms newleft newright in
 573   newmeta, (w', p, (ty, newleft, newright, o'), m, a)
 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       let bo' = apply_subst s (S.subst other bo) in
 840       let t' =
 841         let name = C.Name ("x_SupR_" ^ (string_of_int !sup_r_counter)) in
 842         incr sup_r_counter;
 843         let l, r =
 844           if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
 845         (name, ty, S.lift 1 eq_ty, l, r)
 846       in
 847       let name = C.Name ("x_SupR_" ^ (string_of_int !sup_r_counter)) in
 848       incr sup_r_counter;
 849       let bo'' =
 850         let l, r =
 851           if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
 852         C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
 853                 S.lift 1 eq_ty; l; r]
 854       in
 855       bo',
 856       Inference.ProofBlock (s, eq_URI, (name, ty), bo'', eq_found, eqproof)
 857     in
 858     let newmeta, newequality =
 859       let left, right =
 860         if ordering = U.Gt then newgoal, apply_subst s right
 861         else apply_subst s left, newgoal in
 862       let neworder = !Utils.compare_terms left right
 863       and newmenv = newmetas @ menv'
 864       and newargs = args @ args' in
 865       let eq' =
 866         let w = Utils.compute_equality_weight eq_ty left right in
 867         (w, newproof, (eq_ty, left, right, neworder), newmenv, newargs)
 868       and env = (metasenv, context, ugraph) in
 869       let newm, eq' = Inference.fix_metas !maxmeta eq' in
 870       newm, eq'
 871     in
 872     maxmeta := newmeta;
 873
 874     let time2 = Unix.gettimeofday () in
 875     build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
 876
 877     newequality
 878   in
 879   let new1 = List.map (build_new U.Gt) res1
 880   and new2 = List.map (build_new U.Lt) res2 in
 881   let ok e = not (Inference.is_identity (metasenv, context, ugraph) e) in
 882   (!maxmeta,
 883    (List.filter ok (new1 @ new2)))
 884 ;;
 885
 886
 887 (** demodulation, when the target is a goal *)
 888 let rec demodulation_goal newmeta env table goal =
 889   let module C = Cic in
 890   let module S = CicSubstitution in
 891   let module M = CicMetaSubst in
 892   let module HL = HelmLibraryObjects in
 893   let metasenv, context, ugraph = env in
 894   let maxmeta = ref newmeta in
 895   let proof, metas, term = goal in
 896   let metasenv' = metasenv @ metas in
 897
 898   let build_newgoal (t, subst, menv, ug, (eq_found, eq_URI)) =
 899     let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
 900     let what, other = if pos = Utils.Left then what, other else other, what in
 901     let ty =
 902       try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
 903       with CicUtil.Meta_not_found _ -> ty
 904     in
 905     let newterm, newproof =
 906       let bo = apply_subst subst (S.subst other t) in
 907       let bo' = apply_subst subst t in
 908       let name = C.Name ("x_DemodGoal_" ^ (string_of_int !demod_counter)) in
 909       incr demod_counter;
 910       let metaproof =
 911         incr maxmeta;
 912         let irl =
 913           CicMkImplicit.identity_relocation_list_for_metavariable context in
 914 (*         debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta)); *)
 915         C.Meta (!maxmeta, irl)
 916       in
 917       let eq_found =
 918         let proof' =
 919           let termlist =
 920             if pos = Utils.Left then [ty; what; other]
 921             else [ty; other; what]
 922           in
 923           Inference.ProofSymBlock (termlist, proof')
 924         in
 925         let what, other =
 926           if pos = Utils.Left then what, other else other, what
 927         in
 928         pos, (0, proof', (ty, other, what, Utils.Incomparable), menv', args')
 929       in
 930       let goal_proof =
 931         let pb =
 932           Inference.ProofBlock (subst, eq_URI, (name, ty), bo',
 933                                 eq_found, Inference.BasicProof metaproof)
 934         in
 935         let rec repl = function
 936           | Inference.NoProof ->
 937 (*               debug_print (lazy "replacing a NoProof"); *)
 938               pb
 939           | Inference.BasicProof _ ->
 940 (*               debug_print (lazy "replacing a BasicProof"); *)
 941               pb
 942           | Inference.ProofGoalBlock (_, parent_proof) ->
 943 (*               debug_print (lazy "replacing another ProofGoalBlock"); *)
 944               Inference.ProofGoalBlock (pb, parent_proof)
 945           | (Inference.SubProof (term, meta_index, p) as subproof) ->
 946 (*               debug_print *)
 947 (*                 (lazy *)
 948 (*                    (Printf.sprintf "replacing %s" *)
 949 (*                       (Inference.string_of_proof subproof))); *)
 950               Inference.SubProof (term, meta_index, repl p)
 951           | _ -> assert false
 952         in repl proof
 953       in
 954       bo, Inference.ProofGoalBlock (Inference.NoProof, goal_proof)
 955     in
 956     let m = Inference.metas_of_term newterm in
 957     let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) metas in
 958     !maxmeta, (newproof, newmetasenv, newterm)
 959   in
 960   let res =
 961     demodulation_aux ~typecheck:true metasenv' context ugraph table 0 term
 962   in
 963   match res with
 964   | Some t ->
 965       let newmeta, newgoal = build_newgoal t in
 966       let _, _, newg = newgoal in
 967       if Inference.meta_convertibility term newg then
 968         newmeta, newgoal
 969       else
 970         demodulation_goal newmeta env table newgoal
 971   | None ->
 972       newmeta, goal
 973 ;;
 974
 975
 976 (** demodulation, when the target is a theorem *)
 977 let rec demodulation_theorem newmeta env table theorem =
 978   let module C = Cic in
 979   let module S = CicSubstitution in
 980   let module M = CicMetaSubst in
 981   let module HL = HelmLibraryObjects in
 982   let metasenv, context, ugraph = env in
 983   let maxmeta = ref newmeta in
 984   let proof, metas, term = theorem in
 985   let term, termty, metas = theorem in
 986   let metasenv' = metasenv @ metas in
 987
 988   let build_newtheorem (t, subst, menv, ug, (eq_found, eq_URI)) =
 989     let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
 990     let what, other = if pos = Utils.Left then what, other else other, what in
 991     let newterm, newty =
 992       let bo = apply_subst subst (S.subst other t) in
 993       let bo' = apply_subst subst t in
 994       let name = C.Name ("x_DemodThm_" ^ (string_of_int !demod_counter)) in
 995       incr demod_counter;
 996       let newproof =
 997         Inference.ProofBlock (subst, eq_URI, (name, ty), bo', eq_found,
 998                               Inference.BasicProof term)
 999       in
1000       (Inference.build_proof_term newproof, bo)
1001     in
1002     let m = Inference.metas_of_term newterm in
1003     let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) metas in
1004     !maxmeta, (newterm, newty, newmetasenv)
1005   in
1006   let res =
1007     demodulation_aux ~typecheck:true metasenv' context ugraph table 0 termty
1008   in
1009   match res with
1010   | Some t ->
1011       let newmeta, newthm = build_newtheorem t in
1012       let newt, newty, _ = newthm in
1013       if Inference.meta_convertibility termty newty then
1014         newmeta, newthm
1015       else
1016         demodulation_theorem newmeta env table newthm
1017   | None ->
1018       newmeta, theorem
1019 ;;