Skip to content

Commit e961d7f

Browse files
brendanzabbrendanzab
committed
Move experiments into a different module
1 parent 098bbf7 commit e961d7f

File tree

8 files changed

+295
-279
lines changed

8 files changed

+295
-279
lines changed

‎experiments/idris/fathom.ipkg‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -14,17 +14,24 @@ package fathom
1414

1515
-- modules to install
1616
modules = Fathom
17+
1718
, Fathom.Base
1819
, Fathom.Data.Bit
1920
, Fathom.Data.Iso
2021
, Fathom.Data.Sing
2122
, Fathom.Data.Word
23+
2224
, Fathom.Closed.IndexedInductive
2325
, Fathom.Closed.IndexedInductiveCustom
2426
, Fathom.Closed.InductiveRecursive
2527
, Fathom.Closed.InductiveRecursiveCustom
2628
, Fathom.Open.Record
2729

30+
, Playground
31+
, Playground.OpenType.IndexedInductive
32+
, Playground.OpenType.InductiveRecursive
33+
, Playground.OpenType.Record
34+
2835
-- main file (i.e. file to load at REPL)
2936
-- main =
3037

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

Lines changed: 0 additions & 97 deletions
Original file line numberDiff line numberDiff line change
@@ -235,100 +235,3 @@ u16Be = Custom (MkCustomFormat
235235
, decode = map cast (decodeU16 BE)
236236
, encode = encodeU16 BE . cast {to = Bits16}
237237
})
238-
239-
240-
-----------------
241-
-- EXPERIMENTS --
242-
-----------------
243-
244-
-- Reproduction of difficulties in OpenType format
245-
246-
namespace OpenTypeTest.FormatOf
247-
248-
Flag : Type
249-
Flag =
250-
( id : Nat
251-
** repeat :
252-
case id of
253-
0 => Nat
254-
S n => Sing {A = Nat} 0
255-
** Sing ()
256-
)
257-
258-
(.repeat) : Flag -> Nat
259-
(.repeat) (0 ** repeat ** _) = repeat
260-
(.repeat) (S _ ** repeat ** _) = val repeat
261-
262-
263-
-- def flag = {
264-
-- flag <- u8,
265-
-- repeat <- match ((u8_and flag 8) != (0 : U8)) {
266-
-- true => u8,
267-
-- false => succeed U8 0,
268-
-- },
269-
-- };
270-
flag : FormatOf Flag
271-
flag = do
272-
flag <- u8
273-
repeat <- case flag of
274-
0 => u8
275-
S _ => Pure {A = Nat} 0
276-
Pure ()
277-
278-
279-
SimpleGlyph : Type
280-
SimpleGlyph =
281-
( flag : Flag
282-
** Sing (flag.repeat + 1)
283-
)
284-
285-
286-
-- def simple_glyph = fun (number_of_contours : U16) => {
287-
-- ...
288-
-- let flag_repeat = fun (f : Repr flag) => f.repeat + (1 : U8),
289-
-- ...
290-
-- };
291-
simple_glyph : FormatOf SimpleGlyph
292-
simple_glyph = do
293-
flag <- flag
294-
Pure (flag.repeat + 1)
295-
296-
297-
namespace OpenTypeTest.Format
298-
299-
-- Reproduction of difficulties in OpenType format
300-
301-
-- def flag = {
302-
-- flag <- u8,
303-
-- repeat <- match ((u8_and flag 8) != (0 : U8)) {
304-
-- true => u8,
305-
-- false => succeed U8 0,
306-
-- },
307-
-- };
308-
flag : Format
309-
flag = Format.do
310-
id <- toFormat u8
311-
repeat <- case id of
312-
0 => toFormat u8
313-
S n => pure {A = Nat} 0
314-
pure ()
315-
316-
317-
-- def simple_glyph = fun (number_of_contours : U16) => {
318-
-- ...
319-
-- let flag_repeat = fun (f : Repr flag) => f.repeat + (1 : U8),
320-
-- ...
321-
-- };
322-
simple_glyph : Format
323-
simple_glyph = Format.do
324-
flag <- flag
325-
let
326-
repeat : Nat
327-
repeat = ?todo_repeat
328-
-- repeat = case the (Format.Rep flag) flag of
329-
-- (0 ** repeat ** MkSing ()) => repeat
330-
-- (S n ** repeat ** MkSing ()) => repeat
331-
332-
-- Error: While processing right hand side of simple_glyph. While processing right hand side
333-
-- of simple_glyph,repeat. Can't match on 0 as it must have a polymorphic type.
334-
pure (repeat + 1)

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

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -215,3 +215,8 @@ namespace FormatOf
215215
bind f1 f2 with (toFormatEq f1)
216216
bind _ f2 | (Element f1 prf) =
217217
?todoFormatOf_bind
218+
219+
220+
public export
221+
(>>=) : {0 A : Type} -> {0 B : A -> Type} -> (f : FormatOf A) -> ((x : A) -> FormatOf (B x)) -> FormatOf (x : A ** B x)
222+
(>>=) = bind

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

Lines changed: 0 additions & 91 deletions
Original file line numberDiff line numberDiff line change
@@ -255,94 +255,3 @@ namespace FormatOf
255255
public export
256256
(>>=) : {0 A : Type} -> {0 B : A -> Type} -> (f : FormatOf A) -> ((x : A) -> FormatOf (B x)) -> FormatOf (x : A ** B x)
257257
(>>=) = bind
258-
259-
260-
-----------------
261-
-- EXPERIMENTS --
262-
-----------------
263-
264-
-- Reproduction of difficulties in OpenType format
265-
266-
namespace OpenTypeTest.Format
267-
268-
-- def flag = {
269-
-- flag <- u8,
270-
-- repeat <- match ((u8_and flag 8) != (0 : U8)) {
271-
-- true => u8,
272-
-- false => succeed U8 0,
273-
-- },
274-
-- };
275-
flag : Format
276-
flag = do
277-
id <- u8
278-
repeat <- case id of
279-
0 => u8
280-
S n => Pure {A = Nat} 0
281-
Pure ()
282-
283-
284-
-- def simple_glyph = fun (number_of_contours : U16) => {
285-
-- ...
286-
-- let flag_repeat = fun (f : Repr flag) => f.repeat + (1 : U8),
287-
-- ...
288-
-- };
289-
simple_glyph : Format
290-
simple_glyph = do
291-
flag <- flag
292-
let
293-
repeat : Nat
294-
repeat = case flag of
295-
(0 ** repeat ** MkSing ()) => repeat
296-
(S n ** repeat ** MkSing ()) => repeat
297-
Pure (repeat + 1)
298-
299-
300-
namespace OpenTypeTest.FormatOf
301-
302-
Flag : Type
303-
Flag =
304-
( id : Nat
305-
** repeat :
306-
case id of
307-
0 => Nat
308-
S n => Sing {A = Nat} 0
309-
** Sing ()
310-
)
311-
312-
(.repeat) : Flag -> Nat
313-
(.repeat) (0 ** repeat ** _) = repeat
314-
(.repeat) (S _ ** repeat ** _) = val repeat
315-
316-
317-
-- def flag = {
318-
-- flag <- u8,
319-
-- repeat <- match ((u8_and flag 8) != (0 : U8)) {
320-
-- true => u8,
321-
-- false => succeed U8 0,
322-
-- },
323-
-- };
324-
flag : FormatOf Flag
325-
flag = FormatOf.do
326-
flag <- toFormatOf u8
327-
repeat <- case flag of
328-
0 => toFormatOf u8
329-
S _ => pure {A = Nat} 0
330-
pure ()
331-
332-
333-
SimpleGlyph : Type
334-
SimpleGlyph =
335-
( flag : Flag
336-
** Sing (flag.repeat + 1)
337-
)
338-
339-
340-
-- def simple_glyph = fun (number_of_contours : U16) => {
341-
-- ...
342-
-- let flag_repeat = fun (f : Repr flag) => f.repeat + (1 : U8),
343-
-- ...
344-
-- };
345-
simple_glyph : FormatOf SimpleGlyph
346-
simple_glyph = FormatOf.do
347-
flag <- flag
348-
pure (flag.repeat + 1)

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

Lines changed: 0 additions & 91 deletions
Original file line numberDiff line numberDiff line change
@@ -280,94 +280,3 @@ namespace FormatOf
280280
public export
281281
(>>=) : {0 A : Type} -> {0 B : A -> Type} -> (f : FormatOf A) -> ((x : A) -> FormatOf (B x)) -> FormatOf (x : A ** B x)
282282
(>>=) = bind
283-
284-
285-
-----------------
286-
-- EXPERIMENTS --
287-
-----------------
288-
289-
-- Reproduction of difficulties in OpenType format
290-
291-
namespace OpenTypeTest.Format
292-
293-
-- def flag = {
294-
-- flag <- u8,
295-
-- repeat <- match ((u8_and flag 8) != (0 : U8)) {
296-
-- true => u8,
297-
-- false => succeed U8 0,
298-
-- },
299-
-- };
300-
flag : Format
301-
flag = do
302-
id <- u8
303-
repeat <- case id of
304-
0 => u8
305-
S _ => pure {A = Nat} 0
306-
pure ()
307-
308-
309-
(.repeat) : Format.flag.Rep -> Nat
310-
(.repeat) (0 ** repeat ** _) = repeat
311-
(.repeat) (S _ ** repeat ** _) = val repeat
312-
313-
314-
-- def simple_glyph = fun (number_of_contours : U16) => {
315-
-- ...
316-
-- let flag_repeat = fun (f : Repr flag) => f.repeat + (1 : U8),
317-
-- ...
318-
-- };
319-
simple_glyph : Format
320-
simple_glyph = do
321-
flag <- flag
322-
pure (flag.repeat + 1)
323-
324-
325-
namespace OpenTypeTest.FormatOf
326-
327-
Flag : Type
328-
Flag =
329-
( id : Nat
330-
** repeat :
331-
case id of
332-
0 => Nat
333-
S n => Sing {A = Nat} 0
334-
** Sing ()
335-
)
336-
337-
(.repeat) : Flag -> Nat
338-
(.repeat) (0 ** repeat ** _) = repeat
339-
(.repeat) (S _ ** repeat ** _) = val repeat
340-
341-
342-
-- def flag = {
343-
-- flag <- u8,
344-
-- repeat <- match ((u8_and flag 8) != (0 : U8)) {
345-
-- true => u8,
346-
-- false => succeed U8 0,
347-
-- },
348-
-- };
349-
flag : FormatOf Flag
350-
flag = FormatOf.do
351-
flag <- toFormatOf u8
352-
repeat <- case flag of
353-
0 => toFormatOf u8
354-
S _ => pure {A = Nat} 0
355-
pure ()
356-
357-
358-
SimpleGlyph : Type
359-
SimpleGlyph =
360-
( flag : Flag
361-
** Sing (flag.repeat + 1)
362-
)
363-
364-
365-
-- def simple_glyph = fun (number_of_contours : U16) => {
366-
-- ...
367-
-- let flag_repeat = fun (f : Repr flag) => f.repeat + (1 : U8),
368-
-- ...
369-
-- };
370-
simple_glyph : FormatOf SimpleGlyph
371-
simple_glyph = FormatOf.do
372-
flag <- flag
373-
pure (flag.repeat + 1)

0 commit comments

Comments
 (0)