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     | (pos, (proof, (ty, left, right, o), metas, args))::tl ->
  66         let do_match c other eq_URI =
  67           Printf.printf "provo con %s: %s, %s\n\n"
  68             (if unif_fun == Inference.matching then "MATCHING"
  69              else if unif_fun == CicUnification.fo_unif then "UNIFICATION"
  70              else "??????????")
  71             (CicPp.pp term names)
  72             (CicPp.pp (S.lift lift_amount c) names);
  73           let subst', metasenv', ugraph' =
  74 (*             Inference.matching (metasenv @ metas) context term *)
  75 (*               (S.lift lift_amount c) ugraph *)
  76             unif_fun (metasenv @ metas) context
  77               term (S.lift lift_amount c) ugraph
  78           in
  79 (*           let names = U.names_of_context context in *)
  80           Printf.printf "MATCH FOUND: %s, %s\n"
  81             (CicPp.pp term names) (CicPp.pp (S.lift lift_amount c) names);
  82           Some (C.Rel (1 + lift_amount), subst', metasenv', ugraph',
  83                 (proof, ty, c, other, eq_URI))
  84         in
  85         let c, other, eq_URI =
  86           if pos = Left then left, right, HL.Logic.eq_ind_URI
  87           else right, left, HL.Logic.eq_ind_r_URI
  88         in
  89         if o <> U.Incomparable then
  90           try
  91             print_endline "SONO QUI!";
  92             let res = do_match c other eq_URI in
  93             print_endline "RITORNO RES";
  94             res
  95           with e ->
  96             Printf.printf "ERRORE!: %s\n" (Printexc.to_string e);
  97             find_matches unif_fun metasenv context ugraph lift_amount term tl
  98         else
  99           let res =
 100             try
 101               let res = do_match c other eq_URI in
 102               print_endline "RITORNO RES 2";
 103               res
 104             with e -> None in
 105           match res with
 106           | Some (_, s, _, _, _) ->
 107               let c' = M.apply_subst s c
 108               and other' = M.apply_subst s other in
 109               let order = cmp c' other' in
 110               let names = U.names_of_context context in
 111               Printf.printf "c': %s\nother': %s\norder: %s\n\n"
 112                 (CicPp.pp c' names) (CicPp.pp other' names)
 113                 (U.string_of_comparison order);
 114 (*               if cmp (M.apply_subst s c) (M.apply_subst s other) = U.Gt then *)
 115               if order = U.Gt then
 116                 res
 117               else
 118                 find_matches unif_fun metasenv context ugraph
 119                   lift_amount term tl
 120           | None ->
 121               find_matches unif_fun metasenv context ugraph lift_amount term tl
 122 ;;
 123
 124
 125 let rec demodulate_term metasenv context ugraph table lift_amount term =
 126   let module C = Cic in
 127   let module S = CicSubstitution in
 128   let module M = CicMetaSubst in
 129   let module HL = HelmLibraryObjects in
 130   let hd_term = head_of_term term in
 131   let candidates = try Hashtbl.find table hd_term with Not_found -> [] in
 132   match term with
 133   | C.Meta _ -> None
 134   | term ->
 135       let res =
 136         find_matches Inference.matching metasenv context ugraph
 137           lift_amount term candidates
 138       in
 139       if res <> None then
 140         res
 141       else
 142         match term with
 143         | C.Appl l ->
 144             let res, ll =
 145               List.fold_left
 146                 (fun (res, tl) t ->
 147                    if res <> None then
 148                      (res, tl @ [S.lift 1 t])
 149                    else
 150                      let r =
 151                        demodulate_term metasenv context ugraph table
 152                          lift_amount t
 153                      in
 154                      match r with
 155                      | None -> (None, tl @ [S.lift 1 t])
 156                      | Some (rel, _, _, _, _) -> (r, tl @ [rel]))
 157                 (None, []) l
 158             in (
 159               match res with
 160               | None -> None
 161               | Some (_, subst, menv, ug, info) ->
 162                   Some (C.Appl ll, subst, menv, ug, info)
 163             )
 164         | C.Prod (nn, s, t) ->
 165             let r1 =
 166               demodulate_term metasenv context ugraph table lift_amount s in (
 167               match r1 with
 168               | None ->
 169                   let r2 =
 170                     demodulate_term metasenv
 171                       ((Some (nn, C.Decl s))::context) ugraph
 172                       table (lift_amount+1) t
 173                   in (
 174                     match r2 with
 175                     | None -> None
 176                     | Some (t', subst, menv, ug, info) ->
 177                         Some (C.Prod (nn, (S.lift 1 s), t'),
 178                               subst, menv, ug, info)
 179                   )
 180               | Some (s', subst, menv, ug, info) ->
 181                   Some (C.Prod (nn, s', (S.lift 1 t)), subst, menv, ug, info)
 182             )
 183         | t ->
 184 (*             Printf.printf "Ne` Appl ne` Prod: %s\n" *)
 185 (*               (CicPp.pp t (Utils.names_of_context context)); *)
 186             None
 187 ;;
 188
 189
 190 let rec demodulate newmeta env table target =
 191   let module C = Cic in
 192   let module S = CicSubstitution in
 193   let module M = CicMetaSubst in
 194   let module HL = HelmLibraryObjects in
 195   print_endline "\n\ndemodulate";
 196   let metasenv, context, ugraph = env in
 197   let proof, (eq_ty, left, right, order), metas, args = target in
 198   let metasenv' = metasenv @ metas in
 199   let build_newtarget is_left
 200       (t, subst, menv, ug, (proof', ty, what, other, eq_URI)) =
 201     let newterm, newproof =
 202       let bo = S.subst (M.apply_subst subst other) t in
 203       let bo'' =
 204         C.Appl ([C.MutInd (HL.Logic.eq_URI, 0, []);
 205                  S.lift 1 eq_ty] @
 206                  if is_left then [bo; S.lift 1 right] else [S.lift 1 left; bo])
 207       in
 208       let t' = C.Lambda (C.Anonymous, ty, bo'') in
 209       bo,
 210       M.apply_subst subst (C.Appl [C.Const (eq_URI, []); ty; what; t';
 211                                    proof; other; proof'])
 212     in
 213     let newmeta, newtarget =
 214       let left, right = if is_left then newterm, right else left, newterm in
 215       let m =
 216         (Inference.metas_of_term left) @ (Inference.metas_of_term right)
 217       in
 218       let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) metas
 219       and newargs =
 220         List.filter
 221           (function C.Meta (i, _) -> List.mem i m | _ -> assert false)
 222           args
 223       in
 224       let ordering = !Utils.compare_terms left right in
 225       newmeta, (newproof, (eq_ty, left, right, ordering), newmetasenv, newargs)
 226     in
 227     newmeta, newtarget
 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 then
 234         newmeta, newtarget
 235       else
 236         demodulate newmeta env table newtarget
 237   | None ->
 238       let res = demodulate_term metasenv' context ugraph table 0 right in
 239       match res with
 240       | Some t ->
 241           let newmeta, newtarget = build_newtarget false t in
 242           if Inference.is_identity (metasenv', context, ugraph) newtarget then
 243             newmeta, newtarget
 244           else
 245             demodulate newmeta env table newtarget
 246       | None ->
 247           newmeta, target
 248 ;;
 249
 250
 251 let rec betaexpand_term metasenv context ugraph table lift_amount term =
 252   let module C = Cic in
 253   let module S = CicSubstitution in
 254   let module M = CicMetaSubst in
 255   let module HL = HelmLibraryObjects in
 256   let hd_term = head_of_term term in
 257   let candidates = try Hashtbl.find table hd_term with Not_found -> [] in
 258   let res, lifted_term =
 259     match term with
 260     | C.Meta (i, l) ->
 261         let l =
 262           List.map (function
 263                       | Some t -> Some (S.lift lift_amount t)
 264                       | None -> None) l
 265         in
 266         [], C.Meta (i, l)
 267
 268     | C.Rel m ->
 269         [], if m <= lift_amount then C.Rel m else C.Rel (m+1)
 270
 271     | C.Prod (nn, s, t) ->
 272         let l1, lifted_s =
 273           betaexpand_term metasenv context ugraph table lift_amount s in
 274         let l2, lifted_t =
 275           betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
 276             table (lift_amount+1) t in
 277         let l1' =
 278           List.map
 279             (fun (t, s, m, ug, info) ->
 280                C.Prod (nn, t, lifted_t), s, m, ug, info) l1
 281         and l2' =
 282           List.map
 283             (fun (t, s, m, ug, info) ->
 284                C.Prod (nn, lifted_s, t), s, m, ug, info) l2 in
 285         l1' @ l2', C.Prod (nn, lifted_s, lifted_t)
 286
 287     | C.Appl l ->
 288         let l', lifted_l =
 289           List.fold_right
 290             (fun arg (res, lifted_tl) ->
 291                let arg_res, lifted_arg =
 292                  betaexpand_term metasenv context ugraph table lift_amount arg
 293                in
 294                let l1 =
 295                  List.map
 296                    (fun (a, s, m, ug, info) -> a::lifted_tl, s, m, ug, info)
 297                    arg_res
 298                in
 299                (l1 @
 300                   (List.map
 301                      (fun (r, s, m, ug, info) -> lifted_arg::r, s, m, ug, info)
 302                      res),
 303                 lifted_arg::lifted_tl)
 304             ) l ([], [])
 305         in
 306         (List.map (fun (l, s, m, ug, info) -> (C.Appl l, s, m, ug, info)) l',
 307          C.Appl lifted_l)
 308
 309     | t -> [], (S.lift lift_amount t)
 310   in
 311   match term with
 312   | C.Meta _ -> res, lifted_term
 313   | _ ->
 314 (*       let names = Utils.names_of_context context in *)
 315 (*       Printf.printf "CHIAMO find_matches su: %s\n" (CicPp.pp term names); *)
 316       match
 317         find_matches CicUnification.fo_unif metasenv context ugraph
 318           lift_amount term candidates
 319       with
 320       | None -> res, lifted_term
 321       | Some r ->
 322 (*           let _, _, _, _, (_, _, what, _, _) = r in *)
 323 (*           Printf.printf "OK, aggiungo a res: %s\n" (CicPp.pp what names); *)
 324           r::res, lifted_term
 325 ;;
 326
 327
 328 let superposition_left (metasenv, context, ugraph) table target =
 329   let module C = Cic in
 330   let module S = CicSubstitution in
 331   let module M = CicMetaSubst in
 332   let module HL = HelmLibraryObjects in
 333   let module CR = CicReduction in
 334   let module U = Utils in
 335   print_endline "\n\nsuperposition_left";
 336   let proof, (eq_ty, left, right, ordering), _, _ = target in
 337   let expansions, _ =
 338     let term = if ordering = U.Gt then left else right in
 339     let res =
 340       betaexpand_term metasenv context ugraph table 0 term in
 341 (*     let names = U.names_of_context context in *)
 342 (*     Printf.printf "\n\nsuperposition_left: %s\n%s\n" *)
 343 (*       (CicPp.pp term names) *)
 344 (*       (String.concat "\n" *)
 345 (*          (List.map *)
 346 (*             (fun (_, _, _, _, (_, _, what, _, _)) -> CicPp.pp what names) *)
 347 (*             (fst res))); *)
 348     res
 349   in
 350   let build_new (bo, s, m, ug, (proof', ty, what, other, eq_URI)) =
 351     let newgoal, newproof =
 352       let bo' = S.subst (M.apply_subst s other) bo in
 353       let bo'' =
 354         C.Appl (
 355           [C.MutInd (HL.Logic.eq_URI, 0, []);
 356            S.lift 1 eq_ty] @
 357             if ordering = U.Gt then [bo'; S.lift 1 right]
 358             else [S.lift 1 left; bo'])
 359       in
 360       let t' = C.Lambda (C.Anonymous, ty, bo'') in
 361       S.subst (M.apply_subst s other) bo,
 362       M.apply_subst s
 363         (C.Appl [C.Const (eq_URI, []); ty; what; t';
 364                  proof; other; proof'])
 365     in
 366     let left, right, newordering =
 367       if ordering = U.Gt then
 368         newgoal, right, !Utils.compare_terms newgoal right
 369       else
 370         left, newgoal, !Utils.compare_terms left newgoal
 371     in
 372     (newproof, (eq_ty, left, right, ordering), [], [])
 373   in
 374   List.map build_new expansions
 375 ;;
 376
 377
 378 let superposition_right newmeta (metasenv, context, ugraph) table target =
 379   let module C = Cic in
 380   let module S = CicSubstitution in
 381   let module M = CicMetaSubst in
 382   let module HL = HelmLibraryObjects in
 383   let module CR = CicReduction in
 384   let module U = Utils in
 385   print_endline "\n\nsuperposition_right";
 386   let eqproof, (eq_ty, left, right, ordering), newmetas, args = target in
 387   let metasenv' = metasenv @ newmetas in
 388   let maxmeta = ref newmeta in
 389   let res1, res2 =
 390     match ordering with
 391     | U.Gt -> fst (betaexpand_term metasenv' context ugraph table 0 left), []
 392     | U.Lt -> [], fst (betaexpand_term metasenv' context ugraph table 0 right)
 393     | _ ->
 394         let res l r =
 395           List.filter
 396             (fun (_, subst, _, _, _) ->
 397                let subst = M.apply_subst subst in
 398                let o = !Utils.compare_terms (subst l) (subst r) in
 399                o <> U.Lt && o <> U.Le)
 400             (fst (betaexpand_term metasenv' context ugraph table 0 l))
 401         in
 402         (res left right), (res right left)
 403   in
 404   let build_new ordering (bo, s, m, ug, (proof', ty, what, other, eq_URI)) =
 405     let newgoal, newproof =
 406       let bo' = S.subst (M.apply_subst s other) bo in
 407       let bo'' =
 408         C.Appl (
 409           [C.MutInd (HL.Logic.eq_URI, 0, []);
 410            S.lift 1 eq_ty] @
 411             if ordering = U.Gt then [bo'; S.lift 1 right]
 412             else [S.lift 1 left; bo'])
 413       in
 414       let t' = C.Lambda (C.Anonymous, ty, bo'') in
 415       S.subst (M.apply_subst s other) bo,
 416       M.apply_subst s
 417         (C.Appl [C.Const (eq_URI, []); ty; what; t';
 418                  eqproof; other; proof'])
 419     in
 420     let newmeta, newequality =
 421       let left, right, newordering =
 422         if ordering = U.Gt then
 423           newgoal, right, !Utils.compare_terms newgoal right
 424         else
 425           left, newgoal, !Utils.compare_terms left newgoal
 426       in
 427       Inference.fix_metas !maxmeta
 428         (newproof, (eq_ty, left, right, ordering), [], [])
 429     in
 430     maxmeta := newmeta;
 431     newequality
 432   in
 433   let new1 = List.map (build_new U.Gt) res1
 434   and new2 = List.map (build_new U.Lt) res2 in
 435   let ok = function
 436     | _, (_, left, right, _), _, _ ->
 437         not (fst (CR.are_convertible context left right ugraph))
 438   in
 439   (!maxmeta,
 440    (List.filter ok (new1 @ new2)))
 441 ;;