{-# LANGUAGE
  TypeOperators
, FlexibleContexts
, TypeFamilies
, UndecidableInstances #-}

module Calculus.Connectives.Linear where

import Calculus.Expr
import Calculus.Connectives.Simple

import Auxiliary.NameSource

import Data.Functor
import Control.Monad.State

-- Simultaneous conjunction
data SimConj f = SimConj f f

-- Alternative conjunction
data AltConj f = AltConj f f

-- Disjunction (external choice)
data Disj f = Disj f f

-- Linear implication (resource implication)
data ResImpl f = ResImpl f f

-- Unrestricted implication
data ValImpl f = ValImpl f f

-- Unit (trivial goal which requires no resources)
data Unit f = Unit

-- Top (trivial goal which consumes all resources)
data Top f = Top

-- Zero (impossibility)
data Zero f = Zero

-- Modal operation (states that `f` is valid)
data Modal f = Modal f

{-
    LinearInput.
-}
type LinearInput = SimConj :+: AltConj :+: Disj :+:
                      ResImpl :+: ValImpl :+: Unit :+:
                        Top :+: Zero :+: Modal :+: SimpleInput
                        
type LinearFormula = Formula LinearInput

{- 
    Functor instances.
-}
instance Functor SimConj where
  fmap f (SimConj a b) = SimConj (f a) (f b)
  
instance Functor AltConj where
  fmap f (AltConj a b) = AltConj (f a) (f b)

instance Functor Disj where
  fmap f (Disj a b) = Disj (f a) (f b)
  
instance Functor ResImpl where
  fmap f (ResImpl a b) = ResImpl (f a) (f b)

instance Functor ValImpl where
  fmap f (ValImpl a b) = ValImpl (f a) (f b)
  
instance Functor Unit where
  fmap _ Unit = Unit
  
instance Functor Top where
  fmap _ Top = Top
  
instance Functor Zero where
  fmap _ Zero = Zero
  
instance Functor Modal where
  fmap f (Modal g) = Modal (f g)
  
{-
    Smart constructors.
-}
(&&:) :: (SimConj :<: f) => Expr f -> Expr f -> Expr f
(&&:) f = inject . SimConj f

($$:) :: (AltConj :<: f) => Expr f -> Expr f -> Expr f
($$:) f = inject . AltConj f

(||:) :: (Disj :<: f) => Expr f -> Expr f -> Expr f
(||:) f = inject . Disj f

(->:) :: (ResImpl :<: f) => Expr f -> Expr f -> Expr f
(->:) f = inject . ResImpl f

(=>:) :: (ValImpl :<: f) => Expr f -> Expr f -> Expr f
(=>:) f = inject . ValImpl f

unit :: (Unit :<: f) => Expr f
unit = inject Unit

top :: (Top :<: f) => Expr f
top = inject Top

zero :: (Zero :<: f) => Expr f
zero = inject Zero

modal :: (Modal :<: f) => Expr f -> Expr f
modal = inject . Modal

{- Lists of synchronious and asynchronious connectives -}

type RightAsyncInput = ResImpl :+: ValImpl :+: AltConj :+: Top :+: ForAll
type RightSyncInput  = SimConj :+: Unit :+: Disj :+: Zero :+: Modal :+: Exists
type LeftAsyncInput  = RightSyncInput
type LeftSyncInput   = RightAsyncInput

{- Render -}

instance Render SimConj where
  render (SimConj a b) = renderBinOp "&&" (a, b)
       
instance Render AltConj where
  render (AltConj a b) = renderBinOp "$$" (a, b)
    
instance Render Disj where
  render (Disj a b) = renderBinOp "||" (a, b)
  
instance Render ResImpl where
  render (ResImpl a b) = renderBinOp "->" (a, b)
  
instance Render ValImpl where
  render (ValImpl a b) = renderBinOp "=>" (a, b)
  
instance Render Unit where
  render Unit = return "1"
  
instance Render Top where
  render Top = return "T"
  
instance Render Zero where
  render Zero = return "0"
  
instance Render Modal where
  render (Modal a) =
    do ns <- get
       return $ "!" ++ pretty ns a 
