khb/khs_exec_seq.ml


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62

open Util
open Khs_ast
open Khs_exec

let chans = Hashtbl.create 12
let ch_id =
    let p = ref 0 in
    fun () -> p := !p + 1; !p

let proc = ref []
let proc_spawned = ref []

let spawn proc pos =
    proc_spawned :=
        { proc with xpos = pos }::(!proc_spawned)

let newchan proc =
    let id = ch_id () in
    Hashtbl.add chans id (Queue.create());
    Many (Smap.add (psep^"in") (VInt id)
            (Smap.add (psep^"out") (VInt id) Smap.empty))

let proc_step proc =
    match proc.xstatus with
    | PSDone -> false
    | PSExec | PSExecRecvd _ ->
        exec_stmt proc;
        true
    | PSSend(c, kv) ->
        proc.xstatus <- PSExec;
        begin 
            if (int_of_kbval c) == 0 then
                Format.printf "%s@." (kval_descr kv)
            else
                Queue.push kv (Hashtbl.find chans (int_of_kbval c))
        end; 
        true
    | PSRecv(c) ->
        let q = Hashtbl.find chans (int_of_kbval c) in
        if not (Queue.is_empty q) then
            proc.xstatus <- PSExecRecvd (Queue.pop q);
        true

let exec_program p =
    let proc0 = {
        xspawn = spawn;
        xnewchan = newchan;
        xprog = p;
        xvals = Smap.empty;
        xstatus = PSExec;
        xpos = 0
    } in
    proc0.xvals <- Smap.add framevar (VInt 0) proc0.xvals;
    proc0.xvals <- Smap.add "stdout" (VInt 0) proc0.xvals;
    proc := [ proc0 ];
    while List.length !proc > 0 do
        proc := List.filter proc_step !proc;
        proc := !proc_spawned @ !proc;
        proc_spawned := [];
    done