module Agda.TypeChecking.Unquote where

import Control.Arrow (first, second)
import Control.Monad.State
import Control.Monad.Reader
import Control.Monad.Writer hiding ((<>))

import Data.Char
import qualified Data.HashSet as HashSet
import Data.Maybe (fromMaybe)
import Data.Traversable (traverse)
import Data.Word

import Agda.Syntax.Common
import Agda.Syntax.Internal as I
import qualified Agda.Syntax.Reflected as R
import qualified Agda.Syntax.Abstract as A
import Agda.Syntax.Literal
import Agda.Syntax.Position
import Agda.Syntax.Fixity
import Agda.Syntax.Info
import Agda.Syntax.Translation.ReflectedToAbstract

import Agda.TypeChecking.Constraints
import Agda.TypeChecking.MetaVars.Mention
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Monad.Builtin
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Quote
import Agda.TypeChecking.Conversion
import Agda.TypeChecking.EtaContract
import Agda.TypeChecking.Primitive

import {-# SOURCE #-} Agda.TypeChecking.Rules.Term
import {-# SOURCE #-} Agda.TypeChecking.Rules.Def

import Agda.Utils.Except
  ( mkExceptT
  , MonadError(catchError, throwError)
  , ExceptT
  , runExceptT
  )
import Agda.Utils.Either
import Agda.Utils.Lens
import Agda.Utils.Monad
import Agda.Utils.Pretty (prettyShow)
import Agda.Utils.String ( Str(Str), unStr )
import qualified Agda.Interaction.Options.Lenses as Lens

import Agda.Utils.Impossible

agdaTermType :: TCM Type
agdaTermType :: TCM Type
agdaTermType = Sort' Term -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El (Integer -> Sort' Term
mkType Integer
0) (Term -> Type) -> TCMT IO Term -> TCM Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTerm

agdaTypeType :: TCM Type
agdaTypeType :: TCM Type
agdaTypeType = TCM Type
agdaTermType

qNameType :: TCM Type
qNameType :: TCM Type
qNameType = Sort' Term -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El (Integer -> Sort' Term
mkType Integer
0) (Term -> Type) -> TCMT IO Term -> TCM Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primQName

data Dirty = Dirty | Clean
  deriving (Dirty -> Dirty -> Bool
(Dirty -> Dirty -> Bool) -> (Dirty -> Dirty -> Bool) -> Eq Dirty
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Dirty -> Dirty -> Bool
$c/= :: Dirty -> Dirty -> Bool
== :: Dirty -> Dirty -> Bool
$c== :: Dirty -> Dirty -> Bool
Eq)

-- Keep track of the original context. We need to use that when adding new
-- definitions. Also state snapshot from last commit and whether the state is
-- dirty (definitions have been added).
type UnquoteState = (Dirty, TCState)
type UnquoteM = ReaderT Context (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))

type UnquoteRes a = Either UnquoteError ((a, UnquoteState), [QName])

unpackUnquoteM :: UnquoteM a -> Context -> UnquoteState -> TCM (UnquoteRes a)
unpackUnquoteM :: UnquoteM a -> Context -> UnquoteState -> TCM (UnquoteRes a)
unpackUnquoteM UnquoteM a
m Context
cxt UnquoteState
s = ExceptT UnquoteError TCM ((a, UnquoteState), [QName])
-> TCM (UnquoteRes a)
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (ExceptT UnquoteError TCM ((a, UnquoteState), [QName])
 -> TCM (UnquoteRes a))
-> ExceptT UnquoteError TCM ((a, UnquoteState), [QName])
-> TCM (UnquoteRes a)
forall a b. (a -> b) -> a -> b
$ WriterT [QName] (ExceptT UnquoteError TCM) (a, UnquoteState)
-> ExceptT UnquoteError TCM ((a, UnquoteState), [QName])
forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT (WriterT [QName] (ExceptT UnquoteError TCM) (a, UnquoteState)
 -> ExceptT UnquoteError TCM ((a, UnquoteState), [QName]))
-> WriterT [QName] (ExceptT UnquoteError TCM) (a, UnquoteState)
-> ExceptT UnquoteError TCM ((a, UnquoteState), [QName])
forall a b. (a -> b) -> a -> b
$ StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)) a
-> UnquoteState
-> WriterT [QName] (ExceptT UnquoteError TCM) (a, UnquoteState)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (UnquoteM a
-> Context
-> StateT
     UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)) a
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT UnquoteM a
m Context
cxt) UnquoteState
s

packUnquoteM :: (Context -> UnquoteState -> TCM (UnquoteRes a)) -> UnquoteM a
packUnquoteM :: (Context -> UnquoteState -> TCM (UnquoteRes a)) -> UnquoteM a
packUnquoteM Context -> UnquoteState -> TCM (UnquoteRes a)
f = (Context
 -> StateT
      UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)) a)
-> UnquoteM a
forall r (m :: * -> *) a. (r -> m a) -> ReaderT r m a
ReaderT ((Context
  -> StateT
       UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)) a)
 -> UnquoteM a)
-> (Context
    -> StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)) a)
-> UnquoteM a
forall a b. (a -> b) -> a -> b
$ \ Context
cxt -> (UnquoteState
 -> WriterT [QName] (ExceptT UnquoteError TCM) (a, UnquoteState))
-> StateT
     UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)) a
forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
StateT ((UnquoteState
  -> WriterT [QName] (ExceptT UnquoteError TCM) (a, UnquoteState))
 -> StateT
      UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)) a)
-> (UnquoteState
    -> WriterT [QName] (ExceptT UnquoteError TCM) (a, UnquoteState))
-> StateT
     UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)) a
forall a b. (a -> b) -> a -> b
$ \ UnquoteState
s -> ExceptT UnquoteError TCM ((a, UnquoteState), [QName])
-> WriterT [QName] (ExceptT UnquoteError TCM) (a, UnquoteState)
forall w (m :: * -> *) a. m (a, w) -> WriterT w m a
WriterT (ExceptT UnquoteError TCM ((a, UnquoteState), [QName])
 -> WriterT [QName] (ExceptT UnquoteError TCM) (a, UnquoteState))
-> ExceptT UnquoteError TCM ((a, UnquoteState), [QName])
-> WriterT [QName] (ExceptT UnquoteError TCM) (a, UnquoteState)
forall a b. (a -> b) -> a -> b
$ TCM (UnquoteRes a)
-> ExceptT UnquoteError TCM ((a, UnquoteState), [QName])
forall (m :: * -> *) e a. m (Either e a) -> ExceptT e m a
mkExceptT (TCM (UnquoteRes a)
 -> ExceptT UnquoteError TCM ((a, UnquoteState), [QName]))
-> TCM (UnquoteRes a)
-> ExceptT UnquoteError TCM ((a, UnquoteState), [QName])
forall a b. (a -> b) -> a -> b
$ Context -> UnquoteState -> TCM (UnquoteRes a)
f Context
cxt UnquoteState
s

runUnquoteM :: UnquoteM a -> TCM (Either UnquoteError (a, [QName]))
runUnquoteM :: UnquoteM a -> TCM (Either UnquoteError (a, [QName]))
runUnquoteM UnquoteM a
m = do
  Context
cxt <- (TCEnv -> Context) -> TCMT IO Context
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Context
envContext
  TCState
s   <- TCMT IO TCState
forall (m :: * -> *). MonadTCState m => m TCState
getTC
  UnquoteRes a
z   <- UnquoteM a -> Context -> UnquoteState -> TCM (UnquoteRes a)
forall a.
UnquoteM a -> Context -> UnquoteState -> TCM (UnquoteRes a)
unpackUnquoteM UnquoteM a
m Context
cxt (Dirty
Clean, TCState
s)
  case UnquoteRes a
z of
    Left UnquoteError
err              -> Either UnquoteError (a, [QName])
-> TCM (Either UnquoteError (a, [QName]))
forall (m :: * -> *) a. Monad m => a -> m a
return (Either UnquoteError (a, [QName])
 -> TCM (Either UnquoteError (a, [QName])))
-> Either UnquoteError (a, [QName])
-> TCM (Either UnquoteError (a, [QName]))
forall a b. (a -> b) -> a -> b
$ UnquoteError -> Either UnquoteError (a, [QName])
forall a b. a -> Either a b
Left UnquoteError
err
    Right ((a
x, UnquoteState
_), [QName]
decls) -> (a, [QName]) -> Either UnquoteError (a, [QName])
forall a b. b -> Either a b
Right (a
x, [QName]
decls) Either UnquoteError (a, [QName])
-> TCMT IO () -> TCM (Either UnquoteError (a, [QName]))
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ (QName -> TCMT IO ()) -> [QName] -> TCMT IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ QName -> TCMT IO ()
forall (m :: * -> *).
(HasConstInfo m, ReadTCState m, MonadError TCErr m) =>
QName -> m ()
isDefined [QName]
decls
  where
    isDefined :: QName -> m ()
isDefined QName
x = do
      Defn
def <- Definition -> Defn
theDef (Definition -> Defn) -> m Definition -> m Defn
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
x
      case Defn
def of
        Function{funClauses :: Defn -> [Clause]
funClauses = []} -> String -> m ()
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
String -> m a
genericError (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ String
"Missing definition for " String -> String -> String
forall a. [a] -> [a] -> [a]
++ QName -> String
forall a. Pretty a => a -> String
prettyShow QName
x
        Defn
_       -> () -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

liftU1 :: (TCM (UnquoteRes a) -> TCM (UnquoteRes b)) -> UnquoteM a -> UnquoteM b
liftU1 :: (TCM (UnquoteRes a) -> TCM (UnquoteRes b))
-> UnquoteM a -> UnquoteM b
liftU1 TCM (UnquoteRes a) -> TCM (UnquoteRes b)
f UnquoteM a
m = (Context -> UnquoteState -> TCM (UnquoteRes b)) -> UnquoteM b
forall a.
(Context -> UnquoteState -> TCM (UnquoteRes a)) -> UnquoteM a
packUnquoteM ((Context -> UnquoteState -> TCM (UnquoteRes b)) -> UnquoteM b)
-> (Context -> UnquoteState -> TCM (UnquoteRes b)) -> UnquoteM b
forall a b. (a -> b) -> a -> b
$ \ Context
cxt UnquoteState
s -> TCM (UnquoteRes a) -> TCM (UnquoteRes b)
f (UnquoteM a -> Context -> UnquoteState -> TCM (UnquoteRes a)
forall a.
UnquoteM a -> Context -> UnquoteState -> TCM (UnquoteRes a)
unpackUnquoteM UnquoteM a
m Context
cxt UnquoteState
s)

liftU2 :: (TCM (UnquoteRes a) -> TCM (UnquoteRes b) -> TCM (UnquoteRes c)) -> UnquoteM a -> UnquoteM b -> UnquoteM c
liftU2 :: (TCM (UnquoteRes a) -> TCM (UnquoteRes b) -> TCM (UnquoteRes c))
-> UnquoteM a -> UnquoteM b -> UnquoteM c
liftU2 TCM (UnquoteRes a) -> TCM (UnquoteRes b) -> TCM (UnquoteRes c)
f UnquoteM a
m1 UnquoteM b
m2 = (Context -> UnquoteState -> TCM (UnquoteRes c)) -> UnquoteM c
forall a.
(Context -> UnquoteState -> TCM (UnquoteRes a)) -> UnquoteM a
packUnquoteM ((Context -> UnquoteState -> TCM (UnquoteRes c)) -> UnquoteM c)
-> (Context -> UnquoteState -> TCM (UnquoteRes c)) -> UnquoteM c
forall a b. (a -> b) -> a -> b
$ \ Context
cxt UnquoteState
s -> TCM (UnquoteRes a) -> TCM (UnquoteRes b) -> TCM (UnquoteRes c)
f (UnquoteM a -> Context -> UnquoteState -> TCM (UnquoteRes a)
forall a.
UnquoteM a -> Context -> UnquoteState -> TCM (UnquoteRes a)
unpackUnquoteM UnquoteM a
m1 Context
cxt UnquoteState
s) (UnquoteM b -> Context -> UnquoteState -> TCM (UnquoteRes b)
forall a.
UnquoteM a -> Context -> UnquoteState -> TCM (UnquoteRes a)
unpackUnquoteM UnquoteM b
m2 Context
cxt UnquoteState
s)

inOriginalContext :: UnquoteM a -> UnquoteM a
inOriginalContext :: UnquoteM a -> UnquoteM a
inOriginalContext UnquoteM a
m =
  (Context -> UnquoteState -> TCM (UnquoteRes a)) -> UnquoteM a
forall a.
(Context -> UnquoteState -> TCM (UnquoteRes a)) -> UnquoteM a
packUnquoteM ((Context -> UnquoteState -> TCM (UnquoteRes a)) -> UnquoteM a)
-> (Context -> UnquoteState -> TCM (UnquoteRes a)) -> UnquoteM a
forall a b. (a -> b) -> a -> b
$ \ Context
cxt UnquoteState
s ->
    (Context -> Context) -> TCM (UnquoteRes a) -> TCM (UnquoteRes a)
forall (tcm :: * -> *) a.
MonadTCEnv tcm =>
(Context -> Context) -> tcm a -> tcm a
unsafeModifyContext (Context -> Context -> Context
forall a b. a -> b -> a
const Context
cxt) (TCM (UnquoteRes a) -> TCM (UnquoteRes a))
-> TCM (UnquoteRes a) -> TCM (UnquoteRes a)
forall a b. (a -> b) -> a -> b
$ UnquoteM a -> Context -> UnquoteState -> TCM (UnquoteRes a)
forall a.
UnquoteM a -> Context -> UnquoteState -> TCM (UnquoteRes a)
unpackUnquoteM UnquoteM a
m Context
cxt UnquoteState
s

isCon :: ConHead -> TCM Term -> UnquoteM Bool
isCon :: ConHead -> TCMT IO Term -> UnquoteM Bool
isCon ConHead
con TCMT IO Term
tm = do Term
t <- TCMT IO Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM TCMT IO Term
tm
                  case Term
t of
                    Con ConHead
con' ConInfo
_ Elims
_ -> Bool -> UnquoteM Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (ConHead
con ConHead -> ConHead -> Bool
forall a. Eq a => a -> a -> Bool
== ConHead
con')
                    Term
_ -> Bool -> UnquoteM Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

isDef :: QName -> TCM Term -> UnquoteM Bool
isDef :: QName -> TCMT IO Term -> UnquoteM Bool
isDef QName
f TCMT IO Term
tm = do
  Term
t <- TCMT IO Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCMT IO Term
 -> ReaderT
      Context
      (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
      Term)
-> TCMT IO Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
forall a b. (a -> b) -> a -> b
$ Term -> TCMT IO Term
forall (m :: * -> *) a.
(MonadTCEnv m, HasConstInfo m, HasOptions m, TermLike a) =>
a -> m a
etaContract (Term -> TCMT IO Term) -> TCMT IO Term -> TCMT IO Term
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Term -> TCMT IO Term
forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
normalise (Term -> TCMT IO Term) -> TCMT IO Term -> TCMT IO Term
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO Term
tm
  case Term
t of
    Def QName
g Elims
_ -> Bool -> UnquoteM Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (QName
f QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
g)
    Term
_       -> Bool -> UnquoteM Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

reduceQuotedTerm :: Term -> UnquoteM Term
reduceQuotedTerm :: Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
reduceQuotedTerm Term
t = do
  Either MetaId Term
b <- Term
-> (MetaId
    -> Term
    -> ReaderT
         Context
         (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
         (Either MetaId Term))
-> (NotBlocked
    -> Term
    -> ReaderT
         Context
         (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
         (Either MetaId Term))
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     (Either MetaId Term)
forall t (m :: * -> *) a.
(Reduce t, IsMeta t, MonadReduce m, HasBuiltins m) =>
t -> (MetaId -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
ifBlocked Term
t {-then-} (\ MetaId
m Term
_ -> Either MetaId Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     (Either MetaId Term)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either MetaId Term
 -> ReaderT
      Context
      (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
      (Either MetaId Term))
-> Either MetaId Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     (Either MetaId Term)
forall a b. (a -> b) -> a -> b
$ MetaId -> Either MetaId Term
forall a b. a -> Either a b
Left  MetaId
m)
                   {-else-} (\ NotBlocked
_ Term
t -> Either MetaId Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     (Either MetaId Term)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either MetaId Term
 -> ReaderT
      Context
      (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
      (Either MetaId Term))
-> Either MetaId Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     (Either MetaId Term)
forall a b. (a -> b) -> a -> b
$ Term -> Either MetaId Term
forall a b. b -> Either a b
Right Term
t)
  case Either MetaId Term
b of
    Left MetaId
m  -> do TCState
s <- (UnquoteState -> TCState)
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     TCState
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets UnquoteState -> TCState
forall a b. (a, b) -> b
snd; UnquoteError
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (UnquoteError
 -> ReaderT
      Context
      (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
      Term)
-> UnquoteError
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
forall a b. (a -> b) -> a -> b
$ TCState -> MetaId -> UnquoteError
BlockedOnMeta TCState
s MetaId
m
    Right Term
t -> Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
t

class Unquote a where
  unquote :: I.Term -> UnquoteM a

unquoteN :: Unquote a => Arg Term -> UnquoteM a
unquoteN :: Arg Term -> UnquoteM a
unquoteN Arg Term
a | Arg Term -> Bool
forall a. LensHiding a => a -> Bool
visible Arg Term
a Bool -> Bool -> Bool
&& Arg Term -> Bool
forall a. LensRelevance a => a -> Bool
isRelevant Arg Term
a =
    Term -> UnquoteM a
forall a. Unquote a => Term -> UnquoteM a
unquote (Term -> UnquoteM a) -> Term -> UnquoteM a
forall a b. (a -> b) -> a -> b
$ Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
a
unquoteN Arg Term
a = UnquoteError -> UnquoteM a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (UnquoteError -> UnquoteM a) -> UnquoteError -> UnquoteM a
forall a b. (a -> b) -> a -> b
$ String -> Arg Term -> UnquoteError
BadVisibility String
"visible" Arg Term
a

choice :: Monad m => [(m Bool, m a)] -> m a -> m a
choice :: [(m Bool, m a)] -> m a -> m a
choice [] m a
dflt = m a
dflt
choice ((m Bool
mb, m a
mx) : [(m Bool, m a)]
mxs) m a
dflt = m Bool -> m a -> m a -> m a
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM m Bool
mb m a
mx (m a -> m a) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ [(m Bool, m a)] -> m a -> m a
forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
choice [(m Bool, m a)]
mxs m a
dflt

ensureDef :: QName -> UnquoteM QName
ensureDef :: QName -> UnquoteM QName
ensureDef QName
x = do
  Defn
i <- (SigError -> Defn)
-> (Definition -> Defn) -> Either SigError Definition -> Defn
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Defn -> SigError -> Defn
forall a b. a -> b -> a
const Defn
Axiom) Definition -> Defn
theDef (Either SigError Definition -> Defn)
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     (Either SigError Definition)
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Defn
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     (Either SigError Definition)
forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Either SigError Definition)
getConstInfo' QName
x  -- for recursive unquoteDecl
  case Defn
i of
    Constructor{} -> do
      Doc
def <- TCM Doc
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Doc
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM Doc
 -> ReaderT
      Context
      (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
      Doc)
-> TCM Doc
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Doc
forall a b. (a -> b) -> a -> b
$ Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Term -> TCM Doc) -> TCMT IO Term -> TCM Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTermDef
      Doc
con <- TCM Doc
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Doc
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM Doc
 -> ReaderT
      Context
      (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
      Doc)
-> TCM Doc
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Doc
forall a b. (a -> b) -> a -> b
$ Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Term -> TCM Doc) -> TCMT IO Term -> TCM Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTermCon
      UnquoteError -> UnquoteM QName
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (UnquoteError -> UnquoteM QName) -> UnquoteError -> UnquoteM QName
forall a b. (a -> b) -> a -> b
$ QName -> String -> String -> UnquoteError
ConInsteadOfDef QName
x (Doc -> String
forall a. Show a => a -> String
show Doc
def) (Doc -> String
forall a. Show a => a -> String
show Doc
con)
    Defn
_ -> QName -> UnquoteM QName
forall (m :: * -> *) a. Monad m => a -> m a
return QName
x

ensureCon :: QName -> UnquoteM QName
ensureCon :: QName -> UnquoteM QName
ensureCon QName
x = do
  Defn
i <- (SigError -> Defn)
-> (Definition -> Defn) -> Either SigError Definition -> Defn
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Defn -> SigError -> Defn
forall a b. a -> b -> a
const Defn
Axiom) Definition -> Defn
theDef (Either SigError Definition -> Defn)
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     (Either SigError Definition)
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Defn
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     (Either SigError Definition)
forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Either SigError Definition)
getConstInfo' QName
x  -- for recursive unquoteDecl
  case Defn
i of
    Constructor{} -> QName -> UnquoteM QName
forall (m :: * -> *) a. Monad m => a -> m a
return QName
x
    Defn
_ -> do
      Doc
def <- TCM Doc
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Doc
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM Doc
 -> ReaderT
      Context
      (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
      Doc)
-> TCM Doc
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Doc
forall a b. (a -> b) -> a -> b
$ Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Term -> TCM Doc) -> TCMT IO Term -> TCM Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTermDef
      Doc
con <- TCM Doc
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Doc
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM Doc
 -> ReaderT
      Context
      (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
      Doc)
-> TCM Doc
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Doc
forall a b. (a -> b) -> a -> b
$ Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Term -> TCM Doc) -> TCMT IO Term -> TCM Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTermCon
      UnquoteError -> UnquoteM QName
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (UnquoteError -> UnquoteM QName) -> UnquoteError -> UnquoteM QName
forall a b. (a -> b) -> a -> b
$ QName -> String -> String -> UnquoteError
DefInsteadOfCon QName
x (Doc -> String
forall a. Show a => a -> String
show Doc
def) (Doc -> String
forall a. Show a => a -> String
show Doc
con)

pickName :: R.Type -> String
pickName :: Type -> String
pickName Type
a =
  case Type
a of
    R.Pi{}   -> String
"f"
    R.Sort{} -> String
"A"
    R.Def QName
d Elims
_ | Char
c:String
_ <- Name -> String
forall a. Show a => a -> String
show (QName -> Name
qnameName QName
d),
              Char -> Bool
isAlpha Char
c -> [Char -> Char
toLower Char
c]
    Type
_        -> String
"_"

-- TODO: reflect Quantity, Cohesion
instance Unquote Modality where
  unquote :: Term -> UnquoteM Modality
unquote Term
t = (\ Relevance
r -> Relevance -> Quantity -> Cohesion -> Modality
Modality Relevance
r Quantity
defaultQuantity Cohesion
defaultCohesion) (Relevance -> Modality)
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Relevance
-> UnquoteM Modality
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Relevance
forall a. Unquote a => Term -> UnquoteM a
unquote Term
t

instance Unquote ArgInfo where
  unquote :: Term -> UnquoteM ArgInfo
unquote Term
t = do
    Term
t <- Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
reduceQuotedTerm Term
t
    case Term
t of
      Con ConHead
c ConInfo
_ Elims
es | Just [Arg Term
h,Arg Term
r] <- Elims -> Maybe [Arg Term]
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es ->
        [(UnquoteM Bool, UnquoteM ArgInfo)]
-> UnquoteM ArgInfo -> UnquoteM ArgInfo
forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
choice
          [(ConHead
c ConHead -> TCMT IO Term -> UnquoteM Bool
`isCon` TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primArgArgInfo,
              Hiding -> Modality -> Origin -> FreeVariables -> ArgInfo
ArgInfo (Hiding -> Modality -> Origin -> FreeVariables -> ArgInfo)
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Hiding
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     (Modality -> Origin -> FreeVariables -> ArgInfo)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Arg Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Hiding
forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
h ReaderT
  Context
  (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
  (Modality -> Origin -> FreeVariables -> ArgInfo)
-> UnquoteM Modality
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     (Origin -> FreeVariables -> ArgInfo)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Arg Term -> UnquoteM Modality
forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
r ReaderT
  Context
  (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
  (Origin -> FreeVariables -> ArgInfo)
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Origin
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     (FreeVariables -> ArgInfo)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Origin
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Origin
forall (f :: * -> *) a. Applicative f => a -> f a
pure Origin
Reflected ReaderT
  Context
  (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
  (FreeVariables -> ArgInfo)
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     FreeVariables
-> UnquoteM ArgInfo
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> FreeVariables
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     FreeVariables
forall (f :: * -> *) a. Applicative f => a -> f a
pure FreeVariables
unknownFreeVariables)]
          UnquoteM ArgInfo
forall a. HasCallStack => a
__IMPOSSIBLE__
      Con ConHead
c ConInfo
_ Elims
_ -> UnquoteM ArgInfo
forall a. HasCallStack => a
__IMPOSSIBLE__
      Term
_ -> UnquoteError -> UnquoteM ArgInfo
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (UnquoteError -> UnquoteM ArgInfo)
-> UnquoteError -> UnquoteM ArgInfo
forall a b. (a -> b) -> a -> b
$ String -> Term -> UnquoteError
NonCanonical String
"arg info" Term
t

instance Unquote a => Unquote (Arg a) where
  unquote :: Term -> UnquoteM (Arg a)
unquote Term
t = do
    Term
t <- Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
reduceQuotedTerm Term
t
    case Term
t of
      Con ConHead
c ConInfo
_ Elims
es | Just [Arg Term
info,Arg Term
x] <- Elims -> Maybe [Arg Term]
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es ->
        [(UnquoteM Bool, UnquoteM (Arg a))]
-> UnquoteM (Arg a) -> UnquoteM (Arg a)
forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
choice
          [(ConHead
c ConHead -> TCMT IO Term -> UnquoteM Bool
`isCon` TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primArgArg, ArgInfo -> a -> Arg a
forall e. ArgInfo -> e -> Arg e
Arg (ArgInfo -> a -> Arg a)
-> UnquoteM ArgInfo
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     (a -> Arg a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Arg Term -> UnquoteM ArgInfo
forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
info ReaderT
  Context
  (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
  (a -> Arg a)
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     a
-> UnquoteM (Arg a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Arg Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     a
forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
x)]
          UnquoteM (Arg a)
forall a. HasCallStack => a
__IMPOSSIBLE__
      Con ConHead
c ConInfo
_ Elims
_ -> UnquoteM (Arg a)
forall a. HasCallStack => a
__IMPOSSIBLE__
      Term
_ -> UnquoteError -> UnquoteM (Arg a)
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (UnquoteError -> UnquoteM (Arg a))
-> UnquoteError -> UnquoteM (Arg a)
forall a b. (a -> b) -> a -> b
$ String -> Term -> UnquoteError
NonCanonical String
"arg" Term
t

-- Andreas, 2013-10-20: currently, post-fix projections are not part of the
-- quoted syntax.
instance Unquote R.Elim where
  unquote :: Term -> UnquoteM Elim
unquote Term
t = Arg Type -> Elim
forall a. Arg a -> Elim' a
R.Apply (Arg Type -> Elim)
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     (Arg Type)
-> UnquoteM Elim
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     (Arg Type)
forall a. Unquote a => Term -> UnquoteM a
unquote Term
t

instance Unquote Bool where
  unquote :: Term -> UnquoteM Bool
unquote Term
t = do
    Term
t <- Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
reduceQuotedTerm Term
t
    case Term
t of
      Con ConHead
c ConInfo
_ [] ->
        [(UnquoteM Bool, UnquoteM Bool)] -> UnquoteM Bool -> UnquoteM Bool
forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
choice [ (ConHead
c ConHead -> TCMT IO Term -> UnquoteM Bool
`isCon` TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primTrue,  Bool -> UnquoteM Bool
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True)
               , (ConHead
c ConHead -> TCMT IO Term -> UnquoteM Bool
`isCon` TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primFalse, Bool -> UnquoteM Bool
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False) ]
               UnquoteM Bool
forall a. HasCallStack => a
__IMPOSSIBLE__
      Term
_ -> UnquoteError -> UnquoteM Bool
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (UnquoteError -> UnquoteM Bool) -> UnquoteError -> UnquoteM Bool
forall a b. (a -> b) -> a -> b
$ String -> Term -> UnquoteError
NonCanonical String
"boolean" Term
t

instance Unquote Integer where
  unquote :: Term -> UnquoteM Integer
unquote Term
t = do
    Term
t <- Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
reduceQuotedTerm Term
t
    case Term
t of
      Lit (LitNat Range
_ Integer
n) -> Integer -> UnquoteM Integer
forall (m :: * -> *) a. Monad m => a -> m a
return Integer
n
      Term
_ -> UnquoteError -> UnquoteM Integer
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (UnquoteError -> UnquoteM Integer)
-> UnquoteError -> UnquoteM Integer
forall a b. (a -> b) -> a -> b
$ String -> Term -> UnquoteError
NonCanonical String
"integer" Term
t

instance Unquote Word64 where
  unquote :: Term -> UnquoteM Word64
unquote Term
t = do
    Term
t <- Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
reduceQuotedTerm Term
t
    case Term
t of
      Lit (LitWord64 Range
_ Word64
n) -> Word64 -> UnquoteM Word64
forall (m :: * -> *) a. Monad m => a -> m a
return Word64
n
      Term
_ -> UnquoteError -> UnquoteM Word64
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (UnquoteError -> UnquoteM Word64)
-> UnquoteError -> UnquoteM Word64
forall a b. (a -> b) -> a -> b
$ String -> Term -> UnquoteError
NonCanonical String
"word64" Term
t

instance Unquote Double where
  unquote :: Term -> UnquoteM Double
unquote Term
t = do
    Term
t <- Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
reduceQuotedTerm Term
t
    case Term
t of
      Lit (LitFloat Range
_ Double
x) -> Double -> UnquoteM Double
forall (m :: * -> *) a. Monad m => a -> m a
return Double
x
      Term
_ -> UnquoteError -> UnquoteM Double
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (UnquoteError -> UnquoteM Double)
-> UnquoteError -> UnquoteM Double
forall a b. (a -> b) -> a -> b
$ String -> Term -> UnquoteError
NonCanonical String
"float" Term
t

instance Unquote Char where
  unquote :: Term -> UnquoteM Char
unquote Term
t = do
    Term
t <- Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
reduceQuotedTerm Term
t
    case Term
t of
      Lit (LitChar Range
_ Char
x) -> Char -> UnquoteM Char
forall (m :: * -> *) a. Monad m => a -> m a
return Char
x
      Term
_ -> UnquoteError -> UnquoteM Char
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (UnquoteError -> UnquoteM Char) -> UnquoteError -> UnquoteM Char
forall a b. (a -> b) -> a -> b
$ String -> Term -> UnquoteError
NonCanonical String
"char" Term
t

instance Unquote Str where
  unquote :: Term -> UnquoteM Str
unquote Term
t = do
    Term
t <- Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
reduceQuotedTerm Term
t
    case Term
t of
      Lit (LitString Range
_ String
x) -> Str -> UnquoteM Str
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Str
Str String
x)
      Term
_ -> UnquoteError -> UnquoteM Str
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (UnquoteError -> UnquoteM Str) -> UnquoteError -> UnquoteM Str
forall a b. (a -> b) -> a -> b
$ String -> Term -> UnquoteError
NonCanonical String
"string" Term
t

unquoteString :: Term -> UnquoteM String
unquoteString :: Term -> UnquoteM String
unquoteString Term
x = Str -> String
unStr (Str -> String) -> UnquoteM Str -> UnquoteM String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> UnquoteM Str
forall a. Unquote a => Term -> UnquoteM a
unquote Term
x

unquoteNString :: Arg Term -> UnquoteM String
unquoteNString :: Arg Term -> UnquoteM String
unquoteNString Arg Term
x = Str -> String
unStr (Str -> String) -> UnquoteM Str -> UnquoteM String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Arg Term -> UnquoteM Str
forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
x

data ErrorPart = StrPart String | TermPart A.Expr | NamePart QName

instance PrettyTCM ErrorPart where
  prettyTCM :: ErrorPart -> m Doc
prettyTCM (StrPart String
s) = String -> m Doc
forall (m :: * -> *). Monad m => String -> m Doc
text String
s
  prettyTCM (TermPart Expr
t) = Expr -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Expr
t
  prettyTCM (NamePart QName
x) = QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
x

instance Unquote ErrorPart where
  unquote :: Term -> UnquoteM ErrorPart
unquote Term
t = do
    Term
t <- Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
reduceQuotedTerm Term
t
    case Term
t of
      Con ConHead
c ConInfo
_ Elims
es | Just [Arg Term
x] <- Elims -> Maybe [Arg Term]
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es ->
        [(UnquoteM Bool, UnquoteM ErrorPart)]
-> UnquoteM ErrorPart -> UnquoteM ErrorPart
forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
choice [ (ConHead
c ConHead -> TCMT IO Term -> UnquoteM Bool
`isCon` TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaErrorPartString, String -> ErrorPart
StrPart  (String -> ErrorPart) -> UnquoteM String -> UnquoteM ErrorPart
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Arg Term -> UnquoteM String
unquoteNString Arg Term
x)
               , (ConHead
c ConHead -> TCMT IO Term -> UnquoteM Bool
`isCon` TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaErrorPartTerm,   Expr -> ErrorPart
TermPart (Expr -> ErrorPart)
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Expr
-> UnquoteM ErrorPart
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((TCM Expr
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Expr
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM Expr
 -> ReaderT
      Context
      (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
      Expr)
-> (Type -> TCM Expr)
-> Type
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> TCM Expr
forall r a (m :: * -> *).
(ToAbstract r a, MonadFresh NameId m, MonadError TCErr m,
 MonadTCEnv m, ReadTCState m, HasOptions m, HasConstInfo m) =>
r -> m a
toAbstractWithoutImplicit) (Type
 -> ReaderT
      Context
      (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
      Expr)
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Type
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (Arg Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Type
forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
x :: UnquoteM R.Term)))
               , (ConHead
c ConHead -> TCMT IO Term -> UnquoteM Bool
`isCon` TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaErrorPartName,   QName -> ErrorPart
NamePart (QName -> ErrorPart) -> UnquoteM QName -> UnquoteM ErrorPart
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Arg Term -> UnquoteM QName
forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
x) ]
               UnquoteM ErrorPart
forall a. HasCallStack => a
__IMPOSSIBLE__
      Term
_ -> UnquoteError -> UnquoteM ErrorPart
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (UnquoteError -> UnquoteM ErrorPart)
-> UnquoteError -> UnquoteM ErrorPart
forall a b. (a -> b) -> a -> b
$ String -> Term -> UnquoteError
NonCanonical String
"error part" Term
t

instance Unquote a => Unquote [a] where
  unquote :: Term -> UnquoteM [a]
unquote Term
t = do
    Term
t <- Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
reduceQuotedTerm Term
t
    case Term
t of
      Con ConHead
c ConInfo
_ Elims
es | Just [Arg Term
x,Arg Term
xs] <- Elims -> Maybe [Arg Term]
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es ->
        [(UnquoteM Bool, UnquoteM [a])] -> UnquoteM [a] -> UnquoteM [a]
forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
choice
          [(ConHead
c ConHead -> TCMT IO Term -> UnquoteM Bool
`isCon` TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primCons, (:) (a -> [a] -> [a])
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     a
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     ([a] -> [a])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Arg Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     a
forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
x ReaderT
  Context
  (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
  ([a] -> [a])
-> UnquoteM [a] -> UnquoteM [a]
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Arg Term -> UnquoteM [a]
forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
xs)]
          UnquoteM [a]
forall a. HasCallStack => a
__IMPOSSIBLE__
      Con ConHead
c ConInfo
_ [] ->
        [(UnquoteM Bool, UnquoteM [a])] -> UnquoteM [a] -> UnquoteM [a]
forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
choice
          [(ConHead
c ConHead -> TCMT IO Term -> UnquoteM Bool
`isCon` TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primNil, [a] -> UnquoteM [a]
forall (m :: * -> *) a. Monad m => a -> m a
return [])]
          UnquoteM [a]
forall a. HasCallStack => a
__IMPOSSIBLE__
      Con ConHead
c ConInfo
_ Elims
_ -> UnquoteM [a]
forall a. HasCallStack => a
__IMPOSSIBLE__
      Term
_ -> UnquoteError -> UnquoteM [a]
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (UnquoteError -> UnquoteM [a]) -> UnquoteError -> UnquoteM [a]
forall a b. (a -> b) -> a -> b
$ String -> Term -> UnquoteError
NonCanonical String
"list" Term
t

instance Unquote Hiding where
  unquote :: Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Hiding
unquote Term
t = do
    Term
t <- Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
reduceQuotedTerm Term
t
    case Term
t of
      Con ConHead
c ConInfo
_ [] ->
        [(UnquoteM Bool,
  ReaderT
    Context
    (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
    Hiding)]
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Hiding
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Hiding
forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
choice
          [(ConHead
c ConHead -> TCMT IO Term -> UnquoteM Bool
`isCon` TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primHidden,  Hiding
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Hiding
forall (m :: * -> *) a. Monad m => a -> m a
return Hiding
Hidden)
          ,(ConHead
c ConHead -> TCMT IO Term -> UnquoteM Bool
`isCon` TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primInstance, Hiding
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Hiding
forall (m :: * -> *) a. Monad m => a -> m a
return (Overlappable -> Hiding
Instance Overlappable
NoOverlap))
          ,(ConHead
c ConHead -> TCMT IO Term -> UnquoteM Bool
`isCon` TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primVisible, Hiding
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Hiding
forall (m :: * -> *) a. Monad m => a -> m a
return Hiding
NotHidden)]
          ReaderT
  Context
  (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
  Hiding
forall a. HasCallStack => a
__IMPOSSIBLE__
      Con ConHead
c ConInfo
_ Elims
vs -> ReaderT
  Context
  (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
  Hiding
forall a. HasCallStack => a
__IMPOSSIBLE__
      Term
_        -> UnquoteError
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Hiding
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (UnquoteError
 -> ReaderT
      Context
      (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
      Hiding)
-> UnquoteError
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Hiding
forall a b. (a -> b) -> a -> b
$ String -> Term -> UnquoteError
NonCanonical String
"visibility" Term
t

instance Unquote Relevance where
  unquote :: Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Relevance
unquote Term
t = do
    Term
t <- Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
reduceQuotedTerm Term
t
    case Term
t of
      Con ConHead
c ConInfo
_ [] ->
        [(UnquoteM Bool,
  ReaderT
    Context
    (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
    Relevance)]
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Relevance
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Relevance
forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
choice
          [(ConHead
c ConHead -> TCMT IO Term -> UnquoteM Bool
`isCon` TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primRelevant,   Relevance
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Relevance
forall (m :: * -> *) a. Monad m => a -> m a
return Relevance
Relevant)
          ,(ConHead
c ConHead -> TCMT IO Term -> UnquoteM Bool
`isCon` TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIrrelevant, Relevance
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Relevance
forall (m :: * -> *) a. Monad m => a -> m a
return Relevance
Irrelevant)]
          ReaderT
  Context
  (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
  Relevance
forall a. HasCallStack => a
__IMPOSSIBLE__
      Con ConHead
c ConInfo
_ Elims
vs -> ReaderT
  Context
  (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
  Relevance
forall a. HasCallStack => a
__IMPOSSIBLE__
      Term
_        -> UnquoteError
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Relevance
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (UnquoteError
 -> ReaderT
      Context
      (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
      Relevance)
-> UnquoteError
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Relevance
forall a b. (a -> b) -> a -> b
$ String -> Term -> UnquoteError
NonCanonical String
"relevance" Term
t

instance Unquote QName where
  unquote :: Term -> UnquoteM QName
unquote Term
t = do
    Term
t <- Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
reduceQuotedTerm Term
t
    case Term
t of
      Lit (LitQName Range
_ QName
x) -> QName -> UnquoteM QName
forall (m :: * -> *) a. Monad m => a -> m a
return QName
x
      Term
_                  -> UnquoteError -> UnquoteM QName
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (UnquoteError -> UnquoteM QName) -> UnquoteError -> UnquoteM QName
forall a b. (a -> b) -> a -> b
$ String -> Term -> UnquoteError
NonCanonical String
"name" Term
t

instance Unquote a => Unquote (R.Abs a) where
  unquote :: Term -> UnquoteM (Abs a)
unquote Term
t = do
    Term
t <- Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
reduceQuotedTerm Term
t
    case Term
t of
      Con ConHead
c ConInfo
_ Elims
es | Just [Arg Term
x,Arg Term
y] <- Elims -> Maybe [Arg Term]
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es ->
        [(UnquoteM Bool, UnquoteM (Abs a))]
-> UnquoteM (Abs a) -> UnquoteM (Abs a)
forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
choice
          [(ConHead
c ConHead -> TCMT IO Term -> UnquoteM Bool
`isCon` TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAbsAbs, String -> a -> Abs a
forall a. String -> a -> Abs a
R.Abs (String -> a -> Abs a)
-> UnquoteM String
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     (a -> Abs a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> String
forall (t :: * -> *) a. (Foldable t, IsString (t a)) => t a -> t a
hint (String -> String) -> UnquoteM String -> UnquoteM String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Arg Term -> UnquoteM String
unquoteNString Arg Term
x) ReaderT
  Context
  (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
  (a -> Abs a)
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     a
-> UnquoteM (Abs a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Arg Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     a
forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
y)]
          UnquoteM (Abs a)
forall a. HasCallStack => a
__IMPOSSIBLE__
      Con ConHead
c ConInfo
_ Elims
_ -> UnquoteM (Abs a)
forall a. HasCallStack => a
__IMPOSSIBLE__
      Term
_ -> UnquoteError -> UnquoteM (Abs a)
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (UnquoteError -> UnquoteM (Abs a))
-> UnquoteError -> UnquoteM (Abs a)
forall a b. (a -> b) -> a -> b
$ String -> Term -> UnquoteError
NonCanonical String
"abstraction" Term
t

    where hint :: t a -> t a
hint t a
x | Bool -> Bool
not (t a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null t a
x) = t a
x
                 | Bool
otherwise    = t a
"_"

instance Unquote MetaId where
  unquote :: Term -> UnquoteM MetaId
unquote Term
t = do
    Term
t <- Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
reduceQuotedTerm Term
t
    case Term
t of
      Lit (LitMeta Range
r AbsolutePath
f MetaId
x) -> TCM MetaId -> UnquoteM MetaId
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM MetaId -> UnquoteM MetaId) -> TCM MetaId -> UnquoteM MetaId
forall a b. (a -> b) -> a -> b
$ do
        Bool
live <- (AbsolutePath
f AbsolutePath -> AbsolutePath -> Bool
forall a. Eq a => a -> a -> Bool
==) (AbsolutePath -> Bool) -> TCMT IO AbsolutePath -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO AbsolutePath
forall (m :: * -> *). MonadTCEnv m => m AbsolutePath
getCurrentPath
        Bool -> TCMT IO () -> TCMT IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
live (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ do
            TopLevelModuleName
m <- TopLevelModuleName
-> Maybe TopLevelModuleName -> TopLevelModuleName
forall a. a -> Maybe a -> a
fromMaybe TopLevelModuleName
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe TopLevelModuleName -> TopLevelModuleName)
-> TCMT IO (Maybe TopLevelModuleName) -> TCMT IO TopLevelModuleName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> AbsolutePath -> TCMT IO (Maybe TopLevelModuleName)
forall (m :: * -> *).
ReadTCState m =>
AbsolutePath -> m (Maybe TopLevelModuleName)
lookupModuleFromSource AbsolutePath
f
            TypeError -> TCMT IO ()
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO ())
-> (Doc -> TypeError) -> Doc -> TCMT IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError (Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<
              [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep [ TCM Doc
"Can't unquote stale metavariable"
                  , TopLevelModuleName -> TCM Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty TopLevelModuleName
m TCM Doc -> TCM Doc -> TCM Doc
forall a. Semigroup a => a -> a -> a
<> TCM Doc
"." TCM Doc -> TCM Doc -> TCM Doc
forall a. Semigroup a => a -> a -> a
<> MetaId -> TCM Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty MetaId
x ]
        MetaId -> TCM MetaId
forall (m :: * -> *) a. Monad m => a -> m a
return MetaId
x
      Term
_ -> UnquoteError -> UnquoteM MetaId
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (UnquoteError -> UnquoteM MetaId)
-> UnquoteError -> UnquoteM MetaId
forall a b. (a -> b) -> a -> b
$ String -> Term -> UnquoteError
NonCanonical String
"meta variable" Term
t

instance Unquote a => Unquote (Dom a) where
  unquote :: Term -> UnquoteM (Dom a)
unquote Term
t = Arg a -> Dom a
forall a. Arg a -> Dom a
domFromArg (Arg a -> Dom a)
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     (Arg a)
-> UnquoteM (Dom a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     (Arg a)
forall a. Unquote a => Term -> UnquoteM a
unquote Term
t

instance Unquote R.Sort where
  unquote :: Term -> UnquoteM Sort
unquote Term
t = do
    Term
t <- Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
reduceQuotedTerm Term
t
    case Term
t of
      Con ConHead
c ConInfo
_ [] ->
        [(UnquoteM Bool, UnquoteM Sort)] -> UnquoteM Sort -> UnquoteM Sort
forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
choice
          [(ConHead
c ConHead -> TCMT IO Term -> UnquoteM Bool
`isCon` TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaSortUnsupported, Sort -> UnquoteM Sort
forall (m :: * -> *) a. Monad m => a -> m a
return Sort
R.UnknownS)]
          UnquoteM Sort
forall a. HasCallStack => a
__IMPOSSIBLE__
      Con ConHead
c ConInfo
_ Elims
es | Just [Arg Term
u] <- Elims -> Maybe [Arg Term]
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es ->
        [(UnquoteM Bool, UnquoteM Sort)] -> UnquoteM Sort -> UnquoteM Sort
forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
choice
          [(ConHead
c ConHead -> TCMT IO Term -> UnquoteM Bool
`isCon` TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaSortSet, Type -> Sort
R.SetS (Type -> Sort)
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Type
-> UnquoteM Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Arg Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Type
forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
u)
          ,(ConHead
c ConHead -> TCMT IO Term -> UnquoteM Bool
`isCon` TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaSortLit, Integer -> Sort
R.LitS (Integer -> Sort) -> UnquoteM Integer -> UnquoteM Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Arg Term -> UnquoteM Integer
forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
u)]
          UnquoteM Sort
forall a. HasCallStack => a
__IMPOSSIBLE__
      Con ConHead
c ConInfo
_ Elims
_ -> UnquoteM Sort
forall a. HasCallStack => a
__IMPOSSIBLE__
      Term
_ -> UnquoteError -> UnquoteM Sort
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (UnquoteError -> UnquoteM Sort) -> UnquoteError -> UnquoteM Sort
forall a b. (a -> b) -> a -> b
$ String -> Term -> UnquoteError
NonCanonical String
"sort" Term
t

instance Unquote Literal where
  unquote :: Term -> UnquoteM Literal
unquote Term
t = do
    Term
t <- Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
reduceQuotedTerm Term
t
    let litMeta :: Range -> MetaId -> m Literal
litMeta Range
r MetaId
x = do
          AbsolutePath
file <- m AbsolutePath
forall (m :: * -> *). MonadTCEnv m => m AbsolutePath
getCurrentPath
          Literal -> m Literal
forall (m :: * -> *) a. Monad m => a -> m a
return (Literal -> m Literal) -> Literal -> m Literal
forall a b. (a -> b) -> a -> b
$ Range -> AbsolutePath -> MetaId -> Literal
LitMeta Range
r AbsolutePath
file MetaId
x
    case Term
t of
      Con ConHead
c ConInfo
_ Elims
es | Just [Arg Term
x] <- Elims -> Maybe [Arg Term]
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es ->
        [(UnquoteM Bool, UnquoteM Literal)]
-> UnquoteM Literal -> UnquoteM Literal
forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
choice
          [ (ConHead
c ConHead -> TCMT IO Term -> UnquoteM Bool
`isCon` TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaLitNat,    Range -> Integer -> Literal
LitNat    Range
forall a. Range' a
noRange (Integer -> Literal) -> UnquoteM Integer -> UnquoteM Literal
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Arg Term -> UnquoteM Integer
forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
x)
          , (ConHead
c ConHead -> TCMT IO Term -> UnquoteM Bool
`isCon` TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaLitFloat,  Range -> Double -> Literal
LitFloat  Range
forall a. Range' a
noRange (Double -> Literal) -> UnquoteM Double -> UnquoteM Literal
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Arg Term -> UnquoteM Double
forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
x)
          , (ConHead
c ConHead -> TCMT IO Term -> UnquoteM Bool
`isCon` TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaLitChar,   Range -> Char -> Literal
LitChar   Range
forall a. Range' a
noRange (Char -> Literal) -> UnquoteM Char -> UnquoteM Literal
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Arg Term -> UnquoteM Char
forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
x)
          , (ConHead
c ConHead -> TCMT IO Term -> UnquoteM Bool
`isCon` TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaLitString, Range -> String -> Literal
LitString Range
forall a. Range' a
noRange (String -> Literal) -> UnquoteM String -> UnquoteM Literal
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Arg Term -> UnquoteM String
unquoteNString Arg Term
x)
          , (ConHead
c ConHead -> TCMT IO Term -> UnquoteM Bool
`isCon` TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaLitQName,  Range -> QName -> Literal
LitQName  Range
forall a. Range' a
noRange (QName -> Literal) -> UnquoteM QName -> UnquoteM Literal
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Arg Term -> UnquoteM QName
forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
x)
          , (ConHead
c ConHead -> TCMT IO Term -> UnquoteM Bool
`isCon` TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaLitMeta,   Range -> MetaId -> UnquoteM Literal
forall (m :: * -> *). MonadTCEnv m => Range -> MetaId -> m Literal
litMeta   Range
forall a. Range' a
noRange (MetaId -> UnquoteM Literal) -> UnquoteM MetaId -> UnquoteM Literal
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Arg Term -> UnquoteM MetaId
forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
x) ]
          UnquoteM Literal
forall a. HasCallStack => a
__IMPOSSIBLE__
      Con ConHead
c ConInfo
_ Elims
_ -> UnquoteM Literal
forall a. HasCallStack => a
__IMPOSSIBLE__
      Term
_ -> UnquoteError -> UnquoteM Literal
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (UnquoteError -> UnquoteM Literal)
-> UnquoteError -> UnquoteM Literal
forall a b. (a -> b) -> a -> b
$ String -> Term -> UnquoteError
NonCanonical String
"literal" Term
t

instance Unquote R.Term where
  unquote :: Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Type
unquote Term
t = do
    Term
t <- Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
reduceQuotedTerm Term
t
    case Term
t of
      Con ConHead
c ConInfo
_ [] ->
        [(UnquoteM Bool,
  ReaderT
    Context
    (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
    Type)]
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Type
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Type
forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
choice
          [ (ConHead
c ConHead -> TCMT IO Term -> UnquoteM Bool
`isCon` TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTermUnsupported, Type
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
R.Unknown) ]
          ReaderT
  Context
  (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
  Type
forall a. HasCallStack => a
__IMPOSSIBLE__

      Con ConHead
c ConInfo
_ Elims
es | Just [Arg Term
x] <- Elims -> Maybe [Arg Term]
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es ->
        [(UnquoteM Bool,
  ReaderT
    Context
    (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
    Type)]
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Type
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Type
forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
choice
          [ (ConHead
c ConHead -> TCMT IO Term -> UnquoteM Bool
`isCon` TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTermSort,      Sort -> Type
R.Sort      (Sort -> Type)
-> UnquoteM Sort
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Arg Term -> UnquoteM Sort
forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
x)
          , (ConHead
c ConHead -> TCMT IO Term -> UnquoteM Bool
`isCon` TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTermLit,       Literal -> Type
R.Lit       (Literal -> Type)
-> UnquoteM Literal
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Arg Term -> UnquoteM Literal
forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
x) ]
          ReaderT
  Context
  (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
  Type
forall a. HasCallStack => a
__IMPOSSIBLE__

      Con ConHead
c ConInfo
_ Elims
es | Just [Arg Term
x, Arg Term
y] <- Elims -> Maybe [Arg Term]
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es ->
        [(UnquoteM Bool,
  ReaderT
    Context
    (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
    Type)]
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Type
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Type
forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
choice
          [ (ConHead
c ConHead -> TCMT IO Term -> UnquoteM Bool
`isCon` TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTermVar,     Int -> Elims -> Type
R.Var     (Int -> Elims -> Type)
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Int
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     (Elims -> Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer -> Int)
-> UnquoteM Integer
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Arg Term -> UnquoteM Integer
forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
x) ReaderT
  Context
  (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
  (Elims -> Type)
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Elims
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Type
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Arg Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Elims
forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
y)
          , (ConHead
c ConHead -> TCMT IO Term -> UnquoteM Bool
`isCon` TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTermCon,     QName -> Elims -> Type
R.Con     (QName -> Elims -> Type)
-> UnquoteM QName
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     (Elims -> Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (QName -> UnquoteM QName
ensureCon (QName -> UnquoteM QName) -> UnquoteM QName -> UnquoteM QName
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Arg Term -> UnquoteM QName
forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
x) ReaderT
  Context
  (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
  (Elims -> Type)
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Elims
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Type
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Arg Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Elims
forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
y)
          , (ConHead
c ConHead -> TCMT IO Term -> UnquoteM Bool
`isCon` TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTermDef,     QName -> Elims -> Type
R.Def     (QName -> Elims -> Type)
-> UnquoteM QName
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     (Elims -> Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (QName -> UnquoteM QName
ensureDef (QName -> UnquoteM QName) -> UnquoteM QName -> UnquoteM QName
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Arg Term -> UnquoteM QName
forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
x) ReaderT
  Context
  (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
  (Elims -> Type)
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Elims
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Type
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Arg Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Elims
forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
y)
          , (ConHead
c ConHead -> TCMT IO Term -> UnquoteM Bool
`isCon` TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTermMeta,    MetaId -> Elims -> Type
R.Meta    (MetaId -> Elims -> Type)
-> UnquoteM MetaId
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     (Elims -> Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Arg Term -> UnquoteM MetaId
forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
x ReaderT
  Context
  (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
  (Elims -> Type)
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Elims
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Type
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Arg Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Elims
forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
y)
          , (ConHead
c ConHead -> TCMT IO Term -> UnquoteM Bool
`isCon` TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTermLam,     Hiding -> Abs Type -> Type
R.Lam     (Hiding -> Abs Type -> Type)
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Hiding
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     (Abs Type -> Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Arg Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Hiding
forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
x ReaderT
  Context
  (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
  (Abs Type -> Type)
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     (Abs Type)
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Type
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Arg Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     (Abs Type)
forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
y)
          , (ConHead
c ConHead -> TCMT IO Term -> UnquoteM Bool
`isCon` TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTermPi,      Dom Type -> Abs Type -> Type
mkPi      (Dom Type -> Abs Type -> Type)
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     (Dom Type)
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     (Abs Type -> Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Arg Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     (Dom Type)
forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
x ReaderT
  Context
  (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
  (Abs Type -> Type)
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     (Abs Type)
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Type
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Arg Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     (Abs Type)
forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
y)
          , (ConHead
c ConHead -> TCMT IO Term -> UnquoteM Bool
`isCon` TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTermExtLam,  [Clause] -> Elims -> Type
R.ExtLam  ([Clause] -> Elims -> Type)
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     [Clause]
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     (Elims -> Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Arg Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     [Clause]
forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
x ReaderT
  Context
  (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
  (Elims -> Type)
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Elims
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Type
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Arg Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Elims
forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
y) ]
          ReaderT
  Context
  (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
  Type
forall a. HasCallStack => a
__IMPOSSIBLE__
        where
          mkPi :: Dom R.Type -> R.Abs R.Type -> R.Term
          -- TODO: implement Free for reflected syntax so this works again
          --mkPi a (R.Abs "_" b) = R.Pi a (R.Abs x b)
          --  where x | 0 `freeIn` b = pickName (unDom a)
          --          | otherwise    = "_"
          mkPi :: Dom Type -> Abs Type -> Type
mkPi Dom Type
a (R.Abs String
"_" Type
b) = Dom Type -> Abs Type -> Type
R.Pi Dom Type
a (String -> Type -> Abs Type
forall a. String -> a -> Abs a
R.Abs (Type -> String
pickName (Dom Type -> Type
forall t e. Dom' t e -> e
unDom Dom Type
a)) Type
b)
          mkPi Dom Type
a Abs Type
b = Dom Type -> Abs Type -> Type
R.Pi Dom Type
a Abs Type
b

      Con{} -> ReaderT
  Context
  (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
  Type
forall a. HasCallStack => a
__IMPOSSIBLE__
      Lit{} -> ReaderT
  Context
  (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
  Type
forall a. HasCallStack => a
__IMPOSSIBLE__
      Term
_ -> UnquoteError
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Type
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (UnquoteError
 -> ReaderT
      Context
      (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
      Type)
-> UnquoteError
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Type
forall a b. (a -> b) -> a -> b
$ String -> Term -> UnquoteError
NonCanonical String
"term" Term
t

instance Unquote R.Pattern where
  unquote :: Term -> UnquoteM Pattern
unquote Term
t = do
    Term
t <- Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
reduceQuotedTerm Term
t
    case Term
t of
      Con ConHead
c ConInfo
_ [] ->
        [(UnquoteM Bool, UnquoteM Pattern)]
-> UnquoteM Pattern -> UnquoteM Pattern
forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
choice
          [ (ConHead
c ConHead -> TCMT IO Term -> UnquoteM Bool
`isCon` TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaPatAbsurd, Pattern -> UnquoteM Pattern
forall (m :: * -> *) a. Monad m => a -> m a
return Pattern
R.AbsurdP)
          , (ConHead
c ConHead -> TCMT IO Term -> UnquoteM Bool
`isCon` TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaPatDot,    Pattern -> UnquoteM Pattern
forall (m :: * -> *) a. Monad m => a -> m a
return Pattern
R.DotP)
          ] UnquoteM Pattern
forall a. HasCallStack => a
__IMPOSSIBLE__
      Con ConHead
c ConInfo
_ Elims
es | Just [Arg Term
x] <- Elims -> Maybe [Arg Term]
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es ->
        [(UnquoteM Bool, UnquoteM Pattern)]
-> UnquoteM Pattern -> UnquoteM Pattern
forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
choice
          [ (ConHead
c ConHead -> TCMT IO Term -> UnquoteM Bool
`isCon` TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaPatVar,  String -> Pattern
R.VarP  (String -> Pattern) -> UnquoteM String -> UnquoteM Pattern
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Arg Term -> UnquoteM String
unquoteNString Arg Term
x)
          , (ConHead
c ConHead -> TCMT IO Term -> UnquoteM Bool
`isCon` TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaPatProj, QName -> Pattern
R.ProjP (QName -> Pattern) -> UnquoteM QName -> UnquoteM Pattern
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Arg Term -> UnquoteM QName
forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
x)
          , (ConHead
c ConHead -> TCMT IO Term -> UnquoteM Bool
`isCon` TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaPatLit,  Literal -> Pattern
R.LitP  (Literal -> Pattern) -> UnquoteM Literal -> UnquoteM Pattern
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Arg Term -> UnquoteM Literal
forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
x) ]
          UnquoteM Pattern
forall a. HasCallStack => a
__IMPOSSIBLE__
      Con ConHead
c ConInfo
_ Elims
es | Just [Arg Term
x, Arg Term
y] <- Elims -> Maybe [Arg Term]
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es ->
        [(UnquoteM Bool, UnquoteM Pattern)]
-> UnquoteM Pattern -> UnquoteM Pattern
forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
choice
          [ (ConHead
c ConHead -> TCMT IO Term -> UnquoteM Bool
`isCon` TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaPatCon, QName -> [Arg Pattern] -> Pattern
R.ConP (QName -> [Arg Pattern] -> Pattern)
-> UnquoteM QName
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     ([Arg Pattern] -> Pattern)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Arg Term -> UnquoteM QName
forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
x ReaderT
  Context
  (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
  ([Arg Pattern] -> Pattern)
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     [Arg Pattern]
-> UnquoteM Pattern
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Arg Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     [Arg Pattern]
forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
y) ]
          UnquoteM Pattern
forall a. HasCallStack => a
__IMPOSSIBLE__
      Con ConHead
c ConInfo
_ Elims
_ -> UnquoteM Pattern
forall a. HasCallStack => a
__IMPOSSIBLE__
      Term
_ -> UnquoteError -> UnquoteM Pattern
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (UnquoteError -> UnquoteM Pattern)
-> UnquoteError -> UnquoteM Pattern
forall a b. (a -> b) -> a -> b
$ String -> Term -> UnquoteError
NonCanonical String
"pattern" Term
t

instance Unquote R.Clause where
  unquote :: Term -> UnquoteM Clause
unquote Term
t = do
    Term
t <- Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
reduceQuotedTerm Term
t
    case Term
t of
      Con ConHead
c ConInfo
_ Elims
es | Just [Arg Term
x] <- Elims -> Maybe [Arg Term]
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es ->
        [(UnquoteM Bool, UnquoteM Clause)]
-> UnquoteM Clause -> UnquoteM Clause
forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
choice
          [ (ConHead
c ConHead -> TCMT IO Term -> UnquoteM Bool
`isCon` TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaClauseAbsurd, [Arg Pattern] -> Clause
R.AbsurdClause ([Arg Pattern] -> Clause)
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     [Arg Pattern]
-> UnquoteM Clause
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Arg Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     [Arg Pattern]
forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
x) ]
          UnquoteM Clause
forall a. HasCallStack => a
__IMPOSSIBLE__
      Con ConHead
c ConInfo
_ Elims
es | Just [Arg Term
x, Arg Term
y] <- Elims -> Maybe [Arg Term]
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es ->
        [(UnquoteM Bool, UnquoteM Clause)]
-> UnquoteM Clause -> UnquoteM Clause
forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
choice
          [ (ConHead
c ConHead -> TCMT IO Term -> UnquoteM Bool
`isCon` TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaClauseClause, [Arg Pattern] -> Type -> Clause
R.Clause ([Arg Pattern] -> Type -> Clause)
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     [Arg Pattern]
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     (Type -> Clause)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Arg Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     [Arg Pattern]
forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
x ReaderT
  Context
  (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
  (Type -> Clause)
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Type
-> UnquoteM Clause
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Arg Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Type
forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
y) ]
          UnquoteM Clause
forall a. HasCallStack => a
__IMPOSSIBLE__
      Con ConHead
c ConInfo
_ Elims
_ -> UnquoteM Clause
forall a. HasCallStack => a
__IMPOSSIBLE__
      Term
_ -> UnquoteError -> UnquoteM Clause
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (UnquoteError -> UnquoteM Clause)
-> UnquoteError -> UnquoteM Clause
forall a b. (a -> b) -> a -> b
$ String -> Term -> UnquoteError
NonCanonical String
"clause" Term
t

-- Unquoting TCM computations ---------------------------------------------

-- | Argument should be a term of type @Term → TCM A@ for some A. Returns the
--   resulting term of type @A@. The second argument is the term for the hole,
--   which will typically be a metavariable. This is passed to the computation
--   (quoted).
unquoteTCM :: I.Term -> I.Term -> UnquoteM I.Term
unquoteTCM :: Term
-> Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
unquoteTCM Term
m Term
hole = do
  Term
qhole <- TCMT IO Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCMT IO Term
 -> ReaderT
      Context
      (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
      Term)
-> TCMT IO Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
forall a b. (a -> b) -> a -> b
$ Term -> TCMT IO Term
quoteTerm Term
hole
  Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
evalTCM (Term
m Term -> [Arg Term] -> Term
forall t. Apply t => t -> [Arg Term] -> t
`apply` [Term -> Arg Term
forall a. a -> Arg a
defaultArg Term
qhole])

evalTCM :: I.Term -> UnquoteM I.Term
evalTCM :: Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
evalTCM Term
v = do
  Term
v <- Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
reduceQuotedTerm Term
v
  TCMT IO ()
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     ()
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCMT IO ()
 -> ReaderT
      Context
      (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
      ())
-> TCMT IO ()
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     ()
forall a b. (a -> b) -> a -> b
$ String -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCM Doc -> m ()
reportSDoc String
"tc.unquote.eval" Int
90 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"evalTCM" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v
  let failEval :: ReaderT
  Context
  (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
  a
failEval = UnquoteError
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (UnquoteError
 -> ReaderT
      Context
      (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
      a)
-> UnquoteError
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     a
forall a b. (a -> b) -> a -> b
$ String -> Term -> UnquoteError
NonCanonical String
"type checking computation" Term
v

  case Term
v of
    I.Def QName
f [] ->
      [(UnquoteM Bool,
  ReaderT
    Context
    (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
    Term)]
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
choice [ (QName
f QName -> TCMT IO Term -> UnquoteM Bool
`isDef` TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMGetContext,       ReaderT
  Context
  (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
  Term
tcGetContext)
             , (QName
f QName -> TCMT IO Term -> UnquoteM Bool
`isDef` TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMCommit,           ReaderT
  Context
  (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
  Term
tcCommit)
             ]
             ReaderT
  Context
  (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
  Term
forall a.
ReaderT
  Context
  (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
  a
failEval
    I.Def QName
f [Elim
u] ->
      [(UnquoteM Bool,
  ReaderT
    Context
    (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
    Term)]
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
choice [ (QName
f QName -> TCMT IO Term -> UnquoteM Bool
`isDef` TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMInferType,                  (Type -> TCMT IO Term)
-> Elim
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
forall a b. Unquote a => (a -> TCM b) -> Elim -> UnquoteM b
tcFun1 Type -> TCMT IO Term
tcInferType                  Elim
u)
             , (QName
f QName -> TCMT IO Term -> UnquoteM Bool
`isDef` TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMNormalise,                  (Type -> TCMT IO Term)
-> Elim
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
forall a b. Unquote a => (a -> TCM b) -> Elim -> UnquoteM b
tcFun1 Type -> TCMT IO Term
tcNormalise                  Elim
u)
             , (QName
f QName -> TCMT IO Term -> UnquoteM Bool
`isDef` TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMReduce,                     (Type -> TCMT IO Term)
-> Elim
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
forall a b. Unquote a => (a -> TCM b) -> Elim -> UnquoteM b
tcFun1 Type -> TCMT IO Term
tcReduce                     Elim
u)
             , (QName
f QName -> TCMT IO Term -> UnquoteM Bool
`isDef` TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMGetType,                    (QName -> TCMT IO Term)
-> Elim
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
forall a b. Unquote a => (a -> TCM b) -> Elim -> UnquoteM b
tcFun1 QName -> TCMT IO Term
tcGetType                    Elim
u)
             , (QName
f QName -> TCMT IO Term -> UnquoteM Bool
`isDef` TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMGetDefinition,              (QName -> TCMT IO Term)
-> Elim
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
forall a b. Unquote a => (a -> TCM b) -> Elim -> UnquoteM b
tcFun1 QName -> TCMT IO Term
tcGetDefinition              Elim
u)
             , (QName
f QName -> TCMT IO Term -> UnquoteM Bool
`isDef` TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMIsMacro,                    (QName -> TCMT IO Term)
-> Elim
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
forall a b. Unquote a => (a -> TCM b) -> Elim -> UnquoteM b
tcFun1 QName -> TCMT IO Term
tcIsMacro                    Elim
u)
             , (QName
f QName -> TCMT IO Term -> UnquoteM Bool
`isDef` TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMFreshName,                  (Str -> TCMT IO Term)
-> Elim
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
forall a b. Unquote a => (a -> TCM b) -> Elim -> UnquoteM b
tcFun1 Str -> TCMT IO Term
tcFreshName                  Elim
u)
             ]
             ReaderT
  Context
  (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
  Term
forall a.
ReaderT
  Context
  (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
  a
failEval
    I.Def QName
f [Elim
u, Elim
v] ->
      [(UnquoteM Bool,
  ReaderT
    Context
    (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
    Term)]
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
choice [ (QName
f QName -> TCMT IO Term -> UnquoteM Bool
`isDef` TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMUnify,      (Type -> Type -> TCMT IO Term)
-> Elim
-> Elim
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
forall a b c.
(Unquote a, Unquote b) =>
(a -> b -> TCM c) -> Elim -> Elim -> UnquoteM c
tcFun2 Type -> Type -> TCMT IO Term
tcUnify      Elim
u Elim
v)
             , (QName
f QName -> TCMT IO Term -> UnquoteM Bool
`isDef` TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMCheckType,  (Type -> Type -> TCMT IO Term)
-> Elim
-> Elim
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
forall a b c.
(Unquote a, Unquote b) =>
(a -> b -> TCM c) -> Elim -> Elim -> UnquoteM c
tcFun2 Type -> Type -> TCMT IO Term
tcCheckType  Elim
u Elim
v)
             , (QName
f QName -> TCMT IO Term -> UnquoteM Bool
`isDef` TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMDeclareDef, (Arg QName
 -> Type
 -> ReaderT
      Context
      (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
      Term)
-> Elim
-> Elim
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
forall a b c.
(Unquote a, Unquote b) =>
(a -> b -> UnquoteM c) -> Elim -> Elim -> UnquoteM c
uqFun2 Arg QName
-> Type
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
tcDeclareDef Elim
u Elim
v)
             , (QName
f QName -> TCMT IO Term -> UnquoteM Bool
`isDef` TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMDeclarePostulate, (Arg QName
 -> Type
 -> ReaderT
      Context
      (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
      Term)
-> Elim
-> Elim
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
forall a b c.
(Unquote a, Unquote b) =>
(a -> b -> UnquoteM c) -> Elim -> Elim -> UnquoteM c
uqFun2 Arg QName
-> Type
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
tcDeclarePostulate Elim
u Elim
v)
             , (QName
f QName -> TCMT IO Term -> UnquoteM Bool
`isDef` TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMDefineFun,  (QName
 -> [Clause]
 -> ReaderT
      Context
      (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
      Term)
-> Elim
-> Elim
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
forall a b c.
(Unquote a, Unquote b) =>
(a -> b -> UnquoteM c) -> Elim -> Elim -> UnquoteM c
uqFun2 QName
-> [Clause]
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
tcDefineFun  Elim
u Elim
v) ]
             ReaderT
  Context
  (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
  Term
forall a.
ReaderT
  Context
  (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
  a
failEval
    I.Def QName
f [Elim
l, Elim
a, Elim
u] ->
      [(UnquoteM Bool,
  ReaderT
    Context
    (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
    Term)]
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
choice [ (QName
f QName -> TCMT IO Term -> UnquoteM Bool
`isDef` TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMReturn,      Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Elim -> Term
forall c. Elim' c -> c
unElim Elim
u))
             , (QName
f QName -> TCMT IO Term -> UnquoteM Bool
`isDef` TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMTypeError,   ([ErrorPart] -> TCMT IO Term)
-> Elim
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
forall a b. Unquote a => (a -> TCM b) -> Elim -> UnquoteM b
tcFun1 [ErrorPart] -> TCMT IO Term
forall a. [ErrorPart] -> TCM a
tcTypeError   Elim
u)
             , (QName
f QName -> TCMT IO Term -> UnquoteM Bool
`isDef` TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMQuoteTerm,   Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
tcQuoteTerm (Elim -> Term
forall c. Elim' c -> c
unElim Elim
u))
             , (QName
f QName -> TCMT IO Term -> UnquoteM Bool
`isDef` TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMUnquoteTerm, (Type -> TCMT IO Term)
-> Elim
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
forall a b. Unquote a => (a -> TCM b) -> Elim -> UnquoteM b
tcFun1 (Type -> Type -> TCMT IO Term
tcUnquoteTerm (Term -> Term -> Type
forall t a. t -> a -> Type'' t a
mkT (Elim -> Term
forall c. Elim' c -> c
unElim Elim
l) (Elim -> Term
forall c. Elim' c -> c
unElim Elim
a))) Elim
u)
             , (QName
f QName -> TCMT IO Term -> UnquoteM Bool
`isDef` TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMBlockOnMeta, (MetaId
 -> ReaderT
      Context
      (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
      Term)
-> Elim
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
forall a b. Unquote a => (a -> UnquoteM b) -> Elim -> UnquoteM b
uqFun1 MetaId
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
tcBlockOnMeta Elim
u)
             , (QName
f QName -> TCMT IO Term -> UnquoteM Bool
`isDef` TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMDebugPrint,  (Str -> Integer -> [ErrorPart] -> TCMT IO Term)
-> Elim
-> Elim
-> Elim
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
forall a b c d.
(Unquote a, Unquote b, Unquote c) =>
(a -> b -> c -> TCM d) -> Elim -> Elim -> Elim -> UnquoteM d
tcFun3 Str -> Integer -> [ErrorPart] -> TCMT IO Term
tcDebugPrint Elim
l Elim
a Elim
u)
             , (QName
f QName -> TCMT IO Term -> UnquoteM Bool
`isDef` TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMNoConstraints, Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
tcNoConstraints (Elim -> Term
forall c. Elim' c -> c
unElim Elim
u))
             , (QName
f QName -> TCMT IO Term -> UnquoteM Bool
`isDef` TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMRunSpeculative, Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
tcRunSpeculative (Elim -> Term
forall c. Elim' c -> c
unElim Elim
u))
             ]
             ReaderT
  Context
  (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
  Term
forall a.
ReaderT
  Context
  (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
  a
failEval
    I.Def QName
f [Elim
_, Elim
_, Elim
u, Elim
v] ->
      [(UnquoteM Bool,
  ReaderT
    Context
    (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
    Term)]
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
choice [ (QName
f QName -> TCMT IO Term -> UnquoteM Bool
`isDef` TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMCatchError,    Term
-> Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
tcCatchError    (Elim -> Term
forall c. Elim' c -> c
unElim Elim
u) (Elim -> Term
forall c. Elim' c -> c
unElim Elim
v))
             , (QName
f QName -> TCMT IO Term -> UnquoteM Bool
`isDef` TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMWithNormalisation, Term
-> Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
tcWithNormalisation (Elim -> Term
forall c. Elim' c -> c
unElim Elim
u) (Elim -> Term
forall c. Elim' c -> c
unElim Elim
v))
             , (QName
f QName -> TCMT IO Term -> UnquoteM Bool
`isDef` TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMExtendContext, Term
-> Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
tcExtendContext (Elim -> Term
forall c. Elim' c -> c
unElim Elim
u) (Elim -> Term
forall c. Elim' c -> c
unElim Elim
v))
             , (QName
f QName -> TCMT IO Term -> UnquoteM Bool
`isDef` TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMInContext,     Term
-> Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
tcInContext     (Elim -> Term
forall c. Elim' c -> c
unElim Elim
u) (Elim -> Term
forall c. Elim' c -> c
unElim Elim
v)) ]
             ReaderT
  Context
  (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
  Term
forall a.
ReaderT
  Context
  (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
  a
failEval
    I.Def QName
f [Elim
_, Elim
_, Elim
_, Elim
_, Elim
m, Elim
k] ->
      [(UnquoteM Bool,
  ReaderT
    Context
    (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
    Term)]
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
choice [ (QName
f QName -> TCMT IO Term -> UnquoteM Bool
`isDef` TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMBind, Term
-> Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
tcBind (Elim -> Term
forall c. Elim' c -> c
unElim Elim
m) (Elim -> Term
forall c. Elim' c -> c
unElim Elim
k)) ]
             ReaderT
  Context
  (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
  Term
forall a.
ReaderT
  Context
  (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
  a
failEval
    Term
_ -> ReaderT
  Context
  (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
  Term
forall a.
ReaderT
  Context
  (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
  a
failEval
  where
    unElim :: Elim' c -> c
unElim = Arg c -> c
forall e. Arg e -> e
unArg (Arg c -> c) -> (Elim' c -> Arg c) -> Elim' c -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg c -> Maybe (Arg c) -> Arg c
forall a. a -> Maybe a -> a
fromMaybe Arg c
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe (Arg c) -> Arg c)
-> (Elim' c -> Maybe (Arg c)) -> Elim' c -> Arg c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Elim' c -> Maybe (Arg c)
forall a. Elim' a -> Maybe (Arg a)
isApplyElim
    tcBind :: Term
-> Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
tcBind Term
m Term
k = do Term
v <- Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
evalTCM Term
m
                    Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
evalTCM (Term
k Term -> [Arg Term] -> Term
forall t. Apply t => t -> [Arg Term] -> t
`apply` [Term -> Arg Term
forall a. a -> Arg a
defaultArg Term
v])

    process :: (InstantiateFull a, Normalise a) => a -> TCM a
    process :: a -> TCM a
process a
v = do
      Bool
norm <- Lens' Bool TCEnv -> TCMT IO Bool
forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
viewTC Lens' Bool TCEnv
eUnquoteNormalise
      if Bool
norm then a -> TCM a
forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
normalise a
v else a -> TCM a
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull a
v

    mkT :: t -> a -> Type'' t a
mkT t
l a
a = Sort' t -> a -> Type'' t a
forall t a. Sort' t -> a -> Type'' t a
El Sort' t
s a
a
      where s :: Sort' t
s = Level' t -> Sort' t
forall t. Level' t -> Sort' t
Type (Level' t -> Sort' t) -> Level' t -> Sort' t
forall a b. (a -> b) -> a -> b
$ Integer -> [PlusLevel' t] -> Level' t
forall t. Integer -> [PlusLevel' t] -> Level' t
Max Integer
0 [Integer -> LevelAtom' t -> PlusLevel' t
forall t. Integer -> LevelAtom' t -> PlusLevel' t
Plus Integer
0 (LevelAtom' t -> PlusLevel' t) -> LevelAtom' t -> PlusLevel' t
forall a b. (a -> b) -> a -> b
$ t -> LevelAtom' t
forall t. t -> LevelAtom' t
UnreducedLevel t
l]

    -- Don't catch Unquote errors!
    tcCatchError :: Term -> Term -> UnquoteM Term
    tcCatchError :: Term
-> Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
tcCatchError Term
m Term
h =
      (TCM (UnquoteRes Term)
 -> TCM (UnquoteRes Term) -> TCM (UnquoteRes Term))
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
forall a b c.
(TCM (UnquoteRes a) -> TCM (UnquoteRes b) -> TCM (UnquoteRes c))
-> UnquoteM a -> UnquoteM b -> UnquoteM c
liftU2 (\ TCM (UnquoteRes Term)
m1 TCM (UnquoteRes Term)
m2 -> TCM (UnquoteRes Term)
m1 TCM (UnquoteRes Term)
-> (TCErr -> TCM (UnquoteRes Term)) -> TCM (UnquoteRes Term)
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \ TCErr
_ -> TCM (UnquoteRes Term)
m2) (Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
evalTCM Term
m) (Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
evalTCM Term
h)

    tcWithNormalisation :: Term -> Term -> UnquoteM Term
    tcWithNormalisation :: Term
-> Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
tcWithNormalisation Term
b Term
m = do
      Bool
v <- Term -> UnquoteM Bool
forall a. Unquote a => Term -> UnquoteM a
unquote Term
b
      (TCM (UnquoteRes Term) -> TCM (UnquoteRes Term))
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
forall a b.
(TCM (UnquoteRes a) -> TCM (UnquoteRes b))
-> UnquoteM a -> UnquoteM b
liftU1 (Lens' Bool TCEnv
-> (Bool -> Bool) -> TCM (UnquoteRes Term) -> TCM (UnquoteRes Term)
forall (m :: * -> *) a b.
MonadTCEnv m =>
Lens' a TCEnv -> (a -> a) -> m b -> m b
locallyTC Lens' Bool TCEnv
eUnquoteNormalise ((Bool -> Bool) -> TCM (UnquoteRes Term) -> TCM (UnquoteRes Term))
-> (Bool -> Bool) -> TCM (UnquoteRes Term) -> TCM (UnquoteRes Term)
forall a b. (a -> b) -> a -> b
$ Bool -> Bool -> Bool
forall a b. a -> b -> a
const Bool
v) (Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
evalTCM Term
m)

    uqFun1 :: Unquote a => (a -> UnquoteM b) -> Elim -> UnquoteM b
    uqFun1 :: (a -> UnquoteM b) -> Elim -> UnquoteM b
uqFun1 a -> UnquoteM b
fun Elim
a = do
      a
a <- Term -> UnquoteM a
forall a. Unquote a => Term -> UnquoteM a
unquote (Elim -> Term
forall c. Elim' c -> c
unElim Elim
a)
      a -> UnquoteM b
fun a
a

    tcFun1 :: Unquote a => (a -> TCM b) -> Elim -> UnquoteM b
    tcFun1 :: (a -> TCM b) -> Elim -> UnquoteM b
tcFun1 a -> TCM b
fun = (a -> UnquoteM b) -> Elim -> UnquoteM b
forall a b. Unquote a => (a -> UnquoteM b) -> Elim -> UnquoteM b
uqFun1 (TCM b -> UnquoteM b
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM b -> UnquoteM b) -> (a -> TCM b) -> a -> UnquoteM b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> TCM b
fun)

    uqFun2 :: (Unquote a, Unquote b) => (a -> b -> UnquoteM c) -> Elim -> Elim -> UnquoteM c
    uqFun2 :: (a -> b -> UnquoteM c) -> Elim -> Elim -> UnquoteM c
uqFun2 a -> b -> UnquoteM c
fun Elim
a Elim
b = do
      a
a <- Term -> UnquoteM a
forall a. Unquote a => Term -> UnquoteM a
unquote (Elim -> Term
forall c. Elim' c -> c
unElim Elim
a)
      b
b <- Term -> UnquoteM b
forall a. Unquote a => Term -> UnquoteM a
unquote (Elim -> Term
forall c. Elim' c -> c
unElim Elim
b)
      a -> b -> UnquoteM c
fun a
a b
b

    uqFun3 :: (Unquote a, Unquote b, Unquote c) => (a -> b -> c -> UnquoteM d) -> Elim -> Elim -> Elim -> UnquoteM d
    uqFun3 :: (a -> b -> c -> UnquoteM d) -> Elim -> Elim -> Elim -> UnquoteM d
uqFun3 a -> b -> c -> UnquoteM d
fun Elim
a Elim
b Elim
c = do
      a
a <- Term -> UnquoteM a
forall a. Unquote a => Term -> UnquoteM a
unquote (Elim -> Term
forall c. Elim' c -> c
unElim Elim
a)
      b
b <- Term -> UnquoteM b
forall a. Unquote a => Term -> UnquoteM a
unquote (Elim -> Term
forall c. Elim' c -> c
unElim Elim
b)
      c
c <- Term -> UnquoteM c
forall a. Unquote a => Term -> UnquoteM a
unquote (Elim -> Term
forall c. Elim' c -> c
unElim Elim
c)
      a -> b -> c -> UnquoteM d
fun a
a b
b c
c

    tcFun2 :: (Unquote a, Unquote b) => (a -> b -> TCM c) -> Elim -> Elim -> UnquoteM c
    tcFun2 :: (a -> b -> TCM c) -> Elim -> Elim -> UnquoteM c
tcFun2 a -> b -> TCM c
fun = (a -> b -> UnquoteM c) -> Elim -> Elim -> UnquoteM c
forall a b c.
(Unquote a, Unquote b) =>
(a -> b -> UnquoteM c) -> Elim -> Elim -> UnquoteM c
uqFun2 (\ a
x b
y -> TCM c -> UnquoteM c
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (a -> b -> TCM c
fun a
x b
y))

    tcFun3 :: (Unquote a, Unquote b, Unquote c) => (a -> b -> c -> TCM d) -> Elim -> Elim -> Elim -> UnquoteM d
    tcFun3 :: (a -> b -> c -> TCM d) -> Elim -> Elim -> Elim -> UnquoteM d
tcFun3 a -> b -> c -> TCM d
fun = (a -> b -> c -> UnquoteM d) -> Elim -> Elim -> Elim -> UnquoteM d
forall a b c d.
(Unquote a, Unquote b, Unquote c) =>
(a -> b -> c -> UnquoteM d) -> Elim -> Elim -> Elim -> UnquoteM d
uqFun3 (\ a
x b
y c
z -> TCM d -> UnquoteM d
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (a -> b -> c -> TCM d
fun a
x b
y c
z))

    tcFreshName :: Str -> TCM Term
    tcFreshName :: Str -> TCMT IO Term
tcFreshName Str
s = do
      ModuleName
m <- TCMT IO ModuleName
forall (m :: * -> *). MonadTCEnv m => m ModuleName
currentModule
      QName -> Term
quoteName (QName -> Term) -> (Name -> QName) -> Name -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleName -> Name -> QName
qualify ModuleName
m (Name -> Term) -> TCMT IO Name -> TCMT IO Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> TCMT IO Name
forall a (m :: * -> *).
(FreshName a, MonadFresh NameId m) =>
a -> m Name
freshName_ (Str -> String
unStr Str
s)

    tcUnify :: R.Term -> R.Term -> TCM Term
    tcUnify :: Type -> Type -> TCMT IO Term
tcUnify Type
u Type
v = do
      (Term
u, Type
a) <- Expr -> TCM (Term, Type)
inferExpr        (Expr -> TCM (Term, Type)) -> TCM Expr -> TCM (Term, Type)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Type -> TCM Expr
forall r a (m :: * -> *).
(ToAbstract r a, MonadFresh NameId m, MonadError TCErr m,
 MonadTCEnv m, ReadTCState m, HasOptions m, HasConstInfo m) =>
r -> m a
toAbstract_ Type
u
      Term
v      <- (Expr -> Type -> TCMT IO Term) -> Type -> Expr -> TCMT IO Term
forall a b c. (a -> b -> c) -> b -> a -> c
flip Expr -> Type -> TCMT IO Term
checkExpr Type
a (Expr -> TCMT IO Term) -> TCM Expr -> TCMT IO Term
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Type -> TCM Expr
forall r a (m :: * -> *).
(ToAbstract r a, MonadFresh NameId m, MonadError TCErr m,
 MonadTCEnv m, ReadTCState m, HasOptions m, HasConstInfo m) =>
r -> m a
toAbstract_ Type
v
      Type -> Term -> Term -> TCMT IO ()
forall (m :: * -> *).
MonadConversion m =>
Type -> Term -> Term -> m ()
equalTerm Type
a Term
u Term
v
      TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primUnitUnit

    tcBlockOnMeta :: MetaId -> UnquoteM Term
    tcBlockOnMeta :: MetaId
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
tcBlockOnMeta MetaId
x = do
      TCState
s <- (UnquoteState -> TCState)
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     TCState
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets UnquoteState -> TCState
forall a b. (a, b) -> b
snd
      UnquoteError
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCState -> MetaId -> UnquoteError
BlockedOnMeta TCState
s MetaId
x)

    tcCommit :: UnquoteM Term
    tcCommit :: ReaderT
  Context
  (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
  Term
tcCommit = do
      Dirty
dirty <- (UnquoteState -> Dirty)
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Dirty
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets UnquoteState -> Dirty
forall a b. (a, b) -> a
fst
      Bool
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     ()
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Dirty
dirty Dirty -> Dirty -> Bool
forall a. Eq a => a -> a -> Bool
== Dirty
Dirty) (ReaderT
   Context
   (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
   ()
 -> ReaderT
      Context
      (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
      ())
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     ()
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     ()
forall a b. (a -> b) -> a -> b
$
        TCMT IO ()
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     ()
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCMT IO ()
 -> ReaderT
      Context
      (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
      ())
-> TCMT IO ()
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     ()
forall a b. (a -> b) -> a -> b
$ TypeError -> TCMT IO ()
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO ()) -> TypeError -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ String -> TypeError
GenericError String
"Cannot use commitTC after declaring new definitions."
      TCState
s <- ReaderT
  Context
  (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
  TCState
forall (m :: * -> *). MonadTCState m => m TCState
getTC
      (UnquoteState -> UnquoteState)
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((TCState -> TCState) -> UnquoteState -> UnquoteState
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second ((TCState -> TCState) -> UnquoteState -> UnquoteState)
-> (TCState -> TCState) -> UnquoteState -> UnquoteState
forall a b. (a -> b) -> a -> b
$ TCState -> TCState -> TCState
forall a b. a -> b -> a
const TCState
s)
      TCMT IO Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primUnitUnit

    tcTypeError :: [ErrorPart] -> TCM a
    tcTypeError :: [ErrorPart] -> TCM a
tcTypeError [ErrorPart]
err = TypeError -> TCM a
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> TCM a) -> (Doc -> TypeError) -> Doc -> TCM a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError (Doc -> TCM a) -> TCM Doc -> TCM a
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ((ErrorPart -> TCM Doc) -> [ErrorPart] -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map ErrorPart -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [ErrorPart]
err)

    tcDebugPrint :: Str -> Integer -> [ErrorPart] -> TCM Term
    tcDebugPrint :: Str -> Integer -> [ErrorPart] -> TCMT IO Term
tcDebugPrint (Str String
s) Integer
n [ErrorPart]
msg = do
      String -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCM Doc -> m ()
reportSDoc String
s (Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
n) (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
fsep ((ErrorPart -> TCM Doc) -> [ErrorPart] -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map ErrorPart -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [ErrorPart]
msg)
      TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primUnitUnit

    tcNoConstraints :: Term -> UnquoteM Term
    tcNoConstraints :: Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
tcNoConstraints Term
m = (TCM (UnquoteRes Term) -> TCM (UnquoteRes Term))
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
forall a b.
(TCM (UnquoteRes a) -> TCM (UnquoteRes b))
-> UnquoteM a -> UnquoteM b
liftU1 TCM (UnquoteRes Term) -> TCM (UnquoteRes Term)
forall (m :: * -> *) a.
(MonadConstraint m, MonadWarning m, MonadError TCErr m,
 MonadFresh ProblemId m) =>
m a -> m a
noConstraints (Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
evalTCM Term
m)

    tcInferType :: R.Term -> TCM Term
    tcInferType :: Type -> TCMT IO Term
tcInferType Type
v = do
      (Term
_, Type
a) <- Expr -> TCM (Term, Type)
inferExpr (Expr -> TCM (Term, Type)) -> TCM Expr -> TCM (Term, Type)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Type -> TCM Expr
forall r a (m :: * -> *).
(ToAbstract r a, MonadFresh NameId m, MonadError TCErr m,
 MonadTCEnv m, ReadTCState m, HasOptions m, HasConstInfo m) =>
r -> m a
toAbstract_ Type
v
      Type -> TCMT IO Term
quoteType (Type -> TCMT IO Term) -> TCM Type -> TCMT IO Term
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Type -> TCM Type
forall a. (InstantiateFull a, Normalise a) => a -> TCM a
process Type
a

    tcCheckType :: R.Term -> R.Type -> TCM Term
    tcCheckType :: Type -> Type -> TCMT IO Term
tcCheckType Type
v Type
a = do
      Type
a <- Expr -> TCM Type
isType_ (Expr -> TCM Type) -> TCM Expr -> TCM Type
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Type -> TCM Expr
forall r a (m :: * -> *).
(ToAbstract r a, MonadFresh NameId m, MonadError TCErr m,
 MonadTCEnv m, ReadTCState m, HasOptions m, HasConstInfo m) =>
r -> m a
toAbstract_ Type
a
      Expr
e <- Type -> TCM Expr
forall r a (m :: * -> *).
(ToAbstract r a, MonadFresh NameId m, MonadError TCErr m,
 MonadTCEnv m, ReadTCState m, HasOptions m, HasConstInfo m) =>
r -> m a
toAbstract_ Type
v
      Term
v <- Expr -> Type -> TCMT IO Term
checkExpr Expr
e Type
a
      Term -> TCMT IO Term
quoteTerm (Term -> TCMT IO Term) -> TCMT IO Term -> TCMT IO Term
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Term -> TCMT IO Term
forall a. (InstantiateFull a, Normalise a) => a -> TCM a
process Term
v

    tcQuoteTerm :: Term -> UnquoteM Term
    tcQuoteTerm :: Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
tcQuoteTerm Term
v = TCMT IO Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCMT IO Term
 -> ReaderT
      Context
      (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
      Term)
-> TCMT IO Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
forall a b. (a -> b) -> a -> b
$ Term -> TCMT IO Term
quoteTerm (Term -> TCMT IO Term) -> TCMT IO Term -> TCMT IO Term
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Term -> TCMT IO Term
forall a. (InstantiateFull a, Normalise a) => a -> TCM a
process Term
v

    tcUnquoteTerm :: Type -> R.Term -> TCM Term
    tcUnquoteTerm :: Type -> Type -> TCMT IO Term
tcUnquoteTerm Type
a Type
v = do
      Expr
e <- Type -> TCM Expr
forall r a (m :: * -> *).
(ToAbstract r a, MonadFresh NameId m, MonadError TCErr m,
 MonadTCEnv m, ReadTCState m, HasOptions m, HasConstInfo m) =>
r -> m a
toAbstract_ Type
v
      Expr -> Type -> TCMT IO Term
checkExpr Expr
e Type
a

    tcNormalise :: R.Term -> TCM Term
    tcNormalise :: Type -> TCMT IO Term
tcNormalise Type
v = do
      (Term
v, Type
_) <- Expr -> TCM (Term, Type)
inferExpr (Expr -> TCM (Term, Type)) -> TCM Expr -> TCM (Term, Type)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Type -> TCM Expr
forall r a (m :: * -> *).
(ToAbstract r a, MonadFresh NameId m, MonadError TCErr m,
 MonadTCEnv m, ReadTCState m, HasOptions m, HasConstInfo m) =>
r -> m a
toAbstract_ Type
v
      Term -> TCMT IO Term
quoteTerm (Term -> TCMT IO Term) -> TCMT IO Term -> TCMT IO Term
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Term -> TCMT IO Term
forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
normalise Term
v

    tcReduce :: R.Term -> TCM Term
    tcReduce :: Type -> TCMT IO Term
tcReduce Type
v = do
      (Term
v, Type
_) <- Expr -> TCM (Term, Type)
inferExpr (Expr -> TCM (Term, Type)) -> TCM Expr -> TCM (Term, Type)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Type -> TCM Expr
forall r a (m :: * -> *).
(ToAbstract r a, MonadFresh NameId m, MonadError TCErr m,
 MonadTCEnv m, ReadTCState m, HasOptions m, HasConstInfo m) =>
r -> m a
toAbstract_ Type
v
      Term -> TCMT IO Term
quoteTerm (Term -> TCMT IO Term) -> TCMT IO Term -> TCMT IO Term
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Term -> TCMT IO Term
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (Term -> TCMT IO Term) -> TCMT IO Term -> TCMT IO Term
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Term -> TCMT IO Term
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull Term
v

    tcGetContext :: UnquoteM Term
    tcGetContext :: ReaderT
  Context
  (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
  Term
tcGetContext = TCMT IO Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCMT IO Term
 -> ReaderT
      Context
      (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
      Term)
-> TCMT IO Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
forall a b. (a -> b) -> a -> b
$ do
      [Dom' Term Type]
as <- (Dom' Term (Name, Type) -> Dom' Term Type)
-> Context -> [Dom' Term Type]
forall a b. (a -> b) -> [a] -> [b]
map (((Name, Type) -> Type) -> Dom' Term (Name, Type) -> Dom' Term Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Name, Type) -> Type
forall a b. (a, b) -> b
snd) (Context -> [Dom' Term Type])
-> TCMT IO Context -> TCMT IO [Dom' Term Type]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO Context
forall (m :: * -> *). MonadTCEnv m => m Context
getContext
      [Dom' Term Type]
as <- [Dom' Term Type] -> TCMT IO [Dom' Term Type]
forall (m :: * -> *) a.
(MonadTCEnv m, HasConstInfo m, HasOptions m, TermLike a) =>
a -> m a
etaContract ([Dom' Term Type] -> TCMT IO [Dom' Term Type])
-> TCMT IO [Dom' Term Type] -> TCMT IO [Dom' Term Type]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [Dom' Term Type] -> TCMT IO [Dom' Term Type]
forall a. (InstantiateFull a, Normalise a) => a -> TCM a
process [Dom' Term Type]
as
      TCM ([Term] -> Term)
buildList TCM ([Term] -> Term) -> TCMT IO [Term] -> TCMT IO Term
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Dom' Term Type -> TCMT IO Term)
-> [Dom' Term Type] -> TCMT IO [Term]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Dom' Term Type -> TCMT IO Term
quoteDom [Dom' Term Type]
as

    extendCxt :: Arg R.Type -> UnquoteM a -> UnquoteM a
    extendCxt :: Arg Type -> UnquoteM a -> UnquoteM a
extendCxt Arg Type
a UnquoteM a
m = do
      Arg Type
a <- TCM (Arg Type)
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     (Arg Type)
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM (Arg Type)
 -> ReaderT
      Context
      (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
      (Arg Type))
-> TCM (Arg Type)
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     (Arg Type)
forall a b. (a -> b) -> a -> b
$ (Type -> TCM Type) -> Arg Type -> TCM (Arg Type)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (Expr -> TCM Type
isType_ (Expr -> TCM Type) -> (Type -> TCM Expr) -> Type -> TCM Type
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Type -> TCM Expr
forall r a (m :: * -> *).
(ToAbstract r a, MonadFresh NameId m, MonadError TCErr m,
 MonadTCEnv m, ReadTCState m, HasOptions m, HasConstInfo m) =>
r -> m a
toAbstract_) Arg Type
a
      (TCM (UnquoteRes a) -> TCM (UnquoteRes a))
-> UnquoteM a -> UnquoteM a
forall a b.
(TCM (UnquoteRes a) -> TCM (UnquoteRes b))
-> UnquoteM a -> UnquoteM b
liftU1 (Dom' Term Type -> TCM (UnquoteRes a) -> TCM (UnquoteRes a)
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (Arg Type -> Dom' Term Type
forall a. Arg a -> Dom a
domFromArg Arg Type
a :: Dom Type)) UnquoteM a
m

    tcExtendContext :: Term -> Term -> UnquoteM Term
    tcExtendContext :: Term
-> Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
tcExtendContext Term
a Term
m = do
      Arg Type
a <- Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     (Arg Type)
forall a. Unquote a => Term -> UnquoteM a
unquote Term
a
      Empty -> Term -> Term
forall t a. Subst t a => Empty -> a -> a
strengthen Empty
forall a. HasCallStack => a
__UNREACHABLE__ (Term -> Term)
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Arg Type
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
forall a. Arg Type -> UnquoteM a -> UnquoteM a
extendCxt Arg Type
a (Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
evalTCM (Term
 -> ReaderT
      Context
      (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
      Term)
-> Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
forall a b. (a -> b) -> a -> b
$ Int -> Term -> Term
forall t a. Subst t a => Int -> a -> a
raise Int
1 Term
m)

    tcInContext :: Term -> Term -> UnquoteM Term
    tcInContext :: Term
-> Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
tcInContext Term
c Term
m = do
      [Arg Type]
c <- Term -> UnquoteM [Arg Type]
forall a. Unquote a => Term -> UnquoteM a
unquote Term
c
      (TCM (UnquoteRes Term) -> TCM (UnquoteRes Term))
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
forall a b.
(TCM (UnquoteRes a) -> TCM (UnquoteRes b))
-> UnquoteM a -> UnquoteM b
liftU1 TCM (UnquoteRes Term) -> TCM (UnquoteRes Term)
forall (m :: * -> *) a. (MonadTCEnv m, ReadTCState m) => m a -> m a
unsafeInTopContext (ReaderT
   Context
   (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
   Term
 -> ReaderT
      Context
      (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
      Term)
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
forall a b. (a -> b) -> a -> b
$ [Arg Type]
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
go [Arg Type]
c (Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
evalTCM Term
m)
      where
        go :: [Arg R.Type] -> UnquoteM Term -> UnquoteM Term
        go :: [Arg Type]
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
go []       ReaderT
  Context
  (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
  Term
m = ReaderT
  Context
  (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
  Term
m
        go (Arg Type
a : [Arg Type]
as) ReaderT
  Context
  (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
  Term
m = [Arg Type]
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
go [Arg Type]
as (Arg Type
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
forall a. Arg Type -> UnquoteM a -> UnquoteM a
extendCxt Arg Type
a ReaderT
  Context
  (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
  Term
m)

    constInfo :: QName -> TCM Definition
    constInfo :: QName -> TCM Definition
constInfo QName
x = (SigError -> TCM Definition)
-> (Definition -> TCM Definition)
-> Either SigError Definition
-> TCM Definition
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either SigError -> TCM Definition
forall (m :: * -> *) p a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
p -> m a
err Definition -> TCM Definition
forall (m :: * -> *) a. Monad m => a -> m a
return (Either SigError Definition -> TCM Definition)
-> TCMT IO (Either SigError Definition) -> TCM Definition
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< QName -> TCMT IO (Either SigError Definition)
forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Either SigError Definition)
getConstInfo' QName
x
      where err :: p -> m a
err p
_ = String -> m a
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
String -> m a
genericError (String -> m a) -> String -> m a
forall a b. (a -> b) -> a -> b
$ String
"Unbound name: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ QName -> String
forall a. Pretty a => a -> String
prettyShow QName
x

    tcGetType :: QName -> TCM Term
    tcGetType :: QName -> TCMT IO Term
tcGetType QName
x = Type -> TCMT IO Term
quoteType (Type -> TCMT IO Term)
-> (Definition -> Type) -> Definition -> TCMT IO Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> Type
defType (Definition -> TCMT IO Term) -> TCM Definition -> TCMT IO Term
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< QName -> TCM Definition
constInfo QName
x

    tcIsMacro :: QName -> TCM Term
    tcIsMacro :: QName -> TCMT IO Term
tcIsMacro QName
x = do
      Term
true  <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primTrue
      Term
false <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primFalse
      let qBool :: Bool -> Term
qBool Bool
True  = Term
true
          qBool Bool
False = Term
false
      Bool -> Term
qBool (Bool -> Term) -> (Definition -> Bool) -> Definition -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Defn -> Bool
isMacro (Defn -> Bool) -> (Definition -> Defn) -> Definition -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> Defn
theDef (Definition -> Term) -> TCM Definition -> TCMT IO Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCM Definition
constInfo QName
x

    tcGetDefinition :: QName -> TCM Term
    tcGetDefinition :: QName -> TCMT IO Term
tcGetDefinition QName
x = Definition -> TCMT IO Term
quoteDefn (Definition -> TCMT IO Term) -> TCM Definition -> TCMT IO Term
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< QName -> TCM Definition
constInfo QName
x

    setDirty :: UnquoteM ()
    setDirty :: ReaderT
  Context
  (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
  ()
setDirty = (UnquoteState -> UnquoteState)
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((Dirty -> Dirty) -> UnquoteState -> UnquoteState
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first ((Dirty -> Dirty) -> UnquoteState -> UnquoteState)
-> (Dirty -> Dirty) -> UnquoteState -> UnquoteState
forall a b. (a -> b) -> a -> b
$ Dirty -> Dirty -> Dirty
forall a b. a -> b -> a
const Dirty
Dirty)

    tcDeclareDef :: Arg QName -> R.Type -> UnquoteM Term
    tcDeclareDef :: Arg QName
-> Type
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
tcDeclareDef (Arg ArgInfo
i QName
x) Type
a = ReaderT
  Context
  (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
  Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
forall a. UnquoteM a -> UnquoteM a
inOriginalContext (ReaderT
   Context
   (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
   Term
 -> ReaderT
      Context
      (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
      Term)
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
forall a b. (a -> b) -> a -> b
$ do
      ReaderT
  Context
  (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
  ()
setDirty
      let r :: Relevance
r = ArgInfo -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance ArgInfo
i
      Bool
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     ()
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (ArgInfo -> Bool
forall a. LensHiding a => a -> Bool
hidden ArgInfo
i) (ReaderT
   Context
   (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
   ()
 -> ReaderT
      Context
      (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
      ())
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     ()
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     ()
forall a b. (a -> b) -> a -> b
$ TCMT IO ()
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     ()
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCMT IO ()
 -> ReaderT
      Context
      (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
      ())
-> TCMT IO ()
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     ()
forall a b. (a -> b) -> a -> b
$ TypeError -> TCMT IO ()
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO ())
-> (Doc -> TypeError) -> Doc -> TCMT IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError (Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<
        TCM Doc
"Cannot declare hidden function" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
x
      [QName]
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [QName
x]
      TCMT IO Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCMT IO Term
 -> ReaderT
      Context
      (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
      Term)
-> TCMT IO Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
forall a b. (a -> b) -> a -> b
$ do
        String -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCM Doc -> m ()
reportSDoc String
"tc.unquote.decl" Int
10 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep
          [ TCM Doc
"declare" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
x TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
":"
          , Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Type -> TCM Doc
forall r a (m :: * -> *).
(ToAbstract r a, PrettyTCM a, MonadPretty m, MonadError TCErr m) =>
r -> m Doc
prettyR Type
a
          ]
        Type
a <- Expr -> TCM Type
isType_ (Expr -> TCM Type) -> TCM Expr -> TCM Type
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Type -> TCM Expr
forall r a (m :: * -> *).
(ToAbstract r a, MonadFresh NameId m, MonadError TCErr m,
 MonadTCEnv m, ReadTCState m, HasOptions m, HasConstInfo m) =>
r -> m a
toAbstract_ Type
a
        Bool
alreadyDefined <- Either SigError Definition -> Bool
forall a b. Either a b -> Bool
isRight (Either SigError Definition -> Bool)
-> TCMT IO (Either SigError Definition) -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO (Either SigError Definition)
forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Either SigError Definition)
getConstInfo' QName
x
        Bool -> TCMT IO () -> TCMT IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
alreadyDefined (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ String -> TCMT IO ()
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
String -> m a
genericError (String -> TCMT IO ()) -> String -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ String
"Multiple declarations of " String -> String -> String
forall a. [a] -> [a] -> [a]
++ QName -> String
forall a. Pretty a => a -> String
prettyShow QName
x
        QName -> Definition -> TCMT IO ()
addConstant QName
x (Definition -> TCMT IO ()) -> Definition -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ ArgInfo -> QName -> Type -> Defn -> Definition
defaultDefn ArgInfo
i QName
x Type
a Defn
emptyFunction
        Bool -> TCMT IO () -> TCMT IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (ArgInfo -> Bool
forall a. LensHiding a => a -> Bool
isInstance ArgInfo
i) (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ QName -> Type -> TCMT IO ()
addTypedInstance QName
x Type
a
        TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primUnitUnit

    tcDeclarePostulate :: Arg QName -> R.Type -> UnquoteM Term
    tcDeclarePostulate :: Arg QName
-> Type
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
tcDeclarePostulate (Arg ArgInfo
i QName
x) Type
a = ReaderT
  Context
  (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
  Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
forall a. UnquoteM a -> UnquoteM a
inOriginalContext (ReaderT
   Context
   (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
   Term
 -> ReaderT
      Context
      (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
      Term)
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
forall a b. (a -> b) -> a -> b
$ do
      CommandLineOptions
clo <- ReaderT
  Context
  (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
  CommandLineOptions
forall (m :: * -> *). HasOptions m => m CommandLineOptions
commandLineOptions
      Bool
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     ()
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (CommandLineOptions -> Bool
forall a. LensSafeMode a => a -> Bool
Lens.getSafeMode CommandLineOptions
clo) (ReaderT
   Context
   (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
   ()
 -> ReaderT
      Context
      (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
      ())
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     ()
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     ()
forall a b. (a -> b) -> a -> b
$ TCMT IO ()
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     ()
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCMT IO ()
 -> ReaderT
      Context
      (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
      ())
-> TCMT IO ()
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     ()
forall a b. (a -> b) -> a -> b
$ TypeError -> TCMT IO ()
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO ())
-> (Doc -> TypeError) -> Doc -> TCMT IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError (Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<
        TCM Doc
"Cannot postulate '" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
x TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
":" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCM Doc
forall r a (m :: * -> *).
(ToAbstract r a, PrettyTCM a, MonadPretty m, MonadError TCErr m) =>
r -> m Doc
prettyR Type
a TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
"' with safe flag"
      ReaderT
  Context
  (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
  ()
setDirty
      let r :: Relevance
r = ArgInfo -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance ArgInfo
i
      Bool
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     ()
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (ArgInfo -> Bool
forall a. LensHiding a => a -> Bool
hidden ArgInfo
i) (ReaderT
   Context
   (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
   ()
 -> ReaderT
      Context
      (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
      ())
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     ()
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     ()
forall a b. (a -> b) -> a -> b
$ TCMT IO ()
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     ()
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCMT IO ()
 -> ReaderT
      Context
      (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
      ())
-> TCMT IO ()
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     ()
forall a b. (a -> b) -> a -> b
$ TypeError -> TCMT IO ()
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO ())
-> (Doc -> TypeError) -> Doc -> TCMT IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError (Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<
        TCM Doc
"Cannot declare hidden function" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
x
      [QName]
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [QName
x]
      TCMT IO Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCMT IO Term
 -> ReaderT
      Context
      (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
      Term)
-> TCMT IO Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
forall a b. (a -> b) -> a -> b
$ do
        String -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCM Doc -> m ()
reportSDoc String
"tc.unquote.decl" Int
10 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
sep
          [ TCM Doc
"declare Postulate" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
x TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCM Doc
":"
          , Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Type -> TCM Doc
forall r a (m :: * -> *).
(ToAbstract r a, PrettyTCM a, MonadPretty m, MonadError TCErr m) =>
r -> m Doc
prettyR Type
a
          ]
        Type
a <- Expr -> TCM Type
isType_ (Expr -> TCM Type) -> TCM Expr -> TCM Type
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Type -> TCM Expr
forall r a (m :: * -> *).
(ToAbstract r a, MonadFresh NameId m, MonadError TCErr m,
 MonadTCEnv m, ReadTCState m, HasOptions m, HasConstInfo m) =>
r -> m a
toAbstract_ Type
a
        Bool
alreadyDefined <- Either SigError Definition -> Bool
forall a b. Either a b -> Bool
isRight (Either SigError Definition -> Bool)
-> TCMT IO (Either SigError Definition) -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO (Either SigError Definition)
forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Either SigError Definition)
getConstInfo' QName
x
        Bool -> TCMT IO () -> TCMT IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
alreadyDefined (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ String -> TCMT IO ()
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
String -> m a
genericError (String -> TCMT IO ()) -> String -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ String
"Multiple declarations of " String -> String -> String
forall a. [a] -> [a] -> [a]
++ QName -> String
forall a. Pretty a => a -> String
prettyShow QName
x
        QName -> Definition -> TCMT IO ()
addConstant QName
x (Definition -> TCMT IO ()) -> Definition -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ ArgInfo -> QName -> Type -> Defn -> Definition
defaultDefn ArgInfo
i QName
x Type
a Defn
Axiom
        Bool -> TCMT IO () -> TCMT IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (ArgInfo -> Bool
forall a. LensHiding a => a -> Bool
isInstance ArgInfo
i) (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ QName -> Type -> TCMT IO ()
addTypedInstance QName
x Type
a
        TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primUnitUnit

    tcDefineFun :: QName -> [R.Clause] -> UnquoteM Term
    tcDefineFun :: QName
-> [Clause]
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
tcDefineFun QName
x [Clause]
cs = ReaderT
  Context
  (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
  Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
forall a. UnquoteM a -> UnquoteM a
inOriginalContext (ReaderT
   Context
   (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
   Term
 -> ReaderT
      Context
      (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
      Term)
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
forall a b. (a -> b) -> a -> b
$ (ReaderT
  Context
  (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
  ()
setDirty ReaderT
  Context
  (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
  ()
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>>) (ReaderT
   Context
   (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
   Term
 -> ReaderT
      Context
      (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
      Term)
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
forall a b. (a -> b) -> a -> b
$ TCMT IO Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCMT IO Term
 -> ReaderT
      Context
      (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
      Term)
-> TCMT IO Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
forall a b. (a -> b) -> a -> b
$ do
      TCMT IO Bool -> TCMT IO () -> TCMT IO ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (Either SigError Definition -> Bool
forall a b. Either a b -> Bool
isLeft (Either SigError Definition -> Bool)
-> TCMT IO (Either SigError Definition) -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO (Either SigError Definition)
forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Either SigError Definition)
getConstInfo' QName
x) (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
        String -> TCMT IO ()
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
String -> m a
genericError (String -> TCMT IO ()) -> String -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ String
"Missing declaration for " String -> String -> String
forall a. [a] -> [a] -> [a]
++ QName -> String
forall a. Pretty a => a -> String
prettyShow QName
x
      [Clause]
cs <- (Clause -> TCMT IO Clause) -> [Clause] -> TCMT IO [Clause]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (QNamed Clause -> TCMT IO Clause
forall r a (m :: * -> *).
(ToAbstract r a, MonadFresh NameId m, MonadError TCErr m,
 MonadTCEnv m, ReadTCState m, HasOptions m, HasConstInfo m) =>
r -> m a
toAbstract_ (QNamed Clause -> TCMT IO Clause)
-> (Clause -> QNamed Clause) -> Clause -> TCMT IO Clause
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Clause -> QNamed Clause
forall a. QName -> a -> QNamed a
QNamed QName
x) [Clause]
cs
      String -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCM Doc -> m ()
reportSDoc String
"tc.unquote.def" Int
10 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat ([TCM Doc] -> TCM Doc) -> [TCM Doc] -> TCM Doc
forall a b. (a -> b) -> a -> b
$ (Clause -> TCM Doc) -> [Clause] -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map Clause -> TCM Doc
forall c a (m :: * -> *).
(Pretty c, ToConcrete a c, MonadAbsToCon m) =>
a -> m Doc
prettyA [Clause]
cs
      let accessDontCare :: a
accessDontCare = a
forall a. HasCallStack => a
__IMPOSSIBLE__  -- or ConcreteDef, value not looked at
      IsAbstract
ac <- (TCEnv -> IsAbstract) -> TCMT IO IsAbstract
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC (TCEnv -> Lens' IsAbstract TCEnv -> IsAbstract
forall o i. o -> Lens' i o -> i
^. forall a. LensIsAbstract a => Lens' IsAbstract a
Lens' IsAbstract TCEnv
lensIsAbstract)     -- Issue #4012, respect AbstractMode
      let i :: DefInfo' t
i = Name -> Fixity' -> Access -> IsAbstract -> Range -> DefInfo' t
forall t.
Name -> Fixity' -> Access -> IsAbstract -> Range -> DefInfo' t
mkDefInfo (Name -> Name
nameConcrete (Name -> Name) -> Name -> Name
forall a b. (a -> b) -> a -> b
$ QName -> Name
qnameName QName
x) Fixity'
noFixity' Access
forall a. a
accessDontCare IsAbstract
ac Range
forall a. Range' a
noRange
      Delayed -> DefInfo -> QName -> [Clause] -> TCMT IO ()
checkFunDef Delayed
NotDelayed DefInfo
forall t. DefInfo' t
i QName
x [Clause]
cs
      TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primUnitUnit

    tcRunSpeculative :: Term -> UnquoteM Term
    tcRunSpeculative :: Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
tcRunSpeculative Term
mu = do
      TCState
oldState <- ReaderT
  Context
  (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
  TCState
forall (m :: * -> *). MonadTCState m => m TCState
getTC
      Term
u <- Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (Term
 -> ReaderT
      Context
      (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
      Term)
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
evalTCM Term
mu
      case Term
u of
        Con ConHead
_ ConInfo
_ [Apply (Arg { unArg :: forall e. Arg e -> e
unArg = Term
x }), Apply (Arg { unArg :: forall e. Arg e -> e
unArg = Term
b })] -> do
          UnquoteM Bool
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     ()
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM (Term -> UnquoteM Bool
forall a. Unquote a => Term -> UnquoteM a
unquote Term
b) (ReaderT
   Context
   (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
   ()
 -> ReaderT
      Context
      (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
      ())
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     ()
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     ()
forall a b. (a -> b) -> a -> b
$ TCState
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     ()
forall (m :: * -> *). MonadTCState m => TCState -> m ()
putTC TCState
oldState
          Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
x
        Term
_ -> TCMT IO Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCMT IO Term
 -> ReaderT
      Context
      (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
      Term)
-> TCMT IO Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
forall a b. (a -> b) -> a -> b
$ TypeError -> TCMT IO Term
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO Term)
-> (Doc -> TypeError) -> Doc -> TCMT IO Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError (Doc -> TCMT IO Term) -> TCM Doc -> TCMT IO Term
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<
          TCM Doc
"Should be a pair: " TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
u