author | krauss |
Sat, 02 Jan 2010 23:18:58 +0100 | |
changeset 34232 | 36a2a3029fd3 |
parent 33961 | 03f2ab6a4ea6 |
child 36773 | acb789f3936b |
permissions | -rw-r--r-- |
31775 | 1 |
(* Title: HOL/Tools/Function/sum_tree.ML |
25555 | 2 |
Author: Alexander Krauss, TU Muenchen |
3 |
||
4 |
Some common tools for working with sum types in balanced tree form. |
|
5 |
*) |
|
6 |
||
7 |
structure SumTree = |
|
8 |
struct |
|
9 |
||
10 |
(* Theory dependencies *) |
|
33961 | 11 |
val proj_in_rules = [@{thm Projl_Inl}, @{thm Projr_Inr}] |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33961
diff
changeset
|
12 |
val sumcase_split_ss = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33961
diff
changeset
|
13 |
HOL_basic_ss addsimps (@{thm Product_Type.split} :: @{thms sum.cases}) |
25555 | 14 |
|
15 |
(* top-down access in balanced tree *) |
|
16 |
fun access_top_down {left, right, init} len i = |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33961
diff
changeset
|
17 |
Balanced_Tree.access |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33961
diff
changeset
|
18 |
{left = (fn f => f o left), right = (fn f => f o right), init = I} len i init |
25555 | 19 |
|
20 |
(* Sum types *) |
|
21 |
fun mk_sumT LT RT = Type ("+", [LT, RT]) |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33961
diff
changeset
|
22 |
fun mk_sumcase TL TR T l r = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33961
diff
changeset
|
23 |
Const (@{const_name sum.sum_case}, |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33961
diff
changeset
|
24 |
(TL --> T) --> (TR --> T) --> mk_sumT TL TR --> T) $ l $ r |
25555 | 25 |
|
26 |
val App = curry op $ |
|
27 |
||
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33961
diff
changeset
|
28 |
fun mk_inj ST n i = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33961
diff
changeset
|
29 |
access_top_down |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33961
diff
changeset
|
30 |
{ init = (ST, I : term -> term), |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33961
diff
changeset
|
31 |
left = (fn (T as Type ("+", [LT, RT]), inj) => |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33961
diff
changeset
|
32 |
(LT, inj o App (Const (@{const_name Inl}, LT --> T)))), |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33961
diff
changeset
|
33 |
right =(fn (T as Type ("+", [LT, RT]), inj) => |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33961
diff
changeset
|
34 |
(RT, inj o App (Const (@{const_name Inr}, RT --> T))))} n i |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33961
diff
changeset
|
35 |
|> snd |
25555 | 36 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33961
diff
changeset
|
37 |
fun mk_proj ST n i = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33961
diff
changeset
|
38 |
access_top_down |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33961
diff
changeset
|
39 |
{ init = (ST, I : term -> term), |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33961
diff
changeset
|
40 |
left = (fn (T as Type ("+", [LT, RT]), proj) => |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33961
diff
changeset
|
41 |
(LT, App (Const (@{const_name Sum_Type.Projl}, T --> LT)) o proj)), |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33961
diff
changeset
|
42 |
right =(fn (T as Type ("+", [LT, RT]), proj) => |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33961
diff
changeset
|
43 |
(RT, App (Const (@{const_name Sum_Type.Projr}, T --> RT)) o proj))} n i |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33961
diff
changeset
|
44 |
|> snd |
25555 | 45 |
|
46 |
fun mk_sumcases T fs = |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33961
diff
changeset
|
47 |
Balanced_Tree.make (fn ((f, fT), (g, gT)) => (mk_sumcase fT gT T f g, mk_sumT fT gT)) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33961
diff
changeset
|
48 |
(map (fn f => (f, domain_type (fastype_of f))) fs) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33961
diff
changeset
|
49 |
|> fst |
25555 | 50 |
|
51 |
end |