|
1 (* Title: Pure/Syntax/extension |
|
2 ID: $Id$ |
|
3 Author: Tobias Nipkow and Markus Wenzel, TU Muenchen |
|
4 |
|
5 Syntax definition (internal interface) |
|
6 *) |
|
7 |
|
8 signature EXTENSION0 = |
|
9 sig |
|
10 val typeT: typ |
|
11 val constrainC: string |
|
12 end; |
|
13 |
|
14 signature EXTENSION = |
|
15 sig |
|
16 include EXTENSION0 |
|
17 structure XGram: XGRAM |
|
18 local open XGram XGram.Ast in |
|
19 datatype mfix = Mfix of string * typ * string * int list * int |
|
20 datatype ext = |
|
21 Ext of { |
|
22 roots: string list, |
|
23 mfix: mfix list, |
|
24 extra_consts: string list, |
|
25 parse_ast_translation: (string * (ast list -> ast)) list, |
|
26 parse_preproc: (ast -> ast) option, |
|
27 parse_postproc: (ast -> ast) option, |
|
28 parse_translation: (string * (term list -> term)) list, |
|
29 print_translation: (string * (term list -> term)) list, |
|
30 print_preproc: (ast -> ast) option, |
|
31 print_postproc: (ast -> ast) option, |
|
32 print_ast_translation: (string * (ast list -> ast)) list} |
|
33 datatype synrules = |
|
34 SynRules of { |
|
35 parse_rules: (ast * ast) list, |
|
36 print_rules: (ast * ast) list} |
|
37 val max_pri: int |
|
38 val logic: string |
|
39 val id: string |
|
40 val idT: typ |
|
41 val var: string |
|
42 val varT: typ |
|
43 val tfree: string |
|
44 val tfreeT: typ |
|
45 val tvar: string |
|
46 val tvarT: typ |
|
47 val typ_to_nt: typ -> string |
|
48 val applC: string |
|
49 val args: string |
|
50 val empty_synrules: synrules |
|
51 val empty: string xgram |
|
52 val extend: string xgram -> (ext * synrules) -> string xgram |
|
53 end |
|
54 end; |
|
55 |
|
56 functor ExtensionFun(XGram: XGRAM): EXTENSION = |
|
57 struct |
|
58 |
|
59 structure XGram = XGram; |
|
60 open XGram XGram.Ast; |
|
61 |
|
62 |
|
63 (** datatype ext **) |
|
64 |
|
65 (* Mfix (sy, ty, c, pl, p): |
|
66 sy: production as symbolic string |
|
67 ty: type description of production |
|
68 c: corresponding Isabelle Const |
|
69 pl: priorities of nonterminals in sy |
|
70 p: priority of production |
|
71 *) |
|
72 |
|
73 datatype mfix = Mfix of string * typ * string * int list * int; |
|
74 |
|
75 datatype ext = |
|
76 Ext of { |
|
77 roots: string list, |
|
78 mfix: mfix list, |
|
79 extra_consts: string list, |
|
80 parse_ast_translation: (string * (ast list -> ast)) list, |
|
81 parse_preproc: (ast -> ast) option, |
|
82 parse_postproc: (ast -> ast) option, |
|
83 parse_translation: (string * (term list -> term)) list, |
|
84 print_translation: (string * (term list -> term)) list, |
|
85 print_preproc: (ast -> ast) option, |
|
86 print_postproc: (ast -> ast) option, |
|
87 print_ast_translation: (string * (ast list -> ast)) list}; |
|
88 |
|
89 datatype synrules = |
|
90 SynRules of { |
|
91 parse_rules: (ast * ast) list, |
|
92 print_rules: (ast * ast) list}; |
|
93 |
|
94 |
|
95 (* empty_synrules *) |
|
96 |
|
97 val empty_synrules = SynRules {parse_rules = [], print_rules = []}; |
|
98 |
|
99 |
|
100 (* empty xgram *) |
|
101 |
|
102 val empty = |
|
103 XGram { |
|
104 roots = [], prods = [], consts = [], |
|
105 parse_ast_translation = [], |
|
106 parse_preproc = None, |
|
107 parse_rules = [], |
|
108 parse_postproc = None, |
|
109 parse_translation = [], |
|
110 print_translation = [], |
|
111 print_preproc = None, |
|
112 print_rules = [], |
|
113 print_postproc = None, |
|
114 print_ast_translation = []}; |
|
115 |
|
116 |
|
117 |
|
118 (** syntactic constants etc. **) |
|
119 |
|
120 val max_pri = 1000; (*maximum legal priority*) |
|
121 |
|
122 val logic = "logic"; |
|
123 val logicT = Type (logic, []); |
|
124 |
|
125 val logic1 = "logic1"; |
|
126 val logic1T = Type (logic1, []); |
|
127 |
|
128 val funT = Type ("fun", []); |
|
129 |
|
130 |
|
131 (* terminals *) |
|
132 |
|
133 val id = "id"; |
|
134 val idT = Type (id, []); |
|
135 |
|
136 val var = "var"; |
|
137 val varT = Type (var, []); |
|
138 |
|
139 val tfree = "tfree"; |
|
140 val tfreeT = Type (tfree, []); |
|
141 |
|
142 val tvar = "tvar"; |
|
143 val tvarT = Type (tvar, []); |
|
144 |
|
145 val terminalTs = [idT, varT, tfreeT, tvarT]; |
|
146 |
|
147 |
|
148 val args = "args"; |
|
149 val argsT = Type (args, []); |
|
150 |
|
151 val typeT = Type ("type", []); |
|
152 |
|
153 val applC = "_appl"; |
|
154 val constrainC = "_constrain"; |
|
155 |
|
156 |
|
157 fun typ_to_nt (Type (c, _)) = c |
|
158 | typ_to_nt _ = logic; |
|
159 |
|
160 |
|
161 |
|
162 (** extend xgram **) (* FIXME clean *) |
|
163 |
|
164 fun nonts syn = foldl (fn (i, "_") => i + 1 | (i, _) => i) (0, explode syn); |
|
165 |
|
166 val meta_chs = ["(", ")", "/", "_"]; |
|
167 |
|
168 fun mk_term(pref, []) = (pref, []) |
|
169 | mk_term(pref, "'"::c::cl) = mk_term(pref^c, cl) |
|
170 | mk_term(pref, l as c::cl) = if is_blank(c) orelse c mem meta_chs |
|
171 then (pref, l) else mk_term(pref^c, cl); |
|
172 |
|
173 fun mk_space(sp, []) = (sp, []) | |
|
174 mk_space(sp, cl as c::cl') = |
|
175 if is_blank(c) then mk_space(sp^c, cl') else (sp, cl); |
|
176 |
|
177 exception ARG_EXN; |
|
178 exception BLOCK_EXN; |
|
179 |
|
180 fun mk_syntax([], ar, _, b, sy) = if b=0 then (sy, ar) else raise BLOCK_EXN |
|
181 | mk_syntax("_"::cs, Type("fun", [ar, ar']), [], b, sy) = |
|
182 mk_syntax(cs, ar', [], b, sy@[Nonterminal(typ_to_nt ar, 0)]) |
|
183 | mk_syntax("_"::cs, Type("fun", [ar, ar']), p::pl, b, sy) = |
|
184 mk_syntax(cs, ar', pl, b, sy@[Nonterminal(typ_to_nt ar, p)]) |
|
185 | mk_syntax("_"::cs, _, _, _, _) = raise ARG_EXN |
|
186 | mk_syntax("("::cs, ar, pl, b, sy) = let val (i, cs') = scan_int cs |
|
187 in mk_syntax(cs', ar, pl, b+1, sy@[Bg(i)]) end |
|
188 | mk_syntax(")"::cs, ar, pl, b, sy) = |
|
189 if b>0 then mk_syntax(cs, ar, pl, b-1, sy@[En]) else raise BLOCK_EXN |
|
190 | mk_syntax("/"::cs, ar, pl, b, sy) = let val (sp, cs') = take_prefix is_blank cs |
|
191 in mk_syntax(cs', ar, pl, b, sy@[Brk(length sp)]) end |
|
192 | mk_syntax(c::cs, ar, pl, b, sy) = |
|
193 let val (term, rest) = |
|
194 if is_blank(c) |
|
195 then let val (sp, cs') = mk_space(c, cs) in (Space(sp), cs') end |
|
196 else let val (tk, cs') = mk_term("", c::cs) in(Terminal(tk), cs') end |
|
197 in mk_syntax(rest, ar, pl, b, sy@[term]) end; |
|
198 |
|
199 fun pri_test1 p = if 0 <= p andalso p <= max_pri then () |
|
200 else error("Priority out of range: " ^ string_of_int p) |
|
201 fun pri_test(pl, p) = (pri_test1 p; seq pri_test1 pl); |
|
202 |
|
203 fun mk_prod2(sy, T, opn, pl, p) = |
|
204 let val (syn, T') = mk_syntax(explode sy, T, pl, 0, []) handle |
|
205 ARG_EXN => |
|
206 error("More arguments in "^sy^" than in corresponding type") | |
|
207 BLOCK_EXN => error("Unbalanced block parantheses in "^sy); |
|
208 val nt = case T' of Type(c, _) => c | _ => logic1; |
|
209 in Prod(nt, syn, opn, p) end; |
|
210 |
|
211 fun mk_prod1(sy, T, opn, pl, p) = (pri_test(pl, p); mk_prod2(sy, T, opn, pl, p)); |
|
212 |
|
213 |
|
214 fun terminal1(T as Type("fun", _)) = hd(binder_types T) mem terminalTs |
|
215 | terminal1 _ = false; |
|
216 |
|
217 fun mk_prod(Mfix(sy, T, "", pl, p)) = if nonts sy <> 1 |
|
218 then error"Copy op must have exactly one argument" else |
|
219 if filter_out is_blank (explode sy) = ["_"] andalso |
|
220 not(terminal1 T) |
|
221 then mk_prod2(sy, T, "", [copy_pri], copy_pri) |
|
222 else mk_prod1(sy, T, "", pl, p) |
|
223 | mk_prod(Mfix(sy, T, const, pl, p)) = mk_prod1(sy, T, const, pl, p) |
|
224 |
|
225 |
|
226 |
|
227 fun extend (XGram xgram) (Ext ext, SynRules rules) = |
|
228 let |
|
229 infix oo; |
|
230 |
|
231 fun None oo None = None |
|
232 | (Some f) oo None = Some f |
|
233 | None oo (Some g) = Some g |
|
234 | (Some f) oo (Some g) = Some (f o g); |
|
235 |
|
236 fun descend (from, to) = Mfix ("_", to --> from, "", [0], 0); |
|
237 |
|
238 fun parents T = Mfix ("(1'(_'))", T --> T, "", [0], max_pri); |
|
239 |
|
240 fun mkappl T = |
|
241 Mfix ("_(1'(_'))", [funT, argsT] ---> T, applC, [max_pri, 0], max_pri); |
|
242 |
|
243 fun mkid T = Mfix ("_", idT --> T, "", [], max_pri); |
|
244 |
|
245 fun mkvar T = Mfix ("_", varT --> T, "", [], max_pri); |
|
246 |
|
247 fun constrain T = |
|
248 Mfix ("_::_", [T, typeT]--->T, constrainC, [max_pri, 0], max_pri - 1); |
|
249 |
|
250 |
|
251 val {roots = roots1, prods, consts, |
|
252 parse_ast_translation = parse_ast_translation1, |
|
253 parse_preproc = parse_preproc1, |
|
254 parse_rules = parse_rules1, |
|
255 parse_postproc = parse_postproc1, |
|
256 parse_translation = parse_translation1, |
|
257 print_translation = print_translation1, |
|
258 print_preproc = print_preproc1, |
|
259 print_rules = print_rules1, |
|
260 print_postproc = print_postproc1, |
|
261 print_ast_translation = print_ast_translation1} = xgram; |
|
262 |
|
263 val {roots = roots2, mfix, extra_consts, |
|
264 parse_ast_translation = parse_ast_translation2, |
|
265 parse_preproc = parse_preproc2, |
|
266 parse_postproc = parse_postproc2, |
|
267 parse_translation = parse_translation2, |
|
268 print_translation = print_translation2, |
|
269 print_preproc = print_preproc2, |
|
270 print_postproc = print_postproc2, |
|
271 print_ast_translation = print_ast_translation2} = ext; |
|
272 |
|
273 val {parse_rules = parse_rules2, print_rules = print_rules2} = rules; |
|
274 |
|
275 val Troots = map (apr (Type, [])) (roots2 \\ roots1); |
|
276 val Troots' = Troots \\ [typeT, propT, logicT]; |
|
277 val mfix' = mfix @ map parents (Troots \ logicT) @ map mkappl Troots' @ |
|
278 map mkid Troots' @ map mkvar Troots' @ map constrain Troots' @ |
|
279 map (apl (logicT, descend)) (Troots \\ [typeT, logicT]) @ |
|
280 map (apr (descend, logic1T)) Troots'; |
|
281 in |
|
282 XGram { |
|
283 roots = distinct (roots1 @ roots2), |
|
284 (* roots = roots1 union roots2, *) (* FIXME remove *) |
|
285 prods = prods @ map mk_prod mfix', |
|
286 consts = consts union extra_consts, |
|
287 parse_ast_translation = parse_ast_translation1 @ parse_ast_translation2, |
|
288 parse_preproc = parse_preproc1 oo parse_preproc2, |
|
289 parse_rules = parse_rules1 @ parse_rules2, |
|
290 parse_postproc = parse_postproc2 oo parse_postproc1, |
|
291 parse_translation = parse_translation1 @ parse_translation2, |
|
292 print_translation = print_translation1 @ print_translation2, |
|
293 print_preproc = print_preproc1 oo print_preproc2, |
|
294 print_rules = print_rules1 @ print_rules2, |
|
295 print_postproc = print_postproc2 oo print_postproc1, |
|
296 print_ast_translation = print_ast_translation1 @ print_ast_translation2} |
|
297 end; |
|
298 |
|
299 |
|
300 end; |
|
301 |