Idris.ElabTerm

Documentation

data ElabMode

Constructors

ETyDecl

ELHS

ERHS

Instances

Eq ElabMode

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

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

getUnmatchable :: Context -> Name -> [Bool]

data ElabCtxt

Constructors

ElabCtxt

Fields

e_inarg :: Bool

e_guarded :: Bool

e_intype :: Bool

e_qq :: Bool

e_nomatching :: Bool

can't pattern match

initElabCtxt :: ElabCtxt

goal_polymorphic :: ElabD Bool

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

pruneAlt :: [PTerm] -> [PTerm]

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

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

solveAuto :: IState -> Name -> Bool -> Name -> ElabD ()

solveAutos :: IState -> Name -> Bool -> ElabD ()

trivial' :: IState -> ElabD ()

proofSearch' :: IState -> Bool -> Bool -> Int -> Bool -> Maybe Name -> Name -> [Name] -> StateT (ElabState EState) TC ()

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

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

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

case_ :: Bool -> Bool -> IState -> Name -> PTerm -> ElabD ()

runTac :: Bool -> IState -> Maybe FC -> 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

reifyArithTy :: Term -> ElabD ArithTy

reifyNativeTy :: Term -> ElabD NativeTy

reifyIntTy :: Term -> ElabD IntTy

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

claimTT :: Name -> ElabD Name

reflectQuotePattern :: [Name] -> Term -> ElabD ()

Convert a reflected term to a more suitable form for pattern-matching. In particular, the less-interesting bits are elaborated to _ patterns. This happens to NameTypes, universe levels, names that are bound but not used, and the type annotation field of the P constructor.

reflectQuote :: [Name] -> Term -> Raw

Create a reflected term, but leave refs to the provided name intact

reflectNameType :: NameType -> Raw

reflectName :: Name -> Raw

reflectNameQuotePattern :: Name -> ElabD ()

Elaborate a name to a pattern. This means that NS and UN will be intact. MNs corresponding to will care about the string but not the number. All others become _.

reflectBinder :: Binder Term -> Raw

reflectBinderQuote :: [Name] -> Binder Term -> Raw

mkList :: Raw -> [Raw] -> 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 ()