# HG changeset patch # User wenzelm # Date 850494872 -3600 # Node ID 4127499d9b525b1ec1661a9a264b4f8803a37c12 # Parent e7c2bce815ba76c0cb95b6326cac2ac38d29610a added extend_trfunsT; removed test: prtabs_of; removed chartrans; diff -r e7c2bce815ba -r 4127499d9b52 src/Pure/Syntax/syntax.ML --- a/src/Pure/Syntax/syntax.ML Fri Dec 13 17:30:28 1996 +0100 +++ b/src/Pure/Syntax/syntax.ML Fri Dec 13 17:34:32 1996 +0100 @@ -8,15 +8,15 @@ infix |-> <-| <->; signature BASIC_SYNTAX = - sig +sig include AST0 include SYN_TRANS0 include MIXFIX0 include PRINTER0 - end; +end; signature SYNTAX = - sig +sig include AST1 include LEXICON0 include SYN_EXT0 @@ -38,6 +38,7 @@ (string * (term list -> term)) list * (string * (term list -> term)) list * (string * (ast list -> ast)) list -> syntax + val extend_trfunsT: syntax -> (string * (typ -> term list -> term)) list -> syntax val extend_trrules: syntax -> (string * string) trrule list -> syntax val extend_trrules_i: syntax -> ast trrule list -> syntax val merge_syntaxes: syntax -> syntax -> syntax @@ -57,8 +58,7 @@ val simple_string_of_typ: typ -> string val simple_pprint_typ: typ -> pprint_args -> unit val ambiguity_level: int ref - val prtabs_of: syntax -> Printer.prtabs (* FIXME test only *) - end; +end; structure Syntax : SYNTAX = struct @@ -69,6 +69,7 @@ (** tables of translation functions **) (*the ref serves as unique id*) +(*does not subsume typed print translations*) type 'a trtab = (('a list -> 'a) * unit ref) Symtab.table; val dest_trtab = Symtab.dest; @@ -125,7 +126,6 @@ datatype syntax = Syntax of { - chartrans: (string * string) list, lexicon: lexicon, logtypes: string list, gram: gram, @@ -133,7 +133,7 @@ parse_ast_trtab: ast trtab, parse_ruletab: ruletab, parse_trtab: term trtab, - print_trtab: term trtab, + print_trtab: ((typ -> term list -> term) * unit ref) Symtab.table, print_ruletab: ruletab, print_ast_trtab: ast trtab, prtabs: prtabs}; @@ -143,7 +143,6 @@ val empty_syntax = Syntax { - chartrans = [], lexicon = empty_lexicon, logtypes = [], gram = empty_gram, @@ -161,16 +160,14 @@ fun extend_syntax (mode, inout) (Syntax tabs) syn_ext = let - val {chartrans = _, lexicon, logtypes = logtypes1, gram, consts = consts1, + val {lexicon, logtypes = logtypes1, gram, consts = consts1, parse_ast_trtab, parse_ruletab, parse_trtab, print_trtab, print_ruletab, print_ast_trtab, prtabs} = tabs; val SynExt {logtypes = logtypes2, xprods, consts = consts2, parse_ast_translation, parse_rules, parse_translation, print_translation, print_rules, print_ast_translation} = syn_ext; - val prtabs' = extend_prtabs prtabs mode xprods; in Syntax { - chartrans = chartrans_of prtabs', lexicon = if inout then extend_lexicon lexicon (delims_of xprods) else lexicon, logtypes = extend_list logtypes1 logtypes2, gram = if inout then extend_gram gram xprods else gram, @@ -183,7 +180,7 @@ print_ruletab = extend_ruletab print_ruletab print_rules, print_ast_trtab = extend_trtab print_ast_trtab print_ast_translation "print ast translation", - prtabs = prtabs'} + prtabs = extend_prtabs prtabs mode xprods} end; @@ -191,21 +188,19 @@ fun merge_syntaxes (Syntax tabs1) (Syntax tabs2) = let - val {chartrans = _, lexicon = lexicon1, logtypes = logtypes1, gram = gram1, + val {lexicon = lexicon1, logtypes = logtypes1, gram = gram1, consts = consts1, parse_ast_trtab = parse_ast_trtab1, parse_ruletab = parse_ruletab1, parse_trtab = parse_trtab1, print_trtab = print_trtab1, print_ruletab = print_ruletab1, print_ast_trtab = print_ast_trtab1, prtabs = prtabs1} = tabs1; - val {chartrans = _, lexicon = lexicon2, logtypes = logtypes2, gram = gram2, + val {lexicon = lexicon2, logtypes = logtypes2, gram = gram2, consts = consts2, parse_ast_trtab = parse_ast_trtab2, parse_ruletab = parse_ruletab2, parse_trtab = parse_trtab2, print_trtab = print_trtab2, print_ruletab = print_ruletab2, print_ast_trtab = print_ast_trtab2, prtabs = prtabs2} = tabs2; - val prtabs = merge_prtabs prtabs1 prtabs2; in Syntax { - chartrans = chartrans_of prtabs, lexicon = merge_lexicons lexicon1 lexicon2, logtypes = merge_lists logtypes1 logtypes2, gram = merge_grams gram1 gram2, @@ -218,7 +213,7 @@ print_ruletab = merge_ruletabs print_ruletab1 print_ruletab2, print_ast_trtab = merge_trtabs print_ast_trtab1 print_ast_trtab2 "print ast translation", - prtabs = prtabs} + prtabs = merge_prtabs prtabs1 prtabs2} end; @@ -238,16 +233,12 @@ fun print_gram (Syntax tabs) = let - val pretty_chartrans = - map (fn (c, s) => Pretty.str (c ^ " -> " ^ quote s)); - - val {chartrans, lexicon, logtypes, gram, prtabs, ...} = tabs; + val {lexicon, logtypes, gram, prtabs, ...} = tabs; in - Pretty.writeln (Pretty.big_list "chartrans:" (pretty_chartrans chartrans)); Pretty.writeln (pretty_strs_qs "lexicon:" (dest_lexicon lexicon)); Pretty.writeln (Pretty.strs ("logtypes:" :: logtypes)); Pretty.writeln (Pretty.big_list "prods:" (pretty_gram gram)); - Pretty.writeln (pretty_strs_qs "printer modes:" (prmodes_of prtabs)) + Pretty.writeln (pretty_strs_qs "print modes:" (prmodes_of prtabs)) end; @@ -442,6 +433,8 @@ val extend_trfuns = ext_syntax syn_ext_trfuns ("", true); +val extend_trfunsT = ext_syntax syn_ext_trfunsT ("", true); + fun extend_trrules syn rules = ext_syntax syn_ext_rules ("", true) syn (prep_rules (read_pattern syn) rules); @@ -449,9 +442,4 @@ ext_syntax syn_ext_rules ("", true) syn (prep_rules I rules); - -(* FIXME test only *) - -fun prtabs_of (Syntax {prtabs, ...}) = prtabs; - end;