equal
deleted
inserted
replaced
16 val list_nth = List.nth; |
16 val list_nth = List.nth; |
17 val list_map = map; |
17 val list_map = map; |
18 |
18 |
19 open AbstractMachine; |
19 open AbstractMachine; |
20 |
20 |
21 val compiled_rewriter = ref (NONE:(term -> term)Option.option) |
21 val compiled_rewriter = Unsynchronized.ref (NONE:(term -> term)Option.option) |
22 |
22 |
23 fun set_compiled_rewriter r = (compiled_rewriter := SOME r) |
23 fun set_compiled_rewriter r = (compiled_rewriter := SOME r) |
24 |
24 |
25 type program = (term -> term) |
25 type program = (term -> term) |
26 |
26 |
79 | constants_of_term (Const c) = [c] |
79 | constants_of_term (Const c) = [c] |
80 | constants_of_term (Computed c) = constants_of_term c |
80 | constants_of_term (Computed c) = constants_of_term c |
81 |
81 |
82 fun load_rules sname name prog = |
82 fun load_rules sname name prog = |
83 let |
83 let |
84 val buffer = ref "" |
84 val buffer = Unsynchronized.ref "" |
85 fun write s = (buffer := (!buffer)^s) |
85 fun write s = (buffer := (!buffer)^s) |
86 fun writeln s = (write s; write "\n") |
86 fun writeln s = (write s; write "\n") |
87 fun writelist [] = () |
87 fun writelist [] = () |
88 | writelist (s::ss) = (writeln s; writelist ss) |
88 | writelist (s::ss) = (writeln s; writelist ss) |
89 fun str i = Int.toString i |
89 fun str i = Int.toString i |
110 "fun cont (Continue _) = true", |
110 "fun cont (Continue _) = true", |
111 " | cont _ = false", |
111 " | cont _ = false", |
112 "", |
112 "", |
113 "fun do_reduction reduce p =", |
113 "fun do_reduction reduce p =", |
114 " let", |
114 " let", |
115 " val s = ref (Continue p)", |
115 " val s = Unsynchronized.ref (Continue p)", |
116 " val _ = while cont (!s) do (s := reduce (proj_C (!s)))", |
116 " val _ = while cont (!s) do (s := reduce (proj_C (!s)))", |
117 " in", |
117 " in", |
118 " proj_S (!s)", |
118 " proj_S (!s)", |
119 " end", |
119 " end", |
120 ""] |
120 ""] |