0 | module JS.Inheritance
  1 |
  2 | import Control.Monad.Either
  3 | import JS.Util
  4 | import Data.List.Quantifiers.Extra
  5 | import Data.String
  6 |
  7 | %default total
  8 |
  9 | --------------------------------------------------------------------------------
 10 | --          Upcasting
 11 | --------------------------------------------------------------------------------
 12 |
 13 | ||| A `JSType` describes a type's inheritance chains and implemented
 14 | ||| mixins. It is used to safely and conveniently cast a value to a
 15 | ||| less specific type mentioned either in the list of
 16 | ||| mixins or parent types by means of funciton `up` and operator `:>`.
 17 | public export
 18 | interface JSType a where
 19 |
 20 |   ||| The inheritance chain of parent types of this data type
 21 |   ||| (starting at the direct supertype). At runtime, such an inheritance
 22 |   ||| chain can be inspected by recursively calling the Javascript
 23 |   ||| function `Object.getPrototypeOf`.
 24 |   parents : List Type
 25 |
 26 |   ||| A Mixin is a concept from WebIDL: It is as programming interface
 27 |   ||| shared by several types. Unlike a WebIDL interface, a mixin does
 28 |   ||| not describe a type but just set of shared functions and
 29 |   ||| attributes. Mixins are not observable by means of inspecting
 30 |   ||| a value's prototype chain. It is therefore much harder
 31 |   ||| (and right now not supported in this library) to at runtime
 32 |   ||| check, whether a value implements a given mixin.
 33 |   mixins : List Type
 34 |
 35 | ||| Convenience alias for `parents`, which takes an explicit
 36 | ||| erased type argument.
 37 | public export
 38 | 0 Types : (0 a : Type) -> JSType a => List Type
 39 | Types a = a :: parents {a} ++ mixins {a}
 40 |
 41 | ||| Safe upcasting. This uses `believe_me` internally and is
 42 | ||| therefore of course only safe, if the `JSType` implementation
 43 | ||| is correct according to some specification and the backend
 44 | ||| properly adhere to this specification.
 45 | public export %inline
 46 | up : (0 _ : JSType a) => a -> {auto 0 _ : Elem b (Types a)} -> b
 47 | up v = believe_me v
 48 |
 49 | export infixl 1 :>
 50 |
 51 | ||| Operator version of `up`.
 52 | public export %inline
 53 | (:>) :
 54 |      {auto 0 _ : JSType a}
 55 |   -> a
 56 |   -> (0 b : Type)
 57 |   -> {auto 0 _ : Elem b (Types a)}
 58 |   -> b
 59 | a :> _ = up a
 60 |
 61 | --------------------------------------------------------------------------------
 62 | --          Downcasting
 63 | --------------------------------------------------------------------------------
 64 |
 65 | %foreign #"""
 66 |          javascript:lambda:(s,v)=>{
 67 |          var o = v;
 68 |            while (o != null) {
 69 |              var p = Object.getPrototypeOf(o);
 70 |              var cn = p.constructor.name;
 71 |              if (cn === s) {
 72 |                return 1;
 73 |              } else if (cn === "Object") {
 74 |                return 0;
 75 |              }
 76 |              o = p;
 77 |            }
 78 |            return 0;
 79 |          }
 80 |          """#
 81 | prim__hasProtoName : String -> AnyPtr -> Double
 82 |
 83 | ||| This is an interface which should be implemented by external
 84 | ||| types, the type of which can be inspected at runtime.
 85 | |||
 86 | ||| This allows us to at runtime try and safely cast any value
 87 | ||| to the type implementing this interface.
 88 | |||
 89 | ||| Typically, there are two mechanisms for inspecting a value's
 90 | ||| type at runtime: Function `typeof`, which is mainly useful
 91 | ||| for primitives, and function `unsafeCastOnPrototypeName`, which
 92 | ||| inspects a value's prototype chain
 93 | ||| ([see also](https://developer.mozilla.org/en-US/docs/Web/JavaScript/Inheritance_and_the_prototype_chain)).
 94 | |||
 95 | ||| Note, that the intention of this interface is to use it
 96 | ||| on *external* types and *primitives*, but not on types
 97 | ||| defined in Idris2. If you need to marshal Idris2 values
 98 | ||| from and to the FFI, use interfaces `ToJS` and `FromJS`.
 99 | public export
100 | interface SafeCast a where
101 |   safeCast : {0 x : Type} -> x -> Maybe a
102 |
103 | public export %inline
104 | castTo : (0 a : Type) -> SafeCast a => x -> Maybe a
105 | castTo _ v = safeCast v
106 |
107 | ||| Tries to create an n-ary sum by trying all possible
108 | ||| casts. The first successful cast will determine the
109 | ||| result.
110 | export
111 | safeCastAny : (prf : All SafeCast ts) => x -> Maybe (HSum ts)
112 | safeCastAny @{[]}     x = Nothing
113 | safeCastAny @{h :: t} x = case safeCast @{h} x of
114 |   Just v  => Just $ Here v
115 |   Nothing => There <$> safeCastAny @{t} x
116 |
117 | ||| This is a utility function to implement instances of
118 | ||| `SafeCast`. Only use, if you know what you are doing.
119 | export
120 | unsafeCastOnPrototypeName : String -> a -> Maybe b
121 | unsafeCastOnPrototypeName s a =
122 |   if prim__hasProtoName s (believe_me a) == 1.0
123 |      then Just (believe_me a)
124 |      else Nothing
125 |
126 | ||| This is a utility function to implement instances of
127 | ||| `SafeCast`. Only use, if you know what you are doing.
128 | export
129 | unsafeCastOnTypeof : String -> a -> Maybe b
130 | unsafeCastOnTypeof s a =
131 |   if typeof a == s then Just (believe_me a) else Nothing
132 |
133 | export
134 | SafeCast Integer where
135 |   safeCast = unsafeCastOnTypeof "bigint"
136 |
137 | export
138 | SafeCast Double where
139 |   safeCast = unsafeCastOnTypeof "number"
140 |
141 | export
142 | SafeCast String where
143 |   safeCast = unsafeCastOnTypeof "string"
144 |
145 | -- As far as I understand, there are no "single characters"
146 | -- in Javascript, only strings of length 1. Thats why we go via
147 | -- String here
148 | export
149 | SafeCast Char where
150 |   safeCast v = safeCast v >>= \s =>
151 |     case strM s of
152 |       StrCons x "" => Just x
153 |       _            => Nothing
154 |
155 | export
156 | bounded : Num a => (min : Integer) -> (max : Integer) -> x -> Maybe a
157 | bounded min max ptr =
158 |   safeCast ptr >>= \n =>
159 |     if n >= min && n <= max
160 |       then Just (fromInteger n)
161 |       else Nothing
162 |
163 | export
164 | SafeCast Bits8 where
165 |   safeCast = bounded 0 0xff
166 |
167 | export
168 | SafeCast Bits16 where
169 |   safeCast = bounded 0 0xffff
170 |
171 | export
172 | SafeCast Bits32 where
173 |   safeCast = bounded 0 0xffffffff
174 |
175 | export
176 | SafeCast Bits64 where
177 |   safeCast = bounded 0 0xffffffffffffffff
178 |
179 | export
180 | SafeCast Int8 where
181 |   safeCast = bounded (-0x80) 0x7f
182 |
183 | export
184 | SafeCast Int16 where
185 |   safeCast = bounded (-0x8000) 0x7fff
186 |
187 | export
188 | SafeCast Int32 where
189 |   safeCast = bounded (-0x80000000) 0x7fffffff
190 |
191 | export
192 | SafeCast Int64 where
193 |   safeCast = bounded (-0x8000000000000000) 0x7fffffffffffffff
194 |
195 | export
196 | SafeCast Int where
197 |   safeCast = bounded (- 0x80000000) (0x7fffffff)
198 |
199 | export
200 | tryCast : SafeCast a => (fun : Lazy String) -> x -> JSIO a
201 | tryCast fun val = case safeCast val of
202 |   Just a  => pure a
203 |   Nothing => throwError $ CastErr fun val
204 |
205 | export
206 | tryCast_ : (0 a : Type) -> SafeCast a => (fun : Lazy String) -> x -> JSIO a
207 | tryCast_ _ = tryCast
208 |
209 | export
210 | castingTo : SafeCast a => (fun : String) -> JSIO x -> JSIO a
211 | castingTo fun io = io >>= tryCast fun
212 |