author | wenzelm |
Wed, 06 Apr 2011 13:33:46 +0200 | |
changeset 42247 | 12fe41a92cd5 |
parent 42224 | 578a51fae383 |
child 42264 | b6c1b0c4c511 |
permissions | -rw-r--r-- |
18 | 1 |
(* Title: Pure/Syntax/ast.ML |
0 | 2 |
Author: Markus Wenzel, TU Muenchen |
3 |
||
18 | 4 |
Abstract syntax trees, translation rules, matching and normalization of asts. |
0 | 5 |
*) |
6 |
||
42224
578a51fae383
discontinued special treatment of structure Ast: no pervasive content, no inclusion in structure Syntax;
wenzelm
parents:
42048
diff
changeset
|
7 |
signature AST = |
16609 | 8 |
sig |
0 | 9 |
datatype ast = |
10 |
Constant of string | |
|
11 |
Variable of string | |
|
12 |
Appl of ast list |
|
42224
578a51fae383
discontinued special treatment of structure Ast: no pervasive content, no inclusion in structure Syntax;
wenzelm
parents:
42048
diff
changeset
|
13 |
val mk_appl: ast -> ast list -> ast |
258 | 14 |
exception AST of string * ast list |
18 | 15 |
val pretty_ast: ast -> Pretty.T |
258 | 16 |
val pretty_rule: ast * ast -> Pretty.T |
42224
578a51fae383
discontinued special treatment of structure Ast: no pervasive content, no inclusion in structure Syntax;
wenzelm
parents:
42048
diff
changeset
|
17 |
val head_of_rule: ast * ast -> string |
578a51fae383
discontinued special treatment of structure Ast: no pervasive content, no inclusion in structure Syntax;
wenzelm
parents:
42048
diff
changeset
|
18 |
val rule_error: ast * ast -> string option |
10913 | 19 |
val fold_ast: string -> ast list -> ast |
20 |
val fold_ast_p: string -> ast list * ast -> ast |
|
21 |
val unfold_ast: string -> ast -> ast list |
|
22 |
val unfold_ast_p: string -> ast -> ast list * ast |
|
41377
390c53904220
configuration option "syntax_ast_trace" and "syntax_ast_stat";
wenzelm
parents:
38328
diff
changeset
|
23 |
val ast_trace_raw: Config.raw |
390c53904220
configuration option "syntax_ast_trace" and "syntax_ast_stat";
wenzelm
parents:
38328
diff
changeset
|
24 |
val ast_trace: bool Config.T |
390c53904220
configuration option "syntax_ast_trace" and "syntax_ast_stat";
wenzelm
parents:
38328
diff
changeset
|
25 |
val ast_stat_raw: Config.raw |
390c53904220
configuration option "syntax_ast_trace" and "syntax_ast_stat";
wenzelm
parents:
38328
diff
changeset
|
26 |
val ast_stat: bool Config.T |
390c53904220
configuration option "syntax_ast_trace" and "syntax_ast_stat";
wenzelm
parents:
38328
diff
changeset
|
27 |
val normalize: Proof.context -> (string -> (ast * ast) list) -> ast -> ast |
16609 | 28 |
end; |
0 | 29 |
|
42224
578a51fae383
discontinued special treatment of structure Ast: no pervasive content, no inclusion in structure Syntax;
wenzelm
parents:
42048
diff
changeset
|
30 |
structure Ast: AST = |
0 | 31 |
struct |
32 |
||
18 | 33 |
(** abstract syntax trees **) |
0 | 34 |
|
35 |
(*asts come in two flavours: |
|
18 | 36 |
- ordinary asts representing terms and typs: Variables are (often) treated |
37 |
like Constants; |
|
0 | 38 |
- patterns used as lhs and rhs in rules: Variables are placeholders for |
39 |
proper asts*) |
|
40 |
||
41 |
datatype ast = |
|
18 | 42 |
Constant of string | (*"not", "_abs", "fun"*) |
43 |
Variable of string | (*x, ?x, 'a, ?'a*) |
|
44 |
Appl of ast list; (*(f x y z), ("fun" 'a 'b), ("_abs" x t)*) |
|
0 | 45 |
|
46 |
(*the list of subasts of an Appl node has to contain at least 2 elements, i.e. |
|
47 |
there are no empty asts or nullary applications; use mk_appl for convenience*) |
|
18 | 48 |
fun mk_appl f [] = f |
49 |
| mk_appl f args = Appl (f :: args); |
|
0 | 50 |
|
51 |
(*exception for system errors involving asts*) |
|
52 |
exception AST of string * ast list; |
|
53 |
||
54 |
||
55 |
||
18 | 56 |
(** print asts in a LISP-like style **) |
57 |
||
14599 | 58 |
fun pretty_ast (Constant a) = Pretty.quote (Pretty.str a) |
42048
afd11ca8e018
support for encoded positions (for id_position, longid_position) as pseudo type-constraints -- still inactive;
wenzelm
parents:
41377
diff
changeset
|
59 |
| pretty_ast (Variable x) = |
afd11ca8e018
support for encoded positions (for id_position, longid_position) as pseudo type-constraints -- still inactive;
wenzelm
parents:
41377
diff
changeset
|
60 |
(case Lexicon.decode_position x of |
afd11ca8e018
support for encoded positions (for id_position, longid_position) as pseudo type-constraints -- still inactive;
wenzelm
parents:
41377
diff
changeset
|
61 |
SOME pos => Lexicon.pretty_position pos |
afd11ca8e018
support for encoded positions (for id_position, longid_position) as pseudo type-constraints -- still inactive;
wenzelm
parents:
41377
diff
changeset
|
62 |
| NONE => Pretty.str x) |
38328 | 63 |
| pretty_ast (Appl asts) = Pretty.enclose "(" ")" (Pretty.breaks (map pretty_ast asts)); |
18 | 64 |
|
65 |
fun pretty_rule (lhs, rhs) = |
|
235 | 66 |
Pretty.block [pretty_ast lhs, Pretty.str " ->", Pretty.brk 2, pretty_ast rhs]; |
18 | 67 |
|
68 |
||
0 | 69 |
(* head_of_ast, head_of_rule *) |
70 |
||
9372
7834e56e2277
AST translation rules no longer require constant head on LHS;
wenzelm
parents:
8997
diff
changeset
|
71 |
fun head_of_ast (Constant a) = a |
7834e56e2277
AST translation rules no longer require constant head on LHS;
wenzelm
parents:
8997
diff
changeset
|
72 |
| head_of_ast (Appl (Constant a :: _)) = a |
7834e56e2277
AST translation rules no longer require constant head on LHS;
wenzelm
parents:
8997
diff
changeset
|
73 |
| head_of_ast _ = ""; |
0 | 74 |
|
9372
7834e56e2277
AST translation rules no longer require constant head on LHS;
wenzelm
parents:
8997
diff
changeset
|
75 |
fun head_of_rule (lhs, _) = head_of_ast lhs; |
0 | 76 |
|
77 |
||
78 |
||
18 | 79 |
(** check translation rules **) |
0 | 80 |
|
32784 | 81 |
fun rule_error (lhs, rhs) = |
0 | 82 |
let |
19486 | 83 |
fun add_vars (Constant _) = I |
84 |
| add_vars (Variable x) = cons x |
|
85 |
| add_vars (Appl asts) = fold add_vars asts; |
|
0 | 86 |
|
19486 | 87 |
val lvars = add_vars lhs []; |
88 |
val rvars = add_vars rhs []; |
|
0 | 89 |
in |
19486 | 90 |
if has_duplicates (op =) lvars then SOME "duplicate vars in lhs" |
33038 | 91 |
else if not (subset (op =) (rvars, lvars)) then SOME "rhs contains extra variables" |
15531 | 92 |
else NONE |
0 | 93 |
end; |
94 |
||
95 |
||
96 |
||
18 | 97 |
(** ast translation utilities **) |
0 | 98 |
|
99 |
(* fold asts *) |
|
100 |
||
101 |
fun fold_ast _ [] = raise Match |
|
102 |
| fold_ast _ [y] = y |
|
103 |
| fold_ast c (x :: xs) = Appl [Constant c, x, fold_ast c xs]; |
|
104 |
||
19473 | 105 |
fun fold_ast_p c = uncurry (fold_rev (fn x => fn xs => Appl [Constant c, x, xs])); |
0 | 106 |
|
107 |
||
108 |
(* unfold asts *) |
|
109 |
||
110 |
fun unfold_ast c (y as Appl [Constant c', x, xs]) = |
|
16609 | 111 |
if c = c' then x :: unfold_ast c xs else [y] |
0 | 112 |
| unfold_ast _ y = [y]; |
113 |
||
114 |
fun unfold_ast_p c (y as Appl [Constant c', x, xs]) = |
|
18 | 115 |
if c = c' then apfst (cons x) (unfold_ast_p c xs) |
0 | 116 |
else ([], y) |
117 |
| unfold_ast_p _ y = ([], y); |
|
118 |
||
119 |
||
16609 | 120 |
|
0 | 121 |
(** normalization of asts **) |
122 |
||
123 |
(* match *) |
|
124 |
||
125 |
fun match ast pat = |
|
126 |
let |
|
127 |
exception NO_MATCH; |
|
128 |
||
1127
42ec82147d83
changed macro expander such that patterns also match prefixes of appls;
wenzelm
parents:
922
diff
changeset
|
129 |
fun mtch (Constant a) (Constant b) env = |
0 | 130 |
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
|
131 |
| mtch (Variable a) (Constant b) env = |
0 | 132 |
if a = b then env else raise NO_MATCH |
17412 | 133 |
| 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
|
134 |
| 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
|
135 |
| mtch _ _ _ = raise NO_MATCH |
42ec82147d83
changed macro expander such that patterns also match prefixes of appls;
wenzelm
parents:
922
diff
changeset
|
136 |
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
|
137 |
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
|
138 |
| mtch_lst [] [] env = env |
42ec82147d83
changed macro expander such that patterns also match prefixes of appls;
wenzelm
parents:
922
diff
changeset
|
139 |
| mtch_lst _ _ _ = raise NO_MATCH; |
42ec82147d83
changed macro expander such that patterns also match prefixes of appls;
wenzelm
parents:
922
diff
changeset
|
140 |
|
42ec82147d83
changed macro expander such that patterns also match prefixes of appls;
wenzelm
parents:
922
diff
changeset
|
141 |
val (head, args) = |
42ec82147d83
changed macro expander such that patterns also match prefixes of appls;
wenzelm
parents:
922
diff
changeset
|
142 |
(case (ast, pat) of |
42ec82147d83
changed macro expander such that patterns also match prefixes of appls;
wenzelm
parents:
922
diff
changeset
|
143 |
(Appl asts, Appl pats) => |
42ec82147d83
changed macro expander such that patterns also match prefixes of appls;
wenzelm
parents:
922
diff
changeset
|
144 |
let val a = length asts and p = length pats in |
33957 | 145 |
if a > p then (Appl (take p asts), drop p asts) |
1127
42ec82147d83
changed macro expander such that patterns also match prefixes of appls;
wenzelm
parents:
922
diff
changeset
|
146 |
else (ast, []) |
42ec82147d83
changed macro expander such that patterns also match prefixes of appls;
wenzelm
parents:
922
diff
changeset
|
147 |
end |
42ec82147d83
changed macro expander such that patterns also match prefixes of appls;
wenzelm
parents:
922
diff
changeset
|
148 |
| _ => (ast, [])); |
0 | 149 |
in |
15531 | 150 |
SOME (mtch head pat Symtab.empty, args) handle NO_MATCH => NONE |
0 | 151 |
end; |
152 |
||
153 |
||
18 | 154 |
(* normalize *) |
0 | 155 |
|
41377
390c53904220
configuration option "syntax_ast_trace" and "syntax_ast_stat";
wenzelm
parents:
38328
diff
changeset
|
156 |
val ast_trace_raw = Config.declare "syntax_ast_trace" (fn _ => Config.Bool false); |
390c53904220
configuration option "syntax_ast_trace" and "syntax_ast_stat";
wenzelm
parents:
38328
diff
changeset
|
157 |
val ast_trace = Config.bool ast_trace_raw; |
390c53904220
configuration option "syntax_ast_trace" and "syntax_ast_stat";
wenzelm
parents:
38328
diff
changeset
|
158 |
|
390c53904220
configuration option "syntax_ast_trace" and "syntax_ast_stat";
wenzelm
parents:
38328
diff
changeset
|
159 |
val ast_stat_raw = Config.declare "syntax_ast_stat" (fn _ => Config.Bool false); |
390c53904220
configuration option "syntax_ast_trace" and "syntax_ast_stat";
wenzelm
parents:
38328
diff
changeset
|
160 |
val ast_stat = Config.bool ast_stat_raw; |
0 | 161 |
|
42048
afd11ca8e018
support for encoded positions (for id_position, longid_position) as pseudo type-constraints -- still inactive;
wenzelm
parents:
41377
diff
changeset
|
162 |
fun message head body = |
afd11ca8e018
support for encoded positions (for id_position, longid_position) as pseudo type-constraints -- still inactive;
wenzelm
parents:
41377
diff
changeset
|
163 |
Pretty.string_of (Pretty.block [Pretty.str head, Pretty.brk 1, body]); |
afd11ca8e018
support for encoded positions (for id_position, longid_position) as pseudo type-constraints -- still inactive;
wenzelm
parents:
41377
diff
changeset
|
164 |
|
41377
390c53904220
configuration option "syntax_ast_trace" and "syntax_ast_stat";
wenzelm
parents:
38328
diff
changeset
|
165 |
(*the normalizer works yoyo-like: top-down, bottom-up, top-down, ...*) |
390c53904220
configuration option "syntax_ast_trace" and "syntax_ast_stat";
wenzelm
parents:
38328
diff
changeset
|
166 |
fun normalize ctxt get_rules pre_ast = |
0 | 167 |
let |
41377
390c53904220
configuration option "syntax_ast_trace" and "syntax_ast_stat";
wenzelm
parents:
38328
diff
changeset
|
168 |
val trace = Config.get ctxt ast_trace; |
390c53904220
configuration option "syntax_ast_trace" and "syntax_ast_stat";
wenzelm
parents:
38328
diff
changeset
|
169 |
val stat = Config.get ctxt ast_stat; |
390c53904220
configuration option "syntax_ast_trace" and "syntax_ast_stat";
wenzelm
parents:
38328
diff
changeset
|
170 |
|
32738 | 171 |
val passes = Unsynchronized.ref 0; |
172 |
val failed_matches = Unsynchronized.ref 0; |
|
173 |
val changes = Unsynchronized.ref 0; |
|
0 | 174 |
|
18 | 175 |
fun subst _ (ast as Constant _) = ast |
17412 | 176 |
| subst env (Variable x) = the (Symtab.lookup env x) |
0 | 177 |
| subst env (Appl asts) = Appl (map (subst env) asts); |
178 |
||
11733 | 179 |
fun try_rules ((lhs, rhs) :: pats) ast = |
0 | 180 |
(case match ast lhs of |
15531 | 181 |
SOME (env, args) => |
32738 | 182 |
(Unsynchronized.inc changes; SOME (mk_appl (subst env rhs) args)) |
183 |
| NONE => (Unsynchronized.inc failed_matches; try_rules pats ast)) |
|
15531 | 184 |
| try_rules [] _ = NONE; |
11733 | 185 |
val try_headless_rules = try_rules (get_rules ""); |
0 | 186 |
|
11733 | 187 |
fun try ast a = |
188 |
(case try_rules (get_rules a) ast of |
|
15531 | 189 |
NONE => try_headless_rules ast |
11733 | 190 |
| some => some); |
0 | 191 |
|
192 |
fun rewrite (ast as Constant a) = try ast a |
|
193 |
| rewrite (ast as Variable a) = try ast a |
|
194 |
| rewrite (ast as Appl (Constant a :: _)) = try ast a |
|
195 |
| rewrite (ast as Appl (Variable a :: _)) = try ast a |
|
11733 | 196 |
| rewrite ast = try_headless_rules ast; |
0 | 197 |
|
198 |
fun rewrote old_ast new_ast = |
|
42048
afd11ca8e018
support for encoded positions (for id_position, longid_position) as pseudo type-constraints -- still inactive;
wenzelm
parents:
41377
diff
changeset
|
199 |
if trace then tracing (message "rewrote:" (pretty_rule (old_ast, new_ast))) |
21962 | 200 |
else (); |
0 | 201 |
|
202 |
fun norm_root ast = |
|
203 |
(case rewrite ast of |
|
15531 | 204 |
SOME new_ast => (rewrote ast new_ast; norm_root new_ast) |
205 |
| NONE => ast); |
|
0 | 206 |
|
207 |
fun norm ast = |
|
208 |
(case norm_root ast of |
|
209 |
Appl sub_asts => |
|
210 |
let |
|
211 |
val old_changes = ! changes; |
|
212 |
val new_ast = Appl (map norm sub_asts); |
|
213 |
in |
|
214 |
if old_changes = ! changes then new_ast else norm_root new_ast |
|
215 |
end |
|
216 |
| atomic_ast => atomic_ast); |
|
217 |
||
218 |
fun normal ast = |
|
219 |
let |
|
220 |
val old_changes = ! changes; |
|
221 |
val new_ast = norm ast; |
|
222 |
in |
|
32738 | 223 |
Unsynchronized.inc passes; |
0 | 224 |
if old_changes = ! changes then new_ast else normal new_ast |
225 |
end; |
|
226 |
||
227 |
||
42048
afd11ca8e018
support for encoded positions (for id_position, longid_position) as pseudo type-constraints -- still inactive;
wenzelm
parents:
41377
diff
changeset
|
228 |
val _ = if trace then tracing (message "pre:" (pretty_ast pre_ast)) else (); |
9372
7834e56e2277
AST translation rules no longer require constant head on LHS;
wenzelm
parents:
8997
diff
changeset
|
229 |
val post_ast = normal pre_ast; |
21962 | 230 |
val _ = |
231 |
if trace orelse stat then |
|
42048
afd11ca8e018
support for encoded positions (for id_position, longid_position) as pseudo type-constraints -- still inactive;
wenzelm
parents:
41377
diff
changeset
|
232 |
tracing (message "post:" (pretty_ast post_ast) ^ "\nnormalize: " ^ |
21962 | 233 |
string_of_int (! passes) ^ " passes, " ^ |
234 |
string_of_int (! changes) ^ " changes, " ^ |
|
235 |
string_of_int (! failed_matches) ^ " matches failed") |
|
236 |
else (); |
|
237 |
in post_ast end; |
|
0 | 238 |
|
1506 | 239 |
end; |