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