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