author  nipkow 
Tue, 04 Jan 1994 17:03:52 +0100  
changeset 211  7ab45715c0a6 
parent 206  0d624d1ba9cc 
child 224  d762f9421933 
permissions  rwrr 
19  1 
(* Title: Pure/sign.ML 
0  2 
ID: $Id$ 
19  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
0  4 
Copyright 1992 University of Cambridge 
5 

143  6 
The abstract types "sg" (signatures) and "cterm" / "ctyp" (certified terms / 
7 
typs under a signature). 

0  8 
*) 
9 

19  10 
signature SIGN = 
0  11 
sig 
12 
structure Type: TYPE 

13 
structure Symtab: SYMTAB 

14 
structure Syntax: SYNTAX 

143  15 
sharing Symtab = Type.Symtab 
0  16 
type sg 
17 
type cterm 

18 
type ctyp 

19 
val cfun: (term > term) > (cterm > cterm) 

20 
val cterm_of: sg > term > cterm 

21 
val ctyp_of: sg > typ > ctyp 

22 
val extend: sg > string > 

19  23 
(class * class list) list * class list * 
24 
(string list * int) list * 

200  25 
(string * indexname list * string) list * 
19  26 
(string list * (sort list * class)) list * 
27 
(string list * string)list * Syntax.sext option > sg 

0  28 
val merge: sg * sg > sg 
29 
val pure: sg 

30 
val read_cterm: sg > string * typ > cterm 

31 
val read_ctyp: sg > string > ctyp 

32 
val read_insts: sg > (indexname > typ option) * (indexname > sort option) 

19  33 
> (indexname > typ option) * (indexname > sort option) 
34 
> (string*string)list 

35 
> (indexname*ctyp)list * (cterm*cterm)list 

0  36 
val read_typ: sg * (indexname > sort option) > string > typ 
37 
val rep_cterm: cterm > {T: typ, t: term, sign: sg, maxidx: int} 

38 
val rep_ctyp: ctyp > {T: typ, sign: sg} 

39 
val rep_sg: sg > {tsig: Type.type_sig, 

19  40 
const_tab: typ Symtab.table, 
41 
syn: Syntax.syntax, 

42 
stamps: string ref list} 

0  43 
val string_of_cterm: cterm > string 
44 
val string_of_ctyp: ctyp > string 

45 
val pprint_cterm: cterm > pprint_args > unit 

46 
val pprint_ctyp: ctyp > pprint_args > unit 

47 
val string_of_term: sg > term > string 

48 
val string_of_typ: sg > typ > string 

206
0d624d1ba9cc
added subsig: sg * sg > bool to test if one signature is contained in another.
nipkow
parents:
200
diff
changeset

49 
val subsig: sg * sg > bool 
0  50 
val pprint_term: sg > term > pprint_args > unit 
51 
val pprint_typ: sg > typ > pprint_args > unit 

52 
val term_of: cterm > term 

53 
val typ_of: ctyp > typ 

54 
val pretty_term: sg > term > Syntax.Pretty.T 

211  55 
val fake_cterm_of: sg > term > cterm 
0  56 
end; 
57 

200  58 
functor SignFun(structure Type: TYPE and Syntax: SYNTAX) : SIGN = 
143  59 
struct 
0  60 

61 
structure Type = Type; 

62 
structure Symtab = Type.Symtab; 

63 
structure Syntax = Syntax; 

64 
structure Pretty = Syntax.Pretty 

65 

143  66 

67 
(* Signatures of theories. *) 

68 

19  69 
datatype sg = 
143  70 
Sg of { 
71 
tsig: Type.type_sig, (*ordersorted signature of types*) 

72 
const_tab: typ Symtab.table, (*types of constants*) 

73 
syn: Syntax.syntax, (*syntax for parsing and printing*) 

74 
stamps: string ref list}; (*unique theory indentifier*) 

0  75 

76 

77 
fun rep_sg (Sg args) = args; 

78 

206
0d624d1ba9cc
added subsig: sg * sg > bool to test if one signature is contained in another.
nipkow
parents:
200
diff
changeset

79 
fun subsig(Sg{stamps=s1,...},Sg{stamps=s2,...}) = s1 subset s2; 
0d624d1ba9cc
added subsig: sg * sg > bool to test if one signature is contained in another.
nipkow
parents:
200
diff
changeset

80 

0  81 
fun string_of_typ(Sg{tsig,syn,...}) = Syntax.string_of_typ syn; 
82 

83 
fun pprint_typ(Sg{syn,...}) = Pretty.pprint o Pretty.quote o (Syntax.pretty_typ syn); 

84 

85 
(*Is constant present in table with more generic type?*) 

86 
fun valid_const tsig ctab (a,T) = case Symtab.lookup(ctab, a) of 

19  87 
Some U => Type.typ_instance(tsig,T,U)  _ => false; 
0  88 

89 

90 
(*Check a term for errors. Are all constants and types valid in signature? 

91 
Does not check that term is welltyped!*) 

19  92 
fun term_errors (sign as Sg{tsig,const_tab,...}) = 
200  93 
let val showtyp = string_of_typ sign 
0  94 
fun terrs (Const (a,T), errs) = 
19  95 
if valid_const tsig const_tab (a,T) 
200  96 
then Type.type_errors tsig (T,errs) 
19  97 
else ("Illegal type for constant: " ^ a ^ ": " ^ showtyp T) :: errs 
200  98 
 terrs (Free (_,T), errs) = Type.type_errors tsig (T,errs) 
0  99 
 terrs (Var ((a,i),T), errs) = 
200  100 
if i>=0 then Type.type_errors tsig (T,errs) 
19  101 
else ("Negative index for Var: " ^ a) :: errs 
0  102 
 terrs (Bound _, errs) = errs (*loose bvars detected by type_of*) 
19  103 
 terrs (Abs (_,T,t), errs) = 
200  104 
Type.type_errors tsig (T,terrs(t,errs)) 
0  105 
 terrs (f$t, errs) = terrs(f, terrs (t,errs)) 
106 
in terrs end; 

107 

108 

169  109 

0  110 
(** The Extend operation **) 
111 

169  112 
(* Extend a signature: may add classes, types and constants. The "ref" in 
113 
stamps ensures that no two signatures are identical  it is impossible to 

114 
forge a signature. *) 

115 

116 
fun extend (Sg {tsig, const_tab, syn, stamps}) name 

200  117 
(classes, default, types, abbr, arities, const_decs, opt_sext) = 
169  118 
let 
119 
fun err_in_typ s = error ("The error(s) above occurred in type " ^ quote s); 

120 

121 
fun read_typ tsg sy s = 

122 
Syntax.read_typ sy (K (Type.defaultS tsg)) s handle ERROR => err_in_typ s; 

123 

124 
fun check_typ tsg sy ty = 

200  125 
(case Type.type_errors tsg (ty, []) of 
169  126 
[] => ty 
127 
 errs => (prs (cat_lines errs); err_in_typ (Syntax.string_of_typ sy ty))); 

128 

129 
(*reset TVar indices to zero, renaming to preserve distinctness*) 

130 
fun zero_tvar_indices T = 

131 
let 

132 
val inxSs = typ_tvars T; 

133 
val nms' = variantlist (map (#1 o #1) inxSs, []); 

134 
val tye = map (fn ((v, S), a) => (v, TVar ((a, 0), S))) (inxSs ~~ nms'); 

135 
in typ_subst_TVars tye T end; 

136 

137 
(*read and check the type mentioned in a const declaration; zero type var 

138 
indices because type inference requires it*) 

139 

140 
fun read_consts tsg sy (cs, s) = 

141 
let val ty = zero_tvar_indices (Type.varifyT (read_typ tsg sy s)); 

142 
in 

200  143 
(case Type.type_errors tsg (ty, []) of 
169  144 
[] => (cs, ty) 
145 
 errs => error (cat_lines (("Error in type of constants " ^ 

146 
space_implode " " (map quote cs)) :: errs))) 

147 
end; 

0  148 

155  149 
val tsig' = Type.extend (tsig, classes, default, types, arities); 
143  150 

200  151 
fun read_typ_abbr(a,v,s)= 
152 
let val T = Type.varifyT(read_typ tsig' syn s) 

153 
in (a,(v,T)) end handle ERROR => error("This error occured in abbreviation "^ quote a); 

154 

155 
val abbr' = map read_typ_abbr abbr; 

156 
val tsig'' = Type.add_abbrs(tsig',abbr'); 

143  157 

169  158 
val read_ty = 
200  159 
(Type.expand_typ tsig'') o (check_typ tsig'' syn) o (read_typ tsig'' syn); 
160 
val log_types = Type.logical_types tsig''; 

155  161 
val xconsts = map #1 classes @ flat (map #1 types) @ flat (map #1 const_decs); 
169  162 
val sext = case opt_sext of Some sx => sx  None => Syntax.empty_sext; 
163 

164 
val syn' = Syntax.extend syn read_ty (log_types, xconsts, sext); 

165 

166 
val const_decs' = 

200  167 
map (read_consts tsig'' syn') (Syntax.constants sext @ const_decs); 
143  168 
in 
169 
Sg { 

200  170 
tsig = tsig'', 
143  171 
const_tab = Symtab.st_of_declist (const_decs', const_tab) 
172 
handle Symtab.DUPLICATE a => error ("Constant " ^ quote a ^ " declared twice"), 

173 
syn = syn', 

169  174 
stamps = ref name :: stamps} 
143  175 
end; 
0  176 

177 

178 
(* The empty signature *) 

143  179 

169  180 
val sg0 = Sg {tsig = Type.tsig0, const_tab = Symtab.null, 
181 
syn = Syntax.type_syn, stamps = []}; 

0  182 

143  183 

184 
(* The pure signature *) 

185 

186 
val pure = extend sg0 "Pure" 

0  187 
([("logic", [])], 
188 
["logic"], 

143  189 
[(["fun"], 2), 
190 
(["prop"], 0), 

191 
(Syntax.syntax_types, 0)], 

200  192 
[], 
0  193 
[(["fun"], ([["logic"], ["logic"]], "logic")), 
194 
(["prop"], ([], "logic"))], 

171  195 
[([Syntax.constrainC], "'a::logic => 'a")], 
143  196 
Some Syntax.pure_sext); 
197 

0  198 

199 

200 
(** The Merge operation **) 

201 

202 
(*Update table with (a,x) providing any existing asgt to "a" equals x. *) 

203 
fun update_eq ((a,x),tab) = 

204 
case Symtab.lookup(tab,a) of 

19  205 
None => Symtab.update((a,x), tab) 
206 
 Some y => if x=y then tab 

207 
else raise TERM ("Incompatible types for constant: "^a, []); 

0  208 

209 
(*Combine tables, updating tab2 by tab1 and checking.*) 

19  210 
fun merge_tabs (tab1,tab2) = 
0  211 
Symtab.balance (foldr update_eq (Symtab.alist_of tab1, tab2)); 
212 

213 
(*Combine tables, overwriting tab2 with tab1.*) 

19  214 
fun smash_tabs (tab1,tab2) = 
0  215 
Symtab.balance (foldr Symtab.update (Symtab.alist_of tab1, tab2)); 
216 

217 
(*Combine stamps, checking that theory names are disjoint. *) 

19  218 
fun merge_stamps (stamps1,stamps2) = 
0  219 
let val stamps = stamps1 union stamps2 in 
220 
case findrep (map ! stamps) of 

221 
a::_ => error ("Attempt to merge different versions of theory: " ^ a) 

222 
 [] => stamps 

223 
end; 

224 

225 
(*Merge two signatures. Forms unions of tables. Prefers sign1. *) 

169  226 
fun merge 
227 
(sign1 as Sg {tsig = tsig1, const_tab = ctab1, stamps = stamps1, syn = syn1}, 

228 
sign2 as Sg {tsig = tsig2, const_tab = ctab2, stamps = stamps2, syn = syn2}) = 

0  229 
if stamps2 subset stamps1 then sign1 
230 
else if stamps1 subset stamps2 then sign2 

169  231 
else (*neither is union already; must form union*) 
232 
let val tsig = Type.merge (tsig1, tsig2); 

233 
in 

234 
Sg {tsig = tsig, const_tab = merge_tabs (ctab1, ctab2), 

235 
stamps = merge_stamps (stamps1, stamps2), 

236 
syn = Syntax.merge (Type.logical_types tsig) syn1 syn2} 

237 
end; 

238 

0  239 

240 

241 
(**** CERTIFIED TYPES ****) 

242 

243 

244 
(*Certified typs under a signature*) 

245 
datatype ctyp = Ctyp of {sign: sg, T: typ}; 

246 

247 
fun rep_ctyp(Ctyp ctyp) = ctyp; 

248 

249 
fun typ_of (Ctyp{sign,T}) = T; 

250 

251 
fun ctyp_of (sign as Sg{tsig,...}) T = 

200  252 
case Type.type_errors tsig (T,[]) of 
19  253 
[] => Ctyp{sign= sign,T= T} 
254 
 errs => error (cat_lines ("Error in type:" :: errs)); 

0  255 

256 
(*The only use is a horrible hack in the simplifier!*) 

257 
fun read_typ(Sg{tsig,syn,...}, defS) s = 

258 
let val term = Syntax.read syn Syntax.typeT s; 

19  259 
val S0 = Type.defaultS tsig; 
260 
fun defS0 s = case defS s of Some S => S  None => S0; 

0  261 
in Syntax.typ_of_term defS0 term end; 
262 

263 
fun read_ctyp sign = ctyp_of sign o read_typ(sign, K None); 

264 

265 
fun string_of_ctyp (Ctyp{sign,T}) = string_of_typ sign T; 

266 

267 
fun pprint_ctyp (Ctyp{sign,T}) = pprint_typ sign T; 

268 

269 

270 
(**** CERTIFIED TERMS ****) 

271 

272 
(*Certified terms under a signature, with checked typ and maxidx of Vars*) 

273 
datatype cterm = Cterm of {sign: sg, t: term, T: typ, maxidx: int}; 

274 

275 
fun rep_cterm (Cterm args) = args; 

276 

277 
(*Return the underlying term*) 

278 
fun term_of (Cterm{sign,t,T,maxidx}) = t; 

279 

280 
(** pretty printing of terms **) 

281 

282 
fun pretty_term (Sg{tsig,syn,...}) = Syntax.pretty_term syn; 

283 

284 
fun string_of_term sign t = Pretty.string_of (pretty_term sign t); 

285 

286 
fun pprint_term sign = Pretty.pprint o Pretty.quote o (pretty_term sign); 

287 

288 
fun string_of_cterm (Cterm{sign,t,...}) = string_of_term sign t; 

289 

290 
fun pprint_cterm (Cterm{sign,t,...}) = pprint_term sign t; 

291 

292 
(*Create a cterm by checking a "raw" term with respect to a signature*) 

293 
fun cterm_of sign t = 

294 
case term_errors sign (t,[]) of 

295 
[] => Cterm{sign=sign, t=t, T= type_of t, maxidx= maxidx_of_term t} 

296 
 errs => raise TERM(cat_lines("Term not in signature"::errs), [t]); 

297 

211  298 
fun fake_cterm_of sign t = 
299 
Cterm{sign=sign, t=t, T= fastype_of t, maxidx= maxidx_of_term t} 

300 

0  301 
fun cfun f = fn Cterm{sign,t,...} => cterm_of sign (f t); 
302 

303 
(*Lexing, parsing, polymorphic typechecking of a term.*) 

304 
fun read_def_cterm (sign as Sg{tsig, const_tab, syn,...}, types, sorts) 

19  305 
(a,T) = 
0  306 
let val showtyp = string_of_typ sign 
307 
and showterm = string_of_term sign 

308 
fun termerr [] = "" 

19  309 
 termerr [t] = "\nInvolving this term:\n" ^ showterm t ^ "\n" 
310 
 termerr ts = "\nInvolving these terms:\n" ^ 

311 
cat_lines (map showterm ts) 

0  312 
val t = Syntax.read syn T a; 
313 
val (t',tye) = Type.infer_types (tsig, const_tab, types, 

19  314 
sorts, showtyp, T, t) 
315 
handle TYPE (msg, Ts, ts) => 

316 
error ("Type checking error: " ^ msg ^ "\n" ^ 

317 
cat_lines (map showtyp Ts) ^ termerr ts) 

0  318 
in (cterm_of sign t', tye) 
319 
end 

320 
handle TERM (msg, _) => error ("Error: " ^ msg); 

321 

322 

323 
fun read_cterm sign = #1 o (read_def_cterm (sign, K None, K None)); 

324 

325 
(** reading of instantiations **) 

326 

327 
fun indexname cs = case Syntax.scan_varname cs of (v,[]) => v 

19  328 
 _ => error("Lexical error in variable name " ^ quote (implode cs)); 
0  329 

330 
fun absent ixn = 

331 
error("No such variable in term: " ^ Syntax.string_of_vname ixn); 

332 

333 
fun inst_failure ixn = 

334 
error("Instantiation of " ^ Syntax.string_of_vname ixn ^ " fails"); 

335 

336 
fun read_insts (sign as Sg{tsig,...}) (rtypes,rsorts) (types,sorts) insts = 

337 
let fun split([],tvs,vs) = (tvs,vs) 

338 
 split((sv,st)::l,tvs,vs) = (case explode sv of 

19  339 
"'"::cs => split(l,(indexname cs,st)::tvs,vs) 
340 
 cs => split(l,tvs,(indexname cs,st)::vs)); 

0  341 
val (tvs,vs) = split(insts,[],[]); 
342 
fun readT((a,i),st) = 

19  343 
let val ixn = ("'" ^ a,i); 
344 
val S = case rsorts ixn of Some S => S  None => absent ixn; 

345 
val T = read_typ (sign,sorts) st; 

346 
in if Type.typ_instance(tsig,T,TVar(ixn,S)) then (ixn,T) 

347 
else inst_failure ixn 

348 
end 

0  349 
val tye = map readT tvs; 
350 
fun add_cterm ((cts,tye), (ixn,st)) = 

19  351 
let val T = case rtypes ixn of 
352 
Some T => typ_subst_TVars tye T 

353 
 None => absent ixn; 

354 
val (ct,tye2) = read_def_cterm (sign,types,sorts) (st,T); 

200  355 
val cv = cterm_of sign (Var(ixn,typ_subst_TVars tye2 T)) 
356 
in ((cv,ct)::cts,tye2 @ tye) end 

0  357 
val (cterms,tye') = foldl add_cterm (([],tye), vs); 
200  358 
in (map (fn (ixn,T) => (ixn,ctyp_of sign T)) tye', cterms) end; 
0  359 

360 
end; 

143  361 