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

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

compare with master

unifiedsplit

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

9using (m : Type -> Type)

10 instance Handler Random m where

11 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

13 k seed' seed'

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

15

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

25|||

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

27rndFin : (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))

29 return (toFin v)

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

31 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

31 |||

32 ||| @ r The resource being handled.

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

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

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

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

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

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

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

37

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

39resourceType : EFFECT -> Type

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

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

678

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

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

681− | BelieveMe | Mutual [Name] | NotProductive

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

682 deriving (Show, Eq)

683

684instance Show Totality where

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

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

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

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

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

691 show (Partial NotProductive) = "not productive"

692 show (Partial NotProductive) = "not productive"

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

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

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

694 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

9import Idris.AbsSyntax

10import Idris.Delaborate

11import Idris.Error

12−import Idris.Output (iWarn)

12+import Idris.Output (iWarn, iputStrLn)

13

14import Data.List

15import Data.Either

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

255 case lookupTotal n (tt_ctxt i) of

256 [tot@(Partial NotCovering)] ->

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

258− addIBC (IBCTotCheckErr fc msg)

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

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

260− _ -> return ()

259+ addIBC (IBCTotCheckErr fc msg)

260+ [Partial _] ->

261− case lookupCtxt n (idris_callgraph i) of

261+ case lookupCtxt n (idris_callgraph i) of

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

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

263− (map fst (calls cg))

263+ (map fst (calls cg))

264+ _ -> return ()

264− _ -> return ()

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

265checkAllCovering _ _ _ _ = return ()

266checkAllCovering _ _ _ _ = return ()

266

267

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

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

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

415-- buildSCG (fc, n)

416-- buildSCG (fc, n)

416-- logLvl 2 $ "Built SCG"

417-- logLvl 2 $ "Built SCG"

417 i <- getIState

418 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

418 t <- checkTotality [] fc n

423 t <- checkTotality [] fc n

419 case t of

424 case t of

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

425 -- 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

28ty [] x = Constant x

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

30

31−total, partial :: Totality

31+total, partial, iopartial :: Totality

32total = Total []

33partial = Partial NotCovering

34+iopartial = Partial ExternalIO

34

35

35primitives :: [Prim]

36primitives :: [Prim]

36primitives =

37primitives =

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

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

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

165 (1, LStrRev) total,

166 (1, LStrRev) total,

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

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

167− (1, LReadStr) partial,

168+ (1, LReadStr) iopartial,

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

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

169 (0, LVMPtr) total,

170 (0, LVMPtr) total,

170 -- Streams

171 -- Streams

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

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

172− (0, LStdIn) partial,

173+ (0, LStdIn) iopartial,

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

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

174− (0, LStdOut) partial,

175+ (0, LStdOut) iopartial,

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

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

176− (0, LStdErr) partial,

177+ (0, LStdErr) iopartial,

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

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

178 (0, LNullPtr) total,

179 (0, LNullPtr) total,

179 -- Managed pointer registration

180 -- Managed pointer registration