Idris.ParseExpr

Documentation

allowImp :: SyntaxInfo -> SyntaxInfo

Allow implicit type declarations

disallowImp :: SyntaxInfo -> SyntaxInfo

Disallow implicit type declarations

fullExpr :: SyntaxInfo -> IdrisParser PTerm

Parses an expression as a whole FullExpr ::= Expr EOF_t;

expr :: SyntaxInfo -> IdrisParser PTerm

Parses an expression Expr ::= Expr';

expr' :: SyntaxInfo -> IdrisParser PTerm

Parses either an internally defined expression or a user-defined one Expr' ::= External (User-defined) Syntax | InternalExpr;

doexpr' :: SyntaxInfo -> IdrisParser PTerm

externalExpr :: SyntaxInfo -> IdrisParser PTerm

Parses a user-defined expression

simpleExternalExpr :: SyntaxInfo -> IdrisParser PTerm

Parses a simple user-defined expression

extensions :: SyntaxInfo -> [Syntax] -> IdrisParser PTerm

Tries to parse a user-defined expression given a list of syntactic extensions

data SynMatch

Constructors

SynTm PTerm

SynBind Name

extension :: SyntaxInfo -> Syntax -> IdrisParser PTerm

Tries to parse an expression given a user-defined rule

internalExpr :: SyntaxInfo -> IdrisParser PTerm

Parses a (normal) built-in expression InternalExpr ::= App | MatchApp | UnifyLog | RecordType | SimpleExpr | Lambda | QuoteGoal | Let | RewriteTerm | Pi | CaseExpr | DoBlock ;

caseExpr :: SyntaxInfo -> IdrisParser PTerm

Parses a case expression CaseExpr ::= 'case' Expr 'of' OpenBlock CaseOption+ CloseBlock;

caseOption :: SyntaxInfo -> IdrisParser (PTerm, PTerm)

Parses a case in a case expression CaseOption ::= Expr '=>' Expr Terminator ;

proofExpr :: SyntaxInfo -> IdrisParser PTerm

Parses a proof block ProofExpr ::= proof OpenBlock Tactic'* CloseBlock ;

tacticsExpr :: SyntaxInfo -> IdrisParser PTerm

Parses a tactics block TacticsExpr := tactics OpenBlock Tactic'* CloseBlock ;

simpleExpr :: SyntaxInfo -> IdrisParser PTerm

Parses a simple expression SimpleExpr ::= '![' Term ']' | ? Name | % 'instance' | refl ('{' Expr '}')? | ProofExpr | TacticsExpr | FnName | List | Comprehension | Alt | Idiom | '(' Bracketed | Constant | Type | '_|_' | '_' | ;

bracketed :: SyntaxInfo -> IdrisParser PTerm

Parses the rest of an expression in braces Bracketed ::= ')' | Expr ')' | ExprList ')' | Expr ** Expr ')' | Operator Expr ')' | Expr Operator ')' | Name : Expr ** Expr ')' ;

bracketedExpr :: SyntaxInfo -> PTerm -> IdrisParser PTerm

modifyConst :: SyntaxInfo -> FC -> PTerm -> PTerm

Finds optimal type for integer constant

listExpr :: SyntaxInfo -> IdrisParser PTerm

Parses a list literal expression e.g. [1,2,3] ListExpr ::= '[' ExprList? ']' ; ExprList ::= Expr | Expr ',' ExprList ;

alt :: SyntaxInfo -> IdrisParser PTerm

Parses an alternative expression Alt ::= '(|' Expr_List '|)'; Expr_List ::= Expr' | Expr' ',' Expr_List ;

hsimpleExpr :: SyntaxInfo -> IdrisParser PTerm

Parses a possibly hidden simple expression HSimpleExpr ::= . SimpleExpr | SimpleExpr ;

matchApp :: SyntaxInfo -> IdrisParser PTerm

Parses a matching application expression MatchApp ::= SimpleExpr <== FnName ;

unifyLog :: SyntaxInfo -> IdrisParser PTerm

Parses a unification log expression UnifyLog ::= % unifyLog SimpleExpr ;

disamb :: SyntaxInfo -> IdrisParser PTerm

Parses a disambiguation expression Disamb ::= % disamb NameList Expr ;

noImplicits :: SyntaxInfo -> IdrisParser PTerm

Parses a no implicits expression NoImplicits ::= % noImplicits SimpleExpr ;

app :: SyntaxInfo -> IdrisParser PTerm

Parses a function application expression App ::= mkForeign Arg Arg* | SimpleExpr Arg+ ;

arg :: SyntaxInfo -> IdrisParser PArg

Parses a function argument Arg ::= ImplicitArg | ConstraintArg | SimpleExpr ;

implicitArg :: SyntaxInfo -> IdrisParser PArg

Parses an implicit function argument ImplicitArg ::= '{' Name ('=' Expr)? '}' ;

constraintArg :: SyntaxInfo -> IdrisParser PArg

Parses a constraint argument (for selecting a named type class instance)

    ConstraintArg ::=
      '@{' Expr '}'
      ;

recordType :: SyntaxInfo -> IdrisParser PTerm

Parses a record field setter expression RecordType ::= record '{' FieldTypeList '}'; FieldTypeList ::= FieldType | FieldType ',' FieldTypeList ; FieldType ::= FnName '=' Expr ;

mkType :: Name -> Name

Creates setters for record types on necessary functions

typeExpr :: SyntaxInfo -> IdrisParser PTerm

Parses a type signature TypeSig ::= : Expr ; TypeExpr ::= ConstraintList? Expr;

lambda :: SyntaxInfo -> IdrisParser PTerm

Parses a lambda expression Lambda ::= \\ TypeOptDeclList '=>' Expr | \\ SimpleExprList '=>' Expr ; SimpleExprList ::= SimpleExpr | SimpleExpr ',' SimpleExprList ;

rewriteTerm :: SyntaxInfo -> IdrisParser PTerm

Parses a term rewrite expression RewriteTerm ::= rewrite Expr (==> Expr)? 'in' Expr ;

let_ :: SyntaxInfo -> IdrisParser PTerm

Parses a let binding Let ::= 'let' Name TypeSig'? '=' Expr 'in' Expr | 'let' Expr' '=' Expr' 'in' Expr TypeSig' ::= : Expr' ;

quoteGoal :: SyntaxInfo -> IdrisParser PTerm

Parses a quote goal

QuoteGoal ::=
  quoteGoal Name by Expr 'in' Expr
  ;

pi :: SyntaxInfo -> IdrisParser PTerm

Parses a dependent type signature

Pi ::=
    '|'? Static? '('           TypeDeclList ')' DocComment '->' Expr
  | '|'? Static? '{'           TypeDeclList '}'            '->' Expr
  |              '{' auto    TypeDeclList '}'            '->' Expr
  |              '{' 'default' TypeDeclList '}'            '->' Expr
  ;

constraintList :: SyntaxInfo -> IdrisParser [PTerm]

Parses a type constraint list

ConstraintList ::=
    '(' Expr_List ')' '=>'
  | Expr              '=>'
  ;

typeDeclList :: SyntaxInfo -> IdrisParser [(Name, PTerm)]

Parses a type declaration list TypeDeclList ::= FunctionSignatureList | NameList TypeSig ;

FunctionSignatureList ::=
    Name TypeSig
  | Name TypeSig ',' FunctionSignatureList
  ;

tyOptDeclList :: SyntaxInfo -> IdrisParser [(Name, PTerm)]

Parses a type declaration list with optional parameters TypeOptDeclList ::= NameOrPlaceholder TypeSig? | NameOrPlaceholder TypeSig? ',' TypeOptDeclList ;

NameOrPlaceHolder ::= Name | '_';

comprehension :: SyntaxInfo -> IdrisParser PTerm

Parses a list comprehension Comprehension ::= '[' Expr '|' DoList ']';

DoList ::=
    Do
  | Do ',' DoList
  ;

doBlock :: SyntaxInfo -> IdrisParser PTerm

Parses a do-block Do' ::= Do KeepTerminator;

DoBlock ::=
  'do' OpenBlock Do'+ CloseBlock
  ;

do_ :: SyntaxInfo -> IdrisParser PDo

Parses an expression inside a do block Do ::= 'let' Name TypeSig'? '=' Expr | 'let' Expr' '=' Expr | Name '<-' Expr | Expr' '<-' Expr | Expr ;

idiom :: SyntaxInfo -> IdrisParser PTerm

Parses an expression in idiom brackets Idiom ::= '[|' Expr '|]';

constant :: IdrisParser Const

Parses a constant or literal expression

Constant ::=
    Integer
  | Int
  | Char
  | Float
  | String
  | Ptr
  | prim__UnsafeBuffer
  | Bits8
  | Bits16
  | Bits32
  | Bits64
  | Bits8x16
  | Bits16x8
  | Bits32x4
  | Bits64x2
  | Float_t
  | Natural_t
  | VerbatimString_t
  | String_t
  | Char_t
  ;

verbatimStringLiteral :: MonadicParsing m => m String

Parses a verbatim multi-line string literal (triple-quoted)

VerbatimString_t ::=
  '"""' ~'"""' '"""'
;

static :: IdrisParser Static

Parses a static modifier

Static ::=
  '[' static ']'
;

tactic :: SyntaxInfo -> IdrisParser PTactic

Parses a tactic script

Tactic ::= intro NameList?
       |   intros
       |   refine      Name Imp+
       |   mrefine     Name
       |   rewrite     Expr
       |   equiv       Expr
       |   'let'         Name : Expr' '=' Expr
       |   'let'         Name           '=' Expr
       |   focus       Name
       |   exact       Expr
       |   applyTactic Expr
       |   reflect     Expr
       |   fill        Expr
       |   try         Tactic '|' Tactic
       |   '{' TacticSeq '}'
       |   compute
       |   trivial
       |   solve
       |   attack
       |   state
       |   term
       |   undo
       |   qed
       |   abandon
       |   : q
       ;

Imp ::= ? | '_';

TacticSeq ::=
    Tactic ';' Tactic
  | Tactic ';' TacticSeq
  ;

fullTactic :: SyntaxInfo -> IdrisParser PTactic

Parses a tactic as a whole