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
{ quoteTermWithKit :: Term -> ReduceM Term
, quoteTypeWithKit :: Type -> ReduceM Term
, quoteClauseWithKit :: Clause -> ReduceM Term
, quoteDomWithKit :: Dom Type -> ReduceM Term
, quoteDefnWithKit :: Definition -> ReduceM Term
, quoteListWithKit :: forall a. (a -> ReduceM Term) -> [a] -> ReduceM Term
}
quotingKit :: TCM QuotingKit
quotingKit = do
currentFile <- fromMaybe __IMPOSSIBLE__ <$> asksTC envCurrentPath
hidden <- primHidden
instanceH <- primInstance
visible <- primVisible
relevant <- primRelevant
irrelevant <- primIrrelevant
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
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
t @@ u = apply <$> t <*> ((:[]) . defaultArg <$> u)
(!@) :: Apply a => a -> ReduceM Term -> ReduceM a
t !@ u = pure t @@ u
(!@!) :: Apply a => a -> Term -> ReduceM a
t !@! u = pure t @@ pure u
quoteHiding :: Hiding -> ReduceM Term
quoteHiding Hidden = pure hidden
quoteHiding Instance{} = pure instanceH
quoteHiding NotHidden = pure visible
quoteRelevance :: Relevance -> ReduceM Term
quoteRelevance Relevant = pure relevant
quoteRelevance Irrelevant = pure irrelevant
quoteRelevance NonStrict = pure relevant
quoteArgInfo :: ArgInfo -> ReduceM Term
quoteArgInfo (ArgInfo h m _ _) =
arginfo !@ quoteHiding h @@ quoteRelevance (getRelevance m)
quoteLit :: Literal -> ReduceM Term
quoteLit l@LitNat{} = litNat !@! Lit l
quoteLit l@LitWord64{} = litWord64 !@! Lit l
quoteLit l@LitFloat{} = litFloat !@! Lit l
quoteLit l@LitChar{} = litChar !@! Lit l
quoteLit l@LitString{} = litString !@! Lit l
quoteLit l@LitQName{} = litQName !@! Lit l
quoteLit l@LitMeta {} = litMeta !@! Lit l
quoteSortLevelTerm :: Level -> ReduceM Term
quoteSortLevelTerm (ClosedLevel n) = setLit !@! Lit (LitNat noRange n)
quoteSortLevelTerm l = set !@ quoteTerm (unlevelWithKit lkit l)
quoteSort :: Sort -> ReduceM Term
quoteSort (Type t) = quoteSortLevelTerm t
quoteSort Prop{} = pure unsupportedSort
quoteSort Inf = pure unsupportedSort
quoteSort SizeUniv = pure unsupportedSort
quoteSort PiSort{} = pure unsupportedSort
quoteSort UnivSort{} = pure unsupportedSort
quoteSort (MetaS x es) = quoteTerm $ MetaV x es
quoteSort (DefS d es) = quoteTerm $ Def d es
quoteSort (DummyS s) =__IMPOSSIBLE_VERBOSE__ s
quoteType :: Type -> ReduceM Term
quoteType (El _ t) = quoteTerm t
quoteQName :: QName -> ReduceM Term
quoteQName x = pure $ Lit $ LitQName noRange x
quotePats :: [NamedArg DeBruijnPattern] -> ReduceM Term
quotePats ps = list $ map (quoteArg quotePat . fmap namedThing) ps
quotePat :: DeBruijnPattern -> ReduceM Term
quotePat p
| patternOrigin p == Just PatOAbsurd = pure absurdP
quotePat (VarP o x) = varP !@! quoteString (dbPatVarName x)
quotePat (DotP _ _) = pure dotP
quotePat (ConP c _ ps) = conP !@ quoteQName (conName c) @@ quotePats ps
quotePat (LitP _ l) = litP !@ quoteLit l
quotePat (ProjP _ x) = projP !@ quoteQName x
quotePat (IApplyP o t u x) = pure unsupported
quotePat DefP{} = pure unsupported
quoteClause :: Clause -> ReduceM Term
quoteClause cl@Clause{namedClausePats = ps, clauseBody = body} =
case body of
Nothing -> absurdClause !@ quotePats ps
Just b ->
let perm = fromMaybe __IMPOSSIBLE__ $ dbPatPerm' False ps
v = applySubst (renamingR perm) b
in normalClause !@ quotePats ps @@ quoteTerm v
list :: [ReduceM Term] -> ReduceM Term
list = foldr (\ a as -> cons !@ a @@ as) (pure nil)
quoteList :: (a -> ReduceM Term) -> [a] -> ReduceM Term
quoteList q xs = list (map q xs)
quoteDom :: (a -> ReduceM Term) -> Dom a -> ReduceM Term
quoteDom q Dom{domInfo = info, unDom = t} = arg !@ quoteArgInfo info @@ q t
quoteAbs :: Subst t a => (a -> ReduceM Term) -> Abs a -> ReduceM Term
quoteAbs q (Abs s t) = abs !@! quoteString s @@ q t
quoteAbs q (NoAbs s t) = abs !@! quoteString s @@ q (raise 1 t)
quoteArg :: (a -> ReduceM Term) -> Arg a -> ReduceM Term
quoteArg q (Arg info t) = arg !@ quoteArgInfo info @@ q t
quoteArgs :: Args -> ReduceM Term
quoteArgs ts = list (map (quoteArg quoteTerm) ts)
quoteTerm :: Term -> ReduceM Term
quoteTerm v =
case unSpine v of
Var n es ->
let ts = fromMaybe __IMPOSSIBLE__ $ allApplyElims es
in var !@! Lit (LitNat noRange $ fromIntegral n) @@ quoteArgs ts
Lam info t -> lam !@ quoteHiding (getHiding info) @@ quoteAbs quoteTerm t
Def x es -> do
defn <- getConstInfo x
let
conOrProjPars = defParameters defn
ts = fromMaybe __IMPOSSIBLE__ $ allApplyElims es
qx Function{ funExtLam = Just (ExtLamInfo m _), funClauses = cs } = do
unless (null conOrProjPars) __IMPOSSIBLE__
n <- size <$> lookupSection m
let (pars, args) = splitAt n ts
extlam !@ list (map (quoteClause . (`apply` pars)) cs)
@@ list (map (quoteArg quoteTerm) args)
qx df@Function{ funCompiled = Just Fail, funClauses = [cl] } = do
let n = length (namedClausePats cl) - 1
extlam !@ list [quoteClause $ dropArgs n cl]
@@ list (drop n $ map (quoteArg quoteTerm) ts)
qx _ = do
n <- getDefFreeVars x
def !@! quoteName x
@@ list (drop n $ conOrProjPars ++ map (quoteArg quoteTerm) ts)
qx (theDef defn)
Con x ci es | Just ts <- allApplyElims es -> do
cDef <- getConstInfo (conName x)
n <- getDefFreeVars (conName x)
let args = list $ drop n $ defParameters cDef ++ map (quoteArg quoteTerm) ts
con !@! quoteConName x @@ args
Con x ci es -> pure unsupported
Pi t u -> pi !@ quoteDom quoteType t
@@ quoteAbs quoteType u
Level l -> quoteTerm (unlevelWithKit lkit l)
Lit l -> lit !@ quoteLit l
Sort s -> sort !@ quoteSort s
MetaV x es -> meta !@! quoteMeta currentFile x @@ quoteArgs vs
where vs = fromMaybe __IMPOSSIBLE__ $ allApplyElims es
DontCare{} -> pure unsupported
Dummy s _ -> __IMPOSSIBLE_VERBOSE__ s
defParameters :: Definition -> [ReduceM Term]
defParameters def = map par hiding
where
np = case theDef def of
Constructor{ conPars = np } -> np
Function{ funProjection = Just p } -> projIndex p - 1
_ -> 0
TelV tel _ = telView' (defType def)
hiding = map (getHiding &&& getRelevance) $ take np $ telToList tel
par (h, r) = arg !@ (arginfo !@ quoteHiding h @@ quoteRelevance r) @@ pure unsupported
quoteDefn :: Definition -> ReduceM Term
quoteDefn def =
case theDef def of
Function{funClauses = cs} ->
agdaDefinitionFunDef !@ quoteList quoteClause cs
Datatype{dataPars = np, dataCons = cs} ->
agdaDefinitionDataDef !@! quoteNat (fromIntegral np) @@ quoteList (pure . quoteName) cs
Record{recConHead = c, recFields = fs} ->
agdaDefinitionRecordDef
!@! quoteName (conName c)
@@ quoteList (quoteDom (pure . quoteName)) fs
Axiom{} -> pure agdaDefinitionPostulate
DataOrRecSig{} -> pure agdaDefinitionPostulate
GeneralizableVar{} -> pure agdaDefinitionPostulate
AbstractDefn{}-> pure agdaDefinitionPostulate
Primitive{primClauses = cs} | not $ null cs ->
agdaDefinitionFunDef !@ quoteList quoteClause cs
Primitive{} -> pure agdaDefinitionPrimitive
Constructor{conData = d} ->
agdaDefinitionDataConstructor !@! quoteName d
return $ QuotingKit quoteTerm quoteType quoteClause (quoteDom quoteType) quoteDefn quoteList
quoteString :: String -> Term
quoteString = Lit . LitString noRange
quoteName :: QName -> Term
quoteName x = Lit (LitQName noRange x)
quoteNat :: Integer -> Term
quoteNat n
| n >= 0 = Lit (LitNat noRange n)
| otherwise = __IMPOSSIBLE__
quoteConName :: ConHead -> Term
quoteConName = quoteName . conName
quoteMeta :: AbsolutePath -> MetaId -> Term
quoteMeta file = Lit . LitMeta noRange file
quoteTerm :: Term -> TCM Term
quoteTerm v = do
kit <- quotingKit
runReduceM (quoteTermWithKit kit v)
quoteType :: Type -> TCM Term
quoteType v = do
kit <- quotingKit
runReduceM (quoteTypeWithKit kit v)
quoteDom :: Dom Type -> TCM Term
quoteDom v = do
kit <- quotingKit
runReduceM (quoteDomWithKit kit v)
quoteDefn :: Definition -> TCM Term
quoteDefn def = do
kit <- quotingKit
runReduceM (quoteDefnWithKit kit def)
quoteList :: [Term] -> TCM Term
quoteList xs = do
kit <- quotingKit
runReduceM (quoteListWithKit kit pure xs)