module Agda.TypeChecking.Quote where

import Control.Arrow ((&&&))
import Control.Monad

import Data.Maybe (fromMaybe)
import qualified Data.Text as T

import qualified Agda.Syntax.Abstract as A
import Agda.Syntax.Common
import Agda.Syntax.Internal as I
import Agda.Syntax.Literal
import Agda.Syntax.Position

import Agda.TypeChecking.CompiledClause
import Agda.TypeChecking.DropArgs
import Agda.TypeChecking.Level
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Primitive.Base
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Substitute

import Agda.Utils.Impossible
import Agda.Utils.FileName
import Agda.Utils.Functor
import Agda.Utils.List
import Agda.Utils.Pretty (prettyShow)
import Agda.Utils.Size

-- | Parse @quote@.
quotedName :: (MonadTCError m, MonadAbsToCon m) => A.Expr -> m QName
quotedName :: Expr -> m QName
quotedName = \case
  A.Var Name
x          -> String -> m QName
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
String -> m a
genericError (String -> m QName) -> String -> m QName
forall a b. (a -> b) -> a -> b
$ String
"Cannot quote a variable " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Pretty a => a -> String
prettyShow Name
x
  A.Def QName
x          -> QName -> m QName
forall (m :: * -> *) a. Monad m => a -> m a
return QName
x
  A.Macro QName
x        -> QName -> m QName
forall (m :: * -> *) a. Monad m => a -> m a
return QName
x
  A.Proj ProjOrigin
_o AmbiguousQName
p      -> AmbiguousQName -> m QName
forall (m :: * -> *).
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
AmbiguousQName -> m QName
unambiguous AmbiguousQName
p
  A.Con AmbiguousQName
c          -> AmbiguousQName -> m QName
forall (m :: * -> *).
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
AmbiguousQName -> m QName
unambiguous AmbiguousQName
c
  A.ScopedExpr ScopeInfo
_ Expr
e -> Expr -> m QName
forall (m :: * -> *).
(MonadTCError m, MonadAbsToCon m) =>
Expr -> m QName
quotedName Expr
e
  Expr
e -> Doc -> m QName
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
Doc -> m a
genericDocError (Doc -> m QName) -> m Doc -> m QName
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
    String -> m Doc
forall (m :: * -> *). Applicative m => String -> m Doc
text String
"Can only quote defined names, but encountered" m Doc -> m Doc -> m Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> Expr -> m Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA Expr
e
  where
  unambiguous :: AmbiguousQName -> m QName
unambiguous AmbiguousQName
xs
    | Just QName
x <- AmbiguousQName -> Maybe QName
getUnambiguous AmbiguousQName
xs = QName -> m QName
forall (m :: * -> *) a. Monad m => a -> m a
return QName
x
    | Bool
otherwise =
        String -> m QName
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
String -> m a
genericError (String -> m QName) -> String -> m QName
forall a b. (a -> b) -> a -> b
$ String
"quote: Ambigous name: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ List1 QName -> String
forall a. Pretty a => a -> String
prettyShow (AmbiguousQName -> List1 QName
unAmbQ AmbiguousQName
xs)


data QuotingKit = QuotingKit
  { QuotingKit -> Term -> ReduceM Term
quoteTermWithKit   :: Term       -> ReduceM Term
  , QuotingKit -> Type -> ReduceM Term
quoteTypeWithKit   :: Type       -> ReduceM Term
  , QuotingKit -> Dom Type -> ReduceM Term
quoteDomWithKit    :: Dom Type   -> ReduceM Term
  , QuotingKit -> Definition -> ReduceM Term
quoteDefnWithKit   :: Definition -> ReduceM Term
  , QuotingKit -> forall a. (a -> ReduceM Term) -> [a] -> ReduceM Term
quoteListWithKit   :: forall a. (a -> ReduceM Term) -> [a] -> ReduceM Term
  }

quotingKit :: TCM QuotingKit
quotingKit :: TCM QuotingKit
quotingKit = do
  AbsolutePath
currentFile     <- AbsolutePath -> Maybe AbsolutePath -> AbsolutePath
forall a. a -> Maybe a -> a
fromMaybe AbsolutePath
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe AbsolutePath -> AbsolutePath)
-> TCMT IO (Maybe AbsolutePath) -> TCMT IO AbsolutePath
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (TCEnv -> Maybe AbsolutePath) -> TCMT IO (Maybe AbsolutePath)
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Maybe AbsolutePath
envCurrentPath
  Term
hidden          <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primHidden
  Term
instanceH       <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primInstance
  Term
visible         <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primVisible
  Term
relevant        <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primRelevant
  Term
irrelevant      <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIrrelevant
  Term
quantity0       <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primQuantity0
  Term
quantityω       <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primQuantityω
  Term
modality        <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primModalityConstructor
  Term
nil             <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primNil
  Term
cons            <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primCons
  Term
abs             <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAbsAbs
  Term
arg             <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primArgArg
  Term
arginfo         <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primArgArgInfo
  Term
var             <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTermVar
  Term
lam             <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTermLam
  Term
extlam          <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTermExtLam
  Term
def             <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTermDef
  Term
con             <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTermCon
  Term
pi              <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTermPi
  Term
sort            <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTermSort
  Term
meta            <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTermMeta
  Term
lit             <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTermLit
  Term
litNat          <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaLitNat
  Term
litWord64       <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaLitNat
  Term
litFloat        <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaLitFloat
  Term
litChar         <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaLitChar
  Term
litString       <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaLitString
  Term
litQName        <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaLitQName
  Term
litMeta         <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaLitMeta
  Term
normalClause    <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaClauseClause
  Term
absurdClause    <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaClauseAbsurd
  Term
varP            <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaPatVar
  Term
conP            <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaPatCon
  Term
dotP            <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaPatDot
  Term
litP            <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaPatLit
  Term
projP           <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaPatProj
  Term
absurdP         <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaPatAbsurd
  Term
set             <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaSortSet
  Term
setLit          <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaSortLit
  Term
prop            <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaSortProp
  Term
propLit         <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaSortPropLit
  Term
inf             <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaSortInf
  Term
unsupportedSort <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaSortUnsupported
  Term
sucLevel        <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelSuc
  Term
lub             <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelMax
  LevelKit
lkit            <- TCMT IO LevelKit
forall (m :: * -> *). HasBuiltins m => m LevelKit
requireLevels
  Con ConHead
z ConInfo
_ Elims
_       <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primZero
  Con ConHead
s ConInfo
_ Elims
_       <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSuc
  Term
unsupported     <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTermUnsupported

  Term
agdaDefinitionFunDef          <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaDefinitionFunDef
  Term
agdaDefinitionDataDef         <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaDefinitionDataDef
  Term
agdaDefinitionRecordDef       <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaDefinitionRecordDef
  Term
agdaDefinitionPostulate       <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaDefinitionPostulate
  Term
agdaDefinitionPrimitive       <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaDefinitionPrimitive
  Term
agdaDefinitionDataConstructor <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaDefinitionDataConstructor

  let (@@) :: Apply a => ReduceM a -> ReduceM Term -> ReduceM a
      ReduceM a
t @@ :: ReduceM a -> ReduceM Term -> ReduceM a
@@ ReduceM Term
u = a -> Args -> a
forall t. Apply t => t -> Args -> t
apply (a -> Args -> a) -> ReduceM a -> ReduceM (Args -> a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ReduceM a
t ReduceM (Args -> a) -> ReduceM Args -> ReduceM a
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ((Arg Term -> Args -> Args
forall a. a -> [a] -> [a]
:[]) (Arg Term -> Args) -> (Term -> Arg Term) -> Term -> Args
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Arg Term
forall a. a -> Arg a
defaultArg (Term -> Args) -> ReduceM Term -> ReduceM Args
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ReduceM Term
u)

      (!@) :: Apply a => a -> ReduceM Term -> ReduceM a
      a
t !@ :: a -> ReduceM Term -> ReduceM a
!@ ReduceM Term
u = a -> ReduceM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
t ReduceM a -> ReduceM Term -> ReduceM a
forall a. Apply a => ReduceM a -> ReduceM Term -> ReduceM a
@@ ReduceM Term
u

      (!@!) :: Apply a => a -> Term -> ReduceM a
      a
t !@! :: a -> Term -> ReduceM a
!@! Term
u = a -> ReduceM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
t ReduceM a -> ReduceM Term -> ReduceM a
forall a. Apply a => ReduceM a -> ReduceM Term -> ReduceM a
@@ Term -> ReduceM Term
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
u

      quoteHiding :: Hiding -> ReduceM Term
      quoteHiding :: Hiding -> ReduceM Term
quoteHiding Hiding
Hidden     = Term -> ReduceM Term
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
hidden
      quoteHiding Instance{} = Term -> ReduceM Term
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
instanceH
      quoteHiding Hiding
NotHidden  = Term -> ReduceM Term
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
visible

      quoteRelevance :: Relevance -> ReduceM Term
      quoteRelevance :: Relevance -> ReduceM Term
quoteRelevance Relevance
Relevant   = Term -> ReduceM Term
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
relevant
      quoteRelevance Relevance
Irrelevant = Term -> ReduceM Term
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
irrelevant
      quoteRelevance Relevance
NonStrict  = Term -> ReduceM Term
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
relevant

      quoteQuantity :: Quantity -> ReduceM Term
      quoteQuantity :: Quantity -> ReduceM Term
quoteQuantity (Quantity0 Q0Origin
_) = Term -> ReduceM Term
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
quantity0
      quoteQuantity (Quantity1 Q1Origin
_) = ReduceM Term
forall a. HasCallStack => a
__IMPOSSIBLE__
      quoteQuantity (Quantityω QωOrigin
_) = Term -> ReduceM Term
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
quantityω

      -- TODO: quote Annotation
      quoteModality :: Modality -> ReduceM Term
      quoteModality :: Modality -> ReduceM Term
quoteModality Modality
m =
        Term
modality Term -> ReduceM Term -> ReduceM Term
forall a. Apply a => a -> ReduceM Term -> ReduceM a
!@ Relevance -> ReduceM Term
quoteRelevance (Modality -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance Modality
m)
                 ReduceM Term -> ReduceM Term -> ReduceM Term
forall a. Apply a => ReduceM a -> ReduceM Term -> ReduceM a
@@ Quantity -> ReduceM Term
quoteQuantity  (Modality -> Quantity
forall a. LensQuantity a => a -> Quantity
getQuantity  Modality
m)

      quoteArgInfo :: ArgInfo -> ReduceM Term
      quoteArgInfo :: ArgInfo -> ReduceM Term
quoteArgInfo (ArgInfo Hiding
h Modality
m Origin
_ FreeVariables
_ Annotation
_) =
        Term
arginfo Term -> ReduceM Term -> ReduceM Term
forall a. Apply a => a -> ReduceM Term -> ReduceM a
!@ Hiding -> ReduceM Term
quoteHiding Hiding
h
                ReduceM Term -> ReduceM Term -> ReduceM Term
forall a. Apply a => ReduceM a -> ReduceM Term -> ReduceM a
@@ Modality -> ReduceM Term
quoteModality Modality
m

      quoteLit :: Literal -> ReduceM Term
      quoteLit :: Literal -> ReduceM Term
quoteLit l :: Literal
l@LitNat{}    = Term
litNat    Term -> Term -> ReduceM Term
forall a. Apply a => a -> Term -> ReduceM a
!@! Literal -> Term
Lit Literal
l
      quoteLit l :: Literal
l@LitWord64{} = Term
litWord64 Term -> Term -> ReduceM Term
forall a. Apply a => a -> Term -> ReduceM a
!@! Literal -> Term
Lit Literal
l
      quoteLit l :: Literal
l@LitFloat{}  = Term
litFloat  Term -> Term -> ReduceM Term
forall a. Apply a => a -> Term -> ReduceM a
!@! Literal -> Term
Lit Literal
l
      quoteLit l :: Literal
l@LitChar{}   = Term
litChar   Term -> Term -> ReduceM Term
forall a. Apply a => a -> Term -> ReduceM a
!@! Literal -> Term
Lit Literal
l
      quoteLit l :: Literal
l@LitString{} = Term
litString Term -> Term -> ReduceM Term
forall a. Apply a => a -> Term -> ReduceM a
!@! Literal -> Term
Lit Literal
l
      quoteLit l :: Literal
l@LitQName{}  = Term
litQName  Term -> Term -> ReduceM Term
forall a. Apply a => a -> Term -> ReduceM a
!@! Literal -> Term
Lit Literal
l
      quoteLit l :: Literal
l@LitMeta {}  = Term
litMeta   Term -> Term -> ReduceM Term
forall a. Apply a => a -> Term -> ReduceM a
!@! Literal -> Term
Lit Literal
l

      -- We keep no ranges in the quoted term, so the equality on terms
      -- is only on the structure.
      quoteSortLevelTerm :: Term -> Term -> Level -> ReduceM Term
      quoteSortLevelTerm :: Term -> Term -> Level -> ReduceM Term
quoteSortLevelTerm Term
fromLit Term
fromLevel (ClosedLevel Integer
n) = Term
fromLit Term -> Term -> ReduceM Term
forall a. Apply a => a -> Term -> ReduceM a
!@! Literal -> Term
Lit (Integer -> Literal
LitNat Integer
n)
      quoteSortLevelTerm Term
fromLit Term
fromLevel Level
l               = Term
fromLevel Term -> ReduceM Term -> ReduceM Term
forall a. Apply a => a -> ReduceM Term -> ReduceM a
!@ Term -> ReduceM Term
quoteTerm (LevelKit -> Level -> Term
unlevelWithKit LevelKit
lkit Level
l)

      quoteSort :: Sort -> ReduceM Term
      quoteSort :: Sort -> ReduceM Term
quoteSort (Type Level
t) = Term -> Term -> Level -> ReduceM Term
quoteSortLevelTerm Term
setLit Term
set Level
t
      quoteSort (Prop Level
t) = Term -> Term -> Level -> ReduceM Term
quoteSortLevelTerm Term
propLit Term
prop Level
t
      quoteSort (Inf IsFibrant
f Integer
n) = case IsFibrant
f of
        IsFibrant
IsFibrant -> Term
inf Term -> Term -> ReduceM Term
forall a. Apply a => a -> Term -> ReduceM a
!@! Literal -> Term
Lit (Integer -> Literal
LitNat Integer
n)
        IsFibrant
IsStrict  -> Term -> ReduceM Term
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
unsupportedSort
      quoteSort SSet{}   = Term -> ReduceM Term
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
unsupportedSort
      quoteSort Sort
SizeUniv = Term -> ReduceM Term
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
unsupportedSort
      quoteSort Sort
LockUniv = Term -> ReduceM Term
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
unsupportedSort
      quoteSort PiSort{} = Term -> ReduceM Term
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
unsupportedSort
      quoteSort FunSort{} = Term -> ReduceM Term
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
unsupportedSort
      quoteSort UnivSort{}   = Term -> ReduceM Term
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
unsupportedSort
      quoteSort (MetaS MetaId
x Elims
es) = Term -> ReduceM Term
quoteTerm (Term -> ReduceM Term) -> Term -> ReduceM Term
forall a b. (a -> b) -> a -> b
$ MetaId -> Elims -> Term
MetaV MetaId
x Elims
es
      quoteSort (DefS QName
d Elims
es)  = Term -> ReduceM Term
quoteTerm (Term -> ReduceM Term) -> Term -> ReduceM Term
forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
Def QName
d Elims
es
      quoteSort (DummyS String
s)   =String -> ReduceM Term
forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
String -> m a
__IMPOSSIBLE_VERBOSE__ String
s

      quoteType :: Type -> ReduceM Term
      quoteType :: Type -> ReduceM Term
quoteType (El Sort
_ Term
t) = Term -> ReduceM Term
quoteTerm Term
t

      quoteQName :: QName -> ReduceM Term
      quoteQName :: QName -> ReduceM Term
quoteQName QName
x = Term -> ReduceM Term
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term -> ReduceM Term) -> Term -> ReduceM Term
forall a b. (a -> b) -> a -> b
$ Literal -> Term
Lit (Literal -> Term) -> Literal -> Term
forall a b. (a -> b) -> a -> b
$ QName -> Literal
LitQName QName
x

      quotePats :: [NamedArg DeBruijnPattern] -> ReduceM Term
      quotePats :: [NamedArg DeBruijnPattern] -> ReduceM Term
quotePats [NamedArg DeBruijnPattern]
ps = [ReduceM Term] -> ReduceM Term
list ([ReduceM Term] -> ReduceM Term) -> [ReduceM Term] -> ReduceM Term
forall a b. (a -> b) -> a -> b
$ (NamedArg DeBruijnPattern -> ReduceM Term)
-> [NamedArg DeBruijnPattern] -> [ReduceM Term]
forall a b. (a -> b) -> [a] -> [b]
map ((DeBruijnPattern -> ReduceM Term)
-> Arg DeBruijnPattern -> ReduceM Term
forall a. (a -> ReduceM Term) -> Arg a -> ReduceM Term
quoteArg DeBruijnPattern -> ReduceM Term
quotePat (Arg DeBruijnPattern -> ReduceM Term)
-> (NamedArg DeBruijnPattern -> Arg DeBruijnPattern)
-> NamedArg DeBruijnPattern
-> ReduceM Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Named NamedName DeBruijnPattern -> DeBruijnPattern)
-> NamedArg DeBruijnPattern -> Arg DeBruijnPattern
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Named NamedName DeBruijnPattern -> DeBruijnPattern
forall name a. Named name a -> a
namedThing) [NamedArg DeBruijnPattern]
ps

      quotePat :: DeBruijnPattern -> ReduceM Term
      quotePat :: DeBruijnPattern -> ReduceM Term
quotePat p :: DeBruijnPattern
p@(VarP PatternInfo
_ DBPatVar
x)
       | DeBruijnPattern -> Maybe PatOrigin
forall x. Pattern' x -> Maybe PatOrigin
patternOrigin DeBruijnPattern
p Maybe PatOrigin -> Maybe PatOrigin -> Bool
forall a. Eq a => a -> a -> Bool
== PatOrigin -> Maybe PatOrigin
forall a. a -> Maybe a
Just PatOrigin
PatOAbsurd = Term
absurdP Term -> Term -> ReduceM Term
forall a. Apply a => a -> Term -> ReduceM a
!@! Integer -> Term
quoteNat (Int -> Integer
forall a. Integral a => a -> Integer
toInteger (Int -> Integer) -> Int -> Integer
forall a b. (a -> b) -> a -> b
$ DBPatVar -> Int
dbPatVarIndex DBPatVar
x)
      quotePat (VarP PatternInfo
o DBPatVar
x)        = Term
varP Term -> Term -> ReduceM Term
forall a. Apply a => a -> Term -> ReduceM a
!@! Integer -> Term
quoteNat (Int -> Integer
forall a. Integral a => a -> Integer
toInteger (Int -> Integer) -> Int -> Integer
forall a b. (a -> b) -> a -> b
$ DBPatVar -> Int
dbPatVarIndex DBPatVar
x)
      quotePat (DotP PatternInfo
_ Term
t)        = Term
dotP Term -> ReduceM Term -> ReduceM Term
forall a. Apply a => a -> ReduceM Term -> ReduceM a
!@ Term -> ReduceM Term
quoteTerm Term
t
      quotePat (ConP ConHead
c ConPatternInfo
_ [NamedArg DeBruijnPattern]
ps)     = Term
conP Term -> ReduceM Term -> ReduceM Term
forall a. Apply a => a -> ReduceM Term -> ReduceM a
!@ QName -> ReduceM Term
quoteQName (ConHead -> QName
conName ConHead
c) ReduceM Term -> ReduceM Term -> ReduceM Term
forall a. Apply a => ReduceM a -> ReduceM Term -> ReduceM a
@@ [NamedArg DeBruijnPattern] -> ReduceM Term
quotePats [NamedArg DeBruijnPattern]
ps
      quotePat (LitP PatternInfo
_ Literal
l)        = Term
litP Term -> ReduceM Term -> ReduceM Term
forall a. Apply a => a -> ReduceM Term -> ReduceM a
!@ Literal -> ReduceM Term
quoteLit Literal
l
      quotePat (ProjP ProjOrigin
_ QName
x)       = Term
projP Term -> ReduceM Term -> ReduceM Term
forall a. Apply a => a -> ReduceM Term -> ReduceM a
!@ QName -> ReduceM Term
quoteQName QName
x
      quotePat (IApplyP PatternInfo
o Term
t Term
u DBPatVar
x) = Term -> ReduceM Term
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
unsupported
      quotePat DefP{}            = Term -> ReduceM Term
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
unsupported

      quoteClause :: Maybe Projection -> Clause -> ReduceM Term
      quoteClause :: Maybe Projection -> Clause -> ReduceM Term
quoteClause Maybe Projection
proj cl :: Clause
cl@Clause{ clauseTel :: Clause -> Telescope
clauseTel = Telescope
tel, namedClausePats :: Clause -> [NamedArg DeBruijnPattern]
namedClausePats = [NamedArg DeBruijnPattern]
ps, clauseBody :: Clause -> Maybe Term
clauseBody = Maybe Term
body} =
        case Maybe Term
body of
          Maybe Term
Nothing -> Term
absurdClause Term -> ReduceM Term -> ReduceM Term
forall a. Apply a => a -> ReduceM Term -> ReduceM a
!@ Telescope -> ReduceM Term
quoteTelescope Telescope
tel ReduceM Term -> ReduceM Term -> ReduceM Term
forall a. Apply a => ReduceM a -> ReduceM Term -> ReduceM a
@@ [NamedArg DeBruijnPattern] -> ReduceM Term
quotePats [NamedArg DeBruijnPattern]
ps'
          Just Term
b  -> Term
normalClause Term -> ReduceM Term -> ReduceM Term
forall a. Apply a => a -> ReduceM Term -> ReduceM a
!@ Telescope -> ReduceM Term
quoteTelescope Telescope
tel ReduceM Term -> ReduceM Term -> ReduceM Term
forall a. Apply a => ReduceM a -> ReduceM Term -> ReduceM a
@@ [NamedArg DeBruijnPattern] -> ReduceM Term
quotePats [NamedArg DeBruijnPattern]
ps' ReduceM Term -> ReduceM Term -> ReduceM Term
forall a. Apply a => ReduceM a -> ReduceM Term -> ReduceM a
@@ Term -> ReduceM Term
quoteTerm Term
b
        where
          -- #5128: restore dropped parameters if projection-like
          ps' :: [NamedArg DeBruijnPattern]
ps' =
            case Maybe Projection
proj of
              Maybe Projection
Nothing -> [NamedArg DeBruijnPattern]
ps
              Just Projection
p  -> [NamedArg DeBruijnPattern]
pars [NamedArg DeBruijnPattern]
-> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
forall a. [a] -> [a] -> [a]
++ [NamedArg DeBruijnPattern]
ps
                where
                  n :: Int
n    = Projection -> Int
projIndex Projection
p Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1
                  pars :: [NamedArg DeBruijnPattern]
pars = ((Int, Dom' Term (String, Type)) -> NamedArg DeBruijnPattern)
-> [(Int, Dom' Term (String, Type))] -> [NamedArg DeBruijnPattern]
forall a b. (a -> b) -> [a] -> [b]
map (Int, Dom' Term (String, Type)) -> NamedArg DeBruijnPattern
forall t b name.
(Int, Dom' t (String, b)) -> Arg (Named name DeBruijnPattern)
toVar ([(Int, Dom' Term (String, Type))] -> [NamedArg DeBruijnPattern])
-> [(Int, Dom' Term (String, Type))] -> [NamedArg DeBruijnPattern]
forall a b. (a -> b) -> a -> b
$ Int
-> [(Int, Dom' Term (String, Type))]
-> [(Int, Dom' Term (String, Type))]
forall a. Int -> [a] -> [a]
take Int
n ([(Int, Dom' Term (String, Type))]
 -> [(Int, Dom' Term (String, Type))])
-> [(Int, Dom' Term (String, Type))]
-> [(Int, Dom' Term (String, Type))]
forall a b. (a -> b) -> a -> b
$ [Int]
-> [Dom' Term (String, Type)] -> [(Int, Dom' Term (String, Type))]
forall a b. [a] -> [b] -> [(a, b)]
zip (Int -> [Int]
forall a. Integral a => a -> [a]
downFrom (Int -> [Int]) -> Int -> [Int]
forall a b. (a -> b) -> a -> b
$ Telescope -> Int
forall a. Sized a => a -> Int
size Telescope
tel) (Telescope -> [Dom' Term (String, Type)]
forall t. Tele (Dom t) -> [Dom (String, t)]
telToList Telescope
tel)
                  toVar :: (Int, Dom' t (String, b)) -> Arg (Named name DeBruijnPattern)
toVar (Int
i, Dom' t (String, b)
d) = Dom' t (String, b) -> Arg (String, b)
forall t a. Dom' t a -> Arg a
argFromDom Dom' t (String, b)
d Arg (String, b)
-> ((String, b) -> Named name DeBruijnPattern)
-> Arg (Named name DeBruijnPattern)
forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \ (String
x, b
_) -> DeBruijnPattern -> Named name DeBruijnPattern
forall a name. a -> Named name a
unnamed (DeBruijnPattern -> Named name DeBruijnPattern)
-> DeBruijnPattern -> Named name DeBruijnPattern
forall a b. (a -> b) -> a -> b
$ DBPatVar -> DeBruijnPattern
forall a. a -> Pattern' a
I.varP (String -> Int -> DBPatVar
DBPatVar String
x Int
i)

      quoteTelescope :: Telescope -> ReduceM Term
      quoteTelescope :: Telescope -> ReduceM Term
quoteTelescope Telescope
tel = (Dom' Term (String, Type) -> ReduceM Term)
-> [Dom' Term (String, Type)] -> ReduceM Term
forall a. (a -> ReduceM Term) -> [a] -> ReduceM Term
quoteList Dom' Term (String, Type) -> ReduceM Term
quoteTelEntry ([Dom' Term (String, Type)] -> ReduceM Term)
-> [Dom' Term (String, Type)] -> ReduceM Term
forall a b. (a -> b) -> a -> b
$ Telescope -> [Dom' Term (String, Type)]
forall t. Tele (Dom t) -> [Dom (String, t)]
telToList Telescope
tel
        where
          quoteTelEntry :: Dom (ArgName, Type) -> ReduceM Term
          quoteTelEntry :: Dom' Term (String, Type) -> ReduceM Term
quoteTelEntry dom :: Dom' Term (String, Type)
dom@Dom{ unDom :: forall t e. Dom' t e -> e
unDom = (String
x , Type
t) } = do
            SigmaKit{QName
ConHead
sigmaSnd :: SigmaKit -> QName
sigmaFst :: SigmaKit -> QName
sigmaCon :: SigmaKit -> ConHead
sigmaName :: SigmaKit -> QName
sigmaSnd :: QName
sigmaFst :: QName
sigmaCon :: ConHead
sigmaName :: QName
..} <- SigmaKit -> Maybe SigmaKit -> SigmaKit
forall a. a -> Maybe a -> a
fromMaybe SigmaKit
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe SigmaKit -> SigmaKit)
-> ReduceM (Maybe SigmaKit) -> ReduceM SigmaKit
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ReduceM (Maybe SigmaKit)
forall (m :: * -> *).
(HasBuiltins m, HasConstInfo m) =>
m (Maybe SigmaKit)
getSigmaKit
            ConHead -> ConInfo -> Elims -> Term
Con ConHead
sigmaCon ConInfo
ConOSystem [] Term -> Term -> ReduceM Term
forall a. Apply a => a -> Term -> ReduceM a
!@! String -> Term
quoteString String
x ReduceM Term -> ReduceM Term -> ReduceM Term
forall a. Apply a => ReduceM a -> ReduceM Term -> ReduceM a
@@ (Type -> ReduceM Term) -> Dom Type -> ReduceM Term
forall a. (a -> ReduceM Term) -> Dom a -> ReduceM Term
quoteDom Type -> ReduceM Term
quoteType (((String, Type) -> Type) -> Dom' Term (String, Type) -> Dom Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (String, Type) -> Type
forall a b. (a, b) -> b
snd Dom' Term (String, Type)
dom)

      list :: [ReduceM Term] -> ReduceM Term
      list :: [ReduceM Term] -> ReduceM Term
list = (ReduceM Term -> ReduceM Term -> ReduceM Term)
-> ReduceM Term -> [ReduceM Term] -> ReduceM Term
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ ReduceM Term
a ReduceM Term
as -> Term
cons Term -> ReduceM Term -> ReduceM Term
forall a. Apply a => a -> ReduceM Term -> ReduceM a
!@ ReduceM Term
a ReduceM Term -> ReduceM Term -> ReduceM Term
forall a. Apply a => ReduceM a -> ReduceM Term -> ReduceM a
@@ ReduceM Term
as) (Term -> ReduceM Term
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
nil)

      quoteList :: (a -> ReduceM Term) -> [a] -> ReduceM Term
      quoteList :: (a -> ReduceM Term) -> [a] -> ReduceM Term
quoteList a -> ReduceM Term
q [a]
xs = [ReduceM Term] -> ReduceM Term
list ((a -> ReduceM Term) -> [a] -> [ReduceM Term]
forall a b. (a -> b) -> [a] -> [b]
map a -> ReduceM Term
q [a]
xs)

      quoteDom :: (a -> ReduceM Term) -> Dom a -> ReduceM Term
      quoteDom :: (a -> ReduceM Term) -> Dom a -> ReduceM Term
quoteDom a -> ReduceM Term
q Dom{domInfo :: forall t e. Dom' t e -> ArgInfo
domInfo = ArgInfo
info, unDom :: forall t e. Dom' t e -> e
unDom = a
t} = Term
arg Term -> ReduceM Term -> ReduceM Term
forall a. Apply a => a -> ReduceM Term -> ReduceM a
!@ ArgInfo -> ReduceM Term
quoteArgInfo ArgInfo
info ReduceM Term -> ReduceM Term -> ReduceM Term
forall a. Apply a => ReduceM a -> ReduceM Term -> ReduceM a
@@ a -> ReduceM Term
q a
t

      quoteAbs :: Subst a => (a -> ReduceM Term) -> Abs a -> ReduceM Term
      quoteAbs :: (a -> ReduceM Term) -> Abs a -> ReduceM Term
quoteAbs a -> ReduceM Term
q (Abs String
s a
t)   = Term
abs Term -> Term -> ReduceM Term
forall a. Apply a => a -> Term -> ReduceM a
!@! String -> Term
quoteString String
s ReduceM Term -> ReduceM Term -> ReduceM Term
forall a. Apply a => ReduceM a -> ReduceM Term -> ReduceM a
@@ a -> ReduceM Term
q a
t
      quoteAbs a -> ReduceM Term
q (NoAbs String
s a
t) = Term
abs Term -> Term -> ReduceM Term
forall a. Apply a => a -> Term -> ReduceM a
!@! String -> Term
quoteString String
s ReduceM Term -> ReduceM Term -> ReduceM Term
forall a. Apply a => ReduceM a -> ReduceM Term -> ReduceM a
@@ a -> ReduceM Term
q (Int -> a -> a
forall a. Subst a => Int -> a -> a
raise Int
1 a
t)

      quoteArg :: (a -> ReduceM Term) -> Arg a -> ReduceM Term
      quoteArg :: (a -> ReduceM Term) -> Arg a -> ReduceM Term
quoteArg a -> ReduceM Term
q (Arg ArgInfo
info a
t) = Term
arg Term -> ReduceM Term -> ReduceM Term
forall a. Apply a => a -> ReduceM Term -> ReduceM a
!@ ArgInfo -> ReduceM Term
quoteArgInfo ArgInfo
info ReduceM Term -> ReduceM Term -> ReduceM Term
forall a. Apply a => ReduceM a -> ReduceM Term -> ReduceM a
@@ a -> ReduceM Term
q a
t

      quoteArgs :: Args -> ReduceM Term
      quoteArgs :: Args -> ReduceM Term
quoteArgs Args
ts = [ReduceM Term] -> ReduceM Term
list ((Arg Term -> ReduceM Term) -> Args -> [ReduceM Term]
forall a b. (a -> b) -> [a] -> [b]
map ((Term -> ReduceM Term) -> Arg Term -> ReduceM Term
forall a. (a -> ReduceM Term) -> Arg a -> ReduceM Term
quoteArg Term -> ReduceM Term
quoteTerm) Args
ts)

      quoteTerm :: Term -> ReduceM Term
      quoteTerm :: Term -> ReduceM Term
quoteTerm Term
v = do
        Term
v <- Term -> ReduceM Term
forall t. Instantiate t => t -> ReduceM t
instantiate' Term
v
        case Term -> Term
unSpine Term
v of
          Var Int
n Elims
es   ->
             let ts :: Args
ts = Args -> Maybe Args -> Args
forall a. a -> Maybe a -> a
fromMaybe Args
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
             in  Term
var Term -> Term -> ReduceM Term
forall a. Apply a => a -> Term -> ReduceM a
!@! Literal -> Term
Lit (Integer -> Literal
LitNat (Integer -> Literal) -> Integer -> Literal
forall a b. (a -> b) -> a -> b
$ Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
n) ReduceM Term -> ReduceM Term -> ReduceM Term
forall a. Apply a => ReduceM a -> ReduceM Term -> ReduceM a
@@ Args -> ReduceM Term
quoteArgs Args
ts
          Lam ArgInfo
info Abs Term
t -> Term
lam Term -> ReduceM Term -> ReduceM Term
forall a. Apply a => a -> ReduceM Term -> ReduceM a
!@ Hiding -> ReduceM Term
quoteHiding (ArgInfo -> Hiding
forall a. LensHiding a => a -> Hiding
getHiding ArgInfo
info) ReduceM Term -> ReduceM Term -> ReduceM Term
forall a. Apply a => ReduceM a -> ReduceM Term -> ReduceM a
@@ (Term -> ReduceM Term) -> Abs Term -> ReduceM Term
forall a. Subst a => (a -> ReduceM Term) -> Abs a -> ReduceM Term
quoteAbs Term -> ReduceM Term
quoteTerm Abs Term
t
          Def QName
x Elims
es   -> do
            Definition
defn <- QName -> ReduceM Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
x
            Bool
r <- ReduceM Bool
forall (m :: * -> *). MonadTCEnv m => m Bool
isReconstructed
            -- #2220: remember to restore dropped parameters
            let
              conOrProjPars :: [ReduceM Term]
conOrProjPars = Definition -> Bool -> [ReduceM Term]
defParameters Definition
defn Bool
r
              ts :: Args
ts = Args -> Maybe Args -> Args
forall a. a -> Maybe a -> a
fromMaybe Args
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
              qx :: Defn -> ReduceM Term
qx Function{ funExtLam :: Defn -> Maybe ExtLamInfo
funExtLam = Just (ExtLamInfo ModuleName
m Bool
False Maybe System
_), funClauses :: Defn -> [Clause]
funClauses = [Clause]
cs } = do
                    -- An extended lambda should not have any extra parameters!
                    Bool -> ReduceM () -> ReduceM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([ReduceM Term] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [ReduceM Term]
conOrProjPars) ReduceM ()
forall a. HasCallStack => a
__IMPOSSIBLE__
                    Int
n <- Telescope -> Int
forall a. Sized a => a -> Int
size (Telescope -> Int) -> ReduceM Telescope -> ReduceM Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ModuleName -> ReduceM Telescope
forall (m :: * -> *).
(Functor m, ReadTCState m) =>
ModuleName -> m Telescope
lookupSection ModuleName
m
                    let (Args
pars, Args
args) = Int -> Args -> (Args, Args)
forall a. Int -> [a] -> ([a], [a])
splitAt Int
n Args
ts
                    Term
extlam Term -> ReduceM Term -> ReduceM Term
forall a. Apply a => a -> ReduceM Term -> ReduceM a
!@ [ReduceM Term] -> ReduceM Term
list ((Clause -> ReduceM Term) -> [Clause] -> [ReduceM Term]
forall a b. (a -> b) -> [a] -> [b]
map (Maybe Projection -> Clause -> ReduceM Term
quoteClause Maybe Projection
forall a. Maybe a
Nothing (Clause -> ReduceM Term)
-> (Clause -> Clause) -> Clause -> ReduceM Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Clause -> Args -> Clause
forall t. Apply t => t -> Args -> t
`apply` Args
pars)) [Clause]
cs)
                           ReduceM Term -> ReduceM Term -> ReduceM Term
forall a. Apply a => ReduceM a -> ReduceM Term -> ReduceM a
@@ [ReduceM Term] -> ReduceM Term
list ((Arg Term -> ReduceM Term) -> Args -> [ReduceM Term]
forall a b. (a -> b) -> [a] -> [b]
map ((Term -> ReduceM Term) -> Arg Term -> ReduceM Term
forall a. (a -> ReduceM Term) -> Arg a -> ReduceM Term
quoteArg Term -> ReduceM Term
quoteTerm) Args
args)
              qx df :: Defn
df@Function{ funExtLam :: Defn -> Maybe ExtLamInfo
funExtLam = Just (ExtLamInfo ModuleName
_ Bool
True Maybe System
_), funCompiled :: Defn -> Maybe CompiledClauses
funCompiled = Just Fail{}, funClauses :: Defn -> [Clause]
funClauses = [Clause
cl] } = do
                    -- See also corresponding code in InternalToAbstract
                    let n :: Int
n = [NamedArg DeBruijnPattern] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Clause -> [NamedArg DeBruijnPattern]
namedClausePats Clause
cl) Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1
                        pars :: Args
pars = Int -> Args -> Args
forall a. Int -> [a] -> [a]
take Int
n Args
ts
                    Term
extlam Term -> ReduceM Term -> ReduceM Term
forall a. Apply a => a -> ReduceM Term -> ReduceM a
!@ [ReduceM Term] -> ReduceM Term
list [Maybe Projection -> Clause -> ReduceM Term
quoteClause Maybe Projection
forall a. Maybe a
Nothing (Clause -> ReduceM Term) -> Clause -> ReduceM Term
forall a b. (a -> b) -> a -> b
$ Clause
cl Clause -> Args -> Clause
forall t. Apply t => t -> Args -> t
`apply` Args
pars ]
                           ReduceM Term -> ReduceM Term -> ReduceM Term
forall a. Apply a => ReduceM a -> ReduceM Term -> ReduceM a
@@ [ReduceM Term] -> ReduceM Term
list (Int -> [ReduceM Term] -> [ReduceM Term]
forall a. Int -> [a] -> [a]
drop Int
n ([ReduceM Term] -> [ReduceM Term])
-> [ReduceM Term] -> [ReduceM Term]
forall a b. (a -> b) -> a -> b
$ (Arg Term -> ReduceM Term) -> Args -> [ReduceM Term]
forall a b. (a -> b) -> [a] -> [b]
map ((Term -> ReduceM Term) -> Arg Term -> ReduceM Term
forall a. (a -> ReduceM Term) -> Arg a -> ReduceM Term
quoteArg Term -> ReduceM Term
quoteTerm) Args
ts)
              qx Defn
_ = do
                Int
n <- QName -> ReduceM Int
forall (m :: * -> *).
(Functor m, Applicative m, ReadTCState m, MonadTCEnv m) =>
QName -> m Int
getDefFreeVars QName
x
                Term
def Term -> Term -> ReduceM Term
forall a. Apply a => a -> Term -> ReduceM a
!@! QName -> Term
quoteName QName
x
                     ReduceM Term -> ReduceM Term -> ReduceM Term
forall a. Apply a => ReduceM a -> ReduceM Term -> ReduceM a
@@ [ReduceM Term] -> ReduceM Term
list (Int -> [ReduceM Term] -> [ReduceM Term]
forall a. Int -> [a] -> [a]
drop Int
n ([ReduceM Term] -> [ReduceM Term])
-> [ReduceM Term] -> [ReduceM Term]
forall a b. (a -> b) -> a -> b
$ [ReduceM Term]
conOrProjPars [ReduceM Term] -> [ReduceM Term] -> [ReduceM Term]
forall a. [a] -> [a] -> [a]
++ (Arg Term -> ReduceM Term) -> Args -> [ReduceM Term]
forall a b. (a -> b) -> [a] -> [b]
map ((Term -> ReduceM Term) -> Arg Term -> ReduceM Term
forall a. (a -> ReduceM Term) -> Arg a -> ReduceM Term
quoteArg Term -> ReduceM Term
quoteTerm) Args
ts)
            Defn -> ReduceM Term
qx (Definition -> Defn
theDef Definition
defn)
          Con ConHead
x ConInfo
ci Elims
es | Just Args
ts <- Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es -> do
            Bool
r <- ReduceM Bool
forall (m :: * -> *). MonadTCEnv m => m Bool
isReconstructed
            Definition
cDef <- QName -> ReduceM Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo (ConHead -> QName
conName ConHead
x)
            Int
n    <- QName -> ReduceM Int
forall (m :: * -> *).
(Functor m, Applicative m, ReadTCState m, MonadTCEnv m) =>
QName -> m Int
getDefFreeVars (ConHead -> QName
conName ConHead
x)
            let args :: ReduceM Term
args = [ReduceM Term] -> ReduceM Term
list ([ReduceM Term] -> ReduceM Term) -> [ReduceM Term] -> ReduceM Term
forall a b. (a -> b) -> a -> b
$ Int -> [ReduceM Term] -> [ReduceM Term]
forall a. Int -> [a] -> [a]
drop Int
n ([ReduceM Term] -> [ReduceM Term])
-> [ReduceM Term] -> [ReduceM Term]
forall a b. (a -> b) -> a -> b
$ Definition -> Bool -> [ReduceM Term]
defParameters Definition
cDef Bool
r [ReduceM Term] -> [ReduceM Term] -> [ReduceM Term]
forall a. [a] -> [a] -> [a]
++ (Arg Term -> ReduceM Term) -> Args -> [ReduceM Term]
forall a b. (a -> b) -> [a] -> [b]
map ((Term -> ReduceM Term) -> Arg Term -> ReduceM Term
forall a. (a -> ReduceM Term) -> Arg a -> ReduceM Term
quoteArg Term -> ReduceM Term
quoteTerm) Args
ts
            Term
con Term -> Term -> ReduceM Term
forall a. Apply a => a -> Term -> ReduceM a
!@! ConHead -> Term
quoteConName ConHead
x ReduceM Term -> ReduceM Term -> ReduceM Term
forall a. Apply a => ReduceM a -> ReduceM Term -> ReduceM a
@@ ReduceM Term
args
          Con ConHead
x ConInfo
ci Elims
es -> Term -> ReduceM Term
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
unsupported
          Pi Dom Type
t Abs Type
u     -> Term
pi Term -> ReduceM Term -> ReduceM Term
forall a. Apply a => a -> ReduceM Term -> ReduceM a
!@  (Type -> ReduceM Term) -> Dom Type -> ReduceM Term
forall a. (a -> ReduceM Term) -> Dom a -> ReduceM Term
quoteDom Type -> ReduceM Term
quoteType Dom Type
t
                            ReduceM Term -> ReduceM Term -> ReduceM Term
forall a. Apply a => ReduceM a -> ReduceM Term -> ReduceM a
@@ (Type -> ReduceM Term) -> Abs Type -> ReduceM Term
forall a. Subst a => (a -> ReduceM Term) -> Abs a -> ReduceM Term
quoteAbs Type -> ReduceM Term
quoteType Abs Type
u
          Level Level
l    -> Term -> ReduceM Term
quoteTerm (LevelKit -> Level -> Term
unlevelWithKit LevelKit
lkit Level
l)
          Lit Literal
l      -> Term
lit Term -> ReduceM Term -> ReduceM Term
forall a. Apply a => a -> ReduceM Term -> ReduceM a
!@ Literal -> ReduceM Term
quoteLit Literal
l
          Sort Sort
s     -> Term
sort Term -> ReduceM Term -> ReduceM Term
forall a. Apply a => a -> ReduceM Term -> ReduceM a
!@ Sort -> ReduceM Term
quoteSort Sort
s
          MetaV MetaId
x Elims
es -> Term
meta Term -> Term -> ReduceM Term
forall a. Apply a => a -> Term -> ReduceM a
!@! AbsolutePath -> MetaId -> Term
quoteMeta AbsolutePath
currentFile MetaId
x ReduceM Term -> ReduceM Term -> ReduceM Term
forall a. Apply a => ReduceM a -> ReduceM Term -> ReduceM a
@@ Args -> ReduceM Term
quoteArgs Args
vs
            where vs :: Args
vs = Args -> Maybe Args -> Args
forall a. a -> Maybe a -> a
fromMaybe Args
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
          DontCare Term
u -> Term -> ReduceM Term
quoteTerm Term
u
          Dummy String
s Elims
_  -> String -> ReduceM Term
forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
String -> m a
__IMPOSSIBLE_VERBOSE__ String
s

      defParameters :: Definition -> Bool -> [ReduceM Term]
      defParameters :: Definition -> Bool -> [ReduceM Term]
defParameters Definition
def Bool
True  = []
      defParameters Definition
def Bool
False = (Dom' Term (String, Type) -> ReduceM Term)
-> [Dom' Term (String, Type)] -> [ReduceM Term]
forall a b. (a -> b) -> [a] -> [b]
map Dom' Term (String, Type) -> ReduceM Term
par [Dom' Term (String, Type)]
hiding
        where
          np :: Int
np = case Definition -> Defn
theDef Definition
def of
                 Constructor{ conPars :: Defn -> Int
conPars = Int
np }        -> Int
np
                 Function{ funProjection :: Defn -> Maybe Projection
funProjection = Just Projection
p } -> Projection -> Int
projIndex Projection
p Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1
                 Defn
_                                  -> Int
0
          TelV Telescope
tel Type
_ = Type -> TelV Type
telView' (Definition -> Type
defType Definition
def)
          hiding :: [Dom' Term (String, Type)]
hiding     = Int -> [Dom' Term (String, Type)] -> [Dom' Term (String, Type)]
forall a. Int -> [a] -> [a]
take Int
np ([Dom' Term (String, Type)] -> [Dom' Term (String, Type)])
-> [Dom' Term (String, Type)] -> [Dom' Term (String, Type)]
forall a b. (a -> b) -> a -> b
$ Telescope -> [Dom' Term (String, Type)]
forall t. Tele (Dom t) -> [Dom (String, t)]
telToList Telescope
tel
          par :: Dom' Term (String, Type) -> ReduceM Term
par Dom' Term (String, Type)
d      = Term
arg Term -> ReduceM Term -> ReduceM Term
forall a. Apply a => a -> ReduceM Term -> ReduceM a
!@ ArgInfo -> ReduceM Term
quoteArgInfo (Dom' Term (String, Type) -> ArgInfo
forall t e. Dom' t e -> ArgInfo
domInfo Dom' Term (String, Type)
d)
                           ReduceM Term -> ReduceM Term -> ReduceM Term
forall a. Apply a => ReduceM a -> ReduceM Term -> ReduceM a
@@ Term -> ReduceM Term
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
unsupported

      quoteDefn :: Definition -> ReduceM Term
      quoteDefn :: Definition -> ReduceM Term
quoteDefn Definition
def =
        case Definition -> Defn
theDef Definition
def of
          Function{funClauses :: Defn -> [Clause]
funClauses = [Clause]
cs, funProjection :: Defn -> Maybe Projection
funProjection = Maybe Projection
proj} ->
            Term
agdaDefinitionFunDef Term -> ReduceM Term -> ReduceM Term
forall a. Apply a => a -> ReduceM Term -> ReduceM a
!@ (Clause -> ReduceM Term) -> [Clause] -> ReduceM Term
forall a. (a -> ReduceM Term) -> [a] -> ReduceM Term
quoteList (Maybe Projection -> Clause -> ReduceM Term
quoteClause Maybe Projection
proj) [Clause]
cs
          Datatype{dataPars :: Defn -> Int
dataPars = Int
np, dataCons :: Defn -> [QName]
dataCons = [QName]
cs} ->
            Term
agdaDefinitionDataDef Term -> Term -> ReduceM Term
forall a. Apply a => a -> Term -> ReduceM a
!@! Integer -> Term
quoteNat (Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
np) ReduceM Term -> ReduceM Term -> ReduceM Term
forall a. Apply a => ReduceM a -> ReduceM Term -> ReduceM a
@@ (QName -> ReduceM Term) -> [QName] -> ReduceM Term
forall a. (a -> ReduceM Term) -> [a] -> ReduceM Term
quoteList (Term -> ReduceM Term
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term -> ReduceM Term) -> (QName -> Term) -> QName -> ReduceM Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Term
quoteName) [QName]
cs
          Record{recConHead :: Defn -> ConHead
recConHead = ConHead
c, recFields :: Defn -> [Dom QName]
recFields = [Dom QName]
fs} ->
            Term
agdaDefinitionRecordDef
              Term -> Term -> ReduceM Term
forall a. Apply a => a -> Term -> ReduceM a
!@! QName -> Term
quoteName (ConHead -> QName
conName ConHead
c)
              ReduceM Term -> ReduceM Term -> ReduceM Term
forall a. Apply a => ReduceM a -> ReduceM Term -> ReduceM a
@@ (Dom QName -> ReduceM Term) -> [Dom QName] -> ReduceM Term
forall a. (a -> ReduceM Term) -> [a] -> ReduceM Term
quoteList ((QName -> ReduceM Term) -> Dom QName -> ReduceM Term
forall a. (a -> ReduceM Term) -> Dom a -> ReduceM Term
quoteDom (Term -> ReduceM Term
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term -> ReduceM Term) -> (QName -> Term) -> QName -> ReduceM Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Term
quoteName)) [Dom QName]
fs
          Axiom{}       -> Term -> ReduceM Term
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
agdaDefinitionPostulate
          DataOrRecSig{} -> Term -> ReduceM Term
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
agdaDefinitionPostulate
          GeneralizableVar{} -> Term -> ReduceM Term
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
agdaDefinitionPostulate  -- TODO: reflect generalizable vars
          AbstractDefn{}-> Term -> ReduceM Term
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
agdaDefinitionPostulate
          Primitive{primClauses :: Defn -> [Clause]
primClauses = [Clause]
cs} | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [Clause] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Clause]
cs ->
            Term
agdaDefinitionFunDef Term -> ReduceM Term -> ReduceM Term
forall a. Apply a => a -> ReduceM Term -> ReduceM a
!@ (Clause -> ReduceM Term) -> [Clause] -> ReduceM Term
forall a. (a -> ReduceM Term) -> [a] -> ReduceM Term
quoteList (Maybe Projection -> Clause -> ReduceM Term
quoteClause Maybe Projection
forall a. Maybe a
Nothing) [Clause]
cs
          Primitive{}   -> Term -> ReduceM Term
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
agdaDefinitionPrimitive
          PrimitiveSort{} -> Term -> ReduceM Term
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
agdaDefinitionPrimitive
          Constructor{conData :: Defn -> QName
conData = QName
d} ->
            Term
agdaDefinitionDataConstructor Term -> Term -> ReduceM Term
forall a. Apply a => a -> Term -> ReduceM a
!@! QName -> Term
quoteName QName
d

  QuotingKit -> TCM QuotingKit
forall (m :: * -> *) a. Monad m => a -> m a
return (QuotingKit -> TCM QuotingKit) -> QuotingKit -> TCM QuotingKit
forall a b. (a -> b) -> a -> b
$ (Term -> ReduceM Term)
-> (Type -> ReduceM Term)
-> (Dom Type -> ReduceM Term)
-> (Definition -> ReduceM Term)
-> (forall a. (a -> ReduceM Term) -> [a] -> ReduceM Term)
-> QuotingKit
QuotingKit Term -> ReduceM Term
quoteTerm Type -> ReduceM Term
quoteType ((Type -> ReduceM Term) -> Dom Type -> ReduceM Term
forall a. (a -> ReduceM Term) -> Dom a -> ReduceM Term
quoteDom Type -> ReduceM Term
quoteType) Definition -> ReduceM Term
quoteDefn forall a. (a -> ReduceM Term) -> [a] -> ReduceM Term
quoteList

quoteString :: String -> Term
quoteString :: String -> Term
quoteString = Literal -> Term
Lit (Literal -> Term) -> (String -> Literal) -> String -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Literal
LitString (Text -> Literal) -> (String -> Text) -> String -> Literal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Text
T.pack

quoteName :: QName -> Term
quoteName :: QName -> Term
quoteName QName
x = Literal -> Term
Lit (QName -> Literal
LitQName QName
x)

quoteNat :: Integer -> Term
quoteNat :: Integer -> Term
quoteNat Integer
n
  | Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0    = Literal -> Term
Lit (Integer -> Literal
LitNat Integer
n)
  | Bool
otherwise = Term
forall a. HasCallStack => a
__IMPOSSIBLE__

quoteConName :: ConHead -> Term
quoteConName :: ConHead -> Term
quoteConName = QName -> Term
quoteName (QName -> Term) -> (ConHead -> QName) -> ConHead -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ConHead -> QName
conName

quoteMeta :: AbsolutePath -> MetaId -> Term
quoteMeta :: AbsolutePath -> MetaId -> Term
quoteMeta AbsolutePath
file = Literal -> Term
Lit (Literal -> Term) -> (MetaId -> Literal) -> MetaId -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AbsolutePath -> MetaId -> Literal
LitMeta AbsolutePath
file

quoteTerm :: Term -> TCM Term
quoteTerm :: Term -> TCMT IO Term
quoteTerm Term
v = do
  QuotingKit
kit <- TCM QuotingKit
quotingKit
  ReduceM Term -> TCMT IO Term
forall a. ReduceM a -> TCM a
runReduceM (QuotingKit -> Term -> ReduceM Term
quoteTermWithKit QuotingKit
kit Term
v)

quoteType :: Type -> TCM Term
quoteType :: Type -> TCMT IO Term
quoteType Type
v = do
  QuotingKit
kit <- TCM QuotingKit
quotingKit
  ReduceM Term -> TCMT IO Term
forall a. ReduceM a -> TCM a
runReduceM (QuotingKit -> Type -> ReduceM Term
quoteTypeWithKit QuotingKit
kit Type
v)

quoteDom :: Dom Type -> TCM Term
quoteDom :: Dom Type -> TCMT IO Term
quoteDom Dom Type
v = do
  QuotingKit
kit <- TCM QuotingKit
quotingKit
  ReduceM Term -> TCMT IO Term
forall a. ReduceM a -> TCM a
runReduceM (QuotingKit -> Dom Type -> ReduceM Term
quoteDomWithKit QuotingKit
kit Dom Type
v)

quoteDefn :: Definition -> TCM Term
quoteDefn :: Definition -> TCMT IO Term
quoteDefn Definition
def = do
  QuotingKit
kit <- TCM QuotingKit
quotingKit
  ReduceM Term -> TCMT IO Term
forall a. ReduceM a -> TCM a
runReduceM (QuotingKit -> Definition -> ReduceM Term
quoteDefnWithKit QuotingKit
kit Definition
def)

quoteList :: [Term] -> TCM Term
quoteList :: [Term] -> TCMT IO Term
quoteList [Term]
xs = do
  QuotingKit
kit <- TCM QuotingKit
quotingKit
  ReduceM Term -> TCMT IO Term
forall a. ReduceM a -> TCM a
runReduceM (QuotingKit -> (Term -> ReduceM Term) -> [Term] -> ReduceM Term
QuotingKit -> forall a. (a -> ReduceM Term) -> [a] -> ReduceM Term
quoteListWithKit QuotingKit
kit Term -> ReduceM Term
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Term]
xs)