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 |
|