# HG changeset patch
# User Tatsuki IHA <innparusu@cr.ie.u-ryukyu.ac.jp>
# Date 1514543304 -32400
# Node ID ef965008bef140dd93701f87d94d4f4e7fad5338
# Parent  1861e41aa96a8db59d49f91bfaa38523feb3f38b# Parent  a7548f01f013576813708de5392dbb88947f1483
Merge

diff -r 1861e41aa96a -r ef965008bef1 src/parallel_execution/stack.agda
--- a/src/parallel_execution/stack.agda	Fri Dec 29 18:49:13 2017 +0900
+++ b/src/parallel_execution/stack.agda	Fri Dec 29 19:28:24 2017 +0900
@@ -12,10 +12,10 @@
   True  : Bool
   False : Bool
 
--- equal : {a : Set} -> a -> a -> Bool
--- equal x y with x ≡ y
--- equal x .x | refl = True
--- equal _ _ | _ = False
+record _∧_ {a b : Set} : Set where
+  field
+    pi1 : a
+    pi2 : b
 
 data Maybe (a : Set) : Set  where
   Nothing : Maybe a
@@ -117,20 +117,6 @@
 
 
 
--- get2SingleLinkedStack : {a t : Set} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> (Maybe a) -> t) -> t
--- get2SingleLinkedStack stack cs with (top stack)
--- ...                                | Nothing = cs stack  Nothing
--- ...                                | Just d  = get2 cs stack
---    where
---      get2 : SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t
---      get2 stack cs with (next d)
--- ...                    | Nothing = cs stack Nothing
--- ...                    | Just d d1 = cs stack (Just data1) (just data2)
---                          where
---                            data1  = datum d
---                            data2  = datum d1
-
-
 emptySingleLinkedStack : {a : Set} -> SingleLinkedStack a
 emptySingleLinkedStack = record {top = Nothing}
 
@@ -160,20 +146,29 @@
 testStack01 v = pushStack createSingleLinkedStack v (
    \s -> popStack s (\s1 d1 -> True))
 
-testStack02 : {t : Set} -> (Stack (SingleLinkedStack ℕ) -> t) -> t
+testStack02 : (Stack (SingleLinkedStack ℕ) -> Bool) -> Bool
 testStack02 cs = pushStack createSingleLinkedStack 1 (
    \s -> pushStack s 2 cs)
 
-testStack031 : {d1 d2 : ℕ } -> d1 ≡ 1 -> d2 ≡ 2 -> Bool
-testStack031 refl refl = True
+
+testStack031 : (d1 d2 : ℕ ) -> Bool
+testStack031 1 2 = True
+testStack031 _ _ = False
+
+testStack032 : (d1 d2 : Maybe ℕ) -> Bool
+testStack032  (Just d1) (Just d2) = testStack031 d1 d2
+testStack032  _ _ = False
 
-testStack032 : (d1 d2 : Maybe ℕ) -> {!!}
-testStack032 (Just d1) (Just d2) = testStack031 {d1} {d2} {!!} {!!}
-testStack032 _ _ = False
+testStack03 : Stack (SingleLinkedStack ℕ) -> ((Maybe ℕ) -> (Maybe ℕ) -> Bool ) -> Bool
+testStack03 s cs = pop2Stack s (
+   \s d1 d2 -> cs d1 d2 )
 
-testStack03 : {t : Set} -> Stack (SingleLinkedStack ℕ) -> {!!}
-testStack03 s = pop2Stack s (
-   \s d1 d2 -> testStack032 d1 d2 )
+testStack04 : Bool
+testStack04 = testStack02 (\s -> testStack03 s testStack032)
+
+testStack05 : Set
+testStack05 = testStack04 ≡ True
+
 
 lemma : {A : Set} {a : A} -> test03 a ≡ False
 lemma = refl