{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}

module Language.REST.Op where

import Data.Text as T
import Data.Hashable
import Data.String
import GHC.Generics (Generic)
import Language.REST.SMT

-- | The operators used in 'RuntimeTerm' and 'MetaTerm'
newtype Op = Op Text deriving (Op -> Op -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Op -> Op -> Bool
$c/= :: Op -> Op -> Bool
== :: Op -> Op -> Bool
$c== :: Op -> Op -> Bool
Eq, Eq Op
Op -> Op -> Bool
Op -> Op -> Ordering
Op -> Op -> Op
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 :: Op -> Op -> Op
$cmin :: Op -> Op -> Op
max :: Op -> Op -> Op
$cmax :: Op -> Op -> Op
>= :: Op -> Op -> Bool
$c>= :: Op -> Op -> Bool
> :: Op -> Op -> Bool
$c> :: Op -> Op -> Bool
<= :: Op -> Op -> Bool
$c<= :: Op -> Op -> Bool
< :: Op -> Op -> Bool
$c< :: Op -> Op -> Bool
compare :: Op -> Op -> Ordering
$ccompare :: Op -> Op -> Ordering
Ord, Eq Op
Int -> Op -> Int
Op -> Int
forall a. Eq a -> (Int -> a -> Int) -> (a -> Int) -> Hashable a
hash :: Op -> Int
$chash :: Op -> Int
hashWithSalt :: Int -> Op -> Int
$chashWithSalt :: Int -> Op -> Int
Hashable, forall x. Rep Op x -> Op
forall x. Op -> Rep Op x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Op x -> Op
$cfrom :: forall x. Op -> Rep Op x
Generic)

instance Show Op where
  show :: Op -> String
show (Op Text
o) = Text -> String
unpack Text
o

instance IsString Op where
  fromString :: String -> Op
fromString = Text -> Op
Op forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Text
pack

instance ToSMTVar Op Int where
  toSMTVar :: Op -> SMTVar Int
toSMTVar (Op Text
"ite") = forall a. Text -> SMTVar a
SMTVar Text
"_ite_"
  toSMTVar (Op Text
op) = forall a. Text -> SMTVar a
SMTVar forall a b. (a -> b) -> a -> b
$ Text -> Text -> Text
T.append Text
"op_" forall a b. (a -> b) -> a -> b
$ (Char -> Text) -> Text -> Text
T.concatMap Char -> Text
go Text
op
    where
        go :: Char -> Text
go Char
'∅'  = Text
"_empty_"
        go Char
'₀'  = Text
"0"
        go Char
'₁'  = Text
"1"
        go Char
'$'  = Text
"_dollar_"
        go Char
'['  = Text
"_lb_"
        go Char
']'  = Text
"_rb_"
        go Char
':'  = Text
"_colon_"
        go Char
'.'  = Text
"_dot_"
        go Char
'#'  = Text
"_pound_"
        go Char
'\'' = Text
"_comma_"
        go Char
'/'  = Text
"_slash_"
        go Char
' '  = Text
"_space_"
        go Char
'∪'  = Text
"_cup_"
        go Char
'\\' = Text
"_bslash_"
        go Char
'(' = Text
"_lp_"
        go Char
')' = Text
"_rp_"
        go Char
c    = Char -> Text
singleton Char
c