Safe Haskell | None |
---|---|
Language | Haskell98 |
- addConstant :: QName -> Definition -> TCM ()
- setTerminates :: QName -> Bool -> TCM ()
- modifyFunClauses :: QName -> ([Clause] -> [Clause]) -> TCM ()
- addClauses :: QName -> [Clause] -> TCM ()
- addHaskellCode :: QName -> HaskellType -> HaskellCode -> TCM ()
- addHaskellExport :: QName -> HaskellType -> String -> TCM ()
- addHaskellType :: QName -> HaskellType -> TCM ()
- addEpicCode :: QName -> EpicCode -> TCM ()
- addJSCode :: QName -> String -> TCM ()
- markStatic :: QName -> TCM ()
- unionSignatures :: [Signature] -> Signature
- addSection :: ModuleName -> Nat -> TCM ()
- lookupSection :: ModuleName -> TCM Telescope
- addDisplayForms :: QName -> TCM ()
- applySection :: ModuleName -> Telescope -> ModuleName -> Args -> Ren QName -> Ren ModuleName -> TCM ()
- addDisplayForm :: QName -> DisplayForm -> TCM ()
- canonicalName :: QName -> TCM QName
- sameDef :: QName -> QName -> TCM (Maybe QName)
- whatInduction :: QName -> TCM Induction
- singleConstructorType :: QName -> TCM Bool
- class (Functor m, Applicative m, Monad m) => HasConstInfo m where
- getConstInfo :: QName -> m Definition
- getConInfo :: MonadTCM tcm => ConHead -> tcm Definition
- getPolarity :: QName -> TCM [Polarity]
- getPolarity' :: Comparison -> QName -> TCM [Polarity]
- setPolarity :: QName -> [Polarity] -> TCM ()
- getArgOccurrences :: QName -> TCM [Occurrence]
- getArgOccurrence :: QName -> Nat -> TCM Occurrence
- setArgOccurrences :: QName -> [Occurrence] -> TCM ()
- getMutual :: QName -> TCM [QName]
- setMutual :: QName -> [QName] -> TCM ()
- mutuallyRecursive :: QName -> QName -> TCM Bool
- getSection :: ModuleName -> TCM (Maybe Section)
- getSecFreeVars :: ModuleName -> TCM Nat
- getModuleFreeVars :: ModuleName -> TCM Nat
- getDefFreeVars :: QName -> TCM Nat
- freeVarsToApply :: QName -> TCM Args
- instantiateDef :: Definition -> TCM Definition
- makeAbstract :: Definition -> Maybe Definition
- inAbstractMode :: TCM a -> TCM a
- inConcreteMode :: TCM a -> TCM a
- ignoreAbstractMode :: MonadReader TCEnv m => m a -> m a
- treatAbstractly :: MonadReader TCEnv m => QName -> m Bool
- treatAbstractly' :: QName -> TCEnv -> Bool
- typeOfConst :: QName -> TCM Type
- relOfConst :: QName -> TCM Relevance
- colOfConst :: QName -> TCM [Color]
- sortOfConst :: QName -> TCM Sort
- isProjection :: QName -> TCM (Maybe Projection)
- isProjection_ :: Defn -> Maybe Projection
- isProperProjection :: Defn -> Bool
- projectionArgs :: Defn -> Int
- applyDef :: QName -> Arg Term -> TCM Term
- getDefType :: QName -> Type -> TCM (Maybe Type)
Documentation
addConstant :: QName -> Definition -> TCM () Source
Add a constant to the signature. Lifts the definition to top level.
setTerminates :: QName -> Bool -> TCM () Source
Set termination info of a defined function symbol.
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.
addHaskellCode :: QName -> HaskellType -> HaskellCode -> TCM () Source
addHaskellExport :: QName -> HaskellType -> String -> TCM () Source
addHaskellType :: QName -> HaskellType -> TCM () Source
addEpicCode :: QName -> EpicCode -> TCM () Source
markStatic :: QName -> TCM () Source
unionSignatures :: [Signature] -> Signature Source
addSection :: ModuleName -> Nat -> TCM () Source
Add a section to the signature.
lookupSection :: ModuleName -> TCM Telescope Source
Lookup a section. If it doesn't exist that just means that the module wasn't parameterised.
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. |
-> Ren QName | Imported names (given as renaming). |
-> Ren ModuleName | Imported modules (given as renaming). |
-> TCM () |
Module application (followed by module parameter abstraction).
addDisplayForm :: QName -> DisplayForm -> TCM () Source
canonicalName :: QName -> TCM QName Source
whatInduction :: 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.
class (Functor m, Applicative m, Monad 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.
HasConstInfo ReduceM | |
HasConstInfo Unify | |
HasConstInfo (TCMT IO) | |
(HasConstInfo m, Error err) => HasConstInfo (ExceptionT err m) |
getConInfo :: MonadTCM tcm => ConHead -> tcm Definition Source
getPolarity :: QName -> TCM [Polarity] Source
Look up the polarity of a definition.
getPolarity' :: Comparison -> QName -> TCM [Polarity] Source
Look up polarity of a definition and compose with polarity
represented by Comparison
.
setPolarity :: QName -> [Polarity] -> TCM () Source
Set the polarity of a definition.
getArgOccurrences :: QName -> TCM [Occurrence] Source
Return a finite list of argument occurrences.
getArgOccurrence :: QName -> Nat -> TCM Occurrence Source
setArgOccurrences :: QName -> [Occurrence] -> TCM () Source
mutuallyRecursive :: QName -> QName -> TCM Bool Source
Check whether two definitions are mutually recursive.
getSection :: ModuleName -> TCM (Maybe Section) Source
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.
getSecFreeVars :: ModuleName -> TCM Nat Source
Look up the number of free variables of a section. This is equal to the number of parameters if we're currently inside the section and 0 otherwise.
getModuleFreeVars :: ModuleName -> TCM Nat Source
Compute the number of free variables of a module. This is the sum of the free variables of its sections.
getDefFreeVars :: QName -> TCM Nat Source
Compute the number of free variables of a defined name. This is the sum of the free variables of the sections it's contained in.
freeVarsToApply :: QName -> TCM Args Source
Compute the context variables to apply a definition to.
instantiateDef :: Definition -> TCM Definition Source
Instantiate a closed definition with the correct part of the current context.
makeAbstract :: Definition -> Maybe Definition Source
Give the abstract view of a definition.
inAbstractMode :: TCM a -> TCM a Source
Enter abstract mode. Abstract definition in the current module are transparent.
inConcreteMode :: TCM a -> TCM 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.
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
typeOfConst :: QName -> TCM Type Source
Get type of a constant, instantiated to the current context.
relOfConst :: QName -> TCM Relevance Source
Get relevance of a constant.
colOfConst :: QName -> TCM [Color] Source
Get colors of a constant.
sortOfConst :: QName -> TCM Sort Source
The name must be a datatype.
isProjection :: QName -> TCM (Maybe Projection) Source
Is it the name of a record projection?
isProjection_ :: Defn -> Maybe Projection Source
isProperProjection :: Defn -> Bool Source
projectionArgs :: Defn -> Int Source
Number of dropped initial arguments.
applyDef :: QName -> Arg Term -> TCM Term Source
Apply a function f
to its first argument, producing the proper
postfix projection if f
is a projection.
getDefType :: QName -> Type -> TCM (Maybe Type) Source
getDefType f t
computes the type of (possibly projection-(like))
function t
whose first argument has type t
.
The parameters
for f
are extracted from t
.
Nothing
if f
is projection(like) but
t
is not a datarecordaxiom type.
Precondition: t
is reduced.
See also: getConType