{-@ LIQUID "--no-totality" @-}

module Zipper (getUp, getDown, getFocus) where

import Prelude hiding (reverse)

import Data.Set

data Stack a = Stack { focus  :: !a        -- focused thing in this set
                     , up     :: [a]       -- jokers to the left
                     , down   :: [a] }     -- jokers to the right

{-@ type UListDif a N = {v:[a] | ((not (Set_mem N (listElts v))) && (Set_emp (listDup v)))} @-}

{-@
data Stack a = Stack { focus :: a
                     , up    :: UListDif a focus
                     , down  :: UListDif a focus }
@-}

{-@ measure listDup :: [a] -> (Set a)
  listDup([]) = {v | Set_emp v }
  listDup(x:xs) = {v | v = if (Set_mem x (listElts xs)) then (Set_cup (Set_sng x) (listDup xs)) else (listDup xs) }
  @-}

{-@ type UStack a = {v:Stack a |(Set_emp (Set_cap (listElts (getUp v)) (listElts (getDown v))))}@-}

{-@ measure getFocus @-}
getFocus :: Stack a -> a
getFocus (Stack xfocus _ _) = xfocus

{-@ measure getUp @-}
getUp :: Stack a -> [a]
getUp (Stack xfocus xup xdown) = xup

{-@ measure getDown @-}
getDown :: Stack a -> [a]
getDown (Stack xfocus xup xdown) = xdown


-- QUALIFIERS
{-@ q :: x:a ->  {v:[a] |(not (Set_mem x (listElts v)))} @-}
q :: a -> [a]
q = undefined
{-@ q1 :: x:a ->  {v:[a] |(Set_mem x (listElts v))} @-}
q1 :: a -> [a]
q1 = undefined
{-@ q0 :: x:a ->  {v:[a] |(Set_emp(listDup v))} @-}
q0 :: a -> [a]
q0 = undefined


{-@ focusUp :: UStack a -> UStack a @-}
focusUp :: Stack a -> Stack a
focusUp (Stack t [] rs)     = Stack xiggety xs [] where (xiggety:xs) = reverse (t:rs)
focusUp (Stack t (l:ls) rs) = Stack l ls (t:rs)

{-@ focusDown :: UStack a -> UStack a @-}
focusDown :: Stack a -> Stack a
focusDown = reverseStack . focusUp . reverseStack

-- | reverse a stack: up becomes down and down becomes up.
{-@ reverseStack :: UStack a -> UStack a @-}
reverseStack :: Stack a -> Stack a
reverseStack (Stack t ls rs) = Stack t rs ls


-- TODO ASSUMES
{-@ reverse :: {v:[a] | (Set_emp (listDup v))} -> {v:[a]|(Set_emp (listDup v))} @-}
reverse :: [a] -> [a]
reverse = undefined