5ba96c1 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Effect handlers should be covering

They don't make sense if they don't handle all possible operations, and this can lead to strange errors (one of which I've just been debugging in Protocols!)

commit5ba96c11ccd8b875edca7904e5bd183fd7380757 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateFri 23 May 2014, 19:31 (12 years ago) parentd5a2ba4

5 files changed+25−18

compare with master

unifiedsplit

libs/effects/Effect/Random.idr+2−2 libs/effects/Effects.idr+3−3 src/Idris/Core/Evaluate.hs+2−1 src/Idris/Coverage.hs+12−7 src/Idris/Primitives.hs+6−5

libs/effects/Effect/Random.idr+2−2

@@ -9,7 +9,7 @@ data Random : Effect where

99using (m : Type -> Type)

1010 instance Handler Random m where

1111 handle seed getRandom k

12− = let seed' = (1664525 * seed + 1013904223) `prim__sremBigInt` (pow 2 32) in

12+ = let seed' = assert_total ((1664525 * seed + 1013904223) `prim__sremBigInt` (pow 2 32)) in

1313 k seed' seed'

1414 handle seed (setSeed n) k = k () n

1515

@@ -25,7 +25,7 @@ rndInt lower upper = do v <- getRandom

2525|||

2626||| Note that rndFin k takes values 0, 1, ..., k.

2727rndFin : (k : Nat) -> { [RND] } Eff m (Fin (S k))

28−rndFin k = do let v = !getRandom `prim__sremBigInt` (cast (S k))

28+rndFin k = do let v = assert_total $ !getRandom `prim__sremBigInt` (cast (S k))

2929 return (toFin v)

3030 where toFin : Integer -> Fin (S k)

3131 toFin x = case integerToFin x (S k) of

libs/effects/Effects.idr+3−3

@@ -31,9 +31,9 @@ class Handler (e : Effect) (m : Type -> Type) where

3131 |||

3232 ||| @ r The resource being handled.

3333 ||| @ eff The effect to be applied.

34− ||| @ ctxt The context in which to handle the effect.

35− handle : (r : res) -> (eff : e t res resk) ->

36− (ctxt : ((x : t) -> resk x -> m a)) -> m a

34+ ||| @ k The continuation to pass the result of the effect

35+ covering handle : (r : res) -> (eff : e t res resk) ->

36+ (k : ((x : t) -> resk x -> m a)) -> m a

3737

3838||| Get the resource type (handy at the REPL to find out about an effect)

3939resourceType : EFFECT -> Type

src/Idris/Core/Evaluate.hs+2−1

@@ -678,7 +678,7 @@ data Totality = Total [Int] -- ^ well-founded arguments

678678

679679-- | Reasons why a function may not be total

680680data PReason = Other [Name] | Itself | NotCovering | NotPositive | UseUndef Name

681− | BelieveMe | Mutual [Name] | NotProductive

681+ | ExternalIO | BelieveMe | Mutual [Name] | NotProductive

682682 deriving (Show, Eq)

683683

684684instance Show Totality where

@@ -688,6 +688,7 @@ instance Show Totality where

688688 show (Partial Itself) = "possibly not total as it is not well founded"

689689 show (Partial NotCovering) = "not total as there are missing cases"

690690 show (Partial NotPositive) = "not strictly positive"

691+ show (Partial ExternalIO) = "an external IO primitive"

691692 show (Partial NotProductive) = "not productive"

692693 show (Partial BelieveMe) = "not total due to use of believe_me in proof"

693694 show (Partial (Other ns)) = "possibly not total due to: " ++ showSep ", " (map show ns)

src/Idris/Coverage.hs+12−7

@@ -9,7 +9,7 @@ import Idris.Core.CaseTree

99import Idris.AbsSyntax

1010import Idris.Delaborate

1111import Idris.Error

12−import Idris.Output (iWarn)

12+import Idris.Output (iWarn, iputStrLn)

1313

1414import Data.List

1515import Data.Either

@@ -255,13 +255,14 @@ checkAllCovering fc done top n | not (n `elem` done)

255255 case lookupTotal n (tt_ctxt i) of

256256 [tot@(Partial NotCovering)] ->

257257 do let msg = show top ++ " is " ++ show tot ++ " due to " ++ show n

258− addIBC (IBCTotCheckErr fc msg)

259258 putIState i { idris_totcheckfail = (fc, msg) : idris_totcheckfail i }

260− _ -> return ()

261− case lookupCtxt n (idris_callgraph i) of

262− [cg] -> mapM_ (checkAllCovering fc (n : done) top)

263− (map fst (calls cg))

264− _ -> return ()

259+ addIBC (IBCTotCheckErr fc msg)

260+ [Partial _] ->

261+ case lookupCtxt n (idris_callgraph i) of

262+ [cg] -> mapM_ (checkAllCovering fc (n : done) top)

263+ (map fst (calls cg))

264+ _ -> return ()

265+ x -> return () -- stop if total

265266checkAllCovering _ _ _ _ = return ()

266267

267268-- Check if, in a given type n, the constructor cn : ty is strictly positive,

@@ -415,6 +416,10 @@ checkDeclTotality (fc, n)

415416-- buildSCG (fc, n)

416417-- logLvl 2 $ "Built SCG"

417418 i <- getIState

419+ let opts = case lookupCtxt n (idris_flags i) of

420+ [fs] -> fs

421+ _ -> []

422+ when (CoveringFn `elem` opts) $ checkAllCovering fc [] n n

418423 t <- checkTotality [] fc n

419424 case t of

420425 -- if it's not total, it can't reduce, to keep

src/Idris/Primitives.hs+6−5

@@ -28,9 +28,10 @@ ty :: [Const] -> Const -> Type

2828ty [] x = Constant x

2929ty (t:ts) x = Bind (sMN 0 "T") (Pi (Constant t)) (ty ts x)

3030

31−total, partial :: Totality

31+total, partial, iopartial :: Totality

3232total = Total []

3333partial = Partial NotCovering

34+iopartial = Partial ExternalIO

3435

3536primitives :: [Prim]

3637primitives =

@@ -164,16 +165,16 @@ primitives =

164165 Prim (sUN "prim__strRev") (ty [StrType] StrType) 1 (p_strRev)

165166 (1, LStrRev) total,

166167 Prim (sUN "prim__readString") (ty [PtrType] StrType) 1 (p_cantreduce)

167− (1, LReadStr) partial,

168+ (1, LReadStr) iopartial,

168169 Prim (sUN "prim__vm") (ty [] PtrType) 0 (p_cantreduce)

169170 (0, LVMPtr) total,

170171 -- Streams

171172 Prim (sUN "prim__stdin") (ty [] PtrType) 0 (p_cantreduce)

172− (0, LStdIn) partial,

173+ (0, LStdIn) iopartial,

173174 Prim (sUN "prim__stdout") (ty [] PtrType) 0 (p_cantreduce)

174− (0, LStdOut) partial,

175+ (0, LStdOut) iopartial,

175176 Prim (sUN "prim__stderr") (ty [] PtrType) 0 (p_cantreduce)

176− (0, LStdErr) partial,

177+ (0, LStdErr) iopartial,

177178 Prim (sUN "prim__null") (ty [] PtrType) 0 (p_cantreduce)

178179 (0, LNullPtr) total,

179180 -- Managed pointer registration