author  wenzelm 
Fri, 02 Oct 2009 22:15:08 +0200  
changeset 32861  105f40051387 
parent 32740  9dd0a2f83429 
child 32952  aeb1e44fbc19 
permissions  rwrr 
24584  1 
(* Title: Tools/Compute_Oracle/am_sml.ML 
23663  2 
Author: Steven Obua 
3 

4 
ToDO: "parameterless rewrite cannot be used in pattern": In a lot of cases it CAN be used, and these cases should be handled properly; 

5 
right now, all cases throw an exception. 

6 

7 
*) 

8 

9 
signature AM_SML = 

10 
sig 

11 
include ABSTRACT_MACHINE 

12 
val save_result : (string * term) > unit 

13 
val set_compiled_rewriter : (term > term) > unit 

14 
val list_nth : 'a list * int > 'a 

32740  15 
val dump_output : (string option) Unsynchronized.ref 
23663  16 
end 
17 

18 
structure AM_SML : AM_SML = struct 

19 

20 
open AbstractMachine; 

21 

32740  22 
val dump_output = Unsynchronized.ref (NONE: string option) 
25520  23 

23663  24 
type program = string * string * (int Inttab.table) * (int Inttab.table) * (term Inttab.table) * (term > term) 
25 

32740  26 
val saved_result = Unsynchronized.ref (NONE:(string*term)option) 
23663  27 

28 
fun save_result r = (saved_result := SOME r) 

29 
fun clear_result () = (saved_result := NONE) 

30 

31 
val list_nth = List.nth 

32 

33 
(*fun list_nth (l,n) = (writeln (makestring ("list_nth", (length l,n))); List.nth (l,n))*) 

34 

32740  35 
val compiled_rewriter = Unsynchronized.ref (NONE:(term > term)Option.option) 
23663  36 

37 
fun set_compiled_rewriter r = (compiled_rewriter := SOME r) 

38 

39 
fun count_patternvars PVar = 1 

40 
 count_patternvars (PConst (_, ps)) = 

41 
List.foldl (fn (p, count) => (count_patternvars p)+count) 0 ps 

42 

43 
fun update_arity arity code a = 

44 
(case Inttab.lookup arity code of 

45 
NONE => Inttab.update_new (code, a) arity 

24134
6e69e0031f34
added int type constraints to accomodate hacked SML/NJ;
wenzelm
parents:
23663
diff
changeset

46 
 SOME (a': int) => if a > a' then Inttab.update (code, a) arity else arity) 
23663  47 

48 
(* We have to find out the maximal arity of each constant *) 

49 
fun collect_pattern_arity PVar arity = arity 

50 
 collect_pattern_arity (PConst (c, args)) arity = fold collect_pattern_arity args (update_arity arity c (length args)) 

51 

52 
(* We also need to find out the maximal toplevel arity of each function constant *) 

53 
fun collect_pattern_toplevel_arity PVar arity = raise Compile "internal error: collect_pattern_toplevel_arity" 

54 
 collect_pattern_toplevel_arity (PConst (c, args)) arity = update_arity arity c (length args) 

55 

56 
local 

57 
fun collect applevel (Var _) arity = arity 

58 
 collect applevel (Const c) arity = update_arity arity c applevel 

59 
 collect applevel (Abs m) arity = collect 0 m arity 

60 
 collect applevel (App (a,b)) arity = collect 0 b (collect (applevel + 1) a arity) 

61 
in 

62 
fun collect_term_arity t arity = collect 0 t arity 

63 
end 

64 

65 
fun collect_guard_arity (Guard (a,b)) arity = collect_term_arity b (collect_term_arity a arity) 

66 

67 

68 
fun rep n x = if n < 0 then raise Compile "internal error: rep" else if n = 0 then [] else x::(rep (n1) x) 

69 

70 
fun beta (Const c) = Const c 

71 
 beta (Var i) = Var i 

72 
 beta (App (Abs m, b)) = beta (unlift 0 (subst 0 m (lift 0 b))) 

73 
 beta (App (a, b)) = 

74 
(case beta a of 

75 
Abs m => beta (App (Abs m, b)) 

76 
 a => App (a, beta b)) 

77 
 beta (Abs m) = Abs (beta m) 

25217  78 
 beta (Computed t) = Computed t 
23663  79 
and subst x (Const c) t = Const c 
80 
 subst x (Var i) t = if i = x then t else Var i 

81 
 subst x (App (a,b)) t = App (subst x a t, subst x b t) 

82 
 subst x (Abs m) t = Abs (subst (x+1) m (lift 0 t)) 

83 
and lift level (Const c) = Const c 

84 
 lift level (App (a,b)) = App (lift level a, lift level b) 

85 
 lift level (Var i) = if i < level then Var i else Var (i+1) 

86 
 lift level (Abs m) = Abs (lift (level + 1) m) 

87 
and unlift level (Const c) = Const c 

88 
 unlift level (App (a, b)) = App (unlift level a, unlift level b) 

89 
 unlift level (Abs m) = Abs (unlift (level+1) m) 

90 
 unlift level (Var i) = if i < level then Var i else Var (i1) 

91 

92 
fun nlift level n (Var m) = if m < level then Var m else Var (m+n) 

93 
 nlift level n (Const c) = Const c 

94 
 nlift level n (App (a,b)) = App (nlift level n a, nlift level n b) 

95 
 nlift level n (Abs b) = Abs (nlift (level+1) n b) 

96 

97 
fun subst_const (c, t) (Const c') = if c = c' then t else Const c' 

98 
 subst_const _ (Var i) = Var i 

99 
 subst_const ct (App (a, b)) = App (subst_const ct a, subst_const ct b) 

100 
 subst_const ct (Abs m) = Abs (subst_const ct m) 

101 

102 
(* Remove all rules that are just parameterless rewrites. This is necessary because SML does not allow functions with no parameters. *) 

103 
fun inline_rules rules = 

104 
let 

105 
fun term_contains_const c (App (a, b)) = term_contains_const c a orelse term_contains_const c b 

106 
 term_contains_const c (Abs m) = term_contains_const c m 

107 
 term_contains_const c (Var i) = false 

108 
 term_contains_const c (Const c') = (c = c') 

109 
fun find_rewrite [] = NONE 

110 
 find_rewrite ((prems, PConst (c, []), r) :: _) = 

111 
if check_freevars 0 r then 

112 
if term_contains_const c r then 

113 
raise Compile "parameterless rewrite is caught in cycle" 

114 
else if not (null prems) then 

115 
raise Compile "parameterless rewrite may not be guarded" 

116 
else 

117 
SOME (c, r) 

118 
else raise Compile "unbound variable on right hand side or guards of rule" 

119 
 find_rewrite (_ :: rules) = find_rewrite rules 

120 
fun remove_rewrite (c,r) [] = [] 

121 
 remove_rewrite (cr as (c,r)) ((rule as (prems', PConst (c', args), r'))::rules) = 

122 
(if c = c' then 

123 
if null args andalso r = r' andalso null (prems') then 

124 
remove_rewrite cr rules 

125 
else raise Compile "incompatible parameterless rewrites found" 

126 
else 

127 
rule :: (remove_rewrite cr rules)) 

128 
 remove_rewrite cr (r::rs) = r::(remove_rewrite cr rs) 

129 
fun pattern_contains_const c (PConst (c', args)) = (c = c' orelse exists (pattern_contains_const c) args) 

130 
 pattern_contains_const c (PVar) = false 

131 
fun inline_rewrite (ct as (c, _)) (prems, p, r) = 

132 
if pattern_contains_const c p then 

133 
raise Compile "parameterless rewrite cannot be used in pattern" 

134 
else (map (fn (Guard (a,b)) => Guard (subst_const ct a, subst_const ct b)) prems, p, subst_const ct r) 

135 
fun inline inlined rules = 

136 
(case find_rewrite rules of 

137 
NONE => (Inttab.make inlined, rules) 

138 
 SOME ct => 

139 
let 

140 
val rules = map (inline_rewrite ct) (remove_rewrite ct rules) 

141 
val inlined = ct :: (map (fn (c', r) => (c', subst_const ct r)) inlined) 

142 
in 

143 
inline inlined rules 

144 
end) 

145 
in 

146 
inline [] rules 

147 
end 

148 

149 

150 
(* 

151 
Calculate the arity, the toplevel_arity, and adjust rules so that all toplevel pattern constants have maximal arity. 

152 
Also beta reduce the adjusted right hand side of a rule. 

153 
*) 

154 
fun adjust_rules rules = 

155 
let 

156 
val arity = fold (fn (prems, p, t) => fn arity => fold collect_guard_arity prems (collect_term_arity t (collect_pattern_arity p arity))) rules Inttab.empty 

157 
val toplevel_arity = fold (fn (_, p, t) => fn arity => collect_pattern_toplevel_arity p arity) rules Inttab.empty 

158 
fun arity_of c = the (Inttab.lookup arity c) 

159 
fun toplevel_arity_of c = the (Inttab.lookup toplevel_arity c) 

25520  160 
fun test_pattern PVar = () 
161 
 test_pattern (C as PConst (c, args)) = if (length args <> arity_of c) then raise Compile ("Constant inside pattern must have maximal arity") else (map test_pattern args; ()) 

23663  162 
fun adjust_rule (_, PVar, _) = raise Compile ("pattern may not be a variable") 
163 
 adjust_rule (_, PConst (_, []), _) = raise Compile ("cannot deal with rewrites that take no parameters") 

164 
 adjust_rule (rule as (prems, p as PConst (c, args),t)) = 

165 
let 

166 
val patternvars_counted = count_patternvars p 

167 
fun check_fv t = check_freevars patternvars_counted t 

168 
val _ = if not (check_fv t) then raise Compile ("unbound variables on right hand side of rule") else () 

169 
val _ = if not (forall (fn (Guard (a,b)) => check_fv a andalso check_fv b) prems) then raise Compile ("unbound variables in guards") else () 

25520  170 
val _ = map test_pattern args 
23663  171 
val len = length args 
172 
val arity = arity_of c 

173 
val lift = nlift 0 

25520  174 
fun addapps_tm n t = if n=0 then t else addapps_tm (n1) (App (t, Var (n1))) 
175 
fun adjust_term n t = addapps_tm n (lift n t) 

176 
fun adjust_guard n (Guard (a,b)) = Guard (lift n a, lift n b) 

23663  177 
in 
178 
if len = arity then 

179 
rule 

180 
else if arity >= len then 

181 
(map (adjust_guard (aritylen)) prems, PConst (c, args @ (rep (aritylen) PVar)), adjust_term (aritylen) t) 

182 
else (raise Compile "internal error in adjust_rule") 

183 
end 

25520  184 
fun beta_rule (prems, p, t) = ((prems, p, beta t) handle Match => raise Compile "beta_rule") 
23663  185 
in 
186 
(arity, toplevel_arity, map (beta_rule o adjust_rule) rules) 

187 
end 

188 

189 
fun print_term module arity_of toplevel_arity_of pattern_var_count pattern_lazy_var_count = 

190 
let 

191 
fun str x = string_of_int x 

192 
fun protect_blank s = if exists_string Symbol.is_ascii_blank s then "(" ^ s ^")" else s 

193 
val module_prefix = (case module of NONE => ""  SOME s => s^".") 

194 
fun print_apps d f [] = f 

195 
 print_apps d f (a::args) = print_apps d (module_prefix^"app "^(protect_blank f)^" "^(protect_blank (print_term d a))) args 

196 
and print_call d (App (a, b)) args = print_call d a (b::args) 

197 
 print_call d (Const c) args = 

198 
(case arity_of c of 

199 
NONE => print_apps d (module_prefix^"Const "^(str c)) args 

200 
 SOME 0 => module_prefix^"C"^(str c) 

201 
 SOME a => 

202 
let 

203 
val len = length args 

204 
in 

205 
if a <= len then 

206 
let 

207 
val strict_a = (case toplevel_arity_of c of SOME sa => sa  NONE => a) 

208 
val _ = if strict_a > a then raise Compile "strict" else () 

209 
val s = module_prefix^"c"^(str c)^(concat (map (fn t => " "^(protect_blank (print_term d t))) (List.take (args, strict_a)))) 

210 
val s = s^(concat (map (fn t => " (fn () => "^print_term d t^")") (List.drop (List.take (args, a), strict_a)))) 

211 
in 

212 
print_apps d s (List.drop (args, a)) 

213 
end 

214 
else 

215 
let 

216 
fun mk_apps n t = if n = 0 then t else mk_apps (n1) (App (t, Var (n  1))) 

217 
fun mk_lambdas n t = if n = 0 then t else mk_lambdas (n1) (Abs t) 

218 
fun append_args [] t = t 

219 
 append_args (c::cs) t = append_args cs (App (t, c)) 

220 
in 

221 
print_term d (mk_lambdas (alen) (mk_apps (alen) (nlift 0 (alen) (append_args args (Const c))))) 

222 
end 

223 
end) 

224 
 print_call d t args = print_apps d (print_term d t) args 

225 
and print_term d (Var x) = 

226 
if x < d then 

227 
"b"^(str (dx1)) 

228 
else 

229 
let 

230 
val n = pattern_var_count  (xd)  1 

231 
val x = "x"^(str n) 

232 
in 

233 
if n < pattern_var_count  pattern_lazy_var_count then 

234 
x 

235 
else 

236 
"("^x^" ())" 

237 
end 

238 
 print_term d (Abs c) = module_prefix^"Abs (fn b"^(str d)^" => "^(print_term (d + 1) c)^")" 

239 
 print_term d t = print_call d t [] 

240 
in 

241 
print_term 0 

242 
end 

243 

244 
fun section n = if n = 0 then [] else (section (n1))@[n1] 

245 

246 
fun print_rule gnum arity_of toplevel_arity_of (guards, p, t) = 

247 
let 

248 
fun str x = Int.toString x 

249 
fun print_pattern top n PVar = (n+1, "x"^(str n)) 

250 
 print_pattern top n (PConst (c, [])) = (n, (if top then "c" else "C")^(str c)^(if top andalso gnum > 0 then "_"^(str gnum) else "")) 

251 
 print_pattern top n (PConst (c, args)) = 

252 
let 

253 
val f = (if top then "c" else "C")^(str c)^(if top andalso gnum > 0 then "_"^(str gnum) else "") 

254 
val (n, s) = print_pattern_list 0 top (n, f) args 

255 
in 

256 
(n, s) 

257 
end 

258 
and print_pattern_list' counter top (n,p) [] = if top then (n,p) else (n,p^")") 

259 
 print_pattern_list' counter top (n, p) (t::ts) = 

260 
let 

261 
val (n, t) = print_pattern false n t 

262 
in 

263 
print_pattern_list' (counter + 1) top (n, if top then p^" (a"^(str counter)^" as ("^t^"))" else p^", "^t) ts 

264 
end 

265 
and print_pattern_list counter top (n, p) (t::ts) = 

266 
let 

267 
val (n, t) = print_pattern false n t 

268 
in 

269 
print_pattern_list' (counter + 1) top (n, if top then p^" (a"^(str counter)^" as ("^t^"))" else p^" ("^t) ts 

270 
end 

271 
val c = (case p of PConst (c, _) => c  _ => raise Match) 

272 
val (n, pattern) = print_pattern true 0 p 

273 
val lazy_vars = the (arity_of c)  the (toplevel_arity_of c) 

274 
fun print_tm tm = print_term NONE arity_of toplevel_arity_of n lazy_vars tm 

275 
fun print_guard (Guard (a,b)) = "term_eq ("^(print_tm a)^") ("^(print_tm b)^")" 

276 
val else_branch = "c"^(str c)^"_"^(str (gnum+1))^(concat (map (fn i => " a"^(str i)) (section (the (arity_of c))))) 

277 
fun print_guards t [] = print_tm t 

278 
 print_guards t (g::gs) = "if ("^(print_guard g)^")"^(concat (map (fn g => " andalso ("^(print_guard g)^")") gs))^" then ("^(print_tm t)^") else "^else_branch 

279 
in 

280 
(if null guards then gnum else gnum+1, pattern^" = "^(print_guards t guards)) 

281 
end 

282 

283 
fun group_rules rules = 

284 
let 

285 
fun add_rule (r as (_, PConst (c,_), _)) groups = 

286 
let 

287 
val rs = (case Inttab.lookup groups c of NONE => []  SOME rs => rs) 

288 
in 

289 
Inttab.update (c, r::rs) groups 

290 
end 

291 
 add_rule _ _ = raise Compile "internal error group_rules" 

292 
in 

293 
fold_rev add_rule rules Inttab.empty 

294 
end 

295 

296 
fun sml_prog name code rules = 

297 
let 

32740  298 
val buffer = Unsynchronized.ref "" 
23663  299 
fun write s = (buffer := (!buffer)^s) 
300 
fun writeln s = (write s; write "\n") 

301 
fun writelist [] = () 

302 
 writelist (s::ss) = (writeln s; writelist ss) 

303 
fun str i = Int.toString i 

304 
val (inlinetab, rules) = inline_rules rules 

305 
val (arity, toplevel_arity, rules) = adjust_rules rules 

306 
val rules = group_rules rules 

307 
val constants = Inttab.keys arity 

308 
fun arity_of c = Inttab.lookup arity c 

309 
fun toplevel_arity_of c = Inttab.lookup toplevel_arity c 

310 
fun rep_str s n = concat (rep n s) 

311 
fun indexed s n = s^(str n) 

312 
fun string_of_tuple [] = "" 

313 
 string_of_tuple (x::xs) = "("^x^(concat (map (fn s => ", "^s) xs))^")" 

314 
fun string_of_args [] = "" 

315 
 string_of_args (x::xs) = x^(concat (map (fn s => " "^s) xs)) 

316 
fun default_case gnum c = 

317 
let 

318 
val leftargs = concat (map (indexed " x") (section (the (arity_of c)))) 

319 
val rightargs = section (the (arity_of c)) 

320 
val strict_args = (case toplevel_arity_of c of NONE => the (arity_of c)  SOME sa => sa) 

321 
val xs = map (fn n => if n < strict_args then "x"^(str n) else "x"^(str n)^"()") rightargs 

322 
val right = (indexed "C" c)^" "^(string_of_tuple xs) 

31322
526e149999cc
attempt to eliminate adhoc makestring at runtime (which is not welldefined);
wenzelm
parents:
30678
diff
changeset

323 
val message = "(\"unresolved lazy call: " ^ string_of_int c ^ "\")" 
24654  324 
val right = if strict_args < the (arity_of c) then "raise AM_SML.Run "^message else right 
23663  325 
in 
326 
(indexed "c" c)^(if gnum > 0 then "_"^(str gnum) else "")^leftargs^" = "^right 

327 
end 

328 

329 
fun eval_rules c = 

330 
let 

331 
val arity = the (arity_of c) 

332 
val strict_arity = (case toplevel_arity_of c of NONE => arity  SOME sa => sa) 

333 
fun eval_rule n = 

334 
let 

335 
val sc = string_of_int c 

336 
val left = fold (fn i => fn s => "AbstractMachine.App ("^s^(indexed ", x" i)^")") (section n) ("AbstractMachine.Const "^sc) 

337 
fun arg i = 

338 
let 

339 
val x = indexed "x" i 

340 
val x = if i < n then "(eval bounds "^x^")" else x 

341 
val x = if i < strict_arity then x else "(fn () => "^x^")" 

342 
in 

343 
x 

344 
end 

345 
val right = "c"^sc^" "^(string_of_args (map arg (section arity))) 

346 
val right = fold_rev (fn i => fn s => "Abs (fn "^(indexed "x" i)^" => "^s^")") (List.drop (section arity, n)) right 

347 
val right = if arity > 0 then right else "C"^sc 

348 
in 

349 
"  eval bounds ("^left^") = "^right 

350 
end 

351 
in 

352 
map eval_rule (rev (section (arity + 1))) 

353 
end 

25217  354 

25220  355 
fun convert_computed_rules (c: int) : string list = 
25217  356 
let 
357 
val arity = the (arity_of c) 

358 
fun eval_rule () = 

359 
let 

360 
val sc = string_of_int c 

361 
val left = fold (fn i => fn s => "AbstractMachine.App ("^s^(indexed ", x" i)^")") (section arity) ("AbstractMachine.Const "^sc) 

362 
fun arg i = "(convert_computed "^(indexed "x" i)^")" 

363 
val right = "C"^sc^" "^(string_of_tuple (map arg (section arity))) 

364 
val right = if arity > 0 then right else "C"^sc 

365 
in 

366 
"  convert_computed ("^left^") = "^right 

367 
end 

368 
in 

369 
[eval_rule ()] 

370 
end 

23663  371 

372 
fun mk_constr_type_args n = if n > 0 then " of Term "^(rep_str " * Term" (n1)) else "" 

24654  373 
val _ = writelist [ 
23663  374 
"structure "^name^" = struct", 
375 
"", 

376 
"datatype Term = Const of int  App of Term * Term  Abs of (Term > Term)", 

377 
" "^(concat (map (fn c => "  C"^(str c)^(mk_constr_type_args (the (arity_of c)))) constants)), 

378 
""] 

379 
fun make_constr c argprefix = "(C"^(str c)^" "^(string_of_tuple (map (fn i => argprefix^(str i)) (section (the (arity_of c)))))^")" 

380 
fun make_term_eq c = "  term_eq "^(make_constr c "a")^" "^(make_constr c "b")^" = "^ 

381 
(case the (arity_of c) of 

382 
0 => "true" 

383 
 n => 

384 
let 

385 
val eqs = map (fn i => "term_eq a"^(str i)^" b"^(str i)) (section n) 

386 
val (eq, eqs) = (List.hd eqs, map (fn s => " andalso "^s) (List.tl eqs)) 

387 
in 

388 
eq^(concat eqs) 

389 
end) 

390 
val _ = writelist [ 

391 
"fun term_eq (Const c1) (Const c2) = (c1 = c2)", 

392 
"  term_eq (App (a1,a2)) (App (b1,b2)) = term_eq a1 b1 andalso term_eq a2 b2"] 

393 
val _ = writelist (map make_term_eq constants) 

394 
val _ = writelist [ 

395 
"  term_eq _ _ = false", 

396 
"" 

397 
] 

398 
val _ = writelist [ 

399 
"fun app (Abs a) b = a b", 

400 
"  app a b = App (a, b)", 

401 
""] 

402 
fun defcase gnum c = (case arity_of c of NONE => []  SOME a => if a > 0 then [default_case gnum c] else []) 

403 
fun writefundecl [] = () 

404 
 writefundecl (x::xs) = writelist ((("and "^x)::(map (fn s => "  "^s) xs))) 

405 
fun list_group c = (case Inttab.lookup rules c of 

406 
NONE => [defcase 0 c] 

407 
 SOME rs => 

408 
let 

409 
val rs = 

410 
fold 

411 
(fn r => 

412 
fn rs => 

413 
let 

414 
val (gnum, l, rs) = 

415 
(case rs of 

416 
[] => (0, [], []) 

417 
 (gnum, l)::rs => (gnum, l, rs)) 

418 
val (gnum', r) = print_rule gnum arity_of toplevel_arity_of r 

419 
in 

420 
if gnum' = gnum then 

421 
(gnum, r::l)::rs 

422 
else 

423 
let 

424 
val args = concat (map (fn i => " a"^(str i)) (section (the (arity_of c)))) 

425 
fun gnumc g = if g > 0 then "c"^(str c)^"_"^(str g)^args else "c"^(str c)^args 

426 
val s = gnumc (gnum) ^ " = " ^ gnumc (gnum') 

427 
in 

428 
(gnum', [])::(gnum, s::r::l)::rs 

429 
end 

430 
end) 

431 
rs [] 

432 
val rs = (case rs of [] => [(0,defcase 0 c)]  (gnum,l)::rs => (gnum, (defcase gnum c)@l)::rs) 

433 
in 

434 
rev (map (fn z => rev (snd z)) rs) 

435 
end) 

436 
val _ = map (fn z => (map writefundecl z; writeln "")) (map list_group constants) 

437 
val _ = writelist [ 

438 
"fun convert (Const i) = AM_SML.Const i", 

439 
"  convert (App (a, b)) = AM_SML.App (convert a, convert b)", 

440 
"  convert (Abs _) = raise AM_SML.Run \"no abstraction in result allowed\""] 

441 
fun make_convert c = 

442 
let 

443 
val args = map (indexed "a") (section (the (arity_of c))) 

444 
val leftargs = 

445 
case args of 

446 
[] => "" 

447 
 (x::xs) => "("^x^(concat (map (fn s => ", "^s) xs))^")" 

448 
val args = map (indexed "convert a") (section (the (arity_of c))) 

449 
val right = fold (fn x => fn s => "AM_SML.App ("^s^", "^x^")") args ("AM_SML.Const "^(str c)) 

450 
in 

451 
"  convert (C"^(str c)^" "^leftargs^") = "^right 

452 
end 

453 
val _ = writelist (map make_convert constants) 

25217  454 
val _ = writelist [ 
455 
"", 

456 
"fun convert_computed (AbstractMachine.Abs b) = raise AM_SML.Run \"no abstraction in convert_computed allowed\"", 

457 
"  convert_computed (AbstractMachine.Var i) = raise AM_SML.Run \"no bound variables in convert_computed allowed\""] 

458 
val _ = map (writelist o convert_computed_rules) constants 

459 
val _ = writelist [ 

460 
"  convert_computed (AbstractMachine.Const c) = Const c", 

461 
"  convert_computed (AbstractMachine.App (a, b)) = App (convert_computed a, convert_computed b)", 

462 
"  convert_computed (AbstractMachine.Computed a) = raise AM_SML.Run \"no nesting in convert_computed allowed\""] 

23663  463 
val _ = writelist [ 
464 
"", 

465 
"fun eval bounds (AbstractMachine.Abs m) = Abs (fn b => eval (b::bounds) m)", 

466 
"  eval bounds (AbstractMachine.Var i) = AM_SML.list_nth (bounds, i)"] 

467 
val _ = map (writelist o eval_rules) constants 

468 
val _ = writelist [ 

469 
"  eval bounds (AbstractMachine.App (a, b)) = app (eval bounds a) (eval bounds b)", 

25217  470 
"  eval bounds (AbstractMachine.Const c) = Const c", 
471 
"  eval bounds (AbstractMachine.Computed t) = convert_computed t"] 

23663  472 
val _ = writelist [ 
473 
"", 

474 
"fun export term = AM_SML.save_result (\""^code^"\", convert term)", 

475 
"", 

24654  476 
"val _ = AM_SML.set_compiled_rewriter (fn t => (convert (eval [] t)))", 
23663  477 
"", 
478 
"end"] 

479 
in 

480 
(arity, toplevel_arity, inlinetab, !buffer) 

481 
end 

482 

32740  483 
val guid_counter = Unsynchronized.ref 0 
23663  484 
fun get_guid () = 
485 
let 

486 
val c = !guid_counter 

487 
val _ = guid_counter := !guid_counter + 1 

488 
in 

489 
(LargeInt.toString (Time.toMicroseconds (Time.now ()))) ^ (string_of_int c) 

490 
end 

491 

492 

493 
fun writeTextFile name s = File.write (Path.explode name) s 

494 

31327  495 
fun use_source src = use_text ML_Env.local_context (1, "") false src 
23663  496 

25520  497 
fun compile cache_patterns const_arity eqs = 
23663  498 
let 
499 
val guid = get_guid () 

500 
val code = Real.toString (random ()) 

501 
val module = "AMSML_"^guid 

502 
val (arity, toplevel_arity, inlinetab, source) = sml_prog module code eqs 

25520  503 
val _ = case !dump_output of NONE => ()  SOME p => writeTextFile p source 
23663  504 
val _ = compiled_rewriter := NONE 
505 
val _ = use_source source 

506 
in 

507 
case !compiled_rewriter of 

508 
NONE => raise Compile "broken link to compiled function" 

509 
 SOME f => (module, code, arity, toplevel_arity, inlinetab, f) 

510 
end 

511 

512 

513 
fun run' (module, code, arity, toplevel_arity, inlinetab, compiled_fun) t = 

514 
let 

515 
val _ = if check_freevars 0 t then () else raise Run ("can only compute closed terms") 

516 
fun inline (Const c) = (case Inttab.lookup inlinetab c of NONE => Const c  SOME t => t) 

517 
 inline (Var i) = Var i 

518 
 inline (App (a, b)) = App (inline a, inline b) 

519 
 inline (Abs m) = Abs (inline m) 

520 
val t = beta (inline t) 

521 
fun arity_of c = Inttab.lookup arity c 

522 
fun toplevel_arity_of c = Inttab.lookup toplevel_arity c 

523 
val term = print_term NONE arity_of toplevel_arity_of 0 0 t 

524 
val source = "local open "^module^" in val _ = export ("^term^") end" 

525 
val _ = writeTextFile "Gencode_call.ML" source 

526 
val _ = clear_result () 

527 
val _ = use_source source 

528 
in 

529 
case !saved_result of 

530 
NONE => raise Run "broken link to compiled code" 

531 
 SOME (code', t) => (clear_result (); if code' = code then t else raise Run "link to compiled code was hijacked") 

532 
end 

533 

534 
fun run (module, code, arity, toplevel_arity, inlinetab, compiled_fun) t = 

535 
let 

536 
val _ = if check_freevars 0 t then () else raise Run ("can only compute closed terms") 

537 
fun inline (Const c) = (case Inttab.lookup inlinetab c of NONE => Const c  SOME t => t) 

538 
 inline (Var i) = Var i 

539 
 inline (App (a, b)) = App (inline a, inline b) 

540 
 inline (Abs m) = Abs (inline m) 

25217  541 
 inline (Computed t) = Computed t 
23663  542 
in 
543 
compiled_fun (beta (inline t)) 

544 
end 

545 

546 
fun discard p = () 

547 

548 
end 