idris-0.10.3: Functional Programming Language with Dependent Types

Safe HaskellNone
LanguageHaskell98

Idris.Reflection

Description

Code related to Idris's reflection system. This module contains quoters and unquoters along with some supporting datatypes.

Synopsis

Documentation

data RErasure Source

Constructors

RErased 
RNotErased 

Instances

data RFunArg Source

Constructors

RFunArg 

Instances

data RTyDecl Source

Constructors

RDeclare Name [RFunArg] Raw 

Instances

data RFunClause a Source

Constructors

RMkFunClause a a 
RMkImpossibleClause a 

Instances

data RFunDefn a Source

Constructors

RDefineFun Name [RFunClause a] 

Instances

reflm :: String -> Name Source

Prefix a name with the Language.Reflection namespace

tacN :: String -> Name Source

Prefix a name with the Language.Reflection.Elab namespace

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

Reify tactics from their reflected representation

reifyPair :: (Term -> ElabD a) -> (Term -> ElabD b) -> Term -> ElabD (a, b) Source

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

reifyTT :: Term -> ElabD Term Source

Reify terms from their reflected representation

reifyRaw :: Term -> ElabD Raw Source

Reify raw terms from their reflected representation

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

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.

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

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

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

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 _.

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

mkList :: Raw -> [Raw] -> 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

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

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

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

rawTripleTy :: Raw -> Raw -> Raw -> Raw Source

Idris tuples nest to the right

rawTriple :: (Raw, Raw, Raw) -> (Raw, Raw, Raw) -> Raw Source

reflectFC :: FC -> Raw Source

Reflect a file context

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.

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.

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

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

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

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