Skip to content

Commit acabfc1

Browse files
brendanzabbrendanzab
committed
Make better use of namespaces
1 parent e961d7f commit acabfc1

File tree

6 files changed

+475
-354
lines changed

6 files changed

+475
-354
lines changed

‎experiments/idris/src/Fathom/Closed/IndexedInductive.idr‎

Lines changed: 72 additions & 89 deletions
Original file line numberDiff line numberDiff line change
@@ -29,77 +29,56 @@ data FormatOf : Type -> Type where
2929
Bind : {0 A : Type} -> {0 B : A -> Type} -> (f : FormatOf A) -> ((x : A) -> FormatOf (B x)) -> FormatOf (x : A ** B x)
3030

3131

32-
-- Support for do notation
32+
namespace FormatOf
3333

34-
public export
35-
pure : {0 A : Type} -> (x : A) -> FormatOf (Sing x)
36-
pure = Pure
34+
-- Support for do notation
3735

38-
public export
39-
(>>=) : {0 A : Type} -> {0 B : A -> Type} -> (f : FormatOf A) -> ((x : A) -> FormatOf (B x)) -> FormatOf (x : A ** B x)
40-
(>>=) = Bind
41-
42-
43-
---------------------------
44-
-- ENCODER/DECODER PAIRS --
45-
---------------------------
46-
47-
48-
export
49-
decode : {0 A, S : Type} -> (f : FormatOf A) -> Decode (A, Colist S) (Colist S)
50-
decode End [] = Just ((), [])
51-
decode End (_::_) = Nothing
52-
decode Fail _ = Nothing
53-
decode (Pure x) buffer =
54-
Just (MkSing x, buffer)
55-
decode (Skip f _) buffer = do
56-
(x, buffer') <- decode f buffer
57-
Just ((), buffer')
58-
decode (Repeat 0 f) buffer =
59-
Just ([], buffer)
60-
decode (Repeat (S len) f) buffer = do
61-
(x, buffer') <- decode f buffer
62-
(xs, buffer'') <- decode (Repeat len f) buffer'
63-
Just (x :: xs, buffer'')
64-
decode (Bind f1 f2) buffer = do
65-
(x, buffer') <- decode f1 buffer
66-
(y, buffer'') <- decode (f2 x) buffer'
67-
Just ((x ** y), buffer'')
68-
69-
-- export
70-
-- decode : {0 A, S : Type} -> (f : FormatOf A) -> Decode (A, Colist S) (Colist S)
71-
-- decode End
72-
-- = \buffer => case buffer of
73-
-- [] => Just ((), [])
74-
-- _::_ => Nothing
75-
-- decode Fail
76-
-- = const Nothing
77-
-- decode (Pure x)
78-
-- = pure (MkSing x)
79-
-- decode (Skip f _)
80-
-- = do _ <- decode f
81-
-- pure ()
82-
-- decode (Repeat 0 f) = pure []
83-
-- decode (Repeat (S len) f)
84-
-- = do x <- decode f
85-
-- xs <- decode (Repeat len f)
86-
-- pure (x :: xs)
87-
-- decode (Bind f1 f2)
88-
-- = do x <- decode f1
89-
-- y <- decode (f2 x)
90-
-- pure (x ** y)
91-
92-
93-
export
94-
encode : {0 A, S : Type} -> (f : FormatOf A) -> Encode A (Colist S)
95-
encode End () = Just []
96-
encode (Pure x) (MkSing _) = Just []
97-
encode (Skip f def) () = encode f def
98-
encode (Repeat Z f) [] = Just []
99-
encode (Repeat (S len) f) (x :: xs) =
100-
[| encode f x <+> encode (Repeat len f) xs |]
101-
encode (Bind f1 f2) (x ** y) =
102-
[| encode f1 x <+> encode (f2 x) y |]
36+
public export
37+
pure : {0 A : Type} -> (x : A) -> FormatOf (Sing x)
38+
pure = Pure
39+
40+
public export
41+
(>>=) : {0 A : Type} -> {0 B : A -> Type} -> (f : FormatOf A) -> ((x : A) -> FormatOf (B x)) -> FormatOf (x : A ** B x)
42+
(>>=) = Bind
43+
44+
45+
---------------------------
46+
-- ENCODER/DECODER PAIRS --
47+
---------------------------
48+
49+
50+
export
51+
decode : {0 A, S : Type} -> (f : FormatOf A) -> Decode (A, Colist S) (Colist S)
52+
decode End [] = Just ((), [])
53+
decode End (_::_) = Nothing
54+
decode Fail _ = Nothing
55+
decode (Pure x) buffer =
56+
Just (MkSing x, buffer)
57+
decode (Skip f _) buffer = do
58+
(x, buffer') <- decode f buffer
59+
Just ((), buffer')
60+
decode (Repeat 0 f) buffer =
61+
Just ([], buffer)
62+
decode (Repeat (S len) f) buffer = do
63+
(x, buffer') <- decode f buffer
64+
(xs, buffer'') <- decode (Repeat len f) buffer'
65+
Just (x :: xs, buffer'')
66+
decode (Bind f1 f2) buffer = do
67+
(x, buffer') <- decode f1 buffer
68+
(y, buffer'') <- decode (f2 x) buffer'
69+
Just ((x ** y), buffer'')
70+
71+
72+
export
73+
encode : {0 A, S : Type} -> (f : FormatOf A) -> Encode A (Colist S)
74+
encode End () = Just []
75+
encode (Pure x) (MkSing _) = Just []
76+
encode (Skip f def) () = encode f def
77+
encode (Repeat Z f) [] = Just []
78+
encode (Repeat (S len) f) (x :: xs) =
79+
[| encode f x <+> encode (Repeat len f) xs |]
80+
encode (Bind f1 f2) (x ** y) =
81+
[| encode f1 x <+> encode (f2 x) y |]
10382
10483
10584
-------------------------
@@ -122,14 +101,32 @@ record Format where
122101
------------------------------------
123102
124103
125-
public export
126-
toFormatOf : (f : Format) -> FormatOf f.Rep
127-
toFormatOf (MkFormat _ f) = f
104+
namespace Format
128105
106+
public export
107+
toFormatOf : (f : Format) -> FormatOf f.Rep
108+
toFormatOf (MkFormat _ f) = f
109+
110+
111+
||| Convert a format description into an indexed format description with an
112+
||| equality proof that the representation is the same as the index.
113+
public export
114+
toFormatOfEq : {0 A : Type} -> (Subset Format (\f => f.Rep = A)) -> FormatOf A
115+
toFormatOfEq (Element f prf) = rewrite sym prf in f.format
129116
130-
public export
131-
toFormat : {0 A : Type} -> FormatOf A -> Format
132-
toFormat f = MkFormat A f
117+
118+
namespace FormatOf
119+
120+
public export
121+
toFormat : {0 A : Type} -> FormatOf A -> Format
122+
toFormat f = MkFormat A f
123+
124+
125+
||| Convert an indexed format description to a existential format description,
126+
||| along with a proof that the representation is the same as the index.
127+
public export
128+
toFormatEq : {0 A : Type} -> FormatOf A -> (Subset Format (\f => f.Rep = A))
129+
toFormatEq f = Element (MkFormat A f) Refl
133130
134131
135132
public export
@@ -142,20 +139,6 @@ toFormatOfIso = MkIso
142139
}
143140
144141
145-
||| Convert a format description into an indexed format description with an
146-
||| equality proof that the representation is the same as the index.
147-
public export
148-
toFormatOfEq : {0 A : Type} -> (Subset Format (\f => f.Rep = A)) -> FormatOf A
149-
toFormatOfEq (Element f prf) = rewrite sym prf in f.format
150-
151-
152-
||| Convert an indexed format description to a existential format description,
153-
||| along with a proof that the representation is the same as the index.
154-
public export
155-
toFormatEq : {0 A : Type} -> FormatOf A -> (Subset Format (\f => f.Rep = A))
156-
toFormatEq f = Element (MkFormat A f) Refl
157-
158-
159142
public export
160143
toFormatOfEqIso : Iso (Exists (\a => (Subset Format (\f => f.Rep = a)))) (Exists FormatOf)
161144
toFormatOfEqIso = MkIso

‎experiments/idris/src/Fathom/Closed/IndexedInductiveCustom.idr‎

Lines changed: 74 additions & 68 deletions
Original file line numberDiff line numberDiff line change
@@ -43,56 +43,58 @@ data FormatOf : (A : Type) -> Type where
4343
Custom : (f : CustomFormat) -> FormatOf f.Rep
4444

4545

46-
-- Support for do notation
46+
namespace FormatOf
4747

48-
public export
49-
pure : {0 A : Type} -> (x : A) -> FormatOf (Sing x)
50-
pure = Pure
48+
-- Support for do notation
5149

52-
public export
53-
(>>=) : {0 A : Type} -> {0 B : A -> Type} -> (f : FormatOf A) -> ((x : A) -> FormatOf (B x)) -> FormatOf (x : A ** B x)
54-
(>>=) = Bind
55-
56-
57-
---------------------------
58-
-- ENCODER/DECODER PAIRS --
59-
---------------------------
60-
61-
62-
export
63-
decode : {0 A : Type} -> (f : FormatOf A) -> Decode (A, ByteStream) (ByteStream)
64-
decode End [] = Just ((), [])
65-
decode End (_::_) = Nothing
66-
decode Fail _ = Nothing
67-
decode (Pure x) buffer =
68-
Just (MkSing x, buffer)
69-
decode (Skip f _) buffer = do
70-
(x, buffer') <- decode f buffer
71-
Just ((), buffer')
72-
decode (Repeat 0 f) buffer =
73-
Just ([], buffer)
74-
decode (Repeat (S len) f) buffer = do
75-
(x, buffer') <- decode f buffer
76-
(xs, buffer'') <- decode (Repeat len f) buffer'
77-
Just (x :: xs, buffer'')
78-
decode (Bind f1 f2) buffer = do
79-
(x, buffer') <- decode f1 buffer
80-
(y, buffer'') <- decode (f2 x) buffer'
81-
Just ((x ** y), buffer'')
82-
decode (Custom f) buffer = f.decode buffer
83-
84-
85-
export
86-
encode : {0 A : Type} -> (f : FormatOf A) -> Encode A (ByteStream)
87-
encode End () = Just []
88-
encode (Pure x) (MkSing _) = Just []
89-
encode (Skip f def) () = encode f def
90-
encode (Repeat Z f) [] = Just []
91-
encode (Repeat (S len) f) (x :: xs) =
92-
[| encode f x <+> encode (Repeat len f) xs |]
93-
encode (Bind f1 f2) (x ** y) =
94-
[| encode f1 x <+> encode (f2 x) y |]
95-
encode (Custom f) x = f.encode x
50+
public export
51+
pure : {0 A : Type} -> (x : A) -> FormatOf (Sing x)
52+
pure = Pure
53+
54+
public export
55+
(>>=) : {0 A : Type} -> {0 B : A -> Type} -> (f : FormatOf A) -> ((x : A) -> FormatOf (B x)) -> FormatOf (x : A ** B x)
56+
(>>=) = Bind
57+
58+
59+
---------------------------
60+
-- ENCODER/DECODER PAIRS --
61+
---------------------------
62+
63+
64+
export
65+
decode : {0 A : Type} -> (f : FormatOf A) -> Decode (A, ByteStream) (ByteStream)
66+
decode End [] = Just ((), [])
67+
decode End (_::_) = Nothing
68+
decode Fail _ = Nothing
69+
decode (Pure x) buffer =
70+
Just (MkSing x, buffer)
71+
decode (Skip f _) buffer = do
72+
(x, buffer') <- decode f buffer
73+
Just ((), buffer')
74+
decode (Repeat 0 f) buffer =
75+
Just ([], buffer)
76+
decode (Repeat (S len) f) buffer = do
77+
(x, buffer') <- decode f buffer
78+
(xs, buffer'') <- decode (Repeat len f) buffer'
79+
Just (x :: xs, buffer'')
80+
decode (Bind f1 f2) buffer = do
81+
(x, buffer') <- decode f1 buffer
82+
(y, buffer'') <- decode (f2 x) buffer'
83+
Just ((x ** y), buffer'')
84+
decode (Custom f) buffer = f.decode buffer
85+
86+
87+
export
88+
encode : {0 A : Type} -> (f : FormatOf A) -> Encode A (ByteStream)
89+
encode End () = Just []
90+
encode (Pure x) (MkSing _) = Just []
91+
encode (Skip f def) () = encode f def
92+
encode (Repeat Z f) [] = Just []
93+
encode (Repeat (S len) f) (x :: xs) =
94+
[| encode f x <+> encode (Repeat len f) xs |]
95+
encode (Bind f1 f2) (x ** y) =
96+
[| encode f1 x <+> encode (f2 x) y |]
97+
encode (Custom f) x = f.encode x
9698
9799
98100
-------------------------
@@ -115,14 +117,32 @@ record Format where
115117
------------------------------------
116118
117119
118-
public export
119-
toFormatOf : (f : Format) -> FormatOf f.Rep
120-
toFormatOf (MkFormat _ f) = f
120+
namespace Format
121121
122+
public export
123+
toFormatOf : (f : Format) -> FormatOf f.Rep
124+
toFormatOf (MkFormat _ f) = f
125+
126+
127+
||| Convert a format description into an indexed format description with an
128+
||| equality proof that the representation is the same as the index.
129+
public export
130+
toFormatOfEq : {0 A : Type} -> (Subset Format (\f => f.Rep = A)) -> FormatOf A
131+
toFormatOfEq (Element f prf) = rewrite sym prf in f.format
122132
123-
public export
124-
toFormat : {0 A : Type} -> FormatOf A -> Format
125-
toFormat f = MkFormat A f
133+
134+
namespace FormatOf
135+
136+
public export
137+
toFormat : {0 A : Type} -> FormatOf A -> Format
138+
toFormat f = MkFormat A f
139+
140+
141+
||| Convert an indexed format description to a existential format description,
142+
||| along with a proof that the representation is the same as the index.
143+
public export
144+
toFormatEq : {0 A : Type} -> FormatOf A -> (Subset Format (\f => f.Rep = A))
145+
toFormatEq f = Element (MkFormat A f) Refl
126146
127147
128148
public export
@@ -135,20 +155,6 @@ toFormatOfIso = MkIso
135155
}
136156
137157
138-
||| Convert a format description into an indexed format description with an
139-
||| equality proof that the representation is the same as the index.
140-
public export
141-
toFormatOfEq : {0 A : Type} -> (Subset Format (\f => f.Rep = A)) -> FormatOf A
142-
toFormatOfEq (Element f prf) = rewrite sym prf in f.format
143-
144-
145-
||| Convert an indexed format description to a existential format description,
146-
||| along with a proof that the representation is the same as the index.
147-
public export
148-
toFormatEq : {0 A : Type} -> FormatOf A -> (Subset Format (\f => f.Rep = A))
149-
toFormatEq f = Element (MkFormat A f) Refl
150-
151-
152158
public export
153159
toFormatOfEqIso : Iso (Exists (\a => (Subset Format (\f => f.Rep = a)))) (Exists FormatOf)
154160
toFormatOfEqIso = MkIso

0 commit comments

Comments
 (0)