Mercurial > hg > Papers > 2021 > soto-prosym
comparison Paper/src/bt_impl/replace.agda.replaced @ 5:339fb67b4375
INIT rbt.agda
| author | soto <soto@cr.ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 07 Nov 2021 00:51:16 +0900 |
| parents | |
| children |
comparison
equal
deleted
inserted
replaced
| 4:72667e8198e2 | 5:339fb67b4375 |
|---|---|
| 1 replace : {n m : Level} {A : Set n} {t : Set m} !$\rightarrow$! (env : Env A ) | |
| 2 !$\rightarrow$! (next : Env A !$\rightarrow$! t ) | |
| 3 !$\rightarrow$! (exit : Env A !$\rightarrow$! t) !$\rightarrow$! t | |
| 4 replace env next exit = replace-c (varl env) env next exit where | |
| 5 replace-c : {n m : Level} {A : Set n} {t : Set m} !$\rightarrow$! List (bt A) !$\rightarrow$! (env : Env A ) | |
| 6 !$\rightarrow$! (next : Env A !$\rightarrow$! t ) | |
| 7 !$\rightarrow$! (exit : Env A !$\rightarrow$! t) !$\rightarrow$! t | |
| 8 replace-c st env next exit with st | |
| 9 ... | [] = exit env | |
| 10 ... | leaf !$\text{::}$! st1 = replace-c st1 env next exit | |
| 11 ... | n@(node key-t value ltree rtree) !$\text{::}$! st1 with <-cmp (varn env) (key-t) | |
| 12 ... | tri< a !$\neg$!b !$\neg$!c = replace-c st1 record env{vart = (node key-t value (vart env) rtree); varl = st1} next exit | |
| 13 ... | tri!$\approx$! !$\neg$!a b !$\neg$!c = replace-c st1 record env{vart = (node key-t (varv env) ltree rtree); varl = st1} next exit | |
| 14 ... | tri> !$\neg$!a !$\neg$!b c = replace-c st1 record env{vart = (node key-t value ltree (vart env)); varl = st1} next exit |