blob: 5781eaafba4d895ef9e1a005678706b1a764a13a (
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
|
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)
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
|
