@@ -0,0 +1,541 @@
1+module Control.ST
2+
3+import Language.Reflection.Utils
4+
5+%default total
6+
7+infix 5 :::
8+
9+{- A resource is a pair of a label and the current type stored there -}
10+public export
11+data Resource : Type where
12+ MkRes : label -> Type -> Resource
13+
14+%error_reverse
15+public export
16+(:::) : label -> Type -> Resource
17+(:::) = MkRes
18+
19+export
20+data Var = MkVar -- Phantom, just for labelling purposes
21+
22+{- Contexts for holding current resources states -}
23+namespace Context
24+ public export
25+ data Context : Type where
26+ Nil : Context
27+ (::) : Resource -> Context -> Context
28+
29+ public export
30+ (++) : Context -> Context -> Context
31+ (++) [] ys = ys
32+ (++) (x :: xs) ys = x :: xs ++ ys
33+
34+{- Proof that a label has a particular type in a given context -}
35+public export
36+data InState : lbl -> Type -> Context -> Type where
37+ Here : InState lbl st (MkRes lbl st :: rs)
38+ There : InState lbl st rs -> InState lbl st (r :: rs)
39+
40+{- Update an entry in a context with a new state -}
41+public export
42+updateCtxt : (ctxt : Context) ->
43+ InState lbl st ctxt -> Type -> Context
44+updateCtxt (MkRes lbl _ :: rs) Here val = (MkRes lbl val :: rs)
45+updateCtxt (r :: rs) (There x) ty = r :: updateCtxt rs x ty
46+
47+{- Remove an entry from a context -}
48+public export
49+drop : (ctxt : Context) -> (prf : InState lbl st ctxt) ->
50+ Context
51+drop (MkRes lbl st :: rs) Here = rs
52+drop (r :: rs) (There p) = r :: drop rs p
53+
54+{- Proof that a resource state (label/type) is in a context -}
55+public export
56+data ElemCtxt : Resource -> Context -> Type where
57+ HereCtxt : ElemCtxt a (a :: as)
58+ ThereCtxt : ElemCtxt a as -> ElemCtxt a (b :: as)
59+
60+public export %error_reduce
61+dropEl : (ys: _) -> ElemCtxt x ys -> Context
62+dropEl (x :: as) HereCtxt = as
63+dropEl (x :: as) (ThereCtxt p) = x :: dropEl as p
64+
65+{- Proof that a variable name is in a context -}
66+public export
67+data VarInCtxt : Var -> Context -> Type where
68+ VarHere : VarInCtxt a (MkRes a st :: as)
69+ VarThere : VarInCtxt a as -> VarInCtxt a (b :: as)
70+
71+public export %error_reduce
72+dropVarIn : (ys: _) -> VarInCtxt x ys -> Context
73+dropVarIn ((MkRes x _) :: as) VarHere = as
74+dropVarIn (x :: as) (VarThere p) = x :: dropVarIn as p
75+
76+public export
77+data Composite : List Type -> Type where
78+ CompNil : Composite []
79+ CompCons : (x : a) -> Composite as -> Composite (a :: as)
80+
81+namespace VarList
82+ public export
83+ data VarList : List Type -> Type where
84+ Nil : VarList []
85+ (::) : Var -> VarList ts -> VarList (t :: ts)
86+
87+ public export
88+ mkCtxt : VarList tys -> Context
89+ mkCtxt [] = []
90+ mkCtxt {tys = (t :: ts)} (v :: vs) = (v ::: t) :: mkCtxt vs
91+
92+{- Proof that a context is a subset of another context -}
93+public export
94+data SubCtxt : Context -> Context -> Type where
95+ SubNil : SubCtxt [] []
96+ InCtxt : (el : ElemCtxt x ys) -> SubCtxt xs (dropEl ys el) ->
97+ SubCtxt (x :: xs) ys
98+ Skip : SubCtxt xs ys -> SubCtxt xs (y :: ys)
99+
100+%hint
101+public export
102+subCtxtId : SubCtxt xs xs
103+subCtxtId {xs = []} = SubNil
104+subCtxtId {xs = (x :: xs)} = InCtxt HereCtxt subCtxtId
105+
106+public export
107+subCtxtNil : SubCtxt [] xs
108+subCtxtNil {xs = []} = SubNil
109+subCtxtNil {xs = (x :: xs)} = Skip subCtxtNil
110+
111+{- Proof that every variable in the list appears once in the context -}
112+public export
113+data VarsIn : List Var -> Context -> Type where
114+ VarsNil : VarsIn [] []
115+ InCtxtVar : (el : VarInCtxt x ys) -> VarsIn xs (dropVarIn ys el) ->
116+ VarsIn (x :: xs) ys
117+ SkipVar : VarsIn xs ys -> VarsIn xs (y :: ys)
118+
119+public export
120+Uninhabited (ElemCtxt x []) where
121+ uninhabited HereCtxt impossible
122+ uninhabited (ThereCtxt _) impossible
123+
124+public export %error_reduce
125+updateWith : (new : Context) -> (xs : Context) ->
126+ SubCtxt ys xs -> Context
127+-- At the end, add the ones which were updated by the subctxt
128+updateWith new [] SubNil = new
129+updateWith new [] (InCtxt el z) = absurd el
130+-- Don't add the ones which were consumed by the subctxt
131+updateWith [] (x :: xs) (InCtxt el p)
132+ = updateWith [] (dropEl _ el) p
133+updateWith (n :: ns) (x :: xs) (InCtxt el p)
134+ = n :: updateWith ns (dropEl _ el) p
135+-- Do add the ones we didn't use in the subctxt
136+updateWith new (x :: xs) (Skip p) = x :: updateWith new xs p
137+
138+public export
139+getVarType : (xs : Context) -> VarInCtxt v xs -> Type
140+getVarType ((MkRes v st) :: as) VarHere = st
141+getVarType (b :: as) (VarThere x) = getVarType as x
142+
143+public export
144+getCombineType : VarsIn ys xs -> List Type
145+getCombineType VarsNil = []
146+getCombineType (InCtxtVar el y) = getVarType _ el :: getCombineType y
147+getCombineType (SkipVar x) = getCombineType x
148+
149+public export
150+dropCombined : VarsIn vs ctxt -> Context
151+dropCombined {ctxt = []} VarsNil = []
152+dropCombined {ctxt} (InCtxtVar el y) = dropCombined y
153+dropCombined {ctxt = (y :: ys)} (SkipVar x) = y :: dropCombined x
154+
155+public export
156+combineVarsIn : (ctxt : Context) -> VarsIn (comp :: vs) ctxt -> Context
157+combineVarsIn {comp} ctxt (InCtxtVar el x)
158+ = ((comp ::: Composite (getCombineType x)) :: dropCombined (InCtxtVar el x))
159+combineVarsIn (y :: ys) (SkipVar x) = y :: combineVarsIn ys x
160+
161+namespace Env
162+ public export
163+ data Env : Context -> Type where
164+ Nil : Env []
165+ (::) : ty -> Env xs -> Env ((lbl ::: ty) :: xs)
166+
167+lookupEnv : InState lbl ty ctxt -> Env ctxt -> ty
168+lookupEnv Here (x :: xs) = x
169+lookupEnv (There p) (x :: xs) = lookupEnv p xs
170+
171+updateEnv : (prf : InState lbl ty ctxt) -> Env ctxt -> ty' ->
172+ Env (updateCtxt ctxt prf ty')
173+updateEnv Here (x :: xs) val = val :: xs
174+updateEnv (There p) (x :: xs) val = x :: updateEnv p xs val
175+
176+dropVal : (prf : InState lbl st ctxt) -> Env ctxt -> Env (drop ctxt prf)
177+dropVal Here (x :: xs) = xs
178+dropVal (There p) (x :: xs) = x :: dropVal p xs
179+
180+envElem : ElemCtxt x xs -> Env xs -> Env [x]
181+envElem HereCtxt (x :: xs) = [x]
182+envElem (ThereCtxt p) (x :: xs) = envElem p xs
183+
184+dropDups : Env xs -> (el : ElemCtxt x xs) -> Env (dropEl xs el)
185+dropDups (y :: ys) HereCtxt = ys
186+dropDups (y :: ys) (ThereCtxt p) = y :: dropDups ys p
187+
188+
189+dropEntry : Env ctxt -> (prf : VarInCtxt x ctxt) -> Env (dropVarIn ctxt prf)
190+dropEntry (x :: env) VarHere = env
191+dropEntry (x :: env) (VarThere y) = x :: dropEntry env y
192+
193+dropVarsIn : Env ctxt -> (prf : VarsIn vs ctxt) -> Env (dropCombined prf)
194+dropVarsIn [] VarsNil = []
195+dropVarsIn env (InCtxtVar el z) = dropVarsIn (dropEntry env el) z
196+dropVarsIn (x :: env) (SkipVar z) = x :: dropVarsIn env z
197+
198+getVarEntry : Env ctxt -> (prf : VarInCtxt v ctxt) -> getVarType ctxt prf
199+getVarEntry (x :: xs) VarHere = x
200+getVarEntry (x :: env) (VarThere p) = getVarEntry env p
201+
202+mkComposite : Env ctxt -> (prf : VarsIn vs ctxt) -> Composite (getCombineType prf)
203+mkComposite [] VarsNil = CompNil
204+mkComposite env (InCtxtVar el z)
205+ = CompCons (getVarEntry env el) (mkComposite (dropEntry env el) z)
206+mkComposite (x :: env) (SkipVar z) = mkComposite env z
207+
208+rebuildVarsIn : Env ctxt -> (prf : VarsIn (comp :: vs) ctxt) ->
209+ Env (combineVarsIn ctxt prf)
210+rebuildVarsIn env (InCtxtVar el p)
211+ = mkComposite (dropEntry env el) p :: dropVarsIn env (InCtxtVar el p)
212+rebuildVarsIn (x :: env) (SkipVar p) = x :: rebuildVarsIn env p
213+
214+{- Some things to make STrans interfaces look prettier -}
215+
216+infix 6 :->
217+
218+public export
219+data Action : Type -> Type where
220+ Stable : lbl -> Type -> Action ty
221+ Trans : lbl -> Type -> (ty -> Type) -> Action ty
222+ Remove : lbl -> Type -> Action ty
223+ Add : (ty -> Context) -> Action ty
224+
225+namespace Stable
226+ public export %error_reduce
227+ (:::) : lbl -> Type -> Action ty
228+ (:::) = Stable
229+
230+namespace Trans
231+ public export
232+ data Trans ty = (:->) Type Type
233+
234+ public export %error_reduce
235+ (:::) : lbl -> Trans ty -> Action ty
236+ (:::) lbl (st :-> st') = Trans lbl st (const st')
237+
238+namespace DepTrans
239+ public export
240+ data DepTrans ty = (:->) Type (ty -> Type)
241+
242+ public export %error_reduce
243+ (:::) : lbl -> DepTrans ty -> Action ty
244+ (:::) lbl (st :-> st') = Trans lbl st st'
245+
246+public export
247+or : a -> a -> Either b c -> a
248+or x y = either (const x) (const y)
249+
250+public export
251+add : Type -> Action a
252+add ty = Add (\var => [var ::: ty])
253+
254+public export
255+addIfRight : Type -> Action (Either a b)
256+addIfRight ty = Add (either (const []) (\var => [var ::: ty]))
257+
258+public export
259+addIfJust : Type -> Action (Maybe a)
260+addIfJust ty = Add (maybe [] (\var => [var ::: ty]))
261+
262+public export
263+kept : SubCtxt xs ys -> Context
264+kept SubNil = []
265+kept (InCtxt el p) = kept p
266+kept (Skip {y} p) = y :: kept p
267+
268+-- We can only use new/delete/read/write on things wrapped in State. Only an
269+-- interface implementation should know that a thing is defined as State,
270+-- so it's the only thing that's able to peek at the internals
271+public export
272+data State : Type -> Type where
273+ Value : ty -> State ty
274+
275+export
276+data STrans : (m : Type -> Type) ->
277+ (ty : Type) ->
278+ Context -> (ty -> Context) ->
279+ Type where
280+ Pure : (result : ty) ->
281+ STrans m ty (out_fn result) out_fn
282+ Bind : STrans m a st1 st2_fn ->
283+ ((result : a) ->
284+ STrans m b (st2_fn result) st3_fn) ->
285+ STrans m b st1 st3_fn
286+ Lift : Monad m => m t -> STrans m t ctxt (const ctxt)
287+
288+ New : (val : state) ->
289+ STrans m Var ctxt (\lbl => (lbl ::: state) :: ctxt)
290+ Delete : (lbl : Var) ->
291+ (prf : InState lbl st ctxt) ->
292+ STrans m () ctxt (const (drop ctxt prf))
293+ DropSubCtxt : (prf : SubCtxt ys xs) ->
294+ STrans m (Env ys) xs (const (kept prf))
295+
296+ Split : (lbl : Var) ->
297+ (prf : InState lbl (Composite vars) ctxt) ->
298+ STrans m (VarList vars) ctxt
299+ (\ vs => mkCtxt vs ++
300+ updateCtxt ctxt prf (State ()))
301+ Combine : (comp : Var) -> (vs : List Var) ->
302+ (prf : VarsIn (comp :: vs) ctxt) ->
303+ STrans m () ctxt
304+ (const (combineVarsIn ctxt prf))
305+
306+ Call : STrans m t sub new_f -> (ctxt_prf : SubCtxt sub old) ->
307+ STrans m t old (\res => updateWith (new_f res) old ctxt_prf)
308+
309+ Read : (lbl : Var) ->
310+ (prf : InState lbl ty ctxt) ->
311+ STrans m ty ctxt (const ctxt)
312+ Write : (lbl : Var) ->
313+ (prf : InState lbl ty ctxt) ->
314+ (val : ty') ->
315+ STrans m () ctxt (const (updateCtxt ctxt prf ty'))
316+
317+export
318+dropEnv : Env ys -> SubCtxt xs ys -> Env xs
319+dropEnv [] SubNil = []
320+dropEnv [] (InCtxt idx rest) = absurd idx
321+dropEnv (z :: zs) (InCtxt idx rest)
322+ = let [e] = envElem idx (z :: zs) in
323+ e :: dropEnv (dropDups (z :: zs) idx) rest
324+dropEnv (z :: zs) (Skip p) = dropEnv zs p
325+
326+keepEnv : Env ys -> (prf : SubCtxt xs ys) -> Env (kept prf)
327+keepEnv env SubNil = env
328+keepEnv env (InCtxt el prf) = keepEnv (dropDups env el) prf
329+keepEnv (z :: zs) (Skip prf) = z :: keepEnv zs prf
330+
331+-- Corresponds pretty much exactly to 'updateWith'
332+rebuildEnv : Env new -> Env old -> (prf : SubCtxt sub old) ->
333+ Env (updateWith new old prf)
334+rebuildEnv new [] SubNil = new
335+rebuildEnv new [] (InCtxt el p) = absurd el
336+rebuildEnv [] (x :: xs) (InCtxt el p)
337+ = rebuildEnv [] (dropDups (x :: xs) el) p
338+rebuildEnv (e :: es) (x :: xs) (InCtxt el p)
339+ = e :: rebuildEnv es (dropDups (x :: xs) el) p
340+rebuildEnv new (x :: xs) (Skip p) = x :: rebuildEnv new xs p
341+
342+runST : Env invars -> STrans m a invars outfn ->
343+ ((x : a) -> Env (outfn x) -> m b) -> m b
344+runST env (Pure result) k = k result env
345+runST env (Bind prog next) k
346+ = runST env prog (\prog', env' => runST env' (next prog') k)
347+runST env (Lift action) k
348+ = do res <- action
349+ k res env
350+runST env (New val) k = k MkVar (val :: env)
351+runST env (Delete lbl prf) k = k () (dropVal prf env)
352+runST env (DropSubCtxt prf) k = k (dropEnv env prf) (keepEnv env prf)
353+runST env (Split lbl prf) k = let val = lookupEnv prf env
354+ env' = updateEnv prf env (Value ()) in
355+ k (mkVars val) (addToEnv val env')
356+ where
357+ mkVars : Composite ts -> VarList ts
358+ mkVars CompNil = []
359+ mkVars (CompCons x xs) = MkVar :: mkVars xs
360+
361+ addToEnv : (comp : Composite ts) -> Env xs -> Env (mkCtxt (mkVars comp) ++ xs)
362+ addToEnv CompNil env = env
363+ addToEnv (CompCons x xs) env = x :: addToEnv xs env
364+runST env (Combine lbl vs prf) k = k () (rebuildVarsIn env prf)
365+runST env (Call prog ctxt_prf) k
366+ = let env' = dropEnv env ctxt_prf in
367+ runST env' prog
368+ (\prog', envk => k prog' (rebuildEnv envk env ctxt_prf))
369+runST env (Read lbl prf) k = k (lookupEnv prf env) env
370+runST env (Write lbl prf val) k = k () (updateEnv prf env val)
371+
372+
373+export
374+pure : (result : ty) -> STrans m ty (out_fn result) out_fn
375+pure = Pure
376+
377+export
378+(>>=) : STrans m a st1 st2_fn ->
379+ ((result : a) -> STrans m b (st2_fn result) st3_fn) ->
380+ STrans m b st1 st3_fn
381+(>>=) = Bind
382+
383+export
384+lift : Monad m => m t -> STrans m t ctxt (const ctxt)
385+lift = Lift
386+
387+export
388+new : (val : state) ->
389+ STrans m Var ctxt (\lbl => (lbl ::: State state) :: ctxt)
390+new val = New (Value val)
391+
392+export
393+delete : (lbl : Var) ->
394+ {auto prf : InState lbl (State st) ctxt} ->
395+ STrans m () ctxt (const (drop ctxt prf))
396+delete lbl {prf} = Delete lbl prf
397+
398+-- Keep only a subset of the current set of resources. Returns the
399+-- environment corresponding to the dropped portion.
400+export
401+dropSubCtxt : {auto prf : SubCtxt ys xs} ->
402+ STrans m (Env ys) xs (const (kept prf))
403+dropSubCtxt {prf} = DropSubCtxt prf
404+
405+export
406+split : (lbl : Var) ->
407+ {auto prf : InState lbl (Composite vars) ctxt} ->
408+ STrans m (VarList vars) ctxt
409+ (\ vs => mkCtxt vs ++
410+ updateCtxt ctxt prf (State ()))
411+split lbl {prf} = Split lbl prf
412+
413+export
414+combine : (comp : Var) -> (vs : List Var) ->
415+ {auto prf : InState comp (State ()) ctxt} ->
416+ {auto var_prf : VarsIn (comp :: vs) ctxt} ->
417+ STrans m () ctxt
418+ (const (combineVarsIn ctxt var_prf))
419+combine comp vs {var_prf} = Combine comp vs var_prf
420+
421+export -- implicit ???
422+call : STrans m t sub new_f ->
423+ {auto ctxt_prf : SubCtxt sub old} ->
424+ STrans m t old (\res => updateWith (new_f res) old ctxt_prf)
425+call prog {ctxt_prf} = Call prog ctxt_prf
426+
427+export
428+read : (lbl : Var) ->
429+ {auto prf : InState lbl (State ty) ctxt} ->
430+ STrans m ty ctxt (const ctxt)
431+read lbl {prf} = do Value x <- Read lbl prf
432+ pure x
433+
434+export
435+write : (lbl : Var) ->
436+ {auto prf : InState lbl ty ctxt} ->
437+ (val : ty') ->
438+ STrans m () ctxt (const (updateCtxt ctxt prf (State ty')))
439+write lbl {prf} val = Write lbl prf (Value val)
440+
441+public export %error_reduce
442+out_res : ty -> (as : List (Action ty)) -> Context
443+out_res x [] = []
444+out_res x ((Stable lbl inr) :: xs) = (lbl ::: inr) :: out_res x xs
445+out_res x ((Trans lbl inr outr) :: xs)
446+ = (lbl ::: outr x) :: out_res x xs
447+out_res x ((Remove lbl inr) :: xs) = out_res x xs
448+out_res x (Add outf :: xs) = outf x ++ out_res x xs
449+
450+public export %error_reduce
451+in_res : (as : List (Action ty)) -> Context
452+in_res [] = []
453+in_res ((Stable lbl inr) :: xs) = (lbl ::: inr) :: in_res xs
454+in_res ((Trans lbl inr outr) :: xs) = (lbl ::: inr) :: in_res xs
455+in_res ((Remove lbl inr) :: xs) = (lbl ::: inr) :: in_res xs
456+in_res (Add outf :: xs) = in_res xs
457+
458+public export
459+%error_reduce -- always evaluate this before showing errors
460+ST : (m : Type -> Type) ->
461+ (ty : Type) ->
462+ List (Action ty) -> Type
463+ST m ty xs = STrans m ty (in_res xs) (\result : ty => out_res result xs)
464+
465+-- Console IO is useful sufficiently often that let's have it here
466+public export
467+interface ConsoleIO (m : Type -> Type) where
468+ putStr : String -> STrans m () xs (const xs)
469+ getStr : STrans m String xs (const xs)
470+
471+export
472+ConsoleIO IO where
473+ putStr str = lift (Interactive.putStr str)
474+ getStr = lift Interactive.getLine
475+
476+
477+export
478+run : Applicative m => ST m a [] -> m a
479+run prog = runST [] prog (\res, env' => pure res)
480+
481+||| runWith allows running an STrans program with an initial environment,
482+||| which must be consumed.
483+||| It's only allowed in the IO monad, because it's inherently unsafe, so
484+||| we don't want to be able to use it under a 'lift in just *any* ST program -
485+||| if we have access to an 'Env' we can easily duplicate it - so it's the
486+||| responsibility of an implementation of an interface in IO which uses it
487+||| to ensure that it isn't duplicated.
488+export
489+runWith : {ctxtf : _} ->
490+ Env ctxt -> STrans IO a ctxt (\res => ctxtf res) ->
491+ IO (res ** Env (ctxtf res))
492+runWith env prog = runST env prog (\res, env' => pure (res ** env'))
493+
494+export
495+runPure : ST Basics.id a [] -> a
496+runPure prog = runST [] prog (\res, env' => res)
497+
498+%language ErrorReflection
499+
500+%error_handler
501+export
502+st_precondition : Err -> Maybe (List ErrorReportPart)
503+st_precondition (CantSolveGoal `(SubCtxt ~sub ~all) _)
504+ = pure
505+ [TextPart "'call' is not valid here. ",
506+ TextPart "The operation has preconditions ",
507+ TermPart sub,
508+ TextPart " which is not a sub set of ",
509+ TermPart all]
510+st_precondition (CantUnify _ tm1 tm2 _ _ _)
511+ = do reqPre <- getPreconditions tm1
512+ gotPre <- getPreconditions tm2
513+ reqPost <- getPostconditions tm1
514+ gotPost <- getPostconditions tm2
515+ pure $ [TextPart "Error in state transition:"] ++
516+ renderPre gotPre reqPre ++
517+ renderPost gotPost reqPost
518+
519+ where
520+ getPreconditions : TT -> Maybe TT
521+ getPreconditions `(STrans ~m ~ret ~pre ~post) = Just pre
522+ getPreconditions _ = Nothing
523+
524+ getPostconditions : TT -> Maybe TT
525+ getPostconditions `(STrans ~m ~ret ~pre ~post) = Just post
526+ getPostconditions _ = Nothing
527+
528+ renderPre : TT -> TT -> List (ErrorReportPart)
529+ renderPre got req
530+ = [SubReport [TextPart "Operation has preconditions: ",
531+ TermPart req],
532+ SubReport [TextPart "States here are: ",
533+ TermPart got]]
534+ renderPost : TT -> TT -> List (ErrorReportPart)
535+ renderPost got req
536+ = [SubReport [TextPart "Operation has postconditions: ",
537+ TermPart req],
538+ SubReport [TextPart "Required result states here are: ",
539+ TermPart got]]
540+
541+st_precondition _ = Nothing