idris-0.11.1: Functional Programming Language with Dependent Types

Safe HaskellNone



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



data RErasure Source




data RFunArg Source




data RTyDecl Source


RDeclare Name [RFunArg] Raw 


data RFunClause a Source


RMkFunClause a a 
RMkImpossibleClause a 


data RFunDefn a Source


RDefineFun Name [RFunClause a] 


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