# HG changeset patch # User traytel # Date 1394454196 -3600 # Node ID 8875cdcfc85b3423607d9cfa0887d955fc8d23a8 # Parent 57e2cfba9c6eed8164fa4b28fa590cc98ff4802d unfold intermediate definitions after sealing the bnf diff -r 57e2cfba9c6e -r 8875cdcfc85b src/HOL/BNF_Comp.thy --- a/src/HOL/BNF_Comp.thy Sun Mar 09 22:45:09 2014 +0100 +++ b/src/HOL/BNF_Comp.thy Mon Mar 10 13:23:16 2014 +0100 @@ -147,6 +147,9 @@ definition id_bnf_comp :: "'a \ 'a" where "id_bnf_comp \ (\x. x)" +lemma id_bnf_comp_apply: "id_bnf_comp x = x" + unfolding id_bnf_comp_def by simp + bnf ID: 'a map: "id_bnf_comp :: ('a \ 'b) \ 'a \ 'b" sets: "\x. {x}" diff -r 57e2cfba9c6e -r 8875cdcfc85b src/HOL/Library/bnf_decl.ML --- a/src/HOL/Library/bnf_decl.ML Sun Mar 09 22:45:09 2014 +0100 +++ b/src/HOL/Library/bnf_decl.ML Mon Mar 10 13:23:16 2014 +0100 @@ -68,7 +68,7 @@ val Fwits = map2 (fn witb => fn witT => Const (Local_Theory.full_name lthy witb, witT)) witbs witTs; val (key, goals, (triv_tac_opt, wit_goalss), after_qed, lthy, _) = - prepare_def Do_Inline (user_policy Note_Some) I (K I) (K I) (SOME (map TFree deads)) + prepare_def Do_Inline (user_policy Note_Some) false I (K I) (K I) (SOME (map TFree deads)) user_mapb user_relb user_setbs ((((((Binding.empty, T), Fmap), Fsets), Fbd), Fwits), NONE) lthy; diff -r 57e2cfba9c6e -r 8875cdcfc85b src/HOL/Tools/BNF/bnf_comp.ML --- a/src/HOL/Tools/BNF/bnf_comp.ML Sun Mar 09 22:45:09 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_comp.ML Mon Mar 10 13:23:16 2014 +0100 @@ -338,8 +338,8 @@ (maps wit_thms_of_bnf inners); val (bnf', lthy') = - bnf_def const_policy (K Dont_Note) qualify tacs wit_tac (SOME (oDs @ flat Dss)) Binding.empty - Binding.empty [] ((((((b, CCA), mapx), sets'), bd'), wits), SOME rel) lthy; + bnf_def const_policy (K Dont_Note) true qualify tacs wit_tac (SOME (oDs @ flat Dss)) + Binding.empty Binding.empty [] ((((((b, CCA), mapx), sets'), bd'), wits), SOME rel) lthy; val phi = Morphism.thm_morphism "BNF" (unfold_thms lthy' [id_bnf_comp_def]) @@ -436,8 +436,8 @@ fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf); val (bnf', lthy') = - bnf_def Smart_Inline (K Dont_Note) qualify tacs wit_tac (SOME (killedAs @ Ds)) Binding.empty - Binding.empty [] ((((((b, T), mapx), sets), bd), wits), SOME rel) lthy; + bnf_def Smart_Inline (K Dont_Note) true qualify tacs wit_tac (SOME (killedAs @ Ds)) + Binding.empty Binding.empty [] ((((((b, T), mapx), sets), bd), wits), SOME rel) lthy; in (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy')) end; @@ -526,8 +526,8 @@ fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf); val (bnf', lthy') = - bnf_def Smart_Inline (K Dont_Note) qualify tacs wit_tac (SOME Ds) Binding.empty Binding.empty - [] ((((((b, T), mapx), sets), bd), wits), SOME rel) lthy; + bnf_def Smart_Inline (K Dont_Note) true qualify tacs wit_tac (SOME Ds) Binding.empty + Binding.empty [] ((((((b, T), mapx), sets), bd), wits), SOME rel) lthy; in (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy')) end; @@ -607,8 +607,8 @@ fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf); val (bnf', lthy') = - bnf_def Smart_Inline (K Dont_Note) qualify tacs wit_tac (SOME Ds) Binding.empty Binding.empty - [] ((((((b, T), mapx), sets), bd), wits), SOME rel) lthy; + bnf_def Smart_Inline (K Dont_Note) true qualify tacs wit_tac (SOME Ds) Binding.empty + Binding.empty [] ((((((b, T), mapx), sets), bd), wits), SOME rel) lthy; in (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy')) end; @@ -765,21 +765,6 @@ |> mk_Frees' "f" (map2 (curry op -->) As Bs) ||>> mk_Frees' "R" (map2 mk_pred2T As Bs); - val map_unfolds = map (unfold_thms lthy [id_bnf_comp_def]) (#map_unfolds unfold_set); - val set_unfoldss = #set_unfoldss unfold_set; - val rel_unfolds = map (unfold_thms lthy [id_bnf_comp_def]) (#rel_unfolds unfold_set); - - val expand_maps = expand_id_bnf_comp_def o - fold expand_term_const (map (single o Logic.dest_equals o Thm.prop_of) map_unfolds); - val expand_sets = - fold expand_term_const (map (map (Logic.dest_equals o Thm.prop_of)) set_unfoldss); - val expand_rels = expand_id_bnf_comp_def o - fold expand_term_const (map (single o Logic.dest_equals o Thm.prop_of) rel_unfolds); - fun unfold_maps ctxt = fold (unfold_thms ctxt o single) (id_bnf_comp_def :: map_unfolds); - fun unfold_sets ctxt = fold (unfold_thms ctxt) set_unfoldss; - fun unfold_rels ctxt = fold (unfold_thms ctxt o single) (id_bnf_comp_def :: rel_unfolds); - fun unfold_all ctxt = unfold_sets ctxt o unfold_maps ctxt o unfold_rels ctxt; - val repTA = mk_T_of_bnf Ds As bnf; val T_bind = qualify b; val TA_params = Term.add_tfreesT repTA []; @@ -800,12 +785,12 @@ abs_inverse = Abs_inverse', type_definition = type_definition}; val bnf_map = fold_rev Term.absfree fs' (HOLogic.mk_comp (HOLogic.mk_comp (AbsB, - Term.list_comb (expand_maps (mk_map_of_bnf Ds As Bs bnf), fs)), RepA)); - val bnf_sets = map ((fn t => HOLogic.mk_comp (t, RepA)) o expand_maps o expand_sets) + Term.list_comb (mk_map_of_bnf Ds As Bs bnf, fs)), RepA)); + val bnf_sets = map ((fn t => HOLogic.mk_comp (t, RepA))) (mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf); val bnf_bd = mk_bd_of_bnf Ds As bnf; val bnf_rel = fold_rev Term.absfree Rs' (mk_vimage2p RepA RepB $ - (Term.list_comb (expand_rels (mk_rel_of_bnf Ds As Bs bnf), Rs))); + (Term.list_comb (mk_rel_of_bnf Ds As Bs bnf, Rs))); (*bd may depend only on dead type variables*) val bd_repT = fst (dest_relT (fastype_of bnf_bd)); @@ -836,24 +821,22 @@ (bnf_bd', bd_ordIso, bd_card_order, bd_cinfinite) end; - fun map_id0_tac ctxt = - rtac (@{thm type_copy_map_id0} OF [type_definition, unfold_maps ctxt (map_id0_of_bnf bnf)]) 1; - fun map_comp0_tac ctxt = - rtac (@{thm type_copy_map_comp0} OF - [type_definition, unfold_maps ctxt (map_comp0_of_bnf bnf)]) 1; - fun map_cong0_tac ctxt = - EVERY' (rtac @{thm type_copy_map_cong0} :: rtac (unfold_all ctxt (map_cong0_of_bnf bnf)) :: + fun map_id0_tac _ = + rtac (@{thm type_copy_map_id0} OF [type_definition, map_id0_of_bnf bnf]) 1; + fun map_comp0_tac _ = + rtac (@{thm type_copy_map_comp0} OF [type_definition, map_comp0_of_bnf bnf]) 1; + fun map_cong0_tac _ = + EVERY' (rtac @{thm type_copy_map_cong0} :: rtac (map_cong0_of_bnf bnf) :: map (fn i => EVERY' [select_prem_tac live (dtac meta_spec) i, etac meta_mp, etac (o_apply RS equalityD2 RS set_mp)]) (1 upto live)) 1; - fun set_map0_tac thm ctxt = - rtac (@{thm type_copy_set_map0} OF [type_definition, unfold_all ctxt thm]) 1; - val set_bd_tacs = map (fn thm => fn ctxt => rtac (@{thm ordLeq_ordIso_trans} OF - [unfold_sets ctxt thm, bd_ordIso] RS @{thm type_copy_set_bd}) 1) - (set_bd_of_bnf bnf); - fun le_rel_OO_tac ctxt = - rtac (unfold_rels ctxt (le_rel_OO_of_bnf bnf) RS @{thm vimage2p_relcompp_mono}) 1; + fun set_map0_tac thm _ = + rtac (@{thm type_copy_set_map0} OF [type_definition, thm]) 1; + val set_bd_tacs = map (fn thm => fn _ => rtac (@{thm ordLeq_ordIso_trans} OF + [thm, bd_ordIso] RS @{thm type_copy_set_bd}) 1) (set_bd_of_bnf bnf); + fun le_rel_OO_tac _ = + rtac (le_rel_OO_of_bnf bnf RS @{thm vimage2p_relcompp_mono}) 1; fun rel_OO_Grp_tac ctxt = - (rtac (unfold_all ctxt (rel_OO_Grp_of_bnf bnf) RS @{thm vimage2p_cong} RS trans) THEN' + (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; @@ -864,18 +847,40 @@ val bnf_wits = map (fn (I, t) => fold Term.absdummy (map (nth As) I) - (AbsA $ Term.list_comb (expand_id_bnf_comp_def t, map Bound (0 upto length I - 1)))) + (AbsA $ Term.list_comb (t, map Bound (0 upto length I - 1)))) (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf); - fun wit_tac ctxt = ALLGOALS (dtac (type_definition RS @{thm type_copy_wit})) THEN - mk_simple_wit_tac (map (unfold_all ctxt) (wit_thms_of_bnf bnf)); + fun wit_tac _ = ALLGOALS (dtac (type_definition RS @{thm type_copy_wit})) THEN + mk_simple_wit_tac (wit_thms_of_bnf bnf); val (bnf', lthy') = - bnf_def Hardly_Inline (user_policy Dont_Note) qualify tacs wit_tac (SOME all_deads) + bnf_def Hardly_Inline (user_policy Dont_Note) true qualify tacs wit_tac (SOME all_deads) Binding.empty Binding.empty [] ((((((b, TA), bnf_map), bnf_sets), bnf_bd'), bnf_wits), SOME bnf_rel) lthy; + + val unfolds = @{thm id_bnf_comp_apply} :: + (#map_unfolds unfold_set @ flat (#set_unfoldss unfold_set) @ #rel_unfolds unfold_set); + + val bnf'' = bnf' |> morph_bnf_defs (Morphism.thm_morphism "BNF" (unfold_thms lthy' unfolds)); + + val map_def = map_def_of_bnf bnf''; + val set_defs = set_defs_of_bnf bnf''; + val rel_def = map_def_of_bnf bnf''; + + val bnf_b = qualify b; + val def_qualify = + Thm.def_binding o Binding.conceal o Binding.qualify false (Binding.name_of bnf_b); + fun mk_prefix_binding pre = Binding.prefix_name (pre ^ "_") bnf_b; + val map_b = def_qualify (mk_prefix_binding mapN); + val rel_b = def_qualify (mk_prefix_binding relN); + val set_bs = if live = 1 then [def_qualify (mk_prefix_binding setN)] + else map (fn i => def_qualify (mk_prefix_binding (mk_setN i))) (1 upto live); + + val notes = (map_b, map_def) :: (rel_b, rel_def) :: (set_bs ~~ set_defs) + |> map (fn (b, def) => ((b, []), [([def], [])])) + val lthy'' = lthy' |> Local_Theory.notes notes |> snd in - ((bnf', (all_deads, absT_info)), lthy') + ((bnf'', (all_deads, absT_info)), lthy'') end; exception BAD_DEAD of typ * typ; diff -r 57e2cfba9c6e -r 8875cdcfc85b src/HOL/Tools/BNF/bnf_def.ML --- a/src/HOL/Tools/BNF/bnf_def.ML Sun Mar 09 22:45:09 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_def.ML Mon Mar 10 13:23:16 2014 +0100 @@ -12,6 +12,7 @@ type nonemptiness_witness = {I: int list, wit: term, prop: thm list} val morph_bnf: morphism -> bnf -> bnf + val morph_bnf_defs: morphism -> bnf -> bnf val bnf_of: Proof.context -> string -> bnf option val register_bnf: string -> (bnf * local_theory) -> (bnf * local_theory) @@ -100,16 +101,16 @@ Proof.context val print_bnfs: Proof.context -> unit - val prepare_def: inline_policy -> (Proof.context -> fact_policy) -> (binding -> binding) -> - (Proof.context -> 'a -> typ) -> (Proof.context -> 'b -> term) -> typ list option -> - binding -> binding -> binding list -> + val prepare_def: inline_policy -> (Proof.context -> fact_policy) -> bool -> + (binding -> binding) -> (Proof.context -> 'a -> typ) -> (Proof.context -> 'b -> term) -> + typ list option -> binding -> binding -> binding list -> (((((binding * 'a) * 'b) * 'b list) * 'b) * 'b list) * 'b option -> Proof.context -> string * term list * ((Proof.context -> thm list -> tactic) option * term list list) * ((thm list -> thm list list) -> thm list list -> Proof.context -> bnf * local_theory) * local_theory * thm list - val define_bnf_consts: inline_policy -> fact_policy -> typ list option -> + val define_bnf_consts: inline_policy -> fact_policy -> bool -> typ list option -> binding -> binding -> binding list -> (((((binding * typ) * term) * term list) * term) * term list) * term option -> local_theory -> ((typ list * typ list * typ list * typ) * @@ -121,7 +122,7 @@ (typ list -> typ list -> typ list -> term) * (typ list -> typ list -> typ list -> term))) * local_theory - val bnf_def: inline_policy -> (Proof.context -> fact_policy) -> (binding -> binding) -> + val bnf_def: inline_policy -> (Proof.context -> fact_policy) -> bool -> (binding -> binding) -> (Proof.context -> tactic) list -> (Proof.context -> tactic) -> typ list option -> binding -> binding -> binding list -> @@ -434,22 +435,27 @@ axioms = axioms, defs = defs, facts = facts, nwits = length wits, wits = wits, rel = rel}; -fun morph_bnf phi (BNF {name = name, T = T, live = live, lives = lives, lives' = lives', +fun map_bnf f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 + (BNF {name = name, T = T, live = live, lives = lives, lives' = lives', dead = dead, deads = deads, map = map, sets = sets, bd = bd, axioms = axioms, defs = defs, facts = facts, nwits = nwits, wits = wits, rel = rel}) = - BNF {name = Morphism.binding phi name, T = Morphism.typ phi T, - live = live, lives = List.map (Morphism.typ phi) lives, - lives' = List.map (Morphism.typ phi) lives', - dead = dead, deads = List.map (Morphism.typ phi) deads, - map = Morphism.term phi map, sets = List.map (Morphism.term phi) sets, - bd = Morphism.term phi bd, - axioms = morph_axioms phi axioms, - defs = morph_defs phi defs, - facts = morph_facts phi facts, - nwits = nwits, - wits = List.map (morph_witness phi) wits, - rel = Morphism.term phi rel}; + BNF {name = f1 name, T = f2 T, + live = f3 live, lives = f4 lives, lives' = f5 lives', dead = f6 dead, deads = f7 deads, + map = f8 map, sets = f9 sets, bd = f10 bd, + axioms = f11 axioms, defs = f12 defs, facts = f13 facts, + nwits = f14 nwits, wits = f15 wits, rel = f16 rel}; + +fun morph_bnf phi = + let + val Tphi = Morphism.typ phi; + val tphi = Morphism.term phi; + in + map_bnf (Morphism.binding phi) Tphi I (map Tphi) (map Tphi) I (map Tphi) tphi (map tphi) tphi + (morph_axioms phi) (morph_defs phi) (morph_facts phi) I (map (morph_witness phi)) tphi + end; + +fun morph_bnf_defs phi = map_bnf I I I I I I I I I I I (morph_defs phi) I I I I; structure Data = Generic_Data ( @@ -660,7 +666,7 @@ (* Define new BNFs *) -fun define_bnf_consts const_policy fact_policy Ds_opt map_b rel_b set_bs +fun define_bnf_consts const_policy fact_policy internal Ds_opt map_b rel_b set_bs ((((((bnf_b, T_rhs), map_rhs), set_rhss), bd_rhs), wit_rhss), rel_rhs_opt) no_defs_lthy = let val live = length set_rhss; @@ -683,8 +689,9 @@ ((rhs, Drule.reflexive_thm), lthy) else let val b = b () in - apfst (apsnd snd) (Local_Theory.define ((b, NoSyn), ((Thm.def_binding b, []), rhs)) - lthy) + apfst (apsnd snd) + ((if internal then Local_Theory.define_internal else Local_Theory.define) + ((b, NoSyn), ((Thm.def_binding b, []), rhs)) lthy) end end; @@ -830,8 +837,8 @@ (mk_bnf_map, mk_bnf_t, mk_bnf_T, mk_bnf_rel, mk_OO_Grp)), lthy) end; -fun prepare_def const_policy mk_fact_policy qualify prep_typ prep_term Ds_opt map_b rel_b set_bs - ((((((raw_bnf_b, raw_bnf_T), raw_map), raw_sets), raw_bd), raw_wits), raw_rel_opt) +fun prepare_def const_policy mk_fact_policy internal qualify prep_typ prep_term Ds_opt map_b rel_b + set_bs ((((((raw_bnf_b, raw_bnf_T), raw_map), raw_sets), raw_bd), raw_wits), raw_rel_opt) no_defs_lthy = let val fact_policy = mk_fact_policy no_defs_lthy; @@ -861,7 +868,7 @@ (bnf_map, bnf_sets, bnf_bd, bnf_wits, bnf_rel), (bnf_map_def, bnf_set_defs, bnf_bd_def, bnf_wit_defs, bnf_rel_def), (mk_bnf_map_Ds, mk_bnf_t_Ds, mk_bnf_T_Ds, _, mk_OO_Grp)), lthy) = - define_bnf_consts const_policy fact_policy Ds_opt map_b rel_b set_bs + define_bnf_consts const_policy fact_policy internal Ds_opt map_b rel_b set_bs ((((((bnf_b, T_rhs), map_rhs), set_rhss), bd_rhs), wit_rhss), rel_rhs_opt) no_defs_lthy; val dead = length deads; @@ -1304,7 +1311,7 @@ (bnf, Local_Theory.declaration {syntax = false, pervasive = true} (fn phi => Data.map (Symtab.update (key, morph_bnf phi bnf))) lthy); -fun bnf_def const_policy fact_policy qualify tacs wit_tac Ds map_b rel_b set_bs = +fun bnf_def const_policy fact_policy internal qualify tacs wit_tac Ds map_b rel_b set_bs = (fn (_, goals, (triv_tac_opt, wit_goalss), after_qed, lthy, one_step_defs) => let fun mk_wits_tac ctxt set_maps = @@ -1324,7 +1331,7 @@ goals (map (fn tac => fn {context = ctxt, prems = _} => unfold_thms_tac ctxt one_step_defs THEN tac ctxt) tacs) |> (fn thms => after_qed mk_wit_thms (map single thms) lthy) - end) oo prepare_def const_policy fact_policy qualify (K I) (K I) Ds map_b rel_b set_bs; + end) oo prepare_def const_policy fact_policy internal qualify (K I) (K I) Ds map_b rel_b set_bs; val bnf_cmd = (fn (key, goals, (triv_tac_opt, wit_goalss), after_qed, lthy, defs) => let @@ -1343,8 +1350,8 @@ Proof.unfolding ([[(defs, [])]]) (Proof.theorem NONE (snd o register_bnf key oo after_qed mk_wit_thms) (map (single o rpair []) goals @ nontriv_wit_goals) lthy) - end) oo prepare_def Do_Inline (user_policy Note_Some) I Syntax.read_typ Syntax.read_term NONE - Binding.empty Binding.empty []; + end) oo prepare_def Do_Inline (user_policy Note_Some) false I Syntax.read_typ Syntax.read_term + NONE Binding.empty Binding.empty []; fun print_bnfs ctxt = let diff -r 57e2cfba9c6e -r 8875cdcfc85b src/HOL/Tools/BNF/bnf_gfp.ML --- a/src/HOL/Tools/BNF/bnf_gfp.ML Sun Mar 09 22:45:09 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_gfp.ML Mon Mar 10 13:23:16 2014 +0100 @@ -2088,7 +2088,7 @@ val (Jbnf_consts, lthy) = fold_map8 (fn b => fn map_b => fn rel_b => fn set_bs => fn mapx => fn sets => fn wits => fn T => fn lthy => - define_bnf_consts Dont_Inline (user_policy Note_Some lthy) (SOME deads) + define_bnf_consts Dont_Inline (user_policy Note_Some lthy) false (SOME deads) map_b rel_b set_bs ((((((b, T), fold_rev Term.absfree fs' mapx), sets), sbd), wits), NONE) lthy) bs map_bs rel_bs set_bss fs_maps setss_by_bnf all_witss Ts lthy; @@ -2516,7 +2516,7 @@ val (Jbnfs, lthy) = fold_map7 (fn b => fn tacs => fn map_b => fn rel_b => fn set_bs => fn Jwit_thms => fn consts => fn lthy => - bnf_def Do_Inline (user_policy Note_Some) I tacs (wit_tac Jwit_thms) (SOME deads) + bnf_def Do_Inline (user_policy Note_Some) false I tacs (wit_tac Jwit_thms) (SOME deads) map_b rel_b set_bs consts lthy |> register_bnf (Local_Theory.full_name lthy b)) bs tacss map_bs rel_bs set_bss Jwit_thmss diff -r 57e2cfba9c6e -r 8875cdcfc85b src/HOL/Tools/BNF/bnf_lfp.ML --- a/src/HOL/Tools/BNF/bnf_lfp.ML Sun Mar 09 22:45:09 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_lfp.ML Mon Mar 10 13:23:16 2014 +0100 @@ -1483,7 +1483,7 @@ val (Ibnf_consts, lthy) = fold_map8 (fn b => fn map_b => fn rel_b => fn set_bs => fn mapx => fn sets => fn wits => fn T => fn lthy => - define_bnf_consts Dont_Inline (user_policy Note_Some lthy) (SOME deads) + define_bnf_consts Dont_Inline (user_policy Note_Some lthy) false (SOME deads) map_b rel_b set_bs ((((((b, T), fold_rev Term.absfree fs' mapx), sets), sbd), wits), NONE) lthy) bs map_bs rel_bs set_bss fs_maps setss_by_bnf ctor_witss Ts lthy; @@ -1769,7 +1769,7 @@ val (Ibnfs, lthy) = fold_map6 (fn b => fn tacs => fn map_b => fn rel_b => fn set_bs => fn consts => fn lthy => - bnf_def Do_Inline (user_policy Note_Some) I tacs wit_tac (SOME deads) + bnf_def Do_Inline (user_policy Note_Some) false I tacs wit_tac (SOME deads) map_b rel_b set_bs consts lthy |> register_bnf (Local_Theory.full_name lthy b)) bs tacss map_bs rel_bs set_bss