content: {-|
  Module      : What4.Symbol
  Description : Datatype for representing names that can be communicated to solvers
  Copyright   : (c) Galois Inc, 2015-2020
  License     : BSD3
  Maintainer  : jhendrix@galois.com
  
  This defines a datatype for representing identifiers that can be
  used with Crucible.  These must start with an ASCII letter and can consist
  of any characters in the set @['a'-'z' 'A'-'Z' '0'-'9' '_']@ as long as the
  result is not an SMTLIB or Yices keyword.
  -}
  {-# LANGUAGE GeneralizedNewtypeDeriving #-}
  module What4.Symbol
    ( SolverSymbol
    , solverSymbolAsText
    , SolverSymbolError
    , emptySymbol
    , userSymbol
    , systemSymbol
    , safeSymbol
    , ppSolverSymbolError
    ) where
  
  import           Data.Char
  import           Data.Hashable
  import           Data.Set (Set)
  import qualified Data.Set as Set
  import           Data.String
  import           Data.Text (Text)
  import qualified Data.Text as Text
  
  import qualified Text.Encoding.Z as Z
  
  isAsciiLetter :: Char -> Bool
  isAsciiLetter c
    =  'A' <= c && c <= 'Z'
    || 'a' <= c && c <= 'z'
  
  isSymbolChar :: Char -> Bool
  isSymbolChar c
    = isAsciiLetter c
    || isDigit c
    || c == '_'
    || c == '\''
    || c == '!'
  
  -- | This describes why a given text value was not a valid solver symbol.
  data SolverSymbolError
     = SymbolEmpty
     | SymbolNoStartWithChar
     | SymbolIllegalChar
     | SymbolSMTLIBReserved
     | SymbolYicesReserved
  
  instance Show SolverSymbolError where
    show e = "Identifier " ++ ppSolverSymbolError e
  
  
  ppSolverSymbolError :: SolverSymbolError -> String
  ppSolverSymbolError e =
    case e of
      SymbolEmpty           -> "cannot be empty."
      SymbolNoStartWithChar -> "must start with a letter."
      SymbolIllegalChar     -> "contains an illegal character."
      SymbolSMTLIBReserved  -> "is an SMTLIB reserved word."
      SymbolYicesReserved   -> "is a Yices reserved word."
  
  
  -- | This represents a name known to the solver.
  --
  -- We have three types of symbols:
  --
  -- * The empty symbol
  --
  -- * A user symbol
  --
  -- * A system symbol
  --
  -- A user symbol should consist of a letter followed by any combination
  -- of letters, digits, and underscore characters.  It also cannot be a reserved
  -- word in Yices or SMTLIB.
  --
  -- A system symbol should start with a letter followed by any number of
  -- letter, digit, underscore or an exclamation mark characters.  It must
  -- contain at least one exclamation mark to distinguish itself from user
  -- symbols.
  newtype SolverSymbol = SolverSymbol { solverSymbolAsText :: Text }
    deriving (Eq, Ord, Hashable)
  
  -- | Return the empty symbol.
  emptySymbol :: SolverSymbol
  emptySymbol = SolverSymbol Text.empty
  
  -- | This returns either a user symbol or the empty symbol if the string is empty.
  userSymbol :: String -> Either SolverSymbolError SolverSymbol
  userSymbol s
    | elem '!' s = Left SymbolIllegalChar
    | otherwise = parseAnySymbol s
  
  systemSymbol :: String -> SolverSymbol
  systemSymbol s
      -- System symbols must contain an exclamation mark to distinguish them from
      -- user symbols (which are not allowed to have exclamation marks).
    | '!' `notElem` s =
      error $
        "The system symbol " ++ show s ++ " must contain at least one exclamation mark '!'"
    | otherwise =
      case parseAnySymbol s of
        Left e -> error ("Error parsing system symbol " ++ show s ++ ": " ++ ppSolverSymbolError e)
        Right r -> r
  
  
  -- | Attempts to create a user symbol from the given string.  If this fails
  --   for some reason, the string is Z-encoded into a system symbol instead
  --   with the prefix \"zenc!\".
  safeSymbol :: String -> SolverSymbol
  safeSymbol str =
    case userSymbol str of
      Right s -> s
      Left _err -> systemSymbol ("zenc!" ++ Z.zEncodeString str)
  
  instance Show SolverSymbol where
    show s = Text.unpack (solverSymbolAsText s)
  
  -- | This attempts to parse a string as a valid solver symbol.
  parseAnySymbol :: String -> Either SolverSymbolError SolverSymbol
  parseAnySymbol [] = Right emptySymbol
  parseAnySymbol (h:r)
    | isAsciiLetter h == False          = Left SymbolNoStartWithChar
    | all isSymbolChar r == False       = Left SymbolIllegalChar
    | t `Set.member` smtlibKeywordSet   = Left SymbolSMTLIBReserved
    | t `Set.member` yicesKeywordSet    = Left SymbolYicesReserved
    | otherwise = Right (SolverSymbol t)
    where t = if elem '\'' r
              then fromString ("|" ++ (h:r) ++ "|")
              else fromString (h:r)
  
  smtlibKeywordSet :: Set Text
  smtlibKeywordSet = Set.fromList (fromString <$> smtlibKeywords)
  
  yicesKeywordSet :: Set Text
  yicesKeywordSet = Set.fromList (fromString <$> yicesKeywords)
  
  -- | This is the list of keywords in SMTLIB 2.5
  smtlibKeywords :: [String]
  smtlibKeywords =
    [ "BINARY"
    , "DECIMAL"
    , "HEXADECIMAL"
    , "NUMERAL"
    , "STRING"
    , "as"
    , "let"
    , "exists"
    , "forall"
    , "par"
    , "assert"
    , "check-sat"
    , "check-sat-assuming"
    , "declare-const"
    , "declare-fun"
    , "declare-sort"
    , "define-fun"
    , "define-fun-rec"
    , "define-funs-rec"
    , "define-sort"
    , "echo"
    , "exit"
    , "get-assertions"
    , "get-assignment"
    , "get-info"
    , "get-model"
    , "get-option"
    , "get-proof"
    , "get-unsat-assumptions"
    , "get-unsat-core"
    , "get-value"
    , "pop"
    , "push"
    , "reset"
    , "reset-assertions"
    , "set-info"
    , "set-logic"
    , "set-option"
    ]
  
  yicesKeywords :: [String]
  yicesKeywords =
    [ "abs"
    , "and"
    , "assert"
    , "bit"
    , "bitvector"
    , "bool"
    , "bool-to-bv"
    , "bv-add"
    , "bv-and"
    , "bv-ashift-right"
    , "bv-ashr"
    , "bv-comp"
    , "bv-concat"
    , "bv-div"
    , "bv-extract"
    , "bv-ge"
    , "bv-gt"
    , "bv-le"
    , "bv-lshr"
    , "bv-lt"
    , "bv-mul"
    , "bv-nand"
    , "bv-neg"
    , "bv-nor"
    , "bv-not"
    , "bv-or"
    , "bv-pow"
    , "bv-redand"
    , "bv-redor"
    , "bv-rem"
    , "bv-repeat"
    , "bv-rotate-left"
    , "bv-rotate-right"
    , "bv-sdiv"
    , "bv-sge"
    , "bv-sgt"
    , "bv-shift-left0"
    , "bv-shift-left1"
    , "bv-shift-right0"
    , "bv-shift-right1"
    , "bv-shl"
    , "bv-sign-extend"
    , "bv-sle"
    , "bv-slt"
    , "bv-smod"
    , "bv-srem"
    , "bv-sub"
    , "bv-xnor"
    , "bv-xor"
    , "bv-zero-extend"
    , "ceil"
    , "check"
    , "define"
    , "define-type"
    , "distinct"
    , "div"
    , "divides"
    , "dump-context"
    , "echo"
    , "ef-solve"
    , "eval"
    , "exists"
    , "exit"
    , "export-to-dimacs"
    , "false"
    , "floor"
    , "forall"
    , "help"
    , "if"
    , "include"
    , "int"
    , "is-int"
    , "ite"
    , "lambda"
    , "let"
    , "mk-bv"
    , "mk-tuple"
    , "mod"
    , "not"
    , "or"
    , "pop"
    , "push"
    , "real"
    , "reset"
    , "reset-stats"
    , "scalar"
    , "select"
    , "set-param"
    , "set-timeout"
    , "show-implicant"
    , "show-model"
    , "show-param"
    , "show-params"
    , "show-stats"
    , "true"
    , "tuple"
    , "tuple-update"
    , "update"
    , "xor"
    ]
  