added ProofContext.tsig_of -- proforma version for local name space only, not logical content;
authorwenzelm
Tue Mar 09 14:35:02 2010 +0100 (2010-03-09)
changeset 35669a91c7ed801b8
parent 35668 69e1740fbfb1
child 35670 3007b46c1660
added ProofContext.tsig_of -- proforma version for local name space only, not logical content;
added ProofContext.read_type_name_proper;
localized ProofContext.read_class/read_arity/cert_arity;
localized ProofContext.class_space/type_space etc.;
src/Pure/Isar/class.ML
src/Pure/Isar/class_target.ML
src/Pure/Isar/proof_context.ML
src/Pure/ROOT.ML
src/Pure/axclass.ML
src/Pure/sign.ML
src/Pure/type.ML
     1.1 --- a/src/Pure/Isar/class.ML	Tue Mar 09 14:29:47 2010 +0100
     1.2 +++ b/src/Pure/Isar/class.ML	Tue Mar 09 14:35:02 2010 +0100
     1.3 @@ -338,7 +338,7 @@
     1.4  
     1.5  val subclass = gen_subclass (K I) user_proof;
     1.6  fun prove_subclass tac = gen_subclass (K I) (tactic_proof tac);
     1.7 -val subclass_cmd = gen_subclass Sign.read_class user_proof;
     1.8 +val subclass_cmd = gen_subclass (ProofContext.read_class o ProofContext.init) user_proof;
     1.9  
    1.10  end; (*local*)
    1.11  
     2.1 --- a/src/Pure/Isar/class_target.ML	Tue Mar 09 14:29:47 2010 +0100
     2.2 +++ b/src/Pure/Isar/class_target.ML	Tue Mar 09 14:35:02 2010 +0100
     2.3 @@ -417,7 +417,8 @@
     2.4  
     2.5  fun read_multi_arity thy (raw_tycos, raw_sorts, raw_sort) =
     2.6    let
     2.7 -    val all_arities = map (fn raw_tyco => Sign.read_arity thy
     2.8 +    val ctxt = ProofContext.init thy;
     2.9 +    val all_arities = map (fn raw_tyco => ProofContext.read_arity ctxt
    2.10        (raw_tyco, raw_sorts, raw_sort)) raw_tycos;
    2.11      val tycos = map #1 all_arities;
    2.12      val (_, sorts, sort) = hd all_arities;
     3.1 --- a/src/Pure/Isar/proof_context.ML	Tue Mar 09 14:29:47 2010 +0100
     3.2 +++ b/src/Pure/Isar/proof_context.ML	Tue Mar 09 14:35:02 2010 +0100
     3.3 @@ -27,6 +27,7 @@
     3.4    val restore_naming: Proof.context -> Proof.context -> Proof.context
     3.5    val full_name: Proof.context -> binding -> string
     3.6    val syn_of: Proof.context -> Syntax.syntax
     3.7 +  val tsig_of: Proof.context -> Type.tsig
     3.8    val consts_of: Proof.context -> Consts.T
     3.9    val the_const_constraint: Proof.context -> string -> typ
    3.10    val set_syntax_mode: Syntax.mode -> Proof.context -> Proof.context
    3.11 @@ -41,6 +42,9 @@
    3.12    val pretty_term_abbrev: Proof.context -> term -> Pretty.T
    3.13    val pretty_fact_aux: Proof.context -> bool -> string * thm list -> Pretty.T
    3.14    val pretty_fact: Proof.context -> string * thm list -> Pretty.T
    3.15 +  val read_class: Proof.context -> xstring -> class
    3.16 +  val read_arity: Proof.context -> xstring * string list * string -> arity
    3.17 +  val cert_arity: Proof.context -> arity -> arity
    3.18    val read_typ: Proof.context -> string -> typ
    3.19    val read_typ_syntax: Proof.context -> string -> typ
    3.20    val read_typ_abbrev: Proof.context -> string -> typ
    3.21 @@ -53,6 +57,7 @@
    3.22    val inferred_param: string -> Proof.context -> typ * Proof.context
    3.23    val inferred_fixes: Proof.context -> (string * typ) list * Proof.context
    3.24    val read_type_name: Proof.context -> bool -> string -> typ
    3.25 +  val read_type_name_proper: Proof.context -> bool -> string -> typ
    3.26    val read_const_proper: Proof.context -> bool -> string -> term
    3.27    val read_const: Proof.context -> bool -> string -> term
    3.28    val allow_dummies: Proof.context -> Proof.context
    3.29 @@ -167,16 +172,17 @@
    3.30  
    3.31  datatype ctxt =
    3.32    Ctxt of
    3.33 -   {mode: mode,                                       (*inner syntax mode*)
    3.34 -    naming: Name_Space.naming,                        (*local naming conventions*)
    3.35 -    syntax: Local_Syntax.T,                           (*local syntax*)
    3.36 -    consts: Consts.T * Consts.T,                      (*local/global consts*)
    3.37 -    facts: Facts.T,                                   (*local facts*)
    3.38 +   {mode: mode,                       (*inner syntax mode*)
    3.39 +    naming: Name_Space.naming,        (*local naming conventions*)
    3.40 +    syntax: Local_Syntax.T,           (*local syntax*)
    3.41 +    tsigs: Type.tsig * Type.tsig,     (*local/global type signature -- local name space only*)
    3.42 +    consts: Consts.T * Consts.T,      (*local/global consts -- local name space/abbrevs only*)
    3.43 +    facts: Facts.T,                   (*local facts*)
    3.44      cases: (string * (Rule_Cases.T * bool)) list};    (*named case contexts*)
    3.45  
    3.46 -fun make_ctxt (mode, naming, syntax, consts, facts, cases) =
    3.47 +fun make_ctxt (mode, naming, syntax, tsigs, consts, facts, cases) =
    3.48    Ctxt {mode = mode, naming = naming, syntax = syntax,
    3.49 -    consts = consts, facts = facts, cases = cases};
    3.50 +    tsigs = tsigs, consts = consts, facts = facts, cases = cases};
    3.51  
    3.52  val local_naming = Name_Space.default_naming |> Name_Space.add_path "local";
    3.53  
    3.54 @@ -185,41 +191,46 @@
    3.55    type T = ctxt;
    3.56    fun init thy =
    3.57      make_ctxt (mode_default, local_naming, Local_Syntax.init thy,
    3.58 +      (Sign.tsig_of thy, Sign.tsig_of thy),
    3.59        (Sign.consts_of thy, Sign.consts_of thy), Facts.empty, []);
    3.60  );
    3.61  
    3.62  fun rep_context ctxt = ContextData.get ctxt |> (fn Ctxt args => args);
    3.63  
    3.64  fun map_context f =
    3.65 -  ContextData.map (fn Ctxt {mode, naming, syntax, consts, facts, cases} =>
    3.66 -    make_ctxt (f (mode, naming, syntax, consts, facts, cases)));
    3.67 +  ContextData.map (fn Ctxt {mode, naming, syntax, tsigs, consts, facts, cases} =>
    3.68 +    make_ctxt (f (mode, naming, syntax, tsigs, consts, facts, cases)));
    3.69  
    3.70 -fun set_mode mode = map_context (fn (_, naming, syntax, consts, facts, cases) =>
    3.71 -  (mode, naming, syntax, consts, facts, cases));
    3.72 +fun set_mode mode = map_context (fn (_, naming, syntax, tsigs, consts, facts, cases) =>
    3.73 +  (mode, naming, syntax, tsigs, consts, facts, cases));
    3.74  
    3.75  fun map_mode f =
    3.76 -  map_context (fn (Mode {stmt, pattern, schematic, abbrev}, naming, syntax, consts, facts, cases) =>
    3.77 -    (make_mode (f (stmt, pattern, schematic, abbrev)), naming, syntax, consts, facts, cases));
    3.78 +  map_context (fn (Mode {stmt, pattern, schematic, abbrev}, naming, syntax, tsigs, consts, facts, cases) =>
    3.79 +    (make_mode (f (stmt, pattern, schematic, abbrev)), naming, syntax, tsigs, consts, facts, cases));
    3.80  
    3.81  fun map_naming f =
    3.82 -  map_context (fn (mode, naming, syntax, consts, facts, cases) =>
    3.83 -    (mode, f naming, syntax, consts, facts, cases));
    3.84 +  map_context (fn (mode, naming, syntax, tsigs, consts, facts, cases) =>
    3.85 +    (mode, f naming, syntax, tsigs, consts, facts, cases));
    3.86  
    3.87  fun map_syntax f =
    3.88 -  map_context (fn (mode, naming, syntax, consts, facts, cases) =>
    3.89 -    (mode, naming, f syntax, consts, facts, cases));
    3.90 +  map_context (fn (mode, naming, syntax, tsigs, consts, facts, cases) =>
    3.91 +    (mode, naming, f syntax, tsigs, consts, facts, cases));
    3.92 +
    3.93 +fun map_tsigs f =
    3.94 +  map_context (fn (mode, naming, syntax, tsigs, consts, facts, cases) =>
    3.95 +    (mode, naming, syntax, f tsigs, consts, facts, cases));
    3.96  
    3.97  fun map_consts f =
    3.98 -  map_context (fn (mode, naming, syntax, consts, facts, cases) =>
    3.99 -    (mode, naming, syntax, f consts, facts, cases));
   3.100 +  map_context (fn (mode, naming, syntax, tsigs, consts, facts, cases) =>
   3.101 +    (mode, naming, syntax, tsigs, f consts, facts, cases));
   3.102  
   3.103  fun map_facts f =
   3.104 -  map_context (fn (mode, naming, syntax, consts, facts, cases) =>
   3.105 -    (mode, naming, syntax, consts, f facts, cases));
   3.106 +  map_context (fn (mode, naming, syntax, tsigs, consts, facts, cases) =>
   3.107 +    (mode, naming, syntax, tsigs, consts, f facts, cases));
   3.108  
   3.109  fun map_cases f =
   3.110 -  map_context (fn (mode, naming, syntax, consts, facts, cases) =>
   3.111 -    (mode, naming, syntax, consts, facts, f cases));
   3.112 +  map_context (fn (mode, naming, syntax, tsigs, consts, facts, cases) =>
   3.113 +    (mode, naming, syntax, tsigs, consts, facts, f cases));
   3.114  
   3.115  val get_mode = #mode o rep_context;
   3.116  val restore_mode = set_mode o get_mode;
   3.117 @@ -237,6 +248,8 @@
   3.118  val set_syntax_mode = map_syntax o Local_Syntax.set_mode;
   3.119  val restore_syntax_mode = map_syntax o Local_Syntax.restore_mode o syntax_of;
   3.120  
   3.121 +val tsig_of = #1 o #tsigs o rep_context;
   3.122 +
   3.123  val consts_of = #1 o #consts o rep_context;
   3.124  val the_const_constraint = Consts.the_constraint o consts_of;
   3.125  
   3.126 @@ -246,8 +259,13 @@
   3.127  
   3.128  (* theory transfer *)
   3.129  
   3.130 -fun transfer_syntax thy =
   3.131 -  map_syntax (Local_Syntax.rebuild thy) #>
   3.132 +fun transfer_syntax thy ctxt = ctxt |>
   3.133 +  map_syntax (Local_Syntax.rebuild thy) |>
   3.134 +  map_tsigs (fn tsigs as (local_tsig, global_tsig) =>
   3.135 +    let val thy_tsig = Sign.tsig_of thy in
   3.136 +      if Type.eq_tsig (thy_tsig, global_tsig) then tsigs
   3.137 +      else (Type.merge_tsigs (Syntax.pp ctxt) (local_tsig, thy_tsig), thy_tsig)
   3.138 +    end) |>
   3.139    map_consts (fn consts as (local_consts, global_consts) =>
   3.140      let val thy_consts = Sign.consts_of thy in
   3.141        if Consts.eq_consts (thy_consts, global_consts) then consts
   3.142 @@ -299,23 +317,49 @@
   3.143  
   3.144  (** prepare types **)
   3.145  
   3.146 -(* read_typ *)
   3.147 +(* classes *)
   3.148 +
   3.149 +fun read_class ctxt text =
   3.150 +  let
   3.151 +    val tsig = tsig_of ctxt;
   3.152 +    val (syms, pos) = Syntax.read_token text;
   3.153 +    val c = Type.cert_class tsig (Type.intern_class tsig (Symbol_Pos.content syms))
   3.154 +      handle TYPE (msg, _, _) => error (msg ^ Position.str_of pos);
   3.155 +    val _ = Position.report (Markup.tclass c) pos;
   3.156 +  in c end;
   3.157 +
   3.158 +
   3.159 +(* type arities *)
   3.160 +
   3.161 +local
   3.162 +
   3.163 +fun prep_arity prep_tycon prep_sort ctxt (t, Ss, S) =
   3.164 +  let val arity = (prep_tycon ctxt t, map (prep_sort ctxt) Ss, prep_sort ctxt S)
   3.165 +  in Type.add_arity (Syntax.pp ctxt) arity (tsig_of ctxt); arity end;
   3.166 +
   3.167 +in
   3.168 +
   3.169 +val read_arity = prep_arity (Type.intern_type o tsig_of) Syntax.read_sort;
   3.170 +val cert_arity = prep_arity (K I) (Type.cert_sort o tsig_of);
   3.171 +
   3.172 +end;
   3.173 +
   3.174 +
   3.175 +(* types *)
   3.176  
   3.177  fun read_typ_mode mode ctxt s =
   3.178    Syntax.read_typ (Type.set_mode mode ctxt) s;
   3.179  
   3.180 -val read_typ        = read_typ_mode Type.mode_default;
   3.181 +val read_typ = read_typ_mode Type.mode_default;
   3.182  val read_typ_syntax = read_typ_mode Type.mode_syntax;
   3.183  val read_typ_abbrev = read_typ_mode Type.mode_abbrev;
   3.184  
   3.185  
   3.186 -(* cert_typ *)
   3.187 -
   3.188  fun cert_typ_mode mode ctxt T =
   3.189 -  Sign.certify_typ_mode mode (theory_of ctxt) T
   3.190 +  Type.cert_typ_mode mode (tsig_of ctxt) T
   3.191      handle TYPE (msg, _, _) => error msg;
   3.192  
   3.193 -val cert_typ        = cert_typ_mode Type.mode_default;
   3.194 +val cert_typ = cert_typ_mode Type.mode_default;
   3.195  val cert_typ_syntax = cert_typ_mode Type.mode_syntax;
   3.196  val cert_typ_abbrev = cert_typ_mode Type.mode_abbrev;
   3.197  
   3.198 @@ -424,16 +468,16 @@
   3.199  
   3.200  fun read_type_name ctxt strict text =
   3.201    let
   3.202 -    val thy = theory_of ctxt;
   3.203 +    val tsig = tsig_of ctxt;
   3.204      val (c, pos) = token_content text;
   3.205    in
   3.206      if Syntax.is_tid c then
   3.207       (Position.report Markup.tfree pos;
   3.208 -      TFree (c, the_default (Sign.defaultS thy) (Variable.def_sort ctxt (c, ~1))))
   3.209 +      TFree (c, the_default (Type.defaultS tsig) (Variable.def_sort ctxt (c, ~1))))
   3.210      else
   3.211        let
   3.212 -        val d = Sign.intern_type thy c;
   3.213 -        val decl = Sign.the_type_decl thy d;
   3.214 +        val d = Type.intern_type tsig c;
   3.215 +        val decl = Type.the_decl tsig d;
   3.216          val _ = Position.report (Markup.tycon d) pos;
   3.217          fun err () = error ("Bad type name: " ^ quote d);
   3.218          val args =
   3.219 @@ -444,6 +488,12 @@
   3.220        in Type (d, replicate args dummyT) end
   3.221    end;
   3.222  
   3.223 +fun read_type_name_proper ctxt strict text =
   3.224 +  (case read_type_name ctxt strict text of
   3.225 +    T as Type _ => T
   3.226 +  | T => error ("Not a type constructor: " ^ Syntax.string_of_typ ctxt T));
   3.227 +
   3.228 +
   3.229  fun read_const_proper ctxt strict = prep_const_proper ctxt strict o token_content;
   3.230  
   3.231  fun read_const ctxt strict text =
   3.232 @@ -470,8 +520,6 @@
   3.233  
   3.234  (* local abbreviations *)
   3.235  
   3.236 -val tsig_of = Sign.tsig_of o ProofContext.theory_of;
   3.237 -
   3.238  local
   3.239  
   3.240  fun certify_consts ctxt = Consts.certify (Syntax.pp ctxt) (tsig_of ctxt)
   3.241 @@ -553,9 +601,9 @@
   3.242  
   3.243  (* types *)
   3.244  
   3.245 -fun get_sort thy def_sort raw_env =
   3.246 +fun get_sort ctxt def_sort raw_env =
   3.247    let
   3.248 -    val tsig = Sign.tsig_of thy;
   3.249 +    val tsig = tsig_of ctxt;
   3.250  
   3.251      fun eq ((xi, S), (xi', S')) =
   3.252        Term.eq_ix (xi, xi') andalso Type.eq_sort tsig (S, S');
   3.253 @@ -571,8 +619,8 @@
   3.254        | (SOME S, NONE) => S
   3.255        | (SOME S, SOME S') =>
   3.256            if Type.eq_sort tsig (S, S') then S'
   3.257 -          else error ("Sort constraint " ^ Syntax.string_of_sort_global thy S ^
   3.258 -            " inconsistent with default " ^ Syntax.string_of_sort_global thy S' ^
   3.259 +          else error ("Sort constraint " ^ Syntax.string_of_sort ctxt S ^
   3.260 +            " inconsistent with default " ^ Syntax.string_of_sort ctxt S' ^
   3.261              " for type variable " ^ quote (Term.string_of_vname' xi)));
   3.262    in get end;
   3.263  
   3.264 @@ -594,12 +642,10 @@
   3.265  in
   3.266  
   3.267  fun term_context ctxt =
   3.268 -  let val thy = theory_of ctxt in
   3.269 -   {get_sort = get_sort thy (Variable.def_sort ctxt),
   3.270 -    map_const = fn a => ((true, #1 (Term.dest_Const (read_const_proper ctxt false a)))
   3.271 -      handle ERROR _ => (false, Consts.intern (consts_of ctxt) a)),
   3.272 -    map_free = intern_skolem ctxt (Variable.def_type ctxt false)}
   3.273 -  end;
   3.274 +  {get_sort = get_sort ctxt (Variable.def_sort ctxt),
   3.275 +   map_const = fn a => ((true, #1 (Term.dest_Const (read_const_proper ctxt false a)))
   3.276 +     handle ERROR _ => (false, Consts.intern (consts_of ctxt) a)),
   3.277 +   map_free = intern_skolem ctxt (Variable.def_type ctxt false)};
   3.278  
   3.279  fun decode_term ctxt =
   3.280    let val {get_sort, map_const, map_free} = term_context ctxt
   3.281 @@ -680,8 +726,7 @@
   3.282  
   3.283  fun parse_typ ctxt text =
   3.284    let
   3.285 -    val thy = theory_of ctxt;
   3.286 -    val get_sort = get_sort thy (Variable.def_sort ctxt);
   3.287 +    val get_sort = get_sort ctxt (Variable.def_sort ctxt);
   3.288      val (syms, pos) = Syntax.parse_token Markup.typ text;
   3.289      val T = Syntax.standard_parse_typ ctxt (syn_of ctxt) get_sort (syms, pos)
   3.290        handle ERROR msg => cat_error msg ("Failed to parse type" ^ Position.str_of pos);
   3.291 @@ -689,7 +734,6 @@
   3.292  
   3.293  fun parse_term T ctxt text =
   3.294    let
   3.295 -    val thy = theory_of ctxt;
   3.296      val {get_sort, map_const, map_free} = term_context ctxt;
   3.297  
   3.298      val (T', _) = TypeInfer.paramify_dummies T 0;
   3.299 @@ -700,33 +744,33 @@
   3.300        handle ERROR msg => SOME msg;
   3.301      val t =
   3.302        Syntax.standard_parse_term (Syntax.pp ctxt) check get_sort map_const map_free
   3.303 -        ctxt (Sign.is_logtype thy) (syn_of ctxt) T' (syms, pos)
   3.304 +        ctxt (Type.is_logtype (tsig_of ctxt)) (syn_of ctxt) T' (syms, pos)
   3.305        handle ERROR msg => cat_error msg  ("Failed to parse " ^ kind ^ Position.str_of pos);
   3.306    in t end;
   3.307  
   3.308  
   3.309  fun unparse_sort ctxt =
   3.310 -  Syntax.standard_unparse_sort {extern_class = Sign.extern_class (theory_of ctxt)}
   3.311 +  Syntax.standard_unparse_sort {extern_class = Type.extern_class (tsig_of ctxt)}
   3.312      ctxt (syn_of ctxt);
   3.313  
   3.314  fun unparse_typ ctxt =
   3.315    let
   3.316 -    val thy = theory_of ctxt;
   3.317 -    val extern = {extern_class = Sign.extern_class thy, extern_type = Sign.extern_type thy};
   3.318 +    val tsig = tsig_of ctxt;
   3.319 +    val extern = {extern_class = Type.extern_class tsig, extern_type = Type.extern_type tsig};
   3.320    in Syntax.standard_unparse_typ extern ctxt (syn_of ctxt) end;
   3.321  
   3.322  fun unparse_term ctxt =
   3.323    let
   3.324 -    val thy = theory_of ctxt;
   3.325 +    val tsig = tsig_of ctxt;
   3.326      val syntax = syntax_of ctxt;
   3.327      val consts = consts_of ctxt;
   3.328      val extern =
   3.329 -     {extern_class = Sign.extern_class thy,
   3.330 -      extern_type = Sign.extern_type thy,
   3.331 +     {extern_class = Type.extern_class tsig,
   3.332 +      extern_type = Type.extern_type tsig,
   3.333        extern_const = Consts.extern consts};
   3.334    in
   3.335      Syntax.standard_unparse_term (Local_Syntax.idents_of syntax) extern ctxt
   3.336 -      (Local_Syntax.syn_of syntax) (not (PureThy.old_appl_syntax thy))
   3.337 +      (Local_Syntax.syn_of syntax) (not (PureThy.old_appl_syntax (theory_of ctxt)))
   3.338    end;
   3.339  
   3.340  in
   3.341 @@ -999,7 +1043,14 @@
   3.342  end;
   3.343  
   3.344  
   3.345 -(* authentic constants *)
   3.346 +(* authentic logical entities *)
   3.347 +
   3.348 +val _ = Context.>>
   3.349 +  (Context.map_theory
   3.350 +    (Sign.add_advanced_trfuns
   3.351 +      (Syntax.type_ast_trs
   3.352 +        {read_class = read_class,
   3.353 +          read_type = fn ctxt => #1 o dest_Type o read_type_name_proper ctxt false}, [], [], [])));
   3.354  
   3.355  local
   3.356  
     4.1 --- a/src/Pure/ROOT.ML	Tue Mar 09 14:29:47 2010 +0100
     4.2 +++ b/src/Pure/ROOT.ML	Tue Mar 09 14:35:02 2010 +0100
     4.3 @@ -148,7 +148,6 @@
     4.4  use "assumption.ML";
     4.5  use "display.ML";
     4.6  use "goal.ML";
     4.7 -use "axclass.ML";
     4.8  
     4.9  
    4.10  (* Isar -- Intelligible Semi-Automated Reasoning *)
    4.11 @@ -209,6 +208,7 @@
    4.12  use "Isar/local_theory.ML";
    4.13  use "Isar/overloading.ML";
    4.14  use "Isar/locale.ML";
    4.15 +use "axclass.ML";
    4.16  use "Isar/class_target.ML";
    4.17  use "Isar/theory_target.ML";
    4.18  use "Isar/expression.ML";
     5.1 --- a/src/Pure/axclass.ML	Tue Mar 09 14:29:47 2010 +0100
     5.2 +++ b/src/Pure/axclass.ML	Tue Mar 09 14:35:02 2010 +0100
     5.3 @@ -280,7 +280,7 @@
     5.4    in (c1, c2) end;
     5.5  
     5.6  fun read_classrel thy raw_rel =
     5.7 -  cert_classrel thy (pairself (Sign.read_class thy) raw_rel)
     5.8 +  cert_classrel thy (pairself (ProofContext.read_class (ProofContext.init thy)) raw_rel)
     5.9      handle TYPE (msg, _, _) => error msg;
    5.10  
    5.11  
    5.12 @@ -387,7 +387,7 @@
    5.13  fun prove_arity raw_arity tac thy =
    5.14    let
    5.15      val ctxt = ProofContext.init thy;
    5.16 -    val arity = Sign.cert_arity thy raw_arity;
    5.17 +    val arity = ProofContext.cert_arity ctxt raw_arity;
    5.18      val names = map (prefix arity_prefix) (Logic.name_arities arity);
    5.19      val props = Logic.mk_arities arity;
    5.20      val ths = Goal.prove_multi ctxt [] [] props
    5.21 @@ -530,7 +530,7 @@
    5.22      (map (prefix classrel_prefix o Logic.name_classrel)) add_classrel;
    5.23  
    5.24  fun ax_arity prep =
    5.25 -  axiomatize prep Logic.mk_arities
    5.26 +  axiomatize (prep o ProofContext.init) Logic.mk_arities
    5.27      (map (prefix arity_prefix) o Logic.name_arities) add_arity;
    5.28  
    5.29  fun class_const c =
    5.30 @@ -550,11 +550,11 @@
    5.31  in
    5.32  
    5.33  val axiomatize_class = ax_class Sign.certify_class cert_classrel;
    5.34 -val axiomatize_class_cmd = ax_class Sign.read_class read_classrel;
    5.35 +val axiomatize_class_cmd = ax_class (ProofContext.read_class o ProofContext.init) read_classrel;
    5.36  val axiomatize_classrel = ax_classrel cert_classrel;
    5.37  val axiomatize_classrel_cmd = ax_classrel read_classrel;
    5.38 -val axiomatize_arity = ax_arity Sign.cert_arity;
    5.39 -val axiomatize_arity_cmd = ax_arity Sign.read_arity;
    5.40 +val axiomatize_arity = ax_arity ProofContext.cert_arity;
    5.41 +val axiomatize_arity_cmd = ax_arity ProofContext.read_arity;
    5.42  
    5.43  end;
    5.44  
     6.1 --- a/src/Pure/sign.ML	Tue Mar 09 14:29:47 2010 +0100
     6.2 +++ b/src/Pure/sign.ML	Tue Mar 09 14:35:02 2010 +0100
     6.3 @@ -53,11 +53,7 @@
     6.4    val extern_type: theory -> string -> xstring
     6.5    val intern_const: theory -> xstring -> string
     6.6    val extern_const: theory -> string -> xstring
     6.7 -  val intern_sort: theory -> sort -> sort
     6.8 -  val extern_sort: theory -> sort -> sort
     6.9 -  val intern_typ: theory -> typ -> typ
    6.10    val intern_term: theory -> term -> term
    6.11 -  val the_type_decl: theory -> string -> Type.decl
    6.12    val arity_number: theory -> string -> int
    6.13    val arity_sorts: theory -> string -> sort -> sort list
    6.14    val certify_class: theory -> class -> class
    6.15 @@ -71,9 +67,6 @@
    6.16    val no_frees: Pretty.pp -> term -> term
    6.17    val no_vars: Pretty.pp -> term -> term
    6.18    val cert_def: Proof.context -> term -> (string * typ) * term
    6.19 -  val read_class: theory -> xstring -> class
    6.20 -  val read_arity: theory -> xstring * string list * string -> arity
    6.21 -  val cert_arity: theory -> arity -> arity
    6.22    val add_defsort: string -> theory -> theory
    6.23    val add_defsort_i: sort -> theory -> theory
    6.24    val add_types: (binding * int * mixfix) list -> theory -> theory
    6.25 @@ -154,7 +147,7 @@
    6.26      make_sign (Name_Space.default_naming, syn, tsig, consts);
    6.27  
    6.28    val empty =
    6.29 -    make_sign (Name_Space.default_naming, Syntax.empty_syntax, Type.empty_tsig, Consts.empty);
    6.30 +    make_sign (Name_Space.default_naming, Syntax.basic_syntax, Type.empty_tsig, Consts.empty);
    6.31  
    6.32    fun merge pp (sign1, sign2) =
    6.33      let
    6.34 @@ -236,8 +229,8 @@
    6.35  
    6.36  (** intern / extern names **)
    6.37  
    6.38 -val class_space = #1 o #classes o Type.rep_tsig o tsig_of;
    6.39 -val type_space = #1 o #types o Type.rep_tsig o tsig_of;
    6.40 +val class_space = Type.class_space o tsig_of;
    6.41 +val type_space = Type.type_space o tsig_of;
    6.42  val const_space = Consts.space_of o consts_of;
    6.43  
    6.44  val intern_class = Name_Space.intern o class_space;
    6.45 @@ -247,9 +240,6 @@
    6.46  val intern_const = Name_Space.intern o const_space;
    6.47  val extern_const = Name_Space.extern o const_space;
    6.48  
    6.49 -val intern_sort = map o intern_class;
    6.50 -val extern_sort = map o extern_class;
    6.51 -
    6.52  local
    6.53  
    6.54  fun map_typ f g (Type (c, Ts)) = Type (g c, map (map_typ f g) Ts)
    6.55 @@ -265,7 +255,6 @@
    6.56  
    6.57  in
    6.58  
    6.59 -fun intern_typ thy = map_typ (intern_class thy) (intern_type thy);
    6.60  fun intern_term thy = map_term (intern_class thy) (intern_type thy) (intern_const thy);
    6.61  
    6.62  end;
    6.63 @@ -276,7 +265,6 @@
    6.64  
    6.65  (* certify wrt. type signature *)
    6.66  
    6.67 -val the_type_decl = Type.the_decl o tsig_of;
    6.68  val arity_number = Type.arity_number o tsig_of;
    6.69  fun arity_sorts thy = Type.arity_sorts (Syntax.pp_global thy) (tsig_of thy);
    6.70  
    6.71 @@ -367,51 +355,6 @@
    6.72  
    6.73  
    6.74  
    6.75 -(** read and certify entities **)    (*exception ERROR*)
    6.76 -
    6.77 -(* classes *)
    6.78 -
    6.79 -fun read_class thy text =
    6.80 -  let
    6.81 -    val (syms, pos) = Syntax.read_token text;
    6.82 -    val c = certify_class thy (intern_class thy (Symbol_Pos.content syms))
    6.83 -      handle TYPE (msg, _, _) => error (msg ^ Position.str_of pos);
    6.84 -    val _ = Position.report (Markup.tclass c) pos;
    6.85 -  in c end;
    6.86 -
    6.87 -
    6.88 -(* type arities *)
    6.89 -
    6.90 -fun prep_arity prep_tycon prep_sort thy (t, Ss, S) =
    6.91 -  let val arity = (prep_tycon thy t, map (prep_sort thy) Ss, prep_sort thy S)
    6.92 -  in Type.add_arity (Syntax.pp_global thy) arity (tsig_of thy); arity end;
    6.93 -
    6.94 -val read_arity = prep_arity intern_type Syntax.read_sort_global;
    6.95 -val cert_arity = prep_arity (K I) certify_sort;
    6.96 -
    6.97 -
    6.98 -(* type syntax entities *)
    6.99 -
   6.100 -local
   6.101 -
   6.102 -fun read_type thy text =
   6.103 -  let
   6.104 -    val (syms, pos) = Syntax.read_token text;
   6.105 -    val c = intern_type thy (Symbol_Pos.content syms);
   6.106 -    val _ = the_type_decl thy c;
   6.107 -    val _ = Position.report (Markup.tycon c) pos;
   6.108 -  in c end;
   6.109 -
   6.110 -in
   6.111 -
   6.112 -val _ = Context.>>
   6.113 -  (Context.map_theory
   6.114 -    (map_syn (K (Syntax.basic_syntax {read_class = read_class, read_type = read_type}))));
   6.115 -
   6.116 -end;
   6.117 -
   6.118 -
   6.119 -
   6.120  (** signature extension functions **)  (*exception ERROR/TYPE*)
   6.121  
   6.122  (* add default sort *)
     7.1 --- a/src/Pure/type.ML	Tue Mar 09 14:29:47 2010 +0100
     7.2 +++ b/src/Pure/type.ML	Tue Mar 09 14:35:02 2010 +0100
     7.3 @@ -13,12 +13,16 @@
     7.4      Abbreviation of string list * typ * bool |
     7.5      Nonterminal
     7.6    type tsig
     7.7 +  val eq_tsig: tsig * tsig -> bool
     7.8    val rep_tsig: tsig ->
     7.9     {classes: Name_Space.T * Sorts.algebra,
    7.10      default: sort,
    7.11      types: decl Name_Space.table,
    7.12      log_types: string list}
    7.13    val empty_tsig: tsig
    7.14 +  val class_space: tsig -> Name_Space.T
    7.15 +  val intern_class: tsig -> xstring -> string
    7.16 +  val extern_class: tsig -> string -> xstring
    7.17    val defaultS: tsig -> sort
    7.18    val logical_types: tsig -> string list
    7.19    val eq_sort: tsig -> sort * sort -> bool
    7.20 @@ -35,6 +39,10 @@
    7.21    val get_mode: Proof.context -> mode
    7.22    val set_mode: mode -> Proof.context -> Proof.context
    7.23    val restore_mode: Proof.context -> Proof.context -> Proof.context
    7.24 +  val type_space: tsig -> Name_Space.T
    7.25 +  val intern_type: tsig -> xstring -> string
    7.26 +  val extern_type: tsig -> string -> xstring
    7.27 +  val is_logtype: tsig -> string -> bool
    7.28    val the_decl: tsig -> string -> decl
    7.29    val cert_typ_mode: mode -> tsig -> typ -> typ
    7.30    val cert_typ: tsig -> typ -> typ
    7.31 @@ -103,6 +111,13 @@
    7.32      types: decl Name_Space.table,           (*declared types*)
    7.33      log_types: string list};                (*logical types sorted by number of arguments*)
    7.34  
    7.35 +fun eq_tsig
    7.36 +   (TSig {classes = classes1, default = default1, types = types1, log_types = _},
    7.37 +    TSig {classes = classes2, default = default2, types = types2, log_types = _}) =
    7.38 +  pointer_eq (classes1, classes2) andalso
    7.39 +  default1 = default2 andalso
    7.40 +  pointer_eq (types1, types2);
    7.41 +
    7.42  fun rep_tsig (TSig comps) = comps;
    7.43  
    7.44  fun make_tsig (classes, default, types, log_types) =
    7.45 @@ -124,6 +139,11 @@
    7.46  
    7.47  (* classes and sorts *)
    7.48  
    7.49 +val class_space = #1 o #classes o rep_tsig;
    7.50 +
    7.51 +val intern_class = Name_Space.intern o class_space;
    7.52 +val extern_class = Name_Space.extern o class_space;
    7.53 +
    7.54  fun defaultS (TSig {default, ...}) = default;
    7.55  fun logical_types (TSig {log_types, ...}) = log_types;
    7.56  
    7.57 @@ -158,7 +178,15 @@
    7.58  fun restore_mode ctxt = set_mode (get_mode ctxt);
    7.59  
    7.60  
    7.61 -(* lookup types *)
    7.62 +(* types *)
    7.63 +
    7.64 +val type_space = #1 o #types o rep_tsig;
    7.65 +
    7.66 +val intern_type = Name_Space.intern o type_space;
    7.67 +val extern_type = Name_Space.extern o type_space;
    7.68 +
    7.69 +val is_logtype = member (op =) o logical_types;
    7.70 +
    7.71  
    7.72  fun undecl_type c = "Undeclared type constructor: " ^ quote c;
    7.73