Documentation

Allow implicit type declarations

Disallow implicit type declarations

Parses an expression as a whole

  FullExpr ::= Expr EOF_t;

Parses an expression

  Expr ::= Expr';

Parses either an internally defined expression or a user-defined one

Expr' ::=  External (User-defined) Syntax
      |   InternalExpr;

Parses a user-defined expression

Parses a simple user-defined expression

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

Tries to parse an expression given a user-defined rule

Parses a (normal) built-in expression

InternalExpr ::=
  App
  | MatchApp
  | UnifyLog
  | RecordType
  | SimpleExpr
  | Lambda
  | QuoteGoal
  | Let
  | RewriteTerm
  | Pi
  | DoBlock
  ;

Parses a case expression

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

Parses a case in a case expression

CaseOption ::=
  Expr '=>' Expr Terminator
  ;

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

Parses a tactics block

TacticsExpr :=
  tactics OpenBlock Tactic'* CloseBlock
;

Parses a simple expression

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

Parses the rest of an expression in braces

Bracketed ::=
  ')'
  | Expr ')'
  | ExprList ')'
  | Expr ** Expr ')'
  | Operator Expr ')'
  | Expr Operator ')'
  | Name : Expr ** Expr ')'
  ;

Finds optimal type for integer constant

Parses a list literal expression e.g. [1,2,3]

ListExpr ::=
  '[' ExprList? ']'
;

ExprList ::=
  Expr
  | Expr ',' ExprList
  ;

Parses an alternative expression

  Alt ::= '(|' Expr_List '|)';

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

Parses a possibly hidden simple expression

HSimpleExpr ::=
  . SimpleExpr
  | SimpleExpr
  ;

Parses a matching application expression

MatchApp ::=
  SimpleExpr <== FnName
  ;

Parses a unification log expression

UnifyLog ::=
  % unifyLog SimpleExpr
  ;

Parses a no implicits expression

NoImplicits ::=
  % noImplicits SimpleExpr
  ;

Parses a function application expression

App ::=
  mkForeign Arg Arg*
  | SimpleExpr Arg+
  ;

Parses a function argument

Arg ::=
  ImplicitArg
  | ConstraintArg
  | SimpleExpr
  ;

Parses an implicit function argument

ImplicitArg ::=
  '{' Name ('=' Expr)? '}'
  ;

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

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

Parses a record field setter expression

RecordType ::=
  record '{' FieldTypeList '}';

FieldTypeList ::=
  FieldType
  | FieldType ',' FieldTypeList
  ;

FieldType ::=
  FnName '=' Expr
  ;

Creates setters for record types on necessary functions

Parses a type signature

TypeSig ::=
  : Expr
  ;

TypeExpr ::= ConstraintList? Expr;

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

SimpleExprList ::=
  SimpleExpr
  | SimpleExpr ',' SimpleExprList
  ;

Parses a term rewrite expression

RewriteTerm ::=
  rewrite Expr (==> Expr)? 'in' Expr
  ;

Parses a let binding

Let ::=
  'let' Name TypeSig'? '=' Expr  'in' Expr
| 'let' Expr'          '=' Expr' 'in' Expr

TypeSig' ::=
  : Expr'
  ;

Parses a quote goal

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

Parses a dependent type signature

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

Parses a type constraint list

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

Parses a type declaration list

TypeDeclList ::=
    FunctionSignatureList
  | NameList TypeSig
  ;

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

Parses a type declaration list with optional parameters

TypeOptDeclList ::=
    NameOrPlaceholder TypeSig?
  | NameOrPlaceholder TypeSig? ',' TypeOptDeclList
  ;

NameOrPlaceHolder ::= Name | '_';

Parses a list comprehension

Comprehension ::= '[' Expr '|' DoList ']';

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

Parses a do-block

Do' ::= Do KeepTerminator;

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

Parses an expression inside a do block

Do ::=
    'let' Name  TypeSig'?      '=' Expr
  | 'let' Expr'                '=' Expr
  | Name  '<-' Expr
  | Expr' '<-' Expr
  | Expr
  ;

Parses an expression in idiom brackets

Idiom ::= '[|' Expr '|]';

Parses a constant or literal expression

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

Parses a static modifier

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

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
  ;

Parses a tactic as a whole