text:
module Web.Internal.MediastreamPrim

import JS
import Web.Internal.Types

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

namespace ConstrainablePattern

  export
  %foreign "browser:lambda:(x,a)=>x.applyConstraints(a)"
  prim__applyConstraints :  ConstrainablePattern
                         -> UndefOr Constraints
                         -> PrimIO (Promise Undefined)

  export
  %foreign "browser:lambda:x=>x.getCapabilities()"
  prim__getCapabilities : ConstrainablePattern -> PrimIO Capabilities

  export
  %foreign "browser:lambda:x=>x.getConstraints()"
  prim__getConstraints : ConstrainablePattern -> PrimIO Constraints

  export
  %foreign "browser:lambda:x=>x.getSettings()"
  prim__getSettings : ConstrainablePattern -> PrimIO Settings

namespace InputDeviceInfo

  export
  %foreign "browser:lambda:x=>x.getCapabilities()"
  prim__getCapabilities : InputDeviceInfo -> PrimIO MediaTrackCapabilities

namespace MediaDeviceInfo

  export
  %foreign "browser:lambda:x=>x.deviceId"
  prim__deviceId : MediaDeviceInfo -> PrimIO String

  export
  %foreign "browser:lambda:x=>x.groupId"
  prim__groupId : MediaDeviceInfo -> PrimIO String

  export
  %foreign "browser:lambda:x=>x.kind"
  prim__kind : MediaDeviceInfo -> PrimIO String

  export
  %foreign "browser:lambda:x=>x.label"
  prim__label : MediaDeviceInfo -> PrimIO String

  export
  %foreign "browser:lambda:x=>x.toJSON()"
  prim__toJSON : MediaDeviceInfo -> PrimIO Object

namespace MediaDevices

  export
  %foreign "browser:lambda:x=>x.ondevicechange"
  prim__ondevicechange : MediaDevices -> PrimIO (Nullable EventHandlerNonNull)

  export
  %foreign "browser:lambda:(x,v)=>{x.ondevicechange = v}"
  prim__setOndevicechange :  MediaDevices
                          -> Nullable EventHandlerNonNull
                          -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.enumerateDevices()"
  prim__enumerateDevices :  MediaDevices
                         -> PrimIO (Promise (Array MediaDeviceInfo))

  export
  %foreign "browser:lambda:x=>x.getSupportedConstraints()"
  prim__getSupportedConstraints :  MediaDevices
                                -> PrimIO MediaTrackSupportedConstraints

  export
  %foreign "browser:lambda:(x,a)=>x.getUserMedia(a)"
  prim__getUserMedia :  MediaDevices
                     -> UndefOr MediaStreamConstraints
                     -> PrimIO (Promise MediaStream)

namespace MediaStream

  export
  %foreign "browser:lambda:()=> new MediaStream()"
  prim__new : PrimIO MediaStream

  export
  %foreign "browser:lambda:(a)=> new MediaStream(a)"
  prim__new1 : MediaStream -> PrimIO MediaStream

  export
  %foreign "browser:lambda:(a)=> new MediaStream(a)"
  prim__new2 : Array MediaStreamTrack -> PrimIO MediaStream

  export
  %foreign "browser:lambda:x=>x.active"
  prim__active : MediaStream -> PrimIO Boolean

  export
  %foreign "browser:lambda:x=>x.id"
  prim__id : MediaStream -> PrimIO String

  export
  %foreign "browser:lambda:x=>x.onaddtrack"
  prim__onaddtrack : MediaStream -> PrimIO (Nullable EventHandlerNonNull)

  export
  %foreign "browser:lambda:(x,v)=>{x.onaddtrack = v}"
  prim__setOnaddtrack : MediaStream -> Nullable EventHandlerNonNull -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.onremovetrack"
  prim__onremovetrack : MediaStream -> PrimIO (Nullable EventHandlerNonNull)

  export
  %foreign "browser:lambda:(x,v)=>{x.onremovetrack = v}"
  prim__setOnremovetrack :  MediaStream
                         -> Nullable EventHandlerNonNull
                         -> PrimIO ()

  export
  %foreign "browser:lambda:(x,a)=>x.addTrack(a)"
  prim__addTrack : MediaStream -> MediaStreamTrack -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.clone()"
  prim__clone : MediaStream -> PrimIO MediaStream

  export
  %foreign "browser:lambda:x=>x.getAudioTracks()"
  prim__getAudioTracks : MediaStream -> PrimIO (Array MediaStreamTrack)

  export
  %foreign "browser:lambda:(x,a)=>x.getTrackById(a)"
  prim__getTrackById :  MediaStream
                     -> String
                     -> PrimIO (Nullable MediaStreamTrack)

  export
  %foreign "browser:lambda:x=>x.getTracks()"
  prim__getTracks : MediaStream -> PrimIO (Array MediaStreamTrack)

  export
  %foreign "browser:lambda:x=>x.getVideoTracks()"
  prim__getVideoTracks : MediaStream -> PrimIO (Array MediaStreamTrack)

  export
  %foreign "browser:lambda:(x,a)=>x.removeTrack(a)"
  prim__removeTrack : MediaStream -> MediaStreamTrack -> PrimIO ()

namespace MediaStreamTrack

  export
  %foreign "browser:lambda:x=>x.enabled"
  prim__enabled : MediaStreamTrack -> PrimIO Boolean

  export
  %foreign "browser:lambda:(x,v)=>{x.enabled = v}"
  prim__setEnabled : MediaStreamTrack -> Boolean -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.id"
  prim__id : MediaStreamTrack -> PrimIO String

  export
  %foreign "browser:lambda:x=>x.kind"
  prim__kind : MediaStreamTrack -> PrimIO String

  export
  %foreign "browser:lambda:x=>x.label"
  prim__label : MediaStreamTrack -> PrimIO String

  export
  %foreign "browser:lambda:x=>x.muted"
  prim__muted : MediaStreamTrack -> PrimIO Boolean

  export
  %foreign "browser:lambda:x=>x.onended"
  prim__onended : MediaStreamTrack -> PrimIO (Nullable EventHandlerNonNull)

  export
  %foreign "browser:lambda:(x,v)=>{x.onended = v}"
  prim__setOnended :  MediaStreamTrack
                   -> Nullable EventHandlerNonNull
                   -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.onmute"
  prim__onmute : MediaStreamTrack -> PrimIO (Nullable EventHandlerNonNull)

  export
  %foreign "browser:lambda:(x,v)=>{x.onmute = v}"
  prim__setOnmute :  MediaStreamTrack
                  -> Nullable EventHandlerNonNull
                  -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.onunmute"
  prim__onunmute : MediaStreamTrack -> PrimIO (Nullable EventHandlerNonNull)

  export
  %foreign "browser:lambda:(x,v)=>{x.onunmute = v}"
  prim__setOnunmute :  MediaStreamTrack
                    -> Nullable EventHandlerNonNull
                    -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.readyState"
  prim__readyState : MediaStreamTrack -> PrimIO String

  export
  %foreign "browser:lambda:(x,a)=>x.applyConstraints(a)"
  prim__applyConstraints :  MediaStreamTrack
                         -> UndefOr MediaTrackConstraints
                         -> PrimIO (Promise Undefined)

  export
  %foreign "browser:lambda:x=>x.clone()"
  prim__clone : MediaStreamTrack -> PrimIO MediaStreamTrack

  export
  %foreign "browser:lambda:x=>x.getCapabilities()"
  prim__getCapabilities : MediaStreamTrack -> PrimIO MediaTrackCapabilities

  export
  %foreign "browser:lambda:x=>x.getConstraints()"
  prim__getConstraints : MediaStreamTrack -> PrimIO MediaTrackConstraints

  export
  %foreign "browser:lambda:x=>x.getSettings()"
  prim__getSettings : MediaStreamTrack -> PrimIO MediaTrackSettings

  export
  %foreign "browser:lambda:x=>x.stop()"
  prim__stop : MediaStreamTrack -> PrimIO ()

namespace MediaStreamTrackEvent

  export
  %foreign "browser:lambda:(a,b)=> new MediaStreamTrackEvent(a,b)"
  prim__new :  String
            -> MediaStreamTrackEventInit
            -> PrimIO MediaStreamTrackEvent

  export
  %foreign "browser:lambda:x=>x.track"
  prim__track : MediaStreamTrackEvent -> PrimIO MediaStreamTrack

namespace OverconstrainedError

  export
  %foreign "browser:lambda:(a,b)=> new OverconstrainedError(a,b)"
  prim__new : String -> UndefOr String -> PrimIO OverconstrainedError

  export
  %foreign "browser:lambda:x=>x.constraint"
  prim__constraint : OverconstrainedError -> PrimIO String

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

namespace Capabilities

  export
  %foreign "browser:lambda:()=> {}"
  prim__new : PrimIO Capabilities

namespace ConstrainBooleanParameters

  export
  %foreign "browser:lambda:(a,b)=> {exact: a,ideal: b}"
  prim__new :  UndefOr Boolean
            -> UndefOr Boolean
            -> PrimIO ConstrainBooleanParameters

  export
  %foreign "browser:lambda:x=>x.exact"
  prim__exact : ConstrainBooleanParameters -> PrimIO (UndefOr Boolean)

  export
  %foreign "browser:lambda:(x,v)=>{x.exact = v}"
  prim__setExact : ConstrainBooleanParameters -> UndefOr Boolean -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.ideal"
  prim__ideal : ConstrainBooleanParameters -> PrimIO (UndefOr Boolean)

  export
  %foreign "browser:lambda:(x,v)=>{x.ideal = v}"
  prim__setIdeal : ConstrainBooleanParameters -> UndefOr Boolean -> PrimIO ()

namespace ConstrainDOMStringParameters

  export
  %foreign "browser:lambda:(a,b)=> {exact: a,ideal: b}"
  prim__new :  UndefOr (Union2 String (Array String))
            -> UndefOr (Union2 String (Array String))
            -> PrimIO ConstrainDOMStringParameters

  export
  %foreign "browser:lambda:x=>x.exact"
  prim__exact :  ConstrainDOMStringParameters
              -> PrimIO (UndefOr (Union2 String (Array String)))

  export
  %foreign "browser:lambda:(x,v)=>{x.exact = v}"
  prim__setExact :  ConstrainDOMStringParameters
                 -> UndefOr (Union2 String (Array String))
                 -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.ideal"
  prim__ideal :  ConstrainDOMStringParameters
              -> PrimIO (UndefOr (Union2 String (Array String)))

  export
  %foreign "browser:lambda:(x,v)=>{x.ideal = v}"
  prim__setIdeal :  ConstrainDOMStringParameters
                 -> UndefOr (Union2 String (Array String))
                 -> PrimIO ()

namespace ConstrainDoubleRange

  export
  %foreign "browser:lambda:(a,b)=> {exact: a,ideal: b}"
  prim__new : UndefOr Double -> UndefOr Double -> PrimIO ConstrainDoubleRange

  export
  %foreign "browser:lambda:x=>x.exact"
  prim__exact : ConstrainDoubleRange -> PrimIO (UndefOr Double)

  export
  %foreign "browser:lambda:(x,v)=>{x.exact = v}"
  prim__setExact : ConstrainDoubleRange -> UndefOr Double -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.ideal"
  prim__ideal : ConstrainDoubleRange -> PrimIO (UndefOr Double)

  export
  %foreign "browser:lambda:(x,v)=>{x.ideal = v}"
  prim__setIdeal : ConstrainDoubleRange -> UndefOr Double -> PrimIO ()

namespace ConstrainULongRange

  export
  %foreign "browser:lambda:(a,b)=> {exact: a,ideal: b}"
  prim__new : UndefOr Bits32 -> UndefOr Bits32 -> PrimIO ConstrainULongRange

  export
  %foreign "browser:lambda:x=>x.exact"
  prim__exact : ConstrainULongRange -> PrimIO (UndefOr Bits32)

  export
  %foreign "browser:lambda:(x,v)=>{x.exact = v}"
  prim__setExact : ConstrainULongRange -> UndefOr Bits32 -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.ideal"
  prim__ideal : ConstrainULongRange -> PrimIO (UndefOr Bits32)

  export
  %foreign "browser:lambda:(x,v)=>{x.ideal = v}"
  prim__setIdeal : ConstrainULongRange -> UndefOr Bits32 -> PrimIO ()

namespace ConstraintSet

  export
  %foreign "browser:lambda:()=> {}"
  prim__new : PrimIO ConstraintSet

namespace Constraints

  export
  %foreign "browser:lambda:(a)=> {advanced: a}"
  prim__new : UndefOr (Array ConstraintSet) -> PrimIO Constraints

  export
  %foreign "browser:lambda:x=>x.advanced"
  prim__advanced : Constraints -> PrimIO (UndefOr (Array ConstraintSet))

  export
  %foreign "browser:lambda:(x,v)=>{x.advanced = v}"
  prim__setAdvanced : Constraints -> UndefOr (Array ConstraintSet) -> PrimIO ()

namespace DoubleRange

  export
  %foreign "browser:lambda:(a,b)=> {max: a,min: b}"
  prim__new : UndefOr Double -> UndefOr Double -> PrimIO DoubleRange

  export
  %foreign "browser:lambda:x=>x.max"
  prim__max : DoubleRange -> PrimIO (UndefOr Double)

  export
  %foreign "browser:lambda:(x,v)=>{x.max = v}"
  prim__setMax : DoubleRange -> UndefOr Double -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.min"
  prim__min : DoubleRange -> PrimIO (UndefOr Double)

  export
  %foreign "browser:lambda:(x,v)=>{x.min = v}"
  prim__setMin : DoubleRange -> UndefOr Double -> PrimIO ()

namespace MediaStreamConstraints

  export
  %foreign "browser:lambda:(a,b)=> {video: a,audio: b}"
  prim__new :  UndefOr (Union2 Boolean MediaTrackConstraints)
            -> UndefOr (Union2 Boolean MediaTrackConstraints)
            -> PrimIO MediaStreamConstraints

  export
  %foreign "browser:lambda:x=>x.audio"
  prim__audio :  MediaStreamConstraints
              -> PrimIO (UndefOr (Union2 Boolean MediaTrackConstraints))

  export
  %foreign "browser:lambda:(x,v)=>{x.audio = v}"
  prim__setAudio :  MediaStreamConstraints
                 -> UndefOr (Union2 Boolean MediaTrackConstraints)
                 -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.video"
  prim__video :  MediaStreamConstraints
              -> PrimIO (UndefOr (Union2 Boolean MediaTrackConstraints))

  export
  %foreign "browser:lambda:(x,v)=>{x.video = v}"
  prim__setVideo :  MediaStreamConstraints
                 -> UndefOr (Union2 Boolean MediaTrackConstraints)
                 -> PrimIO ()

namespace MediaStreamTrackEventInit

  export
  %foreign "browser:lambda:(a)=> {track: a}"
  prim__new : MediaStreamTrack -> PrimIO MediaStreamTrackEventInit

  export
  %foreign "browser:lambda:x=>x.track"
  prim__track : MediaStreamTrackEventInit -> PrimIO MediaStreamTrack

  export
  %foreign "browser:lambda:(x,v)=>{x.track = v}"
  prim__setTrack : MediaStreamTrackEventInit -> MediaStreamTrack -> PrimIO ()

namespace MediaTrackCapabilities

  export
  %foreign "browser:lambda:(a,b,c,d,e,f,g,h,i,j,k,l,m,n,o)=> {width: a,height: b,aspectRatio: c,frameRate: d,facingMode: e,resizeMode: f,sampleRate: g,sampleSize: h,echoCancellation: i,autoGainControl: j,noiseSuppression: k,latency: l,channelCount: m,deviceId: n,groupId: o}"
  prim__new :  UndefOr ULongRange
            -> UndefOr ULongRange
            -> UndefOr DoubleRange
            -> UndefOr DoubleRange
            -> UndefOr (Array String)
            -> UndefOr (Array String)
            -> UndefOr ULongRange
            -> UndefOr ULongRange
            -> UndefOr (Array Boolean)
            -> UndefOr (Array Boolean)
            -> UndefOr (Array Boolean)
            -> UndefOr DoubleRange
            -> UndefOr ULongRange
            -> UndefOr String
            -> UndefOr String
            -> PrimIO MediaTrackCapabilities

  export
  %foreign "browser:lambda:x=>x.aspectRatio"
  prim__aspectRatio : MediaTrackCapabilities -> PrimIO (UndefOr DoubleRange)

  export
  %foreign "browser:lambda:(x,v)=>{x.aspectRatio = v}"
  prim__setAspectRatio :  MediaTrackCapabilities
                       -> UndefOr DoubleRange
                       -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.autoGainControl"
  prim__autoGainControl :  MediaTrackCapabilities
                        -> PrimIO (UndefOr (Array Boolean))

  export
  %foreign "browser:lambda:(x,v)=>{x.autoGainControl = v}"
  prim__setAutoGainControl :  MediaTrackCapabilities
                           -> UndefOr (Array Boolean)
                           -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.channelCount"
  prim__channelCount : MediaTrackCapabilities -> PrimIO (UndefOr ULongRange)

  export
  %foreign "browser:lambda:(x,v)=>{x.channelCount = v}"
  prim__setChannelCount :  MediaTrackCapabilities
                        -> UndefOr ULongRange
                        -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.deviceId"
  prim__deviceId : MediaTrackCapabilities -> PrimIO (UndefOr String)

  export
  %foreign "browser:lambda:(x,v)=>{x.deviceId = v}"
  prim__setDeviceId : MediaTrackCapabilities -> UndefOr String -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.echoCancellation"
  prim__echoCancellation :  MediaTrackCapabilities
                         -> PrimIO (UndefOr (Array Boolean))

  export
  %foreign "browser:lambda:(x,v)=>{x.echoCancellation = v}"
  prim__setEchoCancellation :  MediaTrackCapabilities
                            -> UndefOr (Array Boolean)
                            -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.facingMode"
  prim__facingMode : MediaTrackCapabilities -> PrimIO (UndefOr (Array String))

  export
  %foreign "browser:lambda:(x,v)=>{x.facingMode = v}"
  prim__setFacingMode :  MediaTrackCapabilities
                      -> UndefOr (Array String)
                      -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.frameRate"
  prim__frameRate : MediaTrackCapabilities -> PrimIO (UndefOr DoubleRange)

  export
  %foreign "browser:lambda:(x,v)=>{x.frameRate = v}"
  prim__setFrameRate :  MediaTrackCapabilities
                     -> UndefOr DoubleRange
                     -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.groupId"
  prim__groupId : MediaTrackCapabilities -> PrimIO (UndefOr String)

  export
  %foreign "browser:lambda:(x,v)=>{x.groupId = v}"
  prim__setGroupId : MediaTrackCapabilities -> UndefOr String -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.height"
  prim__height : MediaTrackCapabilities -> PrimIO (UndefOr ULongRange)

  export
  %foreign "browser:lambda:(x,v)=>{x.height = v}"
  prim__setHeight : MediaTrackCapabilities -> UndefOr ULongRange -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.latency"
  prim__latency : MediaTrackCapabilities -> PrimIO (UndefOr DoubleRange)

  export
  %foreign "browser:lambda:(x,v)=>{x.latency = v}"
  prim__setLatency : MediaTrackCapabilities -> UndefOr DoubleRange -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.noiseSuppression"
  prim__noiseSuppression :  MediaTrackCapabilities
                         -> PrimIO (UndefOr (Array Boolean))

  export
  %foreign "browser:lambda:(x,v)=>{x.noiseSuppression = v}"
  prim__setNoiseSuppression :  MediaTrackCapabilities
                            -> UndefOr (Array Boolean)
                            -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.resizeMode"
  prim__resizeMode : MediaTrackCapabilities -> PrimIO (UndefOr (Array String))

  export
  %foreign "browser:lambda:(x,v)=>{x.resizeMode = v}"
  prim__setResizeMode :  MediaTrackCapabilities
                      -> UndefOr (Array String)
                      -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.sampleRate"
  prim__sampleRate : MediaTrackCapabilities -> PrimIO (UndefOr ULongRange)

  export
  %foreign "browser:lambda:(x,v)=>{x.sampleRate = v}"
  prim__setSampleRate :  MediaTrackCapabilities
                      -> UndefOr ULongRange
                      -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.sampleSize"
  prim__sampleSize : MediaTrackCapabilities -> PrimIO (UndefOr ULongRange)

  export
  %foreign "browser:lambda:(x,v)=>{x.sampleSize = v}"
  prim__setSampleSize :  MediaTrackCapabilities
                      -> UndefOr ULongRange
                      -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.width"
  prim__width : MediaTrackCapabilities -> PrimIO (UndefOr ULongRange)

  export
  %foreign "browser:lambda:(x,v)=>{x.width = v}"
  prim__setWidth : MediaTrackCapabilities -> UndefOr ULongRange -> PrimIO ()

namespace MediaTrackConstraintSet

  export
  %foreign "browser:lambda:(a,b,c,d,e,f,g,h,i,j,k,l,m,n,o)=> {width: a,height: b,aspectRatio: c,frameRate: d,facingMode: e,resizeMode: f,sampleRate: g,sampleSize: h,echoCancellation: i,autoGainControl: j,noiseSuppression: k,latency: l,channelCount: m,deviceId: n,groupId: o}"
  prim__new :  UndefOr (Union2 Bits32 ConstrainULongRange)
            -> UndefOr (Union2 Bits32 ConstrainULongRange)
            -> UndefOr (Union2 Double ConstrainDoubleRange)
            -> UndefOr (Union2 Double ConstrainDoubleRange)
            -> UndefOr (Union3 String
                               (Array String)
                               ConstrainDOMStringParameters)
            -> UndefOr (Union3 String
                               (Array String)
                               ConstrainDOMStringParameters)
            -> UndefOr (Union2 Bits32 ConstrainULongRange)
            -> UndefOr (Union2 Bits32 ConstrainULongRange)
            -> UndefOr (Union2 Boolean ConstrainBooleanParameters)
            -> UndefOr (Union2 Boolean ConstrainBooleanParameters)
            -> UndefOr (Union2 Boolean ConstrainBooleanParameters)
            -> UndefOr (Union2 Double ConstrainDoubleRange)
            -> UndefOr (Union2 Bits32 ConstrainULongRange)
            -> UndefOr (Union3 String
                               (Array String)
                               ConstrainDOMStringParameters)
            -> UndefOr (Union3 String
                               (Array String)
                               ConstrainDOMStringParameters)
            -> PrimIO MediaTrackConstraintSet

  export
  %foreign "browser:lambda:x=>x.aspectRatio"
  prim__aspectRatio :  MediaTrackConstraintSet
                    -> PrimIO (UndefOr (Union2 Double ConstrainDoubleRange))

  export
  %foreign "browser:lambda:(x,v)=>{x.aspectRatio = v}"
  prim__setAspectRatio :  MediaTrackConstraintSet
                       -> UndefOr (Union2 Double ConstrainDoubleRange)
                       -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.autoGainControl"
  prim__autoGainControl :  MediaTrackConstraintSet
                        -> PrimIO (UndefOr (Union2 Boolean
                                                   ConstrainBooleanParameters))

  export
  %foreign "browser:lambda:(x,v)=>{x.autoGainControl = v}"
  prim__setAutoGainControl :  MediaTrackConstraintSet
                           -> UndefOr (Union2 Boolean
                                              ConstrainBooleanParameters)
                           -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.channelCount"
  prim__channelCount :  MediaTrackConstraintSet
                     -> PrimIO (UndefOr (Union2 Bits32 ConstrainULongRange))

  export
  %foreign "browser:lambda:(x,v)=>{x.channelCount = v}"
  prim__setChannelCount :  MediaTrackConstraintSet
                        -> UndefOr (Union2 Bits32 ConstrainULongRange)
                        -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.deviceId"
  prim__deviceId :  MediaTrackConstraintSet
                 -> PrimIO (UndefOr (Union3 String
                                            (Array String)
                                            ConstrainDOMStringParameters))

  export
  %foreign "browser:lambda:(x,v)=>{x.deviceId = v}"
  prim__setDeviceId :  MediaTrackConstraintSet
                    -> UndefOr (Union3 String
                                       (Array String)
                                       ConstrainDOMStringParameters)
                    -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.echoCancellation"
  prim__echoCancellation :  MediaTrackConstraintSet
                         -> PrimIO (UndefOr (Union2 Boolean
                                                    ConstrainBooleanParameters))

  export
  %foreign "browser:lambda:(x,v)=>{x.echoCancellation = v}"
  prim__setEchoCancellation :  MediaTrackConstraintSet
                            -> UndefOr (Union2 Boolean
                                               ConstrainBooleanParameters)
                            -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.facingMode"
  prim__facingMode :  MediaTrackConstraintSet
                   -> PrimIO (UndefOr (Union3 String
                                              (Array String)
                                              ConstrainDOMStringParameters))

  export
  %foreign "browser:lambda:(x,v)=>{x.facingMode = v}"
  prim__setFacingMode :  MediaTrackConstraintSet
                      -> UndefOr (Union3 String
                                         (Array String)
                                         ConstrainDOMStringParameters)
                      -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.frameRate"
  prim__frameRate :  MediaTrackConstraintSet
                  -> PrimIO (UndefOr (Union2 Double ConstrainDoubleRange))

  export
  %foreign "browser:lambda:(x,v)=>{x.frameRate = v}"
  prim__setFrameRate :  MediaTrackConstraintSet
                     -> UndefOr (Union2 Double ConstrainDoubleRange)
                     -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.groupId"
  prim__groupId :  MediaTrackConstraintSet
                -> PrimIO (UndefOr (Union3 String
                                           (Array String)
                                           ConstrainDOMStringParameters))

  export
  %foreign "browser:lambda:(x,v)=>{x.groupId = v}"
  prim__setGroupId :  MediaTrackConstraintSet
                   -> UndefOr (Union3 String
                                      (Array String)
                                      ConstrainDOMStringParameters)
                   -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.height"
  prim__height :  MediaTrackConstraintSet
               -> PrimIO (UndefOr (Union2 Bits32 ConstrainULongRange))

  export
  %foreign "browser:lambda:(x,v)=>{x.height = v}"
  prim__setHeight :  MediaTrackConstraintSet
                  -> UndefOr (Union2 Bits32 ConstrainULongRange)
                  -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.latency"
  prim__latency :  MediaTrackConstraintSet
                -> PrimIO (UndefOr (Union2 Double ConstrainDoubleRange))

  export
  %foreign "browser:lambda:(x,v)=>{x.latency = v}"
  prim__setLatency :  MediaTrackConstraintSet
                   -> UndefOr (Union2 Double ConstrainDoubleRange)
                   -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.noiseSuppression"
  prim__noiseSuppression :  MediaTrackConstraintSet
                         -> PrimIO (UndefOr (Union2 Boolean
                                                    ConstrainBooleanParameters))

  export
  %foreign "browser:lambda:(x,v)=>{x.noiseSuppression = v}"
  prim__setNoiseSuppression :  MediaTrackConstraintSet
                            -> UndefOr (Union2 Boolean
                                               ConstrainBooleanParameters)
                            -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.resizeMode"
  prim__resizeMode :  MediaTrackConstraintSet
                   -> PrimIO (UndefOr (Union3 String
                                              (Array String)
                                              ConstrainDOMStringParameters))

  export
  %foreign "browser:lambda:(x,v)=>{x.resizeMode = v}"
  prim__setResizeMode :  MediaTrackConstraintSet
                      -> UndefOr (Union3 String
                                         (Array String)
                                         ConstrainDOMStringParameters)
                      -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.sampleRate"
  prim__sampleRate :  MediaTrackConstraintSet
                   -> PrimIO (UndefOr (Union2 Bits32 ConstrainULongRange))

  export
  %foreign "browser:lambda:(x,v)=>{x.sampleRate = v}"
  prim__setSampleRate :  MediaTrackConstraintSet
                      -> UndefOr (Union2 Bits32 ConstrainULongRange)
                      -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.sampleSize"
  prim__sampleSize :  MediaTrackConstraintSet
                   -> PrimIO (UndefOr (Union2 Bits32 ConstrainULongRange))

  export
  %foreign "browser:lambda:(x,v)=>{x.sampleSize = v}"
  prim__setSampleSize :  MediaTrackConstraintSet
                      -> UndefOr (Union2 Bits32 ConstrainULongRange)
                      -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.width"
  prim__width :  MediaTrackConstraintSet
              -> PrimIO (UndefOr (Union2 Bits32 ConstrainULongRange))

  export
  %foreign "browser:lambda:(x,v)=>{x.width = v}"
  prim__setWidth :  MediaTrackConstraintSet
                 -> UndefOr (Union2 Bits32 ConstrainULongRange)
                 -> PrimIO ()

namespace MediaTrackConstraints

  export
  %foreign "browser:lambda:(a)=> {advanced: a}"
  prim__new :  UndefOr (Array MediaTrackConstraintSet)
            -> PrimIO MediaTrackConstraints

  export
  %foreign "browser:lambda:x=>x.advanced"
  prim__advanced :  MediaTrackConstraints
                 -> PrimIO (UndefOr (Array MediaTrackConstraintSet))

  export
  %foreign "browser:lambda:(x,v)=>{x.advanced = v}"
  prim__setAdvanced :  MediaTrackConstraints
                    -> UndefOr (Array MediaTrackConstraintSet)
                    -> PrimIO ()

namespace MediaTrackSettings

  export
  %foreign "browser:lambda:(a,b,c,d,e,f,g,h,i,j,k,l,m,n,o)=> {width: a,height: b,aspectRatio: c,frameRate: d,facingMode: e,resizeMode: f,sampleRate: g,sampleSize: h,echoCancellation: i,autoGainControl: j,noiseSuppression: k,latency: l,channelCount: m,deviceId: n,groupId: o}"
  prim__new :  UndefOr Int32
            -> UndefOr Int32
            -> UndefOr Double
            -> UndefOr Double
            -> UndefOr String
            -> UndefOr String
            -> UndefOr Int32
            -> UndefOr Int32
            -> UndefOr Boolean
            -> UndefOr Boolean
            -> UndefOr Boolean
            -> UndefOr Double
            -> UndefOr Int32
            -> UndefOr String
            -> UndefOr String
            -> PrimIO MediaTrackSettings

  export
  %foreign "browser:lambda:x=>x.aspectRatio"
  prim__aspectRatio : MediaTrackSettings -> PrimIO (UndefOr Double)

  export
  %foreign "browser:lambda:(x,v)=>{x.aspectRatio = v}"
  prim__setAspectRatio : MediaTrackSettings -> UndefOr Double -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.autoGainControl"
  prim__autoGainControl : MediaTrackSettings -> PrimIO (UndefOr Boolean)

  export
  %foreign "browser:lambda:(x,v)=>{x.autoGainControl = v}"
  prim__setAutoGainControl : MediaTrackSettings -> UndefOr Boolean -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.channelCount"
  prim__channelCount : MediaTrackSettings -> PrimIO (UndefOr Int32)

  export
  %foreign "browser:lambda:(x,v)=>{x.channelCount = v}"
  prim__setChannelCount : MediaTrackSettings -> UndefOr Int32 -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.deviceId"
  prim__deviceId : MediaTrackSettings -> PrimIO (UndefOr String)

  export
  %foreign "browser:lambda:(x,v)=>{x.deviceId = v}"
  prim__setDeviceId : MediaTrackSettings -> UndefOr String -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.echoCancellation"
  prim__echoCancellation : MediaTrackSettings -> PrimIO (UndefOr Boolean)

  export
  %foreign "browser:lambda:(x,v)=>{x.echoCancellation = v}"
  prim__setEchoCancellation : MediaTrackSettings -> UndefOr Boolean -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.facingMode"
  prim__facingMode : MediaTrackSettings -> PrimIO (UndefOr String)

  export
  %foreign "browser:lambda:(x,v)=>{x.facingMode = v}"
  prim__setFacingMode : MediaTrackSettings -> UndefOr String -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.frameRate"
  prim__frameRate : MediaTrackSettings -> PrimIO (UndefOr Double)

  export
  %foreign "browser:lambda:(x,v)=>{x.frameRate = v}"
  prim__setFrameRate : MediaTrackSettings -> UndefOr Double -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.groupId"
  prim__groupId : MediaTrackSettings -> PrimIO (UndefOr String)

  export
  %foreign "browser:lambda:(x,v)=>{x.groupId = v}"
  prim__setGroupId : MediaTrackSettings -> UndefOr String -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.height"
  prim__height : MediaTrackSettings -> PrimIO (UndefOr Int32)

  export
  %foreign "browser:lambda:(x,v)=>{x.height = v}"
  prim__setHeight : MediaTrackSettings -> UndefOr Int32 -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.latency"
  prim__latency : MediaTrackSettings -> PrimIO (UndefOr Double)

  export
  %foreign "browser:lambda:(x,v)=>{x.latency = v}"
  prim__setLatency : MediaTrackSettings -> UndefOr Double -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.noiseSuppression"
  prim__noiseSuppression : MediaTrackSettings -> PrimIO (UndefOr Boolean)

  export
  %foreign "browser:lambda:(x,v)=>{x.noiseSuppression = v}"
  prim__setNoiseSuppression : MediaTrackSettings -> UndefOr Boolean -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.resizeMode"
  prim__resizeMode : MediaTrackSettings -> PrimIO (UndefOr String)

  export
  %foreign "browser:lambda:(x,v)=>{x.resizeMode = v}"
  prim__setResizeMode : MediaTrackSettings -> UndefOr String -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.sampleRate"
  prim__sampleRate : MediaTrackSettings -> PrimIO (UndefOr Int32)

  export
  %foreign "browser:lambda:(x,v)=>{x.sampleRate = v}"
  prim__setSampleRate : MediaTrackSettings -> UndefOr Int32 -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.sampleSize"
  prim__sampleSize : MediaTrackSettings -> PrimIO (UndefOr Int32)

  export
  %foreign "browser:lambda:(x,v)=>{x.sampleSize = v}"
  prim__setSampleSize : MediaTrackSettings -> UndefOr Int32 -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.width"
  prim__width : MediaTrackSettings -> PrimIO (UndefOr Int32)

  export
  %foreign "browser:lambda:(x,v)=>{x.width = v}"
  prim__setWidth : MediaTrackSettings -> UndefOr Int32 -> PrimIO ()

namespace MediaTrackSupportedConstraints

  export
  %foreign "browser:lambda:(a,b,c,d,e,f,g,h,i,j,k,l,m,n,o)=> {width: a,height: b,aspectRatio: c,frameRate: d,facingMode: e,resizeMode: f,sampleRate: g,sampleSize: h,echoCancellation: i,autoGainControl: j,noiseSuppression: k,latency: l,channelCount: m,deviceId: n,groupId: o}"
  prim__new :  UndefOr Boolean
            -> UndefOr Boolean
            -> UndefOr Boolean
            -> UndefOr Boolean
            -> UndefOr Boolean
            -> UndefOr Boolean
            -> UndefOr Boolean
            -> UndefOr Boolean
            -> UndefOr Boolean
            -> UndefOr Boolean
            -> UndefOr Boolean
            -> UndefOr Boolean
            -> UndefOr Boolean
            -> UndefOr Boolean
            -> UndefOr Boolean
            -> PrimIO MediaTrackSupportedConstraints

  export
  %foreign "browser:lambda:x=>x.aspectRatio"
  prim__aspectRatio : MediaTrackSupportedConstraints -> PrimIO (UndefOr Boolean)

  export
  %foreign "browser:lambda:(x,v)=>{x.aspectRatio = v}"
  prim__setAspectRatio :  MediaTrackSupportedConstraints
                       -> UndefOr Boolean
                       -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.autoGainControl"
  prim__autoGainControl :  MediaTrackSupportedConstraints
                        -> PrimIO (UndefOr Boolean)

  export
  %foreign "browser:lambda:(x,v)=>{x.autoGainControl = v}"
  prim__setAutoGainControl :  MediaTrackSupportedConstraints
                           -> UndefOr Boolean
                           -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.channelCount"
  prim__channelCount :  MediaTrackSupportedConstraints
                     -> PrimIO (UndefOr Boolean)

  export
  %foreign "browser:lambda:(x,v)=>{x.channelCount = v}"
  prim__setChannelCount :  MediaTrackSupportedConstraints
                        -> UndefOr Boolean
                        -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.deviceId"
  prim__deviceId : MediaTrackSupportedConstraints -> PrimIO (UndefOr Boolean)

  export
  %foreign "browser:lambda:(x,v)=>{x.deviceId = v}"
  prim__setDeviceId :  MediaTrackSupportedConstraints
                    -> UndefOr Boolean
                    -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.echoCancellation"
  prim__echoCancellation :  MediaTrackSupportedConstraints
                         -> PrimIO (UndefOr Boolean)

  export
  %foreign "browser:lambda:(x,v)=>{x.echoCancellation = v}"
  prim__setEchoCancellation :  MediaTrackSupportedConstraints
                            -> UndefOr Boolean
                            -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.facingMode"
  prim__facingMode : MediaTrackSupportedConstraints -> PrimIO (UndefOr Boolean)

  export
  %foreign "browser:lambda:(x,v)=>{x.facingMode = v}"
  prim__setFacingMode :  MediaTrackSupportedConstraints
                      -> UndefOr Boolean
                      -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.frameRate"
  prim__frameRate : MediaTrackSupportedConstraints -> PrimIO (UndefOr Boolean)

  export
  %foreign "browser:lambda:(x,v)=>{x.frameRate = v}"
  prim__setFrameRate :  MediaTrackSupportedConstraints
                     -> UndefOr Boolean
                     -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.groupId"
  prim__groupId : MediaTrackSupportedConstraints -> PrimIO (UndefOr Boolean)

  export
  %foreign "browser:lambda:(x,v)=>{x.groupId = v}"
  prim__setGroupId :  MediaTrackSupportedConstraints
                   -> UndefOr Boolean
                   -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.height"
  prim__height : MediaTrackSupportedConstraints -> PrimIO (UndefOr Boolean)

  export
  %foreign "browser:lambda:(x,v)=>{x.height = v}"
  prim__setHeight :  MediaTrackSupportedConstraints
                  -> UndefOr Boolean
                  -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.latency"
  prim__latency : MediaTrackSupportedConstraints -> PrimIO (UndefOr Boolean)

  export
  %foreign "browser:lambda:(x,v)=>{x.latency = v}"
  prim__setLatency :  MediaTrackSupportedConstraints
                   -> UndefOr Boolean
                   -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.noiseSuppression"
  prim__noiseSuppression :  MediaTrackSupportedConstraints
                         -> PrimIO (UndefOr Boolean)

  export
  %foreign "browser:lambda:(x,v)=>{x.noiseSuppression = v}"
  prim__setNoiseSuppression :  MediaTrackSupportedConstraints
                            -> UndefOr Boolean
                            -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.resizeMode"
  prim__resizeMode : MediaTrackSupportedConstraints -> PrimIO (UndefOr Boolean)

  export
  %foreign "browser:lambda:(x,v)=>{x.resizeMode = v}"
  prim__setResizeMode :  MediaTrackSupportedConstraints
                      -> UndefOr Boolean
                      -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.sampleRate"
  prim__sampleRate : MediaTrackSupportedConstraints -> PrimIO (UndefOr Boolean)

  export
  %foreign "browser:lambda:(x,v)=>{x.sampleRate = v}"
  prim__setSampleRate :  MediaTrackSupportedConstraints
                      -> UndefOr Boolean
                      -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.sampleSize"
  prim__sampleSize : MediaTrackSupportedConstraints -> PrimIO (UndefOr Boolean)

  export
  %foreign "browser:lambda:(x,v)=>{x.sampleSize = v}"
  prim__setSampleSize :  MediaTrackSupportedConstraints
                      -> UndefOr Boolean
                      -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.width"
  prim__width : MediaTrackSupportedConstraints -> PrimIO (UndefOr Boolean)

  export
  %foreign "browser:lambda:(x,v)=>{x.width = v}"
  prim__setWidth :  MediaTrackSupportedConstraints
                 -> UndefOr Boolean
                 -> PrimIO ()

namespace Settings

  export
  %foreign "browser:lambda:()=> {}"
  prim__new : PrimIO Settings

namespace ULongRange

  export
  %foreign "browser:lambda:(a,b)=> {max: a,min: b}"
  prim__new : UndefOr Bits32 -> UndefOr Bits32 -> PrimIO ULongRange

  export
  %foreign "browser:lambda:x=>x.max"
  prim__max : ULongRange -> PrimIO (UndefOr Bits32)

  export
  %foreign "browser:lambda:(x,v)=>{x.max = v}"
  prim__setMax : ULongRange -> UndefOr Bits32 -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.min"
  prim__min : ULongRange -> PrimIO (UndefOr Bits32)

  export
  %foreign "browser:lambda:(x,v)=>{x.min = v}"
  prim__setMin : ULongRange -> UndefOr Bits32 -> PrimIO ()

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

namespace NavigatorUserMediaErrorCallback

  export
  %foreign "browser:lambda:x=>(a)=>x(a)()"
  prim__toNavigatorUserMediaErrorCallback :  ( DOMException -> IO () )
                                          -> PrimIO NavigatorUserMediaErrorCallback

namespace NavigatorUserMediaSuccessCallback

  export
  %foreign "browser:lambda:x=>(a)=>x(a)()"
  prim__toNavigatorUserMediaSuccessCallback :  ( MediaStream -> IO () )
                                            -> PrimIO NavigatorUserMediaSuccessCallback


text:
module Verpackung.IOEither

public export
data IOEither a b
 = MkIOEither (IO (Either a b))

export
Functor (IOEither a) where
  map func (MkIOEither x) = MkIOEither (map (map func) x)

||| Lift a two-argument function to an applicative
export
liftA2 : Applicative f => (a -> b -> c) -> f a -> f b -> f c
liftA2 f a b = (map f a) <*> b

export
Applicative (IOEither a) where
  pure x = MkIOEither (pure (pure x))
  (<*>) (MkIOEither x) (MkIOEither y) = MkIOEither (liftA2 (<*>) x y)

export
Monad (IOEither a) where
  (>>=) (MkIOEither x) f = MkIOEither (do x' <- x
                                          (case x' of
                                                (Left l) => pure (Left l)
                                                (Right r) => let MkIOEither g = f r in
                                                                 g))
  join x = x >>= id

export
liftEither : Either e a -> IOEither e a
liftEither = MkIOEither . pure

export
liftIO : IO a -> IOEither e a
liftIO x = MkIOEither $ do
  x' <- x
  pure $ pure x'

export
liftIOEither : IOEither e a -> IO (Either e a)
liftIOEither (MkIOEither x) = x

export
mapErr : (e -> e') -> IOEither e a -> IOEither e' a
mapErr f (MkIOEither x) = MkIOEither (do
  x' <- x
  case x' of
        (Left l) => pure (Left (f l))
        (Right r) => pure (Right r))

ext: idr

max_stars_repo_name: alexhumphreys/verpackung

max_issues_repo_name: alexhumphreys/verpackung

max_forks_repo_name: alexhumphreys/verpackung


text:
import System.Signal
import System

main : IO ()
main = do
  Right () <- ignoreSignal SigABRT
    | Left (Error code) => putStrLn $ "error " ++ (show code)
  putStrLn "before"
  Right () <- raiseSignal SigABRT
    | Left (Error code) => putStrLn $ "received error code from signal call: " ++ (show code)
  sleep 1
  putStrLn "after"
  Right () <- defaultSignal SigABRT
    | Left (Error code) => putStrLn $ "error " ++ (show code)
  putStrLn "done."


text:
{-
Copyright 2020, Mokshasoft AB (mokshasoft.com)

This software may be distributed and modified according to the terms of
the BSD 2-Clause license. Note that NO WARRANTY is provided.
See "LICENSE_BSD2.txt" for details.
-}

module FreeRTOS.Queue

%default total

%include C "FreeRTOS/idris_FreeRTOS.h"
%include C "idris_rts.h"

||| A handle to a queue
export
data QueueHandle : Type -> Type where
    MkQueueHandle : (handle : Ptr) -> QueueHandle itemType

||| Create a queue.
export
create : (itemType : Type) -> Int -> IO (Maybe (QueueHandle itemType))
create _ len = do
    ptr <- foreign FFI_C "wrapper_xQueueCreate" (Int -> IO Ptr) len
    if !(nullPtr ptr)
        then pure Nothing
        else pure (Just (MkQueueHandle ptr))

||| Delete a queue.
export
delete : QueueHandle itemType -> IO ()
delete (MkQueueHandle handle) =
    foreign FFI_C "wrapper_vQueueDelete" (Ptr -> IO ()) handle

||| Put an element at the end of the queue, block until not full.
export
put : QueueHandle itemType -> itemType -> IO ()
put {itemType} (MkQueueHandle handle) value =
    foreign FFI_C "idris_queuePut" (Ptr -> Raw itemType -> IO ()) handle (MkRaw value)

||| Get an element from the front of the queue, block until an item is available.
export
get : QueueHandle itemType -> IO itemType
get {itemType} (MkQueueHandle handle) = do
    me <- getMyVM
    MkRaw x <- foreign FFI_C "idris_queueGet" (Ptr -> Ptr -> IO (Raw itemType)) me handle
    pure x

max_stars_repo_name: mokshasoft/FreeRTOS-community-ports

max_issues_repo_name: mokshasoft/FreeRTOS-community-ports

max_forks_repo_name: mokshasoft/FreeRTOS-community-ports


text:
||| Implementation  of ordering relations for `Fin`ite numbers
module Data.Fin.Order

import Control.Relation
import Control.Order
import Data.Fin
import Data.Fun
import Data.Rel
import Data.Nat
import Data.Nat.Order
import Decidable.Decidable

%default total

using (k : Nat)

  public export
  data FinLTE : Fin k -> Fin k -> Type where
    FromNatPrf : {m, n : Fin k} -> LTE (finToNat m) (finToNat n) -> FinLTE m n

  public export
  Transitive (Fin k) FinLTE where
    transitive (FromNatPrf xy) (FromNatPrf yz) =
      FromNatPrf $ transitive {rel = LTE} xy yz

  public export
  Reflexive (Fin k) FinLTE where
    reflexive = FromNatPrf $ reflexive {rel = LTE}

  public export
  Preorder (Fin k) FinLTE where

  public export
  Antisymmetric (Fin k) FinLTE where
    antisymmetric {x} {y} (FromNatPrf xy) (FromNatPrf yx) =
      finToNatInjective x y $
        antisymmetric {rel = LTE} xy yx

  public export
  PartialOrder (Fin k) FinLTE where

  public export
  Connex (Fin k) FinLTE where
    connex {x = FZ} _ =  Left $ FromNatPrf LTEZero
    connex {y = FZ} _ = Right $ FromNatPrf LTEZero
    connex {x = FS k} {y = FS j} prf =
      case connex {rel = FinLTE} $ prf . (cong FS) of
        Left  (FromNatPrf p) => Left  $ FromNatPrf $ LTESucc p
        Right (FromNatPrf p) => Right $ FromNatPrf $ LTESucc p

  public export
  Decidable 2 [Fin k, Fin k] FinLTE where
    decide m n with (decideLTE (finToNat m) (finToNat n))
      decide m n | Yes prf    = Yes (FromNatPrf prf)
      decide m n | No  disprf = No (\ (FromNatPrf prf) => disprf prf)


text:
%language ElabReflection

triv : Elab ()
triv =
    do
        compute
        g <- getGoal
        case (snd g) of
            `(() : Type) =>
                do
                    fill `(() : ())
                    solve
            otherGoal =>
                fail [
                    TermPart otherGoal,
                    TextPart "is not trivial"
                ]

mkId : Elab ()
mkId =
    do
        intro `{{x}}
        fill (Var `{{x}})
        solve

idNat : Nat -> Nat
idNat = %runElab mkId

idUnit : () -> ()
idUnit = %runElab mkId

idString : String -> String
idString = %runElab mkId


text:
-- ------------------------------------------------------------- [ DayTime.idr ]
||| Module    : DayTime.idr
||| Copyright : (c) Jan de Muijnck-Hughes
||| License   : see LICENSE
|||
module Commons.Data.DayTime

%default total
%access public export

-- ----------------------------------------------------------------- [ DayTime ]
||| Simple Record for DayTime
record DayTime where
  constructor MkDaytime
  year    : Int
  month   : Int
  day     : Int
  hour    : Int
  minute  : Int
  seconds : Int

Show DayTime where
    show date = unwords [show (year    date), "-",
                         show (month   date), "-",
                         show (day     date), " ",
                         show (hour    date), ":",
                         show (minute  date), ":",
                         show (seconds date) ]

-- --------------------------------------------------------------------- [ EOF ]

max_stars_repo_name: jfdm/idris-common

max_issues_repo_name: jfdm/idris-common

max_forks_repo_name: jfdm/idris-common


text:
module Text.Markup.Edda.Process.Inline

import Data.AVL.Dict

import Text.Markup.Edda.Model.Common
import Text.Markup.Edda.Model.Raw
import Text.Markup.Edda.Model.Processed

import Text.Markup.Edda.Process.Squash

%default total
%access private

treatPunc : Char -> Maybe (Edda INLINE)

treatPunc ' '  = Just Space
treatPunc '\n' = Just Newline
treatPunc '\t' = Just Tab
treatPunc '<'  = Just LAngle
treatPunc '>'  = Just RAngle
treatPunc ':'  = Just Colon
treatPunc ';'  = Just Semi
treatPunc '/'  = Just FSlash
treatPunc '\\' = Just BSlash
treatPunc '\'' = Just Apostrophe
treatPunc '-'  = Just Hyphen
treatPunc ','  = Just Comma
treatPunc '+'  = Just Plus
treatPunc '!'  = Just Bang
treatPunc '.'  = Just Period
treatPunc '?'  = Just QMark
treatPunc '#'  = Just Hash
treatPunc '='  = Just Equals
treatPunc '$'  = Just Dollar
treatPunc '|'  = Just Pipe

treatPunc '{' = Just LBrace
treatPunc '}' = Just RBrace
treatPunc '(' = Just LParen
treatPunc ')' = Just RParen
treatPunc '[' = Just LBrack
treatPunc ']' = Just RBrack
treatPunc '"' = Just SMark

treatPunc _  = Nothing

mutual
  refineInline : EddaRaw INLINE -> Edda INLINE

  refineInline (Link RefTy     url desc) = Ref url
  refineInline (Link ExposedTy url desc) = Hyper url Nil
  refineInline (Link HyperTy   url desc) = Hyper url $ refineInlines desc
  refineInline (Link FnoteTy   url desc) = FNote url $ refineInlines desc
  refineInline (Link CiteTy    url desc) = Cite ParenSty url -- <= @TODO

  refineInline (Mark BoldTy   txt) = Bold   $ refineInlines txt
  refineInline (Mark EmphTy   txt) = Emph   $ refineInlines txt
  refineInline (Mark StrikeTy txt) = Strike $ refineInlines txt
  refineInline (Mark UlineTy  txt) = Uline  $ refineInlines txt

  refineInline (Punc c) =
    case treatPunc c of
      Just p  => p
      Nothing => MiscPunc c

  refineInline (Font SerifTy s) = Text s
  refineInline (Font SansTy  s) = Sans s
  refineInline (Font ScapTy  s) = Scap s
  refineInline (Font MonoTy  s) = Mono s

  refineInline (Raw VerbTy v) = Verb v
  refineInline (Raw CodeTy v) = Code v
  refineInline (Raw MathTy v) = Math v

  refineInlines : List (EddaRaw INLINE) -> List (Edda INLINE)
  refineInlines is = map refineInline is

export
process : List (EddaRaw INLINE) -> List (Edda INLINE)
process Nil = Nil
process xs  = squash2 $ squash3 $ refineInlines xs

-- --------------------------------------------------------------------- [ EOF ]

max_stars_repo_name: jfdm/edda

max_issues_repo_name: jfdm/edda

max_forks_repo_name: jfdm/edda


text:
import Data.Vect

infixr 5 .+.

data Schema = SString
            | SInt
            | SChar
            | (.+.) Schema Schema

SchemaType : Schema -> Type
SchemaType SString = String
SchemaType SInt = Int
SchemaType SChar = Char
SchemaType (x .+. y) = (SchemaType x, SchemaType y)

record DataStore where
    constructor MkData
    schema : Schema
    size : Nat
    items : Vect size (SchemaType schema)

addToStore : (store : DataStore) -> SchemaType (schema store) -> DataStore
addToStore (MkData schema size items) newItem =
    MkData schema _ (addToData items)
    where
        addToData : Vect oldsize (SchemaType schema) -> Vect (S oldsize) (SchemaType schema)
        addToData [] = [newItem]
        addToData (x :: xs) = x :: addToData xs

display : SchemaType schema -> String
display {schema = SString} item = show item
display {schema = SInt} item = show item
display {schema = SChar} item = show item
display {schema = (y .+. z)} (itemL, itemR) = display itemL ++ ", " ++ display itemR

getEntry : (pos : Integer) -> (store : DataStore) -> Maybe (String, DataStore)
getEntry pos store =
    let store_items = items store in
        case integerToFin pos (size store) of
            Nothing => Just ("Out of range\n", store)
            Just id => Just (display (index id (items store)) ++ "\n", store)

data Command : Schema -> Type where
    SetSchema : (newSchema : Schema) -> Command schema
    Add : SchemaType schema -> Command schema
    Get : Maybe Integer -> Command schema
    Quit : Command schema

parsePrefix : (schema : Schema) -> String -> Maybe (SchemaType schema, String)
parsePrefix SString input = getQuoted (unpack input)
    where
        getQuoted : List Char -> Maybe (String, String)
        getQuoted ('"' :: xs) = case span (/= '"') xs of
                                    (quoted, '"' :: rest) => Just (pack quoted, ltrim (pack rest))
                                    _ => Nothing
        getQuoted _ = Nothing

parsePrefix SInt input = case span isDigit input of
                        ("", rest) => Nothing
                        (num, rest) => Just (cast num, ltrim rest)

parsePrefix SChar input = getChar (unpack input)
    where
        getChar : List Char -> Maybe (Char, String)
        getChar (char :: ' ' :: rest) = Just (char, pack rest)
        getChar (char :: []) = Just (char, "")
        getChar _ = Nothing

parsePrefix (schemaL .+. schemaR) input =
    do
        (lVal, input') <- parsePrefix schemaL input
        (rVal, input'') <- parsePrefix schemaR input'
        Just ((lVal, rVal), input'')

parseBySchema : (schema : Schema) -> String -> Maybe (SchemaType schema)
parseBySchema schema input = case parsePrefix schema input of
                                Just (res, "") => Just res
                                Just _ => Nothing
                                Nothing => Nothing

parseSchema : List String -> Maybe Schema
parseSchema ("String" :: xs) =
    case xs of
        [] => Just SString
        _ =>
            do
                restSchema <- parseSchema xs
                Just (SString .+. restSchema)
parseSchema ("Int" :: xs) =
    case xs of
        [] => Just SInt
        _ =>
            do
                restSchema <- parseSchema xs
                Just (SInt .+. restSchema)
parseSchema ("Char" :: xs) =
    case xs of
        [] => Just SChar
        _ =>
            do
                restSchema <- parseSchema xs
                Just (SChar .+. restSchema)
parseSchema _ = Nothing

parseCommand : (schema : Schema) -> String -> String -> Maybe (Command schema)
parseCommand schema "add" rest =
    do
        restOk <- parseBySchema schema rest
        Just (Add restOk)
parseCommand schema "get" "" = Just (Get Nothing)
parseCommand schema "get" val =
    case all isDigit (unpack val) of
        False => Nothing
        True => Just (Get $ Just (cast val))
parseCommand schema "schema" val =
    do
        schemaok <- parseSchema (words val)
        Just (SetSchema schemaok)
parseCommand schema "quit" "" = Just Quit
parseCommand _ _ _ = Nothing

parse : (schema : Schema) -> (input : String) -> Maybe (Command schema)
parse schema input = case span (/= ' ') input of
                        (cmd, args) => parseCommand schema cmd (ltrim args)

setSchema : (store : DataStore) -> Schema -> Maybe DataStore
setSchema store schema = case size store of
                            Z => Just (MkData schema _ [])
                            S k => Nothing

showItems : Vect len (SchemaType schema) -> String
showItems [] = ""
showItems (item :: items') = display item ++ "\n" ++ showItems items'

processInput : DataStore -> String -> Maybe (String, DataStore)
processInput store input
    = case parse (schema store) input of
            Nothing => Just ("Invalid command\n", store)
            Just (Add item) =>
                Just ("ID " ++ show (size store) ++ "\n", addToStore store item)
            Just (Get Nothing) => Just (showItems $ items store, store)
            Just (Get $ Just pos) => getEntry pos store
            Just (SetSchema schema') =>
                case setSchema store schema' of
                    Nothing => Just ("Can't update schema\n", store)
                    Just store' => Just ("OK\n", store')
            Just Quit => Nothing

main : IO ()
main = replWith (MkData (SString .+. SInt) _ []) "Command: " processInput


text:
module Data.Time.Clock.AbsoluteTime

import Data.Fixed
import Data.Time.Calendar.Days
import Data.Time.Clock.DiffTime

import Generics.Derive

%default total
%language ElabReflection

-- --------------------------------------------------------------------------

export data AbsoluteTime = MkAbsoluteTime DiffTime
%runElab derive "AbsoluteTime" [Generic, Eq, Ord, DecEq]

||| The epoch of TAI, which is 1858-11-17 00:00:00 TAI.
export taiEpoch : AbsoluteTime
taiEpoch = MkAbsoluteTime 0

export taiNominalDayStart : Day -> AbsoluteTime
taiNominalDayStart day =
  MkAbsoluteTime $ SecondsToDiffTime $ cast $ day.modifiedJulianDay * 86400

||| addAbsoluteTime a b = a + b
export addAbsoluteTime : DiffTime -> AbsoluteTime -> AbsoluteTime
addAbsoluteTime t (MkAbsoluteTime a) = MkAbsoluteTime (a + t)

||| diffAbsoluteTime a b = a - b
export diffAbsoluteTime : AbsoluteTime -> AbsoluteTime -> DiffTime
diffAbsoluteTime (MkAbsoluteTime a) (MkAbsoluteTime b) = a - b

-- --------------------------------------------------------------------------
-- vim: tw=80 sw=2 expandtab :


text:
-- Namespaces are currently allowed to be empty, as modules are, but also
-- require their contents to be indented to denote where they end.
-- Whereas a module's end is the end of the file.

-- Since there's no indentation each namespace ends imediately. So each Test
-- defines things at the module level, causing an `already defined` error.

namespace X
private
data Test = A | B

namespace Y
private
data Test = A | B


text:
module Main

import Average

toLine : String -> String
toLine = (++ "\n")

main : IO ()
main = repl prompt $ toLine . (outputPrefix ++) . show . averageWordLen
        where
            prompt = "Enter a String: "
            outputPrefix = "The average word length is "


text:
module Data.Utils

import Data.Bits
import Data.Buffer
import Data.Vect

export
enumerateVect : {n : Nat} -> Vect n a -> Vect n (Int, a)
enumerateVect l = enumerate' 0 l where
  enumerate' : {n : Nat} -> Int -> Vect n a -> Vect n (Int, a)
  enumerate' _ [] = []
  enumerate' i (x::xs) = (i, x)::(enumerate' (i+1) xs)

export
enumerate : List a -> List (Int, a)
enumerate l = enumerate' 0 l where
  enumerate' : Int -> List a -> List (Int, a)
  enumerate' _ [] = []
  enumerate' i (x::xs) = (i, x)::(enumerate' (i+1) xs)

hexDigit : Bits64 -> Char
hexDigit 0 = '0'
hexDigit 1 = '1'
hexDigit 2 = '2'
hexDigit 3 = '3'
hexDigit 4 = '4'
hexDigit 5 = '5'
hexDigit 6 = '6'
hexDigit 7 = '7'
hexDigit 8 = '8'
hexDigit 9 = '9'
hexDigit 10 = 'a'
hexDigit 11 = 'b'
hexDigit 12 = 'c'
hexDigit 13 = 'd'
hexDigit 14 = 'e'
hexDigit 15 = 'f'
hexDigit _ = 'X' -- TMP HACK: Ideally we'd have a bounds proof, generated below

export
asHex : Bits64 -> String
asHex 0 = "0"
asHex n = pack $ asHex' n []
  where
    asHex' : Bits64 -> List Char -> List Char
    asHex' 0 hex = hex
    asHex' n hex = asHex' (assert_smaller n (n `shiftR` 4)) (hexDigit (n .&. 0xf) :: hex)

export
asHex2 : Int -> String
asHex2 0 = "00"
asHex2 c = let s = asHex (cast {to=Bits64} c) in
               if length s == 1 then "0" ++ s else s

export
doubleToHex : Double -> String
doubleToHex d = let bytes = unsafePerformIO (do
                                buf <- (assert_total $ fromMaybe $ idris_crash "no buf") <$> newBuffer 8
                                setDouble buf 0 d
                                bufferData buf
                                ) in
                                concatMap asHex2 $ reverse bytes

export
repeatStr : String -> Nat -> String
repeatStr s 0 = ""
repeatStr s (S x) = s ++ repeatStr s x

export
showSep : String -> List String -> String
showSep sep xs = showSepGo True xs "" where
  showSepGo : Bool -> List String -> String -> String
  showSepGo first [] acc = acc
  showSepGo first (x::xs) acc = if first then showSepGo False xs (acc ++ x)
                                         else showSepGo False xs (acc ++ sep ++ x)


text:
module Hedgehog.Internal.Util

import Data.DPair
import Data.List
import Data.Colist

%default total
--------------------------------------------------------------------------------
--          SafeDiv
--------------------------------------------------------------------------------

||| Interface providing a safe (total) division operation
||| by proving that the divisor is non-zero.
public export
interface Neg a => SafeDiv (0 a : Type) (0 pred : a -> Type) | a where
  total safeDiv' : (n,d : a) -> (0 prf : pred d) -> a

public export
SafeDiv Int (\d => d == 0 = False) where
  safeDiv' n d _ = n `div` d

public export
SafeDiv Integer (\d => d == 0 = False) where
  safeDiv' n d _ = n `div` d

public export
SafeDiv Double (\d => d == 0 = False) where
  safeDiv' n d _ = n / d

public export total
safeDiv : SafeDiv a pred => (n,d : a) -> {auto 0 ok : pred d} -> a
safeDiv n d = safeDiv' n d ok

public export total
fromPred : (a -> Bool) -> a -> Maybe a
fromPred p a = guard (p a) $> a

--------------------------------------------------------------------------------
--          ToInteger
--------------------------------------------------------------------------------

public export
interface Num a => ToInteger a where
  toInteger : a -> Integer

  toNat : a -> Nat
  toNat = integerToNat . toInteger

public export
ToInteger Integer where toInteger = id

public export
ToInteger Int8 where toInteger = cast

public export
ToInteger Int16 where toInteger = cast

public export
ToInteger Int32 where toInteger = cast

public export
ToInteger Int64 where toInteger = cast

public export
ToInteger Int where toInteger = cast

public export
ToInteger Bits8 where toInteger = cast

public export
ToInteger Bits16 where toInteger = cast

public export
ToInteger Bits32 where toInteger = cast

public export
ToInteger Bits64 where toInteger = cast

public export
ToInteger Nat where
  toInteger = cast
  toNat = id

public export
ToInteger Double where toInteger = cast

public export
fromIntegral : ToInteger a => Num b => a -> b
fromIntegral = fromInteger . toInteger

public export
round : Num a => Double -> a
round v = let f = floor v
              v' = if v - f < 0.5 then f else ceiling v
           in fromInteger $ cast v'

--------------------------------------------------------------------------------
--          (Lazy) List Utilities
--------------------------------------------------------------------------------

public export
iterateBefore : (p : a -> Bool) -> (a -> a) -> (v : a) -> Colist a
iterateBefore p f = takeBefore p . iterate f

public export
iterateBefore0 : Eq a => Num a => (a -> a) -> (start : a) -> Colist a
iterateBefore0 = iterateBefore (0 ==)

||| Prepends the first list in reverse order to the
||| second list.
public export
prepRev : List a -> List a -> List a
prepRev []        ys = ys
prepRev (x :: xs) ys = prepRev xs (x :: ys)

public export
signum : Ord a => Neg a => a -> a
signum x = if x < 0
              then (-1)
              else if x == 0 then 0 else 1

--------------------------------------------------------------------------------
--          Colists
--------------------------------------------------------------------------------

||| Cons an element on to the front of a list unless it is already there.
public export total
consNub : Eq a => a -> Colist a -> Colist a
consNub x []          = [x]
consNub x l@(y :: xs) = if x == y then l else x :: l

public export
concatColist : Colist (Colist a) -> Colist a
concatColist ((x :: xs) :: ys)       = x :: concatColist (xs :: ys)
concatColist ([] :: (x :: xs) :: ys) = x :: concatColist (xs :: ys)
concatColist _                       = []

public export
concatMapColist : (a -> Colist b) -> Colist a -> Colist b
concatMapColist f = concatColist . map f

public export
fromFoldable : Foldable f => f a -> Colist a
fromFoldable = fromList . toList

--------------------------------------------------------------------------------
--          Numeric Utilities
--------------------------------------------------------------------------------

public export
IsInUnit : Double -> Bool
IsInUnit d = 0.0 < d && d < 1.0

public export
0 InUnit : Type
InUnit = Subset Double (\x => IsInUnit x = True)

export
recipBits64 : Subset Bits64 (\x => x >= 2 = True) -> InUnit
recipBits64 (Element v _) =
  Element (1.0 / fromInteger (cast v)) (believe_me (Refl {x = True} ))

-- Algorithm taken from
-- https://web.archive.org/web/20151110174102/http://home.online.no/~pjacklam/notes/invnorm/
-- Accurate to about one part in 10^9.
--
-- The 'erf' package uses the same algorithm, but with an extra step
-- to get a fully accurate result, which we skip because it requires
-- the 'erfc' function.
export
invnormcdf : (p : InUnit) -> Double
invnormcdf (Element p _) =
  let a1 = -3.969683028665376e+01
      a2 =  2.209460984245205e+02
      a3 = -2.759285104469687e+02
      a4 =  1.383577518672690e+02
      a5 = -3.066479806614716e+01
      a6 =  2.506628277459239e+00

      b1 = -5.447609879822406e+01
      b2 =  1.615858368580409e+02
      b3 = -1.556989798598866e+02
      b4 =  6.680131188771972e+01
      b5 = -1.328068155288572e+01

      c1 = -7.784894002430293e-03
      c2 = -3.223964580411365e-01
      c3 = -2.400758277161838e+00
      c4 = -2.549732539343734e+00
      c5 =  4.374664141464968e+00
      c6 =  2.938163982698783e+00

      d1 =  7.784695709041462e-03
      d2 =  3.224671290700398e-01
      d3 =  2.445134137142996e+00
      d4 =  3.754408661907416e+00

      p_low  = 0.02425
      p_high = 1 - p_low
      q      = sqrt(-2*log(p))

   in if p < p_low
         then (((((c1*q+c2)*q+c3)*q+c4)*q+c5)*q+c6) /
              ((((d1*q+d2)*q+d3)*q+d4)*q+1)
         else
           if p <= p_high
              then
                let
                  q = p - 0.5
                  r = q*q
                in
                  (((((a1*r+a2)*r+a3)*r+a4)*r+a5)*r+a6)*q /
                  (((((b1*r+b2)*r+b3)*r+b4)*r+b5)*r+1)
              else
                let
                  q = sqrt(-2*log(1-p))
                in
                  -(((((c1*q+c2)*q+c3)*q+c4)*q+c5)*q+c6) /
                   ((((d1*q+d2)*q+d3)*q+d4)*q+1)


text:
import Data.Vect

tryIndex : {n : _} -> Integer -> Vect n a -> Maybe a
tryIndex {n} i xs = case integerToFin i n of
                         Nothing => Nothing
                         Just idx => Just (index idx xs)


text:
module System.File.Permissions

import public System.File.Error
import System.File.Meta
import System.File.Support
import public System.File.Types
import System.FFI

%default total

fileClass : String
fileClass = "io/github/mmhelloworld/idrisjvm/runtime/ChannelIo"

%foreign support "idris2_chmod"
         "node:support:chmod,support_system_file"
         jvm' fileClass "chmod" "String int" "int"
prim__chmod : String -> Int -> PrimIO Int

namespace FileMode
  public export
  data FileMode = Read | Write | Execute

public export
record Permissions where
  constructor MkPermissions
  user   : List FileMode
  group  : List FileMode
  others : List FileMode

mkMode : Permissions -> Int
mkMode p
    = getMs (user p) * 64 + getMs (group p) * 8 + getMs (others p)
  where
    getM : FileMode -> Int
    getM Read = 4
    getM Write = 2
    getM Execute = 1

    getMs : List FileMode -> Int
    getMs = sum . map getM

export
chmodRaw : HasIO io => String -> Int -> io (Either FileError ())
chmodRaw fname p
    = do ok <- primIO $ prim__chmod fname p
         if ok == 0
            then pure (Right ())
            else returnError

export
chmod : HasIO io => String -> Permissions -> io (Either FileError ())
chmod fname p = chmodRaw fname (mkMode p)


text:
module Core.Name

import Data.List
import Data.String
import Data.Maybe
import Decidable.Equality
import Libraries.Text.PrettyPrint.Prettyprinter
import Libraries.Text.PrettyPrint.Prettyprinter.Util
import Libraries.Utils.String

import public Core.Name.Namespace

%default total

||| A username has some structure
public export
data UserName : Type where
  Basic : String -> UserName -- default name constructor       e.g. map
  Field : String -> UserName -- field accessor                 e.g. .fst
  Underscore : UserName      -- no name                        e.g. _

||| A smart constructor taking a string and parsing it as the appropriate
||| username
export
mkUserName : String -> UserName
mkUserName "_" = Underscore
mkUserName str with (strM str)
  mkUserName _   | StrCons '.' n = Field n
  mkUserName str | _             = Basic str

||| Name helps us track a name's structure as well as its origin:
||| was it user-provided or machine-manufactured? For what reason?
public export
data Name : Type where
     NS : Namespace -> Name -> Name -- in a namespace
     UN : UserName -> Name -- user defined name
     MN : String -> Int -> Name -- machine generated name
     PV : Name -> Int -> Name -- pattern variable name; int is the resolved function id
     DN : String -> Name -> Name -- a name and how to display it
     Nested : (Int, Int) -> Name -> Name -- nested function name
     CaseBlock : String -> Int -> Name -- case block nested in (resolved) name
     WithBlock : String -> Int -> Name -- with block nested in (resolved) name
     Resolved : Int -> Name -- resolved, index into context

export
mkNamespacedName : Maybe Namespace -> UserName -> Name
mkNamespacedName Nothing nm = UN nm
mkNamespacedName (Just ns) nm = NS ns (UN nm)

||| `matches a b` checks that the name `a` matches `b` assuming
||| the name roots are already known to be matching.
||| For instance, both `reverse` and `List.reverse` match the fully
||| qualified name `Data.List.reverse`.
export
matches : Name -> Name -> Bool
matches (NS ns _) (NS cns _) = isApproximationOf ns cns
matches (NS _ _) _
  -- gallais: I don't understand this case but that's what was there.
  = True -- no in library name, so root doesn't match
matches _ _ = True -- no prefix, so root must match, so good

-- Update a name imported with 'import as', for creating an alias
export
asName : ModuleIdent -> -- Initial module name
         Namespace -> -- 'as' module name
         Name -> -- identifier
         Name
asName old new (DN s n) = DN s (asName old new n)
asName old new (NS ns n)
    = NS (replace old new ns) n
asName _ _ n = n

export
userNameRoot : Name -> Maybe UserName
userNameRoot (NS _ n) = userNameRoot n
userNameRoot (UN n) = Just n
userNameRoot (DN _ n) = userNameRoot n
userNameRoot _ = Nothing

export
isUnderscoreName : Name -> Bool
isUnderscoreName (UN Underscore) = True
isUnderscoreName (MN "_" _) = True
isUnderscoreName _ = False

export
isPatternVariable : UserName -> Bool
isPatternVariable (Basic nm) = lowerFirst nm
isPatternVariable (Field _) = False
isPatternVariable Underscore = True

export
isUserName : Name -> Bool
isUserName (PV _ _) = False
isUserName (MN _ _) = False
isUserName (NS _ n) = isUserName n
isUserName (DN _ n) = isUserName n
isUserName _ = True

||| True iff name can be traced back to a source name.
||| Used to determine whether it needs semantic highlighting.
export
isSourceName : Name -> Bool
isSourceName (NS _ n) = isSourceName n
isSourceName (UN _) = True
isSourceName (MN _ _) = False
isSourceName (PV n _) = isSourceName n
isSourceName (DN _ n) = isSourceName n
isSourceName (Nested _ n) = isSourceName n
isSourceName (CaseBlock _ _) = False
isSourceName (WithBlock _ _) = False
isSourceName (Resolved _) = False

export
isRF : Name -> Maybe (Namespace, String)
isRF (NS ns n) = map (mapFst (ns <.>)) (isRF n)
isRF (UN (Field n)) = Just (emptyNS, n)
isRF _ = Nothing

export
isUN : Name -> Maybe UserName
isUN (UN un) = Just un
isUN _ = Nothing

export
isBasic : UserName -> Maybe String
isBasic (Basic str) = Just str
isBasic _ = Nothing

export
displayUserName : UserName -> String
displayUserName (Basic n) = n
displayUserName (Field n) = n
displayUserName Underscore = "_"

export
nameRoot : Name -> String
nameRoot (NS _ n) = nameRoot n
nameRoot (UN n) = displayUserName n
nameRoot (MN n _) = n
nameRoot (PV n _) = nameRoot n
nameRoot (DN _ n) = nameRoot n
nameRoot (Nested _ inner) = nameRoot inner
nameRoot (CaseBlock n _) = "$" ++ show n
nameRoot (WithBlock n _) = "$" ++ show n
nameRoot (Resolved i) = "$" ++ show i

export
displayName : Name -> (Maybe Namespace, String)
displayName (NS ns n) = mapFst (pure . maybe ns (ns <.>)) $ displayName n
displayName (UN n) = (Nothing, displayUserName n)
displayName (MN n _) = (Nothing, n)
displayName (PV n _) = displayName n
displayName (DN n _) = (Nothing, n)
displayName (Nested _ n) = displayName n
displayName (CaseBlock outer _) = (Nothing, "case block in " ++ show outer)
displayName (WithBlock outer _) = (Nothing, "with block in " ++ show outer)
displayName (Resolved i) = (Nothing, "$resolved" ++ show i)

export
splitNS : Name -> (Namespace, Name)
splitNS (NS ns nm) = mapFst (ns <.>) (splitNS nm)
splitNS nm = (emptyNS, nm)

--- Drop a namespace from a name
export
dropNS : Name -> Name
dropNS (NS _ n) = n
dropNS n = n

-- Drop all of the namespaces from a name
export
dropAllNS : Name -> Name
dropAllNS (NS _ n) = dropAllNS n
dropAllNS n = n

export
mbApplyNS : Maybe Namespace -> Name -> Name
mbApplyNS Nothing n = n
mbApplyNS (Just ns) n = NS ns n

export
isUnsafeBuiltin : Name -> Bool
isUnsafeBuiltin nm = case splitNS nm of
  (ns, UN (Basic str)) =>
       (ns == builtinNS || ns == emptyNS)
    && any {t = List} id
           [ "assert_" `isPrefixOf` str
           , str `elem` [ "prim__believe_me", "believe_me"
                        , "prim__crash", "idris_crash"
                        ]
           ]
  _ => False

export
Show UserName where
  show (Basic n) = n
  show (Field n) = "." ++ n
  show Underscore = "_"

export
Show Name where
  show (NS ns n@(UN (Field _))) = show ns ++ ".(" ++ show n ++ ")"
  show (NS ns n) = show ns ++ "." ++ show n
  show (UN x) = show x
  show (MN x y) = "{" ++ x ++ ":" ++ show y ++ "}"
  show (PV n d) = "{P:" ++ show n ++ ":" ++ show d ++ "}"
  show (DN str n) = str
  show (Nested (outer, idx) inner)
      = show outer ++ ":" ++ show idx ++ ":" ++ show inner
  show (CaseBlock outer i) = "case block in " ++ outer
  show (WithBlock outer i) = "with block in " ++ outer
  show (Resolved x) = "$resolved" ++ show x

export
[RawUN] Show UserName where
  show (Basic n) = "Basic " ++ n
  show (Field n) = "Field " ++ n
  show Underscore = "Underscore"

export
[Raw] Show Name where
  show (NS ns n) = "NS " ++ show ns ++ " (" ++ show n ++ ")"
  show (UN x) = "UN (" ++ show @{RawUN} x ++ ")"
  show (MN x y) = "MN (" ++ show x ++ ") " ++ show y
  show (PV n d) = "PV (" ++ show n ++ ") " ++ show d
  show (DN str n) = "DN " ++ str ++ " (" ++ show n ++ ")"
  show (Nested ij n) = "Nested " ++ show ij ++ " (" ++ show n ++ ")"
  show (CaseBlock str i) = "CaseBlock " ++ str ++ " " ++ show i
  show (WithBlock str i) = "CaseBlock " ++ str ++ " " ++ show i
  show (Resolved i) = "Resolved " ++ show i

export
Pretty UserName where
  pretty (Basic n) = pretty n
  pretty (Field n) = "." <+> pretty n
  pretty Underscore = "_"

export
Pretty Name where
  pretty (NS ns n@(UN (Field _))) = pretty ns <+> dot <+> parens (pretty n)
  pretty (NS ns n) = pretty ns <+> dot <+> pretty n
  pretty (UN x) = pretty x
  pretty (MN x y) = braces (pretty x <+> colon <+> pretty y)
  pretty (PV n d) = braces (pretty 'P' <+> colon <+> pretty n <+> colon <+> pretty d)
  pretty (DN str _) = pretty str
  pretty (Nested (outer, idx) inner)
    = pretty outer <+> colon <+> pretty idx <+> colon <+> pretty inner
  pretty (CaseBlock outer _) = reflow "case block in" <++> pretty outer
  pretty (WithBlock outer _) = reflow "with block in" <++> pretty outer
  pretty (Resolved x) = pretty "$resolved" <+> pretty x

export
Eq UserName where
  (==) (Basic x) (Basic y) = x == y
  (==) (Field x) (Field y) = x == y
  (==) Underscore Underscore = True
  (==) _ _ = False

export
Eq Name where
    (==) (NS ns n) (NS ns' n') = n == n' && ns == ns'
    (==) (UN x) (UN y) = x == y
    (==) (MN x y) (MN x' y') = y == y' && x == x'
    (==) (PV x y) (PV x' y') = x == x' && y == y'
    (==) (DN _ n) (DN _ n') = n == n'
    (==) (Nested x y) (Nested x' y') = x == x' && y == y'
    (==) (CaseBlock x y) (CaseBlock x' y') = y == y' && x == x'
    (==) (WithBlock x y) (WithBlock x' y') = y == y' && x == x'
    (==) (Resolved x) (Resolved x') = x == x'
    (==) _ _ = False

usernameTag : UserName -> Int
usernameTag (Basic _) = 0
usernameTag (Field _) = 2
usernameTag Underscore = 3

export
Ord UserName where
  compare (Basic x) (Basic y) = compare x y
  compare (Field x) (Field y) = compare x y
  compare Underscore Underscore = EQ
  compare x y = compare (usernameTag x) (usernameTag y)

nameTag : Name -> Int
nameTag (NS _ _) = 0
nameTag (UN _) = 1
nameTag (MN _ _) = 2
nameTag (PV _ _) = 3
nameTag (DN _ _) = 4
nameTag (Nested _ _) = 6
nameTag (CaseBlock _ _) = 7
nameTag (WithBlock _ _) = 8
nameTag (Resolved _) = 9

export
Ord Name where
    compare (NS x y) (NS x' y')
        = case compare y y' of -- Compare base name first (more likely to differ)
               EQ => compare x x'
               -- Because of the terrible way Idris 1 compiles 'case', this
               -- is actually faster than just having 't => t'...
               GT => GT
               LT => LT
    compare (UN x) (UN y) = compare x y
    compare (MN x y) (MN x' y')
        = case compare y y' of
               EQ => compare x x'
               GT => GT
               LT => LT
    compare (PV x y) (PV x' y')
        = case compare y y' of
               EQ => compare x x'
               GT => GT
               LT => LT
    compare (DN _ n) (DN _ n') = compare n n'
    compare (Nested x y) (Nested x' y')
        = case compare y y' of
               EQ => compare x x'
               GT => GT
               LT => LT
    compare (CaseBlock x y) (CaseBlock x' y')
        = case compare y y' of
               EQ => compare x x'
               GT => GT
               LT => LT
    compare (WithBlock x y) (WithBlock x' y')
        = case compare y y' of
               EQ => compare x x'
               GT => GT
               LT => LT
    compare (Resolved x) (Resolved y) = compare x y

    compare x y = compare (nameTag x) (nameTag y)

export
userNameEq : (x, y : UserName) -> Maybe (x = y)
userNameEq (Basic x) (Basic y) with (decEq x y)
  userNameEq (Basic x) (Basic y) | Yes prf = Just (cong Basic prf)
  userNameEq (Basic x) (Basic y) | No nprf = Nothing
userNameEq (Field x) (Field y) with (decEq x y)
  userNameEq (Field x) (Field y) | Yes prf = Just (cong Field prf)
  userNameEq (Field x) (Field y) | No nprf = Nothing
userNameEq Underscore Underscore = Just Refl
userNameEq _ _ = Nothing

export
nameEq : (x : Name) -> (y : Name) -> Maybe (x = y)
nameEq (NS xs x) (NS ys y) with (decEq xs ys)
  nameEq (NS ys x) (NS ys y) | (Yes Refl) with (nameEq x y)
    nameEq (NS ys x) (NS ys y) | (Yes Refl) | Nothing = Nothing
    nameEq (NS ys y) (NS ys y) | (Yes Refl) | (Just Refl) = Just Refl
  nameEq (NS xs x) (NS ys y) | (No contra) = Nothing
nameEq (UN x) (UN y) = map (cong UN) (userNameEq x y)
nameEq (MN x t) (MN x' t') with (decEq x x')
  nameEq (MN x t) (MN x t') | (Yes Refl) with (decEq t t')
    nameEq (MN x t) (MN x t) | (Yes Refl) | (Yes Refl) = Just Refl
    nameEq (MN x t) (MN x t') | (Yes Refl) | (No contra) = Nothing
  nameEq (MN x t) (MN x' t') | (No contra) = Nothing
nameEq (PV x t) (PV y t') with (nameEq x y)
  nameEq (PV y t) (PV y t') | (Just Refl) with (decEq t t')
    nameEq (PV y t) (PV y t) | (Just Refl) | (Yes Refl) = Just Refl
    nameEq (PV y t) (PV y t') | (Just Refl) | (No p) = Nothing
  nameEq (PV x t) (PV y t') | Nothing = Nothing
nameEq (DN x t) (DN y t') with (decEq x y)
  nameEq (DN y t) (DN y t') | (Yes Refl) with (nameEq t t')
    nameEq (DN y t) (DN y t) | (Yes Refl) | (Just Refl) = Just Refl
    nameEq (DN y t) (DN y t') | (Yes Refl) | Nothing = Nothing
  nameEq (DN x t) (DN y t') | (No p) = Nothing
nameEq (Nested x y) (Nested x' y') with (decEq x x')
  nameEq (Nested x y) (Nested x' y') | (No p) = Nothing
  nameEq (Nested x y) (Nested x y') | (Yes Refl) with (nameEq y y')
    nameEq (Nested x y) (Nested x y') | (Yes Refl) | Nothing = Nothing
    nameEq (Nested x y) (Nested x y) | (Yes Refl) | (Just Refl) = Just Refl
nameEq (CaseBlock x y) (CaseBlock x' y') with (decEq x x')
  nameEq (CaseBlock x y) (CaseBlock x' y') | (No p) = Nothing
  nameEq (CaseBlock x y) (CaseBlock x y') | (Yes Refl) with (decEq y y')
    nameEq (CaseBlock x y) (CaseBlock x y') | (Yes Refl) | (No p) = Nothing
    nameEq (CaseBlock x y) (CaseBlock x y) | (Yes Refl) | (Yes Refl) = Just Refl
nameEq (WithBlock x y) (WithBlock x' y') with (decEq x x')
  nameEq (WithBlock x y) (WithBlock x' y') | (No p) = Nothing
  nameEq (WithBlock x y) (WithBlock x y') | (Yes Refl) with (decEq y y')
    nameEq (WithBlock x y) (WithBlock x y') | (Yes Refl) | (No p) = Nothing
    nameEq (WithBlock x y) (WithBlock x y) | (Yes Refl) | (Yes Refl) = Just Refl
nameEq (Resolved x) (Resolved y) with (decEq x y)
  nameEq (Resolved y) (Resolved y) | (Yes Refl) = Just Refl
  nameEq (Resolved x) (Resolved y) | (No contra) = Nothing
nameEq _ _ = Nothing

export
namesEq : (xs : List Name) -> (ys : List Name) -> Maybe (xs = ys)
namesEq [] [] = Just Refl
namesEq (x :: xs) (y :: ys)
    = do p <- nameEq x y
         ps <- namesEq xs ys
         rewrite p
         rewrite ps
         Just Refl
namesEq _ _ = Nothing


text:
-- Find the numbers in a list that are greater than a given number.
greater : Int -> List Int -> List Int
greater number list = filter (> number) list

-- Create data types representing even and odd numbers such that:
-- – The successor to an even number is an odd number, and
-- – The successor to an odd number is an even number.
data EvenOdd = Even Nat | Odd Nat

succ : EvenOdd -> EvenOdd
succ (Even n) = Odd (S n)
succ (Odd n)  = Even (S n)

-- Build a parameterized data type representing a binary tree.
data BinaryTree a = Leaf a | Node (BinaryTree a) (BinaryTree a)

-- Reverse the elements of a list. (Hint: You may need some helper functions.)
reverse : List a -> List a
reverse = reverse' []
  where
    reverse' : List a -> List a -> List a
    reverse' acc []      = acc
    reverse' acc (x::xs) = reverse' (x::acc) xs

max_stars_repo_name: hemslo/seven-in-seven

max_issues_repo_name: hemslo/seven-in-seven

max_forks_repo_name: hemslo/seven-in-seven


text:
module Monad

-- Attempt to write monad from memory with default implementations
interface Applicative m => MyMonad (m : Type -> Type) where
          myBind : m a -> (a -> m b) -> m b
          myJoin : m (m a) -> m a
          myJoin s = myBind s id
          myBind s func = myJoin $ func <$> s

MyMonad Maybe where
  myBind Nothing f = Nothing
  myBind (Just x) f = f x


text:
> module Discussion

> import Fix

# Data Types a la Carte in Idris

A brief discussion on design choices implementing DTalC.

## Syntax

One of the problems with the [original Data Types a la Carte implementation](http://www.cs.ru.nl/~W.Swierstra/Publications/DataTypesALaCarte.pdf),
was that the coproduct, `(:+:)`, allowed arbitrary grouping of signatures,
e.g. `(f :+: g) :+: g`. However, injection only performed a linear search from
left to right, and so the subtyping relation could not be satisfied in cases
which were not right-associative, such as `f :≺: (f :+: g) :+: h`.

To remedy this, a [list of signatures can be used instead](https://reasonablypolymorphic.com/blog/better-data-types-a-la-carte/).
For example, `f :+: g` would be written as `Sig [f, g]`, using `Sig` below.
Here, `fs` is a list of the different signatures that make up the composite
signature `Sig`. The `a` is the type given to each `f` in `fs`.

(Side note: An alternative method to solve injection into non-right-associative
signatures involves using a [backtracking search](http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.643.3533&rep=rep1&type=pdf),
but using a list provides a simpler solution)

> data Sig : (fs : List (Type -> Type)) -> (a : Type) -> Type where
>     Here  : f a -> Sig (f :: fs) a
>     There : Sig fs a -> Sig (f :: fs) a

Instead of `InL` and `InR` constructors for the coproduct, `Sig` uses `Here`
and `There` to describe how to construct a value of a signature. For example,
the DSL from Data Types a la Carte paper can be described as:

> data Val k = V Int
> data Add k = A k k

Using the standard definition of Fix, and the `Here` and `There` constructors,
DSLs containing both values and addition can be created. Below represents the
expression `1 + 2`:

> ex1 : Fix (Sig [Val, Add])
> ex1 = In (There (Here (A x y))) where
>     x = In (Here (V 1))
>     y = In (Here (V 2))

Clearly, this is very cumbersome to write, and so, like in the original paper,
it would be better to automate injection into some super-type. This will involve
finding the correct combination of `There` and `Here`.

Attempting to use interface instances, like in the original paper, such as
those below to perform this linear-search requires overlapping instances, which
Idris [does not allow](http://docs.idris-lang.org/en/v0.9.18/tutorial/classes.html).

Therefore, another solution to this search is required. Fortunately, this has
already been solved in the standard library (see `Elem` in [Data.List](https://github.com/idris-lang/Idris-dev/blob/master/libs/base/Data/List.idr)),
with a structure similar to `Elem` below.

The constructor `H` is a proof the signature `f` is at the front of the list
of signatures to be composed together, `fs`. The constructor `T` is a proof the
signature is after the front of the list.

> data Elem : (f : Type -> Type) -> (fs : List (Type -> Type)) -> Type where
>     H : Elem f (f :: fs)
>     T : Elem f ys -> Elem f (y :: ys)

Using this, an `inj` function can be created to construct a sequence of `Here`
and `There`:

> inj' : Elem f fs -> f a -> Sig fs a
> inj' H     x = Here x
> inj' (T t) x = There (inj' t x)

However, this does not currently provide any advantage over manually using
`Here` and `There`, since `inj'` requires manually specifying `H` and `T`.
However, Idris' automatic proof search can be leveraged to have it automatically
find the correct combination of `H` and `T`:

> inj : {auto prf : Elem f fs} -> f a -> Sig fs a
> inj {prf=H}   x = Here x
> inj {prf=T t} x = There (inj {prf=t} x)

For convenience, `inj` can be adapted to work with `Fix`:

> inject : {auto prf : Elem f fs} -> f (Fix (Sig fs)) -> Fix (Sig fs)
> inject = In . inj

Putting this together, smart constructors can be created for the example DSL.
Instead of a type constraint, `Val :<: f`, such as in the original paper,
`Elem Val fs` is used to prove that `Val` exists in `fs`:

> val : {auto prf : Elem Val fs} -> Int -> Fix (Sig fs)
> val x = inject (V x)

> add : {auto prf : Elem Add fs} -> Fix (Sig fs) -> Fix (Sig fs) -> Fix (Sig fs)
> add x y = inject (A x y)

Putting this all together, DSLs containing values and addition can be succinctly
represented:

> ex2 : Fix (Sig [Val, Add])
> ex2 = add (val 1) (add (val 2) (val 3))

## Semantics

In the original paper, typeclasses provide a method to specify the semantics
of different pieces of syntax separately, by providing an algebra `f a -> a`
to fold over a fix tree `Fix f`.

In order to fold over a `Fix` tree using `cata`, a `f` needs to be a functor:

```idris
cata : Functor f => (f a -> a) -> Fix f -> a
cata alg = alg . map (cata alg) . inop
```

In this implementation `f` is `Sig fs`, therefore, `Sig fs` needs to be a
functor. This *could* be done by modifying the definition of `Here` to be
`Here : Functor f => f a -> Sig (f :: fs) a`. However, in the implementation
so-far no functions have required `f` to be a functor and so this solution feels
sub-optimal.

Instead, the functor instance for `Sig fs` will be defined inductively such that
`Sig fs` will be a functor when each `f` in `fs` has its own definition of functor.

Firstly, where there are no signatures it is not possible to map over anything:

> Functor (Sig []) where
>     map _ (Here _) impossible
>     map _ (There _) impossible

For the base case, `Here`, `map func x` calls `map : (a -> b) -> f a -> f b`.
Whereas, in the recursive case, `There`, `map func t` calls
`map : (a -> b) -> Sig fs a -> Sig fs b`.

> (Functor f, Functor (Sig fs)) => Functor (Sig (f :: fs)) where
>     map func (Here x) = Here (map func x)
>     map func (There t) = There (map func t)

Continuing the example, by defining functor instances for both values and
addition, `Sig [Val, Add]` is also a functor.

> Functor Val where
>     map f (V x) = V x

> Functor Add where
>     map f (A x y) = A (f x) (f y)

In order to define the algebra `f a -> a` for a signature `f`, an interface is
used to allow the algebra for different pieces of syntax to be defined separately.

> interface Alg (f : Type -> Type) (a : Type) where
>     alg : f a -> a

Using the same technique used to define the `Functor` instance for `Sig`, the
`Alg` instance will be defined for `Sig fs`, provided each `f` in `fs` has its
own `Alg` instance. Again, when there is no syntax it is not possible to
use the algebras of any signatures:

> Alg (Sig []) a where
>     alg (Here _) impossible
>     alg (There _) impossible

In the base case, `alg x` uses `alg : f a -> a`. The recursive case uses
`alg : Sig fs -> a`.

> (Alg f a, Alg (Sig fs) a) => Alg (Sig (f :: fs)) a where
>     alg (Here x) = alg x
>     alg (There x) = alg x

To continue the expression example, `Alg` instances can be created that
translate into a result integer:

> Alg Val Int where
>     alg (V x) = x

> Alg Add Int where
>     alg (A x y) = x + y

Given signatures which have an algebra to which converts their syntax to
integers, a `calc` function can be created which calculates the value of an
expression:

> calc : (Functor (Sig fs), Alg (Sig fs) Int) => Fix (Sig fs) -> Int
> calc = cata alg

## Summary

This demonstrates how Data Types a la Carte can be implemented in such as
way as to solve one of the original problems. This shows how the inability to
create overlapping instances is solved by using the `Elem` type, and how
automatic proof search can be used to automatically inject into a type.

## Related Work: Effect Handlers

A problem inherent with Data Types a la Carte is it inability to allow
different semantic domains to be easily composed. To extend the DSL presented
with exceptions, for example, would require reimplementing the interface
instances `Alg Val Int` and `Alg Add Int` to be `Alg Val (Either Err Int)` and
`Alg Add (Either Err Int)`. One solution to this is [Effect Handlers](http://okmij.org/ftp/Haskell/extensible/extensible-a-la-carte.html)
which handle only specific parts of the syntax composed, instead of *all* the
syntax at once. Fortunately, this has [already been implemented in Idris](http://docs.idris-lang.org/en/latest/effects/introduction.html).

ext: lidr

max_stars_repo_name: BakerSmithA/alacarte-idris

max_issues_repo_name: BakerSmithA/alacarte-idris

max_forks_repo_name: BakerSmithA/alacarte-idris


text:
module SemVar.Data

import Data.String
import Data.List
import Data.Maybe

import Extra.String

%default total

public export
record Version where
  constructor MkVersion
  major : Int
  minor : Int
  patch : Int
  release : Maybe String
  metadata : Maybe String

%name Version version

export
Show Version where
  show version =
    join "" [ show (major version)
    , "."
    , show (minor version)
    , "."
    , show (patch version)
    , ((fromMaybe "") . map ((++) "-")) (release version)
    , ((fromMaybe "") . map ((++) "+")) (metadata version)
    ]

export
Eq Version where
  version0 == version1 =
    (major version0) == (major version1) &&
    (minor version0) == (minor version1) &&
    (patch version0) == (patch version1) &&
    (release version0) == (release version1) &&
    (metadata version0) == (metadata version1)

public export
data Requirement : Type where
  GT : Version -> Requirement
  GTE : Version -> Requirement
  LT : Version -> Requirement
  LTE : Version -> Requirement
  EQ : Version -> Requirement
  AND : Requirement -> Requirement -> Requirement
  OR : Requirement -> Requirement -> Requirement

%name Requirement requirement

-- TODO: Improve show with a pretty form, if possible
export
Show Requirement where
  show (AND req0 req1) = (show req0) ++ " " ++ (show req1)
  show (OR req0 req1) = (show req0) ++ " || " ++ (show req1)
  show (GT version) = ">" ++ (show version)
  show (GTE version) = ">=" ++ (show version)
  show (LT version) = "<" ++ (show version)
  show (LTE version) = "<=" ++ (show version)
  show (EQ version) = "=" ++ (show version)

export
Eq Requirement where
  (AND req0a req0b) == (AND req1a req1b) = req0a == req1a && req0b == req1b
  (OR req0a req0b) == (OR req1a req1b) = req0a == req1a && req0b == req1b
  (GT version0) == (GT version1) = version0 == version1
  (GTE version0) == (GTE version1) = version0 == version1
  (LT version0) == (LT version1) = version0 == version1
  (LTE version0) == (LTE version1) = version0 == version1
  (EQ version0) == (EQ version1) = version0 == version1
  _ == _ = False

export
nextMinor : Version -> Version
nextMinor version =
  MkVersion (major version) ((minor version) + 1) 0 Nothing Nothing

export
nextMajor : Version -> Version
nextMajor (MkVersion 0 minor _ _ _) =
  MkVersion 0 (minor + 1) 0 Nothing Nothing
nextMajor version =
  MkVersion ((major version) + 1) 0 0 Nothing Nothing

export
Ord Version where
  compare (MkVersion major0 minor0 patch0 release0 metadata0) (MkVersion major1 minor1 patch1 release1 metadata1) =
      case compare major0 major1 of
        EQ =>
          case compare minor0 minor1 of
            EQ =>
              case compare patch0 patch1 of
                EQ =>
                  case (release0, release1) of
                    (Just _, Nothing) =>
                      LT
                    (Nothing, Just _) =>
                      GT
                    _ =>
                      EQ
                els =>
                  els
            els =>
              els
        els =>
          els

gte : Version -> Version -> Bool
gte v0 v1 =
  let cmp = compare v0 v1
  in cmp == GT || cmp == EQ

lte : Version -> Version -> Bool
lte v0 v1 =
  let cmp = compare v0 v1
  in cmp == LT || cmp == EQ

-- TODO: We might want to make this dependently typed
export
satisfy : Requirement -> Version -> Bool
satisfy (AND reqA reqB) version = (satisfy reqA version) && (satisfy reqB version)
satisfy (OR reqA reqB) version = (satisfy reqA version) || (satisfy reqB version)
satisfy (GTE v0) v1 = v1 `gte` v0
satisfy (GT v0) v1 = compare v1 v0 == GT
satisfy (LTE v0) v1 = v1 `lte` v0
satisfy (LT v0) v1 = compare v1 v0 == LT
satisfy (EQ v0) v1 = compare v1 v0 == EQ
satisfy _ _ = False

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
module Inigo.Async.Package

import Inigo.Paths
import Inigo.Async.Base
import Inigo.Async.CloudFlare.KV
import Inigo.Async.FS
import Inigo.Async.Promise
import Inigo.Package.Package
import Inigo.Package.PackageDhall
import Inigo.Package.PackageIndex

||| Gets a package from the "packages" KV
export
getPackage : String -> Promise (Either String Package)
getPackage package =
  map parsePackage (read "packages" package)

||| Returns an index with all packages
export
index : Promise (Either String PackageIndex)
index =
  map parsePackageIndex (read "packages" "index")

public export
data InigoPackagePath
  = TomlPath String
  | DhallPath String

export
Show InigoPackagePath where
  show (TomlPath x) = x
  show (DhallPath x) = x

export
packageFilePath : String -> Promise InigoPackagePath
packageFilePath src =
  let tomlPath = src </> inigoTomlPath
      dhallPath = src </> inigoDhallPath
  in do
    tp <- fs_exists tomlPath
    dp <- fs_exists dhallPath
    case (tp, dp) of
         (True, False) => pure $ TomlPath tomlPath
         (False, True) => pure $ DhallPath dhallPath
         (True, True) => reject "Conflict: both Inigo.toml and Inigo.dhall found"
         (False, False) => reject "Inigo.toml or Inigo.dhall file not found"

parseFile : InigoPackagePath -> Promise Package
parseFile (TomlPath path) = do
  contents <- fs_readFile path
  let Right package = parsePackage contents
    | Left err => reject ("Error reading toml package: " ++ err)
  pure package
parseFile (DhallPath path) = do
  -- can pass the file path to dhall so it can handle relative imports
  Right package <- parsePackageDhall path
    | Left err => reject ("Error reading dhall package: " ++ err)
  pure package

export
readPackage : String -> Promise Package
readPackage dir = parseFile !(packageFilePath dir)

export
currPackage : Promise Package
currPackage = readPackage "." -- current dir


text:
module Dart.Core.String

import Dart.FFI.Elab
import Dart.Core

%language ElabReflection

%runElab importDart [
  package "dart:core" [
    primitive $ class' "String" [
      final "bool" "isEmpty",
      final "bool" "isNotEmpty",

      fun "String" "padLeft" [
        "width" :: "int",
        "padding" :: "String"
      ],

      fun "String" "padRight" [
        "width" :: "int",
        "padding" :: "String"
      ]
    ]
  ]
]


text:
module URI

import Node.URI

test : (fn : String -> Either URIError String) -> String -> String
test fn input = case fn input of
  Left (MkURIError message) => message
  Right result => result

main : IO ()
main = do
  -- examples from: https://developer.mozilla.org/en-US/docs/Web/JavaScript/Reference/Global_Objects/decodeURI
  putStrLn $ test decodeURI "https://developer.mozilla.org/ru/docs/JavaScript_%D1%88%D0%B5%D0%BB%D0%BB%D1%8B"
  putStrLn $ test decodeURI "%E0%A4%A"

  -- examples from: https://developer.mozilla.org/en-US/docs/Web/JavaScript/Reference/Global_Objects/decodeURIComponent
  putStrLn $ test decodeURIComponent "JavaScript_%D1%88%D0%B5%D0%BB%D0%BB%D1%8B"
  putStrLn $ test decodeURIComponent "%E0%A4%A"
  putStrLn $ test decodeURIComponent "search+query%20%28correct%29"

  -- examples from: https://developer.mozilla.org/en-US/docs/Web/JavaScript/Reference/Global_Objects/encodeURI
  putStrLn $ test decodeURI $ test encodeURI "https://mozilla.org/?x=шеллы"

  let set1 = ";,/?:@&=+$#"
      set2 = "-_.!~*'()"
      set3 = "ABC abc 123"

  putStrLn $ test encodeURI set1
  putStrLn $ test encodeURI set2
  putStrLn $ test encodeURI set3

  putStrLn $ test encodeURIComponent set1
  putStrLn $ test encodeURIComponent set2
  putStrLn $ test encodeURIComponent set3

--  putStrLn $ test encodeURI "\uD800\uDFFF"
--  putStrLn $ test encodeURI "\uD800"
--  putStrLn $ test encodeURI "\uDFFF"

  -- examples from: https://developer.mozilla.org/en-US/docs/Web/JavaScript/Reference/Global_Objects/encodeURIComponent
  putStrLn $ test encodeURIComponent "test?"
  putStrLn $ test encodeURIComponent "шеллы"

max_stars_repo_name: kbertalan/tyttp

max_issues_repo_name: kbertalan/tyttp

max_forks_repo_name: kbertalan/tyttp