Idris2Doc : Text.WebIDL.Codegen.Types

Text.WebIDL.Codegen.Types

(source)
Reexports
import public Data.SortedMap
Definitions
data Kind : Type
  The kind of a WebIDL identifier.
  
  This is needed when converting external types to Idris2 types
  in the code generator: Aliases need to be resolved, Enums
  converted to their `String` representation, Callback arguments
  are Idris2 functions that need to be converted to an external
  type.

  Totality: total
  Visibility: public export
  Constructors:
  
KAlias : Identifier -> Kind
  
KCallback : Identifier -> Kind
  
KDictionary : Identifier -> Kind
  
KEnum : Identifier -> Kind
  
KInterface : Bool -> Identifier -> Kind
  
KMixin : Identifier -> Kind
  
KOther : Identifier -> Kind

  Hints:
  
Eq Kind
  
Show Kind
isParent : Kind -> Bool
  Totality: total
  Visibility: public export
ident : Kind -> Identifier
  Totality: total
  Visibility: public export
kindToString : Kind -> String
  Totality: total
  Visibility: public export
data Wrapper : Type
  Totality: total
  Visibility: public export
  Constructors:
  
Direct : Wrapper
  
Opt : Wrapper
  
May : Wrapper
  
OptMay : Wrapper
opt : Wrapper -> Wrapper
  Totality: total
  Visibility: public export
may : Wrapper -> Wrapper
  Totality: total
  Visibility: public export
data SimpleType : Type
  Totality: total
  Visibility: public export
  Constructors:
  
Undef : SimpleType
  The undefined type (or () if it is a return type)
  
Boolean : SimpleType
  `Boolean` at the FFI, `Bool` in the API.
  
Interface : Bool -> Identifier -> SimpleType
  A Web IDL interface. This has an instance of `SafeCast`,
  and is being abstracted over when used in an argument
  list in the API, but only, when the `isParent` flag is set to true.
  If this flag is `False`, meaning that there are no subtypes of
  this type, we do not abstract over the type to improve
  type inference.
  
Dictionary : Identifier -> SimpleType
  A dictionary, specifying a Javascript object with a
  set of mandatory and optional attributes.
  This is always abstracted over, since theoretically
  every value with the same set of attributes is
  a dictionary of the given type.
  
  The type of a dictionary cannot be verified at
  runtime, therefore they have no instance of `SafeCast`.
  
Mixin : Identifier -> SimpleType
  A Web IDL `Mixin` is a set of attributes and operations (functions)
  shared by several types. A type includes a given mixin, if
  a corresponding `includes` statement is provided in the spec.
  
  Mixins do not define new types, and whether a value implements
  a given mixin can typcally not be verified at runtime, therefore
  mixins come without an instance of `SafeCast`.
  runtime, therefore they have no instance of `SafeCast`.
  
Primitive : String -> SimpleType
  Primitive type or a wrapper of a primitive.
  This is the same at the FFI and API and
  has an instance of `SafeCast`.
  
Unchangeable : String -> SimpleType
  Types that do not change between FFI and API
  
Enum : Identifier -> SimpleType
  Enum type at the API, Strings at the FFI
  
Array : CGType -> SimpleType
  Some kind of Array
  
Record : String -> CGType -> SimpleType
  Some kind of Record
data CGType : Type
  Totality: total
  Visibility: public export
  Constructors:
  
Any : CGType
  
Promise : CGType -> CGType
  
Simple : Nullable SimpleType -> CGType
  
Union : Nullable (List1 SimpleType) -> CGType
isIndex : CGType -> Bool
  True, if the type can be used as an index in a
  WebIDL `Getter` or `Setter`, that is, it corresponds
  to either an `unsigned long` or a `DOMString`.

  Totality: total
  Visibility: export
safeCast : SimpleType -> Bool
  True, if the FFI representation of the given type
  has a `SafeCast` implementation

  Totality: total
  Visibility: export
sameArgType : SimpleType -> Bool
  True, if the type uses the same representation in
  the FFI and the API as a function argument

  Totality: total
  Visibility: export
sameRetType : SimpleType -> Bool
  True, if the type uses the same representation in
  the FFI and the API as a return value.

  Totality: total
  Visibility: export
inheritance : SimpleType -> Maybe (Identifier, Wrapper)
  Totality: total
  Visibility: export
simple : SimpleType -> CGType
  Totality: total
  Visibility: public export
unchangeable : String -> CGType
  Totality: total
  Visibility: public export
iface : Bool -> Identifier -> CGType
  Totality: total
  Visibility: public export
mixin : Identifier -> CGType
  Totality: total
  Visibility: public export
dict : Identifier -> CGType
  Totality: total
  Visibility: public export
fromKind : Kind -> CGType
  Wrapps the given kind in return type.

  Totality: total
  Visibility: export
safeCast : CGType -> Bool
  True, if the FFI representation of the given type
  has a `SafeCast` implementation

  Totality: total
  Visibility: export
sameArgType : CGType -> Bool
  True, if the given type is the same in the API and
  the FFI when used as an argument

  Totality: total
  Visibility: export
sameRetType : CGType -> Bool
  True, if the given type is the same in the API and
  the FFI when used as a return value

  Totality: total
  Visibility: export
inheritance : CGType -> Maybe (Identifier, Wrapper)
  Totality: total
  Visibility: export
data ReturnType : Type
  A function's return type.

  Totality: total
  Visibility: public export
  Constructors:
  
Undefined : ReturnType
  This will be mapped to `()` in the codegen.
  
UndefOr : CGType -> Maybe Default -> ReturnType
  The attribute in question might not be defined
  The return type will be wrapped in `UndefOr` in
  the code generator.
  
Def : CGType -> ReturnType
  Nothing special about the wrapped return type.
isUndefined : ReturnType -> Bool
  Checks if the return type is `Undefined`.

  Totality: total
  Visibility: public export
simple : SimpleType -> ReturnType
  Totality: total
  Visibility: public export
unchangeable : String -> ReturnType
  Totality: total
  Visibility: public export
fromKind : Kind -> ReturnType
  Wrapps the given kind in return type.

  Totality: total
  Visibility: export
safeCast : ReturnType -> Bool
  True, if the given FFI type has a `SafeCast` instance

  Totality: total
  Visibility: export
sameType : ReturnType -> Bool
  True, if the given return type is the same in the API and
  the FFI.

  Totality: total
  Visibility: export
record CGConstType : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkConstType : String -> CGConstType

  Projection: 
.primitive : CGConstType -> String
.primitive : CGConstType -> String
  Totality: total
  Visibility: public export
primitive : CGConstType -> String
  Totality: total
  Visibility: public export
record CGConst : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkConst : CGConstType -> Identifier -> ConstValue -> CGConst

  Projections:
  
.name : CGConst -> Identifier
  
.type : CGConst -> CGConstType
  
.value : CGConst -> ConstValue
.type : CGConst -> CGConstType
  Totality: total
  Visibility: public export
type : CGConst -> CGConstType
  Totality: total
  Visibility: public export
.name : CGConst -> Identifier
  Totality: total
  Visibility: public export
name : CGConst -> Identifier
  Totality: total
  Visibility: public export
.value : CGConst -> ConstValue
  Totality: total
  Visibility: public export
value : CGConst -> ConstValue
  Totality: total
  Visibility: public export
data CGArg : Type
  A function argument in the code generator.

  Totality: total
  Visibility: public export
  Constructors:
  
Mandatory : ArgumentName -> CGType -> CGArg
  A mandatory function argument
  
Optional : ArgumentName -> CGType -> Default -> CGArg
  An optional function argument together with its
  default value if the argument is `undefined`.
  
VarArg : ArgumentName -> CGType -> CGArg
  A variadic function argument
argName : CGArg -> ArgumentName
  Totality: total
  Visibility: export
argType : CGArg -> CGType
  Totality: total
  Visibility: export
isOptional : CGArg -> Bool
  Totality: total
  Visibility: export
safeCast : CGArg -> Bool
  True, if the given FFI type has a `SafeCast` instance

  Totality: total
  Visibility: export
sameType : CGArg -> Bool
  True, if the given argument type is the same in the API and
  the FFI.

  Totality: total
  Visibility: export
inheritance : CGArg -> Maybe (Identifier, Wrapper)
  Totality: total
  Visibility: export
Args : Type
  Totality: total
  Visibility: public export
data CGFunction : Type
  A function, for which we will generate some code.

  Totality: total
  Visibility: public export
  Constructors:
  
Attribute : AttributeName -> Kind -> CGArg -> ReturnType -> CGFunction
  A read-write attribute
  
AttributeGet : AttributeName -> Kind -> ReturnType -> CGFunction
  An attribute getter.
  
StaticAttributeSet : AttributeName -> Kind -> CGArg -> CGFunction
  A static attribute setter.
  
StaticAttributeGet : AttributeName -> Kind -> ReturnType -> CGFunction
  A static attribute getter.
  
Getter : Kind -> CGArg -> ReturnType -> CGFunction
  An indexed getter.
  
Setter : Kind -> CGArg -> CGArg -> CGFunction
  An indexed setter.
  
Constructor : Kind -> Args -> CGFunction
  An interface constructor with (possibly) optional arguments.
  
DictConstructor : Kind -> Args -> CGFunction
  An interface constructor with (possibly) optional arguments.
  
Regular : OperationName -> Kind -> Args -> ReturnType -> CGFunction
  A regular function with (possibly) optional arguments.
  
Static : OperationName -> Kind -> Args -> ReturnType -> CGFunction
  A static function with (possibly) optional arguments.
priority : CGFunction -> (Nat, (String, Nat))
  This is used for sorting lists of functions to
  determine the order in which they appear
  in the generated code.
  
  Attributes will come first, sorted by name,
  setters, getters, and unsetter grouped together in
  that order.
  
  All other functions come later and will be sorted by name.

  Totality: total
  Visibility: export
record JSType : Type
  An external, un-parameterized Javascript type, represented
  by an identifier. Such a type comes with a parent
  type (given as an `inheritance` value in the spec)
  and a number of mixed in types.
  
  The actual name of the type is not included, as the set
  of types is given in `Env` as a `SortedMap`.

  Totality: total
  Visibility: public export
  Constructor: 
MkJSType : Maybe Identifier -> List Identifier -> JSType

  Projections:
  
.mixins : JSType -> List Identifier
  
.parent : JSType -> Maybe Identifier
.parent : JSType -> Maybe Identifier
  Totality: total
  Visibility: public export
parent : JSType -> Maybe Identifier
  Totality: total
  Visibility: public export
.mixins : JSType -> List Identifier
  Totality: total
  Visibility: public export
mixins : JSType -> List Identifier
  Totality: total
  Visibility: public export
record Supertypes : Type
  The parent types and mixins of a type. This is
  used by the code generator to implement the
  `JS.Inheritance.JSType` instances.

  Totality: total
  Visibility: public export
  Constructor: 
MkSupertypes : List Identifier -> List Identifier -> Supertypes

  Projections:
  
.mixins : Supertypes -> List Identifier
  
.parents : Supertypes -> List Identifier
.parents : Supertypes -> List Identifier
  Totality: total
  Visibility: public export
parents : Supertypes -> List Identifier
  Totality: total
  Visibility: public export
.mixins : Supertypes -> List Identifier
  Totality: total
  Visibility: public export
mixins : Supertypes -> List Identifier
  Totality: total
  Visibility: public export
record CGDict : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkDict : Identifier -> Supertypes -> List CGFunction -> CGDict

  Projections:
  
.functions : CGDict -> List CGFunction
  
.name : CGDict -> Identifier
  
.super : CGDict -> Supertypes
.name : CGDict -> Identifier
  Totality: total
  Visibility: public export
name : CGDict -> Identifier
  Totality: total
  Visibility: public export
.super : CGDict -> Supertypes
  Totality: total
  Visibility: public export
super : CGDict -> Supertypes
  Totality: total
  Visibility: public export
.functions : CGDict -> List CGFunction
  Totality: total
  Visibility: public export
functions : CGDict -> List CGFunction
  Totality: total
  Visibility: public export
record CGIface : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkIface : Identifier -> Supertypes -> List CGConst -> List CGFunction -> CGIface

  Projections:
  
.constants : CGIface -> List CGConst
  
.functions : CGIface -> List CGFunction
  
.name : CGIface -> Identifier
  
.super : CGIface -> Supertypes
.name : CGIface -> Identifier
  Totality: total
  Visibility: public export
name : CGIface -> Identifier
  Totality: total
  Visibility: public export
.super : CGIface -> Supertypes
  Totality: total
  Visibility: public export
super : CGIface -> Supertypes
  Totality: total
  Visibility: public export
.constants : CGIface -> List CGConst
  Totality: total
  Visibility: public export
constants : CGIface -> List CGConst
  Totality: total
  Visibility: public export
.functions : CGIface -> List CGFunction
  Totality: total
  Visibility: public export
functions : CGIface -> List CGFunction
  Totality: total
  Visibility: public export
record CGMixin : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkMixin : Identifier -> List CGConst -> List CGFunction -> CGMixin

  Projections:
  
.constants : CGMixin -> List CGConst
  
.functions : CGMixin -> List CGFunction
  
.name : CGMixin -> Identifier
.name : CGMixin -> Identifier
  Totality: total
  Visibility: public export
name : CGMixin -> Identifier
  Totality: total
  Visibility: public export
.constants : CGMixin -> List CGConst
  Totality: total
  Visibility: public export
constants : CGMixin -> List CGConst
  Totality: total
  Visibility: public export
.functions : CGMixin -> List CGFunction
  Totality: total
  Visibility: public export
functions : CGMixin -> List CGFunction
  Totality: total
  Visibility: public export
record CGCallback : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkCallback : Identifier -> List CGConst -> ReturnType -> Args -> CGCallback

  Projections:
  
.args : CGCallback -> Args
  
.constants : CGCallback -> List CGConst
  
.name : CGCallback -> Identifier
  
.type : CGCallback -> ReturnType
.name : CGCallback -> Identifier
  Totality: total
  Visibility: public export
name : CGCallback -> Identifier
  Totality: total
  Visibility: public export
.constants : CGCallback -> List CGConst
  Totality: total
  Visibility: public export
constants : CGCallback -> List CGConst
  Totality: total
  Visibility: public export
.type : CGCallback -> ReturnType
  Totality: total
  Visibility: public export
type : CGCallback -> ReturnType
  Totality: total
  Visibility: public export
.args : CGCallback -> Args
  Totality: total
  Visibility: public export
args : CGCallback -> Args
  Totality: total
  Visibility: public export
record CGDomain : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkDomain : String -> List CGCallback -> List CGDict -> List Enum -> List CGIface -> List CGMixin -> CGDomain

  Projections:
  
.callbacks : CGDomain -> List CGCallback
  
.dicts : CGDomain -> List CGDict
  
.enums : CGDomain -> List Enum
  
.ifaces : CGDomain -> List CGIface
  
.mixins : CGDomain -> List CGMixin
  
.name : CGDomain -> String
.name : CGDomain -> String
  Totality: total
  Visibility: public export
name : CGDomain -> String
  Totality: total
  Visibility: public export
.callbacks : CGDomain -> List CGCallback
  Totality: total
  Visibility: public export
callbacks : CGDomain -> List CGCallback
  Totality: total
  Visibility: public export
.dicts : CGDomain -> List CGDict
  Totality: total
  Visibility: public export
dicts : CGDomain -> List CGDict
  Totality: total
  Visibility: public export
.enums : CGDomain -> List Enum
  Totality: total
  Visibility: public export
enums : CGDomain -> List Enum
  Totality: total
  Visibility: public export
.ifaces : CGDomain -> List CGIface
  Totality: total
  Visibility: public export
ifaces : CGDomain -> List CGIface
  Totality: total
  Visibility: public export
.mixins : CGDomain -> List CGMixin
  Totality: total
  Visibility: public export
mixins : CGDomain -> List CGMixin
  Totality: total
  Visibility: public export
domainFunctions : CGDomain -> List CGFunction
  Totality: total
  Visibility: export
record Env : Type
  Codegen environment.
  
  This includes a mapping from identifiers to the kinds
  they represent, a mapping from identifiers to their
  inheritance relations (`jsTypes`) and a mapping of
  type aliases.
  
  The `maxInheritance` constant is used when calculating a
  type's supertypes to avoid a potentially infinite loop.

  Totality: total
  Visibility: public export
  Constructor: 
MkEnv : Nat -> SortedMap Identifier Kind -> SortedMap Identifier JSType -> SortedMap Identifier (IdlTypeF ExtAttributeList Kind) -> Env

  Projections:
  
.aliases : Env -> SortedMap Identifier (IdlTypeF ExtAttributeList Kind)
  
.jsTypes : Env -> SortedMap Identifier JSType
  
.kinds : Env -> SortedMap Identifier Kind
  
.maxInheritance : Env -> Nat
.maxInheritance : Env -> Nat
  Totality: total
  Visibility: public export
maxInheritance : Env -> Nat
  Totality: total
  Visibility: public export
.kinds : Env -> SortedMap Identifier Kind
  Totality: total
  Visibility: public export
kinds : Env -> SortedMap Identifier Kind
  Totality: total
  Visibility: public export
.jsTypes : Env -> SortedMap Identifier JSType
  Totality: total
  Visibility: public export
jsTypes : Env -> SortedMap Identifier JSType
  Totality: total
  Visibility: public export
.aliases : Env -> SortedMap Identifier (IdlTypeF ExtAttributeList Kind)
  Totality: total
  Visibility: public export
aliases : Env -> SortedMap Identifier (IdlTypeF ExtAttributeList Kind)
  Totality: total
  Visibility: public export
data CodegenErr : Type
  Totality: total
  Visibility: public export
  Constructors:
  
AnyInUnion : Domain -> CodegenErr
  
CBInterfaceInvalidOps : Domain -> Identifier -> Nat -> CodegenErr
  
InvalidConstType : Domain -> CodegenErr
  
InvalidGetter : Domain -> Identifier -> CodegenErr
  
InvalidSetter : Domain -> Identifier -> CodegenErr
  
NullableAny : Domain -> CodegenErr
  
NullablePromise : Domain -> CodegenErr
  
PromiseInUnion : Domain -> CodegenErr
  
RegularOpWithoutName : Domain -> Identifier -> CodegenErr
  
UnresolvedAlias : Domain -> Identifier -> CodegenErr
Codegen : Type -> Type
  Totality: total
  Visibility: public export