author | wenzelm |
Sat, 03 Nov 2018 20:09:39 +0100 | |
changeset 69227 | 71b48b749836 |
parent 54407 | e95831757903 |
permissions | -rw-r--r-- |
31775 | 1 |
(* Title: HOL/Tools/Function/pattern_split.ML |
20270
3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff
changeset
|
2 |
Author: Alexander Krauss, TU Muenchen |
3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff
changeset
|
3 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
4 |
Fairly ad-hoc pattern splitting. |
20270
3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff
changeset
|
5 |
*) |
3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff
changeset
|
6 |
|
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
33049
diff
changeset
|
7 |
signature FUNCTION_SPLIT = |
20270
3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff
changeset
|
8 |
sig |
20289 | 9 |
val split_some_equations : |
21237 | 10 |
Proof.context -> (bool * term) list -> term list list |
20270
3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff
changeset
|
11 |
|
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20344
diff
changeset
|
12 |
val split_all_equations : |
21237 | 13 |
Proof.context -> term list -> term list list |
20270
3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff
changeset
|
14 |
end |
3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff
changeset
|
15 |
|
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
33049
diff
changeset
|
16 |
structure Function_Split : FUNCTION_SPLIT = |
20270
3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff
changeset
|
17 |
struct |
3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff
changeset
|
18 |
|
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
33049
diff
changeset
|
19 |
open Function_Lib |
20270
3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff
changeset
|
20 |
|
42362
5528970ac6f7
observe firm naming convention ctxt: Proof.context;
wenzelm
parents:
42361
diff
changeset
|
21 |
fun new_var ctxt vs T = |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
22 |
let |
42362
5528970ac6f7
observe firm naming convention ctxt: Proof.context;
wenzelm
parents:
42361
diff
changeset
|
23 |
val [v] = Variable.variant_frees ctxt vs [("v", T)] |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
24 |
in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
25 |
(Free v :: vs, Free v) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
26 |
end |
20270
3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff
changeset
|
27 |
|
42362
5528970ac6f7
observe firm naming convention ctxt: Proof.context;
wenzelm
parents:
42361
diff
changeset
|
28 |
fun saturate ctxt vs t = |
5528970ac6f7
observe firm naming convention ctxt: Proof.context;
wenzelm
parents:
42361
diff
changeset
|
29 |
fold (fn T => fn (vs, t) => new_var ctxt vs T |> apsnd (curry op $ t)) |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
30 |
(binder_types (fastype_of t)) (vs, t) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
31 |
|
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
32 |
|
20636 | 33 |
fun join ((vs1,sub1), (vs2,sub2)) = (merge (op aconv) (vs1,vs2), sub1 @ sub2) |
25538 | 34 |
fun join_product (xs, ys) = map_product (curry join) xs ys |
20636 | 35 |
|
36 |
exception DISJ |
|
37 |
||
42362
5528970ac6f7
observe firm naming convention ctxt: Proof.context;
wenzelm
parents:
42361
diff
changeset
|
38 |
fun pattern_subtract_subst ctxt vs t t' = |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
39 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
40 |
exception DISJ |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
41 |
fun pattern_subtract_subst_aux vs _ (Free v2) = [] |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
42 |
| pattern_subtract_subst_aux vs (v as (Free (_, T))) t' = |
20344 | 43 |
let |
54406 | 44 |
fun aux constr = |
42362
5528970ac6f7
observe firm naming convention ctxt: Proof.context;
wenzelm
parents:
42361
diff
changeset
|
45 |
let |
5528970ac6f7
observe firm naming convention ctxt: Proof.context;
wenzelm
parents:
42361
diff
changeset
|
46 |
val (vs', t) = saturate ctxt vs constr |
5528970ac6f7
observe firm naming convention ctxt: Proof.context;
wenzelm
parents:
42361
diff
changeset
|
47 |
val substs = pattern_subtract_subst ctxt vs' t t' |
5528970ac6f7
observe firm naming convention ctxt: Proof.context;
wenzelm
parents:
42361
diff
changeset
|
48 |
in |
5528970ac6f7
observe firm naming convention ctxt: Proof.context;
wenzelm
parents:
42361
diff
changeset
|
49 |
map (fn (vs, subst) => (vs, (v,t)::subst)) substs |
5528970ac6f7
observe firm naming convention ctxt: Proof.context;
wenzelm
parents:
42361
diff
changeset
|
50 |
end |
20270
3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff
changeset
|
51 |
in |
54407
e95831757903
ported part of function package to new 'Ctr_Sugar' abstraction
blanchet
parents:
54406
diff
changeset
|
52 |
maps aux (inst_constrs_of ctxt T) |
20636 | 53 |
end |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
54 |
| pattern_subtract_subst_aux vs t t' = |
42362
5528970ac6f7
observe firm naming convention ctxt: Proof.context;
wenzelm
parents:
42361
diff
changeset
|
55 |
let |
5528970ac6f7
observe firm naming convention ctxt: Proof.context;
wenzelm
parents:
42361
diff
changeset
|
56 |
val (C, ps) = strip_comb t |
5528970ac6f7
observe firm naming convention ctxt: Proof.context;
wenzelm
parents:
42361
diff
changeset
|
57 |
val (C', qs) = strip_comb t' |
5528970ac6f7
observe firm naming convention ctxt: Proof.context;
wenzelm
parents:
42361
diff
changeset
|
58 |
in |
5528970ac6f7
observe firm naming convention ctxt: Proof.context;
wenzelm
parents:
42361
diff
changeset
|
59 |
if C = C' |
5528970ac6f7
observe firm naming convention ctxt: Proof.context;
wenzelm
parents:
42361
diff
changeset
|
60 |
then flat (map2 (pattern_subtract_subst_aux vs) ps qs) |
5528970ac6f7
observe firm naming convention ctxt: Proof.context;
wenzelm
parents:
42361
diff
changeset
|
61 |
else raise DISJ |
5528970ac6f7
observe firm naming convention ctxt: Proof.context;
wenzelm
parents:
42361
diff
changeset
|
62 |
end |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
63 |
in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
64 |
pattern_subtract_subst_aux vs t t' |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
65 |
handle DISJ => [(vs, [])] |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
66 |
end |
20270
3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff
changeset
|
67 |
|
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20344
diff
changeset
|
68 |
(* p - q *) |
42362
5528970ac6f7
observe firm naming convention ctxt: Proof.context;
wenzelm
parents:
42361
diff
changeset
|
69 |
fun pattern_subtract ctxt eq2 eq1 = |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
70 |
let |
42362
5528970ac6f7
observe firm naming convention ctxt: Proof.context;
wenzelm
parents:
42361
diff
changeset
|
71 |
val thy = Proof_Context.theory_of ctxt |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
72 |
|
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
73 |
val (vs, feq1 as (_ $ (_ $ lhs1 $ _))) = dest_all_all eq1 |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
74 |
val (_, _ $ (_ $ lhs2 $ _)) = dest_all_all eq2 |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
75 |
|
42362
5528970ac6f7
observe firm naming convention ctxt: Proof.context;
wenzelm
parents:
42361
diff
changeset
|
76 |
val substs = pattern_subtract_subst ctxt vs lhs1 lhs2 |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
77 |
|
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
78 |
fun instantiate (vs', sigma) = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
79 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
80 |
val t = Pattern.rewrite_term thy sigma [] feq1 |
42483 | 81 |
val xs = fold_aterms |
82 |
(fn x as Free (a, _) => |
|
83 |
if not (Variable.is_fixed ctxt a) andalso member (op =) vs' x |
|
84 |
then insert (op =) x else I |
|
85 |
| _ => I) t []; |
|
86 |
in fold Logic.all xs t end |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
87 |
in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
88 |
map instantiate substs |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
89 |
end |
20270
3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff
changeset
|
90 |
|
3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff
changeset
|
91 |
(* ps - p' *) |
42362
5528970ac6f7
observe firm naming convention ctxt: Proof.context;
wenzelm
parents:
42361
diff
changeset
|
92 |
fun pattern_subtract_from_many ctxt p'= |
5528970ac6f7
observe firm naming convention ctxt: Proof.context;
wenzelm
parents:
42361
diff
changeset
|
93 |
maps (pattern_subtract ctxt p') |
20270
3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff
changeset
|
94 |
|
3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff
changeset
|
95 |
(* in reverse order *) |
42362
5528970ac6f7
observe firm naming convention ctxt: Proof.context;
wenzelm
parents:
42361
diff
changeset
|
96 |
fun pattern_subtract_many ctxt ps' = |
5528970ac6f7
observe firm naming convention ctxt: Proof.context;
wenzelm
parents:
42361
diff
changeset
|
97 |
fold_rev (pattern_subtract_from_many ctxt) ps' |
20270
3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff
changeset
|
98 |
|
42362
5528970ac6f7
observe firm naming convention ctxt: Proof.context;
wenzelm
parents:
42361
diff
changeset
|
99 |
fun split_some_equations ctxt eqns = |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
100 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
101 |
fun split_aux prev [] = [] |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
102 |
| split_aux prev ((true, eq) :: es) = |
42362
5528970ac6f7
observe firm naming convention ctxt: Proof.context;
wenzelm
parents:
42361
diff
changeset
|
103 |
pattern_subtract_many ctxt prev [eq] :: split_aux (eq :: prev) es |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
104 |
| split_aux prev ((false, eq) :: es) = |
42362
5528970ac6f7
observe firm naming convention ctxt: Proof.context;
wenzelm
parents:
42361
diff
changeset
|
105 |
[eq] :: split_aux (eq :: prev) es |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
106 |
in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
107 |
split_aux [] eqns |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
108 |
end |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
109 |
|
42362
5528970ac6f7
observe firm naming convention ctxt: Proof.context;
wenzelm
parents:
42361
diff
changeset
|
110 |
fun split_all_equations ctxt = |
5528970ac6f7
observe firm naming convention ctxt: Proof.context;
wenzelm
parents:
42361
diff
changeset
|
111 |
split_some_equations ctxt o map (pair true) |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20344
diff
changeset
|
112 |
|
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20344
diff
changeset
|
113 |
|
20270
3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff
changeset
|
114 |
end |