{-# OPTIONS_GHC -Wunused-imports #-}

module Agda.TypeChecking.Quote where

import Control.Monad

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

import Agda.Syntax.Abstract qualified 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.Utils.Size
import Agda.Utils.Maybe.Strict qualified as Strict

-- | Parse @quote@.
quotedName :: (MonadTCError m, MonadAbsToCon m) => A.Expr -> m QName
quotedName :: forall (m :: * -> *).
(MonadTCError m, MonadAbsToCon m) =>
Expr -> m QName
quotedName = \case
  -- Andreas, 2024-09-27, issue #7514
  -- Is it intended to be able to quote Set but not Set1?
  A.Def' QName
x Suffix
NoSuffix -> 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 -> TypeError -> m QName
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> m QName) -> TypeError -> m QName
forall a b. (a -> b) -> a -> b
$ CannotQuote -> TypeError
CannotQuote (CannotQuote -> TypeError) -> CannotQuote -> TypeError
forall a b. (a -> b) -> a -> b
$ Expr -> CannotQuote
CannotQuoteExpression Expr
e
  where
    unambiguous :: AmbiguousQName -> m QName
unambiguous AmbiguousQName
ambX = case AmbiguousQName -> Maybe QName
getUnambiguous AmbiguousQName
ambX of
      Just QName
x  -> QName -> m QName
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return QName
x
      Maybe QName
Nothing -> TypeError -> m QName
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> m QName) -> TypeError -> m QName
forall a b. (a -> b) -> a -> b
$ CannotQuote -> TypeError
CannotQuote (CannotQuote -> TypeError) -> CannotQuote -> TypeError
forall a b. (a -> b) -> a -> b
$ AmbiguousQName -> CannotQuote
CannotQuoteAmbiguous AmbiguousQName
ambX


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 = \case
        Relevant        {} -> Term -> ReduceM Term
forall a. a -> ReduceM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
relevant
        Irrelevant      {} -> Term -> ReduceM Term
forall a. a -> ReduceM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
irrelevant
        ShapeIrrelevant {} -> 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 String
s)   =String -> ReduceM Term
forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
String -> m a
__IMPOSSIBLE_VERBOSE__ String
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 (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 (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f 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
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

      quoteTelEntry :: Dom (ArgName, 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{..} <- 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 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
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, HasCallStack) =>
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
Strict.Nothing), 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
Strict.Nothing), 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 :: * -> *).
(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 DummyTermKind
s Elims
_  -> String -> ReduceM Term
forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
String -> m a
__IMPOSSIBLE_VERBOSE__ (DummyTermKind -> String
forall a. Show a => a -> String
show DummyTermKind
s)

      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         = Definition -> Int
droppedPars Definition
def
          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 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, HasCallStack) =>
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 :: 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 :: 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)