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