diff -r 054e9a9fccad -r be0f5d8d511b src/HOL/Tools/BNF/bnf_comp.ML --- a/src/HOL/Tools/BNF/bnf_comp.ML Fri Sep 12 17:51:31 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_comp.ML Sat Sep 13 18:08:38 2014 +0200 @@ -42,7 +42,7 @@ val mk_repT: typ -> typ -> typ -> typ val mk_abs: typ -> term -> term val mk_rep: typ -> term -> term - val seal_bnf: (binding -> binding) -> unfold_set -> binding -> typ list -> BNF_Def.bnf -> + val seal_bnf: (binding -> binding) -> unfold_set -> binding -> bool -> typ list -> BNF_Def.bnf -> local_theory -> (BNF_Def.bnf * (typ list * absT_info)) * local_theory end; @@ -629,7 +629,7 @@ lift_bnf qualify n bnf #> uncurry (permute_bnf qualify src dest); -fun normalize_bnfs qualify Ass Ds sort bnfs accum = +fun normalize_bnfs qualify Ass Ds flatten_tyargs bnfs accum = let val before_kill_src = map (fn As => 0 upto (length As - 1)) Ass; val kill_poss = map (find_indices op = Ds) Ass; @@ -642,7 +642,7 @@ kill_ns before_kill_src before_kill_dest bnfs accum; val Ass' = map2 (map o nth) Ass live_poss; - val As = sort Ass'; + val As = flatten_tyargs Ass'; val after_lift_dest = replicate (length Ass') (0 upto (length As - 1)); val old_poss = map (map (fn x => find_index (fn y => x = y) As)) Ass'; val new_poss = map2 (subtract op =) old_poss after_lift_dest; @@ -657,7 +657,7 @@ fun default_comp_sort Ass = Library.sort (Term_Ord.typ_ord o pairself TFree) (fold (fold (insert (op =))) Ass []); -fun raw_compose_bnf const_policy qualify sort outer inners oDs Dss tfreess accum = +fun raw_compose_bnf const_policy qualify flatten_tyargs outer inners oDs Dss tfreess accum = let val b = name_of_bnf outer; @@ -665,7 +665,7 @@ val Ds = fold (fold Term.add_tfreesT) (oDs :: Dss) []; val ((kill_poss, As), (inners', ((cache', unfold_set'), lthy'))) = - normalize_bnfs qualify Ass Ds sort inners accum; + normalize_bnfs qualify Ass Ds flatten_tyargs inners accum; val Ds = oDs @ flat (map3 (uncurry append oo curry swap oo map o nth) tfreess kill_poss Dss); val As = map TFree As; @@ -675,12 +675,14 @@ (clean_compose_bnf const_policy (qualify 0) b outer inners' (unfold_set', lthy'))) end; -fun compose_bnf const_policy qualify sort outer inners oDs Dss tfreess (accum as ((cache, _), _)) = +fun compose_bnf const_policy qualify flatten_tyargs outer inners oDs Dss tfreess + (accum as ((cache, _), _)) = let val key = key_of_compose oDs Dss tfreess outer inners in (case Typtab.lookup cache key of SOME bnf_Ds_As => (bnf_Ds_As, accum) | NONE => - cache_comp key (raw_compose_bnf const_policy qualify sort outer inners oDs Dss tfreess accum)) + cache_comp key + (raw_compose_bnf const_policy qualify flatten_tyargs outer inners oDs Dss tfreess accum)) end; (* Hide the type of the bound (optimization) and unfold the definitions (nicer to the user) *) @@ -730,35 +732,34 @@ val smart_max_inline_type_size = 5; (*FUDGE*) -fun maybe_typedef (b, As, mx) set opt_morphs tac = +fun maybe_typedef force_out_of_line (b, As, mx) set opt_morphs tac = let val repT = HOLogic.dest_setT (fastype_of set); - val inline = Term.size_of_typ repT <= smart_max_inline_type_size; + val out_of_line = force_out_of_line orelse Term.size_of_typ repT > smart_max_inline_type_size; in - if inline then + if out_of_line then + typedef (b, As, mx) set opt_morphs tac + #>> (fn (T_name, ({Rep_name, Abs_name, ...}, + {type_definition, Abs_inverse, Abs_inject, Abs_cases, ...}) : Typedef.info) => + (Type (T_name, map TFree As), + (Rep_name, Abs_name, type_definition, Abs_inverse, Abs_inject, Abs_cases))) + else pair (repT, (@{const_name id_bnf}, @{const_name id_bnf}, @{thm type_definition_id_bnf_UNIV}, @{thm type_definition.Abs_inverse[OF type_definition_id_bnf_UNIV]}, @{thm type_definition.Abs_inject[OF type_definition_id_bnf_UNIV]}, @{thm type_definition.Abs_cases[OF type_definition_id_bnf_UNIV]})) - else - typedef (b, As, mx) set opt_morphs tac - #>> (fn (T_name, ({Rep_name, Abs_name, ...}, - {type_definition, Abs_inverse, Abs_inject, Abs_cases, ...}) : Typedef.info) => - (Type (T_name, map TFree As), - (Rep_name, Abs_name, type_definition, Abs_inverse, Abs_inject, Abs_cases))) end; -fun seal_bnf qualify (unfold_set : unfold_set) b Ds bnf lthy = +fun seal_bnf qualify (unfold_set : unfold_set) b has_live_phantoms Ds bnf lthy = let val live = live_of_bnf bnf; val nwits = nwits_of_bnf bnf; - val (As, lthy1) = apfst (map TFree) + val ((As, As'), lthy1) = apfst (`(map TFree)) (Variable.invent_types (replicate live @{sort type}) (fold Variable.declare_typ Ds lthy)); - val (Bs, _) = apfst (map TFree) - (Variable.invent_types (replicate live @{sort type}) lthy1); + val (Bs, _) = apfst (map TFree) (Variable.invent_types (replicate live @{sort type}) lthy1); val (((fs, fs'), (Rs, Rs')), _(*names_lthy*)) = lthy |> mk_Frees' "f" (map2 (curry op -->) As Bs) @@ -766,10 +767,10 @@ val repTA = mk_T_of_bnf Ds As bnf; val T_bind = qualify b; - val TA_params = Term.add_tfreesT repTA []; + val TA_params = Term.add_tfreesT repTA (if has_live_phantoms then As' else []); val ((TA, (Rep_name, Abs_name, type_definition, Abs_inverse, Abs_inject, _)), lthy) = - maybe_typedef (T_bind, TA_params, NoSyn) - (HOLogic.mk_UNIV repTA) NONE (EVERY' [rtac exI, rtac UNIV_I] 1) lthy; + maybe_typedef has_live_phantoms (T_bind, TA_params, NoSyn) (HOLogic.mk_UNIV repTA) NONE + (EVERY' [rtac exI, rtac UNIV_I] 1) lthy; val repTB = mk_T_of_bnf Ds Bs bnf; val TB = Term.typ_subst_atomic (As ~~ Bs) TA; @@ -798,7 +799,7 @@ val all_deads = map TFree (fold Term.add_tfreesT Ds []); val ((bdT, (_, Abs_bd_name, _, _, Abs_bdT_inject, Abs_bdT_cases)), lthy) = - maybe_typedef (bdT_bind, params, NoSyn) + maybe_typedef false (bdT_bind, params, NoSyn) (HOLogic.mk_UNIV bd_repT) NONE (EVERY' [rtac exI, rtac UNIV_I] 1) lthy; val (bnf_bd', bd_ordIso, bd_card_order, bd_cinfinite) = @@ -836,9 +837,11 @@ rtac (le_rel_OO_of_bnf bnf RS @{thm vimage2p_relcompp_mono}) 1; fun rel_OO_Grp_tac ctxt = (rtac (rel_OO_Grp_of_bnf bnf RS @{thm vimage2p_cong} RS trans) THEN' - SELECT_GOAL (unfold_thms_tac ctxt [o_apply, - type_definition RS @{thm type_copy_vimage2p_Grp_Rep}, - type_definition RS @{thm vimage2p_relcompp_converse}]) THEN' rtac refl) 1; + subst_tac ctxt NONE [type_definition RS @{thm vimage2p_relcompp_converse}] THEN' + SELECT_GOAL (unfold_thms_tac ctxt [o_apply, + type_definition RS @{thm type_copy_vimage2p_Grp_Rep}, + type_definition RS @{thm vimage2p_relcompp_converse}]) THEN' + rtac refl) 1; val tacs = zip_axioms map_id0_tac map_comp0_tac map_cong0_tac (map set_map0_tac (set_map0_of_bnf bnf)) (K (rtac bd_card_order 1)) (K (rtac bd_cinfinite 1)) @@ -888,7 +891,8 @@ fun bnf_of_typ _ _ _ _ Ds0 (T as TFree T') accum = (if member (op =) Ds0 T' then (DEADID_bnf, ([T], [])) else (ID_bnf, ([], [T])), accum) | bnf_of_typ _ _ _ _ _ (TVar _) _ = error "Unexpected schematic variable" - | bnf_of_typ const_policy qualify' sort Xs Ds0 (T as Type (C, Ts)) (accum as (_, lthy)) = + | bnf_of_typ const_policy qualify' flatten_tyargs Xs Ds0 (T as Type (C, Ts)) + (accum as (_, lthy)) = let fun check_bad_dead ((_, (deads, _)), _) = let val Ds = fold Term.add_tfreesT deads [] in @@ -926,10 +930,10 @@ val Ts' = map (nth Ts) (subtract (op =) oDs_pos (0 upto length Ts - 1)); val ((inners, (Dss, Ass)), (accum', lthy')) = apfst (apsnd split_list o split_list) - (fold_map2 (fn i => bnf_of_typ Smart_Inline (qualify i) sort Xs Ds0) + (fold_map2 (fn i => bnf_of_typ Smart_Inline (qualify i) flatten_tyargs Xs Ds0) (if length Ts' = 1 then [0] else (1 upto length Ts')) Ts' accum); in - compose_bnf const_policy qualify sort bnf inners oDs Dss Ass (accum', lthy') + compose_bnf const_policy qualify flatten_tyargs bnf inners oDs Dss Ass (accum', lthy') end) |> tap check_bad_dead end;