text:
import Control.ST
import Js.Dom
import Data.Vect

data TodoAction : Nat -> Type where
  TodoAdd : TodoAction n
  TodoChangeInputString : String -> TodoAction n
  TodoRemove : Fin n -> TodoAction n

record TodoState (n : Nat) where
  constructor MkTodoState
  todos : Vect n String
  inputString : String

removeTodo : Fin (S n) -> TodoState (S n) -> TodoState n
removeTodo i (MkTodoState tds inps) = MkTodoState (deleteAt i tds) inps

addTodo : TodoState n -> TodoState (S n)
addTodo (MkTodoState tds inps) = MkTodoState (inps :: tds) ""

Gui : Dom m => Nat -> Type
Gui {m} = DomRef {m} Nat TodoState TodoAction

vwTasks : Vect n String -> Html (TodoAction n)
vwTasks todos =
  let idxTodos = zip range todos
  in div [] (map renderTodo $ toList idxTodos)
  where
    renderTodo : (Fin n, String) -> Html (TodoAction n)
    renderTodo (idx, s) =
      div [] [button [onclick (TodoRemove idx)] "x", text s]

vw : (n:Nat) -> TodoState n -> Html (TodoAction n)
vw n st =
  div
    []
    [ form [] TodoAdd [input [onchange TodoChangeInputString, value $ inputString st]]
    , vwTasks $ todos st
    ]

total
lenAfterAction : (n : Nat) -> TodoAction n -> Nat
lenAfterAction n TodoAdd = S n
lenAfterAction (S n) (TodoRemove _) = n
lenAfterAction n (TodoChangeInputString _) = n

procAct : Dom m => (d:Var) -> (a:TodoAction n) -> ST m () [d ::: Gui {m} n :-> Gui {m} (lenAfterAction n a)]
procAct {n} d TodoAdd =
  domUpdateM d n (S n) addTodo
procAct {n=S k} d (TodoRemove i) =
  domUpdateM d (S k) k (removeTodo i)
procAct d (TodoChangeInputString s) =
  domUpdate d (record {inputString = s})

pageLoop : Dom m => (d:Var) -> ST m () [remove d (Gui {m} n)]
pageLoop d =
  do
    x <- getInput d
    procAct d x
    pageLoop d

page : Dom m => ST m () []
page =
  do
    d <- initBody [] vw 0 (MkTodoState [] "")
    pageLoop d

main : JS_IO ()
main = setASync_ $ run page

max_stars_repo_name: rbarreiro/idrisjs

max_issues_repo_name: prozacchiwawa/idrisjs

max_forks_repo_name: prozacchiwawa/idrisjs


text:
> module Tests.DecIn
> import TestFramework
> import Data.List
> import Data.List.DecIn
> %access export

Simple smoke test verifying that

> smokeDecIn : IO ()
> smokeDecIn = case (decIn (S Z) [1,2,3]) of
>                   Yes Here => putStrLn "smokeDecIn test passed"
>                   Yes (There x) => putStrLn "smokeDecIn returned There"
>                   No contra => putStrLn "smokeDecIn returned No"

ext: lidr

max_stars_repo_name: nicklecompte/idris-finite-sets

max_issues_repo_name: nicklecompte/idris-finite-sets

max_forks_repo_name: nicklecompte/idris-finite-sets


text:
{--
Copyright 2021 Joel Berkeley

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    http://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
--}
||| This module contains functionality for Gaussian process inference.
module Model.GaussianProcess

import Tensor
import Data
import Model
import Model.Kernel
import Model.MeanFunction
import Optimize
import Distribution

||| A Gaussian process is a collection of random variables, any finite number of which have joint
||| Gaussian distribution. It can be viewed as a function from a feature space to a joint Gaussian
||| distribution over a target space.
|||
||| @features The shape of the feature domain.
public export
data GaussianProcess : (0 features : Shape) -> Type where
  ||| Construct a `GaussianProcess` as a pair of mean function and kernel.
  MkGP : MeanFunction features -> Kernel features -> GaussianProcess features

posterior :
  GaussianProcess features
  -> Tensor [] Double
  -> {s : _} -> (Tensor ((S s) :: features) Double, Tensor [S s] Double)
  -> GaussianProcess features
posterior (MkGP prior_meanf prior_kernel) noise (x_train, y_train) =
  let l = cholesky (prior_kernel x_train x_train + diag {n=S s} noise)
      alpha = l.T \\ (l \\ y_train)

      posterior_meanf : MeanFunction features
      posterior_meanf x = prior_meanf x + (prior_kernel x x_train) @@ alpha

      posterior_kernel : Kernel features
      posterior_kernel x x' = prior_kernel x x' -
                              (l \\ (prior_kernel x_train x)).T @@ (l \\ (prior_kernel x_train x'))

   in MkGP posterior_meanf posterior_kernel

log_marginal_likelihood :
  GaussianProcess features
  -> Tensor [] Double
  -> {s : _} -> (Tensor ((S s) :: features) Double, Tensor [S s] Double)
  -> Tensor [] Double
log_marginal_likelihood (MkGP _ kernel) noise (x, y) =
  let l = cholesky (kernel x x + diag {n=S s} noise)
      alpha = l.T \\ (l \\ y)
      log2pi = log $ const $ 2.0 * pi
   in - y @@ alpha / const 2 - trace (log l) - (const $ cast (S s)) * log2pi / const 2

||| A trainable model implementing vanilla Gaussian process regression. That is, regression with a
||| Gaussian process as conjugate prior for homoscedastic Gaussian likelihoods. See the following
||| for details:
|||
||| Gaussian Processes for Machine Learning
||| Carl Edward Rasmussen and Christopher K. I. Williams
||| The MIT Press, 2006. ISBN 0-262-18253-X.
|||
||| or
|||
||| Pattern Recognition and Machine Learning, Christopher M. Bishop
public export
data ConjugateGPRegression : (0 features : Shape) -> Type where
  MkConjugateGPR : (Tensor [p] Double -> GaussianProcess features) -> Tensor [p] Double
                   -> Tensor [] Double -> ConjugateGPRegression features

||| Construct a probabilistic model for the latent target values.
export
predict_latent : ConjugateGPRegression features
  -> ProbabilisticModel features {marginal=Gaussian [1]}
predict_latent (MkConjugateGPR mk_gp gp_params _) x =
  let (MkGP meanf kernel) = mk_gp gp_params
    in MkGaussian (expand 1 $ meanf x) (expand 2 $ kernel x x)

||| Fit the Gaussian process and noise to the specified data.
export
fit : ConjugateGPRegression features
  -> (forall n . Tensor [n] Double -> Optimizer $ Tensor [n] Double)
  -> Dataset features [1]
  -> ConjugateGPRegression features
fit (MkConjugateGPR {p} mk_prior gp_params noise) optimizer (MkDataset x y) =
  let objective : Tensor [S p] Double -> Tensor [] Double
      objective params = let (noise, prior_params) = split 1 params
                          in log_marginal_likelihood (mk_prior prior_params)
                             (squeeze noise) (x, squeeze y)

      (noise, gp_params) := split 1 $ optimizer (concat (expand 0 noise) gp_params) objective

      mk_posterior : Tensor [p] Double -> GaussianProcess features
      mk_posterior params' = posterior (mk_prior params') (squeeze noise) (x, squeeze y)

    in MkConjugateGPR mk_posterior gp_params (squeeze noise)

ext: idr

max_stars_repo_name: joelberkeley/spidr

max_issues_repo_name: joelberkeley/spidr

max_forks_repo_name: joelberkeley/spidr


text:
||| Interface for fine grained console actions
module Termios

import Control.ST
import Control.ST.ImplicitCall

%access public export
%default total

||| The terminal mode being used
data TerminalMode =
    ||| The specific terminal mode being used here
    TUI

interface (Monad m, ConsoleIO m) => Termios (m : Type -> Type) where
    Status : (mode : TerminalMode) -> Type
    ||| Initializes the TUI mode
    initialize : ST m Var [add (Status TUI)]
    ||| Returns the console mode to the previous state
    cleanup : {terminal : Var} -> ST m () [remove terminal (Status TUI)]
    ||| Gets a single char without waiting for character return
    getCh : {terminal : Var} -> ST m Char [terminal ::: Status TUI]

max_stars_repo_name: zenntenn/Idris-Termios

max_issues_repo_name: zenntenn/Idris-Termios

max_forks_repo_name: zenntenn/Idris-Termios


text:
x : {default Integer 0 a : Type} -> (Num a, Neg a) => a
x = -1

y : Double
y = 1 + x

description : String
description = show x

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
-- Exercise 1
data Elem : a -> List a -> Type where
     Here : Elem x (x :: xs)
     There : Elem x xs -> Elem x (y :: xs)

-- Exercise 2
data Last : List a -> a -> Type where
     LastOne : Last [value] value
     LastCons : (prf : Last xs value) -> Last (x :: xs) value

lastNotNil : (value : a) -> Last [] x -> Void
lastNotNil _ LastOne impossible
lastNotNil _ (LastCons _) impossible

lastNotCons : (contra : Last (x :: xs) value -> Void) ->
              Last (y :: (x :: xs)) value -> Void
lastNotCons contra (LastCons prf) = contra prf

lastNotSingleton : (contra : (y = value) -> Void) -> Last [y] value -> Void
lastNotSingleton contra LastOne = contra Refl
lastNotSingleton _ (LastCons LastOne) impossible
lastNotSingleton _ (LastCons (LastCons _)) impossible

isLast : DecEq a => (xs : List a) -> (value : a) -> Dec (Last xs value)
isLast [] value = No (lastNotNil value)
isLast (y :: []) value = case decEq y value of
                              (Yes Refl) => Yes LastOne
                              (No contra) => No (lastNotSingleton contra)
isLast (y :: (x :: xs)) value = case isLast (x :: xs) value of
                                     (Yes prf) => Yes (LastCons prf)
                                     (No contra) => No (lastNotCons contra)


text:
module TyTTP

import public TyTTP.Core.Error
import public TyTTP.Core.Promise
import public TyTTP.Core.Request
import public TyTTP.Core.Response
import public TyTTP.Core.Routing
import public TyTTP.Core.Step
import public TyTTP.Core.Stream

max_stars_repo_name: kbertalan/tyttp

max_issues_repo_name: kbertalan/tyttp

max_forks_repo_name: kbertalan/tyttp


text:
module Main

pythag : Int -> List (Int, Int, Int)
pythag max = [(x, y, z) | z <- [1..max], y <- [1..z], x <- [1..y], x * x + y * y == z * z]

main : IO ()
main = printLn (pythag 100)

max_stars_repo_name: asandroq/idris-gambit

max_issues_repo_name: asandroq/idris-gambit

max_forks_repo_name: asandroq/idris-gambit


text:
module Data.Bytes.Strict

import public Data.Bytes.Strict.Internal
import public Data.Bytes.Strict.API


text:
{-
  Simple monadic parser module, based heavily on that by
  Graham Hutton.
-}

module IdrisWeb.Common.Parser

import Prelude
import Prelude.Monad
import Prelude.Applicative
import Prelude.List
import Builtins

%access public

infixr 5 |||

{-
The monad of parsers
--------------------
-}

data Parser a                 =  P (String -> Either String (a, String))

parse                         : Parser a -> String -> Either String (a, String)
parse (P p) inp               =  p inp

instance Functor Parser where
    -- fmap : (a -> b) -> f a -> f b
    -- fmap : (a -> b) -> Parser a -> Parser b
    -- Given a function (a -> b), and a parser a, make a parser b
    map f p = P (\inp => case parse p inp of
                                  (Left err) => Left err
                                  -- Apply f to the v that we got from parsing
                                  (Right (v, rest)) => Right ((f v), rest))

instance Applicative Parser where
    pure v      = P (\inp => Right (v, inp))
    -- Parse to get the function, then parse to get the first argument
    a <$> b = P (\inp => do (f, rest) <- parse a inp
                            (x, rest') <- parse b rest
                            pure ((f x), rest'))

instance Monad Parser where
--    pure v                  =  P (\inp => Right (v,inp))
    -- m a -> (a -> m b) -> m b
    p >>= f                   =  P (\inp => case parse p inp of
                                               (Left err)       => Left err
                                               (Right (v,rest)) => parse (f v) rest)

--mplus : Monad m => m a -> m a -> m a
mplus : Parser a -> Parser a -> Parser a
mplus p q                  =  P (\inp => case parse p inp of
                                       Left msg      => parse q inp
                                       Right (v,out) => Right(v,out))

{-
Basic parsers
-------------
-}

failure                       : String -> Parser a
failure msg                   = P (\inp => Left msg)

item                          : Parser Char
item                          =  P (\inp => case unpack inp of
                                               []      => Left "Error! Parsing empty list."
                                               (x::xs) => Right (x, pack xs))

{-
Choice
--------
---}

(|||)                         : Parser a -> Parser a -> Parser a
p ||| q                       =  p `mplus` q

--{-
--Derived primitives
---}

sat                           : (Char -> Bool) -> Parser Char
sat p                         = item >>= (\x => if p x then pure x else failure "failed")

oneof                         : List Char -> Parser Char
oneof xs                      = sat (\x => elem x xs)

digit                         : Parser Char
digit                         =  sat isDigit

lower                         : Parser Char
lower                         =  sat isLower

upper                         : Parser Char
upper                         =  sat isUpper

letter                        : Parser Char
letter                        =  sat isAlpha

alphanum                      : Parser Char
alphanum                      =  sat isAlphaNum

char                          : Char -> Parser Char
char x                        =  sat (== x)

helper                        : List Char -> Parser (List Char)
string                        : String -> Parser String
string s                      = do result <- helper (unpack s)
                                   pure (pack result)

helper []                     =  pure Prelude.List.Nil
helper (x::xs)                =  do char x
                                    string (cast xs)
                                    pure (x :: xs)

many                          : Parser a -> Parser (List a)
many1                         : Parser a -> Parser (List a)
many1 p                       = do v <- p
                                   vs <- many p
                                   pure $ Prelude.List.(::) v vs

bool : Parser Bool
bool = parseTrue ||| parseFalse
  where parseTrue : Parser Bool
        parseTrue  = do oneof ['T', 't']
                        string "rue"
                        pure True
        parseFalse = do oneof ['F', 'f']
                        string "alse"
                        pure False

many p                        =  many1 p `mplus` pure Prelude.List.Nil

ident                         : Parser String
ident                         =  do x  <- letter
                                    xs <- many1 alphanum
                                    pure (pack(x::xs))

nat                           : Parser Int
nat                           =  do xs <- many1 digit
                                    pure (cast (cast xs))

int                           : Parser Int
int                           =  neg ||| nat
  where neg : Parser Int
        neg = do char '-'
                 n <- nat
                 pure (-n)

space                         : Parser ()
space                         =  do many (sat isSpace)
                                    pure ()
--{-
--Ignoring spacing
---}

token                         : Parser a -> Parser a
token p                       =  do space
                                    v <- p
                                    space
                                    pure v

identifier                    : Parser String
identifier                    =  token ident

natural                       : Parser Int
natural                       =  token nat

integer                       : Parser Int
integer                       =  token int

symbol                        : String -> Parser String
symbol xs                     =  token (string xs)

strToken : Parser String
strToken = map pack (token (many1 alphanum))

--apply                           : Parser a -> String -> List (a,String)
--apply p                     = parse (space >>= (\_ => p))

--{-
-- Expressions
---}

factor                        : Parser Int
term                          : Parser Int
expr                          : Parser Int
expr                          =  do t <- term
                                    do symbol "+"
                                       e <- expr
                                       pure $ t + e
                                  `mplus` pure t

factor                        =  do symbol "("
                                    do e <- expr
                                       symbol ")"
                                       pure e
                                  `mplus` natural

term                          =  do f <- factor
                                    do symbol "*"
                                       t <- term
                                       pure (f * t)
                                  `mplus` pure f

eval                          : String -> Maybe Int
eval xs                       =  case (parse expr xs) of
                                     Right (n,rest) => if rest == "" then Just n else Nothing
                                     Left msg  => Nothing

max_stars_repo_name: idris-hackers/IdrisWeb

max_issues_repo_name: idris-hackers/IdrisWeb

max_forks_repo_name: idris-hackers/IdrisWeb


text:
import Data.List.Views
import Data.List.Views.Extra
import Data.Nat.Views

||| Returns maximum equal suffix of two input lists
-- idris2 cannot check inside pairs so totality check fails
-- equalSuffix : Eq a => List a -> List a -> List a
-- equalSuffix input1 input2 with (snocList input1, snocList input2)
--   equalSuffix (xs ++ [x]) (ys ++ [y]) | ((Snoc x xs xsrec), (Snoc y ys ysrec))
--     = if x == y then equalSuffix xs ys ++ [x] else []
--   equalSuffix _ _ | (Empty, _) = []
--   equalSuffix _ _ | (_, Empty) = []

||| Returns maximum equal suffix of two input lists
equalSuffix : Eq a => List a -> List a -> List a
equalSuffix input1 input2 with (snocList input1)
  equalSuffix [] _ | Empty = []
  equalSuffix (xs ++ [x]) input2 | (Snoc x xs rec) with (snocList input2)
    equalSuffix (xs ++ [x]) [] | (Snoc x xs rec) | Empty = []
    equalSuffix (xs ++ [x]) (ys ++ [y]) | (Snoc x xs rec) | (Snoc y ys z)
        = if x == y then equalSuffix xs ys ++ [x] else []

-- with recursion, but bug
-- equalSuffix : Eq a => List a -> List a -> List a
-- equalSuffix input1 input2 with (snocList input1)
--   equalSuffix [] _ | Empty = []
--   equalSuffix (xs ++ [x]) input2 | (Snoc x xs recxs) with (snocList input2)
--     equalSuffix (xs ++ [x]) [] | (Snoc x xs recxs) | Empty = []
--     equalSuffix (xs ++ [x]) (ys ++ [y]) | (Snoc x xs recxs) | (Snoc y ys recys)
--         = if x == y then (equalSuffix xs ys | recxs | recys) ++ [x] else []

||| Turns Nat into binary string (slow)
toBinary : Nat -> String
toBinary n with (halfRec n)
  toBinary 0 | HalfRecZ = ""
  toBinary (k + k) | (HalfRecEven k rec) = (toBinary k | rec) ++ "0"
  toBinary (S (k + k)) | (HalfRecOdd k rec) = (toBinary k | rec) ++ "1"

||| Returns True if a List is traversed the same forwards and backwards
palindrome : Eq a => List a -> Bool
palindrome input with (vList input)
  palindrome [] | VNil = True
  palindrome [x] | VOne = True
  palindrome (x :: (xs ++ [y])) | (VCons rec) =
    if x == y then (palindrome xs | rec) else False


text:
module Ch05.EvalLambdaCalculus

import Ch05.LambdaCalculus

%default total

-----------------------------------------------------------------------
-- Evaluating the "evil" lambda calculus, one parentheses at a time.
-----------------------------------------------------------------------

-- Remark: Defining the evaluation rules for the toy language of
-- arithmetic expressions was very straightforward (even though
-- implementing the evaluation function turned out to be quite
-- involved, since we needed to prove totality.)
--
-- However, for the lambda calculus it isn't because of the problem
-- of variable capture. The book only makes some vagues hand gestures
-- suggesting we work with "terms up to alpha-conversion" and then
-- proceeds to give a prescription of substitution that is only partially
-- defined on terms.
--
-- To give sense to this vague suggestion, we might be tempted to
-- introduce a parametrized type `AlphaConverts t1 t2` that
-- says when two terms can be derived from each other by alpha
-- conversion (renaming of bound variables). Of course, the operation
-- of alpha conversion is a special case of variable substitution so
-- it seems we get stuck in a vicious circle.
-- Supposing that we won't, we might then proceed to form something
-- like a quotient type by forcing the existence of a function
--
--     AlphaConverts t1 t2 -> (t1 = t2)
--
-- (e.g. using believe_me). But that would be serious messing with
-- the type checker, so I don't like it.
--
-- So, I think I proceed as follows:
-- Define substitution using mutual recursion between a partially defined
-- substitution operation and an alpha-conversion operation that converts any
-- term to a term accepted by the partially defined substitution function.

-- TODO: Fix the definition below.
data AlphaConverts : Term -> Term -> Type where
  RenameLambda : {x, y : Variable} ->
                 {t : Term} ->
                 Not (OccursFree x t) ->
                 Not (OccursFree y t) ->
                 AlphaConverts (Abs x t) (Abs y t)
  ConvertBody : AlphaConverts t t' ->
                AlphaConverts (Abs x t) (Abs x t')
  ConvertsFun : AlphaConverts f f' ->
                AlphaConverts (App f x) (App f' x)
  ConvertsArg : AlphaConverts x x' ->
                AlphaConverts (App f x) (App f x')

max_stars_repo_name: mr-infty/tapl

max_issues_repo_name: mr-infty/tapl

max_forks_repo_name: mr-infty/tapl


text:
||| State based wraper for the Ncurses C library
module Ncurses

import Control.ST

%lib C "ncurses"
%include C "Ncurses/ncurses_extra.h"
%link C "Ncurses/ncurses_extra.o"

%access public export
%default total

private
cBool : Bool -> Int
cBool True = 1
cBool False = 0

data NcursesStatus = NotInitialized | Initialized

data Window = WindowPtr Ptr

-- Commenting out the ones that I don't need yet, as Idris currently gets very slow if there are too many of these functions defined
interface Ncurses (m : Type -> Type) where
{
  Status : NcursesStatus -> Type
  ||| Outputs a string, without trailing newline
  putStr : Window -> (str : String) -> STrans m () xs (const xs)
  ||| Gets the most recent line entered
  getStr : Window -> STrans m String xs (const xs)
  ||| Outputs a string, with a trailing newline
  putStrLn : Window -> (str : String) -> STrans m () xs (const xs)
  ||| Outputs a single character
  putChar : Window -> (char : Char) -> STrans m () xs (const xs)
  ||| Gets the next character, after a newline
  -- getChar : Window -> STrans m Char xs (const xs)
  ||| Gets a single character, without waiting for a newline
  getCh : Window -> STrans m Char xs (const xs)
  -- lines : STrans m Int xs (const xs)
  -- cols : STrans m Int xs (const xs)
  initscr : STrans m Window xs (const xs)
  endwin : STrans m Int xs (const xs)
  -- refresh : Window -> STrans m Int xs (const xs)
  cbreak : STrans m Int xs (const xs)
  nocbreak : STrans m Int xs (const xs)
  echo : STrans m Int xs (const xs)
  noecho : STrans m Int xs (const xs)
  -- halfdelay : STrans m Int xs (const xs)
  -- intrflush : Window -> Bool -> STrans m Int xs (const xs)
  keypad : Window -> Bool -> STrans m Int xs (const xs)
  -- meta : Window -> Bool -> STrans m Int xs (const xs)
  -- nodelay : Window -> Bool -> STrans m Int xs (const xs)
  -- raw : STrans m Int xs (const xs)
  -- noraw : STrans m Int xs (const xs)
  -- noqiflush : STrans m Int xs (const xs)
  -- qiflush : STrans m Int xs (const xs)
  -- notimeout : Window -> Bool -> STrans m Int xs (const xs)
  -- timeout : Int -> STrans m () xs (const xs)
  -- wtimeout : Window -> Int -> STrans m () xs (const xs)
  -- typeahead : Nat -> STrans m Int xs (const xs)
  -- clearok : Window -> Bool -> STrans m Int xs (const xs)
  -- idlok : Window -> Bool -> STrans m Int xs (const xs)
  -- idcok : Window -> Bool -> STrans m Int xs (const xs)
  -- immedok : Window -> Bool -> STrans m Int xs (const xs)
  -- leaveok : Window -> Bool -> STrans m Int xs (const xs)
  -- setscrreg : (top : Int) -> (bottom : Int) -> STrans m Int xs (const xs)
  -- wsetscrreg : Window -> (top : Int) -> (bottom : Int) -> STrans m Int xs (const xs)
  -- scrollok : Window -> Bool -> STrans m Int xs (const xs)
  -- nl : STrans m Int xs (const xs)
  -- nonl : STrans m Int xs (const xs)
}

private total
intReturn : (str : String) -> Ncurses IO => STrans IO Int xs (const xs)
intReturn str = lift $ foreign FFI_C str (IO Int)

private total
windowBoolIntReturn : (str : String) -> Window -> Bool -> Ncurses IO => STrans IO Int xs (const xs)
windowBoolIntReturn str (WindowPtr p) a = lift $ foreign FFI_C str (Ptr -> Int -> IO Int) p (cBool a)

Ncurses IO where
{
  putStr (WindowPtr p) str = lift $ foreign FFI_C "wprintw" (Ptr -> String -> IO ()) p str
  putStrLn w str = putStr w (str ++ "\n")
  getStr (WindowPtr p) = lift $ foreign FFI_C "getStr" (Ptr -> IO String) p
  putChar (WindowPtr p) char = lift $ foreign FFI_C "putChar" (Ptr -> Char -> IO()) p char
  --getChar (WindowPtr p) = lift $ foreign FFI_C "getChar" (Ptr -> IO Char) p
  getCh (WindowPtr p) = lift $ foreign FFI_C "wgetch" (Ptr -> IO Char) p
  -- lines = intReturn "getLines"
  -- cols = intReturn "getCols"
  initscr = lift $ map WindowPtr $ foreign FFI_C "initscr" (IO Ptr)
  endwin = intReturn "endwin"
  -- refresh (WindowPtr p) = lift $ foreign FFI_C "wrefresh" (Ptr -> IO Int) p
  cbreak = intReturn "cbreak"
  nocbreak = intReturn "nocbreak"
  echo = intReturn "echo"
  noecho = intReturn "noecho"
  -- halfdelay = intReturn "halfdelay"
  -- intrflush w a = windowBoolIntReturn "intrflush" w a
  keypad w a = windowBoolIntReturn "keypad" w a
  -- meta w a = windowBoolIntReturn "meta" w a
  -- nodelay w a = windowBoolIntReturn "nodelay" w a
  -- raw = intReturn "raw"
  -- noraw = intReturn "noraw"
  -- noqiflush = intReturn "noqiflush"
  -- qiflush = intReturn "qiflush"
  -- notimeout w a = windowBoolIntReturn "notimeout" w a
  -- timeout k = lift $ foreign FFI_C "timeout" (Int -> IO ()) k
  -- wtimeout (WindowPtr p) k = lift $ foreign FFI_C "wtimeout" (Ptr -> Int -> IO ()) p k
  -- typeahead fileDescriptor = lift $ foreign FFI_C "typeahead" (Int -> IO Int) (toIntNat fileDescriptor)
  -- clearok w a = windowBoolIntReturn "clearok" w a
  -- idlok w a = windowBoolIntReturn "idlok" w a
  -- idcok w a = windowBoolIntReturn "idcok" w a
  -- immedok w a = windowBoolIntReturn "immedok" w a
  -- leaveok w a = windowBoolIntReturn "leaveok" w a
  -- setscrreg top bottom = lift $ foreign FFI_C "setscrreg" (Int -> Int -> IO Int) top bottom
  -- wsetscrreg (WindowPtr ptr) top bottom = lift $ foreign FFI_C "wsetscrreg" (Ptr -> Int -> Int -> IO Int) ptr top bottom
  -- scrollok w a = windowBoolIntReturn "scrollok" w a
  -- nl = intReturn "nl"
  -- nonl = intReturn "nonl"
}

{-
private
liftError : IO Int -> NcursesIO ()
liftError code = MkNcursesIO (map liftErr code) where
  liftErr code = if code == -1 then Left NullWindow else Right ()

runNcurses : (NcursesError -> IO b) -> (a -> IO b) -> NcursesIO a -> IO b
runNcurses f g nio = do
  e <- unliftIO nio
  case e of
    Left err => f err
    Right a => g a

ncursesMain : NcursesIO () -> IO ()
ncursesMain = runNcurses logError pure where
  logError NullWindow = putStrLn "NULL window"

-}

max_stars_repo_name: zenntenn/idris-curses

max_issues_repo_name: zenntenn/idris-curses

max_forks_repo_name: zenntenn/idris-curses


text:
module System.File.Extra

import System
import System.Info

-- TODO: interface with C functions for symlinks in POSIX & Windows environments.
--       for now, I'll skip the C library and just call out to system.
export
symlink : HasIO io => (from : String) -> (to : String) -> io Bool
symlink from to =
  [ res == 0 | res <- if isWindows
       then putStrLn "Unsupported (so far)" >> pure 1
       else system "ln -s \"\{from}\" \"\{to}\"" ]

max_stars_repo_name: memoryruins/idv

max_issues_repo_name: memoryruins/idv

max_forks_repo_name: memoryruins/idv


text:
module Vector

import DataTypes
import Control.ST
import Control.ST.Exception

%access public export

outOfBoundsError : String -> Integer -> List LispVal -> LispError
outOfBoundsError name index vec =
    Default $
        name ++
        ": index is out of range; " ++
        "index: " ++ show index ++ "; valid range: " ++ show (length vec)

isVector : PrimitiveLispFunc
isVector args = case args of
    [(LispVector n _)] => pure $ LispBool True
    [_] => pure $ LispBool False
    a => Left $ NumArgs (MinMax 1 1) (cast $ length args) a

vectorLength : PrimitiveLispFunc
vectorLength args = case args of
    [(LispVector n vec)] => pure $ LispInteger $ cast n
    [v] => Left $ TypeMismatch "Vector" v
    a => Left $ NumArgs (MinMax 1 1) (cast $ length args) a

vectorRef : PrimitiveLispFunc
vectorRef args =
  case args of
    [LispVector n vec, LispInteger m] =>
      case index' (fromIntegerNat m) vec of
        Just val => pure val
        Nothing => Left $ outOfBoundsError "vector-ref" m vec
    [v] => Left $ TypeMismatch "Vector" v
    a => Left $ NumArgs (MinMax 2 2) (cast $ length args) a

vectorPrimitives : List (String, PrimitiveLispFunc)
vectorPrimitives =
    [ ("vector?", isVector)
    , ("vector-length", vectorLength)
    , ("vector-ref", vectorRef)
    ]

max_stars_repo_name: ebenpack/lidrisp

max_issues_repo_name: ebenpack/lidrisp

max_forks_repo_name: ebenpack/lidrisp


text:
module Inigo.Async.Base

import Data.Maybe
import Inigo.Async.Promise
import Inigo.Async.Util
import Inigo.Paths

%foreign (promisifyPrim "()=>new Promise((resolve,reject)=>{})")
never__prim : promise ()

%foreign (promisifyPrim "(_,err)=>new Promise((resolve,reject)=>reject(err))")
reject__prim : String -> promise a

%foreign (promisifyResolve "null" "(text)=>console.log(text)")
log__prim : String -> promise ()

%foreign (promisifyPrim (toArray "(cmd,args,workDir,detached,verbose)=>new Promise((resolve,reject)=>{let opts={detached:detached===1, stdio: ['ignore', process.stdout, process.stderr],cwd:workDir};require('child_process').spawn(cmd, toArray(args), opts).on('close', (code) => resolve(code))})"))
system__prim : String -> List String -> String -> Int -> Int -> promise Int

%foreign (promisifyPrim (toArray "(cmd,args,detached,verbose)=>new Promise((resolve,reject)=>{let opts={detached:detached===1, stdio: 'inherit'};require('child_process').spawn(cmd, toArray(args), opts).on('close', (code) => resolve(code))})"))
systemWithStdIO__prim : String -> List String -> Int -> Int -> promise Int

export
never : Promise ()
never =
  promisify never__prim

export
reject : String -> Promise a
reject err =
  promisify (reject__prim err)

export
log : String -> Promise ()
log text =
  promisify (log__prim text)

export
debugLog : String -> Promise ()
debugLog text = when DEBUG $ log text

export
system : String -> List String -> Maybe String -> Bool -> Bool -> Promise Int
system cmd args cwd detached verbose =
  promisify (system__prim cmd args (fromMaybe "" cwd) (boolToInt detached) (boolToInt verbose))

export
systemWithStdIO : String -> List String -> Bool -> Bool -> Promise Int
systemWithStdIO cmd args detached verbose =
  promisify (systemWithStdIO__prim cmd args (boolToInt detached) (boolToInt verbose))

-- This is here and not in `Promise.idr` since it relies on `reject`
export
liftEither : Either String a -> Promise a
liftEither x =
  do
    let Right res = x
      | Left err => reject err
    pure res

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
module Intro
import Data.Vect

-- a term (object) with its type
three : Nat
three = 3

next: Nat -> Nat -- the type is a function type
next n = n + 1

-- a recursive definition
fct: Nat -> Nat
fct Z = 1
fct (S k) = (S k) * (fct k) -- this is primitive recursion

loop: Nat -> Nat
loop Z = Z
loop (S k) = loop k + (loop (k + 2)) -- this is horrible

fibPair: Nat -> (Nat, Nat)
fibPair Z = (1, 1)
fibPair (S k) = case fibPair k of
                     (a, b) => (b, a + b)

fibo: Nat -> Nat
fibo n = fst (fibPair n)

-- types are terms, i.e., first class, so have types
Naturals : Type
Naturals = Nat

natToNat : Type
natToNat = Nat -> Nat

anotherThree : Naturals
anotherThree = 3

add : Nat -> Nat -> Nat -- Curryed type
add m n = m + n

data BinTree : Type where
  Leaf : BinTree
  Node : (left: BinTree) -> (right: BinTree) -> BinTree

egTree: BinTree
egTree = Node (Node Leaf (Node Leaf Leaf)) Leaf

numberVertices : BinTree -> Nat
numberVertices Leaf = 1
numberVertices (Node left right) =
  (numberVertices left) + (numberVertices right) + 1

-- a parametrized type (generic)
data LTree : Type -> Type where
  LLeaf : (a: Type) -> (label: a) -> LTree a
  LNode : (a : Type) -> (left : LTree a) -> (right : LTree a) -> LTree a

egLTree : LTree Nat
egLTree =
  LNode Nat (
  LNode Nat (LLeaf Nat 1) (LNode Nat (LLeaf Nat 3) (LLeaf Nat 4))
  ) (LLeaf Nat 7)

labels : (a: Type) -> LTree a -> List a
labels a (LLeaf a label) = [label]
labels a (LNode a left right) =
  (labels a left) ++ (labels a right)

Tuple: Nat -> Type -- tuples of Natural numbers
Tuple Z = Unit
Tuple (S k) = (Nat, Tuple k)

egTuple : Tuple 2
egTuple = (3, (4, ()))

countdown : (n: Nat) -> Tuple n -- this is a dependent function
countdown Z = ()
countdown (S k) = (S k, countdown k)

cntd : (n: Nat) -> Vect (S n) Nat
cntd Z = [0]
cntd (S k) = (S k) :: (cntd k)

zipNat : (n: Nat) -> Vect n Nat -> Vect n Nat -> Vect n (Nat, Nat)
zipNat Z [] [] = []
zipNat (S len) (x :: xs) (y :: ys) = (x , y) :: (zipNat len xs ys)

zip : (n: Nat) -> (a: Type) -> (b: Type) -> Vect n a -> Vect n b -> Vect n (a, b)
zip Z a b [] [] = []
zip (S len) a b (x :: xs) (y :: ys) =
  (x, y) :: (zip len a b xs ys)

append: (n: Nat) -> (a: Type) -> (x: a) -> Vect n a -> Vect (S n) a
append Z a x [] = [x]
append (S len) a x (y :: xs) =
  y :: (append len a x xs)

filter: (n: Nat) -> (a: Type) -> (p: a -> Bool) -> Vect n a -> (m: Nat ** Vect m a)
filter Z a p [] = (Z ** [])
filter (S len) a p (x :: xs) =
  (case p x of
        False => filter len a p xs
        True => (case filter len a p xs of
                      (m ** pf) =>
                        (S m ** x :: pf) ))

data Nothing : Type where

vacuous : (a: Type) -> Nothing -> a

-- some space

max_stars_repo_name: siddhartha-gadgil/TrainLogic

max_issues_repo_name: siddhartha-gadgil/TrainLogic

max_forks_repo_name: siddhartha-gadgil/TrainLogic


text:
module Libgit.Remote

import Control.Monad.Managed

import Libgit.FFI
import Libgit.Types

withRemote : GitRepository -> String -> (GitResult GitRemote -> IO a) -> IO a
withRemote (MkGitRepository repoPtr) name act = do
  let cgr = git_lookup_remote repoPtr name
  (err, ptr) <- getGitResultPair cgr
  res <- act (MkGitRemote <$> toGitResult err ptr)
  primIO (prim_git_remote_free ptr)
  pure res

||| Lookup a repository remote by its name.
|||
||| Returns on success a managed reference to a Git remote
||| Returns on failure a Git error code.
|||
||| @repo The Git repository.
||| @name The string name of the remote.
export
remote : (repo : GitRepository)
      -> (name : String)
      -> Managed (GitResult GitRemote)
remote repo name = managed (withRemote repo name)

||| Download new data and update tips from a Git remote.
|||
||| Returns a Git error code.
|||
||| @remote The Git remote to fetch.
export
remoteFetch : (remote : GitRemote) -> IO Int
remoteFetch (MkGitRemote remote) = do
  let cgr = git_fetch_options_init
  (0, ptr) <- getGitResultPair cgr
    | (err, ptr) => pure err <* primIO (prim_free ptr)
  res <- primIO (prim_git_remote_fetch remote null_ptr ptr null_string)
  pure res <* primIO (prim_free ptr)

||| Download new data and update tips from a Git remote.
|||
||| Returns a Git error code.
|||
||| @remote The Git remote to fetch.
||| @reflogMessage The message to write in the reflog for this fetch.
export
remoteFetch' : (remote : GitRemote)
            -> (reflogMessage : String)
            -> IO Int
remoteFetch' (MkGitRemote remote) reflogMessage = do
  let cgr = git_fetch_options_init
  (0, ptr) <- getGitResultPair cgr
    | (err, ptr) => pure err <* primIO (prim_free ptr)
  res <- primIO (prim_git_remote_fetch remote null_ptr ptr (make_string reflogMessage))
  pure res <* primIO (prim_free ptr)

max_forks_repo_name: bigs/libgit-idris


text:
myReplace : forall p . (0 rule : x = y) -> (1 val : p y) -> p x
myReplace Refl prf = prf

bad : (0 x : Bool) -> Bool
bad False = True
bad True = False

data LT : Nat -> Nat -> Type where
     LeZ : LT Z (S k)
     LeS : LT j k -> LT (S j) (S k)

-- prf isn't used in the run time case tree, so erasure okay
minus : (x : Nat) -> (y : Nat) -> (0 prf : LT y x) -> Nat
minus (S k) Z LeZ = S k
minus (S k) (S j) (LeS p) = minus k j p

-- y is used in the run time case tree, so erasure not okay
minusBad : (x : Nat) -> (0 y : Nat) -> (0 prf : LT y x) -> Nat
minusBad (S k) Z LeZ = S k
minusBad (S k) (S j) (LeS p) = minusBad k j p

prf : {k : _} -> LT k (S (S k))
prf {k=Z} = LeZ
prf {k=S _} = LeS prf


text:
module TTUtils

import Prelude.Strings as S
import Language.Reflection.Utils
-- import Pruviloj.Core
-- import Pruviloj

%language ElabReflection

-- implementation Show TT where
--   show _ = "foo"

-- implementation Show x => Show (Binder x) where
--   show _ = "binder"

-- implementation Show x => Show (FunDefn x) where
--    show ttname = "TTname"

public export
record FnDesc where
  constructor MkFnDesc
  nameType : NameType
  fnType : TT
  fnDef : (FunDefn TT)

-- implementation Show FnDesc where
--   show fd =
--     "nameType: " ++ (show (nameType fd)) ++ "\n"
--     ++ "fnType: " ++ (show (fnType fd)) ++ "\n"
--     ++ "fnDef: " ++ (show (fnDef fd)) ++ "\n"

public export
getTTForFn : TTName -> Elab ()
getTTForFn n =
  do
    (_,nt,t) <- lookupTyExact n
    fnd <- lookupFunDefnExact n
    fill `(MkFnDesc ~(quote nt) ~(quote t) ~(quote fnd))
    --    fill `((~(quote nt)))
    solve

bar : Int -> Int
bar xxx = 42

bar2 : Nat -> Nat
bar2 xxx = S xxx

bar3 : Nat -> Nat
bar3 = \x => S x

bar4 : (n : Nat) -> Nat
bar4 = \x => S x

bar5 : Nat -> Nat
bar5 Z = Z
bar5 (S k) = k

foo' : FnDesc
foo' = %runElab (getTTForFn `{bar})

foo2 : FnDesc
foo2 = %runElab (getTTForFn `{bar2})

foo3 : FnDesc
foo3 = %runElab (getTTForFn `{bar3})

foo4 : FnDesc
foo4 = %runElab (getTTForFn `{bar4})

foo5 : FnDesc
foo5 = %runElab (getTTForFn `{bar5})


text:
interface Foo m where
  bar : k -> v -> m k v -> m k v

-- This is kind of meaningless, except it exposes a potential error where
-- (\s, t => List (s, t)) is substituted in as 'm' in 'm k v' and the ks
-- clash, so one has to be renamed.
Eq k => Foo (\s, t => List (s, t)) where
  bar x y z = ?bang


text:
module Network.Curl.Prim.Multi

-------------------------------------------------
-- Multi
-------------------------------------------------
-- curl_multi_add_handle
-- curl_multi_assign
-- curl_multi_cleanup
-- curl_multi_fdset
-- curl_multi_info_read
-- curl_multi_init
-- curl_multi_perform
-- curl_multi_remove_handle
-- curl_multi_setopt
-- curl_multi_socket_action
-- curl_multi_strerror
-- curl_multi_timeout
-- curl_multi_poll
-- curl_multi_wait
-- curl_multi_wakeup
-------------------------------------------------

-- import Network.Curl.Prim.Mem
import Network.Curl.Prim.Other

import Network.Curl.Types
-- import Derive.Enum

import Data.Buffer

import Language.Reflection
%language ElabReflection

-- curl_multi_init
%foreign "C:curl_multi_init,libcurl,curl/curl.h"
prim_curl_multi_init : PrimIO (Ptr HandlePtr)

export
curl_multi_init : HasIO io => io (Maybe (CurlHandle Multi))
curl_multi_init = do r <- primIO prim_curl_multi_init
                     pure $ if believe_me r == 0 then Nothing
                                                 else Just (MkH r)
-- curl_multi_cleanup
%foreign "C:curl_multi_cleanup,libcurl,curl/curl.h"
prim_curl_multi_cleanup : Ptr HandlePtr -> PrimIO ()

export
curl_multi_cleanup : HasIO io => CurlHandle Multi -> io ()
curl_multi_cleanup (MkH ptr) = primIO (prim_curl_multi_cleanup ptr)

{- curl_multi_socket_action
CURLMcode curl_multi_socket_action(CURLM * multi_handle,
                                   curl_socket_t sockfd,
                                   int ev_bitmask,
                                   int *running_handles);
-}
%foreign "C:curl_multi_socket_action,libcurl,curl/curl.h"
prim_curl_multi_socket_action : Ptr HandlePtr -> Int -> Int -> Ptr Int -> PrimIO (Ptr HandlePtr)

export
curl_multi_socket_action : HasIO io => CurlHandle Multi -> Int -> Int -> Ptr Int ->
curl_multi_socket_action = ?SDfsfd

-- curl_multi_info_read

%foreign "C:curl_multi_setopt,libcurl,curl/curl.h"
prim_curl_multi_setopt_long : Ptr HandlePtr -> Int -> Int -> PrimIO Int

%foreign "C:curl_multi_setopt,libcurl,curl/curl.h"
prim_curl_multi_setopt_objptr : Ptr HandlePtr -> Int -> AnyPtr -> PrimIO Int

%foreign "C:curl_multi_setopt,libcurl,curl/curl.h"
prim_curl_multi_setopt_off_t : Ptr HandlePtr -> Int -> Bits64 -> PrimIO Int

%foreign "C:curl_multi_setopt,libcurl,curl/curl.h"
prim_curl_multi_setopt_blob : Ptr HandlePtr -> Int -> Buffer -> PrimIO Int

-- mSetOptPrim is to fill the role of
{-
%foreign "C:curl_multi_setopt,libcurl,curl/curl.h"
prim_curl_multi_setopt : Ptr HandlePtr -> Int -> any -> PrimIO CurlECode
-}
-- We can't pass 'any' or an arbitrary Type to a foreign function, but we can
-- generate that function at the type we need.
-- e.g. mSetOptPrim CURLMOPT_SOCKETFUNCTION would generate and declare:
--   %foreign "C:curl_multi_setopt,libcurl,curl/curl.h"
--   setOptPrim_CURLMOPT_SOCKETFUNCTION : Ptr HandlePtr -> Int
--     -> (HandlePtr -> Int -> Int -> AnyPtr -> AnyPtr -> PrimIO Int)
--     -> PrimIO Int
-- Specializing `any` to `(HandlePtr -> Int -> Int -> AnyPtr -> AnyPtr -> PrimIO Int)`
-- in accordance with the type given by `paramType CURLMOPT_SOCKETFUNCTION`

-- mSetOptPrim then also inserts the name of the generated prim at the use-site.
-- Below in `curl_multi_setopt` we use let to give it a place to generate to and
-- then use it. It wasn't happy about being placed directly where `prim` is
-- used instead of with the let. Possibly this is a parsing issue wih %runElab
-- or my own misunderstanding.
-- I'd like to have this take IO instead of PrimIO so users don't have to write
-- toPrim but it's a fair bit more involved to massage the types since the ffi
-- expects PrimIO
%macro
mSetOptPrim : {opty : _} -> (opt : CurlMOption opty)
           -> Elab (Ptr HandlePtr -> Int -> paramType opt -> PrimIO Int)
mSetOptPrim opt = do
  let name = UN $ "setOptPrim_" ++ show opt
  z <- quote (paramType opt)
  str <- quote "C:curl_multi_setopt,libcurl,curl/curl.h"
  let ty = MkTy EmptyFC EmptyFC name `(Ptr HandlePtr -> Int -> ~z -> PrimIO Int)
  let claim = IClaim EmptyFC MW Private
                [ForeignFn [str]] ty
  declare [claim] -- generate prim
  check (IVar EmptyFC name) -- insert prim's name

-- hideous but we only need to define it once
export
total
curl_multi_setopt : HasIO io => CurlHandle Multi -> {ty : _}
                 -> (opt : CurlMOption ty) -> paramType opt -> io CurlMCode
curl_multi_setopt (MkH h) opt@CURLMOPT_SOCKETFUNCTION v = do
    let prim = mSetOptPrim opt
    pure (unsafeFromCode !(primIO $ prim h (toCode opt) v))
curl_multi_setopt (MkH h) opt@CURLMOPT_TIMERFUNCTION v = do
    let prim = mSetOptPrim opt
    pure (unsafeFromCode !(primIO $ prim h (toCode opt) v))
curl_multi_setopt (MkH h) opt@CURLMOPT_PUSHFUNCTION v = do
    let prim = mSetOptPrim opt
    pure (unsafeFromCode !(primIO $ prim h (toCode opt) v))
curl_multi_setopt (MkH h) opt@CURLMOPT_PIPELINING v = pure $ -- special, bitmask, TODO, determine if we care
    unsafeFromCode !(primIO $ prim_curl_multi_setopt_long h (toCode opt) v)
curl_multi_setopt {ty = CURLOPTTYPE_LONG} (MkH h) opt v = pure $
    unsafeFromCode !(primIO $ prim_curl_multi_setopt_long h (toCode opt) v)
curl_multi_setopt {ty = CURLOPTTYPE_OBJECTPOINT} (MkH h) opt v = pure $
    unsafeFromCode !(primIO $ prim_curl_multi_setopt_objptr h (toCode opt) v)
curl_multi_setopt {ty = CURLOPTTYPE_OFF_T} (MkH h) opt v = pure $
    unsafeFromCode !(primIO $ prim_curl_multi_setopt_off_t h (toCode opt) v)
curl_multi_setopt {ty = CURLOPTTYPE_BLOB} (MkH h) opt v = pure $
    unsafeFromCode !(primIO $ prim_curl_multi_setopt_blob h (toCode opt) v)
curl_multi_setopt {ty = UnusedOptType} _ _ _ = pure CURLM_UNKNOWN_OPTION
--                      ^can't happen during normal use

useoptest : IO ()
useoptest = do
  Just r <- curl_multi_init
    | _ => printLn "foo"
  CURLM_OK <- curl_multi_setopt r CURLMOPT_SOCKETFUNCTION $ \h,sock,info,dat,sdat => toPrim $ do
      pure 0
    | o => printLn o
  -- curl_multi_setopt r CURLMOPT_LASTENTRY ?this_accepts_only_void
  putStrLn "was set"
  curl_multi_cleanup r


text:
module BoundedNat

import Data.Fin
import Data.So

%default total

namespace MaybeResult

  atm : (xs : List a) -> (n : Nat) -> Maybe a
  atm []      _     = Nothing
  atm (x::_)  Z     = Just x
  atm (_::xs) (S n) = xs `atm` n

namespace SoLtParam

  ats : (xs : List a) -> (n : Nat) -> {auto ok : So (n `lt` length xs)} -> a
  ats (x::_)  Z          = x
  ats (_::xs) (S k) {ok} = xs `ats` k
  ats []      Z     impossible
  ats []      (S k) impossible

  x0s : Char
  x0s = ['1', '2', '3'] `ats` 0

  x2s : Char
  x2s = ['1', '2', '3'] `ats` 2

  --x3s : Char
  --x3s = ['1', '2', '3'] `ats` 3

namespace SoJustParam

  ltlt : So (n < k) -> So (n `lt` k)
  ltlt {n = Z} {k = Z} so = so
  ltlt {n = Z} {k = (S k)} so = so
  ltlt {n = (S j)} {k = Z} so = so
  ltlt {n = (S j)} {k = (S l)} _ with (choose (j < l))
    ltlt                         _ | Left subso = ltlt subso
    ltlt {n = (S j)} {k = (S l)} _ | Right sso with (compare j l)
      ltlt _ | Right sso | LT = absurd sso

  atss : (xs : List a) -> (n : Nat) -> {auto ok : So (n < length xs)} -> a
  atss xs n {ok} = SoLtParam.ats xs n {ok = ltlt ok}

  x0ss : Char
  x0ss = ['1', '2', '3'] `atss` 0

  x2ss : Char
  x2ss = ['1', '2', '3'] `atss` 2

  --x3ss : Char
  --x3ss = ['1', '2', '3'] `atss` 3

namespace LteParam

  atl : (xs : List a) -> (n : Nat) -> {auto ok : LT n (length xs)} -> a
  atl (x::_)  Z                        = x
  atl (_::xs) (S n) {ok = (LTESucc _)} = xs `atl` n

  x0l : Char
  x0l = ['1', '2', '3'] `atl` 0

  x2l : Char
  x2l = ['1', '2', '3'] `atl` 2

  --x3l : Char
  --x3l = ['1', '2', '3'] `atl` 3

namespace InBoundsParam

  ati : (xs : List a) -> (n : Nat) -> {auto ok : InBounds n xs} -> a
  ati (x::_)  Z                      = x
  ati (_::xs) (S k) {ok = InLater _} = xs `ati` k

  x0i : Char
  x0i = ['1', '2', '3'] `ati` 0

  x2i : Char
  x2i = ['1', '2', '3'] `ati` 2

  --x3i : Char
  --x3i = ['1', '2', '3'] `ati` 3

namespace CumstomWithLte

  data BoundedNat : Nat -> Type where
    MkBNat : (n : Nat) -> {auto ok : LT n b} -> BoundedNat b

  atb : (xs : List a) -> BoundedNat (length xs) -> a
  atb (x::_)  (MkBNat Z)                        = x
  atb (_::xs) (MkBNat (S n) {ok = (LTESucc _)}) = xs `atb` MkBNat n
  atb []      (MkBNat n) impossible

  x0b : Char
  x0b = ['1', '2', '3'] `atb` MkBNat 0

  x2b : Char
  x2b = ['1', '2', '3'] `atb` MkBNat 2

  --x3b : Char
  --x3b = ['1', '2', '3'] `atb` MkBNat 3

namespace FinParam

  atf : (xs : List a) -> Fin (length xs) -> a
  atf (x::_)  FZ     = x
  atf (_::xs) (FS n) = xs `atf` n

  x0f : Char
  x0f = ['1', '2', '3'] `atf` 0

  x2f : Char
  x2f = ['1', '2', '3'] `atf` 2

  --x3f : Char
  --x3f = ['1', '2', '3'] `atf` 3

max_stars_repo_name: buzden/code-in-lectures

max_issues_repo_name: buzden/code-in-lectures

max_forks_repo_name: buzden/code-in-lectures


text:
module FFI
import Data.HVect
import Data.Vect

%hide IO
%access public export

data UnsafeRaw;
data Boxed t = MkBoxed t

Unsafe : Type
Unsafe = Boxed UnsafeRaw

mutual

    data FList : Type -> Type where
        MockFList : (t: Type) -> FList t

    -- sized vector
    data FVect : Nat -> Type -> Type where
        MockFVect : (n: Nat) -> (t: Type) -> FVect n t

    -- Heterogeneous Vector.
    -- In many language, it's called `tuple`.
    data FHVect : Vect n Type -> Type where
        MockFHVect : (xs: Vect n Type) -> FHVect xs

    data CamTypes : Type -> Type where
        Cam_Unsafe   : CamTypes Unsafe

    data ForeignName
       = Builtin String
       | Library String String
       | BuiltinVar String
       | LibraryVar String String

    FFICam : FFI
    FFICam = MkFFI CamTypes ForeignName String

    public export
    IO : Type -> Type
    IO = IO' FFICam

FFun0 : Type
FFun0 = IO Unsafe

FFun1 : Type
FFun1 = Unsafe -> IO Unsafe

FFun2 : Type
FFun2 = Unsafe -> Unsafe -> IO Unsafe

FFun3 : Type
FFun3 = Unsafe -> Unsafe -> Unsafe -> IO Unsafe

||| call foreign language apis
%inline
fcall: (ty : Type) -> (fname : ForeignName) -> {auto fty : FTy FFICam [] ty} -> ty
fcall ty fname = foreign FFICam fname ty

%inline
fvar : String -> IO Unsafe
fvar n = fcall (IO Unsafe) (BuiltinVar n)

%inline
fcall0 : String -> IO Unsafe
fcall0 n = fcall FFun0 (Builtin n)

%inline
fcall1 : String -> Unsafe -> IO Unsafe
fcall1 n src = fcall FFun1 (Builtin n) src

%inline
fcall2 : String -> Unsafe ->  Unsafe -> IO Unsafe
fcall2 n src1 src2 = fcall FFun2 (Builtin n) src1 src2

%inline
fcall3 : String -> Unsafe ->  Unsafe -> Unsafe -> IO Unsafe
fcall3 n src1 src2 src3 = fcall FFun3 (Builtin n) src1 src2 src3

%inline
fassert: a -> b -> IO ()
fassert a b =
        let a = believe_me a in
        let b = believe_me b in
        believe_me $ fcall FFun2 (Builtin "cam-assert") a b

max_stars_repo_name: thautwarm/idris-cam

max_issues_repo_name: thautwarm/idris-cam

max_forks_repo_name: thautwarm/idris-cam


text:
module Pinball

import Effects
import Effect.SDL
import Effect.State
import Effect.StdIO
import Effect.Socket

||| The flipper state tracks the position of four flippers
record Flippers : Type where
  MkFlippers : (f1, f2, f3, f4 : Bool) -> Flippers

||| Convert a flipper record into the network representation
msg : Flippers -> String
msg (MkFlippers f1 f2 f3 f4) =
  strCons (prim__intToChar 0xff) .
  singleton . prim__intToChar . prim__zextB8_Int $
  (if f1 then 0x1 else 0) `prim__orB8`
  ((if f2 then 0x2 else 0) `prim__orB8`
   ((if f3 then 0x4 else 0) `prim__orB8`
    ((if f4 then 0x8 else 0) `prim__orB8` 0x10)))

||| Send the current LCD message over the network, prefixed with length
doMessage : { [ 'Message ::: STATE String, UDP Socket ] } Eff ()
doMessage = do text <- 'Message :- get
               send (IPv4Addr 192 168 43 119) 2811
                    (strCons (prim__intToChar $ cast (length text) ) text)
               return ()

||| Send the current flipper state over the network, prefixed with 0xff
doFlippers : { [ 'Flippers ::: STATE Flippers, UDP Socket ] } Eff ()
doFlippers = do send (IPv4Addr 192 168 43 119) 2811 (msg !('Flippers :- get))
                return ()

||| Handle a keypress, updating internal state and sending messages
keys : Maybe Event ->
       { [ SDL_ON
         , 'Flippers ::: STATE Flippers
         , 'Message ::: STATE String
         , UDP Socket
         ] } Eff Bool
keys (Just AppQuit) = return False
keys (Just (KeyDown (KeyAny 'a'))) = do 'Flippers :- update (record { f1 = True })
                                        doFlippers
                                        return True
keys (Just (KeyUp (KeyAny 'a'))) = do 'Flippers :- update (record { f1 = False})
                                      doFlippers
                                      return True
keys (Just (KeyDown (KeyAny 's'))) = do 'Flippers :- update (record { f2 = True })
                                        doFlippers
                                        return True
keys (Just (KeyUp (KeyAny 's'))) = do 'Flippers :- update (record { f2 = False})
                                      doFlippers
                                      return True
keys (Just (KeyDown (KeyAny 'k'))) = do 'Flippers :- update (record { f3 = True })
                                        doFlippers
                                        return True
keys (Just (KeyUp (KeyAny 'k'))) = do 'Flippers :- update (record { f3 = False})
                                      doFlippers
                                      return True
keys (Just (KeyDown (KeyAny 'l'))) = do 'Flippers :- update (record { f4 = True })
                                        doFlippers
                                        return True
keys (Just (KeyUp (KeyAny 'l'))) = do 'Flippers :- update (record { f4 = False})
                                      doFlippers
                                      return True
keys (Just (KeyDown KeySpace)) = do 'Message :- put "Space down"
                                    doMessage
                                    return True
keys (Just (KeyUp KeySpace)) = do 'Message :- put "Space up"
                                  doMessage
                                  return True
keys _ = return True

||| Draw key indicators for the pressed flipper buttons
draw : { [ SDL_ON, 'Flippers ::: STATE Flippers ] } Eff ()
draw = with Effects do
         MkFlippers a b c d <- 'Flippers :- get
         ellipse (colour a) 40 40 10 10
         ellipse (colour b) 80 40 10 10
         ellipse (colour c) 120 40 10 10
         ellipse (colour d) 160 40 10 10
   where colour : Bool -> Colour
         colour True = green
         colour False = white

||| The actual main function
main' : { [ SDL ()
          , 'Flippers ::: STATE Flippers
          , 'Message ::: STATE String
          , STDIO
          , UDP ()
          ] } Eff ()
main' = do putStrLn "Starting"
           case !mksocket of
             Left err => putStrLn "No connect"
             Right () => do initialise 600 100
                            loop
                            quit
                            close

  where
    loop : { [ SDL_ON
             , 'Flippers ::: STATE Flippers
             , 'Message ::: STATE String
             , STDIO
             , UDP Socket
             ] } Eff ()
    loop = do draw
              flip
              flippers <- 'Flippers :- get
              when !(keys !poll) loop

namespace Main
  ||| A stub to run `main'`.
  main : IO ()
  main = runInit [ ()
                 , 'Flippers := MkFlippers False False False False
                 , 'Message := "startup"
                 , ()
                 , ()
                 ] main'

max_stars_repo_name: GaloisInc/self-aware-pinball

max_issues_repo_name: GaloisInc/self-aware-pinball

max_forks_repo_name: GaloisInc/self-aware-pinball


text:
module Data.Time.Calendar.Types

%default total

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

public export Year : Type
Year = Integer

public export MonthOfYear : Type
MonthOfYear = Int

public export DayOfMonth : Type
DayOfMonth = Int

public export DayOfYear : Type
DayOfYear = Int

public export WeekOfYear : Type
WeekOfYear = Int

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


text:
module Data.Iso

public export
record Iso (a, b : Type) where
  constructor MkIso
  to : a -> b
  from : b -> a
  toFrom : (x : b) -> to (from x) === x
  fromTo : (x : a) -> from (to x) === x

-- TODO: transitive and reflexive for ISO

max_stars_repo_name: andrevidela/dev-notes

max_issues_repo_name: andrevidela/dev-notes

max_forks_repo_name: andrevidela/dev-notes


text:
module TypeTrans.HOF where

loop
loop cond action v

max_stars_repo_name: RossMeikleham/MSci-Project

max_issues_repo_name: RossMeikleham/MSci-Project

max_forks_repo_name: RossMeikleham/MSci-Project


text:
||| Unix file descriptor and lowlevel unbuffered IO.
|||
||| Copyright 2021, HATTORI, Hiroki
||| This file is released under the MIT license, see LICENSE for more detail.
|||
module System.IO.Handle.Unix

import Data.Buffer
import Data.String

import public System.IO.Handle.Types
import System.IO.Util.GetLine

%default total

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

export
data Handle : List Permission -> Type where
  MkHandle : {permission:List Permission} -> Int -> Handle permission

export stdin : Handle [Readable]
stdin = MkHandle 0

export stdout : Handle [Writable]
stdout = MkHandle 1

export stderr : Handle [Writable]
stderr = MkHandle 2

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

%foreign "C:read,libc 6"
         "node:lambda:(fd,b,n) => require('fs').readSync(Number(fd), b, 0, Number(n))"
prim__unix_read_buffer : (fd:Int) -> (dst:Buffer) -> (bytes:Int) -> PrimIO Int

%foreign "C:write,libc 6"
         "node:lambda:(fd,b,n) => require('fs').writeSync(fd, b, {length:n})"
prim__unix_write_buffer : Int -> Buffer -> Int -> PrimIO Int
%foreign "C:write,libc 6"
         "node:lambda:(fd,s,n) => require('fs').writeSync(Number(fd), s, {length:Number(n)})"
prim__unix_write_string : Int -> String -> Int -> PrimIO Int

%foreign "C:ioctl,libc 6"
         "node:lambda:(fd,k,b) => require('ioctl').ioctl((Number(fd), k, b)"
prim__unix_ioctl_ptr : Int -> Bits32 -> Buffer -> PrimIO Int

%foreign "C:close,libc 6"
         "node:lambda:(fd) => require('fs').close(Number(fd))"
prim_unix_close : (fd:Int) -> PrimIO Int

-- ---------------------------------------------------------------------------
-- Buffer IO

export hRead' : HasIO io => Handle ps -> {auto ok:elem Readable ps = True}
             -> Buffer {- -> (ofs:Int) -} -> io Int
hRead' (MkHandle fd) b = do
  n <- rawSize b
  primIO $ prim__unix_read_buffer fd b n

export hRead : HasIO io => Handle ps -> {auto ok:elem Readable ps = True}
            -> (maxbytes:Nat)
            -> io (Maybe (Int, Maybe Buffer))
hRead h maxbytes = do
  Just b <- newBuffer (cast maxbytes)
    | Nothing => pure $ Nothing
  r <- hRead' h b
  if r <= 0
     then do
       pure $ Just (r, Nothing)
     else do
       pure $ Just (r, Just b)

export hWrite : HasIO io => Handle ps -> {auto ok:elem Writable ps = True}
             -> Buffer -> (bytes:Nat) -> io Int
hWrite (MkHandle fd) b bytes = primIO $ prim__unix_write_buffer fd b (cast bytes)

-- ---------------------------------------------------------------------------
-- Char IO -- ofcourse very slow.

export hPutChar : HasIO io => Handle ps -> {auto ok:elem Writable ps = True}
               -> Char -> io Int
hPutChar (MkHandle fd) ch = do
  primIO $ prim__unix_write_string fd (singleton ch) 1

export hGetChar' : HasIO io => Handle ps -> {auto ok:elem Readable ps = True}
                -> io (Maybe (Either Int Char))
hGetChar' h = do
  Just (n, Just b) <- hRead h 1
    | Nothing => pure Nothing
    | Just (n, Nothing) => pure $ Just $ Left n
  ch <- getByte b 0
  pure $ Just $ Right $ cast{to=Char} ch

export hGetChar : HasIO io => Handle ps -> {auto ok:elem Readable ps = True}
               -> io (Maybe Char)
hGetChar h = do
  Just (Right ch) <- hGetChar' h
    | Nothing => pure Nothing
    | Just (Left _) => pure Nothing
  pure $ Just ch

-- ---------------------------------------------------------------------------
-- String IO

export hPutStr : HasIO io => Handle ps -> {auto ok:elem Writable ps = True}
              -> String -> io Int
hPutStr (MkHandle fd) str = do
  let n = cast $ length str
  primIO $ prim__unix_write_string fd str n

export hPutStrLn : HasIO io => Handle ps -> {auto ok:elem Writable ps = True}
               -> String -> io Int
hPutStrLn h str = hPutStr h $ str ++ "\n"

export hGetLine : HasIO io => Handle ps -> {auto ok:elem Readable ps = True}
               -> io (Maybe String)
hGetLine h = mkGetLine (hGetChar h) 4096

-- ---------------------------------------------------------------------------
-- open/close

export hClose : HasIO io => Handle ps -> io Int
hClose (MkHandle fd) = primIO $ prim_unix_close fd

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


text:
module Erlang.Data.Buffer

import Erlang
import public Erlang.System.File

%default total

BufferPayload : Type
BufferPayload = ErlTuple2 String Int

%extern prim__erlBufferNew       : (size : Int) -> BufferPayload
%extern prim__erlBufferResize    : (buf : BufferPayload) -> (newSize : Int) -> BufferPayload
%extern prim__erlBufferFlatten   : (buf : BufferPayload) -> (maxbytes : Int) -> BufferPayload
%extern prim__erlBufferSetByte   : (buf : BufferPayload) -> (loc : Int) -> (value : Int) -> BufferPayload
%extern prim__erlBufferGetByte   : (buf : BufferPayload) -> (loc : Int) -> Int
%extern prim__erlBufferSetBits8  : (buf : BufferPayload) -> (loc : Int) -> (value : Bits8) -> BufferPayload
%extern prim__erlBufferGetBits8  : (buf : BufferPayload) -> (loc : Int) -> Bits8
%extern prim__erlBufferSetBits16 : (buf : BufferPayload) -> (loc : Int) -> (value : Bits16) -> BufferPayload
%extern prim__erlBufferGetBits16 : (buf : BufferPayload) -> (loc : Int) -> Bits16
%extern prim__erlBufferSetBits32 : (buf : BufferPayload) -> (loc : Int) -> (value : Bits32) -> BufferPayload
%extern prim__erlBufferGetBits32 : (buf : BufferPayload) -> (loc : Int) -> Bits32
%extern prim__erlBufferSetBits64 : (buf : BufferPayload) -> (loc : Int) -> (value : Bits64) -> BufferPayload
%extern prim__erlBufferGetBits64 : (buf : BufferPayload) -> (loc : Int) -> Bits64
%extern prim__erlBufferSetInt32  : (buf : BufferPayload) -> (loc : Int) -> (value : Int) -> BufferPayload
%extern prim__erlBufferGetInt32  : (buf : BufferPayload) -> (loc : Int) -> Int
%extern prim__erlBufferSetInt64  : (buf : BufferPayload) -> (loc : Int) -> (value : Int) -> BufferPayload
%extern prim__erlBufferGetInt64  : (buf : BufferPayload) -> (loc : Int) -> Int
%extern prim__erlBufferSetDouble : (buf : BufferPayload) -> (loc : Int) -> (value : Double) -> BufferPayload
%extern prim__erlBufferGetDouble : (buf : BufferPayload) -> (loc : Int) -> Double
%extern prim__erlBufferSetString : (buf : BufferPayload) -> (loc : Int) -> (value : String) -> BufferPayload
%extern prim__erlBufferGetString : (buf : BufferPayload) -> (loc : Int) -> (len : Int) -> String

export
data Buffer : Type where
  MkBuffer : ErlReference -> Buffer

%inline
getBufferPayload : HasIO io => Buffer -> io BufferPayload
getBufferPayload (MkBuffer ref) =
  pure $ erlUnsafeCall BufferPayload "erlang" "get" [ref]

%inline
setBufferPayload : HasIO io => Buffer -> BufferPayload -> io ()
setBufferPayload (MkBuffer ref) content = do
  pure $ erlUnsafeCall ErlTerm "erlang" "put" [ref, content]
  pure ()

%inline
updateBufferPayload : HasIO io => Buffer -> (BufferPayload -> BufferPayload) -> io ()
updateBufferPayload buf updateFn = do
  old <- getBufferPayload buf
  setBufferPayload buf (updateFn old)

export
newBuffer : HasIO io => Int -> io (Maybe Buffer)
newBuffer size = do
  ref <- pure $ erlUnsafeCall ErlReference "erlang" "make_ref" []
  let payload = prim__erlBufferNew size
  let buf = MkBuffer ref
  setBufferPayload buf payload
  pure $ Just buf

-- might be needed if we do this in C...
export
freeBuffer : HasIO io => Buffer -> io ()
freeBuffer buf = pure ()

export
rawSize : HasIO io => Buffer -> io Int
rawSize buf = do
  MkTuple2 _ size <- getBufferPayload buf
  pure size

flatten : HasIO io => Buffer -> (maxbytes : Int) -> io ()
flatten buf maxbytes = do
  updateBufferPayload buf (\payload => prim__erlBufferFlatten payload maxbytes)

-- Assumes val is in the range 0-255
export
setByte : HasIO io => Buffer -> (loc : Int) -> (val : Int) -> io ()
setByte buf loc val = do
  updateBufferPayload buf (\payload => prim__erlBufferSetByte payload loc val)

export
getByte : HasIO io => Buffer -> (loc : Int) -> io Int
getByte buf loc = do
  payload <- getBufferPayload buf
  pure $ prim__erlBufferGetByte payload loc

export
setBits8 : HasIO io => Buffer -> (loc : Int) -> (val : Bits8) -> io ()
setBits8 buf loc val = do
  updateBufferPayload buf (\payload => prim__erlBufferSetBits8 payload loc val)

export
getBits8 : HasIO io => Buffer -> (loc : Int) -> io Bits8
getBits8 buf loc = do
  payload <- getBufferPayload buf
  pure $ prim__erlBufferGetBits8 payload loc

export
setBits16 : HasIO io => Buffer -> (loc : Int) -> (val : Bits16) -> io ()
setBits16 buf loc val = do
  updateBufferPayload buf (\payload => prim__erlBufferSetBits16 payload loc val)

export
getBits16 : HasIO io => Buffer -> (loc : Int) -> io Bits16
getBits16 buf loc = do
  payload <- getBufferPayload buf
  pure $ prim__erlBufferGetBits16 payload loc

export
setBits32 : HasIO io => Buffer -> (loc : Int) -> (val : Bits32) -> io ()
setBits32 buf loc val = do
  updateBufferPayload buf (\payload => prim__erlBufferSetBits32 payload loc val)

export
getBits32 : HasIO io => Buffer -> (loc : Int) -> io Bits32
getBits32 buf loc = do
  payload <- getBufferPayload buf
  pure $ prim__erlBufferGetBits32 payload loc

export
setBits64 : HasIO io => Buffer -> (loc : Int) -> (val : Bits64) -> io ()
setBits64 buf loc val = do
  updateBufferPayload buf (\payload => prim__erlBufferSetBits64 payload loc val)

export
getBits64 : HasIO io => Buffer -> (loc : Int) -> io Bits64
getBits64 buf loc = do
  payload <- getBufferPayload buf
  pure $ prim__erlBufferGetBits64 payload loc

export
setInt32 : HasIO io => Buffer -> (loc : Int) -> (val : Int) -> io ()
setInt32 buf loc val = do
  updateBufferPayload buf (\payload => prim__erlBufferSetInt32 payload loc val)

export
getInt32 : HasIO io => Buffer -> (loc : Int) -> io Int
getInt32 buf loc = do
  payload <- getBufferPayload buf
  pure $ prim__erlBufferGetInt32 payload loc

export
setInt : HasIO io => Buffer -> (loc : Int) -> (val : Int) -> io ()
setInt buf loc val = do
  updateBufferPayload buf (\payload => prim__erlBufferSetInt64 payload loc val)

export
getInt : HasIO io => Buffer -> (loc : Int) -> io Int
getInt buf loc = do
  payload <- getBufferPayload buf
  pure $ prim__erlBufferGetInt64 payload loc

export
setDouble : HasIO io => Buffer -> (loc : Int) -> (val : Double) -> io ()
setDouble buf loc val = do
  updateBufferPayload buf (\payload => prim__erlBufferSetDouble payload loc val)

export
getDouble : HasIO io => Buffer -> (loc : Int) -> io Double
getDouble buf loc = do
  payload <- getBufferPayload buf
  pure $ prim__erlBufferGetDouble payload loc

export
stringByteLength : String -> Int
stringByteLength str =
  erlUnsafeCall Int "erlang" "byte_size" [str]

export
setString : HasIO io => Buffer -> (loc : Int) -> (val : String) -> io ()
setString buf loc val = do
  updateBufferPayload buf (\payload => prim__erlBufferSetString payload loc val)

export
getString : HasIO io => Buffer -> (loc : Int) -> (len : Int) -> io String
getString buf loc len = do
  payload <- getBufferPayload buf
  pure $ prim__erlBufferGetString payload loc len

export covering
bufferData : HasIO io => Buffer -> io (List Int)
bufferData buf = do
  len <- rawSize buf
  unpackTo [] len
  where
    covering
    unpackTo : List Int -> Int -> io (List Int)
    unpackTo acc 0 = pure acc
    unpackTo acc loc = do
      val <- getByte buf (loc - 1)
      unpackTo (val :: acc) (loc - 1)

export
copyData : HasIO io => (src : Buffer) -> (start, len : Int) -> (dest : Buffer) -> (loc : Int) -> io ()
copyData src start len dest loc = do
  srcBinary <- getString src start len
  setString dest loc srcBinary

-- Create a new buffer by reading all the contents from the given file
-- Fails if no bytes can be read or buffer can't be created
export
createBufferFromFile : HasIO io => (filePath : String) -> io (Either FileError Buffer)
createBufferFromFile filePath = do
  result <- pure $ erlUnsafeCall ErlTerm "file" "read_file" [filePath]
  let Right str = erlDecode (okTuple string) result
    | _ => pure (Left FileReadError)
  let strSize = erlUnsafeCall Int "erlang" "byte_size" [str]
  ref <- pure $ erlUnsafeCall ErlReference "erlang" "make_ref" []
  pure $ erlUnsafeCall ErlTerm "erlang" "put" [ref, MkTuple2 str strSize]
  pure (Right (MkBuffer ref))

-- TODO: `maxbytes` is unused
export
writeBufferToFile : HasIO io => (filePath : String) -> Buffer -> (maxbytes : Int) -> io (Either FileError ())
writeBufferToFile filePath buf maxbytes = do
  flatten buf maxbytes
  MkTuple2 binary _ <- getBufferPayload buf
  result <- pure $ erlUnsafeCall ErlTerm "file" "write_file" [filePath, binary]
  pure $ erlDecodeDef (Left FileWriteError) (exact (MkAtom "ok") *> pure (Right ())) result

export
resizeBuffer : HasIO io => Buffer -> Int -> io (Maybe Buffer)
resizeBuffer buf newSize = do
  updateBufferPayload buf (\payload => prim__erlBufferResize payload newSize)
  pure $ Just buf


text:
module Test.Transducers.Examples

import Control.Monad.State
import Transducers
import Test.Transducers.Utils

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

sumLength : StatelessStep Int String
sumLength totalLength str = totalLength + fromNat (length str)

test_sumLength : Test
test_sumLength =
  assertEq 10 (foldl sumLength 0 ["abc", "de", "", "fghij"])

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

sumLengthOfEveryOddStrings : Step Bool Int String
sumLengthOfEveryOddStrings totalLength str = do
  doSum <- get
  modify not
  pure $ if doSum
    then Continue (sumLength totalLength str)
    else Continue (totalLength)

test_sumLengthOfEveryOddStrings : Test
test_sumLengthOfEveryOddStrings = do
  assertEq 6 $
    reduce (MkReducer True sumLengthOfEveryOddStrings (const id)) 0 ["abc", "de", "", "fg", "hij"]

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

sumLengthUntil : Int -> Step () Int String
sumLengthUntil maxValue totalLength str =
  pure $ if totalLength <= maxValue
    then Continue (sumLength totalLength str)
    else Done totalLength

test_sumLengthUntil : Test
test_sumLengthUntil = do
  assertEq 7 $
    reduce (MkReducer () (sumLengthUntil 5) (const id)) 0 ["abc", "de", "", "fg", "hij"]

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

sumSquaresOfOdds : List Int -> Int
sumSquaresOfOdds = transduce (filtering odd . mapping (\x => x * x)) (+) 0

test_sumSquaresOfOdds : Test
test_sumSquaresOfOdds =
  assertEq (1 + 9 + 25 + 49 + 81) $ sumSquaresOfOdds [1..10]

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

unwordSmallNames : Nat -> List String -> String
unwordSmallNames maxLength strings =
  transduce (filtering smallStrings . interspersing " ") (++) "" strings
  where smallStrings s = length s <= maxLength

test_unwordSmallNames : Test
test_unwordSmallNames =
  assertEq "a bbbb ddd e" $ unwordSmallNames 4 (words "a bbbb ccccc ddd e")

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

startsWith : Char -> String -> Bool
startsWith c str =
  if length str == 0 then False else strHead str == c

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

export
run_tests : IO ()
run_tests =
  runTestSuite [
    test_sumSquaresOfOdds,
    test_unwordSmallNames,
    test_sumLength,
    test_sumLengthOfEveryOddStrings]

max_stars_repo_name: QuentinDuval/IdrisReducers

max_issues_repo_name: QuentinDuval/IdrisReducers

max_forks_repo_name: QuentinDuval/IdrisReducers