# HG changeset patch
# User ryokka
# Date 1534411328 -32400
# Node ID 70b09cbefd451dfd6c2339ff136f1a7bc2ec3de8
# Parent  8777baeb90f86d80c11ae3d13befe8cfe07ea65a
add queue.agda

diff -r 8777baeb90f8 -r 70b09cbefd45 queue.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/queue.agda	Thu Aug 16 18:22:08 2018 +0900
@@ -0,0 +1,122 @@
+open import Level renaming (suc to succ ; zero to Zero )
+module Queue where
+
+open import Relation.Binary.PropositionalEquality
+open import Relation.Binary.Core
+open import Data.Nat
+
+data Maybe {n : Level } (a : Set n) : Set n where
+  Nothing : Maybe a
+  Just    : a -> Maybe a
+
+data Bool {n : Level }: Set n where
+  True : Bool
+  False : Bool
+
+
+record QueueMethods {n m : Level} (a : Set n) {t : Set m} (queueImpl : Set n) : Set (m Level.⊔ n) where
+  field
+    put   : queueImpl -> a -> (queueImpl -> t) -> t
+    take  : queueImpl -> (queueImpl -> Maybe a -> t) -> t
+    clear : queueImpl -> (queueImpl -> t) -> t
+open QueueMethods
+
+record Queue {n m : Level} (a : Set n) {t : Set m} (qu : Set n) : Set (m Level.⊔ n) where
+  field
+    queue : qu
+    queueMethods : QueueMethods {n} {m} a {t} qu
+  putQueue : a -> (Queue a qu -> t) -> t
+  putQueue a next = put (queueMethods) (queue) a (\q1 -> next record {queue = q1 ; queueMethods = queueMethods})
+  takeQueue : (Queue a qu -> Maybe a -> t) -> t
+  takeQueue next = take (queueMethods) (queue) (\q1 d1 -> next record {queue = q1 ; queueMethods = queueMethods} d1)
+  clearQueue : (Queue a qu -> t) -> t
+  clearQueue next = clear (queueMethods) (queue) (\q1 -> next record {queue = q1 ; queueMethods = queueMethods})
+open Queue
+
+
+
+record Element {n : Level} (a : Set n) : Set n where
+  inductive
+  constructor cons
+  field
+    datum : a  -- `data` is reserved by Agda.
+    next : Maybe (Element a)
+open Element
+
+
+record SingleLinkedQueue {n : Level} (a : Set n) : Set n where
+  field
+    top : Maybe (Element a)
+    last : Maybe (Element a)
+open SingleLinkedQueue
+
+
+{-# TERMINATING #-}
+reverseElement : {n : Level} {a : Set n} -> Element a -> Maybe (Element a) -> Element a
+reverseElement el Nothing with next el
+... | Just el1 = reverseElement el1 (Just rev)
+  where
+    rev = cons (datum el) Nothing
+... | Nothing = el
+reverseElement el (Just el0) with next el
+... | Just el1 = reverseElement el1 (Just (cons (datum el) (Just el0)))
+... | Nothing = (cons (datum el) (Just el0))
+
+
+{-# TERMINATING #-}
+putSingleLinkedQueue : {n m : Level} {t : Set m} {a : Set n} -> SingleLinkedQueue a -> a -> (Code : SingleLinkedQueue a -> t) -> t
+putSingleLinkedQueue queue a cs with top queue
+... | Just te = cs queue1
+  where
+    re = reverseElement te Nothing
+    ce = cons a (Just re)
+    commit = reverseElement ce Nothing
+    queue1 = record queue {top = Just commit}
+... | Nothing = cs queue1
+  where
+    cel = record {datum = a ; next = Nothing}
+    queue1 = record {top = Just cel ; last = Just cel}
+
+{-# TERMINATING #-}
+takeSingleLinkedQueue : {n m : Level} {t : Set m} {a : Set n} -> SingleLinkedQueue a -> (Code : SingleLinkedQueue a -> (Maybe a) -> t) -> t
+takeSingleLinkedQueue queue cs with (top queue)
+... | Just te = cs record {top = (next te) ; last = Just (lastElement te)} (Just (datum te))
+  where
+    lastElement : {n : Level} {a : Set n} -> Element a -> Element a
+    lastElement el with next el
+    ... | Just el1 = lastElement el1
+    ... | Nothing = el
+... | Nothing = cs queue Nothing
+
+clearSingleLinkedQueue : {n m : Level} {t : Set m} {a : Set n} -> SingleLinkedQueue a -> (SingleLinkedQueue a -> t) -> t
+clearSingleLinkedQueue queue cs = cs (record {top = Nothing ; last = Nothing})
+
+
+emptySingleLinkedQueue : {n : Level} {a : Set n} -> SingleLinkedQueue a
+emptySingleLinkedQueue = record {top = Nothing ; last = Nothing}
+
+singleLinkedQueueSpec : {n m : Level } {t : Set m } {a : Set n} -> QueueMethods {n} {m} a {t} (SingleLinkedQueue a)
+singleLinkedQueueSpec = record {
+                                    put = putSingleLinkedQueue
+                                  ; take  = takeSingleLinkedQueue
+                                  ; clear = clearSingleLinkedQueue
+                                }
+
+
+createSingleLinkedQueue : {n m : Level} {t : Set m} {a : Set n} -> Queue {n} {m} a {t} (SingleLinkedQueue a)
+createSingleLinkedQueue = record {
+  queue = emptySingleLinkedQueue ;
+  queueMethods = singleLinkedQueueSpec
+  }
+
+
+check1 = putSingleLinkedQueue emptySingleLinkedQueue 1 (\q1 -> putSingleLinkedQueue q1 2 (\q2 -> putSingleLinkedQueue q2 3 (\q3 -> putSingleLinkedQueue q3 4 (\q4 -> putSingleLinkedQueue q4 5 (\q5 -> q5)))))
+
+
+check2 = putSingleLinkedQueue emptySingleLinkedQueue 1 (\q1 -> putSingleLinkedQueue q1 2 (\q2 -> putSingleLinkedQueue q2 3 (\q3 -> putSingleLinkedQueue q3 4 (\q4 -> takeSingleLinkedQueue q4 (\q d -> q)))))
+
+
+test01 : {n : Level } {a : Set n} -> SingleLinkedQueue a -> Maybe a -> Bool {n}
+test01 queue _ with (top queue)
+...                  | (Just _) = True
+...                  | Nothing  = False
diff -r 8777baeb90f8 -r 70b09cbefd45 redBlackTreeTest.agda
--- a/redBlackTreeTest.agda	Sun May 06 19:35:38 2018 +0900
+++ b/redBlackTreeTest.agda	Thu Aug 16 18:22:08 2018 +0900
@@ -52,19 +52,19 @@
 test2 = refl
 
 open ≡-Reasoning
-test3 : putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero}) 1 1 
+test3 : putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ {Set Level.zero}) 1 1
     $ λ t → putTree1 t 2 2
     $ λ t → putTree1 t 3 3
-    $ λ t → putTree1 t 4 4    
+    $ λ t → putTree1 t 4 4
     $ λ t → getRedBlackTree t 1
-    $ λ t x → check2 x 1 ≡ True  
+    $ λ t x → check2 x 1 ≡ True
 test3 = begin
     check2 (Just (record {key = 1 ; value = 1 ; color = Black ; left = Nothing ; right = Just (leafNode 2 2)})) 1
   ≡⟨ refl ⟩
     True
   ∎
 
-test31 = putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ ) 1 1 
+test31 = putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ ) 1 1
     $ λ t → putTree1 t 2 2
     $ λ t → putTree1 t 3 3
     $ λ t → putTree1 t 4 4
@@ -72,11 +72,11 @@
     $ λ t x → x
 
 -- test5 : Maybe (Node ℕ ℕ)
-test5 = putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ ) 4 4 
+test5 = putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ ) 4 4
     $ λ t → putTree1 t 6 6
     $ λ t0 →  clearSingleLinkedStack (nodeStack t0)
     $ λ s → findNode1 t0 s (leafNode 3 3) ( root t0 )
-    $ λ t1 s n1 → replaceNode t1 s n1 
+    $ λ t1 s n1 → replaceNode t1 s n1
     $ λ t → getRedBlackTree t 3
     -- $ λ t x → SingleLinkedStack.top (stack s)
     -- $ λ t x → n1
@@ -103,7 +103,7 @@
     value1 = 1
 
 test8 : Maybe (Node ℕ ℕ)
-test8 = putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ) 1 1 
+test8 = putTree1 {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ) 1 1
     $ λ t → putTree1 t 2 2 (λ  t → root t)
 
 
@@ -116,19 +116,19 @@
     λ t x → check2 x 1 ≡ True   )))
 test10 = refl
 
-test11 = putRedBlackTree {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ) 1 1 
+test11 = putRedBlackTree {_} {_} {ℕ} {ℕ} (createEmptyRedBlackTreeℕ ℕ) 1 1
     $ λ t → putRedBlackTree t 2 2
     $ λ t → putRedBlackTree t 3 3
     $ λ t → getRedBlackTree t 2
     $ λ t x → root t
 
 
-redBlackInSomeState :{ m : Level } (a : Set Level.zero) (n : Maybe (Node a ℕ)) {t : Set m} → RedBlackTree {Level.zero} {m} {t} a ℕ 
+redBlackInSomeState :{ m : Level } (a : Set Level.zero) (n : Maybe (Node a ℕ)) {t : Set m} → RedBlackTree {Level.zero} {m} {t} a ℕ
 redBlackInSomeState {m} a n {t} = record { root = n ; nodeStack = emptySingleLinkedStack ; compare = compareT }
 
 
 compTri :  ( x y : ℕ ) ->  Tri  (x < y) ( x ≡ y )  ( x > y )
-compTri = IsStrictTotalOrder.compare (Relation.Binary.StrictTotalOrder.isStrictTotalOrder strictTotalOrder) 
+compTri = IsStrictTotalOrder.compare (Relation.Binary.StrictTotalOrder.isStrictTotalOrder strictTotalOrder)
    where open import  Relation.Binary
 
 checkT : {m : Level } (n : Maybe (Node  ℕ ℕ)) → ℕ → Bool {m}
@@ -174,10 +174,12 @@
 putTest1 : (n : Maybe (Node ℕ ℕ))
          → (k : ℕ) (x : ℕ)
          → putTree1 {_} {_} {ℕ} {ℕ} (redBlackInSomeState {_} ℕ n {Set Level.zero}) k x
-           (λ  t → getRedBlackTree t k (λ  t x1 → checkT x1 x  ≡ True)) 
+           (λ  t → getRedBlackTree t k (λ  t x1 → checkT x1 x  ≡ True))
 putTest1 n k x with n
 ...  | Just n1 = lemma0
    where
+     upelem : (eleN : Element (Node ℕ ℕ)) -> (Node ℕ ℕ)
+     upelem eleN = n1
      tree0 : (s : SingleLinkedStack (Node ℕ ℕ) ) → RedBlackTree ℕ ℕ
      tree0 s = record { root = Just n1 ; nodeStack = s ; compare = compareT }
      lemma2 : (s : SingleLinkedStack (Node ℕ ℕ) ) → StackTreeInvariant (leafNode k x) s (tree0 s)
@@ -185,15 +187,15 @@
               (λ  t → getRedBlackTree t k (λ  t x1 → checkT x1 x  ≡ True)))
      lemma2 s STI with compTri k (key n1)
      ... |  tri≈ le refl gt = lemma5 s ( tree0 s ) n1
-        where 
+        where
            lemma5 :  (s : SingleLinkedStack (Node ℕ ℕ) )  → ( t :  RedBlackTree  ℕ ℕ  ) → ( n :  Node ℕ ℕ  ) → popSingleLinkedStack ( record { top = Just (cons n (SingleLinkedStack.top s)) }  )
-                   ( \ s1  _ -> (replaceNode (tree0 s1) s1 (record n1 { key = k ; value = x } ) (λ t → 
+                   ( \ s1  _ -> (replaceNode (tree0 s1) s1 (record n1 { key = k ; value = x } ) (λ t →
                       GetRedBlackTree.checkNode t (key n1) (λ t₁ x1 → checkT x1 x ≡ True) (root t))) )
            lemma5 s t n with (top s)
            ...          | Just n2  with compTri k k
            ...            | tri< _ neq _ =  ⊥-elim (neq refl)
            ...            | tri> _ neq _ =  ⊥-elim (neq refl)
-           ...            | tri≈  _ refl _  =  ⊥-elim ( (notInStack STI)  {!!} )
+           ...            | tri≈  _ refl _  =  ⊥-elim (notInStack STI ({!!}))
            lemma5 s t n | Nothing with compTri k k
            ...            | tri≈  _ refl _  = checkEQ x _ refl
            ...            | tri< _ neq _ =  ⊥-elim (neq refl)
@@ -203,12 +205,12 @@
      lemma0 : clearSingleLinkedStack (record {top = Nothing}) (\s → findNode (tree0 s) s (leafNode k x) n1 (λ  tree1 s n1 → replaceNode tree1 s n1
               (λ  t → getRedBlackTree t k (λ  t x1 → checkT x1 x  ≡ True))))
      lemma0 = lemma2 (record {top = Nothing}) ( record { sti = {!!}  ; notInStack = {!!} } )
-...  | Nothing = lemma1  
-   where 
+...  | Nothing = lemma1
+   where
      lemma1 : getRedBlackTree {_} {_} {ℕ} {ℕ} {Set Level.zero} ( record {  root = Just ( record {
                key   = k ; value = x ; right = Nothing ; left  = Nothing ; color = Red } ) ; nodeStack = record { top = Nothing } ; compare = λ x₁ y → compareT x₁ y  } ) k
-        ( λ  t x1 → checkT x1 x  ≡ True) 
-     lemma1 with compTri k k 
+        ( λ  t x1 → checkT x1 x  ≡ True)
+     lemma1 with compTri k k
      ... | tri≈  _ refl _ = checkEQ x _ refl
      ... | tri< _ neq _ =  ⊥-elim (neq refl)
      ... | tri> _ neq _ =  ⊥-elim (neq refl)
diff -r 8777baeb90f8 -r 70b09cbefd45 stack.agda
--- a/stack.agda	Sun May 06 19:35:38 2018 +0900
+++ b/stack.agda	Thu Aug 16 18:22:08 2018 +0900
@@ -25,7 +25,7 @@
   Nothing : Maybe a
   Just    : a -> Maybe a
 
-record StackMethods {n m : Level } (a : Set n ) {t : Set m }(stackImpl : Set n ) : Set (m Level.⊔ n) where
+record StackMethods {n m : Level } (a : Set n ) {t : Set m } (stackImpl : Set n ) : Set (m Level.⊔ n) where
   field
     push : stackImpl -> a -> (stackImpl -> t) -> t
     pop  : stackImpl -> (stackImpl -> Maybe a -> t) -> t