Mercurial > hg > Gears > GearsAgda
view hoareRedBlackTree.agda @ 581:09e9e8fd7568
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sat, 02 Nov 2019 19:23:10 +0900 |
parents | 99429fdb3b8b |
children | 1a5dd71199f1 |
line wrap: on
line source
module hoareRedBlackTree where open import Level hiding (zero) open import Data.Nat hiding (compare) open import Data.Nat.Properties as NatProp open import Data.Maybe -- open import Data.Bool open import Data.Empty open import Data.List open import Relation.Binary open import Relation.Binary.PropositionalEquality open import logic 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 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 SingleLinkedStack = List emptySingleLinkedStack : {n : Level } {Data : Set n} -> SingleLinkedStack Data emptySingleLinkedStack = [] pushSingleLinkedStack : {n m : Level } {t : Set m } {Data : Set n} -> List Data -> Data -> (Code : SingleLinkedStack Data -> t) -> t pushSingleLinkedStack stack datum next = next ( datum ∷ stack ) popSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t popSingleLinkedStack [] cs = cs [] nothing popSingleLinkedStack (data1 ∷ s) cs = cs s (just data1) data Color {n : Level } : Set n where Red : Color Black : Color record Node {n : Level } (a : Set n) : Set n where inductive field key : ℕ value : a right : Maybe (Node a ) left : Maybe (Node a ) color : Color {n} open Node record RedBlackTree {n : Level } (a : Set n) : Set n where field root : Maybe (Node a ) nodeStack : SingleLinkedStack (Node a ) -- compare : k → k → Tri A B C -- <-cmp open RedBlackTree ---- -- find node potition to insert or to delete, the path will be in the stack -- {-# TERMINATING #-} findNode : {n m : Level } {a : Set n} {t : Set m} → RedBlackTree {n} a → (Node a ) → (RedBlackTree {n} a → t) → t findNode {n} {m} {a} {t} tree n0 next with root tree findNode {n} {m} {a} {t} tree n0 next | nothing = next tree findNode {n} {m} {a} {t} tree n0 next | just x with <-cmp (key x) (key n0) findNode {n} {m} {a} {t} tree n0 next | just x | tri≈ ¬a b ¬c = next tree findNode {n} {m} {a} {t} tree n0 next | just x | tri< a₁ ¬b ¬c = pushSingleLinkedStack (nodeStack tree) x (λ s → findNode (record {root = (left x) ; nodeStack = s}) n0 next) findNode {n} {m} {a} {t} tree n0 next | just x | tri> ¬a ¬b c = pushSingleLinkedStack (nodeStack tree) x (λ s → findNode (record {root = (right x) ; nodeStack = s}) n0 next) findNode1 : {n m : Level } {a : Set n} {t : Set m} → RedBlackTree {n} a → (Node a ) → (RedBlackTree {n} a → t) → t findNode1 {n} {m} {a} {t} tree n0 next = findNode2 (root tree) (nodeStack tree) module FindNode where findNode2 : (Maybe (Node a )) → SingleLinkedStack (Node a ) → t findNode2 nothing st = next record { root = nothing ; nodeStack = st } findNode2 (just x) st with <-cmp (key n0) (key x) ... | tri≈ ¬a b ¬c = next (record {root = just x ; nodeStack = st }) ... | tri< a ¬b ¬c = pushSingleLinkedStack st x (λ s1 → findNode2 (right x) s1) ... | tri> ¬a ¬b c = pushSingleLinkedStack st x (λ s1 → findNode2 (left x) s1) node001 : Node ℕ node001 = record { key = 2 ; value = 3 ; left = nothing ; right = nothing ; color = Black } node002 : Node ℕ node002 = record { key = 1 ; value = 3 ; left = just node001 ; right = nothing ; color = Black } node003 : Node ℕ node003 = record { key = 0 ; value = 3 ; left = just node002 ; right = nothing ; color = Black } test001 = findNode1 {Level.zero} {Level.zero} {ℕ} {RedBlackTree ℕ} ( record { root = nothing ; nodeStack = emptySingleLinkedStack } ) node001 ( λ tree → tree ) test002 = findNode1 {Level.zero} {Level.zero} {ℕ} {RedBlackTree ℕ} ( record { root = just node001 ; nodeStack = emptySingleLinkedStack } ) node001 ( λ tree → tree ) test003 = findNode1 {Level.zero} {Level.zero} {ℕ} {RedBlackTree ℕ} ( record { root = just node003 ; nodeStack = emptySingleLinkedStack } ) node001 ( λ tree → tree ) test004 = findNode {Level.zero} {Level.zero} {ℕ} {RedBlackTree ℕ} ( record { root = just node003 ; nodeStack = emptySingleLinkedStack } ) node001 ( λ tree → tree ) createEmptyRedBlackTreeℕ : {n m : Level} {t : Set m} (a : Set n) (b : ℕ) → RedBlackTree {n} a createEmptyRedBlackTreeℕ a b = record { root = nothing ; nodeStack = emptySingleLinkedStack } findNodeLeft : {n : Level } {a : Set n} (r : Node a ) (t : SingleLinkedStack (Node a)) → Set n findNodeLeft x [] = (left x ≡ nothing ) ∧ (right x ≡ nothing ) findNodeLeft {n} x (h ∷ t) = Lift n ((key x) < (key h)) findNodeRight : {n : Level } {a : Set n} (r : Node a ) (t : SingleLinkedStack (Node a)) → Set n findNodeRight x [] = (left x ≡ nothing ) ∧ (right x ≡ nothing ) findNodeRight {n} x (h ∷ t) = Lift n ((key x) > (key h)) data FindNodeInvariant {n : Level } {a : Set n} : (t : SingleLinkedStack (Node a)) (original : RedBlackTree {n} a ) → Set n where fni-Top : (now : RedBlackTree {n} a ) → FindNodeInvariant [] now fni-Left : (x : Node a) (t : SingleLinkedStack (Node a)) (original : RedBlackTree {n} a ) → FindNodeInvariant ( x ∷ t ) original → findNodeLeft x t → FindNodeInvariant t original fni-Right : (x : Node a) (t : SingleLinkedStack (Node a)) (original : RedBlackTree {n} a ) → FindNodeInvariant ( x ∷ t ) original → findNodeRight x t → FindNodeInvariant t original findNode1h : {n m : Level } {a : Set n} {t : Set m} → (tree : RedBlackTree {n} a ) → (Node a ) → ( FindNodeInvariant (nodeStack tree) tree) → ((new : RedBlackTree {n} a) → FindNodeInvariant (nodeStack new) tree → t ) → t findNode1h {n} {m} {a} {t} tree n0 prev next = findNode2h (root tree) (nodeStack tree) prev module FindNodeH where findNode2h : (Maybe (Node a )) → (s : SingleLinkedStack (Node a )) → FindNodeInvariant s tree → t findNode2h nothing st prev = next record { root = nothing ; nodeStack = st } {!!} -- ( fni-Last ? ) findNode2h (just x) st prev with <-cmp (key n0) (key x) ... | tri≈ ¬a b ¬c = next (record {root = just x ; nodeStack = st }) {!!} -- ( fni-Last ? ) ... | tri< a ¬b ¬c = pushSingleLinkedStack st x (λ s1 → findNode2h (right x) s1 (fni-Left x s1 tree {!!} {!!}) ) ... | tri> ¬a ¬b c = pushSingleLinkedStack st x (λ s1 → findNode2h (left x) s1 (fni-Right x s1 tree {!!} {!!}) )