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