Mercurial > hg > Gears > GearsAgda
changeset 428:ff4ab9add959
fix findNode
| author | ryokka |
|---|---|
| date | Sat, 07 Oct 2017 19:00:22 +0900 |
| parents | 07ccd411ad70 |
| children | 54352ed97f34 |
| files | src/parallel_execution/RedBlackTree.agda |
| diffstat | 1 files changed, 4 insertions(+), 1 deletions(-) [+] |
line wrap: on
line diff
--- a/src/parallel_execution/RedBlackTree.agda Sat Oct 07 18:22:31 2017 +0900 +++ b/src/parallel_execution/RedBlackTree.agda Sat Oct 07 19:00:22 2017 +0900 @@ -44,12 +44,15 @@ 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 = next (record tree { root = just 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 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 = } }) insertNode tree datum next = get2 (stack tree) (\ s d1 d2 -> insertCase1 ( record { root = root tree; stack = s }) datum d1 d2 next)