minitt 0.1.6

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

// Primitive helpers
character =
 _{ ASCII_ALPHA
  | "_"
  | "\'"
  | "\\"
  | '0'..'9'
  }
identifier_simple =
 @{ !"let"
  ~ !"rec"
  ~ !"split"
  ~ !"sum"
  ~ !"\\lambda"
  ~ !"\\Sigma"
  ~ !"\\Pi"
  ~ !"0"
  ~ !"1"
  ~ !"_"
  ~ character+
  }
identifier_raw =
 @{ ("fun" ~ character+)
  | ("split" ~ character+)
  | ("let" ~ character+)
  | ("rec" ~ character+)
  | ("0" ~ character+)
  | ("1" ~ character+)
  | ("_" ~ character+)
  }
identifier = { identifier_simple | identifier_raw }
constructor_name = @{ ASCII_ALPHA_UPPER ~ identifier? }
pi = _{ "Π" | "\\Pi" }
sigma = _{ "Σ" | "\\Sigma" }
lambda = _{ "λ" | "\\lambda" }
multiplication = _{ "*" | "\\times" | "×" }
let_or_rec = { "let" | "rec" }
one = { "1" }
unit = { "0" }
universe = { "U" }
void = { EOI }
meta_var = { "_" }

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

// Extracted helpers
typed_abstraction = _{ pattern ~ ":" ~ expression ~ "." ~ 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 ~ pattern ~ "=>" ~ 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 ~ "->" ~ expression }
pair_type = { atom ~ multiplication ~ expression }

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

// Declaration
declaration =
 { let_or_rec
 ~ pattern
 ~ ":" ~ expression
 ~ "=" ~ expression
 ~ ";" ~ expression
 }