@@ -84,60 +84,78 @@ syntax "{" [inst] "==>" "{" {b} "}" [outst] "}" [eff]
8484syntax "{" [inst] "==>" [outst] "}" [eff] = eff inst (\result => outst)
8585
8686-- --------------------------------------- [ Properties and Proof Construction ]
87+
88+public export
89+data SubElem : a -> List a -> Type where
90+ Z : SubElem a (a :: as)
91+ S : SubElem a as -> SubElem a (b :: as)
92+
8793public export
8894data 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)
92−
93−%hint
94−subListId : SubList xs xs
95−subListId {xs = Nil} = SubNil
96−subListId {xs = x :: xs} = Keep subListId
95+ SubNil : SubList [] xs
96+ InList : SubElem x ys -> SubList xs ys -> SubList (x :: xs) ys
9797
9898namespace Env
9999 public export
100100 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)
101+ Nil : Env m Nil
102+ (::) : Handler eff m => a -> Env m xs -> Env m (MkEff a eff :: xs)
103103
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)
104+namespace EffElem
105+ public export
106+ data EffElem : Effect -> Type ->
107+ List EFFECT -> Type where
108+ Here : EffElem x a (MkEff a x :: xs)
109+ There : EffElem x a xs -> EffElem x a (y :: xs)
110+
111+total envElem : SubElem x xs -> Env m xs -> Env m [x]
112+envElem Z (x :: xs) = [x]
113+envElem (S k) (x :: xs) = envElem k xs
109114
110115||| make an environment corresponding to a sub-list
111−private
112−dropEnv : Env m ys -> SubList xs ys -> Env m xs
116+%assert_total dropEnv : Env m ys -> SubList xs ys -> Env m xs
113117dropEnv [] SubNil = []
114−dropEnv (v :: vs) (Keep rest) = v :: dropEnv vs rest
115−dropEnv (v :: vs) (Drop rest) = dropEnv vs rest
118+-- dropEnv [] (InList y z) impossible
119+dropEnv (y::ys) SubNil = []
120+dropEnv e@(y::ys) (InList idx rest) =
121+ let [x] = envElem idx e
122+ in x :: dropEnv e rest
116123
117124public 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) = []
125+total updateAt : (idx : SubElem x' xs) -> (a:Type) -> List EFFECT -> List EFFECT
126+updateAt Z a [] = []
127+updateAt Z a ((MkEff b eff) :: xs) = (MkEff a eff) :: xs
128+updateAt (S k) a [] = []
129+updateAt (S k) a (x :: xs) = x :: updateAt k a xs
130+
131+public export
132+total updateWith : (ys' : List EFFECT) -> (xs : List EFFECT) ->
133+ SubList ys xs -> List EFFECT
134+updateWith [] xs sl = xs
135+updateWith (y :: ys) xs SubNil = xs
136+updateWith ((MkEff a f) :: ys) xs (InList idx rest) = updateAt idx a (updateWith ys xs rest)
137+
138+public export
139+total replaceEnvAt : (x : a) -> (idx : SubElem x' xs) -> Env m ys ->
140+ Env m (updateAt idx a ys)
141+replaceEnvAt x Z [] = []
142+replaceEnvAt x Z (y :: ys) = x :: ys
143+replaceEnvAt x (S k) [] = []
144+replaceEnvAt x (S k) (y :: ys) = y :: replaceEnvAt x k ys
125145
126146||| Put things back, replacing old with new in the sub-environment
127−private
128−rebuildEnv : Env m ys' -> (prf : SubList ys xs) ->
147+public export
148+total rebuildEnv : {ys':List EFFECT} -> Env m ys' -> (prf : SubList ys xs) ->
129149 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−
150+rebuildEnv [] SubNil env = env
151+rebuildEnv (x :: xs) SubNil env = env
152+rebuildEnv [] (InList w s) env = env
153+rebuildEnv (x :: xs) (InList idx rest) env = replaceEnvAt x idx (rebuildEnv xs rest env)
136154
137155-- -------------------------------------------------- [ The Effect EDSL itself ]
138156
139157public export
140−updateResTy : (val : t) ->
158+total updateResTy : (val : t) ->
141159 (xs : List EFFECT) -> EffElem e a xs -> e t a b ->
142160 List EFFECT
143161updateResTy {b} val (MkEff a e :: xs) Here n = (MkEff (b val) e) :: xs