@@ -7,6 +7,7 @@ module Idris.Reflection where
8import Control.Applicative ((<$>), (<*>), pure)
8import Control.Applicative ((<$>), (<*>), pure)
9import Control.Monad (liftM, liftM2, liftM4)
9import Control.Monad (liftM, liftM2, liftM4)
10+import Control.Monad.State.Strict (lift)
10import Data.Maybe (catMaybes)
11import Data.Maybe (catMaybes)
11import Data.List ((\\), findIndex)
12import Data.List ((\\), findIndex)
12import qualified Data.Text as T
13import qualified Data.Text as T
@@ -21,6 +22,7 @@ import Idris.AbsSyntaxTree (ArgOpt(..),ElabD, IState(tt_ctxt, idris_implicits,id
21 initEState, pairCon, pairTy)
22 initEState, pairCon, pairTy)
22import Idris.Delaborate (delab)
23import Idris.Delaborate (delab)
24data RErasure = RErased | RNotErased deriving Show
26data RErasure = RErased | RNotErased deriving Show
26data RPlicity = RExplicit | RImplicit | RConstraint deriving Show
28data RPlicity = RExplicit | RImplicit | RConstraint deriving Show
@@ -351,6 +353,11 @@ reifyTTConstApp f (Constant c@(B32 _))
351 | f == reflm "B32" = return $ c
353 | f == reflm "B32" = return $ c
352reifyTTConstApp f (Constant c@(B64 _))
354reifyTTConstApp f (Constant c@(B64 _))
353 | f == reflm "B64" = return $ c
355 | f == reflm "B64" = return $ c
356+reifyTTConstApp f v@(P _ _ _) =
357+ lift . tfail . Msg $
358+ "Can't reify the variable " ++
360+ " as a constant, because its value is not statically known."
354reifyTTConstApp f arg = fail ("Unknown reflection constant: " ++ show (f, arg))
361reifyTTConstApp f arg = fail ("Unknown reflection constant: " ++ show (f, arg))
356reifyArithTy :: Term -> ElabD ArithTy
363reifyArithTy :: Term -> ElabD ArithTy