src/Pure/more_pattern.ML
author wenzelm
Sat Nov 04 15:24:40 2017 +0100 (19 months ago)
changeset 67003 49850a679c2c
parent 59095 3100a7b1c092
child 67010 cf56dd6f3ad1
permissions -rw-r--r--
more robust sorted_entries;
wenzelm@59026
     1
(*  Title:      Pure/more_pattern.ML
wenzelm@59026
     2
    Author:     Tobias Nipkow, TU Muenchen
wenzelm@59026
     3
    Author:     Stefan Berghofer, TU Muenchen
wenzelm@59026
     4
wenzelm@59026
     5
Add-ons to Higher-Order Patterns, outside the inference kernel.
wenzelm@59026
     6
*)
wenzelm@59026
     7
wenzelm@59026
     8
signature PATTERN =
wenzelm@59026
     9
sig
wenzelm@59026
    10
  include PATTERN
wenzelm@59026
    11
  val matches: theory -> term * term -> bool
wenzelm@59026
    12
  val matchess: theory -> term list * term list -> bool
wenzelm@59026
    13
  val equiv: theory -> term * term -> bool
wenzelm@59026
    14
  val first_order: term -> bool
wenzelm@59026
    15
  val pattern: term -> bool
wenzelm@59026
    16
  val match_rew: theory -> term -> term * term -> (term * term) option
wenzelm@59026
    17
  val rewrite_term: theory -> (term * term) list -> (term -> term option) list -> term -> term
wenzelm@59026
    18
  val rewrite_term_top: theory -> (term * term) list -> (term -> term option) list -> term -> term
wenzelm@59026
    19
end;
wenzelm@59026
    20
wenzelm@59026
    21
structure Pattern: PATTERN =
wenzelm@59026
    22
struct
wenzelm@59026
    23
wenzelm@59026
    24
fun matches thy po =
wenzelm@59026
    25
  (Pattern.match thy po (Vartab.empty, Vartab.empty); true) handle Pattern.MATCH => false;
wenzelm@59026
    26
wenzelm@59026
    27
fun matchess thy (ps, os) =
wenzelm@59026
    28
  length ps = length os andalso
wenzelm@59026
    29
    ((fold (Pattern.match thy) (ps ~~ os) (Vartab.empty, Vartab.empty); true)
wenzelm@59026
    30
      handle Pattern.MATCH => false);
wenzelm@59026
    31
wenzelm@59026
    32
fun equiv thy (t, u) = matches thy (t, u) andalso matches thy (u, t);
wenzelm@59026
    33
wenzelm@59026
    34
fun first_order (Abs (_, _, t)) = first_order t
wenzelm@59027
    35
  | first_order (Var _ $ _) = false
wenzelm@59027
    36
  | first_order (t $ u) = first_order t andalso first_order u
wenzelm@59026
    37
  | first_order _ = true;
wenzelm@59026
    38
wenzelm@59026
    39
fun pattern (Abs (_, _, t)) = pattern t
wenzelm@59026
    40
  | pattern t =
wenzelm@59026
    41
      let val (head, args) = strip_comb t in
wenzelm@59026
    42
        if is_Var head then
wenzelm@59026
    43
          forall is_Bound args andalso not (has_duplicates (op aconv) args)
wenzelm@59026
    44
        else forall pattern args
wenzelm@59026
    45
      end;
wenzelm@59026
    46
wenzelm@59026
    47
wenzelm@59026
    48
(* rewriting -- simple but fast *)
wenzelm@59026
    49
wenzelm@59026
    50
fun match_rew thy tm (tm1, tm2) =
wenzelm@59026
    51
  let val rtm = the_default tm2 (Term.rename_abs tm1 tm tm2) in
wenzelm@59026
    52
    SOME (Envir.subst_term (Pattern.match thy (tm1, tm) (Vartab.empty, Vartab.empty)) rtm, rtm)
wenzelm@59026
    53
      handle Pattern.MATCH => NONE
wenzelm@59026
    54
  end;
wenzelm@59026
    55
wenzelm@59026
    56
fun gen_rewrite_term bot thy rules procs tm =
wenzelm@59026
    57
  let
wenzelm@59026
    58
    val skel0 = Bound 0;
wenzelm@59026
    59
wenzelm@59026
    60
    fun variant_absfree bounds (x, T, t) =
wenzelm@59026
    61
      let
wenzelm@59026
    62
        val (x', t') = Term.dest_abs (Name.bound bounds, T, t);
wenzelm@59026
    63
        fun abs u = Abs (x, T, abstract_over (Free (x', T), u));
wenzelm@59026
    64
      in (abs, t') end;
wenzelm@59026
    65
wenzelm@59026
    66
    fun rew (Abs (_, _, body) $ t) = SOME (subst_bound (t, body), skel0)
wenzelm@59026
    67
      | rew tm =
wenzelm@59026
    68
          (case get_first (match_rew thy tm) rules of
wenzelm@59026
    69
            NONE => Option.map (rpair skel0) (get_first (fn p => p tm) procs)
wenzelm@59026
    70
          | x => x);
wenzelm@59026
    71
wenzelm@59026
    72
    fun rew_sub r bounds skel (tm1 $ tm2) = (case tm1 of
wenzelm@59026
    73
            Abs (_, _, body) =>
wenzelm@59026
    74
              let val tm' = subst_bound (tm2, body)
wenzelm@59026
    75
              in SOME (the_default tm' (rew_sub r bounds skel0 tm')) end
wenzelm@59026
    76
          | _ =>
wenzelm@59026
    77
            let val (skel1, skel2) = (case skel of
wenzelm@59026
    78
                skel1 $ skel2 => (skel1, skel2)
wenzelm@59026
    79
              | _ => (skel0, skel0))
wenzelm@59026
    80
            in case r bounds skel1 tm1 of
wenzelm@59026
    81
                SOME tm1' => (case r bounds skel2 tm2 of
wenzelm@59026
    82
                    SOME tm2' => SOME (tm1' $ tm2')
wenzelm@59026
    83
                  | NONE => SOME (tm1' $ tm2))
wenzelm@59026
    84
              | NONE => (case r bounds skel2 tm2 of
wenzelm@59026
    85
                    SOME tm2' => SOME (tm1 $ tm2')
wenzelm@59026
    86
                  | NONE => NONE)
wenzelm@59026
    87
            end)
wenzelm@59026
    88
      | rew_sub r bounds skel (Abs body) =
wenzelm@59026
    89
          let
wenzelm@59026
    90
            val (abs, tm') = variant_absfree bounds body;
wenzelm@59026
    91
            val skel' = (case skel of Abs (_, _, skel') => skel' | _ => skel0)
wenzelm@59026
    92
          in case r (bounds + 1) skel' tm' of
wenzelm@59026
    93
              SOME tm'' => SOME (abs tm'')
wenzelm@59026
    94
            | NONE => NONE
wenzelm@59026
    95
          end
wenzelm@59026
    96
      | rew_sub _ _ _ _ = NONE;
wenzelm@59026
    97
wenzelm@59026
    98
    fun rew_bot bounds (Var _) _ = NONE
wenzelm@59026
    99
      | rew_bot bounds skel tm = (case rew_sub rew_bot bounds skel tm of
wenzelm@59026
   100
          SOME tm1 => (case rew tm1 of
wenzelm@59026
   101
              SOME (tm2, skel') => SOME (the_default tm2 (rew_bot bounds skel' tm2))
wenzelm@59026
   102
            | NONE => SOME tm1)
wenzelm@59026
   103
        | NONE => (case rew tm of
wenzelm@59026
   104
              SOME (tm1, skel') => SOME (the_default tm1 (rew_bot bounds skel' tm1))
wenzelm@59026
   105
            | NONE => NONE));
wenzelm@59026
   106
wenzelm@59026
   107
    fun rew_top bounds _ tm = (case rew tm of
wenzelm@59026
   108
          SOME (tm1, _) => (case rew_sub rew_top bounds skel0 tm1 of
wenzelm@59026
   109
              SOME tm2 => SOME (the_default tm2 (rew_top bounds skel0 tm2))
wenzelm@59026
   110
            | NONE => SOME tm1)
wenzelm@59026
   111
        | NONE => (case rew_sub rew_top bounds skel0 tm of
wenzelm@59026
   112
              SOME tm1 => SOME (the_default tm1 (rew_top bounds skel0 tm1))
wenzelm@59026
   113
            | NONE => NONE));
wenzelm@59026
   114
wenzelm@59026
   115
  in the_default tm ((if bot then rew_bot else rew_top) 0 skel0 tm) end;
wenzelm@59026
   116
wenzelm@59026
   117
val rewrite_term = gen_rewrite_term true;
wenzelm@59026
   118
val rewrite_term_top = gen_rewrite_term false;
wenzelm@59026
   119
wenzelm@59026
   120
wenzelm@59026
   121
open Pattern;
wenzelm@59026
   122
wenzelm@59026
   123
end;
wenzelm@59026
   124