text:
module Physics.Box2D

import Data.Vect
import Control.ST

import public Physics.Vector2D
import public Physics.Box2D.Definitions
import Physics.Box2D.Defaults

%link C "box2d.o"
%include C "box2d.h"
%flag C "-lBox2D -lstdc++"
-- %flag C "-g -fno-omit-frame-pointer"

export
data World = MkWorld Ptr

public export
record CollisionForBody where
  constructor MkCollisionForBody
  id : Int
  body : Body
  velocity : Vector2D
  fixtureName : String

public export
data AABB = MkAABB Vector2D Vector2D -- lower, upper

public export
data AABBQuery = MkAABBQuery String String AABB -- query_initiator, query_name

-- public export
-- data QueryResult = MkQueryResult Int Body

public export
data Event = CollisionStart CollisionForBody CollisionForBody
           | CollisionStop CollisionForBody CollisionForBody
           | QueryResult String String Int Body

export
createWorld : Vector2D -> IO Box2D.World
createWorld (x, y) = foreign FFI_C "createWorld" (Double -> Double -> IO Ptr) x y >>= pure . MkWorld

export
destroyWorld : Box2D.World -> IO ()
destroyWorld (MkWorld ptr) = foreign FFI_C "destroyWorld" (Ptr -> IO ()) ptr

maybeBoolToInt : Maybe Bool -> Int
maybeBoolToInt (Just True) = 1
maybeBoolToInt _ = 0

typeToInt : BodyType -> Int
typeToInt Static = 0
typeToInt Dynamic = 1
typeToInt Kinematic = 2

export
createBody : Box2D.World -> BodyDefinition -> IO (Int, Body)
createBody (MkWorld ptr) (MkBodyDefinition type (x, y) angle fixedRotation bullet)
  = with IO do
      body <- foreign FFI_C "createBody" (Ptr -> Int -> Double -> Double -> Double -> Int -> Int -> IO Ptr)
                      ptr (typeToInt type) x y (fromMaybe 0 angle) (maybeBoolToInt fixedRotation)
                      (maybeBoolToInt bullet)
      id <- foreign FFI_C "getId" (Ptr -> IO Int) body
      pure (id, MkBody body)

serializePoints : List Vector2D -> String
serializePoints [] = ""
serializePoints ((x, y) :: xs) = cast x ++ " " ++ cast y ++ " " ++ serializePoints xs

export
createFixture : Box2D.World -> Body -> FixtureDefinition -> IO Fixture
createFixture (MkWorld world_ptr) (MkBody body_ptr) fd
  = let (offx, offy) = fromMaybe nullVector (offset fd)
        angle' = fromMaybe 0 (angle fd)
        groupIndex' = fromMaybe 0 (groupIndex fd)
        categoryBits' = fromMaybe 0x0001 (categoryBits fd)
        maskBits' = fromMaybe 0xFFFF (maskBits fd)
        density' = fromMaybe Defaults.density (density fd)
        friction' = fromMaybe Defaults.friction (friction fd)
        restitution' = fromMaybe Defaults.restitution (restitution fd)
        name' = fromMaybe "" (name fd)
        in case shape fd of
          Circle r => foreign FFI_C "createFixtureCircle"
            (Ptr -> Ptr -> Double -> Double -> Double -> Double -> Double -> Double -> Double ->
             Int -> Int -> Int -> String -> IO Ptr)
            world_ptr body_ptr r offx offy angle' density' friction' restitution'
            groupIndex' categoryBits' maskBits' name' >>= pure . MkFixture
          Box (x, y) => foreign FFI_C "createFixtureBox"
            (Ptr -> Ptr -> Double -> Double -> Double -> Double -> Double -> Double -> Double -> Double ->
             Int -> Int -> Int -> String -> IO Ptr)
            world_ptr body_ptr x y offx offy angle' density' friction' restitution'
            groupIndex' categoryBits' maskBits' name' >>= pure . MkFixture
          Polygon xs => (foreign FFI_C "createFixturePolygon"
            (Ptr -> Ptr -> String -> Int -> Double -> Double -> Double ->
             Int -> Int -> Int -> String -> IO Ptr)
            world_ptr body_ptr (serializePoints xs) (fromNat $ length xs) density'
            friction' restitution' groupIndex' categoryBits' maskBits' name')
              >>= pure . MkFixture
          Chain xs => (foreign FFI_C "createFixtureChain"
            (Ptr -> Ptr -> String -> Int -> Double -> Double -> Double ->
             Int -> Int -> Int -> String -> IO Ptr)
            world_ptr body_ptr (serializePoints xs) (fromNat $ length xs) density'
            friction' restitution' groupIndex' categoryBits' maskBits' name')
              >>= pure . MkFixture

export
createFixture' : Box2D.World -> Body -> Shape -> (density' : Double) -> IO Fixture
createFixture' world body shape density'
  = let fixture = record {density = Just density'} (defaultFixture shape) in
        createFixture world body fixture

defaultCollide : Maybe Bool -> Int
defaultCollide Nothing = 0
defaultCollide (Just False) = 0
defaultCollide (Just True) = 1

export
createRevoluteJoint : Box2D.World -> RevoluteJointDefinition -> IO Joint
createRevoluteJoint (MkWorld world_ptr) def
  = let collideConnected = defaultCollide (collideConnected def)
        MkBody bodyA_ptr = bodyA def
        MkBody bodyB_ptr = bodyB def
        (localAnchorAx, localAnchorAy) = localAnchorA def
        (localAnchorBx, localAnchorBy) = localAnchorB def
        in with IO do
          joint_ptr <- foreign FFI_C "createRevoluteJoint"
                (Ptr -> Ptr -> Ptr -> Int -> Double -> Double -> Double -> Double -> IO Ptr)
                world_ptr bodyA_ptr bodyB_ptr collideConnected
                localAnchorAx localAnchorAy localAnchorBx localAnchorBy
          pure $ MkJoint joint_ptr

export
destroy : Box2D.World -> Body -> IO ()
destroy (MkWorld ptr_w) (MkBody ptr_b) = foreign FFI_C "destroy" (Ptr -> Ptr -> IO ()) ptr_w ptr_b

setFilter' : Ptr -> String -> Int -> Int -> Int -> IO ()
setFilter' = foreign FFI_C "setFilter" (Ptr -> String -> Int -> Int -> Int -> IO ())

export
setFilter : Body -> Maybe String -> Int -> Int -> IO ()
setFilter (MkBody ptr) Nothing filterData which
  = setFilter' ptr "" 1 filterData which
setFilter (MkBody ptr) (Just fixtureName) filterData which
  = setFilter' ptr fixtureName 0 filterData which

setFilterBit' : Ptr -> String -> Int -> Int -> Int -> IO ()
setFilterBit' = foreign FFI_C "setFilterBit" (Ptr -> String -> Int -> Int -> Int -> IO ())

export
setFilterBit : Body -> Maybe String -> Int -> Int -> IO ()
setFilterBit (MkBody ptr) Nothing filterData which
  = setFilterBit' ptr "" 1 filterData which
setFilterBit (MkBody ptr) (Just fixtureName) filterData which
  = setFilterBit' ptr fixtureName 0 filterData which

unsetFilterBit' : Ptr -> String -> Int -> Int -> Int -> IO ()
unsetFilterBit' = foreign FFI_C "unsetFilterBit" (Ptr -> String -> Int -> Int -> Int -> IO ())

export
unsetFilterBit : Body -> Maybe String -> Int -> Int -> IO ()
unsetFilterBit (MkBody ptr) Nothing filterData which
  = unsetFilterBit' ptr "" 1 filterData which
unsetFilterBit (MkBody ptr) (Just fixtureName) filterData which
  = unsetFilterBit' ptr fixtureName 0 filterData which

export
step : Box2D.World ->
       (timeStep : Double) ->
       (velocityIterations : Int) ->
       (positionIterations : Int) ->
       IO ()
step (MkWorld ptr) = foreign FFI_C "step" (Ptr -> Double -> Int -> Int -> IO ()) ptr

export
queryAABB : Box2D.World -> AABBQuery -> IO ()
queryAABB (MkWorld ptr) (MkAABBQuery id name (MkAABB (lx, ly) (ux, uy)))
  = foreign FFI_C "queryAABB"
        (Ptr -> String -> String -> Double -> Double -> Double -> Double -> IO ())
        ptr id name lx ly ux uy

export
applyImpulse : Body -> Vector2D -> IO ()
applyImpulse (MkBody ptr) (x, y)
  = foreign FFI_C "applyImpulse" (Ptr -> Double -> Double -> IO ()) ptr x y

export
applyForce : Body -> (force : Vector2D) -> (offset : Vector2D) -> IO ()
applyForce (MkBody ptr) (x, y) (offx, offy)
  = foreign FFI_C "applyForce" (Ptr -> Double -> Double -> Double -> Double -> IO ())
            ptr x y offx offy

export
getMass : Body -> IO Double
getMass (MkBody ptr) = foreign FFI_C "getMass" (Ptr -> IO Double) ptr

export
getPosition : Body -> IO Vector2D
getPosition (MkBody ptr) = with IO do
  x <- foreign FFI_C "getPosx" (Ptr -> IO Double) ptr
  y <- foreign FFI_C "getPosy" (Ptr -> IO Double) ptr
  pure (x, y)

export
getWorldCenter : Body -> IO Vector2D
getWorldCenter (MkBody ptr) = with IO do
  x <- foreign FFI_C "getWCx" (Ptr -> IO Double) ptr
  y <- foreign FFI_C "getWCy" (Ptr -> IO Double) ptr
  pure (x, y)

export
getAngle : Body -> IO Double
getAngle (MkBody ptr) = foreign FFI_C "getAngle" (Ptr -> IO Double) ptr

export
getVelocity : Body -> IO Vector2D
getVelocity (MkBody ptr) = do
  x <- foreign FFI_C "getVelx" (Ptr -> IO Double) ptr
  y <- foreign FFI_C "getVely" (Ptr -> IO Double) ptr
  pure (x, y)

export
pollCollision : Box2D.World -> IO (Maybe Event)
pollCollision (MkWorld w_ptr) = with IO do
  ptr <- foreign FFI_C "topCollision" (Ptr -> IO Ptr) w_ptr
  if ptr == null then pure Nothing else with IO do
    ptr_body_one <- foreign FFI_C "getBodyOne" (Ptr -> IO Ptr) ptr
    ptr_body_two <- foreign FFI_C "getBodyTwo" (Ptr -> IO Ptr) ptr
    id_one <- foreign FFI_C "getIdOne" (Ptr -> IO Int) ptr
    id_two <- foreign FFI_C "getIdTwo" (Ptr -> IO Int) ptr
    start <- foreign FFI_C "getStart" (Ptr -> IO Int) ptr
    velx_one <- foreign FFI_C "getColVelx" (Ptr -> Int -> IO Double) ptr 1
    velx_two <- foreign FFI_C "getColVelx" (Ptr -> Int -> IO Double) ptr 2
    vely_one <- foreign FFI_C "getColVely" (Ptr -> Int -> IO Double) ptr 1
    vely_two <- foreign FFI_C "getColVely" (Ptr -> Int -> IO Double) ptr 2
    name_one <- foreign FFI_C "getColFixtureName" (Ptr -> Int -> IO String) ptr 1
    name_two <- foreign FFI_C "getColFixtureName" (Ptr -> Int -> IO String) ptr 2
    foreign FFI_C "popCollision" (Ptr -> IO ()) w_ptr
    let for_one = MkCollisionForBody
      id_one (MkBody ptr_body_one) (velx_one, vely_one) name_one
    let for_two = MkCollisionForBody
      id_two (MkBody ptr_body_two) (velx_two, vely_two) name_two
    let event = if start == 1
      then CollisionStart for_one for_two
      else CollisionStop for_one for_two
    pure $ Just event

-- pollEvents : (box : Var) -> ST m (List Event) [box ::: SBox2D]
export
pollCollisions : Box2D.World -> IO (List Event)
pollCollisions world = with IO do
  Just event <- pollCollision world | pure []
  pure $ event :: !(pollCollisions world)

-- export
pollQuery : Box2D.World -> IO (Maybe Event)
pollQuery (MkWorld w_ptr) = with IO do
  ptr <- foreign FFI_C "topQueryResult" (Ptr -> IO Ptr) w_ptr
  if ptr == null then pure Nothing else with IO do
    query_initiator <- foreign FFI_C "getQueryId" (Ptr -> IO String) ptr
    query_name <- foreign FFI_C "getQueryName" (Ptr -> IO String) ptr
    body_id <- foreign FFI_C "getQueryBodyId" (Ptr -> IO Int) ptr
    body <- foreign FFI_C "getQueryBody" (Ptr -> IO Ptr) ptr
    foreign FFI_C "popQuery" (Ptr -> IO ()) w_ptr
    pure $ Just $ QueryResult query_initiator query_name body_id (MkBody body)

-- export
pollQueries : Box2D.World -> IO (List Event)
pollQueries world = with IO do
  Just result <- pollQuery world | pure []
  pure $ result :: !(pollQueries world)

export
pollEvents : Box2D.World -> IO (List Event)
pollEvents world = pure $ !(pollCollisions world) ++ !(pollQueries world)


text:
data Tree a = Empty
            | Node (Tree a) a (Tree a)

testTree : Tree String
testTree = Node (Node (Node Empty "Jim" Empty) "Fred"
                      (Node Empty "Sheila" Empty)) "Alice"
                (Node Empty "Bob" (Node Empty "Eve" Empty))

flatten : Tree a -> List a
flatten Empty = []
flatten (Node left val right) = flatten left ++ val :: flatten right

treeLabelWith : Stream labelType -> Tree a ->
                (Stream labelType, Tree (labelType, a))
treeLabelWith lbls Empty = (lbls, Empty)
treeLabelWith lbls (Node left val right)
     = let (this :: lblsLeft, left_labelled) = treeLabelWith lbls left
           (lblsRight, right_labelled) = treeLabelWith lblsLeft right
                in
           (lblsRight, Node left_labelled (this, val) right_labelled)

treeLabel : Tree a -> Tree (Integer, a)
treeLabel tree = snd (treeLabelWith [1..] tree)

ext: idr


text:
-- test that a sent thing arrives and is the thing that was sent

import System
import System.Concurrency.BufferedChannel

main : IO ()
main = do bcRef <- makeBufferedChannel
          let val = 3
          (MkDPair bc send) <- becomeSender bcRef
          (MkDPair bc' recv) <- becomeReceiver NonBlocking bcRef

          send Signal bc val
          sleep 1   -- give the value time to propagate
          (Just val') <- recv bc'
            | Nothing => putStrLn "ERROR: Value disappeared from channel."
          if val /= val'
             then putStrLn "ERROR: Value changed in transit."
             else putStrLn "Success!"


text:
module SemVar.Parser

import SemVar.Lexer
import SemVar.Data
import Text.Parser
import Text.Token
import Data.List

import public SemVar.Tokens

%default total

release : Grammar _ SemVarToken True String
release =
  do
    match Hyphen
    match Text

metadata : Grammar _ SemVarToken True String
metadata =
  do
    match Plus
    match Text

dotOrDefault : Grammar _ SemVarToken False Int
dotOrDefault =
  option 0 (
    do
      match Dot
      match Number
  )

version : Grammar _ SemVarToken True Version
version =
  do
    major <- match Number
    minor <- dotOrDefault
    patch <- dotOrDefault
    release <- optional release
    metadata <- optional metadata
    pure (MkVersion major minor patch release metadata)

tilde : Grammar _ SemVarToken True Requirement
tilde =
  do
    match Tilde
    v <- version
    pure $ AND (GTE v) (LT $ nextMinor v)

pin : Grammar _ SemVarToken True Requirement
pin =
  do
    match Caret
    v <- version
    pure $ case v of
      MkVersion 0 0 patch Nothing Nothing =>
        EQ v
      _ =>
        AND (GTE v) (LT $ nextMajor v)

exact : Grammar _ SemVarToken True Requirement
exact =
  do
    ignore $ optional (match CmpEQ)
    v <- version
    pure $ EQ v

gt : Grammar _ SemVarToken True Requirement
gt =
  do
    ignore $ optional (match CmpGT)
    v <- version
    pure $ GT v

lt : Grammar _ SemVarToken True Requirement
lt =
  do
    ignore $ optional (match CmpLT)
    v <- version
    pure $ LT v

gte : Grammar _ SemVarToken True Requirement
gte =
  do
    ignore $ optional (match CmpGTE)
    v <- version
    pure $ GTE v

lte : Grammar _ SemVarToken True Requirement
lte =
  do
    ignore $ optional (match CmpLTE)
    v <- version
    pure $ LTE v

range : Grammar _ SemVarToken True Requirement
range =
  do
    v0 <- version
    ignore $ optional (match Whitespace)
    match Hyphen
    ignore $ optional (match Whitespace)
    v1 <- version
    pure $ AND (GTE v0) (LTE v1)

simpleRequirement : Grammar _ SemVarToken True Requirement
simpleRequirement =
  (
        range
    <|> tilde
    <|> pin
    <|> exact
    <|> gte
    <|> gt
    <|> lte
    <|> lt
  )

conj : Grammar _ SemVarToken True Requirement
conj =
  do
    v0 <- simpleRequirement
    match Whitespace
    v1 <- simpleRequirement
    pure $ AND v0 v1

disjuction : Grammar _ SemVarToken True Requirement
disjuction =
  do
    v0 <- simpleRequirement
    ignore $ optional (match Whitespace)
    ignore $ match Pipe
    ignore $ optional (match Whitespace)
    v1 <- simpleRequirement
    pure $ OR v0 v1

requirement : Grammar _ SemVarToken True Requirement
requirement =
  (
        conj
    <|> disjuction
    <|> simpleRequirement
  )

export
parseVersionToks : List (WithBounds SemVarToken) -> Maybe Version
parseVersionToks toks = case parse version toks of
                      Right (j, []) => Just j
                      _ => Nothing

export
parseRequirementToks : List (WithBounds SemVarToken) -> Maybe Requirement
parseRequirementToks toks = case parse requirement toks of
                      Right (j, []) => Just j
                      _ => Nothing

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
import Data.Vect

{-
Matrix type using type synonyms
 -}

Matrix : Nat -> Nat -> Type
Matrix i j = Vect i (Vect j Double)

testMatrix : Matrix 2 3
testMatrix = [[0, 0, 0], [0, 0, 0]]


text:
module CosetRep

import Group
import Cosets
%access public export

--Generates (equivalent) representatives of the image in g of a
--coset (element of the transversal type) in the transversal type
repgen: (trav: Type) -> Transversal trav -> (y: trav) -> trav
repgen trav (MkTransversal h (MkGroup h (+) pfh) g (MkGroup g (*) pfg) sbgrp trav pftrav) y = (DPair.fst (DPair.snd  ((Basics.snd (DPair.snd pftrav)) (f y)) )) where
    f: trav -> g
    f = DPair.fst pftrav
    incl: h->g
    incl = DPair.fst sbgrp

--Proof of uniqueness of the coset representative in trav, in the following sense
--Proof that the operation that generates coset representative in trav for an
--element of g (from CosetAll) inverts the function generating a coset representative by going from trav to g (from IsTraversal)
CorepFinv: (trav: Type) -> (pft: Transversal trav) -> (y: trav) -> (repgen trav pft y = y)
CorepFinv  trav (MkTransversal h (MkGroup h (+) pfh) g (MkGroup g (*) pfg) sbgrp trav pftrav)
  y = (sym (
  (Basics.fst (DPair.snd pftrav)) y rep (p ** (sym (DPair.snd (DPair.snd  ((Basics.snd (DPair.snd pftrav)) (f y)) ))))
  )) where
  rep: trav
  rep = (DPair.fst (DPair.snd  ((Basics.snd (DPair.snd pftrav)) ((DPair.fst pftrav) y) ) ))
  f: trav -> g
  f = (DPair.fst pftrav)
  p: h
  p = (DPair.fst  ((Basics.snd (DPair.snd  pftrav)) (f y)))


text:
-- ------------------------------------------------------------- [ Process.idr ]
--
-- Implementation of the Daytime protocol
--
-- --------------------------------------------------------------------- [ EOH ]
module Daytime

import Effects
import Effect.StdIO
import Effect.Default
import Effect.Msg

import System.Protocol

import RFC.Daytime
import RFC.Utils

import Utils

-- ---------------------------------------------------------- [ Server Process ]

||| Implementation of the Daytime Protocol from the Server's perspective.
|||
||| @proc The PID of the client process.
covering
daytimeServer : (proc : PID)
              -> Process (daytime) 'Server ['Client := proc] [STDIO] ()
daytimeServer proc = do
    msg <- recvFrom 'Client
    sendTo 'Client (getDayTime)
    return ()

-- ---------------------------------------------------------- [ Client Process ]

||| Implementation of the Daytime Protocol from the Client's perspective.
|||
||| @proc The PID of the server process.
covering
daytimeClient : (proc : PID)
              -> Process (daytime) 'Client ['Server := proc] [STDIO] ()
daytimeClient proc = do
    sendTo 'Server Nothing
    dt <- recvFrom 'Server
    case dt of
      Left err => do
        putStrLn $ "Time not returned: " ++ err
        return ()
      Right res => do
        putStrLn $ "The time is: " ++ show res
        return ()

-- ------------------------------------------------------ [ Sample Innvocation ]

||| Sample Innvocation of the Echo protocols between the client and
||| server functions.
covering
doDaytimeProcess : IO ()
doDaytimeProcess = runConc [()] doDaytime'
  where
    doDaytime' : Process (daytime) 'Client [] [STDIO] ()
    doDaytime' = do
       server <- spawn (daytimeServer) [()]
       setChan 'Server server
       daytimeClient server
       dropChan 'Server

-- -------------------------------------------------------------------- [ Main ]
namespace Main
  main : IO ()
  main = doDaytimeProcess

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

max_stars_repo_name: jfdm/idris-protocol-examples

max_issues_repo_name: jfdm/idris-protocol-examples

max_forks_repo_name: jfdm/idris-protocol-examples


text:
module Cordial.Model.Common.Necessary

import Cordial.Model.Common.Essential

%access public export
%default total

data OptTy = REQ | OPT

data OptionalTy = CompletelyOptional
                | ProducerOptional
                | ConsumerOptional
                | IsRequired

%hint
calcOptTy : (endpoint : Endpoint)
         -> (optTy    : OptionalTy)
         -> OptTy
calcOptTy PRODUCER CompletelyOptional = OPT
calcOptTy PRODUCER ProducerOptional = OPT
calcOptTy PRODUCER ConsumerOptional = REQ
calcOptTy PRODUCER IsRequired = REQ
calcOptTy CONSUMER CompletelyOptional = OPT
calcOptTy CONSUMER ProducerOptional = REQ
calcOptTy CONSUMER ConsumerOptional = OPT
calcOptTy CONSUMER IsRequired = REQ

data OptionalKind : (endpoint : Endpoint)
                 -> (opt : OptionalTy)
                 -> (ty  : OptTy)
                 -> Type
  where
    IsOptPA : OptionalKind PRODUCER CompletelyOptional OPT
    IsOptPP : OptionalKind PRODUCER ProducerOptional   OPT
    IsReqPC : OptionalKind PRODUCER ConsumerOptional   REQ
    IsReqPR : OptionalKind PRODUCER IsRequired         REQ

    IsOptCA : OptionalKind CONSUMER CompletelyOptional OPT
    IsReqCP : OptionalKind CONSUMER ProducerOptional   REQ
    IsOptCC : OptionalKind CONSUMER ConsumerOptional   OPT
    IsReqCR : OptionalKind CONSUMER IsRequired         REQ

||| Is the port required or optional
data Necessary : (ty : OptTy)
              -> (endpoint : Endpoint)
              -> (optTy : OptionalTy)
              -> (prf : OptionalKind endpoint optTy ty)
              -> Type
  where
   Required : Necessary REQ endpoint opt kind
   Optional : Necessary OPT endpoint opt kind

%hint
calcOptKind : (endpoint : Endpoint)
           -> (opt      : OptionalTy)
           -> OptionalKind endpoint opt (calcOptTy endpoint opt)
calcOptKind endpoint opt with (endpoint)
  calcOptKind endpoint opt | PRODUCER with (opt)
    calcOptKind endpoint opt | PRODUCER | CompletelyOptional = IsOptPA
    calcOptKind endpoint opt | PRODUCER | ProducerOptional = IsOptPP
    calcOptKind endpoint opt | PRODUCER | ConsumerOptional = IsReqPC
    calcOptKind endpoint opt | PRODUCER | IsRequired = IsReqPR

  calcOptKind endpoint opt | CONSUMER with (opt)
    calcOptKind endpoint opt | CONSUMER | CompletelyOptional = IsOptCA
    calcOptKind endpoint opt | CONSUMER | ProducerOptional = IsReqCP
    calcOptKind endpoint opt | CONSUMER | ConsumerOptional = IsOptCC
    calcOptKind endpoint opt | CONSUMER | IsRequired = IsReqCR

%hint
calcNecessary : (endpoint : Endpoint)
             -> (opt      : OptionalTy)
             -> Necessary (calcOptTy endpoint opt) endpoint opt (calcOptKind endpoint opt)
calcNecessary endpoint opt with (calcOptKind endpoint opt)
  calcNecessary PRODUCER CompletelyOptional | IsOptPA = Optional
  calcNecessary PRODUCER ProducerOptional | IsOptPP = Optional
  calcNecessary PRODUCER ConsumerOptional | IsReqPC = Required
  calcNecessary PRODUCER IsRequired | IsReqPR = Required
  calcNecessary CONSUMER CompletelyOptional | IsOptCA = Optional
  calcNecessary CONSUMER ProducerOptional | IsReqCP = Required
  calcNecessary CONSUMER ConsumerOptional | IsOptCC = Optional
  calcNecessary CONSUMER IsRequired | IsReqCR = Required

namespace Calculated
     Necessary : (endpoint : Endpoint)
              -> (opt : OptionalTy)
              -> Type
     Necessary endpoint flow = Necessary.Necessary (calcOptTy endpoint flow) endpoint flow (calcOptKind endpoint flow)
-- --------------------------------------------------------------------- [ EOF ]

max_stars_repo_name: border-patrol/cordial

max_issues_repo_name: border-patrol/cordial

max_forks_repo_name: border-patrol/cordial


text:
module Main

import Resimp

data Purpose = Reading | Writing

pstring : Purpose -> String
pstring Reading = "r"
pstring Writing = "w"

data FILE : Purpose -> Type where
    OpenH : File -> FILE p

syntax "ifM" [test] "then" [t] "else" [e]
    = test >>= (\b => if b then t else e)

open : String -> (p:Purpose) -> Creator (Either () (FILE p))
open fn p = ioc (do Right h <- fopen fn (pstring p)
                       | Left err => pure (Left ())
                    pure (Right (OpenH h)))

close : FILE p -> Updater ()
close (OpenH h) = iou (closeFile h)

readLine : FILE Reading -> Reader String
readLine (OpenH h) = ior (do Right str <- fGetLine h
                                   | pure ""
                             pure str)

eof : FILE Reading -> Reader Bool
eof (OpenH h) = ior (fEOF h)

syntax rclose [h]    = Update close h
syntax rreadLine [h] = Use readLine h
syntax reof [h]      = Use eof h

syntax rputStrLn [s] = Lift (putStrLn s)
syntax rputStr [s] = Lift (putStr s)

syntax "if" "opened" [f] "then" [e] "else" [t] = Check f t e

--------

readH : String -> RES ()
readH fn = res (do let x = open fn Reading
                   if opened x then
                       do str <- rreadLine x
                          rputStr str
                          rclose x
                       else rputStrLn "Error")

main : IO ()
main = run (readH "test014file")

max_stars_repo_name: grin-compiler/idris-grin

max_issues_repo_name: grin-compiler/idris-grin

max_forks_repo_name: grin-compiler/idris-grin


text:
module Crypto.RSA

import Data.List
import Data.Vect
import Data.Bits
import Utils.Misc
import Utils.Bytes
import Crypto.Random
import Data.Nat
import Crypto.Hash
import Data.List1
import Data.Fin
import Data.Stream
import Data.Fin.Extra
import Crypto.Hash.OID

export
data RSAPublicKey : Type where
  MkRSAPublicKey : (n : Integer) -> (e : Integer) -> RSAPublicKey

-- TODO: check if there are more constraints needed between n and e
-- also maybe use a proof instead of masking the constructor in the future
export
mk_rsa_publickey : Integer -> Integer -> Maybe RSAPublicKey
mk_rsa_publickey n e = guard (1 == gcd' n e) $> MkRSAPublicKey n e

export
rsa_encrypt : RSAPublicKey -> Integer -> Integer
rsa_encrypt (MkRSAPublicKey n e) m = pow_mod m e n

-- RFC 8017

export
os2ip : Foldable t => t Bits8 -> Integer
os2ip = be_to_integer

export
i2osp : Nat -> Integer -> Maybe (List Bits8)
i2osp b_len x =
  let mask = (shiftL 1 (8 * b_len)) - 1
      x' = x .&. mask
  in (guard $ x == x') $> (toList $ integer_to_be b_len x)

export
rsavp1 : RSAPublicKey -> Integer -> Maybe Integer
rsavp1 pk@(MkRSAPublicKey n e) s = guard (s > 0 && s < (n - 1)) $> rsa_encrypt pk s

record PSSEncodedMessage n where
  hash_digest : Vect n Bits8
  db : List Bits8

public export
MaskGenerationFunction : Type
MaskGenerationFunction = (n : Nat) -> List Bits8 -> Vect n Bits8

export
mgf1 : {algo : _} -> (h : Hash algo) => MaskGenerationFunction
mgf1 n seed = take n $ stream_concat $ map (\x => hash algo (seed <+> (toList $ integer_to_be 4 $ cast x))) nats

export
modulus_bits : RSAPublicKey -> Nat
modulus_bits (MkRSAPublicKey n _) = if n > 0 then go Z n else 0
  where
    go : Nat -> Integer -> Nat
    go n x = if x == 0 then n else go (S n) (shiftR x 1)

export
emsa_pss_verify : {algo : _} -> (h : Hash algo) => MaskGenerationFunction -> Nat -> List Bits8 -> List1 Bits8 -> Nat -> Maybe ()
emsa_pss_verify mgf sLen message em emBits = do
  let mHash = hash algo message
  let emLen = divCeilNZ emBits 8 SIsNonZero
  let (em, 0xbc) = uncons1 em
  | _ => Nothing -- Invalid padding
  (maskedDB, digest) <- splitLastAt1 (digest_nbyte {algo}) em
  -- check padding
  guard $ check_padding (modFinNZ emBits 8 SIsNonZero) (head maskedDB)
  let db = zipWith xor (toList maskedDB) (toList $ mgf (length maskedDB) (toList digest))
  (padding, salt) <- splitLastAt1 sLen db
  -- unset padding bits
  bits_to_be_cleared <- natToFin (minus (8 * emLen) emBits) _
  let mask = shiftR (the Bits8 oneBits) bits_to_be_cleared
  let (pxs, px) = uncons1 $ (mask .&. head padding) ::: (tail padding)
  -- check padding
  guard (0 == (foldr (.|.) 0 pxs))
  guard (1 == px)
  -- check salt length
  guard $ digest `s_eq` hash algo (replicate 8 0 <+> toList mHash <+> toList salt)
  where
    check_padding : Fin 8 -> Bits8 -> Bool
    check_padding FZ _ = True
    check_padding n b = 0 == shiftR b n

export
rsassa_pss_verify' : {algo : _} -> (h : Hash algo) => MaskGenerationFunction -> Nat -> RSAPublicKey -> List Bits8 -> List Bits8 -> Bool
rsassa_pss_verify' mask_gen salt_len pk message signature = isJust $ do
  let modBits = modulus_bits pk
  let s = os2ip signature
  m <- rsavp1 pk s
  let emLen = divCeilNZ (pred modBits) 8 SIsNonZero
  em <- i2osp emLen m >>= fromList
  emsa_pss_verify {algo} mask_gen salt_len message em (pred modBits)

export
rsassa_pss_verify : {algo : _} -> Hash algo => RSAPublicKey -> List Bits8 -> List Bits8 -> Bool
rsassa_pss_verify = rsassa_pss_verify' {algo} (mgf1 {algo}) (digest_nbyte {algo})

export
emsa_pkcs1_v15_encode : {algo : _} -> RegisteredHash algo => List Bits8 -> Nat -> Maybe (List Bits8)
emsa_pkcs1_v15_encode message emLen = do
  let h = hashWithHeader {algo} message
  let paddingLen = (emLen `minus` der_digest_n_byte {algo}) `minus` 3
  guard (paddingLen >= 8)
  let padding = replicate paddingLen 0xff
  pure $ [ 0x00, 0x01 ] <+> padding <+> [ 0x00 ] <+> toList h

export
rsassa_pkcs1_v15_verify : {algo : _} -> RegisteredHash algo => RSAPublicKey -> List Bits8 -> List Bits8 -> Bool
rsassa_pkcs1_v15_verify pk message signature = isJust $ do
  let k = divCeilNZ (modulus_bits pk) 8 SIsNonZero
  guard (k == length signature)

  let s = os2ip signature
  m <- rsavp1 pk s
  em <- i2osp k m

  em' <- emsa_pkcs1_v15_encode {algo} message k
  guard (em `s_eq'` em')


text:
||| Javascript utilities. If these prove to be useful in
||| applications, they should eventually go into their
||| own package.
module JS.Util

import public Control.Monad.Either
import Data.Maybe

export
doubleToBool : Double -> Bool
doubleToBool d = d /= 0.0

%foreign "javascript:lambda:v=>typeof(v)"
prim__typeOf : AnyPtr -> String

||| Inspect the type of a value at runtime by means of
||| Javascript function `typeof`.
export
typeof : a -> String
typeof v = prim__typeOf (believe_me v)

%foreign "javascript:lambda:(a,b)=>a === b?1:0"
prim__eqv : AnyPtr -> AnyPtr -> Double

||| Heterogeneous pointer equality. This calls the Javascript
||| `===` operator internally.
export
eqv : a -> b -> Bool
eqv x y = doubleToBool $ prim__eqv (believe_me x) (believe_me y)

%foreign "javascript:lambda:x=>String(x)"
prim__show : AnyPtr -> String

||| Displays a JS value by passing it to `String(...)`.
export
jsShow : a -> String
jsShow v = prim__show (believe_me v)

--------------------------------------------------------------------------------
--          IO
--------------------------------------------------------------------------------

%foreign "browser:lambda:x=>console.log(x)"
prim__consoleLog : String -> PrimIO ()

export
consoleLog : HasIO io => String -> io ()
consoleLog s = primIO $ prim__consoleLog s

public export
data JSErr : Type where
  Caught    : (msg : String) -> JSErr
  CastErr   : (inFunction : String) -> (value : a) -> JSErr
  IsNothing : (callSite : String) -> JSErr

export
dispErr : JSErr -> String
dispErr (CastErr inFunction value) = #"""
  Error when casting a Javascript value in function \#{inFunction}.
    The value was: \#{jsShow value}.
    The value's type was \#{typeof value}.
  """#

dispErr (IsNothing callSite) =
  #"Trying to extract a value from Nothing at \#{callSite}"#

dispErr (Caught msg) = msg

public export
JSIO : Type -> Type
JSIO = EitherT JSErr IO

export
runJSWith : Lazy (JSErr -> IO a) -> JSIO a -> IO a
runJSWith f (MkEitherT io) = io >>= either f pure

export
runJS : JSIO () -> IO ()
runJS = runJSWith (consoleLog . dispErr)

export
runJSWithDefault : Lazy a -> JSIO a -> IO a
runJSWithDefault a = runJSWith (\e => consoleLog (dispErr e) $> a)

export %inline
primJS : PrimIO a -> JSIO a
primJS = primIO

export
unMaybe : (callSite : String) -> JSIO (Maybe a) -> JSIO a
unMaybe callSite io = do Just a <- io
                           | Nothing => throwError $ IsNothing callSite
                         pure a

--------------------------------------------------------------------------------
--          Error handling
--------------------------------------------------------------------------------

%foreign "javascript:lambda:(u,io) => {try { return [1,io()]; } catch (e) { return [0,String(e)] }}"
prim__tryIO : forall a . IO a -> PrimIO AnyPtr

%foreign "javascript:lambda:(x,y,f,v) => {try { return [1,f(v)]; } catch (e) { return [0,String(e)] }}"
prim__try : forall a,b . (a -> b) -> a -> AnyPtr

%foreign "javascript:lambda:x => x[0]"
prim__errTag : AnyPtr -> Double

%foreign "javascript:lambda:x => x[1]"
prim__errVal : AnyPtr -> AnyPtr

toEither : AnyPtr -> Either JSErr a
toEither ptr = if 1 == prim__errTag ptr
                  then Right (believe_me (prim__errVal ptr))
                  else Left $ Caught (believe_me (prim__errVal ptr))

||| Tries to execute an IO action, wrapping any runtime exception
||| in its stringified version in a `Left . Caught`.
export
tryIO : IO a -> JSIO a
tryIO io = do ptr <- primIO $ prim__tryIO io
              if 1 == prim__errTag ptr
                 then pure (believe_me (prim__errVal ptr))
                 else throwError $ Caught (believe_me (prim__errVal ptr))

||| Error handling in pure functions. This should only be used
||| in foreign function calls that might fail but or otherwise
||| pure calculations.
export
try : (a -> b) -> a -> Either JSErr b
try f a = toEither $ prim__try f a

--------------------------------------------------------------------------------
--          Common external types
--------------------------------------------------------------------------------

||| See [spec](https://html.spec.whatwg.org/#windowproxy)
export
data WindowProxy : Type where [external]


text:
module Sixel.Symbols

import Sixel.Library

export
%foreign (sixelutils "sixel_utils_version")
version : String

export
%foreign (sixelutils "sixel_utils_abi_version")
abiVersion : String

export
interface Show t => Symbolic t s | s where
  hint     : s -> String
  binding  : s -> t
  symbol   : s -> String
  symbolBy : (t -> AnyPtr) -> s -> String

  symbolBy f symbol =
    let val = binding symbol
        ptr = f val
        in if prim__isConcreteAny ptr
              then prim__toStringAny ptr
              else hint symbol ++ " " ++ show val

--

public export
data Status = MkStatus Int

namespace Status
  %foreign (sixelutils "sixel_utils_succeeded")
  sixel_utils_succeeded : Int -> Int

  export %inline
  succeeded : Status -> Bool
  succeeded (MkStatus s) = intToBool (sixel_utils_succeeded s)

  --

  %foreign (sixelutils "sixel_utils_failed")
  sixel_utils_failed : Int -> Int

  export %inline
  failed : Status -> Bool
  failed (MkStatus s) = intToBool (sixel_utils_failed s)

  --

  %foreign (sixelutils "sixel_utils_status_symbol")
  sixel_utils_status_symbol : Int -> AnyPtr

  export
  Symbolic Int Status where
    hint _               = "Status"
    binding (MkStatus b) = b
    symbol               = symbolBy sixel_utils_status_symbol

  export
  Eq Status where
    (==) x y = binding x == binding y

  export
  Show Status where
    show = symbol

  --

  %foreign (sixelutils "sixel_utils_ok")
  sixel_utils_ok : Int

  export %inline
  Ok : Status
  Ok = MkStatus sixel_utils_ok

  --

  %foreign (sixelutils "sixel_utils_runtime_error")
  sixel_utils_runtime_error : Int

  export %inline
  RuntimeError : Status
  RuntimeError = MkStatus sixel_utils_runtime_error

  --

  %foreign (sixelutils "sixel_utils_logic_error")
  sixel_utils_logic_error : Int

  export %inline
  LogicError : Status
  LogicError = MkStatus sixel_utils_logic_error

  --

  %foreign (sixelutils "sixel_utils_feature_error")
  sixel_utils_feature_error : Int

  export %inline
  FeatureError : Status
  FeatureError = MkStatus sixel_utils_feature_error

  --

  %foreign (sixelutils "sixel_utils_libc_error")
  sixel_utils_libc_error : Int

  export %inline
  LibcError : Status
  LibcError = MkStatus sixel_utils_libc_error

  --

  %foreign (sixelutils "sixel_utils_curl_error")
  sixel_utils_curl_error : Int

  export %inline
  CurlError : Status
  CurlError = MkStatus sixel_utils_curl_error

  --

  %foreign (sixelutils "sixel_utils_jpeg_error")
  sixel_utils_jpeg_error : Int

  export %inline
  JpegError : Status
  JpegError = MkStatus sixel_utils_jpeg_error

  --

  %foreign (sixelutils "sixel_utils_png_error")
  sixel_utils_png_error : Int

  export %inline
  PngError : Status
  PngError = MkStatus sixel_utils_png_error

  --

  %foreign (sixelutils "sixel_utils_gdk_error")
  sixel_utils_gdk_error : Int

  export %inline
  GdkError : Status
  GdkError = MkStatus sixel_utils_gdk_error

  --

  %foreign (sixelutils "sixel_utils_gd_error")
  sixel_utils_gd_error : Int

  export %inline
  GdError : Status
  GdError = MkStatus sixel_utils_gd_error

  --

  %foreign (sixelutils "sixel_utils_stbi_error")
  sixel_utils_stbi_error : Int

  export %inline
  StbiError : Status
  StbiError = MkStatus sixel_utils_stbi_error

  --

  %foreign (sixelutils "sixel_utils_stbiw_error")
  sixel_utils_stbiw_error : Int

  export %inline
  StbiwError : Status
  StbiwError = MkStatus sixel_utils_stbiw_error

  --

  %foreign (sixelutils "sixel_utils_interrupted")
  sixel_utils_interrupted : Int

  export %inline
  Interrupted : Status
  Interrupted = MkStatus sixel_utils_interrupted

  --

  %foreign (sixelutils "sixel_utils_bad_allocation")
  sixel_utils_bad_allocation : Int

  export %inline
  BadAllocation : Status
  BadAllocation = MkStatus sixel_utils_bad_allocation

  --

  %foreign (sixelutils "sixel_utils_bad_argument")
  sixel_utils_bad_argument : Int

  export %inline
  BadArgument : Status
  BadArgument = MkStatus sixel_utils_bad_argument

  --

  %foreign (sixelutils "sixel_utils_bad_input")
  sixel_utils_bad_input : Int

  export %inline
  BadInput : Status
  BadInput = MkStatus sixel_utils_bad_input

  --

  %foreign (sixelutils "sixel_utils_bad_integer_overflow")
  sixel_utils_bad_integer_overflow : Int

  export %inline
  BadIntegerOverflow : Status
  BadIntegerOverflow = MkStatus sixel_utils_bad_integer_overflow

  --

  %foreign (sixelutils "sixel_utils_not_implemented")
  sixel_utils_not_implemented : Int

  export %inline
  NotImplemented : Status
  NotImplemented = MkStatus sixel_utils_not_implemented

--

public export
data MethodForLargest = MkMethodForLargest Int

namespace MethodForLargest
  %foreign (sixelutils "sixel_utils_large_symbol")
  sixel_utils_large_symbol : Int -> AnyPtr

  export
  Symbolic Int MethodForLargest where
    hint _                         = "MethodForLargest"
    binding (MkMethodForLargest b) = b
    symbol                         = symbolBy sixel_utils_large_symbol

  export
  Eq MethodForLargest where
    (==) x y = binding x == binding y

  export
  Show MethodForLargest where
    show = symbol

  --

  %foreign (sixelutils "sixel_utils_large_auto")
  sixel_utils_large_auto : Int

  export %inline
  LargeAuto : MethodForLargest
  LargeAuto = MkMethodForLargest sixel_utils_large_auto

  --

  %foreign (sixelutils "sixel_utils_large_norm")
  sixel_utils_large_norm : Int

  export %inline
  LargeNorm : MethodForLargest
  LargeNorm = MkMethodForLargest sixel_utils_large_norm

  --

  %foreign (sixelutils "sixel_utils_large_lum")
  sixel_utils_large_lum : Int

  export %inline
  LargeLum : MethodForLargest
  LargeLum = MkMethodForLargest sixel_utils_large_lum

--

public export
data MethodForRep = MkMethodForRep Int

namespace MethodForRep
  %foreign (sixelutils "sixel_utils_rep_symbol")
  sixel_utils_rep_symbol : Int -> AnyPtr

  export
  Symbolic Int MethodForRep where
    hint _                     = "MethodForRep"
    binding (MkMethodForRep b) = b
    symbol                     = symbolBy sixel_utils_rep_symbol

  export
  Eq MethodForRep where
    (==) x y = binding x == binding y

  export
  Show MethodForRep where
    show = symbol

  --

  %foreign (sixelutils "sixel_utils_rep_auto")
  sixel_utils_rep_auto : Int

  export %inline
  RepAuto : MethodForRep
  RepAuto = MkMethodForRep sixel_utils_rep_auto

  --

  %foreign (sixelutils "sixel_utils_rep_center_box")
  sixel_utils_rep_center_box : Int

  export %inline
  RepCenterBox : MethodForRep
  RepCenterBox = MkMethodForRep sixel_utils_rep_center_box

  --

  %foreign (sixelutils "sixel_utils_rep_average_colors")
  sixel_utils_rep_average_colors : Int

  export %inline
  RepAverageColors : MethodForRep
  RepAverageColors = MkMethodForRep sixel_utils_rep_average_colors

  --

  %foreign (sixelutils "sixel_utils_rep_average_pixels")
  sixel_utils_rep_average_pixels : Int

  export %inline
  RepAveragePixels : MethodForRep
  RepAveragePixels = MkMethodForRep sixel_utils_rep_average_pixels

--

public export
data MethodForDiffuse = MkMethodForDiffuse Int

namespace MethodForDiffuse
  %foreign (sixelutils "sixel_utils_diffuse_symbol")
  sixel_utils_diffuse_symbol : Int -> AnyPtr

  export
  Symbolic Int MethodForDiffuse where
    hint _                         = "MethodForDiffuse"
    binding (MkMethodForDiffuse b) = b
    symbol                         = symbolBy sixel_utils_diffuse_symbol

  export
  Eq MethodForDiffuse where
    (==) x y = binding x == binding y

  export
  Show MethodForDiffuse where
    show = symbol

  --

  %foreign (sixelutils "sixel_utils_diffuse_auto")
  sixel_utils_diffuse_auto : Int

  export %inline
  DiffuseAuto : MethodForDiffuse
  DiffuseAuto = MkMethodForDiffuse sixel_utils_diffuse_auto

  --

  %foreign (sixelutils "sixel_utils_diffuse_none")
  sixel_utils_diffuse_none : Int

  export %inline
  DiffuseNone : MethodForDiffuse
  DiffuseNone = MkMethodForDiffuse sixel_utils_diffuse_none

  --

  %foreign (sixelutils "sixel_utils_diffuse_atkinson")
  sixel_utils_diffuse_atkinson : Int

  export %inline
  DiffuseAtkinson : MethodForDiffuse
  DiffuseAtkinson = MkMethodForDiffuse sixel_utils_diffuse_atkinson

  --

  %foreign (sixelutils "sixel_utils_diffuse_fs")
  sixel_utils_diffuse_fs : Int

  export %inline
  DiffuseFs : MethodForDiffuse
  DiffuseFs = MkMethodForDiffuse sixel_utils_diffuse_fs

  --

  %foreign (sixelutils "sixel_utils_diffuse_jajuni")
  sixel_utils_diffuse_jajuni : Int

  export %inline
  DiffuseJajuni : MethodForDiffuse
  DiffuseJajuni = MkMethodForDiffuse sixel_utils_diffuse_jajuni

  --

  %foreign (sixelutils "sixel_utils_diffuse_stucki")
  sixel_utils_diffuse_stucki : Int

  export %inline
  DiffuseStucki : MethodForDiffuse
  DiffuseStucki = MkMethodForDiffuse sixel_utils_diffuse_stucki

  --

  %foreign (sixelutils "sixel_utils_diffuse_burkes")
  sixel_utils_diffuse_burkes : Int

  export %inline
  DiffuseBurkes : MethodForDiffuse
  DiffuseBurkes = MkMethodForDiffuse sixel_utils_diffuse_burkes

  --

  %foreign (sixelutils "sixel_utils_diffuse_a_dither")
  sixel_utils_diffuse_a_dither : Int

  export %inline
  DiffuseADiffuse : MethodForDiffuse
  DiffuseADiffuse = MkMethodForDiffuse sixel_utils_diffuse_a_dither

  --

  %foreign (sixelutils "sixel_utils_diffuse_x_dither")
  sixel_utils_diffuse_x_dither : Int

  export %inline
  DiffuseXDither : MethodForDiffuse
  DiffuseXDither = MkMethodForDiffuse sixel_utils_diffuse_x_dither

--

public export
data QualityMode = MkQualityMode Int

namespace QualityMode
  %foreign (sixelutils "sixel_utils_quality_symbol")
  sixel_utils_quality_symbol : Int -> AnyPtr

  export
  Symbolic Int QualityMode where
    hint _                    = "QualityMode"
    binding (MkQualityMode b) = b
    symbol                    = symbolBy sixel_utils_quality_symbol

  export
  Eq QualityMode where
    (==) x y = binding x == binding y

  export
  Show QualityMode where
    show = symbol

  --

  %foreign (sixelutils "sixel_utils_quality_auto")
  sixel_utils_quality_auto : Int

  export %inline
  QualityAuto : QualityMode
  QualityAuto = MkQualityMode sixel_utils_quality_auto

  --

  %foreign (sixelutils "sixel_utils_quality_high")
  sixel_utils_quality_high : Int

  export %inline
  QualityHigh : QualityMode
  QualityHigh = MkQualityMode sixel_utils_quality_high

  --

  %foreign (sixelutils "sixel_utils_quality_low")
  sixel_utils_quality_low : Int

  export %inline
  QualityLow : QualityMode
  QualityLow = MkQualityMode sixel_utils_quality_low

  --

  %foreign (sixelutils "sixel_utils_quality_full")
  sixel_utils_quality_full : Int

  export %inline
  QualityFull : QualityMode
  QualityFull = MkQualityMode sixel_utils_quality_full

  --

  %foreign (sixelutils "sixel_utils_quality_highcolor")
  sixel_utils_quality_highcolor : Int

  export %inline
  QualityHighcolor : QualityMode
  QualityHighcolor = MkQualityMode sixel_utils_quality_highcolor

--

public export
data BuiltinDither = MkBuiltinDither Int

namespace BuiltinDither
  %foreign (sixelutils "sixel_utils_builtin_symbol")
  sixel_utils_builtin_symbol : Int -> AnyPtr

  export
  Symbolic Int BuiltinDither where
    hint _                      = "BuiltinDither"
    binding (MkBuiltinDither b) = b
    symbol                      = symbolBy sixel_utils_builtin_symbol

  export
  Eq BuiltinDither where
    (==) x y = binding x == binding y

  export
  Show BuiltinDither where
    show = symbol

  --

  %foreign (sixelutils "sixel_utils_builtin_mono_dark")
  sixel_utils_builtin_mono_dark : Int

  export %inline
  BuiltinMonoDark : BuiltinDither
  BuiltinMonoDark = MkBuiltinDither sixel_utils_builtin_mono_dark

  --

  %foreign (sixelutils "sixel_utils_builtin_mono_light")
  sixel_utils_builtin_mono_light : Int

  export %inline
  BuiltinMonoLight : BuiltinDither
  BuiltinMonoLight = MkBuiltinDither sixel_utils_builtin_mono_light

  --

  %foreign (sixelutils "sixel_utils_builtin_xterm16")
  sixel_utils_builtin_xterm16 : Int

  export %inline
  BuiltinXterm16 : BuiltinDither
  BuiltinXterm16 = MkBuiltinDither sixel_utils_builtin_xterm16

  --

  %foreign (sixelutils "sixel_utils_builtin_xterm256")
  sixel_utils_builtin_xterm256 : Int

  export %inline
  BuiltinXterm256 : BuiltinDither
  BuiltinXterm256 = MkBuiltinDither sixel_utils_builtin_xterm256

  --

  %foreign (sixelutils "sixel_utils_builtin_vt340_mono")
  sixel_utils_builtin_vt340_mono : Int

  export %inline
  BuiltinVt340Mono : BuiltinDither
  BuiltinVt340Mono = MkBuiltinDither sixel_utils_builtin_vt340_mono

  --

  %foreign (sixelutils "sixel_utils_builtin_vt340_color")
  sixel_utils_builtin_vt340_color : Int

  export %inline
  BuiltinVt340Color : BuiltinDither
  BuiltinVt340Color = MkBuiltinDither sixel_utils_builtin_vt340_color

  --

  %foreign (sixelutils "sixel_utils_builtin_g1")
  sixel_utils_builtin_g1 : Int

  export %inline
  BuiltinG1 : BuiltinDither
  BuiltinG1 = MkBuiltinDither sixel_utils_builtin_g1

  --

  %foreign (sixelutils "sixel_utils_builtin_g2")
  sixel_utils_builtin_g2 : Int

  export %inline
  BuiltinG2 : BuiltinDither
  BuiltinG2 = MkBuiltinDither sixel_utils_builtin_g2

  --

  %foreign (sixelutils "sixel_utils_builtin_g4")
  sixel_utils_builtin_g4 : Int

  export %inline
  BuiltinG4 : BuiltinDither
  BuiltinG4 = MkBuiltinDither sixel_utils_builtin_g4

  --

  %foreign (sixelutils "sixel_utils_builtin_g8")
  sixel_utils_builtin_g8 : Int

  export %inline
  BuiltinG8 : BuiltinDither
  BuiltinG8 = MkBuiltinDither sixel_utils_builtin_g8

--

public export
data PixelFormat = MkPixelFormat Int

namespace PixelFormat
  %foreign (sixelutils "sixel_utils_pixelformat_symbol")
  sixel_utils_pixelformat_symbol : Int -> AnyPtr

  export
  Symbolic Int PixelFormat where
    hint _                    = "PixelFormat"
    binding (MkPixelFormat b) = b
    symbol                    = symbolBy sixel_utils_pixelformat_symbol

  export
  Eq PixelFormat where
    (==) x y = binding x == binding y

  export
  Show PixelFormat where
    show = symbol

  --

  %foreign (sixelutils "sixel_utils_pixelformat_rgb555")
  sixel_utils_pixelformat_rgb555 : Int

  export %inline
  PixelFormatRgb555 : PixelFormat
  PixelFormatRgb555 = MkPixelFormat sixel_utils_pixelformat_rgb555

  --

  %foreign (sixelutils "sixel_utils_pixelformat_rgb565")
  sixel_utils_pixelformat_rgb565 : Int

  export %inline
  PixelFormatRgb565 : PixelFormat
  PixelFormatRgb565 = MkPixelFormat sixel_utils_pixelformat_rgb565

  --

  %foreign (sixelutils "sixel_utils_pixelformat_rgb888")
  sixel_utils_pixelformat_rgb888 : Int

  export %inline
  PixelFormatRgb888 : PixelFormat
  PixelFormatRgb888 = MkPixelFormat sixel_utils_pixelformat_rgb888

  --

  %foreign (sixelutils "sixel_utils_pixelformat_bgr555")
  sixel_utils_pixelformat_bgr555 : Int

  export %inline
  PixelFormatBgr555 : PixelFormat
  PixelFormatBgr555 = MkPixelFormat sixel_utils_pixelformat_bgr555

  --

  %foreign (sixelutils "sixel_utils_pixelformat_bgr565")
  sixel_utils_pixelformat_bgr565 : Int

  export %inline
  PixelFormatBgr565 : PixelFormat
  PixelFormatBgr565 = MkPixelFormat sixel_utils_pixelformat_bgr565

  --

  %foreign (sixelutils "sixel_utils_pixelformat_bgr888")
  sixel_utils_pixelformat_bgr888 : Int

  export %inline
  PixelFormatBgr888 : PixelFormat
  PixelFormatBgr888 = MkPixelFormat sixel_utils_pixelformat_bgr888

  --

  %foreign (sixelutils "sixel_utils_pixelformat_argb8888")
  sixel_utils_pixelformat_argb8888 : Int

  export %inline
  PixelFormatArgb8888 : PixelFormat
  PixelFormatArgb8888 = MkPixelFormat sixel_utils_pixelformat_argb8888

  --

  %foreign (sixelutils "sixel_utils_pixelformat_rgba8888")
  sixel_utils_pixelformat_rgba8888 : Int

  export %inline
  PixelFormatRgba8888 : PixelFormat
  PixelFormatRgba8888 = MkPixelFormat sixel_utils_pixelformat_rgba8888

  --

  %foreign (sixelutils "sixel_utils_pixelformat_abgr8888")
  sixel_utils_pixelformat_abgr8888 : Int

  export %inline
  PixelFormatAbgr8888 : PixelFormat
  PixelFormatAbgr8888 = MkPixelFormat sixel_utils_pixelformat_abgr8888

  --

  %foreign (sixelutils "sixel_utils_pixelformat_bgra8888")
  sixel_utils_pixelformat_bgra8888 : Int

  export %inline
  PixelFormatBgra8888 : PixelFormat
  PixelFormatBgra8888 = MkPixelFormat sixel_utils_pixelformat_bgra8888

  --

  %foreign (sixelutils "sixel_utils_pixelformat_g1")
  sixel_utils_pixelformat_g1 : Int

  export %inline
  PixelFormatG1 : PixelFormat
  PixelFormatG1 = MkPixelFormat sixel_utils_pixelformat_g1

  --

  %foreign (sixelutils "sixel_utils_pixelformat_g2")
  sixel_utils_pixelformat_g2 : Int

  export %inline
  PixelFormatG2 : PixelFormat
  PixelFormatG2 = MkPixelFormat sixel_utils_pixelformat_g2

  --

  %foreign (sixelutils "sixel_utils_pixelformat_g4")
  sixel_utils_pixelformat_g4 : Int

  export %inline
  PixelFormatG4 : PixelFormat
  PixelFormatG4 = MkPixelFormat sixel_utils_pixelformat_g4

  --

  %foreign (sixelutils "sixel_utils_pixelformat_g8")
  sixel_utils_pixelformat_g8 : Int

  export %inline
  PixelFormatG8 : PixelFormat
  PixelFormatG8 = MkPixelFormat sixel_utils_pixelformat_g8

  --

  %foreign (sixelutils "sixel_utils_pixelformat_ag88")
  sixel_utils_pixelformat_ag88 : Int

  export %inline
  PixelFormatAg88 : PixelFormat
  PixelFormatAg88 = MkPixelFormat sixel_utils_pixelformat_ag88

  --

  %foreign (sixelutils "sixel_utils_pixelformat_ga88")
  sixel_utils_pixelformat_ga88 : Int

  export %inline
  PixelFormatGa88 : PixelFormat
  PixelFormatGa88 = MkPixelFormat sixel_utils_pixelformat_ga88

  --

  %foreign (sixelutils "sixel_utils_pixelformat_pal1")
  sixel_utils_pixelformat_pal1 : Int

  export %inline
  PixelFormatPal1 : PixelFormat
  PixelFormatPal1 = MkPixelFormat sixel_utils_pixelformat_pal1

  --

  %foreign (sixelutils "sixel_utils_pixelformat_pal2")
  sixel_utils_pixelformat_pal2 : Int

  export %inline
  PixelFormatPal2 : PixelFormat
  PixelFormatPal2 = MkPixelFormat sixel_utils_pixelformat_pal2

  --

  %foreign (sixelutils "sixel_utils_pixelformat_pal4")
  sixel_utils_pixelformat_pal4 : Int

  export %inline
  PixelFormatPal4 : PixelFormat
  PixelFormatPal4 = MkPixelFormat sixel_utils_pixelformat_pal4

  --

  %foreign (sixelutils "sixel_utils_pixelformat_pal8")
  sixel_utils_pixelformat_pal8 : Int

  export %inline
  PixelFormatPal8 : PixelFormat
  PixelFormatPal8 = MkPixelFormat sixel_utils_pixelformat_pal8

--

public export
data PaletteType = MkPaletteType Int

namespace PaletteType
  %foreign (sixelutils "sixel_utils_palettetype_symbol")
  sixel_utils_palettetype_symbol : Int -> AnyPtr

  export
  Symbolic Int PaletteType where
    hint _                    = "PaletteType"
    binding (MkPaletteType b) = b
    symbol                    = symbolBy sixel_utils_palettetype_symbol

  export
  Eq PaletteType where
    (==) x y = binding x == binding y

  export
  Show PaletteType where
    show = symbol

  --

  %foreign (sixelutils "sixel_utils_palettetype_auto")
  sixel_utils_palettetype_auto : Int

  export %inline
  PaletteTypeAuto : PaletteType
  PaletteTypeAuto = MkPaletteType sixel_utils_palettetype_auto

  --

  %foreign (sixelutils "sixel_utils_palettetype_hls")
  sixel_utils_palettetype_hls : Int

  export %inline
  PaletteTypeHls : PaletteType
  PaletteTypeHls = MkPaletteType sixel_utils_palettetype_hls

  --

  %foreign (sixelutils "sixel_utils_palettetype_rgb")
  sixel_utils_palettetype_rgb : Int

  export %inline
  PaletteTypeRgb : PaletteType
  PaletteTypeRgb = MkPaletteType sixel_utils_palettetype_rgb

--

public export
data EncodePolicy = MkEncodePolicy Int

namespace EncodePolicy
  %foreign (sixelutils "sixel_utils_encodepolicy_symbol")
  sixel_utils_encodepolicy_symbol : Int -> AnyPtr

  export
  Symbolic Int EncodePolicy where
    hint _                     = "EncodePolicy"
    binding (MkEncodePolicy b) = b
    symbol                     = symbolBy sixel_utils_encodepolicy_symbol

  export
  Eq EncodePolicy where
    (==) x y = binding x == binding y

  export
  Show EncodePolicy where
    show = symbol

  --

  %foreign (sixelutils "sixel_utils_encodepolicy_auto")
  sixel_utils_encodepolicy_auto : Int

  export %inline
  EncodePolicyAuto : EncodePolicy
  EncodePolicyAuto = MkEncodePolicy sixel_utils_encodepolicy_auto

  --

  %foreign (sixelutils "sixel_utils_encodepolicy_fast")
  sixel_utils_encodepolicy_fast : Int

  export %inline
  EncodePolicyFast : EncodePolicy
  EncodePolicyFast = MkEncodePolicy sixel_utils_encodepolicy_fast

  --

  %foreign (sixelutils "sixel_utils_encodepolicy_size")
  sixel_utils_encodepolicy_size : Int

  export %inline
  EncodePolicySize : EncodePolicy
  EncodePolicySize = MkEncodePolicy sixel_utils_encodepolicy_size

--

public export
data MethodForResampling = MkMethodForResampling Int

namespace MethodForResampling
  %foreign (sixelutils "sixel_utils_res_symbol")
  sixel_utils_res_symbol : Int -> AnyPtr

  export %inline
  Symbolic Int MethodForResampling where
    hint _                            = "MethodForResampling"
    binding (MkMethodForResampling b) = b
    symbol                            = symbolBy sixel_utils_res_symbol

  export
  Eq MethodForResampling where
    (==) x y = binding x == binding y

  export
  Show MethodForResampling where
    show = symbol

  --

  %foreign (sixelutils "sixel_utils_res_nearest")
  sixel_utils_res_nearest : Int

  export %inline
  ResNearest : MethodForResampling
  ResNearest = MkMethodForResampling sixel_utils_res_nearest

  --

  %foreign (sixelutils "sixel_utils_res_gaussian")
  sixel_utils_res_gaussian : Int

  export %inline
  ResGaussian : MethodForResampling
  ResGaussian = MkMethodForResampling sixel_utils_res_gaussian

  --

  %foreign (sixelutils "sixel_utils_res_hanning")
  sixel_utils_res_hanning : Int

  export %inline
  ResHanning : MethodForResampling
  ResHanning = MkMethodForResampling sixel_utils_res_hanning

  --

  %foreign (sixelutils "sixel_utils_res_hamming")
  sixel_utils_res_hamming : Int

  export %inline
  ResHamming : MethodForResampling
  ResHamming = MkMethodForResampling sixel_utils_res_hamming

  --

  %foreign (sixelutils "sixel_utils_res_bilinear")
  sixel_utils_res_bilinear : Int

  export %inline
  ResBilinear : MethodForResampling
  ResBilinear = MkMethodForResampling sixel_utils_res_bilinear

  --

  %foreign (sixelutils "sixel_utils_res_welsh")
  sixel_utils_res_welsh : Int

  export %inline
  ResWelsh : MethodForResampling
  ResWelsh = MkMethodForResampling sixel_utils_res_welsh

  --

  %foreign (sixelutils "sixel_utils_res_bicubic")
  sixel_utils_res_bicubic : Int

  export %inline
  ResBicubic : MethodForResampling
  ResBicubic = MkMethodForResampling sixel_utils_res_bicubic

  --

  %foreign (sixelutils "sixel_utils_res_lanczos2")
  sixel_utils_res_lanczos2 : Int

  export %inline
  ResLanczos2 : MethodForResampling
  ResLanczos2 = MkMethodForResampling sixel_utils_res_lanczos2

  --

  %foreign (sixelutils "sixel_utils_res_lanczos3")
  sixel_utils_res_lanczos3 : Int

  export %inline
  ResLanczos3 : MethodForResampling
  ResLanczos3 = MkMethodForResampling sixel_utils_res_lanczos3

  --

  %foreign (sixelutils "sixel_utils_res_lanczos4")
  sixel_utils_res_lanczos4 : Int

  export %inline
  ResLanczos4 : MethodForResampling
  ResLanczos4 = MkMethodForResampling sixel_utils_res_lanczos4

--

public export
data ImageFormat = MkImageFormat Int

namespace ImageFormat
  %foreign (sixelutils "sixel_utils_format_symbol")
  sixel_utils_format_symbol : Int -> AnyPtr

  export
  Symbolic Int ImageFormat where
    hint _               = "ImageFormat"
    binding (MkImageFormat b) = b
    symbol               = symbolBy sixel_utils_format_symbol

  export
  Eq ImageFormat where
    (==) x y = binding x == binding y

  export
  Show ImageFormat where
    show = symbol

  --

  %foreign (sixelutils "sixel_utils_format_gif")
  sixel_utils_format_gif : Int

  export %inline
  FormatGif : ImageFormat
  FormatGif = MkImageFormat sixel_utils_format_gif

  --

  %foreign (sixelutils "sixel_utils_format_png")
  sixel_utils_format_png : Int

  export %inline
  FormatPng : ImageFormat
  FormatPng = MkImageFormat sixel_utils_format_png

  --

  %foreign (sixelutils "sixel_utils_format_bmp")
  sixel_utils_format_bmp : Int

  export %inline
  FormatBmp : ImageFormat
  FormatBmp = MkImageFormat sixel_utils_format_bmp

  --

  %foreign (sixelutils "sixel_utils_format_jpg")
  sixel_utils_format_jpg : Int

  export %inline
  FormatJpg : ImageFormat
  FormatJpg = MkImageFormat sixel_utils_format_jpg

  --

  %foreign (sixelutils "sixel_utils_format_tga")
  sixel_utils_format_tga : Int

  export %inline
  FormatTga : ImageFormat
  FormatTga = MkImageFormat sixel_utils_format_tga

  --

  %foreign (sixelutils "sixel_utils_format_wbmp")
  sixel_utils_format_wbmp : Int

  export %inline
  FormatWbmp : ImageFormat
  FormatWbmp = MkImageFormat sixel_utils_format_wbmp

  --

  %foreign (sixelutils "sixel_utils_format_tiff")
  sixel_utils_format_tiff : Int

  export %inline
  FormatTiff : ImageFormat
  FormatTiff = MkImageFormat sixel_utils_format_tiff

  --

  %foreign (sixelutils "sixel_utils_format_sixel")
  sixel_utils_format_sixel : Int

  export %inline
  FormatSixel : ImageFormat
  FormatSixel = MkImageFormat sixel_utils_format_sixel

  --

  %foreign (sixelutils "sixel_utils_format_pnm")
  sixel_utils_format_pnm : Int

  export %inline
  FormatPnm : ImageFormat
  FormatPnm = MkImageFormat sixel_utils_format_pnm

  --

  %foreign (sixelutils "sixel_utils_format_gd2")
  sixel_utils_format_gd2 : Int

  export %inline
  FormatGd2 : ImageFormat
  FormatGd2 = MkImageFormat sixel_utils_format_gd2

  --

  %foreign (sixelutils "sixel_utils_format_psd")
  sixel_utils_format_psd : Int

  export %inline
  FormatPsd : ImageFormat
  FormatPsd = MkImageFormat sixel_utils_format_psd

  --

  %foreign (sixelutils "sixel_utils_format_hdr")
  sixel_utils_format_hdr : Int

  export %inline
  FormatHdr : ImageFormat
  FormatHdr = MkImageFormat sixel_utils_format_hdr

--

public export
data LoopControl = MkLoopControl Int

namespace LoopControl
  %foreign (sixelutils "sixel_utils_loop_symbol")
  sixel_utils_loop_symbol : Int -> AnyPtr

  export
  Symbolic Int LoopControl where
    hint _                    = "LoopControl"
    binding (MkLoopControl b) = b
    symbol                    = symbolBy sixel_utils_loop_symbol

  export
  Eq LoopControl where
    (==) x y = binding x == binding y

  export
  Show LoopControl where
    show = symbol

  --

  %foreign (sixelutils "sixel_utils_loop_auto")
  sixel_utils_loop_auto : Int

  export %inline
  LoopAuto : LoopControl
  LoopAuto = MkLoopControl sixel_utils_loop_auto

  --

  %foreign (sixelutils "sixel_utils_loop_force")
  sixel_utils_loop_force : Int

  export %inline
  LoopForce : LoopControl
  LoopForce = MkLoopControl sixel_utils_loop_force

  --

  %foreign (sixelutils "sixel_utils_loop_disable")
  sixel_utils_loop_disable : Int

  export %inline
  LoopDisable : LoopControl
  LoopDisable = MkLoopControl sixel_utils_loop_disable

--

public export
data OptFlag = MkOptFlag Int

namespace OptFlag
  export
  Symbolic Int OptFlag where
    hint _                   = "OptFlag"
    binding (MkOptFlag flag) = flag
    symbol  (MkOptFlag flag) = "OptFlag " ++ show flag

  --

  %foreign (sixelutils "sixel_utils_optflag_input")
  sixel_utils_optflag_input : Int

  export %inline
  OptFlagInput : OptFlag
  OptFlagInput = MkOptFlag sixel_utils_optflag_input

  --

  %foreign (sixelutils "sixel_utils_optflag_output")
  sixel_utils_optflag_output : Int

  export %inline
  OptFlagOutput : OptFlag
  OptFlagOutput = MkOptFlag sixel_utils_optflag_output

  --

  %foreign (sixelutils "sixel_utils_optflag_outfile")
  sixel_utils_optflag_outfile : Int

  export %inline
  OptFlagOutfile : OptFlag
  OptFlagOutfile = MkOptFlag sixel_utils_optflag_outfile

  --

  %foreign (sixelutils "sixel_utils_optflag_7bit_mode")
  sixel_utils_optflag_7bit_mode : Int

  export %inline
  OptFlag7BitMode : OptFlag
  OptFlag7BitMode = MkOptFlag sixel_utils_optflag_7bit_mode

  --

  %foreign (sixelutils "sixel_utils_optflag_8bit_mode")
  sixel_utils_optflag_8bit_mode : Int

  export %inline
  OptFlag8BitMode : OptFlag
  OptFlag8BitMode = MkOptFlag sixel_utils_optflag_8bit_mode

  --

  %foreign (sixelutils "sixel_utils_optflag_has_gri_arg_limit")
  sixel_utils_optflag_has_gri_arg_limit : Int

  export %inline
  OptFlagHasGriArgLimit : OptFlag
  OptFlagHasGriArgLimit = MkOptFlag sixel_utils_optflag_has_gri_arg_limit

  --

  %foreign (sixelutils "sixel_utils_optflag_colors")
  sixel_utils_optflag_colors : Int

  export %inline
  OptFlagColors : OptFlag
  OptFlagColors = MkOptFlag sixel_utils_optflag_colors

  --

  %foreign (sixelutils "sixel_utils_optflag_mapfile")
  sixel_utils_optflag_mapfile : Int

  export %inline
  OptFlagMapfile : OptFlag
  OptFlagMapfile = MkOptFlag sixel_utils_optflag_mapfile

  --

  %foreign (sixelutils "sixel_utils_optflag_monochrome")
  sixel_utils_optflag_monochrome : Int

  export %inline
  OptFlagMonochrome : OptFlag
  OptFlagMonochrome = MkOptFlag sixel_utils_optflag_monochrome

  --

  %foreign (sixelutils "sixel_utils_optflag_insecure")
  sixel_utils_optflag_insecure : Int

  export %inline
  OptFlagInsecure : OptFlag
  OptFlagInsecure = MkOptFlag sixel_utils_optflag_insecure

  --

  %foreign (sixelutils "sixel_utils_optflag_invert")
  sixel_utils_optflag_invert : Int

  export %inline
  OptFlagInvert : OptFlag
  OptFlagInvert = MkOptFlag sixel_utils_optflag_invert

  --

  %foreign (sixelutils "sixel_utils_optflag_high_color")
  sixel_utils_optflag_high_color : Int

  export %inline
  OptFlagHighColor : OptFlag
  OptFlagHighColor = MkOptFlag sixel_utils_optflag_high_color

  --

  %foreign (sixelutils "sixel_utils_optflag_use_macro")
  sixel_utils_optflag_use_macro : Int

  export %inline
  OptFlagUseMacro : OptFlag
  OptFlagUseMacro = MkOptFlag sixel_utils_optflag_use_macro

  --

  %foreign (sixelutils "sixel_utils_optflag_macro_number")
  sixel_utils_optflag_macro_number : Int

  export %inline
  OptFlagMacroNumber : OptFlag
  OptFlagMacroNumber = MkOptFlag sixel_utils_optflag_macro_number

  --

  %foreign (sixelutils "sixel_utils_optflag_complexion_score")
  sixel_utils_optflag_complexion_score : Int

  export %inline
  OptFlagComplexionScore : OptFlag
  OptFlagComplexionScore = MkOptFlag sixel_utils_optflag_complexion_score

  --

  %foreign (sixelutils "sixel_utils_optflag_ignore_delay")
  sixel_utils_optflag_ignore_delay : Int

  export %inline
  OptFlagIgnoreDelay : OptFlag
  OptFlagIgnoreDelay = MkOptFlag sixel_utils_optflag_ignore_delay

  --

  %foreign (sixelutils "sixel_utils_optflag_static")
  sixel_utils_optflag_static : Int

  export %inline
  OptFlagStatic : OptFlag
  OptFlagStatic = MkOptFlag sixel_utils_optflag_static

  --

  %foreign (sixelutils "sixel_utils_optflag_diffusion")
  sixel_utils_optflag_diffusion : Int

  export %inline
  OptFlagDiffusion : OptFlag
  OptFlagDiffusion = MkOptFlag sixel_utils_optflag_diffusion

  --

  %foreign (sixelutils "sixel_utils_optflag_find_largest")
  sixel_utils_optflag_find_largest : Int

  export %inline
  OptFlagFindLargest : OptFlag
  OptFlagFindLargest = MkOptFlag sixel_utils_optflag_find_largest

  --

  %foreign (sixelutils "sixel_utils_optflag_select_color")
  sixel_utils_optflag_select_color : Int

  export %inline
  OptFlagSelectColor : OptFlag
  OptFlagSelectColor = MkOptFlag sixel_utils_optflag_select_color

  --

  %foreign (sixelutils "sixel_utils_optflag_crop")
  sixel_utils_optflag_crop : Int

  export %inline
  OptFlagCrop : OptFlag
  OptFlagCrop = MkOptFlag sixel_utils_optflag_crop

  --

  %foreign (sixelutils "sixel_utils_optflag_width")
  sixel_utils_optflag_width : Int

  export %inline
  OptFlagWidth : OptFlag
  OptFlagWidth = MkOptFlag sixel_utils_optflag_width

  --

  %foreign (sixelutils "sixel_utils_optflag_height")
  sixel_utils_optflag_height : Int

  export %inline
  OptFlagHeight : OptFlag
  OptFlagHeight = MkOptFlag sixel_utils_optflag_height

  --

  %foreign (sixelutils "sixel_utils_optflag_resampling")
  sixel_utils_optflag_resampling : Int

  export %inline
  OptFlagResampling : OptFlag
  OptFlagResampling = MkOptFlag sixel_utils_optflag_resampling

  --

  %foreign (sixelutils "sixel_utils_optflag_quality")
  sixel_utils_optflag_quality : Int

  export %inline
  OptFlagQuality : OptFlag
  OptFlagQuality = MkOptFlag sixel_utils_optflag_quality

  --

  %foreign (sixelutils "sixel_utils_optflag_loopmode")
  sixel_utils_optflag_loopmode : Int

  export %inline
  OptFlagLoopmode : OptFlag
  OptFlagLoopmode = MkOptFlag sixel_utils_optflag_loopmode

  --

  %foreign (sixelutils "sixel_utils_optflag_palette_type")
  sixel_utils_optflag_palette_type : Int

  export %inline
  OptFlagPaletteType : OptFlag
  OptFlagPaletteType = MkOptFlag sixel_utils_optflag_palette_type

  --

  %foreign (sixelutils "sixel_utils_optflag_builtin_palette")
  sixel_utils_optflag_builtin_palette : Int

  export %inline
  OptFlagBuiltinPalette : OptFlag
  OptFlagBuiltinPalette = MkOptFlag sixel_utils_optflag_builtin_palette

  --

  %foreign (sixelutils "sixel_utils_optflag_encode_policy")
  sixel_utils_optflag_encode_policy : Int

  export %inline
  OptFlagEncodePolicy : OptFlag
  OptFlagEncodePolicy = MkOptFlag sixel_utils_optflag_encode_policy

  --

  %foreign (sixelutils "sixel_utils_optflag_bgcolor")
  sixel_utils_optflag_bgcolor : Int

  export %inline
  OptFlagBgcolor : OptFlag
  OptFlagBgcolor = MkOptFlag sixel_utils_optflag_bgcolor

  --

  %foreign (sixelutils "sixel_utils_optflag_penetrate")
  sixel_utils_optflag_penetrate : Int

  export %inline
  OptFlagPenetrate : OptFlag
  OptFlagPenetrate = MkOptFlag sixel_utils_optflag_penetrate

  --

  %foreign (sixelutils "sixel_utils_optflag_pipe_mode")
  sixel_utils_optflag_pipe_mode : Int

  export %inline
  OptFlagPipeMode : OptFlag
  OptFlagPipeMode = MkOptFlag sixel_utils_optflag_pipe_mode

  --

  %foreign (sixelutils "sixel_utils_optflag_verbose")
  sixel_utils_optflag_verbose : Int

  export %inline
  OptFlagVerbose : OptFlag
  OptFlagVerbose = MkOptFlag sixel_utils_optflag_verbose

  --

  %foreign (sixelutils "sixel_utils_optflag_version")
  sixel_utils_optflag_version : Int

  export %inline
  OptFlagVersion : OptFlag
  OptFlagVersion = MkOptFlag sixel_utils_optflag_version

  --

  %foreign (sixelutils "sixel_utils_optflag_help")
  sixel_utils_optflag_help : Int

  export %inline
  OptFlagHelp : OptFlag
  OptFlagHelp = MkOptFlag sixel_utils_optflag_help

max_stars_repo_name: Kaiepi/id-sixel

max_issues_repo_name: Kaiepi/id-sixel

max_forks_repo_name: Kaiepi/id-sixel


text:
data Format = CInt Format | CString Format | COther Char Format | CEnd

charsToFormat : List Char -> Format
charsToFormat [] = CEnd
charsToFormat ('%' :: 's' :: xs) = CString $ charsToFormat xs
charsToFormat ('%' :: 'd' :: xs) = CInt $ charsToFormat xs
charsToFormat (x :: xs) = COther x $ charsToFormat xs

formatToType : Format -> Type
formatToType (CInt x) = Int -> formatToType x
formatToType (CString x) = String -> formatToType x
formatToType (COther c x) = formatToType x
formatToType CEnd = String

formatToFormatType : (f : Format) -> (acc : String) -> formatToType f
formatToFormatType (CInt y) acc = (\i => formatToFormatType y (acc ++ show i))
formatToFormatType (CString y) acc = (\s' => formatToFormatType y (acc ++ s'))
formatToFormatType (COther c y) acc = formatToFormatType y (acc ++ singleton c)
formatToFormatType CEnd acc = acc

printf : (s : String) -> formatToType (charsToFormat (unpack s))
printf s = formatToFormatType (charsToFormat (unpack s)) ""

greeting : String -> Int -> String
greeting = printf "Hello %s %d"

max_stars_repo_name: jimmyhmiller/one-hundred-lines-or-less

max_issues_repo_name: jimmyhmiller/one-hundred-lines-or-less

max_forks_repo_name: jimmyhmiller/one-hundred-lines-or-less


text:
-- --------------------------------------------------------------- [ Query.idr ]
-- Module    : Query.idr
-- Copyright : (c) Jan de Muijnck-Hughes
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
||| Predefined Query Wrappers for XPath stuff.
module XML.XPath.Query

import XML.DOM
import XML.XPath

%access export

||| Use XPath to find some nodes satisfying some query
|||
||| @convErr Convert XPathError to a local Error Type
||| @qstr    The query to run.
||| @node    The thing we are querying
getNodes : (convErr : XPathError -> a)
        -> (qstr : String)
        -> (node : Document ty)
        -> {auto prf : CanQuery ty}
        -> Either a (ty' ** XPathResult ty')
getNodes convErr qstr doc =
  case query qstr doc of
    Left err  => Left $ convErr err
    Right res => Right res

||| Use XPath to find the first node that satisfies some query.
|||
||| @convErr Convert XPathError to a local Error Type
||| @qstr    The query to run.
||| @node    The thing we are querying
getNode : (convErr : XPathError -> a)
       -> (qstr : String)
       -> (node : Document ty)
       -> {auto prf : CanQuery ty}
       -> Either a (ty' ** Document ty')
getNode convErr qstr doc = do
  (_ ** res) <- getNodes convErr qstr doc
  case res of -- QueryError qstr loc msg
    Empty    => Left (convErr $ SingletonError qstr)
    (Nodes _ (x::_)) => Right (_ ** x)

||| Use XPath to find nodes satisfying some query get the text or
||| cdata inside or a specific attribute.
|||
||| @test    The test to execute.
||| @convErr Convert XPathError to a local error type.
||| @qstr    The query to run.
||| @node    The thing we are querying.
getNodeValues : (test : XPath ty' (TEST b))
             -> (convErr : XPathError -> a)
             -> (qstr : String)
             -> (node  : Document ty)
             -> {auto prfB : ValidNode ty}
             -> {auto prf : CanQuery ty}
             -> Either a (List String)
getNodeValues test convErr qstr doc = do
    (_ ** res) <- getNodes convErr (concat [qstr, "/", show test]) doc
    case res of
      Empty => pure Nil
      (Nodes prf xs) => do
        let vals = mapMaybe (\x => getNodeValue {prf=prf} x) xs
        pure vals

||| Use XPath to find the first node that satisfies some query get the
||| text or cdata inside or a specific attribute.
|||
||| @test    The test to execute.
||| @convErr Convert XPathError to a local error type.
||| @qstr    The query to run.
||| @node    The thing we are querying.
getNodeValue : (test : XPath ty' (TEST b))
            -> (convErr : XPathError -> a)
            -> (qstr : String)
            -> (node : Document ty)
            -> {auto prfV : ValidNode ty}
            -> {auto prf : CanQuery ty}
            -> Either a String
getNodeValue test convErr qstr doc = do
    res <- getNodeValues test convErr qstr doc
    case res of
      Nil    => Left (convErr $ SingletonError (qstr))
      (x::_) => Right x

||| Use XPath to get the values for a named attribute in a node satisfying the
||| given Query
|||
||| @name    The name of the attribute.
||| @convErr Convert XPathError to a local error type.
||| @qstr    The query to run.
||| @node    The thing we are querying.
getNamedAttrs : (name : String)
             -> (convErr : XPathError -> a)
             -> (qstr : String)
             -> (node : Document ty)
             -> {auto prfV : ValidNode ty}
             -> {auto prf : CanQuery ty}
             -> Either a (List String)
getNamedAttrs name convErr qstr doc = getNodeValues (Attr name) convErr qstr doc

||| Use XPath to get the *first* value for a named attribute in a node
||| satisfying the given Query
|||
||| @name    The name of the attribute.
||| @convErr Convert XPathError to a local error type.
||| @qstr    The query to run.
||| @node    The thing we are querying.
getNamedAttr : (name : String)
            -> (convErr : XPathError -> a)
            -> (qstr : String)
            -> (node : Document ty)
            -> {auto prfV : ValidNode ty}
            -> {auto prf : CanQuery ty}
            -> Either a String
getNamedAttr name convErr qstr doc = getNodeValue (Attr name) convErr qstr doc

||| Use XPath to get the text values for the nodes satisfying the
||| given Query
|||
||| @convErr Convert XPathError to a local error type.
||| @qstr    The query to run.
||| @node    The thing we are querying.
getTextNodes : (convErr : XPathError -> a)
            -> (qstr : String)
            -> (node : Document ty)
            -> {auto prfV : ValidNode ty}
            -> {auto prf : CanQuery ty}
            -> Either a (List String)
getTextNodes convErr qstr doc = getNodeValues Text convErr qstr doc

||| Use XPath to get the text value for the first node that satisfies
||| the given Query
|||
||| @convErr Convert XPathError to a local error type.
||| @qstr    The query to run.
||| @node    The thing we are querying.
getTextNode : (convErr : XPathError -> a)
           -> (qstr : String)
           -> (node : Document ty)
            -> {auto prfV : ValidNode ty}
           -> {auto prf : CanQuery ty}
           -> Either a String
getTextNode convErr qstr doc = getNodeValue Text convErr qstr doc

||| Use XPath to get the CData values for the nodes satisfying the
||| given Query
|||
||| @convErr Convert XPathError to a local error type.
||| @qstr    The query to run.
||| @node    The thing we are querying.
getCDataNodes : (convErr : XPathError -> a)
             -> (qstr : String)
             -> (node : Document ty)
             -> {auto prf : CanQuery ty}
            -> {auto prfV : ValidNode ty}
             -> Either a (List String)
getCDataNodes convErr qstr doc = getNodeValues CData convErr qstr doc

||| Use XPath to get the CData value for the first node that satisfies
||| the given Query
|||
||| @convErr Convert XPathError to a local error type.
||| @qstr    The query to run.
||| @node    The thing we are querying.
getCDataNode : (convErr : XPathError -> a)
            -> (qstr : String)
            -> (node : Document ty)
            -> {auto prfV : ValidNode ty}
            -> {auto prf : CanQuery ty}
            -> Either a String
getCDataNode convErr qstr doc = getNodeValue CData convErr qstr doc

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

max_stars_repo_name: jfdm/idris-xml

max_issues_repo_name: jfdm/idris-xml

max_forks_repo_name: jfdm/idris-xml


text:
module Minecraft.Core.Entity.Pickup.Export

import public Minecraft.Core.Entity.Pickup

%default total

max_stars_repo_name: po-stulate/postulate

max_issues_repo_name: po-stulate/postulate

max_forks_repo_name: po-stulate/postulate


text:
module Minecraft.Base.PreClassic.Stone.Item

import public Minecraft.Base.PreClassic.Stone
import public Minecraft.Core.Item.Export
import public Minecraft.Core.Item.Put.Export
import public Minecraft.Data.Type.Vtbl

%default total

namespace Export
  public export %hint stoneItem : Item Stone.Item
  public export %hint putStone  : Put  Stone.Item
  public export %hint stoneVtbl : Vtbl Stone.Item


text:
module BatchedQueue

import Queue

%default total
%access private

export
data BatchedQueue a = BQ (List a) (List a)

check : List a -> List a -> BatchedQueue a
check [] r = BQ (reverse r) []
check f  r = BQ f           r

export
Queue BatchedQueue where
  empty = BQ [] []
  isEmpty (BQ f r) = isNil f

  snoc (BQ f r) x = check f (x :: r)

  head (BQ []       _) = idris_crash "empty queue"
  head (BQ (x :: f) r) = x

  tail (BQ []       _) = idris_crash "empty queue"
  tail (BQ (x :: f) r) = check f r


text:
-- ----------------------------------------------------------- [ DataTypes.idr ]
-- Module      : Exercises.Test.DataTypes
-- Description : Test covering the Chapter 4 exercises in Edwin Brady's
--               book, "Type-Driven Development with Idris."
-- --------------------------------------------------------------------- [ EOH ]
module Exercises.Test.DataTypes

import Exercises.DataTypes

import Test.Helpers

import Data.Vect
%hide Data.Vect.overLength

%access export

implementation Eq (Tree Integer) where
  Empty == Empty                     = True
  (Node l1 x1 r1) == (Node l2 x2 r2) = x1 == x2 && l1 == l2 && r1 == r2
  _ == _                             = False

implementation Show (Tree Integer) where
  show t = "#<Tree>" -- FIXME

testListToTree : IO Bool
testListToTree =
  "listToTree" `assertEqual'` Node (Node Empty 1 Empty)
                                  2
                                  (Node (Node Empty 3 (Node Empty 4 Empty))
                                        5
                                        Empty) $
  listToTree [1,4,3,5,2]

testTreeToList : IO Bool
testTreeToList =
  "treeToList" `assertEqual'` [1..9] $
  treeToList (listToTree [4,1,8,7,2,3,9,5,6])

allTests : List (IO Bool)
allTests = [ testListToTree
           , testTreeToList
           ]

runTests : IO (Vect (length DataTypes.allTests) Bool)
runTests = testChapter "4: User Defined Data Types" allTests

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

max_stars_repo_name: yurrriq/tdd-with-idris

max_issues_repo_name: yurrriq/tdd-with-idris

max_forks_repo_name: yurrriq/tdd-with-idris


text:
{-
0.42
1.68
1.34
0.34
-}
module Main

main : IO ()
main =
  traverse_
    (\op => printLn $ 0.84 `op` 0.5)
    [(*), (/), (+), (-)]

max_stars_repo_name: Despair/idris-cil

max_issues_repo_name: Despair/idris-cil

max_forks_repo_name: Despair/idris-cil


text:
module Sixel.Dither

import Data.Buffer
import System.FFI

import Sixel.Library
import Sixel.Symbols
import Sixel.Allocator

public export
PrimDither : Type
PrimDither = GCAnyPtr

export
data Dither : (0 n : Nat) -> Type where
  PointDither : PrimDither -> Dither Z
  RootDither  : Dither n -> Dither (S n)

%foreign (sixelutils "sixel_utils_dither_ptr_new")
sixel_utils_dither_ptr_new :  PrimIO (Ptr AnyPtr)

%foreign (sixelutils "sixel_utils_dither_ptr_deref")
sixel_utils_dither_ptr_deref : Ptr AnyPtr -> AnyPtr

%foreign (sixel "sixel_dither_new")
sixel_dither_new : Ptr AnyPtr -> (ncolors : Int) -> PrimAllocator -> PrimIO Int

%foreign (sixel "sixel_dither_get")
sixel_dither_get : (builtin : Int) -> PrimIO AnyPtr

%foreign (sixel "sixel_dither_ref")
sixel_dither_ref : PrimDither -> ()

%foreign (sixel "sixel_dither_unref")
sixel_dither_unref : PrimDither -> ()

%foreign (sixel "sixel_dither_unref")
sixel_dither_destroy : AnyPtr -> PrimIO ()

%foreign (sixel "sixel_dither_initialize")
sixel_dither_initialize :
  PrimDither -> (pixels : Buffer) -> (w : Int) -> (h : Int) ->
    (pixelFormat : Int) -> (large : Int) -> (rep : Int) -> (quality : Int) ->
    PrimIO Int

%foreign (sixel "sixel_dither_set_diffusion_type")
sixel_dither_set_diffusion_type : PrimDither -> (diffuse : Int) -> ()

%foreign (sixel "sixel_dither_get_num_of_palette_colors")
sixel_dither_get_num_of_palette_colors : PrimDither -> Int

%foreign (sixel "sixel_dither_get_num_of_histogram_colors")
sixel_dither_get_num_of_histogram_colors : PrimDither -> Int

%foreign (sixel "sixel_dither_get_palette")
sixel_dither_get_palette : PrimDither -> String

%foreign (sixel "sixel_dither_set_palette")
sixel_dither_set_palette : PrimDither -> (palette : String) -> ()

%foreign (sixel "sixel_dither_set_complexion_score")
sixel_dither_set_complexion_score : PrimDither -> (score : Int) -> ()

%foreign (sixel "sixel_dither_set_body_only")
sixel_dither_set_body_only : PrimDither -> (setting : Int) -> ()

%foreign (sixel "sixel_dither_set_optimize_palette")
sixel_dither_set_optimize_palette : PrimDither -> (setting : Int) -> ()

%foreign (sixel "sixel_dither_set_pixelformat")
sixel_dither_set_pixelformat : PrimDither -> (pixelFormat : Int) -> ()

%foreign (sixel "sixel_dither_set_transparent")
sixel_dither_set_transparent : PrimDither -> (index : Int) -> ()

export
MkDither : {auto n : Nat} ->
  {default (-1) ncolors : Int} ->
  {default (getNullAllocator n) alloc : Allocator n} ->
  IO (Either Status (Dither Z))
MkDither {ncolors} {alloc} = do
  ppdither <- fromPrim sixel_utils_dither_ptr_new
  status   <- MkStatus <$> fromPrim (sixel_dither_new ppdither ncolors (toPrim alloc))
  pdither  <- onCollectAny (sixel_utils_dither_ptr_deref ppdither) (\pd => fromPrim $ sixel_dither_destroy pd)
  pure $ if succeeded status then Right (PointDither pdither) else Left status

export
getDither : BuiltinDither -> IO (Maybe (Dither Z))
getDither builtin = do
  ptr     <- fromPrim $ sixel_dither_get $ binding builtin
  pdither <- onCollectAny ptr (\pd => fromPrim $ sixel_dither_destroy pd)
  pure $ if prim__isConcreteAny ptr
            then Just (PointDither pdither)
            else Nothing

export
ref : Dither n -> IO (Dither (S n))
ref (RootDither dither)          = RootDither <$> ref dither
ref dither@(PointDither pdither) = let _ = sixel_dither_ref pdither in pure $ RootDither dither

export
unref : Dither (S n) -> IO (Dither n)
unref (RootDither dither@(RootDither _))        = RootDither <$> unref dither
unref (RootDither dither@(PointDither pdither)) = let _ = sixel_dither_unref pdither in pure dither

export
refs : Dither n -> Nat
refs (RootDither dither) = S (refs dither)
refs (PointDither _)     = Z

export
toPrim : Dither n -> PrimDither
toPrim (RootDither dither)   = toPrim dither
toPrim (PointDither pdither) = pdither

export
initialize :
  Dither n -> (image : Buffer) -> (w : Int) -> (h : Int) ->
    PixelFormat -> MethodForLargest -> MethodForRep -> QualityMode ->
    IO (Either Status ())
initialize dither pixels w h pixelformat large rep quality = let pdither = toPrim dither in do
  status <- MkStatus <$> fromPrim (sixel_dither_initialize
    (toPrim dither) pixels w h (binding pixelformat) (binding large) (binding rep) (binding quality))
  pure $ if succeeded status then Right () else Left status

export %inline
setDiffusionType : Dither n -> MethodForDiffuse -> IO ()
setDiffusionType dither methodForDiffuse =
  pure $ sixel_dither_set_diffusion_type (toPrim dither) (binding methodForDiffuse)

export %inline
getNumOfPaletteColors : Dither n -> IO Int
getNumOfPaletteColors dither = pure $ sixel_dither_get_num_of_palette_colors (toPrim dither)

export %inline
getNumOfHistogramColors : Dither n -> IO Int
getNumOfHistogramColors dither = pure $ sixel_dither_get_num_of_histogram_colors (toPrim dither)

export %inline
setComplexionScore : Dither n -> (score : Int) -> IO ()
setComplexionScore dither score = pure $ sixel_dither_set_complexion_score (toPrim dither) score

export %inline
setBodyOnly : Dither n -> (setting : Bool) -> IO ()
setBodyOnly dither setting = pure $ sixel_dither_set_body_only (toPrim dither) (ifThenElse setting 1 0)

export %inline
setOptimizePalette : Dither n -> (setting : Bool) -> IO ()
setOptimizePalette dither setting = pure $ sixel_dither_set_optimize_palette (toPrim dither) (ifThenElse setting 1 0)

export %inline
setPixelFormat : Dither n -> PixelFormat -> IO ()
setPixelFormat dither pixelformat = pure $ sixel_dither_set_pixelformat (toPrim dither) (binding pixelformat)

export %inline
setTransparent : Dither n -> (index : Int) -> IO ()
setTransparent dither setting = pure $ sixel_dither_set_transparent (toPrim dither) setting


text:
module System.Console.Extra

import Data.List
import Data.String
import System.File
import System.Info
import System

import public Data.Fuel

ignoreStdOut : String
ignoreStdOut =
  if isWindows
     then ">NUL"
     else ">/dev/null"

ignoreStdErr : String
ignoreStdErr =
  if isWindows
     then "2>NUL"
     else "2>/dev/null"

redirectStdErr : String
redirectStdErr = "2>&1"

||| Ignore the stdout and stderr from the given command and return
||| the status code resulting from running the command.
export
ignoreOutput : HasIO io => (cmd : String) -> io Int
ignoreOutput cmd = system $ unwords [cmd, ignoreStdOut, redirectStdErr]

||| Eat the stdout and return True if there was any
||| output to stdout (and stderror if ignoreStdErr is False).
export
eatOutput : HasIO io => (ignoreStdErr : Bool) -> (cmd : String) -> io Bool
eatOutput ignStdErr cmd = do
  let fullCmd = unwords [cmd, (if ignStdErr then ignoreStdErr else redirectStdErr)]
  Right h <- popen fullCmd Read
    | Left _ => pure False
  Right l <- fGetLine h
    | Left _ => pure False
  ignore $ pclose h
  pure $ l /= ""

||| Read lines from the given command's stdout.
export
readLines : HasIO io => Fuel -> (ignoreStdErr : Bool) -> (cmd : String) -> io (List String)
readLines fuel ignStdErr cmd = do
    let fullCmd = unwords [cmd, (if ignStdErr then ignoreStdErr else redirectStdErr)]
    Right h <- popen fullCmd Read
      | _ => pure []
    lines <- readLines' fuel h []
    ignore $ pclose h
    pure lines
  where
    readLines' : Fuel -> File -> List String -> io (List String)
    readLines' Dry _ acc = pure $ reverse acc
    readLines' (More fuel) h acc =
      if !(fEOF h)
         then readLines' Dry h acc
         else do
           Right l <- fGetLine h
             | Left _ => readLines' Dry h acc
           readLines' fuel h (l :: acc)

||| Prompt the user for confirmation to do something.
export
confirm : HasIO io => (message : String) -> io Bool
confirm message = do
  putStr $ message ++ " [Y/n] "
  response <- getLine
  case response of
       ""  => pure True
       "y" => pure True
       "Y" => pure True
       _   => pure False

max_stars_repo_name: memoryruins/idv

max_issues_repo_name: memoryruins/idv

max_forks_repo_name: memoryruins/idv


text:
import Data.So
import Data.List.Quantifiers
import Data.String.Views
import Data.List

allowedWords : List String
allowedWords = [ "foo", "bar", "baz" ]

data StrPrefix : StrList outer -> StrList inner -> Type where
  Empty : StrPrefix (SCons x xs) SNil
  Next : StrPrefix ys xs -> StrPrefix (SCons x ys) (SCons x xs)

prefixWorks : StrPrefix (strList "foo12312") (strList "foo")
prefixWorks = Next (Next (Next Empty))

anyDoesNot : Any ( \inner => StrPrefix (strList "bar1234") (strList inner) ) Main.allowedWords
--anyDoesNot = There (Here (Next (Next (Next Empty))))
anyDoesNot = There (Here (Next (Next (Next Empty))))

infixes : List String
infixes = filter (\x => isInfixOf x "bar1234") Main.allowedWords

numberInfixes : String -> Nat
numberInfixes word = length $ filter (\w => isInfixOf w word) Main.allowedWords

isGT : GT (length Main.infixes) Z
isGT = LTESucc LTEZero

print : (w:String) -> { auto prf : GT (numberInfixes w) Z } -> String
print w = w

x : String
x = print "bax1234"

anyRefl : Any ( \inner => (=) "bar" inner) Main.allowedWords
anyRefl = There (Here Refl)

max_stars_repo_name: janschultecom/seo-router

max_issues_repo_name: janschultecom/seo-router

max_forks_repo_name: janschultecom/seo-router


text:
module Main

import Graphics.SDL2
import Effect.Random
import Effects
import Data.Vect
import System
import Prelude.Providers
import Data.String

%access public export

record Body where
   constructor MkBody
   body_x, body_y : Int
   body_vel_x, body_vel_y, body_remainder_x, body_remainder_y : Double

-- TODO make vectors in Body
somePos : Vect 4 Int
somePos = [0,0, 0, 0]

implementation Show Body where
        show body = "(MkBody " <+> show (body_x body)
                    <+> "," <+> show (body_y body)
                    <+> "," <+> show (body_vel_x body)
                    <+> "," <+> show (body_vel_y body)
                    <+> "," <+> show (body_remainder_x body)
                    <+> "," <+> show (body_remainder_y body)
                    <+> ")"

body : Renderer -> Body -> IO ()
body renderer body =  do
  filledEllipse renderer (body_x body) (body_y body) 10 10 255 0 0 255

nbody_count : Int
nbody_count = 30

window_width : Int
window_width = 400

window_height : Int
window_height = 500

draw : Renderer -> List Body -> IO ()
draw renderer bodys =  do
   filledRect renderer 0 0 900 900 255 255 254 254
   traverse_ (body renderer) bodys

centerFunc : (Int, (Double, Double)) -> Body -> (Int, (Double, Double))
centerFunc (0, _) body = (1, cast $ body_x body, cast $ body_y body)
centerFunc (ix, (prev_x, prev_y)) body =
    (1,
    prev_x * prevFrac + fraction * (cast $ body_x body),
    prev_y * prevFrac + fraction * (cast $ body_y body))
           where
              fraction = 1 / cast ix
              prevFrac = 1 - fraction

findMassCenter : List Body -> (Double, Double)
findMassCenter = snd . foldl centerFunc (0, 0, 0)

updateWithVel : Double -> Double -> Int -> Int
updateWithVel x y d = (cast x) + (cast y) + d

stripDecimals : Double -> Int
stripDecimals = cast

recordUpdate : Integer -> (Double, Double) -> Body -> Body
recordUpdate fpsI center body =
    let  xchange : Double = ((fst center) - (cast $ body_x body))
         ychange : Double = ((fst center) - (cast $ body_y body))
         new_x_vel : Double = (xchange * fps + (body_vel_x body) )
         new_y_vel = (ychange * fps + (body_vel_y body))
         new_body_remainder_x = (new_x_vel - (cast $ stripDecimals new_x_vel)) + body_remainder_x body
         new_body_remainder_y = (new_y_vel - (cast $ stripDecimals new_y_vel)) + body_remainder_x body
         new_body_remainder_x' = if abs new_body_remainder_x > 1 then 0.0 else  new_body_remainder_x
         new_body_remainder_y' = if abs new_body_remainder_y > 1 then 0.0 else  new_body_remainder_y
    in
        (record { body_vel_x = new_x_vel,
                  body_vel_y = new_y_vel,
                  body_remainder_x = new_body_remainder_x',
                  body_remainder_y = new_body_remainder_y',
                  body_x $= updateWithVel (body_vel_x body) new_body_remainder_x,
                  body_y $= updateWithVel (body_vel_y body) new_body_remainder_y
               } body)
  where
     fps = (cast fpsI) / 1000

update : Integer -> List Body -> List Body
update fps bodies =
  let center = findMassCenter bodies
  in map (recordUpdate fps center) bodies

windowLoop : Renderer -> Integer -> List Body -> IO ()
windowLoop renderer fps bodys = do
   start <- clockTime
   renderClear renderer
   draw renderer bodys
   renderPresent renderer
   end <- clockTime
   let diff = nanoseconds end - nanoseconds start
   isQuit <- pollEventsForQuit
   case bodys of
        (x :: _)  => putStrLn $ show x
        [] => pure ()
   if isQuit then
           putStrLn "hello hello_world!"
           else windowLoop renderer diff $ update 1 bodys

randomNumbers : Int -> Integer -> Int -> IO (List Integer)
randomNumbers 0 _ _ = pure empty
randomNumbers depth x max = do
    out <- run (do
            srand x
            rndInt 0 (cast max)
            )
    res <- randomNumbers (depth -1) out max
    pure $ res <+> pure out

makeBodys : List Integer -> List Integer -> List Body
makeBodys rngIntWidth rngInthHeights = do
    (width, height) <- zip rngIntWidth rngInthHeights
    pure $ MkBody (fromInteger width) (fromInteger height) 0 0 0 0

askInt : String -> IO (Maybe Integer)
askInt msg = do
  putStrLn msg
  resp <- getLine
  pure $ parseInteger resp
    -- the readInt function is left as an exercise

nbodyFunc : IO ()
nbodyFunc = do
    seed <- fromMaybe 22 <$> askInt "Seed plz"
    rngIntWidth <- randomNumbers nbody_count seed window_width
    rngInthHeights <- randomNumbers nbody_count (seed * 5) window_height
    initialRender <- init window_width window_height
    windowLoop initialRender 0 (makeBodys rngIntWidth rngInthHeights)

max_stars_repo_name: jappeace/idris-age-of-conquerors

max_issues_repo_name: jappeace/idris-age-of-conquerors

max_forks_repo_name: jappeace/idris-age-of-conquerors


text:
||| Note: The difference to a 'strict' Writer implementation is
||| that accumulation of values does not happen in the
||| Applicative and Monad instances but when invoking `Writer`-specific
||| functions like `writer` or `listen`.
module Control.Monad.Writer.CPS

import Control.Monad.Identity
import Control.Monad.Trans

%default total

||| A writer monad parameterized by:
|||
|||   @w the output to accumulate.
|||
|||   @m The inner monad.
|||
||| The `pure` function produces the output `neutral`, while `>>=`
||| combines the outputs of the subcomputations using `<+>`.
public export
record WriterT (w : Type) (m : Type -> Type) (a : Type) where
  constructor MkWriterT
  unWriterT : w -> m (a, w)

||| Construct an writer computation from a (result,output) computation.
||| (The inverse of `runWriterT`.)
public export %inline
writerT : (Functor m, Semigroup w) => m (a, w) -> WriterT w m a
writerT f = MkWriterT $ \w => (\(a,w') => (a,w <+> w')) <$> f

||| Unwrap a writer computation.
||| (The inverse of 'writerT'.)
public export %inline
runWriterT : Monoid w => WriterT w m a -> m (a,w)
runWriterT m = unWriterT m neutral

||| Extract the output from a writer computation.
public export %inline
execWriterT : (Functor m, Monoid w) => WriterT w m a -> m w
execWriterT = map snd . runWriterT

||| Map both the return value and output of a computation using
||| the given function.
public export %inline
mapWriterT :  (Functor n, Monoid w, Semigroup w')
           => (m (a, w) -> n (b, w')) -> WriterT w m a -> WriterT w' n b
mapWriterT f m = MkWriterT $ \w =>
                  (\(a,w') => (a,w <+> w')) <$> f (runWriterT m)

--------------------------------------------------------------------------------
--          Writer Functions
--------------------------------------------------------------------------------

||| The `return` function produces the output `neutral`, while `>>=`
||| combines the outputs of the subcomputations using `<+>`.
public export
Writer : Type -> Type -> Type
Writer w = WriterT w Identity

||| Unwrap a writer computation as a (result, output) pair.
public export %inline
runWriter : Monoid w => Writer w a -> (a, w)
runWriter = runIdentity . runWriterT

||| Extract the output from a writer computation.
public export %inline
execWriter : Monoid w => Writer w a -> w
execWriter = runIdentity . execWriterT

||| Map both the return value and output of a computation using
||| the given function.
public export %inline
mapWriter :  (Monoid w, Semigroup w')
          => ((a, w) -> (b, w')) -> Writer w a -> Writer w' b
mapWriter f = mapWriterT $ \(Id p) => Id (f p)

--------------------------------------------------------------------------------
--          Implementations
--------------------------------------------------------------------------------

public export %inline
Functor m => Functor (WriterT w m) where
  map f m = MkWriterT $ \w => (\(a,w') => (f a,w')) <$> unWriterT m w

public export %inline
Monad m => Applicative (WriterT w m) where
  pure a = MkWriterT $ \w => pure (a,w)
  MkWriterT mf <*> MkWriterT mx =
    MkWriterT $ \w => do (f,w1) <- mf w
                         (a,w2) <- mx w1
                         pure (f a,w2)

public export %inline
(Monad m, Alternative m) => Alternative (WriterT w m) where
  empty = MkWriterT $ \_ => empty
  MkWriterT m <|> mn = MkWriterT $ \w => m w <|> unWriterT mn w

public export %inline
Monad m => Monad (WriterT w m) where
  m >>= k = MkWriterT $ \w => do (a,w1) <- unWriterT m w
                                 unWriterT (k a) w1

public export %inline
MonadTrans (WriterT w) where
  lift m = MkWriterT $ \w => map (\a => (a,w)) m

public export %inline
HasIO m => HasIO (WriterT w m) where
  liftIO = lift . liftIO


text:
module Compiler.Generated

import Idris.Version

export
generatedString : String -> String
generatedString backend =
  "@" ++ "generated by Idris " ++ (show version) ++ ", " ++ backend ++ " backend"


text:
module Compo2

import Incrementer
import Twicer
import Halfer

%default total

-- Realized (incrementer . twicer . halfer).
rlz_compo2_attrs : RealizedAttributes
rlz_compo2_attrs = MkRealizedAttributes (MkCosts 600 60 6) 0.8
-- The following does not work because 601 ≠ 300+200+100
-- rlz_compo2_attrs = MkRealizedAttributes (MkCosts 601 60 6) 0.8
rlz_compo2 : RealizedFunction (Int -> Int) Compo2.rlz_compo2_attrs
rlz_compo2 = (compose rlz_incrementer (compose rlz_twicer rlz_halfer))

max_stars_repo_name: nunet-io/ai-dsl

max_issues_repo_name: nunet-io/ai-dsl

max_forks_repo_name: nunet-io/ai-dsl