138 | is_detail _ _ _ = false; |
138 | is_detail _ _ _ = false; |
139 ----------------------------------------*) |
139 ----------------------------------------*) |
140 |
140 |
141 (* holds calculations; these are read/updated from the java-frontend at each interaction*) |
141 (* holds calculations; these are read/updated from the java-frontend at each interaction*) |
142 val states = Synchronized.var "isac_states" ([] : |
142 val states = Synchronized.var "isac_states" ([] : |
143 (calcID * (* the id unique for a calculation *) |
143 (Celem.calcID * (* the id unique for a calculation *) |
144 (Chead.calcstate * (* the interpreter state *) |
144 (Chead.calcstate * (* the interpreter state *) |
145 (iterID * (* 1 sets the 'active formula': a calc. can have several visitors*) |
145 (Celem.iterID * (* 1 sets the 'active formula': a calc. can have several visitors*) |
146 Ctree.pos' (* for iterator of a user *) |
146 Ctree.pos' (* for iterator of a user *) |
147 (* TODO iterID * pos' should go to java-frontend *) |
147 (* TODO iterID * pos' should go to java-frontend *) |
148 ) list)) list); |
148 ) list)) list); |
149 |
149 |
150 fun reset_states () = Synchronized.change states (fn _ => []); |
150 fun reset_states () = Synchronized.change states (fn _ => []); |
181 | SOME ps => (new_key ps 1):calcID; |
181 | SOME ps => (new_key ps 1):calcID; |
182 > get_calcID 1 (!states); |
182 > get_calcID 1 (!states); |
183 val it = 1 : calcID |
183 val it = 1 : calcID |
184 *) |
184 *) |
185 (* add users to a calcstate *) |
185 (* add users to a calcstate *) |
186 fun get_iterID (cI:calcID) |
186 fun get_iterID (cI: Celem.calcID) |
187 (p:(calcID * (Chead.calcstate * (iterID * Ctree.pos') list)) list) = |
187 (p: (Celem.calcID * (Chead.calcstate * (Celem.iterID * Ctree.pos') list)) list) = |
188 case assoc (p, cI) of |
188 case assoc (p, cI) of |
189 NONE => error ("get_iterID: no iterID " ^ (string_of_int cI)) |
189 NONE => error ("get_iterID: no iterID " ^ (string_of_int cI)) |
190 | SOME (_, us) => (new_key us 1):iterID; |
190 | SOME (_, us) => (new_key us 1): Celem.iterID; |
191 (* get_iterID 3 (!states); |
191 (* get_iterID 3 (!states); |
192 val it = 2 : iterID*) |
192 val it = 2 : iterID*) |
193 |
193 |
194 |
194 |
195 (** retrieve, update, delete a state by iterID, calcID **) |
195 (** retrieve, update, delete a state by iterID, calcID **) |
205 |
205 |
206 (*///7.10. |
206 (*///7.10. |
207 fun get_state (uI:iterID) (pI:calcID) = get_cal uI pI (!states); |
207 fun get_state (uI:iterID) (pI:calcID) = get_cal uI pI (!states); |
208 fun get_calc (uI:iterID) (pI:calcID) = (snd o (get_cal uI pI)) (!states); |
208 fun get_calc (uI:iterID) (pI:calcID) = (snd o (get_cal uI pI)) (!states); |
209 *) |
209 *) |
210 fun get_calc (cI:calcID) = |
210 fun get_calc (cI: Celem.calcID) = |
211 case assoc (Synchronized.value states, cI) of |
211 case assoc (Synchronized.value states, cI) of |
212 NONE => error ("get_calc "^(string_of_int cI)^" not existent") |
212 NONE => error ("get_calc "^(string_of_int cI)^" not existent") |
213 | SOME (c, _) => c; |
213 | SOME (c, _) => c; |
214 fun get_pos (cI:calcID) (uI:iterID) = |
214 fun get_pos (cI: Celem.calcID) (uI: Celem.iterID) = |
215 case assoc (Synchronized.value states, cI) of |
215 case assoc (Synchronized.value states, cI) of |
216 NONE => error ("get_pos: calc " ^ (string_of_int cI) |
216 NONE => error ("get_pos: calc " ^ (string_of_int cI) |
217 ^ " not existent") |
217 ^ " not existent") |
218 | SOME (_, us) => |
218 | SOME (_, us) => |
219 (case assoc (us, uI) of |
219 (case assoc (us, uI) of |
247 |
247 |
248 > del_user 3; |
248 > del_user 3; |
249 > !states; |
249 > !states; |
250 val it = [(4,[(#,#)]),(1,[(#,#)])] : states |
250 val it = [(4,[(#,#)]),(1,[(#,#)])] : states |
251 *) |
251 *) |
252 fun del_assoc2 (cI:calcID) (uI:iterID) ps = |
252 fun del_assoc2 (cI: Celem.calcID) (uI: Celem.iterID) ps = |
253 case assoc (ps, cI) of |
253 case assoc (ps, cI) of |
254 NONE => ps |
254 NONE => ps |
255 | SOME (cs, us) => |
255 | SOME (cs, us) => |
256 overwrite (ps, (cI, (cs, del_assoc (us, uI)))); |
256 overwrite (ps, (cI, (cs, del_assoc (us, uI)))); |
257 (* |
257 (* |
265 let val new_ps = overwrite (the (assoc (ps, uI)), (pI, p)) |
265 let val new_ps = overwrite (the (assoc (ps, uI)), (pI, p)) |
266 in (overwrite (ps, (uI, new_ps))) |
266 in (overwrite (ps, (uI, new_ps))) |
267 handle _ => error ("overwrite2 " ^ (string_of_int uI) ^ |
267 handle _ => error ("overwrite2 " ^ (string_of_int uI) ^ |
268 " " ^ (string_of_int pI) ^ " not existent") |
268 " " ^ (string_of_int pI) ^ " not existent") |
269 end;*) |
269 end;*) |
270 fun overwrite2 (ps, (((cI:calcID), (uI:iterID)), p)) = |
270 fun overwrite2 (ps, (((cI: Celem.calcID), (uI: Celem.iterID)), p)) = |
271 case assoc (ps, cI) of |
271 case assoc (ps, cI) of |
272 NONE => |
272 NONE => |
273 error ("overwrite2: calc " ^ (string_of_int uI) ^" not existent") |
273 error ("overwrite2: calc " ^ (string_of_int uI) ^" not existent") |
274 | SOME (cs, us) => |
274 | SOME (cs, us) => |
275 overwrite (ps, (cI ,(cs, overwrite (us, (uI, p))))); |
275 overwrite (ps, (cI ,(cs, overwrite (us, (uI, p))))); |
279 case assoc (Synchronized.value states, cI) of |
279 case assoc (Synchronized.value states, cI) of |
280 NONE => error ... |
280 NONE => error ... |
281 | SOME (_, us) => |
281 | SOME (_, us) => |
282 Synchronized.change states (fn s => overwrite ...) |
282 Synchronized.change states (fn s => overwrite ...) |
283 *) |
283 *) |
284 fun upd_calc (cI:calcID) cs = Synchronized.change states |
284 fun upd_calc (cI: Celem.calcID) cs = Synchronized.change states |
285 (fn s => case assoc (s, cI) of |
285 (fn s => case assoc (s, cI) of |
286 NONE => error ("upd_calc " ^ (string_of_int cI) ^ " not existent") |
286 NONE => error ("upd_calc " ^ (string_of_int cI) ^ " not existent") |
287 | SOME (_, us) => overwrite (s, (cI, (cs, us)))); |
287 | SOME (_, us) => overwrite (s, (cI, (cs, us)))); |
288 (*WN051210 testing before initac: only 1 taci in calcstate so far: |
288 (*WN051210 testing before initac: only 1 taci in calcstate so far: |
289 fun upd_calc (cI:calcID) (cs as (_, tacis):calcstate) = |
289 fun upd_calc (cI:calcID) (cs as (_, tacis):calcstate) = |
299 (*///7.10. |
299 (*///7.10. |
300 fun upd_tacis (uI:iterID) (pI:calcID) tacis = |
300 fun upd_tacis (uI:iterID) (pI:calcID) tacis = |
301 let val (p, (ptp,_)) = get_state uI pI |
301 let val (p, (ptp,_)) = get_state uI pI |
302 in states:= |
302 in states:= |
303 overwrite2 ((!states), ((uI, pI), (p, (ptp, tacis)))) end;*) |
303 overwrite2 ((!states), ((uI, pI), (p, (ptp, tacis)))) end;*) |
304 fun upd_tacis (cI:calcID) tacis = Synchronized.change states |
304 fun upd_tacis (cI: Celem.calcID) tacis = Synchronized.change states |
305 (fn s => case assoc (s, cI) of |
305 (fn s => case assoc (s, cI) of |
306 NONE => |
306 NONE => |
307 error ("upd_tacis: calctree " ^ (string_of_int cI) ^ " not existent") |
307 error ("upd_tacis: calctree " ^ (string_of_int cI) ^ " not existent") |
308 | SOME ((ptp, _), us) => overwrite (s, (cI, ((ptp, tacis), us)))); |
308 | SOME ((ptp, _), us) => overwrite (s, (cI, ((ptp, tacis), us)))); |
309 (*///7.10. |
309 (*///7.10. |
310 fun upd_ipos (uI:iterID) (pI:calcID) (ip:pos') = |
310 fun upd_ipos (uI:iterID) (pI:calcID) (ip:pos') = |
311 let val (_, calc) = get_state uI pI |
311 let val (_, calc) = get_state uI pI |
312 in states:= overwrite2 ((!states), ((uI, pI), (ip, calc))) end;*) |
312 in states:= overwrite2 ((!states), ((uI, pI), (ip, calc))) end;*) |
313 fun upd_ipos (cI:calcID) (uI:iterID) (ip: Ctree.pos') = Synchronized.change states |
313 fun upd_ipos (cI: Celem.calcID) (uI: Celem.iterID) (ip: Ctree.pos') = Synchronized.change states |
314 (fn s => case assoc (s, cI) of |
314 (fn s => case assoc (s, cI) of |
315 NONE => |
315 NONE => |
316 error ("upd_ipos: calctree " ^ (string_of_int cI) ^ " not existent") |
316 error ("upd_ipos: calctree " ^ (string_of_int cI) ^ " not existent") |
317 | SOME (cs, us) => overwrite2 (s, ((cI, uI), ip))); |
317 | SOME (cs, us) => overwrite2 (s, ((cI, uI), ip))); |
318 |
318 |
341 (*///7.10 |
341 (*///7.10 |
342 fun add_calc (uI:iterID) (s:state) = |
342 fun add_calc (uI:iterID) (s:state) = |
343 let val (new_calcID, new_calcs) = add_pID uI s (!states) |
343 let val (new_calcID, new_calcs) = add_pID uI s (!states) |
344 in states:= new_calcs; |
344 in states:= new_calcs; |
345 new_calcID end; *) |
345 new_calcID end; *) |
346 fun add_user (cI:calcID) = Synchronized.change_result states |
346 fun add_user (cI: Celem.calcID) = Synchronized.change_result states |
347 (fn s => case assoc (s, cI) of |
347 (fn s => case assoc (s, cI) of |
348 NONE => |
348 NONE => |
349 error ("add_user: calctree " ^ (string_of_int cI) ^ " not existent") |
349 error ("add_user: calctree " ^ (string_of_int cI) ^ " not existent") |
350 | SOME (cs, us) => |
350 | SOME (cs, us) => |
351 let |
351 let |
352 val new_uI = new_key us 1 |
352 val new_uI = new_key us 1 |
353 in (new_uI:iterID, overwrite2 (s, ((cI, new_uI), Ctree.e_pos'))) end); |
353 in (new_uI: Celem.iterID, overwrite2 (s, ((cI, new_uI), Ctree.e_pos'))) end); |
354 |
354 |
355 (*///10.10. |
355 (*///10.10. |
356 fun del_calc (uI:iterID) (pI:calcID) = |
356 fun del_calc (uI:iterID) (pI:calcID) = |
357 (states:= del_assoc2 uI pI (!states); pI);*) |
357 (states:= del_assoc2 uI pI (!states); pI);*) |
358 fun del_user (cI:calcID) (uI:iterID) = |
358 fun del_user (cI: Celem.calcID) (uI: Celem.iterID) = |
359 Synchronized.change_result states (fn s => (uI, del_assoc2 cI uI s)); |
359 Synchronized.change_result states (fn s => (uI, del_assoc2 cI uI s)); |
360 |
360 |
361 |
361 |
362 (** add and delete calculations **) |
362 (** add and delete calculations **) |
363 |
363 |
364 (* here is the _only_ critical section on states, |
364 (* here is the _only_ critical section on states, |
365 because a single calculation (with _one_ cI) is sequential *) |
365 because a single calculation (with _one_ cI) is sequential *) |
366 fun add_calc (cs: Chead.calcstate) = Synchronized.change_result states |
366 fun add_calc (cs: Chead.calcstate) = Synchronized.change_result states |
367 (fn s => |
367 (fn s => |
368 let val new_cI = new_key s 1 |
368 let val new_cI = new_key s 1 |
369 in (new_cI:calcID, s @ [(new_cI, (cs, []))]) end); |
369 in (new_cI: Celem.calcID, s @ [(new_cI, (cs, []))]) end); |
370 |
370 |
371 (* delete doesn't report non existing elements *) |
371 (* delete doesn't report non existing elements *) |
372 (*///7.10 |
372 (*///7.10 |
373 fun del_user (uI:userID) = |
373 fun del_user (uI:userID) = |
374 (states:= del_assoc (!states, uI); uI);*) |
374 (states:= del_assoc (!states, uI); uI);*) |
375 fun del_calc (cI:calcID) = Synchronized.change_result states |
375 fun del_calc (cI: Celem.calcID) = Synchronized.change_result states |
376 (fn s => (cI:calcID, del_assoc (s, cI))); |
376 (fn s => (cI: Celem.calcID, del_assoc (s, cI))); |
377 |
377 |
378 (* -------------- test all exported funs -------------- |
378 (* -------------- test all exported funs -------------- |
379 ///7.10 |
379 ///7.10 |
380 Compiler.Control.Print.printDepth:=8; |
380 Compiler.Control.Print.printDepth:=8; |
381 states:=[]; |
381 states:=[]; |