{-# Language UndecidableInstances,FlexibleInstances,PolyKinds,MultiParamTypeClasses,TypeOperators, GADTs , KindSignatures , DataKinds , ConstraintKinds , TypeApplications , RankNTypes , ScopedTypeVariables , TypeFamilies#-}

import GHC.Exts 

----
-- Defunctionalization

data TyFun :: * -> * -> *

type a ~> b = TyFun a b -> *
infixr 0 ~>

type family Apply (f :: k1 ~> k2) (x :: k1) = (k :: k2) 

type a @@ b = Apply a b
infixl 9 @@

----
-- Prelude

type family IF (b :: Bool) (x :: k) (y :: k) :: k where
 IF 'False _ y = y
 IF 'True  x _ = x

type family (!!) (xs :: [k]) (n :: Nat) :: k where
 (!!) (x ': xs) Zero  = x
 (!!) (x ': xs) (Succ n) = xs !! n

type family Elem (x :: k) (xs :: [k]) :: Bool where
 Elem x '[] = 'False
 Elem x (x ':  _) = 'True
 Elem x (y ': ys) = Elem x ys

type family Not (a :: Bool) :: Bool where
 Not 'True  = 'False
 Not 'False = 'True 

type family And (a :: Bool) (b :: Bool) :: Bool where
 And 'True  'True  = 'True
 And 'False 'True  = 'False 
 And 'True  'False = 'False
 And 'False 'False = 'False

type family GT (a :: Nat) (b :: Nat) :: Bool where
 GT Zero (Succ n) = 'False
 GT (Succ n) Zero = 'True
 GT (Succ n) (Succ m) = GT n m

----
-- Intro

-- a snoc list
data Snoc a = Empty | Snoc (Snoc a) a

-- Natural numbers

data Nat where
 Zero :: Nat
 Succ :: Nat -> Nat

-- singletons Nat
data SNat (n :: Nat) where
 SZero :: SNat 'Zero
 SSucc :: SNat n -> SNat ('Succ n)

-- a snoc list which just containes SNats
data SnocSNats where
 EmptySNats :: SnocSNats 
 SnocSNats  :: SnocSNats -> SNat n -> SnocSNats 

{-
now want a snoc list of snats
where there is a constraint on them
so that the the nats point to other positions
where there are nats that point back to this position.
-}

-- a Maybe Nat
data MNat where
 MNone :: MNat
 MZero :: MNat
 MSucc :: MNat -> MNat

type family FromMNat (m :: MNat) :: Nat where
 FromMNat MZero = Zero
 FromMNat (MSucc n) = Succ (FromMNat n)

type family ToMNat (m :: Nat) :: MNat where
 ToMNat Zero = MZero
 ToMNat (Succ n) = MSucc (ToMNat n)

type family MNEquals (a :: MNat) (b :: MNat) :: Bool where
 MNEquals MNone MNone = 'True
 MNEquals MZero MZero = 'True
 MNEquals (MSucc n) (MSucc m) = MNEquals n m 
 MNEquals _ _ = 'False

type family IsJustNat (n :: MNat) :: Constraint where
 IsJustNat 'MNone = ("error" ~ "IsJustNat MNone")
 IsJustNat _ = ()

-- singletons maybe nat
data SMNat (n :: MNat) where
 SMNone :: SMNat 'MNone
 SMZero :: SMNat 'MZero
 SMSucc :: IsJustNat n => SMNat n -> SMNat ('MSucc n)

-- a snoc list which just containes SNats
data SnocSMNats where
 EmptySMNats :: SnocSMNats 
 SnocSMNats  :: SnocSMNats -> SMNat n -> SnocSMNats 

-- now add a constraint, and an arbitrary running total


----
-- Main

data Container len constraint update total a where
 EmptyContainer :: Container 'Zero constraint update total a
 SnocContainer :: constraint len total n => Container len constraint update total a -> a n -> Container (Succ len) constraint update (update @@ n @@ len @@ total) a

type C (len :: Nat) (total :: [MNat]) = Container len Constr UpdateSymbol total SMNat

emptyC :: C 'Zero '[]
emptyC = EmptyContainer 

snocC :: Constr len total n => C len total -> SMNat n -> C (Succ len) (Update n len total)
snocC = SnocContainer 

{-
check that
1. if the current position (len) is `Elem total' then 2 else 3
2. this position is linked to, 
   it must have a MNat equal to the position it was linked from.
3. this position is not already linked to. 
   check that if the MNat isnt MNone, 
   that its greater than the current position (len).
   this establishes a link to a subsequent element.

a. check if its MNone, if yes then b else c
b. its MNone, ensure that len is not Elem total
c. its not MNone, 
   its either a forwards or backwards link,
   check this first,
   if its GT len, then d else e
d. the link is yet to be established,
   this means it shouldnt be len Elem total.
   can combine this with b?
e. this closes a link len should be Elem total
   and this value should be at position n.

x. if its MNone or n `GT` len, then;  ensure that len is not Elem total
y. its a backwards link, ensure len `Elem` total, and total !! n == len
-}

----
-- The Constraint

class    (True ~ ConstrHelper n len total) => Constr (len :: Nat) (total :: [MNat]) (n :: MNat) 
instance (True ~ ConstrHelper n len total) => Constr (len :: Nat) (total :: [MNat]) (n :: MNat) 

type ConstrHelper (n :: MNat) (len :: Nat) (total :: [MNat]) =  ConstrHelperX n len total 

type family ConstrHelperX (n :: MNat) (len :: Nat) (total :: [MNat]) :: Bool where
 ConstrHelperX MNone len total = Not (Elem (ToMNat len) total)
 ConstrHelperX n len total = IF (GT (FromMNat n) len) (Not (Elem (ToMNat len) total)) (ConstrHelperY n len total)

type family ConstrHelperY (n :: MNat) (len :: Nat) (total :: [MNat]) :: Bool where
 ConstrHelperY n len total = And (Elem (ToMNat len) total) ((total !! (FromMNat n)) `MNEquals` (ToMNat len))

----
-- The Update function (for the total)

data UpdateSymbol :: MNat ~> Nat ~> [MNat] ~> [MNat]
type instance Apply UpdateSymbol a = UpdateSym1 a

data UpdateSym1 :: MNat -> Nat ~> [MNat] ~> [MNat]
type instance Apply (UpdateSym1 a) b = UpdateSym2 a b

data UpdateSym2 :: MNat -> Nat -> [MNat] ~> [MNat]
type instance Apply (UpdateSym2 a b) c = Update a b c

type family Update (n :: MNat) (len :: Nat) (total :: [MNat]) :: [MNat] where
 Update MNone len total = MNone ': total
 Update n len total = IF (Elem (ToMNat len) total) (MNone ': (CloseLink (FromMNat n) total)) (n ': total)

-- len > n by the constraint, as otherwise it would be a forward link
type family CloseLink (i :: Nat) (xs :: [MNat]) :: [MNat] where
 CloseLink Zero (x ': xs) = MNone ': xs
 CloseLink (Succ n) (x ': xs) = x ': (CloseLink n xs)

----
-- Test

test
  :: C ('Succ ('Succ ('Succ ('Succ ('Succ 'Zero)))))
       '[ 'MNone, 'MNone, 'MNone, 'MNone, 'MNone]
test = emptyC 
       `snocC` (SMNone)
       `snocC` (SMSucc (SMSucc (SMSucc SMZero)))
       `snocC` (SMNone)
       `snocC` (SMSucc SMZero)
       `snocC` (SMNone)