Mercurial > hg > Papers > 2022 > soto-sigos
comparison Paper/src/bt_impl/find.agda.replaced @ 0:14a0e409d574
ADD fast commit
| author | soto <soto@cr.ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 24 Apr 2022 23:13:44 +0900 |
| parents | |
| children |
comparison
equal
deleted
inserted
replaced
| -1:000000000000 | 0:14a0e409d574 |
|---|---|
| 1 find : {n m : Level} {A : Set n} {t : Set m} !$\rightarrow$! (env : Env A ) | |
| 2 !$\rightarrow$! (next : (env : Env A ) !$\rightarrow$! t ) | |
| 3 !$\rightarrow$! (exit : (env : Env A ) !$\rightarrow$! t ) !$\rightarrow$! t | |
| 4 find env next exit = find-c (vart env) env next exit where | |
| 5 find-c : {n m : Level} {A : Set n} {t : Set m} !$\rightarrow$! (tree : bt A) !$\rightarrow$! (env : Env A ) | |
| 6 !$\rightarrow$! (next : (env : Env A ) !$\rightarrow$! t ) | |
| 7 !$\rightarrow$! (exit : (env : Env A ) !$\rightarrow$! t ) !$\rightarrow$! t | |
| 8 find-c leaf env next exit = exit env | |
| 9 find-c n@(node key-t value ltree rtree) env next exit with <-cmp (varn env) key-t | |
| 10 ... | tri< a !$\neg$!b !$\neg$!c = find-c ltree record env {vart = ltree ; varl = (n !$\text{::}$! (varl env))} next exit | |
| 11 ... | tri!$\approx$! !$\neg$!a b !$\neg$!c = exit record env {vart = n} | |
| 12 ... | tri> !$\neg$!a !$\neg$!b c = find-c rtree record env {vart = rtree ; varl = (n !$\text{::}$! (varl env))} next exit |