[ new ] modular-dom: Modularizing the Idris dom bindings

.github/workflows/ci-lib.yml

@@ -33,6 +33,8 @@ jobs:
         run: pack install js
       - name: Build dom
         run: pack install dom
+      - name: Build modular-dom
+        run: pack install modular-dom
       - name: Build docs
         run: pack build docs/docs.ipkg
       - name: Run test

docs/src/Tutorial.md

@@ -493,7 +493,7 @@ of an unfamiliar function much easier.
 
 #### Subtyping
 
-Subtyping relations as described for interfaces, mixins, and dictionaries,
+~~Subtyping relations as described for interfaces, mixins, and dictionaries,
 are handled by interface `JS.Inheritance.JSType`. Implementations of
 this interface list associated parent types and mixins for an
 external Idris type. Function `up` and operator `(:>)` can be
@@ -517,7 +517,12 @@ additional gain in flexibility.
 Two examples: `Web.Dom.Node.firstChild` abstracts over the
 parent node's type, while `Web.Html.HTMLButtonElement.checkValidity`
 uses concrete types, since there are no child interfaces for
-`HTMLButtonElement` in the spec.
+`HTMLButtonElement` in the spec.~~
+
+The above no longer applies. Subtyping is handle simply by implementing
+`Cast a b`, where `b` is a parent type or mixin of `a`. Since
+types `a` and `b` are usually external types, such `Cast` implementations
+use `believe_me` internally.
 
 ### Web IDL types
 
@@ -558,9 +563,9 @@ nodes to the body like so:
 ```idris
 addNodes : HTMLButtonElement -> HTMLDivElement -> HTMLDivElement -> JSIO ()
 addNodes btn txtDiv outDiv =
-  ignore $ (!body `append` [ Here $ btn :> Node
-                           , Here $ txtDiv :> Node
-                           , Here $ outDiv :> Node
+  ignore $ (!body `append` [ Here $ cast btn
+                           , Here $ cast txtDiv
+                           , Here $ cast outDiv
                            ])
 ```
 

js/src/JS/Inheritance.idr

@@ -15,13 +15,16 @@ import Data.String
 ||| mixins. It is used to safely and conveniently cast a value to a
 ||| less specific type mentioned either in the list of
 ||| mixins or parent types by means of funciton `up` and operator `:>`.
+|||
+||| Deprecated: Use `Cast` and `cast` instead
 public export
 interface JSType a where
 
   ||| The inheritance chain of parent types of this data type
   ||| (starting at the direct supertype). At runtime, such an inheritance
   ||| chain can be inspected by recursively calling the Javascript
   ||| function `Object.getPrototypeOf`.
+  %deprecate
   parents : List Type
 
   ||| A Mixin is a concept from WebIDL: It is as programming interface
@@ -31,26 +34,30 @@ interface JSType a where
   ||| a value's prototype chain. It is therefore much harder
   ||| (and right now not supported in this library) to at runtime
   ||| check, whether a value implements a given mixin.
+  %deprecate
   mixins : List Type
 
 ||| Convenience alias for `parents`, which takes an explicit
 ||| erased type argument.
-public export
+||| Deprecated: Use `Cast` and `cast` instead
+public export %deprecate
 0 Types : (0 a : Type) -> JSType a => List Type
 Types a = a :: parents {a} ++ mixins {a}
 
 ||| Safe upcasting. This uses `believe_me` internally and is
 ||| therefore of course only safe, if the `JSType` implementation
 ||| is correct according to some specification and the backend
 ||| properly adhere to this specification.
-public export %inline
+||| Deprecated: Use `Cast` and `cast` instead
+public export %inline %deprecate
 up : (0 _ : JSType a) => a -> {auto 0 _ : Elem b (Types a)} -> b
 up v = believe_me v
 
 infixl 1 :>
 
 ||| Operator version of `up`.
-public export %inline
+||| Deprecated: Use `Cast` and `cast` instead
+public export %inline %deprecate
 (:>) : (0 _ : JSType a) => a -> (0 b : Type) -> {auto 0 _ : Elem b (Types a)} -> b
 a :> _ = up a
 

js/src/JS/Nullable.idr

@@ -13,16 +13,16 @@ data Nullable : Type -> Type where [external]
 %foreign "javascript:lambda:()=>null"
 prim__null : AnyPtr
 
-export
+export %inline
 null : Nullable a
 null = believe_me prim__null
 
-export
+export %inline
 nonNull : a -> Nullable a
 nonNull = believe_me
 
 ||| Tests, whether a value of questionable origin is null
-export
+export %inline
 isNull : a -> Bool
 isNull = eqv prim__null
 
@@ -31,8 +31,8 @@ maybeToNullable : Maybe a -> Nullable a
 maybeToNullable = maybe null nonNull
 
 export
-mayUp : (0 _ : JSType a) => Maybe a -> {auto 0 _ : Elem b (Types a)} -> Nullable b
-mayUp x = maybe null (\v => nonNull $ up v) x
+mayUp : Cast a b => Maybe a -> Nullable b
+mayUp x = maybe null (\v => nonNull $ cast v) x
 
 export
 nullableToMaybe : Nullable a -> Maybe a

js/src/JS/Undefined.idr

@@ -149,14 +149,11 @@ optionalToUndefOr : Optional a -> UndefOr a
 optionalToUndefOr = optional undef def
 
 export
-optUp : (0 _ : JSType a) => Optional a -> {auto 0 _ : Elem b (Types a)} -> UndefOr b
-optUp x = optional undef (\v => def $ up v) x
+optUp : Cast a b => Optional a -> UndefOr b
+optUp x = optional undef (\v => def $ cast v) x
 
 export
-omyUp :  (0 _ : JSType a)
-      => Optional (Maybe a)
-      -> {auto 0 _ : Elem b (Types a)}
-      -> UndefOr (Nullable b)
+omyUp : Cast a b => Optional (Maybe a) -> UndefOr (Nullable b)
 omyUp x = optionalToUndefOr $ map (\m => mayUp m) x
 
 public export