text:
module Web.Raw.Streams

import JS
import Web.Internal.StreamsPrim
import Web.Internal.Types

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

namespace ByteLengthQueuingStrategy

  export
  new :  (0 _ : JSType t1)
      => {auto 0 _ : Elem QueuingStrategyInit (Types t1)}
      -> (init : t1)
      -> JSIO ByteLengthQueuingStrategy
  new a = primJS $ ByteLengthQueuingStrategy.prim__new (up a)

  export
  highWaterMark : (obj : ByteLengthQueuingStrategy) -> JSIO Double
  highWaterMark a = primJS $ ByteLengthQueuingStrategy.prim__highWaterMark a

  export
  size : (obj : ByteLengthQueuingStrategy) -> JSIO Function
  size a = primJS $ ByteLengthQueuingStrategy.prim__size a

namespace CountQueuingStrategy

  export
  new :  (0 _ : JSType t1)
      => {auto 0 _ : Elem QueuingStrategyInit (Types t1)}
      -> (init : t1)
      -> JSIO CountQueuingStrategy
  new a = primJS $ CountQueuingStrategy.prim__new (up a)

  export
  highWaterMark : (obj : CountQueuingStrategy) -> JSIO Double
  highWaterMark a = primJS $ CountQueuingStrategy.prim__highWaterMark a

  export
  size : (obj : CountQueuingStrategy) -> JSIO Function
  size a = primJS $ CountQueuingStrategy.prim__size a

namespace ReadableByteStreamController

  export
  byobRequest :  (obj : ReadableByteStreamController)
              -> JSIO (Maybe ReadableStreamBYOBRequest)
  byobRequest a = tryJS "ReadableByteStreamController.byobRequest"
                $ ReadableByteStreamController.prim__byobRequest a

  export
  desiredSize : (obj : ReadableByteStreamController) -> JSIO (Maybe Double)
  desiredSize a = tryJS "ReadableByteStreamController.desiredSize"
                $ ReadableByteStreamController.prim__desiredSize a

  export
  close : (obj : ReadableByteStreamController) -> JSIO ()
  close a = primJS $ ReadableByteStreamController.prim__close a

  export
  enqueue :  (obj : ReadableByteStreamController)
          -> (chunk : NS I [ Int8Array
                           , Int16Array
                           , Int32Array
                           , UInt8Array
                           , UInt8Array
                           , UInt8Array
                           , UInt8ClampedArray
                           , Float32Array
                           , Float64Array
                           , DataView
                           ])
          -> JSIO ()
  enqueue a b = primJS $ ReadableByteStreamController.prim__enqueue a (toFFI b)

  export
  error : (obj : ReadableByteStreamController) -> (e : Optional Any) -> JSIO ()
  error a b = primJS $ ReadableByteStreamController.prim__error a (toFFI b)

  export
  error' : (obj : ReadableByteStreamController) -> JSIO ()
  error' a = primJS $ ReadableByteStreamController.prim__error a undef

namespace ReadableStream

  export
  new :  (0 _ : JSType t1)
      => (0 _ : JSType t2)
      => {auto 0 _ : Elem Object (Types t1)}
      -> {auto 0 _ : Elem QueuingStrategy (Types t2)}
      -> (underlyingSource : Optional t1)
      -> (strategy : Optional t2)
      -> JSIO ReadableStream
  new a b = primJS $ ReadableStream.prim__new (optUp a) (optUp b)

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

  export
  locked : (obj : ReadableStream) -> JSIO Bool
  locked a = tryJS "ReadableStream.locked" $ ReadableStream.prim__locked a

  export
  cancel :  (obj : ReadableStream)
         -> (reason : Optional Any)
         -> JSIO (Promise Undefined)
  cancel a b = primJS $ ReadableStream.prim__cancel a (toFFI b)

  export
  cancel' : (obj : ReadableStream) -> JSIO (Promise Undefined)
  cancel' a = primJS $ ReadableStream.prim__cancel a undef

  export
  getReader :  (0 _ : JSType t1)
            => {auto 0 _ : Elem ReadableStreamGetReaderOptions (Types t1)}
            -> (obj : ReadableStream)
            -> (options : Optional t1)
            -> JSIO (NS I [ ReadableStreamDefaultReader
                          , ReadableStreamBYOBReader
                          ])
  getReader a b = tryJS "ReadableStream.getReader"
                $ ReadableStream.prim__getReader a (optUp b)

  export
  getReader' :  (obj : ReadableStream)
             -> JSIO (NS I [ ReadableStreamDefaultReader
                           , ReadableStreamBYOBReader
                           ])
  getReader' a = tryJS "ReadableStream.getReader'"
               $ ReadableStream.prim__getReader a undef

  export
  pipeThrough :  (0 _ : JSType t1)
              => (0 _ : JSType t2)
              => {auto 0 _ : Elem ReadableWritablePair (Types t1)}
              -> {auto 0 _ : Elem StreamPipeOptions (Types t2)}
              -> (obj : ReadableStream)
              -> (transform : t1)
              -> (options : Optional t2)
              -> JSIO ReadableStream
  pipeThrough a b c = primJS
                    $ ReadableStream.prim__pipeThrough a (up b) (optUp c)

  export
  pipeThrough' :  (0 _ : JSType t1)
               => {auto 0 _ : Elem ReadableWritablePair (Types t1)}
               -> (obj : ReadableStream)
               -> (transform : t1)
               -> JSIO ReadableStream
  pipeThrough' a b = primJS $ ReadableStream.prim__pipeThrough a (up b) undef

  export
  pipeTo :  (0 _ : JSType t1)
         => {auto 0 _ : Elem StreamPipeOptions (Types t1)}
         -> (obj : ReadableStream)
         -> (destination : WritableStream)
         -> (options : Optional t1)
         -> JSIO (Promise Undefined)
  pipeTo a b c = primJS $ ReadableStream.prim__pipeTo a b (optUp c)

  export
  pipeTo' :  (obj : ReadableStream)
          -> (destination : WritableStream)
          -> JSIO (Promise Undefined)
  pipeTo' a b = primJS $ ReadableStream.prim__pipeTo a b undef

  export
  tee : (obj : ReadableStream) -> JSIO (Array ReadableStream)
  tee a = primJS $ ReadableStream.prim__tee a

namespace ReadableStreamBYOBReader

  export
  new : (stream : ReadableStream) -> JSIO ReadableStreamBYOBReader
  new a = primJS $ ReadableStreamBYOBReader.prim__new a

  export
  read :  (obj : ReadableStreamBYOBReader)
       -> (view : NS I [ Int8Array
                       , Int16Array
                       , Int32Array
                       , UInt8Array
                       , UInt8Array
                       , UInt8Array
                       , UInt8ClampedArray
                       , Float32Array
                       , Float64Array
                       , DataView
                       ])
       -> JSIO (Promise ReadableStreamBYOBReadResult)
  read a b = primJS $ ReadableStreamBYOBReader.prim__read a (toFFI b)

  export
  releaseLock : (obj : ReadableStreamBYOBReader) -> JSIO ()
  releaseLock a = primJS $ ReadableStreamBYOBReader.prim__releaseLock a

namespace ReadableStreamBYOBRequest

  export
  view :  (obj : ReadableStreamBYOBRequest)
       -> JSIO (Maybe (Union10 Int8Array
                               Int16Array
                               Int32Array
                               UInt8Array
                               UInt8Array
                               UInt8Array
                               UInt8ClampedArray
                               Float32Array
                               Float64Array
                               DataView))
  view a = tryJS "ReadableStreamBYOBRequest.view"
         $ ReadableStreamBYOBRequest.prim__view a

  export
  respond :  (obj : ReadableStreamBYOBRequest)
          -> (bytesWritten : JSBits64)
          -> JSIO ()
  respond a b = primJS $ ReadableStreamBYOBRequest.prim__respond a b

  export
  respondWithNewView :  (obj : ReadableStreamBYOBRequest)
                     -> (view : NS I [ Int8Array
                                     , Int16Array
                                     , Int32Array
                                     , UInt8Array
                                     , UInt8Array
                                     , UInt8Array
                                     , UInt8ClampedArray
                                     , Float32Array
                                     , Float64Array
                                     , DataView
                                     ])
                     -> JSIO ()
  respondWithNewView a b = primJS
                         $ ReadableStreamBYOBRequest.prim__respondWithNewView a
                                                                              (toFFI b)

namespace ReadableStreamDefaultController

  export
  desiredSize : (obj : ReadableStreamDefaultController) -> JSIO (Maybe Double)
  desiredSize a = tryJS "ReadableStreamDefaultController.desiredSize"
                $ ReadableStreamDefaultController.prim__desiredSize a

  export
  close : (obj : ReadableStreamDefaultController) -> JSIO ()
  close a = primJS $ ReadableStreamDefaultController.prim__close a

  export
  enqueue :  (obj : ReadableStreamDefaultController)
          -> (chunk : Optional Any)
          -> JSIO ()
  enqueue a b = primJS
              $ ReadableStreamDefaultController.prim__enqueue a (toFFI b)

  export
  enqueue' : (obj : ReadableStreamDefaultController) -> JSIO ()
  enqueue' a = primJS $ ReadableStreamDefaultController.prim__enqueue a undef

  export
  error :  (obj : ReadableStreamDefaultController)
        -> (e : Optional Any)
        -> JSIO ()
  error a b = primJS $ ReadableStreamDefaultController.prim__error a (toFFI b)

  export
  error' : (obj : ReadableStreamDefaultController) -> JSIO ()
  error' a = primJS $ ReadableStreamDefaultController.prim__error a undef

namespace ReadableStreamDefaultReader

  export
  new : (stream : ReadableStream) -> JSIO ReadableStreamDefaultReader
  new a = primJS $ ReadableStreamDefaultReader.prim__new a

  export
  read :  (obj : ReadableStreamDefaultReader)
       -> JSIO (Promise ReadableStreamDefaultReadResult)
  read a = primJS $ ReadableStreamDefaultReader.prim__read a

  export
  releaseLock : (obj : ReadableStreamDefaultReader) -> JSIO ()
  releaseLock a = primJS $ ReadableStreamDefaultReader.prim__releaseLock a

namespace TransformStream

  export
  new :  (0 _ : JSType t1)
      => (0 _ : JSType t2)
      => (0 _ : JSType t3)
      => {auto 0 _ : Elem Object (Types t1)}
      -> {auto 0 _ : Elem QueuingStrategy (Types t2)}
      -> {auto 0 _ : Elem QueuingStrategy (Types t3)}
      -> (transformer : Optional t1)
      -> (writableStrategy : Optional t2)
      -> (readableStrategy : Optional t3)
      -> JSIO TransformStream
  new a b c = primJS $ TransformStream.prim__new (optUp a) (optUp b) (optUp c)

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

  export
  readable : (obj : TransformStream) -> JSIO ReadableStream
  readable a = primJS $ TransformStream.prim__readable a

  export
  writable : (obj : TransformStream) -> JSIO WritableStream
  writable a = primJS $ TransformStream.prim__writable a

namespace TransformStreamDefaultController

  export
  desiredSize : (obj : TransformStreamDefaultController) -> JSIO (Maybe Double)
  desiredSize a = tryJS "TransformStreamDefaultController.desiredSize"
                $ TransformStreamDefaultController.prim__desiredSize a

  export
  enqueue :  (obj : TransformStreamDefaultController)
          -> (chunk : Optional Any)
          -> JSIO ()
  enqueue a b = primJS
              $ TransformStreamDefaultController.prim__enqueue a (toFFI b)

  export
  enqueue' : (obj : TransformStreamDefaultController) -> JSIO ()
  enqueue' a = primJS $ TransformStreamDefaultController.prim__enqueue a undef

  export
  error :  (obj : TransformStreamDefaultController)
        -> (reason : Optional Any)
        -> JSIO ()
  error a b = primJS $ TransformStreamDefaultController.prim__error a (toFFI b)

  export
  error' : (obj : TransformStreamDefaultController) -> JSIO ()
  error' a = primJS $ TransformStreamDefaultController.prim__error a undef

  export
  terminate : (obj : TransformStreamDefaultController) -> JSIO ()
  terminate a = primJS $ TransformStreamDefaultController.prim__terminate a

namespace WritableStream

  export
  new :  (0 _ : JSType t1)
      => (0 _ : JSType t2)
      => {auto 0 _ : Elem Object (Types t1)}
      -> {auto 0 _ : Elem QueuingStrategy (Types t2)}
      -> (underlyingSink : Optional t1)
      -> (strategy : Optional t2)
      -> JSIO WritableStream
  new a b = primJS $ WritableStream.prim__new (optUp a) (optUp b)

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

  export
  locked : (obj : WritableStream) -> JSIO Bool
  locked a = tryJS "WritableStream.locked" $ WritableStream.prim__locked a

  export
  abort :  (obj : WritableStream)
        -> (reason : Optional Any)
        -> JSIO (Promise Undefined)
  abort a b = primJS $ WritableStream.prim__abort a (toFFI b)

  export
  abort' : (obj : WritableStream) -> JSIO (Promise Undefined)
  abort' a = primJS $ WritableStream.prim__abort a undef

  export
  close : (obj : WritableStream) -> JSIO (Promise Undefined)
  close a = primJS $ WritableStream.prim__close a

  export
  getWriter : (obj : WritableStream) -> JSIO WritableStreamDefaultWriter
  getWriter a = primJS $ WritableStream.prim__getWriter a

namespace WritableStreamDefaultController

  export
  error :  (obj : WritableStreamDefaultController)
        -> (e : Optional Any)
        -> JSIO ()
  error a b = primJS $ WritableStreamDefaultController.prim__error a (toFFI b)

  export
  error' : (obj : WritableStreamDefaultController) -> JSIO ()
  error' a = primJS $ WritableStreamDefaultController.prim__error a undef

namespace WritableStreamDefaultWriter

  export
  new : (stream : WritableStream) -> JSIO WritableStreamDefaultWriter
  new a = primJS $ WritableStreamDefaultWriter.prim__new a

  export
  closed : (obj : WritableStreamDefaultWriter) -> JSIO (Promise Undefined)
  closed a = primJS $ WritableStreamDefaultWriter.prim__closed a

  export
  desiredSize : (obj : WritableStreamDefaultWriter) -> JSIO (Maybe Double)
  desiredSize a = tryJS "WritableStreamDefaultWriter.desiredSize"
                $ WritableStreamDefaultWriter.prim__desiredSize a

  export
  ready : (obj : WritableStreamDefaultWriter) -> JSIO (Promise Undefined)
  ready a = primJS $ WritableStreamDefaultWriter.prim__ready a

  export
  abort :  (obj : WritableStreamDefaultWriter)
        -> (reason : Optional Any)
        -> JSIO (Promise Undefined)
  abort a b = primJS $ WritableStreamDefaultWriter.prim__abort a (toFFI b)

  export
  abort' : (obj : WritableStreamDefaultWriter) -> JSIO (Promise Undefined)
  abort' a = primJS $ WritableStreamDefaultWriter.prim__abort a undef

  export
  close : (obj : WritableStreamDefaultWriter) -> JSIO (Promise Undefined)
  close a = primJS $ WritableStreamDefaultWriter.prim__close a

  export
  releaseLock : (obj : WritableStreamDefaultWriter) -> JSIO ()
  releaseLock a = primJS $ WritableStreamDefaultWriter.prim__releaseLock a

  export
  write :  (obj : WritableStreamDefaultWriter)
        -> (chunk : Optional Any)
        -> JSIO (Promise Undefined)
  write a b = primJS $ WritableStreamDefaultWriter.prim__write a (toFFI b)

  export
  write' : (obj : WritableStreamDefaultWriter) -> JSIO (Promise Undefined)
  write' a = primJS $ WritableStreamDefaultWriter.prim__write a undef

--------------------------------------------------------------------------------
--          Mixins
--------------------------------------------------------------------------------

namespace GenericTransformStream

  export
  readable :  (0 _ : JSType t1)
           => {auto 0 _ : Elem GenericTransformStream (Types t1)}
           -> (obj : t1)
           -> JSIO ReadableStream
  readable a = primJS $ GenericTransformStream.prim__readable (up a)

  export
  writable :  (0 _ : JSType t1)
           => {auto 0 _ : Elem GenericTransformStream (Types t1)}
           -> (obj : t1)
           -> JSIO WritableStream
  writable a = primJS $ GenericTransformStream.prim__writable (up a)

namespace ReadableStreamGenericReader

  export
  closed :  (0 _ : JSType t1)
         => {auto 0 _ : Elem ReadableStreamGenericReader (Types t1)}
         -> (obj : t1)
         -> JSIO (Promise Undefined)
  closed a = primJS $ ReadableStreamGenericReader.prim__closed (up a)

  export
  cancel :  (0 _ : JSType t1)
         => {auto 0 _ : Elem ReadableStreamGenericReader (Types t1)}
         -> (obj : t1)
         -> (reason : Optional Any)
         -> JSIO (Promise Undefined)
  cancel a b = primJS
             $ ReadableStreamGenericReader.prim__cancel (up a) (toFFI b)

  export
  cancel' :  (0 _ : JSType t1)
          => {auto 0 _ : Elem ReadableStreamGenericReader (Types t1)}
          -> (obj : t1)
          -> JSIO (Promise Undefined)
  cancel' a = primJS $ ReadableStreamGenericReader.prim__cancel (up a) undef

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

namespace QueuingStrategy

  export
  new :  (highWaterMark : Optional Double)
      -> (size : Optional QueuingStrategySize)
      -> JSIO QueuingStrategy
  new a b = primJS $ QueuingStrategy.prim__new (toFFI a) (toFFI b)

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

  export
  highWaterMark :  (0 _ : JSType t)
                => {auto 0 _ : Elem QueuingStrategy (Types t)}
                -> t
                -> Attribute False Optional Double
  highWaterMark v = fromUndefOrPrimNoDefault "QueuingStrategy.gethighWaterMark"
                                             prim__highWaterMark
                                             prim__setHighWaterMark
                                             (v :> QueuingStrategy)

  export
  size :  (0 _ : JSType t)
       => {auto 0 _ : Elem QueuingStrategy (Types t)}
       -> t
       -> Attribute False Optional QueuingStrategySize
  size v = fromUndefOrPrimNoDefault "QueuingStrategy.getsize"
                                    prim__size
                                    prim__setSize
                                    (v :> QueuingStrategy)

namespace QueuingStrategyInit

  export
  new : (highWaterMark : Double) -> JSIO QueuingStrategyInit
  new a = primJS $ QueuingStrategyInit.prim__new a

  export
  highWaterMark :  (0 _ : JSType t)
                => {auto 0 _ : Elem QueuingStrategyInit (Types t)}
                -> t
                -> Attribute True I Double
  highWaterMark v = fromPrim "QueuingStrategyInit.gethighWaterMark"
                             prim__highWaterMark
                             prim__setHighWaterMark
                             (v :> QueuingStrategyInit)

namespace ReadableStreamBYOBReadResult

  export
  new :  (value : Optional (NS I [ Int8Array
                                 , Int16Array
                                 , Int32Array
                                 , UInt8Array
                                 , UInt8Array
                                 , UInt8Array
                                 , UInt8ClampedArray
                                 , Float32Array
                                 , Float64Array
                                 , DataView
                                 ]))
      -> (done : Optional Bool)
      -> JSIO ReadableStreamBYOBReadResult
  new a b = primJS $ ReadableStreamBYOBReadResult.prim__new (toFFI a) (toFFI b)

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

  export
  done :  (0 _ : JSType t)
       => {auto 0 _ : Elem ReadableStreamBYOBReadResult (Types t)}
       -> t
       -> Attribute False Optional Bool
  done v = fromUndefOrPrimNoDefault "ReadableStreamBYOBReadResult.getdone"
                                    prim__done
                                    prim__setDone
                                    (v :> ReadableStreamBYOBReadResult)

  export
  value :  (0 _ : JSType t)
        => {auto 0 _ : Elem ReadableStreamBYOBReadResult (Types t)}
        -> t
        -> Attribute False Optional (Union10 Int8Array
                                             Int16Array
                                             Int32Array
                                             UInt8Array
                                             UInt8Array
                                             UInt8Array
                                             UInt8ClampedArray
                                             Float32Array
                                             Float64Array
                                             DataView)
  value v = fromUndefOrPrimNoDefault "ReadableStreamBYOBReadResult.getvalue"
                                     prim__value
                                     prim__setValue
                                     (v :> ReadableStreamBYOBReadResult)

namespace ReadableStreamDefaultReadResult

  export
  new :  (value : Optional Any)
      -> (done : Optional Bool)
      -> JSIO ReadableStreamDefaultReadResult
  new a b = primJS
          $ ReadableStreamDefaultReadResult.prim__new (toFFI a) (toFFI b)

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

  export
  done :  (0 _ : JSType t)
       => {auto 0 _ : Elem ReadableStreamDefaultReadResult (Types t)}
       -> t
       -> Attribute False Optional Bool
  done v = fromUndefOrPrimNoDefault "ReadableStreamDefaultReadResult.getdone"
                                    prim__done
                                    prim__setDone
                                    (v :> ReadableStreamDefaultReadResult)

  export
  value :  (0 _ : JSType t)
        => {auto 0 _ : Elem ReadableStreamDefaultReadResult (Types t)}
        -> t
        -> Attribute False Optional Any
  value v = fromUndefOrPrimNoDefault "ReadableStreamDefaultReadResult.getvalue"
                                     prim__value
                                     prim__setValue
                                     (v :> ReadableStreamDefaultReadResult)

namespace ReadableStreamGetReaderOptions

  export
  new :  (mode : Optional ReadableStreamReaderMode)
      -> JSIO ReadableStreamGetReaderOptions
  new a = primJS $ ReadableStreamGetReaderOptions.prim__new (toFFI a)

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

  export
  mode :  (0 _ : JSType t)
       => {auto 0 _ : Elem ReadableStreamGetReaderOptions (Types t)}
       -> t
       -> Attribute False Optional ReadableStreamReaderMode
  mode v = fromUndefOrPrimNoDefault "ReadableStreamGetReaderOptions.getmode"
                                    prim__mode
                                    prim__setMode
                                    (v :> ReadableStreamGetReaderOptions)

namespace ReadableStreamIteratorOptions

  export
  new : (preventCancel : Optional Bool) -> JSIO ReadableStreamIteratorOptions
  new a = primJS $ ReadableStreamIteratorOptions.prim__new (toFFI a)

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

  export
  preventCancel :  (0 _ : JSType t)
                => {auto 0 _ : Elem ReadableStreamIteratorOptions (Types t)}
                -> t
                -> Attribute True Optional Bool
  preventCancel v = fromUndefOrPrim "ReadableStreamIteratorOptions.getpreventCancel"
                                    prim__preventCancel
                                    prim__setPreventCancel
                                    False
                                    (v :> ReadableStreamIteratorOptions)

namespace ReadableWritablePair

  export
  new :  (readable : ReadableStream)
      -> (writable : WritableStream)
      -> JSIO ReadableWritablePair
  new a b = primJS $ ReadableWritablePair.prim__new a b

  export
  readable :  (0 _ : JSType t)
           => {auto 0 _ : Elem ReadableWritablePair (Types t)}
           -> t
           -> Attribute True I ReadableStream
  readable v = fromPrim "ReadableWritablePair.getreadable"
                        prim__readable
                        prim__setReadable
                        (v :> ReadableWritablePair)

  export
  writable :  (0 _ : JSType t)
           => {auto 0 _ : Elem ReadableWritablePair (Types t)}
           -> t
           -> Attribute True I WritableStream
  writable v = fromPrim "ReadableWritablePair.getwritable"
                        prim__writable
                        prim__setWritable
                        (v :> ReadableWritablePair)

namespace StreamPipeOptions

  export
  new :  (preventClose : Optional Bool)
      -> (preventAbort : Optional Bool)
      -> (preventCancel : Optional Bool)
      -> (signal : Optional AbortSignal)
      -> JSIO StreamPipeOptions
  new a b c d = primJS
              $ StreamPipeOptions.prim__new (toFFI a)
                                            (toFFI b)
                                            (toFFI c)
                                            (toFFI d)

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

  export
  preventAbort :  (0 _ : JSType t)
               => {auto 0 _ : Elem StreamPipeOptions (Types t)}
               -> t
               -> Attribute True Optional Bool
  preventAbort v = fromUndefOrPrim "StreamPipeOptions.getpreventAbort"
                                   prim__preventAbort
                                   prim__setPreventAbort
                                   False
                                   (v :> StreamPipeOptions)

  export
  preventCancel :  (0 _ : JSType t)
                => {auto 0 _ : Elem StreamPipeOptions (Types t)}
                -> t
                -> Attribute True Optional Bool
  preventCancel v = fromUndefOrPrim "StreamPipeOptions.getpreventCancel"
                                    prim__preventCancel
                                    prim__setPreventCancel
                                    False
                                    (v :> StreamPipeOptions)

  export
  preventClose :  (0 _ : JSType t)
               => {auto 0 _ : Elem StreamPipeOptions (Types t)}
               -> t
               -> Attribute True Optional Bool
  preventClose v = fromUndefOrPrim "StreamPipeOptions.getpreventClose"
                                   prim__preventClose
                                   prim__setPreventClose
                                   False
                                   (v :> StreamPipeOptions)

  export
  signal :  (0 _ : JSType t)
         => {auto 0 _ : Elem StreamPipeOptions (Types t)}
         -> t
         -> Attribute False Optional AbortSignal
  signal v = fromUndefOrPrimNoDefault "StreamPipeOptions.getsignal"
                                      prim__signal
                                      prim__setSignal
                                      (v :> StreamPipeOptions)

namespace Transformer

  export
  new :  (start : Optional TransformerStartCallback)
      -> (transform : Optional TransformerTransformCallback)
      -> (flush : Optional TransformerFlushCallback)
      -> (readableType : Optional Any)
      -> (writableType : Optional Any)
      -> JSIO Transformer
  new a b c d e = primJS
                $ Transformer.prim__new (toFFI a)
                                        (toFFI b)
                                        (toFFI c)
                                        (toFFI d)
                                        (toFFI e)

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

  export
  flush :  (0 _ : JSType t)
        => {auto 0 _ : Elem Transformer (Types t)}
        -> t
        -> Attribute False Optional TransformerFlushCallback
  flush v = fromUndefOrPrimNoDefault "Transformer.getflush"
                                     prim__flush
                                     prim__setFlush
                                     (v :> Transformer)

  export
  readableType :  (0 _ : JSType t)
               => {auto 0 _ : Elem Transformer (Types t)}
               -> t
               -> Attribute False Optional Any
  readableType v = fromUndefOrPrimNoDefault "Transformer.getreadableType"
                                            prim__readableType
                                            prim__setReadableType
                                            (v :> Transformer)

  export
  start :  (0 _ : JSType t)
        => {auto 0 _ : Elem Transformer (Types t)}
        -> t
        -> Attribute False Optional TransformerStartCallback
  start v = fromUndefOrPrimNoDefault "Transformer.getstart"
                                     prim__start
                                     prim__setStart
                                     (v :> Transformer)

  export
  transform :  (0 _ : JSType t)
            => {auto 0 _ : Elem Transformer (Types t)}
            -> t
            -> Attribute False Optional TransformerTransformCallback
  transform v = fromUndefOrPrimNoDefault "Transformer.gettransform"
                                         prim__transform
                                         prim__setTransform
                                         (v :> Transformer)

  export
  writableType :  (0 _ : JSType t)
               => {auto 0 _ : Elem Transformer (Types t)}
               -> t
               -> Attribute False Optional Any
  writableType v = fromUndefOrPrimNoDefault "Transformer.getwritableType"
                                            prim__writableType
                                            prim__setWritableType
                                            (v :> Transformer)

namespace UnderlyingSink

  export
  new :  (start : Optional UnderlyingSinkStartCallback)
      -> (write : Optional UnderlyingSinkWriteCallback)
      -> (close : Optional UnderlyingSinkCloseCallback)
      -> (abort : Optional UnderlyingSinkAbortCallback)
      -> (type : Optional Any)
      -> JSIO UnderlyingSink
  new a b c d e = primJS
                $ UnderlyingSink.prim__new (toFFI a)
                                           (toFFI b)
                                           (toFFI c)
                                           (toFFI d)
                                           (toFFI e)

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

  export
  abort :  (0 _ : JSType t)
        => {auto 0 _ : Elem UnderlyingSink (Types t)}
        -> t
        -> Attribute False Optional UnderlyingSinkAbortCallback
  abort v = fromUndefOrPrimNoDefault "UnderlyingSink.getabort"
                                     prim__abort
                                     prim__setAbort
                                     (v :> UnderlyingSink)

  export
  close :  (0 _ : JSType t)
        => {auto 0 _ : Elem UnderlyingSink (Types t)}
        -> t
        -> Attribute False Optional UnderlyingSinkCloseCallback
  close v = fromUndefOrPrimNoDefault "UnderlyingSink.getclose"
                                     prim__close
                                     prim__setClose
                                     (v :> UnderlyingSink)

  export
  start :  (0 _ : JSType t)
        => {auto 0 _ : Elem UnderlyingSink (Types t)}
        -> t
        -> Attribute False Optional UnderlyingSinkStartCallback
  start v = fromUndefOrPrimNoDefault "UnderlyingSink.getstart"
                                     prim__start
                                     prim__setStart
                                     (v :> UnderlyingSink)

  export
  type :  (0 _ : JSType t)
       => {auto 0 _ : Elem UnderlyingSink (Types t)}
       -> t
       -> Attribute False Optional Any
  type v = fromUndefOrPrimNoDefault "UnderlyingSink.gettype"
                                    prim__type
                                    prim__setType
                                    (v :> UnderlyingSink)

  export
  write :  (0 _ : JSType t)
        => {auto 0 _ : Elem UnderlyingSink (Types t)}
        -> t
        -> Attribute False Optional UnderlyingSinkWriteCallback
  write v = fromUndefOrPrimNoDefault "UnderlyingSink.getwrite"
                                     prim__write
                                     prim__setWrite
                                     (v :> UnderlyingSink)

namespace UnderlyingSource

  export
  new :  (start : Optional UnderlyingSourceStartCallback)
      -> (pull : Optional UnderlyingSourcePullCallback)
      -> (cancel : Optional UnderlyingSourceCancelCallback)
      -> (type : Optional ReadableStreamType)
      -> (autoAllocateChunkSize : Optional JSBits64)
      -> JSIO UnderlyingSource
  new a b c d e = primJS
                $ UnderlyingSource.prim__new (toFFI a)
                                             (toFFI b)
                                             (toFFI c)
                                             (toFFI d)
                                             (toFFI e)

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

  export
  autoAllocateChunkSize :  (0 _ : JSType t)
                        => {auto 0 _ : Elem UnderlyingSource (Types t)}
                        -> t
                        -> Attribute False Optional JSBits64
  autoAllocateChunkSize v = fromUndefOrPrimNoDefault "UnderlyingSource.getautoAllocateChunkSize"
                                                     prim__autoAllocateChunkSize
                                                     prim__setAutoAllocateChunkSize
                                                     (v :> UnderlyingSource)

  export
  cancel :  (0 _ : JSType t)
         => {auto 0 _ : Elem UnderlyingSource (Types t)}
         -> t
         -> Attribute False Optional UnderlyingSourceCancelCallback
  cancel v = fromUndefOrPrimNoDefault "UnderlyingSource.getcancel"
                                      prim__cancel
                                      prim__setCancel
                                      (v :> UnderlyingSource)

  export
  pull :  (0 _ : JSType t)
       => {auto 0 _ : Elem UnderlyingSource (Types t)}
       -> t
       -> Attribute False Optional UnderlyingSourcePullCallback
  pull v = fromUndefOrPrimNoDefault "UnderlyingSource.getpull"
                                    prim__pull
                                    prim__setPull
                                    (v :> UnderlyingSource)

  export
  start :  (0 _ : JSType t)
        => {auto 0 _ : Elem UnderlyingSource (Types t)}
        -> t
        -> Attribute False Optional UnderlyingSourceStartCallback
  start v = fromUndefOrPrimNoDefault "UnderlyingSource.getstart"
                                     prim__start
                                     prim__setStart
                                     (v :> UnderlyingSource)

  export
  type :  (0 _ : JSType t)
       => {auto 0 _ : Elem UnderlyingSource (Types t)}
       -> t
       -> Attribute False Optional ReadableStreamType
  type v = fromUndefOrPrimNoDefault "UnderlyingSource.gettype"
                                    prim__type
                                    prim__setType
                                    (v :> UnderlyingSource)

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

namespace QueuingStrategySize

  export
  toQueuingStrategySize :  ( UndefOr AnyPtr -> IO Double )
                        -> JSIO QueuingStrategySize
  toQueuingStrategySize cb = primJS $ prim__toQueuingStrategySize cb

namespace TransformerFlushCallback

  export
  toTransformerFlushCallback :  (  TransformStreamDefaultController
                                -> IO (Promise Undefined)
                                )
                             -> JSIO TransformerFlushCallback
  toTransformerFlushCallback cb = primJS $ prim__toTransformerFlushCallback cb

namespace TransformerStartCallback

  export
  toTransformerStartCallback :  (  TransformStreamDefaultController
                                -> IO AnyPtr
                                )
                             -> JSIO TransformerStartCallback
  toTransformerStartCallback cb = primJS $ prim__toTransformerStartCallback cb

namespace TransformerTransformCallback

  export
  toTransformerTransformCallback :  (  AnyPtr
                                    -> TransformStreamDefaultController
                                    -> IO (Promise Undefined)
                                    )
                                 -> JSIO TransformerTransformCallback
  toTransformerTransformCallback cb = primJS $ prim__toTransformerTransformCallback cb

namespace UnderlyingSinkAbortCallback

  export
  toUnderlyingSinkAbortCallback :  ( UndefOr AnyPtr -> IO (Promise Undefined) )
                                -> JSIO UnderlyingSinkAbortCallback
  toUnderlyingSinkAbortCallback cb = primJS $ prim__toUnderlyingSinkAbortCallback cb

namespace UnderlyingSinkCloseCallback

  export
  toUnderlyingSinkCloseCallback :  (() -> IO (Promise Undefined))
                                -> JSIO UnderlyingSinkCloseCallback
  toUnderlyingSinkCloseCallback cb = primJS $ prim__toUnderlyingSinkCloseCallback cb

namespace UnderlyingSinkStartCallback

  export
  toUnderlyingSinkStartCallback :  (  WritableStreamDefaultController
                                   -> IO AnyPtr
                                   )
                                -> JSIO UnderlyingSinkStartCallback
  toUnderlyingSinkStartCallback cb = primJS $ prim__toUnderlyingSinkStartCallback cb

namespace UnderlyingSinkWriteCallback

  export
  toUnderlyingSinkWriteCallback :  (  AnyPtr
                                   -> WritableStreamDefaultController
                                   -> IO (Promise Undefined)
                                   )
                                -> JSIO UnderlyingSinkWriteCallback
  toUnderlyingSinkWriteCallback cb = primJS $ prim__toUnderlyingSinkWriteCallback cb

namespace UnderlyingSourceCancelCallback

  export
  toUnderlyingSourceCancelCallback :  (  UndefOr AnyPtr
                                      -> IO (Promise Undefined)
                                      )
                                   -> JSIO UnderlyingSourceCancelCallback
  toUnderlyingSourceCancelCallback cb = primJS $ prim__toUnderlyingSourceCancelCallback cb

namespace UnderlyingSourcePullCallback

  export
  toUnderlyingSourcePullCallback :  (  Union2 ReadableStreamDefaultController
                                              ReadableByteStreamController
                                    -> IO (Promise Undefined)
                                    )
                                 -> JSIO UnderlyingSourcePullCallback
  toUnderlyingSourcePullCallback cb = primJS $ prim__toUnderlyingSourcePullCallback cb

namespace UnderlyingSourceStartCallback

  export
  toUnderlyingSourceStartCallback :  (  Union2 ReadableStreamDefaultController
                                               ReadableByteStreamController
                                     -> IO AnyPtr
                                     )
                                  -> JSIO UnderlyingSourceStartCallback
  toUnderlyingSourceStartCallback cb = primJS $ prim__toUnderlyingSourceStartCallback cb


text:
> module SequentialDecisionProblems.applications.Main

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

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

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

> import FastSimpleProb.SimpleProb
> import FastSimpleProb.BasicOperations
> import FastSimpleProb.BasicProperties
> import FastSimpleProb.MonadicOperations
> import FastSimpleProb.MonadicProperties
> import FastSimpleProb.Measures
> import FastSimpleProb.MeasuresProperties
> import Sigma.Sigma
> import Sigma.Operations
> import Sigma.Properties
> import Nat.LTProperties
> import Double.Predicates
> import NonNegDouble.NonNegDouble
> import NonNegDouble.Constants
> import NonNegDouble.BasicOperations
> import NonNegDouble.Operations
> import NonNegDouble.Properties
> import NonNegDouble.Predicates
> import NonNegDouble.LTEProperties
> import NonNegDouble.Measures
> import NonNegDouble.MeasureProperties
> import Finite.Predicates
> import Finite.Operations
> import Finite.Properties
> import Unique.Predicates
> import Decidable.Predicates
> import LocalEffect.Exception
> import LocalEffect.StdIO
> import Fin.Operations
> import Fraction.Fraction
> import Fraction.Normal
> import Nat.Positive
> import List.Operations
> import Unit.Properties

> -- %default total
> %auto_implicits off

> -- %logging 5

* Introduction

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

* Controls

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

> SequentialDecisionProblems.CoreTheory.Ctrl _ _ = FreezeOrIncrease

* States

The decision maker can observe three values: the cumulated effects of
its own decisions, of the decisions taken by "others", and a state of
the world. The latter can be either good or bad

> SequentialDecisionProblems.CoreTheory.State t = (Nat, Nat, GoodOrBad)

The idea is that the world starts in a good state but, if the sum of the
cumulated emissions of the decision maker and of the "others" increase
beyond a certain threshold, there is a non-zero probability to turn to a
bad state. Once there, there is no chance to come back to a good state.

In this game, we assume that the decision maker and the "others" take
the same decisions in a competitive setup, see section on rewards.

* Transition function

> threshold : Nat
> threshold = Z

> p   :  Double
> p   =  1.0

> p1  :  NonNegDouble
> p1  =  cast (p   / (p + 1.0))
> p2  :  NonNegDouble
> p2  =  cast (1.0 / (p + 1.0))

> SequentialDecisionProblems.CoreTheory.nexts t (s1, s2, Good) Freeze =
>   if (s1 + s2 <= threshold)
>   then mkSimpleProb [((s1, s2, Good), one)]
>   else mkSimpleProb [((s1, s2, Good), p1), ((s1, s2, Bad), p2)]

> SequentialDecisionProblems.CoreTheory.nexts t (s1, s2, Good) Increase =
>   if (s1 + s2 <= threshold)
>   then mkSimpleProb [((S s1, S s2, Good), one)]
>   else mkSimpleProb [((S s1, S s2, Good), p1), ((S s1, S s2, Bad), p2)]

> SequentialDecisionProblems.CoreTheory.nexts t (s1, s2, Bad) Freeze =
>   mkSimpleProb [((s1, s2, Bad), one)]

> SequentialDecisionProblems.CoreTheory.nexts t (s1, s2, Bad) Increase =
>   mkSimpleProb [((S s1, S s2, Bad), one)]

* |Val| and |LTE|:

> SequentialDecisionProblems.CoreTheory.Val =
>   NonNegDouble.NonNegDouble

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

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

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

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

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

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

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

* Reward function

The idea is that, at every step, being in a good world yields more
benefits than being in a bad world:

> benefitsGood : NonNegDouble
> benefitsGood = one

> benefitsBad  : NonNegDouble
> benefitsBad  = NonNegDouble.Constants.zero

Freezing emissions also brings less benefits than increasing
emissions. However, increasing emissions in a bad world yields less
benefits than increasing emissions in a good world:

> benefitsFreeze : NonNegDouble
> benefitsFreeze = NonNegDouble.Constants.zero

> benefitsIncreaseGood : NonNegDouble
> benefitsIncreaseGood = one

> benefitsIncreaseBad : NonNegDouble
> benefitsIncreaseBad = cast 0.9

> using implementation NumNonNegDouble
>
>   SequentialDecisionProblems.CoreTheory.reward _ (_, _, _) Freeze   (_, _, Good) = benefitsGood + benefitsFreeze
>   SequentialDecisionProblems.CoreTheory.reward _ (_, _, _) Increase (_, _, Good) = benefitsGood + benefitsIncreaseGood
>   SequentialDecisionProblems.CoreTheory.reward _ (_, _, _) Freeze   (_, _,  Bad) = benefitsBad  + benefitsFreeze
>   SequentialDecisionProblems.CoreTheory.reward _ (_, _, _) Increase (_, _,  Bad) = benefitsBad  + benefitsIncreaseBad

* Completing the problem specification

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

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

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

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

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

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

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

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

> SequentialDecisionProblems.Utils.finiteViable n x = finiteUnit

> SequentialDecisionProblems.Utils.decidableViable n x = decidableUnit

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

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

which immediately implies |reachableSpec1|:

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

Finally, we have to show that controls are finite

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

* Optimal policies, optimal decisions, ...

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

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

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

> computation : { [STDIO] } Eff ()
> computation =
>   do putStr ("enter number of steps:\n")
>      nSteps <- getNat
>      case (decidableViable {t = Z} nSteps (Z, Z, Good)) of
>        (Yes v) => do putStrLn ("computing optimal policies ...")
>                      ps   <- pure (backwardsInduction Z nSteps)
>                      putStrLn ("computing optimal controls ...")
>                      mxys <- pure (possibleStateCtrlSeqs (Z, Z, Good) () v ps)
>                      putStrLn "possible state-control sequences:"
>                      putStr "  "
>                      putStrLn (show mxys)
>                      -- mvs <- pure (possibleRewards' mxys)
>                      -- putStrLn "possible rewards:"
>                      -- putStr "  "
>                      -- putStrLn (show mvs)
>                      -- mxyvs <- pure (possibleStateCtrlSeqsRewards' mxys)
>                      -- putStrLn "possible state-control sequences and rewards:"
>                      -- putStr "  "
>                      -- putStrLn (show mxyvs)
>                      -- putStrLn "measure of possible rewards: "
>                      -- putStr "  "
>                      -- putStrLn (show (meas mvs))
>                      -- argmaxmax <- pure (argmaxMax {A = StateCtrlSeq Z nSteps} {B = Val} totalPreorderLTE (support mxyvs) (nonEmptyLemma mxyvs))
>                      -- putStrLn "best possible state-control sequence: "
>                      -- putStr "  "
>                      -- putStrLn (show (fst argmaxmax))
>                      -- putStrLn "best possible reward: "
>                      -- putStr "  "
>                      -- putStrLn (show (snd argmaxmax))
>                      -- -- argminmin <- pure (argminMin totalPreorderLTE (support mxyvs) (nonEmptyLemma mxyvs))
>                      -- -- putStrLn "worst possible state-control sequence: "
>                      -- -- putStr "  "
>                      -- -- putStrLn (show (fst argminmin))
>                      -- -- putStrLn "worst possible reward: "
>                      -- -- putStr "  "
>                      -- -- putStrLn (show (snd argminmin))
>                      putStrLn ("done!")
>        (No _)  => putStrLn ("initial state non viable for " ++ cast {from = Int} (cast nSteps) ++ " steps")

> main : IO ()
> main = run computation

> {-

> ---}

[1] Stanford Encyclopedia of Phylosophy, Causal Decision Theory, 2010

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

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
module ProveVoid

%default total

data In : (f : Type -> Type) -> Type where
  MkIn : (f : Type -> Type) -> In f

tToT : Type -> Type
tToT i = Int

injIn' : {z : Type -> Type} -> {y : Type->Type} -> In z = In y -> z = y
injIn' {z=x} {y=x} (Refl {A=Type} {x=_}) = Refl

{-
injIn' : {A : Type} -> {z : A} -> {y : A} -> z = y -> z = y
injIn' Refl = Refl
-}

foo : Int
foo = 42

-- This step requires definitional type constructor injectivity and is
-- the source of the problem.
injIn : In z = In y -> z = y
injIn {z=z} {y=y} prf =
  case prf of
    (Refl {A=_} {x=_}) => Refl

P : Type -> Type
--P x = (a : (Type -> Type) ** (In a = x, a x -> Void))
P x = DPair (Type -> Type) (\a => (In a = x, a x -> Void))

InP : Type
InP = In P

func1 : P InP -> Void
func1 (v ** (inAEqXPrf, axIsVoidPrf)) =
  let
    lem1 = (injIn inAEqXPrf)
    lem2  = replace {P=\ x => x (In P) -> Void} lem1
    lem3 : (P (In P) -> Void) = lem2 axIsVoidPrf
    ans = lem3 (P ** (Refl, lem3))
  in ?xxx --

total -- for extra oumph!
lem2 : Void
lem2 =
  let foo : P InP = (P ** (Refl, func1))
      ans = func1 foo
  in ?xxx2

fee : Type -> Type
--fee x = (b : Type ** List b)
fee x = DPair Type (\b => List b)
--fee x = DPair Type List

x : Int -> Int
x = (\z => 52)

ext: idr


text:
module DepSec.Lattice

import public DepSec.Poset

%access public export
%hide Prelude.Monad.join
%default total

||| Verified join semilattice
interface JoinSemilattice a where
  join : a -> a -> a
  associative : (x, y, z : a) -> x `join` (y `join` z) = (x `join` y) `join` z
  commutative : (x, y : a)    -> x `join` y = y `join` x
  idempotent  : (x : a)       -> x `join` x = x

||| A well defined join induces a partial ordering.
implementation JoinSemilattice a => Poset a where
  leq x y = (x `join` y = y)
  reflexive = idempotent
  antisymmetric x y lexy leyx =
    rewrite sym $ lexy in
    rewrite commutative x y in
    rewrite sym $ leyx in Refl
  transitive x y z lexy leyx =
    rewrite sym $ leyx in
    rewrite associative x y z in
    rewrite sym $ lexy in Refl

||| A join-semilattice with an identity element (the lattices' bottom)
||| of the join operation.
interface JoinSemilattice a => BoundedJoinSemilattice a where
  Bottom : a
  unitary : (e : a) -> e `join` Bottom = e

||| Decidable partial ordering
decLeq : JoinSemilattice a => DecEq a => (x, y : a) -> Dec (x `leq` y)
decLeq x y = decEq (x `join` y) y

--------------------------------------------------------------------------------
--- Lemmas
--------------------------------------------------------------------------------
leq_bot_x : BoundedJoinSemilattice lt
         => (x : lt)
         -> Bottom `leq` x
leq_bot_x x =
  rewrite commutative Bottom x in
  unitary x

join_x_xy : JoinSemilattice lt
          => (x, y: lt)
          -> join x (join x y) = join x y
join_x_xy x y =
  rewrite associative x x y in
  rewrite idempotent x in Refl

join_y_xy : JoinSemilattice lt
         => (x, y : lt)
         -> join y (join x y) = join x y
join_y_xy x y =
  rewrite commutative x y in
  rewrite associative y y x in
  rewrite idempotent y in Refl

max_stars_repo_name: simongregersen/DepSec

max_issues_repo_name: simongregersen/DepSec

max_forks_repo_name: simongregersen/DepSec


text:
module Skeletons

import public Skeletons.Farm
import public Skeletons.Pipeline


text:
module Main

import System

printLength : IO ()
printLength = getLine >>= \input => let len = length input in putStrLn $ show len

printLengthDo : IO ()
printLengthDo = do
              input <- getLine
              let len = length input
              putStrLn $ show len

printLonger : IO ()
printLonger = putStrLn "Enter the first string:" >>= \_ =>
              getLine >>= \inp1 =>
              putStrLn "Enter the second string:" >>= \_ =>
              getLine >>= \inp2 =>
              let len1 = length inp1 in
              let len2 = length inp2 in
              if len1 > len2 then
                 putStr ("The length of the longer string is " ++ (show len1) ++ "\n")
              else
                 putStr ("The length of the longer string is " ++ (show len2) ++ "\n")

printLongerDo : IO ()
printLongerDo = do
            putStrLn "Enter the first string:"
            inp1 <- getLine
            putStrLn "Enter the second string:"
            inp2 <- getLine
            let len1 = length inp1
            let len2 = length inp2
            if len1 > len2 then
               putStr ("The length of the longer string is " ++ (show len1) ++ "\n")
            else
               putStr ("The length of the longer string is " ++ (show len2) ++ "\n")

readNumber : IO (Maybe Nat)
readNumber = do
           input <- getLine
           if all isDigit (unpack input) then
              pure $ Just (cast input)
           else
              pure Nothing

readPair : IO (String, String)
readPair = do
         str1 <- getLine
         str2 <- getLine
         pure (str1, str2)

usePair : IO ()
usePair = do
          (str1, str2) <- readPair
          putStrLn ("You entered " ++ str1 ++ " and " ++ str2)

-- We can directly pattern match on values obtained by executing some action
-- Alternative case matches can be provided after the vertical bar like below
readNumbers : IO (Maybe (Nat, Nat))
readNumbers = do
              Just num1_ok <- readNumber | Nothing => pure Nothing
              Just num2_ok <- readNumber | Nothing => pure Nothing
              pure (Just (num1_ok, num2_ok))

guess : (target : Nat) -> (guesses : Nat) -> IO ()
guess target guesses = do
             putStrLn "Guess the number:"
             Just no <- readNumber
           | Nothing => do putStrLn "The entered input is invalid. Please try again!"
                           guess target guesses
             let newGuesses = guesses + 1
             putStrLn ("You have guessed " ++ (show newGuesses) ++ " times")
             case compare no target of
                  LT => do putStrLn "The number you have entered is too low. Please try again!"
                           guess target newGuesses
                  GT => do putStrLn "The number you have entered is too high. Please try again!"
                           guess target newGuesses
                  EQ => putStrLn "The number you have entered is correct. Congrats!"

myrepl : (prompt : String) -> (onInput : String -> String) -> IO ()
myrepl prompt onInput = do
                      putStrLn prompt
                      input <- getLine
                      putStrLn $ onInput input
                      myrepl prompt onInput

myreplWith : (state : a) -> (prompt : String) ->
             (onInput : a -> String -> Maybe (String, a)) -> IO ()
myreplWith state prompt onInput =
           do putStrLn prompt
              input <- getLine
              case onInput state input of
                   Just (output, newState)
                        => do putStrLn output
                              myreplWith newState prompt onInput
                   Nothing => putStrLn ""

main : IO ()
main = do
     rint <- time
     let no = fromInteger (rint) `modNat` 100
     guess no 0

max_stars_repo_name: balajisivaraman/idris-book

max_issues_repo_name: balajisivaraman/idris-book

max_forks_repo_name: balajisivaraman/idris-book


text:
import Stuff

efn : ((0 x : Nat) -> Nat -> Nat) -> Nat
efn f = f (S Z) (S Z)

okfn : ((x : Nat) -> Nat -> Nat) -> Nat
okfn f = f (S Z) (S Z)

ignore : (0 x : Nat) -> Nat -> Nat
ignore x y = y

lin : (1 x : Nat) -> Nat -> Nat
lin x y = S x


text:
module TryIndex

import Data.Vect

%default total

tryIndex : { n : _ } -> Integer -> Vect n elem -> Maybe elem
tryIndex m xs = case integerToFin m n of
                     Nothing => Nothing
                     Just idx => Just $ index idx xs

vi : Vect 5 Int
vi = [1, 2, 3, 4, 5]

max_stars_repo_name: timmyjose-study/tdd-with-idris

max_issues_repo_name: timmyjose-study/tdd-with-idris

max_forks_repo_name: timmyjose-study/tdd-with-idris


text:
module Libgit.Object

import Control.Monad.Managed

import Libgit.FFI
import Libgit.Oid
import Libgit.Types

enrichGitObject : AnyPtr -> (typ ** GitObject typ)
enrichGitObject ptr =
  let objTyp = gitObjectTypeFromInt (git_object_type ptr) in
    (objTyp ** MkGitObject ptr)

withGitObject : GitRepository
             -> GitOid
             -> (GitResult (typ ** GitObject typ) -> IO a)
             -> IO a
withGitObject (MkGitRepository repoPtr) (MkGitOid oidPtr) act = do
  let cgr = git_lookup_object repoPtr oidPtr (gitObjectTypeToInt GitObjectAny)
  result <- getGitResult cgr
  let objResult = enrichGitObject <$> result
  actResult <- act objResult
  case result of
    Right ptr => pure actResult <* primIO (prim_git_object_free ptr)
    Left _ => pure actResult

||| Retrieve an object of any type from a Git repository.
|||
||| Returns on success a dependent pair of the object's type and a managed
||| reference to the object.
||| Returns on failure a Git error code.
|||
||| @repo The GitRepository to retrieve the object from.
||| @oid  The object ID to retrieve from the repository.
export
gitObject : (repo : GitRepository)
         -> (oid : GitOid)
         -> Managed (GitResult (typ ** GitObject typ))
gitObject repo oid = managed (withGitObject repo oid)

||| Retrieve an object of any type from a Git repository based on the object
||| ID's string representation.
|||
||| Returns on success a dependent pair of the object's type and a managed
||| reference to the object.
||| Returns on failure a Git error code.
|||
||| @repo The GitRepository to retrieve the object from.
||| @str  The string representation of an object ID.
export
gitObjectFromString : GitRepository
                   -> String
                   -> Managed (GitResult (typ ** GitObject typ))
gitObjectFromString repo str = do
  Right oid <- oidFromString str
    | Left err => pure (Left err)
  gitObject repo oid

withParsedRev : (repo : GitRepository)
             -> (rev : String)
             -> (GitResult (typ ** GitObject typ) -> IO a)
             -> IO a
withParsedRev (MkGitRepository repo) rev act = do
  cgr <- primIO (prim_git_single_revparse repo rev)
  (err, ptr) <- getGitResultPair cgr
  let revResult = enrichGitObject <$> toGitResult err ptr
  result <- act revResult
  primIO (prim_git_object_free ptr)
  pure result

||| Parse a formatted revision string into a Git object.
|||
||| Returns on success a managed reference to the Git object.
||| Returns on failure a Git error code.
|||
||| @repo The Git repository to perform the lookup in.
||| @rev  The string, formatted per the git revision spec
|||       http://git-scm.com/docs/git-rev-parse.html#_specifying_revisions),
|||       to parse into an object.
export
revParse : (repo : GitRepository)
        -> (rev : String)
        -> Managed (GitResult (typ ** GitObject typ))
revParse repo rev = managed (withParsedRev repo rev)

withTypedGitObject : GitRepository
                  -> GitOid
                  -> (typ : GitObjectType)
                  -> (GitResult (GitObject typ) -> IO a)
                  -> IO a
withTypedGitObject (MkGitRepository repoPtr) (MkGitOid oidPtr) typ act = do
  let cgr = git_lookup_object repoPtr oidPtr (gitObjectTypeToInt typ)
  result <- getGitResult cgr
  actResult <- act (MkGitObject <$> result)
  case result of
    Right ptr => pure actResult <* primIO (prim_git_object_free ptr)
    Left _ => pure actResult

||| Retrieve an object of a specific type from a Git repository.
|||
||| Returns on success a managed reference to the object.
||| Returns on failure a Git error code.
|||
||| @repo The GitRepository to retrieve the object from.
||| @oid  The object ID to retrieve from the repository.
||| @typ  The GitObjectType of the object to retrieve.
export
typedGitObject : GitRepository
              -> GitOid
              -> (typ : GitObjectType)
              -> Managed (GitResult (GitObject typ))
typedGitObject repo oid typ = managed (withTypedGitObject repo oid typ)

||| Retrieve an object of a specific type from a Git repository based on the
||| object ID's string representation.
|||
||| Returns on success a managed reference to the object.
||| Returns on failure a Git error code.
|||
||| @repo The GitRepository to retrieve the object from.
||| @str  The string representation of an object ID.
||| @typ  The GitObjectType of the object to retrieve.
export
typedGitObjectFromString : GitRepository
                        -> String
                        -> (typ : GitObjectType)
                        -> Managed (GitResult (GitObject typ))
typedGitObjectFromString repo str typ = do
  Right oid <- oidFromString str
    | Left err => pure (Left err)
  managed (withTypedGitObject repo oid typ)

max_forks_repo_name: bigs/libgit-idris


text:
import Data.Vect

myReverse : Vect n elem -> Vect n elem
myReverse [] = []
myReverse {n = S k} (x :: xs) = reverseProof x xs (myReverse xs ++ [x])
  where
    reverseProof : Vect (k + 1) elem -> Vect (S k) elem
    reverseProof {k} result = rewrite (plusCommutative 1 k) in result


text:
{-
 - Associated YT tutorial: https://youtu.be/TEWy9vZcxW4
 -
 - Launch REPL with:
 - > idris -p contrib -p effects
 -
-}
import Util

||| Inputs (samplex x inputs)
X : Matrix 3 4 Double
X = [[1, 2, 3, 2.5],
     [2.0, 5.0, -1.0, 2.0],
     [-1.5, 2.7, 3.3, -0.8]]

||| Data structure for a dense layer
record Layer_Dense (n_inputs : Nat) (n_neurons : Nat) where
  constructor MkLayer_Dense
  weights : Matrix n_inputs n_neurons Double
  biases : Vect n_neurons Double
-- Note: can't make output a field, since we don't don't know
--       how many samples we'll be given

||| Smart constructor for a dense layer
newLayer_Dense : (n_inputs : Nat) ->
                 (n_neurons : Nat) ->
                 Eff (Layer_Dense n_inputs n_neurons) [RND]
newLayer_Dense n_inputs n_neurons = pure $
  MkLayer_Dense
    !(rndMat n_inputs n_neurons (-1) 1)
    (zeroVect n_neurons)

||| Feed inputs into the layer and compute outputs
forward : Layer_Dense i n -> Matrix m i Double -> Matrix m n Double
forward layer inputs = (inputs <> (weights layer)) <+ (biases layer)

main : IO ()
main = do
  let layer1 = runPure $ newLayer_Dense 4 5
  let layer2 = runPure $ newLayer_Dense 5 2
  let output1 = forward layer1 X
  -- printLn $ output1
  let output2 = forward layer2 output1
  printLn $ output2


text:
import Fuel

%default total

public export
data InfIO : Type where
  Do : IO a -> (a -> Inf InfIO) -> InfIO

public export
(>>=) : IO a -> (a -> Inf InfIO) -> InfIO
(>>=) = Do

public export
run : Fuel -> InfIO -> IO ()
run (More fuel) (Do c f) = do
  res <- c
  run fuel (f res)
run Dry _ = putStrLn "Out of Fuel"

max_stars_repo_name: tekerson/type-driven-development

max_issues_repo_name: tekerson/type-driven-development

max_forks_repo_name: tekerson/type-driven-development


text:
module Compiler.LLVM.Instruction

import Data.Vect

import Control.Codegen
import Compiler.LLVM.IR
import Data.Utils

-- TODO: get rid of this instance, replace usage with lower-level calls
export
ToIR String where
  toIR = id
  showWithoutType = id

export
load : {t : IRType} -> IRValue (Pointer n t) -> Codegen (IRValue t)
load IRDiscard = pure nullPtr
load {t} mv = do
  loaded <- assignSSA $ "load " ++ (show t) ++ ", " ++ (toIR mv)
  pure $ SSA t loaded

export
store : {t : IRType} -> IRValue t -> IRValue (Pointer n t) -> Codegen ()
store _ IRDiscard = pure ()
store {t} v dst = do
  appendCode $ "  store " ++ (toIR v) ++ ", " ++ (toIR dst)

export
icmp : {t : IRType} -> String -> IRValue t -> IRValue t -> Codegen (IRValue I1)
icmp {t} cond a b = do
  compare <- assignSSA $ "icmp " ++ cond ++ " " ++ (show t) ++ " " ++ showWithoutType a ++ ", " ++ showWithoutType b
  pure $ SSA I1 compare

export
fcmp : String -> IRValue F64 -> IRValue F64 -> Codegen (IRValue I1)
fcmp cond a b = do
  compare <- assignSSA $ "fcmp " ++ cond ++ " double " ++ showWithoutType a ++ ", " ++ showWithoutType b
  pure $ SSA I1 compare

export
mkZext : {to : IRType} -> IRValue from -> Codegen (IRValue to)
mkZext {to} val = (SSA to) <$> assignSSA ("zext " ++ toIR val ++ " to " ++ show to)

export
mkSext : {to : IRType} -> IRValue from -> Codegen (IRValue to)
mkSext {to} val = (SSA to) <$> assignSSA ("sext " ++ toIR val ++ " to " ++ show to)

export
fptosi : {to : IRType} -> IRValue from -> Codegen (IRValue to)
fptosi {to} val = (SSA to) <$> assignSSA ("fptosi " ++ toIR val ++ " to " ++ show to)

export
fptoui : {to : IRType} -> IRValue from -> Codegen (IRValue to)
fptoui {to} val = (SSA to) <$> assignSSA ("fptoui " ++ toIR val ++ " to " ++ show to)

export
sitofp : {to : IRType} -> IRValue from -> Codegen (IRValue to)
sitofp {to} val = (SSA to) <$> assignSSA ("sitofp " ++ toIR val ++ " to " ++ show to)

export
uitofp : {to : IRType} -> IRValue from -> Codegen (IRValue to)
uitofp {to} val = (SSA to) <$> assignSSA ("uitofp " ++ toIR val ++ " to " ++ show to)

export
phi : {t : IRType} -> List (IRValue t, IRLabel) -> Codegen (IRValue t)
phi xs = (SSA t) <$> assignSSA ("phi " ++ show t ++ " " ++ showSep ", " (map getEdge xs)) where
  getEdge : (IRValue t, IRLabel) -> String
  getEdge (val, lbl) = "[ " ++ showWithoutType val ++ ", " ++ showWithoutType lbl ++ " ]"

export
getElementPtr : {t : IRType} -> {n : Int} -> IRValue (Pointer n t) -> IRValue ot -> Codegen (IRValue (Pointer n t))
getElementPtr {t} {n} ptr offset =
  SSA (Pointer n t) <$> assignSSA ("getelementptr inbounds " ++ show t ++ ", " ++ toIR ptr ++ ", " ++ toIR offset)

export
bitcastA : {from : IRType} -> {to : IRType} -> {n : Int} -> IRValue from -> Codegen (IRValue (Pointer n to))
bitcastA {from} {to} {n} val = (SSA (Pointer n to)) <$> assignSSA ("bitcast " ++ toIR val ++ " to " ++ show (Pointer n to))

export
mkBinOp : {t : IRType} -> String -> IRValue t -> IRValue t -> Codegen (IRValue t)
mkBinOp {t} s a b = do
  result <- assignSSA $ s ++ " " ++ (show t) ++ " " ++ showWithoutType a ++ ", " ++ showWithoutType b
  pure $ SSA t result

export
mkXOr : {t : IRType} -> IRValue t -> IRValue t -> Codegen (IRValue t)
mkXOr = mkBinOp "xor"

export
mkOr : {t : IRType} -> IRValue t -> IRValue t -> Codegen (IRValue t)
mkOr = mkBinOp "or"

export
mkAnd : {t : IRType} -> IRValue t -> IRValue t -> Codegen (IRValue t)
mkAnd = mkBinOp "and"

export
mkAdd : {t : IRType} -> IRValue t -> IRValue t -> Codegen (IRValue t)
mkAdd = mkBinOp "add"

export
mkAddNoWrap : {t : IRType} -> IRValue t -> IRValue t -> Codegen (IRValue t)
mkAddNoWrap = mkBinOp "add nuw nsw"

export
mkMul : {t : IRType} -> IRValue t -> IRValue t -> Codegen (IRValue t)
mkMul = mkBinOp "mul"

export
mkSub : {t : IRType} -> IRValue t -> IRValue t -> Codegen (IRValue t)
mkSub = mkBinOp "sub"

export
mkSDiv : {t : IRType} -> IRValue t -> IRValue t -> Codegen (IRValue t)
mkSDiv = mkBinOp "sdiv"

export
mkSRem : {t : IRType} -> IRValue t -> IRValue t -> Codegen (IRValue t)
mkSRem = mkBinOp "srem"

export
mkUDiv : {t : IRType} -> IRValue t -> IRValue t -> Codegen (IRValue t)
mkUDiv = mkBinOp "udiv"

export
mkURem : {t : IRType} -> IRValue t -> IRValue t -> Codegen (IRValue t)
mkURem = mkBinOp "urem"

export
mkShiftL : {t : IRType} -> IRValue t -> IRValue t -> Codegen (IRValue t)
mkShiftL = mkBinOp "shl"

export
mkShiftR : {t : IRType} -> IRValue t -> IRValue t -> Codegen (IRValue t)
mkShiftR = mkBinOp "lshr"

export
mkAShiftR : {t : IRType} -> IRValue t -> IRValue t -> Codegen (IRValue t)
mkAShiftR = mkBinOp "ashr"

export
unlikely : IRValue I1 -> Codegen (IRValue I1)
unlikely cond = (SSA I1) <$> assignSSA (" call ccc i1 @llvm.expect.i1(" ++ toIR cond ++ ", i1 0)")

export
likely : IRValue I1 -> Codegen (IRValue I1)
likely cond = (SSA I1) <$> assignSSA (" call ccc i1 @llvm.expect.i1(" ++ toIR cond ++ ", i1 1)")

export
branch : IRValue I1 -> (true : IRLabel) -> (false : IRLabel) -> Codegen ()
branch cond whenTrue whenFalse =
  appendCode $ "br " ++ toIR cond ++ ", " ++ toIR whenTrue ++ ", " ++ toIR whenFalse

export
jump : IRLabel -> Codegen ()
jump to =
  appendCode $ "br " ++ toIR to

export
mkIf_ : (cond : Codegen (IRValue I1)) ->
        (true : Codegen ()) ->
        (false : Codegen ()) ->
        Codegen ()
mkIf_ cond true false = do
  lblTrue <- genLabel "t"
  lblTrueEnd <- genLabel "te"
  lblFalse <- genLabel "f"
  lblFalseEnd <- genLabel "fe"
  lblEnd <- genLabel "e"

  branch !(cond) lblTrue lblFalse
  beginLabel lblTrue
  true
  jump lblTrueEnd
  beginLabel lblTrueEnd
  jump lblEnd
  beginLabel lblFalse
  false
  jump lblFalseEnd
  beginLabel lblFalseEnd
  jump lblEnd
  beginLabel lblEnd

export
mkIf : {t : IRType} ->
       (cond : Codegen (IRValue I1)) ->
       (true : Codegen (IRValue t)) ->
       (false : Codegen (IRValue t)) ->
               Codegen (IRValue t)
mkIf cond true false = do
  lblTrue <- genLabel "t"
  lblTrueEnd <- genLabel "te"
  lblFalse <- genLabel "f"
  lblFalseEnd <- genLabel "fe"
  lblEnd <- genLabel "e"

  branch !(cond) lblTrue lblFalse
  beginLabel lblTrue
  valTrue <- true
  jump lblTrueEnd
  beginLabel lblTrueEnd
  jump lblEnd
  beginLabel lblFalse
  valFalse <- false
  jump lblFalseEnd
  beginLabel lblFalseEnd
  jump lblEnd
  beginLabel lblEnd
  phi [(valTrue, lblTrueEnd), (valFalse, lblFalseEnd)]

export
mkSelect : {t : IRType} -> IRValue I1 -> IRValue t -> IRValue t -> Codegen (IRValue t)
mkSelect {t} s a b = do
  (SSA t) <$> assignSSA ("select " ++ toIR s ++ ", " ++ toIR a ++ ", " ++ toIR b)

export
mkMin : {t : IRType} -> IRValue t -> IRValue t -> Codegen (IRValue t)
mkMin {t} a b = do
  aSmaller <- icmp "slt" a b
  (SSA t) <$> assignSSA ("select " ++ toIR aSmaller ++ ", " ++ toIR a ++ ", " ++ toIR b)

export
mkMax : {t : IRType} -> IRValue t -> IRValue t -> Codegen (IRValue t)
mkMax {t} a b = do
  aLarger <- icmp "sgt" a b
  (SSA t) <$> assignSSA ("select " ++ toIR aLarger ++ ", " ++ toIR a ++ ", " ++ toIR b)

export
voidCall : String -> String -> Vect n String -> Codegen ()
voidCall cconv name args =
  appendCode $ "  call " ++ cconv ++ " void " ++ name ++ "(" ++ (showSep ", " (toList args)) ++ ")"

export
call : {t : IRType} -> String -> String -> Vect n String -> Codegen (IRValue t)
call {t} cconv name args =
  SSA t <$> (assignSSA $ "  call " ++ cconv ++ " " ++ show t ++ " " ++ name ++ "(" ++ (showSep ", " (toList args)) ++ ")")

export
mkTrunc : {to : IRType} -> IRValue from -> Codegen (IRValue to)
mkTrunc {to} val = (SSA to) <$> assignSSA ("trunc " ++ toIR val ++ " to " ++ show to)

export
mkAbs : IRValue I32 -> Codegen (IRValue I32)
mkAbs val = call "ccc" "@rapid.abs.i32" [toIR val, "i1 1"]

export
mkAbs64 : IRValue I64 -> Codegen (IRValue I64)
mkAbs64 val = call "ccc" "@rapid.abs.i64" [toIR val, "i1 1"]


text:
-- -------------------------------------------------------------- [ Errmsg.idr ]
-- Module      : Lightyear.Errmsg
-- Description : Error message formatting.
--
-- This code is distributed under the BSD 2-clause license.
-- See the file LICENSE in the root directory for its full text.
-- --------------------------------------------------------------------- [ EOH ]
module Errmsg

import Lightyear.Core

%access export
-- ------------------------------------------------------------------- [ Begin ]

interface Layout str where
  lineLengths : str -> List Int

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

private
rowcol : List Int -> List Int -> (Int, Int)
rowcol       ws        []  = (0,0)  -- should not happen
rowcol (w :: ws) (x :: []) = (1 + (nat2int $ length ws), 1 + w-x)
rowcol (w :: ws) (x :: xs) = rowcol ws xs
rowcol       []        xs  = (0,0)  -- should not happen

private
formatItem : Layout str => str
                        -> (str, String)
                        -> String
formatItem whole (rest, msg)
  = let (row, col) = rowcol (reverse $ lineLengths whole) (reverse $ lineLengths rest)
    in "at " ++ show row ++ ":" ++ show col ++ " expected:\n  " ++ msg

formatError : Layout str => str
                         -> List (str, String)
                         -> String
formatError whole = unlines . map (formatItem whole)
-- --------------------------------------------------------------------- [ EOF ]

max_stars_repo_name: david-christiansen/lightyear

max_issues_repo_name: david-christiansen/lightyear

max_forks_repo_name: david-christiansen/lightyear


text:
module Main

import Erlang

readFile : String -> IO (Maybe String)
readFile filename = do
  Right result <- erlCall "file" "read_file" [filename]
    | Left _ => do
      putStrLn "Failed to read file"
      pure Nothing
  let Right (MkTuple2 ok content) = erlDecode
        (tuple2 (exact (MkAtom "ok")) string)
        result
    | Left _ => do
      putStrLn "Failed to decode"
      pure Nothing
  pure $ Just content

main : IO ()
main = do
  Just content <- readFile "secret.txt"
    | Nothing => putStrLn "Failed to read content"
  putStrLn content

examplePerson : ErlAnyMap
examplePerson = insert "loves_idris" (MkAtom "true") $ insert "age" 33 $ insert "name" "Christian" empty

record Person where
  constructor MkPerson
  name : String
  age : Integer
  lovesIdris : Bool

Show Person where
  show (MkPerson name age lovesIdris) = "(MkPerson " ++ show name ++ " " ++ show age ++ " " ++ show lovesIdris ++ ")"

main2 : IO ()
main2 = do
  let Just result = erlDecodeMay
        (mapSubset
          [ "name" := string
          , "age" := integer
          , "loves_idris" := bool
          ])
        examplePerson
    | Nothing => putStrLn "Unable to decode person"
  let name = get "name" result
  let age = get "age" result
  let lovesIdris = get "loves_idris" result
  printLn (MkPerson name age lovesIdris)


text:
import Aoc
import Data.List
import Data.List1
import Data.Strings
import Data.SortedMap
import Debug.Trace

data Production = Terminal String | NTs (List (List Int))
Show Production where
  show (Terminal s) = show s
  show (NTs s) = show s

Rules : Type
Rules = SortedMap Int Production

toRules : List (Int, Production) -> Rules
toRules = fromList

parseRule : String -> Maybe (Int, Production)
parseRule s = do
  (sn:::[rest]) <- pure (split (==':') s) | _ => Nothing
  n <- parsePositive {a=Int} sn
  case split (=='"') rest of
    (" ":::[t,""]) => Just (n, Terminal t)
    _ =>
      let parseChain = traverse parsePositive . forget . split (==' ') . trim
      in case traverse parseChain . forget . split (=='|') . trim $ rest of
        Just nts => Just (n, NTs nts)
        Nothing => Nothing

munch : Eq a => List a -> List a -> Maybe (List a)
munch [] ys = Just ys
munch (x::xs) [] = Nothing
munch (x::xs) (y::ys) = if x == y then munch xs ys else Nothing

mutual
  matches : Rules -> Int -> List Char -> List (List Char)
  matches rs k cs =
    case lookup k rs of
      Nothing => []
      Just (Terminal t) => toList $ munch (unpack t) cs
      Just (NTs alts) => do
        alt <- alts
        matchesSeq rs alt cs

  matchesSeq : Rules -> List Int -> List Char -> List (List Char)
  matchesSeq rs [] cs = [cs]
  matchesSeq rs (k::ks) cs = do
    cs' <- matches rs k cs
    matchesSeq rs ks cs'

matchesFully : Rules -> Int -> String -> Bool
matchesFully rs k s = any (==[]) $ matches rs k (unpack s)

main : IO ()
main = do
  (ls1:::[ls2]) <- readParagraphs | _ => putStrLn "paragraph parse error"
  Just rules <- pure $ toRules <$> traverse parseRule ls1 | _ => putStrLn "rule parse error"
  putStr "*   "; printLn $ count (matchesFully rules 0) ls2
  let rules' = insert 8 (NTs [[42,8],[42]]) $ insert 11 (NTs [[42,31],[42,11,31]]) $ rules
  putStr "**  "; printLn $ count (matchesFully rules' 0) ls2


text:
import Data.Vect

%default total

-- variable

-- function1 incr

-- function2 add

-- adt sum type

-- function adt show

-- Nat

-- mylist

-- variable xs vect

-- vtake

-- vtake to string

-- vappend


text:
module Circuits.Idealised.Types

import Decidable.Equality

import Data.List.Elem

import public Circuits.Common

%default total

public export
data GateKind = AND  | IOR  | XOR
              | ANDN | IORN | XORN | JOIN

export
Show GateKind where
  show AND  = "and"
  show IOR  = "or"
  show XOR  = "xor"
  show ANDN = "nand"
  show IORN = "nor"
  show XORN = "xnor"
  show JOIN = "join"

public export
data Direction = INPUT | OUTPUT

Uninhabited (INPUT = OUTPUT) where
  uninhabited Refl impossible

DecEq Direction where
  decEq INPUT INPUT   = Yes Refl
  decEq INPUT OUTPUT  = No absurd
  decEq OUTPUT INPUT  = No (negEqSym absurd)
  decEq OUTPUT OUTPUT = Yes Refl

export
Show Direction where
  show INPUT  = "input"
  show OUTPUT = "output"

public export
data PortHasProperties : Direction -> DType -> (Direction, DType) -> Type
  where
    PortHas : PortHasProperties flow type (flow,type)

public export
data Ty : Type where
  TyUnit : Ty
  TyPort : (Direction, DType) -> Ty

  TyGate : Ty

export
Show Ty where
  show TyUnit = "()"
  show (TyPort (d,t)) = concat ["TyPort(", show d, ",", show t, ")"]
  show TyGate = "TyGate"

Uninhabited (TyUnit = (TyPort x)) where
  uninhabited Refl impossible

Uninhabited (TyUnit = TyGate) where
  uninhabited Refl impossible

Uninhabited (TyPort x = TyGate) where
  uninhabited Refl impossible

export
DecEq Ty where
  decEq TyUnit TyUnit = Yes Refl
  decEq TyUnit (TyPort x) = No absurd
  decEq TyUnit TyGate = No absurd

  decEq (TyPort x) TyUnit = No (negEqSym absurd)
  decEq (TyPort x) (TyPort y) with (decEq x y)
    decEq (TyPort x) (TyPort x) | (Yes Refl)
      = Yes Refl
    decEq (TyPort x) (TyPort y) | (No contra)
      = No (\Refl => contra Refl)
  decEq (TyPort x) TyGate = No (absurd)

  decEq TyGate TyUnit = No (negEqSym absurd)
  decEq TyGate (TyPort x) = No (negEqSym absurd)
  decEq TyGate TyGate = Yes Refl

public export
data Used : (Ty, Usage) -> Type where
  IsUsed : Used (type, USED)

Uninhabited (Used (type,FREE)) where
  uninhabited IsUsed impossible

export
used : (p : (Ty,Usage)) -> Dec (Used p)
used (ty,USED) = Yes IsUsed
used (ty,FREE) = No absurd

public export
data Use : (old : List (Ty, Usage))
        -> (prf : Elem (type,FREE) old)
        -> (new : List (Ty, Usage))
        -> Type
  where
    H : Use ((type,FREE) :: rest)
            Here
            ((type,USED) :: rest)
    T : Use old later new
     -> Use ((type',usage')::old) (There later) ((type',usage')::new)

export
use : (ctxt : List (Ty, Usage))
   -> (prf : Elem (type, FREE) ctxt)
          -> (DPair (List (Ty, Usage))
                    (Use ctxt prf))
use ((type, FREE) :: xs) Here
  = (MkDPair ((type, USED) :: xs) H)
use ((y, z) :: xs) (There x) with (use xs x)
  use ((y, z) :: xs) (There x) | ((MkDPair fst snd))
    = (MkDPair ((y, z) :: fst) (T snd))

export
useAlt : {ctxt : List (Ty, Usage)}
      -> (prf : Elem (type, FREE) ctxt)
             -> (DPair (List (Ty, Usage))
                       (Use ctxt prf))
useAlt {ctxt = ((type, FREE) :: xs)} Here
  = MkDPair ((type, USED) :: xs) H
useAlt {ctxt = (y :: xs)} (There x) with (useAlt x)
  useAlt {ctxt = ((y, z) :: xs)} (There x) | (MkDPair fst snd) = MkDPair ((y, z) :: fst) (T snd)

-- [ EOF ]

max_stars_repo_name: gallais/linear-circuits

max_issues_repo_name: gallais/linear-circuits

max_forks_repo_name: gallais/linear-circuits


text:
module Main

import Cairo

PRIME : Felt
PRIME = fromInteger 3618502788666131213697322783095070105623107215331596699973092056135872020481

-- The +1 -1 simulates integer division on this specific felt
HALF : Felt
HALF = ((PRIME + 1) `div` 2) -1

%noinline
main : Cairo ()
main = do
    output HALF
    output (HALF + 1)
    let r = 1 `div` 3
    output r
    output (r * 3)

max_stars_repo_name: skyro-compiler/skyro

max_issues_repo_name: skyro-compiler/skyro

max_forks_repo_name: skyro-compiler/skyro


text:
data Foo : Nat -> Type where

0 G : (0 yv : Nat) -> Type
G yv = Foo yv -> Bool

partial
f : (0 x : Nat) -> Nat
f x = case G x of
           (Foo x' -> _) => x'


text:
module NCurses.Types

import Data.Nat

%default total

||| Window size.
public export
record Size where
  constructor MkSize
  height : Nat
  width  : Nat

||| Position
public export
record Position where
  constructor MkPosition
  row : Nat
  col : Nat

export
MkRow : Nat -> Position
MkRow n = MkPosition n 0

export
up : Position -> Position
up = { row $= pred }

export
down : Position -> Position
down = { row $= S }

export
left : Position -> Position
left = { col $= pred }

export
right : Position -> Position
right = { col $= S }

public export
data CursorVisibility = CInvisible | CNormal| CHighlyVisible

||| Keys that can be used when keypad is turned on.
public export
data Key = F0
         | F1
         | F2
         | F3
         | F4
         | F5
         | F6
         | F7
         | F8
         | F9
         | F10
         | F11
         | F12
         | Up
         | Down
         | Left
         | Right
         | Backspace

export
allKeys : List Key
allKeys = [F0, F1, F2, F3, F4, F5, F6, F7, F8, F9, F10, F11, F12
          , Up, Down, Left, Right
          , Backspace
          ]

||| The default ncurses colors that can be used in constructing
||| color pairs.
public export
data Color
  = Black
  | Red
  | Green
  | Yellow
  | Blue
  | Magenta
  | Cyan
  | White

||| Attributes that can be given to text within an ncurses window.
||| @ cp is the representation of colour pairs
public export
data Attribute' cp
  = Normal
  | Underline
  | Standout
  | Reverse
  | Blink
  | Dim
  | Bold
  | Protected
  | Invisible
  | CP cp

max_stars_repo_name: gallais/ncurses-idris

max_issues_repo_name: gallais/ncurses-idris

max_forks_repo_name: gallais/ncurses-idris