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

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

syntax :: Syntax
syntax = Syntax
  { sName = "Agda"
  , sFilename = "agda.xml"
  , sShortname = "Agda"
  , sContexts =
      fromList
        [ ( "char"
          , Context
              { cName = "char"
              , cSyntax = "Agda"
              , cRules =
                  [ Rule
                      { rMatcher = Detect2Chars '\\' '\''
                      , 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 = "Agda"
              , cRules =
                  [ Rule
                      { rMatcher =
                          RegExpr
                            RE
                              { reString = "\\{-#.*#-\\}"
                              , reCompiled = Just (compileRegex True "\\{-#.*#-\\}")
                              , reCaseSensitive = True
                              }
                      , rAttribute = PreprocessorTok
                      , 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
                               [ "abstract"
                               , "codata"
                               , "coinductive"
                               , "constructor"
                               , "data"
                               , "field"
                               , "forall"
                               , "hiding"
                               , "import"
                               , "in"
                               , "inductive"
                               , "infix"
                               , "infixl"
                               , "infixr"
                               , "let"
                               , "module"
                               , "mutual"
                               , "open"
                               , "pattern"
                               , "postulate"
                               , "primitive"
                               , "private"
                               , "public"
                               , "quote"
                               , "quoteGoal"
                               , "quoteTerm"
                               , "record"
                               , "renaming"
                               , "rewrite"
                               , "syntax"
                               , "to"
                               , "unquote"
                               , "using"
                               , "where"
                               , "with"
                               ])
                      , rAttribute = KeywordTok
                      , rIncludeAttribute = False
                      , rDynamic = False
                      , rCaseSensitive = True
                      , rChildren = []
                      , rLookahead = False
                      , rFirstNonspace = False
                      , rColumn = Nothing
                      , rContextSwitch = []
                      }
                  , Rule
                      { rMatcher =
                          RegExpr
                            RE
                              { reString =
                                  "(Prop|Set[\226\130\128-\226\130\137]+|Set[0-9]*)(?=([_;.\"(){}@]|\\s|$))"
                              , reCompiled =
                                  Just
                                    (compileRegex
                                       True
                                       "(Prop|Set[\226\130\128-\226\130\137]+|Set[0-9]*)(?=([_;.\"(){}@]|\\s|$))")
                              , reCaseSensitive = True
                              }
                      , rAttribute = DataTypeTok
                      , rIncludeAttribute = False
                      , rDynamic = False
                      , rCaseSensitive = True
                      , rChildren = []
                      , rLookahead = False
                      , rFirstNonspace = False
                      , rColumn = Nothing
                      , rContextSwitch = []
                      }
                  , Rule
                      { rMatcher =
                          RegExpr
                            RE
                              { reString =
                                  "(->|\226\134\146|\226\136\128|\206\187|:|=|\\|)(?=([_;.\"(){}@]|\\s|$))"
                              , reCompiled =
                                  Just
                                    (compileRegex
                                       True
                                       "(->|\226\134\146|\226\136\128|\206\187|:|=|\\|)(?=([_;.\"(){}@]|\\s|$))")
                              , reCaseSensitive = True
                              }
                      , rAttribute = OtherTok
                      , rIncludeAttribute = False
                      , rDynamic = False
                      , rCaseSensitive = True
                      , rChildren = []
                      , rLookahead = False
                      , rFirstNonspace = False
                      , rColumn = Nothing
                      , rContextSwitch = []
                      }
                  , Rule
                      { rMatcher =
                          RegExpr
                            RE
                              { reString = "\\d+\\.\\d+(?=([_;.\"(){}@]|\\s|$))"
                              , reCompiled =
                                  Just (compileRegex True "\\d+\\.\\d+(?=([_;.\"(){}@]|\\s|$))")
                              , reCaseSensitive = True
                              }
                      , rAttribute = FloatTok
                      , rIncludeAttribute = False
                      , rDynamic = False
                      , rCaseSensitive = True
                      , rChildren = []
                      , rLookahead = False
                      , rFirstNonspace = False
                      , rColumn = Nothing
                      , rContextSwitch = []
                      }
                  , Rule
                      { rMatcher =
                          RegExpr
                            RE
                              { reString = "[0-9]+(?=([_;.\"(){}@]|\\s|$))"
                              , reCompiled =
                                  Just (compileRegex True "[0-9]+(?=([_;.\"(){}@]|\\s|$))")
                              , reCaseSensitive = True
                              }
                      , rAttribute = DecValTok
                      , 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 ( "Agda" , "char" ) ]
                      }
                  , Rule
                      { rMatcher = DetectChar '"'
                      , rAttribute = StringTok
                      , rIncludeAttribute = False
                      , rDynamic = False
                      , rCaseSensitive = True
                      , rChildren = []
                      , rLookahead = False
                      , rFirstNonspace = False
                      , rColumn = Nothing
                      , rContextSwitch = [ Push ( "Agda" , "string" ) ]
                      }
                  , Rule
                      { rMatcher = Detect2Chars '-' '-'
                      , rAttribute = CommentTok
                      , rIncludeAttribute = False
                      , rDynamic = False
                      , rCaseSensitive = True
                      , rChildren = []
                      , rLookahead = False
                      , rFirstNonspace = False
                      , rColumn = Nothing
                      , rContextSwitch = [ Push ( "Agda" , "comment" ) ]
                      }
                  , Rule
                      { rMatcher = Detect2Chars '{' '-'
                      , rAttribute = CommentTok
                      , rIncludeAttribute = False
                      , rDynamic = False
                      , rCaseSensitive = True
                      , rChildren = []
                      , rLookahead = False
                      , rFirstNonspace = False
                      , rColumn = Nothing
                      , rContextSwitch = [ Push ( "Agda" , "comments" ) ]
                      }
                  , Rule
                      { rMatcher = Detect2Chars '{' '!'
                      , rAttribute = OtherTok
                      , rIncludeAttribute = False
                      , rDynamic = False
                      , rCaseSensitive = True
                      , rChildren = []
                      , rLookahead = False
                      , rFirstNonspace = False
                      , rColumn = Nothing
                      , rContextSwitch = [ Push ( "Agda" , "hole" ) ]
                      }
                  , Rule
                      { rMatcher = AnyChar "_;.\"(){}@\\\\"
                      , rAttribute = OtherTok
                      , rIncludeAttribute = False
                      , rDynamic = False
                      , rCaseSensitive = True
                      , rChildren = []
                      , rLookahead = False
                      , rFirstNonspace = False
                      , rColumn = Nothing
                      , rContextSwitch = []
                      }
                  , Rule
                      { rMatcher =
                          RegExpr
                            RE
                              { reString = "[^_;.\"(){}@\\s]+"
                              , reCompiled = Just (compileRegex True "[^_;.\"(){}@\\s]+")
                              , reCaseSensitive = True
                              }
                      , rAttribute = NormalTok
                      , rIncludeAttribute = False
                      , rDynamic = False
                      , rCaseSensitive = True
                      , rChildren = []
                      , rLookahead = False
                      , rFirstNonspace = False
                      , rColumn = Nothing
                      , rContextSwitch = []
                      }
                  ]
              , cAttribute = NormalTok
              , cLineEmptyContext = []
              , cLineEndContext = []
              , cLineBeginContext = []
              , cFallthrough = False
              , cFallthroughContext = []
              , cDynamic = False
              }
          )
        , ( "comment"
          , Context
              { cName = "comment"
              , cSyntax = "Agda"
              , cRules = []
              , cAttribute = CommentTok
              , cLineEmptyContext = []
              , cLineEndContext = [ Pop ]
              , cLineBeginContext = []
              , cFallthrough = False
              , cFallthroughContext = []
              , cDynamic = False
              }
          )
        , ( "comments"
          , Context
              { cName = "comments"
              , cSyntax = "Agda"
              , cRules =
                  [ Rule
                      { rMatcher = Detect2Chars '{' '-'
                      , rAttribute = CommentTok
                      , rIncludeAttribute = False
                      , rDynamic = False
                      , rCaseSensitive = True
                      , rChildren = []
                      , rLookahead = False
                      , rFirstNonspace = False
                      , rColumn = Nothing
                      , rContextSwitch = [ Push ( "Agda" , "comments" ) ]
                      }
                  , Rule
                      { rMatcher = Detect2Chars '-' '}'
                      , rAttribute = CommentTok
                      , rIncludeAttribute = False
                      , rDynamic = False
                      , rCaseSensitive = True
                      , rChildren = []
                      , rLookahead = False
                      , rFirstNonspace = False
                      , rColumn = Nothing
                      , rContextSwitch = [ Pop ]
                      }
                  ]
              , cAttribute = CommentTok
              , cLineEmptyContext = []
              , cLineEndContext = []
              , cLineBeginContext = []
              , cFallthrough = False
              , cFallthroughContext = []
              , cDynamic = False
              }
          )
        , ( "hole"
          , Context
              { cName = "hole"
              , cSyntax = "Agda"
              , cRules =
                  [ Rule
                      { rMatcher = Detect2Chars '!' '}'
                      , rAttribute = OtherTok
                      , rIncludeAttribute = False
                      , rDynamic = False
                      , rCaseSensitive = True
                      , rChildren = []
                      , rLookahead = False
                      , rFirstNonspace = False
                      , rColumn = Nothing
                      , rContextSwitch = [ Pop ]
                      }
                  ]
              , cAttribute = OtherTok
              , cLineEmptyContext = []
              , cLineEndContext = []
              , cLineBeginContext = []
              , cFallthrough = False
              , cFallthroughContext = []
              , cDynamic = False
              }
          )
        , ( "string"
          , Context
              { cName = "string"
              , cSyntax = "Agda"
              , cRules =
                  [ Rule
                      { rMatcher = Detect2Chars '\\' '"'
                      , rAttribute = StringTok
                      , rIncludeAttribute = False
                      , rDynamic = False
                      , rCaseSensitive = True
                      , rChildren = []
                      , rLookahead = False
                      , rFirstNonspace = False
                      , rColumn = Nothing
                      , rContextSwitch = []
                      }
                  , Rule
                      { rMatcher = DetectChar '"'
                      , 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 = "Matthias C. M. Troffaes"
  , sVersion = "2"
  , sLicense = "LGPL"
  , sExtensions = [ "*.agda" ]
  , sStartingContext = "code"
  }