text:
module UserApi

import Control.Monad.Freer
import Debug.Trace
import Control.Monad.Id
import Data.Fin
import Control.Monad.State

%access public export
%default total
||| currently,some explorations on building computational graphs.
-- non dependent version,for testing only.see below for dependent version
data Tensor : Type where
  DoubleT : Double -> Tensor

implementation Show Tensor where
  show (DoubleT x) = show x

data GraphData : Type -> Type where
  Mul : Tensor -> Tensor -> GraphData Tensor
  Placeholder : GraphData Tensor
  Constant : Double -> GraphData Tensor

FreeGraph : Type --type of computation graph ,freer graph
FreeGraph = Freer GraphData Tensor

implicit gt2fg : GraphData Tensor -> FreeGraph
gt2fg = liftF

--check this at repl!
exampleGraph : FreeGraph
exampleGraph = do
  t<-liftF Placeholder
  a<-liftF Placeholder
  b<-Placeholder -- same,with implicits
  liftF (Mul t a)

--another example
mulG : FreeGraph
mulG = do
  x<-liftF $ Constant 1
  y<-liftF $ Constant 3
  liftF $ Mul x y

numericGradId : {x : Type}->  GraphData Tensor->GraphData x -> Id x
numericGradId Placeholder (Mul x y) =  pure $ DoubleT  2.0
numericGradId (Constant z) (Mul (DoubleT x) (DoubleT y)) =
  let res : Double =(x*y + 0.1)/(z+0.1) in
  pure $ trace (show z ++ "," ++show x) $ DoubleT res
numericGradId (Mul x y) (Mul (DoubleT z) (DoubleT w)) = pure $ DoubleT 3.0
numericGradId _ (Constant x) = pure $ DoubleT 3.0
numericGradId _ Placeholder = pure $ DoubleT 4.0

--try do some gradients,not ok yet
const1 : GraphData Tensor
const1 = Constant 1

mainGradId : Id String
mainGradId = do
  x <- (foldFreer ((trace "xxx" numericGradId) const1) mulG)
  --print x
  pure $ show x

||| dependent version
data TensorD : List Nat -> Type where
  MkTensorD : TensorD xs

data GraphDataD : Type -> Type where
  InD : (s : List Nat) -> GraphDataD $ TensorD s -- graph input,like Placeholder
  OutD : (s : List Nat) -> GraphDataD $ TensorD s -- graph output
  TrainableD : (s : List Nat) -> GraphDataD $ TensorD s -- variable in tf
  MulD : TensorD s -> TensorD s -> GraphDataD $ TensorD s
  VecMulD : TensorD [v] -> TensorD [v,_] -> GraphDataD $ TensorD [v] -- vec `mul` matrix ,safely
  MapD : TensorD x -> (TensorD x->TensorD x)->GraphDataD $ TensorD x -- for efficiency,pass map to tf c lib

tensorRank : TensorD x -> Nat
tensorRank {x=s} _ = length s

tensor1 : TensorD [1,2,3]
tensor1 = MkTensorD

tensorShape1 : TensorD a -> List Nat
tensorShape1 {a=zz} MkTensorD = zz

depGraph1 : GraphDataD $ TensorD [1,2,3]
depGraph1 = MulD tensor1 MkTensorD

FreeGraphD : Type->Type --type of computation graph ,freer graph
FreeGraphD a = Freer GraphDataD a

implicit liftd : GraphDataD a -> Freer GraphDataD a
liftd = liftF

depGraph2 : FreeGraphD $ (TensorD [1],TensorD [1])
depGraph2 = do
  in1<-liftF $ InD [1]
  out1<-liftF $ InD [1]
  out2<-InD [2] -- using implicits
  pure (in1,out1)

compGraphD : FreeGraphD $ TensorD [1]
compGraphD = do
  (in1,out1)<-depGraph2
  MulD in1 in1

interp1 : {x : Type}-> GraphDataD x -> State String x
interp1 (InD s) = ST (\x => Id (MkTensorD, x++" in "++ (show s)++" "))
interp1 (OutD s) = ST (\s => Id (MkTensorD, s++" out "))
interp1 (TrainableD s) = ST (\s => Id (MkTensorD, s++" train "))
interp1 (MulD x y) = ST (\s => Id (MkTensorD, s++" mul "))
interp1 (VecMulD y z) = ST (\s => Id (MkTensorD, s++" vec "))
interp1 (MapD y f) = ST (\s => Id (MkTensorD, s++" map "))
-- FreeGraph : Type --type of computation graph ,freer graph
-- FreeGraph = Freer GraphData Tensor

max_stars_repo_name: doofin/differentiable-idris

max_issues_repo_name: doofin/differentiable-idris

max_forks_repo_name: doofin/differentiable-idris


text:
module InsertionSort

import Data.Vect
import Data.Fin
import Permutation
import PermCons
import Finite
import DecOrderNat
import LTE_Properties
import SortingWithProof

%access public export
%default total

Smaller : Nat -> Nat -> Nat
Smaller Z n = Z
Smaller  m Z = Z
Smaller  (S m) (S n) = (S (Smaller m n))

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

Min : (m: Nat) -> (n: Nat) -> Either (LTE m n) (LTE n m)
Min Z n = Left LTEZero
Min m Z = Right LTEZero
Min (S a) (S b) = case (Min a b) of
                       (Left l) => Left (LTESucc l)
                       (Right r) => Right (LTESucc r)

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

insert: (k: Nat) -> (Vect n Nat) -> (Vect (S n) Nat)
insert k Nil = k :: Nil
insert k (x :: xs) = case (decMin k x) of
    (Left pf) => k :: x :: xs
    (Right pf) => x :: (insert k xs)

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

sort : (Vect n Nat) -> (Vect n Nat)
sort [] = []
sort (x :: xs) = insert x (sort xs)

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

VectMin: (n: Nat) -> (Vect n Nat) -> Nat
VectMin Z [] = Z
VectMin (S Z) [k] = k
VectMin (S (S len)) (x :: xs) = Smaller (VectMin (S len) xs) (x)

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

CheckSortedVect : (n: Nat) -> (Vect n Nat) -> Bool
CheckSortedVect Z [] = True
CheckSortedVect (S Z) [k] = True
CheckSortedVect (S (S n)) (x :: xs) = case (isLTE x (VectMin (S n) xs)) of
                                         (Yes prf) => (CheckSortedVect (S n) xs)
                                         (No contra) => False

ext: idr


text:
module Extra.C.FFI

public export
libc : String -> String
libc f = "C:" <+> f <+> ",libc"

public export
libextra : String -> String
libextra f = "C:" <+> f <+> ",libextra"


text:
module Crypto.Hash.Interfaces

import Data.Vect

public export
interface Digest (0 algo : Type) where
  digest_nbyte : Nat
  update : List Bits8 -> algo -> algo
  finalize : algo -> Vect digest_nbyte Bits8

public export
interface Digest algo => Hash algo where
  block_nbyte : Nat
  initialize : algo

public export
interface Digest algo => MAC (0 key : Type) algo where
  initialize_mac : key -> algo


text:
module Uri.Util

import Data.Buffer
import Debug.Trace

public export
hexDigitToDigit : Char -> Int
hexDigitToDigit c =
         if c >= '0' && c <= '9' then (cast c) - (cast '0')
    else if c >= 'A' && c <= 'F' then (cast c) - (cast 'A') + 10
    else if c >= 'a' && c <= 'f' then (cast c) - (cast 'a') + 10
    else 0

public export
hexToStringIO : List Int -> IO String
hexToStringIO list = do
        let size = length list
        res <- newBuffer (cast $ size)
        case res of
            Just buf => getString (hexToStr buf 0 list) 0 (cast size)
            Nothing => pure ""
    where
        hexToStr : Buffer -> Int -> List Int -> Buffer
        hexToStr buf idx (h :: tl) =
            let () = unsafePerformIO (setByte buf idx h) in
            hexToStr buf (idx+1) tl
        hexToStr buf idx [] = buf

%inline
public export
hexToStr : List Int -> String
hexToStr = unsafePerformIO . hexToStringIO

max_stars_repo_name: felipegchi/sayURI

max_issues_repo_name: felipegchi/sayURI

max_forks_repo_name: felipegchi/sayURI


text:
import Data.String

-- StringOrInt : Bool -> Type
-- StringOrInt False = String
-- StringOrInt True = Int

valToString : (isInt : Bool) -> (case isInt of
                                      True => String
                                      False => Int) -> String
valToString False x = cast x
valToString True x = trim x

max_stars_repo_name: brunoflores/type-driven-with-idris

max_issues_repo_name: brunoflores/type-driven-with-idris

max_forks_repo_name: brunoflores/type-driven-with-idris


text:
-- Idris2

import System
import System.Concurrency

-- Test `conditionWaitTimeout` times out for 1 main and 1 child thread

main : IO ()
main =
  do cvMutex <- makeMutex
     cv <- makeCondition
     t <- fork $ do mutexAcquire cvMutex
                    conditionWaitTimeout cv cvMutex 1000000
                    putStrLn "Where are you mother?"
                    mutexRelease cvMutex
     sleep 2
     putStrLn "Sorry I'm late child!"
     threadWait t


text:
module Control.Optics.Setter

import public Control.Optics.Types

export
sets : ((a -> b) -> s -> t) -> Setter s t a b
sets l (Mor f) = Mor $ Id . l (runIdentity . f)

export
mapped : Functor f => Setter (f a) (f b) a b
mapped = sets map

export
over : Setter s t a b -> (a -> b) -> s -> t
over optic f = runIdentity . applyMor (optic (Mor (Id . f)))

export
set : Setter s t a b -> b -> s -> t
set optic b = over optic (const b)

infixr 4 .~
export
(.~) : Setter s t a b -> b -> s -> t
(.~) = set

infixr 4 %~
export
(%~) : Setter s t a b -> (a -> b) -> s -> t
(%~) = over


text:
-- vim: ft=idris sw=2 ts=2 et

-- exercise of day1

-- find all numbers in a list that are greater than a given one
greater : Ord a => a -> List a -> List a
greater n ls = filter (\x => x > n) ls

-- find every other list element, starting from first element
everyOther : List a -> List a
everyOther [] = []
everyOther (x1 :: []) = [x1]
everyOther (x1 :: x2 :: xs) = x1 :: everyOther xs

-- playcard data type
data Color = Kreuz | Pik | Herz | Karo
data Value = Sieben | Acht | Neun | Zehn | Bube | Dame | Koenig | Ass
data Card = Pair Color Value
data Deck = List Card

-- even & odd numbers
mutual
  data Even = Two | EvenSucc Odd
  data Odd = One | OddSucc Even

-- binary tree
data BTree a =
  Node (BTree a) (BTree a) | Leaf

-- reverse a list
rev : List a -> List a
rev l = rev' l [] where
  rev' : List a -> List a -> List a
  rev' [] b = b
  rev' (a :: as) b = rev' as (a :: b)

max_stars_repo_name: kkirstein/proglang-playground

max_issues_repo_name: kkirstein/proglang-playground

max_forks_repo_name: kkirstein/proglang-playground


text:
{-
Copyright 2018, Mokshasoft AB (mokshasoft.com)

This software may be distributed and modified according to the terms of
the BSD 2-Clause license. Note that NO WARRANTY is provided.
See "LICENSE_BSD2.txt" for details.
-}

{-
  ported from kernel/libsel4/include/sel4/syscalls.h
-}

module seL4.Syscalls

import seL4.SharedTypes

%include C "ffi-syscalls.h"

%access public export
%default total

-- void seL4_Send(seL4_CPtr dest, seL4_MessageInfo_t msgInfo);
seL4_Send : Int -> SeL4_MessageInfo -> IO ()
seL4_Send dest msgInfo =
    foreign FFI_C "ffi_seL4_Send" (Int -> SeL4_MessageInfo -> IO ()) dest msgInfo

-- seL4_MessageInfo_t seL4_Recv(seL4_CPtr src, seL4_Word* sender);
-- seL4_MessageInfo_t seL4_Call(seL4_CPtr dest, seL4_MessageInfo_t msgInfo);
-- void seL4_Reply(seL4_MessageInfo_t msgInfo);
-- void seL4_NBSend(seL4_CPtr dest, seL4_MessageInfo_t msgInfo);
-- seL4_MessageInfo_t seL4_ReplyRecv(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Word *sender);
-- seL4_MessageInfo_t seL4_NBRecv(seL4_CPtr src, seL4_Word* sender);

-- void seL4_Yield(void);
seL4_Yield : IO ()
seL4_Yield = foreign FFI_C "seL4_Yield" (IO ())

-- void seL4_Signal(seL4_CPtr dest);
-- void seL4_Wait(seL4_CPtr src, seL4_Word *sender);
-- seL4_MessageInfo_t seL4_Poll(seL4_CPtr src, seL4_Word *sender);

ifdef(`CONFIG_PRINTING', `

-- void seL4_DebugPutChar(char c);
seL4_DebugPutChar : Char -> IO ()
seL4_DebugPutChar c = foreign FFI_C "seL4_DebugPutChar" (Char -> IO ()) c

-- void seL4_DebugDumpScheduler(void);
seL4_DebugDumpScheduler : IO ()
seL4_DebugDumpScheduler = foreign FFI_C "seL4_DebugDumpScheduler" (IO ())

')

ifdef(`CONFIG_DEBUG_BUILD', `

-- void seL4_DebugHalt(void);
seL4_DebugHalt : IO ()
seL4_DebugHalt = foreign FFI_C "seL4_DebugHalt" (IO ())

-- void seL4_DebugSnapshot(void);
seL4_DebugSnapshot : IO ()
seL4_DebugSnapshot = foreign FFI_C "seL4_DebugSnapshot" (IO ())

-- seL4_Uint32 seL4_DebugCapIdentify(seL4_CPtr cap);

-- void seL4_DebugNameThread(seL4_CPtr tcb, const char *name);
seL4_DebugNameThread : Int -> String -> IO ()
seL4_DebugNameThread cap name =
    foreign FFI_C "seL4_DebugNameThread" (Int -> String -> IO ()) cap name

')

ifdef(`CONFIG_DANGEROUS_CODE_INJECTION', `

-- void seL4_DebugRun(void (* userfn) (void *), void* userarg);

')

ifdef(`CONFIG_ENABLE_BENCHMARKS', `

-- seL4_Error seL4_BenchmarkResetLog(void);
-- seL4_Word seL4_BenchmarkFinalizeLog(void);
-- seL4_Error seL4_BenchmarkSetLogBuffer(seL4_Word frame_cptr);

-- void seL4_BenchmarkNullSyscall(void);
seL4_BenchmarkNullSyscall : IO ()
seL4_BenchmarkNullSyscall = foreign FFI_C "seL4_BenchmarkNullSyscall" (IO ())

-- void seL4_BenchmarkFlushCaches(void);
seL4_BenchmarkFlushCaches : IO ()
seL4_BenchmarkFlushCaches = foreign FFI_C "seL4_BenchmarkFlushCaches" (IO ())

ifdef(`CONFIG_BENCHMARK_TRACK_UTILISATION', `

-- void seL4_BenchmarkGetThreadUtilisation(seL4_Word tcb_cptr);
-- void seL4_BenchmarkResetThreadUtilisation(seL4_Word tcb_cptr);

')
')

ifdef(`CONFIG_ARCH_X86', `
ifdef(`CONFIG_VTX', `

-- seL4_Word seL4_VMEnter(seL4_Word *sender);

')
')


text:
module Control.Functor.Indexed

infixl 1 <<&>>
infixr 4 <<$>>, <<$, $>>

||| An Indexed Functor.
||| This interface is indexed backwards of similar utlities in Haskell
||| to make it more readily compatible with the evolution of a type from
||| Indexed simply on values (or types) but also on functions that depend on
||| those values.
|||
||| An indexed functor where the mappable type comes last does not later
||| refactor into what this library calls a TransitionIndexed type as readily.
public export
interface IndexedFunctor x y (0 f : Type -> x -> y -> Type) | f where
  total
  map : {0 j : x} -> {0 k : y} -> (a -> b) -> f a j k -> f b j k

||| Map for indexed functors.
public export
(<<$>>) : IndexedFunctor x y f => (a -> b) -> f a j k -> f b j k
(<<$>>) = map

||| Flipped version of `<<$>>`
public export
(<<&>>) : IndexedFunctor x y f => f a j k -> (a -> b) -> f b j k
(<<&>>) = flip (<<$>>)

||| Run something for effects, replacing the return value afterwards.
public export
(<<$) : IndexedFunctor x y f => b -> f a j k -> f b j k
(<<$) = map . const

||| Flipped version of `<<$`
public export
($>>) : IndexedFunctor x y f => f a j k -> b -> f b j k
($>>) = flip (<<$)

||| Run something for effects, throwing away the return value.
%inline
public export
ignore : IndexedFunctor x y f => f a j k -> f () j k
ignore = map (const ())

max_stars_repo_name: mattpolzin/idris-indexed

max_issues_repo_name: mattpolzin/idris-indexed

max_forks_repo_name: mattpolzin/idris-indexed


text:
import Config.JSON

main : IO ()
main = case parse parseJSONFile "[1, 2, 3  , {}]" of
         Left l => putStrLn l
         Right r => print r

max_stars_repo_name: slaven-s/idrispkgs

max_issues_repo_name: puffnfresh/idrispkgs

max_forks_repo_name: puffnfresh/idrispkgs


text:
data Direction = North
               | East
               | South
               | West

turn_clockwise : Direction -> Direction
turn_clockwise North = East
turn_clockwise East = South
turn_clockwise South = West
turn_clockwise West = North

data Shape = ||| A triangle, with base length and height
             Triangle Double Double
           | ||| A rectangle with length and height
             Rectangle Double Double
           | ||| A circle, with its radius
             Circle Double

area : Shape -> Double
area (Triangle base height) = 0.5 * base * height
area (Rectangle length height) = length * height
area (Circle radius) = pi * radius * radius

data Picture = Primitive Shape
             | Combine Picture Picture
             | Rotate Double Picture
             | Translate Double Double Picture

rectangle : Picture
rectangle = Primitive (Rectangle 20 10)

circle : Picture
circle = Primitive (Circle 5)

triangle : Picture
triangle = Primitive (Triangle 10 10)

test_pic : Picture
test_pic = Combine (Translate 5 5 rectangle)
                   (Combine (Translate 35 5 circle)
                            (Translate 15 25 triangle))

%name Shape shape, shape1, shape2
%name Picture pic, pic1, pic2

picture_area : Picture -> Double
picture_area (Primitive shape) = area shape
picture_area (Combine pic pic1) = picture_area pic + picture_area pic1
picture_area (Rotate x pic) = picture_area pic
picture_area (Translate x y pic) = picture_area pic

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

%name Tree tree, tree1

insert : Ord a =>
         a -> Tree a -> Tree a
insert x Empty = Node Empty x Empty
insert x orig@(Node left y right) = case compare x y of
                                    LT => Node (insert x left) y right
                                    EQ => orig
                                    GT => Node left y (insert x right)

listToTree : Ord a => List a -> Tree a
listToTree xs = foldr insert Empty xs

foldrTree : (a -> as -> as) -> as -> Tree a -> as
foldrTree f x Empty = x
foldrTree f x (Node lft y rgt) = let rgt' = (foldrTree f x rgt) in
                                 foldrTree f (f y rgt') lft

treeToList : Tree a -> List a
treeToList tree = foldrTree (::) [] tree

data Expr = PrimInt Int
          | Add Expr Expr
          | Sub Expr Expr
          | Mult Expr Expr

evaluate : Expr -> Int
evaluate (PrimInt x) = x
evaluate (Add x y) = evaluate x + evaluate y
evaluate (Sub x y) = evaluate x - evaluate y
evaluate (Mult x y) = evaluate x * evaluate y

maxMaybe : Ord a => Maybe a -> Maybe a -> Maybe a
maxMaybe Nothing x = x
maxMaybe x Nothing = x
maxMaybe (Just x) (Just y) = Just (max x y)

triangleSize : Shape -> Maybe Double
triangleSize tri@(Triangle _ _) = Just (area tri)
triangleSize _ = Nothing

biggestFound : Maybe Double -> Picture -> Maybe Double
biggestFound x (Primitive p) = maxMaybe x (triangleSize p)
biggestFound x (Combine pic pic1) = biggestFound (biggestFound x pic) pic1
biggestFound x (Rotate y pic) = biggestFound x pic
biggestFound x (Translate y z pic) = biggestFound x pic

biggestTriangle : Picture -> Maybe Double
biggestTriangle pic = biggestFound Nothing pic

data PowerSource = Petrol | Pedal

data Vehicle : PowerSource -> Type where
  Bicycle : Vehicle Pedal
  Unicycle : Vehicle Pedal
  Car : (fuel : Nat) -> Vehicle Petrol
  Bus : (fuel : Nat) -> Vehicle Petrol

wheels : Vehicle p -> Nat
wheels Bicycle = 2
wheels Unicycle = 1
wheels (Car fuel) = 4
wheels (Bus fuel) = 4

refuel : Vehicle Petrol -> Vehicle Petrol
refuel (Car fuel) = Car 100
refuel (Bus fuel) = Car 200

max_stars_repo_name: tekerson/type-driven-development

max_issues_repo_name: tekerson/type-driven-development

max_forks_repo_name: tekerson/type-driven-development


text:
import Data.String

-- examples taken from https://hsivonen.fi/string-length/

foo : String
foo = "ällo"

clef : String
clef = "Clef: 𝄞"

ällo : Int
ällo = 42

facepalm : String
facepalm = "🤦🏼♂"

family : String
family = "👨👨👧👧"

strId : String -> String
strId s = case strM s of
               StrNil => ""
               StrCons h t => strCons h t

main : IO ()
main = do printLn ällo
          putStrLn foo
          putStrLn $ strId foo
          printLn $ length foo
          putStrLn clef
          putStrLn $ cast $ assert_total $ strIndex clef 6
          printLn $ length clef
          putStrLn facepalm
          printLn $ length facepalm
          putStrLn family
          printLn $ length family
          putStrLn "Snowman: ☃"
          putStrLn "Wikipedia: $¢ह€한𐍈"


text:
module Main

import Data.List

main : IO ()
main = putStr $ concat $ mapMaybe Just ["Hello", " STG!\n"]

max_stars_repo_name: andorp/IdrisExtSTGCodegen

max_issues_repo_name: andorp/IdrisExtSTGCodegen

max_forks_repo_name: andorp/IdrisExtSTGCodegen


text:
module Examples

import Hardware
import Processor
--------------------------------------------------
--               helper functions

nil : Instruction
nil = DATA 0

accumR : Register
stopR : Register
incR : Register
boolR : Register
accumR = R1
incR = R2
stopR = R3
boolR = R4

dat : Int -> Instruction
dat x = DATA x

--------------------------------------------------
--               ex simple loop

simpleAsm : List Instruction
simpleAsm =
  [ ADD accumR accumR incR
  , EQUAL boolR accumR stopR
  , NOT boolR boolR
  , JUMPI boolR (-3)
  ]

export
simpleLoop : Memory
simpleLoop = MkMemory (MkRegisters 0 1 6 0 0 0) simpleAsm

max_stars_repo_name: nickgeoca/QVM

max_issues_repo_name: nickgeoca/QVM

max_forks_repo_name: nickgeoca/QVM


text:
module Units

%default total

data Unit = Degrees | Radians | Pixels | Meters
data Dim : Unit -> Type where
  Deg : Float -> Dim Degrees
  Rad : Float -> Dim Radians
  Pix : Float -> Dim Pixels
  M : Float -> Dim Meters

max_stars_repo_name: david-christiansen/idris-raytracer

max_issues_repo_name: david-christiansen/idris-raytracer

max_forks_repo_name: david-christiansen/idris-raytracer


text:
{-
Copyright 2019, Mokshasoft AB (mokshasoft.com)

This software may be distributed and modified according to the terms of
the BSD 2-Clause license. Note that NO WARRANTY is provided.
See "LICENSE_BSD2.txt" for details.
-}

module BareMetal.HwGpio

%access public export
%default total

{-
    Registers Definition
-}

gpioRevision : Bits32
gpioRevision =
    0x0
gpioSysconfig : Bits32
gpioSysconfig =
    0x10
gpioIrqstatusRaw : Bits32 -> Bits32
gpioIrqstatusRaw n =
    0x24 + (n * 4)
gpioIrqstatus : Bits32 -> Bits32
gpioIrqstatus n =
    0x2c + (n * 4)
gpioIrqstatusSet : Bits32 -> Bits32
gpioIrqstatusSet n =
    0x34 + (n * 4)
gpioIrqstatusClr : Bits32 -> Bits32
gpioIrqstatusClr n =
    0x3c + (n * 4)
gpioIrqwaken : Bits32 -> Bits32
gpioIrqwaken n =
    0x44 + (n * 4)
gpioSysstatus : Bits32
gpioSysstatus =
    0x114
gpioCtrl : Bits32
gpioCtrl =
    0x130
gpioOe : Bits32
gpioOe =
    0x134
gpioDatain : Bits32
gpioDatain =
    0x138
gpioDataout : Bits32
gpioDataout =
    0x13c
gpioLeveldetect : Bits32 -> Bits32
gpioLeveldetect n =
    0x140 + (n * 4)
gpioRisingdetect : Bits32
gpioRisingdetect =
    0x148
gpioFallingdetect : Bits32
gpioFallingdetect =
    0x14c
gpioDebouncenable : Bits32
gpioDebouncenable =
    0x150
gpioDebouncingtime : Bits32
gpioDebouncingtime =
    0x154
gpioCleardataout : Bits32
gpioCleardataout =
    0x190
gpioSetdataout : Bits32
gpioSetdataout =
    0x194

{-
    Field Definition Macros
-}

-- revision
gpioRevisionCustom : Bits32
gpioRevisionCustom =
    0x000000c0
gpioRevisionCustomShift : Bits32
gpioRevisionCustomShift =
    0x00000006

gpioRevisionFunc : Bits32
gpioRevisionFunc =
    0x0fff0000
gpioRevisionFuncShift : Bits32
gpioRevisionFuncShift =
    0x00000010

gpioRevisionMajor : Bits32
gpioRevisionMajor =
    0x00000700
gpioRevisionMajorShift : Bits32
gpioRevisionMajorShift =
    0x00000008

gpioRevisionMinor : Bits32
gpioRevisionMinor =
    0x0000003f
gpioRevisionMinorShift : Bits32
gpioRevisionMinorShift =
    0x00000000

gpioRevisionRtl : Bits32
gpioRevisionRtl =
    0x0000f800
gpioRevisionRtlShift : Bits32
gpioRevisionRtlShift =
    0x0000000b

gpioRevisionScheme : Bits32
gpioRevisionScheme =
    0xc0000000
gpioRevisionSchemeShift : Bits32
gpioRevisionSchemeShift =
    0x0000001e

-- sysconfig
gpioSysconfigAutoidle : Bits32
gpioSysconfigAutoidle =
    0x00000001
gpioSysconfigAutoidleShift : Bits32
gpioSysconfigAutoidleShift =
    0x00000000
gpioSysconfigAutoidleAutomatic : Bits32
gpioSysconfigAutoidleAutomatic =
    0x1
gpioSysconfigAutoidleFreerun : Bits32
gpioSysconfigAutoidleFreerun =
    0x0

gpioSysconfigEnawakeup : Bits32
gpioSysconfigEnawakeup =
    0x00000004
gpioSysconfigEnawakeupShift : Bits32
gpioSysconfigEnawakeupShift =
    0x00000002
gpioSysconfigEnawakeupDisable : Bits32
gpioSysconfigEnawakeupDisable =
    0x0
gpioSysconfigEnawakeupEnable : Bits32
gpioSysconfigEnawakeupEnable =
    0x1

gpioSysconfigIdlemode : Bits32
gpioSysconfigIdlemode =
    0x00000018
gpioSysconfigIdlemodeShift : Bits32
gpioSysconfigIdlemodeShift =
    0x00000003
gpioSysconfigIdlemodeForceidle : Bits32
gpioSysconfigIdlemodeForceidle =
    0x0
gpioSysconfigIdlemodeNoidle : Bits32
gpioSysconfigIdlemodeNoidle =
    0x1
gpioSysconfigIdlemodeSmartidle : Bits32
gpioSysconfigIdlemodeSmartidle =
    0x2
gpioSysconfigIdlemodeSmartidlewakeup : Bits32
gpioSysconfigIdlemodeSmartidlewakeup =
    0x3

gpioSysconfigSoftreset : Bits32
gpioSysconfigSoftreset =
    0x00000002
gpioSysconfigSoftresetShift : Bits32
gpioSysconfigSoftresetShift =
    0x00000001
gpioSysconfigSoftresetNormal : Bits32
gpioSysconfigSoftresetNormal =
    0x0
gpioSysconfigSoftresetReset : Bits32
gpioSysconfigSoftresetReset =
    0x1

-- irqstatusRaw0
gpioIrqstatusRaw0Intline : Bits32
gpioIrqstatusRaw0Intline =
    0xffffffff
gpioIrqstatusRaw0IntlineShift : Bits32
gpioIrqstatusRaw0IntlineShift =
    0x00000000

-- irqstatusRaw1
gpioIrqstatusRaw1Intline : Bits32
gpioIrqstatusRaw1Intline =
    0xffffffff
gpioIrqstatusRaw1IntlineShift : Bits32
gpioIrqstatusRaw1IntlineShift =
    0x00000000

-- irqstatus0
gpioIrqstatus0Intline : Bits32
gpioIrqstatus0Intline =
    0xffffffff
gpioIrqstatus0IntlineShift : Bits32
gpioIrqstatus0IntlineShift =
    0x00000000

-- irqstatus1
gpioIrqstatus1Intline : Bits32
gpioIrqstatus1Intline =
    0xffffffff
gpioIrqstatus1IntlineShift : Bits32
gpioIrqstatus1IntlineShift =
    0x00000000

-- irqstatusSet0
gpioIrqstatusSet0Intline : Bits32
gpioIrqstatusSet0Intline =
    0xffffffff
gpioIrqstatusSet0IntlineShift : Bits32
gpioIrqstatusSet0IntlineShift =
    0x00000000

-- irqstatusSet1
gpioIrqstatusSet1Intline : Bits32
gpioIrqstatusSet1Intline =
    0xffffffff
gpioIrqstatusSet1IntlineShift : Bits32
gpioIrqstatusSet1IntlineShift =
    0x00000000

-- irqstatusClr0
gpioIrqstatusClr0Intline : Bits32
gpioIrqstatusClr0Intline =
    0xffffffff
gpioIrqstatusClr0IntlineShift : Bits32
gpioIrqstatusClr0IntlineShift =
    0x00000000

-- irqstatusClr1
gpioIrqstatusClr1Intline : Bits32
gpioIrqstatusClr1Intline =
    0xffffffff
gpioIrqstatusClr1IntlineShift : Bits32
gpioIrqstatusClr1IntlineShift =
    0x00000000

-- sysstatus
gpioSysstatusResetdone : Bits32
gpioSysstatusResetdone =
    0x00000001
gpioSysstatusResetdoneShift : Bits32
gpioSysstatusResetdoneShift =
    0x00000000
gpioSysstatusResetdoneComplete : Bits32
gpioSysstatusResetdoneComplete =
    0x1
gpioSysstatusResetdoneOngoing : Bits32
gpioSysstatusResetdoneOngoing =
    0x0

-- ctrl
gpioCtrlDisablemodule : Bits32
gpioCtrlDisablemodule =
    0x00000001
gpioCtrlDisablemoduleShift : Bits32
gpioCtrlDisablemoduleShift =
    0x00000000
gpioCtrlDisablemoduleDisabled : Bits32
gpioCtrlDisablemoduleDisabled =
    0x1
gpioCtrlDisablemoduleEnabled : Bits32
gpioCtrlDisablemoduleEnabled =
    0x0

gpioCtrlGatingratio : Bits32
gpioCtrlGatingratio =
    0x00000006
gpioCtrlGatingratioShift : Bits32
gpioCtrlGatingratioShift =
    0x00000001
gpioCtrlGatingratioN1 : Bits32
gpioCtrlGatingratioN1 =
    0x0
gpioCtrlGatingratioN2 : Bits32
gpioCtrlGatingratioN2 =
    0x1
gpioCtrlGatingratioN4 : Bits32
gpioCtrlGatingratioN4 =
    0x2
gpioCtrlGatingratioN8 : Bits32
gpioCtrlGatingratioN8 =
    0x3

-- oe
gpioOeOutputen : Bits32
gpioOeOutputen =
    0xffffffff
gpioOeOutputenShift : Bits32
gpioOeOutputenShift =
    0x00000000
gpioOeOutputenDisabled : Bits32
gpioOeOutputenDisabled =
    0x1
gpioOeOutputenEnabled : Bits32
gpioOeOutputenEnabled =
    0x0

-- datain
gpioDatainDatain : Bits32
gpioDatainDatain =
    0xffffffff
gpioDatainDatainShift : Bits32
gpioDatainDatainShift =
    0x00000000

-- dataout
gpioDataoutDataout : Bits32
gpioDataoutDataout =
    0xffffffff
gpioDataoutDataoutShift : Bits32
gpioDataoutDataoutShift =
    0x00000000

-- leveldetect0
gpioLeveldetect0Leveldetect0 : Bits32
gpioLeveldetect0Leveldetect0 =
    0xffffffff
gpioLeveldetect0Leveldetect0Shift : Bits32
gpioLeveldetect0Leveldetect0Shift =
    0x00000000
gpioLeveldetect0Leveldetect0Disabled : Bits32
gpioLeveldetect0Leveldetect0Disabled =
    0x0
gpioLeveldetect0Leveldetect0Enabled : Bits32
gpioLeveldetect0Leveldetect0Enabled =
    0x1

-- leveldetect1
gpioLeveldetect1Leveldetect1 : Bits32
gpioLeveldetect1Leveldetect1 =
    0xffffffff
gpioLeveldetect1Leveldetect1Shift : Bits32
gpioLeveldetect1Leveldetect1Shift =
    0x00000000
gpioLeveldetect1Leveldetect1Disabled : Bits32
gpioLeveldetect1Leveldetect1Disabled =
    0x0
gpioLeveldetect1Leveldetect1Enabled : Bits32
gpioLeveldetect1Leveldetect1Enabled =
    0x1

-- risingdetect
gpioRisingdetectRisingdetect : Bits32
gpioRisingdetectRisingdetect =
    0xffffffff
gpioRisingdetectRisingdetectShift : Bits32
gpioRisingdetectRisingdetectShift =
    0x00000000
gpioRisingdetectRisingdetectDisabled : Bits32
gpioRisingdetectRisingdetectDisabled =
    0x0
gpioRisingdetectRisingdetectEnabled : Bits32
gpioRisingdetectRisingdetectEnabled =
    0x1

-- fallingdetect
gpioFallingdetectFallingdetect : Bits32
gpioFallingdetectFallingdetect =
    0xffffffff
gpioFallingdetectFallingdetectShift : Bits32
gpioFallingdetectFallingdetectShift =
    0x00000000
gpioFallingdetectFallingdetectDisabled : Bits32
gpioFallingdetectFallingdetectDisabled =
    0x0
gpioFallingdetectFallingdetectEnabled : Bits32
gpioFallingdetectFallingdetectEnabled =
    0x1

-- debouncenable
gpioDebouncenableDebounceenable : Bits32
gpioDebouncenableDebounceenable =
    0xffffffff
gpioDebouncenableDebounceenableShift : Bits32
gpioDebouncenableDebounceenableShift =
    0x00000000
gpioDebouncenableDebounceenableDebounce : Bits32
gpioDebouncenableDebounceenableDebounce =
    0x1
gpioDebouncenableDebounceenableNodebounce : Bits32
gpioDebouncenableDebounceenableNodebounce =
    0x0

-- debouncingtime
gpioDebouncingtimeDebouncetime : Bits32
gpioDebouncingtimeDebouncetime =
    0x000000ff
gpioDebouncingtimeDebouncetimeShift : Bits32
gpioDebouncingtimeDebouncetimeShift =
    0x00000000

-- cleardataout
gpioCleardataoutIntline : Bits32
gpioCleardataoutIntline =
    0xffffffff
gpioCleardataoutIntlineShift : Bits32
gpioCleardataoutIntlineShift =
    0x00000000

-- setdataout
gpioSetdataoutIntline : Bits32
gpioSetdataoutIntline =
    0xffffffff
gpioSetdataoutIntlineShift : Bits32
gpioSetdataoutIntlineShift =
    0x00000000

max_stars_repo_name: mokshasoft/bare-metal-idris-drivers

max_issues_repo_name: mokshasoft/bare-metal-idris-drivers

max_forks_repo_name: mokshasoft/bare-metal-idris-drivers


text:
module Task.Universe

import Control.Monad.Ref

import Data.String
import public Data.Universe

import Helpers

%default total
%access public export

-- Labels ----------------------------------------------------------------------

Label : Type
Label = String

isLabel : String -> Bool
isLabel s               with ( strM s )
 isLabel ""             | StrNil      = False
 isLabel (strCons c cs) | StrCons c _ = isUpper c

-- Primitive types -------------------------------------------------------------

data PrimitiveTy
  = UNIT
  | BOOL
  | INT
  | STRING

-- Lemmas --

Uninhabited (UNIT = BOOL) where
  uninhabited Refl impossible

Uninhabited (UNIT = INT) where
  uninhabited Refl impossible

Uninhabited (UNIT = STRING) where
  uninhabited Refl impossible

Uninhabited (BOOL = INT) where
  uninhabited Refl impossible

Uninhabited (BOOL = STRING) where
  uninhabited Refl impossible

Uninhabited (INT = STRING) where
  uninhabited Refl impossible

-- Universe --

DecEq PrimitiveTy where
  decEq UNIT   UNIT   = Yes Refl
  decEq BOOL   BOOL   = Yes Refl
  decEq INT    INT    = Yes Refl
  decEq STRING STRING = Yes Refl
  decEq UNIT   BOOL   = No absurd
  decEq BOOL   UNIT   = No (negEqSym absurd)
  decEq UNIT   INT    = No absurd
  decEq INT    UNIT   = No (negEqSym absurd)
  decEq UNIT   STRING = No absurd
  decEq STRING UNIT   = No (negEqSym absurd)
  decEq BOOL   INT    = No absurd
  decEq INT    BOOL   = No (negEqSym absurd)
  decEq BOOL   STRING = No absurd
  decEq STRING BOOL   = No (negEqSym absurd)
  decEq INT    STRING = No absurd
  decEq STRING INT    = No (negEqSym absurd)

Universe PrimitiveTy where
  typeOf UNIT   = ()
  typeOf BOOL   = Bool
  typeOf INT    = Int
  typeOf STRING = String

  show UNIT   = %implementation
  show BOOL   = %implementation
  show INT    = %implementation
  show STRING = %implementation

  eq UNIT   = %implementation
  eq BOOL   = %implementation
  eq INT    = %implementation
  eq STRING = %implementation

-- Full type universe ----------------------------------------------------------

data Ty
  = PAIR Ty Ty
  | LIST Ty
  | LOC Ty
  | PRIM PrimitiveTy

-- Lemmas --

Uninhabited (PAIR _ _ = LIST _) where
  uninhabited Refl impossible

Uninhabited (PAIR _ _ = LOC _) where
  uninhabited Refl impossible

Uninhabited (PAIR _ _ = PRIM _) where
  uninhabited Refl impossible

Uninhabited (LIST _ = LOC _) where
  uninhabited Refl impossible

Uninhabited (LIST _ = PRIM _) where
  uninhabited Refl impossible

Uninhabited (LOC _ = PRIM _) where
  uninhabited Refl impossible

private
list_neq : (a = b -> Void) -> (LIST a = LIST b) -> Void
list_neq contra Refl = contra Refl

private
loc_neq : (a = b -> Void) -> (LOC a = LOC b) -> Void
loc_neq contra Refl = contra Refl

private
prim_neq : (p = q -> Void) -> (PRIM p = PRIM q) -> Void
prim_neq contra Refl = contra Refl

private
snd_neq : (b = b' -> Void) -> (PAIR a b = PAIR a b') -> Void
snd_neq contra Refl = contra Refl

private
fst_neq : (a = a' -> Void) -> (PAIR a b = PAIR a' b) -> Void
fst_neq contra Refl = contra Refl

private
both_neq : (a = a' -> Void) -> (b = b' -> Void) -> (PAIR a b = PAIR a' b') -> Void
both_neq contra_a contra_b Refl = contra_a Refl

-- Decidablility --

DecEq Ty where
  decEq (PAIR a b) (PAIR a' b')     with (decEq a a')
    decEq (PAIR a b) (PAIR a b')    | (Yes Refl)  with (decEq b b')
      decEq (PAIR a b) (PAIR a b)   | (Yes Refl)  | (Yes Refl)    = Yes Refl
      decEq (PAIR a b) (PAIR a b')  | (Yes Refl)  | (No contra)   = No (snd_neq contra)
    decEq (PAIR a b) (PAIR a' b')   | (No contra) with (decEq b b')
      decEq (PAIR a b) (PAIR a' b)  | (No contra) | (Yes Refl)    = No (fst_neq contra)
      decEq (PAIR a b) (PAIR a' b') | (No contra) | (No contra')  = No (both_neq contra contra')

  decEq (LIST a)  (LIST b)   with (decEq a b)
    decEq (LIST b)  (LIST b) | (Yes Refl)                         = Yes Refl
    decEq (LIST a)  (LIST b) | (No contra)                        = No (list_neq contra)

  decEq (LOC a)  (LOC b)   with (decEq a b)
    decEq (LOC b)  (LOC b) | (Yes Refl)                           = Yes Refl
    decEq (LOC a)  (LOC b) | (No contra)                          = No (loc_neq contra)

  decEq (PRIM p)  (PRIM q)   with (decEq p q)
    decEq (PRIM q)  (PRIM q) | (Yes Refl)                         = Yes Refl
    decEq (PRIM p)  (PRIM q) | (No contra)                        = No (prim_neq contra)

  decEq (PAIR _ _) (LIST _)                                       = No absurd
  decEq (LIST _)   (PAIR _ _)                                     = No (negEqSym absurd)
  decEq (PAIR _ _) (LOC _)                                        = No absurd
  decEq (LOC _)    (PAIR _ _)                                     = No (negEqSym absurd)
  decEq (PAIR _ _) (PRIM _)                                       = No absurd
  decEq (PRIM _)   (PAIR _ _)                                     = No (negEqSym absurd)

  decEq (LIST _)   (LOC _)                                        = No absurd
  decEq (LOC _)    (LIST _)                                       = No (negEqSym absurd)
  decEq (LIST _)   (PRIM _)                                       = No absurd
  decEq (PRIM _)   (LIST _)                                       = No (negEqSym absurd)

  decEq (LOC _)    (PRIM _)                                       = No absurd
  decEq (PRIM _)   (LOC _)                                        = No (negEqSym absurd)

Eq (IORef a) where
  (==) r1 r2 = False

Show (IORef a) where
  show ref = "<ref>"

Universe Ty where
  typeOf (PAIR a b) = ( typeOf a, typeOf b )
  typeOf (LIST a)   = List (typeOf a)
  typeOf (LOC a)    = IORef (typeOf a) --FIXME: is this ok??? Should be parametrised over `MonadRef l m`...
  typeOf (PRIM p)   = typeOf p

  show (PAIR x y) with ( show x, show y )
    | ( show_x, show_y ) = %implementation
  show (LIST x) with ( show x )
    | show_x = %implementation
  show (LOC x) with ( show x )
    | show_x = %implementation
  show (PRIM x) with ( show x )
    | show_x = %implementation

  eq (PAIR x y) with ( eq x, eq y )
    | ( eq_x, eq_y ) = %implementation
  eq (LIST x) with ( eq x )
    | eq_x = %implementation
  eq (LOC x) with ( eq x )
    | eq_x = %implementation
  eq (PRIM x) with ( eq x )
    | eq_x = %implementation

-- Parsing --

parse : String -> Maybe (b : Ty ** ( typeOf b ))
parse "()"                                                        = Just (PRIM UNIT ** ())
parse "True"                                                      = Just (PRIM BOOL ** True)
parse "False"                                                     = Just (PRIM BOOL ** False)
parse s   with (the (Maybe Int) (parseInteger s))
  parse s | Just int                                              = Just (PRIM INT ** int)
  parse s | Nothing                        with (decons s)
    parse (between '"' '"' rest) | Nothing | (Multi '"' '"' rest) = Just (PRIM STRING ** rest)
    parse _                      | Nothing | _                    = Nothing

--FIXME: add pairs and lists, but no locs

max_stars_repo_name: mklinik/task-semantics

max_issues_repo_name: mklinik/task-semantics

max_forks_repo_name: mklinik/task-semantics


text:
-- -------------------------------------------------------------- [ Parser.idr ]
-- Description : A simple parser for command options.
-- Copyright   : (c) Jan de Muijnck-Hughes
-- License     : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
module ArgParse.Parser

import ArgParse.Lexer
import ArgParse.Parser.API

import ArgParse.Model

%access private

-- ----------------------------------------------------------------- [ Parsers ]

flagLong : Rule Arg
flagLong = do
  l <- longFlag
  pure $ Flag l

flagShort : Rule Arg
flagShort = do
   s <- shortFlag
   pure $ Flag s

kvLong : Rule Arg
kvLong = do
    key <- longFlag
    equals
    value <- (arg <|> quoted)
    pure $ KeyValue key value

kvShort : Rule Arg
kvShort = do
    k <- shortFlag
    v <- (arg <|> quoted)
    pure $ KeyValue k v

options : Rule Arg
options = kvShort <|> kvLong <|> flagShort <|> flagLong <|> (do fs <- arg; pure $ File fs)

args : EmptyRule $ List Arg
args = do
    os <- many options
    pure $ os

public export
data ParseError = ParseFail String (Maybe (Int, Int)) (List Token)
                | LexFail (Int, Int, String)

export
Show ParseError where
  show (ParseFail err loc toks)
      = "Parse error: " ++ err ++ " at " ++ show loc ++ "\n" ++ show toks
  show (LexFail (c, l, str))
      = "Lex error at " ++ show (c, l) ++ " input: " ++ str

export
parseArgs : String -> Either ParseError (List Arg)
parseArgs str =
  case Lexer.lex str of
    Left err => Left (LexFail err)

    Right toks =>
      case parse toks args of

            Left (Error err []) =>
              Left $ ParseFail err Nothing []

            Left (Error err (t :: ts)) =>
              Left $ ParseFail err (Just (line t, col t))
                                   (map tok (t :: ts))
            Right (val, _) => Right val

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

max_stars_repo_name: jfdm/idris-argparse

max_issues_repo_name: jfdm/idris-argparse

max_forks_repo_name: jfdm/idris-argparse


text:
module Js.Json
{-
import public Lightyear
import public Lightyear.Char
import public Lightyear.Strings

import Pruviloj.Core
import public Data.SortedMap

public export
data JsonValue = JsonString String
               | JsonNumber Double
               | JsonBool Bool
               | JsonNull
               | JsonArray (List JsonValue)
               | JsonObject (SortedMap String JsonValue)

{-
export
Eq JsonValue where
  (==) (JsonString x) (JsonString y) = x == y
  (==) (JsonNumber x) (JsonNumber y) = x == y
  (==) JsonNull JsonNull = True
  (==) (JsonArray x) (JsonArray y) = x == y
  (==) (JsonObject x) (JsonObject y) = toList x == toList y
  (==) _ _ = False
-}

export
Show JsonValue where
  show (JsonString s)   = show s
  show (JsonNumber x)   = show x
  show (JsonBool True ) = "true"
  show (JsonBool False) = "false"
  show  JsonNull        = "null"
  show (JsonArray  xs)  = show xs
  show (JsonObject xs)  =
      "{" ++ intercalate ", " (map fmtItem $ SortedMap.toList xs) ++ "}"
    where
      intercalate : String -> List String -> String
      intercalate sep [] = ""
      intercalate sep [x] = x
      intercalate sep (x :: xs) = x ++ sep ++ intercalate sep xs

      fmtItem (k, v) = show k ++ ": " ++ show v

hex : Parser Int
hex = do
  c <- map (ord . toUpper) $ satisfy isHexDigit
  pure $ if c >= ord '0' && c <= ord '9' then c - ord '0'
                                         else 10 + c - ord 'A'

hexQuad : Parser Int
hexQuad = do
  a <- hex
  b <- hex
  c <- hex
  d <- hex
  pure $ a * 4096 + b * 256 + c * 16 + d

specialChar : Parser Char
specialChar = do
  c <- satisfy (const True)
  case c of
    '"'  => pure '"'
    '\\' => pure '\\'
    '/'  => pure '/'
    'b'  => pure '\b'
    'f'  => pure '\f'
    'n'  => pure '\n'
    'r'  => pure '\r'
    't'  => pure '\t'
    'u'  => map chr hexQuad
    _    => fail "expected special char"

jsonString' : Parser (List Char)
jsonString' = (char '"' *!> pure Prelude.List.Nil) <|> do
  c <- satisfy (/= '"')
  if (c == '\\') then map (::) specialChar <*> jsonString'
                 else map (c ::) jsonString'

jsonString : Parser String
jsonString = char '"' *> map pack jsonString' <?> "JSON string"

-- inspired by Haskell's Data.Scientific module
record Scientific where
  constructor MkScientific
  coefficient : Integer
  exponent : Integer

scientificToFloat : Scientific -> Double
scientificToFloat (MkScientific c e) = fromInteger c * exp
  where exp = if e < 0 then 1 / pow 10 (fromIntegerNat (- e))
                       else pow 10 (fromIntegerNat e)

parseScientific : Parser Scientific
parseScientific = do sign <- maybe 1 (const (-1)) `map` opt (char '-')
                     digits <- some digit
                     hasComma <- isJust `map` opt (char '.')
                     decimals <- if hasComma then some digit else pure Prelude.List.Nil
                     hasExponent <- isJust `map` opt (char 'e')
                     exponent <- if hasExponent then integer else pure 0
                     pure $ MkScientific (sign * fromDigits (digits ++ decimals))
                                         (exponent - cast (length decimals))
  where fromDigits : List (Fin 10) -> Integer
        fromDigits = foldl (\a, b => 10 * a + cast b) 0

jsonNumber : Parser Double
jsonNumber = map scientificToFloat parseScientific

jsonBool : Parser Bool
jsonBool  =  (char 't' >! string "rue"  *> pure True)
         <|> (char 'f' >! string "alse" *> pure False) <?> "JSON Bool"

jsonNull : Parser ()
jsonNull = (char 'n' >! string "ull" >! pure ()) <?> "JSON Null"

mutual
  jsonArray : Parser (List JsonValue)
  jsonArray = char '[' *!> (jsonValue `sepBy` (char ',')) <* char ']'

  keyValuePair : Parser (String, JsonValue)
  keyValuePair = do
    key <- spaces *> jsonString <* spaces
    char ':'
    value <- jsonValue
    pure (key, value)

  jsonObject : Parser (SortedMap String JsonValue)
  jsonObject = map fromList (char '{' >! (keyValuePair `sepBy` char ',') <* char '}')

  jsonValue' : Parser JsonValue
  jsonValue' =  (map JsonString jsonString)
            <|> (map JsonNumber jsonNumber)
            <|> (map JsonBool   jsonBool)
            <|> (pure JsonNull <* jsonNull)
            <|>| map JsonArray  jsonArray
            <|>| map JsonObject jsonObject

  jsonValue : Parser JsonValue
  jsonValue = spaces *> jsonValue' <* spaces

jsonToplevelValue : Parser JsonValue
jsonToplevelValue = (map JsonArray jsonArray) <|> (map JsonObject jsonObject)

export
parsJson : String -> Either String JsonValue
parsJson s = parse jsonValue s

public export
interface ToJson a where
  toJson : a -> JsonValue

public export
interface FromJson a where
  fromJson : JsonValue -> Either String a

export
interface (ToJson a, FromJson a) => BothJson a where

export
(ToJson a, FromJson a) => BothJson a where

export
FromJson String where
  fromJson (JsonString s) = Right s
  fromJson o = Left $ "fromJson: " ++ show o ++ " is not a String"

export
ToJson String where
  toJson s = JsonString s

export
FromJson JsonValue where
  fromJson = Right

export
ToJson JsonValue where
  toJson = id

export
FromJson () where
  fromJson JsonNull = Right ()

export
ToJson () where
  toJson () = JsonNull

export
ToJson a => ToJson (List a) where
  toJson x = JsonArray $ map toJson x

export
FromJson a => FromJson (List a) where
  fromJson (JsonArray x) = sequence $ map fromJson x

export
ToJson a => ToJson (Vect n a) where
  toJson x = JsonArray $ toList $ map toJson x

vectFromJson : FromJson a => JsonValue -> Either String (Vect n a)
vectFromJson {n} {a} (JsonArray x) =
  let p1 = the (List (Either String a)) $ map fromJson x
      p2 = sequence $ fromList p1
  in case exactLength n <$> p2 of
        Right (Just z) => Right z

export
FromJson a => FromJson (Vect n a) where
  fromJson = vectFromJson

export
(ToJson a, ToJson b) => ToJson (a,b) where
  toJson (x, y) = JsonArray [toJson x, toJson y]

export
(FromJson a, FromJson b) => FromJson (a, b) where
  fromJson (JsonArray [x, y]) = MkPair <$> fromJson x <*> fromJson y

export
decode : FromJson a => String -> Either String a
decode x = parsJson x >>= fromJson

export
encode : ToJson a => a -> String
encode x = show $ toJson x
-}

max_stars_repo_name: rbarreiro/idrisjs

max_issues_repo_name: prozacchiwawa/idrisjs

max_forks_repo_name: prozacchiwawa/idrisjs


text:
module Commons.Control.Logging.Logger

import Control.IOExcept
import Control.ST

import Data.AVL.Dict

%default total
%access export

public export
interface (Show ty, Eq ty, Ord ty) => LogElement ty where

public export
interface Logging (m : Type -> Type)
  where
    Logger : Type -> Type -> Type

    start : (LogElement e, LogElement c)
         => (levels     : List (e, Nat))
         -> (categories : List c)
         -> (formatter  : c -> e -> Nat -> String -> String)
         -> ST m Var [add $ Logger e c]

    stop : (logger : Var) -> ST m () [remove logger (Logger e c)]

    setCategories : (logger : Var)
                 -> (categories : List c)
                 -> ST m () [logger ::: Logger e c]

    setEventLoggingLevel : (LogElement e)
                        => (logger : Var)
                        -> (event  : e)
                        -> (level  : Nat)
                        -> ST m () [logger ::: Logger e c]

    getLoggingState : (logger : Var)
                   -> ST m (List (e, Nat), List c) [logger ::: Logger e c]

    log : (LogElement e, LogElement c)
       => (logger   : Var)
       -> (category : c)
       -> (event    : e)
       -> (level    : Nat)
       -> (message  : String)
       -> ST m () [logger ::: Logger e c]

record LoggingState x y where
  constructor MkState
  events     : Dict x Nat
  categories : List y
  formatter  : y -> x -> Nat -> String -> String

Logging IO where
  Logger x y = State (LoggingState x y)

  start levels categories formatter = do
    let startST = MkState (fromList levels) categories formatter
    logger <- new startST
    pure logger

  stop logger = delete logger

  setCategories logger cats =
    update logger (\st => record {categories = cats} st)

  setEventLoggingLevel logger event level =
    update logger (record {events $= (insert event level)})

  getLoggingState logger = do
    st <- read logger
    pure (toList (events st), categories st)

  log logger category event level msg = do
    st <- read logger
    let curr_lvl = fromMaybe Z (lookup event (events st))
    case compare level curr_lvl of
      GT => pure ()
      _  => do
        let can_log = elem category (categories st) || isNil (categories st)
        if not can_log
          then pure ()
          else putStrLn $ (formatter st) category event level msg

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

max_stars_repo_name: jfdm/idris-common

max_issues_repo_name: jfdm/idris-common

max_forks_repo_name: jfdm/idris-common


text:
module Web.Raw.Mediasource

import JS
import Web.Internal.MediasourcePrim
import Web.Internal.Types

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

namespace MediaSource

  export
  new : JSIO MediaSource
  new = primJS $ MediaSource.prim__new

  export
  isTypeSupported : (type : String) -> JSIO Bool
  isTypeSupported a = tryJS "MediaSource.isTypeSupported"
                    $ MediaSource.prim__isTypeSupported a

  export
  activeSourceBuffers : (obj : MediaSource) -> JSIO SourceBufferList
  activeSourceBuffers a = primJS $ MediaSource.prim__activeSourceBuffers a

  export
  duration : MediaSource -> Attribute True I Double
  duration v = fromPrim "MediaSource.getduration"
                        prim__duration
                        prim__setDuration
                        v

  export
  onsourceclose : MediaSource -> Attribute False Maybe EventHandlerNonNull
  onsourceclose v = fromNullablePrim "MediaSource.getonsourceclose"
                                     prim__onsourceclose
                                     prim__setOnsourceclose
                                     v

  export
  onsourceended : MediaSource -> Attribute False Maybe EventHandlerNonNull
  onsourceended v = fromNullablePrim "MediaSource.getonsourceended"
                                     prim__onsourceended
                                     prim__setOnsourceended
                                     v

  export
  onsourceopen : MediaSource -> Attribute False Maybe EventHandlerNonNull
  onsourceopen v = fromNullablePrim "MediaSource.getonsourceopen"
                                    prim__onsourceopen
                                    prim__setOnsourceopen
                                    v

  export
  readyState : (obj : MediaSource) -> JSIO ReadyState
  readyState a = tryJS "MediaSource.readyState" $ MediaSource.prim__readyState a

  export
  sourceBuffers : (obj : MediaSource) -> JSIO SourceBufferList
  sourceBuffers a = primJS $ MediaSource.prim__sourceBuffers a

  export
  addSourceBuffer : (obj : MediaSource) -> (type : String) -> JSIO SourceBuffer
  addSourceBuffer a b = primJS $ MediaSource.prim__addSourceBuffer a b

  export
  clearLiveSeekableRange : (obj : MediaSource) -> JSIO ()
  clearLiveSeekableRange a = primJS $ MediaSource.prim__clearLiveSeekableRange a

  export
  endOfStream :  (obj : MediaSource)
              -> (error : Optional EndOfStreamError)
              -> JSIO ()
  endOfStream a b = primJS $ MediaSource.prim__endOfStream a (toFFI b)

  export
  endOfStream' : (obj : MediaSource) -> JSIO ()
  endOfStream' a = primJS $ MediaSource.prim__endOfStream a undef

  export
  removeSourceBuffer :  (obj : MediaSource)
                     -> (sourceBuffer : SourceBuffer)
                     -> JSIO ()
  removeSourceBuffer a b = primJS $ MediaSource.prim__removeSourceBuffer a b

  export
  setLiveSeekableRange :  (obj : MediaSource)
                       -> (start : Double)
                       -> (end : Double)
                       -> JSIO ()
  setLiveSeekableRange a b c = primJS
                             $ MediaSource.prim__setLiveSeekableRange a b c

namespace SourceBuffer

  export
  appendWindowEnd : SourceBuffer -> Attribute True I Double
  appendWindowEnd v = fromPrim "SourceBuffer.getappendWindowEnd"
                               prim__appendWindowEnd
                               prim__setAppendWindowEnd
                               v

  export
  appendWindowStart : SourceBuffer -> Attribute True I Double
  appendWindowStart v = fromPrim "SourceBuffer.getappendWindowStart"
                                 prim__appendWindowStart
                                 prim__setAppendWindowStart
                                 v

  export
  audioTracks : (obj : SourceBuffer) -> JSIO AudioTrackList
  audioTracks a = primJS $ SourceBuffer.prim__audioTracks a

  export
  buffered : (obj : SourceBuffer) -> JSIO TimeRanges
  buffered a = primJS $ SourceBuffer.prim__buffered a

  export
  mode : SourceBuffer -> Attribute True I AppendMode
  mode v = fromPrim "SourceBuffer.getmode" prim__mode prim__setMode v

  export
  onabort : SourceBuffer -> Attribute False Maybe EventHandlerNonNull
  onabort v = fromNullablePrim "SourceBuffer.getonabort"
                               prim__onabort
                               prim__setOnabort
                               v

  export
  onerror : SourceBuffer -> Attribute False Maybe EventHandlerNonNull
  onerror v = fromNullablePrim "SourceBuffer.getonerror"
                               prim__onerror
                               prim__setOnerror
                               v

  export
  onupdate : SourceBuffer -> Attribute False Maybe EventHandlerNonNull
  onupdate v = fromNullablePrim "SourceBuffer.getonupdate"
                                prim__onupdate
                                prim__setOnupdate
                                v

  export
  onupdateend : SourceBuffer -> Attribute False Maybe EventHandlerNonNull
  onupdateend v = fromNullablePrim "SourceBuffer.getonupdateend"
                                   prim__onupdateend
                                   prim__setOnupdateend
                                   v

  export
  onupdatestart : SourceBuffer -> Attribute False Maybe EventHandlerNonNull
  onupdatestart v = fromNullablePrim "SourceBuffer.getonupdatestart"
                                     prim__onupdatestart
                                     prim__setOnupdatestart
                                     v

  export
  textTracks : (obj : SourceBuffer) -> JSIO TextTrackList
  textTracks a = primJS $ SourceBuffer.prim__textTracks a

  export
  timestampOffset : SourceBuffer -> Attribute True I Double
  timestampOffset v = fromPrim "SourceBuffer.gettimestampOffset"
                               prim__timestampOffset
                               prim__setTimestampOffset
                               v

  export
  updating : (obj : SourceBuffer) -> JSIO Bool
  updating a = tryJS "SourceBuffer.updating" $ SourceBuffer.prim__updating a

  export
  videoTracks : (obj : SourceBuffer) -> JSIO VideoTrackList
  videoTracks a = primJS $ SourceBuffer.prim__videoTracks a

  export
  abort : (obj : SourceBuffer) -> JSIO ()
  abort a = primJS $ SourceBuffer.prim__abort a

  export
  appendBuffer :  (obj : SourceBuffer)
               -> (data_ : NS I [ Int8Array
                                , Int16Array
                                , Int32Array
                                , UInt8Array
                                , UInt8Array
                                , UInt8Array
                                , UInt8ClampedArray
                                , Float32Array
                                , Float64Array
                                , DataView
                                , ArrayBuffer
                                ])
               -> JSIO ()
  appendBuffer a b = primJS $ SourceBuffer.prim__appendBuffer a (toFFI b)

  export
  remove : (obj : SourceBuffer) -> (start : Double) -> (end : Double) -> JSIO ()
  remove a b c = primJS $ SourceBuffer.prim__remove a b c

namespace SourceBufferList

  export
  get : (obj : SourceBufferList) -> (index : Bits32) -> JSIO SourceBuffer
  get a b = primJS $ SourceBufferList.prim__get a b

  export
  length : (obj : SourceBufferList) -> JSIO Bits32
  length a = primJS $ SourceBufferList.prim__length a

  export
  onaddsourcebuffer :  SourceBufferList
                    -> Attribute False Maybe EventHandlerNonNull
  onaddsourcebuffer v = fromNullablePrim "SourceBufferList.getonaddsourcebuffer"
                                         prim__onaddsourcebuffer
                                         prim__setOnaddsourcebuffer
                                         v

  export
  onremovesourcebuffer :  SourceBufferList
                       -> Attribute False Maybe EventHandlerNonNull
  onremovesourcebuffer v = fromNullablePrim "SourceBufferList.getonremovesourcebuffer"
                                            prim__onremovesourcebuffer
                                            prim__setOnremovesourcebuffer
                                            v


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

import Data.String

import Language.SystemVerilog.MetaTypes

%default total

public export
data TError = IdentifierNotFound String
            | UnexpectedType Ty
            | MalformedExpr
            | General String
            | Nested String TError

export
Show TError where
  show (IdentifierNotFound x) = unwords ["Identifier Not Found:", show x]
  show (UnexpectedType x) = unwords ["Unexpected Type:", show x]
  show MalformedExpr = "Malformed Expression"
  show (General err) = unwords ["Generic Error:", err]
  show (Nested desc err) = desc ++ "\n" ++ show err

max_stars_repo_name: border-patrol/lightclick

max_issues_repo_name: border-patrol/lightclick

max_forks_repo_name: border-patrol/lightclick


text:
-- Intuitionistic propositional logic, PHOAS approach, initial encoding

module Pi.Ip

%default total

-- Types

infixl 2 :&&
infixl 1 :||
infixr 0 :=>
data Ty : Type where
  UNIT  :             Ty
  (:=>) : Ty -> Ty -> Ty
  (:&&) : Ty -> Ty -> Ty
  (:||) : Ty -> Ty -> Ty
  FALSE :             Ty

infixr 0 :<=>
(:<=>) : Ty -> Ty -> Ty
(:<=>) a b = (a :=> b) :&& (b :=> a)

NOT : Ty -> Ty
NOT a = a :=> FALSE

TRUE : Ty
TRUE = FALSE :=> FALSE

-- Context and truth judgement

Cx : Type
Cx = Ty -> Type

isTrue : Ty -> Cx -> Type
isTrue a tc = tc a

-- Terms

infixl 1 :$
data Tm : Cx -> Ty -> Type where
  var   : isTrue a tc                -> Tm tc a
  lam'  : (isTrue a tc -> Tm tc b)   -> Tm tc (a :=> b)
  (:$)  : Tm tc (a :=> b) -> Tm tc a -> Tm tc b
  pair  : Tm tc a         -> Tm tc b -> Tm tc (a :&& b)
  fst   : Tm tc (a :&& b)            -> Tm tc a
  snd   : Tm tc (a :&& b)            -> Tm tc b
  left  : Tm tc a                    -> Tm tc (a :|| b)
  right : Tm tc b                    -> Tm tc (a :|| b)
  case' : Tm tc (a :|| b) -> (isTrue a tc -> Tm tc c) -> (isTrue b tc -> Tm tc c) -> Tm tc c
  abort : Tm tc FALSE                -> Tm tc a

lam'' : (Tm tc a -> Tm tc b) -> Tm tc (a :=> b)
lam'' f = lam' $ \x => f (var x)

case'' : Tm tc (a :|| b) -> (Tm tc a -> Tm tc c) -> (Tm tc b -> Tm tc c) -> Tm tc c
case'' xy f g = case' xy (\x => f (var x)) (\y => g (var y))

syntax "lam" {a} ":=>" [b]   = lam'' (\a => b)
syntax "[" [a] "," [b] "]"   = pair a b
syntax "case" [ab] "of" {a} ":=>" [c1] or {b} ":=>" [c2] = case'' ab (\a => c1) (\b => c2)

Thm : Ty -> Type
Thm a = {tc : Cx} -> Tm tc a

-- Example theorems

t1 : Thm (a :=> NOT a :=> b)
t1 =
  lam x :=>
    lam f :=> abort (f :$ x)

t2 : Thm (NOT a :=> a :=> b)
t2 =
  lam f :=>
    lam x :=> abort (f :$ x)

t3 : Thm (a :=> NOT (NOT a))
t3 =
  lam x :=>
    lam f :=> f :$ x

t4 : Thm (NOT a :<=> NOT (NOT (NOT a)))
t4 =
  [ lam f :=>
      lam g :=> g :$ f
  , lam g :=>
      lam x :=> g :$ (lam f :=> f :$ x)
  ]

max_stars_repo_name: mietek/formal-logic

max_issues_repo_name: mietek/formal-logic

max_forks_repo_name: mietek/formal-logic


text:
module Control.App.Console

import public Control.App

public export
interface Console e where
  putChar : Char -> App {l} e ()
  putStr : String -> App {l} e ()
  getChar : App {l} e Char
  getLine : App {l} e String

export
PrimIO e => Console e where
  putChar c = primIO $ putChar c
  putStr str = primIO $ putStr str
  getChar = primIO getChar
  getLine = primIO getLine

export
putStrLn : Console e => String -> App {l} e ()
putStrLn str = putStr (str ++ "\n")

export
putCharLn : Console e => Char -> App {l} e ()
putCharLn c = putStrLn $ strCons c ""

export
print : (Console e, Show a) => a -> App {l} e ()
print x = putStr $ show x

export
printLn : (Console e, Show a) => a -> App {l} e ()
printLn x = putStrLn $ show x


text:
module Procedures

import DataTypes
import Environment

%access public export

isProcedure : PrimitiveLispFunc
isProcedure [LispFunc _ _ _ _ _] = pure $ LispBool True
isProcedure [LispPrimitiveFunc _ _] = pure $ LispBool True
isProcedure [_] = pure $ LispBool False
isProcedure args = Left $ NumArgs (MinMax 1 1) (cast $ length args) args

procedurePrimitives : List (String, PrimitiveLispFunc)
procedurePrimitives =
    [ ("procedure?", isProcedure)
    ]

max_stars_repo_name: ebenpack/lidrisp

max_issues_repo_name: ebenpack/lidrisp

max_forks_repo_name: ebenpack/lidrisp


text:
module Main

main : IO ()
main = do
    printLn $ divNat 1809022195644390369852458 91238741987
    printLn $ div (-432642342742368327462378462387) 36473264372

    -- values at the border between C ints and bignums
    printLn $ div 1073741822 73892
    printLn $ div 1073741823 73892
    printLn $ div 1073741824 73892
    printLn $ div (-1073741823) 73892
    printLn $ div (-1073741824) 73892
    printLn $ div (-1073741825) 73892

max_stars_repo_name: grin-compiler/idris-grin

max_issues_repo_name: grin-compiler/idris-grin

max_forks_repo_name: grin-compiler/idris-grin


text:
module algebraic

-- Algebraic laws

data Bit = O | I

or : Bit -> Bit -> Bit
or 0 x1 = x1
or I x1 = I

orAssociative  : (a : Bit) ->
                 (b : Bit) ->
                 (c : Bit) ->
                 (a `or` b) `or` c = a `or` (b `or` c)
-- or = ?orAssociative_rhs_1
orAssociative O b c = refl
-- or = ?orAssociative_rhs_2
orAssociative I b c = refl

BitString : Type
-- list of bits
BitString = List Bit

bsor : BitString -> BitString -> BitString
bsor [] x1 = x1
bsor xs [] = xs
bsor (x :: xs) (y :: ys) = (x `or` y) :: (xs `bsor` ys)

max_stars_repo_name: ExpandingShapes/idris-experiments

max_issues_repo_name: ExpandingShapes/idris-experiments

max_forks_repo_name: ExpandingShapes/idris-experiments


text:
> module Fin.Operations

> import Data.Fin
> import Data.Vect

> %default total

> %access public export

> ||| 'Tail' of a finite function
> tail : {A : Type} -> {n : Nat} ->
>        (Fin (S n) -> A) -> (Fin n -> A)
> -- tail f k = f (FS k)
> tail f = f . FS

> ||| Maps a finite function to a vector
> toVect : {A : Type} -> {n : Nat} ->
>          (Fin n -> A) -> Vect n A
> toVect {n =   Z} _ = Nil
> toVect {n = S m} f = (f FZ) :: (toVect (tail f))
> -- toVect f = map f range

> ||| Sum of the values of a finite function
> sum : {n : Nat} -> (Fin n -> Nat) -> Nat
> sum {n = Z}   f = Z
> sum {n = S m} f = f FZ + sum (tail f)

> ||| Fold function for Fin
> foldFin : {X : Nat -> Type} -> (f1 : (n : Nat) -> X (S n)) ->
>                                (f2 : (n : Nat) -> X n -> X (S n)) ->
>                                Fin n -> X n
> foldFin {n = Z} f1 f2 x impossible
> foldFin {n = S m} f1 f2 FZ = f1 m
> foldFin {n = S m} f1 f2 (FS i) = f2 m (foldFin f1 f2 i)

Obs: Previous functions are not folds, since they do not take a |Fin|
as argument.

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
module Main

import System.File
import Network.Curl.Easy
import Network.Curl.Easy.Enum
import Network.Curl.Easy.FFI

import System.FFI

data TestCase = TestC String (IO Bool)

doTest : String -> IO Bool -> TestCase
doTest = TestC

runTestCase : TestCase -> IO ()
runTestCase (TestC name test) = do
  if !test
    then putStrLn $ name ++ " :: Ok"
    else putStrLn $ name ++ " :: FAILED"

testInitCleaup : TestCase
testInitCleaup = doTest "initCleanup" $
  do
    curl <- curl_easy_init
    curl_easy_cleanup curl
    pure True

testRequestGoogle : TestCase
testRequestGoogle = doTest "requestGoogle" $
  do
    putStrLn "init"
    curl <- curl_easy_init
    putStrLn $ "Set url with opt code:" ++ show (toCode CurlOptUrl)
    CurlEOk <- curl_easy_setopt curl CurlOptUrl "https://www.google.com"
        | err => (putStrLn $ "Failed with error: " ++ show err) *> pure False

    putStrLn "Perform"
    CurlEOk <- curl_easy_perform curl
        | err => (putStrLn $ "Failed with error: " ++ show err) *> pure False

    putStrLn "Cleanup"
    curl_easy_cleanup curl

    pure True

testRequestToFile : TestCase
testRequestToFile = doTest "testRequestToFile" $
  do
    putStrLn "init"
    curl <- curl_easy_init
    putStrLn $ "Set url with opt code:" ++ show (toCode CurlOptUrl)
    CurlEOk <- curl_easy_setopt curl CurlOptUrl "https://www.google.com"
        | err => (putStrLn $ "Failed with error: " ++ show err) *> pure False

    putStrLn "New File"
    Right (FHandle file) <- openFile "/tmp/idris2-curl.tmp" WriteTruncate
        | Left err => (putStrLn $ "File creation failed: " ++ show err) *> pure False

    putStrLn "Set write func"
    CurlEOk <- curl_easy_setopt curl CurlOptWritedata (ObjectPtrFile file)
        | err => (putStrLn $ "CurlOptWritefunction with error: " ++ show err) *> pure False

    putStrLn "Perform"
    CurlEOk <- curl_easy_perform curl
        | err => (putStrLn $ "Failed with error: " ++ show err) *> pure False

    putStrLn "Cleanup"
    curl_easy_cleanup curl

    pure True

main : IO ()
main = do
  runTestCase testInitCleaup
  runTestCase testRequestGoogle
  runTestCase testRequestToFile


text:
module Test.Signature

import Test.Assertions
import Idrlisp.Sexp
import Idrlisp.Pattern
import Idrlisp.Signature

%default covering

matchSignature : (sig : Signature ()) -> Sexp () -> Maybe (SignatureType sig)
matchSignature = match

matchArgsSignature : (sig : ArgsSignature ()) -> List (Sexp ()) -> Maybe (SignatureType sig)
matchArgsSignature = match

signatureTest : IO ()
signatureTest = describe "Signature" $ do
  let any  : Signature () = Any "any"
  let num  : Signature () = Num "num"
  let sym  : Signature () = Sym "sym"
  let str  : Signature () = Str "str"
  let bool : Signature () = Bool "bool"
  let nil  : Signature () = Nil
  let vec2 : Signature () = [Num "x", Num "y"]
  let strs : Signature () = List (Str "strs")
  let pat  : Signature () = Pat "args"
  let numOrStr : Signature () = Or num str

  describe "show" $ do
    any `shouldShow` "any"
    num `shouldShow` "num"
    sym `shouldShow` "sym"
    str `shouldShow` "str"
    bool `shouldShow` "bool"
    nil `shouldShow` "()"
    vec2 `shouldShow` "(x y)"
    strs `shouldShow` "(strs ...)"
    pat `shouldShow` "args"
    numOrStr `shouldShow` "(or num str)"
  describe "match" $ do
    matchSignature any (Num 123)
      `shouldBe` Just (Sexp.Num 123)
    matchSignature any (Sym "foo")
      `shouldBe` Just (Sexp.Sym "foo")
    matchSignature num (Num 123)
      `shouldBe` Just 123
    matchSignature num (Str "foo")
      `shouldBe` Nothing
    matchSignature sym (Sym "foo")
      `shouldBe` Just "foo"
    matchSignature sym (Str "foo")
      `shouldBe` Nothing
    matchSignature str (Str "bar")
      `shouldBe` Just "bar"
    matchSignature str (Sym "bar")
      `shouldBe` Nothing
    matchSignature bool (Bool True)
      `shouldBe` Just True
    matchSignature bool (Sym "bar")
      `shouldBe` Nothing
    matchSignature nil []
      `shouldBe` Just ()
    matchSignature nil (Sym "bar")
      `shouldBe` Nothing
    matchSignature vec2 []
      `shouldBe` Nothing
    matchSignature vec2 [Num 123, Num 456]
      `shouldBe` Just (123, 456)
    matchSignature vec2 [Num 123]
      `shouldBe` Nothing
    matchSignature vec2 [Num 123, Num 456, Num 789]
      `shouldBe` Nothing
    matchSignature strs [Str "foo", Str "bar", Str "baz"]
      `shouldBe` Just ["foo", "bar", "baz"]
    matchSignature strs [Str "foo", Str "bar", Num 0]
      `shouldBe` Nothing
    matchSignature strs (Str "foo" :: Str "bar" :: Str "baz")
      `shouldBe` Nothing
    matchSignature pat (Sym "foo" :: Sym "bar" :: Sym "baz")
      `shouldBe` Just (MkPattern ["foo", "bar"] (Just "baz"))
    matchSignature pat [Sym "foo", Sym "bar", Sym "baz"]
      `shouldBe` Just (MkPattern ["foo", "bar", "baz"] Nothing)
    matchSignature pat (Sym "xs")
      `shouldBe` Just (MkPattern [] (Just "xs"))
    matchSignature pat (Num 1)
      `shouldBe` Nothing
    matchSignature numOrStr (Num 1)
      `shouldBe` Just (Left 1)
    matchSignature numOrStr (Str "foo")
      `shouldBe` Just (Right "foo")
    matchSignature numOrStr (Sym "foo")
      `shouldBe` Nothing

argsSignatureTest : IO ()
argsSignatureTest = describe "ArgsSignature" $ do
  let zero      : ArgsSignature () = []
  let one       : ArgsSignature () = [Any "x"]
  let two       : ArgsSignature () = [Any "x", Any "y"]
  let twoOrMore : ArgsSignature () = (Any "x" :: Any "y" :: Rest (Any "z"))

  describe "show" $ do
    zero `shouldShow` "()"
    one `shouldShow` "(x)"
    two `shouldShow` "(x y)"
    twoOrMore `shouldShow` "(x y z ...)"
  describe "match" $ do
    matchArgsSignature zero []
      `shouldBe` Just ()
    matchArgsSignature zero [Num 1]
      `shouldBe` Nothing
    matchArgsSignature one [Num 1]
      `shouldBe` Just (Num 1)
    matchArgsSignature one []
      `shouldBe` Nothing
    matchArgsSignature one [Num 1, Num 2]
      `shouldBe` Nothing
    matchArgsSignature two [Num 1, Num 2]
      `shouldBe` Just (Num 1, Num 2)
    matchArgsSignature two [Num 1, Num 2, Num 3]
      `shouldBe` Nothing
    matchArgsSignature twoOrMore [Num 1, Num 2]
      `shouldBe` Just (Num 1, Num 2, [])
    matchArgsSignature twoOrMore [Num 1]
      `shouldBe` Nothing
    matchArgsSignature twoOrMore [Num 1, Num 2, Num 3, Num 4]
      `shouldBe` Just (Num 1, Num 2, [Num 3, Num 4])

export
test : IO ()
test = describe "Idrlisp.Signature" $ do
  signatureTest
  argsSignatureTest

max_stars_repo_name: yubrot/idrlisp

max_issues_repo_name: yubrot/idrlisp

max_forks_repo_name: yubrot/idrlisp


text:
module Dart.Core.Map

import Dart.FFI.Elab
import Dart.Core

%language ElabReflection

%runElab importDart [
  package "dart:core" [
    generic ["k", "v"] $
      class' "MapEntry" [
        final "k" "key",
        final "v" "value"
      ]
  ]
]

namespace Map

  namespace FromIterable

    public export
    data Tag : Type where

    %inline
    public export
    key : {a : Type} -> {k : Type} -> Parameter Tag
    key = mkParameter "key" (a -> k)

    %inline
    public export
    value : {a : Type} -> {v : Type} -> Parameter Tag
    value = mkParameter "value" (a -> v)

    %inline
    public export
    NamedParameters : {a : Type} -> {k : Type} -> {v : Type} -> Type
    NamedParameters = Parameters [FromIterable.key {a = a} {k = k}, FromIterable.value {a = a} {v = v}]

  %inline
  export
  fromIterable : HasIO io
    => {k : Type}
    -> {v : Type}
    -> {iterable : Type}
    -> {a : Type}
    -> iterable
    -> IsAssignableFrom (Iterable a) iterable
    => (a -> k)
    -> (a -> v)
    -> io (Map k v)
  fromIterable iter fk fv = primIO $
    prim__dart_new
      (Map k v)
      "fromIterable"
      [iter]
      (the (FromIterable.NamedParameters {a = a} {k = k} {v = v}) [key @= fk, value @= fv])

  %inline
  public export
  fromPairs : {k : Type} -> {v : Type} -> Prelude.List (k, v) -> IO (Dart.Core.Map k v)
  fromPairs entries = Map.fromIterable (Dart.Core.List.fromList entries) fst snd

  %inline
  export
  new : HasIO io => {k : Type} -> {v : Type} -> io (Map k v)
  new = primIO $ prim__dart_new (Map k v) "" [] none

  %inline
  export
  put : HasIO io => {k : Type} -> k -> {v : Type} -> v -> Map k v -> io ()
  put k v m = primIO $ prim__dart_invoke "[]" [] [m, k, v] none


text:
module Primitives.Primitives

import Core.Context
import CairoCode.CairoCode
import Data.SortedSet
import Data.SortedMap
import Primitives.Common
import Primitives.Felt
import Primitives.UInt
import Primitives.Int
import Primitives.BigInt
import CairoCode.Traversal.Base
import Utils.Helpers
import CodeGen.CodeGenHelper
import Debug.Trace
import CommonDef

[no_op] PrimFn where
  eval [_] = Just $ ArgValue 0
  eval _ = Nothing

  generateCode r [a] _ = Raw "\{ compileRegDecl r } = \{ compileReg a } # no_op\n"
  generateCode _ _ _ = assert_total $ idris_crash "Bad arguments to generateCode no_op"

[believeme] PrimFn where
  eval [_,_,_] = Just $ ArgValue 2 -- Do nothing, trust that it works :)
  eval _ = Nothing

  generateCode r [_,_,a] _ = Raw "\{ compileRegDecl r } = \{ compileReg a } # believeme\n"
  generateCode _ _ _ = assert_total $ idris_crash "Bad arguments to generateCode believeme"

-- Todo: extract error message if static
[crash] PrimFn where
  eval [_,_] = Just $ Failure "Crash"
  eval _ = Nothing

  generateCode r [_,_] _ = Instructions [ERROR r "Crash"]
  generateCode _ _ _ = assert_total $ idris_crash "Bad arguments to generateCode crash"

associate : (rec:PrimFn) => (f:(PrimFn -> a)) -> a
associate fun = fun rec

-- Dispatch
dispatch : CairoPrimFn -> ((PrimFn => a) -> a)
dispatch (Add t) = case t of
  IntType => associate @{add_int}
  Int8Type => associate @{add_int8}
  Int16Type => associate @{add_int16}
  Int32Type => associate @{add_int32}
  Int64Type => associate @{add_int64}
  FeltType => associate @{add_felt}
  IntegerType => associate @{add_integer}
  Bits8Type => associate @{add_uint8}
  Bits16Type => associate @{add_uint16}
  Bits32Type => associate @{add_uint32}
  Bits64Type => associate @{add_uint64}
  _ => assert_total $ idris_crash $ "Type not supported for add: " ++ show t

dispatch (Sub t) = case t of
  IntType => associate @{sub_int}
  Int8Type => associate @{sub_int8}
  Int16Type => associate @{sub_int16}
  Int32Type => associate @{sub_int32}
  Int64Type => associate @{sub_int64}
  FeltType => associate @{sub_felt}
  IntegerType => associate @{sub_integer}
  Bits8Type => associate @{sub_uint8}
  Bits16Type => associate @{sub_uint16}
  Bits32Type => associate @{sub_uint32}
  Bits64Type => associate @{sub_uint64}
  _ => assert_total $ idris_crash $ "Type not supported for sub: " ++ show t

dispatch (Mul t) = case t of
  IntType => associate @{mul_int}
  Int8Type => associate @{mul_int8}
  Int16Type => associate @{mul_int16}
  Int32Type => associate @{mul_int32}
  Int64Type => associate @{mul_int64}
  FeltType => associate @{mul_felt}
  IntegerType => associate @{mul_integer}
  Bits8Type => associate @{mul_uint8}
  Bits16Type => associate @{mul_uint16}
  Bits32Type => associate @{mul_uint32}
  Bits64Type => associate @{mul_uint64}
  _ => assert_total $ idris_crash $ "Type not supported for mul: " ++ show t

dispatch (Div t) = case t of
  IntType => associate @{div_int}
  Int8Type => associate @{div_int8}
  Int16Type => associate @{div_int16}
  Int32Type => associate @{div_int32}
  Int64Type => associate @{div_int64}
  FeltType => associate @{div_felt}
  IntegerType => associate @{div_integer}
  Bits8Type => associate @{div_uint8}
  Bits16Type => associate @{div_uint16}
  Bits32Type => associate @{div_uint32}
  Bits64Type => associate @{div_uint64}
  _ => assert_total $ idris_crash $ "Type not supported for mul: " ++ show t

dispatch (Mod t) = case t of
  IntType => associate @{mod_int}
  Int8Type => associate @{mod_int8}
  Int16Type => associate @{mod_int16}
  Int32Type => associate @{mod_int32}
  Int64Type => associate @{mod_int64}
  -- FeltType => associate @{mod_felt} -- NOT supported
  IntegerType => associate @{mod_integer}
  Bits8Type => associate @{mod_uint8}
  Bits16Type => associate @{mod_uint16}
  Bits32Type => associate @{mod_uint32}
  Bits64Type => associate @{mod_uint64}
  _ => assert_total $ idris_crash $ "Type not supported for mod: " ++ show t

dispatch (Neg t) = case t of
  IntType => associate @{neg_int}
  Int8Type => associate @{neg_int8}
  Int16Type => associate @{neg_int16}
  Int32Type => associate @{neg_int32}
  Int64Type => associate @{neg_int64}
  FeltType => associate @{neg_felt}
  IntegerType => associate @{neg_integer}
  Bits8Type => associate @{neg_uint8}
  Bits16Type => associate @{neg_uint16}
  Bits32Type => associate @{neg_uint32}
  Bits64Type => associate @{neg_uint64}
  _ => assert_total $ idris_crash $ "Type not supported for neg: " ++ show t

dispatch (ShiftL t) = case t of
  IntType => associate @{shl_int}
  Int8Type => associate @{shl_int8}
  Int16Type => associate @{shl_int16}
  Int32Type => associate @{shl_int32}
  Int64Type => associate @{shl_int64}
  -- FeltType => associate @{shl_felt}
  -- IntegerType => associate @{shl_integer}
  Bits8Type => associate @{shl_uint8}
  Bits16Type => associate @{shl_uint16}
  Bits32Type => associate @{shl_uint32}
  Bits64Type => associate @{shl_uint64}
  _ => assert_total $ idris_crash $ "Type not supported for shiftl: " ++ show t

dispatch (ShiftR t) = case t of
  IntType => associate @{shr_int}
  Int8Type => associate @{shr_int8}
  Int16Type => associate @{shr_int16}
  Int32Type => associate @{shr_int32}
  Int64Type => associate @{shr_int64}
  -- FeltType => associate @{shr_felt}
  -- IntegerType => associate @{shr_integer}
  Bits8Type => associate @{shr_uint8}
  Bits16Type => associate @{shr_uint16}
  Bits32Type => associate @{shr_uint32}
  Bits64Type => associate @{shr_uint64}
  _ => assert_total $ idris_crash $ "Type not supported for shiftr: " ++ show t

dispatch (BAnd t) = case t of
  IntType => associate @{and_int}
  Int8Type => associate @{and_int8}
  Int16Type => associate @{and_int16}
  Int32Type => associate @{and_int32}
  Int64Type => associate @{and_int64}
  -- FeltType => associate @{and_felt}
  -- IntegerType => associate @{and_integer}
  Bits8Type => associate @{and_uint8}
  Bits16Type => associate @{and_uint16}
  Bits32Type => associate @{and_uint32}
  Bits64Type => associate @{and_uint64}
  _ => assert_total $ idris_crash $ "Type not supported for band: " ++ show t

dispatch (BOr t) = case t of
  IntType => associate @{or_int}
  Int8Type => associate @{or_int8}
  Int16Type => associate @{or_int16}
  Int32Type => associate @{or_int32}
  Int64Type => associate @{or_int64}
  -- FeltType => associate @{or_felt}
  -- IntegerType => associate @{or_integer}
  Bits8Type => associate @{or_uint8}
  Bits16Type => associate @{or_uint16}
  Bits32Type => associate @{or_uint32}
  Bits64Type => associate @{or_uint64}
  _ => assert_total $ idris_crash $ "Type not supported for bor: " ++ show t

dispatch (BXOr t) = case t of
  IntType => associate @{xor_int}
  Int8Type => associate @{xor_int8}
  Int16Type => associate @{xor_int16}
  Int32Type => associate @{xor_int32}
  Int64Type => associate @{xor_int64}
  -- FeltType => associate @{xor_felt}
  -- IntegerType => associate @{xor_integer}
  Bits8Type => associate @{xor_uint8}
  Bits16Type => associate @{xor_uint16}
  Bits32Type => associate @{xor_uint32}
  Bits64Type => associate @{xor_uint64}
  _ => assert_total $ idris_crash $ "Type not supported for bxor: " ++ show t

dispatch (LT t) = case t of
  IntType => associate @{lt_int}
  Int8Type => associate @{lt_int8}
  Int16Type => associate @{lt_int16}
  Int32Type => associate @{lt_int32}
  Int64Type => associate @{lt_int64}
  -- FeltType => associate @{lt_felt}
  -- IntegerType => associate @{lt_integer}
  Bits8Type => associate @{lt_uint8}
  Bits16Type => associate @{lt_uint16}
  Bits32Type => associate @{lt_uint32}
  Bits64Type => associate @{lt_uint64}
  _ => assert_total $ idris_crash $ "Type not supported for lt: " ++ show t

dispatch (LTE t) = case t of
  IntType => associate @{lte_int}
  Int8Type => associate @{lte_int8}
  Int16Type => associate @{lte_int16}
  Int32Type => associate @{lte_int32}
  Int64Type => associate @{lte_int64}
  -- FeltType => associate @{lte_felt}
  -- IntegerType => associate @{lte_integer}
  Bits8Type => associate @{lte_uint8}
  Bits16Type => associate @{lte_uint16}
  Bits32Type => associate @{lte_uint32}
  Bits64Type => associate @{lte_uint64}
  _ => assert_total $ idris_crash $ "Type not supported for lte: " ++ show t

dispatch (EQ t) = case t of
  IntType => associate @{eq_int}
  Int8Type => associate @{eq_int8}
  Int16Type => associate @{eq_int16}
  Int32Type => associate @{eq_int32}
  Int64Type => associate @{eq_int64}
  FeltType => associate @{eq_felt}
  -- IntegerType => associate @{eq_integer}
  Bits8Type => associate @{eq_uint8}
  Bits16Type => associate @{eq_uint16}
  Bits32Type => associate @{eq_uint32}
  Bits64Type => associate @{eq_uint64}
  _ => assert_total $ idris_crash $ "Type not supported for eq: " ++ show t

dispatch (GTE t) = case t of
  IntType => associate @{gte_int}
  Int8Type => associate @{gte_int8}
  Int16Type => associate @{gte_int16}
  Int32Type => associate @{gte_int32}
  Int64Type => associate @{gte_int64}
  -- FeltType => associate @{gte_felt}
  -- IntegerType => associate @{gte_integer}
  Bits8Type => associate @{gte_uint8}
  Bits16Type => associate @{gte_uint16}
  Bits32Type => associate @{gte_uint32}
  Bits64Type => associate @{gte_uint64}
  _ => assert_total $ idris_crash $ "Type not supported for gte: " ++ show t

dispatch (GT t) = case t of
  IntType => associate @{gt_int}
  Int8Type => associate @{gt_int8}
  Int16Type => associate @{gt_int16}
  Int32Type => associate @{gt_int32}
  Int64Type => associate @{gt_int64}
  -- FeltType => associate @{gt_felt}
  -- IntegerType => associate @{gt_integer}
  Bits8Type => associate @{gt_uint8}
  Bits16Type => associate @{gt_uint16}
  Bits32Type => associate @{gt_uint32}
  Bits64Type => associate @{gt_uint64}
  _ => assert_total $ idris_crash $ "Type not supported for gt: " ++ show t

dispatch (Cast IntegerType IntType) = associate @{cast_integer_to_int}
dispatch (Cast _ IntType) = associate @{cast_to_int}

-- Casts to Int8
dispatch (Cast t Int8Type) = case t of
  IntegerType => associate @{cast_integer_to_int8}
  Int8Type => associate @{no_op}
  _ => associate @{cast_to_int8}

-- Casts to Int16
dispatch (Cast t Int16Type) = case t of
  IntegerType => associate @{cast_integer_to_int16}
  Bits8Type => associate @{no_op}
  Int8Type => associate @{no_op}
  Int16Type =>  associate @{no_op}
  _ => associate @{cast_to_int16}

-- Casts to Int32
dispatch (Cast t Int32Type) = case t of
  IntegerType => associate @{cast_integer_to_int32}
  Bits8Type => associate @{no_op}
  Int8Type => associate @{no_op}
  Bits16Type => associate @{no_op}
  Int16Type => associate @{no_op}
  Int32Type => associate @{no_op}
  _ => associate @{cast_to_int32}

-- Casts to Int64
dispatch (Cast t Int64Type) = case t of
  IntegerType => associate @{cast_integer_to_int64}
  Bits8Type => associate @{no_op}
  Int8Type => associate @{no_op}
  Bits16Type => associate @{no_op}
  Int16Type => associate @{no_op}
  Bits32Type => associate @{no_op}
  Int32Type => associate @{no_op}
  Int64Type => associate @{no_op}
  _ => associate @{cast_to_int64}

dispatch (Cast IntegerType FeltType) = associate @{cast_integer_to_felt}
dispatch (Cast _ FeltType) = associate @{cast_to_felt}

dispatch (Cast IntegerType IntegerType) = associate @{no_op}
dispatch (Cast _ IntegerType) = associate @{cast_to_integer}

-- Casts to Bits8
dispatch (Cast t Bits8Type) = case t of
  IntegerType => associate @{cast_integer_to_uint8}
  Bits8Type => associate @{no_op}
  _ => associate @{cast_to_uint8}

-- Casts to Bits16
dispatch (Cast t Bits16Type) = case t of
  IntegerType => associate @{cast_integer_to_uint16}
  Bits8Type => associate @{no_op}
  Bits16Type => associate @{no_op}
  _ => associate @{cast_to_uint16}

-- Casts to Bits32
dispatch (Cast t Bits32Type) = case t of
  IntegerType => associate @{cast_integer_to_uint32}
  Bits8Type => associate @{no_op}
  Bits16Type => associate @{no_op}
  Bits32Type => associate @{no_op}
  _  => associate @{cast_to_uint32}

-- Casts to Bits64
dispatch (Cast t Bits64Type) = case t of
  IntegerType => associate @{cast_integer_to_uint64}
  Bits8Type => associate @{no_op}
  Bits16Type => associate @{no_op}
  Bits32Type => associate @{no_op}
  Bits64Type => associate @{no_op}
  _  => associate @{cast_to_uint64}

dispatch (BelieveMe) = associate @{believeme}
dispatch (Crash) = associate @{crash}

dispatch op = assert_total $ idris_crash $ "Operation not supported: " ++ show op

export
evaluateConstantOp : CairoPrimFn -> List ValueInfo -> Maybe EvalRes
evaluateConstantOp fn args = dispatch fn eval args

export
primFnApStable : CairoPrimFn -> Bool
primFnApStable fn = dispatch fn apStable

export
primFnLinearImplicits : CairoPrimFn -> SortedSet LinearImplicit
primFnLinearImplicits fn = dispatch fn implicits

export
primFnImports : CairoPrimFn -> SortedSet Import
primFnImports fn = dispatch fn imports

export
primFnDependencies : CairoPrimFn -> SortedMap Name (Lazy CairoDef)
primFnDependencies fn = dispatch fn dependencies

export
primFnDependencyNames : CairoPrimFn -> SortedSet Name
primFnDependencyNames = keySet . primFnDependencies

export
generatePrimFnCode : CairoPrimFn -> (res:CairoReg) -> (args:List CairoReg) -> LinearImplicitArgs -> PrimFnCode
generatePrimFnCode fn = dispatch fn generateCode

export
findPrimFnDeps: List (Name, CairoDef) -> List (Name, CairoDef)
findPrimFnDeps defs = map (\(n,d) => (n,d)) $ SortedMap.toList allDeps
  where
    primFnCollector : InstVisit CairoReg -> SortedMap Name (Lazy CairoDef)
    primFnCollector (VisitOp _ _ primFn _) = primFnDependencies primFn
    primFnCollector _ = empty

    allDeps : SortedMap Name (Lazy CairoDef)
    allDeps = snd $ runVisitConcatCairoDefs @{dropDuplicateKeysMonoid} (pureTraversal primFnCollector) defs

max_stars_repo_name: skyro-compiler/skyro

max_issues_repo_name: skyro-compiler/skyro

max_forks_repo_name: skyro-compiler/skyro


text:
-- The Great Theorem Prover Showdown (https://github.com/hwayne/lets-prove-leftpad/)
--
-- Code here is nearly completely copied from @porglezomp's Idris implementation, just for the
-- purpose of self edification.

module LeftPad

import Data.Vect

-- As I am totally new to theorem proving, I hereby write down some confusions about this proof:
--
-- * This implementation seems to sidestep the proof of the post-condition that the suffix does be
--   the original string. Is it still sound?
-- * The use of dependent pair seems redundant?
-- * Is `rewrite` deprecated by the new Elaborator Reflection system?

-- `minus` is saturating subtraction
-- `maximum` has branch `maximum Z m` but not `maximum m Z`
-- The 3rd case:
--     - Goal := maximum (S k) (S n) = (S n - S k) + S k
--     - maximum (S k) (S n) = S (maximum k n)
--     - Goal => S (maximum k n) = (S n - S k) + S k
--     - Induction hypothesis := maximum k n = (n - k) + k
--     - Goal => S ((n - k) + k) = (S n - S k) + S k
--
--     - plusSuccRightSucc l r := S (l + r) = l + S r
--     - plusSuccRightSucc (n - k) k => S ((n - k) + k) = (n - k) + S k
--     - Goal => (n - k) + S k = (S n - S k) + S k
--     - minus (S left) (S right) = minus left right
--     - Goal => trivial

eq_max : (n, k : Nat) -> maximum k n = plus (n `minus` k) k
eq_max n     Z     = rewrite minusZeroRight n in
                     rewrite plusZeroRightNeutral n in
                     Refl
eq_max Z     (S _) = Refl
eq_max (S n) (S k) = rewrite sym $ plusSuccRightSucc (n `minus` k) k in
                     rewrite eq_max n k in
                     Refl

leftPad : (padChar : Char) -> (n : Nat) -> (xs : Vect k Char) -> Vect (maximum k n) Char
leftPad {k} padChar n xs = rewrite eq_max n k
  in
    replicate (n `minus` k) padChar ++ xs

max_stars_repo_name: gyk/TrivialSolutions

max_issues_repo_name: gyk/TrivialSolutions

max_forks_repo_name: gyk/TrivialSolutions


text:
import Aoc
import Data.List
import Data.Nat
import Data.Strings
import Data.Vect
%default total

||| Shift an element onto the end of a vector, deleting the first.
shiftVec : a -> Vect (S n) a -> Vect (S n) a
shiftVec x (_::t) = rewrite plusCommutative 1 n in t ++ [x]

||| Find an "invalid" number in the list, using a window, which is initially the preamble.
findInvalid : {n : Nat} -> Vect (S n) Int -> List Int -> Maybe Int
findInvalid window [] = Nothing
findInvalid window (x::xs) =
  if any ((==x) . sum) $ combinations 2 $ toList window
    then findInvalid (shiftVec x window) xs
    else Just x

||| slice 3 5 xs == [xs!!3, xs!!4, xs!!5]
slice : Nat -> Nat -> List a -> List a
slice lo hi = take (minus (S hi) lo) . drop lo

||| Given n and xs, return all (i,j) so that (i<j) and sum (slice i j xs) == n.
rangesSummingTo : (Eq a, Num a, Neg a) => a -> List a -> List (Nat, Nat)
rangesSummingTo n xs =
  let ys = scanl1 (+) xs
      cs = combinations 2 (zip [0..length ys] ys)
  in [(i+1, j) | [(i,y1),(j,y2)] <- cs, y2 - y1 == n, i+1 < j]

main : IO ()
main = do
  xs <- readIntegerLines {a=Int}
  putStr "*   "
  Just (preamble, rest) <- pure (takeVect 25 xs) | Nothing => putStrLn "input too short!"
  Just n <- pure (findInvalid preamble rest)     | Nothing => putStrLn "found no answer to *"
  printLn n
  putStr "**  "
  [(lo, hi)] <- pure (rangesSummingTo n xs) | [] => putStrLn "no solution for **"
                                            | _  => putStrLn "multiple solutions for **"
  s@(_::_) <- pure (slice lo hi xs)         | [] => putStrLn "solution for ** is empty"
  printLn (foldl1 min s + foldl1 max s)


text:
{-
Copyright 2018, Mokshasoft AB (mokshasoft.com)

This software may be distributed and modified according to the terms of
the BSD 2-Clause license. Note that NO WARRANTY is provided.
See "LICENSE_BSD2.txt" for details.
-}

{-
  FFI for gpio_v2.h:
    https://github.com/mokshasoft/starterwarefree/blob/master/include/gpio_v2.h
-}

module StarterWareFree.Drivers

%access public export
%default total
%include C "gpio_v2.h"

GPIO_DIR_OUTPUT : Int
GPIO_DIR_OUTPUT = 0x0

GPIO_PIN_HIGH : Int
GPIO_PIN_HIGH = 0x1

GPIO_PIN_LOW : Int
GPIO_PIN_LOW = 0x0

GPIOModuleReset : Int -> IO ()
GPIOModuleReset baseAdd =
    foreign FFI_C "GPIOModuleReset" (Int -> IO ()) baseAdd

GPIOModuleEnable : Int -> IO ()
GPIOModuleEnable baseAdd =
    foreign FFI_C "GPIOModuleEnable" (Int -> IO ()) baseAdd

GPIOModuleDisable : Int -> IO ()
GPIOModuleDisable baseAdd =
    foreign FFI_C "GPIOModuleDisable" (Int -> IO ()) baseAdd

GPIODirModeSet : Int -> Int -> Int -> IO ()
GPIODirModeSet baseAdd pinNumber pinDirection =
    foreign FFI_C "GPIODirModeSet" (Int -> Int -> Int -> IO ()) baseAdd pinNumber pinDirection

GPIODirModeGet : Int -> Int -> IO Int
GPIODirModeGet baseAdd pinNumber =
    foreign FFI_C "GPIODirModeGet" (Int -> Int -> IO Int) baseAdd pinNumber

GPIOPinWrite : Int -> Int -> Int -> IO ()
GPIOPinWrite baseAdd pinNumber pinValue =
    foreign FFI_C "GPIOPinWrite" (Int -> Int -> Int -> IO ()) baseAdd pinNumber pinValue

GPIOPinRead : Int -> Int -> IO Int
GPIOPinRead baseAdd pinNumber =
    foreign FFI_C "GPIOPinRead" (Int -> Int -> IO Int) baseAdd pinNumber

GPIOMultiplePinsWrite : Int -> Int -> Int -> IO ()
GPIOMultiplePinsWrite baseAdd setMask clrMask =
    foreign FFI_C "GPIOMultiplePinsWrite" (Int -> Int -> Int -> IO ()) baseAdd setMask clrMask

GPIOMultiplePinsRead : Int -> Int -> IO Int
GPIOMultiplePinsRead baseAdd readMask =
    foreign FFI_C "GPIOMultiplePinsRead" (Int -> Int -> IO Int) baseAdd readMask

GPIOPinIntEnable : Int -> Int -> Int -> IO ()
GPIOPinIntEnable baseAdd intLine pinNumber =
    foreign FFI_C "GPIOPinIntEnable" (Int -> Int -> Int -> IO ()) baseAdd intLine pinNumber

GPIOPinIntDisable : Int -> Int -> Int -> IO ()
GPIOPinIntDisable baseAdd intLine pinNumber =
    foreign FFI_C "GPIOPinIntDisable" (Int -> Int -> Int -> IO ()) baseAdd intLine pinNumber

GPIOIntTypeSet : Int -> Int -> Int -> IO ()
GPIOIntTypeSet baseAdd pinNumber eventType =
    foreign FFI_C "GPIOIntTypeSet" (Int -> Int -> Int -> IO ()) baseAdd pinNumber eventType

GPIOIntTypeGet : Int -> Int -> IO Int
GPIOIntTypeGet baseAdd pinNumber =
    foreign FFI_C "GPIOIntTypeGet" (Int -> Int -> IO Int) baseAdd pinNumber

GPIOPinIntStatus : Int -> Int -> Int -> IO Int
GPIOPinIntStatus baseAdd intLine pinNumber =
    foreign FFI_C "GPIOPinIntStatus" (Int -> Int -> Int -> IO Int) baseAdd intLine pinNumber

GPIOPinIntClear : Int -> Int -> Int -> IO ()
GPIOPinIntClear baseAdd intLine pinNumber =
    foreign FFI_C "GPIOPinIntClear" (Int -> Int -> Int -> IO ()) baseAdd intLine pinNumber

GPIORawIntStatus : Int -> Int -> Int -> IO Int
GPIORawIntStatus baseAdd intLine readMask =
    foreign FFI_C "GPIORawIntStatus" (Int -> Int -> Int -> IO Int) baseAdd intLine readMask

GPIOTriggerPinInt : Int -> Int -> Int -> IO ()
GPIOTriggerPinInt baseAdd intLine pinNumber =
    foreign FFI_C "GPIOTriggerPinInt" (Int -> Int -> Int -> IO ()) baseAdd intLine pinNumber

GPIOWakeupGlobalEnable : Int -> IO ()
GPIOWakeupGlobalEnable baseAdd =
    foreign FFI_C "GPIOWakeupGlobalEnable" (Int -> IO ()) baseAdd

GPIOWakeupGlobalDisable : Int -> IO ()
GPIOWakeupGlobalDisable baseAdd =
    foreign FFI_C "GPIOWakeupGlobalDisable" (Int -> IO ()) baseAdd

GPIOPinIntWakeUpEnable : Int -> Int -> Int -> IO ()
GPIOPinIntWakeUpEnable baseAdd intLine pinNumber =
    foreign FFI_C "GPIOPinIntWakeUpEnable" (Int -> Int -> Int -> IO ()) baseAdd intLine pinNumber

GPIOPinIntWakeUpDisable : Int -> Int -> Int -> IO ()
GPIOPinIntWakeUpDisable baseAdd intLine pinNumber =
    foreign FFI_C "GPIOPinIntWakeUpDisable" (Int -> Int -> Int -> IO ()) baseAdd intLine pinNumber

GPIOAutoIdleModeControl : Int -> Int -> IO ()
GPIOAutoIdleModeControl baseAdd modeFlag =
    foreign FFI_C "GPIOAutoIdleModeControl" (Int -> Int -> IO ()) baseAdd modeFlag

GPIOIdleModeConfigure : Int -> Int -> IO ()
GPIOIdleModeConfigure baseAdd modeFlag =
    foreign FFI_C "GPIOIdleModeConfigure" (Int -> Int -> IO ()) baseAdd modeFlag

GPIOGatingRatioConfigure : Int -> Int -> IO ()
GPIOGatingRatioConfigure baseAdd configFlag =
    foreign FFI_C "GPIOGatingRatioConfigure" (Int -> Int -> IO ()) baseAdd configFlag

GPIODebounceFuncControl : Int -> Int -> Int -> IO ()
GPIODebounceFuncControl baseAdd pinNumber controlFlag =
    foreign FFI_C "GPIODebounceFuncControl" (Int -> Int -> Int -> IO ()) baseAdd pinNumber controlFlag

GPIODebounceTimeConfig : Int -> Int -> IO ()
GPIODebounceTimeConfig baseAdd debounceTime =
    foreign FFI_C "GPIODebounceTimeConfig" (Int -> Int -> IO ()) baseAdd debounceTime

GPIORevisionInfoGet : Int -> IO Int
GPIORevisionInfoGet baseAdd =
    foreign FFI_C "GPIORevisionInfoGet" (Int -> IO Int) baseAdd

max_stars_repo_name: mokshasoft/starterwarefree-idris-ffi

max_issues_repo_name: mokshasoft/starterwarefree-idris-ffi

max_forks_repo_name: mokshasoft/starterwarefree-idris-ffi


text:
module Ex8

import Decidable.Equality
import Data.Nat
import Data.Vect

%default total

same_cons : { xs : List a } -> { ys : List a } -> xs = ys -> x :: xs = x :: ys
same_cons Refl = Refl

same_lists : { xs : List a } -> { ys : List a } -> x = y -> xs = ys -> x :: xs = y :: ys
same_lists Refl Refl = Refl

data ThreeEq : a -> b -> c -> Type where
  AllSame : ThreeEq x x x

allSameS : (x, y, z : Nat) -> ThreeEq x y z -> ThreeEq (S x) (S y) (S z)
allSameS _ _ _ AllSame = AllSame

myPlusCommutes : (n : Nat) -> (m : Nat) -> n + m =  m + n
myPlusCommutes Z m = rewrite plusZeroRightNeutral m in Refl
myPlusCommutes (S k) m = rewrite myPlusCommutes k m in
                                 rewrite plusSuccRightSucc m k in Refl

reverseProof_nil : Vect n a -> Vect (plus n 0) a
reverseProof_nil {n} xs = rewrite plusZeroRightNeutral n in xs

reverseProof_xs : Vect (S n + k) a -> Vect (plus n (S k)) a
reverseProof_xs {n} {k} xs = rewrite sym (plusSuccRightSucc n k) in xs

myReverse : Vect n a -> Vect n a
myReverse xs = reverse' [] xs where
  reverse' : forall n, m. Vect n a -> Vect m a -> Vect (n + m) a
  reverse' acc [] = reverseProof_nil acc
  reverse' acc (x :: xs) = reverseProof_xs (reverse' (x :: acc) xs)

headUnequal : DecEq a => { xs : Vect n a } ->  { ys : Vect n a } ->
                         (contra : (x = y) -> Void) -> ((x :: xs) = (y :: ys)) -> Void
headUnequal contra Refl = contra Refl

tailUnequal : DecEq a => { xs : Vect n a } -> { ys : Vect n a } ->
                         (contra : (xs = ys) -> Void) -> ((x :: xs) = (y :: ys)) -> Void
tailUnequal contra Refl = contra Refl

max_stars_repo_name: timmyjose-study/tdd-with-idris

max_issues_repo_name: timmyjose-study/tdd-with-idris

max_forks_repo_name: timmyjose-study/tdd-with-idris


text:
-- ---------------------------------------------------------------- [ Time.idr ]
-- Module  : Data.Time
--
-- License : This code is distributed under the MIT license. See the
--           file LICENSE in the root directory for its full text.
-- --------------------------------------------------------------------- [ EOH ]
module Data.Time

-- import public Data.Time.Calendar
-- import public Data.Time.Clock
-- import public Data.Time.LocalTime
-- import public Data.Time.Format

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

max_stars_repo_name: yurrriq/idris-time

max_issues_repo_name: yurrriq/idris-time

max_forks_repo_name: yurrriq/idris-time


text:
module Repl

import Control.ST
import Control.ST.Exception
import DataTypes
import Util
import Lists
import Numbers
import Strings
import Vector
import Data.Complex
import Parse
import ParserCombinator
import Data.Complex
import Primitives
import Data.SortedMap
import Environment
import Data.IORef
import Eval

%access public export

--------------
-- Run
-- Repl
--------------

readOrThrow : (Show a, Context m) => Parser a -> String -> ST m a []
readOrThrow parser input =
  case parse parser input of
    ParseError (MkError err) _ pos => throw $ LispParseError err pos
    ParseSuccess val s pos => pure val

readExprList : Context m => String -> ST m (List LispVal) []
readExprList = readOrThrow $ (many' go) <* eof
    where
    go = do
        skipMany space
        e <- parseExpr
        skipMany space
        pure e

evalExprList : Context m => EnvRef LispVal -> String -> ST m (List LispVal) []
evalExprList envRef expr =
    do parsed <- readExprList expr
       evaled <- traverse' (eval envRef) parsed
       pure $ evaled
    where
        traverse' : Context m => (LispVal -> ST m LispVal []) -> List LispVal -> ST m (List LispVal) []
        traverse' f [] = pure []
        traverse' f (x::xs) = do v <- f x
                                 vs <- traverse' f xs
                                 pure (v :: vs)


text:
module Test.Server.Template.TemplateTest

import IdrTest.Test
import IdrTest.Expectation

import Server.Template.Template

%default total

export
suite : Test
suite =
  describe "Template Tests"
    [ test "Show Template" (\_ => assertEq
        (template "My Template <%% DESC %%>" [("DESC","Rocks")])
        "My Template Rocks"
      )
    ]

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
module Program

import CommonTestingStuff

delays : List FinDuration
delays = [250.millis, 600.millis, 0.seconds, 1.seconds, 4.seconds]

p : PrintString m => CanSleep m => Time -> FinDuration -> m Unit
p offset d = do
  sleepFor d
  printTime offset "after waiting for \{show d}"

export
beforeString : String
beforeString = "before coop, delays: \{show delays}"

export
program : PrintString m => CanSleep m => ConcurrentApplicative m => m Unit
program = do
  offset <- currentTime
  printTime offset "===== usual applicative"
  for_ delays $ p offset
  printTime offset "==== end"

  offset <- currentTime
  printTime offset "==== parallel applicative"
  for_ delays @{Concurrent} $ p offset
  printTime offset "==== end"