idris- Functional Programming Language with Dependent Types

Safe HaskellNone




record :: SyntaxInfo -> IdrisParser PDecl Source

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

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, [(Name, Docstring)], Name, PTerm, FC, [Name]) Source

Parses a type constructor declaration Constructor ::= DocComment? FnName TypeSig;

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

Parses a constructor for simple discriminative union data types SimpleConstructor ::= FnName SimpleExpr* DocComment?

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;