provide direct access to the different kinds of type declarations;
authorwenzelm
Thu Feb 25 22:05:34 2010 +0100 (2010-02-25)
changeset 353593ec03a3cd9d0
parent 35358 63fb71d29eba
child 35360 df2b2168e43a
provide direct access to the different kinds of type declarations;
src/Pure/sign.ML
src/Pure/type.ML
     1.1 --- a/src/Pure/sign.ML	Thu Feb 25 09:16:16 2010 +0100
     1.2 +++ b/src/Pure/sign.ML	Thu Feb 25 22:05:34 2010 +0100
     1.3 @@ -60,6 +60,7 @@
     1.4    val intern_term: theory -> term -> term
     1.5    val extern_term: theory -> term -> term
     1.6    val intern_tycons: theory -> typ -> typ
     1.7 +  val the_type_decl: theory -> string -> Type.decl
     1.8    val arity_number: theory -> string -> int
     1.9    val arity_sorts: theory -> string -> sort -> sort list
    1.10    val certify_class: theory -> class -> class
    1.11 @@ -308,6 +309,7 @@
    1.12  
    1.13  (* certify wrt. type signature *)
    1.14  
    1.15 +val the_type_decl = Type.the_decl o tsig_of;
    1.16  val arity_number = Type.arity_number o tsig_of;
    1.17  fun arity_sorts thy = Type.arity_sorts (Syntax.pp_global thy) (tsig_of thy);
    1.18  
     2.1 --- a/src/Pure/type.ML	Thu Feb 25 09:16:16 2010 +0100
     2.2 +++ b/src/Pure/type.ML	Thu Feb 25 22:05:34 2010 +0100
     2.3 @@ -35,6 +35,7 @@
     2.4    val get_mode: Proof.context -> mode
     2.5    val set_mode: mode -> Proof.context -> Proof.context
     2.6    val restore_mode: Proof.context -> Proof.context -> Proof.context
     2.7 +  val the_decl: tsig -> string -> decl
     2.8    val cert_typ_mode: mode -> tsig -> typ -> typ
     2.9    val cert_typ: tsig -> typ -> typ
    2.10    val arity_number: tsig -> string -> int
    2.11 @@ -163,6 +164,11 @@
    2.12  
    2.13  fun lookup_type (TSig {types = (_, types), ...}) = Symtab.lookup types;
    2.14  
    2.15 +fun the_decl tsig c =
    2.16 +  (case lookup_type tsig c of
    2.17 +    NONE => error (undecl_type c)
    2.18 +  | SOME decl => decl);
    2.19 +
    2.20  
    2.21  (* certified types *)
    2.22  
    2.23 @@ -189,15 +195,14 @@
    2.24              val Ts' = map cert Ts;
    2.25              fun nargs n = if length Ts <> n then err (bad_nargs c) else ();
    2.26            in
    2.27 -            (case lookup_type tsig c of
    2.28 -              SOME (LogicalType n) => (nargs n; Type (c, Ts'))
    2.29 -            | SOME (Abbreviation (vs, U, syn)) =>
    2.30 +            (case the_decl tsig c of
    2.31 +              LogicalType n => (nargs n; Type (c, Ts'))
    2.32 +            | Abbreviation (vs, U, syn) =>
    2.33                 (nargs (length vs);
    2.34                  if syn then check_logical c else ();
    2.35                  if normalize then inst_typ (vs ~~ Ts') U
    2.36                  else Type (c, Ts'))
    2.37 -            | SOME Nonterminal => (nargs 0; check_logical c; T)
    2.38 -            | NONE => err (undecl_type c))
    2.39 +            | Nonterminal => (nargs 0; check_logical c; T))
    2.40            end
    2.41        | cert (TFree (x, S)) = TFree (x, cert_sort tsig S)
    2.42        | cert (TVar (xi as (_, i), S)) =