Metamath raku grammar

Metamath.rakumod

# Metamath commentless grammar
# remove comments beforehand with
# .subst: / '$(' ~ '$)' .*? /, '', :g

unit grammar Metamath;

rule TOP { ^ <database> $ }

rule database { <outermost-scope-stmt>* }
rule outermost-scope-stmt {
  | <include-stmt> 
    | <constant-stmt> 
    | <stmt>
}

rule include-stmt { '$[' ~ '$]' <filename> }
rule constant-stmt { '$c' ~ '$.' <constant>+ }

rule stmt {
  <block> |
    <variable-stmt> | <disjoint-stmt> | <hypothesis-stmt> | <assert-stmt>
}

rule block { '${' ~ '$}' <stmt>* }
rule variable-stmt { '$v' ~ '$.' <variable>* }
rule disjoint-stmt { '$d' ~ '$.' <variable> ** 2..* }
rule hypothesis-stmt { <floating-stmt> | <essential-stmt> }

rule floating-stmt { <LABEL> '$f' ~ '$.' [<typecode> <variable>] }
rule essential-stmt { <LABEL> '$e' ~ '$.' [<typecode> <MATH-SYMBOL> *] }

rule assert-stmt { <axiom-stmt> | <provable-stmt> }

rule axiom-stmt { <LABEL> '$a' ~ '$.' [ <typecode> <MATH-SYMBOL> * ] }

rule provable-stmt {
  <LABEL> '$p' <typecode> <MATH-SYMBOL> * '$=' ~ '$.' <proof>
}
rule proof { <uncompressed-proof> | <compressed-proof> }
rule uncompressed-proof { [ <LABEL> | '?' ] + }
rule compressed-proof { [ '(' ~ ')' <LABEL> * ] <COMPRESSED-PROOF-BLOCK> + }

rule typecode { <constant> }

rule filename { <MATH-SYMBOL> }
rule constant { <MATH-SYMBOL> }
rule variable { <MATH-SYMBOL> }

token MATH-SYMBOL { <+[\H]-[$]>+ }
token LABEL { <+alpha+digit+[.-]>+ }
token COMPRESSED-PROOF-BLOCK { <[A..Z?]>+ }