Idris.ElabTerm

Documentation

data ElabInfo

Constructors

EInfo

Fields

params :: [(Name, PTerm)]

inblock :: Ctxt [Name]

liftname :: Name -> Name

namespace :: Maybe [String]

toplevel :: ElabInfo

build :: IState -> ElabInfo -> Bool -> FnOpts -> Name -> PTerm -> ElabD (Term, [(Name, (Int, Maybe Name, Type))], [PDecl])

buildTC :: IState -> ElabInfo -> Bool -> FnOpts -> Name -> PTerm -> ElabD (Term, [(Name, (Int, Maybe Name, Type))], [PDecl])

elab :: IState -> ElabInfo -> Bool -> FnOpts -> Name -> PTerm -> ElabD ()

pruneAlt :: [PTerm] -> [PTerm]

pruneByType :: Term -> Context -> [PTerm] -> [PTerm]

findInstances :: IState -> Term -> [Name]

trivial' :: IState -> ElabD ()

proofSearch' :: IState -> Maybe Name -> Name -> [Name] -> ElabD ()

resolveTC :: Int -> Term -> Name -> IState -> ElabD ()

resTC' :: (Eq a, Num a) => [TT Name] -> a -> Term -> Name -> IState -> StateT (ElabState [PDecl]) TC ()

collectDeferred :: Maybe Name -> Term -> State [(Name, (Int, Maybe Name, Type))] Term

runTac :: Bool -> IState -> Name -> PTactic -> ElabD ()

reflm :: String -> Name

Prefix a name with the Language.Reflection namespace

reify :: IState -> Term -> ElabD PTactic

Reify tactics from their reflected representation

reifyApp :: IState -> Name -> [Term] -> ElabD PTactic

reifyTT :: Term -> ElabD Term

Reify terms from their reflected representation

reifyTTApp :: Name -> [Term] -> ElabD Term

reifyRaw :: Term -> ElabD Raw

Reify raw terms from their reflected representation

reifyRawApp :: Name -> [Term] -> ElabD Raw

reifyTTName :: Term -> ElabD Name

reifyTTNameApp :: Name -> [Term] -> ElabD Name

reifyTTNamespace :: Term -> ElabD [String]

reifyTTNameType :: Term -> ElabD NameType

reifyTTBinder :: (Term -> ElabD a) -> Name -> Term -> ElabD (Binder a)

reifyTTBinderApp :: (Term -> ElabD a) -> Name -> [Term] -> ElabD (Binder a)

reifyTTConst :: Term -> ElabD Const

reifyTTConstApp :: Name -> Term -> ElabD Const

reifyTTUExp :: Term -> ElabD UExp

reflCall :: String -> [Raw] -> Raw

Create a reflected call to a named function/constructor

reflect :: Term -> Raw

Lift a term into its Language.Reflection.TT representation

reflectNameType :: NameType -> Raw

reflectName :: Name -> Raw

reflectBinder :: Binder Term -> Raw

reflectConstant :: Const -> Raw

reflectUExp :: UExp -> Raw

reflectEnv :: Env -> Raw

Reflect the environment of a proof into a List (TTName, Binder TT)

rawBool :: Bool -> Raw

Reflect an error into the internal datatype of Idris -- TODO

rawNil :: Raw -> Raw

rawCons :: Raw -> Raw -> Raw -> Raw

rawList :: Raw -> [Raw] -> Raw

rawPairTy :: Raw -> Raw -> Raw

rawPair :: (Raw, Raw) -> (Raw, Raw) -> Raw

reflectCtxt :: [(Name, Type)] -> Raw

reflectErr :: Err -> Raw

elaboratingArgErr :: [(Name, Name)] -> Err -> Err

withErrorReflection :: Idris a -> Idris a

fromTTMaybe :: Term -> Maybe Term

reflErrName :: String -> Name

reifyReportPart :: Term -> Either Err ErrorReportPart

Attempt to reify a report part from TT to the internal representation. Not in Idris or ElabD monads because it should be usable from either.

envTupleType :: Raw

solveAll :: Elab' aux ()