191ad06 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Add with_val and pureM syntax

Allows updating the set of effects based on a declared return value (pure is not quite enough for this: we need to provide the return value then a program which updates the set of effects/states to justify it being a value return value!) e.g. (somewhat contived, but...) readInt : { [STATE (Vect n Int), STDIO] ==> {done} if done then [STATE (Vect n Int), STDIO] else [STATE (Vect (S n) Int), STDIO] } Eff IO Bool readInt = do let x = trim !getStr if (x == "END") then pureM True else do putM (cast x :: !get) pureM False pureM x is equivalent to with_val x (pure ())

commit191ad06b14c22a2aca860afd153357eeada3e19a authorEdwin Brady <ecb10@st-andrews.ac.uk> dateTue 11 Mar 2014, 12:47 (13 years ago) parent992acb4

1 file changed+25−20

compare with master

unifiedsplit

libs/neweffects/Effects.idr+25−20

libs/neweffects/Effects.idr+25−20

@@ -162,26 +162,28 @@ relabel {xs = (MkEff a e :: xs)} l (v :: vs) = (l := v) :: relabel l vs

162162data Eff : (m : Type -> Type) ->

163163 (x : Type) ->

164164 List EFFECT -> (x -> List EFFECT) -> Type where

165− value : a -> Eff m a xs (\v => xs)

166− ebind : Eff m a xs xs' ->

167− ((val : a) -> Eff m b (xs' val) xs'') -> Eff m b xs xs''

168− effect : (prf : EffElem e a xs) ->

169− (eff : e t a b) ->

170− Eff m t xs (\v => updateResTy v xs prf eff)

171−

172− lift : (prf : SubList ys xs) ->

173− Eff m t ys ys' -> Eff m t xs (\v => updateWith (ys' v) xs prf)

174− newInit : Handler e m =>

175− res ->

176− Eff m a (MkEff res e :: xs) (\v => (MkEff res' e :: xs')) ->

177− Eff m a xs (\v => xs')

178− catch : Catchable m err =>

179− Eff m a xs xs' -> (err -> Eff m a xs xs') ->

180− Eff m a xs xs'

181−

182− (:-) : (l : ty) ->

183− Eff m t [x] xs' -> -- [x] (\v => xs) ->

184− Eff m t [l ::: x] (\v => map (l :::) (xs' v))

165+ value : a -> Eff m a xs (\v => xs)

166+ with_val : (val : a) -> Eff m () xs (\v => xs' val) ->

167+ Eff m a xs xs'

168+ ebind : Eff m a xs xs' ->

169+ ((val : a) -> Eff m b (xs' val) xs'') -> Eff m b xs xs''

170+ effect : (prf : EffElem e a xs) ->

171+ (eff : e t a b) ->

172+ Eff m t xs (\v => updateResTy v xs prf eff)

173+

174+ lift : (prf : SubList ys xs) ->

175+ Eff m t ys ys' -> Eff m t xs (\v => updateWith (ys' v) xs prf)

176+ newInit : Handler e m =>

177+ res ->

178+ Eff m a (MkEff res e :: xs) (\v => (MkEff res' e :: xs')) ->

179+ Eff m a xs (\v => xs')

180+ catch : Catchable m err =>

181+ Eff m a xs xs' -> (err -> Eff m a xs xs') ->

182+ Eff m a xs xs'

183+

184+ (:-) : (l : ty) ->

185+ Eff m t [x] xs' -> -- [x] (\v => xs) ->

186+ Eff m t [l ::: x] (\v => map (l :::) (xs' v))

185187

186188(>>=) : Eff m a xs xs' ->

187189 ((val : a) -> Eff m b (xs' val) xs'') -> Eff m b xs xs''

@@ -197,6 +199,8 @@ infixl 2 <$>

197199pure : a -> Eff m a xs (\v => xs)

198200pure = value

199201

202+syntax pureM [val] = with_val val (pure ())

203+

200204(<$>) : Eff m (a -> b) xs (\v => xs) ->

201205 Eff m a xs (\v => xs) -> Eff m b xs (\v => xs)

202206(<$>) prog v = do fn <- prog

@@ -220,6 +224,7 @@ execEff {e} {a} {res} {resk} (val :: env) (There p) eff k

220224

221225eff : Env m xs -> Eff m a xs xs' -> ((x : a) -> Env m (xs' x) -> m b) -> m b

222226eff env (value x) k = k x env

227+eff env (with_val x prog) k = eff env prog (\p', env' => k x env')

223228eff env (prog `ebind` c) k

224229 = eff env prog (\p', env' => eff env' (c p') k)

225230eff env (effect prf effP) k = execEff env prf effP k