library States version 0.0

%% CASL States
%% A. Nonymous

spec Stateful[sort S][sort D] =
   free type St[S,D] ::= st(state: S; data: D)
end

spec Unit = 
   free type Unit ::=  *
end

spec Maybe[sort S] =
   free type Maybe[S] ::= just(val :? S) | nothing
end

spec Ref[sort State][sort Elem] = 
   Stateful[sort State][sort Elem]
and
   Stateful[sort State][sort Unit]
then
   sorts Ref[Elem]
then
   Stateful[sort State][sort Ref[Elem]]
then 
   ops
      newRef : State* Elem            -> St[State,Ref[Elem]];
      getRef : State* Ref[Elem]       -> St[State,Elem];
      setRef : State* Ref[Elem]* Elem -> St[State,Unit];

   forall s, s', s'', s''': State; r, r1, r2: Ref[Elem]; a, b: Elem
   . newRef(s, a) = st(s', r1) /\ newRef(s', b)= st(s'', r2)
      => not (r1= r2) 
   . newRef(s, a) = st(s', r1) => data(getRef(s', r1))= a
   . data(getRef(state(setRef(s, r, a)), r))= a
   . data(getRef(state(setRef(s, r1, a)), r2))= data(getRef(s, r2)) 
                                                if not(r1= r2)
   . setRef(state(setRef(s, r, a)), r, b)  = setRef(s, r, b)
   . setRef(state(setRef(s, r1, a)), r2, b)= 
     setRef(state(setRef(s, r2, b)), r1, a)     if not (r1= r2)
end


spec LocalStateArg = 
   sorts S, X, Y
then Stateful[sort S][sort X]
 and Stateful[sort S][sort Y]
then ops f:St[S,X]-> St[S,Y] 
end     

spec LocalState [LocalStateArg] =
   ops run[f]: X-> Y
   forall x:X. exists s: S
   . run[f](x) = data(f(st(s, x))) 
end