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 (sign, 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, sign, eq)::x_entry)
  20   in
  21 (*   (match ordering with *)
  22 (*    | Utils.Gt ->  *)
  23 (*        index hl Left *)
  24 (*    | Utils.Lt ->  *)
  25 (*        index hr Right *)
  26 (*    | _ -> index hl Left; *)
  27 (*        index hr Right); *)
  28   index hl Left;
  29   index hr Right;
  30   table
  31 ;;
  32
  33
  34 let remove_index table (sign, eq) =
  35   let _, (_, l, r, ordering), _, _ = eq in
  36   let hl = head_of_term l
  37   and hr = head_of_term r in
  38   let remove_index x pos =
  39     let x_entry = try Hashtbl.find table x with Not_found -> [] in
  40     let newentry = List.filter (fun e -> e <> (pos, sign, eq)) x_entry in
  41     Hashtbl.replace table x newentry
  42   in
  43   remove_index hl Left;
  44   remove_index hr Right;
  45   table
  46 ;;
  47
  48
  49 let rec find_matches metasenv context ugraph lift_amount term =
  50   let module C = Cic in
  51   let module U = Utils in
  52   let module S = CicSubstitution in
  53   let module M = CicMetaSubst in
  54   let module HL = HelmLibraryObjects in
  55   let cmp = !Utils.compare_terms in
  56   function
  57     | [] -> None
  58     | (_, U.Negative, _)::tl ->
  59         find_matches metasenv context ugraph lift_amount term tl
  60     | (pos, U.Positive, (_, (_, _, _, o), _, _))::tl
  61         when (pos = Left && o = U.Lt) || (pos = Right && o = U.Gt) ->
  62         find_matches metasenv context ugraph lift_amount term tl
  63     | (pos, U.Positive, (proof, (ty, left, right, o), metas, args))::tl ->
  64         let do_match c other eq_URI =
  65           let subst', metasenv', ugraph' =
  66             Inference.matching (metasenv @ metas) context term
  67               (S.lift lift_amount c) ugraph
  68           in
  69           Some (C.Rel (1 + lift_amount), subst', metasenv', ugraph',
  70                 (proof, ty, c, other, eq_URI))
  71         in
  72         let c, other, eq_URI =
  73           if pos = Left then left, right, HL.Logic.eq_ind_URI
  74           else right, left, HL.Logic.eq_ind_r_URI
  75         in
  76         if o <> U.Incomparable then
  77           try do_match c other eq_URI
  78           with e -> find_matches metasenv context ugraph lift_amount term tl
  79         else
  80           let res = try do_match c other eq_URI with e -> None in
  81           match res with
  82           | Some (_, s, _, _, _) ->
  83               if cmp (M.apply_subst s left) (M.apply_subst s right) =
  84                 (if pos = Left then U.Gt else U.Lt) then
  85                   res
  86               else
  87                 find_matches metasenv context ugraph lift_amount term tl
  88           | None ->
  89               find_matches metasenv context ugraph lift_amount term tl
  90 ;;
  91
  92
  93 let rec demodulate_term metasenv context ugraph table lift_amount term =
  94   let module C = Cic in
  95   let module S = CicSubstitution in
  96   let module M = CicMetaSubst in
  97   let module HL = HelmLibraryObjects in
  98   let hd_term = head_of_term term in
  99   let candidates = try Hashtbl.find table hd_term with Not_found -> [] in
 100   match term with
 101   | C.Meta _ -> None
 102   | term ->
 103       let res =
 104         find_matches metasenv context ugraph lift_amount term candidates
 105       in
 106       if res <> None then
 107         res
 108       else
 109         match term with
 110         | C.Appl l ->
 111             let res, ll =
 112               List.fold_left
 113                 (fun (res, tl) t ->
 114                    if res <> None then
 115                      (res, tl @ [S.lift 1 t])
 116                    else
 117                      let r =
 118                        demodulate_term metasenv context ugraph table
 119                          lift_amount t
 120                      in
 121                      match r with
 122                      | None -> (None, tl @ [S.lift 1 t])
 123                      | Some (rel, _, _, _, _) -> (r, tl @ [rel]))
 124                 (None, []) l
 125             in (
 126               match res with
 127               | None -> None
 128               | Some (_, subst, menv, ug, info) ->
 129                   Some (C.Appl ll, subst, menv, ug, info)
 130             )
 131         | C.Prod (nn, s, t) ->
 132             let r1 =
 133               demodulate_term metasenv context ugraph table lift_amount s in (
 134               match r1 with
 135               | None ->
 136                   let r2 =
 137                     demodulate_term metasenv
 138                       ((Some (nn, C.Decl s))::context) ugraph
 139                       table (lift_amount+1) t
 140                   in (
 141                     match r2 with
 142                     | None -> None
 143                     | Some (t', subst, menv, ug, info) ->
 144                         Some (C.Prod (nn, (S.lift 1 s), t'),
 145                               subst, menv, ug, info)
 146                   )
 147               | Some (s', subst, menv, ug, info) ->
 148                   Some (C.Prod (nn, s', (S.lift 1 t)), subst, menv, ug, info)
 149             )
 150         | t ->
 151             Printf.printf "Ne` Appl ne` Prod: %s\n"
 152               (CicPp.pp t (Utils.names_of_context context));
 153             None
 154 ;;
 155
 156
 157 let rec demodulate newmeta env table target =
 158   let module C = Cic in
 159   let module S = CicSubstitution in
 160   let module M = CicMetaSubst in
 161   let module HL = HelmLibraryObjects in
 162   let metasenv, context, ugraph = env in
 163   let proof, (eq_ty, left, right, order), metas, args = target in
 164   let metasenv = metasenv @ metas in
 165   let build_newtarget is_left
 166       (t, subst, menv, ug, (proof', ty, what, other, eq_URI)) =
 167     let newterm, newproof =
 168       let bo = S.subst (M.apply_subst subst other) t in
 169       let bo'' =
 170         C.Appl ([C.MutInd (HL.Logic.eq_URI, 0, []);
 171                  S.lift 1 eq_ty] @
 172                   if is_left then [bo; S.lift 1 right] else [S.lift 1 left; bo])
 173       in
 174       let t' = C.Lambda (C.Anonymous, ty, bo'') in
 175       bo,
 176       M.apply_subst subst (C.Appl [C.Const (eq_URI, []); ty; what; t';
 177                                    proof; other; proof'])
 178     in
 179     let newmeta, newtarget =
 180       let left, right = if is_left then newterm, right else left, newterm in
 181       let m =
 182         (Inference.metas_of_term left) @ (Inference.metas_of_term right)
 183       in
 184       let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) metas
 185       and newargs =
 186         List.filter
 187           (function C.Meta (i, _) -> List.mem i m | _ -> assert false)
 188           args
 189       in
 190       let ordering = !Utils.compare_terms left right in
 191       newmeta, (newproof, (eq_ty, left, right, ordering), newmetasenv, newargs)
 192     in
 193     newmeta, newtarget
 194   in
 195   let res = demodulate_term metasenv context ugraph table 0 left in
 196   match res with
 197   | Some t ->
 198       let newmeta, newtarget = build_newtarget true t in
 199       if Inference.is_identity (metasenv, context, ugraph) newtarget then
 200         newmeta, newtarget
 201       else
 202         demodulate newmeta env table newtarget
 203   | None ->
 204       let res = demodulate_term metasenv context ugraph table 0 right in
 205       match res with
 206       | Some t ->
 207           let newmeta, newtarget = build_newtarget false t in
 208           if Inference.is_identity (metasenv, context, ugraph) newtarget then
 209             newmeta, newtarget
 210           else
 211             demodulate newmeta env table newtarget
 212       | None ->
 213           newmeta, target
 214 ;;
 215
 216
 217 let rec betaexpand_term metasenv context ugraph table lift_amount term =
 218   let module C = Cic in
 219   let module S = CicSubstitution in
 220   let module M = CicMetaSubst in
 221   let module HL = HelmLibraryObjects in
 222   let hd_term = head_of_term term in
 223   let candidates = try Hashtbl.find table hd_term with Not_found -> [] in
 224   let res, lifted_term =
 225     match term with
 226     | C.Meta (i, l) ->
 227         let l =
 228           List.map (function
 229                       | Some t -> Some (S.lift lift_amount t)
 230                       | None -> None) l
 231         in
 232         [], C.Meta (i, l)
 233
 234     | C.Rel m ->
 235         [], if m <= lift_amount then C.Rel m else C.Rel (m+1)
 236
 237     | C.Prod (nn, s, t) ->
 238         let l1, lifted_s =
 239           betaexpand_term metasenv context ugraph table lift_amount s in
 240         let l2, lifted_t =
 241           betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
 242             table (lift_amount+1) t in
 243         let l1' =
 244           List.map
 245             (fun (t, s, m, ug, info) ->
 246                C.Prod (nn, t, lifted_t), s, m, ug, info) l1
 247         and l2' =
 248           List.map
 249             (fun (t, s, m, ug, info) ->
 250                C.Prod (nn, lifted_s, t), s, m, ug, info) l2 in
 251         l1' @ l2', C.Prod (nn, lifted_s, lifted_t)
 252
 253     | C.Appl l ->
 254         let l', lifted_l =
 255           List.fold_right
 256             (fun arg (res, lifted_tl) ->
 257                let arg_res, lifted_arg =
 258                  betaexpand_term metasenv context ugraph table lift_amount arg
 259                in
 260                let l1 =
 261                  List.map
 262                    (fun (a, s, m, ug, info) -> a::lifted_tl, s, m, ug, info)
 263                    arg_res
 264                in
 265                (l1 @
 266                   (List.map
 267                      (fun (r, s, m, ug, info) -> lifted_arg::r, s, m, ug, info)
 268                      res),
 269                 lifted_arg::lifted_tl)
 270             ) l ([], [])
 271         in
 272         (List.map (fun (l, s, m, ug, info) -> (C.Appl l, s, m, ug, info)) l',
 273          C.Appl lifted_l)
 274
 275     | t -> [], (S.lift lift_amount t)
 276   in
 277   match term with
 278   | C.Meta _ -> res, lifted_term
 279   | _ ->
 280       match
 281         find_matches metasenv context ugraph lift_amount term candidates
 282       with
 283       | None -> res, lifted_term
 284       | Some r -> r::res, lifted_term
 285 ;;
 286
 287
 288 let superposition_left (metasenv, context, ugraph) table target =
 289   let module C = Cic in
 290   let module S = CicSubstitution in
 291   let module M = CicMetaSubst in
 292   let module HL = HelmLibraryObjects in
 293   let module CR = CicReduction in
 294   let module U = Utils in
 295   let proof, (eq_ty, left, right, ordering), _, _ = target in
 296   let expansions, _ =
 297     let term = if ordering = U.Gt then left else right in
 298     betaexpand_term metasenv context ugraph table 0 term
 299   in
 300   let build_new (bo, s, m, ug, (proof', ty, what, other, eq_URI)) =
 301     let newgoal, newproof =
 302       let bo' = S.subst (M.apply_subst s other) bo in
 303       let bo'' =
 304         C.Appl (
 305           [C.MutInd (HL.Logic.eq_URI, 0, []);
 306            S.lift 1 eq_ty] @
 307             if ordering = U.Gt then [bo'; S.lift 1 right]
 308             else [S.lift 1 left; bo'])
 309       in
 310       let t' = C.Lambda (C.Anonymous, ty, bo'') in
 311       S.subst (M.apply_subst s other) bo,
 312       M.apply_subst s
 313         (C.Appl [C.Const (eq_URI, []); ty; what; t';
 314                  proof; other; proof'])
 315     in
 316     let left, right, newordering =
 317       if ordering = U.Gt then
 318         newgoal, right, !Utils.compare_terms newgoal right
 319       else
 320         left, newgoal, !Utils.compare_terms left newgoal
 321     in
 322     (newproof, (eq_ty, left, right, ordering), [], [])
 323   in
 324   List.map build_new expansions
 325 ;;
 326
 327
 328 let superposition_right newmeta (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   let eqproof, (eq_ty, left, right, ordering), newmetas, args = target in
 336   let maxmeta = ref newmeta in
 337   let res1, res2 =
 338     match ordering with
 339     | U.Gt -> fst (betaexpand_term metasenv context ugraph table 0 left), []
 340     | U.Lt -> [], fst (betaexpand_term metasenv context ugraph table 0 right)
 341     | _ ->
 342         let res l r =
 343           List.filter
 344             (fun (_, subst, _, _, _) ->
 345                let subst = M.apply_subst subst in
 346                let o = !Utils.compare_terms (subst l) (subst r) in
 347                o <> U.Lt && o <> U.Le)
 348             (fst (betaexpand_term metasenv context ugraph table 0 l))
 349         in
 350         (res left right), (res right left)
 351   in
 352   let build_new ordering (bo, s, m, ug, (proof', ty, what, other, eq_URI)) =
 353     let newgoal, newproof =
 354       let bo' = S.subst (M.apply_subst s other) bo in
 355       let bo'' =
 356         C.Appl (
 357           [C.MutInd (HL.Logic.eq_URI, 0, []);
 358            S.lift 1 eq_ty] @
 359             if ordering = U.Gt then [bo'; S.lift 1 right]
 360             else [S.lift 1 left; bo'])
 361       in
 362       let t' = C.Lambda (C.Anonymous, ty, bo'') in
 363       S.subst (M.apply_subst s other) bo,
 364       M.apply_subst s
 365         (C.Appl [C.Const (eq_URI, []); ty; what; t';
 366                  eqproof; other; proof'])
 367     in
 368     let newmeta, newequality =
 369       let left, right, newordering =
 370         if ordering = U.Gt then
 371           newgoal, right, !Utils.compare_terms newgoal right
 372         else
 373           left, newgoal, !Utils.compare_terms left newgoal
 374       in
 375       Inference.fix_metas !maxmeta
 376         (newproof, (eq_ty, left, right, ordering), [], [])
 377     in
 378     maxmeta := newmeta;
 379     newequality
 380   in
 381   let new1 = List.map (build_new U.Gt) res1
 382   and new2 = List.map (build_new U.Lt) res2 in
 383   let ok = function
 384     | _, (_, left, right, _), _, _ ->
 385         not (fst (CR.are_convertible context left right ugraph))
 386   in
 387   (!maxmeta,
 388    (List.filter ok (new1 @ new2)))
 389 ;;