module Data.Logical.Let
  ( Let
  , LetT
  , Var
  , MonadLet
  , free
  , val
  , (===)
  , runLet
  , runLetT
  ) where



import Data.Map (Map)
import Control.Monad.Reader
import Control.Monad.State
import Control.Monad.Writer

import Data.Logical.Knot



type VarId = Integer

newtype Let x a = Let (StateT VarId (Knot VarId x) a)
        deriving (Monad, MonadFix, MonadKnot VarId x)

newtype LetT x m a = LetT (StateT VarId (KnotT VarId x m) a)
        deriving (Monad, MonadFix, MonadKnot VarId x)

data Var x = Var VarId x



instance MonadTrans (LetT x)
  where
    lift = LetT . lift . lift
  -- Couldn't be derived for some reason

instance MonadKnot i x m => MonadKnot i x (StateT s m)
  where
    askKnot      = lift . askKnot
    askKnotDef x = lift . askKnotDef x
    i *= x       = lift (i *= x)
  -- So that MonadKnot can be derived for Let and LetT.



free_ :: MonadKnot VarId x m => StateT VarId m (Var x)
free_ = do
    vid <- get
    put (succ vid)
    x <- lift $ askKnot vid
    return (Var vid x)

class MonadKnot VarId x m => MonadLet x m | m -> x
  where
    free :: m (Var x)

instance MonadLet x (Let x)
  where
    free = Let free_

instance Monad m => MonadLet x (LetT x m)
  where
    free = LetT free_



val :: Var x -> x
val (Var _ x) = x

infix 1 ===

(===) :: MonadLet x m => Var x -> x -> m ()
Var vid _ === x = vid *= x

var :: MonadLet x m => x -> m (Var x)
var x = do
    v <- free
    v === x
    return v


test = runLet $ do
    a' <- var a
    a' === a
    return a
  where
    a = 4 :: Int

acc = error "Multiple assignments to variable"

runLet :: Let x a -> a
runLet (Let ma) = fst $ fst $ accKnot acc $ runStateT ma 0

runLetT :: MonadFix m => LetT x m a -> m a
runLetT (LetT ma) = liftM (fst.fst) $ accKnotT acc $ runStateT ma 0