@@ -77,49 +77,64 @@ syntax "{" [inst] "==>" "{" {b} "}" [outst] "}" [eff]
7777syntax "{" [inst] "==>" [outst] "}" [eff] = eff inst (\result => outst)
7878
7979-- --------------------------------------- [ Properties and Proof Construction ]
80−data SubList : List a -> List a -> Type where
81− SubNil : SubList [] []
82− Keep : SubList xs ys -> SubList (x :: xs) (x :: ys)
83− Drop : SubList xs ys -> SubList xs (x :: ys)
8480
85−%hint
86−subListId : SubList xs xs
87−subListId {xs = Nil} = SubNil
88−subListId {xs = x :: xs} = Keep subListId
81+data SubElem : a -> List a -> Type where
82+ Z : SubElem a (a :: as)
83+ S : SubElem a as -> SubElem a (b :: as)
84+
85+data SubList : List a -> List a -> Type where
86+ SubNil : SubList [] xs
87+ InList : SubElem x ys -> SubList xs ys -> SubList (x :: xs) ys
8988
9089namespace Env
9190 data Env : (m : Type -> Type) -> List EFFECT -> Type where
92− Nil : Env m Nil
93− (::) : Handler eff m => a -> Env m xs -> Env m (MkEff a eff :: xs)
94−
95−data EffElem : Effect -> Type ->
96− List EFFECT -> Type where
97− Here : EffElem x a (MkEff a x :: xs)
98− There : EffElem x a xs -> EffElem x a (y :: xs)
91+ Nil : Env m Nil
92+ (::) : Handler eff m => a -> Env m xs -> Env m (MkEff a eff :: xs)
93+
94+namespace EffElem
95+ data EffElem : Effect -> Type ->
96+ List EFFECT -> Type where
97+ Here : EffElem x a (MkEff a x :: xs)
98+ There : EffElem x a xs -> EffElem x a (y :: xs)
99+
100+envElem : SubElem x xs -> Env m xs -> Env m [x]
101+envElem Z (x :: xs) = [x]
102+envElem (S k) (x :: xs) = envElem k xs
99103
100104||| make an environment corresponding to a sub-list
101105dropEnv : Env m ys -> SubList xs ys -> Env m xs
102106dropEnv [] SubNil = []
103−dropEnv (v :: vs) (Keep rest) = v :: dropEnv vs rest
104−dropEnv (v :: vs) (Drop rest) = dropEnv vs rest
105−
106−updateWith : (ys' : List a) -> (xs : List a) ->
107− SubList ys xs -> List a
108−updateWith (y :: ys) (x :: xs) (Keep rest) = y :: updateWith ys xs rest
109−updateWith ys (x :: xs) (Drop rest) = x :: updateWith ys xs rest
110−updateWith [] [] SubNil = []
111−updateWith (y :: ys) [] SubNil = y :: ys
112−updateWith [] (x :: xs) (Keep rest) = []
107+dropEnv (y::ys) SubNil = []
108+dropEnv e@(y::ys) (InList idx rest) =
109+ let [x] = envElem idx e
110+ in x :: dropEnv e rest
111+
112+updateAt : (idx : SubElem x' xs) -> (a:Type) -> List EFFECT -> List EFFECT
113+updateAt Z a [] = []
114+updateAt Z a ((MkEff b eff) :: xs) = (MkEff a eff) :: xs
115+updateAt (S k) a [] = []
116+updateAt (S k) a (x :: xs) = x :: updateAt k a xs
117+
118+updateWith : (ys' : List EFFECT) -> (xs : List EFFECT) ->
119+ SubList ys xs -> List EFFECT
120+updateWith [] xs sl = xs
121+updateWith (y :: ys) xs SubNil = xs
122+updateWith ((MkEff a f) :: ys) xs (InList idx rest) = updateAt idx a (updateWith ys xs rest)
123+
124+replaceEnvAt : (x : a) -> (idx : SubElem x' xs) -> Env m ys ->
125+ Env m (updateAt idx a ys)
126+replaceEnvAt x Z [] = []
127+replaceEnvAt x Z (y :: ys) = x :: ys
128+replaceEnvAt x (S k) [] = []
129+replaceEnvAt x (S k) (y :: ys) = y :: replaceEnvAt x k ys
113130
114131||| Put things back, replacing old with new in the sub-environment
115−rebuildEnv : Env m ys' -> (prf : SubList ys xs) ->
132+rebuildEnv : {ys':List EFFECT} -> Env m ys' -> (prf : SubList ys xs) ->
116133 Env m xs -> Env m (updateWith ys' xs prf)
117−rebuildEnv [] SubNil env = env
118−rebuildEnv (x :: xs) SubNil env = x :: xs
119−rebuildEnv [] (Keep rest) (y :: env) = []
120−rebuildEnv (x :: xs) (Keep rest) (y :: env) = x :: rebuildEnv xs rest env
121−rebuildEnv xs (Drop rest) (y :: env) = y :: rebuildEnv xs rest env
122−
134+rebuildEnv [] SubNil env = env
135+rebuildEnv (x :: xs) SubNil env = env
136+rebuildEnv [] (InList w s) env = env
137+rebuildEnv (x :: xs) (InList idx rest) env = replaceEnvAt x idx (rebuildEnv xs rest env)
123138
124139-- -------------------------------------------------- [ The Effect EDSL itself ]
125140