@@ -7,6 +7,7 @@ module Idris.Reflection where
77
88import Control.Applicative ((<$>), (<*>), pure)
99import Control.Monad (liftM, liftM2, liftM4)
10+import Control.Monad.State.Strict (lift)
1011import Data.Maybe (catMaybes)
1112import Data.List ((\\), findIndex)
1213import qualified Data.Text as T
@@ -21,6 +22,7 @@ import Idris.AbsSyntaxTree (ArgOpt(..),ElabD, IState(tt_ctxt, idris_implicits,id
2122 initEState, pairCon, pairTy)
2223import Idris.Delaborate (delab)
2324
25+
2426data RErasure = RErased | RNotErased deriving Show
2527
2628data RPlicity = RExplicit | RImplicit | RConstraint deriving Show
@@ -351,6 +353,11 @@ reifyTTConstApp f (Constant c@(B32 _))
351353 | f == reflm "B32" = return $ c
352354reifyTTConstApp f (Constant c@(B64 _))
353355 | f == reflm "B64" = return $ c
356+reifyTTConstApp f v@(P _ _ _) =
357+ lift . tfail . Msg $
358+ "Can't reify the variable " ++
359+ show v ++
360+ " as a constant, because its value is not statically known."
354361reifyTTConstApp f arg = fail ("Unknown reflection constant: " ++ show (f, arg))
355362
356363reifyArithTy :: Term -> ElabD ArithTy