@@ -214,26 +214,48 @@ 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+ -- Ensure that the experimental extension is enabled
217218 if not (TypeProviders `elem` idris_language_extensions i)
218219 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
220+ "\".\nYou must turn on the TypeProviders extension."
221+ else do ctxt <- getContext
222+
223+ -- First elaborate the expected type (and check that it's a type)
224+ (ty', typ) <- elabVal toplevel False ty
225+ unless (isTType typ) $
226+ (fail $ "Expected a type, got " ++ show ty' ++ " : " ++ show typ)
227+
228+ -- Elaborate the provider term to TT and check that the type matches
229+ (e, et) <- elabVal toplevel False tm
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
230235 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'
236+
237+ -- Execute the type provider and normalise the result
238+ rhs <- execute e
239+ let rhs' = normalise ctxt [] rhs
240+ logLvl 1 $ "Normalised " ++ show n ++ "'s RHS to " ++ show 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
246+ elabClauses info fc [] n [PClause fc n (PRef fc $ n) [] (delab i tm) []]
247+ logLvl 1 $ "Elaborated provider " ++ show n ++ " as: " ++ show tm
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+
237259
238260elabRecord :: ElabInfo -> SyntaxInfo -> String -> FC -> Name ->
239261 PTerm -> String -> Name -> PTerm -> Idris ()