{-# LANGUAGE OverloadedStrings #-}
module Skylighting.Syntax.Idris (syntax) where

import Skylighting.Types
import Data.Map
import Skylighting.Regex
import qualified Data.Set

syntax :: Syntax
syntax = Syntax
  { sName = "Idris"
  , sFilename = "idris.xml"
  , sShortname = "Idris"
  , sContexts =
      fromList
        [ ( "block comment"
          , Context
              { cName = "block comment"
              , cSyntax = "Idris"
              , cRules =
                  [ Rule
                      { rMatcher = Detect2Chars '-' '}'
                      , rAttribute = CommentTok
                      , rIncludeAttribute = False
                      , rDynamic = False
                      , rCaseSensitive = True
                      , rChildren = []
                      , rLookahead = False
                      , rFirstNonspace = False
                      , rColumn = Nothing
                      , rContextSwitch = [ Pop ]
                      }
                  , Rule
                      { rMatcher = Detect2Chars '{' '-'
                      , rAttribute = CommentTok
                      , rIncludeAttribute = False
                      , rDynamic = False
                      , rCaseSensitive = True
                      , rChildren = []
                      , rLookahead = False
                      , rFirstNonspace = False
                      , rColumn = Nothing
                      , rContextSwitch = [ Push ( "Idris" , "block comment" ) ]
                      }
                  ]
              , cAttribute = CommentTok
              , cLineEmptyContext = []
              , cLineEndContext = []
              , cLineBeginContext = []
              , cFallthrough = False
              , cFallthroughContext = []
              , cDynamic = False
              }
          )
        , ( "char"
          , Context
              { cName = "char"
              , cSyntax = "Idris"
              , cRules =
                  [ Rule
                      { rMatcher =
                          RegExpr
                            RE
                              { reString = "\\\\."
                              , reCompiled = Just (compileRegex True "\\\\.")
                              , reCaseSensitive = True
                              }
                      , rAttribute = CharTok
                      , rIncludeAttribute = False
                      , rDynamic = False
                      , rCaseSensitive = True
                      , rChildren = []
                      , rLookahead = False
                      , rFirstNonspace = False
                      , rColumn = Nothing
                      , rContextSwitch = []
                      }
                  , Rule
                      { rMatcher = DetectChar '\''
                      , rAttribute = CharTok
                      , rIncludeAttribute = False
                      , rDynamic = False
                      , rCaseSensitive = True
                      , rChildren = []
                      , rLookahead = False
                      , rFirstNonspace = False
                      , rColumn = Nothing
                      , rContextSwitch = [ Pop ]
                      }
                  ]
              , cAttribute = CharTok
              , cLineEmptyContext = []
              , cLineEndContext = [ Pop ]
              , cLineBeginContext = []
              , cFallthrough = False
              , cFallthroughContext = []
              , cDynamic = False
              }
          )
        , ( "code"
          , Context
              { cName = "code"
              , cSyntax = "Idris"
              , cRules =
                  [ Rule
                      { rMatcher =
                          RegExpr
                            RE
                              { reString = "---*[^!#\\$%&\\*\\+/<=>\\?\\@\\^\\|~\\.:]?"
                              , reCompiled =
                                  Just
                                    (compileRegex True "---*[^!#\\$%&\\*\\+/<=>\\?\\@\\^\\|~\\.:]?")
                              , reCaseSensitive = True
                              }
                      , rAttribute = CommentTok
                      , rIncludeAttribute = False
                      , rDynamic = False
                      , rCaseSensitive = True
                      , rChildren = []
                      , rLookahead = False
                      , rFirstNonspace = False
                      , rColumn = Nothing
                      , rContextSwitch = [ Push ( "Idris" , "line comment" ) ]
                      }
                  , Rule
                      { rMatcher =
                          RegExpr
                            RE
                              { reString = "\\|\\|\\|[^\\-!#\\$%&\\*\\+/<=>\\?\\@\\^\\|~\\.:]?"
                              , reCompiled =
                                  Just
                                    (compileRegex
                                       True "\\|\\|\\|[^\\-!#\\$%&\\*\\+/<=>\\?\\@\\^\\|~\\.:]?")
                              , reCaseSensitive = True
                              }
                      , rAttribute = CommentTok
                      , rIncludeAttribute = False
                      , rDynamic = False
                      , rCaseSensitive = True
                      , rChildren = []
                      , rLookahead = False
                      , rFirstNonspace = False
                      , rColumn = Nothing
                      , rContextSwitch = [ Push ( "Idris" , "line comment" ) ]
                      }
                  , Rule
                      { rMatcher = Detect2Chars '{' '-'
                      , rAttribute = CommentTok
                      , rIncludeAttribute = False
                      , rDynamic = False
                      , rCaseSensitive = True
                      , rChildren = []
                      , rLookahead = False
                      , rFirstNonspace = False
                      , rColumn = Nothing
                      , rContextSwitch = [ Push ( "Idris" , "block comment" ) ]
                      }
                  , Rule
                      { rMatcher =
                          RegExpr
                            RE
                              { reString =
                                  "\\s*([a-z]+\\s+)*([A-Za-z][A-Za-z0-9_]*'*|\\([\\-!#\\$%&\\*\\+\\./<=>\\?@\\\\^\\|~:]+\\))\\s*:"
                              , reCompiled =
                                  Just
                                    (compileRegex
                                       True
                                       "\\s*([a-z]+\\s+)*([A-Za-z][A-Za-z0-9_]*'*|\\([\\-!#\\$%&\\*\\+\\./<=>\\?@\\\\^\\|~:]+\\))\\s*:")
                              , reCaseSensitive = True
                              }
                      , rAttribute = NormalTok
                      , rIncludeAttribute = False
                      , rDynamic = False
                      , rCaseSensitive = True
                      , rChildren = []
                      , rLookahead = True
                      , rFirstNonspace = False
                      , rColumn = Just 0
                      , rContextSwitch = [ Push ( "Idris" , "declaration" ) ]
                      }
                  , Rule
                      { rMatcher =
                          Keyword
                            KeywordAttr
                              { keywordCaseSensitive = True
                              , keywordDelims =
                                  Data.Set.fromList "\t\n !%&()*+,-./:;<=>?[\\]^{|}~"
                              }
                            (makeWordSet
                               True
                               [ "abstract"
                               , "auto"
                               , "case"
                               , "class"
                               , "codata"
                               , "covering"
                               , "data"
                               , "default"
                               , "do"
                               , "dsl"
                               , "else"
                               , "if"
                               , "implicit"
                               , "import"
                               , "impossible"
                               , "in"
                               , "index_first"
                               , "index_next"
                               , "infix"
                               , "infixl"
                               , "infixr"
                               , "instance"
                               , "lambda"
                               , "let"
                               , "module"
                               , "mututal"
                               , "namespace"
                               , "of"
                               , "parameters"
                               , "partial"
                               , "pattern"
                               , "postulate"
                               , "prefix"
                               , "private"
                               , "proof"
                               , "public"
                               , "record"
                               , "rewrite"
                               , "static"
                               , "syntax"
                               , "tactics"
                               , "term"
                               , "then"
                               , "total"
                               , "using"
                               , "variable"
                               , "where"
                               , "with"
                               ])
                      , rAttribute = KeywordTok
                      , rIncludeAttribute = False
                      , rDynamic = False
                      , rCaseSensitive = True
                      , rChildren = []
                      , rLookahead = False
                      , rFirstNonspace = False
                      , rColumn = Nothing
                      , rContextSwitch = []
                      }
                  , Rule
                      { rMatcher = DetectChar '%'
                      , rAttribute = KeywordTok
                      , rIncludeAttribute = False
                      , rDynamic = False
                      , rCaseSensitive = True
                      , rChildren = []
                      , rLookahead = False
                      , rFirstNonspace = False
                      , rColumn = Nothing
                      , rContextSwitch = [ Push ( "Idris" , "directive" ) ]
                      }
                  , Rule
                      { rMatcher =
                          Keyword
                            KeywordAttr
                              { keywordCaseSensitive = True
                              , keywordDelims =
                                  Data.Set.fromList "\t\n !%&()*+,-./:;<=>?[\\]^{|}~"
                              }
                            (makeWordSet
                               True
                               [ "applyTactic"
                               , "attack"
                               , "compute"
                               , "exact"
                               , "fill"
                               , "focus"
                               , "induction"
                               , "intro"
                               , "intros"
                               , "let"
                               , "refine"
                               , "reflect"
                               , "rewrite"
                               , "solve"
                               , "trivial"
                               , "try"
                               ])
                      , rAttribute = KeywordTok
                      , rIncludeAttribute = False
                      , rDynamic = False
                      , rCaseSensitive = True
                      , rChildren = []
                      , rLookahead = False
                      , rFirstNonspace = False
                      , rColumn = Nothing
                      , rContextSwitch = []
                      }
                  , Rule
                      { rMatcher = DetectChar '\''
                      , rAttribute = CharTok
                      , rIncludeAttribute = False
                      , rDynamic = False
                      , rCaseSensitive = True
                      , rChildren = []
                      , rLookahead = False
                      , rFirstNonspace = False
                      , rColumn = Nothing
                      , rContextSwitch = [ Push ( "Idris" , "char" ) ]
                      }
                  , Rule
                      { rMatcher = DetectChar '"'
                      , rAttribute = StringTok
                      , rIncludeAttribute = False
                      , rDynamic = False
                      , rCaseSensitive = True
                      , rChildren = []
                      , rLookahead = False
                      , rFirstNonspace = False
                      , rColumn = Nothing
                      , rContextSwitch = [ Push ( "Idris" , "string" ) ]
                      }
                  , Rule
                      { rMatcher = Int
                      , rAttribute = DecValTok
                      , rIncludeAttribute = False
                      , rDynamic = False
                      , rCaseSensitive = True
                      , rChildren = []
                      , rLookahead = False
                      , rFirstNonspace = False
                      , rColumn = Nothing
                      , rContextSwitch = []
                      }
                  , Rule
                      { rMatcher =
                          RegExpr
                            RE
                              { reString = "0[Xx][0-9A-Fa-f]+"
                              , reCompiled = Just (compileRegex True "0[Xx][0-9A-Fa-f]+")
                              , reCaseSensitive = True
                              }
                      , rAttribute = BaseNTok
                      , rIncludeAttribute = False
                      , rDynamic = False
                      , rCaseSensitive = True
                      , rChildren = []
                      , rLookahead = False
                      , rFirstNonspace = False
                      , rColumn = Nothing
                      , rContextSwitch = []
                      }
                  , Rule
                      { rMatcher =
                          RegExpr
                            RE
                              { reString = "0[Xx][0-9A-Fa-f]+"
                              , reCompiled = Just (compileRegex True "0[Xx][0-9A-Fa-f]+")
                              , reCaseSensitive = True
                              }
                      , rAttribute = BaseNTok
                      , rIncludeAttribute = False
                      , rDynamic = False
                      , rCaseSensitive = True
                      , rChildren = []
                      , rLookahead = False
                      , rFirstNonspace = False
                      , rColumn = Nothing
                      , rContextSwitch = []
                      }
                  , Rule
                      { rMatcher =
                          RegExpr
                            RE
                              { reString = "\\d+\\.\\d+([eE][-+]?\\d+)?"
                              , reCompiled =
                                  Just (compileRegex True "\\d+\\.\\d+([eE][-+]?\\d+)?")
                              , reCaseSensitive = True
                              }
                      , rAttribute = FloatTok
                      , rIncludeAttribute = False
                      , rDynamic = False
                      , rCaseSensitive = True
                      , rChildren = []
                      , rLookahead = False
                      , rFirstNonspace = False
                      , rColumn = Nothing
                      , rContextSwitch = []
                      }
                  , Rule
                      { rMatcher =
                          RegExpr
                            RE
                              { reString = "([A-Z][a-zA-Z0-9_]*'*|_\\|_)"
                              , reCompiled =
                                  Just (compileRegex True "([A-Z][a-zA-Z0-9_]*'*|_\\|_)")
                              , reCaseSensitive = True
                              }
                      , rAttribute = DataTypeTok
                      , rIncludeAttribute = False
                      , rDynamic = False
                      , rCaseSensitive = True
                      , rChildren = []
                      , rLookahead = False
                      , rFirstNonspace = False
                      , rColumn = Nothing
                      , rContextSwitch = []
                      }
                  , Rule
                      { rMatcher =
                          RegExpr
                            RE
                              { reString = "[a-z][a-zA-Z0-9_]*'*"
                              , reCompiled = Just (compileRegex True "[a-z][a-zA-Z0-9_]*'*")
                              , reCaseSensitive = True
                              }
                      , rAttribute = NormalTok
                      , rIncludeAttribute = False
                      , rDynamic = False
                      , rCaseSensitive = True
                      , rChildren = []
                      , rLookahead = False
                      , rFirstNonspace = False
                      , rColumn = Nothing
                      , rContextSwitch = []
                      }
                  , Rule
                      { rMatcher =
                          RegExpr
                            RE
                              { reString = "\\?[a-z][A-Za-z0-9_]+'*"
                              , reCompiled = Just (compileRegex True "\\?[a-z][A-Za-z0-9_]+'*")
                              , reCaseSensitive = True
                              }
                      , rAttribute = OtherTok
                      , rIncludeAttribute = False
                      , rDynamic = False
                      , rCaseSensitive = True
                      , rChildren = []
                      , rLookahead = False
                      , rFirstNonspace = False
                      , rColumn = Nothing
                      , rContextSwitch = []
                      }
                  , Rule
                      { rMatcher =
                          RegExpr
                            RE
                              { reString = "(:|=>|\\->|<\\-)"
                              , reCompiled = Just (compileRegex True "(:|=>|\\->|<\\-)")
                              , reCaseSensitive = True
                              }
                      , rAttribute = OtherTok
                      , rIncludeAttribute = False
                      , rDynamic = False
                      , rCaseSensitive = True
                      , rChildren = []
                      , rLookahead = False
                      , rFirstNonspace = False
                      , rColumn = Nothing
                      , rContextSwitch = []
                      }
                  , Rule
                      { rMatcher =
                          RegExpr
                            RE
                              { reString = "([\\-!#\\$%&\\*\\+\\./<=>\\?@\\\\^\\|~:]+|\\b_\\b)"
                              , reCompiled =
                                  Just
                                    (compileRegex
                                       True "([\\-!#\\$%&\\*\\+\\./<=>\\?@\\\\^\\|~:]+|\\b_\\b)")
                              , reCaseSensitive = True
                              }
                      , rAttribute = FunctionTok
                      , rIncludeAttribute = False
                      , rDynamic = False
                      , rCaseSensitive = True
                      , rChildren = []
                      , rLookahead = False
                      , rFirstNonspace = False
                      , rColumn = Nothing
                      , rContextSwitch = []
                      }
                  , Rule
                      { rMatcher =
                          RegExpr
                            RE
                              { reString = "`[A-Za-z][A-Za-z0-9_]*'*`"
                              , reCompiled = Just (compileRegex True "`[A-Za-z][A-Za-z0-9_]*'*`")
                              , reCaseSensitive = True
                              }
                      , rAttribute = FunctionTok
                      , rIncludeAttribute = False
                      , rDynamic = False
                      , rCaseSensitive = True
                      , rChildren = []
                      , rLookahead = False
                      , rFirstNonspace = False
                      , rColumn = Nothing
                      , rContextSwitch = []
                      }
                  ]
              , cAttribute = NormalTok
              , cLineEmptyContext = []
              , cLineEndContext = []
              , cLineBeginContext = []
              , cFallthrough = False
              , cFallthroughContext = []
              , cDynamic = False
              }
          )
        , ( "declaration"
          , Context
              { cName = "declaration"
              , cSyntax = "Idris"
              , cRules =
                  [ Rule
                      { rMatcher =
                          Keyword
                            KeywordAttr
                              { keywordCaseSensitive = True
                              , keywordDelims =
                                  Data.Set.fromList "\t\n !%&()*+,-./:;<=>?[\\]^{|}~"
                              }
                            (makeWordSet
                               True
                               [ "abstract"
                               , "auto"
                               , "case"
                               , "class"
                               , "codata"
                               , "covering"
                               , "data"
                               , "default"
                               , "do"
                               , "dsl"
                               , "else"
                               , "if"
                               , "implicit"
                               , "import"
                               , "impossible"
                               , "in"
                               , "index_first"
                               , "index_next"
                               , "infix"
                               , "infixl"
                               , "infixr"
                               , "instance"
                               , "lambda"
                               , "let"
                               , "module"
                               , "mututal"
                               , "namespace"
                               , "of"
                               , "parameters"
                               , "partial"
                               , "pattern"
                               , "postulate"
                               , "prefix"
                               , "private"
                               , "proof"
                               , "public"
                               , "record"
                               , "rewrite"
                               , "static"
                               , "syntax"
                               , "tactics"
                               , "term"
                               , "then"
                               , "total"
                               , "using"
                               , "variable"
                               , "where"
                               , "with"
                               ])
                      , rAttribute = KeywordTok
                      , rIncludeAttribute = False
                      , rDynamic = False
                      , rCaseSensitive = True
                      , rChildren = []
                      , rLookahead = False
                      , rFirstNonspace = False
                      , rColumn = Nothing
                      , rContextSwitch = []
                      }
                  , Rule
                      { rMatcher =
                          RegExpr
                            RE
                              { reString = "([A-Z][a-zA-Z0-9_]*'*|_\\|_)"
                              , reCompiled =
                                  Just (compileRegex True "([A-Z][a-zA-Z0-9_]*'*|_\\|_)")
                              , reCaseSensitive = True
                              }
                      , rAttribute = DataTypeTok
                      , rIncludeAttribute = False
                      , rDynamic = False
                      , rCaseSensitive = True
                      , rChildren = []
                      , rLookahead = False
                      , rFirstNonspace = False
                      , rColumn = Nothing
                      , rContextSwitch = []
                      }
                  , Rule
                      { rMatcher =
                          RegExpr
                            RE
                              { reString = "[a-z][A-Za-z0-9_]*'*"
                              , reCompiled = Just (compileRegex True "[a-z][A-Za-z0-9_]*'*")
                              , reCaseSensitive = True
                              }
                      , rAttribute = FunctionTok
                      , rIncludeAttribute = False
                      , rDynamic = False
                      , rCaseSensitive = True
                      , rChildren = []
                      , rLookahead = False
                      , rFirstNonspace = False
                      , rColumn = Nothing
                      , rContextSwitch = []
                      }
                  , Rule
                      { rMatcher =
                          RegExpr
                            RE
                              { reString = "\\([\\-!#\\$%&\\*\\+\\./<=>\\?@\\\\^\\|~:]+\\)"
                              , reCompiled =
                                  Just
                                    (compileRegex
                                       True "\\([\\-!#\\$%&\\*\\+\\./<=>\\?@\\\\^\\|~:]+\\)")
                              , reCaseSensitive = True
                              }
                      , rAttribute = FunctionTok
                      , rIncludeAttribute = False
                      , rDynamic = False
                      , rCaseSensitive = True
                      , rChildren = []
                      , rLookahead = False
                      , rFirstNonspace = False
                      , rColumn = Nothing
                      , rContextSwitch = []
                      }
                  , Rule
                      { rMatcher = DetectChar ':'
                      , rAttribute = OtherTok
                      , rIncludeAttribute = False
                      , rDynamic = False
                      , rCaseSensitive = True
                      , rChildren = []
                      , rLookahead = False
                      , rFirstNonspace = False
                      , rColumn = Nothing
                      , rContextSwitch = [ Pop ]
                      }
                  ]
              , cAttribute = NormalTok
              , cLineEmptyContext = []
              , cLineEndContext = [ Pop ]
              , cLineBeginContext = []
              , cFallthrough = False
              , cFallthroughContext = []
              , cDynamic = False
              }
          )
        , ( "directive"
          , Context
              { cName = "directive"
              , cSyntax = "Idris"
              , cRules =
                  [ Rule
                      { rMatcher =
                          Keyword
                            KeywordAttr
                              { keywordCaseSensitive = True
                              , keywordDelims =
                                  Data.Set.fromList "\t\n !%&()*+,-./:;<=>?[\\]^{|}~"
                              }
                            (makeWordSet
                               True
                               [ "abstract"
                               , "auto"
                               , "case"
                               , "class"
                               , "codata"
                               , "covering"
                               , "data"
                               , "default"
                               , "do"
                               , "dsl"
                               , "else"
                               , "if"
                               , "implicit"
                               , "import"
                               , "impossible"
                               , "in"
                               , "index_first"
                               , "index_next"
                               , "infix"
                               , "infixl"
                               , "infixr"
                               , "instance"
                               , "lambda"
                               , "let"
                               , "module"
                               , "mututal"
                               , "namespace"
                               , "of"
                               , "parameters"
                               , "partial"
                               , "pattern"
                               , "postulate"
                               , "prefix"
                               , "private"
                               , "proof"
                               , "public"
                               , "record"
                               , "rewrite"
                               , "static"
                               , "syntax"
                               , "tactics"
                               , "term"
                               , "then"
                               , "total"
                               , "using"
                               , "variable"
                               , "where"
                               , "with"
                               ])
                      , rAttribute = KeywordTok
                      , rIncludeAttribute = False
                      , rDynamic = False
                      , rCaseSensitive = True
                      , rChildren = []
                      , rLookahead = False
                      , rFirstNonspace = False
                      , rColumn = Nothing
                      , rContextSwitch = []
                      }
                  , Rule
                      { rMatcher =
                          Keyword
                            KeywordAttr
                              { keywordCaseSensitive = True
                              , keywordDelims =
                                  Data.Set.fromList "\t\n !%&()*+,-./:;<=>?[\\]^{|}~"
                              }
                            (makeWordSet
                               True
                               [ "access"
                               , "assert_total"
                               , "default"
                               , "dynamic"
                               , "elim"
                               , "error_handlers"
                               , "error_reverse"
                               , "flag"
                               , "hide"
                               , "include"
                               , "language"
                               , "lib"
                               , "link"
                               , "name"
                               , "provide"
                               , "reflection"
                               ])
                      , rAttribute = KeywordTok
                      , rIncludeAttribute = False
                      , rDynamic = False
                      , rCaseSensitive = True
                      , rChildren = []
                      , rLookahead = False
                      , rFirstNonspace = False
                      , rColumn = Nothing
                      , rContextSwitch = []
                      }
                  ]
              , cAttribute = NormalTok
              , cLineEmptyContext = []
              , cLineEndContext = [ Pop ]
              , cLineBeginContext = []
              , cFallthrough = False
              , cFallthroughContext = []
              , cDynamic = False
              }
          )
        , ( "line comment"
          , Context
              { cName = "line comment"
              , cSyntax = "Idris"
              , cRules = []
              , cAttribute = CommentTok
              , cLineEmptyContext = []
              , cLineEndContext = [ Pop ]
              , cLineBeginContext = []
              , cFallthrough = False
              , cFallthroughContext = []
              , cDynamic = False
              }
          )
        , ( "string"
          , Context
              { cName = "string"
              , cSyntax = "Idris"
              , cRules =
                  [ Rule
                      { rMatcher =
                          RegExpr
                            RE
                              { reString = "\\\\."
                              , reCompiled = Just (compileRegex True "\\\\.")
                              , reCaseSensitive = True
                              }
                      , rAttribute = StringTok
                      , rIncludeAttribute = False
                      , rDynamic = False
                      , rCaseSensitive = True
                      , rChildren = []
                      , rLookahead = False
                      , rFirstNonspace = False
                      , rColumn = Nothing
                      , rContextSwitch = []
                      }
                  , Rule
                      { rMatcher =
                          RegExpr
                            RE
                              { reString = "\""
                              , reCompiled = Just (compileRegex True "\"")
                              , reCaseSensitive = True
                              }
                      , rAttribute = StringTok
                      , rIncludeAttribute = False
                      , rDynamic = False
                      , rCaseSensitive = True
                      , rChildren = []
                      , rLookahead = False
                      , rFirstNonspace = False
                      , rColumn = Nothing
                      , rContextSwitch = [ Pop ]
                      }
                  ]
              , cAttribute = StringTok
              , cLineEmptyContext = []
              , cLineEndContext = []
              , cLineBeginContext = []
              , cFallthrough = False
              , cFallthroughContext = []
              , cDynamic = False
              }
          )
        ]
  , sAuthor = "Alexander Shabalin"
  , sVersion = "1.0"
  , sLicense = "LGPL"
  , sExtensions = [ "*.idr" ]
  , sStartingContext = "code"
  }