helm/ocaml/paramodulation/indexing.ml

   1 (* type naif_indexing =
   2     (Cic.term * ((bool * Inference.equality) list)) list
   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 unif_fun 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             unif_fun (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 unif_fun 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 unif_fun metasenv context ugraph
 116                   lift_amount term tl
 117           | None ->
 118               find_matches unif_fun metasenv context ugraph lift_amount term tl
 119 ;;
 120
 121
 122 let rec demodulate_term metasenv context ugraph table lift_amount term =
 123   let module C = Cic in
 124   let module S = CicSubstitution in
 125   let module M = CicMetaSubst in
 126   let module HL = HelmLibraryObjects in
 127   let hd_term = head_of_term term in
 128   let candidates = try Hashtbl.find table hd_term with Not_found -> [] in
 129   match term with
 130   | C.Meta _ -> None
 131   | term ->
 132       let res =
 133         find_matches Inference.matching metasenv context ugraph
 134           lift_amount term candidates
 135       in
 136       if res <> None then
 137         res
 138       else
 139         match term with
 140         | C.Appl l ->
 141             let res, ll =
 142               List.fold_left
 143                 (fun (res, tl) t ->
 144                    if res <> None then
 145                      (res, tl @ [S.lift 1 t])
 146                    else
 147                      let r =
 148                        demodulate_term metasenv context ugraph table
 149                          lift_amount t
 150                      in
 151                      match r with
 152                      | None -> (None, tl @ [S.lift 1 t])
 153                      | Some (rel, _, _, _, _) -> (r, tl @ [rel]))
 154                 (None, []) l
 155             in (
 156               match res with
 157               | None -> None
 158               | Some (_, subst, menv, ug, eq_found) ->
 159                   Some (C.Appl ll, subst, menv, ug, eq_found)
 160             )
 161         | C.Prod (nn, s, t) ->
 162             let r1 =
 163               demodulate_term metasenv context ugraph table lift_amount s in (
 164               match r1 with
 165               | None ->
 166                   let r2 =
 167                     demodulate_term metasenv
 168                       ((Some (nn, C.Decl s))::context) ugraph
 169                       table (lift_amount+1) t
 170                   in (
 171                     match r2 with
 172                     | None -> None
 173                     | Some (t', subst, menv, ug, eq_found) ->
 174                         Some (C.Prod (nn, (S.lift 1 s), t'),
 175                               subst, menv, ug, eq_found)
 176                   )
 177               | Some (s', subst, menv, ug, eq_found) ->
 178                   Some (C.Prod (nn, s', (S.lift 1 t)),
 179                         subst, menv, ug, eq_found)
 180             )
 181         | t ->
 182 (*             Printf.printf "Ne` Appl ne` Prod: %s\n" *)
 183 (*               (CicPp.pp t (Utils.names_of_context context)); *)
 184             None
 185 ;;
 186
 187
 188 let rec demodulation newmeta env table target =
 189   let module C = Cic in
 190   let module S = CicSubstitution in
 191   let module M = CicMetaSubst in
 192   let module HL = HelmLibraryObjects in
 193   let metasenv, context, ugraph = env in
 194   let proof, (eq_ty, left, right, order), metas, args = target in
 195 (*   let _ = *)
 196 (*     let names = Utils.names_of_context context in *)
 197 (*     Printf.printf "demodulation %s = %s\n" *)
 198 (*       (CicPp.pp left names) (CicPp.pp right names) *)
 199 (*   in *)
 200   let metasenv' = metasenv @ metas in
 201   let build_newtarget is_left (t, subst, menv, ug, (eq_found, eq_URI)) =
 202     let pos, (proof', (ty, what, other, _), menv', args') = eq_found in
 203     let what, other = if pos = Left then what, other else other, what in
 204     let newterm, newproof =
 205       let bo = M.apply_subst subst (S.subst other t) in
 206       let bo'' =
 207         C.Appl ([C.MutInd (HL.Logic.eq_URI, 0, []);
 208                  S.lift 1 eq_ty] @
 209                  if is_left then [bo; S.lift 1 right] else [S.lift 1 left; bo])
 210       in
 211       let t' = C.Lambda (C.Anonymous, ty, bo'') in
 212       bo,
 213       M.apply_subst subst (C.Appl [C.Const (eq_URI, []); ty; what; t';
 214                                    proof; other; proof'])
 215     in
 216     let left, right = if is_left then newterm, right else left, newterm in
 217     let m =
 218       (Inference.metas_of_term left) @ (Inference.metas_of_term right)
 219     in
 220     let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) metas
 221     and newargs =
 222       List.filter
 223         (function C.Meta (i, _) -> List.mem i m | _ -> assert false)
 224         args
 225     in
 226     let ordering = !Utils.compare_terms left right in
 227     newmeta, (newproof, (eq_ty, left, right, ordering), newmetasenv, newargs)
 228   in
 229   let res = demodulate_term metasenv' context ugraph table 0 left in
 230   match res with
 231   | Some t ->
 232       let newmeta, newtarget = build_newtarget true t in
 233       if (Inference.is_identity (metasenv', context, ugraph) newtarget) ||
 234         (Inference.meta_convertibility_eq target newtarget) then
 235           newmeta, newtarget
 236       else (
 237 (*         Printf.printf "Going on 1:\ntarget: %s\nnewtarget: %s\n%s\n\n" *)
 238 (*           (Inference.string_of_equality ~env target) *)
 239 (*           (Inference.string_of_equality ~env newtarget) *)
 240 (*           (string_of_bool (target = newtarget)); *)
 241         demodulation newmeta env table newtarget
 242       )
 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 (*             Printf.printf "Going on 2:\ntarget: %s\nnewtarget: %s\n\n" *)
 253 (*               (Inference.string_of_equality ~env target) *)
 254 (*               (Inference.string_of_equality ~env newtarget); *)
 255             demodulation newmeta env table newtarget
 256           )
 257       | None ->
 258           newmeta, target
 259 ;;
 260
 261
 262 let rec find_all_matches metasenv context ugraph lift_amount term =
 263   let module C = Cic in
 264   let module U = Utils in
 265   let module S = CicSubstitution in
 266   let module M = CicMetaSubst in
 267   let module HL = HelmLibraryObjects in
 268   let cmp = !Utils.compare_terms in
 269   let names = Utils.names_of_context context in
 270   function
 271     | [] -> []
 272     | candidate::tl ->
 273         let pos, (proof, (ty, left, right, o), metas, args) = candidate in
 274         let do_match c other eq_URI =
 275           let subst', metasenv', ugraph' =
 276             CicUnification.fo_unif (metasenv @ metas) context
 277               term (S.lift lift_amount c) ugraph
 278           in
 279           (C.Rel (1 + lift_amount), subst', metasenv', ugraph',
 280            (candidate, eq_URI))
 281         in
 282         let c, other, eq_URI =
 283           if pos = Left then left, right, HL.Logic.eq_ind_URI
 284           else right, left, HL.Logic.eq_ind_r_URI
 285         in
 286         if o <> U.Incomparable then
 287           try
 288             let res = do_match c other eq_URI in
 289             res::(find_all_matches metasenv context ugraph lift_amount term tl)
 290           with e ->
 291             find_all_matches metasenv context ugraph lift_amount term tl
 292         else
 293           try
 294             let res = do_match c other eq_URI in
 295             match res with
 296             | _, s, _, _, _ ->
 297                 let c' = M.apply_subst s c
 298                 and other' = M.apply_subst s other in
 299                 let order = cmp c' other' in
 300                 let names = U.names_of_context context in
 301                 if order <> U.Lt && order <> U.Le then
 302                   res::(find_all_matches metasenv context ugraph
 303                           lift_amount term tl)
 304                 else
 305                   find_all_matches metasenv context ugraph lift_amount term tl
 306           with e ->
 307             find_all_matches metasenv context ugraph lift_amount term tl
 308 ;;
 309
 310
 311 let rec betaexpand_term metasenv context ugraph table lift_amount term =
 312   let module C = Cic in
 313   let module S = CicSubstitution in
 314   let module M = CicMetaSubst in
 315   let module HL = HelmLibraryObjects in
 316   let hd_term = head_of_term term in
 317   let candidates = try Hashtbl.find table hd_term with Not_found -> [] in
 318   let res, lifted_term =
 319     match term with
 320     | C.Meta (i, l) ->
 321         let l', lifted_l =
 322           List.fold_right
 323             (fun arg (res, lifted_tl) ->
 324                match arg with
 325                | Some arg ->
 326                    let arg_res, lifted_arg =
 327                      betaexpand_term metasenv context ugraph table
 328                        lift_amount arg in
 329                    let l1 =
 330                      List.map
 331                        (fun (t, s, m, ug, eq_found) ->
 332                           (Some t)::lifted_tl, s, m, ug, eq_found)
 333                        arg_res
 334                    in
 335                    (l1 @
 336                       (List.map
 337                          (fun (l, s, m, ug, eq_found) ->
 338                             (Some lifted_arg)::l, s, m, ug, eq_found)
 339                          res),
 340                     (Some lifted_arg)::lifted_tl)
 341                | None ->
 342                    (List.map
 343                       (fun (r, s, m, ug, eq_found) ->
 344                          None::r, s, m, ug, eq_found) res,
 345                     None::lifted_tl)
 346             ) l ([], [])
 347         in
 348         let e =
 349           List.map
 350             (fun (l, s, m, ug, eq_found) ->
 351                (C.Meta (i, l), s, m, ug, eq_found)) l'
 352         in
 353         e, C.Meta (i, lifted_l)
 354
 355     | C.Rel m ->
 356         [], if m <= lift_amount then C.Rel m else C.Rel (m+1)
 357
 358     | C.Prod (nn, s, t) ->
 359         let l1, lifted_s =
 360           betaexpand_term metasenv context ugraph table lift_amount s in
 361         let l2, lifted_t =
 362           betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
 363             table (lift_amount+1) t in
 364         let l1' =
 365           List.map
 366             (fun (t, s, m, ug, eq_found) ->
 367                C.Prod (nn, t, lifted_t), s, m, ug, eq_found) l1
 368         and l2' =
 369           List.map
 370             (fun (t, s, m, ug, eq_found) ->
 371                C.Prod (nn, lifted_s, t), s, m, ug, eq_found) l2 in
 372         l1' @ l2', C.Prod (nn, lifted_s, lifted_t)
 373
 374     | C.Appl l ->
 375         let l', lifted_l =
 376           List.fold_right
 377             (fun arg (res, lifted_tl) ->
 378                let arg_res, lifted_arg =
 379                  betaexpand_term metasenv context ugraph table lift_amount arg
 380                in
 381                let l1 =
 382                  List.map
 383                    (fun (a, s, m, ug, eq_found) ->
 384                       a::lifted_tl, s, m, ug, eq_found)
 385                    arg_res
 386                in
 387                (l1 @
 388                   (List.map
 389                      (fun (r, s, m, ug, eq_found) ->
 390                         lifted_arg::r, s, m, ug, eq_found)
 391                      res),
 392                 lifted_arg::lifted_tl)
 393             ) l ([], [])
 394         in
 395         (List.map
 396            (fun (l, s, m, ug, eq_found) -> (C.Appl l, s, m, ug, eq_found)) l',
 397          C.Appl lifted_l)
 398
 399     | t -> [], (S.lift lift_amount t)
 400   in
 401   match term with
 402   | C.Meta _ -> res, lifted_term
 403   | term ->
 404 (*       let names = Utils.names_of_context context in *)
 405 (*       Printf.printf "CHIAMO find_all_matches su: %s\n" (CicPp.pp term names); *)
 406       let r =
 407         find_all_matches metasenv context ugraph lift_amount term candidates
 408       in
 409       r @ res, lifted_term
 410 (*       match *)
 411 (*         find_all_matches metasenv context ugraph lift_amount term candidates *)
 412 (*       with *)
 413 (*       | None -> res, lifted_term *)
 414 (*       | Some r -> *)
 415 (*           r::res, lifted_term *)
 416 ;;
 417
 418
 419 let superposition_left (metasenv, context, ugraph) table target =
 420   let module C = Cic in
 421   let module S = CicSubstitution in
 422   let module M = CicMetaSubst in
 423   let module HL = HelmLibraryObjects in
 424   let module CR = CicReduction in
 425   let module U = Utils in
 426 (*   print_endline "superposition_left"; *)
 427   let proof, (eq_ty, left, right, ordering), _, _ = target in
 428   let expansions, _ =
 429     let term = if ordering = U.Gt then left else right in
 430     betaexpand_term metasenv context ugraph table 0 term
 431   in
 432   let build_new (bo, s, m, ug, (eq_found, eq_URI)) =
 433     let pos, (proof', (ty, what, other, _), menv', args') = eq_found in
 434     let what, other = if pos = Left then what, other else other, what in
 435     let newgoal, newproof =
 436       let bo' = M.apply_subst s (S.subst other bo) in
 437       let bo'' =
 438         C.Appl (
 439           [C.MutInd (HL.Logic.eq_URI, 0, []);
 440            S.lift 1 eq_ty] @
 441             if ordering = U.Gt then [bo'; S.lift 1 right]
 442             else [S.lift 1 left; bo'])
 443       in
 444       let t' = C.Lambda (C.Anonymous, ty, bo'') in
 445       bo',
 446       M.apply_subst s
 447         (C.Appl [C.Const (eq_URI, []); ty; what; t';
 448                  proof; other; proof'])
 449     in
 450     let left, right =
 451       if ordering = U.Gt then newgoal, right else left, newgoal in
 452     let neworder = !Utils.compare_terms left right in
 453     (newproof, (eq_ty, left, right, neworder), [], [])
 454   in
 455   List.map build_new expansions
 456 ;;
 457
 458
 459 let superposition_right newmeta (metasenv, context, ugraph) table target =
 460   let module C = Cic in
 461   let module S = CicSubstitution in
 462   let module M = CicMetaSubst in
 463   let module HL = HelmLibraryObjects in
 464   let module CR = CicReduction in
 465   let module U = Utils in
 466 (*   print_endline "superposition_right"; *)
 467   let eqproof, (eq_ty, left, right, ordering), newmetas, args = target in
 468   let metasenv' = metasenv @ newmetas in
 469   let maxmeta = ref newmeta in
 470   let res1, res2 =
 471     match ordering with
 472     | U.Gt -> fst (betaexpand_term metasenv' context ugraph table 0 left), []
 473     | U.Lt -> [], fst (betaexpand_term metasenv' context ugraph table 0 right)
 474     | _ ->
 475         let res l r =
 476           List.filter
 477             (fun (_, subst, _, _, _) ->
 478                let subst = M.apply_subst subst in
 479                let o = !Utils.compare_terms (subst l) (subst r) in
 480                o <> U.Lt && o <> U.Le)
 481             (fst (betaexpand_term metasenv' context ugraph table 0 l))
 482         in
 483         (res left right), (res right left)
 484   in
 485   let build_new ordering (bo, s, m, ug, (eq_found, eq_URI)) =
 486     let pos, (proof', (ty, what, other, _), menv', args') = eq_found in
 487     let what, other = if pos = Left then what, other else other, what in
 488     let newgoal, newproof =
 489       let bo' = M.apply_subst s (S.subst other bo) in
 490       let bo'' =
 491         C.Appl (
 492           [C.MutInd (HL.Logic.eq_URI, 0, []); S.lift 1 eq_ty] @
 493             if ordering = U.Gt then [bo'; S.lift 1 right]
 494             else [S.lift 1 left; bo'])
 495       in
 496       let t' = C.Lambda (C.Anonymous, ty, bo'') in
 497       bo',
 498       M.apply_subst s
 499         (C.Appl [C.Const (eq_URI, []); ty; what; t';
 500                  eqproof; other; proof'])
 501     in
 502     let newmeta, newequality =
 503       let left, right =
 504         if ordering = U.Gt then newgoal, M.apply_subst s right
 505         else M.apply_subst s left, newgoal in
 506       let neworder = !Utils.compare_terms left right
 507       and newmenv = newmetas @ menv'
 508       and newargs = args @ args' in
 509       let eq' = (newproof, (eq_ty, left, right, neworder), newmenv, newargs)
 510       and env = (metasenv, context, ugraph) in
 511 (*       Printf.printf "eq' prima di fix_metas: %s\n" *)
 512 (*         (Inference.string_of_equality eq' ~env); *)
 513       let newm, eq' = Inference.fix_metas !maxmeta eq' in
 514 (*       Printf.printf "eq' dopo fix_metas: %s\n" *)
 515 (*         (Inference.string_of_equality eq' ~env); *)
 516       newm, eq'
 517     in
 518     maxmeta := newmeta;
 519     newequality
 520   in
 521   let new1 = List.map (build_new U.Gt) res1
 522   and new2 = List.map (build_new U.Lt) res2 in
 523   let ok = function
 524     | _, (_, left, right, _), _, _ ->
 525         not (fst (CR.are_convertible context left right ugraph))
 526   in
 527   (!maxmeta,
 528    (List.filter ok (new1 @ new2)))
 529 ;;