text:
> module Fraction.Predicates

> import Fraction.Fraction
> import PNat.PNat
> import PNat.Operations
> import Nat.Positive

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

> ||| Proofs that `x` is less than or equal to `y`
> ||| @ x the smaller number
> ||| @ y the larger number
> LTE : (x, y : Fraction) -> Type
> LTE (n1, d1') (n2, d2') = Prelude.Nat.LTE (n1 * (toNat d2')) (n2 * (toNat d1'))

> ||| An equivalence relation (see below)
> Eq : Fraction -> Fraction -> Type
> Eq (m, d') (n, e') = let d = toNat d' in
>                      let e = toNat e' in
>                      m * e = n * d
> -- %freeze Eq

The idea is to use |Eq| implement non-negative rational numbers as
quotient of fractions by |Eq|.

A naive approach toward implementing (non-negative) rational numbers
(for which equality is well represented by syntactical equality) could
be to define rational numbers as normalized fractions, something like

  NonNegRational = Subset Fraction Normal

where |Normal : Fraction -> Type| represents the property of being in
normal form, see "FractionNormal". It is easy to see that |normalize|
does indeed return fractions in normal form, see |normalNormalize| in
"FractionProperties". Thus, one could implement addition and
multiplication of rational numbers in terms of |normalize| and of
fraction addition and multiplication. For instance:

  plus : NonNegRational -> NonNegRational -> NonNegRational
  plus x' y' = let x   =  getWitness x' in
               let y   =  getWitness y' in
               Element (normalize (x + y)) (normalNormalize (x + y))

and similarly for multiplication. The problem with this approach is that
implementing proofs of

  1.  x + y = y + x
  2.  x + 0 = x
  3.  x + (y + z) = (x + y) + z
  4.  x * y = y * x
  5.  x * 1 = x

for fractions is tedious but trivial. Extending 1,2,4,5 to rational
numbers is pretty straightforward but extending 3 and deriving

  6.  x * (y + z) = (x * y) + (x * z)

(which does not hold for fractions) turns out to be a nightmare. With
|Eq| we can take advantage of Tim Richter's "SplitQuotient" and
"KernelQuotient" modules (see ...) to define ...

...

To this end, we only need to show that:

 a. Fraction addition and multiplication preserve Eq:

    a1.  (x Eq x') -> (y Eq y') -> (x + y) Eq (x' + y')
    a2.  (x Eq x') -> (y Eq y') -> (x * y) Eq (x' * y')

 b. Normalize fulfills:

    b1.  (normalize x) Eq x
    b2.  x Eq y -> normalize x = normalize y

These properties are implemented via

< plusPreservesEq : (x, x', y, y' : Fraction) ->
<                   (x `Eq` x') -> (y `Eq` y') -> (x + y) `Eq` (x' + y')

< multPreservesEq : (x, x', y, y' : Fraction) ->
<                   (x `Eq` x') -> (y `Eq` y') -> (x * y) `Eq` (x' * y')

and

< normalizeEqLemma1 : (x : Fraction) -> (normalize x) `Eq` x

< normalizeEqLemma2 : (x : Fraction) -> (y : Fraction) ->
<                     x `Eq` y -> normalize x = normalize y

in "FractionEqProperties".

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
module B

public export
record Rec where
  constructor MkRec
  field : Char --- Unit and Bool don't cause the bug

public export
defaultRec : Rec
defaultRec = MkRec 'a'

ext: idr


text:
module ArithCmd

import Data.Primitives.Views
import System

%default total

data Fuel = Dry | More (Lazy Fuel)

partial
forever : Fuel
forever = More forever

data Command : Type -> Type where
  PutStr  : String -> Command ()
  GetLine : Command String
  Bind : Command a -> (a -> Command b) -> Command b
  Pure : a -> Command a

implementation Functor Command where
  map func cmdA = Bind cmdA (\valA => Pure (func valA))

implementation Applicative Command where
  pure valA = Pure valA
  (<*>) cmdAB cmdA = Bind cmdAB (\funcAB => map funcAB cmdA)

implementation Monad Command where
  (>>=) = Bind

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

data Input = Answer Int | QuitCmd

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

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

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

runCommand : Command ty -> IO ty
runCommand (PutStr x)       = putStr x
runCommand GetLine          = getLine
runCommand (Bind cmdA func) =
  do
    res <- runCommand cmdA
    runCommand (func res)
runCommand (Pure x)       = pure x

run : Fuel -> ConsoleIO a -> IO (Maybe a)
run Dry      _                = pure Nothing
run (More fuel) (Quit res)    = pure (Just res)
run (More fuel) (Do cmd func) =
  do
    cmdRes <- runCommand cmd
    let res = func cmdRes
    run fuel res

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

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

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

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

max_stars_repo_name: coffius/idris-exercises

max_issues_repo_name: coffius/idris-exercises

max_forks_repo_name: coffius/idris-exercises


text:
module Circuits

total
wiresIn : Nat -> Type
wiresIn Z = Type
wiresIn (S k) = Wire -> (wiresIn k)

data Box : (inputCount : Nat) -> Type where
  MkBox : (n : Nat) -> (wiresIn n) -> Box n

data Wire : Type where
  MkWire : Wire

max_stars_repo_name: ostera/asdf

max_issues_repo_name: ostera/asdf

max_forks_repo_name: ostera/asdf


text:
module InstancesSpec

%default total

MapType

max_stars_repo_name: Kazark/tyclgen

max_issues_repo_name: Kazark/tyclgen

max_forks_repo_name: Kazark/tyclgen


text:
-- ----------------------------------------------------------------- [ ABE.idr ]
-- Module      : ABE
-- Description : Types for Attribute Based Encryption
-- Copyright   : (c) Jan de Muijnck-Hughes
-- License     : see LICENSE
-- --------------------------------------------------------------------- [ EOF ]
module Crypto.Adv.ABE

import Crypto.Adv.Key

data ABEKeyType = CipherTextPolicy | KeyPolicy

max_stars_repo_name: silky/idris-crypto-types

max_issues_repo_name: silky/idris-crypto-types

max_forks_repo_name: silky/idris-crypto-types


text:
module Error

import Control.Monad.Error.Interface
import Control.Monad.Error.Either
import Data.String
import TyTTP

orThrow : MonadError e m => Maybe a -> e -> m a
orThrow m e = case m of
  Just a  => pure a
  Nothing => throwError e

data Error = ParseError String

parseIntegerM : MonadError Error m => String -> m Int
parseIntegerM s = parseInteger s `orThrow` ParseError ("Could not parse as int: " <+> s)

hParseRequest : MonadError e m
  => (String -> m a')
  -> Step me h1 u Request.simpleBody s h2 String b
  -> m $ Step me h1 u Request.simpleBody s h2 a' b
hParseRequest parser step = do
  result <- parser step.request.body
  pure $ { response.body := result } step

exampleErrorHandling : Step () String () Request.simpleBody () () String String -> IO ()
exampleErrorHandling initialStep = do
  putStrLn $ "\nErrors: " <+> initialStep.request.body <+> "\n"

  let handler = hParseRequest parseIntegerM >=> hEcho {m = EitherT Error IO}
  result <- runEitherT $ handler initialStep

  case result of
    Left  (ParseError e) => putStrLn e
    Right a => putStrLn $ show a.response.body

main : IO ()
main = do
  let res = MkResponse () () ""
      step = MkStep (MkRequest () "/" () "request") res

  exampleErrorHandling step
  exampleErrorHandling $ MkStep (MkRequest () "/" () "134") res

max_stars_repo_name: kbertalan/tyttp

max_issues_repo_name: kbertalan/tyttp

max_forks_repo_name: kbertalan/tyttp


text:
module Language.LSP.CodeAction.CaseSplit

import Core.Context
import Core.Core
import Core.Env
import Core.Metadata
import Core.UnifyState
import Data.List1
import Data.String
import Idris.IDEMode.CaseSplit
import Idris.REPL.Opts
import Idris.Syntax
import Idris.Syntax
import Language.JSON
import Language.LSP.Message
import Libraries.Data.List.Extra
import Libraries.Data.PosMap
import Server.Configuration
import Server.Response
import Server.Utils
import System.File
import TTImp.Interactive.CaseSplit
import TTImp.TTImp

-- fork of updateCase in Idris.IDEMode.CaseSplit.updateCase
originalLine : Ref Ctxt Defs
            => Ref Syn SyntaxInfo
            => Ref ROpts REPLOpts
            => List ClauseUpdate -> Int -> Int
            -> Core String
originalLine splits line col = do
  Just f <- gets ROpts mainfile
    | Nothing => throw (InternalError "No file loaded")
  Right file <- coreLift $ readFile f
    | Left err => throw (FileErr f err)
  let Just l = elemAt (forget $ lines file) (integerToNat (cast line))
    | Nothing => throw (InternalError "File too short!")
  pure l

export
caseSplit : Ref LSPConf LSPConfiguration
         => Ref MD Metadata
         => Ref Ctxt Defs
         => Ref UST UState
         => Ref Syn SyntaxInfo
         => Ref ROpts REPLOpts
         => OneOf [Int, String, Null] -> CodeActionParams -> Core (Maybe CodeAction)
caseSplit msgId params = do
  let True = params.range.start.line == params.range.end.line
      | _ => pure Nothing

  meta <- get MD
  let line = params.range.start.line
  let col = params.range.start.character
  let Just name = findInTree (line, col) (nameLocMap meta)
    | Nothing => pure Nothing

  let find = if col > 0
                then within (line, col)
                else onLine line

  OK splits <- getSplits (anyAt find) name
     | SplitFail err => pure Nothing

  lines <- updateCase splits line col
  original <- originalLine splits line col

  let docURI = params.textDocument.uri
  let rng = MkRange (MkPosition line 0)
                    (MkPosition line (cast (length original)))
  let edit = MkTextEdit rng (unlines lines)
  let workspaceEdit = MkWorkspaceEdit
        { changes           = Just (singleton docURI [edit])
        , documentChanges   = Nothing
        , changeAnnotations = Nothing
        }
  pure $ Just $ MkCodeAction
    { title       = "Case split on \{show name}"
    , kind        = Just $ Other "case-split"
    , diagnostics = Just []
    , isPreferred = Just False
    , disabled    = Nothing
    , edit        = Just workspaceEdit
    , command     = Nothing
    , data_       = Nothing
    }


text:
printLength : IO ()
printLength = putStr "Input string: " >>= \_ =>
              getLine >>= \input =>
              let len = length input in
              putStrLn (show len)


text:
import Data.Vect

data Format = Number Format
            | Str Format
            | Chr Format
            | Dbl Format
            | Lit String Format
            | End

PrintfType : Format -> Type
PrintfType (Number fmt) = (i : Int) -> PrintfType fmt
PrintfType (Str fmt) = (str : String) -> PrintfType fmt
PrintfType (Chr fmt) = (char : Char) -> PrintfType fmt
PrintfType (Dbl fmt) = (double : Double) -> PrintfType fmt
PrintfType (Lit str fmt) = PrintfType fmt
PrintfType End = String

printfFmt : (fmt : Format) -> (acc : String) -> PrintfType fmt
printfFmt (Number fmt) acc = \i => printfFmt fmt (acc ++ show i)
printfFmt (Str fmt) acc = \str => printfFmt fmt (acc ++ str)
printfFmt (Chr fmt) acc = \chr => printfFmt fmt (acc ++ (show chr))
printfFmt (Dbl fmt) acc = \dbl => printfFmt fmt (acc ++ (cast dbl))
printfFmt (Lit str fmt) acc = printfFmt fmt (acc ++ str)
printfFmt End acc = acc

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

printf : (fmt : String) -> PrintfType (toFormat $ unpack fmt)
printf fmt = printfFmt _ ""

Matrix : Nat -> Nat -> Type
Matrix n m = Vect n (Vect m Double)

testMatrix : Matrix 2 3
testMatrix = [[0, 0, 0], [0, 0, 0]]


text:
module TyTTP.Core.Promise

import Control.Monad.Trans

public export
record Callbacks e (m : Type -> Type) a where
  constructor MkCallbacks
  onSucceded : a -> m ()
  onFailed : e -> m ()

public export
record Promise e (m : Type -> Type) a where
  constructor MkPromise
  continuation : Callbacks e m a -> m ()

export
Functor (Promise e m) where
  map f (MkPromise ca) = MkPromise $ \cb => ca $ MkCallbacks (cb.onSucceded . f) cb.onFailed

mutual

  export
  Applicative (Promise e m) where
    pure a = MkPromise $ \cb => cb.onSucceded a
    fn <*> pa = fn >>= \f => map f pa

  export
  Monad (Promise e m) where
    (>>=) (MkPromise conta) f = MkPromise $ \cb => conta $ MkCallbacks
        { onSucceded = \a =>
            let MkPromise contb = f a
            in contb cb
        , onFailed = cb.onFailed
        }

export
MonadTrans (Promise e) where
  lift ma = MkPromise $ \cb => ma >>= cb.onSucceded

export
HasIO m => HasIO (Promise e m) where
  liftIO = lift . liftIO

export
fail : e -> Promise e m a
fail e = MkPromise $ \cb => cb.onFailed e


text:
module Idris.Doc.HTML

import Core.Context
import Core.Core
import Core.Directory

import Data.Strings

import Parser.Lexer.Source

import Libraries.Text.PrettyPrint.Prettyprinter
import Libraries.Text.PrettyPrint.Prettyprinter.Render.HTML
import Libraries.Text.PrettyPrint.Prettyprinter.SimpleDocTree

import Idris.Doc.String
import Idris.Package.Types
import Idris.Pretty
import Idris.Version

%default covering

getNS : Name -> String
getNS (NS ns _) = show ns
getNS _ = ""

hasNS : Name -> Bool
hasNS (NS _ _) = True
hasNS _ = False

tryCanonicalName : {auto c : Ref Ctxt Defs} ->
                FC -> Name -> Core (Maybe Name)
tryCanonicalName fc n with (hasNS n)
  tryCanonicalName fc n | True
      = do defs <- get Ctxt
           case !(lookupCtxtName n (gamma defs)) of
                [(n, _, _)] => pure $ Just n
                _ => pure Nothing
  tryCanonicalName fc n | False = pure Nothing

packageInternal : {auto c : Ref Ctxt Defs} ->
                  Name -> Core Bool
packageInternal (NS ns _) =
  do let mi = nsAsModuleIdent ns
     catch ((const True) <$> nsToSource emptyFC mi) (\_ => pure False)
packageInternal _ = pure False

prettyNameRoot : Name -> String
prettyNameRoot n =
  let root = htmlEscape $ nameRoot n in
  if isOpName n then "(" ++ root ++ ")" else root

renderHtml : {auto c : Ref Ctxt Defs} ->
             SimpleDocTree IdrisDocAnn ->
             Core String
renderHtml STEmpty = pure neutral
renderHtml (STChar ' ') = pure " "
renderHtml (STChar c) = pure $ cast c
renderHtml (STText _ text) = pure $ htmlEscape text
renderHtml (STLine _) = pure "
"
renderHtml (STAnn Declarations rest) = pure $ "
" <+> !(renderHtml rest) <+> "
"
renderHtml (STAnn (Decl n) rest) = pure $ "
" <+> !(renderHtml rest) <+> "
"
renderHtml (STAnn DocStringBody rest) = pure $ "
" <+> !(renderHtml rest) <+> "
"
renderHtml (STAnn DCon rest) = do
  resthtml <- renderHtml rest
  pure $ "" <+> resthtml <+> ""
renderHtml (STAnn (TCon n) rest) = do
  pure $ "" <+> (prettyNameRoot n) <+> ""
renderHtml (STAnn (Fun n) rest) = do
  pure $ "" <+> (prettyNameRoot n) <+> ""
renderHtml (STAnn Header rest) = do
  resthtml <- renderHtml rest
  pure $ "" <+> resthtml <+> ""
renderHtml (STAnn (Syntax (SynRef n)) rest) = do
  resthtml <- renderHtml rest
  Just cName <- tryCanonicalName emptyFC n
    | Nothing => pure $ "" <+> resthtml <+> ""
  True <- packageInternal cName
    | False => pure $ "<span class=\"type resolved\" title=\"" <+> (htmlEscape $ show cName) <+> "\">" <+> (htmlEscape $ nameRoot cName) <+> ""
  pure $ "" <+> (htmlEscape $ nameRoot cName) <+> ""
renderHtml (STAnn ann rest) = do
  resthtml <- renderHtml rest
  pure $ "" ++ resthtml ++ ""
renderHtml (STConcat docs) = pure $ fastConcat !(traverse renderHtml docs)

removeNewlinesFromDeclarations : SimpleDocTree IdrisDocAnn -> SimpleDocTree IdrisDocAnn
removeNewlinesFromDeclarations = go False
  where
    go : Bool -> SimpleDocTree IdrisDocAnn -> SimpleDocTree IdrisDocAnn
    go False l@(STLine i) = l
    go True l@(STLine i) = STEmpty
    go ignoring (STConcat docs) = STConcat $ map (go ignoring) docs
    go _ (STAnn Declarations rest) = STAnn Declarations $ go True rest
    go _ (STAnn ann rest) = STAnn ann $ go False rest
    go _ doc = doc

docDocToHtml : {auto c : Ref Ctxt Defs} ->
               Doc IdrisDocAnn ->
               Core String
docDocToHtml doc =
  let dt = SimpleDocTree.fromStream $ layoutUnbounded doc in
      renderHtml $ removeNewlinesFromDeclarations dt

htmlPreamble : String -> String -> String -> String
htmlPreamble title root class = "<!DOCTYPE html><meta charset=\"utf-8\">"
  ++ "<title>" ++ htmlEscape title ++ "</title>"
  ++ "<link rel=\"stylesheet\" href=\"" ++ root ++ "styles.css\">"
  ++ ""
  ++ "Idris2Doc : " ++ htmlEscape title
  ++ "Index"
  ++ "
"

htmlFooter : String
htmlFooter = "
Produced by Idris 2 version " ++ (showVersion True version) ++ ""

export
renderDocIndex : PkgDesc -> String
renderDocIndex pkg = fastConcat $
  [ htmlPreamble (name pkg) "" "index"
  , "
Package ", name pkg, " - Namespaces
"
  , "
"] ++
  (map moduleLink $ modules pkg) ++
  [ "
"
  , htmlFooter
  ]
    where
      moduleLink : (ModuleIdent, String) -> String
      moduleLink (mod, filename) =
         "
" ++ (show mod) ++ "
"

export
renderModuleDoc : {auto c : Ref Ctxt Defs} ->
                  ModuleIdent ->
                  Doc IdrisDocAnn ->
                  Core String
renderModuleDoc mod allModuleDocs = pure $ fastConcat
  [ htmlPreamble (show mod) "../" "namespace"
  , "
", show mod, "
"
  , !(docDocToHtml allModuleDocs)
  , htmlFooter
  ]

max_stars_repo_name: mmhelloworld/idris-jvm

max_issues_repo_name: mmhelloworld/idris-jvm

max_forks_repo_name: mmhelloworld/idris-jvm


text:
module Main

import Language.JSON.Data
import IdrisJvm.IO
import IdrisJvm.System
import IdrisJvm.JvmImport
import Java.Lang
import Java.Util
import Java.Util.Function
import Data.Vect
import Mmhelloworld.IdrisSpringBoot.Boot.Autoconfigure
import Io.Github.Mmhelloworld.SpringBoot

%access public export
%hide Java.Util.HashMap.get

onApplicationReady : ApplicationArguments -> JVM_IO ()
onApplicationReady args = printLn "hello from Idris"

greet : ServerRequest -> JVM_IO Mono
greet request = ok "hello world"

beans : List Bean
beans = [
    runner onApplicationReady,
    get "/greet" greet
]

springMain : StringArray -> JVM_IO ()
springMain args = runSpring (classLit "main/IdrisSpringMain") beans args

main : JVM_IO ()
main = pure ()

exportSpringBootApp : FFI_Export FFI_JVM "main/IdrisSpringMain" []
exportSpringBootApp =
  Fun classWith (Anns [ <@SpringBootApplication> [] ]) $
  Fun springMain (ExportStatic "main") $
  End

max_stars_repo_name: mmhelloworld/idris-spring-boot-example

max_issues_repo_name: mmhelloworld/idris-spring-boot-example

max_forks_repo_name: mmhelloworld/idris-spring-boot-example


text:
module Commons.Control.Logging.Simple

import Control.ST

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

  startLogging : (lvl : Nat)
              -> ST m (Var) [add Logger]

  setLevel : (logger : Var)
          -> (lvl : Nat)
          -> ST m () [logger ::: Logger]

  log : (logger : Var)
     -> (lvl    : Nat)
     -> (msg    : String)
     -> ST m () [logger ::: Logger]

  endLogging : (logger : Var)
            -> ST m () [Remove logger Logger]

public export
Logging IO where
  Logger = State Nat

  startLogging lvl = do
    logger <- new lvl
    pure logger

  setLevel logger new = write logger new

  log logger lvl msg = do
    curr <- read logger
    case compare lvl curr of
      GT => pure ()
      _  => do
        putStr $ unwords ["[", show lvl, "]", msg]
        pure ()

  endLogging logger = delete logger

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

max_stars_repo_name: jfdm/idris-common

max_issues_repo_name: jfdm/idris-common

max_forks_repo_name: jfdm/idris-common


text:
module Minecraft.Data.Type.As

import public Minecraft.Data.Type.Ctx
import public Minecraft.Data.Type.Vtbl

%default total

public export
record As kind where
  constructor New
  ctx : Ctx kind
  val : ctx.type
  {auto vtbl : Vtbl ctx.type}

export
new : {kind : Type -> Type} -> (type : Type) -> (val : type) -> (impl : kind type) => (vtbl : Vtbl type) => As kind
new {kind} type val @{impl} @{vtbl} = New ((#) type @{impl}) val @{vtbl}

export
app : forall r. {kind : Type -> Type} -> (x : As kind) -> (f : kind x.ctx.type => x.ctx.type -> r) -> r
app {kind} x f = f @{x.ctx.impl} x.val

export
cast : (kind : Type -> Type) -> As _ -> Maybe (As kind)
cast kind (New ctx val {vtbl}) = case vtable @{vtbl} (kind ctx.type) of
  Just impl => Just (New ((#) ctx.type {impl}) val @{vtbl})
  Nothing => Nothing

export
castApp : forall r. (kind : Type -> Type) -> (x : As _) -> (f : kind x.ctx.type => x.ctx.type -> r) -> Maybe r
castApp kind  (New ctx val {vtbl}) f = case vtable @{vtbl} (kind ctx.type) of
  Just impl => Just (f @{impl} val)
  Nothing => Nothing

max_stars_repo_name: po-stulate/postulate

max_issues_repo_name: po-stulate/postulate

max_forks_repo_name: po-stulate/postulate


text:
module Demo.Utils

%access public export
%default total

demoSquare : Num a => a -> a
demoSquare a = a * a

demoQuad : Num a => a -> a
demoQuad a = (demoSquare . demoSquare) a

max_stars_repo_name: roycrippen/scratch

max_issues_repo_name: roycrippen/scratch

max_forks_repo_name: roycrippen/scratch


text:
module Depling.Replace

import Depling
import Depling.Incr
import Utils
import Data.Fin
import Data.Vect

mutual
	total
	dReplace' : DAST n -> DAST n -> DAST n -> DAST n
	dReplace' rp ra (ʌ v) = ʌ v
	dReplace' rp ra (λ at b) = λ (dReplace rp ra at) (dReplace (incr FZ rp) (incr FZ ra) b)
	dReplace' rp ra (λT at rt) = λT (dReplace rp ra at) (dReplace (incr FZ rp) (incr FZ ra) rt)
	dReplace' rp ra (f =!= a) = dReplace rp ra f =!= dReplace rp ra a
	dReplace' rp ra 𝕋 = 𝕋
	dReplace' rp ra (𝔽 at rt b) =
		𝔽
			(dReplace (                    rp) (                    ra) at)
			(dReplace (          incr FZ $ rp) (          incr FZ $ ra) rt)
			(dReplace (incr FZ $ incr FZ $ rp) (incr FZ $ incr FZ $ ra) b )
	dReplace' rp ra (𝕌 n t) = 𝕌 n $ dReplace rp ra t
	dReplace' rp ra (ℂ cn as) = assert_total $ ℂ cn $ map (dReplace rp ra) as
	dReplace' rp ra (ℙ v cn t f) = ℙ (dReplace rp ra v) cn (dReplace (incr' rp) (incr' ra) t) (dReplace rp ra f)
	dReplace' rp ra (𝔹 t) = 𝔹 $ dReplace rp ra t

	total
	export
	dReplace : DAST n -> DAST n -> DAST n -> DAST n
	dReplace rp ra a = if a == rp then ra else dReplace' rp ra a

max_stars_repo_name: CoderPuppy/idris-depling

max_issues_repo_name: CoderPuppy/idris-depling

max_forks_repo_name: CoderPuppy/idris-depling


text:
module Main

import WordsProvider
import Data.List
import Data.List.Quantifiers

%language TypeProviders

%provide (seoWords : List String) with readWords "seo-words.txt"

numberInfixes : String -> Nat
numberInfixes word = length $ filter (\w => isInfixOf w word) $ filter (/= "") seoWords

say : (s:String) -> { auto prf : GT (numberInfixes s) Z } -> IO ()
say s = printLn s

main : IO ()
main = say "brand-1234"

max_stars_repo_name: janschultecom/seo-router

max_issues_repo_name: janschultecom/seo-router

max_forks_repo_name: janschultecom/seo-router


text:
module BinaryFormats.Data.Bit

%default total

||| A binary digit (either 0 or 1)
public export
data Bit : Type where
    ||| The 0 digit
    O : Bit
    ||| The 1 digit
    I : Bit

max_stars_repo_name: brendanzab/idris-power-of-pi

max_issues_repo_name: brendanzab/idris-power-of-pi

max_forks_repo_name: brendanzab/idris-power-of-pi


text:
module RFC.Greeter

import Effects
import Effect.StdIO
import Effect.Default
import Effect.State

import System.Protocol

%access public

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

-- Internal representations
data Command = GreetMe String | Help | Quit

-- How we display the internal representation for Command.
instance Show Command where
    show (GreetMe str) = ":greet " ++ show str
    show Quit = ":q"
    show Help = ":?"

-- -------------------------------------------------- [ Protocol Specification ]

GreeterProto : Type -> Type
GreeterProto t = Protocol ['Alice, 'Bob] ()

total
gBody : GreeterProto ()
gBody = do
    'Bob ==> 'Alice | String
    cmd <- 'Alice ==> 'Bob | Command
    case cmd of
      GreetMe str => do
        'Bob ==> 'Alice | String
        Rec gBody

      Help => do
        'Bob ==> 'Alice | String
        Rec gBody

      Quit => Done

total
greeter : GreeterProto () -> GreeterProto ()
greeter body = do
    'Alice ==> 'Bob | String
    body
    Done

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

max_stars_repo_name: jfdm/idris-protocol-examples

max_issues_repo_name: jfdm/idris-protocol-examples

max_forks_repo_name: jfdm/idris-protocol-examples


text:
module Idris.Main

import Compiler.Common
import Compiler.Erlang.Erlang
import Idris.Driver

main : IO ()
main = mainWithCodegens [("erlang", codegenErlang)]


text:
module TypeTrans.Array

-- Module to represent Vector types, we use
-- Array as it's not already a taken construct
-- in the Idris prelude

import Data.Vect
import Data.List

%default total

-- A Shape is a Vector which represents the structure
-- of an Array e.g. the shape of [[1,2,3],[1,2,3]] would be [2,3]
Shape : Type
Shape = List Nat

-- Rank represents the number of dimensions in an
-- Array, e.g. the rank of [[]] would be 2
Rank : Type
Rank = Nat

Array : Shape -> Type -> Type
Array [] t  = t
Array (v::vs) t = Vect v (Array vs t)

-- Give number of dimensions in the given Array
dim : Array xs t -> Nat
dim arr {xs} = length xs

-- Given a Vector returns the number of items
-- in the vector
length' : Vect n t -> Nat
length' v {n} = n

-- Give the shape of a given array
shape : Array xs t -> Shape
shape arr {xs} = xs

-- Gives a count of the total amount of elements in
-- a vector based on its dimensions
size : Array xs t -> Nat
size arr {xs} = foldr (*) 1 xs

-- Proof that a zero dimensional array cannot
-- contain more than zero dimensions
arrayCannotBeEmpty : Array (0::xs) t -> Void
arrayCannotBeEmpty (v::vs) impossible

-- | Lift a 0 dimensional Vector  into a 1 dimensional
--  Vector
singleton : Array (xs) t -> Array (1::xs) t
singleton t = [t]

-- | Inverse operation from singletonV, reduce dimension
-- of a 1 dimensional Vector with a single value into
-- a 0 dimensional Vector
invSingleton : Array (1::xs) t -> Array (xs) t
invSingleton [t] = t

-- | Map operation on an Array, maps
--   all base elements
mapA : (a -> b) -> Array xs a -> Array xs b
mapA f v {xs=[]}  = f v
mapA f v {xs = (y::ys)} = map (mapA f) v

mapM : Monad m => (a -> m b) -> Vect n a -> m (Vect n b)
mapM _ Nil = return Vect.Nil
mapM f (x::xs) = do
  x' <- f x
  xs' <- mapM f xs
  return (Vect.(::) x' xs')

mapM_ : Monad m => (a -> m b) -> Vect n a -> m ()
mapM_ _ Nil = return ()
mapM_ f (x::xs) = do
  f x
  mapM_ f xs

mapMA : Monad m => (a -> m b) -> Array xs a -> m (Array xs b)
mapMA f v {xs=[]} = f v
mapMA f v {xs = (y::ys)} = mapM (mapMA f) v

mapMA_ : Monad m => (a -> m b) -> Array xs a -> m ()
mapMA_ f v = do
  mapMA f v
  return ()

mapML : Monad m => (a -> m b) -> List a -> m (List b)
mapML _ [] = return []
mapML f (x::xs) = do
    x' <- f x
    xs' <- mapML f xs
    return (x'::xs')

mapML_ : Monad m => (a -> m b) -> List a -> m ()
mapML_ f v = do
  mapML f v
  return ()

-- | Reduce the dimensions of a 2+ dimensional vector
redDim : Array (x1::x2::xs) t -> Array (x1*x2::xs) t
redDim [] = []
redDim (v::vs) = v ++ redDim vs

-- | Flaten an Array down to 1 dimension
flattenA : Array (x::xs) t -> (n ** Array [S n] t)
flattenA v {x = Z} = void (arrayCannotBeEmpty v)
flattenA v {x=S m} {xs=[]}  = (_ ** v)
flattenA v {xs = (y::ys)} = (flattenA (redDim v))

-- | FoldL operation on Array
foldlA : (a -> b -> a) -> a -> Array (x::xs) b -> a
foldlA f e v with (flattenA v)
  | (_ ** v') = foldlA' f e v'
  where foldlA' : (a -> b -> a) -> a -> Array [(S ys)] b -> a
        foldlA' f e v = foldl f e v

-- | Foldl1 operation on an Array
foldlA1 : (a -> a -> a) -> Array (x::xs) a -> a
foldlA1 f v with (flattenA v)
  | (_ ** v') = foldlA1' f v'
  where foldlA1' : (a -> a -> a) -> Array [(S ys)] a -> a
        foldlA1' f v = foldl1 f v

-- | Transpose a 2+ dimensional Vector, switches first and second dimensions
transposeA : Array (x1::x2::xs) t -> Array (x2::x1::xs) t
transposeA = transpose

-- Given a 1+ dimensional Vector in which the size of the highest dimension
-- sz_d0 = m * n, increases the Vector by 1 dimension by taking m lots
-- of n values
incDim : Array (m * n::xs) t -> Array (m::n::xs) t
incDim v {m = Z}  = []
incDim v {m = S r} {n} =
    let (fstN, rest) = (take n v, drop n v) in
        fstN :: (incDim rest)

reshape' : Array (x1::(m * x2)::xs) t -> Array((x1 * m)::x2::xs) t
reshape' [] = []
reshape' (v::vs) = incDim v ++ reshape' vs

reshape : Array (x1::(m * x2)::xs) t -> Array ((m * x1)::x2::xs) t
reshape v {m} {x1} = rewrite (multCommutative m x1) in reshape' v

invReshape' : Array ((x1 * m)::x2::xs) t -> Array (x1::(m * x2)::xs) t
invReshape' v {x1 = Z} = []
invReshape' v {x1 =S r} = map redDim $ incDim v

invReshape : Array ((m * x1)::x2::xs) t -> Array (x1::(m * x2)::xs) t
invReshape v = invReshape' $ flip v
  where flip : Array ((m * x1)::x2::xs) t -> Array ((x1 * m)::x2::xs) t
        flip v {m} {x1} = rewrite multCommutative x1 m in v

-- Section for reshaping a vector keeping the dimensionality
-- the same except showing that the most outer dimension
-- is comprised of 2 factors multiplied together

-- Proof dividing 0 by a non zero number gives 0
divZProof : (m : Nat) -> (nz : Not (m = Z)) -> divNatNZ 0 m nz = 0
divZProof Z nz = void (nz Refl)
divZProof (S Z) _ = Refl
divZProof (S (S n)) _ = Refl

-- Proof modulo 0 by a non zero number gives 0
modZProof : (m : Nat) -> (nz : Not (m = Z)) -> modNatNZ 0 m nz = 0
modZProof Z nz = void (nz Refl)
modZProof (S Z) _ = Refl
modZProof (S (S n)) _ = Refl

-- Proof modNatNZ (m * n) n = 0
modMProof : (m : Nat) -> (n: Nat) -> {default SIsNotZ nz : Not (m = Z)} -> modNatNZ (mult m n) m nz = 0
modMProof Z _ {nz} = void (nz Refl)
modMProof _ Z ?= Z
modMProof m n ?= Z

-- TODO fill these out latee
TypeTrans.Array.modMProof_lemma_1 = proof
  intro
  intro
  exact believe_me Z

TypeTrans.Array.modMProof_lemma_2 = proof
  intro
  intro
  exact believe_me Z

-- Proof of the Quotient Remainder theorem for the specific
-- case of remainder = mod n m, and quotient = div n m
divModProof : (m : Nat) -> (n : Nat) ->
                           (nz : Not (m = Z)) ->
                           (n = m * (divNatNZ n m nz) + (modNatNZ n m nz))
divModProof Z _ nz = void (nz Refl) -- Contraction m /= Z by supplied nz proof
divModProof m Z nz ?= Z -- Proof when n = 0 for all m
divModProof m n nz ?= n

TypeTrans.Array.divModProof_lemma_1 = proof
  intros
  rewrite sym (divZProof m nz)
  rewrite sym (modZProof m nz)
  rewrite sym (plusZeroRightNeutral (mult m 0))
  rewrite sym (multZeroRightZero m)
  trivial

-- TODO Temporary "believe_me" proof, should be replaced
-- with the proof that n = m * (n `div` m) + (n `mod` m) if/when possible
TypeTrans.Array.divModProof_lemma_2 = proof
  intro
  intro
  exact believe_me n

-- Proof that when m divides n that n = m * (n / m) in the case of
-- integer division
factorDivProof : (m : Nat) -> (n : Nat) ->
                        (nz : Not (m = Z)) ->
                        (mz : modNatNZ n m nz = Z) -> n = m * (divNatNZ n m nz)

factorDivProof Z _ nz _ = void (nz Refl) -- Contradiction, m /= Z by supplied nz proof
factorDivProof m Z nz _ ?= Z
factorDivProof m n nz mz ?= n

TypeTrans.Array.factorDivProof_lemma_1 = proof
  intros
  rewrite sym (divZProof m nz)
  rewrite sym (multZeroRightZero m)
  trivial

-- Considering this is a special case of the Quotient Remainder theorem
-- (remainder = 0) we show that this is contained within it, and use that
-- proof to prove this proof
TypeTrans.Array.factorDivProof_lemma_2 = proof
  intros
  rewrite (plusZeroRightNeutral (m * divNatNZ n m nz))
  rewrite mz
  rewrite (divModProof m n nz)
  trivial

-- Given a Vector of size n and a natural number m, and the conditions that m | n and m != 0
-- transforms the Vector of size n into a  Vector of size (m * (n `div` m)) which is equivalent
reshapeByFactor : (m : Nat) -> Array (n::ns) t ->
                               {default SIsNotZ nz : Not (m = Z)} ->
                               {auto mz : modNatNZ n m nz = Z} ->
                               Array ((m * (divNatNZ n m nz))::ns) t

reshapeByFactor Z _ {nz} = void (nz Refl)
reshapeByFactor m xs {n} {nz} {mz} = rewrite sym (factorDivProof m n nz mz) in xs

-- Split in one step
splitA : (m : Nat) -> Array (n::ns) t ->
                               {default SIsNotZ nz : Not (m = Z)} ->
                               {auto mz : modNatNZ n m nz = Z} ->
                               Array (m ::(divNatNZ n m nz)::ns) t
splitA m a {mz} {nz} = incDim $ reshapeByFactor m a {mz = mz} {nz = nz}

-- Helper functions for reshaping Vectors instead of Arrays,
-- as Unification behaviour is being a bit strange atm,

-- Flatten a 2d vector into a 1d vector
merge : Vect x1 (Vect x2 t) -> Vect (x1 * x2) t
merge [] = []
merge (v::vs) = v ++ merge vs

incDimV : Vect (m * n) t -> Vect m (Vect n t)
incDimV v {m = Z}  = []
incDimV v {m = S r} {n} =
    let (fstN, rest) = (take n v, drop n v) in
        fstN :: (incDimV rest)

reshapeByFV : (m : Nat) -> Vect n t ->
                               {default SIsNotZ nz : Not (m = Z)} ->
                               {auto mz : modNatNZ n m nz = Z} ->
                               Vect (m * divNatNZ n m nz) t

reshapeByFV Z _ {nz} = void (nz Refl)
reshapeByFV m xs {n} {nz} {mz} = rewrite sym (factorDivProof m n nz mz) in xs

splitV : (m : Nat) -> Vect n t ->
                               {default SIsNotZ nz : Not (m = Z)} ->
                               {auto mz : modNatNZ n m nz = Z} ->
                               Vect m (Vect (divNatNZ n m nz) t)
splitV m a {mz} {nz} = incDimV $ reshapeByFV m a {mz = mz} {nz = nz}

doubleToNat : Double -> Nat
doubleToNat d = fromIntegerNat $ cast d

-- Generate all factors for a given number
factors : Nat -> List Nat
factors (S Z) = [(S Z)]
factors n = assert_total $ lows ++ (reverse $ map (div n) lows)
    where lows = filter ((== 0) . modNat n) [1..doubleToNat .floor . sqrt $ cast n]

-- Get all factors of the largest dimension in
-- the given Vector
factorsV : Array (x::xs) t -> List Nat
factorsV {x} _ = factors x

-- Generate all factor pairs of a given natural number
factorPairs : Nat -> List (Nat, Nat)
factorPairs n = assert_total $ map (\f => (f, div n f)) fs
  where fs = factors n

-- Sacrificing totality for functionality, split an Array into a higher
-- dimension
partial
splitA2 : (n : Nat) -> Array (x::xs) t -> Array (n :: div x n :: xs) t
splitA2 n xs {x} = split' n (div x n) (toList xs)
  where
        partial
        getN : (n : Nat) -> List t -> Vect n t
        getN Z l = []
        getN (S n) (x::xs) = x::(getN n xs)

        partial
        split' : (m : Nat) -> (n : Nat) -> List t -> Vect m (Vect n t)
        split' Z _ _ = []
        split' (S m) n xs = (getN n xs)::(split' m n (drop n xs))

infixr 5 !!;
partial
(!!) : {a : Type} -> List a -> Nat -> a
(x::xs) !! Z = x
(x::xs) !! (S n) = xs !! n

-- Split an array by the nth factor of its highest dimension,
-- returns a Sigma Type containing the given factor with the split array
partial
splitNFactor: (n : Nat) -> Array (x::xs) t -> (f : Nat ** Array (f :: div x f :: xs) t)
splitNFactor n xs {x} = (f ** (splitA2 f xs))
  where f = factors x !! n

-- Generate all possible vector combinations using the factors of the highest
-- dimension of the given vector, returns a list of sigma values containing the
-- largest dimension of each split array along with the split array itself
partial
splitFactors : Array (x::xs) t -> List (f : Nat ** Array (f :: div x f :: xs) t)
splitFactors xs {x} = map (\f => (f ** splitA2 f xs)) (factors x)

partial
convertFactors : (f ** Array (f :: div x f :: xs) t) -> (ys ** Array ys t)
convertFactors (f ** ys) {x} {xs} = assert_total $ ((f :: div x f :: xs) ** ys)

partial
splitFactorsGeneric : Array (x::xs) t -> List (ys ** Array ys t)
splitFactorsGeneric xs = map convertFactors $ splitFactors xs

toVect : Array (x::xs) t -> Vect x (Array xs t)
toVect = id

fromVect : Vect n t -> Array [n] t
fromVect = id

partial
printVect : (Show t) => Vect xs t -> IO()
printVect xs = do
  print "[ "
  mapM_ (\x => print x >>= \_ => print " ") xs
  print "]"

partial
printArr : (Show t) => Array xs t -> IO ()
printArr vs {t} = printArr' vs >>= \_ => putStrLn ""
  where
    printArr' : (Show t) => Array xs t -> IO ()
    printArr' v {xs=[]} = print v >>= \_ => putStr ""
    printArr' v {xs = (y::ys)} = do
      putStr "["
      case v of
        [] => putStr ""
        (a::as) => do
          mapM_ (\x => printArr' x >>= \_ => putStr ",") $ init (a::as)
          printArr' (last (a::as))

      putStr "]"

partial
printSigmaArr : (Show t) => (xs ** Array xs t) -> IO ()
printSigmaArr v {t} with (v)
  | (xs ** vs) = printArr vs {t}

partial
printArrs : (Show t) => List (xs ** Array xs t) -> IO ()
printArrs vs {t} = mapML_ (\v => printSigmaArr v {t}) vs

max_stars_repo_name: RossMeikleham/MSci-Project

max_issues_repo_name: RossMeikleham/MSci-Project

max_forks_repo_name: RossMeikleham/MSci-Project


text:
module Main

readString : String -> IO String
readString d = pure d

test : String -> IO ()
test s = do
  s' <- readString s
  printLn (the Double (cast s'), the Integer (cast s'), the Int (cast s'))

bigInteger : IO Integer
bigInteger = pure 9223372036854775808

main : IO ()
main = do
  test "42.5"
  test "-42.5"
  test "42"
  test "-42"
  test "foo"
  printLn !bigInteger


text:
import Data.Nat

partial fizzBuzzSimple: (x: Nat) -> String
fizzBuzzSimple x with (modNat x (the Nat 3), modNat x (the Nat 5))
  fizzBuzzSimple x | (Z, Z) = "fizzbuzz"
  fizzBuzzSimple x | (Z, _) = "fizz"
  fizzBuzzSimple x | (_, Z) = "buzz"
  fizzBuzzSimple x | _ = show x


text:
module Main

import HelloIdris2.Main

main : IO ()
main = do HelloIdris2.Main.multigreet

max_stars_repo_name: alexhumphreys/verpackung

max_issues_repo_name: alexhumphreys/verpackung

max_forks_repo_name: alexhumphreys/verpackung


text:
module Data.List.Elem.Extra

import Data.List
import Data.List.Elem

%default total

||| Proof that an element is still inside a list if we append to it.
public export
elemAppLeft : (xs, ys : List a) -> (prf : Elem x xs) -> Elem x (xs ++ ys)
elemAppLeft (x :: xs) ys Here = Here
elemAppLeft (x :: xs) ys (There prf2) = There $ elemAppLeft xs ys prf2

||| Proof that an element is still inside a list if we prepend to it.
public export
elemAppRight :  (ys, xs : List a) -> (prf : Elem x xs) -> Elem x (ys ++ xs)
elemAppRight [] xs prf = prf
elemAppRight (y :: ys) xs prf = There $ elemAppRight ys xs prf

||| Proof that membership on append implies membership in left or right sublist.
public export
elemAppLorR : (xs, ys : List a)
           -> (prf : Elem k (xs ++ ys))
           -> Either (Elem k xs) (Elem k ys)
elemAppLorR [] [] prf = absurd prf
elemAppLorR [] _ prf = Right prf
elemAppLorR (x :: xs) [] prf =
  Left $ rewrite sym $ appendNilRightNeutral xs in prf
elemAppLorR (x :: xs) _ Here = Left Here
elemAppLorR (x :: xs) ys (There prf) = mapFst There $ elemAppLorR xs ys prf

||| Proof that x is not in (xs ++ ys) implies proof that x is not in xs.
public export
notElemAppLeft : (xs, ys : List a)
              -> (prf : Not (Elem x (xs ++ ys)))
              -> Not (Elem x xs)
notElemAppLeft xs ys prf = prf . elemAppLeft xs ys

||| Proof that x is not in (xs ++ ys) implies proof that x is not in ys.
public export
notElemAppRight : (ys, xs : List a)
               -> (prf : Not (Elem x (xs ++ ys)))
               -> Not (Elem x ys)
notElemAppRight ys xs prf = prf . elemAppRight xs ys


text:
module Main

import Effects
import Effect.StdIO
import IdrisJvm.IO
import IdrisJvm.Effects

hello : Eff () [STDIO]
hello = do
  putStrLn "Hello world!"
  putChar 'b'
  putStrLn "ar"

main : JVM_IO ()
main = run hello


text:
module Arith

import Data.Primitives.Views

public export
randoms : Int -> Stream Int
randoms seed = let seed' = 1664525 * seed + 1013904223 in
                   (seed' `shiftR` 2) :: randoms seed'
public export
arithInputs : Int -> Stream Int
arithInputs seed = map bound (randoms seed)
  where bound : Int -> Int
        bound x with (divides x 12)
          bound ((12 * div) + rem) | (DivBy prf) = rem + 1

quiz : Stream Int -> (score : Nat) -> IO ()
quiz (n1 :: n2 :: ns) score =
     do putStrLn $ "Thy score: " ++ show score
        putStr $ show n1 ++ " * " ++ show n2 ++ "? "
        answer <- getLine
        if cast answer == n1 * n2
           then putStrLn "Correct" >>= \_ => quiz ns $ score + 1
           else putStrLn ("Wrong. Answer is: " ++ show (n1 * n2)) >>= \_ => quiz ns score

-- 11.1 Ex. # 1
every_other : Stream ty -> Stream ty
every_other (v1 :: v2 :: vs) = v2 :: every_other vs

max_stars_repo_path: Chapter 11/Arith.idr

max_issues_repo_path: Chapter 11/Arith.idr

max_forks_repo_path: Chapter 11/Arith.idr


text:
module Main

import Data.Vect
import Data.Stream

foo : List Char
foo = unpack $ pack $ take 4000 (repeat 'a')

factorialAux : Integer -> Integer -> Integer
factorialAux 0 a = a
factorialAux n a = factorialAux (n-1) (a*n)

factorial : Integer -> Integer
factorial n = factorialAux n 1

sum : Nat -> Nat
sum n = go 0 n where
  go : Nat -> Nat -> Nat
  go acc Z = acc
  go acc n@(S k) = go (acc + n) k

main : IO ()
main =
   do
      printLn $ factorial 100
      printLn $ factorial 10000
      printLn $ show $ the (Vect 3 String) ["red", "green", "blue"]
      printLn foo
      printLn (sum 50000)


text:
import Data.Buffer

main : IO ()
main = do Just buf <- newBuffer 40
          printLn (size buf)
          setInt buf 5 (-1024567890)
          setInt buf 36 1034567890
          setString buf 20 "Hello world!"

          printLn !(bufferData buf)

          setDouble buf 10 123.456

          val <- getInt buf 5
          printLn val
          val <- getInt buf 6
          printLn val

          val <- getDouble buf 10
          printLn val

          val <- getInt buf 36
          printLn val
          val <- getInt buf 37 -- out of bounds, expect 0
          printLn val

          str <- getString buf 20 10
          putStrLn str
          str <- getString buf 20 12
          putStrLn str
          str <- getString buf 200 12 -- out of bounds, expect ""
          printLn str
          str <- getString buf 35 12 -- out of bounds, expect ""
          printLn str

max_stars_repo_name: grin-compiler/idris-grin

max_issues_repo_name: grin-compiler/idris-grin

max_forks_repo_name: grin-compiler/idris-grin


text:
|||
|||
||| Module    : Context.idr
||| Copyright : (c) Jan de Muijnck-Hughes
||| License   : see LICENSE
|||
module Toolkit.DeBruijn.Context

import Decidable.Equality

import Data.DPair
import Data.Singleton

import Toolkit.Decidable.Informative

import Toolkit.Data.List.AtIndex
import Toolkit.Data.DList
import Toolkit.Data.DList.AtIndex

import Toolkit.DeBruijn.Context.Item

%default total

-- A reverse cons operator.
infixr 6 +=

namespace List
  ||| Append `x` to the head of `xs`.
  public export
  (+=) : List a -> a -> List a
  (+=) xs x = x :: xs

public export
Context : (kind : Type) -> (types : List kind) -> Type
Context kind = DList kind Item

export
extend : (ctxt  : Context kind types)
      -> (label : String)
      -> (type  : kind)
               -> Context kind (types += type)
extend ctxt label type
  = I label type :: ctxt

export
(+=) : (ctxt  : Context kind types)
    -> (label : String)
    -> (type  : kind)
             -> Context kind (types += type)
(+=) = extend

||| A quantifier over the context that the given predicate holds.
|||
||| This is modelled after De Bruijn indices, and the underlying
||| quantifier is `Any`.
|||
public export
data Exists : (kind : Type)
           -> (pred  : (type : kind) -> Type)
           -> (key   : String)
           -> {types : List kind}
           -> (ctxt  : Context kind types)
                    -> Type
  where
    E : {ctxt : Context kind types}
     -> {pred : (type : kind) -> Type}
     -> (type : kind)
     -> (item : Item type)
     -> (prf  : pred type)
     -> {loc  : Nat}
     -> (locC : HoldsAtIndex kind Item (Holds kind pred key) ctxt loc)
     -> (locN : AtIndex type types loc)
             -> Exists kind pred key ctxt

export
deBruijn : {ctxt : Context kind types}
        -> (prf  : Exists kind pred key ctxt)
                -> (type ** DPair Nat (AtIndex type types))
deBruijn (E type item prf locC locN)
  = (type ** _ ** locN)

namespace Exists
  public export
  data Error type = NotFound
                  | NotSatisfied type

isEmpty : Exists kind pred key [] -> Void
isEmpty (E _ _ _ (Here x) _) impossible
isEmpty (E _ _ _ (There contra later) _) impossible

notLater : (Holds  kind pred key  h      -> Void)
        -> (Exists kind pred key       t -> Void)
        ->  Exists kind pred key (h :: t)
        -> Void
notLater f g (E type item prf (Here x) locN) = f x
notLater f g (E type item prf (There contra later) (There x)) = g (E type item prf later x)

export
exists : {kind  : Type}
      -> {types : List kind}
      -> {pred  : (type : kind) -> Type}
      -> (func  : (type : kind) -> DecInfo err (pred type))
      -> (key   : String)
      -> (ctxt  : Context kind types)
               -> DecInfo (Exists.Error err)
                          (Exists kind pred key ctxt)

exists f _ []
  = No NotFound
       isEmpty
exists f key (head :: tail) with (holds f key head)
  exists f key ((I str x) :: tail) | (Yes (H prfK prf))
    = Yes (E _ (I str x) prf (Here (H prfK prf)) Here)

  exists f key (head :: tail) | (No msg contra) with (exists f key tail)
    exists f key (head :: tail) | (No msg contra) | (Yes (E type item prf locC locN))
      = Yes (E type item prf (There contra locC) (There locN))

    -- [ Note ]
    --
    -- we need to ensure that the 'correct' error message has been satisfied.
    exists f key (head :: tail) | (No (NotSatisfied x) contra) | (No msgR contraR)
      = No (NotSatisfied x)
           (notLater contra contraR)
    exists f key (head :: tail) | (No (WrongName x y) contra) | (No msgR contraR)
      = No msgR
           (notLater contra contraR)

namespace Lookup

  public export
  IsBound : {kind  : Type}
         -> {types : List kind}
         -> (key   : String)
         -> (ctxt  : Context kind types)
                  -> Type
  IsBound {kind} str ctxt
    = Exists kind Singleton
                str
                ctxt

  single : (item : kind)
                -> DecInfo () (Singleton item)
  single item = Yes (Val item)

  export
  lookup : {kind  : Type}
        -> {types : List kind}
        -> (str   : String)
        -> (ctxt  : Context kind types)
                 -> DecInfo (Exists.Error ())
                            (IsBound str ctxt)
  lookup = exists single

-- [ EOF ]

max_stars_repo_name: border-patrol/linear-circuits

max_issues_repo_name: border-patrol/linear-circuits

max_forks_repo_name: border-patrol/linear-circuits


text:
||| Module tries to implement all the friendly methods provided by the Haskell datatime library.
module Data.DateTime

import Data.Time.Clock.Internal.UTCTime
import Data.Time.Clock.System
import Data.Time.Clock.Internal.SystemTime
import Data.Time.Calendar.Gregorian
import Internal.CTimespec
import Data.Time.Calendar.Days
import Data.Time.Clock.Internal.DiffTime
import Data.Time.Calendar.Days
import Data.Time.LocalTime.Internal.TimeOfDay

import Data.Fin

||| A structure that stores MJD as Days and Diff time
DateTime: Type
DateTime = UTCTime

||| Return the Gregorian date based on the call to machine's getSystemTime
public export
today : IO Gregorian
today = do
  let (MkUTCTime x y) = systemToUTCTime !getSystemTime
  pure $ toGregorian x

||| Add days to Gregorian
public export
addDays: Gregorian -> Nat -> Gregorian
addDays gregorian n =
  let
    x = fromGregorian gregorian
    new_gregororian = addDays (cast n) x
  in
    toGregorian new_gregororian

||| Build the DateTime object based on machince getSystemTime
public export
getUTCTime: IO DateTime
getUTCTime = pure $ systemToUTCTime !getSystemTime

||| Return the current TimeOfDay based on machine's getSystemTime
public export
getCurrentUTCTimeOfDay : IO TimeOfDay
getCurrentUTCTimeOfDay = do
  utcTime <- getUTCTime
  pure $ timeToTimeOfDay (utctDayTime utcTime)

max_stars_repo_name: gdevanla/idris-time

max_issues_repo_name: gdevanla/idris-time

max_forks_repo_name: gdevanla/idris-time


text:
module Relative

public export
record Relative where
  constructor CreateRelative
  id : Either String Integer
  name : Either Integer String
  type : Integer

max_stars_repo_name: GrandArchTemplar/IdrisVKAPI

max_issues_repo_name: GrandArchTemplar/IdrisVKAPI

max_forks_repo_name: GrandArchTemplar/IdrisVKAPI


text:
module Data.Bytes.Strict.Internal

import Data.Bytes.Util
import Data.Bytes.Prim

import Data.Word.Word8

import Data.Strings -- fastAppend
import Data.List    -- intersperse
import Data.So      -- for our NonEmpty

%default total

private
moduleName : String
moduleName = "Data.Bytes.Strict.Internal"

-- Our Bytes type, a Ptr to a `block` of memory, the current 0-based offset
-- into that memory, its size in bytes.
public export
data Bytes : Type where
  MkB : (b : Block) -> (pos : Int) -> (len : Int) -> Bytes

-- It'd be nice to be able to provide NonEmpty based on `len` but it's quite a
-- hassle to have a Nat here with the various castings around the codebase and
-- other concerns.

public export
data NonEmpty : Bytes -> Type where
  IsNonEmpty : So (len > 0) -> NonEmpty (MkB _ _ len)

-- ^ how can I provide this proof without making the user need access
-- to MkB? Simply by having my own functions imlpicity prove that when
-- used? Things like cons and singleton and append? And if a
-- ByteString comes from elsewhere we use Dec?

-- This is here instead of in a 'where' due to a current coverage checking bug
private
soNotSonot' : So x -> So (not x) -> Void -- So x -> Not (So (not x))
soNotSonot' Oh Oh impossible

export -- Does this need public export or is being Dec enough for proofs?
isNonEmpty : (b : Bytes) -> Dec (NonEmpty b)
isNonEmpty (MkB _ _ len) with (choose (len > 0))
  isNonEmpty (MkB _ _ len) | (Left t) = Yes (IsNonEmpty t)
  isNonEmpty (MkB _ _ len) | (Right f) = No (\(IsNonEmpty t) => soNotSonot' t f)

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

{- NB: In the bytestring lib of haskell they use unsafePerformIO
because of how the strictness analzer and sharing works, they note:
The use of unsafePerformIO in allocating functions (unsafeCreate) is critical!

Otherwise:
 singleton 255 `compare` singleton 127
is compiled to:
 case mallocByteString 2 of
     ForeignPtr f internals ->
          case writeWord8OffAddr# f 0 255 of _ ->
          case writeWord8OffAddr# f 0 127 of _ ->
          case eqAddr# f f of
                 False -> case compare (GHC.Prim.plusAddr# f 0)
                                       (GHC.Prim.plusAddr# f 0)
TODO: Find out if this distinction is true in idris.
-}

export
unsafeCreateBytes : Int -> (MutBlock -> IO ()) -> Bytes
unsafeCreateBytes len f = unsafePerformIO $ do
    b <- allocateAndFill len f
    pure (MkB b 0 len)

export
unsafeCreateNBytes : Int -> (MutBlock -> IO Int) -> Bytes
unsafeCreateNBytes len f = unsafePerformIO $ do
    (b, i) <- allocateAndFillToN len f
    pure (MkB b 0 i)

export
unsafeCreateNBytes' : Int -> (MutBlock -> IO (Int,a)) -> (Bytes, a)
unsafeCreateNBytes' len f = unsafePerformIO $ do
    (b, i, a) <- allocateAndFillToN' len f
    pure ((MkB b 0 i), a)

export
unsafeCreateAndTrim : Int -> (MutBlock -> IO Int) -> Bytes
unsafeCreateAndTrim len0 f = unsafePerformIO $ do
    (b, len) <- allocateAndTrim len0 f
    pure (MkB b 0 len)

-- This is internal so NonEmpty is used to keep the library maker honest.
-- TODO: Why is NonEmpty for List available here? I have not imported
-- Data.List!
export
packUpToNBytes : Int -> (l : List Word8) -> (Bytes, List Word8)
packUpToNBytes len xs0 = unsafeCreateNBytes' len $ \p => go p len 0 xs0
  where
    go : MutBlock -> Int -> Int -> List Word8 -> IO (Int, List Word8)
    go b n pos [] = pure (len - n, [])
    go b 0 pos xs = pure (len, xs)
    go b n pos (x :: xs) = setByte b pos x *> go b (n-1) (pos+1) xs

-- Unpacking bytestrings into lists effeciently is a tradeoff: on the one hand
-- we would like to write a tight loop that just blats the list into memory, on
-- the other hand we want it to be unpacked lazily so we don't end up with a
-- massive list data structure in memory.
--
-- Our strategy is to combine both: we will unpack lazily in reasonable sized
-- chunks, where each chunk is unpacked strictly.
--
-- unpackBytes and unpackChars do the lazy loop, while unpackAppendBytes and
-- unpackAppendChars do the chunks strictly.

-- unpackBytes : Bytes -> List Word8

-- Intended complexity: O(n+m)
-- No need to export, simply use <+>
private
append : Bytes -> Bytes -> Bytes
append (MkB xs xpos xlen) (MkB ys ypos ylen)
  = unsafeCreateBytes (xlen + ylen) $ \p => do
      copyBlock xs xpos xlen p 0
      copyBlock ys ypos ylen p xlen

-- Debug use ONLY, **don't ever use this**, bytes are not characters!
-- Further, this shows the whole block, not just the live part.
-- TODO: Remove this down the road, or  otherwise prevent it from escaping this
-- package. If a person wants to Show/Read/OverloadedString Bytes they should
-- create a principled package that does this. Bytes are not Strings.
export
Show Bytes where
  show (MkB b pos len) = "MkB " ++ show_block b ++ " " ++ show pos ++ " " ++ show len
    where
      show_block : Block -> String
      show_block buf
        = "[" ++ fastAppend (intersperse ","
            (map show . unsafePerformIO $ blockData buf)) ++ "]"

private
compareBytes : Bytes -> Bytes -> Ordering
compareBytes (MkB _  _    0   ) (MkB _  _    0   ) = EQ
compareBytes (MkB xb xpos xlen) (MkB yb ypos ylen) =
    unsafePerformIO $ go (xlen-1) (ylen-1) xb yb
  where
    go : Int -> Int -> Block -> Block -> IO Ordering
    go 0 0 xb yb = [| getByte xb xpos `compare` getByte yb ypos |]
    go 0 _ _ _   = pure LT
    go _ 0 _ _   = pure GT
    go k j xb yb
      = do EQ <- [| getByte xb (xpos + k) `compare` getByte yb (ypos + j) |]
             | res => pure res
           assert_total $ go (k-1) (j-1) xb yb

-- Offset will tend to be 0 so we first compare length, then block object
-- equality, then offset. The block should be a simple ptr comparison so it's
-- worth doing before trying for a full compareBytes. This order is partly
-- because it makes sense and partly because ByteString does it this way.
-- However I'm not sure why length is checked before block object equality,
-- perhaps in ghc length has a cheaper comparison than than the extra
-- foreignPtr prodding that ptr equality needs.

-- To ask if we are nominally equal.
infixl 9 `basicEq`
private
basicEq : Bytes -> Bytes -> Bool
MkB xb xpos xlen `basicEq` MkB yb ypos ylen
    = xlen == ylen && (unsafePerformIO (exactEqBlock xb yb) && xpos == ypos)

export
implementation
Eq Bytes where
  x == y = x `basicEq` y || compareBytes x y == EQ

-- basicEq is much speedier than compareBytes, use it when possible!
export
Ord Bytes where
  compare = compareBytes
  x >= y = x `basicEq` y || compareBytes x y == GT
  x <= y = x `basicEq` y || compareBytes x y == LT

export
Semigroup Bytes where
  (<+>) = append

-- Is there any way to make this a unique object? There's no real reason to
-- have this be anything other than the null ptr. Or at the very least there's
-- no reason to ever create more than one.
-- TODO: Investigate this as backends develop ^
export
Monoid Bytes where
  neutral = unsafeCreateBytes 0 (\_ => pure ())

-- Other things down the road that might need to concat, e.g.
-- sconcat/mconcat/foldMap should use this since it avoids a ton of copying by
-- checking the required size upfront. The idea here is to first compute the
-- size of the Bytes we need to make and then fill it. Despite going over the
-- list twice this makes it significantly faster than piece-wise methods that
-- must copy over and over to build up.
-- TODO: test this!
-- TODO: This could be even faster with a foldl style library that traverses the
-- list only once
-- NB: Unlike for allocation the crash here is for bad behavior (overflow) so it
-- would not be correct to lie about its totality. To that end we should want to
-- create a different total concat later to reduce partiality infection.
export
partial
concat : List Bytes -> Bytes
concat bs = let maxlen = getLen bs
            in  unsafeCreateBytes maxlen (go 0 (maxlen-1) bs)
  where
    partial
    getLen : List Bytes -> Int
    getLen [] = 0                -- Check overflow of Int, which would be bad.
    getLen (MkB _ _ len :: bs) = checkedAdd moduleName "concat" len (getLen bs)

    go : (buf_pos : Int) -> (end : Int) -> List Bytes -> MutBlock -> IO ()
    go n_pos end [] buf = pure ()
    go n_pos end (MkB b pos len :: bs) buf
      = if n_pos > end then pure ()
                       else do copyBlock b pos len buf n_pos
                               go (n_pos + len) end bs buf

export
total
concat' : List Bytes -> Maybe Bytes
concat' bs = let maxlen = getLen bs
             in (\l => unsafeCreateBytes l (go 0 (l-1) bs)) <$> maxlen
  where
    getLen : List Bytes -> Maybe Int
    getLen [] = Just 0                -- Check overflow of Int, which would be bad.
    getLen (MkB _ _ len :: bs) =
      getLen bs >>= \v => let v = len + v
                          in if v >= 0 then Just v
                                       else Nothing

    go : (buf_pos : Int) -> (end : Int) -> List Bytes -> MutBlock -> IO ()
    go n_pos end [] buf = pure ()
    go n_pos end (MkB b pos len :: bs) buf
      = if n_pos > end then pure ()
                       else do copyBlock b pos len buf n_pos
                               go (n_pos + len) end bs buf


text:
||| Copyright 2016 Google Inc.
|||
||| Licensed under the Apache License, Version 2.0 (the "License");
||| you may not use this file except in compliance with the License.
||| You may obtain a copy of the License at
|||
|||     http://www.apache.org/licenses/LICENSE-2.0
|||
||| Unless required by applicable law or agreed to in writing, software
||| distributed under the License is distributed on an "AS IS" BASIS,
||| WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
||| See the License for the specific language governing permissions and
||| limitations under the License.
|||
||| A small unit testing framework.

module Test.UnitTest

import Protobuf.Util

%access export

public export Test : Type -> Type
Test = Either String

failAssert : String -> Test a
failAssert err = Left err

assertEq : (Eq a, Show a) => (given : a) -> (expected : a) -> Test ()
assertEq g e = if g == e
  then return ()
  else failAssert ("assertEq failed: got " ++ (show g) ++ ", expected " ++ (show e))

assertEq' : Eq a => (given : a) -> (expected : a) -> Test ()
assertEq' g e = if g == e
    then return ()
    else failAssert "assertEq Failed"

record TestCase where
  constructor MkTestCase
  name : String
  test : Test ()

runTestCase : String -> TestCase -> IO ()
runTestCase f c = let fullname = f ++ "." ++ (name c) in do {
    putStrLn $ "[ RUN      ] " ++ fullname
    case (test c) of
      Left err => do {
        putStrLn err
        putStrLn $ "[   FAILED ] " ++ fullname
      }
      Right () => putStrLn $ "[       OK ] " ++ fullname
}

record TestFixture where
  constructor MkTestFixture
  name : String
  tests : List TestCase

runTests : TestFixture -> IO ()
runTests f = do {
  forEach (runTestCase (name f)) (tests f)
}

max_stars_repo_name: google/idris-protobuf

max_issues_repo_name: google/idris-protobuf

max_forks_repo_name: google/idris-protobuf


text:
import System
import System.Errno

main : IO ()
main = do
  -- `2` is `ENOENT` on all OS
  -- and the message is the same on all OS
  let s = strerror 2
  True <- pure (s == "No such file or directory")
    | False => do
      putStrLn ("strerror for 2 is " ++ s)
      exitFailure
  pure ()


text:
module Main

import Control.Monad.State
import Data.Fin
import Data.List
import Data.Nat
import Data.SortedMap
import Data.Vect

data Wire : Type where
  MkWire : Int -> Wire

Eq Wire where
  (MkWire a) == (MkWire b) = a == b

Ord Wire where
  compare (MkWire a) (MkWire b) = compare a b

Show Wire where
  show (MkWire a) = "wire(" ++ show a ++ ")"

data Component : Type where
  Nand : (a : Wire) -> (b : Wire) -> (aNandB : Wire) -> Component
  One : (alwaysOne : Wire) -> Component
  Zero : (alwaysZero : Wire) -> Component
  Observer : (tag : String) -> Wire -> Component
  Relay : (in' : Wire) -> (out : Wire) -> Component
  -- Boot : Wire -> Component

Show Component where
  show (Nand a b o) = show o ++ "=" ++ "~(" ++ show a ++ "&" ++ show b ++ ")"
  show (One w) = show w ++ "=1"
  show (Zero w) = show w ++ "=0"
  show (Observer tag w) = tag ++ "=" ++ show w
  show (Relay i o) = show o ++ "=" ++ show i
  -- show (Boot w) = show w ++ "=<boot>"

Circuit : Type
Circuit = List Component

record BuilderState where
  constructor MkBuilderState
  wireCounter : Int
  circuit : List Component

CircuitBuilder : Type -> Type
CircuitBuilder = State BuilderState

runCircuitBuilder : CircuitBuilder a -> Circuit
runCircuitBuilder = circuit . execState (MkBuilderState 0 [])

newWire : CircuitBuilder Wire
newWire = do
  wire <- gets wireCounter
  modify record { wireCounter $= (+ 1) }
  pure (MkWire wire)

addComponents : List Component -> CircuitBuilder ()
addComponents ts = modify record { circuit $= (ts ++) }

observe : String -> Wire -> CircuitBuilder ()
observe tag w = addComponents [ Observer tag w ]

combinatorial : (Wire -> CircuitBuilder (List Component)) -> CircuitBuilder Wire
combinatorial f = do
  out <- newWire
  comps <- f out
  addComponents comps
  pure out

relay : Wire -> CircuitBuilder Wire
relay w = combinatorial \out =>
  pure [ Relay w out ]

relay_ : Wire -> Wire -> CircuitBuilder ()
relay_ i o = addComponents [ Relay i o ]

delay : Nat -> Wire -> CircuitBuilder Wire
delay 0 w = pure w
delay (S k) w = relay w >>= delay k

-- boot : Wire -> CircuitBuilder ()
-- boot w = addComponents [ Boot w ]

nand : Wire -> Wire -> CircuitBuilder Wire
nand a b = combinatorial \out =>
  pure [ Nand a b out ]

nand_ : Wire -> Wire -> Wire -> CircuitBuilder ()
nand_ a b o = addComponents [ Nand a b o ]

one : CircuitBuilder Wire
one = combinatorial \out =>
  pure [ One out ]

one_ : Wire -> CircuitBuilder ()
one_ w = addComponents [ One w ]

zero : CircuitBuilder Wire
zero = combinatorial \out =>
  pure [ Zero out ]

zero_ : Wire -> CircuitBuilder ()
zero_ w = addComponents [ Zero w ]

not : Wire -> CircuitBuilder Wire
not a = nand a !one

not_ : Wire -> Wire -> CircuitBuilder ()
not_ a na = addComponents [ Nand a !one na ]

and : Wire -> Wire -> CircuitBuilder Wire
and a b = not !(nand a b)

or : Wire -> Wire -> CircuitBuilder Wire
or a b = nand !(not a) !(not b)

xor : Wire -> Wire -> CircuitBuilder Wire
xor a b = and !(nand a b) !(or a b)

nor : Wire -> Wire -> CircuitBuilder Wire
nor a b = not !(or a b)

nor_ : Wire -> Wire -> Wire -> CircuitBuilder ()
nor_ a b o = not_ !(or a b) o

halfAdder : Wire -> Wire -> CircuitBuilder (Wire, Wire)
halfAdder a b = [| (xor a b, and a b) |]

fullAdder : Wire -> Wire -> Wire -> CircuitBuilder (Wire, Wire)
fullAdder a b carryIn = do
  (sum1, carry1) <- halfAdder a b
  (sum2, carry2) <- halfAdder sum1 carryIn
  pure (sum2, !(or carry1 carry2))

Byte : Type
Byte = Vect 8 Wire

dFoldL : {n : Nat}
  -> (0 motive : Nat -> Type)
  -> (forall p. motive p -> a -> motive (S p))
  -> motive 0
  -> Vect n a
  -> motive n
dFoldL {n} motive f acc v = rewrite sym $ plusZeroRightNeutral n in helper acc v
  where
    helper : {q, m : Nat} -> motive m -> Vect q a -> motive (q + m)
    helper acc Nil = acc
    helper {q = S q, m} acc (x :: xs) = rewrite plusSuccRightSucc q m in helper (f acc x) xs

byteAdder : Byte -> Byte -> Wire -> CircuitBuilder (Byte, Wire)
byteAdder as bs carryIn = dFoldL (\n => CircuitBuilder (Vect n Wire, Wire)) (\ms, ab => f !ms ab) (pure (Nil, carryIn)) (zipWith (,) as bs)
  where
    f : (Vect n Wire, Wire) -> (Wire, Wire) -> CircuitBuilder (Vect (S n) Wire, Wire)
    f (os, c) (a, b) = do
      (o, c') <- fullAdder a b c
      pure (snoc os o, c')

binsToConsts : Vect n (Fin 2) -> CircuitBuilder (Vect n Wire)
binsToConsts = traverse \b =>
  case b of
    1 => one
    0 => zero

-- binsToBootedWires : Vect n (Fin 2) -> CircuitBuilder (Vect n Wire)
-- binsToBootedWires = traverse \b => do
--   w <- newWire
--   if b == 1 then boot w else pure ()
--   pure w

clock : (halfWidthMinusOne : Nat) -> CircuitBuilder Wire
clock n = do
  w <- newWire
  i <- delay n w
  not_ i w
  pure i

gatedSRLatch_ : (set : Wire) -> (reset : Wire) -> (enable : Wire)
  -> (q : Wire) -> (nq : Wire) -> CircuitBuilder ()
gatedSRLatch_ s r e q nq= do
  s' <- and s e
  r' <- and r e
  nor_ r' nq q
  nor_ s' q nq
  pure ()

gatedSRLatch : (set : Wire) -> (reset : Wire) -> (enable : Wire) -> CircuitBuilder (Wire, Wire)
gatedSRLatch s r e = do
  q <- newWire
  nq <- newWire
  gatedSRLatch_ s r e q nq
  pure (q, nq)

gatedDLatch : (data' : Wire) -> (enable : Wire) -> CircuitBuilder (Wire, Wire)
gatedDLatch d e = gatedSRLatch d !(not d) e

dFlipFlop_ : (data' : Wire) -> (clock : Wire) -> (dataNext : Wire) -> CircuitBuilder ()
dFlipFlop_ d clk dn = do
  (q, nq) <- gatedDLatch d !(not clk)
  dummy <- newWire
  gatedSRLatch_ q nq clk dn dummy

dFlipFlop : (data' : Wire) -> (clock : Wire) -> CircuitBuilder Wire
dFlipFlop d clk = do
  dn <- newWire
  dFlipFlop_ d clk dn
  pure dn

data Signal = High | Low

Show Signal where
  show High = "1"
  show Low = "0"

data CircuitState
  = Valid (SortedMap Wire Signal)
  | Invalid

Show CircuitState where
  show (Valid cstate) = show cstate
  show Invalid = "invalid circuit state"

Semigroup CircuitState where
  Invalid <+> _ = Invalid
  _ <+> Invalid = Invalid
  Valid a <+> Valid b = toCS . sequence $ mergeWith m (map Just a) (map Just b)
    where
      m : Maybe Signal -> Maybe Signal -> Maybe Signal
      m (Just High) (Just High) = Just High
      m (Just Low) (Just Low) = Just Low
      m _ _ = Nothing

      toCS : Maybe (SortedMap Wire Signal) -> CircuitState
      toCS (Just cs) = Valid cs
      toCS Nothing = Invalid

Monoid CircuitState where
  neutral = Valid empty

lookupSignal : Wire -> CircuitState -> Maybe Signal
lookupSignal w (Valid cs) = lookup w cs
lookupSignal w Invalid = Nothing

initialState : Circuit -> CircuitState
initialState = concat . map toMap
  where
    toMap : Component -> CircuitState
    toMap (Nand a b c) = Valid . fromList $ [ (a, Low), (b, Low), (c, Low) ]
    toMap (One w) = Valid . fromList $ [ (w, Low) ]
    toMap (Zero w) = Valid . fromList $ [ (w, Low) ]
    toMap (Observer _ w) = Valid . fromList $ [ (w, Low) ]
    toMap (Relay i o) = Valid . fromList $ [ (i, Low), (o, Low) ]
    -- toMap (Boot w) = Valid . fromList $ [ (w, High) ]

count : (n : Nat) -> Vect n Nat
count 0 = Nil
count (S n) = snoc (count n) n

runCircuit : Circuit -> CircuitState-> CircuitState
runCircuit comps cstate = concat . map drive $ comps
  where
    signalNand : Signal -> Signal -> Signal
    signalNand High High = Low
    signalNand High Low = High
    signalNand Low High = High
    signalNand Low Low = High

    drive : Component -> CircuitState
    drive (Nand a b o) =
      let as = lookupSignal a cstate
          bs = lookupSignal b cstate
      in case (as, bs) of
        (Just asig, Just bsig) => Valid . fromList $ [ (o, signalNand asig bsig) ]
        _ => Invalid
    drive (One w) = Valid . fromList $ [ (w, High) ]
    drive (Zero w) = Valid . fromList $ [ (w, Low) ]
    drive (Observer _ w) = Valid empty
    drive (Relay i o) =
      case lookupSignal i cstate of
        Just isig => Valid . fromList $ [ (o, isig) ]
        Nothing => Invalid
    -- drive (Boot w) = Valid empty

Observations : Type
Observations = List (String, Signal)

getObservations : Circuit -> CircuitState -> Observations
getObservations comps (Valid cstate) = concatMap ob $ comps
  where
    ob : Component -> List (String, Signal)
    ob (Observer tag w) =
      case lookup w cstate of
        Just sig => [ (tag, sig) ]
        Nothing => []
    ob _ = []
getObservations _ Invalid = []

putObservationsLn : Observations -> IO ()
putObservationsLn = (>> putChar '\n') . traverse f
  where
    f : (String, Signal) -> IO ()
    f (tag, sig) = putStr $ tag ++ "=" ++ show sig ++ ", "

exampleAdder : Circuit
exampleAdder = runCircuitBuilder $ do
  const2 <- binsToConsts [ 0, 1, 0, 0, 0, 0, 0, 0 ]
  const3 <- binsToConsts [ 1, 1, 0, 0, 0, 0, 0, 0 ]
  (shouldBe5, shouldBe0) <- byteAdder const2 const3 !zero
  let indexed5 = zipWith (,) shouldBe5 (count 8)
  traverse (\(w, n) => observe ("out[" ++ show n ++ "]") w) indexed5
  observe "out_carry" shouldBe0

exampleClock : Nat -> Circuit
exampleClock n = runCircuitBuilder $ do
  c <- clock n
  observe "clock" c

exampleLatch : Circuit
exampleLatch = runCircuitBuilder $ do
  (q, nq) <- gatedSRLatch !zero !one !one
  observe "q" q
  observe "~q" nq

exampleDff : Circuit
exampleDff = runCircuitBuilder $ do
  clk <- clock 40
  observe "clk" clk
  dFlipFlop !one clk >>= observe "dn"

main : IO ()
main =
  let exm = exampleDff
  in map (const ()) . traverse (putObservationsLn . getObservations exm) . iterateN 200 (runCircuit exm) . initialState $ exm

max_stars_repo_name: nicball/playground

max_issues_repo_name: nicball/playground

max_forks_repo_name: nicball/playground


text:
-- Dummy
module System.IO.Handle


text:
module Text.Markdown.Definition

-- Inline ----------------------------------------------------------

data Literal = MkLiteral String

data InlineTag = Str
               | SoftBreak
               | LineBreak
               | Code
               | RawHtml
               | Entity
               | Emph
               | Strong
               | Link
               | Image

mutual
  data Inline = NullInline | MkInline Inline'

  record Linkable : Type where
         MkLinkable : (label : Inline) ->
                      (url   : String) ->
                      (title : String) ->
                      Linkable

  data Content = NullContent
               | MkLiteralContent  Literal
               | MkInlineContent   Inline
               | MkLinkableContent Linkable

  record Inline' : Type where
         MkInline' : (tag     : InlineTag) ->
                     (content : Content  ) ->
                     (next    : Inline   ) ->
                     Inline'

-- Block -----------------------------------------------------------

data BlockTag = Document
              | BlockQuote
              | GenericList
              | GenericListItem
              | FencedCode
              | IndentedCode
              | HtmlBlock
              | Paragraph
              | AtxHeader
              | SetExtHeader
              | HRule
              | ReferenceDef

data ListType = Bullet
              | Ordered

data Delimiter = Period
               | Parens

record ListData : Type where
       MkListData : (listType     : ListType ) ->
                    (markerOffset : Int      ) ->
                    (padding      : Int      ) ->
                    (start        : Int      ) ->
                    (delimiter    : Delimiter) ->
                    (bulletChar   : Char     ) ->
                    (tight        : Bool     ) ->
                    ListData

record FencedCodeData : Type where
       MkFencedCodeData : (fenceLength : Int   ) ->
                          (fenceOffset : Int   ) ->
                          (fenceChar   : Char  ) ->
                          (info        : String) ->
                          FencedCodeData

data HeaderLevel = MkHeaderLevel Int

-- data RefMap --FIXME!

data Attributes = NullAttributes
                | MkListDataAttributes       ListData
                | MkFencedCodeDataAttributes FencedCodeData
                | MkHeaderLevelAttributes    HeaderLevel
                -- | MkRefMapAttributes      RefMap --FIXME!

mutual
  data Block = NullBlock | MkBlock Block'

  record Block' : Type where
         MkBlock' : (tag           : BlockTag  ) ->
                    (startLine     : Int       ) ->
                    (startColumn   : Int       ) ->
                    (endLine       : Int       ) ->
                    (open          : Bool      ) ->
                    (lastLineBlank : Bool      ) ->
                    (children      : Block     ) ->
                    (stringContent : String    ) ->
                    (inlineContent : Inline    ) ->
                    (attributes    : Attributes) ->
                    (next          : Block     ) ->
                    Block'

-- Markdown --------------------------------------------------------

record Meta : Type where
       MkMeta : (source : String) ->
                Meta

record Markdown : Type where
       MkMarkdown : (meta   : Meta      ) ->
                    (blocks : List Block) ->
                    Markdown

-- Show instance ---------------------------------------------------

instance Show Block where
         show NullBlock = show "NullBlock"
         show (MkBlock block') = show "MkBlock" --FIXME!

instance Show Markdown where
         show (MkMarkdown meta blocks) = show $ source meta

max_stars_repo_name: soimort/idris-commonmark

max_issues_repo_name: soimort/idris-commonmark

max_forks_repo_name: soimort/idris-commonmark


text:
module ElemsAreSame
import Data.Vect
--=======================================================================================================
--=======================================================================================================
--Elems are same
--=======================================================================================================
--=======================================================================================================
public export data ElemsAreSame : (xs:Vect n e) -> (ys:Vect n e) -> Type where
    ||| Empty vectors are the same
    NilIsNil :
        ElemsAreSame Nil Nil
    ||| Prepending x to two vectors with the same elements
    ||| Gives two vectors which still have the same elements
    PrependXIsPrependX :
        (x:e) -> ElemsAreSame zs zs' ->
        ElemsAreSame (x::zs) (x::zs')
    ||| Given two elements x and y
    ||| and a proof that two vectors zs and zs' have the same elements
    |||
    PrependXYIsPrependYX :
        (x:e) -> (y:e) -> ElemsAreSame zs zs' ->
        ElemsAreSame (x::(y::zs)) (y::(x::(zs')))
    -- NOTE: Probably could derive this last axiom from the prior ones
    SamenessIsTransitive :
        ElemsAreSame xs zs -> ElemsAreSame zs ys ->
        ElemsAreSame xs ys

export sameListsAreSame: (xs: Vect n e) -> ElemsAreSame xs xs
sameListsAreSame [] = NilIsNil
sameListsAreSame (x :: xs) = PrependXIsPrependX x (sameListsAreSame xs)

swap: ElemsAreSame xs ys -> ElemsAreSame ys xs
swap NilIsNil = NilIsNil
swap (PrependXIsPrependX x y) = PrependXIsPrependX x (swap y)
swap (PrependXYIsPrependYX x y z) = PrependXYIsPrependYX y x (swap z)
swap (SamenessIsTransitive x y) = SamenessIsTransitive (swap y)
                     (SamenessIsTransitive y (swap (SamenessIsTransitive x y)))

export swapHeads: ElemsAreSame (x::y::zs) us -> ElemsAreSame (y::x::zs) us
swapHeads {x} {y} {zs} {us} e = let xYIsYX = PrependXYIsPrependYX y x (sameListsAreSame zs) in
                                    SamenessIsTransitive xYIsYX e


text:
data A : Type where
  The : Type -> A

U : A -> Type
U (The x) = x

works : (a : A) -> (H : U a) -> (let q = H in Nat)
works a h = 0

fails : (a : A) -> (H : U a) -> (let q : U a = H in Nat)
fails a h = 0

dolet : Maybe Int -> Maybe Int -> Maybe Int
dolet x y
    = do let Just x' : Maybe Int = x
             | Nothing => Nothing
         y' <- y
         pure (x' + y')

dolet2 : Maybe Int -> Maybe Int -> Maybe Int
dolet2 x y
    = do let Just x' : Maybe String = x
             | Nothing => Nothing
         y' <- y
         pure (x' + y')


text:
module BST

import NatOrder

-- decideOrder x y = ?decideOrder_rhs

-- ordering : Nat -> Nat ->

data BinaryTree = Empty | HasValue Nat BinaryTree BinaryTree

tree1 : BinaryTree
tree1 = HasValue 5 (HasValue 3 Empty Empty) (HasValue 8 Empty (HasValue 10 Empty Empty))

tree2 : BinaryTree
tree2 = ?tree2_ex

total
insert : BinaryTree -> Nat -> BinaryTree
insert Empty n = HasValue n Empty Empty
insert (HasValue k left right) n =
    case decideOrder n k of
        (LessThan n_lt_k) => HasValue k (insert left n) right
        (Equal n_eq_k) => HasValue k left right
        (GreaterThan n_gt_k) => HasValue k left (insert right n)

total
find : BinaryTree -> Nat -> Bool
find Empty n = False
find (HasValue k left right) n =
    case decideOrder n k of
        (LessThan n_lt_k) => find left n
        (Equal n_eq_k) => True
        (GreaterThan n_gt_k) => find right n

-- find (insert tree n) n --> find (insert Empty n) n --> find (HasValue n Empty Empty) n
total
findTheorem : (tree : BinaryTree) -> (n : Nat) -> find (insert tree n) n = True
findTheorem Empty n = ?findTheorem_rhs_1
findTheorem (HasValue k x y) n = ?findTheorem_rhs_2


text:
module PreorderReasoning

import Basic
import Path

infixl 2  |=>
prefix 3  ||
infix  3  ...

||| Reason about paths/identities transitively.
||| Start at Reflexivity.
namespace PreorderReasoningPath
  public export
  data StepP : a -> b -> Type where
    (...) : (0 y : a) -> (0 step : x == y) -> StepP x y

  public export
  data DeriveP : (x : a) -> (y : b) -> Type where
    (||) : (0 x : a) -> DeriveP x x
    (|=>) : DeriveP x y -> {0 z : a} -> (step : StepP y z) -> DeriveP x z

  public export
  Chain : {x, y : a} -> DeriveP x y -> x == y
  Chain (|| x) = Refl x
  Chain ((|=>) der (_ ... Refl _)) = Chain der

||| Reason about functions transitively.
||| Start at Identity.
namespace PreorderReasoningFunction
  public export
  data StepF : a -> b -> Type where
    (...) : (b : Type) -> (f : a -> b) -> StepF a b

  public export
  data DeriveF : a -> b -> Type where
    (||) : (a : Type) -> DeriveF a a
    (|=>) : DeriveF a b
         -> StepF b c
         -> DeriveF a c

  public export
  Chain : DeriveF a b -> a -> b
  Chain (|| _) = id
  Chain (p |=> (_ ... f)) = f `compose` Chain p


text:
module Tests.Array

import TypeTrans.Array
import Data.Vect

assertEq : Eq a => (given : a) -> (expected : a) -> IO ()
assertEq g e = if g == e
    then putStrLn "Test Passed"
    else putStrLn "Test Failed"

assertNotEq : Eq a => (given : a) -> (expected : a) -> IO ()
assertNotEq g e = if not (g == e)
    then putStrLn "Test Passed"
    else putStrLn "Test Failed"

assertTrue : Bool -> IO ()
assertTrue b = if b
                then putStrLn "Test Passed"
                else putStrLn "Test Failed"

assertFalse : Bool -> IO ()
assertFalse b = assertTrue (not b)

testRedDim : IO ()
testRedDim = assertEq (redDim arr) reducedArr

  where arr : Array [3, 3] Int
        arr = [[2,3,7], [4,2,6], [5,7,9]]

        reducedArr : Array [9] Int
        reducedArr = [2,3,7,4,2,6,5,7,9]

testIncDim : IO ()
testIncDim = assertEq (incDim arr) incArr

  where arr : Array [2 * 2] Int
        arr = [2, 3, 4, 5]

        incArr : Array [2,2] Int
        incArr = [[2, 3], [4, 5]]

testIncDimFactor : IO ()
testIncDimFactor = assertEq (incDim $ reshapeByFactor 3 arr) incArr

    where arr : Array [3] Int
          arr = [27, 10, 2]

          incArr : Array [3, 1] Int
          incArr = [[27], [10], [2]]

-- Test reducing dimensions, and then increasing
-- results in the same initial Array
testRedInc : IO ()
testRedInc = assertEq (incDim $ redDim arr') arr'

  where arr' : Array [3, 3] Int
        arr' = [[1,3,7], [4,2,6], [5,7,9]]

-- Test increasing dimensions and then reducing
-- results in the same initial Array
testIncRed : IO ()
testIncRed = assertEq (redDim $ incDim $ reshapeByFactor 3 arr) arr

 where
       arr : Array [3] Int
       arr = [27, 10, 2]

{-
testIncFactors : IO ()
testIncFactors = do
    assertTrue res0

  where arr : Array [8] Int
        arr = [1, 2, 3, 4, 5, 6, 7, 8]

        arr0 : Array [1, 8] Int
        arr0 = [[1, 2, 3, 4, 5, 6, 7, 8]]

        res0 : Bool
        res0  with (splitNFactor 0 arr)
                | (_ ** xs) = xs == arr0
-}

testSplitting : IO ()
testSplitting = do
                  printSplitArr
  where

    arr : Array [20] Int
    arr = [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20];

    arr2 : (xs ** Array (1::xs) Int)
    arr2 = ([1,1] ** [[[1]]])

    liftArr : Array [S x] Int -> (xs ** Array ((S x)::xs) Int)
    liftArr vs = ([] ** vs)

    printSplitArr : IO()
    printSplitArr with  (liftArr arr)
      | (vs ** xs) = printArrs (splitFactorsGeneric xs) {t=Int}

    test20 : Array (x::xs) t -> IO ()
    test20 a = print "todo"

    test10 : IO ()
    test10 with (arr2)
      | (_ ** xs) = test20 xs


text:
double : Num x => x -> x
double x = x + x

twice : (a -> a) -> a -> a
twice f x = f (f x)

Shape : Type
rotate : Shape -> Shape

quadruple : Num a => a -> a
quadruple = twice double

turn_around : Shape -> Shape
turn_around = twice rotate

max_stars_repo_name: curtisalexander/tdd-idris

max_issues_repo_name: curtisalexander/tdd-idris

max_forks_repo_name: curtisalexander/tdd-idris