0 | module JS.Nullable
 1 |
 2 | import Data.List.Elem
 3 | import JS.Inheritance
 4 | import JS.Marshall
 5 | import JS.Util
 6 |
 7 | %default total
 8 |
 9 | export
10 | data Nullable : Type -> Type where [external]
11 |
12 | %foreign "javascript:lambda:()=>null"
13 | prim__null : AnyPtr
14 |
15 | export
16 | null : Nullable a
17 | null = believe_me prim__null
18 |
19 | export
20 | nonNull : a -> Nullable a
21 | nonNull = believe_me
22 |
23 | ||| Tests, whether a value of questionable origin is null
24 | export
25 | isNull : a -> Bool
26 | isNull = eqv prim__null
27 |
28 | export
29 | maybeToNullable : Maybe a -> Nullable a
30 | maybeToNullable = maybe null nonNull
31 |
32 | export
33 | mayUp :
34 |      {auto 0 _ : JSType a}
35 |   -> Maybe a
36 |   -> {auto 0 _ : Elem b (Types a)}
37 |   -> Nullable b
38 | mayUp x = maybe null (\v => nonNull $ up v) x
39 |
40 | export
41 | nullableToMaybe : Nullable a -> Maybe a
42 | nullableToMaybe v = if isNull v then Nothing else Just (believe_me v)
43 |
44 | export
45 | ToFFI a b => ToFFI (Maybe a) (Nullable b) where
46 |   toFFI = maybeToNullable . map toFFI
47 |
48 | export
49 | FromFFI a b => FromFFI (Maybe a) (Nullable b) where
50 |   fromFFI v = case nullableToMaybe v of
51 |     Nothing => Just Nothing
52 |     Just x  => map Just $ fromFFI x
53 |
54 | export
55 | SafeCast a => SafeCast (Nullable a) where
56 |   safeCast ptr =
57 |     if isNull ptr
58 |       then Just null
59 |       else map nonNull $ safeCast ptr
60 |