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!$\prime$!
  where
    test01!$\prime$! : {a : Set} !$\rightarrow$! (SingleLinkedStack a !$\times$! Maybe a) !$\rightarrow$! Bool
    test01!$\prime$! (record { top = Nothing } , _) = False
    test01!$\prime$! (record { top = Just x } ,  _)  = True


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


test03 : {a : Set} !$\rightarrow$! CodeSegment a (SingleLinkedStack a)
test03  = cs test03!$\prime$!
  where
    test03!$\prime$! : {a : Set} !$\rightarrow$! a !$\rightarrow$! SingleLinkedStack a
    test03!$\prime$! 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
-}