Mercurial > hg > Gears > GearsAgda

comparison hoareBinaryTree.agda @ 596:4be84ddbf593

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author ryokka
date Thu, 16 Jan 2020 17:53:47 +0900
parents 0927df986552
children 89fd7cf09b2a
comparison
equal deleted inserted replaced
595:0927df986552 596:4be84ddbf593
64 64
65 -- 65 --
66 -- 66 --
67 -- no children , having left node , having right node , having both 67 -- no children , having left node , having right node , having both
68 -- 68 --
69 data bt' {n : Level} (A : Set n) : (key : ℕ) → Set n where -- (a : Setn) 69 data bt' {n : Level} { l r : ℕ } (A : Set n) : (key : ℕ) → Set n where -- (a : Setn)
70 bt'-leaf : (key : ℕ) → bt' A key 70 bt'-leaf : (key : ℕ) → bt' A key
71 bt'-node : { l r : ℕ } → (key : ℕ) → (value : A) → 71 bt'-node : { l r : ℕ } → (key : ℕ) → (value : A) →
72 bt' {n} A l → bt' {n} A r → l ≤ key → key ≤ r → bt' A key 72 bt' {n} {{!!}} {{!!}} A l → bt' {n} {{!!}} {{!!}} A r → l ≤ key → key ≤ r → bt' A key
73 73
74 data bt'-path {n : Level} (A : Set n) : Set n where -- (a : Setn) 74 data bt'-path {n : Level} (A : Set n) : ℕ → Set n where -- (a : Setn)
75 bt'-left : (key : ℕ) → {left-key : ℕ} → (bt' A left-key ) → (key ≤ left-key) → bt'-path A 75 bt'-left : (key : ℕ) → {left-key : ℕ} → (bt' A left-key ) → (key ≤ left-key) → bt'-path A left-key
76 bt'-right : (key : ℕ) → {right-key : ℕ} → (bt' A right-key ) → (right-key ≤ key) → bt'-path A 76 bt'-right : (key : ℕ) → {right-key : ℕ} → (bt' A right-key ) → (right-key ≤ key) → bt'-path A right-key
77 77
78 78
79 test = bt'-left {Z} {ℕ} 3 {5} (bt'-leaf 5) (s≤s (s≤s (s≤s z≤n))) 79 test = bt'-left {Z} {ℕ} 3 {5} (bt'-leaf 5) (s≤s (s≤s (s≤s z≤n)))
80 80
81 81
93 93
94 tree+stack≡tree は find 後の tree と stack をもって 94 tree+stack≡tree は find 後の tree と stack をもって
95 reverse した stack を使って find をチェックするかんじ? 95 reverse した stack を使って find をチェックするかんじ?
96 --} 96 --}
97 97
98
98 tree+stack : {n m : Level} {A : Set n} {t : Set m} {tn : ℕ} → (tree mtree : bt' A tn ) 99 tree+stack : {n m : Level} {A : Set n} {t : Set m} {tn : ℕ} → (tree mtree : bt' A tn )
99 → (stack : List (bt'-path A )) → Set n 100 → (stack : List (bt'-path A tn)) → Set n
100 tree+stack tree mtree [] = tree ≡ mtree 101 tree+stack tree mtree [] = tree ≡ mtree -- fin case
101 tree+stack {n} {m} {A} {t} {tn} tree mtree (bt'-left key x x₁ ∷ stack) = (mtree ≡ {!!}) ∧ (tree+stack {n} {_} {_} {_} {tn} tree {!!} stack) 102 tree+stack {n} {m} {A} {t} {.key₁} tree mtree@(bt'-leaf key₁) (bt'-left key x x₁ ∷ stack) = (mtree ≡ x) ∧ (tree+stack {n} {m} {_} {t} tree {!!} stack)
102 tree+stack {n} {m} {A} {t} {tn} tree mtree (bt'-right key x x₁ ∷ stack) = (mtree ≡ {!!}) ∧ (tree+stack {n} {_} {_} {_} {tn} tree {!!} stack) 103 tree+stack {n} {m} {A} {t} {.key₁} tree mtree@(bt'-node {l} {r} key₁ value lmtree rmtree x₂ x₃) (bt'-left key x x₁ ∷ stack) = (mtree ≡ x) ∧ (tree+stack {n} {m} {_} {t} {{!!}} tree {!!} stack)
104 tree+stack {n} {m} {A} {t} {tn} tree mtree (bt'-right key x x₁ ∷ stack) = (mtree ≡ x) ∧ (tree+stack {n} {m} {_} {t} {tn} tree {!!} stack)
103 -- tree+stack tree mtree (bt'-right key {rkey} x x₁ ∷ stack) = (mtree ≡ {!!}) ∧ (tree+stack tree {!!} stack) -- tn ≡ rkey がひつよう 105 -- tree+stack tree mtree (bt'-right key {rkey} x x₁ ∷ stack) = (mtree ≡ {!!}) ∧ (tree+stack tree {!!} stack) -- tn ≡ rkey がひつよう
104 106
105 tree+stack≡tree : {n m : Level} {A : Set n} {t : Set m} {tn : ℕ} → (tree mtree : bt' A tn ) 107 tree+stack≡tree : {n m : Level} {A : Set n} {t : Set m} {tn : ℕ} → (tree mtree : bt' A tn )
106 → (stack : List (bt'-path A )) → (reverse stack) ≡ {!!} 108 → (stack : List (bt'-path A tn)) → (reverse stack) ≡ {!!}
107 tree+stack≡tree tree (bt'-leaf key) stack = {!!} 109 tree+stack≡tree tree (bt'-leaf key) stack = {!!}
108 tree+stack≡tree tree (bt'-node key value mtree mtree₁ x x₁) stack = {!!} 110 tree+stack≡tree tree (bt'-node key value mtree mtree₁ x x₁) stack = {!!}
109 111
110 bt-find' : {n m : Level} {A : Set n} {t : Set m} {tn : ℕ} → (key : ℕ) → (tree : bt' A tn ) → List (bt'-path A ) 112 bt-find' : {n m : Level} {A : Set n} {t : Set m} {tn : ℕ} → (key : ℕ) → (tree : bt' A tn ) → List (bt'-path A tn)
111 → ( {key1 : ℕ } → bt' A key1 → List (bt'-path A ) → t ) → t 113 → ( {key1 : ℕ } → bt' A key1 → List (bt'-path A key1) → t ) → t
112 bt-find' key tr@(bt'-leaf key₁) stack next = next tr stack -- no key found 114 bt-find' key tr@(bt'-leaf key₁) stack next = next tr stack -- no key found
113 bt-find' key (bt'-node key₁ value tree tree₁ x x₁) stack next with <-cmp key key₁ 115 bt-find' key (bt'-node key₁ value tree tree₁ x x₁) stack next with <-cmp key key₁
114 bt-find' key tr@(bt'-node {l} {r} key₁ value tree tree₁ x x₁) stack next | tri< a ¬b ¬c = 116 bt-find' key tr@(bt'-node {l} {r} key₁ value tree tree₁ x x₁) stack next | tri< a ¬b ¬c =
115 bt-find' key tree ( (bt'-left key {key₁} tr (<⇒≤ a) ) ∷ stack) next 117 bt-find' key tree ( (bt'-left key {!!} ({!!}) ) ∷ {!!}) next
116 bt-find' key found@(bt'-node key₁ value tree tree₁ x x₁) stack next | tri≈ ¬a b ¬c = next found stack 118 bt-find' key found@(bt'-node key₁ value tree tree₁ x x₁) stack next | tri≈ ¬a b ¬c = next found stack
117 bt-find' key tr@(bt'-node key₁ value tree tree₁ x x₁) stack next | tri> ¬a ¬b c = 119 bt-find' key tr@(bt'-node key₁ value tree tree₁ x x₁) stack next | tri> ¬a ¬b c =
118 bt-find' key tree ( (bt'-right key {key₁} tr (<⇒≤ c) ) ∷ stack) next 120 bt-find' key tree ( (bt'-right key {!!} {!!} ) ∷ {!!}) next
119 121
120 122
121 bt-find-step : {n m : Level} {A : Set n} {t : Set m} {tn : ℕ} → (key : ℕ) → (tree : bt' A tn ) → List (bt'-path A ) 123 bt-find-step : {n m : Level} {A : Set n} {t : Set m} {tn : ℕ} → (key : ℕ) → (tree : bt' A tn ) → List (bt'-path A tn)
122 → ( {key1 : ℕ } → bt' A key1 → List (bt'-path A ) → t ) → t 124 → ( {key1 : ℕ } → bt' A key1 → List (bt'-path A key1) → t ) → t
123 bt-find-step key tr@(bt'-leaf key₁) stack exit = exit tr stack -- no key found 125 bt-find-step key tr@(bt'-leaf key₁) stack exit = exit tr stack -- no key found
124 bt-find-step key (bt'-node key₁ value tree tree₁ x x₁) stack next = {!!} 126 bt-find-step key (bt'-node key₁ value tree tree₁ x x₁) stack next = {!!}
125 127
126 a<sa : { a : ℕ } → a < suc a 128 a<sa : { a : ℕ } → a < suc a
127 a<sa {zero} = s≤s z≤n 129 a<sa {zero} = s≤s z≤n
133 135
134 pa<a : { a : ℕ } → pred (suc a) < suc a 136 pa<a : { a : ℕ } → pred (suc a) < suc a
135 pa<a {zero} = s≤s z≤n 137 pa<a {zero} = s≤s z≤n
136 pa<a {suc a} = s≤s pa<a 138 pa<a {suc a} = s≤s pa<a
137 139
138 bt-replace' : {n m : Level} {A : Set n} {t : Set m} {tn : ℕ} → (key : ℕ) → (value : A ) → (tree : bt' A tn ) → List (bt'-path A ) 140 bt-replace' : {n m : Level} {A : Set n} {t : Set m} {tn : ℕ} → (key : ℕ) → (value : A ) → (tree : bt' A tn ) → List (bt'-path A {!!})
139 → ({key1 : ℕ } → bt' A key1 → t ) → t 141 → ({key1 : ℕ } → bt' A key1 → t ) → t
140 bt-replace' {n} {m} {A} {t} {tn} key value node stack next = bt-replace1 tn node where 142 bt-replace' {n} {m} {A} {t} {tn} key value node stack next = bt-replace1 tn node where
141 bt-replace0 : {tn : ℕ } (node : bt' A tn ) → List (bt'-path A ) → t 143 bt-replace0 : {tn : ℕ } (node : bt' A tn ) → List (bt'-path A {!!}) → t
142 bt-replace0 node [] = next node 144 bt-replace0 node [] = next node
143 bt-replace0 node (bt'-left key (bt'-leaf key₁) x₁ ∷ stack) = {!!} 145 bt-replace0 node (bt'-left key (bt'-leaf key₁) x₁ ∷ stack) = {!!}
144 bt-replace0 {tn} node (bt'-left key (bt'-node key₁ value x x₂ x₃ x₄) x₁ ∷ stack) = bt-replace0 {key₁} (bt'-node key₁ value node x₂ {!!} x₄ ) stack 146 bt-replace0 {tn} node (bt'-left key (bt'-node key₁ value x x₂ x₃ x₄) x₁ ∷ stack) = bt-replace0 {key₁} (bt'-node key₁ value node x₂ {!!} x₄ ) stack
145 bt-replace0 node (bt'-right key x x₁ ∷ stack) = {!!} 147 bt-replace0 node (bt'-right key x x₁ ∷ stack) = {!!}
146 bt-replace1 : (tn : ℕ ) (tree : bt' A tn ) → t 148 bt-replace1 : (tn : ℕ ) (tree : bt' A tn ) → t