added chartrans;
authorwenzelm
Tue Dec 10 13:02:02 1996 +0100 (1996-12-10)
changeset 2366a163d2be1bb5
parent 2365 38295260a740
child 2367 eba760ebe315
added chartrans;
prmode: added 'inout' option;
src/Pure/Syntax/syntax.ML
     1.1 --- a/src/Pure/Syntax/syntax.ML	Tue Dec 10 13:00:52 1996 +0100
     1.2 +++ b/src/Pure/Syntax/syntax.ML	Tue Dec 10 13:02:02 1996 +0100
     1.3 @@ -31,7 +31,7 @@
     1.4    type syntax
     1.5    val extend_log_types: syntax -> string list -> syntax
     1.6    val extend_type_gram: syntax -> (string * int * mixfix) list -> syntax
     1.7 -  val extend_const_gram: syntax -> string -> (string * typ * mixfix) list -> syntax
     1.8 +  val extend_const_gram: syntax -> string * bool -> (string * typ * mixfix) list -> syntax
     1.9    val extend_consts: syntax -> string list -> syntax
    1.10    val extend_trfuns: syntax ->
    1.11      (string * (ast list -> ast)) list *
    1.12 @@ -57,6 +57,7 @@
    1.13    val simple_string_of_typ: typ -> string
    1.14    val simple_pprint_typ: typ -> pprint_args -> unit
    1.15    val ambiguity_level: int ref
    1.16 +  val prtabs_of: syntax -> Printer.prtabs   (* FIXME test only *)
    1.17    end;
    1.18  
    1.19  structure Syntax : SYNTAX =
    1.20 @@ -124,6 +125,7 @@
    1.21  
    1.22  datatype syntax =
    1.23    Syntax of {
    1.24 +    chartrans: (string * string) list,
    1.25      lexicon: lexicon,
    1.26      logtypes: string list,
    1.27      gram: gram,
    1.28 @@ -141,6 +143,7 @@
    1.29  
    1.30  val empty_syntax =
    1.31    Syntax {
    1.32 +    chartrans = [],
    1.33      lexicon = empty_lexicon,
    1.34      logtypes = [],
    1.35      gram = empty_gram,
    1.36 @@ -156,19 +159,21 @@
    1.37  
    1.38  (* extend_syntax *)
    1.39  
    1.40 -fun extend_syntax prmode (Syntax tabs) syn_ext =
    1.41 +fun extend_syntax (mode, inout) (Syntax tabs) syn_ext =
    1.42    let
    1.43 -    val {lexicon, logtypes = logtypes1, gram, consts = consts1, parse_ast_trtab,
    1.44 -      parse_ruletab, parse_trtab, print_trtab, print_ruletab, print_ast_trtab,
    1.45 -      prtabs} = tabs;
    1.46 +    val {chartrans = _, lexicon, logtypes = logtypes1, gram, consts = consts1,
    1.47 +      parse_ast_trtab, parse_ruletab, parse_trtab, print_trtab, print_ruletab,
    1.48 +      print_ast_trtab, prtabs} = tabs;
    1.49      val SynExt {logtypes = logtypes2, xprods, consts = consts2, parse_ast_translation,
    1.50        parse_rules, parse_translation, print_translation, print_rules,
    1.51        print_ast_translation} = syn_ext;
    1.52 +    val prtabs' = extend_prtabs prtabs mode xprods;
    1.53    in
    1.54      Syntax {
    1.55 -      lexicon = if prmode = "" then extend_lexicon lexicon (delims_of xprods) else lexicon,
    1.56 +      chartrans = chartrans_of prtabs',
    1.57 +      lexicon = if inout then extend_lexicon lexicon (delims_of xprods) else lexicon,
    1.58        logtypes = extend_list logtypes1 logtypes2,
    1.59 -      gram = if prmode = "" then extend_gram gram xprods else gram,
    1.60 +      gram = if inout then extend_gram gram xprods else gram,
    1.61        consts = consts2 union consts1,
    1.62        parse_ast_trtab =
    1.63          extend_trtab parse_ast_trtab parse_ast_translation "parse ast translation",
    1.64 @@ -178,7 +183,7 @@
    1.65        print_ruletab = extend_ruletab print_ruletab print_rules,
    1.66        print_ast_trtab =
    1.67          extend_trtab print_ast_trtab print_ast_translation "print ast translation",
    1.68 -      prtabs = extend_prtabs prtabs prmode xprods}
    1.69 +      prtabs = prtabs'}
    1.70    end;
    1.71  
    1.72  
    1.73 @@ -186,19 +191,21 @@
    1.74  
    1.75  fun merge_syntaxes (Syntax tabs1) (Syntax tabs2) =
    1.76    let
    1.77 -    val {lexicon = lexicon1, logtypes = logtypes1, gram = gram1, consts = consts1,
    1.78 -      parse_ast_trtab = parse_ast_trtab1, parse_ruletab = parse_ruletab1,
    1.79 +    val {chartrans = _, lexicon = lexicon1, logtypes = logtypes1, gram = gram1,
    1.80 +      consts = consts1, parse_ast_trtab = parse_ast_trtab1, parse_ruletab = parse_ruletab1,
    1.81        parse_trtab = parse_trtab1, print_trtab = print_trtab1,
    1.82        print_ruletab = print_ruletab1, print_ast_trtab = print_ast_trtab1,
    1.83        prtabs = prtabs1} = tabs1;
    1.84  
    1.85 -    val {lexicon = lexicon2, logtypes = logtypes2, gram = gram2, consts = consts2,
    1.86 -      parse_ast_trtab = parse_ast_trtab2, parse_ruletab = parse_ruletab2,
    1.87 +    val {chartrans = _, lexicon = lexicon2, logtypes = logtypes2, gram = gram2,
    1.88 +      consts = consts2, parse_ast_trtab = parse_ast_trtab2, parse_ruletab = parse_ruletab2,
    1.89        parse_trtab = parse_trtab2, print_trtab = print_trtab2,
    1.90        print_ruletab = print_ruletab2, print_ast_trtab = print_ast_trtab2,
    1.91        prtabs = prtabs2} = tabs2;
    1.92 +    val prtabs = merge_prtabs prtabs1 prtabs2;
    1.93    in
    1.94      Syntax {
    1.95 +      chartrans = chartrans_of prtabs,
    1.96        lexicon = merge_lexicons lexicon1 lexicon2,
    1.97        logtypes = merge_lists logtypes1 logtypes2,
    1.98        gram = merge_grams gram1 gram2,
    1.99 @@ -211,14 +218,14 @@
   1.100        print_ruletab = merge_ruletabs print_ruletab1 print_ruletab2,
   1.101        print_ast_trtab =
   1.102          merge_trtabs print_ast_trtab1 print_ast_trtab2 "print ast translation",
   1.103 -      prtabs = merge_prtabs prtabs1 prtabs2}
   1.104 +      prtabs = prtabs}
   1.105    end;
   1.106  
   1.107  
   1.108  (* type_syn *)
   1.109  
   1.110 -val type_syn = extend_syntax "" empty_syntax type_ext;
   1.111 -val pure_syn = extend_syntax "" type_syn pure_ext;
   1.112 +val type_syn = extend_syntax ("", true) empty_syntax type_ext;
   1.113 +val pure_syn = extend_syntax ("", true) type_syn pure_ext;
   1.114  
   1.115  
   1.116  (** inspect syntax **)
   1.117 @@ -231,8 +238,12 @@
   1.118  
   1.119  fun print_gram (Syntax tabs) =
   1.120    let
   1.121 -    val {lexicon, logtypes, gram, prtabs, ...} = tabs;
   1.122 +    val pretty_chartrans =
   1.123 +      map (fn (c, s) => Pretty.str (c ^ " -> " ^ quote s));
   1.124 +
   1.125 +    val {chartrans, lexicon, logtypes, gram, prtabs, ...} = tabs;
   1.126    in
   1.127 +    Pretty.writeln (Pretty.big_list "chartrans:" (pretty_chartrans chartrans));
   1.128      Pretty.writeln (pretty_strs_qs "lexicon:" (dest_lexicon lexicon));
   1.129      Pretty.writeln (Pretty.strs ("logtypes:" :: logtypes));
   1.130      Pretty.writeln (Pretty.big_list "prods:" (pretty_gram gram));
   1.131 @@ -277,7 +288,8 @@
   1.132    let
   1.133      val {lexicon, gram, parse_ast_trtab, parse_ruletab, ...} = tabs;
   1.134  
   1.135 -    val toks = tokenize lexicon false str;
   1.136 +    val chars = SymbolFont.read_charnames (explode str);
   1.137 +    val toks = tokenize lexicon false chars;
   1.138      val _ = writeln ("tokens: " ^ space_implode " " (map display_token toks));
   1.139  
   1.140      fun show_pt pt =
   1.141 @@ -300,7 +312,8 @@
   1.142    let
   1.143      val {lexicon, gram, parse_ast_trtab, logtypes, ...} = tabs;
   1.144      val root' = if root mem logtypes then logic else root;
   1.145 -    val pts = parse gram root' (tokenize lexicon xids str);
   1.146 +    val chars = SymbolFont.read_charnames (explode str);
   1.147 +    val pts = parse gram root' (tokenize lexicon xids chars);
   1.148  
   1.149      fun show_pt pt = writeln (str_of_ast (pt_to_ast (K None) pt));
   1.150    in
   1.151 @@ -419,20 +432,26 @@
   1.152  
   1.153  
   1.154  fun extend_log_types syn logtypes =
   1.155 -  extend_syntax "" syn (syn_ext_logtypes logtypes);
   1.156 +  extend_syntax ("", true) syn (syn_ext_logtypes logtypes);
   1.157  
   1.158 -val extend_type_gram = ext_syntax syn_ext_types "";
   1.159 +val extend_type_gram = ext_syntax syn_ext_types ("", true);
   1.160  
   1.161  fun extend_const_gram syn prmode = ext_syntax syn_ext_consts prmode syn;
   1.162  
   1.163 -val extend_consts = ext_syntax syn_ext_const_names "";
   1.164 +val extend_consts = ext_syntax syn_ext_const_names ("", true);
   1.165  
   1.166 -val extend_trfuns = ext_syntax syn_ext_trfuns "";
   1.167 +val extend_trfuns = ext_syntax syn_ext_trfuns ("", true);
   1.168  
   1.169  fun extend_trrules syn rules =
   1.170 -  ext_syntax syn_ext_rules "" syn (prep_rules (read_pattern syn) rules);
   1.171 +  ext_syntax syn_ext_rules ("", true) syn (prep_rules (read_pattern syn) rules);
   1.172  
   1.173  fun extend_trrules_i syn rules =
   1.174 -  ext_syntax syn_ext_rules "" syn (prep_rules I rules);
   1.175 +  ext_syntax syn_ext_rules ("", true) syn (prep_rules I rules);
   1.176 +
   1.177 +
   1.178 +
   1.179 +(* FIXME test only *)
   1.180 +
   1.181 +fun prtabs_of (Syntax {prtabs, ...}) = prtabs;
   1.182  
   1.183  end;