63 (string * (term list -> term)) list * |
63 (string * (term list -> term)) list * |
64 (string * (term list -> term)) list * |
64 (string * (term list -> term)) list * |
65 (string * (Syntax.ast list -> Syntax.ast)) list -> theory -> theory |
65 (string * (Syntax.ast list -> Syntax.ast)) list -> theory -> theory |
66 val add_trfunsT: |
66 val add_trfunsT: |
67 (string * (bool -> typ -> term list -> term)) list -> theory -> theory |
67 (string * (bool -> typ -> term list -> term)) list -> theory -> theory |
|
68 val add_advanced_trfuns: |
|
69 (string * (Sign.sg -> Syntax.ast list -> Syntax.ast)) list * |
|
70 (string * (Sign.sg -> term list -> term)) list * |
|
71 (string * (Sign.sg -> term list -> term)) list * |
|
72 (string * (Sign.sg -> Syntax.ast list -> Syntax.ast)) list -> theory -> theory |
|
73 val add_advanced_trfunsT: |
|
74 (string * (Sign.sg -> bool -> typ -> term list -> term)) list -> theory -> theory |
68 val add_tokentrfuns: |
75 val add_tokentrfuns: |
69 (string * string * (string -> string * real)) list -> theory -> theory |
76 (string * string * (string -> string * real)) list -> theory -> theory |
70 val add_mode_tokentrfuns: string -> (string * (string -> string * real)) list |
77 val add_mode_tokentrfuns: string -> (string * (string -> string * real)) list |
71 -> theory -> theory |
78 -> theory -> theory |
72 val add_trrules: (xstring * string) Syntax.trrule list -> theory -> theory |
79 val add_trrules: (xstring * string) Syntax.trrule list -> theory -> theory |
193 |
200 |
194 (* extend signature of a theory *) |
201 (* extend signature of a theory *) |
195 |
202 |
196 fun ext_sign extfun decls thy = ext_theory thy (extfun decls) I [] []; |
203 fun ext_sign extfun decls thy = ext_theory thy (extfun decls) I [] []; |
197 |
204 |
198 val add_classes = ext_sign Sign.add_classes; |
205 val add_classes = ext_sign Sign.add_classes; |
199 val add_classes_i = ext_sign Sign.add_classes_i; |
206 val add_classes_i = ext_sign Sign.add_classes_i; |
200 val add_classrel = ext_sign Sign.add_classrel; |
207 val add_classrel = ext_sign Sign.add_classrel; |
201 val add_classrel_i = ext_sign Sign.add_classrel_i; |
208 val add_classrel_i = ext_sign Sign.add_classrel_i; |
202 val add_defsort = ext_sign Sign.add_defsort; |
209 val add_defsort = ext_sign Sign.add_defsort; |
203 val add_defsort_i = ext_sign Sign.add_defsort_i; |
210 val add_defsort_i = ext_sign Sign.add_defsort_i; |
204 val add_types = ext_sign Sign.add_types; |
211 val add_types = ext_sign Sign.add_types; |
205 val add_nonterminals = ext_sign Sign.add_nonterminals; |
212 val add_nonterminals = ext_sign Sign.add_nonterminals; |
206 val add_tyabbrs = ext_sign Sign.add_tyabbrs; |
213 val add_tyabbrs = ext_sign Sign.add_tyabbrs; |
207 val add_tyabbrs_i = ext_sign Sign.add_tyabbrs_i; |
214 val add_tyabbrs_i = ext_sign Sign.add_tyabbrs_i; |
208 val add_arities = ext_sign Sign.add_arities; |
215 val add_arities = ext_sign Sign.add_arities; |
209 val add_arities_i = ext_sign Sign.add_arities_i; |
216 val add_arities_i = ext_sign Sign.add_arities_i; |
210 val add_consts = ext_sign Sign.add_consts; |
217 val add_consts = ext_sign Sign.add_consts; |
211 val add_consts_i = ext_sign Sign.add_consts_i; |
218 val add_consts_i = ext_sign Sign.add_consts_i; |
212 val add_syntax = ext_sign Sign.add_syntax; |
219 val add_syntax = ext_sign Sign.add_syntax; |
213 val add_syntax_i = ext_sign Sign.add_syntax_i; |
220 val add_syntax_i = ext_sign Sign.add_syntax_i; |
214 val add_modesyntax = curry (ext_sign Sign.add_modesyntax); |
221 val add_modesyntax = curry (ext_sign Sign.add_modesyntax); |
215 val add_modesyntax_i = curry (ext_sign Sign.add_modesyntax_i); |
222 val add_modesyntax_i = curry (ext_sign Sign.add_modesyntax_i); |
216 val add_trfuns = ext_sign Sign.add_trfuns; |
223 val add_trfuns = ext_sign Sign.add_trfuns; |
217 val add_trfunsT = ext_sign Sign.add_trfunsT; |
224 val add_trfunsT = ext_sign Sign.add_trfunsT; |
218 val add_tokentrfuns = ext_sign Sign.add_tokentrfuns; |
225 val add_advanced_trfuns = ext_sign Sign.add_advanced_trfuns; |
|
226 val add_advanced_trfunsT = ext_sign Sign.add_advanced_trfunsT; |
|
227 val add_tokentrfuns = ext_sign Sign.add_tokentrfuns; |
219 fun add_mode_tokentrfuns m = add_tokentrfuns o map (fn (s, f) => (m, s, f)); |
228 fun add_mode_tokentrfuns m = add_tokentrfuns o map (fn (s, f) => (m, s, f)); |
220 val add_trrules = ext_sign Sign.add_trrules; |
229 val add_trrules = ext_sign Sign.add_trrules; |
221 val add_trrules_i = ext_sign Sign.add_trrules_i; |
230 val add_trrules_i = ext_sign Sign.add_trrules_i; |
222 val add_path = ext_sign Sign.add_path; |
231 val add_path = ext_sign Sign.add_path; |
223 val parent_path = add_path ".."; |
232 val parent_path = add_path ".."; |
224 val root_path = add_path "/"; |
233 val root_path = add_path "/"; |
225 val absolute_path = add_path "//"; |
234 val absolute_path = add_path "//"; |
226 val add_space = ext_sign Sign.add_space; |
235 val add_space = ext_sign Sign.add_space; |
227 val hide_space = ext_sign o Sign.hide_space; |
236 val hide_space = ext_sign o Sign.hide_space; |
228 val hide_space_i = ext_sign o Sign.hide_space_i; |
237 val hide_space_i = ext_sign o Sign.hide_space_i; |
229 fun hide_classes b = curry (hide_space_i b) Sign.classK; |
238 fun hide_classes b = curry (hide_space_i b) Sign.classK; |
230 fun hide_types b = curry (hide_space_i b) Sign.typeK; |
239 fun hide_types b = curry (hide_space_i b) Sign.typeK; |
231 fun hide_consts b = curry (hide_space_i b) Sign.constK; |
240 fun hide_consts b = curry (hide_space_i b) Sign.constK; |
232 val add_name = ext_sign Sign.add_name; |
241 val add_name = ext_sign Sign.add_name; |
233 val copy = ext_sign (K Sign.copy) (); |
242 val copy = ext_sign (K Sign.copy) (); |
234 val prep_ext = ext_sign (K Sign.prep_ext) (); |
243 val prep_ext = ext_sign (K Sign.prep_ext) (); |
235 |
244 |
236 |
245 |
237 |
246 |
238 (** add axioms **) |
247 (** add axioms **) |
239 |
248 |
261 end; |
270 end; |
262 |
271 |
263 (*some duplication of code with read_def_cterm*) |
272 (*some duplication of code with read_def_cterm*) |
264 fun read_def_axm (sg, types, sorts) used (name, str) = |
273 fun read_def_axm (sg, types, sorts) used (name, str) = |
265 let |
274 let |
266 val ts = Syntax.read (#syn (Sign.rep_sg sg)) propT str; |
275 val ts = Syntax.read (Sign.syn_of sg) propT str; |
267 val (t, _) = Sign.infer_types sg types sorts used true (ts, propT); |
276 val (t, _) = Sign.infer_types sg types sorts used true (ts, propT); |
268 in cert_axm sg (name, t) end |
277 in cert_axm sg (name, t) end |
269 handle ERROR => err_in_axm name; |
278 handle ERROR => err_in_axm name; |
270 |
279 |
271 fun read_axm sg name_str = read_def_axm (sg, K None, K None) [] name_str; |
280 fun read_axm sg name_str = read_def_axm (sg, K None, K None) [] name_str; |