Permalink
Browse files

Minor effects changes (locally, search depth)

  • Loading branch information...
1 parent 83b7ae5 commit 9cb4a832723e8729d759881108e36cda2e71b9fb @edwinb committed Mar 23, 2013
Showing with 8 additions and 2 deletions.
  1. +6 −0 effects/Effect/State.idr
  2. +2 −2 effects/Effects.idr
View
@@ -33,4 +33,10 @@ updateM : (x -> y) -> EffM m [STATE x] [STATE y] ()
updateM f = do val <- get
putM (f val)
+locally : x -> Eff m [STATE x] t -> Eff m [STATE y] t
+locally newst prog = do st <- get
+ putM newst
+ val <- prog
+ putM st
+ return val
View
@@ -116,14 +116,14 @@ data EffM : (m : Type -> Type) ->
-- Eff : List (EFFECT m) -> Type -> Type
implicit
-lift' : {default tactics { reflect findSubList 10; solve; }
+lift' : {default tactics { reflect findSubList 100; solve; }
prf : SubList ys xs} ->
EffM m ys ys' t -> EffM m xs (updateWith ys' xs prf) t
lift' {prf} e = lift prf e
implicit
effect' : {a, b: _} -> {e : Effect} ->
- {default tactics { reflect findEffElem 10; solve; }
+ {default tactics { reflect findEffElem 100; solve; }
prf : EffElem e a xs} ->
(eff : e a b t) ->
EffM m xs (updateResTy xs prf eff) t

0 comments on commit 9cb4a83

Please sign in to comment.