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