Mercurial > hg > Papers > 2021 > soto-prosym

comparison Paper/src/bt_verif/find.agda @ 5:339fb67b4375

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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 findP : {n m : Level} {A : Set n} {t : Set m} → (env : Env A)
2 → treeInvariant env ∧ stackInvariant env
3 → (exit : (env : Env A) → treeInvariant env ∧ stackInvariant env → t ) → t
4 findP env Cond exit = findP-c (vart env) env Cond exit where
5 findP-c : {n m : Level} {A : Set n} {t : Set m} → (tree : bt A) → (env : Env A)
6 → treeInvariant env ∧ stackInvariant env
7 → (exit : (env : Env A) → treeInvariant env ∧ stackInvariant env → t ) → t
8 findP-c leaf env Cond exit = exit env Cond
9 findP-c n@(node key-t value ltree rtree) env Cond exit with <-cmp key-t (varn env)
10 ... | tri< a ¬b ¬c = findP-c ltree record env {vart = ltree ; varl = (n ∷ (varl env))} {!!} exit
11 ... | tri≈ ¬a b ¬c = exit record env {vart = n} {!!}
12 ... | tri> ¬a ¬b c = findP-c rtree record env {vart = rtree ; varl = (n ∷ (varl env))} {!!} exit