src/Pure/sign.ML
author wenzelm
Tue Feb 08 14:09:34 1994 +0100 (1994-02-08)
changeset 266 3fe01df1a614
parent 251 c9b984c0a674
child 267 ab78019b8ec8
permissions -rw-r--r--
improved eq_sg;
cosmetical change in print_sg;
wenzelm@19
     1
(*  Title:      Pure/sign.ML
clasohm@0
     2
    ID:         $Id$
wenzelm@251
     3
    Author:     Lawrence C Paulson and Markus Wenzel
clasohm@0
     4
wenzelm@251
     5
The abstract type "sg" of signatures.
wenzelm@251
     6
wenzelm@251
     7
TODO:
wenzelm@251
     8
  a clean modular sequential Sign.extend (using sg_ext list);
clasohm@0
     9
*)
clasohm@0
    10
wenzelm@19
    11
signature SIGN =
clasohm@0
    12
sig
clasohm@0
    13
  structure Symtab: SYMTAB
clasohm@0
    14
  structure Syntax: SYNTAX
wenzelm@251
    15
  structure Type: TYPE
wenzelm@143
    16
  sharing Symtab = Type.Symtab
wenzelm@251
    17
  local open Type in
wenzelm@251
    18
    type sg
wenzelm@251
    19
    val rep_sg: sg ->
wenzelm@251
    20
      {tsig: type_sig,
wenzelm@251
    21
       const_tab: typ Symtab.table,
wenzelm@251
    22
       syn: Syntax.syntax,
wenzelm@251
    23
       stamps: string ref list}
wenzelm@251
    24
    val subsig: sg * sg -> bool
wenzelm@251
    25
    val eq_sg: sg * sg -> bool
wenzelm@251
    26
    val print_sg: sg -> unit
wenzelm@251
    27
    val pprint_sg: sg -> pprint_args -> unit
wenzelm@251
    28
    val pretty_term: sg -> term -> Syntax.Pretty.T
wenzelm@251
    29
    val pretty_typ: sg -> typ -> Syntax.Pretty.T
wenzelm@251
    30
    val string_of_term: sg -> term -> string
wenzelm@251
    31
    val string_of_typ: sg -> typ -> string
wenzelm@251
    32
    val pprint_term: sg -> term -> pprint_args -> unit
wenzelm@251
    33
    val pprint_typ: sg -> typ -> pprint_args -> unit
wenzelm@251
    34
    val certify_typ: sg -> typ -> typ
wenzelm@251
    35
    val certify_term: sg -> term -> term * typ * int
wenzelm@251
    36
    val read_typ: sg * (indexname -> sort option) -> string -> typ
wenzelm@251
    37
    val extend: sg -> string ->
wenzelm@251
    38
      (class * class list) list * class list *
wenzelm@251
    39
      (string list * int) list *
wenzelm@251
    40
      (string * string list * string) list *
wenzelm@251
    41
      (string list * (sort list * class)) list *
wenzelm@251
    42
      (string list * string) list * Syntax.sext option -> sg
wenzelm@251
    43
    val merge: sg * sg -> sg
wenzelm@251
    44
    val pure: sg
wenzelm@251
    45
  end
clasohm@0
    46
end;
clasohm@0
    47
wenzelm@251
    48
functor SignFun(structure Syntax: SYNTAX and Type: TYPE): SIGN =
wenzelm@143
    49
struct
clasohm@0
    50
clasohm@0
    51
structure Symtab = Type.Symtab;
clasohm@0
    52
structure Syntax = Syntax;
wenzelm@251
    53
structure Pretty = Syntax.Pretty;
wenzelm@251
    54
structure Type = Type;
wenzelm@251
    55
open Type;
clasohm@0
    56
wenzelm@143
    57
wenzelm@251
    58
(** datatype sg **)
wenzelm@251
    59
wenzelm@251
    60
(*the "ref" in stamps ensures that no two signatures are identical -- it is
wenzelm@251
    61
  impossible to forge a signature*)
wenzelm@143
    62
wenzelm@19
    63
datatype sg =
wenzelm@143
    64
  Sg of {
wenzelm@251
    65
    tsig: type_sig,                 (*order-sorted signature of types*)
wenzelm@143
    66
    const_tab: typ Symtab.table,    (*types of constants*)
wenzelm@143
    67
    syn: Syntax.syntax,             (*syntax for parsing and printing*)
wenzelm@143
    68
    stamps: string ref list};       (*unique theory indentifier*)
clasohm@0
    69
clasohm@0
    70
fun rep_sg (Sg args) = args;
clasohm@0
    71
nipkow@206
    72
wenzelm@251
    73
fun subsig (Sg {stamps = s1, ...}, Sg {stamps = s2, ...}) = s1 subset s2;
clasohm@0
    74
wenzelm@266
    75
fun eq_sg (Sg {stamps = s1, ...}, Sg {stamps = s2, ...}) = eq_set (s1, s2);
clasohm@0
    76
clasohm@0
    77
clasohm@0
    78
wenzelm@251
    79
(** print signature **)
wenzelm@251
    80
wenzelm@251
    81
fun print_sg sg =
wenzelm@251
    82
  let
wenzelm@251
    83
    fun prt_typ syn ty = Pretty.quote (Syntax.pretty_typ syn ty);
wenzelm@251
    84
wenzelm@251
    85
    fun pretty_sort [cl] = Pretty.str cl
wenzelm@251
    86
      | pretty_sort cls = Pretty.str_list "{" "}" cls;
wenzelm@251
    87
wenzelm@251
    88
    fun pretty_subclass (cl, cls) = Pretty.block
wenzelm@251
    89
      [Pretty.str (cl ^ " <"), Pretty.brk 1, pretty_sort cls];
wenzelm@251
    90
wenzelm@251
    91
    fun pretty_default cls = Pretty.block
wenzelm@251
    92
      [Pretty.str "default:", Pretty.brk 1, pretty_sort cls];
wenzelm@251
    93
wenzelm@251
    94
    fun pretty_arg (ty, n) = Pretty.str (ty ^ " " ^ string_of_int n);
wenzelm@251
    95
wenzelm@251
    96
    fun pretty_abbr syn (ty, (vs, rhs)) = Pretty.block
wenzelm@251
    97
      [prt_typ syn (Type (ty, map (fn v => TVar (v, [])) vs)),
wenzelm@251
    98
        Pretty.str " =", Pretty.brk 1, prt_typ syn rhs];
wenzelm@251
    99
wenzelm@251
   100
    fun pretty_arity ty (cl, []) = Pretty.block
wenzelm@251
   101
          [Pretty.str (ty ^ " ::"), Pretty.brk 1, Pretty.str cl]
wenzelm@251
   102
      | pretty_arity ty (cl, srts) = Pretty.block
wenzelm@251
   103
          [Pretty.str (ty ^ " ::"), Pretty.brk 1,
wenzelm@251
   104
            Pretty.list "(" ")" (map pretty_sort srts),
wenzelm@251
   105
            Pretty.brk 1, Pretty.str cl];
wenzelm@251
   106
wenzelm@251
   107
    fun pretty_coreg (ty, ars) = map (pretty_arity ty) ars;
wenzelm@251
   108
wenzelm@251
   109
    fun pretty_const syn (c, ty) = Pretty.block
wenzelm@266
   110
      [Pretty.str (quote c ^ " ::"), Pretty.brk 1, prt_typ syn ty];
wenzelm@251
   111
wenzelm@251
   112
wenzelm@251
   113
    val Sg {tsig, const_tab, syn, stamps} = sg;
wenzelm@251
   114
    val {classes, subclass, default, args, abbrs, coreg} = rep_tsig tsig;
wenzelm@251
   115
  in
wenzelm@251
   116
    Pretty.writeln (Pretty.strs ("stamps:" :: map ! stamps));
wenzelm@251
   117
    Pretty.writeln (Pretty.strs ("classes:" :: classes));
wenzelm@251
   118
    Pretty.writeln (Pretty.big_list "subclass:" (map pretty_subclass subclass));
wenzelm@251
   119
    Pretty.writeln (pretty_default default);
wenzelm@251
   120
    Pretty.writeln (Pretty.big_list "types:" (map pretty_arg args));
wenzelm@251
   121
    Pretty.writeln (Pretty.big_list "abbrs:" (map (pretty_abbr syn) abbrs));
wenzelm@251
   122
    Pretty.writeln (Pretty.big_list "coreg:" (flat (map pretty_coreg coreg)));
wenzelm@251
   123
    Pretty.writeln (Pretty.big_list "consts:"
wenzelm@251
   124
      (map (pretty_const syn) (Symtab.alist_of const_tab)))
wenzelm@251
   125
  end;
wenzelm@251
   126
wenzelm@251
   127
wenzelm@251
   128
fun pprint_sg (Sg {stamps, ...}) =
wenzelm@251
   129
  Pretty.pprint (Pretty.str_list "{" "}" (map ! stamps));
wenzelm@251
   130
wenzelm@251
   131
wenzelm@251
   132
wenzelm@251
   133
(** pretty printing of terms and types **)
wenzelm@251
   134
wenzelm@251
   135
fun pretty_term (Sg {syn, ...}) = Syntax.pretty_term syn;
wenzelm@251
   136
fun pretty_typ (Sg {syn, ...}) = Syntax.pretty_typ syn;
wenzelm@251
   137
wenzelm@251
   138
fun string_of_term (Sg {syn, ...}) = Syntax.string_of_term syn;
wenzelm@251
   139
fun string_of_typ (Sg {syn, ...}) = Syntax.string_of_typ syn;
wenzelm@251
   140
wenzelm@251
   141
fun pprint_term sg = Pretty.pprint o Pretty.quote o (pretty_term sg);
wenzelm@251
   142
fun pprint_typ sg = Pretty.pprint o Pretty.quote o (pretty_typ sg);
clasohm@0
   143
clasohm@0
   144
wenzelm@169
   145
wenzelm@251
   146
(** certify types and terms **)
wenzelm@251
   147
wenzelm@251
   148
(*errors are indicated by exception TYPE*)
wenzelm@251
   149
wenzelm@251
   150
fun certify_typ (Sg {tsig, ...}) ty = cert_typ tsig ty;
wenzelm@251
   151
wenzelm@251
   152
wenzelm@251
   153
(* FIXME -> term.ML (?) *)
wenzelm@251
   154
fun mapfilter_atoms f (Abs (_, _, t)) = mapfilter_atoms f t
wenzelm@251
   155
  | mapfilter_atoms f (t $ u) = mapfilter_atoms f t @ mapfilter_atoms f u
wenzelm@251
   156
  | mapfilter_atoms f a = (case f a of Some y => [y] | None => []);
clasohm@0
   157
wenzelm@251
   158
fun certify_term (sg as Sg {tsig, const_tab, ...}) tm =
wenzelm@251
   159
  let
wenzelm@251
   160
    fun valid_const a T =
wenzelm@251
   161
      (case Symtab.lookup (const_tab, a) of
wenzelm@251
   162
        Some U => typ_instance (tsig, T, U)
wenzelm@251
   163
      | _ => false);
wenzelm@169
   164
wenzelm@251
   165
    fun atom_err (Const (a, T)) =
wenzelm@251
   166
          if valid_const a T then None
wenzelm@251
   167
          else Some ("Illegal type for constant " ^ quote a ^ " :: " ^
wenzelm@251
   168
            quote (string_of_typ sg T))
wenzelm@251
   169
      | atom_err (Var ((x, i), _)) =
wenzelm@251
   170
          if i < 0 then Some ("Negative index for Var " ^ quote x) else None
wenzelm@251
   171
      | atom_err _ = None;
wenzelm@251
   172
wenzelm@169
   173
wenzelm@251
   174
    val norm_tm =
wenzelm@251
   175
      (case it_term_types (typ_errors tsig) (tm, []) of
wenzelm@251
   176
        [] => map_term_types (norm_typ tsig) tm
wenzelm@251
   177
      | errs => raise_type (cat_lines errs) [] [tm]);
wenzelm@251
   178
  in
wenzelm@251
   179
    (case mapfilter_atoms atom_err norm_tm of
wenzelm@251
   180
      [] => (norm_tm, type_of norm_tm, maxidx_of_term norm_tm)
wenzelm@251
   181
    | errs => raise_type (cat_lines errs) [] [norm_tm])
wenzelm@251
   182
  end;
wenzelm@251
   183
wenzelm@251
   184
wenzelm@251
   185
wenzelm@251
   186
(** read types **)
wenzelm@251
   187
wenzelm@251
   188
(*read and certify typ wrt a signature; errors are indicated by
wenzelm@251
   189
  exception ERROR (with messages already printed)*)
wenzelm@169
   190
wenzelm@251
   191
fun rd_typ tsig syn sort_of s =
wenzelm@251
   192
  let
wenzelm@251
   193
    val def_sort = defaultS tsig;
wenzelm@251
   194
    val raw_ty =        (*this may raise ERROR, too!*)
wenzelm@251
   195
      Syntax.read_typ syn (fn x => if_none (sort_of x) def_sort) s;
wenzelm@251
   196
  in
wenzelm@251
   197
    cert_typ tsig raw_ty
wenzelm@251
   198
      handle TYPE (msg, _, _) => error msg
wenzelm@251
   199
  end
wenzelm@251
   200
  handle ERROR => error ("The error(s) above occurred in type " ^ quote s);
wenzelm@169
   201
wenzelm@251
   202
fun read_typ (Sg {tsig, syn, ...}, sort_of) s = rd_typ tsig syn sort_of s;
wenzelm@251
   203
wenzelm@251
   204
wenzelm@251
   205
wenzelm@251
   206
(** extend signature **)
wenzelm@251
   207
wenzelm@251
   208
(*errors are indicated by exception ERROR (with messages already printed)*)
wenzelm@251
   209
wenzelm@251
   210
fun extend sg name (classes, default, types, abbrs, arities, consts, opt_sext) =
wenzelm@251
   211
  let
wenzelm@251
   212
    (*reset TVar indices to 0, renaming to preserve distinctness*)
wenzelm@251
   213
    fun zero_tvar_idxs T =
wenzelm@169
   214
      let
wenzelm@169
   215
        val inxSs = typ_tvars T;
wenzelm@169
   216
        val nms' = variantlist (map (#1 o #1) inxSs, []);
wenzelm@251
   217
        val tye = map2 (fn ((v, S), a) => (v, TVar ((a, 0), S))) (inxSs, nms');
wenzelm@251
   218
      in
wenzelm@251
   219
        typ_subst_TVars tye T
wenzelm@251
   220
      end;
wenzelm@169
   221
wenzelm@169
   222
    (*read and check the type mentioned in a const declaration; zero type var
wenzelm@169
   223
      indices because type inference requires it*)
wenzelm@251
   224
    fun read_const tsig syn (c, s) =
wenzelm@251
   225
      (c, zero_tvar_idxs (varifyT (rd_typ tsig syn (K None) s)))
wenzelm@251
   226
        handle ERROR => error ("in declaration of constant " ^ quote c);
wenzelm@169
   227
wenzelm@251
   228
    fun read_abbr tsig syn (c, vs, rhs_src) =
wenzelm@251
   229
      (c, (map (rpair 0) vs, varifyT (rd_typ tsig syn (K None) rhs_src)
wenzelm@251
   230
        handle ERROR => error ("in type abbreviation " ^ quote c)));
wenzelm@251
   231
clasohm@0
   232
wenzelm@251
   233
    val Sg {tsig, const_tab, syn, stamps} = sg;
wenzelm@251
   234
    val xconsts = map #1 classes @ flat (map #1 types) @ map #1 abbrs @
wenzelm@251
   235
      flat (map #1 consts);
wenzelm@251
   236
    val sext = if_none opt_sext Syntax.empty_sext;
wenzelm@143
   237
wenzelm@251
   238
    val tsig' = extend_tsig tsig (classes, default, types, arities);
wenzelm@251
   239
    val tsig1 = ext_tsig_abbrs tsig' (map (read_abbr tsig' syn) abbrs);
nipkow@200
   240
wenzelm@251
   241
    val syn1 = Syntax.extend syn (rd_typ tsig1 syn (K None))
wenzelm@251
   242
      (logical_types tsig1, xconsts, sext);
wenzelm@143
   243
wenzelm@251
   244
    val all_consts = flat (map (fn (cs, s) => map (rpair s) cs)
wenzelm@251
   245
      (Syntax.constants sext @ consts));
wenzelm@169
   246
wenzelm@251
   247
    val const_tab1 =                              (* FIXME bug: vvvv should be syn *)
wenzelm@251
   248
      Symtab.extend (K false) (const_tab, map (read_const tsig1 syn1) all_consts)
wenzelm@251
   249
        handle Symtab.DUPLICATE c
wenzelm@251
   250
          => error ("Constant " ^ quote c ^ " declared twice");
wenzelm@169
   251
wenzelm@251
   252
    val stamps1 =
wenzelm@251
   253
      if exists (equal name o !) stamps then
wenzelm@251
   254
        error ("Theory already contains a " ^ quote name ^ " component")
wenzelm@251
   255
      else stamps @ [ref name];
wenzelm@143
   256
  in
wenzelm@251
   257
    Sg {tsig = tsig1, const_tab = const_tab1, syn = syn1, stamps = stamps1}
wenzelm@143
   258
  end;
clasohm@0
   259
clasohm@0
   260
wenzelm@251
   261
wenzelm@251
   262
(** merge signatures **)
wenzelm@251
   263
wenzelm@251
   264
(*errors are indicated by exception TERM*)
wenzelm@143
   265
wenzelm@251
   266
fun check_stamps stamps =
wenzelm@251
   267
  (case duplicates (map ! stamps) of
wenzelm@251
   268
    [] => stamps
wenzelm@251
   269
  | dups => raise_term ("Attempt to merge different versions of theories " ^
wenzelm@251
   270
      commas (map quote dups)) []);
wenzelm@143
   271
wenzelm@251
   272
fun merge (sg1, sg2) =
wenzelm@251
   273
  if subsig (sg2, sg1) then sg1
wenzelm@251
   274
  else if subsig (sg1, sg2) then sg2
wenzelm@251
   275
  else
wenzelm@251
   276
    (*neither is union already; must form union*)
wenzelm@251
   277
    let
wenzelm@251
   278
      val Sg {tsig = tsig1, const_tab = const_tab1, syn = syn1,
wenzelm@251
   279
        stamps = stamps1} = sg1;
wenzelm@251
   280
      val Sg {tsig = tsig2, const_tab = const_tab2, syn = syn2,
wenzelm@251
   281
        stamps = stamps2} = sg2;
wenzelm@251
   282
wenzelm@251
   283
      val tsig = merge_tsigs (tsig1, tsig2);
wenzelm@251
   284
wenzelm@251
   285
      val const_tab = Symtab.merge (op =) (const_tab1, const_tab2)
wenzelm@251
   286
        handle Symtab.DUPLICATE c =>
wenzelm@251
   287
          raise_term ("Incompatible types for constant " ^ quote c) [];
wenzelm@251
   288
wenzelm@251
   289
      val syn = Syntax.merge (logical_types tsig) syn1 syn2;
wenzelm@251
   290
wenzelm@251
   291
      val stamps = check_stamps (merge_lists stamps1 stamps2);
wenzelm@251
   292
    in
wenzelm@251
   293
      Sg {tsig = tsig, const_tab = const_tab, syn = syn, stamps = stamps}
wenzelm@251
   294
    end;
wenzelm@143
   295
clasohm@0
   296
clasohm@0
   297
wenzelm@251
   298
(** the Pure signature **)
clasohm@0
   299
wenzelm@251
   300
val sg0 = Sg {tsig = tsig0, const_tab = Symtab.null,
wenzelm@251
   301
  syn = Syntax.type_syn, stamps = []};
clasohm@0
   302
wenzelm@251
   303
val pure = extend sg0 "Pure"
wenzelm@251
   304
  ([("logic", [])],
wenzelm@251
   305
   ["logic"],
wenzelm@251
   306
   [(["fun"], 2),
wenzelm@251
   307
    (["prop"], 0),
wenzelm@251
   308
    (Syntax.syntax_types, 0)],
wenzelm@251
   309
   [],
wenzelm@251
   310
   [(["fun"],  ([["logic"], ["logic"]], "logic")),
wenzelm@251
   311
    (["prop"], ([], "logic"))],
wenzelm@251
   312
   ([Syntax.constrainC], "'a::{} => 'a") :: Syntax.syntax_consts,
wenzelm@251
   313
   Some Syntax.pure_sext);
clasohm@0
   314
clasohm@0
   315
clasohm@0
   316
end;
wenzelm@143
   317