Mercurial > hg > Gears > GearsAgda

changeset 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
files hoareBinaryTree.agda
diffstat 1 files changed, 20 insertions(+), 18 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree.agda	Thu Jan 16 16:04:59 2020 +0900
+++ b/hoareBinaryTree.agda	Thu Jan 16 17:53:47 2020 +0900
@@ -66,14 +66,14 @@
 --
 --  no children , having left node , having right node , having both
 --
-data bt' {n : Level} (A : Set n) : (key : ℕ) →  Set n where --  (a : Setn)
+data bt' {n : Level} { l r : ℕ } (A : Set n) : (key : ℕ) →  Set n where --  (a : Setn)
   bt'-leaf : (key : ℕ) → bt' A key
   bt'-node : { l r : ℕ } → (key : ℕ) → (value : A) →
-             bt' {n} A l  → bt' {n} A r → l ≤ key → key ≤ r → bt' A key
+             bt' {n} {{!!}} {{!!}} A l  → bt' {n} {{!!}} {{!!}} 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
-  bt'-right : (key : ℕ) → {right-key : ℕ} → (bt' A right-key ) → (right-key ≤ key) → bt'-path A
+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)))
@@ -95,31 +95,33 @@
 reverse した stack を使って find をチェックするかんじ?
 --}
 
+
 tree+stack : {n m : Level} {A : Set n} {t : Set m} {tn : ℕ} →  (tree mtree : bt' A tn )
-  → (stack : List (bt'-path A )) → Set n
-tree+stack tree mtree [] = tree ≡ mtree
-tree+stack {n} {m} {A} {t} {tn} tree mtree (bt'-left key x x₁ ∷ stack) = (mtree ≡ {!!}) ∧ (tree+stack {n} {_} {_} {_} {tn} tree {!!} stack)
-tree+stack {n} {m} {A} {t} {tn} tree mtree (bt'-right key x x₁ ∷ stack) = (mtree ≡ {!!}) ∧ (tree+stack {n} {_} {_} {_} {tn} tree {!!} stack)
+  → (stack : List (bt'-path A tn)) → Set n
+tree+stack tree mtree [] = tree ≡ mtree -- fin case
+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)
+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)
+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)
 -- tree+stack tree mtree (bt'-right key {rkey} x x₁ ∷ stack) = (mtree ≡ {!!}) ∧ (tree+stack tree {!!} stack) -- tn ≡ rkey がひつよう
 
 tree+stack≡tree : {n m : Level} {A : Set n} {t : Set m} {tn : ℕ} →  (tree mtree : bt' A tn )
-  → (stack : List (bt'-path A )) →  (reverse stack) ≡ {!!}
+  → (stack : List (bt'-path A tn)) →  (reverse stack) ≡ {!!}
 tree+stack≡tree tree (bt'-leaf key) stack = {!!}
 tree+stack≡tree tree (bt'-node key value mtree mtree₁ x x₁) stack = {!!}
 
-bt-find' : {n m : Level} {A : Set n} {t : Set m} {tn : ℕ} → (key : ℕ) → (tree : bt' A tn ) → List (bt'-path A )
-    → ( {key1 : ℕ } → bt' A  key1 → List (bt'-path A ) → t ) → t
+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 {key₁} tr (<⇒≤ a) )  ∷ stack)  next
+         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 {key₁} tr (<⇒≤ c) )  ∷ stack)  next
+         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 )
-    → ( {key1 : ℕ } → bt' A  key1 → List (bt'-path A ) → t ) → t
+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 = {!!}
 
@@ -135,10 +137,10 @@
 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 )
+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 : {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