Skip to content

Commit 348f7fd

Browse files
brendanzabbrendanzab
committed
Move compiler experiments
1 parent 9fbf359 commit 348f7fd

File tree

3 files changed

+105
-97
lines changed

3 files changed

+105
-97
lines changed

‎experiments/idris/fathom.ipkg‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -27,6 +27,7 @@ modules = Fathom
2727
, Fathom.Format.Record
2828

2929
, Playground
30+
, Playground.Extraction
3031
, Playground.HeterogeneousSequences
3132
, Playground.OpenType.IndexedInductive
3233
, Playground.OpenType.InductiveRecursive

‎experiments/idris/src/Playground/Extraction.idr‎

Lines changed: 104 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,104 @@
1+
||| Thinking about extracting format descriptions to Rust
2+
3+
module Playground.Extraction
4+
5+
6+
import Fathom.Data.Sing
7+
import Fathom.Format.InductiveRecursiveCustom
8+
9+
10+
namespace Rust
11+
12+
data RType : Type where
13+
Var : String -> RType
14+
U8 : RType
15+
U16 : RType
16+
U32 : RType
17+
U64 : RType
18+
I8 : RType
19+
I16 : RType
20+
I32 : RType
21+
I64 : RType
22+
Never : RType
23+
Tuple : List RType -> RType
24+
Vec : RType -> RType
25+
26+
27+
data Item : Type where
28+
Struct : List (String, RType) -> Item
29+
Enum : List (String, RType) -> Item
30+
DecodeFn : () -> Item
31+
EncodeFn : () -> Item
32+
33+
34+
record Module where
35+
constructor MkModule
36+
items : List (String, Item)
37+
38+
39+
namespace Compile
40+
41+
-- TODO: Cache compilations of definitions
42+
-- eg. of structs, enums, endocers and decoders
43+
44+
45+
compileFormat : Format -> (Rust.Module -> Maybe Rust.Module)
46+
compileFormat f =
47+
-- compile rep
48+
-- compile decode
49+
-- compile encode
50+
?todo_compileFormat
51+
52+
53+
compileRep : (f : Format) -> Maybe Rust.RType
54+
compileRep End = Just (Rust.Tuple [])
55+
compileRep Fail = Just (Rust.Never)
56+
compileRep (Ignore _ _) = Just (Rust.Tuple [])
57+
compileRep (Repeat _ f) =
58+
Just (Rust.Vec !(compileRep f)) -- TODO: Compile to a contract? Or maybe a
59+
-- fixed size array if the length is known
60+
-- or just throw away the info
61+
compileRep (Pure x) =
62+
?todo_compileSingRep -- TODO: interpret an Idris type as a Rust type??
63+
-- perhaps we need to restrict this?
64+
compileRep (Pair f1 f2) =
65+
Just (Rust.Tuple
66+
[ !(compileRep f1)
67+
, !(compileRep f2)
68+
])
69+
compileRep (Bind f1 f2) =
70+
Just (Tuple
71+
[ !(compileRep f1)
72+
, !(compileRep (f2 ?todo_compileBind_x)) -- TODO: how to bind the output?
73+
-- enum based on the values of `x : Rep f1`?
74+
-- depends on how `x` is used inside `f2`
75+
])
76+
compileRep (Custom f) =
77+
-- TODO: f.RustRep
78+
Nothing
79+
80+
81+
compileDecode : Format -> (Rust.Module -> Maybe Rust.Module)
82+
compileDecode End = ?todo_compileDecodeEnd
83+
compileDecode Fail = ?todo_compileDecodeFail
84+
compileDecode (Pure x) = ?todo_compileDecodePure
85+
compileDecode (Ignore f _) = ?todo_compileDecodeIgnore
86+
compileDecode (Repeat len f) = ?todo_compileDecodeRepeat
87+
compileDecode (Pair f1 f2) = ?todo_compileDecodePair
88+
compileDecode (Bind f1 f2) = ?todo_compileDecodeBind
89+
compileDecode (Custom f) =
90+
-- TODO: f.rustDecode
91+
?todo_compileDecodeCustom
92+
93+
94+
compileEncode : Format -> (Rust.Module -> Maybe Rust.Module)
95+
compileEncode End = ?todo_compileEncodeEnd
96+
compileEncode Fail = ?todo_compileEncodeFail
97+
compileEncode (Pure x) = ?todo_compileEncodePure
98+
compileEncode (Ignore f def) = ?todo_compileEncodeIgnore
99+
compileEncode (Repeat len f) = ?todo_compileEncodeRepeat
100+
compileEncode (Pair f1 f2) = ?todo_compileEncodePair
101+
compileEncode (Bind f1 f2) = ?todo_compileEncodeBind
102+
compileEncode (Custom f) =
103+
-- TODO: f.rustEncode
104+
?todo_compileEncodeCustom

‎experiments/idris/src/Playground/OpenType/InductiveRecursive.idr‎

Lines changed: 0 additions & 97 deletions
Original file line numberDiff line numberDiff line change
@@ -90,100 +90,3 @@ namespace FormatOf
9090
simple_glyph = FormatOf.do
9191
flag <- flag
9292
pure (flag.repeat + 1)
93-
94-
95-
-- Thinking about compilation
96-
97-
namespace Rust
98-
99-
data RType : Type where
100-
Var : String -> RType
101-
U8 : RType
102-
U16 : RType
103-
U32 : RType
104-
U64 : RType
105-
I8 : RType
106-
I16 : RType
107-
I32 : RType
108-
I64 : RType
109-
Never : RType
110-
Tuple : List RType -> RType
111-
Vec : RType -> RType
112-
113-
data Item : Type where
114-
Struct : List (String, RType) -> Item
115-
Enum : List (String, RType) -> Item
116-
DecodeFn : () -> Item
117-
EncodeFn : () -> Item
118-
119-
record Module where
120-
constructor MkModule
121-
items : List (String, Item)
122-
123-
124-
namespace Compile
125-
126-
-- TODO: Cache compilations of definitions
127-
-- eg. of structs, enums, endocers and decoders
128-
129-
130-
compileFormat : Format -> (Rust.Module -> Maybe Rust.Module)
131-
compileFormat f =
132-
-- compile rep
133-
-- compile decode
134-
-- compile encode
135-
?todo_compileFormat
136-
137-
138-
compileRep : (f : Format) -> Maybe Rust.RType
139-
compileRep End = Just (Rust.Tuple [])
140-
compileRep Fail = Just (Rust.Never)
141-
compileRep (Ignore _ _) = Just (Rust.Tuple [])
142-
compileRep (Repeat _ f) =
143-
Just (Rust.Vec !(compileRep f)) -- TODO: Compile to a contract? Or maybe a
144-
-- fixed size array if the length is known
145-
-- or just throw away the info
146-
compileRep (Pure x) =
147-
?todo_compileSingRep -- TODO: interpret an Idris type as a Rust type??
148-
-- perhaps we need to restrict this?
149-
compileRep (Pair f1 f2) =
150-
Just (Rust.Tuple
151-
[ !(compileRep f1)
152-
, !(compileRep f2)
153-
])
154-
compileRep (Bind f1 f2) =
155-
Just (Tuple
156-
[ !(compileRep f1)
157-
, !(compileRep (f2 ?todo_compileBind_x)) -- TODO: how to bind the output?
158-
-- enum based on the values of `x : Rep f1`?
159-
-- depends on how `x` is used inside `f2`
160-
])
161-
compileRep (Custom f) =
162-
-- TODO: f.RustRep
163-
Nothing
164-
165-
166-
compileDecode : Format -> (Rust.Module -> Maybe Rust.Module)
167-
compileDecode End = ?todo_compileDecodeEnd
168-
compileDecode Fail = ?todo_compileDecodeFail
169-
compileDecode (Pure x) = ?todo_compileDecodePure
170-
compileDecode (Ignore f _) = ?todo_compileDecodeIgnore
171-
compileDecode (Repeat len f) = ?todo_compileDecodeRepeat
172-
compileDecode (Pair f1 f2) = ?todo_compileDecodePair
173-
compileDecode (Bind f1 f2) = ?todo_compileDecodeBind
174-
compileDecode (Custom f) =
175-
-- TODO: f.rustDecode
176-
?todo_compileDecodeCustom
177-
178-
179-
compileEncode : Format -> (Rust.Module -> Maybe Rust.Module)
180-
compileEncode End = ?todo_compileEncodeEnd
181-
compileEncode Fail = ?todo_compileEncodeFail
182-
compileEncode (Pure x) = ?todo_compileEncodePure
183-
compileEncode (Ignore f def) = ?todo_compileEncodeIgnore
184-
compileEncode (Repeat len f) = ?todo_compileEncodeRepeat
185-
compileEncode (Pair f1 f2) = ?todo_compileEncodePair
186-
compileEncode (Bind f1 f2) = ?todo_compileEncodeBind
187-
compileEncode (Custom f) =
188-
-- TODO: f.rustEncode
189-
?todo_compileEncodeCustom

0 commit comments

Comments
 (0)