Mercurial > hg > Papers > 2019 > oshiro-thesis

comparison final_main/src/AgdaTreeImpl.agda.replaced @ 0:83f997abf3b5

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
first commit
author e155702
date Thu, 14 Feb 2019 16:51:50 +0900
parents
children
comparison
equal deleted inserted replaced
-1:000000000000 0:83f997abf3b5
1 record TreeMethods {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.@$\sqcup$@ n) where
2 field
3 putImpl : treeImpl @$\rightarrow$@ a @$\rightarrow$@ (treeImpl @$\rightarrow$@ t) @$\rightarrow$@ t
4 getImpl : treeImpl @$\rightarrow$@ (treeImpl @$\rightarrow$@ Maybe a @$\rightarrow$@ t) @$\rightarrow$@ t
5 open TreeMethods
6
7 record Tree {n m : Level } {a : Set n } {t : Set m } (treeImpl : Set n ) : Set (m Level.@$\sqcup$@ n) where
8 field
9 tree : treeImpl
10 treeMethods : TreeMethods {n} {m} {a} {t} treeImpl
11 putTree : a @$\rightarrow$@ (Tree treeImpl @$\rightarrow$@ t) @$\rightarrow$@ t
12 putTree d next = putImpl (treeMethods ) tree d (\t1 @$\rightarrow$@ next (record {tree = t1 ; treeMethods = treeMethods} ))
13 getTree : (Tree treeImpl @$\rightarrow$@ Maybe a @$\rightarrow$@ t) @$\rightarrow$@ t
14 getTree next = getImpl (treeMethods ) tree (\t1 d @$\rightarrow$@ next (record {tree = t1 ; treeMethods = treeMethods} ) d )
15 open Tree
16
17 record Node {n : Level } (a k : Set n) : Set n where
18 inductive
19 field
20 key : k
21 value : a
22 right : Maybe (Node a k)
23 left : Maybe (Node a k)
24 color : Color {n}
25 open Node
26
27 leafNode : {n : Level } {a k : Set n} @$\rightarrow$@ k @$\rightarrow$@ a @$\rightarrow$@ Node a k
28 leafNode k1 value = record {
29 key = k1 ;
30 value = value ;
31 right = Nothing ;
32 left = Nothing ;
33 color = Red
34 }
35 record RedBlackTree {n m : Level } {t : Set m} (a k : Set n) : Set (m Level.@$\sqcup$@ n) where
36 field
37 root : Maybe (Node a k)
38 nodeStack : SingleLinkedStack (Node a k)
39 compare : k @$\rightarrow$@ k @$\rightarrow$@ CompareResult {n}
40 open RedBlackTree
41
42 putRedBlackTree : {n m : Level } {a k : Set n} {t : Set m} @$\rightarrow$@ RedBlackTree {n} {m} {t} a k @$\rightarrow$@ k @$\rightarrow$@ a @$\rightarrow$@ (RedBlackTree {n} {m} {t} a k @$\rightarrow$@ t) @$\rightarrow$@ t
43 putRedBlackTree {n} {m} {a} {k} {t} tree k1 value next with (root tree)
44 ... | Nothing = next (record tree {root = Just (leafNode k1 value) })
45 ... | Just n2 = clearSingleLinkedStack (nodeStack tree) (\ s @$\rightarrow$@ findNode tree s (leafNode k1 value) n2 (\ tree1 s n1 @$\rightarrow$@ insertNode tree1 s n1 next))
46
47 -- 以下省略