text:
module Rationals

isFactorInt : Integer -> Integer -> Type  --Needed for defining Integer division
isFactorInt m n = (k : Integer ** (m * k = n))

divides : (m: Integer) -> (n: Integer) -> (k: Integer ** (m * k = n)) -> Integer
divides m n k = (fst k)

Pair : Type
Pair = (Integer, Integer)

Eucl: (a: Nat) -> (b: Nat) -> (Nat, Nat) --Euclidean algorithm implemented by Chinmaya
Eucl Z b = (0,0)
Eucl (S k) b = case (lte (S (S k)) b) of
                    False => (S(fst(Eucl (minus (S k) b) b)), snd(Eucl (minus (S k) b) b))
                    True => (0, S k)

gcdab : Nat -> Nat -> Nat -- Produces the GCD of two numbers. This will be useful to produce the simplified form of a rational number.
gcdab b Z = b
gcdab a b = gcdab b (snd (Eucl a b))

data NotZero : Integer -> Type where --Proof that a number is not zero, needed to construct Q
  OneNotZero : NotZero 1
  NegativeNotZero : ( n: Integer ) -> NotZero n -> NotZero (-n)
  PositiveNotZero : ( m: Integer ) -> LTE 1 (fromIntegerNat m)  -> NotZero m

make_rational : (p: Nat) -> (q: Integer) -> NotZero q -> Pair
make_rational p q x = (toIntegerNat(p), q)

InclusionMap : (n : Nat) -> Pair --Includes the naturals in Q
InclusionMap n = make_rational n 1 OneNotZero

AddRationals : (x: Pair) -> NotZero (snd x) -> (y: Pair) -> NotZero (snd y) -> Pair
AddRationals x a y b = ((fst x)*(snd y) + (snd x)*(fst y), (snd x)*(snd y))

MultiplyRationals : (x: Pair) -> NotZero (snd x) -> (y: Pair) -> NotZero (snd y) -> Pair
MultiplyRationals x a y b =((fst x)*(fst y), (snd x)*(snd y))

MultInverse : (x: Pair) -> NotZero (fst x) -> NotZero (snd x) -> Pair
MultInverse x y z = ((snd x), (fst x))

AddInverse : (x: Pair) -> NotZero (snd x) -> Pair
AddInverse x a = (-(fst x), (snd x))

Subtraction : (x: Pair) -> NotZero (snd x) -> (y: Pair) -> NotZero (snd y) -> Pair
Subtraction x a y b = AddRationals x a (AddInverse y b) b

Division : (x: Pair) -> NotZero (snd x) -> (y: Pair) -> NotZero (fst y) -> NotZero (snd y) -> Pair
Division x a y b c = MultiplyRationals x a (MultInverse y b c) b

--SimplifyRational : (x: Pair) -> NotZero (snd x) -> Pair
--SimplifyRational x a = (divides (gcdab fromIntegerNat((fst x)) fromIntegerNat((snd x))) ___ (fst x), divides (gcdab fromIntegerNat((fst x)) fromIntegerNat((snd x)) __ (snd x))

--Above, I will need to supply a proof that the GCD divides the two numbers. Then, the function defined above will produce the rational in simplified form.


text:
module Rhone.Canvas

import Control.Monad.Dom
import Data.List
import Data.SOP
import JS
import Web.Html

import public Rhone.Canvas.Angle
import public Rhone.Canvas.Scene
import public Rhone.Canvas.Shape
import public Rhone.Canvas.Style
import public Rhone.Canvas.Transformation

%default total

public export
record Canvas where
  constructor MkCanvas
  ref           : ElemRef HTMLCanvasElement
  width, height : Double
  scene         : Scene

--------------------------------------------------------------------------------
--          IO
--------------------------------------------------------------------------------

export
context2D :  LiftJSIO m
          => ElemRef HTMLCanvasElement
          -> m CanvasRenderingContext2D
context2D ref = liftJSIO $ do
  canvas <- getElementByRef ref
  m      <- getContext' canvas "2d"
  case m >>= (\ns => extract CanvasRenderingContext2D ns) of
    Just c  => pure c
    Nothing => throwError $ Caught "Rhone.Canvas.context2d: No rendering context for canvas"

export
render : LiftJSIO m => Canvas -> m ()
render (MkCanvas ref w h scene) = liftJSIO $ do
  ctxt <- context2D ref
  apply ctxt $ Rect 0 0 w h Clear
  apply ctxt scene

ext: idr


text:
module Main

import Data.List
import Data.String
import Data.String.Iterator

Show Ordering where
  show EQ = "EQ"
  show LT = "LT"
  show GT = "GT"

strings : List String
strings = [
    "abc"
  , "abcdefg"
  , "abd"
  , "zzz"
  ]
compareResults : List (String, String, Ordering)
compareResults = [
  (s1, s2, compare s1 s2) | s1 <- strings, s2 <- strings
  ]

strFun : (String -> String -> Bool) -> List (String, String, Bool)
strFun f = [
  (s1, s2, s1 `f` s2) | s1 <- strings, s2 <- strings
  ]

printRow : (String, String, Ordering) -> IO ()
printRow (s1, s2, c) = putStrLn $ "\"" ++ s1 ++ "\" `compare` \"" ++ s2 ++ "\" = " ++ show c

strOps : List (String, (String -> String -> Bool))
strOps = [
    ("< ", (<))
  , ("<=", (<=))
  , ("==", (==))
  , (">=", (>=))
  , ("> ", (>))
  ]

strMatch : String -> String
strMatch "" = "(empty)"
strMatch "abc" = "(def)"
strMatch "def" = "(ghi)"
strMatch "ghi" = "(xyz)"
strMatch _ = "(other)"

alphabet : String
alphabet = "ABCDEFGHIJKLMNOPQRSTUVWXYZ"

partial
main : IO ()
main = do
  if "hello" == "hello world" then putStrLn "equal" else putStrLn "not equal"
  traverse_ printRow compareResults
  traverse_ putStrLn [
    "\"" ++ s1 ++ "\" " ++ fst sOp ++ " \"" ++ s2 ++ "\" = " ++ show ((snd sOp) s1 s2) | s1 <- strings, s2 <- strings, sOp <- strOps
    ]
  putStrLn "substrings:"
  putStrLn (prim__strTail alphabet)
  putStrLn (substr 0 0 alphabet)
  putStrLn (substr 0 25 alphabet)
  putStrLn (substr 0 26 alphabet)
  putStrLn (substr 0 27 alphabet)
  putStrLn (substr 9 3 alphabet)
  putStrLn (substr 9 9999 alphabet)
  putStrLn (substr 9999 4 alphabet)
  putStrLn $ "neg1: " ++ (prim__strSubstr (-12) 8 alphabet)
  putStrLn $ "neg2: " ++ (prim__strSubstr 4 (-17) alphabet)
  putStrLn $ "neg3: " ++ (prim__strSubstr (-13) (-5) alphabet)
  putStrLn $ "neg4: " ++ (prim__strSubstr 28 (-4) alphabet)
  putStrLn $ "rev1: " ++ (prim__strReverse "")
  putStrLn $ "rev2: " ++ (prim__strReverse "x")
  putStrLn $ "rev3: " ++ (prim__strReverse alphabet)
  printLn $ fastUnpack "abc456@//$"
  printLn $ toList $ Iterator.unpack "abc987@//$"
  putStrLn $ strMatch $ fastPack $ unpack ""
  putStrLn $ strMatch $ fastPack $ unpack "abc"
  putStrLn $ strMatch $ fastPack $ unpack "def"
  putStrLn $ strMatch $ fastPack $ unpack "ghi"
  putStrLn $ strMatch $ fastPack $ unpack "zyx"

max_stars_repo_name: boxfire/rapid

max_issues_repo_name: boxfire/rapid

max_forks_repo_name: boxfire/rapid


text:
import Data.Vect
import Data.Fin

Vect_ext : (v : Vect n a) -> (w : Vect n a) -> ((i : Fin n) -> index i v = index i w)
  -> v = w

Weird : (v: Vect n a) -> v = v
Weird v =  Vect_ext ?hole0 ?hole1 ?hole2

f : Bool -> Nat
f True = 0
f True = ?help
f False = 1


text:
module Lists

%elim data NatPair = MkPair Nat Nat

natFst : NatPair -> Nat
natFst (MkPair a b) = a

natSnd : NatPair -> Nat
natSnd (MkPair a b) = b

pairIsSurjective : (a:Nat) -> (b:Nat) -> (MkPair a b) = (MkPair (natFst (MkPair a b)) (natSnd (MkPair a b)))
pairIsSurjective = ?pairIsSurjectiveCase

pairIsSurjective2 : (p:NatPair) -> p = MkPair (natFst p) (natSnd p)
pairIsSurjective2 = ?pairSurCase

Lists.pairSurCase = proof
  intro
  induction p
  intros
  compute
  trivial

mkNatPair : NatPair -> (Nat,Nat)
mkNatPair (MkPair a b) = (a,b)

surjectivePairingStuck : (a:NatPair) -> a = (MkPair (natFst a) (natSnd a))
surjectivePairingStuck = ?surjectivePairingStuckCase

Lists.surjectivePairingStuckCase = proof
  intros
  induction a
  compute
  intros
  trivial

%elim data NatList =
  Nil
  | Cons Nat NatList

repeat : (n:Nat) -> (count:Nat) -> NatList
repeat n Z = Nil
repeat n (S k) = Cons n (repeat n k)

length : (n:NatList) -> Nat
length Nil = Z
length (Cons x xs) = S (length xs)

app : (a:NatList) -> (b:NatList) -> NatList
app Nil b = b
app (Cons x xs) b = Cons x (app xs b)

syntax [x] "::" [xs] = Cons x xs
syntax "[ ]" = Nil
syntax "[" [x] "]" = (Cons x Nil)
syntax "[" [x] "," rem "," [y] "]" = (Cons x (app rem (Cons y Nil)))
syntax [a] "++" [b] = app a b

head : (default:Nat) -> NatList -> Nat
head n Nil = n
head n (Cons x xs) = x

tail : NatList -> NatList
tail Nil = Nil
tail (Cons x xs) = xs

filterZeros : NatList -> NatList
filterZeros Nil = Nil
filterZeros (Cons Z xs) = filterZeros xs
filterZeros (Cons n xs) = Cons n (filterZeros xs)

testFilterZeros : filterZeros $ Cons 0 (Cons 1 Nil) = (Cons 1 Nil)
testFilterZeros  = refl

oddMembers : NatList -> NatList
oddMembers Nil = Nil
oddMembers (Cons Z xs) = oddMembers xs
oddMembers (Cons x xs) = if (mod x 2) == 1
                            then Cons x (oddMembers xs)
                            else oddMembers xs

testOddMembers : oddMembers $ Cons Z (Cons 1 (Cons 2 Nil)) = (Cons 1 Nil)
testOddMembers = refl

countOddMembers : NatList -> Nat
countOddMembers xs = Lists.length $ oddMembers xs

testCountOddMembers : countOddMembers (Cons Z (Cons 1 (Cons 2 Nil))) = (S Z)
testCountOddMembers = refl

appNilEnd : (xs:NatList) -> app xs Lists.Nil = xs
appNilEnd xs = ?appNilProof

Lists.appNilProof = proof
  intro
  induction xs
  trivial
  intros
  compute
  rewrite ihn__1
  trivial

rCons : (xs:NatList) -> (i:Nat) -> NatList
rCons Nil i = Cons i Lists.Nil
rCons (Cons x xs) i = Cons x (rCons xs i)

rev : NatList -> NatList
rev Nil = Nil
rev (Cons x xs) = rCons xs x

lengthRCons : (n:Nat) -> (xs:NatList) -> length (rCons xs n) = S (length xs)
lengthRCons n xs = ?lengthRConsProof

Lists.lengthRConsProof = proof
  intros
  induction xs
  trivial
  intros
  compute
  rewrite ihn__1
  trivial

revLengthRefl : (xs:NatList) -> length (rev xs) = length xs
revLengthRefl = ?revLengthReflProof

Lists.revLengthReflProof = proof
  intros
  induction xs
  trivial
  intros
  compute
  rewrite (lengthRCons n__0 n__1)
  trivial

revRCons : (xs:NatList) -> (n:Nat) -> rev (rCons xs n) = Cons n (rev xs)
revRCons Lists.Nil n = ?revRConsBaseProof
revRCons xs n = ?revRConsSuccProof

Lists.revRConsBaseProof = proof
  intros
  trivial

revInvolutive : rev $ rev xs = xs
revInvolutive = ?revInvolutiveProof

max_stars_repo_name: joshvera/software-foundations-in-idris

max_issues_repo_name: joshvera/software-foundations-in-idris

max_forks_repo_name: joshvera/software-foundations-in-idris


text:
module Network.Curl.Easy

import public Network.Curl.Types
import public Network.Curl.Global

import Data.IORef
import Data.Buffer

import Data.List as L

-- The 'Easy Curl Interface'
{-
The easy interface is a synchronous, efficient, quickly used and... yes, easy
interface for file transfers. Numerous applications have been built using this.

When using libcurl you init your easy-session and get a handle, which you use as
input to the following interface functions you use.

You continue by setting all the options you want in the upcoming transfer, most
important among them is the URL itself. You might want to set some callbacks as
well that will be called from the library when data is available etc.

When all is setup, you tell libcurl to perform the transfer. It will then do the
entire operation and won't return until it is done or failed.

After the performance is made, you may get information about the transfer and
then you cleanup the easy-session's handle and libcurl is entirely off the hook!

-}

-- withEasy = init *> do <* cleanup

import Network.Curl.Prim

export
curlEasyInit : HasIO io => io (Maybe (CurlHandle Easy))
curlEasyInit = curl_easy_init

export
curlEasyCleanup : HasIO io => CurlHandle Easy -> io ()
curlEasyCleanup = curl_easy_cleanup

export
curlEasySetopt : HasIO io => CurlHandle Easy -> {ty : _}
              -> (opt : CurlEOption ty) -> paramType opt -> io CurlECode
curlEasySetopt = curl_easy_setopt

export
curlEasyPerform : HasIO io => CurlHandle Easy -> io CurlECode
curlEasyPerform = curl_easy_perform

stringCaptureFunc : Buffer -> Int -> IORef (List String) -> PrimIO Int
stringCaptureFunc buf len ref = toPrim $ do
  str <- getString buf 0 len
  modifyIORef ref (str ::)
  pure len

-- This function fails sometimes mysteriously in chez scheme :(
-- seems like it could be writing to a buffer before the ffi makes it?
export
partial
||| Plain jane fetch a url and put the response body into a String
easyFetchUrl : HasIO io => (url : String) -> io (Either CurlECode String)
easyFetchUrl url = do
    CURLE_OK <- curlGlobalInit
      | err => pure $ Left err
    Just eh <- curlEasyInit
      | Nothing => idris_crash "curl easy init failed!"
    CURLE_OK <- curlEasySetopt eh CURLOPT_URL url
      | err => pure $ Left err
    ref <- newIORef []
    CURLE_OK <- curlEasySetopt eh CURLOPT_WRITEFUNCTION
        (\buf,_,len,_ => stringCaptureFunc buf len ref)
      | err => pure $ Left err
    CURLE_OK <- curlEasyPerform eh
      | err => pure $ Left err
    d <- concat . L.reverse <$> readIORef ref
    curlEasyCleanup eh
    curlGlobalCleanup
    pure (Right d)


text:
checkEqNat : (num1 : Nat) -> (num2 : Nat) -> Maybe (num1 = num2)
checkEqNat 0 0 = Just Refl
checkEqNat 0 (S k) = Nothing
checkEqNat (S k) 0 = Nothing
checkEqNat (S k) (S j) = case checkEqNat k j of
                              Nothing => Nothing
                              Just prf => Just (cong S prf)

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

exactLength : {m : _} -> (len : Nat) -> (input : Vect m a) -> Maybe (Vect len a)
exactLength len input = case checkEqNat m len of
                             Nothing => Nothing
                             Just prf => Just ?something


text:
module Replica.App.Run

import Control.ANSI
import Control.App
import Control.App.Console

import Data.Either
import Data.List
import Data.List1
import Data.Maybe
import Data.String
import Data.String.Extra

import Language.JSON

import System.Future
import System.Path

import Replica.App.FileSystem
import Replica.App.Format
import Replica.App.Log
import Replica.App.Replica
import Replica.App.Run.Dependencies
import Replica.App.System

import Replica.Command.Run
import Replica.Core.Parse
import Replica.Core.Types
import Replica.Option.Global
import Replica.Other.Decorated
import Replica.Other.String
import Replica.Other.Validation

%default total

data RunContext : Type where

record TestOutput where
  constructor MkTestOutput
  status : Int
  std : String
  file : Maybe String

normalize : String -> String
normalize = unlines . map unwords . filter (not . force . null) . map (assert_total words) . forget . lines

-- Create the folders needed by Replica (usually ./.replica/test and ./.replica/log)
prepareReplicaDir : SystemIO (SystemError :: e) =>
  FileSystem (FSError :: e) =>
  Has [ State RunContext RunCommand
      , State GlobalConfig Global
      , Exception ReplicaError
      , Console
      ] e => App e String
prepareReplicaDir = do
  debug $ "GlobalConfig: \{!(show <$> get GlobalConfig)}"
  catchNew setAbsoluteReplicaDir
    (\err : FSError => throw $ CantAccessTestFile "current directory")
  rDir <- getReplicaDir
  log "Replica directory: \{rDir}"
  debug "Creating test directory: \{testDir rDir}"
  catchNew (system "mkdir -p \{show (testDir rDir)}")
    (\err : SystemError => throw $ CantAccessTestFile "\{show (testDir rDir)}")
  debug "Creating log directory: \{testDir rDir}"
  catchNew (system "mkdir -p \{show (logDir rDir)}")
    (\err : SystemError => throw $ CantAccessTestFile "\{show (logDir rDir)}")
  pure rDir

runAll :
  SystemIO (SystemError :: e) =>
  State GlobalConfig Global e =>
  Exception TestError e =>
  Console e =>
  (phase : Maybe String) ->
  (String -> TestError) ->
  List String -> App e ()
runAll phase liftError [] = pure ()
runAll phase liftError (x :: xs) = do
  maybe (pure ()) (\p => log "\{p}: \{x}") phase
  handle (system "(\{x}) 1> /dev/null 2> /dev/null")
    (const $ runAll phase liftError xs)
    (\err : SystemError => throw $ liftError x)

expectedVsGiven : State GlobalConfig Global e =>
  Nat -> String -> String -> App e (List String)
expectedVsGiven k expected given = pure $ map (withOffset k) $
  ( "Expected:" :: map !red (forget $ lines expected)) ++
  ( "Given:" :: map !green (forget $ lines given))

nativeShow : State GlobalConfig Global e =>
  Console e => String -> String -> App e ()
nativeShow expected given =
  putStrLn $ unlines !(expectedVsGiven 0 expected given)

-- Provide different ways to show the difference between expectations and givens
showDiff : SystemIO (SystemError :: e) =>
  State GlobalConfig Global e =>
  State CurrentTest Test e =>
  Console e => DiffCommand -> String -> String -> App e ()
showDiff Native expected given = nativeShow expected given
showDiff Diff x y = catchNew
  (system $ "git diff --minimal --word-diff=color --no-index -- \{!getExpectedOutput} \{!getOutputFile}")
  (\err : SystemError => nativeShow x y)
showDiff GitDiff x y = catchNew
  (system $ "git diff --minimal --word-diff=color --no-index -- \{!getExpectedOutput} \{!getOutputFile}")
  (\err : SystemError => nativeShow x y)
showDiff (Custom z) x y = catchNew
  (system $ "\{z} \{!getExpectedOutput} \{!getOutputFile}")
  (\err : SystemError => nativeShow x y)

-- on mismatch, check if we should replace the golden value
interactiveGolden : SystemIO (SystemError :: e) =>
  FileSystem (FSError :: e) =>
  Has [ State CurrentTest Test
      , State GlobalConfig Global
      , Exception TestError
      , Console
      ] e =>
  (source : Maybe String) ->
  (given : String) ->
  (expected : Maybe String) ->
  App e (Maybe FailReason)
interactiveGolden source given expected = do
  t <- get CurrentTest
  putStrLn $ "\{t.name}: Golden value mismatch for \{maybe "standard output" ("file " ++) source}"
  showExpectedAndGiven
  putStrLn $ "Do you want to \{maybe "set" (const "replace") expected} the golden value? [N/y]"
  if !readAnswer
     then do
       f <- expectedFile
       handle (writeFile f given)
         (const $ pure Nothing)
         (\err : FSError => throw $ FileSystemError "Cannot write golden value")
     else pure . Just $ maybe
       (WrongOutput source (GoldenIsMissing given))
       (WrongOutput source . flip DifferentOutput given)
       expected
  where

    expectedFile : App e String
    expectedFile = maybe getExpectedOutput (const getExpectedFile) source

    readAnswer : App e Bool
    readAnswer = do
      answer <- getLine
      pure $ toLower answer `elem` ["y", "yes"]

    showExpectedAndGiven : App e ()
    showExpectedAndGiven = do
      let Just str = expected
        | _ => do
          putStrLn "Expected: Nothing Found"
          putStrLn "Given:"
          putStrLn given
      showDiff !(diff <$> get GlobalConfig) str given

getExpected : FileSystem (FSError :: e) =>
  Has [ State RunContext RunCommand
      , Exception TestError
      , Console
      ] e => String -> App e (Maybe String)
getExpected src= do
  handle (readFile src)
    (pure . Just)
    (\err : FSError => case err of
        MissingFile _ => pure Nothing
        err => throw $ FileSystemError "Cannot read expectation")

checkPartial : (ordered : OrderSensitive) -> (xs : List String) ->
               (given : String) ->
               Maybe FailReason
checkPartial Ordered [] given = Nothing
checkPartial Ordered (x :: xs) given = do
  let (s::_) = unpack x
      | [] => checkPartial Ordered xs given
  case break (== s) given of
       (_, "") => Just $ WrongOutput Nothing (PartialOutputMismatch Ordered (x::xs) given)
       (_, str) => if isPrefixOf x str
                      then checkPartial Ordered xs (assert_smaller given $ drop (length x) str)
                      else checkPartial Ordered (x::xs) (assert_smaller given $ drop 1 str)

checkPartial Whatever xs given = let
  errors = catMaybes $ map (\exp => guard (not $ isInfixOf exp given) $> exp) xs
  in case errors of
          [] => Nothing
          _  => Just $ WrongOutput Nothing (PartialOutputMismatch Whatever errors given)

checkOutput : SystemIO (SystemError :: e) =>
  FileSystem (FSError :: e) =>
  Has [ State CurrentTest Test
      , State GlobalConfig Global
      , State RunContext RunCommand
      , Exception TestError
      , Console ] e =>
  (source : Maybe String) ->
  (given : String) ->
  App e (Maybe (FailReason, Maybe (App e (Maybe FailReason))))
checkOutput source given = do
  t <- get CurrentTest
  let Generated = maybe t.expectation (const Generated) source
       | Exact expected => noInteractionOnFailure $
                             checkExact t.spaceSensitive expected given
       | Partial x xs => noInteractionOnFailure $ checkPartial' t.spaceSensitive x xs given
  Just expected <- getExpected $ maybe !getExpectedOutput (const !getExpectedFile) source
    | Nothing => interactiveFailure Nothing $ Just $ WrongOutput source (GoldenIsMissing given)
  interactiveFailure (Just expected) $ checkExact t.spaceSensitive expected given
  where
    checkExact : (spaceSensitive : Bool) -> (expected, given : String) -> Maybe FailReason
    checkExact spaceSensitive expected given = let
      e : String = if spaceSensitive then expected else normalize expected
      g : String = if spaceSensitive then given else normalize given
      in guard (e /= g) $> WrongOutput source (DifferentOutput expected given)
    checkPartial' : (spaceSensitive : Bool) -> (o : OrderSensitive) ->
                    (expected : List String) -> (given : String) -> Maybe FailReason
    checkPartial' spaceSensitive o expected given = let
      e : List String = if spaceSensitive then expected else map normalize expected
      g : String = if spaceSensitive then given else normalize given
      in checkPartial o e g
    noInteractionOnFailure : Maybe FailReason ->
      App e (Maybe (FailReason, Maybe (App e (Maybe FailReason))))
    noInteractionOnFailure = pure . map (flip MkPair Nothing)
    interactiveFailure :
      Maybe String ->
      Maybe FailReason ->
      App e (Maybe (FailReason, Maybe (App e (Maybe FailReason))))
    interactiveFailure expected =
      pure . map (flip MkPair (Just $ interactiveGolden source given expected))

checkStatus : Maybe Bool -> Int -> Maybe FailReason
checkStatus Nothing y = Nothing
checkStatus (Just True) y = guard (y /= 0) $> WrongStatus True
checkStatus (Just False) y = guard (y == 0) $> WrongStatus False

checkExpectations :  SystemIO (SystemError :: e) =>
  FileSystem (FSError :: e) =>
  Has [ State CurrentTest Test
      , State GlobalConfig Global
      , State RunContext RunCommand
      , Exception TestError
      , Console ] e =>
  (ouputs : TestOutput) ->
  App e TestResult
checkExpectations outputs = do
  t <- get CurrentTest
  ctx <- get RunContext
  let statusFailure = checkStatus t.mustSucceed outputs.status
  stdFailure <- checkOutput Nothing outputs.std
  fileFailure <- maybe (pure Nothing) (checkOutput t.file) outputs.file
  let failures = catMaybes [statusFailure, fst <$> stdFailure, fst <$> fileFailure]
  debug $ withOffset 4 "Check success"
  let (x :: xs) = failures
    | _ => pure Success
  let Nothing = statusFailure
    | _ => pure $ Fail failures
  debug $ withOffset 4
        "Check interactive: \{show $ isNothing statusFailure} \{show ctx.interactive}"
  let (Nothing, True) = (statusFailure, ctx.interactive)
    | _ =>  pure $ Fail failures
  stdFinalFailure <- do
    Just (_, Just newF) <- pure stdFailure
      | e => pure $ fst <$> e
    newF
  fileFinalFailure <- do
    Just (_, Just newF) <- pure fileFailure
      | e => pure $ fst <$> e
    newF
  let (x :: xs) = catMaybes [statusFailure, stdFinalFailure, fileFinalFailure]
    | _ => pure Success
  pure $ Fail (x :: xs)

generateInput : FileSystem (FSError :: e) =>
      Has [ State CurrentTest Test
          , State GlobalConfig Global
          , Exception TestError ] e =>
      App e (Maybe String)
generateInput = do
  Just input <- input <$> get CurrentTest
    | _ => pure Nothing
  f <- getInputFile
  catchNew (writeFile f input)
    (\e : FSError => throw $ FileSystemError "Can't write input file \{f}")
  pure (Just f)

collectOutputs : SystemIO (SystemError :: e) =>
  FileSystem (FSError :: e) =>
  Has [ State CurrentTest Test
      , State GlobalConfig Global
      , State RunContext RunCommand
      , Exception TestError
      , Console
      ] e => App e (Either TestResult TestOutput)
collectOutputs = do
  t <- get CurrentTest
  debug $ withOffset 2 "Check pending"
  let False = t.pending
    | True => pure $ Left Skipped
  outputFile <- getOutputFile
  exitStatus <- runCommand outputFile
  output <- catchNew (readFile $ outputFile)
    (\e : FSError => throw $
          FileSystemError "Can't read output file \{outputFile}")
  let Just f = t.file
    | Nothing => pure $ Right $  MkTestOutput exitStatus output Nothing
  Just fileContent <- catchNew (Just <$> readFile f) (\err : FSError => pure Nothing)
    | Nothing => pure $ Left $ Fail [ExpectedFileNotFound f]
  pure $ Right $ MkTestOutput exitStatus output (Just fileContent)
  where
    runCommand : String -> App e Int
    runCommand outputFile = do
      t <- get CurrentTest
      inputFile <- generateInput
      let cmd = "(\{t.command}) \{maybe "" ("< " ++ )inputFile} > \"\{outputFile}\""
      log $ withOffset 2 "Running command: \{cmd}"
      handle (system cmd) (const $ pure 0) (\(Err n) => pure n)

testCore : SystemIO (SystemError :: e) =>
  FileSystem (FSError :: e) =>
  Has [ State CurrentTest Test
      , State GlobalConfig Global
      , State RunContext RunCommand
      , Exception TestError
      , Console
      ] e => App e TestResult
testCore = do

  Right outputs <- collectOutputs
    | Left res => pure res
  checkExpectations outputs

-- the whole test execution, including pre and post operation
performTest : SystemIO (SystemError :: e) =>
  FileSystem (FSError :: e) =>
  Has [ State CurrentTest Test
      , State GlobalConfig Global
      , State RunContext RunCommand
      , Exception TestError
      , Console
      ] e => App e TestResult
performTest = do
  t <- get CurrentTest
  runAll (Just "Before") InitializationFailed t.beforeTest
  res <- testCore
  runAll (Just "After") (WrapUpFailed res) t.afterTest
  pure res

-- move to the right directory and perform the test
runTest : SystemIO (SystemError :: e) =>
  FileSystem (FSError :: e) =>
  Has [ State CurrentTest Test
      , State RunContext RunCommand
      , State GlobalConfig Global
      , Exception TestError
      , Console
      ] e => App e TestResult
runTest = do
  ctx <- get RunContext
  t <- get CurrentTest
  createTestDir
  let wd = fromMaybe ctx.workingDir t.workingDir
  log "Executing \{t.name}"
  debug $ withOffset 2 $ show t
  log   $ withOffset 2 "Working directory: \{show wd}"
  catchNew (inDir wd performTest)
    (\err : FSError => throw $ FileSystemError
      "Error: cannot enter or exit test working directory \{show wd}")
  where
    inDir : (dir : String) -> App e a -> App (FSError :: e) a
    inDir dir exec = do
      pwd <- getCurrentDir
      changeDir dir
      Right res <- lift $ catch (Right <$> exec)
                                (\err : TestError => pure $ Left err)
        | Left err => changeDir pwd >> lift (throw err)
      changeDir pwd
      pure res
    continueIfExists : FSError -> App e ()
    continueIfExists (FileExists _) = pure ()
    continueIfExists _ = throw $ FileSystemError "Cant't create or accesse test directory"
    createTestDir : App e ()
    createTestDir = do
      testDir <- getSingleTestDir
      catchNew (createDir testDir) continueIfExists

testOutput :
  Has [ State RunContext RunCommand
      , State GlobalConfig Global
      , Console
      ] e => String -> Either TestError TestResult -> App e ()
testOutput name (Left y) = do
  putStr (withOffset 2 $ (!yellow "\{!err} \{name}: "))
  putStrLn (displayTestError y)
testOutput name (Right Skipped) =
   putStrLn $ withOffset 2 "\{!pending} \{name}"
testOutput name (Right Success) = do
  if !(hideSuccess <$> get RunContext)
     then pure ()
     else putStrLn $ withOffset 2 "\{!ok} \{name}"
testOutput name (Right (Fail xs)) = do
  putStrLn $ withOffset 2 $ !red "\{!ko} \{name}: \{unwords $ map displayFailReason xs}"
  let Just (expected, given) = getContentMismatch xs
    | Nothing => pure ()
  putStrLn $ unlines !(expectedVsGiven 6 expected given)
  where
    getContentMismatch : List FailReason -> Maybe (String, String)
    getContentMismatch [] = Nothing
    getContentMismatch (WrongOutput src (DifferentOutput x y) :: _) = Just (x, y)
    getContentMismatch (_ :: xs) = getContentMismatch xs

runAllTests : SystemIO (SystemError :: TestError :: e) =>
  SystemIO (SystemError :: e) =>
  FileSystem (FSError :: TestError :: e) =>
  Console (TestError :: e) =>
  Has [ State RunContext RunCommand
      , State GlobalConfig Global
      , Console
      ] e =>  TestPlan -> App e (List (String, Either TestError TestResult))
runAllTests plan = do
  putStrLn $ separator 80
  putStrLn $ !bold "Running tests..."
  batchTests [] plan
  where
    processTest : Test -> App e (String, Either TestError TestResult)
    processTest x = do

      rdir <- getReplicaDir
      let False = x.pending
        | True => pure (x.name, Right Skipped)
      r <- handle
             (new x runTest)
             (pure . MkPair x.name . Right)
             (\err : TestError => pure (x.name, Left err))
      pure r
    prepareBatch : Nat -> TestPlan -> (List Test, List Test)
    prepareBatch n plan = if n == 0
                             then (plan.now, Prelude.Nil)
                             else splitAt n plan.now
    processResult : TestPlan -> (String, Either TestError TestResult) -> TestPlan
    processResult plan (tName, Right Success) = validate tName plan
    processResult plan (tName, _) = fail tName plan
    batchTests : List (String, Either TestError TestResult) ->
                 TestPlan -> App e (List (String, Either TestError TestResult))
    batchTests acc plan = do
      n <- threads <$> get RunContext
      case prepareBatch n plan of
           ([], later) => pure $ join
              [ acc
              , map (\t => (t.name, Left Inaccessible)) plan.later
              , map (\(reason, t) => (t.name, Left $ RequirementsFailed reason)) plan.skipped
              ]
           (now, nextBatches) => do
             res <- map await <$> traverse (map (fork . delay) . processTest) now
             when (not !(interactive <$> get RunContext))
               (traverse_ (uncurry testOutput) res)
             p <- punitive <$> get RunContext
             if p && any (not . isFullSuccess . snd) res
                then pure res
                else do
                   let plan' = record {now = nextBatches} plan
                   debug $ displayPlan plan'
                   batchTests (acc ++ res) $ assert_smaller plan (foldl processResult plan' res)

report : Console e => State GlobalConfig Global e => Stats -> App e ()
report x = do
  putStrLn $ separator 80
  putStrLn $ !bold "Summary:"
  let nb = countTests x
  if nb == 0
     then putStrLn $ withOffset 2 "No test"
     else putStrLn $ unlines $ catMaybes
    [ guard (x.successes > 0) $>
        withOffset 2 "\{!ok} (Success): \{show x.successes} / \{show nb}"
    , guard (x.failures > 0) $>
        withOffset 2 "\{!ko} (Failure): \{show x.failures} / \{show nb}"
    , guard (x.errors > 0) $>
        withOffset 2 "\{!err}  (Errors): \{show x.errors} / \{show nb}"
    , guard (x.skipped > 0) $>
        withOffset 2 "\{!pending}  (Pending): \{show x.skipped} / \{show nb}"
    ]

filterTests : FileSystem (FSError :: e) =>
  Has [ State RunContext RunCommand
      , State GlobalConfig Global
      , Exception ReplicaError
      , Console
      ] e => (s, r : List Test) -> App e TestPlan
filterTests s r = do
  f <- filter <$> get RunContext
  debug $ "Filters: \{show f}"
  let (selected, rejected) = partition (keepTest f) s
  pure $ foldl (\p, t => validate t.name p) (buildPlan selected) (r ++ rejected)

getLastFailures : FileSystem (FSError :: e) =>
  Has [ State GlobalConfig Global
      , Exception ReplicaError
      , Console
      ] e => App e (List Test, List Test)
getLastFailures = do
  repl <- getReplica
  logFile <- lastRunLog <$> getReplicaDir
  lastLog <- catchNew (readFile logFile)
    (\err : FSError => throw $ CantAccessTestFile logFile)
  let Just json = parse lastLog
    | Nothing => throw $ InvalidJSON ["Can't parse JSON (invalid syntax)"]
  let Valid report = parseReport json
    | Error err => throw $ InvalidJSON err
  let notWorking = fst <$> filter (not . isFullSuccess . snd) report
  let (selected, rejected) = partition (flip elem notWorking . name) repl.tests
  debug $ "Previous invalid tests: \{show selected}"
  pure (selected, rejected)

defineActiveTests : FileSystem (FSError :: e) =>
  Has [ State RunContext RunCommand
      , State GlobalConfig Global
      , Exception ReplicaError
      , Console
      ] e => App e TestPlan
defineActiveTests = do
  last <- if !((.filter.lastFailures) <$> get RunContext)
        then getLastFailures
        else do
          repl <- getReplica
          pure (repl.tests, [])
  uncurry filterTests last

export
runReplica : SystemIO (SystemError :: TestError :: e) =>
  SystemIO (SystemError :: e) =>
  FileSystem (FSError :: TestError :: e) =>
  FileSystem (FSError :: e) =>
  Console (TestError :: e) =>
  Has [ State RunContext RunCommand
      , State GlobalConfig Global
      , Exception ReplicaError
      , Console
      ] e => App e Stats
runReplica = do
  debug $ "Run: \{show !(get RunContext)}"
  rDir <- prepareReplicaDir
  plan <- defineActiveTests
  log $ displayPlan plan
  result <- runAllTests plan
  let logFile = lastRunLog rDir
  catchNew (writeFile logFile (show $ reportToJSON result))
    (\err : FSError => throw $ CantAccessTestFile logFile)
  when !(interactive <$> get RunContext)
    (do putStrLn $ separator 80
        putStrLn $ !bold "Test results:"
        traverse_ (uncurry testOutput) result)
  let stats = asStats $ snd <$> result
  report $ stats
  pure stats

max_stars_repo_name: teto/REPLica

max_issues_repo_name: teto/REPLica

max_forks_repo_name: teto/REPLica


text:
module VectMissing

using (x : a, xs : Vect n a)
  data IsElem : a -> Vect n a -> Type where
       First : IsElem x (x :: xs)
       Later : IsElem x xs -> IsElem x (y :: xs)

  instance Uninhabited (IsElem x []) where
    uninhabited First impossible
    uninhabited (Later p) impossible

  isElem : DecEq a => (x : a) -> (xs : Vect n a) -> Maybe (IsElem x xs)
  isElem x [] = Nothing
  isElem x (y :: xs) with (decEq x y)
    isElem x (x :: xs) | (Yes refl) = Just First
    isElem x (y :: xs) | (No f) = Just (Later !(isElem x xs))

  shrink : (xs : Vect (S n) a) -> IsElem x xs -> Vect n a
  shrink (x :: ys) First = ys
  shrink (y :: []) (Later p) = absurd p
  shrink (y :: (x :: xs)) (Later p) = y :: shrink (x :: xs) p

max_stars_repo_name: silky/idris-demos

max_issues_repo_name: silky/idris-demos

max_forks_repo_name: silky/idris-demos


text:
-- -------------------------------------------------------------- [ Parser.idr ]
-- Module      : UML.Code.Parser
-- Description :
-- Copyright   : (c) Jan de Muijnck-Hughes
-- License     : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
module UML.Code.Parser

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

import UML.Code.Model
import UML.Utils.Parsing

%access public

-- -------------------------------------------------------------------- [ Data ]
attr : Parser (String, String)
attr = do
    n <- ident <* space
    colon
    ty <- ident <* space
    pure $ MkPair n ty
  <?> "Parse Attribute"

simpleDtype : Parser DType
simpleDtype = do
    token "data"
    id <- ident <* space
    pure $ MkSType id
   <?> "Simple Data Type"

complexDtype : Parser DType
complexDtype = do
    token "data"
    id <- ident <* space
    body <- braces (commaSep1 (attr <* space) <* space)
    pure $ MkCType id body
   <?> "Complex Data Type"

dtype : Parser DType
dtype = complexDtype <|> simpleDtype <?> "Data Types"

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

paramfunc : Parser Function
paramfunc = do
    id <- ident <* space
    colon
    ps <- some (parens attr <* token "->")
    rty <- ident <* space
    pure $ MkPFunc id ps rty
  <?> "Func with parameters"

noparamfunc : Parser Function
noparamfunc = do
    id <- ident <* space
    colon
    rty <- ident
    pure $ MkFunc id rty

funcs : Parser Function
funcs = paramfunc <|> noparamfunc

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

max_stars_repo_name: jfdm/idris-uml

max_issues_repo_name: jfdm/idris-uml

max_forks_repo_name: jfdm/idris-uml


text:
module Spacing

id : {n : Nat} -> Nat
id {  n} = ?a


text:
plus' : Nat -> Nat -> Nat
plus' Z     y = y
plus' (S k) y = S (plus' k y)

mult' : Nat -> Nat -> Nat
mult' Z     y = Z
mult' (S k) y = plus' y (mult' k y)


text:
total
data Foo : Type where
  MkFoo : (Foo -> Foo) -> Foo


text:
module Network.TLS.Magic

import Data.Vect
import Network.TLS.Parsing
import Network.TLS.AEAD
import Utils.Bytes
import Utils.Misc
import Crypto.Hash
import Crypto.ECDH
import Crypto.Curve
import Crypto.Curve.Weierstrass
import Generics.Derive

%language ElabReflection

-- in TLS 1.3, the severity is implicit in the type of alert being sent, and the "level" field can safely be ignored
public export
data AlertLevel : Type where
  Warning : AlertLevel
  Fatal : AlertLevel

%runElab derive "AlertLevel" [Generic, Meta, Eq, Show]

public export
alert_level_to_id : AlertLevel -> Bits8
alert_level_to_id Warning = 1
alert_level_to_id Fatal = 2

public export
id_to_alert_level : Bits8 -> Maybe AlertLevel
id_to_alert_level 1 = Just Warning
id_to_alert_level 2 = Just Warning
id_to_alert_level _ = Nothing

public export
data AlertDescription : Type where
  CloseNotify : AlertDescription
  UnexpectedMessage : AlertDescription
  BadRecordMac : AlertDescription
  RecordOverflow : AlertDescription
  HandshakeFailure : AlertDescription
  BadCertificate : AlertDescription
  UnsupportedCertificate : AlertDescription
  CertificateRevoked : AlertDescription
  CertificateExpired : AlertDescription
  CertificateUnknown : AlertDescription
  IllegalParameter : AlertDescription
  UnknownCA : AlertDescription
  AccessDenied : AlertDescription
  DecodeError : AlertDescription
  DecryptError : AlertDescription
  ProtocolVersion : AlertDescription
  InsufficientSecurity : AlertDescription
  InternalError : AlertDescription
  InappropriateFallback : AlertDescription
  UserCanceled : AlertDescription
  MissingExtension : AlertDescription
  UnsupportedExtension : AlertDescription
  UnrecognizedName : AlertDescription
  BadCertificateStatusResponse : AlertDescription
  UnknownPskIdentity : AlertDescription
  CertificateRequired : AlertDescription
  NoApplicationProtocol : AlertDescription

%runElab derive "AlertDescription" [Generic, Meta, Eq, Show]

public export
alert_description_to_id : AlertDescription -> Bits8
alert_description_to_id CloseNotify = 0
alert_description_to_id UnexpectedMessage = 10
alert_description_to_id BadRecordMac = 20
alert_description_to_id RecordOverflow = 22
alert_description_to_id HandshakeFailure = 40
alert_description_to_id BadCertificate = 42
alert_description_to_id UnsupportedCertificate = 43
alert_description_to_id CertificateRevoked = 44
alert_description_to_id CertificateExpired = 45
alert_description_to_id CertificateUnknown = 46
alert_description_to_id IllegalParameter = 47
alert_description_to_id UnknownCA = 48
alert_description_to_id AccessDenied = 49
alert_description_to_id DecodeError = 50
alert_description_to_id DecryptError = 51
alert_description_to_id ProtocolVersion = 70
alert_description_to_id InsufficientSecurity = 71
alert_description_to_id InternalError = 80
alert_description_to_id InappropriateFallback = 86
alert_description_to_id UserCanceled = 90
alert_description_to_id MissingExtension = 109
alert_description_to_id UnsupportedExtension = 110
alert_description_to_id UnrecognizedName = 112
alert_description_to_id BadCertificateStatusResponse = 113
alert_description_to_id UnknownPskIdentity = 115
alert_description_to_id CertificateRequired = 116
alert_description_to_id NoApplicationProtocol = 120

public export
id_to_alert_description : Bits8 -> Maybe AlertDescription
id_to_alert_description 0 = Just CloseNotify
id_to_alert_description 10 = Just UnexpectedMessage
id_to_alert_description 20 = Just BadRecordMac
id_to_alert_description 22 = Just RecordOverflow
id_to_alert_description 40 = Just HandshakeFailure
id_to_alert_description 42 = Just BadCertificate
id_to_alert_description 43 = Just UnsupportedCertificate
id_to_alert_description 44 = Just CertificateRevoked
id_to_alert_description 45 = Just CertificateExpired
id_to_alert_description 46 = Just CertificateUnknown
id_to_alert_description 47 = Just IllegalParameter
id_to_alert_description 48 = Just UnknownCA
id_to_alert_description 49 = Just AccessDenied
id_to_alert_description 50 = Just DecodeError
id_to_alert_description 51 = Just DecryptError
id_to_alert_description 70 = Just ProtocolVersion
id_to_alert_description 71 = Just InsufficientSecurity
id_to_alert_description 80 = Just InternalError
id_to_alert_description 86 = Just InappropriateFallback
id_to_alert_description 90 = Just UserCanceled
id_to_alert_description 109 = Just MissingExtension
id_to_alert_description 110 = Just UnsupportedExtension
id_to_alert_description 112 = Just UnrecognizedName
id_to_alert_description 113 = Just BadCertificateStatusResponse
id_to_alert_description 115 = Just UnknownPskIdentity
id_to_alert_description 116 = Just CertificateRequired
id_to_alert_description 120 = Just NoApplicationProtocol
id_to_alert_description _ = Nothing

public export
data SupportedGroup : Type where
  X25519 : SupportedGroup
  X448 : SupportedGroup
  SECP256r1 : SupportedGroup
  SECP384r1 : SupportedGroup
  SECP521r1 : SupportedGroup

%runElab derive "SupportedGroup" [Generic, Meta, Eq, Show]

public export
supported_group_to_id : SupportedGroup -> (Bits8, Bits8)
supported_group_to_id X25519 = (0x00, 0x1d)
supported_group_to_id X448 = (0x00, 0x1e)
supported_group_to_id SECP256r1 = (0x00, 0x17)
supported_group_to_id SECP384r1 = (0x00, 0x18)
supported_group_to_id SECP521r1 = (0x00, 0x19)

public export
id_to_supported_group : (Bits8, Bits8) -> Maybe SupportedGroup
id_to_supported_group (0x00, 0x1d) = Just X25519
id_to_supported_group (0x00, 0x1e) = Just X448
id_to_supported_group (0x00, 0x17) = Just SECP256r1
id_to_supported_group (0x00, 0x18) = Just SECP384r1
id_to_supported_group (0x00, 0x19) = Just SECP521r1
id_to_supported_group _ = Nothing

public export
curve_group_to_type : SupportedGroup -> (DPair Type ECDHCyclicGroup)
curve_group_to_type X25519 = MkDPair X25519_DH %search
curve_group_to_type X448 = MkDPair X448_DH %search
curve_group_to_type SECP256r1 = MkDPair P256 %search
curve_group_to_type SECP384r1 = MkDPair P384 %search
curve_group_to_type SECP521r1 = MkDPair P521 %search

public export
curve_group_to_scalar_type : SupportedGroup -> Type
curve_group_to_scalar_type group = Scalar @{snd $ curve_group_to_type group}

public export
curve_group_to_element_type : SupportedGroup -> Type
curve_group_to_element_type group = Element @{snd $ curve_group_to_type group}

public export
data SignatureAlgorithm : Type where
  RSA_PKCS1_SHA256       : SignatureAlgorithm
  RSA_PKCS1_SHA384       : SignatureAlgorithm
  RSA_PKCS1_SHA512       : SignatureAlgorithm

  ECDSA_SECP256r1_SHA256 : SignatureAlgorithm
  ECDSA_SECP384r1_SHA384 : SignatureAlgorithm
  ECDSA_SECP521r1_SHA512 : SignatureAlgorithm

  RSA_PSS_RSAE_SHA256    : SignatureAlgorithm
  RSA_PSS_RSAE_SHA384    : SignatureAlgorithm
  RSA_PSS_RSAE_SHA512    : SignatureAlgorithm

%runElab derive "SignatureAlgorithm" [Generic, Meta, Eq, Show]

public export
signature_algorithm_to_id : SignatureAlgorithm -> (Bits8, Bits8)
signature_algorithm_to_id RSA_PKCS1_SHA256 = (0x04, 0x01)
signature_algorithm_to_id RSA_PKCS1_SHA384 = (0x05, 0x01)
signature_algorithm_to_id RSA_PKCS1_SHA512 = (0x06, 0x01)

signature_algorithm_to_id ECDSA_SECP256r1_SHA256 = (0x04, 0x03)
signature_algorithm_to_id ECDSA_SECP384r1_SHA384 = (0x05, 0x03)
signature_algorithm_to_id ECDSA_SECP521r1_SHA512 = (0x06, 0x03)

signature_algorithm_to_id RSA_PSS_RSAE_SHA256 = (0x08, 0x04)
signature_algorithm_to_id RSA_PSS_RSAE_SHA384 = (0x08, 0x05)
signature_algorithm_to_id RSA_PSS_RSAE_SHA512 = (0x08, 0x06)

public export
id_to_signature_algorithm : (Bits8, Bits8) -> Maybe SignatureAlgorithm
id_to_signature_algorithm (0x04, 0x01) = Just RSA_PKCS1_SHA256
id_to_signature_algorithm (0x05, 0x01) = Just RSA_PKCS1_SHA384
id_to_signature_algorithm (0x06, 0x01) = Just RSA_PKCS1_SHA512

id_to_signature_algorithm (0x04, 0x03) = Just ECDSA_SECP256r1_SHA256
id_to_signature_algorithm (0x05, 0x03) = Just ECDSA_SECP384r1_SHA384
id_to_signature_algorithm (0x06, 0x03) = Just ECDSA_SECP521r1_SHA512

id_to_signature_algorithm (0x08, 0x04) = Just RSA_PSS_RSAE_SHA256
id_to_signature_algorithm (0x08, 0x05) = Just RSA_PSS_RSAE_SHA384
id_to_signature_algorithm (0x08, 0x06) = Just RSA_PSS_RSAE_SHA512

id_to_signature_algorithm _ = Nothing

public export
data CompressionLevel : Type where
  Null : CompressionLevel

%runElab derive "CompressionLevel" [Generic, Meta, Eq, Show]

public export
compression_level_to_id : CompressionLevel -> Bits8
compression_level_to_id Null = 0x00

public export
id_to_compression_level : Bits8 -> Maybe CompressionLevel
id_to_compression_level 0x00 = Just Null
id_to_compression_level _ = Nothing

public export
data CipherSuite : Type where
  ||| TLS 1.3 Cipher Suites
  TLS_AES_128_GCM_SHA256 : CipherSuite
  TLS_AES_256_GCM_SHA384 : CipherSuite
  TLS_CHACHA20_POLY1305_SHA256 : CipherSuite
  ||| TLS 1.2 Cipher Suites
  TLS_ECDHE_RSA_WITH_AES_128_GCM_SHA256 : CipherSuite
  TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384 : CipherSuite
  TLS_ECDHE_ECDSA_WITH_AES_128_GCM_SHA256 : CipherSuite
  TLS_ECDHE_ECDSA_WITH_AES_256_GCM_SHA384 : CipherSuite
  TLS_ECDHE_RSA_WITH_CHACHA20_POLY1305_SHA256 : CipherSuite
  TLS_ECDHE_ECDSA_WITH_CHACHA20_POLY1305_SHA256 : CipherSuite

%runElab derive "CipherSuite" [Generic, Meta, Eq, Show]

public export
cipher_suite_to_id : CipherSuite -> (Bits8, Bits8)
cipher_suite_to_id TLS_AES_128_GCM_SHA256 = (0x13, 0x01)
cipher_suite_to_id TLS_AES_256_GCM_SHA384 = (0x13, 0x02)
cipher_suite_to_id TLS_CHACHA20_POLY1305_SHA256 = (0x13, 0x03)
cipher_suite_to_id TLS_ECDHE_RSA_WITH_AES_128_GCM_SHA256 = (0xc0, 0x2f)
cipher_suite_to_id TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384 = (0xc0, 0x30)
cipher_suite_to_id TLS_ECDHE_ECDSA_WITH_AES_128_GCM_SHA256 = (0xc0, 0x2b)
cipher_suite_to_id TLS_ECDHE_ECDSA_WITH_AES_256_GCM_SHA384 = (0xc0, 0x2c)
cipher_suite_to_id TLS_ECDHE_RSA_WITH_CHACHA20_POLY1305_SHA256 = (0xcc, 0xa8)
cipher_suite_to_id TLS_ECDHE_ECDSA_WITH_CHACHA20_POLY1305_SHA256 = (0xcc, 0xa9)

public export
id_to_cipher_suite : (Bits8, Bits8) -> Maybe CipherSuite
id_to_cipher_suite (0x13, 0x01) = Just TLS_AES_128_GCM_SHA256
id_to_cipher_suite (0x13, 0x02) = Just TLS_AES_256_GCM_SHA384
id_to_cipher_suite (0x13, 0x03) = Just TLS_CHACHA20_POLY1305_SHA256
id_to_cipher_suite (0xc0, 0x2f) = Just TLS_ECDHE_RSA_WITH_AES_128_GCM_SHA256
id_to_cipher_suite (0xc0, 0x30) = Just TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384
id_to_cipher_suite (0xc0, 0x2b) = Just TLS_ECDHE_ECDSA_WITH_AES_128_GCM_SHA256
id_to_cipher_suite (0xc0, 0x2c) = Just TLS_ECDHE_ECDSA_WITH_AES_256_GCM_SHA384
id_to_cipher_suite (0xcc, 0xa8) = Just TLS_ECDHE_RSA_WITH_CHACHA20_POLY1305_SHA256
id_to_cipher_suite (0xcc, 0xa9) = Just TLS_ECDHE_ECDSA_WITH_CHACHA20_POLY1305_SHA256
id_to_cipher_suite _ = Nothing

public export
ciphersuite_to_hash_type : CipherSuite -> (DPair Type Hash)
ciphersuite_to_hash_type TLS_AES_128_GCM_SHA256 = MkDPair Sha256 %search
ciphersuite_to_hash_type TLS_AES_256_GCM_SHA384 = MkDPair Sha384 %search
ciphersuite_to_hash_type TLS_CHACHA20_POLY1305_SHA256 = MkDPair Sha256 %search
ciphersuite_to_hash_type TLS_ECDHE_RSA_WITH_AES_128_GCM_SHA256 = MkDPair Sha256 %search
ciphersuite_to_hash_type TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384 = MkDPair Sha384 %search
ciphersuite_to_hash_type TLS_ECDHE_ECDSA_WITH_AES_128_GCM_SHA256 = MkDPair Sha256 %search
ciphersuite_to_hash_type TLS_ECDHE_ECDSA_WITH_AES_256_GCM_SHA384 = MkDPair Sha384 %search
ciphersuite_to_hash_type TLS_ECDHE_RSA_WITH_CHACHA20_POLY1305_SHA256 = MkDPair Sha256 %search
ciphersuite_to_hash_type TLS_ECDHE_ECDSA_WITH_CHACHA20_POLY1305_SHA256 = MkDPair Sha256 %search

public export
ciphersuite_to_prf_type : CipherSuite -> (DPair Type Hash)
ciphersuite_to_prf_type TLS_AES_256_GCM_SHA384 = MkDPair Sha384 %search
ciphersuite_to_prf_type TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384 = MkDPair Sha384 %search
ciphersuite_to_prf_type TLS_ECDHE_ECDSA_WITH_AES_256_GCM_SHA384 = MkDPair Sha384 %search
ciphersuite_to_prf_type _ = MkDPair Sha256 %search

public export
ciphersuite_to_verify_data_len : CipherSuite -> Nat
ciphersuite_to_verify_data_len _ = 12

public export
ciphersuite_to_aead_type : CipherSuite -> (DPair Type AEAD)
ciphersuite_to_aead_type TLS_AES_128_GCM_SHA256 = MkDPair TLS13_AES_128_GCM %search
ciphersuite_to_aead_type TLS_AES_256_GCM_SHA384 = MkDPair TLS13_AES_256_GCM %search

ciphersuite_to_aead_type TLS_ECDHE_RSA_WITH_AES_128_GCM_SHA256 = MkDPair TLS12_AES_128_GCM %search
ciphersuite_to_aead_type TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384 = MkDPair TLS12_AES_256_GCM %search
ciphersuite_to_aead_type TLS_ECDHE_ECDSA_WITH_AES_128_GCM_SHA256 = MkDPair TLS12_AES_128_GCM %search
ciphersuite_to_aead_type TLS_ECDHE_ECDSA_WITH_AES_256_GCM_SHA384 = MkDPair TLS12_AES_256_GCM %search

ciphersuite_to_aead_type TLS_CHACHA20_POLY1305_SHA256 = MkDPair TLS1213_ChaCha20_Poly1305 %search
ciphersuite_to_aead_type TLS_ECDHE_RSA_WITH_CHACHA20_POLY1305_SHA256 = MkDPair TLS1213_ChaCha20_Poly1305 %search
ciphersuite_to_aead_type TLS_ECDHE_ECDSA_WITH_CHACHA20_POLY1305_SHA256 = MkDPair TLS1213_ChaCha20_Poly1305 %search

public export
data TLSVersion : Type where
  TLS10 : TLSVersion
  TLS11 : TLSVersion
  TLS12 : TLSVersion
  TLS13 : TLSVersion

public export
tls_version_to_id : TLSVersion -> (Bits8, Bits8)
tls_version_to_id TLS10 = (0x03, 0x01)
tls_version_to_id TLS11 = (0x03, 0x02)
tls_version_to_id TLS12 = (0x03, 0x03)
tls_version_to_id TLS13 = (0x03, 0x04)

public export
id_to_tls_version : (Bits8, Bits8) -> Maybe TLSVersion
id_to_tls_version (0x03, 0x01) = Just TLS10
id_to_tls_version (0x03, 0x02) = Just TLS11
id_to_tls_version (0x03, 0x03) = Just TLS12
id_to_tls_version (0x03, 0x04) = Just TLS13
id_to_tls_version _ = Nothing

%runElab derive "TLSVersion" [Generic, Meta, Eq, Ord, Show]

public export
data ExtensionType : Type where
  ServerName : ExtensionType
  SupportedGroups : ExtensionType
  SupportedVersions : ExtensionType
  SignatureAlgorithms : ExtensionType
  KeyShare : ExtensionType
  Unknown : (Bits8, Bits8) -> ExtensionType

%runElab derive "ExtensionType" [Generic, Meta, Eq, Show]

public export
extension_type_to_id : ExtensionType -> (Bits8, Bits8)
extension_type_to_id ServerName          = (0x00, 0x00)
extension_type_to_id SupportedGroups     = (0x00, 0x0a)
extension_type_to_id SignatureAlgorithms = (0x00, 0x0d)
extension_type_to_id SupportedVersions   = (0x00, 0x2b)
extension_type_to_id KeyShare            = (0x00, 0x33)
extension_type_to_id (Unknown x)         = x

public export
id_to_extension_type : (Bits8, Bits8) -> ExtensionType
id_to_extension_type (0x00, 0x00) = ServerName
id_to_extension_type (0x00, 0x0a) = SupportedGroups
id_to_extension_type (0x00, 0x0d) = SignatureAlgorithms
id_to_extension_type (0x00, 0x2b) = SupportedVersions
id_to_extension_type (0x00, 0x33) = KeyShare
id_to_extension_type x = Unknown x

public export
data HandshakeType : Type where
  ClientHello : HandshakeType
  ServerHello : HandshakeType
  NewSessionTicket : HandshakeType
  EncryptedExtensions : HandshakeType
  Certificate : HandshakeType
  CertificateVerify : HandshakeType
  Finished : HandshakeType
  ServerKeyExchange : HandshakeType
  ServerHelloDone : HandshakeType
  ClientKeyExchange : HandshakeType

%runElab derive "HandshakeType" [Generic, Meta, Eq, Show]

public export
handshake_type_to_id : HandshakeType -> Bits8
handshake_type_to_id ClientHello = 0x01
handshake_type_to_id ServerHello = 0x02
handshake_type_to_id NewSessionTicket = 0x04
handshake_type_to_id EncryptedExtensions = 0x08
handshake_type_to_id Certificate = 0x0b
handshake_type_to_id CertificateVerify = 0x0f
handshake_type_to_id Finished = 0x14
handshake_type_to_id ServerKeyExchange = 0x0c
handshake_type_to_id ServerHelloDone = 0x0e
handshake_type_to_id ClientKeyExchange = 0x10

public export
id_to_handshake_type : Bits8 -> Maybe HandshakeType
id_to_handshake_type 0x01 = Just ClientHello
id_to_handshake_type 0x02 = Just ServerHello
id_to_handshake_type 0x04 = Just NewSessionTicket
id_to_handshake_type 0x08 = Just EncryptedExtensions
id_to_handshake_type 0x0b = Just Certificate
id_to_handshake_type 0x0f = Just CertificateVerify
id_to_handshake_type 0x14 = Just Finished
id_to_handshake_type 0x0c = Just ServerKeyExchange
id_to_handshake_type 0x0e = Just ServerHelloDone
id_to_handshake_type 0x10 = Just ClientKeyExchange
id_to_handshake_type _ = Nothing

public export
data RecordType : Type where
  ChangeCipherSpec : RecordType
  Handshake : RecordType
  ApplicationData : RecordType
  Alert : RecordType

%runElab derive "RecordType" [Generic, Meta, Eq, Show]

public export
record_type_to_id : RecordType -> Bits8
record_type_to_id ChangeCipherSpec = 0x14
record_type_to_id Handshake = 0x16
record_type_to_id ApplicationData = 0x17
record_type_to_id Alert = 0x15

public export
id_to_record_type : Bits8 -> Maybe RecordType
id_to_record_type 0x14 = Just ChangeCipherSpec
id_to_record_type 0x15 = Just Alert
id_to_record_type 0x16 = Just Handshake
id_to_record_type 0x17 = Just ApplicationData
id_to_record_type _ = Nothing

namespace Parsing
  ||| creates a parserializer given an isomorphism from a type to a constant
  export
  magic : (Cons (Posed Bits8) i, Monoid i) => {k : Nat} -> (a -> Vect (S k) Bits8) -> (Vect (S k) Bits8 -> Maybe a) -> Parserializer Bits8 i (SimpleError String) a
  magic encode decode = MkParserializer (toList . encode) $ do
    bs <- count (S k) token
    let bytes = map get bs
    let Just phi = decode bytes
    | Nothing =>
      let
        (begin, end) = mapHom pos (head bs, last bs)
      in
        fail $ msg $ "at position " <+> show begin <+> "-" <+> show end <+> ", unknown id: " <+> xxd (toList bytes)
    pure phi

  export
  alert_level : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) AlertLevel
  alert_level = under "alert level" $ magic (to_vect . alert_level_to_id) (id_to_alert_level . from_vect)

  export
  alert_description : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) AlertDescription
  alert_description = magic (to_vect . alert_description_to_id) (id_to_alert_description . from_vect)

  export
  tls_version : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) TLSVersion
  tls_version = under "tls version" $ magic (pair_to_vect . tls_version_to_id) (id_to_tls_version . vect_to_pair)

  export
  cipher_suite : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) CipherSuite
  cipher_suite = under "cipher suite" $ magic (pair_to_vect . cipher_suite_to_id) (id_to_cipher_suite . vect_to_pair)

  export
  supported_group : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) SupportedGroup
  supported_group = under "supported group" $ magic (pair_to_vect . supported_group_to_id) (id_to_supported_group . vect_to_pair)

  export
  signature_algorithm : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) SignatureAlgorithm
  signature_algorithm = under "signature algorithm" $ magic (pair_to_vect . signature_algorithm_to_id) (id_to_signature_algorithm . vect_to_pair)

  export
  compression_level : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) CompressionLevel
  compression_level = under "compression level" $ magic (to_vect . compression_level_to_id) (id_to_compression_level . from_vect)

  public export
  extension_type : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) ExtensionType
  extension_type = under "extension type" $ magic (pair_to_vect . extension_type_to_id) (Just . id_to_extension_type . vect_to_pair)

  public export
  handshake_type : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) HandshakeType
  handshake_type = under "handshake type" $ magic (to_vect . handshake_type_to_id) (id_to_handshake_type . from_vect)

  export
  record_type : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) RecordType
  record_type = under "record type" $ magic (to_vect . record_type_to_id) (id_to_record_type . from_vect)


text:
module TypeTrans.Transformations

import TypeTrans.AST
import Data.Vect

incrDim : Nat -> TypeT -> Maybe TypeT
incrDim Z __ = Nothing
incrDim m (Vec sz tp) =
  if nsz * m == sz
    then Just (Vec m (Vec nsz tp))
    else Nothing
  where
    nsz = sz `div` m
incrDim _ _ = Nothing

redDim : TypeT -> Maybe TypeT
redDim  (Vec sz1 (Vec sz2 tp)) = Just (Vec (sz1 * sz2) tp)
redDim _ = Nothing

{-
splitMap : Int -> Action -> Action
splitMap m (Map v a) = Compose [Merge m, Map v (Map v a), Split m]

splitFold : Int -> Action -> Action
splitFold m (Fold v fa acc) =  Compose [Fold v (Fold v fa acc) acc, Split m]

splitAssocFoldByMap : Int -> Action -> Action
splitAssocFoldByMap m (Fold v afa acc) = Compose [Fold v afa acc, Map v (Fold v afa acc), Split m]

liftMapCompose : Action -> Action
liftMapCompose (Map v (Compose as)) = Compose (map (Map v) as)

-- Check
liftComposeMap : Action -> Action
liftComposeMap (Compose ((Map v a)::xs)) = Map v (Compose as)
    where
        as = map (\(Map _ a) => a) ((Map v a)::xs)

splitCompose : Action -> Action
splitCompose (Compose (a::as)) = Compose [a,Compose as]

mergeCompose : Action -> Action
mergeCompose (Compose (a::Compose as::[])) = Compose (a::as)
-- -----------------------------
--

combineSplitMerge : Action -> Action -> Action
combineSplitMerge s m =
    let
        Split n1 = s
        Merge n2 = m
    in
        Distr n1 n2

combineSplitDistr : Action -> Action -> Action
combineSplitDistr s m =
    let
        Split n1 = s
        Distr n2 n3 = m
    in
        Distr n1 n3 -- CHECK!!

combineDistrMerge : Action -> Action -> Action
combineDistrMerge s m =
    let
        Distr n1 n2= s
        Merge n3 = m
    in
        Distr n1 n3

joinSplitMerge_helper : ((Action -> Action -> Action) , (Action -> Bool) , (Action -> Bool),
                          List Action, List Action)  -> List Action
joinSplitMerge_helper (comb, t1, t2, [], as') = as'
joinSplitMerge_helper (comb, t1, t2, s::m::ras, as') =
    if (t1 s && t2 m)
      then
        joinSplitMerge_helper (comb, t1, t2,ras, (as'++[comb s m]))
      else
        joinSplitMerge_helper (comb, t1, t2,(m::ras), (as'++[s]))

isSplit : Action -> Bool
isSplit (Split _) = True
isSplit _ = False

isMerge : Action -> Bool
isMerge (Merge _) = True
isMerge _ = False

isDistr : Action -> Bool
isDistr (Distr _ _) = True
isDistr _ = False

joinSplitMerge : Action -> Action
joinSplitMerge (Compose [a]) =  Compose [a]
joinSplitMerge (Compose []) =  Compose []
joinSplitMerge (Compose as) = Compose (joinSplitMerge_helper (combineSplitMerge, isSplit, isMerge, as, []))

joinSplitDistr : Action -> Action
joinSplitDistr (Compose [a]) =  Compose [a]
joinSplitDistr (Compose []) =  Compose []
joinSplitDistr (Compose as) = Compose (joinSplitMerge_helper (combineSplitDistr, isSplit, isDistr, as, []))

joinDistrMerge : Action -> Action
joinDistrMerge (Compose [a]) =  Compose [a]
joinDistrMerge (Compose []) =  Compose []
joinDistrMerge (Compose as) = Compose (joinSplitMerge_helper (combineDistrMerge, isDistr, isMerge, as, []))

-- -----------------------------
--TODO Check
letToNestedLet : Argument -> Argument
letToNestedLet (Let exprs res) = case exprs of
  (x::xs) => (Let exprs res)
  -- Need verbosity of x1::x2::xs for automatic proof checker to
  -- infer that exprs is non empty
  (x1::x2::xs) => letToNestedLet (Let (init (x1::x2::xs))
                    (Let [Prelude.List.last (x1::x2::xs)] res))

-- TODO check, doesn't make sense
-- Lambda [Argument] Argument -> Action
-- Let [(Argument, Argument)] Argument -> Argument
-- Res Action Argument -> Argument
--letToLambda : Argument -> Argument
--letToLambda (Let [(lhs, rhs)] res) = Res (Lambda lhs res) rhs
-}

max_stars_repo_name: RossMeikleham/MSci-Project

max_issues_repo_name: RossMeikleham/MSci-Project

max_forks_repo_name: RossMeikleham/MSci-Project


text:
module Exercises.Chapter9

%access  public export
%default total

namespace List

  -- Exercise 9.1.6.1

  data Elem  : a -> List a -> Type where
       Here  : Elem x (x :: xs)
       There : (later : Elem x xs) -> Elem x (y :: xs)

  -- Exercise 9.1.6.2

  data Last     : List a -> a -> Type where
       LastOne  : Last [value] value
       LastCons : (prf : Last xs value) -> Last (x :: xs) value

  notLastNil : Not (Last [] value)
  notLastNil LastOne      impossible
  notLastNil (LastCons _) impossible

  notTha1 : Not (x = value) -> Not (Last [x] value)
  notTha1 contra  LastOne       = contra Refl
  notTha1 _      (LastCons nil) = notLastNil nil

  noWay : Not (xs = []) -> Not (Last xs value) -> Not (Last (x :: xs) value)
  noWay contra _       LastOne       = absurd (contra Refl)
  noWay _      contra (LastCons prf) = contra prf

  isLast : DecEq a => (xs : List a) -> (value : a) -> Dec (Last xs value)
  isLast [] _ = No notLastNil
  isLast (x :: xs) value with (isLast xs value)
    | Yes prf = Yes (LastCons prf)
    | No callate with (decEq xs [])
      isLast (x::_) value | _ | Yes Refl with (decEq x value)
        isLast [_] _ | _ | _ | Yes Refl = Yes LastOne
        | No sucka = No (notTha1 sucka)
      | No jose = No (noWay jose callate)

max_stars_repo_name: yurrriq/tdd-with-idris

max_issues_repo_name: yurrriq/tdd-with-idris

max_forks_repo_name: yurrriq/tdd-with-idris


text:
||| Central module use to import the Specdris test framework for
||| io code.
module Specdris.SpecIO

import System

import public Specdris.Data.SpecState
import public Specdris.Data.SpecResult
import public Specdris.Data.SpecInfo

import public Specdris.Core
import public Specdris.Expectations

import Specdris.Data.ConsoleColor

%access export
%default total

||| Adds a context/description to the spec test. It can have
||| nested descriptions or spec cases.
describe: (description : String) -> SpecTree' ffi -> SpecTree' ffi
describe descr tree = Node (Leaf $ Left $ Describe descr)
                           (tree)

||| Adds a spec case to the spec test. Spec cases consist only
||| of expectations. Nested spec cases or descriptions are not
||| allowed.
it : (description : String) -> IO' ffi SpecResult -> SpecTree' ffi
it descr spec = Node (Leaf $ Left $ It  descr)
                     (Leaf $ Right spec)

||| Empty `IO` effect
defaultIO : IO' ffi ()
defaultIO = pure ()

||| No `around` effect, just returns the given spec case
noAround : IO' ffi SpecResult -> IO' ffi SpecResult
noAround spec = spec

||| Executes a spec test.
|||
||| @ beforeAll `IO` effect which will be executed before the spec test (optional)
||| @ afterAll  `IO` effect which will be executed after the spec test (optional)
||| @ around a function to perform effects before/after every spec case (optional)
specIOWithState : {default defaultIO beforeAll : IO' ffi ()} ->
                  {default defaultIO afterAll : IO' ffi ()} ->
                  {default noAround around : IO' ffi SpecResult -> IO' ffi SpecResult} ->
                  {default False storeOutput : Bool} ->

                  SpecTree' ffi ->
                  IO' ffi SpecState
specIOWithState {beforeAll} {around} tree {afterAll} {storeOutput}
  = do beforeAll
       state <- evaluate around storeOutput tree
       afterAll

       pure state

||| Executes a spec test and prints the result.
|||
||| @ beforeAll `IO' ffi` effect which will be executed before the spec test (optional)
||| @ afterAll  `IO' ffi` effect which will be executed after the spec test (optional)
||| @ around a function to perform effects before/after every spec case (optional)
specIO' : {default defaultIO beforeAll : IO' ffi ()} ->
          {default defaultIO afterAll : IO' ffi ()} ->
          {default noAround around : IO' ffi SpecResult -> IO' ffi SpecResult} ->
          {default False storeOutput : Bool} ->

          SpecTree' ffi ->
          IO' ffi ()
specIO' {beforeAll} {around} tree {afterAll} {storeOutput}
  = do state <- specIOWithState {beforeAll = beforeAll} {afterAll = afterAll} {around = around} {storeOutput = storeOutput} tree
       putStrLn' $ "\n" ++ stateToStr state

||| Executes a spec test, prints the result to the command line, and exits
||| with an error code if any tests have failed.
|||
||| @ beforeAll `IO` effect which will be executed before the spec test (optional)
||| @ afterAll  `IO` effect which will be executed after the spec test (optional)
||| @ around a function to perform effects before/after every spec case (optional)
specIO : {default defaultIO beforeAll : IO ()} ->
         {default defaultIO afterAll : IO ()} ->
         {default noAround around : IO SpecResult -> IO SpecResult} ->
         {default False storeOutput : Bool} ->

         SpecTree ->
         IO ()
specIO {beforeAll} {around} tree {afterAll} {storeOutput}
  = do state <- specIOWithState {beforeAll = beforeAll} {afterAll = afterAll} {around = around} {storeOutput = storeOutput} tree

       putStrLn $ "\n" ++ stateToStr state

       if (failed state) > 0 then
         exitFailure
       else
         pure ()

max_stars_repo_name: pheymann/specdris

max_issues_repo_name: pheymann/specdris

max_forks_repo_name: pheymann/specdris


text:
module Inigo.Package.ExtraDep

import Data.List1
import Data.String
import Extra.String
import Inigo.Package.ParseHelpers
import Inigo.Paths
import System.Path
import Toml

-- TODO: Other methods?
public export
data Download
    = Git
    | SubDir

public export
DownloadInfo : Download -> Type
DownloadInfo Git = String -- commit
DownloadInfo SubDir = ()

public export
record ExtraDep where
    constructor MkExtraDep
    download : Download
    downloadInfo : DownloadInfo download
    url : String
    subDirs : List String

export
Show ExtraDep where
    show (MkExtraDep Git commit url subDirs) =
        "MkExtraDep{download=git, download-info=\"\{commit}\", url=\"\{url}\", subDirs=\{show subDirs}}"
    show (MkExtraDep SubDir () url subDirs) =
        "MkExtraDep{download=folder, url=\"\{url}\", subDirs=\{show subDirs}}"

export
Eq ExtraDep where
    MkExtraDep Git commit0 url0 subDirs0 == MkExtraDep Git commit1 url1 subDirs1 =
        commit0 == commit1 && url0 == url1 && subDirs0 == subDirs1
    MkExtraDep SubDir _ url0 subDirs0 == MkExtraDep SubDir _ url1 subDirs1 =
        url0 == url1 && subDirs0 == subDirs1
    _ == _ = False

export
eqIgnoreSubDirs : ExtraDep -> ExtraDep -> Bool
MkExtraDep Git commit0 url0 _ `eqIgnoreSubDirs` MkExtraDep Git commit1 url1 _ =
    commit0 == commit1 && url0 == url1
MkExtraDep SubDir _ url0 _ `eqIgnoreSubDirs` MkExtraDep SubDir _ url1 _ =
    url0 == url1
_ `eqIgnoreSubDirs` _ = False

export
toToml : List ExtraDep -> Toml
toToml deps = [(["extra-dep"], ArrTab $ depToToml <$> deps)]
  where
    depToToml : ExtraDep -> Toml
    depToToml (MkExtraDep Git commit url subDirs) =
        [ (["download"], Str "git")
        , (["commit"], Str commit)
        , (["url"], Str url)
        , (["sub-folders"], Lst (Str <$> subDirs))
        ]
    depToToml (MkExtraDep SubDir () url subDirs) =
        [ (["download"], Str "folder")
        , (["url"], Str url)
        , (["sub-folders"], Lst (Str <$> subDirs))
        ]

export
parseDownload : Toml -> Either String Download
parseDownload toml = case get ["download"] toml of
    Just (Str "git") => Right Git
    Just (Str "folder") => Right SubDir
    Just (Str val) => Left "Invalid download method: \{val}"
    Just val => Left "Inavlid value for field download: \{show val}"
    Nothing => Left "Missing field download"

export
parseExtraDeps : Toml -> Either String (List ExtraDep)
parseExtraDeps toml = case get ["extra-dep"] toml of
    Nothing => Right []
    Just (ArrTab deps) => foldlM extraDep [] deps
    Just val => Left "Invalid extra dependency found: \{show val}"
  where
    sanitiseCommit : String -> Either String String
    sanitiseCommit str =
        let len = length str
            allHex = all isHexDigit $ unpack str
        in if len == 7 || len == 40 && allHex
            then Right str
            else Left "Invalid commit: \"\{str}\""

    extraDep : List ExtraDep -> Toml -> Either String (List ExtraDep)
    extraDep deps toml = do
        url <- string ["url"] toml
        subDirs <- withDefault [""] $ listStr ["sub-folders"] toml
        download <- parseDownload toml
        case download of
            Git => do
                commit <- string ["commit"] toml >>= sanitiseCommit
                pure $ MkExtraDep Git commit url subDirs :: deps
            SubDir => do
                pure $ MkExtraDep SubDir () url subDirs :: deps

genFolder : String -> String
genFolder = concat . map escapeChar . unpack
  where
    escapeChar : Char -> String
    escapeChar c = if isAlphaNum c || c == '@'
        then cast c
        else "_" ++ show (ord c)

export
getExtraDepDir : ExtraDep -> String
getExtraDepDir (MkExtraDep Git commit url _) = inigoDepDir </> genFolder "\{url}@\{commit}"
getExtraDepDir (MkExtraDep SubDir _ url _) = url

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
module Strings

import DataTypes
import Control.ST
import Control.ST.Exception
import DataTypes
import Util
import Data.String.Extra

%access public export

unpackStr : LispVal -> ThrowsError String
unpackStr (LispString s) = pure s
unpackStr notString = Left $ TypeMismatch "string" notString

strBoolBinop' : (LispVal -> ThrowsError String) -> (String -> String -> Bool) -> PrimitiveLispFunc
strBoolBinop' unpacker = boolBinop unpacker

strBoolBinop : (String -> String -> Bool) -> PrimitiveLispFunc
strBoolBinop = strBoolBinop' unpackStr

isString : PrimitiveLispFunc
isString [LispString _] = pure $ LispBool True
isString _ = pure $ LispBool False

makeString : PrimitiveLispFunc
makeString [n@(LispInteger _)] = makeString [n, LispCharacter $ chr 0]
makeString [LispInteger n, LispCharacter c] =
  pure $ LispString $ pack $ replicate (cast n) c
makeString _ = Left $ Default "Invalid arguments to `make-string`"

strLen : PrimitiveLispFunc
strLen [LispString s] = pure $ LispInteger $ cast $ length s
strLen _ = Left $ Default "Invalid arguments to `string-length`"

strAppend : PrimitiveLispFunc
strAppend [] = pure $ LispString ""
strAppend [s@(LispString _)] = pure s
strAppend ((LispString s1)::(LispString s2)::xs) = strAppend (LispString (s1 ++ s2) :: xs)
strAppend _ = Left $ Default "Invalid arguments to `string-append`"

stringToSymbol : PrimitiveLispFunc
stringToSymbol [LispString s] = pure $ LispAtom s
stringToSymbol [arg] = Left $ TypeMismatch "string" arg
stringToSymbol args = Left $ NumArgs (MinMax 1 1) (cast $ length args) args

stringRef : PrimitiveLispFunc
stringRef [LispString s, LispInteger n] =
    let idx = fromIntegerNat n
    in case index idx s of
            Just c => pure $ LispCharacter c
            Nothing => Left $ Default "string-ref: index is out of range"
stringRef [v, LispInteger n] = Left $ TypeMismatch "string" v
stringRef [LispString s, v] = Left $ TypeMismatch "integer" v
stringRef args = Left $ NumArgs (MinMax 2 2) (cast $ length args) args

substring : PrimitiveLispFunc
substring [LispString s, LispInteger m, LispInteger n] =
    let start = fromIntegerNat m
        end = fromIntegerNat n
        len = fromIntegerNat (n - m)
    in if start >= 0 && end <= length s
            then pure $ LispString $ substr start len s
            else Left $ Default "substring: ending index is out of range"

strPrimitives : List (String, PrimitiveLispFunc)
strPrimitives =
  [ ("string=?", strBoolBinop (==))
  , ("string<?", strBoolBinop (<))
  , ("string>?", strBoolBinop (>))
  , ("string<=?", strBoolBinop (<=))
  , ("string>=?", strBoolBinop (>=))
  , ("string?", isString)
  , ("string->symbol", stringToSymbol)
  , ("string-ref", stringRef)
  , ("make-string", makeString)
  , ("string-length", strLen)
  , ("string-append", strAppend)
  , ("substring", substring)
  ]

max_stars_repo_name: ebenpack/lidrisp

max_issues_repo_name: ebenpack/lidrisp

max_forks_repo_name: ebenpack/lidrisp


text:
module Sixel.Decoder

import System.FFI

import Sixel.Library
import Sixel.Symbols
import Sixel.Allocator

public export
PrimDecoder : Type
PrimDecoder = GCAnyPtr

export
data Decoder : (0 n : Nat) -> Type where
  PointDecoder : PrimDecoder -> Decoder Z
  RootDecoder  : Decoder n -> Decoder (S n)

%foreign (sixelutils "sixel_utils_decoder_ptr_new")
sixel_utils_decoder_ptr_new : PrimIO (Ptr AnyPtr)

%foreign (sixelutils "sixel_utils_decoder_ptr_deref")
sixel_utils_decoder_ptr_deref : Ptr AnyPtr -> AnyPtr

%foreign (sixel "sixel_decoder_new")
sixel_decoder_new : Ptr AnyPtr -> PrimAllocator -> PrimIO Int

%foreign (sixel "sixel_decoder_ref")
sixel_decoder_ref : PrimDecoder -> ()

%foreign (sixel "sixel_decoder_unref")
sixel_decoder_unref : PrimDecoder -> ()

%foreign (sixel "sixel_decoder_unref")
sixel_decoder_destroy : AnyPtr -> PrimIO ()

%foreign (sixel "sixel_decoder_setopt")
sixel_decoder_setopt : PrimDecoder -> (optflag : Int) -> (setting : String) -> PrimIO Int

%foreign (sixel "sixel_decoder_decode")
sixel_decoder_decode : PrimDecoder -> PrimIO Int

export
MkDecoder : {auto n : Nat} -> {default (getNullAllocator n) alloc : Allocator n} -> IO (Either Status (Decoder Z))
MkDecoder {alloc} = do
  ppdecoder <- fromPrim sixel_utils_decoder_ptr_new
  status    <- MkStatus <$> fromPrim (sixel_decoder_new ppdecoder (toPrim alloc))
  pdecoder  <- onCollectAny (sixel_utils_decoder_ptr_deref ppdecoder) (\pd => fromPrim $ sixel_decoder_destroy pd)
  pure $ if succeeded status then Right (PointDecoder pdecoder) else Left status

export
ref : Decoder n -> IO (Decoder (S n))
ref (RootDecoder decoder)           = RootDecoder <$> ref decoder
ref decoder@(PointDecoder pdecoder) = let _ = sixel_decoder_ref pdecoder in pure $ RootDecoder decoder

export
unref : Decoder (S n) -> IO (Decoder n)
unref (RootDecoder decoder@(RootDecoder _))         = RootDecoder <$> unref decoder
unref (RootDecoder decoder@(PointDecoder pdecoder)) = let _ = sixel_decoder_unref pdecoder in pure decoder

export
refs : Decoder n -> Nat
refs (RootDecoder decoder) = S (refs decoder)
refs (PointDecoder _)      = Z

export
toPrim : Decoder n -> PrimDecoder
toPrim (RootDecoder decoder)   = toPrim decoder
toPrim (PointDecoder pdecoder) = pdecoder

export
setOpt : Decoder n -> (optflag : OptFlag) -> (setting : String) -> IO (Either Status ())
setOpt decoder optflag setting = do
  status <- MkStatus <$> fromPrim (sixel_decoder_setopt (toPrim decoder) (binding optflag) setting)
  pure $ if succeeded status then Right () else Left status

export
decode : Decoder n -> IO (Either Status ())
decode decoder = do
  status <- MkStatus <$> fromPrim (sixel_decoder_decode (toPrim decoder))
  pure $ if succeeded status then Right () else Left status

max_stars_repo_name: Kaiepi/id-sixel

max_issues_repo_name: Kaiepi/id-sixel

max_forks_repo_name: Kaiepi/id-sixel


text:
module FreeDelivery

-- Based on https://www.cs.ox.ac.uk/jeremy.gibbons/publications/delivery.pdf

data FreeA : (Type -> Type) -> Type -> Type where
  Pure : a -> FreeA f a
  More : f (a -> b) -> FreeA f a -> FreeA f b

Functor f => Functor (FreeA f) where
  map f (Pure x) = Pure $ f x
  map f (More fab ffa) = More (map (f .) fab) ffa

Functor f => Applicative (FreeA f) where
 pure x = Pure x

 (Pure f) <*> fa = map f fa
 (More h fa') <*> fa = More (map uncurry h) (pure (\x, y => (x, y)) <*> fa' <*> fa)

data Command : Type -> Type where
  Say : String -> Command ()
  Toast : Int -> Command ()
  Sense : Command Int

interface SerializeCommand a where
  serialize : a -> (String, String)
interface DeserializeCommand a where
    deserialize : a -> (String, String) -> Maybe a

SerializeCommand (Command a) where
  serialize (Say x) = ("Say", x)
  serialize (Toast x) = ("Toast", show x)
  serialize Sense = ("Sense", "")

DeserializeCommand (Command a) where
  deserialize (Say _) ("Say", s) = Just $ Say s
  deserialize (Toast _) ("Toast", s) = Just $ Toast (cast s)
  deserialize Sense ("Sense", s) = Just $ Sense
  deserialize _ _ = Nothing

data ActionA : Type -> Type where
  Con : Command r -> (r -> a) -> ActionA a

Functor ActionA where
  map f (Con c k) = Con c (f . k)

ProgramA : Type -> Type
ProgramA a = FreeA ActionA a

effectA : Command r -> ProgramA r
effectA c = More (Con c (\r, () => r)) (Pure ())

sayA : String -> ProgramA ()
sayA s = effectA (Say s)

toastA : Int -> ProgramA ()
toastA n = effectA (Toast n)

senseA : ProgramA Int
senseA = effectA Sense

straightA : Int -> ProgramA (Int, Int)
straightA n = pure (\t, (), t' => (t, t')) <*> senseA <*> toastA n <*> senseA

serializeA : ProgramA a -> List (String, String)
serializeA (Pure _) = []
serializeA (More (Con c _) fa') = serialize c :: serializeA fa'

deserializeA : ProgramA a -> List (String, String) -> Maybe (ProgramA a)
deserializeA (Pure x) [] = Just $ Pure x
deserializeA (More (Con c k) fa') (s :: ss) with (deserialize c s)
  deserializeA (More (Con c k) fa') (s :: ss) | Nothing = Nothing
  deserializeA (More (Con c k) fa') (s :: ss) | (Just c') = pure (More (Con c' k)) <*> deserializeA fa' ss
deserializeA _ _ = Nothing

testSerialize : List (String, String)
testSerialize = serializeA (straightA 1)

testDeserialize : Maybe (ProgramA (Int, Int))
testDeserialize = deserializeA (straightA 2) testSerialize

max_stars_repo_name: STELIORD/idris-snippets

max_issues_repo_name: stjordanis/idris-snippets

max_forks_repo_name: stjordanis/idris-snippets


text:
module Demo

import Data.Vect

%default total

data Nat' : Type where
  Z' : Nat'
  S' : Nat' -> Nat'

%name Nat' n,m,o

plus' : Nat' -> Nat' -> Nat'
plus' Z'     m = m
plus' (S' n) m = S' (plus' n m)

data Vect' : Nat -> Type -> Type where
  Nil : Vect' Z a
  (::) : a -> Vect' n a -> Vect' (S n) a

%name Vect' xs,ys,zs

append : Vect' n a -> Vect' m a -> Vect' (n + m) a
append Nil       ys = ys
append (x :: xs) ys = x :: (append xs ys)

zip : Vect' n a -> Vect' n b -> Vect' n (a, b)
zip []        []        = []
zip (x :: xs) (y :: ys) = (x, y) :: (zip xs ys)

take' : (n : Nat) -> Vect (n + m) a -> Vect n a
take' Z     xs = []
take' (S k) (x :: xs) = x :: take' k xs

drop' : (n : Nat) -> Vect (n + m) a -> Vect m a
drop' Z xs = xs
drop' (S k) (x :: xs) = drop' k xs

data SnocList : List a -> Type where
  SnocNil : SnocList []
  Snoc    : (xs : List a) -> (x :a) -> SnocList (xs ++ [x])

snocced : (xs : List a) -> SnocList xs
snocced [] = SnocNil
snocced (x :: xs) with (snocced xs)
  snocced (x :: [])          | SnocNil     = Snoc [] x
  snocced (x :: (ys ++ [y])) | (Snoc ys y) = Snoc (x :: ys) y

rot : Nat -> List a -> List a
rot Z       xs                        = xs
rot (S k)   xs       with (snocced xs)
  rot (S k) []          | SnocNil     = []
  rot (S k) (ys ++ [x]) | (Snoc ys x) = rot k (x::ys)

max_stars_repo_name: tgrospic/dependently-typed-slides

max_issues_repo_name: tgrospic/dependently-typed-slides

max_forks_repo_name: tgrospic/dependently-typed-slides


text:
module Data.List.Views.Extra

import Data.List
import Data.List.Reverse
import Data.List.Views
import Data.Nat
import Data.List.Equalities

%default total

||| Proof that two numbers differ by at most one
public export
data Balanced : Nat -> Nat -> Type where
  BalancedZ   : Balanced Z Z
  BalancedL   : Balanced (S Z) Z
  BalancedRec : Balanced n m -> Balanced (S n) (S m)

%name Balanced bal, b

Uninhabited (Balanced Z (S k)) where
  uninhabited BalancedZ impossible
  uninhabited BalancedL impossible
  uninhabited (BalancedRec rec) impossible

export
balancedPred : Balanced (S x) (S y) -> Balanced x y
balancedPred (BalancedRec pred) = pred

export
mkBalancedEq : {n, m : Nat} -> n = m -> Balanced n m
mkBalancedEq {n = 0} Refl = BalancedZ
mkBalancedEq {n = (S k)} Refl = BalancedRec $ mkBalancedEq {n = k} Refl

export
mkBalancedL : {n, m : Nat} -> n = S m -> Balanced n m
mkBalancedL {m = 0} Refl = BalancedL
mkBalancedL {m = S k} Refl = BalancedRec (mkBalancedL Refl)

||| View of a list split into two halves
|||
||| The lengths of the lists are guaranteed to differ by at most one
public export
data SplitBalanced : List a -> Type where
  MkSplitBal
    : {xs, ys : List a}
    -> Balanced (length xs) (length ys)
    -> SplitBalanced (xs ++ ys)

private
splitBalancedHelper
  : (revLs : List a)
  -> (rs : List a)
  -> (doubleSkip : List a)
  -> (length rs = length revLs + length doubleSkip)
  -> SplitBalanced (reverse revLs ++ rs)
splitBalancedHelper revLs rs [] prf = MkSplitBal balancedLeftsAndRights
  where
    lengthsEqual : length rs = length revLs
    lengthsEqual =
      rewrite sym (plusZeroRightNeutral (length revLs)) in prf
    balancedLeftsAndRights : Balanced (length (reverse revLs)) (length rs)
    balancedLeftsAndRights =
      rewrite reverseLength revLs in
        rewrite lengthsEqual in
          mkBalancedEq Refl
splitBalancedHelper revLs [] (x :: xs) prf =
  absurd $
    the (0 = S (plus (length revLs) (length xs)))
      rewrite plusSuccRightSucc (length revLs) (length xs) in
        prf
splitBalancedHelper revLs (x :: rs) [lastItem] prf =
  rewrite appendAssociative (reverse revLs) [x] rs in
    rewrite sym (reverseCons x revLs) in
      MkSplitBal $
        the (Balanced (length (reverseOnto [x] revLs)) (length rs)) $
          rewrite reverseCons x revLs in
            rewrite lengthSnoc x (reverse revLs) in
              rewrite reverseLength revLs in
                rewrite lengthsEqual in
                  mkBalancedL Refl
  where
    lengthsEqual : length rs = length revLs
    lengthsEqual =
      cong pred $
        the (S (length rs) = S (length revLs)) $
          rewrite plusCommutative 1 (length revLs) in prf
splitBalancedHelper revLs (x :: oneFurther) (_ :: (_ :: twoFurther)) prf =
  rewrite appendAssociative (reverse revLs) [x] oneFurther in
    rewrite sym (reverseCons x revLs) in
      splitBalancedHelper (x :: revLs) oneFurther twoFurther $
        cong pred $
          the (S (length oneFurther) = S (S (plus (length revLs) (length twoFurther)))) $
          rewrite plusSuccRightSucc (length revLs) (length twoFurther) in
            rewrite plusSuccRightSucc (length revLs) (S (length twoFurther)) in
              prf

||| Covering function for the `SplitBalanced`
|||
||| Constructs the view in linear time
export
splitBalanced : (input : List a) -> SplitBalanced input
splitBalanced input = splitBalancedHelper [] input input Refl

||| The `VList` view allows us to recurse on the middle of a list,
||| inspecting the front and back elements simultaneously.
public export
data VList : List a -> Type where
  VNil : VList []
  VOne : VList [x]
  VCons : {x, y : a} -> {xs : List a} -> (rec : Lazy (VList xs)) -> VList (x :: xs ++ [y])

private
toVList
  : (xs : List a)
  -> SnocList ys
  -> Balanced (length xs) (length ys)
  -> VList (xs ++ ys)
toVList [] Empty BalancedZ = VNil
toVList [x] Empty BalancedL = VOne
toVList [] (Snoc x zs rec) prf =
  absurd $
    the (Balanced 0 (S (length zs))) $
      rewrite sym (lengthSnoc x zs) in prf
toVList (x :: xs) (Snoc y ys srec) prf =
  rewrite appendAssociative xs ys [y] in
    VCons $
      toVList xs srec $
        balancedPred $
          rewrite sym (lengthSnoc y ys) in prf

||| Covering function for `VList`
||| Constructs the view in linear time.
export
vList : (xs : List a) -> VList xs
vList xs with (splitBalanced xs)
  vList (ys ++ zs) | (MkSplitBal prf) = toVList ys (snocList zs) prf

||| Lazy filtering of a list based on a predicate.
public export
data LazyFilterRec : List a -> Type where
  Exhausted : (skip : List a) -> LazyFilterRec skip
  Found     : (skip : List a) -- initial non-matching elements
            -> (head : a)      -- first match
            -> Lazy (LazyFilterRec rest)
            -> LazyFilterRec (skip ++ (head :: rest))

||| Covering function for the LazyFilterRec view.
||| Constructs the view lazily in linear time.
total export
lazyFilterRec : (pred : (a -> Bool)) -> (xs : List a) -> LazyFilterRec xs
lazyFilterRec pred [] = Exhausted []
lazyFilterRec pred (x :: xs) with (pred x)
  lazyFilterRec pred (x :: xs) | True = Found [] x (lazyFilterRec pred xs)
  lazyFilterRec pred (x :: []) | False = Exhausted [x]
  lazyFilterRec pred (x :: rest@(_ :: xs)) | False = filterHelper [x] rest
    where
      filterHelper
        : (reverseOfSkipped : List a)
        -> {auto prf1 : NonEmpty reverseOfSkipped}
        -> (rest : List a)
        -> {auto prf2 : NonEmpty rest}
        -> LazyFilterRec (reverse reverseOfSkipped ++ rest)
      filterHelper revSkipped (y :: xs) with (pred y)
      filterHelper revSkipped (y :: xs) | True =
        Found (reverse revSkipped) y (lazyFilterRec pred xs)
      filterHelper revSkipped (y :: []) | False =
        rewrite sym (reverseOntoSpec [y] revSkipped) in
          Exhausted $ reverse (y :: revSkipped)
      filterHelper revSkipped (y :: (z :: zs)) | False =
        rewrite appendAssociative (reverse revSkipped) [y] (z :: zs) in
          rewrite sym (reverseOntoSpec [y] revSkipped) in
            filterHelper (y :: revSkipped) (z :: zs)


text:
import System.Concurrency

-- Test that put/get works for multiple values.
main : IO ()
main =
  do c <- makeChannel
     t <- fork $ ignore (for [0..2] $ \n => channelPut c n)
     v0 <- channelGet c
     v1 <- channelGet c
     v2 <- channelGet c
     threadWait t
     if v0 == 0 && v1 == 1 && v2 == 2
        then putStrLn "Success!"
        else putStrLn "At least one value changed in transmission."


text:
module Parser.Unlit

import public Text.Literate
import Data.Strings

%default total

public export
data LiterateModes = Bird | Org | CMark

export
styleBird : LiterateStyle
styleBird = MkLitStyle Nil [">", "<"] [".lidr"]

export
styleOrg : LiterateStyle
styleOrg = MkLitStyle
              [ ("#+BEGIN_SRC idris","#+END_SRC")
              , ("#+begin_src idris","#+end_src")
              , ("#+COMMENT idris","#+END_COMMENT")
              , ("#+comment idris","#+end_comment")]
              ["#+IDRIS:"]
              [".org"]

export
styleCMark : LiterateStyle
styleCMark = MkLitStyle
              [("```idris", "```"), ("~~~idris", "~~~")]
              Nil
              [".md", ".markdown"]

export
isLitFile : String -> Maybe LiterateStyle
isLitFile fname =
    case isStyle styleBird of
      Just s => Just s
      Nothing => case isStyle styleOrg of
                     Just s => Just s
                     Nothing => isStyle styleCMark

  where
   hasSuffix : String -> Bool
   hasSuffix ext = isSuffixOf ext fname

   isStyle : LiterateStyle -> Maybe LiterateStyle
   isStyle style =
     if any hasSuffix (file_extensions style)
      then Just style
      else Nothing

export
isLitLine : String -> (Maybe String, String)
isLitLine str =
  case isLiterateLine styleBird str of
     (Just l, s) => (Just l, s)
     otherwise => case isLiterateLine styleOrg str of
                    (Just l, s) => (Just l, s)
                    otherwise => case isLiterateLine styleCMark str of
                                   (Just l, s) => (Just l, s)
                                   otherwise => (Nothing, str)

export
unlit : Maybe LiterateStyle -> String -> Either LiterateError String
unlit Nothing  str = Right str
unlit (Just s) str = unlit s str

export
relit : Maybe String -> String -> String
relit Nothing     str = str
relit (Just mark) str = unwords [mark, str]


text:
data SnocList: List a -> Type where
  Empty: SnocList []
  Snoc: (rec: SnocList xs) -> SnocList (xs ++ [x])

snocListHelp: (snoc: SnocList input) -> (rest: List a) -> SnocList (input ++ rest)
snocListHelp {input} snoc [] = rewrite appendNilRightNeutral input in snoc
snocListHelp {input} snoc (x :: xs) =
  rewrite appendAssociative input [x] xs in
          snocListHelp (Snoc snoc) xs
-- snocListHelp {input} snoc [] = ?noRewrite1 snoc
-- snocListHelp {input} snoc (x :: xs) = ?noRewrite2 (snocListHelp (Snoc snoc {x}) xs)

snocList: (xs: List a) -> SnocList xs
snocList xs = snocListHelp Empty xs

total myReverseHelper: (input: List a) -> SnocList input -> List a
myReverseHelper []          Empty      = []
myReverseHelper (xs ++ [x]) (Snoc rec) = x :: myReverseHelper xs rec

total myReverse: List a -> List a
myReverse input with (snocList input)
  myReverse []          | Empty       = []
  myReverse (xs ++ [x]) | (Snoc rec)  = x :: myReverse xs | rec

total isSuffix: Eq a => List a -> List a -> Bool
isSuffix input1 input2 with (snocList input1)
  isSuffix []          input2 | Empty      = True
  isSuffix (xs ++ [x]) input2 | (Snoc xsrec) with (snocList input2)
    isSuffix (xs ++ [x]) []          | (Snoc xsrec) | Empty        = False
    isSuffix (xs ++ [x]) (ys ++ [y]) | (Snoc xsrec) | (Snoc ysrec) =
      if x == y
      then isSuffix xs ys | xsrec | ysrec
      else False

list100: List Int
list100 = [1..100]

suffix: List Int
suffix = [90..100]

notSuffix: List Int
notSuffix = [1..10]

max_stars_repo_name: coffius/idris-exercises

max_issues_repo_name: coffius/idris-exercises

max_forks_repo_name: coffius/idris-exercises


text:
module Hezarfen.Definitions

%access public export

||| Simply-typed eliminator for `Dec`
dec : {a, c : Type} -> Lazy (a -> c) -> Lazy ((a -> Void) -> c) -> Dec a -> c
dec f _ (Yes prf) = f prf
dec _ g (No contra) = g contra

max_stars_repo_name: joom/hezarfen

max_issues_repo_name: joom/hezarfen

max_forks_repo_name: joom/hezarfen


text:
module Main

import Data.Strings
import Data.Vect

%default total

partial
readVectInt : HasIO io => io (n : Nat ** Vect n Int)
readVectInt = do x <- getLine
                 if x == ""
                    then pure $ (_ ** [])
                    else do (_ ** ns) <- readVectInt
                            pure $ (_ ** (cast x :: ns))

partial
addVectInts : HasIO io => io ()
addVectInts = do putStrLn "Enter the first vector (blank line to end)"
                 (len1 ** xs) <- readVectInt
                 putStrLn "Enter the second vector (blank line to end)"
                 (len2 ** ys) <- readVectInt
                 case exactLength len1 ys of
                      Nothing => putStrLn "Vectors are of unequal lengths"
                      Just ys' => printLn $ zipWith (+) xs ys'

max_stars_repo_name: timmyjose-study/tdd-with-idris

max_issues_repo_name: timmyjose-study/tdd-with-idris

max_forks_repo_name: timmyjose-study/tdd-with-idris


text:
-- 7.3 Exercises

data Vect : Nat -> Type -> Type where
     Nil  : Vect Z a
     (::) : (x : a) -> (xs : Vect k a) -> Vect (S k) a
%name Vect xs, ys, zs

Eq a => Eq (Vect n a) where
     (==) [] [] = True
     (==) (x :: xs) (y :: ys) = x == y && xs == ys
     (==) _ _ = False

Foldable (Vect n) where
     foldr func init [] = init
     foldr func init (x :: xs) = let acc = func x init in foldr func acc xs

Functor (Vect n) where
     map func [] = []
     map func (x :: xs) = func x :: map func xs


text: module PQ.FFI.CRUD


text:
module Data.PullRequest

import Data.Config
import Data.Date
import Data.Either
import Data.List
import Data.Vect
import Language.JSON
import Language.JSON.Accessors

%default total

public export
data PRState = Open | Closed

export
Show PRState where
  show Open   = "open"
  show Closed = "closed"

export
Eq PRState where
  Open   == Open   = True
  Closed == Closed = True
  _ == _ = False

public export
record PullRequest where
  constructor MkPullRequest
  ||| The pull request's "number" (as seen in URIs referring to the PR).
  number    : Integer
  ||| When the PR was created.
  createdAt : Date
  ||| The `login` of the author of the pull request.
  author    : String
  ||| Open or Closed status.
  state     : PRState
  ||| A List of all reviewers requested on the PR.
  reviewers : List String

%name PullRequest pr, pr1, pr2

export
Show PullRequest where
  show (MkPullRequest number _ author state _) = "\{show number}: \{show author} (\{show state})"

export
(.webURI) : Config => PullRequest -> String
pr.webURI @{config} = "https://github.com/\{config.org}/\{config.repo}/pull/\{show pr.number}"

export
isAuthor : String -> PullRequest -> Bool
isAuthor login = (== login) . author

export
isRequestedReviewer : String -> PullRequest -> Bool
isRequestedReviewer login = any (== login) . reviewers

parseState : String -> Either String PRState
parseState "open"   = Right Open
parseState "closed" = Right Closed
parseState str      = Left "Failed to parse a Pull Request State (open/closed). Found \{str}."

parseDateTime : String -> Either String Date
parseDateTime = maybeToEither "Failed to parse Date" . parseDateTimeString

export
parsePR : JSON -> Either String PullRequest
parsePR json =
 do pr <- object json
    [pullNumber, authorLogin, stateStr, createdAtStr, reviewerList] <- lookupAll ["pull_number", "author", "state", "created_at", "reviewers"] pr
    number    <- integer pullNumber
    author    <- string authorLogin
    state     <- parseState    =<< string stateStr
    createdAt <- parseDateTime =<< string createdAtStr
    reviewers <- array string reviewerList
    pure $ MkPullRequest {
        number
      , createdAt
      , author
      , state
      , reviewers
      }

||| Parse a single user from a JSON String
export
parsePullRequestString : String -> Either String PullRequest
parsePullRequestString =
  (maybeToEither "Failed to parse JSON" . JSON.parse) >=> parsePR

||| Parse a list of users from a JSON String
export
parsePullRequestsString : String -> Either String (List PullRequest)
parsePullRequestsString =
  (maybeToEither "Failed to parse JSON" . JSON.parse) >=> array parsePR

max_stars_repo_name: mattpolzin/harmony

max_issues_repo_name: mattpolzin/harmony

max_forks_repo_name: mattpolzin/harmony


text:
module Main

data LazyList : Type -> Type where
  Nil : LazyList ty
  (::) : (value : ty) -> Inf (LazyList ty) -> LazyList ty

%name LazyList xs, ys, zs

upto : Integer -> Integer -> LazyList Integer
upto n m = case n > m of
  True => Nil
  False => n :: upto (n + 1) m

sum : LazyList Integer -> Integer
sum [] = 0
sum (x :: xs) = x + sum xs

main : IO ()
main = do
  printLn (sum (upto 1 10000))

max_stars_repo_name: pdani/idris-grin

max_issues_repo_name: pdani/idris-grin

max_forks_repo_name: pdani/idris-grin


text:
module MiniParser

import Types

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

import Combi

symbol : Parser Char
symbol = oneOf "!#$%&|*+-/:<=>?@^_~"

spaces : Parser ()
spaces = skipMany1 space

parseString : Parser Val
parseString = do
                char '"'
                x <- many $ noneOf "\""
                char '"'
                pure $ S $ pack x

parseAtom : Parser Val
parseAtom = do
              fst <- letter <|> symbol
              rest <- many (alphaNum <|> symbol)
              let atom = pack $ fst :: rest
              pure $ case atom of
                            "#t" => B True
                            "#f" => B False
                            otherwise => A atom

positiveInt : (Num n, Monad m, Stream Char s) => ParserT s m n
positiveInt = do
                ds <- some digit
                let theInt = getInteger ds
                pure $ fromInteger theInt
              where
                getInteger : List (Fin 10) -> Integer
                getInteger = foldl (\a => \b => 10 * a + cast b) 0

parseNumber : Parser Val
parseNumber = pure $ N !positiveInt

mutual
  parseQuoted : Parser Val
  parseQuoted = do
                  char '\''
                  pure $ L [(A "quote"), !parseExpr]

  parseList : Parser Val
  parseList = pure $ L !(sepBy parseExpr MiniParser.spaces)

  parseDottedList : Parser Val
  parseDottedList = do
                      head <- endBy parseExpr MiniParser.spaces
                      tail <- do
                                char '.'
                                MiniParser.spaces
                                parseExpr
                      pure $ D head tail

  export
  parseExpr : Parser Val
  parseExpr = parseAtom
           <|> parseString
           <|> parseNumber
           <|> parseQuoted
           <|> do char '('
                  x <- parseList
                  char ')'
                  pure x
           <|> do char '('
                  x <- parseDottedList
                  char ')'
                  pure x


text:
module AssRecRule

import Data.Fin
import Data.Vect

{-
 The recursion function for lists of type `a`. Define this by pattern matching
-}
recList : (a: Type) ->  (x: Type) -> x -> (a -> List a -> x -> x) -> (List a -> x)
recList a x emp fn [] = emp
recList a x emp fn (head :: ls) = fn head ls (recList a x emp fn ls)

{-
Given a list of type `a` and a function `f: a -> b` get a list of type `b`
by applying `f` to each element.
Note: Define using `recList` and without pattern matching on lists.
-}
mapList : (a: Type) -> (b: Type) -> (f: a -> b) -> List a -> List b
mapList a b f ls = recList a (List b) [] map ls where
  map head la lb = (f head) :: lb

{-
Given a list of type `a`, an initial value `init: a` and an operation `op: a -> a -> a`,
get an element of `a` by starting with init and repeatedly applying the elements of the
list,
e.g. fold Nat 1 (*) ([22] :: [3] :: [])  = 1 * 22 * 3
Note: Define using `recList` and without pattern matching on lists.
-}
foldList : (a: Type) ->  (init: a) -> (op : a -> a -> a) -> List a -> a
foldList a init op ls = recList a a init map ls where
  map head la val = op head val

{-
The induction function on the `Fin` indexed type family. Define this by pattern matching.
-}
inducFin : (xs : (n: Nat) -> Fin n -> Type) ->
  (base : (m: Nat) -> xs (S m) FZ) ->
  (step : (p: Nat) -> (k: Fin p) ->  (prev: xs p k) -> (xs (S p) (FS k))) ->
  (q: Nat) -> (j: Fin q) -> xs q j
inducFin _ _ _ Z FZ impossible
inducFin _ _ _ Z (FS _) impossible
inducFin xs base step (S k) FZ = base k
inducFin xs base step (S k) (FS x) = step k x (inducFin xs base step k x)

{-
Given a type `a`, a natural number `q`, an element `j : Fin q` and a vector `v` of length q with entries of type `a`,
get the element in position `j` of `v`. Note that this is always well defined.

Note: Define using `inducList` and without pattern matching on the `Fin` family. You may pattern match on Vectors.
The definition should have only one case, and there should be no case splitting on `Fin`.
-}
fetchElem : (a: Type) -> (q: Nat) -> (j: Fin q) -> (Vect q a -> a)
fetchElem a q j ys = inducFin xs base step q j ys where
  xs: (n: Nat) -> Fin n -> Type
  xs n j = Vect n a -> a
  base m = retHead where
    retHead: Vect (S m) a -> a --retrieve Head
    retHead (x :: ls) = x
  step p k prev = retStep where --reduce list to smaller one
    retStep : Vect (S p) a -> a
    retStep (x :: ls) = prev ls