v0.1.z での構文の定式化

# expression/type/kind identifiers and labels:
x, l ::=
  (a lowercased identifier)

# module/signature identifiers and constructors:
X, C ::=
  (a capitalized identifier)

# (order-0) type variables:
type-var ::=
  (a lowercased identifier preceded by a single quotation mark)

# row variables:
row-var ::=
  (a lowercased identifier preceded by a single quotation mark and a question mark)

# source files:
file ::=
  header 'module' X [':>' S] '=' M

# headers:
header ::=
  (要加筆)

# module expressions:
M ::=
  | '(' M ')'
  | [X '.']* X                     # paths
  | 'fun' '(' X ':' S ')' '->' M   # functor abstractions
  | [X '.']* X '(' [X '.']* X ')'  # functor applications
  | 'struct' [B]* 'end'            # structures
  | [X '.']* X ':>' S              # coercion

# bindings:
B ::=
  | 'val' bind-val
  | 'type' bind-type
  | 'module' X [':>' S]? '=' M
  | 'signature' X '=' S
  | 'include' M

# value bindings:
bind-val ::=
  | bind-val-single
  | 'rec' bind-val-single ['and' bind-val-single]

bind-val-single ::=
  | x quant [bind-val-parameter]* '=' E
  | 'math' [x]? \x quant [bind-val-parameter]* '=' E
  | 'inline' [x]? \x quant [bind-val-parameter]* '=' E
  | 'block' [x]? +x quant [bind-val-parameter]* '=' E

bind-val-parameter ::=
  | '?(' [opt-parameter]* ')' parameter

# labeled optional parameters:
opt-parameter ::=
  | label '=' P [':' T]? ['=' E]?

# mandatory parameters:
parameter ::=
  | P                # patterns
  | '(' P ':' T ')'  # patterns with type annotations

# signatures:
S ::=
  | '(' S ')'
  | [X '.']* X                 # paths
  | '(' X ':' S ')' '->' S     # functor signatures
  | 'sig' [D]* 'end'           # structure signatures
  | S 'with' 'type' bind-type

# declarations:
D ::=
  | 'val' x quant ':' T
  | 'type' x '::' K
  | 'type' bind-type
  | 'module' X ':' S
  | 'signature' X '=' S
  | 'include' S

# order-1 kinds:
K ::=
  | base-kind
  | '(' [base-kind >? ',']+ ')' '->' base-kind

# base kinds:
base-kind ::=
  | x  # kind names (only 'o' is valid)

# row kinds:
row-kind ::=
  | '(|' [l >? ',']+ '|)'

# types:
T ::=
  | '(' T ')'
  | type-var                      # type variables
  | [X '.']* x [T]*               # type applications
  | [type-opts]? T '->' T         # function types
  | T '*' T ['*' T]*              # product types
  | '(|' [ l ':' T >? ',']+ '|)'  # record types
  | 'math' cmd-parameter-types    # math command types
  | 'inline' cmd-parameter-types  # inline command types
  | 'block' cmd-parameter-types   # block command types

cmd-parameter-types ::=
  | [' [cmd-parameter-type >? ',']* ']'

cmd-parameter-type ::=
  | [type-opts-closed]? T

type-opts ::=
  | type-opts-closed
  | '?(' [label ':' T ',']+ row-var ')'

type-opts-closed ::=
  | '?(' [label ':' T >? ',']+ ')'

# universal quantifiers
quant ::=
  | [type-var]* [row-var '::' row-kind]*

# expressions:
E ::=
  | '(' E ')'
  | [X '.']* x                          # variables
  | 'fun' [bind-val-parameter]* '->' E  # abstractions
  | E [expr-opts]? E                    # applications
  | 'let' bind-val 'in' E               # local value bindings
  | 'let' non-var-pattern '=' E 'in' E  # pattern matching by let
  | 'match' E 'with' [P '->' E]+ 'end'  # pattern matching
  | 'if' E 'then' E 'else' E            # conditional branching
  | [X '.']* C [E]?                     # constructor applications
  | E bin-op E                          # binary operations
  | un-op E                             # unary operations
  | matchable-const
  | non-matchable-const
  | '{' TI '}'                          # inline texts
  | '\'<' TB '>'                        # block texts
  | '${' TM '}'                         # math formulae
  (要加筆)

# inline texts:
TI ::=
  (要加筆)

# block texts:
TB ::=  
  (要加筆)

# math formulae:
TM ::=
  (要加筆)

expr-opts ::=
  | '?(' [label '=' E >? /,/]+ ')'

matchable-const ::=
  | '(' ')'  # the unit value
  | 'true'
  | 'false'
  | (a decimal integer literal)
  | (a hexadecimal integer literal)
  | (a string literal enclosed by back ticks)

non-matchable-const ::=
  | (a floating-point number literal)
  | (a length literal)

# patterns:
P ::=
  | x                # variable patterns
  | non-var-pattern  # non-variable patterns

# patterns except for variables:
non-var-pattern ::=
  | '(' non-var-pattern ')'
  | '_'                        # wildcards
  | [X '.']* C [P]?            # constructor patterns
  | '(' P ',' [P >? ',']+ ')'  # tuple patterns
  | matchable-const