module Agda.TypeChecking.Quote where
import Control.Applicative
import Control.Monad.State (evalState, get, put)
import Control.Monad.Writer (execWriterT, tell)
import Control.Monad.Trans (lift)
import Data.Char
import Data.Maybe (fromMaybe)
import Data.Traversable (traverse)
import Agda.Syntax.Common
import Agda.Syntax.Internal as I
import Agda.Syntax.Literal
import Agda.Syntax.Position
import Agda.Syntax.Translation.InternalToAbstract
import Agda.TypeChecking.CompiledClause
import Agda.TypeChecking.Datatypes ( getConHead )
import Agda.TypeChecking.DropArgs
import Agda.TypeChecking.Free
import Agda.TypeChecking.Level
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Monad.Builtin
import Agda.TypeChecking.Monad.Exception
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Reduce.Monad
import Agda.TypeChecking.Substitute
import Agda.Utils.Except
import Agda.Utils.Impossible
import Agda.Utils.Monad ( ifM )
import Agda.Utils.Permutation ( Permutation(Perm) )
import Agda.Utils.String ( Str(Str), unStr )
import Agda.Utils.VarSet (VarSet)
import qualified Agda.Utils.VarSet as Set
#include "undefined.h"
data QuotingKit = QuotingKit
{ quoteTermWithKit :: Term -> ReduceM Term
, quoteTypeWithKit :: Type -> ReduceM Term
, quoteClauseWithKit :: Clause -> ReduceM Term
, quoteDomWithKit :: I.Dom Type -> ReduceM Term
}
quotingKit :: TCM QuotingKit
quotingKit = do
hidden <- primHidden
instanceH <- primInstance
visible <- primVisible
relevant <- primRelevant
irrelevant <- primIrrelevant
nil <- primNil
cons <- primCons
arg <- primArgArg
arginfo <- primArgArgInfo
var <- primAgdaTermVar
lam <- primAgdaTermLam
extlam <- primAgdaTermExtLam
def <- primAgdaTermDef
con <- primAgdaTermCon
pi <- primAgdaTermPi
sort <- primAgdaTermSort
lit <- primAgdaTermLit
litNat <- primAgdaLitNat
litFloat <- primAgdaLitFloat
litChar <- primAgdaLitChar
litString <- primAgdaLitString
litQName <- primAgdaLitQName
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
el <- primAgdaTypeEl
Con z _ <- ignoreSharing <$> primZero
Con s _ <- ignoreSharing <$> primSuc
unsupported <- primAgdaTermUnsupported
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
quoteRelevance Forced{} = pure relevant
quoteRelevance UnusedArg = pure relevant
quoteArgInfo :: I.ArgInfo -> ReduceM Term
quoteArgInfo (ArgInfo h r cs) = arginfo !@ quoteHiding h
@@ quoteRelevance r
quoteLit :: Literal -> ReduceM Term
quoteLit l@LitInt{} = lit !@ (litNat !@! Lit l)
quoteLit l@LitFloat{} = lit !@ (litFloat !@! Lit l)
quoteLit l@LitChar{} = lit !@ (litChar !@! Lit l)
quoteLit l@LitString{} = lit !@ (litString !@! Lit l)
quoteLit l@LitQName{} = lit !@ (litQName !@! Lit l)
quoteSortLevelTerm :: Level -> ReduceM Term
quoteSortLevelTerm (Max []) = setLit !@! Lit (LitInt noRange 0)
quoteSortLevelTerm (Max [ClosedLevel n]) = setLit !@! Lit (LitInt 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 DLub{} = pure unsupportedSort
quoteType :: Type -> ReduceM Term
quoteType (El s t) = el !@ quoteSort s @@ quoteTerm t
quoteQName :: QName -> ReduceM Term
quoteQName x = pure $ Lit $ LitQName noRange x
quotePats :: [I.NamedArg Pattern] -> ReduceM Term
quotePats ps = list $ map (quoteArg quotePat . fmap namedThing) ps
quotePat :: Pattern -> ReduceM Term
quotePat (VarP "()") = pure absurdP
quotePat (VarP _) = pure varP
quotePat (DotP _) = pure dotP
quotePat (ConP c _ ps) = conP !@ quoteQName (conName c) @@ quotePats ps
quotePat (LitP l) = litP !@! Lit l
quotePat (ProjP x) = projP !@ quoteQName x
quoteBody :: I.ClauseBody -> Maybe (ReduceM Term)
quoteBody (Body a) = Just (quoteTerm a)
quoteBody (Bind b) = quoteBody (absBody b)
quoteBody NoBody = Nothing
quoteClause :: Clause -> ReduceM Term
quoteClause Clause{namedClausePats = ps, clauseBody = body} =
case quoteBody body of
Nothing -> absurdClause !@ quotePats ps
Just b -> normalClause !@ quotePats ps @@ b
list :: [ReduceM Term] -> ReduceM Term
list [] = pure nil
list (a : as) = cons !@ a @@ list as
quoteDom :: (Type -> ReduceM Term) -> I.Dom Type -> ReduceM Term
quoteDom q (Dom info t) = arg !@ quoteArgInfo info @@ q t
quoteArg :: (a -> ReduceM Term) -> I.Arg a -> ReduceM Term
quoteArg q (Arg info t) = arg !@ quoteArgInfo info @@ q t
quoteArgs :: I.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 (LitInt noRange $ fromIntegral n) @@ quoteArgs ts
Lam info t -> lam !@ quoteHiding (getHiding info) @@ quoteTerm (absBody t)
Def x es -> do
d <- theDef <$> getConstInfo x
qx d @@ quoteArgs ts
where
ts = fromMaybe __IMPOSSIBLE__ $ allApplyElims es
qx Function{ funExtLam = Just (h, nh), funClauses = cs } =
extlam !@ list (map (quoteClause . dropArgs (h + nh)) cs)
qx Function{ funCompiled = Just Fail, funClauses = [cl] } =
extlam !@ list [quoteClause $ dropArgs (length (clausePats cl) 1) cl]
qx _ = def !@! quoteName x
Con x ts -> con !@! quoteConName x @@ quoteArgs ts
Pi t u -> pi !@ quoteDom quoteType t
@@ quoteType (absBody u)
Level l -> quoteTerm (unlevelWithKit lkit l)
Lit lit -> quoteLit lit
Sort s -> sort !@ quoteSort s
Shared p -> quoteTerm $ derefPtr p
MetaV{} -> pure unsupported
DontCare{} -> pure unsupported
ExtLam{} -> __IMPOSSIBLE__
return $ QuotingKit quoteTerm quoteType quoteClause (quoteDom quoteType)
quoteName :: QName -> Term
quoteName x = Lit (LitQName noRange x)
quoteConName :: ConHead -> Term
quoteConName = quoteName . conName
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)