text:
module Web.Raw.Mediastream

import JS
import Web.Internal.MediastreamPrim
import Web.Internal.Types

--------------------------------------------------------------------------------
--          Interfaces
--------------------------------------------------------------------------------

namespace ConstrainablePattern

  export
  applyConstraints :  (0 _ : JSType t1)
                   => {auto 0 _ : Elem Constraints (Types t1)}
                   -> (obj : ConstrainablePattern)
                   -> (constraints : Optional t1)
                   -> JSIO (Promise Undefined)
  applyConstraints a b = primJS
                       $ ConstrainablePattern.prim__applyConstraints a (optUp b)

  export
  applyConstraints' : (obj : ConstrainablePattern) -> JSIO (Promise Undefined)
  applyConstraints' a = primJS
                      $ ConstrainablePattern.prim__applyConstraints a undef

  export
  getCapabilities : (obj : ConstrainablePattern) -> JSIO Capabilities
  getCapabilities a = primJS $ ConstrainablePattern.prim__getCapabilities a

  export
  getConstraints : (obj : ConstrainablePattern) -> JSIO Constraints
  getConstraints a = primJS $ ConstrainablePattern.prim__getConstraints a

  export
  getSettings : (obj : ConstrainablePattern) -> JSIO Settings
  getSettings a = primJS $ ConstrainablePattern.prim__getSettings a

namespace InputDeviceInfo

  export
  getCapabilities : (obj : InputDeviceInfo) -> JSIO MediaTrackCapabilities
  getCapabilities a = primJS $ InputDeviceInfo.prim__getCapabilities a

namespace MediaDeviceInfo

  export
  deviceId :  (0 _ : JSType t1)
           => {auto 0 _ : Elem MediaDeviceInfo (Types t1)}
           -> (obj : t1)
           -> JSIO String
  deviceId a = primJS $ MediaDeviceInfo.prim__deviceId (up a)

  export
  groupId :  (0 _ : JSType t1)
          => {auto 0 _ : Elem MediaDeviceInfo (Types t1)}
          -> (obj : t1)
          -> JSIO String
  groupId a = primJS $ MediaDeviceInfo.prim__groupId (up a)

  export
  kind :  (0 _ : JSType t1)
       => {auto 0 _ : Elem MediaDeviceInfo (Types t1)}
       -> (obj : t1)
       -> JSIO MediaDeviceKind
  kind a = tryJS "MediaDeviceInfo.kind" $ MediaDeviceInfo.prim__kind (up a)

  export
  label :  (0 _ : JSType t1)
        => {auto 0 _ : Elem MediaDeviceInfo (Types t1)}
        -> (obj : t1)
        -> JSIO String
  label a = primJS $ MediaDeviceInfo.prim__label (up a)

  export
  toJSON :  (0 _ : JSType t1)
         => {auto 0 _ : Elem MediaDeviceInfo (Types t1)}
         -> (obj : t1)
         -> JSIO Object
  toJSON a = primJS $ MediaDeviceInfo.prim__toJSON (up a)

namespace MediaDevices

  export
  ondevicechange : MediaDevices -> Attribute False Maybe EventHandlerNonNull
  ondevicechange v = fromNullablePrim "MediaDevices.getondevicechange"
                                      prim__ondevicechange
                                      prim__setOndevicechange
                                      v

  export
  enumerateDevices :  (obj : MediaDevices)
                   -> JSIO (Promise (Array MediaDeviceInfo))
  enumerateDevices a = primJS $ MediaDevices.prim__enumerateDevices a

  export
  getSupportedConstraints :  (obj : MediaDevices)
                          -> JSIO MediaTrackSupportedConstraints
  getSupportedConstraints a = primJS
                            $ MediaDevices.prim__getSupportedConstraints a

  export
  getUserMedia :  (0 _ : JSType t1)
               => {auto 0 _ : Elem MediaStreamConstraints (Types t1)}
               -> (obj : MediaDevices)
               -> (constraints : Optional t1)
               -> JSIO (Promise MediaStream)
  getUserMedia a b = primJS $ MediaDevices.prim__getUserMedia a (optUp b)

  export
  getUserMedia' : (obj : MediaDevices) -> JSIO (Promise MediaStream)
  getUserMedia' a = primJS $ MediaDevices.prim__getUserMedia a undef

namespace MediaStream

  export
  new : JSIO MediaStream
  new = primJS $ MediaStream.prim__new

  export
  new1 : (stream : MediaStream) -> JSIO MediaStream
  new1 a = primJS $ MediaStream.prim__new1 a

  export
  new2 : (tracks : Array MediaStreamTrack) -> JSIO MediaStream
  new2 a = primJS $ MediaStream.prim__new2 a

  export
  active : (obj : MediaStream) -> JSIO Bool
  active a = tryJS "MediaStream.active" $ MediaStream.prim__active a

  export
  id : (obj : MediaStream) -> JSIO String
  id a = primJS $ MediaStream.prim__id a

  export
  onaddtrack : MediaStream -> Attribute False Maybe EventHandlerNonNull
  onaddtrack v = fromNullablePrim "MediaStream.getonaddtrack"
                                  prim__onaddtrack
                                  prim__setOnaddtrack
                                  v

  export
  onremovetrack : MediaStream -> Attribute False Maybe EventHandlerNonNull
  onremovetrack v = fromNullablePrim "MediaStream.getonremovetrack"
                                     prim__onremovetrack
                                     prim__setOnremovetrack
                                     v

  export
  addTrack : (obj : MediaStream) -> (track : MediaStreamTrack) -> JSIO ()
  addTrack a b = primJS $ MediaStream.prim__addTrack a b

  export
  clone : (obj : MediaStream) -> JSIO MediaStream
  clone a = primJS $ MediaStream.prim__clone a

  export
  getAudioTracks : (obj : MediaStream) -> JSIO (Array MediaStreamTrack)
  getAudioTracks a = primJS $ MediaStream.prim__getAudioTracks a

  export
  getTrackById :  (obj : MediaStream)
               -> (trackId : String)
               -> JSIO (Maybe MediaStreamTrack)
  getTrackById a b = tryJS "MediaStream.getTrackById"
                   $ MediaStream.prim__getTrackById a b

  export
  getTracks : (obj : MediaStream) -> JSIO (Array MediaStreamTrack)
  getTracks a = primJS $ MediaStream.prim__getTracks a

  export
  getVideoTracks : (obj : MediaStream) -> JSIO (Array MediaStreamTrack)
  getVideoTracks a = primJS $ MediaStream.prim__getVideoTracks a

  export
  removeTrack : (obj : MediaStream) -> (track : MediaStreamTrack) -> JSIO ()
  removeTrack a b = primJS $ MediaStream.prim__removeTrack a b

namespace MediaStreamTrack

  export
  enabled : MediaStreamTrack -> Attribute True I Bool
  enabled v = fromPrim "MediaStreamTrack.getenabled"
                       prim__enabled
                       prim__setEnabled
                       v

  export
  id : (obj : MediaStreamTrack) -> JSIO String
  id a = primJS $ MediaStreamTrack.prim__id a

  export
  kind : (obj : MediaStreamTrack) -> JSIO String
  kind a = primJS $ MediaStreamTrack.prim__kind a

  export
  label : (obj : MediaStreamTrack) -> JSIO String
  label a = primJS $ MediaStreamTrack.prim__label a

  export
  muted : (obj : MediaStreamTrack) -> JSIO Bool
  muted a = tryJS "MediaStreamTrack.muted" $ MediaStreamTrack.prim__muted a

  export
  onended : MediaStreamTrack -> Attribute False Maybe EventHandlerNonNull
  onended v = fromNullablePrim "MediaStreamTrack.getonended"
                               prim__onended
                               prim__setOnended
                               v

  export
  onmute : MediaStreamTrack -> Attribute False Maybe EventHandlerNonNull
  onmute v = fromNullablePrim "MediaStreamTrack.getonmute"
                              prim__onmute
                              prim__setOnmute
                              v

  export
  onunmute : MediaStreamTrack -> Attribute False Maybe EventHandlerNonNull
  onunmute v = fromNullablePrim "MediaStreamTrack.getonunmute"
                                prim__onunmute
                                prim__setOnunmute
                                v

  export
  readyState : (obj : MediaStreamTrack) -> JSIO MediaStreamTrackState
  readyState a = tryJS "MediaStreamTrack.readyState"
               $ MediaStreamTrack.prim__readyState a

  export
  applyConstraints :  (0 _ : JSType t1)
                   => {auto 0 _ : Elem MediaTrackConstraints (Types t1)}
                   -> (obj : MediaStreamTrack)
                   -> (constraints : Optional t1)
                   -> JSIO (Promise Undefined)
  applyConstraints a b = primJS
                       $ MediaStreamTrack.prim__applyConstraints a (optUp b)

  export
  applyConstraints' : (obj : MediaStreamTrack) -> JSIO (Promise Undefined)
  applyConstraints' a = primJS $ MediaStreamTrack.prim__applyConstraints a undef

  export
  clone : (obj : MediaStreamTrack) -> JSIO MediaStreamTrack
  clone a = primJS $ MediaStreamTrack.prim__clone a

  export
  getCapabilities : (obj : MediaStreamTrack) -> JSIO MediaTrackCapabilities
  getCapabilities a = primJS $ MediaStreamTrack.prim__getCapabilities a

  export
  getConstraints : (obj : MediaStreamTrack) -> JSIO MediaTrackConstraints
  getConstraints a = primJS $ MediaStreamTrack.prim__getConstraints a

  export
  getSettings : (obj : MediaStreamTrack) -> JSIO MediaTrackSettings
  getSettings a = primJS $ MediaStreamTrack.prim__getSettings a

  export
  stop : (obj : MediaStreamTrack) -> JSIO ()
  stop a = primJS $ MediaStreamTrack.prim__stop a

namespace MediaStreamTrackEvent

  export
  new :  (0 _ : JSType t1)
      => {auto 0 _ : Elem MediaStreamTrackEventInit (Types t1)}
      -> (type : String)
      -> (eventInitDict : t1)
      -> JSIO MediaStreamTrackEvent
  new a b = primJS $ MediaStreamTrackEvent.prim__new a (up b)

  export
  track : (obj : MediaStreamTrackEvent) -> JSIO MediaStreamTrack
  track a = primJS $ MediaStreamTrackEvent.prim__track a

namespace OverconstrainedError

  export
  new :  (constraint : String)
      -> (message : Optional String)
      -> JSIO OverconstrainedError
  new a b = primJS $ OverconstrainedError.prim__new a (toFFI b)

  export
  new' : (constraint : String) -> JSIO OverconstrainedError
  new' a = primJS $ OverconstrainedError.prim__new a undef

  export
  constraint : (obj : OverconstrainedError) -> JSIO String
  constraint a = primJS $ OverconstrainedError.prim__constraint a

--------------------------------------------------------------------------------
--          Dictionaries
--------------------------------------------------------------------------------

namespace Capabilities

  export
  new : JSIO Capabilities
  new = primJS $ Capabilities.prim__new

namespace ConstrainBooleanParameters

  export
  new :  (exact : Optional Bool)
      -> (ideal : Optional Bool)
      -> JSIO ConstrainBooleanParameters
  new a b = primJS $ ConstrainBooleanParameters.prim__new (toFFI a) (toFFI b)

  export
  new' : JSIO ConstrainBooleanParameters
  new' = primJS $ ConstrainBooleanParameters.prim__new undef undef

  export
  exact :  (0 _ : JSType t)
        => {auto 0 _ : Elem ConstrainBooleanParameters (Types t)}
        -> t
        -> Attribute False Optional Bool
  exact v = fromUndefOrPrimNoDefault "ConstrainBooleanParameters.getexact"
                                     prim__exact
                                     prim__setExact
                                     (v :> ConstrainBooleanParameters)

  export
  ideal :  (0 _ : JSType t)
        => {auto 0 _ : Elem ConstrainBooleanParameters (Types t)}
        -> t
        -> Attribute False Optional Bool
  ideal v = fromUndefOrPrimNoDefault "ConstrainBooleanParameters.getideal"
                                     prim__ideal
                                     prim__setIdeal
                                     (v :> ConstrainBooleanParameters)

namespace ConstrainDOMStringParameters

  export
  new :  (exact : Optional (NS I [ String , Array String ]))
      -> (ideal : Optional (NS I [ String , Array String ]))
      -> JSIO ConstrainDOMStringParameters
  new a b = primJS $ ConstrainDOMStringParameters.prim__new (toFFI a) (toFFI b)

  export
  new' : JSIO ConstrainDOMStringParameters
  new' = primJS $ ConstrainDOMStringParameters.prim__new undef undef

  export
  exact :  (0 _ : JSType t)
        => {auto 0 _ : Elem ConstrainDOMStringParameters (Types t)}
        -> t
        -> Attribute False Optional (Union2 String (Array String))
  exact v = fromUndefOrPrimNoDefault "ConstrainDOMStringParameters.getexact"
                                     prim__exact
                                     prim__setExact
                                     (v :> ConstrainDOMStringParameters)

  export
  ideal :  (0 _ : JSType t)
        => {auto 0 _ : Elem ConstrainDOMStringParameters (Types t)}
        -> t
        -> Attribute False Optional (Union2 String (Array String))
  ideal v = fromUndefOrPrimNoDefault "ConstrainDOMStringParameters.getideal"
                                     prim__ideal
                                     prim__setIdeal
                                     (v :> ConstrainDOMStringParameters)

namespace ConstrainDoubleRange

  export
  new :  (exact : Optional Double)
      -> (ideal : Optional Double)
      -> JSIO ConstrainDoubleRange
  new a b = primJS $ ConstrainDoubleRange.prim__new (toFFI a) (toFFI b)

  export
  new' : JSIO ConstrainDoubleRange
  new' = primJS $ ConstrainDoubleRange.prim__new undef undef

  export
  exact :  (0 _ : JSType t)
        => {auto 0 _ : Elem ConstrainDoubleRange (Types t)}
        -> t
        -> Attribute False Optional Double
  exact v = fromUndefOrPrimNoDefault "ConstrainDoubleRange.getexact"
                                     prim__exact
                                     prim__setExact
                                     (v :> ConstrainDoubleRange)

  export
  ideal :  (0 _ : JSType t)
        => {auto 0 _ : Elem ConstrainDoubleRange (Types t)}
        -> t
        -> Attribute False Optional Double
  ideal v = fromUndefOrPrimNoDefault "ConstrainDoubleRange.getideal"
                                     prim__ideal
                                     prim__setIdeal
                                     (v :> ConstrainDoubleRange)

namespace ConstrainULongRange

  export
  new :  (exact : Optional Bits32)
      -> (ideal : Optional Bits32)
      -> JSIO ConstrainULongRange
  new a b = primJS $ ConstrainULongRange.prim__new (toFFI a) (toFFI b)

  export
  new' : JSIO ConstrainULongRange
  new' = primJS $ ConstrainULongRange.prim__new undef undef

  export
  exact :  (0 _ : JSType t)
        => {auto 0 _ : Elem ConstrainULongRange (Types t)}
        -> t
        -> Attribute False Optional Bits32
  exact v = fromUndefOrPrimNoDefault "ConstrainULongRange.getexact"
                                     prim__exact
                                     prim__setExact
                                     (v :> ConstrainULongRange)

  export
  ideal :  (0 _ : JSType t)
        => {auto 0 _ : Elem ConstrainULongRange (Types t)}
        -> t
        -> Attribute False Optional Bits32
  ideal v = fromUndefOrPrimNoDefault "ConstrainULongRange.getideal"
                                     prim__ideal
                                     prim__setIdeal
                                     (v :> ConstrainULongRange)

namespace ConstraintSet

  export
  new : JSIO ConstraintSet
  new = primJS $ ConstraintSet.prim__new

namespace Constraints

  export
  new : (advanced : Optional (Array ConstraintSet)) -> JSIO Constraints
  new a = primJS $ Constraints.prim__new (toFFI a)

  export
  new' : JSIO Constraints
  new' = primJS $ Constraints.prim__new undef

  export
  advanced :  (0 _ : JSType t)
           => {auto 0 _ : Elem Constraints (Types t)}
           -> t
           -> Attribute False Optional (Array ConstraintSet)
  advanced v = fromUndefOrPrimNoDefault "Constraints.getadvanced"
                                        prim__advanced
                                        prim__setAdvanced
                                        (v :> Constraints)

namespace DoubleRange

  export
  new : (max : Optional Double) -> (min : Optional Double) -> JSIO DoubleRange
  new a b = primJS $ DoubleRange.prim__new (toFFI a) (toFFI b)

  export
  new' : JSIO DoubleRange
  new' = primJS $ DoubleRange.prim__new undef undef

  export
  max :  (0 _ : JSType t)
      => {auto 0 _ : Elem DoubleRange (Types t)}
      -> t
      -> Attribute False Optional Double
  max v = fromUndefOrPrimNoDefault "DoubleRange.getmax"
                                   prim__max
                                   prim__setMax
                                   (v :> DoubleRange)

  export
  min :  (0 _ : JSType t)
      => {auto 0 _ : Elem DoubleRange (Types t)}
      -> t
      -> Attribute False Optional Double
  min v = fromUndefOrPrimNoDefault "DoubleRange.getmin"
                                   prim__min
                                   prim__setMin
                                   (v :> DoubleRange)

namespace MediaStreamConstraints

  export
  new :  (video : Optional (NS I [ Bool , MediaTrackConstraints ]))
      -> (audio : Optional (NS I [ Bool , MediaTrackConstraints ]))
      -> JSIO MediaStreamConstraints
  new a b = primJS $ MediaStreamConstraints.prim__new (toFFI a) (toFFI b)

  export
  new' : JSIO MediaStreamConstraints
  new' = primJS $ MediaStreamConstraints.prim__new undef undef

  export
  audio :  (0 _ : JSType t)
        => {auto 0 _ : Elem MediaStreamConstraints (Types t)}
        -> t
        -> Attribute False Optional (Union2 Boolean MediaTrackConstraints)
  audio v = fromUndefOrPrimNoDefault "MediaStreamConstraints.getaudio"
                                     prim__audio
                                     prim__setAudio
                                     (v :> MediaStreamConstraints)

  export
  video :  (0 _ : JSType t)
        => {auto 0 _ : Elem MediaStreamConstraints (Types t)}
        -> t
        -> Attribute False Optional (Union2 Boolean MediaTrackConstraints)
  video v = fromUndefOrPrimNoDefault "MediaStreamConstraints.getvideo"
                                     prim__video
                                     prim__setVideo
                                     (v :> MediaStreamConstraints)

namespace MediaStreamTrackEventInit

  export
  new : (track : MediaStreamTrack) -> JSIO MediaStreamTrackEventInit
  new a = primJS $ MediaStreamTrackEventInit.prim__new a

  export
  track :  (0 _ : JSType t)
        => {auto 0 _ : Elem MediaStreamTrackEventInit (Types t)}
        -> t
        -> Attribute True I MediaStreamTrack
  track v = fromPrim "MediaStreamTrackEventInit.gettrack"
                     prim__track
                     prim__setTrack
                     (v :> MediaStreamTrackEventInit)

namespace MediaTrackCapabilities

  export
  new :  (0 _ : JSType t1)
      => (0 _ : JSType t2)
      => (0 _ : JSType t3)
      => (0 _ : JSType t4)
      => (0 _ : JSType t5)
      => (0 _ : JSType t6)
      => (0 _ : JSType t7)
      => (0 _ : JSType t8)
      => {auto 0 _ : Elem ULongRange (Types t1)}
      -> {auto 0 _ : Elem ULongRange (Types t2)}
      -> {auto 0 _ : Elem DoubleRange (Types t3)}
      -> {auto 0 _ : Elem DoubleRange (Types t4)}
      -> {auto 0 _ : Elem ULongRange (Types t5)}
      -> {auto 0 _ : Elem ULongRange (Types t6)}
      -> {auto 0 _ : Elem DoubleRange (Types t7)}
      -> {auto 0 _ : Elem ULongRange (Types t8)}
      -> (width : Optional t1)
      -> (height : Optional t2)
      -> (aspectRatio : Optional t3)
      -> (frameRate : Optional t4)
      -> (facingMode : Optional (Array String))
      -> (resizeMode : Optional (Array String))
      -> (sampleRate : Optional t5)
      -> (sampleSize : Optional t6)
      -> (echoCancellation : Optional (Array Boolean))
      -> (autoGainControl : Optional (Array Boolean))
      -> (noiseSuppression : Optional (Array Boolean))
      -> (latency : Optional t7)
      -> (channelCount : Optional t8)
      -> (deviceId : Optional String)
      -> (groupId : Optional String)
      -> JSIO MediaTrackCapabilities
  new a b c d e f g h i j k l m n o = primJS
                                    $ MediaTrackCapabilities.prim__new (optUp a)
                                                                       (optUp b)
                                                                       (optUp c)
                                                                       (optUp d)
                                                                       (toFFI e)
                                                                       (toFFI f)
                                                                       (optUp g)
                                                                       (optUp h)
                                                                       (toFFI i)
                                                                       (toFFI j)
                                                                       (toFFI k)
                                                                       (optUp l)
                                                                       (optUp m)
                                                                       (toFFI n)
                                                                       (toFFI o)

  export
  new' : JSIO MediaTrackCapabilities
  new' = primJS
       $ MediaTrackCapabilities.prim__new undef
                                          undef
                                          undef
                                          undef
                                          undef
                                          undef
                                          undef
                                          undef
                                          undef
                                          undef
                                          undef
                                          undef
                                          undef
                                          undef
                                          undef

  export
  aspectRatio :  (0 _ : JSType t)
              => {auto 0 _ : Elem MediaTrackCapabilities (Types t)}
              -> t
              -> Attribute False Optional DoubleRange
  aspectRatio v = fromUndefOrPrimNoDefault "MediaTrackCapabilities.getaspectRatio"
                                           prim__aspectRatio
                                           prim__setAspectRatio
                                           (v :> MediaTrackCapabilities)

  export
  autoGainControl :  (0 _ : JSType t)
                  => {auto 0 _ : Elem MediaTrackCapabilities (Types t)}
                  -> t
                  -> Attribute False Optional (Array Boolean)
  autoGainControl v = fromUndefOrPrimNoDefault "MediaTrackCapabilities.getautoGainControl"
                                               prim__autoGainControl
                                               prim__setAutoGainControl
                                               (v :> MediaTrackCapabilities)

  export
  channelCount :  (0 _ : JSType t)
               => {auto 0 _ : Elem MediaTrackCapabilities (Types t)}
               -> t
               -> Attribute False Optional ULongRange
  channelCount v = fromUndefOrPrimNoDefault "MediaTrackCapabilities.getchannelCount"
                                            prim__channelCount
                                            prim__setChannelCount
                                            (v :> MediaTrackCapabilities)

  export
  deviceId :  (0 _ : JSType t)
           => {auto 0 _ : Elem MediaTrackCapabilities (Types t)}
           -> t
           -> Attribute False Optional String
  deviceId v = fromUndefOrPrimNoDefault "MediaTrackCapabilities.getdeviceId"
                                        prim__deviceId
                                        prim__setDeviceId
                                        (v :> MediaTrackCapabilities)

  export
  echoCancellation :  (0 _ : JSType t)
                   => {auto 0 _ : Elem MediaTrackCapabilities (Types t)}
                   -> t
                   -> Attribute False Optional (Array Boolean)
  echoCancellation v = fromUndefOrPrimNoDefault "MediaTrackCapabilities.getechoCancellation"
                                                prim__echoCancellation
                                                prim__setEchoCancellation
                                                (v :> MediaTrackCapabilities)

  export
  facingMode :  (0 _ : JSType t)
             => {auto 0 _ : Elem MediaTrackCapabilities (Types t)}
             -> t
             -> Attribute False Optional (Array String)
  facingMode v = fromUndefOrPrimNoDefault "MediaTrackCapabilities.getfacingMode"
                                          prim__facingMode
                                          prim__setFacingMode
                                          (v :> MediaTrackCapabilities)

  export
  frameRate :  (0 _ : JSType t)
            => {auto 0 _ : Elem MediaTrackCapabilities (Types t)}
            -> t
            -> Attribute False Optional DoubleRange
  frameRate v = fromUndefOrPrimNoDefault "MediaTrackCapabilities.getframeRate"
                                         prim__frameRate
                                         prim__setFrameRate
                                         (v :> MediaTrackCapabilities)

  export
  groupId :  (0 _ : JSType t)
          => {auto 0 _ : Elem MediaTrackCapabilities (Types t)}
          -> t
          -> Attribute False Optional String
  groupId v = fromUndefOrPrimNoDefault "MediaTrackCapabilities.getgroupId"
                                       prim__groupId
                                       prim__setGroupId
                                       (v :> MediaTrackCapabilities)

  export
  height :  (0 _ : JSType t)
         => {auto 0 _ : Elem MediaTrackCapabilities (Types t)}
         -> t
         -> Attribute False Optional ULongRange
  height v = fromUndefOrPrimNoDefault "MediaTrackCapabilities.getheight"
                                      prim__height
                                      prim__setHeight
                                      (v :> MediaTrackCapabilities)

  export
  latency :  (0 _ : JSType t)
          => {auto 0 _ : Elem MediaTrackCapabilities (Types t)}
          -> t
          -> Attribute False Optional DoubleRange
  latency v = fromUndefOrPrimNoDefault "MediaTrackCapabilities.getlatency"
                                       prim__latency
                                       prim__setLatency
                                       (v :> MediaTrackCapabilities)

  export
  noiseSuppression :  (0 _ : JSType t)
                   => {auto 0 _ : Elem MediaTrackCapabilities (Types t)}
                   -> t
                   -> Attribute False Optional (Array Boolean)
  noiseSuppression v = fromUndefOrPrimNoDefault "MediaTrackCapabilities.getnoiseSuppression"
                                                prim__noiseSuppression
                                                prim__setNoiseSuppression
                                                (v :> MediaTrackCapabilities)

  export
  resizeMode :  (0 _ : JSType t)
             => {auto 0 _ : Elem MediaTrackCapabilities (Types t)}
             -> t
             -> Attribute False Optional (Array String)
  resizeMode v = fromUndefOrPrimNoDefault "MediaTrackCapabilities.getresizeMode"
                                          prim__resizeMode
                                          prim__setResizeMode
                                          (v :> MediaTrackCapabilities)

  export
  sampleRate :  (0 _ : JSType t)
             => {auto 0 _ : Elem MediaTrackCapabilities (Types t)}
             -> t
             -> Attribute False Optional ULongRange
  sampleRate v = fromUndefOrPrimNoDefault "MediaTrackCapabilities.getsampleRate"
                                          prim__sampleRate
                                          prim__setSampleRate
                                          (v :> MediaTrackCapabilities)

  export
  sampleSize :  (0 _ : JSType t)
             => {auto 0 _ : Elem MediaTrackCapabilities (Types t)}
             -> t
             -> Attribute False Optional ULongRange
  sampleSize v = fromUndefOrPrimNoDefault "MediaTrackCapabilities.getsampleSize"
                                          prim__sampleSize
                                          prim__setSampleSize
                                          (v :> MediaTrackCapabilities)

  export
  width :  (0 _ : JSType t)
        => {auto 0 _ : Elem MediaTrackCapabilities (Types t)}
        -> t
        -> Attribute False Optional ULongRange
  width v = fromUndefOrPrimNoDefault "MediaTrackCapabilities.getwidth"
                                     prim__width
                                     prim__setWidth
                                     (v :> MediaTrackCapabilities)

namespace MediaTrackConstraintSet

  export
  new :  (width : Optional (NS I [ Bits32 , ConstrainULongRange ]))
      -> (height : Optional (NS I [ Bits32 , ConstrainULongRange ]))
      -> (aspectRatio : Optional (NS I [ Double , ConstrainDoubleRange ]))
      -> (frameRate : Optional (NS I [ Double , ConstrainDoubleRange ]))
      -> (facingMode : Optional (NS I [ String
                                      , Array String
                                      , ConstrainDOMStringParameters
                                      ]))
      -> (resizeMode : Optional (NS I [ String
                                      , Array String
                                      , ConstrainDOMStringParameters
                                      ]))
      -> (sampleRate : Optional (NS I [ Bits32 , ConstrainULongRange ]))
      -> (sampleSize : Optional (NS I [ Bits32 , ConstrainULongRange ]))
      -> (echoCancellation : Optional (NS I [ Bool
                                            , ConstrainBooleanParameters
                                            ]))
      -> (autoGainControl : Optional (NS I [ Bool
                                           , ConstrainBooleanParameters
                                           ]))
      -> (noiseSuppression : Optional (NS I [ Bool
                                            , ConstrainBooleanParameters
                                            ]))
      -> (latency : Optional (NS I [ Double , ConstrainDoubleRange ]))
      -> (channelCount : Optional (NS I [ Bits32 , ConstrainULongRange ]))
      -> (deviceId : Optional (NS I [ String
                                    , Array String
                                    , ConstrainDOMStringParameters
                                    ]))
      -> (groupId : Optional (NS I [ String
                                   , Array String
                                   , ConstrainDOMStringParameters
                                   ]))
      -> JSIO MediaTrackConstraintSet
  new a b c d e f g h i j k l m n o = primJS
                                    $ MediaTrackConstraintSet.prim__new (toFFI a)
                                                                        (toFFI b)
                                                                        (toFFI c)
                                                                        (toFFI d)
                                                                        (toFFI e)
                                                                        (toFFI f)
                                                                        (toFFI g)
                                                                        (toFFI h)
                                                                        (toFFI i)
                                                                        (toFFI j)
                                                                        (toFFI k)
                                                                        (toFFI l)
                                                                        (toFFI m)
                                                                        (toFFI n)
                                                                        (toFFI o)

  export
  new' : JSIO MediaTrackConstraintSet
  new' = primJS
       $ MediaTrackConstraintSet.prim__new undef
                                           undef
                                           undef
                                           undef
                                           undef
                                           undef
                                           undef
                                           undef
                                           undef
                                           undef
                                           undef
                                           undef
                                           undef
                                           undef
                                           undef

  export
  aspectRatio :  (0 _ : JSType t)
              => {auto 0 _ : Elem MediaTrackConstraintSet (Types t)}
              -> t
              -> Attribute False Optional (Union2 Double ConstrainDoubleRange)
  aspectRatio v = fromUndefOrPrimNoDefault "MediaTrackConstraintSet.getaspectRatio"
                                           prim__aspectRatio
                                           prim__setAspectRatio
                                           (v :> MediaTrackConstraintSet)

  export
  autoGainControl :  (0 _ : JSType t)
                  => {auto 0 _ : Elem MediaTrackConstraintSet (Types t)}
                  -> t
                  -> Attribute False Optional (Union2 Boolean
                                                      ConstrainBooleanParameters)
  autoGainControl v = fromUndefOrPrimNoDefault "MediaTrackConstraintSet.getautoGainControl"
                                               prim__autoGainControl
                                               prim__setAutoGainControl
                                               (v :> MediaTrackConstraintSet)

  export
  channelCount :  (0 _ : JSType t)
               => {auto 0 _ : Elem MediaTrackConstraintSet (Types t)}
               -> t
               -> Attribute False Optional (Union2 Bits32 ConstrainULongRange)
  channelCount v = fromUndefOrPrimNoDefault "MediaTrackConstraintSet.getchannelCount"
                                            prim__channelCount
                                            prim__setChannelCount
                                            (v :> MediaTrackConstraintSet)

  export
  deviceId :  (0 _ : JSType t)
           => {auto 0 _ : Elem MediaTrackConstraintSet (Types t)}
           -> t
           -> Attribute False Optional (Union3 String
                                               (Array String)
                                               ConstrainDOMStringParameters)
  deviceId v = fromUndefOrPrimNoDefault "MediaTrackConstraintSet.getdeviceId"
                                        prim__deviceId
                                        prim__setDeviceId
                                        (v :> MediaTrackConstraintSet)

  export
  echoCancellation :  (0 _ : JSType t)
                   => {auto 0 _ : Elem MediaTrackConstraintSet (Types t)}
                   -> t
                   -> Attribute False Optional (Union2 Boolean
                                                       ConstrainBooleanParameters)
  echoCancellation v = fromUndefOrPrimNoDefault "MediaTrackConstraintSet.getechoCancellation"
                                                prim__echoCancellation
                                                prim__setEchoCancellation
                                                (v :> MediaTrackConstraintSet)

  export
  facingMode :  (0 _ : JSType t)
             => {auto 0 _ : Elem MediaTrackConstraintSet (Types t)}
             -> t
             -> Attribute False Optional (Union3 String
                                                 (Array String)
                                                 ConstrainDOMStringParameters)
  facingMode v = fromUndefOrPrimNoDefault "MediaTrackConstraintSet.getfacingMode"
                                          prim__facingMode
                                          prim__setFacingMode
                                          (v :> MediaTrackConstraintSet)

  export
  frameRate :  (0 _ : JSType t)
            => {auto 0 _ : Elem MediaTrackConstraintSet (Types t)}
            -> t
            -> Attribute False Optional (Union2 Double ConstrainDoubleRange)
  frameRate v = fromUndefOrPrimNoDefault "MediaTrackConstraintSet.getframeRate"
                                         prim__frameRate
                                         prim__setFrameRate
                                         (v :> MediaTrackConstraintSet)

  export
  groupId :  (0 _ : JSType t)
          => {auto 0 _ : Elem MediaTrackConstraintSet (Types t)}
          -> t
          -> Attribute False Optional (Union3 String
                                              (Array String)
                                              ConstrainDOMStringParameters)
  groupId v = fromUndefOrPrimNoDefault "MediaTrackConstraintSet.getgroupId"
                                       prim__groupId
                                       prim__setGroupId
                                       (v :> MediaTrackConstraintSet)

  export
  height :  (0 _ : JSType t)
         => {auto 0 _ : Elem MediaTrackConstraintSet (Types t)}
         -> t
         -> Attribute False Optional (Union2 Bits32 ConstrainULongRange)
  height v = fromUndefOrPrimNoDefault "MediaTrackConstraintSet.getheight"
                                      prim__height
                                      prim__setHeight
                                      (v :> MediaTrackConstraintSet)

  export
  latency :  (0 _ : JSType t)
          => {auto 0 _ : Elem MediaTrackConstraintSet (Types t)}
          -> t
          -> Attribute False Optional (Union2 Double ConstrainDoubleRange)
  latency v = fromUndefOrPrimNoDefault "MediaTrackConstraintSet.getlatency"
                                       prim__latency
                                       prim__setLatency
                                       (v :> MediaTrackConstraintSet)

  export
  noiseSuppression :  (0 _ : JSType t)
                   => {auto 0 _ : Elem MediaTrackConstraintSet (Types t)}
                   -> t
                   -> Attribute False Optional (Union2 Boolean
                                                       ConstrainBooleanParameters)
  noiseSuppression v = fromUndefOrPrimNoDefault "MediaTrackConstraintSet.getnoiseSuppression"
                                                prim__noiseSuppression
                                                prim__setNoiseSuppression
                                                (v :> MediaTrackConstraintSet)

  export
  resizeMode :  (0 _ : JSType t)
             => {auto 0 _ : Elem MediaTrackConstraintSet (Types t)}
             -> t
             -> Attribute False Optional (Union3 String
                                                 (Array String)
                                                 ConstrainDOMStringParameters)
  resizeMode v = fromUndefOrPrimNoDefault "MediaTrackConstraintSet.getresizeMode"
                                          prim__resizeMode
                                          prim__setResizeMode
                                          (v :> MediaTrackConstraintSet)

  export
  sampleRate :  (0 _ : JSType t)
             => {auto 0 _ : Elem MediaTrackConstraintSet (Types t)}
             -> t
             -> Attribute False Optional (Union2 Bits32 ConstrainULongRange)
  sampleRate v = fromUndefOrPrimNoDefault "MediaTrackConstraintSet.getsampleRate"
                                          prim__sampleRate
                                          prim__setSampleRate
                                          (v :> MediaTrackConstraintSet)

  export
  sampleSize :  (0 _ : JSType t)
             => {auto 0 _ : Elem MediaTrackConstraintSet (Types t)}
             -> t
             -> Attribute False Optional (Union2 Bits32 ConstrainULongRange)
  sampleSize v = fromUndefOrPrimNoDefault "MediaTrackConstraintSet.getsampleSize"
                                          prim__sampleSize
                                          prim__setSampleSize
                                          (v :> MediaTrackConstraintSet)

  export
  width :  (0 _ : JSType t)
        => {auto 0 _ : Elem MediaTrackConstraintSet (Types t)}
        -> t
        -> Attribute False Optional (Union2 Bits32 ConstrainULongRange)
  width v = fromUndefOrPrimNoDefault "MediaTrackConstraintSet.getwidth"
                                     prim__width
                                     prim__setWidth
                                     (v :> MediaTrackConstraintSet)

namespace MediaTrackConstraints

  export
  new :  (advanced : Optional (Array MediaTrackConstraintSet))
      -> JSIO MediaTrackConstraints
  new a = primJS $ MediaTrackConstraints.prim__new (toFFI a)

  export
  new' : JSIO MediaTrackConstraints
  new' = primJS $ MediaTrackConstraints.prim__new undef

  export
  advanced :  (0 _ : JSType t)
           => {auto 0 _ : Elem MediaTrackConstraints (Types t)}
           -> t
           -> Attribute False Optional (Array MediaTrackConstraintSet)
  advanced v = fromUndefOrPrimNoDefault "MediaTrackConstraints.getadvanced"
                                        prim__advanced
                                        prim__setAdvanced
                                        (v :> MediaTrackConstraints)

namespace MediaTrackSettings

  export
  new :  (width : Optional Int32)
      -> (height : Optional Int32)
      -> (aspectRatio : Optional Double)
      -> (frameRate : Optional Double)
      -> (facingMode : Optional String)
      -> (resizeMode : Optional String)
      -> (sampleRate : Optional Int32)
      -> (sampleSize : Optional Int32)
      -> (echoCancellation : Optional Bool)
      -> (autoGainControl : Optional Bool)
      -> (noiseSuppression : Optional Bool)
      -> (latency : Optional Double)
      -> (channelCount : Optional Int32)
      -> (deviceId : Optional String)
      -> (groupId : Optional String)
      -> JSIO MediaTrackSettings
  new a b c d e f g h i j k l m n o = primJS
                                    $ MediaTrackSettings.prim__new (toFFI a)
                                                                   (toFFI b)
                                                                   (toFFI c)
                                                                   (toFFI d)
                                                                   (toFFI e)
                                                                   (toFFI f)
                                                                   (toFFI g)
                                                                   (toFFI h)
                                                                   (toFFI i)
                                                                   (toFFI j)
                                                                   (toFFI k)
                                                                   (toFFI l)
                                                                   (toFFI m)
                                                                   (toFFI n)
                                                                   (toFFI o)

  export
  new' : JSIO MediaTrackSettings
  new' = primJS
       $ MediaTrackSettings.prim__new undef
                                      undef
                                      undef
                                      undef
                                      undef
                                      undef
                                      undef
                                      undef
                                      undef
                                      undef
                                      undef
                                      undef
                                      undef
                                      undef
                                      undef

  export
  aspectRatio :  (0 _ : JSType t)
              => {auto 0 _ : Elem MediaTrackSettings (Types t)}
              -> t
              -> Attribute False Optional Double
  aspectRatio v = fromUndefOrPrimNoDefault "MediaTrackSettings.getaspectRatio"
                                           prim__aspectRatio
                                           prim__setAspectRatio
                                           (v :> MediaTrackSettings)

  export
  autoGainControl :  (0 _ : JSType t)
                  => {auto 0 _ : Elem MediaTrackSettings (Types t)}
                  -> t
                  -> Attribute False Optional Bool
  autoGainControl v = fromUndefOrPrimNoDefault "MediaTrackSettings.getautoGainControl"
                                               prim__autoGainControl
                                               prim__setAutoGainControl
                                               (v :> MediaTrackSettings)

  export
  channelCount :  (0 _ : JSType t)
               => {auto 0 _ : Elem MediaTrackSettings (Types t)}
               -> t
               -> Attribute False Optional Int32
  channelCount v = fromUndefOrPrimNoDefault "MediaTrackSettings.getchannelCount"
                                            prim__channelCount
                                            prim__setChannelCount
                                            (v :> MediaTrackSettings)

  export
  deviceId :  (0 _ : JSType t)
           => {auto 0 _ : Elem MediaTrackSettings (Types t)}
           -> t
           -> Attribute False Optional String
  deviceId v = fromUndefOrPrimNoDefault "MediaTrackSettings.getdeviceId"
                                        prim__deviceId
                                        prim__setDeviceId
                                        (v :> MediaTrackSettings)

  export
  echoCancellation :  (0 _ : JSType t)
                   => {auto 0 _ : Elem MediaTrackSettings (Types t)}
                   -> t
                   -> Attribute False Optional Bool
  echoCancellation v = fromUndefOrPrimNoDefault "MediaTrackSettings.getechoCancellation"
                                                prim__echoCancellation
                                                prim__setEchoCancellation
                                                (v :> MediaTrackSettings)

  export
  facingMode :  (0 _ : JSType t)
             => {auto 0 _ : Elem MediaTrackSettings (Types t)}
             -> t
             -> Attribute False Optional String
  facingMode v = fromUndefOrPrimNoDefault "MediaTrackSettings.getfacingMode"
                                          prim__facingMode
                                          prim__setFacingMode
                                          (v :> MediaTrackSettings)

  export
  frameRate :  (0 _ : JSType t)
            => {auto 0 _ : Elem MediaTrackSettings (Types t)}
            -> t
            -> Attribute False Optional Double
  frameRate v = fromUndefOrPrimNoDefault "MediaTrackSettings.getframeRate"
                                         prim__frameRate
                                         prim__setFrameRate
                                         (v :> MediaTrackSettings)

  export
  groupId :  (0 _ : JSType t)
          => {auto 0 _ : Elem MediaTrackSettings (Types t)}
          -> t
          -> Attribute False Optional String
  groupId v = fromUndefOrPrimNoDefault "MediaTrackSettings.getgroupId"
                                       prim__groupId
                                       prim__setGroupId
                                       (v :> MediaTrackSettings)

  export
  height :  (0 _ : JSType t)
         => {auto 0 _ : Elem MediaTrackSettings (Types t)}
         -> t
         -> Attribute False Optional Int32
  height v = fromUndefOrPrimNoDefault "MediaTrackSettings.getheight"
                                      prim__height
                                      prim__setHeight
                                      (v :> MediaTrackSettings)

  export
  latency :  (0 _ : JSType t)
          => {auto 0 _ : Elem MediaTrackSettings (Types t)}
          -> t
          -> Attribute False Optional Double
  latency v = fromUndefOrPrimNoDefault "MediaTrackSettings.getlatency"
                                       prim__latency
                                       prim__setLatency
                                       (v :> MediaTrackSettings)

  export
  noiseSuppression :  (0 _ : JSType t)
                   => {auto 0 _ : Elem MediaTrackSettings (Types t)}
                   -> t
                   -> Attribute False Optional Bool
  noiseSuppression v = fromUndefOrPrimNoDefault "MediaTrackSettings.getnoiseSuppression"
                                                prim__noiseSuppression
                                                prim__setNoiseSuppression
                                                (v :> MediaTrackSettings)

  export
  resizeMode :  (0 _ : JSType t)
             => {auto 0 _ : Elem MediaTrackSettings (Types t)}
             -> t
             -> Attribute False Optional String
  resizeMode v = fromUndefOrPrimNoDefault "MediaTrackSettings.getresizeMode"
                                          prim__resizeMode
                                          prim__setResizeMode
                                          (v :> MediaTrackSettings)

  export
  sampleRate :  (0 _ : JSType t)
             => {auto 0 _ : Elem MediaTrackSettings (Types t)}
             -> t
             -> Attribute False Optional Int32
  sampleRate v = fromUndefOrPrimNoDefault "MediaTrackSettings.getsampleRate"
                                          prim__sampleRate
                                          prim__setSampleRate
                                          (v :> MediaTrackSettings)

  export
  sampleSize :  (0 _ : JSType t)
             => {auto 0 _ : Elem MediaTrackSettings (Types t)}
             -> t
             -> Attribute False Optional Int32
  sampleSize v = fromUndefOrPrimNoDefault "MediaTrackSettings.getsampleSize"
                                          prim__sampleSize
                                          prim__setSampleSize
                                          (v :> MediaTrackSettings)

  export
  width :  (0 _ : JSType t)
        => {auto 0 _ : Elem MediaTrackSettings (Types t)}
        -> t
        -> Attribute False Optional Int32
  width v = fromUndefOrPrimNoDefault "MediaTrackSettings.getwidth"
                                     prim__width
                                     prim__setWidth
                                     (v :> MediaTrackSettings)

namespace MediaTrackSupportedConstraints

  export
  new :  (width : Optional Bool)
      -> (height : Optional Bool)
      -> (aspectRatio : Optional Bool)
      -> (frameRate : Optional Bool)
      -> (facingMode : Optional Bool)
      -> (resizeMode : Optional Bool)
      -> (sampleRate : Optional Bool)
      -> (sampleSize : Optional Bool)
      -> (echoCancellation : Optional Bool)
      -> (autoGainControl : Optional Bool)
      -> (noiseSuppression : Optional Bool)
      -> (latency : Optional Bool)
      -> (channelCount : Optional Bool)
      -> (deviceId : Optional Bool)
      -> (groupId : Optional Bool)
      -> JSIO MediaTrackSupportedConstraints
  new a b c d e f g h i j k l m n o = primJS
                                    $ MediaTrackSupportedConstraints.prim__new (toFFI a)
                                                                               (toFFI b)
                                                                               (toFFI c)
                                                                               (toFFI d)
                                                                               (toFFI e)
                                                                               (toFFI f)
                                                                               (toFFI g)
                                                                               (toFFI h)
                                                                               (toFFI i)
                                                                               (toFFI j)
                                                                               (toFFI k)
                                                                               (toFFI l)
                                                                               (toFFI m)
                                                                               (toFFI n)
                                                                               (toFFI o)

  export
  new' : JSIO MediaTrackSupportedConstraints
  new' = primJS
       $ MediaTrackSupportedConstraints.prim__new undef
                                                  undef
                                                  undef
                                                  undef
                                                  undef
                                                  undef
                                                  undef
                                                  undef
                                                  undef
                                                  undef
                                                  undef
                                                  undef
                                                  undef
                                                  undef
                                                  undef

  export
  aspectRatio :  (0 _ : JSType t)
              => {auto 0 _ : Elem MediaTrackSupportedConstraints (Types t)}
              -> t
              -> Attribute True Optional Bool
  aspectRatio v = fromUndefOrPrim "MediaTrackSupportedConstraints.getaspectRatio"
                                  prim__aspectRatio
                                  prim__setAspectRatio
                                  True
                                  (v :> MediaTrackSupportedConstraints)

  export
  autoGainControl :  (0 _ : JSType t)
                  => {auto 0 _ : Elem MediaTrackSupportedConstraints (Types t)}
                  -> t
                  -> Attribute True Optional Bool
  autoGainControl v = fromUndefOrPrim "MediaTrackSupportedConstraints.getautoGainControl"
                                      prim__autoGainControl
                                      prim__setAutoGainControl
                                      True
                                      (v :> MediaTrackSupportedConstraints)

  export
  channelCount :  (0 _ : JSType t)
               => {auto 0 _ : Elem MediaTrackSupportedConstraints (Types t)}
               -> t
               -> Attribute True Optional Bool
  channelCount v = fromUndefOrPrim "MediaTrackSupportedConstraints.getchannelCount"
                                   prim__channelCount
                                   prim__setChannelCount
                                   True
                                   (v :> MediaTrackSupportedConstraints)

  export
  deviceId :  (0 _ : JSType t)
           => {auto 0 _ : Elem MediaTrackSupportedConstraints (Types t)}
           -> t
           -> Attribute True Optional Bool
  deviceId v = fromUndefOrPrim "MediaTrackSupportedConstraints.getdeviceId"
                               prim__deviceId
                               prim__setDeviceId
                               True
                               (v :> MediaTrackSupportedConstraints)

  export
  echoCancellation :  (0 _ : JSType t)
                   => {auto 0 _ : Elem MediaTrackSupportedConstraints (Types t)}
                   -> t
                   -> Attribute True Optional Bool
  echoCancellation v = fromUndefOrPrim "MediaTrackSupportedConstraints.getechoCancellation"
                                       prim__echoCancellation
                                       prim__setEchoCancellation
                                       True
                                       (v :> MediaTrackSupportedConstraints)

  export
  facingMode :  (0 _ : JSType t)
             => {auto 0 _ : Elem MediaTrackSupportedConstraints (Types t)}
             -> t
             -> Attribute True Optional Bool
  facingMode v = fromUndefOrPrim "MediaTrackSupportedConstraints.getfacingMode"
                                 prim__facingMode
                                 prim__setFacingMode
                                 True
                                 (v :> MediaTrackSupportedConstraints)

  export
  frameRate :  (0 _ : JSType t)
            => {auto 0 _ : Elem MediaTrackSupportedConstraints (Types t)}
            -> t
            -> Attribute True Optional Bool
  frameRate v = fromUndefOrPrim "MediaTrackSupportedConstraints.getframeRate"
                                prim__frameRate
                                prim__setFrameRate
                                True
                                (v :> MediaTrackSupportedConstraints)

  export
  groupId :  (0 _ : JSType t)
          => {auto 0 _ : Elem MediaTrackSupportedConstraints (Types t)}
          -> t
          -> Attribute True Optional Bool
  groupId v = fromUndefOrPrim "MediaTrackSupportedConstraints.getgroupId"
                              prim__groupId
                              prim__setGroupId
                              True
                              (v :> MediaTrackSupportedConstraints)

  export
  height :  (0 _ : JSType t)
         => {auto 0 _ : Elem MediaTrackSupportedConstraints (Types t)}
         -> t
         -> Attribute True Optional Bool
  height v = fromUndefOrPrim "MediaTrackSupportedConstraints.getheight"
                             prim__height
                             prim__setHeight
                             True
                             (v :> MediaTrackSupportedConstraints)

  export
  latency :  (0 _ : JSType t)
          => {auto 0 _ : Elem MediaTrackSupportedConstraints (Types t)}
          -> t
          -> Attribute True Optional Bool
  latency v = fromUndefOrPrim "MediaTrackSupportedConstraints.getlatency"
                              prim__latency
                              prim__setLatency
                              True
                              (v :> MediaTrackSupportedConstraints)

  export
  noiseSuppression :  (0 _ : JSType t)
                   => {auto 0 _ : Elem MediaTrackSupportedConstraints (Types t)}
                   -> t
                   -> Attribute True Optional Bool
  noiseSuppression v = fromUndefOrPrim "MediaTrackSupportedConstraints.getnoiseSuppression"
                                       prim__noiseSuppression
                                       prim__setNoiseSuppression
                                       True
                                       (v :> MediaTrackSupportedConstraints)

  export
  resizeMode :  (0 _ : JSType t)
             => {auto 0 _ : Elem MediaTrackSupportedConstraints (Types t)}
             -> t
             -> Attribute True Optional Bool
  resizeMode v = fromUndefOrPrim "MediaTrackSupportedConstraints.getresizeMode"
                                 prim__resizeMode
                                 prim__setResizeMode
                                 True
                                 (v :> MediaTrackSupportedConstraints)

  export
  sampleRate :  (0 _ : JSType t)
             => {auto 0 _ : Elem MediaTrackSupportedConstraints (Types t)}
             -> t
             -> Attribute True Optional Bool
  sampleRate v = fromUndefOrPrim "MediaTrackSupportedConstraints.getsampleRate"
                                 prim__sampleRate
                                 prim__setSampleRate
                                 True
                                 (v :> MediaTrackSupportedConstraints)

  export
  sampleSize :  (0 _ : JSType t)
             => {auto 0 _ : Elem MediaTrackSupportedConstraints (Types t)}
             -> t
             -> Attribute True Optional Bool
  sampleSize v = fromUndefOrPrim "MediaTrackSupportedConstraints.getsampleSize"
                                 prim__sampleSize
                                 prim__setSampleSize
                                 True
                                 (v :> MediaTrackSupportedConstraints)

  export
  width :  (0 _ : JSType t)
        => {auto 0 _ : Elem MediaTrackSupportedConstraints (Types t)}
        -> t
        -> Attribute True Optional Bool
  width v = fromUndefOrPrim "MediaTrackSupportedConstraints.getwidth"
                            prim__width
                            prim__setWidth
                            True
                            (v :> MediaTrackSupportedConstraints)

namespace Settings

  export
  new : JSIO Settings
  new = primJS $ Settings.prim__new

namespace ULongRange

  export
  new : (max : Optional Bits32) -> (min : Optional Bits32) -> JSIO ULongRange
  new a b = primJS $ ULongRange.prim__new (toFFI a) (toFFI b)

  export
  new' : JSIO ULongRange
  new' = primJS $ ULongRange.prim__new undef undef

  export
  max :  (0 _ : JSType t)
      => {auto 0 _ : Elem ULongRange (Types t)}
      -> t
      -> Attribute False Optional Bits32
  max v = fromUndefOrPrimNoDefault "ULongRange.getmax"
                                   prim__max
                                   prim__setMax
                                   (v :> ULongRange)

  export
  min :  (0 _ : JSType t)
      => {auto 0 _ : Elem ULongRange (Types t)}
      -> t
      -> Attribute False Optional Bits32
  min v = fromUndefOrPrimNoDefault "ULongRange.getmin"
                                   prim__min
                                   prim__setMin
                                   (v :> ULongRange)

--------------------------------------------------------------------------------
--          Callbacks
--------------------------------------------------------------------------------

namespace NavigatorUserMediaErrorCallback

  export
  toNavigatorUserMediaErrorCallback :  ( DOMException -> IO () )
                                    -> JSIO NavigatorUserMediaErrorCallback
  toNavigatorUserMediaErrorCallback cb = primJS $ prim__toNavigatorUserMediaErrorCallback cb

namespace NavigatorUserMediaSuccessCallback

  export
  toNavigatorUserMediaSuccessCallback :  ( MediaStream -> IO () )
                                      -> JSIO NavigatorUserMediaSuccessCallback
  toNavigatorUserMediaSuccessCallback cb = primJS $ prim__toNavigatorUserMediaSuccessCallback cb


text:
module Network.HTTP.Protocol

import Data.String
import Generics.Derive

%language ElabReflection

public export
data Protocol : Type where
  HTTP : Protocol
  HTTPS : Protocol

%runElab derive "Protocol" [Generic, Meta, Eq, DecEq, Show]

public export
protocol_port_number : Protocol -> Bits16
protocol_port_number HTTP = 80
protocol_port_number HTTPS = 443

public export
protocol_from_str : String -> Maybe Protocol
protocol_from_str protocol =
  case toUpper protocol of
    "HTTP" => Just HTTP
    "HTTPS" => Just HTTPS
    _ => Nothing

ext: idr


text:
= Chapter 3

> module Exercises.Interactive

Import `Data.Vect`, because we'll need it later.

> import public Data.Vect

Export functions by default.

> %access export

== 3.2.4 Exercises

=== 1. `length : List a -> Nat`

> my_length : List a -> Nat

Move the point over `my_length` and press `M-RET d` to add a clause.

```idris
my_length xs = ?my_length_rhs
```

Move the point over `xs` and press `C-c C-c` to case split on it.

```idris
my_length [] = ?my_length_rhs_1
my_length (x :: xs) = ?my_length_rhs_2
```

With the point on `?my_length_rhs_1`, press `M-RET p` to have Idris fill in `0`.

> my_length [] = 0

Fill out `?my_length_rhs_2` manually.

> my_length (x :: xs) = S (my_length xs)

=== 2. `reverse : List a -> List a`

> my_reverse : List a -> List a

`M-RET d` on `my_reverse` to add a clause.

```idris
my_reverse xs = ?my_reverse_rhs
```

Case split on `xs` (`C-c C-c`).

```idris
my_reverse [] = ?my_reverse_rhs_1
my_reverse (x :: xs) = ?my_reverse_rhs_2
```

Have Idris fill in `?my_reverse_rhs_1`.

```idris
my_reverse [] = []
```

We're actually going to need to do some fold-like recursion here, so revert back
to `my_reverse xs = ?my_reverse_rhs` and add a `where` clause with a local
function, `go`.

```idris
my_reverse xs = ?my_reverse_rhs
  where go : List a -> List a -> List a
```

Add a clause for `go` (`M-RET d`).

```idris
my_reverse xs = ?my_reverse_rhs
  where
    go : List a -> List a -> List a
    go xs ys = ?go_rhs
```

Case split on `xs` (`C-c C-c`).

```idris
go [] ys = ?go_rhs_1
go (x :: xs) ys = ?go_rhs_2
```

Rename `ys` to `acc`(umulator).

```idris
go [] acc = ?go_rhs_1
go (x :: xs) acc = ?go_rhs_2
```

Have Idris fill in `?go_rhs_1` (`M-RET p`).

```idris
go [] acc = acc
```

Fill in `?go_rhs_2` and `?my_reverse_rhs` manually. Rename the top-level `xs`
to `lst` to avoid confusion/shadowing.

> my_reverse lst = go lst []
>   where
>     go : List a -> List a -> List a
>     go [] acc = acc
>     go (x :: xs) acc = go xs (x :: acc)

=== 3. `map : (a -> b) -> List a -> List b`

> my_map : (a -> b) -> List a -> List b

Press `M-RET d` on `map` to add a clause.

```idris
my_map f xs = ?my_map_rhs
```

Case split (`C-c C-c`) on `xs`.

```idris
my_map f [] = ?my_map_rhs_1
my_map f (x :: xs) = ?my_map_rhs_2
```

Have Idris fill in `?my_map_rhs_1` (`M-RET p`).

> my_map f [] = []

Fill in `?my_map_rhs_2` manually.

> my_map f (x :: xs) = f x :: my_map f xs

=== 4. `map : (a -> b) -> Vect n a -> Vect n b`

> my_vect_map : (a -> b) -> Vect n a -> Vect n b

Add a `my_vect_map` clause (`M-RET d`).

```idris
my_vect_map f xs = ?my_vect_map_rhs
```

~~Case split (`C-c C-c`) on `xs`.~~

N.B. That doesn't seem to work, for whatever reason,
so add the clauses manually.

```idris
my_vect_map f [] = ?my_vect_map_rhs_1
my_vect_map f (x :: xs) = ?my_vect_map_rhs_2
```

Emacs or Idris seems upset about the holes too, so fill them in manually.

> my_vect_map f [] = []
> my_vect_map f (x :: xs) = f x :: map f xs

== 3.3.3 Exercises

=== 1. Reimplement `transpose_mat` with `zipWith` instead of `transpose_helper`

*Type* `transpose_mat`.

```idris
transpose_mat : Vect m (Vect n elem) -> Vect n (Vect m elem)
```

*Define* `transpose_mat`.

N.B. Emacs or Idris is still upset, so this is not very interactive.

```idris
transpose_mat [] = ?transpose_mat_rhs_1
transpose_mat (x :: xs) = ?transpose_mat_rhs_2
```

*Type* `?transpose_mat_rhs_1`.

```idris
  elem : Type
     n : Nat
--------------------------------------
transpose_mat_rhs_1 : Vect n (Vect 0 elem)
```

Rename `?transpose_mat_rhs_1` to `?create_empties` and make a lemma (a.k.a. lift
it to a top-level function) with `M-RET i e`.

```idris
create_empties : Vect n (Vect 0 elem)

transpose_mat : Vect m (Vect n elem) -> Vect n (Vect m elem)
transpose_mat [] = create_empties
transpose_mat (x :: xs) = ?transpose_mat_rhs_2
```

*Type* `?transpose_mat_rhs_2`.

```idris
  elem : Type
     n : Nat
     x : Vect n elem
     k : Nat
    xs : Vect k (Vect n elem)
--------------------------------------
transpose_mat_rhs_2 : Vect n (Vect (S k) elem)
```

(Further) *define* `transpose_mat`.

```idris
create_empties : Vect n (Vect 0 elem)

transpose_mat : Vect m (Vect n elem) -> Vect n (Vect m elem)
transpose_mat [] = create_empties
transpose_mat (x :: xs) = let xs_trans = transpose_mat xs
                          in ?transpose_mat_rhs_2
```

Fill in `?transpose_mat_rhs_2` with `zipWith
and do away with the intermediate variable, `xs_trans`.

```idris
create_empties : Vect n (Vect 0 elem)

transpose_mat : Vect m (Vect n elem) -> Vect n (Vect m elem)
transpose_mat [] = create_empties
transpose_mat (x :: xs) = zipWith (::) x (transpose_mat xs)
```

*Define* `create_empties`.

> public export
> create_empties : Vect n (Vect 0 elem)
> create_empties {n} = replicate n []

> public export
> transpose_mat : Vect m (Vect n elem) -> Vect n (Vect m elem)
> transpose_mat [] = create_empties
> transpose_mat (x :: xs) = zipWith (::) x (transpose_mat xs)

=== 2. `addMatrix`

> public export
> addMatrix : Num numType =>
>             Vect rows (Vect cols numType) -> Vect rows (Vect cols numType) ->
>             Vect rows (Vect cols numType)
> addMatrix []          ys          = ys
> addMatrix (xs :: xxs) (ys :: yys) = zipWith (+) xs ys :: addMatrix xxs yys

=== 3. `multMatrix`

> public export
> multMatrix : Num numType =>
>              Vect n (Vect m numType) -> Vect m (Vect p numType) ->
>              Vect n (Vect p numType)
> multMatrix left right = map (go (transpose_mat right)) left
>   where
>     go : Vect p (Vect m numType) -> Vect m numType -> Vect p numType
>     go xs ys = map (sum . zipWith (*) ys) xs

\[
  \begin{pmatrix}
    1 &   2 \\
    3 &   4 \\
    5 &   6
  \end{pmatrix} \times
  \begin{pmatrix}
    7 &   8 &   9 &  10 \\
   11 &  12 &  13 &  14
  \end{pmatrix} =
  \begin{pmatrix}
   29 &  32 &  35 &  38 \\
   65 &  72 &  79 &  86 \\
  101 & 112 & 123 & 134
  \end{pmatrix}
\]

ext: lidr

max_stars_repo_name: yurrriq/tdd-with-idris

max_issues_repo_name: yurrriq/tdd-with-idris

max_forks_repo_name: yurrriq/tdd-with-idris


text:
-- ------------------------------------------------------------- [ Strings.idr ]
-- Module      : Lightyear.Strings
-- Description : String-related parsers.
--
-- This code is distributed under the BSD 2-clause license.
-- See the file LICENSE in the root directory for its full text.
-- --------------------------------------------------------------------- [ EOH ]
module Lightyear.Strings

import public Data.Vect
import public Data.Fin

import public Control.Monad.Identity

import Lightyear.Core
import Lightyear.Combinators
import Lightyear.Errmsg

import Lightyear.Char

%access export

-- -------------------------------------------------------- [ Helper Functions ]
private
nat2int : Nat -> Int
nat2int  Z    = 0
nat2int (S x) = 1 + nat2int x

implementation Layout String where
  lineLengths = map (nat2int . Prelude.Strings.length) . lines

-- --------------------------------------------------------- [ A String Parser ]
||| Parsers, specialised to Strings
public export
Parser : Type -> Type
Parser = ParserT String Identity

||| Run a parser against an input string
parse : Parser a -> String -> Either String a
parse f s = let Id r = execParserT f s in case r of
  Success _ x => Right x
  Failure es  => Left $ formatError s es

implementation Stream Char String where
  uncons s with (strM s)
    uncons ""             | StrNil       = Nothing
    uncons (strCons x xs) | StrCons x xs = Just (x, xs)

-- ---------------------------------------------------------- [ Reserved Stuff ]

||| A parser that matches a particular string
string : Monad m => String -> ParserT String m String
string s = pack <$> (traverse char $ unpack s) <?> "string " ++ show s

-- ------------------------------------------------------------------- [ Space ]

||| A simple lexer that strips white space from tokens
lexeme : Monad m => ParserT String m a -> ParserT String m a
lexeme p = p <* spaces

-- ------------------------------------------------------------------ [ Tokens ]

||| A parser that matches a specific string, then skips following whitespace
token : Monad m => String -> ParserT String m ()
token s = lexeme (skip (string s)) <?> "token " ++ show s

||| Parses ',' and trailing whitespace.
comma : Monad m => ParserT String m ()
comma = token "," <?> "Comma"

||| Parses '=' and trailing whitespace.
equals : Monad m => ParserT String m ()
equals = token "=" <?> "equals"

||| Parses '.' and trailing whitespace.
dot : Monad m => ParserT String m ()
dot = token "." <?> "dot"

||| Parses ':' and trailing whitespace.
colon : Monad m => ParserT String m ()
colon = token ":" <?> "colon"

||| Parses ';' and trailing whitespace.
semi : Monad m => ParserT String m ()
semi = token ";" <?> "semi colon"

-- -------------------------------------------------- [ Delineated Expressions ]

||| Parses `p` enclosed in parenthesis and returns result of `p`.
parens : Monad m => ParserT String m a -> ParserT String m a
parens p = between (token "(") (token ")") p

||| Parses `p` enclosed in brackets and returns result of `p`.
brackets : Monad m => ParserT String m a -> ParserT String m a
brackets p = between (token "[") (token "]") p

||| Parses `p` enclosed in braces and returns the result of `p`.
braces : Monad m => ParserT String m a -> ParserT String m a
braces p = between (token "{") (token "}") p

||| Parses `p` enclosed in angles and returns the result of `p`.
angles : Monad m => ParserT String m a -> ParserT String m a
angles p = between (token "<") (token ">") p

||| Parses `p` enclosed in single quotes and returns the result of `p`.
||| Not to be used for charLiterals.
squote : Monad m => ParserT String m a -> ParserT String m a
squote p = between (char '\'') (lexeme $ char '\'') p

||| Parses `p` enclosed in double quotes and returns the result of `p`.
||| Not to be used for `stringLiterals`.
dquote : Monad m => ParserT String m a -> ParserT String m a
dquote p = between (char '\"') (lexeme $ char '\"') p

||| Collect the literal string contained between two characters
quoted' : Monad m => Char -> Char -> ParserT String m String
quoted' l r = map pack $ between (char l) (lexeme $ char r) (some (satisfy (/= r)))

||| Literal string between two identical characters
quoted : Monad m => Char -> ParserT String m String
quoted c = quoted' c c

-- --------------------------------------------------- [ Separated Expressions ]
||| Parses /one/ or more occurrences of `p` separated by `comma`.
commaSep1 : Monad m => ParserT String m a -> ParserT String m (List a)
commaSep1 p = p `sepBy1` comma

||| Parses /zero/ or more occurrences of `p` separated by `comma`.
commaSep : Monad m => ParserT String m a -> ParserT String m (List a)
commaSep p = p `sepBy` comma

||| Parses /one/ or more occurrences of `p` separated by `semi`.
semiSep1 : Monad m => ParserT String m a -> ParserT String m (List a)
semiSep1 p = p `sepBy1` semi

||| Parses /zero/ or more occurrences of `p` separated by `semi`.
semiSep : Monad m => ParserT String m a -> ParserT String m (List a)
semiSep p = p `sepBy` semi

||| Run some parser `p` until the second parser is encountered,
||| collecting a list of success for `p`, and the result of the second
||| parser is dropped.
|||
||| Primarily useful for collecting single line comments and other
||| similar verbatim environments.
manyTill : Monad m => ParserT String m a
                   -> ParserT String m b
                   -> ParserT String m (List a)
manyTill p end = scan
  where
    scan : Monad m => ParserT String m (List a)
    scan = do { end; return List.Nil } <|>
           do { x <- p; xs <- scan; return (x::xs)}

-- -------------------------------------------------------- [ Testing Function ]

testParser : Parser a -> String -> IO (Maybe a)
testParser p s = case parse p s of
  Left  e => putStrLn e *> pure Nothing
  Right x => pure (Just x)
-- --------------------------------------------------------------------- [ EOF ]

max_stars_repo_name: david-christiansen/lightyear

max_issues_repo_name: david-christiansen/lightyear

max_forks_repo_name: david-christiansen/lightyear


text:
> module SequentialDecisionProblems.applications.Main

> import Data.Fin
> import Data.List
> import Data.List.Quantifiers
> import Data.So
> import Effects
> import Effect.Exception
> import Effect.StdIO

> import SequentialDecisionProblems.CoreTheory
> import SequentialDecisionProblems.FullTheory
> import SequentialDecisionProblems.TabBackwardsInduction
> import SequentialDecisionProblems.Utils
> import SequentialDecisionProblems.FastStochasticDefaults
> import SequentialDecisionProblems.CoreTheoryOptDefaults
> import SequentialDecisionProblems.FullTheoryOptDefaults
> import SequentialDecisionProblems.TabBackwardsInductionOptDefaults

> import SequentialDecisionProblems.applications.FreezeOrIncrease
> import SequentialDecisionProblems.applications.GoodOrBad

> import FastSimpleProb.SimpleProb
> import FastSimpleProb.BasicOperations
> import FastSimpleProb.BasicProperties
> import FastSimpleProb.MonadicOperations
> import FastSimpleProb.MonadicProperties
> import FastSimpleProb.Measures
> import FastSimpleProb.MeasuresProperties
> import Sigma.Sigma
> import Double.Predicates
> import Double.Postulates
> import Double.Operations
> import Double.Properties
> import NonNegDouble.NonNegDouble
> import NonNegDouble.Constants
> import NonNegDouble.BasicOperations
> import NonNegDouble.Operations
> import NonNegDouble.Properties
> import NonNegDouble.Predicates
> import NonNegDouble.LTEProperties
> import Finite.Predicates
> import Finite.Operations
> import Finite.Properties
> import Decidable.Predicates
> import Decidable.Properties
> import LocalEffect.Exception
> import LocalEffect.StdIO
> import Fin.Operations
> import List.Operations
> import Unit.Properties

> -- %default total
> %auto_implicits off

> -- %logging 5

* Introduction

We specify a first emissions game as a stochastic sequential decision
problem with a single decision maker.

* Controls

At each decision step, the decision maker has two options: freezing
emissions or increasing emissions:

> SequentialDecisionProblems.CoreTheory.Ctrl _ _ = FreezeOrIncrease

* States

At each decision step, the decision maker has to choose an option on the
bases of two data: the amount of cumulated emissions and the state of
the world. The latter can be either good or bad:

> SequentialDecisionProblems.CoreTheory.State t = (Fin (S t), GoodOrBad)

The idea is that the game starts with zero cumulated emissions and with
the world in the good state. In these conditions, the probability to
turn to the bad state is low. But if the cumulated emissions increase
beyond a critical threshold, the probability that the state of the world
turns bad increases.  If the world is the bad state, there is no chance
to come back to the good state. As for controls, it is useful to show
that |State| is finite:

* Transition function

> -- The critical threshold
> cr : Double
> cr = 0.0

> -- The probability of staying in a good world when the cumulated
> -- emissions are below the critical threshold
> p1  :  NonNegDouble
> p1  =  cast 0.65

> -- The probabilities of staying in a good world when the cumulated
> -- emissions are above the critical threshold
> p2  :  NonNegDouble
> p2  =  cast 0.1

> -- The transition function: good world, freezing emissions
> SequentialDecisionProblems.CoreTheory.nexts t (e, Good) Freeze =
>   let goodState = (weaken e, Good) in
>   let badState  = (weaken e, Bad) in
>   if (fromFin e <= cr)
>   then mkSimpleProb [(goodState, p1), (badState, one - p1)]
>   else mkSimpleProb [(goodState, p2), (badState, one - p2)]

> -- The transition function: good world, increasing emissions
> SequentialDecisionProblems.CoreTheory.nexts t (e, Good) Increase =
>   let goodState = (FS e, Good) in
>   let badState  = (FS e, Bad) in
>   if (fromFin e <= cr)  then mkSimpleProb [(goodState, p1), (badState, one - p1)]
>                         else mkSimpleProb [(goodState, p2), (badState, one - p2)]

> -- The transition function: bad world, freezing emissions
> SequentialDecisionProblems.CoreTheory.nexts t (e, Bad) Freeze =
>   let badState  = (weaken e, Bad) in mkSimpleProb [(badState, one)]

> -- The transition function: bad world, increasing emissions
> SequentialDecisionProblems.CoreTheory.nexts t (e, Bad) Increase =
>   let badState  = (FS e, Bad) in mkSimpleProb [(badState, one)]

* |Val| and |LTE|:

> SequentialDecisionProblems.CoreTheory.Val =
>   NonNegDouble.NonNegDouble

> SequentialDecisionProblems.CoreTheory.plus =
>   NonNegDouble.Operations.plus

> SequentialDecisionProblems.CoreTheory.zero =
>   fromInteger @{NumNonNegDouble} 0

> SequentialDecisionProblems.CoreTheory.LTE =
>   NonNegDouble.Predicates.LTE

> SequentialDecisionProblems.FullTheory.reflexiveLTE =
>   NonNegDouble.LTEProperties.reflexiveLTE

> SequentialDecisionProblems.FullTheory.transitiveLTE =
>   NonNegDouble.LTEProperties.transitiveLTE

> SequentialDecisionProblems.FullTheory.monotonePlusLTE =
>   NonNegDouble.LTEProperties.monotonePlusLTE

> SequentialDecisionProblems.CoreTheoryOptDefaults.totalPreorderLTE =
>   NonNegDouble.LTEProperties.totalPreorderLTE

* Reward function

The idea is that being in a good world yields one unit of benefits per
step and being in a bad world yield less benefits:

> -- Ratio of the benefits in a bad world and the benefits in a good world
> badOverGood : NonNegDouble
> badOverGood = cast 0.5

> -- Sanity check
> badOverGoodLTEone : badOverGood `NonNegDouble.Predicates.LTE` one
> badOverGoodLTEone = MkLTE Oh

Emitting greenhouse gases also brings benefits. These are a fraction of
the step benefits in a good world and freezing emissions brings less
benefits than increasing emissions:

> -- Ratio between freezing emissions benefits and step benefits (in a good world)
> freezeOverGood : NonNegDouble
> freezeOverGood = cast 0.1

> -- Ratio between increasing emissions benefits and step benefits (in a good world)
> increaseOverGood : NonNegDouble
> increaseOverGood = cast 0.3

> -- Sanity check
> freezeOverGoodLTEone : freezeOverGood `NonNegDouble.Predicates.LTE` one
> freezeOverGoodLTEone = MkLTE Oh

> -- Sanity check
> increaseOverGoodLTEone : increaseOverGood `NonNegDouble.Predicates.LTE` one
> increaseOverGoodLTEone = MkLTE Oh

> -- Sanity check
> freezeLTEincrease : freezeOverGood `NonNegDouble.Predicates.LTE` increaseOverGood
> freezeLTEincrease = MkLTE Oh

> -- Reward function:
>
> using implementation NumNonNegDouble
>
>   SequentialDecisionProblems.CoreTheory.reward _ _ Freeze   (_, Good) =
>     one                       + one * freezeOverGood
>   SequentialDecisionProblems.CoreTheory.reward _ _ Increase (_, Good) =
>     one                       + one * increaseOverGood
>   SequentialDecisionProblems.CoreTheory.reward _ _ Freeze   (_,  Bad) =
>     one * badOverGood + one * freezeOverGood
>   SequentialDecisionProblems.CoreTheory.reward _ _ Increase (_,  Bad) =
>     one * badOverGood + one * increaseOverGood

* Completing the problem specification

To be able to apply the verified, generic backwards induction algorithm
of |CoreTheory| to compute optimal policies for our problem, we have to
explain how the decision maker accounts for uncertainties on rewards
induced by uncertainties in the transition function. We first assume
that the decision maker measures uncertain rewards by their expected
value:

> SequentialDecisionProblems.CoreTheory.meas = expectedValue
> SequentialDecisionProblems.FullTheory.measMon = monotoneExpectedValue

Further on, we have to implement the notions of viability and
reachability. We start by positing that all states are viable for any
number of steps:

> -- Viable : (n : Nat) -> State t -> Type
> SequentialDecisionProblems.CoreTheory.Viable n x = Unit

From this definition, it trivially follows that all elements of an
arbitrary list of states are viable for an arbitrary number of steps:

> viableLemma : {t, n : Nat} -> (xs : List (State t)) -> All (Viable n) xs
> viableLemma  Nil      = Nil
> viableLemma {t} {n} (x :: xs) = () :: (viableLemma {t} {n} xs)

This fact and the (less trivial) result that simple probability
distributions are never empty, see |nonEmptyLemma| in
|MonadicProperties| in |SimpleProb|, allows us to show that the above
definition of |Viable| fulfills |viableSpec1|:

> -- viableSpec1 : (x : State t) -> Viable (S n) x -> GoodCtrl t x
> SequentialDecisionProblems.CoreTheory.viableSpec1 {t} {n} s v =
>   MkSigma Freeze (ne, av) where
>     ne : SequentialDecisionProblems.CoreTheory.NotEmpty (nexts t s Freeze)
>     ne = nonEmptyLemma (nexts t s Freeze)
>     av : SequentialDecisionProblems.CoreTheory.All (Viable {t = S t} n) (nexts t s Freeze)
>     av = viableLemma {t = S t} (support (nexts t s Freeze))

> SequentialDecisionProblems.Utils.finiteViable n x = finiteUnit

> SequentialDecisionProblems.Utils.decidableViable n x = decidableUnit

For reachability, we proceed in a similar way. We say that all states
are reachable

> -- Reachable : State t' -> Type
> SequentialDecisionProblems.CoreTheory.Reachable x' = Unit

which immediately implies |reachableSpec1|:

> -- reachableSpec1 : (x : State t) -> Reachable {t' = t} x -> (y : Ctrl t x) -> All (Reachable {t' = S t}) (nexts t x y)
> SequentialDecisionProblems.CoreTheory.reachableSpec1 {t} x r y = all (nexts t x y) where
>   all : (sp : SimpleProb  (State (S t))) -> SequentialDecisionProblems.CoreTheory.All (Reachable {t' = S t}) sp
>   all sp = all' (support sp) where
>     all' : (xs : List (State (S t))) -> Data.List.Quantifiers.All (Reachable {t' = S t}) xs
>     all' Nil = Nil
>     all' (x :: xs) = () :: (all' xs)

and decidability of |Reachable|:

> SequentialDecisionProblems.TabBackwardsInduction.decidableReachable x = decidableUnit

Finally, we have to show that controls are finite

> -- finiteCtrl : {t : Nat} -> (x : State t) -> Finite (Ctrl t x)
> SequentialDecisionProblems.Utils.finiteCtrl _ = finiteFreezeOrIncrease

and, in order to use the fast, tail-recursive tabulated version of
backwards induction, that states are finite:

> SequentialDecisionProblems.TabBackwardsInduction.finiteState t =
>   finitePair (finiteFin) (finiteGoodOrBad)

* Optimal policies, optimal decisions, ...

We can now apply the results of our |CoreTheory| and of the |FullTheory|
to compute verified optimal policies, possible state-control sequences,
etc. To this end, we need to be able to show the outcome of the decision
process. This means implemeting functions to print states and controls:

> -- showState : {t : Nat} -> State t -> String
> SequentialDecisionProblems.Utils.showState {t} (e, Good) =
>   "(" ++ show (finToNat e) ++ ",Good)"
> SequentialDecisionProblems.Utils.showState {t} (e, Bad) =
>   "(" ++ show (finToNat e) ++ ",Bad)"

> -- showControl : {t : Nat} -> {x : State t} -> Ctrl t x -> String
> SequentialDecisionProblems.Utils.showCtrl {t} {x} Freeze = "Freeze"
> SequentialDecisionProblems.Utils.showCtrl {t} {x} Increase = "Increase"

>
> using implementation ShowNonNegDouble
>
>   computation : { [STDIO] } Eff ()
>   computation =
>     do putStr ("enter number of steps:\n")
>        nSteps <- getNat
>        case (decidableViable {t = Z} nSteps (FZ, Good)) of
>          (Yes v) => do putStrLn ("computing optimal policies ...")
>                        -- ps   <- pure (backwardsInduction Z nSteps)
>                        ps   <- pure (tabTailRecursiveBackwardsInduction Z nSteps)
>                        putStrLn ("computing optimal controls ...")
>                        mxys <- pure (possibleStateCtrlSeqs (FZ, Good) () v ps)
>                        putStrLn "possible state-control sequences:"
>                        putStr "  "
>                        putStrLn (showlong mxys)
>                        mvs <- pure (possibleRewards' mxys)
>                        putStrLn "possible rewards:"
>                        putStr "  "
>                        putStrLn (show mvs)
>                        putStrLn ("done!")
>          (No _)  => putStrLn ("initial state non viable for " ++ cast {from = Int} (cast nSteps) ++ " steps")

> main : IO ()
> main = run computation

> {-

> ---}

-- Local Variables:
-- idris-packages: ("effects")
-- End:

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
module JS

%access public export

%inline
js : (fname : String) ->
     (ty : Type) ->
     {auto fty : FTy FFI_JS [] ty} ->
     ty
js = foreign FFI_JS

SetKeyValue : Type
SetKeyValue = Ptr -> (key : String) -> (value : String) -> JS_IO ()

GetString : Type
GetString = Ptr -> JS_IO String

SendString : Type
SendString = Ptr -> String -> JS_IO ()

SendInt : Type
SendInt = Ptr -> Int -> JS_IO ()

Command : Type
Command = Ptr -> JS_IO ()

TwoArgChain : Type
TwoArgChain = JsFn (Ptr -> JsFn (Ptr -> JS_IO ()))

write : SendString
write = js "%0.write(%1)" SendString

writeHead : Cast a Int => (res : Ptr) -> (code : a) -> JS_IO ()
writeHead res code = js "%0.writeHead(%1)" SendInt res (cast code)

setHeader : Ptr -> (String, String) -> JS_IO ()
setHeader ptrRes (k, v) =
  js "%0.setHeader(%1, %2)"
     (Ptr -> String -> String -> JS_IO ())
     ptrRes k v

setHeaders : Ptr -> List (String, String) -> JS_IO ()
setHeaders = traverse_ . setHeader

method : GetString
method = js "%0.method" GetString

url : GetString
url = js "%0.url" GetString

end : Command
end = js "%0.end()" Command

byteLength : String -> JS_IO Int
byteLength = js "Buffer.byteLength(%0)" (String -> JS_IO Int)

max_stars_repo_name: camelpunch/idris-web-server

max_issues_repo_name: camelpunch/idris-web-server

max_forks_repo_name: camelpunch/idris-web-server


text:
module HOF

%default total

twice : (a -> a) -> a -> a
twice f x = f (f x)

Shape : Type
rotate : Shape -> Shape

double : Num ty => ty -> ty
double x = x + x

quadruple : Num ty => ty -> ty
quadruple = twice double

turnAround : Shape -> Shape
turnAround = twice rotate

max_stars_repo_name: timmyjose-study/tdd-with-idris

max_issues_repo_name: timmyjose-study/tdd-with-idris

max_forks_repo_name: timmyjose-study/tdd-with-idris


text:
module IncoherentIDefAndPatClauseNames

import Language.Reflection

%language ElabReflection

declBody : Elab ()
declBody = declare [
    IDef EmptyFC `{test} [
      PatClause EmptyFC
        (IVar EmptyFC `{test2})
        (IPrimVal EmptyFC $ BI 4)
    ]
  ]

test : Integer
test2 : Integer

%runElab declBody

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
module GTK.GLib

import GTK.Utils
import GTK.GTK

libglib : String -> String
libglib fname = "C:\{fname},libglib-2.0.so"

public export
G_CONNECT_AFTER : Int
G_CONNECT_AFTER = 0b1

public export
G_CONNECT_SWAPPED : Int
G_CONNECT_SWAPPED = 0b10

public export
GConnectFlags : Type
GConnectFlags = Int

public export
GCallback : Type
GCallback = PrimIO ()

export
data GClosure : Type where

public export
GClosureNotify : Type
GClosureNotify = AnyPtr -> Ptr GClosure -> PrimIO ()

export
data GObject : Type where

export %foreign libglib "g_signal_connect_data"
g_signal_connect_data : Ptr GObject -> (detailed_signal : String) -> GCallback -> (data_ : AnyPtr) -> GConnectFlags -> GClosureNotify -> PrimIO Int

export
to_object : Ptr GtkWidget -> Ptr GObject
to_object = believe_me


text:
module Cat

import World

%access export

record Cat where
  constructor MkCat
  catHealth : Int
  catBlack  : Bool

%name Cat cat, cat'

catAttack : Int -> Cat -> Cat
catAttack x (MkCat h b) = if b then MkCat (h + x) b
                               else if h <= x then MkCat 0 True
                                              else MkCat (h - x) b

entityCat : Entity Cat
entityCat = MkEntity catHealth catAttack

spawnCat : Key -> Cat -> Host -> Host
spawnCat = spawn entityCat


text:
module Erlang.Data.Ref

import public Erlang.Data.IORef
import public Erlang.Control.Monad.ST

%default total

public export
interface Ref m (r : Type -> Type) | m where
  newRef : a -> m (r a)
  readRef : r a -> m a
  writeRef : r a -> a -> m ()

export
HasIO io => Ref io IORef where
  newRef = newIORef
  readRef = readIORef
  writeRef = writeIORef

export
Ref (ST s) (STRef s) where
  newRef = newSTRef
  readRef = readSTRef
  writeRef = writeSTRef


text:
module Monoids

%default total

{-
  interface Semigroup ty where
    (<+>) : ty -> ty -> ty

  interface Semigroup ty => Monoid ty where
    neutral : ty
-}

-- lets' define IntS as Monoids under both addition and multiplication

[PlusIntSemi] Semigroup Int where
  (<+>) x y = x + y

[PlusIntMonoid] Monoid Int using PlusIntSemi where
  neutral = 0

[MultIntSemi] Semigroup Int where
  (<+>) x y = x * y

[MultIntMonoid] Monoid Int using MultIntSemi where
  neutral = 1

max_stars_repo_name: timmyjose-study/idris-from-the-docs

max_issues_repo_name: timmyjose-study/idris-from-the-docs

max_forks_repo_name: timmyjose-study/idris-from-the-docs


text:
module Data.String.StringUtils

import Data.Bool.BoolTheorems
import Data.Nat.NatTheorems

%default total
%access public export

strIndex' : (str : String)
            -> (idx : Nat)
            -> {prf : Nat.LT idx (length str)}
            -> Char
strIndex' str idx =
  assert_total (prim__strIndex str (toIntNat idx))

private
chrDigit : (c : Char) -> Maybe Nat
chrDigit c = if isDigit c then Just (cast $ (ord c) - (ord '0')) else Nothing

Cast String (Maybe Nat) where
  cast s = doCast 0 0 totalLength where
    totalLength : Nat
    totalLength = length s

    -- TODO: Remaining length is redundant with offset.
    doCast : Nat -> Nat -> Nat -> Maybe Nat
    doCast accum offs Z = Just accum
    doCast accum offs (S lRet) =
      ifWithProofs (ltNat offs totalLength)
        (\prfLt => do
          digit <- chrDigit (strIndex' s offs {
                     prf = natALtBIsTrueImpliesLTAB offs totalLength $
                       ltNatIsLt prfLt})
          doCast (accum * 10 + digit) (S offs) lRet
        )
        (\_ => Just accum)

private
natCast : String -> Maybe Nat
natCast = cast

private
test_cast_valid_string : (natCast "123" = Just 123)
test_cast_valid_string = Refl

private
test_cast_invalid_string : (natCast "123a" = Nothing)
test_cast_invalid_string = Refl

-- TODO: Round tripping property? Contains non-digit implies Nothing?


text:
module Idris.SetOptions

import Core.Context
import Core.Directory
import Core.Metadata
import Core.Options
import Core.Unify
import Utils.Path

import Idris.CommandLine
import Idris.Error
import Idris.REPL
import Idris.Syntax
import Idris.Version

import IdrisPaths

import Data.So
import System

%default covering

dirOption : Dirs -> DirCommand -> Core ()
dirOption dirs LibDir
    = coreLift $ putStrLn
         (prefix_dir dirs </> "idris2-" ++ showVersion False version)

-- Options to be processed before type checking. Return whether to continue.
export
preOptions : {auto c : Ref Ctxt Defs} ->
             {auto o : Ref ROpts REPLOpts} ->
             List CLOpt -> Core Bool
preOptions [] = pure True
preOptions (NoBanner :: opts)
    = do setSession (record { nobanner = True } !getSession)
         preOptions opts
-- These things are processed later, but imply nobanner too
preOptions (OutputFile _ :: opts)
    = do setSession (record { nobanner = True } !getSession)
         preOptions opts
preOptions (ExecFn _ :: opts)
    = do setSession (record { nobanner = True } !getSession)
         preOptions opts
preOptions (IdeMode :: opts)
    = do setSession (record { nobanner = True } !getSession)
         preOptions opts
preOptions (IdeModeSocket _ :: opts)
    = do setSession (record { nobanner = True } !getSession)
         preOptions opts
preOptions (CheckOnly :: opts)
    = do setSession (record { nobanner = True } !getSession)
         preOptions opts
preOptions (Quiet :: opts)
    = do setOutput (REPL True)
         preOptions opts
preOptions (NoPrelude :: opts)
    = do setSession (record { noprelude = True } !getSession)
         preOptions opts
preOptions (SetCG e :: opts)
    = do defs <- get Ctxt
         case getCG (options defs) e of
            Just cg => do setCG cg
                          preOptions opts
            Nothing =>
              do coreLift $ putStrLn "No such code generator"
                 coreLift $ putStrLn $ "Code generators available: " ++
                                 showSep ", " (map fst (availableCGs (options defs)))
                 coreLift $ exitWith (ExitFailure 1)
preOptions (Directive d :: opts)
    = do setSession (record { directives $= (d::) } !getSession)
         preOptions opts
preOptions (PkgName p :: opts)
    = do addPkg p
         preOptions opts
preOptions (SourceDir d :: opts)
    = do setSourceDir (Just d)
         preOptions opts
preOptions (BuildDir d :: opts)
    = do setBuildDir d
         preOptions opts
preOptions (OutputDir d :: opts)
    = do setOutputDir (Just d)
         preOptions opts
preOptions (Directory d :: opts)
    = do defs <- get Ctxt
         dirOption (dirs (options defs)) d
         pure False
preOptions (Timing :: opts)
    = do setLogTimings True
         preOptions opts
preOptions (DebugElabCheck :: opts)
    = do setDebugElabCheck True
         preOptions opts
preOptions (RunREPL _ :: opts)
    = do setOutput (REPL True)
         setSession (record { nobanner = True } !getSession)
         preOptions opts
preOptions (FindIPKG :: opts)
    = do setSession (record { findipkg = True } !getSession)
         preOptions opts
preOptions (ChangedModules ns :: opts)
    = do setSession (record { changedModules = ns } !getSession)
         preOptions opts
preOptions (DumpCases f :: opts)
    = do setSession (record { dumpcases = Just f } !getSession)
         preOptions opts
preOptions (DumpLifted f :: opts)
    = do setSession (record { dumplifted = Just f } !getSession)
         preOptions opts
preOptions (DumpANF f :: opts)
    = do setSession (record { dumpanf = Just f } !getSession)
         preOptions opts
preOptions (DumpVMCode f :: opts)
    = do setSession (record { dumpvmcode = Just f } !getSession)
         preOptions opts
preOptions (Logging n :: opts)
    = do setSession (record { logLevel $= insertLogLevel n } !getSession)
         preOptions opts
preOptions (ConsoleWidth n :: opts)
    = do setConsoleWidth n
         preOptions opts
preOptions (Color b :: opts)
    = do setColor b
         preOptions opts
preOptions (_ :: opts) = preOptions opts

-- Options to be processed after type checking. Returns whether execution
-- should continue (i.e., whether to start a REPL)
export
postOptions : {auto c : Ref Ctxt Defs} ->
              {auto u : Ref UST UState} ->
              {auto s : Ref Syn SyntaxInfo} ->
              {auto m : Ref MD Metadata} ->
              {auto o : Ref ROpts REPLOpts} ->
              REPLResult -> List CLOpt -> Core Bool
postOptions _ [] = pure True
postOptions res@(ErrorLoadingFile _ _) (OutputFile _ :: rest)
    = do postOptions res rest
         pure False
postOptions res (OutputFile outfile :: rest)
    = do compileExp (PRef (MkFC "(script)" (0, 0) (0, 0)) (UN "main")) outfile
         postOptions res rest
         pure False
postOptions res (ExecFn str :: rest)
    = catch (do execExp (PRef (MkFC "(script)" (0, 0) (0, 0)) (UN str))
                postOptions res rest
                pure False)
            (\err => do perror err >>= printError; pure False)
postOptions res (CheckOnly :: rest)
    = do postOptions res rest
         pure False
postOptions res (RunREPL str :: rest)
    = do replCmd str
         pure False
postOptions res (_ :: rest) = postOptions res rest

export
ideMode : List CLOpt -> Bool
ideMode [] = False
ideMode (IdeMode :: _) = True
ideMode (_ :: xs) = ideMode xs

export
ideModeSocket : List CLOpt -> Bool
ideModeSocket [] = False
ideModeSocket (IdeModeSocket _ :: _) = True
ideModeSocket (_ :: xs) = ideModeSocket xs