{-# LANGUAGE DerivingVia          #-}
{-# LANGUAGE UndecidableInstances #-}

{-# OPTIONS_GHC -Wno-orphans #-}

module ZkFold.Symbolic.Interpreter (Interpreter (..)) where

import           Control.Applicative              (Applicative)
import           Control.DeepSeq                  (NFData)
import           Control.Monad                    (Monad, return)
import           Data.Aeson                       (FromJSON, ToJSON)
import           Data.Eq                          (Eq)
import           Data.Function                    (id, ($))
import           Data.Functor                     (Functor, (<$>))
import           Data.Functor.Identity            (Identity (..))
import           GHC.Generics                     (Generic)
import           Text.Show                        (Show)

import           ZkFold.Base.Control.HApplicative
import           ZkFold.Base.Data.HFunctor
import           ZkFold.Base.Data.Package
import           ZkFold.Symbolic.Class
import           ZkFold.Symbolic.MonadCircuit

newtype Interpreter a f = Interpreter { forall {k} (a :: k) (f :: k -> Type). Interpreter a f -> f a
runInterpreter :: f a }
    deriving (Interpreter a f -> Interpreter a f -> Bool
(Interpreter a f -> Interpreter a f -> Bool)
-> (Interpreter a f -> Interpreter a f -> Bool)
-> Eq (Interpreter a f)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall k (a :: k) (f :: k -> Type).
Eq (f a) =>
Interpreter a f -> Interpreter a f -> Bool
$c== :: forall k (a :: k) (f :: k -> Type).
Eq (f a) =>
Interpreter a f -> Interpreter a f -> Bool
== :: Interpreter a f -> Interpreter a f -> Bool
$c/= :: forall k (a :: k) (f :: k -> Type).
Eq (f a) =>
Interpreter a f -> Interpreter a f -> Bool
/= :: Interpreter a f -> Interpreter a f -> Bool
Eq, Int -> Interpreter a f -> ShowS
[Interpreter a f] -> ShowS
Interpreter a f -> String
(Int -> Interpreter a f -> ShowS)
-> (Interpreter a f -> String)
-> ([Interpreter a f] -> ShowS)
-> Show (Interpreter a f)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (a :: k) (f :: k -> Type).
Show (f a) =>
Int -> Interpreter a f -> ShowS
forall k (a :: k) (f :: k -> Type).
Show (f a) =>
[Interpreter a f] -> ShowS
forall k (a :: k) (f :: k -> Type).
Show (f a) =>
Interpreter a f -> String
$cshowsPrec :: forall k (a :: k) (f :: k -> Type).
Show (f a) =>
Int -> Interpreter a f -> ShowS
showsPrec :: Int -> Interpreter a f -> ShowS
$cshow :: forall k (a :: k) (f :: k -> Type).
Show (f a) =>
Interpreter a f -> String
show :: Interpreter a f -> String
$cshowList :: forall k (a :: k) (f :: k -> Type).
Show (f a) =>
[Interpreter a f] -> ShowS
showList :: [Interpreter a f] -> ShowS
Show, (forall x. Interpreter a f -> Rep (Interpreter a f) x)
-> (forall x. Rep (Interpreter a f) x -> Interpreter a f)
-> Generic (Interpreter a f)
forall x. Rep (Interpreter a f) x -> Interpreter a f
forall x. Interpreter a f -> Rep (Interpreter a f) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall k (a :: k) (f :: k -> Type) x.
Rep (Interpreter a f) x -> Interpreter a f
forall k (a :: k) (f :: k -> Type) x.
Interpreter a f -> Rep (Interpreter a f) x
$cfrom :: forall k (a :: k) (f :: k -> Type) x.
Interpreter a f -> Rep (Interpreter a f) x
from :: forall x. Interpreter a f -> Rep (Interpreter a f) x
$cto :: forall k (a :: k) (f :: k -> Type) x.
Rep (Interpreter a f) x -> Interpreter a f
to :: forall x. Rep (Interpreter a f) x -> Interpreter a f
Generic, Interpreter a f -> ()
(Interpreter a f -> ()) -> NFData (Interpreter a f)
forall a. (a -> ()) -> NFData a
forall k (a :: k) (f :: k -> Type).
NFData (f a) =>
Interpreter a f -> ()
$crnf :: forall k (a :: k) (f :: k -> Type).
NFData (f a) =>
Interpreter a f -> ()
rnf :: Interpreter a f -> ()
NFData)
    deriving newtype (Value -> Parser [Interpreter a f]
Value -> Parser (Interpreter a f)
(Value -> Parser (Interpreter a f))
-> (Value -> Parser [Interpreter a f])
-> FromJSON (Interpreter a f)
forall a.
(Value -> Parser a) -> (Value -> Parser [a]) -> FromJSON a
forall k (a :: k) (f :: k -> Type).
FromJSON (f a) =>
Value -> Parser [Interpreter a f]
forall k (a :: k) (f :: k -> Type).
FromJSON (f a) =>
Value -> Parser (Interpreter a f)
$cparseJSON :: forall k (a :: k) (f :: k -> Type).
FromJSON (f a) =>
Value -> Parser (Interpreter a f)
parseJSON :: Value -> Parser (Interpreter a f)
$cparseJSONList :: forall k (a :: k) (f :: k -> Type).
FromJSON (f a) =>
Value -> Parser [Interpreter a f]
parseJSONList :: Value -> Parser [Interpreter a f]
FromJSON, [Interpreter a f] -> Value
[Interpreter a f] -> Encoding
Interpreter a f -> Value
Interpreter a f -> Encoding
(Interpreter a f -> Value)
-> (Interpreter a f -> Encoding)
-> ([Interpreter a f] -> Value)
-> ([Interpreter a f] -> Encoding)
-> ToJSON (Interpreter a f)
forall a.
(a -> Value)
-> (a -> Encoding)
-> ([a] -> Value)
-> ([a] -> Encoding)
-> ToJSON a
forall k (a :: k) (f :: k -> Type).
ToJSON (f a) =>
[Interpreter a f] -> Value
forall k (a :: k) (f :: k -> Type).
ToJSON (f a) =>
[Interpreter a f] -> Encoding
forall k (a :: k) (f :: k -> Type).
ToJSON (f a) =>
Interpreter a f -> Value
forall k (a :: k) (f :: k -> Type).
ToJSON (f a) =>
Interpreter a f -> Encoding
$ctoJSON :: forall k (a :: k) (f :: k -> Type).
ToJSON (f a) =>
Interpreter a f -> Value
toJSON :: Interpreter a f -> Value
$ctoEncoding :: forall k (a :: k) (f :: k -> Type).
ToJSON (f a) =>
Interpreter a f -> Encoding
toEncoding :: Interpreter a f -> Encoding
$ctoJSONList :: forall k (a :: k) (f :: k -> Type).
ToJSON (f a) =>
[Interpreter a f] -> Value
toJSONList :: [Interpreter a f] -> Value
$ctoEncodingList :: forall k (a :: k) (f :: k -> Type).
ToJSON (f a) =>
[Interpreter a f] -> Encoding
toEncodingList :: [Interpreter a f] -> Encoding
ToJSON)

instance HFunctor (Interpreter a) where
  hmap :: forall (f :: k -> Type) (g :: k -> Type).
(forall (a :: k). f a -> g a) -> Interpreter a f -> Interpreter a g
hmap forall (a :: k). f a -> g a
f (Interpreter f a
x) = g a -> Interpreter a g
forall {k} (a :: k) (f :: k -> Type). f a -> Interpreter a f
Interpreter (f a -> g a
forall (a :: k). f a -> g a
f f a
x)

instance HApplicative (Interpreter a) where
  hpure :: forall (f :: k -> Type). (forall (a :: k). f a) -> Interpreter a f
hpure = f a -> Interpreter a f
(forall (a :: k). f a) -> Interpreter a f
forall {k} (a :: k) (f :: k -> Type). f a -> Interpreter a f
Interpreter
  hliftA2 :: forall (f :: k -> Type) (g :: k -> Type) (h :: k -> Type).
(forall (a :: k). f a -> g a -> h a)
-> Interpreter a f -> Interpreter a g -> Interpreter a h
hliftA2 forall (a :: k). f a -> g a -> h a
f (Interpreter f a
x) (Interpreter g a
y) = h a -> Interpreter a h
forall {k} (a :: k) (f :: k -> Type). f a -> Interpreter a f
Interpreter (f a -> g a -> h a
forall (a :: k). f a -> g a -> h a
f f a
x g a
y)

instance Package (Interpreter a) where
  unpackWith :: forall (f :: Type -> Type) (h :: k1 -> Type) (g :: k1 -> Type).
Functor f =>
(forall (a :: k1). h a -> f (g a))
-> Interpreter a h -> f (Interpreter a g)
unpackWith forall (a :: k1). h a -> f (g a)
f (Interpreter h a
x) = g a -> Interpreter a g
forall {k} (a :: k) (f :: k -> Type). f a -> Interpreter a f
Interpreter (g a -> Interpreter a g) -> f (g a) -> f (Interpreter a g)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> h a -> f (g a)
forall (a :: k1). h a -> f (g a)
f h a
x
  packWith :: forall (f :: Type -> Type) (g :: k1 -> Type) (h :: k1 -> Type).
(Foldable f, Functor f) =>
(forall (a :: k1). f (g a) -> h a)
-> f (Interpreter a g) -> Interpreter a h
packWith forall (a :: k1). f (g a) -> h a
f f (Interpreter a g)
g = h a -> Interpreter a h
forall {k} (a :: k) (f :: k -> Type). f a -> Interpreter a f
Interpreter (h a -> Interpreter a h) -> h a -> Interpreter a h
forall a b. (a -> b) -> a -> b
$ f (g a) -> h a
forall (a :: k1). f (g a) -> h a
f (Interpreter a g -> g a
forall {k} (a :: k) (f :: k -> Type). Interpreter a f -> f a
runInterpreter (Interpreter a g -> g a) -> f (Interpreter a g) -> f (g a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> f (Interpreter a g)
g)

instance Arithmetic a => Symbolic (Interpreter a) where
  type BaseField (Interpreter a) = a
  type WitnessField (Interpreter a) = a
  witnessF :: forall (f :: Type -> Type).
Functor f =>
Interpreter a f -> f (WitnessField (Interpreter a))
witnessF (Interpreter f a
x) = f a
f (WitnessField (Interpreter a))
x
  fromCircuitF :: forall (f :: Type -> Type) (g :: Type -> Type).
Interpreter a f
-> CircuitFun '[f] g (Interpreter a) -> Interpreter a g
fromCircuitF (Interpreter f a
x) CircuitFun '[f] g (Interpreter a)
c = g a -> Interpreter a g
forall {k} (a :: k) (f :: k -> Type). f a -> Interpreter a f
Interpreter (g a -> Interpreter a g) -> g a -> Interpreter a g
forall a b. (a -> b) -> a -> b
$ forall {k} (a :: k) x. Witnesses a x -> x
forall a x. Witnesses a x -> x
runWitnesses @a (FunBody '[f] g a (Witnesses a)
f a -> Witnesses a (g a)
CircuitFun '[f] g (Interpreter a)
c f a
x)
  sanityF :: forall a (f :: Type -> Type) (g :: Type -> Type).
(BaseField (Interpreter a) ~ a) =>
Interpreter a f
-> (f a -> g a)
-> (Interpreter a f -> Interpreter a g)
-> Interpreter a g
sanityF (Interpreter f a
x) f a -> g a
f Interpreter a f -> Interpreter a g
_ = g a -> Interpreter a g
forall {k} (a :: k) (f :: k -> Type). f a -> Interpreter a f
Interpreter (f a -> g a
f f a
f a
x)

-- | An example implementation of a @'MonadCircuit'@ which computes witnesses
-- immediately and drops the constraints.
newtype Witnesses a x = Witnesses { forall {k} (a :: k) x. Witnesses a x -> x
runWitnesses :: x }
  deriving ((forall a b. (a -> b) -> Witnesses a a -> Witnesses a b)
-> (forall a b. a -> Witnesses a b -> Witnesses a a)
-> Functor (Witnesses a)
forall k (a :: k) a b. a -> Witnesses a b -> Witnesses a a
forall k (a :: k) a b. (a -> b) -> Witnesses a a -> Witnesses a b
forall a b. a -> Witnesses a b -> Witnesses a a
forall a b. (a -> b) -> Witnesses a a -> Witnesses a b
forall (f :: Type -> Type).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall k (a :: k) a b. (a -> b) -> Witnesses a a -> Witnesses a b
fmap :: forall a b. (a -> b) -> Witnesses a a -> Witnesses a b
$c<$ :: forall k (a :: k) a b. a -> Witnesses a b -> Witnesses a a
<$ :: forall a b. a -> Witnesses a b -> Witnesses a a
Functor, Functor (Witnesses a)
Functor (Witnesses a) =>
(forall a. a -> Witnesses a a)
-> (forall a b.
    Witnesses a (a -> b) -> Witnesses a a -> Witnesses a b)
-> (forall a b c.
    (a -> b -> c) -> Witnesses a a -> Witnesses a b -> Witnesses a c)
-> (forall a b. Witnesses a a -> Witnesses a b -> Witnesses a b)
-> (forall a b. Witnesses a a -> Witnesses a b -> Witnesses a a)
-> Applicative (Witnesses a)
forall a. a -> Witnesses a a
forall k (a :: k). Functor (Witnesses a)
forall k (a :: k) a. a -> Witnesses a a
forall k (a :: k) a b.
Witnesses a a -> Witnesses a b -> Witnesses a a
forall k (a :: k) a b.
Witnesses a a -> Witnesses a b -> Witnesses a b
forall k (a :: k) a b.
Witnesses a (a -> b) -> Witnesses a a -> Witnesses a b
forall k (a :: k) a b c.
(a -> b -> c) -> Witnesses a a -> Witnesses a b -> Witnesses a c
forall a b. Witnesses a a -> Witnesses a b -> Witnesses a a
forall a b. Witnesses a a -> Witnesses a b -> Witnesses a b
forall a b. Witnesses a (a -> b) -> Witnesses a a -> Witnesses a b
forall a b c.
(a -> b -> c) -> Witnesses a a -> Witnesses a b -> Witnesses a c
forall (f :: Type -> Type).
Functor f =>
(forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
$cpure :: forall k (a :: k) a. a -> Witnesses a a
pure :: forall a. a -> Witnesses a a
$c<*> :: forall k (a :: k) a b.
Witnesses a (a -> b) -> Witnesses a a -> Witnesses a b
<*> :: forall a b. Witnesses a (a -> b) -> Witnesses a a -> Witnesses a b
$cliftA2 :: forall k (a :: k) a b c.
(a -> b -> c) -> Witnesses a a -> Witnesses a b -> Witnesses a c
liftA2 :: forall a b c.
(a -> b -> c) -> Witnesses a a -> Witnesses a b -> Witnesses a c
$c*> :: forall k (a :: k) a b.
Witnesses a a -> Witnesses a b -> Witnesses a b
*> :: forall a b. Witnesses a a -> Witnesses a b -> Witnesses a b
$c<* :: forall k (a :: k) a b.
Witnesses a a -> Witnesses a b -> Witnesses a a
<* :: forall a b. Witnesses a a -> Witnesses a b -> Witnesses a a
Applicative, Applicative (Witnesses a)
Applicative (Witnesses a) =>
(forall a b.
 Witnesses a a -> (a -> Witnesses a b) -> Witnesses a b)
-> (forall a b. Witnesses a a -> Witnesses a b -> Witnesses a b)
-> (forall a. a -> Witnesses a a)
-> Monad (Witnesses a)
forall a. a -> Witnesses a a
forall k (a :: k). Applicative (Witnesses a)
forall k (a :: k) a. a -> Witnesses a a
forall k (a :: k) a b.
Witnesses a a -> Witnesses a b -> Witnesses a b
forall k (a :: k) a b.
Witnesses a a -> (a -> Witnesses a b) -> Witnesses a b
forall a b. Witnesses a a -> Witnesses a b -> Witnesses a b
forall a b. Witnesses a a -> (a -> Witnesses a b) -> Witnesses a b
forall (m :: Type -> Type).
Applicative m =>
(forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
$c>>= :: forall k (a :: k) a b.
Witnesses a a -> (a -> Witnesses a b) -> Witnesses a b
>>= :: forall a b. Witnesses a a -> (a -> Witnesses a b) -> Witnesses a b
$c>> :: forall k (a :: k) a b.
Witnesses a a -> Witnesses a b -> Witnesses a b
>> :: forall a b. Witnesses a a -> Witnesses a b -> Witnesses a b
$creturn :: forall k (a :: k) a. a -> Witnesses a a
return :: forall a. a -> Witnesses a a
Monad) via Identity

instance Arithmetic a => Witness a a where
  at :: a -> a
at = a -> a
forall a. a -> a
id

instance Arithmetic a => MonadCircuit a a a (Witnesses a) where
  unconstrained :: a -> Witnesses a a
unconstrained = a -> Witnesses a a
forall a. a -> Witnesses a a
forall (m :: Type -> Type) a. Monad m => a -> m a
return
  constraint :: ClosedPoly a a -> Witnesses a ()
constraint ClosedPoly a a
_ = () -> Witnesses a ()
forall a. a -> Witnesses a a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ()
  rangeConstraint :: a -> a -> Witnesses a ()
rangeConstraint a
_ a
_ = () -> Witnesses a ()
forall a. a -> Witnesses a a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ()