common entity definitions within a global or local theory context;
authorwenzelm
Thu May 12 22:06:18 2016 +0200 (2016-05-12)
changeset 630907aa9ac5165e4
parent 63089 40134ddec3bf
child 63091 54f16a0a3069
common entity definitions within a global or local theory context;
src/Pure/Isar/attrib.ML
src/Pure/Isar/entity.ML
src/Pure/Isar/local_theory.ML
src/Pure/Isar/method.ML
src/Pure/ROOT.ML
     1.1 --- a/src/Pure/Isar/attrib.ML	Thu May 12 14:38:53 2016 +0200
     1.2 +++ b/src/Pure/Isar/attrib.ML	Thu May 12 22:06:18 2016 +0200
     1.3 @@ -109,13 +109,9 @@
     1.4    fun merge data : T = Name_Space.merge_tables data;
     1.5  );
     1.6  
     1.7 -val get_attributes = Attributes.get o Context.Proof;
     1.8 +val ops_attributes = {get_data = Attributes.get, put_data = Attributes.put};
     1.9  
    1.10 -fun transfer_attributes ctxt =
    1.11 -  let
    1.12 -    val attribs0 = Attributes.get (Context.Theory (Proof_Context.theory_of ctxt));
    1.13 -    val attribs' = Name_Space.merge_tables (attribs0, get_attributes ctxt);
    1.14 -  in Context.proof_map (Attributes.put attribs') ctxt end;
    1.15 +val get_attributes = Attributes.get o Context.Proof;
    1.16  
    1.17  fun print_attributes verbose ctxt =
    1.18    let
    1.19 @@ -134,19 +130,11 @@
    1.20  
    1.21  (* define *)
    1.22  
    1.23 -fun define_global binding att comment thy =
    1.24 -  let
    1.25 -    val context = Context.Theory thy;
    1.26 -    val (name, attribs') =
    1.27 -      Name_Space.define context true (binding, (att, comment)) (Attributes.get context);
    1.28 -  in (name, Context.the_theory (Attributes.put attribs' context)) end;
    1.29 +fun define_global binding att comment =
    1.30 +  Entity.define_global ops_attributes binding (att, comment);
    1.31  
    1.32  fun define binding att comment =
    1.33 -  Local_Theory.background_theory_result (define_global binding att comment)
    1.34 -  #-> (fn name =>
    1.35 -    Local_Theory.map_contexts (K transfer_attributes)
    1.36 -    #> Local_Theory.generic_alias Attributes.map binding name
    1.37 -    #> pair name);
    1.38 +  Entity.define ops_attributes binding (att, comment);
    1.39  
    1.40  
    1.41  (* check *)
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/Pure/Isar/entity.ML	Thu May 12 22:06:18 2016 +0200
     2.3 @@ -0,0 +1,58 @@
     2.4 +(*  Title:      Pure/Isar/entity.ML
     2.5 +    Author:     Makarius
     2.6 +
     2.7 +Entity definitions within a global or local theory context.
     2.8 +*)
     2.9 +
    2.10 +signature ENTITY =
    2.11 +sig
    2.12 +  type 'a data_ops =
    2.13 +   {get_data: Context.generic -> 'a Name_Space.table,
    2.14 +    put_data: 'a Name_Space.table -> Context.generic -> Context.generic}
    2.15 +  val define_global: 'a data_ops -> binding -> 'a -> theory -> string * theory
    2.16 +  val define: 'a data_ops -> binding -> 'a -> local_theory -> string * local_theory
    2.17 +end;
    2.18 +
    2.19 +structure Entity: ENTITY =
    2.20 +struct
    2.21 +
    2.22 +(* context data *)
    2.23 +
    2.24 +type 'a data_ops =
    2.25 + {get_data: Context.generic -> 'a Name_Space.table,
    2.26 +  put_data: 'a Name_Space.table -> Context.generic -> Context.generic};
    2.27 +
    2.28 +
    2.29 +(* global definition (foundation) *)
    2.30 +
    2.31 +fun define_global {get_data, put_data} b x thy =
    2.32 +  let
    2.33 +    val context = Context.Theory thy;
    2.34 +    val (name, data') = Name_Space.define context true (b, x) (get_data context);
    2.35 +  in (name, Context.the_theory (put_data data' context)) end;
    2.36 +
    2.37 +
    2.38 +(* local definition *)
    2.39 +
    2.40 +fun alias {get_data, put_data} binding name =
    2.41 +  Local_Theory.declaration {syntax = false, pervasive = false} (fn phi => fn context =>
    2.42 +    let
    2.43 +      val naming = Name_Space.naming_of context;
    2.44 +      val binding' = Morphism.binding phi binding;
    2.45 +      val data' = Name_Space.alias_table naming binding' name (get_data context);
    2.46 +    in put_data data' context end);
    2.47 +
    2.48 +fun transfer {get_data, put_data} ctxt =
    2.49 +  let
    2.50 +    val data0 = get_data (Context.Theory (Proof_Context.theory_of ctxt));
    2.51 +    val data' = Name_Space.merge_tables (data0, get_data (Context.Proof ctxt));
    2.52 +  in Context.proof_map (put_data data') ctxt end;
    2.53 +
    2.54 +fun define ops binding x =
    2.55 +  Local_Theory.background_theory_result (define_global ops binding x)
    2.56 +  #-> (fn name =>
    2.57 +    Local_Theory.map_contexts (K (transfer ops))
    2.58 +    #> alias ops binding name
    2.59 +    #> pair name);
    2.60 +
    2.61 +end;
     3.1 --- a/src/Pure/Isar/local_theory.ML	Thu May 12 14:38:53 2016 +0200
     3.2 +++ b/src/Pure/Isar/local_theory.ML	Thu May 12 22:06:18 2016 +0200
     3.3 @@ -61,9 +61,6 @@
     3.4    val set_defsort: sort -> local_theory -> local_theory
     3.5    val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> local_theory -> local_theory
     3.6    val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
     3.7 -  val generic_alias:
     3.8 -    (('a Name_Space.table -> 'a Name_Space.table) -> Context.generic -> Context.generic) ->
     3.9 -    binding -> string -> local_theory -> local_theory
    3.10    val class_alias: binding -> class -> local_theory -> local_theory
    3.11    val type_alias: binding -> string -> local_theory -> local_theory
    3.12    val const_alias: binding -> string -> local_theory -> local_theory
    3.13 @@ -329,13 +326,6 @@
    3.14  
    3.15  (* name space aliases *)
    3.16  
    3.17 -fun generic_alias app b name =
    3.18 -  declaration {syntax = false, pervasive = false} (fn phi => fn context =>
    3.19 -    let
    3.20 -      val naming = Name_Space.naming_of context;
    3.21 -      val b' = Morphism.binding phi b;
    3.22 -    in app (Name_Space.alias_table naming b' name) context end);
    3.23 -
    3.24  fun syntax_alias global_alias local_alias b name =
    3.25    declaration {syntax = true, pervasive = false} (fn phi =>
    3.26      let val b' = Morphism.binding phi b
     4.1 --- a/src/Pure/Isar/method.ML	Thu May 12 14:38:53 2016 +0200
     4.2 +++ b/src/Pure/Isar/method.ML	Thu May 12 22:06:18 2016 +0200
     4.3 @@ -333,6 +333,8 @@
     4.4  val get_methods = fst o Data.get;
     4.5  val map_methods = Data.map o apfst;
     4.6  
     4.7 +val ops_methods = {get_data = get_methods, put_data = map_methods o K};
     4.8 +
     4.9  
    4.10  (* ML tactic *)
    4.11  
    4.12 @@ -390,12 +392,6 @@
    4.13  
    4.14  (* method definitions *)
    4.15  
    4.16 -fun transfer_methods ctxt =
    4.17 -  let
    4.18 -    val meths0 = get_methods (Context.Theory (Proof_Context.theory_of ctxt));
    4.19 -    val meths' = Name_Space.merge_tables (meths0, get_methods (Context.Proof ctxt));
    4.20 -  in Context.proof_map (map_methods (K meths')) ctxt end;
    4.21 -
    4.22  fun print_methods verbose ctxt =
    4.23    let
    4.24      val meths = get_methods (Context.Proof ctxt);
    4.25 @@ -411,19 +407,11 @@
    4.26  
    4.27  (* define *)
    4.28  
    4.29 -fun define_global binding meth comment thy =
    4.30 -  let
    4.31 -    val context = Context.Theory thy;
    4.32 -    val (name, meths') =
    4.33 -      Name_Space.define context true (binding, (meth, comment)) (get_methods context);
    4.34 -  in (name, Context.the_theory (map_methods (K meths') context)) end;
    4.35 +fun define_global binding meth comment =
    4.36 +  Entity.define_global ops_methods binding (meth, comment);
    4.37  
    4.38  fun define binding meth comment =
    4.39 -  Local_Theory.background_theory_result (define_global binding meth comment)
    4.40 -  #-> (fn name =>
    4.41 -    Local_Theory.map_contexts (K transfer_methods)
    4.42 -    #> Local_Theory.generic_alias map_methods binding name
    4.43 -    #> pair name);
    4.44 +  Entity.define ops_methods binding (meth, comment);
    4.45  
    4.46  
    4.47  (* check *)
     5.1 --- a/src/Pure/ROOT.ML	Thu May 12 14:38:53 2016 +0200
     5.2 +++ b/src/Pure/ROOT.ML	Thu May 12 22:06:18 2016 +0200
     5.3 @@ -204,6 +204,7 @@
     5.4  
     5.5  (*theory specifications*)
     5.6  ML_file "Isar/local_theory.ML";
     5.7 +ML_file "Isar/entity.ML";
     5.8  ML_file "Thy/thy_header.ML";
     5.9  ML_file "PIDE/command_span.ML";
    5.10  ML_file "Thy/thy_syntax.ML";