wneuper/isa: src/Tools/isac/Frontend/states.sml@460c24a6a6ba

     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 type iterID = int;

   142 type calcID = int;

   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 = Unsynchronized.ref ([]:(iterID * (calcID * state) list) list);

   150 *)

   152 val states = Unsynchronized.ref

   153         ([]:(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 *)

   165 (** create new instances of users and ptrees

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

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

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

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

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

   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 => 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 => error ("get_pos: calc " ^ (string_of_int cI)

   224 			     ^ " not existent")

   225       | SOME (_, us) =>

   226 	(case assoc (us, uI) of

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

   228 				 ^ " not existent")

   229 	  | SOME p => p);

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

   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

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

   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 _ => 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 	error ("overwrite2: calc " ^ (string_of_int uI) ^" not existent")

   281       | SOME (cs, us) =>

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

   284 fun upd_calc (cI:calcID) cs =

   285     case assoc (!states, cI) of

   286 	NONE => 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 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 =

   305     case assoc (!states, cI) of

   306 	NONE =>

   307 	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 	error ("upd_ipos: calctree "^(string_of_int cI)^" not existent")

   318       | SOME (cs, us) =>

   319 	states:= overwrite2 (!states, ((cI, uI), ip));

   322 (** add and delete calcs **)

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

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

   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;

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

   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,[])]

   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,[])]

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

   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

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

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

   425 del_user 1; !states;

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

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

   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)), []), []))]

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

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

   459 get_calc 1; get_calc 2;

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

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

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

   470 del_calc 1; !states;

   471 |val it = 1 : calcID

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

   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)), []), []))]

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

author	Walther Neuper <neuper@ist.tugraz.at>
	Tue, 28 Sep 2010 09:06:56 +0200
branch	isac-update-Isa09-2
changeset 38031	460c24a6a6ba
parent 38007	d679c1f837a7
child 55432	1780e9905d80
permissions	-rw-r--r--