@@ -84,60 +84,71 @@ syntax "{" [inst] "==>" "{" {b} "}" [outst] "}" [eff]
8484syntax "{" [inst] "==>" [outst] "}" [eff] = eff inst (\result => outst)
8585
8686-- --------------------------------------- [ Properties and Proof Construction ]
87−public export
88−data SubList : List a -> List a -> Type where
89− SubNil : SubList [] []
90− Keep : SubList xs ys -> SubList (x :: xs) (x :: ys)
91− Drop : SubList xs ys -> SubList xs (x :: ys)
9287
93−%hint
94−subListId : SubList xs xs
95−subListId {xs = Nil} = SubNil
96−subListId {xs = x :: xs} = Keep subListId
88+data SubElem : a -> List a -> Type where
89+ Z : SubElem a (a :: as)
90+ S : SubElem a as -> SubElem a (b :: as)
91+
92+data SubList : List a -> List a -> Type where
93+ SubNil : SubList [] xs
94+ InList : SubElem x ys -> SubList xs ys -> SubList (x :: xs) ys
9795
9896namespace Env
9997 public export
10098 data Env : (m : Type -> Type) -> List EFFECT -> Type where
101− Nil : Env m Nil
102− (::) : Handler eff m => a -> Env m xs -> Env m (MkEff a eff :: xs)
103−
104−public export
105−data EffElem : Effect -> Type ->
106− List EFFECT -> Type where
107− Here : EffElem x a (MkEff a x :: xs)
108− There : EffElem x a xs -> EffElem x a (y :: xs)
99+ Nil : Env m Nil
100+ (::) : Handler eff m => a -> Env m xs -> Env m (MkEff a eff :: xs)
101+
102+namespace EffElem
103+ data EffElem : Effect -> Type ->
104+ List EFFECT -> Type where
105+ Here : EffElem x a (MkEff a x :: xs)
106+ There : EffElem x a xs -> EffElem x a (y :: xs)
107+
108+total envElem : SubElem x xs -> Env m xs -> Env m [x]
109+envElem Z (x :: xs) = [x]
110+envElem (S k) (x :: xs) = envElem k xs
109111
110112||| make an environment corresponding to a sub-list
111−private
112−dropEnv : Env m ys -> SubList xs ys -> Env m xs
113+%assert_total dropEnv : Env m ys -> SubList xs ys -> Env m xs
113114dropEnv [] SubNil = []
114−dropEnv (v :: vs) (Keep rest) = v :: dropEnv vs rest
115−dropEnv (v :: vs) (Drop rest) = dropEnv vs rest
116−
117−public export
118−updateWith : (ys' : List a) -> (xs : List a) ->
119− SubList ys xs -> List a
120−updateWith (y :: ys) (x :: xs) (Keep rest) = y :: updateWith ys xs rest
121−updateWith ys (x :: xs) (Drop rest) = x :: updateWith ys xs rest
122−updateWith [] [] SubNil = []
123−updateWith (y :: ys) [] SubNil = y :: ys
124−updateWith [] (x :: xs) (Keep rest) = []
115+-- dropEnv [] (InList y z) impossible
116+dropEnv (y::ys) SubNil = []
117+dropEnv e@(y::ys) (InList idx rest) =
118+ let [x] = envElem idx e
119+ in x :: dropEnv e rest
120+
121+total updateAt : (idx : SubElem x' xs) -> (a:Type) -> List EFFECT -> List EFFECT
122+updateAt Z a [] = []
123+updateAt Z a ((MkEff b eff) :: xs) = (MkEff a eff) :: xs
124+updateAt (S k) a [] = []
125+updateAt (S k) a (x :: xs) = x :: updateAt k a xs
126+
127+total updateWith : (ys' : List EFFECT) -> (xs : List EFFECT) ->
128+ SubList ys xs -> List EFFECT
129+updateWith [] xs sl = xs
130+updateWith (y :: ys) xs SubNil = xs
131+updateWith ((MkEff a f) :: ys) xs (InList idx rest) = updateAt idx a (updateWith ys xs rest)
132+
133+total replaceEnvAt : (x : a) -> (idx : SubElem x' xs) -> Env m ys ->
134+ Env m (updateAt idx a ys)
135+replaceEnvAt x Z [] = []
136+replaceEnvAt x Z (y :: ys) = x :: ys
137+replaceEnvAt x (S k) [] = []
138+replaceEnvAt x (S k) (y :: ys) = y :: replaceEnvAt x k ys
125139
126140||| Put things back, replacing old with new in the sub-environment
127−private
128−rebuildEnv : Env m ys' -> (prf : SubList ys xs) ->
141+total rebuildEnv : {ys':List EFFECT} -> Env m ys' -> (prf : SubList ys xs) ->
129142 Env m xs -> Env m (updateWith ys' xs prf)
130−rebuildEnv [] SubNil env = env
131−rebuildEnv (x :: xs) SubNil env = x :: xs
132−rebuildEnv [] (Keep rest) (y :: env) = []
133−rebuildEnv (x :: xs) (Keep rest) (y :: env) = x :: rebuildEnv xs rest env
134−rebuildEnv xs (Drop rest) (y :: env) = y :: rebuildEnv xs rest env
135−
143+rebuildEnv [] SubNil env = env
144+rebuildEnv (x :: xs) SubNil env = env
145+rebuildEnv [] (InList w s) env = env
146+rebuildEnv (x :: xs) (InList idx rest) env = replaceEnvAt x idx (rebuildEnv xs rest env)
136147
137148-- -------------------------------------------------- [ The Effect EDSL itself ]
138149
139150public export
140−updateResTy : (val : t) ->
151+total updateResTy : (val : t) ->
141152 (xs : List EFFECT) -> EffElem e a xs -> e t a b ->
142153 List EFFECT
143154updateResTy {b} val (MkEff a e :: xs) Here n = (MkEff (b val) e) :: xs