9cb4a83 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Minor effects changes (locally, search depth)

commit9cb4a832723e8729d759881108e36cda2e71b9fb authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 23 Mar 2013, 10:28 (14 years ago) parent83b7ae5

2 files changed+8−2

unifiedsplit

effects/Effect/State.idr+6

@@ -33,4 +33,10 @@ updateM : (x -> y) -> EffM m [STATE x] [STATE y] ()

3333updateM f = do val <- get

3434 putM (f val)

3535

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

3642

effects/Effects.idr+2−2

@@ -116,14 +116,14 @@ data EffM : (m : Type -> Type) ->

116116-- Eff : List (EFFECT m) -> Type -> Type

117117

118118implicit

119−lift' : {default tactics { reflect findSubList 10; solve; }

119+lift' : {default tactics { reflect findSubList 100; solve; }

120120 prf : SubList ys xs} ->

121121 EffM m ys ys' t -> EffM m xs (updateWith ys' xs prf) t

122122lift' {prf} e = lift prf e

123123

124124implicit

125125effect' : {a, b: _} -> {e : Effect} ->

126− {default tactics { reflect findEffElem 10; solve; }

126+ {default tactics { reflect findEffElem 100; solve; }

127127 prf : EffElem e a xs} ->

128128 (eff : e a b t) ->

129129 EffM m xs (updateResTy xs prf eff) t