idris-1.3.0: Functional Programming Language with Dependent Types

LicenseBSD3
MaintainerThe Idris Community.
Safe HaskellNone
LanguageHaskell2010

Idris.Reflection

Description

 

Synopsis

Documentation

data RFunArg Source #

Constructors

RFunArg 

Fields

Instances

data RFunClause a Source #

Constructors

RMkFunClause a a 
RMkImpossibleClause a 

Instances

data RFunDefn a Source #

Constructors

RDefineFun Name [RFunClause a] 

Instances

Show a => Show (RFunDefn a) Source # 

Methods

showsPrec :: Int -> RFunDefn a -> ShowS #

show :: RFunDefn a -> String #

showList :: [RFunDefn a] -> ShowS #

data RTyDecl Source #

Constructors

RDeclare Name [RFunArg] Raw 

Instances

buildDatatypes :: IState -> Name -> [RDatatype] Source #

Build the reflected datatype definition(s) that correspond(s) to a provided unqualified name

buildFunDefns :: IState -> Name -> [RFunDefn Term] Source #

Build the reflected function definition(s) that correspond(s) to a provided unqualifed name

getArgs :: [PArg] -> Raw -> ([RFunArg], Raw) Source #

Apply Idris's implicit info to get a signature. The [PArg] should come from a lookup in idris_implicits on IState.

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

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

rawPair :: (Raw, Raw) -> (Raw, Raw) -> Raw Source #

reflect :: Term -> Raw Source #

Lift a term into its Language.Reflection.TT representation

reflectDatatype :: RDatatype -> Raw Source #

reflectEnv :: Env -> Raw Source #

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

reflectFC :: FC -> Raw Source #

Reflect a file context

reflectRaw :: Raw -> Raw Source #

Lift a term into its Language.Reflection.Raw representation

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

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

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.

reflm :: String -> Name Source #

Prefix a name with the Language.Reflection namespace

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

Reify tactics from their reflected representation

reifyList :: (Term -> ElabD a) -> Term -> ElabD [a] Source #

reifyRaw :: Term -> ElabD Raw Source #

Reify raw terms from their reflected representation

reifyReportPart :: Term -> Either Err ErrorReportPart Source #

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.

reifyTT :: Term -> ElabD Term Source #

Reify terms from their reflected representation

tacN :: String -> Name Source #

Prefix a name with the Language.Reflection.Elab namespace