{-# LANGUAGE DerivingStrategies        #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE GADTs                     #-}
{-# LANGUAGE OverloadedStrings         #-}
{-# LANGUAGE TypeOperators             #-}
{-# LANGUAGE UndecidableInstances      #-}


module ZkFold.Symbolic.Compiler.ArithmeticCircuit.Lookup where

import           Control.DeepSeq
import           Data.Aeson.Types
import           Data.ByteString  (ByteString)
import           Data.Set
import qualified Data.Text        as T
import           Data.Typeable
import           GHC.Base
import           GHC.Generics     (Generic, Par1, (:*:))
import           Prelude          (Show)


data LookupType a = forall f. (Functor f, Typeable f) => LookupType { ()
lTable :: LookupTable a f }

deriving instance (Show a) => Show (LookupType a)

tryEq :: (Typeable f, Typeable g) => LookupTable a f -> LookupTable a g -> Bool
tryEq :: forall (f :: Type -> Type) (g :: Type -> Type) a.
(Typeable f, Typeable g) =>
LookupTable a f -> LookupTable a g -> Bool
tryEq LookupTable a f
a LookupTable a g
b = LookupTable a f -> TypeRep
forall {k} (proxy :: k -> Type) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep LookupTable a f
a TypeRep -> TypeRep -> Bool
forall a. Eq a => a -> a -> Bool
== LookupTable a g -> TypeRep
forall {k} (proxy :: k -> Type) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep LookupTable a g
b

instance Eq a => Eq (LookupType a) where
  (==) :: LookupType a -> LookupType a -> Bool
  == :: LookupType a -> LookupType a -> Bool
(==) (LookupType LookupTable a f
lt1) (LookupType LookupTable a f
lt2) = LookupTable a f -> LookupTable a f -> Bool
forall (f :: Type -> Type) (g :: Type -> Type) a.
(Typeable f, Typeable g) =>
LookupTable a f -> LookupTable a g -> Bool
tryEq LookupTable a f
lt1 LookupTable a f
lt2

tryCompare :: (Typeable f, Typeable g) => LookupTable a f -> LookupTable a g -> Ordering
tryCompare :: forall (f :: Type -> Type) (g :: Type -> Type) a.
(Typeable f, Typeable g) =>
LookupTable a f -> LookupTable a g -> Ordering
tryCompare LookupTable a f
a LookupTable a g
b = TypeRep -> TypeRep -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (LookupTable a f -> TypeRep
forall {k} (proxy :: k -> Type) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep LookupTable a f
a) (LookupTable a g -> TypeRep
forall {k} (proxy :: k -> Type) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep LookupTable a g
b)-- then compare a (fromJust (cast b)) else EQ

instance Ord a => Ord (LookupType a) where
  compare :: LookupType a -> LookupType a -> Ordering
  compare :: LookupType a -> LookupType a -> Ordering
compare (LookupType LookupTable a f
lt1) (LookupType LookupTable a f
lt2) = LookupTable a f -> LookupTable a f -> Ordering
forall (f :: Type -> Type) (g :: Type -> Type) a.
(Typeable f, Typeable g) =>
LookupTable a f -> LookupTable a g -> Ordering
tryCompare LookupTable a f
lt1 LookupTable a f
lt2

instance (ToJSON a) => ToJSON (LookupType a) where
  toJSON :: LookupType a -> Value
toJSON (LookupType LookupTable a f
lt) = LookupTable a f -> Value
forall a. ToJSON a => a -> Value
toJSON LookupTable a f
lt
instance (ToJSON a) => ToJSONKey (LookupType a)

instance (FromJSON a) => FromJSON (LookupType a) where
  parseJSON :: Value -> Parser (LookupType a)
parseJSON (Object Object
v) = Object
v Object -> Key -> Parser (LookupType a)
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"lookupType"
  parseJSON Value
invalid    =
    String -> Parser (LookupType a) -> Parser (LookupType a)
forall a. String -> Parser a -> Parser a
prependFailure String
"parsing LookupType failed, "
        (String -> Value -> Parser (LookupType a)
forall a. String -> Value -> Parser a
typeMismatch String
"Object" Value
invalid)
instance (FromJSONKey a, FromJSON a) => FromJSONKey (LookupType a)


-- | @LookupTable a f@ is a type of compact lookup table descriptions using ideas from relational algebra.
-- @a@ is a base field type, @f@ is a functor such that @f a@ is a type whose subset this lookup table describes.
data LookupTable a f where
  -- | @Ranges@ describes a set of disjoint intervals on the base field.
  Ranges :: Set (a, a) -> LookupTable a Par1
  -- | @Product t u@ is a cartesian product of tables @t@ and @u@.
  Product :: LookupTable a f -> LookupTable a g -> LookupTable a (f :*: g)
  -- | @Plot f x@ is a plot of a function @f@ with @x@ as a domain.
  Plot :: FunctionId (f a -> g a) -> LookupTable a f -> LookupTable a (f :*: g)


newtype FunctionId f = FunctionId { forall {k} (f :: k). FunctionId f -> ByteString
funcHash :: ByteString }
  deriving (FunctionId f -> FunctionId f -> Bool
(FunctionId f -> FunctionId f -> Bool)
-> (FunctionId f -> FunctionId f -> Bool) -> Eq (FunctionId f)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall k (f :: k). FunctionId f -> FunctionId f -> Bool
$c== :: forall k (f :: k). FunctionId f -> FunctionId f -> Bool
== :: FunctionId f -> FunctionId f -> Bool
$c/= :: forall k (f :: k). FunctionId f -> FunctionId f -> Bool
/= :: FunctionId f -> FunctionId f -> Bool
Eq, Eq (FunctionId f)
Eq (FunctionId f) =>
(FunctionId f -> FunctionId f -> Ordering)
-> (FunctionId f -> FunctionId f -> Bool)
-> (FunctionId f -> FunctionId f -> Bool)
-> (FunctionId f -> FunctionId f -> Bool)
-> (FunctionId f -> FunctionId f -> Bool)
-> (FunctionId f -> FunctionId f -> FunctionId f)
-> (FunctionId f -> FunctionId f -> FunctionId f)
-> Ord (FunctionId f)
FunctionId f -> FunctionId f -> Bool
FunctionId f -> FunctionId f -> Ordering
FunctionId f -> FunctionId f -> FunctionId f
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
forall k (f :: k). Eq (FunctionId f)
forall k (f :: k). FunctionId f -> FunctionId f -> Bool
forall k (f :: k). FunctionId f -> FunctionId f -> Ordering
forall k (f :: k). FunctionId f -> FunctionId f -> FunctionId f
$ccompare :: forall k (f :: k). FunctionId f -> FunctionId f -> Ordering
compare :: FunctionId f -> FunctionId f -> Ordering
$c< :: forall k (f :: k). FunctionId f -> FunctionId f -> Bool
< :: FunctionId f -> FunctionId f -> Bool
$c<= :: forall k (f :: k). FunctionId f -> FunctionId f -> Bool
<= :: FunctionId f -> FunctionId f -> Bool
$c> :: forall k (f :: k). FunctionId f -> FunctionId f -> Bool
> :: FunctionId f -> FunctionId f -> Bool
$c>= :: forall k (f :: k). FunctionId f -> FunctionId f -> Bool
>= :: FunctionId f -> FunctionId f -> Bool
$cmax :: forall k (f :: k). FunctionId f -> FunctionId f -> FunctionId f
max :: FunctionId f -> FunctionId f -> FunctionId f
$cmin :: forall k (f :: k). FunctionId f -> FunctionId f -> FunctionId f
min :: FunctionId f -> FunctionId f -> FunctionId f
Ord, Int -> FunctionId f -> ShowS
[FunctionId f] -> ShowS
FunctionId f -> String
(Int -> FunctionId f -> ShowS)
-> (FunctionId f -> String)
-> ([FunctionId f] -> ShowS)
-> Show (FunctionId f)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (f :: k). Int -> FunctionId f -> ShowS
forall k (f :: k). [FunctionId f] -> ShowS
forall k (f :: k). FunctionId f -> String
$cshowsPrec :: forall k (f :: k). Int -> FunctionId f -> ShowS
showsPrec :: Int -> FunctionId f -> ShowS
$cshow :: forall k (f :: k). FunctionId f -> String
show :: FunctionId f -> String
$cshowList :: forall k (f :: k). [FunctionId f] -> ShowS
showList :: [FunctionId f] -> ShowS
Show, (forall x. FunctionId f -> Rep (FunctionId f) x)
-> (forall x. Rep (FunctionId f) x -> FunctionId f)
-> Generic (FunctionId f)
forall x. Rep (FunctionId f) x -> FunctionId f
forall x. FunctionId f -> Rep (FunctionId f) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall k (f :: k) x. Rep (FunctionId f) x -> FunctionId f
forall k (f :: k) x. FunctionId f -> Rep (FunctionId f) x
$cfrom :: forall k (f :: k) x. FunctionId f -> Rep (FunctionId f) x
from :: forall x. FunctionId f -> Rep (FunctionId f) x
$cto :: forall k (f :: k) x. Rep (FunctionId f) x -> FunctionId f
to :: forall x. Rep (FunctionId f) x -> FunctionId f
Generic)

deriving instance (Eq a) => Eq (LookupTable a f)
deriving instance (Ord a) => Ord (LookupTable a f)
deriving instance (Show a) => Show (LookupTable a f)

instance (ToJSON a) => ToJSON (LookupTable a f) where
  toJSON :: LookupTable a f -> Value
toJSON (Ranges Set (a, a)
p)    = Set (a, a) -> Value
forall a. ToJSON a => a -> Value
toJSON Set (a, a)
p
  toJSON (Product LookupTable a f
_ LookupTable a g
_) = Text -> Value
String (Text -> Value) -> (String -> Text) -> String -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Text
T.pack (String -> Value) -> String -> Value
forall a b. (a -> b) -> a -> b
$ String
"Product"
  toJSON (Plot FunctionId (f a -> g a)
_ LookupTable a f
_)    = Text -> Value
String (Text -> Value) -> (String -> Text) -> String -> Value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Text
T.pack (String -> Value) -> String -> Value
forall a b. (a -> b) -> a -> b
$ String
"Plot"

instance (ToJSON a) => ToJSONKey (LookupTable a f)
instance (FromJSON a) => FromJSON (LookupTable a f) where
  parseJSON :: Value -> Parser (LookupTable a f)
parseJSON = Value -> Parser (LookupTable a f)
forall a. HasCallStack => a
undefined

instance (FromJSON a) => FromJSONKey (LookupTable a f)

instance NFData (LookupType a) where
  rnf :: LookupType a -> ()
rnf = LookupType a -> ()
forall a. a -> ()
rwhnf

isRange :: LookupType a -> Bool
isRange :: forall a. LookupType a -> Bool
isRange (LookupType LookupTable a f
l) = case LookupTable a f
l of
  Ranges Set (a, a)
_ -> Bool
True
  LookupTable a f
_        -> Bool
False

fromRange :: LookupType a -> Set (a, a)
fromRange :: forall a. LookupType a -> Set (a, a)
fromRange (LookupType (Ranges Set (a, a)
a)) = Set (a, a)
a
fromRange LookupType a
_                       = String -> Set (a, a)
forall a. HasCallStack => String -> a
error String
"it's not Range lookup"