helm/ocaml/paramodulation/indexing.ml

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