Mercurial > hg > Gears > GearsAgda
changeset 604:2075785a124a
new approach
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 03 Nov 2021 10:32:56 +0900 |
| parents | 41e1c9e9718d |
| children | f8cc98fcc34b |
| files | hoareBinaryTree.agda logic.agda |
| diffstat | 2 files changed, 31 insertions(+), 583 deletions(-) [+] |
line wrap: on
line diff
--- a/hoareBinaryTree.agda Tue Nov 02 19:32:10 2021 +0900 +++ b/hoareBinaryTree.agda Wed Nov 03 10:32:56 2021 +0900 @@ -18,33 +18,6 @@ open import logic -SingleLinkedStack = List - -emptySingleLinkedStack : {n : Level } {Data : Set n} -> SingleLinkedStack Data -emptySingleLinkedStack = [] - -clearSingleLinkedStack : {n m : Level } {Data : Set n} {t : Set m} -> SingleLinkedStack Data → ( SingleLinkedStack Data → t) → t -clearSingleLinkedStack [] cg = cg [] -clearSingleLinkedStack (x ∷ as) cg = cg [] - -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) - - - -emptySigmaStack : {n : Level } { Data : Set n} → List Data -emptySigmaStack = [] - -pushSigmaStack : {n m : Level} {d d2 : Set n} {t : Set m} → d2 → List d → (List (d × d2) → t) → t -pushSigmaStack {n} {m} {d} d2 st next = next (Data.List.zip (st) (d2 ∷ []) ) - -tt = pushSigmaStack 3 (true ∷ []) (λ st → st) - _iso_ : {n : Level} {a : Set n} → ℕ → ℕ → Set d iso d' = (¬ (suc d ≤ d')) ∧ (¬ (suc d' ≤ d)) @@ -57,565 +30,40 @@ -- no children , having left node , having right node , having both -- data bt {n : Level} (A : Set n) : Set n where - L : bt A - N : (key : ℕ) → - (ltree : bt A ) → (rtree : bt A ) → bt A - -data bt-path' {n : Level} (A : Set n) : Set n where - left : (bt A) → bt-path' A - right : (bt A) → bt-path' A - - - -tree->key : {n : Level} {A : Set n} → (tree : bt A) → ℕ -tree->key {n} L = zero -tree->key {n} (N key tree tree₁) = key - -node-ex : {n : Level} {A : Set n} → bt A -node-ex {n} {A} = (N zero (L) (L)) - -ex : {n : Level} {A : Set n} → bt A -ex {n} {A} = (N {n} {A} 8 (N 6 (N 2 (N 1 L L) (N 3 L L)) (N 7 L L)) (N 9 L L)) - -exLR : {n : Level} {A : Set n} → bt A -exLR {n} {A} = (N {n} {A} 4 (N 2 L (N 3 L L)) (N 5 L L)) - -exRL : {n : Level} {A : Set n} → bt A -exRL {n} {A} = (N {n} {A} 3 L (N 5 (N 4 L L) L)) - -leaf-ex : {n : Level} {A : Set n} → bt A -leaf-ex {n} {A} = L - - -findLoopInv : {n m : Level} {A : Set n} {t : Set m} → (orig : bt A) → (modify : bt A ) - → (stack : List (bt-path' A)) → Set n -findLoopInv {n} {m} {A} {t} tree mtree [] = tree ≡ mtree -findLoopInv {n} {m} {A} {t} tree mtree (left L ∷ st) = mtree ≡ (L) -findLoopInv {n} {m} {A} {t} tree mtree (right L ∷ st) = mtree ≡ (L) -findLoopInv {n} {m} {A} {t} tree mtree (left (N key x x₁) ∷ st) = mtree ≡ x -findLoopInv {n} {m} {A} {t} tree mtree (right (N key x x₁) ∷ st) = mtree ≡ x₁ - - -hightMerge : {n m : Level} {A : Set n} {t : Set m} → (l r : ℕ) → (ℕ → t) → t -hightMerge lh rh next with <-cmp lh rh -hightMerge lh rh next | tri< a ¬b ¬c = next rh -hightMerge lh rh next | tri≈ ¬a b ¬c = next lh -hightMerge lh rh next | tri> ¬a ¬b c = next lh - - -isHightL : {n m : Level} {A : Set n} {t : Set m} → bt A → (ℕ → t) → t -isHightL L next = next zero -isHightL {n} {_} {A} (N key tree tree₁) next = isHightL tree λ x → next (suc x) - -isHightR : {n m : Level} {A : Set n} {t : Set m} → bt A → (ℕ → t) → t -isHightR L next = next zero -isHightR {n} {_} {A} (N key tree tree₁) next = isHightR tree₁ λ x → next (suc x) - -isHight : {n m : Level} {A : Set n} {t : Set m} → bt A → (ℕ → t) → t -isHight L next = next zero -isHight {n} {_} {A} tr@(N key tree tree₁) next = isHightL tr (λ lh → isHightR tr λ rh → hightMerge {n} {_} {A} (suc lh) (suc rh) next) - -treeHight : {n m : Level} {A : Set n} {t : Set m} → bt A → (ℕ → t) → t -treeHight L next = next zero -treeHight {n} {_} {A} (N key tree tree₁) next = isHight tree (λ lh → isHight tree₁ (λ rh → hightMerge {n} {_} {A} (lh) (rh) next)) - -rhight : {n : Level} {A : Set n} → bt A → ℕ -rhight L = zero -rhight (N key tree tree₁) with <-cmp (rhight tree) (rhight tree₁) -rhight (N key tree tree₁) | tri< a ¬b ¬c = suc (rhight tree₁) -rhight (N key tree tree₁) | tri≈ ¬a b ¬c = suc (rhight tree₁) -rhight (N key tree tree₁) | tri> ¬a ¬b c = suc (rhight tree) - -leaf≠node : {n : Level} {A : Set n} {a : ℕ} {l r : bt A} → ((N {n} {A} a l r) ≡ L) → ⊥ -leaf≠node () - -leafIsNoHight : {n : Level} {A : Set n} (tree : bt A) → tree ≡ L → (treeHight tree (λ x → x) ≡ 0) -leafIsNoHight L refl = refl - - -hight-tree : {n : Level} {A : Set n} {k : ℕ} {l r : bt A} → ℕ → (tree : bt A) → Set n -hight-tree zero tree = tree ≡ L -hight-tree {n} {A} {k} {l} {r} (suc h) tree = tree ≡ (N k l r) - - -hightIsNotLeaf : {n : Level} {A : Set n} (h : ℕ) → (tree : bt A) → (0 ≡ treeHight tree (λ x → x)) → (tree ≡ L) -hightIsNotLeaf h tree eq = {!!} - --- leaf≡0 : {n : Level} {A : Set n} (tree : bt A) → (rhight tree ≡ 0) → tree ≡ L --- leaf≡0 L _ = refl - --- find-function sepalate "next", "loop" -find-hoare-next : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree mt : bt A ) → (st : List (bt-path' A)) → (findLoopInv {n} {m} {A} {t} tree mt st) - → (next : (nt : bt A) → (ns : List (bt-path' A)) → (findLoopInv {n} {m} {A} {t} tree nt ns) → t ) - → (exit : (nt : bt A) → (ns : List (bt-path' A)) → (nt ≡ L) ∨ (key ≡ tree->key nt) → t ) → t -find-hoare-next key leaf@(L) mt st eq _ exit = exit leaf st (case1 refl) -find-hoare-next key (N key₁ tree tree₁) mt st eq next exit with <-cmp key key₁ -find-hoare-next key node@(N key₁ tree tree₁) mt st eq _ exit | tri≈ ¬a b ¬c = exit node st (case2 b) -find-hoare-next key node@(N key₁ tree tree₁) mt st eq next _ | tri< a ¬b ¬c = next tree ((left node) ∷ st) refl -find-hoare-next key node@(N key₁ tree tree₁) mt st eq next _ | tri> ¬a ¬b c = next tree₁ ((right node) ∷ st) refl - -find-hoare-loop : {n m : Level} {A : Set n} {t : Set m} → (hight key : ℕ) → (tree mt : bt A ) → (st : List (bt-path' A)) → (findLoopInv {n} {m} {A} {t} tree mt st) - → (exit : (nt : bt A) → (ns : List (bt-path' A)) → (nt ≡ L) ∨ (key ≡ tree->key nt) → t) → t -find-hoare-loop zero key tree mt st eq exit with key ≟ (tree->key tree) -find-hoare-loop zero key tree mt st eq exit | yes p = exit tree st (case2 p) -find-hoare-loop zero key tree mt st eq exit | no ¬p = exit tree st (case1 {!!}) - -find-hoare-loop (suc h) key otr lf@(L) st eq exit = exit lf st (case1 refl) -find-hoare-loop (suc h) key otr tr@(N key₁ tree tree₁) st eq exit = find-hoare-next key otr tr st eq ((λ tr1 st1 eq → find-hoare-loop h key otr tr1 st1 eq exit)) exit - - - --- bt-find : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree : bt A ) → List (bt-path A) --- → ( bt A → List (bt-path A) → t ) → t --- bt-find {n} {m} {A} {t} key leaf@(L) stack exit = exit leaf stack --- bt-find {n} {m} {A} {t} key (N key₁ tree tree₁) stack next with <-cmp key key₁ --- bt-find {n} {m} {A} {t} key node@(N key₁ tree tree₁) stack exit | tri≈ ¬a b ¬c = exit node stack --- bt-find {n} {m} {A} {t} key node@(N key₁ ltree rtree) stack next | tri< a ¬b ¬c = bt-find key ltree (bt-left key node ∷ stack) next --- bt-find {n} {m} {A} {t} key node@(N key₁ ltree rtree) stack next | tri> ¬a ¬b c = bt-find key rtree (bt-right key node ∷ stack) next - - --- bt-find' : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree : bt A ) → List (bt-path' A) → ( bt A → List (bt-path' A) → t ) → t --- bt-find' key leaf@(L) stack exit = exit leaf stack --- bt-find' key node@(N key1 lnode rnode) stack exit with <-cmp key key1 --- bt-find' key node@(N key1 lnode rnode) stack exit | tri≈ ¬a b ¬c = exit node stack --- bt-find' key node@(N key1 lnode rnode) stack next | tri< a ¬b ¬c = bt-find' key lnode ((left node) ∷ stack) next --- bt-find' key node@(N key1 lnode rnode) stack next | tri> ¬a ¬b c = bt-find' key rnode ((right node) ∷ stack) next - - --- find-next : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree : bt A ) → List (bt-path' A) --- → (next : bt A → List (bt-path' A) → t ) → (exit : bt A → List (bt-path' A) → t ) → t --- find-next key leaf@(L) st _ exit = exit leaf st --- find-next key (N key₁ tree tree₁) st next exit with <-cmp key key₁ --- find-next key node@(N key₁ tree tree₁) st _ exit | tri≈ ¬a b ¬c = exit node st --- find-next key node@(N key₁ tree tree₁) st next _ | tri< a ¬b ¬c = next tree ((left node) ∷ st) --- find-next key node@(N key₁ tree tree₁) st next _ | tri> ¬a ¬b c = next tree₁ ((right node) ∷ st) - --- find-loop は bt-find' とだいたい一緒(induction してるくらい) --- これも多分 Zコンビネータの一種? --- loop で induction してる hight は現在の木の最大長より大きければよい(find-next が抜けきるため) --- 逆に木の最大長より小さい(たどるルートより小さい)場合は途中経過の値が返る + leaf : bt A + node : (key : ℕ) → (value : A) → + (left : bt A ) → (write : bt A ) → bt A --- find-loop : {n m : Level} {A : Set n} {t : Set m} → (hight key : ℕ) → (tree : bt A ) → List (bt-path' A) → (exit : bt A → List (bt-path' A) → t) → t --- find-loop zero key tree st exit = exit tree st --- find-loop (suc h) key lf@(L) st exit = exit lf st --- find-loop (suc h) key tr@(N key₁ tree tree₁) st exit = find-next key tr st ((λ tr1 st1 → find-loop h key tr1 st1 exit)) exit - --- bt-replace : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → bt A → List (bt-path A) → (bt A → t ) → t --- bt-replace {n} {m} {A} {t} ikey otree stack next = bt-replace0 otree where --- bt-replace1 : bt A → List (bt-path A) → t --- bt-replace1 tree [] = next tree --- bt-replace1 node (bt-left key (L) ∷ stack) = bt-replace1 node stack --- bt-replace1 node (bt-right key (L) ∷ stack) = bt-replace1 node stack --- bt-replace1 node (bt-left key (N key₁ x x₁) ∷ stack) = bt-replace1 (N key₁ node x₁) stack --- bt-replace1 node (bt-right key (N key₁ x x₁) ∷ stack) = bt-replace1 (N key₁ x node) stack --- bt-replace0 : (tree : bt A) → t --- bt-replace0 tree@(N key ltr rtr) = bt-replace1 tree stack -- find case --- bt-replace0 (L) = {!!} - - - --- bt-insert : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → bt A → (bt A → t ) → t --- bt-insert {n} {m} {A} {t} key tree next = bt-find key tree [] (λ tr st → bt-replace key tr st (λ new → next new)) - - -{-- -[ok] find でステップ毎にみている node と stack の top を一致させる -[ok] find 中はnode と stack の top が一致する(pre は stack の中身がなく, post は stack の top とずれる) - -tree+stack≡tree は find 後の tree と stack をもって -reverse した stack を使って find をチェックするかんじ? ---} - -{-- -tree+stack は tree と stack を受け取ってひとしさ(関係)を返すやつ - ---} - --- tree+stack : {n m : Level} {A : Set n} {t : Set m} → (tree mtree : bt A ) --- → (stack : List (bt-path A)) → Set n --- tree+stack tree mtree [] = tree ≡ mtree -- fin case --- tree+stack {n} {m} {A} {t} tree mtree@(L) (bt-left key x ∷ stack) = (mtree ≡ x) -- unknow case --- tree+stack {n} {m} {A} {t} tree mtree@(L) (bt-right key x ∷ stack) = (mtree ≡ x) -- we nofound leaf's left, right node --- tree+stack {n} {m} {A} {t} tree mtree@(N key1 ltree rtree) (bt-left key x ∷ stack) = (mtree ≡ x) ∧ (tree+stack {n} {m} {_} {t} tree ltree stack) -- correct case --- tree+stack {n} {m} {A} {t} tree mtree@(N key₁ ltree rtree) (bt-right key x ∷ stack) = (mtree ≡ x) ∧ (tree+stack {n} {m} {_} {t} tree rtree stack) - -{-- -tree+stack - 2. find loop → "top of reverse stack" ≡ "find route orig tree" ---} - --- s+t≡t : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree : bt A ) → (stack : List (bt-path' {n} A)) → bt-find' key tree stack (λ mt st → s+t {n} {A} tree mt st) --- s+t≡t {n} {m} {A} {t} key (L) [] = refl --- s+t≡t {n} {m} {A} {t} key (L) (left x ∷ []) = refl --- s+t≡t {n} {m} {A} {t} key (L) (left x ∷ x₁ ∷ stack) = refl --- s+t≡t {n} {m} {A} {t} key (L) (right x ∷ []) = refl --- s+t≡t {n} {m} {A} {t} key (L) (right x ∷ x₁ ∷ stack) = refl --- s+t≡t {n} {m} {A} {t} key (N key₁ tree tree₁) [] with <-cmp key key₁ --- s+t≡t {n} {m} {A} {t} key (N key₁ tree tree₁) [] | tri≈ ¬a b ¬c = refl --- s+t≡t {n} {m} {A} {t} key (N key₁ tree tree₁) [] | tri< a ¬b ¬c = {!!} --- s+t≡t {n} {m} {A} {t} key (N key₁ tree tree₁) [] | tri> ¬a ¬b c = {!!} --- s+t≡t {n} {m} {A} {t} key (N key₁ tree tree₁) (x ∷ stack) = {!!} - - +find : {n : Level} {A : Set n} {t : Set n} → (key : ℕ) → (tree : bt A ) → List (bt A) + → (next : bt A → List (bt A) → t ) → (exit : bt A → List (bt A) → t ) → t +find key leaf st _ exit = exit leaf st +find key (node key₁ v tree tree₁) st next exit with <-cmp key key₁ +find key n st _ exit | tri≈ ¬a b ¬c = exit n st +find key n@(node key₁ v tree tree₁) st next _ | tri< a ¬b ¬c = next tree (n ∷ st) +find key n@(node key₁ v tree tree₁) st next _ | tri> ¬a ¬b c = next tree₁ (n ∷ st) --- s+t : {n : Level} {A : Set n} → (tree mtree : bt A ) → (stack : List (bt-path' {n} A)) → Set n --- s+t tree mtree [] = tree ≡ mtree --- s+t tree mtree (x ∷ []) = tree ≡ mtree --- s+t tr@(L) mt (left x ∷ x₁ ∷ stack) = tr ≡ mt --- s+t {n} {A} tr@(N key tree tree₁) mt (left x ∷ x₁ ∷ stack) = (mt ≡ x) ∧ (s+t {n} {A} tree (path2tree x₁) stack) --- s+t tr@(L) mt (right x ∷ x₁ ∷ stack) = tr ≡ mt --- s+t {n} {A} tr@(N key tree tree₁) mt (right x ∷ x₁ ∷ stack) = (mt ≡ x) ∧ (s+t {n} {A} tree₁ (path2tree x₁) stack) - --- data treeType {n : Level} (A : Set n) : Set n where --- leaf-t : treeType A --- node-t : treeType A - --- isType : {n : Level} {A : Set n} → bt A → treeType A --- isType (L) = leaf-t --- isType (N key tree tree₁) = node-t - --- data findState : Set where --- s1 : findState --- s2 : findState --- sf : findState - --- findStateP : {n : Level} {A : Set n} → findState → ℕ → bt A → (mnode : bt A) → List (bt-path' A) → Set n --- findStateP s1 key node mnode stack = stack ≡ [] --- findStateP s2 key node mnode stack = (s+t node mnode (reverse stack)) --- findStateP sf key node mnode stack = (key ≡ (tree->key mnode)) ∨ ((isType mnode) ≡ leaf-t) - --- findStartPwP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree mtree : bt A ) → (findStateP s1 key tree mtree [] → t) → t --- findStartPwP key tree mtree next = next refl - - - --- findLoopPwP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree mtree : bt A ) → (st : List (bt-path' A)) --- → (findStateP s2 key tree mtree st) --- → (next : (tr : bt A) → (st : List (bt-path' A)) → (findStateP s2 key tree mtree st) → t) --- → (exit : (tr : bt A) → (st : List (bt-path' A)) → (findStateP sf key tree mtree st) → t ) → t --- findLoopPwP key tree (L) [] state next exit = exit tree [] (case2 refl) --- findLoopPwP key tree (N key₁ mtree mtree₁) [] state next exit = next tree [] {!!} --- findLoopPwP key tree mtree (x ∷ []) state next exit = {!!} --- findLoopPwP key tree (L) (x ∷ x₁ ∷ stack) state next exit = {!!} --- findLoopPwP key tree (N key₁ mtree mtree₁) (left x ∷ x₁ ∷ stack) state next exit = --- next {!!} {!!} {!!} --- findLoopPwP key tree (N key₁ mtree mtree₁) (right x ∷ x₁ ∷ stack) state next exit = {!!} - - --- -- tree+stack' {n} {m} {A} {t} (N key ltree rtree) mtree@(N key₁ lmtree rmtree) (x ∷ stack) with <-cmp key key₁ --- tree+stack' {n} {m} {A} {t} tt@(N key ltree rtree) mt@(N key₁ lmtree rmtree) (x ∷ stack) | tri≈ ¬a b ¬c = tt ≡ mt --- tree+stack' {n} {m} {A} {t} tt@(N key ltree rtree) mt@(N key₁ lmtree rmtree) st@(x ∷ stack) | tri< a ¬b ¬c = (mt ≡ x) ∧ tree+stack' {n} {m} {A} {t} tt lmtree (mt ∷ st) --- tree+stack' {n} {m} {A} {t} tt@(N key ltree rtree) mt@(N key₁ lmtree rmtree) st@(x ∷ stack) | tri> ¬a ¬b c = (mt ≡ x) ∧ tree+stack' {n} {m} {A} {t} tt rmtree (mt ∷ st) - - - --- tree+stack≡tree : {n m : Level} {A : Set n} {t : Set m} → (tree mtree : bt A ) --- → (stack : List (bt-path A )) → tree+stack {_} {m} {_} {t} tree mtree (reverse stack) --- tree+stack≡tree tree (L key) stack = {!!} --- tree+stack≡tree tree (N key rtree ltree) stack = {!!} - - - --- loop はきっと start, running, stop の3つに分けて考えるといいよね -{-- find status - 1. find start → stack empty - 2. find loop → stack Not empty ∧ node Not empty - or "in reverse stack" ≡ "find route orig tree" - 3. find fin → "stack Not empty ∧ current node is leaf" - or "stack Not empty ∧ current node key ≡ find-key" ---} - --- find-step : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree : bt A) → (stack : List (bt A)) --- → (next : (mtree : bt A) → (stack1 : List (bt A)) → (tree+stack' {n} {m} {A} {t} tree mtree stack1 ) → t) --- → (exit : (mtree : bt A) → List (bt A) → (tree ≡ L (tree->key mtree )) ∨ (key ≡ (tree->key mtree)) → t) → t --- find-step {n} {m} {A} {t} key (L) stack next exit = exit (L) stack (case1 refl) --- find-step {n} {m} {A} {t} key (N key₁ node node₁) stack next exit with <-cmp key key₁ --- find-step {n} {m} {A} {t} key (N key₁ node node₁) stack next exit | tri≈ ¬a b ¬c = exit (N key₁ node node₁) stack (case2 b) --- find-step {n} {m} {A} {t} key (N key₁ node node₁) stack next exit | tri< a ¬b ¬c = next node stack {!!} --- find-step {n} {m} {A} {t} key (N key₁ node node₁) stack next exit | tri> ¬a ¬b c = next node₁ stack {!!} - +{-# TERMINATING #-} +find-loop : {n : Level} {A : Set n} {t : Set n} → (key : ℕ) → bt A → List (bt A) → (exit : bt A → List (bt A) → t) → t +find-loop {_} {A} {t} key tree st exit = find-loop1 tree st where + find-loop1 : bt A → List (bt A) → t + find-loop1 tree st = find key tree st find-loop1 exit --- find-check : {n m : Level} {A : Set n} {t : Set m} → (k : ℕ) → (tree : bt A ) --- → (stack : List (bt-path A )) → bt-find k tree [] (λ mtree mstack → tree+stack {_} {m} {_} {t} tree mtree (reverse mstack)) --- find-check {n} {m} {A} {t} key (L) [] = refl --- find-check {n} {m} {A} {t} key (N key₁ tree tree₁) [] with <-cmp key key₁ --- find-check {n} {m} {A} {t} key (N key₁ tree tree₁) [] | tri≈ ¬a b ¬c = refl --- find-check {n} {m} {A} {t} key (N key₁ tree tree₁) [] | tri< a ¬b ¬c = {!!} --- find-check {n} {m} {A} {t} key (N key₁ tree tree₁) [] | tri> ¬a ¬b c = {!!} --- find-check {n} {m} {A} {t} key tree (x ∷ stack) = {!!} - - --- module ts where --- tbt : {n : Level} {A : Set n} → bt A --- tbt {n} {A} = N {n} {A} 8 (N 6 (N 2 (L) (L)) (L)) (L) - --- find : {n : Level} {A : Set n} → ℕ → List (bt-path A) --- find {n} {A} key = bt-find key tbt [] (λ x y → y ) - --- find' : {n : Level} {A : Set n} → ℕ → bt A --- find' {n} {A} key = bt-find' key tbt [] (λ x y → x ) - --- rep : {n m : Level} {A : Set n} {t : Set m} → ℕ → bt A --- rep {n} {m} {A} {t} key = bt-find {n} {_} {A} key tbt [] (λ tr st → bt-replace key tr st (λ mtr → mtr)) - --- ins : {n m : Level} {A : Set n} {t : Set m} → ℕ → bt A --- ins {n} {m} {A} {t} key = bt-insert key tbt (λ tr → tr) - --- test : {n m : Level} {A : Set n} {t : Set m} (key : ℕ) --- → bt-find {n} {_} {A} {_} key tbt [] (λ x y → tree+stack {n} {m} {A} {t} tbt x y) --- test key = {!!} --- -- --- --- no children , having left node , having right node , having both --- -data bt' {n : Level} (A : Set n) : (key : ℕ) → Set n where -- (a : Setn) - bt'-leaf : (key : ℕ) → bt' A key - bt'-node : { l r : ℕ } → (key : ℕ) → (value : A) → - bt' A l → bt' A r → l ≤ key → key ≤ r → bt' A key - --- data bt'-path {n : Level} (A : Set n) : ℕ → Set n where -- (a : Setn) --- bt'-left : (key : ℕ) → {left-key : ℕ} → (bt' A left-key ) → (key ≤ left-key) → bt'-path A left-key --- bt'-right : (key : ℕ) → {right-key : ℕ} → (bt' A right-key ) → (right-key ≤ key) → bt'-path A right-key - - --- test = bt'-left {Z} {ℕ} 3 {5} (bt'-leaf 5) (s≤s (s≤s (s≤s z≤n))) - - - --- reverse1 : List (bt' A tn) → List (bt' A tn) → List (bt' A tn) --- reverse1 [] s1 = s1+ --- reverse1 (x ∷ s0) s1 with reverse1 s0 (x ∷ s1) --- ... | as = {!!} - - - --- bt-find' : {n m : Level} {A : Set n} {t : Set m} {tn : ℕ} → (key : ℕ) → (tree : bt' A tn ) → List (bt'-path A tn) --- → ( {key1 : ℕ } → bt' A key1 → List (bt'-path A key1) → t ) → t --- bt-find' key tr@(bt'-leaf key₁) stack next = next tr stack -- no key found --- bt-find' key (bt'-node key₁ value tree tree₁ x x₁) stack next with <-cmp key key₁ --- bt-find' key tr@(bt'-node {l} {r} key₁ value tree tree₁ x x₁) stack next | tri< a ¬b ¬c = --- bt-find' key tree ( (bt'-left key {!!} ({!!}) ) ∷ {!!}) next --- bt-find' key found@(bt'-node key₁ value tree tree₁ x x₁) stack next | tri≈ ¬a b ¬c = next found stack --- bt-find' key tr@(bt'-node key₁ value tree tree₁ x x₁) stack next | tri> ¬a ¬b c = --- bt-find' key tree ( (bt'-right key {!!} {!!} ) ∷ {!!}) next - - --- bt-find-step : {n m : Level} {A : Set n} {t : Set m} {tn : ℕ} → (key : ℕ) → (tree : bt' A tn ) → List (bt'-path A tn) --- → ( {key1 : ℕ } → bt' A key1 → List (bt'-path A key1) → t ) → t --- bt-find-step key tr@(bt'-leaf key₁) stack exit = exit tr stack -- no key found --- bt-find-step key (bt'-node key₁ value tree tree₁ x x₁) stack next = {!!} - --- a<sa : { a : ℕ } → a < suc a --- a<sa {zero} = s≤s z≤n --- a<sa {suc a} = s≤s a<sa - --- a≤sa : { a : ℕ } → a ≤ suc a --- a≤sa {zero} = z≤n --- a≤sa {suc a} = s≤s a≤sa - --- pa<a : { a : ℕ } → pred (suc a) < suc a --- pa<a {zero} = s≤s z≤n --- pa<a {suc a} = s≤s pa<a - --- bt-replace' : {n m : Level} {A : Set n} {t : Set m} {tn : ℕ} → (key : ℕ) → (value : A ) → (tree : bt' A tn ) → List (bt'-path A {!!}) --- → ({key1 : ℕ } → bt' A key1 → t ) → t --- bt-replace' {n} {m} {A} {t} {tn} key value node stack next = bt-replace1 tn node where --- bt-replace0 : {tn : ℕ } (node : bt' A tn ) → List (bt'-path A {!!}) → t --- bt-replace0 node [] = next node --- bt-replace0 node (bt'-left key (bt'-leaf key₁) x₁ ∷ stack) = {!!} --- 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 --- bt-replace0 node (bt'-right key x x₁ ∷ stack) = {!!} --- bt-replace1 : (tn : ℕ ) (tree : bt' A tn ) → t --- bt-replace1 tn (bt'-leaf key0) = bt-replace0 (bt'-node tn value --- (bt'-leaf (pred tn)) (bt'-leaf (suc tn) ) (≤⇒pred≤ ≤-refl) a≤sa) stack --- bt-replace1 tn (bt'-node key value node node₁ x x₁) = bt-replace0 (bt'-node key value node node₁ x x₁) stack - --- tree->key : {n : Level} {tn : ℕ} → (A : Set n) → (tree : bt' A tn ) → ℕ --- tree->key {n} {.key} (A) (bt'-leaf key) = key --- tree->key {n} {.key} (A) (bt'-node key value tree tree₁ x x₁) = key - - --- bt-find'-assert1 : {n m : Level} {A : Set n} {t : Set m} {tn : ℕ} → (tree : bt' A tn ) → Set n --- bt-find'-assert1 {n} {m} {A} {t} {tn} tree = (key : ℕ) → (val : A) → bt-find' key tree [] (λ tree1 stack → key ≡ (tree->key A tree1)) - - --- bt-replace-hoare : {n m : Level} {A : Set n} {t : Set m} {tn : ℕ} → (key : ℕ) → (value : A ) → (tree : bt' A tn ) --- → (pre : bt-find'-assert1 {n} {m} {A} {t} tree → bt-replace' {!!} {!!} {!!} {!!} {!!}) → t --- bt-replace-hoare key value tree stack = {!!} - - - --- find'-support : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (d : ℕ) → (tree : bt' {n} {a} ) → SingleLinkedStack (bt' {n} {a} ) → ( (bt' {n} {a} ) → SingleLinkedStack (bt' {n} {a} ) → Maybe (Σ ℕ (λ d' → _iso_ {n} {a} d d')) → t ) → t - --- find'-support {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key leaf@(bt'-leaf x) st cg = cg leaf st nothing --- find'-support {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (bt'-node d tree₁ tree₂ x x₁) st cg with <-cmp key d --- find'-support {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key node@(bt'-node d tree₁ tree₂ x x₁) st cg | tri≈ ¬a b ¬c = cg node st (just (d , iso-intro {n} {a} ¬a ¬c)) - --- find'-support {n} {m} {a} {t} key node@(bt'-node ⦃ nl ⦄ ⦃ l' ⦄ ⦃ nu ⦄ ⦃ u' ⦄ d L R x x₁) st cg | tri< a₁ ¬b ¬c = --- pushSingleLinkedStack st node --- (λ st2 → find'-support {n} {m} {a} {t} {{l'}} {{d}} key L st2 cg) - --- find'-support {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key node@(bt'-node ⦃ ll ⦄ ⦃ ll' ⦄ ⦃ lr ⦄ ⦃ lr' ⦄ d L R x x₁) st cg | tri> ¬a ¬b c = pushSingleLinkedStack st node --- (λ st2 → find'-support {n} {m} {a} {t} {{d}} {{lr'}} key R st2 cg) - - - --- lleaf : {n : Level} {a : Set n} → bt {n} {a} --- lleaf = (L ⦃ 0 ⦄ ⦃ 3 ⦄ z≤n) - --- lleaf1 : {n : Level} {A : Set n} → (0 < 3) → (a : A) → (d : ℕ ) → bt' {n} A d --- lleaf1 0<3 a d = bt'-leaf d - --- test-node1 : bt' ℕ 3 --- test-node1 = bt'-node (3) 3 (bt'-leaf 2) (bt'-leaf 4) (s≤s (s≤s {!!})) (s≤s (s≤s (s≤s {!!}))) - - --- rleaf : {n : Level} {a : Set n} → bt {n} {a} --- rleaf = (L ⦃ 3 ⦄ ⦃ 3 ⦄ (s≤s (s≤s (s≤s z≤n)))) - --- test-node : {n : Level} {a : Set n} → bt {n} {a} --- test-node {n} {a} = (N ⦃ 0 ⦄ ⦃ 0 ⦄ ⦃ 4 ⦄ ⦃ 4 ⦄ 3 lleaf rleaf z≤n ≤-refl ) +replace : {n : Level} {A : Set n} {t : Set n} → (key : ℕ) → (value : A) → bt A → List (bt A) → (next : ℕ → A → bt A → List (bt A) → t ) → (exit : bt A → t) → t +replace key value tree [] next exit = exit tree +replace key value tree (leaf ∷ st) next exit = next key value tree st +replace key value tree (node key₁ value₁ left right ∷ st) next exit with <-cmp key key₁ +... | tri< a ¬b ¬c = next key value (node key₁ value₁ tree right ) st +... | tri≈ ¬a b ¬c = next key value (node key₁ value left right ) st +... | tri> ¬a ¬b c = next key value (node key₁ value₁ left tree ) st --- -- stt : {n m : Level} {a : Set n} {t : Set m} → {!!} --- -- stt {n} {m} {a} {t} = pushSingleLinkedStack [] (test-node ) (λ st → pushSingleLinkedStack st lleaf (λ st2 → st2) ) - - - --- -- search の {{ l }} {{ u }} はその時みている node の 大小。 l が小さく u が大きい --- -- ここでは d が現在の node のkey値なので比較後のsearch では値が変わる --- bt-search : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (d : ℕ) → bt {n} {a} → (Maybe (Σ ℕ (λ d' → _iso_ {n} {a} d d')) → t ) → t --- bt-search {n} {m} {a} {t} key (L x) cg = cg nothing --- bt-search {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (N ⦃ ll ⦄ ⦃ l' ⦄ ⦃ uu ⦄ ⦃ u' ⦄ d L R x x₁) cg with <-cmp key d --- bt-search {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (N ⦃ ll ⦄ ⦃ l' ⦄ ⦃ uu ⦄ ⦃ u' ⦄ d L R x x₁) cg | tri< a₁ ¬b ¬c = bt-search ⦃ l' ⦄ ⦃ d ⦄ key L cg --- bt-search {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (N ⦃ ll ⦄ ⦃ l' ⦄ ⦃ uu ⦄ ⦃ u' ⦄ d L R x x₁) cg | tri≈ ¬a b ¬c = cg (just (d , iso-intro {n} {a} ¬a ¬c)) --- bt-search {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (N ⦃ ll ⦄ ⦃ l' ⦄ ⦃ uu ⦄ ⦃ u' ⦄ d L R x x₁) cg | tri> ¬a ¬b c = bt-search ⦃ d ⦄ ⦃ u' ⦄ key R cg - --- -- bt-search {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (N ⦃ l ⦄ ⦃ l' ⦄ ⦃ u ⦄ ⦃ u' ⦄ d L R x x₁) cg | tri< a₁ ¬b ¬c = ? -- bt-search ⦃ l' ⦄ ⦃ d ⦄ key L cg --- -- bt-search {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (N d L R x x₁) cg | tri≈ ¬a b ¬c = cg (just (d , iso-intro {n} {a} ¬a ¬c)) --- -- bt-search {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (N ⦃ l ⦄ ⦃ l' ⦄ ⦃ u ⦄ ⦃ u' ⦄ d L R x x₁) cg | tri> ¬a ¬b c = bt-search ⦃ d ⦄ ⦃ u' ⦄ key R cg - - --- -- この辺の test を書くときは型を考えるのがやや面倒なので先に動作を書いてから型を ? から補間するとよさそう --- bt-search-test : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (x : (x₁ : Maybe (Σ ℕ (λ z → ((x₂ : 4 ≤ z) → ⊥) ∧ ((x₂ : suc z ≤ 3) → ⊥)))) → t) → t --- bt-search-test {n} {m} {a} {t} = bt-search {n} {m} {a} {t} ⦃ zero ⦄ ⦃ 4 ⦄ 3 test-node - --- bt-search-test-bad : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (x : (x₁ : Maybe (Σ ℕ (λ z → ((x₂ : 8 ≤ z) → ⊥) ∧ ((x₂ : suc z ≤ 7) → ⊥)))) → t) → t --- bt-search-test-bad {n} {m} {a} {t} = bt-search {n} {m} {a} {t} ⦃ zero ⦄ ⦃ 4 ⦄ 7 test-node - - --- -- up-some : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ {d : ℕ} → (Maybe (Σ ℕ (λ d' → _iso_ {n} {a} d d'))) → (Maybe ℕ) --- -- up-some (just (fst , snd)) = just fst --- -- up-some nothing = nothing - --- search-lem : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (key : ℕ) → (tree : bt {n} {a} ) → bt-search ⦃ l ⦄ ⦃ u ⦄ key tree (λ gdata → gdata ≡ gdata) --- search-lem {n} {m} {a} {t} key (L x) = refl --- search-lem {n} {m} {a} {t} key (N d tree₁ tree₂ x x₁) with <-cmp key d --- search-lem {n} {m} {a} {t} key (N ⦃ ll ⦄ ⦃ ll' ⦄ ⦃ lr ⦄ ⦃ lr' ⦄ d tree₁ tree₂ x x₁) | tri< lt ¬eq ¬gt = search-lem {n} {m} {a} {t} ⦃ ll' ⦄ ⦃ d ⦄ key tree₁ --- search-lem {n} {m} {a} {t} key (N d tree₁ tree₂ x x₁) | tri≈ ¬lt eq ¬gt = refl --- search-lem {n} {m} {a} {t} key (N ⦃ ll ⦄ ⦃ ll' ⦄ ⦃ lr ⦄ ⦃ lr' ⦄ d tree₁ tree₂ x x₁) | tri> ¬lt ¬eq gt = search-lem {n} {m} {a} {t} ⦃ d ⦄ ⦃ lr' ⦄ key tree₂ - - --- -- bt-find --- find-support : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (d : ℕ) → (tree : bt {n} {a} ) → SingleLinkedStack (bt {n} {a} ) → ( (bt {n} {a} ) → SingleLinkedStack (bt {n} {a} ) → Maybe (Σ ℕ (λ d' → _iso_ {n} {a} d d')) → t ) → t - --- find-support {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key leaf@(L x) st cg = cg leaf st nothing --- find-support {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (N d tree₁ tree₂ x x₁) st cg with <-cmp key d --- find-support {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key node@(N d tree₁ tree₂ x x₁) st cg | tri≈ ¬a b ¬c = cg node st (just (d , iso-intro {n} {a} ¬a ¬c)) - --- find-support {n} {m} {a} {t} key node@(N ⦃ nl ⦄ ⦃ l' ⦄ ⦃ nu ⦄ ⦃ u' ⦄ d L R x x₁) st cg | tri< a₁ ¬b ¬c = --- pushSingleLinkedStack st node --- (λ st2 → find-support {n} {m} {a} {t} {{l'}} {{d}} key L st2 cg) - --- find-support {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key node@(N ⦃ ll ⦄ ⦃ ll' ⦄ ⦃ lr ⦄ ⦃ lr' ⦄ d L R x x₁) st cg | tri> ¬a ¬b c = pushSingleLinkedStack st node --- (λ st2 → find-support {n} {m} {a} {t} {{d}} {{lr'}} key R st2 cg) - --- bt-find : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (d : ℕ) → (tree : bt {n} {a} ) → SingleLinkedStack (bt {n} {a} ) → ( (bt {n} {a} ) → SingleLinkedStack (bt {n} {a} ) → Maybe (Σ ℕ (λ d' → _iso_ {n} {a} d d')) → t ) → t --- bt-find {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key tr st cg = clearSingleLinkedStack st --- (λ cst → find-support ⦃ l ⦄ ⦃ u ⦄ key tr cst cg) - --- find-test : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → List bt -- ? --- find-test {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ = bt-find {n} {_} {a} ⦃ l ⦄ ⦃ u ⦄ 3 test-node [] (λ tt st ad → st) --- {-- result --- λ {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ → --- N 3 (L z≤n) (L (s≤s (s≤s (s≤s z≤n)))) z≤n (s≤s (s≤s (s≤s (s≤s z≤n)))) ∷ [] --- --} - --- find-lem : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (d : ℕ) → (tree : bt {n} {a}) → (st : List (bt {n} {a})) → find-support {{l}} {{u}} d tree st (λ ta st ad → ta ≡ ta) --- find-lem d (L x) st = refl --- find-lem d (N d₁ tree tree₁ x x₁) st with <-cmp d d₁ --- find-lem d (N d₁ tree tree₁ x x₁) st | tri≈ ¬a b ¬c = refl - +{-# TERMINATING #-} +replace-loop : {n : Level} {A : Set n} {t : Set n} → (key : ℕ) → (value : A) → bt A → List (bt A) → (exit : bt A → t) → t +replace-loop {_} {A} {t} key value tree st exit = replace-loop1 key value tree st where + replace-loop1 : (key : ℕ) → (value : A) → bt A → List (bt A) → t + replace-loop1 key value tree st = replace key value tree st replace-loop1 exit --- find-lem d (N d₁ tree tree₁ x x₁) st | tri< a ¬b ¬c with tri< a ¬b ¬c --- find-lem {n} {m} {a} {t} {{l}} {{u}} d (N d₁ tree tree₁ x x₁) st | tri< lt ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ = find-lem {n} {m} {a} {t} {{l}} {{u}} d tree {!!} --- find-lem d (N d₁ tree tree₁ x x₁) st | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = {!!} --- find-lem d (N d₁ tree tree₁ x x₁) st | tri< a ¬b ¬c | tri> ¬a ¬b₁ c = {!!} - --- find-lem d (N d₁ tree tree₁ x x₁) st | tri> ¬a ¬b c = {!!} - --- bt-singleton :{n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (d : ℕ) → ( (bt {n} {a} ) → t ) → t --- bt-singleton {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ d cg = cg (N ⦃ 0 ⦄ ⦃ 0 ⦄ ⦃ d ⦄ ⦃ d ⦄ d (L ⦃ 0 ⦄ ⦃ d ⦄ z≤n ) (L ⦃ d ⦄ ⦃ d ⦄ ≤-refl) z≤n ≤-refl) - - --- singleton-test : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → bt -- ? --- singleton-test {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ = bt-singleton {n} {_} {a} ⦃ l ⦄ ⦃ u ⦄ 10 λ x → x - - --- replace-helper : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (tree : bt {n} {a} ) → SingleLinkedStack (bt {n} {a} ) → ( (bt {n} {a} ) → t ) → t --- replace-helper {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ tree [] cg = cg tree --- replace-helper {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ tree@(N d L R x₁ x₂) (L x ∷ st) cg = replace-helper ⦃ l ⦄ ⦃ u ⦄ tree st cg -- Unknown Case --- replace-helper {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ (N d tree tree₁ x₁ x₂) (N d₁ x x₃ x₄ x₅ ∷ st) cg with <-cmp d d₁ --- replace-helper {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ subt@(N d tree tree₁ x₁ x₂) (N d₁ x x₃ x₄ x₅ ∷ st) cg | tri< a₁ ¬b ¬c = replace-helper ⦃ l ⦄ ⦃ u ⦄ (N d₁ subt x₃ x₄ x₅) st cg --- replace-helper {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ subt@(N d tree tree₁ x₁ x₂) (N d₁ x x₃ x₄ x₅ ∷ st) cg | tri≈ ¬a b ¬c = replace-helper ⦃ l ⦄ ⦃ u ⦄ (N d₁ subt x₃ x₄ x₅) st cg --- replace-helper {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ subt@(N d tree tree₁ x₁ x₂) (N d₁ x x₃ x₄ x₅ ∷ st) cg | tri> ¬a ¬b c = replace-helper ⦃ l ⦄ ⦃ u ⦄ (N d₁ x₃ subt x₄ x₅) st cg --- replace-helper {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ tree (x ∷ st) cg = replace-helper ⦃ l ⦄ ⦃ u ⦄ tree st cg -- Unknown Case - - - --- bt-replace : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ --- → (d : ℕ) → (bt {n} {a} ) → SingleLinkedStack (bt {n} {a} ) --- → Maybe (Σ ℕ (λ d' → _iso_ {n} {a} d d')) → ( (bt {n} {a} ) → t ) → t --- bt-replace {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ d tree st eqP cg = replace-helper {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ ((N ⦃ 0 ⦄ ⦃ 0 ⦄ ⦃ d ⦄ ⦃ d ⦄ d (L ⦃ 0 ⦄ ⦃ d ⦄ z≤n ) (L ⦃ d ⦄ ⦃ d ⦄ ≤-refl) z≤n ≤-refl)) st cg - - - --- -- 証明に insert がはいっててほしい --- bt-insert : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (d : ℕ) → (tree : bt {n} {a}) --- → ((bt {n} {a}) → t) → t +insertTree : {n : Level} {A : Set n} {t : Set n} → (tree : bt A) → (key : ℕ) → (value : A) → (next : bt A → t ) → t +insertTree tree key value exit = find-loop key tree [] ( λ t st → replace-loop key value t st exit ) --- bt-insert {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ d tree cg = bt-find {n} {_} {a} ⦃ l ⦄ ⦃ u ⦄ d tree [] (λ tt st ad → bt-replace ⦃ l ⦄ ⦃ u ⦄ d tt st ad cg ) - --- pickKey : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (tree : bt {n} {a}) → Maybe ℕ --- pickKey (L x) = nothing --- pickKey (N d tree tree₁ x x₁) = just d - --- insert-test : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → bt -- ? --- insert-test {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ = bt-insert {n} {_} {a} ⦃ l ⦄ ⦃ u ⦄ 1 test-node λ x → x - --- insert-test-l : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → bt -- ? --- insert-test-l {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ = bt-insert {n} {_} {a} ⦃ l ⦄ ⦃ u ⦄ 1 (lleaf) λ x → x - - --- insert-lem : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (d : ℕ) → (tree : bt {n} {a}) --- → bt-insert {n} {_} {a} ⦃ l ⦄ ⦃ u ⦄ d tree (λ tree1 → bt-find ⦃ l ⦄ ⦃ u ⦄ d tree1 [] --- (λ tt st ad → (pickKey {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ tt) ≡ just d ) ) - +insertTest1 = insertTree leaf 1 1 (λ x → x ) --- insert-lem d (L x) with <-cmp d d -- bt-insert d (L x) (λ tree1 → {!!}) --- insert-lem d (L x) | tri< a ¬b ¬c = ⊥-elim (¬b refl) --- insert-lem d (L x) | tri≈ ¬a b ¬c = refl --- insert-lem d (L x) | tri> ¬a ¬b c = ⊥-elim (¬b refl) --- insert-lem d (N d₁ tree tree₁ x x₁) with <-cmp d d₁ --- -- bt-insert d (N d₁ tree tree₁ x x₁) (λ tree1 → {!!}) --- insert-lem d (N d₁ tree tree₁ x x₁) | tri≈ ¬a b ¬c with <-cmp d d --- insert-lem d (N d₁ tree tree₁ x x₁) | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ = ⊥-elim (¬b refl) --- insert-lem d (N d₁ tree tree₁ x x₁) | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ = refl --- insert-lem d (N d₁ tree tree₁ x x₁) | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c = ⊥-elim (¬b refl) - --- insert-lem d (N d₁ tree tree₁ x x₁) | tri< a ¬b ¬c = {!!} --- where --- lem-helper : find-support ⦃ {!!} ⦄ ⦃ {!!} ⦄ d tree (N d₁ tree tree₁ x x₁ ∷ []) (λ tt₁ st ad → replace-helper ⦃ {!!} ⦄ ⦃ {!!} ⦄ (N ⦃ {!!} ⦄ ⦃ {!!} ⦄ ⦃ {!!} ⦄ ⦃ {!!} ⦄ d (L ⦃ 0 ⦄ ⦃ d ⦄ z≤n) (L ⦃ {!!} ⦄ ⦃ {!!} ⦄ (≤-reflexive refl)) z≤n (≤-reflexive refl)) st (λ tree1 → find-support ⦃ {!!} ⦄ ⦃ {!!} ⦄ d tree1 [] (λ tt₂ st₁ ad₁ → pickKey {{!!}} {{!!}} {{!!}} {{!!}} ⦃ {!!} ⦄ ⦃ {!!} ⦄ tt₂ ≡ just d))) --- lem-helper = {!!} - --- insert-lem d (N d₁ tree tree₁ x x₁) | tri> ¬a ¬b c = {!!} -
--- a/logic.agda Tue Nov 02 19:32:10 2021 +0900 +++ b/logic.agda Wed Nov 03 10:32:56 2021 +0900 @@ -2,7 +2,7 @@ open import Level open import Relation.Nullary -open import Relation.Binary +open import Relation.Binary hiding (_⇔_) open import Relation.Binary.PropositionalEquality open import Data.Empty