|
0
|
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 |
