Safe Haskell | None |
---|---|
Language | Haskell98 |
- instantiate :: Instantiate a => a -> TCM a
- instantiateFull :: InstantiateFull a => a -> TCM a
- reduce :: Reduce a => a -> TCM a
- reduceB :: Reduce a => a -> TCM (Blocked a)
- normalise :: Normalise a => a -> TCM a
- simplify :: Simplify a => a -> TCM a
- class Instantiate t where
- instantiate' :: t -> ReduceM t
- ifBlocked :: MonadTCM tcm => Term -> (MetaId -> Term -> tcm a) -> (Term -> tcm a) -> tcm a
- ifBlockedType :: MonadTCM tcm => Type -> (MetaId -> Type -> tcm a) -> (Type -> tcm a) -> tcm a
- class Reduce t where
- unfoldDefinition :: Bool -> (Term -> ReduceM (Blocked Term)) -> Term -> QName -> Args -> ReduceM (Blocked Term)
- unfoldDefinitionE :: Bool -> (Term -> ReduceM (Blocked Term)) -> Term -> QName -> Elims -> ReduceM (Blocked Term)
- unfoldDefinition' :: Bool -> (Term -> ReduceM (Simplification, Blocked Term)) -> Term -> QName -> Elims -> ReduceM (Simplification, Blocked Term)
- reduceDefCopy :: QName -> Args -> TCM (Reduced () Term)
- reduceHead :: Term -> TCM (Blocked Term)
- reduceHead' :: Term -> ReduceM (Blocked Term)
- appDef_ :: QName -> Term -> [Clause] -> Maybe CompiledClauses -> MaybeReducedArgs -> ReduceM (Reduced (Blocked Term) Term)
- appDefE_ :: QName -> Term -> [Clause] -> Maybe CompiledClauses -> MaybeReducedElims -> ReduceM (Reduced (Blocked Term) Term)
- appDef :: Term -> CompiledClauses -> MaybeReducedArgs -> ReduceM (Reduced (Blocked Term) Term)
- appDefE :: Term -> CompiledClauses -> MaybeReducedElims -> ReduceM (Reduced (Blocked Term) Term)
- appDef' :: Term -> [Clause] -> MaybeReducedArgs -> ReduceM (Reduced (Blocked Term) Term)
- appDefE' :: Term -> [Clause] -> MaybeReducedElims -> ReduceM (Reduced (Blocked Term) Term)
- class Simplify t where
- simplifyBlocked' :: Simplify t => Blocked t -> ReduceM t
- class Normalise t where
- normalise' :: t -> ReduceM t
- class InstantiateFull t where
- instantiateFull' :: t -> ReduceM t
Documentation
instantiate :: Instantiate a => a -> TCM a Source
instantiateFull :: InstantiateFull a => a -> TCM a Source
class Instantiate t where Source
Instantiate something. Results in an open meta variable or a non meta. Doesn't do any reduction, and preserves blocking tags (when blocking meta is uninstantiated).
instantiate' :: t -> ReduceM t Source
Instantiate LevelAtom | |
Instantiate PlusLevel | |
Instantiate Level | |
Instantiate Sort | |
Instantiate Telescope | |
Instantiate Type | |
Instantiate Elim | |
Instantiate Term | |
Instantiate Constraint | |
Instantiate t => Instantiate [t] | |
Instantiate a => Instantiate (Blocked a) | |
Instantiate t => Instantiate (Abs t) | |
Instantiate t => Instantiate (Dom t) | |
Instantiate t => Instantiate (Arg t) | |
Instantiate a => Instantiate (Closure a) | |
(Instantiate a, Instantiate b) => Instantiate (a, b) | |
(Ord k, Instantiate e) => Instantiate (Map k e) | |
(Instantiate a, Instantiate b, Instantiate c) => Instantiate (a, b, c) |
Reduction to weak head normal form.
ifBlockedType :: MonadTCM tcm => Type -> (MetaId -> Type -> tcm a) -> (Type -> tcm a) -> tcm a Source
Nothing
Reduce LevelAtom | |
Reduce PlusLevel | |
Reduce Level | |
Reduce Sort | |
Reduce Telescope | |
Reduce Type | |
Reduce Elim | |
Reduce Term | |
Reduce Constraint | |
Reduce t => Reduce [t] | |
(Subst t, Reduce t) => Reduce (Abs t) | |
Reduce t => Reduce (Dom t) | |
Reduce t => Reduce (Arg t) | |
Reduce a => Reduce (Closure a) | |
(Reduce a, Reduce b) => Reduce (a, b) | |
(Ord k, Reduce e) => Reduce (Map k e) | |
(Reduce a, Reduce b, Reduce c) => Reduce (a, b, c) |
unfoldDefinition :: Bool -> (Term -> ReduceM (Blocked Term)) -> Term -> QName -> Args -> ReduceM (Blocked Term) Source
If the first argument is True
, then a single delayed clause may
be unfolded.
unfoldDefinitionE :: Bool -> (Term -> ReduceM (Blocked Term)) -> Term -> QName -> Elims -> ReduceM (Blocked Term) Source
unfoldDefinition' :: Bool -> (Term -> ReduceM (Simplification, Blocked Term)) -> Term -> QName -> Elims -> ReduceM (Simplification, Blocked Term) Source
reduceDefCopy :: QName -> Args -> TCM (Reduced () Term) Source
Reduce a non-primitive definition if it is a copy linking to another def.
appDef_ :: QName -> Term -> [Clause] -> Maybe CompiledClauses -> MaybeReducedArgs -> ReduceM (Reduced (Blocked Term) Term) Source
Apply a definition using the compiled clauses, or fall back to ordinary clauses if no compiled clauses exist.
appDefE_ :: QName -> Term -> [Clause] -> Maybe CompiledClauses -> MaybeReducedElims -> ReduceM (Reduced (Blocked Term) Term) Source
appDef :: Term -> CompiledClauses -> MaybeReducedArgs -> ReduceM (Reduced (Blocked Term) Term) Source
Apply a defined function to it's arguments, using the compiled clauses. The original term is the first argument applied to the third.
appDefE :: Term -> CompiledClauses -> MaybeReducedElims -> ReduceM (Reduced (Blocked Term) Term) Source
appDef' :: Term -> [Clause] -> MaybeReducedArgs -> ReduceM (Reduced (Blocked Term) Term) Source
Apply a defined function to it's arguments, using the original clauses.
Simplification
Only unfold definitions if this leads to simplification which means that a constructor/literal pattern is matched.
Simplify Bool | |
Simplify Pattern | |
Simplify ClauseBody | |
Simplify LevelAtom | |
Simplify PlusLevel | |
Simplify Level | |
Simplify Sort | |
Simplify Type | |
Simplify Elim | |
Simplify Term | |
Simplify DisplayForm | |
Simplify Constraint | |
Simplify ProblemConstraint | |
Simplify t => Simplify [t] | |
Simplify a => Simplify (Maybe a) | |
(Subst a, Simplify a) => Simplify (Tele a) | |
(Subst t, Simplify t) => Simplify (Abs t) | |
Simplify t => Simplify (Dom t) | |
Simplify t => Simplify (Arg t) | |
Simplify a => Simplify (Closure a) | |
(Simplify a, Simplify b) => Simplify (a, b) | |
(Ord k, Simplify e) => Simplify (Map k e) | |
Simplify t => Simplify (Named name t) | |
(Simplify a, Simplify b, Simplify c) => Simplify (a, b, c) |
simplifyBlocked' :: Simplify t => Blocked t -> ReduceM t Source
Normalisation
class Normalise t where Source
normalise' :: t -> ReduceM t Source
Normalise Bool | |
Normalise Pattern | |
Normalise ClauseBody | |
Normalise LevelAtom | |
Normalise PlusLevel | |
Normalise Level | |
Normalise Sort | |
Normalise Type | |
Normalise Elim | |
Normalise Term | |
Normalise DisplayForm | |
Normalise Constraint | |
Normalise ProblemConstraint | |
Normalise t => Normalise [t] | |
Normalise a => Normalise (Maybe a) | |
(Subst a, Normalise a) => Normalise (Tele a) | |
(Subst t, Normalise t) => Normalise (Abs t) | |
Normalise t => Normalise (Dom t) | |
Normalise t => Normalise (Arg t) | |
Normalise a => Normalise (Closure a) | |
(Normalise a, Normalise b) => Normalise (a, b) | |
(Ord k, Normalise e) => Normalise (Map k e) | |
Normalise t => Normalise (Named name t) | |
(Normalise a, Normalise b, Normalise c) => Normalise (a, b, c) |
Full instantiation
class InstantiateFull t where Source
instantiateFull'
instantiate
s metas everywhere (and recursively)
but does not reduce
.
instantiateFull' :: t -> ReduceM t Source