helm/ocaml/paramodulation/indexing.ml

   1
   2 type retrieval_mode = Matching | Unification;;
   3
   4
   5 let empty_table () =
   6   Path_indexing.PSTrie.empty
   7 ;;
   8
   9 let index = Path_indexing.index
  10 and remove_index = Path_indexing.remove_index
  11 and in_index = Path_indexing.in_index;;
  12
  13 let get_candidates mode trie term =
  14   let s =
  15     match mode with
  16     | Matching -> Path_indexing.retrieve_generalizations trie term
  17     | Unification -> Path_indexing.retrieve_unifiables trie term
  18   in
  19   Path_indexing.PosEqSet.elements s
  20 ;;
  21
  22
  23 (*
  24 let empty_table () =
  25   Discrimination_tree.DiscriminationTree.empty
  26 ;;
  27
  28 let index = Discrimination_tree.index
  29 and remove_index = Discrimination_tree.remove_index
  30 and in_index = Discrimination_tree.in_index;;
  31
  32 let get_candidates mode tree term =
  33   match mode with
  34   | Matching -> Discrimination_tree.retrieve_generalizations tree term
  35   | Unification -> Discrimination_tree.retrieve_unifiables tree term
  36 ;;
  37 *)
  38
  39
  40 let rec find_matches metasenv context ugraph lift_amount term =
  41   let module C = Cic in
  42   let module U = Utils in
  43   let module S = CicSubstitution in
  44   let module M = CicMetaSubst in
  45   let module HL = HelmLibraryObjects in
  46   let cmp = !Utils.compare_terms in
  47   let names = Utils.names_of_context context in
  48   function
  49     | [] -> None
  50     | candidate::tl ->
  51         let pos, (proof, (ty, left, right, o), metas, args) = candidate in
  52         let do_match c other eq_URI =
  53           let subst', metasenv', ugraph' =
  54             Inference.matching (metasenv @ metas) context
  55               term (S.lift lift_amount c) ugraph
  56           in
  57           Some (C.Rel (1 + lift_amount), subst', metasenv', ugraph',
  58                 (candidate, eq_URI))
  59         in
  60         let c, other, eq_URI =
  61           if pos = Utils.Left then left, right, HL.Logic.eq_ind_URI
  62           else right, left, HL.Logic.eq_ind_r_URI
  63         in
  64         if o <> U.Incomparable then
  65           try
  66             do_match c other eq_URI
  67           with e ->
  68             find_matches metasenv context ugraph lift_amount term tl
  69         else
  70           let res = try do_match c other eq_URI with e -> None in
  71           match res with
  72           | Some (_, s, _, _, _) ->
  73               let c' = M.apply_subst s c
  74               and other' = M.apply_subst s other in
  75               let order = cmp c' other' in
  76               let names = U.names_of_context context in
  77               if order = U.Gt then
  78                 res
  79               else
  80                 find_matches metasenv context ugraph lift_amount term tl
  81           | None ->
  82               find_matches metasenv context ugraph lift_amount term tl
  83 ;;
  84
  85
  86 let rec find_all_matches ?(unif_fun=CicUnification.fo_unif)
  87     metasenv context ugraph lift_amount term =
  88   let module C = Cic in
  89   let module U = Utils in
  90   let module S = CicSubstitution in
  91   let module M = CicMetaSubst in
  92   let module HL = HelmLibraryObjects in
  93   let cmp = !Utils.compare_terms in
  94   let names = Utils.names_of_context context in
  95   function
  96     | [] -> []
  97     | candidate::tl ->
  98         let pos, (proof, (ty, left, right, o), metas, args) = candidate in
  99         let do_match c other eq_URI =
 100           let subst', metasenv', ugraph' =
 101             unif_fun (metasenv @ metas) context
 102               term (S.lift lift_amount c) ugraph
 103           in
 104           (C.Rel (1 + lift_amount), subst', metasenv', ugraph',
 105            (candidate, eq_URI))
 106         in
 107         let c, other, eq_URI =
 108           if pos = Utils.Left then left, right, HL.Logic.eq_ind_URI
 109           else right, left, HL.Logic.eq_ind_r_URI
 110         in
 111         if o <> U.Incomparable then
 112           try
 113             let res = do_match c other eq_URI in
 114             res::(find_all_matches ~unif_fun metasenv context ugraph
 115                     lift_amount term tl)
 116           with e ->
 117             find_all_matches ~unif_fun metasenv context ugraph
 118               lift_amount term tl
 119         else
 120           try
 121             let res = do_match c other eq_URI in
 122             match res with
 123             | _, s, _, _, _ ->
 124                 let c' = M.apply_subst s c
 125                 and other' = M.apply_subst s other in
 126                 let order = cmp c' other' in
 127                 let names = U.names_of_context context in
 128                 if order <> U.Lt && order <> U.Le then
 129                   res::(find_all_matches ~unif_fun metasenv context ugraph
 130                           lift_amount term tl)
 131                 else
 132                   find_all_matches ~unif_fun metasenv context ugraph
 133                     lift_amount term tl
 134           with e ->
 135             find_all_matches ~unif_fun metasenv context ugraph
 136               lift_amount term tl
 137 ;;
 138
 139
 140 let subsumption env table target =
 141   let _, (ty, tl, tr, _), tmetas, _ = target in
 142   let metasenv, context, ugraph = env in
 143   let metasenv = metasenv @ tmetas in
 144   let samesubst subst subst' =
 145     let tbl = Hashtbl.create (List.length subst) in
 146     List.iter (fun (m, (c, t1, t2)) -> Hashtbl.add tbl m (c, t1, t2)) subst;
 147     List.for_all
 148       (fun (m, (c, t1, t2)) ->
 149          try
 150            let c', t1', t2' = Hashtbl.find tbl m in
 151            if (c = c') && (t1 = t1') && (t2 = t2') then true
 152            else false
 153          with Not_found ->
 154            true)
 155       subst'
 156   in
 157   let subsaux left right =
 158     let leftc = get_candidates Matching table left in
 159     let leftr =
 160       find_all_matches ~unif_fun:Inference.matching
 161         metasenv context ugraph 0 left leftc
 162     in
 163     let ok what (_, subst, menv, ug, ((pos, (_, (_, l, r, o), _, _)), _)) =
 164       try
 165         let other = if pos = Utils.Left then r else l in
 166         let subst', menv', ug' =
 167           Inference.matching metasenv context what other ugraph in
 168         samesubst subst subst'
 169       with e ->
 170         false
 171     in
 172     let r = List.exists (ok right) leftr in
 173     if r then
 174       true
 175     else
 176       let rightc = get_candidates Matching table right in
 177       let rightr =
 178         find_all_matches ~unif_fun:Inference.matching
 179           metasenv context ugraph 0 right rightc
 180       in
 181       List.exists (ok left) rightr
 182   in
 183   let res =  subsaux tl tr in
 184   if res then (
 185     Printf.printf "subsumption!:\ntarget: %s\n"
 186       (Inference.string_of_equality ~env target);
 187     print_newline ();
 188   );
 189   res
 190 ;;
 191
 192
 193 let rec demodulate_term metasenv context ugraph table lift_amount term =
 194   let module C = Cic in
 195   let module S = CicSubstitution in
 196   let module M = CicMetaSubst in
 197   let module HL = HelmLibraryObjects in
 198   let candidates = get_candidates Matching table term in
 199   match term with
 200   | C.Meta _ -> None
 201   | term ->
 202       let res =
 203         find_matches metasenv context ugraph lift_amount term candidates
 204       in
 205       if res <> None then
 206         res
 207       else
 208         match term with
 209         | C.Appl l ->
 210             let res, ll =
 211               List.fold_left
 212                 (fun (res, tl) t ->
 213                    if res <> None then
 214                      (res, tl @ [S.lift 1 t])
 215                    else
 216                      let r =
 217                        demodulate_term metasenv context ugraph table
 218                          lift_amount t
 219                      in
 220                      match r with
 221                      | None -> (None, tl @ [S.lift 1 t])
 222                      | Some (rel, _, _, _, _) -> (r, tl @ [rel]))
 223                 (None, []) l
 224             in (
 225               match res with
 226               | None -> None
 227               | Some (_, subst, menv, ug, eq_found) ->
 228                   Some (C.Appl ll, subst, menv, ug, eq_found)
 229             )
 230         | C.Prod (nn, s, t) ->
 231             let r1 =
 232               demodulate_term metasenv context ugraph table lift_amount s in (
 233               match r1 with
 234               | None ->
 235                   let r2 =
 236                     demodulate_term metasenv
 237                       ((Some (nn, C.Decl s))::context) ugraph
 238                       table (lift_amount+1) t
 239                   in (
 240                     match r2 with
 241                     | None -> None
 242                     | Some (t', subst, menv, ug, eq_found) ->
 243                         Some (C.Prod (nn, (S.lift 1 s), t'),
 244                               subst, menv, ug, eq_found)
 245                   )
 246               | Some (s', subst, menv, ug, eq_found) ->
 247                   Some (C.Prod (nn, s', (S.lift 1 t)),
 248                         subst, menv, ug, eq_found)
 249             )
 250         | t ->
 251             None
 252 ;;
 253
 254
 255 let rec demodulation newmeta env table target =
 256   let module C = Cic in
 257   let module S = CicSubstitution in
 258   let module M = CicMetaSubst in
 259   let module HL = HelmLibraryObjects in
 260   let metasenv, context, ugraph = env in
 261   let proof, (eq_ty, left, right, order), metas, args = target in
 262   let metasenv' = metasenv @ metas in
 263   let build_newtarget is_left (t, subst, menv, ug, (eq_found, eq_URI)) =
 264     let pos, (proof', (ty, what, other, _), menv', args') = eq_found in
 265     let what, other = if pos = Utils.Left then what, other else other, what in
 266     let newterm, newproof =
 267       let bo = M.apply_subst subst (S.subst other t) in
 268       let bo'' =
 269         C.Appl ([C.MutInd (HL.Logic.eq_URI, 0, []);
 270                  S.lift 1 eq_ty] @
 271                  if is_left then [bo; S.lift 1 right] else [S.lift 1 left; bo])
 272       in
 273       let t' = C.Lambda (C.Anonymous, ty, bo'') in
 274       bo,
 275       M.apply_subst subst (C.Appl [C.Const (eq_URI, []); ty; what; t';
 276                                    proof; other; proof'])
 277     in
 278     let left, right = if is_left then newterm, right else left, newterm in
 279     let m =
 280       (Inference.metas_of_term left) @ (Inference.metas_of_term right)
 281     in
 282     let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) metas
 283     and newargs =
 284       List.filter
 285         (function C.Meta (i, _) -> List.mem i m | _ -> assert false)
 286         args
 287     in
 288     let ordering = !Utils.compare_terms left right in
 289     newmeta, (newproof, (eq_ty, left, right, ordering), newmetasenv, newargs)
 290   in
 291   let res = demodulate_term metasenv' context ugraph table 0 left in
 292   let build_identity (p, (t, l, r, o), m, a) =
 293     match o with
 294     | Utils.Gt -> (p, (t, r, r, Utils.Eq), m, a)
 295     | _ -> (p, (t, l, l, Utils.Eq), m, a)
 296   in
 297   match res with
 298   | Some t ->
 299       let newmeta, newtarget = build_newtarget true t in
 300       if (Inference.is_identity (metasenv', context, ugraph) newtarget) ||
 301         (Inference.meta_convertibility_eq target newtarget) then
 302           newmeta, newtarget
 303       else
 304         if subsumption env table newtarget then
 305           newmeta, build_identity newtarget
 306         else
 307           demodulation newmeta env table newtarget
 308   | None ->
 309       let res = demodulate_term metasenv' context ugraph table 0 right in
 310       match res with
 311       | Some t ->
 312           let newmeta, newtarget = build_newtarget false t in
 313           if (Inference.is_identity (metasenv', context, ugraph) newtarget) ||
 314             (Inference.meta_convertibility_eq target newtarget) then
 315               newmeta, newtarget
 316           else
 317             if subsumption env table newtarget then
 318               newmeta, build_identity newtarget
 319             else
 320               demodulation newmeta env table newtarget
 321       | None ->
 322           newmeta, target
 323 ;;
 324
 325
 326 let rec betaexpand_term metasenv context ugraph table lift_amount term =
 327   let module C = Cic in
 328   let module S = CicSubstitution in
 329   let module M = CicMetaSubst in
 330   let module HL = HelmLibraryObjects in
 331   let candidates = get_candidates Unification table term in
 332   let res, lifted_term =
 333     match term with
 334     | C.Meta (i, l) ->
 335         let l', lifted_l =
 336           List.fold_right
 337             (fun arg (res, lifted_tl) ->
 338                match arg with
 339                | Some arg ->
 340                    let arg_res, lifted_arg =
 341                      betaexpand_term metasenv context ugraph table
 342                        lift_amount arg in
 343                    let l1 =
 344                      List.map
 345                        (fun (t, s, m, ug, eq_found) ->
 346                           (Some t)::lifted_tl, s, m, ug, eq_found)
 347                        arg_res
 348                    in
 349                    (l1 @
 350                       (List.map
 351                          (fun (l, s, m, ug, eq_found) ->
 352                             (Some lifted_arg)::l, s, m, ug, eq_found)
 353                          res),
 354                     (Some lifted_arg)::lifted_tl)
 355                | None ->
 356                    (List.map
 357                       (fun (r, s, m, ug, eq_found) ->
 358                          None::r, s, m, ug, eq_found) res,
 359                     None::lifted_tl)
 360             ) l ([], [])
 361         in
 362         let e =
 363           List.map
 364             (fun (l, s, m, ug, eq_found) ->
 365                (C.Meta (i, l), s, m, ug, eq_found)) l'
 366         in
 367         e, C.Meta (i, lifted_l)
 368
 369     | C.Rel m ->
 370         [], if m <= lift_amount then C.Rel m else C.Rel (m+1)
 371
 372     | C.Prod (nn, s, t) ->
 373         let l1, lifted_s =
 374           betaexpand_term metasenv context ugraph table lift_amount s in
 375         let l2, lifted_t =
 376           betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
 377             table (lift_amount+1) t in
 378         let l1' =
 379           List.map
 380             (fun (t, s, m, ug, eq_found) ->
 381                C.Prod (nn, t, lifted_t), s, m, ug, eq_found) l1
 382         and l2' =
 383           List.map
 384             (fun (t, s, m, ug, eq_found) ->
 385                C.Prod (nn, lifted_s, t), s, m, ug, eq_found) l2 in
 386         l1' @ l2', C.Prod (nn, lifted_s, lifted_t)
 387
 388     | C.Appl l ->
 389         let l', lifted_l =
 390           List.fold_right
 391             (fun arg (res, lifted_tl) ->
 392                let arg_res, lifted_arg =
 393                  betaexpand_term metasenv context ugraph table lift_amount arg
 394                in
 395                let l1 =
 396                  List.map
 397                    (fun (a, s, m, ug, eq_found) ->
 398                       a::lifted_tl, s, m, ug, eq_found)
 399                    arg_res
 400                in
 401                (l1 @
 402                   (List.map
 403                      (fun (r, s, m, ug, eq_found) ->
 404                         lifted_arg::r, s, m, ug, eq_found)
 405                      res),
 406                 lifted_arg::lifted_tl)
 407             ) l ([], [])
 408         in
 409         (List.map
 410            (fun (l, s, m, ug, eq_found) -> (C.Appl l, s, m, ug, eq_found)) l',
 411          C.Appl lifted_l)
 412
 413     | t -> [], (S.lift lift_amount t)
 414   in
 415   match term with
 416   | C.Meta _ -> res, lifted_term
 417   | term ->
 418       let r =
 419         find_all_matches metasenv context ugraph lift_amount term candidates
 420       in
 421       r @ res, lifted_term
 422 ;;
 423
 424
 425 let superposition_left (metasenv, context, ugraph) table target =
 426   let module C = Cic in
 427   let module S = CicSubstitution in
 428   let module M = CicMetaSubst in
 429   let module HL = HelmLibraryObjects in
 430   let module CR = CicReduction in
 431   let module U = Utils in
 432   let proof, (eq_ty, left, right, ordering), _, _ = target in
 433   let expansions, _ =
 434     let term = if ordering = U.Gt then left else right in
 435     betaexpand_term metasenv context ugraph table 0 term
 436   in
 437   let build_new (bo, s, m, ug, (eq_found, eq_URI)) =
 438     let pos, (proof', (ty, what, other, _), menv', args') = eq_found in
 439     let what, other = if pos = Utils.Left then what, other else other, what in
 440     let newgoal, newproof =
 441       let bo' = M.apply_subst s (S.subst other bo) in
 442       let bo'' =
 443         C.Appl (
 444           [C.MutInd (HL.Logic.eq_URI, 0, []);
 445            S.lift 1 eq_ty] @
 446             if ordering = U.Gt then [bo'; S.lift 1 right]
 447             else [S.lift 1 left; bo'])
 448       in
 449       let t' = C.Lambda (C.Anonymous, ty, bo'') in
 450       bo',
 451       M.apply_subst s
 452         (C.Appl [C.Const (eq_URI, []); ty; what; t';
 453                  proof; other; proof'])
 454     in
 455     let left, right =
 456       if ordering = U.Gt then newgoal, right else left, newgoal in
 457     let neworder = !Utils.compare_terms left right in
 458     (newproof, (eq_ty, left, right, neworder), [], [])
 459   in
 460   List.map build_new expansions
 461 ;;
 462
 463
 464 let superposition_right newmeta (metasenv, context, ugraph) table target =
 465   let module C = Cic in
 466   let module S = CicSubstitution in
 467   let module M = CicMetaSubst in
 468   let module HL = HelmLibraryObjects in
 469   let module CR = CicReduction in
 470   let module U = Utils in
 471   let eqproof, (eq_ty, left, right, ordering), newmetas, args = target in
 472   let metasenv' = metasenv @ newmetas in
 473   let maxmeta = ref newmeta in
 474   let res1, res2 =
 475     match ordering with
 476     | U.Gt -> fst (betaexpand_term metasenv' context ugraph table 0 left), []
 477     | U.Lt -> [], fst (betaexpand_term metasenv' context ugraph table 0 right)
 478     | _ ->
 479         let res l r =
 480           List.filter
 481             (fun (_, subst, _, _, _) ->
 482                let subst = M.apply_subst subst in
 483                let o = !Utils.compare_terms (subst l) (subst r) in
 484                o <> U.Lt && o <> U.Le)
 485             (fst (betaexpand_term metasenv' context ugraph table 0 l))
 486         in
 487         (res left right), (res right left)
 488   in
 489   let build_new ordering (bo, s, m, ug, (eq_found, eq_URI)) =
 490     let pos, (proof', (ty, what, other, _), menv', args') = eq_found in
 491     let what, other = if pos = Utils.Left then what, other else other, what in
 492     let newgoal, newproof =
 493       let bo' = M.apply_subst s (S.subst other bo) in
 494       let bo'' =
 495         C.Appl (
 496           [C.MutInd (HL.Logic.eq_URI, 0, []); S.lift 1 eq_ty] @
 497             if ordering = U.Gt then [bo'; S.lift 1 right]
 498             else [S.lift 1 left; bo'])
 499       in
 500       let t' = C.Lambda (C.Anonymous, ty, bo'') in
 501       bo',
 502       M.apply_subst s
 503         (C.Appl [C.Const (eq_URI, []); ty; what; t';
 504                  eqproof; other; proof'])
 505     in
 506     let newmeta, newequality =
 507       let left, right =
 508         if ordering = U.Gt then newgoal, M.apply_subst s right
 509         else M.apply_subst s left, newgoal in
 510       let neworder = !Utils.compare_terms left right
 511       and newmenv = newmetas @ menv'
 512       and newargs = args @ args' in
 513       let eq' = (newproof, (eq_ty, left, right, neworder), newmenv, newargs)
 514       and env = (metasenv, context, ugraph) in
 515       let newm, eq' = Inference.fix_metas !maxmeta eq' in
 516       newm, eq'
 517     in
 518     maxmeta := newmeta;
 519     newequality
 520   in
 521   let new1 = List.map (build_new U.Gt) res1
 522   and new2 = List.map (build_new U.Lt) res2 in
 523   let ok = function
 524     | _, (_, left, right, _), _, _ ->
 525         not (fst (CR.are_convertible context left right ugraph))
 526   in
 527   (!maxmeta,
 528    (List.filter ok (new1 @ new2)))
 529 ;;