Annotation of /sml/branches/SMLNJ/src/smlnj-lib/Reactive/machine.sml

Parent Directory | Revision Log

---

Revision 2 - (view) (download)
Original Path: sml/trunk/src/smlnj-lib/Reactive/machine.sml

1 :	monnier	2	(* machine.sml
2 :			*
3 :			* COPYRIGHT (c) 1997 Bell Labs, Lucent Technologies.
4 :			*
5 :			* This is an implementation of the reactive interpreter instructions,
6 :			* and functions to generate them.
7 :			*)
8 :
9 :			structure Machine : sig
10 :
11 :			(* activation return codes *)
12 :			datatype state
13 :			= TERM (* execution of the instruction is complete; activation
14 :			* at future instances has no effect.
15 :			*)
16 :			| STOP (* execution is stopped in this instant, but could
17 :			* progress in the next instant.
18 :			*)
19 :			| SUSP (* exeuction is suspended and must be resumed during this
20 :			* instant.
21 :			*)
22 :
23 :			type in_signal
24 :			type out_signal
25 :
26 :			type instant = int
27 :			type signal_state = instant ref
28 :
29 :			datatype signal = SIG of {
30 :			name : Atom.atom,
31 :			id : int,
32 :			state : signal_state
33 :			}
34 :
35 :			datatype machine = M of {
36 :			now : instant ref,
37 :			moveFlg : bool ref,
38 :			endOfInstant : bool ref,
39 :			prog : code,
40 :			signals : signal list,
41 :			inputs : signal list,
42 :			outputs : signal list
43 :			}
44 :
45 :			and code = C of {
46 :			isTerm : unit -> bool,
47 :			terminate : unit -> unit,
48 :			reset : unit -> unit,
49 :			preempt : machine -> unit,
50 :			activation : machine -> state
51 :			}
52 :
53 :			val runMachine : machine -> bool
54 :			val resetMachine : machine -> unit
55 :			val inputsOf : machine -> in_signal list
56 :			val outputsOf : machine -> out_signal list
57 :
58 :			val inputSignal : in_signal -> Atom.atom
59 :			val outputSignal : out_signal -> Atom.atom
60 :			val setInSignal : (in_signal * bool) -> unit
61 :			val getInSignal : in_signal -> bool
62 :			val getOutSignal : out_signal -> bool
63 :
64 :			type config
65 :
66 :			val || : (code * code) -> code
67 :			val & : (code * code) -> code
68 :			val nothing : code
69 :			val stop : unit -> code
70 :			val suspend : unit -> code
71 :			val action : (machine -> unit) -> code
72 :			val exec : {
73 :			start : machine -> unit,
74 :			stop : machine -> unit,
75 :			done : machine -> bool
76 :			} -> code
77 :			val ifThenElse : ((machine -> bool) * code * code) -> code
78 :			val repeat : (int * code) -> code
79 :			val loop : code -> code
80 :			val close : code -> code
81 :			val emit : signal -> code
82 :			val await : config -> code
83 :			val when : (config * code * code) -> code
84 :			val trapWith : (config * code * code) -> code
85 :
86 :			end = struct
87 :
88 :			structure I = Instruction (* for the config type *)
89 :
90 :			datatype state
91 :			= TERM
92 :			| STOP
93 :			| SUSP
94 :
95 :			type instant = int
96 :			type signal_state = instant ref
97 :
98 :			datatype signal = SIG of {
99 :			name : Atom.atom,
100 :			id : int,
101 :			state : signal_state
102 :			}
103 :
104 :			type config = signal I.config
105 :
106 :			datatype machine = M of {
107 :			now : instant ref,
108 :			moveFlg : bool ref,
109 :			endOfInstant : bool ref,
110 :			prog : code,
111 :			signals : signal list,
112 :			inputs : signal list,
113 :			outputs : signal list
114 :			}
115 :
116 :			and code = C of {
117 :			isTerm : unit -> bool,
118 :			terminate : unit -> unit,
119 :			reset : unit -> unit,
120 :			preempt : machine -> unit,
121 :			activation : machine -> state
122 :			}
123 :
124 :
125 :			fun now (M{now=t, ...}) = !t
126 :			fun newMove (M{moveFlg, ...}) = moveFlg := true
127 :			fun isEndOfInstant (M{endOfInstant, ...}) = !endOfInstant
128 :
129 :			datatype presence = PRESENT | ABSENT | UNKNOWN
130 :
131 :			fun presence (m, SIG{state, ...}) = let
132 :			val ts = !state
133 :			val now = now m
134 :			in
135 :			if (now = ts) then PRESENT
136 :			else if ((now = ~ts) orelse (isEndOfInstant m)) then ABSENT
137 :			else UNKNOWN
138 :			end
139 :
140 :			fun present (m, SIG{state, ...}) = (now m = !state)
141 :			fun absent (m, SIG{state, ...}) = (now m = ~(!state))
142 :			fun emitSig (m, SIG{state, ...}) = state := now m
143 :			fun emitNot (m, SIG{state, ...}) = state := ~(now m)
144 :
145 :			datatype in_signal = IN of (machine * signal)
146 :			datatype out_signal = OUT of (machine * signal)
147 :
148 :			fun inputSignal (IN(_, SIG{name, ...})) = name
149 :			fun outputSignal (OUT(_, SIG{name, ...})) = name
150 :			fun setInSignal (IN(m, s), false) = emitNot(m, s)
151 :			| setInSignal (IN(m, s), true) = emitSig(m, s)
152 :			fun getInSignal (IN(m, s)) = present(m, s)
153 :			fun getOutSignal (OUT(m, s)) = present(m, s)
154 :
155 :			fun terminate (C{terminate=f, ...}) = f()
156 :			fun isTerm (C{isTerm=f, ...}) = f()
157 :			fun reset (C{reset=f, ...}) = f()
158 :			fun preemption (C{preempt=f, ...}, m) = f m
159 :			fun activation (C{activation=f, ...}, m) = f m
160 :
161 :			fun activate (i, m) = if (isTerm i)
162 :			then TERM
163 :			else (case activation(i, m)
164 :			of TERM => (terminate i; TERM)
165 :			| res => res
166 :			(* end case *))
167 :
168 :			fun preempt (i, m) = if (isTerm i)
169 :			then ()
170 :			else (preemption(i, m); terminate i)
171 :
172 :			(* default instruction methods *)
173 :			fun isTermMeth termFlg () = !termFlg
174 :			fun terminateMeth termFlg () = termFlg := true
175 :			fun resetMeth termFlg () = termFlg := false
176 :
177 :			fun || (i1, i2) = let
178 :			val termFlg = ref false
179 :			val leftSts = ref SUSP
180 :			val rightSts = ref SUSP
181 :			fun resetMeth () = (
182 :			termFlg := false; leftSts := SUSP; rightSts := SUSP;
183 :			reset i1; reset i2)
184 :			fun preemptMeth m = (preempt(i1, m); preempt(i2, m))
185 :			fun activationMeth m = (
186 :			if (!leftSts = SUSP) then leftSts := activate(i1, m) else ();
187 :			if (!rightSts = SUSP) then rightSts := activate(i2, m) else ();
188 :			case (!leftSts, !rightSts)
189 :			of (TERM, TERM) => TERM
190 :			| (SUSP, _) => SUSP
191 :			| (_, SUSP) => SUSP
192 :			| _ => (leftSts := SUSP; rightSts := SUSP; STOP)
193 :			(* end case *))
194 :			in
195 :			C{ isTerm = isTermMeth termFlg,
196 :			terminate = terminateMeth termFlg,
197 :			reset = resetMeth,
198 :			preempt = preemptMeth,
199 :			activation = activationMeth
200 :			}
201 :			end
202 :
203 :			fun & (i1, i2) = let
204 :			val termFlg = ref false
205 :			fun resetMeth () = (termFlg := false; reset i1; reset i2)
206 :			fun preemptMeth m = (preempt(i1, m); preempt(i2, m))
207 :			fun activationMeth m =
208 :			if (isTerm i1)
209 :			then activate(i2, m)
210 :			else (case activate(i1, m)
211 :			of TERM => activate(i2, m)
212 :			| res => res
213 :			(* end case *))
214 :			in
215 :			C{ isTerm = isTermMeth termFlg,
216 :			terminate = terminateMeth termFlg,
217 :			reset = resetMeth,
218 :			preempt = preemptMeth,
219 :			activation = activationMeth
220 :			}
221 :			end
222 :
223 :			val nothing = C{
224 :			isTerm = fn () => true,
225 :			terminate = fn () => (),
226 :			reset = fn () => (),
227 :			preempt = fn _ => (),
228 :			activation = fn _ => TERM
229 :			}
230 :
231 :			fun stop () = let
232 :			val termFlg = ref false
233 :			in
234 :			C{ isTerm = isTermMeth termFlg,
235 :			terminate = terminateMeth termFlg,
236 :			reset = resetMeth termFlg,
237 :			preempt = fn _ => (),
238 :			activation = fn _ => STOP
239 :			}
240 :			end
241 :
242 :			fun suspend () = let
243 :			val termFlg = ref false
244 :			in
245 :			C{ isTerm = isTermMeth termFlg,
246 :			terminate = terminateMeth termFlg,
247 :			reset = resetMeth termFlg,
248 :			preempt = fn _ => (),
249 :			activation = fn _ => (termFlg := true; STOP)
250 :			}
251 :			end
252 :
253 :			fun action f = let
254 :			val termFlg = ref false
255 :			in
256 :			C{ isTerm = isTermMeth termFlg,
257 :			terminate = terminateMeth termFlg,
258 :			reset = resetMeth termFlg,
259 :			preempt = fn _ => (),
260 :			activation = fn m => (f m; TERM)
261 :			}
262 :			end
263 :
264 :			fun exec {start, stop, done} = let
265 :			val termFlg = ref false
266 :			val running = ref false
267 :			(** NOTE: what if a reset occurs while we are running? We would need to change
268 :			** the type of resetMeth to take a machine parameter.
269 :			**)
270 :			fun resetMeth () = (termFlg := false)
271 :			fun preemptMeth m = if !running then (running := false; stop m) else ()
272 :			fun activationMeth m = if !running
273 :			then if done m
274 :			then (running := false; TERM)
275 :			else STOP
276 :			else (running := true; start m; SUSP)
277 :			in
278 :			C{ isTerm = isTermMeth termFlg,
279 :			terminate = terminateMeth termFlg,
280 :			reset = resetMeth,
281 :			preempt = preemptMeth,
282 :			activation = activationMeth
283 :			}
284 :			end
285 :
286 :			fun ifThenElse (pred, i1, i2) = let
287 :			val termFlg = ref false
288 :			val cond = ref NONE
289 :			fun resetMeth () = (
290 :			termFlg := false;
291 :			case !cond
292 :			of (SOME true) => reset i1
293 :			| (SOME false) => reset i2
294 :			| NONE => ()
295 :			(* end case *);
296 :			cond := NONE)
297 :			fun preemptMeth m = (case !cond
298 :			of (SOME true) => preempt(i1, m)
299 :			| (SOME false) => preempt(i2, m)
300 :			| NONE => ()
301 :			(* end case *))
302 :			fun activationMeth m = (case !cond
303 :			of (SOME true) => activate(i1, m)
304 :			| (SOME false) => activate(i2, m)
305 :			| NONE => let
306 :			val b = pred m
307 :			in
308 :			cond := SOME b;
309 :			if b then activate(i1, m) else activate(i2, m)
310 :			end
311 :			(* end case *))
312 :			in
313 :			C{ isTerm = isTermMeth termFlg,
314 :			terminate = terminateMeth termFlg,
315 :			reset = resetMeth,
316 :			preempt = preemptMeth,
317 :			activation = activationMeth
318 :			}
319 :			end
320 :
321 :			fun repeat (n, i) = let
322 :			val termFlg = ref false
323 :			val counter = ref n
324 :			fun resetMeth () = (termFlg := false; counter := n)
325 :			fun preemptMeth m = preempt(i, m)
326 :			fun activationMeth m =
327 :			if (!counter > 0)
328 :			then (case activate(i, m)
329 :			of TERM => (counter := !counter-1; reset i; TERM)
330 :			| res => res
331 :			(* end case *))
332 :			else TERM
333 :			in
334 :			C{ isTerm = isTermMeth termFlg,
335 :			terminate = terminateMeth termFlg,
336 :			reset = resetMeth,
337 :			preempt = preemptMeth,
338 :			activation = activationMeth
339 :			}
340 :			end
341 :
342 :			fun loop i = let
343 :			val termFlg = ref false
344 :			val endReached = ref false
345 :			fun resetMeth () = (termFlg := false; endReached := false)
346 :			fun preemptMeth m = preempt (i, m)
347 :			fun activationMeth m = (case activate(i, m)
348 :			of TERM => if (!endReached)
349 :			then (
350 :			(* say(m, "instantaneous loop detected\n"); *)
351 :			STOP)
352 :			else (endReached := true; reset i; TERM)
353 :			| STOP => (endReached := false; STOP)
354 :			| SUSP => SUSP
355 :			(* end case *))
356 :			in
357 :			C{ isTerm = isTermMeth termFlg,
358 :			terminate = terminateMeth termFlg,
359 :			reset = resetMeth,
360 :			preempt = preemptMeth,
361 :			activation = activationMeth
362 :			}
363 :			end
364 :
365 :			fun close i = let
366 :			val termFlg = ref false
367 :			fun activationMeth m = (case activate(i, m)
368 :			of SUSP => activationMeth m
369 :			| res => res
370 :			(* end case *))
371 :			in
372 :			C{ isTerm = isTermMeth termFlg,
373 :			terminate = terminateMeth termFlg,
374 :			reset = resetMeth termFlg,
375 :			preempt = fn _ => (),
376 :			activation = activationMeth
377 :			}
378 :			end
379 :
380 :			(** Configuration evaluation **)
381 :			fun fixed (m, c) = let
382 :			fun fix (I.posConfig id) = (presence(m, id) <> UNKNOWN)
383 :			| fix (I.negConfig id) = (presence(m, id) <> UNKNOWN)
384 :			| fix (I.orConfig(c1, c2)) = let
385 :			val b1 = fix c1 and b2 = fix c2
386 :			in
387 :			(b1 andalso evaluate(m, c1)) orelse
388 :			(b2 andalso evaluate(m, c2)) orelse
389 :			(b1 andalso b2)
390 :			end
391 :			| fix (I.andConfig(c1, c2)) = let
392 :			val b1 = fix c1 and b2 = fix c2
393 :			in
394 :			(b1 andalso not(evaluate(m, c1))) orelse
395 :			(b2 andalso not(evaluate(m, c2))) orelse
396 :			(b1 andalso b2)
397 :			end
398 :			in
399 :			fix c
400 :			end
401 :
402 :			and evaluate (m, c) = let
403 :			fun eval (I.posConfig id) = present(m, id)
404 :			| eval (I.negConfig id) = not(present(m, id))
405 :			| eval (I.orConfig(c1, c2)) = eval c1 orelse eval c2
406 :			| eval (I.andConfig(c1, c2)) = eval c1 andalso eval c2
407 :			in
408 :			eval c
409 :			end
410 :
411 :			fun fixedEval (m, c) = let
412 :			fun f (I.posConfig id) = (case presence(m, id)
413 :			of UNKNOWN => NONE
414 :			| PRESENT => SOME true
415 :			| ABSENT => SOME false
416 :			(* end case *))
417 :			| f (I.negConfig id) = (case presence(m, id)
418 :			of UNKNOWN => NONE
419 :			| PRESENT => SOME false
420 :			| ABSENT => SOME true
421 :			(* end case *))
422 :			| f (I.andConfig(c1, c2)) = (case (f c1, f c2)
423 :			of (SOME false, _) => SOME false
424 :			| (_, SOME false) => SOME false
425 :			| (SOME true, SOME true) => SOME true
426 :			| _ => NONE
427 :			(* end case *))
428 :			| f (I.orConfig(c1, c2)) = (case (f c1, f c2)
429 :			of (SOME true, _) => SOME true
430 :			| (_, SOME true) => SOME true
431 :			| (SOME false, SOME false) => SOME false
432 :			| _ => NONE
433 :			(* end case *))
434 :			in
435 :			f c
436 :			end
437 :
438 :			fun emit signal = let
439 :			val termFlg = ref false
440 :			fun activationMeth m = (
441 :			newMove m;
442 :			emitSig(m, signal);
443 :			TERM)
444 :			in
445 :			C{ isTerm = isTermMeth termFlg,
446 :			terminate = terminateMeth termFlg,
447 :			reset = resetMeth termFlg,
448 :			preempt = fn _ => (),
449 :			activation = activationMeth
450 :			}
451 :			end
452 :
453 :			fun await c = let
454 :			val termFlg = ref false
455 :			fun activationMeth m = (case fixedEval(m, c)
456 :			of NONE => SUSP
457 :			| (SOME true) => STOP
458 :			| (SOME false) => (
459 :			termFlg := true;
460 :			if (isEndOfInstant m) then STOP else TERM)
461 :			(* end case *))
462 :			in
463 :			C{ isTerm = isTermMeth termFlg,
464 :			terminate = terminateMeth termFlg,
465 :			reset = resetMeth termFlg,
466 :			preempt = fn _ => (),
467 :			activation = activationMeth
468 :			}
469 :			end
470 :
471 :			fun when (c, i1, i2) = let
472 :			val termFlg = ref false
473 :			val value = ref NONE
474 :			fun resetMeth m = (
475 :			termFlg := false;
476 :			reset i1; reset i2;
477 :			value := NONE)
478 :			fun preemptMeth m = (preempt(i1, m); preempt(i2, m))
479 :			fun activationMeth m = (case !value
480 :			of NONE => (case fixedEval(m, c)
481 :			of NONE => SUSP
482 :			| (SOME v) => (
483 :			value := SOME v;
484 :			if (isEndOfInstant m)
485 :			then STOP
486 :			else if v
487 :			then activate(i1, m)
488 :			else activate(i2, m))
489 :			(* end case *))
490 :			| (SOME true) => activate(i1, m)
491 :			| (SOME false) => activate(i2, m)
492 :			(* end case *))
493 :			in
494 :			C{ isTerm = isTermMeth termFlg,
495 :			terminate = terminateMeth termFlg,
496 :			reset = resetMeth,
497 :			preempt = preemptMeth,
498 :			activation = activationMeth
499 :			}
500 :			end
501 :
502 :			fun trapWith (c, i1, i2) = let
503 :			val termFlg = ref false
504 :			val activeHandle = ref false
505 :			val resumeBody = ref true
506 :			fun resetMeth m = (
507 :			termFlg := false;
508 :			reset i1; reset i2;
509 :			activeHandle := false;
510 :			resumeBody := true)
511 :			fun preemptMeth m = if (! activeHandle)
512 :			then preempt(i2, m)
513 :			else preempt(i1, m)
514 :			fun activationMeth m =
515 :			if (! activeHandle)
516 :			then activate(i2, m)
517 :			else let
518 :			fun chkConfig () = (case fixedEval(m, c)
519 :			of NONE => SUSP
520 :			| (SOME true) => ( (* actual preemption *)
521 :			preempt(i1, m);
522 :			activeHandle := true;
523 :			if (isEndOfInstant m)
524 :			then STOP
525 :			else activate(i2, m))
526 :			| (SOME false) => (
527 :			resumeBody := true;
528 :			STOP)
529 :			(* end case *))
530 :			in
531 :			if (! resumeBody)
532 :			then (case activate(i1, m)
533 :			of STOP => (resumeBody := false; chkConfig())
534 :			| res => res
535 :			(* end case *))
536 :			else chkConfig()
537 :			end
538 :			in
539 :			C{ isTerm = isTermMeth termFlg,
540 :			terminate = terminateMeth termFlg,
541 :			reset = resetMeth,
542 :			preempt = preemptMeth,
543 :			activation = activationMeth
544 :			}
545 :			end
546 :
547 :			(* run a machine to a stable state; return true if that is a terminal state *)
548 :			fun runMachine (m as M{now, moveFlg, endOfInstant, prog, ...}) = let
549 :			fun untilStop () = (case activate(prog, m)
550 :			of SUSP => (
551 :			if !moveFlg
552 :			then moveFlg := false
553 :			else endOfInstant := true;
554 :			untilStop ())
555 :			| STOP => false
556 :			| TERM => true
557 :			(* end case *))
558 :			in
559 :			endOfInstant := false;
560 :			moveFlg := false;
561 :			untilStop () before now := !now+1
562 :			end
563 :
564 :			(* reset a machine back to its initial state *)
565 :			fun resetMachine (M{
566 :			now, moveFlg, endOfInstant, prog, signals, inputs, outputs
567 :			}) = let
568 :			fun resetSig (SIG{state, ...}) = state := 0
569 :			in
570 :			now := 1;
571 :			moveFlg := false;
572 :			endOfInstant := false;
573 :			reset prog;
574 :			List.app resetSig signals;
575 :			List.app resetSig inputs;
576 :			List.app resetSig outputs
577 :			end
578 :
579 :			fun inputsOf (m as M{inputs, ...}) = List.map (fn s => IN(m, s)) inputs
580 :			fun outputsOf (m as M{inputs, ...}) = List.map (fn s => OUT(m, s)) inputs
581 :
582 :			end;

---

root@smlnj-gforge.cs.uchicago.edu	ViewVC Help
Powered by ViewVC 1.0.0