Draft grammar for the Amy programming language

amy.grammar

tokens:
  INFINITY ≔ '∞'
  ZERO ≔ '0'
  ONE ≔ '1'
  NONZERO ≔ /[1-9][0-9]*/
  QUESTION_MARK ≔ '?'
  BANG ≔ '!'

  NAME ≔ /[A-Za-z_][A-Za-z0-9_']*/
  CONTAINS ≔ '∋'

  PLUS ≔ '+'
  MINUS ≔ '-'
  ASTERISK ≔ '*'

  COLON ≔ ':'
  COLON_EQUAL ≔ '≔'
  VERTICAL_BAR ≔ '│'

  ARROW_LEFT ≔ '←'
  ARROW_DOWN ≔ '↓'
  ARROW_LONG_RIGHT ≔ '->'

  PAREN_LEFT ≔ '('
  PAREN_RIGHT ≔ ')'

;; general rules

annotation ⩴ COLON type_expr

;; grading defaults to linear, hence 'explicit'
grading ⩴
  | affine_grading
  | quantified_grading
  | linear_explicit_grading
  | unbounded_grading

affine_grading ⩴ QUESTION_MARK
quantified_grading ⩴ NONZERO
linear_explicit_grading ⩴ ONE
unbounded_grading ⩴ INFINITY

;; patterns

pattern ⩴
  | app_pattern
  | assigning_pattern
  | capturing_pattern ;; identifier pattern
  | grouping_pattern
  | integer_pattern
  | intro_pattern

app_pattern ⩴ grouping_pattern pattern+
assigning_pattern ⩴ NAME COLON_EQUAL pattern

capturing_pattern ⩴
  | NAME
  | NAME CONTAINS capturing_pattern

grouping_pattern ⩴ PAREN_LEFT pattern PAREN_RIGHT
integer_pattern ⩴ ZERO | NONZERO
intro_pattern ⩴ PLUS pattern

;; type-level expressions

type_expr ⩴
  | arrow_type_expr
  | grading_type_expr
  | grouping_type_expr
  | identifier_type_expr

arrow_type_expr ⩴ grouping_type_expr ARROW_LONG_RIGHT type_expr

grading_type_expr ⩴
  | elim_type_expr  ;; or consuming
  | intro_type_expr ;; or producing

elim_type_expr ⩴ MINUS grading? type_expr
intro_type_expr ⩴ PLUS type_expr
grouping_type_expr ⩴ PAREN_LEFT type_expr PAREN_RIGHT

identifier_type_expr ⩴
  | NAME
  | NAME CONTAINS identifier_type_expr

;; term-level expressions

expr ⩴
  | app_expr
  | elim_expr
  | grouping_expr
  | identifier_expr
  | integer_expr
  | intro_expr

app_expr ⩴ grouping_expr expr+
elim_expr ⩴ MINUS expr
grouping_expr ⩴ PAREN_LEFT expr PAREN_RIGHT

identifier_expr ⩴
  | NAME
  | NAME CONTAINS identifier_expr

integer_expr ⩴ ZERO | NONZERO
intro_expr ⩴ PLUS grading? expr

;; statements

stmt ⩴
  | bring_stmt
  | close_stmt
  | compute_stmt
  | elim_stmt
  | intro_stmt
  | pose_stmt

bring_stmt ⩴ ARROW_DOWN identifier_expr
close_stmt ⩴ BANG NAME
compute_stmt ⩴ ARROW_LEFT expr
elim_stmt ⩴ MINUS NAME
intro_stmt ⩴ PLUS grading? NAME annotation? intro_body

intro_body ⩴
  | COLON_EQUAL expr
  | (VERTICAL_BAR? intro_branch) (VERTICAL_BAR intro_branch)*

intro_branch ⩴ NAME pattern* COLON_EQUAL expr
pose_stmt ⩴ ASTERISK NAME COLON type_expr

;; program

program ⩴ stmt*

example.amy

↓ IO

*∞  Bool : Type
*∞  False : Bool
*∞  True : Bool
!   Bool

+∞  fact : Nat -> Nat
│   fact 0 ≔ 1
│   fact (n ≔ S n') ≔ mul n (fact n')

+ n ≔ 42
← IO∋print (- Nat∋to_decimal n)