text:
module Idris.ProcessIdr

import Compiler.RefC.RefC
import Compiler.Scheme.Chez
import Compiler.Scheme.ChezSep
import Compiler.Scheme.Racket
import Compiler.Scheme.Gambit
import Compiler.ES.Node
import Compiler.ES.Javascript
import Compiler.Common
import Compiler.Inline
import Compiler.Interpreter.VMCode
import Compiler.Jvm.Codegen

import Core.Binary
import Core.Context
import Core.Core
import Core.Context.Log
import Core.Directory
import Core.Env
import Core.Hash
import Core.Metadata
import Core.Options
import Core.Unify

import Parser.Unlit

import TTImp.Elab.Check
import TTImp.ProcessDecls
import TTImp.TTImp

import Idris.Desugar
import Idris.Desugar.Mutual
import Idris.Parser
import Idris.REPL.Common
import Idris.REPL.Opts
import Idris.Syntax
import Idris.Pretty
import Idris.Doc.String

import Data.List
import Libraries.Data.NameMap
import Libraries.Data.SortedMap
import Libraries.Utils.Path

import System
import System.File

%default covering

processDecls : {auto c : Ref Ctxt Defs} ->
               {auto u : Ref UST UState} ->
               {auto s : Ref Syn SyntaxInfo} ->
               {auto m : Ref MD Metadata} ->
               List PDecl -> Core (List Error)

processDecl : {auto c : Ref Ctxt Defs} ->
              {auto u : Ref UST UState} ->
              {auto s : Ref Syn SyntaxInfo} ->
              {auto m : Ref MD Metadata} ->
              PDecl -> Core (List Error)

-- Special cases to avoid treating these big blocks as units
-- This should give us better error recovery (the whole block won't fail
-- as soon as one of the definitions fails)
processDecl (PNamespace fc ns ps)
    = withExtendedNS ns $ processDecls ps
processDecl (PMutual fc ps)
    = let (tys, defs) = splitMutual ps in
      processDecls (tys ++ defs)

processDecl decl
    = catch (do impdecls <- desugarDecl [] decl
                traverse_ (Check.processDecl [] (MkNested []) []) impdecls
                pure [])
            (\err => do giveUpConstraints -- or we'll keep trying...
                        pure [err])

processDecls decls
    = do xs <- concat <$> traverse processDecl decls
         Nothing <- checkDelayedHoles
             | Just err => pure (if null xs then [err] else xs)
         errs <- logTime ("+++ Totality check overall") getTotalityErrors
         pure (xs ++ errs)

readModule : {auto c : Ref Ctxt Defs} ->
             {auto u : Ref UST UState} ->
             {auto s : Ref Syn SyntaxInfo} ->
             (full : Bool) -> -- load everything transitively (needed for REPL and compiling)
             FC ->
             (visible : Bool) -> -- Is import visible to top level module?
             (imp : ModuleIdent) -> -- Module name to import
             (as : Namespace) -> -- Namespace to import into
             Core ()
readModule full loc vis imp as
    = do defs <- get Ctxt
         let False = (imp, vis, as) `elem` map snd (allImported defs)
             | True => when vis (setVisible (miAsNamespace imp))
         Right fname <- nsToPath loc imp
               | Left err => throw err
         Just (syn, hash, more) <- readFromTTC False {extra = SyntaxInfo}
                                                  loc vis fname imp as
              | Nothing => when vis (setVisible (miAsNamespace imp)) -- already loaded, just set visibility
         extendSyn syn

         defs <- get Ctxt
         modNS <- getNS
         when vis $ setVisible (miAsNamespace imp)
         traverse_ (\ mimp =>
                       do let m = fst mimp
                          let reexp = fst (snd mimp)
                          let as = snd (snd mimp)
                          when (reexp || full) $ readModule full loc reexp m as) more
         setNS modNS

readImport : {auto c : Ref Ctxt Defs} ->
             {auto u : Ref UST UState} ->
             {auto s : Ref Syn SyntaxInfo} ->
             Bool -> Import -> Core ()
readImport full imp
    = do readModule full (loc imp) True (path imp) (nameAs imp)
         addImported (path imp, reexport imp, nameAs imp)

||| Adds new import to the namespace without changing the current top-level namespace
export
addImport : {auto c : Ref Ctxt Defs} ->
            {auto u : Ref UST UState} ->
            {auto s : Ref Syn SyntaxInfo} ->
            Import -> Core ()
addImport imp
    = do topNS <- getNS
         readImport True imp
         setNS topNS

readImportMeta : {auto c : Ref Ctxt Defs} ->
                 {auto u : Ref UST UState} ->
                 Import -> Core (Bool, (Namespace, Int))
readImportMeta imp
    = do Right ttcFileName <- nsToPath (loc imp) (path imp)
               | Left err => throw err
         (_, interfaceHash) <- readHashes ttcFileName
         pure (reexport imp, (nameAs imp, interfaceHash))

prelude : Import
prelude = MkImport (MkFC (Virtual Interactive) (0, 0) (0, 0)) False
                     (nsAsModuleIdent preludeNS) preludeNS

export
readPrelude : {auto c : Ref Ctxt Defs} ->
              {auto u : Ref UST UState} ->
              {auto s : Ref Syn SyntaxInfo} ->
              Bool -> Core ()
readPrelude full
    = do readImport full prelude
         setNS mainNS

-- Import a TTC for use as the main file (e.g. at the REPL)
export
readAsMain : {auto c : Ref Ctxt Defs} ->
             {auto u : Ref UST UState} ->
             {auto s : Ref Syn SyntaxInfo} ->
             (fname : String) -> Core ()
readAsMain fname
    = do Just (syn, _, more) <- readFromTTC {extra = SyntaxInfo}
                                             True EmptyFC True fname (nsAsModuleIdent emptyNS) emptyNS
              | Nothing => throw (InternalError "Already loaded")

         replNS <- getNS
         replNestedNS <- getNestedNS
         extendSyn syn

         -- Read the main file's top level imported modules, so we have access
         -- to their names (and any of their public imports)
         ustm <- get UST
         traverse_ (\ mimp =>
                       do let m = fst mimp
                          let as = snd (snd mimp)
                          readModule True emptyFC True m as
                          addImported (m, True, as)) more

         -- also load the prelude, if required, so that we have access to it
         -- at the REPL.
         when (not (noprelude !getSession)) $
              readModule True emptyFC True (nsAsModuleIdent preludeNS) preludeNS

         -- We're in the namespace from the first TTC, so use the next name
         -- from that for the fresh metavariable name generation
         -- TODO: Maybe we should record this per namespace, since this is
         -- a little bit of a hack? Or maybe that will have too much overhead.
         ust <- get UST
         put UST (record { nextName = nextName ustm } ust)

         setNS replNS
         setNestedNS replNestedNS

addPrelude : List Import -> List Import
addPrelude imps
  = if not (nsAsModuleIdent preludeNS `elem` map path imps)
       then prelude :: imps
       else imps

export
readHeader : {auto c : Ref Ctxt Defs} ->
             {auto o : Ref ROpts REPLOpts} ->
             (path : String) -> (origin : ModuleIdent) -> Core Module
readHeader path origin
    = do Right res <- coreLift (readFile path)
            | Left err => throw (FileErr path err)
         -- Stop at the first :, that's definitely not part of the header, to
         -- save lexing the whole file unnecessarily
         setCurrentElabSource res -- for error printing purposes
         let Right (ws, decor, mod)
            = runParserTo (PhysicalIdrSrc origin)
                          (isLitFile path) (is ':') res
                          (progHdr (PhysicalIdrSrc origin))
            | Left err => throw err
         traverse_ recordWarning ws
         pure mod

%foreign "scheme:collect"
prim__gc : Int -> PrimIO ()

gc : IO ()
gc = primIO $ prim__gc 4

export
addPublicHash : {auto c : Ref Ctxt Defs} ->
                (Bool, (Namespace, Int)) -> Core ()
addPublicHash (True, (mod, h)) = do addHash mod; addHash h
addPublicHash _ = pure ()

||| If the source file is older
unchangedTime : (sourceFileName : String) -> (ttcFileName : String) -> Core Bool
unchangedTime sourceFileName ttcFileName
  = do srcTime <- modTime sourceFileName
       ttcTime <- modTime ttcFileName
       pure $ srcTime <= ttcTime

||| If the source file hash hasn't changed
unchangedHash : (hashFn : Maybe String) -> (sourceFileName : String) -> (ttcFileName : String) -> Core Bool
unchangedHash hashFn sourceFileName ttcFileName
  = do Just sourceCodeHash        <- hashFileWith hashFn sourceFileName
             | _ => pure False
       (Just storedSourceHash, _) <- readHashes ttcFileName
             | _ => pure False
       pure $ sourceCodeHash == storedSourceHash

export
getCG : {auto o : Ref ROpts REPLOpts} ->
        {auto c : Ref Ctxt Defs} ->
        CG -> Core (Maybe Codegen)
getCG Chez = pure $ Just codegenChez
getCG ChezSep = pure $ Just codegenChezSep
getCG Racket = pure $ Just codegenRacket
getCG Gambit = pure $ Just codegenGambit
getCG Node = pure $ Just codegenNode
getCG Javascript = pure $ Just codegenJavascript
getCG RefC = pure $ Just codegenRefC
getCG VMCodeInterp = pure $ Just codegenVMCodeInterp
getCG Jvm = pure $ Just codegenJvm
getCG (Other s) = getCodegen s

export
findCG : {auto o : Ref ROpts REPLOpts} ->
         {auto c : Ref Ctxt Defs} -> Core (Maybe Codegen)
findCG
    = do defs <- get Ctxt
         getCG (codegen (session (options defs)))

||| Process everything in the module; return the syntax information which
||| needs to be written to the TTC (e.g. exported infix operators)
||| Returns 'Nothing' if it didn't reload anything
processMod : {auto c : Ref Ctxt Defs} ->
             {auto u : Ref UST UState} ->
             {auto s : Ref Syn SyntaxInfo} ->
             {auto m : Ref MD Metadata} ->
             {auto o : Ref ROpts REPLOpts} ->
             (sourceFileName : String) ->
             (ttcFileName : String) ->
             (msg : Doc IdrisAnn) ->
             (sourcecode : String) ->
             (origin : ModuleIdent) ->
             Core (Maybe (List Error))
processMod sourceFileName ttcFileName msg sourcecode origin
    = catch (do
        setCurrentElabSource sourcecode
        session <- getSession

        -- Just read the header to start with (this is to get the imports and
        -- see if we can avoid rebuilding if none have changed)
        moduleHeader <- readHeader sourceFileName origin
        let ns = moduleNS moduleHeader

        -- Add an implicit prelude import
        let imports =
          if (session.noprelude || moduleNS moduleHeader == nsAsModuleIdent preludeNS)
             then imports moduleHeader
             else addPrelude $ imports moduleHeader

        importMetas <- traverse readImportMeta imports
        let importInterfaceHashes = snd <$> importMetas

        defs <- get Ctxt
        log "module.hash" 5 $ "Interface hash of " ++ show ns ++ ": " ++ show (ifaceHash defs)
        log "module.hash" 5 $ "Interface hashes of " ++ show ns ++ " hashes:\n" ++
          show (sort importInterfaceHashes)
        storedImportInterfaceHashes <- readImportHashes ttcFileName
        log "module.hash" 5 $ "Stored interface hashes of " ++ ttcFileName ++ ":\n" ++
          show (sort storedImportInterfaceHashes)

        sourceUnchanged <- (if session.checkHashesInsteadOfModTime
          then unchangedHash (defs.options.hashFn) else unchangedTime) sourceFileName ttcFileName

        -- If neither the source nor the interface hashes of imports have changed then no rebuilding is needed
        if (sourceUnchanged && sort importInterfaceHashes == sort storedImportInterfaceHashes)
           then -- Hashes the same, source up to date, just set the ns
                -- for the REPL
                do setNS (miAsNamespace ns)
                   pure Nothing
           else -- needs rebuilding
             do iputStrLn msg
                Right (ws, decor, mod) <-
                    logTime ("++ Parsing " ++ sourceFileName) $
                      pure $ runParser (PhysicalIdrSrc origin)
                                       (isLitFile sourceFileName)
                                       sourcecode
                                       (do p <- prog (PhysicalIdrSrc origin); eoi; pure p)
                  | Left err => pure (Just [err])
                traverse_ recordWarning ws
                -- save the doc string for the current module
                log "doc.module" 10 $ unlines
                  [ "Recording doc"
                  , documentation mod
                  , "for module " ++ show (moduleNS mod)
                  ]
                addModDocString (moduleNS mod) (documentation mod)

                addSemanticDecorations decor
                initHash
                traverse_ addPublicHash (sort importMetas)
                resetNextVar
                when (ns /= nsAsModuleIdent mainNS) $
                      when (ns /= origin) $
                          throw (GenericMsg mod.headerLoc
                                   ("Module name " ++ show ns ++
                                    " does not match file name " ++ show sourceFileName))

                -- read import ttcs in full here
                -- Note: We should only import .ttc - assumption is that there's
                -- a phase before this which builds the dependency graph
                -- (also that we only build child dependencies if rebuilding
                -- changes the interface - will need to store a hash in .ttc!)
                logTime "++ Reading imports" $
                   traverse_ (readImport False) imports

                -- Before we process the source, make sure the "hide_everywhere"
                -- names are set to private (TODO, maybe if we want this?)
--                 defs <- get Ctxt
--                 traverse (\x => setVisibility emptyFC x Private) (hiddenNames defs)
                setNS (miAsNamespace ns)
                errs <- logTime "++ Processing decls" $
                            processDecls (decls mod)
--                 coreLift $ gc

                when (isNil errs) $
                   logTime "++ Compile defs" $ compileAndInlineAll

                -- Save the import hashes for the imports we just read.
                -- If they haven't changed next time, and the source
                -- file hasn't changed, no need to rebuild.
                defs <- get Ctxt
                put Ctxt (record { importHashes = importInterfaceHashes } defs)
                pure (Just errs))
          (\err => pure (Just [err]))

-- Process a file. Returns any errors, rather than throwing them, because there
-- might be lots of errors collected across a whole file.
export
process : {auto c : Ref Ctxt Defs} ->
          {auto m : Ref MD Metadata} ->
          {auto u : Ref UST UState} ->
          {auto s : Ref Syn SyntaxInfo} ->
          {auto o : Ref ROpts REPLOpts} ->
          Doc IdrisAnn -> FileName ->
          (moduleIdent : ModuleIdent) ->
          Core (List Error)
process buildmsg sourceFileName ident
    = do Right res <- coreLift (readFile sourceFileName)
               | Left err => pure [FileErr sourceFileName err]
         catch (do ttcFileName <- getTTCFileName sourceFileName "ttc"
                   Just errs <- logTime ("+ Elaborating " ++ sourceFileName) $
                                   processMod sourceFileName ttcFileName buildmsg res ident
                        | Nothing => pure [] -- skipped it
                   if isNil errs
                      then
                        do defs <- get Ctxt
                           ns <- ctxtPathToNS sourceFileName
                           makeBuildDirectory ns
                           traverse_
                              (\cg =>
                                  do Just cgdata <- getCG cg
                                          | Nothing =>
                                              coreLift $ putStrLn $ "No incremental code generator for " ++ show cg
                                     Just res <- incCompile cgdata sourceFileName
                                          | Nothing => pure ()
                                     setIncData cg res)
                              (incrementalCGs !getSession)

                           writeToTTC !(get Syn) sourceFileName ttcFileName
                           ttmFileName <- getTTCFileName sourceFileName "ttm"
                           writeToTTM ttmFileName
                           pure []
                      else do pure errs)
               (\err => pure [err])


text:
module Data.DPair

%default total

namespace Exists

  ||| A dependent pair in which the first field (witness) should be
  ||| erased at runtime.
  |||
  ||| We can use `Exists` to construct dependent types in which the
  ||| type-level value is erased at runtime but used at compile time.
  ||| This type-level value could represent, for instance, a value
  ||| required for an intrinsic invariant required as part of the
  ||| dependent type's representation.
  |||
  ||| @type The type of the type-level value in the proof.
  ||| @this The dependent type that requires an instance of `type`.
  public export
  data Exists : (this : type -> Type) -> Type where
    Evidence : (0 value : type)
            -> (prf : this value)
            -> Exists this

  ||| Return the type-level value (evidence) required by the dependent type.
  |||
  ||| We need to be in the Erased setting for this to work.
  |||
  ||| @type The type-level value's type.
  ||| @pred The dependent type that requires an instance of `type`.
  ||| @prf  That there is a value that satisfies `prf`.
  public export
  0
  fst : {0 type : Type}
     -> {0 pred : type -> Type}
     -> (1 prf  : Exists pred)
     -> type
  fst (Evidence value _) = value

  ||| Return the dependently typed value.
  |||
  ||| @type The type-level value's type.
  ||| @pred The dependent type that requires an instance of `type`.
  ||| @prf  That there is a value that satisfies `prf`.
  public export
  snd : {0 type : Type}
     -> {0 pred : type -> Type}
     -> (1 prf  : Exists pred)
     -> pred (Exists.fst prf)
  snd (Evidence value prf) = prf

namespace Subset

  ||| A dependent pair in which the second field (evidence) should not
  ||| be required at runtime.
  |||
  ||| We can use `Subset` to provide extrinsic invariants about a
  ||| value and know that these invariants are erased at
  ||| runtime but used at compile time.
  |||
  ||| @type The type-level value's type.
  ||| @pred The dependent type that requires an instance of `type`.
  public export
  data Subset : (type : Type)
             -> (pred : type -> Type)
             -> Type
    where
      Element : (value : type)
             -> (0 prf : pred value)
             -> Subset type pred

  ||| Return the type-level value (evidence) required by the dependent type.
  |||
  ||| @type The type-level value's type.
  ||| @pred The dependent type that requires an instance of `type`.
  ||| @prf  That there is a value that satisfies `prf`.
  public export
  fst : {0 type : Type}
     -> {0 pred : type -> Type}
     -> (1 prf  : Subset type pred)
     -> type
  fst (Element value prf) = value

  ||| Return the dependently typed value.
  |||
  ||| We need to be in the erased setting for this to work.
  |||
  ||| @type The type-level value's type.
  ||| @pred The dependent type that requires an instance of `type`.
  ||| @prf  That there is a value that satisfies `prf`.
  public export
  0
  snd : {0 type : Type}
     -> {0 pred : type -> Type}
     -> (1 value : Subset type pred)
     -> pred (Subset.fst value)
  snd (Element value prf) = prf

ext: idr


text:
module lib.Library1

import lib.Library2
import lib.Library5

export
salute1 : String
salute1 = "Hello, I'm library 1, and there is someone who wants to say something\n" ++
          salute2 ++ "\n" ++
          "  AND! I can also ask Library5!!!:\n" ++
          salute5


text:
-- ------------------------------------------------------------- [ Process.idr ]
--
-- Implementation of the echo protocol for process communication.
--
-- --------------------------------------------------------------------- [ EOH ]
module TCPHandshake

import Effects
import Effect.StdIO
import Effect.Default
import Effect.Msg

import System.Protocol

import RFC.Handshake

covering
bob : Nat -> (client : PID)
      -> Process (handshake) 'Bob ['Alice := client] [STDIO] ()
bob seqno client = do
    (msg, x) <- recvFrom 'Alice
    let x' = S x
    putStrLn $ "Bob -> Alice: SynAck, " ++ show seqno ++ ", " ++ show x'
    sendTo 'Alice (SynAck, seqno, (S x ** Refl))
    (msg1, no') <- recvFrom 'Alice
    putStrLn $ "Received from Alice: " ++ show (getWitness no')
    pure ()

covering
alice : Nat -> (server : PID)
      -> Process (handshake) 'Alice ['Bob := server] [STDIO] ()
alice seqno server = do
    putStrLn $ "Alice -> Bob: Syn, " ++ show seqno
    sendTo 'Bob (Syn, seqno)
    (msg, y, x) <- recvFrom 'Bob
    putStrLn $ "Alice -> Bob: Ack " ++ show (S y)
    sendTo 'Bob (Ack, (S y ** Refl))
    pure ()

covering
doHandshake : IO ()
doHandshake = runConc [()] doShake
  where
    doShake : Process (handshake) 'Alice [] [STDIO] ()
    doShake = do
       server <- spawn (bob 2) [()]
       setChan 'Bob server
       alice 100 server
       dropChan 'Bob
       pure ()

-- -------------------------------------------------------------------- [ Main ]
namespace Main
  main : IO ()
  main = doHandshake

-- --------------------------------------------------------------------- [ 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 BadRefl

import IdrisPrelude

plus : Nat -> Nat -> Nat
plus =
  natElim
    ( \ _ => (Nat -> Nat) )           -- motive
    ( \ n => n )                    -- case for Zero
    ( \ p, rec, n => Succ (rec n) )   -- case for Succ

-- the other direction requires induction on N:
postulate pNPlus0isN : (n : Nat) -> Eq Nat (plus n Zero) n

-- the other direction requires induction on N:
succPlus : (n : Nat) -> Eq Nat  (Succ n) (plus (Succ n) Zero)
succPlus =
  (\n => pNPlus0isN (Succ n))

max_stars_repo_name: JoeyEremondi/lambda-pi-constraint

max_issues_repo_name: JoeyEremondi/lambda-pi-constraint

max_forks_repo_name: JoeyEremondi/lambda-pi-constraint


text:
module Test

import Data.List
import System

import RandomTest
import CertTest
import LTLS
import Control.Monad.Error.Either

%default partial

run_test : String -> EitherT String IO () -> IO Bool
run_test name test = do
  Right () <- runEitherT test
  | Left err => putStrLn "\{name}: failed \{err}" $> False
  putStrLn "\{name}: success" $> True

run : List (IO Bool) -> IO ()
run tests = do
  results <- sequence tests
  let [] = filter not results
  | xs => putStrLn "\{show (length xs)} tests failed" *> exitFailure
  putStrLn "all tests passed"

export
main : IO ()
main = run
  [ (run_test "csprng" test_random)
  , (run_test "certstore" test_cert)
  , (run_test "tls connection" tls_test_unit)
  ]


text:
-- --------------------------------------------------------------- [ State.idr ]
-- Module    : State.idr
-- Copyright : (c) Jan de Muijnck-Hughes
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
||| State for Building Patterns from the AST.
module Sif.DSL.State

import Effects
import Effect.Default

import Sif.Types
import Sif.AbsSyntax
import Sif.Pattern
import Sif.Error

-- -------------------------------------------------------------- [ Directives ]
%access export
%default total

-- -------------------------------------------------------------------- [ Body ]
public export
record BuildState where
  constructor MkSState
  getProbID        : Maybe String
  getRQs           : List (String, SifAST TyREQ)
  pattTitle        : String
  pattDesc         : Maybe String
  getPFName        : String
  getSFName        : String

defBuildSt : String -> String -> BuildState
defBuildSt p s = MkSState Nothing Nil "" Nothing p s

Default BuildState where
  default = defBuildSt "" ""

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

max_stars_repo_name: jfdm/sif-lang

max_issues_repo_name: jfdm/sif-lang

max_forks_repo_name: jfdm/sif-lang


text:
module Main

import Control.IOExcept
import Data.Vect

import Effects
import Effect.File
import Effect.Random
import Effect.StdIO
import Effect.System

%access public export

data HState      = NotRunning
                 | Running Nat Nat

data GuessResult = Correct | Incorrect

data Hangman     : HState -> Type where
     GameStart   : Hangman NotRunning
     GameWon     : (word    : String)                -> Hangman NotRunning
     GameLost    : (word    : String)                -> Hangman NotRunning
     InProgress  : (word    : String)                ->
                   (guesses : Nat)                   ->
                   (got     : List Char)             ->
                   (missing : Vect letters Char)     ->
                   Hangman (Running guesses letters)

implementation Default (Hangman NotRunning) where
  default = GameStart

implementation Show (Hangman state) where
  show GameStart                             = "Starting"
  show (GameWon word)                        = "Game won: word was " ++ word
  show (GameLost word)                       = "Game lost: word was " ++ word
  show (InProgress word guesses got missing) =
      unlines [ pack (map hideMissing (unpack word))
              , "Got " ++ show got ++ " so far"
              , show guesses ++ " guesses left"
              ]
    where
      hideMissing : Char -> Char
      hideMissing c = ifThenElse (c `elem` missing) '_' c

export
letters : String -> List Char
letters = map toUpper . nub . unpack

%access private

initState : (word : String) -> Hangman (Running 6 (length (letters word)))
initState word = InProgress (toUpper word) _ [] (fromList (letters word))

removeElem : (x : a) -> (xs : Vect (S n) a) ->
             {auto prf : Elem x xs} ->
             Vect n a
removeElem x (x :: ys) {prf = Here}                  = ys
removeElem {n = Z} x [y] {prf = There later}         = absurd later
removeElem {n = S _} x (y :: ys) {prf = There later} = y :: removeElem x ys

%access public export

data HangmanRules : Effect where
     NewGame      : (word : String) ->
                    sig HangmanRules ()
                        (Hangman NotRunning)
                        (Hangman (Running 6 (length (letters word))))
     ||| No guesses left, so the player has lost.
     Lost         : sig HangmanRules ()
                        (Hangman (Running 0 (S letters)))
                        (Hangman NotRunning)
     ||| No letters left to guess, so the player has won.
     Won          : sig HangmanRules ()
                        (Hangman (Running (S guesses) 0))
                        (Hangman NotRunning)
     Guess        : (letter : Char) ->
                    sig HangmanRules GuessResult
                        (Hangman (Running (S guesses) (S letters)))
                        (\res =>
                             Hangman $
                             case res of
                                  Correct   => Running (S guesses) letters
                                  Incorrect => Running guesses (S letters))
     ShowState    : sig HangmanRules String (Hangman state)
     -- Message      : (message : String) -> sig HangmanRules () (Hangman state)
     -- ReadGuess    : sig HangmanRules Char (Hangman state)

HANGMAN : HState -> EFFECT
HANGMAN state = MkEff (Hangman state) HangmanRules

%access export

guess : (letter : Char) ->
        Eff GuessResult
            [HANGMAN (Running (S guesses) (S letters))]
            (\res =>
                [HANGMAN (case res of
                               Correct   => Running (S guesses) letters
                               Incorrect => Running guesses (S letters))])
guess letter = call (Guess letter)

won : Eff () [HANGMAN (Running (S guesses) 0)] [HANGMAN NotRunning]
won = call Won

lost : Eff () [HANGMAN (Running 0 (S letters))] [HANGMAN NotRunning]
lost = call Lost

newGame : (word : String) ->
          Eff () [HANGMAN NotRunning]
                 [HANGMAN (Running 6 (length (letters word)))]
newGame word = call (NewGame word)

showState : Eff String [HANGMAN state]
showState = call ShowState

public export
implementation Handler HangmanRules m where
  handle (InProgress word _ _ _) Won k  = k () (GameWon word)
  handle (InProgress word _ _ _) Lost k = k () (GameLost word)
  handle state ShowState  k             = k (show state) state
  handle _ (NewGame word) k             = k () (initState word)
  handle (InProgress word (S guesses) got missing) (Guess letter) k =
      case isElem letter missing of
           Yes _ => k Correct $ InProgress word _ (letter :: got)
                                           (removeElem letter missing)
           No _  => k Incorrect (InProgress word _ got missing)

partial
game : Eff () [HANGMAN (Running (S guesses) letters), STDIO]
              [HANGMAN NotRunning, STDIO]
game {letters = Z}             = won
game {guesses} {letters = S k} =
    do putStrLn !showState
       putStr "Enter guess: "
       case !(unpack . trim <$> getStr) of
            [letter] => case !(guess (toUpper letter)) of
                             Correct   => do putStrLn "Correct"
                                             case k of
                                               Z   => won
                                               S j => game
                             Incorrect => do putStrLn "Incorrect"
                                             case guesses of
                                                  Z   => lost
                                                  S k => game
            _        => do putStrLn "Invalid input!"
                           game

words : ?wlen
words = with Vect [ "idris", "agda", "haskell", "miranda",
                    "java", "javascript", "fortran", "basic", "racket",
                    "coffeescript", "rust", "purescript", "clean", "links",
                    "koka", "cobol" ]

wlen = %runElab search

%default partial

runGame : Eff () [HANGMAN NotRunning, FILE (), RND, STDIO, SYSTEM]
runGame = do srand !time
             newGame !(rndSelect' words)
             game
             putStrLn !showState

main : IO ()
main = run runGame

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

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:
%language TypeProviders

strToType : String -> Type
strToType "Int" = Int
strToType _ = Nat

fromFile : String -> IO (Provider Type)
fromFile fname = do Right str <- readFile fname
                      | Left err =>
                            do
                                putStrLn "Failed to load file"
                                pure (Provide Void)
                    pure (Provide (strToType (trim str)))

%provide (T1 : Type) with fromFile "theType"

foo : T1
foo = 2


text:
module Main

import Effects
import Effect.File
import Effect.State
import Effect.StdIO
import Control.IOExcept

data Count : Type where

TestFileIO : Type -> Type -> Type
TestFileIO st t = Eff t [FILE st, STDIO, Count ::: STATE Int]

readFileCount : Eff (FileOpResult (List String)) [FILE R, STDIO, Count ::: STATE Int]
readFileCount = readAcc []
  where
    readAcc : List String
           -> Eff (FileOpResult (List String)) [FILE R, STDIO, Count ::: STATE Int]
    readAcc acc = do
      e <- eof
      if (not e)
         then do
           (Result str) <- readLine
                         | (FError err) => pure (FError err)
           Count :- put (!(Count :- get) + 1)
           readAcc (str :: acc)
         else do
           let res = reverse acc
           pure $ Result res

testFile : TestFileIO () ()
testFile = do
    Success <- open "testFile" Read
             | (FError err) => do
                 putStrLn "Error!"
                 pure ()
    (Result fcontents) <- readFileCount
                        | (FError err) => do
                            close
                            putStrLn "Error!"
                            pure ()
    putStrLn (show fcontents)
    close
    putStrLn (show !(Count :- get))

main : IO ()
main = run testFile

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 PeerTest

import public Peer
import System
import Channel
import Util
import Effects
import Effect.Random
import Effect.StdIO

firstPeerTest : (chans : PeerChannels) -> (sock : Socket) ->
    (ip : SocketAddress) -> (port : Int) ->
    PeerCmd () Setup Setup
firstPeerTest chans sock ip port =
    do PutStrLn $ "Socket is listening for connections on: " ++ (show ip) ++ ":" ++ (show port)
       ListenForNewClients sock chans
       BroadcastToClients chans

connectingPeerTest : (chans : PeerChannels) -> (mySock : Socket) ->
                 (myIp : SocketAddress) -> (myPort : Int) ->
                 (newIp : SocketAddress) -> (newPort : Int) ->
                 PeerCmd () NotReady Running
connectingPeerTest chans mySock myIp myPort newIp newPort =
  do Right newSock <- CreateSocket | Left err => Error (show err)
     ok <- Connect newSock newIp newPort
     if ok == 0 then
      do Push (connChan chans) newSock
         WaitForRelayedMessages newSock (relayed chans)
         PutStrLn $ "Socket is listening for connections on: " ++ (show myIp) ++ ":" ++ (show myPort)
         RecMessages newSock newIp chans
         ListenForNewClients mySock chans
         BroadcastToClients chans
         -- THIS IS NOT AN ERROR BUT A FORCE THROUGH STATES FOR TESTING BEHAVIOUR
         Error $ ""
     else Error $ "Something went wrong : error code " ++ (show ok)

startConnectingPeersChain : (nrOfPeers : Nat) -> (ip : SocketAddress)
                        -> (newPort : Int) -> IO ()
startConnectingPeersChain Z ip newPort = pure ()
startConnectingPeersChain (S n) ip newPort = do connChan <- makeChan (the (List Socket) [])
                                                msgQueue <- makeChan (the (List Message) [])
                                                relayed <- makeChan (the (List Message) [])
                                                chans <- pure (MkPeerChans msgQueue relayed connChan)
                                                Right sock <- socket AF_INET Stream 0
                                                    | Left err => putStr (show err)
                                                port <- pure (3500 + (cast n))
                                                ok <- bind sock (Just ip) port
                                                listeningCode <- listen sock
                                                putStrLn $ "Creating peer nr: " ++ (show (n + 1))
                                                run (connectingPeerTest chans sock ip port ip newPort)
                                                startConnectingPeersChain n ip port

startConnectingPeersToFirstPeer : (nrOfPeers : Nat) -> (ip : SocketAddress)
                                -> (newPort : Int) -> IO ()
startConnectingPeersToFirstPeer Z ip newPort = pure ()
startConnectingPeersToFirstPeer (S n) ip newPort = do connChan <- makeChan (the (List Socket) [])
                                                      msgQueue <- makeChan (the (List Message) [])
                                                      relayed <- makeChan (the (List Message) [])
                                                      chans <- pure (MkPeerChans msgQueue relayed connChan)
                                                      Right sock <- socket AF_INET Stream 0
                                                        | Left err => putStr (show err)
                                                      port <- pure (3500 + (cast n))
                                                      ok <- bind sock (Just ip) port
                                                      listeningCode <- listen sock
                                                      putStrLn $ "Creating peer nr: " ++ (show (n + 1))
                                                      run (connectingPeerTest chans sock ip port ip newPort)
                                                      startConnectingPeersToFirstPeer n ip port

startconnectingPeersRandom : (nrOfPeers : Nat) -> (ip : SocketAddress)
                            -> (newPort : Int) -> IO ()
startconnectingPeersRandom Z ip newPort = pure ()
startconnectingPeersRandom (S n) ip newPort = do connChan <- makeChan (the (List Socket) [])
                                                 msgQueue <- makeChan (the (List Message) [])
                                                 relayed <- makeChan (the (List Message) [])
                                                 chans <- pure (MkPeerChans msgQueue relayed connChan)
                                                 Right sock <- socket AF_INET Stream 0
                                                    | Left err => putStr (show err)
                                                 rndProg <- pure (rndInt (cast n) 100)
                                                 rndNr <- Effects.run rndProg
                                                 port <- pure (3500 + (fromInteger rndNr))
                                                 ok <- bind sock (Just ip) port
                                                 listeningCode <- listen sock
                                                 putStrLn $ "Creating peer nr: " ++ (show (n + 1))
                                                 run (connectingPeerTest chans sock ip port ip newPort)
                                                 startconnectingPeersRandom n ip port

peerTest1 : IO ()
peerTest1 = do Right sock <- socket AF_INET Stream 0
                | Left err => putStr (show err)
               connChan <- makeChan (the (List Socket) [])
               msgQueue <- makeChan (the (List Message) [])
               relayed <- makeChan (the (List Message) [])
               chans <- pure (MkPeerChans msgQueue relayed connChan)
               putStrLn "Select what ip you want to use, by inputting the number in the parentheses:"
               ip <- selectIp
               port <- pure 3500
               ok <- bind sock (Just ip) port
               listeningCode <- listen sock
               run (firstPeerTest chans sock ip port)
               putStrLn "Created first peer"
               startConnectingPeersToFirstPeer 100 ip port
               addSingleMsg "hello" msgQueue "123"
               usleep 1000000
               pure ()

peerTest2 : IO ()
peerTest2 = do Right sock <- socket AF_INET Stream 0
                | Left err => putStr (show err)
               connChan <- makeChan (the (List Socket) [])
               msgQueue <- makeChan (the (List Message) [])
               relayed <- makeChan (the (List Message) [])
               chans <- pure (MkPeerChans msgQueue relayed connChan)
               putStrLn "Select what ip you want to use, by inputting the number in the parentheses:"
               ip <- selectIp
               seed <- time
               port <- pure 3500
               ok <- bind sock (Just ip) port
               listeningCode <- listen sock
               run (firstPeerTest chans sock ip port)
               putStrLn "Created first peer"
               startConnectingPeersChain 100 ip port
               addSingleMsg "hello" msgQueue "123"
               usleep 1000000
               pure ()

peerTest3 : IO ()
peerTest3 = do Right sock <- socket AF_INET Stream 0
                | Left err => putStr (show err)
               connChan <- makeChan (the (List Socket) [])
               msgQueue <- makeChan (the (List Message) [])
               relayed <- makeChan (the (List Message) [])
               chans <- pure (MkPeerChans msgQueue relayed connChan)
               putStrLn "Select what ip you want to use, by inputting the number in the parentheses:"
               ip <- selectIp
               seed <- time
               port <- pure 3500
               ok <- bind sock (Just ip) port
               listeningCode <- listen sock
               run (firstPeerTest chans sock ip port)
               putStrLn "Created first peer"
               startconnectingPeersRandom 100 ip port
               addSingleMsg "hello" msgQueue "123"
               usleep 1000000
               pure ()

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

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

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


text:
-- -------------------------------------------------------------- [ Parser.idr ]
-- Description : A command line argument parser
-- Copyright   : (c) Huw Campbell
-- --------------------------------------------------------------------- [ EOH ]
module Options.Applicative.Usage

import public Text.PrettyPrint.WL

import Options.Applicative.Builder
import Options.Applicative.Chunk
import Options.Applicative.Types
import Options.Applicative.Maybe
import Options.Applicative.Run
import Control.Lens
import Control.Monad.State
import Control.Monad.Trans

%default total
%access public export

data OptTree : a -> Type where
  Leaf     : a                -> OptTree a
  MultNode : List (OptTree a) -> OptTree a
  AltNode  : List (OptTree a) -> OptTree a

record OptHelpInfo where
  constructor MkOptHelpInfo
  hinfoMulti, hinfoDefault : Bool

renderName : OptName -> Doc
renderName (ShortName c) = char '-' |+| char c
renderName (LongName s)  = text "--" |+| text s

renderNames : List OptName -> Doc
renderNames Nil       = empty
renderNames [n]       = renderName n
renderNames (n :: ns) = (foldl (\x, y => x |++| char '|' |++| renderName y) (renderName n) ns)

optDesc : Bool -> Bool -> OptHelpInfo -> Option g a -> Chunk Doc
optDesc withHidden withParens info (Opt pp rdr) =
  render mm (pp ^. visibility == Visible || withHidden) (hinfoDefault info) (reqParens && withParens)
    where
      mm : Chunk Doc
      mm = Just $ case rdr of
        (OptionReader ns _ m) => renderNames ns |++| (text m)
        (FlagReader ns _)     => renderNames ns
        (ArgReader _ m)       => text m
        (CmdReader _ m)       => text m

      reqParens : Bool
      reqParens = case rdr of
        (OptionReader (_ :: _) _ _)  => True
        (OptionReader _ _ _)         => False
        (FlagReader (_ :: _ :: _) _) => True
        (FlagReader _ _)             => False
        (ArgReader _ _)              => False
        (CmdReader _ _)              => False

      render : Chunk Doc -> Bool -> Bool -> Bool -> Chunk Doc
      render _      False  _    _    = Nothing
      render chunk  _      True _    = map brackets chunk
      render chunk  _      _    True = map parens   chunk
      render chunk  _      _    _    = chunk

partial
fold_tree : OptTree (Chunk Doc) -> Chunk Doc
fold_tree (Leaf x) = x
fold_tree (MultNode xs) = foldr (combine . fold_tree) Nothing xs
fold_tree (AltNode xs) = alt_node
                       . filter nonEmptyChunk
                       . map fold_tree $ xs
  where
    partial
    alt_node : List (Chunk Doc) -> Chunk Doc
    alt_node [n]       = n
    alt_node (n :: ns) = map parens
                       . foldl (chunked (\x, y => x <+> char '|' <+> y)) n
                       $ ns

-- | Map a polymorphic function over all the options of a parser, and collect
-- the results in a tree.
partial
treeMapParser : ({ g : ParamType } -> {x : Type} -> OptHelpInfo -> Option g x -> b) -> Parser a -> OptTree b
treeMapParser g = simplify . go False False g
  where
    partial
    simplify : OptTree a -> OptTree a
    simplify (Leaf x)      = Leaf x
    simplify (MultNode xs) =
      case the (List (OptTree a)) (concatMap (remove_mult . simplify) xs) of
        [x] => x
        xs' => MultNode xs'
      where
        remove_mult (MultNode ts) = ts
        remove_mult t             = [t]
    simplify (AltNode xs)  =
      case the (List (OptTree a)) (concatMap (remove_alt . simplify) xs) of
        []  => MultNode []
        [x] => x
        xs' => AltNode xs'
      where
        remove_alt (AltNode ts)  = ts
        remove_alt (MultNode []) = []
        remove_alt t             = [t]

    has_default : Parser a -> Bool
    has_default p = isJust (evalParser p)

    go : Bool -> Bool -> ({ g : ParamType } -> {x : Type} -> OptHelpInfo -> Option g x -> b) -> Parser a -> OptTree b
    go _ _ _ (NilP _)     = MultNode []
    go m d f (OptP opt)   = case opt ^. visibility of
      Internal => MultNode []
      _        => Leaf (f (MkOptHelpInfo m d) opt)
    go m d f (AppP p1 p2) = MultNode [go m d f p1, go m d f p2]
    go m d f (AltP p1 p2) = AltNode  [go m d' f p1, go m d' f p2]
      where d' = d || has_default p1 || has_default p2

partial
flattenTree : OptTree a -> List a
flattenTree (Leaf x)      = [x]
flattenTree (MultNode xs) = xs >>= flattenTree
flattenTree (AltNode xs)  = xs >>= flattenTree

partial
briefDesc : Parser a -> Chunk Doc
briefDesc = fold_tree . treeMapParser (optDesc False True)

partial
fullDesc : Parser a -> Chunk Doc
fullDesc = tabulate . catMaybes . flattenTree . treeMapParser doc
  where
    doc : OptHelpInfo -> Option g a -> Maybe (Doc, Doc)
    doc info opt = do
      let n = optDesc True False info opt
      let h = opt ^. help
      guard . nonEmptyChunk $ n
      pure (extractChunk n, h)

-- | Generate the help text for a program.
partial
parserHelp : Parser a -> Doc
parserHelp p =
  text "Usage:" |++| extractChunk (briefDesc p) |/| with_title "Available options:" (fullDesc p)
  where
    with_title : String -> Chunk Doc -> Doc
    with_title title ch = text title |/| extractChunk ch

max_stars_repo_name: statebox/optparse-idris

max_issues_repo_name: statebox/optparse-idris

max_forks_repo_name: statebox/optparse-idris


text:
module Data.List1

%default total

public export
record List1 a where
  constructor (::)
  head : a
  tail : List a

public export
toList : (1 xs : List1 a) -> List a
toList (x :: xs) = x :: xs

public export
reverseOnto : (1 acc : List1 a) -> (1 xs : List a) -> List1 a
reverseOnto acc []        = acc
reverseOnto acc (x :: xs) = reverseOnto (x :: toList acc) xs

public export
reverse : (1 xs : List1 a) -> List1 a
reverse (x :: xs) = reverseOnto [x] xs

export
fromList : (1 xs : List a) -> Maybe (List1 a)
fromList [] = Nothing
fromList (x :: xs) = Just (x :: xs)

export
appendl : (1 xs : List1 a) -> (1 ys : List a) -> List1 a
appendl (x :: xs) ys = x :: xs ++ ys

export
append : (1 xs, ys : List1 a) -> List1 a
append xs ys = appendl xs (toList ys)

export
lappend : (1 xs : List a) -> (1 ys : List1 a) -> List1 a
lappend [] ys = ys
lappend (x :: xs) ys = append (x :: xs) ys

export
Functor List1 where
  map f (x :: xs) = f x :: map f xs

export
Foldable List1 where
  foldr c n (x :: xs) = c x (foldr c n xs)

export
Show a => Show (List1 a) where
  show = show . toList

export
Applicative List1 where
  pure x = [x]
  f :: fs <*> xs = appendl (map f xs) (fs <*> toList xs)

export
Monad List1 where
  (x :: xs) >>= f = appendl (f x) (xs >>= toList . f)


text:
module Test

import Test.LazyTest

testStrict  : IO ()
testLazy    : IO ()
testBuilder : IO ()

partial
main : IO ()
main = do
  -- testStrict
  -- testLazy
  -- testBuilder
  printLn "Testing lazy file IO:" *> lazyIOTest
  -- This crashes currently for errors, obvious we'll want a better testing
  -- method as we go.


text:
module Control.Monad.Indexed

%access public
%default total

class IndexedFunctor (f : Type -> Type -> Type -> Type) where
  imap : (a -> b) -> f i i a -> f i i b

-- fがIndexedFunctorな時点で、fの種は確定すると思うのだが、明示しないと受け付けてくれない...
infixl 2 <:$>
class IndexedFunctor f => IndexedApplicative (f : Type -> Type -> Type -> Type) where
  ipure : a -> f i i a
  (<:$>) : f i i (a -> b) -> f i i a -> f i i b

infixl 2 :>>=
class IndexedApplicative f => IndexedMonad (f : Type -> Type -> Type -> Type) where
  (:>>=) : f j k x -> (x -> f j k a) -> f i k a

iflatten : IndexedMonad f => f i j (f i j a) -> f i j a
iflatten a = a :>>= id

ireturn : IndexedMonad f => a -> f i i a
ireturn = ipure

max_stars_repo_name: seagull-kamome/idris-toy

max_issues_repo_name: seagull-kamome/idris-toy

max_forks_repo_name: seagull-kamome/idris-toy


text:
module Syntax.WithProof

prefix 10 @@

||| Until Idris2 supports the 'with (...) proof p' construct, here's a
||| poor-man's replacement.
public export
(@@) : (t : a ) -> (u : a ** t = u)
(@@) x = ( x ** Refl)


text:
module Data.Prim.Integer

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

%default total

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

replace' : (0 p : a -> Type) -> (0 _ : x = y) -> p x -> p y
replace' p prf px = replace {p} prf px

derive :  {0 a,b : Type}
       -> (x : a)
       -> FastDerivation a b
       -> b
derive x z = case Calc z of Refl => x

---------
-- Axioms

||| This axiom, which only holds for unbounded integers, relates
||| addition and the ordering of integers:
|||
||| From `k < m` follows `n + k < n + m` for all integers `k`, `m`, and `n`.
export
0 plusGT : (k,m,n : Integer) -> k < m -> n + k < n + m
plusGT k m n x = strictLT x $ mkLT unsafeRefl

||| This axiom, which only holds for unbounded integers, relates
||| multiplication and the ordering of integers:
|||
||| From `0 < m` and `0 < n` follows `0 < m * n` for all integers `m` and `n`.
export
0 multPosPosGT0 : (m,n : Integer) -> 0 < m -> 0 < n -> 0 < m * n
multPosPosGT0 _ _ p1 p2 = strictLT p1 $ strictLT p2 $ mkLT unsafeRefl

||| There is no integer between 0 and 1.
export
0 oneAfterZero : (n : Integer) -> 0 < n -> 1 <= n
oneAfterZero n gt0 = case comp 1 n of
  LT x _ _ => Left x
  EQ _ x _ => Right x
  GT _ _ x => strictLT gt0
            $ strictLT x
            $ assert_total
            $ idris_crash "IMPOSSIBLE: Integer between 0 and 1"

||| For positive `d`, `mod n d` is a non-negative number
||| strictly smaller than `d`.
export
0 modLT : (n,d : Integer) -> 0 < d -> (0 <= mod n d, mod n d < d)
modLT n d x with (mod n d)
  _ | 0 = (Right Refl, x)
  _ | _ = strictLT x (Left $ mkLT unsafeRefl, mkLT unsafeRefl)

export
0 modNegEQ : (n,d : Integer) -> d < 0 -> mod n d === mod n (neg d)
modNegEQ n d x = strictLT x unsafeRefl

export
0 lawDivMod : (n,d : Integer) -> d /= 0 -> d * div n d + mod n d === n
lawDivMod n d (Left x)  = strictLT x unsafeRefl
lawDivMod n d (Right x) = strictLT x unsafeRefl

----------------------------
-- Division

||| Safe division.
export %inline
sdiv : (n,d : Integer) -> (0 prf : d /= 0) => Integer
sdiv n d = n `div` d

||| Safe modulo.
export %inline
smod : (n,d : Integer) -> (0 prf : d /= 0) => Integer
smod n d = n `mod` d

--------------------------------------------------------------------------------
--          Well-Foundedness
--------------------------------------------------------------------------------

public export
0 BoundedLT : (lowerBound : Integer) -> Integer -> Integer -> Type
BoundedLT lowerBound x y = (lowerBound <= x, x < y)

public export
0 BoundedGT : (upperBound : Integer) -> Integer -> Integer -> Type
BoundedGT upperBound x y = (upperBound >= x, x > y)

||| Every value of type `Integer` with a fixed lower bound
||| is accessible with relation to `(<)`.
export
accessLT : (m : Integer) -> Accessible (BoundedLT lb) m
accessLT m = Access $ \n,lt => accessLT (assert_smaller m n)

||| Every value of type `Integer` with a fixed upper bound
||| is accessible with relation to `(>)`.
export
accessGT : (m : Integer) -> Accessible (BoundedGT ub) m
accessGT m = Access $ \n,gt => accessGT (assert_smaller m n)


text:
module FFI

import Data.Promise

%default total

promiseIO : (primFn : (String -> PrimIO ()) -> (String -> PrimIO ()) -> PrimIO ()) -> Promise String
promiseIO primFn =
  promisify $ \ok,notOk => primFn (\res => toPrim $ ok res) (\err => toPrim $ notOk err)

node_ffi : (libName : String) -> (fnName : String) -> String
node_ffi libName fnName = "node:support:\{fnName},\{libName}"

max_stars_repo_name: mattpolzin/harmony

max_issues_repo_name: mattpolzin/harmony

max_forks_repo_name: mattpolzin/harmony


text:
||| A graph whose vertices have a restricted in/out degree.
module Toolkit.Data.Graph.EdgeBounded

import Decidable.Equality

import Data.String
import Data.List.Elem
import Data.List.Quantifiers

import Toolkit.Decidable.Do
import Toolkit.Decidable.Informative

import Toolkit.Data.Nat
import Toolkit.Data.Pair
import Toolkit.Data.List.Size
import Toolkit.Data.List.Occurs.Does

%default total

namespace Vertex
  public export
  data Flow = SRC | SNK | BI

  export
  Show Flow where
    show SRC = "IN"
    show SNK = "OUT"
    show BI = "INOUT"

  Uninhabited (SRC = SNK) where
    uninhabited Refl impossible

  Uninhabited (SRC = BI) where
    uninhabited Refl impossible

  Uninhabited (SNK = BI) where
    uninhabited Refl impossible

  DecEq Flow where
    decEq SRC SRC = Yes Refl
    decEq SRC SNK = No absurd
    decEq SRC BI = No absurd
    decEq SNK SRC = No (negEqSym absurd)
    decEq SNK SNK = Yes Refl
    decEq SNK BI = No absurd
    decEq BI SRC = No (negEqSym absurd)
    decEq BI SNK = No (negEqSym absurd)
    decEq BI BI = Yes Refl

  public export
  data Vertex a = Node a Nat Nat Nat
              | Leaf a Flow Nat Nat

  Uninhabited (Node d k j i = Leaf a s x y) where
    uninhabited Refl impossible

  decEq : DecEq type => (a,b : Vertex type) -> Dec (a = b)
  decEq (Node d k j i) (Node e a b c)
    = decDo $ do Refl <- decEq d e `otherwise` (\Refl => Refl)
                 Refl <- decEq k a `otherwise` (\Refl => Refl)
                 Refl <- decEq j b `otherwise` (\Refl => Refl)
                 Refl <- decEq i c `otherwise` (\Refl => Refl)
                 pure Refl

  decEq (Node _ _ _ _) (Leaf _ _ _ _) = No absurd

  decEq (Leaf _ _ _ _) (Node _ _ _ _) = No (negEqSym absurd)

  decEq (Leaf d k j i) (Leaf e a b c)
    = decDo $ do Refl <- decEq d e `otherwise` (\Refl => Refl)
                 Refl <- decEq k a `otherwise` (\Refl => Refl)
                 Refl <- decEq j b `otherwise` (\Refl => Refl)
                 Refl <- decEq i c `otherwise` (\Refl => Refl)
                 pure Refl

  export
  DecEq type => DecEq (Vertex type ) where
    decEq = Vertex.decEq

  namespace API
    public export
    ident : Vertex type -> Nat
    ident (Node d   k j i) = k
    ident (Leaf d f k j)   = k

    public export
    degreeOut : Vertex type -> Nat
    degreeOut (Node _ k j i)   = i
    degreeOut (Leaf _ SRC k j) = j
    degreeOut (Leaf _ SNK k j) = 0
    degreeOut (Leaf _ BI k j)  = j

    public export
    degreeIn : Vertex type -> Nat
    degreeIn (Node _ k j i)   = j
    degreeIn (Leaf _ SRC k j) = 0
    degreeIn (Leaf _ SNK k j) = j
    degreeIn (Leaf _ BI k j)  = j

    export
    driver : type -> Nat -> Nat -> Vertex type
    driver d = Leaf d SRC

    export
    catcher : type -> Nat -> Nat -> Vertex type
    catcher d = Leaf d SNK

    export
    gateway : type -> Nat -> Nat -> Vertex type
    gateway d = Leaf d BI

    export
    node : type -> Nat -> Nat -> Nat -> Vertex type
    node = Node

    export
    both : type -> Nat -> Nat -> Vertex type
    both d i n = Node d i n n

namespace Graph

  public export
  Vertices : Type -> Type
  Vertices = (List . Vertex)

  public export
  Edge : Type
  Edge = Pair Nat Nat

  public export
  Edges : Type
  Edges = List Edge

  public export
  record Graph type where
    constructor MkGraph
    nodes : Vertices type
    edges : Edges

  public export
  empty : Graph type
  empty = MkGraph Nil Nil

  namespace API

    export
    insertNode : DecEq type => Vertex type -> Graph type -> Graph type
    insertNode k (MkGraph nodes edges) with (isElem k nodes)
      insertNode k (MkGraph nodes edges) | (Yes prf)
        = MkGraph nodes edges
      insertNode k (MkGraph nodes edges) | (No contra)
        = MkGraph (k::nodes) edges

    export
    insertEdge : (Nat, Nat) -> Graph type -> Graph type
    insertEdge (a, b) = { edges $= (::) (a,b)}

    from : DecEq type
        => Graph type
        -> Vertices type
        -> Edges
        -> Graph type
    from g nodes
      = foldr insertEdge (foldr insertNode g nodes)

    export
    fromLists : DecEq type => Vertices type -> Edges -> Graph type
    fromLists = from empty

    export
    updateWith : DecEq type
              => Graph type
              -> Vertices type
              -> Edges
              -> Graph type
    updateWith = from

    export
    merge : DecEq type => (a,b : Graph type) -> Graph type
    merge (MkGraph vs es) g
      = from g vs es

-- [ EOF ]

max_stars_repo_name: gallais/linear-circuits

max_issues_repo_name: gallais/linear-circuits

max_forks_repo_name: gallais/linear-circuits


text:
module Data.Optics.Lens

import Data.Morphisms

||| Lens
data Lens s a =
  MkLens (s -> a) (s -> a -> s)

%name Lens lens, lens1, lens2

%default total

||| return the getter part of the lens
get: Lens s a -> (s -> a)
get (MkLens get set)  = get

||| return the setter part of the lens
set: Lens s a -> (s -> a -> s)
set (MkLens get set)  = set

||| modify the part of a structure
modify: (a -> a) -> Lens s a -> s -> s
modify f lens s =  set lens s (f . (get lens) $ s)

||| modify the part of a structure using an Endomorphism
modifyE: Endomorphism a -> (Lens s a) -> s -> s
modifyE (Endo f) lens = modify f lens

||| modify the part of a structure using a functor to do so
modifyF : Functor m => (a -> m a) -> Lens s a -> s -> m s
modifyF f lens s = map (set lens s) (f . (get lens) $ s)

||| modify the part of a structure using a kleisli morphism
modifyK: Monad m => Kleislimorphism m a a -> Lens s a -> (s -> m s)
modifyK kleisli lens = modifyF (applyKleisli kleisli) lens

--
--  Compositions
--

infixr 9 #:+
||| compose two lenses
(#:+) : Lens a b -> Lens s a -> Lens s b
lens2 #:+ lens1 = MkLens newGet newSet
  where
    newGet : s -> b
    newGet= get lens2 . get lens1

    newSet: s -> b -> s
    newSet s b = let a' = get lens1 s
                     newA = set lens2 a' b
                     newS = set lens1 s newA in
                     newS

infixr 9 +:#
(+:#) : Lens s a -> Lens a b -> Lens s b
(+:#) = flip (#:+)

max_stars_repo_name: justjoheinz/idris-optics

max_issues_repo_name: justjoheinz/idris-optics

max_forks_repo_name: justjoheinz/idris-optics


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

%name Vect xs, ys, zs

my_cong : forall f . (x : a) -> (y : a) -> x = y -> f x = f y

my_curry : ((a, b) -> c) -> a -> b -> c

my_uncurry : (a -> b -> c) -> (a, b) -> c

append : Vect n a -> Vect m a -> Vect (n + m) a

lappend : (1 xs : List a) -> (1 ys : List a) -> List a

zipWith : (a -> b -> c) -> Vect n a -> Vect n b -> Vect n c

data Env : Vect n Type -> Type where
     ENil : Env []
     ECons : a -> Env xs -> Env (a :: xs)

%name Env es

data Elem : a -> Vect n a -> Type where
     Here : Elem x (x :: xs)
     There : (p : Elem x xs) -> Elem x (y :: xs)

lookup : Elem ty vs -> Env vs -> ty

data Tree : (a : Type) -> Type where
  Leaf : a -> Tree a
  Node : a -> Tree a -> Tree a -> Tree a

foo : Tree Nat


text:
module Hedgehog.Internal.Seed

import Data.Bounded
import Data.Bits
import Data.DPair
import Data.Fin

import Generics.Derive

%default total

%language ElabReflection

--------------------------------------------------------------------------------
--          Implementation Utilities
--------------------------------------------------------------------------------

shiftXor : Index {a = Bits64} -> Bits64 -> Bits64
shiftXor n w = w `xor` (w `shiftR` n)

shiftXorMultiply : Index {a = Bits64} -> Bits64 -> Bits64 -> Bits64
shiftXorMultiply n k w = shiftXor n w * k

-- Note: in JDK implementations the mix64 and mix64variant13
-- (which is inlined into mixGamma) are swapped.
mix64 : Bits64 -> Bits64
mix64 z0 =
   -- MurmurHash3Mixer
    let z1 = shiftXorMultiply 33 0xff51afd7ed558ccd z0
        z2 = shiftXorMultiply 33 0xc4ceb9fe1a85ec53 z1
        z3 = shiftXor 33 z2
    in z3

-- used only in mixGamma
mix64variant13 : Bits64 -> Bits64
mix64variant13 z0 =
   -- Better Bit Mixing - Improving on MurmurHash3's 64-bit Finalizer
   -- http://zimbry.blogspot.fi/2011/09/better-bit-mixing-improving-on.html
   --
   -- Stafford's Mix13
    let z1 = shiftXorMultiply 30 0xbf58476d1ce4e5b9 z0 -- MurmurHash3 mix constants
        z2 = shiftXorMultiply 27 0x94d049bb133111eb z1
        z3 = shiftXor 31 z2
    in z3

mixGamma : Bits64 -> Bits64
mixGamma z0 =
    let z1 = mix64variant13 z0 .|. 1             -- force to be odd
        n  = popCount (z1 `xor` (z1 `shiftR` 1))
    -- see: http://www.pcg-random.org/posts/bugs-in-splitmix.html
    -- let's trust the text of the paper, not the code.
    in if n >= 24
        then z1
        else z1 `xor` 0xaaaaaaaaaaaaaaaa

goldenGamma : Bits64
goldenGamma = 0x9e3779b97f4a7c15

bits64ToDouble : Bits64 -> Double
bits64ToDouble = fromInteger . cast

doubleUlp : Double
doubleUlp =  1.0 / bits64ToDouble (1 `shiftL` 53)

mask : Bits64 -> Bits64
mask n = sl 1
       . sl 2
       . sl 4
       . sl 8
       . sl 16
       $ sl 32 maxBound
  where sl : Index {a = Bits64} -> Bits64 -> Bits64
        sl s x = let x' = shiftR x s
                  in if x' < n then x else x'

two64 : Integer
two64 = 1 `shiftL` 64

--------------------------------------------------------------------------------
--          Seed
--------------------------------------------------------------------------------

public export
data Seed = MkSeed Bits64 Bits64

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

||| Create an Seed from the given seed.
export
smGen : Bits64 -> Seed
smGen s = MkSeed (mix64 s) (mixGamma (s + goldenGamma))

%foreign "scheme:blodwen-random"
         "javascript:lambda:x=>BigInt(Math.floor(Math.random() * Number(x)))"
prim__random_Bits64 : Bits64 -> PrimIO Bits64

||| Initialize 'SMGen' using entropy available on the system (time, ...)
export
initSMGen : HasIO io => io Seed
initSMGen = liftIO
          . map smGen
          $ fromPrim (prim__random_Bits64 maxBound)

||| Split a generator into a two uncorrelated generators.
|||
||| Note: This is `splitSMGen` in Haskell
export
split : Seed -> (Seed, Seed)
split (MkSeed seed gamma) =
  let seed'  = seed  + gamma
      seed'' = seed' + gamma
   in (MkSeed seed'' gamma, MkSeed (mix64 seed') (mixGamma seed''))

||| Generates a 64-bit value
export
nextBits64 : Seed -> (Bits64, Seed)
nextBits64 (MkSeed seed gamma) = let seed' = seed + gamma
                                  in (mix64 seed', MkSeed seed' gamma)

||| Generate a `Double` in [0, 1) range.
export
nextDouble : Seed -> (Double, Seed)
nextDouble g = let (w64,g') = nextBits64 g
                in (bits64ToDouble (w64 `shiftR` 11) * doubleUlp, g')

||| Generate a `Double` in [x, y) range.
export
nextDoubleR : (lower: Double) -> (upper: Double) -> Seed -> (Double, Seed)
nextDoubleR x y = let g = \l,u => let diff = u - l
                                   in mapFst (\f => l + f * diff) . nextDouble
                   in if x <= y then g x y else g y x

--------------------------------------------------------------------------------
--          Generating Integer Ranges
--------------------------------------------------------------------------------

||| Generates values in the closed interval [0,range].
export
nextBits64R : (range : Bits64) -> Seed -> (Bits64,Seed)
nextBits64R range = go 100 (mask range)
  where go : Nat -> Bits64 -> Seed -> (Bits64, Seed)
        go 0 _ gv       = (0,gv)
        go (S k) msk gv = let (x,gv') = nextBits64 gv
                              x' = x .&. msk
                           in if x' > range
                                then go k msk gv'
                                else (x', gv')

-- bitmask with rejection for Integers.
nextIntegerImpl : Integer -> Seed -> (Integer,Seed)
nextIntegerImpl range = let (leadMask,restDigits) = calc 0 range
                         in loop 100 leadMask restDigits
  where calc : Nat -> Integer -> (Bits64,Nat)
        calc n x  = if x < two64
                       then (mask $ cast x, n)
                       else calc (n + 1) (assert_smaller x (x `shiftR` 64))

        go : Integer -> Nat -> Seed -> (Integer, Seed)
        go acc 0     g = (acc, g)
        go acc (S k) g = let (x, g') = nextBits64 g
                          in go (shiftL acc 64 .|. cast x) k g'

        loop : Nat -> Bits64 -> Nat -> Seed -> (Integer,Seed)
        loop 0     _   _ gv = (0,gv)
        loop (S k) bm rd g0 = let (x,g1) = nextBits64 g0
                                  (n,g') = go (cast $ x .&. bm) rd g1
                               in if n <= range
                                    then (n,g')
                                    else loop k bm rd g'

export
nextIntegerR : (Integer,Integer) -> Seed -> (Integer,Seed)
nextIntegerR (x,y) = let f = \l,u => mapFst (l+) . nextIntegerImpl (u-l)
                      in if x <= y then f x y else f y x


text:
module Mmhelloworld.IdrisJackson.Core

import IdrisJvm.IO

%access public export

JsonGenerator : Type
JsonGenerator = JVM_Native (Class "com/fasterxml/jackson/core/JsonGenerator")

JsonParser : Type
JsonParser = JVM_Native (Class "com/fasterxml/jackson/core/JsonParser")

TreeNode : Type
TreeNode = JVM_Native (Interface "com/fasterxml/jackson/core/TreeNode")

max_stars_repo_name: mmhelloworld/idris-jackson

max_issues_repo_name: mmhelloworld/idris-jackson

max_forks_repo_name: mmhelloworld/idris-jackson


text:
module Data.MSF

import public Data.MSF.Core
import public Data.MSF.Event
import public Data.MSF.Running
import public Data.MSF.Util
import public Data.SOP


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

import GRL.Lang.GLang
import Sif.Types
import Sif.Pattern.Model

%access export

namespace AST

  public export
  data SifAST : SifTy -> Type where
    Req : (ident : String)
       -> (ty    : RTy)
       -> (title : String)
       -> (desc  : Maybe String)
       -> SifAST TyREQ

    Problem : (ident : String)
           -> (title : String)
           -> (desc  : Maybe String)
           -> (contexts : List (Pair String SifDomain))
           -> List (SifAST TyREQ)
           -> SifAST TyPROBLEM

    Affect : (value : CValue)
          -> (id : String)
          -> (desc : Maybe String)
          -> SifAST TyAFFECTS

    Trait : (ty : TTy)
         -> (title : String)
         -> (value : SValue)
         -> (desc  : Maybe String)
         -> (affects : List (SifAST TyAFFECTS))
         -> SifAST tyTRAIT

    Property : (title : String)
            -> (desc : Maybe String)
            -> (traits : List (SifAST TyTRAIT))
            -> SifAST tyPROPERTY

    Solution : (title : String)
            -> (probID : Pair String (Maybe String)) -- problem id and pattern desc
            -> (desc : Maybe String)
            -> (ctxtID : String)
            -> (properties : List (SifAST TyPROPERTY))
            -> SifAST TySOLUTION

    Pattern : (title : String)
           -> (desc : Maybe String)
           -> (problem : SifAST TyPROBLEM)
           -> (solution : SifAST TySOLUTION)
           -> SifAST TyPATTERN

  getSolutionContextID : SifAST TySOLUTION -> String
  getSolutionContextID (Solution _ _ _ id _) = id

  getProblemDomains : SifAST TyPROBLEM -> List (String, SifDomain)
  getProblemDomains (Problem _ _ _ cs _) = cs

  compatible : SifAST TyPROBLEM -> SifAST TySOLUTION -> Maybe SifDomain
  compatible p s = lookup (getSolutionContextID s) (getProblemDomains p)

  Show (SifAST ty) where
    show (Req i ty t d)       = unwords ["Req", show i, show ty, show t, show d]
    show (Problem i t d c rs) = unwords ["Problem", show i, show t, show d, show c, show rs]
    show (Affect v i d)       = unwords ["Affect", show v, show i, show d]
    show (Trait ty t v d as)  = unwords ["Trait", show ty, show t, show v, show d, show as]
    show (Property t d ts)    = unwords ["Property", show t, show d, show ts]
    show (Solution t p d c ps) = unwords ["Solution", show t, show p, show d, show c, show ps]
    show (Pattern t d p s)     = unwords ["Pattern", show t, show d, show p, show s]

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


text:
||| A small library introducing string positions
||| This can be used as an alternative to unpacking a string into a list of
||| characters
module Data.String.Position

import Data.String

%default total

||| @ValidPosition points to an existing character into
||| @str  its parameter string
||| Do NOT publicly export so that users cannot manufacture arbitrary positions
export
record ValidPosition (str : String) where
  constructor MkValidPosition
  ||| @currentIndex is the valid position into str
  currentIndex    : Int
  ||| @parameterLength is the length of the parameter str
  parameterLength : Int
-- TODO: add invariants?
--  0 isLength : length str === parameterLength
--  0 isIndex  : (0 `LTE` currentIndex, 0 `LT` parameterLength)

||| A position is either a ValidPosition or the end of the string
public export
Position : String -> Type
Position str = Maybe (ValidPosition str)

||| Manufacture a position by checking it is strictly inside the string
export
mkPosition : (str : String) -> Int -> Position str
mkPosition str idx
  = do let len : Int = cast (length str)
       guard (0 <= idx && idx < len)
       pure (MkValidPosition idx len)

||| Move a position (note that we do not need access to the string here)
export
mvPosition : ValidPosition str -> Int -> Position str
mvPosition (MkValidPosition pos len) idx
  = do guard (0 <= idx && idx < len)
       pure (MkValidPosition idx len)

||| Find the initial position inside the input string
export
init : (str : String) -> Position str
init str = mkPosition str 0

||| Move from a valid position to the next position in the string
export
next : ValidPosition str -> Position str
next (MkValidPosition pos len)
  = do let idx = pos + 1
       guard (idx < len)
       pure (MkValidPosition idx len)

||| We can safely access the character at a valid position
export
index : {str : _} -> ValidPosition str -> Char
index pos = assert_total (strIndex str pos.currentIndex)

||| We can successfully uncons the substring starting at a `ValidPosition`.
||| Note that we can use `map uncons pos` to uncons the substring starting
||| a `Position`.
export
uncons : {str : _} -> ValidPosition str -> (Char, Position str)
uncons pos = (index pos, next pos)

||| @span keeps munching characters of the substring starting at a given
||| position as long as the predicate is true of them. It returns the position
||| after the last successful munch.
||| Using `subString` to recover the string selected by `span` should yield
||| the same result as Data.String's `span`. That is to say we should have:
||| ```
||| subString pos (Position.span p pos) = String.span p (subString pos Nothing)
||| ```
export
span : {str : _} -> (Char -> Bool) -> Position str -> Position str
span p pos = do (c, str) <- map uncons pos
                if p c then assert_total (span p str) else pos

||| @count computes the length of the substring one would obtain if one were
||| to filter out characters based on the predicate passed as an argument.
||| It replaces the `length (filter p (fastUnpack str))` pattern.
export
count : {str : _} -> (Char -> Bool) -> Position str -> Nat
count p Nothing = 0
count p (Just pos) =
  if p (index pos)
    then S (assert_total (count p (next pos)))
    else assert_total (count p (next pos))

||| Distance between a starting position and an end one.
||| We assume that the end position is *after* the starting one, otherwise the
||| output may be negative.
export
distance : (start : Position str) ->
           (end : Position str) -> Int
distance Nothing _ = 0
distance (Just pos) pos' =
  let start = pos.currentIndex
      end = maybe pos.parameterLength currentIndex pos'
  in end - start

||| the substring of length `distance start end` that is contained between
||| start (inclusive) and end (exclusive).
export
subString : {str : _} ->
            (start : Position str) ->
            (end : Position str) -> String
subString Nothing pos' = ""
subString (Just pos) pos' =
  let start = pos.currentIndex
      end = maybe pos.parameterLength currentIndex pos'
  in assert_total (strSubstr start (end - start) str)


text:
module Circuits.NetList.AST

import Toolkit.Data.Location
import Toolkit.Data.Whole

import Ref
import Circuits.NetList.Types

%default total

public export
data AST = Var Ref
         | Port FileContext Direction DType Ref AST
         | Wire FileContext DType Ref AST
         | GateDecl FileContext Ref AST AST

         | Shim FileContext Direction AST
         | Assign FileContext AST AST AST

         | Mux FileContext AST AST AST AST

         | GateU FileContext Unary.Kind AST AST
         | GateB FileContext Binary.Kind AST AST AST

         | Index FileContext Nat AST

         | Split   FileContext AST AST AST
         | Collect FileContext AST AST AST

         | Stop FileContext

export
setSource : String -> AST -> AST
setSource new (Var x)
  = Var ({span $= setSource new} x)

setSource new (Port x y z w v)
  = (Port (setSource new x)
           y
           z
           (setSource new w)
           (setSource new v))

setSource new (Wire x y z w)
  = (Wire (setSource new x)
          y
          (setSource new z)
          (setSource new w))

setSource new (GateDecl x v y z)
  = (GateDecl (setSource new x)
              (setSource new v)
          (setSource new y)
          (setSource new z))

setSource new (Assign fc i o rest)
  = Assign (setSource new fc)
           (setSource new i)
           (setSource new o)
           (setSource new rest)

setSource new (Shim fc d i)
  = Shim (setSource new fc)
         d
         (setSource new i)

setSource new (Mux x y z w v)
  = (Mux (setSource new x)
         (setSource new y)
         (setSource new z)
         (setSource new w)
         (setSource new v))

setSource new (GateU x k y z)
  = (GateU (setSource new x)
         k
         (setSource new y)
         (setSource new z))

setSource new (GateB x y z w v)
  = (GateB (setSource new x)
          y
          (setSource new z)
          (setSource new w)
          (setSource new v))

setSource new (Stop x)
  = (Stop (setSource new x))

setSource new (Index x y z)
  = (Index (setSource new x)
            y
            (setSource new z))

setSource new (Split fc a b i)
  = Split (setSource new fc)
          (setSource new a)
          (setSource new b)
          (setSource new i)

setSource new (Collect fc a b i)
  = Collect (setSource new fc)
            (setSource new a)
            (setSource new b)
            (setSource new i)

-- [ EOF ]


text:
-- exercises in "Type-Driven Development with Idris"
-- chapter 6

import Data.Vect

-- check that all functions are total
%default total

Matrix : (rows : Nat) -> (cols : Nat) -> Type -> Type
Matrix n m t = Vect n (Vect m t)

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

-- for the fun, we rewrite the examples from chapter 3

createEmptyVector : Matrix n 0 t
createEmptyVector {n} = replicate n []

transposeMatrix : Matrix m n t -> Matrix n m t
transposeMatrix [] = createEmptyVector
transposeMatrix (x :: xs) = let xsTrans = transposeMatrix xs in
                                zipWith (::) x xsTrans

addVector : Num t => Vect n t -> Vect n t -> Vect n t
addVector = zipWith (+)

multVector : Num t => Vect n t -> Vect n t -> t
multVector xs ys = sum $ zipWith (*) xs ys

addMatrix : Num t => Matrix m n t -> Matrix m n t -> Matrix m n t
addMatrix = zipWith (addVector)

multMatrixHelper2 : Num t => Vect n t -> Matrix p n t -> Vect p t
multMatrixHelper2 x ys = map (multVector x) ys

multMatrixHelper : Num t => Matrix m n t -> Matrix p n t -> Matrix m p t
multMatrixHelper xs ys = map (flip multMatrixHelper2 $ ys) xs

multMatrix : Num t => Matrix m n t -> Matrix n p t -> Matrix m p t
multMatrix xs ys = multMatrixHelper xs $ transposeMatrix ys

v1 : Matrix 3 2 Nat
v1 = [[1,2],[3,4],[5,6]]

v2 : Matrix 2 4 Nat
v2 = [[7,8,9,10],[11,12,13,14]]

v1v1 : Matrix 3 2 Nat
v1v1 = addMatrix v1 v1
-- v1v1 : Matrix 3 2 Nat
-- [[2, 4], [6, 8], [10, 12]] : Vect 3 (Vect 2 Nat)

v1v2 : Matrix 3 4 Nat
v1v2 = multMatrix v1 v2
-- v1v2 : Matrix 3 4 Nat
-- [[29, 32, 35, 38], [65, 72, 79, 86], [101, 112, 123, 134]] : Vect 3 (Vect 4 Nat)

-- we get nice error messages
--
-- > addMatrix v1 v2
-- (input):1:1-15:When checking an application of function Main.addMatrix:
--         Type mismatch between
--                 Matrix 2 4 Nat (Type of v2)
--         and
--                 Matrix 3 2 Nat (Expected type)
-- > multMatrix v1 v1
-- (input):1:1-16:When checking an application of function Main.multMatrix:
--         Type mismatch between
--                 Matrix 3 2 Nat (Type of v1)
--         and
--                 Matrix 2 p Nat (Expected type)

max_stars_repo_name: pascalpoizat/idris-book

max_issues_repo_name: pascalpoizat/idris-book

max_forks_repo_name: pascalpoizat/idris-book