blob: 465e92c8501dc424291bd3f5c54ab32e40d8f877 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
|
module Inky.Data.SnocList.Elem
import public Data.SnocList.Elem
import Data.DPair
import Data.Nat
import Data.Singleton
import Inky.Decidable
import Inky.Decidable.Maybe
import Inky.Data.Assoc
import Inky.Data.SnocList
export
Uninhabited (Here {sx, x} ~=~ There {sx = sy, x = z, y} i) where
uninhabited Refl impossible
export
Uninhabited (There {sx = sy, x = z, y} i ~=~ Here {sx, x}) where
uninhabited Refl impossible
export
thereCong :
{0 i : Elem x sx} -> {0 j : Elem y sx} -> i = j ->
There {y = z} i = There {y = z} j
thereCong Refl = Refl
export
toNatCong : {0 i : Elem x sx} -> {0 j : Elem y sx} -> i = j -> elemToNat i = elemToNat j
toNatCong Refl = Refl
export
thereInjective :
{0 i : Elem x sx} -> {0 j : Elem y sx} -> There {y = z} i = There {y = z} j ->
i = j
thereInjective Refl = Refl
export
toNatInjective : {i : Elem x sx} -> {j : Elem y sx} -> (0 _ : elemToNat i = elemToNat j) -> i = j
toNatInjective {i = Here} {j = Here} prf = Refl
toNatInjective {i = There i} {j = There j} prf with (toNatInjective {i} {j} $ injective prf)
toNatInjective {i = There i} {j = There .(i)} prf | Refl = Refl
-- Decidable Equality -----------------------------------------------------------
public export
reflectEq : (i : Elem x sx) -> (j : Elem y sx) -> (i = j) `When` (elemToNat i == elemToNat j)
reflectEq Here Here = Refl
reflectEq Here (There j) = absurd
reflectEq (There i) Here = absurd
reflectEq (There i) (There j) = mapWhen thereCong thereInjective $ reflectEq i j
public export
decEq : (i : Elem x sx) -> (j : Elem y sx) -> Dec' (i = j)
decEq i j = (elemToNat i == elemToNat j) `Because` reflectEq i j
-- Weakening -------------------------------------------------------------------
public export
wknL : Elem x sx -> LengthOf sy -> Elem x (sx ++ sy)
wknL pos Z = pos
wknL pos (S len) = There (wknL pos len)
public export
wknR : Elem x sx -> Elem x (sy ++ sx)
wknR Here = Here
wknR (There pos) = There (wknR pos)
public export
split : LengthOf sy -> Elem x (sx ++ sy) -> Either (Elem x sx) (Elem x sy)
split Z pos = Left pos
split (S len) Here = Right Here
split (S len) (There pos) = mapSnd There $ split len pos
-- Lookup ----------------------------------------------------------------------
export
nameOf : {sx : SnocList a} -> Elem x sx -> Singleton x
nameOf Here = Val x
nameOf (There pos) = nameOf pos
-- Search ----------------------------------------------------------------------
export
lookup : DecEq' a => (x : a) -> (sx : SnocList a) -> Maybe (Elem x sx)
lookup x [<] = Nothing
lookup x (sx :< y) =
case decEq x y of
True `Because` Refl => Just Here
False `Because` _ => There <$> lookup x sx
public export
decLookup : (n : String) -> (sx : SnocList (Assoc a)) -> DecWhen a (\x => Elem (n :- x) sx)
decLookup n [<] = Nothing `Because` (\_ => absurd)
decLookup n (sx :< (k :- x)) =
map (maybe x id) leftToRight rightToLeft $
first (decEq n k) (decLookup n sx)
where
leftToRight :
forall n. (m : Maybe a) ->
maybe (n = k) (\y => Elem (n :- y) sx) m ->
Elem (n :- maybe x Basics.id m) (sx :< (k :- x))
leftToRight Nothing Refl = Here
leftToRight (Just _) prf = There prf
rightToLeft :
forall n.
(Not (n = k), (y : a) -> Not (Elem (n :- y) sx)) ->
(y : a) -> Not (Elem (n :- y) (sx :< (k :- x)))
rightToLeft (neq, contra) _ Here = neq Refl
rightToLeft (neq, contra) y (There i) = contra y i
|
