author  lcp 
Tue, 18 Jan 1994 13:46:08 +0100  
changeset 229  4002c4cd450c 
parent 224  d762f9421933 
child 251  c9b984c0a674 
permissions  rwrr 
19  1 
(* Title: Pure/sign.ML 
0  2 
ID: $Id$ 
19  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
224
diff
changeset

4 
Copyright 1994 University of Cambridge 
0  5 

229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
224
diff
changeset

6 
The abstract types "sg" of signatures 
0  7 
*) 
8 

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

12 
structure Symtab: SYMTAB 

13 
structure Syntax: SYNTAX 

143  14 
sharing Symtab = Type.Symtab 
0  15 
type sg 
16 
val extend: sg > string > 

19  17 
(class * class list) list * class list * 
18 
(string list * int) list * 

200  19 
(string * indexname list * string) list * 
19  20 
(string list * (sort list * class)) list * 
21 
(string list * string)list * Syntax.sext option > sg 

0  22 
val merge: sg * sg > sg 
23 
val pure: sg 

24 
val read_typ: sg * (indexname > sort option) > string > typ 

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

19  26 
const_tab: typ Symtab.table, 
27 
syn: Syntax.syntax, 

28 
stamps: string ref list} 

0  29 
val string_of_term: sg > term > string 
30 
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

31 
val subsig: sg * sg > bool 
0  32 
val pprint_term: sg > term > pprint_args > unit 
33 
val pprint_typ: sg > typ > pprint_args > unit 

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

229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
224
diff
changeset

35 
val term_errors: sg > term > string list 
0  36 
end; 
37 

200  38 
functor SignFun(structure Type: TYPE and Syntax: SYNTAX) : SIGN = 
143  39 
struct 
0  40 

41 
structure Type = Type; 

42 
structure Symtab = Type.Symtab; 

43 
structure Syntax = Syntax; 

44 
structure Pretty = Syntax.Pretty 

45 

143  46 

47 
(* Signatures of theories. *) 

48 

19  49 
datatype sg = 
143  50 
Sg of { 
51 
tsig: Type.type_sig, (*ordersorted signature of types*) 

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

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

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

0  55 

56 

57 
fun rep_sg (Sg args) = args; 

58 

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

59 
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

60 

0  61 
fun string_of_typ(Sg{tsig,syn,...}) = Syntax.string_of_typ syn; 
62 

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

64 

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

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

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

69 

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

71 
Does not check that term is welltyped!*) 

19  72 
fun term_errors (sign as Sg{tsig,const_tab,...}) = 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
224
diff
changeset

73 
let val showtyp = string_of_typ sign 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
224
diff
changeset

74 
fun terrs (Const (a,T), errs) = 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
224
diff
changeset

75 
if valid_const tsig const_tab (a,T) 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
224
diff
changeset

76 
then Type.type_errors tsig (T,errs) 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
224
diff
changeset

77 
else ("Illegal type for constant: " ^ a ^ ": " ^ showtyp T) :: errs 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
224
diff
changeset

78 
 terrs (Free (_,T), errs) = Type.type_errors tsig (T,errs) 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
224
diff
changeset

79 
 terrs (Var ((a,i),T), errs) = 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
224
diff
changeset

80 
if i>=0 then Type.type_errors tsig (T,errs) 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
224
diff
changeset

81 
else ("Negative index for Var: " ^ a) :: errs 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
224
diff
changeset

82 
 terrs (Bound _, errs) = errs (*loose bvars detected by type_of*) 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
224
diff
changeset

83 
 terrs (Abs (_,T,t), errs) = 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
224
diff
changeset

84 
Type.type_errors tsig (T,terrs(t,errs)) 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
224
diff
changeset

85 
 terrs (f$t, errs) = terrs(f, terrs (t,errs)) 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
224
diff
changeset

86 
in fn t => terrs(t,[]) end; 
0  87 

88 

169  89 

0  90 
(** The Extend operation **) 
91 

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

94 
forge a signature. *) 

95 

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

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

100 

101 
fun read_typ tsg sy s = 

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

103 

104 
fun check_typ tsg sy ty = 

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

108 

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

110 
fun zero_tvar_indices T = 

111 
let 

112 
val inxSs = typ_tvars T; 

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

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

115 
in typ_subst_TVars tye T end; 

116 

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

118 
indices because type inference requires it*) 

119 

120 
fun read_consts tsg sy (cs, s) = 

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

122 
in 

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

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

127 
end; 

0  128 

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

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

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

134 

135 
val abbr' = map read_typ_abbr abbr; 

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

143  137 

169  138 
val read_ty = 
200  139 
(Type.expand_typ tsig'') o (check_typ tsig'' syn) o (read_typ tsig'' syn); 
140 
val log_types = Type.logical_types tsig''; 

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

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

145 

146 
val const_decs' = 

200  147 
map (read_consts tsig'' syn') (Syntax.constants sext @ const_decs); 
143  148 
in 
149 
Sg { 

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

153 
syn = syn', 

169  154 
stamps = ref name :: stamps} 
143  155 
end; 
0  156 

157 

158 
(* The empty signature *) 

143  159 

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

0  162 

143  163 

164 
(* The pure signature *) 

165 

166 
val pure = extend sg0 "Pure" 

0  167 
([("logic", [])], 
168 
["logic"], 

143  169 
[(["fun"], 2), 
170 
(["prop"], 0), 

171 
(Syntax.syntax_types, 0)], 

200  172 
[], 
0  173 
[(["fun"], ([["logic"], ["logic"]], "logic")), 
174 
(["prop"], ([], "logic"))], 

171  175 
[([Syntax.constrainC], "'a::logic => 'a")], 
143  176 
Some Syntax.pure_sext); 
177 

0  178 

179 

180 
(** The Merge operation **) 

181 

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

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

184 
case Symtab.lookup(tab,a) of 

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

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

0  188 

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

19  190 
fun merge_tabs (tab1,tab2) = 
0  191 
Symtab.balance (foldr update_eq (Symtab.alist_of tab1, tab2)); 
192 

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

19  194 
fun smash_tabs (tab1,tab2) = 
0  195 
Symtab.balance (foldr Symtab.update (Symtab.alist_of tab1, tab2)); 
196 

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

19  198 
fun merge_stamps (stamps1,stamps2) = 
0  199 
let val stamps = stamps1 union stamps2 in 
200 
case findrep (map ! stamps) of 

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

202 
 [] => stamps 

203 
end; 

204 

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

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

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

0  209 
if stamps2 subset stamps1 then sign1 
210 
else if stamps1 subset stamps2 then sign2 

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

213 
in 

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

215 
stamps = merge_stamps (stamps1, stamps2), 

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

217 
end; 

218 

0  219 

220 

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

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

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

0  225 
in Syntax.typ_of_term defS0 term end; 
226 

227 
(** pretty printing of terms **) 

228 

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

230 

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

232 

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

234 

235 
end; 

143  236 