0 | module JS.Undefined
  1 |
  2 | import Data.List.Elem
  3 | import JS.Util
  4 | import JS.Inheritance
  5 | import JS.Marshall
  6 | import JS.Nullable
  7 |
  8 | %default total
  9 |
 10 | --------------------------------------------------------------------------------
 11 | --          Undefined
 12 | --------------------------------------------------------------------------------
 13 |
 14 | export
 15 | data Undefined : Type where [external]
 16 |
 17 | ||| The `undefined` constant
 18 | export
 19 | %foreign "javascript:lambda:()=>undefined"
 20 | undefined : Undefined
 21 |
 22 | export
 23 | Eq Undefined where
 24 |   _ == _ = True
 25 |
 26 | export
 27 | Show Undefined where
 28 |   show _ = "undefined"
 29 |
 30 | %foreign "javascript:lambda:x=>x === undefined?1:0"
 31 | prim__isUndefined : AnyPtr -> Bool
 32 |
 33 | ||| Tests, whether a value of questionable origin is undefined
 34 | export
 35 | isUndefined : a -> Bool
 36 | isUndefined v = prim__isUndefined (believe_me v)
 37 |
 38 | export
 39 | ToFFI Undefined Undefined where
 40 |   toFFI = id
 41 |
 42 | export
 43 | FromFFI Undefined Undefined where
 44 |   fromFFI = Just
 45 |
 46 | export
 47 | SafeCast Undefined where
 48 |   safeCast ptr = if isUndefined ptr then Just undefined else Nothing
 49 |
 50 | --------------------------------------------------------------------------------
 51 | --          UndefOr
 52 | --------------------------------------------------------------------------------
 53 |
 54 | export
 55 | data UndefOr : Type -> Type where [external]
 56 |
 57 | export
 58 | undef : UndefOr a
 59 | undef = believe_me undefined
 60 |
 61 | export
 62 | def : a -> UndefOr a
 63 | def = believe_me
 64 |
 65 | export
 66 | SafeCast a => SafeCast (UndefOr a) where
 67 |   safeCast ptr =
 68 |     if isUndefined ptr
 69 |       then Just undef
 70 |       else map def $ safeCast ptr
 71 |
 72 | --------------------------------------------------------------------------------
 73 | --          Optional
 74 | --------------------------------------------------------------------------------
 75 |
 76 | public export
 77 | data Optional : (a : Type) -> Type where
 78 |   Undef : Optional a
 79 |   Def   : a -> Optional a
 80 |
 81 | export
 82 | Show a => Show (Optional a) where
 83 |   showPrec _ Undef   = "Undef"
 84 |   showPrec p (Def a) = showCon p "Def" (showArg a)
 85 |
 86 | public export
 87 | Eq a => Eq (Optional a) where
 88 |   Undef == Undef = True
 89 |   Def x == Def y = x == y
 90 |   _     == _     = False
 91 |
 92 | public export
 93 | Ord a => Ord (Optional a) where
 94 |   compare Undef Undef     = EQ
 95 |   compare Undef (Def _)   = LT
 96 |   compare (Def _) Undef   = GT
 97 |   compare (Def x) (Def y) = compare x y
 98 |
 99 | public export
100 | Functor Optional where
101 |   map _ Undef   = Undef
102 |   map f (Def x) = Def $ f x
103 |
104 | public export
105 | Applicative Optional where
106 |   pure = Def
107 |   Def f <*> Def a = Def $ f a
108 |   _     <*>     _ = Undef
109 |
110 | public export
111 | Monad Optional where
112 |   Undef >>= _ = Undef
113 |   Def x >>= f = f x
114 |
115 | public export
116 | Alternative Optional where
117 |   empty = Undef
118 |   Undef <|> x = x
119 |   Def v <|> _ = Def v
120 |
121 | public export
122 | Foldable Optional where
123 |   foldr _ acc Undef   = acc
124 |   foldr f acc (Def x) = f x acc
125 |
126 |   foldl _ acc Undef   = acc
127 |   foldl f acc (Def x) = f acc x
128 |
129 |   null Undef   = True
130 |   null (Def _) = False
131 |
132 | public export
133 | Traversable Optional where
134 |   traverse f Undef   = pure Undef
135 |   traverse f (Def x) = Def <$> f x
136 |
137 | public export
138 | optional : Lazy b -> (a -> b) -> Optional a -> b
139 | optional x f Undef   = x
140 | optional _ f (Def y) = f y
141 |
142 | public export
143 | fromOptional : Lazy a -> Optional a -> a
144 | fromOptional a Undef   = a
145 | fromOptional _ (Def a) = a
146 |
147 | export
148 | optionalToUndefOr : Optional a -> UndefOr a
149 | optionalToUndefOr = optional undef def
150 |
151 | export
152 | optUp :
153 |      {auto 0 _ : JSType a}
154 |   -> Optional a
155 |   -> {auto 0 _ : Elem b (Types a)}
156 |   -> UndefOr b
157 | optUp x = optional undef (\v => def $ up v) x
158 |
159 | export
160 | omyUp :
161 |      {auto 0 _ : JSType a}
162 |   -> Optional (Maybe a)
163 |   -> {auto 0 _ : Elem b (Types a)}
164 |   -> UndefOr (Nullable b)
165 | omyUp x = optionalToUndefOr $ map (\m => mayUp m) x
166 |
167 | public export
168 | maybeToOptional : Maybe a -> Optional a
169 | maybeToOptional = maybe Undef Def
170 |
171 | public export
172 | optionalToMaybe : Optional a -> Maybe a
173 | optionalToMaybe = optional Nothing Just
174 |
175 | export
176 | undeforToOptional : UndefOr a -> Optional a
177 | undeforToOptional v = if isUndefined v then Undef else Def (believe_me v)
178 |
179 | export
180 | undeforToMaybe : UndefOr a -> Maybe a
181 | undeforToMaybe v = if isUndefined v then Nothing else Just (believe_me v)
182 |
183 | export
184 | ToFFI a b => ToFFI (Optional a) (UndefOr b) where
185 |   toFFI = optionalToUndefOr . map toFFI
186 |
187 | export
188 | FromFFI a b => FromFFI (Optional a) (UndefOr b) where
189 |   fromFFI v = case undeforToOptional v of
190 |     Undef => Just Undef
191 |     Def x => map Def $ fromFFI x
192 |