Idris.AbsSyntax

Contents

• if it's just a type variable or concrete type, do it early (0)
• if there's only type variables and injective constructors, do it next (1)
• if there's a function type, next (2)
• finally, everything else (3)

Synopsis

• getContext :: Idris Context
• forCodegen :: Codegen -> [(Codegen, a)] -> [a]
• getObjectFiles :: Codegen -> Idris [FilePath]
• addObjectFile :: Codegen -> FilePath -> Idris ()
• getLibs :: Codegen -> Idris [String]
• addLib :: Codegen -> String -> Idris ()
• getFlags :: Codegen -> Idris [String]
• addFlag :: Codegen -> String -> Idris ()
• addDyLib :: [String] -> Idris (Either DynamicLib String)
• addHdr :: Codegen -> String -> Idris ()
• addLangExt :: LanguageExt -> Idris ()
• addTrans :: (Term, Term) -> Idris ()
• totcheck :: (FC, Name) -> Idris ()
• defer_totcheck :: (FC, Name) -> Idris ()
• clear_totcheck :: Idris ()
• setFlags :: Name -> [FnOpt] -> Idris ()
• setAccessibility :: Name -> Accessibility -> Idris ()
• setTotality :: Name -> Totality -> Idris ()
• getTotality :: Name -> Idris Totality
• getCoercionsTo :: IState -> Type -> [Name]
• addToCG :: Name -> CGInfo -> Idris ()
• getAllNames :: Name -> Idris [Name]
• allNames :: [Name] -> Name -> Idris [Name]
• addCoercion :: Name -> Idris ()
• addDocStr :: Name -> String -> Idris ()
• addToCalledG :: Name -> [Name] -> Idris ()
• addInstance :: Bool -> Name -> Name -> Idris ()
• addClass :: Name -> ClassInfo -> Idris ()
• addIBC :: IBCWrite -> Idris ()
• clearIBC :: Idris ()
• getHdrs :: Codegen -> Idris [String]
• setErrLine :: Int -> Idris ()
• clearErr :: Idris ()
• getSO :: Idris (Maybe String)
• setSO :: Maybe String -> Idris ()
• getIState :: Idris IState
• putIState :: IState -> Idris ()
• runIO :: IO a -> Idris a
• getName :: Idris Int
• addInternalApp :: FilePath -> Int -> PTerm -> Idris ()
• getInternalApp :: FilePath -> Int -> Idris PTerm
• checkUndefined :: FC -> Name -> Idris ()
• isUndefined :: FC -> Name -> Idris Bool
• setContext :: Context -> Idris ()
• updateContext :: (Context -> Context) -> Idris ()
• addConstraints :: FC -> (Int, [UConstraint]) -> Idris ()
• addDeferred :: [(Name, (Int, Maybe Name, Type, Bool))] -> Idris ()
• addDeferredTyCon :: [(Name, (Int, Maybe Name, Type, Bool))] -> Idris ()
• addDeferred' :: NameType -> [(Name, (Int, Maybe Name, Type, Bool))] -> Idris ()
• solveDeferred :: Name -> Idris ()
• ihPrintResult :: Handle -> String -> Idris ()
• ihPrintError :: Handle -> String -> Idris ()
• ihputStrLn :: Handle -> String -> Idris ()
• iputStrLn :: String -> Idris ()
• iPrintError :: String -> Idris ()
• iPrintResult :: String -> Idris ()
• iWarn :: FC -> String -> Idris ()
• ideslavePutSExp :: SExpable a => String -> a -> Idris ()
• iputGoal :: String -> Idris ()
• isetPrompt :: String -> Idris ()
• ihWarn :: Handle -> FC -> String -> Idris ()
• setLogLevel :: Int -> Idris ()
• setCmdLine :: [Opt] -> Idris ()
• getCmdLine :: Idris [Opt]
• getDumpDefun :: Idris (Maybe FilePath)
• getDumpCases :: Idris (Maybe FilePath)
• logLevel :: Idris Int
• setErrContext :: Bool -> Idris ()
• errContext :: Idris Bool
• useREPL :: Idris Bool
• setREPL :: Bool -> Idris ()
• setNoBanner :: Bool -> Idris ()
• getNoBanner :: Idris Bool
• setQuiet :: Bool -> Idris ()
• getQuiet :: Idris Bool
• setCodegen :: Codegen -> Idris ()
• codegen :: Idris Codegen
• setOutputTy :: OutputType -> Idris ()
• outputTy :: Idris OutputType
• setIdeSlave :: Bool -> Idris ()
• setTargetTriple :: String -> Idris ()
• targetTriple :: Idris String
• setTargetCPU :: String -> Idris ()
• targetCPU :: Idris String
• setOptLevel :: Word -> Idris ()
• optLevel :: Idris Word
• verbose :: Idris Bool
• setVerbose :: Bool -> Idris ()
• typeInType :: Idris Bool
• setTypeInType :: Bool -> Idris ()
• coverage :: Idris Bool
• setCoverage :: Bool -> Idris ()
• setIBCSubDir :: FilePath -> Idris ()
• valIBCSubDir :: IState -> Idris FilePath
• addImportDir :: FilePath -> Idris ()
• setImportDirs :: [FilePath] -> Idris ()
• allImportDirs :: Idris [FilePath]
• colourise :: Idris Bool
• setColourise :: Bool -> Idris ()
• setOutH :: Handle -> Idris ()
• impShow :: Idris Bool
• setImpShow :: Bool -> Idris ()
• setColour :: ColourType -> IdrisColour -> Idris ()
• logLvl :: Int -> String -> Idris ()
• cmdOptType :: Opt -> Idris Bool
• iLOG :: String -> Idris ()
• noErrors :: Idris Bool
• setTypeCase :: Bool -> Idris ()
• bi :: FC
• inferTy :: Name
• inferCon :: Name
• inferDecl :: PData' PTerm
• infTerm :: PTerm -> PTerm
• infP :: TT Name
• getInferTerm :: Term -> Term
• getInferType :: Term -> Term
• primNames :: [Name]
• unitTy :: Name
• unitCon :: Name
• unitDecl :: PData' PTerm
• falseTy :: Name
• falseDecl :: PData' PTerm
• pairTy :: Name
• pairCon :: Name
• pairDecl :: PData' PTerm
• eqTy :: Name
• eqCon :: Name
• eqDecl :: PData' PTerm
• sigmaTy :: Name
• existsCon :: Name
• piBind :: [(Name, PTerm)] -> PTerm -> PTerm
• piBindp :: Plicity -> [(Name, PTerm)] -> PTerm -> PTerm
• expandParams :: (Name -> Name) -> [(Name, PTerm)] -> [Name] -> [Name] -> PTerm -> PTerm
• expandParamsD :: Bool -> IState -> (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl
• mapsnd :: (t -> t2) -> (t1, t) -> (t1, t2)
• getPriority :: IState -> PTerm -> Int
• addStatics :: Name -> Term -> PTerm -> Idris ()
• addUsingConstraints :: SyntaxInfo -> FC -> PTerm -> Idris PTerm
• implicit :: SyntaxInfo -> Name -> PTerm -> Idris PTerm
• implicit' :: SyntaxInfo -> [Name] -> Name -> PTerm -> Idris PTerm
• implicitise :: SyntaxInfo -> [Name] -> IState -> PTerm -> (PTerm, [PArg])
• addImplPat :: IState -> PTerm -> PTerm
• addImplBound :: IState -> [Name] -> PTerm -> PTerm
• addImplBoundInf :: IState -> [Name] -> [Name] -> PTerm -> PTerm
• addImpl :: IState -> PTerm -> PTerm
• addImpl' :: Bool -> [Name] -> [Name] -> IState -> PTerm -> PTerm
• aiFn :: Bool -> Bool -> IState -> FC -> Name -> [PArg] -> Either Err PTerm
• stripLinear :: IState -> PTerm -> PTerm
• stripUnmatchable :: IState -> PTerm -> PTerm
• mkPApp :: FC -> Int -> PTerm -> [PArg] -> PTerm
• findStatics :: IState -> PTerm -> (PTerm, [Bool])
• dumpDecls :: [PDecl] -> String
• dumpDecl :: PDecl' PTerm -> [Char]
• data EitherErr a b
  • = LeftErr a
  • | RightOK b
• toEither :: EitherErr a b -> Either a b
• matchClause :: IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
• matchClause' :: Bool -> IState -> PTerm -> PTerm -> Either (PTerm, PTerm) [(Name, PTerm)]
• substMatches :: [(Name, PTerm)] -> PTerm -> PTerm
• substMatchesShadow :: [(Name, PTerm)] -> [Name] -> PTerm -> PTerm
• substMatch :: Name -> PTerm -> PTerm -> PTerm
• substMatchShadow :: Name -> [Name] -> PTerm -> PTerm -> PTerm
• shadow :: Name -> Name -> PTerm -> PTerm
• module Idris.AbsSyntaxTree

Documentation

if it's just a type variable or concrete type, do it early (0)

if there's only type variables and injective constructors, do it next (1)

if there's a function type, next (2)

finally, everything else (3)