src/Pure/sign.ML
author nipkow
Thu Dec 30 10:18:23 1993 +0100 (1993-12-30)
changeset 206 0d624d1ba9cc
parent 200 39a931cc6558
child 211 7ab45715c0a6
permissions -rw-r--r--
added subsig: sg * sg -> bool to test if one signature is contained in another.
wenzelm@19
     1
(*  Title:      Pure/sign.ML
clasohm@0
     2
    ID:         $Id$
wenzelm@19
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
clasohm@0
     4
    Copyright   1992  University of Cambridge
clasohm@0
     5
wenzelm@143
     6
The abstract types "sg" (signatures) and "cterm" / "ctyp" (certified terms /
wenzelm@143
     7
typs under a signature).
clasohm@0
     8
*)
clasohm@0
     9
wenzelm@19
    10
signature SIGN =
clasohm@0
    11
sig
clasohm@0
    12
  structure Type: TYPE
clasohm@0
    13
  structure Symtab: SYMTAB
clasohm@0
    14
  structure Syntax: SYNTAX
wenzelm@143
    15
  sharing Symtab = Type.Symtab
clasohm@0
    16
  type sg
clasohm@0
    17
  type cterm
clasohm@0
    18
  type ctyp
clasohm@0
    19
  val cfun: (term -> term) -> (cterm -> cterm)
clasohm@0
    20
  val cterm_of: sg -> term -> cterm
clasohm@0
    21
  val ctyp_of: sg -> typ -> ctyp
clasohm@0
    22
  val extend: sg -> string ->
wenzelm@19
    23
        (class * class list) list * class list *
wenzelm@19
    24
        (string list * int) list *
nipkow@200
    25
        (string * indexname list * string) list *
wenzelm@19
    26
        (string list * (sort list * class)) list *
wenzelm@19
    27
        (string list * string)list * Syntax.sext option -> sg
clasohm@0
    28
  val merge: sg * sg -> sg
clasohm@0
    29
  val pure: sg
clasohm@0
    30
  val read_cterm: sg -> string * typ -> cterm
clasohm@0
    31
  val read_ctyp: sg -> string -> ctyp
clasohm@0
    32
  val read_insts: sg -> (indexname -> typ option) * (indexname -> sort option)
wenzelm@19
    33
                  -> (indexname -> typ option) * (indexname -> sort option)
wenzelm@19
    34
                  -> (string*string)list
wenzelm@19
    35
                  -> (indexname*ctyp)list * (cterm*cterm)list
clasohm@0
    36
  val read_typ: sg * (indexname -> sort option) -> string -> typ
clasohm@0
    37
  val rep_cterm: cterm -> {T: typ, t: term, sign: sg, maxidx: int}
clasohm@0
    38
  val rep_ctyp: ctyp -> {T: typ, sign: sg}
clasohm@0
    39
  val rep_sg: sg -> {tsig: Type.type_sig,
wenzelm@19
    40
                     const_tab: typ Symtab.table,
wenzelm@19
    41
                     syn: Syntax.syntax,
wenzelm@19
    42
                     stamps: string ref list}
clasohm@0
    43
  val string_of_cterm: cterm -> string
clasohm@0
    44
  val string_of_ctyp: ctyp -> string
clasohm@0
    45
  val pprint_cterm: cterm -> pprint_args -> unit
clasohm@0
    46
  val pprint_ctyp: ctyp -> pprint_args -> unit
clasohm@0
    47
  val string_of_term: sg -> term -> string
clasohm@0
    48
  val string_of_typ: sg -> typ -> string
nipkow@206
    49
  val subsig: sg * sg -> bool
clasohm@0
    50
  val pprint_term: sg -> term -> pprint_args -> unit
clasohm@0
    51
  val pprint_typ: sg -> typ -> pprint_args -> unit
clasohm@0
    52
  val term_of: cterm -> term
clasohm@0
    53
  val typ_of: ctyp -> typ
clasohm@0
    54
  val pretty_term: sg -> term -> Syntax.Pretty.T
clasohm@0
    55
end;
clasohm@0
    56
nipkow@200
    57
functor SignFun(structure Type: TYPE and Syntax: SYNTAX) : SIGN =
wenzelm@143
    58
struct
clasohm@0
    59
clasohm@0
    60
structure Type = Type;
clasohm@0
    61
structure Symtab = Type.Symtab;
clasohm@0
    62
structure Syntax = Syntax;
clasohm@0
    63
structure Pretty = Syntax.Pretty
clasohm@0
    64
wenzelm@143
    65
wenzelm@143
    66
(* Signatures of theories. *)
wenzelm@143
    67
wenzelm@19
    68
datatype sg =
wenzelm@143
    69
  Sg of {
wenzelm@143
    70
    tsig: Type.type_sig,            (*order-sorted signature of types*)
wenzelm@143
    71
    const_tab: typ Symtab.table,    (*types of constants*)
wenzelm@143
    72
    syn: Syntax.syntax,             (*syntax for parsing and printing*)
wenzelm@143
    73
    stamps: string ref list};       (*unique theory indentifier*)
clasohm@0
    74
clasohm@0
    75
clasohm@0
    76
fun rep_sg (Sg args) = args;
clasohm@0
    77
nipkow@206
    78
fun subsig(Sg{stamps=s1,...},Sg{stamps=s2,...}) = s1 subset s2;
nipkow@206
    79
clasohm@0
    80
fun string_of_typ(Sg{tsig,syn,...}) = Syntax.string_of_typ syn;
clasohm@0
    81
clasohm@0
    82
fun pprint_typ(Sg{syn,...}) = Pretty.pprint o Pretty.quote o (Syntax.pretty_typ syn);
clasohm@0
    83
clasohm@0
    84
(*Is constant present in table with more generic type?*)
clasohm@0
    85
fun valid_const tsig ctab (a,T) = case Symtab.lookup(ctab, a) of
wenzelm@19
    86
        Some U => Type.typ_instance(tsig,T,U) | _ => false;
clasohm@0
    87
clasohm@0
    88
clasohm@0
    89
(*Check a term for errors.  Are all constants and types valid in signature?
clasohm@0
    90
  Does not check that term is well-typed!*)
wenzelm@19
    91
fun term_errors (sign as Sg{tsig,const_tab,...}) =
nipkow@200
    92
let val showtyp = string_of_typ sign
clasohm@0
    93
    fun terrs (Const (a,T), errs) =
wenzelm@19
    94
        if valid_const tsig const_tab (a,T)
nipkow@200
    95
        then Type.type_errors tsig (T,errs)
wenzelm@19
    96
        else ("Illegal type for constant: " ^ a ^ ": " ^ showtyp T) :: errs
nipkow@200
    97
      | terrs (Free (_,T), errs) = Type.type_errors tsig (T,errs)
clasohm@0
    98
      | terrs (Var  ((a,i),T), errs) =
nipkow@200
    99
        if  i>=0  then  Type.type_errors tsig (T,errs)
wenzelm@19
   100
        else  ("Negative index for Var: " ^ a) :: errs
clasohm@0
   101
      | terrs (Bound _, errs) = errs (*loose bvars detected by type_of*)
wenzelm@19
   102
      | terrs (Abs (_,T,t), errs) =
nipkow@200
   103
            Type.type_errors tsig (T,terrs(t,errs))
clasohm@0
   104
      | terrs (f$t, errs) = terrs(f, terrs (t,errs))
clasohm@0
   105
in  terrs  end;
clasohm@0
   106
clasohm@0
   107
wenzelm@169
   108
clasohm@0
   109
(** The Extend operation **)
clasohm@0
   110
wenzelm@169
   111
(* Extend a signature: may add classes, types and constants. The "ref" in
wenzelm@169
   112
   stamps ensures that no two signatures are identical -- it is impossible to
wenzelm@169
   113
   forge a signature. *)
wenzelm@169
   114
wenzelm@169
   115
fun extend (Sg {tsig, const_tab, syn, stamps}) name
nipkow@200
   116
  (classes, default, types, abbr, arities, const_decs, opt_sext) =
wenzelm@169
   117
  let
wenzelm@169
   118
    fun err_in_typ s = error ("The error(s) above occurred in type " ^ quote s);
wenzelm@169
   119
wenzelm@169
   120
    fun read_typ tsg sy s =
wenzelm@169
   121
      Syntax.read_typ sy (K (Type.defaultS tsg)) s handle ERROR => err_in_typ s;
wenzelm@169
   122
wenzelm@169
   123
    fun check_typ tsg sy ty =
nipkow@200
   124
      (case Type.type_errors tsg (ty, []) of
wenzelm@169
   125
        [] => ty
wenzelm@169
   126
      | errs => (prs (cat_lines errs); err_in_typ (Syntax.string_of_typ sy ty)));
wenzelm@169
   127
wenzelm@169
   128
    (*reset TVar indices to zero, renaming to preserve distinctness*)
wenzelm@169
   129
    fun zero_tvar_indices T =
wenzelm@169
   130
      let
wenzelm@169
   131
        val inxSs = typ_tvars T;
wenzelm@169
   132
        val nms' = variantlist (map (#1 o #1) inxSs, []);
wenzelm@169
   133
        val tye = map (fn ((v, S), a) => (v, TVar ((a, 0), S))) (inxSs ~~ nms');
wenzelm@169
   134
      in typ_subst_TVars tye T end;
wenzelm@169
   135
wenzelm@169
   136
    (*read and check the type mentioned in a const declaration; zero type var
wenzelm@169
   137
      indices because type inference requires it*)
wenzelm@169
   138
wenzelm@169
   139
    fun read_consts tsg sy (cs, s) =
wenzelm@169
   140
      let val ty = zero_tvar_indices (Type.varifyT (read_typ tsg sy s));
wenzelm@169
   141
      in
nipkow@200
   142
        (case Type.type_errors tsg (ty, []) of
wenzelm@169
   143
          [] => (cs, ty)
wenzelm@169
   144
        | errs => error (cat_lines (("Error in type of constants " ^
wenzelm@169
   145
            space_implode " " (map quote cs)) :: errs)))
wenzelm@169
   146
      end;
clasohm@0
   147
nipkow@155
   148
    val tsig' = Type.extend (tsig, classes, default, types, arities);
wenzelm@143
   149
nipkow@200
   150
    fun read_typ_abbr(a,v,s)=
nipkow@200
   151
      let val T = Type.varifyT(read_typ tsig' syn s)
nipkow@200
   152
      in (a,(v,T)) end handle ERROR => error("This error occured in abbreviation "^ quote a);
nipkow@200
   153
nipkow@200
   154
    val abbr' = map read_typ_abbr abbr;
nipkow@200
   155
    val tsig'' = Type.add_abbrs(tsig',abbr');
wenzelm@143
   156
wenzelm@169
   157
    val read_ty =
nipkow@200
   158
      (Type.expand_typ tsig'') o (check_typ tsig'' syn) o (read_typ tsig'' syn);
nipkow@200
   159
    val log_types = Type.logical_types tsig'';
nipkow@155
   160
    val xconsts = map #1 classes @ flat (map #1 types) @ flat (map #1 const_decs);
wenzelm@169
   161
    val sext = case opt_sext of Some sx => sx | None => Syntax.empty_sext;
wenzelm@169
   162
wenzelm@169
   163
    val syn' = Syntax.extend syn read_ty (log_types, xconsts, sext);
wenzelm@169
   164
wenzelm@169
   165
    val const_decs' =
nipkow@200
   166
      map (read_consts tsig'' syn') (Syntax.constants sext @ const_decs);
wenzelm@143
   167
  in
wenzelm@143
   168
    Sg {
nipkow@200
   169
      tsig = tsig'',
wenzelm@143
   170
      const_tab = Symtab.st_of_declist (const_decs', const_tab)
wenzelm@143
   171
        handle Symtab.DUPLICATE a => error ("Constant " ^ quote a ^ " declared twice"),
wenzelm@143
   172
      syn = syn',
wenzelm@169
   173
      stamps = ref name :: stamps}
wenzelm@143
   174
  end;
clasohm@0
   175
clasohm@0
   176
clasohm@0
   177
(* The empty signature *)
wenzelm@143
   178
wenzelm@169
   179
val sg0 = Sg {tsig = Type.tsig0, const_tab = Symtab.null,
wenzelm@169
   180
  syn = Syntax.type_syn, stamps = []};
clasohm@0
   181
wenzelm@143
   182
wenzelm@143
   183
(* The pure signature *)
wenzelm@143
   184
wenzelm@143
   185
val pure = extend sg0 "Pure"
clasohm@0
   186
([("logic", [])],
clasohm@0
   187
 ["logic"],
wenzelm@143
   188
 [(["fun"], 2),
wenzelm@143
   189
  (["prop"], 0),
wenzelm@143
   190
  (Syntax.syntax_types, 0)],
nipkow@200
   191
 [],
clasohm@0
   192
 [(["fun"],  ([["logic"], ["logic"]], "logic")),
clasohm@0
   193
  (["prop"], ([], "logic"))],
wenzelm@171
   194
 [([Syntax.constrainC], "'a::logic => 'a")],
wenzelm@143
   195
 Some Syntax.pure_sext);
wenzelm@143
   196
clasohm@0
   197
clasohm@0
   198
clasohm@0
   199
(** The Merge operation **)
clasohm@0
   200
clasohm@0
   201
(*Update table with (a,x) providing any existing asgt to "a" equals x. *)
clasohm@0
   202
fun update_eq ((a,x),tab) =
clasohm@0
   203
    case Symtab.lookup(tab,a) of
wenzelm@19
   204
        None => Symtab.update((a,x), tab)
wenzelm@19
   205
      | Some y => if x=y then tab
wenzelm@19
   206
            else  raise TERM ("Incompatible types for constant: "^a, []);
clasohm@0
   207
clasohm@0
   208
(*Combine tables, updating tab2 by tab1 and checking.*)
wenzelm@19
   209
fun merge_tabs (tab1,tab2) =
clasohm@0
   210
    Symtab.balance (foldr update_eq (Symtab.alist_of tab1, tab2));
clasohm@0
   211
clasohm@0
   212
(*Combine tables, overwriting tab2 with tab1.*)
wenzelm@19
   213
fun smash_tabs (tab1,tab2) =
clasohm@0
   214
    Symtab.balance (foldr Symtab.update (Symtab.alist_of tab1, tab2));
clasohm@0
   215
clasohm@0
   216
(*Combine stamps, checking that theory names are disjoint. *)
wenzelm@19
   217
fun merge_stamps (stamps1,stamps2) =
clasohm@0
   218
  let val stamps = stamps1 union stamps2 in
clasohm@0
   219
  case findrep (map ! stamps) of
clasohm@0
   220
     a::_ => error ("Attempt to merge different versions of theory: " ^ a)
clasohm@0
   221
   | [] => stamps
clasohm@0
   222
  end;
clasohm@0
   223
clasohm@0
   224
(*Merge two signatures.  Forms unions of tables.  Prefers sign1. *)
wenzelm@169
   225
fun merge
wenzelm@169
   226
  (sign1 as Sg {tsig = tsig1, const_tab = ctab1, stamps = stamps1, syn = syn1},
wenzelm@169
   227
   sign2 as Sg {tsig = tsig2, const_tab = ctab2, stamps = stamps2, syn = syn2}) =
clasohm@0
   228
    if stamps2 subset stamps1 then sign1
clasohm@0
   229
    else if stamps1 subset stamps2 then sign2
wenzelm@169
   230
    else (*neither is union already; must form union*)
wenzelm@169
   231
      let val tsig = Type.merge (tsig1, tsig2);
wenzelm@169
   232
      in
wenzelm@169
   233
        Sg {tsig = tsig, const_tab = merge_tabs (ctab1, ctab2),
wenzelm@169
   234
          stamps = merge_stamps (stamps1, stamps2),
wenzelm@169
   235
          syn = Syntax.merge (Type.logical_types tsig) syn1 syn2}
wenzelm@169
   236
      end;
wenzelm@169
   237
clasohm@0
   238
clasohm@0
   239
clasohm@0
   240
(**** CERTIFIED TYPES ****)
clasohm@0
   241
clasohm@0
   242
clasohm@0
   243
(*Certified typs under a signature*)
clasohm@0
   244
datatype ctyp = Ctyp of {sign: sg,  T: typ};
clasohm@0
   245
clasohm@0
   246
fun rep_ctyp(Ctyp ctyp) = ctyp;
clasohm@0
   247
clasohm@0
   248
fun typ_of (Ctyp{sign,T}) = T;
clasohm@0
   249
clasohm@0
   250
fun ctyp_of (sign as Sg{tsig,...}) T =
nipkow@200
   251
        case Type.type_errors tsig (T,[]) of
wenzelm@19
   252
          [] => Ctyp{sign= sign,T= T}
wenzelm@19
   253
        | errs =>  error (cat_lines ("Error in type:" :: errs));
clasohm@0
   254
clasohm@0
   255
(*The only use is a horrible hack in the simplifier!*)
clasohm@0
   256
fun read_typ(Sg{tsig,syn,...}, defS) s =
clasohm@0
   257
    let val term = Syntax.read syn Syntax.typeT s;
wenzelm@19
   258
        val S0 = Type.defaultS tsig;
wenzelm@19
   259
        fun defS0 s = case defS s of Some S => S | None => S0;
clasohm@0
   260
    in Syntax.typ_of_term defS0 term end;
clasohm@0
   261
clasohm@0
   262
fun read_ctyp sign = ctyp_of sign o read_typ(sign, K None);
clasohm@0
   263
clasohm@0
   264
fun string_of_ctyp (Ctyp{sign,T}) = string_of_typ sign T;
clasohm@0
   265
clasohm@0
   266
fun pprint_ctyp (Ctyp{sign,T}) = pprint_typ sign T;
clasohm@0
   267
clasohm@0
   268
clasohm@0
   269
(**** CERTIFIED TERMS ****)
clasohm@0
   270
clasohm@0
   271
(*Certified terms under a signature, with checked typ and maxidx of Vars*)
clasohm@0
   272
datatype cterm = Cterm of {sign: sg,  t: term,  T: typ,  maxidx: int};
clasohm@0
   273
clasohm@0
   274
fun rep_cterm (Cterm args) = args;
clasohm@0
   275
clasohm@0
   276
(*Return the underlying term*)
clasohm@0
   277
fun term_of (Cterm{sign,t,T,maxidx}) = t;
clasohm@0
   278
clasohm@0
   279
(** pretty printing of terms **)
clasohm@0
   280
clasohm@0
   281
fun pretty_term (Sg{tsig,syn,...}) = Syntax.pretty_term syn;
clasohm@0
   282
clasohm@0
   283
fun string_of_term sign t = Pretty.string_of (pretty_term sign t);
clasohm@0
   284
clasohm@0
   285
fun pprint_term sign = Pretty.pprint o Pretty.quote o (pretty_term sign);
clasohm@0
   286
clasohm@0
   287
fun string_of_cterm (Cterm{sign,t,...}) = string_of_term sign t;
clasohm@0
   288
clasohm@0
   289
fun pprint_cterm (Cterm{sign,t,...}) = pprint_term sign t;
clasohm@0
   290
clasohm@0
   291
(*Create a cterm by checking a "raw" term with respect to a signature*)
clasohm@0
   292
fun cterm_of sign t =
clasohm@0
   293
  case  term_errors sign (t,[])  of
clasohm@0
   294
      [] => Cterm{sign=sign, t=t, T= type_of t, maxidx= maxidx_of_term t}
clasohm@0
   295
    | errs => raise TERM(cat_lines("Term not in signature"::errs), [t]);
clasohm@0
   296
clasohm@0
   297
fun cfun f = fn Cterm{sign,t,...} => cterm_of sign (f t);
clasohm@0
   298
clasohm@0
   299
(*Lexing, parsing, polymorphic typechecking of a term.*)
clasohm@0
   300
fun read_def_cterm (sign as Sg{tsig, const_tab, syn,...}, types, sorts)
wenzelm@19
   301
                   (a,T) =
clasohm@0
   302
  let val showtyp = string_of_typ sign
clasohm@0
   303
      and showterm = string_of_term sign
clasohm@0
   304
      fun termerr [] = ""
wenzelm@19
   305
        | termerr [t] = "\nInvolving this term:\n" ^ showterm t ^ "\n"
wenzelm@19
   306
        | termerr ts = "\nInvolving these terms:\n" ^
wenzelm@19
   307
                       cat_lines (map showterm ts)
clasohm@0
   308
      val t = Syntax.read syn T a;
clasohm@0
   309
      val (t',tye) = Type.infer_types (tsig, const_tab, types,
wenzelm@19
   310
                                       sorts, showtyp, T, t)
wenzelm@19
   311
                  handle TYPE (msg, Ts, ts) =>
wenzelm@19
   312
          error ("Type checking error: " ^ msg ^ "\n" ^
wenzelm@19
   313
                  cat_lines (map showtyp Ts) ^ termerr ts)
clasohm@0
   314
  in (cterm_of sign t', tye)
clasohm@0
   315
  end
clasohm@0
   316
  handle TERM (msg, _) => error ("Error: " ^  msg);
clasohm@0
   317
clasohm@0
   318
clasohm@0
   319
fun read_cterm sign = #1 o (read_def_cterm (sign, K None, K None));
clasohm@0
   320
clasohm@0
   321
(** reading of instantiations **)
clasohm@0
   322
clasohm@0
   323
fun indexname cs = case Syntax.scan_varname cs of (v,[]) => v
wenzelm@19
   324
        | _ => error("Lexical error in variable name " ^ quote (implode cs));
clasohm@0
   325
clasohm@0
   326
fun absent ixn =
clasohm@0
   327
  error("No such variable in term: " ^ Syntax.string_of_vname ixn);
clasohm@0
   328
clasohm@0
   329
fun inst_failure ixn =
clasohm@0
   330
  error("Instantiation of " ^ Syntax.string_of_vname ixn ^ " fails");
clasohm@0
   331
clasohm@0
   332
fun read_insts (sign as Sg{tsig,...}) (rtypes,rsorts) (types,sorts) insts =
clasohm@0
   333
let fun split([],tvs,vs) = (tvs,vs)
clasohm@0
   334
      | split((sv,st)::l,tvs,vs) = (case explode sv of
wenzelm@19
   335
                  "'"::cs => split(l,(indexname cs,st)::tvs,vs)
wenzelm@19
   336
                | cs => split(l,tvs,(indexname cs,st)::vs));
clasohm@0
   337
    val (tvs,vs) = split(insts,[],[]);
clasohm@0
   338
    fun readT((a,i),st) =
wenzelm@19
   339
        let val ixn = ("'" ^ a,i);
wenzelm@19
   340
            val S = case rsorts ixn of Some S => S | None => absent ixn;
wenzelm@19
   341
            val T = read_typ (sign,sorts) st;
wenzelm@19
   342
        in if Type.typ_instance(tsig,T,TVar(ixn,S)) then (ixn,T)
wenzelm@19
   343
           else inst_failure ixn
wenzelm@19
   344
        end
clasohm@0
   345
    val tye = map readT tvs;
clasohm@0
   346
    fun add_cterm ((cts,tye), (ixn,st)) =
wenzelm@19
   347
        let val T = case rtypes ixn of
wenzelm@19
   348
                      Some T => typ_subst_TVars tye T
wenzelm@19
   349
                    | None => absent ixn;
wenzelm@19
   350
            val (ct,tye2) = read_def_cterm (sign,types,sorts) (st,T);
nipkow@200
   351
            val cv = cterm_of sign (Var(ixn,typ_subst_TVars tye2 T))
nipkow@200
   352
        in ((cv,ct)::cts,tye2 @ tye) end
clasohm@0
   353
    val (cterms,tye') = foldl add_cterm (([],tye), vs);
nipkow@200
   354
in (map (fn (ixn,T) => (ixn,ctyp_of sign T)) tye', cterms) end;
clasohm@0
   355
clasohm@0
   356
end;
wenzelm@143
   357