idris-1.3.2: Functional Programming Language with Dependent Types

LicenseBSD3
MaintainerThe Idris Community.
Safe HaskellNone
LanguageHaskell2010

Idris.Parser.Ops

Description

 
Synopsis

Documentation

table :: [FixDecl] -> [[Operator IdrisParser PTerm]] Source #

Creates table for fixity declarations to build expression parser using pre-build and user-defined operator/fixity declarations

backtickOperator :: (Parsing m, MonadState IState m) => m Name Source #

Parses a function used as an operator -- enclosed in backticks

  BacktickOperator ::=
    '`' Name '`'
    ;

operatorName :: (Parsing m, MonadState IState m) => m Name Source #

Parses an operator name (either a symbolic name or a backtick-quoted name)

  OperatorName ::=
      SymbolicOperator
    | BacktickOperator
    ;

operatorFront :: Parsing m => m Name Source #

Parses an operator in function position i.e. enclosed by `()', with an optional namespace

  OperatorFront ::=
    '(' '=' ')'
    | (Identifier_t .)? '(' Operator_t ')'
    ;

fnName :: (Parsing m, MonadState IState m) => m Name Source #

Parses a function (either normal name or operator)

  FnName ::= Name | OperatorFront;

fixity :: IdrisParser PDecl Source #

Parses a fixity declaration Fixity ::= FixityType Natural_t OperatorList Terminator ;

checkDeclFixity :: IdrisParser PDecl -> IdrisParser PDecl Source #

Check that a declaration of an operator also has fixity declared

checkNameFixity :: Name -> IdrisParser () Source #

Checks that an operator name also has a fixity declaration

fixityType :: IdrisParser (Int -> Fixity) Source #

Parses a fixity declaration type (i.e. infix or prefix, associtavity) FixityType ::= 'infixl' | 'infixr' | 'infix' | prefix ;

symbolicOperator :: Parsing m => m String Source #

Parses an operator

reservedOp :: Parsing m => String -> m () Source #

Parses a reserved operator