# HG changeset patch # User Tatsuki IHA # Date 1515063074 -32400 # Node ID d595acd16550c4351fb4652f27e0a21b84da17bc # Parent 62a77785cb2be0b10ea210b20f89e58e7def82b4# Parent 54ff7a97aec1c3c6ee7ca1741426907d28014fc6 Merge diff -r 62a77785cb2b -r d595acd16550 src/parallel_execution/RedBlackTree.agda --- a/src/parallel_execution/RedBlackTree.agda Thu Jan 04 19:50:46 2018 +0900 +++ b/src/parallel_execution/RedBlackTree.agda Thu Jan 04 19:51:14 2018 +0900 @@ -1,78 +1,99 @@ module RedBlackTree where open import stack +open import Level -record Tree {a t : Set} (treeImpl : Set) : Set where +record TreeMethods {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.⊔ n) where + field + putImpl : treeImpl -> a -> (treeImpl -> t) -> t + getImpl : treeImpl -> (treeImpl -> Maybe a -> t) -> t +open TreeMethods + +record Tree {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.⊔ n) where field tree : treeImpl - putImpl : treeImpl -> a -> (treeImpl -> t) -> t - getImpl : treeImpl -> (treeImpl -> Maybe a -> t) -> t + treeMethods : TreeMethods {n} {m} {a} {t} treeImpl + putTree : a -> (Tree treeImpl -> t) -> t + putTree d next = putImpl (treeMethods ) tree d (\t1 -> next (record {tree = t1 ; treeMethods = treeMethods} )) + getTree : (Tree treeImpl -> Maybe a -> t) -> t + getTree next = getImpl (treeMethods ) tree (\t1 d -> next (record {tree = t1 ; treeMethods = treeMethods} ) d ) open Tree - -putTree : {a t : Set} -> Tree -> a -> (Tree -> t) -> t -putTree {a} {t} t0 d next = (putImpl t0) (tree t0) d (\t1 -> next (record t0 {tree = t1} )) - -getTree : {a t : Set} -> Tree -> (Tree -> t) -> t -getTree {a} {t} t0 next = (getImpl t0) (tree t0) (\t1 -> next t0) - - -data Color : Set where +data Color {n : Level } : Set n where Red : Color Black : Color -record Node (a : Set) : Set where +data CompareResult {n : Level } : Set n where + LT : CompareResult + GT : CompareResult + EQ : CompareResult + +record Node {n : Level } (a k : Set n) : Set n where + inductive field - node : Element a - right : Maybe (Node a) - left : Maybe (Node a) - color : Color + key : k + value : a + right : Maybe (Node a k) + left : Maybe (Node a k) + color : Color {n} +open Node -record RedBlackTree (a : Set) : Set where +record RedBlackTree {n m : Level } {t : Set m} (a k si : Set n) : Set (m Level.⊔ n) where field - root : Maybe (Node a) - stack : Stack + root : Maybe (Node a k) + nodeStack : Stack {n} {m} (Node a k) {t} si + compare : k -> k -> CompareResult {n} open RedBlackTree -insertNode : ? -insertNode tree datum next = get2 (stack tree) (\ s d1 d2 -> insertCase1 ( record { root = root tree; stack = s }) datum d1 d2 next) +open Stack + -putRedBlackTree : {Data t : Set} -> RedBlackTree Data -> Data -> (Code : RedBlackTree Data -> t) -> t -putRedBlackTree tree datum next with (root tree) -... | Nothing = insertNode tree datum next -... | Just n = findNode tree datum n (\ tree1 -> insertNode tree1 datum next) - -findNode : {Data t : Set} -> RedBlackTree Data -> Data -> Node Data -> (Code : RedBlackTree Data (RedBlackTree Data -> t) -> t) -> t -findNode tree datum n next = pushStack (stack tree) n (\ s -> findNode1 (record tree {stack = s }) datum n next) +insertNode : {n m : Level } {t : Set m } {a k si : Set n} -> RedBlackTree {n} {m} {t} a k si -> Stack (Node a k) si -> Node a k -> (RedBlackTree {n} {m} {t} a k si -> t) -> t +insertNode tree s datum next = get2Stack s (\ s d1 d2 -> {!!} tree s datum d1 d2 next) -findNode1 : {Data t : Set} -> RedBlackTree Data -> Data -> Data -> (Code : RedBlackTree Data (RedBlackTree Data -> t) -> t) -> t -findNode1 tree datum n next with (compare datum n) -... | EQ = popStack (tree stack) (\s d -> findNode3 d (record tree { root = just (record n {node = datum}); stack = s }) next) -... | GT = findNode2 tree datum (right n) next -... | LT = findNode2 tree datum (left n) next +findNode : {n m : Level } {a k si : Set n} {t : Set m} -> RedBlackTree {n} {m} {t} a k si -> Stack (Node a k) si -> (Node a k) -> (Node a k) -> (RedBlackTree {n} {m} {t} a k si -> Stack (Node a k) si -> Node a k -> t) -> t +findNode {n} {m} {a} {k} {si} {t} tree s n0 n1 next = pushStack s n1 (\ s -> findNode1 s n1) where - findNode2 tree datum nothing next = insertNode tree datum next - findNode2 tree datum (just n) next = findNode (record tree {root = just n}) datum n next - findNode3 nothing tree next = next tree - findNode3 (just n) tree next = - popStack (tree stack) (\s d -> findNode3 d (record { root = record n {right = ? } })) + findNode2 : Stack (Node a k) si -> (Maybe (Node a k)) -> t + findNode2 s Nothing = next tree s n0 + findNode2 s (Just n) = findNode tree s n0 n next + findNode1 : Stack (Node a k) si -> (Node a k) -> t + findNode1 s n1 with (compare tree (key n0) (key n1)) + ... | EQ = next tree s n0 + ... | GT = findNode2 s (right n1) + ... | LT = findNode2 s (left n1) + where + -- findNode3 : Stack (Node a k) si -> (Maybe (Node a k)) -> t + -- findNode3 s nothing = next tree s n0 + -- findNode3 s (Just n) = + -- popStack (nodeStack tree) (\s d -> findNode3 s d) -insertCase1 tree datum nothing grandparent next = next (record { root = ?; stack = createSingleLinkedStack }) -insertCase1 tree datum (just parent) grandparent next = insertCase2 tree datum parent grandparent next - -insertCase2 tree datum parent grandparent next with (color parent) -... | Red = insertCase3 tree datum parent grandparent next -... | Black = next (record { root = ?; stack = createSingleLinkedStack }) +leafNode : {n m : Level } {a k si : Set n} {t : Set m} -> k -> a -> Node a k +leafNode k1 value = record { + key = k1 ; + value = value ; + right = Nothing ; + left = Nothing ; + color = Black + } -insertCase3 tree datum parent grandparent next +putRedBlackTree : {n m : Level } {a k si : Set n} {t : Set m} -> RedBlackTree {n} {m} {t} a k si -> k -> a -> (RedBlackTree {n} {m} {t} a k si -> t) -> t +putRedBlackTree {n} {m} {a} {k} {si} {t} tree k1 value next with (root tree) +... | Nothing = next (record tree {root = Just (leafNode k1 value) }) +... | Just n2 = findNode tree (nodeStack tree) (leafNode {n} {m} {a} {k} {si} {t} k1 value) n2 (\ tree1 s n1 -> insertNode tree1 s n1 next) -getRedBlackTree : {a t : Set} -> RedBlackTree a -> (Code : RedBlackTree a -> (Maybe a) -> t) -> t -getRedBlackTree tree cs with (root tree) -... | Nothing = cs tree Nothing -... | Just d = cs stack1 (Just data1) +getRedBlackTree : {n m : Level } {a k si : Set n} {t : Set m} -> RedBlackTree {n} {m} {t} a k si -> k -> (RedBlackTree {n} {m} {t} a k si -> (Maybe (Node a k)) -> t) -> t +getRedBlackTree {_} {_} {a} {k} {_} {t} tree k1 cs = checkNode (root tree) where - data1 = datum d - stack1 = record { root = (next d) } + checkNode : Maybe (Node a k) -> t + checkNode Nothing = cs tree Nothing + checkNode (Just n) = search n + where + search : Node a k -> t + search n with compare tree k1 (key n) + search n | LT = checkNode (left n) + search n | GT = checkNode (right n) + search n | EQ = cs tree (Just n) diff -r 62a77785cb2b -r d595acd16550 src/parallel_execution/stack.agda --- a/src/parallel_execution/stack.agda Thu Jan 04 19:50:46 2018 +0900 +++ b/src/parallel_execution/stack.agda Thu Jan 04 19:51:14 2018 +0900 @@ -21,7 +21,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 @@ -30,19 +30,19 @@ get2 : stackImpl -> (stackImpl -> Maybe a -> Maybe a -> t) -> t open StackMethods -record Stack {n m : Level } {a : Set n } {t : Set m } (si : Set n ) : Set (m Level.⊔ n) where +record Stack {n m : Level } (a : Set n ) {t : Set m } (si : Set n ) : Set (m Level.⊔ n) where field stack : si - stackMethods : StackMethods {n} {m} {a} {t} si - pushStack : a -> (Stack si -> t) -> t + stackMethods : StackMethods {n} {m} a {t} si + pushStack : a -> (Stack a si -> t) -> t pushStack d next = push (stackMethods ) (stack ) d (\s1 -> next (record {stack = s1 ; stackMethods = stackMethods } )) - popStack : (Stack si -> Maybe a -> t) -> t + popStack : (Stack a si -> Maybe a -> t) -> t popStack next = pop (stackMethods ) (stack ) (\s1 d1 -> next (record {stack = s1 ; stackMethods = stackMethods }) d1 ) - pop2Stack : (Stack si -> Maybe a -> Maybe a -> t) -> t + pop2Stack : (Stack a si -> Maybe a -> Maybe a -> t) -> t pop2Stack next = pop2 (stackMethods ) (stack ) (\s1 d1 d2 -> next (record {stack = s1 ; stackMethods = stackMethods }) d1 d2) - getStack : (Stack si -> Maybe a -> t) -> t + getStack : (Stack a si -> Maybe a -> t) -> t getStack next = get (stackMethods ) (stack ) (\s1 d1 -> next (record {stack = s1 ; stackMethods = stackMethods }) d1 ) - get2Stack : (Stack si -> Maybe a -> Maybe a -> t) -> t + get2Stack : (Stack a si -> Maybe a -> Maybe a -> t) -> t get2Stack next = get2 (stackMethods ) (stack ) (\s1 d1 d2 -> next (record {stack = s1 ; stackMethods = stackMethods }) d1 d2) open Stack @@ -95,7 +95,7 @@ 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)) + ... | Just d1 = cs (record {top = (next d1)}) (Just (datum d)) (Just (datum d1)) getSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t @@ -120,18 +120,28 @@ emptySingleLinkedStack : {n : Level } {a : Set n} -> SingleLinkedStack a emptySingleLinkedStack = record {top = Nothing} -createSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> Stack {n} {m} {a} {t} (SingleLinkedStack a) -createSingleLinkedStack = record { - stack = emptySingleLinkedStack ; - stackMethods = record { +----- +-- Basic stack implementations are specifications of a Stack +-- +singleLinkedStackSpec : {n m : Level } {t : Set m } {a : Set n} -> StackMethods {n} {m} a {t} (SingleLinkedStack a) +singleLinkedStackSpec = record { push = pushSingleLinkedStack ; pop = popSingleLinkedStack ; pop2 = pop2SingleLinkedStack ; get = getSingleLinkedStack ; get2 = get2SingleLinkedStack - } } +createSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> Stack {n} {m} a {t} (SingleLinkedStack a) +createSingleLinkedStack = record { + stack = emptySingleLinkedStack ; + stackMethods = singleLinkedStackSpec + } + +---- +-- +-- proof of properties ( concrete cases ) +-- test01 : {n : Level } {a : Set n} -> SingleLinkedStack a -> Maybe a -> Bool {n} test01 stack _ with (top stack) @@ -155,7 +165,7 @@ -- after push 1 and 2, pop2 get 1 and 2 -testStack02 : {m : Level } -> ( Stack (SingleLinkedStack ℕ) -> Bool {m} ) -> Bool {m} +testStack02 : {m : Level } -> ( Stack ℕ (SingleLinkedStack ℕ) -> Bool {m} ) -> Bool {m} testStack02 cs = pushStack createSingleLinkedStack 1 ( \s -> pushStack s 2 cs) @@ -168,7 +178,7 @@ testStack032 (Just d1) (Just d2) = testStack031 d1 d2 testStack032 _ _ = False -testStack03 : {m : Level } -> Stack (SingleLinkedStack ℕ) -> ((Maybe ℕ) -> (Maybe ℕ) -> Bool {m} ) -> Bool {m} +testStack03 : {m : Level } -> Stack ℕ (SingleLinkedStack ℕ) -> ((Maybe ℕ) -> (Maybe ℕ) -> Bool {m} ) -> Bool {m} testStack03 s cs = pop2Stack s ( \s d1 d2 -> cs d1 d2 ) @@ -180,23 +190,21 @@ ------ -- +-- proof of properties with indefinite state of stack +-- -- this should be proved by properties of the stack inteface, not only by the implementation, -- and the implementation have to provides the properties. -- --- we cannot write "s ≡ s3", since level of the Set does not fit , but we cant use stack s ≡ stack s3 +-- we cannot write "s ≡ s3", since level of the Set does not fit , but use stack s ≡ stack s3 is ok. +-- anyway some implementations may result s != s3 -- --- push->push->pop2 : {l : Level } {D : Set l} (x y : D ) (s : Stack (SingleLinkedStack D) ) -> --- pushStack s x ( \s1 -> pushStack s1 y ( \s2 -> pop2Stack s2 ( \s3 y1 x1 -> ((stack s ≡ stack s3 ) ∧ ( (Just x ≡ x1 ) ∧ (Just y ≡ y1 ) ) )))) --- push->push->pop2 {l} {D} x y s = {!!} --- where --- t0 : (s3 : Stack {_} {succ l} {D} {Set l} (SingleLinkedStack D)) (x1 y1 : Maybe D) -> (stack s ≡ stack s3 ) -> (Just x ≡ x1 ) -> (Just y ≡ y1 ) --- -> ((stack s ≡ stack s3 ) ∧ ( (Just x ≡ x1 ) ∧ (Just y ≡ y1 ) )) --- t0 s3 x1 y1 refl refl refl = record { pi1 = refl ; pi2 = record { pi1 = refl ; pi2 = refl } } --- t1 : (s2 : Stack (SingleLinkedStack D)) -> pop2Stack s2 ( \s3 y1 x1 -> ((stack s ≡ stack s3 ) ∧ ( (Just x ≡ x1 ) ∧ (Just y ≡ y1 ) ) )) --- t1 s2 = {!!} --- t2 : (s1 : Stack (SingleLinkedStack D)) (x1 y1 : Maybe D) -> --- pushStack s1 y ( \s2 -> pop2Stack s2 ( \s3 y1 x1 -> ((stack s ≡ stack s3 ) ∧ ( (Just x ≡ x1 ) ∧ (Just y ≡ y1 ) ) ) )) --- t2 s1 = {!!} + +stackInSomeState : {l m : Level } {D : Set l} {t : Set m } (s : SingleLinkedStack D ) -> Stack {l} {m} D {t} ( SingleLinkedStack D ) +stackInSomeState s = record { stack = s ; stackMethods = singleLinkedStackSpec } + +push->push->pop2 : {l : Level } {D : Set l} (x y : D ) (s : SingleLinkedStack D ) -> + pushStack ( stackInSomeState s ) x ( \s1 -> pushStack s1 y ( \s2 -> pop2Stack s2 ( \s3 y1 x1 -> (Just x ≡ x1 ) ∧ (Just y ≡ y1 ) ) )) +push->push->pop2 {l} {D} x y s = record { pi1 = refl ; pi2 = refl } id : {n : Level} {A : Set n} -> A -> A