helm/ocaml/paramodulation/indexing.ml

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