Safe Haskell | None |
---|---|
Language | Haskell2010 |
Synopsis
- addConstant :: QName -> Definition -> TCM ()
- setTerminates :: QName -> Bool -> TCM ()
- modifyFunClauses :: QName -> ([Clause] -> [Clause]) -> TCM ()
- addClauses :: QName -> [Clause] -> TCM ()
- mkPragma :: String -> TCM CompilerPragma
- addPragma :: BackendName -> QName -> String -> TCM ()
- type HaskellCode = String
- type HaskellType = String
- type JSCode = String
- type CoreCode = String
- addDeprecatedPragma :: String -> BackendName -> QName -> String -> TCM ()
- dataFormat :: String -> [String] -> String
- addHaskellCode :: QName -> HaskellCode -> TCM ()
- addHaskellExport :: QName -> String -> TCM ()
- addHaskellType :: QName -> HaskellType -> TCM ()
- addHaskellData :: QName -> HaskellType -> [HaskellCode] -> TCM ()
- addJSCode :: QName -> JSCode -> TCM ()
- addCoreCode :: QName -> CoreCode -> TCM ()
- addCoreType :: QName -> CoreCode -> [CoreCode] -> TCM ()
- getUniqueCompilerPragma :: BackendName -> QName -> TCM (Maybe CompilerPragma)
- setFunctionFlag :: FunctionFlag -> Bool -> QName -> TCM ()
- markStatic :: QName -> TCM ()
- markInline :: Bool -> QName -> TCM ()
- markInjective :: QName -> TCM ()
- unionSignatures :: [Signature] -> Signature
- addSection :: ModuleName -> TCM ()
- setModuleCheckpoint :: ModuleName -> TCM ()
- getSection :: (Functor m, ReadTCState m) => ModuleName -> m (Maybe Section)
- lookupSection :: (Functor m, ReadTCState m) => ModuleName -> m Telescope
- addDisplayForms :: QName -> TCM ()
- applySection :: ModuleName -> Telescope -> ModuleName -> Args -> ScopeCopyInfo -> TCM ()
- applySection' :: ModuleName -> Telescope -> ModuleName -> Args -> ScopeCopyInfo -> TCM ()
- addDisplayForm :: QName -> DisplayForm -> TCM ()
- isLocal :: QName -> TCM Bool
- getDisplayForms :: QName -> TCM [LocalDisplayForm]
- chaseDisplayForms :: QName -> TCM (Set QName)
- hasLoopingDisplayForm :: QName -> TCM Bool
- canonicalName :: QName -> TCM QName
- sameDef :: QName -> QName -> TCM (Maybe QName)
- whatInduction :: MonadTCM tcm => QName -> tcm Induction
- singleConstructorType :: QName -> TCM Bool
- data SigError
- sigError :: (String -> a) -> a -> SigError -> a
- class (Functor m, Applicative m, Monad m, HasOptions m, MonadDebug m, MonadReader TCEnv m) => HasConstInfo m where
- defaultGetRewriteRulesFor :: Monad m => m TCState -> QName -> m RewriteRules
- getOriginalProjection :: HasConstInfo m => QName -> m QName
- defaultGetConstInfo :: (HasOptions m, MonadDebug m, MonadReader TCEnv m) => TCState -> TCEnv -> QName -> m (Either SigError Definition)
- getConInfo :: MonadTCM tcm => ConHead -> tcm Definition
- getPolarity :: QName -> TCM [Polarity]
- getPolarity' :: Comparison -> QName -> TCM [Polarity]
- setPolarity :: QName -> [Polarity] -> TCM ()
- getForcedArgs :: QName -> TCM [IsForced]
- getArgOccurrence :: QName -> Nat -> TCM Occurrence
- setArgOccurrences :: QName -> [Occurrence] -> TCM ()
- modifyArgOccurrences :: QName -> ([Occurrence] -> [Occurrence]) -> TCM ()
- setTreeless :: QName -> TTerm -> TCM ()
- setCompiledArgUse :: QName -> [Bool] -> TCM ()
- getCompiled :: QName -> TCM (Maybe Compiled)
- getErasedConArgs :: QName -> TCM [Bool]
- setErasedConArgs :: QName -> [Bool] -> TCM ()
- getTreeless :: QName -> TCM (Maybe TTerm)
- getCompiledArgUse :: QName -> TCM [Bool]
- getMutual :: QName -> TCM (Maybe [QName])
- getMutual_ :: Defn -> Maybe [QName]
- setMutual :: QName -> [QName] -> TCM ()
- mutuallyRecursive :: QName -> QName -> TCM Bool
- definitelyNonRecursive_ :: Defn -> Bool
- getCurrentModuleFreeVars :: TCM Nat
- getDefModule :: HasConstInfo m => QName -> m ModuleName
- getDefFreeVars :: (Functor m, Applicative m, ReadTCState m, MonadReader TCEnv m) => QName -> m Nat
- freeVarsToApply :: (Functor m, HasConstInfo m, HasOptions m, ReadTCState m, MonadReader TCEnv m, MonadDebug m) => QName -> m Args
- getModuleFreeVars :: (Functor m, Applicative m, MonadReader TCEnv m, ReadTCState m) => ModuleName -> m Nat
- moduleParamsToApply :: (Functor m, Applicative m, HasOptions m, MonadReader TCEnv m, ReadTCState m, MonadDebug m) => ModuleName -> m Args
- inFreshModuleIfFreeParams :: TCM a -> TCM a
- instantiateDef :: Definition -> TCM Definition
- instantiateRewriteRule :: (Functor m, HasConstInfo m, HasOptions m, ReadTCState m, MonadReader TCEnv m, MonadDebug m) => RewriteRule -> m RewriteRule
- instantiateRewriteRules :: (Functor m, HasConstInfo m, HasOptions m, ReadTCState m, MonadReader TCEnv m, MonadDebug m) => RewriteRules -> m RewriteRules
- makeAbstract :: Definition -> Maybe Definition
- inAbstractMode :: MonadReader TCEnv m => m a -> m a
- inConcreteMode :: MonadReader TCEnv m => m a -> m a
- ignoreAbstractMode :: MonadReader TCEnv m => m a -> m a
- inConcreteOrAbstractMode :: (MonadReader TCEnv m, HasConstInfo m) => QName -> (Definition -> m a) -> m a
- treatAbstractly :: MonadReader TCEnv m => QName -> m Bool
- treatAbstractly' :: QName -> TCEnv -> Bool
- typeOfConst :: QName -> TCM Type
- relOfConst :: QName -> TCM Relevance
- droppedPars :: Definition -> Int
- isProjection :: HasConstInfo m => QName -> m (Maybe Projection)
- isProjection_ :: Defn -> Maybe Projection
- isStaticFun :: Defn -> Bool
- isInlineFun :: Defn -> Bool
- isProperProjection :: Defn -> Bool
- projectionArgs :: Defn -> Int
- usesCopatterns :: QName -> TCM Bool
- applyDef :: ProjOrigin -> QName -> Arg Term -> TCM Term
Documentation
addConstant :: QName -> Definition -> TCM () Source #
Add a constant to the signature. Lifts the definition to top level.
modifyFunClauses :: QName -> ([Clause] -> [Clause]) -> TCM () Source #
Modify the clauses of a function.
addClauses :: QName -> [Clause] -> TCM () Source #
Lifts clauses to the top-level and adds them to definition.
Also adjusts the funCopatternLHS
field if necessary.
Temporary **
type HaskellCode = String Source #
type HaskellType = String Source #
addDeprecatedPragma :: String -> BackendName -> QName -> String -> TCM () Source #
addHaskellCode :: QName -> HaskellCode -> TCM () Source #
addHaskellType :: QName -> HaskellType -> TCM () Source #
addHaskellData :: QName -> HaskellType -> [HaskellCode] -> TCM () Source #
End of temporary functions **
getUniqueCompilerPragma :: BackendName -> QName -> TCM (Maybe CompilerPragma) Source #
setFunctionFlag :: FunctionFlag -> Bool -> QName -> TCM () Source #
markStatic :: QName -> TCM () Source #
markInjective :: QName -> TCM () Source #
unionSignatures :: [Signature] -> Signature Source #
addSection :: ModuleName -> TCM () Source #
Add a section to the signature.
The current context will be stored as the cumulative module parameters for this section.
setModuleCheckpoint :: ModuleName -> TCM () Source #
Sets the checkpoint for the given module to the current checkpoint.
getSection :: (Functor m, ReadTCState m) => ModuleName -> m (Maybe Section) Source #
Get a section.
Why Maybe? The reason is that we look up all prefixes of a module to compute number of parameters, and for hierarchical top-level modules, A.B.C say, A and A.B do not exist.
lookupSection :: (Functor m, ReadTCState m) => ModuleName -> m Telescope Source #
Lookup a section telescope.
If it doesn't exist, like in hierarchical top-level modules, the section telescope is empty.
addDisplayForms :: QName -> TCM () Source #
:: ModuleName | Name of new module defined by the module macro. |
-> Telescope | Parameters of new module. |
-> ModuleName | Name of old module applied to arguments. |
-> Args | Arguments of module application. |
-> ScopeCopyInfo | Imported names and modules |
-> TCM () |
Module application (followed by module parameter abstraction).
applySection' :: ModuleName -> Telescope -> ModuleName -> Args -> ScopeCopyInfo -> TCM () Source #
addDisplayForm :: QName -> DisplayForm -> TCM () Source #
Add a display form to a definition (could be in this or imported signature).
getDisplayForms :: QName -> TCM [LocalDisplayForm] Source #
chaseDisplayForms :: QName -> TCM (Set QName) Source #
Find all names used (recursively) by display forms of a given name.
whatInduction :: MonadTCM tcm => QName -> tcm Induction Source #
Can be called on either a (co)datatype, a record type or a (co)constructor.
singleConstructorType :: QName -> TCM Bool Source #
Does the given constructor come from a single-constructor type?
Precondition: The name has to refer to a constructor.
Signature lookup errors.
SigUnknown String | The name is not in the signature; default error message. |
SigAbstract | The name is not available, since it is abstract. |
class (Functor m, Applicative m, Monad m, HasOptions m, MonadDebug m, MonadReader TCEnv m) => HasConstInfo m where Source #
getConstInfo :: QName -> m Definition Source #
Lookup the definition of a name. The result is a closed thing, all free variables have been abstracted over.
getConstInfo' :: QName -> m (Either SigError Definition) Source #
Version that reports exceptions:
getRewriteRulesFor :: QName -> m RewriteRules Source #
Lookup the rewrite rules with the given head symbol.
Instances
defaultGetRewriteRulesFor :: Monad m => m TCState -> QName -> m RewriteRules Source #
getOriginalProjection :: HasConstInfo m => QName -> m QName Source #
Get the original name of the projection (the current one could be from a module application).
defaultGetConstInfo :: (HasOptions m, MonadDebug m, MonadReader TCEnv m) => TCState -> TCEnv -> QName -> m (Either SigError Definition) Source #
getConInfo :: MonadTCM tcm => ConHead -> tcm Definition Source #
getPolarity' :: Comparison -> QName -> TCM [Polarity] Source #
Look up polarity of a definition and compose with polarity
represented by Comparison
.
getArgOccurrence :: QName -> Nat -> TCM Occurrence Source #
Get argument occurrence info for argument i
of definition d
(never fails).
setArgOccurrences :: QName -> [Occurrence] -> TCM () Source #
Sets the defArgOccurrences
for the given identifier (which
should already exist in the signature).
modifyArgOccurrences :: QName -> ([Occurrence] -> [Occurrence]) -> TCM () Source #
getMutual :: QName -> TCM (Maybe [QName]) Source #
Get the mutually recursive identifiers of a symbol from the signature.
getMutual_ :: Defn -> Maybe [QName] Source #
Get the mutually recursive identifiers from a Definition
.
mutuallyRecursive :: QName -> QName -> TCM Bool Source #
Check whether two definitions are mutually recursive.
definitelyNonRecursive_ :: Defn -> Bool Source #
A functiondatarecord definition is nonRecursive if it is not even mutually recursive with itself.
getCurrentModuleFreeVars :: TCM Nat Source #
Get the number of parameters to the current module.
getDefModule :: HasConstInfo m => QName -> m ModuleName Source #
getDefFreeVars :: (Functor m, Applicative m, ReadTCState m, MonadReader TCEnv m) => QName -> m Nat Source #
Compute the number of free variables of a defined name. This is the sum of number of parameters shared with the current module and the number of anonymous variables (if the name comes from a let-bound module).
freeVarsToApply :: (Functor m, HasConstInfo m, HasOptions m, ReadTCState m, MonadReader TCEnv m, MonadDebug m) => QName -> m Args Source #
getModuleFreeVars :: (Functor m, Applicative m, MonadReader TCEnv m, ReadTCState m) => ModuleName -> m Nat Source #
moduleParamsToApply :: (Functor m, Applicative m, HasOptions m, MonadReader TCEnv m, ReadTCState m, MonadDebug m) => ModuleName -> m Args Source #
Compute the context variables to apply a definition to.
We have to insert the module telescope of the common prefix of the current module and the module where the definition comes from. (Properly raised to the current context.)
Example:
module M₁ Γ where
module M₁ Δ where
f = ...
module M₃ Θ where
... M₁.M₂.f [insert Γ raised by Θ]
inFreshModuleIfFreeParams :: TCM a -> TCM a Source #
Unless all variables in the context are module parameters, create a fresh module to capture the non-module parameters. Used when unquoting to make sure generated definitions work properly.
instantiateDef :: Definition -> TCM Definition Source #
Instantiate a closed definition with the correct part of the current context.
instantiateRewriteRule :: (Functor m, HasConstInfo m, HasOptions m, ReadTCState m, MonadReader TCEnv m, MonadDebug m) => RewriteRule -> m RewriteRule Source #
instantiateRewriteRules :: (Functor m, HasConstInfo m, HasOptions m, ReadTCState m, MonadReader TCEnv m, MonadDebug m) => RewriteRules -> m RewriteRules Source #
makeAbstract :: Definition -> Maybe Definition Source #
Give the abstract view of a definition.
inAbstractMode :: MonadReader TCEnv m => m a -> m a Source #
Enter abstract mode. Abstract definition in the current module are transparent.
inConcreteMode :: MonadReader TCEnv m => m a -> m a Source #
Not in abstract mode. All abstract definitions are opaque.
ignoreAbstractMode :: MonadReader TCEnv m => m a -> m a Source #
Ignore abstract mode. All abstract definitions are transparent.
inConcreteOrAbstractMode :: (MonadReader TCEnv m, HasConstInfo m) => QName -> (Definition -> m a) -> m a Source #
Enter concrete or abstract mode depending on whether the given identifier is concrete or abstract.
treatAbstractly :: MonadReader TCEnv m => QName -> m Bool Source #
Check whether a name might have to be treated abstractly (either if we're
inAbstractMode
or it's not a local name). Returns true for things not
declared abstract as well, but for those makeAbstract
will have no effect.
treatAbstractly' :: QName -> TCEnv -> Bool Source #
Andreas, 2015-07-01:
If the current
module is a weak suffix of the identifier module,
we can see through its abstract definition if we are abstract.
(Then treatAbstractly'
returns False
).
If I am not mistaken, then we cannot see definitions in the where
block of an abstract function from the perspective of the function,
because then the current module is a strict prefix of the module
of the local identifier.
This problem is fixed by removing trailing anonymous module name parts
(underscores) from both names.
typeOfConst :: QName -> TCM Type Source #
Get type of a constant, instantiated to the current context.
droppedPars :: Definition -> Int Source #
The number of dropped parameters for a definition. 0 except for projection(-like) functions and constructors.
isProjection :: HasConstInfo m => QName -> m (Maybe Projection) Source #
Is it the name of a record projection?
isProjection_ :: Defn -> Maybe Projection Source #
isStaticFun :: Defn -> Bool Source #
Is it a function marked STATIC?
isInlineFun :: Defn -> Bool Source #
Is it a function marked INLINE?
isProperProjection :: Defn -> Bool Source #
Returns True
if we are dealing with a proper projection,
i.e., not a projection-like function nor a record field value
(projection applied to argument).
projectionArgs :: Defn -> Int Source #
Number of dropped initial arguments of a projection(-like) function.