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