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