src/Pure/Syntax/syntax.ML
author wenzelm
Wed Jan 19 14:21:26 1994 +0100 (1994-01-19)
changeset 237 a7d3e712767a
parent 175 c02750f7f604
child 260 967813b8a7bf
permissions -rw-r--r--
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
now much leaner (eliminated gramgraph, all data except tables of old
parser are shared); simplified the internal interfaces for syntax
extension;
wenzelm@18
     1
(*  Title:      Pure/Syntax/syntax.ML
clasohm@0
     2
    ID:         $Id$
clasohm@0
     3
    Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
wenzelm@18
     4
wenzelm@18
     5
Root of Isabelle's syntax module.
clasohm@0
     6
*)
clasohm@0
     7
clasohm@0
     8
signature SYNTAX =
clasohm@0
     9
sig
wenzelm@18
    10
  include AST0
clasohm@0
    11
  include LEXICON0
wenzelm@237
    12
  include SYN_EXT0
clasohm@0
    13
  include TYPE_EXT0
clasohm@0
    14
  include SEXTENSION1
clasohm@0
    15
  include PRINTER0
wenzelm@18
    16
  type syntax
wenzelm@18
    17
  val type_syn: syntax
wenzelm@144
    18
  val extend: syntax -> (string -> typ) -> string list * string list * sext -> syntax
wenzelm@167
    19
  val merge: string list -> syntax -> syntax -> syntax
wenzelm@18
    20
  val print_gram: syntax -> unit
wenzelm@18
    21
  val print_trans: syntax -> unit
wenzelm@18
    22
  val print_syntax: syntax -> unit
wenzelm@18
    23
  val test_read: syntax -> string -> string -> unit
wenzelm@18
    24
  val read: syntax -> typ -> string -> term
wenzelm@144
    25
  val read_typ: syntax -> (indexname -> sort) -> string -> typ
wenzelm@237
    26
  val simple_read_typ: string -> typ
wenzelm@18
    27
  val pretty_term: syntax -> term -> Pretty.T
wenzelm@18
    28
  val pretty_typ: syntax -> typ -> Pretty.T
wenzelm@18
    29
  val string_of_term: syntax -> term -> string
wenzelm@18
    30
  val string_of_typ: syntax -> typ -> string
clasohm@0
    31
end;
clasohm@0
    32
clasohm@0
    33
functor SyntaxFun(structure Symtab: SYMTAB and TypeExt: TYPE_EXT
wenzelm@237
    34
  and SExtension: SEXTENSION and Printer: PRINTER
wenzelm@237
    35
  sharing SExtension.Parser.SynExt = TypeExt.SynExt = Printer.SynExt)(*: SYNTAX *) = (* FIXME *)
clasohm@0
    36
struct
clasohm@0
    37
wenzelm@237
    38
structure SynExt = TypeExt.SynExt;
wenzelm@237
    39
structure Parser = SExtension.Parser;
wenzelm@237
    40
structure Lexicon = Parser.Lexicon;
wenzelm@237
    41
open Lexicon SynExt SynExt.Ast Parser TypeExt SExtension Printer;
wenzelm@237
    42
wenzelm@237
    43
wenzelm@237
    44
(** tables of translation functions **)
wenzelm@237
    45
wenzelm@237
    46
(*the ref serves as unique id*)
wenzelm@237
    47
type 'a trtab = (('a list -> 'a) * unit ref) Symtab.table;
wenzelm@237
    48
wenzelm@237
    49
val dest_trtab = Symtab.alist_of;
wenzelm@237
    50
wenzelm@237
    51
fun lookup_trtab tab c =
wenzelm@237
    52
  apsome fst (Symtab.lookup (tab, c));
clasohm@0
    53
clasohm@0
    54
wenzelm@237
    55
(* empty, extend, merge trtabs *)
wenzelm@237
    56
wenzelm@237
    57
fun err_dup_trfun name c =
wenzelm@237
    58
  error ("More than one " ^ name ^ " for " ^ quote c);
wenzelm@237
    59
wenzelm@237
    60
val empty_trtab = Symtab.null;
wenzelm@237
    61
wenzelm@237
    62
fun extend_trtab tab trfuns name =
wenzelm@237
    63
  Symtab.extend eq_snd (tab, map (fn (c, f) => (c, (f, ref ()))) trfuns)
wenzelm@237
    64
    handle Symtab.DUPLICATE c => err_dup_trfun name c;
wenzelm@237
    65
wenzelm@237
    66
fun merge_trtabs tab1 tab2 name =
wenzelm@237
    67
  Symtab.merge eq_snd (tab1, tab2)
wenzelm@237
    68
    handle Symtab.DUPLICATE c => err_dup_trfun name c;
wenzelm@237
    69
wenzelm@237
    70
wenzelm@237
    71
wenzelm@237
    72
(** tables of translation rules **)
wenzelm@237
    73
wenzelm@237
    74
type ruletab = (ast * ast) list Symtab.table;
wenzelm@237
    75
wenzelm@237
    76
fun dest_ruletab tab = flat (map snd (Symtab.alist_of tab));
wenzelm@237
    77
wenzelm@237
    78
wenzelm@237
    79
(* lookup_ruletab *)
wenzelm@237
    80
wenzelm@237
    81
fun lookup_ruletab tab =
wenzelm@237
    82
  if Symtab.is_null tab then None
wenzelm@237
    83
  else Some (fn a => Symtab.lookup_multi (tab, a));
wenzelm@237
    84
wenzelm@237
    85
wenzelm@237
    86
(* empty, extend, merge ruletabs *)
wenzelm@237
    87
wenzelm@237
    88
val empty_ruletab = Symtab.null;
wenzelm@237
    89
wenzelm@237
    90
fun extend_ruletab tab rules =
wenzelm@237
    91
  generic_extend (op =) Symtab.dest_multi Symtab.make_multi tab
wenzelm@237
    92
    (map (fn r => (head_of_rule r, r)) (distinct rules));
wenzelm@237
    93
wenzelm@237
    94
fun merge_ruletabs tab1 tab2 =
wenzelm@237
    95
  generic_merge (op =) Symtab.dest_multi Symtab.make_multi tab1 tab2;
clasohm@0
    96
clasohm@0
    97
clasohm@0
    98
clasohm@0
    99
(** datatype syntax **)
clasohm@0
   100
wenzelm@237
   101
datatype syntax =
wenzelm@237
   102
  Syntax of {
wenzelm@18
   103
    lexicon: lexicon,
wenzelm@18
   104
    roots: string list,
wenzelm@18
   105
    gram: gram,
wenzelm@18
   106
    consts: string list,
wenzelm@237
   107
    parse_ast_trtab: ast trtab,
wenzelm@237
   108
    parse_ruletab: ruletab,
wenzelm@237
   109
    parse_trtab: term trtab,
wenzelm@237
   110
    print_trtab: term trtab,
wenzelm@237
   111
    print_ruletab: ruletab,
wenzelm@237
   112
    print_ast_trtab: ast trtab,
wenzelm@18
   113
    prtab: prtab};
clasohm@0
   114
wenzelm@18
   115
wenzelm@237
   116
(* empty_syntax *)
wenzelm@18
   117
wenzelm@237
   118
val empty_syntax =
wenzelm@237
   119
  Syntax {
wenzelm@167
   120
    lexicon = empty_lexicon,
wenzelm@167
   121
    roots = [],
wenzelm@171
   122
    gram = empty_gram,
wenzelm@167
   123
    consts = [],
wenzelm@237
   124
    parse_ast_trtab = empty_trtab,
wenzelm@237
   125
    parse_ruletab = empty_ruletab,
wenzelm@237
   126
    parse_trtab = empty_trtab,
wenzelm@237
   127
    print_trtab = empty_trtab,
wenzelm@237
   128
    print_ruletab = empty_ruletab,
wenzelm@237
   129
    print_ast_trtab = empty_trtab,
wenzelm@167
   130
    prtab = empty_prtab};
wenzelm@167
   131
wenzelm@167
   132
wenzelm@237
   133
(* extend_syntax *)
wenzelm@167
   134
wenzelm@237
   135
fun extend_syntax (Syntax tabs) syn_ext =
wenzelm@167
   136
  let
wenzelm@167
   137
    val {lexicon, roots = roots1, gram, consts = consts1, parse_ast_trtab,
wenzelm@237
   138
      parse_ruletab, parse_trtab, print_trtab, print_ruletab, print_ast_trtab,
wenzelm@237
   139
      prtab} = tabs;
wenzelm@237
   140
    val SynExt {roots = roots2, xprods, consts = consts2, parse_ast_translation,
wenzelm@167
   141
      parse_rules, parse_translation, print_translation, print_rules,
wenzelm@237
   142
      print_ast_translation} = syn_ext;
wenzelm@167
   143
  in
wenzelm@237
   144
    Syntax {
wenzelm@237
   145
      lexicon = extend_lexicon lexicon (delims_of xprods),
wenzelm@237
   146
      roots = extend_list roots1 roots2,
wenzelm@237
   147
      gram = extend_gram gram roots2 xprods,
wenzelm@167
   148
      consts = consts2 union consts1,
wenzelm@167
   149
      parse_ast_trtab =
wenzelm@167
   150
        extend_trtab parse_ast_trtab parse_ast_translation "parse ast translation",
wenzelm@167
   151
      parse_ruletab = extend_ruletab parse_ruletab parse_rules,
wenzelm@167
   152
      parse_trtab = extend_trtab parse_trtab parse_translation "parse translation",
wenzelm@167
   153
      print_trtab = extend_trtab print_trtab print_translation "print translation",
wenzelm@167
   154
      print_ruletab = extend_ruletab print_ruletab print_rules,
wenzelm@237
   155
      print_ast_trtab =
wenzelm@237
   156
        extend_trtab print_ast_trtab print_ast_translation "print ast translation",
wenzelm@237
   157
      prtab = extend_prtab prtab xprods}
wenzelm@18
   158
  end;
wenzelm@18
   159
wenzelm@18
   160
wenzelm@237
   161
(* merge_syntaxes *)
clasohm@0
   162
wenzelm@237
   163
fun merge_syntaxes (Syntax tabs1) (Syntax tabs2) =
clasohm@0
   164
  let
wenzelm@237
   165
    val {lexicon = lexicon1, roots = roots1, gram = gram1, consts = consts1,
wenzelm@237
   166
      parse_ast_trtab = parse_ast_trtab1, parse_ruletab = parse_ruletab1,
wenzelm@237
   167
      parse_trtab = parse_trtab1, print_trtab = print_trtab1,
wenzelm@237
   168
      print_ruletab = print_ruletab1, print_ast_trtab = print_ast_trtab1,
wenzelm@237
   169
      prtab = prtab1} = tabs1;
wenzelm@237
   170
wenzelm@237
   171
    val {lexicon = lexicon2, roots = roots2, gram = gram2, consts = consts2,
wenzelm@237
   172
      parse_ast_trtab = parse_ast_trtab2, parse_ruletab = parse_ruletab2,
wenzelm@237
   173
      parse_trtab = parse_trtab2, print_trtab = print_trtab2,
wenzelm@237
   174
      print_ruletab = print_ruletab2, print_ast_trtab = print_ast_trtab2,
wenzelm@237
   175
      prtab = prtab2} = tabs2;
clasohm@0
   176
  in
wenzelm@237
   177
    Syntax {
wenzelm@237
   178
      lexicon = merge_lexicons lexicon1 lexicon2,
wenzelm@237
   179
      roots = merge_lists roots1 roots2,
wenzelm@237
   180
      gram = merge_grams gram1 gram2,
wenzelm@237
   181
      consts = merge_lists consts1 consts2,
wenzelm@237
   182
      parse_ast_trtab =
wenzelm@237
   183
        merge_trtabs parse_ast_trtab1 parse_ast_trtab2 "parse ast translation",
wenzelm@237
   184
      parse_ruletab = merge_ruletabs parse_ruletab1 parse_ruletab2,
wenzelm@237
   185
      parse_trtab = merge_trtabs parse_trtab1 parse_trtab2 "parse translation",
wenzelm@237
   186
      print_trtab = merge_trtabs print_trtab1 print_trtab2 "print translation",
wenzelm@237
   187
      print_ruletab = merge_ruletabs print_ruletab1 print_ruletab2,
wenzelm@237
   188
      print_ast_trtab =
wenzelm@237
   189
        merge_trtabs print_ast_trtab1 print_ast_trtab2 "print ast translation",
wenzelm@237
   190
      prtab = merge_prtabs prtab1 prtab2}
clasohm@0
   191
  end;
clasohm@0
   192
clasohm@0
   193
clasohm@0
   194
wenzelm@237
   195
(** inspect syntax **)
clasohm@0
   196
clasohm@0
   197
fun string_of_big_list name prts =
wenzelm@237
   198
  Pretty.string_of (Pretty.block (Pretty.fbreaks (Pretty.str name :: prts)));
clasohm@0
   199
wenzelm@18
   200
fun string_of_strings name strs =
wenzelm@237
   201
  Pretty.string_of (Pretty.block (Pretty.breaks
wenzelm@237
   202
    (map Pretty.str (name :: map quote (sort_strings strs)))));
clasohm@0
   203
wenzelm@18
   204
wenzelm@18
   205
(* print_gram *)
clasohm@0
   206
wenzelm@237
   207
fun print_gram (Syntax tabs) =
clasohm@0
   208
  let
wenzelm@237
   209
    val {lexicon, roots, gram, ...} = tabs;
clasohm@0
   210
  in
wenzelm@237
   211
    writeln (string_of_strings "lexicon:" (dest_lexicon lexicon));
wenzelm@237
   212
    writeln (Pretty.string_of (Pretty.block (Pretty.breaks
wenzelm@237
   213
      (map Pretty.str ("roots:" :: roots)))));
wenzelm@237
   214
    writeln (string_of_big_list "prods:" (pretty_gram gram))
clasohm@0
   215
  end;
clasohm@0
   216
clasohm@0
   217
wenzelm@18
   218
(* print_trans *)
clasohm@0
   219
wenzelm@237
   220
fun print_trans (Syntax tabs) =
clasohm@0
   221
  let
wenzelm@237
   222
    fun string_of_trtab name tab =
wenzelm@237
   223
      string_of_strings name (map fst (dest_trtab tab));
clasohm@0
   224
wenzelm@237
   225
    fun string_of_ruletab name tab =
wenzelm@237
   226
      string_of_big_list name (map pretty_rule (dest_ruletab tab));
clasohm@0
   227
wenzelm@237
   228
    val {consts, parse_ast_trtab, parse_ruletab, parse_trtab, print_trtab,
wenzelm@237
   229
      print_ruletab, print_ast_trtab, ...} = tabs;
clasohm@0
   230
  in
clasohm@0
   231
    writeln (string_of_strings "consts:" consts);
wenzelm@237
   232
    writeln (string_of_trtab "parse_ast_translation:" parse_ast_trtab);
wenzelm@237
   233
    writeln (string_of_ruletab "parse_rules:" parse_ruletab);
wenzelm@237
   234
    writeln (string_of_trtab "parse_translation:" parse_trtab);
wenzelm@237
   235
    writeln (string_of_trtab "print_translation:" print_trtab);
wenzelm@237
   236
    writeln (string_of_ruletab "print_rules:" print_ruletab);
wenzelm@237
   237
    writeln (string_of_trtab "print_ast_translation:" print_ast_trtab)
clasohm@0
   238
  end;
clasohm@0
   239
clasohm@0
   240
clasohm@0
   241
(* print_syntax *)
clasohm@0
   242
wenzelm@237
   243
fun print_syntax syn = (print_gram syn; print_trans syn);
clasohm@0
   244
clasohm@0
   245
clasohm@0
   246
wenzelm@237
   247
(** read **)
wenzelm@18
   248
wenzelm@18
   249
(* read_ast *)
wenzelm@18
   250
wenzelm@237
   251
fun read_ast (Syntax tabs) xids root str =
wenzelm@18
   252
  let
wenzelm@237
   253
    val {lexicon, gram, parse_ast_trtab, ...} = tabs;
wenzelm@18
   254
  in
wenzelm@237
   255
    pt_to_ast (lookup_trtab parse_ast_trtab)
wenzelm@18
   256
      (parse gram root (tokenize lexicon xids str))
clasohm@0
   257
  end;
clasohm@0
   258
clasohm@0
   259
wenzelm@237
   260
(* test_read *)
wenzelm@18
   261
wenzelm@237
   262
fun test_read (Syntax tabs) root str =
wenzelm@18
   263
  let
wenzelm@237
   264
    val {lexicon, gram, parse_ast_trtab, parse_ruletab, ...} = tabs;
wenzelm@18
   265
wenzelm@18
   266
    val toks = tokenize lexicon false str;
wenzelm@18
   267
    val _ = writeln ("tokens: " ^ space_implode " " (map display_token toks));
wenzelm@18
   268
wenzelm@18
   269
    val pt = parse gram root toks;
wenzelm@18
   270
    val raw_ast = pt_to_ast (K None) pt;
wenzelm@18
   271
    val _ = writeln ("raw: " ^ str_of_ast raw_ast);
wenzelm@18
   272
wenzelm@237
   273
    val pre_ast = pt_to_ast (lookup_trtab parse_ast_trtab) pt;
wenzelm@237
   274
    val _ = normalize true true (lookup_ruletab parse_ruletab) pre_ast;
wenzelm@18
   275
  in () end;
wenzelm@18
   276
wenzelm@18
   277
wenzelm@237
   278
(* read *)
clasohm@0
   279
wenzelm@237
   280
fun read (syn as Syntax tabs) ty str =
clasohm@0
   281
  let
wenzelm@237
   282
    val {parse_ruletab, parse_trtab, ...} = tabs;
wenzelm@18
   283
    val ast = read_ast syn false (typ_to_nonterm ty) str;
clasohm@0
   284
  in
wenzelm@237
   285
    ast_to_term (lookup_trtab parse_trtab)
wenzelm@237
   286
      (normalize_ast (lookup_ruletab parse_ruletab) ast)
clasohm@0
   287
  end;
clasohm@0
   288
clasohm@0
   289
wenzelm@237
   290
(* read types *)
clasohm@0
   291
wenzelm@237
   292
fun read_typ syn def_sort str =
wenzelm@237
   293
  typ_of_term def_sort (read syn typeT str);
wenzelm@144
   294
wenzelm@237
   295
val type_syn = extend_syntax empty_syntax type_ext;
wenzelm@237
   296
wenzelm@237
   297
fun simple_read_typ str = read_typ type_syn (K []) str;
wenzelm@144
   298
wenzelm@144
   299
wenzelm@237
   300
(* read rules *)
wenzelm@18
   301
wenzelm@18
   302
fun read_rule syn (xrule as ((_, lhs_src), (_, rhs_src))) =
wenzelm@18
   303
  let
wenzelm@237
   304
    val Syntax {consts, ...} = syn;
wenzelm@18
   305
wenzelm@18
   306
    fun constantify (ast as Constant _) = ast
wenzelm@18
   307
      | constantify (ast as Variable x) =
wenzelm@18
   308
          if x mem consts then Constant x else ast
wenzelm@18
   309
      | constantify (Appl asts) = Appl (map constantify asts);
clasohm@0
   310
wenzelm@18
   311
    fun read_pat (root, str) =
wenzelm@18
   312
      constantify (read_ast syn true root str)
wenzelm@18
   313
        handle ERROR => error ("The error above occurred in " ^ quote str);
wenzelm@18
   314
wenzelm@18
   315
    val rule as (lhs, rhs) = (pairself read_pat) xrule;
wenzelm@18
   316
  in
wenzelm@18
   317
    (case rule_error rule of
wenzelm@18
   318
      Some msg =>
wenzelm@18
   319
        error ("Error in syntax translation rule: " ^ msg ^
wenzelm@18
   320
          "\nexternal: " ^ quote lhs_src ^ "  ->  " ^ quote rhs_src ^
wenzelm@18
   321
          "\ninternal: " ^ str_of_ast lhs ^ "  ->  " ^ str_of_ast rhs)
wenzelm@18
   322
    | None => rule)
wenzelm@18
   323
  end;
clasohm@0
   324
wenzelm@18
   325
fun read_xrules syn xrules =
wenzelm@18
   326
  let
wenzelm@18
   327
    fun right_rule (xpat1 |-> xpat2) = Some (xpat1, xpat2)
wenzelm@18
   328
      | right_rule (xpat1 <-| xpat2) = None
wenzelm@18
   329
      | right_rule (xpat1 <-> xpat2) = Some (xpat1, xpat2);
clasohm@0
   330
wenzelm@18
   331
    fun left_rule (xpat1 |-> xpat2) = None
wenzelm@18
   332
      | left_rule (xpat1 <-| xpat2) = Some (xpat2, xpat1)
wenzelm@18
   333
      | left_rule (xpat1 <-> xpat2) = Some (xpat2, xpat1);
wenzelm@18
   334
  in
wenzelm@18
   335
    (map (read_rule syn) (mapfilter right_rule xrules),
wenzelm@18
   336
     map (read_rule syn) (mapfilter left_rule xrules))
wenzelm@18
   337
  end;
wenzelm@18
   338
wenzelm@18
   339
wenzelm@18
   340
wenzelm@18
   341
(** pretty terms or typs **)
wenzelm@18
   342
wenzelm@237
   343
fun pretty_t t_to_ast pretty_t (syn as Syntax tabs) t =
clasohm@0
   344
  let
wenzelm@237
   345
    val {print_trtab, print_ruletab, print_ast_trtab, prtab, ...} = tabs;
wenzelm@237
   346
    val ast = t_to_ast (lookup_trtab print_trtab) t;
clasohm@0
   347
  in
wenzelm@237
   348
    pretty_t prtab (lookup_trtab print_ast_trtab)
wenzelm@237
   349
      (normalize_ast (lookup_ruletab print_ruletab) ast)
clasohm@0
   350
  end;
clasohm@0
   351
clasohm@0
   352
val pretty_term = pretty_t term_to_ast pretty_term_ast;
clasohm@0
   353
clasohm@0
   354
val pretty_typ = pretty_t typ_to_ast pretty_typ_ast;
clasohm@0
   355
clasohm@0
   356
fun string_of_term syn t = Pretty.string_of (pretty_term syn t);
clasohm@0
   357
clasohm@0
   358
fun string_of_typ syn ty = Pretty.string_of (pretty_typ syn ty);
clasohm@0
   359
clasohm@0
   360
clasohm@0
   361
wenzelm@237
   362
(** build syntax **)
wenzelm@167
   363
wenzelm@237
   364
(* extend *)
wenzelm@167
   365
wenzelm@237
   366
fun extend syn0 read_ty (all_roots, xconsts, sext) =
wenzelm@237
   367
  let
wenzelm@237
   368
    val Syntax {roots, ...} = syn0;
wenzelm@174
   369
wenzelm@237
   370
    val syn1 = extend_syntax syn0
wenzelm@237
   371
      (syn_ext_of_sext (all_roots \\ roots) xconsts read_ty sext);
wenzelm@167
   372
wenzelm@237
   373
    val syn2 = extend_syntax syn1
wenzelm@237
   374
      (syn_ext_rules (read_xrules syn1 (xrules_of sext)));
wenzelm@237
   375
  in syn2 end;
clasohm@0
   376
clasohm@0
   377
clasohm@0
   378
(* merge *)
clasohm@0
   379
wenzelm@237
   380
fun merge all_roots syn1 syn2 =
wenzelm@167
   381
  let
wenzelm@237
   382
    val syn as (Syntax {roots, ...}) = merge_syntaxes syn1 syn2;
wenzelm@167
   383
  in
wenzelm@237
   384
    (case all_roots \\ roots of
wenzelm@237
   385
      [] => syn
wenzelm@237
   386
    | new_roots => (writeln (string_of_strings "DEBUG new roots:" new_roots); (* FIXME debug *)
wenzelm@237
   387
        extend_syntax syn (syn_ext_roots new_roots)))
wenzelm@167
   388
  end;
clasohm@0
   389
clasohm@0
   390
clasohm@0
   391
end;
clasohm@0
   392