Mercurial > hg > GearsTemplate

changeset 498:01f0a2cdcc43

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Merge
author Tatsuki IHA <innparusu@cr.ie.u-ryukyu.ac.jp>
date Mon, 01 Jan 2018 06:38:13 +0900
parents 809974b25ecb (current diff) 8e133a3938c0 (diff)
children 2c125aa7a577
files
diffstat 1 files changed, 56 insertions(+), 56 deletions(-) [+]
line wrap: on
line diff
--- a/src/parallel_execution/stack.agda	Mon Jan 01 06:37:29 2018 +0900
+++ b/src/parallel_execution/stack.agda	Mon Jan 01 06:38:13 2018 +0900
@@ -1,27 +1,27 @@
-module stack where
+open import Level renaming (suc to succ )
+module stack  where
 
 open import Relation.Binary.PropositionalEquality
 open import Relation.Binary.Core
 open import Data.Nat
-open import Level renaming (suc to succ ; zero to Zero)
 
 ex : 1 + 2 ≡ 3
 ex = refl
 
-data Bool : Set where
+data Bool {n : Level } : Set (succ n) where
   True  : Bool
   False : Bool
 
-record _∧_ {a b : Set} : Set where
+record _∧_ {n : Level } {a b : Set n} : Set n where
   field
     pi1 : a
     pi2 : b
 
-data Maybe (a : Set) : Set  where
+data Maybe {n : Level } (a : Set n) : Set n where
   Nothing : Maybe a
   Just    : a -> Maybe a
 
-record Stack {a t : Set} (stackImpl : Set) : Set  where
+record Stack {n : Level } {a : Set n } {t : Set (succ n) }(stackImpl : Set n ) : Set (succ n ) where
   field
     stack : stackImpl
     push : stackImpl -> a -> (stackImpl -> t) -> t
@@ -31,35 +31,35 @@
     get2 : stackImpl -> (stackImpl -> Maybe a -> Maybe a -> t) -> t
 open Stack
 
-pushStack : {a t si : Set} -> Stack si -> a -> (Stack si -> t) -> t
-pushStack {a} {t} s0 d next = push s0 (stack s0) d (\s1 -> next (record s0 {stack = s1} ))
+pushStack : {n : Level } {t : Set (succ n)} {a si : Set n}  -> Stack si -> a -> (Stack si -> t) -> t
+pushStack {t} {a} s0 d next = push s0 (stack s0) d (\s1 -> next (record s0 {stack = s1} ))
 
-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 )
+popStack : {n : Level } { t : Set (succ n)} {a si : Set n} -> Stack si -> (Stack si -> Maybe a  -> t) -> t
+popStack {t} {a} s0  next = pop s0 (stack s0) (\s1 d1 -> next (record s0 {stack = s1}) d1 )
 
-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)
+pop2Stack : {n : Level } { t : Set (succ n)} { a  si : Set n} -> Stack si -> (Stack si -> Maybe a -> Maybe a -> t) -> t
+pop2Stack {t} {a} 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 )
+getStack : {n : Level } {t : Set (succ n)} {a  si : Set n} -> Stack si -> (Stack si -> Maybe a  -> t) -> t
+getStack {t} {a} 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)
+get2Stack : {n : Level } {t : Set (succ n)} {a  si : Set n} -> Stack si -> (Stack si -> Maybe a -> Maybe a -> t) -> t
+get2Stack {t} {a} s0 next = get2 s0 (stack s0) (\s1 d1 d2 -> next (record s0 {stack = s1}) d1 d2)
 
 
-data Element (a : Set) : Set where
+data Element {n : Level } (a : Set n) : Set n where
   cons : a -> Maybe (Element a) -> Element a
 
-datum : {a : Set} -> Element a -> a
+datum : {n : Level } {a : Set n} -> Element a -> a
 datum (cons a _) = a
 
-next : {a : Set} -> Element a -> Maybe (Element a)
+next : {n : Level } {a : Set n} -> Element a -> 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 (suc l) where
+record Element {l : Level} (a : Set n l) : Set n (suc l) where
   field
     datum : a  -- `data` is reserved by Agda.
     next : Maybe (Element a)
@@ -67,19 +67,19 @@
 
 
 
-record SingleLinkedStack (a : Set) : Set where
+record SingleLinkedStack {n : Level } (a : Set n) : Set n where
   field
     top : Maybe (Element a)
 open SingleLinkedStack
 
-pushSingleLinkedStack : {Data t : Set} -> SingleLinkedStack Data -> Data -> (Code : SingleLinkedStack Data -> t) -> t
+pushSingleLinkedStack : {n : Level } {t : Set (succ n) } {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 : {a t : Set} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t
+popSingleLinkedStack : {n : Level } {t : Set (succ n) } {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,40 +87,40 @@
     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)
+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)
 ...                                | 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' : {n : Level } {t : Set (succ n) }  -> 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 : {n : Level } {t : Set (succ n) } {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 : {a t : Set} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> (Maybe a) -> t) -> t
-get2SingleLinkedStack {a} stack cs with (top stack)
+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)
 ...                                | Nothing = cs stack Nothing Nothing
 ...                                | Just d = get2SingleLinkedStack' stack cs
   where
-    get2SingleLinkedStack' : {t : Set} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> (Maybe a) -> t) -> t
+    get2SingleLinkedStack' : {n : Level} {t : Set (succ n) } -> 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))
 
 
 
-emptySingleLinkedStack : {a : Set} -> SingleLinkedStack a
+emptySingleLinkedStack : {n : Level } {a : Set n} -> SingleLinkedStack a
 emptySingleLinkedStack = record {top = Nothing}
 
-createSingleLinkedStack : {a b : Set} -> Stack {a} {b} (SingleLinkedStack a)
+createSingleLinkedStack : {n : Level } {t : Set (succ n) } {a : Set n} -> Stack {n} {a} {t} (SingleLinkedStack a)
 createSingleLinkedStack = record { stack = emptySingleLinkedStack
                                  ; push = pushSingleLinkedStack
                                  ; pop  = popSingleLinkedStack
@@ -130,19 +130,19 @@
                                  }
 
 
-test01 : {a : Set} -> SingleLinkedStack a -> Maybe a -> Bool
+test01 : {n : Level } {a : Set n} -> SingleLinkedStack a -> Maybe a -> Bool
 test01 stack _ with (top stack)
 ...                  | (Just _) = True
 ...                  | Nothing  = False
 
 
-test02 : {a : Set} -> SingleLinkedStack a -> Bool
-test02 stack = (popSingleLinkedStack stack) test01
+test02 : {n : Level } {a : Set n} -> SingleLinkedStack a -> Bool
+test02 stack = popSingleLinkedStack stack test01
 
-test03 : {a : Set} -> a ->  Bool
+test03 : {n : Level } {a : Set n} -> a ->  Bool
 test03 v = pushSingleLinkedStack emptySingleLinkedStack v test02
 
-testStack01 : {a : Set} -> a -> Bool
+testStack01 : {n : Level } {a : Set n} -> a -> Bool
 testStack01 v = pushStack createSingleLinkedStack v (
    \s -> popStack s (\s1 d1 -> True))
 
@@ -166,49 +166,49 @@
 testStack04 : Bool
 testStack04 = testStack02 (\s -> testStack03 s testStack032)
 
-testStack05 : Set
-testStack05 = testStack04 ≡ True
+testStack05 : { n : Level} -> Set n
+testStack05 = {!!} -- testStack04 ≡ True
 
 
-lemma : {A : Set} {a : A} -> test03 a ≡ False
+lemma : {n : Level} {A : Set n} {a : A} -> test03 a ≡ False
 lemma = refl
 
-id : {A : Set} -> A -> A
+id : {n : Level} {A : Set n} -> A -> A
 id a = a
 
 
-n-push : {A : Set} {a : A} -> ℕ -> SingleLinkedStack A -> SingleLinkedStack A
+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 -> s)
+n-push {_} {A} {a} (suc n) s = {!!} -- pushSingleLinkedStack (n-push {_} {A} {a} n s) a (\s -> ?)
 
-n-pop : {A : Set} {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 : {A : Set} {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 : {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 : {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 {A} {a} (suc (suc n)) (pushSingleLinkedStack s a id)
+push-and-n-pop {_} {A} {a} (suc n) s = begin
+   {!!} -- n-pop {_} {n} {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 _ -> s)) (push-and-n-pop n s) ⟩ 
-  popSingleLinkedStack (n-pop {A} {a} n s) (\s _ -> s)
+   {!!} -- 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)
   ≡⟨ refl ⟩
-  n-pop {A} {a} (suc n) s
+    {!!} -- n-pop {_} {n} {A} {a} (suc n) 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 : {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)
   ≡⟨ 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-push-pop-equiv n s ⟩
@@ -216,5 +216,5 @@
   ∎
 
 
-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 : Level} {A : Set n} {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