File tree 4 files changed +97
-14
lines changed
4 files changed +97
-14
lines changed Original file line number Diff line number Diff line change @@ -4,6 +4,8 @@ version = 0.1.0
4
4
5
5
modules
6
6
= Dart.Core
7
+ , Dart.Core.Map
8
+ , Dart.Core.Set
7
9
, Dart.FFI
8
10
, Dart.FFI.Constructors
9
11
, Dart.FFI.Elab
Original file line number Diff line number Diff line change @@ -35,8 +35,13 @@ List element = GenericType "List,dart:core" [element]
35
35
36
36
%inline
37
37
public export
38
- DartMap : Type -> Type -> Type
39
- DartMap key val = GenericType " Map,dart:core" [key, val]
38
+ Map : Type -> Type -> Type
39
+ Map k v = GenericType " Map,dart:core" [k, v]
40
+
41
+ %inline
42
+ public export
43
+ Set : Type -> Type
44
+ Set e = GenericType " Set,dart:core" [e]
40
45
41
46
namespace Object
42
47
@@ -137,18 +142,6 @@ namespace List
137
142
traverse_ (`add` result) (toList es)
138
143
pure result
139
144
140
- namespace Map
141
-
142
- % inline
143
- export
144
- new : HasIO io => {key : Type } -> {val : Type } -> io (DartMap key val)
145
- new = primIO $ prim__dart_new (DartMap key val) " " [] none
146
-
147
- % inline
148
- export
149
- put : HasIO io => {key : Type } -> key -> {val : Type } -> val -> DartMap key val -> io ()
150
- put k v m = primIO $ prim__dart_invoke " []" [] [m, k, v] none
151
-
152
145
%inline
153
146
public export
154
147
Duration : Type
Original file line number Diff line number Diff line change
1
+ module Dart.Core.Map
2
+
3
+ import Dart.FFI.Elab
4
+ import Dart.Core
5
+
6
+ %language ElabReflection
7
+
8
+ %runElab importDart [
9
+ package " dart:core" [
10
+ generic [" k" , " v" ] $
11
+ class ' "MapEntry" [
12
+ final " k" " key" ,
13
+ final " v" " value"
14
+ ]
15
+ ]
16
+ ]
17
+
18
+ namespace Map
19
+
20
+ namespace FromIterable
21
+
22
+ public export
23
+ data Tag : Type where
24
+
25
+ % inline
26
+ public export
27
+ key : {a : Type } -> {k : Type } -> Parameter Tag
28
+ key = mkParameter " key" (a -> k)
29
+
30
+ % inline
31
+ public export
32
+ value : {a : Type } -> {v : Type } -> Parameter Tag
33
+ value = mkParameter " value" (a -> v)
34
+
35
+ % inline
36
+ public export
37
+ NamedParameters : {a : Type } -> {k : Type } -> {v : Type } -> Type
38
+ NamedParameters = Parameters [FromIterable . key {a = a} {k = k}, FromIterable . value {a = a} {v = v}]
39
+
40
+ % inline
41
+ export
42
+ fromIterable : HasIO io
43
+ => {k : Type }
44
+ -> {v : Type }
45
+ -> {iterable : Type }
46
+ -> {a : Type }
47
+ -> iterable
48
+ -> IsAssignableFrom (Iterable a) iterable
49
+ => (a -> k)
50
+ -> (a -> v)
51
+ -> io (Map k v)
52
+ fromIterable iter fk fv = primIO $
53
+ prim__dart_new
54
+ (Map k v)
55
+ " fromIterable"
56
+ [iter]
57
+ (the (FromIterable . NamedParameters {a = a} {k = k} {v = v}) [key @= fk, value @= fv])
58
+
59
+ % inline
60
+ public export
61
+ fromPairs : {k : Type } -> {v : Type } -> Prelude.List (k, v) -> IO (Dart.Core.Map k v)
62
+ fromPairs entries = Map . fromIterable (Dart . Core . List . fromList entries) fst snd
63
+
64
+ % inline
65
+ export
66
+ new : HasIO io => {k : Type } -> {v : Type } -> io (Map k v)
67
+ new = primIO $ prim__dart_new (Map k v) " " [] none
68
+
69
+ % inline
70
+ export
71
+ put : HasIO io => {k : Type } -> k -> {v : Type } -> v -> Map k v -> io ()
72
+ put k v m = primIO $ prim__dart_invoke " []" [] [m, k, v] none
Original file line number Diff line number Diff line change
1
+ module Dart.Core.Set
2
+
3
+ import Dart.FFI.Elab
4
+ import Dart.Core
5
+
6
+ %language ElabReflection
7
+
8
+ %runElab importDart [
9
+ package " dart:core" [
10
+ partial ' $
11
+ generic [" e" ] $
12
+ class ' "Set" [
13
+ io " bool" " contains" [" element" :: " e" ]
14
+ ]
15
+ ]
16
+ ]
You can’t perform that action at this time.
0 commit comments