git.iko.soy/Idris-dev
on master help sign in
Added totality checks to Effects reordering functions and a %assert_total directive for dropEnv where I cannot figure out how to deal with the failing case (which I'm pretty sure is impossible).
d36eeeaAaron Craelius
libs/effects/Effects.idr+8−7
compare with master
unifiedsplit
@@ -97,31 +97,32 @@ namespace EffElem
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)
99
99
100−envElem : SubElem x xs -> Env m xs -> Env m [x]
100+total envElem : SubElem x xs -> Env m xs -> Env m [x]
101envElem Z (x :: xs) = [x]
101envElem Z (x :: xs) = [x]
102envElem (S k) (x :: xs) = envElem k xs
102envElem (S k) (x :: xs) = envElem k xs
103
103
104||| make an environment corresponding to a sub-list
104||| 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
106dropEnv [] SubNil = []
106dropEnv [] SubNil = []
107+-- dropEnv [] (InList y z) impossible
107dropEnv (y::ys) SubNil = []
108dropEnv (y::ys) SubNil = []
108dropEnv e@(y::ys) (InList idx rest) =
109dropEnv e@(y::ys) (InList idx rest) =
109 let [x] = envElem idx e
110 let [x] = envElem idx e
110 in x :: dropEnv e rest
111 in x :: dropEnv e rest
111
112
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
113updateAt Z a [] = []
114updateAt Z a [] = []
114updateAt Z a ((MkEff b eff) :: xs) = (MkEff a eff) :: xs
115updateAt Z a ((MkEff b eff) :: xs) = (MkEff a eff) :: xs
115updateAt (S k) a [] = []
116updateAt (S k) a [] = []
116updateAt (S k) a (x :: xs) = x :: updateAt k a xs
117updateAt (S k) a (x :: xs) = x :: updateAt k a xs
117
118
118−updateWith : (ys' : List EFFECT) -> (xs : List EFFECT) ->
119+total updateWith : (ys' : List EFFECT) -> (xs : List EFFECT) ->
119 SubList ys xs -> List EFFECT
120 SubList ys xs -> List EFFECT
120updateWith [] xs sl = xs
121updateWith [] xs sl = xs
121updateWith (y :: ys) xs SubNil = xs
122updateWith (y :: ys) xs SubNil = xs
122updateWith ((MkEff a f) :: ys) xs (InList idx rest) = updateAt idx a (updateWith ys xs rest)
123updateWith ((MkEff a f) :: ys) xs (InList idx rest) = updateAt idx a (updateWith ys xs rest)
123
124
124−replaceEnvAt : (x : a) -> (idx : SubElem x' xs) -> Env m ys ->
125+total replaceEnvAt : (x : a) -> (idx : SubElem x' xs) -> Env m ys ->
125 Env m (updateAt idx a ys)
126 Env m (updateAt idx a ys)
126replaceEnvAt x Z [] = []
127replaceEnvAt x Z [] = []
127replaceEnvAt x Z (y :: ys) = x :: ys
128replaceEnvAt x Z (y :: ys) = x :: ys
@@ -129,7 +130,7 @@ replaceEnvAt x (S k) [] = []
129replaceEnvAt x (S k) (y :: ys) = y :: replaceEnvAt x k ys
130replaceEnvAt x (S k) (y :: ys) = y :: replaceEnvAt x k ys
130
131
131||| Put things back, replacing old with new in the sub-environment
132||| 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) ->
133 Env m xs -> Env m (updateWith ys' xs prf)
134 Env m xs -> Env m (updateWith ys' xs prf)
134rebuildEnv [] SubNil env = env
135rebuildEnv [] SubNil env = env
135rebuildEnv (x :: xs) SubNil env = env
136rebuildEnv (x :: xs) SubNil env = env
@@ -138,7 +139,7 @@ rebuildEnv (x :: xs) (InList idx rest) env = replaceEnvAt x idx (rebuildEnv xs r
138
139
139-- -------------------------------------------------- [ The Effect EDSL itself ]
140-- -------------------------------------------------- [ The Effect EDSL itself ]
140
141
141−updateResTy : (val : t) ->
142+total updateResTy : (val : t) ->
142 (xs : List EFFECT) -> EffElem e a xs -> e t a b ->
143 (xs : List EFFECT) -> EffElem e a xs -> e t a b ->
143 List EFFECT
144 List EFFECT
144updateResTy {b} val (MkEff a e :: xs) Here n = (MkEff (b val) e) :: xs
145updateResTy {b} val (MkEff a e :: xs) Here n = (MkEff (b val) e) :: xs