added the_const_type;
authorwenzelm
Sun Jun 05 23:07:26 2005 +0200 (2005-06-05)
changeset 16288df2b550a17f6
parent 16287 7a03b4b4df67
child 16289 958207815931
added the_const_type;
src/Pure/sign.ML
     1.1 --- a/src/Pure/sign.ML	Sun Jun 05 23:07:25 2005 +0200
     1.2 +++ b/src/Pure/sign.ML	Sun Jun 05 23:07:26 2005 +0200
     1.3 @@ -39,7 +39,9 @@
     1.4    val is_draft: sg -> bool
     1.5    val is_stale: sg -> bool
     1.6    val syn_of: sg -> Syntax.syntax
     1.7 +  val naming_of: sg -> NameSpace.naming
     1.8    val const_type: sg -> string -> typ option
     1.9 +  val the_const_type: sg -> string -> typ          (*exception TYPE*)
    1.10    val declared_tyname: sg -> string -> bool
    1.11    val declared_const: sg -> string -> bool
    1.12    val classes: sg -> class list
    1.13 @@ -52,7 +54,6 @@
    1.14    val classK: string
    1.15    val typeK: string
    1.16    val constK: string
    1.17 -  val naming_of: sg -> NameSpace.naming
    1.18    val base_name: string -> bstring
    1.19    val full_name: sg -> bstring -> string
    1.20    val full_name_path: sg -> string -> bstring -> string
    1.21 @@ -99,7 +100,7 @@
    1.22    val read_typ': Syntax.syntax -> sg * (indexname -> sort option) -> string -> typ
    1.23    val read_typ_raw': Syntax.syntax -> sg * (indexname -> sort option) -> string -> typ
    1.24    val read_tyname: sg -> string -> typ
    1.25 -  val read_const: sg -> string -> term
    1.26 +  val read_const: sg -> string -> term        (*exception TYPE*)
    1.27    val infer_types: Pretty.pp -> sg -> (indexname -> typ option) ->
    1.28      (indexname -> sort option) -> string list -> bool
    1.29      -> xterm list * typ -> term * (indexname * typ) list
    1.30 @@ -237,10 +238,15 @@
    1.31  val str_of_sg = Pretty.str_of o pretty_sg;
    1.32  val pprint_sg = Pretty.pprint o pretty_sg;
    1.33  
    1.34 +fun naming_of (Sg (_, {naming, ...})) = naming;
    1.35  val tsig_of = #tsig o rep_sg;
    1.36  fun is_logtype sg c = c mem_string Type.logical_types (tsig_of sg);
    1.37 +
    1.38  fun const_type (Sg (_, {consts, ...})) c = Option.map #1 (Symtab.lookup (consts, c));
    1.39 -fun naming_of (Sg (_, {naming, ...})) = naming;
    1.40 +
    1.41 +fun the_const_type sg c =
    1.42 +  (case const_type sg c of SOME T => T
    1.43 +  | NONE => raise TYPE ("Undeclared constant " ^ quote c, [], []));
    1.44  
    1.45  fun declared_tyname sg c = is_some (Symtab.lookup (#types (Type.rep_tsig (tsig_of sg)), c));
    1.46  fun declared_const sg c = is_some (const_type sg c);
    1.47 @@ -759,10 +765,8 @@
    1.48    end;
    1.49  
    1.50  fun read_const sg raw_c =
    1.51 -  let val c = intern_const sg raw_c in
    1.52 -    if is_some (const_type sg c) then Const (c, dummyT)
    1.53 -    else raise TYPE ("Undeclared constant: " ^ quote c, [], [])
    1.54 -  end;
    1.55 +  let val c = intern_const sg raw_c
    1.56 +  in the_const_type sg c; Const (c, dummyT) end;
    1.57  
    1.58  
    1.59