module Agda.TypeChecking.Quote where

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

import Data.Maybe (fromMaybe)

import Agda.Syntax.Common
import Agda.Syntax.Internal as I
import Agda.Syntax.Internal.Pattern ( dbPatPerm' )
import Agda.Syntax.Literal
import Agda.Syntax.Position

import Agda.TypeChecking.CompiledClause
import Agda.TypeChecking.DropArgs
import Agda.TypeChecking.Level
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Monad.Builtin
import Agda.TypeChecking.Substitute

import Agda.Utils.Impossible
import Agda.Utils.FileName
import Agda.Utils.Size


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

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

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

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

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

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

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

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

      -- TODO: quote Quanity
      quoteArgInfo :: ArgInfo -> ReduceM Term
      quoteArgInfo :: ArgInfo -> ReduceM Term
quoteArgInfo (ArgInfo Hiding
h Modality
m Origin
_ FreeVariables
_) =
        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
@@ Relevance -> ReduceM Term
quoteRelevance (Modality -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance Modality
m)

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

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

      quoteSort :: Sort -> ReduceM Term
      quoteSort :: Sort -> ReduceM Term
quoteSort (Type Level
t) = Level -> ReduceM Term
quoteSortLevelTerm Level
t
      quoteSort Prop{}   = Term -> ReduceM Term
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
unsupportedSort
      quoteSort Sort
Inf      = Term -> ReduceM Term
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
unsupportedSort
      quoteSort Sort
SizeUniv = Term -> ReduceM Term
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
unsupportedSort
      quoteSort PiSort{} = Term -> ReduceM Term
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
unsupportedSort
      quoteSort FunSort{} = Term -> ReduceM Term
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
unsupportedSort
      quoteSort UnivSort{}   = Term -> ReduceM Term
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
unsupportedSort
      quoteSort (MetaS MetaId
x Elims
es) = Term -> ReduceM Term
quoteTerm (Term -> ReduceM Term) -> Term -> ReduceM Term
forall a b. (a -> b) -> a -> b
$ MetaId -> Elims -> Term
MetaV MetaId
x Elims
es
      quoteSort (DefS QName
d Elims
es)  = Term -> ReduceM Term
quoteTerm (Term -> ReduceM Term) -> Term -> ReduceM Term
forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
Def QName
d Elims
es
      quoteSort (DummyS String
s)   =String -> ReduceM Term
forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
String -> m a
__IMPOSSIBLE_VERBOSE__ String
s

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

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

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

      quotePat :: DeBruijnPattern -> ReduceM Term
      quotePat :: DeBruijnPattern -> ReduceM Term
quotePat DeBruijnPattern
p
       | 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 -> ReduceM Term
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
absurdP
      quotePat (VarP PatternInfo
o DBPatVar
x)        = Term
varP Term -> Term -> ReduceM Term
forall a. Apply a => a -> Term -> ReduceM a
!@! String -> Term
quoteString (DBPatVar -> String
dbPatVarName DBPatVar
x)
      quotePat (DotP PatternInfo
_ Term
_)        = Term -> ReduceM Term
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
dotP
      quotePat (ConP ConHead
c ConPatternInfo
_ [NamedArg DeBruijnPattern]
ps)     = Term
conP Term -> ReduceM Term -> ReduceM Term
forall a. Apply a => a -> ReduceM Term -> ReduceM a
!@ QName -> ReduceM Term
quoteQName (ConHead -> QName
conName ConHead
c) ReduceM Term -> ReduceM Term -> ReduceM Term
forall a. Apply a => ReduceM a -> ReduceM Term -> ReduceM a
@@ [NamedArg DeBruijnPattern] -> ReduceM Term
quotePats [NamedArg DeBruijnPattern]
ps
      quotePat (LitP PatternInfo
_ Literal
l)        = Term
litP Term -> ReduceM Term -> ReduceM Term
forall a. Apply a => a -> ReduceM Term -> ReduceM a
!@ Literal -> ReduceM Term
quoteLit Literal
l
      quotePat (ProjP ProjOrigin
_ QName
x)       = Term
projP Term -> ReduceM Term -> ReduceM Term
forall a. Apply a => a -> ReduceM Term -> ReduceM a
!@ QName -> ReduceM Term
quoteQName QName
x
      quotePat (IApplyP PatternInfo
o Term
t Term
u DBPatVar
x) = Term -> ReduceM Term
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
unsupported
      quotePat DefP{}            = Term -> ReduceM Term
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
unsupported

      quoteClause :: Clause -> ReduceM Term
      quoteClause :: Clause -> ReduceM Term
quoteClause cl :: Clause
cl@Clause{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
!@ [NamedArg DeBruijnPattern] -> ReduceM Term
quotePats [NamedArg DeBruijnPattern]
ps
          Just Term
b  ->
            let perm :: Permutation
perm = Permutation -> Maybe Permutation -> Permutation
forall a. a -> Maybe a -> a
fromMaybe Permutation
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Permutation -> Permutation)
-> Maybe Permutation -> Permutation
forall a b. (a -> b) -> a -> b
$ Bool -> [NamedArg DeBruijnPattern] -> Maybe Permutation
dbPatPerm' Bool
False [NamedArg DeBruijnPattern]
ps -- Dot patterns don't count (#2203)
                v :: Term
v    = Substitution' Term -> Term -> Term
forall t a. Subst t a => Substitution' t -> a -> a
applySubst (Permutation -> Substitution' Term
forall a. DeBruijn a => Permutation -> Substitution' a
renamingR Permutation
perm) Term
b
            in Term
normalClause Term -> ReduceM Term -> ReduceM Term
forall a. Apply a => 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
v

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

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

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

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

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

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

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

      defParameters :: Definition -> [ReduceM Term]
      defParameters :: Definition -> [ReduceM Term]
defParameters Definition
def = ((Hiding, Relevance) -> ReduceM Term)
-> [(Hiding, Relevance)] -> [ReduceM Term]
forall a b. (a -> b) -> [a] -> [b]
map (Hiding, Relevance) -> ReduceM Term
par [(Hiding, Relevance)]
hiding
        where
          np :: Nat
np = case Definition -> Defn
theDef Definition
def of
                 Constructor{ conPars :: Defn -> Nat
conPars = Nat
np }        -> Nat
np
                 Function{ funProjection :: Defn -> Maybe Projection
funProjection = Just Projection
p } -> Projection -> Nat
projIndex Projection
p Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
1
                 Defn
_                                  -> Nat
0
          TelV Telescope
tel Type
_ = Type -> TelV Type
telView' (Definition -> Type
defType Definition
def)
          hiding :: [(Hiding, Relevance)]
hiding     = (Dom (String, Type) -> (Hiding, Relevance))
-> [Dom (String, Type)] -> [(Hiding, Relevance)]
forall a b. (a -> b) -> [a] -> [b]
map (Dom (String, Type) -> Hiding
forall a. LensHiding a => a -> Hiding
getHiding (Dom (String, Type) -> Hiding)
-> (Dom (String, Type) -> Relevance)
-> Dom (String, Type)
-> (Hiding, Relevance)
forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& Dom (String, Type) -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance) ([Dom (String, Type)] -> [(Hiding, Relevance)])
-> [Dom (String, Type)] -> [(Hiding, Relevance)]
forall a b. (a -> b) -> a -> b
$ Nat -> [Dom (String, Type)] -> [Dom (String, Type)]
forall a. Nat -> [a] -> [a]
take Nat
np ([Dom (String, Type)] -> [Dom (String, Type)])
-> [Dom (String, Type)] -> [Dom (String, Type)]
forall a b. (a -> b) -> a -> b
$ Telescope -> [Dom (String, Type)]
forall t. Tele (Dom t) -> [Dom (String, t)]
telToList Telescope
tel
          par :: (Hiding, Relevance) -> ReduceM Term
par (Hiding
h, Relevance
r) = Term
arg Term -> ReduceM Term -> ReduceM Term
forall a. Apply a => a -> ReduceM Term -> ReduceM a
!@ (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
@@ Relevance -> ReduceM Term
quoteRelevance Relevance
r) ReduceM Term -> ReduceM Term -> ReduceM Term
forall a. Apply a => ReduceM a -> ReduceM Term -> ReduceM a
@@ Term -> ReduceM Term
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
unsupported

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

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

quoteString :: String -> Term
quoteString :: String -> Term
quoteString = Literal -> Term
Lit (Literal -> Term) -> (String -> Literal) -> String -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Range -> String -> Literal
LitString Range
forall a. Range' a
noRange

quoteName :: QName -> Term
quoteName :: QName -> Term
quoteName QName
x = Literal -> Term
Lit (Range -> QName -> Literal
LitQName Range
forall a. Range' a
noRange 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 (Range -> Integer -> Literal
LitNat Range
forall a. Range' a
noRange Integer
n)
  | Bool
otherwise = Term
forall a. HasCallStack => a
__IMPOSSIBLE__

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

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

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

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

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

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

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