text:
module NetTest

import Network.Socket

main : IO ()
main = do
  putStrLn "net"
  printLn $ toCode AF_UNIX
  Right sock <- socket AF_INET Stream 0
    | Left err => printLn err

  let addr = IPv4Addr 127 0 0 1

  0 <- bind sock (Just addr) 4077
    | err => putStrLn $ "bind error: " ++ show err

  0 <- listen sock
    | err => putStrLn $ "listen error: " ++ show err

  Right (conn, saddr) <- accept sock
    | Left err => putStrLn $ "accept error: " ++ show err

  pure ()

ext: idr

max_stars_repo_name: boxfire/rapid

max_issues_repo_name: boxfire/rapid

max_forks_repo_name: boxfire/rapid


text:
module DatesProblem

import Data.Vect

%default total

{-
  Helpers
-}

||| Generic Type for Non-inclusive Range of Integers
data Range : Integer -> Integer -> Type where
  MkRange : (min : Integer) -> (max : Integer) -> Range min max

||| Proof that an integer is in range
inRange : Range min max -> Integer -> Type
inRange (MkRange min max) x = Dec (x > min = x < max)

{-
  Date Specific
-}

data Year : Type where
  MkYear : (year : Integer) -> Year

%name Year y,y1,y2,y3

isLeap : Year -> Bool
isLeap (MkYear year) = (modNatNZ (toNat year) 4 SIsNotZ) == 0

data Month : Type where
  January   : Month
  February  : Month
  March     : Month
  April     : Month
  May       : Month
  June      : Month
  July      : Month
  August    : Month
  September : Month
  October   : Month
  November  : Month
  December  : Month

%name Month m,m1,m2,m3

monthOrder : Month -> Nat
monthOrder January   = 1
monthOrder February  = 2
monthOrder March     = 3
monthOrder April     = 4
monthOrder May       = 5
monthOrder June      = 6
monthOrder July      = 7
monthOrder August    = 8
monthOrder September = 9
monthOrder October   = 10
monthOrder November  = 11
monthOrder December  = 12

monthDays : Year -> Month -> Integer
monthDays _    January   = 30
monthDays year February  = if isLeap year then 29 else 28
monthDays _    March     = 30
monthDays _    April     = 31
monthDays _    May       = 30
monthDays _    June      = 31
monthDays _    July      = 30
monthDays _    August    = 31
monthDays _    September = 30
monthDays _    October   = 31
monthDays _    November  = 30
monthDays _    December  = 31

previousMonth : Month -> Month
previousMonth January   = December
previousMonth February  = January
previousMonth March     = February
previousMonth April     = March
previousMonth May       = April
previousMonth June      = May
previousMonth July      = June
previousMonth August    = July
previousMonth September = August
previousMonth October   = September
previousMonth November  = October
previousMonth December  = November

data Day : Type where
  MkDay : (day : Nat) -> Day

%name Day d,d1,d2,d3

inDayRange : Nat -> Day -> Type
inDayRange n (MkDay day) =
  let
    n' = toIntegerNat n
    range = (MkRange 1 (n'+1))
    day' = (toIntegerNat day)
  in
    inRange range day'

validDate : Year -> Month -> Day -> Type
validDate year month = inDayRange (toNat $ monthDays year month)

data Date : Type where
  MkDate : (day : Day) ->
           (month : Month) ->
           (year : Year) ->
           { auto p : (validDate year month day) } -> Date

%name Date d,d1,d2,d3

Eq Year where
  (==) (MkYear y) (MkYear y') = y == y'

Eq Month where
  (==) x y  = monthOrder x == monthOrder y

Eq Day where
  (==) (MkDay y) (MkDay y') = y == y'

Eq Date where
  (==) (MkDate d m y) (MkDate d' m' y') = d == d' && m == m' && y == y'

Ord Year where
  compare (MkYear y) (MkYear y') = compare y y'

Ord Month where
  compare x y = compare (monthOrder x) (monthOrder y)

Ord Day where
  compare (MkDay d) (MkDay d') = compare d d'

Ord Date where
  compare (MkDate d m y) (MkDate d' m' y') =
    case compare y y' of
         EQ => case compare m m' of
                    EQ => compare y y'
                    result => result
         result => result

beginIsBeforeEnd : Date -> Date -> Type
beginIsBeforeEnd begin end = case compare begin end of
                                  LT => Dec (begin = begin)
                                  _ => Not (begin = end)

daysToMonth : Year -> Month -> Integer
daysToMonth year month = count (previousMonth month) (monthOrder $ previousMonth month)
  where
    count : Month -> Nat -> Integer
    count m Z = 0
    count m (S k) = (monthDays year m) + count (previousMonth m) k

daysInDate : Date -> Integer
daysInDate (MkDate (MkDay days) month year@(MkYear y)) =
  let
    yearDays = (y - 1) * 365
    monthDays = daysToMonth year month
  in
    yearDays + monthDays + (toIntegerNat days)

distanceBetweenDates : (begin : Date) ->
                       (end : Date) ->
                       { auto prf : (beginIsBeforeEnd begin end) } -> Integer
distanceBetweenDates a b = daysInDate b - daysInDate a

data DateRange : Type where
  MkDateRange : (begin : Date) ->
                (end : Date) ->
                { auto prf : (beginIsBeforeEnd begin end) } ->
                DateRange

%name DateRange dr,dr1,dr2,dr3

distanceInRange : DateRange -> Integer
distanceInRange (MkDateRange begin end) = distanceBetweenDates begin end

{-
  Sample Dates
-}

date_one : Date
date_one = MkDate (MkDay 28) September (MkYear 1991)

date_two : Date
date_two = MkDate (MkDay 29) February (MkYear 2008)

date_three : Date
date_three = MkDate (MkDay 30) September (MkYear 1992)

{-
  Ranges Logic
-}

max_stars_repo_name: ostera/asdf

max_issues_repo_name: ostera/asdf

max_forks_repo_name: ostera/asdf


text:
import Data.Either
import Data.List
import Data.Maybe
import Data.String
import Data.Binary
import Data.Binary.Digit

import System.File

Eq Digit where
  I == I = True
  O == O = True
  I == O = False
  O == I = False

lookupMaybe : Nat -> List a -> Maybe a
lookupMaybe _ [] = Nothing
lookupMaybe Z (x :: _) = Just x
lookupMaybe (S n) (_ :: l) = lookupMaybe n l

significant : (Nat, Nat) -> Bin -> (Nat, Nat)
significant (n, c) b = case lookupMaybe n b of
                            Just d => case d of
                                           I => (n, c + 1)
                                           O => (n, c)
                            Nothing => (n, c)

toBin : String -> Bin
toBin s = (\c => if c == '1' then I else O) <$> unpack s

oxygen2 : Nat -> List Bin -> Bin
oxygen2 n [] = []
oxygen2 n (b :: []) = b
oxygen2 n l@(_ :: _ :: _) = let len = length l
                                (_, c) = foldl significant (n, 0) l
                                d = if c + c >= len then I else O in
                                oxygen2 (n + 1) $ filter (\b => case lookupMaybe n b of
                                                                     Just d2 => d == d2
                                                                     Nothing => False) $ l

oxygen : List Bin -> Bin
oxygen l = oxygen2 0 l

scrubber2 : Nat -> List Bin -> Bin
scrubber2 n [] = []
scrubber2 n (b :: []) = b
scrubber2 n l@(_ :: _ :: _) = let len = length l
                                  (_, c) = foldl significant (n, 0) l
                                  d = if c + c >= len then O else I in
                                  scrubber2 (n + 1) $ filter (\b => case lookupMaybe n b of
                                                                         Just d2 => d == d2
                                                                         Nothing => False) $ l

scrubber : List Bin -> Bin
scrubber l = scrubber2 0 l

run : String -> IO ()
run s = do let lines = toBin <$> (lines $ trim $ s)
           let o = toNat $ reverse $ oxygen $ lines
           let s = toNat $ reverse $ scrubber $ lines
           putStrLn $ show $ s * o

main : IO ()
main = do Right s <- readFile "input.txt"
            | Left err => putStrLn $ show err
          run s


text:
module Main

import Control.IOExcept
import Data.IORef
import Dbcritic.Check
import Dbcritic.Check.IndexFkRef
import Dbcritic.Check.PrimaryKey
import Dbcritic.Check.PrimaryKeyBigint
import Dbcritic.Check.TimeZone
import Dbcritic.Check.Timestamptz
import Dbcritic.Config
import Dbcritic.Libpq
import System

checks : List Check
checks = [ checkIndexFkRef, checkPrimaryKey, checkPrimaryKeyBigint, checkTimeZone, checkTimestamptz ]

main' : IOExcept String Int
main' = do

    config <- readConfig ".dbcriticrc"
    conn   <- pgConnect ""
    index  <- ioe_lift $ newIORef 0

    for_ checks $ \check => do
        allIssues <- inspect check conn
        let allSilences = getSilences config check
        let issues = filter (not . isSilenced allSilences) allIssues
        let unsilence = filter (not . silencesIssue allIssues) allSilences

        for_ issues $ \issue => do
            index' <- ioe_lift $ modifyIORef index (+ 1) *> readIORef index
            ioe_lift $ putStrLn (formatIssue index' check issue)

        for_ unsilence $ \silence => do
            index' <- ioe_lift $ modifyIORef index (+ 1) *> readIORef index
            ioe_lift $ putStrLn (formatSilence index' silence)

    count <- ioe_lift $ readIORef index
    pure $ if count > 0 then 1 else 0

main : IO ()
main = do
    result <- runIOExcept main'
    case result of
        Right n  => exit n
        Left err => do fPutStrLn stderr err
                       exit 2

max_stars_repo_name: channable/dbcritic

max_issues_repo_name: channable/dbcritic

max_forks_repo_name: channable/dbcritic


text:
Data Vect : Nat -> Type -> Type
  Nil : Vect 0 a
  (::) : a -> Vect n a -> Vect (n + 1) a

max_stars_repo_name: RossMeikleham/MSci-Project

max_issues_repo_name: RossMeikleham/MSci-Project

max_forks_repo_name: RossMeikleham/MSci-Project


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

||| Example DSML through reSkinning the GRL.
module GRL.Test.DSML.PML

import public GRL.Common
import public GRL.IR
import public GRL.Model
import public GRL.Builder
import public GRL.Pretty

%access public export

-- ---------------------------------------------------------------- [ DSML Def ]
data ETy = PaperTy | SecTy | AuthTy | RevTy | BibTy | AbsTy

data PTy = ElemTy ETy | SLinkTy | ALinkTy

data ValidAction : ETy -> ETy -> Type where
  AS : ValidAction AuthTy SecTy
  RS : ValidAction RevTy  SecTy
  AB : ValidAction AuthTy BibTy
  RB : ValidAction RevTy  BibTy
  AA : ValidAction AuthTy AbsTy
  RA : ValidAction RevTy  AbsTy

data ValidPElem : ETy -> Type where
  SP : ValidPElem SecTy
  BP : ValidPElem BibTy
  AP : ValidPElem AbsTy

data PML : PTy -> GTy -> Type where
  MkPaper : String -> PML (ElemTy PaperTy) ELEM
  MkSect  : String -> PML (ElemTy SecTy)   ELEM
  MkBib   : PML (ElemTy BibTy) ELEM
  MkAbs   : PML (ElemTy AbsTy) ELEM
  MkAuth  : String -> SValue -> PML (ElemTy AuthTy)  ELEM
  MkRev   : String -> SValue -> PML (ElemTy RevTy)   ELEM

  AddElem : PML (ElemTy PaperTy) ELEM
         -> PML (ElemTy x) ELEM
         -> {auto prf : ValidPElem x}
         -> PML SLinkTy STRUCT

  AddAction : PML (ElemTy x) ELEM
           -> PML (ElemTy y) ELEM
           -> {auto prf : ValidAction x y}
           -> PML ALinkTy INTENT

GRL (\x => PML ty x) where
  mkElem (MkPaper t) = Elem GOALty t Nothing
  mkElem (MkSect  t) = Elem GOALty t Nothing
  mkElem (MkBib)     = Elem GOALty "Bibliography" Nothing
  mkElem (MkAbs)     = Elem GOALty "Abstract" Nothing

  mkElem (MkAuth t s) = Elem TASKty ("Authoring " ++ t) (Just s)
  mkElem (MkRev  t s) = Elem TASKty ("Reviewing " ++ t) (Just s)

  mkIntent (AddAction x y) = ILink IMPACTSty MAKES (mkElem x) (mkElem y)

  mkStruct (AddElem x y) = SLink ANDty (mkElem x) [(mkElem y)]

-- ---------------------------------------------------------------- [ MkPretty ]

syntax [a] "==>" [b] = AddAction a b
syntax [a] "&=" [b]  = AddElem a b

PAPER : Type
PAPER = PML (ElemTy PaperTy) ELEM

SECT : Type
SECT = PML (ElemTy SecTy) ELEM

BIB : Type
BIB = PML (ElemTy BibTy) ELEM

ABSTRACT : Type
ABSTRACT = PML (ElemTy AbsTy) ELEM

WRITING : Type
WRITING = PML (ElemTy AuthTy) ELEM

REVIEW : Type
REVIEW = PML (ElemTy RevTy) ELEM

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

max_stars_repo_name: jfdm/idris-grl

max_issues_repo_name: jfdm/idris-grl

max_forks_repo_name: jfdm/idris-grl


text:
module Control.Effect.Misc

-- TODO
-- Some definitions from this file may be later
-- relocated to more suitable places.

namespace Functor
  public export
  [Id] Functor (\x => x) where
    map f x = f x

  %hint public export
  FunctorId : Functor (\x => x)
  FunctorId = Functor.Id

  public export
  [LeftPair] Functor (, s) where
    map f (x, y) = (f x, y)

  %hint public export
  FunctorLeftPair : Functor (, s)
  FunctorLeftPair = Functor.LeftPair

namespace Applicative
  public export
  [Id] Applicative (\x => x) where
    pure x = x
    f <*> x = f x

  %hint public export
  ApplicativeId : Applicative (\x => x)
  ApplicativeId = Applicative.Id

namespace Monad
  public export
  [Id] Monad (\x => x) where
    x >>= f = f x

  %hint public export
  MonadId : Monad (\x => x)
  MonadId = Monad.Id


text:
module Crypto.AES.Big

import Utils.ConstantTable
import Crypto.AES.Common
import Data.Bits
import Utils.Bytes
import Data.List
import Data.Fin
import Data.Fin.Extra
import Data.Vect
import Utils.Misc

ssm0 : ConstantTable 256 Bits32
ssm0 = from_vect
  [ 0xC66363A5, 0xF87C7C84, 0xEE777799, 0xF67B7B8D, 0xFFF2F20D, 0xD66B6BBD
  , 0xDE6F6FB1, 0x91C5C554, 0x60303050, 0x02010103, 0xCE6767A9, 0x562B2B7D
  , 0xE7FEFE19, 0xB5D7D762, 0x4DABABE6, 0xEC76769A, 0x8FCACA45, 0x1F82829D
  , 0x89C9C940, 0xFA7D7D87, 0xEFFAFA15, 0xB25959EB, 0x8E4747C9, 0xFBF0F00B
  , 0x41ADADEC, 0xB3D4D467, 0x5FA2A2FD, 0x45AFAFEA, 0x239C9CBF, 0x53A4A4F7
  , 0xE4727296, 0x9BC0C05B, 0x75B7B7C2, 0xE1FDFD1C, 0x3D9393AE, 0x4C26266A
  , 0x6C36365A, 0x7E3F3F41, 0xF5F7F702, 0x83CCCC4F, 0x6834345C, 0x51A5A5F4
  , 0xD1E5E534, 0xF9F1F108, 0xE2717193, 0xABD8D873, 0x62313153, 0x2A15153F
  , 0x0804040C, 0x95C7C752, 0x46232365, 0x9DC3C35E, 0x30181828, 0x379696A1
  , 0x0A05050F, 0x2F9A9AB5, 0x0E070709, 0x24121236, 0x1B80809B, 0xDFE2E23D
  , 0xCDEBEB26, 0x4E272769, 0x7FB2B2CD, 0xEA75759F, 0x1209091B, 0x1D83839E
  , 0x582C2C74, 0x341A1A2E, 0x361B1B2D, 0xDC6E6EB2, 0xB45A5AEE, 0x5BA0A0FB
  , 0xA45252F6, 0x763B3B4D, 0xB7D6D661, 0x7DB3B3CE, 0x5229297B, 0xDDE3E33E
  , 0x5E2F2F71, 0x13848497, 0xA65353F5, 0xB9D1D168, 0x00000000, 0xC1EDED2C
  , 0x40202060, 0xE3FCFC1F, 0x79B1B1C8, 0xB65B5BED, 0xD46A6ABE, 0x8DCBCB46
  , 0x67BEBED9, 0x7239394B, 0x944A4ADE, 0x984C4CD4, 0xB05858E8, 0x85CFCF4A
  , 0xBBD0D06B, 0xC5EFEF2A, 0x4FAAAAE5, 0xEDFBFB16, 0x864343C5, 0x9A4D4DD7
  , 0x66333355, 0x11858594, 0x8A4545CF, 0xE9F9F910, 0x04020206, 0xFE7F7F81
  , 0xA05050F0, 0x783C3C44, 0x259F9FBA, 0x4BA8A8E3, 0xA25151F3, 0x5DA3A3FE
  , 0x804040C0, 0x058F8F8A, 0x3F9292AD, 0x219D9DBC, 0x70383848, 0xF1F5F504
  , 0x63BCBCDF, 0x77B6B6C1, 0xAFDADA75, 0x42212163, 0x20101030, 0xE5FFFF1A
  , 0xFDF3F30E, 0xBFD2D26D, 0x81CDCD4C, 0x180C0C14, 0x26131335, 0xC3ECEC2F
  , 0xBE5F5FE1, 0x359797A2, 0x884444CC, 0x2E171739, 0x93C4C457, 0x55A7A7F2
  , 0xFC7E7E82, 0x7A3D3D47, 0xC86464AC, 0xBA5D5DE7, 0x3219192B, 0xE6737395
  , 0xC06060A0, 0x19818198, 0x9E4F4FD1, 0xA3DCDC7F, 0x44222266, 0x542A2A7E
  , 0x3B9090AB, 0x0B888883, 0x8C4646CA, 0xC7EEEE29, 0x6BB8B8D3, 0x2814143C
  , 0xA7DEDE79, 0xBC5E5EE2, 0x160B0B1D, 0xADDBDB76, 0xDBE0E03B, 0x64323256
  , 0x743A3A4E, 0x140A0A1E, 0x924949DB, 0x0C06060A, 0x4824246C, 0xB85C5CE4
  , 0x9FC2C25D, 0xBDD3D36E, 0x43ACACEF, 0xC46262A6, 0x399191A8, 0x319595A4
  , 0xD3E4E437, 0xF279798B, 0xD5E7E732, 0x8BC8C843, 0x6E373759, 0xDA6D6DB7
  , 0x018D8D8C, 0xB1D5D564, 0x9C4E4ED2, 0x49A9A9E0, 0xD86C6CB4, 0xAC5656FA
  , 0xF3F4F407, 0xCFEAEA25, 0xCA6565AF, 0xF47A7A8E, 0x47AEAEE9, 0x10080818
  , 0x6FBABAD5, 0xF0787888, 0x4A25256F, 0x5C2E2E72, 0x381C1C24, 0x57A6A6F1
  , 0x73B4B4C7, 0x97C6C651, 0xCBE8E823, 0xA1DDDD7C, 0xE874749C, 0x3E1F1F21
  , 0x964B4BDD, 0x61BDBDDC, 0x0D8B8B86, 0x0F8A8A85, 0xE0707090, 0x7C3E3E42
  , 0x71B5B5C4, 0xCC6666AA, 0x904848D8, 0x06030305, 0xF7F6F601, 0x1C0E0E12
  , 0xC26161A3, 0x6A35355F, 0xAE5757F9, 0x69B9B9D0, 0x17868691, 0x99C1C158
  , 0x3A1D1D27, 0x279E9EB9, 0xD9E1E138, 0xEBF8F813, 0x2B9898B3, 0x22111133
  , 0xD26969BB, 0xA9D9D970, 0x078E8E89, 0x339494A7, 0x2D9B9BB6, 0x3C1E1E22
  , 0x15878792, 0xC9E9E920, 0x87CECE49, 0xAA5555FF, 0x50282878, 0xA5DFDF7A
  , 0x038C8C8F, 0x59A1A1F8, 0x09898980, 0x1A0D0D17, 0x65BFBFDA, 0xD7E6E631
  , 0x844242C6, 0xD06868B8, 0x824141C3, 0x299999B0, 0x5A2D2D77, 0x1E0F0F11
  , 0x7BB0B0CB, 0xA85454FC, 0x6DBBBBD6, 0x2C16163A ]

lookup_ssm0 : Bits32 -> Bits32
lookup_ssm0 x = index_bits8 (cast x) ssm0

lookup_sbox : Bits32 -> Bits32 -> Bits32 -> Bits32 -> Bits32
lookup_sbox s0 s1 s2 s3 =
  let a = cast $ index_bits8 (cast $ shiftR s0 24) sbox
      b = cast $ index_bits8 (cast $ shiftR s1 16) sbox
      c = cast $ index_bits8 (cast $ shiftR s2 8) sbox
      d = cast $ index_bits8 (cast s3) sbox
  in (shiftL a 24) .|. (shiftL b 16) .|. (shiftL c 8) .|. d

sbox_ext : Fin 32 -> Bits32 -> Bits32
sbox_ext i = rotr i . lookup_ssm0

expand_key_stream : {n_k : _} -> {auto 0 ok : NonZero n_k} -> Vect n_k (Vect 4 Bits8) -> Stream Bits32
expand_key_stream key = map from_be $ prepend (toList key) $ expand_key key

encrypt_block' : Nat -> Stream Bits32 -> Vect 4 Bits32 -> Vect 16 Bits8

encrypt_block' Z skey [s0, s1, s2, s3] =
  concat $ map (to_be {n=4}) $ vecxor (Stream.take 4 skey)
  [ lookup_sbox s0 s1 s2 s3
  , lookup_sbox s1 s2 s3 s0
  , lookup_sbox s2 s3 s0 s1
  , lookup_sbox s3 s0 s1 s2 ]

encrypt_block' (S n) skey [s0, s1, s2, s3] =
  let (s, skey) = splitAt 4 skey
  in encrypt_block' n skey $ vecxor s
     [ (sbox_ext 0 $ shiftR s0 24) `xor` (sbox_ext 8 $ shiftR s1 16) `xor` (sbox_ext 16 $ shiftR s2 8) `xor` (sbox_ext 24 s3)
     , (sbox_ext 0 $ shiftR s1 24) `xor` (sbox_ext 8 $ shiftR s2 16) `xor` (sbox_ext 16 $ shiftR s3 8) `xor` (sbox_ext 24 s0)
     , (sbox_ext 0 $ shiftR s2 24) `xor` (sbox_ext 8 $ shiftR s3 16) `xor` (sbox_ext 16 $ shiftR s0 8) `xor` (sbox_ext 24 s1)
     , (sbox_ext 0 $ shiftR s3 24) `xor` (sbox_ext 8 $ shiftR s0 16) `xor` (sbox_ext 16 $ shiftR s1 8) `xor` (sbox_ext 24 s2)
     ]

export
encrypt_block : (mode : Mode) -> (key : Vect ((get_n_k mode) * 4) Bits8) -> Vect 16 Bits8 -> Vect 16 Bits8
encrypt_block mode key plaintext =
  let buf = map (from_be {n=4,a=Bits32}) $ group 4 4 plaintext
      (s, skey) = splitAt 4 (expand_key_stream {ok = n_k_never_Z mode} $ group _ _ key)
  in encrypt_block' (get_main_rounds mode) skey $ vecxor buf s


text:
module Core.Directory

import Core.Context
import Core.Core
import Core.FC
import Core.Name
import Core.Options
import Utils.Path

import Data.List
import Data.Strings
import Data.Maybe

import System.Directory
import System.File
import System.Info

%default total

-- Return the name of the first file available in the list
export
firstAvailable : List String -> Core (Maybe String)
firstAvailable [] = pure Nothing
firstAvailable (f :: fs)
    = do Right ok <- coreLift $ openFile f Read
               | Left err => firstAvailable fs
         coreLift $ closeFile ok
         pure (Just f)

dirExists : String -> IO Bool
dirExists dir = do Right d <- openDir dir
                       | Left _ => pure False
                   closeDir d
                   pure True

getPkgDirs : {auto c : Ref Ctxt Defs} -> Core (List String)
getPkgDirs
    = do d <- getDirs
         session <- getSession
         dirs <- traverse (getPkgDir (package_dirs d)) (packages session)
         pure $ mapMaybe id dirs
  where
    getPkgDir : List String -> String -> Core (Maybe String)
    getPkgDir [] _ = pure Nothing
    getPkgDir (dir :: dirs) pkg
        = do let d = dir </> pkg
             True <- coreLift $ dirExists d
               | False => getPkgDir dirs pkg
             pure (Just d)

export
covering
readDataFile : {auto c : Ref Ctxt Defs} ->
               String -> Core String
readDataFile fname
    = do d <- getDirs
         let fs = map (\p => p </> fname) (data_dirs d)
         Just f <- firstAvailable fs
            | Nothing => throw (InternalError ("Can't find data file " ++ fname ++
                                               " in any of " ++ show fs))
         Right d <- coreLift $ readFile f
            | Left err => throw (FileErr f err)
         pure d

-- Look for a library file required by a code generator. Look in the
-- library directories, and in the lib/ subdirectoriy of all the 'extra import'
-- directories
export
findLibraryFile : {auto c : Ref Ctxt Defs} ->
                  String -> Core String
findLibraryFile fname
    = do d <- getDirs
         pkgDirs <- getPkgDirs
         let fs = map (</> fname) (lib_dirs d) ++
               map (</> "lib") pkgDirs
         Just f <- firstAvailable fs
            | Nothing => throw (InternalError ("Can't find library " ++ fname))
         pure f

-- Given a namespace, return the full path to the checked module,
-- looking first in the build directory then in the extra_dirs
export
nsToPath : {auto c : Ref Ctxt Defs} ->
           FC -> ModuleIdent -> Core (Either Error String)
nsToPath loc ns
    = do d <- getDirs
         pkgDirs <- getPkgDirs
         let fnameBase = joinPath (reverse $ unsafeUnfoldModuleIdent ns)
         let fs = map (\p => p </> fnameBase <.> "ttc")
                      ((build_dir d </> "ttc") :: pkgDirs ++ extra_dirs d)
         Just f <- firstAvailable fs
            | Nothing => pure (Left (ModuleNotFound loc ns))
         pure (Right f)

-- Given a namespace, return the full path to the source module (if it
-- exists in the working directory)
export
nsToSource : {auto c : Ref Ctxt Defs} ->
             FC -> ModuleIdent -> Core String
nsToSource loc ns
    = do d <- getDirs
         let fnameOrig = joinPath (reverse $ unsafeUnfoldModuleIdent ns)
         let fnameBase = maybe fnameOrig (\srcdir => srcdir </> fnameOrig) (source_dir d)
         let fs = map (\ext => fnameBase <.> ext)
                      [".idr", ".lidr", ".yaff", ".org", ".md"]
         Just f <- firstAvailable fs
            | Nothing => throw (ModuleNotFound loc ns)
         pure f

-- Given a filename in the working directory + source directory, return the correct
-- namespace for it
export
pathToNS : String -> Maybe String -> String -> Core ModuleIdent
pathToNS wdir sdir fname
    = let sdir = fromMaybe "" sdir
          base = if isAbsolute fname then wdir </> sdir else sdir
        in
          case stripPrefix base fname of
               Nothing => throw (UserError ("Source file " ++ show fname
                                            ++ " is not in the source directory "
                                            ++ show (wdir </> sdir)))
               Just p => pure $ unsafeFoldModuleIdent $ map show $ reverse $ (parse (p <.> "")).body

-- Create subdirectories, if they don't exist
export
covering
mkdirAll : String -> IO (Either FileError ())
mkdirAll dir = if parse dir == emptyPath
                  then pure (Right ())
                  else do exist <- dirExists dir
                          if exist
                             then pure (Right ())
                             else do Right () <- case parent dir of
                                          Just parent => mkdirAll parent
                                          Nothing => pure (Right ())
                                        | err => pure err
                                     createDir dir

-- Given a namespace (i.e. a module name), make the build directory for the
-- corresponding ttc file
export
covering
makeBuildDirectory : {auto c : Ref Ctxt Defs} ->
                     ModuleIdent -> Core ()
makeBuildDirectory ns
    = do d <- getDirs
         let bdir = build_dir d </> "ttc"
         let ns = reverse $ fromMaybe [] $ tail' $ unsafeUnfoldModuleIdent ns -- first item is file name
         let ndir = joinPath ns
         Right _ <- coreLift $ mkdirAll (bdir </> ndir)
            | Left err => throw (FileErr (build_dir d </> ndir) err)
         pure ()

export
covering
ensureDirectoryExists : String -> Core ()
ensureDirectoryExists dir
    = do Right _ <- coreLift $ mkdirAll dir
            | Left err => throw (FileErr dir err)
         pure ()

-- Given a source file, return the name of the ttc file to generate
export
getTTCFileName : {auto c : Ref Ctxt Defs} ->
                 String -> String -> Core String
getTTCFileName inp ext
    = do ns <- getNS
         d <- getDirs
         -- Get its namespace from the file relative to the working directory
         -- and generate the ttc file from that
         ns <- pathToNS (working_dir d) (source_dir d) inp
         let fname = joinPath (reverse $ unsafeUnfoldModuleIdent ns) <.> ext
         let bdir = build_dir d
         pure $ bdir </> "ttc" </> fname

-- Given a root executable name, return the name in the build directory
export
getExecFileName : {auto c : Ref Ctxt Defs} -> String -> Core String
getExecFileName efile
    = do d <- getDirs
         pure $ build_dir d </> efile

getEntries : Directory -> IO (List String)
getEntries d
    = do Right f <- dirEntry d
             | Left err => pure []
         ds <- assert_total $ getEntries d
         pure (f :: ds)

dirEntries : String -> IO (Either FileError (List String))
dirEntries dir
    = do Right d <- openDir dir
             | Left err => pure (Left err)
         ds <- getEntries d
         closeDir d
         pure (Right ds)

-- Find an ipkg file in any of the directories above this one
-- returns the directory, the ipkg file name, and the directories we've
-- gone up
export
covering
findIpkgFile : IO (Maybe (String, String, String))
findIpkgFile
    = do Just dir <- currentDir
              | Nothing => pure Nothing
         res <- findIpkgFile' dir ""
         pure res
  where
    covering
    findIpkgFile' : String -> String -> IO (Maybe (String, String, String))
    findIpkgFile' dir up
        = do Right files <- dirEntries dir
                 | Left err => pure Nothing
             let Just f = find (\f => extension f == Just "ipkg") files
                 | Nothing => case splitParent dir of
                                   Just (parent, end) => findIpkgFile' parent (end </> up)
                                   Nothing => pure Nothing
             pure $ Just (dir, f, up)


text:
module Data.JSON.ToString

import Data.JSON.Value
import Data.Scientific

-- TODO: check if this is working correctly!
private
isControlChar : Char -> Bool
isControlChar c =
  or [ cast c >= (0*1) && cast c <= (15*1 + 1*16)
     , cast c == (15*1 + 7*16)
     , cast c == (5*1 + 8*16)
     ]
-- TODO: this nice escaped version doesn't parse unfortunately
--  or [ c >= '\u0000' && c <= '\u001F'
--     , c == '\u007F'
--     , c == '\u0085'
--     ]

-- TODO: check if this is working correctly!
private
escapeUnicodeChar : Char -> List Char
escapeUnicodeChar c = ['\\', 'u'] ++ map fst [hex3, hex2, hex1, hex0] where
  f : Int -> (Char, Int)
  f x = (toChar (c), r) where
    c : Int
    c = x `mod` 16
    r : Int
    r = x `div` 16
    toChar : Int -> Char
    toChar x = cast $ if x < 10
                         then x + cast '0'
                         else x + cast 'A'
  hex0 : (Char,Int)
  hex0 = f $ cast c
  hex1 : (Char,Int)
  hex1 = f $ snd hex0
  hex2 : (Char,Int)
  hex2 = f $ snd hex1
  hex3 : (Char,Int)
  hex3 = f $ snd hex2

private
escapeControlChar : Char -> List Char
escapeControlChar c = if isControlChar c
                         then escapeUnicodeChar c
                         else [c]

private
escapeChars : List Char -> List Char
escapeChars [] = []
escapeChars (c :: cs) = c' ++ escapeChars cs where
  prependBackslash : Char -> List Char
  prependBackslash c = ['\\', c]
  c' : List Char
  c' = case c of
            '"' => prependBackslash '"'
            '\\' => prependBackslash '\\'
            '\b' => prependBackslash 'b'
            '\f' => prependBackslash 'f'
            '\n' => prependBackslash 'n'
            '\r' => prependBackslash 'r'
            _ => escapeControlChar c

public export
toString : JSONValue -> String
toString JSONNull = "null"
toString (JSONBool x) = case x of
                             True => "true"
                             False => "false"
toString (JSONNumber x) = prettyShowScientific x
toString (JSONString x) = pack $ escapeChars $ unpack $ x where
toString (JSONObject xs) = "{" ++ pairsToString xs ++ "}" where
  pairsToString : List (String, JSONValue) -> String
  pairsToString [] = ""
  pairsToString ((name, value) :: []) = toString (JSONString name) ++ ":" ++ toString value
  pairsToString (pair :: pairs) = pairsToString [pair] ++ "," ++ pairsToString pairs
toString (JSONArray xs) = "[" ++ valuesToString xs ++ "]" where
  valuesToString : List JSONValue -> String
  valuesToString [] = ""
  valuesToString (x :: []) = toString x
  valuesToString (x :: xs) = valuesToString [x] ++ "," ++ valuesToString xs


text:
-- see: http://docs.idris-lang.org/en/latest/tutorial/interp.html
-- module Interp

import Data.Vect
import Data.Fin

data Ty = TyInt | TyBool | TyFun Ty Ty

interpTy : Ty -> Type
interpTy TyInt       = Int
interpTy TyBool      = Bool
interpTy (TyFun A T) = interpTy A -> interpTy T

using (G:Vect n Ty)  -- the context
  -- `HasType i G T` is a proof that variable `i` in context `G` has type `T`
  data HasType : (i : Fin n) -> Vect n Ty -> Ty -> Type where
    -- proof that the most recently defined variable is well-typed:
    Stop : HasType FZ (t :: G) t                       -- de-Brujin index 0
    Pop  : HasType k G t -> HasType (FS k) (u :: G) t  -- Pop Stop is index 1, ...

  data Expr : Vect n Ty -> Ty -> Type where
    Var : HasType i G t
          -> Expr G t
    Val : (x : Int)
          -> Expr G TyInt
    Lam : Expr (a :: G) t
          -> Expr G (TyFun a t)
    App : Expr G (TyFun a t)
          -> Expr G a
          -> Expr G t
    Op  : (interpTy a -> interpTy b -> interpTy c) ->
          Expr G a -> Expr G b
          -> Expr G c
    If  : Expr G TyBool -> Lazy (Expr G a) -> Lazy (Expr G a)
          -> Expr G a

  data Env : Vect n Ty -> Type where
    Nil   : Env Nil
    (::)  : interpTy a -> Env G -> Env (a :: G)

  -- given a proof that a variable if defined in the context,
  --   we can produce a value from the environment:
  lookup : HasType i G t -> Env G -> interpTy t
  lookup Stop    (x :: xs) = x
  lookup (Pop k) (x :: xs) = lookup k xs

  interp : Env G -> Expr G t -> interpTy t
  interp env (Var i)      = lookup i env
  interp env (Val x)      = x
  interp env (Lam sc)     = \x => interp (x :: env) sc
  interp env (App f s)    = (interp env f) (interp env s)
  interp env (Op op x y)  = op (interp env x) (interp env y)
  interp env (If cnd thn els)
                          = if interp env cnd
                            then interp env thn
                            else interp env els

  succ : Expr G (TyFun TyInt TyInt)
  succ = Lam (Op (+) (Var Stop) (Val 1))

  add : Expr G (TyFun TyInt (TyFun TyInt TyInt)) -- \x.\y.y + x
  add = Lam (Lam (Op (+) (Var Stop) (Var (Pop Stop))))
  -- `interp [] (App (App add (Val 2)) (Val 2))` gives `4 : Int`

  iszero : Expr G (TyFun TyInt TyBool)
  iszero = Lam (Op (==) (Var Stop) (Val 0))

  -- `interp [] (App fact (Val 4))` gives `24 : Int`
  fact : Expr G (TyFun TyInt TyInt)
  fact = Lam (If (App iszero (Var Stop))
                 (Val 1)
                 (Op (*) (Var Stop)
                         (App fact (Op (-) (Var Stop) (Val 1)))))

main : IO ()
main = do
  putStr "Enter a number: "
  n <- getLine
  printLn (interp [] fact (cast n))

max_stars_repo_name: EarlGray/language-snippets

max_issues_repo_name: EarlGray/language-incubator

max_forks_repo_name: EarlGray/language-incubator


text:
module Text.Quantity

%default total

public export
record Quantity where
  constructor Qty
  min : Nat
  max : Maybe Nat

public export
Show Quantity where
  show (Qty Z Nothing) = "*"
  show (Qty Z (Just (S Z))) = "?"
  show (Qty (S Z) Nothing) = "+"
  show (Qty min max) = "{" ++ show min ++ showMax ++ "}"
    where
      showMax : String
      showMax = case max of
                     Nothing => ","
                     Just max' => if min == max'
                                     then ""
                                     else "," ++ show max'

public export
between : Nat -> Nat -> Quantity
between min max = Qty min (Just max)

public export
atLeast : Nat -> Quantity
atLeast min = Qty min Nothing

public export
atMost : Nat -> Quantity
atMost max = Qty 0 (Just max)

public export
exactly : Nat -> Quantity
exactly n = Qty n (Just n)

public export
inOrder : Quantity -> Bool
inOrder (Qty min Nothing) = True
inOrder (Qty min (Just max)) = min <= max


text:
module Data.Vector

%default total
%access public export

export data Vector : Type -> Type

%extern prim__Vector_empty : Ptr
%extern prim__Vector_replicate : Nat -> Ptr -> Ptr
%extern prim__Vector_length : Ptr -> Nat
%extern prim__Vector_null : Ptr -> Bool
%extern prim__Vector_index : Ptr -> Nat -> Ptr
%extern prim__Vector_replaceAt : Nat -> Ptr -> Ptr -> Ptr
%extern prim__Vector_insertAt : Nat -> Ptr -> Ptr -> Ptr

||| O(1) Empty vector
empty : Vector a
empty = believe_me prim__Vector_empty

||| O(n) Vector of the given length with the same value in each position.
replicate : Nat -> a -> Vector a
replicate n x = believe_me (prim__Vector_replicate n (believe_me x))

||| O(1) Vector with exactly one element
singleton : a -> Vector a
singleton = replicate 1

||| O(1) Yield the length of the vector.
length : Vector a -> Nat
length xs = prim__Vector_length (believe_me xs)

||| O(1) Test whether a vector if empty
null : Vector a -> Bool
null xs = prim__Vector_null (believe_me xs)

infixl 10 !!

||| O(1) Indexing
(!!) : Vector a -> Nat -> a
(!!) xs i = believe_me (prim__Vector_index (believe_me xs) (believe_me i))

||| O(1) Safe Indexing
index' : Nat -> Vector a -> Maybe a
index' i xs = if (i < length xs) then Just (xs !! i) else Nothing

||| O(length xs) Insert new element.
unsafeInsertAt : Nat -> a -> Vector a -> Vector a
unsafeInsertAt n x xs = believe_me (prim__Vector_insertAt n (believe_me x) (believe_me xs))

||| O(length xs) Insert new element.
unsafeReplaceAt : Nat -> a -> Vector a -> Vector a
unsafeReplaceAt n x xs = believe_me (prim__Vector_replaceAt n (believe_me x) (believe_me xs))

||| O(length xs) Prepends an element.
(::) : a -> Vector a -> Vector a
(::) = unsafeInsertAt 0

||| O(1)
lastIndex : Vector a -> Maybe Nat
lastIndex xs =
  let
    n = length xs
  in
    case 1 `isLTE` n of
      Yes prf => Just (n - 1)
      _       => Nothing

elem : Eq a => a -> Vector a -> Bool
elem x xs =
  case length xs of
    Z   => False
    S k => go k
  where
    go : Nat -> Bool
    go Z = x == xs !! 0
    go i@(S k) = if x == xs !! i then True else go k

Foldable Vector where
  foldr f init xs =
    case length xs of
      Z   => init
      S k => go k init
    where
      go : Nat -> acc -> acc
      go Z       acc = f (xs !! 0) acc
      go i@(S k) acc = go k (f (xs !! i) acc)

  foldl f init xs =
    case length xs of
      Z   => init
      S k => go Z k init
    where
      go : Nat -> Nat -> acc -> acc
      go i Z     acc = f acc (xs !! i)
      go i (S k) acc = go (S i) k (f acc (xs !! i))

Show a => Show (Vector a) where
  show xs = foldl (\acc, e => (if (length acc > 1) then (acc ++ ", ") else acc) ++ show e) "[" xs ++ "]"

max_stars_repo_name: alaendle/idris-cil

max_issues_repo_name: alaendle/idris-cil

max_forks_repo_name: alaendle/idris-cil


text:
module Main
import Average

showAverage : String -> String
showAverage str = "Average : " ++ (show (average str)) ++ "\n"

main : IO ()
main = repl "> " showAverage

max_stars_repo_name: neduard/type-driven-development

max_issues_repo_name: neduard/type-driven-development

max_forks_repo_name: neduard/type-driven-development


text:
module Data.Crypto.Encryption.Block.EncryptionMode

import Data.Bits

import Data.Crypto.Encryption
import Data.Crypto.Encryption.Block
import Data.Crypto.Encryption.Stream
import Data.Crypto.Util

%default total
%access public export

data ElectronicCookbook : Nat -> Type where
  ECB : ElectronicCookbook n

-- This is ECB (Electronic Cookbook) - no initialization vector
-- ECB should be considered insecure regardless of the cipher used
implementation EncryptionMode ElectronicCookbook where
  encryptBlocks key _ blocks = map (encryptBlock key) blocks
  decryptBlocks key _ blocks = map (decryptBlock key) blocks

data CipherBlockChainingMode : Nat -> Type where
  CBC : Bits n -> CipherBlockChainingMode n

implementation EncryptionMode CipherBlockChainingMode where
  encryptBlocks _ _ [] = []
  encryptBlocks key (CBC iv) (plain::rest) =
    let ciph = encryptBlock key (plain `xor` iv)
    in ciph :: encryptBlocks key (CBC ciph) rest
  decryptBlocks _ _ [] = []
  decryptBlocks key (CBC iv) (ciph::rest) =
    (decryptBlock key ciph `xor` iv) :: decryptBlocks key (CBC ciph) rest

data PropagatingCipherBlockChainingMode : Nat -> Type where
  PCBC : Bits n -> PropagatingCipherBlockChainingMode n

implementation EncryptionMode PropagatingCipherBlockChainingMode where
  encryptBlocks _ _ [] = []
  encryptBlocks key (PCBC iv) (plain::rest) =
    let ciph = encryptBlock key (plain `xor` iv)
    in ciph :: encryptBlocks key (PCBC (plain `xor` ciph)) rest
  decryptBlocks _ _ [] = []
  decryptBlocks key (PCBC iv) (ciph::rest) =
    let plain = decryptBlock key ciph `xor` iv
    in plain :: decryptBlocks key (PCBC (plain `xor` ciph)) rest

data CipherFeedbackMode : Nat -> Type where
  CFB : Bits n -> CipherFeedbackMode n

implementation EncryptionMode CipherFeedbackMode where
  encryptBlocks _ _ [] = []
  encryptBlocks key (CFB iv) (plain::rest) =
    let ciph = encryptBlock key iv `xor` plain
    in ciph :: encryptBlocks key (PCBC ciph) rest
  decryptBlocks _ _ [] = []
  decryptBlocks key (CFB iv) (ciph::rest) =
    (decryptBlock key iv `xor` ciph) :: decryptBlocks key (PCBC ciph) rest

data OutputFeedbackMode : Nat -> Type where
  OFB : Bits n -> OutputFeedbackMode n

implementation EncryptionMode OutputFeedbackMode where
  encryptBlocks _ _ [] = []
  encryptBlocks key (OFB iv) (plain::rest) =
    let newIV = encryptBlock key iv
    in (plain `xor` newIV) :: encryptBlocks key (OFB newIV) rest
  decryptBlocks _ _ [] = []
  decryptBlocks key (OFB iv) (ciph::rest) =
    let newIV = decryptBlock key iv
    in (ciph `xor` newIV) :: decryptBlocks key (OFB newIV) rest

||| `OutputFeedbackMode` allows any `BlockCipher` to be treated as a
||| `StreamCipher`.
implementation BlockCipher b bitsPerBlock _ => StreamCipher (b, OutputFeedbackMode bitsPerBlock) bitsPerBlock where
  generateKeystream (b, OFB iv) =
    let newIV = encryptBlock b iv
    in newIV :: (generateKeystream (b, OFB newIV))

||| Counter mode takes a nonce, an initial “counter” value, and a function to
||| get the next counter value.
data CounterMode : Nat -> Type where
  CTR : Bits m -> Bits n -> (Bits n -> Bits n) -> CounterMode (m + n)

||| The most common counter mode starts at 0 and moves sequentially through the
||| natural numbers.
incrementalCTR : Bits m -> CounterMode (m + n)
incrementalCTR m = CTR m (intToBits 0) (plus (intToBits 1))

implementation EncryptionMode CounterMode where
  encryptBlocks _ _ [] = []
  encryptBlocks key (CTR nonce counter f) (plain::rest) =
    (plain `xor` encryptBlock key (append nonce counter))
      :: encryptBlocks key (CTR nonce (f counter) f) rest
  decryptBlocks _ _ [] = []
  decryptBlocks key (CTR nonce counter f) (ciph::rest) =
    (ciph `xor` decryptBlock key (append nonce counter))
      :: decryptBlocks key (CTR nonce (f counter) f) rest

||| `CounterMode` allows any `BlockCipher` to be treated as a `StreamCipher`.
implementation BlockCipher b bitsPerBlock _ => StreamCipher (b, CounterMode bitsPerBlock) bitsPerBlock where
  generateKeystream (b, CTR nonce counter f) =
    encryptBlock b (append nonce counter)
      :: generateKeystream (b, CTR nonce (f counter) f)

max_stars_repo_name: idris-hackers/idris-crypto

max_issues_repo_name: idris-hackers/idris-crypto

max_forks_repo_name: idris-hackers/idris-crypto


text:
module Data.Prim.Bits32

import public Control.WellFounded
import public Data.DPair
import public Data.Prim.Ord
import public Algebra.Solver.Ring
import Syntax.PreorderReasoning

%default total

unsafeRefl : a === b
unsafeRefl = believe_me (Refl {x = a})

--------------------------------------------------------------------------------
--          (<)
--------------------------------------------------------------------------------

||| Witness that `m < n === True`.
export
data (<) : (m,n : Bits32) -> Type where
  LT : {0 m,n : Bits32} -> (0 prf : (m < n) === True) -> m < n

||| Contructor for `(<)`.
|||
||| This can only be used in an erased context.
export %hint
0 mkLT : (0 prf : (m < n) === True) -> m < n
mkLT = LT

||| Extractor for `(<)`.
|||
||| This can only be used in an erased context.
export
0 runLT : m < n -> (m < n) === True
runLT (LT prf) = prf

||| We don't trust values of type `(<)` too much,
||| so we use this when creating magical results.
export
strictLT : (0 p : m < n) -> Lazy c -> c
strictLT (LT prf) x = x

--------------------------------------------------------------------------------
--          Aliases
--------------------------------------------------------------------------------

||| Flipped version of `(<)`.
public export
0 (>) : (m,n : Bits32) -> Type
m > n = n < m

||| `m <= n` mean that either `m < n` or `m === n` holds.
public export
0 (<=) : (m,n : Bits32) -> Type
m <= n = Either (m < n) (m === n)

||| Flipped version of `(<=)`.
public export
0 (>=) : (m,n : Bits32) -> Type
m >= n = n <= m

||| `m /= n` mean that either `m < n` or `m > n` holds.
public export
0 (/=) : (m,n : Bits32) -> Type
m /= n = Either (m < n) (m > n)

--------------------------------------------------------------------------------
--          Order
--------------------------------------------------------------------------------

0 ltNotEQ : m < n -> Not (m === n)
ltNotEQ x = strictLT x $ assert_total (idris_crash "IMPOSSIBLE: LT and EQ")

0 ltNotGT : m < n -> Not (n < m)
ltNotGT x = strictLT x $ assert_total (idris_crash "IMPOSSIBLE: LT and GT")

0 eqNotLT : m === n -> Not (m < n)
eqNotLT = flip ltNotEQ

export
comp : (m,n : Bits32) -> Trichotomy (<) m n
comp m n = case prim__lt_Bits32 m n of
  0 => case prim__eq_Bits32 m n of
    0 => GT (ltNotGT $ LT unsafeRefl) (ltNotEQ $ LT unsafeRefl) (LT unsafeRefl)
    x => EQ (eqNotLT unsafeRefl) (unsafeRefl) (eqNotLT unsafeRefl)
  x => LT (LT unsafeRefl) (ltNotEQ $ LT unsafeRefl) (ltNotGT $ LT unsafeRefl)

export
Total Bits32 (<) where
  trichotomy   = comp
  transLT p q  = strictLT p $ strictLT q $ LT unsafeRefl

--------------------------------------------------------------------------------
--          Bounds and Well-Foundedness
--------------------------------------------------------------------------------

||| Lower bound of `Bits32`
public export
MinBits32 : Bits32
MinBits32 = 0

||| Upper bound of `Bits32`
public export
MaxBits32 : Bits32
MaxBits32 = 0xffffffff

||| `m >= 0` for all `m` of type `Bits32`.
export
0 GTE_MinBits32 : (m : Bits32) -> m >= MinBits32
GTE_MinBits32 m = case comp MinBits32 m of
  LT x f g => %search
  EQ f x g => %search
  GT f g x => assert_total $ idris_crash "IMPOSSIBLE: Bits32 smaller than 0"

||| Not value of type `Bits32` is less than zero.
export
0 Not_LT_MinBits32 : m < 0 -> Void
Not_LT_MinBits32 = GTE_not_LT (GTE_MinBits32 m)

||| `m <= MaxBits32` for all `m` of type `Bits32`.
export
0 LTE_MaxBits32 : (m : Bits32) -> m <= MaxBits32
LTE_MaxBits32 m = case comp m MaxBits32 of
  LT x f g => %search
  EQ f x g => %search
  GT f g x => assert_total
            $ idris_crash "IMPOSSIBLE: Bits32 greater than \{show MaxBits32}"

||| Not value of type `Bits32` is greater than `MaxBits32`.
export
0 Not_GT_MaxBits32 : m > MaxBits32 -> Void
Not_GT_MaxBits32 = LTE_not_GT (LTE_MaxBits32 m)

||| Every value of type `Bits32` is accessible with relation
||| to `(<)`.
export
accessLT : (m : Bits32) -> Accessible (<) m
accessLT m = Access $ \n,lt => accessLT (assert_smaller m n)

||| `(<)` is well founded.
export %inline
WellFounded Bits32 (<) where
  wellFounded = accessLT

||| Every value of type `Bits32` is accessible with relation
||| to `(>)`.
export
accessGT : (m : Bits32) -> Accessible (>) m
accessGT m = Access $ \n,gt => accessGT (assert_smaller m n)

||| `(>)` is well founded.
export %inline
[GT] WellFounded Bits32 (>) where
  wellFounded = accessGT

--------------------------------------------------------------------------------
--          Arithmetics
--------------------------------------------------------------------------------

||| Safe division.
|||
||| This uses `0 < d` as a constraint instead
||| of `0 /= d`, because in my experience, the former
||| is much more useful.
export %inline
sdiv : (n,d : Bits32) -> (0 prf : 0 < d) => Bits32
sdiv n d = n `div` d

||| Refined division.
|||
||| This comes with a proof that the result is
||| strictly smaller than `n`.
|||
||| This uses `0 < n` as a constraint instead
||| of `0 /= n`, because in my experience, the former
||| is much more useful.
export %inline
rdiv :  (n,d : Bits32)
     -> (0 dgt1 : 1 < d)
     => (0 ngt0 : 0 < n)
     => Subset Bits32 (< n)
rdiv n d = Element (n `div` d) (LT unsafeRefl)

||| Safe modulo.
|||
||| This uses `0 < d` as a constraint instead
||| of `0 /= d`, because in my experience, the former
||| is much more useful.
|||
||| If you need the postcondition that the result is strictly
||| smaller than `d`, use `rmod` instead.
export %inline
smod : (n,d : Bits32) -> (0 prf : 0 < d) => Bits32
smod n d = n `mod` d

||| Refined modulo.
|||
||| This comes with a proof that the result is strictly smaller
||| than `d`.
|||
||| It uses `0 < d` as a constraint instead
||| of `0 /= d`, because in my experience, the former
||| is much more useful.
export %inline
rmod : (n,d : Bits32) -> (0 prf : 0 < d) => Subset Bits32 (< d)
rmod n d = Element (n `mod` d) (LT unsafeRefl)


text:
module Main

%default total

%logging "declare.data.parameters" 20
%logging "eval.eta" 10

-- explicit
data Value : (value : Nat -> Type) -> Type where
  EmptyV : {0 value : Nat -> Type} -> Value (\ n => value n)

data TValue : Nat -> Type where
  MkTupleV : Value (\n => TValue n) -> TValue n


text:
-- Exercises.idr
-- Solutions for exercises of chapter 2

module Exercises

import Data.Vect

-- length function
myLength : List a -> Nat
myLength [] = 0
myLength (x :: xs) = 1 + myLength xs

-- reverse function
myReverse : List a -> List a
myReverse [] = []
myReverse (x :: xs) = (myReverse xs) ++ [x]

-- myVectReverse : Vect n a -> Vect n a
-- myVectReverse [] = []
-- myVectReverse (x :: xs) = (?myVectReverse_rhs xs) ++ (the (Vect 1 _) [x])

-- map function
myMap : (a -> b) -> List a -> List b
myMap f [] = []
myMap f (x :: xs) = f x :: myMap f xs

myVectMap : (a -> b) -> Vect n a -> Vect n b
myVectMap f [] = []
myVectMap f (x :: xs) = f x :: myVectMap f xs

max_stars_repo_name: kkirstein/proglang-playground

max_issues_repo_name: kkirstein/proglang-playground

max_forks_repo_name: kkirstein/proglang-playground


text:
module Minecraft.Base.PreClassic.Air.Export

import public Minecraft.Base.PreClassic.Air.Block.Export

%default total

max_stars_repo_name: po-stulate/postulate

max_issues_repo_name: po-stulate/postulate

max_forks_repo_name: po-stulate/postulate


text:
> module NatBasicProperties

> %default total
> %auto_implicits on
> %access export
> -- %access public export

> {-
> implementation Uninhabited (S n = Z) where
>   uninhabited Refl impossible
> -}

> |||
> predInjective : (left : Nat) -> (right : Nat) -> Not (S left = S right) -> Not (left = right)
> predInjective left right contra = contra . (eqSucc left right)
> %freeze predInjective

> |||
> succInjective' : (left : Nat) -> (right : Nat) -> Not (left = right) -> Not (S left = S right)
> succInjective' left right contra = contra . (succInjective left right)
> %freeze succInjective'

> {-

> ---}

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
module Data.Crypto.MAC.HMAC

import Data.Bits
import Data.Vect

import Data.Crypto.Hash
import Data.Crypto.MAC
import Data.Crypto.Util

%default total
%access private

public export
data HashMAC : Nat -> Type -> Type where
  HMAC : Bits n -> h -> HashMAC n h

formatKey : Hash h b o => HashMAC n h -> Bits b
formatKey {b=b} {n=n} (HMAC k h) =
  if n <= b then zeroExtend k else zeroExtend (hashMessage h [k])

ipad : Hash h b o => HashMAC n h -> Bits b
ipad {b=b} _ = concat (replicate (b `div` 8) (intToBits {n=8} 0x36))

opad : Hash h b o => HashMAC n h -> Bits b
opad {b=b} _ = concat (replicate (b `div` 8) (intToBits 0x5c))

implementation Hash h b o => Signer (HashMAC n h) b o where
  signMessage (HMAC key hash) message =
    let fixedKey = formatKey (HMAC key hash)
    in hashMessage hash
                   (append (fixedKey `xor` opad)
                           (hashMessage hash
                                        (append (fixedKey `xor` ipad)
                                                (concat message))))

-- TODO: Remove when the default impl on MAC works.
implementation Hash h b o => Verifier (HashMAC n h) b o where
  verifyMessage key message digest = digest == signMessage key message

implementation Hash h b o => MAC (HashMAC n h) b o where


text:
module Main

import ContriverText.Tests

main : IO ()
main = appMain {f=FFI_C}

max_stars_repo_name: rocketnia/contrivertext

max_issues_repo_name: rocketnia/contrivertext

max_forks_repo_name: rocketnia/contrivertext


text:
||| Foreign interface to Javascript
|||
||| Copyright 2021, HATTORI, Hiroki
||| This file is released under the MIT license, see LICENSE for more detail.
|||
module Foreign.Javascript.Types

import Data.Maybe

%default total

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

export data JSMaybe : Type -> Type where [external]
export data JSAny : Type where [external]  -- Or, shoukd I use (JSValue "") instead?

public export JSTypes : Type
JSTypes = String

public export %inline
jsTyUndefined, jsTyBoolean, jsTyNumber, jsTyBigInt, jsTyString, jsTySymbol, jsTyFunction, jsTyObject : JSTypes
jsTyUndefined = "undefifned"
jsTyBoolean   = "boolean"
jsTyNumber    = "number"
jsTyBigInt    = "bigint"
jsTyString    = "string"
jsTySymbol    = "symbol"
jsTyFunction  = "function"
jsTyObject    = "object"

export data JSVal : JSTypes -> Type where [external]
public export %inline
JSUndefined, JSBoolean, JSNumber, JSBigInt, JSString, JSSymbol, JSFunction, JSMaybeObject : Type
JSUndefined = JSVal jsTyUndefined
JSBoolean   = JSVal jsTyBoolean
JSNumber    = JSVal jsTyNumber
JSBigInt    = JSVal jsTyBigInt
JSString    = JSVal jsTyString
JSSymbol    = JSVal jsTySymbol
JSFunction  = JSVal jsTyFunction
JSMaybeObject = JSVal jsTyObject -- null or valid object

export data JSObj : String -> Type where [external]

public export %inline
Cast a JSAny => Cast a (JSMaybe JSAny) where
  cast x = believe_me $ the JSAny $ cast x

public export %inline Cast (JSVal a) (JSMaybe (JSVal a)) where cast = believe_me
public export %inline Cast (JSVal a) JSAny where cast = believe_me

public export %foreign "javascript:lambda:x => x?1:0"
jsUnsafeBooleanToInt : (0 _:Cast a (JSMaybe JSAny)) => a -> Int

public export %inline
Cast JSBoolean Bool where
  cast x with (jsUnsafeBooleanToInt x)
    _ | 0 = False
    _ | _ = True

-- --------------------------------------------------------------------------
namespace SpecialValue

  %foreign "javascript:lambda:_ => undefined"
  %inline unsafeJsUndefined : {0 ty:Type} -> ty

  %foreign "javascript:lambda:_ => null"
  %inline unsafeJsNull : (0 ty:Type) -> ty

  %foreign "javascript:lambda:_ => true"
  %inline unsafeJsTrue : (0 ty:Type) => ty
  %foreign "javascript:lambda:_ => false"
  %inline unsafeHsFalse : (0 ty:Type) => ty

  namespace JSAnyValue

    public export
    jsNull : JSAny
    jsNull = unsafeJsNull {ty=JSAny}

    export %inline jsTrue : () => JSAny
    export %inline jsFalse : () => JSAny

  namespace JSMaybe

    export jsUndefined : JSMaybe JSAny
    jsUndefined = unsafeJsUndefined

    %foreign "javascript:lambda:x => ((x === undefined)?1:0)"
    prim__jsIsUndefined : JSMaybe JSAny -> Int

    export jsIsUndefined : JSMaybe ty -> Bool
    jsIsUndefined x = if prim__jsIsUndefined (believe_me x) == 0 then False else True

    public export %inline jsNull, jsTrue, jsFalse : JSMaybe JSAny
    jsNull = believe_me $ the JSAny jsNull
    jsTrue = believe_me $ the JSAny jsTrue
    jsFalse = believe_me $ the JSAny jsFalse

    %foreign "javascript:lambda:(_,x) => (x === null)"
    prim__jsIsNull : JSMaybe JSAny -> JSAny
    public export jsIsNull : Cast a (JSMaybe JSAny) => a -> JSBoolean
    jsIsNull x = believe_me $ prim__jsIsNull $ cast x

    namespace JSAnyValue
      public export %inline jsJust : JSAny -> JSMaybe JSAny
      jsJust = believe_me

    namespace JSValue
      public export %inline jsJust : JSVal t -> JSMaybe (JSVal t)
      jsJust = believe_me

  namespace JSVal
    public export jsUndefined : JSUndefined
    jsUndefined = believe_me $ the (JSMaybe JSAny) jsUndefined

    public export jsNull : JSMaybeObject
    jsNull = believe_me $ the JSAny jsNull

    public export jsTrue, jsFalse : JSBoolean
    jsTrue = believe_me $ the JSAny jsTrue
    jsFalse = believe_me $ the JSAny jsFalse

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

%foreign "javascript:lambda:(_, x) => x"
public export %inline unsafeToJSAny : {0 ty:Type} -> ty -> JSAny

public export %inline Cast Int JSAny where cast = unsafeToJSAny
public export %inline Cast Integer JSAny where cast = unsafeToJSAny
public export %inline Cast Double JSAny where cast = unsafeToJSAny
public export %inline Cast String JSAny where cast = unsafeToJSAny
public export %inline
Cast Bool JSAny where
  cast True = jsTrue
  cast False = jsFalse

public export %inline FromDouble JSAny where fromDouble = unsafeToJSAny
public export %inline FromString JSAny where fromString = unsafeToJSAny

public export %inline Cast Bool JSBoolean where cast = believe_me . unsafeToJSAny

public export %inline FromDouble JSNumber where fromDouble = believe_me .  unsafeToJSAny
public export %inline FromString JSString where fromString = believe_me .  unsafeToJSAny

{-
  you can just use (maybe jsAny cast) instead.
public export %inline Cast (Maybe JSAny) (JSMaybe JSAny) where
public export %inline Cast (Maybe (JSVal ty) (JSMaybe (JSVal ty)) where
-}
-- From JSMaybe
public export %inline
Cast (JSMaybe ty) (Maybe ty) where
  cast x =
    if jsIsUndefined x
      then Nothing
      else Just (believe_me x)

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

%foreign "javascript:lambda:(x, y) => (x == y)"
prim_jsEqual : (0 _:Cast a (JSMaybe JSAny)) => a -> a -> JSAny
%foreign "javascript:lambda:(x, y) => (x === y)"
prim_jsSame : (0 _:Cast a (JSMaybe JSAny)) => a -> a -> JSAny

public export %inline
jsEqual, jsSame: (0 _:Cast a (JSMaybe JSAny)) => a -> a -> JSBoolean
jsEqual x y = believe_me $ prim_jsEqual x y
jsSame x y = believe_me $ prim_jsSame x y

%foreign "javascript:lambda:(x, y) => (x === y)?1:0"
prim__jsEq : JSMaybe JSAny -> JSMaybe JSAny -> Int

public export Eq (JSMaybe a) where (==) x y = if prim__jsEq (believe_me x) (believe_me y) == 0 then False else True
public export Eq JSAny       where (==) x y = if prim__jsEq (believe_me x) (believe_me y) == 0 then False else True
public export Eq (JSVal ty)  where (==) x y = if prim__jsEq (believe_me x) (believe_me y) == 0 then False else True
public export Eq (JSObj ty)  where (==) x y = if prim__jsEq (believe_me x) (believe_me y) == 0 then False else True

-- --------------------------------------------------------------------------
-- Numeric operations
--

%foreign "javascript:lambda:(x,y) => x + y"
prim__jsPlus : JSAny -> JSAny -> JSAny
%foreign "javascript:lambda:(x,y) => x * y"
prim__jsMult : JSAny -> JSAny -> JSAny

public export
Num JSNumber where
  x + y = believe_me $ prim__jsPlus (believe_me x) (believe_me y)
  x * y = believe_me $ prim__jsMult (believe_me x) (believe_me y)
  fromInteger = believe_me . unsafeToJSAny

public export
Num JSBigInt where
  x + y = believe_me $ prim__jsPlus (believe_me x) (believe_me y)
  x * y = believe_me $ prim__jsMult (believe_me x) (believe_me y)
  fromInteger = believe_me . unsafeToJSAny

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

%foreign "javascript:lambda:(_, _, x) => typeof x"
public export %inline jsTypeOf : (0 _:Cast ty (JSMaybe JSAny)) => ty -> JSTypes

public export
toJSVal : Cast a (JSMaybe JSAny) => a -> (ty:JSTypes ** JSVal ty)
toJSVal x = (jsTypeOf x ** believe_me x)

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

public export %inline
JSObject, JSArray, JSMap: Type
JSObject = JSObj "Object"
JSArray  = JSObj "Array"
JSMap    = JSObj "Map"

export
toJSObject : Cast a (JSMaybe JSAny) => a -> (JSObject -> Maybe b) -> Maybe b
toJSObject x f with (toJSVal x)
  _ | ("object" ** x') =
    if jsIsNull x == jsTrue
       then f $ believe_me x'
       else Nothing
  _ | _ = Nothing

%foreign "javascript:lambda:(x,y) => y[x]"
prim_jsProp : String -> JSAny -> JSMaybe JSAny

export
jsProp : String -> JSObj x -> JSMaybe JSAny
jsProp x y = prim_jsProp x (believe_me y)

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


text:
module Frees

import Control.Monad.Freer
import Debug.Trace
import Control.Monad.State
import Control.Monad.Writer
import System
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

mulG : FreeGraph
mulG = do
  x<-liftF $ Constant 2
  y<-liftF $ Constant 3
  liftF $ Mul x y

st : State String Int
st = ST (\str => Id (1, str++"1,"))

stm : State String Int
stm = do
  st
  st

free2state : {x : Type} -> GraphData x -> State String x
free2state (Mul (DoubleT x) (DoubleT y)) = ST (\str => Id (DoubleT $ x*y, str++"mul"))
free2state Placeholder = ST (\str => Id (DoubleT $ 0.0, str++"Placeholder,"))
free2state (Constant x) = ST (\str => Id (DoubleT $ x, str++"Constant,"))

free2li : {x : Type} -> GraphData x -> List x
free2li (Mul (DoubleT x) (DoubleT y)) = pure $ DoubleT $ x*y
free2li Placeholder = pure $ DoubleT 1
free2li (Constant x) = [DoubleT 1,DoubleT x]

free2w : {x : Type} -> GraphData x -> Writer String x
free2w (Mul (DoubleT x) (DoubleT y)) = do
  tell "(Mul (DoubleT x) (DoubleT y))"
  pure $ DoubleT $ x*y
free2w Placeholder = do
  tell "Placeholder"
  pure $ DoubleT 1
free2w (Constant x) = do
  tell "(Constant x)"
  pure $ DoubleT x

f2st : State String Tensor
f2st = foldFreer free2state mulG

data Sess : Type where
  Loginfo : String->String->Sess

data SessData : Type -> Type where
  GetSess : SessData Sess

SessGraph : Type --type of computation graph ,freer graph
SessGraph = Freer SessData Sess

implicit liftd : SessData Sess -> SessGraph
liftd = liftF

sess1 : SessGraph
sess1 = do
  x<-GetSess
  GetSess

max_stars_repo_name: idris-industry/paradise

max_issues_repo_name: idris-industry/paradise

max_forks_repo_name: idris-industry/paradise


text:
module Main

import BTree

main : IO ()
main = do let t = toTree [1,8,2,139287,7,-776,9,3]
          print (BTree.toList t)


text:
module Idris.Codegen.ExtSTG.StringTable

import Libraries.Data.StringMap
import Core.Context
import Idris.Codegen.ExtSTG.Core
import Idris.Codegen.ExtSTG.STG

{-
Local String literals are registered during the compilation of the ANF.expression.

When compiling and LitString is found, we try to register as a TopLevel definition.
If there was already in the StringTable we just return the BinderID for the TopLevel
definition. The StgApp of that binder will evaluate to an Addr which needs to
be wrapped in an StgStringLit data constructor.

When the compilation of the expression is finished, the compilation of the module happens,
at that point the learned TopLevel string definitions needs to be registered in the module.
-}

export
StringTableMap : Type
StringTableMap = StringMap TopBinding

public export
data StringTableR : Type where

public export
StringTableRef : Type
StringTableRef = Ref StringTableR StringTableMap

newEntry
  :  {auto _ : UniqueMapRef}
  -> {auto _ : Ref Counter Int}
  -> FC -> String -> StringTableMap -> Core (StringTableMap, BinderId (SingleValue AddrRep))
newEntry fc str m = case lookup str m of
  Nothing => do
    strBinder <- mkFreshSBinderRepStr GlobalScope (SingleValue AddrRep) fc "stringTableEntry"
    pure (insert str (StgTopStringLit strBinder str) m, binderId strBinder)
  Just (StgTopStringLit strBinder _) =>
    pure (m, binderId strBinder) -- TODO: Check this binder
  Just (StgTopLifted _) =>
    coreFail $ InternalError $ "TopLifted find in StringTable for" ++ show str

||| Create a new StringTableRef that contains a StringTableMap
export
newStringTableRef : Core StringTableRef
newStringTableRef = newRef StringTableR empty

||| Try to register a new String and return its BinderId
export
registerString
  :  {auto _ : StringTableRef}
  -> {auto _ : UniqueMapRef}
  -> {auto _ : Ref Counter Int}
  -> FC -> String
  -> Core (BinderId (SingleValue AddrRep))
registerString fc str = do
  m0      <- get StringTableR
  (m1, b) <- newEntry fc str m0
  put StringTableR m1
  pure b

||| Returns all the toplevel binders registered in the StringTable
export
topLevelBinders
  :  {auto _ : StringTableRef}
  -> Core (List TopBinding)
topLevelBinders = map values $ get StringTableR

max_stars_repo_name: andorp/IdrisExtSTGCodegen

max_issues_repo_name: andorp/IdrisExtSTGCodegen

max_forks_repo_name: andorp/IdrisExtSTGCodegen


text:
import Data.Vect

f1 : (n : Nat) -> Vect n Nat -> Vect (S n) Nat
f1 a b = a :: b

f2 : (n : Nat) -> case n of
  k => Vect k Nat -> Vect (S k) Nat
f2 a b = a :: b

f3 : (n : Nat) -> case n of
  Z => Vect Z Nat -> Vect (S Z) Nat
  (S k) => Vect (S k) Nat -> Vect (S (S k)) Nat
f3 Z b = a :: b
f3 (S a) b = a :: b

f4 : (n : (Nat, Nat)) -> case n of
  (x, y) => Vect x Nat -> Vect (S x) Nat
f4 (_, a) b = a :: b

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
{-
Read
reading
Write
writing
ReadWrite
writing
-}
module Main

import CIL.FFI

{-

  [Flags]
  enum System.IO.FileAccess {
    Read  = 1,
    Write = 2,
    ReadWrite = Read + Write
  }

-}

namespace System.IO.FileAccess

  FileAccessTy : CILTy
  FileAccessTy = corlibTyVal "System.IO.FileAccess"

  FileAccess : Type
  FileAccess = CIL FileAccessTy

  instance IsA Object FileAccess where {}

  Read : CIL_IO FileAccess
  Read = invoke (CILEnumValueOf FileAccessTy "1")
                (CIL_IO FileAccess)

  Write : CIL_IO FileAccess
  Write = invoke (CILEnumValueOf FileAccessTy "2")
                 (CIL_IO FileAccess)

  ReadWrite : CIL_IO FileAccess
  ReadWrite = invoke (CILEnumValueOf FileAccessTy "3")
                     (CIL_IO FileAccess)

namespace System.IO.TFileAccess

  ||| ADT version of `System.IO.FileAccess`.
  data TFileAccess = Read
                   | Write
                   | ReadWrite

  fromEnum : FileAccess -> CIL_IO TFileAccess
  fromEnum e = do
    i32 <- ToInt32 e
    return $
      case i32 of
        1 => Read
        2 => Write
        _ => ReadWrite

describe : TFileAccess -> String
describe Read = "reading"
describe _    = "writing"

testEnumAsObject : FileAccess -> CIL_IO ()
testEnumAsObject e = putStrLn !(ToString e)

testFromEnum : FileAccess -> CIL_IO ()
testFromEnum e = putStrLn (describe !(fromEnum e))

main : CIL_IO ()
main = do
  for_ [!Read, !Write, !ReadWrite] $
    \e => do testEnumAsObject e
             testFromEnum e

max_stars_repo_name: Despair/idris-cil

max_issues_repo_name: Despair/idris-cil

max_forks_repo_name: Despair/idris-cil


text:
module Data.Array16

||| Array of 16 elements.
||| This is designed for speed not as a user facing interface.
public export
record Array16 a where
    constructor MkA16
    i_0 : a
    i_1 : a
    i_2 : a
    i_3 : a
    i_4 : a
    i_5 : a
    i_6 : a
    i_7 : a
    i_8 : a
    i_9 : a
    i_a : a
    i_b : a
    i_c : a
    i_d : a
    i_e : a
    i_f : a

export
Functor Array16 where
    map f = record
        { i_0 $= f
        , i_1 $= f
        , i_2 $= f
        , i_3 $= f
        , i_4 $= f
        , i_5 $= f
        , i_6 $= f
        , i_7 $= f
        , i_8 $= f
        , i_9 $= f
        , i_a $= f
        , i_b $= f
        , i_c $= f
        , i_d $= f
        , i_e $= f
        , i_f $= f
        }

export
Foldable Array16 where
    foldl f z ar = let f' = flip f in
        f' ar.i_f $
        f' ar.i_e $
        f' ar.i_d $
        f' ar.i_c $
        f' ar.i_b $
        f' ar.i_a $
        f' ar.i_9 $
        f' ar.i_8 $
        f' ar.i_7 $
        f' ar.i_6 $
        f' ar.i_5 $
        f' ar.i_4 $
        f' ar.i_3 $
        f' ar.i_2 $
        f' ar.i_1 $
        f' ar.i_0 z

    foldr f z ar =
        f ar.i_0 $
        f ar.i_1 $
        f ar.i_2 $
        f ar.i_3 $
        f ar.i_4 $
        f ar.i_5 $
        f ar.i_6 $
        f ar.i_7 $
        f ar.i_8 $
        f ar.i_9 $
        f ar.i_a $
        f ar.i_b $
        f ar.i_c $
        f ar.i_d $
        f ar.i_e $
        f ar.i_f z

||| Get the `idx`th value.
||| If out of bounds return the last value.
export
index : (idx : Bits64) -> Array16 a -> a
index i ar = case i of
    0x0 => ar.i_0
    0x1 => ar.i_1
    0x2 => ar.i_2
    0x3 => ar.i_3
    0x4 => ar.i_4
    0x5 => ar.i_5
    0x6 => ar.i_6
    0x7 => ar.i_7
    0x8 => ar.i_8
    0x9 => ar.i_9
    0xa => ar.i_a
    0xb => ar.i_b
    0xc => ar.i_c
    0xd => ar.i_d
    0xe => ar.i_e
    _   => ar.i_f

||| Write a new value to the `idx`th value.
||| If out of bounds leave unmodified.
export
write : (idx : Bits64) -> a -> Array16 a -> Array16 a
write idx a ar = case idx of
    0x0 => record {i_0 = a} ar
    0x1 => record {i_1 = a} ar
    0x2 => record {i_2 = a} ar
    0x3 => record {i_3 = a} ar
    0x4 => record {i_4 = a} ar
    0x5 => record {i_5 = a} ar
    0x6 => record {i_6 = a} ar
    0x7 => record {i_7 = a} ar
    0x8 => record {i_8 = a} ar
    0x9 => record {i_9 = a} ar
    0xa => record {i_a = a} ar
    0xb => record {i_b = a} ar
    0xc => record {i_c = a} ar
    0xd => record {i_d = a} ar
    0xe => record {i_e = a} ar
    0xf => record {i_f = a} ar
    _ => ar

||| Update the `idx`th value.
||| If out of bounds leave unmodified.
export
update : (idx : Bits64) -> (a -> a) -> Array16 a -> Array16 a
update idx f ar = case idx of
    0x0 => record {i_0 $= f} ar
    0x1 => record {i_1 $= f} ar
    0x2 => record {i_2 $= f} ar
    0x3 => record {i_3 $= f} ar
    0x4 => record {i_4 $= f} ar
    0x5 => record {i_5 $= f} ar
    0x6 => record {i_6 $= f} ar
    0x7 => record {i_7 $= f} ar
    0x8 => record {i_8 $= f} ar
    0x9 => record {i_9 $= f} ar
    0xa => record {i_a $= f} ar
    0xb => record {i_b $= f} ar
    0xc => record {i_c $= f} ar
    0xd => record {i_d $= f} ar
    0xe => record {i_e $= f} ar
    0xf => record {i_f $= f} ar
    _ => ar

||| Initial an Array with a default value.
export
new : a -> Array16 a
new a = MkA16
    { i_0 = a
    , i_1 = a
    , i_2 = a
    , i_3 = a
    , i_4 = a
    , i_5 = a
    , i_6 = a
    , i_7 = a
    , i_8 = a
    , i_9 = a
    , i_a = a
    , i_b = a
    , i_c = a
    , i_d = a
    , i_e = a
    , i_f = a
    }


text:
module Highlight.Regions

||| There are three types of global names that we will highlight
public export
data NameHL = Function | Constructor | TypeConstructor

implementation Show NameHL where
  showPrec d Function = "Function"
  showPrec d Constructor = "Constructor"
  showPrec d TypeConstructor = "TypeConstructor"

implementation Eq NameHL where
  Function        == Function        = True
  Function        == Constructor     = True
  TypeConstructor == TypeConstructor = True
  _               == _               = False

implementation Ord NameHL where
  compare Function        Function = EQ
  compare Function        Constructor = LT
  compare Function        TypeConstructor = LT
  compare Constructor     Function = GT
  compare Constructor     Constructor = EQ
  compare Constructor     TypeConstructor = LT
  compare TypeConstructor Function = GT
  compare TypeConstructor Constructor = GT
  compare TypeConstructor TypeConstructor = EQ

||| Highlighting instructions
public export
data HighlightType : Type where
  ||| This is a name from the global context
  Name : NameHL -> (docstring : String) -> (type : String) -> HighlightType
  ||| This is a bound name from the local context
  Bound : (isImplicit : Bool) -> HighlightType
  ||| This is a language keyword (or part of a user syntax rule)
  Keyword : HighlightType

implementation Eq HighlightType where
  (Name hl doc ty) == (Name hl' doc' ty') = hl == hl' && doc == doc' && ty == ty'
  (Bound b) == (Bound b') = b == b'
  Keyword == Keyword = True
  _ == _ = False

export
implementation Ord HighlightType where
  compare (Name x y z) (Name a b c) =
    case compare x a of
      LT => LT
      GT => GT
      EQ => case compare y b of
              LT => LT
              GT => GT
              EQ => compare z c
  compare (Name x y z) (Bound _)    = LT
  compare (Name x y z) Keyword      = LT
  compare (Bound _)    (Name _ _ _) = GT
  compare (Bound x)    (Bound y)    = compare x y
  compare (Bound _)    Keyword      = LT
  compare Keyword      (Name _ _ _) = GT
  compare Keyword      (Bound _)    = GT
  compare Keyword      Keyword      = EQ

export
implementation Show HighlightType where
    showPrec d (Name x docstring type) =
        showCon d "Name" $ showArg x ++ showArg docstring ++ showArg type
    showPrec d (Bound isImplicit) =
        showCon d "Bound" $ showArg isImplicit
    showPrec d Keyword = "Keyword"

||| Regions are spans in the source code
public export
record Region meta where
  constructor MkRegion
  fileName    : String
  startLine   : Integer
  startColumn : Integer
  endLine     : Integer
  endColumn   : Integer
  metadata    : meta

export
implementation Functor Region where
  map f (MkRegion fn sl sc el ec meta) =
    MkRegion fn sl sc el ec (f meta)

export
implementation Show a => Show (Region a) where
  showPrec d x = showCon d "MkRegion" $
                   showArg (fileName x) ++
                   showArg (startLine x) ++ showArg (startColumn x) ++
                   showArg (endLine x) ++ showArg (endColumn x) ++
                   showArg (metadata x)

implementation Eq a => Eq (Region a) where
  r1 == r2 = fileName r1    == fileName r2 &&
             startLine r1   == startLine r2 &&
             startColumn r1 == startColumn r2 &&
             endLine r1     == endLine r2 &&
             endColumn r1   == endColumn r2 &&
             metadata r1    == metadata r2

||| This Ord implementation is important - we must sort regions in
||| increasing order of start position, then increasing order of end
||| position. That means we can traverse them in order for opening and
||| use a stack to track end positions.
export
implementation Ord a => Ord (Region a) where
  compare r1 r2 =
      case compare (fileName r1) (fileName r2) of
        LT => LT
        GT => GT
        EQ => case compare (startLine r1) (startLine r2) of
                LT => LT
                GT => GT
                EQ => case compare (startColumn r1) (startColumn r2) of
                        LT => LT
                        GT => GT
                        EQ => case compare (endLine r1) (endLine r2) of
                                LT => LT
                                GT => GT
                                EQ => case compare (endColumn r1) (endColumn r2) of
                                        LT => LT
                                        GT => GT
                                        EQ => compare (metadata r1) (metadata r2)


text:
-- Copyright (c) 2013 Radek Micek

module Algo

-- s - state, i - reason of interruption, r - result of whole computation.
data AlgoResult s i r
  = Interrupt s i (s -> AlgoResult s i r)
  | Finish s r

data Algo s i r a
  = MkAlgo (s -> (a -> s -> AlgoResult s i r) -> AlgoResult s i r)

runAlgo : Algo s i r a -> s -> (a -> s -> AlgoResult s i r) -> AlgoResult s i r
runAlgo (MkAlgo x) = x

algoReturn : a -> Algo s i r a
algoReturn a = MkAlgo $ \s, k => k a s

algoBind : Algo s i r a -> (a -> Algo s i r b) -> Algo s i r b
algoBind x f = MkAlgo $ \s, k =>
  runAlgo x s (\a, s' => runAlgo (f a) s' k)

instance Functor (Algo s i r) where
  fmap f x = algoBind x (\x' => algoReturn (f x'))

instance Applicative (Algo s i r) where
  pure = algoReturn
  f <$> x =
    algoBind f (\f' =>
    algoBind x (\x' =>
    algoReturn (f' x')))

instance Monad (Algo s i r) where
  return = algoReturn
  (>>=) = algoBind

run : s -> Algo s i r r -> AlgoResult s i r
run s x = runAlgo x s (\r, s' => Finish s' r)

interrupt : i -> Algo s i r ()
interrupt i = MkAlgo $ \s, k => Interrupt s i (k ())

resume : s -> (s -> AlgoResult s i r) -> AlgoResult s i r
resume s k = k s

put : s -> Algo s i r ()
put s = MkAlgo $ \_, k => k () s

get : Algo s i r s
get = MkAlgo $ \s, k => k s s

max_stars_repo_name: radekm/satviz

max_issues_repo_name: radekm/satviz

max_forks_repo_name: radekm/satviz


text:
import Control.Linear.LIO

import Network.Socket

data SocketState = Ready | Bound | Listening | Open | Closed

data Socket : SocketState -> Type where
     MkSocket : Socket.Data.Socket -> Socket st

newSocket : LinearIO io
      => (fam  : SocketFamily)
      -> (ty   : SocketType)
      -> (pnum : ProtocolNumber)
      -> (success : (1 _ : Socket Ready) -> L io ())
      -> (fail : SocketError -> L io ())
      -> L io ()
newSocket fam ty pnum success fail
    = do Right rawsock <- socket fam ty pnum
               | Left err => fail err
         success (MkSocket rawsock)

bind : LinearIO io =>
       (1 _ : Socket Ready) ->
       (addr : Maybe SocketAddress) ->
       (port : Port) ->
       L io {use=1} (Res Bool (\res => Socket (case res of
                                                    False => Closed
                                                    True => Bound)))
bind (MkSocket sock) addr port
    = do ok <- Socket.bind sock addr port
         if ok == 0
            then pure1 (True # ?foo1)
            else pure1 (False # ?foo2)


text:
module Cosets

import Group
%access public export

--The type of proofs that a type trav Transverses a given coset only once,
--if at all
CosetInj: (h: Type) -> (pfh: Group h) -> (g: Type) -> (pfg: Group g) ->
          (sbgrp: Subgroup h pfh g pfg) ->
          (trav: Type) -> (f: trav -> g) -> Type
CosetInj  h (MkGroup h (+) pfh) g (MkGroup g (*) pfg) sbgrp trav f =
  ((x: trav) -> (y: trav) ->
  (p: h ** (f x) = (incl p)*(f y)) -> (x = y)) where
  incl = (fst sbgrp)

--The type of proofs that a type trav Transverses every coset of a given
-- group g wrt a subgroup h
CosetAll: (h: Type) -> (pfh: Group h) -> (g: Type) -> (pfg: Group g) ->
          (sbgrp: Subgroup h pfh g pfg) ->
          (trav: Type) -> (f: trav -> g) -> Type
CosetAll h (MkGroup h (+) pfh) g (MkGroup g (*) pfg) sbgrp trav f =
  ((a: g) ->
  (p: h ** (t: trav ** ((incl p)*(f t) = a)))) where
  incl = (fst sbgrp)

-- Transversal type - the type of proofs that a given type is a Transversal
-- of a group g wrt a subgroup h
IsTransversal: (h: Type) -> (pfh: Group h) -> (g: Type) -> (pfg: Group g) ->
               (sbgrp: Subgroup h pfh g pfg) -> (trav: Type) -> Type
IsTransversal h pfh g pfg sbgrp trav = DPair (trav -> g) (\f =>
  (CosetInj h pfh g pfg sbgrp trav f,
  CosetAll  h pfh g pfg sbgrp trav f)
  )

--The transversal data type
data Transversal: (trav: Type) -> Type where
  MkTransversal: (h: Type) -> (pfh: Group h) -> (g: Type) -> (pfg: Group g) ->
                 (sbgrp: Subgroup h pfh g pfg) -> (trav: Type) ->
                 (IsTransversal h pfh g pfg sbgrp trav) -> Transversal trav

--Defining the multiplication operation between elements of a traversal
MulTrans: (trav: Type) -> (Transversal trav) -> trav -> trav -> trav
MulTrans trav (MkTransversal h (MkGroup h (+) pfh) g (MkGroup g (*) pfg) sbgrp trav pftrav) y z = (fst (snd ((snd (snd pftrav)) ((f y)*(f z))))) where
  f: trav -> g
  f = (fst pftrav)


text:
module Doc

||| World!
export
world : Nat -> Nat
world x = x*2

nope : Nat
nope = 0

export
||| Hello!
hello : Int -> Int
hello x = x*2


text:
mutual
  record A where
    b : B
  record B where
    a : A


text:
import Data.String

import System.File
import System.Info

main : IO ()
main = do
    Right f <- popen ("echo " ++ escapeArg "Hello, world") Read
        | Left err => printLn err
    Right contents <- fGetLine f
        | Left err => printLn err
    printLn $ trim contents
    0 <- pclose f
        | n => printLn n

    let cmd : List String = if not isWindows
                               then ["printf", "Hello, %s", "$PATH"]
                               else ["echo", "Hello, $PATH"]
    Right f <- popen cmd Read
        | Left err => printLn err
    Right contents <- fGetLine f
        | Left err => printLn err
    printLn $ (ifThenElse isWindows trim id) contents
    0 <- pclose f
        | n => printLn n

    Right f <- popen ["exit", "17"] Read
        | Left err => printLn err
    printLn !(pclose f)


text:
module RecordInWhere

import Data.Vect

f1 : Int
f1 = 5 where
  data X : Type where
    MkX : (a : Int) -> X

f2 : Int
f2 = 5 where
  record X where
    constructor MkX
    a : Int

f3 : Nat -> Int
f3 x = 5 where
  data X : Type where
    MkX : (a : Int) -> X

f4 : Nat -> Int
f4 x = 5 where
  data X : Type where
    MkX : (a : Vect x Int) -> X

f5 : Nat -> Int
f5 x = 5 where
  record X5 where
    constructor MkX5
    a : Int

f6 : Nat -> Int
f6 x = 5 where
  record X6 where
    constructor MkX6
    a : Vect x Int


text:
{- Ctrl-Alt-A: Add definition
   Ctrl-Alt-C: Case split
   Ctrl-Alt-D: Documentation
   Ctrl-Alt-L: Lift hole: Lifts a hole to the top level as a new function definition
   Ctrl-Alt-M: Match: Replaces a hole with a case expression that matches on an intermediate result
   Ctrl-Alt-R: Reloads and typechecks the current buffer
   Ctrl-Alt-S: Search
   Ctrl-Alt-T: Type-check: Displays the type under cursor -}
module Main

import Data.Vect

-- 6.1.1

Position : Type
Position = (Double, Double)

Polygon : Nat -> Type
Polygon n = Vect n Position

tri : Polygon 3
tri = [(0.0, 0.0), (3.0, 0.0), (0.0, 4.0)]

tri2 : Polygon 3
tri2 = [(0, 0), (0, 0), (0, 0)]

-- 6.1.2

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

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

-- 6.2.1

AdderType : (numargs : Nat) -> Type -> Type
AdderType Z     t = t
AdderType (S k) t = (next : t) -> AdderType k t

adder : Num numType => (numargs : Nat) -> (acc : numType) -> AdderType numargs numType
adder Z     acc = acc
adder (S k) acc = \next => adder k (next + acc)

adder1 : (numargs : Nat) -> (acc : Int) -> AdderType numargs Int
adder1 = adder

-- 6.2.2

data Format : Type where
  Number : Format -> Format
  Str    : Format -> Format
  Lit    : String -> Format -> Format
  End    : Format

PrintfType : Format -> Type
PrintfType (Number x) = Int -> PrintfType x
PrintfType (Str x) = String -> PrintfType x
PrintfType (Lit x y) = PrintfType y
PrintfType End = String

toFormat : List Char -> Format
toFormat [] = End
toFormat ('%' :: 'd' :: chars) = Number (toFormat chars)
toFormat ('%' :: 's' :: chars) = Str (toFormat chars)
toFormat ('%' :: chars) = Lit "%" (toFormat chars)
toFormat (c :: chars) = case toFormat chars of
  Lit l f => Lit (strCons c l) f
  fmt => Lit (strCons c "") fmt

printFmt : (fmt : Format) -> (acc : String) -> PrintfType fmt
printFmt (Number x) acc = \num => printFmt x (acc ++ show num)
printFmt (Str x) acc = \str => printFmt x (acc ++ str)
printFmt (Lit x y) acc = printFmt y (acc ++ x)
printFmt End acc = acc

printf : (s : String) -> (PrintfType (toFormat (unpack s)))
printf fmt = printFmt (toFormat (unpack fmt)) ""

main : IO ()
main = do
  printLn tri
  printLn tri2
  printLn (valToString False "  string  ")
  printLn (valToString True 42)
  printLn (adder1 0 10)
  printLn (adder1 1 10 15)
  printLn (adder1 2 1 4 7)
  putStrLn (printf "Hello!")
  putStrLn (printf "Answer : %d" 42)
  putStrLn (printf "%s numner %d" "Page" 97)

max_stars_repo_name: pdani/idris-grin

max_issues_repo_name: pdani/idris-grin

max_forks_repo_name: pdani/idris-grin


text:
-- --------------------------------------------------------------- [ Nonce.idr ]
-- Module      : Nonce
-- Description : Types for Nonces
-- Copyright   : (c) Jan de Muijnck-Hughes
-- License     : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
module Crypto.Nonce

import Crypto.Common

data TyNonce = Zero | Random

||| Nonces for guaranteeing freshness.
|||
||| @ s The setting.
||| @ tyN The nonce type.
||| @ l The length.
data Nonce : (s : Setting) -> (tyN : TyNonce) -> (l : Nat) -> Type where
  ||| The all zero nonce for asymmetric encryption.
  MkZeroPkNonce : Vect n a -> Nonce Asymm Zero n
  ||| A randomly generated nonce for asymmetric encryption.
  MkRndPkNonce  : Vect n a -> Nonce Asymm Random n

  ||| The all zero nonce for symmetric encryption.
  MkZeroSkNonce : Vect n a -> Nonce Symm Zero n
  ||| A randomly generated nonce for symmetric encryption.
  MkRndSkNonce  : Vect n a -> Nonce Symm Random n

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

max_stars_repo_name: silky/idris-crypto-types

max_issues_repo_name: silky/idris-crypto-types

max_forks_repo_name: silky/idris-crypto-types


text:
module Idris.IDEMode.SyntaxHighlight

import Core.Context
import Core.InitPrimitives
import Core.Metadata
import Core.TT

import Idris.REPL
import Idris.IDEMode.Commands

import Data.List

%default covering

data Decoration : Type where
  Typ : Decoration
  Function : Decoration
  Data : Decoration
  Keyword : Decoration
  Bound : Decoration

SExpable Decoration where
  toSExp Typ = SymbolAtom "type"
  toSExp Function = SymbolAtom "function"
  toSExp Data = SymbolAtom "data"
  toSExp Keyword = SymbolAtom "keyword"
  toSExp Bound = SymbolAtom "bound"

record Highlight where
  constructor MkHighlight
  location : FC
  name : Name
  isImplicit : Bool
  key : String
  decor : Decoration
  docOverview : String
  typ : String
  ns : String

SExpable FC where
  toSExp (MkFC fname (startLine, startCol) (endLine, endCol))
    = SExpList [ SExpList [ SymbolAtom "filename", StringAtom fname ]
               , SExpList [ SymbolAtom "start", IntegerAtom (cast startLine + 1), IntegerAtom (cast startCol + 1) ]
               , SExpList [ SymbolAtom "end", IntegerAtom (cast endLine + 1), IntegerAtom (cast endCol + 1) ]
               ]
  toSExp EmptyFC = SExpList []

SExpable Highlight where
  toSExp (MkHighlight loc nam impl k dec doc t ns)
    = SExpList [ toSExp loc
               , SExpList [ SExpList [ SymbolAtom "name", StringAtom (show nam) ]
                          , SExpList [ SymbolAtom "namespace", StringAtom ns ]
                          , SExpList [ SymbolAtom "decor", toSExp dec ]
                          , SExpList [ SymbolAtom "implicit", toSExp impl ]
                          , SExpList [ SymbolAtom "key", StringAtom k ]
                          , SExpList [ SymbolAtom "doc-overview", StringAtom doc ]
                          , SExpList [ SymbolAtom "type", StringAtom t ]
                          ]
               ]

inFile : String -> (FC, (Name, Nat, ClosedTerm)) -> Bool
inFile fname (MkFC file _ _, _) = file == fname
inFile _     (EmptyFC, _)       = False

||| Output some data using current dialog index
export
printOutput : {auto o : Ref ROpts REPLOpts} ->
              SExp -> Core ()
printOutput msg
  =  do opts <- get ROpts
        case idemode opts of
          REPL _ => pure ()
          IDEMode i _ f =>
            send f (SExpList [SymbolAtom "output",
                              msg, toSExp i])

outputHighlight : {auto opts : Ref ROpts REPLOpts} ->
                  Highlight -> Core ()
outputHighlight h =
  printOutput $ SExpList [ SymbolAtom "ok"
                         , SExpList [ SymbolAtom "highlight-source"
                                    , toSExp hlt
                                    ]
                         ]
  where
    hlt : List Highlight
    hlt = [h]

outputNameSyntax : {auto opts : Ref ROpts REPLOpts} ->
                   (FC, (Name, Nat, ClosedTerm)) -> Core ()
outputNameSyntax (fc, (name, _, term)) =
  let dec = case term of
                 (Local fc x idx y) => Just Bound

                 -- See definition of NameType in Core.TT for possible values of Ref's nametype field
                 -- data NameType : Type where
                 -- Bound   : NameType
                 -- Func    : NameType
                 -- DataCon : (tag : Int) -> (arity : Nat) -> NameType
                 -- TyCon   : (tag : Int) -> (arity : Nat) -> NameType
                 (Ref fc Bound name) => Just Bound
                 (Ref fc Func name) => Just Function
                 (Ref fc (DataCon tag arity) name) => Just Data
                 (Ref fc (TyCon tag arity) name) => Just Typ
                 (Meta fc x y xs) => Just Bound
                 (Bind fc x b scope) => Just Bound
                 (App fc fn arg) => Just Bound
                 (As fc x as pat) => Just Bound
                 (TDelayed fc x y) => Nothing
                 (TDelay fc x ty arg) => Nothing
                 (TForce fc x y) => Nothing
                 (PrimVal fc c) => Just Typ
                 (Erased fc imp) => Just Bound
                 (TType fc) => Just Typ
      hilite = Prelude.map (\ d => MkHighlight fc name False "" d "" (show term) "") dec
  in maybe (pure ()) outputHighlight hilite

export
outputSyntaxHighlighting : {auto m : Ref MD Metadata} ->
                           {auto opts : Ref ROpts REPLOpts} ->
                           String ->
                           REPLResult ->
                           Core REPLResult
outputSyntaxHighlighting fname loadResult = do
  allNames <- filter (inFile fname) . names <$> get MD
--  decls <- filter (inFile fname) . tydecls <$> get MD
  _ <- traverse outputNameSyntax allNames -- ++ decls)
  pure loadResult


text:
module Main

removeDuplicatesFromSorted : Eq a => List a -> List a
removeDuplicatesFromSorted [] = []
removeDuplicatesFromSorted (x :: []) = [x]
removeDuplicatesFromSorted (x :: (y :: ys)) with (x == y)
  removeDuplicatesFromSorted (x :: (y :: ys)) | False = x :: removeDuplicatesFromSorted (y :: ys)
  removeDuplicatesFromSorted (x :: (y :: ys)) | True = removeDuplicatesFromSorted (y :: ys)

elemInAll : Eq a => a -> List (List a) -> Bool
elemInAll x xss = all (elem x) xss

record Group where
  constructor MkGroup
  questions : List Char
  answers : List (List Char)

Show Group where
  show (MkGroup questions answers) = "Group " ++ show questions ++ " " ++ show answers

parseGroups : String -> List (List (List Char))
parseGroups = map (map unpack) . splitOn "" . lines

createGroup : List (List Char) -> Group
createGroup unsortedAnswers = MkGroup questions answers
  where answers = sort $ map sort unsortedAnswers
        questions = removeDuplicatesFromSorted . sort $ concat answers

countYesAnswers : Group -> Nat
countYesAnswers (MkGroup questions answers) = length questions

countEveryoneYesAnswers : Group -> Nat
countEveryoneYesAnswers (MkGroup questions answers) =
  length $ filter id $ elemInAll <$> questions <*> pure answers

main : IO ()
main = do
  f <- readFile "./data"

  putStrLn "Part 1"
  print $ (sum . map countYesAnswers . map createGroup . parseGroups) <$> f
  putStrLn ""

  putStrLn "Part 2"
  print $ (sum . map countEveryoneYesAnswers . map createGroup . parseGroups) <$> f
  putStrLn ""


text:
module Network.HTTP.Pool.IOStuff

import Utils.Handle
import Utils.Bytes
import Utils.Misc
import Utils.Handle.C
import Control.Linear.LIO
import Network.Socket
import Data.String
import Data.String.Extra
import Network.HTTP.Message
import Network.HTTP.Header
import Utils.String
import Data.Nat
import Data.Vect
import System.Future
import System
import Data.Fin

%hide Network.Socket.close

public export
OkOrError : Type -> Type -> Type
OkOrError t_ok t_closed = Res Bool $ \ok => if ok then Res String (const $ Handle' t_ok t_closed) else Res String (const t_closed)

public export
read_line' : LinearIO m =>
             List Bits8 ->
             (1 _ : Handle' t_ok t_closed) ->
             L1 m $ OkOrError t_ok t_closed
read_line' acc handle = do
  (True # ([char] # handle)) <- read handle 1
  | (True # (char # handle)) => do
    handle' <- close handle
    pure1 (False # ("read line failed, somehow read returns \{show (length char)} bytes instead of 1" # handle'))
  | (False # (error # handle)) => pure1 (False # ("read line failed: \{error}" # handle))
  case char of
    -- \n = 10, \r = 13
    10 => do
      let Just string = utf8_pack $ reverse acc
      | Nothing => do
        handle' <- close handle
        pure1 (False # ("read line failed, cannot parse utf8 line" # handle'))
      pure1 (True # (string # handle))
    13 => do
      (True # ([10] # handle)) <- read handle 1
      | (True # ([char] # handle)) => do
        handle' <- close handle
        pure1 (False # ("read line failed, \\n expected after \\r, got \{show char} instead" # handle'))
      | (True # (char # handle)) => do
        handle' <- close handle
        pure1 (False # ("read line failed, somehow read returns \{show (length char)} bytes instead of 1" # handle'))
      | (False # (error # handle)) => pure1 (False # ("read line failed: \{error}" # handle))
      let Just string = utf8_pack $ reverse acc
      | Nothing => do
        handle' <- close handle
        pure1 (False # ("read line failed, cannot parse utf8 line" # handle'))
      pure1 (True # (string # handle))
    x => read_line' (x :: acc) handle

public export
read_line : LinearIO m => (1 _ : Handle' t_ok t_closed) -> L1 m $ OkOrError t_ok t_closed
read_line = read_line' []

public export
read_until_empty_line' : String -> LinearIO m => (1 _ : Handle' t_ok t_closed) -> L1 m $ OkOrError t_ok t_closed
read_until_empty_line' acc handle = do
  (True # (line # handle)) <- read_line handle
  | (False # (error # handle)) => pure1 (False # ("read line failed: \{error}" # handle))
  if null line then pure1 (True # (acc # handle)) else read_until_empty_line' (acc <+> "\n" <+> line) handle

public export
read_until_empty_line : LinearIO m => (1 _ : Handle' t_ok t_closed) -> L1 m $ OkOrError t_ok t_closed
read_until_empty_line = read_until_empty_line' ""


text:
module Http.Response

import Lightyear.Core
import Lightyear.Combinators
import Lightyear.Char
import Lightyear.Strings

import public Data.SortedMap
import public Http.Request
import public Http.RawResponse
import public Http.Error

import Data.Bytes as B

%access export

public export
record ResponseStatus where
  constructor MkResponseStatus
  responseStatusVersion : String
  responseStatusCode : Int
  responseStatusComment : String

implementation Show ResponseStatus where
  show (MkResponseStatus ver code cmt) =
    "MkResponseStatus " ++ ver ++ " " ++ show code ++ " " ++ cmt

public export
record Response a where
  constructor MkResponse
  responseStatus : ResponseStatus
  ||| A Map of all response headers with the key being all lowercase
  responseHeaders : SortedMap String String
  responseBody : a

getHeader : Response a -> String -> Maybe String
getHeader r k = lookup (toLower k) (responseHeaders r)

private
responseStatusParser : Parser ResponseStatus
responseStatusParser = do
  version <- some (noneOf " \n\r")
  space
  statusCode <- integer
  space
  comment <- some (noneOf "\n\r")
  crlf
  pure $ MkResponseStatus (pack version) statusCode (pack comment)

private
headerFieldParser : Parser (String, String)
headerFieldParser = do
  key <- some (noneOf ":\n\r")
  char ':' >! opt (char ' ')
  value <- some (noneOf "\n\r")
  opt (char ' ') >! crlf
  pure (pack (toLower <$> key), pack value)

private
parseBodyChunkEncoded : Parser String
parseBodyChunkEncoded = do
    x <- hexParser
    opt $ do
      spaces
      char ';'
      some (noneOf "\n\r")
    crlf
    if x == 0 then many (noneOf "\n\r") *> crlf *> pure ""
              else liftA2 (++) (parseBody x) parseBodyChunkEncoded
  where
    hexParser' : Int -> Parser Int
    hexParser' x = do
      c <- hexDigit
      hex2 <- opt $ hexParser' (x*16)
      let hex = ord $ toUpper c
      let num = if hex >= ord '0' && hex <= ord '9'
                   then hex - ord '0'
                   else 10 + hex - ord 'A'
      case hex2 of
           Just x => pure (x * num)
           Nothing => pure num
    hexParser : Parser Int
    hexParser = hexParser' 1
    parseBody : Int -> Parser String
    parseBody x = do
      n <- pack <$> many (oneOf "\n\r")
      s <- pack <$> some (noneOf "\n\r")
      let len = the Int $ cast $ B.length (B.fromString (s ++ n))
      if (x - len) < 0 then fail ("Somehow the String " ++ s ++ n ++ " is longer than " ++ show x)
      else if (x - len) == 0 then crlf *> pure s
                           else map (s ++) $ parseBody (x - len)

private
bodyParser : SortedMap String String -> Parser String
bodyParser map with (lookup "content-length" map)
  | Nothing = parseBodyChunkEncoded
  | Just x = pack <$> ntimes (cast $ the Int (cast x)) anyChar

private
responseParser : Parser (Response String)
responseParser = do
  status <- responseStatusParser
  fields <- many headerFieldParser
  body <- crlf >! bodyParser (fromList fields)
  pure $ MkResponse status (fromList fields) body

parseResponse : RawResponse String -> Either HttpError (Response String)
parseResponse (MkRawResponse input) = case parse responseParser input of
                                           Left err => Left $ HttpParseError err
                                           Right re => Right re

max_stars_repo_name: unthingable/idris-https

max_issues_repo_name: unthingable/idris-https

max_forks_repo_name: unthingable/idris-https


text:
-- --------------------------------------------------------------- [ Model.idr ]
-- Description : The Model
-- Copyright   : (c) Jan de Muijnck-Hughes
-- License     : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
module Commons.Options.ArgParse.Model

%access public export

data Arg : Type where
  Flag : String -> Arg
  KeyValue : String -> String -> Arg
  File : String -> Arg

Show Arg where
  show (Flag f) = "[Flag " ++ show f ++ "]"
  show (KeyValue k v) = "[KeyValue " ++ show k ++ " : " ++ show v ++ "]"
  show (File fs) = "[File " ++ show fs ++ "]"

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

max_stars_repo_name: jfdm/idris-common

max_issues_repo_name: jfdm/idris-common

max_forks_repo_name: jfdm/idris-common


text:
module Circuits.NetList.Main

import System
import System.File

import Data.String
import Data.Fin
import Data.List.Elem
import Data.List1

import Text.Lexer
import Text.Parser

import Toolkit.Data.Location
import Toolkit.Text.Lexer.Run
import Toolkit.Text.Parser.Run

import Toolkit.Data.Graph.EdgeBounded
import Toolkit.Data.Graph.EdgeBounded.HasExactDegree
import Toolkit.Data.List.Occurs.Does

import Circuits.NetList
import Circuits.NetList.Pretty

netlist : (fname : String)
                -> NetList ()
netlist fname
  = do putStrLn "// LOG : Starting NetList "

       ast <- fromFile fname

       log "// \{show ast}"

       log "// LOG : Parsing Successful"

       term <- Design.check ast

       log "// \{show term}"

       log "// LOG : Type Checking Complete"

       prf <- isSound term

       log "// LOG : Soundness Check Complete"

       putStrLn ((showGraph . fst . getGraph) prf)

       log "// LOG : BYE"

main : IO Unit
main
  = do fname <- processArgs !getArgs
       run (netlist fname)

-- [ EOF ]

max_stars_repo_name: border-patrol/linear-circuits

max_issues_repo_name: border-patrol/linear-circuits

max_forks_repo_name: border-patrol/linear-circuits


text:
module Libraries.Utils.String

%default total

export
dotSep : List String -> String
dotSep [] = ""
dotSep [x] = x
dotSep (x :: xs) = x ++ concat ["." ++ y | y <- xs]

export
stripSurrounds : (lead : Nat) -> (tail : Nat) -> String -> String
stripSurrounds lead tail str = substr lead (length str `minus` (lead + tail)) str

export
stripQuotes : String -> String
stripQuotes = stripSurrounds 1 1

export
lowerFirst : String -> Bool
lowerFirst "" = False
lowerFirst str = isLower $ assert_total $ prim__strHead str

escapeGeneric : Char -> List Char -> String -> String
escapeGeneric esc toEscape = pack . foldr escape [] . unpack
  where
    escape : Char -> List Char -> List Char
    escape c cs =
      if elem c toEscape
        then (esc :: c :: cs)
        else (c :: cs)

export
escapeStringUnix : String -> String
escapeStringUnix = escapeGeneric '\\' ['"', '\\']

export
escapeStringChez : String -> String
escapeStringChez = escapeGeneric '\\' ['\'', '\\']