Idris.ElabDecls

Documentation

recheckC :: FC -> Env -> TT Name -> StateT IState (ErrorT Err IO) (Term, Type)

checkDef :: FC -> [(Name, (Int, Maybe Name, TT Name))] -> StateT IState (ErrorT Err IO) [(Name, (Int, Maybe Name, Term))]

checkAddDef :: Bool -> Bool -> FC -> [(Name, (Int, Maybe Name, TT Name))] -> StateT IState (ErrorT Err IO) [(Name, (Int, Maybe Name, Term))]

elabType :: ElabInfo -> SyntaxInfo -> String -> FC -> FnOpts -> Name -> PTerm -> Idris Type

Elaborate a top-level type declaration - for example, foo : Int -> Int.

elabType' :: Bool -> ElabInfo -> SyntaxInfo -> String -> FC -> FnOpts -> Name -> PTerm -> Idris Type

elabPostulate :: ElabInfo -> SyntaxInfo -> String -> FC -> FnOpts -> Name -> PTerm -> Idris ()

elabData :: ElabInfo -> SyntaxInfo -> String -> FC -> DataOpts -> PData -> Idris ()

type EliminatorState = StateT (Map String Int) Idris

elabEliminator :: [Int] -> Name -> PTerm -> [(String, Name, PTerm, FC, [Name])] -> ElabInfo -> EliminatorState ()

elabPrims :: Idris ()

Elaborate primitives

elabProvider :: ElabInfo -> SyntaxInfo -> FC -> Name -> PTerm -> PTerm -> Idris ()

Elaborate a type provider

elabTransform :: ElabInfo -> FC -> Bool -> PTerm -> PTerm -> Idris ()

Elaborate a type provider

elabRecord :: ElabInfo -> SyntaxInfo -> String -> FC -> Name -> PTerm -> String -> Name -> PTerm -> Idris ()

elabCon :: ElabInfo -> SyntaxInfo -> Name -> Bool -> (String, Name, PTerm, FC, [Name]) -> Idris (Name, Type)

elabClauses :: ElabInfo -> FC -> FnOpts -> Name -> [PClause] -> Idris ()

Elaborate a collection of left-hand and right-hand pairs - that is, a top-level definition.

elabPE :: ElabInfo -> FC -> Name -> Term -> Idris ()

elabValBind :: ElabInfo -> Bool -> PTerm -> Idris (Term, Type, [(Name, Type)])

elabVal :: ElabInfo -> Bool -> PTerm -> Idris (Term, Type)

checkPossible :: ElabInfo -> FC -> Bool -> Name -> PTerm -> Idris Bool

elabClause :: ElabInfo -> FnOpts -> (Int, PClause) -> Idris (Either Term (Term, Term))

data MArgTy

Constructors

IA

EA

CA

Instances

Show MArgTy

elabClass :: ElabInfo -> SyntaxInfo -> String -> FC -> [PTerm] -> Name -> [(Name, PTerm)] -> [PDecl] -> Idris ()

elabInstance :: ElabInfo -> SyntaxInfo -> ElabWhat -> FC -> [PTerm] -> Name -> [PTerm] -> PTerm -> Maybe Name -> [PDecl] -> Idris ()

decorateid :: (Name -> Name) -> PDecl' PTerm -> PDecl' PTerm

pbinds :: TT Name -> StateT (ElabState aux) TC ()

pbty :: TT n -> TT n -> TT n

getPBtys :: TT t -> [(t, TT t)]

psolve :: TT t -> StateT (ElabState aux) TC ()

pvars :: IState -> TT Name -> [(Name, PTerm)]

data ElabWhat

Constructors

ETypes

EDefns

EAll

Instances

Eq ElabWhat

Show ElabWhat

elabDecls :: ElabInfo -> [PDecl] -> Idris ()

elabDecl :: ElabWhat -> ElabInfo -> PDecl -> Idris ()

elabDecl' :: ElabWhat -> ElabInfo -> PDecl' PTerm -> StateT IState (ErrorT Err IO) ()

elabCaseBlock :: ElabInfo -> [FnOpt] -> PDecl' PTerm -> StateT IState (ErrorT Err IO) ()

checkInferred :: FC -> PTerm -> PTerm -> Idris ()

inferredDiff :: FC -> PTerm -> PTerm -> Idris Bool