|
1 (* Title: Pure/theory.ML |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson and Markus Wenzel |
|
4 Copyright 1996 University of Cambridge |
|
5 |
|
6 Theories |
|
7 *) |
|
8 |
|
9 signature THEORY = |
|
10 sig |
|
11 type theory |
|
12 exception THEORY of string * theory list |
|
13 val rep_theory : theory -> |
|
14 {sign: Sign.sg, new_axioms: term Symtab.table, parents: theory list} |
|
15 val sign_of : theory -> Sign.sg |
|
16 val syn_of : theory -> Syntax.syntax |
|
17 val stamps_of_thy : theory -> string ref list |
|
18 val parents_of : theory -> theory list |
|
19 val subthy : theory * theory -> bool |
|
20 val eq_thy : theory * theory -> bool |
|
21 val proto_pure_thy : theory |
|
22 val pure_thy : theory |
|
23 val cpure_thy : theory |
|
24 (*theory primitives*) |
|
25 val add_classes : (class * class list) list -> theory -> theory |
|
26 val add_classrel : (class * class) list -> theory -> theory |
|
27 val add_defsort : sort -> theory -> theory |
|
28 val add_types : (string * int * mixfix) list -> theory -> theory |
|
29 val add_tyabbrs : (string * string list * string * mixfix) list |
|
30 -> theory -> theory |
|
31 val add_tyabbrs_i : (string * string list * typ * mixfix) list |
|
32 -> theory -> theory |
|
33 val add_arities : (string * sort list * sort) list -> theory -> theory |
|
34 val add_consts : (string * string * mixfix) list -> theory -> theory |
|
35 val add_consts_i : (string * typ * mixfix) list -> theory -> theory |
|
36 val add_syntax : (string * string * mixfix) list -> theory -> theory |
|
37 val add_syntax_i : (string * typ * mixfix) list -> theory -> theory |
|
38 val add_trfuns : |
|
39 (string * (Syntax.ast list -> Syntax.ast)) list * |
|
40 (string * (term list -> term)) list * |
|
41 (string * (term list -> term)) list * |
|
42 (string * (Syntax.ast list -> Syntax.ast)) list -> theory -> theory |
|
43 val add_trrules : (string * string)Syntax.trrule list -> theory -> theory |
|
44 val add_trrules_i : Syntax.ast Syntax.trrule list -> theory -> theory |
|
45 val cert_axm : Sign.sg -> string * term -> string * term |
|
46 val read_axm : Sign.sg -> string * string -> string * term |
|
47 val inferT_axm : Sign.sg -> string * term -> string * term |
|
48 val add_axioms : (string * string) list -> theory -> theory |
|
49 val add_axioms_i : (string * term) list -> theory -> theory |
|
50 val add_thyname : string -> theory -> theory |
|
51 |
|
52 val merge_theories : theory * theory -> theory |
|
53 val merge_thy_list : bool -> theory list -> theory |
|
54 end; |
|
55 |
|
56 |
|
57 structure Theory : THEORY = |
|
58 struct |
|
59 (*** Theories ***) |
|
60 |
|
61 datatype theory = |
|
62 Theory of { |
|
63 sign: Sign.sg, |
|
64 new_axioms: term Symtab.table, |
|
65 parents: theory list}; |
|
66 |
|
67 fun rep_theory (Theory args) = args; |
|
68 |
|
69 (*errors involving theories*) |
|
70 exception THEORY of string * theory list; |
|
71 |
|
72 |
|
73 val sign_of = #sign o rep_theory; |
|
74 val syn_of = #syn o Sign.rep_sg o sign_of; |
|
75 |
|
76 (*stamps associated with a theory*) |
|
77 val stamps_of_thy = #stamps o Sign.rep_sg o sign_of; |
|
78 |
|
79 (*return the immediate ancestors*) |
|
80 val parents_of = #parents o rep_theory; |
|
81 |
|
82 |
|
83 (*compare theories*) |
|
84 val subthy = Sign.subsig o pairself sign_of; |
|
85 val eq_thy = Sign.eq_sg o pairself sign_of; |
|
86 |
|
87 |
|
88 (* the Pure theories *) |
|
89 |
|
90 val proto_pure_thy = |
|
91 Theory {sign = Sign.proto_pure, new_axioms = Symtab.null, parents = []}; |
|
92 |
|
93 val pure_thy = |
|
94 Theory {sign = Sign.pure, new_axioms = Symtab.null, parents = []}; |
|
95 |
|
96 val cpure_thy = |
|
97 Theory {sign = Sign.cpure, new_axioms = Symtab.null, parents = []}; |
|
98 |
|
99 |
|
100 |
|
101 (** extend theory **) |
|
102 |
|
103 fun err_dup_axms names = |
|
104 error ("Duplicate axiom name(s) " ^ commas_quote names); |
|
105 |
|
106 fun ext_thy (thy as Theory {sign, new_axioms, parents}) sign1 new_axms = |
|
107 let |
|
108 val draft = Sign.is_draft sign; |
|
109 val new_axioms1 = |
|
110 Symtab.extend_new (if draft then new_axioms else Symtab.null, new_axms) |
|
111 handle Symtab.DUPS names => err_dup_axms names; |
|
112 val parents1 = if draft then parents else [thy]; |
|
113 in |
|
114 Theory {sign = sign1, new_axioms = new_axioms1, parents = parents1} |
|
115 end; |
|
116 |
|
117 |
|
118 (* extend signature of a theory *) |
|
119 |
|
120 fun ext_sg extfun decls (thy as Theory {sign, ...}) = |
|
121 ext_thy thy (extfun decls sign) []; |
|
122 |
|
123 val add_classes = ext_sg Sign.add_classes; |
|
124 val add_classrel = ext_sg Sign.add_classrel; |
|
125 val add_defsort = ext_sg Sign.add_defsort; |
|
126 val add_types = ext_sg Sign.add_types; |
|
127 val add_tyabbrs = ext_sg Sign.add_tyabbrs; |
|
128 val add_tyabbrs_i = ext_sg Sign.add_tyabbrs_i; |
|
129 val add_arities = ext_sg Sign.add_arities; |
|
130 val add_consts = ext_sg Sign.add_consts; |
|
131 val add_consts_i = ext_sg Sign.add_consts_i; |
|
132 val add_syntax = ext_sg Sign.add_syntax; |
|
133 val add_syntax_i = ext_sg Sign.add_syntax_i; |
|
134 val add_trfuns = ext_sg Sign.add_trfuns; |
|
135 val add_trrules = ext_sg Sign.add_trrules; |
|
136 val add_trrules_i = ext_sg Sign.add_trrules_i; |
|
137 val add_thyname = ext_sg Sign.add_name; |
|
138 |
|
139 |
|
140 (* prepare axioms *) |
|
141 |
|
142 fun err_in_axm name = |
|
143 error ("The error(s) above occurred in axiom " ^ quote name); |
|
144 |
|
145 fun no_vars tm = |
|
146 if null (term_vars tm) andalso null (term_tvars tm) then tm |
|
147 else error "Illegal schematic variable(s) in term"; |
|
148 |
|
149 fun cert_axm sg (name, raw_tm) = |
|
150 let |
|
151 val (t, T, _) = Sign.certify_term sg raw_tm |
|
152 handle TYPE arg => error (Sign.exn_type_msg sg arg) |
|
153 | TERM (msg, _) => error msg; |
|
154 in |
|
155 assert (T = propT) "Term not of type prop"; |
|
156 (name, no_vars t) |
|
157 end |
|
158 handle ERROR => err_in_axm name; |
|
159 |
|
160 (*Some duplication of code with read_def_cterm*) |
|
161 fun read_axm sg (name, str) = |
|
162 let val ts = Syntax.read (#syn (Sign.rep_sg sg)) propT str; |
|
163 val (_, t, _) = |
|
164 Sign.infer_types sg (K None) (K None) [] true (ts,propT); |
|
165 in cert_axm sg (name,t) end; |
|
166 |
|
167 fun inferT_axm sg (name, pre_tm) = |
|
168 let val t = #2(Sign.infer_types sg (K None) (K None) [] true |
|
169 ([pre_tm], propT)) |
|
170 in (name, no_vars t) end |
|
171 handle ERROR => err_in_axm name; |
|
172 |
|
173 |
|
174 (* extend axioms of a theory *) |
|
175 |
|
176 fun ext_axms prep_axm axms (thy as Theory {sign, ...}) = |
|
177 let |
|
178 val sign1 = Sign.make_draft sign; |
|
179 val axioms = map (apsnd (Term.compress_term o Logic.varify) o |
|
180 prep_axm sign) |
|
181 axms; |
|
182 in |
|
183 ext_thy thy sign1 axioms |
|
184 end; |
|
185 |
|
186 val add_axioms = ext_axms read_axm; |
|
187 val add_axioms_i = ext_axms cert_axm; |
|
188 |
|
189 |
|
190 |
|
191 (** merge theories **) |
|
192 |
|
193 fun merge_thy_list mk_draft thys = |
|
194 let |
|
195 fun is_union thy = forall (fn t => subthy (t, thy)) thys; |
|
196 val is_draft = Sign.is_draft o sign_of; |
|
197 |
|
198 fun add_sign (sg, Theory {sign, ...}) = |
|
199 Sign.merge (sg, sign) handle TERM (msg, _) => error msg; |
|
200 in |
|
201 (case (find_first is_union thys, exists is_draft thys) of |
|
202 (Some thy, _) => thy |
|
203 | (None, true) => raise THEORY ("Illegal merge of draft theories", thys) |
|
204 | (None, false) => Theory { |
|
205 sign = |
|
206 (if mk_draft then Sign.make_draft else I) |
|
207 (foldl add_sign (Sign.proto_pure, thys)), |
|
208 new_axioms = Symtab.null, |
|
209 parents = thys}) |
|
210 end; |
|
211 |
|
212 fun merge_theories (thy1, thy2) = merge_thy_list false [thy1, thy2]; |
|
213 |
|
214 |
|
215 end; |
|
216 |
|
217 open Theory; |