module ZkFold.Symbolic.Data.Switch where

import           Data.Function                    (const, ($), (.))
import           Data.Proxy                       (Proxy (..))

import           ZkFold.Symbolic.Class            (Symbolic (..))
import           ZkFold.Symbolic.Data.Bool        (Bool)
import           ZkFold.Symbolic.Data.Class       (SymbolicData (..))
import           ZkFold.Symbolic.Data.Conditional (Conditional (..))
import           ZkFold.Symbolic.Data.Payloaded   (Payloaded (..))

-- | A 'Switch' of a 'SymbolicData' @x@ to context @c@
-- is a separate Symbolic datatype which has the same layout and payload as @x@,
-- but is defined in a context @c@ which can differ from @'Context' x@.
--
-- In other words, it is a useful default 'Replica' of @x@ in context @c@
-- when nothing else works.
data Switch c x = Switch
  { forall (c :: (Type -> Type) -> Type) x. Switch c x -> c (Layout x)
sLayout  :: c (Layout x)
  , forall (c :: (Type -> Type) -> Type) x.
Switch c x -> Payload x (WitnessField c)
sPayload :: Payload x (WitnessField c)
  }

instance (Symbolic c, SymbolicData x) => SymbolicData (Switch c x) where
  type Context (Switch c x) = c
  type Support (Switch c x) = Proxy c
  type Layout (Switch c x) = Layout x
  type Payload (Switch c x) = Payload x
  arithmetize :: Switch c x
-> Support (Switch c x)
-> Context (Switch c x) (Layout (Switch c x))
arithmetize = c (Layout x) -> Proxy c -> c (Layout x)
forall a b. a -> b -> a
const (c (Layout x) -> Proxy c -> c (Layout x))
-> (Switch c x -> c (Layout x))
-> Switch c x
-> Proxy c
-> c (Layout x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Switch c x -> c (Layout x)
forall (c :: (Type -> Type) -> Type) x. Switch c x -> c (Layout x)
sLayout
  payload :: Switch c x
-> Support (Switch c x)
-> Payload (Switch c x) (WitnessField (Context (Switch c x)))
payload = Payload x (WitnessField c) -> Proxy c -> Payload x (WitnessField c)
forall a b. a -> b -> a
const (Payload x (WitnessField c)
 -> Proxy c -> Payload x (WitnessField c))
-> (Switch c x -> Payload x (WitnessField c))
-> Switch c x
-> Proxy c
-> Payload x (WitnessField c)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Switch c x -> Payload x (WitnessField c)
forall (c :: (Type -> Type) -> Type) x.
Switch c x -> Payload x (WitnessField c)
sPayload
  restore :: forall (c :: (Type -> Type) -> Type).
(Context (Switch c x) ~ c) =>
(Support (Switch c x)
 -> (c (Layout (Switch c x)),
     Payload (Switch c x) (WitnessField c)))
-> Switch c x
restore Support (Switch c x)
-> (c (Layout (Switch c x)), Payload (Switch c x) (WitnessField c))
f = let (c (Layout (Switch c x))
sLayout, Payload (Switch c x) (WitnessField c)
sPayload) = Support (Switch c x)
-> (c (Layout (Switch c x)), Payload (Switch c x) (WitnessField c))
f Proxy c
Support (Switch c x)
forall {k} (t :: k). Proxy t
Proxy in Switch {c (Layout x)
c (Layout (Switch c x))
Payload x (WitnessField c)
Payload (Switch c x) (WitnessField c)
sLayout :: c (Layout x)
sPayload :: Payload x (WitnessField c)
sLayout :: c (Layout (Switch c x))
sPayload :: Payload (Switch c x) (WitnessField c)
..}

instance (Symbolic c, SymbolicData x) => Conditional (Bool c) (Switch c x) where
  bool :: Switch c x -> Switch c x -> Bool c -> Switch c x
bool (Switch c (Layout x)
fl Payload x (WitnessField c)
fp) (Switch c (Layout x)
tl Payload x (WitnessField c)
tp) Bool c
b =
    c (Layout x) -> Payload x (WitnessField c) -> Switch c x
forall (c :: (Type -> Type) -> Type) x.
c (Layout x) -> Payload x (WitnessField c) -> Switch c x
Switch (c (Layout x) -> c (Layout x) -> Bool c -> c (Layout x)
forall b a. Conditional b a => a -> a -> b -> a
bool c (Layout x)
fl c (Layout x)
tl Bool c
b) (Payload x (WitnessField c) -> Switch c x)
-> Payload x (WitnessField c) -> Switch c x
forall a b. (a -> b) -> a -> b
$ Payloaded (Payload x) c -> Payload x (WitnessField c)
forall (f :: Type -> Type) (c :: (Type -> Type) -> Type).
Payloaded f c -> f (WitnessField c)
runPayloaded (Payloaded (Payload x) c -> Payload x (WitnessField c))
-> Payloaded (Payload x) c -> Payload x (WitnessField c)
forall a b. (a -> b) -> a -> b
$
      Payloaded (Payload x) c
-> Payloaded (Payload x) c -> Bool c -> Payloaded (Payload x) c
forall b a. Conditional b a => a -> a -> b -> a
bool (Payload x (WitnessField c) -> Payloaded (Payload x) c
forall (f :: Type -> Type) (c :: (Type -> Type) -> Type).
f (WitnessField c) -> Payloaded f c
Payloaded Payload x (WitnessField c)
fp :: Payloaded (Payload x) c) (Payload x (WitnessField c) -> Payloaded (Payload x) c
forall (f :: Type -> Type) (c :: (Type -> Type) -> Type).
f (WitnessField c) -> Payloaded f c
Payloaded Payload x (WitnessField c)
tp) Bool c
b