module Agda.TypeChecking.Monad.Signature where
import Prelude hiding (null)
import Control.Arrow (first, second, (***))
import Control.Applicative hiding (empty)
import Control.Monad.State
import Control.Monad.Reader
import Control.Monad.Trans.Maybe
import Data.List hiding (null)
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Maybe
import Data.Monoid
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 qualified Agda.Compiler.UHC.Pragmas.Base as CR
import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Monad.Context
import Agda.TypeChecking.Monad.Options
import Agda.TypeChecking.Monad.Env
import Agda.TypeChecking.Monad.Exception ( ExceptionT )
import Agda.TypeChecking.Monad.Mutual
import Agda.TypeChecking.Monad.Open
import Agda.TypeChecking.Monad.Local
import Agda.TypeChecking.Monad.State
import Agda.TypeChecking.Positivity.Occurrence
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.CompiledClause.Compile
import Agda.TypeChecking.Polarity
import Agda.TypeChecking.ProjectionLike
import Agda.Utils.Except ( Error )
import Agda.Utils.Functor
import Agda.Utils.Lens
import Agda.Utils.List
import Agda.Utils.Map as Map
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.Permutation
import Agda.Utils.Pretty
import Agda.Utils.Size
import qualified Agda.Utils.HashMap as HMap
#include "undefined.h"
import Agda.Utils.Impossible
addConstant :: QName -> Definition -> TCM ()
addConstant q d = do
reportSLn "tc.signature" 20 $ "adding constant " ++ show q ++ " to signature"
tel <- getContextTelescope
let tel' = replaceEmptyName "r" $ killRange $ case theDef d of
Constructor{} -> fmap hideOrKeepInstance tel
Function{ funProjection = Just Projection{ projProper = True, 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 }
reportSLn "tc.signature" 30 $ "lambda-lifted definition = " ++ show 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 $ setT
where
setT def@Function{} = def { funTerminates = Just b }
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
modifyFunClauses q (++ abstract tel cls)
ensureNoCompiledHaskell :: QName -> TCM ()
ensureNoCompiledHaskell q =
whenM (isJust . compiledHaskell . defCompiledRep <$> getConstInfo q) $
typeError $ GenericError $ "Multiple Haskell bindings for " ++ show q ++ ". " ++
"Note that builtin numbers, booleans, chars and strings don't need " ++
"COMPILED pragmas."
addHaskellCode :: QName -> HaskellType -> HaskellCode -> TCM ()
addHaskellCode q hsTy hsDef = do
ensureNoCompiledHaskell q
modifySignature $ updateDefinition q $ updateDefCompiledRep $ addHs
where
addHs crep = crep { compiledHaskell = Just $ HsDefn hsTy hsDef }
addHaskellExport :: QName -> HaskellType -> String -> TCM ()
addHaskellExport q hsTy hsName = do
ensureNoCompiledHaskell q
modifySignature $ updateDefinition q $ updateDefCompiledRep $ addHs
where
addHs crep = crep { exportHaskell = Just (HsExport hsTy hsName)}
addHaskellType :: QName -> HaskellType -> TCM ()
addHaskellType q hsTy = do
ensureNoCompiledHaskell q
modifySignature $ updateDefinition q $ updateDefCompiledRep $ addHs
where
addHs crep = crep { compiledHaskell = Just $ HsType hsTy }
addEpicCode :: QName -> EpicCode -> TCM ()
addEpicCode q epDef = modifySignature $ updateDefinition q $ updateDefCompiledRep $ addEp
where
addEp crep = crep { compiledEpic = Just epDef }
addJSCode :: QName -> String -> TCM ()
addJSCode q jsDef = modifySignature $ updateDefinition q $ updateDefCompiledRep $ addJS
where
addJS crep = crep { compiledJS = Just jsDef }
addCoreCode :: QName -> CR.CoreExpr -> TCM ()
addCoreCode q crDef = modifySignature $ updateDefinition q $ updateDefCompiledRep $ addCore crDef
where
addCore e crep = crep { compiledCore = Just $ CrDefn e }
addCoreConstr :: QName -> CR.CoreConstr -> TCM ()
addCoreConstr q con = modifySignature $ updateDefinition q $ updateDefCompiledRep $ addCore
where
addCore crep = crep {compiledCore = Just $ CrConstr con }
addCoreType :: QName -> CR.CoreType -> TCM ()
addCoreType q crTy = modifySignature $ updateDefinition q $ updateDefCompiledRep $ addCr
where
addCr crep = crep { compiledCore = Just $ CrType crTy }
setFunctionFlag :: FunctionFlag -> Bool -> QName -> TCM ()
setFunctionFlag flag val q = modifyGlobalDefinition q $ set (theDefLens . funFlag flag) val
markStatic :: QName -> TCM ()
markStatic = setFunctionFlag FunStatic True
markInline :: QName -> TCM ()
markInline = setFunctionFlag FunInline 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
reportSLn "tc.section" 10 $ "warning: redundantly adding existing section " ++ show m
reportSLn "tc.section" 60 $ "with content " ++ show sec
else do
reportSLn "impossible" 10 $ "overwriting existing section " ++ show m
reportSLn "impossible" 60 $ "of content " ++ show sec'
reportSLn "impossible" 60 $ "with content " ++ show sec
__IMPOSSIBLE__
setDefaultModuleParameters m
modifySignature $ over sigSections $ Map.insert m sec
setDefaultModuleParameters :: ModuleName -> TCM ()
setDefaultModuleParameters m =
stModuleParameters %= Map.insert m defaultModuleParameters
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
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
reportSLn "tc.display.section" 20 $ "adding display form " ++ show y ++ " --> " ++ show top
++ "\n " ++ show df
addDisplayForm y df
add args top y es
Just v -> noDispForm x $ "not a def body, but " ++ show 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 []
reportSLn "tc.display.section" 20 $ "adding display form " ++ show y ++ " --> " ++ show top
++ "\n " ++ show df
addDisplayForm y df
[] -> noDispForm x "no clauses"
(_:_:_) -> noDispForm x "many clauses"
noDispForm x reason = reportSLn "tc.display.section" 30 $
"no display form from " ++ show 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 rd = do
ds <- nub . concat <$> mapM (constructorData . fst) rd
cs <- nub . concat <$> mapM (dataConstructors . fst) rd
new <- concat <$> mapM rename (ds ++ cs)
reportSLn "tc.mod.apply.complete" 30 $
"also copying: " ++ show new
return $ new ++ rd
where
rename x =
case lookup x rd of
Nothing -> do y <- freshName_ (show x)
return [(x, qnameFromList [y])]
Just{} -> return []
constructorData x = do
def <- theDef <$> getConstInfo x
return $ case def of
Constructor{ conData = d } -> [d]
_ -> []
dataConstructors x = do
def <- theDef <$> getConstInfo x
return $ case def of
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
reportSLn "tc.mod.apply" 10 $ render $ vcat
[ text "applySection"
, text "new =" <+> text (show new)
, text "ptel =" <+> text (show ptel)
, text "old =" <+> text (show old)
, text "ts =" <+> text (show ts)
]
reportSLn "tc.mod.apply" 80 $ render $ vcat
[ text "arguments: " <+> text (show ts)
]
mapM_ (copyDef ts) rd
mapM_ (copySec ts) rm
mapM_ computePolarity (map snd rd)
where
copyName x = fromMaybe x $ lookup x rd
argsToUse x = do
let m = commonParentModule old x
reportSLn "tc.mod.apply" 80 $ "Common prefix: " ++ show m
size <$> lookupSection m
copyDef :: Args -> (QName, QName) -> TCM ()
copyDef ts (x, y) = do
def <- getConstInfo x
np <- argsToUse (qnameModule x)
copyDef' np def
where
copyDef' np d = do
reportSLn "tc.mod.apply" 60 $ "making new def for " ++ show y ++ " from " ++ show x ++ " with " ++ show np ++ " args " ++ show (defAbstract d)
reportSLn "tc.mod.apply" 80 $
"args = " ++ show ts' ++ "\n" ++
"old type = " ++ prettyShow (defType d)
reportSLn "tc.mod.apply" 80 $
"new type = " ++ prettyShow 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'
inst = defInstance d
nd :: QName -> TCM Definition
nd y = for def $ \ df -> Defn
{ defArgInfo = defArgInfo d
, defName = y
, defType = t
, defPolarity = pol
, defArgOccurrences = occ
, defDisplay = []
, defMutual = 1
, defCompiledRep = noCompiledRep
, defInstance = inst
, defCopy = True
, defMatchable = False
, theDef = df }
oldDef = theDef d
isCon = case oldDef of { Constructor{} -> True ; _ -> False }
mutual = case oldDef of { Function{funMutual = m} -> m ; _ -> [] }
extlam = case oldDef of { Function{funExtLam = e} -> e ; _ -> Nothing }
with = case oldDef of { Function{funWith = w} -> copyName <$> w ; _ -> Nothing }
isVar0 t = case ignoreSharing $ 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'
}
_ -> 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'
}
_ -> do
cc <- compileClauses Nothing [cl]
let newDef =
set funMacro (oldDef ^. funMacro) $
set funStatic (oldDef ^. funStatic) $
set funInline True $
emptyFunction
{ funClauses = [cl]
, funCompiled = Just cc
, funMutual = mutual
, funProjection = proj
, funTerminates = Just True
, funExtLam = extlam
, funWith = with
, funCopatternLHS = isCopatternLHS [cl]
}
reportSLn "tc.mod.apply" 80 $ "new def for " ++ show x ++ "\n " ++ show newDef
return newDef
cl = Clause { clauseRange = getRange $ defClauses d
, clauseTel = EmptyTel
, namedClausePats = []
, clauseBody = Just $ case oldDef of
Function{funProjection = Just p} -> projDropParsApply p ProjSystem ts'
_ -> Def x $ map Apply ts'
, clauseType = Just $ defaultArg t
, clauseCatchall = False
}
copySec :: Args -> (ModuleName, ModuleName) -> TCM ()
copySec ts (x, y) = do
totalArgs <- argsToUse x
tel <- lookupSection x
let sectionTel = apply tel $ take totalArgs ts
reportSLn "tc.mod.apply" 80 $ "Copying section " ++ show x ++ " to " ++ show y
reportSLn "tc.mod.apply" 80 $ " ts = " ++ intercalate "; " (map prettyShow ts)
reportSLn "tc.mod.apply" 80 $ " totalArgs = " ++ show totalArgs
reportSLn "tc.mod.apply" 80 $ " tel = " ++ intercalate " " (map (fst . unDom) $ telToList tel)
reportSLn "tc.mod.apply" 80 $ " sectionTel = " ++ intercalate " " (map (fst . unDom) $ telToList ptel)
addContext sectionTel $ addSection y
addDisplayForm :: QName -> DisplayForm -> TCM ()
addDisplayForm x df = do
d <- makeLocal df
let add = updateDefinition x $ \ def -> def{ defDisplay = d : defDisplay def }
ifM (isLocal x)
(modifySignature add)
(stImportsDisplayForms %= HMap.insertWith (++) x [d])
whenM (hasLoopingDisplayForm x) $
typeError . GenericDocError $ text "Cannot add recursive display form for" <+> pretty x
isLocal :: QName -> TCM Bool
isLocal x = isJust . HMap.lookup x <$> use (stSignature . sigDefinitions)
getDisplayForms :: QName -> TCM [LocalDisplayForm]
getDisplayForms q = do
ds <- defDisplay <$> getConstInfo q
ds1 <- maybe [] id . HMap.lookup q <$> use stImportsDisplayForms
ds2 <- maybe [] id . HMap.lookup q <$> use 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 :: QName -> TCM 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 (Shared p) = extract $ derefPtr p
extract _ = __IMPOSSIBLE__
sameDef :: QName -> QName -> TCM (Maybe QName)
sameDef d1 d2 = do
c1 <- canonicalName d1
c2 <- canonicalName d2
if (c1 == c2) then return $ Just c1 else return Nothing
whatInduction :: QName -> TCM Induction
whatInduction c = do
def <- theDef <$> getConstInfo c
case def of
Datatype{ dataInduction = i } -> return i
Record{ recRecursive = False} -> return Inductive
Record{ recInduction = i } -> return $ fromMaybe Inductive i
Constructor{ conInd = i } -> return i
_ -> __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__
class (Functor m, Applicative m, Monad m) => HasConstInfo m where
getConstInfo :: QName -> m Definition
getRewriteRulesFor :: QName -> m RewriteRules
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 get
getConstInfo q = join $ pureTCM $ \st env ->
let defs = st^.(stSignature . sigDefinitions)
idefs = st^.(stImports . sigDefinitions)
in case catMaybes [HMap.lookup q defs, HMap.lookup q idefs] of
[] -> fail $ "Unbound name: " ++ show q ++ " " ++ showQNameId q
[d] -> mkAbs env d
ds -> fail $ "Ambiguous name: " ++ show q
where
mkAbs env d
| treatAbstractly' q' env =
case makeAbstract d of
Just d -> return d
Nothing -> notInScope $ qnameToConcrete q
| otherwise = return 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 (MaybeT m) where
getConstInfo = lift . getConstInfo
getRewriteRulesFor = lift . getRewriteRulesFor
instance (HasConstInfo m, Error err) => HasConstInfo (ExceptionT err m) where
getConstInfo = lift . getConstInfo
getRewriteRulesFor = lift . getRewriteRulesFor
getConInfo :: MonadTCM tcm => ConHead -> tcm Definition
getConInfo = liftTCM . getConstInfo . conName
getPolarity :: QName -> TCM [Polarity]
getPolarity q = defPolarity <$> getConstInfo q
getPolarity' :: Comparison -> QName -> TCM [Polarity]
getPolarity' CmpEq q = map (composePol Invariant) <$> getPolarity q
getPolarity' CmpLeq q = getPolarity q
setPolarity :: QName -> [Polarity] -> TCM ()
setPolarity q pol = do
reportSLn "tc.polarity.set" 20 $
"Setting polarity of " ++ show q ++ " to " ++ show pol ++ "."
modifySignature $ updateDefinition q $ updateDefPolarity $ const pol
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 $ setTT
where
setTT def@Defn{theDef = fun@Function{}} =
def{theDef = fun{funTreeless = Just (Compiled t [])}}
setTT def = __IMPOSSIBLE__
setCompiledArgUse :: QName -> [Bool] -> TCM ()
setCompiledArgUse q use = modifyGlobalDefinition q $ setTT
where
setTT def@Defn{theDef = fun@Function{}} =
def{theDef = fun{funTreeless = for (funTreeless fun) $ \ c -> c { cArgUsage = use }}}
setTT def = __IMPOSSIBLE__
getCompiled :: QName -> TCM (Maybe Compiled)
getCompiled q = do
def <- theDef <$> getConstInfo q
return $ case def of
Function{ funTreeless = t } -> t
_ -> Nothing
getErasedConArgs :: QName -> TCM [Bool]
getErasedConArgs q = do
def <- getConstInfo q
case theDef def of
Constructor{ conData = d, conPars = np, conErased = es } -> do
ddef <- getConstInfo d
case compiledHaskell $ defCompiledRep ddef of
Nothing -> return es
Just _ -> do
TelV tel _ <- telView $ defType def
return $ replicate (size tel np) False
_ -> __IMPOSSIBLE__
setErasedConArgs :: QName -> [Bool] -> TCM ()
setErasedConArgs q args = modifyGlobalDefinition q setArgs
where
setArgs def@Defn{theDef = con@Constructor{}} =
def{ theDef = con{ conErased = args } }
setArgs def = def
getTreeless :: QName -> TCM (Maybe TTerm)
getTreeless q = fmap cTreeless <$> getCompiled q
getCompiledArgUse :: QName -> TCM [Bool]
getCompiledArgUse q = maybe [] cArgUsage <$> getCompiled q
getMutual :: QName -> TCM [QName]
getMutual d = do
def <- theDef <$> getConstInfo d
return $ case def of
Function { funMutual = m } -> m
Datatype { dataMutual = m } -> m
Record { recMutual = m } -> m
_ -> []
setMutual :: QName -> [QName] -> TCM ()
setMutual d m = modifySignature $ updateDefinition d $ updateTheDef $ \ def ->
case def of
Function{} -> def { funMutual = m }
Datatype{} -> def {dataMutual = m }
Record{} -> def { recMutual = m }
_ -> __IMPOSSIBLE__
mutuallyRecursive :: QName -> QName -> TCM Bool
mutuallyRecursive d d' = (d `elem`) <$> getMutual d'
getCurrentModuleFreeVars :: TCM Nat
getCurrentModuleFreeVars = size <$> (lookupSection =<< currentModule)
getDefFreeVars :: (Functor m, Applicative m, ReadTCState m, MonadReader TCEnv m) => QName -> m Nat
getDefFreeVars = getModuleFreeVars . qnameModule
freeVarsToApply :: QName -> TCM Args
freeVarsToApply = moduleParamsToApply . qnameModule
getModuleFreeVars :: (Functor m, Applicative m, ReadTCState m, MonadReader TCEnv m) => ModuleName -> m Nat
getModuleFreeVars m = do
m0 <- commonParentModule m <$> currentModule
(+) <$> getAnonymousVariables m <*> (size <$> lookupSection m0)
moduleParamsToApply :: ModuleName -> TCM Args
moduleParamsToApply m = do
reportSLn "tc.sig.param" 90 $ "computing module parameters of " ++ show m
cxt <- getContext
n <- getModuleFreeVars m
tel <- take n . telToList <$> lookupSection m
sub <- getModuleParameterSub m
reportSLn "tc.sig.param" 60 $ unlines $
[ " n = " ++ show n
, " cxt = " ++ show (map (fmap fst) cxt)
, " sub = " ++ show sub
]
unless (size tel == n) __IMPOSSIBLE__
let args = applySubst sub $ zipWith (\ i a -> var i <$ argFromDom a) (downFrom n) tel
reportSLn "tc.sig.param" 60 $ " args = " ++ show args
getSection m >>= \case
Nothing -> do
return args
Just (Section stel) -> do
when (size stel < size args) __IMPOSSIBLE__
return $ zipWith (\ (Dom ai _) (Arg _ v) -> Arg ai v) (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_ "_"
addSection m'
withCurrentModule m' k
instantiateDef :: Definition -> TCM Definition
instantiateDef d = do
vs <- freeVarsToApply $ defName d
verboseS "tc.sig.inst" 30 $ do
ctx <- getContext
m <- currentModule
reportSLn "tc.sig.inst" 30 $
"instDef in " ++ show m ++ ": " ++ show (defName d) ++ " " ++
unwords (map show $ zipWith (<$) (reverse $ map (fst . unDom) ctx) vs)
return $ d `apply` vs
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 Datatype {} = Just AbstractDefn
makeAbs Function {} = Just AbstractDefn
makeAbs Constructor{} = Nothing
makeAbs d@Record{} = Just AbstractDefn
makeAbs Primitive{} = __IMPOSSIBLE__
makeAbs AbstractDefn = __IMPOSSIBLE__
inAbstractMode :: MonadReader TCEnv m => m a -> m a
inAbstractMode = local $ \e -> e { envAbstractMode = AbstractMode,
envAllowDestructiveUpdate = False }
inConcreteMode :: MonadReader TCEnv m => m a -> m a
inConcreteMode = local $ \e -> e { envAbstractMode = ConcreteMode }
ignoreAbstractMode :: MonadReader TCEnv m => m a -> m a
ignoreAbstractMode = local $ \e -> e { envAbstractMode = IgnoreAbstractMode,
envAllowDestructiveUpdate = False }
inConcreteOrAbstractMode :: (MonadReader TCEnv 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 :: MonadReader TCEnv m => QName -> m Bool
treatAbstractly q = asks $ treatAbstractly' q
treatAbstractly' :: QName -> TCEnv -> Bool
treatAbstractly' q env = case envAbstractMode env of
ConcreteMode -> True
IgnoreAbstractMode -> False
AbstractMode -> not $ current == m || current `isSubModuleOf` m
where
current = dropAnon $ envCurrentModule env
m = dropAnon $ qnameModule q
dropAnon (MName ms) = MName $ reverse $ dropWhile isNoName $ reverse ms
typeOfConst :: QName -> TCM Type
typeOfConst q = defType <$> (instantiateDef =<< getConstInfo q)
relOfConst :: QName -> TCM Relevance
relOfConst q = defRelevance <$> getConstInfo q
sortOfConst :: QName -> TCM Sort
sortOfConst q =
do d <- theDef <$> getConstInfo q
case d of
Datatype{dataSort = s} -> return s
_ -> fail $ "Expected " ++ show q ++ " to be a datatype."
droppedPars :: Definition -> Int
droppedPars d = case theDef d of
Axiom{} -> 0
def@Function{} -> projectionArgs def
Datatype {dataPars = _} -> 0
Record {recPars = _} -> 0
Constructor{conPars = n} -> n
Primitive{} -> 0
AbstractDefn -> __IMPOSSIBLE__
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 projProper isP
projectionArgs :: Defn -> Int
projectionArgs = maybe 0 (max 0 . pred . projIndex) . isProjection_
usesCopatterns :: QName -> TCM Bool
usesCopatterns q = do
d <- theDef <$> getConstInfo q
return $ case d of
Function{ funCopatternLHS = b } -> b
_ -> False
applyDef :: ProjOrigin -> QName -> Arg Term -> TCM 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 not (projProper isP) then fallback else do
return $ unArg a `applyE` [Proj o $ projOrig isP]