Mercurial > hg > Gears > GearsAgda

changeset 499:2c125aa7a577

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
stack.agda leveled
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 01 Jan 2018 09:34:46 +0900
parents 01f0a2cdcc43
children 6d984ea42fd2
files src/parallel_execution/stack.agda
diffstat 1 files changed, 42 insertions(+), 39 deletions(-) [+]
line wrap: on
line diff
--- a/src/parallel_execution/stack.agda	Mon Jan 01 06:38:13 2018 +0900
+++ b/src/parallel_execution/stack.agda	Mon Jan 01 09:34:46 2018 +0900
@@ -1,4 +1,4 @@
-open import Level renaming (suc to succ )
+open import Level renaming (suc to succ ; zero to Zero )
 module stack  where
 
 open import Relation.Binary.PropositionalEquality
@@ -21,7 +21,7 @@
   Nothing : Maybe a
   Just    : a -> Maybe a
 
-record Stack {n : Level } {a : Set n } {t : Set (succ n) }(stackImpl : Set n ) : Set (succ n ) where
+record Stack {n m : Level } {a : Set n } {t : Set m }(stackImpl : Set n ) : Set (m Level.⊔ n) where
   field
     stack : stackImpl
     push : stackImpl -> a -> (stackImpl -> t) -> t
@@ -72,14 +72,14 @@
     top : Maybe (Element a)
 open SingleLinkedStack
 
-pushSingleLinkedStack : {n : Level } {t : Set (succ n) } {Data : Set n} -> SingleLinkedStack Data -> Data -> (Code : SingleLinkedStack Data -> t) -> t
+pushSingleLinkedStack : {n m : Level } {t : Set m } {Data : Set n} -> SingleLinkedStack Data -> Data -> (Code : SingleLinkedStack Data -> t) -> t
 pushSingleLinkedStack stack datum next = next stack1
   where
     element = cons datum (top stack)
     stack1  = record {top = Just element}
 
 
-popSingleLinkedStack : {n : Level } {t : Set (succ n) } {a  : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t
+popSingleLinkedStack : {n m : Level } {t : Set m } {a  : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t
 popSingleLinkedStack stack cs with (top stack)
 ...                                | Nothing = cs stack  Nothing
 ...                                | Just d  = cs stack1 (Just data1)
@@ -87,30 +87,30 @@
     data1  = datum d
     stack1 = record { top = (next d) }
 
-pop2SingleLinkedStack : {n : Level } {t : Set (succ n) } {a  : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> (Maybe a) -> t) -> t
-pop2SingleLinkedStack {n} {t} {a} stack cs with (top stack)
+pop2SingleLinkedStack : {n m : Level } {t : Set m } {a  : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> (Maybe a) -> t) -> t
+pop2SingleLinkedStack {n} {m} {t} {a} stack cs with (top stack)
 ...                                | Nothing = cs stack Nothing Nothing
-...                                | Just d = pop2SingleLinkedStack' stack cs
+...                                | Just d = pop2SingleLinkedStack' {n} {m} stack cs
   where
-    pop2SingleLinkedStack' : {n : Level } {t : Set (succ n) }  -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> (Maybe a) -> t) -> t
+    pop2SingleLinkedStack' : {n m : Level } {t : Set m }  -> 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 : {n : Level } {t : Set (succ n) } {a  : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t
+getSingleLinkedStack : {n m : Level } {t : Set m } {a  : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t
 getSingleLinkedStack stack cs with (top stack)
 ...                                | Nothing = cs stack  Nothing
 ...                                | Just d  = cs stack (Just data1)
   where
     data1  = datum d
 
-get2SingleLinkedStack : {n : Level } {t : Set (succ n) } {a  : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> (Maybe a) -> t) -> t
-get2SingleLinkedStack {_} {t} {a} stack cs with (top stack)
+get2SingleLinkedStack : {n m : Level } {t : Set m } {a  : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> (Maybe a) -> t) -> t
+get2SingleLinkedStack {n} {m} {t} {a} stack cs with (top stack)
 ...                                | Nothing = cs stack Nothing Nothing
-...                                | Just d = get2SingleLinkedStack' stack cs
+...                                | Just d = get2SingleLinkedStack' {n} {m} stack cs
   where
-    get2SingleLinkedStack' : {n : Level} {t : Set (succ n) } -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> (Maybe a) -> t) -> t
+    get2SingleLinkedStack' : {n m : Level} {t : Set m } -> 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))
@@ -120,7 +120,7 @@
 emptySingleLinkedStack : {n : Level } {a : Set n} -> SingleLinkedStack a
 emptySingleLinkedStack = record {top = Nothing}
 
-createSingleLinkedStack : {n : Level } {t : Set (succ n) } {a : Set n} -> Stack {n} {a} {t} (SingleLinkedStack a)
+createSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> Stack {n} {m} {a} {t} (SingleLinkedStack a)
 createSingleLinkedStack = record { stack = emptySingleLinkedStack
                                  ; push = pushSingleLinkedStack
                                  ; pop  = popSingleLinkedStack
@@ -130,7 +130,7 @@
                                  }
 
 
-test01 : {n : Level } {a : Set n} -> SingleLinkedStack a -> Maybe a -> Bool
+test01 : {n : Level } {a : Set n} -> SingleLinkedStack a -> Maybe a -> Bool {n}
 test01 stack _ with (top stack)
 ...                  | (Just _) = True
 ...                  | Nothing  = False
@@ -142,6 +142,12 @@
 test03 : {n : Level } {a : Set n} -> a ->  Bool
 test03 v = pushSingleLinkedStack emptySingleLinkedStack v test02
 
+-- after a push and a pop, the stack is empty
+lemma : {n : Level} {A : Set n} {a : A} -> test03 a ≡ False
+lemma = refl
+
+-- after push 1 and 2, pop2 get 1 and 2
+
 testStack01 : {n : Level } {a : Set n} -> a -> Bool
 testStack01 v = pushStack createSingleLinkedStack v (
    \s -> popStack s (\s1 d1 -> True))
@@ -151,11 +157,11 @@
    \s -> pushStack s 2 cs)
 
 
-testStack031 : (d1 d2 : ℕ ) -> Bool
+testStack031 : (d1 d2 : ℕ ) -> Bool {Zero}
 testStack031 1 2 = True
 testStack031 _ _ = False
 
-testStack032 : (d1 d2 : Maybe ℕ) -> Bool
+testStack032 : (d1 d2 : Maybe ℕ) -> Bool {Zero}
 testStack032  (Just d1) (Just d2) = testStack031 d1 d2
 testStack032  _ _ = False
 
@@ -166,53 +172,50 @@
 testStack04 : Bool
 testStack04 = testStack02 (\s -> testStack03 s testStack032)
 
-testStack05 : { n : Level} -> Set n
-testStack05 = {!!} -- testStack04 ≡ True
-
-
-lemma : {n : Level} {A : Set n} {a : A} -> test03 a ≡ False
-lemma = refl
+testStack05 : Set (succ Zero)
+testStack05 = testStack04 ≡ True
 
 id : {n : Level} {A : Set n} -> A -> A
 id a = a
 
+-- push a, n times
 
 n-push : {n : Level} {A : Set n} {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 -> ?)
+n-push {l} {A} {a} (suc n) s = pushSingleLinkedStack (n-push {l} {A} {a} n s) a (\s -> s ) 
 
-n-pop : {n : Level} {A : Set n} {a : A} -> ℕ -> SingleLinkedStack A -> SingleLinkedStack A
+n-pop :  {n : Level}{A : Set n} {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)
+n-pop  {_} {A} {a} (suc n) s = popSingleLinkedStack (n-pop {_} {A} {a} n s) (\s _ -> s )
 
 open ≡-Reasoning
 
-push-pop-equiv : {n : Level} {A : Set n} {a : A} (s : SingleLinkedStack A) -> {!!} -- popSingleLinkedStack (pushSingleLinkedStack s a (\s -> s)) (\s _ -> s) ≡ s
+push-pop-equiv : {n : Level} {A : Set n} {a : A} (s : SingleLinkedStack A) -> (popSingleLinkedStack (pushSingleLinkedStack s a (\s -> s)) (\s _ -> s) ) ≡ s
 push-pop-equiv s = refl
 
-push-and-n-pop : {n : Level} {A : Set n} {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 : {n : Level} {A : Set n} {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 {_} {n} {A} {a} (suc (suc n)) (pushSingleLinkedStack s a id)
+   n-pop {_} {A} {a} (suc (suc n)) (pushSingleLinkedStack s a id)
   ≡⟨ refl ⟩
-   {!!} -- popSingleLinkedStack (n-pop {_} {A} {a} (suc n) (pushSingleLinkedStack s a id)) (\s _ -> s)
-  ≡⟨ cong (\s -> popSingleLinkedStack s (\s _ -> {!!})) (push-and-n-pop n s) ⟩ 
-   {!!}  -- popSingleLinkedStack (n-pop {_} {n} {A} {a} n s) (\s _ -> s)
+   popSingleLinkedStack (n-pop {_} {A} {a} (suc n) (pushSingleLinkedStack s a id)) (\s _ -> s)
+  ≡⟨ cong (\s -> popSingleLinkedStack s (\s _ -> s )) (push-and-n-pop n s) ⟩ 
+   popSingleLinkedStack (n-pop {_} {A} {a} n s) (\s _ -> s)
   ≡⟨ refl ⟩
-    {!!} -- n-pop {_} {n} {A} {a} (suc n) s
+    n-pop {_} {A} {a} (suc n) s
   ∎
   
 
-n-push-pop-equiv : {n : Level} {A : Set n} {a : A} (n : ℕ) (s : SingleLinkedStack A) -> {!!} -- (n-pop {A} {a} n (n-push {A} {a} n s)) ≡ s
+n-push-pop-equiv : {n : Level} {A : Set n} {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)
+n-push-pop-equiv {_} {A} {a} (suc n) s = begin
+    n-pop {_} {A} {a} (suc n) (n-push (suc n) s)
   ≡⟨ refl ⟩
-  {!!} -- n-pop {A} {a} (suc n) (pushSingleLinkedStack (n-push n s) a (\s -> s))
+    n-pop {_} {A} {a} (suc n) (pushSingleLinkedStack (n-push n s) a (\s -> s))
   ≡⟨ push-and-n-pop n (n-push n s)  ⟩
-  n-pop {A} {a} n (n-push n s)
+    n-pop {_} {A} {a} n (n-push n s)
   ≡⟨ n-push-pop-equiv n s ⟩
-  s
+    s
   ∎