Home My Page Projects Code Snippets Project Openings SML/NJ
Summary Activity Forums Tracker Lists Tasks Docs Surveys News SCM Files

SCM Repository

[smlnj] Annotation of /sml/trunk/src/smlnj-lib/Reactive/machine.sml
ViewVC logotype

Annotation of /sml/trunk/src/smlnj-lib/Reactive/machine.sml

Parent Directory Parent Directory | Revision Log Revision Log


Revision 651 - (view) (download)

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 : monnier 8 val exec : (machine -> {stop : unit -> unit, done : unit -> bool}) -> code
73 : monnier 2 val ifThenElse : ((machine -> bool) * code * code) -> code
74 :     val repeat : (int * code) -> code
75 :     val loop : code -> code
76 :     val close : code -> code
77 :     val emit : signal -> code
78 :     val await : config -> code
79 :     val when : (config * code * code) -> code
80 :     val trapWith : (config * code * code) -> code
81 :    
82 :     end = struct
83 :    
84 :     structure I = Instruction (* for the config type *)
85 :    
86 :     datatype state
87 :     = TERM
88 :     | STOP
89 :     | SUSP
90 :    
91 :     type instant = int
92 :     type signal_state = instant ref
93 :    
94 :     datatype signal = SIG of {
95 :     name : Atom.atom,
96 :     id : int,
97 :     state : signal_state
98 :     }
99 :    
100 :     type config = signal I.config
101 :    
102 :     datatype machine = M of {
103 :     now : instant ref,
104 :     moveFlg : bool ref,
105 :     endOfInstant : bool ref,
106 :     prog : code,
107 :     signals : signal list,
108 :     inputs : signal list,
109 :     outputs : signal list
110 :     }
111 :    
112 :     and code = C of {
113 :     isTerm : unit -> bool,
114 :     terminate : unit -> unit,
115 :     reset : unit -> unit,
116 :     preempt : machine -> unit,
117 :     activation : machine -> state
118 :     }
119 :    
120 :    
121 :     fun now (M{now=t, ...}) = !t
122 :     fun newMove (M{moveFlg, ...}) = moveFlg := true
123 :     fun isEndOfInstant (M{endOfInstant, ...}) = !endOfInstant
124 :    
125 :     datatype presence = PRESENT | ABSENT | UNKNOWN
126 :    
127 :     fun presence (m, SIG{state, ...}) = let
128 :     val ts = !state
129 :     val now = now m
130 :     in
131 :     if (now = ts) then PRESENT
132 :     else if ((now = ~ts) orelse (isEndOfInstant m)) then ABSENT
133 :     else UNKNOWN
134 :     end
135 :    
136 :     fun present (m, SIG{state, ...}) = (now m = !state)
137 :     fun absent (m, SIG{state, ...}) = (now m = ~(!state))
138 :     fun emitSig (m, SIG{state, ...}) = state := now m
139 :     fun emitNot (m, SIG{state, ...}) = state := ~(now m)
140 :    
141 :     datatype in_signal = IN of (machine * signal)
142 :     datatype out_signal = OUT of (machine * signal)
143 :    
144 :     fun inputSignal (IN(_, SIG{name, ...})) = name
145 :     fun outputSignal (OUT(_, SIG{name, ...})) = name
146 :     fun setInSignal (IN(m, s), false) = emitNot(m, s)
147 :     | setInSignal (IN(m, s), true) = emitSig(m, s)
148 :     fun getInSignal (IN(m, s)) = present(m, s)
149 :     fun getOutSignal (OUT(m, s)) = present(m, s)
150 :    
151 :     fun terminate (C{terminate=f, ...}) = f()
152 :     fun isTerm (C{isTerm=f, ...}) = f()
153 :     fun reset (C{reset=f, ...}) = f()
154 :     fun preemption (C{preempt=f, ...}, m) = f m
155 :     fun activation (C{activation=f, ...}, m) = f m
156 :    
157 :     fun activate (i, m) = if (isTerm i)
158 :     then TERM
159 :     else (case activation(i, m)
160 :     of TERM => (terminate i; TERM)
161 :     | res => res
162 :     (* end case *))
163 :    
164 :     fun preempt (i, m) = if (isTerm i)
165 :     then ()
166 :     else (preemption(i, m); terminate i)
167 :    
168 :     (* default instruction methods *)
169 :     fun isTermMeth termFlg () = !termFlg
170 :     fun terminateMeth termFlg () = termFlg := true
171 :     fun resetMeth termFlg () = termFlg := false
172 :    
173 :     fun || (i1, i2) = let
174 :     val termFlg = ref false
175 :     val leftSts = ref SUSP
176 :     val rightSts = ref SUSP
177 :     fun resetMeth () = (
178 :     termFlg := false; leftSts := SUSP; rightSts := SUSP;
179 :     reset i1; reset i2)
180 :     fun preemptMeth m = (preempt(i1, m); preempt(i2, m))
181 :     fun activationMeth m = (
182 :     if (!leftSts = SUSP) then leftSts := activate(i1, m) else ();
183 :     if (!rightSts = SUSP) then rightSts := activate(i2, m) else ();
184 :     case (!leftSts, !rightSts)
185 :     of (TERM, TERM) => TERM
186 :     | (SUSP, _) => SUSP
187 :     | (_, SUSP) => SUSP
188 :     | _ => (leftSts := SUSP; rightSts := SUSP; STOP)
189 :     (* end case *))
190 :     in
191 :     C{ isTerm = isTermMeth termFlg,
192 :     terminate = terminateMeth termFlg,
193 :     reset = resetMeth,
194 :     preempt = preemptMeth,
195 :     activation = activationMeth
196 :     }
197 :     end
198 :    
199 :     fun & (i1, i2) = let
200 :     val termFlg = ref false
201 :     fun resetMeth () = (termFlg := false; reset i1; reset i2)
202 :     fun preemptMeth m = (preempt(i1, m); preempt(i2, m))
203 :     fun activationMeth m =
204 :     if (isTerm i1)
205 :     then activate(i2, m)
206 :     else (case activate(i1, m)
207 :     of TERM => activate(i2, m)
208 :     | res => res
209 :     (* end case *))
210 :     in
211 :     C{ isTerm = isTermMeth termFlg,
212 :     terminate = terminateMeth termFlg,
213 :     reset = resetMeth,
214 :     preempt = preemptMeth,
215 :     activation = activationMeth
216 :     }
217 :     end
218 :    
219 :     val nothing = C{
220 :     isTerm = fn () => true,
221 :     terminate = fn () => (),
222 :     reset = fn () => (),
223 :     preempt = fn _ => (),
224 :     activation = fn _ => TERM
225 :     }
226 :    
227 :     fun stop () = let
228 :     val termFlg = ref false
229 :     in
230 :     C{ isTerm = isTermMeth termFlg,
231 :     terminate = terminateMeth termFlg,
232 :     reset = resetMeth termFlg,
233 :     preempt = fn _ => (),
234 :     activation = fn _ => STOP
235 :     }
236 :     end
237 :    
238 :     fun suspend () = let
239 :     val termFlg = ref false
240 :     in
241 :     C{ isTerm = isTermMeth termFlg,
242 :     terminate = terminateMeth termFlg,
243 :     reset = resetMeth termFlg,
244 :     preempt = fn _ => (),
245 :     activation = fn _ => (termFlg := true; STOP)
246 :     }
247 :     end
248 :    
249 :     fun action f = let
250 :     val termFlg = ref false
251 :     in
252 :     C{ isTerm = isTermMeth termFlg,
253 :     terminate = terminateMeth termFlg,
254 :     reset = resetMeth termFlg,
255 :     preempt = fn _ => (),
256 :     activation = fn m => (f m; TERM)
257 :     }
258 :     end
259 :    
260 : monnier 8 fun exec f = let
261 : monnier 2 val termFlg = ref false
262 : monnier 8 val ops = ref(NONE : {stop : unit -> unit, done : unit -> bool} option)
263 : monnier 2 (** NOTE: what if a reset occurs while we are running? We would need to change
264 :     ** the type of resetMeth to take a machine parameter.
265 :     **)
266 :     fun resetMeth () = (termFlg := false)
267 : monnier 8 fun preemptMeth m = (case !ops
268 :     of NONE => ()
269 :     | SOME{stop, ...} => (ops := NONE; stop())
270 :     (* end case *))
271 :     fun activationMeth m = (case !ops
272 :     of SOME{done, ...} => if done ()
273 :     then (ops := NONE; TERM)
274 :     else STOP
275 :     | NONE => (ops := SOME(f m); SUSP)
276 :     (* end case *))
277 : monnier 2 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