blob: cc7c0886f16f079bec31adef38e405e2745a2c23 (
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
|
module Inky.Data.SnocList.Var
import public Inky.Data.SnocList.Elem
import Data.Singleton
import Inky.Data.SnocList
import Inky.Decidable
export
prefix 2 %%
public export
record Var (sx : SnocList a) where
constructor (%%)
0 name : a
{auto pos : Elem name sx}
%name Var i, j, k
public export
toVar : Elem x sx -> Var sx
toVar pos = (%%) x {pos}
public export
ThereVar : Var sx -> Var (sx :< x)
ThereVar i = toVar (There i.pos)
export
Show (Var sx) where
show i = show (elemToNat i.pos)
-- Basic Properties ---------------------------------------------------------
export
toVarCong : {0 i : Elem x sx} -> {0 j : Elem y sx} -> i = j -> toVar i = toVar j
toVarCong Refl = Refl
export
posCong : {0 i, j : Var sx} -> i = j -> i.pos ~=~ j.pos
posCong Refl = Refl
export
toVarInjective : {i : Elem x sx} -> {j : Elem y sx} -> (0 _ : toVar i = toVar j) -> i = j
toVarInjective prf = toNatInjective $ toNatCong $ posCong prf
export
posInjective : {i : Var sx} -> {j : Var sx} -> (0 _ : i.pos ~=~ j.pos) -> i = j
posInjective {i = %% x} {j = %% y} prf = irrelevantEq $ toVarCong prf
-- Decidable Equality ----------------------------------------------------------
public export
DecEq' (Var {a} sx) where
does i j = (decEq i.pos j.pos).does
reason i j =
mapWhen (\prf => irrelevantEq $ posInjective prf) posCong $
(decEq i.pos j.pos).reason
-- Weakening -------------------------------------------------------------------
public export
wknL : (len : LengthOf sy) => Var sx -> Var (sx ++ sy)
wknL i = toVar $ wknL i.pos len
public export
wknR : Var sx -> Var (sy ++ sx)
wknR i = toVar $ wknR i.pos
public export
split : {auto len : LengthOf sy} -> Var (sx ++ sy) -> Either (Var sx) (Var sy)
split i = bimap toVar toVar $ split len i.pos
public export
lift1 :
(Var sx -> Var sy) ->
Var (sx :< x) -> Var (sy :< y)
lift1 f ((%%) x {pos = Here}) = %% y
lift1 f ((%%) name {pos = There i}) = ThereVar (f $ %% name)
-- Names -----------------------------------------------------------------------
export
nameOf : {sx : SnocList a} -> (i : Var sx) -> Singleton i.name
nameOf i = nameOf i.pos
-- Search ----------------------------------------------------------------------
export
lookup : DecEq' a => (x : a) -> (sx : SnocList a) -> Maybe (Var sx)
lookup x sx = toVar <$> lookup x sx
|
