@@ -215,45 +215,47 @@ elabProvider :: ElabInfo -> SyntaxInfo -> FC -> Name -> PTerm -> PTerm -> Idris
215elabProvider info syn fc n ty tm
215elabProvider info syn fc n ty tm
216 = do i <- getIState
216 = do i <- getIState
217 -- Ensure that the experimental extension is enabled
217 -- Ensure that the experimental extension is enabled
218− if not (TypeProviders `elem` idris_language_extensions i)
218+ unless (TypeProviders `elem` idris_language_extensions i) $
219− then fail $ "Failed to define type provider \"" ++ show n ++
219+ fail $ "Failed to define type provider \"" ++ show n ++
220− "\".\nYou must turn on the TypeProviders extension."
220+ "\".\nYou must turn on the TypeProviders extension."
221− else do ctxt <- getContext
223− -- First elaborate the expected type (and check that it's a type)
224+ -- First elaborate the expected type (and check that it's a type)
224− (ty', typ) <- elabVal toplevel False ty
225+ (ty', typ) <- elabVal toplevel False ty
225− unless (isTType typ) $
226+ unless (isTType typ) $
226− (fail $ "Expected a type, got " ++ show ty' ++ " : " ++ show typ)
227+ (fail $ "Expected a type, got " ++ show ty' ++ " : " ++ show typ)
228− -- Elaborate the provider term to TT and check that the type matches
229+ -- Elaborate the provider term to TT and check that the type matches
229− (e, et) <- elabVal toplevel False tm
230+ (e, et) <- elabVal toplevel False tm
230− unless (isProviderOf ty' et) $
231+ unless (isProviderOf ty' et) $
231− fail $ "Expected provider type IO (Provider (" ++
232+ fail $ "Expected provider type IO (Provider (" ++
232− show ty' ++ "))" ++ ", got " ++ show et ++ " instead."
233+ show ty' ++ "))" ++ ", got " ++ show et ++ " instead."
234− -- Create the top-level type declaration
235+ -- Create the top-level type declaration
235− elabType info syn "" fc [] n ty
236+ elabType info syn "" fc [] n ty
237− -- Execute the type provider and normalise the result
238+ -- Execute the type provider and normalise the result
238− rhs <- execute e
239+ rhs <- execute e
239− let rhs' = normalise ctxt [] rhs
240+ let rhs' = normalise ctxt [] rhs
240− logLvl 1 $ "Normalised " ++ show n ++ "'s RHS to " ++ show rhs
241+ logLvl 1 $ "Normalised " ++ show n ++ "'s RHS to " ++ show rhs
242− -- Extract the provided term from the type provider
243+ -- Extract the provided term from the type provider
243− tm <- getProvided rhs'
244+ tm <- getProvided rhs'
245− -- Finally add a top-level definition of the provided term
246+ -- Finally add a top-level definition of the provided term
246− elabClauses info fc [] n [PClause fc n (PRef fc $ n) [] (delab i tm) []]
247+ elabClauses info fc [] n [PClause fc n (PRef fc $ n) [] (delab i tm) []]
247− logLvl 1 $ "Elaborated provider " ++ show n ++ " as: " ++ show tm
248+ logLvl 1 $ "Elaborated provider " ++ show n ++ " as: " ++ show tm
249 where isTType :: TT Name -> Bool
250 where isTType :: TT Name -> Bool
250 isTType (TType _) = True
251 isTType (TType _) = True
251 isTType _ = False
252 isTType _ = False
253 isProviderOf :: TT Name -> TT Name -> Bool
254 isProviderOf :: TT Name -> TT Name -> Bool
255+ isProviderOf tp prov
254− isProviderOf tp prov | (P _ (UN "IO") _, [prov']) <- unApply prov
256+ | (P _ (UN "IO") _, [prov']) <- unApply prov
255− , (P _ (NS (UN "Provider") ["Providers"]) _, [tp']) <- unApply prov'
257+ , (P _ (NS (UN "Provider") ["Providers"]) _, [tp']) <- unApply prov'
256− , tp == tp' = True
258+ , tp == tp' = True
257 isProviderOf _ _ = False
259 isProviderOf _ _ = False