|
1
|
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≈ !$\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 |
