author | haftmann |
Thu, 01 Jul 2010 16:54:44 +0200 | |
changeset 37678 | 0040bafffdef |
parent 37387 | 3581483cca6c |
child 49965 | ee25a04fa06a |
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 *) |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33961
diff
changeset
|
11 |
val sumcase_split_ss = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33961
diff
changeset
|
12 |
HOL_basic_ss addsimps (@{thm Product_Type.split} :: @{thms sum.cases}) |
25555 | 13 |
|
14 |
(* top-down access in balanced tree *) |
|
15 |
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
|
16 |
Balanced_Tree.access |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33961
diff
changeset
|
17 |
{left = (fn f => f o left), right = (fn f => f o right), init = I} len i init |
25555 | 18 |
|
19 |
(* Sum types *) |
|
37678
0040bafffdef
"prod" and "sum" replace "*" and "+" respectively
haftmann
parents:
37387
diff
changeset
|
20 |
fun mk_sumT LT RT = Type (@{type_name Sum_Type.sum}, [LT, RT]) |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33961
diff
changeset
|
21 |
fun mk_sumcase TL TR T l r = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33961
diff
changeset
|
22 |
Const (@{const_name sum.sum_case}, |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33961
diff
changeset
|
23 |
(TL --> T) --> (TR --> T) --> mk_sumT TL TR --> T) $ l $ r |
25555 | 24 |
|
25 |
val App = curry op $ |
|
26 |
||
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33961
diff
changeset
|
27 |
fun mk_inj ST n i = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33961
diff
changeset
|
28 |
access_top_down |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33961
diff
changeset
|
29 |
{ init = (ST, I : term -> term), |
37678
0040bafffdef
"prod" and "sum" replace "*" and "+" respectively
haftmann
parents:
37387
diff
changeset
|
30 |
left = (fn (T as Type (@{type_name Sum_Type.sum}, [LT, RT]), inj) => |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33961
diff
changeset
|
31 |
(LT, inj o App (Const (@{const_name Inl}, LT --> T)))), |
37678
0040bafffdef
"prod" and "sum" replace "*" and "+" respectively
haftmann
parents:
37387
diff
changeset
|
32 |
right =(fn (T as Type (@{type_name Sum_Type.sum}, [LT, RT]), inj) => |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33961
diff
changeset
|
33 |
(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
|
34 |
|> snd |
25555 | 35 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33961
diff
changeset
|
36 |
fun mk_proj ST n i = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33961
diff
changeset
|
37 |
access_top_down |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33961
diff
changeset
|
38 |
{ init = (ST, I : term -> term), |
37678
0040bafffdef
"prod" and "sum" replace "*" and "+" respectively
haftmann
parents:
37387
diff
changeset
|
39 |
left = (fn (T as Type (@{type_name Sum_Type.sum}, [LT, RT]), proj) => |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33961
diff
changeset
|
40 |
(LT, App (Const (@{const_name Sum_Type.Projl}, T --> LT)) o proj)), |
37678
0040bafffdef
"prod" and "sum" replace "*" and "+" respectively
haftmann
parents:
37387
diff
changeset
|
41 |
right =(fn (T as Type (@{type_name Sum_Type.sum}, [LT, RT]), proj) => |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33961
diff
changeset
|
42 |
(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
|
43 |
|> snd |
25555 | 44 |
|
45 |
fun mk_sumcases T fs = |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
33961
diff
changeset
|
46 |
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
|
47 |
(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
|
48 |
|> fst |
25555 | 49 |
|
50 |
end |