helm/ocaml/paramodulation/indexing.ml

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