src/Pure/Syntax/syntax.ML
author clasohm
Thu Sep 16 12:20:38 1993 +0200 (1993-09-16)
changeset 0 a5a9c433f639
child 18 c9ec452ff08f
permissions -rw-r--r--
Initial revision
clasohm@0
     1
(*  Title:      Pure/Syntax/syntax
clasohm@0
     2
    ID:         $Id$
clasohm@0
     3
    Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
clasohm@0
     4
*)
clasohm@0
     5
clasohm@0
     6
signature SYNTAX =
clasohm@0
     7
sig
clasohm@0
     8
  (* FIXME include AST0 (?) *)
clasohm@0
     9
  include LEXICON0
clasohm@0
    10
  include EXTENSION0
clasohm@0
    11
  include TYPE_EXT0
clasohm@0
    12
  include SEXTENSION1
clasohm@0
    13
  include PRINTER0
clasohm@0
    14
  structure Extension: EXTENSION
clasohm@0
    15
  structure Pretty: PRETTY
clasohm@0
    16
  local open Extension.XGram Extension.XGram.Ast in
clasohm@0
    17
    type syntax
clasohm@0
    18
    val print_gram: syntax -> unit
clasohm@0
    19
    val print_trans: syntax -> unit
clasohm@0
    20
    val print_syntax: syntax -> unit
clasohm@0
    21
    val read_ast: syntax -> string * string -> ast
clasohm@0
    22
    val read: syntax -> typ -> string -> term
clasohm@0
    23
    val pretty_term: syntax -> term -> Pretty.T
clasohm@0
    24
    val pretty_typ: syntax -> typ -> Pretty.T
clasohm@0
    25
    val string_of_term: syntax -> term -> string
clasohm@0
    26
    val string_of_typ: syntax -> typ -> string
clasohm@0
    27
    val type_syn: syntax
clasohm@0
    28
    val extend: syntax * (indexname -> sort) -> string list * string list * sext
clasohm@0
    29
      -> syntax
clasohm@0
    30
    val merge: syntax * syntax -> syntax
clasohm@0
    31
  end
clasohm@0
    32
end;
clasohm@0
    33
clasohm@0
    34
functor SyntaxFun(structure Symtab: SYMTAB and TypeExt: TYPE_EXT
clasohm@0
    35
  and Parser: PARSER and SExtension: SEXTENSION and Printer: PRINTER
clasohm@0
    36
  sharing TypeExt.Extension.XGram = Parser.XGram = Printer.XGram
clasohm@0
    37
  and TypeExt.Extension = SExtension.Extension
clasohm@0
    38
  and Parser.ParseTree.Ast = Parser.XGram.Ast)(*: SYNTAX *) = (* FIXME *)
clasohm@0
    39
struct
clasohm@0
    40
clasohm@0
    41
structure Extension = TypeExt.Extension;
clasohm@0
    42
structure XGram = Extension.XGram;
clasohm@0
    43
structure Lexicon = Parser.ParseTree.Lexicon;
clasohm@0
    44
open Lexicon Extension TypeExt SExtension Printer XGram XGram.Ast;
clasohm@0
    45
clasohm@0
    46
clasohm@0
    47
fun lookup tab a = Symtab.lookup (tab, a);
clasohm@0
    48
clasohm@0
    49
clasohm@0
    50
clasohm@0
    51
(** datatype syntax **)
clasohm@0
    52
clasohm@0
    53
datatype tables =
clasohm@0
    54
  Tab of {
clasohm@0
    55
    gram: Parser.Gram,
clasohm@0
    56
    lexicon: Lexicon,
clasohm@0
    57
    const_tab: unit Symtab.table,
clasohm@0
    58
    parse_ast_trtab: (ast list -> ast) Symtab.table,
clasohm@0
    59
    parse_preproc: ast -> ast,
clasohm@0
    60
    parse_ruletab: (ast * ast) list Symtab.table,
clasohm@0
    61
    parse_postproc: ast -> ast,
clasohm@0
    62
    parse_trtab: (term list -> term) Symtab.table,
clasohm@0
    63
    print_trtab: (term list -> term) Symtab.table,
clasohm@0
    64
    print_preproc: ast -> ast,
clasohm@0
    65
    print_ruletab: (ast * ast) list Symtab.table,
clasohm@0
    66
    print_postproc: ast -> ast,
clasohm@0
    67
    print_tab: Printer.tab};
clasohm@0
    68
clasohm@0
    69
datatype gramgraph =
clasohm@0
    70
  EmptyGG |
clasohm@0
    71
  ExtGG of gramgraph ref * (ext * synrules) |
clasohm@0
    72
  MergeGG of gramgraph ref * gramgraph ref;
clasohm@0
    73
clasohm@0
    74
datatype syntax = Syntax of gramgraph ref * tables;
clasohm@0
    75
clasohm@0
    76
clasohm@0
    77
clasohm@0
    78
(*** compile syntax ***)
clasohm@0
    79
clasohm@0
    80
(* ggr_to_xgram *)
clasohm@0
    81
clasohm@0
    82
fun ggr_to_xgram ggr =
clasohm@0
    83
  let
clasohm@0
    84
    fun flatGG ggr (xg, v) =
clasohm@0
    85
      if ggr mem v then (xg, v) else flatGG' ggr (xg, ggr :: v)
clasohm@0
    86
    and flatGG' (ref EmptyGG) xgv = xgv
clasohm@0
    87
      | flatGG' (ref (ExtGG (ggr, ext))) xgv =
clasohm@0
    88
          let
clasohm@0
    89
            val (xg', v') = flatGG ggr xgv
clasohm@0
    90
          in
clasohm@0
    91
            (Extension.extend xg' ext, v')
clasohm@0
    92
          end
clasohm@0
    93
      | flatGG' (ref (MergeGG (ggr1, ggr2))) xgv =
clasohm@0
    94
          flatGG ggr1 (flatGG ggr2 xgv);
clasohm@0
    95
  in
clasohm@0
    96
    fst (flatGG ggr (Extension.empty, []))
clasohm@0
    97
  end;
clasohm@0
    98
clasohm@0
    99
clasohm@0
   100
(* mk_ruletab *)
clasohm@0
   101
clasohm@0
   102
fun mk_ruletab rules =
clasohm@0
   103
  let
clasohm@0
   104
    fun add_rule (r, tab) =
clasohm@0
   105
      let
clasohm@0
   106
        val a = head_of_rule r
clasohm@0
   107
      in
clasohm@0
   108
        case lookup tab a of
clasohm@0
   109
          None => Symtab.update ((a, [r]), tab)
clasohm@0
   110
        | Some rs => Symtab.update ((a, r :: rs), tab)
clasohm@0
   111
      end;
clasohm@0
   112
  in
clasohm@0
   113
    Symtab.balance (foldr add_rule (rules, Symtab.null))
clasohm@0
   114
  end;
clasohm@0
   115
clasohm@0
   116
clasohm@0
   117
(* make_syntax *)
clasohm@0
   118
clasohm@0
   119
fun make_syntax ggr =
clasohm@0
   120
  let
clasohm@0
   121
    fun mk_const_tab cs =
clasohm@0
   122
      Symtab.balance
clasohm@0
   123
        (Symtab.st_of_alist ((map (fn c => (c, ())) cs), Symtab.null));
clasohm@0
   124
clasohm@0
   125
    fun mk_trtab alst name =
clasohm@0
   126
      Symtab.balance (Symtab.st_of_alist (alst, Symtab.null))
clasohm@0
   127
        handle Symtab.DUPLICATE s => error ("More than one " ^ name ^ " for " ^ quote s);
clasohm@0
   128
clasohm@0
   129
    fun mk_proc (Some f) = f
clasohm@0
   130
      | mk_proc None = I;
clasohm@0
   131
clasohm@0
   132
    fun all_strings (opl: string prod list): string list =
clasohm@0
   133
        flat (map (fn Prod (_, syn, _, _) => terminals syn) opl);
clasohm@0
   134
clasohm@0
   135
    fun str_to_tok (opl: string prod list, lex: Lexicon): Token prod list =
clasohm@0
   136
      map
clasohm@0
   137
        (fn Prod (t, syn, s, pa) =>
clasohm@0
   138
          Prod (t, translate (hd o tokenize lex) syn, s, pa))
clasohm@0
   139
        opl;
clasohm@0
   140
clasohm@0
   141
    fun xgram_to_tables (XGram xgram) =
clasohm@0
   142
      let
clasohm@0
   143
        val {roots, prods, consts, parse_ast_translation, parse_preproc, parse_rules,
clasohm@0
   144
          parse_postproc, parse_translation, print_translation, print_preproc,
clasohm@0
   145
          print_rules, print_postproc, print_ast_translation} = xgram;
clasohm@0
   146
        val lexicon = mk_lexicon (all_strings prods);
clasohm@0
   147
      in
clasohm@0
   148
        Tab {
clasohm@0
   149
          gram = Parser.compile_xgram (roots, str_to_tok (prods, lexicon)),
clasohm@0
   150
          lexicon = lexicon,
clasohm@0
   151
          const_tab = mk_const_tab consts,
clasohm@0
   152
          parse_ast_trtab = mk_trtab parse_ast_translation "parse ast translation",
clasohm@0
   153
          parse_preproc = mk_proc parse_preproc,
clasohm@0
   154
          parse_ruletab = mk_ruletab parse_rules,
clasohm@0
   155
          parse_postproc = mk_proc parse_postproc,
clasohm@0
   156
          parse_trtab = mk_trtab parse_translation "parse translation",
clasohm@0
   157
          print_trtab = mk_trtab print_translation "print translation",
clasohm@0
   158
          print_preproc = mk_proc print_preproc,
clasohm@0
   159
          print_ruletab = mk_ruletab print_rules,
clasohm@0
   160
          print_postproc = mk_proc print_postproc,
clasohm@0
   161
          print_tab = mk_print_tab prods
clasohm@0
   162
            (mk_trtab print_ast_translation "print ast translation")}
clasohm@0
   163
      end;
clasohm@0
   164
  in
clasohm@0
   165
    Syntax (ggr, xgram_to_tables (ggr_to_xgram ggr))
clasohm@0
   166
  end;
clasohm@0
   167
clasohm@0
   168
clasohm@0
   169
(* add_synrules *)
clasohm@0
   170
clasohm@0
   171
fun add_synrules (Tab tabs) (SynRules rules) =
clasohm@0
   172
  let
clasohm@0
   173
    val {gram, lexicon, const_tab, parse_ast_trtab, parse_preproc, parse_ruletab,
clasohm@0
   174
      parse_postproc, parse_trtab, print_trtab, print_preproc, print_ruletab,
clasohm@0
   175
      print_postproc, print_tab} = tabs;
clasohm@0
   176
    val {parse_rules, print_rules} = rules;
clasohm@0
   177
    val parse_rs = flat (map snd (Symtab.alist_of parse_ruletab)) @ parse_rules;
clasohm@0
   178
    val print_rs = flat (map snd (Symtab.alist_of print_ruletab)) @ print_rules;
clasohm@0
   179
  in
clasohm@0
   180
    Tab {
clasohm@0
   181
      gram = gram, lexicon = lexicon, const_tab = const_tab,
clasohm@0
   182
      parse_ast_trtab = parse_ast_trtab,
clasohm@0
   183
      parse_preproc = parse_preproc,
clasohm@0
   184
      parse_ruletab = mk_ruletab parse_rs,
clasohm@0
   185
      parse_postproc = parse_postproc,
clasohm@0
   186
      parse_trtab = parse_trtab,
clasohm@0
   187
      print_trtab = print_trtab,
clasohm@0
   188
      print_preproc = print_preproc,
clasohm@0
   189
      print_ruletab = mk_ruletab print_rs,
clasohm@0
   190
      print_postproc = print_postproc,
clasohm@0
   191
      print_tab = print_tab}
clasohm@0
   192
  end;
clasohm@0
   193
clasohm@0
   194
clasohm@0
   195
clasohm@0
   196
(*** inspect syntax ***)
clasohm@0
   197
clasohm@0
   198
(* print_syntax_old *) (* FIXME remove *)
clasohm@0
   199
clasohm@0
   200
fun print_syntax_old (Syntax (_, Tab {gram, lexicon, ...})) =
clasohm@0
   201
  Parser.print_gram (gram, lexicon);
clasohm@0
   202
clasohm@0
   203
clasohm@0
   204
clasohm@0
   205
fun xgram_of (Syntax (ggr, _)) = ggr_to_xgram ggr;
clasohm@0
   206
clasohm@0
   207
fun string_of_big_list name prts =
clasohm@0
   208
  Pretty.string_of (Pretty.blk (2,
clasohm@0
   209
    separate Pretty.fbrk (Pretty.str name :: prts)));
clasohm@0
   210
clasohm@0
   211
clasohm@0
   212
(* print_gram *)    (* FIXME check *)
clasohm@0
   213
clasohm@0
   214
fun prt_gram (XGram {roots, prods, ...}) =
clasohm@0
   215
  let
clasohm@0
   216
    fun pretty_name name = [Pretty.str (name ^ " ="), Pretty.brk 1];
clasohm@0
   217
clasohm@0
   218
    fun pretty_xsymbs (Terminal s :: xs) =
clasohm@0
   219
          Pretty.str (quote s) :: Pretty.brk 1 :: pretty_xsymbs xs
clasohm@0
   220
      | pretty_xsymbs (Nonterminal (s, p) :: xs) =
clasohm@0
   221
          (if is_terminal s then Pretty.str s
clasohm@0
   222
          else Pretty.str (s ^ "[" ^ string_of_int p ^ "]"))
clasohm@0
   223
            :: Pretty.brk 1 :: pretty_xsymbs xs
clasohm@0
   224
      | pretty_xsymbs (_ :: xs) = pretty_xsymbs xs
clasohm@0
   225
      | pretty_xsymbs [] = [];
clasohm@0
   226
clasohm@0
   227
    fun pretty_const "" = [Pretty.brk 1]
clasohm@0
   228
      | pretty_const c = [Pretty.str (" => " ^ quote c), Pretty.brk 1];
clasohm@0
   229
clasohm@0
   230
    fun pretty_pri p = [Pretty.str ("(" ^ string_of_int p ^ ")")];
clasohm@0
   231
clasohm@0
   232
    fun pretty_prod (Prod (name, xsymbs, const, pri)) =
clasohm@0
   233
      Pretty.blk (2, pretty_name name @ pretty_xsymbs xsymbs @
clasohm@0
   234
        pretty_const const @ pretty_pri pri);
clasohm@0
   235
  in
clasohm@0
   236
    writeln (Pretty.string_of (Pretty.blk (2,
clasohm@0
   237
      separate (Pretty.brk 1) (map Pretty.str ("roots:" :: roots)))));
clasohm@0
   238
    writeln (string_of_big_list "prods:" (map pretty_prod prods))
clasohm@0
   239
  end;
clasohm@0
   240
clasohm@0
   241
clasohm@0
   242
val print_gram = prt_gram o xgram_of;
clasohm@0
   243
clasohm@0
   244
clasohm@0
   245
(* print_trans *)   (* FIXME check *)
clasohm@0
   246
clasohm@0
   247
fun prt_trans (XGram xgram) =
clasohm@0
   248
  let
clasohm@0
   249
    fun string_of_strings name strs =
clasohm@0
   250
      Pretty.string_of (Pretty.blk (2,
clasohm@0
   251
        separate (Pretty.brk 1) (map Pretty.str (name :: map quote strs))));
clasohm@0
   252
clasohm@0
   253
    fun string_of_trs name trs = string_of_strings name (map fst trs);
clasohm@0
   254
clasohm@0
   255
    fun string_of_proc name proc =
clasohm@0
   256
      Pretty.string_of (Pretty.blk (2, [Pretty.str name, Pretty.brk 1,
clasohm@0
   257
        Pretty.str (if is_none proc then "None" else "Some fn")]));
clasohm@0
   258
clasohm@0
   259
    fun string_of_rules name rules =
clasohm@0
   260
      string_of_big_list name (map pretty_rule rules);
clasohm@0
   261
clasohm@0
   262
clasohm@0
   263
    val {consts, parse_ast_translation, parse_preproc, parse_rules,
clasohm@0
   264
      parse_postproc, parse_translation, print_translation, print_preproc,
clasohm@0
   265
      print_rules, print_postproc, print_ast_translation, ...} = xgram;
clasohm@0
   266
  in
clasohm@0
   267
    writeln (string_of_strings "consts:" consts);
clasohm@0
   268
    writeln (string_of_trs "parse_ast_translation:" parse_ast_translation);
clasohm@0
   269
    writeln (string_of_proc "parse_preproc:" parse_preproc);
clasohm@0
   270
    writeln (string_of_rules "parse_rules:" parse_rules);
clasohm@0
   271
    writeln (string_of_proc "parse_postproc:" parse_postproc);
clasohm@0
   272
    writeln (string_of_trs "parse_translation:" parse_translation);
clasohm@0
   273
    writeln (string_of_trs "print_translation:" print_translation);
clasohm@0
   274
    writeln (string_of_proc "print_preproc:" print_preproc);
clasohm@0
   275
    writeln (string_of_rules "print_rules:" print_rules);
clasohm@0
   276
    writeln (string_of_proc "print_postproc:" print_postproc);
clasohm@0
   277
    writeln (string_of_trs "print_ast_translation:" print_ast_translation)
clasohm@0
   278
  end;
clasohm@0
   279
clasohm@0
   280
clasohm@0
   281
val print_trans = prt_trans o xgram_of;
clasohm@0
   282
clasohm@0
   283
clasohm@0
   284
(* print_syntax *)
clasohm@0
   285
clasohm@0
   286
fun print_syntax syn =
clasohm@0
   287
  let
clasohm@0
   288
    val xgram = xgram_of syn;
clasohm@0
   289
  in
clasohm@0
   290
    prt_gram xgram; prt_trans xgram
clasohm@0
   291
  end;
clasohm@0
   292
clasohm@0
   293
clasohm@0
   294
clasohm@0
   295
(*** parsing and printing ***)
clasohm@0
   296
clasohm@0
   297
(* read_ast *)
clasohm@0
   298
clasohm@0
   299
fun read_ast syn (root, s) =
clasohm@0
   300
  let
clasohm@0
   301
    val Syntax (_, Tab {gram, lexicon, parse_ast_trtab, ...}) = syn;
clasohm@0
   302
    val root = if Parser.parsable (gram, root) then root else error ("Unparsable root " ^ root) (* Extension.logic *);    (* FIXME *)
clasohm@0
   303
    fun syn_err toks =
clasohm@0
   304
      error ("Syntax error at\n" ^ space_implode " " (map token_to_string toks));
clasohm@0
   305
  in
clasohm@0
   306
    Parser.ParseTree.pt_to_ast (lookup parse_ast_trtab)
clasohm@0
   307
      (Parser.parse (gram, root, tokenize lexicon s))
clasohm@0
   308
        handle Parser.SYNTAX_ERR toks => syn_err toks
clasohm@0
   309
  end;
clasohm@0
   310
clasohm@0
   311
clasohm@0
   312
(* norm_ast *)
clasohm@0
   313
clasohm@0
   314
fun norm_ast ruletab ast =
clasohm@0
   315
  let
clasohm@0
   316
    fun get_rules a =
clasohm@0
   317
      (case lookup ruletab a of
clasohm@0
   318
        Some rules => rules
clasohm@0
   319
      | None => []);
clasohm@0
   320
  in
clasohm@0
   321
    normalize (if Symtab.is_null ruletab then None else Some get_rules) ast
clasohm@0
   322
  end;
clasohm@0
   323
clasohm@0
   324
clasohm@0
   325
clasohm@0
   326
(** read **)
clasohm@0
   327
clasohm@0
   328
fun read (syn as Syntax (_, Tab tabs)) ty s =
clasohm@0
   329
  let
clasohm@0
   330
    val {parse_preproc, parse_ruletab, parse_postproc, parse_trtab, ...} = tabs;
clasohm@0
   331
    val ast = read_ast syn (typ_to_nt ty, s);
clasohm@0
   332
  in
clasohm@0
   333
    ast_to_term (lookup parse_trtab)
clasohm@0
   334
      (parse_postproc (norm_ast parse_ruletab (parse_preproc ast)))
clasohm@0
   335
  end;
clasohm@0
   336
clasohm@0
   337
clasohm@0
   338
clasohm@0
   339
(** pprint_ast **)
clasohm@0
   340
clasohm@0
   341
val pprint_ast = Pretty.pprint o pretty_ast;
clasohm@0
   342
clasohm@0
   343
clasohm@0
   344
clasohm@0
   345
(** pretty term, typ **)
clasohm@0
   346
clasohm@0
   347
fun pretty_t t_to_ast pretty_t (syn as Syntax (_, Tab tabs)) t =
clasohm@0
   348
  let
clasohm@0
   349
    val {print_trtab, print_preproc, print_ruletab, print_postproc, print_tab, ...} = tabs;
clasohm@0
   350
    val ast = t_to_ast (lookup print_trtab) t;
clasohm@0
   351
  in
clasohm@0
   352
    pretty_t print_tab
clasohm@0
   353
      (print_postproc (norm_ast print_ruletab (print_preproc ast)))
clasohm@0
   354
  end;
clasohm@0
   355
clasohm@0
   356
val pretty_term = pretty_t term_to_ast pretty_term_ast;
clasohm@0
   357
clasohm@0
   358
val pretty_typ = pretty_t typ_to_ast pretty_typ_ast;
clasohm@0
   359
clasohm@0
   360
fun string_of_term syn t = Pretty.string_of (pretty_term syn t);
clasohm@0
   361
clasohm@0
   362
fun string_of_typ syn ty = Pretty.string_of (pretty_typ syn ty);
clasohm@0
   363
clasohm@0
   364
clasohm@0
   365
clasohm@0
   366
(*** build syntax ***)
clasohm@0
   367
clasohm@0
   368
(* type_syn *)
clasohm@0
   369
clasohm@0
   370
val type_syn = make_syntax (ref (ExtGG (ref EmptyGG, (type_ext, empty_synrules))));
clasohm@0
   371
clasohm@0
   372
clasohm@0
   373
(* extend *)  (* FIXME check *)
clasohm@0
   374
clasohm@0
   375
fun extend (old_syn as Syntax (ggr, _), def_sort) (roots, xconsts, sext) =
clasohm@0
   376
  let
clasohm@0
   377
    fun read_typ s = typ_of_term def_sort (read old_syn typeT s);
clasohm@0
   378
    val ext = ext_of_sext roots xconsts read_typ sext;
clasohm@0
   379
clasohm@0
   380
    fun right_rule (xpat1 |-> xpat2) = Some (xpat1, xpat2)
clasohm@0
   381
      | right_rule (xpat1 <-| xpat2) = None
clasohm@0
   382
      | right_rule (xpat1 <-> xpat2) = Some (xpat1, xpat2);
clasohm@0
   383
clasohm@0
   384
    fun left_rule (xpat1 |-> xpat2) = None
clasohm@0
   385
      | left_rule (xpat1 <-| xpat2) = Some (xpat2, xpat1)
clasohm@0
   386
      | left_rule (xpat1 <-> xpat2) = Some (xpat2, xpat1);
clasohm@0
   387
clasohm@0
   388
    val (tmp_syn as Syntax (_, tmp_tabs)) =
clasohm@0
   389
      make_syntax (ref (ExtGG (ggr, (ext, empty_synrules))));
clasohm@0
   390
    val Syntax (_, Tab {const_tab, ...}) = tmp_syn;
clasohm@0
   391
clasohm@0
   392
    fun constantify (ast as (Constant _)) = ast
clasohm@0
   393
      | constantify (ast as (Variable x)) =
clasohm@0
   394
          if is_some (lookup const_tab x) then Constant x else ast
clasohm@0
   395
      | constantify (Appl asts) = Appl (map constantify asts);
clasohm@0
   396
clasohm@0
   397
    fun read_pat (r_s as (root, s)) =
clasohm@0
   398
      constantify ((read_ast tmp_syn r_s)
clasohm@0
   399
        handle ERROR => error ("The error above occurred in " ^ quote s));
clasohm@0
   400
clasohm@0
   401
    fun read_rule (xrule as ((_, lhs_src), (_, rhs_src))) =
clasohm@0
   402
      let
clasohm@0
   403
        val rule as (lhs, rhs) = (pairself read_pat) xrule;
clasohm@0
   404
      in
clasohm@0
   405
        case rule_error rule of
clasohm@0
   406
          Some msg =>
clasohm@0
   407
            error ("Error in syntax translation rule: " ^ msg ^
clasohm@0
   408
              "\nexternal: " ^ quote lhs_src ^ "  ->  " ^ quote rhs_src ^
clasohm@0
   409
              "\ninternal: " ^ str_of_ast lhs ^ "  ->  " ^ str_of_ast rhs)
clasohm@0
   410
        | None => rule
clasohm@0
   411
      end;
clasohm@0
   412
clasohm@0
   413
    val xrules = xrules_of sext;
clasohm@0
   414
    val new_rules =
clasohm@0
   415
      SynRules {
clasohm@0
   416
        parse_rules = map read_rule (mapfilter right_rule xrules),
clasohm@0
   417
        print_rules = map read_rule (mapfilter left_rule xrules)};
clasohm@0
   418
  in
clasohm@0
   419
    Syntax (ref (ExtGG (ggr, (ext, new_rules))), add_synrules tmp_tabs new_rules)
clasohm@0
   420
  end;
clasohm@0
   421
clasohm@0
   422
clasohm@0
   423
(* merge *)
clasohm@0
   424
clasohm@0
   425
fun merge (Syntax (ggr1, _), Syntax (ggr2, _)) =
clasohm@0
   426
  make_syntax (ref (MergeGG (ggr1, ggr2)));
clasohm@0
   427
clasohm@0
   428
clasohm@0
   429
end;
clasohm@0
   430