moved consts declarations to consts.ML;
authorwenzelm
Wed Nov 02 14:46:58 2005 +0100 (2005-11-02)
changeset 180627a666583e869
parent 18061 972e3d554eb8
child 18063 c4bffc47c11b
moved consts declarations to consts.ML;
src/Pure/sign.ML
     1.1 --- a/src/Pure/sign.ML	Wed Nov 02 14:46:57 2005 +0100
     1.2 +++ b/src/Pure/sign.ML	Wed Nov 02 14:46:58 2005 +0100
     1.3 @@ -3,7 +3,7 @@
     1.4      Author:     Lawrence C Paulson and Markus Wenzel
     1.5  
     1.6  Logical signature content: naming conventions, concrete syntax, type
     1.7 -signature, constant declarations.
     1.8 +signature, polymorphic constants.
     1.9  *)
    1.10  
    1.11  signature SIGN_THEORY =
    1.12 @@ -86,7 +86,7 @@
    1.13     {naming: NameSpace.naming,
    1.14      syn: Syntax.syntax,
    1.15      tsig: Type.tsig,
    1.16 -    consts: ((typ * bool) * serial) NameSpace.table * typ Symtab.table}
    1.17 +    consts: Consts.T}
    1.18    val naming_of: theory -> NameSpace.naming
    1.19    val base_name: string -> bstring
    1.20    val full_name: theory -> bstring -> string
    1.21 @@ -113,7 +113,8 @@
    1.22    val the_const_type: theory -> string -> typ
    1.23    val declared_tyname: theory -> string -> bool
    1.24    val declared_const: theory -> string -> bool
    1.25 -  val monomorphic: theory -> string -> bool
    1.26 +  val const_monomorphic: theory -> string -> bool
    1.27 +  val const_typargs: theory -> string -> typ -> typ list
    1.28    val class_space: theory -> NameSpace.T
    1.29    val type_space: theory -> NameSpace.T
    1.30    val const_space: theory -> NameSpace.T
    1.31 @@ -192,23 +193,14 @@
    1.32  (** datatype sign **)
    1.33  
    1.34  datatype sign = Sign of
    1.35 - {naming: NameSpace.naming,                   (*common naming conventions*)
    1.36 -  syn: Syntax.syntax,                         (*concrete syntax for terms, types, sorts*)
    1.37 -  tsig: Type.tsig,                            (*order-sorted signature of types*)
    1.38 -  consts:
    1.39 -    ((typ * bool) * serial) NameSpace.table * (*type schemes of declared term constants*)
    1.40 -    typ Symtab.table};                        (*type constraints for constants*)
    1.41 -
    1.42 + {naming: NameSpace.naming,     (*common naming conventions*)
    1.43 +  syn: Syntax.syntax,           (*concrete syntax for terms, types, sorts*)
    1.44 +  tsig: Type.tsig,              (*order-sorted signature of types*)
    1.45 +  consts: Consts.T};            (*polymorphic constants*)
    1.46  
    1.47  fun make_sign (naming, syn, tsig, consts) =
    1.48    Sign {naming = naming, syn = syn, tsig = tsig, consts = consts};
    1.49  
    1.50 -fun err_dup_consts cs =
    1.51 -  error ("Duplicate declaration of constant(s) " ^ commas_quote cs);
    1.52 -
    1.53 -fun err_inconsistent_constraints cs =
    1.54 -  error ("Inconsistent type constraints for constant(s) " ^ commas_quote cs);
    1.55 -
    1.56  structure SignData = TheoryDataFun
    1.57  (struct
    1.58    val name = "Pure/sign";
    1.59 @@ -217,22 +209,19 @@
    1.60    fun extend (Sign {syn, tsig, consts, ...}) =
    1.61      make_sign (NameSpace.default_naming, syn, tsig, consts);
    1.62  
    1.63 -  val empty = make_sign (NameSpace.default_naming, Syntax.pure_syn, Type.empty_tsig,
    1.64 -    (NameSpace.empty_table, Symtab.empty));
    1.65 +  val empty =
    1.66 +    make_sign (NameSpace.default_naming, Syntax.pure_syn, Type.empty_tsig, Consts.empty);
    1.67  
    1.68    fun merge pp (sign1, sign2) =
    1.69      let
    1.70 -      val Sign {naming = _, syn = syn1, tsig = tsig1, consts = (consts1, constraints1)} = sign1;
    1.71 -      val Sign {naming = _, syn = syn2, tsig = tsig2, consts = (consts2, constraints2)} = sign2;
    1.72 +      val Sign {naming = _, syn = syn1, tsig = tsig1, consts = consts1} = sign1;
    1.73 +      val Sign {naming = _, syn = syn2, tsig = tsig2, consts = consts2} = sign2;
    1.74  
    1.75        val naming = NameSpace.default_naming;
    1.76        val syn = Syntax.merge_syntaxes syn1 syn2;
    1.77        val tsig = Type.merge_tsigs pp (tsig1, tsig2);
    1.78 -      val consts = NameSpace.merge_tables (eq_snd (op =)) (consts1, consts2)
    1.79 -        handle Symtab.DUPS cs => err_dup_consts cs;
    1.80 -      val constraints = Symtab.merge (op =) (constraints1, constraints2)
    1.81 -        handle Symtab.DUPS cs => err_inconsistent_constraints cs;
    1.82 -    in make_sign (naming, syn, tsig, (consts, constraints)) end;
    1.83 +      val consts = Consts.merge (consts1, consts2);
    1.84 +    in make_sign (naming, syn, tsig, consts) end;
    1.85  
    1.86    fun print _ _ = ();
    1.87  end);
    1.88 @@ -282,40 +271,26 @@
    1.89  fun is_logtype thy c = c mem_string Type.logical_types (tsig_of thy);
    1.90  
    1.91  
    1.92 -(* consts signature *)
    1.93 -
    1.94 -fun const_constraint thy c =
    1.95 -  let val ((_, consts), constraints) = #consts (rep_sg thy) in
    1.96 -    (case Symtab.lookup constraints c of
    1.97 -      NONE => Option.map (#1 o #1) (Symtab.lookup consts c)
    1.98 -    | some => some)
    1.99 -  end;
   1.100 +(* polymorphic constants *)
   1.101  
   1.102 -fun the_const_constraint thy c =
   1.103 -  (case const_constraint thy c of SOME T => T
   1.104 -  | NONE => raise TYPE ("Undeclared constant " ^ quote c, [], []));
   1.105 -
   1.106 -val lookup_const = Symtab.lookup o #2 o #1 o #consts o rep_sg;
   1.107 -val const_type = Option.map (#1 o #1) oo lookup_const;
   1.108 -
   1.109 -fun the_const_type thy c =
   1.110 -  (case const_type thy c of SOME T => T
   1.111 -  | NONE => raise TYPE ("Undeclared constant " ^ quote c, [], []));
   1.112 +val consts_of = #consts o rep_sg;
   1.113 +val the_const_constraint = Consts.constraint o consts_of;
   1.114 +val const_constraint = try o the_const_constraint;
   1.115 +val the_const_type = Consts.declaration o consts_of;
   1.116 +val const_type = try o the_const_type;
   1.117 +val const_monomorphic = Consts.monomorphic o consts_of;
   1.118 +val const_typargs = Consts.typargs o consts_of;
   1.119  
   1.120  val declared_tyname = Symtab.defined o #2 o #types o Type.rep_tsig o tsig_of;
   1.121  val declared_const = is_some oo const_type;
   1.122  
   1.123 -fun monomorphic thy =
   1.124 -  let val mono = Symtab.lookup (#2 (#1 (#consts (rep_sg thy))))
   1.125 -  in fn c => (case mono c of SOME ((_, m), _) => m | _ => false) end;
   1.126 -
   1.127  
   1.128  
   1.129  (** intern / extern names **)
   1.130  
   1.131  val class_space = #1 o #classes o Type.rep_tsig o tsig_of;
   1.132  val type_space = #1 o #types o Type.rep_tsig o tsig_of;
   1.133 -val const_space = #1 o #1 o #consts o rep_sg
   1.134 +val const_space = Consts.space o consts_of;
   1.135  
   1.136  val intern_class = NameSpace.intern o class_space;
   1.137  val extern_class = NameSpace.extern o class_space;
   1.138 @@ -453,10 +428,10 @@
   1.139      fun check_atoms (t $ u) = (check_atoms t; check_atoms u)
   1.140        | check_atoms (Abs (_, _, t)) = check_atoms t
   1.141        | check_atoms (Const (a, T)) =
   1.142 -          (case lookup_const thy a of
   1.143 +          (case const_type thy a of
   1.144              NONE => err ("Undeclared constant " ^ show_const a T)
   1.145 -          | SOME ((U, mono), _) =>
   1.146 -              if mono andalso T = U orelse typ_instance thy (T, U) then ()
   1.147 +          | SOME U =>
   1.148 +              if typ_instance thy (T, U) then ()
   1.149                else err ("Illegal type for constant " ^ show_const a T))
   1.150        | check_atoms (Var ((x, i), _)) =
   1.151            if i < 0 then err ("Malformed variable: " ^ quote x) else ()
   1.152 @@ -696,24 +671,16 @@
   1.153  
   1.154  local
   1.155  
   1.156 -fun is_mono (Type (_, Ts)) = forall is_mono Ts
   1.157 -  | is_mono _ = false;
   1.158 -
   1.159  fun gen_add_consts prep_typ raw_args thy =
   1.160    let
   1.161      val prepT = Compress.typ thy o Type.varifyT o Type.no_tvars o Term.no_dummyT o prep_typ thy;
   1.162      fun prep (c, T, mx) = ((c, prepT T, mx) handle TYPE (msg, _, _) => error msg)
   1.163        handle ERROR => error ("in declaration of constant " ^ quote (Syntax.const_name c mx));
   1.164      val args = map prep raw_args;
   1.165 -
   1.166 -    val decls = args |> map (fn (c, T, mx) =>
   1.167 -      (Syntax.const_name c mx, ((T, is_mono T), serial ())));
   1.168 -
   1.169 -    fun extend_consts consts = NameSpace.extend_table (naming_of thy) (consts, decls)
   1.170 -      handle Symtab.DUPS cs => err_dup_consts cs;
   1.171 +    val decls = args |> map (fn (c, T, mx) => (Syntax.const_name c mx, T));
   1.172    in
   1.173      thy
   1.174 -    |> map_consts (apfst extend_consts)
   1.175 +    |> map_consts (fold (Consts.declare (naming_of thy)) decls)
   1.176      |> add_syntax_i args
   1.177    end;
   1.178  
   1.179 @@ -734,7 +701,7 @@
   1.180        handle TYPE (msg, _, _) => error msg;
   1.181      val _ = cert_term thy (Const (c, T))
   1.182        handle TYPE (msg, _, _) => error msg;
   1.183 -  in thy |> map_consts (apsnd (Symtab.update (c, T))) end;
   1.184 +  in thy |> map_consts (Consts.constrain (c, T)) end;
   1.185  
   1.186  val add_const_constraint = gen_add_constraint intern_const (read_typ o no_def_sort);
   1.187  val add_const_constraint_i = gen_add_constraint (K I) certify_typ;
   1.188 @@ -872,9 +839,8 @@
   1.189  val hide_classes_i = map_tsig oo Type.hide_classes;
   1.190  fun hide_types b xs thy = thy |> map_tsig (Type.hide_types b (map (intern_type thy) xs));
   1.191  val hide_types_i = map_tsig oo Type.hide_types;
   1.192 -fun hide_consts b xs thy =
   1.193 -  thy |> map_consts (apfst (apfst (fold (NameSpace.hide b o intern_const thy) xs)));
   1.194 -val hide_consts_i = (map_consts o apfst o apfst) oo (fold o NameSpace.hide);
   1.195 +fun hide_consts b xs thy = thy |> map_consts (fold (Consts.hide b o intern_const thy) xs);
   1.196 +val hide_consts_i = map_consts oo (fold o Consts.hide);
   1.197  
   1.198  local
   1.199