e7a35e9 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Remove implicit qualifier for 'effect'

Two reasons: 1. The most important: it makes error messages *so much better* :). Because "effect'" rarely properly fails due to having a very generic type, so any error arises later and breaks the real error which came from lift' 2. It is much easier to explain what's going on when documenting effects! Apologies for breaking effectful code: I now think it is much better this way though.

commite7a35e93e0e87d2029dafec16e85edd73d862ce1 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 25 May 2014, 17:05 (12 years ago) parent636e6e1

14 files changed+58−51

compare with master

unifiedsplit

libs/effects/Effect/Exception.idr+1−1 libs/effects/Effect/File.idr+5−5 libs/effects/Effect/Memory.idr+7−7 libs/effects/Effect/Random.idr+3−3 libs/effects/Effect/Select.idr+1−1 libs/effects/Effect/State.idr+3−3 libs/effects/Effect/StdIO.idr+4−4 libs/effects/Effect/System.idr+3−3 libs/effects/Effects.idr+16−16 src/Idris/AbsSyntaxTree.hs+1 src/Idris/Core/Elaborate.hs+2−1 src/Idris/Core/TT.hs+6−2 src/Idris/ElabTerm.hs+4−3 test/basic006/expected+2−2

libs/effects/Effect/Exception.idr+1−1

@@ -27,7 +27,7 @@ EXCEPTION : Type -> EFFECT

2727EXCEPTION t = MkEff () (Exception t)

2828

2929raise : a -> { [EXCEPTION a ] } Eff m b

30−raise err = Raise err

30+raise err = effect $ Raise err

3131

3232

3333

libs/effects/Effect/File.idr+5−5

@@ -107,27 +107,27 @@ open : Handler FileIO e =>

107107 -> { [FILE_IO ()] ==> [FILE_IO (if result

108108 then OpenFile m

109109 else ())] } Eff e Bool

110−open f m = Open f m

110+open f m = effect $ Open f m

111111

112112

113113||| Close a file.

114114close : Handler FileIO e =>

115115 { [FILE_IO (OpenFile m)] ==> [FILE_IO ()] } Eff e ()

116−close = Close

116+close = effect $ Close

117117

118118||| Read a line from the file.

119119readLine : Handler FileIO e =>

120120 { [FILE_IO (OpenFile Read)] } Eff e String

121−readLine = ReadLine

121+readLine = effect $ ReadLine

122122

123123||| Write a line to a file.

124124writeLine : Handler FileIO e =>

125125 String -> { [FILE_IO (OpenFile Write)] } Eff e ()

126−writeLine str = WriteLine str

126+writeLine str = effect $ WriteLine str

127127

128128||| End of file?

129129eof : Handler FileIO e =>

130130 { [FILE_IO (OpenFile Read)] } Eff e Bool

131−eof = EOF

131+eof = effect $ EOF

132132

133133-- --------------------------------------------------------------------- [ EOF ]

libs/effects/Effect/Memory.idr+7−7

@@ -102,7 +102,7 @@ RAW_MEMORY t = MkEff t RawMemory

102102

103103allocate : (n : Nat) ->

104104 Eff m () [RAW_MEMORY ()] (\v => [RAW_MEMORY (MemoryChunk n 0)])

105−allocate size = Allocate size

105+allocate size = effect $ Allocate size

106106

107107initialize : {i : Nat} ->

108108 {n : Nat} ->

@@ -111,17 +111,17 @@ initialize : {i : Nat} ->

111111 so (i + size <= n) ->

112112 Eff m () [RAW_MEMORY (MemoryChunk n i)]

113113 (\v => [RAW_MEMORY (MemoryChunk n (i + size))])

114−initialize c size prf = Initialize c size prf

114+initialize c size prf = effect $ Initialize c size prf

115115

116116free : Eff m () [RAW_MEMORY (MemoryChunk n i)] (\v => [RAW_MEMORY ()])

117−free = Free

117+free = effect Free

118118

119119peek : {i : Nat} ->

120120 (offset : Nat) ->

121121 (size : Nat) ->

122122 so (offset + size <= i) ->

123123 { [RAW_MEMORY (MemoryChunk n i)] } Eff m (Vect size Bits8)

124−peek offset size prf = Peek offset size prf

124+peek offset size prf = effect $ Peek offset size prf

125125

126126poke : {n : Nat} ->

127127 {i : Nat} ->

@@ -130,11 +130,11 @@ poke : {n : Nat} ->

130130 so (offset <= i && offset + size <= n) ->

131131 Eff m () [RAW_MEMORY (MemoryChunk n i)]

132132 (\v => [RAW_MEMORY (MemoryChunk n (max i (offset + size)))])

133−poke offset content prf = Poke offset content prf

133+poke offset content prf = effect $ Poke offset content prf

134134

135135private

136136getRawPtr : { [RAW_MEMORY (MemoryChunk n i)] } Eff m (MemoryChunk n i)

137−getRawPtr = GetRawPtr

137+getRawPtr = effect $ GetRawPtr

138138

139139private

140140move' : {dst_size : Nat} ->

@@ -149,7 +149,7 @@ move' : {dst_size : Nat} ->

149149 Eff m () [RAW_MEMORY (MemoryChunk dst_size dst_init)]

150150 (\v => [RAW_MEMORY (MemoryChunk dst_size (max dst_init (dst_offset + size)))])

151151move' src_ptr dst_offset src_offset size dst_bounds src_bounds

152− = Move src_ptr dst_offset src_offset size dst_bounds src_bounds

152+ = effect $ Move src_ptr dst_offset src_offset size dst_bounds src_bounds

153153

154154data MoveDescriptor = Dst | Src

155155

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

@@ -18,14 +18,14 @@ RND = MkEff Integer Random

1818

1919||| Generates a random Integer in a given range

2020rndInt : Integer -> Integer -> { [RND] } Eff m Integer

21−rndInt lower upper = do v <- getRandom

21+rndInt lower upper = do v <- effect $ getRandom

2222 return (v `prim__sremBigInt` (upper - lower) + lower)

2323

2424||| Generate a random number in Fin (S `k`)

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 = assert_total $ !getRandom `prim__sremBigInt` (cast (S k))

28+rndFin k = do let v = assert_total $ !(effect 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

@@ -43,5 +43,5 @@ rndSelect (x::xs) = return (Just !(rndSelect' (x::(fromList xs))))

4343

4444||| Sets the random seed

4545srand : Integer -> { [RND] } Eff m ()

46−srand n = setSeed n

46+srand n = effect $ setSeed n

4747

libs/effects/Effect/Select.idr+1−1

@@ -19,5 +19,5 @@ SELECT : EFFECT

1919SELECT = MkEff () Selection

2020

2121select : List a -> { [SELECT] } Eff m a

22−select xs = Select xs

22+select xs = effect $ Select xs

2323

libs/effects/Effect/State.idr+3−3

@@ -17,13 +17,13 @@ STATE : Type -> EFFECT

1717STATE t = MkEff t State

1818

1919get : { [STATE x] } Eff m x

20−get = Get

20+get = effect $ Get

2121

2222put : x -> { [STATE x] } Eff m ()

23−put val = Put val

23+put val = effect $ Put val

2424

2525putM : y -> { [STATE x] ==> [STATE y] } Eff m ()

26−putM val = Put val

26+putM val = effect $ Put val

2727

2828update : (x -> x) -> { [STATE x] } Eff m ()

2929update f = put (f !get)

libs/effects/Effect/StdIO.idr+4−4

@@ -40,11 +40,11 @@ STDIO = MkEff () StdIO

4040

4141||| Write a string to standard output.

4242putStr : Handler StdIO e => String -> { [STDIO] } Eff e ()

43−putStr s = PutStr s

43+putStr s = effect $ PutStr s

4444

4545||| Write a character to standard output.

4646putChar : Handler StdIO e => Char -> { [STDIO] } Eff e ()

47−putChar c = PutCh c

47+putChar c = effect $ PutCh c

4848

4949||| Write a string to standard output, terminating with a newline.

5050putStrLn : Handler StdIO e => String -> { [STDIO] } Eff e ()

@@ -52,9 +52,9 @@ putStrLn s = putStr (s ++ "\n")

5252

5353||| Read a string from standard input.

5454getStr : Handler StdIO e => { [STDIO] } Eff e String

55−getStr = GetStr

55+getStr = effect $ GetStr

5656

5757||| Read a character from standard input.

5858getChar : Handler StdIO e => { [STDIO] } Eff e Char

59−getChar = GetCh

59+getChar = effect $ GetCh

6060

libs/effects/Effect/System.idr+3−3

@@ -28,11 +28,11 @@ SYSTEM : EFFECT

2828SYSTEM = MkEff () System

2929

3030getArgs : Handler System e => { [SYSTEM] } Eff e (List String)

31−getArgs = Args

31+getArgs = effect Args

3232

3333time : Handler System e => { [SYSTEM] } Eff e Int

34−time = Time

34+time = effect Time

3535

3636getEnv : Handler System e => String -> { [SYSTEM] } Eff e (Maybe String)

37−getEnv s = GetEnv s

37+getEnv s = effect $ GetEnv s

3838

libs/effects/Effects.idr+16−16

@@ -144,11 +144,11 @@ data Eff : (m : Type -> Type)

144144 Eff m a xs xs'

145145 ebind : Eff m a xs xs' ->

146146 ((val : a) -> Eff m b (xs' val) xs'') -> Eff m b xs xs''

147− effect : (prf : EffElem e a xs) ->

147+ effectP : (prf : EffElem e a xs) ->

148148 (eff : e t a b) ->

149149 Eff m t xs (\v => updateResTy v xs prf eff)

150150

151− lift : (prf : SubList ys xs) ->

151+ liftP : (prf : SubList ys xs) ->

152152 Eff m t ys ys' -> Eff m t xs (\v => updateWith (ys' v) xs prf)

153153 newInit : Handler e m =>

154154 res ->

@@ -204,8 +204,8 @@ eff env (value x) k = k x env

204204eff env (with_val x prog) k = eff env prog (\p', env' => k x env')

205205eff env (prog `ebind` c) k

206206 = eff env prog (\p', env' => eff env' (c p') k)

207−eff env (effect prf effP) k = execEff env prf effP k

208−eff env (lift prf effP) k

207+eff env (effectP prf effP) k = execEff env prf effP k

208+eff env (liftP prf effP) k

209209 = let env' = dropEnv env prf in

210210 eff env' effP (\p', envk => k p' (rebuildEnv envk prf env))

211211eff env (newInit r prog) k

@@ -233,20 +233,20 @@ syntax MkDefaultEnv = with Env

233233 [default, default, default, default, default, default, default],

234234 [default, default, default, default, default, default, default, default] |)

235235

236−implicit

237−lift' : Eff m t ys ys' ->

238− {default tactics { search 100; }

239− prf : SubList ys xs} ->

240− Eff m t xs (\v => updateWith (ys' v) xs prf)

241−lift' e {prf} = lift prf e

236+effect : {a, b: _} -> {e : Effect} ->

237+ (eff : e t a b) ->

238+ {default tactics { search 100; }

239+ prf : EffElem e a xs} ->

240+ Eff m t xs (\v => updateResTy v xs prf eff)

241+effect e {prf} = effectP prf e

242242

243243implicit

244−effect' : {a, b: _} -> {e : Effect} ->

245− (eff : e t a b) ->

246− {default tactics { search 100; }

247− prf : EffElem e a xs} ->

248− Eff m t xs (\v => updateResTy v xs prf eff)

249−effect' e {prf} = effect prf e

244+lift : Eff m t ys ys' ->

245+ {default tactics { search 100; }

246+ prf : SubList ys xs} ->

247+ Eff m t xs (\v => updateWith (ys' v) xs prf)

248+lift e {prf} = liftP prf e

249+

250250

251251new : Handler e m =>

252252 {default default r : res} ->

src/Idris/AbsSyntaxTree.hs+1

@@ -1338,6 +1338,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd

13381338 prettySe p bnd PImpossible = kwd "impossible"

13391339 prettySe p bnd Placeholder = text "_"

13401340 prettySe p bnd (PDoBlock _) = text "do block pretty not implemented"

1341+ prettySe p bnd (PCoerced t) = prettySe p bnd t

13411342 prettySe p bnd (PElabError s) = pretty s

13421343

13431344 prettySe p bnd _ = text "test"

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

@@ -695,6 +695,7 @@ try' t1 t2 proofSearch

695695 = -- traceWhen r (show err) $

696696 r || proofSearch

697697 recoverableErr (CantSolveGoal _ _) = False

698+ recoverableErr (ProofSearchFail (Msg _)) = True

698699 recoverableErr (ProofSearchFail _) = False

699700 recoverableErr (ElaboratingArg _ _ _ e) = recoverableErr e

700701 recoverableErr (At _ e) = recoverableErr e

@@ -724,7 +725,7 @@ tryAll xs = tryAll' [] 999999 (cantResolve, 0) xs

724725 = do s <- get

725726 ps <- get_probs

726727 case prunStateT pmax True ps x s of

727− OK ((v, newps, probs), s') ->

728+ OK ((v, newps, probs), s') ->

728729 do let cs' = if (newps < pmax)

729730 then [do put s'; return $! v]

730731 else (do put s'; return $! v) : cs

src/Idris/Core/TT.hs+6−2

@@ -184,9 +184,12 @@ score :: Err -> Int

184184score (CantUnify _ _ _ m _ s) = s + score m

185185score (CantResolve _) = 20

186186score (NoSuchVariable _) = 1000

187−score (ProofSearchFail _) = 10000

188−score (CantSolveGoal _ _) = 10000

187+score (ProofSearchFail e) = score e

188+score (CantSolveGoal _ _) = 100000

189189score (InternalMsg _) = -1

190+score (At _ e) = score e

191+score (ElaboratingArg _ _ _ e) = score e

192+score (Elaborating _ _ e) = score e

190193score _ = 0

191194

192195instance Show Err where

@@ -203,6 +206,7 @@ instance Show Err where

203206 show (ElaboratingArg f x prev e) = "Elaborating " ++ show f ++ " arg " ++

204207 show x ++ ": " ++ show e

205208 show (Elaborating what n e) = "Elaborating " ++ what ++ show n ++ ":" ++ show e

209+ show (ProofSearchFail e) = "Proof search fail: " ++ show e

206210 show _ = "Error"

207211

208212instance Pretty Err OutputAnnotation where

src/Idris/ElabTerm.hs+4−3

@@ -495,6 +495,7 @@ elab ist info pattern opts fn tm

495495 where alt t = case getTm t of

496496 PAlternative False _ -> 5

497497 PAlternative True _ -> 1

498+ PTactics _ -> 150

498499 PLam _ _ _ -> 2

499500 PRewrite _ _ _ _ -> 3

500501 _ -> 0

@@ -822,9 +823,9 @@ findInstances ist t

822823trivial' ist

823824 = trivial (elab ist toplevel False [] (sMN 0 "tac")) ist

824825proofSearch' ist rec depth prv top n hints

825− = proofSearch rec prv depth

826− (elab ist toplevel False [] (sMN 0 "tac")) top n hints ist

827−

826+ = do unifyProblems

827+ proofSearch rec prv depth

828+ (elab ist toplevel False [] (sMN 0 "tac")) top n hints ist

828829

829830resolveTC :: Int -> Term -> Name -> IState -> ElabD ()

830831resolveTC = resTC' []

test/basic006/expected+2−2

@@ -1,5 +1,5 @@

1−When elaborating right hand side of foo:

2−test020a.idr:14:18:When elaborating an application of function Prelude.List.reverse:

1+test020a.idr:14:18:When elaborating right hand side of foo:

2+When elaborating an application of function Prelude.List.reverse:

33 Can't unify

44 Vect n a

55 with