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.Abstract.Views
import Agda.Syntax.Translation.InternalToAbstract
import Agda.Syntax.Literal
import Agda.Syntax.Position
import Agda.Syntax.Info as Info
import Agda.Syntax.Translation.ReflectedToAbstract
import Agda.Syntax.Scope.Base (KindOfName(ConName, DataName))

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

import qualified Agda.TypeChecking.Monad.Benchmark as Bench
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 Agda.TypeChecking.InstanceArguments

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

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.Syntax.Common.Pretty (prettyShow)
import qualified Agda.Interaction.Options.Lenses as Lens

import Agda.Utils.Impossible
import Agda.Syntax.Abstract (TypedBindingInfo(tbTacticAttr))

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
$c== :: Dirty -> Dirty -> Bool
== :: Dirty -> Dirty -> Bool
$c/= :: Dirty -> Dirty -> Bool
/= :: 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 :: forall a.
UnquoteM a -> Context -> UnquoteState -> TCM (UnquoteRes a)
unpackUnquoteM UnquoteM a
m Context
cxt UnquoteState
s = ExceptT UnquoteError (TCMT IO) ((a, UnquoteState), [QName])
-> TCMT IO (Either UnquoteError ((a, UnquoteState), [QName]))
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (ExceptT UnquoteError (TCMT IO) ((a, UnquoteState), [QName])
 -> TCMT IO (Either UnquoteError ((a, UnquoteState), [QName])))
-> ExceptT UnquoteError (TCMT IO) ((a, UnquoteState), [QName])
-> TCMT IO (Either UnquoteError ((a, UnquoteState), [QName]))
forall a b. (a -> b) -> a -> b
$ WriterT [QName] (ExceptT UnquoteError (TCMT IO)) (a, UnquoteState)
-> ExceptT UnquoteError (TCMT IO) ((a, UnquoteState), [QName])
forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT (WriterT [QName] (ExceptT UnquoteError (TCMT IO)) (a, UnquoteState)
 -> ExceptT UnquoteError (TCMT IO) ((a, UnquoteState), [QName]))
-> WriterT
     [QName] (ExceptT UnquoteError (TCMT IO)) (a, UnquoteState)
-> ExceptT UnquoteError (TCMT IO) ((a, UnquoteState), [QName])
forall a b. (a -> b) -> a -> b
$ StateT
  UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))) a
-> UnquoteState
-> WriterT
     [QName] (ExceptT UnquoteError (TCMT IO)) (a, UnquoteState)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (UnquoteM a
-> Context
-> StateT
     UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))) 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 :: forall a.
(Context -> UnquoteState -> TCM (UnquoteRes a)) -> UnquoteM a
packUnquoteM Context -> UnquoteState -> TCM (UnquoteRes a)
f = (Context
 -> StateT
      UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))) a)
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     a
forall r (m :: * -> *) a. (r -> m a) -> ReaderT r m a
ReaderT ((Context
  -> StateT
       UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))) a)
 -> ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      a)
-> (Context
    -> StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))) a)
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     a
forall a b. (a -> b) -> a -> b
$ \ Context
cxt -> (UnquoteState
 -> WriterT
      [QName] (ExceptT UnquoteError (TCMT IO)) (a, UnquoteState))
-> StateT
     UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))) a
forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
StateT ((UnquoteState
  -> WriterT
       [QName] (ExceptT UnquoteError (TCMT IO)) (a, UnquoteState))
 -> StateT
      UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))) a)
-> (UnquoteState
    -> WriterT
         [QName] (ExceptT UnquoteError (TCMT IO)) (a, UnquoteState))
-> StateT
     UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))) a
forall a b. (a -> b) -> a -> b
$ \ UnquoteState
s -> ExceptT UnquoteError (TCMT IO) ((a, UnquoteState), [QName])
-> WriterT
     [QName] (ExceptT UnquoteError (TCMT IO)) (a, UnquoteState)
forall w (m :: * -> *) a. m (a, w) -> WriterT w m a
WriterT (ExceptT UnquoteError (TCMT IO) ((a, UnquoteState), [QName])
 -> WriterT
      [QName] (ExceptT UnquoteError (TCMT IO)) (a, UnquoteState))
-> ExceptT UnquoteError (TCMT IO) ((a, UnquoteState), [QName])
-> WriterT
     [QName] (ExceptT UnquoteError (TCMT IO)) (a, UnquoteState)
forall a b. (a -> b) -> a -> b
$ TCM (UnquoteRes a)
-> ExceptT UnquoteError (TCMT IO) ((a, UnquoteState), [QName])
forall e (m :: * -> *) a. m (Either e a) -> ExceptT e m a
ExceptT (TCM (UnquoteRes a)
 -> ExceptT UnquoteError (TCMT IO) ((a, UnquoteState), [QName]))
-> TCM (UnquoteRes a)
-> ExceptT UnquoteError (TCMT IO) ((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 :: forall a. UnquoteM a -> TCM (Either UnquoteError (a, [QName]))
runUnquoteM UnquoteM a
m = do
  cxt <- (TCEnv -> Context) -> TCMT IO Context
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Context
envContext
  s   <- getTC
  pid <- fresh  -- Create a fresh problem for the unquote call. Used in tcSolveInstances.
  z   <- localTC (\ TCEnv
e -> TCEnv
e { envUnquoteProblem = Just pid })
       $ solvingProblem pid
       $ unpackUnquoteM m cxt (Clean, s)
  case z of
    Left UnquoteError
err              -> Either UnquoteError (a, [QName])
-> TCMT IO (Either UnquoteError (a, [QName]))
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either UnquoteError (a, [QName])
 -> TCMT IO (Either UnquoteError (a, [QName])))
-> Either UnquoteError (a, [QName])
-> TCMT IO (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 () -> TCMT IO (Either UnquoteError (a, [QName]))
forall a b. a -> TCMT IO b -> TCMT IO a
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
      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 def of
        Function{funClauses :: Defn -> [Clause]
funClauses = []} -> [Char] -> m ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
[Char] -> m a
genericError ([Char] -> m ()) -> [Char] -> m ()
forall a b. (a -> b) -> a -> b
$ [Char]
"Missing definition for " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ QName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow QName
x
        Defn
_       -> () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

liftU1 :: (TCM (UnquoteRes a) -> TCM (UnquoteRes b)) -> UnquoteM a -> UnquoteM b
liftU1 :: forall a b.
(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 :: forall a b c.
(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 :: forall a. 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 -> do
    n <- TCMT IO Int
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Int
getContextSize
    escapeContext __IMPOSSIBLE__ (n - length cxt) $ unpackUnquoteM m cxt s

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

isDef :: QName -> TCM (Maybe Term) -> UnquoteM Bool
isDef :: QName -> TCM (Maybe Term) -> UnquoteM Bool
isDef QName
f TCM (Maybe Term)
tm = Bool -> (Term -> Bool) -> Maybe Term -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False Term -> Bool
loop (Maybe Term -> Bool)
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     (Maybe Term)
-> UnquoteM Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCM (Maybe Term)
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     (Maybe Term)
forall a.
TCM a
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM TCM (Maybe 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 -> UnquoteM Term
reduceQuotedTerm Term
t = UnquoteM Term -> UnquoteM Term
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
locallyReduceAllDefs (UnquoteM Term -> UnquoteM Term) -> UnquoteM Term -> UnquoteM Term
forall a b. (a -> b) -> a -> b
$ do
  Term
-> (Blocker -> Term -> UnquoteM Term)
-> (NotBlocked -> Term -> UnquoteM Term)
-> UnquoteM 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 s <- (UnquoteState -> TCState)
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     TCState
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets UnquoteState -> TCState
forall a b. (a, b) -> b
snd; throwError $ BlockedOnMeta s m)
              {-else-} (\ NotBlocked
_ Term
t -> Term -> UnquoteM Term
forall a.
a
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     a
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 :: forall a. Unquote a => 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 a.
UnquoteError
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     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
$ [Char] -> Arg Term -> UnquoteError
BadVisibility [Char]
"visible" Arg Term
a

choice :: Monad m => [(m Bool, m a)] -> m a -> m a
choice :: forall (m :: * -> *) a. Monad m => [(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
  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 (TCMT IO))))
     (Either SigError Definition)
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     Defn
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     (Either SigError Definition)
forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Either SigError Definition)
getConstInfo' QName
x  -- for recursive unquoteDecl
  case i of
    Constructor{} -> do
      def <- TCMT IO Doc
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     Doc
forall a.
TCM a
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCMT IO Doc
 -> ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      Doc)
-> TCMT IO Doc
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     Doc
forall a b. (a -> b) -> a -> b
$ Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM (Term -> TCMT IO Doc) -> TCMT IO Term -> TCMT IO 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
      con <- liftTCM $ prettyTCM =<< primAgdaTermCon
      throwError $ ConInsteadOfDef x (show def) (show con)
    Defn
_ -> QName -> UnquoteM QName
forall a.
a
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     a
forall (m :: * -> *) a. Monad m => a -> m a
return QName
x

ensureCon :: QName -> UnquoteM QName
ensureCon :: QName -> UnquoteM QName
ensureCon QName
x = do
  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 (TCMT IO))))
     (Either SigError Definition)
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     Defn
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     (Either SigError Definition)
forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Either SigError Definition)
getConstInfo' QName
x  -- for recursive unquoteDecl
  case i of
    Constructor{} -> QName -> UnquoteM QName
forall a.
a
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     a
forall (m :: * -> *) a. Monad m => a -> m a
return QName
x
    Defn
_ -> do
      def <- TCMT IO Doc
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     Doc
forall a.
TCM a
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCMT IO Doc
 -> ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      Doc)
-> TCMT IO Doc
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     Doc
forall a b. (a -> b) -> a -> b
$ Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM (Term -> TCMT IO Doc) -> TCMT IO Term -> TCMT IO 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
      con <- liftTCM $ prettyTCM =<< primAgdaTermCon
      throwError $ DefInsteadOfCon x (show def) (show con)

pickName :: R.Type -> String
pickName :: Type -> [Char]
pickName Type
a =
  case Type
a of
    R.Pi{}   -> [Char]
"f"
    R.Sort{} -> [Char]
"A"
    R.Def QName
d Elims
_
      | Char
c : [Char]
cs  <- Name -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow (QName -> Name
qnameName QName
d),
        Just Char
lc <- Char -> Maybe Char
reallyToLower Char
c,
        Bool -> Bool
not ([Char] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Char]
cs) Bool -> Bool -> Bool
|| Char -> Bool
isUpper Char
c -> [Char
lc]
    Type
_        -> [Char]
"_"
  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
    t <- Term -> UnquoteM Term
reduceQuotedTerm Term
t
    case 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 -> TCM (Maybe Term) -> UnquoteM Bool
`isCon` BuiltinId -> TCM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinModalityConstructor,
              Relevance -> Quantity -> Cohesion -> Modality
Modality (Relevance -> Quantity -> Cohesion -> Modality)
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     Relevance
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     (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 (TCMT IO))))
     Relevance
forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
r
                       ReaderT
  Context
  (StateT
     UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
  (Quantity -> Cohesion -> Modality)
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     Quantity
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     (Cohesion -> Modality)
forall a b.
ReaderT
  Context
  (StateT
     UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
  (a -> b)
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     a
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Arg Term
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     Quantity
forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
q
                       ReaderT
  Context
  (StateT
     UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
  (Cohesion -> Modality)
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     Cohesion
-> UnquoteM Modality
forall a b.
ReaderT
  Context
  (StateT
     UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
  (a -> b)
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     a
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Cohesion
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     Cohesion
forall a.
a
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     a
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 a.
UnquoteError
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (UnquoteError -> UnquoteM Modality)
-> UnquoteError -> UnquoteM Modality
forall a b. (a -> b) -> a -> b
$ [Char] -> Term -> UnquoteError
NonCanonical [Char]
"modality" Term
t

instance Unquote ArgInfo where
  unquote :: Term -> UnquoteM ArgInfo
unquote Term
t = do
    t <- Term -> UnquoteM Term
reduceQuotedTerm Term
t
    case 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 -> TCM (Maybe Term) -> UnquoteM Bool
`isCon` BuiltinId -> TCM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinArgArgInfo,
              Hiding
-> Modality -> Origin -> FreeVariables -> Annotation -> ArgInfo
ArgInfo (Hiding
 -> Modality -> Origin -> FreeVariables -> Annotation -> ArgInfo)
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     Hiding
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     (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 (TCMT IO))))
     Hiding
forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
h
                      ReaderT
  Context
  (StateT
     UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
  (Modality -> Origin -> FreeVariables -> Annotation -> ArgInfo)
-> UnquoteM Modality
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     (Origin -> FreeVariables -> Annotation -> ArgInfo)
forall a b.
ReaderT
  Context
  (StateT
     UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
  (a -> b)
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     a
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     b
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 (TCMT IO))))
  (Origin -> FreeVariables -> Annotation -> ArgInfo)
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     Origin
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     (FreeVariables -> Annotation -> ArgInfo)
forall a b.
ReaderT
  Context
  (StateT
     UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
  (a -> b)
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     a
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Origin
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     Origin
forall a.
a
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Origin
Reflected
                      ReaderT
  Context
  (StateT
     UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
  (FreeVariables -> Annotation -> ArgInfo)
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     FreeVariables
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     (Annotation -> ArgInfo)
forall a b.
ReaderT
  Context
  (StateT
     UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
  (a -> b)
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     a
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> FreeVariables
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     FreeVariables
forall a.
a
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure FreeVariables
unknownFreeVariables
                      ReaderT
  Context
  (StateT
     UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
  (Annotation -> ArgInfo)
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     Annotation
-> UnquoteM ArgInfo
forall a b.
ReaderT
  Context
  (StateT
     UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
  (a -> b)
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     a
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Annotation
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     Annotation
forall a.
a
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     a
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 a.
UnquoteError
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (UnquoteError -> UnquoteM ArgInfo)
-> UnquoteError -> UnquoteM ArgInfo
forall a b. (a -> b) -> a -> b
$ [Char] -> Term -> UnquoteError
NonCanonical [Char]
"arg info" Term
t

instance Unquote a => Unquote (Arg a) where
  unquote :: Term -> UnquoteM (Arg a)
unquote Term
t = do
    t <- Term -> UnquoteM Term
reduceQuotedTerm Term
t
    case 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 -> TCM (Maybe Term) -> UnquoteM Bool
`isCon` BuiltinId -> TCM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinArgArg, 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 (TCMT IO))))
     (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 (TCMT IO))))
  (a -> Arg a)
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     a
-> UnquoteM (Arg a)
forall a b.
ReaderT
  Context
  (StateT
     UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
  (a -> b)
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     a
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Arg Term
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     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 a.
UnquoteError
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     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
$ [Char] -> Term -> UnquoteError
NonCanonical [Char]
"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 (TCMT IO))))
     (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 (TCMT IO))))
     (Arg Type)
forall a. Unquote a => Term -> UnquoteM a
unquote Term
t

instance Unquote Bool where
  unquote :: Term -> UnquoteM Bool
unquote Term
t = do
    t <- Term -> UnquoteM Term
reduceQuotedTerm Term
t
    case 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 -> TCM (Maybe Term) -> UnquoteM Bool
`isCon` BuiltinId -> TCM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinTrue,  Bool -> UnquoteM Bool
forall a.
a
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True)
               , (ConHead
c ConHead -> TCM (Maybe Term) -> UnquoteM Bool
`isCon` BuiltinId -> TCM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinFalse, Bool -> UnquoteM Bool
forall a.
a
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False) ]
               UnquoteM Bool
forall a. HasCallStack => a
__IMPOSSIBLE__
      Term
_ -> UnquoteError -> UnquoteM Bool
forall a.
UnquoteError
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (UnquoteError -> UnquoteM Bool) -> UnquoteError -> UnquoteM Bool
forall a b. (a -> b) -> a -> b
$ [Char] -> Term -> UnquoteError
NonCanonical [Char]
"boolean" Term
t

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

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

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

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

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

unquoteString :: Term -> UnquoteM String
unquoteString :: Term -> UnquoteM [Char]
unquoteString Term
x = ExeName -> [Char]
T.unpack (ExeName -> [Char]) -> UnquoteM ExeName -> UnquoteM [Char]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> UnquoteM ExeName
forall a. Unquote a => Term -> UnquoteM a
unquote Term
x

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

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

instance PrettyTCM ErrorPart where
  prettyTCM :: forall (m :: * -> *). MonadPretty m => ErrorPart -> m Doc
prettyTCM (StrPart [Char]
s)  = [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
s
  prettyTCM (TermPart Expr
t) = Expr -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Expr -> m Doc
prettyTCM Expr
t
  prettyTCM (PattPart Pattern
p) = Pattern -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Pattern -> m Doc
prettyTCM Pattern
p
  prettyTCM (NamePart QName
x) = QName -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> 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.
renderErrorParts :: [ErrorPart] -> TCM Doc
renderErrorParts :: [ErrorPart] -> TCMT IO Doc
renderErrorParts = [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat ([TCMT IO Doc] -> TCMT IO Doc)
-> ([ErrorPart] -> [TCMT IO Doc]) -> [ErrorPart] -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([ErrorPart] -> TCMT IO Doc) -> [[ErrorPart]] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map ([TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hcat ([TCMT IO Doc] -> TCMT IO Doc)
-> ([ErrorPart] -> [TCMT IO Doc]) -> [ErrorPart] -> TCMT IO Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ErrorPart -> TCMT IO Doc) -> [ErrorPart] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map ErrorPart -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => ErrorPart -> m Doc
prettyTCM) ([[ErrorPart]] -> [TCMT IO Doc])
-> ([ErrorPart] -> [[ErrorPart]]) -> [ErrorPart] -> [TCMT IO Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [ErrorPart] -> [[ErrorPart]]
splitLines
  where
    splitLines :: [ErrorPart] -> [[ErrorPart]]
splitLines [] = []
    splitLines (StrPart [Char]
s : [ErrorPart]
ss) =
      case (Char -> Bool) -> [Char] -> ([Char], [Char])
forall a. (a -> Bool) -> [a] -> ([a], [a])
break (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'\n') [Char]
s of
        ([Char]
s0, Char
'\n' : [Char]
s1) -> [[Char] -> ErrorPart
StrPart [Char]
s0] [ErrorPart] -> [[ErrorPart]] -> [[ErrorPart]]
forall a. a -> [a] -> [a]
: [ErrorPart] -> [[ErrorPart]]
splitLines ([Char] -> ErrorPart
StrPart [Char]
s1 ErrorPart -> [ErrorPart] -> [ErrorPart]
forall a. a -> [a] -> [a]
: [ErrorPart]
ss)
        ([Char]
s0, [Char]
"")        -> ErrorPart -> [[ErrorPart]] -> [[ErrorPart]]
forall {a}. a -> [[a]] -> [[a]]
consLine ([Char] -> ErrorPart
StrPart [Char]
s0) ([ErrorPart] -> [[ErrorPart]]
splitLines [ErrorPart]
ss)
        ([Char], [Char])
_               -> [[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@PattPart{} : [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
    t <- Term -> UnquoteM Term
reduceQuotedTerm Term
t
    case 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 -> TCM (Maybe Term) -> UnquoteM Bool
`isCon` BuiltinId -> TCM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinAgdaErrorPartString, [Char] -> ErrorPart
StrPart ([Char] -> ErrorPart)
-> (ExeName -> [Char]) -> ExeName -> ErrorPart
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExeName -> [Char]
T.unpack (ExeName -> ErrorPart) -> UnquoteM ExeName -> UnquoteM ErrorPart
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Arg Term -> UnquoteM ExeName
unquoteNString Arg Term
x)
               , (ConHead
c ConHead -> TCM (Maybe Term) -> UnquoteM Bool
`isCon` BuiltinId -> TCM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinAgdaErrorPartTerm,   Expr -> ErrorPart
TermPart (Expr -> ErrorPart)
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     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 (TCMT IO))))
     Expr
forall a.
TCM a
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM Expr
 -> ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      Expr)
-> (Type -> TCM Expr)
-> Type
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> TCM Expr
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)
toAbstractWithoutImplicit) (Type
 -> ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      Expr)
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     Type
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (Arg Term
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     Type
forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
x :: UnquoteM R.Term)))
               , (ConHead
c ConHead -> TCM (Maybe Term) -> UnquoteM Bool
`isCon` BuiltinId -> TCM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinAgdaErrorPartPatt,   Pattern -> ErrorPart
PattPart (Pattern -> ErrorPart)
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     Pattern
-> UnquoteM ErrorPart
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((TCM Pattern
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     Pattern
forall a.
TCM a
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM Pattern
 -> ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      Pattern)
-> (Pattern -> TCM Pattern)
-> Pattern
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     Pattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Pattern -> TCM Pattern
Pattern -> TCMT IO (AbsOfRef Pattern)
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) (Pattern
 -> ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      Pattern)
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     Pattern
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     Pattern
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (Arg Term
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     Pattern
forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
x :: UnquoteM R.Pattern)))
               , (ConHead
c ConHead -> TCM (Maybe Term) -> UnquoteM Bool
`isCon` BuiltinId -> TCM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinAgdaErrorPartName,   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 a.
UnquoteError
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (UnquoteError -> UnquoteM ErrorPart)
-> UnquoteError -> UnquoteM ErrorPart
forall a b. (a -> b) -> a -> b
$ [Char] -> Term -> UnquoteError
NonCanonical [Char]
"error part" Term
t

instance Unquote a => Unquote [a] where
  unquote :: Term -> UnquoteM [a]
unquote Term
t = do
    t <- Term -> UnquoteM Term
reduceQuotedTerm Term
t
    case 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 -> TCM (Maybe Term) -> UnquoteM Bool
`isCon` BuiltinId -> TCM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinCons, (:) (a -> [a] -> [a])
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     a
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     ([a] -> [a])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Arg Term
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     a
forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
x ReaderT
  Context
  (StateT
     UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
  ([a] -> [a])
-> UnquoteM [a] -> UnquoteM [a]
forall a b.
ReaderT
  Context
  (StateT
     UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
  (a -> b)
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     a
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     b
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 -> TCM (Maybe Term) -> UnquoteM Bool
`isCon` BuiltinId -> TCM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinNil, [a] -> UnquoteM [a]
forall a.
a
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     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 a.
UnquoteError
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     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
$ [Char] -> Term -> UnquoteError
NonCanonical [Char]
"list" Term
t

instance (Unquote a, Unquote b) => Unquote (a, b) where
  unquote :: Term -> UnquoteM (a, b)
unquote Term
t = do
    t <- Term -> UnquoteM Term
reduceQuotedTerm Term
t
    SigmaKit{..} <- fromMaybe __IMPOSSIBLE__ <$> getSigmaKit
    case 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 a.
a
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     a
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 (TCMT IO))))
     a
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     (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 (TCMT IO))))
     a
forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
x ReaderT
  Context
  (StateT
     UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
  (b -> (a, b))
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     b
-> UnquoteM (a, b)
forall a b.
ReaderT
  Context
  (StateT
     UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
  (a -> b)
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     a
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Arg Term
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     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 a.
UnquoteError
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     a
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
$ [Char] -> Term -> UnquoteError
NonCanonical [Char]
"pair" Term
t

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

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

instance Unquote Quantity where
  unquote :: Term
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     Quantity
unquote Term
t = do
    t <- Term -> UnquoteM Term
reduceQuotedTerm Term
t
    case t of
      Con ConHead
c ConInfo
_ [] ->
        [(UnquoteM Bool,
  ReaderT
    Context
    (StateT
       UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
    Quantity)]
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     Quantity
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     Quantity
forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
choice
          [(ConHead
c ConHead -> TCM (Maybe Term) -> UnquoteM Bool
`isCon` BuiltinId -> TCM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinQuantityω, Quantity
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     Quantity
forall a.
a
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     a
forall (m :: * -> *) a. Monad m => a -> m a
return (Quantity
 -> ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      Quantity)
-> Quantity
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     Quantity
forall a b. (a -> b) -> a -> b
$ QωOrigin -> Quantity
Quantityω QωOrigin
QωInferred)
          ,(ConHead
c ConHead -> TCM (Maybe Term) -> UnquoteM Bool
`isCon` BuiltinId -> TCM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinQuantity0, Quantity
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     Quantity
forall a.
a
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     a
forall (m :: * -> *) a. Monad m => a -> m a
return (Quantity
 -> ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      Quantity)
-> Quantity
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     Quantity
forall a b. (a -> b) -> a -> b
$ Q0Origin -> Quantity
Quantity0 Q0Origin
Q0Inferred)]
          ReaderT
  Context
  (StateT
     UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
  Quantity
forall a. HasCallStack => a
__IMPOSSIBLE__
      Con ConHead
c ConInfo
_ Elims
vs -> ReaderT
  Context
  (StateT
     UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
  Quantity
forall a. HasCallStack => a
__IMPOSSIBLE__
      Term
_        -> UnquoteError
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     Quantity
forall a.
UnquoteError
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (UnquoteError
 -> ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      Quantity)
-> UnquoteError
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     Quantity
forall a b. (a -> b) -> a -> b
$ [Char] -> Term -> UnquoteError
NonCanonical [Char]
"quantity" Term
t

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

instance Unquote a => Unquote (R.Abs a) where
  unquote :: Term -> UnquoteM (Abs a)
unquote Term
t = do
    t <- Term -> UnquoteM Term
reduceQuotedTerm Term
t
    case 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 -> TCM (Maybe Term) -> UnquoteM Bool
`isCon` BuiltinId -> TCM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinAbsAbs, [Char] -> a -> Abs a
forall a. [Char] -> a -> Abs a
R.Abs ([Char] -> a -> Abs a)
-> UnquoteM [Char]
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     (a -> Abs a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([Char] -> [Char]
forall {t :: * -> *} {a}.
(Foldable t, IsString (t a)) =>
t a -> t a
hint ([Char] -> [Char]) -> (ExeName -> [Char]) -> ExeName -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExeName -> [Char]
T.unpack (ExeName -> [Char]) -> UnquoteM ExeName -> UnquoteM [Char]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Arg Term -> UnquoteM ExeName
unquoteNString Arg Term
x) ReaderT
  Context
  (StateT
     UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
  (a -> Abs a)
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     a
-> UnquoteM (Abs a)
forall a b.
ReaderT
  Context
  (StateT
     UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
  (a -> b)
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     a
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Arg Term
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     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 a.
UnquoteError
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     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
$ [Char] -> Term -> UnquoteError
NonCanonical [Char]
"abstraction" Term
t

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

instance Unquote Blocker where
  unquote :: Term -> UnquoteM Blocker
unquote Term
t = do
    t <- Term -> UnquoteM Term
reduceQuotedTerm Term
t
    case 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 Blocker)]
-> UnquoteM Blocker -> UnquoteM Blocker
forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
choice
          [ (ConHead
c ConHead -> TCM (Maybe Term) -> UnquoteM Bool
`isCon` BuiltinId -> TCM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinAgdaBlockerAny, Set Blocker -> Blocker
UnblockOnAny (Set Blocker -> Blocker)
-> ([Blocker] -> Set Blocker) -> [Blocker] -> Blocker
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Blocker] -> Set Blocker
forall a. Ord a => [a] -> Set a
Set.fromList ([Blocker] -> Blocker)
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     [Blocker]
-> UnquoteM Blocker
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Arg Term
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     [Blocker]
forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
x)
          , (ConHead
c ConHead -> TCM (Maybe Term) -> UnquoteM Bool
`isCon` BuiltinId -> TCM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinAgdaBlockerAll, Set Blocker -> Blocker
UnblockOnAll (Set Blocker -> Blocker)
-> ([Blocker] -> Set Blocker) -> [Blocker] -> Blocker
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Blocker] -> Set Blocker
forall a. Ord a => [a] -> Set a
Set.fromList ([Blocker] -> Blocker)
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     [Blocker]
-> UnquoteM Blocker
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Arg Term
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     [Blocker]
forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
x)
          , (ConHead
c ConHead -> TCM (Maybe Term) -> UnquoteM Bool
`isCon` BuiltinId -> TCM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinAgdaBlockerMeta, MetaId -> Blocker
UnblockOnMeta (MetaId -> Blocker)
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     MetaId
-> UnquoteM Blocker
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Arg Term
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     MetaId
forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
x)]
          UnquoteM Blocker
forall a. HasCallStack => a
__IMPOSSIBLE__
      Con ConHead
c ConInfo
_ Elims
_ -> UnquoteM Blocker
forall a. HasCallStack => a
__IMPOSSIBLE__
      Term
_ -> UnquoteError -> UnquoteM Blocker
forall a.
UnquoteError
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (UnquoteError -> UnquoteM Blocker)
-> UnquoteError -> UnquoteM Blocker
forall a b. (a -> b) -> a -> b
$ [Char] -> Term -> UnquoteError
NonCanonical [Char]
"blocker" Term
t

instance Unquote MetaId where
  unquote :: Term
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     MetaId
unquote Term
t = do
    t <- Term -> UnquoteM Term
reduceQuotedTerm Term
t
    case t of
      Lit (LitMeta TopLevelModuleName' Range
m MetaId
x) -> TCM MetaId
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     MetaId
forall a.
TCM a
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM MetaId
 -> ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      MetaId)
-> TCM MetaId
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     MetaId
forall a b. (a -> b) -> a -> b
$ do
        live <- (TopLevelModuleName' Range -> Maybe (TopLevelModuleName' Range)
forall a. a -> Maybe a
Just TopLevelModuleName' Range
m Maybe (TopLevelModuleName' Range)
-> Maybe (TopLevelModuleName' Range) -> Bool
forall a. Eq a => a -> a -> Bool
==) (Maybe (TopLevelModuleName' Range) -> Bool)
-> TCMT IO (Maybe (TopLevelModuleName' Range)) -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO (Maybe (TopLevelModuleName' Range))
forall (m :: * -> *).
(MonadTCEnv m, ReadTCState m) =>
m (Maybe (TopLevelModuleName' Range))
currentTopLevelModule
        unless live $
            typeError . GenericDocError =<<
              sep [ "Can't unquote stale metavariable"
                  , pretty m <> "._" <> pretty (metaId x) ]
        return x
      Term
_ -> UnquoteError
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     MetaId
forall a.
UnquoteError
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (UnquoteError
 -> ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      MetaId)
-> UnquoteError
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     MetaId
forall a b. (a -> b) -> a -> b
$ [Char] -> Term -> UnquoteError
NonCanonical [Char]
"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 (TCMT IO))))
     (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 (TCMT IO))))
     (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
    t <- Term -> UnquoteM Term
reduceQuotedTerm Term
t
    case 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 -> TCM (Maybe Term) -> UnquoteM Bool
`isCon` BuiltinId -> TCM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinAgdaSortUnsupported, Sort -> UnquoteM Sort
forall a.
a
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     a
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 -> TCM (Maybe Term) -> UnquoteM Bool
`isCon` BuiltinId -> TCM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinAgdaSortSet, Type -> Sort
R.SetS (Type -> Sort)
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     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 (TCMT IO))))
     Type
forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
u)
          , (ConHead
c ConHead -> TCM (Maybe Term) -> UnquoteM Bool
`isCon` BuiltinId -> TCM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinAgdaSortLit, 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 -> TCM (Maybe Term) -> UnquoteM Bool
`isCon` BuiltinId -> TCM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinAgdaSortProp, Type -> Sort
R.PropS (Type -> Sort)
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     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 (TCMT IO))))
     Type
forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
u)
          , (ConHead
c ConHead -> TCM (Maybe Term) -> UnquoteM Bool
`isCon` BuiltinId -> TCM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinAgdaSortPropLit, 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 -> TCM (Maybe Term) -> UnquoteM Bool
`isCon` BuiltinId -> TCM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinAgdaSortInf, 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 a.
UnquoteError
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (UnquoteError -> UnquoteM Sort) -> UnquoteError -> UnquoteM Sort
forall a b. (a -> b) -> a -> b
$ [Char] -> Term -> UnquoteError
NonCanonical [Char]
"sort" Term
t

instance Unquote Literal where
  unquote :: Term -> UnquoteM Literal
unquote Term
t = do
    t <- Term -> UnquoteM Term
reduceQuotedTerm Term
t
    case 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 -> TCM (Maybe Term) -> UnquoteM Bool
`isCon` BuiltinId -> TCM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinAgdaLitNat,    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 -> TCM (Maybe Term) -> UnquoteM Bool
`isCon` BuiltinId -> TCM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinAgdaLitFloat,  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 -> TCM (Maybe Term) -> UnquoteM Bool
`isCon` BuiltinId -> TCM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinAgdaLitChar,   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 -> TCM (Maybe Term) -> UnquoteM Bool
`isCon` BuiltinId -> TCM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinAgdaLitString, ExeName -> Literal
LitString (ExeName -> Literal) -> UnquoteM ExeName -> UnquoteM Literal
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Arg Term -> UnquoteM ExeName
unquoteNString Arg Term
x)
          , (ConHead
c ConHead -> TCM (Maybe Term) -> UnquoteM Bool
`isCon` BuiltinId -> TCM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinAgdaLitQName,  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 -> TCM (Maybe Term) -> UnquoteM Bool
`isCon` BuiltinId -> TCM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinAgdaLitMeta,
             TopLevelModuleName' Range -> MetaId -> Literal
LitMeta
               (TopLevelModuleName' Range -> MetaId -> Literal)
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     (TopLevelModuleName' Range)
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     (MetaId -> Literal)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (TopLevelModuleName' Range
-> Maybe (TopLevelModuleName' Range) -> TopLevelModuleName' Range
forall a. a -> Maybe a -> a
fromMaybe TopLevelModuleName' Range
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe (TopLevelModuleName' Range) -> TopLevelModuleName' Range)
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     (Maybe (TopLevelModuleName' Range))
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     (TopLevelModuleName' Range)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ReaderT
  Context
  (StateT
     UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
  (Maybe (TopLevelModuleName' Range))
forall (m :: * -> *).
(MonadTCEnv m, ReadTCState m) =>
m (Maybe (TopLevelModuleName' Range))
currentTopLevelModule)
               ReaderT
  Context
  (StateT
     UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
  (MetaId -> Literal)
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     MetaId
-> UnquoteM Literal
forall a b.
ReaderT
  Context
  (StateT
     UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
  (a -> b)
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     a
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Arg Term
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     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 a.
UnquoteError
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (UnquoteError -> UnquoteM Literal)
-> UnquoteError -> UnquoteM Literal
forall a b. (a -> b) -> a -> b
$ [Char] -> Term -> UnquoteError
NonCanonical [Char]
"literal" Term
t

instance Unquote R.Term where
  unquote :: Term
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     Type
unquote Term
t = do
    t <- Term -> UnquoteM Term
reduceQuotedTerm Term
t
    case t of
      Con ConHead
c ConInfo
_ [] ->
        [(UnquoteM Bool,
  ReaderT
    Context
    (StateT
       UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
    Type)]
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     Type
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     Type
forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
choice
          [ (ConHead
c ConHead -> TCM (Maybe Term) -> UnquoteM Bool
`isCon` BuiltinId -> TCM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinAgdaTermUnsupported, Type
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     Type
forall a.
a
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     a
forall (m :: * -> *) a. Monad m => a -> m a
return Type
R.Unknown) ]
          ReaderT
  Context
  (StateT
     UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
  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 (TCMT IO))))
    Type)]
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     Type
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     Type
forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
choice
          [ (ConHead
c ConHead -> TCM (Maybe Term) -> UnquoteM Bool
`isCon` BuiltinId -> TCM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinAgdaTermSort,      Sort -> Type
R.Sort      (Sort -> Type)
-> UnquoteM Sort
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     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 -> TCM (Maybe Term) -> UnquoteM Bool
`isCon` BuiltinId -> TCM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinAgdaTermLit,       Literal -> Type
R.Lit       (Literal -> Type)
-> UnquoteM Literal
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     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 (TCMT IO))))
  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 (TCMT IO))))
    Type)]
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     Type
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     Type
forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
choice
          [ (ConHead
c ConHead -> TCM (Maybe Term) -> UnquoteM Bool
`isCon` BuiltinId -> TCM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinAgdaTermVar,     Int -> Elims -> Type
R.Var     (Int -> Elims -> Type)
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     Int
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     (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 (TCMT IO))))
     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 (TCMT IO))))
  (Elims -> Type)
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     Elims
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     Type
forall a b.
ReaderT
  Context
  (StateT
     UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
  (a -> b)
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     a
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Arg Term
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     Elims
forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
y)
          , (ConHead
c ConHead -> TCM (Maybe Term) -> UnquoteM Bool
`isCon` BuiltinId -> TCM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinAgdaTermCon,     QName -> Elims -> Type
R.Con     (QName -> Elims -> Type)
-> UnquoteM QName
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     (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 (TCMT IO))))
  (Elims -> Type)
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     Elims
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     Type
forall a b.
ReaderT
  Context
  (StateT
     UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
  (a -> b)
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     a
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Arg Term
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     Elims
forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
y)
          , (ConHead
c ConHead -> TCM (Maybe Term) -> UnquoteM Bool
`isCon` BuiltinId -> TCM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinAgdaTermDef,     QName -> Elims -> Type
R.Def     (QName -> Elims -> Type)
-> UnquoteM QName
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     (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 (TCMT IO))))
  (Elims -> Type)
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     Elims
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     Type
forall a b.
ReaderT
  Context
  (StateT
     UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
  (a -> b)
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     a
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Arg Term
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     Elims
forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
y)
          , (ConHead
c ConHead -> TCM (Maybe Term) -> UnquoteM Bool
`isCon` BuiltinId -> TCM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinAgdaTermMeta,    MetaId -> Elims -> Type
R.Meta    (MetaId -> Elims -> Type)
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     MetaId
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     (Elims -> Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Arg Term
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     MetaId
forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
x ReaderT
  Context
  (StateT
     UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
  (Elims -> Type)
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     Elims
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     Type
forall a b.
ReaderT
  Context
  (StateT
     UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
  (a -> b)
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     a
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Arg Term
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     Elims
forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
y)
          , (ConHead
c ConHead -> TCM (Maybe Term) -> UnquoteM Bool
`isCon` BuiltinId -> TCM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinAgdaTermLam,     Hiding -> Abs Type -> Type
R.Lam     (Hiding -> Abs Type -> Type)
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     Hiding
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     (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 (TCMT IO))))
     Hiding
forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
x ReaderT
  Context
  (StateT
     UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
  (Abs Type -> Type)
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     (Abs Type)
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     Type
forall a b.
ReaderT
  Context
  (StateT
     UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
  (a -> b)
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     a
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Arg Term
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     (Abs Type)
forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
y)
          , (ConHead
c ConHead -> TCM (Maybe Term) -> UnquoteM Bool
`isCon` BuiltinId -> TCM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinAgdaTermPi,      Dom Type -> Abs Type -> Type
mkPi      (Dom Type -> Abs Type -> Type)
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     (Dom Type)
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     (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 (TCMT IO))))
     (Dom Type)
forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
x ReaderT
  Context
  (StateT
     UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
  (Abs Type -> Type)
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     (Abs Type)
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     Type
forall a b.
ReaderT
  Context
  (StateT
     UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
  (a -> b)
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     a
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Arg Term
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     (Abs Type)
forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
y)
          , (ConHead
c ConHead -> TCM (Maybe Term) -> UnquoteM Bool
`isCon` BuiltinId -> TCM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinAgdaTermExtLam,  do
              ps <- Arg Term -> UnquoteM [Clause]
forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
x
              es <- unquoteN y
              case ps of
                []     -> UnquoteError
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     Type
forall a.
UnquoteError
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (UnquoteError
 -> ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      Type)
-> UnquoteError
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     Type
forall a b. (a -> b) -> a -> b
$ Term -> UnquoteError
PatLamWithoutClauses Term
t
                Clause
p : [Clause]
ps -> Type
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     Type
forall a.
a
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type
 -> ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      Type)
-> Type
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     Type
forall a b. (a -> b) -> a -> b
$ List1 Clause -> Elims -> Type
R.ExtLam (Clause
p Clause -> [Clause] -> List1 Clause
forall a. a -> [a] -> NonEmpty a
:| [Clause]
ps) Elims
es
            )
          ]
          ReaderT
  Context
  (StateT
     UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
  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 [Char]
"_" Type
b) = Dom Type -> Abs Type -> Type
R.Pi Dom Type
a ([Char] -> Type -> Abs Type
forall a. [Char] -> a -> Abs a
R.Abs (Type -> [Char]
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 (TCMT IO))))
  Type
forall a. HasCallStack => a
__IMPOSSIBLE__
      Lit{} -> ReaderT
  Context
  (StateT
     UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
  Type
forall a. HasCallStack => a
__IMPOSSIBLE__
      Term
_ -> UnquoteError
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     Type
forall a.
UnquoteError
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (UnquoteError
 -> ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      Type)
-> UnquoteError
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     Type
forall a b. (a -> b) -> a -> b
$ [Char] -> Term -> UnquoteError
NonCanonical [Char]
"term" Term
t

instance Unquote R.Pattern where
  unquote :: Term
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     Pattern
unquote Term
t = do
    t <- Term -> UnquoteM Term
reduceQuotedTerm Term
t
    case 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,
  ReaderT
    Context
    (StateT
       UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
    Pattern)]
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     Pattern
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     Pattern
forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
choice
          [ (ConHead
c ConHead -> TCM (Maybe Term) -> UnquoteM Bool
`isCon` BuiltinId -> TCM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinAgdaPatVar,    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
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     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 -> TCM (Maybe Term) -> UnquoteM Bool
`isCon` BuiltinId -> TCM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinAgdaPatAbsurd, 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
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     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 -> TCM (Maybe Term) -> UnquoteM Bool
`isCon` BuiltinId -> TCM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinAgdaPatDot,    Type -> Pattern
R.DotP  (Type -> Pattern)
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     Type
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     Pattern
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Arg Term
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     Type
forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
x)
          , (ConHead
c ConHead -> TCM (Maybe Term) -> UnquoteM Bool
`isCon` BuiltinId -> TCM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinAgdaPatProj,   QName -> Pattern
R.ProjP (QName -> Pattern)
-> UnquoteM QName
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     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 -> TCM (Maybe Term) -> UnquoteM Bool
`isCon` BuiltinId -> TCM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinAgdaPatLit,    Literal -> Pattern
R.LitP  (Literal -> Pattern)
-> UnquoteM Literal
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     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) ]
          ReaderT
  Context
  (StateT
     UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
  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,
  ReaderT
    Context
    (StateT
       UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
    Pattern)]
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     Pattern
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     Pattern
forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
choice
          [ (ConHead
c ConHead -> TCM (Maybe Term) -> UnquoteM Bool
`isCon` BuiltinId -> TCM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinAgdaPatCon, QName -> [Arg Pattern] -> Pattern
R.ConP (QName -> [Arg Pattern] -> Pattern)
-> UnquoteM QName
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     ([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 (TCMT IO))))
  ([Arg Pattern] -> Pattern)
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     [Arg Pattern]
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     Pattern
forall a b.
ReaderT
  Context
  (StateT
     UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
  (a -> b)
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     a
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Arg Term
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     [Arg Pattern]
forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
y) ]
          ReaderT
  Context
  (StateT
     UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
  Pattern
forall a. HasCallStack => a
__IMPOSSIBLE__
      Con ConHead
c ConInfo
_ Elims
_ -> ReaderT
  Context
  (StateT
     UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
  Pattern
forall a. HasCallStack => a
__IMPOSSIBLE__
      Term
_ -> UnquoteError
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     Pattern
forall a.
UnquoteError
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (UnquoteError
 -> ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      Pattern)
-> UnquoteError
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     Pattern
forall a b. (a -> b) -> a -> b
$ [Char] -> Term -> UnquoteError
NonCanonical [Char]
"pattern" Term
t

instance Unquote R.Clause where
  unquote :: Term -> UnquoteM Clause
unquote Term
t = do
    t <- Term -> UnquoteM Term
reduceQuotedTerm Term
t
    case 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 -> TCM (Maybe Term) -> UnquoteM Bool
`isCon` BuiltinId -> TCM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinAgdaClauseAbsurd, [(ExeName, Arg Type)] -> [Arg Pattern] -> Clause
R.AbsurdClause ([(ExeName, Arg Type)] -> [Arg Pattern] -> Clause)
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     [(ExeName, Arg Type)]
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     ([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 (TCMT IO))))
     [(ExeName, Arg Type)]
forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
x ReaderT
  Context
  (StateT
     UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
  ([Arg Pattern] -> Clause)
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     [Arg Pattern]
-> UnquoteM Clause
forall a b.
ReaderT
  Context
  (StateT
     UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
  (a -> b)
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     a
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Arg Term
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     [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 -> TCM (Maybe Term) -> UnquoteM Bool
`isCon` BuiltinId -> TCM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinAgdaClauseClause, [(ExeName, Arg Type)] -> [Arg Pattern] -> Type -> Clause
R.Clause ([(ExeName, Arg Type)] -> [Arg Pattern] -> Type -> Clause)
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     [(ExeName, Arg Type)]
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     ([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 (TCMT IO))))
     [(ExeName, Arg Type)]
forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
x ReaderT
  Context
  (StateT
     UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
  ([Arg Pattern] -> Type -> Clause)
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     [Arg Pattern]
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     (Type -> Clause)
forall a b.
ReaderT
  Context
  (StateT
     UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
  (a -> b)
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     a
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Arg Term
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     [Arg Pattern]
forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
y ReaderT
  Context
  (StateT
     UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
  (Type -> Clause)
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     Type
-> UnquoteM Clause
forall a b.
ReaderT
  Context
  (StateT
     UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
  (a -> b)
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     a
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Arg Term
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     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 a.
UnquoteError
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (UnquoteError -> UnquoteM Clause)
-> UnquoteError -> UnquoteM Clause
forall a b. (a -> b) -> a -> b
$ [Char] -> Term -> UnquoteError
NonCanonical [Char]
"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 -> UnquoteM Term
unquoteTCM Term
m Term
hole = do
  qhole <- TCMT IO Term -> UnquoteM Term
forall a.
TCM a
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCMT IO Term -> UnquoteM Term) -> TCMT IO Term -> UnquoteM Term
forall a b. (a -> b) -> a -> b
$ Term -> TCMT IO Term
quoteTerm Term
hole
  evalTCM (m `apply` [defaultArg qhole])

evalTCM :: I.Term -> UnquoteM I.Term
evalTCM :: Term -> UnquoteM Term
evalTCM Term
v = Account
  (BenchPhase
     (ReaderT
        Context
        (StateT
           UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))))
-> UnquoteM Term -> UnquoteM Term
forall (m :: * -> *) c.
MonadBench m =>
Account (BenchPhase m) -> m c -> m c
Bench.billTo [BenchPhase
  (ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO)))))
Phase
Bench.Typing, BenchPhase
  (ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO)))))
Phase
Bench.Reflection] do
  v <- Term -> UnquoteM Term
reduceQuotedTerm Term
v
  liftTCM $ reportSDoc "tc.unquote.eval" 90 $ "evalTCM" <+> prettyTCM v
  let failEval = UnquoteError -> UnquoteM Term
forall a.
UnquoteError
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (UnquoteError -> UnquoteM Term) -> UnquoteError -> UnquoteM Term
forall a b. (a -> b) -> a -> b
$ [Char] -> Term -> UnquoteError
NonCanonical [Char]
"type checking computation" Term
v

  case v of
    I.Def QName
f [] ->
      [(UnquoteM Bool, UnquoteM Term)] -> UnquoteM Term -> UnquoteM Term
forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
choice [ (QName
f QName -> TCM (Maybe Term) -> UnquoteM Bool
`isDef` BuiltinId -> TCM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinAgdaTCMGetContext,       UnquoteM Term
tcGetContext)
             , (QName
f QName -> TCM (Maybe Term) -> UnquoteM Bool
`isDef` BuiltinId -> TCM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinAgdaTCMCommit,           UnquoteM Term
tcCommit)
             , (QName
f QName -> TCM (Maybe Term) -> UnquoteM Bool
`isDef` BuiltinId -> TCM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinAgdaTCMAskNormalisation, UnquoteM Term
tcAskNormalisation)
             , (QName
f QName -> TCM (Maybe Term) -> UnquoteM Bool
`isDef` BuiltinId -> TCM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinAgdaTCMAskReconstructed, UnquoteM Term
tcAskReconstructed)
             , (QName
f QName -> TCM (Maybe Term) -> UnquoteM Bool
`isDef` BuiltinId -> TCM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinAgdaTCMAskExpandLast,    UnquoteM Term
tcAskExpandLast)
             , (QName
f QName -> TCM (Maybe Term) -> UnquoteM Bool
`isDef` BuiltinId -> TCM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinAgdaTCMAskReduceDefs,    UnquoteM Term
tcAskReduceDefs)
             , (QName
f QName -> TCM (Maybe Term) -> UnquoteM Bool
`isDef` BuiltinId -> TCM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinAgdaTCMSolveInstances,   UnquoteM Term
tcSolveInstances)
             ]
             UnquoteM Term
failEval
    I.Def QName
f [Elim
u] ->
      [(UnquoteM Bool, UnquoteM Term)] -> UnquoteM Term -> UnquoteM Term
forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
choice [ (QName
f QName -> TCM (Maybe Term) -> UnquoteM Bool
`isDef` BuiltinId -> TCM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinAgdaTCMInferType,                  (Type -> TCMT IO Term) -> Elim -> UnquoteM Term
forall a b. Unquote a => (a -> TCM b) -> Elim -> UnquoteM b
tcFun1 Type -> TCMT IO Term
tcInferType                  Elim
u)
             , (QName
f QName -> TCM (Maybe Term) -> UnquoteM Bool
`isDef` BuiltinId -> TCM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinAgdaTCMNormalise,                  (Type -> TCMT IO Term) -> Elim -> UnquoteM Term
forall a b. Unquote a => (a -> TCM b) -> Elim -> UnquoteM b
tcFun1 Type -> TCMT IO Term
tcNormalise                  Elim
u)
             , (QName
f QName -> TCM (Maybe Term) -> UnquoteM Bool
`isDef` BuiltinId -> TCM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinAgdaTCMReduce,                     (Type -> TCMT IO Term) -> Elim -> UnquoteM Term
forall a b. Unquote a => (a -> TCM b) -> Elim -> UnquoteM b
tcFun1 Type -> TCMT IO Term
tcReduce                     Elim
u)
             , (QName
f QName -> TCM (Maybe Term) -> UnquoteM Bool
`isDef` BuiltinId -> TCM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinAgdaTCMGetType,                    (QName -> TCMT IO Term) -> Elim -> UnquoteM Term
forall a b. Unquote a => (a -> TCM b) -> Elim -> UnquoteM b
tcFun1 QName -> TCMT IO Term
tcGetType                    Elim
u)
             , (QName
f QName -> TCM (Maybe Term) -> UnquoteM Bool
`isDef` BuiltinId -> TCM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinAgdaTCMGetDefinition,              (QName -> TCMT IO Term) -> Elim -> UnquoteM Term
forall a b. Unquote a => (a -> TCM b) -> Elim -> UnquoteM b
tcFun1 QName -> TCMT IO Term
tcGetDefinition              Elim
u)
             , (QName
f QName -> TCM (Maybe Term) -> UnquoteM Bool
`isDef` BuiltinId -> TCM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinAgdaTCMFormatErrorParts,           ([ErrorPart] -> TCMT IO Term) -> Elim -> UnquoteM Term
forall a b. Unquote a => (a -> TCM b) -> Elim -> UnquoteM b
tcFun1 [ErrorPart] -> TCMT IO Term
tcFormatErrorParts           Elim
u)
             , (QName
f QName -> TCM (Maybe Term) -> UnquoteM Bool
`isDef` BuiltinId -> TCM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinAgdaTCMIsMacro,                    (QName -> TCMT IO Term) -> Elim -> UnquoteM Term
forall a b. Unquote a => (a -> TCM b) -> Elim -> UnquoteM b
tcFun1 QName -> TCMT IO Term
tcIsMacro                    Elim
u)
             , (QName
f QName -> TCM (Maybe Term) -> UnquoteM Bool
`isDef` BuiltinId -> TCM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinAgdaTCMFreshName,                  (ExeName -> TCMT IO Term) -> Elim -> UnquoteM Term
forall a b. Unquote a => (a -> TCM b) -> Elim -> UnquoteM b
tcFun1 ExeName -> TCMT IO Term
tcFreshName                  Elim
u)
             , (QName
f QName -> TCM (Maybe Term) -> UnquoteM Bool
`isDef` BuiltinId -> TCM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinAgdaTCMGetInstances,               (MetaId -> UnquoteM Term) -> Elim -> UnquoteM Term
forall a b. Unquote a => (a -> UnquoteM b) -> Elim -> UnquoteM b
uqFun1 MetaId -> UnquoteM Term
tcGetInstances               Elim
u)
             ]
             UnquoteM Term
failEval
    I.Def QName
f [Elim
u, Elim
v] ->
      [(UnquoteM Bool, UnquoteM Term)] -> UnquoteM Term -> UnquoteM Term
forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
choice [ (QName
f QName -> TCM (Maybe Term) -> UnquoteM Bool
`isDef` BuiltinId -> TCM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinAgdaTCMUnify,      (Type -> Type -> TCMT IO Term) -> Elim -> Elim -> UnquoteM 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 -> TCM (Maybe Term) -> UnquoteM Bool
`isDef` BuiltinId -> TCM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinAgdaTCMCheckType,  (Type -> Type -> TCMT IO Term) -> Elim -> Elim -> UnquoteM 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 -> TCM (Maybe Term) -> UnquoteM Bool
`isDef` BuiltinId -> TCM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinAgdaTCMDeclareDef, (Arg QName -> Type -> UnquoteM Term)
-> Elim -> Elim -> UnquoteM Term
forall a b c.
(Unquote a, Unquote b) =>
(a -> b -> UnquoteM c) -> Elim -> Elim -> UnquoteM c
uqFun2 Arg QName -> Type -> UnquoteM Term
tcDeclareDef Elim
u Elim
v)
             , (QName
f QName -> TCM (Maybe Term) -> UnquoteM Bool
`isDef` BuiltinId -> TCM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinAgdaTCMDeclarePostulate, (Arg QName -> Type -> UnquoteM Term)
-> Elim -> Elim -> UnquoteM Term
forall a b c.
(Unquote a, Unquote b) =>
(a -> b -> UnquoteM c) -> Elim -> Elim -> UnquoteM c
uqFun2 Arg QName -> Type -> UnquoteM Term
tcDeclarePostulate Elim
u Elim
v)
             , (QName
f QName -> TCM (Maybe Term) -> UnquoteM Bool
`isDef` BuiltinId -> TCM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinAgdaTCMDefineData, (QName -> [(QName, (Quantity, Type))] -> UnquoteM Term)
-> Elim -> Elim -> UnquoteM Term
forall a b c.
(Unquote a, Unquote b) =>
(a -> b -> UnquoteM c) -> Elim -> Elim -> UnquoteM c
uqFun2 QName -> [(QName, (Quantity, Type))] -> UnquoteM Term
tcDefineData Elim
u Elim
v)
             , (QName
f QName -> TCM (Maybe Term) -> UnquoteM Bool
`isDef` BuiltinId -> TCM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinAgdaTCMDefineFun,  (QName -> [Clause] -> UnquoteM Term)
-> Elim -> Elim -> UnquoteM Term
forall a b c.
(Unquote a, Unquote b) =>
(a -> b -> UnquoteM c) -> Elim -> Elim -> UnquoteM c
uqFun2 QName -> [Clause] -> UnquoteM Term
tcDefineFun  Elim
u Elim
v)
             , (QName
f QName -> TCM (Maybe Term) -> UnquoteM Bool
`isDef` BuiltinId -> TCM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinAgdaTCMQuoteOmegaTerm, Type -> Term -> UnquoteM Term
tcQuoteTerm (Sort' Term -> Type
sort (Sort' Term -> Type) -> Sort' Term -> Type
forall a b. (a -> b) -> a -> b
$ Univ -> Integer -> Sort' Term
forall t. Univ -> Integer -> Sort' t
Inf Univ
UType Integer
0) (Elim -> Term
forall {c}. Elim' c -> c
unElim Elim
v))
             , (QName
f QName -> TCM (Maybe Term) -> UnquoteM Bool
`isDef` BuiltinId -> TCM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinAgdaTCMPragmaForeign, (ExeName -> ExeName -> TCMT IO Term)
-> Elim -> Elim -> UnquoteM Term
forall a b c.
(Unquote a, Unquote b) =>
(a -> b -> TCM c) -> Elim -> Elim -> UnquoteM c
tcFun2 ExeName -> ExeName -> TCMT IO Term
tcPragmaForeign Elim
u Elim
v)
             ]
             UnquoteM Term
failEval
    I.Def QName
f [Elim
l, Elim
a, Elim
u] ->
      [(UnquoteM Bool, UnquoteM Term)] -> UnquoteM Term -> UnquoteM Term
forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
choice [ (QName
f QName -> TCM (Maybe Term) -> UnquoteM Bool
`isDef` BuiltinId -> TCM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinAgdaTCMReturn,             Term -> UnquoteM Term
forall a.
a
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     a
forall (m :: * -> *) a. Monad m => a -> m a
return (Elim -> Term
forall {c}. Elim' c -> c
unElim Elim
u))
             , (QName
f QName -> TCM (Maybe Term) -> UnquoteM Bool
`isDef` BuiltinId -> TCM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinAgdaTCMTypeError,          ([ErrorPart] -> TCMT IO Term) -> Elim -> UnquoteM 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 -> TCM (Maybe Term) -> UnquoteM Bool
`isDef` BuiltinId -> TCM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinAgdaTCMQuoteTerm,          Type -> Term -> UnquoteM Term
tcQuoteTerm (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 -> Term
forall {c}. Elim' c -> c
unElim Elim
u))
             , (QName
f QName -> TCM (Maybe Term) -> UnquoteM Bool
`isDef` BuiltinId -> TCM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinAgdaTCMUnquoteTerm,        (Type -> TCMT IO Term) -> Elim -> UnquoteM 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 -> TCM (Maybe Term) -> UnquoteM Bool
`isDef` BuiltinId -> TCM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinAgdaTCMBlock,              (Blocker -> UnquoteM Term) -> Elim -> UnquoteM Term
forall a b. Unquote a => (a -> UnquoteM b) -> Elim -> UnquoteM b
uqFun1 Blocker -> UnquoteM Term
tcBlock Elim
u)
             , (QName
f QName -> TCM (Maybe Term) -> UnquoteM Bool
`isDef` BuiltinId -> TCM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinAgdaTCMDebugPrint,         (ExeName -> Integer -> [ErrorPart] -> TCMT IO Term)
-> Elim -> Elim -> Elim -> UnquoteM Term
forall a b c d.
(Unquote a, Unquote b, Unquote c) =>
(a -> b -> c -> TCM d) -> Elim -> Elim -> Elim -> UnquoteM d
tcFun3 ExeName -> Integer -> [ErrorPart] -> TCMT IO Term
tcDebugPrint Elim
l Elim
a Elim
u)
             , (QName
f QName -> TCM (Maybe Term) -> UnquoteM Bool
`isDef` BuiltinId -> TCM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinAgdaTCMNoConstraints,      Term -> UnquoteM Term
tcNoConstraints (Elim -> Term
forall {c}. Elim' c -> c
unElim Elim
u))
             , (QName
f QName -> TCM (Maybe Term) -> UnquoteM Bool
`isDef` BuiltinId -> TCM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinAgdaTCMDeclareData, (QName -> Integer -> Type -> UnquoteM Term)
-> Elim -> Elim -> Elim -> UnquoteM Term
forall a b c d.
(Unquote a, Unquote b, Unquote c) =>
(a -> b -> c -> UnquoteM d) -> Elim -> Elim -> Elim -> UnquoteM d
uqFun3 QName -> Integer -> Type -> UnquoteM Term
tcDeclareData Elim
l Elim
a Elim
u)
             , (QName
f QName -> TCM (Maybe Term) -> UnquoteM Bool
`isDef` BuiltinId -> TCM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinAgdaTCMRunSpeculative,     Term -> UnquoteM Term
tcRunSpeculative (Elim -> Term
forall {c}. Elim' c -> c
unElim Elim
u))
             , (QName
f QName -> TCM (Maybe Term) -> UnquoteM Bool
`isDef` BuiltinId -> TCM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinAgdaTCMExec, (ExeName -> [ExeName] -> ExeName -> TCMT IO Term)
-> Elim -> Elim -> Elim -> UnquoteM Term
forall a b c d.
(Unquote a, Unquote b, Unquote c) =>
(a -> b -> c -> TCM d) -> Elim -> Elim -> Elim -> UnquoteM d
tcFun3 ExeName -> [ExeName] -> ExeName -> TCMT IO Term
tcExec Elim
l Elim
a Elim
u)
             , (QName
f QName -> TCM (Maybe Term) -> UnquoteM Bool
`isDef` BuiltinId -> TCM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinAgdaTCMPragmaCompile, (ExeName -> QName -> ExeName -> TCMT IO Term)
-> Elim -> Elim -> Elim -> UnquoteM Term
forall a b c d.
(Unquote a, Unquote b, Unquote c) =>
(a -> b -> c -> TCM d) -> Elim -> Elim -> Elim -> UnquoteM d
tcFun3 ExeName -> QName -> ExeName -> TCMT IO Term
tcPragmaCompile Elim
l Elim
a Elim
u)
             , (QName
f QName -> TCM (Maybe Term) -> UnquoteM Bool
`isDef` BuiltinId -> TCM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinAgdaTCMWorkOnTypes, Term -> UnquoteM Term
tcWorkOnTypes (Elim -> Term
forall {c}. Elim' c -> c
unElim Elim
u))
             ]
             UnquoteM Term
failEval
    I.Def QName
f [Elim
_, Elim
_, Elim
u, Elim
v] ->
      [(UnquoteM Bool, UnquoteM Term)] -> UnquoteM Term -> UnquoteM Term
forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
choice [ (QName
f QName -> TCM (Maybe Term) -> UnquoteM Bool
`isDef` BuiltinId -> TCM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinAgdaTCMCatchError,        Term -> Term -> UnquoteM 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 -> TCM (Maybe Term) -> UnquoteM Bool
`isDef` BuiltinId -> TCM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinAgdaTCMWithNormalisation, Term -> Term -> UnquoteM 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 -> TCM (Maybe Term) -> UnquoteM Bool
`isDef` BuiltinId -> TCM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinAgdaTCMWithReconstructed, Term -> Term -> UnquoteM Term
tcWithReconstructed (Elim -> Term
forall {c}. Elim' c -> c
unElim Elim
u) (Elim -> Term
forall {c}. Elim' c -> c
unElim Elim
v))
             , (QName
f QName -> TCM (Maybe Term) -> UnquoteM Bool
`isDef` BuiltinId -> TCM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinAgdaTCMWithExpandLast,    Term -> Term -> UnquoteM Term
tcWithExpandLast (Elim -> Term
forall {c}. Elim' c -> c
unElim Elim
u) (Elim -> Term
forall {c}. Elim' c -> c
unElim Elim
v))
             , (QName
f QName -> TCM (Maybe Term) -> UnquoteM Bool
`isDef` BuiltinId -> TCM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinAgdaTCMWithReduceDefs,    Term -> Term -> UnquoteM Term
tcWithReduceDefs (Elim -> Term
forall {c}. Elim' c -> c
unElim Elim
u) (Elim -> Term
forall {c}. Elim' c -> c
unElim Elim
v))
             , (QName
f QName -> TCM (Maybe Term) -> UnquoteM Bool
`isDef` BuiltinId -> TCM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinAgdaTCMInContext,         Term -> Term -> UnquoteM Term
tcInContext     (Elim -> Term
forall {c}. Elim' c -> c
unElim Elim
u) (Elim -> Term
forall {c}. Elim' c -> c
unElim Elim
v))
             ]
             UnquoteM Term
failEval
    I.Def QName
f [Elim
_, Elim
_, Elim
u, Elim
v, Elim
w] ->
      [(UnquoteM Bool, UnquoteM Term)] -> UnquoteM Term -> UnquoteM Term
forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
choice [ (QName
f QName -> TCM (Maybe Term) -> UnquoteM Bool
`isDef` BuiltinId -> TCM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinAgdaTCMExtendContext, Term -> Term -> Term -> UnquoteM Term
tcExtendContext (Elim -> Term
forall {c}. Elim' c -> c
unElim Elim
u) (Elim -> Term
forall {c}. Elim' c -> c
unElim Elim
v) (Elim -> Term
forall {c}. Elim' c -> c
unElim Elim
w))
             ]
             UnquoteM Term
failEval
    I.Def QName
f [Elim
_, Elim
_, Elim
_, Elim
_, Elim
m, Elim
k] ->
      [(UnquoteM Bool, UnquoteM Term)] -> UnquoteM Term -> UnquoteM Term
forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
choice [ (QName
f QName -> TCM (Maybe Term) -> UnquoteM Bool
`isDef` BuiltinId -> TCM (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinAgdaTCMBind, Term -> Term -> UnquoteM Term
tcBind (Elim -> Term
forall {c}. Elim' c -> c
unElim Elim
m) (Elim -> Term
forall {c}. Elim' c -> c
unElim Elim
k)) ]
             UnquoteM Term
failEval
    Term
_ -> UnquoteM 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 -> UnquoteM Term
tcBind Term
m Term
k = do v <- Term -> UnquoteM Term
evalTCM Term
m
                    evalTCM (k `apply` [defaultArg v])

    process :: (InstantiateFull a, Normalise a) => a -> TCM a
    process :: forall a. (InstantiateFull a, Normalise a) => a -> TCM a
process a
v = do
      norm <- Lens' TCEnv Bool -> TCMT IO Bool
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (Bool -> f Bool) -> TCEnv -> f TCEnv
Lens' TCEnv Bool
eUnquoteNormalise
      if norm then normalise v else instantiateFull 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 -> UnquoteM Term
tcCatchError Term
m Term
h =
      (TCM (UnquoteRes Term)
 -> TCM (UnquoteRes Term) -> TCM (UnquoteRes Term))
-> UnquoteM Term -> UnquoteM Term -> UnquoteM 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 a. TCMT IO a -> (TCErr -> TCMT IO a) -> TCMT IO a
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \ TCErr
_ -> TCM (UnquoteRes Term)
m2) (Term -> UnquoteM Term
evalTCM Term
m) (Term -> UnquoteM Term
evalTCM Term
h)

    tcAskLens :: ToTerm a => Lens' TCEnv a -> UnquoteM Term
    tcAskLens :: forall a. ToTerm a => Lens' TCEnv a -> UnquoteM Term
tcAskLens Lens' TCEnv a
l = TCMT IO Term -> UnquoteM Term
forall a.
TCM a
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM (a -> Term)
forall a. ToTerm a => TCM (a -> Term)
toTerm TCM (a -> Term) -> TCMT IO a -> TCMT IO Term
forall a b. TCMT IO (a -> b) -> TCMT IO a -> TCMT IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (TCEnv -> a) -> TCMT IO a
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC (\ TCEnv
e -> TCEnv
e TCEnv -> Lens' TCEnv a -> a
forall o i. o -> Lens' o i -> i
^. (a -> f a) -> TCEnv -> f TCEnv
Lens' TCEnv a
l))

    tcWithLens :: Unquote a => Lens' TCEnv a -> Term -> Term -> UnquoteM Term
    tcWithLens :: forall a.
Unquote a =>
Lens' TCEnv a -> Term -> Term -> UnquoteM Term
tcWithLens Lens' TCEnv a
l Term
b Term
m = do
      v <- Term -> UnquoteM a
forall a. Unquote a => Term -> UnquoteM a
unquote Term
b
      liftU1 (locallyTC l $ const v) (evalTCM m)

    tcWithNormalisation, tcWithReconstructed, tcWithExpandLast, tcWithReduceDefs :: Term -> Term -> UnquoteM Term
    tcWithNormalisation :: Term -> Term -> UnquoteM Term
tcWithNormalisation = Lens' TCEnv Bool -> Term -> Term -> UnquoteM Term
forall a.
Unquote a =>
Lens' TCEnv a -> Term -> Term -> UnquoteM Term
tcWithLens (Bool -> f Bool) -> TCEnv -> f TCEnv
Lens' TCEnv Bool
eUnquoteNormalise
    tcWithReconstructed :: Term -> Term -> UnquoteM Term
tcWithReconstructed = Lens' TCEnv Bool -> Term -> Term -> UnquoteM Term
forall a.
Unquote a =>
Lens' TCEnv a -> Term -> Term -> UnquoteM Term
tcWithLens (Bool -> f Bool) -> TCEnv -> f TCEnv
Lens' TCEnv Bool
eReconstructed
    tcWithExpandLast :: Term -> Term -> UnquoteM Term
tcWithExpandLast    = Lens' TCEnv Bool -> Term -> Term -> UnquoteM Term
forall a.
Unquote a =>
Lens' TCEnv a -> Term -> Term -> UnquoteM Term
tcWithLens (Bool -> f Bool) -> TCEnv -> f TCEnv
Lens' TCEnv Bool
eExpandLastBool
    tcWithReduceDefs :: Term -> Term -> UnquoteM Term
tcWithReduceDefs    = Lens' TCEnv (Bool, [QName]) -> Term -> Term -> UnquoteM Term
forall a.
Unquote a =>
Lens' TCEnv a -> Term -> Term -> UnquoteM Term
tcWithLens ((Bool, [QName]) -> f (Bool, [QName])) -> TCEnv -> f TCEnv
Lens' TCEnv (Bool, [QName])
eReduceDefsPair

    tcAskNormalisation, tcAskReconstructed, tcAskExpandLast, tcAskReduceDefs :: UnquoteM Term
    tcAskNormalisation :: UnquoteM Term
tcAskNormalisation = Lens' TCEnv Bool -> UnquoteM Term
forall a. ToTerm a => Lens' TCEnv a -> UnquoteM Term
tcAskLens (Bool -> f Bool) -> TCEnv -> f TCEnv
Lens' TCEnv Bool
eUnquoteNormalise
    tcAskReconstructed :: UnquoteM Term
tcAskReconstructed = Lens' TCEnv Bool -> UnquoteM Term
forall a. ToTerm a => Lens' TCEnv a -> UnquoteM Term
tcAskLens (Bool -> f Bool) -> TCEnv -> f TCEnv
Lens' TCEnv Bool
eReconstructed
    tcAskExpandLast :: UnquoteM Term
tcAskExpandLast    = Lens' TCEnv Bool -> UnquoteM Term
forall a. ToTerm a => Lens' TCEnv a -> UnquoteM Term
tcAskLens (Bool -> f Bool) -> TCEnv -> f TCEnv
Lens' TCEnv Bool
eExpandLastBool
    tcAskReduceDefs :: UnquoteM Term
tcAskReduceDefs    = Lens' TCEnv (Bool, [QName]) -> UnquoteM Term
forall a. ToTerm a => Lens' TCEnv a -> UnquoteM Term
tcAskLens ((Bool, [QName]) -> f (Bool, [QName])) -> TCEnv -> f TCEnv
Lens' TCEnv (Bool, [QName])
eReduceDefsPair

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

    tcFun1 :: Unquote a => (a -> TCM b) -> Elim -> UnquoteM b
    tcFun1 :: forall a b. Unquote a => (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 a.
TCM a
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     a
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 :: forall a b c.
(Unquote a, Unquote b) =>
(a -> b -> UnquoteM c) -> Elim -> Elim -> UnquoteM c
uqFun2 a -> b -> UnquoteM c
fun Elim
a Elim
b = do
      a <- Term -> UnquoteM a
forall a. Unquote a => Term -> UnquoteM a
unquote (Elim -> Term
forall {c}. Elim' c -> c
unElim Elim
a)
      b <- unquote (unElim b)
      fun a b

    uqFun3 :: (Unquote a, Unquote b, Unquote c) => (a -> b -> c -> UnquoteM d) -> Elim -> Elim -> Elim -> UnquoteM d
    uqFun3 :: forall a b c d.
(Unquote a, Unquote b, Unquote c) =>
(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 <- Term -> UnquoteM a
forall a. Unquote a => Term -> UnquoteM a
unquote (Elim -> Term
forall {c}. Elim' c -> c
unElim Elim
a)
      b <- unquote (unElim b)
      c <- unquote (unElim c)
      fun a b c

    tcFun2 :: (Unquote a, Unquote b) => (a -> b -> TCM c) -> Elim -> Elim -> UnquoteM c
    tcFun2 :: forall a b c.
(Unquote a, Unquote b) =>
(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 a.
TCM a
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     a
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 :: forall a b c d.
(Unquote a, Unquote b, Unquote c) =>
(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 a.
TCM a
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     a
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 :: ExeName -> TCMT IO Term
tcFreshName ExeName
s = do
      TCMT IO Bool -> TCMT IO () -> TCMT IO ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (Lens' TCEnv Bool -> TCMT IO Bool
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (Bool -> f Bool) -> TCEnv -> f TCEnv
Lens' TCEnv Bool
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
$ [Char] -> TypeError
GenericError [Char]
"Not supported: declaring new names from an edit-time macro"
      m <- TCMT IO ModuleName
forall (m :: * -> *). MonadTCEnv m => m ModuleName
currentModule
      quoteName . qualify m <$> freshName_ (T.unpack s)

    tcUnify :: R.Term -> R.Term -> TCM Term
    tcUnify :: Type -> Type -> TCMT IO Term
tcUnify Type
u Type
v = do
      (u, 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
      v      <- locallyReduceAllDefs $ flip checkExpr a =<< toAbstract_ v
      equalTerm a u v
      primUnitUnit

    tcBlock :: Blocker -> UnquoteM Term
    tcBlock :: Blocker -> UnquoteM Term
tcBlock Blocker
x = do
      s <- (UnquoteState -> TCState)
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     TCState
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets UnquoteState -> TCState
forall a b. (a, b) -> b
snd
      liftTCM $ reportSDoc "tc.unquote.block" 10 $ pretty (show x)
      throwError (BlockedOnMeta s x)

    tcCommit :: UnquoteM Term
    tcCommit :: UnquoteM Term
tcCommit = do
      dirty <- (UnquoteState -> Dirty)
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     Dirty
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets UnquoteState -> Dirty
forall a b. (a, b) -> a
fst
      when (dirty == Dirty) $
        liftTCM $ typeError $ GenericError "Cannot use commitTC after declaring new definitions."
      s <- getTC
      modify (second $ const s)
      liftTCM primUnitUnit

    tcFormatErrorParts :: [ErrorPart] -> TCM Term
    tcFormatErrorParts :: [ErrorPart] -> TCMT IO Term
tcFormatErrorParts [ErrorPart]
msg = [Char] -> Term
quoteString ([Char] -> Term) -> (Doc -> [Char]) -> Doc -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow (Doc -> Term) -> TCMT IO Doc -> TCMT IO Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [ErrorPart] -> TCMT IO Doc
renderErrorParts [ErrorPart]
msg

    tcTypeError :: [ErrorPart] -> TCM a
    tcTypeError :: forall a. [ErrorPart] -> TCM a
tcTypeError [ErrorPart]
err = TypeError -> TCMT IO a
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO a) -> (Doc -> TypeError) -> Doc -> TCMT IO a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError (Doc -> TCMT IO a) -> TCMT IO Doc -> TCMT IO a
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [ErrorPart] -> TCMT IO Doc
renderErrorParts [ErrorPart]
err

    tcDebugPrint :: Text -> Integer -> [ErrorPart] -> TCM Term
    tcDebugPrint :: ExeName -> Integer -> [ErrorPart] -> TCMT IO Term
tcDebugPrint ExeName
s Integer
n [ErrorPart]
msg = do
      [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
alwaysReportSDoc (ExeName -> [Char]
T.unpack ExeName
s) (Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
n) (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [ErrorPart] -> TCMT IO Doc
renderErrorParts [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 -> UnquoteM Term
tcNoConstraints Term
m = (TCM (UnquoteRes Term) -> TCM (UnquoteRes Term))
-> UnquoteM Term -> UnquoteM 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
reallyNoConstraints (Term -> UnquoteM Term
evalTCM Term
m)

    tcWorkOnTypes :: Term -> UnquoteM Term
    tcWorkOnTypes :: Term -> UnquoteM Term
tcWorkOnTypes Term
m = (TCM (UnquoteRes Term) -> TCM (UnquoteRes Term))
-> UnquoteM Term -> UnquoteM 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, HasOptions m, MonadDebug m) =>
m a -> m a
workOnTypes (Term -> UnquoteM Term
evalTCM Term
m)

    tcInferType :: R.Term -> TCM Term
    tcInferType :: Type -> TCMT IO Term
tcInferType Type
v = do
      r <- TCMT IO Bool
forall (m :: * -> *). MonadTCEnv m => m Bool
isReconstructed
      (_, a) <- inferExpr =<< toAbstract_ v
      if r then do
        a <- process a
        a <- locallyReduceAllDefs $ reconstructParametersInType a
        reportSDoc "tc.reconstruct" 50 $ "Infer after reconstruct:"
          <+> pretty a
        locallyReconstructed (quoteType a)
      else
        quoteType =<< process a

    tcCheckType :: R.Term -> R.Type -> TCM Term
    tcCheckType :: Type -> Type -> TCMT IO Term
tcCheckType Type
v Type
a = do
      r <- TCMT IO Bool
forall (m :: * -> *). MonadTCEnv m => m Bool
isReconstructed
      a <- workOnTypes $ locallyReduceAllDefs $ isType_ =<< toAbstract_ a
      e <- toAbstract_ v
      v <- checkExpr e a
      if r then do
        v <- process v
        v <- locallyReduceAllDefs $ reconstructParameters a v
        locallyReconstructed (quoteTerm v)
      else
        quoteTerm =<< process v

    tcQuoteTerm :: Type -> Term -> UnquoteM Term
    tcQuoteTerm :: Type -> Term -> UnquoteM Term
tcQuoteTerm Type
a Term
v = TCMT IO Term -> UnquoteM Term
forall a.
TCM a
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCMT IO Term -> UnquoteM Term) -> TCMT IO Term -> UnquoteM Term
forall a b. (a -> b) -> a -> b
$ do
      r <- TCMT IO Bool
forall (m :: * -> *). MonadTCEnv m => m Bool
isReconstructed
      if r then do
        v <- process v
        v <- locallyReduceAllDefs $ reconstructParameters a v
        locallyReconstructed (quoteTerm v)
      else
        quoteTerm =<< process v

    tcUnquoteTerm :: Type -> R.Term -> TCM Term
    tcUnquoteTerm :: Type -> Type -> TCMT IO Term
tcUnquoteTerm Type
a Type
v = do
      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
      checkExpr e a

    tcNormalise :: R.Term -> TCM Term
    tcNormalise :: Type -> TCMT IO Term
tcNormalise Type
v = do
      r <- TCMT IO Bool
forall (m :: * -> *). MonadTCEnv m => m Bool
isReconstructed
      (v, t) <- locallyReduceAllDefs $ inferExpr  =<< toAbstract_ v
      if r then do
        v <- normalise v
        t <- normalise t
        v <- locallyReduceAllDefs $ reconstructParameters' defaultAction t v
        reportSDoc "tc.reconstruct" 50 $ "Normalise reconstruct:" <+> pretty v
        locallyReconstructed $ quoteTerm v
      else
       quoteTerm =<< normalise v

    tcReduce :: R.Term -> TCM Term
    tcReduce :: Type -> TCMT IO Term
tcReduce Type
v = do
      r <- TCMT IO Bool
forall (m :: * -> *). MonadTCEnv m => m Bool
isReconstructed
      (v, t) <- locallyReduceAllDefs $ inferExpr =<< toAbstract_ v
      if r then do
        v <- reduce =<< instantiateFull v
        t <- reduce =<< instantiateFull t
        v <- locallyReduceAllDefs $ reconstructParameters' defaultAction t v
        reportSDoc "tc.reconstruct" 50 $ "Reduce reconstruct:" <+> pretty v
        locallyReconstructed $ quoteTerm v
      else
        quoteTerm =<< reduce =<< instantiateFull v

    tcGetContext :: UnquoteM Term
    tcGetContext :: UnquoteM Term
tcGetContext = TCMT IO Term -> UnquoteM Term
forall a.
TCM a
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCMT IO Term -> UnquoteM Term) -> TCMT IO Term -> UnquoteM Term
forall a b. (a -> b) -> a -> b
$ do
      r <- TCMT IO Bool
forall (m :: * -> *). MonadTCEnv m => m Bool
isReconstructed
      as <- map (nameToArgName . fst . unDom &&& fmap snd) <$> getContext
      as <- etaContract =<< process as
      if r then do
        as <- recons (reverse as)
        let as' = [([Char], Dom Type)] -> [([Char], Dom Type)]
forall a. [a] -> [a]
reverse [([Char], Dom Type)]
as
        locallyReconstructed $ buildList <*> mapM quoteDomWithName as'
      else
        buildList <*> mapM quoteDomWithName as
      where
        recons :: [(ArgName, Dom Type)] -> TCM [(ArgName, Dom Type)]
        recons :: [([Char], Dom Type)] -> TCMT IO [([Char], Dom Type)]
recons []                        = [([Char], Dom Type)] -> TCMT IO [([Char], Dom Type)]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return []
        recons (([Char]
s, d :: Dom Type
d@Dom {unDom :: forall t e. Dom' t e -> e
unDom=Type
t}):[([Char], Dom Type)]
ds) = do
          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 Type
d{unDom=t}
          ds' <- addContext (s, d') $ recons ds
          return $ (s, d'):ds'

        quoteDomWithName :: (ArgName, Dom Type) -> TCM Term
        quoteDomWithName :: ([Char], Dom Type) -> TCMT IO Term
quoteDomWithName ([Char]
x, Dom Type
t) = TCM ((ExeName, Dom Type) -> Term)
forall a. ToTerm a => TCM (a -> Term)
toTerm TCM ((ExeName, Dom Type) -> Term)
-> TCMT IO (ExeName, Dom Type) -> TCMT IO Term
forall a b. TCMT IO (a -> b) -> TCMT IO a -> TCMT IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (ExeName, Dom Type) -> TCMT IO (ExeName, Dom Type)
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Char] -> ExeName
T.pack [Char]
x, Dom Type
t)

    extendCxt :: Text -> Arg R.Type -> UnquoteM a -> UnquoteM a
    extendCxt :: forall a. ExeName -> Arg Type -> UnquoteM a -> UnquoteM a
extendCxt ExeName
s Arg Type
a UnquoteM a
m = do
      a <- ReaderT
  Context
  (StateT
     UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
  (Arg Type)
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     (Arg Type)
forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
workOnTypes (ReaderT
   Context
   (StateT
      UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
   (Arg Type)
 -> ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      (Arg Type))
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     (Arg Type)
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     (Arg Type)
forall a b. (a -> b) -> a -> b
$ ReaderT
  Context
  (StateT
     UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
  (Arg Type)
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     (Arg Type)
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
locallyReduceAllDefs (ReaderT
   Context
   (StateT
      UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
   (Arg Type)
 -> ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      (Arg Type))
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     (Arg Type)
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     (Arg Type)
forall a b. (a -> b) -> a -> b
$ TCM (Arg Type)
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     (Arg Type)
forall a.
TCM a
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM (Arg Type)
 -> ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      (Arg Type))
-> TCM (Arg Type)
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     (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)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Arg a -> f (Arg 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
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_) Arg Type
a
      liftU1 (addContext (s, domFromArg a :: Dom Type)) m

    tcExtendContext :: Term -> Term -> Term -> UnquoteM Term
    tcExtendContext :: Term -> Term -> Term -> UnquoteM Term
tcExtendContext Term
s Term
a Term
m = do
      s <- Term -> UnquoteM ExeName
forall a. Unquote a => Term -> UnquoteM a
unquote Term
s
      a <- unquote a
      fmap (strengthen impossible) $ extendCxt s a $ do
        v <- evalTCM $ raise 1 m
        -- 2024-04-20: free variable analysis only really makes sense on normal forms; see #7227
        v <- normalise v
        when (freeIn 0 v) $ liftTCM $ genericDocError =<<
          hcat ["Local variable '", prettyTCM (var 0), "' escaping in result of extendContext:"]
            <?> prettyTCM v
        return v

    tcInContext :: Term -> Term -> UnquoteM Term
    tcInContext :: Term -> Term -> UnquoteM Term
tcInContext Term
c Term
m = do
      c <- Term
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     [(ExeName, Arg Type)]
forall a. Unquote a => Term -> UnquoteM a
unquote Term
c
      inOriginalContext $ go c (evalTCM m)
      where
        go :: [(Text , Arg R.Type)] -> UnquoteM Term -> UnquoteM Term
        go :: [(ExeName, Arg Type)] -> UnquoteM Term -> UnquoteM Term
go []             UnquoteM Term
m = UnquoteM Term
m
        go ((ExeName
s , Arg Type
a) : [(ExeName, Arg Type)]
as) UnquoteM Term
m = [(ExeName, Arg Type)] -> UnquoteM Term -> UnquoteM Term
go [(ExeName, Arg Type)]
as (ExeName -> Arg Type -> UnquoteM Term -> UnquoteM Term
forall a. ExeName -> Arg Type -> UnquoteM a -> UnquoteM a
extendCxt ExeName
s Arg Type
a UnquoteM 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 a. a -> TCMT IO a
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
_ = [Char] -> TCM Definition
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
[Char] -> m a
genericError ([Char] -> TCM Definition) -> [Char] -> TCM Definition
forall a b. (a -> b) -> a -> b
$ [Char]
"Unbound name: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ QName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow QName
x

    tcGetType :: QName -> TCM Term
    tcGetType :: QName -> TCMT IO Term
tcGetType QName
x = do
      r  <- TCMT IO Bool
forall (m :: * -> *). MonadTCEnv m => m Bool
isReconstructed
      ci <- constInfo x >>= instantiateDef
      let t = Definition -> Type
defType Definition
ci
      if r then do
        t <- locallyReduceAllDefs $ reconstructParametersInType t
        quoteType t
      else
        quoteType t


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

    tcGetDefinition :: QName -> TCM Term
    tcGetDefinition :: QName -> TCMT IO Term
tcGetDefinition QName
x = do
      r <- TCMT IO Bool
forall (m :: * -> *). MonadTCEnv m => m Bool
isReconstructed
      if r then
        tcGetDefinitionRecons x
      else
        quoteDefn =<< instantiateDef =<< constInfo x

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

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

      where
        reconsClause :: Clause -> TCM Clause
        reconsClause :: Clause -> TCMT IO Clause
reconsClause Clause
c = do
          tel' <- Tele (Dom Type) -> TCM (Tele (Dom Type))
reconsTel (Tele (Dom Type) -> TCM (Tele (Dom Type)))
-> Tele (Dom Type) -> TCM (Tele (Dom Type))
forall a b. (a -> b) -> a -> b
$ Clause -> Tele (Dom Type)
clauseTel Clause
c
          b' <- case (clauseType c, clauseBody c) of
                (Just Arg Type
t, Just Term
b) ->
                  Tele (Dom Type) -> TCM (Maybe Term) -> TCM (Maybe Term)
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Tele (Dom Type) -> m a -> m a
addContext (Clause -> Tele (Dom Type)
clauseTel Clause
c) (TCM (Maybe Term) -> TCM (Maybe Term))
-> TCM (Maybe Term) -> TCM (Maybe Term)
forall a b. (a -> b) -> a -> b
$ do
                     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 (TCMT IO) -> Type -> Term -> TCMT IO Term
reconstructParameters' Action (TCMT IO)
forall (m :: * -> *). PureTCM m => Action m
defaultAction (Arg Type -> Type
forall e. Arg e -> e
unArg Arg Type
t) Term
b
                     return $ Just bb
                (Maybe (Arg Type), Maybe Term)
_ -> Maybe Term -> TCM (Maybe Term)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Term -> TCM (Maybe Term)) -> Maybe Term -> TCM (Maybe Term)
forall a b. (a -> b) -> a -> b
$ Clause -> Maybe Term
clauseBody Clause
c
          let c' = Clause
c{clauseBody=b', clauseTel=tel'}
          reportSDoc "tc.reconstruct" 50
                   $ "getDefinition reconstructed clause:" <+> pretty c'
          return c'

        reconsTel :: Telescope -> TCM Telescope
        reconsTel :: Tele (Dom Type) -> TCM (Tele (Dom Type))
reconsTel Tele (Dom Type)
EmptyTel = Tele (Dom Type) -> TCM (Tele (Dom Type))
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Tele (Dom Type)
forall a. Tele a
EmptyTel
        reconsTel (ExtendTel Dom Type
_ NoAbs{}) = TCM (Tele (Dom Type))
forall a. HasCallStack => a
__IMPOSSIBLE__
        reconsTel (ExtendTel (d :: Dom Type
d@Dom{unDom :: forall t e. Dom' t e -> e
unDom=Type
t}) ds :: Abs (Tele (Dom Type))
ds@Abs{unAbs :: forall a. Abs a -> a
unAbs=Tele (Dom Type)
ts}) = do
           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 Type
d{unDom=t}
           ts' <- addContext d' $ reconsTel ts
           return $ ExtendTel d' ds{unAbs=ts'}


    setDirty :: UnquoteM ()
    setDirty :: ReaderT
  Context
  (StateT
     UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
  ()
setDirty = (UnquoteState -> UnquoteState)
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((Dirty -> Dirty) -> UnquoteState -> UnquoteState
forall b c d. (b -> c) -> (b, d) -> (c, d)
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 -> UnquoteM Term
tcDeclareDef (Arg ArgInfo
i QName
x) Type
a = UnquoteM Term -> UnquoteM Term
forall a. UnquoteM a -> UnquoteM a
inOriginalContext (UnquoteM Term -> UnquoteM Term) -> UnquoteM Term -> UnquoteM Term
forall a b. (a -> b) -> a -> b
$ do
      ReaderT
  Context
  (StateT
     UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
  ()
setDirty
      Bool
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     ()
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     ()
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 (TCMT IO))))
   ()
 -> ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      ())
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     ()
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     ()
forall a b. (a -> b) -> a -> b
$ TCMT IO ()
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     ()
forall a.
TCM a
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCMT IO ()
 -> ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      ())
-> TCMT IO ()
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (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 ())
-> (Doc -> TypeError) -> Doc -> TCMT IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError (Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<
        TCMT IO Doc
"Cannot declare hidden function" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
x
      [QName]
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [QName
x]
      TCMT IO Term -> UnquoteM Term
forall a.
TCM a
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCMT IO Term -> UnquoteM Term) -> TCMT IO Term -> UnquoteM Term
forall a b. (a -> b) -> a -> b
$ do
        [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
alwaysReportSDoc [Char]
"tc.unquote.decl" Int
10 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
          [ TCMT IO Doc
"declare" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
x TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":"
          , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Type -> TCMT IO Doc
forall r (m :: * -> *).
(ToAbstract r, PrettyTCM (AbsOfRef r), MonadPretty m,
 MonadError TCErr m) =>
r -> m Doc
prettyR Type
a
          ]
        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
        alreadyDefined <- isRight <$> getConstInfo' x
        when alreadyDefined $ genericError $ "Multiple declarations of " ++ prettyShow x
        addConstant' x i x a =<< emptyFunction
        when (isInstance i) $ addTypedInstance x a
        primUnitUnit

    tcDeclarePostulate :: Arg QName -> R.Type -> UnquoteM Term
    tcDeclarePostulate :: Arg QName -> Type -> UnquoteM Term
tcDeclarePostulate (Arg ArgInfo
i QName
x) Type
a = UnquoteM Term -> UnquoteM Term
forall a. UnquoteM a -> UnquoteM a
inOriginalContext (UnquoteM Term -> UnquoteM Term) -> UnquoteM Term -> UnquoteM Term
forall a b. (a -> b) -> a -> b
$ do
      clo <- ReaderT
  Context
  (StateT
     UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
  CommandLineOptions
forall (m :: * -> *). HasOptions m => m CommandLineOptions
commandLineOptions
      when (Lens.getSafeMode clo) $ liftTCM $ typeError . GenericDocError =<<
        "Cannot postulate '" <+> prettyTCM x <+> ":" <+> prettyR a <+> "' with safe flag"
      setDirty
      when (hidden i) $ liftTCM $ typeError . GenericDocError =<<
        "Cannot declare hidden function" <+> prettyTCM x
      tell [x]
      liftTCM $ do
        alwaysReportSDoc "tc.unquote.decl" 10 $ sep
          [ "declare Postulate" <+> prettyTCM x <+> ":"
          , nest 2 $ prettyR a
          ]
        a <- locallyReduceAllDefs $ isType_ =<< toAbstract_ a
        alreadyDefined <- isRight <$> getConstInfo' x
        when alreadyDefined $ genericError $ "Multiple declarations of " ++ prettyShow x
        addConstant' x i x a defaultAxiom
        when (isInstance i) $ addTypedInstance x a
        primUnitUnit

    -- A datatype is expected to be declared with a function type.
    -- The second argument indicates how many preceding types are parameters.
    tcDeclareData :: QName -> Integer -> R.Type -> UnquoteM Term
    tcDeclareData :: QName -> Integer -> Type -> UnquoteM Term
tcDeclareData QName
x Integer
npars Type
t = UnquoteM Term -> UnquoteM Term
forall a. UnquoteM a -> UnquoteM a
inOriginalContext (UnquoteM Term -> UnquoteM Term) -> UnquoteM Term -> UnquoteM Term
forall a b. (a -> b) -> a -> b
$ do
      ReaderT
  Context
  (StateT
     UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
  ()
setDirty
      [QName]
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [QName
x]
      TCMT IO Term -> UnquoteM Term
forall a.
TCM a
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCMT IO Term -> UnquoteM Term) -> TCMT IO Term -> UnquoteM Term
forall a b. (a -> b) -> a -> b
$ do
        [Char] -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
alwaysReportSDoc [Char]
"tc.unquote.decl" Int
10 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
          [ TCMT IO Doc
"declare Data" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
x TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":"
          , Int -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Type -> TCMT IO Doc
forall r (m :: * -> *).
(ToAbstract r, PrettyTCM (AbsOfRef r), MonadPretty m,
 MonadError TCErr m) =>
r -> m Doc
prettyR Type
t
          ]
        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
        when alreadyDefined $ genericError $ "Multiple declarations of " ++ prettyShow x
        e <- toAbstract_ t
        -- The type to be checked with @checkSig@ is without parameters.
        let (tel, e') = splitPars (fromInteger npars) e
        ac <- asksTC (^. lensIsAbstract)
        let defIn = 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
PublicAccess IsAbstract
ac Range
forall a. Range' a
noRange
        checkSig DataName defIn defaultErased x
          (A.GeneralizeTel Map.empty tel) e'
        primUnitUnit

    tcDefineData :: QName -> [(QName, (Quantity, R.Type))] -> UnquoteM Term
    tcDefineData :: QName -> [(QName, (Quantity, Type))] -> UnquoteM Term
tcDefineData QName
x [(QName, (Quantity, Type))]
cs = UnquoteM Term -> UnquoteM Term
forall a. UnquoteM a -> UnquoteM a
inOriginalContext (UnquoteM Term -> UnquoteM Term) -> UnquoteM Term -> UnquoteM Term
forall a b. (a -> b) -> a -> b
$ (ReaderT
  Context
  (StateT
     UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
  ()
setDirty ReaderT
  Context
  (StateT
     UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
  ()
-> UnquoteM Term -> UnquoteM Term
forall a b.
ReaderT
  Context
  (StateT
     UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
  a
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     b
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>>) (UnquoteM Term -> UnquoteM Term) -> UnquoteM Term -> UnquoteM Term
forall a b. (a -> b) -> a -> b
$ TCMT IO Term -> UnquoteM Term
forall a.
TCM a
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCMT IO Term -> UnquoteM Term) -> TCMT IO Term -> UnquoteM Term
forall a b. (a -> b) -> a -> b
$ do
      TCMT IO (Either SigError Definition)
-> (SigError -> TCMT IO Term)
-> (Definition -> TCMT IO Term)
-> TCMT IO Term
forall (m :: * -> *) a b c.
Monad m =>
m (Either a b) -> (a -> m c) -> (b -> m c) -> m c
caseEitherM (QName -> TCMT IO (Either SigError Definition)
forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Either SigError Definition)
getConstInfo' QName
x)
        (TCMT IO Term -> SigError -> TCMT IO Term
forall a b. a -> b -> a
const (TCMT IO Term -> SigError -> TCMT IO Term)
-> TCMT IO Term -> SigError -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ [Char] -> TCMT IO Term
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
[Char] -> m a
genericError ([Char] -> TCMT IO Term) -> [Char] -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ [Char]
"Missing declaration for " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ QName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow QName
x) ((Definition -> TCMT IO Term) -> TCMT IO Term)
-> (Definition -> TCMT IO Term) -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ \Definition
def -> do
        npars <- case Definition -> Defn
theDef Definition
def of
                   DataOrRecSig Int
n -> Int -> TCMT IO Int
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Int
n
                   Defn
_              -> [Char] -> TCMT IO Int
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
[Char] -> m a
genericError ([Char] -> TCMT IO Int) -> [Char] -> TCMT IO Int
forall a b. (a -> b) -> a -> b
$ QName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow QName
x [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
                     [Char]
" is not declared as a datatype or record, or it already has a definition."

        -- For some reasons, reifying parameters and adding them to the context via
        -- `addContext` before `toAbstract_` is different from substituting the type after
        -- `toAbstract_, so some dummy parameters are added and removed later.
        es <- mapM (toAbstract_ . addDummy npars . snd . snd) cs
        alwaysReportSDoc "tc.unquote.def" 10 $ vcat $
          [ "declaring constructors of" <+> prettyTCM x <+> ":" ] ++ map prettyA es

        -- Translate parameters from internal definitions back to abstract syntax.
        t   <- instantiateFull . defType =<< instantiateDef def
        tel <- reify =<< theTel <$> telViewUpTo npars t

        es' <- case mapM (uncurry (substNames' tel) . splitPars npars) es of
                 Maybe [Expr]
Nothing -> [Char] -> TCMT IO [Expr]
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
[Char] -> m a
genericError ([Char] -> TCMT IO [Expr]) -> [Char] -> TCMT IO [Expr]
forall a b. (a -> b) -> a -> b
$ [Char]
"Number of parameters doesn't match!"
                 Just [Expr]
es -> [Expr] -> TCMT IO [Expr]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return [Expr]
es

        ac <- asksTC (^. lensIsAbstract)
        let 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
PublicAccess IsAbstract
ac Range
forall a. Range' a
noRange
            conNames = ((QName, (Quantity, Type)) -> QName)
-> [(QName, (Quantity, Type))] -> [QName]
forall a b. (a -> b) -> [a] -> [b]
map (QName, (Quantity, Type)) -> QName
forall a b. (a, b) -> a
fst [(QName, (Quantity, Type))]
cs
            conQuantities = ((QName, (Quantity, Type)) -> Quantity)
-> [(QName, (Quantity, Type))] -> [Quantity]
forall a b. (a -> b) -> [a] -> [b]
map ((Quantity, Type) -> Quantity
forall a b. (a, b) -> a
fst ((Quantity, Type) -> Quantity)
-> ((QName, (Quantity, Type)) -> (Quantity, Type))
-> (QName, (Quantity, Type))
-> Quantity
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (QName, (Quantity, Type)) -> (Quantity, Type)
forall a b. (a, b) -> b
snd) [(QName, (Quantity, Type))]
cs
            toAxiom QName
c Quantity
q Expr
e = KindOfName
-> DefInfo' Expr
-> ArgInfo
-> Maybe [Occurrence]
-> QName
-> Expr
-> Declaration
A.Axiom KindOfName
ConName DefInfo' Expr
i (Quantity -> ArgInfo -> ArgInfo
forall a. LensQuantity a => Quantity -> a -> a
setQuantity Quantity
q ArgInfo
defaultArgInfo) Maybe [Occurrence]
forall a. Maybe a
Nothing QName
c Expr
e
            as = (QName -> Quantity -> Expr -> Declaration)
-> [QName] -> [Quantity] -> [Expr] -> [Declaration]
forall a b c d. (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
zipWith3 QName -> Quantity -> Expr -> Declaration
toAxiom [QName]
conNames [Quantity]
conQuantities [Expr]
es'
            lams = (TypedBinding -> LamBinding) -> [TypedBinding] -> [LamBinding]
forall a b. (a -> b) -> [a] -> [b]
map (\case {A.TBind Range
_ TypedBindingInfo
tac (NamedArg Binder
b :| []) Expr
_ -> TacticAttribute -> NamedArg Binder -> LamBinding
A.DomainFree (TypedBindingInfo -> TacticAttribute
tbTacticAttr TypedBindingInfo
tac) NamedArg Binder
b
                              ;TypedBinding
_ -> LamBinding
forall a. HasCallStack => a
__IMPOSSIBLE__ }) [TypedBinding]
tel
        alwaysReportSDoc "tc.unquote.def" 10 $ vcat $
          [ "checking datatype: " <+> prettyTCM x <+> " with constructors:"
          , nest 2 (vcat (map prettyTCM conNames))
          ]
        checkDataDef i x YesUniverseCheck (A.DataDefParams Set.empty lams) as
        primUnitUnit
      where
        addDummy :: Int -> R.Type -> R.Type
        addDummy :: Int -> Type -> Type
addDummy Int
0 Type
t = Type
t
        addDummy Int
n Type
t = Dom Type -> Abs Type -> Type
R.Pi (Type -> Dom Type
forall a. a -> Dom a
defaultDom (Sort -> Type
R.Sort (Sort -> Type) -> Sort -> Type
forall a b. (a -> b) -> a -> b
$ Integer -> Sort
R.LitS Integer
0)) ([Char] -> Type -> Abs Type
forall a. [Char] -> a -> Abs a
R.Abs [Char]
"dummy" (Type -> Abs Type) -> Type -> Abs Type
forall a b. (a -> b) -> a -> b
$ Int -> Type -> Type
addDummy (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Type
t)

        substNames' :: [A.TypedBinding] -> [A.TypedBinding] -> A.Expr -> Maybe A.Expr
        substNames' :: [TypedBinding] -> [TypedBinding] -> Expr -> Maybe Expr
substNames' (TypedBinding
a : [TypedBinding]
as) (TypedBinding
b : [TypedBinding]
bs) Expr
e = do
          let (A.TBind Range
_ TypedBindingInfo
_ (NamedArg Binder
na :| [NamedArg Binder]
_) Expr
expra) = TypedBinding
a
              (A.TBind Range
_ TypedBindingInfo
_ (NamedArg Binder
nb :| [NamedArg Binder]
_) Expr
exprb) = TypedBinding
b
              getName :: NamedArg Binder -> Name
getName NamedArg Binder
n = BindName -> Name
A.unBind (BindName -> Name) -> (Binder -> BindName) -> Binder -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Binder -> BindName
forall a. Binder' a -> a
A.binderName (Binder -> Name) -> Binder -> Name
forall a b. (a -> b) -> a -> b
$ NamedArg Binder -> Binder
forall a. NamedArg a -> a
namedArg NamedArg Binder
n
          e' <- [TypedBinding] -> [TypedBinding] -> Expr -> Maybe Expr
substNames' [TypedBinding]
as [TypedBinding]
bs Expr
e
          return $ mapExpr (substName (getName na) (getName nb)) e'
          where
            -- Substitute @Var x@ for @Var y@ in an @Expr@.
            substName :: Name -> Name -> (A.Expr -> A.Expr)
            substName :: Name -> Name -> Expr -> Expr
substName Name
x Name
y e :: Expr
e@(A.Var Name
n)
                    | Name
y Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
n    = Name -> Expr
A.Var Name
x
                    | Bool
otherwise = Expr
e
            substName Name
_ Name
_ Expr
e = Expr
e
        substNames' [] [] Expr
e = Expr -> Maybe Expr
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
e
        substNames' [TypedBinding]
_ [TypedBinding]
_ Expr
_ = Maybe Expr
forall a. Maybe a
Nothing

    tcDefineFun :: QName -> [R.Clause] -> UnquoteM Term
    tcDefineFun :: QName -> [Clause] -> UnquoteM Term
tcDefineFun QName
x [Clause]
cs = UnquoteM Term -> UnquoteM Term
forall a. UnquoteM a -> UnquoteM a
inOriginalContext (UnquoteM Term -> UnquoteM Term) -> UnquoteM Term -> UnquoteM Term
forall a b. (a -> b) -> a -> b
$ (ReaderT
  Context
  (StateT
     UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
  ()
setDirty ReaderT
  Context
  (StateT
     UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
  ()
-> UnquoteM Term -> UnquoteM Term
forall a b.
ReaderT
  Context
  (StateT
     UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
  a
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     b
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>>) (UnquoteM Term -> UnquoteM Term) -> UnquoteM Term -> UnquoteM Term
forall a b. (a -> b) -> a -> b
$ TCMT IO Term -> UnquoteM Term
forall a.
TCM a
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCMT IO Term -> UnquoteM Term) -> TCMT IO Term -> UnquoteM 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
$
        [Char] -> TCMT IO ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
[Char] -> m a
genericError ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [Char]
"Missing declaration for " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ QName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow QName
x
      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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (QNamed Clause -> TCMT IO Clause
QNamed Clause -> TCMT IO (AbsOfRef (QNamed 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
      alwaysReportSDoc "tc.unquote.def" 10 $ vcat $ map prettyA cs
      let accessDontCare = a
forall a. HasCallStack => a
__IMPOSSIBLE__  -- or ConcreteDef, value not looked at
      ac <- asksTC (^. lensIsAbstract)     -- Issue #4012, respect AbstractMode
      oc <- asksTC (^. lensIsOpaque)       -- Issue #6959, respect current opaque block
      let
        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
        i = DefInfo' Expr
i' { Info.defOpaque = oc }
      locallyReduceAllDefs $ checkFunDef i x cs
      primUnitUnit

    tcPragmaForeign :: Text -> Text -> TCM Term
    tcPragmaForeign :: ExeName -> ExeName -> TCMT IO Term
tcPragmaForeign ExeName
backend ExeName
code = do
      [Char] -> [Char] -> TCMT IO ()
addForeignCode (ExeName -> [Char]
T.unpack ExeName
backend) (ExeName -> [Char]
T.unpack ExeName
code)
      TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primUnitUnit

    tcPragmaCompile :: Text -> QName -> Text -> TCM Term
    tcPragmaCompile :: ExeName -> QName -> ExeName -> TCMT IO Term
tcPragmaCompile ExeName
backend QName
name ExeName
code = do
      (Signature -> Signature) -> TCMT IO ()
forall (m :: * -> *).
MonadTCState m =>
(Signature -> Signature) -> m ()
modifySignature ((Signature -> Signature) -> TCMT IO ())
-> (Signature -> Signature) -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ QName -> (Definition -> Definition) -> Signature -> Signature
updateDefinition QName
name ((Definition -> Definition) -> Signature -> Signature)
-> (Definition -> Definition) -> Signature -> Signature
forall a b. (a -> b) -> a -> b
$
        [Char] -> CompilerPragma -> Definition -> Definition
addCompilerPragma (ExeName -> [Char]
T.unpack ExeName
backend) (CompilerPragma -> Definition -> Definition)
-> CompilerPragma -> Definition -> Definition
forall a b. (a -> b) -> a -> b
$ Range -> [Char] -> CompilerPragma
CompilerPragma Range
forall a. Range' a
noRange (ExeName -> [Char]
T.unpack ExeName
code)
      TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primUnitUnit

    tcRunSpeculative :: Term -> UnquoteM Term
    tcRunSpeculative :: Term -> UnquoteM Term
tcRunSpeculative Term
mu = do
      oldState <- ReaderT
  Context
  (StateT
     UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
  TCState
forall (m :: * -> *). MonadTCState m => m TCState
getTC
      u <- reduce =<< evalTCM mu
      case 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 (TCMT IO))))
     ()
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     ()
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 (TCMT IO))))
   ()
 -> ReaderT
      Context
      (StateT
         UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
      ())
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     ()
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     ()
forall a b. (a -> b) -> a -> b
$ TCState
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     ()
forall (m :: * -> *). MonadTCState m => TCState -> m ()
putTC TCState
oldState
          Term -> UnquoteM Term
forall a.
a
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     a
forall (m :: * -> *) a. Monad m => a -> m a
return Term
x
        Term
_ -> TCMT IO Term -> UnquoteM Term
forall a.
TCM a
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCMT IO Term -> UnquoteM Term) -> TCMT IO Term -> UnquoteM 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) -> TCMT IO Doc -> TCMT IO Term
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<
          TCMT IO Doc
"Should be a pair: " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
prettyTCM Term
u

    tcGetInstances :: MetaId -> UnquoteM Term
    tcGetInstances :: MetaId -> UnquoteM Term
tcGetInstances MetaId
m = TCM (Either Blocker [Candidate])
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     (Either Blocker [Candidate])
forall a.
TCM a
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (MetaId -> TCM (Either Blocker [Candidate])
getInstanceCandidates MetaId
m) ReaderT
  Context
  (StateT
     UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
  (Either Blocker [Candidate])
-> (Either Blocker [Candidate] -> UnquoteM Term) -> UnquoteM Term
forall a b.
ReaderT
  Context
  (StateT
     UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
  a
-> (a
    -> ReaderT
         Context
         (StateT
            UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
         b)
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Left Blocker
unblock -> do
        s <- (UnquoteState -> TCState)
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     TCState
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets UnquoteState -> TCState
forall a b. (a, b) -> b
snd
        throwError (BlockedOnMeta s unblock)
      Right [Candidate]
cands -> TCMT IO Term -> UnquoteM Term
forall a.
TCM a
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCMT IO Term -> UnquoteM Term) -> TCMT IO Term -> UnquoteM Term
forall a b. (a -> b) -> a -> b
$
        TCM ([Term] -> Term)
buildList TCM ([Term] -> Term) -> TCMT IO [Term] -> TCMT IO Term
forall a b. TCMT IO (a -> b) -> TCMT IO a -> TCMT IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Candidate -> TCMT IO Term) -> [Candidate] -> TCMT IO [Term]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Term -> TCMT IO Term
quoteTerm (Term -> TCMT IO Term)
-> (Candidate -> Term) -> Candidate -> TCMT IO Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Candidate -> Term
candidateTerm) [Candidate]
cands

    tcSolveInstances :: UnquoteM Term
    tcSolveInstances :: UnquoteM Term
tcSolveInstances = TCMT IO Term -> UnquoteM Term
forall a.
TCM a
-> ReaderT
     Context
     (StateT
        UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
     a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCMT IO Term -> UnquoteM Term) -> TCMT IO Term -> UnquoteM Term
forall a b. (a -> b) -> a -> b
$ do
      Lens' TCState Bool -> (Bool -> Bool) -> TCMT IO () -> TCMT IO ()
forall a b. Lens' TCState a -> (a -> a) -> TCMT IO b -> TCMT IO b
forall (m :: * -> *) a b.
ReadTCState m =>
Lens' TCState a -> (a -> a) -> m b -> m b
locallyTCState (Bool -> f Bool) -> TCState -> f TCState
Lens' TCState Bool
stPostponeInstanceSearch (Bool -> Bool -> Bool
forall a b. a -> b -> a
const Bool
False) (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ do
        -- Steal instance constraints (TODO: not all!)
        current <- (TCEnv -> Set ProblemId) -> TCMT IO (Set ProblemId)
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Set ProblemId
envActiveProblems
        topPid  <- fromMaybe __IMPOSSIBLE__ <$> asksTC envUnquoteProblem
        let steal pc :: ProblemConstraint
pc@(PConstr Set ProblemId
pids Blocker
u Closure Constraint
c)
              | ProblemConstraint -> Bool
isInstance ProblemConstraint
pc
              , ProblemId -> Set ProblemId -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member ProblemId
topPid Set ProblemId
pids = Set ProblemId -> Blocker -> Closure Constraint -> ProblemConstraint
PConstr (Set ProblemId -> Set ProblemId -> Set ProblemId
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set ProblemId
current Set ProblemId
pids) Blocker
u Closure Constraint
c
              | Bool
otherwise              = ProblemConstraint
pc
            isInstance ProblemConstraint
c | FindInstance{} <- Closure Constraint -> Constraint
forall a. Closure a -> a
clValue (ProblemConstraint -> Closure Constraint
theConstraint ProblemConstraint
c) = Bool
True
                         | Bool
otherwise                                   = Bool
False
        modifyAwakeConstraints    $ map steal
        modifySleepingConstraints $ map steal
        wakeConstraints (wakeUpWhen_ isInstance)
        solveSomeAwakeConstraints isInstance True  -- Force solving them now!
      TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primUnitUnit

    splitPars :: Int -> A.Expr -> ([A.TypedBinding], A.Expr)
    splitPars :: Int -> Expr -> ([TypedBinding], Expr)
splitPars Int
0 Expr
e = ([] , Expr
e)
    splitPars Int
npars (A.Pi ExprInfo
_ (TypedBinding
n :| [TypedBinding]
_) Expr
e) = ([TypedBinding] -> [TypedBinding])
-> ([TypedBinding], Expr) -> ([TypedBinding], Expr)
forall b c d. (b -> c) -> (b, d) -> (c, d)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first (TypedBinding
n TypedBinding -> [TypedBinding] -> [TypedBinding]
forall a. a -> [a] -> [a]
:) (Int -> Expr -> ([TypedBinding], Expr)
splitPars (Int
npars Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Expr
e)
    splitPars Int
npars Expr
e = ([TypedBinding], Expr)
forall a. HasCallStack => a
__IMPOSSIBLE__
------------------------------------------------------------------------
-- * 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
  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
  unless allowExec $
    typeError $ GenericError "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 :: ExeName -> [ExeName] -> ExeName -> TCMT IO Term
tcExec ExeName
exe [ExeName]
args ExeName
stdIn = do
  TCMT IO ()
requireAllowExec
  exes <- CommandLineOptions -> Map ExeName [Char]
optTrustedExecutables (CommandLineOptions -> Map ExeName [Char])
-> TCMT IO CommandLineOptions -> TCMT IO (Map ExeName [Char])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO CommandLineOptions
forall (m :: * -> *). HasOptions m => m CommandLineOptions
commandLineOptions
  case Map.lookup exe exes of
    Maybe [Char]
Nothing -> ExeName -> Map ExeName [Char] -> TCMT IO Term
forall a. ExeName -> Map ExeName [Char] -> TCM a
raiseExeNotTrusted ExeName
exe Map ExeName [Char]
exes
    Just [Char]
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 a. IO a -> TCMT IO a
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
$ [Char] -> IO Bool
doesFileExist [Char]
fp) (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ ExeName -> [Char] -> TCMT IO ()
forall a. ExeName -> [Char] -> TCM a
raiseExeNotFound ExeName
exe [Char]
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 a. IO a -> TCMT IO a
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
<$> [Char] -> IO Permissions
getPermissions [Char]
fp) (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ ExeName -> [Char] -> TCMT IO ()
forall a. ExeName -> [Char] -> TCM a
raiseExeNotExecutable ExeName
exe [Char]
fp

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

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

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

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