added extend_trfunsT;
authorwenzelm
Fri Dec 13 17:34:32 1996 +0100 (1996-12-13)
changeset 23834127499d9b52
parent 2382 e7c2bce815ba
child 2384 d360b395766e
added extend_trfunsT;
removed test: prtabs_of;
removed chartrans;
src/Pure/Syntax/syntax.ML
     1.1 --- a/src/Pure/Syntax/syntax.ML	Fri Dec 13 17:30:28 1996 +0100
     1.2 +++ b/src/Pure/Syntax/syntax.ML	Fri Dec 13 17:34:32 1996 +0100
     1.3 @@ -8,15 +8,15 @@
     1.4  infix |-> <-| <->;
     1.5  
     1.6  signature BASIC_SYNTAX =
     1.7 -  sig
     1.8 +sig
     1.9    include AST0
    1.10    include SYN_TRANS0
    1.11    include MIXFIX0
    1.12    include PRINTER0
    1.13 -  end;
    1.14 +end;
    1.15  
    1.16  signature SYNTAX =
    1.17 -  sig
    1.18 +sig
    1.19    include AST1
    1.20    include LEXICON0
    1.21    include SYN_EXT0
    1.22 @@ -38,6 +38,7 @@
    1.23      (string * (term list -> term)) list *
    1.24      (string * (term list -> term)) list *
    1.25      (string * (ast list -> ast)) list -> syntax
    1.26 +  val extend_trfunsT: syntax -> (string * (typ -> term list -> term)) list -> syntax
    1.27    val extend_trrules: syntax -> (string * string) trrule list -> syntax
    1.28    val extend_trrules_i: syntax -> ast trrule list -> syntax
    1.29    val merge_syntaxes: syntax -> syntax -> syntax
    1.30 @@ -57,8 +58,7 @@
    1.31    val simple_string_of_typ: typ -> string
    1.32    val simple_pprint_typ: typ -> pprint_args -> unit
    1.33    val ambiguity_level: int ref
    1.34 -  val prtabs_of: syntax -> Printer.prtabs   (* FIXME test only *)
    1.35 -  end;
    1.36 +end;
    1.37  
    1.38  structure Syntax : SYNTAX =
    1.39  struct
    1.40 @@ -69,6 +69,7 @@
    1.41  (** tables of translation functions **)
    1.42  
    1.43  (*the ref serves as unique id*)
    1.44 +(*does not subsume typed print translations*)
    1.45  type 'a trtab = (('a list -> 'a) * unit ref) Symtab.table;
    1.46  
    1.47  val dest_trtab = Symtab.dest;
    1.48 @@ -125,7 +126,6 @@
    1.49  
    1.50  datatype syntax =
    1.51    Syntax of {
    1.52 -    chartrans: (string * string) list,
    1.53      lexicon: lexicon,
    1.54      logtypes: string list,
    1.55      gram: gram,
    1.56 @@ -133,7 +133,7 @@
    1.57      parse_ast_trtab: ast trtab,
    1.58      parse_ruletab: ruletab,
    1.59      parse_trtab: term trtab,
    1.60 -    print_trtab: term trtab,
    1.61 +    print_trtab: ((typ -> term list -> term) * unit ref) Symtab.table,
    1.62      print_ruletab: ruletab,
    1.63      print_ast_trtab: ast trtab,
    1.64      prtabs: prtabs};
    1.65 @@ -143,7 +143,6 @@
    1.66  
    1.67  val empty_syntax =
    1.68    Syntax {
    1.69 -    chartrans = [],
    1.70      lexicon = empty_lexicon,
    1.71      logtypes = [],
    1.72      gram = empty_gram,
    1.73 @@ -161,16 +160,14 @@
    1.74  
    1.75  fun extend_syntax (mode, inout) (Syntax tabs) syn_ext =
    1.76    let
    1.77 -    val {chartrans = _, lexicon, logtypes = logtypes1, gram, consts = consts1,
    1.78 +    val {lexicon, logtypes = logtypes1, gram, consts = consts1,
    1.79        parse_ast_trtab, parse_ruletab, parse_trtab, print_trtab, print_ruletab,
    1.80        print_ast_trtab, prtabs} = tabs;
    1.81      val SynExt {logtypes = logtypes2, xprods, consts = consts2, parse_ast_translation,
    1.82        parse_rules, parse_translation, print_translation, print_rules,
    1.83        print_ast_translation} = syn_ext;
    1.84 -    val prtabs' = extend_prtabs prtabs mode xprods;
    1.85    in
    1.86      Syntax {
    1.87 -      chartrans = chartrans_of prtabs',
    1.88        lexicon = if inout then extend_lexicon lexicon (delims_of xprods) else lexicon,
    1.89        logtypes = extend_list logtypes1 logtypes2,
    1.90        gram = if inout then extend_gram gram xprods else gram,
    1.91 @@ -183,7 +180,7 @@
    1.92        print_ruletab = extend_ruletab print_ruletab print_rules,
    1.93        print_ast_trtab =
    1.94          extend_trtab print_ast_trtab print_ast_translation "print ast translation",
    1.95 -      prtabs = prtabs'}
    1.96 +      prtabs = extend_prtabs prtabs mode xprods}
    1.97    end;
    1.98  
    1.99  
   1.100 @@ -191,21 +188,19 @@
   1.101  
   1.102  fun merge_syntaxes (Syntax tabs1) (Syntax tabs2) =
   1.103    let
   1.104 -    val {chartrans = _, lexicon = lexicon1, logtypes = logtypes1, gram = gram1,
   1.105 +    val {lexicon = lexicon1, logtypes = logtypes1, gram = gram1,
   1.106        consts = consts1, parse_ast_trtab = parse_ast_trtab1, parse_ruletab = parse_ruletab1,
   1.107        parse_trtab = parse_trtab1, print_trtab = print_trtab1,
   1.108        print_ruletab = print_ruletab1, print_ast_trtab = print_ast_trtab1,
   1.109        prtabs = prtabs1} = tabs1;
   1.110  
   1.111 -    val {chartrans = _, lexicon = lexicon2, logtypes = logtypes2, gram = gram2,
   1.112 +    val {lexicon = lexicon2, logtypes = logtypes2, gram = gram2,
   1.113        consts = consts2, parse_ast_trtab = parse_ast_trtab2, parse_ruletab = parse_ruletab2,
   1.114        parse_trtab = parse_trtab2, print_trtab = print_trtab2,
   1.115        print_ruletab = print_ruletab2, print_ast_trtab = print_ast_trtab2,
   1.116        prtabs = prtabs2} = tabs2;
   1.117 -    val prtabs = merge_prtabs prtabs1 prtabs2;
   1.118    in
   1.119      Syntax {
   1.120 -      chartrans = chartrans_of prtabs,
   1.121        lexicon = merge_lexicons lexicon1 lexicon2,
   1.122        logtypes = merge_lists logtypes1 logtypes2,
   1.123        gram = merge_grams gram1 gram2,
   1.124 @@ -218,7 +213,7 @@
   1.125        print_ruletab = merge_ruletabs print_ruletab1 print_ruletab2,
   1.126        print_ast_trtab =
   1.127          merge_trtabs print_ast_trtab1 print_ast_trtab2 "print ast translation",
   1.128 -      prtabs = prtabs}
   1.129 +      prtabs = merge_prtabs prtabs1 prtabs2}
   1.130    end;
   1.131  
   1.132  
   1.133 @@ -238,16 +233,12 @@
   1.134  
   1.135  fun print_gram (Syntax tabs) =
   1.136    let
   1.137 -    val pretty_chartrans =
   1.138 -      map (fn (c, s) => Pretty.str (c ^ " -> " ^ quote s));
   1.139 -
   1.140 -    val {chartrans, lexicon, logtypes, gram, prtabs, ...} = tabs;
   1.141 +    val {lexicon, logtypes, gram, prtabs, ...} = tabs;
   1.142    in
   1.143 -    Pretty.writeln (Pretty.big_list "chartrans:" (pretty_chartrans chartrans));
   1.144      Pretty.writeln (pretty_strs_qs "lexicon:" (dest_lexicon lexicon));
   1.145      Pretty.writeln (Pretty.strs ("logtypes:" :: logtypes));
   1.146      Pretty.writeln (Pretty.big_list "prods:" (pretty_gram gram));
   1.147 -    Pretty.writeln (pretty_strs_qs "printer modes:" (prmodes_of prtabs))
   1.148 +    Pretty.writeln (pretty_strs_qs "print modes:" (prmodes_of prtabs))
   1.149    end;
   1.150  
   1.151  
   1.152 @@ -442,6 +433,8 @@
   1.153  
   1.154  val extend_trfuns = ext_syntax syn_ext_trfuns ("", true);
   1.155  
   1.156 +val extend_trfunsT = ext_syntax syn_ext_trfunsT ("", true);
   1.157 +
   1.158  fun extend_trrules syn rules =
   1.159    ext_syntax syn_ext_rules ("", true) syn (prep_rules (read_pattern syn) rules);
   1.160  
   1.161 @@ -449,9 +442,4 @@
   1.162    ext_syntax syn_ext_rules ("", true) syn (prep_rules I rules);
   1.163  
   1.164  
   1.165 -
   1.166 -(* FIXME test only *)
   1.167 -
   1.168 -fun prtabs_of (Syntax {prtabs, ...}) = prtabs;
   1.169 -
   1.170  end;