Zipper000.hs

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

module Zipper000 (getUp, getDown) where

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)) } @-}

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

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

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

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

data Foo a b = J | P a b

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

-- focusUp (Stack t [] rs) = Stack t rs []





--------------------------------------------------------------------------------------