Safe Haskell	None
Language	Haskell98

Idris.ElabTerm

Synopsis

Documentation

data ElabMode Source

Constructors

ETyDecl
ELHS
ERHS

Instances

Eq ElabMode

data ElabResult Source

Constructors

ElabResult
Fields resultTerm :: Term The term resulting from elaboration resultMetavars :: [(Name, (Int, Maybe Name, Type))] Information about new metavariables resultCaseDecls :: [PDecl] Deferred declarations as the meaning of case blocks resultContext :: Context The potentially extended context from new definitions resultTyDecls :: [(Name, FC, [PArg], Type)] Meta-info about the new type declarations

processTacticDecls :: [(Name, FC, [PArg], Type)] -> Idris () Source

build :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name -> PTerm -> ElabD ElabResult Source

buildTC :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name -> PTerm -> ElabD ElabResult Source

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

data ElabCtxt Source

Constructors

ElabCtxt
Fields e_inarg :: Bool e_isfn :: Bool Function part of application e_guarded :: Bool e_intype :: Bool e_qq :: Bool e_nomatching :: Bool can't pattern match

initElabCtxt :: ElabCtxt Source

goal_polymorphic :: ElabD Bool Source

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

Returns the set of declarations we need to add to complete the definition (most likely case blocks to elaborate) as well as declarations resulting from user tactic scripts (%runTactics)

pruneAlt :: [PTerm] -> [PTerm] Source

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

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

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

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

trivial' :: IState -> ElabD () Source

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

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

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

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

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

tacN :: String -> Name Source

runTactical :: FC -> Env -> Term -> ElabD () Source

runTac :: Bool -> IState -> Maybe FC -> Name -> PTactic -> ElabD () Source

reflm :: String -> Name Source

Prefix a name with the Language.Reflection namespace

reify :: IState -> Term -> ElabD PTactic Source

Reify tactics from their reflected representation

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

reifyReportParts :: Term -> ElabD [ErrorReportPart] Source

reifyTT :: Term -> ElabD Term Source

Reify terms from their reflected representation

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

reifyRaw :: Term -> ElabD Raw Source

Reify raw terms from their reflected representation

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

reifyTTName :: Term -> ElabD Name Source

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

reifyTTNamespace :: Term -> ElabD [String] Source

reifyTTNameType :: Term -> ElabD NameType Source

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

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

reifyTTConst :: Term -> ElabD Const Source

reifyTTConstApp :: Name -> Term -> ElabD Const Source

reifyArithTy :: Term -> ElabD ArithTy Source

reifyNativeTy :: Term -> ElabD NativeTy Source

reifyIntTy :: Term -> ElabD IntTy Source

reifyTTUExp :: Term -> ElabD UExp Source

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

Create a reflected call to a named function/constructor

reflect :: Term -> Raw Source

Lift a term into its Language.Reflection.TT representation

reflectRaw :: Raw -> Raw Source

Lift a term into its Language.Reflection.Raw representation

claimTT :: Name -> ElabD Name Source

reflectTTQuotePattern :: [Name] -> Term -> ElabD () Source

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.

reflectRawQuotePattern :: [Name] -> Raw -> ElabD () Source

reflectBinderQuotePattern :: ([Name] -> a -> ElabD ()) -> [Name] -> Binder a -> ElabD () Source

reflectUniverse :: Universe -> Raw Source

reflectTTQuote :: [Name] -> Term -> Raw Source

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

reflectRawQuote :: [Name] -> Raw -> Raw Source

reflectNameType :: NameType -> Raw Source

reflectName :: Name -> Raw Source

reflectNameQuotePattern :: Name -> ElabD () Source

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 Source

reflectBinderQuote :: ([Name] -> a -> Raw) -> Name -> [Name] -> Binder a -> Raw Source

mkList :: Raw -> [Raw] -> Raw Source

reflectConstant :: Const -> Raw Source

reflectUExp :: UExp -> Raw Source

reflectEnv :: Env -> Raw Source

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

rawBool :: Bool -> Raw Source

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

rawNil :: Raw -> Raw Source

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

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