235eb87 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #317 from david-christiansen/providers

235eb87Edwin Brady13 years ago

lib/Providers.idr−4

compare with master

unifiedsplit

@@ -3,7 +3,3 @@ module Providers

3public

4data Provider a = Provide a | Error String

6−partial public

7−unProv : IO (Provider a) -> a

8−unProv p = case unsafePerformIO p of

9− Provide x => x

src/Idris/ElabDecls.hs+44−20

@@ -214,26 +214,50 @@ elabData info syn doc fc codata (PDatadecl n t_in dcons)

214elabProvider :: ElabInfo -> SyntaxInfo -> FC -> Name -> PTerm -> PTerm -> Idris ()

215elabProvider info syn fc n ty tm

216 = do i <- getIState

217+ -- Ensure that the experimental extension is enabled

217− if not (TypeProviders `elem` idris_language_extensions i)

218+ unless (TypeProviders `elem` idris_language_extensions i) $

218− then fail $ "Failed to define type provider \"" ++ show n ++

219+ fail $ "Failed to define type provider \"" ++ show n ++

219− "\".\nYou must turn on TypeProviders extension."

220+ "\".\nYou must turn on the TypeProviders extension."

220− else do let expected = providerTy fc ty

221+

221− let using = unProv fc tm

222− logLvl 1 $ "Providing " ++

223− show n ++ " : " ++ show expected ++

224− " as " ++ show using

225− (e', et) <- elabVal toplevel False using

226− ctxt <- getContext

222+ ctxt <- getContext

227− let str = show e' in

223+

228− logLvl 1 $ "Term is " ++ if length str > 200 then (take 200 str) ++ "..." else str

224+ -- First elaborate the expected type (and check that it's a type)

229− let et' = normaliseAll ctxt [] et

225+ (ty', typ) <- elabVal toplevel False ty

226+ unless (isTType typ) $

227+ fail ("Expected a type, got " ++ show ty' ++ " : " ++ show typ)

228+

229+ -- Elaborate the provider term to TT and check that the type matches

230+ (e, et) <- elabVal toplevel False tm

231+ unless (isProviderOf ty' et) $

232+ fail $ "Expected provider type IO (Provider (" ++

233+ show ty' ++ "))" ++ ", got " ++ show et ++ " instead."

234+

235+ -- Create the top-level type declaration

230− elabType info syn "" fc [] n ty

236+ elabType info syn "" fc [] n ty

237+

238+ -- Execute the type provider and normalise the result

231− rhs <- execute e'

239+ rhs <- execute e

240+ let rhs' = normalise ctxt [] rhs

232− logLvl 1 $ "Normalized " ++ show n ++ "'s RHS to " ++ show rhs

241+ logLvl 1 $ "Normalised " ++ show n ++ "'s RHS to " ++ show rhs

233− providerError rhs

242+

243+ -- Extract the provided term from the type provider

244+ tm <- getProvided rhs'

245+

246+ -- Finally add a top-level definition of the provided term

234− elabClauses info fc [] n [PClause fc n (PRef fc $ n) [] (delab i rhs) []]

247+ elabClauses info fc [] n [PClause fc n (PRef fc n) [] (delab i tm) []]

235− logLvl 1 $ "** Elaborated: " ++ show e' ++ " :as: " ++ show et

248+ logLvl 1 $ "Elaborated provider " ++ show n ++ " as: " ++ show tm

236− logLvl 1 $ "** Evaluated: " ++ show rhs ++ " :as: " ++ show et'

249+

250+ where isTType :: TT Name -> Bool

251+ isTType (TType _) = True

252+ isTType _ = False

253+

254+ isProviderOf :: TT Name -> TT Name -> Bool

255+ isProviderOf tp prov

256+ | (P _ (UN "IO") _, [prov']) <- unApply prov

257+ , (P _ (NS (UN "Provider") ["Providers"]) _, [tp']) <- unApply prov'

258+ , tp == tp' = True

259+ isProviderOf _ _ = False

260+

237

261

238elabRecord :: ElabInfo -> SyntaxInfo -> String -> FC -> Name ->

262elabRecord :: ElabInfo -> SyntaxInfo -> String -> FC -> Name ->

239 PTerm -> String -> Name -> PTerm -> Idris ()

263 PTerm -> String -> Name -> PTerm -> Idris ()

src/Idris/Error.hs+1−1

@@ -45,7 +45,7 @@ instance Exception IdrisErr

45ifail :: String -> Idris ()

46ifail str = throwIO (IErr str)

48−ierror :: Err -> Idris ()

48+ierror :: Err -> Idris a

49ierror err = do i <- getIState

50 throwIO (IErr $ pshow i err)

src/Idris/Providers.hs+11−11

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

1{-# LANGUAGE PatternGuards #-}

2−module Idris.Providers where

2+module Idris.Providers (providerTy, getProvided) where

4import Core.TT

5import Core.Evaluate

@@ -14,15 +14,15 @@ import Debug.Trace

14providerTy :: FC -> PTerm -> PTerm

15providerTy fc tm = PApp fc (PRef fc $ UN "Provider") [PExp 0 False tm ""]

17−-- | Wrap the RHS of a type provider definition

18−unProv :: FC -> PTerm -> PTerm

19−unProv fc tm = PApp fc (PRef fc $ NS (UN "unProv") ["Providers"]) [PExp 0 False tm ""]

20−

21−-- | Handle an error, if the type provider returned an error. Otherwise do nothing.

17+-- | Handle an error, if the type provider returned an error. Otherwise return the provided term.

22−providerError :: TT Name -> Idris ()

18+getProvided :: TT Name -> Idris (TT Name)

23−providerError tm | (P _ unProv_case _, _:_:tm':_) <- unApply tm

19+getProvided tm | (P _ (UN "io_return") _, [tp, result]) <- unApply tm

24− , (P _ (NS (UN "Error") ["Providers"]) _, [_, err]) <- unApply tm' =

20+ , (P _ (NS (UN "Error") ["Providers"]) _, [_, err]) <- unApply result =

25 case err of

21 case err of

26 Constant (Str msg) -> ierror . ProviderError $ msg

22 Constant (Str msg) -> ierror . ProviderError $ msg

27− _ -> fail "Error in type provider"

23+ _ -> fail "Internal error in type provider, non-normalised error"

24+ | (P _ (UN "io_return") _, [tp, result]) <- unApply tm

25+ , (P _ (NS (UN "Provide") ["Providers"]) _, [_, res]) <- unApply result =

28− | otherwise = return ()

26+ return res

27+ | otherwise = fail $ "Internal type provider error: result was not " ++

28+ "IO (Provider a), or perhaps missing normalisation."