| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
FreeC.Backend.Coq.Converter.Free
Description
This module contains auxiliary functions that help to generate Coq code
that uses the Free monad.
Synopsis
- genericArgDecls :: Explicitness -> [Binder]
- genericArgVariables :: [Sentence]
- genericApply :: Qualid -> [Term] -> [Term] -> [Term] -> Term
- genericApply' :: Term -> [Term] -> [Term] -> [Term] -> [Term] -> [Term] -> Term
- genericForFree :: Term -> Qualid -> Qualid -> Term
- generatePure :: Term -> Converter Term
- generateBinds :: [Term] -> String -> [Bool] -> [Maybe Term] -> ([Term] -> Converter Term) -> Converter Term
- generateBind :: Term -> String -> Maybe Term -> (Term -> Converter Term) -> Converter Term
Documentation
genericArgDecls :: Explicitness -> [Binder] Source #
The declarations of type parameters for the Free monad.
The first argument controls whether the generated binders are explicit
(e.g. (Shape : Type)) or implicit (e.g. {Shape : Type}).
genericArgVariables :: [Sentence] Source #
Variable sentences for the parameters of the Free monad.
Variable Shape : Type. and Variable Pos : Shape -> Type.
Arguments
| :: Qualid | The name of the function or (type) constructor |
| -> [Term] | The type class instances to pass to the callee. |
| -> [Term] | Implicit arguments to pass explicitly to the callee. |
| -> [Term] | The actual arguments of the callee. |
| -> Term |
Smart constructor for the application of a Coq function or (type)
constructor that requires the parameters for the Free monad.
Arguments
| :: Term | The function or (type) constructor term |
| -> [Term] | The explicit type class instances to pass to the callee. |
| -> [Term] | The implicit type class instances to pass to the callee. |
| -> [Term] | Implicit arguments to pass explicitly to the callee. |
| -> [Term] | The implicit type class arguments that are dependent on the implicit arguments. |
| -> [Term] | The actual arguments of the callee. |
| -> Term |
Like genericApply but takes a function or (type) constructor term instead
of a qualified identifier as its first argument.
genericForFree :: Term -> Qualid -> Qualid -> Term Source #
Smart constructor for a ForFree statement with a given type, property
and Free value.
generatePure :: Term -> Converter Term Source #
Wraps the given Coq term with the pure constructor of the Free monad.
Arguments
| :: [Term] | The values to bind or pass through. |
| -> String | A prefix to use for fresh variables by default. |
| -> [Bool] | If each value should be bound or passed through. |
| -> [Maybe Term] | The types of the values to bind. |
| -> ([Term] -> Converter Term) | Converter for the right-hand side of the generated function. The first argument are the fresh variables and passed through values. |
| -> Converter Term |
Generates a Coq expression that binds the given values to fresh variables
if the position in the given [Bool] list is True.
The fresh variables and the not bound values are passed to the given function in their original order. The fresh variables are not visible outside this function. If a value is a variable, the name of that variable is used as the prefix of the corresponding fresh variable. Otherwise, the given default prefix is used.
If some given type is Nothing, the type of the fresh variable is
inferred by Coq.
Arguments
| :: Term | The left-hand side of the bind operator. |
| -> String | A prefix to use for fresh variable by default. |
| -> Maybe Term | The Coq type of the value to bind or |
| -> (Term -> Converter Term) | Converter for the right-hand side of the generated function. The first argument is the fresh variable. |
| -> Converter Term |
Generates a Coq expressions that binds the given value to a fresh variable.
The generated fresh variable is passed to the given function. It is not visible outside of that function. If the given expression is a variable, the name of that variable is used as the prefix of the fresh variable. Otherwise the given default prefix is used.
If the given expression is an application of the pure constructor,
no bind will be generated. The wrapped value is passed directly to
the given function instead of a fresh variable.
If the third argument is Nothing, the type of the fresh variable is
inferred by Coq.