text:
||| This module provides interfaces similar to `Applicative`
||| and `Traversable` for heterogeneous container types.
||| We distinguish between two types of containers: Product
||| types hold all their values at once, while sum types
||| represent a choice: A generalization of `Either`.
|||
||| The core data types in this library are indexed over a
||| container (typically a List or List of Lists) of values
||| of type `k` plus a type-level function `f` of type `k -> Type`.
||| The values of the container index together with `f` determine
||| the types of values at each position in the
||| heterogeneous product or sum, while the shape of container
||| indices mirror the shape of the corresponding product types.
|||
||| The interfaces in this module allow us to create
||| hetereogeneous containers from sufficiently general functions
||| (`HPure`), use unary functions to change the context of
||| values in a heterogeneous container (`HFunctor`),
||| collapse heterogeneous containers into a single value (`HFoldable`)
||| and run an effectful computation over all values in
||| a heterogeneous container (`HSequence`).
|||
||| In addition, `HFunctor` can be generalized to arbitrary
||| n-ary functions (`HAp`). However, this case is special in that only
||| the last argument of such a function can be a sum type
||| while all other arguments have to be product types.
||| This makes sense, since when combining values of two sum types,
||| we typically cannot guarantee that the values point at
||| same choice and are therefore compatible.
|||
||| Implementation notes:
|||
||| For many of the functions in this module, there is a constrained
||| version taking an implicit heterogeneous product holding
||| the desired implementations. Since Idris2 uses the same
||| mechanism for resolving interface constraints and auto implicits,
||| we do not need an additional structure or interface
||| for these constraints.
||| The disadvantage of this is, that we more often have to explicitly
||| pattern match on these constraint products in order for Idris2
||| to know where to look for implementations.
module Data.SOP.Interfaces

import Data.SOP.Utils

%default total

||| A heterogeneous container indexed over a container type `l`
||| holding values of type `k`.
%inline
public export
HCont : (k : Type) -> (l : Type) -> Type
HCont k l = (k -> Type) -> l -> Type

--------------------------------------------------------------------------------
--          HPure
--------------------------------------------------------------------------------

||| This interface allows a heterogenous product to be filled
||| with values, given a function which produce values of
||| every possible type required.
|||
||| @ k kind of Types in a heterogeneous container's  type level code
|||
||| @ l kind of container used to describe a heterogeneous containr's type
|||     level code
|||
||| @ p the heterogeneous sum or product
public export
interface HPure k l (0 p : HCont k l) | p where

  ||| Creates a heterogeneous product by using the given functio
  ||| to produce values.
  |||
  ||| ```idris example
  ||| Person : (f : Type -> Type) -> Type
  ||| Person f = NP f [String,Int]
  |||
  ||| emptyPerson : Person Maybe
  ||| emptyPerson = hpure Nothing
  ||| ```
  hpure :  {0 f : k -> Type} -> {ks : l}
        -> (forall a . f a) -> p f ks

||| Alias for `hpure empty`.
|||
||| ```idris example
||| Person : (f : Type -> Type) -> Type
||| Person f = NP f [String,Int]
|||
||| emptyPerson : Person Maybe
||| emptyPerson = empty
||| ```
public export
hempty : {ks : _} -> Alternative f => HPure Type l p => p f ks
hempty = hpure empty

||| Fills a heterogeneous structure with a constant value
||| in the (K a) functor.
|||
||| ```idris example
||| Person : (f : Type -> Type) -> Type
||| Person f = NP f [String,Int]
|||
||| fooPerson : Person (K String)
||| fooPerson = hconst "foo"
||| ```
public export
hconst : {ks : _} -> HPure k l p => (v : a) -> p (K a) ks
hconst v = hpure v

--------------------------------------------------------------------------------
--          HFunctor
--------------------------------------------------------------------------------

||| A higher kinded functor allowing us to change the
||| wrapper type or context of an n-ary sum or product.
|||
||| @ k kind of Types in a heterogeneous container's  type level code
|||
||| @ l kind of container used to describe a heterogeneous containr's type
|||     level code
|||
||| @ p the actual heterogeneous container
public export
interface HFunctor k l (0 p : HCont k l) | p where

  ||| Maps the given function over all values in a
  ||| heterogeneous container, thus changing the context
  ||| of all of its values.
  |||
  ||| @ fun maps values in a heterogeneous container to a new context
  |||
  ||| @ p   the heterogeneous container, over which `fun` is mapped.
  |||
  ||| ```idris example
  ||| Person : (f : Type -> Type) -> Type
  ||| Person f = NP f [String,Int]
  |||
  ||| toPersonMaybe : Person I -> Person Maybe
  ||| toPersonMaybe = hmap Just
  ||| ```
  hmap :  {0 f,g : k -> Type}
       -> {0 ks : l}
       -> (fun : forall a . f a -> g a)
       -> p f ks
       -> p g ks

||| Alias for `hmap`
public export %inline
hliftA : HFunctor k l p => (forall a . f a -> g a) -> p f ks -> p g ks
hliftA = hmap

||| Like `hpure` but using a constrained function for
||| generating values. Since Idris is able to provide
||| the required constraints
||| already wrapped in a container of the correct
||| shape, this is actually a derivative of `HFunctor` and not
||| `HPure`. This has interesting consequences for sum
||| types, for which this function is available as well.
||| Since Idris has to choose a value of the sum
||| itself, it will use the first possibility it
||| can fill with the requested constraints.
|||
||| In the first example below, Idris generates the value
||| `MkSOP (Z ["","",[]])`. However, if the first choice does
||| not have a Monoid instance, Idris faithfully chooses the
||| next working possibility. In the second example,
||| the result is `MkSOP (S (Z [[],[]]))`:
|||
||| ```idris example
||| neutralFoo : SOP I [[String,String,List Int],[Int]]
||| neutralFoo = hcpure Monoid neutral
|||
||| neutralBar : SOP I [[String,Int,List Int],[List String, List Int]]
||| neutralBar = hcpure Monoid neutral
||| ```
|||
||| @ c   erased function argument to specify the constraint
|||       to use
|||
||| @ fun generates values depending on the availability of
|||       a constraint
public export
hcpure :  HFunctor k l p
       => (0 c : k -> Type)
       -> (cs : p c ks)
       => (fund : forall a . c a => f a)
       -> p f ks
hcpure _ {cs} fun = hmap (\_ => fun) cs

--------------------------------------------------------------------------------
--          HAp
--------------------------------------------------------------------------------

||| Like `Applicative`, this interface allows to
||| map arbitrary n-ary Rank-2 functions over
||| heterogeneous data structures of the same shape.
||| However, in order to support products as well as sum types
||| all arguments except the last one have to be products
||| indexed over the same container as the last argument.
|||
||| @ k kind of Types in a heterogeneous container's  type level code
|||
||| @ l kind of container used to describe a heterogeneous containr's type
|||     level code
|||
||| @ q heterogeneous product related to `p`. For product types,
|||     this is the same as `p`, for sum types it is the corresponding
|||     product type.
|||
||| @ p the actual heterogeneous container (sum or product)
public export
interface HFunctor k l q => HFunctor k l p => HAp k l q p | p where

  ||| Higher kinded equivalent to `(<*>)`.
  |||
  ||| Applies wrapped functions in the product
  ||| container to the corresponding values in the
  ||| second container.
  |||
  ||| @ q product holding unary Rank-2 functions.
  |||
  ||| @ p sum or product to whose values the functions in `q` should
  |||     be applied
  |||
  ||| ```idris example
  ||| hapTest : SOP Maybe [[String,Int]] -> SOP I [[String,Int]]
  ||| hapTest = hap (MkPOP $ [[fromMaybe "foo", const 12]])
  ||| ```
  hap :  {0 f,g : k -> Type}
      -> {0 ks : l}
      -> q (\a => f a -> g a) ks
      -> p f ks
      -> p g ks

||| Higher kinded version of `liftA2`.
||| This is a generalization of `hliftA` to binary
||| functions.
public export
hliftA2 :  HAp k l q p
        => (forall a . f a -> g a -> h a)
        -> q f ks
        -> p g ks
        -> p h ks
hliftA2 fun fs gs  = hliftA fun fs `hap` gs

||| Higher kinded version of `liftA3`.
||| This is a generalization of `hliftA` to ternary
||| functions.
public export
hliftA3 :  (HAp k l q q, HAp k l q p)
        => (forall a . f a -> g a -> h a -> i a)
        -> q f ks
        -> q g ks
        -> p h ks
        -> p i ks
hliftA3 fun fs gs hs = hliftA2 fun fs gs `hap` hs

||| Higher kinded version of `liftA4`.
||| This is a generalization of `hliftA` to quartenary
||| functions.
public export
hliftA4 :  (HAp k l q q, HAp k l q p)
        => (forall a . f a -> g a -> h a -> i a -> j a)
        -> q f ks
        -> q g ks
        -> q h ks
        -> p i ks
        -> p j ks
hliftA4 fun fs gs hs is = hliftA3 fun fs gs hs `hap` is

||| Like `hmap` but uses a constrained function.
|||
||| @ c   constraint used to convert values
|||
||| @ fun constrained function for converting values to
|||       a new context
|||
||| ```idris example
||| showValues : NP I [String,Int] -> NP (K String) [String,Int]
||| showValues = hcmap Show show
||| ```
public export
hcmap :  HAp k l q p
      => (0 c : k -> Type)
      -> (cs : q c ks)
      => (fun : forall a . c a => f a -> g a)
      -> p f ks
      -> p g ks
hcmap _ {cs} fun = hliftA2 (\_ => fun) cs

||| Alias for `hcmap`
public export %inline
hcliftA :  HAp k l q p
        => (0 c : k -> Type)
        -> q c ks
        => (fun : forall a . c a => f a -> g a)
        -> p f ks
        -> p g ks
hcliftA = hcmap

||| Like `hliftA2` but with a constrained function.
public export %inline
hcliftA2 :  (HAp k l q q, HAp k l q p)
         => (0 c : k -> Type)
         -> (cs : q c ks)
         => (fun : forall a . c a => f a -> g a -> h a)
         -> q f ks
         -> p g ks
         -> p h ks
hcliftA2 _ {cs} fun = hliftA3 (\_ => fun) cs

||| Like `hliftA3` but with a constrained function.
public export %inline
hcliftA3 :  (HAp k l q q, HAp k l q p)
         => (c : k -> Type)
         -> (cs : q c ks)
         => (fun : forall a . c a => f a -> g a -> h a -> i a)
         -> q f ks
         -> q g ks
         -> p h ks
         -> p i ks
hcliftA3 _ {cs} fun = hliftA4 (\_ => fun) cs

--------------------------------------------------------------------------------
--          HFold
--------------------------------------------------------------------------------

public export
interface HFold k l (0 p : HCont k l) | p where

  ||| Strict fold over a heterogeneous sum or product
  ||| parameterized by the constant functor (and thus being actually
  ||| a homogeneous sum or product).
  hfoldl : {0 ks : l} -> (acc -> el -> acc) -> acc -> p (K el) ks -> acc

  ||| Lazy fold over a heterogeneous sum or product
  ||| parameterized by the constant functor (and thus being actually
  ||| a homogeneous sum or product).
  hfoldr :  {0 ks : l}
         -> (el -> Lazy acc -> acc) -> Lazy acc -> p (K el) ks -> acc

||| Calculates the size of a heterogeneous container
public export
hsize : (HFunctor k l p, HFold k l p) => p f ks -> Nat
hsize = hfoldl (+) Z . hmap (const 1)

||| Alias for `hfoldl (<+>) neutral`.
public export
hconcat : (Monoid m, HFold k l p) => p (K m) ks -> m
hconcat = hfoldl (<+>) neutral

||| Alias for `hconcat . hmap fun`
public export
hconcatMap :  (Monoid m, HFunctor k l p, HFold k l p)
           => (fun : forall a . f a -> m) -> p f ks -> m
hconcatMap fun = hconcat . hmap fun

||| Alias for `hconcat . hcmap c fun`
public export
hcconcatMap :  (Monoid m, HAp k l q p, HFold k l p)
            => (0 c : k -> Type)
            -> q c ks
            => (fun : forall a . c a => f a -> m)
            -> p f ks
            -> m
hcconcatMap c fun = hconcat . hcmap c fun

||| Generalization of `sequence_` to heterogeneous containers.
|||
||| Alias for `hfoldl (*>) (pure ())`.
public export
hsequence_ : (Applicative g, HFold k l p) => p (K (g ())) ks -> g ()
hsequence_ = hfoldl (*>) (pure ())

||| Generalization of `traverse_` to heterogeneous containers.
|||
||| Alias for `hsequence_ . hmap fun`.
public export
htraverse_ :  (Applicative g, HFold k l p, HFunctor k l p)
           => (forall a . f a -> g ()) -> p f ks -> g ()
htraverse_ fun = hsequence_ . hmap fun

||| Generalization of `for_` to heterogeneous containers.
public export
hfor_ :  (Applicative g, HFold k l p, HFunctor k l p)
      => p f ks -> (forall a . f a -> g ()) -> g ()
hfor_ = flip htraverse_

||| Generalization of `and` to heterogeneous containers.
public export
hand : HFold k l p => p (K Bool) ks -> Bool
hand = hfoldr (\a,b => a && b) True

||| Generalization of `toList` to heterogeneous containers.
export
htoList : (HFunctor k l p, HFold k l p) => p (K a) ks -> List a
htoList = hconcatMap pure

||| Generalization of `or` to heterogeneous containers.
export
hor : HFold k l p => p (K Bool) ks -> Bool
hor = hfoldr (\a,b => a || b) False

||| Generalization of `all` to heterogeneous containers.
export
hall :   (HFunctor k l p, HFold k l p)
      => (forall a . f a -> Bool)
      -> p f ks -> Bool
hall fun = hand . hmap fun

||| Generalization of `any` to heterogeneous containers.
export
hany :  (HFunctor k l p, HFold k l p)
     => (forall a . f a -> Bool)
     -> p f ks -> Bool
hany fun = hor . hmap fun

||| Generalization of `choice` to heterogeneous containers.
export
hchoice : HFold k l p => Alternative f =>  p (K $ f a) ks -> f a
hchoice = hfoldr (\a,b => a <|> b) empty

--------------------------------------------------------------------------------
--          HSequence
--------------------------------------------------------------------------------

||| Sequencing of applicative effects over a heterogeneous
||| container.
public export
interface HSequence k l (0 p : HCont k l) | p where

  ||| Given a heterogeneous containers holding values
  ||| wrapped in effect `g`, sequences applications of
  ||| `g` to the outside of the heterogeneous container.
  |||
  ||| ```idris example
  ||| seqMaybe : NP Maybe [Int,String] -> Maybe (NP I [Int,String])
  ||| seqMaybe = hsequence
  ||| ```
  hsequence :  {0 ks : l}
            -> {0 f : k -> Type}
            -> Applicative g
            => p (\a => g (f a)) ks
            -> g (p f ks)

||| Traverses a heterogeneous container by applying effectful
||| function `fun`.
|||
||| ```idris example
||| htraverseEx : NP (Either String) [Int,String] -> Maybe (NP I [Int,String])
||| htraverseEx = htraverse (either (const Nothing) Just)
||| ```
export
htraverse :  {0 f,f' : k -> Type}
          -> (Applicative g, HFunctor k l p, HSequence k l p)
          => (fun : forall a . f a -> g (f' a))
          -> p f ks
          -> g (p f' ks)
htraverse fun = hsequence . hmap fun

||| Flipped version of `htraverse`.
export
hfor :  {0 f,f' : k -> Type}
     -> (Applicative g, HFunctor k l p, HSequence k l p)
     => p f ks
     -> (forall a . f a -> g (f' a))
     -> g (p f' ks)
hfor = flip htraverse

||| Constrained version of `htraverse`.
|||
||| ```idris example
||| interface Read a where
|||   read : String -> Maybe a
|||
||| hctraverseEx : NP Read [Int,String] =>
|||                NP (K String) [Int,String] -> Maybe (NP I [Int,String])
||| hctraverseEx = hctraverse Read read
||| ```
export
hctraverse :  {0 f,f' : k -> Type}
           -> (Applicative g, HAp k l q p, HSequence k l p)
           => (0 c : k -> Type)
           -> (cs : q c ks)
           => (forall a . c a => f a -> g (f' a))
           -> p f ks
           -> g (p f' ks)
hctraverse c fun = hsequence . hcmap c fun

||| Flipped version of `hctraverse`.
export
hcfor :  {0 f,f' : k -> Type}
      -> (Applicative g, HAp k l q p, HSequence k l p)
      => (0 c : k -> Type)
      -> (cs : q c ks)
      => p f ks
      -> (forall a . c a => f a -> g (f' a))
      -> g (p f' ks)
hcfor c = flip (hctraverse c)

--------------------------------------------------------------------------------
--          HCollapse
--------------------------------------------------------------------------------

||| Collapsing a heterogeneous container to a homogeneous one
||| of the same shape.
public export
interface HCollapse k l (0 p : HCont k l) (0 collapseTo : Type -> Type) | p where

  ||| A heterogeneous container over constant functor `K a` is
  ||| actually a homogeneous one holding only values of type `a`.
  ||| This function extracts the wrapped values into a homogeneous
  ||| one of the same size and shape.
  hcollapse : {0 a : Type} -> {0 ks : l} -> p (K a) ks -> collapseTo a


text:
module Network.HTTP.Pool.Worker

import Network.Socket
import Network.HTTP.Error
import Network.HTTP.Scheduler
import Network.HTTP.Protocol
import Network.HTTP.Message
import Network.HTTP.Header
import Network.HTTP.URL
import Network.HTTP.Pool.Common
import Utils.String
import Network.TLS
import Network.TLS.Signature
import Crypto.Random
import Crypto.Random.C
import Utils.Handle.C
import Utils.Handle
import Utils.Bytes
import Utils.Streaming
import Utils.Num
import Data.List1
import Data.Nat
import Data.Fin
import Data.String
import System.Concurrency
import Control.Linear.LIO
import Network.HTTP.Pool.IOStuff
import Data.List
import Data.IORef
import Utils.Queue

-- needed for some reason
%hide Network.Socket.close

WriteOkOrError : Type -> Type -> Type -> Type
WriteOkOrError e t_ok t_closed = Res Bool $ \ok => if ok then Handle' t_ok t_closed else Res (HttpError e) (const t_closed)

LogicOkOrError : Type -> Type -> Type
LogicOkOrError t_ok t_closed = Res Bool $ \ok => if ok then Handle' t_ok t_closed else t_closed

worker_write : (1 _ : Handle' t_ok t_closed) -> Integer -> Stream (Of (List Bits8)) IO (Either e ()) -> L1 IO (WriteOkOrError e t_ok t_closed)
worker_write handle remaining stream = do
  Right (chunk, rest) <- liftIO1 $ next stream
  | Left (Left r) => do
    handle <- close handle
    pure1 (False # ((OtherReason r) # handle))
  | Left (Right ()) => if remaining <= 0 then pure1 (True # handle) else do
    handle <- close handle
    pure1 (False # ((ContentLengthMismatch remaining) # handle))
  let should_take = min remaining (natToInteger $ length chunk)
  let chunk = take (integerToNat should_take) chunk
  (True # handle) <- write handle chunk
  | (False # (error # handle)) => pure1 (False # ((SocketError error) # handle))
  worker_write handle (remaining - should_take) rest

worker_finish : Maybe ConnectionAction -> (1 _ : Handle' t_ok t_closed) -> L1 IO (LogicOkOrError t_ok t_closed)
worker_finish (Just KeepAlive) handle =
  pure1 (True # handle)
worker_finish _ handle = do
  handle <- close handle
  pure1 (False # handle)

worker_read_fixed_length : (1 _ : Handle' t_ok t_closed) -> Integer -> Integer -> Channel (Either (HttpError e) (Maybe (List Bits8))) ->
                           L1 IO (LogicOkOrError t_ok t_closed)
worker_read_fixed_length handle remaining chunk_size channel =
  if remaining <= 0
  then do
    liftIO1 $ channelPut channel (Right Nothing)
    pure1 (True # handle)
  else do
    let should_read = min remaining chunk_size
    (True # (content # handle)) <- read handle (integerToNat should_read)
    | (False # (error # handle)) => do
      liftIO1 $ channelPut channel (Left $ SocketError "error while reading response: \{error}")
      pure1 (False # handle)
    liftIO1 $ channelPut channel (Right $ Just content)
    worker_read_fixed_length handle (remaining - should_read) chunk_size channel

worker_read_chunked_end : (1 _ : Handle' t_ok t_closed) -> Channel (Either (HttpError e) (Maybe (List Bits8))) ->
                          L1 IO (LogicOkOrError t_ok t_closed)
worker_read_chunked_end handle channel = do
  (True # ([char] # handle)) <- read handle 1
  | (True # (char # handle)) => do
    handle' <- close handle
    liftIO1 $ channelPut channel (Left $ SocketError "read chunked body failed, somehow read returns \{show (length char)} bytes instead of 1")
    pure1 (False # handle')
  | (False # (error # handle)) => do
    liftIO1 $ channelPut channel (Left $ SocketError "read chunked body failed: \{error}")
    pure1 (False # handle)
  case cast {to=Char} char of
    '\n' =>
      pure1 (True # handle)
    '\r' => do
      (True # ([10] # handle)) <- read handle 1
      | (True # ([char] # handle)) => do
        handle' <- close handle
        liftIO1 $ channelPut channel (Left $ SocketError "read chunked body failed, \\n expected after \\r, got \{show char} instead")
        pure1 (False # handle')
      | (True # (char # handle)) => do
        handle' <- close handle
        liftIO1 $ channelPut channel (Left $ SocketError "read chunked body failed, somehow read returns \{show (length char)} bytes instead of 1")
        pure1 (False # handle')
      | (False # (error # handle)) => do
        liftIO1 $ channelPut channel (Left $ SocketError "read chunked body failed: \{error}")
        pure1 (False # handle)
      pure1 (True # handle)
    chr => do
      handle <- close handle
      liftIO1 $ channelPut channel (Left $ SocketError "read chunked body tail failed: got \{show chr} instead of \\n or \\r")
      pure1 (False # handle)

worker_read_chunked : (1 _ : Handle' t_ok t_closed) -> Channel (Either (HttpError e) (Maybe (List Bits8))) ->
                      L1 IO (LogicOkOrError t_ok t_closed)
worker_read_chunked handle channel = do
  (True # (length_line # handle)) <- read_line handle
  | (False # (error # handle)) => do
    liftIO1 $ channelPut channel (Left $ SocketError "error while reading response: \{error}")
    pure1 (False # handle)
  let Just (S len) = stringToNat 16 $ toLower length_line
  | Just Z => do
    liftIO1 $ channelPut channel (Right Nothing)
    worker_read_chunked_end handle channel
  | Nothing => do
    handle <- close handle
    liftIO1 $ channelPut channel (Left $ SocketError "invalid chunked header: \{length_line}")
    pure1 (False # handle)
  (True # (content # handle)) <- read handle (S len)
  | (False # (error # handle)) => do
    liftIO1 $ channelPut channel (Left $ SocketError "error while reading chunked body: \{error}")
    pure1 (False # handle)

  liftIO1 $ channelPut channel (Right $ Just content)
  worker_read_chunked_end handle channel

worker_logic : {e : _} -> ScheduleRequest e IO -> (1 _ : Handle' t_ok t_closed) -> L1 IO (LogicOkOrError t_ok t_closed)
worker_logic request handle = do
  let throw = \err => channelPut request.response (Left err)

  let http_message = request.raw_http_message
  let Just content_length = lookup_header http_message.headers ContentLength
  | Nothing => do
    liftIO1 $ throw (MissingHeader "Content-Length")
    pure1 (True # handle)
  (True # handle) <- write handle $ utf8_unpack $ serialize_http_message http_message
  | (False # (error # handle)) => do
    liftIO1 $ throw (SocketError error)
    pure1 (False # handle)
  (True # handle) <- worker_write handle content_length $ chunksOf 0x200 request.content
  | (False # (error # handle)) => do
    liftIO1 $ throw error
    pure1 (False # handle)
  (True # (line # handle)) <- read_until_empty_line handle
  | (False # (error # handle)) => do
    liftIO1 $ throw (SocketError "error while reading response header: \{error}")
    pure1 (False # handle)

  let Right response = deserialize_http_response $ (ltrim line <+> "\n") -- for some reason the end line sometimes is not sent
  | Left err => do
    handle <- close handle
    liftIO1 $ throw (SocketError "error parsing http response headers: \{err}")
    pure1 (False # handle)
  let connection_action = lookup_header response.headers Connection

  channel <- liftIO1 (makeChannel {a=(Either (HttpError e) (Maybe (List Bits8)))})
  let schedule_response = MkScheduleResponse response channel
  liftIO1 $ channelPut request.response (Right schedule_response)

  let encodings = join $ toList (forget <$> lookup_header response.headers TransferEncoding)
  if elem Chunked encodings
    then do
      (True # handle) <- worker_read_chunked handle channel
      | (False # handle) => pure1 (False # handle)
      worker_finish connection_action handle
    else do
      let Just content_length = lookup_header response.headers ContentLength
      | Nothing => do
        handle <- close handle
        liftIO1 $ channelPut channel (Left $ MissingHeader "Content-Length")
        pure1 (False # handle)
      (True # handle) <- worker_read_fixed_length handle content_length 0x2000 channel
      | (False # handle) => pure1 (False # handle)
      worker_finish connection_action handle

worker_loop : {e : _} -> IORef Bool -> IO () -> Queue (Event e) -> (1 _ : Handle' t_ok ()) -> L IO ()
worker_loop idle_ref closer queue handle = do
  liftIO1 $ writeIORef idle_ref True
  Request request <- liftIO1 $ recv queue
  | Kill condition => do
    close handle
    liftIO1 closer
    case condition of
      Just cond => liftIO1 $ conditionBroadcast cond
      Nothing => pure ()
  liftIO1 $ writeIORef idle_ref False
  (True # handle) <- worker_logic request handle
  | (False # ()) => liftIO1 closer
  worker_loop idle_ref closer queue handle

export
worker_handle : {e : _} -> Socket -> IORef Bool -> IO () -> Queue (Event e) -> (HttpError e -> IO ()) ->
                (String -> CertificateCheck IO) -> Protocol -> String -> IO ()
worker_handle socket idle_ref closer fetcher throw cert_checker protocol hostname = LIO.run $ do
  let handle = socket_to_handle socket
  case protocol of
    HTTP =>
      worker_loop idle_ref closer fetcher handle
    HTTPS => do
      (True # handle) <-
        tls_handshake hostname
          (X25519 ::: [SECP256r1, SECP384r1])
          supported_signature_algorithms
          (tls13_supported_cipher_suites <+> tls12_supported_cipher_suites)
          handle
          (cert_checker hostname)
      | (False # (err # ())) => liftIO1 $ throw $ SocketError "error during TLS handshake: \{err}"
      worker_loop idle_ref closer fetcher handle

ext: idr


text:
module IdrisWeb.Effect.Cgi

-- Pure functions used by the CGI effects library
-- SimonJF

import System

-- Pure, non-effecting functions
abstract
getVars : List Char -> String -> List (String, String)
getVars seps query = mapMaybe readVar (split (\x => elem x seps) query)
  where
        readVar : String -> Maybe (String, String)
        readVar xs with (split (\x => x == '=') xs)
                | [k, v] = Just (trim k, trim v)
                | _      = Nothing

-- Returns either the environment variable, or the empty string if it does not exist
abstract
safeGetEnvVar : String -> IO String
safeGetEnvVar varname = do env_var <- getEnv varname
                           case env_var of
                                Just var => pure var
                                Nothing =>  pure ""

private
getContent' : Int -> IO String --Eff IO [EXTENDEDSTDIO] String
getContent' x = getC x "" where
      %assert_total
      getC : Int -> String -> IO String
      getC 0 acc = pure $ reverse acc
      getC n acc = if (n > 0)
                      then do x <- getChar
                              getC (n-1) (strCons x acc)
                      else (pure "")

-- Gets the content of the user data.
-- If CONTENT_LENGTH is not present, returns the empty string.
abstract
getContent : IO String
getContent = do
    clen_in <- getEnv "CONTENT_LENGTH" -- Check for CONTENT_LENGTH existence
    case clen_in of
         Just content_length => do let clen = prim__fromStrInt content_length
                                   getContent' clen -- Get content from content length
         Nothing             => pure ""

max_stars_repo_name: idris-hackers/IdrisWeb

max_issues_repo_name: idris-hackers/IdrisWeb

max_forks_repo_name: idris-hackers/IdrisWeb


text:
-- examples in "Type-Driven Development with Idris"
-- chapter 14, section 1, Door part

-- check that all functions are total
%default total

data DoorResult = OK | Jammed

data DoorState = DoorClosed | DoorOpen

data DoorCmd : (ty : Type) ->
               DoorState ->
               (ty -> DoorState) ->
               Type where
  Open :                   DoorCmd DoorResult DoorClosed
                                              (\res => case res of
                                                        OK => DoorOpen
                                                        Jammed => DoorClosed)
  Close :                  DoorCmd ()         DoorOpen      (const DoorClosed)
  RingBell :               DoorCmd ()         DoorClosed    (const DoorClosed)
  Display :  String ->     DoorCmd ()         state         (const state)
  Pure :     (res : ty) -> DoorCmd ty         (state res)   state
  (>>=) :                  DoorCmd a          state1        state2 ->
             ((res : a) -> DoorCmd b          (state2 res)  state3) ->
                           DoorCmd b          state1        state3

doorProg : DoorCmd () DoorClosed (const DoorClosed)
doorProg = do RingBell
              OK <- Open | Jammed => Display "Door Jammed"
              Display "Door OK"
              Close

logOpen : DoorCmd DoorResult DoorClosed
                             (\res => case res of
                                        OK => DoorOpen
                                        Jammed => DoorClosed)
logOpen = do Display "Trying to open the door"
             OK <- Open | Jammed => do Display "Jammed"
                                       Pure Jammed
             Display "Success"
             Pure OK

max_stars_repo_name: pascalpoizat/idris-book

max_issues_repo_name: pascalpoizat/idris-book

max_forks_repo_name: pascalpoizat/idris-book


text:
-- examples in "Type-Driven Development with Idris"
-- chapter 15, section 15.2

import ProcessLib

-- check that all functions are total
%default total

record WCData where
  constructor MkWCData
  wordCount : Nat
  lineCount : Nat

doCount : (content : String) -> WCData
doCount content = let lcount = length (lines content)
                      wcount = length (words content) in
                      MkWCData lcount wcount

data WC = CountFile String
        | GetData String

WCType : WC -> Type
WCType (CountFile x) = ()
WCType (GetData x) = Maybe WCData

countFile : List (String, WCData) -> String ->
            Process WCType (List (String, WCData)) Sent Sent
countFile files fname =
   do Right content <- Action (readFile fname)
            | Left err => Pure files
      let count = doCount content
      Action (putStrLn ("Counting complete for " ++ fname))
      Pure ((fname, doCount content) :: files)

total
wcService : (loaded : List (String, WCData)) -> Service WCType ()
wcService loaded
    = do msg <- Respond (\msg => case msg of
                                      CountFile fname => Pure ()
                                      GetData fname =>
                                            Pure (lookup fname loaded))
         newLoaded <- case msg of
                          Just (CountFile fname) =>
                               countFile loaded fname
                          _ => Pure loaded
         Loop (wcService newLoaded)

procMain : Client ()
procMain = do Just wc <- Spawn (wcService [])
                   | Nothing => Action (putStrLn "Spawn failed")
              Action (putStrLn "Counting test.txt")
              Request wc (CountFile "test.txt")
              Action (putStrLn "Processing")
              Just wcdata <- Request wc (GetData "test.txt")
                   | Nothing => Action (putStrLn "File error")
              Action (putStrLn ("Words: " ++ show (wordCount wcdata)))
              Action (putStrLn ("Lines: " ++ show (lineCount wcdata)))

-- run with:
-- :exec runProc procMain


text:
module HetVect

%default total
%access public export

infixr 7 ::

||| Heterogeneous list
data Vect : List Type -> Type where
  Nil  : Vect []
  (::) : t -> Vect ts -> Vect (t::ts)

-- Name hints for interactive editing
%name Vect vs, ws, xs, ys, zs

curried : (ts : List Type) -> (result : Type) -> Type
curried [] result = result
curried (t :: ts) result = t -> curried ts result

curryV : (f : Vect ts -> result) -> curried ts result
curryV f {ts = []} = f []
curryV f {ts = (t :: ts)} = \x => curryV (f . (x::))

uncurryV : (f : curried ts result) -> Vect ts -> result
uncurryV f [] = f
uncurryV f (x :: xs) = uncurryV (f x) xs

infixr 7 ++

(++) : Vect xs -> Vect ys -> Vect (xs++ys)
[] ++ ws = ws
(v::vs) ++ ws = v :: vs ++ ws

using (x:a, y:a, xs:List a)
  data Elem : a -> List a -> Type where
    Here  : Elem x (x :: xs)
    There : Elem x xs -> Elem x (y :: xs)

||| Nothing can be in an empty Vect
noEmptyElem : {x : a} -> Elem x [] -> Void
noEmptyElem Here impossible

data Subset : List a -> List a -> Type where
  EmptySet : Subset [] ys
  WithElem : (later : Subset xs ys) -> (elem : Elem x ys) -> Subset (x::xs) ys

split : {xs, ys : List Type} -> Vect (xs++ys) -> (Vect xs, Vect ys)
split {xs = []} vs = ([], vs)
split {xs = (x :: xs)} (y :: ys)
  = let (lhs,rhs) = split ys
    in  (y :: lhs, rhs)

uncurryLong
  :  {xs, ys : List Type}
  -> (Vect xs -> Vect ys -> a)
  -> Vect (xs++ys)
  -> a
uncurryLong f = uncurry f . split

lengthen
  :  {xs, ys : List Type}
  -> (Vect ys -> a)
  -> Vect (xs++ys)
  -> a
lengthen {xs=_::xs} f (_::vs) = lengthen {xs} f vs
lengthen {xs=[]} f vs = f vs

remove : (x : a) -> (xs : List a) -> (prf : Elem x xs) -> List a
remove x (x :: ys) Here = ys
remove x (y :: ys) (There z) = y :: remove x ys z

addBack : {xs : List Type} -> {x : Type} -> {auto prf : Elem x xs } -> (val : x) -> (vec : Vect (remove x xs prf)) -> Vect xs
addBack {prf = Here} val vec = val :: vec
addBack {prf = (There x)} val (v::vs) = v :: addBack val vs

max_stars_repo_name: oisdk/belief-propagation-idris

max_issues_repo_name: oisdk/belief-propagation-idris

max_forks_repo_name: oisdk/belief-propagation-idris


text:
module Proofs.TranslationInvarianceTheory

import Common.Util
import Specifications.DiscreteOrderedGroup
import Proofs.GroupCancelationLemmas
import Proofs.GroupTheory
import Proofs.TranslationInvarianceTheory
import Proofs.DiscreteOrderTheory
import Symmetry.Opposite

%default total
%access export

infixl 8 #

rewriteBetween : a = c -> b = d -> Between leq (a,b) x -> Between leq (c,d) x
rewriteBetween p q given = rewrite sym p in rewrite sym q in given

weakenR : PartialOrderSpec rel ->
  rel b c -> Between rel (a,b) x -> Between rel (a,c) x
weakenR spec bc (MkBetween ax xb) =
  MkBetween ax (transitive spec _ _ _ xb bc)

invertBetween : PartiallyOrderedGroupSpec _ _ inv rel ->
  Between rel (a,b) x -> Between rel (inv b, inv a) (inv x)
invertBetween spec (MkBetween ax xb) =
  MkBetween (inverseReversesOrder spec xb)
            (inverseReversesOrder spec ax)

invertSymRange : PartiallyOrderedGroupSpec _ _ inv rel ->
  InSymRange rel inv b x -> InSymRange rel inv b (inv x)
invertSymRange {b} spec given = rewriteBetween Refl o2 o1 where
  o1 : Between rel (inv b, inv (inv b)) (inv x)
  o1 = invertBetween spec given
  o2 : inv (inv b) = b
  o2 = groupInverseInvolution (group spec) b

translateIntervalR : {(#) : Binop s} ->
  PartiallyOrderedMagmaSpec (#) leq -> (c : s) ->
    Between leq (a,b) x -> Between leq (a # c, b # c) (x # c)
translateIntervalR spec c (MkBetween ax xb) = MkBetween
  (translationInvariantR spec _ _ _ ax)
  (translationInvariantR spec _ _ _ xb)

translateIntervalL : {(#) : Binop s} ->
  PartiallyOrderedMagmaSpec (#) leq -> (c : s) ->
    Between leq (a,b) x -> Between leq (c # a, c # b) (c # x)
translateIntervalL spec = translateIntervalR (opposite spec)

composeIntervals : {(#) : Binop s} ->
  PartiallyOrderedMagmaSpec (#) leq ->
    Between leq (a,b) x ->
    Between leq (c,d) y ->
    Between leq (a # c, b # d) (x # y)
composeIntervals spec (MkBetween ax xb) (MkBetween cy yd) = MkBetween
  (composeOrder spec _ _ _ _ ax cy)
  (composeOrder spec _ _ _ _ xb yd)

addInSymRange : {(+) : Binop s} -> PartiallyOrderedGroupSpec (+) _ neg leq ->
  InSymRange leq neg a x ->
  InSymRange leq neg a y ->
  InSymRange leq neg (a + a) (x + y)
addInSymRange {a} spec p q =
  rewrite groupInverseAnti (group spec) a a in
  composeIntervals (invariantOrder spec) p q

public export
decideBetween : Decidable [s,s] leq => (a,b,x : s) -> Dec (Between leq (a,b) x)
decideBetween a b x =
  decideBoth MkBetween betweenL betweenR
    (decision {rel = leq} a x)
    (decision {rel = leq} x b)

public export
decidePivot : Decidable [s,s] leq =>
  DiscreteOrderedGroupSpec add zero neg leq unit ->
    (p,x : s) ->
    Between leq (a,b) x ->
    EitherErased (Between leq (a,p) x)
                 (Between leq (add unit p, b) x)
decidePivot {s} spec p x (MkBetween ax xb) =
  case separate spec x p of
    Left xp => Left (MkBetween ax xp)
    Right px => Right (MkBetween px xb)

public export
decidePivotBis : Decidable [s,s] leq =>
  DiscreteOrderedGroupSpec add zero neg leq unit ->
    (p,x : s) ->
    Between leq (a,b) x ->
    EitherErased (Between leq (a, add (neg unit) p) x)
                 (Between leq (p, b) x)
decidePivotBis {s} spec p x (MkBetween ax xb) =
  case separateBis spec x p of
    Left xp => Left (MkBetween ax xp)
    Right px => Right (MkBetween px xb)

public export
decidePartition3 : Decidable [s,s] leq =>
  DiscreteOrderedGroupSpec add zero neg leq unit ->
    (p,q,x : s) ->
    Between leq (a,b) x ->
    Either3Erased (Between leq (a,p) x)
                  (Between leq (add unit p, add (neg unit) q) x)
                  (Between leq (q,b) x)
decidePartition3 spec p q x axb =
  case decidePivot spec p x axb of
    Left l => Left l
    Right pxb =>
      case decidePivotBis spec q x pxb of
        Left m => Middle m
        Right r => Right r

max_stars_repo_name: jeroennoels/verified-algebra

max_issues_repo_name: jeroennoels/verified-algebra

max_forks_repo_name: jeroennoels/verified-algebra


text:
module Algebra.Solver.Prod

import public Data.List.Elem

%default total

||| A product of variables each represented by the exponent,
||| to which it is raised.
|||
||| When normalizing arithmetic expressions, they often
||| get converted to (sums of) products of variables
||| (listed in index `as`), each raised to a certain
||| exponent. This is the case for commutative monoids
||| (a single product) as well as commutative (semi)rings
||| (a sum of products).
public export
data Prod : (a : Type) -> (as : List a) -> Type where
  Nil  : Prod a []
  (::) : (exp : Nat) -> Prod a xs -> Prod a (x :: xs)

||| Multiplying two products means adding all
||| expontents pairwise.
public export
mult : Prod a as -> Prod a as -> Prod a as
mult []        []        = []
mult (x :: xs) (y :: ys) = (x + y) :: mult xs ys

||| We sort products by lexicographically comparing
||| the exponents.
public export
compProd : Prod a as -> Prod a as -> Ordering
compProd []        []        = EQ
compProd (x :: xs) (y :: ys) = case compare x y of
  LT => LT
  GT => GT
  EQ => compProd xs ys

||| The neutral product where all exponents are zero.
public export
one : {as : List a} -> Prod a as
one {as = []}      = []
one {as = x :: xs} = 0 :: one

||| Convert a single variable to a product of variables.
public export
fromVar : {as : List a} -> Elem x as -> Prod a as
fromVar {as = x :: xs} Here      = 1 :: one
fromVar {as = x :: xs} (There y) = 0 :: fromVar y
fromVar {as = []} Here impossible
fromVar {as = []} (There y) impossible

--------------------------------------------------------------------------------
--          Proofs
--------------------------------------------------------------------------------

Uninhabited (LT = EQ) where
  uninhabited _ impossible

Uninhabited (GT = EQ) where
  uninhabited _ impossible

export
0 pcompNat : (x,y : Nat) -> (compare x y === EQ) -> x === y
pcompNat 0 0         prf = Refl
pcompNat (S k) (S j) prf = cong S $ pcompNat k j prf
pcompNat 0 (S k) Refl impossible
pcompNat (S k) 0 Refl impossible

export
0 pcompProd :  (x,y : Prod a as)
            -> (compProd x y === EQ)
            -> x === y
pcompProd []        []        prf = Refl
pcompProd (x :: xs) (y :: ys) prf with (compare x y) proof eq
  _ | EQ = cong2 (::) (pcompNat x y eq) (pcompProd xs ys prf)
  _ | LT = absurd prf
  _ | GT = absurd prf
pcompProd []        (_ :: _)  Refl impossible
pcompProd (_ :: _)  []        Refl impossible


text:
module Main

import Effects
import Effect.Exception
import Effect.State
import Effect.StdIO

import LispVal
import Eval

repl : EnvCtx -> IO ()
repl env = do
  putStr ">>> "
  exp <- getLine
  e <- evalExpr env exp
  repl e

main : IO ()
main = repl primEnv


text:
;*
;*	CW : Character Windows
;*
;*	cwindows.inc : public include file for CW routines/structures

max_stars_repo_name: minblock/msdos

max_issues_repo_name: minblock/msdos

max_forks_repo_name: minblock/msdos


text:
||| Rational number
|||
||| Copyright 2021, HATTORI, Hiroki
||| This file is released under the MIT license, see LICENSE for more detail.
|||
module Data.Rational

import Data.Maybe
import Data.Integral.Gcd

import Generics.Derive

%default total
%language ElabReflection

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

public export
record Rational where
  constructor MkRational
  num : Integer
  den : Nat
%runElab derive "Rational" [Generic, Eq, DecEq]

export infinity : Rational
infinity = MkRational 0 0

export isInfinity : Rational -> Bool
isInfinity x = x.den == 0

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

export reduce : (num:Integer) -> (den:Nat) -> Rational
reduce x y =
  let d = gcd x $ natToInteger y
   in MkRational (x `div` d) (fromInteger $ (natToInteger y) `div` d)

infixr 9 %:

public export
(%:) : (num:Integer) -> (den:Integer) -> Rational
(%:) num den =
  if den >= 0
     then reduce num $ fromInteger den
     else reduce (negate num) (fromInteger $ negate den)

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

public export Show Rational where show x = show x.num ++ " %: " ++ show x.den

public export
Ord Rational where
  compare x y = let x' = x.num * natToInteger y.den
                    y' = y.num * natToInteger x.den
                  in compare x' y'

public export Cast Integer Rational where cast x = MkRational x 1
Cast ty Integer => Cast ty Rational where cast x = MkRational (cast x) 1

public export
Num Rational where
  x + y = reduce (x.num * natToInteger y.den + y.num * natToInteger x.den) (x.den * y.den)
  x * y = reduce (x.num * y.num) (x.den * y.den)
  fromInteger x = MkRational x 1

public export
Neg Rational where
  negate x = MkRational (negate x.num) x.den
  x - y = reduce (x.num * natToInteger y.den - x.num * natToInteger x.den) (x.den * y.den)

public export
Abs Rational where
  abs x = MkRational (abs x.num) x.den
  -- signum x = MkRational (signum x.num) 1

public export
Fractional Rational where
  x / y = (x.num * natToInteger y.den) %: (y.num * natToInteger x.den)
  recip x = (natToInteger x.den) %: (fromInteger x.num)

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

export floor : Rational -> Maybe Integer
floor x = toMaybe (x.den /= 0) $ x.num `div` (natToInteger x.den)

export ceil : Rational -> Maybe Integer
ceil x = floor $ MkRational (x.num + (natToInteger x.den) - 1) x.den

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


text:
||| Stack-safe, potentially infinite streams of effectful
||| computations.
|||
||| Streams are freer monad transformers, taking three type parameters:
|||
|||  f : The effect type, in which values are wrapped. In most cases,
|||      this is `Of a` for some value type `a`.
|||
|||  m : The effect type, in which computations are run. This is
|||      typically `IO`.
|||
|||  r : The return type of a stream if it is being run to completion.
|||      for provably infinite streams, this is set to `Void`.
|||
||| As an example, a stream reading lines from a file returning
||| the total number of lines read might be of
||| type `Stream (Of String) IO Nat`.
module Stream.Internal

import Control.WellFounded
import Data.Fuel
import Data.Nat

public export
data Stream : (f,m : Type -> Type) -> (r : Type) -> Type where
  Bind : Stream f m r -> (r -> Stream f m s) -> Stream f m s
  P    : r -> Stream f m r
  F    : f r -> Stream f m r
  M    : m r -> Stream f m r

||| Calculates the number of left-nested binds in a `Stream`.
public export
depth : Stream f m r -> Nat
depth (Bind x y) = S $ depth x
depth (P x)      = 0
depth (F x)      = 0
depth (M x)      = 0

public export
Sized (Stream f m r) where
  size = depth

||| A view on a `Stream` with left-nested binds reassociated.
public export
data View : (f,m : Type -> Type) -> (r : Type) -> Type where
  BindP : r   -> (r -> Stream f m s) -> View f m s
  BindF : f r -> (r -> Stream f m s) -> View f m s
  BindM : m r -> (r -> Stream f m s) -> View f m s
  VP    : r   -> View f m r
  VF    : f r -> View f m r
  VM    : m r -> View f m r

view_ : (s : Stream f m r) -> (0 _ : SizeAccessible s) -> View f m r
view_ (Bind x y) (Access rec) = case x of
  F v      => BindF v y
  Bind z w => view_ (Bind z $ \v => Bind (w v) y) (rec _ reflexive)
  P v      => BindP v y
  M v      => BindM v y
view_ (F v) _ = VF v
view_ (P v) _ = VP v
view_ (M v) _ = VM v

export %inline
toView : (s : Stream f m r) -> View f m r
toView s = view_ s (sizeAccessible s)

export %inline
fromView : View f m r -> Stream f m r
fromView (BindP x y) = Bind (P x) y
fromView (BindF x y) = Bind (F x) y
fromView (BindM x y) = Bind (M x) y
fromView (VF x)      = F x
fromView (VP x)      = P x
fromView (VM x)      = M x

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

export
Functor (Stream f m) where
  map f s = Bind s (P . f)

export %inline
Applicative (Stream f m) where
  pure      = P
  fn <*> fk = Bind fn (\fun => map (fun $ ) fk)

export %inline
Monad (Stream f m) where
  (>>=) = Bind

export %inline
HasIO io => HasIO (Stream f io) where
  liftIO = M . liftIO

--------------------------------------------------------------------------------
--          Lifting Values
--------------------------------------------------------------------------------

export %inline
wrap : f (Stream f m r) -> Stream f m r
wrap v = Bind (F v) id

export %inline
effect : m (Stream f m r) -> Stream f m r
effect v = Bind (M v) id

export %inline
yields : f r -> Stream f m r
yields = F

export %inline
yieldsM : m (f r) -> Stream f m r
yieldsM v = Bind (M v) F

export %inline
lift : m r -> Stream f m r
lift = M

--------------------------------------------------------------------------------
--          Running Streams
--------------------------------------------------------------------------------

public export
data Empty : Type -> Type where

export
runWith : Fuel -> Stream Empty IO r -> IO (Maybe r)
runWith fuel s = fromPrim $ go fuel (toView s)
  where go : Fuel -> View Empty IO r -> (1 w : %World) -> IORes (Maybe r)
        go Dry _                w = MkIORes Nothing w
        go (More x) (BindM y z) w =
          let MkIORes val w2 = toPrim y w
           in go x (toView $ z val) w2
        go (More x) (BindP y z) w = go x (toView $ z y) w

        go (More x) (VM r) w =
            let MkIORes val w2 = toPrim r w
             in MkIORes (Just val) w2
        go (More x) (VP r) w = MkIORes (Just r) w

export
runPure : Fuel -> Stream Empty Empty r -> Maybe r
runPure fuel s = go fuel (toView s)
  where go : Fuel -> View Empty Empty r -> Maybe r
        go (More x) (BindP y z) = go x (toView $ z y)
        go (More x) (VP r)      = Just r
        go Dry _                = Nothing

export %inline
runWith_ : Fuel -> Stream Empty IO r -> IO ()
runWith_ f = ignore . runWith f

export %inline
run : Stream Empty IO r -> IO r
run s = fromPrim $ go (toView s)
  where go : View Empty IO r -> (1 w : %World) -> IORes r
        go (BindM y z) w =
          let MkIORes val w2 = toPrim y w
           in go (toView $ z val) w2
        go (BindP y z) w = go (toView $ z y) w
        go (VM r) w = toPrim r w
        go (VP r) w = MkIORes r w

export %inline
run_ : Stream Empty IO r -> IO ()
run_ = runWith_ forever

export
concat : Stream (Stream f m) m r -> Stream f m r
concat s = case toView s of
  BindF eff y => eff      >>= \v => concat (y v)
  BindP val y => pure val >>= \v => concat (y v)
  BindM act y => lift act >>= \v => concat (y v)
  VF eff      => eff
  VP val      => pure val
  VM act      => lift act

--------------------------------------------------------------------------------
--          Mapping Values
--------------------------------------------------------------------------------

maps_ : ((0 x : _) -> f x -> g x) -> Stream f m r -> Stream g m r
maps_ fun fn = case toView fn of
  BindF eff fu => yields (fun _ eff) >>= \x => maps_ fun (fu x)
  BindP val fu => pure val >>= \x => maps_ fun (fu x)
  BindM act fu => lift act >>= \x => maps_ fun (fu x)
  VP val       => pure val
  VF eff       => yields $ fun _ eff
  VM act       => lift act

mapsM_ : ((0 x : _) -> f x -> m (g x)) -> Stream f m r -> Stream g m r
mapsM_ fun fn = case toView fn of
  BindF eff fu => lift (fun _ eff) >>= yields >>= \v => mapsM_ fun (fu v)
  BindP val fu => pure val >>= \x => mapsM_ fun (fu x)
  BindM act fu => lift act >>= \x => mapsM_ fun (fu x)
  VP val       => pure val
  VF eff       => Bind (lift $ fun _ eff) yields
  VM act       => lift act

export
handle : ((0 x : _) -> f x -> m x) -> Stream f m r -> Stream Empty m r
handle fun fn = case toView fn of
  BindF x g => lift (fun _ x) >>= \v => handle fun (g v)
  BindP x g => pure x >>= \v => handle fun (g v)
  BindM x g => lift x >>= \v => handle fun (g v)
  VF x      => lift (fun _ x)
  VP x      => pure x
  VM x      => lift x

export %inline
maps : (forall x . f x -> g x) -> Stream f m r -> Stream g m r
maps fun = maps_ (\_ => fun)

export %inline
mapsM : (forall x . f x -> m (g x)) -> Stream f m r -> Stream g m r
mapsM fun = mapsM_ (\_ => fun)

--------------------------------------------------------------------------------
--          Creating Streams
--------------------------------------------------------------------------------

export
unfold : (s -> m (Either r (f s))) -> s -> Stream f m r
unfold fun vs = lift (fun vs) >>= go
  where go : Either r (f s) -> Stream f m r
        go (Left x)  = pure x
        go (Right x) = yields x >>= unfold fun

export
repeat : f () -> Stream f m Void
repeat v = yields v >> repeat v

export
replicate : Nat -> f () -> Stream f m ()
replicate 0     _ = pure ()
replicate (S k) v = yields v >> replicate k v

--------------------------------------------------------------------------------
--          Splitting Streams
--------------------------------------------------------------------------------

export
splitsAt : Nat -> Stream f m r -> Stream f m (Stream f m r)
splitsAt 0     x = pure x
splitsAt (S k) x = case toView x of
  BindF eff z => Bind (yields eff) (\v => splitsAt k (z v))
  BindP val z => Bind (pure val)   (\v => splitsAt (S k) (z v))
  BindM act z => Bind (lift act)   (\v => splitsAt (S k) (z v))
  VF v        => pure (F v)
  VP v        => pure (P v)
  VM v        => pure (M v)

export
take : Nat -> Stream f m r -> Stream f m ()
take n = ignore . splitsAt n


text:
> module FastSimpleProb.SimpleProb

> import Data.So

> import Double.Predicates
> import NonNegDouble.NonNegDouble
> import NonNegDouble.BasicOperations
> import NonNegDouble.Properties
> import List.Operations

> %default total
> %access public export
> %auto_implicits off

> using implementation NumNonNegDouble
>   |||
>   data SimpleProb : Type -> Type where
>     MkSimpleProb : {A : Type} ->
>                    (aps : List (A, NonNegDouble)) ->
>                    Positive (toDouble (sumMapSnd aps)) ->
>                    SimpleProb A

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
module Text.Token

%default total

||| For a type `kind`, specify a way of converting the recognised
||| string into a value.
|||
||| ```idris example
||| data SimpleKind = SKString | SKInt | SKComma
|||
||| TokenKind SimpleKind where
|||   TokType SKString = String
|||   TokType SKInt = Int
|||   TokType SKComma = ()
|||
|||   tokValue SKString x = x
|||   tokValue SKInt x = cast x
|||   tokValue SKComma x = ()
||| ```
public export
interface TokenKind (k : Type) where
  ||| The type that a token of this kind converts to.
  TokType : k -> Type

  ||| Convert a recognised string into a value. The type is determined
  ||| by the kind of token.
  tokValue : (kind : k) -> String -> TokType kind

||| A token of a particular kind and the text that was recognised.
public export
record Token k where
  constructor Tok
  kind : k
  text : String

||| Get the value of a `Token k`. The resulting type depends upon
||| the kind of token.
public export
value : TokenKind k => (t : Token k) -> TokType (kind t)
value (Tok k x) = tokValue k x


text:
module CropPhoto

import Objects.Photo
import Objects.Crop
import Objects.Rect

public export
record CropPhoto where
  constructor CreateCropPhoto
  photo : Photo.Photo
  crop : Crop.Crop
  rect : Rect.Rect

max_stars_repo_name: GrandArchTemplar/IdrisVKAPI

max_issues_repo_name: GrandArchTemplar/IdrisVKAPI

max_forks_repo_name: GrandArchTemplar/IdrisVKAPI


text:
module Network.HTTP.URL

import Data.String.Parser
import Generics.Derive
import Network.HTTP.Protocol
import Data.String
import Network.HTTP.Path
import Data.So

%language ElabReflection

public export
record Hostname where
  constructor MkHostname
  domain : String
  port : Maybe Bits16

public export
record URLCredential where
  constructor MkURLCredential
  username : String
  password : Maybe String

public export
record URL where
  constructor MkURL
  protocol : String
  credential : Maybe URLCredential
  host : Hostname
  path : Path
  extensions : String

%runElab derive "URLCredential" [Generic, Meta, Eq, Show]
%runElab derive "Hostname" [Generic, Meta, Eq, Show]
%runElab derive "URL" [Generic, Meta, Show]

parse_port_number : Parser Bits16
parse_port_number = do
  n <- natural
  _ <- eos
  if n < 65536 then pure (cast n) else fail "port number bigger than 65535"

parse_host : Parser Hostname
parse_host = do
  domain <- takeWhile (/= ':')
  port <- optional (char ':' *> (parse_port_number <|> pure 0))
  pure (MkHostname domain port)

parse_credential : Parser URLCredential
parse_credential = parse_username_password <|> parse_username where
  parse_username : Parser URLCredential
  parse_username = do
    username <- takeWhile (const True)
    pure (MkURLCredential username Nothing)
  parse_username_password : Parser URLCredential
  parse_username_password = do
    username <- takeUntil ":"
    password <- takeWhile (const True)
    pure (MkURLCredential username $ Just password)

export
parse_url : Parser URL
parse_url = do
  protocol <- takeUntil "://"
  credential <- optional (takeUntil "@")
  domain <- takeUntil "/" <|> takeWhile (const True)

  credential <- case parse parse_credential <$> credential of
    Just (Right (credential, _)) => pure $ Just credential
    Just (Left err) => fail err
    Nothing => pure Nothing

  case parse parse_host domain of
    Right (domain_and_port, _) => do
      path <- takeWhile (\c => (c /= '#') && (c /= '?'))
      extensions <- takeWhile (const True)
      let path = fromString ("/" <+> path)
      pure $ MkURL protocol credential domain_and_port path extensions
    Left err => fail err

export
url_from_string : String -> Either String URL
url_from_string = map fst . parse parse_url . ltrim

public export
data URLProof : AsList m -> Type where
  IsHTTPURL : URLProof ('h' :: 't' :: 't' :: 'p' :: ':' :: '/' :: '/' :: xs)
  IsHTTPSURL : URLProof ('h' :: 't' :: 't' :: 'p' :: 's' :: ':' :: '/' :: '/' :: xs)

export
url' : (str : String) -> {auto 0 ok : URLProof (asList str)} -> URL
url' string =
  case url_from_string string of
    Right x => x
    Left err => assert_total $ idris_crash err

export
add : URL -> String -> URL
add url' string =
  case url_from_string string of
    Right url'' => url''
    Left _ =>
      case break (\c => c == '#' || c == '?') string of
        (path, "") => { path := (url'.path <+> fromString path), extensions := "" } url'
        (path, extension) => { path := (url'.path <+> fromString path), extensions := extension } url'

export
parse_hostname : String -> Either String Hostname
parse_hostname = map fst . parse parse_host . trim

export
hostname_string : Hostname -> String
hostname_string host =
  host.domain <+> case host.port of Just x => ":\{show x}"; Nothing => ""

export
url_port_number : URL -> Maybe Bits16
url_port_number url = url.host.port <|> (protocol_port_number <$> protocol_from_str url.protocol)


text:
data Fin : Nat -> Type where
     FZ : Fin (S k)
     FS : Fin k -> Fin (S k)

natToFin : Nat -> (n : Nat) -> Maybe (Fin n)
natToFin Z     (S j) = Just FZ
natToFin (S k) (S j)
   = case natToFin k j of
          Just k' => Just (FS k')
          Nothing => Nothing
natToFin _ _ = Nothing

integerToFin : Integer -> (n : Nat) -> Maybe (Fin n)
integerToFin x Z = Nothing
integerToFin x n = if x >= 0 then natToFin (fromInteger x) n else Nothing

data IsJust : Maybe a -> Type where
     ItIsJust : IsJust (Just x)

-- Testing that %allow_overloads lets this one through!
partial
fromInteger : {k : Nat} ->
              (n : Integer) ->
              {auto prf : IsJust (integerToFin n k)} ->
              Fin k
fromInteger {k} n {prf}
    = case integerToFin n k of
           Just val => val

foo : Fin 5
foo = 3

bar : Fin 5
bar = 8


text:
import Data.List.Views

total
isSuffix : Eq a => List a -> List a -> Bool
isSuffix input1 input2 with (snocList input1)
  isSuffix [] input2 | Empty = False
  isSuffix (xs ++ [x]) input2 | (Snoc xsrec) with (snocList input2)
    isSuffix (xs ++ [x]) [] | (Snoc xsrec) | Empty = False
    isSuffix (xs ++ [x]) (ys ++ [y]) | (Snoc xsrec) | (Snoc ysrec)
             = if x == y then isSuffix xs ys | xsrec | ysrec
                         else False

max_issues_repo_name: gdevanla/TypeDD-Samples

max_forks_repo_name: gdevanla/TypeDD-Samples


text:
module Streaming.Bytes

import Streaming
-- import Streaming.Internal

import System.File

import Util

import Control.Monad.Trans -- intercalates needs it

{- This module provides ways of constructing streams of bytes (Bits8) and some
   basic manipulations of them.
-}

export
lines : Monad m => Stream (Of Bits8) m a -> Stream (Stream (Of Bits8) m) m a
lines = split (==10)

export
words : Monad m => Stream (Of Bits8) m a -> Stream (Stream (Of Bits8) m) m a
words = split (==32)

export
unlines : Monad m => Stream (Stream (Of Bits8) m) m a -> Stream (Of Bits8) m a
unlines str = intercalates (yield 10) str <* yield 10

export
unwords : Monad m => Stream (Stream (Of Bits8) m) m a -> Stream (Of Bits8) m a
unwords = intercalates (yield 32)

export
charCast : Bits8 -> Char
charCast r = cast (cast {to=Int} r)

-- I expect file primitives to eventually provide Bits8 rather than Char as they
-- do now, in the mean time we cast to Bits8. This is currently correct to do as
-- these are really a 'c char' which is 8 bits.
export
||| A stream of Bits8 as read from an open File from its current position, i.e. fgetc
bits8FromFile : HasIO io => File -> Stream (Of Bits8) io ()
bits8FromFile handle = Build (\r,eff,step => bef handle r eff step)
  where
    bef : File -> (() -> b) -> (eff : io b -> b) -> (step : Of Bits8 b -> b) -> b
    bef file r eff step = eff $ do
      Right c <- fGetChar file
        | Left err => do Prelude.printLn "file read error"
                         pure (r ())
      -- We check here since fEOF doesn't seem to be set by next Step.
      False <- fEOF file
        | True => pure (r ())
      pure $ step (cast (cast {to=Int} c) :> bef file r eff step)

export
||| Open a file and read it as a stream of Bits8
bits8FromFile' : HasIO io => String -> Stream (Of Bits8) io (Either FileError ())
bits8FromFile' file0 = effect $ do
    Right f <- openFile file0 Read
      | Left err => pure . pure $ Left err
    pure $ Build (\r,eff,step => bef f r eff step)
  where
    bef : File -> (Either FileError () -> b) -> (eff : io b -> b)
       -> (step : Of Bits8 b -> b) -> b
    bef file r eff step = eff $ do
      Right c <- fGetChar file
        | Left err => do Prelude.printLn "file read error"
                         closeFile file
                         pure (r (Left err))
      -- We check here since fEOF doesn't seem to be set by next Step.
      False <- fEOF file
        | True => closeFile file *> pure (r (Right ()))
      pure $ step (cast (cast {to=Int} c) :> bef file r eff step)

%foreign "C:fputc,libc"
prim_fputc : Int -> FilePtr -> PrimIO Int

fputc : HasIO io => File -> Bits8 -> io (Either FileError ())
fputc (FHandle ptr) b = do
  let c = cast b
  c' <- primIO $ prim_fputc c ptr
  pure $ if c' == c
    then Right ()
    else Left FileWriteError

export
||| A stream of Bits8 as read from a File from its current position, e.g. fgetc
byteToFile : HasIO io => File -> Stream (Of Bits8) io r -> io (Either FileError r)
byteToFile handle = streamFold (pure . Right) join (bef handle)
  where
    bef : File -> Of Bits8 (io (Either FileError r)) -> io (Either FileError r)
    bef file (b :> r) = do
      Right _ <- fputc file b
        | Left err => do Prelude.printLn "file read error"
                         pure (Left err)
      -- We check here since fEOF doesn't seem to be set by next Step.
      False <- fEOF file
        | True => pure (Left FileWriteError)
      r


text:
module AOC.Day.One

import AOC.Solution

import Data.String
import Data.List

%default total

----------------------------------------------------------------------------
-- Types -------------------------------------------------------------------
----------------------------------------------------------------------------

InputType : Type
InputType = List Integer

----------------------------------------------------------------------------
-- Helper Functions --------------------------------------------------------
----------------------------------------------------------------------------

ascending : Ord a => List a -> Nat
ascending list = foldr (\(x, y), acc => if x < y then S acc else acc) Z (zip list (drop 1 list))

window : (Num a, Ord a) => List a -> List a
window list = zipWith3 (\a, b, c => a + b + c) list (drop 1 list) (drop 2 list)

----------------------------------------------------------------------------
-- Solutions ---------------------------------------------------------------
----------------------------------------------------------------------------

part1 : InputType -> Nat
part1 = ascending

part2 : InputType -> Nat
part2 = ascending . window

----------------------------------------------------------------------------
-- Interface for input/output ----------------------------------------------
----------------------------------------------------------------------------

parser : String -> Maybe (InputType)
parser = sequence . map (parseInteger {a=Integer}) . lines

export
day1 : (inputType ** AOCSolution inputType)
day1 = solutionToDP (MkAOCSolution {
    day = 1
  , parser = parser
  , part1 = show . part1
  , part2 = show . part2
  })