Mercurial > hg > Papers > 2023 > soto-master

annotate Paper/src/bt_impl/replace.agda @ 32:4915eaa51ee0 default tip

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add front
author soto <soto@cr.ie.u-ryukyu.ac.jp>
date Thu, 23 Feb 2023 18:39:56 +0900
parents a72446879486
children
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
1
a72446879486 Init paper
soto <soto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 replace : {n m : Level} {A : Set n} {t : Set m} → (env : Env A )
a72446879486 Init paper
soto <soto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
2 → (next : Env A → t )
a72446879486 Init paper
soto <soto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 → (exit : Env A → t) → t
a72446879486 Init paper
soto <soto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 replace env next exit = replace-c (varl env) env next exit where
a72446879486 Init paper
soto <soto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
5 replace-c : {n m : Level} {A : Set n} {t : Set m} → List (bt A) → (env : Env A )
a72446879486 Init paper
soto <soto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
6 → (next : Env A → t )
a72446879486 Init paper
soto <soto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
7 → (exit : Env A → t) → t
a72446879486 Init paper
soto <soto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
8 replace-c st env next exit with st
a72446879486 Init paper
soto <soto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 ... | [] = exit env
a72446879486 Init paper
soto <soto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 ... | leaf ∷ st1 = replace-c st1 env next exit
a72446879486 Init paper
soto <soto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 ... | n@(node key-t value ltree rtree) ∷ st1 with <-cmp (varn env) (key-t)
a72446879486 Init paper
soto <soto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
12 ... | tri< a ¬b ¬c = replace-c st1 record env{vart = (node key-t value (vart env) rtree); varl = st1} next exit
a72446879486 Init paper
soto <soto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 ... | tri≈ ¬a b ¬c = replace-c st1 record env{vart = (node key-t (varv env) ltree rtree); varl = st1} next exit
a72446879486 Init paper
soto <soto@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 ... | tri> ¬a ¬b c = replace-c st1 record env{vart = (node key-t value ltree (vart env)); varl = st1} next exit