# HG changeset patch # User blanchet # Date 1367481930 -7200 # Node ID af63d7f52c027b194081f7599498b876a8c9374b # Parent cce8b6ba429dd3877403d5a1526d660fbfc68b98 more code rationalization diff -r cce8b6ba429d -r af63d7f52c02 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Thu May 02 09:50:58 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Thu May 02 10:05:30 2013 +0200 @@ -20,7 +20,7 @@ val fp_sugar_of: local_theory -> string -> fp_sugar option - val build_map: local_theory -> typ list -> (int -> typ * typ -> term) -> typ * typ -> term + val build_map': local_theory -> typ list -> (int -> typ * typ -> term) -> typ * typ -> term val mk_fp_iter_fun_types: term -> typ list val mk_fun_arg_typess: int -> int list -> typ -> typ list list @@ -362,37 +362,29 @@ fun defaults_of ((_, ds), _) = ds; fun ctr_mixfix_of (_, mx) = mx; -fun build_map_step lthy build_arg (Type (s, Ts), Type (_, Us)) = - let - val bnf = the (bnf_of lthy s); - val live = live_of_bnf bnf; - val mapx = mk_map live Ts Us (map_of_bnf bnf); - val TUs' = map dest_funT (fst (strip_typeN live (fastype_of mapx))); - in Term.list_comb (mapx, map build_arg TUs') end; - -fun build_map lthy Ts build_simple = - let - fun build (TU as (T, U)) = - if T = U then - id_const T - else - (case find_index (curry (op =) T) Ts of - ~1 => build_map_step lthy build TU - | kk => build_simple kk TU); - in build end; - -fun build_map' lthy build_simple = +fun build_map lthy build_simple = let fun build (TU as (T, U)) = if T = U then id_const T else (case TU of - (Type (s, _), Type (s', _)) => - if s = s' then build_map_step lthy build TU else build_simple TU + (Type (s, Ts), Type (s', Us)) => + if s = s' then + let + val bnf = the (bnf_of lthy s); + val live = live_of_bnf bnf; + val mapx = mk_map live Ts Us (map_of_bnf bnf); + val TUs' = map dest_funT (fst (strip_typeN live (fastype_of mapx))); + in Term.list_comb (mapx, map build TUs') end + else + build_simple TU | _ => build_simple TU); in build end; +fun build_map' lthy Ts build_simple = + build_map lthy (fn (T, U) => build_simple (find_index (curry (op =) T) Ts) (T, U)); + fun build_rel_step lthy build_arg (Type (s, Ts)) = let val bnf = the (bnf_of lthy s); @@ -530,7 +522,7 @@ fun unzip_iters fiters combine (x as Free (_, T)) = if exists_subtype_in fpTs T then - combine (x, build_map lthy fpTs (K o nth fiters) (T, mk_U T) $ x) + combine (x, build_map' lthy fpTs (K o nth fiters) (T, mk_U T) $ x) else ([x], []); @@ -698,7 +690,7 @@ fun intr_coiters fcoiters [] [cf] = let val T = fastype_of cf in - if exists_subtype_in Cs T then build_map lthy Cs (K o nth fcoiters) (T, mk_U T) $ cf + if exists_subtype_in Cs T then build_map' lthy Cs (K o nth fcoiters) (T, mk_U T) $ cf else cf end | intr_coiters fcoiters [cq] [cf, cf'] = @@ -1185,7 +1177,7 @@ let val fpT_to_C = fpT --> C; - fun build_prod_proj mk_proj = build_map' lthy (mk_proj o fst); + fun build_prod_proj mk_proj = build_map lthy (mk_proj o fst); (* TODO: Avoid these complications; cf. corec case *) fun mk_U proj (Type (s as @{type_name prod}, Ts as [T', U])) = @@ -1238,7 +1230,7 @@ let val B_to_fpT = C --> fpT; - fun build_sum_inj mk_inj = build_map' lthy (uncurry mk_inj o dest_sumT o snd); + fun build_sum_inj mk_inj = build_map lthy (uncurry mk_inj o dest_sumT o snd); fun build_dtor_coiter_arg _ [] [cf] = cf | build_dtor_coiter_arg T [cq] [cf, cf'] =