module Synthesizer.Inference.Logic.Signal where

import qualified Synthesizer.Inference.Logic.Process as Process
import qualified UniqueLogicNP.Lazy.SingleStep as Logic
import Synthesizer.Inference.Logic.Process ((<<<), )


newtype T param signal =
   Cons (param -> (signal, param))

evaluate ::
   (Logic.VariableGroup param) =>
   T param signal ->
   signal
evaluate (Cons f) =
   let (x,p) = f (Logic.closeCycleGroup p)
   in  x

singleton ::
   (Eq a) =>
   a -> x -> T (Logic.Variable a) x
singleton a x0 =
   Cons $ \p ->
   let x =
         if a == Logic.variableValue p
           then x0
           else error "Signal.singleton: inconsistent parameter"
   in  (x, Logic.constant a)

pair ::
   (Eq a, Eq b) =>
   T (Logic.Variable a) x ->
   T (Logic.Variable b) y ->
   T (Logic.Variable a, Logic.Variable b) (x,y)
pair (Cons f) (Cons g) =
   Cons $ \(pa,pb) ->
   let (x,qa) = f pa
       (y,qb) = g pb
   in  ((x,y), (qa,qb))

($:) ::
   (Logic.VariableGroup param) =>
   Process.T param result (inSignal -> outSignal) ->
   T param inSignal ->
   T result outSignal
($:) (Process.Cons f) (Cons x) =
   Cons $ \yParams ->
   let (xBody,xResults) = x (Logic.closeCycleGroup xParams)
       (fc, (xParams,yResults)) = f (xResults,yParams)
   in  (fc xBody, yResults)



data Type =
     Char
   | List Type
   deriving (Eq, Show)

charObject :: T (Logic.Variable Type) Char
charObject =
   singleton Char 'a'

stringObject :: T (Logic.Variable Type) String
stringObject =
   singleton (List Char) "bc"

connectListElemTypes ::
   Logic.Variable Type ->
   Logic.Variable Type ->
   (Logic.Variable Type, Logic.Variable Type)
connectListElemTypes =
   Logic.rule2
      (\t0 ->
         case t0 of
            List t1 -> t1
            _ -> error "consList: second parameter must be a List type")
      List

singletonList ::
   Process.T
      (Logic.Variable Type)
      (Logic.Variable Type)
      (Char -> String)
singletonList =
   Process.Cons $ \(p0,q1) ->
      let (q0,p1) = connectListElemTypes p0 q1
          listType = List $ Logic.variableValue q0
          f =
             if listType == Logic.variableValue q1
               then (:[])
               else error "singletonList: inconsistent parameter types"
      in  (f, (q0,p1))

consList ::
   Process.T
      (Logic.Variable Type, Logic.Variable Type)
      (Logic.Variable Type)
      ((Char, String) -> String)
consList =
   Process.Cons $ \((p0,p1), q2) ->
      let (q0,a) = connectListElemTypes p0 p1
          (q1,p2) = Logic.equal a q2
          listType = List $ Logic.variableValue q0
          f =
             if listType == Logic.variableValue q1 &&
                listType == Logic.variableValue p2
               then uncurry (:)
               else error "consList: inconsistent parameter types"
      in  (f, ((q0,q1),p2))

-- this gives wrong alarm
exampleSingleton :: (Type, String)
exampleSingleton =
   evaluate
      ((Process.exposeParameter <<< singletonList)
         $: charObject)

-- this gives wrong alarm
exampleCons :: (Type, String)
exampleCons =
   evaluate
      ((Process.exposeParameter <<< consList)
         $: pair charObject stringObject)

exampleFail0 :: (Type, String)
exampleFail0 =
   evaluate
      ((Process.exposeParameter <<< consList)
         $: pair charObject (singleton Char "bc"))

exampleFail1 :: (Type, String)
exampleFail1 =
   evaluate
      ((Process.exposeParameter <<< consList)
         $: pair (singleton (List Char) 'a') stringObject)

exampleLoop :: (Type, String)
exampleLoop =
   evaluate
      ((Process.exposeParameter <<< Process.loop (Process.double <<< consList))
         $: charObject)