module Agda.TypeChecking.Unquote where

import Control.Arrow          ( first, second, (&&&) )
import Control.Monad          ( (<=<) )
import Control.Monad.Except   ( MonadError(..), ExceptT(..), runExceptT )
import Control.Monad.IO.Class ( MonadIO(..) )
import Control.Monad.Reader   ( ReaderT(..), runReaderT )
import Control.Monad.State    ( gets, modify, StateT(..), runStateT )
import Control.Monad.Writer   ( MonadWriter(..), WriterT(..), runWriterT )
import Control.Monad.Trans    ( lift )

import Data.Char
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Maybe (fromMaybe)
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Text (Text)
import qualified Data.Text as T
import Data.Word

import System.Directory (doesFileExist, getPermissions, executable)
import System.Process ( readProcessWithExitCode )
import System.Exit ( ExitCode(..) )

import Agda.Syntax.Common hiding ( Nat )
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.Info
import Agda.Syntax.Translation.ReflectedToAbstract

import Agda.Interaction.Library ( ExeName )
import Agda.Interaction.Options ( optTrustedExecutables, optAllowExec )

import Agda.TypeChecking.Constraints
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Free
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 Agda.TypeChecking.ReconstructParameters
import Agda.TypeChecking.CheckInternal

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

import Agda.Utils.Either
import Agda.Utils.Lens
import Agda.Utils.List1 (List1, pattern (:|))
import qualified Agda.Utils.List1 as List1
import Agda.Utils.Monad
import Agda.Utils.Pretty (prettyShow)
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 e (m :: * -> *) a. m (Either e a) -> ExceptT e m a
ExceptT (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.
(HasCallStack, MonadTCError 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 = Term -> Bool
loop (Term -> Bool)
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
-> UnquoteM Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f 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
tm
  where
    loop :: Term -> Bool
loop (Def QName
g Elims
_) = QName
f QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
g
    loop (Lam ArgInfo
_ Abs Term
b) = Term -> Bool
loop (Term -> Bool) -> Term -> Bool
forall a b. (a -> b) -> a -> b
$ Abs Term -> Term
forall a. Abs a -> a
unAbs Abs Term
b
    loop Term
_         = Bool
False

reduceQuotedTerm :: Term -> UnquoteM Term
reduceQuotedTerm :: Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
reduceQuotedTerm Term
t = ReaderT
  Context
  (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
  Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
locallyReduceAllDefs (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
  Term
-> (Blocker
    -> Term
    -> ReaderT
         Context
         (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
         Term)
-> (NotBlocked
    -> Term
    -> ReaderT
         Context
         (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
         Term)
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
forall t (m :: * -> *) a.
(Reduce t, IsMeta t, MonadReduce m) =>
t -> (Blocker -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
ifBlocked Term
t {-then-} (\ Blocker
m Term
_ -> 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 -> Blocker -> UnquoteError
BlockedOnMeta TCState
s Blocker
m)
              {-else-} (\ NotBlocked
_ 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
defaultAxiom) 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
defaultAxiom) 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
cs  <- Name -> String
forall a. Pretty a => a -> String
prettyShow (QName -> Name
qnameName QName
d),
        Just Char
lc <- Char -> Maybe Char
reallyToLower Char
c,
        Bool -> Bool
not (String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
cs) Bool -> Bool -> Bool
|| Char -> Bool
isUpper Char
c -> [Char
lc]
    Type
_        -> String
"_"
  where
    -- Heuristic (see #5048 for some discussion):
    -- If first character can be `toLower`ed use that, unless the name has only one character and is
    -- already lower case. (to avoid using the same name for the type and the bound variable).
    reallyToLower :: Char -> Maybe Char
reallyToLower Char
c
      | Char -> Char
toUpper Char
lc Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= Char
lc = Char -> Maybe Char
forall a. a -> Maybe a
Just Char
lc
      | Bool
otherwise        = Maybe Char
forall a. Maybe a
Nothing
      where lc :: Char
lc = Char -> Char
toLower Char
c

-- TODO: reflect Cohesion
instance Unquote Modality where
  unquote :: Term -> UnquoteM Modality
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
r,Arg Term
q] <- Elims -> Maybe [Arg Term]
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es ->
        [(UnquoteM Bool, UnquoteM Modality)]
-> UnquoteM Modality -> UnquoteM Modality
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
primModalityConstructor,
              Relevance -> Quantity -> Cohesion -> Modality
Modality (Relevance -> Quantity -> Cohesion -> Modality)
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Relevance
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     (Quantity -> Cohesion -> Modality)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Arg Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Relevance
forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
r
                       ReaderT
  Context
  (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
  (Quantity -> Cohesion -> Modality)
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Quantity
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     (Cohesion -> Modality)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Arg Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Quantity
forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
q
                       ReaderT
  Context
  (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
  (Cohesion -> Modality)
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Cohesion
-> UnquoteM Modality
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Cohesion
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Cohesion
forall (f :: * -> *) a. Applicative f => a -> f a
pure Cohesion
defaultCohesion)]
          UnquoteM Modality
forall a. HasCallStack => a
__IMPOSSIBLE__
      Con ConHead
c ConInfo
_ Elims
_ -> UnquoteM Modality
forall a. HasCallStack => a
__IMPOSSIBLE__
      Term
_ -> UnquoteError -> UnquoteM Modality
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (UnquoteError -> UnquoteM Modality)
-> UnquoteError -> UnquoteM Modality
forall a b. (a -> b) -> a -> b
$ String -> Term -> UnquoteError
NonCanonical String
"modality" 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
m] <- 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 -> Annotation -> ArgInfo
ArgInfo (Hiding
 -> Modality -> Origin -> FreeVariables -> Annotation -> ArgInfo)
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Hiding
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     (Modality -> Origin -> FreeVariables -> Annotation -> 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 -> Annotation -> ArgInfo)
-> UnquoteM Modality
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     (Origin -> FreeVariables -> Annotation -> 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
m
                      ReaderT
  Context
  (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
  (Origin -> FreeVariables -> Annotation -> ArgInfo)
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Origin
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     (FreeVariables -> Annotation -> 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 -> Annotation -> ArgInfo)
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     FreeVariables
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     (Annotation -> 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
                      ReaderT
  Context
  (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
  (Annotation -> ArgInfo)
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Annotation
-> UnquoteM ArgInfo
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Annotation
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Annotation
forall (f :: * -> *) a. Applicative f => a -> f a
pure Annotation
defaultAnnotation)]
          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 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 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 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 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 Text where
  unquote :: Term -> UnquoteM Text
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 Text
x) -> Text -> UnquoteM Text
forall (m :: * -> *) a. Monad m => a -> m a
return Text
x
      Term
_ -> UnquoteError -> UnquoteM Text
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (UnquoteError -> UnquoteM Text) -> UnquoteError -> UnquoteM Text
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 = Text -> String
T.unpack (Text -> String) -> UnquoteM Text -> UnquoteM String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> UnquoteM Text
forall a. Unquote a => Term -> UnquoteM a
unquote Term
x

unquoteNString :: Arg Term -> UnquoteM Text
unquoteNString :: Arg Term -> UnquoteM Text
unquoteNString = Arg Term -> UnquoteM Text
forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN

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 :: * -> *). Applicative 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

-- | We do a little bit of work here to make it possible to generate nice
--   layout for multi-line error messages. Specifically we split the parts
--   into lines (indicated by \n in a string part) and vcat all the lines.
prettyErrorParts :: [ErrorPart] -> TCM Doc
prettyErrorParts :: [ErrorPart] -> TCM Doc
prettyErrorParts = [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([TCM Doc] -> TCM Doc)
-> ([ErrorPart] -> [TCM Doc]) -> [ErrorPart] -> TCM Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([ErrorPart] -> TCM Doc) -> [[ErrorPart]] -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map ([TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hcat ([TCM Doc] -> TCM Doc)
-> ([ErrorPart] -> [TCM Doc]) -> [ErrorPart] -> TCM Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (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]] -> [TCM Doc])
-> ([ErrorPart] -> [[ErrorPart]]) -> [ErrorPart] -> [TCM Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [ErrorPart] -> [[ErrorPart]]
splitLines
  where
    splitLines :: [ErrorPart] -> [[ErrorPart]]
splitLines [] = []
    splitLines (StrPart String
s : [ErrorPart]
ss) =
      case (Char -> Bool) -> String -> (String, String)
forall a. (a -> Bool) -> [a] -> ([a], [a])
break (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
==Char
'\n') String
s of
        (String
s0, Char
'\n' : String
s1) -> [String -> ErrorPart
StrPart String
s0] [ErrorPart] -> [[ErrorPart]] -> [[ErrorPart]]
forall a. a -> [a] -> [a]
: [ErrorPart] -> [[ErrorPart]]
splitLines (String -> ErrorPart
StrPart String
s1 ErrorPart -> [ErrorPart] -> [ErrorPart]
forall a. a -> [a] -> [a]
: [ErrorPart]
ss)
        (String
s0, String
"")        -> ErrorPart -> [[ErrorPart]] -> [[ErrorPart]]
forall a. a -> [[a]] -> [[a]]
consLine (String -> ErrorPart
StrPart String
s0) ([ErrorPart] -> [[ErrorPart]]
splitLines [ErrorPart]
ss)
        (String, String)
_               -> [[ErrorPart]]
forall a. HasCallStack => a
__IMPOSSIBLE__
    splitLines (p :: ErrorPart
p@TermPart{} : [ErrorPart]
ss) = ErrorPart -> [[ErrorPart]] -> [[ErrorPart]]
forall a. a -> [[a]] -> [[a]]
consLine ErrorPart
p ([ErrorPart] -> [[ErrorPart]]
splitLines [ErrorPart]
ss)
    splitLines (p :: ErrorPart
p@NamePart{} : [ErrorPart]
ss) = ErrorPart -> [[ErrorPart]] -> [[ErrorPart]]
forall a. a -> [[a]] -> [[a]]
consLine ErrorPart
p ([ErrorPart] -> [[ErrorPart]]
splitLines [ErrorPart]
ss)

    consLine :: a -> [[a]] -> [[a]]
consLine a
l []        = [[a
l]]
    consLine a
l ([a]
l' : [[a]]
ls) = (a
l a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
l') [a] -> [[a]] -> [[a]]
forall a. a -> [a] -> [a]
: [[a]]
ls


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) -> (Text -> String) -> Text -> ErrorPart
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> String
T.unpack (Text -> ErrorPart) -> UnquoteM Text -> UnquoteM ErrorPart
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Arg Term -> UnquoteM Text
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 (m :: * -> *).
(ToAbstract r, MonadFresh NameId m, MonadError TCErr m,
 MonadTCEnv m, ReadTCState m, HasOptions m, HasBuiltins m,
 HasConstInfo m) =>
r -> m (AbsOfRef r)
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 a, Unquote b) => Unquote (a, b) where
  unquote :: Term -> UnquoteM (a, b)
unquote Term
t = do
    Term
t <- Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
reduceQuotedTerm Term
t
    SigmaKit{QName
ConHead
sigmaSnd :: SigmaKit -> QName
sigmaFst :: SigmaKit -> QName
sigmaCon :: SigmaKit -> ConHead
sigmaName :: SigmaKit -> QName
sigmaSnd :: QName
sigmaFst :: QName
sigmaCon :: ConHead
sigmaName :: QName
..} <- SigmaKit -> Maybe SigmaKit -> SigmaKit
forall a. a -> Maybe a -> a
fromMaybe SigmaKit
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe SigmaKit -> SigmaKit)
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     (Maybe SigmaKit)
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     SigmaKit
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ReaderT
  Context
  (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
  (Maybe SigmaKit)
forall (m :: * -> *).
(HasBuiltins m, HasConstInfo m) =>
m (Maybe SigmaKit)
getSigmaKit
    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 (a, b))]
-> UnquoteM (a, b) -> UnquoteM (a, b)
forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
choice
          [(Bool -> UnquoteM Bool
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ConHead
c ConHead -> ConHead -> Bool
forall a. Eq a => a -> a -> Bool
== ConHead
sigmaCon), (,) (a -> b -> (a, b))
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     a
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     (b -> (a, b))
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)))
  (b -> (a, b))
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     b
-> UnquoteM (a, b)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Arg Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     b
forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
y)]
          UnquoteM (a, b)
forall a. HasCallStack => a
__IMPOSSIBLE__
      Term
_ -> UnquoteError -> UnquoteM (a, b)
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (UnquoteError -> UnquoteM (a, b))
-> UnquoteError -> UnquoteM (a, b)
forall a b. (a -> b) -> a -> b
$ String -> Term -> UnquoteError
NonCanonical String
"pair" 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 Quantity where
  unquote :: Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Quantity
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)))
    Quantity)]
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Quantity
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Quantity
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
primQuantityω, Quantity
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Quantity
forall (m :: * -> *) a. Monad m => a -> m a
return (Quantity
 -> ReaderT
      Context
      (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
      Quantity)
-> Quantity
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Quantity
forall a b. (a -> b) -> a -> b
$ QωOrigin -> Quantity
Quantityω QωOrigin
QωInferred)
          ,(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
primQuantity0, Quantity
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Quantity
forall (m :: * -> *) a. Monad m => a -> m a
return (Quantity
 -> ReaderT
      Context
      (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
      Quantity)
-> Quantity
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Quantity
forall a b. (a -> b) -> a -> b
$ Q0Origin -> Quantity
Quantity0 Q0Origin
Q0Inferred)]
          ReaderT
  Context
  (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
  Quantity
forall a. HasCallStack => a
__IMPOSSIBLE__
      Con ConHead
c ConInfo
_ Elims
vs -> ReaderT
  Context
  (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
  Quantity
forall a. HasCallStack => a
__IMPOSSIBLE__
      Term
_        -> UnquoteError
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Quantity
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (UnquoteError
 -> ReaderT
      Context
      (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
      Quantity)
-> UnquoteError
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Quantity
forall a b. (a -> b) -> a -> b
$ String -> Term -> UnquoteError
NonCanonical String
"quantity" 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 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) -> (Text -> String) -> Text -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> String
T.unpack (Text -> String) -> UnquoteM Text -> UnquoteM String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Arg Term -> UnquoteM Text
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 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.
(HasCallStack, MonadTCError 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 :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ TCM Doc
"Can't unquote stale metavariable"
                  , TopLevelModuleName -> TCM Doc
forall (m :: * -> *) a. (Applicative 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. (Applicative 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)
          , (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
primAgdaSortProp, Type -> Sort
R.PropS (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
primAgdaSortPropLit, Integer -> Sort
R.PropLitS (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)
          , (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
primAgdaSortInf, Integer -> Sort
R.InfS (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
    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,    Integer -> Literal
LitNat    (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,  Double -> Literal
LitFloat  (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,   Char -> Literal
LitChar   (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, Text -> Literal
LitString (Text -> Literal) -> UnquoteM Text -> UnquoteM Literal
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Arg Term -> UnquoteM Text
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,  QName -> Literal
LitQName  (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,   AbsolutePath -> MetaId -> Literal
LitMeta   (AbsolutePath -> MetaId -> Literal)
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     AbsolutePath
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     (MetaId -> Literal)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ReaderT
  Context
  (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
  AbsolutePath
forall (m :: * -> *). MonadTCEnv m => m AbsolutePath
getCurrentPath ReaderT
  Context
  (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
  (MetaId -> Literal)
-> UnquoteM MetaId -> UnquoteM Literal
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f 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,  List1 Clause -> Elims -> Type
R.ExtLam  (List1 Clause -> Elims -> Type)
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     (List1 Clause)
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     (Elims -> Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([Clause] -> List1 Clause
forall a. [a] -> NonEmpty a
List1.fromList ([Clause] -> List1 Clause)
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     [Clause]
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     (List1 Clause)
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
_ 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,    Int -> Pattern
R.VarP    (Int -> Pattern) -> (Integer -> Int) -> Integer -> Pattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer -> Pattern) -> UnquoteM Integer -> UnquoteM Pattern
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
primAgdaPatAbsurd, Int -> Pattern
R.AbsurdP (Int -> Pattern) -> (Integer -> Int) -> Integer -> Pattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer -> Pattern) -> UnquoteM Integer -> UnquoteM Pattern
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
primAgdaPatDot,    Type -> Pattern
R.DotP  (Type -> Pattern)
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Type
-> UnquoteM Pattern
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
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, 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
primAgdaClauseAbsurd, [(Text, Arg Type)] -> [Arg Pattern] -> Clause
R.AbsurdClause ([(Text, Arg Type)] -> [Arg Pattern] -> Clause)
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     [(Text, Arg Type)]
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     ([Arg Pattern] -> Clause)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Arg Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     [(Text, Arg Type)]
forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
x ReaderT
  Context
  (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
  ([Arg Pattern] -> Clause)
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     [Arg Pattern]
-> 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)))
     [Arg Pattern]
forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
y) ]
          UnquoteM Clause
forall a. HasCallStack => a
__IMPOSSIBLE__
      Con ConHead
c ConInfo
_ Elims
es | Just [Arg Term
x, Arg Term
y, Arg Term
z] <- 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, [(Text, Arg Type)] -> [Arg Pattern] -> Type -> Clause
R.Clause ([(Text, Arg Type)] -> [Arg Pattern] -> Type -> Clause)
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     [(Text, Arg Type)]
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     ([Arg Pattern] -> 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)))
     [(Text, Arg Type)]
forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
x ReaderT
  Context
  (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
  ([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. 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 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
z) ]
          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)))
  Term
failEval = 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
$ 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
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,                  (Text -> 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 Text -> TCMT IO Term
tcFreshName                  Elim
u)
             ]
             ReaderT
  Context
  (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
  Term
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)
             , (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
primAgdaTCMQuoteOmegaTerm, Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
tcQuoteTerm (Elim -> Term
forall c. Elim' c -> c
unElim Elim
v))
             ]
             ReaderT
  Context
  (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
  Term
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,  (Text -> 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 Text -> 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
primAgdaTCMWithReconsParams, Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
tcWithReconsParams (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))
             , (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
primAgdaTCMExec, (Text -> [Text] -> Text -> 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 Text -> [Text] -> Text -> TCMT IO Term
tcExec Elim
l Elim
a Elim
u)
             ]
             ReaderT
  Context
  (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
  Term
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))
             , (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
primAgdaTCMOnlyReduceDefs, Term
-> Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
tcOnlyReduceDefs (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
primAgdaTCMDontReduceDefs, Term
-> Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
tcDontReduceDefs (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
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
failEval
    Term
_ -> ReaderT
  Context
  (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
  Term
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
$ t -> Level' t
forall t. t -> Level' t
atomicLevel 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)

    tcOnlyReduceDefs :: Term
-> Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
tcOnlyReduceDefs = (Set QName -> ReduceDefs)
-> Term
-> Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
tcDoReduceDefs Set QName -> ReduceDefs
OnlyReduceDefs
    tcDontReduceDefs :: Term
-> Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
tcDontReduceDefs = (Set QName -> ReduceDefs)
-> Term
-> Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
tcDoReduceDefs Set QName -> ReduceDefs
DontReduceDefs

    tcWithReconsParams :: Term -> UnquoteM Term
    tcWithReconsParams :: Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
tcWithReconsParams 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. MonadTCEnv m => m a -> m a
locallyReconstructed (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
$ Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
evalTCM Term
m

    tcDoReduceDefs :: (Set QName -> ReduceDefs) -> Term -> Term -> UnquoteM Term
    tcDoReduceDefs :: (Set QName -> ReduceDefs)
-> Term
-> Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
tcDoReduceDefs Set QName -> ReduceDefs
reduceDefs Term
v Term
m = do
      [QName]
qs <- Term -> UnquoteM [QName]
forall a. Unquote a => Term -> UnquoteM a
unquote Term
v
      let defs :: ReduceDefs
defs = Set QName -> ReduceDefs
reduceDefs (Set QName -> ReduceDefs) -> Set QName -> ReduceDefs
forall a b. (a -> b) -> a -> b
$ [QName] -> Set QName
forall a. Ord a => [a] -> Set a
Set.fromList [QName]
qs
      (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' ReduceDefs TCEnv
-> (ReduceDefs -> ReduceDefs)
-> TCM (UnquoteRes Term)
-> TCM (UnquoteRes Term)
forall (m :: * -> *) a b.
MonadTCEnv m =>
Lens' a TCEnv -> (a -> a) -> m b -> m b
locallyTC Lens' ReduceDefs TCEnv
eReduceDefs (ReduceDefs -> ReduceDefs -> ReduceDefs
forall a. Semigroup a => a -> a -> a
<> ReduceDefs
defs)) (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 :: Text -> TCM Term
    tcFreshName :: Text -> TCMT IO Term
tcFreshName Text
s = do
      TCMT IO Bool -> TCMT IO () -> TCMT IO ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (Lens' Bool TCEnv -> TCMT IO Bool
forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
viewTC Lens' Bool TCEnv
eCurrentlyElaborating) (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
        TypeError -> TCMT IO ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO ()) -> TypeError -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ String -> TypeError
GenericError String
"Not supported: declaring new names from an edit-time macro"
      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_ (Text -> String
T.unpack Text
s)

    tcUnify :: R.Term -> R.Term -> TCM Term
    tcUnify :: Type -> Type -> TCMT IO Term
tcUnify Type
u Type
v = do
      (Term
u, Type
a) <- TCMT IO (Term, Type) -> TCMT IO (Term, Type)
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
locallyReduceAllDefs (TCMT IO (Term, Type) -> TCMT IO (Term, Type))
-> TCMT IO (Term, Type) -> TCMT IO (Term, Type)
forall a b. (a -> b) -> a -> b
$ Expr -> TCMT IO (Term, Type)
inferExpr        (Expr -> TCMT IO (Term, Type)) -> TCM Expr -> TCMT IO (Term, Type)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Type -> TCMT IO (AbsOfRef Type)
forall r (m :: * -> *).
(ToAbstract r, MonadFresh NameId m, MonadError TCErr m,
 MonadTCEnv m, ReadTCState m, HasOptions m, HasBuiltins m,
 HasConstInfo m) =>
r -> m (AbsOfRef r)
toAbstract_ Type
u
      Term
v      <- TCMT IO Term -> TCMT IO Term
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
locallyReduceAllDefs (TCMT IO Term -> TCMT IO Term) -> TCMT IO Term -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ (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 -> TCMT IO (AbsOfRef Type)
forall r (m :: * -> *).
(ToAbstract r, MonadFresh NameId m, MonadError TCErr m,
 MonadTCEnv m, ReadTCState m, HasOptions m, HasBuiltins m,
 HasConstInfo m) =>
r -> m (AbsOfRef r)
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 -> Blocker -> UnquoteError
BlockedOnMeta TCState
s (Blocker -> UnquoteError) -> Blocker -> UnquoteError
forall a b. (a -> b) -> a -> b
$ MetaId -> Blocker
unblockOnMeta 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.
(HasCallStack, MonadTCError 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.
(HasCallStack, MonadTCError 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
=<< [ErrorPart] -> TCM Doc
prettyErrorParts [ErrorPart]
err

    tcDebugPrint :: Text -> Integer -> [ErrorPart] -> TCM Term
    tcDebugPrint :: Text -> Integer -> [ErrorPart] -> TCMT IO Term
tcDebugPrint Text
s Integer
n [ErrorPart]
msg = do
      String -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCM Doc -> m ()
reportSDoc (Text -> String
T.unpack Text
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
$ [ErrorPart] -> TCM Doc
prettyErrorParts [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
      Bool
r <- TCMT IO Bool
forall (m :: * -> *). MonadTCEnv m => m Bool
isReconstructed
      (Term
_, Type
a) <- Expr -> TCMT IO (Term, Type)
inferExpr (Expr -> TCMT IO (Term, Type)) -> TCM Expr -> TCMT IO (Term, Type)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Type -> TCMT IO (AbsOfRef Type)
forall r (m :: * -> *).
(ToAbstract r, MonadFresh NameId m, MonadError TCErr m,
 MonadTCEnv m, ReadTCState m, HasOptions m, HasBuiltins m,
 HasConstInfo m) =>
r -> m (AbsOfRef r)
toAbstract_ Type
v
      if Bool
r then do
        Type
a <- Type -> TCM Type
forall a. (InstantiateFull a, Normalise a) => a -> TCM a
process Type
a
        Type
a <- TCM Type -> TCM Type
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
locallyReduceAllDefs (TCM Type -> TCM Type) -> TCM Type -> TCM Type
forall a b. (a -> b) -> a -> b
$ Type -> TCM Type
reconstructParametersInType Type
a
        String -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCM Doc -> m ()
reportSDoc String
"tc.reconstruct" Int
50 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"Infer after reconstruct:"
          TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Type -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Type
a
        TCMT IO Term -> TCMT IO Term
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
locallyReconstructed (Type -> TCMT IO Term
quoteType Type
a)
      else
        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
      Bool
r <- TCMT IO Bool
forall (m :: * -> *). MonadTCEnv m => m Bool
isReconstructed
      Type
a <- TCM Type -> TCM Type
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
locallyReduceAllDefs (TCM Type -> TCM Type) -> TCM Type -> TCM Type
forall a b. (a -> b) -> a -> b
$ 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 -> TCMT IO (AbsOfRef Type)
forall r (m :: * -> *).
(ToAbstract r, MonadFresh NameId m, MonadError TCErr m,
 MonadTCEnv m, ReadTCState m, HasOptions m, HasBuiltins m,
 HasConstInfo m) =>
r -> m (AbsOfRef r)
toAbstract_ Type
a
      Expr
e <- Type -> TCMT IO (AbsOfRef Type)
forall r (m :: * -> *).
(ToAbstract r, MonadFresh NameId m, MonadError TCErr m,
 MonadTCEnv m, ReadTCState m, HasOptions m, HasBuiltins m,
 HasConstInfo m) =>
r -> m (AbsOfRef r)
toAbstract_ Type
v
      Term
v <- Expr -> Type -> TCMT IO Term
checkExpr Expr
e Type
a
      if Bool
r then do
        Term
v <- Term -> TCMT IO Term
forall a. (InstantiateFull a, Normalise a) => a -> TCM a
process Term
v
        Term
v <- TCMT IO Term -> TCMT IO Term
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
locallyReduceAllDefs (TCMT IO Term -> TCMT IO Term) -> TCMT IO Term -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ Action TCM -> Type -> Term -> TCMT IO Term
reconstructParameters' Action TCM
forall (m :: * -> *). PureTCM m => Action m
defaultAction Type
a Term
v
        TCMT IO Term -> TCMT IO Term
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
locallyReconstructed (Term -> TCMT IO Term
quoteTerm Term
v)
      else
        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 -> TCMT IO (AbsOfRef Type)
forall r (m :: * -> *).
(ToAbstract r, MonadFresh NameId m, MonadError TCErr m,
 MonadTCEnv m, ReadTCState m, HasOptions m, HasBuiltins m,
 HasConstInfo m) =>
r -> m (AbsOfRef r)
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
      Bool
r <- TCMT IO Bool
forall (m :: * -> *). MonadTCEnv m => m Bool
isReconstructed
      (Term
v, Type
t) <- TCMT IO (Term, Type) -> TCMT IO (Term, Type)
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
locallyReduceAllDefs (TCMT IO (Term, Type) -> TCMT IO (Term, Type))
-> TCMT IO (Term, Type) -> TCMT IO (Term, Type)
forall a b. (a -> b) -> a -> b
$ Expr -> TCMT IO (Term, Type)
inferExpr  (Expr -> TCMT IO (Term, Type)) -> TCM Expr -> TCMT IO (Term, Type)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Type -> TCMT IO (AbsOfRef Type)
forall r (m :: * -> *).
(ToAbstract r, MonadFresh NameId m, MonadError TCErr m,
 MonadTCEnv m, ReadTCState m, HasOptions m, HasBuiltins m,
 HasConstInfo m) =>
r -> m (AbsOfRef r)
toAbstract_ Type
v
      if Bool
r then do
        Term
v <- Term -> TCMT IO Term
forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
normalise Term
v
        Type
t <- Type -> TCM Type
forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
normalise Type
t
        Term
v <- TCMT IO Term -> TCMT IO Term
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
locallyReduceAllDefs (TCMT IO Term -> TCMT IO Term) -> TCMT IO Term -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ Action TCM -> Type -> Term -> TCMT IO Term
reconstructParameters' Action TCM
forall (m :: * -> *). PureTCM m => Action m
defaultAction Type
t Term
v
        String -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCM Doc -> m ()
reportSDoc String
"tc.reconstruct" Int
50 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"Normalise reconstruct:" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Term
v
        TCMT IO Term -> TCMT IO Term
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
locallyReconstructed (TCMT IO Term -> TCMT IO Term) -> TCMT IO Term -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ Term -> TCMT IO Term
quoteTerm Term
v
      else
       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
      Bool
r <- TCMT IO Bool
forall (m :: * -> *). MonadTCEnv m => m Bool
isReconstructed
      (Term
v, Type
t) <- TCMT IO (Term, Type) -> TCMT IO (Term, Type)
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
locallyReduceAllDefs (TCMT IO (Term, Type) -> TCMT IO (Term, Type))
-> TCMT IO (Term, Type) -> TCMT IO (Term, Type)
forall a b. (a -> b) -> a -> b
$ Expr -> TCMT IO (Term, Type)
inferExpr (Expr -> TCMT IO (Term, Type)) -> TCM Expr -> TCMT IO (Term, Type)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Type -> TCMT IO (AbsOfRef Type)
forall r (m :: * -> *).
(ToAbstract r, MonadFresh NameId m, MonadError TCErr m,
 MonadTCEnv m, ReadTCState m, HasOptions m, HasBuiltins m,
 HasConstInfo m) =>
r -> m (AbsOfRef r)
toAbstract_ Type
v
      if Bool
r then do
        Term
v <- 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
        Type
t <- Type -> TCM Type
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (Type -> TCM Type) -> TCM Type -> TCM Type
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Type -> TCM Type
forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull Type
t
        Term
v <- TCMT IO Term -> TCMT IO Term
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
locallyReduceAllDefs (TCMT IO Term -> TCMT IO Term) -> TCMT IO Term -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ Action TCM -> Type -> Term -> TCMT IO Term
reconstructParameters' Action TCM
forall (m :: * -> *). PureTCM m => Action m
defaultAction Type
t Term
v
        String -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCM Doc -> m ()
reportSDoc String
"tc.reconstruct" Int
50 (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"Reduce reconstruct:" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Term
v
        TCMT IO Term -> TCMT IO Term
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
locallyReconstructed (TCMT IO Term -> TCMT IO Term) -> TCMT IO Term -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ Term -> TCMT IO Term
quoteTerm Term
v
      else
        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
      Bool
r <- TCMT IO Bool
forall (m :: * -> *). MonadTCEnv m => m Bool
isReconstructed
      [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
      if Bool
r then do
         [Dom' Term Type]
as <- [Dom' Term Type] -> TCMT IO [Dom' Term Type]
recons ([Dom' Term Type] -> [Dom' Term Type]
forall a. [a] -> [a]
reverse [Dom' Term Type]
as)
         let as' :: [Dom' Term Type]
as' = [Dom' Term Type] -> [Dom' Term Type]
forall a. [a] -> [a]
reverse [Dom' Term Type]
as
         TCMT IO Term -> TCMT IO Term
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
locallyReconstructed (TCMT IO Term -> TCMT IO Term) -> TCMT IO Term -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ 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'
      else
         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
      where
         recons :: [Dom Type] -> TCM [Dom Type]
         recons :: [Dom' Term Type] -> TCMT IO [Dom' Term Type]
recons [] = [Dom' Term Type] -> TCMT IO [Dom' Term Type]
forall (m :: * -> *) a. Monad m => a -> m a
return []
         recons (d :: Dom' Term Type
d@Dom {unDom :: forall t e. Dom' t e -> e
unDom=Type
t} : [Dom' Term Type]
ds) = do
           Type
t <- TCM Type -> TCM Type
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
locallyReduceAllDefs (TCM Type -> TCM Type) -> TCM Type -> TCM Type
forall a b. (a -> b) -> a -> b
$ Type -> TCM Type
reconstructParametersInType Type
t
           let d' :: Dom' Term Type
d' = Dom' Term Type
d{unDom :: Type
unDom=Type
t}
           [Dom' Term Type]
ds' <- Dom' Term Type
-> TCMT IO [Dom' Term Type] -> TCMT IO [Dom' Term Type]
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Dom' Term Type
d' (TCMT IO [Dom' Term Type] -> TCMT IO [Dom' Term Type])
-> TCMT IO [Dom' Term Type] -> TCMT IO [Dom' Term Type]
forall a b. (a -> b) -> a -> b
$ [Dom' Term Type] -> TCMT IO [Dom' Term Type]
recons [Dom' Term Type]
ds
           [Dom' Term Type] -> TCMT IO [Dom' Term Type]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Dom' Term Type] -> TCMT IO [Dom' Term Type])
-> [Dom' Term Type] -> TCMT IO [Dom' Term Type]
forall a b. (a -> b) -> a -> b
$ Dom' Term Type
d' Dom' Term Type -> [Dom' Term Type] -> [Dom' Term Type]
forall a. a -> [a] -> [a]
: [Dom' Term Type]
ds'

    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 <- ReaderT
  Context
  (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
  (Arg Type)
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     (Arg Type)
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
locallyReduceAllDefs (ReaderT
   Context
   (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
   (Arg Type)
 -> ReaderT
      Context
      (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
      (Arg Type))
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     (Arg Type)
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     (Arg Type)
forall a b. (a -> b) -> a -> b
$ 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 (m :: * -> *).
(ToAbstract r, MonadFresh NameId m, MonadError TCErr m,
 MonadTCEnv m, ReadTCState m, HasOptions m, HasBuiltins m,
 HasConstInfo m) =>
r -> m (AbsOfRef r)
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 ((String, Dom' Term Type)
-> TCM (UnquoteRes a) -> TCM (UnquoteRes a)
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (String
"x" :: String, 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
      (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
fmap (Impossible -> Term -> Term
forall a. Subst a => Impossible -> a -> a
strengthen Impossible
HasCallStack => Impossible
impossible) (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
forall a. Arg Type -> UnquoteM a -> UnquoteM a
extendCxt Arg Type
a (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
        Term
v <- 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 a. Subst a => Int -> a -> a
raise Int
1 Term
m
        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 (Int -> Term -> Bool
forall a. Free a => Int -> a -> Bool
freeIn Int
0 Term
v) (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
$ Doc -> TCMT IO ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
Doc -> m a
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 :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hcat [TCM Doc
"Local variable '", Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Int -> Term
var Int
0), TCM Doc
"' escaping in result of extendContext:"]
            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
        Term
-> ReaderT
     Context
     (StateT UnquoteState (WriterT [QName] (ExceptT UnquoteError TCM)))
     Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
v

    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
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 :: SigError -> TCM Definition
err SigError
_ = String -> TCM Definition
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
String -> m a
genericError (String -> TCM Definition) -> String -> TCM Definition
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 = do
      Bool
r  <- TCMT IO Bool
forall (m :: * -> *). MonadTCEnv m => m Bool
isReconstructed
      Definition
ci <- QName -> TCM Definition
constInfo QName
x
      let t :: Type
t = Definition -> Type
defType Definition
ci
      if Bool
r then do
        Type
t <- TCM Type -> TCM Type
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
locallyReduceAllDefs (TCM Type -> TCM Type) -> TCM Type -> TCM Type
forall a b. (a -> b) -> a -> b
$ Type -> TCM Type
reconstructParametersInType Type
t
        Type -> TCMT IO Term
quoteType Type
t
      else
        Type -> TCMT IO Term
quoteType Type
t


    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 = do
      Bool
r <- TCMT IO Bool
forall (m :: * -> *). MonadTCEnv m => m Bool
isReconstructed
      if Bool
r then
        QName -> TCMT IO Term
tcGetDefinitionRecons QName
x
      else
        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

    tcGetDefinitionRecons :: QName -> TCM Term
    tcGetDefinitionRecons :: QName -> TCMT IO Term
tcGetDefinitionRecons QName
x = do
      ci :: Definition
ci@(Defn {theDef :: Definition -> Defn
theDef=Defn
d}) <- QName -> TCM Definition
constInfo QName
x
      case Defn
d of
        f :: Defn
f@(Function {funClauses :: Defn -> [Clause]
funClauses=[Clause]
cs}) -> do
          [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 Clause -> TCMT IO Clause
reconsClause [Clause]
cs
          TCMT IO Term -> TCMT IO Term
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
locallyReconstructed (TCMT IO Term -> TCMT IO Term) -> TCMT IO Term -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ Definition -> TCMT IO Term
quoteDefn Definition
ci{theDef :: Defn
theDef=Defn
f{funClauses :: [Clause]
funClauses=[Clause]
cs'}}

        Defn
_ -> Definition -> TCMT IO Term
quoteDefn Definition
ci

      where
        reconsClause :: Clause -> TCM Clause
        reconsClause :: Clause -> TCMT IO Clause
reconsClause Clause
c = do
          Telescope
tel' <- Telescope -> TCM Telescope
reconsTel (Telescope -> TCM Telescope) -> Telescope -> TCM Telescope
forall a b. (a -> b) -> a -> b
$ Clause -> Telescope
clauseTel Clause
c
          Maybe Term
b' <- case (Clause -> Maybe (Arg Type)
clauseType Clause
c, Clause -> Maybe Term
clauseBody Clause
c) of
                (Just Arg Type
t, Just Term
b) ->
                  Telescope -> TCMT IO (Maybe Term) -> TCMT IO (Maybe Term)
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (Clause -> Telescope
clauseTel Clause
c) (TCMT IO (Maybe Term) -> TCMT IO (Maybe Term))
-> TCMT IO (Maybe Term) -> TCMT IO (Maybe Term)
forall a b. (a -> b) -> a -> b
$ do
                     Term
bb <- TCMT IO Term -> TCMT IO Term
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
locallyReduceAllDefs
                           (TCMT IO Term -> TCMT IO Term) -> TCMT IO Term -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ Action TCM -> Type -> Term -> TCMT IO Term
reconstructParameters' Action TCM
forall (m :: * -> *). PureTCM m => Action m
defaultAction (Arg Type -> Type
forall e. Arg e -> e
unArg Arg Type
t) Term
b
                     Maybe Term -> TCMT IO (Maybe Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Term -> TCMT IO (Maybe Term))
-> Maybe Term -> TCMT IO (Maybe Term)
forall a b. (a -> b) -> a -> b
$ Term -> Maybe Term
forall a. a -> Maybe a
Just Term
bb
                (Maybe (Arg Type), Maybe Term)
_ -> Maybe Term -> TCMT IO (Maybe Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Term -> TCMT IO (Maybe Term))
-> Maybe Term -> TCMT IO (Maybe Term)
forall a b. (a -> b) -> a -> b
$ Clause -> Maybe Term
clauseBody Clause
c
          let c' :: Clause
c' = Clause
c{clauseBody :: Maybe Term
clauseBody=Maybe Term
b', clauseTel :: Telescope
clauseTel=Telescope
tel'}
          String -> Int -> TCM Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCM Doc -> m ()
reportSDoc String
"tc.reconstruct" Int
50
                   (TCM Doc -> TCMT IO ()) -> TCM Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"getDefinition reconstructed clause:" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Clause -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Clause
c'
          Clause -> TCMT IO Clause
forall (m :: * -> *) a. Monad m => a -> m a
return Clause
c'

        reconsTel :: Telescope -> TCM Telescope
        reconsTel :: Telescope -> TCM Telescope
reconsTel Telescope
EmptyTel = Telescope -> TCM Telescope
forall (m :: * -> *) a. Monad m => a -> m a
return Telescope
forall a. Tele a
EmptyTel
        reconsTel (ExtendTel Dom' Term Type
_ NoAbs{}) = TCM Telescope
forall a. HasCallStack => a
__IMPOSSIBLE__
        reconsTel (ExtendTel (d :: Dom' Term Type
d@Dom{unDom :: forall t e. Dom' t e -> e
unDom=Type
t}) ds :: Abs Telescope
ds@Abs{unAbs :: forall a. Abs a -> a
unAbs=Telescope
ts}) = do
           Type
t <- TCM Type -> TCM Type
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
locallyReduceAllDefs (TCM Type -> TCM Type) -> TCM Type -> TCM Type
forall a b. (a -> b) -> a -> b
$ Type -> TCM Type
reconstructParametersInType Type
t
           let d' :: Dom' Term Type
d' = Dom' Term Type
d{unDom :: Type
unDom=Type
t}
           Telescope
ts' <- Dom' Term Type -> TCM Telescope -> TCM Telescope
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Dom' Term Type
d' (TCM Telescope -> TCM Telescope) -> TCM Telescope -> TCM Telescope
forall a b. (a -> b) -> a -> b
$ Telescope -> TCM Telescope
reconsTel Telescope
ts
           Telescope -> TCM Telescope
forall (m :: * -> *) a. Monad m => a -> m a
return (Telescope -> TCM Telescope) -> Telescope -> TCM Telescope
forall a b. (a -> b) -> a -> b
$ Dom' Term Type -> Abs Telescope -> Telescope
forall a. a -> Abs (Tele a) -> Tele a
ExtendTel Dom' Term Type
d' Abs Telescope
ds{unAbs :: Telescope
unAbs=Telescope
ts'}


    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
      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.
(HasCallStack, MonadTCError 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 :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (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 (m :: * -> *).
(ToAbstract r, PrettyTCM (AbsOfRef r), MonadPretty m,
 MonadError TCErr m) =>
r -> m Doc
prettyR Type
a
          ]
        Type
a <- TCM Type -> TCM Type
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
locallyReduceAllDefs (TCM Type -> TCM Type) -> TCM Type -> TCM Type
forall a b. (a -> b) -> a -> b
$ 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 -> TCMT IO (AbsOfRef Type)
forall r (m :: * -> *).
(ToAbstract r, MonadFresh NameId m, MonadError TCErr m,
 MonadTCEnv m, ReadTCState m, HasOptions m, HasBuiltins m,
 HasConstInfo m) =>
r -> m (AbsOfRef r)
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.
(HasCallStack, MonadTCError 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 -> ArgInfo -> QName -> Type -> Defn -> TCMT IO ()
addConstant' QName
x 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.
(HasCallStack, MonadTCError 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 (m :: * -> *).
(ToAbstract r, PrettyTCM (AbsOfRef r), 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
      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.
(HasCallStack, MonadTCError 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 :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (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 (m :: * -> *).
(ToAbstract r, PrettyTCM (AbsOfRef r), MonadPretty m,
 MonadError TCErr m) =>
r -> m Doc
prettyR Type
a
          ]
        Type
a <- TCM Type -> TCM Type
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
locallyReduceAllDefs (TCM Type -> TCM Type) -> TCM Type -> TCM Type
forall a b. (a -> b) -> a -> b
$ 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 -> TCMT IO (AbsOfRef Type)
forall r (m :: * -> *).
(ToAbstract r, MonadFresh NameId m, MonadError TCErr m,
 MonadTCEnv m, ReadTCState m, HasOptions m, HasBuiltins m,
 HasConstInfo m) =>
r -> m (AbsOfRef r)
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.
(HasCallStack, MonadTCError 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 -> ArgInfo -> QName -> Type -> Defn -> TCMT IO ()
addConstant' QName
x ArgInfo
i QName
x Type
a Defn
defaultAxiom
        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.
(HasCallStack, MonadTCError 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 (m :: * -> *).
(ToAbstract r, MonadFresh NameId m, MonadError TCErr m,
 MonadTCEnv m, ReadTCState m, HasOptions m, HasBuiltins m,
 HasConstInfo m) =>
r -> m (AbsOfRef r)
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 :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (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 a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), 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' Expr
i = Name -> Fixity' -> Access -> IsAbstract -> Range -> DefInfo' Expr
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
      TCMT IO () -> TCMT IO ()
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
locallyReduceAllDefs (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ Delayed -> DefInfo' Expr -> QName -> [Clause] -> TCMT IO ()
checkFunDef Delayed
NotDelayed DefInfo' Expr
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.
(HasCallStack, MonadTCError 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


------------------------------------------------------------------------
-- * Trusted executables
------------------------------------------------------------------------

type ExeArg  = Text
type StdIn   = Text
type StdOut  = Text
type StdErr  = Text

-- | Raise an error if the @--allow-exec@ option was not specified.
--
requireAllowExec :: TCM ()
requireAllowExec :: TCMT IO ()
requireAllowExec = do
  Bool
allowExec <- PragmaOptions -> Bool
optAllowExec (PragmaOptions -> Bool) -> TCMT IO PragmaOptions -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
  Bool -> TCMT IO () -> TCMT IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
allowExec (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$
    TypeError -> TCMT IO ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO ()) -> TypeError -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ String -> TypeError
GenericError String
"Missing option --allow-exec"

-- | Convert an @ExitCode@ to an Agda natural number.
--
exitCodeToNat :: ExitCode -> Nat
exitCodeToNat :: ExitCode -> Nat
exitCodeToNat  ExitCode
ExitSuccess    = Integer -> Nat
Nat Integer
0
exitCodeToNat (ExitFailure Int
n) = Integer -> Nat
Nat (Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
n)

-- | Call a trusted executable with the given arguments and input.
--
--   Returns the exit code, stdout, and stderr.
--
tcExec :: ExeName -> [ExeArg] -> StdIn -> TCM Term
tcExec :: Text -> [Text] -> Text -> TCMT IO Term
tcExec Text
exe [Text]
args Text
stdIn = do
  TCMT IO ()
requireAllowExec
  Map Text String
exes <- CommandLineOptions -> Map Text String
optTrustedExecutables (CommandLineOptions -> Map Text String)
-> TCMT IO CommandLineOptions -> TCMT IO (Map Text String)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO CommandLineOptions
forall (m :: * -> *). HasOptions m => m CommandLineOptions
commandLineOptions
  case Text -> Map Text String -> Maybe String
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Text
exe Map Text String
exes of
    Maybe String
Nothing -> Text -> Map Text String -> TCMT IO Term
forall a. Text -> Map Text String -> TCM a
raiseExeNotTrusted Text
exe Map Text String
exes
    Just String
fp -> do
      -- Check that the executable exists.
      TCMT IO Bool -> TCMT IO () -> TCMT IO ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM (IO Bool -> TCMT IO Bool
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO Bool -> TCMT IO Bool) -> IO Bool -> TCMT IO Bool
forall a b. (a -> b) -> a -> b
$ String -> IO Bool
doesFileExist String
fp) (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ Text -> String -> TCMT IO ()
forall a. Text -> String -> TCM a
raiseExeNotFound Text
exe String
fp
      -- Check that the executable is executable.
      TCMT IO Bool -> TCMT IO () -> TCMT IO ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM (IO Bool -> TCMT IO Bool
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO Bool -> TCMT IO Bool) -> IO Bool -> TCMT IO Bool
forall a b. (a -> b) -> a -> b
$ Permissions -> Bool
executable (Permissions -> Bool) -> IO Permissions -> IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> IO Permissions
getPermissions String
fp) (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ Text -> String -> TCMT IO ()
forall a. Text -> String -> TCM a
raiseExeNotExecutable Text
exe String
fp

      let strArgs :: [String]
strArgs    = Text -> String
T.unpack (Text -> String) -> [Text] -> [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Text]
args
      let strStdIn :: String
strStdIn   = Text -> String
T.unpack Text
stdIn
      (ExitCode
datExitCode, String
strStdOut, String
strStdErr) <- IO (ExitCode, String, String) -> TCMT IO (ExitCode, String, String)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO (ExitCode, String, String)
 -> TCMT IO (ExitCode, String, String))
-> IO (ExitCode, String, String)
-> TCMT IO (ExitCode, String, String)
forall a b. (a -> b) -> a -> b
$ String -> [String] -> String -> IO (ExitCode, String, String)
readProcessWithExitCode String
fp [String]
strArgs String
strStdIn
      let natExitCode :: Nat
natExitCode = ExitCode -> Nat
exitCodeToNat ExitCode
datExitCode
      let txtStdOut :: Text
txtStdOut   = String -> Text
T.pack String
strStdOut
      let txtStdErr :: Text
txtStdErr   = String -> Text
T.pack String
strStdErr
      (Nat, (Text, Text)) -> Term
toR <- TCM ((Nat, (Text, Text)) -> Term)
forall a. ToTerm a => TCM (a -> Term)
toTerm
      Term -> TCMT IO Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> TCMT IO Term) -> Term -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ (Nat, (Text, Text)) -> Term
toR (Nat
natExitCode, (Text
txtStdOut, Text
txtStdErr))

-- | Raise an error if the trusted executable cannot be found.
--
raiseExeNotTrusted :: ExeName -> Map ExeName FilePath -> TCM a
raiseExeNotTrusted :: Text -> Map Text String -> TCM a
raiseExeNotTrusted Text
exe Map Text String
exes = Doc -> TCM a
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
Doc -> m a
genericDocError (Doc -> TCM a) -> TCM Doc -> TCM a
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
  [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([TCM Doc] -> TCM Doc)
-> ([String] -> [TCM Doc]) -> [String] -> TCM Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> TCM Doc) -> [String] -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map String -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty ([String] -> TCM Doc) -> [String] -> TCM Doc
forall a b. (a -> b) -> a -> b
$
    (String
"Could not find '" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Text -> String
T.unpack Text
exe String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"' in list of trusted executables:") String -> [String] -> [String]
forall a. a -> [a] -> [a]
:
    [ String
"  - " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Text -> String
T.unpack Text
exe | Text
exe <- Map Text String -> [Text]
forall k a. Map k a -> [k]
Map.keys Map Text String
exes ]

raiseExeNotFound :: ExeName -> FilePath -> TCM a
raiseExeNotFound :: Text -> String -> TCM a
raiseExeNotFound Text
exe String
fp = Doc -> TCM a
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
Doc -> m a
genericDocError (Doc -> TCM a) -> TCM Doc -> TCM a
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
  String -> TCM Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (String -> TCM Doc) -> String -> TCM Doc
forall a b. (a -> b) -> a -> b
$ String
"Could not find file '" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
fp String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"' for trusted executable " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Text -> String
T.unpack Text
exe

raiseExeNotExecutable :: ExeName -> FilePath -> TCM a
raiseExeNotExecutable :: Text -> String -> TCM a
raiseExeNotExecutable Text
exe String
fp = Doc -> TCM a
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
Doc -> m a
genericDocError (Doc -> TCM a) -> TCM Doc -> TCM a
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
  String -> TCM Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text (String -> TCM Doc) -> String -> TCM Doc
forall a b. (a -> b) -> a -> b
$ String
"File '" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
fp String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"' for trusted executable" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Text -> String
T.unpack Text
exe String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" does not have permission to execute"