git.iko.soy/Idris-dev
on master help sign in
Finish Ctxt->Res update
601bef0Edwin Brady
libs/contrib/Control/ST.idr+139−139
compare with master
unifiedsplit
@@ -39,37 +39,37 @@ data InState : lbl -> Type -> Resources -> Type where
39
39
40{- Update an entry in a context with a new state -}
40{- Update an entry in a context with a new state -}
41public export
41public export
42−updateCtxt : (ctxt : Resources) ->
42+updateRes : (res : Resources) ->
43− InState lbl st ctxt -> Type -> Resources
43+ InState lbl st res -> Type -> Resources
44−updateCtxt (MkRes lbl _ :: rs) Here val = (MkRes lbl val :: rs)
44+updateRes (MkRes lbl _ :: rs) Here val = (MkRes lbl val :: rs)
45−updateCtxt (r :: rs) (There x) ty = r :: updateCtxt rs x ty
45+updateRes (r :: rs) (There x) ty = r :: updateRes rs x ty
46
46
47{- Remove an entry from a context -}
47{- Remove an entry from a context -}
48public export
48public export
49−drop : (ctxt : Resources) -> (prf : InState lbl st ctxt) ->
49+drop : (res : Resources) -> (prf : InState lbl st res) ->
50 Resources
50 Resources
51drop (MkRes lbl st :: rs) Here = rs
51drop (MkRes lbl st :: rs) Here = rs
52drop (r :: rs) (There p) = r :: drop rs p
52drop (r :: rs) (There p) = r :: drop rs p
53
53
54{- Proof that a resource state (label/type) is in a context -}
54{- Proof that a resource state (label/type) is in a context -}
55public export
55public export
56−data ElemCtxt : Resource -> Resources -> Type where
56+data ElemRes : Resource -> Resources -> Type where
57− HereCtxt : ElemCtxt a (a :: as)
57+ HereRes : ElemRes a (a :: as)
58− ThereCtxt : ElemCtxt a as -> ElemCtxt a (b :: as)
58+ ThereRes : ElemRes a as -> ElemRes a (b :: as)
59
59
60public export %error_reduce
60public export %error_reduce
61−dropEl : (ys: _) -> ElemCtxt x ys -> Resources
61+dropEl : (ys: _) -> ElemRes x ys -> Resources
62−dropEl (x :: as) HereCtxt = as
62+dropEl (x :: as) HereRes = as
63−dropEl (x :: as) (ThereCtxt p) = x :: dropEl as p
63+dropEl (x :: as) (ThereRes p) = x :: dropEl as p
64
64
65{- Proof that a variable name is in a context -}
65{- Proof that a variable name is in a context -}
66public export
66public export
67−data VarInCtxt : Var -> Resources -> Type where
67+data VarInRes : Var -> Resources -> Type where
68− VarHere : VarInCtxt a (MkRes a st :: as)
68+ VarHere : VarInRes a (MkRes a st :: as)
69− VarThere : VarInCtxt a as -> VarInCtxt a (b :: as)
69+ VarThere : VarInRes a as -> VarInRes a (b :: as)
70
70
71public export %error_reduce
71public export %error_reduce
72−dropVarIn : (ys: _) -> VarInCtxt x ys -> Resources
72+dropVarIn : (ys: _) -> VarInRes x ys -> Resources
73dropVarIn ((MkRes x _) :: as) VarHere = as
73dropVarIn ((MkRes x _) :: as) VarHere = as
74dropVarIn (x :: as) (VarThere p) = x :: dropVarIn as p
74dropVarIn (x :: as) (VarThere p) = x :: dropVarIn as p
75
75
@@ -85,77 +85,77 @@ namespace VarList
85 (::) : Var -> VarList ts -> VarList (t :: ts)
85 (::) : Var -> VarList ts -> VarList (t :: ts)
86
86
87 public export
87 public export
88− mkCtxt : VarList tys -> Resources
88+ mkRes : VarList tys -> Resources
89− mkCtxt [] = []
89+ mkRes [] = []
90− mkCtxt {tys = (t :: ts)} (v :: vs) = (v ::: t) :: mkCtxt vs
90+ mkRes {tys = (t :: ts)} (v :: vs) = (v ::: t) :: mkRes vs
91
91
92−{- Proof that a context is a subset of another context -}
92+{- Proof that a list of resources is a subset of another list -}
93public export
93public export
94−data SubCtxt : Resources -> Resources -> Type where
94+data SubRes : Resources -> Resources -> Type where
95− SubNil : SubCtxt [] []
95+ SubNil : SubRes [] []
96− Skip : SubCtxt xs ys -> SubCtxt xs (y :: ys)
96+ Skip : SubRes xs ys -> SubRes xs (y :: ys)
97− InCtxt : (el : ElemCtxt x ys) -> SubCtxt xs (dropEl ys el) ->
97+ InRes : (el : ElemRes x ys) -> SubRes xs (dropEl ys el) ->
98− SubCtxt (x :: xs) ys
98+ SubRes (x :: xs) ys
99
99
100%hint
100%hint
101public export
101public export
102−subCtxtId : SubCtxt xs xs
102+subResId : SubRes xs xs
103−subCtxtId {xs = []} = SubNil
103+subResId {xs = []} = SubNil
104−subCtxtId {xs = (x :: xs)} = InCtxt HereCtxt subCtxtId
104+subResId {xs = (x :: xs)} = InRes HereRes subResId
105
105
106public export
106public export
107−subCtxtNil : SubCtxt [] xs
107+subResNil : SubRes [] xs
108−subCtxtNil {xs = []} = SubNil
108+subResNil {xs = []} = SubNil
109−subCtxtNil {xs = (x :: xs)} = Skip subCtxtNil
109+subResNil {xs = (x :: xs)} = Skip subResNil
110
110
111{- Proof that every variable in the list appears once in the context -}
111{- Proof that every variable in the list appears once in the context -}
112public export
112public export
113data VarsIn : List Var -> Resources -> Type where
113data VarsIn : List Var -> Resources -> Type where
114 VarsNil : VarsIn [] []
114 VarsNil : VarsIn [] []
115 SkipVar : VarsIn xs ys -> VarsIn xs (y :: ys)
115 SkipVar : VarsIn xs ys -> VarsIn xs (y :: ys)
116− InCtxtVar : (el : VarInCtxt x ys) -> VarsIn xs (dropVarIn ys el) ->
116+ InResVar : (el : VarInRes x ys) -> VarsIn xs (dropVarIn ys el) ->
117 VarsIn (x :: xs) ys
117 VarsIn (x :: xs) ys
118
118
119public export
119public export
120−Uninhabited (ElemCtxt x []) where
120+Uninhabited (ElemRes x []) where
121− uninhabited HereCtxt impossible
121+ uninhabited HereRes impossible
122− uninhabited (ThereCtxt _) impossible
122+ uninhabited (ThereRes _) impossible
123
123
124public export %error_reduce
124public export %error_reduce
125updateWith : (new : Resources) -> (xs : Resources) ->
125updateWith : (new : Resources) -> (xs : Resources) ->
126− SubCtxt ys xs -> Resources
126+ SubRes ys xs -> Resources
127-- At the end, add the ones which were updated by the subctxt
127-- At the end, add the ones which were updated by the subctxt
128updateWith new [] SubNil = new
128updateWith new [] SubNil = new
129−updateWith new [] (InCtxt el z) = absurd el
129+updateWith new [] (InRes el z) = absurd el
130-- Don't add the ones which were consumed by the subctxt
130-- Don't add the ones which were consumed by the subctxt
131−updateWith [] (x :: xs) (InCtxt el p)
131+updateWith [] (x :: xs) (InRes el p)
132 = updateWith [] (dropEl _ el) p
132 = updateWith [] (dropEl _ el) p
133-- A new item corresponding to an existing thing
133-- A new item corresponding to an existing thing
134−updateWith (n :: ns) (x :: xs) (InCtxt el p)
134+updateWith (n :: ns) (x :: xs) (InRes el p)
135 = n :: updateWith ns (dropEl _ el) p
135 = n :: updateWith ns (dropEl _ el) p
136updateWith new (x :: xs) (Skip p) = x :: updateWith new xs p
136updateWith new (x :: xs) (Skip p) = x :: updateWith new xs p
137
137
138public export
138public export
139−getVarType : (xs : Resources) -> VarInCtxt v xs -> Type
139+getVarType : (xs : Resources) -> VarInRes v xs -> Type
140getVarType ((MkRes v st) :: as) VarHere = st
140getVarType ((MkRes v st) :: as) VarHere = st
141getVarType (b :: as) (VarThere x) = getVarType as x
141getVarType (b :: as) (VarThere x) = getVarType as x
142
142
143public export
143public export
144getCombineType : VarsIn ys xs -> List Type
144getCombineType : VarsIn ys xs -> List Type
145getCombineType VarsNil = []
145getCombineType VarsNil = []
146−getCombineType (InCtxtVar el y) = getVarType _ el :: getCombineType y
146+getCombineType (InResVar el y) = getVarType _ el :: getCombineType y
147getCombineType (SkipVar x) = getCombineType x
147getCombineType (SkipVar x) = getCombineType x
148
148
149public export
149public export
150−dropCombined : VarsIn vs ctxt -> Resources
150+dropCombined : VarsIn vs res -> Resources
151−dropCombined {ctxt = []} VarsNil = []
151+dropCombined {res = []} VarsNil = []
152−dropCombined {ctxt} (InCtxtVar el y) = dropCombined y
152+dropCombined {res} (InResVar el y) = dropCombined y
153−dropCombined {ctxt = (y :: ys)} (SkipVar x) = y :: dropCombined x
153+dropCombined {res = (y :: ys)} (SkipVar x) = y :: dropCombined x
154
154
155public export
155public export
156−combineVarsIn : (ctxt : Resources) -> VarsIn (comp :: vs) ctxt -> Resources
156+combineVarsIn : (res : Resources) -> VarsIn (comp :: vs) res -> Resources
157−combineVarsIn {comp} ctxt (InCtxtVar el x)
157+combineVarsIn {comp} res (InResVar el x)
158− = ((comp ::: Composite (getCombineType x)) :: dropCombined (InCtxtVar el x))
158+ = ((comp ::: Composite (getCombineType x)) :: dropCombined (InResVar el x))
159combineVarsIn (y :: ys) (SkipVar x) = y :: combineVarsIn ys x
159combineVarsIn (y :: ys) (SkipVar x) = y :: combineVarsIn ys x
160
160
161namespace Env
161namespace Env
@@ -168,51 +168,51 @@ namespace Env
168 (++) [] ys = ys
168 (++) [] ys = ys
169 (++) (x :: xs) ys = x :: xs ++ ys
169 (++) (x :: xs) ys = x :: xs ++ ys
170
170
171−lookupEnv : InState lbl ty ctxt -> Env ctxt -> ty
171+lookupEnv : InState lbl ty res -> Env res -> ty
172lookupEnv Here (x :: xs) = x
172lookupEnv Here (x :: xs) = x
173lookupEnv (There p) (x :: xs) = lookupEnv p xs
173lookupEnv (There p) (x :: xs) = lookupEnv p xs
174
174
175−updateEnv : (prf : InState lbl ty ctxt) -> Env ctxt -> ty' ->
175+updateEnv : (prf : InState lbl ty res) -> Env res -> ty' ->
176− Env (updateCtxt ctxt prf ty')
176+ Env (updateRes res prf ty')
177updateEnv Here (x :: xs) val = val :: xs
177updateEnv Here (x :: xs) val = val :: xs
178updateEnv (There p) (x :: xs) val = x :: updateEnv p xs val
178updateEnv (There p) (x :: xs) val = x :: updateEnv p xs val
179
179
180−dropVal : (prf : InState lbl st ctxt) -> Env ctxt -> Env (drop ctxt prf)
180+dropVal : (prf : InState lbl st res) -> Env res -> Env (drop res prf)
181dropVal Here (x :: xs) = xs
181dropVal Here (x :: xs) = xs
182dropVal (There p) (x :: xs) = x :: dropVal p xs
182dropVal (There p) (x :: xs) = x :: dropVal p xs
183
183
184−envElem : ElemCtxt x xs -> Env xs -> Env [x]
184+envElem : ElemRes x xs -> Env xs -> Env [x]
185−envElem HereCtxt (x :: xs) = [x]
185+envElem HereRes (x :: xs) = [x]
186−envElem (ThereCtxt p) (x :: xs) = envElem p xs
186+envElem (ThereRes p) (x :: xs) = envElem p xs
187
187
188−dropDups : Env xs -> (el : ElemCtxt x xs) -> Env (dropEl xs el)
188+dropDups : Env xs -> (el : ElemRes x xs) -> Env (dropEl xs el)
189−dropDups (y :: ys) HereCtxt = ys
189+dropDups (y :: ys) HereRes = ys
190−dropDups (y :: ys) (ThereCtxt p) = y :: dropDups ys p
190+dropDups (y :: ys) (ThereRes p) = y :: dropDups ys p
191
191
192
192
193−dropEntry : Env ctxt -> (prf : VarInCtxt x ctxt) -> Env (dropVarIn ctxt prf)
193+dropEntry : Env res -> (prf : VarInRes x res) -> Env (dropVarIn res prf)
194dropEntry (x :: env) VarHere = env
194dropEntry (x :: env) VarHere = env
195dropEntry (x :: env) (VarThere y) = x :: dropEntry env y
195dropEntry (x :: env) (VarThere y) = x :: dropEntry env y
196
196
197−dropVarsIn : Env ctxt -> (prf : VarsIn vs ctxt) -> Env (dropCombined prf)
197+dropVarsIn : Env res -> (prf : VarsIn vs res) -> Env (dropCombined prf)
198dropVarsIn [] VarsNil = []
198dropVarsIn [] VarsNil = []
199−dropVarsIn env (InCtxtVar el z) = dropVarsIn (dropEntry env el) z
199+dropVarsIn env (InResVar el z) = dropVarsIn (dropEntry env el) z
200dropVarsIn (x :: env) (SkipVar z) = x :: dropVarsIn env z
200dropVarsIn (x :: env) (SkipVar z) = x :: dropVarsIn env z
201
201
202−getVarEntry : Env ctxt -> (prf : VarInCtxt v ctxt) -> getVarType ctxt prf
202+getVarEntry : Env res -> (prf : VarInRes v res) -> getVarType res prf
203getVarEntry (x :: xs) VarHere = x
203getVarEntry (x :: xs) VarHere = x
204getVarEntry (x :: env) (VarThere p) = getVarEntry env p
204getVarEntry (x :: env) (VarThere p) = getVarEntry env p
205
205
206−mkComposite : Env ctxt -> (prf : VarsIn vs ctxt) -> Composite (getCombineType prf)
206+mkComposite : Env res -> (prf : VarsIn vs res) -> Composite (getCombineType prf)
207mkComposite [] VarsNil = CompNil
207mkComposite [] VarsNil = CompNil
208−mkComposite env (InCtxtVar el z)
208+mkComposite env (InResVar el z)
209 = CompCons (getVarEntry env el) (mkComposite (dropEntry env el) z)
209 = CompCons (getVarEntry env el) (mkComposite (dropEntry env el) z)
210mkComposite (x :: env) (SkipVar z) = mkComposite env z
210mkComposite (x :: env) (SkipVar z) = mkComposite env z
211
211
212−rebuildVarsIn : Env ctxt -> (prf : VarsIn (comp :: vs) ctxt) ->
212+rebuildVarsIn : Env res -> (prf : VarsIn (comp :: vs) res) ->
213− Env (combineVarsIn ctxt prf)
213+ Env (combineVarsIn res prf)
214−rebuildVarsIn env (InCtxtVar el p)
214+rebuildVarsIn env (InResVar el p)
215− = mkComposite (dropEntry env el) p :: dropVarsIn env (InCtxtVar el p)
215+ = mkComposite (dropEntry env el) p :: dropVarsIn env (InResVar el p)
216rebuildVarsIn (x :: env) (SkipVar p) = x :: rebuildVarsIn env p
216rebuildVarsIn (x :: env) (SkipVar p) = x :: rebuildVarsIn env p
217
217
218{- Some things to make STrans interfaces look prettier -}
218{- Some things to make STrans interfaces look prettier -}
@@ -264,9 +264,9 @@ addIfJust : Type -> Action (Maybe a)
264addIfJust ty = Add (maybe [] (\var => [var ::: ty]))
264addIfJust ty = Add (maybe [] (\var => [var ::: ty]))
265
265
266public export
266public export
267−kept : SubCtxt xs ys -> Resources
267+kept : SubRes xs ys -> Resources
268kept SubNil = []
268kept SubNil = []
269−kept (InCtxt el p) = kept p
269+kept (InRes el p) = kept p
270kept (Skip {y} p) = y :: kept p
270kept (Skip {y} p) = y :: kept p
271
271
272-- We can only use new/delete/read/write on things wrapped in State. Only an
272-- We can only use new/delete/read/write on things wrapped in State. Only an
@@ -287,41 +287,41 @@ data STrans : (m : Type -> Type) ->
287 ((result : a) ->
287 ((result : a) ->
288 STrans m b (st2_fn result) st3_fn) ->
288 STrans m b (st2_fn result) st3_fn) ->
289 STrans m b st1 st3_fn
289 STrans m b st1 st3_fn
290− Lift : Monad m => m t -> STrans m t ctxt (const ctxt)
290+ Lift : Monad m => m t -> STrans m t res (const res)
291 RunAs : Applicative m => STrans m t in_res (const out_res) ->
291 RunAs : Applicative m => STrans m t in_res (const out_res) ->
292 STrans m (m t) in_res (const out_res)
292 STrans m (m t) in_res (const out_res)
293
293
294 New : (val : state) ->
294 New : (val : state) ->
295− STrans m Var ctxt (\lbl => (lbl ::: state) :: ctxt)
295+ STrans m Var res (\lbl => (lbl ::: state) :: res)
296 Delete : (lbl : Var) ->
296 Delete : (lbl : Var) ->
297− (prf : InState lbl st ctxt) ->
297+ (prf : InState lbl st res) ->
298− STrans m () ctxt (const (drop ctxt prf))
298+ STrans m () res (const (drop res prf))
299− DropSubCtxt : (prf : SubCtxt ys xs) ->
299+ DropSubRes : (prf : SubRes ys xs) ->
300− STrans m (Env ys) xs (const (kept prf))
300+ STrans m (Env ys) xs (const (kept prf))
301
301
302 Split : (lbl : Var) ->
302 Split : (lbl : Var) ->
303− (prf : InState lbl (Composite vars) ctxt) ->
303+ (prf : InState lbl (Composite vars) res) ->
304− STrans m (VarList vars) ctxt
304+ STrans m (VarList vars) res
305− (\ vs => mkCtxt vs ++
305+ (\ vs => mkRes vs ++
306− updateCtxt ctxt prf (State ()))
306+ updateRes res prf (State ()))
307 Combine : (comp : Var) -> (vs : List Var) ->
307 Combine : (comp : Var) -> (vs : List Var) ->
308− (prf : VarsIn (comp :: vs) ctxt) ->
308+ (prf : VarsIn (comp :: vs) res) ->
309− STrans m () ctxt
309+ STrans m () res
310− (const (combineVarsIn ctxt prf))
310+ (const (combineVarsIn res prf))
311 ToEnd : (lbl : Var) ->
311 ToEnd : (lbl : Var) ->
312− (prf : InState lbl state ctxt) ->
312+ (prf : InState lbl state res) ->
313− STrans m () ctxt (const (drop ctxt prf ++ [lbl ::: state]))
313+ STrans m () res (const (drop res prf ++ [lbl ::: state]))
314
314
315− Call : STrans m t sub new_f -> (ctxt_prf : SubCtxt sub old) ->
315+ Call : STrans m t sub new_f -> (res_prf : SubRes sub old) ->
316− STrans m t old (\res => updateWith (new_f res) old ctxt_prf)
316+ STrans m t old (\res => updateWith (new_f res) old res_prf)
317
317
318 Read : (lbl : Var) ->
318 Read : (lbl : Var) ->
319− (prf : InState lbl ty ctxt) ->
319+ (prf : InState lbl ty res) ->
320− STrans m ty ctxt (const ctxt)
320+ STrans m ty res (const res)
321 Write : (lbl : Var) ->
321 Write : (lbl : Var) ->
322− (prf : InState lbl ty ctxt) ->
322+ (prf : InState lbl ty res) ->
323 (val : ty') ->
323 (val : ty') ->
324− STrans m () ctxt (const (updateCtxt ctxt prf ty'))
324+ STrans m () res (const (updateRes res prf ty'))
325
325
326namespace Loop
326namespace Loop
327 export
327 export
@@ -333,27 +333,27 @@ namespace Loop
333 Pure : (result : ty) -> STransLoop m ty (out_fn result) out_fn
333 Pure : (result : ty) -> STransLoop m ty (out_fn result) out_fn
334
334
335export
335export
336−dropEnv : Env ys -> SubCtxt xs ys -> Env xs
336+dropEnv : Env ys -> SubRes xs ys -> Env xs
337dropEnv [] SubNil = []
337dropEnv [] SubNil = []
338−dropEnv [] (InCtxt idx rest) = absurd idx
338+dropEnv [] (InRes idx rest) = absurd idx
339−dropEnv (z :: zs) (InCtxt idx rest)
339+dropEnv (z :: zs) (InRes idx rest)
340 = let [e] = envElem idx (z :: zs) in
340 = let [e] = envElem idx (z :: zs) in
341 e :: dropEnv (dropDups (z :: zs) idx) rest
341 e :: dropEnv (dropDups (z :: zs) idx) rest
342dropEnv (z :: zs) (Skip p) = dropEnv zs p
342dropEnv (z :: zs) (Skip p) = dropEnv zs p
343
343
344−keepEnv : Env ys -> (prf : SubCtxt xs ys) -> Env (kept prf)
344+keepEnv : Env ys -> (prf : SubRes xs ys) -> Env (kept prf)
345keepEnv env SubNil = env
345keepEnv env SubNil = env
346−keepEnv env (InCtxt el prf) = keepEnv (dropDups env el) prf
346+keepEnv env (InRes el prf) = keepEnv (dropDups env el) prf
347keepEnv (z :: zs) (Skip prf) = z :: keepEnv zs prf
347keepEnv (z :: zs) (Skip prf) = z :: keepEnv zs prf
348
348
349-- Corresponds pretty much exactly to 'updateWith'
349-- Corresponds pretty much exactly to 'updateWith'
350−rebuildEnv : Env new -> Env old -> (prf : SubCtxt sub old) ->
350+rebuildEnv : Env new -> Env old -> (prf : SubRes sub old) ->
351 Env (updateWith new old prf)
351 Env (updateWith new old prf)
352rebuildEnv new [] SubNil = new
352rebuildEnv new [] SubNil = new
353−rebuildEnv new [] (InCtxt el p) = absurd el
353+rebuildEnv new [] (InRes el p) = absurd el
354−rebuildEnv [] (x :: xs) (InCtxt el p)
354+rebuildEnv [] (x :: xs) (InRes el p)
355 = rebuildEnv [] (dropDups (x :: xs) el) p
355 = rebuildEnv [] (dropDups (x :: xs) el) p
356−rebuildEnv (e :: es) (x :: xs) (InCtxt el p)
356+rebuildEnv (e :: es) (x :: xs) (InRes el p)
357 = e :: rebuildEnv es (dropDups (x :: xs) el) p
357 = e :: rebuildEnv es (dropDups (x :: xs) el) p
358rebuildEnv new (x :: xs) (Skip p) = x :: rebuildEnv new xs p
358rebuildEnv new (x :: xs) (Skip p) = x :: rebuildEnv new xs p
359
359
@@ -368,7 +368,7 @@ runST env (Lift action) k
368runST env (RunAs prog) k = runST env prog (\res, env' => k (pure res) env')
368runST env (RunAs prog) k = runST env prog (\res, env' => k (pure res) env')
369runST env (New val) k = k MkVar (val :: env)
369runST env (New val) k = k MkVar (val :: env)
370runST env (Delete lbl prf) k = k () (dropVal prf env)
370runST env (Delete lbl prf) k = k () (dropVal prf env)
371−runST env (DropSubCtxt prf) k = k (dropEnv env prf) (keepEnv env prf)
371+runST env (DropSubRes prf) k = k (dropEnv env prf) (keepEnv env prf)
372runST env (Split lbl prf) k = let val = lookupEnv prf env
372runST env (Split lbl prf) k = let val = lookupEnv prf env
373 env' = updateEnv prf env (Value ()) in
373 env' = updateEnv prf env (Value ()) in
374 k (mkVars val) (addToEnv val env')
374 k (mkVars val) (addToEnv val env')
@@ -377,15 +377,15 @@ runST env (Split lbl prf) k = let val = lookupEnv prf env
377 mkVars CompNil = []
377 mkVars CompNil = []
378 mkVars (CompCons x xs) = MkVar :: mkVars xs
378 mkVars (CompCons x xs) = MkVar :: mkVars xs
379
379
380− addToEnv : (comp : Composite ts) -> Env xs -> Env (mkCtxt (mkVars comp) ++ xs)
380+ addToEnv : (comp : Composite ts) -> Env xs -> Env (mkRes (mkVars comp) ++ xs)
381 addToEnv CompNil env = env
381 addToEnv CompNil env = env
382 addToEnv (CompCons x xs) env = x :: addToEnv xs env
382 addToEnv (CompCons x xs) env = x :: addToEnv xs env
383runST env (ToEnd var prf) k = k () (dropVal prf env ++ [lookupEnv prf env])
383runST env (ToEnd var prf) k = k () (dropVal prf env ++ [lookupEnv prf env])
384runST env (Combine lbl vs prf) k = k () (rebuildVarsIn env prf)
384runST env (Combine lbl vs prf) k = k () (rebuildVarsIn env prf)
385−runST env (Call prog ctxt_prf) k
385+runST env (Call prog res_prf) k
386− = let env' = dropEnv env ctxt_prf in
386+ = let env' = dropEnv env res_prf in
387 runST env' prog
387 runST env' prog
388− (\prog', envk => k prog' (rebuildEnv envk env ctxt_prf))
388+ (\prog', envk => k prog' (rebuildEnv envk env res_prf))
389runST env (Read lbl prf) k = k (lookupEnv prf env) env
389runST env (Read lbl prf) k = k (lookupEnv prf env) env
390runST env (Write lbl prf val) k = k () (updateEnv prf env val)
390runST env (Write lbl prf val) k = k () (updateEnv prf env val)
391
391
@@ -415,14 +415,14 @@ export
415(>>=) = Bind
415(>>=) = Bind
416
416
417export
417export
418−returning : (result : ty) -> STrans m () ctxt (const (out_fn result)) ->
418+returning : (result : ty) -> STrans m () res (const (out_fn result)) ->
419− STrans m ty ctxt out_fn
419+ STrans m ty res out_fn
420returning res prog = do prog
420returning res prog = do prog
421 pure res
421 pure res
422
422
423
423
424export
424export
425−lift : Monad m => m t -> STrans m t ctxt (const ctxt)
425+lift : Monad m => m t -> STrans m t res (const res)
426lift = Lift
426lift = Lift
427
427
428export
428export
@@ -432,69 +432,69 @@ runAs = RunAs
432
432
433export
433export
434new : (val : state) ->
434new : (val : state) ->
435− STrans m Var ctxt (\lbl => (lbl ::: State state) :: ctxt)
435+ STrans m Var res (\lbl => (lbl ::: State state) :: res)
436new val = New (Value val)
436new val = New (Value val)
437
437
438export
438export
439delete : (lbl : Var) ->
439delete : (lbl : Var) ->
440− {auto prf : InState lbl (State st) ctxt} ->
440+ {auto prf : InState lbl (State st) res} ->
441− STrans m () ctxt (const (drop ctxt prf))
441+ STrans m () res (const (drop res prf))
442delete lbl {prf} = Delete lbl prf
442delete lbl {prf} = Delete lbl prf
443
443
444-- Keep only a subset of the current set of resources. Returns the
444-- Keep only a subset of the current set of resources. Returns the
445-- environment corresponding to the dropped portion.
445-- environment corresponding to the dropped portion.
446export
446export
447−dropSubCtxt : {auto prf : SubCtxt ys xs} ->
447+dropSub : {auto prf : SubRes ys xs} ->
448− STrans m (Env ys) xs (const (kept prf))
448+ STrans m (Env ys) xs (const (kept prf))
449−dropSubCtxt {prf} = DropSubCtxt prf
449+dropSub {prf} = DropSubRes prf
450
450
451export
451export
452split : (lbl : Var) ->
452split : (lbl : Var) ->
453− {auto prf : InState lbl (Composite vars) ctxt} ->
453+ {auto prf : InState lbl (Composite vars) res} ->
454− STrans m (VarList vars) ctxt
454+ STrans m (VarList vars) res
455− (\ vs => mkCtxt vs ++
455+ (\ vs => mkRes vs ++
456− updateCtxt ctxt prf (State ()))
456+ updateRes res prf (State ()))
457split lbl {prf} = Split lbl prf
457split lbl {prf} = Split lbl prf
458
458
459export
459export
460combine : (comp : Var) -> (vs : List Var) ->
460combine : (comp : Var) -> (vs : List Var) ->
461− {auto prf : InState comp (State ()) ctxt} ->
461+ {auto prf : InState comp (State ()) res} ->
462− {auto var_prf : VarsIn (comp :: vs) ctxt} ->
462+ {auto var_prf : VarsIn (comp :: vs) res} ->
463− STrans m () ctxt
463+ STrans m () res
464− (const (combineVarsIn ctxt var_prf))
464+ (const (combineVarsIn res var_prf))
465combine comp vs {var_prf} = Combine comp vs var_prf
465combine comp vs {var_prf} = Combine comp vs var_prf
466
466
467export
467export
468toEnd : (lbl : Var) ->
468toEnd : (lbl : Var) ->
469− {auto prf : InState lbl state ctxt} ->
469+ {auto prf : InState lbl state res} ->
470− STrans m () ctxt (const (drop ctxt prf ++ [lbl ::: state]))
470+ STrans m () res (const (drop res prf ++ [lbl ::: state]))
471toEnd lbl {prf} = ToEnd lbl prf
471toEnd lbl {prf} = ToEnd lbl prf
472
472
473export -- implicit ???
473export -- implicit ???
474call : STrans m t sub new_f ->
474call : STrans m t sub new_f ->
475− {auto ctxt_prf : SubCtxt sub old} ->
475+ {auto res_prf : SubRes sub old} ->
476− STrans m t old (\res => updateWith (new_f res) old ctxt_prf)
476+ STrans m t old (\res => updateWith (new_f res) old res_prf)
477−call prog {ctxt_prf} = Call prog ctxt_prf
477+call prog {res_prf} = Call prog res_prf
478
478
479export
479export
480read : (lbl : Var) ->
480read : (lbl : Var) ->
481− {auto prf : InState lbl (State ty) ctxt} ->
481+ {auto prf : InState lbl (State ty) res} ->
482− STrans m ty ctxt (const ctxt)
482+ STrans m ty res (const res)
483read lbl {prf} = do Value x <- Read lbl prf
483read lbl {prf} = do Value x <- Read lbl prf
484 pure x
484 pure x
485
485
486export
486export
487write : (lbl : Var) ->
487write : (lbl : Var) ->
488− {auto prf : InState lbl ty ctxt} ->
488+ {auto prf : InState lbl ty res} ->
489 (val : ty') ->
489 (val : ty') ->
490− STrans m () ctxt (const (updateCtxt ctxt prf (State ty')))
490+ STrans m () res (const (updateRes res prf (State ty')))
491write lbl {prf} val = Write lbl prf (Value val)
491write lbl {prf} val = Write lbl prf (Value val)
492
492
493export
493export
494update : (lbl : Var) ->
494update : (lbl : Var) ->
495− {auto prf : InState lbl (State ty) ctxt} ->
495+ {auto prf : InState lbl (State ty) res} ->
496 (ty -> ty') ->
496 (ty -> ty') ->
497− STrans m () ctxt (const (updateCtxt ctxt prf (State ty')))
497+ STrans m () res (const (updateRes res prf (State ty')))
498update lbl f = do x <- read lbl
498update lbl f = do x <- read lbl
499 write lbl (f x)
499 write lbl (f x)
500
500
@@ -575,15 +575,15 @@ runLoop fuel prog onEmpty
575||| responsibility of an implementation of an interface in IO which uses it
575||| responsibility of an implementation of an interface in IO which uses it
576||| to ensure that it isn't duplicated.
576||| to ensure that it isn't duplicated.
577export
577export
578−runWith : {ctxtf : _} ->
578+runWith : {resf : _} ->
579− Env ctxt -> STrans IO a ctxt (\res => ctxtf res) ->
579+ Env res -> STrans IO a res (\result => resf result) ->
580− IO (res ** Env (ctxtf res))
580+ IO (result ** Env (resf result))
581runWith env prog = runST env prog (\res, env' => pure (res ** env'))
581runWith env prog = runST env prog (\res, env' => pure (res ** env'))
582
582
583export
583export
584−runWithLoop : {ctxtf : _} ->
584+runWithLoop : {resf : _} ->
585− Env ctxt -> Fuel -> STransLoop IO a ctxt (\res => ctxtf res) ->
585+ Env res -> Fuel -> STransLoop IO a res (\result => resf result) ->
586− IO (Maybe (res ** Env (ctxtf res)))
586+ IO (Maybe (result ** Env (resf result)))
587runWithLoop env fuel prog
587runWithLoop env fuel prog
588 = runSTLoop fuel env prog (\res, env' => pure (Just (res ** env')))
588 = runSTLoop fuel env prog (\res, env' => pure (Just (res ** env')))
589 (pure Nothing)
589 (pure Nothing)
@@ -597,7 +597,7 @@ runPure prog = runST [] prog (\res, env' => res)
597%error_handler
597%error_handler
598export
598export
599st_precondition : Err -> Maybe (List ErrorReportPart)
599st_precondition : Err -> Maybe (List ErrorReportPart)
600−st_precondition (CantSolveGoal `(SubCtxt ~sub ~all) _)
600+st_precondition (CantSolveGoal `(SubRes ~sub ~all) _)
601 = pure
601 = pure
602 [TextPart "'call' is not valid here. ",
602 [TextPart "'call' is not valid here. ",
603 TextPart "The operation has preconditions ",
603 TextPart "The operation has preconditions ",
libs/contrib/Control/ST/ImplicitCall.idr+2−2
@@ -7,7 +7,7 @@ import Control.ST
7||| potentially more difficult to read.
7||| potentially more difficult to read.
8export implicit
8export implicit
9imp_call : STrans m t ys ys' ->
9imp_call : STrans m t ys ys' ->
10− {auto ctxt_prf : SubCtxt ys xs} ->
10+ {auto res_prf : SubRes ys xs} ->
11− STrans m t xs (\res => updateWith (ys' res) xs ctxt_prf)
11+ STrans m t xs (\res => updateWith (ys' res) xs res_prf)
12imp_call = call
12imp_call = call
13
13