{-# LANGUAGE CPP #-} module Agda.TypeChecking.Quote where import Control.Arrow ((&&&)) import Control.Monad import Control.Monad.State (runState, get, put) import Control.Monad.Reader (asks) 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.Internal.Pattern ( dbPatPerm' ) import Agda.Syntax.Literal import Agda.Syntax.Position import Agda.Syntax.Translation.InternalToAbstract import Agda.TypeChecking.CompiledClause import Agda.TypeChecking.DropArgs import Agda.TypeChecking.Free import Agda.TypeChecking.Level import Agda.TypeChecking.Monad import Agda.TypeChecking.Monad.Builtin import Agda.TypeChecking.Pretty import Agda.TypeChecking.Reduce import Agda.TypeChecking.Reduce.Monad import Agda.TypeChecking.Substitute import Agda.TypeChecking.Telescope import Agda.Utils.Except import Agda.Utils.Impossible import Agda.Utils.Monad ( ifM ) import Agda.Utils.Permutation ( Permutation(Perm), compactP, reverseP ) import Agda.Utils.VarSet (VarSet) import qualified Agda.Utils.VarSet as Set import Agda.Utils.FileName import Agda.Utils.Size #include "undefined.h" 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 -- TODO: quote Quanity 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 -- We keep no ranges in the quoted term, so the equality on terms -- is only on the structure. quoteSortLevelTerm :: Level -> ReduceM Term quoteSortLevelTerm (Max []) = setLit !@! Lit (LitNat noRange 0) quoteSortLevelTerm (Max [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 -- Dot patterns don't count (#2203) v = applySubst (renamingR perm) b in normalClause !@ quotePats ps @@ quoteTerm v list :: [ReduceM Term] -> ReduceM Term list [] = pure nil list (a : as) = cons !@ a @@ list as quoteList :: (a -> ReduceM Term) -> [a] -> ReduceM Term quoteList q xs = list (map q xs) quoteDom :: (Type -> ReduceM Term) -> Dom Type -> 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 -- #2220: remember to restore dropped parameters let conOrProjPars = defParameters defn ts = fromMaybe __IMPOSSIBLE__ $ allApplyElims es qx Function{ funExtLam = Just (ExtLamInfo m _), funClauses = cs } = do -- An extended lambda should not have any extra parameters! 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 -- See also corresponding code in InternalToAbstract 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 -- could be exposed at some point but we have to take care 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 (quoteArg (pure . quoteName)) fs Axiom{} -> pure agdaDefinitionPostulate DataOrRecSig{} -> pure agdaDefinitionPostulate GeneralizableVar{} -> pure agdaDefinitionPostulate -- TODO: reflect generalizable vars 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)