21 include SYN_EXT0 |
21 include SYN_EXT0 |
22 include TYPE_EXT0 |
22 include TYPE_EXT0 |
23 include SYN_TRANS1 |
23 include SYN_TRANS1 |
24 include MIXFIX1 |
24 include MIXFIX1 |
25 include PRINTER0 |
25 include PRINTER0 |
26 val extend_trtab: string -> (string * ('a * stamp)) list -> |
|
27 ('a * stamp) Symtab.table -> ('a * stamp) Symtab.table |
|
28 val merge_trtabs: string -> ('a * stamp) Symtab.table -> ('a * stamp) Symtab.table -> |
|
29 ('a * stamp) Symtab.table |
|
30 val merge_tr'tabs: ('a * stamp) list Symtab.table -> ('a * stamp) list Symtab.table |
|
31 -> ('a * stamp) list Symtab.table |
|
32 val extend_tr'tab: (string * ('a * stamp)) list -> |
|
33 ('a * stamp) list Symtab.table -> ('a * stamp) list Symtab.table |
|
34 datatype 'a trrule = |
26 datatype 'a trrule = |
35 ParseRule of 'a * 'a | |
27 ParseRule of 'a * 'a | |
36 PrintRule of 'a * 'a | |
28 PrintRule of 'a * 'a | |
37 ParsePrintRule of 'a * 'a |
29 ParsePrintRule of 'a * 'a |
38 type syntax |
30 type syntax |
39 val eq_syntax: syntax * syntax -> bool |
31 val eq_syntax: syntax * syntax -> bool |
40 val is_keyword: syntax -> string -> bool |
32 val is_keyword: syntax -> string -> bool |
41 type mode |
33 type mode |
42 val mode_default: mode |
34 val mode_default: mode |
43 val mode_input: mode |
35 val mode_input: mode |
44 val extend_type_gram: (string * int * mixfix) list -> syntax -> syntax |
36 val update_type_gram: (string * int * mixfix) list -> syntax -> syntax |
45 val extend_consts: string list -> syntax -> syntax |
37 val update_consts: string list -> syntax -> syntax |
46 val extend_trfuns: |
38 val update_trfuns: |
47 (string * ((ast list -> ast) * stamp)) list * |
39 (string * ((ast list -> ast) * stamp)) list * |
48 (string * ((term list -> term) * stamp)) list * |
40 (string * ((term list -> term) * stamp)) list * |
49 (string * ((bool -> typ -> term list -> term) * stamp)) list * |
41 (string * ((bool -> typ -> term list -> term) * stamp)) list * |
50 (string * ((ast list -> ast) * stamp)) list -> syntax -> syntax |
42 (string * ((ast list -> ast) * stamp)) list -> syntax -> syntax |
51 val extend_advanced_trfuns: |
43 val update_advanced_trfuns: |
52 (string * ((Proof.context -> ast list -> ast) * stamp)) list * |
44 (string * ((Proof.context -> ast list -> ast) * stamp)) list * |
53 (string * ((Proof.context -> term list -> term) * stamp)) list * |
45 (string * ((Proof.context -> term list -> term) * stamp)) list * |
54 (string * ((Proof.context -> bool -> typ -> term list -> term) * stamp)) list * |
46 (string * ((Proof.context -> bool -> typ -> term list -> term) * stamp)) list * |
55 (string * ((Proof.context -> ast list -> ast) * stamp)) list -> syntax -> syntax |
47 (string * ((Proof.context -> ast list -> ast) * stamp)) list -> syntax -> syntax |
56 val extend_tokentrfuns: (string * string * (string -> output * int)) list -> syntax -> syntax |
48 val extend_tokentrfuns: (string * string * (string -> output * int)) list -> syntax -> syntax |
57 val extend_const_gram: (string -> bool) -> |
49 val update_const_gram: (string -> bool) -> |
58 mode -> (string * typ * mixfix) list -> syntax -> syntax |
50 mode -> (string * typ * mixfix) list -> syntax -> syntax |
59 val remove_const_gram: (string -> bool) -> |
51 val remove_const_gram: (string -> bool) -> |
60 mode -> (string * typ * mixfix) list -> syntax -> syntax |
52 mode -> (string * typ * mixfix) list -> syntax -> syntax |
61 val update_const_gram: (string -> bool) -> |
53 val update_trrules: Proof.context -> (string -> bool) -> syntax -> |
62 mode -> (string * typ * mixfix) list -> syntax -> syntax |
|
63 val extend_trrules: Proof.context -> (string -> bool) -> syntax -> |
|
64 (string * string) trrule list -> syntax -> syntax |
54 (string * string) trrule list -> syntax -> syntax |
65 val remove_trrules: Proof.context -> (string -> bool) -> syntax -> |
55 val remove_trrules: Proof.context -> (string -> bool) -> syntax -> |
66 (string * string) trrule list -> syntax -> syntax |
56 (string * string) trrule list -> syntax -> syntax |
67 val extend_trrules_i: ast trrule list -> syntax -> syntax |
57 val update_trrules_i: ast trrule list -> syntax -> syntax |
68 val remove_trrules_i: ast trrule list -> syntax -> syntax |
58 val remove_trrules_i: ast trrule list -> syntax -> syntax |
69 val map_trrule: ('a -> 'b) -> 'a trrule -> 'b trrule |
59 val map_trrule: ('a -> 'b) -> 'a trrule -> 'b trrule |
70 val merge_syntaxes: syntax -> syntax -> syntax |
60 val merge_syntaxes: syntax -> syntax -> syntax |
71 val basic_syn: syntax |
61 val basic_syn: syntax |
72 val basic_nonterms: string list |
62 val basic_nonterms: string list |
77 val standard_parse_term: Pretty.pp -> (term -> term Exn.result) -> |
67 val standard_parse_term: Pretty.pp -> (term -> term Exn.result) -> |
78 (((string * int) * sort) list -> string * int -> Term.sort) -> |
68 (((string * int) * sort) list -> string * int -> Term.sort) -> |
79 (string -> string option) -> (string -> string option) -> |
69 (string -> string option) -> (string -> string option) -> |
80 (typ -> typ) -> (sort -> sort) -> Proof.context -> |
70 (typ -> typ) -> (sort -> sort) -> Proof.context -> |
81 (string -> bool) -> syntax -> typ -> string -> term |
71 (string -> bool) -> syntax -> typ -> string -> term |
82 val standard_parse_typ: Proof.context -> syntax -> ((indexname * sort) list -> indexname -> sort) -> |
72 val standard_parse_typ: Proof.context -> syntax -> |
83 (sort -> sort) -> string -> typ |
73 ((indexname * sort) list -> indexname -> sort) -> (sort -> sort) -> string -> typ |
84 val standard_parse_sort: Proof.context -> syntax -> (sort -> sort) -> string -> sort |
74 val standard_parse_sort: Proof.context -> syntax -> (sort -> sort) -> string -> sort |
85 val standard_unparse_term: (string -> xstring) -> Proof.context -> syntax -> bool -> term -> Pretty.T |
75 val standard_unparse_term: (string -> xstring) -> |
|
76 Proof.context -> syntax -> bool -> term -> Pretty.T |
86 val standard_unparse_typ: Proof.context -> syntax -> typ -> Pretty.T |
77 val standard_unparse_typ: Proof.context -> syntax -> typ -> Pretty.T |
87 val standard_unparse_sort: Proof.context -> syntax -> sort -> Pretty.T |
78 val standard_unparse_sort: Proof.context -> syntax -> sort -> Pretty.T |
88 val ambiguity_level: int ref |
79 val ambiguity_level: int ref |
89 val ambiguity_is_error: bool ref |
80 val ambiguity_is_error: bool ref |
90 val parse_sort: Proof.context -> string -> sort |
81 val parse_sort: Proof.context -> string -> sort |
164 fun err_dup_trfun name c = |
155 fun err_dup_trfun name c = |
165 error ("More than one " ^ name ^ " for " ^ quote c); |
156 error ("More than one " ^ name ^ " for " ^ quote c); |
166 |
157 |
167 fun remove_trtab trfuns = fold (Symtab.remove SynExt.eq_trfun) trfuns; |
158 fun remove_trtab trfuns = fold (Symtab.remove SynExt.eq_trfun) trfuns; |
168 |
159 |
169 fun extend_trtab name trfuns tab = Symtab.extend (remove_trtab trfuns tab, trfuns) |
160 fun update_trtab name trfuns tab = Symtab.extend (remove_trtab trfuns tab, trfuns) |
170 handle Symtab.DUP c => err_dup_trfun name c; |
161 handle Symtab.DUP c => err_dup_trfun name c; |
171 |
162 |
172 fun merge_trtabs name tab1 tab2 = Symtab.merge SynExt.eq_trfun (tab1, tab2) |
163 fun merge_trtabs name tab1 tab2 = Symtab.merge SynExt.eq_trfun (tab1, tab2) |
173 handle Symtab.DUP c => err_dup_trfun name c; |
164 handle Symtab.DUP c => err_dup_trfun name c; |
174 |
165 |
175 |
166 |
176 (* print (ast) translations *) |
167 (* print (ast) translations *) |
177 |
168 |
178 fun lookup_tr' tab c = map fst (Symtab.lookup_list tab c); |
169 fun lookup_tr' tab c = map fst (Symtab.lookup_list tab c); |
179 fun extend_tr'tab trfuns = fold_rev Symtab.update_list trfuns; |
170 fun update_tr'tab trfuns = fold_rev (Symtab.update_list SynExt.eq_trfun) trfuns; |
180 fun remove_tr'tab trfuns = fold (Symtab.remove_list SynExt.eq_trfun) trfuns; |
171 fun remove_tr'tab trfuns = fold (Symtab.remove_list SynExt.eq_trfun) trfuns; |
181 fun merge_tr'tabs tab1 tab2 = Symtab.merge_list SynExt.eq_trfun (tab1, tab2); |
172 fun merge_tr'tabs tab1 tab2 = Symtab.merge_list SynExt.eq_trfun (tab1, tab2); |
182 |
173 |
183 |
174 |
184 |
175 |
221 type ruletab = (Ast.ast * Ast.ast) list Symtab.table; |
212 type ruletab = (Ast.ast * Ast.ast) list Symtab.table; |
222 |
213 |
223 fun dest_ruletab tab = maps snd (Symtab.dest tab); |
214 fun dest_ruletab tab = maps snd (Symtab.dest tab); |
224 |
215 |
225 |
216 |
226 (* empty, extend, merge ruletabs *) |
217 (* empty, update, merge ruletabs *) |
227 |
218 |
228 val extend_ruletab = fold_rev (fn r => Symtab.update_list (Ast.head_of_rule r, r)); |
219 val update_ruletab = fold_rev (fn r => Symtab.update_list (op =) (Ast.head_of_rule r, r)); |
229 val remove_ruletab = fold (fn r => Symtab.remove_list (op =) (Ast.head_of_rule r, r)); |
220 val remove_ruletab = fold (fn r => Symtab.remove_list (op =) (Ast.head_of_rule r, r)); |
230 fun merge_ruletabs tab1 tab2 = Symtab.merge_list (op =) (tab1, tab2); |
221 fun merge_ruletabs tab1 tab2 = Symtab.merge_list (op =) (tab1, tab2); |
231 |
222 |
232 |
223 |
233 |
224 |
274 print_ast_trtab = Symtab.empty, |
265 print_ast_trtab = Symtab.empty, |
275 tokentrtab = [], |
266 tokentrtab = [], |
276 prtabs = Printer.empty_prtabs}, stamp ()); |
267 prtabs = Printer.empty_prtabs}, stamp ()); |
277 |
268 |
278 |
269 |
279 (* extend_syntax *) |
270 (* update_syntax *) |
280 |
271 |
281 fun extend_syntax (mode, inout) syn_ext (Syntax (tabs, _)) = |
272 fun update_syntax (mode, inout) syn_ext (Syntax (tabs, _)) = |
282 let |
273 let |
283 val {input, lexicon, gram, consts = consts1, prmodes = prmodes1, |
274 val {input, lexicon, gram, consts = consts1, prmodes = prmodes1, |
284 parse_ast_trtab, parse_ruletab, parse_trtab, print_trtab, print_ruletab, |
275 parse_ast_trtab, parse_ruletab, parse_trtab, print_trtab, print_ruletab, |
285 print_ast_trtab, tokentrtab, prtabs} = tabs; |
276 print_ast_trtab, tokentrtab, prtabs} = tabs; |
286 val SynExt.SynExt {xprods, consts = consts2, prmodes = prmodes2, |
277 val SynExt.SynExt {xprods, consts = consts2, prmodes = prmodes2, |
287 parse_ast_translation, parse_rules, parse_translation, print_translation, print_rules, |
278 parse_ast_translation, parse_rules, parse_translation, print_translation, print_rules, |
288 print_ast_translation, token_translation} = syn_ext; |
279 print_ast_translation, token_translation} = syn_ext; |
|
280 val input' = if inout then fold (insert (op =)) xprods input else input; |
|
281 val changed = length input <> length input'; |
289 fun if_inout xs = if inout then xs else []; |
282 fun if_inout xs = if inout then xs else []; |
290 in |
283 in |
291 Syntax |
284 Syntax |
292 ({input = if_inout xprods @ input, |
285 ({input = input', |
293 lexicon = Scan.extend_lexicon (if_inout (SynExt.delims_of xprods)) lexicon, |
286 lexicon = if changed then Scan.extend_lexicon (SynExt.delims_of xprods) lexicon else lexicon, |
294 gram = Parser.extend_gram gram (if_inout xprods), |
287 gram = if changed then Parser.extend_gram gram xprods else gram, |
295 consts = Library.merge (op =) (consts1, filter_out NameSpace.is_qualified consts2), |
288 consts = Library.merge (op =) (consts1, filter_out NameSpace.is_qualified consts2), |
296 prmodes = insert (op =) mode (Library.merge (op =) (prmodes1, prmodes2)), |
289 prmodes = insert (op =) mode (Library.merge (op =) (prmodes1, prmodes2)), |
297 parse_ast_trtab = |
290 parse_ast_trtab = |
298 extend_trtab "parse ast translation" (if_inout parse_ast_translation) parse_ast_trtab, |
291 update_trtab "parse ast translation" (if_inout parse_ast_translation) parse_ast_trtab, |
299 parse_ruletab = extend_ruletab (if_inout parse_rules) parse_ruletab, |
292 parse_ruletab = update_ruletab (if_inout parse_rules) parse_ruletab, |
300 parse_trtab = extend_trtab "parse translation" (if_inout parse_translation) parse_trtab, |
293 parse_trtab = update_trtab "parse translation" (if_inout parse_translation) parse_trtab, |
301 print_trtab = extend_tr'tab print_translation print_trtab, |
294 print_trtab = update_tr'tab print_translation print_trtab, |
302 print_ruletab = extend_ruletab print_rules print_ruletab, |
295 print_ruletab = update_ruletab print_rules print_ruletab, |
303 print_ast_trtab = extend_tr'tab print_ast_translation print_ast_trtab, |
296 print_ast_trtab = update_tr'tab print_ast_translation print_ast_trtab, |
304 tokentrtab = extend_tokentrtab token_translation tokentrtab, |
297 tokentrtab = extend_tokentrtab token_translation tokentrtab, |
305 prtabs = Printer.extend_prtabs mode xprods prtabs}, stamp ()) |
298 prtabs = Printer.update_prtabs mode xprods prtabs}, stamp ()) |
306 end; |
299 end; |
307 |
300 |
308 |
301 |
309 (* remove_syntax *) |
302 (* remove_syntax *) |
310 |
303 |
315 print_ast_translation, token_translation = _} = syn_ext; |
308 print_ast_translation, token_translation = _} = syn_ext; |
316 val {input, lexicon, gram, consts, prmodes, |
309 val {input, lexicon, gram, consts, prmodes, |
317 parse_ast_trtab, parse_ruletab, parse_trtab, print_trtab, print_ruletab, |
310 parse_ast_trtab, parse_ruletab, parse_trtab, print_trtab, print_ruletab, |
318 print_ast_trtab, tokentrtab, prtabs} = tabs; |
311 print_ast_trtab, tokentrtab, prtabs} = tabs; |
319 val input' = if inout then subtract (op =) xprods input else input; |
312 val input' = if inout then subtract (op =) xprods input else input; |
320 val changed = input <> input'; |
313 val changed = length input <> length input'; |
321 fun if_inout xs = if inout then xs else []; |
314 fun if_inout xs = if inout then xs else []; |
322 in |
315 in |
323 Syntax |
316 Syntax |
324 ({input = input', |
317 ({input = input', |
325 lexicon = if changed then Scan.make_lexicon (SynExt.delims_of input') else lexicon, |
318 lexicon = if changed then Scan.make_lexicon (SynExt.delims_of input') else lexicon, |
373 |
366 |
374 (* basic syntax *) |
367 (* basic syntax *) |
375 |
368 |
376 val basic_syn = |
369 val basic_syn = |
377 empty_syntax |
370 empty_syntax |
378 |> extend_syntax mode_default TypeExt.type_ext |
371 |> update_syntax mode_default TypeExt.type_ext |
379 |> extend_syntax mode_default SynExt.pure_ext; |
372 |> update_syntax mode_default SynExt.pure_ext; |
380 |
373 |
381 val basic_nonterms = |
374 val basic_nonterms = |
382 (Lexicon.terminals @ [SynExt.logic, "type", "types", "sort", "classes", |
375 (Lexicon.terminals @ [SynExt.logic, "type", "types", "sort", "classes", |
383 SynExt.args, SynExt.cargs, "pttrn", "pttrns", "idt", "idts", "aprop", |
376 SynExt.args, SynExt.cargs, "pttrn", "pttrns", "idt", "idts", "aprop", |
384 "asms", SynExt.any_, SynExt.sprop, "num_const", "index", "struct"]); |
377 "asms", SynExt.any_, SynExt.sprop, "num_const", "index", "struct"]); |
617 |
610 |
618 |
611 |
619 |
612 |
620 (** modify syntax **) |
613 (** modify syntax **) |
621 |
614 |
622 fun ext_syntax f decls = extend_syntax mode_default (f decls); |
615 fun ext_syntax f decls = update_syntax mode_default (f decls); |
623 |
616 |
624 val extend_type_gram = ext_syntax Mixfix.syn_ext_types; |
617 val update_type_gram = ext_syntax Mixfix.syn_ext_types; |
625 val extend_consts = ext_syntax SynExt.syn_ext_const_names; |
618 val update_consts = ext_syntax SynExt.syn_ext_const_names; |
626 val extend_trfuns = ext_syntax SynExt.syn_ext_trfuns; |
619 val update_trfuns = ext_syntax SynExt.syn_ext_trfuns; |
627 val extend_advanced_trfuns = ext_syntax SynExt.syn_ext_advanced_trfuns; |
620 val update_advanced_trfuns = ext_syntax SynExt.syn_ext_advanced_trfuns; |
628 val extend_tokentrfuns = ext_syntax SynExt.syn_ext_tokentrfuns; |
621 val extend_tokentrfuns = ext_syntax SynExt.syn_ext_tokentrfuns; |
629 |
622 |
630 fun extend_const_gram is_logtype prmode decls = |
623 fun update_const_gram is_logtype prmode decls = |
631 extend_syntax prmode (Mixfix.syn_ext_consts is_logtype decls); |
624 update_syntax prmode (Mixfix.syn_ext_consts is_logtype decls); |
632 |
625 |
633 fun remove_const_gram is_logtype prmode decls = |
626 fun remove_const_gram is_logtype prmode decls = |
634 remove_syntax prmode (Mixfix.syn_ext_consts is_logtype decls); |
627 remove_syntax prmode (Mixfix.syn_ext_consts is_logtype decls); |
635 |
628 |
636 fun update_const_gram is_logtype prmode decls = |
629 fun update_trrules ctxt is_logtype syn = |
637 let val syn_ext = Mixfix.syn_ext_consts is_logtype decls |
|
638 in remove_syntax prmode syn_ext #> extend_syntax prmode syn_ext end; |
|
639 |
|
640 fun extend_trrules ctxt is_logtype syn = |
|
641 ext_syntax SynExt.syn_ext_rules o read_rules ctxt is_logtype syn; |
630 ext_syntax SynExt.syn_ext_rules o read_rules ctxt is_logtype syn; |
642 |
631 |
643 fun remove_trrules ctxt is_logtype syn = |
632 fun remove_trrules ctxt is_logtype syn = |
644 remove_syntax mode_default o SynExt.syn_ext_rules o read_rules ctxt is_logtype syn; |
633 remove_syntax mode_default o SynExt.syn_ext_rules o read_rules ctxt is_logtype syn; |
645 |
634 |
646 val extend_trrules_i = ext_syntax SynExt.syn_ext_rules o cert_rules; |
635 val update_trrules_i = ext_syntax SynExt.syn_ext_rules o cert_rules; |
647 val remove_trrules_i = remove_syntax mode_default o SynExt.syn_ext_rules o cert_rules; |
636 val remove_trrules_i = remove_syntax mode_default o SynExt.syn_ext_rules o cert_rules; |
648 |
637 |
649 |
638 |
650 |
639 |
651 (** inner syntax operations **) |
640 (** inner syntax operations **) |