blob: d1e77455467786108b24166df4bba65614f6f9d4 (
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
|
module CC.Thinning
import Data.Singleton
-- Definition ------------------------------------------------------------------
export
data Thins : (src, tgt : SnocList a) -> Type where
IsDone : [<] `Thins` [<]
IsDrop : src `Thins` tgt -> src `Thins` tgt :< x
IsKeep : src `Thins` tgt -> src :< x `Thins` tgt :< x
%name Thins thin
-- Operations ------------------------------------------------------------------
export
done : [<] `Thins` [<]
done = IsDone
export
drop : src `Thins` tgt -> src `Thins` tgt :< x
drop thin = IsDrop thin
export
keep : src `Thins` tgt -> src :< x `Thins` tgt :< x
keep thin = IsKeep thin
export
empty : {ctx : SnocList a} -> [<] `Thins` ctx
empty {ctx = [<]} = done
empty {ctx = _ :< _} = drop empty
export
id : {ctx : SnocList a} -> ctx `Thins` ctx
id {ctx = [<]} = done
id {ctx = _ :< _} = keep id
export
id' : Singleton ctx -> ctx `Thins` ctx
id' (Val ctx) = id
export
(++) : src1 `Thins` tgt1 -> src2 `Thins` tgt2 -> src1 ++ src2 `Thins` tgt1 ++ tgt2
thin ++ IsDone = thin
thin ++ IsDrop thin' = IsDrop (thin ++ thin')
thin ++ IsKeep thin' = IsKeep (thin ++ thin')
-- Views -----------------------------------------------------------------------
public export
data View : src `Thins` tgt -> Type where
Done : View CC.Thinning.done
Drop : (thin : src `Thins` tgt) -> View (drop thin)
Keep : (thin : src `Thins` tgt) -> View (keep thin)
%name View view
public export
view : (thin : src `Thins` tgt) -> View thin
view IsDone = Done
view (IsDrop thin) = Drop thin
view (IsKeep thin) = Keep thin
|
