@@ -77,49 +77,64 @@ syntax "{" [inst] "==>" "{" {b} "}" [outst] "}" [eff]
77syntax "{" [inst] "==>" [outst] "}" [eff] = eff inst (\result => outst)
77syntax "{" [inst] "==>" [outst] "}" [eff] = eff inst (\result => outst)
79-- --------------------------------------- [ Properties and Proof Construction ]
79-- --------------------------------------- [ 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)
85−%hint
81+data SubElem : a -> List a -> Type where
86−subListId : SubList xs xs
82+ Z : SubElem a (a :: as)
87−subListId {xs = Nil} = SubNil
83+ S : SubElem a as -> SubElem a (b :: as)
88−subListId {xs = x :: xs} = Keep subListId
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
90namespace Env
89namespace Env
91 data Env : (m : Type -> Type) -> List EFFECT -> Type where
90 data Env : (m : Type -> Type) -> List EFFECT -> Type where
92− Nil : Env m Nil
91+ Nil : Env m Nil
93− (::) : Handler eff m => a -> Env m xs -> Env m (MkEff a eff :: xs)
92+ (::) : Handler eff m => a -> Env m xs -> Env m (MkEff a eff :: xs)
95−data EffElem : Effect -> Type ->
95+ data EffElem : Effect -> Type ->
96− List EFFECT -> Type where
96+ List EFFECT -> Type where
97− Here : EffElem x a (MkEff a x :: xs)
97+ Here : EffElem x a (MkEff a x :: xs)
98− There : EffElem x a xs -> EffElem x a (y :: xs)
98+ There : EffElem x a xs -> EffElem x a (y :: xs)
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
100||| make an environment corresponding to a sub-list
104||| make an environment corresponding to a sub-list
101dropEnv : Env m ys -> SubList xs ys -> Env m xs
105dropEnv : Env m ys -> SubList xs ys -> Env m xs
102dropEnv [] SubNil = []
106dropEnv [] SubNil = []
107+dropEnv (y::ys) SubNil = []
108+dropEnv e@(y::ys) (InList idx rest) =
109+ let [x] = envElem idx e
103−dropEnv (v :: vs) (Keep rest) = v :: dropEnv vs rest
110+ in x :: dropEnv e rest
104−dropEnv (v :: vs) (Drop rest) = dropEnv vs rest
111+
105−
112+updateAt : (idx : SubElem x' xs) -> (a:Type) -> List EFFECT -> List EFFECT
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
106−updateWith : (ys' : List a) -> (xs : List a) ->
118+updateWith : (ys' : List EFFECT) -> (xs : List EFFECT) ->
107− SubList ys xs -> List a
119+ SubList ys xs -> List EFFECT
120+updateWith [] xs sl = xs
121+updateWith (y :: ys) xs SubNil = xs
108−updateWith (y :: ys) (x :: xs) (Keep rest) = y :: updateWith ys xs rest
122+updateWith ((MkEff a f) :: ys) xs (InList idx rest) = updateAt idx a (updateWith ys xs rest)
109−updateWith ys (x :: xs) (Drop rest) = x :: updateWith ys xs rest
123+
110−updateWith [] [] SubNil = []
124+replaceEnvAt : (x : a) -> (idx : SubElem x' xs) -> Env m ys ->
111−updateWith (y :: ys) [] SubNil = y :: ys
125+ Env m (updateAt idx a ys)
112−updateWith [] (x :: xs) (Keep rest) = []
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
114||| Put things back, replacing old with new in the sub-environment
131||| 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) ->
116 Env m xs -> Env m (updateWith ys' xs prf)
133 Env m xs -> Env m (updateWith ys' xs prf)
117−rebuildEnv [] SubNil env = env
134+rebuildEnv [] SubNil env = env
118−rebuildEnv (x :: xs) SubNil env = x :: xs
135+rebuildEnv (x :: xs) SubNil env = env
119−rebuildEnv [] (Keep rest) (y :: env) = []
136+rebuildEnv [] (InList w s) env = env
120−rebuildEnv (x :: xs) (Keep rest) (y :: env) = x :: rebuildEnv xs rest env
137+rebuildEnv (x :: xs) (InList idx rest) env = replaceEnvAt x idx (rebuildEnv xs rest env)
121−rebuildEnv xs (Drop rest) (y :: env) = y :: rebuildEnv xs rest env
124-- -------------------------------------------------- [ The Effect EDSL itself ]
139-- -------------------------------------------------- [ The Effect EDSL itself ]