helm/ocaml/paramodulation/indexing.ml

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