Idris.Parser.Expr

Documentation

allowImp :: SyntaxInfo -> SyntaxInfo

Allow implicit type declarations

disallowImp :: SyntaxInfo -> SyntaxInfo

Disallow implicit type declarations

allowConstr :: SyntaxInfo -> SyntaxInfo

Allow scoped constraint arguments

fullExpr :: SyntaxInfo -> IdrisParser PTerm

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

tryFullExpr :: SyntaxInfo -> IState -> String -> Either Err PTerm

expr :: SyntaxInfo -> IdrisParser PTerm

Parses an expression Expr ::= Pi

opExpr :: SyntaxInfo -> IdrisParser PTerm

Parses an expression with possible operator applied OpExpr ::= ;

expr' :: SyntaxInfo -> IdrisParser PTerm

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

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 FC Name

the FC is for highlighting information

Instances

Show SynMatch

extension :: SyntaxInfo -> [Maybe (Name, SynMatch)] -> [Syntax] -> IdrisParser PTerm

updateSynMatch :: [(Name, SynMatch)] -> PTerm -> PTerm

internalExpr :: SyntaxInfo -> IdrisParser PTerm

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

impossible :: IdrisParser PTerm

Parses the "impossible" keyword Impossible ::= impossible

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 (Impossible | '=>' Expr) Terminator ;

warnTacticDeprecation :: FC -> IdrisParser ()

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 ::=

| ? Name | % 'instance' | Refl ('{' Expr '}')? | ProofExpr | TacticsExpr | FnName | Idiom | List | Alt | Bracketed | Constant | Type | Void | Quasiquote | NameQuote | Unquote | '_' ; @

bracketed :: SyntaxInfo -> IdrisParser PTerm

Parses an expression in parentheses Bracketed ::= '(' Bracketed'

bracketed' :: FC -> SyntaxInfo -> IdrisParser PTerm

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

dependentPair :: PunInfo -> [(PTerm, Maybe (FC, PTerm), FC)] -> FC -> SyntaxInfo -> IdrisParser PTerm

Parses the rest of a dependent pair after '(' or '(Expr **'

bracketedExpr :: SyntaxInfo -> FC -> PTerm -> IdrisParser PTerm

Parse the contents of parentheses, after an expression has been parsed.

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

Finds optimal type for integer constant

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 ;

unifyLog :: SyntaxInfo -> IdrisParser PTerm

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

runElab :: SyntaxInfo -> IdrisParser PTerm

Parses a new-style tactics expression RunTactics ::= % runElab SimpleExpr ;

disamb :: SyntaxInfo -> IdrisParser PTerm

Parses a disambiguation expression Disamb ::= with 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* | MatchApp | SimpleExpr Arg* ; MatchApp ::= SimpleExpr <== FnName ;

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 '}'
     ;

quasiquote :: SyntaxInfo -> IdrisParser PTerm

Parses a quasiquote expression (for building reflected terms using the elaborator)

Quasiquote ::= '`(' Expr ')'

unquote :: SyntaxInfo -> IdrisParser PTerm

Parses an unquoting inside a quasiquotation (for building reflected terms using the elaborator)

Unquote ::= ',' Expr

namequote :: SyntaxInfo -> IdrisParser PTerm

Parses a quotation of a name (for using the elaborator to resolve boring details)

NameQuote ::= '`{' Name '}'

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 LambdaTail | \\ SimpleExprList LambdaTail ; SimpleExprList ::= SimpleExpr | SimpleExpr ',' SimpleExprList ; LambdaTail ::= Impossible | '=>' Expr

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' ; @

let_binding :: SyntaxInfo -> StateT IState IdrisInnerParser (FC, PTerm, PTerm, PTerm, [(PTerm, PTerm)])

if_ :: SyntaxInfo -> IdrisParser PTerm

Parses a conditional expression If ::= 'if' Expr 'then' Expr 'else' Expr

quoteGoal :: SyntaxInfo -> IdrisParser PTerm

Parses a quote goal

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

bindsymbol :: (LookAheadParsing m, DeltaParsing m) => [ArgOpt] -> Static -> t -> m Plicity

Parses a dependent type signature

Pi ::= PiOpts Static? Pi'

Pi' ::=
    OpExpr ('->' Pi)?
  | '(' TypeDeclList           ')'            '->' Pi
  | '{' TypeDeclList           '}'            '->' Pi
  | '{' auto    TypeDeclList '}'            '->' Pi
  | '{' 'default' SimpleExpr TypeDeclList '}' '->' Pi
  ;

explicitPi :: [ArgOpt] -> Static -> SyntaxInfo -> StateT IState IdrisInnerParser PTerm

autoImplicit :: t -> Static -> SyntaxInfo -> StateT IState IdrisInnerParser PTerm

defaultImplicit :: t -> Static -> SyntaxInfo -> StateT IState IdrisInnerParser PTerm

normalImplicit :: [ArgOpt] -> Static -> SyntaxInfo -> StateT IState IdrisInnerParser PTerm

constraintPi :: [ArgOpt] -> Static -> SyntaxInfo -> StateT IState IdrisInnerParser PTerm

implicitPi :: [ArgOpt] -> Static -> SyntaxInfo -> StateT IState IdrisInnerParser PTerm

unboundPi :: [ArgOpt] -> Static -> SyntaxInfo -> StateT IState IdrisInnerParser PTerm

pi :: SyntaxInfo -> IdrisParser PTerm

piOpts :: SyntaxInfo -> IdrisParser [ArgOpt]

Parses Possible Options for Pi Expressions PiOpts ::= .?

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

Parses a type constraint list

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

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

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

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

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

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

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

NameOrPlaceHolder ::= Name | '_';

listExpr :: SyntaxInfo -> IdrisParser PTerm

Parses a list literal expression e.g. [1,2,3] or a comprehension [ (x, y) | x <- xs , y <- ys ] ListExpr ::= '[' ']' | '[' Expr '|' DoList ']' | '[' ExprList ']' ; DoList ::= Do | Do ',' DoList ; ExprList ::= Expr | Expr ',' ExprList ;

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 ;

do_alt :: SyntaxInfo -> StateT IState IdrisInnerParser (PTerm, PTerm)

idiom :: SyntaxInfo -> IdrisParser PTerm

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

constants :: [(String, Const)]

Parses a constant or literal expression

Constant ::=
    Integer
  | Int
  | Char
  | Double
  | String
  | Bits8
  | Bits16
  | Bits32
  | Bits64
  | Float_t
  | Natural_t
  | VerbatimString_t
  | String_t
  | Char_t
  ;

constant :: IdrisParser (Const, FC)

Parse a constant and its source span

verbatimStringLiteral :: MonadicParsing m => m (String, FC)

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

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

static :: IdrisParser Static

Parses a static modifier

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

data TacticArg

Parses a tactic script

Tactic ::= intro NameList?
       |   intros
       |   refine      Name Imp+
       |   mrefine     Name
       |   rewrite     Expr
       |   induction   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
  ;

A specification of the arguments that tactics can take

Constructors

NameTArg

Names: n1, n2, n3, ... n

ExprTArg

AltsTArg

StringLitTArg

tactics :: [([String], Maybe TacticArg, SyntaxInfo -> IdrisParser PTactic)]

A list of available tactics and their argument requirements

tactic :: SyntaxInfo -> IdrisParser PTactic

fullTactic :: SyntaxInfo -> IdrisParser PTactic

Parses a tactic as a whole