{- |
It's like Inference.Fix but with a more basic approach
and a complete set of combinators equivalent to the Arrow class.
-}
module Synthesizer.Inference.Logic.Process where

import qualified UniqueLogicNP.Lazy.SingleStep as Logic
import qualified Control.Arrow as Arrow
import Control.Arrow (Arrow, ArrowLoop, )

{-
We could abuse

import qualified Synthesizer.Dimensional.Arrow

or we could formulate that Arrow class more generally
for datatypes with global and local data,
or data that is divided in preprocessing and main processing.
But this is not easily done,
since the Arrows we define here
need constraints on the @param@ type parameter.
-}

{-
The order of pair elements is analoguous to State monad,
but different from Dimensional.Causal.Process.

In the inner of our arrow we use another arrow.
This can be the function type constructor or a causal process,
and certainly other types.
-}
newtype T params results arrow =
   Cons ((params, results) -> (arrow, (params, results)))


forceParam ::
   -- Category arrow
   (Eq a, Arrow arrow) =>
   a ->
   T (Logic.Variable a) (Logic.Variable a) (arrow sig sig)
forceParam a =
   Cons $ \(p,q) ->
      let f =
             if a == Logic.variableValue p &&
                a == Logic.variableValue q
               then Arrow.arr id
               else error "forceParam: inconsistent variable values"
      in  (f, (Logic.constant a, Logic.constant a))

{- |
Params should be a single or a tuple of @Logic.constant x@ variables.
-}
forceParams ::
   -- Category arrow
   (Logic.VariableGroup param, Arrow arrow) =>
   param ->
   T param param (arrow sig sig)
forceParams a =
   Cons $ \(p,q) ->
      let f =
             if Logic.equalValues a p &&
                Logic.equalValues a q
               then Arrow.arr id
               else error "forceParams: inconsistent variable values"
      in  (f, (a, a))


{-
When following the clean theory,
we had to use 'Logic.equal' in order to make the parameters equal.
Instead we just forward the parameters
and let the check be done somewhere else.
We can safe redundant checks this way.
-}
pure ::
   arrow ->
   T param param arrow
pure f =
   Cons $ \(p,q) -> (f, (p,q))


infixr 3 ***
infixr 3 &&&
-- infixr 1 >>>
infixr 1 <<<

{-
I am uncertain, whether closeCycleGroup
and thus the VariableGroup constraint is required.
If it is required, it would be good to have an example
that does not work when closeCycleGroup is omitted.
-}
(<<<) ::
   -- Category arrow
   (Logic.VariableGroup param1, Arrow arrow) =>
   T param1 param2 (arrow sig1 sig2) ->
   T param0 param1 (arrow sig0 sig1) ->
   T param0 param2 (arrow sig0 sig2)
(<<<) (Cons g) (Cons f) =
   Cons $ \(p0,q2) ->
      let (fc, (q0,p1)) = f (p0, Logic.closeCycleGroup q1)
          (gc, (q1,p2)) = g (p1,q2)
      in  (gc Arrow.<<< fc, (q0,p2))

first ::
   (Arrow arrow) =>
   T param0 param1 (arrow sig0 sig1) ->
   T (param0,param) (param1,param) (arrow (sig0,sig) (sig1,sig))
first (Cons f) =
   Cons $ \((p0,p), (q1,q)) ->
      let (fc, (q0,p1)) = f (p0,q1)
      in  (Arrow.first fc, ((q0,p),(p1,q)))

second ::
   (Arrow arrow) =>
   T param0 param1 (arrow sig0 sig1) ->
   T (param,param0) (param,param1) (arrow (sig,sig0) (sig,sig1))
second (Cons f) =
   Cons $ \((p,p0), (q,q1)) ->
      let (fc, (q0,p1)) = f (p0,q1)
      in  (Arrow.second fc, ((p,q0),(q,p1)))

(***) ::
   (Arrow arrow) =>
   T param0 param1 (arrow sig0 sig1) ->
   T param2 param3 (arrow sig2 sig3) ->
   T (param0,param2) (param1,param3) (arrow (sig0,sig2) (sig1,sig3))
(***) (Cons f) (Cons g) =
   Cons $ \((p0,p2), (q1,q3)) ->
      let (fc, (q0,p1)) = f (p0,q1)
          (gc, (q2,p3)) = g (p2,q3)
      in  (fc Arrow.*** gc, ((q0,q2),(p1,p3)))

double ::
   (Logic.VariableGroup param, Arrow arrow) =>
   T param (param, param) (arrow sig (sig,sig))
double =
   Cons $ \(p,(q0,q1)) ->
      let f =
             if Logic.equalValues q0 q1
               then Arrow.arr (\x->(x,x))
               else error "double: inconsistent variable values"
      in  (f, (Logic.mergeGroups q0 q1, (p,p)))

(&&&) ::
   (Logic.VariableGroup param, Arrow arrow) =>
   T param param0 (arrow sig sig0) ->
   T param param1 (arrow sig sig1) ->
   T param (param0,param1) (arrow sig (sig0,sig1))
(&&&) x y =
   (x***y) <<< double

loop ::
   (Logic.VariableGroup param, ArrowLoop arrow) =>
   T (param0,param) (param1,param) (arrow (sig0,sig) (sig1,sig)) ->
   T param0 param1 (arrow sig0 sig1)
loop (Cons f) =
   Cons $ \(p0, q1) ->
      let (fc, ((q0,q),(p1,p))) =
              f ((p0, Logic.closeCycleGroup q),
                 (q1, Logic.closeCycleGroup p))
      in  (Arrow.loop fc, (q0,p1))


exposeParameter ::
   (Arrow arrow) =>
   T (Logic.Variable p) (Logic.Variable p) (arrow a (p, a))
exposeParameter =
   Cons $ \(p,q) -> (Arrow.arr ((,) (Logic.variableValue p)), (p,q))