git.iko.soy/Idris-dev
on 8a3d348 help sign in
Idris-dev/src/Idris/Reflection.hs
18 lines 572 B history raw
1{-|
2Handy tools for doing reflection.
3-}
4module Idris.Reflection where
6import Idris.Core.TT
7import Idris.AbsSyntaxTree (PArg'(..), PArg, PTerm(Placeholder))
9data RArg = RExplicit { argName :: Name, argTy :: Raw }
10 | RImplicit { argName :: Name, argTy :: Raw }
11 | RConstraint { argName :: Name, argTy :: Raw }
13data RTyDecl = RDeclare Name [RArg] Raw
15rArgToPArg :: RArg -> PArg
16rArgToPArg (RExplicit n _) = PExp 0 [] n Placeholder
17rArgToPArg (RImplicit n _) = PImp 0 False [] n Placeholder
18rArgToPArg (RConstraint n _) = PConstraint 0 [] n Placeholder