author | wenzelm |
Wed, 21 Jul 2010 15:44:36 +0200 | |
changeset 37872 | d83659570337 |
parent 32960 | src/Tools/Compute_Oracle/am_sml.ML@69916a850301 |
child 41490 | 0f1e411a1448 |
permissions | -rw-r--r-- |
24584 | 1 |
(* Title: Tools/Compute_Oracle/am_sml.ML |
23663 | 2 |
Author: Steven Obua |
3 |
||
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
4 |
TODO: "parameterless rewrite cannot be used in pattern": In a lot of |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
5 |
cases it CAN be used, and these cases should be handled |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
6 |
properly; right now, all cases raise an exception. |
23663 | 7 |
*) |
8 |
||
9 |
signature AM_SML = |
|
10 |
sig |
|
11 |
include ABSTRACT_MACHINE |
|
12 |
val save_result : (string * term) -> unit |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
13 |
val set_compiled_rewriter : (term -> term) -> unit |
23663 | 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 |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
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 (n-1) 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 |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
75 |
Abs m => beta (App (Abs m, b)) |
23663 | 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 (i-1) |
|
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 |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
105 |
fun term_contains_const c (App (a, b)) = term_contains_const c a orelse term_contains_const c b |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
106 |
| term_contains_const c (Abs m) = term_contains_const c m |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
107 |
| term_contains_const c (Var i) = false |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
108 |
| term_contains_const c (Const c') = (c = c') |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
109 |
fun find_rewrite [] = NONE |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
110 |
| find_rewrite ((prems, PConst (c, []), r) :: _) = |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
111 |
if check_freevars 0 r then |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
112 |
if term_contains_const c r then |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
113 |
raise Compile "parameterless rewrite is caught in cycle" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
114 |
else if not (null prems) then |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
115 |
raise Compile "parameterless rewrite may not be guarded" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
116 |
else |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
117 |
SOME (c, r) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
118 |
else raise Compile "unbound variable on right hand side or guards of rule" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
119 |
| find_rewrite (_ :: rules) = find_rewrite rules |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
120 |
fun remove_rewrite (c,r) [] = [] |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
121 |
| remove_rewrite (cr as (c,r)) ((rule as (prems', PConst (c', args), r'))::rules) = |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
122 |
(if c = c' then |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
123 |
if null args andalso r = r' andalso null (prems') then |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
124 |
remove_rewrite cr rules |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
125 |
else raise Compile "incompatible parameterless rewrites found" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
126 |
else |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
127 |
rule :: (remove_rewrite cr rules)) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
128 |
| remove_rewrite cr (r::rs) = r::(remove_rewrite cr rs) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
129 |
fun pattern_contains_const c (PConst (c', args)) = (c = c' orelse exists (pattern_contains_const c) args) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
130 |
| pattern_contains_const c (PVar) = false |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
131 |
fun inline_rewrite (ct as (c, _)) (prems, p, r) = |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
132 |
if pattern_contains_const c p then |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
133 |
raise Compile "parameterless rewrite cannot be used in pattern" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
134 |
else (map (fn (Guard (a,b)) => Guard (subst_const ct a, subst_const ct b)) prems, p, subst_const ct r) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
135 |
fun inline inlined rules = |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
136 |
(case find_rewrite rules of |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
137 |
NONE => (Inttab.make inlined, rules) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
138 |
| SOME ct => |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
139 |
let |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
140 |
val rules = map (inline_rewrite ct) (remove_rewrite ct rules) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
141 |
val inlined = ct :: (map (fn (c', r) => (c', subst_const ct r)) inlined) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
142 |
in |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
143 |
inline inlined rules |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
144 |
end) |
23663 | 145 |
in |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
146 |
inline [] rules |
23663 | 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 |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
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 |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
157 |
val toplevel_arity = fold (fn (_, p, t) => fn arity => collect_pattern_toplevel_arity p arity) rules Inttab.empty |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
158 |
fun arity_of c = the (Inttab.lookup arity c) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
159 |
fun toplevel_arity_of c = the (Inttab.lookup toplevel_arity c) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
160 |
fun test_pattern PVar = () |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
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; ()) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
162 |
fun adjust_rule (_, PVar, _) = raise Compile ("pattern may not be a variable") |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
163 |
| adjust_rule (_, PConst (_, []), _) = raise Compile ("cannot deal with rewrites that take no parameters") |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
164 |
| adjust_rule (rule as (prems, p as PConst (c, args),t)) = |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
165 |
let |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
166 |
val patternvars_counted = count_patternvars p |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
167 |
fun check_fv t = check_freevars patternvars_counted t |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
168 |
val _ = if not (check_fv t) then raise Compile ("unbound variables on right hand side of rule") else () |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
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 () |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
170 |
val _ = map test_pattern args |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
171 |
val len = length args |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
172 |
val arity = arity_of c |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
173 |
val lift = nlift 0 |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
174 |
fun addapps_tm n t = if n=0 then t else addapps_tm (n-1) (App (t, Var (n-1))) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
175 |
fun adjust_term n t = addapps_tm n (lift n t) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
176 |
fun adjust_guard n (Guard (a,b)) = Guard (lift n a, lift n b) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
177 |
in |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
178 |
if len = arity then |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
179 |
rule |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
180 |
else if arity >= len then |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
181 |
(map (adjust_guard (arity-len)) prems, PConst (c, args @ (rep (arity-len) PVar)), adjust_term (arity-len) t) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
182 |
else (raise Compile "internal error in adjust_rule") |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
183 |
end |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
184 |
fun beta_rule (prems, p, t) = ((prems, p, beta t) handle Match => raise Compile "beta_rule") |
23663 | 185 |
in |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
186 |
(arity, toplevel_arity, map (beta_rule o adjust_rule) rules) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
187 |
end |
23663 | 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 |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
193 |
val module_prefix = (case module of NONE => "" | SOME s => s^".") |
23663 | 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 = |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
198 |
(case arity_of c of |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
199 |
NONE => print_apps d (module_prefix^"Const "^(str c)) args |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
200 |
| SOME 0 => module_prefix^"C"^(str c) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
201 |
| SOME a => |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
202 |
let |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
203 |
val len = length args |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
204 |
in |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
205 |
if a <= len then |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
206 |
let |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
207 |
val strict_a = (case toplevel_arity_of c of SOME sa => sa | NONE => a) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
208 |
val _ = if strict_a > a then raise Compile "strict" else () |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
209 |
val s = module_prefix^"c"^(str c)^(implode (map (fn t => " "^(protect_blank (print_term d t))) (List.take (args, strict_a)))) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
210 |
val s = s^(implode (map (fn t => " (fn () => "^print_term d t^")") (List.drop (List.take (args, a), strict_a)))) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
211 |
in |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
212 |
print_apps d s (List.drop (args, a)) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
213 |
end |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
214 |
else |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
215 |
let |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
216 |
fun mk_apps n t = if n = 0 then t else mk_apps (n-1) (App (t, Var (n - 1))) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
217 |
fun mk_lambdas n t = if n = 0 then t else mk_lambdas (n-1) (Abs t) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
218 |
fun append_args [] t = t |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
219 |
| append_args (c::cs) t = append_args cs (App (t, c)) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
220 |
in |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
221 |
print_term d (mk_lambdas (a-len) (mk_apps (a-len) (nlift 0 (a-len) (append_args args (Const c))))) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
222 |
end |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
223 |
end) |
23663 | 224 |
| print_call d t args = print_apps d (print_term d t) args |
225 |
and print_term d (Var x) = |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
226 |
if x < d then |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
227 |
"b"^(str (d-x-1)) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
228 |
else |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
229 |
let |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
230 |
val n = pattern_var_count - (x-d) - 1 |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
231 |
val x = "x"^(str n) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
232 |
in |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
233 |
if n < pattern_var_count - pattern_lazy_var_count then |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
234 |
x |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
235 |
else |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
236 |
"("^x^" ())" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
237 |
end |
23663 | 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 (n-1))@[n-1] |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
245 |
|
23663 | 246 |
fun print_rule gnum arity_of toplevel_arity_of (guards, p, t) = |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
247 |
let |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
248 |
fun str x = Int.toString x |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
249 |
fun print_pattern top n PVar = (n+1, "x"^(str n)) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
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 "")) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
251 |
| print_pattern top n (PConst (c, args)) = |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
252 |
let |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
253 |
val f = (if top then "c" else "C")^(str c)^(if top andalso gnum > 0 then "_"^(str gnum) else "") |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
254 |
val (n, s) = print_pattern_list 0 top (n, f) args |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
255 |
in |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
256 |
(n, s) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
257 |
end |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
258 |
and print_pattern_list' counter top (n,p) [] = if top then (n,p) else (n,p^")") |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
259 |
| print_pattern_list' counter top (n, p) (t::ts) = |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
260 |
let |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
261 |
val (n, t) = print_pattern false n t |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
262 |
in |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
263 |
print_pattern_list' (counter + 1) top (n, if top then p^" (a"^(str counter)^" as ("^t^"))" else p^", "^t) ts |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
264 |
end |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
265 |
and print_pattern_list counter top (n, p) (t::ts) = |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
266 |
let |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
267 |
val (n, t) = print_pattern false n t |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
268 |
in |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
269 |
print_pattern_list' (counter + 1) top (n, if top then p^" (a"^(str counter)^" as ("^t^"))" else p^" ("^t) ts |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
270 |
end |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
271 |
val c = (case p of PConst (c, _) => c | _ => raise Match) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
272 |
val (n, pattern) = print_pattern true 0 p |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
273 |
val lazy_vars = the (arity_of c) - the (toplevel_arity_of c) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
274 |
fun print_tm tm = print_term NONE arity_of toplevel_arity_of n lazy_vars tm |
23663 | 275 |
fun print_guard (Guard (a,b)) = "term_eq ("^(print_tm a)^") ("^(print_tm b)^")" |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
276 |
val else_branch = "c"^(str c)^"_"^(str (gnum+1))^(implode (map (fn i => " a"^(str i)) (section (the (arity_of c))))) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
277 |
fun print_guards t [] = print_tm t |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
278 |
| print_guards t (g::gs) = "if ("^(print_guard g)^")"^(implode (map (fn g => " andalso ("^(print_guard g)^")") gs))^" then ("^(print_tm t)^") else "^else_branch |
23663 | 279 |
in |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
280 |
(if null guards then gnum else gnum+1, pattern^" = "^(print_guards t guards)) |
23663 | 281 |
end |
282 |
||
283 |
fun group_rules rules = |
|
284 |
let |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
285 |
fun add_rule (r as (_, PConst (c,_), _)) groups = |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
286 |
let |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
287 |
val rs = (case Inttab.lookup groups c of NONE => [] | SOME rs => rs) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
288 |
in |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
289 |
Inttab.update (c, r::rs) groups |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
290 |
end |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
291 |
| add_rule _ _ = raise Compile "internal error group_rules" |
23663 | 292 |
in |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
293 |
fold_rev add_rule rules Inttab.empty |
23663 | 294 |
end |
295 |
||
296 |
fun sml_prog name code rules = |
|
297 |
let |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
298 |
val buffer = Unsynchronized.ref "" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
299 |
fun write s = (buffer := (!buffer)^s) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
300 |
fun writeln s = (write s; write "\n") |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
301 |
fun writelist [] = () |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
302 |
| writelist (s::ss) = (writeln s; writelist ss) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
303 |
fun str i = Int.toString i |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
304 |
val (inlinetab, rules) = inline_rules rules |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
305 |
val (arity, toplevel_arity, rules) = adjust_rules rules |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
306 |
val rules = group_rules rules |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
307 |
val constants = Inttab.keys arity |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
308 |
fun arity_of c = Inttab.lookup arity c |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
309 |
fun toplevel_arity_of c = Inttab.lookup toplevel_arity c |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
310 |
fun rep_str s n = implode (rep n s) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
311 |
fun indexed s n = s^(str n) |
23663 | 312 |
fun string_of_tuple [] = "" |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
313 |
| string_of_tuple (x::xs) = "("^x^(implode (map (fn s => ", "^s) xs))^")" |
23663 | 314 |
fun string_of_args [] = "" |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
315 |
| string_of_args (x::xs) = x^(implode (map (fn s => " "^s) xs)) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
316 |
fun default_case gnum c = |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
317 |
let |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
318 |
val leftargs = implode (map (indexed " x") (section (the (arity_of c)))) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
319 |
val rightargs = section (the (arity_of c)) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
320 |
val strict_args = (case toplevel_arity_of c of NONE => the (arity_of c) | SOME sa => sa) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
321 |
val xs = map (fn n => if n < strict_args then "x"^(str n) else "x"^(str n)^"()") rightargs |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
322 |
val right = (indexed "C" c)^" "^(string_of_tuple xs) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
323 |
val message = "(\"unresolved lazy call: " ^ string_of_int c ^ "\")" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
324 |
val right = if strict_args < the (arity_of c) then "raise AM_SML.Run "^message else right |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
325 |
in |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
326 |
(indexed "c" c)^(if gnum > 0 then "_"^(str gnum) else "")^leftargs^" = "^right |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
327 |
end |
23663 | 328 |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
329 |
fun eval_rules c = |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
330 |
let |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
331 |
val arity = the (arity_of c) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
332 |
val strict_arity = (case toplevel_arity_of c of NONE => arity | SOME sa => sa) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
333 |
fun eval_rule n = |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
334 |
let |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
335 |
val sc = string_of_int c |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
336 |
val left = fold (fn i => fn s => "AbstractMachine.App ("^s^(indexed ", x" i)^")") (section n) ("AbstractMachine.Const "^sc) |
23663 | 337 |
fun arg i = |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
338 |
let |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
339 |
val x = indexed "x" i |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
340 |
val x = if i < n then "(eval bounds "^x^")" else x |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
341 |
val x = if i < strict_arity then x else "(fn () => "^x^")" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
342 |
in |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
343 |
x |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
344 |
end |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
345 |
val right = "c"^sc^" "^(string_of_args (map arg (section arity))) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
346 |
val right = fold_rev (fn i => fn s => "Abs (fn "^(indexed "x" i)^" => "^s^")") (List.drop (section arity, n)) right |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
347 |
val right = if arity > 0 then right else "C"^sc |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
348 |
in |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
349 |
" | eval bounds ("^left^") = "^right |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
350 |
end |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
351 |
in |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
352 |
map eval_rule (rev (section (arity + 1))) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
353 |
end |
25217 | 354 |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
355 |
fun convert_computed_rules (c: int) : string list = |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
356 |
let |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
357 |
val arity = the (arity_of c) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
358 |
fun eval_rule () = |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
359 |
let |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
360 |
val sc = string_of_int c |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
361 |
val left = fold (fn i => fn s => "AbstractMachine.App ("^s^(indexed ", x" i)^")") (section arity) ("AbstractMachine.Const "^sc) |
25217 | 362 |
fun arg i = "(convert_computed "^(indexed "x" i)^")" |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
363 |
val right = "C"^sc^" "^(string_of_tuple (map arg (section arity))) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
364 |
val right = if arity > 0 then right else "C"^sc |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
365 |
in |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
366 |
" | convert_computed ("^left^") = "^right |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
367 |
end |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
368 |
in |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
369 |
[eval_rule ()] |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
370 |
end |
23663 | 371 |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
372 |
fun mk_constr_type_args n = if n > 0 then " of Term "^(rep_str " * Term" (n-1)) else "" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
373 |
val _ = writelist [ |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
374 |
"structure "^name^" = struct", |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
375 |
"", |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
376 |
"datatype Term = Const of int | App of Term * Term | Abs of (Term -> Term)", |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
377 |
" "^(implode (map (fn c => " | C"^(str c)^(mk_constr_type_args (the (arity_of c)))) constants)), |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
378 |
""] |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
379 |
fun make_constr c argprefix = "(C"^(str c)^" "^(string_of_tuple (map (fn i => argprefix^(str i)) (section (the (arity_of c)))))^")" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
380 |
fun make_term_eq c = " | term_eq "^(make_constr c "a")^" "^(make_constr c "b")^" = "^ |
23663 | 381 |
(case the (arity_of c) of |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
382 |
0 => "true" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
383 |
| n => |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
384 |
let |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
385 |
val eqs = map (fn i => "term_eq a"^(str i)^" b"^(str i)) (section n) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
386 |
val (eq, eqs) = (List.hd eqs, map (fn s => " andalso "^s) (List.tl eqs)) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
387 |
in |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
388 |
eq^(implode eqs) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
389 |
end) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
390 |
val _ = writelist [ |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
391 |
"fun term_eq (Const c1) (Const c2) = (c1 = c2)", |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
392 |
" | term_eq (App (a1,a2)) (App (b1,b2)) = term_eq a1 b1 andalso term_eq a2 b2"] |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
393 |
val _ = writelist (map make_term_eq constants) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
394 |
val _ = writelist [ |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
395 |
" | term_eq _ _ = false", |
23663 | 396 |
"" |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
397 |
] |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
398 |
val _ = writelist [ |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
399 |
"fun app (Abs a) b = a b", |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
400 |
" | app a b = App (a, b)", |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
401 |
""] |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
402 |
fun defcase gnum c = (case arity_of c of NONE => [] | SOME a => if a > 0 then [default_case gnum c] else []) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
403 |
fun writefundecl [] = () |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
404 |
| writefundecl (x::xs) = writelist ((("and "^x)::(map (fn s => " | "^s) xs))) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
405 |
fun list_group c = (case Inttab.lookup rules c of |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
406 |
NONE => [defcase 0 c] |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
407 |
| SOME rs => |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
408 |
let |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
409 |
val rs = |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
410 |
fold |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
411 |
(fn r => |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
412 |
fn rs => |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
413 |
let |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
414 |
val (gnum, l, rs) = |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
415 |
(case rs of |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
416 |
[] => (0, [], []) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
417 |
| (gnum, l)::rs => (gnum, l, rs)) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
418 |
val (gnum', r) = print_rule gnum arity_of toplevel_arity_of r |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
419 |
in |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
420 |
if gnum' = gnum then |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
421 |
(gnum, r::l)::rs |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
422 |
else |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
423 |
let |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
424 |
val args = implode (map (fn i => " a"^(str i)) (section (the (arity_of c)))) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
425 |
fun gnumc g = if g > 0 then "c"^(str c)^"_"^(str g)^args else "c"^(str c)^args |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
426 |
val s = gnumc (gnum) ^ " = " ^ gnumc (gnum') |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
427 |
in |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
428 |
(gnum', [])::(gnum, s::r::l)::rs |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
429 |
end |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
430 |
end) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
431 |
rs [] |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
432 |
val rs = (case rs of [] => [(0,defcase 0 c)] | (gnum,l)::rs => (gnum, (defcase gnum c)@l)::rs) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
433 |
in |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
434 |
rev (map (fn z => rev (snd z)) rs) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
435 |
end) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
436 |
val _ = map (fn z => (map writefundecl z; writeln "")) (map list_group constants) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
437 |
val _ = writelist [ |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
438 |
"fun convert (Const i) = AM_SML.Const i", |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
439 |
" | convert (App (a, b)) = AM_SML.App (convert a, convert b)", |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
440 |
" | convert (Abs _) = raise AM_SML.Run \"no abstraction in result allowed\""] |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
441 |
fun make_convert c = |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
442 |
let |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
443 |
val args = map (indexed "a") (section (the (arity_of c))) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
444 |
val leftargs = |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
445 |
case args of |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
446 |
[] => "" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
447 |
| (x::xs) => "("^x^(implode (map (fn s => ", "^s) xs))^")" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
448 |
val args = map (indexed "convert a") (section (the (arity_of c))) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
449 |
val right = fold (fn x => fn s => "AM_SML.App ("^s^", "^x^")") args ("AM_SML.Const "^(str c)) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
450 |
in |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
451 |
" | convert (C"^(str c)^" "^leftargs^") = "^right |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
452 |
end |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
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\""] |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
463 |
val _ = writelist [ |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
464 |
"", |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
465 |
"fun eval bounds (AbstractMachine.Abs m) = Abs (fn b => eval (b::bounds) m)", |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
466 |
" | eval bounds (AbstractMachine.Var i) = AM_SML.list_nth (bounds, i)"] |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
467 |
val _ = map (writelist o eval_rules) constants |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
468 |
val _ = writelist [ |
23663 | 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"] |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
472 |
val _ = writelist [ |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
473 |
"", |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
474 |
"fun export term = AM_SML.save_result (\""^code^"\", convert term)", |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
475 |
"", |
24654 | 476 |
"val _ = AM_SML.set_compiled_rewriter (fn t => (convert (eval [] t)))", |
23663 | 477 |
"", |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
478 |
"end"] |
23663 | 479 |
in |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
480 |
(arity, toplevel_arity, inlinetab, !buffer) |
23663 | 481 |
end |
482 |
||
32740 | 483 |
val guid_counter = Unsynchronized.ref 0 |
23663 | 484 |
fun get_guid () = |
485 |
let |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
486 |
val c = !guid_counter |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
487 |
val _ = guid_counter := !guid_counter + 1 |
23663 | 488 |
in |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
489 |
(LargeInt.toString (Time.toMicroseconds (Time.now ()))) ^ (string_of_int c) |
23663 | 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 |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
499 |
val guid = get_guid () |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
500 |
val code = Real.toString (random ()) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
501 |
val module = "AMSML_"^guid |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
502 |
val (arity, toplevel_arity, inlinetab, source) = sml_prog module code eqs |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
503 |
val _ = case !dump_output of NONE => () | SOME p => writeTextFile p source |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
504 |
val _ = compiled_rewriter := NONE |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
505 |
val _ = use_source source |
23663 | 506 |
in |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
507 |
case !compiled_rewriter of |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
508 |
NONE => raise Compile "broken link to compiled function" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
509 |
| SOME f => (module, code, arity, toplevel_arity, inlinetab, f) |
23663 | 510 |
end |
511 |
||
512 |
||
513 |
fun run' (module, code, arity, toplevel_arity, inlinetab, compiled_fun) t = |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
514 |
let |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
515 |
val _ = if check_freevars 0 t then () else raise Run ("can only compute closed terms") |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
516 |
fun inline (Const c) = (case Inttab.lookup inlinetab c of NONE => Const c | SOME t => t) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
517 |
| inline (Var i) = Var i |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
518 |
| inline (App (a, b)) = App (inline a, inline b) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
519 |
| inline (Abs m) = Abs (inline m) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
520 |
val t = beta (inline t) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
521 |
fun arity_of c = Inttab.lookup arity c |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
522 |
fun toplevel_arity_of c = Inttab.lookup toplevel_arity c |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
523 |
val term = print_term NONE arity_of toplevel_arity_of 0 0 t |
23663 | 524 |
val source = "local open "^module^" in val _ = export ("^term^") end" |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
525 |
val _ = writeTextFile "Gencode_call.ML" source |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
526 |
val _ = clear_result () |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
527 |
val _ = use_source source |
23663 | 528 |
in |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
529 |
case !saved_result of |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
530 |
NONE => raise Run "broken link to compiled code" |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
531 |
| SOME (code', t) => (clear_result (); if code' = code then t else raise Run "link to compiled code was hijacked") |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
532 |
end |
23663 | 533 |
|
534 |
fun run (module, code, arity, toplevel_arity, inlinetab, compiled_fun) t = |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
535 |
let |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
536 |
val _ = if check_freevars 0 t then () else raise Run ("can only compute closed terms") |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
537 |
fun inline (Const c) = (case Inttab.lookup inlinetab c of NONE => Const c | SOME t => t) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
538 |
| inline (Var i) = Var i |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
539 |
| inline (App (a, b)) = App (inline a, inline b) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
540 |
| inline (Abs m) = Abs (inline m) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
541 |
| inline (Computed t) = Computed t |
23663 | 542 |
in |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
543 |
compiled_fun (beta (inline t)) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
544 |
end |
23663 | 545 |
|
546 |
fun discard p = () |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32952
diff
changeset
|
547 |
|
23663 | 548 |
end |