git.iko.soy/Idris-dev
on master help sign in
Minor effects changes (locally, search depth)
9cb4a83Edwin Brady
effects/Effect/State.idr+6
compare with master
unifiedsplit
@@ -33,4 +33,10 @@ updateM : (x -> y) -> EffM m [STATE x] [STATE y] ()
33updateM f = do val <- get
33updateM f = do val <- get
34 putM (f val)
34 putM (f val)
35
35
36+locally : x -> Eff m [STATE x] t -> Eff m [STATE y] t
37+locally newst prog = do st <- get
38+ putM newst
39+ val <- prog
40+ putM st
41+ return val
36
42
effects/Effects.idr+2−2
@@ -116,14 +116,14 @@ data EffM : (m : Type -> Type) ->
116-- Eff : List (EFFECT m) -> Type -> Type
116-- Eff : List (EFFECT m) -> Type -> Type
117
117
118implicit
118implicit
119−lift' : {default tactics { reflect findSubList 10; solve; }
119+lift' : {default tactics { reflect findSubList 100; solve; }
120 prf : SubList ys xs} ->
120 prf : SubList ys xs} ->
121 EffM m ys ys' t -> EffM m xs (updateWith ys' xs prf) t
121 EffM m ys ys' t -> EffM m xs (updateWith ys' xs prf) t
122lift' {prf} e = lift prf e
122lift' {prf} e = lift prf e
123
123
124implicit
124implicit
125effect' : {a, b: _} -> {e : Effect} ->
125effect' : {a, b: _} -> {e : Effect} ->
126− {default tactics { reflect findEffElem 10; solve; }
126+ {default tactics { reflect findEffElem 100; solve; }
127 prf : EffElem e a xs} ->
127 prf : EffElem e a xs} ->
128 (eff : e a b t) ->
128 (eff : e a b t) ->
129 EffM m xs (updateResTy xs prf eff) t
129 EffM m xs (updateResTy xs prf eff) t