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
commit0752bedfdce66d035834597e66bd425d7c3596cf authorDavid Christiansen <david@davidchristiansen.dk> dateFri 5 Apr 2013, 12:11 (14 years ago) parentff0fbfa
3 files changed+15−20
compare with master
unifiedsplit
lib/Providers.idr+4−3 src/Idris/Providers.hs+7−13 test/test023/test023.idr+4−4
lib/Providers.idr+4−3
@@ -1,8 +1,9 @@
11module Providers
22
33public
4−data Provider a = Provide (IO a) | Error (IO String)
4+data Provider a = Provide a | Error String
55
66partial public
7−unProv : Provider a -> a
8−unProv (Provide x) = unsafePerformIO x
7+unProv : IO (Provider a) -> a
8+unProv p = case unsafePerformIO p of
9+ Provide x => x
src/Idris/Providers.hs+7−13
@@ -1,3 +1,4 @@
1+{-# LANGUAGE PatternGuards #-}
12module Idris.Providers where
23
34import Core.TT
@@ -19,16 +20,9 @@ unProv fc tm = PApp fc (PRef fc $ NS (UN "unProv") ["Providers"]) [PExp 0 False
1920
2021-- | Handle an error, if the type provider returned an error. Otherwise do nothing.
2122providerError :: TT Name -> Idris ()
22−providerError tm = case unApply tm of
23− (P _ (NS (UN "unProv") ["Providers"]) _, [_, tm']) ->
24− case unApply tm' of
25− (P _ (NS (UN "Error") ["Providers"]) _, [_, err]) ->
26− do str <- execute err
27− case (unApply str) of
28− (Constant (Str msg), []) ->
29− ierror . ProviderError $ msg
30− (P _ (UN "prim__IO") _, [_, (Constant (Str msg))]) ->
31− ierror . ProviderError $ msg
32− _ -> fail "Error in type provider."
33− _ -> return ()
34− _ -> return ()
23+providerError tm | (P _ unProv_case _, _:_:tm':_) <- unApply tm
24+ , (P _ (NS (UN "Error") ["Providers"]) _, [_, err]) <- unApply tm' =
25+ case err of
26+ Constant (Str msg) -> ierror . ProviderError $ msg
27+ _ -> fail "Error in type provider"
28+ | otherwise = return ()
test/test023/test023.idr+4−4
@@ -7,8 +7,8 @@ import Providers
77%language TypeProviders
88
99-- Provide the Unit type
10−goodProvider : Provider Type
11−goodProvider = Provide (return (the Type ()))
10+goodProvider : IO (Provider Type)
11+goodProvider = return (Provide (the Type ()))
1212
1313%provide (Unit : Type) with goodProvider
1414
@@ -16,8 +16,8 @@ foo : Unit
1616foo = ()
1717
1818-- Always fail
19−badProvider : Provider Type
20−badProvider = Error (return "Always fails")
19+badProvider : IO (Provider Type)
20+badProvider = return (Error "Always fails")
2121
2222%provide (t : Type) with badProvider
2323