src/Pure/sign.ML
changeset 35669 a91c7ed801b8
parent 35429 afa8cf9e63d8
child 35680 897740382442
     1.1 --- a/src/Pure/sign.ML	Tue Mar 09 14:29:47 2010 +0100
     1.2 +++ b/src/Pure/sign.ML	Tue Mar 09 14:35:02 2010 +0100
     1.3 @@ -53,11 +53,7 @@
     1.4    val extern_type: theory -> string -> xstring
     1.5    val intern_const: theory -> xstring -> string
     1.6    val extern_const: theory -> string -> xstring
     1.7 -  val intern_sort: theory -> sort -> sort
     1.8 -  val extern_sort: theory -> sort -> sort
     1.9 -  val intern_typ: theory -> typ -> typ
    1.10    val intern_term: theory -> term -> term
    1.11 -  val the_type_decl: theory -> string -> Type.decl
    1.12    val arity_number: theory -> string -> int
    1.13    val arity_sorts: theory -> string -> sort -> sort list
    1.14    val certify_class: theory -> class -> class
    1.15 @@ -71,9 +67,6 @@
    1.16    val no_frees: Pretty.pp -> term -> term
    1.17    val no_vars: Pretty.pp -> term -> term
    1.18    val cert_def: Proof.context -> term -> (string * typ) * term
    1.19 -  val read_class: theory -> xstring -> class
    1.20 -  val read_arity: theory -> xstring * string list * string -> arity
    1.21 -  val cert_arity: theory -> arity -> arity
    1.22    val add_defsort: string -> theory -> theory
    1.23    val add_defsort_i: sort -> theory -> theory
    1.24    val add_types: (binding * int * mixfix) list -> theory -> theory
    1.25 @@ -154,7 +147,7 @@
    1.26      make_sign (Name_Space.default_naming, syn, tsig, consts);
    1.27  
    1.28    val empty =
    1.29 -    make_sign (Name_Space.default_naming, Syntax.empty_syntax, Type.empty_tsig, Consts.empty);
    1.30 +    make_sign (Name_Space.default_naming, Syntax.basic_syntax, Type.empty_tsig, Consts.empty);
    1.31  
    1.32    fun merge pp (sign1, sign2) =
    1.33      let
    1.34 @@ -236,8 +229,8 @@
    1.35  
    1.36  (** intern / extern names **)
    1.37  
    1.38 -val class_space = #1 o #classes o Type.rep_tsig o tsig_of;
    1.39 -val type_space = #1 o #types o Type.rep_tsig o tsig_of;
    1.40 +val class_space = Type.class_space o tsig_of;
    1.41 +val type_space = Type.type_space o tsig_of;
    1.42  val const_space = Consts.space_of o consts_of;
    1.43  
    1.44  val intern_class = Name_Space.intern o class_space;
    1.45 @@ -247,9 +240,6 @@
    1.46  val intern_const = Name_Space.intern o const_space;
    1.47  val extern_const = Name_Space.extern o const_space;
    1.48  
    1.49 -val intern_sort = map o intern_class;
    1.50 -val extern_sort = map o extern_class;
    1.51 -
    1.52  local
    1.53  
    1.54  fun map_typ f g (Type (c, Ts)) = Type (g c, map (map_typ f g) Ts)
    1.55 @@ -265,7 +255,6 @@
    1.56  
    1.57  in
    1.58  
    1.59 -fun intern_typ thy = map_typ (intern_class thy) (intern_type thy);
    1.60  fun intern_term thy = map_term (intern_class thy) (intern_type thy) (intern_const thy);
    1.61  
    1.62  end;
    1.63 @@ -276,7 +265,6 @@
    1.64  
    1.65  (* certify wrt. type signature *)
    1.66  
    1.67 -val the_type_decl = Type.the_decl o tsig_of;
    1.68  val arity_number = Type.arity_number o tsig_of;
    1.69  fun arity_sorts thy = Type.arity_sorts (Syntax.pp_global thy) (tsig_of thy);
    1.70  
    1.71 @@ -367,51 +355,6 @@
    1.72  
    1.73  
    1.74  
    1.75 -(** read and certify entities **)    (*exception ERROR*)
    1.76 -
    1.77 -(* classes *)
    1.78 -
    1.79 -fun read_class thy text =
    1.80 -  let
    1.81 -    val (syms, pos) = Syntax.read_token text;
    1.82 -    val c = certify_class thy (intern_class thy (Symbol_Pos.content syms))
    1.83 -      handle TYPE (msg, _, _) => error (msg ^ Position.str_of pos);
    1.84 -    val _ = Position.report (Markup.tclass c) pos;
    1.85 -  in c end;
    1.86 -
    1.87 -
    1.88 -(* type arities *)
    1.89 -
    1.90 -fun prep_arity prep_tycon prep_sort thy (t, Ss, S) =
    1.91 -  let val arity = (prep_tycon thy t, map (prep_sort thy) Ss, prep_sort thy S)
    1.92 -  in Type.add_arity (Syntax.pp_global thy) arity (tsig_of thy); arity end;
    1.93 -
    1.94 -val read_arity = prep_arity intern_type Syntax.read_sort_global;
    1.95 -val cert_arity = prep_arity (K I) certify_sort;
    1.96 -
    1.97 -
    1.98 -(* type syntax entities *)
    1.99 -
   1.100 -local
   1.101 -
   1.102 -fun read_type thy text =
   1.103 -  let
   1.104 -    val (syms, pos) = Syntax.read_token text;
   1.105 -    val c = intern_type thy (Symbol_Pos.content syms);
   1.106 -    val _ = the_type_decl thy c;
   1.107 -    val _ = Position.report (Markup.tycon c) pos;
   1.108 -  in c end;
   1.109 -
   1.110 -in
   1.111 -
   1.112 -val _ = Context.>>
   1.113 -  (Context.map_theory
   1.114 -    (map_syn (K (Syntax.basic_syntax {read_class = read_class, read_type = read_type}))));
   1.115 -
   1.116 -end;
   1.117 -
   1.118 -
   1.119 -
   1.120  (** signature extension functions **)  (*exception ERROR/TYPE*)
   1.121  
   1.122  (* add default sort *)