| changeset 60549 | c0a775618258 |
| parent 60269 | 74965ce81297 |
| 60548:5765bd0f7055 | 60549:c0a775618258 |
|---|---|
1 (* states for calculation in global refs |
1 (* states for calculation in global refs |
2 use"../states.sml"; |
2 use"../states.sml"; |
3 use"states.sml"; |
3 use"states.sml"; |
4 *) |
4 *) |
5 |
|
6 signature STATES = |
|
7 sig |
|
8 eqtype iterID |
|
9 eqtype calcID |
|
10 val add_calc: Calc.state_pre -> calcID |
|
11 val get_calc: calcID -> Calc.state_pre |
|
12 val get_pos: calcID -> iterID -> Pos.pos' |
|
13 val del_calc: calcID -> calcID |
|
14 val add_user: calcID -> iterID |
|
15 val del_user: calcID -> iterID -> iterID |
|
16 val reset: unit -> unit |
|
17 (*val reset_states: unit -> unit*) |
|
18 val upd_calc: calcID -> Calc.state_pre -> unit |
|
19 val upd_ipos: calcID -> iterID -> Pos.pos' -> unit |
|
20 val upd_tacis: calcID -> State_Steps.T -> unit |
|
21 |
|
22 \<^isac_test>\<open> |
|
23 (** )val states: (calcID * (Calc.state_pre * (iterID * Pos.pos') list)) list Synchronized.var( **) |
|
24 |
|
25 (** )val del_assoc: (''a * 'b) list * ''a -> (''a * 'b) list( **) |
|
26 (** )val del_assoc2: calcID -> iterID -> (calcID * ('a * (iterID * 'b) list)) list -> ( |
|
27 calcID * ('a * (iterID * 'b) list)) list( **) |
|
28 (** )val get_iterID: calcID -> (calcID * (Calc.state_pre * (iterID * Pos.pos') list)) list -> iterID( **) |
|
29 (** )val new_key: (iterID * 'a) list -> iterID -> iterID( **) |
|
30 (** )val overwrite2: (calcID * ('a * (iterID * 'b) list)) list * ((calcID * iterID) * 'b) -> |
|
31 (calcID * ('a * (iterID * 'b) list)) list( **) |
|
32 \<close> |
|
33 end |
|
34 |
|
35 (**) |
|
36 structure States(**): STATES(**) = |
|
37 struct |
|
38 (**) |
|
5 |
39 |
6 type iterID = int; |
40 type iterID = int; |
7 type calcID = int; |
41 type calcID = int; |
8 |
42 |
9 (* holds calculations; these are read/updated from the java-frontend at each interaction*) |
43 (* holds calculations; these are read/updated from the java-frontend at each interaction*) |
13 (iterID * (* 1 sets the 'active formula': a calc. can have several visitors*) |
47 (iterID * (* 1 sets the 'active formula': a calc. can have several visitors*) |
14 Pos.pos' (* for iterator of a user *) |
48 Pos.pos' (* for iterator of a user *) |
15 (* TODO iterID * pos' should go to java-frontend *) |
49 (* TODO iterID * pos' should go to java-frontend *) |
16 ) list)) list); |
50 ) list)) list); |
17 |
51 |
18 fun reset_states () = Synchronized.change states (fn _ => []); |
52 fun reset () = Synchronized.change states (fn _ => []); |
19 (* |
53 (* |
20 states:= [(3,(Calc.state_empty_pre, [(1,e_pos'), |
54 states:= [(3,(Calc.state_empty_pre, [(1,e_pos'), |
21 (3,e_pos')])), |
55 (3,e_pos')])), |
22 (4,(Calc.state_empty_pre, [(1,e_pos'), |
56 (4,(Calc.state_empty_pre, [(1,e_pos'), |
23 (2,e_pos')]))]; |
57 (2,e_pos')]))]; |
48 (string_of_int uI)) |
82 (string_of_int uI)) |
49 | SOME ps => (new_key ps 1):calcID; |
83 | SOME ps => (new_key ps 1):calcID; |
50 > get_calcID 1 (!states); |
84 > get_calcID 1 (!states); |
51 val it = 1 : calcID |
85 val it = 1 : calcID |
52 *) |
86 *) |
53 (* add users to a Calc.state_pre *) |
|
54 fun get_iterID (cI: calcID) |
|
55 (p: (calcID * (Calc.state_pre * (iterID * Pos.pos') list)) list) = |
|
56 case assoc (p, cI) of |
|
57 NONE => raise ERROR ("get_iterID: no iterID " ^ (string_of_int cI)) |
|
58 | SOME (_, us) => (new_key us 1): iterID; |
|
59 (* get_iterID 3 (!states); |
|
60 val it = 2 : iterID*) |
|
61 |
|
62 |
87 |
63 (** retrieve, update, delete a state by iterID, calcID **) |
88 (** retrieve, update, delete a state by iterID, calcID **) |
64 |
89 |
65 (*///7.10. |
90 (*///7.10. |
66 fun get_state (uI:iterID) (pI:calcID) = get_cal uI pI (!states); |
91 fun get_state (uI:iterID) (pI:calcID) = get_cal uI pI (!states); |
335 |val it = |
360 |val it = |
336 | [(2, (((EmptyPtree, ([], Und)), []), [(2, ([], Und)), (1, ([], Und))])), |
361 | [(2, (((EmptyPtree, ([], Und)), []), [(2, ([], Und)), (1, ([], Und))])), |
337 | (1, (((EmptyPtree, ([], Und)), []), [])), |
362 | (1, (((EmptyPtree, ([], Und)), []), [])), |
338 | (3, (((EmptyPtree, ([], Und)), []), []))] |
363 | (3, (((EmptyPtree, ([], Und)), []), []))] |
339 *) |
364 *) |
365 |
|
366 (**)end(*struct*) |