xref: /plugin/mizarverifiabledocs/src/mizar.grammar (revision 8ead5b40c5012d5be54ad0f60e762955eca45eec)

@top Program { expression }

expression {
  expressionPart+
}

DefinitionBlock {
  "definition" expression "end"
}

Proof {
  "proof" expression "end"
}

NowBlock {
  "now" expression "end"
}

HerebyBlock {
  "hereby" expression "end"
}

expressionPart {
  KeywordControl |
  SupportFunction |
  KeywordOther |
  EntityNameType |
  ReasoningPhrase |
  Comment |
  OpenParen expression CloseParen |
  OpenBrace expression CloseBrace |
  OpenBracket expression CloseBracket |
  DefinitionBlock |
  Proof |
  NowBlock |
  HerebyBlock
}

@tokens {
  KeywordControl {
    "implies" |
    "holds" |
    "being" |
    "for" |
    "st" |
    "ex " |
    "not" |
    "&" |
    "or" |
    "iff"
  }
  SupportFunction {
    "equalities" |
    "expansions" |
    "theorem" |
    "theorems" |
    "scheme" |
    "definitions" |
    "clusters" |
    "signature" |
    "vocabulary" |
    "vocabularies" |
    "notation" |
    "notations" |
    "constructors" |
    "registration " |
    "registrations" |
    "requirements" |
    "schemes"
  }
  KeywordOther {
    "irreflexivity" |
    "connectedness" |
    "compatibility" |
    "contradiction" |
    "correctness" |
    "associativity" |
    "commutativity" |
    "consider" |
    "consistency" |
    "antonym" |
    "canceled" |
    "otherwise" |
    "reconsider" |
    "redefine" |
    "reflexivity" |
    "symmetry" |
    "uniqueness" |
    "transitivity" |
    "idempotence" |
    "asymmetry" |
    "projectivity" |
    "involutiveness" |
    "assume" |
    "cases" |
    "given" |
    "per" |
    "thus" |
    "take" |
    "hence" |
    "is " |
    "let" |
    "and" |
    "attr" |
    "as" |
    "be " |
    "begin" |
    "cluster" |
    "coherence" |
    "def" |
    "deffunc" |
    "defpred" |
    "environ" |
    "equals" |
    "existence" |
    "func" |
    "if " |
    "it" |
    "means" |
    "mode" |
    "of" |
    "over" |
    "pred" |
    "provided" |
    "qua" |
    "reserve" |
    "struct" |
    "such" |
    "synonym" |
    "that" |
    "then" |
    "thesis" |
    "where"
  }
  EntityNameType {
    // "proof"，"end"，"now"，"hereby" は削除
    "case" |
    "suppose"
  }
  Comment { "::" ![\n]* }
  ReasoningPhrase { ("by" | "from") ![^\n;]* }

  OpenParen { "(" }
  CloseParen { ")" }
  OpenBrace { "{" }
  CloseBrace { "}" }
  OpenBracket { "[" }
  CloseBracket { "]" }

  @precedence {
    Comment,
    ReasoningPhrase,
    KeywordControl,
    SupportFunction,
    KeywordOther,
    EntityNameType,
    OpenParen,
    CloseParen,
    OpenBrace,
    CloseBrace,
    OpenBracket,
    CloseBracket
  }
}

@external propSource highlighting from "./highlight.js"