src/Pure/consts.ML
changeset 25041 c1efae25ee76
parent 25037 d6a3dec2375d
child 25048 5a94a87af697
     1.1 --- a/src/Pure/consts.ML	Mon Oct 15 15:29:46 2007 +0200
     1.2 +++ b/src/Pure/consts.ML	Mon Oct 15 21:08:35 2007 +0200
     1.3 @@ -14,11 +14,12 @@
     1.4    val dest: T ->
     1.5     {constants: (typ * (term * term) option) NameSpace.table,
     1.6      constraints: typ NameSpace.table}
     1.7 +  val the_type: T -> string -> typ                                  (*exception TYPE*)
     1.8    val the_abbreviation: T -> string -> typ * (term * term)          (*exception TYPE*)
     1.9 -  val the_declaration: T -> string -> typ                           (*exception TYPE*)
    1.10 +  val type_scheme: T -> string -> typ                               (*exception TYPE*)
    1.11 +  val the_tags: T -> string -> Markup.property list                 (*exception TYPE*)
    1.12    val is_monomorphic: T -> string -> bool                           (*exception TYPE*)
    1.13    val the_constraint: T -> string -> typ                            (*exception TYPE*)
    1.14 -  val the_tags: T -> string -> Markup.property list                 (*exception TYPE*)
    1.15    val space_of: T -> NameSpace.T
    1.16    val intern: T -> xstring -> string
    1.17    val extern: T -> string -> xstring
    1.18 @@ -82,9 +83,9 @@
    1.19  fun the_const (Consts ({decls = (_, tab), ...}, _)) c =
    1.20    (case Symtab.lookup tab c of
    1.21      SOME (decl, _) => decl
    1.22 -  | NONE => raise TYPE ("Undeclared constant: " ^ quote c, [], []));
    1.23 +  | NONE => raise TYPE ("Unknown constant: " ^ quote c, [], []));
    1.24  
    1.25 -fun the_declaration consts c =
    1.26 +fun the_type consts c =
    1.27    (case the_const consts c of
    1.28      ({T, ...}, NONE) => T
    1.29    | _ => raise TYPE ("Not a logical constant: " ^ quote c, [], []));
    1.30 @@ -94,15 +95,17 @@
    1.31      ({T, ...}, SOME abbr) => (T, dest_abbrev abbr)
    1.32    | _ => raise TYPE ("Not an abbreviated constant: " ^ quote c, [], []));
    1.33  
    1.34 -val type_arguments = (#typargs o #1) oo the_const;
    1.35 +val the_decl = #1 oo the_const;
    1.36 +val type_scheme = #T oo the_decl;
    1.37 +val type_arguments = #typargs oo the_decl;
    1.38 +val the_tags = #tags oo the_decl;
    1.39 +
    1.40  val is_monomorphic = null oo type_arguments;
    1.41  
    1.42  fun the_constraint (consts as Consts ({constraints, ...}, _)) c =
    1.43    (case Symtab.lookup constraints c of
    1.44      SOME T => T
    1.45 -  | NONE => #T (#1 (the_const consts c)));
    1.46 -
    1.47 -val the_tags = (#tags o #1) oo the_const;
    1.48 +  | NONE => type_scheme consts c);
    1.49  
    1.50  
    1.51  (* name space and syntax *)
    1.52 @@ -131,7 +134,7 @@
    1.53  fun read_const consts raw_c =
    1.54    let
    1.55      val c = intern consts raw_c;
    1.56 -    val ({T, ...}, _) = the_const consts c handle TYPE (msg, _, _) => error msg;
    1.57 +    val T = type_scheme consts c handle TYPE (msg, _, _) => error msg;
    1.58    in Const (c, T) end;
    1.59  
    1.60  
    1.61 @@ -195,7 +198,7 @@
    1.62  
    1.63  fun instance consts (c, Ts) =
    1.64    let
    1.65 -    val ({ T = declT, ... }, _) = the_const consts c;
    1.66 +    val declT = type_scheme consts c;
    1.67      val vars = map Term.dest_TVar (typargs consts (c, declT));
    1.68      val inst = vars ~~ Ts handle UnequalLengths =>
    1.69        raise TYPE ("Consts.instance", Ts, [Const (c, dummyT)]);