| Copyright | License : BSD3 |
|---|---|
| Maintainer | The Idris Community. |
| Safe Haskell | None |
| Language | Haskell2010 |
Idris.Parser.Data
Description
- record :: SyntaxInfo -> IdrisParser PDecl
- recordParameter :: SyntaxInfo -> IdrisParser (Name, FC, Plicity, PTerm)
- dataI :: IdrisParser DataOpts
- recordI :: IdrisParser DataOpts
- dataOpts :: DataOpts -> IdrisParser DataOpts
- data_ :: SyntaxInfo -> IdrisParser PDecl
- constructor :: SyntaxInfo -> IdrisParser (Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC, [Name])
- simpleConstructor :: SyntaxInfo -> IdrisParser (Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, FC, [PTerm], FC, [Name])
- dsl :: SyntaxInfo -> IdrisParser PDecl
- checkDSL :: DSL -> IdrisParser ()
- overload :: SyntaxInfo -> IdrisParser (String, PTerm)
Documentation
record :: SyntaxInfo -> IdrisParser PDecl Source #
Parses a record type declaration
Record ::=
DocComment Accessibility? record FnName TypeSig 'where' OpenBlock Constructor KeepTerminator CloseBlock;
recordParameter :: SyntaxInfo -> IdrisParser (Name, FC, Plicity, PTerm) Source #
dataI :: IdrisParser DataOpts Source #
Parses data declaration type (normal or codata)
DataI ::= 'data' | codata;
dataOpts :: DataOpts -> IdrisParser DataOpts Source #
Parses if a data should not have a default eliminator
DefaultEliminator ::= noelim?
data_ :: SyntaxInfo -> IdrisParser PDecl Source #
Parses a data type declaration Data ::= DocComment? Accessibility? DataI DefaultEliminator FnName TypeSig ExplicitTypeDataRest? | DocComment? Accessibility? DataI DefaultEliminator FnName Name* DataRest? ; Constructor' ::= Constructor KeepTerminator; ExplicitTypeDataRest ::= 'where' OpenBlock Constructor'* CloseBlock;
DataRest ::= '=' SimpleConstructorList Terminator | 'where'! ; SimpleConstructorList ::= SimpleConstructor | SimpleConstructor '|' SimpleConstructorList ;
constructor :: SyntaxInfo -> IdrisParser (Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, FC, PTerm, FC, [Name]) Source #
Parses a type constructor declaration Constructor ::= DocComment? FnName TypeSig;
simpleConstructor :: SyntaxInfo -> IdrisParser (Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, FC, [PTerm], FC, [Name]) Source #
Parses a constructor for simple discriminated union data types SimpleConstructor ::= FnName SimpleExpr* DocComment?
dsl :: SyntaxInfo -> IdrisParser PDecl Source #
Parses a dsl block declaration
DSL ::= dsl FnName OpenBlock Overload'+ CloseBlock;
checkDSL :: DSL -> IdrisParser () Source #
Checks DSL for errors
overload :: SyntaxInfo -> IdrisParser (String, PTerm) Source #
Parses a DSL overload declaration OverloadIdentifier ::= 'let' | Identifier; Overload ::= OverloadIdentifier '=' Expr;