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