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