2bf5a3c · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Clean up implementation of type providers

2bf5a3cDavid Christiansen13 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+39−17

@@ -214,26 +214,48 @@ 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 if not (TypeProviders `elem` idris_language_extensions i)

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

219 then 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+ else do ctxt <- getContext

221− let using = unProv fc tm

222+

222− logLvl 1 $ "Providing " ++

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

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

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

224− " as " ++ show using

225+ unless (isTType typ) $

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

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

226− ctxt <- getContext

227+

227− let str = show e' in

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

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

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

229− let et' = normaliseAll ctxt [] et

230+ unless (isProviderOf ty' et) $

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

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

233+

234+ -- Create the top-level type declaration

230 elabType info syn "" fc [] n ty

235 elabType info syn "" fc [] n ty

236+

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

231− rhs <- execute e'

238+ rhs <- execute e

239+ let rhs' = normalise ctxt [] rhs

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

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

233− providerError rhs

241+

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

243+ tm <- getProvided rhs'

244+

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

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

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

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

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

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

248+

249+ where isTType :: TT Name -> Bool

250+ isTType (TType _) = True

251+ isTType _ = False

252+

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

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

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

256+ , tp == tp' = True

257+ isProviderOf _ _ = False

258+

237

259

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

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

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

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

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."