module Agda.TypeChecking.Unquote where

import Control.Arrow          ( first, second, (&&&) )
import Control.Monad          ( (<=<), liftM2 )
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
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 Agda.TypeChecking.Constraints
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Free
import Agda.TypeChecking.Irrelevance ( workOnTypes )
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 ( getInstanceCandidates )

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.Utils.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 = forall t a. Sort' t -> a -> Type'' t a
El (Integer -> Sort
mkType Integer
0) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 = forall t a. Sort' t -> a -> Type'' t a
El (Integer -> Sort
mkType Integer
0) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primQName

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

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

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

unpackUnquoteM :: UnquoteM a -> Context -> UnquoteState -> TCM (UnquoteRes a)
unpackUnquoteM :: forall a.
UnquoteM a -> Context -> UnquoteState -> TCM (UnquoteRes a)
unpackUnquoteM UnquoteM a
m Context
cxt UnquoteState
s = forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT forall a b. (a -> b) -> a -> b
$ forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT forall a b. (a -> b) -> a -> b
$ forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (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 = forall r (m :: * -> *) a. (r -> m a) -> ReaderT r m a
ReaderT forall a b. (a -> b) -> a -> b
$ \ Context
cxt -> forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
StateT forall a b. (a -> b) -> a -> b
$ \ UnquoteState
s -> forall w (m :: * -> *) a. m (a, w) -> WriterT w m a
WriterT forall a b. (a -> b) -> a -> b
$ forall e (m :: * -> *) a. m (Either e a) -> ExceptT e m a
ExceptT 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
  Context
cxt <- forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Context
envContext
  TCState
s   <- forall (m :: * -> *). MonadTCState m => m TCState
getTC
  UnquoteRes a
z   <- forall a.
UnquoteM a -> Context -> UnquoteState -> TCM (UnquoteRes a)
unpackUnquoteM UnquoteM a
m Context
cxt (Dirty
Clean, TCState
s)
  case UnquoteRes a
z of
    Left UnquoteError
err              -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left UnquoteError
err
    Right ((a
x, UnquoteState
_), [QName]
decls) -> forall a b. b -> Either a b
Right (a
x, [QName]
decls) forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ forall {m :: * -> *}.
(HasConstInfo m, ReadTCState m, MonadError TCErr m) =>
QName -> m ()
isDefined [QName]
decls
  where
    isDefined :: QName -> m ()
isDefined QName
x = do
      Defn
def <- Definition -> Defn
theDef forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
x
      case Defn
def of
        Function{funClauses :: Defn -> [Clause]
funClauses = []} -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
[Char] -> m a
genericError forall a b. (a -> b) -> a -> b
$ [Char]
"Missing definition for " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow QName
x
        Defn
_       -> 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 = forall a.
(Context -> UnquoteState -> TCM (UnquoteRes a)) -> UnquoteM a
packUnquoteM forall a b. (a -> b) -> a -> b
$ \ Context
cxt UnquoteState
s -> TCM (UnquoteRes a) -> TCM (UnquoteRes b)
f (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 = forall a.
(Context -> UnquoteState -> TCM (UnquoteRes a)) -> UnquoteM a
packUnquoteM forall a b. (a -> b) -> a -> b
$ \ Context
cxt UnquoteState
s -> TCM (UnquoteRes a) -> TCM (UnquoteRes b) -> TCM (UnquoteRes c)
f (forall a.
UnquoteM a -> Context -> UnquoteState -> TCM (UnquoteRes a)
unpackUnquoteM UnquoteM a
m1 Context
cxt UnquoteState
s) (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 =
  forall a.
(Context -> UnquoteState -> TCM (UnquoteRes a)) -> UnquoteM a
packUnquoteM forall a b. (a -> b) -> a -> b
$ \ Context
cxt UnquoteState
s ->
    forall (tcm :: * -> *) a.
MonadTCEnv tcm =>
(Context -> Context) -> tcm a -> tcm a
unsafeModifyContext (forall a b. a -> b -> a
const Context
cxt) forall a b. (a -> b) -> a -> b
$ forall a.
UnquoteM a -> Context -> UnquoteState -> TCM (UnquoteRes a)
unpackUnquoteM UnquoteM a
m Context
cxt UnquoteState
s

isCon :: ConHead -> TCM Term -> UnquoteM Bool
isCon :: ConHead -> TCM Term -> UnquoteM Bool
isCon ConHead
con TCM Term
tm = do Term
t <- forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM TCM Term
tm
                  case Term
t of
                    Con ConHead
con' ConInfo
_ Elims
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return (ConHead
con forall a. Eq a => a -> a -> Bool
== ConHead
con')
                    Term
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

isDef :: QName -> TCM Term -> UnquoteM Bool
isDef :: QName -> TCM Term -> UnquoteM Bool
isDef QName
f TCM Term
tm = Term -> Bool
loop forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM TCM Term
tm
  where
    loop :: Term -> Bool
loop (Def QName
g Elims
_) = QName
f forall a. Eq a => a -> a -> Bool
== QName
g
    loop (Lam ArgInfo
_ Abs Term
b) = Term -> Bool
loop forall a b. (a -> b) -> a -> b
$ forall a. Abs a -> a
unAbs Abs Term
b
    loop Term
_         = Bool
False

reduceQuotedTerm :: Term -> UnquoteM Term
reduceQuotedTerm :: Term -> UnquoteM Term
reduceQuotedTerm Term
t = forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
locallyReduceAllDefs forall a b. (a -> b) -> a -> b
$ do
  forall t (m :: * -> *) a.
(Reduce t, IsMeta t, MonadReduce m) =>
t -> (Blocker -> t -> m a) -> (NotBlocked -> t -> m a) -> m a
ifBlocked Term
t {-then-} (\ Blocker
m Term
_ -> do TCState
s <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets forall a b. (a, b) -> b
snd; forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ TCState -> Blocker -> UnquoteError
BlockedOnMeta TCState
s Blocker
m)
              {-else-} (\ NotBlocked
_ Term
t -> 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 | forall a. LensHiding a => a -> Bool
visible Arg Term
a Bool -> Bool -> Bool
&& forall a. LensRelevance a => a -> Bool
isRelevant Arg Term
a =
    forall a. Unquote a => Term -> UnquoteM a
unquote forall a b. (a -> b) -> a -> b
$ forall e. Arg e -> e
unArg Arg Term
a
unquoteN Arg Term
a = forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError 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 = forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM m Bool
mb m a
mx forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
choice [(m Bool, m a)]
mxs m a
dflt

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

ensureCon :: QName -> UnquoteM QName
ensureCon :: QName -> UnquoteM QName
ensureCon QName
x = do
  Defn
i <- forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (forall a b. a -> b -> a
const Defn
defaultAxiom) Definition -> Defn
theDef forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Either SigError Definition)
getConstInfo' QName
x  -- for recursive unquoteDecl
  case Defn
i of
    Constructor{} -> forall (m :: * -> *) a. Monad m => a -> m a
return QName
x
    Defn
_ -> do
      Doc
def <- forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTermDef
      Doc
con <- forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTermCon
      forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ QName -> [Char] -> [Char] -> UnquoteError
DefInsteadOfCon QName
x (forall a. Show a => a -> [Char]
show Doc
def) (forall a. Show a => a -> [Char]
show Doc
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  <- forall a. Pretty a => a -> [Char]
prettyShow (QName -> Name
qnameName QName
d),
        Just Char
lc <- Char -> Maybe Char
reallyToLower Char
c,
        Bool -> Bool
not (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 forall a. Eq a => a -> a -> Bool
/= Char
lc = forall a. a -> Maybe a
Just Char
lc
      | Bool
otherwise        = forall a. Maybe a
Nothing
      where lc :: Char
lc = Char -> Char
toLower Char
c

-- TODO: reflect Cohesion
instance Unquote Modality where
  unquote :: Term -> UnquoteM Modality
unquote Term
t = do
    Term
t <- Term -> UnquoteM Term
reduceQuotedTerm Term
t
    case Term
t of
      Con ConHead
c ConInfo
_ Elims
es | Just [Arg Term
r,Arg Term
q] <- forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es ->
        forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
choice
          [(ConHead
c ConHead -> TCM Term -> UnquoteM Bool
`isCon` forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primModalityConstructor,
              Relevance -> Quantity -> Cohesion -> Modality
Modality forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
r
                       forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
q
                       forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure Cohesion
defaultCohesion)]
          forall a. HasCallStack => a
__IMPOSSIBLE__
      Con ConHead
c ConInfo
_ Elims
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__
      Term
_ -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError 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
    Term
t <- Term -> UnquoteM Term
reduceQuotedTerm Term
t
    case Term
t of
      Con ConHead
c ConInfo
_ Elims
es | Just [Arg Term
h,Arg Term
m] <- forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es ->
        forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
choice
          [(ConHead
c ConHead -> TCM Term -> UnquoteM Bool
`isCon` forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primArgArgInfo,
              Hiding
-> Modality -> Origin -> FreeVariables -> Annotation -> ArgInfo
ArgInfo forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
h
                      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
m
                      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure Origin
Reflected
                      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure FreeVariables
unknownFreeVariables
                      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure Annotation
defaultAnnotation)]
          forall a. HasCallStack => a
__IMPOSSIBLE__
      Con ConHead
c ConInfo
_ Elims
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__
      Term
_ -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError 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
    Term
t <- Term -> UnquoteM Term
reduceQuotedTerm Term
t
    case Term
t of
      Con ConHead
c ConInfo
_ Elims
es | Just [Arg Term
info,Arg Term
x] <- forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es ->
        forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
choice
          [(ConHead
c ConHead -> TCM Term -> UnquoteM Bool
`isCon` forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primArgArg, forall e. ArgInfo -> e -> Arg e
Arg forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
info forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
x)]
          forall a. HasCallStack => a
__IMPOSSIBLE__
      Con ConHead
c ConInfo
_ Elims
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__
      Term
_ -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError 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 = forall a. Arg a -> Elim' a
R.Apply forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Unquote a => Term -> UnquoteM a
unquote Term
t

instance Unquote Bool where
  unquote :: Term -> UnquoteM Bool
unquote Term
t = do
    Term
t <- Term -> UnquoteM Term
reduceQuotedTerm Term
t
    case Term
t of
      Con ConHead
c ConInfo
_ [] ->
        forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
choice [ (ConHead
c ConHead -> TCM Term -> UnquoteM Bool
`isCon` forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primTrue,  forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True)
               , (ConHead
c ConHead -> TCM Term -> UnquoteM Bool
`isCon` forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primFalse, forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False) ]
               forall a. HasCallStack => a
__IMPOSSIBLE__
      Term
_ -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError 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
    Term
t <- Term -> UnquoteM Term
reduceQuotedTerm Term
t
    case Term
t of
      Lit (LitNat Integer
n) -> forall (m :: * -> *) a. Monad m => a -> m a
return Integer
n
      Term
_ -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError 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
    Term
t <- Term -> UnquoteM Term
reduceQuotedTerm Term
t
    case Term
t of
      Lit (LitWord64 Word64
n) -> forall (m :: * -> *) a. Monad m => a -> m a
return Word64
n
      Term
_ -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError 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
    Term
t <- Term -> UnquoteM Term
reduceQuotedTerm Term
t
    case Term
t of
      Lit (LitFloat Double
x) -> forall (m :: * -> *) a. Monad m => a -> m a
return Double
x
      Term
_ -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError 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
    Term
t <- Term -> UnquoteM Term
reduceQuotedTerm Term
t
    case Term
t of
      Lit (LitChar Char
x) -> forall (m :: * -> *) a. Monad m => a -> m a
return Char
x
      Term
_ -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError 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
    Term
t <- Term -> UnquoteM Term
reduceQuotedTerm Term
t
    case Term
t of
      Lit (LitString ExeName
x) -> forall (m :: * -> *) a. Monad m => a -> m a
return ExeName
x
      Term
_ -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Unquote a => Term -> UnquoteM a
unquote Term
x

unquoteNString :: Arg Term -> UnquoteM Text
unquoteNString :: Arg Term -> UnquoteM ExeName
unquoteNString = 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)  = forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
s
  prettyTCM (TermPart Expr
t) = forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Expr
t
  prettyTCM (PattPart Pattern
p) = forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Pattern
p
  prettyTCM (NamePart QName
x) = forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
x

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


instance Unquote ErrorPart where
  unquote :: Term -> UnquoteM ErrorPart
unquote Term
t = do
    Term
t <- Term -> UnquoteM Term
reduceQuotedTerm Term
t
    case Term
t of
      Con ConHead
c ConInfo
_ Elims
es | Just [Arg Term
x] <- forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es ->
        forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
choice [ (ConHead
c ConHead -> TCM Term -> UnquoteM Bool
`isCon` forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaErrorPartString, [Char] -> ErrorPart
StrPart forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExeName -> [Char]
T.unpack forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Arg Term -> UnquoteM ExeName
unquoteNString Arg Term
x)
               , (ConHead
c ConHead -> TCM Term -> UnquoteM Bool
`isCon` forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaErrorPartTerm,   Expr -> ErrorPart
TermPart forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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) forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
x :: UnquoteM R.Term)))
               , (ConHead
c ConHead -> TCM Term -> UnquoteM Bool
`isCon` forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaErrorPartPatt,   Pattern -> ErrorPart
PattPart forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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) forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
x :: UnquoteM R.Pattern)))
               , (ConHead
c ConHead -> TCM Term -> UnquoteM Bool
`isCon` forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaErrorPartName,   QName -> ErrorPart
NamePart forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
x) ]
               forall a. HasCallStack => a
__IMPOSSIBLE__
      Term
_ -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError 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
    Term
t <- Term -> UnquoteM Term
reduceQuotedTerm Term
t
    case Term
t of
      Con ConHead
c ConInfo
_ Elims
es | Just [Arg Term
x,Arg Term
xs] <- forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es ->
        forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
choice
          [(ConHead
c ConHead -> TCM Term -> UnquoteM Bool
`isCon` forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primCons, (:) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
x forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
xs)]
          forall a. HasCallStack => a
__IMPOSSIBLE__
      Con ConHead
c ConInfo
_ [] ->
        forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
choice
          [(ConHead
c ConHead -> TCM Term -> UnquoteM Bool
`isCon` forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primNil, forall (m :: * -> *) a. Monad m => a -> m a
return [])]
          forall a. HasCallStack => a
__IMPOSSIBLE__
      Con ConHead
c ConInfo
_ Elims
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__
      Term
_ -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError 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
    Term
t <- Term -> UnquoteM Term
reduceQuotedTerm Term
t
    SigmaKit{QName
ConHead
sigmaSnd :: SigmaKit -> QName
sigmaFst :: SigmaKit -> QName
sigmaCon :: SigmaKit -> ConHead
sigmaName :: SigmaKit -> QName
sigmaSnd :: QName
sigmaFst :: QName
sigmaCon :: ConHead
sigmaName :: QName
..} <- forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(HasBuiltins m, HasConstInfo m) =>
m (Maybe SigmaKit)
getSigmaKit
    case Term
t of
      Con ConHead
c ConInfo
_ Elims
es | Just [Arg Term
x,Arg Term
y] <- forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es ->
        forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
choice
          [(forall (f :: * -> *) a. Applicative f => a -> f a
pure (ConHead
c forall a. Eq a => a -> a -> Bool
== ConHead
sigmaCon), (,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
x forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
y)]
          forall a. HasCallStack => a
__IMPOSSIBLE__
      Term
_ -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ [Char] -> Term -> UnquoteError
NonCanonical [Char]
"pair" Term
t

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

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

instance Unquote Quantity where
  unquote :: Term -> UnquoteM Quantity
unquote Term
t = do
    Term
t <- Term -> UnquoteM Term
reduceQuotedTerm Term
t
    case Term
t of
      Con ConHead
c ConInfo
_ [] ->
        forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
choice
          [(ConHead
c ConHead -> TCM Term -> UnquoteM Bool
`isCon` forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primQuantityω, forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ QωOrigin -> Quantity
Quantityω QωOrigin
QωInferred)
          ,(ConHead
c ConHead -> TCM Term -> UnquoteM Bool
`isCon` forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primQuantity0, forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Q0Origin -> Quantity
Quantity0 Q0Origin
Q0Inferred)]
          forall a. HasCallStack => a
__IMPOSSIBLE__
      Con ConHead
c ConInfo
_ Elims
vs -> forall a. HasCallStack => a
__IMPOSSIBLE__
      Term
_        -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError 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
    Term
t <- Term -> UnquoteM Term
reduceQuotedTerm Term
t
    case Term
t of
      Lit (LitQName QName
x) -> forall (m :: * -> *) a. Monad m => a -> m a
return QName
x
      Term
_ -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError 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
    Term
t <- Term -> UnquoteM Term
reduceQuotedTerm Term
t
    case Term
t of
      Con ConHead
c ConInfo
_ Elims
es | Just [Arg Term
x,Arg Term
y] <- forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es ->
        forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
choice
          [(ConHead
c ConHead -> TCM Term -> UnquoteM Bool
`isCon` forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAbsAbs, forall a. [Char] -> a -> Abs a
R.Abs forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall {t :: * -> *} {a}.
(Foldable t, IsString (t a)) =>
t a -> t a
hint forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExeName -> [Char]
T.unpack forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Arg Term -> UnquoteM ExeName
unquoteNString Arg Term
x) forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
y)]
          forall a. HasCallStack => a
__IMPOSSIBLE__
      Con ConHead
c ConInfo
_ Elims
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__
      Term
_ -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError 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 (forall (t :: * -> *) a. Foldable t => t a -> Bool
null t a
x) = t a
x
                 | Bool
otherwise    = t a
"_"

instance Unquote MetaId where
  unquote :: Term -> UnquoteM MetaId
unquote Term
t = do
    Term
t <- Term -> UnquoteM Term
reduceQuotedTerm Term
t
    case Term
t of
      Lit (LitMeta TopLevelModuleName
m MetaId
x) -> forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ do
        Bool
live <- (forall a. a -> Maybe a
Just TopLevelModuleName
m forall a. Eq a => a -> a -> Bool
==) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(MonadTCEnv m, ReadTCState m) =>
m (Maybe TopLevelModuleName)
currentTopLevelModule
        forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
live forall a b. (a -> b) -> a -> b
$
            forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<
              forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep [ TCMT IO Doc
"Can't unquote stale metavariable"
                  , forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty TopLevelModuleName
m forall a. Semigroup a => a -> a -> a
<> TCMT IO Doc
"._" forall a. Semigroup a => a -> a -> a
<> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty (MetaId -> Word64
metaId MetaId
x) ]
        forall (m :: * -> *) a. Monad m => a -> m a
return MetaId
x
      Term
_ -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError 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 = forall a. Arg a -> Dom a
domFromArg forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Unquote a => Term -> UnquoteM a
unquote Term
t

instance Unquote R.Sort where
  unquote :: Term -> UnquoteM Sort
unquote Term
t = do
    Term
t <- Term -> UnquoteM Term
reduceQuotedTerm Term
t
    case Term
t of
      Con ConHead
c ConInfo
_ [] ->
        forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
choice
          [(ConHead
c ConHead -> TCM Term -> UnquoteM Bool
`isCon` forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaSortUnsupported, forall (m :: * -> *) a. Monad m => a -> m a
return Sort
R.UnknownS)]
          forall a. HasCallStack => a
__IMPOSSIBLE__
      Con ConHead
c ConInfo
_ Elims
es | Just [Arg Term
u] <- forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es ->
        forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
choice
          [ (ConHead
c ConHead -> TCM Term -> UnquoteM Bool
`isCon` forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaSortSet, Type -> Sort
R.SetS forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
u)
          , (ConHead
c ConHead -> TCM Term -> UnquoteM Bool
`isCon` forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaSortLit, Integer -> Sort
R.LitS forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
u)
          , (ConHead
c ConHead -> TCM Term -> UnquoteM Bool
`isCon` forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaSortProp, Type -> Sort
R.PropS forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
u)
          , (ConHead
c ConHead -> TCM Term -> UnquoteM Bool
`isCon` forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaSortPropLit, Integer -> Sort
R.PropLitS forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
u)
          , (ConHead
c ConHead -> TCM Term -> UnquoteM Bool
`isCon` forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaSortInf, Integer -> Sort
R.InfS forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
u)
          ]
          forall a. HasCallStack => a
__IMPOSSIBLE__
      Con ConHead
c ConInfo
_ Elims
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__
      Term
_ -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError 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
    Term
t <- Term -> UnquoteM Term
reduceQuotedTerm Term
t
    case Term
t of
      Con ConHead
c ConInfo
_ Elims
es | Just [Arg Term
x] <- forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es ->
        forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
choice
          [ (ConHead
c ConHead -> TCM Term -> UnquoteM Bool
`isCon` forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaLitNat,    Integer -> Literal
LitNat    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
x)
          , (ConHead
c ConHead -> TCM Term -> UnquoteM Bool
`isCon` forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaLitFloat,  Double -> Literal
LitFloat  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
x)
          , (ConHead
c ConHead -> TCM Term -> UnquoteM Bool
`isCon` forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaLitChar,   Char -> Literal
LitChar   forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
x)
          , (ConHead
c ConHead -> TCM Term -> UnquoteM Bool
`isCon` forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaLitString, ExeName -> Literal
LitString forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Arg Term -> UnquoteM ExeName
unquoteNString Arg Term
x)
          , (ConHead
c ConHead -> TCM Term -> UnquoteM Bool
`isCon` forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaLitQName,  QName -> Literal
LitQName  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
x)
          , (ConHead
c ConHead -> TCM Term -> UnquoteM Bool
`isCon` forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaLitMeta,
             TopLevelModuleName -> MetaId -> Literal
LitMeta
               forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(MonadTCEnv m, ReadTCState m) =>
m (Maybe TopLevelModuleName)
currentTopLevelModule)
               forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
x)
          ]
          forall a. HasCallStack => a
__IMPOSSIBLE__
      Con ConHead
c ConInfo
_ Elims
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__
      Term
_ -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ [Char] -> Term -> UnquoteError
NonCanonical [Char]
"literal" Term
t

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

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

      Con ConHead
c ConInfo
_ Elims
es | Just [Arg Term
x, Arg Term
y] <- forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es ->
        forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
choice
          [ (ConHead
c ConHead -> TCM Term -> UnquoteM Bool
`isCon` forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTermVar,     Int -> Elims -> Type
R.Var     forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall a. Num a => Integer -> a
fromInteger forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
x) forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
y)
          , (ConHead
c ConHead -> TCM Term -> UnquoteM Bool
`isCon` forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTermCon,     QName -> Elims -> Type
R.Con     forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (QName -> UnquoteM QName
ensureCon forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
x) forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
y)
          , (ConHead
c ConHead -> TCM Term -> UnquoteM Bool
`isCon` forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTermDef,     QName -> Elims -> Type
R.Def     forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (QName -> UnquoteM QName
ensureDef forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
x) forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
y)
          , (ConHead
c ConHead -> TCM Term -> UnquoteM Bool
`isCon` forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTermMeta,    MetaId -> Elims -> Type
R.Meta    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
x forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
y)
          , (ConHead
c ConHead -> TCM Term -> UnquoteM Bool
`isCon` forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTermLam,     Hiding -> Abs Type -> Type
R.Lam     forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
x forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
y)
          , (ConHead
c ConHead -> TCM Term -> UnquoteM Bool
`isCon` forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTermPi,      Dom Type -> Abs Type -> Type
mkPi      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
x forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
y)
          , (ConHead
c ConHead -> TCM Term -> UnquoteM Bool
`isCon` forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTermExtLam,  List1 Clause -> Elims -> Type
R.ExtLam  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall a. List1 a -> [a] -> List1 a
List1.fromListSafe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
x) forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
y)
          ]
          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 (forall a. [Char] -> a -> Abs a
R.Abs (Type -> [Char]
pickName (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{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
      Lit{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
      Term
_ -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ [Char] -> Term -> UnquoteError
NonCanonical [Char]
"term" Term
t

instance Unquote R.Pattern where
  unquote :: Term -> UnquoteM Pattern
unquote Term
t = do
    Term
t <- Term -> UnquoteM Term
reduceQuotedTerm Term
t
    case Term
t of
      Con ConHead
c ConInfo
_ Elims
es | Just [Arg Term
x] <- forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es ->
        forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
choice
          [ (ConHead
c ConHead -> TCM Term -> UnquoteM Bool
`isCon` forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaPatVar,    Int -> Pattern
R.VarP    forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Num a => Integer -> a
fromInteger forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
x)
          , (ConHead
c ConHead -> TCM Term -> UnquoteM Bool
`isCon` forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaPatAbsurd, Int -> Pattern
R.AbsurdP forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Num a => Integer -> a
fromInteger forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
x)
          , (ConHead
c ConHead -> TCM Term -> UnquoteM Bool
`isCon` forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaPatDot,    Type -> Pattern
R.DotP  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
x)
          , (ConHead
c ConHead -> TCM Term -> UnquoteM Bool
`isCon` forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaPatProj,   QName -> Pattern
R.ProjP forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
x)
          , (ConHead
c ConHead -> TCM Term -> UnquoteM Bool
`isCon` forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaPatLit,    Literal -> Pattern
R.LitP  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
x) ]
          forall a. HasCallStack => a
__IMPOSSIBLE__
      Con ConHead
c ConInfo
_ Elims
es | Just [Arg Term
x, Arg Term
y] <- forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es ->
        forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
choice
          [ (ConHead
c ConHead -> TCM Term -> UnquoteM Bool
`isCon` forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaPatCon, QName -> [Arg Pattern] -> Pattern
R.ConP forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
x forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
y) ]
          forall a. HasCallStack => a
__IMPOSSIBLE__
      Con ConHead
c ConInfo
_ Elims
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__
      Term
_ -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError 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
    Term
t <- Term -> UnquoteM Term
reduceQuotedTerm Term
t
    case Term
t of
      Con ConHead
c ConInfo
_ Elims
es | Just [Arg Term
x, Arg Term
y] <- forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es ->
        forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
choice
          [ (ConHead
c ConHead -> TCM Term -> UnquoteM Bool
`isCon` forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaClauseAbsurd, [(ExeName, Arg Type)] -> [Arg Pattern] -> Clause
R.AbsurdClause forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
x forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
y) ]
          forall a. HasCallStack => a
__IMPOSSIBLE__
      Con ConHead
c ConInfo
_ Elims
es | Just [Arg Term
x, Arg Term
y, Arg Term
z] <- forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es ->
        forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
choice
          [ (ConHead
c ConHead -> TCM Term -> UnquoteM Bool
`isCon` forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaClauseClause, [(ExeName, Arg Type)] -> [Arg Pattern] -> Type -> Clause
R.Clause forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
x forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
y forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. Unquote a => Arg Term -> UnquoteM a
unquoteN Arg Term
z) ]
          forall a. HasCallStack => a
__IMPOSSIBLE__
      Con ConHead
c ConInfo
_ Elims
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__
      Term
_ -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError 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
  Term
qhole <- forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ Term -> TCM Term
quoteTerm Term
hole
  Term -> UnquoteM Term
evalTCM (Term
m forall t. Apply t => t -> [Arg Term] -> t
`apply` [forall a. a -> Arg a
defaultArg Term
qhole])

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

  case Term
v of
    I.Def QName
f [] ->
      forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
choice [ (QName
f QName -> TCM Term -> UnquoteM Bool
`isDef` forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMGetContext,       UnquoteM Term
tcGetContext)
             , (QName
f QName -> TCM Term -> UnquoteM Bool
`isDef` forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMCommit,           UnquoteM Term
tcCommit)
             ]
             UnquoteM Term
failEval
    I.Def QName
f [Elim
u] ->
      forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
choice [ (QName
f QName -> TCM Term -> UnquoteM Bool
`isDef` forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMInferType,                  forall a b. Unquote a => (a -> TCM b) -> Elim -> UnquoteM b
tcFun1 Type -> TCM Term
tcInferType                  Elim
u)
             , (QName
f QName -> TCM Term -> UnquoteM Bool
`isDef` forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMNormalise,                  forall a b. Unquote a => (a -> TCM b) -> Elim -> UnquoteM b
tcFun1 Type -> TCM Term
tcNormalise                  Elim
u)
             , (QName
f QName -> TCM Term -> UnquoteM Bool
`isDef` forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMReduce,                     forall a b. Unquote a => (a -> TCM b) -> Elim -> UnquoteM b
tcFun1 Type -> TCM Term
tcReduce                     Elim
u)
             , (QName
f QName -> TCM Term -> UnquoteM Bool
`isDef` forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMGetType,                    forall a b. Unquote a => (a -> TCM b) -> Elim -> UnquoteM b
tcFun1 QName -> TCM Term
tcGetType                    Elim
u)
             , (QName
f QName -> TCM Term -> UnquoteM Bool
`isDef` forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMGetDefinition,              forall a b. Unquote a => (a -> TCM b) -> Elim -> UnquoteM b
tcFun1 QName -> TCM Term
tcGetDefinition              Elim
u)
             , (QName
f QName -> TCM Term -> UnquoteM Bool
`isDef` forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMFormatErrorParts,           forall a b. Unquote a => (a -> TCM b) -> Elim -> UnquoteM b
tcFun1 [ErrorPart] -> TCM Term
tcFormatErrorParts           Elim
u)
             , (QName
f QName -> TCM Term -> UnquoteM Bool
`isDef` forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMIsMacro,                    forall a b. Unquote a => (a -> TCM b) -> Elim -> UnquoteM b
tcFun1 QName -> TCM Term
tcIsMacro                    Elim
u)
             , (QName
f QName -> TCM Term -> UnquoteM Bool
`isDef` forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMFreshName,                  forall a b. Unquote a => (a -> TCM b) -> Elim -> UnquoteM b
tcFun1 ExeName -> TCM Term
tcFreshName                  Elim
u)
             , (QName
f QName -> TCM Term -> UnquoteM Bool
`isDef` forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMGetInstances,               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] ->
      forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
choice [ (QName
f QName -> TCM Term -> UnquoteM Bool
`isDef` forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMUnify,      forall a b c.
(Unquote a, Unquote b) =>
(a -> b -> TCM c) -> Elim -> Elim -> UnquoteM c
tcFun2 Type -> Type -> TCM Term
tcUnify      Elim
u Elim
v)
             , (QName
f QName -> TCM Term -> UnquoteM Bool
`isDef` forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMCheckType,  forall a b c.
(Unquote a, Unquote b) =>
(a -> b -> TCM c) -> Elim -> Elim -> UnquoteM c
tcFun2 Type -> Type -> TCM Term
tcCheckType  Elim
u Elim
v)
             , (QName
f QName -> TCM Term -> UnquoteM Bool
`isDef` forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMDeclareDef, 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 Term -> UnquoteM Bool
`isDef` forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMDeclarePostulate, 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 Term -> UnquoteM Bool
`isDef` forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMDefineData, forall a b c.
(Unquote a, Unquote b) =>
(a -> b -> UnquoteM c) -> Elim -> Elim -> UnquoteM c
uqFun2 QName -> [(QName, Type)] -> UnquoteM Term
tcDefineData Elim
u Elim
v)
             , (QName
f QName -> TCM Term -> UnquoteM Bool
`isDef` forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMDefineFun,  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 Term -> UnquoteM Bool
`isDef` forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMQuoteOmegaTerm, Type -> Term -> UnquoteM Term
tcQuoteTerm (Sort -> Type
sort forall a b. (a -> b) -> a -> b
$ forall t. IsFibrant -> Integer -> Sort' t
Inf IsFibrant
IsFibrant Integer
0) (forall {c}. Elim' c -> c
unElim Elim
v))
             ]
             UnquoteM Term
failEval
    I.Def QName
f [Elim
l, Elim
a, Elim
u] ->
      forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
choice [ (QName
f QName -> TCM Term -> UnquoteM Bool
`isDef` forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMReturn,      forall (m :: * -> *) a. Monad m => a -> m a
return (forall {c}. Elim' c -> c
unElim Elim
u))
             , (QName
f QName -> TCM Term -> UnquoteM Bool
`isDef` forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMTypeError,   forall a b. Unquote a => (a -> TCM b) -> Elim -> UnquoteM b
tcFun1 forall a. [ErrorPart] -> TCM a
tcTypeError   Elim
u)
             , (QName
f QName -> TCM Term -> UnquoteM Bool
`isDef` forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMQuoteTerm,   Type -> Term -> UnquoteM Term
tcQuoteTerm (forall {t} {a}. t -> a -> Type'' t a
mkT (forall {c}. Elim' c -> c
unElim Elim
l) (forall {c}. Elim' c -> c
unElim Elim
a)) (forall {c}. Elim' c -> c
unElim Elim
u))
             , (QName
f QName -> TCM Term -> UnquoteM Bool
`isDef` forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMUnquoteTerm, forall a b. Unquote a => (a -> TCM b) -> Elim -> UnquoteM b
tcFun1 (Type -> Type -> TCM Term
tcUnquoteTerm (forall {t} {a}. t -> a -> Type'' t a
mkT (forall {c}. Elim' c -> c
unElim Elim
l) (forall {c}. Elim' c -> c
unElim Elim
a))) Elim
u)
             , (QName
f QName -> TCM Term -> UnquoteM Bool
`isDef` forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMBlockOnMeta, forall a b. Unquote a => (a -> UnquoteM b) -> Elim -> UnquoteM b
uqFun1 MetaId -> UnquoteM Term
tcBlockOnMeta Elim
u)
             , (QName
f QName -> TCM Term -> UnquoteM Bool
`isDef` forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMDebugPrint,  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] -> TCM Term
tcDebugPrint Elim
l Elim
a Elim
u)
             , (QName
f QName -> TCM Term -> UnquoteM Bool
`isDef` forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMNoConstraints, Term -> UnquoteM Term
tcNoConstraints (forall {c}. Elim' c -> c
unElim Elim
u))
             , (QName
f QName -> TCM Term -> UnquoteM Bool
`isDef` forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMWithReconsParams, Term -> UnquoteM Term
tcWithReconsParams (forall {c}. Elim' c -> c
unElim Elim
u))
             , (QName
f QName -> TCM Term -> UnquoteM Bool
`isDef` forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMDeclareData, 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 Term -> UnquoteM Bool
`isDef` forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMRunSpeculative, Term -> UnquoteM Term
tcRunSpeculative (forall {c}. Elim' c -> c
unElim Elim
u))
             , (QName
f QName -> TCM Term -> UnquoteM Bool
`isDef` forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMExec, 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 -> TCM Term
tcExec Elim
l Elim
a Elim
u)
             ]
             UnquoteM Term
failEval
    I.Def QName
f [Elim
_, Elim
_, Elim
u, Elim
v] ->
      forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
choice [ (QName
f QName -> TCM Term -> UnquoteM Bool
`isDef` forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMCatchError,    Term -> Term -> UnquoteM Term
tcCatchError    (forall {c}. Elim' c -> c
unElim Elim
u) (forall {c}. Elim' c -> c
unElim Elim
v))
             , (QName
f QName -> TCM Term -> UnquoteM Bool
`isDef` forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMWithNormalisation, Term -> Term -> UnquoteM Term
tcWithNormalisation (forall {c}. Elim' c -> c
unElim Elim
u) (forall {c}. Elim' c -> c
unElim Elim
v))
             , (QName
f QName -> TCM Term -> UnquoteM Bool
`isDef` forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMInContext,     Term -> Term -> UnquoteM Term
tcInContext     (forall {c}. Elim' c -> c
unElim Elim
u) (forall {c}. Elim' c -> c
unElim Elim
v))
             , (QName
f QName -> TCM Term -> UnquoteM Bool
`isDef` forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMOnlyReduceDefs, Term -> Term -> UnquoteM Term
tcOnlyReduceDefs (forall {c}. Elim' c -> c
unElim Elim
u) (forall {c}. Elim' c -> c
unElim Elim
v))
             , (QName
f QName -> TCM Term -> UnquoteM Bool
`isDef` forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMDontReduceDefs, Term -> Term -> UnquoteM Term
tcDontReduceDefs (forall {c}. Elim' c -> c
unElim Elim
u) (forall {c}. Elim' c -> c
unElim Elim
v))
             ]
             UnquoteM Term
failEval
    I.Def QName
f [Elim
_, Elim
_, Elim
u, Elim
v, Elim
w] ->
      forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
choice [ (QName
f QName -> TCM Term -> UnquoteM Bool
`isDef` forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMExtendContext, Term -> Term -> Term -> UnquoteM Term
tcExtendContext (forall {c}. Elim' c -> c
unElim Elim
u) (forall {c}. Elim' c -> c
unElim Elim
v) (forall {c}. Elim' c -> c
unElim Elim
w))
             ]
             UnquoteM Term
failEval
    I.Def QName
f [Elim
_, Elim
_, Elim
_, Elim
_, Elim
m, Elim
k] ->
      forall (m :: * -> *) a. Monad m => [(m Bool, m a)] -> m a -> m a
choice [ (QName
f QName -> TCM Term -> UnquoteM Bool
`isDef` forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMBind, Term -> Term -> UnquoteM Term
tcBind (forall {c}. Elim' c -> c
unElim Elim
m) (forall {c}. Elim' c -> c
unElim Elim
k)) ]
             UnquoteM Term
failEval
    Term
_ -> UnquoteM Term
failEval
  where
    unElim :: Elim' c -> c
unElim = forall e. Arg e -> e
unArg forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Elim' a -> Maybe (Arg a)
isApplyElim
    tcBind :: Term -> Term -> UnquoteM Term
tcBind Term
m Term
k = do Term
v <- Term -> UnquoteM Term
evalTCM Term
m
                    Term -> UnquoteM Term
evalTCM (Term
k forall t. Apply t => t -> [Arg Term] -> t
`apply` [forall a. a -> Arg a
defaultArg Term
v])

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

    mkT :: t -> a -> Type'' t a
mkT t
l a
a = forall t a. Sort' t -> a -> Type'' t a
El Sort' t
s a
a
      where s :: Sort' t
s = forall t. Level' t -> Sort' t
Type forall a b. (a -> b) -> a -> b
$ 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 =
      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 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)

    tcWithNormalisation :: Term -> Term -> UnquoteM Term
    tcWithNormalisation :: Term -> Term -> UnquoteM Term
tcWithNormalisation Term
b Term
m = do
      Bool
v <- forall a. Unquote a => Term -> UnquoteM a
unquote Term
b
      forall a b.
(TCM (UnquoteRes a) -> TCM (UnquoteRes b))
-> UnquoteM a -> UnquoteM b
liftU1 (forall (m :: * -> *) a b.
MonadTCEnv m =>
Lens' a TCEnv -> (a -> a) -> m b -> m b
locallyTC Lens' Bool TCEnv
eUnquoteNormalise forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const Bool
v) (Term -> UnquoteM Term
evalTCM Term
m)

    tcOnlyReduceDefs :: Term -> Term -> UnquoteM Term
tcOnlyReduceDefs = (Set QName -> ReduceDefs) -> Term -> Term -> UnquoteM Term
tcDoReduceDefs Set QName -> ReduceDefs
OnlyReduceDefs
    tcDontReduceDefs :: Term -> Term -> UnquoteM Term
tcDontReduceDefs = (Set QName -> ReduceDefs) -> Term -> Term -> UnquoteM Term
tcDoReduceDefs Set QName -> ReduceDefs
DontReduceDefs

    tcWithReconsParams :: Term -> UnquoteM Term
    tcWithReconsParams :: Term -> UnquoteM Term
tcWithReconsParams Term
m = forall a b.
(TCM (UnquoteRes a) -> TCM (UnquoteRes b))
-> UnquoteM a -> UnquoteM b
liftU1 forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
locallyReconstructed forall a b. (a -> b) -> a -> b
$ Term -> UnquoteM Term
evalTCM Term
m

    tcDoReduceDefs :: (Set QName -> ReduceDefs) -> Term -> Term -> UnquoteM Term
    tcDoReduceDefs :: (Set QName -> ReduceDefs) -> Term -> Term -> UnquoteM Term
tcDoReduceDefs Set QName -> ReduceDefs
reduceDefs Term
v Term
m = do
      [QName]
qs <- forall a. Unquote a => Term -> UnquoteM a
unquote Term
v
      let defs :: ReduceDefs
defs = Set QName -> ReduceDefs
reduceDefs forall a b. (a -> b) -> a -> b
$ forall a. Ord a => [a] -> Set a
Set.fromList [QName]
qs
      forall a b.
(TCM (UnquoteRes a) -> TCM (UnquoteRes b))
-> UnquoteM a -> UnquoteM b
liftU1 (forall (m :: * -> *) a b.
MonadTCEnv m =>
Lens' a TCEnv -> (a -> a) -> m b -> m b
locallyTC Lens' ReduceDefs TCEnv
eReduceDefs (forall a. Semigroup a => a -> a -> a
<> ReduceDefs
defs)) (Term -> UnquoteM Term
evalTCM Term
m)

    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
a <- forall a. Unquote a => Term -> UnquoteM a
unquote (forall {c}. Elim' c -> c
unElim Elim
a)
      a -> UnquoteM b
fun a
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 = forall a b. Unquote a => (a -> UnquoteM b) -> Elim -> UnquoteM b
uqFun1 (forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM 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
a <- forall a. Unquote a => Term -> UnquoteM a
unquote (forall {c}. Elim' c -> c
unElim Elim
a)
      b
b <- forall a. Unquote a => Term -> UnquoteM a
unquote (forall {c}. Elim' c -> c
unElim Elim
b)
      a -> b -> UnquoteM c
fun a
a b
b

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

    tcFun2 :: (Unquote a, Unquote b) => (a -> b -> TCM c) -> Elim -> Elim -> UnquoteM c
    tcFun2 :: forall a b c.
(Unquote a, Unquote b) =>
(a -> b -> TCM c) -> Elim -> Elim -> UnquoteM c
tcFun2 a -> b -> TCM c
fun = forall a b c.
(Unquote a, Unquote b) =>
(a -> b -> UnquoteM c) -> Elim -> Elim -> UnquoteM c
uqFun2 (\ a
x b
y -> 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 = 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 -> 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 -> TCM Term
tcFreshName ExeName
s = do
      forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
viewTC Lens' Bool TCEnv
eCurrentlyElaborating) forall a b. (a -> b) -> a -> b
$
        forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ [Char] -> TypeError
GenericError [Char]
"Not supported: declaring new names from an edit-time macro"
      ModuleName
m <- forall (m :: * -> *). MonadTCEnv m => m ModuleName
currentModule
      QName -> Term
quoteName forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleName -> Name -> QName
qualify ModuleName
m forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(FreshName a, MonadFresh NameId m) =>
a -> m Name
freshName_ (ExeName -> [Char]
T.unpack ExeName
s)

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

    tcBlockOnMeta :: MetaId -> UnquoteM Term
    tcBlockOnMeta :: MetaId -> UnquoteM Term
tcBlockOnMeta MetaId
x = do
      TCState
s <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets forall a b. (a, b) -> b
snd
      forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (TCState -> Blocker -> UnquoteError
BlockedOnMeta TCState
s forall a b. (a -> b) -> a -> b
$ MetaId -> Blocker
unblockOnMeta MetaId
x)

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

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

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

    tcDebugPrint :: Text -> Integer -> [ErrorPart] -> TCM Term
    tcDebugPrint :: ExeName -> Integer -> [ErrorPart] -> TCM Term
tcDebugPrint ExeName
s Integer
n [ErrorPart]
msg = do
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc (ExeName -> [Char]
T.unpack ExeName
s) (forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
n) forall a b. (a -> b) -> a -> b
$ [ErrorPart] -> TCMT IO Doc
prettyErrorParts [ErrorPart]
msg
      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 = forall a b.
(TCM (UnquoteRes a) -> TCM (UnquoteRes b))
-> UnquoteM a -> UnquoteM b
liftU1 forall (m :: * -> *) a.
(MonadConstraint m, MonadWarning m, MonadError TCErr m,
 MonadFresh ProblemId m) =>
m a -> m a
noConstraints (Term -> UnquoteM Term
evalTCM Term
m)

    tcInferType :: R.Term -> TCM Term
    tcInferType :: Type -> TCM Term
tcInferType Type
v = do
      Bool
r <- forall (m :: * -> *). MonadTCEnv m => m Bool
isReconstructed
      (Term
_, Type
a) <- Expr -> TCMT IO (Term, Type)
inferExpr forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall r (m :: * -> *).
(ToAbstract r, MonadFresh NameId m, MonadError TCErr m,
 MonadTCEnv m, ReadTCState m, HasOptions m, HasBuiltins m,
 HasConstInfo m) =>
r -> m (AbsOfRef r)
toAbstract_ Type
v
      if Bool
r then do
        Type
a <- forall a. (InstantiateFull a, Normalise a) => a -> TCM a
process Type
a
        Type
a <- forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
locallyReduceAllDefs forall a b. (a -> b) -> a -> b
$ Type -> TCM Type
reconstructParametersInType Type
a
        forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.reconstruct" Int
50 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Infer after reconstruct:"
          forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Type
a
        forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
locallyReconstructed (Type -> TCM Term
quoteType Type
a)
      else
        Type -> TCM Term
quoteType forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall a. (InstantiateFull a, Normalise a) => a -> TCM a
process Type
a

    tcCheckType :: R.Term -> R.Type -> TCM Term
    tcCheckType :: Type -> Type -> TCM Term
tcCheckType Type
v Type
a = do
      Bool
r <- forall (m :: * -> *). MonadTCEnv m => m Bool
isReconstructed
      Type
a <- forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
workOnTypes forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
locallyReduceAllDefs forall a b. (a -> b) -> a -> b
$ Expr -> TCM Type
isType_ forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall r (m :: * -> *).
(ToAbstract r, MonadFresh NameId m, MonadError TCErr m,
 MonadTCEnv m, ReadTCState m, HasOptions m, HasBuiltins m,
 HasConstInfo m) =>
r -> m (AbsOfRef r)
toAbstract_ Type
a
      Expr
e <- forall r (m :: * -> *).
(ToAbstract r, MonadFresh NameId m, MonadError TCErr m,
 MonadTCEnv m, ReadTCState m, HasOptions m, HasBuiltins m,
 HasConstInfo m) =>
r -> m (AbsOfRef r)
toAbstract_ Type
v
      Term
v <- Expr -> Type -> TCM Term
checkExpr Expr
e Type
a
      if Bool
r then do
        Term
v <- forall a. (InstantiateFull a, Normalise a) => a -> TCM a
process Term
v
        Term
v <- forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
locallyReduceAllDefs forall a b. (a -> b) -> a -> b
$ Type -> Term -> TCM Term
reconstructParameters Type
a Term
v
        forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
locallyReconstructed (Term -> TCM Term
quoteTerm Term
v)
      else
        Term -> TCM Term
quoteTerm forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall a. (InstantiateFull a, Normalise a) => a -> TCM a
process Term
v

    tcQuoteTerm :: Type -> Term -> UnquoteM Term
    tcQuoteTerm :: Type -> Term -> UnquoteM Term
tcQuoteTerm Type
a Term
v = forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ do
      Bool
r <- forall (m :: * -> *). MonadTCEnv m => m Bool
isReconstructed
      if Bool
r then do
        Term
v <- forall a. (InstantiateFull a, Normalise a) => a -> TCM a
process Term
v
        Term
v <- forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
locallyReduceAllDefs forall a b. (a -> b) -> a -> b
$ Type -> Term -> TCM Term
reconstructParameters Type
a Term
v
        forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
locallyReconstructed (Term -> TCM Term
quoteTerm Term
v)
      else
        Term -> TCM Term
quoteTerm forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall a. (InstantiateFull a, Normalise a) => a -> TCM a
process Term
v

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

    tcNormalise :: R.Term -> TCM Term
    tcNormalise :: Type -> TCM Term
tcNormalise Type
v = do
      Bool
r <- forall (m :: * -> *). MonadTCEnv m => m Bool
isReconstructed
      (Term
v, Type
t) <- forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
locallyReduceAllDefs forall a b. (a -> b) -> a -> b
$ Expr -> TCMT IO (Term, Type)
inferExpr  forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall r (m :: * -> *).
(ToAbstract r, MonadFresh NameId m, MonadError TCErr m,
 MonadTCEnv m, ReadTCState m, HasOptions m, HasBuiltins m,
 HasConstInfo m) =>
r -> m (AbsOfRef r)
toAbstract_ Type
v
      if Bool
r then do
        Term
v <- forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
normalise Term
v
        Type
t <- forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
normalise Type
t
        Term
v <- forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
locallyReduceAllDefs forall a b. (a -> b) -> a -> b
$ Action (TCMT IO) -> Type -> Term -> TCM Term
reconstructParameters' forall (m :: * -> *). PureTCM m => Action m
defaultAction Type
t Term
v
        forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.reconstruct" Int
50 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Normalise reconstruct:" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Term
v
        forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
locallyReconstructed forall a b. (a -> b) -> a -> b
$ Term -> TCM Term
quoteTerm Term
v
      else
       Term -> TCM Term
quoteTerm forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
normalise Term
v

    tcReduce :: R.Term -> TCM Term
    tcReduce :: Type -> TCM Term
tcReduce Type
v = do
      Bool
r <- forall (m :: * -> *). MonadTCEnv m => m Bool
isReconstructed
      (Term
v, Type
t) <- forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
locallyReduceAllDefs forall a b. (a -> b) -> a -> b
$ Expr -> TCMT IO (Term, Type)
inferExpr forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall r (m :: * -> *).
(ToAbstract r, MonadFresh NameId m, MonadError TCErr m,
 MonadTCEnv m, ReadTCState m, HasOptions m, HasBuiltins m,
 HasConstInfo m) =>
r -> m (AbsOfRef r)
toAbstract_ Type
v
      if Bool
r then do
        Term
v <- forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull Term
v
        Type
t <- forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull Type
t
        Term
v <- forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
locallyReduceAllDefs forall a b. (a -> b) -> a -> b
$ Action (TCMT IO) -> Type -> Term -> TCM Term
reconstructParameters' forall (m :: * -> *). PureTCM m => Action m
defaultAction Type
t Term
v
        forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.reconstruct" Int
50 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"Reduce reconstruct:" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Term
v
        forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
locallyReconstructed forall a b. (a -> b) -> a -> b
$ Term -> TCM Term
quoteTerm Term
v
      else
        Term -> TCM Term
quoteTerm forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull Term
v

    tcGetContext :: UnquoteM Term
    tcGetContext :: UnquoteM Term
tcGetContext = forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ do
      Bool
r <- forall (m :: * -> *). MonadTCEnv m => m Bool
isReconstructed
      [([Char], Dom Type)]
as <- forall a b. (a -> b) -> [a] -> [b]
map (Name -> [Char]
nameToArgName forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t e. Dom' t e -> e
unDom forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a, b) -> b
snd) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadTCEnv m => m Context
getContext
      [([Char], Dom Type)]
as <- forall (m :: * -> *) a.
(MonadTCEnv m, HasConstInfo m, HasOptions m, TermLike a) =>
a -> m a
etaContract forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall a. (InstantiateFull a, Normalise a) => a -> TCM a
process [([Char], Dom Type)]
as
      if Bool
r then do
        [([Char], Dom Type)]
as <- [([Char], Dom Type)] -> TCMT IO [([Char], Dom Type)]
recons (forall a. [a] -> [a]
reverse [([Char], Dom Type)]
as)
        let as' :: [([Char], Dom Type)]
as' = forall a. [a] -> [a]
reverse [([Char], Dom Type)]
as
        forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
locallyReconstructed forall a b. (a -> b) -> a -> b
$ TCM ([Term] -> Term)
buildList forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ([Char], Dom Type) -> TCM Term
quoteDomWithName [([Char], Dom Type)]
as'
      else
        TCM ([Term] -> Term)
buildList forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ([Char], Dom Type) -> TCM Term
quoteDomWithName [([Char], Dom Type)]
as
      where
        recons :: [(ArgName, Dom Type)] -> TCM [(ArgName, Dom Type)]
        recons :: [([Char], Dom Type)] -> TCMT IO [([Char], Dom Type)]
recons []                        = 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
          Type
t <- forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
locallyReduceAllDefs forall a b. (a -> b) -> a -> b
$ Type -> TCM Type
reconstructParametersInType Type
t
          let d' :: Dom Type
d' = Dom Type
d{unDom :: Type
unDom=Type
t}
          [([Char], Dom Type)]
ds' <- forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext ([Char]
s, Dom Type
d') forall a b. (a -> b) -> a -> b
$ [([Char], Dom Type)] -> TCMT IO [([Char], Dom Type)]
recons [([Char], Dom Type)]
ds
          forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ ([Char]
s, Dom Type
d')forall a. a -> [a] -> [a]
:[([Char], Dom Type)]
ds'

        quoteDomWithName :: (ArgName, Dom Type) -> TCM Term
        quoteDomWithName :: ([Char], Dom Type) -> TCM Term
quoteDomWithName ([Char]
x, Dom Type
t) = forall a. ToTerm a => TCM (a -> Term)
toTerm forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> 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
      Arg Type
a <- forall (m :: * -> *) a.
(MonadTCEnv m, HasOptions m, MonadDebug m) =>
m a -> m a
workOnTypes forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
locallyReduceAllDefs forall a b. (a -> b) -> a -> b
$ forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (Expr -> TCM Type
isType_ forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< 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
      forall a b.
(TCM (UnquoteRes a) -> TCM (UnquoteRes b))
-> UnquoteM a -> UnquoteM b
liftU1 (forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext (ExeName
s, forall a. Arg a -> Dom a
domFromArg Arg Type
a :: Dom Type)) UnquoteM a
m

    tcExtendContext :: Term -> Term -> Term -> UnquoteM Term
    tcExtendContext :: Term -> Term -> Term -> UnquoteM Term
tcExtendContext Term
s Term
a Term
m = do
      ExeName
s <- forall a. Unquote a => Term -> UnquoteM a
unquote Term
s
      Arg Type
a <- forall a. Unquote a => Term -> UnquoteM a
unquote Term
a
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a. Subst a => Impossible -> a -> a
strengthen HasCallStack => Impossible
impossible) forall a b. (a -> b) -> a -> b
$ forall a. ExeName -> Arg Type -> UnquoteM a -> UnquoteM a
extendCxt ExeName
s Arg Type
a forall a b. (a -> b) -> a -> b
$ do
        Term
v <- Term -> UnquoteM Term
evalTCM forall a b. (a -> b) -> a -> b
$ forall a. Subst a => Int -> a -> a
raise Int
1 Term
m
        forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (forall a. Free a => Int -> a -> Bool
freeIn Int
0 Term
v) forall a b. (a -> b) -> a -> b
$ forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
Doc -> m a
genericDocError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<
          forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hcat [TCMT IO Doc
"Local variable '", forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM (Int -> Term
var Int
0), TCMT IO Doc
"' escaping in result of extendContext:"]
            forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<?> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
v
        forall (m :: * -> *) a. Monad m => a -> m a
return Term
v

    tcInContext :: Term -> Term -> UnquoteM Term
    tcInContext :: Term -> Term -> UnquoteM Term
tcInContext Term
c Term
m = do
      [(ExeName, Arg Type)]
c <- forall a. Unquote a => Term -> UnquoteM a
unquote Term
c
      forall a b.
(TCM (UnquoteRes a) -> TCM (UnquoteRes b))
-> UnquoteM a -> UnquoteM b
liftU1 forall (m :: * -> *) a. (MonadTCEnv m, ReadTCState m) => m a -> m a
unsafeInTopContext forall a b. (a -> b) -> a -> b
$ [(ExeName, Arg Type)] -> UnquoteM Term -> UnquoteM Term
go [(ExeName, Arg Type)]
c (Term -> UnquoteM Term
evalTCM Term
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 (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 = forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either SigError -> TCM Definition
err forall (m :: * -> *) a. Monad m => a -> m a
return forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Either SigError Definition)
getConstInfo' QName
x
      where err :: SigError -> TCM Definition
err SigError
_ = forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
[Char] -> m a
genericError forall a b. (a -> b) -> a -> b
$ [Char]
"Unbound name: " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow QName
x

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


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

    tcGetDefinition :: QName -> TCM Term
    tcGetDefinition :: QName -> TCM Term
tcGetDefinition QName
x = do
      Bool
r <- forall (m :: * -> *). MonadTCEnv m => m Bool
isReconstructed
      if Bool
r then
        QName -> TCM Term
tcGetDefinitionRecons QName
x
      else
        Definition -> TCM Term
quoteDefn forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< QName -> TCM Definition
constInfo QName
x

    tcGetDefinitionRecons :: QName -> TCM Term
    tcGetDefinitionRecons :: QName -> TCM Term
tcGetDefinitionRecons QName
x = do
      ci :: Definition
ci@(Defn {theDef :: Definition -> Defn
theDef=Defn
d}) <- QName -> TCM Definition
constInfo QName
x
      case Defn
d of
        f :: Defn
f@(Function {funClauses :: Defn -> [Clause]
funClauses=[Clause]
cs}) -> do
          [Clause]
cs' <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Clause -> TCM Clause
reconsClause [Clause]
cs
          forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
locallyReconstructed forall a b. (a -> b) -> a -> b
$ Definition -> TCM Term
quoteDefn Definition
ci{theDef :: Defn
theDef=Defn
f{funClauses :: [Clause]
funClauses=[Clause]
cs'}}

        Defn
_ -> Definition -> TCM Term
quoteDefn Definition
ci

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

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


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

    tcDeclarePostulate :: Arg QName -> R.Type -> UnquoteM Term
    tcDeclarePostulate :: Arg QName -> Type -> UnquoteM Term
tcDeclarePostulate (Arg ArgInfo
i QName
x) Type
a = forall a. UnquoteM a -> UnquoteM a
inOriginalContext forall a b. (a -> b) -> a -> b
$ do
      CommandLineOptions
clo <- forall (m :: * -> *). HasOptions m => m CommandLineOptions
commandLineOptions
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (forall a. LensSafeMode a => a -> Bool
Lens.getSafeMode CommandLineOptions
clo) forall a b. (a -> b) -> a -> b
$ forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<
        TCMT IO Doc
"Cannot postulate '" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
x forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall r (m :: * -> *).
(ToAbstract r, PrettyTCM (AbsOfRef r), MonadPretty m,
 MonadError TCErr m) =>
r -> m Doc
prettyR Type
a forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
"' with safe flag"
      ReaderT
  Context
  (StateT
     UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
  ()
setDirty
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (forall a. LensHiding a => a -> Bool
hidden ArgInfo
i) forall a b. (a -> b) -> a -> b
$ forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<
        TCMT IO Doc
"Cannot declare hidden function" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
x
      forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [QName
x]
      forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ do
        forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.unquote.decl" Int
10 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
          [ TCMT IO Doc
"declare Postulate" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
x forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":"
          , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall r (m :: * -> *).
(ToAbstract r, PrettyTCM (AbsOfRef r), MonadPretty m,
 MonadError TCErr m) =>
r -> m Doc
prettyR Type
a
          ]
        Type
a <- forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
locallyReduceAllDefs forall a b. (a -> b) -> a -> b
$ Expr -> TCM Type
isType_ forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall r (m :: * -> *).
(ToAbstract r, MonadFresh NameId m, MonadError TCErr m,
 MonadTCEnv m, ReadTCState m, HasOptions m, HasBuiltins m,
 HasConstInfo m) =>
r -> m (AbsOfRef r)
toAbstract_ Type
a
        Bool
alreadyDefined <- forall a b. Either a b -> Bool
isRight forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Either SigError Definition)
getConstInfo' QName
x
        forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
alreadyDefined forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
[Char] -> m a
genericError forall a b. (a -> b) -> a -> b
$ [Char]
"Multiple declarations of " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow QName
x
        QName -> ArgInfo -> QName -> Type -> Defn -> TCMT IO ()
addConstant' QName
x ArgInfo
i QName
x Type
a Defn
defaultAxiom
        forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (forall a. LensHiding a => a -> Bool
isInstance ArgInfo
i) forall a b. (a -> b) -> a -> b
$ QName -> Type -> TCMT IO ()
addTypedInstance QName
x Type
a
        forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
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 = forall a. UnquoteM a -> UnquoteM a
inOriginalContext forall a b. (a -> b) -> a -> b
$ do
      ReaderT
  Context
  (StateT
     UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
  ()
setDirty
      forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [QName
x]
      forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ do
        forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.unquote.decl" Int
10 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
sep
          [ TCMT IO Doc
"declare Data" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
x forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":"
          , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall r (m :: * -> *).
(ToAbstract r, PrettyTCM (AbsOfRef r), MonadPretty m,
 MonadError TCErr m) =>
r -> m Doc
prettyR Type
t
          ]
        Bool
alreadyDefined <- forall a b. Either a b -> Bool
isRight forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Either SigError Definition)
getConstInfo' QName
x
        forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
alreadyDefined forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
[Char] -> m a
genericError forall a b. (a -> b) -> a -> b
$ [Char]
"Multiple declarations of " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow QName
x
        Expr
e <- 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
t
        -- The type to be checked with @checkSig@ is without parameters.
        let ([TypedBinding]
tel, Expr
e') = Int -> Expr -> ([TypedBinding], Expr)
splitPars (forall a. Num a => Integer -> a
fromInteger Integer
npars) Expr
e
        IsAbstract
ac <- forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC (forall o i. o -> Lens' i o -> i
^. forall a. LensIsAbstract a => Lens' IsAbstract a
lensIsAbstract)
        let defIn :: DefInfo' Expr
defIn = forall t.
Name -> Fixity' -> Access -> IsAbstract -> Range -> DefInfo' t
mkDefInfo (Name -> Name
nameConcrete forall a b. (a -> b) -> a -> b
$ QName -> Name
qnameName QName
x) Fixity'
noFixity' Access
PublicAccess IsAbstract
ac forall a. Range' a
noRange
        KindOfName
-> DefInfo' Expr
-> QName
-> GeneralizeTelescope
-> Expr
-> TCMT IO ()
checkSig KindOfName
DataName DefInfo' Expr
defIn QName
x (Map QName Name -> [TypedBinding] -> GeneralizeTelescope
A.GeneralizeTel forall k a. Map k a
Map.empty [TypedBinding]
tel) Expr
e'
        forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primUnitUnit

    tcDefineData :: QName -> [(QName, R.Type)] -> UnquoteM Term
    tcDefineData :: QName -> [(QName, Type)] -> UnquoteM Term
tcDefineData QName
x [(QName, Type)]
cs = forall a. UnquoteM a -> UnquoteM a
inOriginalContext forall a b. (a -> b) -> a -> b
$ (ReaderT
  Context
  (StateT
     UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
  ()
setDirty forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>>) forall a b. (a -> b) -> a -> b
$ forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ do
      forall (m :: * -> *) a b c.
Monad m =>
m (Either a b) -> (a -> m c) -> (b -> m c) -> m c
caseEitherM (forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Either SigError Definition)
getConstInfo' QName
x)
        (forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
[Char] -> m a
genericError forall a b. (a -> b) -> a -> b
$ [Char]
"Missing declaration for " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow QName
x) forall a b. (a -> b) -> a -> b
$ \Definition
def -> do
        Int
npars <- case Definition -> Defn
theDef Definition
def of
                   DataOrRecSig Int
n -> forall (m :: * -> *) a. Monad m => a -> m a
return Int
n
                   Defn
_              -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
[Char] -> m a
genericError forall a b. (a -> b) -> a -> b
$ forall a. Pretty a => a -> [Char]
prettyShow QName
x 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.
        [Expr]
es <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (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_ forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Type -> Type
addDummy Int
npars forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) [(QName, Type)]
cs
        forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.unquote.def" Int
10 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat forall a b. (a -> b) -> a -> b
$
          [ TCMT IO Doc
"declaring constructors of" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
x forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
":" ] forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA [Expr]
es

        -- Translate parameters from internal definitions back to abstract syntax.
        Type
t   <- forall a (m :: * -> *).
(InstantiateFull a, MonadReduce m) =>
a -> m a
instantiateFull forall b c a. (b -> c) -> (a -> b) -> a -> c
. Definition -> Type
defType forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *).
(Functor m, HasConstInfo m, HasOptions m, ReadTCState m,
 MonadTCEnv m, MonadDebug m) =>
Definition -> m Definition
instantiateDef Definition
def
        [TypedBinding]
tel <- forall i (m :: * -> *).
(Reify i, MonadReify m) =>
i -> m (ReifiesTo i)
reify forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall a. TelV a -> Tele (Dom a)
theTel forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Int -> Type -> m TelView
telViewUpTo Int
npars Type
t

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

        IsAbstract
ac <- forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC (forall o i. o -> Lens' i o -> i
^. forall a. LensIsAbstract a => Lens' IsAbstract a
lensIsAbstract)
        let i :: DefInfo' Expr
i = forall t.
Name -> Fixity' -> Access -> IsAbstract -> Range -> DefInfo' t
mkDefInfo (Name -> Name
nameConcrete forall a b. (a -> b) -> a -> b
$ QName -> Name
qnameName QName
x) Fixity'
noFixity' Access
PublicAccess IsAbstract
ac forall a. Range' a
noRange
            conNames :: [QName]
conNames = forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(QName, Type)]
cs
            toAxiom :: QName -> Expr -> Declaration
toAxiom QName
c Expr
e = KindOfName
-> DefInfo' Expr
-> ArgInfo
-> Maybe [Occurrence]
-> QName
-> Expr
-> Declaration
A.Axiom KindOfName
ConName DefInfo' Expr
i ArgInfo
defaultArgInfo forall a. Maybe a
Nothing QName
c Expr
e
            as :: [Declaration]
as = forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith QName -> Expr -> Declaration
toAxiom [QName]
conNames [Expr]
es'
            lams :: [LamBinding]
lams = forall a b. (a -> b) -> [a] -> [b]
map (\case {A.TBind Range
_ TypedBindingInfo
tac (NamedArg Binder
b :| []) Expr
_ -> Maybe Expr -> NamedArg Binder -> LamBinding
A.DomainFree (TypedBindingInfo -> Maybe Expr
tbTacticAttr TypedBindingInfo
tac) NamedArg Binder
b
                              ;TypedBinding
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__ }) [TypedBinding]
tel
        forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.unquote.def" Int
10 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat forall a b. (a -> b) -> a -> b
$
          [ TCMT IO Doc
"checking datatype: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
x forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TCMT IO Doc
" with constructors:"
          , forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
nest Int
2 (forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat (forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM [QName]
conNames))
          ]
        DefInfo' Expr
-> QName
-> UniverseCheck
-> DataDefParams
-> [Declaration]
-> TCMT IO ()
checkDataDef DefInfo' Expr
i QName
x UniverseCheck
YesUniverseCheck (Set Name -> [LamBinding] -> DataDefParams
A.DataDefParams forall a. Set a
Set.empty [LamBinding]
lams) [Declaration]
as
        forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
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 (forall a. a -> Dom a
defaultDom (Sort -> Type
R.Sort forall a b. (a -> b) -> a -> b
$ Integer -> Sort
R.LitS Integer
0)) (forall a. [Char] -> a -> Abs a
R.Abs [Char]
"dummy" forall a b. (a -> b) -> a -> b
$ Int -> Type -> Type
addDummy (Int
n 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Binder' a -> a
A.binderName forall a b. (a -> b) -> a -> b
$ forall a. NamedArg a -> a
namedArg NamedArg Binder
n
          Expr
e' <- [TypedBinding] -> [TypedBinding] -> Expr -> Maybe Expr
substNames' [TypedBinding]
as [TypedBinding]
bs Expr
e
          forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. ExprLike a => (Expr -> Expr) -> a -> a
mapExpr (Name -> Name -> Expr -> Expr
substName (NamedArg Binder -> Name
getName NamedArg Binder
na) (NamedArg Binder -> Name
getName NamedArg Binder
nb)) Expr
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 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 = forall (m :: * -> *) a. Monad m => a -> m a
return Expr
e
        substNames' [TypedBinding]
_ [TypedBinding]
_ Expr
_ = forall a. Maybe a
Nothing

    tcDefineFun :: QName -> [R.Clause] -> UnquoteM Term
    tcDefineFun :: QName -> [Clause] -> UnquoteM Term
tcDefineFun QName
x [Clause]
cs = forall a. UnquoteM a -> UnquoteM a
inOriginalContext forall a b. (a -> b) -> a -> b
$ (ReaderT
  Context
  (StateT
     UnquoteState (WriterT [QName] (ExceptT UnquoteError (TCMT IO))))
  ()
setDirty forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>>) forall a b. (a -> b) -> a -> b
$ forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ do
      forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
whenM (forall a b. Either a b -> Bool
isLeft forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Either SigError Definition)
getConstInfo' QName
x) forall a b. (a -> b) -> a -> b
$
        forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
[Char] -> m a
genericError forall a b. (a -> b) -> a -> b
$ [Char]
"Missing declaration for " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow QName
x
      [Clause]
cs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (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_ forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. QName -> a -> QNamed a
QNamed QName
x) [Clause]
cs
      forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> TCMT IO Doc -> m ()
reportSDoc [Char]
"tc.unquote.def" Int
10 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA [Clause]
cs
      let accessDontCare :: a
accessDontCare = forall a. HasCallStack => a
__IMPOSSIBLE__  -- or ConcreteDef, value not looked at
      IsAbstract
ac <- forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC (forall o i. o -> Lens' i o -> i
^. forall a. LensIsAbstract a => Lens' IsAbstract a
lensIsAbstract)     -- Issue #4012, respect AbstractMode
      let i :: DefInfo' Expr
i = forall t.
Name -> Fixity' -> Access -> IsAbstract -> Range -> DefInfo' t
mkDefInfo (Name -> Name
nameConcrete forall a b. (a -> b) -> a -> b
$ QName -> Name
qnameName QName
x) Fixity'
noFixity' forall {a}. a
accessDontCare IsAbstract
ac forall a. Range' a
noRange
      forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
locallyReduceAllDefs forall a b. (a -> b) -> a -> b
$ Delayed -> DefInfo' Expr -> QName -> [Clause] -> TCMT IO ()
checkFunDef Delayed
NotDelayed DefInfo' Expr
i QName
x [Clause]
cs
      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
      TCState
oldState <- forall (m :: * -> *). MonadTCState m => m TCState
getTC
      Term
u <- forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Term -> UnquoteM Term
evalTCM Term
mu
      case Term
u of
        Con ConHead
_ ConInfo
_ [Apply (Arg { unArg :: forall e. Arg e -> e
unArg = Term
x }), Apply (Arg { unArg :: forall e. Arg e -> e
unArg = Term
b })] -> do
          forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM (forall a. Unquote a => Term -> UnquoteM a
unquote Term
b) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). MonadTCState m => TCState -> m ()
putTC TCState
oldState
          forall (m :: * -> *) a. Monad m => a -> m a
return Term
x
        Term
_ -> forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> TypeError
GenericDocError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<
          TCMT IO Doc
"Should be a pair: " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Term
u

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

    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) = forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first (TypedBinding
n forall a. a -> [a] -> [a]
:) (Int -> Expr -> ([TypedBinding], Expr)
splitPars (Int
npars forall a. Num a => a -> a -> a
- Int
1) Expr
e)
    splitPars Int
npars Expr
e = 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
  Bool
allowExec <- PragmaOptions -> Bool
optAllowExec forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
allowExec forall a b. (a -> b) -> a -> b
$
    forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ [Char] -> TypeError
GenericError [Char]
"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 (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 -> TCM Term
tcExec ExeName
exe [ExeName]
args ExeName
stdIn = do
  TCMT IO ()
requireAllowExec
  Map ExeName [Char]
exes <- CommandLineOptions -> Map ExeName [Char]
optTrustedExecutables forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m CommandLineOptions
commandLineOptions
  case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup ExeName
exe Map ExeName [Char]
exes of
    Maybe [Char]
Nothing -> forall a. ExeName -> Map ExeName [Char] -> TCM a
raiseExeNotTrusted ExeName
exe Map ExeName [Char]
exes
    Just [Char]
fp -> do
      -- Check that the executable exists.
      forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM (forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ [Char] -> IO Bool
doesFileExist [Char]
fp) forall a b. (a -> b) -> a -> b
$ forall a. ExeName -> [Char] -> TCM a
raiseExeNotFound ExeName
exe [Char]
fp
      -- Check that the executable is executable.
      forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM (forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ Permissions -> Bool
executable forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Char] -> IO Permissions
getPermissions [Char]
fp) forall a b. (a -> b) -> a -> b
$ forall a. ExeName -> [Char] -> TCM a
raiseExeNotExecutable ExeName
exe [Char]
fp

      let strArgs :: [[Char]]
strArgs    = ExeName -> [Char]
T.unpack forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [ExeName]
args
      let strStdIn :: [Char]
strStdIn   = ExeName -> [Char]
T.unpack ExeName
stdIn
      (ExitCode
datExitCode, [Char]
strStdOut, [Char]
strStdErr) <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ [Char] -> [[Char]] -> [Char] -> IO (ExitCode, [Char], [Char])
readProcessWithExitCode [Char]
fp [[Char]]
strArgs [Char]
strStdIn
      let natExitCode :: Nat
natExitCode = ExitCode -> Nat
exitCodeToNat ExitCode
datExitCode
      let txtStdOut :: ExeName
txtStdOut   = [Char] -> ExeName
T.pack [Char]
strStdOut
      let txtStdErr :: ExeName
txtStdErr   = [Char] -> ExeName
T.pack [Char]
strStdErr
      (Nat, (ExeName, ExeName)) -> Term
toR <- forall a. ToTerm a => TCM (a -> Term)
toTerm
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ (Nat, (ExeName, ExeName)) -> Term
toR (Nat
natExitCode, (ExeName
txtStdOut, ExeName
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 = forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
Doc -> m a
genericDocError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
  forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty forall a b. (a -> b) -> a -> b
$
    ([Char]
"Could not find '" forall a. [a] -> [a] -> [a]
++ ExeName -> [Char]
T.unpack ExeName
exe forall a. [a] -> [a] -> [a]
++ [Char]
"' in list of trusted executables:") forall a. a -> [a] -> [a]
:
    [ [Char]
"  - " forall a. [a] -> [a] -> [a]
++ ExeName -> [Char]
T.unpack ExeName
exe | ExeName
exe <- 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 = forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
Doc -> m a
genericDocError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
  forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall a b. (a -> b) -> a -> b
$ [Char]
"Could not find file '" forall a. [a] -> [a] -> [a]
++ [Char]
fp forall a. [a] -> [a] -> [a]
++ [Char]
"' for trusted executable " 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 = forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
Doc -> m a
genericDocError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
  forall (m :: * -> *). Applicative m => [Char] -> m Doc
text forall a b. (a -> b) -> a -> b
$ [Char]
"File '" forall a. [a] -> [a] -> [a]
++ [Char]
fp forall a. [a] -> [a] -> [a]
++ [Char]
"' for trusted executable" forall a. [a] -> [a] -> [a]
++ ExeName -> [Char]
T.unpack ExeName
exe forall a. [a] -> [a] -> [a]
++ [Char]
" does not have permission to execute"