author  wenzelm 
Mon, 09 Nov 1998 15:42:08 +0100  
changeset 5840  e2d2b896c717 
parent 5689  ffecea547501 
child 8997  da290d99d8b2 
permissions  rwrr 
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 
25 
val trace_norm_ast: bool ref 

26 
val stat_norm_ast: bool ref 

1506  27 
end; 
18  28 

29 
signature AST = 

1506  30 
sig 
258  31 
include AST1 
0  32 
val head_of_rule: ast * ast > string 
33 
val rule_error: ast * ast > string option 

34 
val fold_ast: string > ast list > ast 

35 
val fold_ast_p: string > ast list * ast > ast 

36 
val unfold_ast: string > ast > ast list 

37 
val unfold_ast_p: string > ast > ast list * ast 

18  38 
val normalize: bool > bool > (string > (ast * ast) list) option > ast > ast 
39 
val normalize_ast: (string > (ast * ast) list) option > ast > ast 

1506  40 
end; 
0  41 

1506  42 
structure Ast : AST = 
0  43 
struct 
44 

18  45 
(** abstract syntax trees **) 
0  46 

47 
(*asts come in two flavours: 

18  48 
 ordinary asts representing terms and typs: Variables are (often) treated 
49 
like Constants; 

0  50 
 patterns used as lhs and rhs in rules: Variables are placeholders for 
51 
proper asts*) 

52 

53 
datatype ast = 

18  54 
Constant of string  (*"not", "_abs", "fun"*) 
55 
Variable of string  (*x, ?x, 'a, ?'a*) 

56 
Appl of ast list; (*(f x y z), ("fun" 'a 'b), ("_abs" x t)*) 

0  57 

58 

59 
(*the list of subasts of an Appl node has to contain at least 2 elements, i.e. 

60 
there are no empty asts or nullary applications; use mk_appl for convenience*) 

61 

18  62 
fun mk_appl f [] = f 
63 
 mk_appl f args = Appl (f :: args); 

0  64 

65 

66 
(*exception for system errors involving asts*) 

67 

68 
exception AST of string * ast list; 

69 

70 

71 

18  72 
(** print asts in a LISPlike style **) 
73 

74 
(* str_of_ast *) 

0  75 

76 
fun str_of_ast (Constant a) = quote a 

77 
 str_of_ast (Variable x) = x 

78 
 str_of_ast (Appl asts) = "(" ^ (space_implode " " (map str_of_ast asts)) ^ ")"; 

79 

80 

18  81 
(* pretty_ast *) 
82 

83 
fun pretty_ast (Constant a) = Pretty.str (quote a) 

84 
 pretty_ast (Variable x) = Pretty.str x 

85 
 pretty_ast (Appl asts) = 

513  86 
Pretty.enclose "(" ")" (Pretty.breaks (map pretty_ast asts)); 
18  87 

88 

89 
(* pprint_ast *) 

90 

91 
val pprint_ast = Pretty.pprint o pretty_ast; 

92 

93 

94 
(* pretty_rule *) 

95 

96 
fun pretty_rule (lhs, rhs) = 

235  97 
Pretty.block [pretty_ast lhs, Pretty.str " >", Pretty.brk 2, pretty_ast rhs]; 
18  98 

99 

0  100 
(* head_of_ast, head_of_rule *) 
101 

102 
fun head_of_ast (Constant a) = Some a 

103 
 head_of_ast (Appl (Constant a :: _)) = Some a 

104 
 head_of_ast _ = None; 

105 

106 
fun head_of_rule (lhs, _) = the (head_of_ast lhs); 

107 

108 

109 

18  110 
(** check translation rules **) 
0  111 

18  112 
(*a wellformed rule (lhs, rhs): (ast * ast) obeys the following conditions: 
0  113 
 the head of lhs is a constant, 
114 
 the lhs has unique vars, 

115 
 vars of rhs is subset of vars of lhs*) 

116 

117 
fun rule_error (rule as (lhs, rhs)) = 

118 
let 

119 
fun vars_of (Constant _) = [] 

120 
 vars_of (Variable x) = [x] 

121 
 vars_of (Appl asts) = flat (map vars_of asts); 

122 

123 
fun unique (x :: xs) = not (x mem xs) andalso unique xs 

124 
 unique [] = true; 

125 

126 
val lvars = vars_of lhs; 

127 
val rvars = vars_of rhs; 

128 
in 

129 
if is_none (head_of_ast lhs) then Some "lhs has no constant head" 

130 
else if not (unique lvars) then Some "duplicate vars in lhs" 

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 

147 

148 
(* unfold asts *) 

149 

150 
fun unfold_ast c (y as Appl [Constant c', x, xs]) = 

151 
if c = c' then x :: (unfold_ast c xs) else [y] 

152 
 unfold_ast _ y = [y]; 

153 

154 
fun unfold_ast_p c (y as Appl [Constant c', x, xs]) = 

18  155 
if c = c' then apfst (cons x) (unfold_ast_p c xs) 
0  156 
else ([], y) 
157 
 unfold_ast_p _ y = ([], y); 

158 

159 

160 
(** normalization of asts **) 

161 

18  162 
(* tracing options *) 
163 

164 
val trace_norm_ast = ref false; 

165 
val stat_norm_ast = ref false; 

166 

167 

0  168 
(* match *) 
169 

170 
fun match ast pat = 

171 
let 

172 
exception NO_MATCH; 

173 

1127
42ec82147d83
changed macro expander such that patterns also match prefixes of appls;
wenzelm
parents:
922
diff
changeset

174 
fun mtch (Constant a) (Constant b) env = 
0  175 
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

176 
 mtch (Variable a) (Constant b) env = 
0  177 
if a = b then env else raise NO_MATCH 
5689  178 
 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

179 
 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

180 
 mtch _ _ _ = raise NO_MATCH 
42ec82147d83
changed macro expander such that patterns also match prefixes of appls;
wenzelm
parents:
922
diff
changeset

181 
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

182 
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

183 
 mtch_lst [] [] env = env 
42ec82147d83
changed macro expander such that patterns also match prefixes of appls;
wenzelm
parents:
922
diff
changeset

184 
 mtch_lst _ _ _ = raise NO_MATCH; 
42ec82147d83
changed macro expander such that patterns also match prefixes of appls;
wenzelm
parents:
922
diff
changeset

185 

42ec82147d83
changed macro expander such that patterns also match prefixes of appls;
wenzelm
parents:
922
diff
changeset

186 
val (head, args) = 
42ec82147d83
changed macro expander such that patterns also match prefixes of appls;
wenzelm
parents:
922
diff
changeset

187 
(case (ast, pat) of 
42ec82147d83
changed macro expander such that patterns also match prefixes of appls;
wenzelm
parents:
922
diff
changeset

188 
(Appl asts, Appl pats) => 
42ec82147d83
changed macro expander such that patterns also match prefixes of appls;
wenzelm
parents:
922
diff
changeset

189 
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

190 
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

191 
else (ast, []) 
42ec82147d83
changed macro expander such that patterns also match prefixes of appls;
wenzelm
parents:
922
diff
changeset

192 
end 
42ec82147d83
changed macro expander such that patterns also match prefixes of appls;
wenzelm
parents:
922
diff
changeset

193 
 _ => (ast, [])); 
0  194 
in 
5689  195 
Some (mtch head pat Symtab.empty, args) handle NO_MATCH => None 
0  196 
end; 
197 

198 

18  199 
(* normalize *) 
0  200 

201 
(*the normalizer works yoyolike: topdown, bottomup, topdown, ...*) 

202 

18  203 
fun normalize trace stat get_rules pre_ast = 
0  204 
let 
205 
val passes = ref 0; 

206 
val lookups = ref 0; 

207 
val failed_matches = ref 0; 

208 
val changes = ref 0; 

209 

18  210 
fun subst _ (ast as Constant _) = ast 
5689  211 
 subst env (Variable x) = the (Symtab.lookup (env, x)) 
0  212 
 subst env (Appl asts) = Appl (map (subst env) asts); 
213 

214 
fun try_rules ast ((lhs, rhs) :: pats) = 

215 
(case match ast lhs of 

1127
42ec82147d83
changed macro expander such that patterns also match prefixes of appls;
wenzelm
parents:
922
diff
changeset

216 
Some (env, args) => 
42ec82147d83
changed macro expander such that patterns also match prefixes of appls;
wenzelm
parents:
922
diff
changeset

217 
(inc changes; Some (mk_appl (subst env rhs) args)) 
0  218 
 None => (inc failed_matches; try_rules ast pats)) 
18  219 
 try_rules _ [] = None; 
0  220 

221 
fun try ast a = (inc lookups; try_rules ast (the get_rules a)); 

222 

223 
fun rewrite (ast as Constant a) = try ast a 

224 
 rewrite (ast as Variable a) = try ast a 

225 
 rewrite (ast as Appl (Constant a :: _)) = try ast a 

226 
 rewrite (ast as Appl (Variable a :: _)) = try ast a 

227 
 rewrite _ = None; 

228 

229 
fun rewrote old_ast new_ast = 

230 
if trace then 

231 
writeln ("rewrote: " ^ str_of_ast old_ast ^ " > " ^ str_of_ast new_ast) 

232 
else (); 

233 

234 
fun norm_root ast = 

235 
(case rewrite ast of 

236 
Some new_ast => (rewrote ast new_ast; norm_root new_ast) 

237 
 None => ast); 

238 

239 
fun norm ast = 

240 
(case norm_root ast of 

241 
Appl sub_asts => 

242 
let 

243 
val old_changes = ! changes; 

244 
val new_ast = Appl (map norm sub_asts); 

245 
in 

246 
if old_changes = ! changes then new_ast else norm_root new_ast 

247 
end 

248 
 atomic_ast => atomic_ast); 

249 

250 
fun normal ast = 

251 
let 

252 
val old_changes = ! changes; 

253 
val new_ast = norm ast; 

254 
in 

255 
inc passes; 

256 
if old_changes = ! changes then new_ast else normal new_ast 

257 
end; 

258 

259 

18  260 
val _ = if trace then writeln ("pre: " ^ str_of_ast pre_ast) else (); 
0  261 

262 
val post_ast = if is_some get_rules then normal pre_ast else pre_ast; 

263 
in 

18  264 
if trace orelse stat then 
0  265 
writeln ("post: " ^ str_of_ast post_ast ^ "\nnormalize: " ^ 
266 
string_of_int (! passes) ^ " passes, " ^ 

267 
string_of_int (! lookups) ^ " lookups, " ^ 

268 
string_of_int (! changes) ^ " changes, " ^ 

269 
string_of_int (! failed_matches) ^ " matches failed") 

270 
else (); 

271 
post_ast 

272 
end; 

273 

274 

18  275 
(* normalize_ast *) 
276 

277 
fun normalize_ast get_rules ast = 

278 
normalize (! trace_norm_ast) (! stat_norm_ast) get_rules ast; 

279 

1506  280 
end; 
18  281 