| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
FreeC.Backend.Agda.Converter.Free
Description
This module contains auxilary functions that help to generate Coq code
that uses the Free monad.
Synopsis
- generatePure :: Expr -> Expr
- bind :: Expr -> Expr -> Expr
- free :: Expr -> Expr
- applyFreeArgs :: QName -> Expr
- addFreeArgs :: [Name] -> [Name]
- freeArgBinder :: [LamBinding]
- undefinedExpr :: Expr
- errorExpr :: Expr
- addPartial :: Expr -> Expr
Documentation
generatePure :: Expr -> Expr Source #
Applies the pure constructor of the free monad to the given expression.
pure is always imported and therefore doesn't need to be qualified.
applyFreeArgs :: QName -> Expr Source #
Apply the Shape and Pos argument to the given type constructor.
c ↦ c Shape Pos
addFreeArgs :: [Name] -> [Name] Source #
Adds the reserved names for the free args Shape and Pos to a list of
names.
freeArgBinder :: [LamBinding] Source #
Binder for the type arguments of the Free monad.
(Shape : Set) (Pos : Shape → Set)
undefinedExpr :: Expr Source #
The identifier for the error term undefined.
addPartial :: Expr -> Expr Source #
Adds an instance argument for the partial type class to the given function type.
τ ↦ ⦃ Partial Shape Pos ⦄ → τ