| Safe Haskell | Safe |
|---|---|
| Language | Haskell2010 |
FreeC.Backend.Coq.Syntax
Contents
Description
This module contains smart constructors for nodes of the Coq AST. For convenience the original Coq AST is exported as well.
Synopsis
- comment :: String -> Sentence
- commentedSentences :: String -> [Sentence] -> [Sentence]
- unpackComment :: Comment -> String
- blankProof :: Proof
- ident :: String -> Ident
- bare :: String -> Qualid
- qualified :: String -> String -> Qualid
- unpackQualid :: Qualid -> Maybe String
- access :: ModuleIdent -> Ident -> Ident
- app :: Term -> [Term] -> Term
- explicitApp :: Qualid -> [Term] -> Term
- arrows :: [Term] -> Term -> Term
- fun :: [Qualid] -> [Maybe Term] -> Term -> Term
- inferredFun :: [Qualid] -> Term -> Term
- typedBinder :: Generalizability -> Explicitness -> [Qualid] -> Term -> Binder
- typedBinder' :: Generalizability -> Explicitness -> Qualid -> Term -> Binder
- variable :: [Qualid] -> Term -> Sentence
- context :: Binder -> Sentence
- definitionSentence :: Qualid -> [Binder] -> Maybe Term -> Term -> Sentence
- notationSentence :: NonEmpty NotationToken -> Term -> [SyntaxModifier] -> Sentence
- nSymbol :: String -> NotationToken
- nIdent :: String -> NotationToken
- sModLevel :: Num -> SyntaxModifier
- sModIdentLevel :: NonEmpty String -> Maybe Num -> SyntaxModifier
- sortType :: Term
- string :: String -> Term
- equation :: Pattern -> Term -> Equation
- match :: Term -> [Equation] -> Term
- equals :: Term -> Term -> Term
- notEquals :: Term -> Term -> Term
- conj :: Term -> Term -> Term
- disj :: Term -> Term -> Term
- setOption :: Maybe Locality -> String -> Maybe (Either Num String) -> Sentence
- unsetOption :: Maybe Locality -> String -> Sentence
- requireImportFrom :: ModuleIdent -> [ModuleIdent] -> Sentence
- requireExportFrom :: ModuleIdent -> [ModuleIdent] -> Sentence
- requireFrom :: ModuleIdent -> [ModuleIdent] -> Sentence
- moduleImport :: [ModuleIdent] -> Sentence
- moduleExport :: [ModuleIdent] -> Sentence
Comments
commentedSentences :: String -> [Sentence] -> [Sentence] Source #
Puts a comment in front of the sentences if there is any sentence.
unpackComment :: Comment -> String Source #
Gets the string from theCoq comment.
Proofs
blankProof :: Proof Source #
An admitted proof that contains only a placeholder text.
Identifiers
unpackQualid :: Qualid -> Maybe String Source #
Gets the identifier for the given unqualified Coq identifier. Returns
Nothing if the given identifier is qualified.
access :: ModuleIdent -> Ident -> Ident Source #
Smart constructor for combining a module name and an identifier.
Functions
app :: Term -> [Term] -> Term Source #
Smart constructor for the application of a Coq function or (type) constructor.
If the first argument is an application term, the arguments are added to that term. Otherwise a new application term is created.
explicitApp :: Qualid -> [Term] -> Term Source #
Smart constructor for the explicit application of a Coq function or constructor to otherwise inferred type arguments.
If there are no type arguments, no ExplicitApp will be created.
Arguments
| :: [Term] | The types of the function arguments. |
| -> Term | The return type of the function. |
| -> Term |
Smart constructor for a Coq function type.
fun :: [Qualid] -> [Maybe Term] -> Term -> Term Source #
Smart constructor for the construction of a Coq lambda expression with the given arguments and right-hand side.
The second argument contains the types of the arguments are inferred by Coq.
inferredFun :: [Qualid] -> Term -> Term Source #
Like fun, but all argument types are inferred.
Binders
typedBinder :: Generalizability -> Explicitness -> [Qualid] -> Term -> Binder Source #
Smart constructor for an explicit or implicit typed Coq binder.
typedBinder' :: Generalizability -> Explicitness -> Qualid -> Term -> Binder Source #
Like typedBinder but for a single identifier.
Assumptions
Definition Sentences
Arguments
| :: Qualid | The name of the definition. |
| -> [Binder] | Binders for the parameters of the definition. |
| -> Maybe Term | The return type of the definition. |
| -> Term | The right-hand side of the definition. |
| -> Sentence |
Smart constructor for a Coq definition sentence.
Notation sentences
Arguments
| :: NonEmpty NotationToken | The notation to define. |
| -> Term | The right-hand side of the notation. |
| -> [SyntaxModifier] | The syntax modifiers of the notation. |
| -> Sentence |
Smart constructor for a Coq notation sentence.
nSymbol :: String -> NotationToken Source #
Smart constructor for a notation token that is a keyword of the notation.
nIdent :: String -> NotationToken Source #
Smart constructor for a notation token that is a variable in the notation.
sModIdentLevel :: NonEmpty String -> Maybe Num -> SyntaxModifier Source #
Smart constructor for a identifier parsing level syntax modifier.
Types
Expressions
equation :: Pattern -> Term -> Equation Source #
Smart constructor for Coq equations for match expressions.
Options
setOption :: Maybe Locality -> String -> Maybe (Either Num String) -> Sentence Source #
Smart constructor for a sentence which sets an option or flag.
unsetOption :: Maybe Locality -> String -> Sentence Source #
Smart constructor for a sentence which unsets an option or flag.
Imports
requireImportFrom :: ModuleIdent -> [ModuleIdent] -> Sentence Source #
Creates a From … Require Import … sentence.
requireExportFrom :: ModuleIdent -> [ModuleIdent] -> Sentence Source #
Creates a From … Require Export … sentence.
requireFrom :: ModuleIdent -> [ModuleIdent] -> Sentence Source #
Creates a From … Require … sentence.
moduleImport :: [ModuleIdent] -> Sentence Source #
Creates an Import … sentence.
moduleExport :: [ModuleIdent] -> Sentence Source #
Creates an Export … sentence.