Mercurial > hg > Papers > 2021 > soto-prosym
view bt/bt.agda @ 3:71a1b18f3d5a
add bt agda source
author | soto <soto@cr.ie.u-ryukyu.ac.jp> |
---|---|
date | Sat, 06 Nov 2021 19:45:49 +0900 |
parents | |
children | 72667e8198e2 |
line wrap: on
line source
module bt where open import Data.Nat open import Level renaming (zero to Z ; suc to succ) open import Data.List open import Data.Nat.Properties as NatProp -- <-cmp open import Relation.Binary open import Function as F hiding (const) data bt {n : Level} (A : Set n) : Set n where leaf : bt A node : (key-t : ℕ) → (value : A) → (ltree : bt A ) → (rtree : bt A ) → bt A record Env {n : Level} (A : Set n) : Set n where field varn : ℕ varv : A vart : bt A varl : List (bt A) open Env {- bt-depth : {n : Level} {A : Set n} → (env : Env A ) → ℕ bt-depth env with vart env ... | leaf = zero ... | node key value ltree rtree = Data.Nat._⊔_ (bt-depth-c ltree ) (bt-depth-c rtree ) where bt-depth-c : {n : Level} {A : Set n} → (tree : bt A ) → ℕ bt-depth-c leaf = suc zero bt-depth-c (node key value lt rt) = suc (Data.Nat._⊔_ (bt-depth-c lt ) ( bt-depth-c rt)) -} bt-depth : {n : Level} {A : Set n} → (tree : bt A ) → ℕ bt-depth leaf = 0 bt-depth (node key value t t₁) = Data.Nat._⊔_ (bt-depth t ) (bt-depth t₁ ) bt-depth1 : {n : Level} {A : Set n} → (env : Env A ) → ℕ bt-depth1 env with vart env ... | tree = bt-depth-c tree where bt-depth-c : {n : Level} {A : Set n} → (tree : bt A ) → ℕ bt-depth-c leaf = zero bt-depth-c (node key value lt rt) = suc (Data.Nat._⊔_ (bt-depth-c lt ) ( bt-depth-c rt)) test-depth : ℕ test-depth = bt-depth (node 3 0 leaf (node 1 1 leaf (node 3 5 leaf leaf))) test-env : {n : Level} {A : Set n} → Env ℕ test-env = record {varn = 0; varv = 4 ; vart = (node 3 2 leaf (node 1 1 leaf (node 3 5 leaf leaf))); varl = []} test-depth1 : ℕ test-depth1 = bt-depth1 record {varn = 0; varv = 4; vart = (node 3 0 leaf (node 1 1 leaf (node 3 5 leaf leaf))); varl = []} find : {n m : Level} {A : Set n} {t : Set m} → (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) find1 : {n m : Level} {A : Set n} {t : Set m} → (env : Env A ) → (next : (env : Env A ) → t ) → (exit : (env : Env A ) → t ) → t find1 env next exit = find1-c (varn env) (vart env) env next exit where find1-c : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree : bt A) → (env : Env A ) → (next : (env : Env A ) → t ) → (exit : (env : Env A ) → t ) → t find1-c key leaf env next exit = exit env find1-c key n@(node key-t value ltree rtree) env next exit with <-cmp key key-t ... | tri< a ¬b ¬c = find1-c key ltree record env {vart = ltree ; varl = (n ∷ (varl env))} next exit ... | tri≈ ¬a b ¬c = exit record env {vart = n} ... | tri> ¬a ¬b c = find1-c key rtree record env {vart = rtree ; varl = (n ∷ (varl env))} next exit {- ... | leaf = exit env ... | n@(node key-t value ltree rtree) with <-cmp (varn env) key-t ... | tri≈ ¬a b ¬c = exit record env {vart = n} ... | tri< a ¬b ¬c = find1 record env {vart = ltree ; varl = (n ∷ (varl env))} next exit ... | tri> ¬a ¬b c = find1 record env {vart = rtree ; varl = (n ∷ (varl env))} next exit -} {-# TERMINATING #-} find-loop : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → bt A → List (bt A) → (exit : bt A → List (bt A) → t) → t find-loop {n} {m} {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-loop-1 : {n m : Level} {A : Set n} {t : Set m} → (env : Env A ) → (exit : (env : Env A ) → t) → t find-loop-1 env exit = find1 env exit exit fin-cg : {n m : Level} {A : Set n} {t : Set m} → t → (env : Env A ) → Env A fin-cg t = (λ env → env ) test-cg = find-loop-1 record {varn = 5; varv = 4; vart = (node 2 2 (node 1 1 leaf leaf) (node 4 4 leaf (node 5 5 leaf leaf))); varl = []} (λ env → env ) replaceNode : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (value : A) → bt A → (bt A → t) → t replaceNode k v leaf next = next (node k v leaf leaf) replaceNode k v (node key value t t₁) next = next (node k v t t₁) replaceNode1 : {n m : Level} {A : Set n} {t : Set m} → (env : Env A ) → (next : Env A → t) → t replaceNode1 env next with vart env ... | leaf = next record env {vart = (node (varn env) (varv env) leaf leaf) } ... | node key-t value ltree rtree = next record env {vart = (node (varn env) (varv env) ltree rtree) } replace : {n m : Level} {A : Set n} {t : Set m} → (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 replace1 : {n m : Level} {A : Set n} {t : Set m} → (env : Env A ) → (next : Env A → t ) → (exit : Env A → t) → t replace1 env next exit = replace1-c (varl env) env next exit where replace1-c : {n m : Level} {A : Set n} {t : Set m} → List (bt A) → (env : Env A ) → (next : Env A → t ) → (exit : Env A → t) → t replace1-c st env next exit with st ... | [] = exit env ... | leaf ∷ st1 = replace1-c st1 env next exit ... | n@(node key-t value ltree rtree) ∷ st1 with <-cmp (varn env) (key-t) ... | tri< a ¬b ¬c = replace1-c st1 record env{vart = (node key-t value (vart env) rtree); varl = st1} next exit ... | tri≈ ¬a b ¬c = replace1-c st1 record env{vart = (node key-t (varv env) ltree rtree); varl = st1} next exit ... | tri> ¬a ¬b c = replace1-c st1 record env{vart = (node key-t value ltree (vart env)); varl = st1} next exit {- replace1 env next exit = next env replace1 env tree (node key₁ value₁ left right ∷ st) next exit with <-cmp (varn env) 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 -} {-# TERMINATING #-} replace-loop : {n m : Level} {A : Set n} {t : Set m} → (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 insertTree : {n m : Level} {A : Set n} {t : Set m} → (tree : bt A) → (key : ℕ) → (value : A) → (next : bt A → t ) → t insertTree tree key value exit = find-loop key tree [] $ λ t st → replaceNode key value t -- find-loop next $ λ t1 → replace-loop key value t1 st exit -- replaceNode exit replace-loop1 : {n m : Level} {A : Set n} {t : Set m} → (env : Env A ) → (exit : (env : Env A ) → t) → t replace-loop1 env exit = replace1 env exit exit insertTree1 : {n m : Level} {A : Set n} {t : Set m} → (tree : bt A) → (key : ℕ) → (value : A) → (next : Env A → t ) → t insertTree1 tree key value exit = find-loop-1 record{varn = key; varv = value; vart = tree ; varl = []} $ λ env → replaceNode1 env $ λ env → replace-loop1 env exit insertTree11 : {n m : Level} {A : Set n} {t : Set m} → (tree : bt A) → (key : ℕ) → (value : A) → (next : Env A → t ) → t insertTree11 tree key value exit = find-loop-1 record{varn = key; varv = value; vart = tree ; varl = []} $ λ env → replaceNode1 env exit test-insert = insertTree1 (node 2 2 (node 1 1 leaf leaf) (node 4 4 leaf (node 5 5 leaf leaf))) 0 5 (λ env → env ) test-insert1 = insertTree11 (node 2 2 (node 1 1 leaf leaf) (node 4 4 leaf (node 5 5 leaf leaf))) 0 5 (λ env → env )