git.iko.soy/Idris-dev
on master help sign in
Replace necessary export modifiers
c6acad2Edwin Brady
libs/effects/Effects.idr+7
compare with master
unifiedsplit
@@ -85,10 +85,12 @@ syntax "{" [inst] "==>" [outst] "}" [eff] = eff inst (\result => outst)
85
85
86-- --------------------------------------- [ Properties and Proof Construction ]
86-- --------------------------------------- [ Properties and Proof Construction ]
87
87
88+public export
88data SubElem : a -> List a -> Type where
89data SubElem : a -> List a -> Type where
89 Z : SubElem a (a :: as)
90 Z : SubElem a (a :: as)
90 S : SubElem a as -> SubElem a (b :: as)
91 S : SubElem a as -> SubElem a (b :: as)
91
92
93+public export
92data SubList : List a -> List a -> Type where
94data SubList : List a -> List a -> Type where
93 SubNil : SubList [] xs
95 SubNil : SubList [] xs
94 InList : SubElem x ys -> SubList xs ys -> SubList (x :: xs) ys
96 InList : SubElem x ys -> SubList xs ys -> SubList (x :: xs) ys
@@ -100,6 +102,7 @@ namespace Env
100 (::) : Handler eff m => a -> Env m xs -> Env m (MkEff a eff :: xs)
102 (::) : Handler eff m => a -> Env m xs -> Env m (MkEff a eff :: xs)
101
103
102namespace EffElem
104namespace EffElem
105+ public export
103 data EffElem : Effect -> Type ->
106 data EffElem : Effect -> Type ->
104 List EFFECT -> Type where
107 List EFFECT -> Type where
105 Here : EffElem x a (MkEff a x :: xs)
108 Here : EffElem x a (MkEff a x :: xs)
@@ -118,18 +121,21 @@ dropEnv e@(y::ys) (InList idx rest) =
118 let [x] = envElem idx e
121 let [x] = envElem idx e
119 in x :: dropEnv e rest
122 in x :: dropEnv e rest
120
123
124+public export
121total updateAt : (idx : SubElem x' xs) -> (a:Type) -> List EFFECT -> List EFFECT
125total updateAt : (idx : SubElem x' xs) -> (a:Type) -> List EFFECT -> List EFFECT
122updateAt Z a [] = []
126updateAt Z a [] = []
123updateAt Z a ((MkEff b eff) :: xs) = (MkEff a eff) :: xs
127updateAt Z a ((MkEff b eff) :: xs) = (MkEff a eff) :: xs
124updateAt (S k) a [] = []
128updateAt (S k) a [] = []
125updateAt (S k) a (x :: xs) = x :: updateAt k a xs
129updateAt (S k) a (x :: xs) = x :: updateAt k a xs
126
130
131+public export
127total updateWith : (ys' : List EFFECT) -> (xs : List EFFECT) ->
132total updateWith : (ys' : List EFFECT) -> (xs : List EFFECT) ->
128 SubList ys xs -> List EFFECT
133 SubList ys xs -> List EFFECT
129updateWith [] xs sl = xs
134updateWith [] xs sl = xs
130updateWith (y :: ys) xs SubNil = xs
135updateWith (y :: ys) xs SubNil = xs
131updateWith ((MkEff a f) :: ys) xs (InList idx rest) = updateAt idx a (updateWith ys xs rest)
136updateWith ((MkEff a f) :: ys) xs (InList idx rest) = updateAt idx a (updateWith ys xs rest)
132
137
138+public export
133total replaceEnvAt : (x : a) -> (idx : SubElem x' xs) -> Env m ys ->
139total replaceEnvAt : (x : a) -> (idx : SubElem x' xs) -> Env m ys ->
134 Env m (updateAt idx a ys)
140 Env m (updateAt idx a ys)
135replaceEnvAt x Z [] = []
141replaceEnvAt x Z [] = []
@@ -138,6 +144,7 @@ replaceEnvAt x (S k) [] = []
138replaceEnvAt x (S k) (y :: ys) = y :: replaceEnvAt x k ys
144replaceEnvAt x (S k) (y :: ys) = y :: replaceEnvAt x k ys
139
145
140||| Put things back, replacing old with new in the sub-environment
146||| Put things back, replacing old with new in the sub-environment
147+public export
141total rebuildEnv : {ys':List EFFECT} -> Env m ys' -> (prf : SubList ys xs) ->
148total rebuildEnv : {ys':List EFFECT} -> Env m ys' -> (prf : SubList ys xs) ->
142 Env m xs -> Env m (updateWith ys' xs prf)
149 Env m xs -> Env m (updateWith ys' xs prf)
143rebuildEnv [] SubNil env = env
150rebuildEnv [] SubNil env = env