Skip to content

Commit 8f5a720

Browse files
brendanzabbrendanzab
committed
Rename ‘skip’ formats to ‘ignore’
1 parent aaa95c9 commit 8f5a720

File tree

7 files changed

+49
-44
lines changed

7 files changed

+49
-44
lines changed

‎experiments/idris/src/Fathom/Base.idr‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -83,6 +83,11 @@ namespace DecodePart
8383
Prelude.map (\(source, target') => (f source, target)) (decode target)
8484

8585

86+
public export
87+
ignore :{0 S, T : Type} -> DecodePart S T -> DecodePart () T
88+
ignore = map (const ())
89+
90+
8691
public export
8792
bind : {0 S1, S2, T : Type} -> DecodePart S1 T -> (S1 -> DecodePart S2 T) -> DecodePart S2 T
8893
bind decode1 decode2 target = do

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

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -24,7 +24,7 @@ data FormatOf : Type -> Type where
2424
End : FormatOf Unit
2525
Fail : FormatOf Void
2626
Pure : {0 A : Type} -> (x : A) -> FormatOf (Sing x)
27-
Skip : {0 A : Type} -> (f : FormatOf A) -> (def : A) -> FormatOf Unit
27+
Ignore : {0 A : Type} -> (f : FormatOf A) -> (def : A) -> FormatOf Unit
2828
Repeat : {0 A : Type} -> (len : Nat) -> FormatOf A -> FormatOf (Vect len A)
2929
Bind : {0 A : Type} -> {0 B : A -> Type} -> (f : FormatOf A) -> ((x : A) -> FormatOf (B x)) -> FormatOf (x : A ** B x)
3030

@@ -54,7 +54,7 @@ namespace FormatOf
5454
(_::_) => Nothing
5555
decode Fail = const Nothing
5656
decode (Pure x) = pure (MkSing x)
57-
decode (Skip f _) = map (const ()) (decode f)
57+
decode (Ignore f _) = ignore (decode f)
5858
decode (Repeat 0 f) = pure []
5959
decode (Repeat (S len) f) = do
6060
x <- decode f
@@ -70,7 +70,7 @@ namespace FormatOf
7070
encode : {0 A, S : Type} -> (f : FormatOf A) -> Encode A (Colist S)
7171
encode End () = Just []
7272
encode (Pure x) (MkSing _) = Just []
73-
encode (Skip f def) () = encode f def
73+
encode (Ignore f def) () = encode f def
7474
encode (Repeat Z f) [] = Just []
7575
encode (Repeat (S len) f) (x :: xs) =
7676
[| encode f x <+> encode (Repeat len f) xs |]
@@ -182,7 +182,7 @@ namespace Format
182182

183183
public export
184184
skip : (f : Format) -> (def : f.Rep) -> Format
185-
skip f def = MkFormat Unit (Skip (toFormatOf f) def)
185+
skip f def = MkFormat Unit (Ignore (toFormatOf f) def)
186186

187187

188188
public export

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

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -37,7 +37,7 @@ data FormatOf : (A : Type) -> Type where
3737
End : FormatOf Unit
3838
Fail : FormatOf Void
3939
Pure : {0 A : Type} -> (x : A) -> FormatOf (Sing x)
40-
Skip : {0 A : Type} -> (f : FormatOf A) -> (def : A) -> FormatOf Unit
40+
Ignore : {0 A : Type} -> (f : FormatOf A) -> (def : A) -> FormatOf Unit
4141
Repeat : {0 A : Type} -> (len : Nat) -> FormatOf A -> FormatOf (Vect len A)
4242
Bind : {0 A : Type} -> {0 B : A -> Type} -> (f : FormatOf A) -> ((x : A) -> FormatOf (B x)) -> FormatOf (x : A ** B x)
4343
Custom : (f : CustomFormat) -> FormatOf f.Rep
@@ -68,7 +68,7 @@ namespace FormatOf
6868
(_::_) => Nothing
6969
decode Fail = const Nothing
7070
decode (Pure x) = pure (MkSing x)
71-
decode (Skip f _) = map (const ()) (decode f)
71+
decode (Ignore f _) = ignore (decode f)
7272
decode (Repeat 0 f) = pure []
7373
decode (Repeat (S len) f) = do
7474
x <- decode f
@@ -85,7 +85,7 @@ namespace FormatOf
8585
encode : {0 A : Type} -> (f : FormatOf A) -> Encode A ByteStream
8686
encode End () = Just []
8787
encode (Pure x) (MkSing _) = Just []
88-
encode (Skip f def) () = encode f def
88+
encode (Ignore f def) () = encode f def
8989
encode (Repeat Z f) [] = Just []
9090
encode (Repeat (S len) f) (x :: xs) =
9191
[| encode f x <+> encode (Repeat len f) xs |]
@@ -197,8 +197,8 @@ namespace Format
197197

198198

199199
public export
200-
skip : (f : Format) -> (def : f.Rep) -> Format
201-
skip f def = MkFormat Unit (Skip (toFormatOf f) def)
200+
ignore : (f : Format) -> (def : f.Rep) -> Format
201+
ignore f def = MkFormat Unit (Ignore (toFormatOf f) def)
202202

203203

204204
public export

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

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -45,7 +45,7 @@ mutual
4545
End : Format
4646
Fail : Format
4747
Pure : {0 A : Type} -> A -> Format
48-
Skip : (f : Format) -> (def : Rep f) -> Format
48+
Ignore : (f : Format) -> (def : Rep f) -> Format
4949
Repeat : Nat -> Format -> Format
5050
Bind : (f : Format) -> (Rep f -> Format) -> Format
5151

@@ -55,7 +55,7 @@ mutual
5555
Rep : Format -> Type
5656
Rep End = Unit
5757
Rep Fail = Void
58-
Rep (Skip _ _) = Unit
58+
Rep (Ignore _ _) = Unit
5959
Rep (Repeat len f) = Vect len (Rep f)
6060
Rep (Pure x) = Sing x
6161
Rep (Bind f1 f2) = (x : Rep f1 ** Rep (f2 x))
@@ -86,7 +86,7 @@ namespace Format
8686
(_::_) => Nothing
8787
decode Fail = const Nothing
8888
decode (Pure x) = pure (MkSing x)
89-
decode (Skip f _) = map (const ()) (decode f)
89+
decode (Ignore f _) = ignore (decode f)
9090
decode (Repeat 0 f) = pure []
9191
decode (Repeat (S len) f) = do
9292
x <- decode f
@@ -102,7 +102,7 @@ namespace Format
102102
encode : (f : Format) -> Encode (Rep f) (Colist a)
103103
encode End () = Just []
104104
encode (Pure x) (MkSing _) = Just []
105-
encode (Skip f def) () = encode f def
105+
encode (Ignore f def) () = encode f def
106106
encode (Repeat Z f) [] = Just []
107107
encode (Repeat (S len) f) (x :: xs) = do
108108
[| encode f x <+> encode (Repeat len f) xs |]
@@ -209,9 +209,9 @@ namespace FormatOf
209209

210210

211211
public export
212-
skip : {0 A : Type} -> (f : FormatOf A) -> (def : A) -> FormatOf Unit
213-
skip f def with (toFormatEq f)
214-
skip _ def | (Element f prf) = MkFormatOf (Skip f (rewrite prf in def))
212+
ignore : {0 A : Type} -> (f : FormatOf A) -> (def : A) -> FormatOf Unit
213+
ignore f def with (toFormatEq f)
214+
ignore _ def | (Element f prf) = MkFormatOf (Ignore f (rewrite prf in def))
215215

216216

217217
public export

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

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -44,7 +44,7 @@ mutual
4444
End : Format
4545
Fail : Format
4646
Pure : {0 A : Type} -> A -> Format
47-
Skip : (f : Format) -> (def : Rep f) -> Format
47+
Ignore : (f : Format) -> (def : Rep f) -> Format
4848
Repeat : Nat -> Format -> Format
4949
Bind : (f : Format) -> (Rep f -> Format) -> Format
5050
Custom : (f : CustomFormat) -> Format
@@ -55,7 +55,7 @@ mutual
5555
Rep : Format -> Type
5656
Rep End = Unit
5757
Rep Fail = Void
58-
Rep (Skip _ _) = Unit
58+
Rep (Ignore _ _) = Unit
5959
Rep (Repeat len f) = Vect len (Rep f)
6060
Rep (Pure x) = Sing x
6161
Rep (Bind f1 f2) = (x : Rep f1 ** Rep (f2 x))
@@ -87,7 +87,7 @@ namespace Format
8787
(_::_) => Nothing
8888
decode Fail = const Nothing
8989
decode (Pure x) = pure (MkSing x)
90-
decode (Skip f _) = map (const ()) (decode f)
90+
decode (Ignore f _) = ignore (decode f)
9191
decode (Repeat 0 f) = pure []
9292
decode (Repeat (S len) f) = do
9393
x <- decode f
@@ -104,7 +104,7 @@ namespace Format
104104
encode : (f : Format) -> Encode (Rep f) ByteStream
105105
encode End () = Just []
106106
encode (Pure x) (MkSing _) = Just []
107-
encode (Skip f def) () = encode f def
107+
encode (Ignore f def) () = encode f def
108108
encode (Repeat Z f) [] = Just []
109109
encode (Repeat (S len) f) (x :: xs) =
110110
[| encode f x <+> encode (Repeat len f) xs |]
@@ -244,9 +244,9 @@ namespace FormatOf
244244

245245

246246
public export
247-
skip : {0 A : Type} -> (f : FormatOf A) -> (def : A) -> FormatOf Unit
248-
skip f def with (toFormatEq f)
249-
skip _ def | (Element f prf) = MkFormatOf (Skip f (rewrite prf in def))
247+
ignore : {0 A : Type} -> (f : FormatOf A) -> (def : A) -> FormatOf Unit
248+
ignore f def with (toFormatEq f)
249+
ignore _ def | (Element f prf) = MkFormatOf (Ignore f (rewrite prf in def))
250250

251251

252252
public export

‎experiments/idris/src/Fathom/Open/Record.idr‎

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -76,13 +76,13 @@ namespace Format
7676

7777

7878
public export
79-
skip : (f : Format) -> (def : f.Rep) -> Format
80-
skip f def = MkFormat { Rep, decode, encode } where
79+
ignore : (f : Format) -> (def : f.Rep) -> Format
80+
ignore f def = MkFormat { Rep, decode, encode } where
8181
Rep : Type
8282
Rep = ()
8383

8484
decode : DecodePart Rep ByteStream
85-
decode = map (const ()) f.decode
85+
decode = ignore f.decode
8686

8787
encode : Encode Rep ByteStream
8888
encode () = f.encode def
@@ -268,9 +268,9 @@ namespace FormatOf
268268

269269

270270
public export
271-
skip : {0 A : Type} -> (f : FormatOf A) -> (def : A) -> FormatOf Unit
272-
skip f def with (toFormatEq f)
273-
skip _ def | (Element f prf) = MkFormatOf (skip f (rewrite prf in def))
271+
ignore : {0 A : Type} -> (f : FormatOf A) -> (def : A) -> FormatOf Unit
272+
ignore f def with (toFormatEq f)
273+
ignore _ def | (Element f prf) = MkFormatOf (ignore f (rewrite prf in def))
274274

275275

276276
public export

‎experiments/idris/src/Playground.idr‎

Lines changed: 15 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -45,7 +45,7 @@ formatOf f = Record.MkFormat
4545
-- End => end.decode
4646
-- Fail => fail.decode
4747
-- Pure x => (pure x).decode
48-
-- Skip f def => (skip (format' f) def).decode
48+
-- Ignore f def => (skip (format' f) def).decode
4949
-- Repeat len f => (repeat len (format' f)).decode
5050
-- Bind f1 f2 => (bind (format' f1) (\x => format' (f2 x))).decode
5151
-- OfSing f r => (format' f).decode
@@ -56,7 +56,7 @@ formatOf f = Record.MkFormat
5656
-- End => end.encode
5757
-- Fail => fail.encode
5858
-- Pure x => (pure x).encode
59-
-- Skip f def => (skip (format' f) def).encode
59+
-- Ignore f def => (skip (format' f) def).encode
6060
-- Repeat len f => (repeat len (format' f)).encode
6161
-- Bind f1 f2 => (bind (format' f1) (\x => format' (f2 x))).encode
6262
-- OfSing f r => (format' f).encode
@@ -68,7 +68,7 @@ indRecToIndexed : (f : IndRec.Format) -> Indexed.FormatOf (Rep f)
6868
indRecToIndexed End = Indexed.End
6969
indRecToIndexed Fail = Indexed.Fail
7070
indRecToIndexed (Pure x) = Indexed.Pure x
71-
indRecToIndexed (Skip f def) = Indexed.Skip (indRecToIndexed f) def
71+
indRecToIndexed (Ignore f def) = Indexed.Ignore (indRecToIndexed f) def
7272
indRecToIndexed (Repeat len f) = Indexed.Repeat len (indRecToIndexed f)
7373
indRecToIndexed (Bind f g) = Indexed.Bind (indRecToIndexed f) (\x => indRecToIndexed (g x))
7474

@@ -80,8 +80,8 @@ mutual
8080
indexedToIndRecFormat (MkFormat () End) = (End ** Refl)
8181
indexedToIndRecFormat (MkFormat Void Fail) = (Fail ** Refl)
8282
indexedToIndRecFormat (MkFormat (Sing x) (Pure x)) = (Pure x ** Refl)
83-
indexedToIndRecFormat (MkFormat () (Skip f def)) with (indexedToIndRecFormatOf f)
84-
_ | MkFormatOf f' = (Skip f' def ** Refl)
83+
indexedToIndRecFormat (MkFormat () (Ignore f def)) with (indexedToIndRecFormatOf f)
84+
_ | MkFormatOf f' = (Ignore f' def ** Refl)
8585
indexedToIndRecFormat (MkFormat (Vect len _) (Repeat len f)) with (indexedToIndRecFormatOf f)
8686
_ | MkFormatOf f' = (Repeat len f' ** Refl)
8787
indexedToIndRecFormat (MkFormat (x : _ ** _) (Bind f1 f2)) with (indexedToIndRecFormatOf f1)
@@ -94,8 +94,8 @@ mutual
9494
indexedToIndRecFormatOf End = MkFormatOf End
9595
indexedToIndRecFormatOf Fail = MkFormatOf Fail
9696
indexedToIndRecFormatOf (Pure x) = MkFormatOf (Pure x)
97-
indexedToIndRecFormatOf (Skip f def) with (indexedToIndRecFormatOf f)
98-
_ | MkFormatOf f' = MkFormatOf (Skip f' def)
97+
indexedToIndRecFormatOf (Ignore f def) with (indexedToIndRecFormatOf f)
98+
_ | MkFormatOf f' = MkFormatOf (Ignore f' def)
9999
indexedToIndRecFormatOf (Repeat len f) with (indexedToIndRecFormatOf f)
100100
_ | MkFormatOf f' = MkFormatOf (Repeat len f')
101101
indexedToIndRecFormatOf (Bind f1 f2) with (indexedToIndRecFormatOf f1)
@@ -123,8 +123,8 @@ mutual
123123
-- indexedToIndRec End = MkFormatOf IndRec.End
124124
-- indexedToIndRec Fail = MkFormatOf IndRec.Fail
125125
-- indexedToIndRec (Pure x) = MkFormatOf (IndRec.Pure x)
126-
-- indexedToIndRec (Skip f def) with (indexedToIndRec f)
127-
-- indexedToIndRec (Skip _ def) | MkFormatOf f = MkFormatOf (IndRec.Skip f def)
126+
-- indexedToIndRec (Ignore f def) with (indexedToIndRec f)
127+
-- indexedToIndRec (Ignore _ def) | MkFormatOf f = MkFormatOf (IndRec.Ignore f def)
128128
-- indexedToIndRec (Repeat len f) with (indexedToIndRec f)
129129
-- indexedToIndRec (Repeat len _) | MkFormatOf f = MkFormatOf (IndRec.Repeat len f)
130130
-- indexedToIndRec (Bind f1 f2) with (indexedToIndRec f1)
@@ -135,7 +135,7 @@ mutual
135135
-- _ | (MkFormatOf End) = MkFormatOf (Bind End ?todo_indexedToIndRec_2)
136136
-- _ | (MkFormatOf Fail) = MkFormatOf (Bind Fail absurd)
137137
-- _ | (MkFormatOf (Pure f)) = MkFormatOf (Bind ?todo_indexedToIndRec_4)
138-
-- _ | (MkFormatOf (Skip f def)) = MkFormatOf (Bind ?todo_indexedToIndRec_5)
138+
-- _ | (MkFormatOf (Ignore f def)) = MkFormatOf (Bind ?todo_indexedToIndRec_5)
139139
-- _ | (MkFormatOf (Repeat k x)) = MkFormatOf (Bind ?todo_indexedToIndRec_6)
140140
-- _ | (MkFormatOf (Bind f g)) = MkFormatOf (Bind ?todo_indexedToIndRec_7)
141141

@@ -164,7 +164,7 @@ mutual
164164
-- _ | (End ** prf) = let bindF1 = Bind f1 in ?todo_indexedToIndRec_2
165165
-- _ | (Fail ** prf) = let bindF1 = Bind f1 in ?todo_indexedToIndRec_3
166166
-- _ | ((Pure f) ** prf) = let bindF1 = Bind f1 in ?todo_indexedToIndRec_4
167-
-- _ | ((Skip f def) ** prf) = let bindF1 = Bind f1 in ?todo_indexedToIndRec_5
167+
-- _ | ((Ignore f def) ** prf) = let bindF1 = Bind f1 in ?todo_indexedToIndRec_5
168168
-- _ | ((Repeat k x) ** prf) = let bindF1 = Bind f1 in ?todo_indexedToIndRec_6
169169
-- _ | ((Bind f g) ** prf) = let bindF1 = Bind f1 in ?todo_indexedToIndRec_7
170170

@@ -205,8 +205,8 @@ mutual
205205
-- indexedToIndRec' End = IndRec.End
206206
-- indexedToIndRec' Fail = IndRec.Fail
207207
-- indexedToIndRec' (Pure x) = IndRec.Pure x
208-
-- indexedToIndRec' (Skip f def) with (MkFormatOf (indexedToIndRec' f))
209-
-- _ | f' = IndRec.Skip (indexedToIndRec' f) ?todo1
208+
-- indexedToIndRec' (Ignore f def) with (MkFormatOf (indexedToIndRec' f))
209+
-- _ | f' = IndRec.Ignore (indexedToIndRec' f) ?todo1
210210
-- indexedToIndRec' (Repeat len f) = IndRec.Repeat len (indexedToIndRec' f)
211211
-- indexedToIndRec' (Bind f1 f2) = IndRec.Bind (indexedToIndRec' f1) ?todo2
212212

@@ -215,8 +215,8 @@ mutual
215215
-- indexedToIndRec'' (MkFormat () End) = IndRec.End
216216
-- indexedToIndRec'' (MkFormat Void Fail) = IndRec.Fail
217217
-- indexedToIndRec'' (MkFormat (Sing x) (Pure x)) = IndRec.Pure x
218-
-- indexedToIndRec'' (MkFormat () (Skip f def)) with (indexedToIndRec'' (MkFormat _ f))
219-
-- _ | f'' = IndRec.Skip f'' ?tododef
218+
-- indexedToIndRec'' (MkFormat () (Ignore f def)) with (indexedToIndRec'' (MkFormat _ f))
219+
-- _ | f'' = IndRec.Ignore f'' ?tododef
220220
-- indexedToIndRec'' (MkFormat rep (Repeat len f)) = IndRec.Repeat len (indexedToIndRec'' f)
221221
-- indexedToIndRec'' (MkFormat rep (Bind f1 f2)) = IndRec.Bind (indexedToIndRec'' f1) ?todo2
222222

0 commit comments

Comments
 (0)