{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE NondecreasingIndentation #-}
{-# LANGUAGE TypeFamilies #-}
module Agda.TypeChecking.Monad.Signature where
import Prelude hiding (null)
import qualified Control.Monad.Fail as Fail
import Control.Monad.State
import Control.Monad.Reader
import Control.Monad.Writer
import Control.Monad.Trans.Maybe
import Control.Monad.Trans.Identity
import qualified Data.List as List
import Data.Set (Set)
import qualified Data.Set as Set
import qualified Data.Map as Map
import qualified Data.HashMap.Strict as HMap
import Data.Maybe
import Agda.Syntax.Abstract.Name
import Agda.Syntax.Abstract (Ren, ScopeCopyInfo(..))
import Agda.Syntax.Common
import Agda.Syntax.Internal as I
import Agda.Syntax.Internal.Names
import Agda.Syntax.Position
import Agda.Syntax.Treeless (Compiled(..), TTerm)
import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Monad.Builtin
import Agda.TypeChecking.Monad.Debug
import Agda.TypeChecking.Monad.Context
import Agda.TypeChecking.Monad.Env
import Agda.TypeChecking.Monad.Mutual
import Agda.TypeChecking.Monad.Open
import Agda.TypeChecking.Monad.State
import Agda.TypeChecking.Monad.Trace
import Agda.TypeChecking.DropArgs
import Agda.TypeChecking.Warnings
import Agda.TypeChecking.Positivity.Occurrence
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.CompiledClause
import Agda.TypeChecking.Coverage.SplitTree
import {-# SOURCE #-} Agda.TypeChecking.CompiledClause.Compile
import {-# SOURCE #-} Agda.TypeChecking.Polarity
import {-# SOURCE #-} Agda.TypeChecking.Pretty
import {-# SOURCE #-} Agda.TypeChecking.ProjectionLike
import {-# SOURCE #-} Agda.Compiler.Treeless.Erase
import {-# SOURCE #-} Agda.Main
import Agda.Utils.Either
import Agda.Utils.Except ( ExceptT )
import Agda.Utils.Functor
import Agda.Utils.Lens
import Agda.Utils.List
import Agda.Utils.ListT
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.Size
import Agda.Utils.Update
import Agda.Utils.Impossible
addConstant :: QName -> Definition -> TCM ()
addConstant q d = do
reportSDoc "tc.signature" 20 $ "adding constant " <+> pretty q <+> " to signature"
tel <- getContextTelescope
let tel' = replaceEmptyName "r" $ killRange $ case theDef d of
Constructor{} -> fmap hideOrKeepInstance tel
Function{ funProjection = Just Projection{ projProper = Just{}, projIndex = n } } ->
let fallback = fmap hideOrKeepInstance tel in
if n > 0 then fallback else
case initLast $ telToList tel of
Nothing -> fallback
Just (doms, dom) -> telFromList $ fmap hideOrKeepInstance doms ++ [dom]
_ -> tel
let d' = abstract tel' $ d { defName = q }
reportSDoc "tc.signature" 60 $ "lambda-lifted definition =" <?> pretty d'
modifySignature $ updateDefinitions $ HMap.insertWith (+++) q d'
i <- currentOrFreshMutualBlock
setMutualBlock i q
where
new +++ old = new { defDisplay = defDisplay new ++ defDisplay old
, defInstance = defInstance new `mplus` defInstance old }
setTerminates :: QName -> Bool -> TCM ()
setTerminates q b = modifySignature $ updateDefinition q $ updateTheDef $ \case
def@Function{} -> def { funTerminates = Just b }
def -> def
setCompiledClauses :: QName -> CompiledClauses -> TCM ()
setCompiledClauses q cc = modifySignature $ updateDefinition q $ updateTheDef $ setT
where
setT def@Function{} = def { funCompiled = Just cc }
setT def = def
setSplitTree :: QName -> SplitTree -> TCM ()
setSplitTree q st = modifySignature $ updateDefinition q $ updateTheDef $ setT
where
setT def@Function{} = def { funSplitTree = Just st }
setT def = def
modifyFunClauses :: QName -> ([Clause] -> [Clause]) -> TCM ()
modifyFunClauses q f =
modifySignature $ updateDefinition q $ updateTheDef $ updateFunClauses f
addClauses :: QName -> [Clause] -> TCM ()
addClauses q cls = do
tel <- getContextTelescope
modifySignature $ updateDefinition q $
updateTheDef (updateFunClauses (++ abstract tel cls))
. updateDefCopatternLHS (|| isCopatternLHS cls)
mkPragma :: String -> TCM CompilerPragma
mkPragma s = CompilerPragma <$> getCurrentRange <*> pure s
addPragma :: BackendName -> QName -> String -> TCM ()
addPragma b q s = ifM erased
(warning $ PragmaCompileErased b q)
$ do
pragma <- mkPragma s
modifySignature $ updateDefinition q $ addCompilerPragma b pragma
where
erased :: TCM Bool
erased = do
def <- theDef <$> getConstInfo q
case def of
Function{} ->
locallyTC eActiveBackendName (const $ Just b) $
locallyTCState stBackends (const $ builtinBackends) $
isErasable q
_ -> pure False
getUniqueCompilerPragma :: BackendName -> QName -> TCM (Maybe CompilerPragma)
getUniqueCompilerPragma backend q = do
ps <- defCompilerPragmas backend <$> getConstInfo q
case ps of
[] -> return Nothing
[p] -> return $ Just p
(_:p1:_) ->
setCurrentRange p1 $
genericDocError =<< do
hang (text ("Conflicting " ++ backend ++ " pragmas for") <+> pretty q <+> "at") 2 $
vcat [ "-" <+> pretty (getRange p) | p <- ps ]
setFunctionFlag :: FunctionFlag -> Bool -> QName -> TCM ()
setFunctionFlag flag val q = modifyGlobalDefinition q $ set (theDefLens . funFlag flag) val
markStatic :: QName -> TCM ()
markStatic = setFunctionFlag FunStatic True
markInline :: Bool -> QName -> TCM ()
markInline b = setFunctionFlag FunInline b
markInjective :: QName -> TCM ()
markInjective q = modifyGlobalDefinition q $ \def -> def { defInjective = True }
unionSignatures :: [Signature] -> Signature
unionSignatures ss = foldr unionSignature emptySignature ss
where
unionSignature (Sig a b c) (Sig a' b' c') =
Sig (Map.union a a')
(HMap.union b b')
(HMap.unionWith mappend c c')
addSection :: ModuleName -> TCM ()
addSection m = do
tel <- getContextTelescope
let sec = Section tel
whenJustM (getSection m) $ \ sec' -> do
if (sec == sec') then do
reportSDoc "tc.section" 10 $ "warning: redundantly adding existing section" <+> pretty m
reportSDoc "tc.section" 60 $ "with content" <+> pretty sec
else do
reportSDoc "impossible" 10 $ "overwriting existing section" <+> pretty m
reportSDoc "impossible" 60 $ "of content " <+> pretty sec'
reportSDoc "impossible" 60 $ "with content" <+> pretty sec
__IMPOSSIBLE__
setModuleCheckpoint m
modifySignature $ over sigSections $ Map.insert m sec
setModuleCheckpoint :: ModuleName -> TCM ()
setModuleCheckpoint m = do
chkpt <- viewTC eCurrentCheckpoint
stModuleCheckpoints `modifyTCLens` Map.insert m chkpt
{-# SPECIALIZE getSection :: ModuleName -> TCM (Maybe Section) #-}
{-# SPECIALIZE getSection :: ModuleName -> ReduceM (Maybe Section) #-}
getSection :: (Functor m, ReadTCState m) => ModuleName -> m (Maybe Section)
getSection m = do
sig <- (^. stSignature . sigSections) <$> getTCState
isig <- (^. stImports . sigSections) <$> getTCState
return $ Map.lookup m sig `mplus` Map.lookup m isig
{-# SPECIALIZE lookupSection :: ModuleName -> TCM Telescope #-}
{-# SPECIALIZE lookupSection :: ModuleName -> ReduceM Telescope #-}
lookupSection :: (Functor m, ReadTCState m) => ModuleName -> m Telescope
lookupSection m = maybe EmptyTel (^. secTelescope) <$> getSection m
addDisplayForms :: QName -> TCM ()
addDisplayForms x = do
def <- getConstInfo x
args <- drop (projectionArgs $ theDef def) <$> getContextArgs
add args x x $ map Apply $ raise 1 args
where
add args top x es0 = do
def <- getConstInfo x
let cs = defClauses def
isCopy = defCopy def
case cs of
[ cl ] -> do
if not isCopy
then noDispForm x "not a copy" else do
if not $ all (isVar . namedArg) $ namedClausePats cl
then noDispForm x "properly matching patterns" else do
let n = size $ namedClausePats cl
(es1, es2) = splitAt n es0
m = n - size es1
vs1 = map unArg $ fromMaybe __IMPOSSIBLE__ $ allApplyElims es1
sub = parallelS $ reverse $ vs1 ++ replicate m (var 0)
body = applySubst sub (compiledClauseBody cl) `applyE` es2
case unSpine <$> body of
Just (Def y es) -> do
let df = Display m es $ DTerm $ Def top $ map Apply args
reportSDoc "tc.display.section" 20 $ vcat
[ "adding display form " <+> pretty y <+> " --> " <+> pretty top
, text (show df)
]
addDisplayForm y df
add args top y es
Just v -> noDispForm x $ "not a def body, but " <+> pretty v
Nothing -> noDispForm x $ "bad body"
[] | Constructor{ conSrcCon = h } <- theDef def -> do
let y = conName h
df = Display 0 [] $ DTerm $ Con (h {conName = top }) ConOSystem []
reportSDoc "tc.display.section" 20 $ vcat
[ "adding display form" <+> pretty y <+> "-->" <+> pretty top
, text (show df)
]
addDisplayForm y df
[] -> noDispForm x "no clauses"
(_:_:_) -> noDispForm x "many clauses"
noDispForm x reason = reportSDoc "tc.display.section" 30 $
"no display form from" <+> pretty x <+> "because" <+> reason
isVar VarP{} = True
isVar _ = False
applySection
:: ModuleName
-> Telescope
-> ModuleName
-> Args
-> ScopeCopyInfo
-> TCM ()
applySection new ptel old ts ScopeCopyInfo{ renModules = rm, renNames = rd } = do
rd <- closeConstructors rd
applySection' new ptel old ts ScopeCopyInfo{ renModules = rm, renNames = rd }
where
closeConstructors :: Ren QName -> TCM (Ren QName)
closeConstructors rd = do
ds <- nubOn id . catMaybes <$> mapM (constructorData . fst) rd
cs <- nubOn id . concat <$> mapM (dataConstructors . fst) rd
new <- concat <$> mapM rename (ds ++ cs)
reportSDoc "tc.mod.apply.complete" 30 $
"also copying: " <+> pretty new
return $ new ++ rd
where
rename :: QName -> TCM (Ren QName)
rename x =
case lookup x rd of
Nothing -> do y <- freshName_ (show $ qnameName x)
return [(x, qnameFromList [y])]
Just{} -> return []
constructorData :: QName -> TCM (Maybe QName)
constructorData x = do
(theDef <$> getConstInfo x) <&> \case
Constructor{ conData = d } -> Just d
_ -> Nothing
dataConstructors :: QName -> TCM [QName]
dataConstructors x = do
(theDef <$> getConstInfo x) <&> \case
Datatype{ dataCons = cs } -> cs
Record{ recConHead = h } -> [conName h]
_ -> []
applySection' :: ModuleName -> Telescope -> ModuleName -> Args -> ScopeCopyInfo -> TCM ()
applySection' new ptel old ts ScopeCopyInfo{ renNames = rd, renModules = rm } = do
do
noCopyList <- catMaybes <$> mapM getName' constrainedPrims
forM_ (map fst rd) $ \ q -> do
when (q `elem` noCopyList) $ typeError (TriedToCopyConstrainedPrim q)
reportSDoc "tc.mod.apply" 10 $ vcat
[ "applySection"
, "new =" <+> pretty new
, "ptel =" <+> pretty ptel
, "old =" <+> pretty old
, "ts =" <+> pretty ts
]
mapM_ (copyDef ts) rd
mapM_ (copySec ts) rm
computePolarity (map snd rd)
where
copyName x = fromMaybe x $ lookup x rd
argsToUse x = do
let m = commonParentModule old x
reportSDoc "tc.mod.apply" 80 $ "Common prefix: " <+> pretty m
size <$> lookupSection m
copyDef :: Args -> (QName, QName) -> TCM ()
copyDef ts (x, y) = do
def <- getConstInfo x
np <- argsToUse (qnameModule x)
hidings <- map getHiding . telToList <$> lookupSection (qnameModule x)
let ts' = zipWith setHiding hidings ts
commonTel <- lookupSection (commonParentModule old $ qnameModule x)
reportSDoc "tc.mod.apply" 80 $ vcat
[ "copyDef" <+> pretty x <+> "->" <+> pretty y
, "ts' = " <+> pretty ts' ]
copyDef' ts' np def
where
copyDef' ts np d = do
reportSDoc "tc.mod.apply" 60 $ "making new def for" <+> pretty y <+> "from" <+> pretty x <+> "with" <+> text (show np) <+> "args" <+> text (show $ defAbstract d)
reportSDoc "tc.mod.apply" 80 $ vcat
[ "args = " <+> text (show ts')
, "old type = " <+> pretty (defType d) ]
reportSDoc "tc.mod.apply" 80 $
"new type = " <+> pretty t
addConstant y =<< nd y
makeProjection y
unless isCon $ whenJust inst $ \ c -> addNamedInstance y c
when (size ptel == 0) $ do
addDisplayForms y
where
ts' = take np ts
t = defType d `piApply` ts'
pol = defPolarity d `apply` ts'
occ = defArgOccurrences d `apply` ts'
gen = defArgGeneralizable d `apply` ts'
inst = defInstance d
nd :: QName -> TCM Definition
nd y = for def $ \ df -> Defn
{ defArgInfo = defArgInfo d
, defName = y
, defType = t
, defPolarity = pol
, defArgOccurrences = occ
, defArgGeneralizable = gen
, defGeneralizedParams = []
, defDisplay = []
, defMutual = -1
, defCompiledRep = noCompiledRep
, defInstance = inst
, defCopy = True
, defMatchable = Set.empty
, defNoCompilation = defNoCompilation d
, defInjective = False
, defCopatternLHS = isCopatternLHS [cl]
, theDef = df }
oldDef = theDef d
isCon = case oldDef of { Constructor{} -> True ; _ -> False }
mutual = case oldDef of { Function{funMutual = m} -> m ; _ -> Nothing }
extlam = case oldDef of { Function{funExtLam = e} -> e ; _ -> Nothing }
with = case oldDef of { Function{funWith = w} -> copyName <$> w ; _ -> Nothing }
isVar0 t = case unArg t of Var 0 [] -> True; _ -> False
proj = case oldDef of
Function{funProjection = Just p@Projection{projIndex = n}}
| size ts' < n || (size ts' == n && maybe True isVar0 (lastMaybe ts'))
-> Just $ p { projIndex = n - size ts'
, projLams = projLams p `apply` ts'
, projProper= fmap copyName $ projProper p
}
_ -> Nothing
def =
case oldDef of
Constructor{ conPars = np, conData = d } -> return $
oldDef { conPars = np - size ts'
, conData = copyName d
}
Datatype{ dataPars = np, dataCons = cs } -> return $
oldDef { dataPars = np - size ts'
, dataClause = Just cl
, dataCons = map copyName cs
}
Record{ recPars = np, recTel = tel } -> return $
oldDef { recPars = np - size ts'
, recClause = Just cl
, recTel = apply tel ts'
}
GeneralizableVar -> return GeneralizableVar
_ -> do
(mst, _, cc) <- compileClauses Nothing [cl]
let newDef =
set funMacro (oldDef ^. funMacro) $
set funStatic (oldDef ^. funStatic) $
set funInline True $
emptyFunction
{ funClauses = [cl]
, funCompiled = Just cc
, funSplitTree = mst
, funMutual = mutual
, funProjection = proj
, funTerminates = Just True
, funExtLam = extlam
, funWith = with
}
reportSDoc "tc.mod.apply" 80 $ ("new def for" <+> pretty x) <?> pretty newDef
return newDef
cl = Clause { clauseLHSRange = getRange $ defClauses d
, clauseFullRange = getRange $ defClauses d
, clauseTel = EmptyTel
, namedClausePats = []
, clauseBody = Just $ dropArgs pars $ case oldDef of
Function{funProjection = Just p} -> projDropParsApply p ProjSystem rel ts'
_ -> Def x $ map Apply ts'
, clauseType = Just $ defaultArg t
, clauseCatchall = False
, clauseUnreachable = Just False
, clauseEllipsis = NoEllipsis
}
where
pars = max 0 $ maybe 0 (pred . projIndex) proj
rel = getRelevance $ defArgInfo d
copySec :: Args -> (ModuleName, ModuleName) -> TCM ()
copySec ts (x, y) = do
totalArgs <- argsToUse x
tel <- lookupSection x
let sectionTel = apply tel $ take totalArgs ts
reportSDoc "tc.mod.apply" 80 $ "Copying section" <+> pretty x <+> "to" <+> pretty y
reportSDoc "tc.mod.apply" 80 $ " ts = " <+> mconcat (List.intersperse "; " (map pretty ts))
reportSDoc "tc.mod.apply" 80 $ " totalArgs = " <+> text (show totalArgs)
reportSDoc "tc.mod.apply" 80 $ " tel = " <+> text (List.intercalate " " (map (fst . unDom) $ telToList tel))
reportSDoc "tc.mod.apply" 80 $ " sectionTel = " <+> text (List.intercalate " " (map (fst . unDom) $ telToList ptel))
addContext sectionTel $ addSection y
addDisplayForm :: QName -> DisplayForm -> TCM ()
addDisplayForm x df = do
d <- makeOpen df
let add = updateDefinition x $ \ def -> def{ defDisplay = d : defDisplay def }
ifM (isLocal x)
(modifySignature add)
(stImportsDisplayForms `modifyTCLens` HMap.insertWith (++) x [d])
whenM (hasLoopingDisplayForm x) $
typeError . GenericDocError =<< do "Cannot add recursive display form for" <+> pretty x
isLocal :: ReadTCState m => QName -> m Bool
isLocal x = HMap.member x <$> useR (stSignature . sigDefinitions)
getDisplayForms :: (HasConstInfo m, ReadTCState m) => QName -> m [LocalDisplayForm]
getDisplayForms q = do
ds <- either (const []) defDisplay <$> getConstInfo' q
ds1 <- HMap.lookupDefault [] q <$> useR stImportsDisplayForms
ds2 <- HMap.lookupDefault [] q <$> useR stImportedDisplayForms
ifM (isLocal q) (return $ ds ++ ds1 ++ ds2)
(return $ ds1 ++ ds ++ ds2)
chaseDisplayForms :: QName -> TCM (Set QName)
chaseDisplayForms q = go Set.empty [q]
where
go used [] = pure used
go used (q : qs) = do
let rhs (Display _ _ e) = e
ds <- (`Set.difference` used) . Set.unions . map (namesIn . rhs . dget)
<$> (getDisplayForms q `catchError_` \ _ -> pure [])
go (Set.union ds used) (Set.toList ds ++ qs)
hasLoopingDisplayForm :: QName -> TCM Bool
hasLoopingDisplayForm q = Set.member q <$> chaseDisplayForms q
canonicalName :: HasConstInfo m => QName -> m QName
canonicalName x = do
def <- theDef <$> getConstInfo x
case def of
Constructor{conSrcCon = c} -> return $ conName c
Record{recClause = Just (Clause{ clauseBody = body })} -> can body
Datatype{dataClause = Just (Clause{ clauseBody = body })} -> can body
_ -> return x
where
can body = canonicalName $ extract $ fromMaybe __IMPOSSIBLE__ body
extract (Def x _) = x
extract _ = __IMPOSSIBLE__
sameDef :: HasConstInfo m => QName -> QName -> m (Maybe QName)
sameDef d1 d2 = do
c1 <- canonicalName d1
c2 <- canonicalName d2
if (c1 == c2) then return $ Just c1 else return Nothing
whatInduction :: MonadTCM tcm => QName -> tcm Induction
whatInduction c = liftTCM $ do
def <- theDef <$> getConstInfo c
mz <- getBuiltinName' builtinIZero
mo <- getBuiltinName' builtinIOne
case def of
Datatype{} -> return Inductive
Record{} | not (recRecursive def) -> return Inductive
Record{ recInduction = i } -> return $ fromMaybe Inductive i
Constructor{ conInd = i } -> return i
_ | Just c == mz || Just c == mo
-> return Inductive
_ -> __IMPOSSIBLE__
singleConstructorType :: QName -> TCM Bool
singleConstructorType q = do
d <- theDef <$> getConstInfo q
case d of
Record {} -> return True
Constructor { conData = d } -> do
di <- theDef <$> getConstInfo d
return $ case di of
Record {} -> True
Datatype { dataCons = cs } -> length cs == 1
_ -> __IMPOSSIBLE__
_ -> __IMPOSSIBLE__
data SigError
= SigUnknown String
| SigAbstract
sigError :: (String -> a) -> a -> SigError -> a
sigError f a = \case
SigUnknown s -> f s
SigAbstract -> a
class ( Functor m
, Applicative m
, Fail.MonadFail m
, HasOptions m
, MonadDebug m
, MonadTCEnv m
) => HasConstInfo m where
getConstInfo :: QName -> m Definition
getConstInfo q = getConstInfo' q >>= \case
Right d -> return d
Left (SigUnknown err) -> __IMPOSSIBLE_VERBOSE__ err
Left SigAbstract -> __IMPOSSIBLE_VERBOSE__ $
"Abstract, thus, not in scope: " ++ show q
getConstInfo' :: QName -> m (Either SigError Definition)
getRewriteRulesFor :: QName -> m RewriteRules
default getConstInfo'
:: (HasConstInfo n, MonadTrans t, m ~ t n)
=> QName -> m (Either SigError Definition)
getConstInfo' = lift . getConstInfo'
default getRewriteRulesFor
:: (HasConstInfo n, MonadTrans t, m ~ t n)
=> QName -> m RewriteRules
getRewriteRulesFor = lift . getRewriteRulesFor
{-# SPECIALIZE getConstInfo :: QName -> TCM Definition #-}
defaultGetRewriteRulesFor :: (Monad m) => m TCState -> QName -> m RewriteRules
defaultGetRewriteRulesFor getTCState q = do
st <- getTCState
let sig = st^.stSignature
imp = st^.stImports
look s = HMap.lookup q $ s ^. sigRewriteRules
return $ mconcat $ catMaybes [look sig, look imp]
getOriginalProjection :: HasConstInfo m => QName -> m QName
getOriginalProjection q = projOrig . fromMaybe __IMPOSSIBLE__ <$> isProjection q
instance HasConstInfo (TCMT IO) where
getRewriteRulesFor = defaultGetRewriteRulesFor getTC
getConstInfo' q = do
st <- getTC
env <- askTC
defaultGetConstInfo st env q
getConstInfo q = getConstInfo' q >>= \case
Right d -> return d
Left (SigUnknown err) -> fail err
Left SigAbstract -> notInScopeError $ qnameToConcrete q
defaultGetConstInfo
:: (HasOptions m, MonadDebug m, MonadTCEnv m)
=> TCState -> TCEnv -> QName -> m (Either SigError Definition)
defaultGetConstInfo st env q = do
let defs = st^.(stSignature . sigDefinitions)
idefs = st^.(stImports . sigDefinitions)
case catMaybes [HMap.lookup q defs, HMap.lookup q idefs] of
[] -> return $ Left $ SigUnknown $ "Unbound name: " ++ show q ++ showQNameId q
[d] -> mkAbs env d
ds -> __IMPOSSIBLE_VERBOSE__ $ "Ambiguous name: " ++ show q
where
mkAbs env d
| treatAbstractly' q' env =
case makeAbstract d of
Just d -> return $ Right d
Nothing -> return $ Left SigAbstract
| otherwise = return $ Right d
where
q' = case theDef d of
Constructor{} -> dropLastModule q
_ -> q
dropLastModule q@QName{ qnameModule = m } =
q{ qnameModule = mnameFromList $ ifNull (mnameToList m) __IMPOSSIBLE__ init }
instance HasConstInfo m => HasConstInfo (ChangeT m)
instance HasConstInfo m => HasConstInfo (ExceptT err m)
instance HasConstInfo m => HasConstInfo (IdentityT m)
instance HasConstInfo m => HasConstInfo (ListT m)
instance HasConstInfo m => HasConstInfo (MaybeT m)
instance HasConstInfo m => HasConstInfo (ReaderT r m)
instance HasConstInfo m => HasConstInfo (StateT s m)
instance (Monoid w, HasConstInfo m) => HasConstInfo (WriterT w m)
{-# INLINE getConInfo #-}
getConInfo :: HasConstInfo m => ConHead -> m Definition
getConInfo = getConstInfo . conName
getPolarity :: HasConstInfo m => QName -> m [Polarity]
getPolarity q = defPolarity <$> getConstInfo q
getPolarity' :: HasConstInfo m => Comparison -> QName -> m [Polarity]
getPolarity' CmpEq q = map (composePol Invariant) <$> getPolarity q
getPolarity' CmpLeq q = getPolarity q
setPolarity :: QName -> [Polarity] -> TCM ()
setPolarity q pol = do
reportSDoc "tc.polarity.set" 20 $
"Setting polarity of" <+> pretty q <+> "to" <+> pretty pol <> "."
modifySignature $ updateDefinition q $ updateDefPolarity $ const pol
getForcedArgs :: HasConstInfo m => QName -> m [IsForced]
getForcedArgs q = defForced <$> getConstInfo q
getArgOccurrence :: QName -> Nat -> TCM Occurrence
getArgOccurrence d i = do
def <- getConstInfo d
return $! case theDef def of
Constructor{} -> StrictPos
_ -> fromMaybe Mixed $ defArgOccurrences def !!! i
setArgOccurrences :: QName -> [Occurrence] -> TCM ()
setArgOccurrences d os = modifyArgOccurrences d $ const os
modifyArgOccurrences :: QName -> ([Occurrence] -> [Occurrence]) -> TCM ()
modifyArgOccurrences d f =
modifySignature $ updateDefinition d $ updateDefArgOccurrences f
setTreeless :: QName -> TTerm -> TCM ()
setTreeless q t =
modifyGlobalDefinition q $ updateTheDef $ \case
fun@Function{} -> fun{ funTreeless = Just $ Compiled t [] }
_ -> __IMPOSSIBLE__
setCompiledArgUse :: QName -> [Bool] -> TCM ()
setCompiledArgUse q use =
modifyGlobalDefinition q $ updateTheDef $ \case
fun@Function{} ->
fun{ funTreeless = for (funTreeless fun) $ \ c -> c { cArgUsage = use } }
_ -> __IMPOSSIBLE__
getCompiled :: QName -> TCM (Maybe Compiled)
getCompiled q = do
(theDef <$> getConstInfo q) <&> \case
Function{ funTreeless = t } -> t
_ -> Nothing
getErasedConArgs :: QName -> TCM [Bool]
getErasedConArgs q = do
def <- getConstInfo q
case theDef def of
Constructor{ conArity, conErased } -> return $
fromMaybe (replicate conArity False) conErased
_ -> __IMPOSSIBLE__
setErasedConArgs :: QName -> [Bool] -> TCM ()
setErasedConArgs q args = modifyGlobalDefinition q $ updateTheDef $ \case
def@Constructor{ conArity }
| length args == conArity -> def{ conErased = Just args }
| otherwise -> __IMPOSSIBLE__
def -> def
getTreeless :: QName -> TCM (Maybe TTerm)
getTreeless q = fmap cTreeless <$> getCompiled q
getCompiledArgUse :: QName -> TCM [Bool]
getCompiledArgUse q = maybe [] cArgUsage <$> getCompiled q
addDataCons :: QName -> [QName] -> TCM ()
addDataCons d cs = modifySignature $ updateDefinition d $ updateTheDef $ \ def ->
let !cs' = cs ++ dataCons def in
case def of
Datatype{} -> def {dataCons = cs' }
_ -> __IMPOSSIBLE__
getMutual :: QName -> TCM (Maybe [QName])
getMutual d = getMutual_ . theDef <$> getConstInfo d
getMutual_ :: Defn -> Maybe [QName]
getMutual_ = \case
Function { funMutual = m } -> m
Datatype { dataMutual = m } -> m
Record { recMutual = m } -> m
_ -> Nothing
setMutual :: QName -> [QName] -> TCM ()
setMutual d m = modifySignature $ updateDefinition d $ updateTheDef $ \ def ->
case def of
Function{} -> def { funMutual = Just m }
Datatype{} -> def {dataMutual = Just m }
Record{} -> def { recMutual = Just m }
_ -> if null m then def else __IMPOSSIBLE__
mutuallyRecursive :: QName -> QName -> TCM Bool
mutuallyRecursive d d1 = (d `elem`) . fromMaybe __IMPOSSIBLE__ <$> getMutual d1
definitelyNonRecursive_ :: Defn -> Bool
definitelyNonRecursive_ = maybe False null . getMutual_
getCurrentModuleFreeVars :: TCM Nat
getCurrentModuleFreeVars = size <$> (lookupSection =<< currentModule)
getDefModule :: HasConstInfo m => QName -> m (Either SigError ModuleName)
getDefModule f = mapRight modName <$> getConstInfo' f
where
modName def = case theDef def of
Function{ funExtLam = Just (ExtLamInfo m _) } -> m
_ -> qnameModule f
getDefFreeVars :: (Functor m, Applicative m, ReadTCState m, MonadTCEnv m) => QName -> m Nat
getDefFreeVars = getModuleFreeVars . qnameModule
freeVarsToApply :: (Functor m, HasConstInfo m, HasOptions m,
ReadTCState m, MonadTCEnv m, MonadDebug m)
=> QName -> m Args
freeVarsToApply q = do
vs <- moduleParamsToApply $ qnameModule q
t <- defType <$> getConstInfo q
let TelV tel _ = telView'UpTo (size vs) t
unless (size tel == size vs) __IMPOSSIBLE__
return $ zipWith (\ arg dom -> unArg arg <$ argFromDom dom) vs $ telToList tel
{-# SPECIALIZE getModuleFreeVars :: ModuleName -> TCM Nat #-}
{-# SPECIALIZE getModuleFreeVars :: ModuleName -> ReduceM Nat #-}
getModuleFreeVars :: (Functor m, Applicative m, MonadTCEnv m, ReadTCState m)
=> ModuleName -> m Nat
getModuleFreeVars m = do
m0 <- commonParentModule m <$> currentModule
(+) <$> getAnonymousVariables m <*> (size <$> lookupSection m0)
moduleParamsToApply :: (Functor m, Applicative m, HasOptions m,
MonadTCEnv m, ReadTCState m, MonadDebug m)
=> ModuleName -> m Args
moduleParamsToApply m = do
traceSDoc "tc.sig.param" 90 ("computing module parameters of " <+> pretty m) $ do
n <- getModuleFreeVars m
traceSDoc "tc.sig.param" 60 (nest 2 $ "n = " <+> text (show n)) $ do
tel <- take n . telToList <$> lookupSection m
traceSDoc "tc.sig.param" 60 (nest 2 $ "tel = " <+> pretty tel) $ do
sub <- getModuleParameterSub m
traceSDoc "tc.sig.param" 60 (do
cxt <- getContext
nest 2 $ vcat
[ "cxt = " <+> prettyTCM (PrettyContext cxt)
, "sub = " <+> pretty sub
]) $ do
unless (size tel == n) __IMPOSSIBLE__
let args = applySubst sub $ zipWith (\ i a -> var i <$ argFromDom a) (downFrom n) tel
traceSDoc "tc.sig.param" 60 (nest 2 $ "args = " <+> prettyList_ (map pretty args)) $ do
getSection m >>= \case
Nothing -> do
return args
Just (Section stel) -> do
when (size stel < size args) __IMPOSSIBLE__
return $ zipWith (\ !dom (Arg _ v) -> v <$ argFromDom dom) (telToList stel) args
inFreshModuleIfFreeParams :: TCM a -> TCM a
inFreshModuleIfFreeParams k = do
sub <- getModuleParameterSub =<< currentModule
if sub == IdS then k else do
m <- currentModule
m' <- qualifyM m . mnameFromList . (:[]) <$>
freshName_ ("_" :: String)
addSection m'
withCurrentModule m' k
{-# SPECIALIZE instantiateDef :: Definition -> TCM Definition #-}
instantiateDef
:: ( Functor m, HasConstInfo m, HasOptions m
, ReadTCState m, MonadTCEnv m, MonadDebug m )
=> Definition -> m Definition
instantiateDef d = do
vs <- freeVarsToApply $ defName d
verboseS "tc.sig.inst" 30 $ do
ctx <- getContext
m <- currentModule
reportSDoc "tc.sig.inst" 30 $
"instDef in" <+> pretty m <> ":" <+> pretty (defName d) <+>
text (unwords $ map show $ zipWith (<$) (reverse $ map (fst . unDom) ctx) vs)
return $ d `apply` vs
instantiateRewriteRule :: (Functor m, HasConstInfo m, HasOptions m,
ReadTCState m, MonadTCEnv m, MonadDebug m)
=> RewriteRule -> m RewriteRule
instantiateRewriteRule rew = do
traceSDoc "rewriting" 95 ("instantiating rewrite rule" <+> pretty (rewName rew) <+> "to the local context.") $ do
vs <- freeVarsToApply $ rewName rew
let rew' = rew `apply` vs
traceSLn "rewriting" 95 ("instantiated rewrite rule: ") $ do
traceSLn "rewriting" 95 (show rew') $ do
return rew'
instantiateRewriteRules :: (Functor m, HasConstInfo m, HasOptions m,
ReadTCState m, MonadTCEnv m, MonadDebug m)
=> RewriteRules -> m RewriteRules
instantiateRewriteRules = mapM instantiateRewriteRule
makeAbstract :: Definition -> Maybe Definition
makeAbstract d =
case defAbstract d of
ConcreteDef -> return d
AbstractDef -> do
def <- makeAbs $ theDef d
return d { defArgOccurrences = []
, defPolarity = []
, theDef = def
}
where
makeAbs Axiom = Just Axiom
makeAbs d@DataOrRecSig{} = Just d
makeAbs d@GeneralizableVar{} = Just d
makeAbs d@Datatype {} = Just $ AbstractDefn d
makeAbs d@Function {} = Just $ AbstractDefn d
makeAbs Constructor{} = Nothing
makeAbs d@Record{} = Just $ AbstractDefn d
makeAbs Primitive{} = __IMPOSSIBLE__
makeAbs AbstractDefn{}= __IMPOSSIBLE__
{-# SPECIALIZE inAbstractMode :: TCM a -> TCM a #-}
inAbstractMode :: MonadTCEnv m => m a -> m a
inAbstractMode = localTC $ \e -> e { envAbstractMode = AbstractMode }
{-# SPECIALIZE inConcreteMode :: TCM a -> TCM a #-}
inConcreteMode :: MonadTCEnv m => m a -> m a
inConcreteMode = localTC $ \e -> e { envAbstractMode = ConcreteMode }
ignoreAbstractMode :: MonadTCEnv m => m a -> m a
ignoreAbstractMode = localTC $ \e -> e { envAbstractMode = IgnoreAbstractMode }
{-# SPECIALIZE inConcreteOrAbstractMode :: QName -> (Definition -> TCM a) -> TCM a #-}
inConcreteOrAbstractMode :: (MonadTCEnv m, HasConstInfo m) => QName -> (Definition -> m a) -> m a
inConcreteOrAbstractMode q cont = do
def <- ignoreAbstractMode $ getConstInfo q
case defAbstract def of
AbstractDef -> inAbstractMode $ cont def
ConcreteDef -> inConcreteMode $ cont def
treatAbstractly :: MonadTCEnv m => QName -> m Bool
treatAbstractly q = asksTC $ treatAbstractly' q
treatAbstractly' :: QName -> TCEnv -> Bool
treatAbstractly' q env = case envAbstractMode env of
ConcreteMode -> True
IgnoreAbstractMode -> False
AbstractMode -> not $ current `isLeChildModuleOf` m
where
current = dropAnon $ envCurrentModule env
m = dropAnon $ qnameModule q
dropAnon (MName ms) = MName $ List.dropWhileEnd isNoName ms
{-# SPECIALIZE typeOfConst :: QName -> TCM Type #-}
typeOfConst :: (HasConstInfo m, ReadTCState m) => QName -> m Type
typeOfConst q = defType <$> (instantiateDef =<< getConstInfo q)
{-# SPECIALIZE relOfConst :: QName -> TCM Relevance #-}
relOfConst :: HasConstInfo m => QName -> m Relevance
relOfConst q = getRelevance <$> getConstInfo q
{-# SPECIALIZE modalityOfConst :: QName -> TCM Modality #-}
modalityOfConst :: HasConstInfo m => QName -> m Modality
modalityOfConst q = getModality <$> getConstInfo q
droppedPars :: Definition -> Int
droppedPars d = case theDef d of
Axiom{} -> 0
DataOrRecSig{} -> 0
GeneralizableVar{} -> 0
def@Function{} -> projectionArgs def
Datatype {dataPars = _} -> 0
Record {recPars = _} -> 0
Constructor{conPars = n} -> n
Primitive{} -> 0
AbstractDefn{} -> __IMPOSSIBLE__
{-# SPECIALIZE isProjection :: QName -> TCM (Maybe Projection) #-}
isProjection :: HasConstInfo m => QName -> m (Maybe Projection)
isProjection qn = isProjection_ . theDef <$> getConstInfo qn
isProjection_ :: Defn -> Maybe Projection
isProjection_ def =
case def of
Function { funProjection = result } -> result
_ -> Nothing
isStaticFun :: Defn -> Bool
isStaticFun = (^. funStatic)
isInlineFun :: Defn -> Bool
isInlineFun = (^. funInline)
isProperProjection :: Defn -> Bool
isProperProjection d = caseMaybe (isProjection_ d) False $ \ isP ->
if projIndex isP <= 0 then False else isJust $ projProper isP
projectionArgs :: Defn -> Int
projectionArgs = maybe 0 (max 0 . pred . projIndex) . isProjection_
usesCopatterns :: (HasConstInfo m) => QName -> m Bool
usesCopatterns q = defCopatternLHS <$> getConstInfo q
applyDef :: (HasConstInfo m)
=> ProjOrigin -> QName -> Arg Term -> m Term
applyDef o f a = do
let fallback = return $ Def f [Apply a]
caseMaybeM (isProjection f) fallback $ \ isP -> do
if projIndex isP <= 0 then fallback else do
if isNothing (projProper isP) then fallback else do
return $ unArg a `applyE` [Proj o $ projOrig isP]