@@ -214,26 +214,50 @@ elabData info syn doc fc codata (PDatadecl n t_in dcons)
214214elabProvider :: ElabInfo -> SyntaxInfo -> FC -> Name -> PTerm -> PTerm -> Idris ()
215215elabProvider info syn fc n ty tm
216216 = do i <- getIState
217− if not (TypeProviders `elem` idris_language_extensions i)
218− then fail $ "Failed to define type provider \"" ++ show n ++
219− "\".\nYou must turn on TypeProviders extension."
220− else do let expected = providerTy fc ty
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
227− let str = show e' in
228− logLvl 1 $ "Term is " ++ if length str > 200 then (take 200 str) ++ "..." else str
229− let et' = normaliseAll ctxt [] et
230− elabType info syn "" fc [] n ty
231− rhs <- execute e'
232− logLvl 1 $ "Normalized " ++ show n ++ "'s RHS to " ++ show rhs
233− providerError rhs
234− elabClauses info fc [] n [PClause fc n (PRef fc $ n) [] (delab i rhs) []]
235− logLvl 1 $ "** Elaborated: " ++ show e' ++ " :as: " ++ show et
236− logLvl 1 $ "** Evaluated: " ++ show rhs ++ " :as: " ++ show et'
217+ -- Ensure that the experimental extension is enabled
218+ unless (TypeProviders `elem` idris_language_extensions i) $
219+ fail $ "Failed to define type provider \"" ++ show n ++
220+ "\".\nYou must turn on the TypeProviders extension."
221+
222+ ctxt <- getContext
223+
224+ -- First elaborate the expected type (and check that it's a type)
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
236+ elabType info syn "" fc [] n ty
237+
238+ -- Execute the type provider and normalise the result
239+ rhs <- execute e
240+ let rhs' = normalise ctxt [] rhs
241+ logLvl 1 $ "Normalised " ++ show n ++ "'s RHS to " ++ show 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
247+ elabClauses info fc [] n [PClause fc n (PRef fc n) [] (delab i tm) []]
248+ logLvl 1 $ "Elaborated provider " ++ show n ++ " as: " ++ show tm
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+
237261
238262elabRecord :: ElabInfo -> SyntaxInfo -> String -> FC -> Name ->
239263 PTerm -> String -> Name -> PTerm -> Idris ()