{-|
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
/= :: SolverSymbol -> SolverSymbol -> Bool
$c/= :: SolverSymbol -> SolverSymbol -> Bool
== :: SolverSymbol -> SolverSymbol -> Bool
$c== :: 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
min :: SolverSymbol -> SolverSymbol -> SolverSymbol
$cmin :: SolverSymbol -> SolverSymbol -> SolverSymbol
max :: SolverSymbol -> SolverSymbol -> SolverSymbol
$cmax :: SolverSymbol -> SolverSymbol -> SolverSymbol
>= :: SolverSymbol -> SolverSymbol -> Bool
$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
compare :: SolverSymbol -> SolverSymbol -> Ordering
$ccompare :: SolverSymbol -> SolverSymbol -> Ordering
$cp1Ord :: Eq SolverSymbol
Ord, Int -> SolverSymbol -> Int
SolverSymbol -> Int
(Int -> SolverSymbol -> Int)
-> (SolverSymbol -> Int) -> Hashable SolverSymbol
forall a. (Int -> a -> Int) -> (a -> Int) -> Hashable a
hash :: SolverSymbol -> Int
$chash :: SolverSymbol -> Int
hashWithSalt :: Int -> SolverSymbol -> Int
$chashWithSalt :: Int -> 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 (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 (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"
  ]