blob: a2500e9db95124b9075bb95fb26a275525db9daa (
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
|
module Core.Thinning
import Data.Fin
-- Definition ------------------------------------------------------------------
data Thinner : Nat -> Nat -> Type where
IsBase : Thinner n (S n)
IsDrop : Thinner m n -> Thinner m (S n)
IsKeep : Thinner m n -> Thinner (S m) (S n)
export
data Thins : Nat -> Nat -> Type where
IsId : n `Thins` n
IsThinner : Thinner m n -> m `Thins` n
%name Thinner thin
%name Thins thin
-- Constructors ----------------------------------------------------------------
export
id : (0 n : Nat) -> n `Thins` n
id n = IsId
export
drop : m `Thins` n -> m `Thins` S n
drop IsId = IsThinner IsBase
drop (IsThinner thin) = IsThinner (IsDrop thin)
export
keep : m `Thins` n -> S m `Thins` S n
keep IsId = IsId
keep (IsThinner thin) = IsThinner (IsKeep thin)
-- Non-Identity ----------------------------------------------------------------
export
data IsNotId : m `Thins` n -> Type where
ItIsThinner : IsNotId (IsThinner thin)
%name IsNotId prf
-- Views -----------------------------------------------------------------------
public export
data View : m `Thins` n -> Type where
Id : (0 n : Nat) -> View (id n)
Drop : (thin : m `Thins` n) -> View (drop thin)
Keep : (thin : m `Thins` n) -> {auto 0 prf : IsNotId thin} -> View (keep thin)
export
view : (thin : m `Thins` n) -> View thin
view IsId = Id m
view (IsThinner IsBase) = Drop (id _)
view (IsThinner (IsDrop thin)) = Drop (IsThinner thin)
view (IsThinner (IsKeep thin)) = Keep (IsThinner thin)
-- Weakening -------------------------------------------------------------------
wkn' : Fin m -> Thinner m n -> Fin n
wkn' i IsBase = FS i
wkn' i (IsDrop thin) = FS (wkn' i thin)
wkn' FZ (IsKeep thin) = FZ
wkn' (FS i) (IsKeep thin) = FS (wkn' i thin)
export
wkn : Fin m -> m `Thins` n -> Fin n
wkn i IsId = i
wkn i (IsThinner thin) = wkn' i thin
-- Composition -----------------------------------------------------------------
comp : Thinner m n -> Thinner k m -> Thinner k n
comp IsBase thin2 = IsDrop thin2
comp (IsDrop thin1) thin2 = IsDrop (comp thin1 thin2)
comp (IsKeep thin1) IsBase = IsDrop thin1
comp (IsKeep thin1) (IsDrop thin2) = IsDrop (comp thin1 thin2)
comp (IsKeep thin1) (IsKeep thin2) = IsKeep (comp thin1 thin2)
export
(.) : m `Thins` n -> k `Thins` m -> k `Thins` n
IsId . thin2 = thin2
IsThinner thin1 . IsId = IsThinner thin1
IsThinner thin1 . IsThinner thin2 = IsThinner (comp thin1 thin2)
|
