neuper@37906
|
1 |
(* states for calculation in global refs
|
neuper@37906
|
2 |
use"../states.sml";
|
neuper@37906
|
3 |
use"states.sml";
|
neuper@37906
|
4 |
*)
|
neuper@37906
|
5 |
|
neuper@37906
|
6 |
(*
|
neuper@37906
|
7 |
type hide = (pblID *
|
neuper@37906
|
8 |
string list * (*hide: tacs +
|
neuper@37906
|
9 |
"ALL", .. result immediately
|
neuper@37906
|
10 |
"MODELPBL", .. modeling hidden
|
neuper@37906
|
11 |
"SPEC", .. specifying hidden
|
neuper@37906
|
12 |
"MODELMET", .. (additional itms !)
|
neuper@37906
|
13 |
"APPLY", .. solving hidden
|
neuper@37906
|
14 |
detail: rls
|
neuper@37906
|
15 |
"Rewrite_*" (as strings) must _not_ be ..
|
neuper@37906
|
16 |
.. contained in this list, rls _only_ !*)
|
neuper@37906
|
17 |
bool) (*inherit to children in pbl-herarchy*)
|
neuper@37906
|
18 |
list;
|
neuper@37906
|
19 |
|
neuper@37906
|
20 |
(*. points a pbl/metID to a sub-hierarchy of key ?.*)
|
neuper@37906
|
21 |
fun is_child_of child key =
|
neuper@37906
|
22 |
let fun is_ch [] [] = true (*is child of itself*)
|
neuper@37906
|
23 |
| is_ch (c::_) [] = true
|
neuper@37906
|
24 |
| is_ch [] (k::_) = false
|
neuper@37906
|
25 |
| is_ch (c::cs) (k::ks) =
|
neuper@37906
|
26 |
if c = k then is_ch cs ks else false
|
neuper@37906
|
27 |
in is_ch (rev child) (rev key) end;
|
neuper@37906
|
28 |
(*
|
neuper@37986
|
29 |
is_child_of ["root'","univar","equation"] ["univar","equation"];
|
neuper@37906
|
30 |
val it = true : bool
|
neuper@37986
|
31 |
is_child_of ["root'","univar","equation"] ["system","equation"];
|
neuper@37906
|
32 |
val it = false : bool
|
neuper@37906
|
33 |
is_child_of ["equation"] ["system","equation"];
|
neuper@37906
|
34 |
val it = false : bool
|
neuper@37986
|
35 |
is_child_of ["root'","univar","equation"] ["linear","univar","equation"];
|
neuper@37906
|
36 |
val it = false : bool
|
neuper@37906
|
37 |
*)
|
neuper@37906
|
38 |
|
neuper@37906
|
39 |
(*.what tactics have to be hidden (in model/specify these may be several).*)
|
neuper@37906
|
40 |
datatype hid =
|
neuper@37906
|
41 |
Show (**)
|
neuper@37906
|
42 |
| Hundef (**)
|
neuper@37906
|
43 |
| Htac (*a tactic has to be hidden*)
|
neuper@37906
|
44 |
| Hmodel (*the model of the (sub)problem has to be hidden*)
|
neuper@37906
|
45 |
| Hspecify (*the specification of the (sub)problem has to be hidden*)
|
neuper@37906
|
46 |
| Happly; (*solving the (sub)problem has to be hidden*)
|
neuper@37906
|
47 |
|
neuper@37906
|
48 |
(*. search all pbls if there is some tactic or model/spec/calc to hide .*)
|
neuper@37906
|
49 |
fun is_hid pblID arg [] = Show
|
neuper@37906
|
50 |
| is_hid pblID arg ((pblID', strs, inherit)::pts) =
|
neuper@37906
|
51 |
let fun is_mem arg =
|
neuper@37906
|
52 |
if arg mem strs then Htac
|
neuper@37906
|
53 |
else if arg mem ["Add_Given","Add_Find","Add_Relation"]
|
neuper@37906
|
54 |
andalso "MODEL" mem strs then Hmodel
|
neuper@37906
|
55 |
else if arg mem ["Specify_Theory","Specify_Problem",
|
neuper@37906
|
56 |
"Specify_Method"]
|
neuper@37906
|
57 |
andalso "SPEC" mem strs then Hspecify
|
neuper@37906
|
58 |
else if "APPLY" mem strs then Htac
|
neuper@37906
|
59 |
else Hundef
|
neuper@37906
|
60 |
in if inherit then
|
neuper@37906
|
61 |
if is_child_of (pblID:pblID) pblID'
|
neuper@37906
|
62 |
then case is_mem arg of Hundef => is_hid pblID arg (pts:hide)
|
neuper@37906
|
63 |
| hid => hid
|
neuper@37906
|
64 |
else is_hid pblID arg pts
|
neuper@37906
|
65 |
else if pblID = pblID'
|
neuper@37906
|
66 |
then case is_mem arg of Hundef => is_hid pblID arg (pts:hide)
|
neuper@37906
|
67 |
| hid => hid
|
neuper@37906
|
68 |
else is_hid pblID arg pts
|
neuper@37906
|
69 |
end;
|
neuper@37906
|
70 |
(*val hide = [([],["Refine_Tacitly"],true),
|
neuper@37906
|
71 |
(["univar","equation"],["Apply_Method","Model_Problem","SPEC"],
|
neuper@37906
|
72 |
false)]
|
neuper@37906
|
73 |
:hide;
|
neuper@37906
|
74 |
is_hid [] "Rewrite" hide;
|
neuper@37906
|
75 |
val it = Show
|
neuper@37906
|
76 |
is_hid ["any","problem"] "Refine_Tacitly" hide;
|
neuper@37906
|
77 |
val it = Htac
|
neuper@37986
|
78 |
is_hid ["root'","univar","equation"] "Apply_Method" hide;
|
neuper@37906
|
79 |
val it = Show
|
neuper@37906
|
80 |
is_hid ["univar","equation"] "Apply_Method" hide;
|
neuper@37906
|
81 |
val it = Htac
|
neuper@37906
|
82 |
is_hid ["univar","equation"] "Specify_Problem" hide;
|
neuper@37906
|
83 |
val it = Hspecify
|
neuper@37906
|
84 |
*)
|
neuper@37906
|
85 |
|
neuper@37906
|
86 |
fun is_hide pblID (tac as (Subproblem (_,pI))) (det:detail) =
|
neuper@37906
|
87 |
is_hid pblID "SELF" det
|
neuper@37906
|
88 |
| is_hide pblID (tac as (Rewrite (thmID,_))) det =
|
neuper@37906
|
89 |
is_hid pblID thmID det
|
neuper@37906
|
90 |
| is_hide pblID (tac as (Rewrite_Inst (_,(thmID,_)))) det =
|
neuper@37906
|
91 |
is_hid pblID thmID det
|
neuper@37906
|
92 |
| is_hide pblID (tac as (Rewrite_Set rls)) det =
|
neuper@37906
|
93 |
is_hid pblID rls det
|
neuper@37906
|
94 |
| is_hide pblID (tac as (Rewrite_Set_Inst (_,rls))) det =
|
neuper@37906
|
95 |
is_hid pblID rls det
|
neuper@37906
|
96 |
| is_hide pblID tac det = is_hid pblID (tac2IDstr tac) det;
|
neuper@37906
|
97 |
(*val hide = [([],["Refine_Tacitly"],true),
|
neuper@37906
|
98 |
(["univar","equation"],["Apply_Method","Model_Problem",
|
neuper@37906
|
99 |
"SPEC","SELF"],
|
neuper@37906
|
100 |
false)]
|
neuper@37906
|
101 |
:hide;
|
neuper@37906
|
102 |
is_hide [] (Rewrite ("","")) hide;
|
neuper@37906
|
103 |
val it = Show
|
neuper@37906
|
104 |
is_hide ["any","problem"] (Refine_Tacitly []) hide;
|
neuper@37906
|
105 |
val it = Htac
|
neuper@37986
|
106 |
is_hide ["root'","univar","equation"] (Apply_Method []) hide;
|
neuper@37906
|
107 |
val it = Show
|
neuper@37906
|
108 |
is_hide ["univar","equation"] (Apply_Method []) hide;
|
neuper@37906
|
109 |
val it = Htac
|
neuper@37906
|
110 |
is_hide ["univar","equation"] (Specify_Problem []) hide;
|
neuper@37906
|
111 |
val it = Hspecify
|
neuper@37906
|
112 |
is_hide ["univar","equation"] (Subproblem (e_domID,["univar","equation"]))hide;
|
neuper@37906
|
113 |
val it = Htac
|
neuper@37906
|
114 |
is_hide ["equation"] (Subproblem (e_domID,["univar","equation"]))hide;
|
neuper@37906
|
115 |
val it = Show
|
neuper@37906
|
116 |
*)
|
neuper@37906
|
117 |
|
neuper@37906
|
118 |
|
neuper@37906
|
119 |
(*. search all pbls in detail if there is some rls' to be detailed .*)
|
neuper@37906
|
120 |
fun is_det pblID arg [] = false
|
neuper@37906
|
121 |
| is_det pblID arg ((pblID', rlss, inherit)::pts) =
|
neuper@37906
|
122 |
if inherit then
|
neuper@37906
|
123 |
if is_child_of (pblID:pblID) pblID'
|
neuper@37906
|
124 |
then if arg mem rlss then true
|
neuper@37906
|
125 |
else is_det pblID arg (pts:detail)
|
neuper@37906
|
126 |
else is_det pblID arg pts
|
neuper@37906
|
127 |
else if pblID = pblID'
|
neuper@37906
|
128 |
then if arg mem rlss then true
|
neuper@37906
|
129 |
else is_det pblID arg (pts:detail)
|
neuper@37906
|
130 |
else is_det pblID arg pts;
|
neuper@37906
|
131 |
|
neuper@37906
|
132 |
(*fun is_detail pblID (tac as (Subproblem (_,pI))) (det:detail) =
|
neuper@37906
|
133 |
is_det pblID "SELF" det*)
|
neuper@37906
|
134 |
fun is_detail pblID (tac as (Rewrite_Set rls)) det =
|
neuper@37906
|
135 |
is_det pblID rls det
|
neuper@37906
|
136 |
| is_detail pblID (tac as (Rewrite_Set_Inst (_,rls))) det =
|
neuper@37906
|
137 |
is_det pblID rls det
|
neuper@37906
|
138 |
| is_detail _ _ _ = false;
|
neuper@37906
|
139 |
----------------------------------------*)
|
neuper@37906
|
140 |
|
neuper@37906
|
141 |
type iterID = int;
|
neuper@37906
|
142 |
type calcID = int;
|
neuper@37906
|
143 |
|
s1210629013@55445
|
144 |
val states = Synchronized.var "isac_states"
|
neuper@38007
|
145 |
([]:(calcID *
|
neuper@37906
|
146 |
(calcstate *
|
neuper@37906
|
147 |
(iterID * (*1 sets the 'active formula'*)
|
neuper@37906
|
148 |
pos' (*for iterator of a user *)
|
neuper@37906
|
149 |
) list)) list);
|
s1210629013@55445
|
150 |
|
s1210629013@55445
|
151 |
fun reset_states () = Synchronized.change states (fn _ => []);
|
neuper@37906
|
152 |
(*
|
neuper@37906
|
153 |
states:= [(3,(e_calcstate, [(1,e_pos'),
|
neuper@37906
|
154 |
(3,e_pos')])),
|
neuper@37906
|
155 |
(4,(e_calcstate, [(1,e_pos'),
|
neuper@37906
|
156 |
(2,e_pos')]))];
|
neuper@37906
|
157 |
*)
|
neuper@37906
|
158 |
|
neuper@37906
|
159 |
(** create new instances of users and ptrees
|
neuper@37906
|
160 |
new keys are the lowest possible in the association list **)
|
neuper@37906
|
161 |
|
neuper@37906
|
162 |
(* add users *)
|
neuper@37906
|
163 |
fun new_key u n = case assoc (u, n) of
|
neuper@37926
|
164 |
NONE => n
|
neuper@37926
|
165 |
| SOME _ => new_key u (n+1);
|
neuper@37906
|
166 |
(*///10.10
|
neuper@37906
|
167 |
fun get_calcID (u:(calcID * (calcstate * (iterID * pos') list)) list) =
|
neuper@37906
|
168 |
(new_key u 1):calcID;*)
|
neuper@37906
|
169 |
(*
|
neuper@37906
|
170 |
val new_iterID = get_calcID (!states);
|
neuper@37906
|
171 |
val it = 1 : int
|
neuper@37906
|
172 |
states:= (!states) @ [(new_iterID, [])];
|
neuper@37906
|
173 |
!states;
|
neuper@37906
|
174 |
val it = [(3,[(#,#),(#,#)]),(4,[(#,#),(#,#)]),(1,[])]
|
neuper@37906
|
175 |
*)
|
neuper@37906
|
176 |
|
neuper@37906
|
177 |
(*///7.10.03/// add states to a users active states
|
neuper@37906
|
178 |
fun get_calcID (uI:iterID) (p:(iterID * (calcID * state) list) list) =
|
neuper@37906
|
179 |
case assoc (p, uI) of
|
neuper@38031
|
180 |
NONE => error ("get_calcID: no iterID " ^
|
neuper@37906
|
181 |
(string_of_int uI))
|
neuper@37926
|
182 |
| SOME ps => (new_key ps 1):calcID;
|
neuper@37906
|
183 |
> get_calcID 1 (!states);
|
neuper@37906
|
184 |
val it = 1 : calcID
|
neuper@37906
|
185 |
*)
|
neuper@37906
|
186 |
(* add users to a calcstate *)
|
neuper@37906
|
187 |
fun get_iterID (cI:calcID)
|
neuper@37906
|
188 |
(p:(calcID * (calcstate * (iterID * pos') list)) list) =
|
neuper@37906
|
189 |
case assoc (p, cI) of
|
neuper@38031
|
190 |
NONE => error ("get_iterID: no iterID " ^ (string_of_int cI))
|
neuper@37926
|
191 |
| SOME (_, us) => (new_key us 1):iterID;
|
neuper@37906
|
192 |
(* get_iterID 3 (!states);
|
neuper@37906
|
193 |
val it = 2 : iterID*)
|
neuper@37906
|
194 |
|
neuper@37906
|
195 |
|
neuper@37906
|
196 |
(** retrieve, update, delete a state by iterID, calcID **)
|
neuper@37906
|
197 |
|
neuper@37906
|
198 |
(*//////7.10.
|
neuper@37906
|
199 |
fun get_cal (uI:iterID) (pI:calcID) (p:(iterID * (calcID * state) list) list) =
|
neuper@37906
|
200 |
(the (assoc2 (p,(uI, pI))))
|
neuper@38031
|
201 |
handle _ => error ("get_state " ^ (string_of_int uI) ^
|
neuper@37906
|
202 |
" " ^ (string_of_int pI) ^ " not existent");
|
neuper@37906
|
203 |
> get_cal 3 1 (!states);
|
neuper@37906
|
204 |
val it = (((EmptyPtree,(#,#)),[]),([],[])) : state
|
neuper@37906
|
205 |
*)
|
neuper@37906
|
206 |
|
neuper@37906
|
207 |
(*///7.10.
|
neuper@37906
|
208 |
fun get_state (uI:iterID) (pI:calcID) = get_cal uI pI (!states);
|
neuper@37906
|
209 |
fun get_calc (uI:iterID) (pI:calcID) = (snd o (get_cal uI pI)) (!states);
|
neuper@37906
|
210 |
*)
|
neuper@37906
|
211 |
fun get_calc (cI:calcID) =
|
s1210629013@55445
|
212 |
case assoc (Synchronized.value states, cI) of
|
neuper@38031
|
213 |
NONE => error ("get_calc "^(string_of_int cI)^" not existent")
|
neuper@37926
|
214 |
| SOME (c, _) => c;
|
neuper@37906
|
215 |
fun get_pos (cI:calcID) (uI:iterID) =
|
s1210629013@55445
|
216 |
case assoc (Synchronized.value states, cI) of
|
neuper@38031
|
217 |
NONE => error ("get_pos: calc " ^ (string_of_int cI)
|
neuper@37906
|
218 |
^ " not existent")
|
neuper@37926
|
219 |
| SOME (_, us) =>
|
neuper@37906
|
220 |
(case assoc (us, uI) of
|
neuper@38031
|
221 |
NONE => error ("get_pos: user " ^ (string_of_int uI)
|
neuper@37906
|
222 |
^ " not existent")
|
neuper@37926
|
223 |
| SOME p => p);
|
neuper@37906
|
224 |
|
neuper@37906
|
225 |
|
neuper@37906
|
226 |
fun del_assoc ([],_) = []
|
neuper@37906
|
227 |
| del_assoc a =
|
neuper@37906
|
228 |
let fun del ([], key) ps = ps
|
neuper@37906
|
229 |
| del ((keyi, xi) :: pairs, key) ps =
|
neuper@37906
|
230 |
if key = keyi then ps @ pairs
|
neuper@37906
|
231 |
else del (pairs, key) (ps @ [(keyi, xi)])
|
neuper@37906
|
232 |
in del a [] end;
|
neuper@37906
|
233 |
(*
|
neuper@37906
|
234 |
> val ps = [(1,"1"),(2,"2"),(3,"3"),(4,"4")];
|
neuper@37906
|
235 |
> del_assoc (ps,3);
|
neuper@37906
|
236 |
val it = [(1,"1"),(2,"2"),(4,"4")] : (int * string) list
|
neuper@37906
|
237 |
*)
|
neuper@37906
|
238 |
|
neuper@37906
|
239 |
(* delete doesn't report non existing elements *)
|
neuper@37906
|
240 |
(*/////7.10.
|
neuper@37906
|
241 |
fun del_assoc2 (uI:iterID) (pI:calcID) ps =
|
neuper@37906
|
242 |
let val new_ps = del_assoc (the (assoc (ps, uI)), pI)
|
neuper@37906
|
243 |
in overwrite (ps, (uI, new_ps)) end;*)
|
neuper@37906
|
244 |
(*
|
neuper@37906
|
245 |
> states:= del_assoc2 4 41 (!states);
|
neuper@37906
|
246 |
> !states;
|
neuper@37906
|
247 |
val it = [(3,[(#,#),(#,#),(#,#)]),(4,[(#,#)]),(1,[(#,#)])] : states
|
neuper@37906
|
248 |
|
neuper@37906
|
249 |
> del_user 3;
|
neuper@37906
|
250 |
> !states;
|
neuper@37906
|
251 |
val it = [(4,[(#,#)]),(1,[(#,#)])] : states
|
neuper@37906
|
252 |
*)
|
neuper@37906
|
253 |
fun del_assoc2 (cI:calcID) (uI:iterID) ps =
|
neuper@37906
|
254 |
case assoc (ps, cI) of
|
neuper@37926
|
255 |
NONE => ps
|
neuper@37926
|
256 |
| SOME (cs, us) =>
|
neuper@37906
|
257 |
overwrite (ps, (cI, (cs, del_assoc (us, uI))));
|
neuper@37906
|
258 |
(*
|
neuper@37906
|
259 |
> del_assoc2 4 1 (!states);
|
neuper@37906
|
260 |
val it =
|
neuper@37906
|
261 |
[(3, (((EmptyPtree, ([], Und)), []), [(1, ([], Und)), (3, ([], Und))])),
|
neuper@37906
|
262 |
(4, (((EmptyPtree, ([], Und)), []), [(2, ([], Und))]))]*)
|
neuper@37906
|
263 |
|
neuper@37906
|
264 |
(*///7.10.
|
neuper@37906
|
265 |
fun overwrite2 (ps, (((uI:iterID), (pI:calcID)), p)) =
|
neuper@37906
|
266 |
let val new_ps = overwrite (the (assoc (ps, uI)), (pI, p))
|
neuper@37906
|
267 |
in (overwrite (ps, (uI, new_ps)))
|
neuper@38031
|
268 |
handle _ => error ("overwrite2 " ^ (string_of_int uI) ^
|
neuper@37906
|
269 |
" " ^ (string_of_int pI) ^ " not existent")
|
neuper@37906
|
270 |
end;*)
|
neuper@37906
|
271 |
fun overwrite2 (ps, (((cI:calcID), (uI:iterID)), p)) =
|
neuper@37906
|
272 |
case assoc (ps, cI) of
|
neuper@37926
|
273 |
NONE =>
|
neuper@38031
|
274 |
error ("overwrite2: calc " ^ (string_of_int uI) ^" not existent")
|
neuper@37926
|
275 |
| SOME (cs, us) =>
|
neuper@37906
|
276 |
overwrite (ps, (cI ,(cs, overwrite (us, (uI, p)))));
|
neuper@37906
|
277 |
|
neuper@55469
|
278 |
(* here is _no_ critical section on states; sufficient would be
|
neuper@55469
|
279 |
fun upd_calc cI cs =
|
neuper@55469
|
280 |
case assoc (Synchronized.value states, cI) of
|
neuper@55469
|
281 |
NONE => error ...
|
neuper@55469
|
282 |
| SOME (_, us) =>
|
neuper@55469
|
283 |
Synchronized.change states (fn s => overwrite ...)
|
neuper@55469
|
284 |
*)
|
s1210629013@55445
|
285 |
fun upd_calc (cI:calcID) cs = Synchronized.change states
|
s1210629013@55445
|
286 |
(fn s => case assoc (s, cI) of
|
s1210629013@55445
|
287 |
NONE => error ("upd_calc " ^ (string_of_int cI) ^ " not existent")
|
s1210629013@55445
|
288 |
| SOME (_, us) => overwrite (s, (cI, (cs, us))));
|
neuper@37906
|
289 |
(*WN051210 testing before initac: only 1 taci in calcstate so far:
|
neuper@37906
|
290 |
fun upd_calc (cI:calcID) (cs as (_, tacis):calcstate) =
|
neuper@37906
|
291 |
(if length tacis > 1
|
neuper@38031
|
292 |
then error ("upd_calc, |tacis|>1: "^tacis2str tacis)
|
neuper@37906
|
293 |
else ();
|
neuper@37906
|
294 |
case assoc (!states, cI) of
|
neuper@38031
|
295 |
NONE => error ("upd_calc "^(string_of_int cI)^" not existent")
|
neuper@37926
|
296 |
| SOME (_, us) => states:= overwrite (!states, (cI, (cs, us)))
|
neuper@37906
|
297 |
);*)
|
neuper@37906
|
298 |
|
neuper@37906
|
299 |
|
neuper@37906
|
300 |
(*///7.10.
|
neuper@37906
|
301 |
fun upd_tacis (uI:iterID) (pI:calcID) tacis =
|
neuper@37906
|
302 |
let val (p, (ptp,_)) = get_state uI pI
|
neuper@37906
|
303 |
in states:=
|
neuper@37906
|
304 |
overwrite2 ((!states), ((uI, pI), (p, (ptp, tacis)))) end;*)
|
s1210629013@55445
|
305 |
fun upd_tacis (cI:calcID) tacis = Synchronized.change states
|
s1210629013@55445
|
306 |
(fn s => case assoc (s, cI) of
|
s1210629013@55445
|
307 |
NONE =>
|
s1210629013@55445
|
308 |
error ("upd_tacis: calctree " ^ (string_of_int cI) ^ " not existent")
|
s1210629013@55445
|
309 |
| SOME ((ptp, _), us) => overwrite (s, (cI, ((ptp, tacis), us))));
|
neuper@37906
|
310 |
(*///7.10.
|
neuper@37906
|
311 |
fun upd_ipos (uI:iterID) (pI:calcID) (ip:pos') =
|
neuper@37906
|
312 |
let val (_, calc) = get_state uI pI
|
neuper@37906
|
313 |
in states:= overwrite2 ((!states), ((uI, pI), (ip, calc))) end;*)
|
s1210629013@55445
|
314 |
fun upd_ipos (cI:calcID) (uI:iterID) (ip:pos') = Synchronized.change states
|
s1210629013@55445
|
315 |
(fn s => case assoc (s, cI) of
|
s1210629013@55445
|
316 |
NONE =>
|
s1210629013@55445
|
317 |
error ("upd_ipos: calctree " ^ (string_of_int cI) ^ " not existent")
|
s1210629013@55445
|
318 |
| SOME (cs, us) => overwrite2 (s, ((cI, uI), ip)));
|
neuper@37906
|
319 |
|
neuper@37906
|
320 |
|
neuper@37906
|
321 |
(** add and delete calcs **)
|
neuper@37906
|
322 |
|
neuper@37906
|
323 |
(*///7.10
|
neuper@37906
|
324 |
fun add_pID (uI:iterID) (s:state) (p:(iterID * (calcID * state) list) list) =
|
neuper@37906
|
325 |
let val new_ID = get_calcID uI p;
|
neuper@37906
|
326 |
val new_states = (the (assoc (p, uI))) @ [(new_ID, s)];
|
neuper@37906
|
327 |
in (new_ID, (overwrite (p, (uI, new_states)))) end;*)
|
neuper@37906
|
328 |
(*
|
neuper@37906
|
329 |
> val (new_calcID, new_states) = add_pID 1 (!states);
|
neuper@37906
|
330 |
> states:= new_states;
|
neuper@37906
|
331 |
> !states;
|
neuper@37906
|
332 |
val it = [(3,[(#,#),(#,#)]),(4,[(#,#),(#,#)]),(1,[(#,#)])] : states
|
neuper@37906
|
333 |
> val (new_calcID, new_states) = add_pID 3 (!states);
|
neuper@37906
|
334 |
> states:= new_states;
|
neuper@37906
|
335 |
> !states;
|
neuper@37906
|
336 |
val it = [(3,[(#,#),(#,#),(#,#)]),(4,[(#,#),(#,#)]),(1,[(#,#)])] : states
|
neuper@37906
|
337 |
> assoc2 (!states, (3, 1));
|
neuper@37926
|
338 |
val it = SOME EmptyPtree : ptree option
|
neuper@37906
|
339 |
> assoc2 (!states, (3, 2));
|
neuper@37926
|
340 |
val it = NONE : ptree option
|
neuper@37906
|
341 |
*)
|
neuper@37906
|
342 |
(*///7.10
|
neuper@37906
|
343 |
fun add_calc (uI:iterID) (s:state) =
|
neuper@37906
|
344 |
let val (new_calcID, new_calcs) = add_pID uI s (!states)
|
neuper@37906
|
345 |
in states:= new_calcs;
|
neuper@37906
|
346 |
new_calcID end; *)
|
s1210629013@55445
|
347 |
fun add_user (cI:calcID) = Synchronized.change_result states
|
s1210629013@55445
|
348 |
(fn s => case assoc (s, cI) of
|
s1210629013@55445
|
349 |
NONE =>
|
s1210629013@55445
|
350 |
error ("add_user: calctree " ^ (string_of_int cI) ^ " not existent")
|
s1210629013@55445
|
351 |
| SOME (cs, us) =>
|
s1210629013@55445
|
352 |
let
|
s1210629013@55445
|
353 |
val new_uI = new_key us 1
|
s1210629013@55445
|
354 |
in (new_uI:iterID, overwrite2 (s, ((cI, new_uI), e_pos'))) end);
|
neuper@37906
|
355 |
|
neuper@37906
|
356 |
(*///10.10.
|
neuper@37906
|
357 |
fun del_calc (uI:iterID) (pI:calcID) =
|
neuper@37906
|
358 |
(states:= del_assoc2 uI pI (!states); pI);*)
|
s1210629013@55445
|
359 |
fun del_user (cI:calcID) (uI:iterID) =
|
s1210629013@55445
|
360 |
Synchronized.change_result states (fn s => (uI, del_assoc2 cI uI s));
|
neuper@37906
|
361 |
|
neuper@37906
|
362 |
|
neuper@37906
|
363 |
(** add and delete calculations **)
|
neuper@55469
|
364 |
|
neuper@55469
|
365 |
(* here is the _only_ critical section on states,
|
neuper@55469
|
366 |
because a single calculation (with _one_ cI) is sequential *)
|
s1210629013@55445
|
367 |
fun add_calc (cs:calcstate) = Synchronized.change_result states
|
s1210629013@55445
|
368 |
(fn s =>
|
s1210629013@55445
|
369 |
let val new_cI = new_key s 1
|
s1210629013@55445
|
370 |
in (new_cI:calcID, s @ [(new_cI, (cs, []))]) end);
|
neuper@37906
|
371 |
|
neuper@37906
|
372 |
(* delete doesn't report non existing elements *)
|
neuper@37906
|
373 |
(*///7.10
|
neuper@37906
|
374 |
fun del_user (uI:userID) =
|
neuper@37906
|
375 |
(states:= del_assoc (!states, uI); uI);*)
|
s1210629013@55445
|
376 |
fun del_calc (cI:calcID) = Synchronized.change_result states
|
s1210629013@55445
|
377 |
(fn s => (cI:calcID, del_assoc (s, cI)));
|
neuper@37906
|
378 |
|
neuper@37906
|
379 |
(* -------------- test all exported funs --------------
|
neuper@37906
|
380 |
///7.10
|
neuper@37906
|
381 |
Compiler.Control.Print.printDepth:=8;
|
neuper@37906
|
382 |
states:=[];
|
neuper@37906
|
383 |
add_user (); add_user (); !states;
|
neuper@37906
|
384 |
ML> val it = 1 : userID
|
neuper@37906
|
385 |
ML> val it = 2 : userID
|
neuper@37906
|
386 |
ML> val it = [(1,[]),(2,[])]
|
neuper@37906
|
387 |
|
neuper@37906
|
388 |
val (hide,detail) = ([(["pI"],["tac"],true)]:hide,
|
neuper@37906
|
389 |
[(["pI"],["tac"],true)]:detail);
|
neuper@37906
|
390 |
add_calc 1 e_state;
|
neuper@37906
|
391 |
add_calc 1 (e_calcstate,(hide,detail)); !states;
|
neuper@37906
|
392 |
ML> val it = 1 : calcID
|
neuper@37906
|
393 |
ML> val it = 2 : calcID
|
neuper@37906
|
394 |
ML> val it =
|
neuper@37906
|
395 |
[(1,
|
neuper@37906
|
396 |
[(1,(((EmptyPtree,(#,#)),[]),([],[]))),
|
neuper@37906
|
397 |
(2,(((EmptyPtree,(#,#)),[]),([(#,#,#)],[(#,#,#)])))]),(2,[])]
|
neuper@37906
|
398 |
|
neuper@37906
|
399 |
val (pt,(p,p_)) = (EmptyPtree,e_pos');
|
neuper@37906
|
400 |
val (pt,_) = cappend_problem pt p Uistate ([],e_spec);
|
neuper@37906
|
401 |
upd_calc 1 2 ((pt,(p,p_)),[]); !states;
|
neuper@37906
|
402 |
ML> val it =
|
neuper@37906
|
403 |
[(1,
|
neuper@37906
|
404 |
[(1,(((EmptyPtree,(#,#)),[]),([],[]))),
|
neuper@37906
|
405 |
(2,(((Nd #,(#,#)),[]),([(#,#,#)],[(#,#,#)])))]),(2,[])]
|
neuper@37906
|
406 |
(* ~~~~~~~~~~~~~~~~~~~~ unchanged !!!*)
|
neuper@37906
|
407 |
|
neuper@37906
|
408 |
get_state 1 1; get_state 1 2;
|
neuper@37906
|
409 |
ML> val it = (((EmptyPtree,([],Und)),[]),([],[])) : state
|
neuper@37906
|
410 |
ML> val it =
|
neuper@37906
|
411 |
(((Nd
|
neuper@37906
|
412 |
(PblObj
|
neuper@37906
|
413 |
{branch=NoBranch,cell=[],env=(#,#,#,#),loc=(#,#),meth=[],
|
neuper@37906
|
414 |
model={Find=#,Given=#,Relate=#,Where=#,With=#},origin=(#,#),
|
neuper@37906
|
415 |
ostate=Incomplete,probl=[],result=(#,#),spec=(#,#,#)},[]),([],Und)),
|
neuper@37906
|
416 |
[]),([(["pI"],["tac"],true)],[(["pI"],["tac"],true)])) : state
|
neuper@37906
|
417 |
|
neuper@37906
|
418 |
del_calc 2 1 (*non existent - NO msg!*); del_calc 1 2; !states;
|
neuper@37906
|
419 |
ML> val it = [(1,[(1,(((EmptyPtree,(#,#)),[]),([],[])))]),(2,[])]
|
neuper@37906
|
420 |
|
neuper@37906
|
421 |
del_user 1; !states;
|
neuper@37906
|
422 |
ML> val it = [(2,[])]
|
neuper@37906
|
423 |
|
neuper@37906
|
424 |
add_user (); add_user (); !states;
|
neuper@37906
|
425 |
ML> val it = 1 : userID
|
neuper@37906
|
426 |
ML> val it = 3 : userID
|
neuper@37906
|
427 |
ML> val it = [(2,[]),(1,[]),(3,[])]
|
neuper@37906
|
428 |
*)
|
neuper@37906
|
429 |
|
neuper@37906
|
430 |
|
neuper@37906
|
431 |
(* -------------- test all exported funs --------------
|
neuper@37906
|
432 |
print_depth 9;
|
neuper@37906
|
433 |
states:=[];
|
neuper@37906
|
434 |
add_calc e_calcstate; add_calc e_calcstate; !states;
|
neuper@37906
|
435 |
|val it = 1 : calcID
|
neuper@37906
|
436 |
|val it = 2 : calcID
|
neuper@37906
|
437 |
|val it =
|
neuper@37906
|
438 |
| [(1, (((EmptyPtree, ([], Und)), []), [])),
|
neuper@37906
|
439 |
| (2, (((EmptyPtree, ([], Und)), []), []))]
|
neuper@37906
|
440 |
|
neuper@37906
|
441 |
add_user 2; add_user 2; !states;
|
neuper@37906
|
442 |
|val it = 1 : userID
|
neuper@37906
|
443 |
|val it = 2 : userID
|
neuper@37906
|
444 |
|val it =
|
neuper@37906
|
445 |
| [(1, (((EmptyPtree, ([], Und)), []), [])),
|
neuper@37906
|
446 |
| (2, (((EmptyPtree, ([], Und)), []), [(1, ([], Und)), (2, ([], Und))]))]
|
neuper@37906
|
447 |
|
neuper@37906
|
448 |
|
neuper@37906
|
449 |
val cs = ((EmptyPtree, ([111], Und)), []) : calcstate;
|
neuper@37906
|
450 |
upd_calc 1 cs; !states;
|
neuper@37906
|
451 |
|val it =
|
neuper@37906
|
452 |
| [(1, (((EmptyPtree, ([111], Und)), []), [])),
|
neuper@37906
|
453 |
| (2, (((EmptyPtree, ([], Und)), []), [(1, ([], Und)), (2, ([], Und))]))]
|
neuper@37906
|
454 |
|
neuper@37906
|
455 |
get_calc 1; get_calc 2;
|
neuper@37906
|
456 |
|val it = ((EmptyPtree, ([111], Und)), []) : calcstate
|
neuper@37906
|
457 |
|val it = ((EmptyPtree, ([], Und)), []) : calcstate
|
neuper@37906
|
458 |
|
neuper@37906
|
459 |
del_user 2 3 (*non existent - NO msg!*); del_user 2 1; !states;
|
neuper@37906
|
460 |
|val it = 3 : userID
|
neuper@37906
|
461 |
|val it = 1 : userID
|
neuper@37906
|
462 |
|val it =
|
neuper@37906
|
463 |
| [(1, (((EmptyPtree, ([111], Und)), []), [])),
|
neuper@37906
|
464 |
| (2, (((EmptyPtree, ([], Und)), []), [(2, ([], Und))]))]
|
neuper@37906
|
465 |
|
neuper@37906
|
466 |
del_calc 1; !states;
|
neuper@37906
|
467 |
|val it = 1 : calcID
|
neuper@37906
|
468 |
|val it = [(2, (((EmptyPtree, ([], Und)), []), [(2, ([], Und))]))]
|
neuper@37906
|
469 |
|
neuper@37906
|
470 |
add_calc e_calcstate; add_calc e_calcstate; !states;
|
neuper@37906
|
471 |
|val it = 1 : calcID
|
neuper@37906
|
472 |
|val it = 3 : calcID
|
neuper@37906
|
473 |
|val it =
|
neuper@37906
|
474 |
| [(2, (((EmptyPtree, ([], Und)), []), [(2, ([], Und))])),
|
neuper@37906
|
475 |
| (1, (((EmptyPtree, ([], Und)), []), [])),
|
neuper@37906
|
476 |
| (3, (((EmptyPtree, ([], Und)), []), []))]
|
neuper@37906
|
477 |
|
neuper@37906
|
478 |
add_user 2; !states;
|
neuper@37906
|
479 |
|val it =
|
neuper@37906
|
480 |
| [(2, (((EmptyPtree, ([], Und)), []), [(2, ([], Und)), (1, ([], Und))])),
|
neuper@37906
|
481 |
| (1, (((EmptyPtree, ([], Und)), []), [])),
|
neuper@37906
|
482 |
| (3, (((EmptyPtree, ([], Und)), []), []))]
|
neuper@38007
|
483 |
*)
|