idris-0.9.18.1: Functional Programming Language with Dependent Types

Safe HaskellNone
LanguageHaskell98

Idris.ParseExpr

Synopsis

Documentation

allowImp :: SyntaxInfo -> SyntaxInfo Source

Allow implicit type declarations

disallowImp :: SyntaxInfo -> SyntaxInfo Source

Disallow implicit type declarations

fullExpr :: SyntaxInfo -> IdrisParser PTerm Source

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

expr :: SyntaxInfo -> IdrisParser PTerm Source

Parses an expression Expr ::= Pi

opExpr :: SyntaxInfo -> IdrisParser PTerm Source

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

expr' :: SyntaxInfo -> IdrisParser PTerm Source

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

externalExpr :: SyntaxInfo -> IdrisParser PTerm Source

Parses a user-defined expression

simpleExternalExpr :: SyntaxInfo -> IdrisParser PTerm Source

Parses a simple user-defined expression

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

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

data SynMatch Source

Constructors

SynTm PTerm 
SynBind Name 

internalExpr :: SyntaxInfo -> IdrisParser PTerm Source

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

impossible :: IdrisParser PTerm Source

Parses the "impossible" keyword Impossible ::= impossible

caseExpr :: SyntaxInfo -> IdrisParser PTerm Source

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

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

Parses a case in a case expression CaseOption ::= Expr (Impossible | '=>' Expr) Terminator ;

proofExpr :: SyntaxInfo -> IdrisParser PTerm Source

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

tacticsExpr :: SyntaxInfo -> IdrisParser PTerm Source

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

simpleExpr :: SyntaxInfo -> IdrisParser PTerm Source

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 Source

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

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

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

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

Finds optimal type for integer constant

alt :: SyntaxInfo -> IdrisParser PTerm Source

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

Expr_List ::= Expr' | Expr' ',' Expr_List ; @

hsimpleExpr :: SyntaxInfo -> IdrisParser PTerm Source

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

unifyLog :: SyntaxInfo -> IdrisParser PTerm Source

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

runElab :: SyntaxInfo -> IdrisParser PTerm Source

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

disamb :: SyntaxInfo -> IdrisParser PTerm Source

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

noImplicits :: SyntaxInfo -> IdrisParser PTerm Source

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

app :: SyntaxInfo -> IdrisParser PTerm Source

Parses a function application expression App ::= mkForeign Arg Arg* | MatchApp | SimpleExpr Arg* ; MatchApp ::= SimpleExpr <== FnName ;

arg :: SyntaxInfo -> IdrisParser PArg Source

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

implicitArg :: SyntaxInfo -> IdrisParser PArg Source

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

constraintArg :: SyntaxInfo -> IdrisParser PArg Source

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

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

quasiquote :: SyntaxInfo -> IdrisParser PTerm Source

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

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

unquote :: SyntaxInfo -> IdrisParser PTerm Source

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

Unquote ::= ',' Expr

namequote :: SyntaxInfo -> IdrisParser PTerm Source

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

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

recordType :: SyntaxInfo -> IdrisParser PTerm Source

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

mkType :: Name -> Name Source

Creates setters for record types on necessary functions

typeExpr :: SyntaxInfo -> IdrisParser PTerm Source

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

lambda :: SyntaxInfo -> IdrisParser PTerm Source

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

rewriteTerm :: SyntaxInfo -> IdrisParser PTerm Source

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

let_ :: SyntaxInfo -> IdrisParser PTerm Source

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

TypeSig' ::= : Expr' ; @

if_ :: SyntaxInfo -> IdrisParser PTerm Source

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

quoteGoal :: SyntaxInfo -> IdrisParser PTerm Source

Parses a quote goal

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

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

Parses a dependent type signature

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

piOpts :: SyntaxInfo -> IdrisParser [ArgOpt] Source

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

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

Parses a type constraint list

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

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

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

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

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

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

NameOrPlaceHolder ::= Name | '_';

listExpr :: SyntaxInfo -> IdrisParser PTerm Source

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 Source

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

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

do_ :: SyntaxInfo -> IdrisParser PDo Source

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

idiom :: SyntaxInfo -> IdrisParser PTerm Source

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

constants :: [(String, Const)] Source

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) Source

Parse a constant and its source span

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

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

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

static :: IdrisParser Static Source

Parses a static modifier

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

data TacticArg Source

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)] Source

A list of available tactics and their argument requirements

fullTactic :: SyntaxInfo -> IdrisParser PTactic Source

Parses a tactic as a whole