@@ -97,31 +97,32 @@ namespace EffElem
9797 Here : EffElem x a (MkEff a x :: xs)
9898 There : EffElem x a xs -> EffElem x a (y :: xs)
9999
100−envElem : SubElem x xs -> Env m xs -> Env m [x]
100+total envElem : SubElem x xs -> Env m xs -> Env m [x]
101101envElem Z (x :: xs) = [x]
102102envElem (S k) (x :: xs) = envElem k xs
103103
104104||| make an environment corresponding to a sub-list
105−dropEnv : Env m ys -> SubList xs ys -> Env m xs
105+%assert_total dropEnv : Env m ys -> SubList xs ys -> Env m xs
106106dropEnv [] SubNil = []
107+-- dropEnv [] (InList y z) impossible
107108dropEnv (y::ys) SubNil = []
108109dropEnv e@(y::ys) (InList idx rest) =
109110 let [x] = envElem idx e
110111 in x :: dropEnv e rest
111112
112−updateAt : (idx : SubElem x' xs) -> (a:Type) -> List EFFECT -> List EFFECT
113+total updateAt : (idx : SubElem x' xs) -> (a:Type) -> List EFFECT -> List EFFECT
113114updateAt Z a [] = []
114115updateAt Z a ((MkEff b eff) :: xs) = (MkEff a eff) :: xs
115116updateAt (S k) a [] = []
116117updateAt (S k) a (x :: xs) = x :: updateAt k a xs
117118
118−updateWith : (ys' : List EFFECT) -> (xs : List EFFECT) ->
119+total updateWith : (ys' : List EFFECT) -> (xs : List EFFECT) ->
119120 SubList ys xs -> List EFFECT
120121updateWith [] xs sl = xs
121122updateWith (y :: ys) xs SubNil = xs
122123updateWith ((MkEff a f) :: ys) xs (InList idx rest) = updateAt idx a (updateWith ys xs rest)
123124
124−replaceEnvAt : (x : a) -> (idx : SubElem x' xs) -> Env m ys ->
125+total replaceEnvAt : (x : a) -> (idx : SubElem x' xs) -> Env m ys ->
125126 Env m (updateAt idx a ys)
126127replaceEnvAt x Z [] = []
127128replaceEnvAt x Z (y :: ys) = x :: ys
@@ -129,7 +130,7 @@ replaceEnvAt x (S k) [] = []
129130replaceEnvAt x (S k) (y :: ys) = y :: replaceEnvAt x k ys
130131
131132||| Put things back, replacing old with new in the sub-environment
132−rebuildEnv : {ys':List EFFECT} -> Env m ys' -> (prf : SubList ys xs) ->
133+total rebuildEnv : {ys':List EFFECT} -> Env m ys' -> (prf : SubList ys xs) ->
133134 Env m xs -> Env m (updateWith ys' xs prf)
134135rebuildEnv [] SubNil env = env
135136rebuildEnv (x :: xs) SubNil env = env
@@ -138,7 +139,7 @@ rebuildEnv (x :: xs) (InList idx rest) env = replaceEnvAt x idx (rebuildEnv xs r
138139
139140-- -------------------------------------------------- [ The Effect EDSL itself ]
140141
141−updateResTy : (val : t) ->
142+total updateResTy : (val : t) ->
142143 (xs : List EFFECT) -> EffElem e a xs -> e t a b ->
143144 List EFFECT
144145updateResTy {b} val (MkEff a e :: xs) Here n = (MkEff (b val) e) :: xs