text:
module MacroInvoke

import Data.Vect
import Tokenizer
import MacroDef

%default total
%access public export

record MacroInv where
  constructor Invoke
  indent : Nat
  appliedArgs : List (String, String)
  macroBody : List String

{-

applyArgs : (def : MacroDef) -> List String -> Maybe (ArgVect def)
applyArgs (Define _ params _) args = replace args <$> lenEq params args

macroInv : (def : MacroDef) -> MacroHeader -> Maybe (MacroInv def)
macroInv def (MacroH indent _ args) =
  Invoke indent <$> applyArgs def args

data State
  = Outside
  | RunningMacro (MacroInv def)

doingIt : List MacroDef -> State -> List String -> List String
doingIt defs Outside [] = []
doingIt defs Outside (x :: xs) =
  case parseHeaderTok "invoke" x of
    Just h =>
      case find (\d => name h == name d) defs of
        Nothing => doingIt defs Outside xs
        Just d  => ?asdf
    Nothing => doingIt defs Outside xs
doingIt defs (RunningMacro x) [] = []
doingIt defs (RunningMacro y) (x :: xs) =
  if parseFooter "inv" x
  then ?asdf
  else doingIt defs (RunningMacro y) xs

invokeMacros : List MacroDef -> List String -> List String
invokeMacros def = doingIt def Outside

 -}

max_stars_repo_name: Kazark/fspp

max_issues_repo_name: Kazark/fspp

max_forks_repo_name: Kazark/fspp


text:
module GoalQQuote

import Data.Vect
import Language.Reflection
import Language.Reflection.Utils

uCon : TT
uCon = `(() : ())

uTy : TT
uTy = `(() : Type)

isDefault : TT -> Bool
isDefault `(()) = True
isDefault _ = False

pTy : TT -> TT -> TT
pTy a b = `((~a, ~b) : Type)

pair : TT -> TT -> TT
pair a b = `((~a, ~b) : (Nat, Nat))

vect : TT
vect = `([1,2] : Vect 2 Nat)

namespace Main
  main : IO ()
  main = putStrLn $
           if isDefault uCon then "con"
                             else if isDefault uTy then "ty"
                                                   else "neither"

ext: idr

max_stars_repo_name: grin-compiler/idris-grin

max_issues_repo_name: grin-compiler/idris-grin

max_forks_repo_name: grin-compiler/idris-grin


text:
module NewEden.Implementations.GMP

import Prelude

import NewEden.Algebra
import NewEden.NaturalAxioms

{- GMP

   If you assume the GMP implementation is valid, you can use
   Natural GMP by importing this package!

-}

data UInteger : Type where
  MkUInteger : (a : Integer) -> (isNonNegative : a < 0 = False)  -> UInteger

instance Show UInteger where
  show (MkUInteger x _) = show x

GMPplus : UInteger -> UInteger -> UInteger
GMPplus (MkUInteger a _) (MkUInteger b _) = MkUInteger (a + b) (believe_me ())

minus : UInteger -> UInteger -> UInteger
minus (MkUInteger a _) (MkUInteger b _) = MkUInteger (a - b) (believe_me ())

GMPmultiply : UInteger -> UInteger -> UInteger
GMPmultiply (MkUInteger a _) (MkUInteger b _) = MkUInteger (a * b) (believe_me ())

GMPzero : UInteger
GMPzero = MkUInteger 0 Refl

GMPone : UInteger
GMPone = MkUInteger 1 Refl

GMPplusAssociative : AssociativeFunction UInteger GMPplus
GMPplusAssociative = MkAssociativeFunction GMPplus (\_,_,_ => believe_me ())

GMPplusMonoid : Monoid UInteger GMPplus GMPzero
GMPplusMonoid = MkMonoid GMPplusAssociative GMPzero (\_ => believe_me ()) (\_ => believe_me ())

GMPmultiplyAssociative : AssociativeFunction UInteger GMPmultiply
GMPmultiplyAssociative = MkAssociativeFunction GMPmultiply (\_,_,_ => believe_me ())

GMPmultiplyMonoid : Monoid UInteger GMPmultiply GMPone
GMPmultiplyMonoid = MkMonoid GMPmultiplyAssociative GMPone (\_ => believe_me ()) (\_ => believe_me ())

GMPcompare : (a:UInteger) -> (b:UInteger) -> Either (a = b) (Either ((c ** ((GMPplus a c = b, (c = GMPzero -> Void))))) (c ** ((GMPplus b c = a, (c = GMPzero -> Void)))))
GMPcompare (MkUInteger x xp) (MkUInteger y yp) =
  case x == y of
    True => Left (believe_me ())
    _ => case x < y of
           True => Right $ Left ((minus (MkUInteger y yp) (MkUInteger x xp)) ** (believe_me (), believe_me ()))
           False => Right $ Right ((minus (MkUInteger x xp) (MkUInteger y yp)) ** (believe_me (), believe_me ()))

GMP : NaturalProperties UInteger
GMP =
  ProofNaturalProperties
      GMPzero
      GMPone
      (believe_me ())
      GMPplus
      (MkCommutativeFunction GMPplus (believe_me ()))
      GMPplusMonoid
      (MkStrictMonoid GMPplusMonoid (\_,_,_ => believe_me ()))
      (\x => MkMonomorphicFunction (GMPplus x) (\_,_,_ => believe_me ()))
      GMPmultiply
      (MkCommutativeFunction GMPmultiply (believe_me ()))
      GMPmultiplyMonoid
      (MkStrictMonoid GMPmultiplyMonoid (\_,_,_ => believe_me ()))
      (\x => MkMonomorphicFunction (GMPmultiply x) (\_,_,_ => believe_me ()))
      (\_ => believe_me ())
      (\_,_,_ => believe_me ())
      (\_,_,_,_ => believe_me ())
      GMPcompare

max_stars_repo_name: identicalsnowflake/neweden

max_issues_repo_name: identicalsnowflake/neweden

max_forks_repo_name: identicalsnowflake/neweden


text:
-- Module      : Itea.Javascript.Timer
-- Description :
-- Copyright   : (c) Simon Nielsen Knights 2018
-- License     : MIT
-- Maintainer  : simonank@mail.ru
-- Stability   : unstable
-- Portability : portable

module Itea.Javascript.Timer
import Itea.Utils

%default covering
%access public export

record Interval where
  constructor MkInterval
  unInterval : Ptr

record Timeout where
  constructor MkTimeout
  unTimeout : Ptr

||| Set an interval a command should be run on
|||
||| @fn command to run
||| @interval interval in milliseconds
setInterval : (fn : (() -> JS_IO ())) -> (interval : Int) -> JS_IO Interval
setInterval fn time =
  MkInterval <$> jscall "setInterval(%0,%1)"
                        (JsFn (() -> JS_IO ()) -> Int -> JS_IO Ptr)
                        (MkJsFn fn) time

||| Clear the interval; this stops future execution of the given command
clearInterval : Interval -> JS_IO ()
clearInterval = jscall "clearInterval(%0)" (Ptr  -> JS_IO ()) . unInterval

||| Run function after a specific time has passed
|||
||| @fn command to run
||| @timeout time to delay before running the command
setTimeout : (fn : (() -> JS_IO ())) -> (timeout : Int) -> JS_IO Timeout
setTimeout fn time =
  MkTimeout <$> jscall "setTimeout(%0,%1)"
                      (JsFn (() -> JS_IO ()) -> Int -> JS_IO Ptr)
                      (MkJsFn fn) time

||| Clear timeout; this stops further execution of the given command
clearTimeout : Timeout -> JS_IO ()
clearTimeout = jscall "clearTimeout(%0)" (Ptr  -> JS_IO ()) . unTimeout

max_stars_repo_name: simonank/idris-tea

max_issues_repo_name: simonank/idris-tea

max_forks_repo_name: simonank/idris-tea


text:
module Text.PrettyPrint.Bernardy

import Data.String
import Data.List
import Data.List1
import public Control.Monad.Reader
import public Control.Monad.Identity

%default total

public export
record LayoutOpts where
    constructor Opts
    lineLength : Int

export
record Layout where
    constructor MkLayout
    content : List1 String
    maxLine : Int
    lastLine : Int
    height : Int

export
record Doc (opts : LayoutOpts) where
    constructor MkDoc
    layouts : List Layout

replicateTR : Nat -> Char -> List Char -> String
replicateTR Z _ acc = pack acc
replicateTR (S k) c acc = replicateTR k c (c :: acc)

indentTR : Nat -> String -> String
indentTR k str = replicateTR k ' ' [] ++ str

namespace Layout
    ||| Render the given layout
    export
    render : Layout -> String
    render (MkLayout (l ::: ls) _ _ _) = unlines (l :: ls)

    ||| Convert a single line of text to a layout.
    |||
    ||| @ str this must be single line of text.
    export
    line : (str : String) -> Layout
    line str =
        let len = prim__strLength str
        in MkLayout
            { content = str ::: []
            , maxLine = len
            , lastLine = len
            , height = 0
            }

    allLines : (inp : List Char) -> (acc : List Char) -> List String
    allLines [] acc = [pack $ reverse acc]
    allLines ('\n' :: '\r' :: xs) acc = pack (reverse acc) :: allLines xs []
    allLines ('\n' :: xs) acc = pack (reverse acc) :: allLines xs []
    allLines ('\r' :: xs) acc = pack (reverse acc) :: allLines xs []
    allLines (x :: xs) acc = allLines xs (x :: acc)

    ||| Convert a string to a layout.
    ||| This preserves any manual formatting
    |||
    ||| @ str the String to pretty print
    export
    text : (str : String) -> Layout
    text str =
        let ls@(h :: t) = allLines (unpack str) []
            | [] => line ""
            (MkStats maxLine lastLine height) =
                foldl
                    (\(MkStats maxLine lastLine height), line =>
                        let len = prim__strLength line
                         in MkStats (max maxLine len) len (height + 1))
                    (MkStats 0 0 (-1))
                    ls
        in MkLayout
            { content = h ::: t
            , maxLine
            , lastLine
            , height
            }
    where
        data Stats : Type where
            MkStats : (maxLine, lastLine, height : Int) -> Stats

    concatContent' : String -> List String -> List1 String -> Nat -> List String
    concatContent' x [] (y ::: ys) k = (x ++ y) :: map (indentTR k) ys
    concatContent' x (x' :: xs) ys k = x :: concatContent' x' xs ys k

    concatContent : List1 String -> List1 String -> Nat -> List1 String
    concatContent (x ::: []) (y ::: ys) k = (x ++ y) ::: map (indentTR k) ys
    concatContent (x ::: (x' :: xs)) ys k = x ::: concatContent' x' xs ys k

    ||| Concatenate to Layouts horizontally
    export
    Semigroup Layout where
        left <+> right = MkLayout
            { content =
                concatContent
                    left.content
                    right.content
                    (cast left.lastLine)
            , maxLine = max left.maxLine $ left.lastLine + right.maxLine
            , lastLine = left.lastLine + right.lastLine
            , height = left.height + right.height
            }

    export
    Monoid Layout where
        neutral = MkLayout
            { content = "" ::: []
            , maxLine = 0
            , lastLine = 0
            , height = 0
            }

    export %inline
    FromString Layout where
        fromString = text

    export
    flush : Layout -> Layout
    flush x = MkLayout
        { content = addNL x.content.head x.content.tail
        , maxLine = x.maxLine
        , lastLine = 0
        , height = x.height + 1
        }
    where
        addNL : String -> List String -> List1 String
        addNL x [] = x ::: [""]
        addNL x (y :: xs) = x ::: forget (addNL y xs)

    export
    indent : Nat -> Layout -> Layout
    indent k x = fromString (replicateTR k ' ' []) <+> x

visible : LayoutOpts -> Layout -> Bool
visible opts x = x.maxLine <= opts.lineLength

shortest : List Layout -> Maybe Layout
shortest [] = Nothing
shortest (x :: xs) = Just $ foldl (\x, y => if x.height <= y.height then x else y) x xs

namespace Doc
    ||| Render the best candidate from the given set of layouts
    export
    render : (opts : _) -> Doc opts -> Maybe String
    render opts (MkDoc xs) = map render $ shortest $ filter (visible opts) xs

    insert : Layout -> List Layout -> List Layout -> List Layout
    insert x [] acc = x :: acc
    insert x (y :: ys) acc = case keep x y of
        KLeft => insert x ys acc
        KBoth => insert x ys (y :: acc)
        KRight => reverseOnto (y :: acc) ys
      where
        data Keep = KLeft | KBoth | KRight

        keep : Layout -> Layout -> Keep
        keep x y =
            if x.maxLine == y.maxLine && x.lastLine == y.maxLine && x.height == y.height
                then KBoth
            else if x.maxLine <= y.maxLine && x.lastLine <= y.maxLine && x.height <= y.height
                then KLeft
            else if x.maxLine >= y.maxLine && x.lastLine >= y.maxLine && x.height >= y.height
                then KRight
            else KBoth

    combine : List Layout -> List Layout -> List Layout
    combine [] ys = ys
    combine (x :: xs) ys = combine xs (insert x ys [])

    export %inline
    (<|>) : Doc opts -> Doc opts -> Doc opts
    MkDoc xs <|> MkDoc ys = MkDoc $ combine xs ys

    export %inline
    (<+>) : {opts : _} -> Doc opts -> Doc opts -> Doc opts
    MkDoc xs <+> MkDoc ys =
        MkDoc $ combine
            [ z
            | x <- xs
            , y <- ys
            , let z = x <+> y
            , visible opts z
            ]
            []

    export
    FromString (Doc opts) where
        fromString str = MkDoc [fromString str]

    export
    empty : Doc opts
    empty = MkDoc [neutral]

    export
    hcat : {opts : _} -> List (Doc opts) -> Doc opts
    hcat xs = foldl (<+>) empty xs

    export
    hsep : {opts : _} -> Doc opts -> Doc opts -> Doc opts
    hsep x y = hcat [x, " ", y]

    export
    flush : {opts : _} -> Doc opts -> Doc opts
    flush (MkDoc xs) = MkDoc $ map flush xs

    export
    vcat : {opts : _} -> Doc opts -> Doc opts -> Doc opts
    vcat x y = flush x <+> y

    export
    indent : {opts : _} -> Nat -> Doc opts -> Doc opts
    indent k (MkDoc xs) =
        MkDoc
            [ y
            | x <- xs
            , let y = indent k x
            , visible opts y
            ]

    export
    hang : {opts : _} -> Nat -> Doc opts -> Doc opts -> Doc opts
    hang k x y = (x <+> y) <|> vcat x (indent k y)

    export
    text : String -> (Doc opts)
    text str = MkDoc [text str]

    export
    sep : {opts : _} -> List (Doc opts) -> Doc opts
    sep [] = empty
    sep (x :: xs) = foldl1 hsep (x ::: xs) <|> foldl1 vcat (x ::: xs)

    infixl 7 <++>

    export
    (<++>) : {opts : _} -> Doc opts -> Doc opts -> Doc opts
    l <++> r = l <+> " " <+> r

public export
interface Pretty a where
    pretty : {opts : _} -> a -> Doc opts

public export
interface PrettyPrec prec a | a where
    prettyPrec : {opts : _} -> prec -> a -> Doc opts

max_stars_repo_name: Z-snails/prettier

max_issues_repo_name: Z-snails/prettier

max_forks_repo_name: Z-snails/prettier


text:
module Main

fred : (String, Int)
fred = ("Fred", 42)

main : IO ()
main = do
    putStrLn . show $ fred
    pure ()

max_stars_repo_name: thautwarm/idris-cam

max_issues_repo_name: thautwarm/idris-cam

max_forks_repo_name: thautwarm/idris-cam


text:
-- --------------------------------------------------------------- [ Utils.idr ]
-- Description : Utility parsing functions.
-- Copyright   : (c) Jan de Muijnck-Hughes
-- License     : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
module Config.Parse.Utils

import Lightyear
import Lightyear.Char
import Lightyear.Strings

%access export

-- ------------------------------------------------------------------- [ Stuff ]
-- These should be merged into Lightyear

word : Parser String
word = map pack (some $ alphaNum) <?> "Word"

ascii : Parser Char
ascii = do
  c <- satisfy (const True)
  case c of
    ','       => satisfy (const False)
    '{'       => satisfy (const False)
    '}'       => satisfy (const False)
    '['       => satisfy (const False)
    ']'       => satisfy (const False)
    otherwise => if ord c >= 33 && ord c <= 176
              then pure c
              else satisfy (const False)

asciiSeq : Parser String
asciiSeq = map pack (some ascii) <?> "Ascii String sans space and braces"

comment : String -> Parser ()
comment str = do
    string str
    manyTill anyChar endOfLine
    pure ()
   <?> unwords ["Comment with char", str]

-- ------------------------------------------------------------- [ Hex Numbers ]
-- Borrowed from Lightyear JSON Examples
hex : Parser Int
hex = do
  c <- map (ord . toUpper) $ satisfy isHexDigit
  pure $ if c >= ord '0' && c <= ord '9'
           then c - ord '0'
           else 10 + c - ord 'A'

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

--Borrowed from Lightyear JSON Examples.
specialChar : Parser Char
specialChar = do
  c <- satisfy (const True)
  case c of
    '"'  => pure '"'
    '\\' => pure '\\'
    '/'  => pure '/'
    'b'  => pure '\b'
    'f'  => pure '\f'
    'n'  => pure '\n'
    'r'  => pure '\r'
    't'  => pure '\t'
    'u'  => map chr hexQuad
    _    => satisfy (const False) <?> "expected special char"

-- ------------------------------------------------------ [ Scientific Numbers ]
-- Borrowed from Lightyear JSON Examples
-- inspired by Haskell's Data.Scientific module

public export
record Scientific where
  constructor MkScientific
  coefficient : Integer
  exponent : Integer

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

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

max_stars_repo_name: jfdm/idris-config

max_issues_repo_name: jfdm/idris-config

max_forks_repo_name: jfdm/idris-config


text:
module Common.ECDSA

import Common

-- An unverified message
-- This is temporary API
export
data TaintedMessage = MkTaintedMessage Felt

export
tainted : Felt -> TaintedMessage
tainted = MkTaintedMessage

-- Returns the verified message
-- This function is not safe: If the returned value is ignored, Idris is free to eliminate the call to this function altogether.
export %inline
%foreign
    "imports:starkware.cairo.common.cairo_builtins SignatureBuiltin, starkware.cairo.common.signature verify_ecdsa_signature"
    "linear_implicits:ecdsa_ptr"
    """
    code:
    func Common_ECDSA_verifySignature(ecdsa_ptr, message, public_key, signature_r, signature_s) -> (message, ecdsa_ptr):
       let ecdsa_ptr_ = cast(ecdsa_ptr, SignatureBuiltin*)
       verify_ecdsa_signature{ecdsa_ptr=ecdsa_ptr_}(message, public_key, signature_r, signature_s)
       return (message, cast(ecdsa_ptr_, felt))
    end
    """
verifySignature : (message: TaintedMessage) -> (public_key: Felt) -> (signature_r: Felt) -> (signature_s: Felt) -> Felt

max_stars_repo_name: skyro-compiler/skyro

max_issues_repo_name: skyro-compiler/skyro

max_forks_repo_name: skyro-compiler/skyro


text:
module RingProperties

import Ring
import Monoid
import Group
import Group_property

%access public export

|||Auxiliary function that provzs that if a+a=a thzn a=0
aplusaZ: (r: Type) -> (pfr: Ring r) -> (a: r) -> ((Ring_Add r pfr a a) =a) -> (a = (DPair.fst(RingAdditive_id r pfr)))
aplusaZ r (MkRing r (+) (*) pfr) a prf = (Group_property_4 r (+) (Basics.fst (Basics.fst pfr)) a a z (trans prf (sym (Basics.fst (pfz a))) )) where
  z: r
  z = (DPair.fst(RingAdditive_id r (MkRing r (+) (*) pfr)))
  pfz: (a: r) -> (a+z=a, z+a=a)
  pfz = DPair.snd (RingAdditive_id r (MkRing r (+) (*) pfr))

|||Proof that 0*a = 0
Zmultleft: (r: Type) -> (pfr: Ring r) -> (a: r) -> ((Ring_Mult r pfr (DPair.fst(RingAdditive_id r pfr)) a) = (DPair.fst(RingAdditive_id r pfr)))
Zmultleft r (MkRing r (+) (*) pfr) a = (aplusaZ r (MkRing r (+) (*) pfr) (z*a) (
    trans (sym (pfd a z z)) (cong {f= \p => p*a} (pfz z))
  ) ) where
  z: r
  z = (DPair.fst(RingAdditive_id r (MkRing r (+) (*) pfr)))
  pfz: (a: r) -> (a+z=a)
  pfz a = Basics.fst ((DPair.snd (RingAdditive_id r (MkRing r (+) (*) pfr))) a)
  pfd: (a: r) -> (b: r) -> (c: r) -> ((b+c)*a = (b*a) + (c*a))
  pfd a b c = Basics.snd ((Basics.snd (Basics.snd pfr)) a b c)

|||Proof that a*0 = 0
Zmultright: (r: Type) -> (pfr: Ring r) -> (a: r) -> ((Ring_Mult r pfr a (DPair.fst(RingAdditive_id r pfr))) = (DPair.fst(RingAdditive_id r pfr)))
Zmultright r (MkRing r (+) (*) pfr) a = (aplusaZ r (MkRing r (+) (*) pfr) (a*z) (
    trans (sym (pfd a z z)) (cong {f= \p => a*p} (pfz z))
    ) ) where
    z: r
    z = (DPair.fst(RingAdditive_id r (MkRing r (+) (*) pfr)))
    pfz: (a: r) -> (a+z=a)
    pfz a = Basics.fst ((DPair.snd (RingAdditive_id r (MkRing r (+) (*) pfr))) a)
    pfd: (a: r) -> (b: r) -> (c: r) -> (a*(b+c) = (a*b) + (a*c))
    pfd a b c = Basics.fst ((Basics.snd (Basics.snd pfr)) a b c)


text:
module Network.TLS.Signature

import Data.List
import Data.Vect
import Utils.Misc
import Utils.Bytes
import Utils.Parser
import Network.TLS.Parse.PEM
import Network.TLS.Parse.DER
import Network.TLS.Parsing
import Data.String.Parser
import Crypto.RSA
import Crypto.Curve
import Crypto.Curve.Weierstrass
import Crypto.Hash
import Crypto.Hash.OID

public export
data PublicKey : Type where
  RsaPublicKey : RSAPublicKey -> PublicKey
  EcdsaPublicKey : Point p => p -> PublicKey

public export
data SignatureParameter : Type where
  RSA_PKCSv15 : (DPair Type RegisteredHash) -> SignatureParameter
  RSA_PSS : (wit : DPair Type Hash) -> (salt_len : Nat) -> MaskGenerationFunction -> SignatureParameter
  ECDSA : DPair Type Hash -> SignatureParameter

export
Show PublicKey where
  show (RsaPublicKey _) = "RSA Public Key"
  show (EcdsaPublicKey _) = "ECDSA Public Key"

export
verify_signature : SignatureParameter -> PublicKey -> List Bits8 -> List Bits8 -> Either String ()
verify_signature (RSA_PKCSv15 hash_wit) (RsaPublicKey public_key) message signature =
  if rsassa_pkcs1_v15_verify @{hash_wit.snd} public_key message signature then pure () else Left "signature does not match message"
verify_signature (RSA_PSS hash_wit salt_len mgf) (RsaPublicKey public_key) message signature =
  if rsassa_pss_verify' @{hash_wit.snd} mgf salt_len public_key message signature then pure () else Left "signature does not match message"
verify_signature (ECDSA hash_wit) (EcdsaPublicKey public_key) message signature = do
  let (Pure [] ok) = feed (map (uncurry MkPosed) $ enumerate Z signature) parse_asn1
  | (Pure leftover _) => Left "parser overfed for ecdsa signature"
  | (Fail err) => Left $ "parser error for ecdsa signature: " <+> show err
  | _ => Left "parser underfed for ecdsa signature"
  let (Universal ** 16 ** Sequence [ (Universal ** 2 ** IntVal x), (Universal ** 2 ** IntVal y) ] ) = ok
  | _ => Left "malformed ecdsa signature"
  let digest = hash @{hash_wit.snd} hash_wit.fst message
  if ecdsa_verify (be_to_integer digest) (MkSignature public_key (x, y)) then pure () else Left "signature does not match message"

verify_signature _ _ message signature = Left "public key does not match signature scheme"

export
verify_signature' : SignatureParameter -> PublicKey -> List Bits8 -> BitArray -> Either String ()
verify_signature' param public_key message (MkBitArray 0 signature) = verify_signature param public_key message signature
verify_signature' param public_key message (MkBitArray n signature) = Left $ "invalid padding: " <+> show n

export
extract_algorithm : ASN1Token -> Maybe (List Nat, Maybe ASN1Token)
extract_algorithm (Universal ** 16 ** Sequence [(Universal ** 6 ** OID algorithm)]) = Just (algorithm, Nothing)
extract_algorithm (Universal ** 16 ** Sequence ((Universal ** 6 ** OID algorithm) :: parameter :: [])) = Just (algorithm, Just parameter)
extract_algorithm _ = Nothing

export
oid_to_hash_algorithm : List Nat -> Maybe (DPair Type Hash)
oid_to_hash_algorithm oid =
  case map natToInteger oid of
    [ 1, 3, 14, 3, 2, 26 ] => Just (MkDPair Sha1 %search)
    [ 2, 16, 840, 1, 101, 3, 4, 2, 1 ] => Just (MkDPair Sha256 %search)
    [ 2, 16, 840, 1, 101, 3, 4, 2, 2 ] => Just (MkDPair Sha384 %search)
    [ 2, 16, 840, 1, 101, 3, 4, 2, 3 ] => Just (MkDPair Sha512 %search)
    _ => Nothing

export
extract_signature_parameter : List Nat -> Maybe ASN1Token -> Either String SignatureParameter
extract_signature_parameter oid parameter = do
  case (map natToInteger oid, parameter) of
    ([1, 2, 840, 113549, 1, 1, 5], Just (Universal ** 5 ** Null)) =>  Right (RSA_PKCSv15 $ MkDPair Sha1 %search)
    ([1, 2, 840, 113549, 1, 1, 11], Just (Universal ** 5 ** Null)) => Right (RSA_PKCSv15 $ MkDPair Sha256 %search)
    ([1, 2, 840, 113549, 1, 1, 12], Just (Universal ** 5 ** Null)) => Right (RSA_PKCSv15 $ MkDPair Sha384 %search)
    ([1, 2, 840, 113549, 1, 1, 13], Just (Universal ** 5 ** Null)) => Right (RSA_PKCSv15 $ MkDPair Sha512 %search)
    ([1, 2, 840, 10045, 4, 3, 2], Nothing) => Right (ECDSA $ MkDPair Sha256 %search)
    ([1, 2, 840, 10045, 4, 3, 3], Nothing) => Right (ECDSA $ MkDPair Sha384 %search)
    ([1, 2, 840, 10045, 4, 3, 4], Nothing) => Right (ECDSA $ MkDPair Sha512 %search)
    ([1, 2, 840, 113549, 1, 1, 10], Just (Universal ** 16 ** Sequence params)) => do
      (wit, params) <- extract_hash_algo params
      (mgf, params) <- extract_mgf params
      (salt, params) <- extract_salt_len params
      extract_trailer params
      pure $ RSA_PSS wit salt mgf
    _ => Left "unrecognized signature parameter"
  where
    extract_hash_algo' : ASN1Token -> Either String (DPair Type Hash)
    extract_hash_algo' (Universal ** 16 ** Sequence ((Universal ** 6 ** OID oid) :: _)) =
      maybe_to_either (oid_to_hash_algorithm oid) "hash algorithm not recognized"
    extract_hash_algo' _ = Left "malformed hash algorithm"

    extract_hash_algo : List ASN1Token -> Either String (DPair Type Hash, List ASN1Token)
    extract_hash_algo [] = Right (MkDPair Sha1 %search, [])
    extract_hash_algo ((ContextSpecific ** 0 ** UnknownConstructed _ _ [ hash_algo ] ) :: xs) =
      (, xs) <$> extract_hash_algo' hash_algo
    extract_hash_algo (x :: xs) = Right (MkDPair Sha1 %search, x :: xs)

    extract_mgf : List ASN1Token -> Either String (MaskGenerationFunction, List ASN1Token)
    extract_mgf [] = Right (mgf1 {algo=Sha1}, [])
    extract_mgf ((ContextSpecific ** 1 ** UnknownConstructed _ _ [ sequence ]) :: xs) =
      case sequence of
        ((Universal ** 16 ** Sequence ((Universal ** 6 ** OID oid) :: param :: []))) =>
          case map natToInteger oid of
            [ 1, 2, 840, 113549, 1, 1, 8 ] => (\wit => (mgf1 @{wit.snd}, xs)) <$> extract_hash_algo' param
            _ => Left "mask generation function not recognized"
        _ => Left "malformed mask generation function"
    extract_mgf (x :: xs) = Right (mgf1 {algo=Sha1}, x :: xs)

    extract_salt_len : List ASN1Token -> Either String (Nat, List ASN1Token)
    extract_salt_len [] = Right (20, [])
    extract_salt_len ((ContextSpecific ** 2 ** UnknownConstructed _ _ [ (Universal ** 2 ** IntVal salt_len) ]) :: xs) =
      if salt_len < 0 then Left "negative salt len" else pure (integerToNat salt_len, xs)
    extract_salt_len (x :: xs) = Right (20, x :: xs)

    extract_trailer : List ASN1Token -> Either String ()
    extract_trailer [] = Right ()
    extract_trailer [ (ContextSpecific ** 3 ** UnknownConstructed _ _ [ (Universal ** 2 ** IntVal trailer ) ]) ] =
      if trailer /= 1 then Left "invalid trailer field" else pure ()
    extract_trailer (x :: xs) = Left "unrecognized field after trailer field"

extract_rsa_key : List Bits8 -> Either String RSAPublicKey
extract_rsa_key pk_content = do
  let (Pure [] ok) = feed (map (uncurry MkPosed) $ enumerate Z pk_content) parse_asn1
  | (Pure leftover _) => Left "parser overfed for SubjectPublicKey"
  | (Fail err) => Left $ "parser error for SubjectPublicKey: " <+> show err
  | _ => Left "parser underfed for SubjectPublicKey"
  let (Universal ** 16 ** Sequence
        [ (Universal ** 2 ** IntVal modulus)
        , (Universal ** 2 ** IntVal public_exponent)
        ]
      ) = ok
  | _ => Left "cannot parse SubjectPublicKey"

  maybe_to_either (mk_rsa_publickey modulus public_exponent) "malformed RSA public key"

extract_ecdsa_key : List Bits8 -> List Integer -> Either String PublicKey
extract_ecdsa_key content [1, 2, 840, 10045, 3, 1, 7] =
  EcdsaPublicKey <$> maybe_to_either (decode {p=P256} content) "fail to parse secp256r1 public key"
extract_ecdsa_key content [1, 3, 132, 0, 34] =
  EcdsaPublicKey <$> maybe_to_either (decode {p=P384} content) "fail to parse secp384r1 public key"
extract_ecdsa_key content [1, 3, 132, 0, 35] =
  EcdsaPublicKey <$> maybe_to_either (decode {p=P521} content) "fail to parse secp521r1 public key"
extract_ecdsa_key _ oid = Left $ "unrecognized elliptic curve group oid: " <+> show oid

export
extract_key' : ASN1Token -> Either String (Vect 20 Bits8, PublicKey)
extract_key' ok = do
  let (Universal ** 16 ** Sequence
        [ algorithm
        , (Universal ** 3 ** Bitstring bitstring)
        ]
      ) = ok
  | _ => Left "cannot parse SubjectPublicKeyInfo"

  let (MkBitArray 0 content) = bitstring
  | _ => Left "incorrect padding for SubjectPublicKey"

  key_info <- maybe_to_either (extract_algorithm algorithm) "cannot parse algorithm in SubjectPublicKeyInfo"

  -- natToInteger is needed because pattern matching list of Nat will kill my cpu big time
  public_key <- case mapFst (map natToInteger) key_info of
    -- PKCS #1 RSA Encryption
    ([1, 2, 840, 113549, 1, 1, 1], Just (Universal ** 5 ** Null)) =>
      RsaPublicKey <$> extract_rsa_key content
    -- RSA PSS
    ([1, 2, 840, 113549, 1, 1, 10], Nothing) =>
      RsaPublicKey <$> extract_rsa_key content
    -- Elliptic Curve Public Key (RFC 5480)
    ([1, 2, 840, 10045, 2, 1], Just (Universal ** 6 ** OID group_id)) =>
      extract_ecdsa_key content $ map natToInteger group_id
    _ => Left "unrecognized signature algorithm parameter"

  pure (hash Sha1 content, public_key)

export
extract_key : List Bits8 -> Either String (Vect 20 Bits8, PublicKey)
extract_key der_public_key = do
  let (Pure [] ok) = feed (map (uncurry MkPosed) $ enumerate Z der_public_key) parse_asn1
  | (Pure leftover _) => Left "parser overfed for SubjectPublicKeyInfo"
  | (Fail err) => Left $ "parser error for SubjectPublicKeyInfo: " <+> show err
  | _ => Left "parser underfed for SubjectPublicKeyInfo"
  extract_key' ok


text:
data EqNat : Nat -> Nat -> Type where
     Same : (x : Nat) -> EqNat x x

total
sameS : (k : Nat) -> (j : Nat) -> (eq : EqNat k j) -> EqNat (S k) (S j)
sameS k k (Same k) = Same (S k)

checkEqNat : (num1 : Nat) -> (num2 : Nat) -> Maybe (EqNat num1 num2)
checkEqNat Z Z = Just (Same Z)
checkEqNat Z (S k) = Nothing
checkEqNat (S k) Z = Nothing
checkEqNat (S k) (S j) = case checkEqNat k j of
                              Nothing => Nothing
                              Just eq => Just (sameS _ _ eq)

max_stars_repo_name: wdomitrz/Coq-Exercises

max_issues_repo_name: wdomitrz/Coq-Exercises

max_forks_repo_name: wdomitrz/Coq-Exercises


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

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

module Main

import BareMetal.Utils as Bare
import BareMetal.SocAM335x
import StwfFFI.GPIO

gpioInstanceAddress : Bits32
gpioInstanceAddress = socGpio1Regs

gpioInstancePinNumber : Int
gpioInstancePinNumber = 23

setupGpio : IO ()
setupGpio = do
    -- Enabling functional clocks for GPIO1 instance
    gpio1ModuleClkConfig

    -- Selecting GPIO1[23] pin for use
    gpio1Pin23PinMuxSetup

    -- Enabling the GPIO module
    gpioModuleEnable gpioInstanceAddress

    -- Resetting the GPIO module
    gpioModuleReset gpioInstanceAddress

    -- Setting the GPIO pin as an output pin
    gpioDirModeSet
        gpioInstanceAddress
        gpioInstancePinNumber
        0

onOffTime : Int
onOffTime = 50000000

blinkLed : IO ()
blinkLed = do
    -- Driving a logic HIGH on the GPIO pin
    gpioPinWrite
        gpioInstanceAddress
        gpioInstancePinNumber
        True

    Bare.busyWait onOffTime

    -- Driving a logic LOW on the GPIO pin
    gpioPinWrite
        gpioInstanceAddress
        gpioInstancePinNumber
        False

    Bare.busyWait onOffTime

    -- Repeat blink
    blinkLed

main : IO ()
main = do
    setupGpio
    blinkLed

max_stars_repo_name: mokshasoft/bare-metal-idris-apps

max_issues_repo_name: mokshasoft/bare-metal-idris-apps

max_forks_repo_name: mokshasoft/bare-metal-idris-apps


text:
data Divisibleby3 : Nat -> Type where
  Three: Divisibleby3 3
  ThreeMultiple: Divisibleby3 x -> Divisibleby3 (3+x)

divBy9: Divisibleby3 9
divBy9 = ThreeMultiple (ThreeMultiple Three)

data DivisiblebyX : Nat -> Nat -> Type where
  Base:DivisiblebyX x x
  Multiple: DivisiblebyX x y -> DivisiblebyX x (x+y)

divBy5_15: DivisiblebyX 5 15
divBy5_15 = Multiple (Multiple Base)

divBy3_15: DivisiblebyX 3 15
divBy3_15 = Multiple (Multiple (Multiple (Multiple Base)))

data FizzBuzzProofSimple: Nat -> Type where
  Fizz: DivisiblebyX 3 x -> FizzBuzzProofSimple x
  Buzz: DivisiblebyX 5 x -> FizzBuzzProofSimple x
  FizzBuzz: DivisiblebyX 3 x -> DivisiblebyX 5 x -> FizzBuzzProofSimple x
  Normal: (x: Nat) -> FizzBuzzProofSimple x

Show (FizzBuzzProofSimple x) where
  show (Fizz _) = "fizz"
  show (Buzz _) = "buzz"
  show (FizzBuzz _ _) = "fizzbuzz"
  show (Normal x) = show x

proof5: FizzBuzzProofSimple 5
proof5 = Buzz Base

proof3: FizzBuzzProofSimple 3
proof3 = Fizz Base

proof7: FizzBuzzProofSimple 7
proof7 = Normal 7

proof15: FizzBuzzProofSimple 15
proof15 = FizzBuzz (Multiple (Multiple (Multiple (Multiple Base)))) (Multiple (Multiple Base))

divisibleby3: (y: Nat) -> Maybe (DivisiblebyX 3 y)
divisibleby3  (S (S (S Z))) = Just Base
divisibleby3 (S (S (S x))) = case divisibleby3 x of
  Nothing => Nothing
  Just y => Just (Multiple y)
divisibleby3 _ = Nothing

divisibleby5: (y: Nat) -> Maybe (DivisiblebyX 5 y)
divisibleby5 (S (S (S (S (S Z))))) = Just(Base)
divisibleby5 (S (S (S (S (S x))))) = case divisibleby5 x of
  Nothing => Nothing
  Just y => Just (Multiple y)
divisibleby5 _ = Nothing

fizzbuzz: (x: Nat) -> FizzBuzzProofSimple x
fizzbuzz x = case (divisibleby3 x, divisibleby5 x) of
  (Nothing, Nothing) => Normal x
  (Just fizz_prf, Just buzz_prf) => FizzBuzz fizz_prf buzz_prf
  (Nothing, Just buzz_prf) => Buzz buzz_prf
  (Just fizz_prf, Nothing) => Fizz fizz_prf

wrongfizzbuzz: (x: Nat) -> FizzBuzzProofSimple x
wrongfizzbuzz x = case (divisibleby3 x, divisibleby5 x) of
  (Nothing, Nothing) => Normal x
  (_, Just buzz_prf) => Buzz buzz_prf
  (Just fizz_prf, _) => Fizz fizz_prf


text:
module Compo3

import Incrementer
import Twicer
import Halfer

%default total

-- Realized (halfer . incrementer . twicer).  If halfer can only take
-- an even interger, then such composition is not valid.
rlz_compo3_attrs : RealizedAttributes
rlz_compo3_attrs = MkRealizedAttributes (MkCosts 600 60 6) 0.8
rlz_compo3 : RealizedFunction (Int -> Int) Compo3.rlz_compo3_attrs
rlz_compo3 = (compose rlz_halfer (compose rlz_incrementer rlz_twicer))

max_stars_repo_name: nunet-io/ai-dsl

max_issues_repo_name: nunet-io/ai-dsl

max_forks_repo_name: nunet-io/ai-dsl


text:
module Examples.Main

import Examples.AOC1
import Examples.AOC2
import Examples.AOC3

main : IO ()
main =  AOC1.part1 >> AOC1.part2
     >> AOC2.part1 >> AOC2.part2
     >> AOC3.part1 >> AOC3.part2


text:
module Data.Bytes.Lazy.API

import Data.Bytes.Lazy.Internal
import Data.Bytes.Strict -- We want Internal and API for now

import Data.Word.Word8

private
moduleName : String
moduleName = "Data.Bytes.Lazy.API"

empty : LBytes
empty = Empty

%inline -- pretty safe inline here
singleton : Word8 -> LBytes
singleton w = Chunk (singleton w) Empty

pack : List Word8 -> Bytes
unpack : Word8 -> List Word8

fromChunks : List Bytes -> LBytes

-- I probably want Lazy Lists here
toChunks : LBytes -> List Bytes

fromStrict : Bytes -> LBytes
fromStrict b = chunk' b Empty

-- expensive, who knows how big this LBytes is!
toStrict : LBytes -> Bytes
toStrict lb = ?saddfs
  where
    goLen0 : LBytes -> Bytes
    goLen1 : LBytes -> Bytes
    goLen  : LBytes -> Bytes
    goCopy : LBytes -> Bytes


text:
-- -------------------------------------------------------------- [ Common.idr ]
-- Module    : Common.idr
-- Copyright : (c) Jan de Muijnck-Hughes
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
||| Sif Specific Parsing Utils
module Sif.DSL.Parser.Common

import Lightyear
import Lightyear.Char
import Lightyear.Strings

import Sif.DSL.Parser.Utils

import Test.Parsing

%access export

literal : Parser String
literal = do
    token "\"\"\""
    ss <- manyTill anyChar (token "\"\"\"")
    pure (pack ss)

sifComment : Parser ()
sifComment = comment "--" "{-" "-}" <?> "Sif Comment"

sifDoc : Parser String
sifDoc = doc ">"
    <?> "Sif Doc String"

descString : Parser String
descString = literal
         <|> (quoted '"')
         <?> "Description Block"

keyword : String -> Parser ()
keyword s = do
     string s
     sifComment
     pure ()

desc : Parser $ String
desc = do
     token "Description"
     s <- descString
     spaces
     pure s
    <?> "Description"

ident : Parser String
ident = do
    i <- (map pack $ some alphaNum)
    spaces
    pure i
  <?> "Identity"

title : Parser String
title = do
   t <- (quoted '"')
   spaces
   pure t
  <?> "Title"

runTests : IO ()
runTests = do
  putStrLn $ heading "Parsing Common Tests"
  canParse (Just "Literal")     literal      "\"\"\" I am a literal\"\"\""
  canParse (Just "Desc String") descString   "\"\"\" I am a literal\"\"\""
  canParse (Just "Desc String") descString   "\"aaaaaa\""
  canParse (Just "Comments")    (sifComment) """-- I am a comment\n"""
  canParse (Just "Comments")    (sifComment) """{- I am a comment -}"""
  canParse (Just "Doc Stringd") sifDoc       "> I am a doc\n"

  parseTestG (Just "Desc")      (desc) "Description \"I am\"" "I am" (==)

  parseTestG (Just "Titles")
             title
             "\"I am a title\""
             "I am a title"
             (==)
  parseTestG (Just "Identifier")
             ident
             "ident"
             "ident"
             (==)

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

max_stars_repo_name: jfdm/sif-lang

max_issues_repo_name: jfdm/sif-lang

max_forks_repo_name: jfdm/sif-lang


text:
||| This module provides a simple common subexpression elimination (CSE)
||| algorithm. The main goal right now is to move duplicate
||| expressions introduced during autosearch (which includes
||| interface resolution) to the top level.
|||
||| As such, the functionality provided by this module should
||| be considered a form of whole program optimization.
||| To keep things simple, it operates only on closed terms right
||| now, which are - in case of several occurences - introduced
||| as new zero-argument toplevel functions.
|||
||| The procedure is very simple: In an analysis step, we
||| iterate over all toplevel definitions once, trying to
||| convert every subexpression to a closed one (no free
||| variables). Closed terms are then stored in a `SortedMap`
||| together with their size and count. In order to only use
||| linear space w.r.t. term size, we start this analysis at the
||| leaves and substitute closed terms with the machine generated
||| names before analyzing parent terms.
|||
||| In a second step, we compare the count of each machine
||| generated name with the count of its parent expression.
||| If they are the same, the name is dropped and replaces with
||| a CSE optimized version of the original expression, otherwise
||| the name is kept and a new zero argumet function of the
||| given name is added to the toplevel, thus eliminating the
||| duplicate expressions.
module Compiler.Opts.CSE

import Core.CompileExpr
import Core.Context
import Core.Context.Log
import Core.Name
import Core.TT

import Core.Ord
import Data.List
import Data.String
import Data.Vect
import Libraries.Data.SortedMap

||| Maping from a pairing of closed terms together with
||| their size (for efficiency) to the number of
||| occurences in toplevel definitions.
public export
UsageMap : Type
UsageMap = SortedMap (Integer, CExp []) (Name, Integer)

||| Number of appearances of a closed expression.
|||
|||  `Once` : The expression occurs exactly once.
|||  `Many` : The expression occurs more than once.
|||  `C n`  : The expression has been counted `n` times
|||           but we will have to compare this value
|||           with the number of occurences of its parent
|||           expression to decide whether it occured
|||           only once or several times.
|||
public export
data Count = Once | Many | C Integer

Show Count where
  show Once  = "Once"
  show Many  = "Many"
  show (C n) = "C " ++ show n

||| After common subexpression analysis we get a mapping
||| from `Name`s to the closed expressions they replace.
||| We use this mapping for substituting the names back
||| to the corresponding expressions, if and only if
||| the expression appears only in one place.
public export
ReplaceMap : Type
ReplaceMap = SortedMap Name (CExp [], Count)

toReplaceMap : UsageMap -> ReplaceMap
toReplaceMap = SortedMap.fromList
             . map (\((_,exp),(n,c)) => (n, (exp, C c)))
             . SortedMap.toList

--------------------------------------------------------------------------------
--          State
--------------------------------------------------------------------------------

data Sts : Type where

record St where
  constructor MkSt
  map : UsageMap
  idx : Int

-- Adds a new closed expression to the `UsageMap`
-- returning a new machine generated name to be used
-- if the expression should be lifted to the toplevel.
-- Very small expressions are being ignored.
store : Ref Sts St => Integer -> CExp [] -> Core (Maybe Name)
store sz exp =
  if sz < 5
     then pure Nothing
     else do
       (MkSt map idx)    <- get Sts

       (name,count,idx2) <-
         case lookup (sz,exp) map of
           Just (nm,cnt) => pure (nm, cnt+1, idx)
           Nothing       => pure (MN "csegen" idx, 1, idx + 1)

       put Sts $ MkSt (insert (sz,exp) (name, count) map) idx2
       pure (Just name)

--------------------------------------------------------------------------------
--          Strengthening of Expressions
--------------------------------------------------------------------------------

dropVar :  (pre : List Name)
        -> (n : Nat)
        -> (0 p : IsVar x n (pre ++ ns))
        -> Maybe (IsVar x n pre)
dropVar [] _ _        = Nothing
dropVar (y :: xs) 0 First = Just First
dropVar (y :: xs) (S k) (Later p) =
  case dropVar xs k p of
    Just p' => Just $ Later p'
    Nothing => Nothing

mutual
  -- tries to 'strengthen' an expression by removing
  -- a prefix of bound variables. typically, this is invoked
  -- with `{pre = []}`.
  dropEnv : {pre : List Name} -> CExp (pre ++ ns) -> Maybe (CExp pre)
  dropEnv (CLocal {idx} fc p) = (\q => CLocal fc q) <$> dropVar pre idx p
  dropEnv (CRef fc x) = Just (CRef fc x)
  dropEnv (CLam fc x y) = CLam fc x <$> dropEnv y
  dropEnv (CLet fc x inlineOK y z) =
    CLet fc x inlineOK <$> dropEnv y <*> dropEnv z
  dropEnv (CApp fc x xs) = CApp fc <$> dropEnv x <*> traverse dropEnv xs
  dropEnv (CCon fc x y tag xs) = CCon fc x y tag <$> traverse dropEnv xs
  dropEnv (COp fc x xs) = COp fc x <$> traverse dropEnv xs
  dropEnv (CExtPrim fc p xs) = CExtPrim fc p <$> traverse dropEnv xs
  dropEnv (CForce fc x y) = CForce fc x <$> dropEnv y
  dropEnv (CDelay fc x y) = CDelay fc x <$> dropEnv y
  dropEnv (CConCase fc sc xs x) =
    CConCase fc            <$>
    dropEnv sc             <*>
    traverse dropConAlt xs <*>
    traverse dropEnv x

  dropEnv (CConstCase fc sc xs x) =
    CConstCase fc            <$>
    dropEnv sc               <*>
    traverse dropConstAlt xs <*>
    traverse dropEnv x

  dropEnv (CPrimVal fc x) = Just $ CPrimVal fc x
  dropEnv (CErased fc) = Just $ CErased fc
  dropEnv (CCrash fc x) = Just $ CCrash fc x

  dropConAlt :  {pre : List Name}
             -> CConAlt (pre ++ ns)
             -> Maybe (CConAlt pre)
  dropConAlt (MkConAlt x y tag args z) =
    MkConAlt x y tag args . embed <$> dropEnv z

  dropConstAlt :  {pre : List Name}
               -> CConstAlt (pre ++ ns)
               -> Maybe (CConstAlt pre)
  dropConstAlt (MkConstAlt x y) = MkConstAlt x <$> dropEnv y

--------------------------------------------------------------------------------
--          Analysis
--------------------------------------------------------------------------------

mutual
  -- Tries to convert an expression and its
  -- sub-expression to closed terms (`CExp []`).
  -- Every occurence of a closed term will be replaced by
  -- a machine generated name and its count in the `UsageMap`
  -- will be increased by one.
  --
  -- Because we start at the leafs and substitute all closed
  -- expressions with machine generated names, we have to
  -- keep track of the original expression's size, which
  -- is returned in addition to the adjusted expressions.
  export
  analyze : Ref Sts St => CExp ns -> Core (Integer, CExp ns)

  -- We ignore prim ops here, since moving them to the toplevel
  -- might interfere with other optimizations, for instance
  -- the one dealing with #1320.
  -- Some other terms are ignored, as I (@stefan-hoeck)
  -- am being conservative here,
  -- not daring to inadvertently change the semantics
  -- of the program.
  analyze c@(COp _ _ _)      = analyzeSubExp c
  analyze c@(CExtPrim _ _ _) = analyzeSubExp c
  analyze c@(CForce _ _ _)   = analyzeSubExp c
  analyze c@(CDelay _ _ _)   = analyzeSubExp c

  analyze exp = do
    (sze, exp') <- analyzeSubExp exp
    case dropEnv {pre = []} exp' of
      Just e0 => do
        Just nm <- store sze e0
          | Nothing => pure (sze, exp')
        pure (sze, CRef EmptyFC nm)
      Nothing => pure (sze, exp')

  analyzeList : Ref Sts St => List (CExp ns) -> Core (Integer, List (CExp ns))
  analyzeList es = do
    (sizes, exps) <- unzip <$> traverse analyze es
    pure (sum sizes, exps)

  analyzeMaybe : Ref Sts St => Maybe (CExp ns) -> Core (Integer, Maybe (CExp ns))
  analyzeMaybe Nothing  = pure (0, Nothing)
  analyzeMaybe (Just e) = do
    (se,e') <- analyze e
    pure (se, Just e')

  analyzeVect : Ref Sts St => Vect n (CExp ns) -> Core (Integer, Vect n (CExp ns))
  analyzeVect es = do
    (sizes, exps) <- unzip <$> traverseVect analyze es
    pure (sum sizes, exps)

  analyzeSubExp : Ref Sts St => CExp ns -> Core (Integer, CExp ns)
  analyzeSubExp e@(CLocal _ _)         = pure (1, e)
  analyzeSubExp e@(CRef _ _)           = pure (1, e)
  analyzeSubExp (CLam f n y)  = do
    (sy, y') <- analyze y
    pure (sy + 1, CLam f n y')

  analyzeSubExp (CLet f n i y z) = do
    (sy, y') <- analyze y
    (sz, z') <- analyze z
    pure (sy + sz + 1, CLet f n i y' z')

  analyzeSubExp (CApp fc x xs) = do
    (sx, x')   <- analyze x
    (sxs, xs') <- analyzeList xs
    pure (sx + sxs + 1, CApp fc x' xs')

  analyzeSubExp (CCon f n c t xs) = do
    (sxs, xs') <- analyzeList xs
    pure (sxs + 1, CCon f n c t xs')

  analyzeSubExp (COp f n xs) = do
    (sxs, xs') <- analyzeVect xs
    pure (sxs + 1, COp f n xs')

  analyzeSubExp (CExtPrim f n xs) = do
    (sxs, xs') <- analyzeList xs
    pure (sxs + 1, CExtPrim f n xs')

  analyzeSubExp (CForce f r y) = do
    (sy, y') <- analyze y
    pure (sy + 1, CForce f r y')

  analyzeSubExp (CDelay f r y) = do
    (sy, y') <- analyze y
    pure (sy + 1, CDelay f r y')

  analyzeSubExp (CConCase f sc xs x) = do
    (ssc, sc') <- analyze sc
    (sxs, xs') <- unzip <$> traverse analyzeConAlt xs
    (sx, x')   <- analyzeMaybe x
    pure (ssc + sum sxs + sx + 1, CConCase f sc' xs' x')

  analyzeSubExp (CConstCase f sc xs x) = do
    (ssc, sc') <- analyze sc
    (sxs, xs') <- unzip <$> traverse analyzeConstAlt xs
    (sx, x')   <- analyzeMaybe x
    pure (ssc + sum sxs + sx + 1, CConstCase f sc' xs' x')

  analyzeSubExp c@(CPrimVal _ _) = pure (1, c)
  analyzeSubExp c@(CErased _)    = pure (1, c)
  analyzeSubExp c@(CCrash _ _)   = pure (1, c)

  analyzeConAlt :  { auto c : Ref Sts St }
                -> CConAlt ns
                -> Core (Integer, CConAlt ns)
  analyzeConAlt (MkConAlt n c t as z) = do
    (sz, z') <- analyze z
    pure (sz + 1, MkConAlt n c t as z')

  analyzeConstAlt : Ref Sts St => CConstAlt ns -> Core (Integer, CConstAlt ns)
  analyzeConstAlt (MkConstAlt c y) = do
    (sy, y') <- analyze y
    pure (sy + 1, MkConstAlt c y')

analyzeDef : Ref Sts St => CDef -> Core CDef
analyzeDef (MkFun args x)      = MkFun args . snd <$> analyze x
analyzeDef d@(MkCon _ _ _)     = pure d
analyzeDef d@(MkForeign _ _ _) = pure d
analyzeDef d@(MkError _)       = pure d

analyzeName :  Ref Sts St
            => Ref Ctxt Defs
            => Name
            -> Core (Maybe (Name, FC, CDef))
analyzeName fn = do
    defs <- get Ctxt
    Just def <- lookupCtxtExact fn (gamma defs)
        | Nothing => do log "compile.execute" 50 $ "Couldn't find " ++ show fn
                        pure Nothing
    let Just cexp = compexpr def
        | Nothing => do log "compile.execute" 50 $ "Couldn't compile " ++ show fn
                        pure Nothing
    cexp' <- analyzeDef cexp
    pure $ Just (fn, location def, cexp')

--------------------------------------------------------------------------------
--          Replacing Expressions
--------------------------------------------------------------------------------

mutual
  -- During the analysis step, we replaced every closed
  -- expression with a machine generated name. We only
  -- want to keep these substitutions, if a closed term
  -- appears in several distinct locations in the code.
  --
  -- We therefore check for each machine generated name, if
  -- the corresponding closed term has a count > 1. If that's
  -- not the case, the machine generated name will be dropped
  -- and replaces with the CSE-optimized original term.
  --
  -- However, during the analysis step, we might get counts > 1
  -- for expressions that still are used only once.
  -- Consider the following situation:
  --
  --    fun1 = exp1(exp2(exp3))
  --    fun2 = exp4(exp2(exp3))
  --
  -- In the example above, `exp2` is a proper common subexpression
  -- that should be lifted to the toplevel, but exp3 is not, although
  -- it will also get a count of 2 in the `UsageMap`.
  -- We therefore compare the count of each child expression
  -- with the count of their parent expression, lifting
  -- a child only if it was counted mor often than its parent.
  replaceRef :  Ref ReplaceMap ReplaceMap
             => Ref Ctxt Defs
             => (parentCount : Integer)
             -> FC
             -> Name
             -> Core (CExp ns)
  replaceRef pc fc n = do
    log "compiler.cse" 10 $ "Trying to replace " ++ show n ++ ": "
    res <- lookup n <$> get ReplaceMap
    case res of
      -- not a name generated during CSE
      Nothing          => do
        log "compiler.cse" 10 $ "  not a name generated during CSE"
        pure (CRef fc n)

      -- Expression count has already been checked and occurs
      -- several times. Replace it with the machine generated name.
      Just (exp, Many) => do
        log "compiler.cse" 10 $ "  already replaced: Occurs many times"
        pure (CApp EmptyFC (CRef fc n) [])

      -- Expression count has already been checked and occurs
      -- only once. Substitute the machine generated name with
      -- the original (but CSE optimized) exp
      Just (exp, Once) => do
        log "compiler.cse" 10 $ "  already replaced: Occurs once"
        pure (embed exp)

      -- Expression count has not yet been compared with the
      -- parent count. Do this now.
      Just (exp, C c)  => do
        log "compiler.cse" 10 $  "  expression of unknown quantity ("
                              ++ show c
                              ++ " occurences)"
        -- We first have to replace all child expressions.
        exp' <- replaceExp c exp
        if c > pc
           -- This is a common subexpression. We set its count to `Many`
           -- and replace it with the machine generated name.
           then do
             log "compiler.cse" 10 $ show n ++ " assigned quantity \"Many\""
             update ReplaceMap (insert n (exp', Many))
             pure (CApp EmptyFC (CRef fc n) [])

           -- This expression occurs only once. We set its count to `Once`
           -- and keep it.
           else do
             log "compiler.cse" 10 $ show n ++ " assigned quantity \"Once\""
             update ReplaceMap (insert n (exp', Once))
             pure (embed exp')

  replaceExp :  Ref ReplaceMap ReplaceMap
             => Ref Ctxt Defs
             => (parentCount : Integer)
             -> CExp ns
             -> Core (CExp ns)
  replaceExp _ e@(CLocal _ _)  = pure e
  replaceExp pc (CRef f n)     = replaceRef pc f n
  replaceExp pc (CLam f n y)   = CLam f n <$> replaceExp pc y
  replaceExp pc (CLet f n i y z) =
    CLet f n i <$> replaceExp pc y <*> replaceExp pc z
  replaceExp pc (CApp f x xs) =
    CApp f <$> replaceExp pc x <*> traverse (replaceExp pc) xs
  replaceExp pc (CCon f n c t xs) =
    CCon f n c t <$> traverse (replaceExp pc) xs
  replaceExp pc (COp f n xs) =
    COp f n <$> traverseVect (replaceExp pc) xs
  replaceExp pc (CExtPrim f n xs) =
    CExtPrim f n <$> traverse (replaceExp pc) xs
  replaceExp pc (CForce f r y) =
    CForce f r <$> replaceExp pc y
  replaceExp pc (CDelay f r y) =
    CDelay f r <$> replaceExp pc y
  replaceExp pc (CConCase f sc xs x) =
    CConCase f                     <$>
    replaceExp pc sc               <*>
    traverse (replaceConAlt pc) xs <*>
    traverseOpt (replaceExp pc) x

  replaceExp pc (CConstCase f sc xs x) = do
    CConstCase f                     <$>
    replaceExp pc sc                 <*>
    traverse (replaceConstAlt pc) xs <*>
    traverseOpt (replaceExp pc) x

  replaceExp _ c@(CPrimVal _ _) = pure c
  replaceExp _ c@(CErased _)    = pure c
  replaceExp _ c@(CCrash _ _)   = pure c

  replaceConAlt :  Ref ReplaceMap ReplaceMap
                => Ref Ctxt Defs
                => (parentCount : Integer)
                -> CConAlt ns
                -> Core (CConAlt ns)
  replaceConAlt pc (MkConAlt n c t as z) =
    MkConAlt n c t as <$> replaceExp pc z

  replaceConstAlt :  Ref ReplaceMap ReplaceMap
                  => Ref Ctxt Defs
                  => (parentCount : Integer)
                  -> CConstAlt ns
                  -> Core (CConstAlt ns)
  replaceConstAlt pc (MkConstAlt c y) =
    MkConstAlt c <$> replaceExp pc y

replaceDef :  Ref ReplaceMap ReplaceMap
           => Ref Ctxt Defs
           => (Name, FC, CDef)
           -> Core (Name, FC, CDef)
replaceDef (n, fc, MkFun args x) =
  (\x' => (n, fc, MkFun args x')) <$> replaceExp 1 x
replaceDef (n, fc, d@(MkCon _ _ _))     = pure (n, fc, d)
replaceDef (n, fc, d@(MkForeign _ _ _)) = pure (n, fc, d)
replaceDef (n, fc, d@(MkError _))       = pure (n, fc, d)

newToplevelDefs : ReplaceMap -> List (Name, FC, CDef)
newToplevelDefs rm = mapMaybe toDef $ SortedMap.toList rm
  where toDef : (Name,(CExp[],Count)) -> Maybe (Name, FC, CDef)
        toDef (nm,(exp,Many)) = Just (nm, EmptyFC, MkFun [] exp)
        toDef _               = Nothing

undefinedCount : (Name, (CExp [], Count)) -> Bool
undefinedCount (_, _, Once) = False
undefinedCount (_, _, Many) = False
undefinedCount (_, _, C x)  = True

||| Runs the CSE alorithm on all provided names and
||| the given main expression.
export
cse :  Ref Ctxt Defs
    => (definitionNames : List Name)
    -> (mainExpr        : CExp ns)
    -> Core (List (Name, FC, CDef), CExp ns)
cse defs me = do
  log "compiler.cse" 10 $ "Analysing " ++ show (length defs) ++ " names"
  s            <- newRef Sts $ MkSt empty 0
  analyzedDefs <- catMaybes <$> traverse analyzeName defs
  MkSt um _    <- get Sts
  srep         <- newRef ReplaceMap $ toReplaceMap um
  replacedDefs <- traverse replaceDef analyzedDefs
  replacedMain <- replaceExp 1 me
  replaceMap   <- get ReplaceMap
  let filtered = SortedMap.toList replaceMap
  log "compiler.cse" 10 $ unlines $
    "Found the following unadjusted subexpressions:"
    ::  map (\(name,(_,cnt)) =>
                  show name ++ ": count " ++ show cnt
           ) filtered
  pure (newToplevelDefs replaceMap ++ replacedDefs, replacedMain)


text:
module EchoServer

import public Network.Socket

socketRecieve : (newSock : Socket) -> IO ()
socketRecieve newSock =
  do putStrLn "Waiting for message..."
     Right (str, res) <- recv newSock 1024
      | Left err => putStrLn (show err)
     putStrLn $ "Client send: " ++ str
     putStrLn $ "Sending back: Hello, " ++ str
     Right ok <- send newSock $ "Hello, " ++ str
      | Left err => putStrLn (show err)
     socketRecieve newSock

serverbound : (sock : Socket) -> (ok : Int) ->
  (ip : SocketAddress) -> (port : Port) -> IO ()
serverbound sock ok ip port =
  do putStrLn $ "Socket is bound to: " ++ (show ip) ++ ":" ++ (show port)
     listeningCode <- listen sock
     putStrLn $ "Socket is listening to: " ++ (show ip) ++ ":" ++ (show port)
     Right (newSock, newIp) <- accept sock | Left err => putStrLn (show err)
     putStrLn $ "Socket accepted connection from: " ++ (show newIp)
     socketRecieve newSock

servererr : (sock : Socket) -> (ok : Int) -> IO ()
servererr sock ok = putStrLn $ "Server failed" ++ (show ok)

startServer : IO ()
startServer =
  do Right sock <- socket AF_INET Stream 0
      | Left err => putStr (show err)
     putStrLn "Socket created"
     ip <- pure (IPv4Addr 192 168 87 189)
     port <- pure (the (Port) 9420)
     ok <- bind sock (Just ip) port
     if ok == 0 then (serverbound sock ok ip port)
     else (servererr sock ok)

max_stars_repo_name: AsmusAB/Idris-peer-to-peer-network

max_issues_repo_name: AsmusAB/Idris-peer-to-peer-network

max_forks_repo_name: AsmusAB/Idris-peer-to-peer-network


text:
module Main

data Point = P Int Int

Show Point where
  show (P x y) = "(Point " ++ show x ++ " " ++ show y ++ ")"

export
makePoint : Int -> Int -> Point
makePoint = P

main : IO ()
main = do
  putStr "makePoint 0 $ 0 => "
  printLn origin
  where
    origin : Point
    origin = makePoint 0 $ 0


text:
||| The telescope data structures.
|||
||| Indexing telescopes by their length (hopefully) helps inform the
||| type-checker during inference.
module Data.Telescope.Telescope

import Data.DPair
import Data.Nat
import Data.Fin

%default total

public export
plusAcc : Nat -> Nat -> Nat
plusAcc Z n = n
plusAcc (S m) n = plusAcc m (S n)

export
plusAccIsPlus : (m, n : Nat) -> (m + n) === plusAcc m n
plusAccIsPlus Z n = Refl
plusAccIsPlus (S m) n =
  rewrite plusSuccRightSucc m n in
  plusAccIsPlus m (S n)

public export
plusAccZeroRightNeutral : (m : Nat) -> plusAcc m 0 === m
plusAccZeroRightNeutral m =
  rewrite sym (plusAccIsPlus m 0) in
  rewrite plusZeroRightNeutral m in
  Refl

infixl 4 -.
infixr 4 .-

namespace Left

  mutual
    ||| A left-nested sequence of dependent types
    public export
    data Telescope : (k : Nat) -> Type where
      Nil  : Telescope 0
      (-.) : (gamma : Left.Telescope k) -> (ty : TypeIn gamma) -> Telescope (S k)

    ||| A type with dependencies in the given context
    public export
    TypeIn : Left.Telescope k -> Type
    TypeIn gamma = (env : Environment gamma) -> Type

    ||| A tuple of values of each type in the telescope
    public export
    Environment : Left.Telescope k -> Type
    Environment [] = ()
    Environment (gamma -. ty) = (env : Environment gamma ** ty env)

  export
  weakenTypeIn : TypeIn gamma -> TypeIn (gamma -. sigma)
  weakenTypeIn ty env = ty (fst env)

  public export
  uncons : (gamma : Telescope (S k)) ->
           (ty : Type
            ** delta : (ty -> Telescope k)
            ** (v : ty) -> Environment (delta v) -> Environment gamma)
  uncons ([] -. ty) = (ty () ** const [] ** \ v, _ => (() ** v))
  uncons (gamma@(_ -. _) -. ty) =
    let (sigma ** delta ** left) = uncons gamma in
    (sigma ** (\ v => delta v -. (\ env => ty (left v env)))
           ** (\ v, (env ** w) => (left v env ** w)))

  public export
  (++) : {n : Nat} -> (gamma : Left.Telescope m) -> (Environment gamma -> Left.Telescope n) ->
         Telescope (plusAcc n m)
  (++) {n = Z} gamma delta = gamma
  (++) {n = S n} gamma delta = (gamma -. sigma) ++ uncurry theta where

    sigma : Environment gamma -> Type
    sigma env = fst (uncons (delta env))

    theta : (env : Environment gamma) -> sigma env -> Telescope n
    theta env val with (uncons (delta env))
      theta env val | (sig ** omega ** _) = omega val

  public export
  cons : {k : Nat} -> (ty : Type) -> (ty -> Left.Telescope k) -> Left.Telescope (S k)
  cons sigma gamma =
    rewrite plusCommutative 1 k in
    rewrite plusAccIsPlus k 1 in
    ([] -. const sigma) ++ (gamma . snd)

  ||| A position between the variables of a telescope, counting from the _end_:
  ||| Telescope:   Nil -. ty1 -. ... -. tyn
  ||| Positions: ^k    ^k-1   ^k-2   ^1     ^0
  public export
  Position : {k : Nat} -> Telescope k -> Type
  Position {k} _ = Fin (S k)

  ||| The position at the beginning of the telescope
  public export
  start : {k : Nat} -> (gamma : Telescope k) -> Position gamma
  start {k} gamma = last

namespace Right

  mutual
    ||| A right-nested sequence of dependent types
    public export
    data Telescope : (k : Nat) -> Type where
      Nil  : Telescope 0
      (.-) : (ty : Type) -> (gamma : ty -> Right.Telescope k) -> Telescope (S k)

    ||| A tuple of values of each type in the telescope
    public export
    Environment : Right.Telescope k -> Type
    Environment [] = ()
    Environment (ty .- gamma) = (v : ty ** Environment (gamma v))

  export
  empty : (0 gamma : Right.Telescope Z) -> Environment gamma
  empty {gamma = []} = ()

  export
  snoc : (gamma : Right.Telescope k) -> (Environment gamma -> Type) -> Right.Telescope (S k)
  snoc [] tau   = tau () .- const []
  snoc (sigma .- gamma) tau = sigma .- \ v => snoc (gamma v) (\ env => tau (v ** env))

  export
  unsnoc : {k : Nat} -> (gamma : Right.Telescope (S k)) ->
           (delta : Right.Telescope k
            ** sigma : (Environment delta -> Type)
            ** (env : Environment delta) -> sigma env -> Environment gamma)
  unsnoc {k = Z} (sigma .- gamma) = ([] ** const sigma ** \ (), v => (v ** empty (gamma v)))
  unsnoc {k = S k} (sigma .- gamma)
    = (sigma .- delta ** uncurry tau ** \ (v ** env) => transp v env) where

    delta : sigma -> Right.Telescope k
    delta v = fst (unsnoc (gamma v))

    tau : (v : sigma) -> Environment (delta v) -> Type
    tau v = fst (snd (unsnoc (gamma v)))

    transp : (v : sigma) -> (env : Environment (delta v)) -> tau v env -> Environment (sigma .- gamma)
    transp v env w = (v ** (snd (snd (unsnoc (gamma v))) env w))

  export
  (++) : (gamma : Right.Telescope m) -> (Environment gamma -> Right.Telescope n) -> Right.Telescope (m + n)
  [] ++ delta = delta ()
  (sigma .- gamma) ++ delta = sigma .- (\ v => (gamma v ++ (\ env => delta (v ** env))))

  export
  split : (gamma : Right.Telescope m) -> (delta : Environment gamma -> Right.Telescope n) ->
          Environment (gamma ++ delta) ->
          (env : Environment gamma ** Environment (delta env))
  split [] delta env = (() ** env)
  split (sigma .- gamma) delta (v ** env) =
    let (env1 ** env2) = split (gamma v) (\env => delta (v ** env)) env in
    ((v ** env1) ** env2)

namespace Tree

  infixl 4 ++

  mutual
    ||| A tree of dependent types
    public export
    data Telescope : (k : Nat) -> Type where
      Nil  : Telescope 0
      Elt  : Type -> Telescope 1
      (++) : (gamma : Tree.Telescope m) ->
             (delta : Tree.Environment gamma -> Tree.Telescope n) ->
              Telescope (m + n)

    ||| A tuple of values of each type in the telescope
    public export
    Environment : Tree.Telescope k -> Type
    Environment [] = ()
    Environment (Elt t) = t
    Environment (gamma ++ delta) = (env : Environment gamma ** Environment (delta env))

  export
  concat : (gamma : Tree.Telescope k) -> (delta : Right.Telescope k ** Environment delta -> Environment gamma)
  concat Nil = ([] ** id)
  concat (Elt t) = ((t .- const []) ** fst)
  concat (gamma ++ delta) =
    let (thetaL ** transpL) = concat gamma in
    ((thetaL ++ \ envL => fst (concat (delta (transpL envL))))
    ** \ env =>
         let (env1 ** env2) = split thetaL (\ envL => fst (concat (delta (transpL envL)))) env in
         (transpL env1 ** snd (concat (delta (transpL env1))) env2)
    )

infix 5 <++>

public export
(<++>) : (gamma : Left.Telescope m) -> (Environment gamma -> Right.Telescope n) -> Right.Telescope (plusAcc m n)
[] <++> delta = delta ()
(gamma -. sigma ) <++> delta = gamma <++> (\ env => sigma env .- \ v => delta (env ** v))

infix 5 >++<

(>++<) : {m, n : Nat} -> (gamma : Right.Telescope m) -> (Environment gamma -> Left.Telescope n) ->
         Left.Telescope (plusAcc m n)
[] >++< delta = delta ()
gamma@(_ .- _) >++< delta =
  let (gamma ** sigma ** transp) = unsnoc gamma in
  gamma >++< \ env => (cons (sigma env) (\ v => delta (transp env v)))

export
leftToRight : Left.Telescope m -> Right.Telescope m
leftToRight gamma = rewrite sym (plusAccZeroRightNeutral m) in (gamma <++> const [])

export
rightToLeft : {m : Nat} -> Right.Telescope m -> Left.Telescope m
rightToLeft gamma = rewrite sym (plusAccZeroRightNeutral m) in (gamma >++< const [])


text:
-- Idris2

import System
import System.Concurrency

-- Test that acquiring the mutex in the parent, then the child blocks correctly
main : IO ()
main =
  do m <- makeMutex
     mutexAcquire m
     putStrLn "Main acquired mutex"
     t <- fork $ do mutexAcquire m
                    putStrLn "Child acquired mutex"
                    sleep 2
                    mutexRelease m
                    putStrLn "Child released mutex"
     sleep 1
     mutexRelease m
     putStrLn "Main released mutex"
     threadWait t


text:
import Data.Vect

using (Show a, Eq a)
  foo : a -> String
  foo x = show x ++ show x

  bar : Int -> Int
  bar x = x + x

using (xs : Vect n a, n : Nat) -- get reordered in dependency order by
                               -- the usual implicit rules
  baz : xs = xs

data Test : Type -> Type -> Type where

using (Test a b)
  needle : a -> b -> ()
  nardle : a -> ()
  noo : b -> ()


text:
module Data.Time.Calendar.MonthDay

import Data.Vect

import Data.Time.Calendar.Private

export
monthLengths: Bool -> Vect 12 Nat
monthLengths False = [31, 28, 31, 30, 31, 30, 31, 31, 30, 31, 30, 31]
monthLengths True = [31, 29, 31, 30, 31, 30, 31, 31, 30, 31, 30, 31]

export
monthSum: Bool -> Vect 12 Nat
monthSum False = [31, 59, 90, 120, 151, 181, 212, 243, 273, 304, 334, 365]
monthSum True = [31, 60, 91, 121, 152, 182, 213, 244, 274, 305, 335, 366]

export
YearBound : (isLeap: Bool) -> Type
YearBound False = Fin 365
YearBound True = Fin 366

export
dayLengthBounds : Fin 12  -> Vect 12 Nat -> Type
dayLengthBounds x xs  = Fin $ succ $ index x xs

export
DayBounds : Fin 12 -> Bool -> Type
DayBounds n isLeap =  (dayLengthBounds n (monthLengths isLeap))

-- defDayLengthBounds : (n: Fin 12) ->  (dayLengthBounds n (monthLengths isLeap))
-- defDayLengthBounds x = Vect.index x (monthLengths True)

-- hole : (n : Integer) -> ((n1 : Nat) -> Maybe (Fin n1)) -> Fin 32
-- hole n f = ?hole_rhs

||| Used to clip the days value to a typed bounded value based on the provided month and isLeap value
export
boundedDay: (n: Int) -> (month: Fin 12) -> (isLeap: Bool) -> Maybe (DayBounds month isLeap)
boundedDay x m isLeap = integerToFin (cast x) (S (Vect.index m (monthLengths isLeap)))

export
boundedDay': (n: Int) -> (month: Fin 12) -> (isLeap: Bool) -> Nat
boundedDay' x m isLeap = Vect.index m (monthLengths isLeap)

-- construct_prf : (n: Nat) -> (xs: List a) -> (prf: NonEmpty xs) ->  InBounds n xs
-- construct_prf _ [] IsNonEmpty impossible
-- construct_prf Z (x :: xs) prf = InFirst
-- construct_prf (S k) (x :: y :: xs) prf = InLater (construct_prf k (y::xs) prf)

-- -- construct_prf Z [] = ?construct_prf_rhs_4
-- -- construct_prf Z (x :: xs) = InFirst
-- -- construct_prf (S k) (x::xs) = InLater (construct_prf k xs)

-- | The length of a given month in the Gregorian or Julian calendars.
-- First arg is leap year flag.
export
monthLength: Bool -> Fin 12 -> Nat
monthLength isLeap month' =
  let
    --inBounds = InBounds (cast (month' - 1)) (monthLengths isLeap)
    monthLengths' = (monthLengths isLeap)
  in
    index month' monthLengths'

--   --Prelude.List.index (cast (month' - 1)) (monthLengths isLeap) {inBounds}

-- ||| Convert month and day in the Gregorian or Julian calendars to day of year.
-- ||| First arg is leap year flag.
export
monthAndDayToDayOfYear : (isLeap: Bool) -> Int -> Int -> Int
monthAndDayToDayOfYear isLeap month day' =
  let
    day' = day'
    k =
      if month <= 2
        then 0
        else if isLeap
                then -1
                else -2
    res = (div (367 * month - 362) 12) + k + day'
  in
    res

export
findMonthDay: Vect n Nat -> Int -> (Int, Int)
findMonthDay (y :: xs) yd =
  if yd > cast y
  then (\(m, d) => (m + 1, d)) (findMonthDay xs (yd - cast y))
  else (1, yd)

export
findDay: Vect n Nat -> Int -> Int
findDay (y :: xs) yd =
  if yd > cast y
  then findDay xs (yd - cast y)
  else yd

export
findMonth : (m: Fin 12) -> (isLeap: Bool) -> Int  -> Fin 12
findMonth FZ isLeap x = if x > cast (Vect.index FZ (monthSum isLeap)) then (FS FZ) else FZ
findMonth (FS y) isLeap x = if x > cast (Vect.index (FS y) (monthSum isLeap)) then succ (FS y) else findMonth (pred (FS y)) isLeap x

-- export
-- findMonth' : (m: Fin 12) -> (in_m: Fin 12) (isLeap: Bool) -> (x: YearBound True)  -> (x ** DayBounds x isLeap)
-- findMonth' FZ in_m isLeap x = if (finToInteger x) > cast (Vect.index FZ (monthSum isLeap)) then ((FS FZ),  else FZ
-- findMonth' (FS y) in_m isLeap x = if (finToInteger x) > cast (Vect.index (FS y) (monthSum isLeap)) then succ (FS y) else findMonth (pred (FS y)) isLeap x

-- ||| Convert day of year in the Gregorian or Julian calendars to month and day.
-- ||| First arg is leap year flag.
export
dayOfYearToMonthAndDay : Bool -> Int -> (Int, Int)
dayOfYearToMonthAndDay isLeap yd =
  let
    clipped = (clip 1 (if isLeap then 366 else 365)  yd)
  in
    findMonthDay (monthLengths isLeap) clipped

max_stars_repo_name: gdevanla/idris-time

max_issues_repo_name: gdevanla/idris-time

max_forks_repo_name: gdevanla/idris-time


text:
module Data.Crypto.Encryption.Stream.ARC4

import Control.Monad.State
import Data.Bits
import Data.Fin
import Data.Vect

import Data.Crypto.Util
import Data.Crypto.Encryption
import Data.Crypto.Encryption.Stream
import Data.Mod

%default total
%access private

-- This is off-by-one to make it easy to prove non-zero with (S x) in the code.
-- Hopefully, no one will ever actually need to construct one of these
-- explicitly.
public export
KeySizeMin1 : Type
KeySizeMin1 = Fin 255

public export
ARC4Key : KeySizeMin1 -> Type
ARC4Key n = Vect (S (cast n)) (Mod 256) -- should be Byte, but can’t convert yet

public export
data AllegedRivestCipher4 : KeySizeMin1 -> Type where
  ARC4 : ARC4Key n -> AllegedRivestCipher4 n

KSA : ARC4Key n -> Vect 256 (Mod 256)
KSA {n=n} key =
  nextJ 255 0 0 (map fromInteger (fromList [0..255]))
  where
    nextJ : Nat -> Fin 256 -> Mod 256 -> Vect 256 (Mod 256) -> Vect 256 (Mod 256)
    nextJ Z i j s =
      let ind = tightmod (cast i) (S (cast n))
      in let newJ = j + index i s + index ind key
         in swap i (cast newJ) s
    nextJ (S c) i j s =
      let ind = tightmod (cast i) (S (cast n))
      in let newJ = j + index i s + index ind key
         in let newS = (swap i (cast newJ) s)
            in case strengthen (FS i) of
              Left _ => newS
              Right newI => nextJ c newI newJ newS

PGRA : Mod 256 -> Mod 256 -> Vect 256 (Mod 256) -> Stream Byte
PGRA i j S = let newI = i + 1
             in let newJ = j + index (cast newI) S
                in let newS = swap (cast newI) (cast newJ) S
                   in Prelude.Stream.(::)
                      (modToBits (index (cast (index (cast newI) newS + index (cast newJ) newS)) newS))
                      (PGRA newI newJ newS)

implementation Cipher (AllegedRivestCipher4 n) 8 where

implementation StreamCipher (AllegedRivestCipher4 n) 8 where
  generateKeystream (ARC4 key) = PGRA 0 0 (KSA key)

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 NonNegDouble.NonNegDouble

> import Double.Predicates

> %default total
> %access public export

> ||| Non negative double precision floating point numbers as sigma types
> NonNegDouble : Type
> -- NonNegDouble = Subset Double NonNegative
> NonNegDouble = Subset Double (\ x => 0.0 `LTE` x)

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
import Data.Vect

allLengths : Vect len String -> Vect len Nat
allLengths [] = []
allLengths (word :: words) = length word :: allLengths words


text:
module Main

-- Test wraparound from upper bounds of Bits types
main : IO ()
main = do putStrLn (show $ the Bits16 maxBound)
          putStrLn (show $ the Bits16 maxBound + 1)
          putStrLn (show $ the Bits32 maxBound)
          putStrLn (show $ the Bits32 maxBound + 1)
          putStrLn (show $ the Bits64 maxBound)
          putStrLn (show $ the Bits64 maxBound + 1)


text:
module Inigo.Account.Account

import Data.List
import Data.Maybe
import Extra.String
import Fmt
import Toml
import Inigo.Async.SubtleCrypto.SubtleCrypto -- TODO: We don't use Async, maybe split package?

||| An account registered with an Inigo server
public export
record Account where
  constructor MkAccount
  ns : String
  email : String
  kdf : Algorithm
  hash : String

public export
Show Account where
  show (MkAccount ns email _ _) = fmt "MkAccount{ns=%s, email=%s, kdf=***, hash=***}" ns email

public export
Eq Account where
  (MkAccount ns0 email0 kdf0 hash0) == (MkAccount ns1 email1 kdf1 hash1) =
    ns0 == ns1 && email0 == email1 && kdf0 == kdf1 && hash0 == hash1

||| Encodes an account into a Toml data type
toToml : Account -> Toml
toToml (MkAccount ns email kdf hash) =
  [ (["ns"], Str ns)
  , (["email"], Str email)
  ] ++ toTomlKdf kdf ++
  [ (["hash"], Str hash)
  ]
  where
    toTomlKdf : Algorithm -> Toml
    toTomlKdf (PBKDF2 sha salt iterations) =
      [ (["kdf", "type"], Str "PBKDF2")
      , (["kdf", "sha"], Str (encodeSha sha))
      , (["kdf", "salt"], Str salt)
      , (["kdf", "iterations"], Num iterations)
      ]

    toTomlKdf (ECDSA sha) =
      [ (["kdf", "type"], Str "ECDSA")
      , (["kdf", "sha"], Str (encodeSha sha))
      ]

||| Decodes a Toml data value into an account object
export
fromToml : Toml -> Maybe Account
fromToml toml =
  do
    ns <- str ["ns"] toml
    email <- str ["email"] toml
    kdf <- fromTomlKdf (getToml ["kdf"] toml)
    hash <- str ["hash"] toml
    pure $ (MkAccount ns email kdf hash)
  where
    str : List String -> Toml -> Maybe String
    str key toml =
      case get key toml of
        Just (Str v) =>
          Just v

        _ =>
          Nothing

    int : List String -> Toml -> Maybe Int
    int key toml =
      case get key toml of
        Just (Num v) =>
          Just v

        _ =>
          Nothing

    fromTomlKdfType : String -> Toml -> Maybe Algorithm
    fromTomlKdfType "PBKDF2" toml =
      do
        sha <- (str ["sha"] toml) >>= decodeSha
        salt <- str ["salt"] toml
        iterations <- int ["iterations"] toml
        pure (PBKDF2 sha salt iterations)
    fromTomlKdfType "ECDSA" toml =
      do
        sha <- (str ["sha"] toml) >>= decodeSha
        pure (ECDSA sha)
    fromTomlKdfType _ _ = Nothing

    fromTomlKdf : Toml -> Maybe Algorithm
    fromTomlKdf toml =
      do
        type <- str ["type"] toml
        fromTomlKdfType type toml

||| Encodes an account into a Toml doc
export
encode : Account -> String
encode =
  encode . toToml

||| Decodes an account from a Toml doc
export
decode : String -> Maybe Account
decode str =
  parseToml str >>= fromToml

-- TODO: Improve quality of Validity parsing, e.g. by passing back a hidden type
export
require : List (Bool, String) -> List String
require conds =
  foldl accumulateErr [] conds
  where
    accumulateErr : List String -> (Bool, String) -> List String
    accumulateErr acc (cond, err) =
      if cond then
        acc
      else
        (err :: acc)

export
nsValid : String -> List String
nsValid str =
  let
    unpacked = unpack str
  in
    require
      [ (length str >= 4, "Namespace must be at least 4 chars")
      , ( (foldl (\acc, el => acc && (isAlphaNum el)) True unpacked) , "Namespace must be alpha-numeric")
      , (fromMaybe False $ map isUpper $ head' unpacked, "Must start with an uppercase letter") --'
      ]

export
emailValid : String -> List String
emailValid email =
  require $ case split '@' email of
    (first :: last :: []) =>
      do
      [ ( length first > 0, "Invalid email username" )
      , ( length last > 0, "Invalid email domain" )
      ]
    _ =>
      [ ( False, "Email must contain a single @ sign" ) ]

export
passphraseValid : String -> List String
passphraseValid passphrase =
  require
    [ ( length passphrase > 10, "Please use a strong passphrase" ) ]

export
mkAccount : String -> String -> Algorithm -> String -> String -> Either String Account
mkAccount ns email kdf passphrase hash =
  do
    validate (nsValid ns)
    validate (emailValid email)
    validate (passphraseValid passphrase)
    pure $ MkAccount ns email kdf hash
  where
    validate : List String -> Either String ()
    validate [] = Right ()
    validate errs = Left (join ", " errs)

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
module Uri.Types

import Data.List

public export
record Authority where
    constructor MkAuthority
    userInfo : Maybe String
    host : String
    port : Maybe Int

public export
record AbsoluteURI where
    constructor MkAbsURI
    scheme : String
    authority : Maybe Authority
    path : Maybe String
    query : Maybe String
    fragment : Maybe String

public export
record RelativeURI where
    constructor MkRelURI
    path : String
    query : Maybe String

public export
data URI
    = Absolute AbsoluteURI
    | Relative RelativeURI

par : String -> List String -> String
par name args = "(" ++ (concat $ intersperse " " (name :: args)) ++ ")"

before : Maybe String -> String -> String
before (Just n) str = str ++ n
before Nothing str = ""

after : Maybe String -> String -> String
after (Just n) str = n ++ str
after Nothing str = ""

public export
interface Encode t where
    encode : t -> String

public export
Encode Authority where
    encode (MkAuthority userinfo host port) =
        (after (userinfo) "@")
     ++ host
     ++ (before (show <$> port) ":")

public export
Encode AbsoluteURI where
    encode (MkAbsURI scheme authority path query fragment) =
        scheme ++ ":" ++ (before (encode <$> authority) "//") ++ (before path "") ++ (before query "?") ++ (before fragment "#")

public export
Encode RelativeURI where
    encode (MkRelURI path query) = par "RelativeURI" [show path, show query]

public export
Encode URI where
    encode (Absolute uri) = encode uri
    encode (Relative uri) = encode uri

-- Show

public export
Show Authority where
    show (MkAuthority userinfo host path) =
        par "Authority" [show userinfo, show host, show path]

public export
Show AbsoluteURI where
    show (MkAbsURI scheme authority path query frag) =
        par "AbsUri" [show scheme, show authority, show path, show query, show frag]

public export
Show RelativeURI where
    show (MkRelURI path query) = par "RelativeURI" [show path, show query]

public export
Show URI where
    show (Absolute uri) = par "Absolute" [show uri]
    show (Relative uri) = par "Relative" [show uri]

max_stars_repo_name: felipegchi/sayURI

max_issues_repo_name: felipegchi/sayURI

max_forks_repo_name: felipegchi/sayURI


text:
module Graphics.Shape
import Data.Vect

%access public export
Point : Type
Point = (Double, Double)

data Path : (n : Nat) -> Type where
  Start  : Point -> Path Z
  Append : Path k -> Point -> Path (S k)

Line : Point -> Point -> Path 1
Line from to = (Start from) `Append` to

Triangle : Path 1 -> Point -> Path 3
Triangle (Append (Start x) y) z = ((Line x y) `Append` z) `Append` x

toPoints : Path n -> Vect (n+1) Point
toPoints (Start x)          = [x]
toPoints (Append path next) = let ps = next :: toPoints path
                              in reverse ps

max_stars_repo_name: eckart/cairo-idris

max_issues_repo_name: eckart/cairo-idris

max_forks_repo_name: eckart/cairo-idris


text:
data SplitList : List a -> Type where
    SplitNil : SplitList []
    SplitOne : SplitList [x]
    SplitPair : (lefts : List a) -> (rights : List a) -> SplitList (lefts ++ rights)

total
splitList : (input : List a) -> SplitList input
splitList input = splitListHelp input input
    where
        splitListHelp : List a -> (input : List a) -> SplitList input
        splitListHelp _ [] = SplitNil
        splitListHelp _ [x] = SplitOne
        splitListHelp (_ :: _ :: counter) (item :: items) =
            case splitListHelp counter items of
                SplitNil => SplitOne
                SplitOne {x} => SplitPair [item] [x]
                SplitPair lefts rights => SplitPair (item :: lefts) rights
        splitListHelp _ items = SplitPair [] items

mergeSort : Ord a => List a -> List a
mergeSort input with (splitList input)
  mergeSort [] | SplitNil = []
  mergeSort [x] | SplitOne = [x]
  mergeSort (lefts ++ rights) | (SplitPair lefts rights) =
    merge (mergeSort lefts) (mergeSort rights)


text:
module BootstrapHeap

import Heap

%default total
%access private

export
data BootstrapHeap : (Type -> Type) -> Type -> Type where
  E : BootstrapHeap h a
  H : a -> h (BootstrapHeap h a) -> BootstrapHeap h a

Eq a => Eq (BootstrapHeap h a) where
  x == y = assert_total $ case x of
    (H x' _) => case y of
      (H y' _) => x' == y'

Ord a => Ord (BootstrapHeap h a) where
  compare x y = assert_total $ case x of
    (H x' _) => case y of
      (H y' _) => compare x' y'

Heap h => Heap (BootstrapHeap h) where
  empty = E
  isEmpty E = True
  isEmpty _ = False

  insert x h = merge (assert_total $ H x empty) h

  merge h1 h2 = assert_total $ case h1 of
    E        => h2
    (H x p1) => case h2 of
      E        => h1
      (H y p2) => if x <= y then H x (insert h2 p1) else H y (insert h1 p2)

  findMin h = assert_total $ case h of
    E       => idris_crash "empty heap"
    (H x p) => x

  deleteMin h = assert_total $ case h of
    E => idris_crash "empty heap"
    (H x p) =>
      if isEmpty p then E
      else let (H y p1) = findMin p
               p2 = deleteMin p
           in (H y (merge p1 p2))


text:
import TestEx

area : Shape -> Double
area s with (shapeView s)
  area (triangle base height) | STriangle = 0.5 * base * height
  area (rectangle width height) | SRectangle = width * height
  area (circle radius) | SCircle = pi * radius * radius

main : IO ()
main = do printLn (area (rectangle 2 3))
          printLn (area (triangle 2 3))
          printLn (area (circle 1))

max_stars_repo_name: grin-compiler/idris-grin

max_issues_repo_name: grin-compiler/idris-grin

max_forks_repo_name: grin-compiler/idris-grin


text:
-- -------------------------------------------------------------- [ Reader.idr ]
-- Module      : Text.Kindle.Clippings.Reader
-- Description : Parse Kinddle clippings.
--
-- License     : This code is distributed under the MIT license. See the
--               file LICENSE in the root directory for its full text.
-- --------------------------------------------------------------------- [ EOH ]
module Text.Kindle.Clippings.Reader

import public Text.Kindle.Clippings.Types

import public Lightyear
import public Lightyear.Char
import public Lightyear.Strings

-- FIXME: Handle this (better)
%access public export

-- -------------------------------------------------------- [ Helper Functions ]

||| Parse a series of one or more non-whitespace characters,
||| packing them into a string.
word : Parser String
word = pack <$> some (satisfy (not . isSpace)) <* spaces

||| Parse a series of characters up to the end of a line.
line : Parser String
line = pack <$> manyTill anyChar endOfLine

||| Parse an parenthesized author name in reverse.
author' : Parser Author
author' = Strings.reverse <$> quoted' ')' '('

||| Parse a title, i.e. the rest of a line, in reverse.
title' : Parser Title
title' = reverse . unwords <$> many word

||| Parse a document, i.e. a title, followed by
||| a possibly absent parenthesized author, in reverse.
||| N.B. This will consider `"bar"` in `"Foo (bar)"` to be an author.
document' : Parser Document
document'= flip Doc <$> opt author' <*> title'

||| Parse a document, i.e. a title, followed by
||| a possibly absent parenthesized author.
||| N.B. This will consider `"bar"` in `"Foo (bar)"` to be an author.
document : Parser Document
document = do
  s <- Strings.reverse <$> line
  either fail pure (Strings.parse document' s)

||| Parse the beginning of the second line of a clipping for its content type.
contentType : Parser String
contentType = string "- " *> opt (string "Your ")
           *> word
           <* (token "on" <|> token "at")

||| Parse a singleton interval, i.e. a single page or location number.
singletonInterval : Parser Interval
singletonInterval = Singleton <$> integer

-- TODO: enforce from =< to
||| Parse a proper interval, i.e. a range of pages or locations.
properInterval : Parser Interval
properInterval = Proper <$> integer <*> (char '-' *> integer)

||| Parse an proper or singleton interval.
interval : Parser Interval
interval = properInterval <|> singletonInterval

||| Parse a reference to a page number or range of pages.
page : Parser Page
page = oneOf "Pp" *> string "age " *> interval <* string " | "

||| Parse a reference to a location or range of locations.
location : Parser Location
location = (token "Loc. " <|> token "Location" <|> token "location")
        *> interval
        <* some (oneOf " |")

||| Parse date of the form, `"%A, %B %d, %Y %T"`.
||| N.B. For now, this ignores the time.
date : Parser Date
date = do token "Added on"
          Just day    <- Days.fromString . pack <$> many letter
            | Nothing => fail "Bad day!"
          comma
          Just month  <- Months.fromString . pack <$> many letter
            | Nothing => fail "Bad month!"
          space
          -- Just date'  <- (\i => integerToFin i 32) <$> integer
          --   | Nothing => fail "Bad date!"
          date'       <- integer
          comma
          year        <- integer
          -- -- TODO: time
          manyTill anyToken endOfLine
          pure $ MkDate day month date' year

||| Parse the end of a clipping record, i.e. zero or more newlines,
||| followed by `"=========="`.
eor : Parser ()
eor = many endOfLine *> token "=========="

||| Parse some content, i.e. empty lines for a `Bookmark`, the `selection` of a
||| `Highlight` or the `body` of a `Note`.
content : Parser String
content = many endOfLine *> pack <$> manyTill anyToken (many endOfLine *> eor)

-- ------------------------------------------------------- [ A Clipping Parser ]

||| Parse an entire clipping.
clipping : Parser (Maybe Clipping)
clipping = do
  doc     <- document
  type    <- contentType
  pos     <- liftA2 mkPosition (opt page) (opt location)
  date    <- pure <$> date
  content <- (<*>) (mkContent type) . pure <$> content
  pure $ Clip doc <$> pos <*> date <*> content

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

max_stars_repo_name: yurrriq/my-clippings

max_issues_repo_name: yurrriq/my-clippings

max_forks_repo_name: yurrriq/my-clippings


text:
module IHateParens

import Data.List

%default total

infixl 0 .|

-- Instead of `f (a b) $ c d` or `f (a b) (c d)` you can write `f .| a b .| c d`
public export %inline
(.|) : (a -> b) -> a -> b
(.|) = id

f : String -> List String -> String
f x = foldr .| (++) . (++ "_") .| "foo" ++ x
--f x = foldr ((++) . (++ "_")) $ "foo" ++ x
--f x = foldr ((++) . (++ "_")) ("foo" ++ x)

f_corr : f "x" ["a", "b", "c"] = "a_b_c_foox"
f_corr = Refl

record Rec where
  constructor MkRec
  oneField : Int
  anotherField : Nat
  yetAnotherField : List Nat

r : Nat -> Rec
r n = MkRec
  .| cast (n + 1)
  .| n + 3
  .| replicate n 5

r_corr : r 4 = MkRec 5 7 [5, 5, 5, 5]
r_corr = Refl

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
import System.File

main : IO ()
main = do
    Right f <- openFile "sampleFile.txt" Read
        | Left err => printLn err
    Right contents <- fRead f
        | Left err => printLn err
    printLn contents


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

Passport : Type
Passport = List (String, String)

||| Split a string at the first colon in it: "abc:def" -> ("abc", "def").
splitColon : String -> (String, String)
splitColon s = let (p, q) = break (==':') s in (p, pack $ drop 1 $ unpack q)

requiredFields : List String
requiredFields = ["byr","iyr","eyr","hgt","hcl","ecl","pid"] -- not "cid"

||| *: Are all required fields present?
isValid1 : Passport -> Bool
isValid1 passport =
  all (\k => any ((==k) . fst) passport) requiredFields

||| Check if a string represents a natural number in a given range [lo, hi].
isNatInRange : Nat -> Nat -> String -> Bool
isNatInRange lo hi s =
  case parsePositive s of
    Nothing => False
    Just n => n >= lo && n <= hi

||| Validate a passport field.
isValidField : (String, String) -> Bool
isValidField (k, v) =
  case k of
    "byr" => isNatInRange 1920 2002 v
    "iyr" => isNatInRange 2010 2020 v
    "eyr" => isNatInRange 2020 2030 v
    "hgt" =>
      case span isDigit v of
        (n, "cm") => isNatInRange 150 193 n
        (n, "in") => isNatInRange 59 76 n
        _ => False
    "hcl" =>
      case unpack v of
        ('#'::xs) => length xs == 6 && all isLowerHexDigit xs
        _ => False
    "ecl" => Prelude.elem v ["amb","blu","brn","gry","grn","hzl","oth"]
    "pid" => let xs = unpack v in length xs == 9 && all isDigit xs
    "cid" => True
    _ => False

||| **: Are all required field present, and are all fields valid?
isValid2 : Passport -> Bool
isValid2 passport =
  isValid1 passport && all isValidField passport

partial
main : IO ()
main = do
  paras <- readParagraphs
  let passports = map (map splitColon . words . unwords) paras
  putStr "*   "; printLn (count isValid1 passports)
  putStr "**  "; printLn (count isValid2 passports)


text:
module Main
import Effects
import Effect.StdIO
import IdrisNet.Socket
import IdrisNet.UDP.UDPClient

getAndSend : Nat -> SocketAddress -> Port ->
            { [UDPCLIENT, STDIO] } Eff IO ()
getAndSend Z sa p = return ()
getAndSend (S k) sa p = do
  putStr $ "Enter a string to send.\n"
  line <- getStr
  case !(udpWriteString sa p line) of
    UDPSuccess _ => getAndSend k sa p
    UDPRecoverableError _ => getAndSend (S k) sa p
    UDPFailure err => putStr ("Error: " ++ (show err) ++ "\n")

main : IO ()
main = run (getAndSend 5 (IPv4Addr 127 0 0 1) 4099)


text:
module Patricia.IntSet

import Patricia.IntMap

%default total
%access export

public export
data IntBitSet : (bits : Nat) -> Type where
  MkIntSet : IntBitMap bits Unit -> IntBitSet bits

||| Integer set with 32 bits integers as an element.
public export
Int32Set : Type
Int32Set = IntBitSet 32

||| `O(n)`. Number of elements in `IntBitSet`.
public export
size : IntBitSet (S n) -> Nat
size (MkIntSet t) = size t

||| `O(min(n, W))`. Check if the value is in the `IntBitSet`.
public export
member : Integer -> IntBitSet (S n) -> Bool
member x (MkIntSet t) = isJust (lookup x t)

||| `O(min(n,W))`. Insert a new `value` in the `IntBitSet`.
||| If the value is already present in the set, the tree isn't changed.
public export
insert : Integer -> IntBitSet (S n) -> IntBitSet (S n)
insert x (MkIntSet t) = MkIntSet (insert x () t)

||| `O(min(n,W))`. Delete the `value` from `IntBitSet`.
||| If the value is not present in the set, the tree isn't changed.
public export
delete : Integer -> IntBitSet (S n) -> IntBitSet (S n)
delete x (MkIntSet t) = MkIntSet (delete x t)

||| Create `IntBitSet` from list of `value`.
public export
fromList : List Integer -> IntBitSet (S n)
fromList = MkIntSet . fromList . map (\x => (x, ()))

max_stars_repo_name: ChShersh/idris-persistent-array

max_issues_repo_name: ChShersh/idris-patricia

max_forks_repo_name: ChShersh/idris-persistent-array


text:
import Control.ST
import Control.ST.ImplicitCall
import Network.Socket

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

data CloseOK : SocketState -> Type where
    CloseOpen : CloseOK Open
    CloseListening : CloseOK Listening

interface Sockets (m : Type -> Type) where
    Sock : SocketState -> Type

    socket : SocketType -> ST m (Either () Var) [addIfRight (Sock Ready)]

    bind : (sock : Var) -> (addr : Maybe SocketAddress) -> (port : Port) ->
            ST m (Either () ()) [sock ::: Sock Ready :-> (Sock Closed `or` Sock Bound)]
    listen : (sock : Var) -> ST m (Either () ())
            [sock ::: Sock Bound :-> (Sock Closed `or` Sock Listening)]
    accept : (sock : Var) -> ST m (Either () Var)
            [sock ::: Sock Listening, addIfRight $ Sock Open]

    connect : (sock : Var) -> SocketAddress -> Port ->
            ST m (Either () ()) [sock ::: Sock Ready :-> (Sock Closed `or` Sock Open)]

    send : (sock : Var) -> String ->
            ST m (Either () ()) [sock ::: Sock Open :-> (Sock Closed `or` Sock Open)]
    recv : (sock : Var) -> ST m (Either () String)
            [sock ::: Sock Open :-> (Sock Closed `or` Sock Open)]

    close : (sock : Var) -> {auto prf : CloseOK st} -> ST m () [sock ::: Sock st :-> Sock Closed]
    remove : (sock : Var) -> ST m () [Remove sock (Sock Closed)]

echoServer : (ConsoleIO m, Sockets m) => (sock : Var) ->
    ST m () [remove sock (Sock {m} Listening)]
echoServer sock =
    do
        Right new <- accept sock
            | Left err => do close sock; remove sock
        Right msg <- recv new
            | Left err => do close sock; remove sock; remove new
        Right ok <- send new ("You said " ++ msg)
            | Left err => do remove new; close sock; remove sock
        close new; remove new; echoServer sock

startServer : (ConsoleIO m, Sockets m) => ST m () []
startServer =
    do
        Right sock <- socket Stream
            | Left err => pure ()
        Right ok <- bind sock Nothing 9442
            | Left err => remove sock
        Right ok <- listen sock
            | Left err => remove sock
        echoServer sock

implementation Sockets IO where
    Sock _ = State Socket

    socket ty =
        do
            Right sock <- lift $ Socket.socket AF_INET ty 0
                | Left err => pure (Left ())
            lbl <- new sock
            pure (Right lbl)

    bind sock addr port =
        do
            ok <- lift $ bind !(read sock) addr port
            if ok /= 0
                then pure (Left ())
                else pure (Right ())

    listen sock =
        do
            ok <- lift $ listen !(read sock)
            if ok /= 0
                then pure (Left ())
                else pure (Right ())

    accept sock =
        do
            Right (conn, addr) <- lift $ accept !(read sock)
                | Left err => pure (Left ())
            lbl <- new conn
            returning (Right lbl) (toEnd lbl)

    connect sock addr port =
        do
            ok <- lift $ connect !(read sock) addr port
            if ok /= 0
                then pure (Left ())
                else pure (Right ())

    close sock =
        do
            lift $ close !(read sock)
            pure ()

    remove sock = delete sock

    send sock msg =
        do
            Right _ <- lift $ send !(read sock) msg
                | Left _ => pure (Left ())
            pure (Right ())
    recv sock =
        do
            Right (msg, len) <- lift $ recv !(read sock) 1024
                | Left _ => pure (Left ())
            pure (Right msg)


text:
module Inspect

data Inspect : a -> Type where
  wi : {A : Type} -> (x : A) -> (y : A) -> (eq: x = y) -> Inspect x

inspect : {A : Type} -> (x : A) -> Inspect x
inspect x = wi x _ Refl

max_stars_repo_name: archaeron/idris-json-rpc

max_issues_repo_name: archaeron/idris-json-rpc

max_forks_repo_name: archaeron/idris-json-rpc


text:
module Using

interface MagmaT a where
  op: a -> a -> a

interface MagmaT a => SemigroupT a where
  assoc: (x, y, z: a) -> (x `op` y) `op` z = x `op` (y `op` z)

[NamedMagma1] MagmaT Bool where
  False `op` False = False
  _     `op` _     = True

[NamedMagma2] MagmaT Bool where
  True `op` True = True
  _    `op` _    = False

[NamedSemigroup1] SemigroupT Bool using NamedMagma1 where
  assoc = ?hole1

[NamedSemigroup2] SemigroupT Bool using NamedMagma2 where
  assoc = ?hole2


text:
module Generics.Newtype.FromDouble

import Generics.Derive
%language ElabReflection

--------------------------------------------------------------------------------
--          FromDouble
--------------------------------------------------------------------------------

-- Derivation of FromDouble for n-ary products or newtypes
-- e.g. `(a,b,c)` or `data Foo a = MkFoo a`  or  `data Foo = Foo Int`

-- n-ary products, e.g. (a,b,c)   (data Foo x y = MkFoo x y)
public export
(all : NP (FromDouble . f) ks) => FromDouble (NP f ks) where
  fromDouble {all = []} _ = []
  fromDouble {all = _::_} d = fromDouble d :: fromDouble d

-- This type of deriving is for newtypes so we restrict oursellves to single constructor types.
public export
(all : NP (FromDouble . f) [k']) => FromDouble (NS f [k']) where
  fromDouble {all = _::_} i = Z (fromDouble i)

public export
POP (FromDouble . f) kss => FromDouble (POP f kss) where
  fromDouble i = MkPOP (fromDouble i)

public export
POP (FromDouble . f) [ks] => FromDouble (SOP f [ks]) where
  fromDouble i = MkSOP (fromDouble i)

export
genericFromDouble : Generic t [code] => POP FromDouble [code] => Double -> t
genericFromDouble = to . fromDouble

export
||| Derives a `FromDouble` implementation for the given data type
||| and visibility.
FromDoubleVis : Visibility -> DeriveUtil -> InterfaceImpl
FromDoubleVis vis g = MkInterfaceImpl "FromDouble" vis []
                       `(MkFromDouble genericFromDouble)
                       (implementationType `(FromDouble) g)

export
||| Alias for `EncodeVis Public`.
FromDouble : DeriveUtil -> InterfaceImpl
FromDouble = FromDoubleVis Public