git.iko.soy/Idris-dev
on bf4e535 help sign in
Idris-dev/src/Idris/Elab/Provider.hs
122 lines 4.5 kB history raw
1{-# LANGUAGE PatternGuards #-}
2module Idris.Elab.Provider(elabProvider) where
4import Idris.AbsSyntax
5import Idris.ASTUtils
6import Idris.DSL
7import Idris.Error
8import Idris.Delaborate
9import Idris.Imports
10import Idris.ElabTerm
11import Idris.Coverage
12import Idris.DataOpts
13import Idris.Providers
14import Idris.Primitives
15import Idris.Inliner
16import Idris.PartialEval
17import Idris.DeepSeq
18import Idris.Output (iputStrLn, pshow, iWarn)
19import IRTS.Lang
21import Idris.Elab.Type
22import Idris.Elab.Clause
23import Idris.Elab.Value
24import Idris.Elab.Utils
26import Idris.Core.TT
27import Idris.Core.Elaborate hiding (Tactic(..))
28import Idris.Core.Evaluate
29import Idris.Core.Execute
30import Idris.Core.Typecheck
31import Idris.Core.CaseTree
33import Idris.Docstrings
35import Prelude hiding (id, (.))
36import Control.Category
38import Control.Applicative hiding (Const)
39import Control.DeepSeq
40import Control.Monad
41import Control.Monad.State.Strict as State
42import Data.List
43import Data.Maybe
44import Debug.Trace
46import qualified Data.Map as Map
47import qualified Data.Set as S
48import qualified Data.Text as T
49import Data.Char(isLetter, toLower)
50import Data.List.Split (splitOn)
52import Util.Pretty(pretty, text)
54-- | Elaborate a type provider
55elabProvider :: Docstring (Either Err PTerm) -> ElabInfo -> SyntaxInfo -> FC -> ProvideWhat -> Name -> Idris ()
56elabProvider doc info syn fc what n
57 = do i <- getIState
58 -- Ensure that the experimental extension is enabled
59 unless (TypeProviders `elem` idris_language_extensions i) $
60 ifail $ "Failed to define type provider \"" ++ show n ++
61 "\".\nYou must turn on the TypeProviders extension."
63 ctxt <- getContext
65 -- First elaborate the expected type (and check that it's a type)
66 -- The goal type for a postulate is always Type.
67 (ty', typ) <- case what of
68 ProvTerm ty p -> elabVal info ERHS ty
69 ProvPostulate _ -> elabVal info ERHS PType
70 unless (isTType typ) $
71 ifail ("Expected a type, got " ++ show ty' ++ " : " ++ show typ)
73 -- Elaborate the provider term to TT and check that the type matches
74 (e, et) <- case what of
75 ProvTerm _ tm -> elabVal info ERHS tm
76 ProvPostulate tm -> elabVal info ERHS tm
77 unless (isProviderOf ctxt ty' et) $
78 ifail $ "Expected provider type " ++ show (providerOf ty') ++
79 ", got " ++ show et ++ " instead."
81 -- Execute the type provider and normalise the result
82 -- use 'run__provider' to convert to a primitive IO action
84 rhs <- execute (mkApp (P Ref (sUN "run__provider") Erased)
85 [Erased, e])
86 let rhs' = normalise ctxt [] rhs
87 logLvl 3 $ "Normalised " ++ show n ++ "'s RHS to " ++ show rhs
89 -- Extract the provided term or postulate from the type provider
90 provided <- getProvided fc rhs'
92 case provided of
93 Provide tm
94 | ProvTerm ty _ <- what ->
95 do -- Finally add a top-level definition of the provided term
96 elabType info syn doc [] fc [] n ty
97 elabClauses info fc [] n [PClause fc n (PApp fc (PRef fc n) []) [] (delab i tm) []]
98 logLvl 3 $ "Elaborated provider " ++ show n ++ " as: " ++ show tm
99 | ProvPostulate _ <- what ->
100 do -- Add the postulate
101 elabPostulate info syn doc fc [] n (delab i tm)
102 logLvl 3 $ "Elaborated provided postulate " ++ show n
103 | otherwise ->
104 ierror . Msg $ "Attempted to provide a postulate where a term was expected."
106 where isTType :: TT Name -> Bool
107 isTType (TType _) = True
108 isTType _ = False
110 -- Note: IO (Providers.Provider ty) is used instead of IO'
111 -- (MkFFI C_FFI) (Providers.Provider ty) in hopes of better
112 -- error messages with less normalisation
113 providerOf :: Type -> Type
114 providerOf ty = App (P Ref (sUN "IO") Erased) $
115 App (P Ref (sNS (sUN "Provider") ["Providers", "Prelude"]) Erased)
116 ty
118 isProviderOf :: Context -> TT Name -> TT Name -> Bool
119 isProviderOf ctxt tp prov =
120 case converts ctxt [] (providerOf tp) prov of
121 OK _ -> True
122 _ -> False