{-# OPTIONS_GHC -Wunused-imports #-}

module Agda.TypeChecking.Quote where

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.Internal.Pattern ( hasDefP )
import Agda.Syntax.Literal
import Agda.Syntax.TopLevelModuleName

import Agda.TypeChecking.CompiledClause
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.Functor
import Agda.Utils.List
import Agda.Syntax.Common.Pretty (prettyShow)
import Agda.Utils.Size

-- | Parse @quote@.
quotedName :: (MonadTCError m, MonadAbsToCon m) => A.Expr -> m QName
quotedName :: forall (m :: * -> *).
(MonadTCError m, MonadAbsToCon m) =>
Expr -> m QName
quotedName = \case
  A.Var Name
x          -> [Char] -> m QName
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
[Char] -> m a
genericError ([Char] -> m QName) -> [Char] -> m QName
forall a b. (a -> b) -> a -> b
$ [Char]
"Cannot quote a variable " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Name -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow Name
x
  A.Def QName
x          -> QName -> m QName
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return QName
x
  A.Macro QName
x        -> QName -> m QName
forall a. a -> m a
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
    [Char] -> m Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
"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 a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return QName
x
    | Bool
otherwise =
        [Char] -> m QName
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
[Char] -> m a
genericError ([Char] -> m QName) -> [Char] -> m QName
forall a b. (a -> b) -> a -> b
$ [Char]
"quote: Ambiguous name: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ List1 QName -> [Char]
forall a. Pretty a => a -> [Char]
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
  currentModule   <- TopLevelModuleName
-> Maybe TopLevelModuleName -> TopLevelModuleName
forall a. a -> Maybe a -> a
fromMaybe TopLevelModuleName
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe TopLevelModuleName -> TopLevelModuleName)
-> TCMT IO (Maybe TopLevelModuleName) -> TCMT IO TopLevelModuleName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO (Maybe TopLevelModuleName)
forall (m :: * -> *).
(MonadTCEnv m, ReadTCState m) =>
m (Maybe TopLevelModuleName)
currentTopLevelModule
  hidden          <- primHidden
  instanceH       <- primInstance
  visible         <- primVisible
  relevant        <- primRelevant
  irrelevant      <- primIrrelevant
  quantity0       <- primQuantity0
  quantityω       <- primQuantityω
  modality        <- primModalityConstructor
  nil             <- primNil
  cons            <- primCons
  abs             <- primAbsAbs
  arg             <- primArgArg
  arginfo         <- primArgArgInfo
  var             <- primAgdaTermVar
  lam             <- primAgdaTermLam
  extlam          <- primAgdaTermExtLam
  def             <- primAgdaTermDef
  con             <- primAgdaTermCon
  pi              <- primAgdaTermPi
  sort            <- primAgdaTermSort
  meta            <- primAgdaTermMeta
  lit             <- primAgdaTermLit
  litNat          <- primAgdaLitNat
  litWord64       <- primAgdaLitNat
  litFloat        <- primAgdaLitFloat
  litChar         <- primAgdaLitChar
  litString       <- primAgdaLitString
  litQName        <- primAgdaLitQName
  litMeta         <- primAgdaLitMeta
  normalClause    <- primAgdaClauseClause
  absurdClause    <- primAgdaClauseAbsurd
  varP            <- primAgdaPatVar
  conP            <- primAgdaPatCon
  dotP            <- primAgdaPatDot
  litP            <- primAgdaPatLit
  projP           <- primAgdaPatProj
  absurdP         <- primAgdaPatAbsurd
  set             <- primAgdaSortSet
  setLit          <- primAgdaSortLit
  prop            <- primAgdaSortProp
  propLit         <- primAgdaSortPropLit
  inf             <- primAgdaSortInf
  unsupportedSort <- primAgdaSortUnsupported
  sucLevel        <- primLevelSuc
  lub             <- primLevelMax
  lkit            <- requireLevels
  Con z _ _       <- primZero
  Con s _ _       <- primSuc
  unsupported     <- primAgdaTermUnsupported

  agdaDefinitionFunDef          <- primAgdaDefinitionFunDef
  agdaDefinitionDataDef         <- primAgdaDefinitionDataDef
  agdaDefinitionRecordDef       <- primAgdaDefinitionRecordDef
  agdaDefinitionPostulate       <- primAgdaDefinitionPostulate
  agdaDefinitionPrimitive       <- primAgdaDefinitionPrimitive
  agdaDefinitionDataConstructor <- primAgdaDefinitionDataConstructor

  let (@@) :: Apply a => ReduceM a -> ReduceM Term -> ReduceM a
      ReduceM a
t @@ 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 a b. ReduceM (a -> b) -> ReduceM a -> ReduceM b
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 !@ ReduceM Term
u = a -> ReduceM a
forall a. 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 !@! Term
u = a -> ReduceM a
forall a. 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 a. a -> ReduceM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
u

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

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

      quoteQuantity :: Quantity -> ReduceM Term
      quoteQuantity (Quantity0 Q0Origin
_) = Term -> ReduceM Term
forall a. a -> ReduceM a
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 a. a -> ReduceM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
quantityω

      -- TODO: quote Annotation
      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 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 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
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 (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 Univ
u Integer
n) = case Univ
u of
        Univ
UType -> Term
inf Term -> Term -> ReduceM Term
forall a. Apply a => a -> Term -> ReduceM a
!@! Literal -> Term
Lit (Integer -> Literal
LitNat Integer
n)
        Univ
UProp -> Term -> ReduceM Term
forall a. a -> ReduceM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
unsupportedSort
        Univ
USSet -> Term -> ReduceM Term
forall a. a -> ReduceM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
unsupportedSort
      quoteSort SSet{}   = Term -> ReduceM Term
forall a. a -> ReduceM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
unsupportedSort
      quoteSort Sort
SizeUniv = Term -> ReduceM Term
forall a. a -> ReduceM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
unsupportedSort
      quoteSort Sort
LockUniv = Term -> ReduceM Term
forall a. a -> ReduceM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
unsupportedSort
      quoteSort Sort
LevelUniv = Term -> ReduceM Term
forall a. a -> ReduceM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
unsupportedSort
      quoteSort Sort
IntervalUniv = Term -> ReduceM Term
forall a. a -> ReduceM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
unsupportedSort
      quoteSort PiSort{} = Term -> ReduceM Term
forall a. a -> ReduceM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
unsupportedSort
      quoteSort FunSort{} = Term -> ReduceM Term
forall a. a -> ReduceM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
unsupportedSort
      quoteSort UnivSort{}   = Term -> ReduceM Term
forall a. a -> ReduceM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
unsupportedSort
      quoteSort (MetaS MetaId
x Elims
es) = Term -> ReduceM Term
forall a. a -> ReduceM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
unsupportedSort
      quoteSort (DefS QName
d Elims
es)  = Term -> ReduceM Term
forall a. a -> ReduceM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
unsupportedSort
      quoteSort (DummyS [Char]
s)   =[Char] -> ReduceM Term
forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
[Char] -> m a
__IMPOSSIBLE_VERBOSE__ [Char]
s

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

      quoteQName :: QName -> ReduceM Term
      quoteQName QName
x = Term -> ReduceM Term
forall a. a -> ReduceM a
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]
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 a b. (a -> b) -> Arg a -> Arg b
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 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
      -- #4763: quote IApply co/patterns as though they were variables
      quotePat (IApplyP PatternInfo
_ Term
_ Term
_ 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 DefP{}            = Term -> ReduceM Term
forall a. a -> ReduceM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
unsupported

      quoteClause :: Either a Projection -> Clause -> ReduceM Term
      quoteClause Either a 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 Either a Projection
proj of
              Left a
_ -> [NamedArg DeBruijnPattern]
ps
              Right 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 ([Char], Type)) -> NamedArg DeBruijnPattern)
-> [(Int, Dom' Term ([Char], Type))] -> [NamedArg DeBruijnPattern]
forall a b. (a -> b) -> [a] -> [b]
map (Int, Dom' Term ([Char], Type)) -> NamedArg DeBruijnPattern
forall {t} {b} {name}.
(Int, Dom' t ([Char], b)) -> Arg (Named name DeBruijnPattern)
toVar ([(Int, Dom' Term ([Char], Type))] -> [NamedArg DeBruijnPattern])
-> [(Int, Dom' Term ([Char], Type))] -> [NamedArg DeBruijnPattern]
forall a b. (a -> b) -> a -> b
$ Int
-> [(Int, Dom' Term ([Char], Type))]
-> [(Int, Dom' Term ([Char], Type))]
forall a. Int -> [a] -> [a]
take Int
n ([(Int, Dom' Term ([Char], Type))]
 -> [(Int, Dom' Term ([Char], Type))])
-> [(Int, Dom' Term ([Char], Type))]
-> [(Int, Dom' Term ([Char], Type))]
forall a b. (a -> b) -> a -> b
$ [Int]
-> [Dom' Term ([Char], Type)] -> [(Int, Dom' Term ([Char], 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 ([Char], Type)]
forall t. Tele (Dom t) -> [Dom ([Char], t)]
telToList Telescope
tel)
                  toVar :: (Int, Dom' t ([Char], b)) -> Arg (Named name DeBruijnPattern)
toVar (Int
i, Dom' t ([Char], b)
d) = Dom' t ([Char], b) -> Arg ([Char], b)
forall t a. Dom' t a -> Arg a
argFromDom Dom' t ([Char], b)
d Arg ([Char], b)
-> (([Char], b) -> Named name DeBruijnPattern)
-> Arg (Named name DeBruijnPattern)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ ([Char]
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 ([Char] -> Int -> DBPatVar
DBPatVar [Char]
x Int
i)

      quoteTelescope :: Telescope -> ReduceM Term
      quoteTelescope Telescope
tel = (Dom' Term ([Char], Type) -> ReduceM Term)
-> [Dom' Term ([Char], Type)] -> ReduceM Term
forall a. (a -> ReduceM Term) -> [a] -> ReduceM Term
quoteList Dom' Term ([Char], Type) -> ReduceM Term
quoteTelEntry ([Dom' Term ([Char], Type)] -> ReduceM Term)
-> [Dom' Term ([Char], Type)] -> ReduceM Term
forall a b. (a -> b) -> a -> b
$ Telescope -> [Dom' Term ([Char], Type)]
forall t. Tele (Dom t) -> [Dom ([Char], t)]
telToList Telescope
tel

      quoteTelEntry :: Dom (ArgName, Type) -> ReduceM Term
      quoteTelEntry dom :: Dom' Term ([Char], Type)
dom@Dom{ unDom :: forall t e. Dom' t e -> e
unDom = ([Char]
x , Type
t) } = do
        SigmaKit{..} <- 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
        Con sigmaCon ConOSystem [] !@! quoteString x @@ quoteDom quoteType (fmap snd dom)

      list :: [ReduceM Term] -> ReduceM Term
      list = (ReduceM Term -> ReduceM Term -> ReduceM Term)
-> ReduceM Term -> [ReduceM Term] -> ReduceM Term
forall a b. (a -> b -> b) -> b -> [a] -> b
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 a. a -> ReduceM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
nil)

      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
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
q (Abs [Char]
s a
t)   = Term
abs Term -> Term -> ReduceM Term
forall a. Apply a => a -> Term -> ReduceM a
!@! [Char] -> Term
quoteString [Char]
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 [Char]
s a
t) = Term
abs Term -> Term -> ReduceM Term
forall a. Apply a => a -> Term -> ReduceM a
!@! [Char] -> Term
quoteString [Char]
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
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
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)

      -- has the clause been generated (in particular by --cubical)?
      -- TODO: have an explicit clause origin field?
      generatedClause :: Clause -> Bool
      generatedClause Clause
cl = [NamedArg DeBruijnPattern] -> Bool
hasDefP (Clause -> [NamedArg DeBruijnPattern]
namedClausePats Clause
cl)

      quoteTerm :: Term -> ReduceM Term
      quoteTerm Term
v = do
        v <- Term -> ReduceM Term
forall t. Instantiate t => t -> ReduceM t
instantiate' Term
v
        case unSpine 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
            defn <- QName -> ReduceM Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
x
            patlams <- viewTC ePrintingPatternLambdas
            let isSeenPatLam = QName -> [QName] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem QName
x [QName]
patlams
            r <- isReconstructed
            -- #2220: remember to restore dropped parameters
            let
              conOrProjPars = Definition -> Bool -> [ReduceM Term]
defParameters Definition
defn Bool
r
              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 Function{ funExtLam :: Defn -> Maybe ExtLamInfo
funExtLam = Just (ExtLamInfo ModuleName
m Bool
False Maybe System
_), funClauses :: Defn -> [Clause]
funClauses = [Clause]
cs }
                | Bool -> Bool
not Bool
isSeenPatLam = Lens' TCEnv [QName]
-> ([QName] -> [QName]) -> ReduceM Term -> ReduceM Term
forall (m :: * -> *) a b.
MonadTCEnv m =>
Lens' TCEnv a -> (a -> a) -> m b -> m b
locallyTC ([QName] -> f [QName]) -> TCEnv -> f TCEnv
Lens' TCEnv [QName]
ePrintingPatternLambdas (QName
x QName -> [QName] -> [QName]
forall a. a -> [a] -> [a]
:) (ReduceM Term -> ReduceM Term) -> ReduceM Term -> ReduceM Term
forall a b. (a -> b) -> a -> b
$ 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 a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [ReduceM Term]
conOrProjPars) ReduceM ()
forall a. HasCallStack => a
__IMPOSSIBLE__
                    cs <- [Clause] -> ReduceM [Clause]
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Clause] -> ReduceM [Clause]) -> [Clause] -> ReduceM [Clause]
forall a b. (a -> b) -> a -> b
$ (Clause -> Bool) -> [Clause] -> [Clause]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Clause -> Bool) -> Clause -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Clause -> Bool
generatedClause) [Clause]
cs
                    n <- size <$> lookupSection m
                    let (pars, args) = splitAt n ts
                    extlam !@ list (map (quoteClause (Left ()) . (`apply` pars)) cs)
                           @@ list (map (quoteArg quoteTerm) 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] }
                | Bool -> Bool
not Bool
isSeenPatLam = Lens' TCEnv [QName]
-> ([QName] -> [QName]) -> ReduceM Term -> ReduceM Term
forall (m :: * -> *) a b.
MonadTCEnv m =>
Lens' TCEnv a -> (a -> a) -> m b -> m b
locallyTC ([QName] -> f [QName]) -> TCEnv -> f TCEnv
Lens' TCEnv [QName]
ePrintingPatternLambdas (QName
x QName -> [QName] -> [QName]
forall a. a -> [a] -> [a]
:) (ReduceM Term -> ReduceM Term) -> ReduceM Term -> ReduceM Term
forall a b. (a -> b) -> a -> b
$ do
                    -- See also corresponding code in InternalToAbstract
                    let n :: Int
n = [NamedArg DeBruijnPattern] -> Int
forall a. [a] -> 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 [Either () Projection -> Clause -> ReduceM Term
forall a. Either a Projection -> Clause -> ReduceM Term
quoteClause (() -> Either () Projection
forall a b. a -> Either a b
Left ()) (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
                n <- QName -> ReduceM Int
forall (m :: * -> *).
(Functor m, Applicative m, ReadTCState m, MonadTCEnv m) =>
QName -> m Int
getDefFreeVars QName
x
                def !@! quoteName x
                     @@ list (drop n $ conOrProjPars ++ map (quoteArg quoteTerm) ts)
            qx (theDef 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
            r <- ReduceM Bool
forall (m :: * -> *). MonadTCEnv m => m Bool
isReconstructed
            cDef <- getConstInfo (conName x)
            n    <- getDefFreeVars (conName x)
            let 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
            con !@! quoteConName x @@ args
          Con ConHead
x ConInfo
ci Elims
es -> Term -> ReduceM Term
forall a. a -> ReduceM a
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
!@! TopLevelModuleName -> MetaId -> Term
quoteMeta TopLevelModuleName
currentModule 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 [Char]
s Elims
_  -> [Char] -> ReduceM Term
forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
[Char] -> m a
__IMPOSSIBLE_VERBOSE__ [Char]
s

      defParameters :: Definition -> Bool -> [ReduceM Term]
      defParameters Definition
def Bool
True  = []
      defParameters Definition
def Bool
False = (Dom' Term ([Char], Type) -> ReduceM Term)
-> [Dom' Term ([Char], Type)] -> [ReduceM Term]
forall a b. (a -> b) -> [a] -> [b]
map Dom' Term ([Char], Type) -> ReduceM Term
par [Dom' Term ([Char], 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 -> Either ProjectionLikenessMissing Projection
funProjection = Right 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 ([Char], Type)]
hiding     = Int -> [Dom' Term ([Char], Type)] -> [Dom' Term ([Char], Type)]
forall a. Int -> [a] -> [a]
take Int
np ([Dom' Term ([Char], Type)] -> [Dom' Term ([Char], Type)])
-> [Dom' Term ([Char], Type)] -> [Dom' Term ([Char], Type)]
forall a b. (a -> b) -> a -> b
$ Telescope -> [Dom' Term ([Char], Type)]
forall t. Tele (Dom t) -> [Dom ([Char], t)]
telToList Telescope
tel
          par :: Dom' Term ([Char], Type) -> ReduceM Term
par Dom' Term ([Char], Type)
d      = Term
arg Term -> ReduceM Term -> ReduceM Term
forall a. Apply a => a -> ReduceM Term -> ReduceM a
!@ ArgInfo -> ReduceM Term
quoteArgInfo (Dom' Term ([Char], Type) -> ArgInfo
forall t e. Dom' t e -> ArgInfo
domInfo Dom' Term ([Char], Type)
d)
                           ReduceM Term -> ReduceM Term -> ReduceM Term
forall a. Apply a => ReduceM a -> ReduceM Term -> ReduceM a
@@ Term -> ReduceM Term
forall a. a -> ReduceM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
unsupported

      quoteDefn :: Definition -> ReduceM Term
      quoteDefn Definition
def =
        case Definition -> Defn
theDef Definition
def of
          Function{funClauses :: Defn -> [Clause]
funClauses = [Clause]
cs, funProjection :: Defn -> Either ProjectionLikenessMissing Projection
funProjection = Either ProjectionLikenessMissing Projection
proj} ->
           do
            -- re #3733: maybe these should be quoted but marked as generated?
            cs <- [Clause] -> ReduceM [Clause]
forall a. a -> ReduceM a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Clause] -> ReduceM [Clause]) -> [Clause] -> ReduceM [Clause]
forall a b. (a -> b) -> a -> b
$ (Clause -> Bool) -> [Clause] -> [Clause]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Clause -> Bool) -> Clause -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Clause -> Bool
generatedClause) [Clause]
cs
            agdaDefinitionFunDef !@ quoteList (quoteClause proj) 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 a. a -> ReduceM a
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 a. a -> ReduceM a
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 a. a -> ReduceM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
agdaDefinitionPostulate
          DataOrRecSig{} -> Term -> ReduceM Term
forall a. a -> ReduceM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
agdaDefinitionPostulate
          GeneralizableVar{} -> Term -> ReduceM Term
forall a. a -> ReduceM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
agdaDefinitionPostulate  -- TODO: reflect generalizable vars
          AbstractDefn{}-> Term -> ReduceM Term
forall a. a -> ReduceM a
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 a. [a] -> 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 (Either () Projection -> Clause -> ReduceM Term
forall a. Either a Projection -> Clause -> ReduceM Term
quoteClause (() -> Either () Projection
forall a b. a -> Either a b
Left ())) [Clause]
cs
          Primitive{}   -> Term -> ReduceM Term
forall a. a -> ReduceM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
agdaDefinitionPrimitive
          PrimitiveSort{} -> Term -> ReduceM Term
forall a. a -> ReduceM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
agdaDefinitionPrimitive
          Constructor{conData :: Defn -> QName
conData = QName
d, conSrcCon :: Defn -> ConHead
conSrcCon = ConHead
c} -> do
            q <- Definition -> Quantity
forall a. LensQuantity a => a -> Quantity
getQuantity (Definition -> Quantity) -> ReduceM Definition -> ReduceM Quantity
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> ReduceM Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo (ConHead -> QName
conName ConHead
c)
            agdaDefinitionDataConstructor !@! quoteName d @@ quoteQuantity q

  return $ QuotingKit quoteTerm quoteType (quoteDom quoteType) quoteDefn quoteList

quoteString :: String -> Term
quoteString :: [Char] -> Term
quoteString = Literal -> Term
Lit (Literal -> Term) -> ([Char] -> Literal) -> [Char] -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Literal
LitString (Text -> Literal) -> ([Char] -> Text) -> [Char] -> Literal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> 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 :: TopLevelModuleName -> MetaId -> Term
quoteMeta :: TopLevelModuleName -> MetaId -> Term
quoteMeta TopLevelModuleName
m = Literal -> Term
Lit (Literal -> Term) -> (MetaId -> Literal) -> MetaId -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TopLevelModuleName -> MetaId -> Literal
LitMeta TopLevelModuleName
m

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

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

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

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

quoteList :: [Term] -> TCM Term
quoteList :: [Term] -> TCMT IO Term
quoteList [Term]
xs = do
  kit <- TCM QuotingKit
quotingKit
  runReduceM (quoteListWithKit kit pure xs)