pop.idr

module Main

import Data.Nat

data Stack_ : Type -> Type where
  Empty : Stack_ a
  One : Stack_ a -> Stack_ a

pop_ : Stack_ a -> Stack_ a
pop_ Empty = Empty
pop_ (One s) = case pop_ s of
  Empty => One Empty
  One s' => One (One s')

data DStack : Stack_ a -> Type where
  DOne : {s : _} -> Nat -> DStack s -> DStack (One s)
  DEmpty : DStack Empty

dpop_ : DStack s -> DStack (pop_ s)
dpop_ DEmpty = DEmpty
dpop_ (DOne {s} n ds) with (pop_ s)
  dpop_ (DOne {s} n ds) | Empty = ?foo2
  dpop_ (DOne {s} n ds) | (One y) with (dpop_ ds)
    dpop_ (DOne {s} n ds) | (One y) | DOne n' ds' = ?bar


{-
e.idr:25:39--25:50:While processing left hand side of with block in with block in dpop_ at e.idr:25:5--27:1:
Can't solve constraint between:
        One ?s
and
        pop_ ?s
at:
25          dpop_ (DOne {s} n ds) | (One y) | DOne n' ds' = ?bar
                                              ^^^^^^^^^^^
-}

pop_ : Stack_ a -> Stack_ a
pop_ Empty = Empty
pop_ (One s) = case pop_ s of
  Empty => One Empty
  One s' => One (One s')

pop_' : Stack_ a -> Stack_ a
pop_' (One s) = s
pop_' _ = Empty

pop_test  : pop_  (One (One (One (One Empty)))) = (One (One (One (One Empty))))
pop_test = Refl -- id

pop_'test : pop_' (One (One (One (One Empty)))) = (One (One (One (One Empty))))
pop_'test = ?notId