author | wenzelm |
Sat, 16 Apr 2011 16:15:37 +0200 | |
changeset 42361 | 23f352990944 |
parent 41114 | f9ae7c2abf7e |
child 42362 | 5528970ac6f7 |
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 |
|
20344 | 21 |
fun new_var ctx vs T = |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
22 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
23 |
val [v] = Variable.variant_frees ctx vs [("v", T)] |
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 |
|
3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff
changeset
|
28 |
fun saturate ctx vs t = |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
29 |
fold (fn T => fn (vs, t) => new_var ctx vs T |> apsnd (curry op $ t)) |
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 |
|
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
33 |
(* This is copied from "pat_completeness.ML" *) |
20270
3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff
changeset
|
34 |
fun inst_constrs_of thy (T as Type (name, _)) = |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
35 |
map (fn (Cn,CT) => |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
36 |
Envir.subst_term_types (Sign.typ_match thy (body_type CT, T) Vartab.empty) (Const (Cn, CT))) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
37 |
(the (Datatype.get_constrs thy name)) |
25402 | 38 |
| inst_constrs_of thy T = raise TYPE ("inst_constrs_of", [T], []) |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
39 |
|
20636 | 40 |
|
41 |
fun join ((vs1,sub1), (vs2,sub2)) = (merge (op aconv) (vs1,vs2), sub1 @ sub2) |
|
25538 | 42 |
fun join_product (xs, ys) = map_product (curry join) xs ys |
20636 | 43 |
|
44 |
exception DISJ |
|
45 |
||
46 |
fun pattern_subtract_subst ctx vs t t' = |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
47 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
48 |
exception DISJ |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
49 |
fun pattern_subtract_subst_aux vs _ (Free v2) = [] |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
50 |
| pattern_subtract_subst_aux vs (v as (Free (_, T))) t' = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
51 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
52 |
fun foo constr = |
20344 | 53 |
let |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
54 |
val (vs', t) = saturate ctx vs constr |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
55 |
val substs = pattern_subtract_subst ctx vs' t t' |
20270
3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff
changeset
|
56 |
in |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
57 |
map (fn (vs, subst) => (vs, (v,t)::subst)) substs |
20636 | 58 |
end |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
59 |
in |
42361 | 60 |
maps foo (inst_constrs_of (Proof_Context.theory_of ctx) T) |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
61 |
end |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
62 |
| pattern_subtract_subst_aux vs t t' = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
63 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
64 |
val (C, ps) = strip_comb t |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
65 |
val (C', qs) = strip_comb t' |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
66 |
in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
67 |
if C = C' |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
68 |
then flat (map2 (pattern_subtract_subst_aux vs) ps qs) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
69 |
else raise DISJ |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
70 |
end |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
71 |
in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
72 |
pattern_subtract_subst_aux vs t t' |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
73 |
handle DISJ => [(vs, [])] |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
74 |
end |
20270
3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff
changeset
|
75 |
|
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20344
diff
changeset
|
76 |
(* p - q *) |
20270
3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff
changeset
|
77 |
fun pattern_subtract ctx eq2 eq1 = |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
78 |
let |
42361 | 79 |
val thy = Proof_Context.theory_of ctx |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
80 |
|
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
81 |
val (vs, feq1 as (_ $ (_ $ lhs1 $ _))) = dest_all_all eq1 |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
82 |
val (_, _ $ (_ $ lhs2 $ _)) = dest_all_all eq2 |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
83 |
|
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
84 |
val substs = pattern_subtract_subst ctx vs lhs1 lhs2 |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
85 |
|
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
86 |
fun instantiate (vs', sigma) = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
87 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
88 |
val t = Pattern.rewrite_term thy sigma [] feq1 |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
89 |
in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
90 |
fold_rev Logic.all (inter (op =) vs' (map Free (frees_in_term ctx t))) t |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
91 |
end |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
92 |
in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
93 |
map instantiate substs |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
94 |
end |
20270
3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff
changeset
|
95 |
|
3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff
changeset
|
96 |
(* ps - p' *) |
3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff
changeset
|
97 |
fun pattern_subtract_from_many ctx p'= |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
98 |
maps (pattern_subtract ctx p') |
20270
3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff
changeset
|
99 |
|
3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff
changeset
|
100 |
(* in reverse order *) |
3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff
changeset
|
101 |
fun pattern_subtract_many ctx ps' = |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
102 |
fold_rev (pattern_subtract_from_many ctx) ps' |
20270
3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff
changeset
|
103 |
|
3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff
changeset
|
104 |
fun split_some_equations ctx eqns = |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
105 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
106 |
fun split_aux prev [] = [] |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
107 |
| split_aux prev ((true, eq) :: es) = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
108 |
pattern_subtract_many ctx prev [eq] :: split_aux (eq :: prev) es |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
109 |
| split_aux prev ((false, eq) :: es) = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
110 |
[eq] :: split_aux (eq :: prev) es |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
111 |
in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
112 |
split_aux [] eqns |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
113 |
end |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
114 |
|
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20344
diff
changeset
|
115 |
fun split_all_equations ctx = |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33855
diff
changeset
|
116 |
split_some_equations ctx o map (pair true) |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20344
diff
changeset
|
117 |
|
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20344
diff
changeset
|
118 |
|
20270
3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
diff
changeset
|
119 |
end |