Mercurial > hg > Gears > Gears

changeset 484:8a22cfd174bf

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
pop2 and get2 in agda
author ryokka
date Fri, 29 Dec 2017 18:29:01 +0900
parents 9098ec0a9e6b
children a7548f01f013 747dd4ba7b44
files src/parallel_execution/stack.agda
diffstat 1 files changed, 52 insertions(+), 21 deletions(-) [+]
line wrap: on
line diff
--- a/src/parallel_execution/stack.agda	Fri Dec 29 11:07:18 2017 +0900
+++ b/src/parallel_execution/stack.agda	Fri Dec 29 18:29:01 2017 +0900
@@ -2,11 +2,11 @@
 
 open import Relation.Binary.PropositionalEquality
 open import Relation.Binary.Core
-
+open import Data.Nat
+open import Level renaming (suc to succ ; zero to Zero)
 
-data Nat : Set where
-  zero : Nat
-  suc  : Nat -> Nat
+ex : 1 + 2 ≡ 3
+ex = refl
 
 data Bool : Set where
   True  : Bool
@@ -26,8 +26,9 @@
     stack : stackImpl
     push : stackImpl -> a -> (stackImpl -> t) -> t
     pop  : stackImpl -> (stackImpl -> Maybe a -> t) -> t
+    pop2 : stackImpl -> (stackImpl -> Maybe a -> Maybe a -> t) -> t
     get  : stackImpl -> (stackImpl -> Maybe a -> t) -> t
-    -- get2 : stackImpl -> (stackImpl -> (Maybe a -> Maybe a) -> t) -> t
+    get2 : stackImpl -> (stackImpl -> Maybe a -> Maybe a -> t) -> t
 open Stack
 
 pushStack : {a t si : Set} -> Stack si -> a -> (Stack si -> t) -> t
@@ -36,8 +37,14 @@
 popStack : {a t si : Set} -> Stack si -> (Stack si -> Maybe a  -> t) -> t
 popStack {a} {t} s0  next = pop s0 (stack s0) (\s1 d1 -> next (record s0 {stack = s1}) d1 )
 
--- get : {a t si : Set} -> Stack si -> (Stack si -> t) -> t
--- get {a} {t} s0 next = pop s0 (stack s0) (\s1 -> next (record s0 {}))
+pop2Stack : {a t si : Set} -> Stack si -> (Stack si -> Maybe a -> Maybe a -> t) -> t
+pop2Stack {a} {t} s0 next = pop2 s0 (stack s0) (\s1 d1 d2 -> next (record s0 {stack = s1}) d1 d2)
+
+getStack : {a t si : Set} -> Stack si -> (Stack si -> Maybe a  -> t) -> t
+getStack {a} {t} s0 next = get s0 (stack s0) (\s1 d1 -> next (record s0 {stack = s1}) d1 )
+
+get2Stack : {a t si : Set} -> Stack si -> (Stack si -> Maybe a -> Maybe a -> t) -> t
+get2Stack {a} {t} s0 next = get2 s0 (stack s0) (\s1 d1 d2 -> next (record s0 {stack = s1}) d1 d2)
 
 
 data Element (a : Set) : Set where
@@ -80,6 +87,17 @@
     data1  = datum d
     stack1 = record { top = (next d) }
 
+pop2SingleLinkedStack : {a t : Set} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> (Maybe a) -> t) -> t
+pop2SingleLinkedStack {a} stack cs with (top stack)
+...                                | Nothing = cs stack Nothing Nothing
+...                                | Just d = pop2SingleLinkedStack' stack cs
+  where
+    pop2SingleLinkedStack' : {t : Set} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> (Maybe a) -> t) -> t
+    pop2SingleLinkedStack' stack cs with (next d)
+    ...              | Nothing = cs stack Nothing Nothing
+    ...              | Just d1 = cs (record {top = (next d)}) (Just (datum d)) (Just (datum d1))
+    
+
 getSingleLinkedStack : {a t : Set} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t
 getSingleLinkedStack stack cs with (top stack)
 ...                                | Nothing = cs stack  Nothing
@@ -88,17 +106,15 @@
     data1  = datum d
 
 get2SingleLinkedStack : {a t : Set} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> (Maybe a) -> t) -> t
-get2SingleLinkedStack stack cs with (top stack)
+get2SingleLinkedStack {a} stack cs with (top stack)
 ...                                | Nothing = cs stack Nothing Nothing
-...                                | Just d = (getSingleLinkedStack2' stack cs)  Nothing
+...                                | Just d = get2SingleLinkedStack' stack cs
   where
-    getSingleLinkedStack2' : {a t : Set} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t
-    getSingleLinkedStack2' stack cs with (next d)
-    ...              | Nothing = cs stack Nothing
-    ...              | Just d1 = cs stack (Just data1 data2)
-         where
-           data1 = datum d
-           data2 = datum d1
+    get2SingleLinkedStack' : {t : Set} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> (Maybe a) -> t) -> t
+    get2SingleLinkedStack' stack cs with (next d)
+    ...              | Nothing = cs stack Nothing Nothing
+    ...              | Just d1 = cs stack (Just (datum d)) (Just (datum d1))
+
 
 
 -- get2SingleLinkedStack : {a t : Set} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> (Maybe a) -> t) -> t
@@ -122,7 +138,9 @@
 createSingleLinkedStack = record { stack = emptySingleLinkedStack
                                  ; push = pushSingleLinkedStack
                                  ; pop  = popSingleLinkedStack
+                                 ; pop2 = pop2SingleLinkedStack
                                  ; get  = getSingleLinkedStack
+                                 ; get2 = get2SingleLinkedStack
                                  }
 
 
@@ -142,7 +160,20 @@
 testStack01 v = pushStack createSingleLinkedStack v (
    \s -> popStack s (\s1 d1 -> True))
 
+testStack02 : {t : Set} -> (Stack (SingleLinkedStack ℕ) -> t) -> t
+testStack02 cs = pushStack createSingleLinkedStack 1 (
+   \s -> pushStack s 2 cs)
 
+testStack031 : {d1 d2 : ℕ } -> d1 ≡ 1 -> d2 ≡ 2 -> Bool
+testStack031 refl refl = True
+
+testStack032 : (d1 d2 : Maybe ℕ) -> {!!}
+testStack032 (Just d1) (Just d2) = testStack031 {d1} {d2} {!!} {!!}
+testStack032 _ _ = False
+
+testStack03 : {t : Set} -> Stack (SingleLinkedStack ℕ) -> {!!}
+testStack03 s = pop2Stack s (
+   \s d1 d2 -> testStack032 d1 d2 )
 
 lemma : {A : Set} {a : A} -> test03 a ≡ False
 lemma = refl
@@ -151,11 +182,11 @@
 id a = a
 
 
-n-push : {A : Set} {a : A} -> Nat -> SingleLinkedStack A -> SingleLinkedStack A
+n-push : {A : Set} {a : A} -> ℕ -> SingleLinkedStack A -> SingleLinkedStack A
 n-push zero s            = s
 n-push {A} {a} (suc n) s = pushSingleLinkedStack (n-push {A} {a} n s) a (\s -> s)
 
-n-pop : {A : Set} {a : A} -> Nat -> SingleLinkedStack A -> SingleLinkedStack A
+n-pop : {A : Set} {a : A} -> ℕ -> SingleLinkedStack A -> SingleLinkedStack A
 n-pop zero    s         = s
 n-pop {A} {a} (suc n) s = popSingleLinkedStack (n-pop {A} {a} n s) (\s _ -> s)
 
@@ -164,7 +195,7 @@
 push-pop-equiv : {A : Set} {a : A} (s : SingleLinkedStack A) -> popSingleLinkedStack (pushSingleLinkedStack s a (\s -> s)) (\s _ -> s) ≡ s
 push-pop-equiv s = refl
 
-push-and-n-pop : {A : Set} {a : A} (n : Nat) (s : SingleLinkedStack A) -> n-pop {A} {a} (suc n) (pushSingleLinkedStack s a id) ≡ n-pop {A} {a} n s
+push-and-n-pop : {A : Set} {a : A} (n : ℕ) (s : SingleLinkedStack A) -> n-pop {A} {a} (suc n) (pushSingleLinkedStack s a id) ≡ 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 {A} {a} (suc (suc n)) (pushSingleLinkedStack s a id)
@@ -177,7 +208,7 @@
   ∎
   
 
-n-push-pop-equiv : {A : Set} {a : A} (n : Nat) (s : SingleLinkedStack A) -> (n-pop {A} {a} n (n-push {A} {a} n s)) ≡ s
+n-push-pop-equiv : {A : Set} {a : A} (n : ℕ) (s : SingleLinkedStack A) -> (n-pop {A} {a} n (n-push {A} {a} n s)) ≡ s
 n-push-pop-equiv zero s            = refl
 n-push-pop-equiv {A} {a} (suc n) s = begin
   n-pop {A} {a} (suc n) (n-push (suc n) s)
@@ -190,5 +221,5 @@
   ∎
 
 
-n-push-pop-equiv-empty : {A : Set} {a : A} -> (n : Nat) -> n-pop {A} {a} n (n-push {A} {a} n emptySingleLinkedStack)  ≡ emptySingleLinkedStack
+n-push-pop-equiv-empty : {A : Set} {a : A} -> (n : ℕ) -> n-pop {A} {a} n (n-push {A} {a} n emptySingleLinkedStack)  ≡ emptySingleLinkedStack
 n-push-pop-equiv-empty n = n-push-pop-equiv n emptySingleLinkedStack