@@ -0,0 +1,541 @@
3+import Language.Reflection.Utils
9+{- A resource is a pair of a label and the current type stored there -}
11+data Resource : Type where
12+ MkRes : label -> Type -> Resource
16+(:::) : label -> Type -> Resource
20+data Var = MkVar -- Phantom, just for labelling purposes
22+{- Contexts for holding current resources states -}
25+ data Context : Type where
27+ (::) : Resource -> Context -> Context
30+ (++) : Context -> Context -> Context
32+ (++) (x :: xs) ys = x :: xs ++ ys
34+{- Proof that a label has a particular type in a given context -}
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)
40+{- Update an entry in a context with a new state -}
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
47+{- Remove an entry from a context -}
49+drop : (ctxt : Context) -> (prf : InState lbl st ctxt) ->
51+drop (MkRes lbl st :: rs) Here = rs
52+drop (r :: rs) (There p) = r :: drop rs p
54+{- Proof that a resource state (label/type) is in a context -}
56+data ElemCtxt : Resource -> Context -> Type where
57+ HereCtxt : ElemCtxt a (a :: as)
58+ ThereCtxt : ElemCtxt a as -> ElemCtxt a (b :: as)
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
65+{- Proof that a variable name is in a context -}
67+data VarInCtxt : Var -> Context -> Type where
68+ VarHere : VarInCtxt a (MkRes a st :: as)
69+ VarThere : VarInCtxt a as -> VarInCtxt a (b :: as)
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
77+data Composite : List Type -> Type where
78+ CompNil : Composite []
79+ CompCons : (x : a) -> Composite as -> Composite (a :: as)
83+ data VarList : List Type -> Type where
85+ (::) : Var -> VarList ts -> VarList (t :: ts)
88+ mkCtxt : VarList tys -> Context
90+ mkCtxt {tys = (t :: ts)} (v :: vs) = (v ::: t) :: mkCtxt vs
92+{- Proof that a context is a subset of another context -}
94+data SubCtxt : Context -> Context -> Type where
95+ SubNil : SubCtxt [] []
96+ InCtxt : (el : ElemCtxt x ys) -> SubCtxt xs (dropEl ys el) ->
98+ Skip : SubCtxt xs ys -> SubCtxt xs (y :: ys)
102+subCtxtId : SubCtxt xs xs
103+subCtxtId {xs = []} = SubNil
104+subCtxtId {xs = (x :: xs)} = InCtxt HereCtxt subCtxtId
107+subCtxtNil : SubCtxt [] xs
108+subCtxtNil {xs = []} = SubNil
109+subCtxtNil {xs = (x :: xs)} = Skip subCtxtNil
111+{- Proof that every variable in the list appears once in the context -}
113+data VarsIn : List Var -> Context -> Type where
114+ VarsNil : VarsIn [] []
115+ InCtxtVar : (el : VarInCtxt x ys) -> VarsIn xs (dropVarIn ys el) ->
117+ SkipVar : VarsIn xs ys -> VarsIn xs (y :: ys)
120+Uninhabited (ElemCtxt x []) where
121+ uninhabited HereCtxt impossible
122+ uninhabited (ThereCtxt _) impossible
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
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
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
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
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
163+ data Env : Context -> Type where
165+ (::) : ty -> Env xs -> Env ((lbl ::: ty) :: xs)
167+lookupEnv : InState lbl ty ctxt -> Env ctxt -> ty
168+lookupEnv Here (x :: xs) = x
169+lookupEnv (There p) (x :: xs) = lookupEnv p xs
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
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
180+envElem : ElemCtxt x xs -> Env xs -> Env [x]
181+envElem HereCtxt (x :: xs) = [x]
182+envElem (ThereCtxt p) (x :: xs) = envElem p xs
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
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
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
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
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
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
214+{- Some things to make STrans interfaces look prettier -}
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
226+ public export %error_reduce
227+ (:::) : lbl -> Type -> Action ty
232+ data Trans ty = (:->) Type Type
234+ public export %error_reduce
235+ (:::) : lbl -> Trans ty -> Action ty
236+ (:::) lbl (st :-> st') = Trans lbl st (const st')
240+ data DepTrans ty = (:->) Type (ty -> Type)
242+ public export %error_reduce
243+ (:::) : lbl -> DepTrans ty -> Action ty
244+ (:::) lbl (st :-> st') = Trans lbl st st'
247+or : a -> a -> Either b c -> a
248+or x y = either (const x) (const y)
251+add : Type -> Action a
252+add ty = Add (\var => [var ::: ty])
255+addIfRight : Type -> Action (Either a b)
256+addIfRight ty = Add (either (const []) (\var => [var ::: ty]))
259+addIfJust : Type -> Action (Maybe a)
260+addIfJust ty = Add (maybe [] (\var => [var ::: ty]))
263+kept : SubCtxt xs ys -> Context
265+kept (InCtxt el p) = kept p
266+kept (Skip {y} p) = y :: kept p
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
272+data State : Type -> Type where
273+ Value : ty -> State ty
276+data STrans : (m : Type -> Type) ->
278+ Context -> (ty -> Context) ->
280+ Pure : (result : ty) ->
281+ STrans m ty (out_fn result) out_fn
282+ Bind : STrans m a st1 st2_fn ->
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)
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))
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) ->
304+ (const (combineVarsIn ctxt prf))
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)
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) ->
315+ STrans m () ctxt (const (updateCtxt ctxt prf ty'))
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
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
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
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
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')
357+ mkVars : Composite ts -> VarList ts
359+ mkVars (CompCons x xs) = MkVar :: mkVars xs
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
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)
374+pure : (result : ty) -> STrans m ty (out_fn result) out_fn
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
384+lift : Monad m => m t -> STrans m t ctxt (const ctxt)
388+new : (val : state) ->
389+ STrans m Var ctxt (\lbl => (lbl ::: State state) :: ctxt)
390+new val = New (Value val)
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
398+-- Keep only a subset of the current set of resources. Returns the
399+-- environment corresponding to the dropped portion.
401+dropSubCtxt : {auto prf : SubCtxt ys xs} ->
402+ STrans m (Env ys) xs (const (kept prf))
403+dropSubCtxt {prf} = DropSubCtxt prf
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
414+combine : (comp : Var) -> (vs : List Var) ->
415+ {auto prf : InState comp (State ()) ctxt} ->
416+ {auto var_prf : VarsIn (comp :: vs) ctxt} ->
418+ (const (combineVarsIn ctxt var_prf))
419+combine comp vs {var_prf} = Combine comp vs var_prf
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
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
435+write : (lbl : Var) ->
436+ {auto prf : InState lbl ty ctxt} ->
438+ STrans m () ctxt (const (updateCtxt ctxt prf (State ty')))
439+write lbl {prf} val = Write lbl prf (Value val)
441+public export %error_reduce
442+out_res : ty -> (as : List (Action ty)) -> Context
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
450+public export %error_reduce
451+in_res : (as : List (Action ty)) -> Context
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
459+%error_reduce -- always evaluate this before showing errors
460+ST : (m : Type -> Type) ->
462+ List (Action ty) -> Type
463+ST m ty xs = STrans m ty (in_res xs) (\result : ty => out_res result xs)
465+-- Console IO is useful sufficiently often that let's have it here
467+interface ConsoleIO (m : Type -> Type) where
468+ putStr : String -> STrans m () xs (const xs)
469+ getStr : STrans m String xs (const xs)
473+ putStr str = lift (Interactive.putStr str)
474+ getStr = lift Interactive.getLine
478+run : Applicative m => ST m a [] -> m a
479+run prog = runST [] prog (\res, env' => pure res)
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.
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'))
495+runPure : ST Basics.id a [] -> a
496+runPure prog = runST [] prog (\res, env' => res)
498+%language ErrorReflection
502+st_precondition : Err -> Maybe (List ErrorReportPart)
503+st_precondition (CantSolveGoal `(SubCtxt ~sub ~all) _)
505+ [TextPart "'call' is not valid here. ",
506+ TextPart "The operation has preconditions ",
508+ TextPart " which is not a sub set of ",
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
520+ getPreconditions : TT -> Maybe TT
521+ getPreconditions `(STrans ~m ~ret ~pre ~post) = Just pre
522+ getPreconditions _ = Nothing
524+ getPostconditions : TT -> Maybe TT
525+ getPostconditions `(STrans ~m ~ret ~pre ~post) = Just post
526+ getPostconditions _ = Nothing
528+ renderPre : TT -> TT -> List (ErrorReportPart)
530+ = [SubReport [TextPart "Operation has preconditions: ",
532+ SubReport [TextPart "States here are: ",
534+ renderPost : TT -> TT -> List (ErrorReportPart)
536+ = [SubReport [TextPart "Operation has postconditions: ",
538+ SubReport [TextPart "Required result states here are: ",
541+st_precondition _ = Nothing