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