git.iko.soy/Idris-dev
on master help sign in
Update type providers so that the decision of failure or otherwise is made in IO
0752bedDavid Christiansen
lib/Providers.idr+4−3
compare with master
unifiedsplit
@@ -1,8 +1,9 @@
1module Providers
1module Providers
2
2
3public
3public
4−data Provider a = Provide (IO a) | Error (IO String)
4+data Provider a = Provide a | Error String
5
5
6partial public
6partial public
7−unProv : Provider a -> a
7+unProv : IO (Provider a) -> a
8−unProv (Provide x) = unsafePerformIO x
8+unProv p = case unsafePerformIO p of
9+ Provide x => x
src/Idris/Providers.hs+7−13
@@ -1,3 +1,4 @@
1+{-# LANGUAGE PatternGuards #-}
1module Idris.Providers where
2module Idris.Providers where
2
3
3import Core.TT
4import Core.TT
@@ -19,16 +20,9 @@ unProv fc tm = PApp fc (PRef fc $ NS (UN "unProv") ["Providers"]) [PExp 0 False
19
20
20-- | Handle an error, if the type provider returned an error. Otherwise do nothing.
21-- | Handle an error, if the type provider returned an error. Otherwise do nothing.
21providerError :: TT Name -> Idris ()
22providerError :: TT Name -> Idris ()
22−providerError tm = case unApply tm of
23+providerError tm | (P _ unProv_case _, _:_:tm':_) <- unApply tm
23− (P _ (NS (UN "unProv") ["Providers"]) _, [_, tm']) ->
24− case unApply tm' of
25− (P _ (NS (UN "Error") ["Providers"]) _, [_, err]) ->
24+ , (P _ (NS (UN "Error") ["Providers"]) _, [_, err]) <- unApply tm' =
26− do str <- execute err
27− case (unApply str) of
25+ case err of
28− (Constant (Str msg), []) ->
29− ierror . ProviderError $ msg
30− (P _ (UN "prim__IO") _, [_, (Constant (Str msg))]) ->
31− ierror . ProviderError $ msg
26+ Constant (Str msg) -> ierror . ProviderError $ msg
32− _ -> fail "Error in type provider."
27+ _ -> fail "Error in type provider"
33− _ -> return ()
34− _ -> return ()
28+ | otherwise = return ()
test/test023/test023.idr+4−4
@@ -7,8 +7,8 @@ import Providers
7%language TypeProviders
7%language TypeProviders
8
8
9-- Provide the Unit type
9-- Provide the Unit type
10−goodProvider : Provider Type
10+goodProvider : IO (Provider Type)
11−goodProvider = Provide (return (the Type ()))
11+goodProvider = return (Provide (the Type ()))
12
12
13%provide (Unit : Type) with goodProvider
13%provide (Unit : Type) with goodProvider
14
14
@@ -16,8 +16,8 @@ foo : Unit
16foo = ()
16foo = ()
17
17
18-- Always fail
18-- Always fail
19−badProvider : Provider Type
19+badProvider : IO (Provider Type)
20−badProvider = Error (return "Always fails")
20+badProvider = return (Error "Always fails")
21
21
22%provide (t : Type) with badProvider
22%provide (t : Type) with badProvider
23
23