git.iko.soy/Idris-dev
on master help sign in
Merge branch 'aaronc-master'
a341cf7Edwin Brady
Dockerfilenew file+6
compare with master
unifiedsplit
@@ -0,0 +1,6 @@
1+FROM haskell:7
2+RUN cabal update
3+ADD . Idris-dev
4+WORKDIR Idris-dev
5+RUN make
6+WORKDIR ..
libs/effects/Effects.idr+53−35
@@ -84,60 +84,78 @@ syntax "{" [inst] "==>" "{" {b} "}" [outst] "}" [eff]
84syntax "{" [inst] "==>" [outst] "}" [eff] = eff inst (\result => outst)
84syntax "{" [inst] "==>" [outst] "}" [eff] = eff inst (\result => outst)
85
85
86-- --------------------------------------- [ Properties and Proof Construction ]
86-- --------------------------------------- [ 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+
87public export
93public export
88data SubList : List a -> List a -> Type where
94data SubList : List a -> List a -> Type where
89− SubNil : SubList [] []
95+ SubNil : SubList [] xs
90− Keep : SubList xs ys -> SubList (x :: xs) (x :: ys)
96+ InList : SubElem x ys -> SubList xs ys -> SubList (x :: xs) 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
97
97
98namespace Env
98namespace Env
99 public export
99 public export
100 data Env : (m : Type -> Type) -> List EFFECT -> Type where
100 data Env : (m : Type -> Type) -> List EFFECT -> Type where
101− Nil : Env m Nil
101+ Nil : Env m Nil
102− (::) : Handler eff m => a -> Env m xs -> Env m (MkEff a eff :: xs)
102+ (::) : Handler eff m => a -> Env m xs -> Env m (MkEff a eff :: xs)
103
103
104+namespace EffElem
104−public export
105+ public export
105−data EffElem : Effect -> Type ->
106+ data EffElem : Effect -> Type ->
106− List EFFECT -> Type where
107+ List EFFECT -> Type where
107− Here : EffElem x a (MkEff a x :: xs)
108+ Here : EffElem x a (MkEff a x :: xs)
108− There : EffElem x a xs -> EffElem x a (y :: 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
109
114
110||| make an environment corresponding to a sub-list
115||| 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
113dropEnv [] SubNil = []
117dropEnv [] SubNil = []
114−dropEnv (v :: vs) (Keep rest) = v :: 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
115−dropEnv (v :: vs) (Drop rest) = dropEnv vs rest
122+ in x :: dropEnv e rest
116
123
117public export
124public export
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
118−updateWith : (ys' : List a) -> (xs : List a) ->
132+total updateWith : (ys' : List EFFECT) -> (xs : List EFFECT) ->
119− SubList ys xs -> List a
133+ SubList ys xs -> List EFFECT
134+updateWith [] xs sl = xs
135+updateWith (y :: ys) xs SubNil = xs
120−updateWith (y :: ys) (x :: xs) (Keep rest) = y :: updateWith ys xs rest
136+updateWith ((MkEff a f) :: ys) xs (InList idx rest) = updateAt idx a (updateWith ys xs rest)
121−updateWith ys (x :: xs) (Drop rest) = x :: updateWith ys xs rest
137+
122−updateWith [] [] SubNil = []
138+public export
123−updateWith (y :: ys) [] SubNil = y :: ys
139+total replaceEnvAt : (x : a) -> (idx : SubElem x' xs) -> Env m ys ->
124−updateWith [] (x :: xs) (Keep rest) = []
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
125
145
126||| Put things back, replacing old with new in the sub-environment
146||| Put things back, replacing old with new in the sub-environment
127−private
147+public export
128−rebuildEnv : Env m ys' -> (prf : SubList ys xs) ->
148+total rebuildEnv : {ys':List EFFECT} -> Env m ys' -> (prf : SubList ys xs) ->
129 Env m xs -> Env m (updateWith ys' xs prf)
149 Env m xs -> Env m (updateWith ys' xs prf)
130−rebuildEnv [] SubNil env = env
150+rebuildEnv [] SubNil env = env
131−rebuildEnv (x :: xs) SubNil env = x :: xs
151+rebuildEnv (x :: xs) SubNil env = env
132−rebuildEnv [] (Keep rest) (y :: env) = []
152+rebuildEnv [] (InList w s) env = env
133−rebuildEnv (x :: xs) (Keep rest) (y :: env) = x :: rebuildEnv xs rest env
153+rebuildEnv (x :: xs) (InList idx rest) env = replaceEnvAt x idx (rebuildEnv xs rest env)
134−rebuildEnv xs (Drop rest) (y :: env) = y :: rebuildEnv xs rest env
135−
136
154
137-- -------------------------------------------------- [ The Effect EDSL itself ]
155-- -------------------------------------------------- [ The Effect EDSL itself ]
138
156
139public export
157public export
140−updateResTy : (val : t) ->
158+total updateResTy : (val : t) ->
141 (xs : List EFFECT) -> EffElem e a xs -> e t a b ->
159 (xs : List EFFECT) -> EffElem e a xs -> e t a b ->
142 List EFFECT
160 List EFFECT
143updateResTy {b} val (MkEff a e :: xs) Here n = (MkEff (b val) e) :: xs
161updateResTy {b} val (MkEff a e :: xs) Here n = (MkEff (b val) e) :: xs