--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/stack.agda.replaced	Tue Sep 08 18:38:08 2020 +0900
@@ -0,0 +1,149 @@
+open import Level renaming (suc to succ ; zero to Zero )
+module stack  where
+
+open import Relation.Binary.PropositionalEquality
+open import Relation.Binary.Core
+open import Data.Nat
+
+ex : 1 + 2 @$\equiv$@ 3
+ex = refl
+
+data Bool {n : Level } : Set n where
+  True  : Bool
+  False : Bool
+
+record _@$\wedge$@_ {n : Level } (a : Set n) (b : Set n): Set n where
+  field
+    pi1 : a
+    pi2 : b
+
+data Maybe {n : Level } (a : Set n) : Set n where
+  Nothing : Maybe a
+  Just    : a @$\rightarrow$@ Maybe a
+
+record StackMethods {n m : Level } (a : Set n ) {t : Set m }(stackImpl : Set n ) : Set (m Level.@$\sqcup$@ n) where
+  field
+    push : stackImpl @$\rightarrow$@ a @$\rightarrow$@ (stackImpl @$\rightarrow$@ t) @$\rightarrow$@ t
+    pop  : stackImpl @$\rightarrow$@ (stackImpl @$\rightarrow$@ Maybe a @$\rightarrow$@ t) @$\rightarrow$@ t
+    pop2 : stackImpl @$\rightarrow$@ (stackImpl @$\rightarrow$@ Maybe a @$\rightarrow$@ Maybe a @$\rightarrow$@ t) @$\rightarrow$@ t
+    get  : stackImpl @$\rightarrow$@ (stackImpl @$\rightarrow$@ Maybe a @$\rightarrow$@ t) @$\rightarrow$@ t
+    get2 : stackImpl @$\rightarrow$@ (stackImpl @$\rightarrow$@ Maybe a @$\rightarrow$@ Maybe a @$\rightarrow$@ t) @$\rightarrow$@ t
+    clear : stackImpl @$\rightarrow$@ (stackImpl @$\rightarrow$@ t) @$\rightarrow$@ t
+open StackMethods
+
+record Stack {n m : Level } (a : Set n ) {t : Set m } (si : Set n ) : Set (m Level.@$\sqcup$@ n) where
+  field
+    stack : si
+    stackMethods : StackMethods {n} {m} a {t} si
+  pushStack :  a @$\rightarrow$@ (Stack a si @$\rightarrow$@ t) @$\rightarrow$@ t
+  pushStack d next = push (stackMethods ) (stack ) d (\s1 @$\rightarrow$@ next (record {stack = s1 ; stackMethods = stackMethods } ))
+  popStack : (Stack a si @$\rightarrow$@ Maybe a  @$\rightarrow$@ t) @$\rightarrow$@ t
+  popStack next = pop (stackMethods ) (stack ) (\s1 d1 @$\rightarrow$@ next (record {stack = s1 ; stackMethods = stackMethods }) d1 )
+  pop2Stack :  (Stack a si @$\rightarrow$@ Maybe a @$\rightarrow$@ Maybe a @$\rightarrow$@ t) @$\rightarrow$@ t
+  pop2Stack next = pop2 (stackMethods ) (stack ) (\s1 d1 d2 @$\rightarrow$@ next (record {stack = s1 ; stackMethods = stackMethods }) d1 d2)
+  getStack :  (Stack a si @$\rightarrow$@ Maybe a  @$\rightarrow$@ t) @$\rightarrow$@ t
+  getStack next = get (stackMethods ) (stack ) (\s1 d1 @$\rightarrow$@ next (record {stack = s1 ; stackMethods = stackMethods }) d1 )
+  get2Stack :  (Stack a si @$\rightarrow$@ Maybe a @$\rightarrow$@ Maybe a @$\rightarrow$@ t) @$\rightarrow$@ t
+  get2Stack next = get2 (stackMethods ) (stack ) (\s1 d1 d2 @$\rightarrow$@ next (record {stack = s1 ; stackMethods = stackMethods }) d1 d2)
+  clearStack : (Stack a si @$\rightarrow$@ t) @$\rightarrow$@ t
+  clearStack next = clear (stackMethods ) (stack ) (\s1 @$\rightarrow$@ next (record {stack = s1 ; stackMethods = stackMethods } ))
+
+open Stack
+
+{--
+data Element {n : Level } (a : Set n) : Set n where
+  cons : a @$\rightarrow$@ Maybe (Element a) @$\rightarrow$@ Element a
+
+
+datum : {n : Level } {a : Set n} @$\rightarrow$@ Element a @$\rightarrow$@ a
+datum (cons a _) = a
+
+next : {n : Level } {a : Set n} @$\rightarrow$@ Element a @$\rightarrow$@ Maybe (Element a)
+next (cons _ n) = n
+--}
+
+
+-- cannot define recrusive record definition. so use linked list with maybe.
+record Element {l : Level} (a : Set l) : Set l where
+  inductive
+  constructor cons
+  field
+    datum : a  -- `data` is reserved by Agda.
+    next : Maybe (Element a)
+
+open Element
+
+
+record SingleLinkedStack {n : Level } (a : Set n) : Set n where
+  field
+    top : Maybe (Element a)
+open SingleLinkedStack
+
+pushSingleLinkedStack : {n m : Level } {t : Set m } {Data : Set n} @$\rightarrow$@ SingleLinkedStack Data @$\rightarrow$@ Data @$\rightarrow$@ (Code : SingleLinkedStack Data @$\rightarrow$@ t) @$\rightarrow$@ t
+pushSingleLinkedStack stack datum next = next stack1
+  where
+    element = cons datum (top stack)
+    stack1  = record {top = Just element}
+
+
+popSingleLinkedStack : {n m : Level } {t : Set m } {a  : Set n} @$\rightarrow$@ SingleLinkedStack a @$\rightarrow$@ (Code : SingleLinkedStack a @$\rightarrow$@ (Maybe a) @$\rightarrow$@ t) @$\rightarrow$@ t
+popSingleLinkedStack stack cs with (top stack)
+...                                | Nothing = cs stack  Nothing
+...                                | Just d  = cs stack1 (Just data1)
+  where
+    data1  = datum d
+    stack1 = record { top = (next d) }
+
+pop2SingleLinkedStack : {n m : Level } {t : Set m } {a  : Set n} @$\rightarrow$@ SingleLinkedStack a @$\rightarrow$@ (Code : SingleLinkedStack a @$\rightarrow$@ (Maybe a) @$\rightarrow$@ (Maybe a) @$\rightarrow$@ t) @$\rightarrow$@ t
+pop2SingleLinkedStack {n} {m} {t} {a} stack cs with (top stack)
+...                                | Nothing = cs stack Nothing Nothing
+...                                | Just d = pop2SingleLinkedStack' {n} {m} stack cs
+  where
+    pop2SingleLinkedStack' : {n m : Level } {t : Set m }  @$\rightarrow$@ SingleLinkedStack a @$\rightarrow$@ (Code : SingleLinkedStack a @$\rightarrow$@ (Maybe a) @$\rightarrow$@ (Maybe a) @$\rightarrow$@ t) @$\rightarrow$@ t
+    pop2SingleLinkedStack' stack cs with (next d)
+    ...              | Nothing = cs stack Nothing Nothing
+    ...              | Just d1 = cs (record {top = (next d1)}) (Just (datum d)) (Just (datum d1))
+
+
+getSingleLinkedStack : {n m : Level } {t : Set m } {a  : Set n} @$\rightarrow$@ SingleLinkedStack a @$\rightarrow$@ (Code : SingleLinkedStack a @$\rightarrow$@ (Maybe a) @$\rightarrow$@ t) @$\rightarrow$@ t
+getSingleLinkedStack stack cs with (top stack)
+...                                | Nothing = cs stack  Nothing
+...                                | Just d  = cs stack (Just data1)
+  where
+    data1  = datum d
+
+get2SingleLinkedStack : {n m : Level } {t : Set m } {a  : Set n} @$\rightarrow$@ SingleLinkedStack a @$\rightarrow$@ (Code : SingleLinkedStack a @$\rightarrow$@ (Maybe a) @$\rightarrow$@ (Maybe a) @$\rightarrow$@ t) @$\rightarrow$@ t
+get2SingleLinkedStack {n} {m} {t} {a} stack cs with (top stack)
+...                                | Nothing = cs stack Nothing Nothing
+...                                | Just d = get2SingleLinkedStack' {n} {m} stack cs
+  where
+    get2SingleLinkedStack' : {n m : Level} {t : Set m } @$\rightarrow$@ SingleLinkedStack a @$\rightarrow$@ (Code : SingleLinkedStack a @$\rightarrow$@ (Maybe a) @$\rightarrow$@ (Maybe a) @$\rightarrow$@ t) @$\rightarrow$@ t
+    get2SingleLinkedStack' stack cs with (next d)
+    ...              | Nothing = cs stack Nothing Nothing
+    ...              | Just d1 = cs stack (Just (datum d)) (Just (datum d1))
+
+clearSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} @$\rightarrow$@ SingleLinkedStack a @$\rightarrow$@ (SingleLinkedStack a @$\rightarrow$@ t) @$\rightarrow$@ t
+clearSingleLinkedStack stack next = next (record {top = Nothing})
+
+
+emptySingleLinkedStack : {n : Level } {a : Set n} @$\rightarrow$@ SingleLinkedStack a
+emptySingleLinkedStack = record {top = Nothing}
+
+-----
+-- Basic stack implementations are specifications of a Stack
+--
+singleLinkedStackSpec : {n m : Level } {t : Set m } {a : Set n} @$\rightarrow$@ StackMethods {n} {m} a {t} (SingleLinkedStack a)
+singleLinkedStackSpec = record {
+                                   push = pushSingleLinkedStack
+                                 ; pop  = popSingleLinkedStack
+                                 ; pop2 = pop2SingleLinkedStack
+                                 ; get  = getSingleLinkedStack
+                                 ; get2 = get2SingleLinkedStack
+                                 ; clear = clearSingleLinkedStack
+                           }
+
+createSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} @$\rightarrow$@ Stack {n} {m} a {t} (SingleLinkedStack a)
+createSingleLinkedStack = record {
+                             stack = emptySingleLinkedStack ;
+                             stackMethods = singleLinkedStackSpec
+                           }