src/Pure/Syntax/xgram.ML
author paulson
Thu Sep 25 12:09:41 1997 +0200 (1997-09-25)
changeset 3706 e57b5902822f
parent 18 c9ec452ff08f
permissions -rw-r--r--
Generalized and exported biresolution_from_nets_tac to allow the declaration
of Clarify_tac
     1 (*  Title:      Pure/Syntax/xgram.ML
     2     ID:         $Id$
     3     Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
     4 
     5 External grammar representation (internal interface).
     6 
     7 TODO:
     8   prod, xsymb: 'a --> string
     9   Terminal --> Literal, Nonterminal --> Argument (?)
    10 *)
    11 
    12 signature XGRAM =
    13 sig
    14   structure Ast: AST
    15   local open Ast in
    16     datatype 'a xsymb =
    17       Terminal of 'a |
    18       Nonterminal of string * int |
    19       Space of string |
    20       Bg of int | Brk of int | En
    21     datatype 'a prod = Prod of string * ('a xsymb list) * string * int
    22     val max_pri: int
    23     val chain_pri: int
    24     val literals_of: string prod list -> string list
    25     datatype xgram =
    26       XGram of {
    27         roots: string list,
    28         prods: string prod list,
    29         consts: string list,
    30         parse_ast_translation: (string * (ast list -> ast)) list,
    31         parse_rules: (ast * ast) list,
    32         parse_translation: (string * (term list -> term)) list,
    33         print_translation: (string * (term list -> term)) list,
    34         print_rules: (ast * ast) list,
    35         print_ast_translation: (string * (ast list -> ast)) list}
    36   end
    37 end;
    38 
    39 functor XGramFun(Ast: AST): XGRAM =
    40 struct
    41 
    42 structure Ast = Ast;
    43 open Ast;
    44 
    45 
    46 (** datatype prod **)
    47 
    48 (*Terminal s: literal token s
    49   Nonterminal (s, p): nonterminal s requiring priority >= p, or valued token
    50   Space s: some white space for printing
    51   Bg, Brk, En: blocks and breaks for pretty printing*)
    52 
    53 datatype 'a xsymb =
    54   Terminal of 'a |
    55   Nonterminal of string * int |
    56   Space of string |
    57   Bg of int | Brk of int | En;
    58 
    59 
    60 (*Prod (lhs, syms, c, p):
    61     lhs: name of nonterminal on the lhs of the production
    62     syms: list of symbols on the rhs of the production
    63     c: head of parse tree
    64     p: priority of this production*)
    65 
    66 datatype 'a prod = Prod of string * ('a xsymb list) * string * int;
    67 
    68 val max_pri = 1000;   (*maximum legal priority*)
    69 val chain_pri = ~1;   (*dummy for chain productions*)
    70 
    71 
    72 (* literals_of *)
    73 
    74 fun literals_of prods =
    75   let
    76     fun lits_of (Prod (_, syn, _, _)) =
    77       mapfilter (fn Terminal s => Some s | _ => None) syn;
    78   in
    79     distinct (flat (map lits_of prods))
    80   end;
    81 
    82 
    83 
    84 (** datatype xgram **)
    85 
    86 datatype xgram =
    87   XGram of {
    88     roots: string list,
    89     prods: string prod list,
    90     consts: string list,
    91     parse_ast_translation: (string * (ast list -> ast)) list,
    92     parse_rules: (ast * ast) list,
    93     parse_translation: (string * (term list -> term)) list,
    94     print_translation: (string * (term list -> term)) list,
    95     print_rules: (ast * ast) list,
    96     print_ast_translation: (string * (ast list -> ast)) list};
    97 
    98 
    99 end;
   100