{-|
Module      : Idris.ElabDecls
Description : Code to elaborate declarations.

License     : BSD3
Maintainer  : The Idris Community.
-}

{-# LANGUAGE DeriveFunctor, FlexibleInstances, MultiParamTypeClasses,
             PatternGuards #-}

module Idris.ElabDecls(elabDecl, elabDecl', elabDecls, elabMain, elabPrims,
                       recinfo) where

import Idris.AbsSyntax
import Idris.Core.Evaluate
import Idris.Core.TT
import Idris.Directives
import Idris.Docstrings hiding (Unchecked)
import Idris.Elab.Clause
import Idris.Elab.Data
import Idris.Elab.Implementation
import Idris.Elab.Interface
import Idris.Elab.Provider
import Idris.Elab.Record
import Idris.Elab.RunElab
import Idris.Elab.Term
import Idris.Elab.Transform
import Idris.Elab.Type
import Idris.Elab.Value
import Idris.Error
import Idris.Options
import Idris.Output (sendHighlighting)
import Idris.Primitives
import Idris.Termination
import IRTS.Lang

import Prelude hiding (id, (.))

import Control.Category
import Control.Monad
import Control.Monad.State.Strict as State
import Data.Maybe
import qualified Data.Set as S
import qualified Data.Text as T


-- | Top level elaborator info, supporting recursive elaboration
recinfo :: FC -> ElabInfo
recinfo :: FC -> ElabInfo
recinfo FC
fc = [(Name, PTerm)]
-> Ctxt [Name]
-> (Name -> Name)
-> [String]
-> Maybe FC
-> String
-> Int
-> [Name]
-> (PTerm -> PTerm)
-> (ElabWhat -> ElabInfo -> PDecl -> Idris ())
-> ElabInfo
EInfo [] Ctxt [Name]
forall {k} {a}. Map k a
emptyContext Name -> Name
forall a. a -> a
forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id [] (FC -> Maybe FC
forall a. a -> Maybe a
Just FC
fc) (FC -> String
fc_fname FC
fc) Int
0 [] PTerm -> PTerm
forall a. a -> a
forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id ElabWhat -> ElabInfo -> PDecl -> Idris ()
elabDecl'

-- | Return the elaborated term which calls 'main'
elabMain :: Idris Term
elabMain :: Idris Term
elabMain = do (Term
m, Term
_) <- ElabInfo -> ElabMode -> PTerm -> Idris (Term, Term)
elabVal (FC -> ElabInfo
recinfo FC
fc) ElabMode
ERHS
                           (FC -> PTerm -> [PArg] -> PTerm
PApp FC
fc (FC -> [FC] -> Name -> PTerm
PRef FC
fc [] (String -> Name
sUN String
"run__IO"))
                                [PTerm -> PArg
forall {t}. t -> PArg' t
pexp (PTerm -> PArg) -> PTerm -> PArg
forall a b. (a -> b) -> a -> b
$ FC -> [FC] -> Name -> PTerm
PRef FC
fc [] (Name -> [String] -> Name
sNS (String -> Name
sUN String
"main") [String
"Main"])])
              Term -> Idris Term
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Term
m
  where fc :: FC
fc = String -> FC
fileFC String
"toplevel"

-- | Elaborate primitives
elabPrims :: Idris ()
elabPrims :: Idris ()
elabPrims = do IState
i <- Idris IState
getIState
               let cs_in :: Set ConstraintFC
cs_in = IState -> Set ConstraintFC
idris_constraints IState
i
               let mkdec :: DataOpts
-> PData' t
-> Docstring (Either Err t)
-> [(Name, Docstring (Either Err t))]
-> PDecl' t
mkdec DataOpts
opt PData' t
decl Docstring (Either Err t)
docs [(Name, Docstring (Either Err t))]
argdocs =
                       Docstring (Either Err t)
-> [(Name, Docstring (Either Err t))]
-> SyntaxInfo
-> FC
-> DataOpts
-> PData' t
-> PDecl' t
forall t.
Docstring (Either Err t)
-> [(Name, Docstring (Either Err t))]
-> SyntaxInfo
-> FC
-> DataOpts
-> PData' t
-> PDecl' t
PData Docstring (Either Err t)
docs [(Name, Docstring (Either Err t))]
argdocs SyntaxInfo
defaultSyntax (String -> FC
fileFC String
"builtin")
                             DataOpts
opt PData' t
decl
               -- need to temporarily add linearity for this since the
               -- argument may be of restricted type
               LanguageExt -> Idris ()
addLangExt LanguageExt
LinearTypes
               ElabWhat -> ElabInfo -> PDecl -> Idris ()
elabDecl' ElabWhat
EAll (FC -> ElabInfo
recinfo FC
primfc) (DataOpts
-> PData' PTerm
-> Docstring (Either Err PTerm)
-> [(Name, Docstring (Either Err PTerm))]
-> PDecl
forall {t}.
DataOpts
-> PData' t
-> Docstring (Either Err t)
-> [(Name, Docstring (Either Err t))]
-> PDecl' t
mkdec DataOpts
forall a. [a]
inferOpts PData' PTerm
inferDecl Docstring (Either Err PTerm)
forall a. Docstring a
emptyDocstring [])
               LanguageExt -> Idris ()
dropLangExt LanguageExt
LinearTypes
               -- We don't want the constraints generated by 'Infer' since
               -- it's only scaffolding for the elaborator
               IState
i <- Idris IState
getIState
               IState -> Idris ()
putIState (IState -> Idris ()) -> IState -> Idris ()
forall a b. (a -> b) -> a -> b
$ IState
i { idris_constraints = cs_in }
               ElabWhat -> ElabInfo -> PDecl -> Idris ()
elabDecl' ElabWhat
EAll (FC -> ElabInfo
recinfo FC
primfc) (DataOpts
-> PData' PTerm
-> Docstring (Either Err PTerm)
-> [(Name, Docstring (Either Err PTerm))]
-> PDecl
forall {t}.
DataOpts
-> PData' t
-> Docstring (Either Err t)
-> [(Name, Docstring (Either Err t))]
-> PDecl' t
mkdec DataOpts
forall a. [a]
eqOpts PData' PTerm
eqDecl Docstring (Either Err PTerm)
forall {t} {b}. Docstring (Either (Err' t) b)
eqDoc [(Name, Docstring (Either Err PTerm))]
forall {t} {b}. [(Name, Docstring (Either (Err' t) b))]
eqParamDoc)

               Name -> Name -> Idris ()
addNameHint Name
eqTy (String -> Name
sUN String
"prf")
               (Prim -> Idris ()) -> [Prim] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Prim -> Idris ()
elabPrim [Prim]
primitives
               -- Special case prim__believe_me because it doesn't work on just constants
               Idris ()
elabBelieveMe
               -- Finally, syntactic equality
               Idris ()
elabSynEq
    where elabPrim :: Prim -> Idris ()
          elabPrim :: Prim -> Idris ()
elabPrim (Prim Name
n Term
ty Int
i [Const] -> Maybe Const
def (Int, PrimFn)
sc Totality
tot)
              = do (Context -> Context) -> Idris ()
updateContext (Name
-> Term -> Int -> ([Value] -> Maybe Value) -> Context -> Context
addOperator Name
n Term
ty Int
i (([Const] -> Maybe Const) -> [Value] -> Maybe Value
valuePrim [Const] -> Maybe Const
def))
                   Name -> Totality -> Idris ()
setTotality Name
n Totality
tot
                   IState
i <- Idris IState
getIState
                   IState -> Idris ()
putIState IState
i { idris_scprims = (n, sc) : idris_scprims i }

          primfc :: FC
primfc = String -> FC
fileFC String
"primitive"

          valuePrim :: ([Const] -> Maybe Const) -> [Value] -> Maybe Value
          valuePrim :: ([Const] -> Maybe Const) -> [Value] -> Maybe Value
valuePrim [Const] -> Maybe Const
prim [Value]
vals = (Const -> Value) -> Maybe Const -> Maybe Value
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Const -> Value
VConstant ((Value -> Maybe Const) -> [Value] -> Maybe [Const]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Value -> Maybe Const
getConst [Value]
vals Maybe [Const] -> ([Const] -> Maybe Const) -> Maybe Const
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= [Const] -> Maybe Const
prim)

          getConst :: Value -> Maybe Const
getConst (VConstant Const
c) = Const -> Maybe Const
forall a. a -> Maybe a
Just Const
c
          getConst Value
_             = Maybe Const
forall a. Maybe a
Nothing


          p_believeMe :: [a] -> Maybe a
p_believeMe [a
_,a
_,a
x] = a -> Maybe a
forall a. a -> Maybe a
Just a
x
          p_believeMe [a]
_ = Maybe a
forall a. Maybe a
Nothing
          believeTy :: Term
believeTy = Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind (String -> Name
sUN String
"a") (RigCount -> Maybe ImplicitInfo -> Term -> Term -> Binder Term
forall b. RigCount -> Maybe ImplicitInfo -> b -> b -> Binder b
Pi RigCount
RigW Maybe ImplicitInfo
forall a. Maybe a
Nothing (UExp -> Term
forall n. UExp -> TT n
TType (String -> Int -> UExp
UVar [] (-Int
2))) (UExp -> Term
forall n. UExp -> TT n
TType (String -> Int -> UExp
UVar [] (-Int
1))))
                       (Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind (String -> Name
sUN String
"b") (RigCount -> Maybe ImplicitInfo -> Term -> Term -> Binder Term
forall b. RigCount -> Maybe ImplicitInfo -> b -> b -> Binder b
Pi RigCount
RigW Maybe ImplicitInfo
forall a. Maybe a
Nothing (UExp -> Term
forall n. UExp -> TT n
TType (String -> Int -> UExp
UVar [] (-Int
2))) (UExp -> Term
forall n. UExp -> TT n
TType (String -> Int -> UExp
UVar [] (-Int
1))))
                         (Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind (String -> Name
sUN String
"x") (RigCount -> Maybe ImplicitInfo -> Term -> Term -> Binder Term
forall b. RigCount -> Maybe ImplicitInfo -> b -> b -> Binder b
Pi RigCount
RigW Maybe ImplicitInfo
forall a. Maybe a
Nothing (Int -> Term
forall n. Int -> TT n
V Int
1) (UExp -> Term
forall n. UExp -> TT n
TType (String -> Int -> UExp
UVar [] (-Int
1)))) (Int -> Term
forall n. Int -> TT n
V Int
1)))
          elabBelieveMe :: Idris ()
elabBelieveMe
             = do let prim__believe_me :: Name
prim__believe_me = String -> Name
sUN String
"prim__believe_me"
                  (Context -> Context) -> Idris ()
updateContext (Name
-> Term -> Int -> ([Value] -> Maybe Value) -> Context -> Context
addOperator Name
prim__believe_me Term
believeTy Int
3 [Value] -> Maybe Value
forall {a}. [a] -> Maybe a
p_believeMe)
                  -- The point is that it is believed to be total, even
                  -- though it clearly isn't :)
                  Name -> Totality -> Idris ()
setTotality Name
prim__believe_me ([Int] -> Totality
Total [])
                  IState
i <- Idris IState
getIState
                  IState -> Idris ()
putIState IState
i {
                      idris_scprims = (prim__believe_me, (3, LNoOp)) : idris_scprims i
                    }

          p_synEq :: [Value] -> Maybe Value
p_synEq [Value
t,Value
_,Value
x,Value
y]
               | Value
x Value -> Value -> Bool
forall a. Eq a => a -> a -> Bool
== Value
y = Value -> Maybe Value
forall a. a -> Maybe a
Just (Value -> Value -> Value
VApp (Value -> Value -> Value
VApp Value
vnJust Value
VErased)
                                (Value -> Value -> Value
VApp (Value -> Value -> Value
VApp Value
vnRefl Value
t) Value
x))
               | Bool
otherwise = Value -> Maybe Value
forall a. a -> Maybe a
Just (Value -> Value -> Value
VApp Value
vnNothing Value
VErased)
          p_synEq [Value]
args = Maybe Value
forall a. Maybe a
Nothing

          nMaybe :: Term
nMaybe = NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P (Int -> Int -> NameType
TCon Int
0 Int
2) (Name -> [String] -> Name
sNS (String -> Name
sUN String
"Maybe") [String
"Maybe", String
"Prelude"]) Term
forall n. TT n
Erased
          vnJust :: Value
vnJust = NameType -> Name -> Value -> Value
VP (Int -> Int -> Bool -> NameType
DCon Int
1 Int
2 Bool
False) (Name -> [String] -> Name
sNS (String -> Name
sUN String
"Just") [String
"Maybe", String
"Prelude"]) Value
VErased
          vnNothing :: Value
vnNothing = NameType -> Name -> Value -> Value
VP (Int -> Int -> Bool -> NameType
DCon Int
0 Int
1 Bool
False) (Name -> [String] -> Name
sNS (String -> Name
sUN String
"Nothing") [String
"Maybe", String
"Prelude"]) Value
VErased
          vnRefl :: Value
vnRefl = NameType -> Name -> Value -> Value
VP (Int -> Int -> Bool -> NameType
DCon Int
0 Int
2 Bool
False) Name
eqCon Value
VErased

          synEqTy :: Term
synEqTy = Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind (String -> Name
sUN String
"a") (RigCount -> Maybe ImplicitInfo -> Term -> Term -> Binder Term
forall b. RigCount -> Maybe ImplicitInfo -> b -> b -> Binder b
Pi RigCount
RigW Maybe ImplicitInfo
forall a. Maybe a
Nothing (UExp -> Term
forall n. UExp -> TT n
TType (String -> Int -> UExp
UVar [] (-Int
3))) (UExp -> Term
forall n. UExp -> TT n
TType (String -> Int -> UExp
UVar [] (-Int
2))))
                     (Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind (String -> Name
sUN String
"b") (RigCount -> Maybe ImplicitInfo -> Term -> Term -> Binder Term
forall b. RigCount -> Maybe ImplicitInfo -> b -> b -> Binder b
Pi RigCount
RigW Maybe ImplicitInfo
forall a. Maybe a
Nothing (UExp -> Term
forall n. UExp -> TT n
TType (String -> Int -> UExp
UVar [] (-Int
3))) (UExp -> Term
forall n. UExp -> TT n
TType (String -> Int -> UExp
UVar [] (-Int
2))))
                      (Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind (String -> Name
sUN String
"x") (RigCount -> Maybe ImplicitInfo -> Term -> Term -> Binder Term
forall b. RigCount -> Maybe ImplicitInfo -> b -> b -> Binder b
Pi RigCount
RigW Maybe ImplicitInfo
forall a. Maybe a
Nothing (Int -> Term
forall n. Int -> TT n
V Int
1) (UExp -> Term
forall n. UExp -> TT n
TType (String -> Int -> UExp
UVar [] (-Int
2))))
                       (Name -> Binder Term -> Term -> Term
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind (String -> Name
sUN String
"y") (RigCount -> Maybe ImplicitInfo -> Term -> Term -> Binder Term
forall b. RigCount -> Maybe ImplicitInfo -> b -> b -> Binder b
Pi RigCount
RigW Maybe ImplicitInfo
forall a. Maybe a
Nothing (Int -> Term
forall n. Int -> TT n
V Int
1) (UExp -> Term
forall n. UExp -> TT n
TType (String -> Int -> UExp
UVar [] (-Int
2))))
                         (Term -> [Term] -> Term
forall n. TT n -> [TT n] -> TT n
mkApp Term
nMaybe [Term -> [Term] -> Term
forall n. TT n -> [TT n] -> TT n
mkApp (NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P (Int -> Int -> NameType
TCon Int
0 Int
4) Name
eqTy Term
forall n. TT n
Erased)
                                               [Int -> Term
forall n. Int -> TT n
V Int
3, Int -> Term
forall n. Int -> TT n
V Int
2, Int -> Term
forall n. Int -> TT n
V Int
1, Int -> Term
forall n. Int -> TT n
V Int
0]]))))
          elabSynEq :: Idris ()
elabSynEq
             = do let synEq :: Name
synEq = String -> Name
sUN String
"prim__syntactic_eq"

                  (Context -> Context) -> Idris ()
updateContext (Name
-> Term -> Int -> ([Value] -> Maybe Value) -> Context -> Context
addOperator Name
synEq Term
synEqTy Int
4 [Value] -> Maybe Value
p_synEq)
                  Name -> Totality -> Idris ()
setTotality Name
synEq ([Int] -> Totality
Total [])
                  IState
i <- Idris IState
getIState
                  IState -> Idris ()
putIState IState
i {
                     idris_scprims = (synEq, (4, LNoOp)) : idris_scprims i
                    }


elabDecls :: ElabInfo -> [PDecl] -> Idris ()
elabDecls :: ElabInfo -> [PDecl] -> Idris ()
elabDecls ElabInfo
info [PDecl]
ds = do (PDecl -> Idris ()) -> [PDecl] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (ElabWhat -> ElabInfo -> PDecl -> Idris ()
elabDecl ElabWhat
EAll ElabInfo
info) [PDecl]
ds

elabDecl :: ElabWhat -> ElabInfo -> PDecl -> Idris ()
elabDecl :: ElabWhat -> ElabInfo -> PDecl -> Idris ()
elabDecl ElabWhat
what ElabInfo
info PDecl
d
    = let info' :: ElabInfo
info' = ElabInfo
info { rec_elabDecl = elabDecl' } in
          Idris () -> (Err -> Idris ()) -> Idris ()
forall a. Idris a -> (Err -> Idris a) -> Idris a
idrisCatch (Idris () -> Idris ()
forall a. Idris a -> Idris a
withErrorReflection (Idris () -> Idris ()) -> Idris () -> Idris ()
forall a b. (a -> b) -> a -> b
$ ElabWhat -> ElabInfo -> PDecl -> Idris ()
elabDecl' ElabWhat
what ElabInfo
info' PDecl
d) (Err -> Idris ()
setAndReport)

elabDecl' :: ElabWhat -> ElabInfo -> PDecl -> Idris ()
elabDecl' ElabWhat
_ ElabInfo
info (PFix FC
_ Fixity
_ [String]
_)
     = () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return () -- nothing to elaborate
elabDecl' ElabWhat
_ ElabInfo
info (PSyntax FC
_ Syntax
p)
     = () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return () -- nothing to elaborate
elabDecl' ElabWhat
what ElabInfo
info (PTy Docstring (Either Err PTerm)
doc [(Name, Docstring (Either Err PTerm))]
argdocs SyntaxInfo
s FC
f FnOpts
o Name
n FC
nfc PTerm
ty)
  | ElabWhat
what ElabWhat -> ElabWhat -> Bool
forall a. Eq a => a -> a -> Bool
/= ElabWhat
EDefns
    = do Int -> String -> Idris ()
logElab Int
1 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"Elaborating type decl " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ FnOpts -> String
forall a. Show a => a -> String
show FnOpts
o
         ElabInfo
-> SyntaxInfo
-> Docstring (Either Err PTerm)
-> [(Name, Docstring (Either Err PTerm))]
-> FC
-> FnOpts
-> Name
-> FC
-> PTerm
-> Idris Term
elabType ElabInfo
info SyntaxInfo
s Docstring (Either Err PTerm)
doc [(Name, Docstring (Either Err PTerm))]
argdocs FC
f FnOpts
o Name
n FC
nfc PTerm
ty
         () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
elabDecl' ElabWhat
what ElabInfo
info (PPostulate Bool
b Docstring (Either Err PTerm)
doc SyntaxInfo
s FC
f FC
nfc FnOpts
o Name
n PTerm
ty)
  | ElabWhat
what ElabWhat -> ElabWhat -> Bool
forall a. Eq a => a -> a -> Bool
/= ElabWhat
EDefns
    = do Int -> String -> Idris ()
logElab Int
1 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"Elaborating postulate " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ FnOpts -> String
forall a. Show a => a -> String
show FnOpts
o
         if Bool
b
            then ElabInfo
-> SyntaxInfo
-> Docstring (Either Err PTerm)
-> FC
-> FC
-> FnOpts
-> Name
-> PTerm
-> Idris ()
elabExtern ElabInfo
info SyntaxInfo
s Docstring (Either Err PTerm)
doc FC
f FC
nfc FnOpts
o Name
n PTerm
ty
            else ElabInfo
-> SyntaxInfo
-> Docstring (Either Err PTerm)
-> FC
-> FC
-> FnOpts
-> Name
-> PTerm
-> Idris ()
elabPostulate ElabInfo
info SyntaxInfo
s Docstring (Either Err PTerm)
doc FC
f FC
nfc FnOpts
o Name
n PTerm
ty
elabDecl' ElabWhat
what ElabInfo
info (PData Docstring (Either Err PTerm)
doc [(Name, Docstring (Either Err PTerm))]
argDocs SyntaxInfo
s FC
f DataOpts
co PData' PTerm
d)
  | ElabWhat
what ElabWhat -> ElabWhat -> Bool
forall a. Eq a => a -> a -> Bool
/= ElabWhat
ETypes
    = do Int -> String -> Idris ()
logElab Int
1 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"Elaborating " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show (PData' PTerm -> Name
forall t. PData' t -> Name
d_name PData' PTerm
d)
         ElabInfo
-> SyntaxInfo
-> Docstring (Either Err PTerm)
-> [(Name, Docstring (Either Err PTerm))]
-> FC
-> DataOpts
-> PData' PTerm
-> Idris ()
elabData ElabInfo
info SyntaxInfo
s Docstring (Either Err PTerm)
doc [(Name, Docstring (Either Err PTerm))]
argDocs FC
f DataOpts
co PData' PTerm
d
  | Bool
otherwise
    = do Int -> String -> Idris ()
logElab Int
1 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"Elaborating [type of] " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show (PData' PTerm -> Name
forall t. PData' t -> Name
d_name PData' PTerm
d)
         ElabInfo
-> SyntaxInfo
-> Docstring (Either Err PTerm)
-> [(Name, Docstring (Either Err PTerm))]
-> FC
-> DataOpts
-> PData' PTerm
-> Idris ()
elabData ElabInfo
info SyntaxInfo
s Docstring (Either Err PTerm)
doc [(Name, Docstring (Either Err PTerm))]
argDocs FC
f DataOpts
co (Name -> FC -> PTerm -> PData' PTerm
forall t. Name -> FC -> t -> PData' t
PLaterdecl (PData' PTerm -> Name
forall t. PData' t -> Name
d_name PData' PTerm
d) (PData' PTerm -> FC
forall t. PData' t -> FC
d_name_fc PData' PTerm
d) (PData' PTerm -> PTerm
forall t. PData' t -> t
d_tcon PData' PTerm
d))
elabDecl' ElabWhat
what ElabInfo
info d :: PDecl
d@(PClauses FC
f FnOpts
o Name
n [PClause' PTerm]
ps)
  | ElabWhat
what ElabWhat -> ElabWhat -> Bool
forall a. Eq a => a -> a -> Bool
/= ElabWhat
ETypes
    = do Int -> String -> Idris ()
logElab Int
1 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"Elaborating clause " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
n
         IState
i <- Idris IState
getIState -- get the type options too
         let o' :: FnOpts
o' = case Name -> Ctxt FnOpts -> [FnOpts]
forall a. Name -> Ctxt a -> [a]
lookupCtxt Name
n (IState -> Ctxt FnOpts
idris_flags IState
i) of
                    [FnOpts
fs] -> FnOpts
fs
                    [] -> []
         ElabInfo -> FC -> FnOpts -> Name -> [PClause' PTerm] -> Idris ()
elabClauses ElabInfo
info FC
f (FnOpts
o FnOpts -> FnOpts -> FnOpts
forall a. [a] -> [a] -> [a]
++ FnOpts
o') Name
n [PClause' PTerm]
ps
elabDecl' ElabWhat
what ElabInfo
info (PMutual FC
f [PDecl]
ps)
    = do IState
i <- Idris IState
forall s (m :: * -> *). MonadState s m => m s
get
         -- Find the interfaces we're defining in the block so that we can
         -- inline them appropriately before totality checking
         let ([Name]
ufnames, [[Name]]
umethss) = [(Name, [Name])] -> ([Name], [[Name]])
forall a b. [(a, b)] -> ([a], [b])
unzip ((PDecl -> Maybe (Name, [Name])) -> [PDecl] -> [(Name, [Name])]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (IState -> PDecl -> Maybe (Name, [Name])
findTCImpl IState
i) [PDecl]
ps)

         case [PDecl]
ps of
              [PDecl
p] -> ElabWhat -> ElabInfo -> PDecl -> Idris ()
elabDecl ElabWhat
what ElabInfo
info PDecl
p
              [PDecl]
_ -> do (PDecl -> Idris ()) -> [PDecl] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (ElabWhat -> ElabInfo -> PDecl -> Idris ()
elabDecl ElabWhat
ETypes ElabInfo
info) [PDecl]
ps
                      (PDecl -> Idris ()) -> [PDecl] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (ElabWhat -> ElabInfo -> PDecl -> Idris ()
elabDecl ElabWhat
EDefns ElabInfo
info) [PDecl]
ps
         -- record mutually defined data definitions
         let datans :: [Name]
datans = (PDecl -> [Name]) -> [PDecl] -> [Name]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap PDecl -> [Name]
declared ([PDecl] -> [PDecl]
forall {t}. [PDecl' t] -> [PDecl' t]
getDataDecls [PDecl]
ps)
         (Name -> Idris ()) -> [Name] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ([Name] -> Name -> Idris ()
setMutData [Name]
datans) [Name]
datans
         Int -> String -> Idris ()
logElab Int
1 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"Rechecking for positivity " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Name] -> String
forall a. Show a => a -> String
show [Name]
datans
         (Name -> Idris ()) -> [Name] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\Name
x -> do Name -> Totality -> Idris ()
setTotality Name
x Totality
Unchecked) [Name]
datans
         -- Do totality checking after entire mutual block
         IState
i <- Idris IState
forall s (m :: * -> *). MonadState s m => m s
get
         (Name -> Idris ()) -> [Name] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\Name
n -> do Int -> String -> Idris ()
logElab Int
5 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"Simplifying " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
n
                         Context
ctxt' <- do Context
ctxt <- StateT IState (ExceptT Err IO) Context
getContext
                                     TC Context -> StateT IState (ExceptT Err IO) Context
forall a. TC a -> Idris a
tclift (TC Context -> StateT IState (ExceptT Err IO) Context)
-> TC Context -> StateT IState (ExceptT Err IO) Context
forall a b. (a -> b) -> a -> b
$ Name -> [Name] -> [[Name]] -> ErasureInfo -> Context -> TC Context
simplifyCasedef Name
n [Name]
ufnames [[Name]]
umethss (IState -> ErasureInfo
getErasureInfo IState
i) Context
ctxt
                         Context -> Idris ()
setContext Context
ctxt')
                 (((FC, Name) -> Name) -> [(FC, Name)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (FC, Name) -> Name
forall a b. (a, b) -> b
snd (IState -> [(FC, Name)]
idris_totcheck IState
i))

         ((FC, Name) -> Idris ()) -> [(FC, Name)] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (FC, Name) -> Idris ()
buildSCG (IState -> [(FC, Name)]
idris_totcheck IState
i)
         ((FC, Name) -> StateT IState (ExceptT Err IO) Totality)
-> [(FC, Name)] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (FC, Name) -> StateT IState (ExceptT Err IO) Totality
checkDeclTotality (IState -> [(FC, Name)]
idris_totcheck IState
i)
         -- We've only checked that things are total independently. Given
         -- the ordering, something we think is total might have called
         -- something we hadn't checked yet
         ((FC, Name) -> Idris ()) -> [(FC, Name)] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (FC, Name) -> Idris ()
verifyTotality (IState -> [(FC, Name)]
idris_totcheck IState
i)
         Idris ()
clear_totcheck
  where isDataDecl :: PDecl' t -> Bool
isDataDecl (PData Docstring (Either Err t)
_ [(Name, Docstring (Either Err t))]
_ SyntaxInfo
_ FC
_ DataOpts
_ PData' t
_) = Bool
True
        isDataDecl PDecl' t
_ = Bool
False

        findTCImpl :: IState -> PDecl -> Maybe (Name, [Name])
        findTCImpl :: IState -> PDecl -> Maybe (Name, [Name])
findTCImpl IState
ist (PImplementation Docstring (Either Err PTerm)
_ [(Name, Docstring (Either Err PTerm))]
_ SyntaxInfo
_ FC
_ [(Name, PTerm)]
_ [Name]
_ Accessibility
_ FnOpts
_ Name
n_in FC
_ [PTerm]
ps [(Name, PTerm)]
_ PTerm
_ Maybe Name
expn [PDecl]
_)
             = let (Name
n, [Name]
meths)
                        = case Name -> Ctxt InterfaceInfo -> [(Name, InterfaceInfo)]
forall a. Name -> Ctxt a -> [(Name, a)]
lookupCtxtName Name
n_in (IState -> Ctxt InterfaceInfo
idris_interfaces IState
ist) of
                               [(Name
n', InterfaceInfo
ci)] -> (Name
n', ((Name, (Bool, FnOpts, PTerm)) -> Name)
-> [(Name, (Bool, FnOpts, PTerm))] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, (Bool, FnOpts, PTerm)) -> Name
forall a b. (a, b) -> a
fst (InterfaceInfo -> [(Name, (Bool, FnOpts, PTerm))]
interface_methods InterfaceInfo
ci))
                               [(Name, InterfaceInfo)]
_ -> (Name
n_in, [])
                   iname :: Name
iname = Name -> [String] -> [PTerm] -> Maybe Name -> Name
forall {a}. Show a => Name -> [String] -> [a] -> Maybe Name -> Name
mkiname Name
n (ElabInfo -> [String]
namespace ElabInfo
info) [PTerm]
ps Maybe Name
expn in
                   (Name, [Name]) -> Maybe (Name, [Name])
forall a. a -> Maybe a
Just (Name
iname, [Name]
meths)
        findTCImpl IState
ist PDecl
_ = Maybe (Name, [Name])
forall a. Maybe a
Nothing

        mkiname :: Name -> [String] -> [a] -> Maybe Name -> Name
mkiname Name
n' [String]
ns [a]
ps' Maybe Name
expn' =
           case Maybe Name
expn' of
                Maybe Name
Nothing -> case [String]
ns of
                              [] -> SpecialName -> Name
SN (Name -> [String] -> SpecialName
sImplementationN Name
n' ((a -> String) -> [a] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map a -> String
forall a. Show a => a -> String
show [a]
ps'))
                              [String]
m -> Name -> [String] -> Name
sNS (SpecialName -> Name
SN (Name -> [String] -> SpecialName
sImplementationN Name
n' ((a -> String) -> [a] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map a -> String
forall a. Show a => a -> String
show [a]
ps'))) [String]
m
                Just Name
nm -> Name
nm

        getDataDecls :: [PDecl' t] -> [PDecl' t]
getDataDecls (PNamespace String
_ FC
_ [PDecl' t]
ds : [PDecl' t]
decls)
           = [PDecl' t] -> [PDecl' t]
getDataDecls [PDecl' t]
ds [PDecl' t] -> [PDecl' t] -> [PDecl' t]
forall a. [a] -> [a] -> [a]
++ [PDecl' t] -> [PDecl' t]
getDataDecls [PDecl' t]
decls
        getDataDecls (PDecl' t
d : [PDecl' t]
decls)
           | PDecl' t -> Bool
forall {t}. PDecl' t -> Bool
isDataDecl PDecl' t
d = PDecl' t
d PDecl' t -> [PDecl' t] -> [PDecl' t]
forall a. a -> [a] -> [a]
: [PDecl' t] -> [PDecl' t]
getDataDecls [PDecl' t]
decls
           | Bool
otherwise = [PDecl' t] -> [PDecl' t]
getDataDecls [PDecl' t]
decls
        getDataDecls [] = []

        setMutData :: [Name] -> Name -> Idris ()
setMutData [Name]
ns Name
n
           = do IState
i <- Idris IState
getIState
                case Name -> Ctxt TypeInfo -> [TypeInfo]
forall a. Name -> Ctxt a -> [a]
lookupCtxt Name
n (IState -> Ctxt TypeInfo
idris_datatypes IState
i) of
                   [TypeInfo
x] -> do let x' :: TypeInfo
x' = TypeInfo
x { mutual_types = ns }
                             IState -> Idris ()
putIState (IState -> Idris ()) -> IState -> Idris ()
forall a b. (a -> b) -> a -> b
$ IState
i { idris_datatypes
                                                = addDef n x' (idris_datatypes i) }
                   [TypeInfo]
_ -> () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

elabDecl' ElabWhat
what ElabInfo
info (PParams FC
f [(Name, PTerm)]
ns [PDecl]
ps)
    = do IState
i <- Idris IState
getIState
         Int -> String -> Idris ()
logElab Int
1 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"Expanding params block with " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [(Name, PTerm)] -> String
forall a. Show a => a -> String
show [(Name, PTerm)]
ns String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" decls " String -> String -> String
forall a. [a] -> [a] -> [a]
++
                [Name] -> String
forall a. Show a => a -> String
show ((PDecl -> [Name]) -> [PDecl] -> [Name]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap PDecl -> [Name]
tldeclared [PDecl]
ps)
         let nblock :: [PDecl]
nblock = IState -> [PDecl]
pblock IState
i
         (PDecl -> Idris ()) -> [PDecl] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (ElabWhat -> ElabInfo -> PDecl -> Idris ()
elabDecl' ElabWhat
what ElabInfo
info) [PDecl]
nblock
  where
    pblock :: IState -> [PDecl]
pblock IState
i = (PDecl -> PDecl) -> [PDecl] -> [PDecl]
forall a b. (a -> b) -> [a] -> [b]
map (Bool
-> IState
-> (Name -> Name)
-> [(Name, PTerm)]
-> [Name]
-> PDecl
-> PDecl
expandParamsD Bool
False IState
i Name -> Name
forall a. a -> a
forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id [(Name, PTerm)]
ns
                      ((PDecl -> [Name]) -> [PDecl] -> [Name]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap PDecl -> [Name]
tldeclared [PDecl]
ps)) [PDecl]
ps

elabDecl' ElabWhat
what ElabInfo
info (POpenInterfaces FC
f [Name]
ns [PDecl]
ds)
    = do [Name]
open <- [Name] -> Idris [Name]
addOpenImpl [Name]
ns
         (PDecl -> Idris ()) -> [PDecl] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (ElabWhat -> ElabInfo -> PDecl -> Idris ()
elabDecl' ElabWhat
what ElabInfo
info) [PDecl]
ds
         [Name] -> Idris ()
setOpenImpl [Name]
open

elabDecl' ElabWhat
what ElabInfo
info (PNamespace String
n FC
nfc [PDecl]
ps) =
  do (PDecl -> Idris ()) -> [PDecl] -> Idris ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (ElabWhat -> ElabInfo -> PDecl -> Idris ()
elabDecl' ElabWhat
what ElabInfo
ninfo) [PDecl]
ps
     let ns :: [Text]
ns = [Text] -> [Text]
forall a. [a] -> [a]
reverse ((String -> Text) -> [String] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map String -> Text
T.pack [String]
newNS)
     Set (FC', OutputAnnotation) -> Idris ()
sendHighlighting (Set (FC', OutputAnnotation) -> Idris ())
-> Set (FC', OutputAnnotation) -> Idris ()
forall a b. (a -> b) -> a -> b
$ [(FC', OutputAnnotation)] -> Set (FC', OutputAnnotation)
forall a. Ord a => [a] -> Set a
S.fromList [(FC -> FC'
FC' FC
nfc, [Text] -> Maybe String -> OutputAnnotation
AnnNamespace [Text]
ns Maybe String
forall a. Maybe a
Nothing)]
  where
    newNS :: [String]
newNS = String
n String -> [String] -> [String]
forall a. a -> [a] -> [a]
: ElabInfo -> [String]
namespace ElabInfo
info
    ninfo :: ElabInfo
ninfo = ElabInfo
info { namespace = newNS }

elabDecl' ElabWhat
what ElabInfo
info (PInterface Docstring (Either Err PTerm)
doc SyntaxInfo
s FC
f [(Name, PTerm)]
cs Name
n FC
nfc [(Name, FC, PTerm)]
ps [(Name, Docstring (Either Err PTerm))]
pdocs [(Name, FC)]
fds [PDecl]
ds Maybe (Name, FC)
cn Docstring (Either Err PTerm)
cd)
    = do Int -> String -> Idris ()
logElab Int
1 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"Elaborating interface " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
n
         ElabInfo
-> SyntaxInfo
-> Docstring (Either Err PTerm)
-> ElabWhat
-> FC
-> [(Name, PTerm)]
-> Name
-> FC
-> [(Name, FC, PTerm)]
-> [(Name, Docstring (Either Err PTerm))]
-> [(Name, FC)]
-> [PDecl]
-> Maybe (Name, FC)
-> Docstring (Either Err PTerm)
-> Idris ()
elabInterface ElabInfo
info (SyntaxInfo
s { syn_params = [] }) Docstring (Either Err PTerm)
doc ElabWhat
what FC
f [(Name, PTerm)]
cs Name
n FC
nfc [(Name, FC, PTerm)]
ps [(Name, Docstring (Either Err PTerm))]
pdocs [(Name, FC)]
fds [PDecl]
ds Maybe (Name, FC)
cn Docstring (Either Err PTerm)
cd
elabDecl' ElabWhat
what ElabInfo
info (PImplementation Docstring (Either Err PTerm)
doc [(Name, Docstring (Either Err PTerm))]
argDocs SyntaxInfo
s FC
f [(Name, PTerm)]
cs [Name]
pnames Accessibility
acc FnOpts
fnopts Name
n FC
nfc [PTerm]
ps [(Name, PTerm)]
pextra PTerm
t Maybe Name
expn [PDecl]
ds)
    = do Int -> String -> Idris ()
logElab Int
1 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"Elaborating implementation " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
n
         ElabInfo
-> SyntaxInfo
-> Docstring (Either Err PTerm)
-> [(Name, Docstring (Either Err PTerm))]
-> ElabWhat
-> FC
-> [(Name, PTerm)]
-> [Name]
-> Accessibility
-> FnOpts
-> Name
-> FC
-> [PTerm]
-> [(Name, PTerm)]
-> PTerm
-> Maybe Name
-> [PDecl]
-> Idris ()
elabImplementation ElabInfo
info SyntaxInfo
s Docstring (Either Err PTerm)
doc [(Name, Docstring (Either Err PTerm))]
argDocs ElabWhat
what FC
f [(Name, PTerm)]
cs [Name]
pnames Accessibility
acc FnOpts
fnopts Name
n FC
nfc [PTerm]
ps [(Name, PTerm)]
pextra PTerm
t Maybe Name
expn [PDecl]
ds
elabDecl' ElabWhat
what ElabInfo
info (PRecord Docstring (Either Err PTerm)
doc SyntaxInfo
rsyn FC
fc DataOpts
opts Name
name FC
nfc [(Name, FC, Plicity, PTerm)]
ps [(Name, Docstring (Either Err PTerm))]
pdocs [(Maybe (Name, FC), Plicity, PTerm,
  Maybe (Docstring (Either Err PTerm)))]
fs Maybe (Name, FC)
cname Docstring (Either Err PTerm)
cdoc SyntaxInfo
csyn)
    = do Int -> String -> Idris ()
logElab Int
1 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"Elaborating record " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
name
         ElabInfo
-> ElabWhat
-> Docstring (Either Err PTerm)
-> SyntaxInfo
-> FC
-> DataOpts
-> Name
-> FC
-> [(Name, FC, Plicity, PTerm)]
-> [(Name, Docstring (Either Err PTerm))]
-> [(Maybe (Name, FC), Plicity, PTerm,
     Maybe (Docstring (Either Err PTerm)))]
-> Maybe (Name, FC)
-> Docstring (Either Err PTerm)
-> SyntaxInfo
-> Idris ()
elabRecord ElabInfo
info ElabWhat
what Docstring (Either Err PTerm)
doc SyntaxInfo
rsyn FC
fc DataOpts
opts Name
name FC
nfc [(Name, FC, Plicity, PTerm)]
ps [(Name, Docstring (Either Err PTerm))]
pdocs [(Maybe (Name, FC), Plicity, PTerm,
  Maybe (Docstring (Either Err PTerm)))]
fs Maybe (Name, FC)
cname Docstring (Either Err PTerm)
cdoc SyntaxInfo
csyn
{-
  | otherwise
    = do logElab 1 $ "Elaborating [type of] " ++ show tyn
         elabData info s doc [] f [] (PLaterdecl tyn ty)
-}
elabDecl' ElabWhat
_ ElabInfo
info (PDSL Name
n DSL' PTerm
dsl)
    = do IState
i <- Idris IState
getIState
         Bool -> Idris () -> Idris ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (LanguageExt
DSLNotation LanguageExt -> [LanguageExt] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` IState -> [LanguageExt]
idris_language_extensions IState
i) (Idris () -> Idris ()) -> Idris () -> Idris ()
forall a b. (a -> b) -> a -> b
$
           String -> Idris ()
forall a. String -> Idris a
ifail String
"You must turn on the DSLNotation extension to use a dsl block"
         IState -> Idris ()
putIState (IState
i { idris_dsls = addDef n dsl (idris_dsls i) })
         IBCWrite -> Idris ()
addIBC (Name -> IBCWrite
IBCDSL Name
n)
elabDecl' ElabWhat
what ElabInfo
info (PDirective i :: Directive
i@(DLogging Integer
_))
  = Directive -> Idris ()
directiveAction Directive
i
elabDecl' ElabWhat
what ElabInfo
info (PDirective Directive
i)
  | ElabWhat
what ElabWhat -> ElabWhat -> Bool
forall a. Eq a => a -> a -> Bool
/= ElabWhat
EDefns = Directive -> Idris ()
directiveAction Directive
i
elabDecl' ElabWhat
what ElabInfo
info (PProvider Docstring (Either Err PTerm)
doc SyntaxInfo
syn FC
fc FC
nfc ProvideWhat' PTerm
provWhat Name
n)
  | ElabWhat
what ElabWhat -> ElabWhat -> Bool
forall a. Eq a => a -> a -> Bool
/= ElabWhat
EDefns
    = do Int -> String -> Idris ()
logElab Int
1 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"Elaborating type provider " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
n
         Docstring (Either Err PTerm)
-> ElabInfo
-> SyntaxInfo
-> FC
-> FC
-> ProvideWhat' PTerm
-> Name
-> Idris ()
elabProvider Docstring (Either Err PTerm)
doc ElabInfo
info SyntaxInfo
syn FC
fc FC
nfc ProvideWhat' PTerm
provWhat Name
n
elabDecl' ElabWhat
what ElabInfo
info (PTransform FC
fc Bool
safety PTerm
old PTerm
new)
    = do ElabInfo -> FC -> Bool -> PTerm -> PTerm -> Idris (Term, Term)
elabTransform ElabInfo
info FC
fc Bool
safety PTerm
old PTerm
new
         () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
elabDecl' ElabWhat
what ElabInfo
info (PRunElabDecl FC
fc PTerm
script [String]
ns)
    = do IState
i <- Idris IState
getIState
         Bool -> Idris () -> Idris ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (LanguageExt
ElabReflection LanguageExt -> [LanguageExt] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` IState -> [LanguageExt]
idris_language_extensions IState
i) (Idris () -> Idris ()) -> Idris () -> Idris ()
forall a b. (a -> b) -> a -> b
$
           Err -> Idris ()
forall a. Err -> Idris a
ierror (Err -> Idris ()) -> Err -> Idris ()
forall a b. (a -> b) -> a -> b
$ FC -> Err -> Err
forall t. FC -> Err' t -> Err' t
At FC
fc (String -> Err
forall t. String -> Err' t
Msg String
"You must turn on the ElabReflection extension to use %runElab")
         ElabInfo -> FC -> PTerm -> [String] -> Idris ()
elabRunElab ElabInfo
info FC
fc PTerm
script [String]
ns
         () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
elabDecl' ElabWhat
_ ElabInfo
_ PDecl
_ = () -> Idris ()
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return () -- skipped this time