text:
module Extra.OpenSSL.EVP.Digest

import Control.Linear.LIO
import Extra.C.CPtr
import Extra.C.Ptr
import Extra.OpenSSL.FFI
import Extra.OpenSSL.OBJ

export
data PRIM__EVP_MD : Type where

export
data PRIM__EVP_MD_CTX : Type where

export
data PRIM__ENGINE : Type where

%foreign libcrypto "EVP_sha224"
export
prim__EVP_sha224 : PrimIO (Ptr PRIM__EVP_MD)

%foreign libcrypto "EVP_sha256"
export
prim__EVP_sha256 : PrimIO (Ptr PRIM__EVP_MD)

%foreign libcrypto "EVP_sha384"
export
prim__EVP_sha384 : PrimIO (Ptr PRIM__EVP_MD)

%foreign libcrypto "EVP_sha512"
export
prim__EVP_sha512 : PrimIO (Ptr PRIM__EVP_MD)

%foreign libcrypto "EVP_MD_type"
export
prim__EVP_MD_type : Ptr PRIM__EVP_MD -> PrimIO CInt

%foreign libcrypto "EVP_get_digestbyname"
export
prim__EVP_get_digestbyname : CString -> PrimIO (Ptr PRIM__EVP_MD)

%foreign libcrypto "EVP_MD_CTX_new"
prim__EVP_MD_CTX_new : PrimIO (Ptr PRIM__EVP_MD_CTX)

%foreign libcrypto "EVP_MD_CTX_free"
prim__EVP_MD_CTX_free : Ptr PRIM__EVP_MD_CTX -> PrimIO ()

%foreign libcrypto "EVP_MD_CTX_reset"
prim__EVP_MD_CTX_reset : Ptr PRIM__EVP_MD_CTX -> PrimIO CInt

%foreign libcrypto "EVP_Digest"
export
prim__EVP_Digest : (data_ptr : Ptr CUChar) -> (data_count : SizeT) -> (digest_ret_ptr : Ptr CUChar) -> (digest_size_ret_ptr : Ptr CUInt) -> Ptr PRIM__EVP_MD -> Ptr PRIM__ENGINE -> PrimIO CUInt

%foreign libcrypto "EVP_DigestInit"
export
prim__EVP_DigestInit : Ptr PRIM__EVP_MD_CTX -> Ptr PRIM__EVP_MD -> PrimIO CInt

%foreign libcrypto "EVP_DigestInit_ex"
export
prim__EVP_DigestInit_ex : Ptr PRIM__EVP_MD_CTX -> Ptr PRIM__EVP_MD -> Ptr PRIM__ENGINE -> PrimIO CInt

%foreign libcrypto "EVP_DigestUpdate"
export
prim__EVP_DigestUpdate : Ptr PRIM__EVP_MD_CTX -> Ptr CUChar -> SizeT -> PrimIO CInt

%foreign libcrypto "EVP_DigestFinal_ex"
export
prim__EVP_DigestFinal_ex : Ptr PRIM__EVP_MD_CTX -> Ptr CUChar -> Ptr CUInt -> PrimIO CInt

-- low level abstractions

public export
data HashAlgo : Type where
  Sha1 : HashAlgo
  Sha224 : HashAlgo
  Sha256 : HashAlgo
  Sha384 : HashAlgo
  Sha512 : HashAlgo
  Md4 : HashAlgo
  Md5 : HashAlgo
  -- UnknownAlgo : HashAlgo

public export
nidToHashAlgo : NID -> Maybe HashAlgo
nidToHashAlgo (MkNID 64)  = Just Sha1
nidToHashAlgo (MkNID 675) = Just Sha224
nidToHashAlgo (MkNID 672) = Just Sha256
nidToHashAlgo (MkNID 673) = Just Sha384
nidToHashAlgo (MkNID 674) = Just Sha512
nidToHashAlgo (MkNID 257) = Just Md4
nidToHashAlgo (MkNID 4) = Just Md5
nidToHashAlgo _ = Nothing

public export
hashAlgoDigestSize : HashAlgo -> Nat
hashAlgoDigestSize Sha1   = 20
hashAlgoDigestSize Sha224 = 28
hashAlgoDigestSize Sha256 = 32
hashAlgoDigestSize Sha384 = 48
hashAlgoDigestSize Sha512 = 64
hashAlgoDigestSize Md4    = 16
hashAlgoDigestSize Md5    = 16

export
data EVP_MD : HashAlgo -> Type where
  MkEVP_MD : Ptr PRIM__EVP_MD -> EVP_MD algo

export
data ENGINE : Type where
  MkENGINE : Ptr PRIM__ENGINE -> ENGINE

export
data EVP_MD_CTX_State : Type where
  EVP_MD_CTX_State_New : EVP_MD_CTX_State
  EVP_MD_CTX_State_Initialized : (algo : HashAlgo) -> EVP_MD_CTX_State
  EVP_MD_CTX_State_Finalized : EVP_MD_CTX_State
  EVP_MD_CTX_State_Freed : EVP_MD_CTX_State

export
data EVP_MD_CTX : EVP_MD_CTX_State -> Type where
  MkEVP_MD_CTX : Ptr PRIM__EVP_MD_CTX -> EVP_MD_CTX state

export
EVP_MD_CTX_new : LinearIO io => L io {use=1} (EVP_MD_CTX EVP_MD_CTX_State_New)
EVP_MD_CTX_new = do
  a <- liftIO1 $ primIO $ prim__EVP_MD_CTX_new
  pure1 $ MkEVP_MD_CTX a

public export
data CanFree_EVP_MD_CTX_State : EVP_MD_CTX_State -> Type where
  CanFree_EVP_MD_CTX_State_New : CanFree_EVP_MD_CTX_State EVP_MD_CTX_State_New
  CanFree_EVP_MD_CTX_State_Initialized : CanFree_EVP_MD_CTX_State (EVP_MD_CTX_State_Initialized _)
  CanFree_EVP_MD_CTX_State_Finalized : CanFree_EVP_MD_CTX_State EVP_MD_CTX_State_Finalized

public export
data CanReset_EVP_MD_CTX_State : EVP_MD_CTX_State -> Type where
  CanReset_EVP_MD_CTX_State_New : CanReset_EVP_MD_CTX_State EVP_MD_CTX_State_New
  CanReset_EVP_MD_CTX_State_Initialized : CanReset_EVP_MD_CTX_State (EVP_MD_CTX_State_Initialized _)
  CanReset_EVP_MD_CTX_State_Finalized : CanReset_EVP_MD_CTX_State EVP_MD_CTX_State_Finalized

public export
data CanInitialize_EVP_MD_CTX_State : EVP_MD_CTX_State -> Type where
  CanInitialize_EVP_MD_CTX_State_New : CanInitialize_EVP_MD_CTX_State EVP_MD_CTX_State_New
  CanInitialize_EVP_MD_CTX_State_Finalized : CanInitialize_EVP_MD_CTX_State EVP_MD_CTX_State_Finalized

export
EVP_MD_CTX_free : LinearIO io => (1 _ : EVP_MD_CTX state) -> {auto okay : CanFree_EVP_MD_CTX_State state} -> L io {use=1} (EVP_MD_CTX EVP_MD_CTX_State_Freed)
EVP_MD_CTX_free (MkEVP_MD_CTX ctx_ptr) = do
  liftIO1 $ primIO $ prim__EVP_MD_CTX_free ctx_ptr
  pure1 $ MkEVP_MD_CTX ctx_ptr

export
doneEVP_MD_CTX : LinearIO io => (1 _ : EVP_MD_CTX EVP_MD_CTX_State_Freed) -> L io ()
doneEVP_MD_CTX (MkEVP_MD_CTX ptr) = pure ()

export
EVP_MD_CTX_reset : LinearIO io => (1 _ : EVP_MD_CTX state) -> {auto okay : CanReset_EVP_MD_CTX_State state} -> L io {use=1} (EVP_MD_CTX EVP_MD_CTX_State_New)
EVP_MD_CTX_reset (MkEVP_MD_CTX ctx_ptr) = do
  _ <- liftIO1 $ primIO $ prim__EVP_MD_CTX_reset ctx_ptr
  pure1 $ MkEVP_MD_CTX ctx_ptr

export
defaultENGINE : ENGINE
defaultENGINE = MkENGINE nullptr

export
EVP_DigestInit_ex : LinearIO io => (1 _ : EVP_MD_CTX state) -> {auto okay : CanInitialize_EVP_MD_CTX_State state} -> EVP_MD algo -> ENGINE -> L io {use=1} (EVP_MD_CTX (EVP_MD_CTX_State_Initialized algo))
EVP_DigestInit_ex (MkEVP_MD_CTX ctx_ptr) (MkEVP_MD md_ptr) (MkENGINE engine_ptr) = do
  _ <- liftIO1 $ primIO $ prim__EVP_DigestInit_ex ctx_ptr md_ptr engine_ptr
  pure1 (MkEVP_MD_CTX ctx_ptr)

export
EVP_DigestUpdate
  : LinearIO io
  => (1 _ : EVP_MD_CTX (EVP_MD_CTX_State_Initialized algo))
  -> {length : Nat}
  -> (1 _ : CPtr (Bytes can_free True can_write length))
  -> L io {use=1} (LPair (EVP_MD_CTX (EVP_MD_CTX_State_Initialized algo)) (CPtr (Bytes can_free True can_write length)))
EVP_DigestUpdate (MkEVP_MD_CTX ctx_ptr) (MkCPtr data_ptr) = do
  let data_count = cast $ natToInteger length
  _ <- liftIO1 $ primIO $ prim__EVP_DigestUpdate ctx_ptr data_ptr data_count
  pure1 $ (MkEVP_MD_CTX ctx_ptr) # (MkCPtr data_ptr)

export
EVP_DigestFinal_ex
  : LinearIO io
  => (1 _ : EVP_MD_CTX (EVP_MD_CTX_State_Initialized algo))
  -> (1 digest_ret_ptr : CPtr (Bytes can_free can_read True (hashAlgoDigestSize algo)))
  -> L io {use=1} (LPair (EVP_MD_CTX EVP_MD_CTX_State_Finalized) (CPtr (Bytes can_free can_read True (hashAlgoDigestSize algo))))
EVP_DigestFinal_ex (MkEVP_MD_CTX ctx_ptr) (MkCPtr digest_ret_ptr) = do
  _ <- liftIO1 $ primIO $ prim__EVP_DigestFinal_ex ctx_ptr digest_ret_ptr nullptr
  pure1 $ (MkEVP_MD_CTX ctx_ptr) # (MkCPtr digest_ret_ptr)

public export
data ExDigestByName : Type where
  NotImplementedYet : ExDigestByName
  NotFound : ExDigestByName

export
Show ExDigestByName where
  show NotImplementedYet = "not implemented yet"
  show NotFound = "not found"

export
EVP_get_digestbyname
  : LinearIO io
  => (1 name : CPtr (NullTerminated can_free))
  -> L io {use=1} (Res Bool (\case
     False => Res ExDigestByName (\_ => CPtr (NullTerminated can_free))
     True  => Res (DPair HashAlgo EVP_MD) (\_ => CPtr (NullTerminated can_free))
   ))
EVP_get_digestbyname (MkCPtr name_ptr) = do
  md_ptr <- primIO $ prim__EVP_get_digestbyname name_ptr
  case md_ptr == nullptr of
    True => pure1 $ False # (NotFound # MkCPtr name_ptr)
    False => do
      id_ <- primIO $ prim__EVP_MD_type md_ptr
      printLn id_
      pure1 $ case nidToHashAlgo (MkNID id_) of
        Nothing => False # (NotImplementedYet # MkCPtr name_ptr)
        Just algo => True # ((algo ** MkEVP_MD md_ptr) # MkCPtr name_ptr)


text:
-- test that a new BC is empty

import System.Concurrency.BufferedChannel

main : IO ()
main = do bcRef <- makeBufferedChannel {a=Nat}
          (MkDPair bc recv) <- becomeReceiver NonBlocking bcRef
          Nothing <- recv bc
            | (Just _) => putStrLn "ERROR: Received something from the void."
          putStrLn "Success!"

ext: idr


text:
module Main

StringOrInt : Bool -> Type
StringOrInt x = case x of
                     True => Int
                     False => String

getStringOrInt : (x : Bool) -> StringOrInt x
getStringOrInt x = case x of
                        True => 42
                        False => "Forty two"

valToString : (x : Bool) -> StringOrInt x -> String
valToString x val = case x of
                         True => ?xtrueType
                         False=> val

main : IO ()
main = putStrLn "Hello, World!"

max_stars_repo_name: brunoflores/type-driven-with-idris

max_issues_repo_name: brunoflores/type-driven-with-idris

max_forks_repo_name: brunoflores/type-driven-with-idris


text:
module Main

myunwords : List String -> String
myunwords [] = ""
myunwords [x] = x
myunwords (x :: xs) = x ++ " " ++ myunwords xs

myunlines : List String -> String
myunlines [] = ""
myunlines [x] = x
myunlines (x :: xs) = x ++ "\n" ++ myunlines xs

main : IO ()
main = do
    let justAList = reverse ["hello", "world"]
    putStrLn $ myunwords justAList
    putStrLn $ show $ myunwords justAList
    putStrLn $ myunlines justAList
    putStrLn $ show $ myunlines justAList
    putStrLn $ show $ if True then [1..10] else [20,9..1]

max_stars_repo_name: ioanluca/real-world-idris

max_issues_repo_name: ioanluca/real-world-idris

max_forks_repo_name: ioanluca/real-world-idris


text:
> module NonNegRational.NonNegRational

> import Fraction.Fraction
> import Fraction.Normal

> %default total

> %access public export

> ||| Non negative rational numbers
> NonNegRational : Type
> NonNegRational = Subset Fraction Normal

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
> module NonNegDouble.Constants

> import Data.So

> import Double.Predicates
> import NonNegDouble.NonNegDouble

> %default total
> %access public export

> |||
> zero : NonNegDouble
> zero = Element 0.0 (MkLTE Oh)

> |||
> one : NonNegDouble
> one = Element 1.0 (MkLTE Oh)


text:
module Main

main : IO ()
main = do
  let x = 1
  let y = 2
  print $ x + y

max_stars_repo_name: andorp/IdrisExtSTGCodegen

max_issues_repo_name: andorp/IdrisExtSTGCodegen

max_forks_repo_name: andorp/IdrisExtSTGCodegen


text:
module Cordial.Model.Common.Name

%default total
%access public export

data NameKind = WHOLE | INDEXED | ANY

data Name : (kind : NameKind) -> (type : Type) -> Type where
  WName : List String -> type -> Name WHOLE type
  IName : List String -> type -> Nat -> Name INDEXED type
  NoName : Name ANY type

max_stars_repo_name: border-patrol/cordial

max_issues_repo_name: border-patrol/cordial

max_forks_repo_name: border-patrol/cordial


text:
module Stack

%access export
%default total

-- | *Stack
data Stack : Nat -> Type -> Type where
     Nil : Stack Z a
     Cons : (x : a) -> (xs : Stack k a) -> Stack (S k) a

%name Stack stack
-- .end

-- | *empty
empty : Stack Z a
empty = Nil
-- .end

-- | *head
head : Stack (S k) a -> a
head (Cons x _xs) = x
-- .end

-- | *tail
tail : Stack (S k) a -> Stack k a
tail (Cons _x xs) = xs
-- .end

-- | *cons
cons : a -> Stack k a -> Stack (S k) a
cons x Nil = Cons x Nil
cons x (Cons y xs) = Cons x (Cons y xs)
-- .end

-- | *reverse
reverse : Stack n a -> Stack n a
reverse {n} stack = go empty stack
  where
    go : (acc : Stack k a) -> (curr : Stack j a) -> Stack (k + j) a
    go {k} acc [] = rewrite plusZeroRightNeutral k in acc
    go {k} {j = S j'} acc (Cons x xs) =
       rewrite sym $ plusSuccRightSucc k j' in go (cons x acc) xs
-- .end

max_stars_repo_name: nomicflux/okasaki-visualization

max_issues_repo_name: nomicflux/okasaki-visualization

max_forks_repo_name: nomicflux/okasaki-visualization


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

Eq elem => Eq (Tree elem) where
    (==) Empty Empty = True
    (==) (Node left e right) (Node left' e' right')
          = left == left' && e == e' && right == right'
    (==) _ _ = False

Functor Tree where
    map f Empty = Empty
    map f (Node left e right)
        = Node (map f left)
               (f e)
               (map f right)

Foldable Tree where
  foldr f acc Empty = acc
  foldr f acc (Node left e right) = let leftfold = foldr f acc left
                                        rightfold = foldr f leftfold right in
                                        f e rightfold

  null Empty = True
  null _ = False


text:
module Main

main : IO ()
main = do putStrLn $ show $ map (\x => x + 1) $ Just 3
          putStrLn $ show $ map (*3) $ reverse [1..10]


text:
module Data.Tree

import Data.List
import Data.List1
import Data.String

%default total

--------------------------------------------------------------------------------
--          Finite Trees
--------------------------------------------------------------------------------

mutual

  ||| A finite rose tree
  public export
  record Tree (a : Type) where
    constructor MkTree
    value : a
    forest : Forest a

  ||| A finite forest of trees
  public export
  Forest : Type -> Type
  Forest = List . Tree

--------------------------------------------------------------------------------
--          Creating Trees
--------------------------------------------------------------------------------

public export
singleton : a -> Tree a
singleton a = MkTree a []

public export
replicate : (width : Nat) -> (depth : Nat) -> a -> Tree a
replicate _         0 x = MkTree x []
replicate width (S k) x = MkTree x $ replicate width (replicate width k x)

||| Unfold a tree up to the given depth.
public export
unfold : (depth : Nat) -> (f : s -> (a,List s)) -> s -> Tree a
unfold 0     f s = MkTree (fst $ f s) []
unfold (S k) f s = let (a,ss) = f s
                    in MkTree a (map (unfold k f) ss)

--------------------------------------------------------------------------------
--          Flattening Trees
--------------------------------------------------------------------------------

zipWithKeep : (a -> a -> a) -> List a -> List a -> List a
zipWithKeep f [] ys = ys
zipWithKeep f xs [] = xs
zipWithKeep f (x :: xs) (y :: ys) = f x y :: zipWithKeep f xs ys

public export
flatten : Tree a -> List a
flatten (MkTree v vs) = v :: flattenF vs
  where flattenF : Forest a -> List a
        flattenF []        = Nil
        flattenF (x :: xs) = flatten x ++ flattenF xs

public export
layers : Tree a -> List (List a)
layers (MkTree v vs) = [v] :: layersF vs
  where layersF : Forest a -> List (List a)
        layersF []        = Nil
        layersF (x :: xs) = zipWithKeep (++) (layers x) (layersF xs)

--------------------------------------------------------------------------------
--          Accessing Elements
--------------------------------------------------------------------------------

public export
index : List Nat -> Tree a -> Maybe a
index []        x = Just x.value
index (y :: ys) x = ix y x.forest >>= index ys
  where ix : Nat -> List b -> Maybe b
        ix _ []            = Nothing
        ix 0     (z :: _)  = Just z
        ix (S k) (_ :: zs) = ix k zs

--------------------------------------------------------------------------------
--          Functor and Monad Implementations
--------------------------------------------------------------------------------

-- All implementations are boilerplaty to satisfy the totality checker.
foldlTree : (a -> e -> a) -> a -> Tree e -> a
foldlTree f acc (MkTree v vs) = foldlF (f acc v) vs
  where foldlF : a -> Forest e -> a
        foldlF y []        = y
        foldlF y (x :: xs) = foldlF (foldlTree f y x) xs

foldrTree : (e -> a -> a) -> a -> Tree e -> a
foldrTree f acc (MkTree v vs) = f v (foldrF acc vs)
  where foldrF : a -> Forest e -> a
        foldrF y []        = y
        foldrF y (x :: xs) = foldrTree f (foldrF y xs) x

traverseTree : Applicative f => (a -> f b) -> Tree a -> f (Tree b)
traverseTree fun (MkTree v vs) = [| MkTree (fun v) (traverseF vs) |]
  where traverseF : Forest a -> f (Forest b)
        traverseF []        = pure []
        traverseF (x :: xs) = [| traverseTree fun x :: traverseF xs |]

mapTree : (a -> b) -> Tree a -> Tree b
mapTree f (MkTree v vs) = MkTree (f v) (mapF vs)
  where mapF : Forest a -> Forest b
        mapF []       = []
        mapF (h :: t) = mapTree f h :: mapF t

bindTree : Tree a -> (a -> Tree b) -> Tree b
bindTree (MkTree va tas) f =
  let MkTree vb tbs = f va
   in MkTree vb (tbs ++ bindF tas)

  where bindF : Forest a -> Forest b
        bindF []        = []
        bindF (x :: xs) = bindTree x f :: bindF xs

apTree : Tree (a -> b) -> Tree a -> Tree b
apTree tf ta = bindTree tf $ \f => mapTree (apply f) ta

joinTree : Tree (Tree a) -> Tree a
joinTree (MkTree (MkTree va tas) ftas) =
  MkTree va $ tas ++ joinF ftas

  where joinF : Forest (Tree a) -> Forest a
        joinF []        = []
        joinF (x :: xs) = joinTree x :: joinF xs

eqTree : Eq a => Tree a -> Tree a -> Bool
eqTree (MkTree x xs) (MkTree y ys) = x == y && eqF xs ys
  where eqF : Forest a -> Forest a -> Bool
        eqF [] []       = True
        eqF [] (_ :: _) = False
        eqF (_ :: _) [] = False
        eqF (x :: xs) (y :: ys) = eqTree x y && eqF xs ys

--------------------------------------------------------------------------------
--          Visualizing Trees
--------------------------------------------------------------------------------

export
drawTree : Tree String -> String
drawTree  = unlines . draw
  where
    drawForest : Forest String -> String
    drawForest  = unlines . map drawTree

    draw : Tree String -> List String
    draw (MkTree x ts0) = lines x ++ subTrees ts0
      where
        shift : String -> String -> List String -> List String
        shift first other tails =
          zipWith (++) (first :: replicate (length tails) other) tails

        subTrees : Forest String -> List String
        subTrees []      = []
        subTrees [t]     = "│" :: shift "└╼" "  " (draw t)
        subTrees (t::ts) = "│" :: shift "├╼" "│ " (draw t) ++ subTrees ts

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

public export %inline
Eq a => Eq (Tree a) where
  (==) = eqTree

public export %inline
Foldable Tree where
  foldl  = foldlTree
  foldr  = foldrTree
  null _ = False

public export %inline
Functor Tree where
  map = mapTree

public export %inline
Applicative Tree where
  pure a = MkTree a Nil
  (<*>)  = apTree

public export %inline
Monad Tree where
  (>>=) = bindTree
  join  = joinTree

public export %inline
Traversable Tree where
  traverse = traverseTree


text:
module Main

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

import Data.Nat
import Data.String.Parser
import Data.String.Parser.Expression

%default partial

table : OperatorTable Nat
table =
  [ [Infix (do token "^"; pure (power) ) AssocRight]
  , [ Infix (do token "*"; pure (*) ) AssocLeft ]
  , [ Infix (do token "+"; pure (+) ) AssocLeft ]
  ]

table' : OperatorTable Integer
table' =
  [ [ Infix (do token "*"; pure (*) ) AssocLeft
    , Infix (do token "/"; pure (div) ) AssocLeft
    ]
  , [ Infix (do token "+"; pure (+) ) AssocLeft
    , Infix (do token "-"; pure (-) ) AssocLeft
    ]
  ]

mutual
  term : Parser Nat
  term = (natural <|> expr) <* spaces
         <?> "simple expression"

  expr : Parser Nat
  expr = buildExpressionParser Nat table term

mutual
  term' : Parser Integer
  term' = (integer <|> expr') <* spaces
         <?> "simple expression"

  expr' : Parser Integer
  expr' = buildExpressionParser Integer table' term'

showRes : Show a => Either String (a, Int) -> IO ()
showRes res = case res of
                Left err => putStrLn err
                Right (xs, rem) => printLn xs

main : IO ()
main = do showRes (parse natural "5678")
          showRes (parse integer "-3")
          showRes (parse expr "1+4^3^2^1")
          showRes (parse expr' "4 + 2 * 3")
          showRes (parse expr' "13-3+1*2-10/2")


text:
module Vect

{-
To write these functions in vim:

\d to make a template definition
\c over a variable to do case analysis on that variable
\o to fill in a hole with the 'obvious' value

-}

append : Vect n a -> Vect m a -> Vect (n + m) a
append [] ys = ys
append (x :: xs) ys = x :: (append xs ys)

vzipWith : (a -> b -> c) -> Vect n a -> Vect n b -> Vect n c
vzipWith f [] [] = []
vzipWith f (x :: xs) (y :: ys) = f x y :: (vzipWith f xs ys)

max_stars_repo_name: silky/idris-demos

max_issues_repo_name: silky/idris-demos

max_forks_repo_name: silky/idris-demos


text:
module TakeN

data TakeN : List a -> Type where
     Fewer : TakeN xs
     Exact : (n_xs : List a) -> TakeN (n_xs ++ rest)

-- Ex. 10.1 # 1
total
takeN : (n : Nat) -> (xs : List a) -> TakeN xs
takeN Z xs = Exact []
takeN (S k) [] = Fewer
takeN (S k) (x :: xs) = case takeN k xs of
                             Fewer => Fewer
                             (Exact n_xs) => Exact $ x :: n_xs

groupByN : (n : Nat) -> (xs : List a) -> List (List a)
groupByN n xs with (takeN n xs)
  groupByN n xs | Fewer = [xs]
  groupByN n (n_xs ++ rest) | (Exact n_xs) = n_xs :: groupByN n rest

-- Ex. 10.1 # 2
halves : List a -> (List a, List a)
halves xs = splitHalf (div (length xs) 2) xs
  where
  splitHalf : Nat -> List a -> (List a, List a)
  splitHalf n xs with (takeN n xs)
    splitHalf n xs | Fewer = ([], xs)
    splitHalf n (n_xs ++ rest) | (Exact n_xs) = (n_xs, rest)


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

import public Minecraft.Base.PreClassic.GrassBlock
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 grassBlockItem : Item GrassBlock.Item
  public export %hint putGrassBlock  : Put  GrassBlock.Item
  public export %hint grassBlockVtbl : Vtbl GrassBlock.Item

max_stars_repo_name: po-stulate/postulate

max_issues_repo_name: po-stulate/postulate

max_forks_repo_name: po-stulate/postulate


text:
module GenericFinal

interface Symantics (rep : Type -> Type) where
  int : rep Int
  bool : rep Bool
  tuple : rep a -> rep b -> rep (a, b)
  list : rep a -> rep (List a)
  maybe : rep a -> rep (Maybe a)

data Printer : Type -> Type where
  P : (a -> String) -> Printer a

Symantics Printer where
  int = P (\x => show x)
  bool = P (\x => show x)
  tuple (P f) (P g) = P (\(x, y) => "(" ++ (f x) ++ ", " ++ (g y) ++ ")")
  list (P f) = P (\xs => let res = foldr (\elem, acc => if acc == "" then f elem else (f elem) ++ ", " ++ acc) "" xs in "[" ++ res ++ "]")
  maybe (P f) = P p
    where
      p : Maybe a -> String
      p Nothing = "Nothing"
      p (Just x) = "Just " ++ f x

print : Printer a -> a -> String
print (P f) = f

example : (List Int, Maybe Bool) -> String
example = print (tuple (list int) (maybe bool))

max_stars_repo_name: STELIORD/idris-snippets

max_issues_repo_name: stjordanis/idris-snippets

max_forks_repo_name: stjordanis/idris-snippets


text:
module TestArgs

import System

main : IO ()
main = getArgs >>= (putStrLn . show)


text:
module Main

import Data.Vect
import System.REPL
import Data.String
import Data.List

infixr 5 .+.

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

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

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

-- Store commands

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

display : {schema : _} -> SchemaType schema -> String
display {schema = SString} item = item
display {schema = SInt} item = show item
display {schema = SChar} item = show item
display {schema = (x .+. y)} (iteml, itemr) = display iteml ++ ", " ++ display itemr

getItem : Integer -> (store : DataStore) -> Maybe (String, DataStore)
getItem i store = case integerToFin i (size store) of
                    Nothing => Just ("Entry not found\n", store)
                    Just i => Just (display (index i (items store)) ++ "\n", store)

getAllItems : (store : DataStore) -> Maybe (String, DataStore)
getAllItems store = let all = printAll (items store) in if all /= ""
                                                           then Just (all, store)
                                                           else Just ("Store empty.\n", store) where
                              printAll : Vect n (SchemaType (schema store)) -> String
                              printAll [] = ""
                              printAll (x :: xs) = display x ++ "\n" ++ printAll xs

search : String -> DataStore -> Maybe (String, DataStore)
search substr store = Just (searchItems (items store), store) where
                            searchItems : Vect n (SchemaType (schema store)) -> String
                            searchItems [] = "No entries with " ++ substr ++ " found\n"
                            searchItems (x :: xs) = case isInfixOf substr (display x) of
                                                          False => searchItems xs
                                                          True => show (length xs) ++ ": " ++ display x ++ "\n"

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

-- -- REPL UI

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

parseBySchema : (schema : Schema) -> String -> Maybe (SchemaType schema)
parseBySchema schema input = case parsePrefix schema input of
                                  Nothing => Nothing
                                  Just (res, "") => Just res
                                  Just _ => Nothing where
                             parsePrefix : (schema : Schema) -> String -> Maybe (SchemaType schema, String)
                             parsePrefix SString input = getQuoted (unpack input) where
                                   getQuoted : List Char -> Maybe (String, String)
                                   getQuoted ('"' :: xs) = case span (/= '"') xs of
                                                                (quoted, '"' :: rest) => Just (pack quoted, ltrim (pack rest))
                                                                _ => Nothing
                                   getQuoted _ = Nothing
                             parsePrefix SInt input = case span isDigit input of
                                                           ("", rest) => Nothing
                                                           (num, rest) => Just (cast num, ltrim rest)
                             parsePrefix SChar input = map (\(ch, rest) => (ch, ltrim rest)) (strUncons input)
                             parsePrefix (x .+. y) input = do (l_val, input') <- parsePrefix x input
                                                              (r_val, input'') <-  parsePrefix y input'
                                                              Just ((l_val, r_val), input'')

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

parseCommand : (schema : Schema) -> String -> String -> Maybe (Command schema)
parseCommand schema cmd rest = case cmd of
                              "schema" => map SetSchema (parseSchema (words rest))
                              "add" => map Add (parseBySchema schema rest)
                              "get" => map Get (Just (parseInteger rest))
                              "search" => Just (Search rest)
                              "size" => Just Size
                              "quit" => Just Quit
                              _ => Nothing

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

processCommand : (store : DataStore) -> Command (schema store) -> Maybe (String, DataStore)
processCommand store (SetSchema newSchema) = case setSchema store newSchema of
                                                  Nothing => Just ("Cannot update schema for non-empty store\n", store)
                                                  Just newStore => Just ("Schema updated\n", newStore)

processCommand store (Add item) = Just ("Added ID " ++ show (size store) ++ " to store\n", addToStore store item)
processCommand store (Get (Just i)) = getItem i store
processCommand store (Get Nothing) = getAllItems store
processCommand store Size = Just (show (size store) ++ " entries in store\n", store)
processCommand store (Search substr) = search substr store
processCommand _ Quit = Nothing

processInput : DataStore -> String -> Maybe (String, DataStore)
processInput store input = case parse (schema store) input of
                                Nothing => Just ("Invalid command\n", store)
                                Just cmd => processCommand store cmd

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


text:
module InterpE

data Expr = Var String      -- variables
          | Val Int         -- values
          | Add Expr Expr   -- addition

data Eval : Type -> Type where
     MkEval : (List (String, Int) -> Maybe a) -> Eval a

fetch : String -> Eval Int
fetch x = MkEval (\e => fetchVal e) where
    fetchVal : List (String, Int) -> Maybe Int
    fetchVal [] = Nothing
    fetchVal ((v, val) :: xs) = if (x == v)
                                  then (Just val)
                                  else (fetchVal xs)

Functor Eval where
    map f (MkEval g) = MkEval (\e => map f (g e))

Applicative Eval where
    pure x = MkEval (\e => Just x)

    (<*>) (MkEval f) (MkEval g) = MkEval (\x => app (f x) (g x)) where
        app : Maybe (a -> b) -> Maybe a -> Maybe b
        app (Just fx) (Just gx) = Just (fx gx)
        app _         _         = Nothing

eval : Expr -> Eval Int
eval (Var x)   = fetch x
eval (Val x)   = [| x |]
eval (Add x y) = [| eval x + eval y |]

runEval : List (String, Int) -> Expr -> Maybe Int
runEval env e = case eval e of
    MkEval envFn => envFn env


text:
||| These are just the same interface implementations as in Prelude.Interfaces,
||| but named, so we can refer to them and safe the dictionaries in data structures.
module Interfaces.Named

%default total
%access public export

[eqUnit] Eq () where
  () == () = True

[eqBool] Eq Bool where
  True  == True  = True
  False == False = True
  _     == _     = False

[eqInt] Eq Int where
  (==) = boolOp prim__eqInt

[eqString] Eq String where
  (==) = boolOp prim__eqString

[eqList] Eq a => Eq (List a) where
  (==) []      []      = True
  (==) (x::xs) (y::ys) with ( x == y )
    | True             = xs == ys
    | False            = False
  (==) _ _             = False

max_stars_repo_name: mklinik/task-semantics

max_issues_repo_name: mklinik/task-semantics

max_forks_repo_name: mklinik/task-semantics


text:
module LightClick.IR.Channel.Normalise.Error

import Data.String

%default total

namespace Normalise
  public export
  data Error = ModuleInlined | NoModuleInstances

  export
  Show Error where
    show ModuleInlined     = "Normalisation Error: Module Inlined"
    show NoModuleInstances = "Normalisation Error: No Module instances found"

public export
Normalise : Type -> Type
Normalise = Either Error

-- [ EOF ]

max_stars_repo_name: border-patrol/lightclick

max_issues_repo_name: border-patrol/lightclick

max_forks_repo_name: border-patrol/lightclick


text:
module Subst

-- Substitution inside untyped lambda calculus terms.

import Term

%default total
%access public export

shift : (cutoff : Nat) -> (distance : Nat) ->
        Nat -> Nat
shift Z     distance k     = distance+k
shift (S c) distance Z     = Z
shift (S c) distance (S k) = S $ shift c distance k

shiftTerm : (cutoff : Nat) -> (distance : Nat) ->
            Term -> Term
--
shiftTerm c d (TVar i) = TVar (shift c d i)
--
shiftTerm c d (TAbs e) = TAbs $ shiftTerm (S c) d e
--
shiftTerm c d (TApp e1 e2) =
  let e1' = shiftTerm c d e1
      e2' = shiftTerm c d e2
  in TApp e1' e2'
--
shiftTerm c d (TRec e1 e2 e3) =
  let e1' = shiftTerm c d e1
      e2' = shiftTerm c d e2
      e3' = shiftTerm c d e3
  in TRec e1' e2' e3'
--
shiftTerm c d TZero = TZero
--
shiftTerm c d (TSucc e) = TSucc $ shiftTerm c d e
--
shiftTerm c d (TPred e) = TPred $ shiftTerm c d e
--
shiftTerm c d (TIfz e1 e2 e3) =
  let e1' = shiftTerm c d e1
      e2' = shiftTerm c d e2
      e3' = shiftTerm c d e3
  in TIfz e1' e2' e3'

subst_var : Term ->       -- Term that is subtituted in.
            (i : Nat) ->  -- The i-th variable (Var i) is substituted for.
            (j : Nat) ->  -- Substitution takes place inside the term (Var j).
            Term
subst_var ts Z     Z     = ts
subst_var ts Z     (S j) = TVar j
subst_var ts (S i) Z     = TVar Z
subst_var ts (S i) (S j) = shiftTerm Z (S Z) $ subst_var ts i j

subst : Term ->       -- Term that is substituted in.
        (i : Nat) ->  -- The i-th varibale (Var i) is substituted for.
        Term ->       -- Substitution takes place inside this term.
        Term
subst ts i (TVar j)        = subst_var ts i j
subst ts i (TAbs e)        = TAbs $ subst ts (S i) e
subst ts i (TApp e1 e2)    = TApp (subst ts i e1)
                                  (subst ts i e2)
subst ts i (TRec e1 e2 e3) = TRec (subst ts i e1)
                                  (subst ts i e2)
                                  (subst ts i e3)
subst _  _ TZero           = TZero
subst ts i (TSucc e)       = TSucc (subst ts i e)
subst ts i (TPred e)       = TPred (subst ts i e)
subst ts i (TIfz e1 e2 e3) = TIfz (subst ts i e1)
                                  (subst ts i e2)
                                  (subst ts i e3)

max_stars_repo_name: normanrink/PCF

max_issues_repo_name: normanrink/PCF

max_forks_repo_name: normanrink/PCF


text:
module GTK.GTK

import GTK.Utils

libgtk : String -> String
libgtk fname = "C:\{fname},libgtk-3.so"

export
data GtkWidget : Type where

public export
GtkWindow, GtkBox, GtkContainer, GtkMenuItem, GtkMenuShell : Type
GtkWindow = GtkWidget
GtkBox = GtkWidget
GtkContainer = GtkWidget
GtkMenuItem = GtkWidget
GtkMenuShell = GtkWidget

public export
GtkWindowType : Type
GtkWindowType  = Int

public export
GTK_WINDOW_TOPLEVEL, GTK_WINDOW_POPUP : GtkWindowType
GTK_WINDOW_TOPLEVEL = 0
GTK_WINDOW_POPUP = 1

public export
GtkAlign : Type
GtkAlign = Int

public export
GTK_ALIGN_FILL, GTK_ALIGN_START, GTK_ALIGN_END, GTK_ALIGN_CENTER, GTK_ALIGN_BASELINE : GtkAlign
GTK_ALIGN_FILL = 0
GTK_ALIGN_START = 1
GTK_ALIGN_END = 2
GTK_ALIGN_CENTER = 3
GTK_ALIGN_BASELINE = 4

public export
GtkWindowPosition : Type
GtkWindowPosition = Int

public export
GTK_WIN_POS_NONE, GTK_WIN_POS_CENTER, GTK_WIN_POS_MOUSE, GTK_WIN_POS_CENTER_ALWAYS, GTK_WIN_POS_CENTER_ON_PARENT : GtkWindowPosition
GTK_WIN_POS_NONE = 0
GTK_WIN_POS_CENTER = 1
GTK_WIN_POS_MOUSE = 2
GTK_WIN_POS_CENTER_ALWAYS = 3
GTK_WIN_POS_CENTER_ON_PARENT = 4

-- gtk_window

export %foreign libgtk "gtk_window_new"
gtk_window_new : GtkWindowType -> PrimIO (Ptr GtkWidget)

export %foreign libgtk "gtk_window_set_title"
gtk_window_set_title : Ptr GtkWindow -> String -> PrimIO ()

export %foreign libgtk "gtk_window_set_default_size"
gtk_window_set_default_size : Ptr GtkWindow -> Int -> Int -> PrimIO ()

export %foreign libgtk "gtk_window_set_default_size"
gtk_window_set_position : Ptr GtkWindow -> GtkWindowPosition -> PrimIO ()

-- gtk_button

export %foreign libgtk "gtk_button_new_with_label"
gtk_button_new_with_label : String -> PrimIO (Ptr GtkWidget)

export %foreign libgtk "gtk_button_new_with_mnemonic"
gtk_button_new_with_mnemonic : String -> PrimIO (Ptr GtkWidget)

-- gtk_alignment

export %foreign libgtk "gtk_alignment_new"
gtk_alignment_new : (xalign : Int) -> (yalign : Int) -> (xscale : Int) -> (yscale : Int) -> PrimIO (Ptr GtkWidget)

-- gtk_container

export %foreign libgtk "gtk_container_add"
gtk_container_add : Ptr GtkContainer -> Ptr GtkWidget -> PrimIO ()

export %foreign libgtk "gtk_container_set_border_width"
gtk_container_set_border_width : Ptr GtkContainer -> Int -> PrimIO ()

-- gtk_menu

export %foreign libgtk "gtk_menu_new"
gtk_menu_new : PrimIO (Ptr GtkWidget)

-- gtk_menu_bar

export %foreign libgtk "gtk_menu_bar_new"
gtk_menu_bar_new : PrimIO (Ptr GtkWidget)

-- gtk_menu_shell

export %foreign libgtk "gtk_menu_shell_append"
gtk_menu_shell_append : Ptr GtkMenuShell -> (child : Ptr GtkWidget) -> PrimIO ()

-- gtk_menu_item

export %foreign libgtk "gtk_menu_item_new_with_label"
gtk_menu_item_new_with_label : (label : String) -> PrimIO (Ptr GtkWidget)

export %foreign libgtk "gtk_menu_item_set_submenu"
gtk_menu_item_set_submenu : Ptr GtkMenuItem -> Ptr GtkWidget -> PrimIO ()

-- gtk_seperator

export %foreign libgtk "gtk_separator_menu_item_new"
gtk_separator_menu_item_new : PrimIO (Ptr GtkWidget)

-- gtk_box

export %foreign libgtk "gtk_box_pack_start"
gtk_box_pack_start : Ptr GtkBox -> Ptr GtkWidget -> (expand : CBool) -> (fill : CBool) -> (padding : Int) -> PrimIO ()

-- gtk_vbox

export %foreign libgtk "gtk_vbox_new"
gtk_vbox_new : (homogeneous : CBool) -> (spacing : Int) -> PrimIO (Ptr GtkWidget)

-- gtk_widget

export %foreign libgtk "gtk_widget_set_tooltip_text"
gtk_widget_set_tooltip_text : Ptr GtkWidget -> String -> PrimIO ()

export %foreign libgtk "gtk_widget_set_halign"
gtk_widget_set_halign : Ptr GtkWidget -> GtkAlign -> PrimIO ()

export %foreign libgtk "gtk_widget_set_valign"
gtk_widget_set_valign : Ptr GtkWidget -> GtkAlign -> PrimIO ()

export %foreign libgtk "gtk_widget_show_all"
gtk_widget_show_all : Ptr GtkWidget -> PrimIO ()

export %foreign libgtk "gtk_widget_show"
gtk_widget_show : Ptr GtkWidget -> PrimIO ()

-- gtk_init

export %foreign libgtk "gtk_init"
gtk_init : (argc : Ptr Int) -> (argv : Ptr String) -> PrimIO ()

-- gtk_main

export %foreign libgtk "gtk_main"
gtk_main : PrimIO ()

export %foreign libgtk "gtk_main_quit"
gtk_main_quit : PrimIO ()


text:
module LazyListTrav

import Data.List.Lazy

import Debug.Trace

%default total

public export
Traversable LazyList where
  traverse = map force .: tr where
    tr : (a -> f b) -> LazyList a -> f (Lazy (LazyList b))
    tr g [] = pure []
    tr g (x::xs) = [| g x :: tr g xs |] where
      (::) : forall a. a -> Lazy (LazyList a) -> Lazy (LazyList a)
      (::) x xs = delay $ Lazy.(::) x xs

debugList : Nat -> LazyList Nat
debugList n = iterateN n f 1 where
  f : Nat -> Nat
  f x = trace "arg: \{show x}" $ x + 1

d : Applicative f => f $ LazyList Nat
d = map (Lazy.take 3) $ traverse pure $ debugList 500

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
module Language.LSP.Message.LinkedEditingRange

import Language.JSON
import Language.LSP.Message.Derive
import Language.LSP.Message.Location
import Language.LSP.Message.Progress
import Language.LSP.Message.TextDocument
import Language.LSP.Message.Utils
import Language.Reflection

%language ElabReflection
%default total

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_linkedEditingRange
public export
record LinkedEditingRangeClientCapabilities where
  constructor MkLinkedEditingRangeClientCapabilities
  dynamicRegistration : Maybe Bool
%runElab deriveJSON defaultOpts `{{LinkedEditingRangeClientCapabilities}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_linkedEditingRange
public export
record LinkedEditingRangeOptions where
  constructor MkLinkedEditingRangesOptions
  workDoneProgress : Maybe Bool
%runElab deriveJSON defaultOpts `{{LinkedEditingRangeOptions}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_linkedEditingRange
public export
record LinkedEditingRangeRegistrationOptions where
  constructor MkLinkedEditingRangesRegistrationOptions
  workDoneProgress : Maybe Bool
  documentSelector : OneOf [DocumentSelector, Null]
  id               : Maybe Bool
%runElab deriveJSON defaultOpts `{{LinkedEditingRangeRegistrationOptions}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_linkedEditingRange
public export
record LinkedEditingRangeParams where
  constructor MkLinkedEditingRangesParams
  workDoneToken : Maybe ProgressToken
  textDocument  : TextDocumentIdentifier
  position      : Position
%runElab deriveJSON defaultOpts `{{LinkedEditingRangeParams}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_linkedEditingRange
public export
record LinkedEditingRanges where
  constructor MkLinkedEditingRanges
  ranges      : List Range
  wordPattern : Maybe String
%runElab deriveJSON defaultOpts `{{LinkedEditingRanges}}


text:
module Control.Cont.Thread

import Data.List

import Control.HigherOrder

import Control.Monad.Free

public export
data Thread : (Type -> Type) -> (Type -> Type) where
  Yield : m a -> Thread m a
  Fork : forall t. m t -> m a -> Thread m a

public export
HThread : (Type -> Type) -> (Type -> Type)
HThread = Thread

public export
yield : Inj Thread sig => Free sig ()
yield = inject $ Yield $ return ()

public export
fork : Inj Thread sig => Free sig a -> Free sig ()
fork d = inject $ Fork d $ return ()

public export
HFunctor Thread where
  hmap f (Yield x) = Yield (f x)
  hmap f (Fork x y) = Fork (f x) (f y)

public export
Syntax Thread where
  emap f (Yield p) = Yield (f p)
  emap f (Fork d p) = Fork d (f p)

  weave s hdl (Yield p) = Yield (hdl (map (const p) s))
  weave s hdl (Fork d p) = Fork (hdl (map (const d) s))
                                (hdl (map (const p) s))

public export
data Daemon : ((Type -> Type) -> (Type -> Type)) -> Type where
  MkDaemon : forall t. Free (Thread :+: sig) t -> Daemon sig

public export
data SThread : (f : (Type -> Type) -> (Type -> Type))
            -> Type
            -> Type where
  SYield : Free (Thread :+: sig) r -> SThread sig r
  SFork : Daemon sig -> Free (Thread :+: sig) r -> SThread sig r
  SActive : r -> SThread sig r

public export
Syntax sig => Functor (SThread sig) where
  map f (SActive x) = SActive (f x)
  map f (SYield p) = SYield (map f p)
  map f (SFork d p) = SFork d (map f p)

mutual
  public export
  thread : Syntax sig
        => Handler (SThread sig) (Free (Thread :+: sig)) (Free sig)
  thread (SActive p) = runThread p
  thread (SYield p) = return (SYield (join p))
  thread (SFork d p) = return (SFork d (join p))

  public export
  runThread : Syntax sig
           => Free (Thread :+: sig) a -> Free sig (SThread sig a)
  runThread (Return x) = return (SActive x)
  runThread (Op (Inl (Yield q))) = return (SYield q)
  runThread (Op (Inl (Fork d q))) = return (SFork (MkDaemon d) q)
  runThread (Op (Inr op)) = Op (weave {s = SThread sig} (SActive ()) thread op)

public export
schedule : Syntax sig => Free (Thread :+: sig) a -> Free sig a
schedule p = master p [] where
  mutual
    daemons : List (Daemon sig) -> List (Daemon sig) -> Free (Thread :+: sig) a -> Free sig a
    daemons [] ds' p = master p (reverse ds')
    daemons (MkDaemon q :: ds) ds' p = do
      r <- runThread q
      case r of
        SActive _ => daemons ds ds' p
        SYield q' => daemons ds (MkDaemon q' :: ds') p
        SFork d' q' => daemons (d' :: ds) (MkDaemon q' :: ds') p

    master : Free (Thread :+: sig) a -> List (Daemon sig) -> Free sig a
    master p ds = do
      r <- runThread p
      case r of
        SActive x => return x
        SYield p => daemons ds [] p
        SFork d p => daemons (d :: ds) [] p


text:
||| Copyright 2016 Google Inc.
|||
||| 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.
|||
||| Equality and Show for descriptors.  Equality for values isn't working so
||| far.

module Protobuf.Util

import Protobuf.Core
import Protobuf.Printer

%access export
%default total

||| Does an action for each element of a list.
forEach : Monad m => (a -> m ()) -> List a -> m ()
forEach _ Nil       = return ()
forEach f (x :: xs) = do {
  f x
  forEach f xs
}

implementation Eq Label where
  Optional == Optional = True
  Required == Required = True
  Repeated == Repeated = True
  _ == _ = False

implementation Eq EnumValueDescriptor where
  (MkEnumValueDescriptor name value) == (MkEnumValueDescriptor name' value') =
    name == name' && value == value'
  _ == _ = False

heteroEq : Eq a => Vect k a -> Vect k' a -> Bool
heteroEq (x::xs) (x'::xs') = x == x'
heteroEq Nil Nil = True
heteroEq _ _ = False

implementation Eq EnumDescriptor where
  (MkEnumDescriptor name values) == (MkEnumDescriptor name' values') =
    name == name' && heteroEq values values'
  _ == _ = False

mutual
  implementation Eq MessageDescriptor where
    (MkMessageDescriptor name fields) == (MkMessageDescriptor name' fields') =
      assert_total $ name == name' && heteroEq fields fields'

  implementation Eq FieldDescriptor where
    (MkFieldDescriptor label ty name number) == (MkFieldDescriptor label' ty' name' number') =
      label == label' && ty == ty' && name == name' && number == number'

  implementation Eq FieldValueDescriptor where
    PBDouble == PBDouble = True
    PBFloat == PBFloat = True
    PBInt32 == PBInt32 = True
    PBInt64 == PBInt64 = True
    PBUInt32 == PBUInt32 = True
    PBUInt64 == PBUInt64 = True
    PBSInt32 == PBSInt32 = True
    PBSInt64 == PBSInt64 = True
    PBFixed32 == PBFixed32 = True
    PBFixed64 == PBFixed64 = True
    PBSFixed32 == PBSFixed32 = True
    PBSFixed64 == PBSFixed64 = True
    PBBool == PBBool = True
    PBString == PBString = True
    PBBytes == PBBytes = True
    (PBMessage m) == (PBMessage m') = m == m'
    (PBEnum e) == (PBEnum e') = e == e'
    _ == _ = False

implementation Show Label where
  show Optional = "optional"
  show Required = "required"
  show Repeated = "repeated"

printEnumValueDescriptor : EnumValueDescriptor -> Printer ()
printEnumValueDescriptor (MkEnumValueDescriptor name value) =
  printIndent *> print (name ++ " = " ++ (show value) ++ ";\n")

printEnumDescriptor : EnumDescriptor -> Printer ()
printEnumDescriptor (MkEnumDescriptor name values) =
    print ("enum " ++ name  ++ " ") *> braces (forEach printEnumValueDescriptor (toList values))

implementation Show EnumDescriptor where
  show = runPrinter . printEnumDescriptor

implementation Show FieldValueDescriptor where
  show PBDouble = "double"
  show PBFloat = "float"
  show PBInt32 = "int32"
  show PBInt64 = "int64"
  show PBSInt32 = "sint32"
  show PBSInt64 = "sint64"
  show PBUInt32 = "uint32"
  show PBUInt64 = "uint64"
  show PBFixed32 = "fixed32"
  show PBFixed64 = "fixed64"
  show PBSFixed32 = "sfixed32"
  show PBSFixed64 = "sfixed64"
  show PBBool = "bool"
  show PBString = "string"
  show PBBytes = "bytes"
  show (PBMessage m) = name m
  show (PBEnum e) = name e

printFieldDescriptor : FieldDescriptor -> Printer ()
printFieldDescriptor (MkFieldDescriptor label ty name number) =
  printIndent *> print (
    (show label) ++ " " ++ (show ty) ++ " " ++ name ++ " = " ++ (show number) ++ ";\n")

printMessageDescriptor : MessageDescriptor -> Printer ()
printMessageDescriptor (MkMessageDescriptor name fields) =
    print ("message " ++ name ++ " ") *> braces (forEach printFieldDescriptor (toList fields))

implementation Show MessageDescriptor where
  show = runPrinter . printMessageDescriptor

max_stars_repo_name: google/idris-protobuf

max_issues_repo_name: google/idris-protobuf

max_forks_repo_name: google/idris-protobuf


text:
module Foreign

import Data.Maybe

import Idris.IDEMode.Commands

import public System.FFI.Lua

-- TODO: Build safe wrappers for sockets and handlers `OpaqueDict`s
-- TODO: PrimIO exposed foreigns are not finalised designs

%foreign "_ => vim.loop.new_pipe(false)"
prim__newPipe : PrimIO OpaqueDict

export
newPipe : HasIO io => io OpaqueDict
newPipe = primIO prim__newPipe

%foreign "_ => vim.loop.new_tcp()"
prim__newTCP : PrimIO OpaqueDict

export
newTCP : HasIO io => io OpaqueDict
newTCP = primIO prim__newTCP

%foreign "idris.support.spawn|support"
prim__spawn : String -> OpaqueDict -> (Int -> Int -> PrimIO ()) -> PrimIO OpaqueDict

export
spawn : HasIO io
     => String
     -> Dict [("args", Lua.List [String, String]), ("stdio", Lua.List [OpaqueDict, OpaqueDict, OpaqueDict])]
     -> (Int -> Int -> IO ())
     -> io (Dict [("handle", OpaqueDict), ("pid", Int)])
spawn cmd (MkDict opts) f =
  MkDict <$> primIO (prim__spawn cmd opts (\x, y => toPrim $ f x y))

%foreign "idris.support.readStart|support"
prim__readStart : OpaqueDict -> (String -> PrimIO ()) -> (String -> PrimIO ()) -> PrimIO () -> PrimIO ()

export
readStart : HasIO io => OpaqueDict
         -> (onok : String -> IO ())
         -> (onerr : String -> IO ())
         -> (onclose : IO ())
         -> io ()
readStart stream onok onerr onclose =
  primIO $ prim__readStart stream (\s => toPrim $ onok s)
                                  (\s => toPrim $ onerr s)
                                  (toPrim onclose)

%foreign "stream, _ => stream:read_stop()"
prim__readStop : OpaqueDict -> PrimIO ()

export
readStop : HasIO io => OpaqueDict -> io ()
readStop = primIO . prim__readStop

%foreign "handle, _ => handle:kill(15)"
prim__sigtermHandle : OpaqueDict -> PrimIO ()

export
sigterm : HasIO io => OpaqueDict -> io ()
sigterm = primIO . prim__sigtermHandle

%foreign "client, _ => client:shutdown()"
prim__shutdown : OpaqueDict -> PrimIO ()

export
shutdown : HasIO io => OpaqueDict -> io ()
shutdown = primIO . prim__shutdown

%foreign "client, _ => client:close()"
prim__close : OpaqueDict -> PrimIO ()

export
close : HasIO io => OpaqueDict -> io ()
close = primIO . prim__close

%foreign "idris.support.connect|support"
prim__connect : OpaqueDict -> String -> Int -> PrimIO () -> (String -> PrimIO ()) -> PrimIO ()

export
connect : HasIO io
       => OpaqueDict
       -> String
       -> Int
       -> IO ()
       -> (String -> IO ())
       -> io ()
connect client host port onok onerr = primIO $ prim__connect client host port (toPrim onok) (\s => toPrim $ onerr s)

%foreign "client, data, _ => client:write(data)"
prim__write : OpaqueDict -> String -> PrimIO ()

export
write : HasIO io => OpaqueDict -> String -> io ()
write client s = primIO $ prim__write client s

%foreign "_ => vim.fn.expand('%:p')"
prim__filePath : PrimIO String

export
filePath : HasIO io => io String
filePath = primIO prim__filePath

-- FIXME: Lua global variable hack
export %foreign "client => function(_) global_client = client end"
setGlobalClient : OpaqueDict -> PrimIO ()

export %foreign "_ => global_client"
getGlobalClient : PrimIO OpaqueDict

export %foreign "idris.support.putCmdInHistory|support"
putCmdInHistory : Int -> IDECommand -> PrimIO Int

export %foreign "idris.support.putLastSearch|support"
putLastSearch : String -> PrimIO Int

export %foreign "idris.support.deleteCmdInHistory|support"
deleteCmdInHistory : Int -> PrimIO ()

export %foreign "idris.support.deleteLastSearch|support"
deleteLastSearch : Int -> PrimIO ()

export %foreign "idris.support.getCmdFromHistory|support"
getCmdFromHistory : Int -> PrimIO (Maybe IDECommand)

export %foreign "idris.support.getLastSearch|support"
getLastSearch : PrimIO (Maybe String)

export %foreign "idris.support.genHistoryIndex|support"
genHistoryIndex : PrimIO Int

export %foreign "idris.support.fastLines|support"
fastLines : String -> List String

%foreign "_ => vim.fn.expand('<cword>')"
prim__cursorWord : PrimIO String

export
cursorWord : HasIO io => io String
cursorWord = primIO prim__cursorWord

%foreign "_ => vim.fn.expand('<cWORD>')"
prim__cursorWord' : PrimIO String

export
cursorWord' : HasIO io => io String
cursorWord' = primIO prim__cursorWord'

%foreign "_ => vim.fn.line('.')"
prim__cursorLine : PrimIO Int

export
cursorLine : HasIO io => io Int
cursorLine = primIO prim__cursorLine

%foreign "_ => vim.fn.col('.')"
prim__cursorColumn : PrimIO Int

export
cursorColumn : HasIO io => io Int
cursorColumn = primIO prim__cursorColumn

%foreign "line, col, _ => vim.fn.cursor(line, col)"
prim__setCursor : Int -> Int -> PrimIO ()

export
setCursor : HasIO io => Int -> Int -> io ()
setCursor l c = primIO $ prim__setCursor l c

%foreign "pat, _ => vim.fn.search(pat)"
prim__searchPattern : String -> PrimIO Int

export
searchPattern : HasIO io => String -> io Int
searchPattern pat = primIO $ prim__searchPattern pat

%foreign "idris.support.getSelection|support"
prim__getSelection : PrimIO String

export
getSelection : HasIO io => io String
getSelection = primIO prim__getSelection

%foreign "_ => vim.api.nvim_command('w')"
prim__saveBuffer : PrimIO ()

%foreign "name, _ => vim.fn.bufexists(name)"
prim__bufexists : String -> PrimIO Int

export
bufexists : HasIO io => String -> io Bool
bufexists bufName = do
  case !(primIO $ prim__bufexists bufName) of
    0 => pure False
    _ => pure True

export
saveBuffer : HasIO io => io ()
saveBuffer = primIO prim__saveBuffer

%foreign "idris.support.isBufferModified|support"
prim__isBufferModified : PrimIO Bool

export
isBufferModified : HasIO io => io Bool
isBufferModified = primIO prim__isBufferModified

%foreign "cmd, _ => vim.api.nvim_command(cmd)"
prim__nvimCommand : String -> PrimIO ()

%foreign "expr, _ => vim.api.nvim_eval(expr)"
prim__nvimEval : String -> PrimIO ty

export
nvimCommand : HasIO io => String -> io ()
nvimCommand = primIO . prim__nvimCommand

export
nvimEval : HasIO io => String -> io ty
nvimEval = primIO . prim__nvimEval

%foreign "key, cmd, _ => vim.api.nvim_set_keymap('n', key, cmd, { noremap = true, silent = true })"
prim__nnoremap : String -> String -> PrimIO ()

%foreign "key, cmd, _ => vim.api.nvim_set_keymap('v', key, cmd, { noremap = true, silent = true })"
prim__vnoremap : String -> String -> PrimIO ()

export
nnoremap : HasIO io => String -> String -> io ()
nnoremap k cmd = primIO $ prim__nnoremap k cmd

export
vnoremap : HasIO io => String -> String -> io ()
vnoremap k cmd = primIO $ prim__vnoremap k cmd

%foreign "idris.support.getGlobalStringVar|support"
prim__getGlobalStringVar : String -> PrimIO (Maybe String)

export
getGlobalStringVar : HasIO io => String -> Lazy String -> io String
getGlobalStringVar key def = do
  val <- primIO $ prim__getGlobalStringVar key
  pure $ fromMaybe def val

export
getGlobalStringVar' : HasIO io => String -> io (Maybe String)
getGlobalStringVar' key = primIO $ prim__getGlobalStringVar key

%foreign "idris.support.getGlobalBoolVar|support"
prim__getGlobalBoolVar : String -> PrimIO (Maybe Bool)

export
getGlobalBoolVar : HasIO io => String -> Lazy Bool -> io Bool
getGlobalBoolVar key def = do
  val <- primIO $ prim__getGlobalBoolVar key
  pure $ fromMaybe def val

export
getGlobalBoolVar' : HasIO io => String -> io (Maybe Bool)
getGlobalBoolVar' key = primIO $ prim__getGlobalBoolVar key

%foreign "idris.support.getGlobalIntVar|support"
prim__getGlobalIntVar : String -> PrimIO (Maybe Int)

export
getGlobalIntVar : HasIO io => String -> Lazy Int -> io Int
getGlobalIntVar key def = do
  val <- primIO $ prim__getGlobalIntVar key
  pure $ fromMaybe def val

export
getGlobalIntVar' : HasIO io => String -> io (Maybe Int)
getGlobalIntVar' key = primIO $ prim__getGlobalIntVar key


text:
module Commons.Config.JSON.Helpers

import Data.PList

import Commons.Config.JSON.Model

%access public export
%default total

data ParseResult : Type where
  PR : (ty : JTy)
    -> (value : JSONDoc ty)
    -> (prf   : JPred ty)
    -> ParseResult

data ArrayResult : List JTy -> Type where
  SR : DList JTy JSONDoc as
    -> DList JTy JPred as
    -> ArrayResult as

combineAsArray : List ParseResult -> (as ** ArrayResult as)
combineAsArray [] = (_ ** SR Nil Nil)
combineAsArray (x :: xs) with (x)
  combineAsArray (x :: xs) | (PR ty value prf) with (combineAsArray xs)
    combineAsArray (x :: xs) | (PR ty value prf) | (as ** pf) with (pf)
      combineAsArray (x :: xs) | (PR ty value prf) | (as ** pf) | (SR rest prfs) =
        (ty ::as ** SR (value::rest) (prf :: prfs))

toArray : List ParseResult -> JSONDoc ARRAY
toArray ps with (combineAsArray ps)
  toArray ps | (x ** prf) with (prf)
    toArray ps | (x ** prf) | (SR rest y) =
      JArray (fromDList rest y)

data DictResult : List JTy -> Type where
  DR : DList JTy (\ty => Pair String (JSONDoc ty)) as
    -> DList JTy JPred as
    -> DictResult as

combineAsDict : List (String, ParseResult)
             -> (as ** DictResult as)
combineAsDict [] = (_ ** DR Nil Nil)
combineAsDict ((a, b) :: xs) with (b)
  combineAsDict ((a, b) :: xs) | (PR ty value prf) with (combineAsDict xs)
    combineAsDict ((a, b) :: xs) | (PR ty value prf) | (x ** pf) with (pf)
      combineAsDict ((a, b) :: xs) | (PR ty value prf) | (x ** pf) | (DR rest y) =
        (ty :: x ** DR (MkPair a value::rest) (prf :: y))

toDict : List (String, ParseResult) -> JSONDoc MAP
toDict xs with (combineAsDict xs)
  toDict xs | (x ** pf) with (pf)
    toDict xs | (x ** pf) | (DR rest y) =
      JMap (fromDList rest y)

max_stars_repo_name: jfdm/idris-common

max_issues_repo_name: jfdm/idris-common

max_forks_repo_name: jfdm/idris-common


text:
module Compiler.ES.Ast

import Core.CompileExpr
import Core.Context
import Compiler.Common
import Data.List1
import Data.Nat
import Data.Vect

%default total

||| A variable in a toplevel function definition
|||
||| When generating the syntax tree of imperative
||| statements and expressions, we decide - based on
||| codegen directives - which Idris names to keep
||| and which names to convert to short, mangled
||| versions.
public export
data Var =
    ||| An unaltered name - usually a toplevel function
    ||| or a function argument with an explicitly given
    ||| name
    VName Name |

    ||| Index of a local variables
    VLoc  Int  |

    ||| Index of a mangled toplevel function
    VRef  Int

||| A minimal expression.
public export
data Minimal =
  ||| A variable
  MVar Var |

  ||| A projection targeting the field of a data type.
  ||| We include these here since it allows us to
  ||| conveniently carry around a `SortedMap Name Minimal`
  ||| for name resolution during the generation of the
  ||| imperative syntax tree.
  MProjection Nat Minimal

--------------------------------------------------------------------------------
--          Expressions
--------------------------------------------------------------------------------

||| The effect of a statement or a block of statements.
||| `Returns` means the
||| result of the final expression will be returned as
||| the current function's result, while `ErrorWithout v`
||| is a reminder, that the block of code will eventually
||| assign a value to `v` and will fail to do so if
||| `v` hasn't previously been declared.
|||
||| This is used as a typelevel index to prevent us from
||| making some common stupid errors like declaring a variable
||| twice, or having several `return` statements in the same
||| block of code.
public export
data Effect = Returns | ErrorWithout Var

mutual
  ||| An expression in a function definition.
  public export
  data Exp : Type where
    ||| A variable or projection. Minimal expressions
    ||| will always be inlined unless explicitly bound
    ||| in an Idris2 `let` expression.
    EMinimal  : Minimal -> Exp

    ||| Lambda expression
    |||
    ||| An empty argument list represents a delayed computation
    ELam      : List Var -> Stmt (Just Returns) -> Exp

    ||| Function application.
    |||
    ||| In case of a zero-argument list, we might also be
    ||| dealing with forcing a delayed computation.
    EApp      : Exp -> List Exp -> Exp

    ||| Saturated construtor application.
    |||
    ||| The tag either represents the name of a type constructor
    ||| (when we are pattern matching on types) or the index
    ||| of a data constructor.
    ECon      : (tag : Either Int Name) -> ConInfo -> List Exp -> Exp

    ||| Primitive operation
    EOp       : {0 arity : Nat} -> PrimFn arity -> Vect arity Exp -> Exp

    ||| Externally defined primitive operation.
    EExtPrim  : Name -> List Exp -> Exp

    ||| A constant primitive.
    EPrimVal  : Constant -> Exp

    ||| An erased value.
    EErased   : Exp

  ||| An imperative statement in a function definition.
  |||
  ||| This is indexed over the `Effect` the statement,
  ||| will have.
  ||| An `effect` of `Nothing` means that the result of
  ||| the statement is `undefined`: The declaration of
  ||| a constant or assignment of a previously declared
  ||| variable. When we sequence statements in a block
  ||| of code, all but the last one of them must have
  ||| effect `Nothing`. This makes sure we properly declare variables
  ||| exactly once before eventually assigning them.
  ||| It makes also sure a block of code does not contain
  ||| several `return` statements (until they are the
  ||| results of the branches of a `switch` statement).
  public export
  data Stmt : (effect : Maybe Effect) -> Type where
    ||| Returns the result of the given expression.
    Return      : Exp -> Stmt (Just Returns)

    ||| Introduces a new constant by assigning the result
    ||| of a single expression to the given variable.
    Const      : (v : Var) -> Exp -> Stmt Nothing

    ||| Assigns the result of an expression to the given variable.
    ||| This will result in an error, if the variable has not
    ||| yet been declared.
    Assign     : (v : Var) -> Exp -> Stmt (Just $ ErrorWithout v)

    ||| Declares (but does not yet assign) a new mutable
    ||| variable. This is the only way to "saturate"
    ||| a `Stmt (Just $ ErrorWithout v)`.
    Declare    : (v : Var) -> Stmt (Just $ ErrorWithout v) -> Stmt Nothing

    ||| Switch statement from a pattern match on
    ||| data or type constructors. The result of each branch
    ||| will have the given `Effect`.
    |||
    ||| The scrutinee has already been lifted to
    ||| the outer scope to make sure it is only
    ||| evaluated once.
    ConSwitch   :  (e         : Effect)
                -> (scrutinee : Minimal)
                -> (alts      : List $ EConAlt e)
                -> (def       : Maybe $ Stmt $ Just e)
                -> Stmt (Just e)

    ||| Switch statement from a pattern on
    ||| a constant. The result of each branch
    ||| will have the given `Effect`.
    ConstSwitch :  (e         : Effect)
                -> (scrutinee : Exp)
                -> (alts      : List $ EConstAlt e)
                -> (def       : Maybe $ Stmt $ Just e)
                -> Stmt (Just e)

    ||| A runtime exception.
    Error       : {0 any : _} -> String -> Stmt (Just any)

    ||| A code block consisting of one or more
    ||| imperative statements.
    Block       :  List1 (Stmt Nothing) -> Stmt e -> Stmt e

  ||| Single branch in a pattern match on a data or
  ||| type constructor.
  public export
  record EConAlt (e : Effect) where
    constructor MkEConAlt
    tag     : Either Int Name
    conInfo : ConInfo
    body    : Stmt (Just e)

  ||| Single branch in a pattern match on a constant
  public export
  record EConstAlt (e : Effect) where
    constructor MkEConstAlt
    constant : Constant
    body     : Stmt (Just e)

export
toMinimal : Exp -> Maybe Minimal
toMinimal (EMinimal v) = Just v
toMinimal _            = Nothing

export
prepend : List (Stmt Nothing) -> Stmt (Just e) -> Stmt (Just e)
prepend []       s = s
prepend (h :: t) s = Block (h ::: t) s

export total
declare : {v : _} -> Stmt (Just $ ErrorWithout v) -> Stmt Nothing
declare (Assign v y)              = Const v y
declare (Block ss s)              = Block ss $ declare s
declare s                         = Declare v s


text:
module Tricho

data Trichotomy : (eq, lt : a -> a -> Type) -> (a -> a -> Type) where
  LT : {0 x, y : a} -> lt x y -> Trichotomy eq lt x y
  EQ : {0 x, y : a} -> eq x y -> Trichotomy eq lt x x
  GT : {0 x, y : a} -> lt y x -> Trichotomy eq lt x y

interface Trichotomous (a : Type) (eq, lt : a -> a -> Type) where

  trichotomy : (x, y : a) -> Trichotomy eq lt x y