//
// Created by intellij-pest on 2019-10-04
// narc-grammar
// Author: ice1000
//
WHITESPACE = _{ WHITE_SPACE | ("//" ~ (!NEWLINE ~ ANY)*) }
// Identifier
ident_char = _{ ASCII_ALPHA }
ident_raw = _{ ident_char ~ ident_following* }
ident_following =
_{ ident_char
| ASCII_DIGIT
| "'"
| "-"
| "+"
| ("/" ~ !"/")
| "\\"
}
///Darkgrey
ident = @{ ident_raw }
///Orange
universe = @{ "Type" }
arrow = _{ "->" }
dot_projection = { "." ~ ident }
///Red
meta = { "_" ~ ident }
dollar_op = _{ "$" }
applied = { primary_expr | dot_projection }
multi_param = { ident+ ~ ":" ~ expr }
implicit = { "{" ~ multi_param ~ "}" }
explicit = { "(" ~ multi_param ~ ")" }
param =
{ implicit
| explicit
| dollar_expr // unnamed parameter
}
//Placeholder
expr = { pi_expr }
pi_expr = { (param ~ arrow)* ~ dollar_expr }
dollar_expr = { app_expr ~ (dollar_op ~ app_expr)* }
app_expr = { primary_expr ~ applied* }
primary_expr =
{ universe
| meta
| ident
| "(" ~ expr ~ ")"
}
pattern =
{ inacc_pat
| cons_pat
| ident
}
cons_pat = { "(" ~ ident ~ pattern* ~ ")" }
// Using the notation from Agda's thesis
inacc_pat = { "|_" ~ expr ~ "_|" }
copattern = { pattern | dot_projection }
clause_body = { copattern* ~ "=" ~ expr }
clause = { "clause" ~ ident ~ clause_body ~ ";" }
definition = { "definition" ~ ident ~ ":" ~ expr ~ ";" }
constructors = { constructor* }
projections = { projection* }
data_body = { param* ~ "{" ~ constructors ~ "}" }
codata_body = { param* ~ "{" ~ projections ~ "}" }
data = { "data" ~ ident ~ data_body ~ ";" }
codata = { "codata" ~ ident ~ codata_body ~ ";" }
// Constructor may have no parameters
constructor = { "constructor" ~ ident ~ param* ~ ";" }
// Fields are annotated with a type instead of parameters
projection = { "projection" ~ ident ~ ":" ~ expr ~ ";" }
decl =
{ definition
| clause
| data
| codata
}
file = { WHITESPACE* ~ decl* ~ WHITESPACE* }