minitt 0.2.2

// Lexical rules
WHITESPACE = _{ " " | "\t" | NEWLINE | ("--" ~ (!NEWLINE ~ ANY)*) }

// Primitive helpers
character =
 _{ ASCII_ALPHA
  | "_"
  | "\'"
  | "\\"
  | '0'..'9'
  }
identifier_simple =
 @{ !"let"
  ~ !"rec"
  ~ !"split"
  ~ !"sum"
  ~ !"const"
  ~ !"\\lambda"
  ~ !"\\Sigma"
  ~ !"\\Pi"
  ~ !"0"
  ~ !"1"
  ~ !"_"
  ~ character+
  }
identifier_raw =
 @{ ("sum" ~ character+)
  | ("split" ~ character+)
  | ("let" ~ character+)
  | ("rec" ~ character+)
  | ("const" ~ character+)
  | ("0" ~ character+)
  | ("1" ~ character+)
  | ("_" ~ character+)
  }
identifier = { identifier_simple | identifier_raw }
constructor_name = @{ ASCII_ALPHA_UPPER ~ identifier? }
pi = _{ "\\Pi" | "\u{03A0}" }
sigma = _{ "\\Sigma" | "\u{03A3}" }
lambda = _{ "\\lambda" | "\u{03BB}" }
multiplication = _{ "*" | "\\times" | "\xd7" | "\u{2716}" }
for_all = _{ "\\forall" | "\u{2200}" }
double_arrow = _{ "=>" | "\u{21d2}" }
single_arrow = _{ "->" | "\u{2192}" }
let_or_rec = { "let" | "rec" }
one = { "1" }
unit = { "0" }
universe = { "U" }
// void = { EOI }
meta_var = { "_" }

// Prefixed parameters
prefix_parameter = { "(" ~ typed_pattern ~ ")" }
prefix_parameters = { prefix_parameter* }

// Patterns
atom_pattern = { identifier | meta_var | "(" ~ pattern ~ ")" }
pair_pattern = { atom_pattern ~ "," ~ pattern }
pattern = { pair_pattern | atom_pattern }
maybe_pattern = { pattern? }

// Extracted helpers
typed_pattern = _{ pattern ~ ":" ~ expression }
typed_abstraction = _{ typed_pattern ~ "." ~ expression }
branches = _{ "{" ~ (constructor ~ ("|" ~ constructor)*)? ~ "}" }
choices = _{ "{" ~ (pattern_match ~ ("|" ~ pattern_match)*)? ~ "}" }

// Atomic expressions
pi_type = { pi ~ typed_abstraction }
lambda_expression = { lambda ~ pattern ~ "." ~ expression }
constructor = { constructor_name ~ expression? }
pattern_match =
 { constructor_name
 ~ maybe_pattern
 ~ double_arrow
 ~ expression
 }
sigma_type = { sigma ~ typed_abstraction }
split = { "split" ~ choices }
sum = { "sum" ~ branches }
variable = { identifier }
atom =
  { universe
  | constructor
  | variable
  | split
  | sum
  | one
  | unit
  | pi_type
  | sigma_type
  | lambda_expression
  | "(" ~ expression ~ ")"
  }

// Syntactic sugars: short-hand for unit patterns
function_type = { atom ~ single_arrow ~ expression }
pair_type = { atom ~ multiplication ~ expression }

// Higher-level expressions
application = { atom ~ expression }
pair = { atom ~ "," ~ expression }
first = { atom ~ ".1" }
second = { atom ~ ".2" }
expression =
 { declaration
 | const_declaration
 | application
 | function_type
 | pair_type
 | first
 | second
 | pair
 | atom
 }

// Declaration
const_declaration =
 { "const"
 ~ pattern
 ~ "=" ~ expression
 ~ ";" ~ expression?
 }
declaration =
 { let_or_rec
 ~ pattern
 ~ prefix_parameters
 ~ ":" ~ expression
 ~ "=" ~ expression
 ~ ";" ~ expression?
 }