blob: 1c8f41f05b53d219c4d3c3775673a66fecd25c9b (
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
|
module Core.Thinning
import Core.Context
-- Definition ------------------------------------------------------------------
data Thinner : Context -> Context -> Type where
IsBase : (0 n : Name) -> Thinner sx (sx :< n)
IsDrop : Thinner sx sy -> (0 n : Name) -> Thinner sx (sy :< n)
IsKeep : Thinner sx sy -> (0 n : Name) -> Thinner (sx :< n) (sy :< n)
export
data Thins : Context -> Context -> Type where
IsId : sx `Thins` sx
IsThinner : Thinner sx sy -> sx `Thins` sy
%name Thinner thinner
%name Thins thin
export
data IsNotId : sx `Thins` sy -> Type where
ItIsThinner : IsNotId (IsThinner thinner)
-- Constructors ----------------------------------------------------------------
export
id : (0 sx : Context) -> sx `Thins` sx
id sx = IsId
export
drop : sx `Thins` sy -> (0 n : Name) -> sx `Thins` sy :< n
drop IsId n = IsThinner (IsBase n)
drop (IsThinner thinner) n = IsThinner (IsDrop thinner n)
export
keep : sx `Thins` sy -> (0 n : Name) -> sx :< n `Thins` sy :< n
keep IsId n = IsId
keep (IsThinner thinner) n = IsThinner (IsKeep thinner n)
-- Views -----------------------------------------------------------------------
public export
data View : sx `Thins` sy -> Type where
Id : (0 sx : Context) -> View (id sx)
Drop : (thin : sx `Thins` sy) -> (0 n : Name) -> View (drop thin n)
Keep :
(thin : sx `Thins` sy) ->
(0 n : Name) ->
(0 prf : IsNotId thin) -> -- For uniqueness
View (keep thin n)
%name View view
export
view : (thin : sx `Thins` sy) -> View thin
view IsId = Id sx
view (IsThinner (IsBase n)) = Drop IsId n
view (IsThinner (IsDrop thinner n)) = Drop (IsThinner thinner) n
view (IsThinner (IsKeep thinner n)) = Keep (IsThinner thinner) n ItIsThinner
-- Operations ------------------------------------------------------------------
comp : Thinner sy sz -> Thinner sx sy -> sx `Thins` sz
comp (IsBase n) thinner1 = drop (IsThinner thinner1) n
comp (IsDrop thinner2 n) thinner1 = drop (comp thinner2 thinner1) n
comp (IsKeep thinner2 n) (IsBase n) = drop (IsThinner thinner2) n
comp (IsKeep thinner2 n) (IsDrop thinner1 n) = drop (comp thinner2 thinner1) n
comp (IsKeep thinner2 n) (IsKeep thinner1 n) = keep (comp thinner2 thinner1) n
export
(.) : sy `Thins` sz -> sx `Thins` sy -> sx `Thins` sz
IsId . thin1 = thin1
(IsThinner thinner2) . IsId = IsThinner thinner2
(IsThinner thinner2) . (IsThinner thinner1) = comp thinner2 thinner1
|
