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