module stack-product where

open import product
open import Data.Product
open import Data.Nat
open import Function using (id)
open import Relation.Binary.PropositionalEquality

-- definition based from Gears(209:5708390a9d88) src/parallel_execution
goto = executeCS

data Bool : Set where
  True  : Bool
  False : Bool

data Maybe (a : Set) : Set  where
  Nothing : Maybe a
  Just    : a @$\rightarrow$@ Maybe a


record Stack {a t : Set} (stackImpl : Set) : Set  where
  field
    stack : stackImpl
    push : CodeSegment (stackImpl @$\times$@ a @$\times$@ (CodeSegment stackImpl t)) t
    pop  : CodeSegment (stackImpl @$\times$@ (CodeSegment (stackImpl @$\times$@ Maybe a) t)) t


data Element (a : Set) : Set where
  cons : a @$\rightarrow$@ Maybe (Element a) @$\rightarrow$@ Element a

datum : {a : Set} @$\rightarrow$@ Element a @$\rightarrow$@ a
datum (cons a _) = a

next : {a : Set} @$\rightarrow$@ Element a @$\rightarrow$@ Maybe (Element a)
next (cons _ n) = n

record SingleLinkedStack (a : Set) : Set where
  field
    top : Maybe (Element a)
open SingleLinkedStack

emptySingleLinkedStack : {a : Set} @$\rightarrow$@ SingleLinkedStack a
emptySingleLinkedStack = record {top = Nothing}




pushSingleLinkedStack : {a t : Set} @$\rightarrow$@ CodeSegment ((SingleLinkedStack a) @$\times$@ a @$\times$@ (CodeSegment (SingleLinkedStack a) t)) t
pushSingleLinkedStack = cs push
  where
    push : {a t : Set} @$\rightarrow$@ ((SingleLinkedStack a) @$\times$@ a @$\times$@ (CodeSegment (SingleLinkedStack a) t)) @$\rightarrow$@ t
    push (stack , datum , next) = goto next stack1
      where
        element = cons datum (top stack)
        stack1  = record {top = Just element}

popSingleLinkedStack : {a t : Set} @$\rightarrow$@ CodeSegment (SingleLinkedStack a @$\times$@ (CodeSegment (SingleLinkedStack a @$\times$@ Maybe a) t))  t
popSingleLinkedStack = cs pop
  where
    pop : {a t : Set} @$\rightarrow$@ (SingleLinkedStack a @$\times$@ (CodeSegment (SingleLinkedStack a @$\times$@ Maybe a) t)) @$\rightarrow$@ t
    pop (record { top = Nothing } , nextCS) = goto nextCS (emptySingleLinkedStack , Nothing) 
    pop (record { top = Just x } , nextCS)  = goto nextCS (stack1 , (Just datum1))
      where
        datum1 = datum x
        stack1 = record { top = (next x) }





createSingleLinkedStack : {a b : Set} @$\rightarrow$@ Stack {a} {b} (SingleLinkedStack a)
createSingleLinkedStack = record { stack = emptySingleLinkedStack
                                 ; push = pushSingleLinkedStack
                                 ; pop  = popSingleLinkedStack
                                 }




test01 : {a : Set} @$\rightarrow$@ CodeSegment (SingleLinkedStack a @$\times$@ Maybe a) Bool
test01 = cs test01'
  where
    test01' : {a : Set} @$\rightarrow$@ (SingleLinkedStack a @$\times$@ Maybe a) @$\rightarrow$@ Bool
    test01' (record { top = Nothing } , _) = False
    test01' (record { top = Just x } ,  _)  = True


test02 : {a : Set} @$\rightarrow$@ CodeSegment (SingleLinkedStack a) (SingleLinkedStack a @$\times$@ Maybe a)
test02 = cs test02'
  where
    test02' : {a : Set} @$\rightarrow$@ SingleLinkedStack a @$\rightarrow$@ (SingleLinkedStack a @$\times$@ Maybe a)
    test02' stack = goto popSingleLinkedStack (stack , (cs id))


test03 : {a : Set} @$\rightarrow$@ CodeSegment a (SingleLinkedStack a)
test03  = cs test03'
  where
    test03' : {a : Set} @$\rightarrow$@ a @$\rightarrow$@ SingleLinkedStack a
    test03' a = goto pushSingleLinkedStack (emptySingleLinkedStack , a , (cs id))


lemma : {A : Set} {a : A} @$\rightarrow$@ goto (test03 ◎ test02 ◎ test01) a @$\equiv$@ False
lemma = refl


n-push : {A : Set} {a : A} @$\rightarrow$@ CodeSegment (@$\mathbb{N}$@  @$\times$@ SingleLinkedStack A) (@$\mathbb{N}$@ @$\times$@ SingleLinkedStack A)
n-push {A} {a} = cs (push {A} {a})
  where
    push : {A : Set} {a : A} @$\rightarrow$@ (@$\mathbb{N}$@ @$\times$@ SingleLinkedStack A) @$\rightarrow$@ (@$\mathbb{N}$@ @$\times$@ SingleLinkedStack A)
    push {A} {a} (zero  , s) = (zero , s)
    push {A} {a} (suc n , s) = goto pushSingleLinkedStack (s , a , {!!} {- n-push -}) -- needs subtype


{-

n-push : {A : Set} {a : A} @$\rightarrow$@ Nat @$\rightarrow$@ SingleLinkedStack A @$\rightarrow$@ SingleLinkedStack A
n-push zero s            = s
n-push {A} {a} (suc n) s = pushSingleLinkedStack (n-push {A} {a} n s) a (\s @$\rightarrow$@ s)

n-pop : {A : Set} {a : A} @$\rightarrow$@ Nat @$\rightarrow$@ SingleLinkedStack A @$\rightarrow$@ SingleLinkedStack A
n-pop zero    s         = s
n-pop {A} {a} (suc n) s = popSingleLinkedStack (n-pop {A} {a} n s) (\s _ @$\rightarrow$@ s)

open @$\equiv$@-Reasoning

push-pop-equiv : {A : Set} {a : A} (s : SingleLinkedStack A) @$\rightarrow$@ popSingleLinkedStack (pushSingleLinkedStack s a (\s @$\rightarrow$@ s)) (\s _ @$\rightarrow$@ s) @$\equiv$@ s
push-pop-equiv s = refl

push-and-n-pop : {A : Set} {a : A} (n : Nat) (s : SingleLinkedStack A) @$\rightarrow$@ n-pop {A} {a} (suc n) (pushSingleLinkedStack s a id) @$\equiv$@ n-pop {A} {a} n s
push-and-n-pop zero s            = refl
push-and-n-pop {A} {a} (suc n) s = begin
  n-pop (suc (suc n)) (pushSingleLinkedStack s a id)
  @$\equiv$@@$\langle$@ refl @$\rangle$@
  popSingleLinkedStack (n-pop (suc n) (pushSingleLinkedStack s a id)) (\s _ @$\rightarrow$@ s)
  @$\equiv$@@$\langle$@ cong (\s @$\rightarrow$@ popSingleLinkedStack s (\s _ @$\rightarrow$@ s)) (push-and-n-pop n s) @$\rangle$@
  popSingleLinkedStack (n-pop n s) (\s _ @$\rightarrow$@ s)
  @$\equiv$@@$\langle$@ refl @$\rangle$@
  n-pop (suc n) s
  @$\blacksquare$@


n-push-pop-equiv : {A : Set} {a : A} (n : Nat) (s : SingleLinkedStack A) @$\rightarrow$@ (n-pop {A} {a} n (n-push {A} {a} n s)) @$\equiv$@ s
n-push-pop-equiv zero s            = refl
n-push-pop-equiv {A} {a} (suc n) s = begin
  n-pop (suc n) (n-push (suc n) s)
  @$\equiv$@@$\langle$@ refl @$\rangle$@
  n-pop (suc n) (pushSingleLinkedStack (n-push n s) a (\s @$\rightarrow$@ s))
  @$\equiv$@@$\langle$@ push-and-n-pop n (n-push n s)  @$\rangle$@
  n-pop n (n-push n s)
  @$\equiv$@@$\langle$@ n-push-pop-equiv n s @$\rangle$@
  s
  @$\blacksquare$@


n-push-pop-equiv-empty : {A : Set} {a : A} @$\rightarrow$@ (n : Nat) @$\rightarrow$@ n-pop {A} {a} n (n-push {A} {a} n emptySingleLinkedStack)  @$\equiv$@ emptySingleLinkedStack
n-push-pop-equiv-empty n = n-push-pop-equiv n emptySingleLinkedStack
-}