1(*  Title:      HOL/Tools/Function/sum_tree.ML
2    Author:     Alexander Krauss, TU Muenchen
3
4Some common tools for working with sum types in balanced tree form.
5*)
6
7signature SUM_TREE =
8sig
9  val sumcase_split_ss: simpset
10  val access_top_down: {init: 'a, left: 'a -> 'a, right: 'a -> 'a} -> int -> int -> 'a
11  val mk_sumT: typ -> typ -> typ
12  val mk_sumcase: typ -> typ -> typ -> term -> term -> term
13  val App: term -> term -> term
14  val mk_inj: typ -> int -> int -> term -> term
15  val mk_proj: typ -> int -> int -> term -> term
16  val mk_sumcases: typ -> term list -> term
17end
18
19structure Sum_Tree: SUM_TREE =
20struct
21
22(* Theory dependencies *)
23val sumcase_split_ss =
24  simpset_of (put_simpset HOL_basic_ss @{context}
25    addsimps (@{thm Product_Type.split} :: @{thms sum.case}))
26
27(* top-down access in balanced tree *)
28fun access_top_down {left, right, init} len i =
29  Balanced_Tree.access
30    {left = (fn f => f o left), right = (fn f => f o right), init = I} len i init
31
32(* Sum types *)
33fun mk_sumT LT RT = Type (\<^type_name>\<open>Sum_Type.sum\<close>, [LT, RT])
34fun mk_sumcase TL TR T l r =
35  Const (\<^const_name>\<open>sum.case_sum\<close>, (TL --> T) --> (TR --> T) --> mk_sumT TL TR --> T) $ l $ r
36
37val App = curry op $
38
39fun mk_inj ST n i =
40  access_top_down
41  { init = (ST, I : term -> term),
42    left = (fn (T as Type (\<^type_name>\<open>Sum_Type.sum\<close>, [LT, RT]), inj) =>
43      (LT, inj o App (Const (\<^const_name>\<open>Inl\<close>, LT --> T)))),
44    right =(fn (T as Type (\<^type_name>\<open>Sum_Type.sum\<close>, [LT, RT]), inj) =>
45      (RT, inj o App (Const (\<^const_name>\<open>Inr\<close>, RT --> T))))} n i
46  |> snd
47
48fun mk_proj ST n i =
49  access_top_down
50  { init = (ST, I : term -> term),
51    left = (fn (T as Type (\<^type_name>\<open>Sum_Type.sum\<close>, [LT, RT]), proj) =>
52      (LT, App (Const (\<^const_name>\<open>Sum_Type.projl\<close>, T --> LT)) o proj)),
53    right =(fn (T as Type (\<^type_name>\<open>Sum_Type.sum\<close>, [LT, RT]), proj) =>
54      (RT, App (Const (\<^const_name>\<open>Sum_Type.projr\<close>, T --> RT)) o proj))} n i
55  |> snd
56
57fun mk_sumcases T fs =
58  Balanced_Tree.make (fn ((f, fT), (g, gT)) => (mk_sumcase fT gT T f g, mk_sumT fT gT))
59    (map (fn f => (f, domain_type (fastype_of f))) fs)
60  |> fst
61
62end
63