Entity definitions within a global or local theory context.
*)
signature ENTITY = sig type'a data_ops =
{get_data: Context.generic -> 'a Name_Space.table,
put_data: 'a Name_Space.table -> Context.generic -> Context.generic} val define_global: 'a data_ops -> binding -> 'a -> theory -> string * theory val define: 'a data_ops -> binding -> 'a -> local_theory -> string * local_theory end;
structure Entity: ENTITY = struct
(* context data *)
type'a data_ops =
{get_data: Context.generic -> 'a Name_Space.table,
put_data: 'a Name_Space.table -> Context.generic -> Context.generic};
(* global definition (foundation) *)
fun define_global {get_data, put_data} b x thy = let val context = Context.Theory thy; val (name, data') = Name_Space.define context true (b, x) (get_data context); in (name, Context.the_theory (put_data data' context)) end;
(* local definition *)
fun alias {get_data, put_data} binding name =
Local_Theory.declaration {syntax = false, pervasive = false, pos = Binding.pos_of binding}
(fn phi => fn context => let val naming = Name_Space.naming_of context; val binding' = Morphism.binding phi binding; val data' = Name_Space.alias_table naming binding' name (get_data context); in put_data data' context end);
fun transfer {get_data, put_data} ctxt = let val data0 = get_data (Context.Theory (Proof_Context.theory_of ctxt)); val data' = Name_Space.merge_tables (data0, get_data (Context.Proof ctxt)); in Context.proof_map (put_data data') ctxt end;
fun define ops binding x =
Local_Theory.background_theory_result (define_global ops binding x)
#-> (fn name =>
Local_Theory.map_contexts (K (transfer ops))
#> alias ops binding name
#> pair name);
end;
¤ Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.0.17Bemerkung:
(vorverarbeitet)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
