idris-0.11.2: Functional Programming Language with Dependent Types

Safe HaskellNone
LanguageHaskell98

Idris.Elab.Term

Synopsis

Documentation

data ElabMode Source

Constructors

ETyDecl 
ETransLHS 
ELHS 
ERHS 

Instances

data ElabResult Source

Constructors

ElabResult 

Fields

resultTerm :: Term

The term resulting from elaboration

resultMetavars :: [(Name, (Int, Maybe Name, Type, [Name]))]

Information about new metavariables

resultCaseDecls :: [PDecl]

Deferred declarations as the meaning of case blocks

resultContext :: Context

The potentially extended context from new definitions

resultTyDecls :: [RDeclInstructions]

Meta-info about the new type declarations

resultHighlighting :: [(FC, OutputAnnotation)]

Saved highlights from elaboration

resultName :: Int

The new global name counter

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

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 (%runElab)

findHighlight :: Name -> ElabD OutputAnnotation Source

Use the local elab context to work out the highlighting for a name

trivialHoles' :: [Name] -> [(Name, Int)] -> IState -> ElabD () Source

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

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

metavarName :: Maybe [String] -> Name -> Name Source

Compute the appropriate name for a top-level metavariable

processTacticDecls :: ElabInfo -> [RDeclInstructions] -> Idris () Source

Do the left-over work after creating declarations in reflected elaborator scripts