1
------------------------------------------------------------------------
2
-- Pointers into star-lists
3
------------------------------------------------------------------------
5
module Data.Star.Pointer where
8
open import Data.Star.Decoration
9
open import Relation.Binary
10
open import Data.Maybe using (Maybe; nothing; just)
12
open import Data.Function
15
-- Pointers into star-lists. The edge pointed to is decorated with Q,
16
-- while other edges are decorated with P.
18
data Pointer {I : Set} {T : Rel I zero} (P Q : EdgePred T)
19
: Rel (Maybe (NonEmpty (Star T))) zero where
20
step : ∀ {i j k} {x : T i j} {xs : Star T j k}
21
(p : P x) → Pointer P Q (just (nonEmpty (x ◅ xs)))
23
done : ∀ {i j k} {x : T i j} {xs : Star T j k}
24
(q : Q x) → Pointer P Q (just (nonEmpty (x ◅ xs))) nothing
26
-- Any P Q xs means that some edge in xs satisfies Q, while all
27
-- preceding edges satisfy P. A star-list of type Any Always Always xs
28
-- is basically a prefix of xs; the existence of such a prefix
29
-- guarantees that xs is non-empty.
31
Any : ∀ {I} {T : Rel I zero} (P Q : EdgePred T) → EdgePred (Star T)
32
Any P Q xs = Star (Pointer P Q) (just (nonEmpty xs)) nothing
34
this : ∀ {I} {T : Rel I zero} {P Q : EdgePred T}
35
{i j k} {x : T i j} {xs : Star T j k} →
36
Q x → Any P Q (x ◅ xs)
39
that : ∀ {I} {T : Rel I zero} {P Q : EdgePred T}
40
{i j k} {x : T i j} {xs : Star T j k} →
41
P x → Any P Q xs → Any P Q (x ◅ xs)
46
data Result {I : Set} (T : Rel I zero) (P Q : EdgePred T) : Set where
47
result : ∀ {i j} {x : T i j}
48
(p : P x) (q : Q x) → Result T P Q
50
-- The first argument points out which edge to extract. The edge is
51
-- returned, together with proofs that it satisfies Q and R.
53
lookup : ∀ {I} {T : Rel I zero} {P Q R : EdgePred T}
54
{i j} {xs : Star T i j} →
55
Any P Q xs → All R xs → Result T Q R
56
lookup (done q ◅ ε) (↦ r ◅ _) = result q r
57
lookup (step p ◅ ps) (↦ r ◅ rs) = lookup ps rs
58
lookup (done _ ◅ () ◅ _) _
60
-- We can define something resembling init.
62
prefixIndex : ∀ {I} {T : Rel I zero} {P Q : EdgePred T}
63
{i j} {xs : Star T i j} →
65
prefixIndex (done {i = i} q ◅ _) = i
66
prefixIndex (step p ◅ ps) = prefixIndex ps
68
prefix : ∀ {I} {T : Rel I zero} {P Q : EdgePred T} {i j} {xs : Star T i j} →
69
(ps : Any P Q xs) → Star T i (prefixIndex ps)
70
prefix (done q ◅ _) = ε
71
prefix (step {x = x} p ◅ ps) = x ◅ prefix ps
73
-- Here we are taking the initial segment of ps (all elements but the
74
-- last, i.e. all edges satisfying P).
76
init : ∀ {I} {T : Rel I zero} {P Q : EdgePred T} {i j} {xs : Star T i j} →
77
(ps : Any P Q xs) → All P (prefix ps)
79
init (step p ◅ ps) = ↦ p ◅ init ps
81
-- One can simplify the implementation by not carrying around the
82
-- indices in the type:
84
last : ∀ {I} {T : Rel I zero} {P Q : EdgePred T}
85
{i j} {xs : Star T i j} →
86
Any P Q xs → NonEmptyEdgePred T Q
87
last ps with lookup ps (decorate (const tt) _)
88
... | result q _ = nonEmptyEdgePred q
added
removed
src/Data/Star/Pointer.agda
