(* states for calculation in global refs

   use"../states.sml";

   use"states.sml";

   *)

(*

type hide = (pblID * 

	     string list * (*hide: tacs + 

					  "ALL",       .. result immediately

					  "MODELPBL",  .. modeling hidden

					  "SPEC",      .. specifying hidden

		                          "MODELMET",  .. (additional itms !)

					  "APPLY",     .. solving hidden

		                    detail: rls

				   "Rewrite_*" (as strings) must _not_ be ..

				   .. contained in this list, rls _only_ !*)

		    bool)         (*inherit to children in pbl-herarchy*)

	       list;

(*. points a pbl/metID to a sub-hierarchy of key ?.*)

fun is_child_of child key =

    let fun is_ch [] [] = true     (*is child of itself*)

	  | is_ch (c::_) [] = true

	  | is_ch [] (k::_) = false

	  | is_ch (c::cs) (k::ks) = 

	    if c = k then is_ch cs ks else false

    in is_ch (rev child) (rev key) end;

(*

is_child_of ["root'","univar","equation"] ["univar","equation"];

val it = true : bool

is_child_of ["root'","univar","equation"] ["system","equation"];

val it = false : bool

is_child_of ["equation"] ["system","equation"];

val it = false : bool

is_child_of ["root'","univar","equation"] ["linear","univar","equation"];

val it = false : bool

*)

(*.what tactics have to be hidden (in model/specify these may be several).*)

datatype hid = 

	 Show      (**)

       | Hundef	   (**)

       | Htac	   (*a tactic has to be hidden*)

       | Hmodel	   (*the model of the (sub)problem has to be hidden*)

       | Hspecify  (*the specification of the (sub)problem has to be hidden*)

       | Happly;   (*solving the (sub)problem has to be hidden*)

(*. search all pbls if there is some tactic or model/spec/calc to hide .*)

fun is_hid pblID arg [] = Show

  | is_hid pblID arg ((pblID', strs, inherit)::pts) = 

    let fun is_mem arg = 

	    if arg mem strs then Htac

	    else if arg mem ["Add_Given","Add_Find","Add_Relation"] 

		    andalso "MODEL" mem strs then Hmodel

	    else if arg mem ["Specify_Theory","Specify_Problem",

			     "Specify_Method"] 

		    andalso "SPEC" mem strs then Hspecify

	    else if "APPLY" mem strs then Htac 

	    else Hundef

    in if inherit then

	   if is_child_of (pblID:pblID) pblID' 

	   then case is_mem arg of Hundef => is_hid pblID arg (pts:hide)

				 | hid => hid

	   else is_hid pblID arg pts

       else if pblID = pblID' 

       then case is_mem arg of Hundef => is_hid pblID arg (pts:hide)

			     | hid => hid

       else is_hid pblID arg pts

    end;

(*val hide = [([],["Refine_Tacitly"],true),

	    (["univar","equation"],["Apply_Method","Model_Problem","SPEC"],

	     false)]

	   :hide;

is_hid [] "Rewrite" hide;

val it = Show

is_hid ["any","problem"] "Refine_Tacitly" hide;

val it = Htac

is_hid ["root'","univar","equation"] "Apply_Method" hide;

val it = Show

is_hid ["univar","equation"] "Apply_Method" hide;

val it = Htac

is_hid ["univar","equation"] "Specify_Problem" hide;

val it = Hspecify

*)

fun is_hide pblID (tac as (Subproblem (_,pI))) (det:detail) = 

    is_hid pblID "SELF" det

  | is_hide pblID (tac as (Rewrite (thmID,_))) det = 

    is_hid pblID thmID det

  | is_hide pblID (tac as (Rewrite_Inst (_,(thmID,_)))) det = 

    is_hid pblID thmID det

  | is_hide pblID (tac as (Rewrite_Set rls)) det = 

    is_hid pblID rls det

  | is_hide pblID (tac as (Rewrite_Set_Inst (_,rls))) det = 

    is_hid pblID rls det

  | is_hide pblID tac det = is_hid pblID (tac2IDstr tac) det;

(*val hide = [([],["Refine_Tacitly"],true),

	    (["univar","equation"],["Apply_Method","Model_Problem",

				    "SPEC","SELF"],

	     false)]

	   :hide;

is_hide [] (Rewrite ("","")) hide;

val it = Show

is_hide ["any","problem"] (Refine_Tacitly []) hide;

val it = Htac

is_hide ["root'","univar","equation"] (Apply_Method []) hide;

val it = Show

is_hide ["univar","equation"] (Apply_Method []) hide;

val it = Htac

is_hide ["univar","equation"] (Specify_Problem []) hide;

val it = Hspecify

is_hide ["univar","equation"] (Subproblem (e_domID,["univar","equation"]))hide;

val it = Htac

is_hide ["equation"] (Subproblem (e_domID,["univar","equation"]))hide;

val it = Show

*)

(*. search all pbls in detail if there is some rls' to be detailed .*)

fun is_det pblID arg [] = false

  | is_det pblID arg ((pblID', rlss, inherit)::pts) = 

    if inherit then

	   if is_child_of (pblID:pblID) pblID' 

	   then if arg mem rlss then true

		else is_det pblID arg (pts:detail)

	   else is_det pblID arg pts

       else if pblID = pblID' 

	   then if arg mem rlss then true

		else is_det pblID arg (pts:detail)

       else is_det pblID arg pts;

(*fun is_detail pblID (tac as (Subproblem (_,pI))) (det:detail) = 

    is_det pblID "SELF" det*)

fun is_detail pblID (tac as (Rewrite_Set rls)) det = 

    is_det pblID rls det

  | is_detail pblID (tac as (Rewrite_Set_Inst (_,rls))) det = 

    is_det pblID rls det

  | is_detail _ _ _ = false;

----------------------------------------*)

(* holds calculations; these are read/updated from the java-frontend at each interaction*)

val states = Synchronized.var "isac_states" ([] :

  (calcID *            (* the id unique for a calculation                               *)

    (Chead.calcstate * (* the interpreter state                                         *) 

      (iterID *        (* 1 sets the 'active formula': a calc. can have several visitors*)

        Ctree.pos'     (* for iterator of a user                                        *)

      (* TODO iterID * pos' should go to java-frontend                                  *)

  ) list)) list);

fun reset_states () = Synchronized.change states (fn _ => []);

(*

states:= [(3,(e_calcstate, [(1,e_pos'),

			    (3,e_pos')])),

	  (4,(e_calcstate, [(1,e_pos'),

			    (2,e_pos')]))];

*)

(** create new instances of users and ptrees

   new keys are the lowest possible in the association list **)

(* add users *)

fun new_key u n = case assoc (u, n) of 

  NONE => n 

| SOME _ => new_key u (n+1);

(*///10.10

fun get_calcID (u:(calcID * (calcstate * (iterID * pos') list)) list) = 

    (new_key u 1):calcID;*)

(*

val new_iterID = get_calcID (!states);

val it = 1 : int

states:= (!states) @ [(new_iterID, [])];

!states;

val it = [(3,[(#,#),(#,#)]),(4,[(#,#),(#,#)]),(1,[])]

*)

(*///7.10.03/// add states to a users active states

fun get_calcID (uI:iterID) (p:(iterID * (calcID * state) list) list) = 

  case assoc (p, uI) of 

    NONE => error ("get_calcID: no iterID " ^ 

			  (string_of_int uI))

  | SOME ps => (new_key ps 1):calcID;

> get_calcID 1 (!states);  

val it = 1 : calcID

*)

(* add users to a calcstate *)

fun get_iterID (cI:calcID) 

	       (p:(calcID * (Chead.calcstate * (iterID * Ctree.pos') list)) list) = 

  case assoc (p, cI) of

    NONE => error ("get_iterID: no iterID " ^ (string_of_int cI))

  | SOME (_, us) => (new_key us 1):iterID;

(* get_iterID 3 (!states);

val it = 2 : iterID*)

(** retrieve, update, delete a state by iterID, calcID **)

(*//////7.10.

fun get_cal (uI:iterID) (pI:calcID) (p:(iterID * (calcID * state) list) list) =

  (the (assoc2 (p,(uI, pI)))) 

  handle _ => error ("get_state " ^ (string_of_int uI) ^

			     " " ^ (string_of_int pI) ^ " not existent");

> get_cal 3 1 (!states);

val it = (((EmptyPtree,(#,#)),[]),([],[])) : state

*)

(*///7.10.

fun get_state (uI:iterID) (pI:calcID) = get_cal uI pI (!states);

fun get_calc  (uI:iterID) (pI:calcID) = (snd o (get_cal uI pI)) (!states);

*)

fun get_calc  (cI:calcID) = 

    case assoc (Synchronized.value states, cI) of 

	NONE => error ("get_calc "^(string_of_int cI)^" not existent")

      | SOME (c, _) => c;

fun get_pos (cI:calcID) (uI:iterID) = 

    case assoc (Synchronized.value states, cI) of 

	NONE => error ("get_pos: calc " ^ (string_of_int cI) 

			     ^ " not existent")

      | SOME (_, us) => 

	(case assoc (us, uI) of 

	    NONE => error ("get_pos: user " ^ (string_of_int uI) 

				 ^ " not existent")

	  | SOME p => p);

fun del_assoc ([],_) = []

  | del_assoc a =

  let fun del ([], key) ps = ps

	| del ((keyi, xi) :: pairs, key) ps =

    if key = keyi then ps @ pairs

    else del (pairs, key) (ps @ [(keyi, xi)])

  in del a [] end;

(*

> val ps =  [(1,"1"),(2,"2"),(3,"3"),(4,"4")];     

> del_assoc (ps,3);

val it = [(1,"1"),(2,"2"),(4,"4")] : (int * string) list

*)

(* delete doesn't report non existing elements *)

(*/////7.10.

fun del_assoc2 (uI:iterID) (pI:calcID) ps =

  let val new_ps = del_assoc (the (assoc (ps, uI)), pI)

  in overwrite (ps, (uI, new_ps)) end;*)

(*

> states:= del_assoc2 4 41 (!states);

> !states;

val it = [(3,[(#,#),(#,#),(#,#)]),(4,[(#,#)]),(1,[(#,#)])] : states

> del_user 3;

> !states;

val it = [(4,[(#,#)]),(1,[(#,#)])] : states

*)

fun del_assoc2 (cI:calcID) (uI:iterID) ps =

    case assoc (ps, cI) of

	NONE => ps

      | SOME (cs, us) => 

	overwrite (ps, (cI, (cs, del_assoc (us, uI))));

(*

> del_assoc2 4 1 (!states);

val it =

   [(3, (((EmptyPtree, ([], Und)), []), [(1, ([], Und)), (3, ([], Und))])),

    (4, (((EmptyPtree, ([], Und)), []), [(2, ([], Und))]))]*)

(*///7.10.

fun overwrite2 (ps, (((uI:iterID), (pI:calcID)), p)) = 

  let val new_ps = overwrite (the (assoc (ps, uI)), (pI, p))

  in (overwrite (ps, (uI, new_ps)))

    handle _ => error ("overwrite2 " ^ (string_of_int uI) ^

			      " " ^ (string_of_int pI) ^ " not existent")

  end;*)

fun overwrite2 (ps, (((cI:calcID), (uI:iterID)), p)) =

    case assoc (ps, cI) of

	NONE => 

	error ("overwrite2: calc " ^ (string_of_int uI) ^" not existent")

      | SOME (cs, us) =>

	overwrite (ps, (cI ,(cs, overwrite (us, (uI, p)))));

(* here is _no_ critical section on states; sufficient would be

  fun upd_calc cI cs =

    case assoc (Synchronized.value states, cI) of

      NONE => error ...

    | SOME (_, us) => 

      Synchronized.change states (fn s => overwrite ...)

*)

fun upd_calc (cI:calcID) cs = Synchronized.change states

        (fn s => case assoc (s, cI) of 

	          NONE => error ("upd_calc " ^ (string_of_int cI) ^ " not existent")

          | SOME (_, us) => overwrite (s, (cI, (cs, us))));

(*WN051210 testing before initac: only 1 taci in calcstate so far:

fun upd_calc (cI:calcID) (cs as (_, tacis):calcstate) =

    (if length tacis > 1 

     then error ("upd_calc, |tacis|>1: "^tacis2str tacis) 

     else ();

    case assoc (!states, cI) of 

	NONE => error ("upd_calc "^(string_of_int cI)^" not existent")

      | SOME (_, us) => states:= overwrite (!states, (cI, (cs, us)))

			);*)

(*///7.10.

fun upd_tacis (uI:iterID) (pI:calcID) tacis =

   let val (p, (ptp,_)) = get_state uI pI 

   in states:= 

      overwrite2 ((!states), ((uI, pI), (p, (ptp, tacis)))) end;*)

fun upd_tacis (cI:calcID) tacis = Synchronized.change states

        (fn s => case assoc (s, cI) of 

	          NONE => 

	            error ("upd_tacis: calctree " ^ (string_of_int cI) ^ " not existent")

          | SOME ((ptp, _), us) => overwrite (s, (cI, ((ptp, tacis), us))));

(*///7.10.

fun upd_ipos (uI:iterID) (pI:calcID) (ip:pos') =

   let val (_, calc) = get_state uI pI 

   in states:= overwrite2 ((!states), ((uI, pI), (ip, calc))) end;*)

fun upd_ipos (cI:calcID) (uI:iterID) (ip: Ctree.pos') = Synchronized.change states

        (fn s => case assoc (s, cI) of 

	          NONE =>

	            error ("upd_ipos: calctree " ^ (string_of_int cI) ^ " not existent")

          | SOME (cs, us) => overwrite2 (s, ((cI, uI), ip)));

(** add and delete calcs **)

(*///7.10

fun add_pID (uI:iterID) (s:state) (p:(iterID * (calcID * state) list) list) = 

  let val new_ID = get_calcID uI p;

    val new_states = (the (assoc (p, uI))) @ [(new_ID, s)];

  in (new_ID, (overwrite (p, (uI, new_states)))) end;*)

(*

> val (new_calcID, new_states) = add_pID 1 (!states);

> states:= new_states;

> !states;

val it = [(3,[(#,#),(#,#)]),(4,[(#,#),(#,#)]),(1,[(#,#)])] : states

> val (new_calcID, new_states) = add_pID 3 (!states);

> states:= new_states;

> !states;

val it = [(3,[(#,#),(#,#),(#,#)]),(4,[(#,#),(#,#)]),(1,[(#,#)])] : states

> assoc2 (!states, (3, 1));

val it = SOME EmptyPtree : ctree option

> assoc2 (!states, (3, 2));

val it = NONE : ctree option

*)

(*///7.10

fun add_calc (uI:iterID) (s:state) = 

    let val (new_calcID, new_calcs) = add_pID uI s (!states)

    in states:= new_calcs; 

    new_calcID end; *)

fun add_user (cI:calcID) = Synchronized.change_result states

        (fn s => case assoc (s, cI) of 

	          NONE =>

	            error ("add_user: calctree " ^ (string_of_int cI) ^ " not existent")

          | SOME (cs, us) =>

	            let

                val new_uI = new_key us 1

	            in (new_uI:iterID, overwrite2 (s, ((cI, new_uI), Ctree.e_pos'))) end);

(*///10.10.

fun del_calc (uI:iterID) (pI:calcID) = 

    (states:= del_assoc2 uI pI (!states); pI);*)

fun del_user (cI:calcID) (uI:iterID) =

      Synchronized.change_result states (fn s => (uI, del_assoc2 cI uI s));

(** add and delete calculations **)

(* here is the _only_ critical section on states,

  because a single calculation (with _one_ cI) is sequential *)

fun add_calc (cs: Chead.calcstate) = Synchronized.change_result states

        (fn s =>

            let val new_cI = new_key s 1

            in (new_cI:calcID, s @ [(new_cI, (cs, []))]) end);

(* delete doesn't report non existing elements *)

(*///7.10

fun del_user (uI:userID) = 

    (states:= del_assoc (!states, uI); uI);*)

fun del_calc (cI:calcID) = Synchronized.change_result states

        (fn s => (cI:calcID, del_assoc (s, cI)));

(* -------------- test all exported funs -------------- 

///7.10

Compiler.Control.Print.printDepth:=8;

states:=[];

add_user (); add_user (); !states;

ML> val it = 1 : userID

ML> val it = 2 : userID

ML> val it = [(1,[]),(2,[])]

val (hide,detail) = ([(["pI"],["tac"],true)]:hide,

		       [(["pI"],["tac"],true)]:detail);

add_calc 1 e_state; 

add_calc 1 (e_calcstate,(hide,detail)); !states;

ML> val it = 1 : calcID

ML> val it = 2 : calcID

ML> val it =

  [(1,

    [(1,(((EmptyPtree,(#,#)),[]),([],[]))),

     (2,(((EmptyPtree,(#,#)),[]),([(#,#,#)],[(#,#,#)])))]),(2,[])]

val (pt,(p,p_)) = (EmptyPtree,e_pos');

val (pt,_) = cappend_problem pt p Uistate ([],e_spec);

upd_calc 1 2 ((pt,(p,p_)),[]); !states;

ML> val it =

  [(1,

    [(1,(((EmptyPtree,(#,#)),[]),([],[]))),

     (2,(((Nd #,(#,#)),[]),([(#,#,#)],[(#,#,#)])))]),(2,[])]

(*                          ~~~~~~~~~~~~~~~~~~~~ unchanged !!!*)

get_state 1 1; get_state 1 2;

ML> val it = (((EmptyPtree,([],Und)),[]),([],[])) : state

ML> val it =

  (((Nd

       (PblObj

          {branch=NoBranch,cell=[],env=(#,#,#,#),loc=(#,#),meth=[],

           model={Find=#,Given=#,Relate=#,Where=#,With=#},origin=(#,#),

           ostate=Incomplete,probl=[],result=(#,#),spec=(#,#,#)},[]),([],Und)),

    []),([(["pI"],["tac"],true)],[(["pI"],["tac"],true)])) : state

del_calc 2 1 (*non existent - NO msg!*); del_calc 1 2; !states;

ML> val it = [(1,[(1,(((EmptyPtree,(#,#)),[]),([],[])))]),(2,[])]

del_user 1; !states;

ML> val it = [(2,[])]

add_user (); add_user (); !states;

ML> val it = 1 : userID

ML> val it = 3 : userID

ML> val it = [(2,[]),(1,[]),(3,[])]

*)

(* -------------- test all exported funs -------------- 

print_depth 9;

states:=[];

add_calc e_calcstate; add_calc e_calcstate; !states;

|val it = 1 : calcID

|val it = 2 : calcID

|val it =

|   [(1, (((EmptyPtree, ([], Und)), []), [])),

|      (2, (((EmptyPtree, ([], Und)), []), []))]

add_user 2; add_user 2; !states; 

|val it = 1 : userID

|val it = 2 : userID

|val it =

|   [(1, (((EmptyPtree, ([], Und)), []), [])),

|      (2, (((EmptyPtree, ([], Und)), []), [(1, ([], Und)), (2, ([], Und))]))]

val cs = ((EmptyPtree, ([111], Und)), []) : calcstate;

upd_calc 1 cs; !states;

|val it =

|   [(1, (((EmptyPtree, ([111], Und)), []), [])),

|      (2, (((EmptyPtree, ([], Und)), []), [(1, ([], Und)), (2, ([], Und))]))]   

get_calc 1; get_calc 2;

|val it = ((EmptyPtree, ([111], Und)), []) : calcstate

|val it = ((EmptyPtree, ([], Und)), []) : calcstate

del_user 2 3 (*non existent - NO msg!*); del_user 2 1; !states;

|val it = 3 : userID

|val it = 1 : userID

|val it =

|   [(1, (((EmptyPtree, ([111], Und)), []), [])),

|      (2, (((EmptyPtree, ([], Und)), []), [(2, ([], Und))]))]

del_calc 1; !states;

|val it = 1 : calcID

|val it = [(2, (((EmptyPtree, ([], Und)), []), [(2, ([], Und))]))]

add_calc e_calcstate; add_calc e_calcstate; !states;

|val it = 1 : calcID

|val it = 3 : calcID

|val it =

|   [(2, (((EmptyPtree, ([], Und)), []), [(2, ([], Und))])),

|      (1, (((EmptyPtree, ([], Und)), []), [])),

|      (3, (((EmptyPtree, ([], Und)), []), []))]

add_user 2; !states;

|val it =

|   [(2, (((EmptyPtree, ([], Und)), []), [(2, ([], Und)), (1, ([], Und))])),

|      (1, (((EmptyPtree, ([], Und)), []), [])),

|      (3, (((EmptyPtree, ([], Und)), []), []))]

*)