18
|
1 |
(* Title: Pure/Syntax/ast.ML
|
0
|
2 |
ID: $Id$
|
|
3 |
Author: Markus Wenzel, TU Muenchen
|
|
4 |
|
18
|
5 |
Abstract syntax trees, translation rules, matching and normalization of asts.
|
0
|
6 |
*)
|
|
7 |
|
18
|
8 |
signature AST0 =
|
0
|
9 |
sig
|
|
10 |
datatype ast =
|
|
11 |
Constant of string |
|
|
12 |
Variable of string |
|
|
13 |
Appl of ast list
|
258
|
14 |
exception AST of string * ast list
|
|
15 |
end;
|
|
16 |
|
|
17 |
signature AST1 =
|
|
18 |
sig
|
|
19 |
include AST0
|
|
20 |
structure Pretty: PRETTY
|
0
|
21 |
val mk_appl: ast -> ast list -> ast
|
18
|
22 |
val str_of_ast: ast -> string
|
|
23 |
val pretty_ast: ast -> Pretty.T
|
258
|
24 |
val pretty_rule: ast * ast -> Pretty.T
|
18
|
25 |
val pprint_ast: ast -> pprint_args -> unit
|
|
26 |
val trace_norm_ast: bool ref
|
|
27 |
val stat_norm_ast: bool ref
|
258
|
28 |
end;
|
18
|
29 |
|
|
30 |
signature AST =
|
|
31 |
sig
|
258
|
32 |
include AST1
|
0
|
33 |
val raise_ast: string -> ast list -> 'a
|
|
34 |
val head_of_rule: ast * ast -> string
|
|
35 |
val rule_error: ast * ast -> string option
|
|
36 |
val fold_ast: string -> ast list -> ast
|
|
37 |
val fold_ast_p: string -> ast list * ast -> ast
|
|
38 |
val unfold_ast: string -> ast -> ast list
|
|
39 |
val unfold_ast_p: string -> ast -> ast list * ast
|
18
|
40 |
val normalize: bool -> bool -> (string -> (ast * ast) list) option -> ast -> ast
|
|
41 |
val normalize_ast: (string -> (ast * ast) list) option -> ast -> ast
|
0
|
42 |
end;
|
|
43 |
|
18
|
44 |
functor AstFun(Pretty: PRETTY): AST =
|
0
|
45 |
struct
|
|
46 |
|
18
|
47 |
structure Pretty = Pretty;
|
|
48 |
|
0
|
49 |
|
18
|
50 |
(** abstract syntax trees **)
|
0
|
51 |
|
|
52 |
(*asts come in two flavours:
|
18
|
53 |
- ordinary asts representing terms and typs: Variables are (often) treated
|
|
54 |
like Constants;
|
0
|
55 |
- patterns used as lhs and rhs in rules: Variables are placeholders for
|
|
56 |
proper asts*)
|
|
57 |
|
|
58 |
datatype ast =
|
18
|
59 |
Constant of string | (*"not", "_abs", "fun"*)
|
|
60 |
Variable of string | (*x, ?x, 'a, ?'a*)
|
|
61 |
Appl of ast list; (*(f x y z), ("fun" 'a 'b), ("_abs" x t)*)
|
0
|
62 |
|
|
63 |
|
|
64 |
(*the list of subasts of an Appl node has to contain at least 2 elements, i.e.
|
|
65 |
there are no empty asts or nullary applications; use mk_appl for convenience*)
|
|
66 |
|
18
|
67 |
fun mk_appl f [] = f
|
|
68 |
| mk_appl f args = Appl (f :: args);
|
0
|
69 |
|
|
70 |
|
|
71 |
(*exception for system errors involving asts*)
|
|
72 |
|
|
73 |
exception AST of string * ast list;
|
|
74 |
|
18
|
75 |
fun raise_ast msg asts = raise AST (msg, asts);
|
0
|
76 |
|
|
77 |
|
18
|
78 |
(** print asts in a LISP-like style **)
|
|
79 |
|
|
80 |
(* str_of_ast *)
|
0
|
81 |
|
|
82 |
fun str_of_ast (Constant a) = quote a
|
|
83 |
| str_of_ast (Variable x) = x
|
|
84 |
| str_of_ast (Appl asts) = "(" ^ (space_implode " " (map str_of_ast asts)) ^ ")";
|
|
85 |
|
|
86 |
|
18
|
87 |
(* pretty_ast *)
|
|
88 |
|
|
89 |
fun pretty_ast (Constant a) = Pretty.str (quote a)
|
|
90 |
| pretty_ast (Variable x) = Pretty.str x
|
|
91 |
| pretty_ast (Appl asts) =
|
513
|
92 |
Pretty.enclose "(" ")" (Pretty.breaks (map pretty_ast asts));
|
18
|
93 |
|
|
94 |
|
|
95 |
(* pprint_ast *)
|
|
96 |
|
|
97 |
val pprint_ast = Pretty.pprint o pretty_ast;
|
|
98 |
|
|
99 |
|
|
100 |
(* pretty_rule *)
|
|
101 |
|
|
102 |
fun pretty_rule (lhs, rhs) =
|
235
|
103 |
Pretty.block [pretty_ast lhs, Pretty.str " ->", Pretty.brk 2, pretty_ast rhs];
|
18
|
104 |
|
|
105 |
|
0
|
106 |
(* head_of_ast, head_of_rule *)
|
|
107 |
|
|
108 |
fun head_of_ast (Constant a) = Some a
|
|
109 |
| head_of_ast (Appl (Constant a :: _)) = Some a
|
|
110 |
| head_of_ast _ = None;
|
|
111 |
|
|
112 |
fun head_of_rule (lhs, _) = the (head_of_ast lhs);
|
|
113 |
|
|
114 |
|
|
115 |
|
18
|
116 |
(** check translation rules **)
|
0
|
117 |
|
18
|
118 |
(*a wellformed rule (lhs, rhs): (ast * ast) obeys the following conditions:
|
0
|
119 |
- the head of lhs is a constant,
|
|
120 |
- the lhs has unique vars,
|
|
121 |
- vars of rhs is subset of vars of lhs*)
|
|
122 |
|
|
123 |
fun rule_error (rule as (lhs, rhs)) =
|
|
124 |
let
|
|
125 |
fun vars_of (Constant _) = []
|
|
126 |
| vars_of (Variable x) = [x]
|
|
127 |
| vars_of (Appl asts) = flat (map vars_of asts);
|
|
128 |
|
|
129 |
fun unique (x :: xs) = not (x mem xs) andalso unique xs
|
|
130 |
| unique [] = true;
|
|
131 |
|
|
132 |
val lvars = vars_of lhs;
|
|
133 |
val rvars = vars_of rhs;
|
|
134 |
in
|
|
135 |
if is_none (head_of_ast lhs) then Some "lhs has no constant head"
|
|
136 |
else if not (unique lvars) then Some "duplicate vars in lhs"
|
|
137 |
else if not (rvars subset lvars) then Some "rhs contains extra variables"
|
|
138 |
else None
|
|
139 |
end;
|
|
140 |
|
|
141 |
|
|
142 |
|
18
|
143 |
(** ast translation utilities **)
|
0
|
144 |
|
|
145 |
(* fold asts *)
|
|
146 |
|
|
147 |
fun fold_ast _ [] = raise Match
|
|
148 |
| fold_ast _ [y] = y
|
|
149 |
| fold_ast c (x :: xs) = Appl [Constant c, x, fold_ast c xs];
|
|
150 |
|
|
151 |
fun fold_ast_p c = foldr (fn (x, xs) => Appl [Constant c, x, xs]);
|
|
152 |
|
|
153 |
|
|
154 |
(* unfold asts *)
|
|
155 |
|
|
156 |
fun unfold_ast c (y as Appl [Constant c', x, xs]) =
|
|
157 |
if c = c' then x :: (unfold_ast c xs) else [y]
|
|
158 |
| unfold_ast _ y = [y];
|
|
159 |
|
|
160 |
fun unfold_ast_p c (y as Appl [Constant c', x, xs]) =
|
18
|
161 |
if c = c' then apfst (cons x) (unfold_ast_p c xs)
|
0
|
162 |
else ([], y)
|
|
163 |
| unfold_ast_p _ y = ([], y);
|
|
164 |
|
|
165 |
|
|
166 |
|
|
167 |
(** normalization of asts **)
|
|
168 |
|
18
|
169 |
(* tracing options *)
|
|
170 |
|
|
171 |
val trace_norm_ast = ref false;
|
|
172 |
val stat_norm_ast = ref false;
|
|
173 |
|
|
174 |
|
0
|
175 |
(* simple env *)
|
|
176 |
|
|
177 |
structure Env =
|
|
178 |
struct
|
|
179 |
val empty = [];
|
|
180 |
val add = op ::;
|
|
181 |
val get = the o assoc;
|
|
182 |
end;
|
|
183 |
|
|
184 |
|
|
185 |
(* match *)
|
|
186 |
|
|
187 |
fun match ast pat =
|
|
188 |
let
|
|
189 |
exception NO_MATCH;
|
|
190 |
|
|
191 |
fun mtch (Constant a, Constant b, env) =
|
|
192 |
if a = b then env else raise NO_MATCH
|
|
193 |
| mtch (Variable a, Constant b, env) =
|
|
194 |
if a = b then env else raise NO_MATCH
|
|
195 |
| mtch (ast, Variable x, env) = Env.add ((x, ast), env)
|
|
196 |
| mtch (Appl asts, Appl pats, env) = mtch_lst (asts, pats, env)
|
|
197 |
| mtch _ = raise NO_MATCH
|
|
198 |
and mtch_lst (ast :: asts, pat :: pats, env) =
|
|
199 |
mtch_lst (asts, pats, mtch (ast, pat, env))
|
|
200 |
| mtch_lst ([], [], env) = env
|
|
201 |
| mtch_lst _ = raise NO_MATCH;
|
|
202 |
in
|
|
203 |
Some (mtch (ast, pat, Env.empty)) handle NO_MATCH => None
|
|
204 |
end;
|
|
205 |
|
|
206 |
|
18
|
207 |
(* normalize *)
|
0
|
208 |
|
|
209 |
(*the normalizer works yoyo-like: top-down, bottom-up, top-down, ...*)
|
|
210 |
|
18
|
211 |
fun normalize trace stat get_rules pre_ast =
|
0
|
212 |
let
|
|
213 |
val passes = ref 0;
|
|
214 |
val lookups = ref 0;
|
|
215 |
val failed_matches = ref 0;
|
|
216 |
val changes = ref 0;
|
|
217 |
|
18
|
218 |
fun subst _ (ast as Constant _) = ast
|
0
|
219 |
| subst env (Variable x) = Env.get (env, x)
|
|
220 |
| subst env (Appl asts) = Appl (map (subst env) asts);
|
|
221 |
|
|
222 |
fun try_rules ast ((lhs, rhs) :: pats) =
|
|
223 |
(case match ast lhs of
|
|
224 |
Some env => (inc changes; Some (subst env rhs))
|
|
225 |
| None => (inc failed_matches; try_rules ast pats))
|
18
|
226 |
| try_rules _ [] = None;
|
0
|
227 |
|
|
228 |
fun try ast a = (inc lookups; try_rules ast (the get_rules a));
|
|
229 |
|
|
230 |
fun rewrite (ast as Constant a) = try ast a
|
|
231 |
| rewrite (ast as Variable a) = try ast a
|
|
232 |
| rewrite (ast as Appl (Constant a :: _)) = try ast a
|
|
233 |
| rewrite (ast as Appl (Variable a :: _)) = try ast a
|
|
234 |
| rewrite _ = None;
|
|
235 |
|
|
236 |
fun rewrote old_ast new_ast =
|
|
237 |
if trace then
|
|
238 |
writeln ("rewrote: " ^ str_of_ast old_ast ^ " -> " ^ str_of_ast new_ast)
|
|
239 |
else ();
|
|
240 |
|
|
241 |
fun norm_root ast =
|
|
242 |
(case rewrite ast of
|
|
243 |
Some new_ast => (rewrote ast new_ast; norm_root new_ast)
|
|
244 |
| None => ast);
|
|
245 |
|
|
246 |
fun norm ast =
|
|
247 |
(case norm_root ast of
|
|
248 |
Appl sub_asts =>
|
|
249 |
let
|
|
250 |
val old_changes = ! changes;
|
|
251 |
val new_ast = Appl (map norm sub_asts);
|
|
252 |
in
|
|
253 |
if old_changes = ! changes then new_ast else norm_root new_ast
|
|
254 |
end
|
|
255 |
| atomic_ast => atomic_ast);
|
|
256 |
|
|
257 |
fun normal ast =
|
|
258 |
let
|
|
259 |
val old_changes = ! changes;
|
|
260 |
val new_ast = norm ast;
|
|
261 |
in
|
|
262 |
inc passes;
|
|
263 |
if old_changes = ! changes then new_ast else normal new_ast
|
|
264 |
end;
|
|
265 |
|
|
266 |
|
18
|
267 |
val _ = if trace then writeln ("pre: " ^ str_of_ast pre_ast) else ();
|
0
|
268 |
|
|
269 |
val post_ast = if is_some get_rules then normal pre_ast else pre_ast;
|
|
270 |
in
|
18
|
271 |
if trace orelse stat then
|
0
|
272 |
writeln ("post: " ^ str_of_ast post_ast ^ "\nnormalize: " ^
|
|
273 |
string_of_int (! passes) ^ " passes, " ^
|
|
274 |
string_of_int (! lookups) ^ " lookups, " ^
|
|
275 |
string_of_int (! changes) ^ " changes, " ^
|
|
276 |
string_of_int (! failed_matches) ^ " matches failed")
|
|
277 |
else ();
|
|
278 |
post_ast
|
|
279 |
end;
|
|
280 |
|
|
281 |
|
18
|
282 |
(* normalize_ast *)
|
|
283 |
|
|
284 |
fun normalize_ast get_rules ast =
|
|
285 |
normalize (! trace_norm_ast) (! stat_norm_ast) get_rules ast;
|
|
286 |
|
|
287 |
|
0
|
288 |
end;
|
|
289 |
|