diff -r 890fafbcf8b0 -r b803f9870e97 src/HOL/Tools/function_package/sum_tools.ML --- a/src/HOL/Tools/function_package/sum_tools.ML Tue Nov 07 21:30:03 2006 +0100 +++ b/src/HOL/Tools/function_package/sum_tools.ML Tue Nov 07 22:06:32 2006 +0100 @@ -46,30 +46,30 @@ | Branch of (typ * (typ * sum_tree) * (typ * sum_tree)) type sum_path = bool list (* true: left, false: right *) - + fun sum_type_of (Leaf T) = T | sum_type_of (Branch (ST,(LT,_),(RT,_))) = ST - - + + fun mk_tree Ts = let - fun mk_tree' 1 [T] = (T, Leaf T, [[]]) - | mk_tree' n Ts = - let - val n2 = n div 2 - val (lTs, rTs) = chop n2 Ts - val (TL, ltree, lpaths) = mk_tree' n2 lTs - val (TR, rtree, rpaths) = mk_tree' (n - n2) rTs - val T = mk_sumT TL TR - val pths = map (cons true) lpaths @ map (cons false) rpaths - in - (T, Branch (T, (TL, ltree), (TR, rtree)), pths) - end + fun mk_tree' 1 [T] = (T, Leaf T, [[]]) + | mk_tree' n Ts = + let + val n2 = n div 2 + val (lTs, rTs) = chop n2 Ts + val (TL, ltree, lpaths) = mk_tree' n2 lTs + val (TR, rtree, rpaths) = mk_tree' (n - n2) rTs + val T = mk_sumT TL TR + val pths = map (cons true) lpaths @ map (cons false) rpaths + in + (T, Branch (T, (TL, ltree), (TR, rtree)), pths) + end in - mk_tree' (length Ts) Ts + mk_tree' (length Ts) Ts end - - + + fun mk_tree_distinct Ts = let fun insert_once T Ts = @@ -78,9 +78,9 @@ in if i = ~1 then (length Ts, Ts @ [T]) else (i, Ts) end - + val (idxs, dist_Ts) = fold_map insert_once Ts [] - + val (ST, tree, pths) = mk_tree dist_Ts in (ST, tree, map (nth pths) idxs) @@ -104,19 +104,19 @@ fun mk_sumcases tree T ts = let - fun mk_sumcases' (Leaf _) (t::ts) = (t,ts) - | mk_sumcases' (Branch (ST, (LT, ltr), (RT, rtr))) ts = - let - val (lcase, ts') = mk_sumcases' ltr ts - val (rcase, ts'') = mk_sumcases' rtr ts' - in - (mk_sumcase LT RT T lcase rcase, ts'') - end - | mk_sumcases' _ [] = sys_error "mk_sumcases" + fun mk_sumcases' (Leaf _) (t::ts) = (t,ts) + | mk_sumcases' (Branch (ST, (LT, ltr), (RT, rtr))) ts = + let + val (lcase, ts') = mk_sumcases' ltr ts + val (rcase, ts'') = mk_sumcases' rtr ts' + in + (mk_sumcase LT RT T lcase rcase, ts'') + end + | mk_sumcases' _ [] = sys_error "mk_sumcases" in - fst (mk_sumcases' tree ts) + fst (mk_sumcases' tree ts) end - + end