wneuper/isa: src/Tools/isac/Frontend/states.sml@255c853ea2f0

     1 (* states for calculation in global refs

     2    use"../states.sml";

     3    use"states.sml";

     4    *)

     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;

    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 *)

    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*)

    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 *)

    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 *)

   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;

   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 ----------------------------------------*)

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

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

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

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

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

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

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

   148   ) list)) list);

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

   151 (*

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

   153 			    (3,e_pos')])),

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

   155 			    (2,e_pos')]))];

   156 *)

   158 (** create new instances of users and ptrees

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

   161 (* add users *)

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

   163   NONE => n

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

   165 (*///10.10

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

   167     (new_key u 1):calcID;*)

   168 (*

   169 val new_iterID = get_calcID (!states);

   170 val it = 1 : int

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

   172 !states;

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

   174 *)

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

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

   178   case assoc (p, uI) of

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

   180 			  (string_of_int uI))

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

   182 > get_calcID 1 (!states);

   183 val it = 1 : calcID

   184 *)

   185 (* add users to a calcstate *)

   186 fun get_iterID (cI:calcID)

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

   188   case assoc (p, cI) of

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

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

   191 (* get_iterID 3 (!states);

   192 val it = 2 : iterID*)

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

   197 (*//////7.10.

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

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

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

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

   202 > get_cal 3 1 (!states);

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

   204 *)

   206 (*///7.10.

   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);

   209 *)

   210 fun get_calc  (cI:calcID) =

   211     case assoc (Synchronized.value states, cI) of

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

   213       | SOME (c, _) => c;

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

   215     case assoc (Synchronized.value states, cI) of

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

   217 			     ^ " not existent")

   218       | SOME (_, us) =>

   219 	(case assoc (us, uI) of

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

   221 				 ^ " not existent")

   222 	  | SOME p => p);

   225 fun del_assoc ([],_) = []

   226   | del_assoc a =

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

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

   229     if key = keyi then ps @ pairs

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

   231   in del a [] end;

   232 (*

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

   234 > del_assoc (ps,3);

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

   236 *)

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

   239 (*/////7.10.

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

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

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

   243 (*

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

   245 > !states;

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

   248 > del_user 3;

   249 > !states;

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

   251 *)

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

   253     case assoc (ps, cI) of

   254 	NONE => ps

   255       | SOME (cs, us) =>

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

   257 (*

   258 > del_assoc2 4 1 (!states);

   259 val it =

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

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

   263 (*///7.10.

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

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

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

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

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

   269   end;*)

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

   271     case assoc (ps, cI) of

   272 	NONE =>

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

   274       | SOME (cs, us) =>

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

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

   278   fun upd_calc cI cs =

   279     case assoc (Synchronized.value states, cI) of

   280       NONE => error ...

   281     | SOME (_, us) =>

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

   283 *)

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

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

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

   287           | SOME (_, us) => overwrite (s, (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 error ("upd_calc, |tacis|>1: "^tacis2str tacis)

   292      else ();

   293     case assoc (!states, cI) of

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

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

   296 			);*)

   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 = Synchronized.change states

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

   306 	          NONE =>

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

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

   309 (*///7.10.

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

   311    let val (_, calc) = get_state uI pI

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

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

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

   315 	          NONE =>

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

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

   320 (** add and delete calcs **)

   322 (*///7.10

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

   324   let val new_ID = get_calcID uI p;

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

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

   327 (*

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

   329 > states:= new_states;

   330 > !states;

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

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

   333 > states:= new_states;

   334 > !states;

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

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

   337 val it = SOME EmptyPtree : ctree option

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

   339 val it = NONE : ctree option

   340 *)

   341 (*///7.10

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

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

   344     in states:= new_calcs;

   345     new_calcID end; *)

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

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

   348 	          NONE =>

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

   350           | SOME (cs, us) =>

   351 	            let

   352                 val new_uI = new_key us 1

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

   355 (*///10.10.

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

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

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

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

   362 (** add and delete calculations **)

   364 (* here is the _only_ critical section on states,

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

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

   367         (fn s =>

   368             let val new_cI = new_key s 1

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

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

   372 (*///7.10

   373 fun del_user (uI:userID) =

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

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

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

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

   379 ///7.10

   380 Compiler.Control.Print.printDepth:=8;

   381 states:=[];

   382 add_user (); add_user (); !states;

   383 ML> val it = 1 : userID

   384 ML> val it = 2 : userID

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

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

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

   389 add_calc 1 e_state;

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

   391 ML> val it = 1 : calcID

   392 ML> val it = 2 : calcID

   393 ML> val it =

   394   [(1,

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

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

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

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

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

   401 ML> val it =

   402   [(1,

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

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

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

   407 get_state 1 1; get_state 1 2;

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

   409 ML> val it =

   410   (((Nd

   411        (PblObj

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

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

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

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

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

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

   420 del_user 1; !states;

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

   423 add_user (); add_user (); !states;

   424 ML> val it = 1 : userID

   425 ML> val it = 3 : userID

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

   427 *)

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

   431 print_depth 9;

   432 states:=[];

   433 add_calc e_calcstate; add_calc e_calcstate; !states;

   434 |val it = 1 : calcID

   435 |val it = 2 : calcID

   436 |val it =

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

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

   440 add_user 2; add_user 2; !states;

   441 |val it = 1 : userID

   442 |val it = 2 : userID

   443 |val it =

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

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

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

   449 upd_calc 1 cs; !states;

   450 |val it =

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

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

   454 get_calc 1; get_calc 2;

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

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

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

   459 |val it = 3 : userID

   460 |val it = 1 : userID

   461 |val it =

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

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

   465 del_calc 1; !states;

   466 |val it = 1 : calcID

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

   469 add_calc e_calcstate; add_calc e_calcstate; !states;

   470 |val it = 1 : calcID

   471 |val it = 3 : calcID

   472 |val it =

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

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

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

   477 add_user 2; !states;

   478 |val it =

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

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

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

   482 *)

author	Walther Neuper <wneuper@ist.tugraz.at>
	Thu, 22 Dec 2016 11:36:20 +0100
changeset 59279	255c853ea2f0
parent 59276	56dc790071cb
child 59405	49d7d410b83c
permissions	-rw-r--r--