// This is a TextMate grammar distributed by `starry-night`.
// This grammar is developed at
// <https://github.com/leanprover/vscode-lean4>
// and licensed `apache-2.0`.
// See <https://github.com/wooorm/starry-night> for more info.
/**
 * @import {Grammar} from '@wooorm/starry-night'
 */

/** @type {Grammar} */
const grammar = {
  extensions: [],
  names: ['lean-4', 'lean4'],
  patterns: [
    {include: '#comments'},
    {match: '\\b(Prop|Type|Sort)\\b', name: 'storage.type.lean4'},
    {
      captures: {
        1: {name: 'storage.modifier.lean4'},
        2: {name: 'storage.modifier.lean4'},
        3: {name: 'storage.modifier.lean4'}
      },
      match: '\\b(attribute\\b\\s*)(?:(\\[[^\\]\\s]*\\])|\\[([^\\]\\s]*))'
    },
    {
      captures: {
        1: {name: 'storage.modifier.lean4'},
        2: {name: 'storage.modifier.lean4'},
        3: {name: 'storage.modifier.lean4'}
      },
      match: '(@)(?:(\\[[^\\]\\s]*\\])|\\[([^\\]\\s]*))'
    },
    {
      match:
        '\\b(?<!\\.)(local|scoped|partial|unsafe|nonrec|public|private|protected|noncomputable|meta)(?!\\.)\\b',
      name: 'storage.modifier.lean4'
    },
    {match: '\\b(sorry|admit|#exit)\\b', name: 'invalid.illegal.lean4'},
    {
      match:
        '#(print|eval|eval!|reduce|synth|widget|where|version|with_exporting|check|check_tactic|check_tactic_failure|check_failure|check_simp|discr_tree_key|discr_tree_simp_key|guard|guard_expr|guard_msgs)\\b',
      name: 'keyword.other.lean4'
    },
    {match: '\\bderiving\\s+instance\\b', name: 'keyword.other.command.lean4'},
    {
      begin:
        '\\b(?<!\\.)(inductive|coinductive|structure|theorem|axiom|abbrev|lemma|def|instance|class)\\b\\s+(\\{[^}]*\\})?',
      beginCaptures: {1: {name: 'keyword.other.definitioncommand.lean4'}},
      end: '(?=\\bwith\\b|\\bextends\\b|\\bwhere\\b|[:\\|\\(\\[\\{⦃<>])',
      name: 'meta.definitioncommand.lean4',
      patterns: [
        {include: '#comments'},
        {include: '#definitionName'},
        {match: ','}
      ]
    },
    {
      match:
        '\\b(?<!\\.)(theorem|show|have|using|haveI|from|suffices|nomatch|nofun|no_index|def|class|structure|instance|elab|set_option|initialize|builtin_initialize|example|inductive_fixpoint|inductive|coinductive_fixpoint|coinductive|termination_by\\?|termination_by|decreasing_by|partial_fixpoint|axiom|universe|variable|module|import all|import|open|export|prelude|renaming|hiding|do|by\\?|by|let|letI|let_expr|extends|mutual|mut|where|rec|declare_syntax_cat|syntax|macro_rules|macro|binop_lazy%|binop%|unop%|binrel_no_prop%|binrel%|leftact%|rightact%|max_prec|leading_parser|elab_rules|deriving|fun|section|namespace|end|prefix|postfix|infixl|infixr|infix|notation|abbrev|if|bif|then|else|calc|matches|match_expr|match|with|forall|for|while|repeat|unless|until|panic!|unreachable!|assert!|try|catch|finally|return|continue|break|exists|mod_cast|exact\\?%|include_str|include|in|trailing_parser|tactic_tag|tactic_alt|tactic_extension|register_tactic_tag|type_of%|binder_predicate|grind_propagator|builtin_grind_propagator|grind_pattern|simproc|builtin_simproc|simproc_pattern%|builtin_simproc_pattern%|simproc_decl|builtin_simproc_decl|dsimproc|builtin_dsimproc|dsimproc_decl|builtin_dsimproc_decl|show_panel_widgets|show_term|seal|unseal|nat_lit|norm_cast_add_elim|println!|private_decl%|declare_config_elab|decl_name%|register_error_explanation|register_builtin_option|register_option|register_parser_alias|register_simp_attr|register_linter_set|register_label_attr|recommended_spelling|reportIssue!|reprove|run_elab|run_cmd|run_meta|value_of%|add_decl_doc|omit|opaque|json%|dbg_trace|trace_goal\\[[^\\]\\s]*\\]|trace\\[[^\\]\\s]*\\]|throwErrorAt|throwError|throwNamedErrorAt|throwNamedError|logNamedWarningAt|logNamedWarning|logNamedErrorAt|logNamedError)(?!\\.)\\b',
      name: 'keyword.other.lean4'
    },
    {begin: '«', contentName: 'entity.name.lean4', end: '»'},
    {
      begin:
        '(s!|m!|throwError|dbg_trace|panic!|reportIssue!|(?:trace_goal|trace)\\[[^\\]\\s]*\\])\\s*"',
      beginCaptures: {1: {name: 'keyword.other.lean4'}},
      end: '"',
      name: 'string.interpolated.lean4',
      patterns: [
        {
          begin: '(\\{)',
          beginCaptures: {1: {name: 'keyword.other.lean4'}},
          end: '(\\})',
          endCaptures: {1: {name: 'keyword.other.lean4'}},
          patterns: [{include: '$self'}]
        },
        {match: '\\\\[\\\\"ntr\']', name: 'constant.character.escape.lean4'},
        {
          match: '\\\\x[0-9A-Fa-f][0-9A-Fa-f]',
          name: 'constant.character.escape.lean4'
        },
        {
          match: '\\\\u[0-9A-Fa-f][0-9A-Fa-f][0-9A-Fa-f][0-9A-Fa-f]',
          name: 'constant.character.escape.lean4'
        }
      ]
    },
    {
      begin: '"',
      end: '"',
      name: 'string.quoted.double.lean4',
      patterns: [
        {match: '\\\\[\\\\"ntr\']', name: 'constant.character.escape.lean4'},
        {
          match: '\\\\x[0-9A-Fa-f][0-9A-Fa-f]',
          name: 'constant.character.escape.lean4'
        },
        {
          match: '\\\\u[0-9A-Fa-f][0-9A-Fa-f][0-9A-Fa-f][0-9A-Fa-f]',
          name: 'constant.character.escape.lean4'
        }
      ]
    },
    {match: '\\b(true|false)\\b', name: 'constant.language.lean4'},
    {match: "(?<!\\]|\\w)'[^\\\\']'", name: 'string.quoted.single.lean4'},
    {
      captures: {1: {name: 'constant.character.escape.lean4'}},
      match:
        "(?<!\\]|\\w)'(\\\\(x[0-9A-Fa-f][0-9A-Fa-f]|u[0-9A-Fa-f][0-9A-Fa-f][0-9A-Fa-f][0-9A-Fa-f]|.))'",
      name: 'string.quoted.single.lean4'
    },
    {
      match:
        '\\b([0-9]+|0([xX][0-9a-fA-F]+)|[-]?(0|[1-9][0-9]*)(\\.[0-9]+)?([eE][+-]?[0-9]+)?)\\b',
      name: 'constant.numeric.lean4'
    }
  ],
  repository: {
    blockComment: {
      begin: '/-',
      end: '-/',
      name: 'comment.block.lean4',
      patterns: [{include: 'source.lean4.markdown'}, {include: '#blockComment'}]
    },
    comments: {
      patterns: [
        {include: '#dashComment'},
        {include: '#docComment'},
        {include: '#modDocComment'},
        {include: '#blockComment'}
      ]
    },
    dashComment: {
      begin: '--',
      end: '$',
      name: 'comment.line.double-dash.lean4',
      patterns: [{include: 'source.lean4.markdown'}]
    },
    definitionName: {
      patterns: [
        {
          match:
            '\\b[^:«»\\(\\)\\{\\}[:space:]=→λ∀?][^:«»\\(\\)\\{\\}[:space:]]*',
          name: 'entity.name.function.lean4'
        },
        {begin: '«', contentName: 'entity.name.function.lean4', end: '»'}
      ]
    },
    docComment: {
      begin: '/--',
      end: '-/',
      name: 'comment.block.documentation.lean4',
      patterns: [{include: 'source.lean4.markdown'}, {include: '#blockComment'}]
    },
    modDocComment: {
      begin: '/-!',
      end: '-/',
      name: 'comment.block.documentation.lean4',
      patterns: [{include: 'source.lean4.markdown'}, {include: '#blockComment'}]
    }
  },
  scopeName: 'source.lean4'
}

export default grammar