Safe Haskell | None |
---|
- allowImp :: SyntaxInfo -> SyntaxInfo
- disallowImp :: SyntaxInfo -> SyntaxInfo
- fullExpr :: SyntaxInfo -> IdrisParser PTerm
- tryFullExpr :: SyntaxInfo -> IState -> String -> Either Err PTerm
- expr :: SyntaxInfo -> IdrisParser PTerm
- opExpr :: SyntaxInfo -> IdrisParser PTerm
- expr' :: SyntaxInfo -> IdrisParser PTerm
- externalExpr :: SyntaxInfo -> IdrisParser PTerm
- simpleExternalExpr :: SyntaxInfo -> IdrisParser PTerm
- extensions :: SyntaxInfo -> [Syntax] -> IdrisParser PTerm
- data SynMatch
- extension :: SyntaxInfo -> Syntax -> IdrisParser PTerm
- internalExpr :: SyntaxInfo -> IdrisParser PTerm
- caseExpr :: SyntaxInfo -> IdrisParser PTerm
- caseOption :: SyntaxInfo -> IdrisParser (PTerm, PTerm)
- proofExpr :: SyntaxInfo -> IdrisParser PTerm
- tacticsExpr :: SyntaxInfo -> IdrisParser PTerm
- simpleExpr :: SyntaxInfo -> IdrisParser PTerm
- bracketed :: SyntaxInfo -> IdrisParser PTerm
- bracketed' :: SyntaxInfo -> IdrisParser PTerm
- bracketedExpr :: SyntaxInfo -> PTerm -> IdrisParser PTerm
- modifyConst :: SyntaxInfo -> FC -> PTerm -> PTerm
- alt :: SyntaxInfo -> IdrisParser PTerm
- hsimpleExpr :: SyntaxInfo -> IdrisParser PTerm
- unifyLog :: SyntaxInfo -> IdrisParser PTerm
- disamb :: SyntaxInfo -> IdrisParser PTerm
- noImplicits :: SyntaxInfo -> IdrisParser PTerm
- app :: SyntaxInfo -> IdrisParser PTerm
- arg :: SyntaxInfo -> IdrisParser PArg
- implicitArg :: SyntaxInfo -> IdrisParser PArg
- constraintArg :: SyntaxInfo -> IdrisParser PArg
- quasiquote :: SyntaxInfo -> IdrisParser PTerm
- unquote :: SyntaxInfo -> IdrisParser PTerm
- recordType :: SyntaxInfo -> IdrisParser PTerm
- mkType :: Name -> Name
- typeExpr :: SyntaxInfo -> IdrisParser PTerm
- lambda :: SyntaxInfo -> IdrisParser PTerm
- rewriteTerm :: SyntaxInfo -> IdrisParser PTerm
- let_ :: SyntaxInfo -> IdrisParser PTerm
- let_binding :: SyntaxInfo -> StateT IState IdrisInnerParser (FC, PTerm, PTerm, PTerm, [(PTerm, PTerm)])
- quoteGoal :: SyntaxInfo -> IdrisParser PTerm
- pi :: SyntaxInfo -> IdrisParser PTerm
- piOpts :: SyntaxInfo -> IdrisParser [ArgOpt]
- constraintList :: SyntaxInfo -> IdrisParser [PTerm]
- typeDeclList :: SyntaxInfo -> IdrisParser [(Name, PTerm)]
- tyOptDeclList :: SyntaxInfo -> IdrisParser [(Name, PTerm)]
- listExpr :: SyntaxInfo -> IdrisParser PTerm
- doBlock :: SyntaxInfo -> IdrisParser PTerm
- do_ :: SyntaxInfo -> IdrisParser PDo
- do_alt :: SyntaxInfo -> StateT IState IdrisInnerParser (PTerm, PTerm)
- idiom :: SyntaxInfo -> IdrisParser PTerm
- constant :: IdrisParser Const
- verbatimStringLiteral :: MonadicParsing m => m String
- static :: IdrisParser Static
- tactic :: SyntaxInfo -> IdrisParser PTactic
- fullTactic :: SyntaxInfo -> IdrisParser PTactic
Documentation
allowImp :: SyntaxInfo -> SyntaxInfoSource
Allow implicit type declarations
disallowImp :: SyntaxInfo -> SyntaxInfoSource
Disallow implicit type declarations
fullExpr :: SyntaxInfo -> IdrisParser PTermSource
Parses an expression as a whole
FullExpr ::= Expr EOF_t;
tryFullExpr :: SyntaxInfo -> IState -> String -> Either Err PTermSource
expr :: SyntaxInfo -> IdrisParser PTermSource
Parses an expression
Expr ::= Pi
opExpr :: SyntaxInfo -> IdrisParser PTermSource
Parses an expression with possible operator applied
OpExpr ::= ;
expr' :: SyntaxInfo -> IdrisParser PTermSource
Parses either an internally defined expression or
a user-defined one
Expr' ::= External (User-defined) Syntax
| InternalExpr;
externalExpr :: SyntaxInfo -> IdrisParser PTermSource
Parses a user-defined expression
simpleExternalExpr :: SyntaxInfo -> IdrisParser PTermSource
Parses a simple user-defined expression
extensions :: SyntaxInfo -> [Syntax] -> IdrisParser PTermSource
Tries to parse a user-defined expression given a list of syntactic extensions
extension :: SyntaxInfo -> Syntax -> IdrisParser PTermSource
Tries to parse an expression given a user-defined rule
internalExpr :: SyntaxInfo -> IdrisParser PTermSource
Parses a (normal) built-in expression
InternalExpr ::=
UnifyLog
| RecordType
| SimpleExpr
| Lambda
| QuoteGoal
| Let
| RewriteTerm
| CaseExpr
| DoBlock
| App
;
caseExpr :: SyntaxInfo -> IdrisParser PTermSource
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 '=>' Expr Terminator
;
proofExpr :: SyntaxInfo -> IdrisParser PTermSource
Parses a proof block
ProofExpr ::=
proof
OpenBlock Tactic'* CloseBlock
;
tacticsExpr :: SyntaxInfo -> IdrisParser PTermSource
Parses a tactics block
TacticsExpr :=
tactics
OpenBlock Tactic'* CloseBlock
;
simpleExpr :: SyntaxInfo -> IdrisParser PTermSource
Parses a simple expression
SimpleExpr ::=
|
?
Name
| % 'instance'
| Refl
('{' Expr '}')?
| ProofExpr
| TacticsExpr
| FnName
| Idiom
| List
| Alt
| Bracketed
| Constant
| Type
| Void
| Quasiquote
| Unquote
| '_'
;
bracketed :: SyntaxInfo -> IdrisParser PTermSource
Parses an expression in braces
Bracketed ::= '(' Bracketed'
bracketed' :: SyntaxInfo -> IdrisParser PTermSource
Parses the rest of an expression in braces
Bracketed' ::=
')'
| Expr ')'
| ExprList ')'
| Expr
**
Expr ')'
| Operator Expr ')'
| Expr Operator ')'
| Name :
Expr **
Expr ')'
;
bracketedExpr :: SyntaxInfo -> PTerm -> IdrisParser PTermSource
modifyConst :: SyntaxInfo -> FC -> PTerm -> PTermSource
Finds optimal type for integer constant
alt :: SyntaxInfo -> IdrisParser PTermSource
Parses an alternative expression
Alt ::= '(|' Expr_List '|)';
Expr_List ::=
Expr'
| Expr' ',' Expr_List
;
hsimpleExpr :: SyntaxInfo -> IdrisParser PTermSource
Parses a possibly hidden simple expression
HSimpleExpr ::=
.
SimpleExpr
| SimpleExpr
;
unifyLog :: SyntaxInfo -> IdrisParser PTermSource
Parses a unification log expression
UnifyLog ::=
%
unifyLog
SimpleExpr
;
disamb :: SyntaxInfo -> IdrisParser PTermSource
Parses a disambiguation expression
Disamb ::=
%
disamb
NameList Expr
;
noImplicits :: SyntaxInfo -> IdrisParser PTermSource
Parses a no implicits expression
NoImplicits ::=
%
noImplicits
SimpleExpr
;
app :: SyntaxInfo -> IdrisParser PTermSource
Parses a function application expression
App ::=
mkForeign
Arg Arg*
| MatchApp
| SimpleExpr Arg*
;
MatchApp ::=
SimpleExpr <==
FnName
;
arg :: SyntaxInfo -> IdrisParser PArgSource
Parses a function argument
Arg ::=
ImplicitArg
| ConstraintArg
| SimpleExpr
;
implicitArg :: SyntaxInfo -> IdrisParser PArgSource
Parses an implicit function argument
ImplicitArg ::=
'{' Name ('=' Expr)? '}'
;
constraintArg :: SyntaxInfo -> IdrisParser PArgSource
Parses a constraint argument (for selecting a named type class instance)
ConstraintArg ::= '@{' Expr '}' ;
quasiquote :: SyntaxInfo -> IdrisParser PTermSource
Parses a quasiquote expression (for building reflected terms using the elaborator)
Quasiquote ::= '`(' Expr ')'
unquote :: SyntaxInfo -> IdrisParser PTermSource
Parses an unquoting inside a quasiquotation (for building reflected terms using the elaborator)
Unquote ::= ',' Expr
recordType :: SyntaxInfo -> IdrisParser PTermSource
Parses a record field setter expression
RecordType ::=
record
'{' FieldTypeList '}';
FieldTypeList ::=
FieldType
| FieldType ',' FieldTypeList
;
FieldType ::=
FnName '=' Expr
;
typeExpr :: SyntaxInfo -> IdrisParser PTermSource
Parses a type signature
TypeSig ::=
:
Expr
;
TypeExpr ::= ConstraintList? Expr;
lambda :: SyntaxInfo -> IdrisParser PTermSource
Parses a lambda expression
Lambda ::=
\\
TypeOptDeclList '=>' Expr
| \\
SimpleExprList '=>' Expr
;
SimpleExprList ::=
SimpleExpr
| SimpleExpr ',' SimpleExprList
;
rewriteTerm :: SyntaxInfo -> IdrisParser PTermSource
Parses a term rewrite expression
RewriteTerm ::=
rewrite
Expr (==>
Expr)? 'in' Expr
;
let_ :: SyntaxInfo -> IdrisParser PTermSource
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)])Source
quoteGoal :: SyntaxInfo -> IdrisParser PTermSource
Parses a quote goal
QuoteGoal ::=quoteGoal
Nameby
Expr 'in' Expr ;
pi :: SyntaxInfo -> IdrisParser PTermSource
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 [PTerm]Source
Parses a type constraint list
ConstraintList ::= '(' Expr_List ')' '=>' | Expr '=>' ;
typeDeclList :: SyntaxInfo -> IdrisParser [(Name, PTerm)]Source
Parses a type declaration list
TypeDeclList ::=
FunctionSignatureList
| NameList TypeSig
;
FunctionSignatureList ::= Name TypeSig | Name TypeSig ',' FunctionSignatureList ;
tyOptDeclList :: SyntaxInfo -> IdrisParser [(Name, PTerm)]Source
Parses a type declaration list with optional parameters
TypeOptDeclList ::=
NameOrPlaceholder TypeSig?
| NameOrPlaceholder TypeSig? ',' TypeOptDeclList
;
NameOrPlaceHolder ::= Name | '_';
listExpr :: SyntaxInfo -> IdrisParser PTermSource
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 PTermSource
Parses a do-block
Do' ::= Do KeepTerminator;
DoBlock ::= 'do' OpenBlock Do'+ CloseBlock ;
do_ :: SyntaxInfo -> IdrisParser PDoSource
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)Source
idiom :: SyntaxInfo -> IdrisParser PTermSource
Parses an expression in idiom brackets
Idiom ::= '[|' Expr '|]';
constant :: IdrisParser ConstSource
Parses a constant or literal expression
Constant ::=Integer
|Int
|Char
|Float
|String
|Ptr
|ManagedPtr
|prim__UnsafeBuffer
|Bits8
|Bits16
|Bits32
|Bits64
|Bits8x16
|Bits16x8
|Bits32x4
|Bits64x2
| Float_t | Natural_t | VerbatimString_t | String_t | Char_t ;
verbatimStringLiteral :: MonadicParsing m => m StringSource
Parses a verbatim multi-line string literal (triple-quoted)
VerbatimString_t ::= '"""' ~'"""' '"""' ;
static :: IdrisParser StaticSource
Parses a static modifier
Static ::= '[' static ']' ;
tactic :: SyntaxInfo -> IdrisParser PTacticSource
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 ;
fullTactic :: SyntaxInfo -> IdrisParser PTacticSource
Parses a tactic as a whole