src/Pure/Syntax/xgram.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/xgram
clasohm@0
     2
    ID:         $Id$
clasohm@0
     3
    Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
clasohm@0
     4
clasohm@0
     5
External Grammar Representation
clasohm@0
     6
clasohm@0
     7
Changes:
clasohm@0
     8
  XGRAM: added Ast, changed XGram,
clasohm@0
     9
    renamed (XSymb, Prod, XGram) to (xsymb, prod, xgram)
clasohm@0
    10
  removed Symtab
clasohm@0
    11
TODO:
clasohm@0
    12
  prod, xsymb, xgram: 'a -> string (?)
clasohm@0
    13
*)
clasohm@0
    14
clasohm@0
    15
signature XGRAM =
clasohm@0
    16
sig
clasohm@0
    17
  structure Ast: AST
clasohm@0
    18
  datatype 'a xsymb =
clasohm@0
    19
    Terminal of 'a |
clasohm@0
    20
    Nonterminal of string * int |
clasohm@0
    21
    Space of string |
clasohm@0
    22
    Bg of int | Brk of int | En
clasohm@0
    23
  datatype 'a prod = Prod of string * ('a xsymb list) * string * int
clasohm@0
    24
  local open Ast in
clasohm@0
    25
    datatype 'a xgram =
clasohm@0
    26
      XGram of {
clasohm@0
    27
        roots: string list,
clasohm@0
    28
        prods: 'a prod list,
clasohm@0
    29
        consts: string list,
clasohm@0
    30
        parse_ast_translation: (string * (ast list -> ast)) list,
clasohm@0
    31
        parse_preproc: (ast -> ast) option,
clasohm@0
    32
        parse_rules: (ast * ast) list,
clasohm@0
    33
        parse_postproc: (ast -> ast) option,
clasohm@0
    34
        parse_translation: (string * (term list -> term)) list,
clasohm@0
    35
        print_translation: (string * (term list -> term)) list,
clasohm@0
    36
        print_preproc: (ast -> ast) option,
clasohm@0
    37
        print_rules: (ast * ast) list,
clasohm@0
    38
        print_postproc: (ast -> ast) option,
clasohm@0
    39
        print_ast_translation: (string * (ast list -> ast)) list}
clasohm@0
    40
  end
clasohm@0
    41
  val copy_pri: int
clasohm@0
    42
  val terminals: 'a xsymb list -> 'a list
clasohm@0
    43
  val nonterminals: 'a xsymb list -> string list
clasohm@0
    44
  val translate: ('a -> 'b) -> 'a xsymb list -> 'b xsymb list
clasohm@0
    45
end;
clasohm@0
    46
clasohm@0
    47
functor XGramFun(Ast: AST)(*: XGRAM*) =  (* FIXME *)
clasohm@0
    48
struct
clasohm@0
    49
clasohm@0
    50
structure Ast = Ast;
clasohm@0
    51
open Ast;
clasohm@0
    52
clasohm@0
    53
(** datatype 'a xgram **)
clasohm@0
    54
clasohm@0
    55
(* Terminal a: terminal a
clasohm@0
    56
   Nonterminal (s, p): nonterminal named s, require priority >= p
clasohm@0
    57
   Space s: some white space for printing
clasohm@0
    58
   Bg, Brk, En: see resp. routines in Pretty *)
clasohm@0
    59
clasohm@0
    60
datatype 'a xsymb =
clasohm@0
    61
  Terminal of 'a |
clasohm@0
    62
  Nonterminal of string * int |
clasohm@0
    63
  Space of string |
clasohm@0
    64
  Bg of int | Brk of int | En;
clasohm@0
    65
clasohm@0
    66
clasohm@0
    67
(* Prod (lhs, rhs, opn, p):
clasohm@0
    68
    lhs: name of nonterminal on the lhs of the production
clasohm@0
    69
    rhs: list of symbols on the rhs of the production
clasohm@0
    70
    opn: name of the corresponding Isabelle Const
clasohm@0
    71
    p: priority of this production, 0 <= p <= max_pri *)
clasohm@0
    72
clasohm@0
    73
datatype 'a prod = Prod of string * ('a xsymb list) * string * int;
clasohm@0
    74
clasohm@0
    75
clasohm@0
    76
datatype 'a xgram =
clasohm@0
    77
  XGram of {
clasohm@0
    78
    roots: string list,
clasohm@0
    79
    prods: 'a prod list,
clasohm@0
    80
    consts: string list,
clasohm@0
    81
    parse_ast_translation: (string * (ast list -> ast)) list,
clasohm@0
    82
    parse_preproc: (ast -> ast) option,
clasohm@0
    83
    parse_rules: (ast * ast) list,
clasohm@0
    84
    parse_postproc: (ast -> ast) option,
clasohm@0
    85
    parse_translation: (string * (term list -> term)) list,
clasohm@0
    86
    print_translation: (string * (term list -> term)) list,
clasohm@0
    87
    print_preproc: (ast -> ast) option,
clasohm@0
    88
    print_rules: (ast * ast) list,
clasohm@0
    89
    print_postproc: (ast -> ast) option,
clasohm@0
    90
    print_ast_translation: (string * (ast list -> ast)) list};
clasohm@0
    91
clasohm@0
    92
clasohm@0
    93
clasohm@0
    94
(** misc stuff **)
clasohm@0
    95
clasohm@0
    96
val copy_pri = ~1;  (* must be < all legal priorities, i.e. 0 *)
clasohm@0
    97
clasohm@0
    98
fun terminals [] = []
clasohm@0
    99
  | terminals (Terminal s :: sl) = s :: terminals sl
clasohm@0
   100
  | terminals (_ :: sl) = terminals sl;
clasohm@0
   101
clasohm@0
   102
fun nonterminals [] = []
clasohm@0
   103
  | nonterminals (Nonterminal (s, _) :: sl) = s :: nonterminals sl
clasohm@0
   104
  | nonterminals (_ :: sl) = nonterminals sl;
clasohm@0
   105
clasohm@0
   106
fun translate trfn =
clasohm@0
   107
  map
clasohm@0
   108
    (fn Terminal t => Terminal (trfn t)
clasohm@0
   109
      | Nonterminal s => Nonterminal s
clasohm@0
   110
      | Space s => Space s
clasohm@0
   111
      | Bg i => Bg i
clasohm@0
   112
      | Brk i => Brk i
clasohm@0
   113
      | En => En);
clasohm@0
   114
clasohm@0
   115
clasohm@0
   116
end;
clasohm@0
   117