Safe Haskell	None

Idris.ParseData

Synopsis

Documentation

record :: SyntaxInfo -> IdrisParser PDecl Source

Parses a record type declaration

Record ::=
    DocComment Accessibility? record FnName TypeSig 'where' OpenBlock Constructor KeepTerminator CloseBlock;

dataI :: IdrisParser Bool Source

Parses data declaration type (normal or codata)

DataI ::= 'data' | codata;

data_ :: SyntaxInfo -> IdrisParser PDecl Source

Parses a data type declaration

Data ::= DocComment? Accessibility? DataI FnName TypeSig ExplicitTypeDataRest?
       | DocComment? Accessibility? DataI FnName Name*   DataRest?
       ;

Constructor' ::= Constructor KeepTerminator;

ExplicitTypeDataRest ::= 'where' OpenBlock Constructor'* CloseBlock;

DataRest ::= '=' SimpleConstructorList Terminator
           | 'where'!
           ;

SimpleConstructorList ::=
    SimpleConstructor
  | SimpleConstructor '|' SimpleConstructorList
  ;

constructor :: SyntaxInfo -> IdrisParser (String, Name, PTerm, FC)Source

Parses a type constructor declaration

  Constructor ::= DocComment? FnName TypeSig;

simpleConstructor :: SyntaxInfo -> IdrisParser (String, Name, [PTerm], FC)Source

Parses a constructor for simple discriminative 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;