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