{-# LANGUAGE TypeOperators #-}

module ZkFold.Symbolic.Data.Morph where

import           Data.Function              (const, ($), (.))
import           Data.Proxy                 (Proxy (..))
import           Data.Type.Equality         (type (~))

import           ZkFold.Symbolic.Class      (Symbolic (BaseField))
import           ZkFold.Symbolic.Data.Class (SymbolicData (..), SymbolicOutput)
import           ZkFold.Symbolic.Fold       (SymbolicFold)

-- | A type @u@ is a 'Replica' of type @t@ in context @c@ iff:
-- * it is 'SymbolicOutput';
-- * its context is @c@;
-- * its representation (layout and payload) match those of @t@.
type Replica c t u =
  ( SymbolicOutput u, Context u ~ c
  , Layout u ~ Layout t, Payload u ~ Payload t)

-- | A function is a "morph" of a function of type @input -> output@
-- /to/ context @c@ iff it is a function of type @i -> o@
-- for some 'Replica's @i@, @o@ of @input@ and @output@, correspondingly,
-- in context @c@.
data MorphTo c input output =
  forall i o. (Replica c input i, Replica c output o) => Morph (i -> o)

-- | One can apply a morph of a function @input -> output@ in context @c@
-- if they provide 'Replica's of @input@ and @output@ in context @c@.
(@) ::
  (Replica c input i, Replica c output o) =>
  MorphTo c input output -> i -> o
Morph i -> o
f @ :: forall (c :: (Type -> Type) -> Type) input i output o.
(Replica c input i, Replica c output o) =>
MorphTo c input output -> i -> o
@ i
x =
  let y :: o
y = i -> o
f (i -> o)
-> ((Proxy c -> (c (Layout input), Payload input (WitnessField c)))
    -> i)
-> (Proxy c -> (c (Layout input), Payload input (WitnessField c)))
-> o
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Proxy c -> (c (Layout input), Payload input (WitnessField c)))
-> i
(Support i -> (c (Layout i), Payload i (WitnessField c))) -> i
forall x (c :: (Type -> Type) -> Type).
(SymbolicData x, Context x ~ c) =>
(Support x -> (c (Layout x), Payload x (WitnessField c))) -> x
forall (c :: (Type -> Type) -> Type).
(Context i ~ c) =>
(Support i -> (c (Layout i), Payload i (WitnessField c))) -> i
restore ((Proxy c -> (c (Layout input), Payload input (WitnessField c)))
 -> o)
-> (Proxy c -> (c (Layout input), Payload input (WitnessField c)))
-> o
forall a b. (a -> b) -> a -> b
$ (c (Layout input), Payload input (WitnessField c))
-> Proxy c -> (c (Layout input), Payload input (WitnessField c))
forall a b. a -> b -> a
const (i -> Support i -> Context i (Layout i)
forall x. SymbolicData x => x -> Support x -> Context x (Layout x)
arithmetize i
x Proxy c
Support i
forall {k} (t :: k). Proxy t
Proxy, i -> Support i -> Payload i (WitnessField (Context i))
forall x.
SymbolicData x =>
x -> Support x -> Payload x (WitnessField (Context x))
payload i
x Proxy c
Support i
forall {k} (t :: k). Proxy t
Proxy)
   in (Support o -> (c (Layout o), Payload o (WitnessField c))) -> o
forall x (c :: (Type -> Type) -> Type).
(SymbolicData x, Context x ~ c) =>
(Support x -> (c (Layout x), Payload x (WitnessField c))) -> x
forall (c :: (Type -> Type) -> Type).
(Context o ~ c) =>
(Support o -> (c (Layout o), Payload o (WitnessField c))) -> o
restore ((Support o -> (c (Layout o), Payload o (WitnessField c))) -> o)
-> (Support o -> (c (Layout o), Payload o (WitnessField c))) -> o
forall a b. (a -> b) -> a -> b
$ (c (Layout output), Payload output (WitnessField c))
-> Proxy c -> (c (Layout output), Payload output (WitnessField c))
forall a b. a -> b -> a
const (o -> Support o -> Context o (Layout o)
forall x. SymbolicData x => x -> Support x -> Context x (Layout x)
arithmetize o
y Proxy c
Support o
forall {k} (t :: k). Proxy t
Proxy, o -> Support o -> Payload o (WitnessField (Context o))
forall x.
SymbolicData x =>
x -> Support x -> Payload x (WitnessField (Context x))
payload o
y Proxy c
Support o
forall {k} (t :: k). Proxy t
Proxy)

-- | A function is a "morph" of a function of type @input -> output@
-- /from/ context @ctx@ iff, for each context @c@ over same base field,
-- it is a morph /to/ @c@.
--
-- Thus, if a function is 'MorphFrom', it can be
-- * safely passed through parametricity boundary set by 'sfoldl';
-- * applied there in an anonymous context to an argument.
type MorphFrom ctx input output =
  forall c.
  (SymbolicFold c, BaseField c ~ BaseField ctx) =>
  MorphTo c input output