e7a35e9 · Idris-dev · git.iko.soy

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

compare with master

unifiedsplit

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

27EXCEPTION t = MkEff () (Exception t)

28

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

30−raise err = Raise err

30+raise err = effect $ Raise err

31

32

33

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

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

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

108 then OpenFile m

109 else ())] } Eff e Bool

110−open f m = Open f m

110+open f m = effect $ Open f m

111

112

113||| Close a file.

114close : Handler FileIO e =>

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

116−close = Close

116+close = effect $ Close

117

118||| Read a line from the file.

119readLine : Handler FileIO e =>

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

121−readLine = ReadLine

121+readLine = effect $ ReadLine

122

123||| Write a line to a file.

124writeLine : Handler FileIO e =>

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

126−writeLine str = WriteLine str

126+writeLine str = effect $ WriteLine str

127

128||| End of file?

129eof : Handler FileIO e =>

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

131−eof = EOF

131+eof = effect $ EOF

132

133-- --------------------------------------------------------------------- [ EOF ]

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

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

102

103allocate : (n : Nat) ->

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

105−allocate size = Allocate size

105+allocate size = effect $ Allocate size

106

107initialize : {i : Nat} ->

108 {n : Nat} ->

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

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

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

113 (\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

115

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

117−free = Free

117+free = effect Free

118

119peek : {i : Nat} ->

120 (offset : Nat) ->

121 (size : Nat) ->

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

123 { [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

125

126poke : {n : Nat} ->

127 {i : Nat} ->

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

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

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

132 (\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

134

135private

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

137−getRawPtr = GetRawPtr

137+getRawPtr = effect $ GetRawPtr

138

139private

140move' : {dst_size : Nat} ->

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

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

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

151move' 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

153

154data MoveDescriptor = Dst | Src

155

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

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

18

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

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

21−rndInt lower upper = do v <- getRandom

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

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

23

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

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

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

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

43

44||| Sets the random seed

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

46−srand n = setSeed n

46+srand n = effect $ setSeed n

47

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

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

19SELECT = MkEff () Selection

20

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

22−select xs = Select xs

22+select xs = effect $ Select xs

23

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

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

17STATE t = MkEff t State

18

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

20−get = Get

20+get = effect $ Get

21

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

23−put val = Put val

23+put val = effect $ Put val

24

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

26−putM val = Put val

26+putM val = effect $ Put val

27

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

29update f = put (f !get)

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

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

40

41||| Write a string to standard output.

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

43−putStr s = PutStr s

43+putStr s = effect $ PutStr s

44

45||| Write a character to standard output.

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

47−putChar c = PutCh c

47+putChar c = effect $ PutCh c

48

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

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

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

52

53||| Read a string from standard input.

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

55−getStr = GetStr

55+getStr = effect $ GetStr

56

57||| Read a character from standard input.

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

59−getChar = GetCh

59+getChar = effect $ GetCh

60

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

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

28SYSTEM = MkEff () System

29

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

31−getArgs = Args

31+getArgs = effect Args

32

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

34−time = Time

34+time = effect Time

35

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

37−getEnv s = GetEnv s

37+getEnv s = effect $ GetEnv s

38

libs/effects/Effects.idr+16−16

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

144 Eff m a xs xs'

145 ebind : Eff m a xs xs' ->

146 ((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) ->

148 (eff : e t a b) ->

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

150

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

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

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

153 newInit : Handler e m =>

154 res ->

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

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

205eff env (prog `ebind` c) k

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

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

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

208−eff env (lift prf effP) k

208+eff env (liftP prf effP) k

209 = let env' = dropEnv env prf in

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

211eff env (newInit r prog) k

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

233 [default, default, default, default, default, default, default],

234 [default, default, default, default, default, default, default, default] |)

235

236−implicit

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

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

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

238− {default tactics { search 100; }

238+ {default tactics { search 100; }

239− prf : SubList ys xs} ->

239+ prf : EffElem e a xs} ->

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

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

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

241+effect e {prf} = effectP prf e

242

243implicit

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

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

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

246− {default tactics { search 100; }

245+ {default tactics { search 100; }

247− prf : EffElem e a xs} ->

246+ prf : SubList ys xs} ->

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

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

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

248+lift e {prf} = liftP prf e

249+

250

251new : Handler e m =>

252 {default default r : res} ->

src/Idris/AbsSyntaxTree.hs+1

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

1338 prettySe p bnd PImpossible = kwd "impossible"

1339 prettySe p bnd Placeholder = text "_"

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

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

1341 prettySe p bnd (PElabError s) = pretty s

1342 prettySe p bnd (PElabError s) = pretty s

1342

1343

1343 prettySe p bnd _ = text "test"

1344 prettySe p bnd _ = text "test"

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

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

695 = -- traceWhen r (show err) $

696 r || proofSearch

697 recoverableErr (CantSolveGoal _ _) = False

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

698 recoverableErr (ProofSearchFail _) = False

699 recoverableErr (ProofSearchFail _) = False

699 recoverableErr (ElaboratingArg _ _ _ e) = recoverableErr e

700 recoverableErr (ElaboratingArg _ _ _ e) = recoverableErr e

700 recoverableErr (At _ e) = recoverableErr e

701 recoverableErr (At _ e) = recoverableErr e

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

724 = do s <- get

725 = do s <- get

725 ps <- get_probs

726 ps <- get_probs

726 case prunStateT pmax True ps x s of

727 case prunStateT pmax True ps x s of

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

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

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

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

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

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

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

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

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

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

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

185score (CantResolve _) = 20

186score (NoSuchVariable _) = 1000

187−score (ProofSearchFail _) = 10000

187+score (ProofSearchFail e) = score e

188−score (CantSolveGoal _ _) = 10000

188+score (CantSolveGoal _ _) = 100000

189score (InternalMsg _) = -1

190+score (At _ e) = score e

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

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

190score _ = 0

193score _ = 0

191

194

192instance Show Err where

195instance Show Err where

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

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

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

204 show x ++ ": " ++ show e

207 show x ++ ": " ++ show e

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

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

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

206 show _ = "Error"

210 show _ = "Error"

207

211

208instance Pretty Err OutputAnnotation where

212instance Pretty Err OutputAnnotation where

src/Idris/ElabTerm.hs+4−3

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

495 where alt t = case getTm t of

496 PAlternative False _ -> 5

497 PAlternative True _ -> 1

498+ PTactics _ -> 150

498 PLam _ _ _ -> 2

499 PLam _ _ _ -> 2

499 PRewrite _ _ _ _ -> 3

500 PRewrite _ _ _ _ -> 3

500 _ -> 0

501 _ -> 0

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

822trivial' ist

823trivial' ist

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

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

824proofSearch' ist rec depth prv top n hints

825proofSearch' ist rec depth prv top n hints

826+ = do unifyProblems

825− = proofSearch rec prv depth

827+ proofSearch rec prv depth

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

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

827−

828

829

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

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

830resolveTC = resTC' []

831resolveTC = resTC' []

test/basic006/expected+2−2

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

1−When elaborating right hand side of foo:

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

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

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

3 Can't unify

4 Vect n a

5 with