text:
module shafiln.odds

import Evens

import Intro

data IsOdd : Nat -> Type where
  OneOdd : IsOdd 1
  SSOdd  : (n:Nat) -> IsOdd n -> IsOdd (S (S (n) ))

ThreeOdd : IsOdd 3
ThreeOdd = SSOdd 1 OneOdd

ZeroNotOdd : IsOdd 0->Void
ZeroNotOdd OneOdd impossible
ZeroNotOdd (SSOdd _ _) impossible

TwoNotOdd : IsOdd 2 ->Void
TwoNotOdd (SSOdd Z OneOdd) impossible
TwoNotOdd (SSOdd Z (SSOdd _ _)) impossible

nOddSnEven : (n:Nat)->IsOdd n ->IsEven (S(n))
nOddSnEven (S(Z)) OneOdd = SSEven Z ZEven
nOddSnEven (S (S k)) (SSOdd k x) = SSEven (S(k)) (nOddSnEven k x)

nEvenSnOdd : (n:Nat)->IsEven n ->IsOdd (S(n))
nEvenSnOdd Z ZEven = OneOdd
nEvenSnOdd (S(S k)) (SSEven k x) = SSOdd (S(k)) (nEvenSnOdd k x)

nEvenOrOdd : (n:Nat)->Either (IsEven n) (IsOdd n)
nEvenOrOdd Z = Left ZEven
nEvenOrOdd (S k) = case (nEvenOrOdd k) of
                        (Left l) => Right (nEvenSnOdd k l)
                        (Right r) => Left (nOddSnEven k r)

nNotEvenAndOdd : (n:Nat)->IsEven n ->IsOdd n->Void
nNotEvenAndOdd Z ZEven OneOdd impossible
nNotEvenAndOdd Z ZEven (SSOdd _ _) impossible
nNotEvenAndOdd (S Z) ZEven _ impossible
nNotEvenAndOdd (S Z) (SSEven _ _) _ impossible
nNotEvenAndOdd (S (S k)) (SSEven k x) (SSOdd k y) = nNotEvenAndOdd k x y

oddPlusOddEven : (n:Nat)->(m:Nat)-> IsOdd n ->IsOdd m ->IsEven (add n m)
oddPlusOddEven (S(Z)) m OneOdd y = nOddSnEven m y
oddPlusOddEven (S(S k)) m (SSOdd k x) y = SSEven (add k m) (oddPlusOddEven k m x y)

apNat : (f: Nat -> Nat) -> (n: Nat) -> (m: Nat) -> n = m -> f n = f m
apNat f m m Refl = Refl

oddIsSdouble : (n:Nat)-> IsOdd n ->(m:Nat ** (n = (S(double m))))
oddIsSdouble (S(Z)) OneOdd = (Z ** Refl)
oddIsSdouble (S (S k)) (SSOdd k x) = case (oddIsSdouble k x) of
                                          (m ** pf) => ((S m) ** (apNat (\l => S(S l)) k (S(double m)) pf))


text:
import Data.Primitives.Views
import Data.Bits
import Data.String
import System

%default total

export
data Command : Type -> Type where
     PutStr : String -> Command ()
     GetLine : Command String

     Pure : ty -> Command ty
     Bind : Command a -> (a -> Command b) -> Command b

export
data ConsoleIO : Type -> Type where
     Quit : a -> ConsoleIO a
     Do : Command a -> (a -> Inf (ConsoleIO b)) -> ConsoleIO b
     Seq : Command () -> Inf (ConsoleIO a) -> ConsoleIO a

namespace CommandDo
  export
  (>>=) : Command a -> (a -> Command b) -> Command b
  (>>=) = Bind

  export
  (>>) : Command () -> Command b -> Command b
  ma >> mb = Bind ma (\ _ => mb)

namespace ConsoleDo
  export
  (>>=) : Command a -> (a -> Inf (ConsoleIO b)) -> ConsoleIO b
  (>>=) = Do

  export
  (>>) : Command () -> Inf (ConsoleIO b) -> ConsoleIO b
  (>>) = Seq

data Fuel = Dry | More (Lazy Fuel)

runCommand : Command a -> IO a
runCommand (PutStr x) = putStr x
runCommand GetLine = getLine
runCommand (Pure val) = pure val
runCommand (Bind c f) = do res <- runCommand c
                           runCommand (f res)

run : Fuel -> ConsoleIO a -> IO (Maybe a)
run fuel (Quit val) = do pure (Just val)
run (More fuel) (Do c f) = do res <- runCommand c
                              run fuel (f res)
run (More fuel) (Seq c d) = do runCommand c; run fuel d
run Dry p = pure Nothing

randoms : Int -> Stream Int
randoms seed = let seed' = 1664525 * seed + 1013904223 in
                   (seed' `shiftR` fromNat 2) :: randoms seed'

arithInputs : Int -> Stream Int
arithInputs seed = map bound (randoms seed)
  where
    bound : Int -> Int
    bound x with (divides x 12)
      bound ((12 * div) + rem) | (DivBy div rem prf) = abs rem + 1

mutual
  correct : Stream Int -> (score : Nat) -> ConsoleIO Nat
  correct nums score
          = do PutStr "Correct!\n"
               quiz nums (score + 1)

  wrong : Stream Int -> Int -> (score : Nat) -> ConsoleIO Nat
  wrong nums ans score
        = do PutStr ("Wrong, the answer is " ++ show ans ++ "\n")
             quiz nums score

  data Input = Answer Int
             | QuitCmd

  readInput : (prompt : String) -> Command Input
  readInput prompt
     = do PutStr prompt
          answer <- GetLine
          if toLower answer == "quit"
             then Pure QuitCmd
             else Pure (Answer (cast answer))

  quiz : Stream Int -> (score : Nat) -> ConsoleIO Nat
  quiz (num1 :: num2 :: nums) score
     = do PutStr ("Score so far: " ++ show score ++ "\n")
          input <- readInput (show num1 ++ " * " ++ show num2 ++ "? ")
          case input of
               Answer answer => if answer == num1 * num2
                                   then correct nums score
                                   else wrong nums (num1 * num2) score
               QuitCmd => Quit score

partial
forever : Fuel
forever = More forever

partial
main : IO ()
main = do seed <- time
          Just score <- run forever (quiz (arithInputs (fromInteger seed)) 0)
               | Nothing => putStrLn "Ran out of fuel"
          putStrLn ("Final score: " ++ show score)

ext: idr


text:
module Language.LSP.CodeAction.GenerateDef

import Core.Context
import Core.Core
import Core.Env
import Core.Metadata
import Core.UnifyState
import Data.String
import Idris.REPL.Opts
import Idris.Resugar
import Idris.Syntax
import Language.JSON
import Language.LSP.CodeAction
import Language.LSP.CodeAction.Utils
import Language.LSP.Message
import Parser.Unlit
import Server.Configuration
import Server.Log
import Server.Utils
import TTImp.Interactive.GenerateDef
import TTImp.TTImp
import TTImp.TTImp.Functor

printClause : Ref Ctxt Defs
           => Ref Syn SyntaxInfo
           => Maybe String -> Nat -> ImpClause -> Core String
printClause l i (PatClause _ lhsraw rhsraw) = do
  lhs <- pterm $ map defaultKindedName lhsraw
  rhs <- pterm $ map defaultKindedName rhsraw
  pure (relit l (pack (replicate i ' ') ++ show lhs ++ " = " ++ show rhs))
printClause l i (WithClause _ lhsraw wvraw prf flags csraw) = do
  lhs <- pterm $ map defaultKindedName lhsraw
  wval <- pterm $ map defaultKindedName wvraw
  cs <- traverse (printClause l (i + 2)) csraw
  pure (relit l ((pack (replicate i ' ')
         ++ show lhs
         ++ " with (" ++ show wval ++ ")"
         ++ maybe "" (\ nm => " proof " ++ show nm) prf
         ++ "\n"))
         ++ showSep "\n" cs)
printClause l i (ImpossibleClause _ lhsraw) = do
  do lhs <- pterm $ map defaultKindedName lhsraw
     pure (relit l (pack (replicate i ' ') ++ show lhs ++ " impossible"))

number : Nat -> List a -> List (Nat, a)
number n [] = []
number n (x :: xs) = (n,x) :: number (S n) xs

export
generateDef : Ref LSPConf LSPConfiguration
            => Ref MD Metadata
            => Ref Ctxt Defs
            => Ref UST UState
            => Ref Syn SyntaxInfo
            => Ref ROpts REPLOpts
            => CodeActionParams -> Core (List CodeAction)
generateDef params = do
  logI GenerateDef "Checking for \{show params.textDocument.uri} at \{show params.range}"
  withSingleLine GenerateDef params (pure []) $ \line => do
    withMultipleCache GenerateDef params GenerateDef $ do

      defs <- branch
      Just (_, n, _, _) <- findTyDeclAt (\p, n => onLine line p)
        | Nothing => do logD GenerateDef "No name found at line \{show line}"
                        pure []
      logD CaseSplit "Found type declaration \{show n}"

      fuel <- gets LSPConf searchLimit
      solutions <- case !(lookupDefExact n defs.gamma) of
        Just None => do
           catch (do searchdefs@((fc, _) :: _) <- makeDefN (\p, n => onLine line p) fuel n
                       | _ => pure []
                     let l : Nat = integerToNat $ cast $ startCol (toNonEmptyFC fc)
                     Just srcLine <- getSourceLine (line + 1)
                       | Nothing => do logE GenerateDef "Source line \{show line} not found"
                                       pure []
                     let (markM, srcLineUnlit) = isLitLine srcLine
                     for searchdefs $ \(_, cs) => do
                       traverse (printClause markM l) cs)
                 (\case Timeout _ => do logI GenerateDef "Timed out"
                                        pure []
                        err => do logC GenerateDef "Unexpected error while searching"
                                  throw err)
        Just _ => do logD GenerateDef "There is already a definition for \{show n}"
                     pure []
        Nothing => do logD GenerateDef "Couldn't find type declaration at line \{show line}"
                      pure []

      put Ctxt defs

      let docURI = params.textDocument.uri
      let rng = MkRange (MkPosition (line + 1) 0) (MkPosition (line + 1) 0) -- insert

      actions <- for (number 1 solutions) $ \(i,funcDef) => do
        let lastLine = fromMaybe "" (last' funcDef)
        let edit = MkTextEdit rng (String.unlines funcDef ++ "\n") -- extra newline
        let workspaceEdit = MkWorkspaceEdit
              { changes           = Just (singleton docURI [edit])
              , documentChanges   = Nothing
              , changeAnnotations = Nothing
              }
        pure $ MkCodeAction
          { title = "Generate definition #\{show i} as ~ \{strSubstr 0 50 lastLine} ..."
          , kind        = Just RefactorRewrite
          , diagnostics = Just []
          , isPreferred = Just False
          , disabled    = Nothing
          , edit        = Just workspaceEdit
          , command     = Nothing
          , data_       = Nothing
          }
      -- TODO: retrieve the line length efficiently
      pure [(MkRange (MkPosition line 0) (MkPosition line 1000), actions)]


text:
module IdrisWeb.Common.Random.RandC
-- Simple binding to a simple C random number library

%link C "rand_c.o"
%include C "rand_c.h"

getRandom : Int -> Int -> IO Int
getRandom min max = mkForeign (FFun "random_number" [FInt, FInt] FInt) min max

{-
-- Quick test harness
main : IO ()
main = do
  rand1 <- getRandom 100 1005
  rand2 <- getRandom 1200000 1230423
  putStrLn $ "random 1: " ++ (show rand1) ++ ", random 2: " ++ (show rand2)
  -}

max_stars_repo_name: idris-hackers/IdrisWeb

max_issues_repo_name: idris-hackers/IdrisWeb

max_forks_repo_name: idris-hackers/IdrisWeb


text:
module permutation_with_constructors

import Data.Vect
import congruence

%access public export
%default total

--- Goal - To define permutations with constructors

data PermC : Nat -> Type where
    Idt : (n : Nat) -> PermC n -- Identity permutation
    Swap : (n : Nat) -> (pos : Fin n) -> (PermC n)
{-
    Flip : (n : Nat) -> PermC n -- [1 2 3 ... n]-> [2 1 3 ... n]
    Shift : (n : Nat) -> PermC n -- [1 2 3 .. n] -> [n 1 2 .. (n-1)]
-}
    CPerm : (n : Nat) -> PermC n -> PermC n -> PermC n

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

||| Method to apply the permutation on a vector

applyPerm : (n : Nat) -> (typ : Type) -> (PermC n) -> (Vect n typ) -> (Vect n typ)

applyPerm Z typ perm v = v
applyPerm (S Z) typ perm v = v
applyPerm (S (S k)) typ (Idt (S (S k))) v = v

applyPerm (S (S k)) typ (Swap (S (S k)) FZ)  v =
    (index (FS FZ) v) :: ( (index FZ v) :: (tail(tail v)))

applyPerm (S (S k)) typ (Swap (S (S k)) (FS pos)) (a :: v) =
    a :: (applyPerm (S k) typ (Swap (S k) pos) v)
--applyPerm (S (S k)) t (Flip (S (S k))) v = (index (FS FZ) v) :: ( (index FZ v) :: (tail(tail v)))
--applyPerm (S (S k)) t (Shift (S (S k))) v = reverse( (index FZ v) :: (reverse (tail v)))

applyPerm n typ (CPerm n f g) v = applyPerm n typ f (applyPerm n typ g v)

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

||| Proof that applyperm respects composition

applyPerm_Comp : (n : Nat) -> (typ : Type) -> (f, g : PermC n) -> (v : Vect n typ) ->
                 ( ((applyPerm n typ (CPerm n f g) ) v) = applyPerm n typ f (applyPerm n typ g v))

applyPerm_Comp Z typ p q v = Refl
applyPerm_Comp (S Z) typ p q v = Refl
applyPerm_Comp (S (S k)) typ p q v = Refl

{-
||| The permutation which shifts k times

many_shifts : (n : Nat) -> (k : Nat) -> (PermC n)
many_shifts n Z = Idt n
many_shifts n (S k) = CPerm n (Shift n) (many_shifts n k)
-}

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

||| viewing a permutation of n elements as a permutation of (n + 1) elements with the first element
||| not moved

includePerm : (n : Nat) -> (PermC n) -> (PermC (S n))
includePerm Z perm = (Idt (S Z))
includePerm (S Z) perm = (Idt (S (S Z)))
includePerm n (Idt n) = Idt (S n)
includePerm n (Swap n pos) = Swap (S n) (FS pos)
--includePerm (S (S k)) (Flip (S (S k))) = Flip (S (S (S k)))
--includePerm (S (S k)) (Shift (S (S k))) = ?rhs
includePerm n (CPerm n f g) = CPerm (S n) (includePerm n f) (includePerm n g)

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

appSwap : (n : Nat) -> (typ : Type) -> (k : Fin n) -> (Vect n typ) -> (Vect n typ)
appSwap n typ k v = applyPerm n typ (Swap n k) v

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

||| auxilliary proof - a map from Fin Z to Void
aux_pf_1 : Fin Z -> Void
aux_pf_1 k impossible

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

||| swap is the inverse of itself
Self_inv_swap : (n : Nat) -> (typ : Type) -> (k : (Fin n)) -> (v : (Vect n typ))->
                ((((appSwap n typ k) . (appSwap n typ k)) v) = v)

Self_inv_swap Z typ k v = Refl
Self_inv_swap (S Z) typ k v = Refl
Self_inv_swap (S (S n)) typ FZ (a :: b :: v) = Refl
Self_inv_swap (S (S n)) typ (FS k) (a :: v) =
     (rewrite (Self_inv_swap (S n) typ k v) in Refl)

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

Is_Left_Inv : (n : Nat) -> (typ : Type) -> (f : ((Vect n typ) -> (Vect n typ)) ) ->
              (g : ((Vect n typ) -> (Vect n typ)) ) -> Type
Is_Left_Inv n typ f g = ( (v : (Vect n typ)) -> ( ((g . f) v) = v))

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

Is_Right_Inv : (n : Nat) -> (typ : Type) -> (f : ((Vect n typ) -> (Vect n typ)) ) ->
               (g : ((Vect n typ) -> (Vect n typ)) ) -> Type
Is_Right_Inv n typ f g = ( (v : (Vect n typ)) -> ( ((f . g) v) = v))

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

Is_Inv : (n : Nat) -> (typ : Type) -> (f : ((Vect n typ) -> (Vect n typ)) ) ->
         (g : ((Vect n typ) -> (Vect n typ)) ) -> Type
Is_Inv n typ f g = ( (Is_Left_Inv n typ f g) , (Is_Right_Inv n typ f g))
------------------------------------------------------------------------------------------

||| (left) Inv(f.h) = (Inv h).(Inv f)

Left_Inv_comp : (n : Nat) -> (typ : Type) ->
                (f, g, h, k : ((Vect n typ) -> (Vect n typ)) ) ->
                (Is_Left_Inv n typ f g) -> (Is_Left_Inv n typ h k) ->
                (Is_Left_Inv n typ (f . h) (k . g))

Left_Inv_comp n typ f g h k pf_fg pf_hk = pf_3 where

    pf_1 : (v : (Vect n typ)) -> ((g (f (h v))) = (h v) )
    pf_1 v = pf_fg (h v)

    pf_2 : (v : (Vect n typ)) -> ( (k (g (f (h v)))) = (k (h v)) )
    pf_2 v = congruence (Vect n typ) (Vect n typ)
                        ((g . f . h) v) (h v) k (pf_1 v)

    pf_3 : (v : (Vect n typ)) -> ( (k (g (f (h v)))) = v )
    pf_3 v = trans (pf_2 v) (pf_hk v)

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

||| (right) Inv(f.h) = (Inv h).(Inv f)

Right_Inv_comp : (n : Nat) -> (typ : Type) ->
                 (f, g, h, k : ((Vect n typ) -> (Vect n typ)) ) ->
                 (Is_Right_Inv n typ f g) -> (Is_Right_Inv n typ h k) ->
                 (Is_Right_Inv n typ (f . h) (k . g))

Right_Inv_comp n typ f g h k pf_fg pf_hk = pf_3 where

   pf_1 : (v : (Vect n typ)) -> ((h (k (g v))) = (g v))
   pf_1 v = pf_hk (g v)

   pf_2 : (v : (Vect n typ)) -> ((f (h (k (g v)))) = (f (g v)) )
   pf_2 v = congruence (Vect n typ) (Vect n typ)
                       ((h . k . g) v) (g v) f (pf_1 v)

   pf_3 : (v : (Vect n typ)) -> ( (f (h (k (g v)))) = v)
   pf_3 v = trans (pf_2 v) (pf_fg v)

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

||| Inverse of f.g is (inv g).(inv f)

Inv_comp : (n : Nat) -> (typ : Type) ->
           (f, g, h, k : ((Vect n typ) -> (Vect n typ)) ) ->
           (Is_Inv n typ f g) -> (Is_Inv n typ h k) ->
           (Is_Inv n typ (f . h) (k . g))

Inv_comp n typ f g h k pf_fg pf_hk = let
    pf_left_fg = fst pf_fg
    pf_right_fg = snd pf_fg
    pf_left_hk = fst pf_hk
    pf_right_hk = snd pf_hk
    pf_left = Left_Inv_comp n typ f g h k pf_left_fg pf_left_hk
    pf_right = Right_Inv_comp n typ f g h k pf_right_fg pf_right_hk
    in
    (pf_left, pf_right)

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

||| The type of bijections

IsBijection : (n : Nat) -> (typ : Type) -> (f : (Vect n typ) -> (Vect n typ) ) -> Type
IsBijection n typ f =
    (g : ((Vect n typ) -> (Vect n typ)) ** ( Is_Inv n typ f g))

||| Proof that permutations are bijections

PermC_are_bij : (n : Nat) -> (typ : Type) -> (perm : PermC n) ->
                (IsBijection n typ (applyPerm n typ perm) )

PermC_are_bij Z typ perm = (idZ ** (fun, fun)) where
    idZ : (Vect Z typ) -> (Vect Z typ)
    idZ = applyPerm Z typ perm
    fun : (v : (Vect Z typ)) -> (v = v)
    fun v = Refl

PermC_are_bij (S Z) typ perm = (idSZ ** (fun, fun)) where
    idSZ : (Vect (S Z) typ) -> (Vect (S Z) typ)
    idSZ = applyPerm (S Z) typ (Idt (S Z))
    fun : (v : (Vect (S Z) typ)) -> (v = v)
    fun v = Refl

PermC_are_bij (S (S k)) typ (Idt (S (S k))) = (idn ** (fun, fun)) where
    idn : (Vect (S (S k)) typ) -> (Vect (S (S k)) typ)
    idn = applyPerm (S (S k)) typ (Idt (S (S k)))
    fun : (v : (Vect (S (S k)) typ)) -> (v = v)
    fun v = Refl

PermC_are_bij  (S (S k)) typ (Swap (S (S k)) pos) =
    ( (appSwap (S (S k)) typ pos) ** (fun, fun)) where
        fun : (v : Vect (S (S k)) typ ) ->
              ((((appSwap (S (S k)) typ pos) . (appSwap (S (S k)) typ pos)) v) = v)
        fun v = (Self_inv_swap (S (S k)) typ pos v)

PermC_are_bij n typ (CPerm n f h) = let
    inv_f = PermC_are_bij n typ f
    g = fst inv_f
    pf_fg = snd inv_f
    pf_fg_left = fst pf_fg
    pf_fg_right = snd pf_fg
    f1 = (applyPerm n typ f)

    inv_h = PermC_are_bij n typ h
    k = fst inv_h
    pf_hk = snd inv_h
    pf_hk_left = fst pf_hk
    pf_hk_right = snd pf_hk
    h1 = (applyPerm n typ h)

    pf_com = applyPerm_Comp n typ f h
    pf_com_1 = \v => (congruence (Vect n typ) (Vect n typ)
        (applyPerm n typ (CPerm n f h) v)
        (applyPerm n typ f (applyPerm n typ h v))
        (k . g) (pf_com v) )

    pf_left_1 =
        Left_Inv_comp n typ f1 g h1 k pf_fg_left pf_hk_left

    pf_left = \v => (trans (pf_com_1 v) (pf_left_1 v))

    pf_right_1 =
        Right_Inv_comp n typ f1 g h1 k pf_fg_right pf_hk_right

    pf_right = \v => (trans (pf_com ((k . g) v) ) (pf_right_1 v) )

    in
    ( (k . g) ** (pf_left , pf_right))


text:
module JS.Marshall

import Control.Monad.Either
import Data.SOP
import JS.Inheritance
import JS.Util

--------------------------------------------------------------------------------
--          Marshalling from and to JS
--------------------------------------------------------------------------------

||| Interface supporting the use of a value as an
||| argument in a foreign function call.
|||
||| Implementations for primitives and external type should be
||| done using `believe_me`, as they are alredy in the correct
||| representation. Idris2 types should be converted to primitives
||| or external constants first.
public export
interface ToFFI a ffiRepr | a where
  toFFI : a -> ffiRepr

export
ToFFI AnyPtr AnyPtr where toFFI = id

export
ToFFI Bits8 Bits8 where toFFI = id

export
ToFFI Bits16 Bits16 where toFFI = id

export
ToFFI Bits32 Bits32 where toFFI = id

export
ToFFI Bits64 Bits64 where toFFI = id

export
ToFFI Int8 Int8 where toFFI = id

export
ToFFI Int16 Int16 where toFFI = id

export
ToFFI Int32 Int32 where toFFI = id

export
ToFFI Int64 Int64 where toFFI = id

export
ToFFI Int Int where toFFI = id

export
ToFFI Char Char where toFFI = id

export
ToFFI Integer Integer where toFFI = id

export
ToFFI Double Double where toFFI = id

export
ToFFI String String where toFFI = id

export
ToFFI WindowProxy WindowProxy where toFFI = id

||| Interface supporting the use of a value as a
||| return type in a foreign function call.
public export
interface FromFFI a ffiRepr | a where
  fromFFI : ffiRepr -> Maybe a

export
FromFFI AnyPtr AnyPtr where fromFFI = Just

export
FromFFI Bits8 Bits8 where fromFFI = Just

export
FromFFI Bits16 Bits16 where fromFFI = Just

export
FromFFI Bits32 Bits32 where fromFFI = Just

export
FromFFI Bits64 Bits64 where fromFFI = Just

export
FromFFI Int8 Int8 where fromFFI = Just

export
FromFFI Int16 Int16 where fromFFI = Just

export
FromFFI Int32 Int32 where fromFFI = Just

export
FromFFI Int64 Int64 where fromFFI = Just

export
FromFFI Char Char where fromFFI = Just

export
FromFFI Int Int where fromFFI = Just

export
FromFFI Integer Integer where fromFFI = Just

export
FromFFI Double Double where fromFFI = Just

export
FromFFI String String where fromFFI = Just

export
FromFFI WindowProxy WindowProxy where fromFFI = Just

export
tryFromFFI : FromFFI a ffiRepr => (fun : Lazy String) -> ffiRepr -> JSIO a
tryFromFFI fun ptr = case fromFFI ptr of
                          Nothing => throwError $ CastErr fun ptr
                          Just v  => pure v

export
tryJS : FromFFI a ffiRepr => (fun : Lazy String) -> PrimIO ffiRepr -> JSIO a
tryJS fun prim = primJS prim >>= tryFromFFI fun


text:
module Starknet.Syscall

import Common
import Common.Memory

-- https://github.com/starkware-libs/cairo-lang/blob/master/src/starkware/starknet/common/syscalls.cairo

export
%foreign
    "imports:starkware.starknet.common.storage normalize_address"
    "linear_implicits:range_check_ptr"
    """
    code:
    func Starknet_Syscall_normalizeAddress(range_check_ptr,address) -> (result, range_check_ptr):
        let (res) = normalize_address{range_check_ptr = range_check_ptr}(address)
        return (res, range_check_ptr)
    end
    """
normalizeAddress : (address: Felt) -> (Felt)

%foreign
    "imports:starkware.starknet.common.syscalls storage_read"
    "untupled:(_,_)"
    """
    code:
    func Starknet_Syscall_storageReadPrim(address, syscall_ptr) -> (syscall_ptr, result):
        let syscall_ptr_ = cast(syscall_ptr, felt*)
        let (res) = storage_read{syscall_ptr = syscall_ptr_}(address)
        return (cast(syscall_ptr_, felt), res)
    end
    """
storageReadPrim : (address: Felt) -> PrimCairo Felt

public export %inline
storageRead : Felt -> Cairo Felt
storageRead address = fromPrimCairo (storageReadPrim address)

%foreign
    "imports:starkware.starknet.common.syscalls storage_write"
    """
    code:
    func Starknet_Syscall_storageWritePrim(address, value, syscall_ptr) -> (syscall_ptr):
        let syscall_ptr_ = cast(syscall_ptr, felt*)
        storage_write{syscall_ptr = syscall_ptr_}(address,value)
        return (cast(syscall_ptr_, felt))
    end
    """
storageWritePrim : (address: Felt) -> (value: Felt) -> PrimCairoUnit

public export %inline
storageWrite : Felt -> Felt -> Cairo ()
storageWrite address value = fromPrimCairoUnit (storageWritePrim address value)

%foreign
    "imports:starkware.starknet.common.syscalls emit_event"
    """
    code:
    func Starknet_Syscall_emitEventPrim(keys_len, keys, data_len, data, syscall_ptr) -> (syscall_ptr):
        let syscall_ptr_ = cast(syscall_ptr, felt*)
        emit_event{syscall_ptr = syscall_ptr_}(keys_len, cast(keys, felt*), data_len, cast(data, felt*))
        return (cast(syscall_ptr_, felt))
    end
    """
emitEventPrim : Felt -> CairoPtr Memory -> Felt -> CairoPtr Memory -> PrimCairoUnit

public export %inline
emitEvent : Felt -> CairoPtr Memory -> Felt -> CairoPtr Memory -> Cairo () -- keys and data should be felt*
emitEvent keys_len keys data_len data_ = fromPrimCairoUnit (emitEventPrim keys_len keys data_len data_)

%foreign
    "imports:starkware.starknet.common.syscalls get_block_timestamp"
    "untupled:(_,_)"
    """
    code:
    func Starknet_Syscall_getBlockTimestampPrim(syscall_ptr) -> (syscall_ptr, result):
        let syscall_ptr_ = cast(syscall_ptr, felt*)
        let (result) = get_block_timestamp{syscall_ptr = syscall_ptr_}()
        return (cast(syscall_ptr_, felt), result)
    end
    """
getBlockTimestampPrim : PrimCairo Felt

public export %inline
getBlockTimestamp : Cairo Felt
getBlockTimestamp = fromPrimCairo getBlockTimestampPrim

max_stars_repo_name: skyro-compiler/skyro

max_issues_repo_name: skyro-compiler/skyro

max_forks_repo_name: skyro-compiler/skyro


text:
module Web.Internal.IndexedDBTypes

import JS

%default total

--------------------------------------------------------------------------------
--          Enums
--------------------------------------------------------------------------------

namespace IDBRequestReadyState

  public export
  data IDBRequestReadyState = Pending | Done

  public export
  Show IDBRequestReadyState where
    show Pending = "pending"
    show Done = "done"

  public export
  Eq IDBRequestReadyState where
    (==) = (==) `on` show

  public export
  Ord IDBRequestReadyState where
    compare = compare `on` show

  public export
  read : String -> Maybe IDBRequestReadyState
  read "pending" = Just Pending
  read "done" = Just Done
  read _ = Nothing

  public export
  fromString :  (s : String)
             -> {auto 0 _ : IsJust (IDBRequestReadyState.read s)}
             -> IDBRequestReadyState
  fromString s = fromJust $ read s

  export
  ToFFI IDBRequestReadyState String where
    toFFI = show

  export
  FromFFI IDBRequestReadyState String where
    fromFFI = read

namespace IDBTransactionDurability

  public export
  data IDBTransactionDurability = Default | Strict | Relaxed

  public export
  Show IDBTransactionDurability where
    show Default = "default"
    show Strict = "strict"
    show Relaxed = "relaxed"

  public export
  Eq IDBTransactionDurability where
    (==) = (==) `on` show

  public export
  Ord IDBTransactionDurability where
    compare = compare `on` show

  public export
  read : String -> Maybe IDBTransactionDurability
  read "default" = Just Default
  read "strict" = Just Strict
  read "relaxed" = Just Relaxed
  read _ = Nothing

  public export
  fromString :  (s : String)
             -> {auto 0 _ : IsJust (IDBTransactionDurability.read s)}
             -> IDBTransactionDurability
  fromString s = fromJust $ read s

  export
  ToFFI IDBTransactionDurability String where
    toFFI = show

  export
  FromFFI IDBTransactionDurability String where
    fromFFI = read

namespace IDBCursorDirection

  public export
  data IDBCursorDirection = Next | Nextunique | Prev | Prevunique

  public export
  Show IDBCursorDirection where
    show Next = "next"
    show Nextunique = "nextunique"
    show Prev = "prev"
    show Prevunique = "prevunique"

  public export
  Eq IDBCursorDirection where
    (==) = (==) `on` show

  public export
  Ord IDBCursorDirection where
    compare = compare `on` show

  public export
  read : String -> Maybe IDBCursorDirection
  read "next" = Just Next
  read "nextunique" = Just Nextunique
  read "prev" = Just Prev
  read "prevunique" = Just Prevunique
  read _ = Nothing

  public export
  fromString :  (s : String)
             -> {auto 0 _ : IsJust (IDBCursorDirection.read s)}
             -> IDBCursorDirection
  fromString s = fromJust $ read s

  export
  ToFFI IDBCursorDirection String where
    toFFI = show

  export
  FromFFI IDBCursorDirection String where
    fromFFI = read

namespace IDBTransactionMode

  public export
  data IDBTransactionMode = Readonly | Readwrite | Versionchange

  public export
  Show IDBTransactionMode where
    show Readonly = "readonly"
    show Readwrite = "readwrite"
    show Versionchange = "versionchange"

  public export
  Eq IDBTransactionMode where
    (==) = (==) `on` show

  public export
  Ord IDBTransactionMode where
    compare = compare `on` show

  public export
  read : String -> Maybe IDBTransactionMode
  read "readonly" = Just Readonly
  read "readwrite" = Just Readwrite
  read "versionchange" = Just Versionchange
  read _ = Nothing

  public export
  fromString :  (s : String)
             -> {auto 0 _ : IsJust (IDBTransactionMode.read s)}
             -> IDBTransactionMode
  fromString s = fromJust $ read s

  export
  ToFFI IDBTransactionMode String where
    toFFI = show

  export
  FromFFI IDBTransactionMode String where
    fromFFI = read

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

export data IDBCursor : Type where [external]

export
ToFFI IDBCursor IDBCursor where toFFI = id

export
FromFFI IDBCursor IDBCursor where fromFFI = Just

export
SafeCast IDBCursor where
  safeCast = unsafeCastOnPrototypeName "IDBCursor"

export data IDBCursorWithValue : Type where [external]

export
ToFFI IDBCursorWithValue IDBCursorWithValue where toFFI = id

export
FromFFI IDBCursorWithValue IDBCursorWithValue where fromFFI = Just

export
SafeCast IDBCursorWithValue where
  safeCast = unsafeCastOnPrototypeName "IDBCursorWithValue"

export data IDBDatabase : Type where [external]

export
ToFFI IDBDatabase IDBDatabase where toFFI = id

export
FromFFI IDBDatabase IDBDatabase where fromFFI = Just

export
SafeCast IDBDatabase where
  safeCast = unsafeCastOnPrototypeName "IDBDatabase"

export data IDBFactory : Type where [external]

export
ToFFI IDBFactory IDBFactory where toFFI = id

export
FromFFI IDBFactory IDBFactory where fromFFI = Just

export
SafeCast IDBFactory where
  safeCast = unsafeCastOnPrototypeName "IDBFactory"

export data IDBIndex : Type where [external]

export
ToFFI IDBIndex IDBIndex where toFFI = id

export
FromFFI IDBIndex IDBIndex where fromFFI = Just

export
SafeCast IDBIndex where
  safeCast = unsafeCastOnPrototypeName "IDBIndex"

export data IDBKeyRange : Type where [external]

export
ToFFI IDBKeyRange IDBKeyRange where toFFI = id

export
FromFFI IDBKeyRange IDBKeyRange where fromFFI = Just

export
SafeCast IDBKeyRange where
  safeCast = unsafeCastOnPrototypeName "IDBKeyRange"

export data IDBObjectStore : Type where [external]

export
ToFFI IDBObjectStore IDBObjectStore where toFFI = id

export
FromFFI IDBObjectStore IDBObjectStore where fromFFI = Just

export
SafeCast IDBObjectStore where
  safeCast = unsafeCastOnPrototypeName "IDBObjectStore"

export data IDBOpenDBRequest : Type where [external]

export
ToFFI IDBOpenDBRequest IDBOpenDBRequest where toFFI = id

export
FromFFI IDBOpenDBRequest IDBOpenDBRequest where fromFFI = Just

export
SafeCast IDBOpenDBRequest where
  safeCast = unsafeCastOnPrototypeName "IDBOpenDBRequest"

export data IDBRequest : Type where [external]

export
ToFFI IDBRequest IDBRequest where toFFI = id

export
FromFFI IDBRequest IDBRequest where fromFFI = Just

export
SafeCast IDBRequest where
  safeCast = unsafeCastOnPrototypeName "IDBRequest"

export data IDBTransaction : Type where [external]

export
ToFFI IDBTransaction IDBTransaction where toFFI = id

export
FromFFI IDBTransaction IDBTransaction where fromFFI = Just

export
SafeCast IDBTransaction where
  safeCast = unsafeCastOnPrototypeName "IDBTransaction"

export data IDBVersionChangeEvent : Type where [external]

export
ToFFI IDBVersionChangeEvent IDBVersionChangeEvent where toFFI = id

export
FromFFI IDBVersionChangeEvent IDBVersionChangeEvent where fromFFI = Just

export
SafeCast IDBVersionChangeEvent where
  safeCast = unsafeCastOnPrototypeName "IDBVersionChangeEvent"

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

export data IDBDatabaseInfo : Type where [external]

export
ToFFI IDBDatabaseInfo IDBDatabaseInfo where toFFI = id

export
FromFFI IDBDatabaseInfo IDBDatabaseInfo where fromFFI = Just

export data IDBIndexParameters : Type where [external]

export
ToFFI IDBIndexParameters IDBIndexParameters where toFFI = id

export
FromFFI IDBIndexParameters IDBIndexParameters where fromFFI = Just

export data IDBObjectStoreParameters : Type where [external]

export
ToFFI IDBObjectStoreParameters IDBObjectStoreParameters where toFFI = id

export
FromFFI IDBObjectStoreParameters IDBObjectStoreParameters where fromFFI = Just

export data IDBTransactionOptions : Type where [external]

export
ToFFI IDBTransactionOptions IDBTransactionOptions where toFFI = id

export
FromFFI IDBTransactionOptions IDBTransactionOptions where fromFFI = Just

export data IDBVersionChangeEventInit : Type where [external]

export
ToFFI IDBVersionChangeEventInit IDBVersionChangeEventInit where toFFI = id

export
FromFFI IDBVersionChangeEventInit IDBVersionChangeEventInit where fromFFI = Just


text:
module Main

import Effect.File
import Effect.State
import Effect.StdIO
import Control.IOExcept

FileIO : Type -> Type -> Type
FileIO st t
  = { [FILE_IO st, STDIO, 'Count ::: STATE Int] } Eff IO t

readFile : FileIO (OpenFile Read) (List String)
readFile = readAcc [] where
    readAcc : List String -> FileIO (OpenFile Read) (List String)
    readAcc acc = do e <- eof
                     if (not e)
                        then do str <- readLine
                                'Count :- put (!('Count :- get) + 1)
                                readAcc (str :: acc)
                        else return (reverse acc)

testFile : FileIO () ()
testFile = case !(open "testFile" Read) of
                 True => do putStrLn (show !readFile)
                            close
                            putStrLn (show !('Count :- get))
                 False => putStrLn ("Error!")

main : IO ()
main = run testFile

max_stars_repo_name: silky/idris-demos

max_issues_repo_name: silky/idris-demos

max_forks_repo_name: silky/idris-demos


text:
module Core.Evaluation

import General

import Core.Variable
import Core.Term

%access export

-- 8_   _8  o8o  YY8YY  oYYo 0   0 8YYYo  o8o  YY8YY YY8YY 8YYYY 8YYYo 8o  0 oYYYo
-- 8"o_o"8 8   8   0   0   " 8___8 8___P 8   8   0     0   8___  8___P 8Yo 8 %___
-- 0  8  0 8YYY8   0   0   , 8"""8 8"""  8YYY8   0     0   8"""  8""Yo 8 Yo8 `"""p
-- 0     0 0   0   0    YooY 0   0 0     0   0   0     0   8oooo 0   0 0   8 YoooY

mutual
	private matchPattern : Pattern -> Term -> Maybe (List Term)
	private matchPatterns : (List (Plict,Pattern)) -> (List (Plict,Term)) -> Maybe (List Term)
	private matchClauses : (List Clause) -> (List (Plict,Term)) -> Maybe Term

	matchPattern (VarPat _) v = Just [v]
	matchPattern (ConPat c ps) (Con c' as) with (c == c')
		| True = matchPatterns ps as
	matchPattern (AssertionPat _) _ = Just []
	matchPattern _ _ = Nothing

	matchPatterns [] [] = Just []
	matchPatterns ((plic,p) :: ps) ((plic',m) :: ms) with (plic == plic')
		| True = do
			vs <- matchPattern p m
			vs' <- matchPatterns ps ms
			pure $ vs ++ vs'
	matchPatterns _ _ = Nothing

-- 8_   _8  o8o  YY8YY  oYYo 0   0  oYYo 0     o8o  0   0 oYYYo 8YYYY oYYYo
-- 8"o_o"8 8   8   0   0   " 8___8 0   " 0    8   8 0   0 %___  8___  %___
-- 0  8  0 8YYY8   0   0   , 8"""8 0   , 0    8YYY8 0   0 `"""p 8"""  `"""p
-- 0     0 0   0   0    YooY 0   0  YooY 8ooo 0   0 "ooo" YoooY 8oooo YoooY

matchClauses [] _ = Nothing
matchClauses (NewClause psc sc :: cs) ms
	= case matchPatterns [ (Expl, p) | p <- descope Name psc ] ms of
		Nothing => matchClauses cs ms
		Just vs => Just (instantiate sc (removeByDummies (names psc) vs))

-- 8YYYY 0   0  o8o  0
-- 8___  0   0 8   8 0
-- 8"""  "o o" 8YYY8 0
-- 8oooo  "8"  0   0 8ooo

-- Standard Eager Evaluation
Eval (Environment FullName Term) Term where
	eval (Meta i) = pure $ Meta i
	eval (Var x) = pure $ Var x

	eval (DottedVar mdl var) = do
		env <- environment
		case lookup (mdl,var) env of
			Nothing => throw $ "Unknown constant/defined term: " ++ show (DottedVar mdl var)
			Just m  => eval m

	eval (AbsoluteDottedVar mdl var) = do
		env <- environment
		case lookup (mdl,var) env of
			Nothing => throw $ "Unknown constant/defined term: " ++ show (AbsoluteDottedVar mdl var)
			Just m  => eval m

	eval (Ann m _) = eval m
	eval Star = pure Star
	eval (Pi plic a sc) = pure $ Pi plic a sc
	eval (Lam plic sc) = pure $ Lam plic sc
	eval (App plic f a) = do
		ef <- eval f
		ea <- eval a
		case ef of
			Lam plic' sc => if (plic == plic')
				then eval (instantiate sc [ea])
				else pure $ App plic ef ea -- should not happen
			_ => pure $ App plic ef ea

	eval (Con c aas) = do
		eas <- Traversable.for aas $ \(plic, a) => do
			a' <- eval a
			pure (plic, a')
		pure $ Con c eas

	eval (Case ms mot cs) = do
		ems <- Traversable.for ms eval
		case matchClauses cs [ (Expl,em) | em <- ems ] of
			Nothing => if any (\p => case p of { (Con _ _) => False ; _ => True }) ems
				then pure (Case ms mot cs)
				else throw $ "Incomplete pattern match: " ++ show (Case ms mot cs)
			Just b  => eval b

	eval (RecordType tele) = pure $ RecordType tele

	eval (RecordCon fields) = RecordCon <$> sequence [ MkPair x <$> eval m | (x,m) <- fields ]

	eval (Project m x) = do
		em <- eval m
		case em of
			RecordCon fields => case lookup x fields of
				Nothing => throw $ "Unknown field '" ++ x ++ "' in record " ++ show (RecordCon fields)
				Just m' => pure m'
			m' => pure $ Project m' x

max_stars_repo_name: totalscript/totalscript

max_issues_repo_name: totalscript/totalscript

max_forks_repo_name: totalscript/totalscript


text:
import Data.Vect

{-
data Vect : Nat -> Type -> Type where
   Nil  : Vect Z a
   (::) : a -> Vect k a -> Vect (S k) a
-}

fourInts : Vect 4 Int
fourInts = [0, 1, 2, 3]

sixInts : Vect 6 Int
sixInts = [4, 5, 6, 7, 8, 9]

tenInts : Vect 10 Int
tenInts = fourInts ++ sixInts

--reverse fourInts

--map (\x => x+1) fourInts

max_stars_repo_name: wdomitrz/Coq-Exercises

max_issues_repo_name: wdomitrz/Coq-Exercises

max_forks_repo_name: wdomitrz/Coq-Exercises


text:
> module Nat.open_issues.Main

> %default total
> %auto_implicits off

> n : Nat
> -- n = 80

> -- %freeze n

> ns : List Nat
> ns = [1..n]

> postulate lemma : (m : Nat) -> 2 * (sum [1..m]) = m * (S m)

> q : 2 * (sum ns) = n * (S n)
> q = lemma n

> {-
> main : IO ()
> main = do putStrLn ("n           = " ++ show n)
>           putStrLn ("sum ns      = " ++ show (sum ns))
> -}

For small |n|, type checking time is roughly constant in |n| and
execution time is roughly linear in |n| as one would expect:

    n   | type check |  run
  ======|============|=======
  10000 |       5.7s | 0.006s
  20000 |       5.8s | 0.012s
  40000 |       6.0s | 0.028s
  80000 |       5.8s | 0.060s

But uncommenting the computation of |q| yields unacceptable type
checking times even for very small |n|:

    n   | type check |  run
  ======|============|=======
   10   |       6.0s | 0.002s
   20   |       5.7s | 0.002s
   40   |       7.6s | 0.002s
   80   |      29.7s | 0.002s
  160   |   11m55.0s | 0.002s
  320   |  243m22.0s | 0.002s
  640   |   killed!  |

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
data Vect : Nat -> Type -> Type where
     Nil : Vect Z a
     (::) : a -> Vect k a -> Vect (S k) a

%name Vect xs, ys, zs

my_cong : forall f . (x : a) -> (y : a) -> x = y -> f x = f y

append : Vect n a -> Vect m a -> Vect (n + m) a

lappend : (1 _ : List a) -> (1 _ : List a) -> List a

lappend1 : List a -> List a -> List a

lappend2 : List a -> List a -> List a
lappend2 [] ys = ?lappend2_rhs_1
lappend2 (x :: xs) ys = ?lappend2_rhs_2


text:
module Common.Pedersen

import Common

public export
%foreign
    "apStable:True"
    "linear_implicits:pedersen_ptr"
    """
    code:
    func Common_Pedersen_pedersenHash(pedersen_ptr, x, y) -> (result, pedersen_ptr):
        assert [pedersen_ptr] = x
        assert [pedersen_ptr + 1] = y
        return ([pedersen_ptr + 2], pedersen_ptr + 3)
    end
    """
pedersenHash : Felt -> Felt -> Felt


text:
module Derive.Enum

import Data.Nat -- LTE example

import public Derive.Common
%language ElabReflection

-- Tooling for basic interfaces of Enumeration types, e.g. data Foo = Biz | Baz
-- This should also support indexed enum types, because our operations are just
-- about the constructors.
-- Use of this module automatically imports Language.Reflection and requires
-- %language ElabReflection to be enabled below your imports.
-- Examples at module bottom

-- The extra constructor checks to ensure Enumeration type can add a fair chunk to
-- the compile time, best to place your types you're deriving for into a module
-- that doesn't change often.

checkList : List a -> List b -> Elab ()
checkList xs ys =
  let lenxs = length xs
      lenys = length ys
  in case compare lenxs lenys of
    LT => fail $ "Provided list is too short to exactly cover all constructors. "
             ++ "Given " ++ show lenxs ++ ", needs " ++ show lenys ++ " elements."
    GT => fail $ "Provided list is too long to exactly cover all constructors. "
             ++ "Given " ++ show lenxs ++ ", needs " ++ show lenys ++ " elements."
    EQ => pure ()

enumName : TTImp -> Maybe Name
enumName (IVar _ n) = Just n
enumName (IApp _ (IVar _ n) r) = Just n
enumName _ = Nothing

-- An enum type's constructors are all non-explicit or just an ivar, and its
-- type is either the first argument of an application or an ivar.
-- e.g. A : {g : Nat} -> Foo g
--      B : Foo Z
--      C : Foo Z
-- e.g. data Foo : Nat -> Type where
--      data Foo : Type where
isEnumType : Name -> Elab Bool
isEnumType n = do
    cons <- constructors n
    pure $ all isEnumCon (map snd cons)
  where
    isEnumCon : TTImp -> Bool
    isEnumCon (IPi _ _ ExplicitArg _ _ retty) = False
    isEnumCon (IPi _ _ _ _ _ retty) = isEnumCon retty
    isEnumCon _ = True -- we got to the end without explicit args

-- combine our checks into one spot:
-- 1. is a given TTImp representing a type
-- 2. do its constructors have no explicit arguments
checkEnumType : TTImp -> Elab Name
checkEnumType ttimp = do
  Just n <- pure $ enumName ttimp
    | _ => fail "Failed to resolve type name"
  guard !(isEnumType n) $ show n ++ " is not an enumeration type."
  pure n

export
%macro
showEnum : Elab (x -> String)
showEnum = do
    Just k <- goal
      | _ => fail "dsfsd"
    logTerm "fgsfds" 1 "goal" k
    Just (IPi _ _ _ _ ty `(String)) <- goal
      | _ => fail "Required type is not: x -> String"
    n <- checkEnumType ty
    cns <- conNames n
    -- cons <- constructors n
    -- traverse (logTerm "" 1 "blah") (map snd cons)
    check `(\lam => ~(ICase eFC `(lam) ty (clause <$> cns)))
    -- check `(\lam => "sdf")
  where
    clause : Name -> Clause
    clause n = PatClause eFC (IVar eFC n) (IPrimVal eFC (Str (nameStr n)))

export
%macro
eqEnum : Elab (x -> x -> Bool)
eqEnum = do
    Just (IPi _ _ _ _ ty1 (IPi _ _ _ _ ty2 `(Prelude.Basics.Bool))) <- goal
      | _ => fail "Required type is not: x -> x -> Bool"
    n1 <- checkEnumType ty1
    n2 <- checkEnumType ty2
    guard (nameStr n1 == nameStr n2) "Required type is not: x -> x -> Bool"
    conns <- conNames n1
    check `(\x,y => ~(casex conns `(x) `(y)))
  where
    -- pattern for a 'case': `(Biz => case ~y of Biz => True; _ => False)
    casey : (y : TTImp) -> (con : Name) -> Clause
    casey y con = PatClause eFC (IVar eFC con) $ ICase eFC y `(_)
      [ PatClause eFC (IVar eFC con) `(True)
      , PatClause eFC `( _ ) `(False)]
    -- `(case ~x of Biz => rpatterns y Biz; Baz => rpatterns y Baz)
    casex : (cons : List Name) -> (x : TTImp) -> (y : TTImp) -> TTImp
    casex cs x y = ICase eFC x `(_) (map (casey y) cs)
    {- casex: case x of
       casey:   Biz => case y of
                  Biz => True
                  _ => False -}

||| This orders enum constructors by their position in the datatype
||| data Foo = Biz | Baz     Biz < Baz
export
%macro
compareEnum : Elab (x -> x -> Ordering)
compareEnum = do
    Just (IPi _ _ _ _ ty1 (IPi _ _ _ _ ty2 `(Prelude.EqOrd.Ordering))) <- goal
      | _ => fail "Required type is not: x -> x -> Ordering"
    n1 <- checkEnumType ty1
    n2 <- checkEnumType ty2
    guard (nameStr n1 == nameStr n2) "Required type is not: x -> x -> Ordering"
    cns <- conNames n1
    clauses <- traverse clause (zip [0 .. intLength cns] cns)
    let toInt = \x => ICase eFC x `(_) clauses
    check `(\a,b => compare {ty=Int} ~(toInt `(a)) ~(toInt `(b)))
  where
    clause : (Int, Name) -> Elab Clause
    clause (i,n) = pure $ PatClause eFC (IVar eFC n) !(quote i)

||| Maps an Int value to each constructor.
||| Provide a more custom list to skip some elements. e.g.
||| enumTo ([0..12] ++ [14..30]) would skip assigning 13
export
%macro
enumTo : List Int -> Elab (x -> Int)
enumTo xs = do
    Just (IPi _ _ _ _ ty `(Int)) <- goal
      | _ => fail "Required type is not: x -> Int"
    n <- checkEnumType ty
    cons <- conNames n
    checkList xs cons
    clauses <- traverse clause (zip xs cons)
    check `(\lam => ~(ICase eFC `(lam) `(_) clauses))
  where
    clause : (a, Name) -> Elab Clause
    clause (i,n) = pure $ PatClause eFC (IVar eFC n) !(quote i)

||| Maps x's constructors to given List of Ints, resulting function yields
||| Nothing if given an Int that is not mapped.
export
%macro
enumFrom : List Int -> Elab (Int -> Maybe x)
enumFrom xs = do
    Just (IPi _ _ _ _ `(Int) `(Prelude.Types.Maybe ~(ty))) <- goal
      | _ => fail "Required type is not: Int -> Maybe x"
    n <- checkEnumType ty
    logTerm "enumfrom" 1 "ty" ty
    logTerm "enumfrom" 1 "nam" (IVar eFC n)
    cons <- conNames n
    checkList xs cons
    clauses <- traverse clause (zip xs cons)
    let catchall_clause =  [PatClause eFC `(_) `(Nothing)]
    check `(\lam => ~(ICase eFC `(lam) `(_) (clauses ++ catchall_clause)))
  where
    clause : (a, Name) -> Elab Clause
    clause (i,n) = do
      r <- quote i
      logTerm "enumfrom" 1 "clausenam" (IVar eFC n)
      logTerm "enumfrom" 1 "clausequot" r
      pure $ PatClause eFC r `(Just ~(IVar eFC n))

||| Maps x's constructors to given List of Ints, resulting function's behavior
||| is undefined if given an Int that is not mapped.
export
%macro
unsafeEnumFrom : List Int -> Elab (Int -> x)
unsafeEnumFrom xs = do
    Just (IPi _ _ _ _ `(Int) ty) <- goal
      | _ => fail "Required type is not: Int -> x"
    n <- checkEnumType ty
    cons <- conNames n
    checkList xs cons
    clauses <- traverse clause (zip xs cons)
    check `(\lam => assert_total $ ~(ICase eFC `(lam) `(_) clauses))
  where
    clause : (a, Name) -> Elab Clause
    clause (i,n) = pure $ PatClause eFC !(quote i) (IVar eFC n)

-------------------------------------------------
-- Examples
-------------------------------------------------

-- some things are ' to avoid namespace clashes, private isn't as private
-- as it seems

-- simple enumeration type, the main target of this module
data Foo = Biz | Baz

-- indexed enumeration type
data IFoo : Nat -> Type where
  NilFoo : IFoo Z
  Bop    : IFoo (S Z)

-- more complex indexed enumeration type, don't be shocked if testing this
-- doens't work in your repl, you simply need to tell it what g or b are. This
-- would be the case if you wrote the functions by hand as well and if g or b
-- were 0-use. This is a hassle because we don't even use g or b, possibly just
-- a limitation of the type search or the fact that these instances work on
-- arguments of just Type.
data IFoo2 : Nat -> Type where
  Brap  : {g : Nat} -> IFoo2 g
  Zoppo : b `LTE` 1 => IFoo2 b
  Boppo : IFoo2 (S Z)

private
interface ToCode' a where
  toCode' : a -> Int

private
interface FromCode' a where
  fromCode' : Int -> Maybe a
  unsafeFromCode' : Int -> a

private
Show Foo where
  show = showEnum

private
Show (IFoo n) where
  show = showEnum

private
Show (IFoo2 n) where
  show = showEnum

private
Eq Foo where
  (==) = eqEnum

private
Ord Foo where
  compare = compareEnum

private
ToCode' Foo where
  toCode' = enumTo [0,1]

private
FromCode' Foo where
  unsafeFromCode' = unsafeEnumFrom [0,1]
  fromCode' = enumFrom [0,1]

eqTest1 : Baz == Baz = True
eqTest1 = Refl

eqTest2 : Baz == Biz = False
eqTest2 = Refl

enumToTest1 : toCode' Baz == 1 = True
enumToTest1 = Refl

enumFromTest1 : unsafeFromCode' 0 == Biz = True
enumFromTest1 = Refl

enumFromTest2 : unsafeFromCode' (-12345) == Baz = True
enumFromTest2 = ?crash

enumFromSafeTest1 : fromCode' 0 == Just Biz = True
enumFromSafeTest1 = Refl

enumFromSafeTest2 : fromCode' 3 == Nothing {ty=Foo} = True
enumFromSafeTest2 = Refl

showTest1 : show Baz == "Baz" = True
showTest1 = Refl

showTest2 : show Bop == "Bop" = True
showTest2 = Refl

showTest3 : show (Brap {g=2}) == "Brap" = True
showTest3 = Refl

compareTest1 : Biz > Baz = False
compareTest1 = Refl

compareTest2 : Biz < Baz = True
compareTest2 = Refl

compareTest3 : compare Biz Baz = LT
compareTest3 = Refl


text:
data List' a = Nil | Cons a (List' a)

-- Generated with `:gd 4 mapList'`
mapList' : ((1 x : a) -> b) -> (1 xs : List' a) -> List' b
mapList' f [] = []
mapList' f (Cons x y) = Cons (f x) (mapList' f y)

data Tree1 a = Nil1 | Node1 a (Tree1 a) (Tree1 a)

mapTree1 : ((1 x : a) -> b) -> (1 t : Tree1 a) -> Tree1 b

data Tree2 a = Nil2 | Node2 a (List' (Tree2 a))

-- TODO: Fix not entirly appropriate definition (nulls list of Node2)
mapTree2 : ((1 x : a) -> b) -> (1 t : Tree2 a) -> Tree2 b


text:
-- ----------------------------------------------------------------- [ IOR.idr ]
-- Module    : IOR.idr
-- Copyright : (c) Jan de Muijnck-Hughes
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]

||| Testing IOR contribution evaluation
module GRL.Test.Contribution

import GRL.Lang.GLang
import GRL.Eval

import GRL.Test.Utils

%default total

-- -------------------------------------------------------- [ Model Definition ]

conn : GOAL
conn = mkGoal "Increase Mobility"

lan : TASK
lan = mkTask "LAN"

wireless : TASK
wireless = mkTask "Wireless"

internet : TASK
internet = mkTask "Internet"

model : GModel
model = emptyModel
   \= conn \= lan \= wireless \= internet
   \= (internet ==> conn | SOMEPOS)
   \= (wireless ==> conn | MAKES)
   \= (lan      ==> conn | SOMENEG)

-- ---------------------------------------------------------- [ IOR Strategies ]

a : Strategy
a = buildStrategy
    [ (lan, NONE)
    , (wireless, WEAKSATIS)
    , (internet, WEAKDEN)]

aExpRes : Strategy
aExpRes = buildStrategy
    [ (conn, NONE)
    , (lan, NONE)
    , (wireless, WEAKSATIS)
    , (internet, WEAKDEN)]

b : Strategy
b = buildStrategy
    [ (lan, NONE)
    , (wireless, WEAKSATIS)
    , (internet, WEAKSATIS)]

bExpRes : Strategy
bExpRes = buildStrategy
    [ (lan, NONE)
    , (wireless, WEAKSATIS)
    , (internet, WEAKSATIS)
    , (conn, WEAKSATIS)]

-- -------------------------------------------------------------------- [ Test ]

export partial
runTest : IO ()
runTest = do
  putStrLn "--> Composition Tests"

  putStrLn "Strategy A:"
  doTest model a aExpRes

  putStrLn "Strategy B:"
  doTest model b bExpRes

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

max_stars_repo_name: jfdm/idris-grl

max_issues_repo_name: jfdm/idris-grl

max_forks_repo_name: jfdm/idris-grl


text:
module Dart.Core.Duration

import Dart.FFI.Elab
import Dart.Core

%language ElabReflection

%runElab importDart [
  package "dart:core" [
    partial' $ class' "Duration" [
      static $ final "Duration" "zero",
      static $ final "int" "microsecondsPerMinute",
      static $ final "int" "microsecondsPerSecond",
      static $ final "int" "microsecondsPerMillisecond",

      final "int" "inSeconds",
      final "int" "inMilliseconds",
      final "int" "inMicroseconds",

      const $ new "" [
        "days" :? "int",
        "hours" :? "int",
        "minutes" :? "int",
        "seconds" :? "int",
        "milliseconds" :? "int",
        "microseconds" :? "int"
      ]
    ]
  ]
]

namespace Duration

  %inline
  public export
  (-) : Duration -> Duration -> Duration
  (-) x y = prim__dart_invoke_pure "-" [] [x, y] Parameters.none

  %inline
  public export
  (+) : Duration -> Duration -> Duration
  (+) x y = prim__dart_invoke_pure "+" [] [x, y] Parameters.none


text:
module Hardware

public export
Word : Type
Word = Int

public export
data Register = R1 | R2 | R3 | R4 | R5 | PC

-- Memory layout
public export
record Registers where
  constructor MkRegisters
  r1, r2, r3, r4, r5, pc : Int

public export
data Instruction : Type where
  ||| Rz = Rx + yR
  ADD     : Register -> Register -> Register -> Instruction
  ||| Rz = sha3(Rx)
  SHA3    : Register -> Register -> Instruction
  ||| Rz = current contract address
  ADDRESS : Register -> Instruction
  ||| Rz = data of location Ry
  LOAD    : Register -> Register -> Instruction
  ||| If Rx, execute at (current location + int)
  JUMPI   : Register -> Int -> Instruction
  ||| Rz = Rx == Ry
  EQUAL   : Register -> Register -> Register -> Instruction
  ||| Rz = !Rx
  NOT     : Register -> Register -> Instruction

  --
  ||| Not an opcode - This is used to load data
  DATA    : Word -> Instruction

public export
record Memory where
  constructor MkMemory
  regs : Registers
  asm  : List Instruction

--------------------------------------------------
--              util functions

export
toRD : Register -> Memory -> Int
toRD R1 m = r1 $ regs m
toRD R2 m = r2 $ regs m
toRD R3 m = r3 $ regs m
toRD R4 m = r4 $ regs m
toRD R5 m = r5 $ regs m
toRD PC m = pc $ regs m

export
updtRD : Register -> Int -> Memory -> Memory
updtRD R1 i m = record { regs->r1 = i } m
updtRD R2 i m = record { regs->r2 = i } m
updtRD R3 i m = record { regs->r3 = i } m
updtRD R4 i m = record { regs->r4 = i } m
updtRD R5 i m = record { regs->r5 = i } m
updtRD PC i m = record { regs->pc = i } m

--------------------------------------------------
--                  print

export
printRegisters : Memory -> IO ()
printRegisters m = let r1' = show $ r1 $ regs m
                       r2' = show $ r2 $ regs m
                       r3' = show $ r3 $ regs m
                       r4' = show $ r4 $ regs m
                       r5' = show $ r5 $ regs m
                       pc' = show $ pc $ regs m
                   in printLn $   "R1-" <+> r1' <+> " "
                              <+> "R2-" <+> r2' <+> " "
                              <+> "R3-" <+> r3' <+> " "
                              <+> "R4-" <+> r4' <+> " "
                              <+> "R5-" <+> r5' <+> " "
                              <+> "PC-" <+> pc' <+> " "

max_stars_repo_name: nickgeoca/QVM

max_issues_repo_name: nickgeoca/QVM

max_forks_repo_name: nickgeoca/QVM


text:
module Erlang.IO

import Erlang.Types

%default total

||| Type-alias for an Erlang exception.
|||
||| The tuple contains the following values (in order): Class, Reason, Stacktrace.
public export
ErlException : Type
ErlException = ErlTuple3 ErlAtom ErlTerm ErlTerm

%extern prim__erlModule : ErlAtom
%extern prim__erlUnsafeCall : (0 ret : Type) -> String -> String -> ErlList xs -> ret
%extern prim__erlTryCatch : IO a -> (1 x : %World) -> IORes (Either ErlException a)

-- CURRENT MODULE

||| Get the name of the current module.
export %inline
erlModule : ErlAtom
erlModule = prim__erlModule

-- FFI

||| Call an Erlang function. (Caution: Wrong usage of this function may result
||| in run-time errors.)
|||
||| The arguments and the return type must be a member of `ErlType`.
||| You can use the `Raw` type if you want to pass any Idris value.
|||
||| This function is considered unsafe for the following reasons:
||| 1. The called Erlang function may perform side-effects.
||| 2. The called Erlang function may crash the process or never terminate.
||| 3. The specified return type may not match the returned value from the
|||    called Erlang function.
|||
||| See `erlCall` for a safe way to call Erlang functions.
export %inline
erlUnsafeCall : (0 ret : Type) -> {auto 0 retPrf : ErlType ret} ->
                (modName : String) -> (funName : String) -> (args : ErlList xs) -> {auto 0 argsPrf : ErlTypes xs} -> ret
erlUnsafeCall ret modName funName args = prim__erlUnsafeCall ret modName funName args

||| Wrap an IO action in a try/catch.
|||
||| `erlTryCatch` should only be necessary when using `erlUnsafeCall`. In
||| these cases you might want to consider using `erlCall` instead.
|||
||| Generally, total functions (including functions of type `IO`) should not
||| crash at run-time.
|||
||| See `erlCall` for an example usage of `erlTryCatch`.
export
erlTryCatch : HasIO io => IO a -> io (Either ErlException a)
erlTryCatch action = primIO (prim__erlTryCatch action)

||| Call an Erlang function.
|||
||| In contrast to `erlUnsafeCall`, `erlCall` is honest about the guarantees
||| it gives:
||| 1. The return type of `erlCall` allows the Erlang function to perform
|||    side-effects.
||| 2. `erlCall` is annotated as partial because the called function may never
|||    terminate. Additionally, if the called Erlang function crashes it should
|||    be caught by the try/catch.
||| 3. `erlCall` returns an `ErlTerm`, which can represent any Erlang value.
|||
||| The `ErlTerm` value can be decoded into a typed Idris value by using the
||| decoding functions from `Erlang.Decode`.
export partial %inline
erlCall : HasIO io => (modName : String) -> (funName : String) -> (args : ErlList xs) -> {auto 0 prf : ErlTypes xs} -> io (Either ErlException ErlTerm)
erlCall modName fnName args = erlTryCatch (pure $ erlUnsafeCall ErlTerm modName fnName args)

-- EXPORT ERLANG FUNCTIONS

||| Export values and functions as named Erlang functions.
|||
||| Example module:
||| ```
||| module Main
|||
||| %cg erlang export exports
|||
||| increment : Integer -> Integer
||| increment x = x + 1
|||
||| exports : ErlExport
||| exports =
|||   Fun "foo" 42
|||     <+> Fun "increment" (MkFun1 increment)
||| ```
|||
||| This example will generate two functions that will be exported:
||| `foo/0` and `increment/1`
|||
||| When exporting a value, the generated function will have an arity of 0.
||| When exporting a function, the generated function will have the same arity
||| as the original function.
public export
data ErlExport : Type where
  Fun : ErlType t => (name : String) -> (expr : t) -> ErlExport
  Combine : ErlExport -> ErlExport -> ErlExport

||| Convenience operator for combining `ErlExport`.
public export %inline
(<+>) : ErlExport -> ErlExport -> ErlExport
(<+>) = Combine


text:
module Network.Curl.Types.CurlEOption

import Network.Curl.Types.Code
import Network.Curl.Types.OptType

import Data.Buffer

import Util -- difference

import Derive.Enum
%language ElabReflection

public export
data CurlEOption : OptType -> Type where
  CURLOPT_WRITEDATA : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_URL : CurlEOption CURLOPTTYPE_STRINGPOINT --CURLOPTTYPE_OBJECTPOINT
  CURLOPT_PORT : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_PROXY : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_USERPWD : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_PROXYUSERPWD : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_RANGE : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_READDATA : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_ERRORBUFFER : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_WRITEFUNCTION : CurlEOption CURLOPTTYPE_FUNCTIONPOINT
  CURLOPT_READFUNCTION : CurlEOption CURLOPTTYPE_FUNCTIONPOINT
  CURLOPT_TIMEOUT : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_INFILESIZE : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_POSTFIELDS : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_REFERER : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_FTPPORT : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_USERAGENT : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_LOW_SPEED_LIMIT : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_LOW_SPEED_TIME : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_RESUME_FROM : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_COOKIE : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_HTTPHEADER : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_HTTPPOST : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_SSLCERT : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_KEYPASSWD : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_CRLF : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_QUOTE : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_HEADERDATA : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_COOKIEFILE : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_SSLVERSION : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_TIMECONDITION : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_TIMEVALUE : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_CUSTOMREQUEST : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_STDERR : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_POSTQUOTE : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_OBSOLETE40 : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_VERBOSE : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_HEADER : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_NOPROGRESS : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_NOBODY : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_FAILONERROR : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_UPLOAD : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_POST : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_DIRLISTONLY : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_APPEND : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_NETRC : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_FOLLOWLOCATION : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_TRANSFERTEXT : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_PUT : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_PROGRESSFUNCTION : CurlEOption CURLOPTTYPE_FUNCTIONPOINT
  CURLOPT_XFERINFODATA : CurlEOption CURLOPTTYPE_OBJECTPOINT -- aka CURLOPT_PROGRESSDATA
  CURLOPT_AUTOREFERER : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_PROXYPORT : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_POSTFIELDSIZE : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_HTTPPROXYTUNNEL : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_INTERFACE : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_KRBLEVEL : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_SSL_VERIFYPEER : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_CAINFO : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_MAXREDIRS : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_FILETIME : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_TELNETOPTIONS : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_MAXCONNECTS : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_OBSOLETE72 : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_FRESH_CONNECT : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_FORBID_REUSE : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_RANDOM_FILE : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_EGDSOCKET : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_CONNECTTIMEOUT : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_HEADERFUNCTION : CurlEOption CURLOPTTYPE_FUNCTIONPOINT
  CURLOPT_HTTPGET : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_SSL_VERIFYHOST : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_COOKIEJAR : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_SSL_CIPHER_LIST : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_HTTP_VERSION : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_FTP_USE_EPSV : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_SSLCERTTYPE : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_SSLKEY : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_SSLKEYTYPE : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_SSLENGINE : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_SSLENGINE_DEFAULT : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_DNS_USE_GLOBAL_CACHE : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_DNS_CACHE_TIMEOUT : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_PREQUOTE : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_DEBUGFUNCTION : CurlEOption CURLOPTTYPE_FUNCTIONPOINT
  CURLOPT_DEBUGDATA : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_COOKIESESSION : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_CAPATH : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_BUFFERSIZE : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_NOSIGNAL : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_SHARE : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_PROXYTYPE : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_ACCEPT_ENCODING : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_PRIVATE : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_HTTP200ALIASES : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_UNRESTRICTED_AUTH : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_FTP_USE_EPRT : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_HTTPAUTH : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_SSL_CTX_FUNCTION : CurlEOption CURLOPTTYPE_FUNCTIONPOINT
  CURLOPT_SSL_CTX_DATA : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_FTP_CREATE_MISSING_DIRS : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_PROXYAUTH : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_SERVER_RESPONSE_TIMEOUT : CurlEOption CURLOPTTYPE_LONG -- aka CURLOPT_FTP_RESPONSE_TIMEOUT
  CURLOPT_IPRESOLVE : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_MAXFILESIZE : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_INFILESIZE_LARGE : CurlEOption CURLOPTTYPE_OFF_T
  CURLOPT_RESUME_FROM_LARGE : CurlEOption CURLOPTTYPE_OFF_T
  CURLOPT_MAXFILESIZE_LARGE : CurlEOption CURLOPTTYPE_OFF_T
  CURLOPT_NETRC_FILE : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_USE_SSL : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_POSTFIELDSIZE_LARGE : CurlEOption CURLOPTTYPE_OFF_T
  CURLOPT_TCP_NODELAY : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_FTPSSLAUTH : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_IOCTLFUNCTION : CurlEOption CURLOPTTYPE_FUNCTIONPOINT
  CURLOPT_IOCTLDATA : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_FTP_ACCOUNT : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_COOKIELIST : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_IGNORE_CONTENT_LENGTH : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_FTP_SKIP_PASV_IP : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_FTP_FILEMETHOD : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_LOCALPORT : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_LOCALPORTRANGE : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_CONNECT_ONLY : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_CONV_FROM_NETWORK_FUNCTION : CurlEOption CURLOPTTYPE_FUNCTIONPOINT
  CURLOPT_CONV_TO_NETWORK_FUNCTION : CurlEOption CURLOPTTYPE_FUNCTIONPOINT
  CURLOPT_CONV_FROM_UTF8_FUNCTION : CurlEOption CURLOPTTYPE_FUNCTIONPOINT
  CURLOPT_MAX_SEND_SPEED_LARGE : CurlEOption CURLOPTTYPE_OFF_T
  CURLOPT_MAX_RECV_SPEED_LARGE : CurlEOption CURLOPTTYPE_OFF_T
  CURLOPT_FTP_ALTERNATIVE_TO_USER : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_SOCKOPTFUNCTION : CurlEOption CURLOPTTYPE_FUNCTIONPOINT
  CURLOPT_SOCKOPTDATA : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_SSL_SESSIONID_CACHE : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_SSH_AUTH_TYPES : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_SSH_PUBLIC_KEYFILE : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_SSH_PRIVATE_KEYFILE : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_FTP_SSL_CCC : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_TIMEOUT_MS : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_CONNECTTIMEOUT_MS : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_HTTP_TRANSFER_DECODING : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_HTTP_CONTENT_DECODING : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_NEW_FILE_PERMS : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_NEW_DIRECTORY_PERMS : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_POSTREDIR : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_SSH_HOST_PUBLIC_KEY_MD5 : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_OPENSOCKETFUNCTION : CurlEOption CURLOPTTYPE_FUNCTIONPOINT
  CURLOPT_OPENSOCKETDATA : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_COPYPOSTFIELDS : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_PROXY_TRANSFER_MODE : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_SEEKFUNCTION : CurlEOption CURLOPTTYPE_FUNCTIONPOINT
  CURLOPT_SEEKDATA : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_CRLFILE : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_ISSUERCERT : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_ADDRESS_SCOPE : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_CERTINFO : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_USERNAME : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_PASSWORD : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_PROXYUSERNAME : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_PROXYPASSWORD : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_NOPROXY : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_TFTP_BLKSIZE : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_SOCKS5_GSSAPI_SERVICE : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_SOCKS5_GSSAPI_NEC : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_PROTOCOLS : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_REDIR_PROTOCOLS : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_SSH_KNOWNHOSTS : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_SSH_KEYFUNCTION : CurlEOption CURLOPTTYPE_FUNCTIONPOINT
  CURLOPT_SSH_KEYDATA : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_MAIL_FROM : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_MAIL_RCPT : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_FTP_USE_PRET : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_RTSP_REQUEST : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_RTSP_SESSION_ID : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_RTSP_STREAM_URI : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_RTSP_TRANSPORT : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_RTSP_CLIENT_CSEQ : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_RTSP_SERVER_CSEQ : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_INTERLEAVEDATA : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_INTERLEAVEFUNCTION : CurlEOption CURLOPTTYPE_FUNCTIONPOINT
  CURLOPT_WILDCARDMATCH : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_CHUNK_BGN_FUNCTION : CurlEOption CURLOPTTYPE_FUNCTIONPOINT
  CURLOPT_CHUNK_END_FUNCTION : CurlEOption CURLOPTTYPE_FUNCTIONPOINT
  CURLOPT_FNMATCH_FUNCTION : CurlEOption CURLOPTTYPE_FUNCTIONPOINT
  CURLOPT_CHUNK_DATA : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_FNMATCH_DATA : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_RESOLVE : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_TLSAUTH_USERNAME : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_TLSAUTH_PASSWORD : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_TLSAUTH_TYPE : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_TRANSFER_ENCODING : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_CLOSESOCKETFUNCTION : CurlEOption CURLOPTTYPE_FUNCTIONPOINT
  CURLOPT_CLOSESOCKETDATA : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_GSSAPI_DELEGATION : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_DNS_SERVERS : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_ACCEPTTIMEOUT_MS : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_TCP_KEEPALIVE : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_TCP_KEEPIDLE : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_TCP_KEEPINTVL : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_SSL_OPTIONS : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_MAIL_AUTH : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_SASL_IR : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_XFERINFOFUNCTION : CurlEOption CURLOPTTYPE_FUNCTIONPOINT
  CURLOPT_XOAUTH2_BEARER : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_DNS_INTERFACE : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_DNS_LOCAL_IP4 : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_DNS_LOCAL_IP6 : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_LOGIN_OPTIONS : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_SSL_ENABLE_NPN : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_SSL_ENABLE_ALPN : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_EXPECT_100_TIMEOUT_MS : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_PROXYHEADER : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_HEADEROPT : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_PINNEDPUBLICKEY : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_UNIX_SOCKET_PATH : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_SSL_VERIFYSTATUS : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_SSL_FALSESTART : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_PATH_AS_IS : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_PROXY_SERVICE_NAME : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_SERVICE_NAME : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_PIPEWAIT : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_DEFAULT_PROTOCOL : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_STREAM_WEIGHT : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_STREAM_DEPENDS : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_STREAM_DEPENDS_E : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_TFTP_NO_OPTIONS : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_CONNECT_TO : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_TCP_FASTOPEN : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_KEEP_SENDING_ON_ERROR : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_PROXY_CAINFO : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_PROXY_CAPATH : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_PROXY_SSL_VERIFYPEER : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_PROXY_SSL_VERIFYHOST : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_PROXY_SSLVERSION : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_PROXY_TLSAUTH_USERNAME : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_PROXY_TLSAUTH_PASSWORD : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_PROXY_TLSAUTH_TYPE : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_PROXY_SSLCERT : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_PROXY_SSLCERTTYPE : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_PROXY_SSLKEY : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_PROXY_SSLKEYTYPE : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_PROXY_KEYPASSWD : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_PROXY_SSL_CIPHER_LIST : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_PROXY_CRLFILE : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_PROXY_SSL_OPTIONS : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_PRE_PROXY : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_PROXY_PINNEDPUBLICKEY : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_ABSTRACT_UNIX_SOCKET : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_SUPPRESS_CONNECT_HEADERS : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_REQUEST_TARGET : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_SOCKS5_AUTH : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_SSH_COMPRESSION : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_MIMEPOST : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_TIMEVALUE_LARGE : CurlEOption CURLOPTTYPE_OFF_T
  CURLOPT_HAPPY_EYEBALLS_TIMEOUT_MS : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_RESOLVER_START_FUNCTION : CurlEOption CURLOPTTYPE_FUNCTIONPOINT
  CURLOPT_RESOLVER_START_DATA : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_HAPROXYPROTOCOL : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_DNS_SHUFFLE_ADDRESSES : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_TLS13_CIPHERS : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_PROXY_TLS13_CIPHERS : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_DISALLOW_USERNAME_IN_URL : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_DOH_URL : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_UPLOAD_BUFFERSIZE : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_UPKEEP_INTERVAL_MS : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_CURLU : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_TRAILERFUNCTION : CurlEOption CURLOPTTYPE_FUNCTIONPOINT
  CURLOPT_TRAILERDATA : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_HTTP09_ALLOWED : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_ALTSVC_CTRL : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_ALTSVC : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_MAXAGE_CONN : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_SASL_AUTHZID : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_MAIL_RCPT_ALLLOWFAILS : CurlEOption CURLOPTTYPE_LONG
  CURLOPT_SSLCERT_BLOB : CurlEOption CURLOPTTYPE_BLOB
  CURLOPT_SSLKEY_BLOB : CurlEOption CURLOPTTYPE_BLOB
  CURLOPT_PROXY_SSLCERT_BLOB : CurlEOption CURLOPTTYPE_BLOB
  CURLOPT_PROXY_SSLKEY_BLOB : CurlEOption CURLOPTTYPE_BLOB
  CURLOPT_ISSUERCERT_BLOB : CurlEOption CURLOPTTYPE_BLOB
  CURLOPT_PROXY_ISSUERCERT : CurlEOption CURLOPTTYPE_OBJECTPOINT
  CURLOPT_PROXY_ISSUERCERT_BLOB : CurlEOption CURLOPTTYPE_BLOB
  CURLOPT_LASTENTRY : CurlEOption UnusedOptType

curlEOptEnumList : List Int
curlEOptEnumList = difference [1..298]
  [8,30,35,38,49,55,66,67,73,122,123,124,125,126,127,128,132,133]
-- ^ remove enums omitted from curl.h

[derivedToCode] ToCode (CurlEOption ty) where
  toCode = enumTo curlEOptEnumList

-- Automate toCode plussing with the power of named instances
public export
{ty : _} -> ToCode (CurlEOption ty) where
  toCode opt = toCode @{derivedToCode} opt + toCode ty

-- from is a little more complicated to automate since we'll need to case ty
-- somehow during elab. tough but we need that if we query curl for current
-- options. We can always do it manually though, but what a mess if so.

-- [derivedFromCode] {ty :_} -> FromCode (CurlEOption ty) where
  -- fromCode {ty} = ?aSDFfd_1

public export
Show (CurlEOption ty) where
  show = showEnum

public export
total
paramType : {ty : _} -> CurlEOption ty -> Type
paramType {ty = CURLOPTTYPE_FUNCTIONPOINT} CURLOPT_WRITEFUNCTION
  = Buffer -> (itemsize : Int) -> (len : Int) -> AnyPtr -> PrimIO Int
paramType {ty = CURLOPTTYPE_FUNCTIONPOINT} CURLOPT_READFUNCTION
  = Buffer -> (itemsize : Int) -> (len : Int) -> AnyPtr -> PrimIO Int
paramType {ty = CURLOPTTYPE_FUNCTIONPOINT} CURLOPT_PROGRESSFUNCTION
  = Int -- use CURLOPT_XFERINFOFUNCTION
paramType {ty = CURLOPTTYPE_FUNCTIONPOINT} CURLOPT_HEADERFUNCTION
  = Buffer -> (size : Int) -> (len : Int) -> AnyPtr -> PrimIO Int
paramType {ty = CURLOPTTYPE_FUNCTIONPOINT} CURLOPT_DEBUGFUNCTION
  = Int -- not implemented (yet)
paramType {ty = CURLOPTTYPE_FUNCTIONPOINT} CURLOPT_SSL_CTX_FUNCTION
  = Int -- not implemented (yet)
paramType {ty = CURLOPTTYPE_FUNCTIONPOINT} CURLOPT_IOCTLFUNCTION
  = Int -- not implemented (yet)
paramType {ty = CURLOPTTYPE_FUNCTIONPOINT} CURLOPT_CONV_FROM_NETWORK_FUNCTION
  = Int -- not implemented (yet)
paramType {ty = CURLOPTTYPE_FUNCTIONPOINT} CURLOPT_CONV_TO_NETWORK_FUNCTION
  = Int -- not implemented (yet)
paramType {ty = CURLOPTTYPE_FUNCTIONPOINT} CURLOPT_CONV_FROM_UTF8_FUNCTION
  = Int -- not implemented (yet)
paramType {ty = CURLOPTTYPE_FUNCTIONPOINT} CURLOPT_SOCKOPTFUNCTION
  = Int -- not implemented (yet)
paramType {ty = CURLOPTTYPE_FUNCTIONPOINT} CURLOPT_OPENSOCKETFUNCTION
  = Int -- not implemented (yet)
paramType {ty = CURLOPTTYPE_FUNCTIONPOINT} CURLOPT_SEEKFUNCTION
  = Int -- AnyPtr -> Bits64 -> Int -> PrimIO Int -- not implemented (yet) NB useful
paramType {ty = CURLOPTTYPE_FUNCTIONPOINT} CURLOPT_SSH_KEYFUNCTION
  = Int -- not implemented (yet)
paramType {ty = CURLOPTTYPE_FUNCTIONPOINT} CURLOPT_INTERLEAVEFUNCTION
  = Int -- not implemented (yet)
paramType {ty = CURLOPTTYPE_FUNCTIONPOINT} CURLOPT_CHUNK_BGN_FUNCTION
  = Int -- not implemented (yet)
paramType {ty = CURLOPTTYPE_FUNCTIONPOINT} CURLOPT_CHUNK_END_FUNCTION
  = Int -- not implemented (yet)
paramType {ty = CURLOPTTYPE_FUNCTIONPOINT} CURLOPT_FNMATCH_FUNCTION
  = Int -- not implemented (yet)
paramType {ty = CURLOPTTYPE_FUNCTIONPOINT} CURLOPT_CLOSESOCKETFUNCTION
  = AnyPtr -> (socket : Int) -> PrimIO Int
paramType {ty = CURLOPTTYPE_FUNCTIONPOINT} CURLOPT_XFERINFOFUNCTION
  = AnyPtr -> (dl_total : Bits64) -> (dl_now : Bits64)
           -> (ul_total : Bits64) -> (ul_now : Bits64) -> PrimIO Int
paramType {ty = CURLOPTTYPE_FUNCTIONPOINT} CURLOPT_RESOLVER_START_FUNCTION
  = Int -- not implemented (yet)
paramType {ty = CURLOPTTYPE_FUNCTIONPOINT} CURLOPT_TRAILERFUNCTION
  = Int -- not implemented (yet)
paramType opt = optType ty

-- paramType CURLOPT_WRITEFUNCTION
  -- = Buffer -> (size : Int) -> (nmemb : Int) -> AnyPtr -> PrimIO Int -- returns amount dealth with


text:
||| Tests for issue #269
import Data.Vect

%unbound_implicits off

record Foo (x : Vect n Nat) where
  constructor MkFoo

parameters (Foo : Vect n Nat)
  bar : Nat
  bar = 0

interface Foo (a : Vect n Nat) where
  baz : Nat

implementation Functor (Vect n) where


text:
||| Extra monad transformers
|||
|||  - StateT (re-exported from base)
|||  - MonadError interface and ExceptT transformer
|||  - MonadReader interface and ReaderT transformer
|||  - MonadCont interface and ContT transformer
|||
||| TODO: WriterT and MonadWriter, RWST transformer
module Extra.Control.MonadTrans

import public Control.Monad.Trans
import public Control.Monad.State

-- Classes

public export
interface Monad m => MonadError e m | m where
  throwError : e -> m a
  catchError : m a -> (e -> m a) -> m a

export
implementation MonadError e (Either e) where
  throwError = Left
  catchError (Left e) f = f e
  catchError (Right x) f = Right x

export
implementation MonadError () Maybe where
  throwError () = Nothing
  catchError Nothing f = f ()
  catchError (Just x) f = Just x

export
implementation MonadError e m => MonadError e (StateT s m) where
  throwError e = lift $ throwError e
  catchError (ST x) f = ST $ \st => catchError (x st) $ flip runStateT st . f

public export
interface Monad m => MonadReader r m | m where
  ask : m r
  local : (r -> r) -> m a -> m a
  reader : (r -> a) -> m a

-- public export
-- implementation MonadReader r ((->) r) where
--   ask = id
--   local f g = g . f
--   reader = id

-- FIXME: remove when #523 is merged
implementation HasIO m => HasIO (StateT s m) where
  liftIO io = ST $ \s => liftIO $ io_bind io $ \a => pure (a, s)

public export
interface Monad m => MonadCont m where
  callCC : ((a -> m b) -> m a) -> m a

export
implementation MonadCont m => MonadCont (StateT s m) where
  callCC f = ST $ \s =>
             callCC $ \c =>
             runStateT (f $ \a => ST $ \s' => c (a, s')) s
-- Which state to use?  Both s or s' make sense     ^^
-- in different situtations.  Choosing s' for now, since
-- that's what Haskell does.

-- ExceptT

public export
record ExceptT (e : Type) (m : Type -> Type) (a : Type) where
  constructor MkExceptT
  runExceptT : m (Either e a)

export
implementation Functor m => Functor (ExceptT e m) where
  map f (MkExceptT x) = MkExceptT $ map (map f) x

export
implementation Monad m => Applicative (ExceptT e m) where
  pure = MkExceptT . pure . pure

  (MkExceptT mf) <*> (MkExceptT mx) = MkExceptT $ do
    Right f <- mf
      | Left e => pure $ Left e
    Right x <- mx
      | Left e => pure $ Left e
    pure $ Right $ f x

export
implementation Monad m => Monad (ExceptT e m) where
  (MkExceptT mx) >>= f = MkExceptT $ do
    Right x <- mx
      | Left e => pure $ Left e
    runExceptT $ f x

export
implementation MonadTrans (ExceptT e) where
  lift x = MkExceptT $ map Right x

export
implementation MonadState s m => MonadState s (ExceptT e m) where
  get = lift get
  put x = lift $ put x

export
implementation Monad m => MonadError e (ExceptT e m) where
  throwError = MkExceptT . pure . Left
  catchError (MkExceptT mx) f = MkExceptT $ do
    Left e <- mx
      | Right x => pure $ Right x
    runExceptT $ f e

export
implementation MonadReader r m => MonadReader r (ExceptT e m) where
  ask = lift ask
  local f (MkExceptT x) = MkExceptT $ local f x
  reader = lift . reader

export
implementation HasIO m => HasIO (ExceptT e m) where
  liftIO io = MkExceptT $ liftIO $ io_bind io (pure . Right)

export
implementation MonadCont m => MonadCont (ExceptT e m) where
  callCC f = MkExceptT $
    callCC $ \cont => runExceptT $ f $ MkExceptT . cont . Right

-- ReaderT

public export
record ReaderT (r : Type) (m : Type -> Type) (a : Type) where
  constructor MkReaderT
  runReaderT : r -> m a

export
implementation Functor m => Functor (ReaderT r m) where
  map f (MkReaderT g) = MkReaderT $ map f . g

export
implementation Applicative m => Applicative (ReaderT r m) where
  pure = MkReaderT . const . pure
  MkReaderT f <*> MkReaderT x = MkReaderT $ \r => f r <*> x r

export
implementation Monad m => Monad (ReaderT r m) where
  MkReaderT x >>= f = MkReaderT $ \r => x r >>= flip runReaderT r . f

export
implementation MonadTrans (ReaderT r) where
  lift = MkReaderT . const

export
implementation Monad m => MonadReader r (ReaderT r m) where
  ask = MkReaderT pure
  local f (MkReaderT x) = MkReaderT $ x . f
  reader f = MkReaderT $ pure . f

export
implementation MonadState s m => MonadState s (ReaderT r m) where
  get = MkReaderT $ const get
  put = MkReaderT . const . put

export
implementation MonadError e m => MonadError e (ReaderT r m) where
  throwError = MkReaderT . const . throwError
  catchError (MkReaderT a) h = MkReaderT $ \r => catchError (a r) (flip runReaderT r . h)

export
implementation HasIO m => HasIO (ReaderT r m) where
  liftIO io = MkReaderT $ \_ => liftIO io

export
implementation MonadCont m => MonadCont (ReaderT r m) where
  callCC f = MkReaderT $ \r =>
    callCC $ \cont => flip runReaderT r $ f $ lift . cont

-- ContT

public export
data ContT : (r : k) -> (m : k -> Type) -> Type -> Type where
  MkContT : ((a -> m r) -> m r) -> ContT r m a

public export
runContT : ContT r m a -> (a -> m r) -> m r
runContT (MkContT c) = c

export
implementation Functor (ContT r m) where
  map f (MkContT c) = MkContT $ c . (. f)

export
implementation Applicative (ContT r m) where
  pure x = MkContT ($ x)
  MkContT f <*> MkContT x = MkContT $ \cont => f $ x . (cont .)

export
implementation Monad (ContT r m) where
  MkContT x >>= f = MkContT $ \cont => x $ (\cx => runContT (f cx) cont)

export
implementation MonadTrans (ContT r) where
  lift x = MkContT (x >>=)

export
implementation MonadCont (ContT r m) where
  callCC f = MkContT $ \cont => runContT (f $ \fc => MkContT $ \_ => cont fc) cont

export
implementation MonadReader r' m => MonadReader r' (ContT r m) where
  ask = lift ask
  local f (MkContT x) = MkContT $ local f . x
  reader = lift . reader

export
implementation MonadState s m => MonadState s (ContT r m) where
  get = lift get
  put = lift . put


text:
-- ---------------------------------------------------------------- [ Echo.idr ]
--
-- This RFC specifies a standard for the ARPA Internet community.  Hosts on
-- the ARPA Internet that choose to implement an Echo Protocol are expected
-- to adopt and implement this standard.
--
-- A very useful debugging and measurement tool is an echo service.  An
-- echo service simply sends back to the originating source any data it
-- receives.
--
-- http://tools.ietf.org/html/rfc862
--
-- --------------------------------------------------------------------- [ EOH ]
module RFC.Echo

import Effects

import Effect.Default
import Effect.StdIO
import Effect.Msg
import System.Protocol

import RFC.Utils

||| An echo service simply sends back to the originating source any
||| data it receives.
|||
||| This is an enhanced version of the protocol in which an invariant
||| is provide that stipulates that the message echoed back is the
||| original message sent.
total
echo : Protocol ['Client, 'Server] ()
echo = do
    msg <- 'Client ==> 'Server | Maybe String
    case msg of
      Just m  => do
        'Server ==> 'Client | Literal m
        Rec echo
      Nothing => Done

||| An echo service simply sends back to the originating source any
||| data it receives.
|||
||| A naive version of the protocol. This version does not provide
||| guarantees over the return message nor provides the recursive step.
total
echo' : Protocol ['Client, 'Server] ()
echo' = do
    'Client ==> 'Server | String
    'Server ==> 'Client | String
    Done

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

max_stars_repo_name: jfdm/idris-protocol-examples

max_issues_repo_name: jfdm/idris-protocol-examples

max_forks_repo_name: jfdm/idris-protocol-examples


text:
-- Day 6: Lanternfish

module Lanternfish
import System
import System.File
import Data.List
import Data.Vect
import Data.String.Parser

{--
The sea floor is getting steeper. Maybe the sleigh keys got carried this way?

A massive school of glowing lanternfish swims past. They must spawn quickly to reach such large numbers - maybe exponentially quickly? You should model their growth rate to be sure.

Although you know nothing about this specific species of lanternfish, you make some guesses about their attributes. Surely, each lanternfish creates a new lanternfish once every 7 days.

However, this process isn't necessarily synchronized between every lanternfish - one lanternfish might have 2 days left until it creates another lanternfish, while another might have 4. So, you can model each fish as a single number that represents the number of days until it creates a new lanternfish.

Furthermore, you reason, a new lanternfish would surely need slightly longer before it's capable of producing more lanternfish: two more days for its first cycle.

So, suppose you have a lanternfish with an internal timer value of 3:

After one day, its internal timer would become 2.
After another day, its internal timer would become 1.
After another day, its internal timer would become 0.
After another day, its internal timer would reset to 6, and it would create a new lanternfish with an internal timer of 8.
After another day, the first lanternfish would have an internal timer of 5, and the second lanternfish would have an internal timer of 7.
A lanternfish that creates a new fish resets its timer to 6, not 7 (because 0 is included as a valid timer value). The new lanternfish starts with an internal timer of 8 and does not start counting down until the next day.

Realizing what you're trying to do, the submarine automatically produces a list of the ages of several hundred nearby lanternfish (your puzzle input). For example, suppose you were given the following list:

3,4,3,1,2
This list means that the first fish has an internal timer of 3, the second fish has an internal timer of 4, and so on until the fifth fish, which has an internal timer of 2. Simulating these fish over several days would proceed as follows:

Initial state: 3,4,3,1,2 -> [0, 1, 1, 2, 1, 0, 0, 0, 0]
After  1 day:  2,3,2,0,1 -> [1, 1, 2, 1, 0, 0, 0, 0, 0]
After  2 days: 1,2,1,6,0,8
After  3 days: 0,1,0,5,6,7,8
After  4 days: 6,0,6,4,5,6,7,8,8
After  5 days: 5,6,5,3,4,5,6,7,7,8
After  6 days: 4,5,4,2,3,4,5,6,6,7
After  7 days: 3,4,3,1,2,3,4,5,5,6
After  8 days: 2,3,2,0,1,2,3,4,4,5
After  9 days: 1,2,1,6,0,1,2,3,3,4,8
After 10 days: 0,1,0,5,6,0,1,2,2,3,7,8
After 11 days: 6,0,6,4,5,6,0,1,1,2,6,7,8,8,8
After 12 days: 5,6,5,3,4,5,6,0,0,1,5,6,7,7,7,8,8
After 13 days: 4,5,4,2,3,4,5,6,6,0,4,5,6,6,6,7,7,8,8
After 14 days: 3,4,3,1,2,3,4,5,5,6,3,4,5,5,5,6,6,7,7,8
After 15 days: 2,3,2,0,1,2,3,4,4,5,2,3,4,4,4,5,5,6,6,7
After 16 days: 1,2,1,6,0,1,2,3,3,4,1,2,3,3,3,4,4,5,5,6,8
After 17 days: 0,1,0,5,6,0,1,2,2,3,0,1,2,2,2,3,3,4,4,5,7,8
After 18 days: 6,0,6,4,5,6,0,1,1,2,6,0,1,1,1,2,2,3,3,4,6,7,8,8,8,8
Each day, a 0 becomes a 6 and adds a new 8 to the end of the list, while each other number decreases by 1 if it was present at the start of the day.

In this example, after 18 days, there are a total of 26 fish. After 80 days, there would be a total of 5934.

Find a way to simulate lanternfish. How many lanternfish would there be after 80 days?

--- Part Two ---
Suppose the lanternfish live forever and have unlimited food and space. Would they take over the entire ocean?

After 256 days in the example above, there would be a total of 26984457539 lanternfish!
--}

zeroes : (n: Nat) -> Vect n Nat
zeroes n = replicate n Z

initCounter : (counter: Vect 9 Nat) -> (states: List (Fin 9)) -> Vect 9 Nat
initCounter counter [] = counter
initCounter counter (x :: xs) = initCounter (replaceAt x (S $ index x counter) counter) xs

growth : (days: Nat) -> (states: Vect 9 Nat) -> Vect 9 Nat
growth Z states = states
growth (S k) states = growth k $ zipWith (+) newFish $ tail states ++ [Z]
    where
      newFish : Vect 9 Nat
      newFish = replaceAt 8 (index 0 states) . replaceAt 6 (index 0 states) $ zeroes 9

main: IO ()
main = do
         args <- getArgs
         let (file :: _) = drop 1 args | [] => printLn "No file provided!"
         (Right symbols) <- readFile file | (Left error) => printLn error
         let (Right (nats, _)) = parse (commaSep natural) symbols | (Left error) => printLn error
         let (Just states) = traverse (\n => natToFin n 9) nats | Nothing => printLn "Invalid states!"
         printLn $ foldr (+) Z $ growth 256 $ initCounter (zeroes 9) states


text:
import Data.String.Parser

import System.File

Input : Type
Input = Nat

parser : Parser Input
parser = natural

part1 : Input -> IO String
part1 a = pure "Part 1 not implemented"

part2 : Input -> IO String
part2 a = pure "Part 2 not implemented"

main : IO ()
main = do Right input <- readFile "input.txt"
            | Left err => printLn err
          Right (a, _) <- pure $ parse parser input
            | Left err => printLn err
          part1 a >>= putStrLn
          part2 a >>= putStrLn


text:
module Main

import Parity
import System

data Bit : Nat -> Type where
     b0 : Bit 0
     b1 : Bit 1

instance Show (Bit n) where
     show b0 = "0"
     show b1 = "1"

infixl 5 #

data Binary : (width : Nat) -> (value : Nat) -> Type where
     zero : Binary Z Z
     (#)  : Binary w v -> Bit bit -> Binary (S w) (bit + 2 * v)

instance Show (Binary w k) where
     show zero = ""
     show (bin # bit) = show bin ++ show bit

addBit : Bit x -> Bit y -> Bit c -> Binary 2 (c + x + y)

adc : Binary w x -> Binary w y -> Bit c -> Binary (S w) (x + c + y)

-- adc zero zero carry ?= zero # carry
-- adc (numx # bx) (numy # by) carry
--      = let (zero # carry0 # lsb) = addBit bx by carry in
--            ?adcBody

{-
addBit b0 b0 b0 = zero # b0 # b0
addBit b0 b0 b1 = zero # b0 # b1
addBit b0 b1 b0 = zero # b0 # b1
addBit b0 b1 b1 = zero # b1 # b0
addBit b1 b0 b0 = zero # b0 # b1
addBit b1 b0 b1 = zero # b1 # b0
addBit b1 b1 b0 = zero # b1 # b0
addBit b1 b1 b1 = zero # b1 # b1
-}

{-
adc zero zero carry = zero # carry
adc (numx # bx) (numy # by) carry
     = let (zero # carry0 # lsb) = addBit bx by carry in
           ?adcBody
-}


text:
module API.Web.Console

import IdrisScript

%access public export
%default total

-- TODO: Proper type
log : String -> JS_IO ()
log = jscall "console.log(%0)" (String -> JS_IO ())

max_stars_repo_name: blau-io/idris-console

max_issues_repo_name: blau-io/idris-console

max_forks_repo_name: blau-io/idris-console


text:
> module Main

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

> J : Type -> Type -> Type
> J R X = (X -> R) -> X

> K : Type -> Type -> Type
> K R X = (X -> R) -> R

> overline : {X, R : Type} -> J R X -> K R X
> overline e p = p (e p)

> otimes : {X, R : Type} -> J R X -> (X -> J R (List X)) -> J R (List X)
> otimes e f p = x :: xs where
>   x   =    e (\ x' => overline (f x') (\ xs' => p (x' :: xs')))
>   xs  =  f x (\ xs' => p (x :: xs'))

> partial
> bigotimes : {X, R : Type} -> List (List X -> J R X) -> J R (List X)
> bigotimes       []   =  \ p => []
> bigotimes (e :: es)  =  (e []) `otimes` (\x => bigotimes [\ xs => d (x :: xs) | d <- es])

> partial
> argsup : {X : Type} -> (xs : List X) -> J Int X
> argsup (x :: Nil) p = x
> argsup (x :: x' :: xs) p = if p x < p x' then argsup (x' :: xs) p else argsup (x :: xs) p

> partial
> e : List Int -> J Int Int
> e _ = argsup [0..7]

> p : List Int -> Int
> p _ = 0

> partial
> main : IO ()
> main = do putStr ("bigotimes (replicate 3 e) p = "
>                   ++
>                   show (bigotimes (replicate 3 e) p) ++ "\n")


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

import public Minecraft.Core.Entity.Pickup.Export
import public Minecraft.Base.PreClassic.Stone.Block
import public Minecraft.Base.PreClassic.Stone.Item
import public Minecraft.Base.PreClassic.Stone.ItemEntity

%default total

[stoneItem']
Item Stone.Item where
  id = "minecraft:stone"
  stackable = Just 64
  givenName = \x => x.base.givenName
  proj = \x => new Stone.ItemEntity Stone.MkItemEntity

[putStone']
Put Stone.Item where
  putItem self = new Stone.Block Stone.MkBlock

[stoneVtbl']
Vtbl Stone.Item where
  vtable (Item Stone.Item) = Just stoneItem
  vtable (Put  Stone.Item) = Just putStone
  vtable _ = Nothing

stoneItem = stoneItem'
putStone  = putStone'
stoneVtbl = stoneVtbl'

max_stars_repo_name: po-stulate/postulate

max_issues_repo_name: po-stulate/postulate

max_forks_repo_name: po-stulate/postulate


text:
||| Allocate foreign memory
|||
||| Copyright 2021, HATTORI, Hiroki
||| This file is released under the MIT license, see LICENSE for more detail.
|||
module Foreign.Memory.Alloc

%default total

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

%foreign "scheme,chez:foreign-alloc"
         "C:malloc,libc"
prim__foreignAlloc : (bytes:Int) -> PrimIO AnyPtr

%foreign "scheme,chez:foreign-free"
prim__foreignFree : AnyPtr -> PrimIO ()

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

export unsafeAllocateMemoryGC : {ty:Type} -> HasIO io => (bytes:Nat) -> io (GCPtr ty)
unsafeAllocateMemoryGC bytes = do
  p <- primIO $ prim__foreignAlloc (cast bytes)
  liftIO $ onCollect (prim__castPtr p)
                     (\p' => primIO $ prim__foreignFree (prim__forgetPtr p'))

export unsafeAllocateMemory : {ty:Type} -> HasIO io => (bytes:Nat) -> io (Ptr ty)
unsafeAllocateMemory bytes = do
  p <- primIO $ prim__foreignAlloc (cast bytes)
  pure $ prim__castPtr p

export unsafeFreeMemory : HasIO io => Ptr ty -> io ()
unsafeFreeMemory p = primIO $ prim__foreignFree (prim__forgetPtr p)

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


text:
module Data.Crypto.Encryption.Block

import Data.Bits
import Data.Crypto.Util
import Data.Crypto.Encryption

%default total
%access public export

||| for a block cypher, you only need to provide functions to encrypt/decrypt a
||| single block.
-- TODO: Use `Maybe Nat` for `maximumBlocks`.
interface BlockCipher k (bitsPerBlock : Nat) (maximumBlocks : Nat) | k where
  encryptBlock : k -> Bits bitsPerBlock -> Bits bitsPerBlock
  decryptBlock : k -> Bits bitsPerBlock -> Bits bitsPerBlock
  -- blockTranslation : k -> Iso b b
  -- blockTranslation = MkIso (encryptBlock k) (decryptBlock k)

||| The encryption mode specifies how to apply a block cipher to multiple blocks
interface EncryptionMode (em : Nat -> Type) where
  encryptBlocks : BlockCipher k bitsPerBlock mb
                  => k -> em bitsPerBlock -> List (Bits bitsPerBlock)
                  -> List (Bits bitsPerBlock)
  decryptBlocks : BlockCipher k bitsPerBlock mb
                  => k -> em bitsPerBlock -> List (Bits bitsPerBlock)
                  -> List (Bits bitsPerBlock)

implementation (BlockCipher bc bitsPerBlock _, EncryptionMode em) =>
         Cipher (bc, em bitsPerBlock) bitsPerBlock where

implementation (BlockCipher bc bitsPerBlock _, EncryptionMode em) =>
         Encrypter (bc, em bitsPerBlock) bitsPerBlock where
  encryptMessage = uncurry encryptBlocks

implementation (BlockCipher bc bitsPerBlock _, EncryptionMode em) =>
         Decrypter (bc, em bitsPerBlock) bitsPerBlock where
  decryptMessage = uncurry decryptBlocks

implementation (BlockCipher bc bitsPerBlock _, EncryptionMode em) =>
         SymmetricCipher (bc, em bitsPerBlock) bitsPerBlock where

max_stars_repo_name: idris-hackers/idris-crypto

max_issues_repo_name: idris-hackers/idris-crypto

max_forks_repo_name: idris-hackers/idris-crypto