    {-|
    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 :: Char -> Bool
    isAsciiLetter Char
    c
      =  Char
    'A' Char -> Char -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Char
    c Bool -> Bool -> Bool
    && Char
    c Char -> Char -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Char
    'Z'
      Bool -> Bool -> Bool
    || Char
    'a' Char -> Char -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Char
    c Bool -> Bool -> Bool
    && Char
    c Char -> Char -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Char
    'z'

    isSymbolChar :: Char -> Bool
    isSymbolChar :: Char -> Bool
    isSymbolChar Char
    c
      = Char -> Bool
    isAsciiLetter Char
    c
      Bool -> Bool -> Bool
    || Char -> Bool
    isDigit Char
    c
      Bool -> Bool -> Bool
    || Char
    c Char -> Char -> Bool
    forall a. Eq a => a -> a -> Bool
    == Char
    '_'
      Bool -> Bool -> Bool
    || Char
    c Char -> Char -> Bool
    forall a. Eq a => a -> a -> Bool
    == Char
    '\''
      Bool -> Bool -> Bool
    || Char
    c Char -> Char -> Bool
    forall a. Eq a => a -> a -> Bool
    == Char
    '!'

    -- | 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 :: SolverSymbolError -> String
    show SolverSymbolError
    e = String
    "Identifier " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ SolverSymbolError -> String
    ppSolverSymbolError SolverSymbolError
    e

    ppSolverSymbolError :: SolverSymbolError -> String
    ppSolverSymbolError :: SolverSymbolError -> String
    ppSolverSymbolError SolverSymbolError
    e =
      case SolverSymbolError
    e of
        SolverSymbolError
    SymbolEmpty           -> String
    "cannot be empty."
        SolverSymbolError
    SymbolNoStartWithChar -> String
    "must start with a letter."
        SolverSymbolError
    SymbolIllegalChar     -> String
    "contains an illegal character."
        SolverSymbolError
    SymbolSMTLIBReserved  -> String
    "is an SMTLIB reserved word."
        SolverSymbolError
    SymbolYicesReserved   -> String
    "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 { SolverSymbol -> Text
    solverSymbolAsText :: Text }
      deriving (SolverSymbol -> SolverSymbol -> Bool
    (SolverSymbol -> SolverSymbol -> Bool)
    -> (SolverSymbol -> SolverSymbol -> Bool) -> Eq SolverSymbol
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: SolverSymbol -> SolverSymbol -> Bool
    == :: SolverSymbol -> SolverSymbol -> Bool
    $c/= :: SolverSymbol -> SolverSymbol -> Bool
    /= :: SolverSymbol -> SolverSymbol -> Bool
    Eq, Eq SolverSymbol
    Eq SolverSymbol =>
    (SolverSymbol -> SolverSymbol -> Ordering)
    -> (SolverSymbol -> SolverSymbol -> Bool)
    -> (SolverSymbol -> SolverSymbol -> Bool)
    -> (SolverSymbol -> SolverSymbol -> Bool)
    -> (SolverSymbol -> SolverSymbol -> Bool)
    -> (SolverSymbol -> SolverSymbol -> SolverSymbol)
    -> (SolverSymbol -> SolverSymbol -> SolverSymbol)
    -> Ord SolverSymbol
    SolverSymbol -> SolverSymbol -> Bool
    SolverSymbol -> SolverSymbol -> Ordering
    SolverSymbol -> SolverSymbol -> SolverSymbol
    forall a.
    Eq a =>
    (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    $ccompare :: SolverSymbol -> SolverSymbol -> Ordering
    compare :: SolverSymbol -> SolverSymbol -> Ordering
    $c< :: SolverSymbol -> SolverSymbol -> Bool
    < :: SolverSymbol -> SolverSymbol -> Bool
    $c<= :: SolverSymbol -> SolverSymbol -> Bool
    <= :: SolverSymbol -> SolverSymbol -> Bool
    $c> :: SolverSymbol -> SolverSymbol -> Bool
    > :: SolverSymbol -> SolverSymbol -> Bool
    $c>= :: SolverSymbol -> SolverSymbol -> Bool
    >= :: SolverSymbol -> SolverSymbol -> Bool
    $cmax :: SolverSymbol -> SolverSymbol -> SolverSymbol
    max :: SolverSymbol -> SolverSymbol -> SolverSymbol
    $cmin :: SolverSymbol -> SolverSymbol -> SolverSymbol
    min :: SolverSymbol -> SolverSymbol -> SolverSymbol
    Ord, Eq SolverSymbol
    Eq SolverSymbol =>
    (Int -> SolverSymbol -> Int)
    -> (SolverSymbol -> Int) -> Hashable SolverSymbol
    Int -> SolverSymbol -> Int
    SolverSymbol -> Int
    forall a. Eq a => (Int -> a -> Int) -> (a -> Int) -> Hashable a
    $chashWithSalt :: Int -> SolverSymbol -> Int
    hashWithSalt :: Int -> SolverSymbol -> Int
    $chash :: SolverSymbol -> Int
    hash :: SolverSymbol -> Int
    Hashable)

    -- | Return the empty symbol.
    emptySymbol :: SolverSymbol
    emptySymbol :: SolverSymbol
    emptySymbol = Text -> SolverSymbol
    SolverSymbol Text
    Text.empty

    -- | This returns either a user symbol or the empty symbol if the string is empty.
    userSymbol :: String -> Either SolverSymbolError SolverSymbol
    userSymbol :: String -> Either SolverSymbolError SolverSymbol
    userSymbol String
    s
      | Char -> String -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: Type -> Type) a.
    (Foldable t, Eq a) =>
    a -> t a -> Bool
    elem Char
    '!' String
    s = SolverSymbolError -> Either SolverSymbolError SolverSymbol
    forall a b. a -> Either a b
    Left SolverSymbolError
    SymbolIllegalChar
      | Bool
    otherwise = String -> Either SolverSymbolError SolverSymbol
    parseAnySymbol String
    s

    systemSymbol :: String -> SolverSymbol
    systemSymbol :: String -> SolverSymbol
    systemSymbol String
    s
        -- System symbols must contain an exclamation mark to distinguish them from
        -- user symbols (which are not allowed to have exclamation marks).
      | Char
    '!' Char -> String -> Bool
    forall (t :: Type -> Type) a.
    (Foldable t, Eq a) =>
    a -> t a -> Bool
    `notElem` String
    s =
        String -> SolverSymbol
    forall a. HasCallStack => String -> a
    error (String -> SolverSymbol) -> String -> SolverSymbol
    forall a b. (a -> b) -> a -> b
    $
          String
    "The system symbol " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ShowS
    forall a. Show a => a -> String
    show String
    s String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    " must contain at least one exclamation mark '!'"
      | Bool
    otherwise =
        case String -> Either SolverSymbolError SolverSymbol
    parseAnySymbol String
    s of
          Left SolverSymbolError
    e -> String -> SolverSymbol
    forall a. HasCallStack => String -> a
    error (String
    "Error parsing system symbol " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ShowS
    forall a. Show a => a -> String
    show String
    s String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    ": " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ SolverSymbolError -> String
    ppSolverSymbolError SolverSymbolError
    e)
          Right SolverSymbol
    r -> SolverSymbol
    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 :: String -> SolverSymbol
    safeSymbol String
    str =
      case String -> Either SolverSymbolError SolverSymbol
    userSymbol String
    str of
        Right SolverSymbol
    s -> SolverSymbol
    s
        Left SolverSymbolError
    _err -> String -> SolverSymbol
    systemSymbol (String
    "zenc!" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ShowS
    Z.zEncodeString String
    str)

    instance Show SolverSymbol where
      show :: SolverSymbol -> String
    show SolverSymbol
    s = Text -> String
    Text.unpack (SolverSymbol -> Text
    solverSymbolAsText SolverSymbol
    s)

    -- | This attempts to parse a string as a valid solver symbol.
    parseAnySymbol :: String -> Either SolverSymbolError SolverSymbol
    parseAnySymbol :: String -> Either SolverSymbolError SolverSymbol
    parseAnySymbol [] = SolverSymbol -> Either SolverSymbolError SolverSymbol
    forall a b. b -> Either a b
    Right SolverSymbol
    emptySymbol
    parseAnySymbol (Char
    h:String
    r)
      | Char -> Bool
    isAsciiLetter Char
    h Bool -> Bool -> Bool
    forall a. Eq a => a -> a -> Bool
    == Bool
    False          = SolverSymbolError -> Either SolverSymbolError SolverSymbol
    forall a b. a -> Either a b
    Left SolverSymbolError
    SymbolNoStartWithChar
      | (Char -> Bool) -> String -> Bool
    forall (t :: Type -> Type) a.
    Foldable t =>
    (a -> Bool) -> t a -> Bool
    all Char -> Bool
    isSymbolChar String
    r Bool -> Bool -> Bool
    forall a. Eq a => a -> a -> Bool
    == Bool
    False       = SolverSymbolError -> Either SolverSymbolError SolverSymbol
    forall a b. a -> Either a b
    Left SolverSymbolError
    SymbolIllegalChar
      | Text
    t Text -> Set Text -> Bool
    forall a. Ord a => a -> Set a -> Bool
    `Set.member` Set Text
    smtlibKeywordSet   = SolverSymbolError -> Either SolverSymbolError SolverSymbol
    forall a b. a -> Either a b
    Left SolverSymbolError
    SymbolSMTLIBReserved
      | Text
    t Text -> Set Text -> Bool
    forall a. Ord a => a -> Set a -> Bool
    `Set.member` Set Text
    yicesKeywordSet    = SolverSymbolError -> Either SolverSymbolError SolverSymbol
    forall a b. a -> Either a b
    Left SolverSymbolError
    SymbolYicesReserved
      | Bool
    otherwise = SolverSymbol -> Either SolverSymbolError SolverSymbol
    forall a b. b -> Either a b
    Right (Text -> SolverSymbol
    SolverSymbol Text
    t)
      where t :: Text
    t = if Char -> String -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: Type -> Type) a.
    (Foldable t, Eq a) =>
    a -> t a -> Bool
    elem Char
    '\'' String
    r
                then String -> Text
    forall a. IsString a => String -> a
    fromString (String
    "|" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ (Char
    hChar -> ShowS
    forall a. a -> [a] -> [a]
    :String
    r) String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    "|")
                else String -> Text
    forall a. IsString a => String -> a
    fromString (Char
    hChar -> ShowS
    forall a. a -> [a] -> [a]
    :String
    r)

    smtlibKeywordSet :: Set Text
    smtlibKeywordSet :: Set Text
    smtlibKeywordSet = [Text] -> Set Text
    forall a. Ord a => [a] -> Set a
    Set.fromList (String -> Text
    forall a. IsString a => String -> a
    fromString (String -> Text) -> [String] -> [Text]
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> [String]
    smtlibKeywords)

    yicesKeywordSet :: Set Text
    yicesKeywordSet :: Set Text
    yicesKeywordSet = [Text] -> Set Text
    forall a. Ord a => [a] -> Set a
    Set.fromList (String -> Text
    forall a. IsString a => String -> a
    fromString (String -> Text) -> [String] -> [Text]
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    <$> [String]
    yicesKeywords)

    -- | This is the list of keywords in SMTLIB 2.5
    smtlibKeywords :: [String]
    smtlibKeywords :: [String]
    smtlibKeywords =
      [ String
    "BINARY"
      , String
    "DECIMAL"
      , String
    "HEXADECIMAL"
      , String
    "NUMERAL"
      , String
    "STRING"
      , String
    "as"
      , String
    "let"
      , String
    "exists"
      , String
    "forall"
      , String
    "par"
      , String
    "assert"
      , String
    "check-sat"
      , String
    "check-sat-assuming"
      , String
    "declare-const"
      , String
    "declare-fun"
      , String
    "declare-sort"
      , String
    "define-fun"
      , String
    "define-fun-rec"
      , String
    "define-funs-rec"
      , String
    "define-sort"
      , String
    "echo"
      , String
    "exit"
      , String
    "get-assertions"
      , String
    "get-assignment"
      , String
    "get-info"
      , String
    "get-model"
      , String
    "get-option"
      , String
    "get-proof"
      , String
    "get-unsat-assumptions"
      , String
    "get-unsat-core"
      , String
    "get-value"
      , String
    "pop"
      , String
    "push"
      , String
    "reset"
      , String
    "reset-assertions"
      , String
    "set-info"
      , String
    "set-logic"
      , String
    "set-option"
      ]

    yicesKeywords :: [String]
    yicesKeywords :: [String]
    yicesKeywords =
      [ String
    "abs"
      , String
    "and"
      , String
    "assert"
      , String
    "bit"
      , String
    "bitvector"
      , String
    "bool"
      , String
    "bool-to-bv"
      , String
    "bv-add"
      , String
    "bv-and"
      , String
    "bv-ashift-right"
      , String
    "bv-ashr"
      , String
    "bv-comp"
      , String
    "bv-concat"
      , String
    "bv-div"
      , String
    "bv-extract"
      , String
    "bv-ge"
      , String
    "bv-gt"
      , String
    "bv-le"
      , String
    "bv-lshr"
      , String
    "bv-lt"
      , String
    "bv-mul"
      , String
    "bv-nand"
      , String
    "bv-neg"
      , String
    "bv-nor"
      , String
    "bv-not"
      , String
    "bv-or"
      , String
    "bv-pow"
      , String
    "bv-redand"
      , String
    "bv-redor"
      , String
    "bv-rem"
      , String
    "bv-repeat"
      , String
    "bv-rotate-left"
      , String
    "bv-rotate-right"
      , String
    "bv-sdiv"
      , String
    "bv-sge"
      , String
    "bv-sgt"
      , String
    "bv-shift-left0"
      , String
    "bv-shift-left1"
      , String
    "bv-shift-right0"
      , String
    "bv-shift-right1"
      , String
    "bv-shl"
      , String
    "bv-sign-extend"
      , String
    "bv-sle"
      , String
    "bv-slt"
      , String
    "bv-smod"
      , String
    "bv-srem"
      , String
    "bv-sub"
      , String
    "bv-xnor"
      , String
    "bv-xor"
      , String
    "bv-zero-extend"
      , String
    "ceil"
      , String
    "check"
      , String
    "define"
      , String
    "define-type"
      , String
    "distinct"
      , String
    "div"
      , String
    "divides"
      , String
    "dump-context"
      , String
    "echo"
      , String
    "ef-solve"
      , String
    "eval"
      , String
    "exists"
      , String
    "exit"
      , String
    "export-to-dimacs"
      , String
    "false"
      , String
    "floor"
      , String
    "forall"
      , String
    "help"
      , String
    "if"
      , String
    "include"
      , String
    "int"
      , String
    "is-int"
      , String
    "ite"
      , String
    "lambda"
      , String
    "let"
      , String
    "mk-bv"
      , String
    "mk-tuple"
      , String
    "mod"
      , String
    "not"
      , String
    "or"
      , String
    "pop"
      , String
    "push"
      , String
    "real"
      , String
    "reset"
      , String
    "reset-stats"
      , String
    "scalar"
      , String
    "select"
      , String
    "set-param"
      , String
    "set-timeout"
      , String
    "show-implicant"
      , String
    "show-model"
      , String
    "show-param"
      , String
    "show-params"
      , String
    "show-stats"
      , String
    "true"
      , String
    "tuple"
      , String
    "tuple-update"
      , String
    "update"
      , String
    "xor"
      ]