src/Pure/sign.ML
changeset 47005 421760a1efe7
parent 45632 b23c42b9f78a
child 47006 5ee8004e2151
     1.1 --- a/src/Pure/sign.ML	Sun Mar 18 12:51:44 2012 +0100
     1.2 +++ b/src/Pure/sign.ML	Sun Mar 18 13:04:22 2012 +0100
     1.3 @@ -7,17 +7,6 @@
     1.4  
     1.5  signature SIGN =
     1.6  sig
     1.7 -  val rep_sg: theory ->
     1.8 -   {naming: Name_Space.naming,
     1.9 -    syn: Syntax.syntax,
    1.10 -    tsig: Type.tsig,
    1.11 -    consts: Consts.T}
    1.12 -  val map_naming: (Name_Space.naming -> Name_Space.naming) -> theory -> theory
    1.13 -  val naming_of: theory -> Name_Space.naming
    1.14 -  val full_name: theory -> binding -> string
    1.15 -  val full_name_path: theory -> string -> binding -> string
    1.16 -  val full_bname: theory -> bstring -> string
    1.17 -  val full_bname_path: theory -> string -> bstring -> string
    1.18    val syn_of: theory -> Syntax.syntax
    1.19    val tsig_of: theory -> Type.tsig
    1.20    val classes_of: theory -> Sorts.algebra
    1.21 @@ -42,6 +31,14 @@
    1.22    val the_const_type: theory -> string -> typ
    1.23    val declared_tyname: theory -> string -> bool
    1.24    val declared_const: theory -> string -> bool
    1.25 +  val naming_of: theory -> Name_Space.naming
    1.26 +  val map_naming: (Name_Space.naming -> Name_Space.naming) -> theory -> theory
    1.27 +  val restore_naming: theory -> theory -> theory
    1.28 +  val inherit_naming: theory -> Proof.context -> Context.generic
    1.29 +  val full_name: theory -> binding -> string
    1.30 +  val full_name_path: theory -> string -> binding -> string
    1.31 +  val full_bname: theory -> bstring -> string
    1.32 +  val full_bname_path: theory -> string -> bstring -> string
    1.33    val const_monomorphic: theory -> string -> bool
    1.34    val const_typargs: theory -> string * typ -> typ list
    1.35    val const_instance: theory -> string * typ list -> typ
    1.36 @@ -67,7 +64,7 @@
    1.37    val cert_prop: theory -> term -> term
    1.38    val no_frees: Proof.context -> term -> term
    1.39    val no_vars: Proof.context -> term -> term
    1.40 -  val add_types: Proof.context -> (binding * int * mixfix) list -> theory -> theory
    1.41 +  val add_type: Proof.context -> binding * int * mixfix -> theory -> theory
    1.42    val add_types_global: (binding * int * mixfix) list -> theory -> theory
    1.43    val add_nonterminals: Proof.context -> binding list -> theory -> theory
    1.44    val add_nonterminals_global: binding list -> theory -> theory
    1.45 @@ -113,7 +110,6 @@
    1.46    val mandatory_path: string -> theory -> theory
    1.47    val qualified_path: bool -> binding -> theory -> theory
    1.48    val local_path: theory -> theory
    1.49 -  val restore_naming: theory -> theory -> theory
    1.50    val hide_class: bool -> string -> theory -> theory
    1.51    val hide_type: bool -> string -> theory -> theory
    1.52    val hide_const: bool -> string -> theory -> theory
    1.53 @@ -125,56 +121,37 @@
    1.54  (** datatype sign **)
    1.55  
    1.56  datatype sign = Sign of
    1.57 - {naming: Name_Space.naming,    (*common naming conventions*)
    1.58 -  syn: Syntax.syntax,           (*concrete syntax for terms, types, sorts*)
    1.59 + {syn: Syntax.syntax,           (*concrete syntax for terms, types, sorts*)
    1.60    tsig: Type.tsig,              (*order-sorted signature of types*)
    1.61    consts: Consts.T};            (*polymorphic constants*)
    1.62  
    1.63 -fun make_sign (naming, syn, tsig, consts) =
    1.64 -  Sign {naming = naming, syn = syn, tsig = tsig, consts = consts};
    1.65 +fun make_sign (syn, tsig, consts) = Sign {syn = syn, tsig = tsig, consts = consts};
    1.66  
    1.67  structure Data = Theory_Data_PP
    1.68  (
    1.69    type T = sign;
    1.70 -  fun extend (Sign {syn, tsig, consts, ...}) =
    1.71 -    make_sign (Name_Space.default_naming, syn, tsig, consts);
    1.72 +  fun extend (Sign {syn, tsig, consts, ...}) = make_sign (syn, tsig, consts);
    1.73  
    1.74 -  val empty =
    1.75 -    make_sign (Name_Space.default_naming, Syntax.empty_syntax, Type.empty_tsig, Consts.empty);
    1.76 +  val empty = make_sign (Syntax.empty_syntax, Type.empty_tsig, Consts.empty);
    1.77  
    1.78    fun merge pp (sign1, sign2) =
    1.79      let
    1.80 -      val ctxt = Syntax.init_pretty pp;
    1.81 -      val Sign {naming = _, syn = syn1, tsig = tsig1, consts = consts1} = sign1;
    1.82 -      val Sign {naming = _, syn = syn2, tsig = tsig2, consts = consts2} = sign2;
    1.83 +      val Sign {syn = syn1, tsig = tsig1, consts = consts1} = sign1;
    1.84 +      val Sign {syn = syn2, tsig = tsig2, consts = consts2} = sign2;
    1.85  
    1.86 -      val naming = Name_Space.default_naming;
    1.87        val syn = Syntax.merge_syntax (syn1, syn2);
    1.88 -      val tsig = Type.merge_tsig ctxt (tsig1, tsig2);
    1.89 +      val tsig = Type.merge_tsig pp (tsig1, tsig2);
    1.90        val consts = Consts.merge (consts1, consts2);
    1.91 -    in make_sign (naming, syn, tsig, consts) end;
    1.92 +    in make_sign (syn, tsig, consts) end;
    1.93  );
    1.94  
    1.95  fun rep_sg thy = Data.get thy |> (fn Sign args => args);
    1.96  
    1.97 -fun map_sign f = Data.map (fn Sign {naming, syn, tsig, consts} =>
    1.98 -  make_sign (f (naming, syn, tsig, consts)));
    1.99 -
   1.100 -fun map_naming f = map_sign (fn (naming, syn, tsig, consts) => (f naming, syn, tsig, consts));
   1.101 -fun map_syn f = map_sign (fn (naming, syn, tsig, consts) => (naming, f syn, tsig, consts));
   1.102 -fun map_tsig f = map_sign (fn (naming, syn, tsig, consts) => (naming, syn, f tsig, consts));
   1.103 -fun map_consts f = map_sign (fn (naming, syn, tsig, consts) => (naming, syn, tsig, f consts));
   1.104 -
   1.105 +fun map_sign f = Data.map (fn Sign {syn, tsig, consts} => make_sign (f (syn, tsig, consts)));
   1.106  
   1.107 -(* naming *)
   1.108 -
   1.109 -val naming_of = #naming o rep_sg;
   1.110 -
   1.111 -val full_name = Name_Space.full_name o naming_of;
   1.112 -fun full_name_path thy path = Name_Space.full_name (Name_Space.add_path path (naming_of thy));
   1.113 -
   1.114 -fun full_bname thy = Name_Space.full_name (naming_of thy) o Binding.name;
   1.115 -fun full_bname_path thy path = full_name_path thy path o Binding.name;
   1.116 +fun map_syn f = map_sign (fn (syn, tsig, consts) => (f syn, tsig, consts));
   1.117 +fun map_tsig f = map_sign (fn (syn, tsig, consts) => (syn, f tsig, consts));
   1.118 +fun map_consts f = map_sign (fn (syn, tsig, consts) => (syn, tsig, f consts));
   1.119  
   1.120  
   1.121  (* syntax *)
   1.122 @@ -222,6 +199,21 @@
   1.123  val declared_const = can o the_const_constraint;
   1.124  
   1.125  
   1.126 +(* naming *)
   1.127 +
   1.128 +val naming_of = Name_Space.naming_of o Context.Theory;
   1.129 +val map_naming = Context.theory_map o Name_Space.map_naming;
   1.130 +val restore_naming = map_naming o K o naming_of;
   1.131 +fun inherit_naming thy =
   1.132 +  Context.Proof o Context.proof_map (Name_Space.map_naming (K (naming_of thy)));
   1.133 +
   1.134 +val full_name = Name_Space.full_name o naming_of;
   1.135 +fun full_name_path thy path = Name_Space.full_name (Name_Space.add_path path (naming_of thy));
   1.136 +
   1.137 +fun full_bname thy = Name_Space.full_name (naming_of thy) o Binding.name;
   1.138 +fun full_bname_path thy path = full_name_path thy path o Binding.name;
   1.139 +
   1.140 +
   1.141  
   1.142  (** name spaces **)
   1.143  
   1.144 @@ -330,22 +322,21 @@
   1.145  
   1.146  (* add type constructors *)
   1.147  
   1.148 -fun add_types ctxt types thy = thy |> map_sign (fn (naming, syn, tsig, consts) =>
   1.149 +fun add_type ctxt (b, n, mx) thy = thy |> map_sign (fn (syn, tsig, consts) =>
   1.150    let
   1.151 -    fun type_syntax (b, n, mx) =
   1.152 -      (Lexicon.mark_type (Name_Space.full_name naming b), Mixfix.make_type n, mx);
   1.153 -    val syn' = Syntax.update_type_gram true Syntax.mode_default (map type_syntax types) syn;
   1.154 -    val tsig' = fold (fn (a, n, _) => Type.add_type ctxt naming (a, n)) types tsig;
   1.155 -  in (naming, syn', tsig', consts) end);
   1.156 +    val type_syntax = (Lexicon.mark_type (full_name thy b), Mixfix.make_type n, mx);
   1.157 +    val syn' = Syntax.update_type_gram true Syntax.mode_default [type_syntax] syn;
   1.158 +    val tsig' = Type.add_type (inherit_naming thy ctxt) (b, n) tsig;
   1.159 +  in (syn', tsig', consts) end);
   1.160  
   1.161  fun add_types_global types thy =
   1.162 -  add_types (Syntax.init_pretty_global thy) types thy;
   1.163 +  fold (add_type (Syntax.init_pretty_global thy)) types thy;
   1.164  
   1.165  
   1.166  (* add nonterminals *)
   1.167  
   1.168 -fun add_nonterminals ctxt ns = map_sign (fn (naming, syn, tsig, consts) =>
   1.169 -  (naming, syn, fold (Type.add_nonterminal ctxt naming) ns tsig, consts));
   1.170 +fun add_nonterminals ctxt ns thy = thy |> map_sign (fn (syn, tsig, consts) =>
   1.171 +  (syn, fold (Type.add_nonterminal (inherit_naming thy ctxt)) ns tsig, consts));
   1.172  
   1.173  fun add_nonterminals_global ns thy =
   1.174    add_nonterminals (Syntax.init_pretty_global thy) ns thy;
   1.175 @@ -353,8 +344,8 @@
   1.176  
   1.177  (* add type abbreviations *)
   1.178  
   1.179 -fun add_type_abbrev ctxt abbr = map_sign (fn (naming, syn, tsig, consts) =>
   1.180 -  (naming, syn, Type.add_abbrev ctxt naming abbr tsig, consts));
   1.181 +fun add_type_abbrev ctxt abbr thy = thy |> map_sign (fn (syn, tsig, consts) =>
   1.182 +  (syn, Type.add_abbrev (inherit_naming thy ctxt) abbr tsig, consts));
   1.183  
   1.184  
   1.185  (* modify syntax *)
   1.186 @@ -409,7 +400,7 @@
   1.187      val args = map prep raw_args;
   1.188    in
   1.189      thy
   1.190 -    |> map_consts (fold (Consts.declare ctxt (naming_of thy) o #1) args)
   1.191 +    |> map_consts (fold (Consts.declare (inherit_naming thy ctxt) o #1) args)
   1.192      |> add_syntax_i (map #2 args)
   1.193      |> pair (map #3 args)
   1.194    end;
   1.195 @@ -437,7 +428,7 @@
   1.196      val t = (prep_tm raw_t handle TYPE (msg, _, _) => error msg | TERM (msg, _) => error msg)
   1.197        handle ERROR msg => cat_error msg ("in constant abbreviation " ^ Binding.print b);
   1.198      val (res, consts') = consts_of thy
   1.199 -      |> Consts.abbreviate ctxt (tsig_of thy) (naming_of thy) mode (b, t);
   1.200 +      |> Consts.abbreviate (inherit_naming thy ctxt) (tsig_of thy) mode (b, t);
   1.201    in (res, thy |> map_consts (K consts')) end;
   1.202  
   1.203  fun revert_abbrev mode c = map_consts (Consts.revert_abbrev mode c);
   1.204 @@ -458,18 +449,16 @@
   1.205  
   1.206  fun primitive_class (bclass, classes) thy =
   1.207    thy
   1.208 -  |> map_sign (fn (naming, syn, tsig, consts) =>
   1.209 -    let
   1.210 -      val ctxt = Syntax.init_pretty_global thy;
   1.211 -      val tsig' = Type.add_class ctxt naming (bclass, classes) tsig;
   1.212 -    in (naming, syn, tsig', consts) end)
   1.213 +  |> map_sign (fn (syn, tsig, consts) =>
   1.214 +      let val tsig' = Type.add_class (Context.Theory thy) (bclass, classes) tsig;
   1.215 +      in (syn, tsig', consts) end)
   1.216    |> add_consts_i [(Binding.map_name Logic.const_of_class bclass, Term.a_itselfT --> propT, NoSyn)];
   1.217  
   1.218  fun primitive_classrel arg thy =
   1.219 -  thy |> map_tsig (Type.add_classrel (Syntax.init_pretty_global thy) arg);
   1.220 +  thy |> map_tsig (Type.add_classrel (Context.pretty_global thy) arg);
   1.221  
   1.222  fun primitive_arity arg thy =
   1.223 -  thy |> map_tsig (Type.add_arity (Syntax.init_pretty_global thy) arg);
   1.224 +  thy |> map_tsig (Type.add_arity (Context.pretty_global thy) arg);
   1.225  
   1.226  
   1.227  (* add translation functions *)
   1.228 @@ -512,8 +501,6 @@
   1.229  
   1.230  fun local_path thy = thy |> root_path |> add_path (Context.theory_name thy);
   1.231  
   1.232 -val restore_naming = map_naming o K o naming_of;
   1.233 -
   1.234  
   1.235  (* hide names *)
   1.236