text:
module Compiler.Scheme.Racket

import Compiler.Common
import Compiler.CompileExpr
import Compiler.Generated
import Compiler.Inline
import Compiler.Scheme.Common

import Core.Options
import Core.Context
import Core.Context.Log
import Core.Directory
import Core.Name
import Core.TT
import Libraries.Utils.Hex
import Libraries.Utils.Path

import Data.List
import Data.Maybe
import Libraries.Data.NameMap
import Data.Nat
import Data.String
import Data.Vect

import Idris.Env

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

%default covering

findRacket : IO String
findRacket =
  do env <- idrisGetEnv "RACKET"
     pure $ fromMaybe "/usr/bin/env racket" env

findRacoExe : IO String
findRacoExe =
  do env <- idrisGetEnv "RACKET_RACO"
     pure $ (fromMaybe "/usr/bin/env raco" env) ++ " exe"

schHeader : Bool -> String -> String
schHeader prof libs
  = "#lang racket/base\n" ++
    "; " ++ (generatedString "Racket") ++ "\n" ++
    "(require racket/async-channel)\n" ++ -- for asynchronous channels
    "(require racket/future)\n" ++ -- for parallelism/concurrency
    "(require racket/math)\n" ++ -- for math ops
    "(require racket/system)\n" ++ -- for system
    "(require rnrs/bytevectors-6)\n" ++ -- for buffers
    "(require rnrs/io/ports-6)\n" ++ -- for files
    "(require srfi/19)\n" ++ -- for file handling and data
    "(require ffi/unsafe ffi/unsafe/define)\n" ++ -- for calling C
    (if prof then "(require profile)\n" else "") ++
    "(require racket/flonum)\n" ++ -- for float-typed transcendental functions
    libs ++
    "(let ()\n"

schFooter : String
schFooter = ") (collect-garbage)"

showRacketChar : Char -> String -> String
showRacketChar '\\' = ("\\\\" ++)
showRacketChar c
   = if c < chr 32 || c > chr 126
        then (("\\u" ++ leftPad '0' 4 (asHex (cast c))) ++)
        else strCons c

showRacketString : List Char -> String -> String
showRacketString [] = id
showRacketString ('"'::cs) = ("\\\"" ++) . showRacketString cs
showRacketString (c ::cs) = (showRacketChar c) . showRacketString cs

racketString : String -> String
racketString cs = strCons '"' (showRacketString (unpack cs) "\"")

mutual
  racketPrim : Int -> ExtPrim -> List NamedCExp -> Core String
  racketPrim i GetField [NmPrimVal _ (Str s), _, _, struct,
                         NmPrimVal _ (Str fld), _]
      = do structsc <- schExp racketPrim racketString 0 struct
           pure $ "(" ++ s ++ "-" ++ fld ++ " " ++ structsc ++ ")"
  racketPrim i GetField [_,_,_,_,_,_]
      = pure "(error \"bad getField\")"
  racketPrim i SetField [NmPrimVal _ (Str s), _, _, struct,
                         NmPrimVal _ (Str fld), _, val, world]
      = do structsc <- schExp racketPrim racketString 0 struct
           valsc <- schExp racketPrim racketString 0 val
           pure $ mkWorld $
                "(set-" ++ s ++ "-" ++ fld ++ "! " ++ structsc ++ " " ++ valsc ++ ")"
  racketPrim i SetField [_,_,_,_,_,_,_,_]
      = pure "(error \"bad setField\")"
  racketPrim i SysCodegen []
      = pure $ "\"racket\""
  racketPrim i OnCollect [_, p, c, world]
      = do p' <- schExp racketPrim racketString 0 p
           c' <- schExp racketPrim racketString 0 c
           pure $ mkWorld $ "(blodwen-register-object " ++ p' ++ " " ++ c' ++ ")"
  racketPrim i OnCollectAny [p, c, world]
      = do p' <- schExp racketPrim racketString 0 p
           c' <- schExp racketPrim racketString 0 c
           pure $ mkWorld $ "(blodwen-register-object " ++ p' ++ " " ++ c' ++ ")"
  racketPrim i MakeFuture [_, work]
      = do work' <- schExp racketPrim racketString 0 work
           pure $ mkWorld $ "(blodwen-make-future " ++ work' ++ ")"
  racketPrim i prim args
      = schExtCommon racketPrim racketString i prim args

-- Reference label for keeping track of loaded external libraries
data Loaded : Type where

-- Label for noting which struct types are declared
data Structs : Type where

-- Label for noting which foreign names are declared
data Done : Type where

cftySpec : FC -> CFType -> Core String
cftySpec fc CFUnit = pure "_void"
cftySpec fc CFInt = pure "_int"
cftySpec fc CFInt8 = pure "_int8"
cftySpec fc CFInt16 = pure "_int16"
cftySpec fc CFInt32 = pure "_int32"
cftySpec fc CFInt64 = pure "_int64"
cftySpec fc CFUnsigned8 = pure "_uint8"
cftySpec fc CFUnsigned16 = pure "_uint16"
cftySpec fc CFUnsigned32 = pure "_uint32"
cftySpec fc CFUnsigned64 = pure "_uint64"
cftySpec fc CFString = pure "_string/utf-8"
cftySpec fc CFDouble = pure "_double"
cftySpec fc CFChar = pure "_int8"
cftySpec fc CFPtr = pure "_pointer"
cftySpec fc CFGCPtr = pure "_pointer"
cftySpec fc CFBuffer = pure "_bytes"
cftySpec fc (CFIORes t) = cftySpec fc t
cftySpec fc (CFStruct n t) = pure $ "_" ++ n ++ "-pointer"
cftySpec fc (CFFun s t) = funTySpec [s] t
  where
    funTySpec : List CFType -> CFType -> Core String
    funTySpec args (CFFun CFWorld t) = funTySpec args t
    funTySpec args (CFFun s t) = funTySpec (s :: args) t
    funTySpec args retty
        = do rtyspec <- cftySpec fc retty
             argspecs <- traverse (cftySpec fc) (reverse args)
             pure $ "(_fun " ++ showSep " " argspecs ++ " -> " ++ rtyspec ++ ")"
cftySpec fc t = throw (GenericMsg fc ("Can't pass argument of type " ++ show t ++
                         " to foreign function"))

loadlib : String -> String -> String
loadlib "libc" _ = "(define-ffi-definer define-libc (ffi-lib #f))\n"
loadlib libn ver
    = "(define-ffi-definer define-" ++ libn ++
      " (ffi-lib \"" ++ libn ++ "\" " ++ ver ++ "))\n"

getLibVers : String -> (String, String)
getLibVers libspec
    = case words libspec of
           [] => ("", "")
           [fn] => case span (/='.') libspec of
                        (root, rest) => (root, "")
           (fn :: vers) =>
               (fst (span (/='.') fn),
                  "'(" ++ showSep " " (map show vers) ++ " #f)" )

cToRkt : CFType -> String -> String
cToRkt CFChar op = "(integer->char " ++ op ++ ")"
cToRkt _ op = op

rktToC : CFType -> String -> String
rktToC CFChar op = "(char->integer " ++ op ++ ")"
rktToC _ op = op

handleRet : CFType -> String -> String
handleRet CFUnit op = op ++ " " ++ mkWorld (schConstructor racketString (UN $ Basic "") (Just 0) [])
handleRet ret op = mkWorld (cToRkt ret op)

cCall : {auto f : Ref Done (List String) } ->
        {auto c : Ref Ctxt Defs} ->
        {auto l : Ref Loaded (List String)} ->
        String -> FC -> (cfn : String) -> (clib : String) ->
        List (Name, CFType) -> CFType -> Core (String, String)
cCall appdir fc cfn clib args (CFIORes CFGCPtr)
    = throw (GenericMsg fc "Can't return GCPtr from a foreign function")
cCall appdir fc cfn clib args CFGCPtr
    = throw (GenericMsg fc "Can't return GCPtr from a foreign function")
cCall appdir fc cfn clib args (CFIORes CFBuffer)
    = throw (GenericMsg fc "Can't return Buffer from a foreign function")
cCall appdir fc cfn clib args CFBuffer
    = throw (GenericMsg fc "Can't return Buffer from a foreign function")
cCall appdir fc cfn libspec args ret
    = do loaded <- get Loaded
         bound <- get Done

         let (libn, vers) = getLibVers libspec
         lib <- if libn `elem` loaded
                   then pure ""
                   else do put Loaded (libn :: loaded)
                           (fname, fullname) <- locate libspec
                           copyLib (appdir </> fname, fullname)
                           pure (loadlib libn vers)

         argTypes <- traverse (\a => do s <- cftySpec fc (snd a)
                                        pure (a, s)) args
         retType <- cftySpec fc ret
         cbind <- if cfn `elem` bound
                     then pure ""
                     else do put Done (cfn :: bound)
                             pure $ "(define-" ++ libn ++ " " ++ cfn ++
                                    " (_fun " ++ showSep " " (map snd argTypes) ++ " -> " ++
                                        retType ++ "))\n"
         let call = "(" ++ cfn ++ " " ++
                    showSep " " !(traverse useArg (map fst argTypes)) ++ ")"

         pure (lib ++ cbind, case ret of
                                  CFIORes rt => handleRet rt call
                                  _ => call)
  where
    mkNs : Int -> List CFType -> List (Maybe (String, CFType))
    mkNs i [] = []
    mkNs i (CFWorld :: xs) = Nothing :: mkNs i xs
    mkNs i (x :: xs) = Just ("cb" ++ show i, x) :: mkNs (i + 1) xs

    applyLams : String -> List (Maybe (String, CFType)) -> String
    applyLams n [] = n
    applyLams n (Nothing :: as) = applyLams ("(" ++ n ++ " #f)") as
    applyLams n (Just (a, ty) :: as)
        = applyLams ("(" ++ n ++ " " ++ cToRkt ty a ++ ")") as

    mkFun : List CFType -> CFType -> String -> String
    mkFun args ret n
        = let argns = mkNs 0 args in
              "(lambda (" ++ showSep " " (map fst (mapMaybe id argns)) ++ ") " ++
              (applyLams n argns ++ ")")

    notWorld : CFType -> Bool
    notWorld CFWorld = False
    notWorld _ = True

    callback : String -> List CFType -> CFType -> Core String
    callback n args (CFFun s t) = callback n (s :: args) t
    callback n args_rev retty
        = do let args = reverse args_rev
             argTypes <- traverse (cftySpec fc) (filter notWorld args)
             retType <- cftySpec fc retty
             pure $ mkFun args retty n

    useArg : (Name, CFType) -> Core String
    useArg (n, CFFun s t) = callback (schName n) [s] t
    useArg (n, ty)
        = pure $ rktToC ty (schName n)

schemeCall : FC -> (sfn : String) ->
             List Name -> CFType -> Core String
schemeCall fc sfn argns ret
    = let call = "(" ++ sfn ++ " " ++ showSep " " (map schName argns) ++ ")" in
          case ret of
               CFIORes _ => pure $ mkWorld call
               _ => pure call

-- Use a calling convention to compile a foreign def.
-- Returns any preamble needed for loading libraries, and the body of the
-- function call.
useCC : {auto f : Ref Done (List String) } ->
        {auto c : Ref Ctxt Defs} ->
        {auto l : Ref Loaded (List String)} ->
        String -> FC -> List String -> List (Name, CFType) -> CFType -> Core (String, String)
useCC appdir fc ccs args ret
    = case parseCC ["scheme,racket", "scheme", "C"] ccs of
           Nothing => throw (NoForeignCC fc ccs)
           Just ("scheme,racket", [sfn]) =>
               do body <- schemeCall fc sfn (map fst args) ret
                  pure ("", body)
           Just ("scheme", [sfn]) =>
               do body <- schemeCall fc sfn (map fst args) ret
                  pure ("", body)
           Just ("C", [cfn, clib]) => cCall appdir fc cfn clib args ret
           Just ("C", [cfn, clib, chdr]) => cCall appdir fc cfn clib args ret
           _ => throw (NoForeignCC fc ccs)

-- For every foreign arg type, return a name, and whether to pass it to the
-- foreign call (we don't pass '%World')
mkArgs : Int -> List CFType -> List (Name, Bool)
mkArgs i [] = []
mkArgs i (CFWorld :: cs) = (MN "farg" i, False) :: mkArgs i cs
mkArgs i (c :: cs) = (MN "farg" i, True) :: mkArgs (i + 1) cs

mkStruct : {auto s : Ref Structs (List String)} ->
           CFType -> Core String
mkStruct (CFStruct n flds)
    = do defs <- traverse mkStruct (map snd flds)
         strs <- get Structs
         if n `elem` strs
            then pure (concat defs)
            else do put Structs (n :: strs)
                    pure $ concat defs ++ "(define-cstruct _" ++ n ++ " ("
                           ++ showSep "\n\t" !(traverse showFld flds) ++ "))\n"
  where
    showFld : (String, CFType) -> Core String
    showFld (n, ty) = pure $ "[" ++ n ++ " " ++ !(cftySpec emptyFC ty) ++ "]"
mkStruct (CFIORes t) = mkStruct t
mkStruct (CFFun a b) = do ignore (mkStruct a); mkStruct b
mkStruct _ = pure ""

schFgnDef : {auto f : Ref Done (List String) } ->
            {auto c : Ref Ctxt Defs} ->
            {auto l : Ref Loaded (List String)} ->
            {auto s : Ref Structs (List String)} ->
            String -> FC -> Name -> NamedDef -> Core (String, String)
schFgnDef appdir fc n (MkNmForeign cs args ret)
    = do let argns = mkArgs 0 args
         let allargns = map fst argns
         let useargns = map fst (filter snd argns)
         argStrs <- traverse mkStruct args
         retStr <- mkStruct ret
         (load, body) <- useCC appdir fc cs (zip useargns args) ret
         defs <- get Ctxt
         pure (concat argStrs ++ retStr ++ load,
                "(define " ++ schName !(full (gamma defs) n) ++
                " (lambda (" ++ showSep " " (map schName allargns) ++ ") " ++
                body ++ "))\n")
schFgnDef _ _ _ _ = pure ("", "")

getFgnCall : {auto f : Ref Done (List String) } ->
             {auto c : Ref Ctxt Defs} ->
             {auto l : Ref Loaded (List String)} ->
             {auto s : Ref Structs (List String)} ->
             String -> (Name, FC, NamedDef) -> Core (String, String)
getFgnCall appdir (n, fc, d) = schFgnDef appdir fc n d

startRacket : String -> String -> String -> String
startRacket racket appdir target = unlines
    [ "#!/bin/sh"
    , "# " ++ (generatedString "Racket")
    , ""
    , "set -e # exit on any error"
    , ""
    , "if [ \"$(uname)\" = Darwin ]; then"
    , "  DIR=$(zsh -c 'printf %s \"$0:A:h\"' \"$0\")"
    , "else"
    , "  DIR=$(dirname \"$(readlink -f -- \"$0\")\")"
    , "fi"
    , ""
    , "export LD_LIBRARY_PATH=\"$DIR/" ++ appdir ++ ":$LD_LIBRARY_PATH\""
    , racket ++ "\"$DIR/" ++ target ++ "\" \"$@\""
    ]

startRacketCmd : String -> String -> String -> String
startRacketCmd racket appdir target = unlines
    [ "@echo off"
    , "set APPDIR=%~dp0"
    , "set PATH=%APPDIR%" ++ appdir ++ ";%PATH%"
    , racket ++ "\"%APPDIR%" ++ target ++ "\" %*"
    ]

startRacketWinSh : String -> String -> String -> String
startRacketWinSh racket appdir target = unlines
    [ "#!/bin/sh"
    , "# " ++ (generatedString "Racket")
    , ""
    , "set -e # exit on any error"
    , ""
    , "DIR=$(dirname \"$(readlink -f -- \"$0\" || cygpath -a -- \"$0\")\")"
    , "PATH=\"$DIR/" ++ appdir ++ ":$PATH\""
    , racket ++ "\"$DIR/" ++ target ++ "\" \"$@\""
    ]

compileToRKT : Ref Ctxt Defs ->
               String -> ClosedTerm -> (outfile : String) -> Core ()
compileToRKT c appdir tm outfile
    = do cdata <- getCompileData False Cases tm
         let ndefs = namedDefs cdata
         let ctm = forget (mainExpr cdata)

         defs <- get Ctxt
         f <- newRef {t = List String} Done empty
         l <- newRef {t = List String} Loaded []
         s <- newRef {t = List String} Structs []
         fgndefs <- traverse (getFgnCall appdir) ndefs
         compdefs <- traverse (getScheme racketPrim racketString) ndefs
         let code = fastAppend (map snd fgndefs ++ compdefs)
         main <- schExp racketPrim racketString 0 ctm
         support <- readDataFile "racket/support.rkt"
         ds <- getDirectives Racket
         extraRuntime <- getExtraRuntime ds
         let prof = profile !getSession
         let runmain
                = if prof
                     then "(profile (void " ++ main ++ ") #:order 'self)\n"
                     else "(void " ++ main ++ ")\n"
         let scm = schHeader prof (concat (map fst fgndefs)) ++
                   support ++ extraRuntime ++ code ++
                   runmain ++ schFooter
         Right () <- coreLift $ writeFile outfile scm
            | Left err => throw (FileErr outfile err)
         coreLift_ $ chmodRaw outfile 0o755
         pure ()

makeSh : String -> String -> String -> String -> Core ()
makeSh racket outShRel appdir outAbs
    = do Right () <- coreLift $ writeFile outShRel (startRacket racket appdir outAbs)
            | Left err => throw (FileErr outShRel err)
         pure ()

||| Make Windows start scripts, one for bash environments and one batch file
makeShWindows : String -> String -> String -> String -> Core ()
makeShWindows racket outShRel appdir outAbs
    = do let cmdFile = outShRel ++ ".cmd"
         Right () <- coreLift $ writeFile cmdFile (startRacketCmd racket appdir outAbs)
            | Left err => throw (FileErr cmdFile err)
         Right () <- coreLift $ writeFile outShRel (startRacketWinSh racket appdir outAbs)
            | Left err => throw (FileErr outShRel err)
         pure ()

compileExpr : Bool -> Ref Ctxt Defs -> (tmpDir : String) -> (outputDir : String) ->
              ClosedTerm -> (outfile : String) -> Core (Maybe String)
compileExpr mkexec c tmpDir outputDir tm outfile
    = do let appDirRel = outfile ++ "_app" -- relative to build dir
         let appDirGen = outputDir </> appDirRel -- relative to here
         coreLift_ $ mkdirAll appDirGen
         Just cwd <- coreLift currentDir
              | Nothing => throw (InternalError "Can't get current directory")

         let ext = if isWindows then ".exe" else ""
         let outRktFile = appDirRel </> outfile <.> "rkt"
         let outBinFile = appDirRel </> outfile <.> ext
         let outRktAbs = cwd </> outputDir </> outRktFile
         let outBinAbs = cwd </> outputDir </> outBinFile

         compileToRKT c appDirGen tm outRktAbs
         raco <- coreLift findRacoExe
         racket <- coreLift findRacket

         ok <- the (Core Int) $ if mkexec
                  then logTime "+ Build racket" $
                         coreLift $
                           system (raco ++ " -o " ++ outBinAbs ++ " " ++ outRktAbs)
                  else pure 0
         if ok == 0
            then do -- TODO: add launcher script
                    let outShRel = outputDir </> outfile
                    if isWindows
                       then if mkexec
                               then makeShWindows "" outShRel appDirRel outBinFile
                               else makeShWindows (racket ++ " ") outShRel appDirRel outRktFile
                       else if mkexec
                               then makeSh "" outShRel appDirRel outBinFile
                               else makeSh (racket ++ " ") outShRel appDirRel outRktFile
                    coreLift_ $ chmodRaw outShRel 0o755
                    pure (Just outShRel)
            else pure Nothing

executeExpr : Ref Ctxt Defs -> (tmpDir : String) -> ClosedTerm -> Core ()
executeExpr c tmpDir tm
    = do Just sh <- compileExpr False c tmpDir tmpDir tm "_tmpracket"
            | Nothing => throw (InternalError "compileExpr returned Nothing")
         coreLift_ $ system sh

export
codegenRacket : Codegen
codegenRacket = MkCG (compileExpr True) executeExpr Nothing Nothing


text:
module Data.Strings.Extra

import Data.Maybe
import Data.List

public export
parseInteger : List Char -> Integer -> Maybe Integer
parseInteger []        acc = Just acc
parseInteger (c :: cs) acc =
  if (c >= '0' && c <= '9')
  then parseInteger cs ((acc * 10) + ((cast c) - (cast '0')))
  else Nothing

||| Joins the character lists by newlines into a single character list.
|||
||| ```idris example
||| unlines' [['l','i','n','e'], ['l','i','n','e','2'], ['l','n','3'], ['D']]
||| ```
public export
unlines' : List (List Char) -> List Char
unlines' [] = []
unlines' (l::ls) = l ++ '\n' :: unlines' ls

||| Joins the strings by newlines into a single string.
|||
||| ```idris example
||| unlines ["line", "line2", "ln3", "D"]
||| ```
public export
unlines : List String -> String
unlines = pack . unlines' . map unpack

ext: idr

max_stars_repo_name: steshaw/hsgames

max_issues_repo_name: steshaw/hsgames

max_forks_repo_name: steshaw/hsgames


text:
-- ------------------------------------------------------------- [ Example.idr ]
-- Module    : Example.idr
-- Copyright : (c) Jan de Muijnck-Hughes
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
module GRL.Lang.Test.TLang

import GRL.Lang.TLang

-- ------------------------------------------------------------ [ Sample Model ]
gpcePaper : TASK
gpcePaper = MkTask "Write GPCE paper"

gpceAbstract : SUBTASK
gpceAbstract = MkSTask "Write the abstract"

writePaper : SUBTASK
writePaper = MkSTask "Write the paper"

doWriting : ACTION
doWriting = MkAction "Do writing"

paperPlan : GModel
paperPlan = emptyModel
  \= gpcePaper
  \= gpceAbstract
  \= writePaper
  \= doWriting
  \= (gpcePaper &= gpceAbstract)
  \= (gpcePaper &= writePaper)
  \= (doWriting ==> writePaper   | MAKES)
  \= (doWriting ==> gpceAbstract | MAKES)

-- -------------------------------------------------------------------- [ Test ]
export
runTest : IO ()
runTest = do
    putStrLn $ prettyModel paperPlan
-- --------------------------------------------------------------------- [ EOF ]

max_stars_repo_name: jfdm/idris-grl

max_issues_repo_name: jfdm/idris-grl

max_forks_repo_name: jfdm/idris-grl


text:
module Network.TLS.Parse.PEM

import Control.Monad.Trans
import Data.String
import Data.String.Extra
import Data.String.Parser
import Utils.Base64
import Utils.Bytes
import Utils.Misc

public export
record PEMBlob where
  constructor MkPEMBlob
  label : String
  content : List Bits8

public export
Show PEMBlob where
  show (MkPEMBlob label content) = label <+> ": " <+> xxd content

is_label_char : Char -> Bool
is_label_char c = (not (isControl c)) && (c /= '-')

label_char : Applicative m => ParseT m Char
label_char = satisfy is_label_char <?> "expected label character"

base64_char : Applicative m => ParseT m Char
base64_char = satisfy is_base64_char <?> "expected base64 character"

takeUntil : Monad m => (stop : String) -> ParseT m ()
takeUntil stop = do
    let StrCons s top = strM stop
      | StrNil => pure ()
    takeUntil' s top
  where
    takeUntil' : Monad m' => (s : Char) -> (top : String) -> ParseT m' ()
    takeUntil' s top = do
        init <- takeWhile (/= s)
        skip $ char s <?> "end of string reached - \{show stop} not found"
        case !(succeeds $ string top) of
             False => takeUntil' s top
             True => pure ()

export
parse_pem_blob : Parser PEMBlob
parse_pem_blob = do
  takeUntil "-----BEGIN "
  label' <- many label_char
  let label = pack label'
  _ <- string "-----"
  spaces
  content <- many ((some base64_char) <* spaces)
  _ <- string "-----END "
  _ <- string label
  _ <- string "-----"
  spaces
  case base64_decode $ pack $ concat content of
    Right str => pure $ MkPEMBlob label str
    Left  err => fail $ "failed parsing PEM content: " <+> err

fold_string : String -> String
fold_string str = pack $ foldl (<+>) [] $ map (<+> ['\n']) $ chunk 64 $ unpack str

export
encode_pem_blob : PEMBlob -> String
encode_pem_blob blob =
  "-----BEGIN " <+> blob.label <+> "-----\n"
  <+> (fold_string $ base64_encode blob.content)
  <+> "-----END " <+> blob.label <+> "-----"


text:
-- ------------------------------------------------------ [ GettingStarted.idr ]
-- Module      : Exercises.Test.GettingStarted
-- Description : Test covering the Chapter 2 exercises in Edwin Brady's
--               book, "Type-Driven Development with Idris."
-- --------------------------------------------------------------------- [ EOH ]
module Exercises.Test.GettingStarted

import Exercises.GettingStarted

import Test.Helpers

import Data.Vect
%hide Data.Vect.overLength

%access export

private
testPalindrome' : String -> (String -> Bool) -> String -> Bool -> IO Bool
testPalindrome' label palindrome string isPalindrome =
  unwords [label, show string] `assertEqual'` isPalindrome $
  palindrome string

testPalindrome : String -> Bool -> IO Bool
testPalindrome = testPalindrome' "Simple.palindrome" Simple.palindrome

testPalindromeCI : String -> Bool -> IO Bool
testPalindromeCI =
  testPalindrome' "CaseInsensitive.palindrome" CaseInsensitive.palindrome

testLongPalindrome : String -> Bool -> IO Bool
testLongPalindrome =
  testPalindrome' "LongerThan10.palindrome" LongerThan10.palindrome

testPalindromeLen : Nat -> String -> Bool -> IO Bool
testPalindromeLen =
  testPalindrome' "LongerThanN.palindrome" . LongerThanN.palindrome

||| `"Hello, Idris world!"` has three words and 19 characters.
testCounts : IO Bool
testCounts =
  "counts" `assertEqual'` (3, 19) $
  counts "Hello, Idris world!"

||| `["One", "Two", "Three", "Four"]` has two strings over three characters.
testOverLength : IO Bool
testOverLength =
  "overLength" `assertEqual'` 2 $
  overLength 3 ["One", "Two", "Three", "Four"]

testTopTen : IO Bool
testTopTen =
  "topTen" `assertEqual'` [100,99..91] $
  topTen [1..100]

allTests : List (IO Bool)
allTests = [ testPalindrome "racecar" True
           , testPalindrome "race car" False
           , testPalindromeCI "Racecar" True
           , testLongPalindrome "racecar" False
           , testLongPalindrome "able was i ere i saw elba" True
           , testPalindromeLen 10 "racecar" False
           , testPalindromeLen 5 "racecar" True
           , testCounts
           , testTopTen
           , testOverLength
           ]

runTests : IO (Vect (length GettingStarted.allTests) Bool)
runTests = testChapter "2: Getting Started" allTests

-- --------------------------------------------------------------------- [ 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:
module Chapter2

import TypesAndFunctions
import Category

%default total

Exercise_2_1_1 : {cat : Category} -> {a, b, c, d : Object cat} ->
  (g : Morphism cat c d) -> (f : Morphism cat b c) ->
  postCompose {cat} {a} {b} {c=d} ((.*) {cat} {a=b} {b=c} {c=d} g f) =
    (postCompose {cat} {a} {b=c} {c=d} g) . (postCompose {cat} {a} {b} {c} f)
Exercise_2_1_1 {cat} _ _ = functionalExtensionality (Associativity cat _ _)

Exercise_2_1_2 : {cat : Category} -> {a, b, c, d : Object cat} ->
  (h : Morphism cat c d) -> (g : Morphism cat b c) -> (f : Morphism cat a b) ->
  postCompose {cat} {a} {b} {c=d} (postCompose {cat} {a=b} {b=c} {c=d} h g) f =
    postCompose h {cat} {a} {b=c} {c=d} (postCompose {cat} {a} {b} {c} g f)
Exercise_2_1_2 {cat} = Associativity cat

Exercise_2_1_3 : {cat : Category} -> {a, b, c, d : Object cat} ->
  (g : Morphism cat b c) -> (f : Morphism cat a b) ->
  preCompose {cat} {a} {b=c} {c=d} ((.*) {cat} {a} {b} {c} g f) =
    (preCompose {cat} {a} {b} {c=d} f) .
      (preCompose {cat} {a=b} {b=c} {c=d} g)
Exercise_2_1_3 {a} {b} {c} {d} {cat} _ _ =
  functionalExtensionality (\_ => sym (Associativity cat _ _ _))

{- Post-composition with the identity leaves arrows unchanged.
 - (So post-composition with the identity is itself the identity on
 - the type of arrows terminating in a.) -}
Exercise_2_3_1_post : {cat : Category} -> {a, b : Object cat} ->
  (f : Morphism cat b a) ->
  postCompose {cat} {a=b} {b=a} {c=a} (catId {cat} a) f = f
Exercise_2_3_1_post f = LeftIdentity cat f

{- Pre-composition with the identity leaves arrows unchanged.
 - (So pre-composition with the identity is itself the identity on
 - the type of arrows originating in a.) -}
Exercise_2_3_1_pre : {cat : Category} -> {a, b : Object cat} ->
  (f : Morphism cat a b) ->
  preCompose {cat} {a} {b=a} {c=b} (catId {cat} a) f = f
Exercise_2_3_1_pre f = RightIdentity cat f

max_stars_repo_name: rokopt/dao-fp-exercises

max_issues_repo_name: rokopt/dao-fp-exercises

max_forks_repo_name: rokopt/dao-fp-exercises


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

import Text.Kindle.Clippings

main : IO ()
main = printLn "Hello, World!"

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

max_stars_repo_name: yurrriq/my-clippings

max_issues_repo_name: yurrriq/my-clippings

max_forks_repo_name: yurrriq/my-clippings


text:
module Control.Effect.Exception

import Data.Contravariant

import Control.EffectAlgebra

import public Control.Effect.Fail

import Control.Monad.Either

||| Exception effect.
public export
data TryE : Type -> (Type -> Type) -> Type -> Type where
  Try : m a -> (e -> m a) -> TryE e m a

public export
Contravariant (\e => TryE e m r) where
  contramap f (Try x h) = Try x (h . f)

public export
EitherE : Type -> (Type -> Type) -> Type -> Type
EitherE e = TryE e :+: FailE e

public export
Inj (EitherE e) sig => Inj (FailE e) sig where
  inj = inj {sub = EitherE e, sup = sig} . Inr

public export
Inj (EitherE e) sig => Inj (TryE e) sig where
  inj = inj {sub = EitherE e, sup = sig} . Inl

||| Try running a computation. If it fails (via Fail) resort to the supplied callback.
public export
try : Inj (TryE e) sig => Algebra sig m => m a -> (e -> m a) -> m a
try x err = send (Try x err)

namespace Algebra
  public export
  [Either] (al : Algebra sig m) => Algebra (EitherE e :+: sig) (EitherT e m) where
    alg ctx hdl (Inl (Inr (Fail x))) = left x
    alg ctx hdl (Inl (Inl (Try t er))) =
      catchE (hdl (t <$ ctx)) (hdl . (<$ ctx) . er)
    alg ctxx hdl (Inr other) =
      let fused = (~<~) {ctx2 = ctx} {m = EitherT e m} f hdl in
      MkEitherT (alg {f = Functor.Compose} {ctx = Either e . ctx} (Right ctxx) fused other)
     where
      f : forall a. Either e (EitherT e m a) -> m (Either e a)
      f (Left x) = pure (Left x)
      f (Right x) = runEitherT x

  %hint public export
  AlgebraEither : (al : Algebra sig m) => Algebra (EitherE e :+: sig) (EitherT e m)
  AlgebraEither = Algebra.Either


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

import Config.INI

import Lightyear.Testing

%access export

-- ------------------------------------------------------------------- [ BEGIN ]

runTests : IO ()
runTests = Testing.runTests
    [ parseTest "INI Test 1"
                parseINI
                """; last modified 1 April 2001 by John Doe
[owner]
name=John Doe
organization=Acme Widgets Inc.

[database]
; use IP address in case network name resolution is not working
server=192.0.2.62
port=143
file="payroll.dat"
"""

    , parseTest "INI Test 2"
                parseINI
                """#Comment
a=b
a=c

[section]
a=b

# comment

[section]

b=b
"""
  ]
-- --------------------------------------------------------------------- [ EOF ]

max_stars_repo_name: jfdm/idris-config

max_issues_repo_name: jfdm/idris-config

max_forks_repo_name: jfdm/idris-config


text:
module Configuration

import Data.Vect
import Data.Fin

data State = UnOccupied
           | Occupied

data Square : Nat -> Type where
     Create : Vect n (Vect n State) -> Square n

times : (n : Nat) -> a -> Vect n a
times Z x = []
times (S k) x = x :: times k x

emptySquare : (n : Nat) -> Vect n (Vect n State)
emptySquare n = times n (times n UnOccupied)

empty : (n : Nat) -> Square n
empty n = Create (emptySquare n)

update : (Fin n, Fin n) -> State -> Vect n (Vect n State) -> Vect n (Vect n State)
update x y xs = xs

play : (Fin n, Fin n) -> Square n -> Square n
play (a, b) (Create xs) = let ys = update (a, b) Occupied xs in
     Create ys

max_stars_repo_name: dvberkel/pylos

max_issues_repo_name: dvberkel/pylos

max_forks_repo_name: dvberkel/pylos


text:
-- -------------------------------------------------------------- [ StringFile ]
-- Module      : Lightyear.StringFile
-- Description : String-related effectful file parsers.
--
-- This code is distributed under the BSD 2-clause license.
-- See the file LICENSE in the root directory for its full text.
-- --------------------------------------------------------------------- [ EOH ]

module Lightyear.StringFile

import public Effects
import public Effect.File

import Lightyear
import Lightyear.Strings

%access export
-- ---------------------------------------------------- [ A String File Parser ]

namespace Lightyear
  private
  readFile : (String -> e) -> String -> Eff (Either e String) [FILE_IO ()]
  readFile errFunc fname = do
      case !(open fname Read) of
        False => pure $ Left (errFunc fname)
        True => do
          src <- readAcc ""
          close
          pure $ Right src
    where
      readAcc : String -> Eff String [FILE_IO (OpenFile Read)]
      readAcc acc = if (not !(eof))
                       then readAcc (acc ++ !(readLine))
                       else pure acc

parseFile : (String -> e)
         -> (String -> String -> e)
         -> Parser a
         -> String
         -> Eff (Either e a) [FILE_IO ()]
parseFile rErr pErr p fn = do
    Right src <- Lightyear.readFile rErr fn | Left err => pure (Left err)
    case parse p src of
      Left err  => pure $ Left (pErr fn err)
      Right res => pure $ Right res

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

max_stars_repo_name: david-christiansen/lightyear

max_issues_repo_name: david-christiansen/lightyear

max_forks_repo_name: david-christiansen/lightyear


text:
module Data.Fin.Extra

import Data.Fin
import Data.Nat

import Syntax.WithProof
import Syntax.PreorderReasoning

%default total

-------------------------------
--- `finToNat`'s properties ---
-------------------------------

||| A Fin's underlying natural number is smaller than the bound
export
elemSmallerThanBound : (n : Fin m) -> LT (finToNat n) m
elemSmallerThanBound FZ = LTESucc LTEZero
elemSmallerThanBound (FS x) = LTESucc (elemSmallerThanBound x)

||| Last's underlying natural number is the bound's predecessor
export
finToNatLastIsBound : {n : Nat} -> finToNat (Fin.last {n}) = n
finToNatLastIsBound {n=Z} = Refl
finToNatLastIsBound {n=S k} = cong S finToNatLastIsBound

||| Weaken does not modify the underlying natural number
export
finToNatWeakenNeutral : {n : Fin m} -> finToNat (weaken n) = finToNat n
finToNatWeakenNeutral = finToNatQuotient (weakenNeutral n)

||| WeakenN does not modify the underlying natural number
export
finToNatWeakenNNeutral : (0 m : Nat) -> (k : Fin n) ->
                         finToNat (weakenN m k) = finToNat k
finToNatWeakenNNeutral m k = finToNatQuotient (weakenNNeutral m k)

||| `Shift k` shifts the underlying natural number by `k`.
export
finToNatShift : (k : Nat) -> (a : Fin n) -> finToNat (shift k a) = k + finToNat a
finToNatShift Z     a = Refl
finToNatShift (S k) a = cong S (finToNatShift k a)

-------------------------------------------------
--- Inversion function and related properties ---
-------------------------------------------------

||| Compute the Fin such that `k + invFin k = n - 1`
public export
invFin : {n : Nat} -> Fin n -> Fin n
invFin FZ = last
invFin (FS k) = weaken (invFin k)

export
invFinSpec : {n : _} -> (i : Fin n) -> 1 + finToNat i + finToNat (invFin i) = n
invFinSpec {n = S k} FZ = cong S finToNatLastIsBound
invFinSpec (FS k) = let H = invFinSpec k in
  let h = finToNatWeakenNeutral {n = invFin k} in
  cong S (rewrite h in H)

||| The inverse of a weakened element is the successor of its inverse
export
invFinWeakenIsFS : {n : Nat} -> (m : Fin n) -> invFin (weaken m) = FS (invFin m)
invFinWeakenIsFS FZ = Refl
invFinWeakenIsFS (FS k) = cong weaken (invFinWeakenIsFS k)

export
invFinLastIsFZ : {n : Nat} -> invFin (last {n}) = FZ
invFinLastIsFZ {n = Z} = Refl
invFinLastIsFZ {n = S n} = cong weaken (invFinLastIsFZ {n})

||| `invFin` is involutive (i.e. applied twice it is the identity)
export
invFinInvolutive : {n : Nat} -> (m : Fin n) -> invFin (invFin m) = m
invFinInvolutive FZ = invFinLastIsFZ
invFinInvolutive (FS k) = Calc $
   |~ invFin (invFin (FS k))
   ~~ invFin (weaken (invFin k)) ...( Refl )
   ~~ FS (invFin (invFin k))     ...( invFinWeakenIsFS (invFin k) )
   ~~ FS k                       ...( cong FS (invFinInvolutive k) )

--------------------------------
--- Strengthening properties ---
--------------------------------

||| It's possible to strengthen a weakened element of Fin **m**.
export
strengthenWeakenIsRight : (n : Fin m) -> strengthen (weaken n) = Just n
strengthenWeakenIsRight FZ = Refl
strengthenWeakenIsRight (FS k) = rewrite strengthenWeakenIsRight k in Refl

||| It's not possible to strengthen the last element of Fin **n**.
export
strengthenLastIsLeft : {n : Nat} -> strengthen (Fin.last {n}) = Nothing
strengthenLastIsLeft {n=Z} = Refl
strengthenLastIsLeft {n=S k} = rewrite strengthenLastIsLeft {n=k} in Refl

||| It's possible to strengthen the inverse of a succesor
export
strengthenNotLastIsRight : {n : Nat} -> (m : Fin n) -> strengthen (invFin (FS m)) = Just (invFin m)
strengthenNotLastIsRight m = strengthenWeakenIsRight (invFin m)

||| Either tightens the bound on a Fin or proves that it's the last.
export
strengthen' : {n : Nat} -> (m : Fin (S n)) ->
              Either (m = Fin.last) (m' : Fin n ** finToNat m = finToNat m')
strengthen' {n = Z} FZ = Left Refl
strengthen' {n = S k} FZ = Right (FZ ** Refl)
strengthen' {n = S k} (FS m) = case strengthen' m of
    Left eq => Left $ cong FS eq
    Right (m' ** eq) => Right (FS m' ** cong S eq)

----------------------------
--- Weakening properties ---
----------------------------

export
weakenNZeroIdentity : (k : Fin n) ->  weakenN 0 k ~~~ k
weakenNZeroIdentity FZ = FZ
weakenNZeroIdentity (FS k) = FS (weakenNZeroIdentity k)

export
shiftFSLinear : (m : Nat) -> (f : Fin n) -> shift m (FS f) ~~~ FS (shift m f)
shiftFSLinear Z     f = reflexive
shiftFSLinear (S m) f = FS (shiftFSLinear m f)

export
shiftLastIsLast : (m : Nat) -> {n : Nat} ->
                  shift m (Fin.last {n}) ~~~ Fin.last {n=m+n}
shiftLastIsLast Z = reflexive
shiftLastIsLast (S m) = FS (shiftLastIsLast m)

-----------------------------------
--- Division-related properties ---
-----------------------------------

||| A view of Nat as a quotient of some number and a finite remainder.
public export
data FractionView : (n : Nat) -> (d : Nat) -> Type where
    Fraction : (n : Nat) -> (d : Nat) -> {auto ok: GT d Z} ->
                (q : Nat) -> (r : Fin d) ->
                q * d + finToNat r = n -> FractionView n d

||| Converts Nat to the fractional view with a non-zero divisor.
export
divMod : (n, d : Nat) -> {auto ok: GT d Z} -> FractionView n d
divMod Z (S d) = Fraction Z (S d) Z FZ Refl
divMod {ok=_} (S n) (S d) =
    let Fraction {ok=ok} n (S d) q r eq = divMod n (S d) in
    case strengthen' r of
        Left eq' => Fraction {ok=ok} (S n) (S d) (S q) FZ $
            rewrite sym eq in
                rewrite trans (cong finToNat eq') finToNatLastIsBound in
                    cong S $ trans
                        (plusZeroRightNeutral (d + q * S d))
                        (plusCommutative d (q * S d))
        Right (r' ** eq') => Fraction {ok=ok} (S n) (S d) q (FS r') $
            rewrite sym $ plusSuccRightSucc (q * S d) (finToNat r') in
                cong S $ trans (sym $ cong (plus (q * S d)) eq') eq

-------------------
--- Conversions ---
-------------------

||| Total function to convert a nat to a Fin, given a proof
||| that it is less than the bound.
public export
natToFinLTE : (n : Nat) -> (0 _ : LT n m) -> Fin m
natToFinLTE Z     (LTESucc _) = FZ
natToFinLTE (S k) (LTESucc l) = FS $ natToFinLTE k l

||| Converting from a Nat to a Fin and back is the identity.
public export
natToFinToNat :
  (n : Nat)
  -> (lte : LT n m)
  -> finToNat (natToFinLTE n lte) = n
natToFinToNat 0 (LTESucc lte) = Refl
natToFinToNat (S k) (LTESucc lte) = cong S (natToFinToNat k lte)

----------------------------------------
--- Result-type changing arithmetics ---
----------------------------------------

||| Addition of `Fin`s as bounded naturals.
||| The resulting type has the smallest possible bound
||| as illustated by the relations with the `last` function.
public export
(+) : {m, n : Nat} -> Fin m -> Fin (S n) -> Fin (m + n)
(+) FZ y = coerce (cong S $ plusCommutative n (pred m)) (weakenN (pred m) y)
(+) (FS x) y = FS (x + y)

||| Multiplication of `Fin`s as bounded naturals.
||| The resulting type has the smallest possible bound
||| as illustated by the relations with the `last` function.
public export
(*) : {m, n : Nat} -> Fin (S m) -> Fin (S n) -> Fin (S (m * n))
(*) FZ _ = FZ
(*) {m = S _} (FS x) y = y + x * y

--- Properties ---

-- Relation between `+` and `*` and their counterparts on `Nat`

export
finToNatPlusHomo : {m, n : Nat} -> (x : Fin m) -> (y : Fin (S n)) ->
                   finToNat (x + y) = finToNat x + finToNat y
finToNatPlusHomo FZ _
  = finToNatQuotient $ transitive
     (coerceEq _)
     (weakenNNeutral _ _)
finToNatPlusHomo (FS x) y = cong S (finToNatPlusHomo x y)

export
finToNatMultHomo : {m, n : Nat} -> (x : Fin (S m)) -> (y : Fin (S n)) ->
                   finToNat (x * y) = finToNat x * finToNat y
finToNatMultHomo FZ _ = Refl
finToNatMultHomo {m = S _} (FS x) y = Calc $
  |~ finToNat (FS x * y)
  ~~ finToNat (y + x * y)                 ...( Refl )
  ~~ finToNat y + finToNat (x * y)        ...( finToNatPlusHomo y (x * y) )
  ~~ finToNat y + finToNat x * finToNat y ...( cong (finToNat y +) (finToNatMultHomo x y) )
  ~~ finToNat (FS x) * finToNat y         ...( Refl )

-- Relations to `Fin`'s `last`

export
plusPreservesLast : (m, n : Nat) -> Fin.last {n=m} + Fin.last {n} = Fin.last
plusPreservesLast Z     n
  = homoPointwiseIsEqual $ transitive
      (coerceEq _)
      (weakenNNeutral _ _)
plusPreservesLast (S m) n = cong FS (plusPreservesLast m n)

export
multPreservesLast : (m, n : Nat) -> Fin.last {n=m} * Fin.last {n} = Fin.last
multPreservesLast Z n = Refl
multPreservesLast (S m) n = Calc $
  |~ last + (last * last)
  ~~ last + last          ...( cong (last +) (multPreservesLast m n) )
  ~~ last                 ...( plusPreservesLast n (m * n) )

-- General addition properties

export
plusSuccRightSucc : {m, n : Nat} -> (left : Fin m) -> (right : Fin (S n)) ->
                    FS (left + right) ~~~ left + FS right
plusSuccRightSucc FZ        right = FS $ congCoerce reflexive
plusSuccRightSucc (FS left) right = FS $ plusSuccRightSucc left right

-- Relations to `Fin`-specific `shift` and `weaken`

export
shiftAsPlus : {m, n : Nat} -> (k : Fin (S m)) ->
              shift n k ~~~ last {n} + k
shiftAsPlus {n=Z}   k =
  symmetric $ transitive (coerceEq _) (weakenNNeutral _ _)
shiftAsPlus {n=S n} k = FS (shiftAsPlus k)

export
weakenNAsPlusFZ : {m, n : Nat} -> (k : Fin n) ->
                  weakenN m k = k + the (Fin (S m)) FZ
weakenNAsPlusFZ FZ = Refl
weakenNAsPlusFZ (FS k) = cong FS (weakenNAsPlusFZ k)

export
weakenNPlusHomo : {0 m, n : Nat} -> (k : Fin p) ->
                  weakenN n (weakenN m k) ~~~ weakenN (m + n) k
weakenNPlusHomo FZ = FZ
weakenNPlusHomo (FS k) = FS (weakenNPlusHomo k)

export
weakenNOfPlus :
  {m, n : Nat} -> (k : Fin m) -> (l : Fin (S n)) ->
  weakenN w (k + l) ~~~ weakenN w k + l
weakenNOfPlus FZ l
  = transitive (congWeakenN (coerceEq _))
  $ transitive (weakenNPlusHomo l)
  $ symmetric (coerceEq _)
weakenNOfPlus (FS k) l = FS (weakenNOfPlus k l)
-- General addition properties (continued)

export
plusZeroLeftNeutral : (k : Fin (S n)) -> FZ + k ~~~ k
plusZeroLeftNeutral k = transitive (coerceEq _) (weakenNNeutral _ k)

export
congPlusLeft : {m, n, p : Nat} -> {k : Fin m} -> {l : Fin n} ->
               (c : Fin (S p)) -> k ~~~ l -> k + c ~~~ l + c
congPlusLeft c FZ
  = transitive (plusZeroLeftNeutral c)
               (symmetric $ plusZeroLeftNeutral c)
congPlusLeft c (FS prf) = FS (congPlusLeft c prf)

export
plusZeroRightNeutral : (k : Fin m) -> k + FZ ~~~ k
plusZeroRightNeutral FZ = FZ
plusZeroRightNeutral (FS k) = FS (plusZeroRightNeutral k)

export
congPlusRight : {m, n, p : Nat} -> {k : Fin (S n)} -> {l : Fin (S p)} ->
                (c : Fin m) -> k ~~~ l -> c + k ~~~ c + l
congPlusRight c FZ
  = transitive (plusZeroRightNeutral c)
               (symmetric $ plusZeroRightNeutral c)
congPlusRight {n = S _} {p = S _} c (FS prf)
  = transitive (symmetric $ plusSuccRightSucc c _)
  $ transitive (FS $ congPlusRight c prf)
               (plusSuccRightSucc c _)
congPlusRight {p = Z} c (FS prf) impossible

export
plusCommutative : {m, n : Nat} -> (left : Fin (S m)) -> (right : Fin (S n)) ->
                  left + right ~~~ right + left
plusCommutative FZ        right
  = transitive (plusZeroLeftNeutral right)
               (symmetric $ plusZeroRightNeutral right)
plusCommutative {m = S _} (FS left) right
  = transitive (FS (plusCommutative left right))
               (plusSuccRightSucc right left)

export
plusAssociative :
  {m, n, p : Nat} ->
  (left : Fin m) -> (centre : Fin (S n)) -> (right : Fin (S p)) ->
  left + (centre + right) ~~~ (left + centre) + right
plusAssociative FZ centre right
  = transitive (plusZeroLeftNeutral (centre + right))
               (congPlusLeft right (symmetric $ plusZeroLeftNeutral centre))
plusAssociative (FS left) centre right = FS (plusAssociative left centre right)

-------------------------------------------------
--- Splitting operations and their properties ---
-------------------------------------------------

||| Converts `Fin`s that are used as indexes of parts to an index of a sum.
|||
||| For example, if you have a `Vect` that is a concatenation of two `Vect`s and
||| you have an index either in the first or the second of the original `Vect`s,
||| using this function you can get an index in the concatenated one.
public export
indexSum : {m : Nat} -> Either (Fin m) (Fin n) -> Fin (m + n)
indexSum (Left  l) = weakenN n l
indexSum (Right r) = shift m r

||| Extracts an index of the first or the second part from the index of a sum.
|||
||| For example, if you have a `Vect` that is a concatenation of the `Vect`s and
||| you have an index of this `Vect`, you have get an index of either left or right
||| original `Vect` using this function.
public export
splitSum : {m : Nat} -> Fin (m + n) -> Either (Fin m) (Fin n)
splitSum {m=Z}   k      = Right k
splitSum {m=S m} FZ     = Left FZ
splitSum {m=S m} (FS k) = mapFst FS $ splitSum k

||| Calculates the index of a square matrix of size `a * b` by indices of each side.
public export
indexProd : {n : Nat} -> Fin m -> Fin n -> Fin (m * n)
indexProd FZ     = weakenN $ mult (pred m) n
indexProd (FS k) = shift n . indexProd k

||| Splits the index of a square matrix of size `a * b` to indices of each side.
public export
splitProd : {m, n : Nat} -> Fin (m * n) -> (Fin m, Fin n)
splitProd {m=S _} p = case splitSum p of
  Left  k => (FZ, k)
  Right l => mapFst FS $ splitProd l

--- Properties ---

export
indexSumPreservesLast :
  (m, n : Nat) -> indexSum {m} (Right $ Fin.last {n}) ~~~ Fin.last {n=m+n}
indexSumPreservesLast Z     n = reflexive
indexSumPreservesLast (S m) n = FS (shiftLastIsLast m)

export
indexProdPreservesLast : (m, n : Nat) ->
         indexProd (Fin.last {n=m}) (Fin.last {n}) = Fin.last
indexProdPreservesLast Z n = homoPointwiseIsEqual
  $ transitive (weakenNZeroIdentity last)
               (congLast (sym $ plusZeroRightNeutral n))
indexProdPreservesLast (S m) n = Calc $
  |~ indexProd (last {n=S m}) (last {n})
  ~~ FS (shift n (indexProd last last)) ...( Refl )
  ~~ FS (shift n last)                  ...( cong (FS . shift n) (indexProdPreservesLast m n ) )
  ~~ last                               ...( homoPointwiseIsEqual prf )

  where

    prf : shift (S n) (Fin.last {n = n + m * S n}) ~~~ Fin.last {n = n + S (n + m * S n)}
    prf = transitive (shiftLastIsLast (S n))
                     (congLast (plusSuccRightSucc n (n + m * S n)))

export
splitSumOfWeakenN : (k : Fin m) -> splitSum {m} {n} (weakenN n k) = Left k
splitSumOfWeakenN FZ = Refl
splitSumOfWeakenN (FS k) = cong (mapFst FS) $ splitSumOfWeakenN k

export
splitSumOfShift : {m : Nat} -> (k : Fin n) -> splitSum {m} {n} (shift m k) = Right k
splitSumOfShift {m=Z}   k = Refl
splitSumOfShift {m=S m} k = cong (mapFst FS) $ splitSumOfShift k

export
splitOfIndexSumInverse : {m : Nat} -> (e : Either (Fin m) (Fin n)) -> splitSum (indexSum e) = e
splitOfIndexSumInverse (Left l) = splitSumOfWeakenN l
splitOfIndexSumInverse (Right r) = splitSumOfShift r

export
indexOfSplitSumInverse : {m, n : Nat} -> (f : Fin (m + n)) -> indexSum (splitSum {m} {n} f) = f
indexOfSplitSumInverse {m=Z}   f  = Refl
indexOfSplitSumInverse {m=S _} FZ = Refl
indexOfSplitSumInverse {m=S _} (FS f) with (indexOfSplitSumInverse f)
  indexOfSplitSumInverse {m=S _} (FS f) | eq with (splitSum f)
    indexOfSplitSumInverse {m=S _} (FS _) | eq | Left  _ = cong FS eq
    indexOfSplitSumInverse {m=S _} (FS _) | eq | Right _ = cong FS eq

export
splitOfIndexProdInverse : {m : Nat} -> (k : Fin m) -> (l : Fin n) ->
                          splitProd (indexProd k l) = (k, l)
splitOfIndexProdInverse FZ     l
   = rewrite splitSumOfWeakenN {n = mult (pred m) n} l in Refl
splitOfIndexProdInverse (FS k) l
   = rewrite splitSumOfShift {m=n} $ indexProd k l in
     cong (mapFst FS) $ splitOfIndexProdInverse k l

export
indexOfSplitProdInverse : {m, n : Nat} -> (f : Fin (m * n)) ->
                          uncurry (indexProd {m} {n}) (splitProd {m} {n} f) = f
indexOfSplitProdInverse {m = S _} f with (@@ splitSum f)
  indexOfSplitProdInverse {m = S _} f | (Left l ** eq) = rewrite eq in Calc $
    |~ indexSum (Left l)
    ~~ indexSum (splitSum f) ...( cong indexSum (sym eq) )
    ~~ f                     ...( indexOfSplitSumInverse f )
  indexOfSplitProdInverse f | (Right r ** eq) with (@@ splitProd r)
    indexOfSplitProdInverse f | (Right r ** eq) | ((p, q) ** eq2)
      = rewrite eq in rewrite eq2 in Calc $
        |~ indexProd (FS p) q
        ~~ shift n (indexProd p q)                   ...( Refl )
        ~~ shift n (uncurry indexProd (splitProd r)) ...( cong (shift n . uncurry indexProd) (sym eq2) )
        ~~ shift n r                                 ...( cong (shift n) (indexOfSplitProdInverse r) )
        ~~ indexSum (splitSum f)                     ...( sym (cong indexSum eq) )
        ~~ f                                         ...( indexOfSplitSumInverse f )


text:
module Test.Chapter7

import Test
import Exercises.Chapter7

%access public export

partial
testFunctorExpr1 : IO ()
testFunctorExpr1 =
 assertEq (map (*2) (the (Expr _) (1 + 2 * 3)))
          (Add (Val 2) (Mul (Val 4) (Val 6)))

-- testFunctorExpr2 :
--   map show (the (Expr _) (1 + 2 * 3)) = Add (Val "1") (Mul (Val "2") (Val "3"))


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

-- check that all functions are total
%default total

--
-- Expressions
--
data Expr num = Val num
              | Add (Expr num) (Expr num)
              | Sub (Expr num) (Expr num)
              | Mul (Expr num) (Expr num)
              | Div (Expr num) (Expr num)
              | Abs (Expr num)

eval : (Neg num, Integral num, Abs num) => Expr num -> num
eval (Val x) = x
eval (Add x y) = eval x + eval y
eval (Sub x y) = eval x - eval y
eval (Mul x y) = eval x * eval y
eval (Div x y) = eval x `div` eval y
eval (Abs x) = abs (eval x)

Num num => Num (Expr num) where
  (+) = Add
  (*) = Mul
  fromInteger = Val . fromInteger

Neg num => Neg (Expr num) where
  negate x = 0 - x
  (-) = Sub

Abs num => Abs (Expr num) where
  abs = Abs

showHelper : Show a => String -> a -> a -> String
showHelper op x y = "(" ++ show x ++ op ++ show y ++ ")"

Show num => Show (Expr num) where
  show (Val x) = show x
  show (Add x y) = showHelper " + " x y
  show (Sub x y) = showHelper " - " x y
  show (Mul x y) = showHelper " * " x y
  show (Div x y) = showHelper " `div`" x y
  show (Abs x) = "(" ++ "abs " ++ show x ++ ")"

(Neg num, Integral num, Abs num, Eq num) => Eq (Expr num) where
  (==) x y = (eval x) == (eval y)

(Neg num, Integral num, Abs num) => Cast (Expr num) num where
  cast orig = eval orig

Functor Expr where
  map func (Val x) = Val $ func x
  map func (Add x y) = Add (map func x) (map func y)
  map func (Sub x y) = Sub (map func x) (map func y)
  map func (Mul x y) = Mul (map func x) (map func y)
  map func (Div x y) = Div (map func x) (map func y)
  map func (Abs x) = Abs $ map func x

max_stars_repo_name: pascalpoizat/idris-book

max_issues_repo_name: pascalpoizat/idris-book

max_forks_repo_name: pascalpoizat/idris-book


text:
module Data.Vect.Elem

import Data.Vect
import Decidable.Equality

--------------------------------------------------------------------------------
-- Vector membership proof
--------------------------------------------------------------------------------

||| A proof that some element is found in a vector
public export
data Elem : a -> Vect k a -> Type where
  Here : Elem x (x::xs)
  There : (later : Elem x xs) -> Elem x (y::xs)

export
Uninhabited (Elem x []) where
  uninhabited Here impossible

||| An item not in the head and not in the tail is not in the Vect at all
export
neitherHereNorThere : Not (x = y) -> Not (Elem x xs) -> Not (Elem x (y :: xs))
neitherHereNorThere xneqy xninxs  Here         = xneqy Refl
neitherHereNorThere xneqy xninxs (There xinxs) = xninxs xinxs

||| A decision procedure for Elem
public export
isElem : DecEq a => (x : a) -> (xs : Vect n a) -> Dec (Elem x xs)
isElem x [] = No uninhabited
isElem x (y::xs) with (decEq x y)
  isElem x (x::xs) | (Yes Refl) = Yes Here
  isElem x (y::xs) | (No xneqy) with (isElem x xs)
    isElem x (y::xs) | (No xneqy) | (Yes xinxs) = Yes (There xinxs)
    isElem x (y::xs) | (No xneqy) | (No xninxs) = No (neitherHereNorThere xneqy xninxs)

public export
replaceElem : (xs : Vect k t) -> (1 _ : Elem x xs) -> (y : t) -> (ys : Vect k t ** Elem y ys)
replaceElem (x::xs) Here y = (y :: xs ** Here)
replaceElem (x::xs) (There xinxs) y with (replaceElem xs xinxs y)
  replaceElem (x::xs) (There xinxs) y | (ys ** yinys) = (x :: ys ** There yinys)

public export
replaceByElem : (xs : Vect k t) -> (1 _ : Elem x xs) -> t -> Vect k t
replaceByElem (x::xs)  Here         y = y :: xs
replaceByElem (x::xs) (There xinxs) y = x :: replaceByElem xs xinxs y

public export
mapElem : {0 xs : Vect k t} -> {0 f : t -> u} ->
          (1 _ : Elem x xs) -> Elem (f x) (map f xs)
mapElem  Here     = Here
mapElem (There e) = There (mapElem e)

||| Remove the element at the given position.
|||
||| @xs The vector to be removed from
||| @p A proof that the element to be removed is in the vector
public export
dropElem : {k : _} -> (xs : Vect (S k) t) -> (1 _ : Elem x xs) -> Vect k t
dropElem           (x::ys)  Here         = ys
dropElem {k = S k} (x::ys) (There later) = x :: dropElem ys later

||| Erase the indices, returning the bounded numeric position of the element
public export
elemToFin : {0 xs : Vect n a} -> (1 _ : Elem x xs) -> Fin n
elemToFin  Here     = FZ
elemToFin (There p) = FS (elemToFin p)

||| Find the element with a proof at a given bounded position
public export
indexElem : (1 _ : Fin n) -> (xs : Vect n a) -> (x ** Elem x xs)
indexElem  FZ    (y::_)  = (y ** Here)
indexElem (FS n) (_::ys) = let (x ** p) = indexElem n ys in
                           (x ** There p)


text:
module Command

import Collie
import Collie.Options.Domain
import Data.List1

import Data.Version

orError : (err : String) -> Maybe a -> Either String a
orError err = maybe (Left err) Right

public export
version : Arguments
version = MkArguments True (Some Version) (orError "Expected a semantic version argument." . parseVersion)

public export
idv : Command "idv"
idv = MkCommand
  { description = """
                  An Idris 2 version manager. Facilitates simultaneous installation of multiple \
                  Idris 2 versions.
                  """
  , subcommands =
     [ "--help"    ::= basic "Print this help text." none
     , "list"      ::= basic "List all installed and available Idris 2 versions." none
     , "install"   ::= installCommand
     , "uninstall" ::= uninstallCommand
     , "select"    ::= selectCommand
     ]
  , modifiers = []
  , arguments = none
  }
  where
    installCommand : Command "install"
    installCommand = MkCommand
      { name = "install"
      , description = "<version> Install the given Idris 2 version and optionally also install the Idris 2 API."
      , subcommands = []
      , modifiers = [
            "--api" ::= (flag $ """
                                Install the Idris 2 API package after installing Idris 2.
                                If the specified version of Idris 2 is already installed, \
                                the API package will be added under the specified installation.
                                """)
          , "--lsp" ::= (flag $ """
                                Install the Idris 2 LSP after installing Idris 2.
                                If the specified version of Idris 2 is already installed, \
                                the LSP server will be added under the specified installation.
                                """)
          ]
      , arguments = version
      }

    uninstallCommand : Command "uninstall"
    uninstallCommand = MkCommand
      { name = "uninstall"
      , description = "<version> Uninstall the given Idris 2 version."
      , subcommands = []
      , modifiers = []
      , arguments = version
      }

    selectCommand : Command "select"
    selectCommand = MkCommand
      { name = "select"
      , description = "<version> Select the given (already installed) version of Idris 2."
      , subcommands =
        [ "system" ::= basic "Select the system install of Idris 2 (generally ~/.idris2/bin/idris2)." none ]
      , modifiers = []
      , arguments = version
      }

public export
(.handleWith) : {nm : String} -> (cmd : Command nm) -> (cmd ~~> IO a) -> IO a
cmd .handleWith h
  = do Right args <- cmd.parseArgs
         | Left err => do putStrLn err
                          putStrLn ""
                          putStrLn (cmd .usage)
                          putStrLn ""
                          exitFailure
       let Pure args = finalising args
         | Fail err => do putStrLn (show err)
                          exitFailure
       handle args h

max_stars_repo_name: memoryruins/idv

max_issues_repo_name: memoryruins/idv

max_forks_repo_name: memoryruins/idv


text:
||| Algebra: The interface to the modules of 'algebra': a representation of
||| several basic algebraic structures (e.g., groups, rings, vector spaces) as
||| Idris datatypes (axioms fully enforced).
|||
||| Mathematically, the idea of an algebraic structure is quite simple. Consider
||| (a) the set of integers \\(\mathbb{Z}\\), (b) two of the most basic
||| functions on it, \\(+: \mathbb{Z}^2 \to \mathbb{Z} \\) and
||| \\(\cdot: \mathbb{Z}^2 \to \mathbb{Z}\\), and (c) two unique elements of it,
||| \\(0\\) and \\(1\\). There are various obvious properties that universally
||| hold; e.g.:
|||
||| * \\(x+(y+z) = (x+y)+z\\), and \\(x\cdot (y\cdot z) = (x\cdot y) \cdot z\\)
||| * \\(x+y= y+x\\), and \\(x\cdot y = y \cdot x\\)
||| * \\(x+0 = x \cdot 1 = x \\)
||| * \\(\exists~y\in \mathbb{Z} [ x+y = 0 ]\\)
||| * \\(x \cdot (y+z) = x \cdot y + x \cdot z\\)
|||
||| (Unquantified variables are implicitly quantified over the domain of
||| discourse, \\(\mathbb{Z}\\).) These properties are referred to,
||| respectively, as **associativity**, **commutativity**, **identities**,
||| **additive inverses**, and **dsitributivity of (multiplication over
||| addition)**. There are various things to note. Plenty of other sets satisfy
||| these laws; for example, the rational numbers, or the real numbers, or the
||| complex numbers. Note also that, say, the irrational numbers do *not*
||| satisfy these properties; \\(pi + (1-\pi)\\) is rational, and so \\(+\\)
||| isn't even a binary function over the irrationals! Finally, note the
||| asymmetry in the fourth law, an asymmetry not present in the others. This is
||| necessary, as the following property (referred to as **multiplicative
||| inverses**) does *not* hold:
|||
||| * \\(\exists y \in \mathbb{Z} [ x \cdot y = 1 ]\\)
|||
||| While \\(2\\), for example, *does* have a multiplicative inverse among the
||| *rationals*, it doesn't when we restrict our attention to the integers. (In
||| fact, not even the rational numbers satisfy the above law, because \\(0\\)
||| does not have a multiplicative inverse. After modifying the law to account
||| for that special case, however, the rationals do satisfy it, while the
||| integers still don't.)
|||
||| So, was the point of all this? All we did was consider some numbers that
||| everyone is familiar with and mention some elementary properties of them.
||| How does that lead to any interesting mathematical questions? Well, the key
||| idea, the crucial motivating question of abstract algebra, is the following:
|||
||| __*What happens when we go in the other direction?*__
|||
||| That is, what happens when we *start* with a list of properties, then ask
||| what sorts of things satisfy it? The answers to this question are more
||| diverse than you may expect. For example, in addition to the integers and
||| its extensions, other more esoteric sets satisfy the above laws. E.g., the
||| set of integers modulo five, \\(\mathbb{Z}\_5 = \left\\{\overline{0},
||| \overline{1}, \overline{2}, \overline{3}, \overline{4}\right\\}\\). In the
||| set, to calculate the \"sum\" of two elements, we calculate their usual sum,
||| then take that modulo 5 (that is, the remainder when dividing by 5; the
||| modulo operation is essentially a generalization of the concept of even and
||| odd numbers to divisibilities other than by 2); similarly with the product.
||| Thus, for example, \\(\overline{4} + \overline{3} = \overline{2}\\). A
||| similar line of reasoning indicates that additive inverses exist\-\-\-in
||| fact, so do multiplicative inverses, at least for non-\\(0\\) elements!
||| Observe:
|||
||| * \\(\overline{1} \cdot \overline{1} = \overline{1}\\)
||| * \\(\overline{2} \cdot \overline{3} = \overline{1}\\)
||| * \\(\overline{3} \cdot \overline{2} = \overline{1}\\)
||| * \\(\overline{4} \cdot \overline{4} = \overline{1}\\)
|||
||| However, if we look at the integers modulo 6 (\\(\mathbb{Z}\_6\\)), we find
||| that multiplicative inverses do *not* always exist; only \\(\overline{1}\\)
||| and \\(\overline\{\-1} = \overline{5}\\) are invertible. (Try it!) In fact,
||| the integers modulo n, \\(\mathbb{Z}\_n\\), satisfy the weakened (i.e.,
||| ignoring \\(0\\)) multiplicative inverse law if and only if \\(n\\) is
||| prime.
|||
||| These do not exhaust the possibilities\-\-\-not even close!\-\-\-but it should
||| be enough to give a taste of what abstract algebra is all about. You start
||| with some set with defined operations (a pairing known as a \"structure\")
||| that you are familiar with, you distill that structure down to its most
||| basic and fundamental properties, and then you look at what sorts of things
||| satisfy those properties and what those properties alone entail. This allows
||| you to generalize familiar structures to more abstract ideas\-\-\-the
||| original motivating structure becomes just a special case of a more general
||| property, and seemingly disparate things suddenly become two special cases
||| of a more general idea.
|||
||| Note that in the process of generalization, we choose to \"forget\" any
||| auxiliary properties of the motivating structure. That is, the set of
||| objects, the binary functions \\(+\\) and \\(\cdot\\), and the privilleged
||| elements \\(0\\) and \\(1\\), are not necessarily numbers, addition,
||| multiplication, zero, or one (respectively)! They can be any mathematical
||| object (that is, any concept that can be precisely defined) satisfying the
||| list of properties above. In other words, they are *like* numbers with
||| respect to the most basic qualities of them, but they may in fact be
||| completely different!
|||
||| Thus, using the axioms as a starting point, one can ask which properties are
||| entailed by them, and which properties will differ between different
||| implementations of the axioms. What are the necessary and sufficient
||| conditions for various additional facts? E.g., does it follow from the laws
||| above that every element has a unique factorization? Among the motivating
||| structure of the integers this was true (a fact known as the Fundamental
||| Theorem of Arithmetic); in general, though, it is false! The question then
||| becomes how to further classify the space of implementations\-\-\-what's the
||| simplest way to divide those that do always admit a unique factorization and
||| those that don't? These are the kinds of questions that the framework of
||| algebraic structures allows you to ask.
|||
||| The laws given above define a ring; that is, any set (with the two defined
||| binary operations over it, as well as the two distinguished elements (which
||| can be thought of as nullary operations for uniformity)) satisfying the
||| above list of properties is known as a __ring__. The laws are called the
||| __ring axioms__. __Ring theory__ is the branch of math studying rings, how
||| they relate to each other (namely, via __ring homomorphisms__), and how they
||| relate to other mathematical objects. Rings are not the only algebraic
||| structure; there are many, many more, and this package defines a few of the
||| more important ones as Idris records, as well as some members of that type.
||| Each module contains in its documentation an overview of that algebraic
||| structure and some interesting properties of them that make them worth
||| studying.
|||
||| To create a term of an algebraic structure's type, one must not only provide
||| the sets and operations with the proper signatures, but also provide proofs
||| of the axioms of that algebraic structure. To see how this works, you might
||| want to take a look at `Algebra.Group`.
module Algebra

import Algebra.Magma

%default total

||| If one attempts to define both the Question and the Answer, the project will
||| fail to typecheck.
export
Answer : Integer
Answer = 42

max_stars_repo_name: greatBigDot/algebra

max_issues_repo_name: greatBigDot/algebra

max_forks_repo_name: greatBigDot/algebra


text:
module Common.Memory
import Common

export
data CairoPtr : Type -> Type where [external]

export
data Memory : Type where [external]

%foreign
    "apStable:True"
    "untupled:(_,_)"
    "imports:starkware.cairo.common.alloc alloc"
    """
    code:
    func Common_Memory_createMemoryPrim(world) -> (world, res):
        let (mem) = alloc()
        return (world, cast(mem,felt))
    end
    """
createMemoryPrim : PrimCairo (CairoPtr Memory)

public export %inline
createMemory : Cairo (CairoPtr Memory)
createMemory = fromPrimCairo createMemoryPrim

%foreign
    "apStable:True"
    """
    code:
    func Common_Memory_writeMemoryPrim(offset, value, ptr, world) -> (world):
        assert [ptr+offset] = value
        return (world)
    end
    """
writeMemoryPrim : (offset:Felt) -> (value: Felt) -> (CairoPtr Memory) -> PrimCairoUnit

public export %inline
writeMemory : Felt -> Felt -> (CairoPtr Memory) -> Cairo ()
writeMemory offset value ptr = fromPrimCairoUnit $ writeMemoryPrim offset value ptr

%foreign
    "apStable:True"
    "untupled:(_,_)"
    """
    code:
    func Common_Memory_readMemoryPrim(offset, ptr, world) -> (world,res):
        let res = [ptr+offset]
        return (world, res)
    end
    """
readMemoryPrim : (offset:Felt) -> (CairoPtr Memory) -> PrimCairo Felt

public export  %inline
readMemory : Felt -> (CairoPtr Memory) -> Cairo Felt
readMemory offset ptr = fromPrimCairo $ readMemoryPrim offset ptr

max_stars_repo_name: skyro-compiler/skyro

max_issues_repo_name: skyro-compiler/skyro

max_forks_repo_name: skyro-compiler/skyro


text:
interface NumMod where
    number : Bool -> Int

implementation [Five] NumMod where
    number b = 5

foo : NumMod => Int
foo = number True + number False

Increment : Int -> NumMod -> NumMod
Increment inc x = AddOne
   where
     foo : NumMod
     foo = x

     implementation [AddOne] NumMod where
       number x = if x then number@{foo} x + inc else inc

using implementation Five
  main : IO ()
  main = do printLn foo
            printLn (foo @{Increment 2 Five})

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:
import Control.Monad.State

increase : Nat -> State Nat ()
increase inc =
    do
        current <- get
        put (current + inc)

update : (stateType -> stateType) -> State stateType ()
update f =
    do
        state <- get
        put (f state)

increase' : Nat -> State Nat ()
increase' inc = update (+inc)


text:
module Main

main : IO ()
main = printLn "Hello Elixir"


text:
module Main

import ContriverText.Tests

main : JS_IO ()
main = do
  appMain {f=FFI_JS}
  runJsTests

max_stars_repo_name: rocketnia/contrivertext

max_issues_repo_name: rocketnia/contrivertext

max_forks_repo_name: rocketnia/contrivertext


text:
module Algebra.Semiring

%default total

infixl 8 |+|
infixl 9 |*|

||| A Semiring has two binary operations and an identity for each
public export
interface Semiring a where
  (|+|) : a -> a -> a
  plusNeutral : a
  (|*|) : a -> a -> a
  timesNeutral : a

||| Erased linearity corresponds to the neutral for |+|
public export
erased : Semiring a => a
erased = plusNeutral

||| Purely linear corresponds to the neutral for |*|
public export
linear : Semiring a => a
linear = timesNeutral

||| A semiring eliminator
public export
elimSemi : (Semiring a, Eq a) => (zero : b) -> (one : b) -> (a -> b) -> a -> b
elimSemi zero one other r {a} =
  if r == Semiring.plusNeutral {a}
     then zero
     else if r == Semiring.timesNeutral {a}
             then one
             else other r

export
isErased : (Semiring a, Eq a) => a -> Bool
isErased = elimSemi True False (const False)

export
isLinear : (Semiring a, Eq a) => a -> Bool
isLinear = elimSemi False True (const False)

export
isRigOther : (Semiring a, Eq a) => a -> Bool
isRigOther = elimSemi False False (const True)

export
branchZero : (Semiring a, Eq a) => Lazy b -> Lazy b -> a -> b
branchZero yes no rig = if isErased rig then yes else no

export
branchOne : (Semiring a, Eq a) => Lazy b -> Lazy b -> a -> b
branchOne yes no rig = if isLinear rig then yes else no

export
branchVal : (Semiring a, Eq a) => Lazy b -> Lazy b -> a -> b
branchVal yes no rig = if isRigOther rig then yes else no


text:
module Js.Node.Module

import Js

%default total
%access export

dir : JS_IO String
dir = js "__dirname" (JS_IO String)

path : JS_IO String
path = js "__filename" (JS_IO String)

max_stars_repo_name: jheiling/idris-js

max_issues_repo_name: jheiling/idris-js

max_forks_repo_name: jheiling/idris-js


text:
module Server.InigoServer.Server

import Inigo.Async.Base
import Inigo.Async.CloudFlare.Worker as Worker
import Inigo.Async.Promise
import Server.InigoServer.Handler

server : Promise ()
server =
  do
    Worker.serve handler
    never -- wait forever

export
main : IO ()
main =
  run server

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
import Control.Monad.Coop

import System.Clock

millis : HasIO io => io Integer
millis = liftIO $ composeTime <$> clockTime Monotonic where
  composeTime : Clock Monotonic -> Integer
  composeTime (MkClock secs nanos) = secs * 1000 + nanos `div` 1000000

Timed IO where
  currentTime = fromInteger <$> millis

printTime : HasIO io => (offset : Integer) -> String -> io Unit
printTime offset s = printLn $ "[time: " ++ show (!millis - offset) ++ "] " ++ s

for : Nat -> Monad m => m a -> m ()
for Z     _ = pure ()
for (S n) a = do a; for n a

export
main : IO Unit
main = do printLn "before coop"
          runCoop $ do
  offset <- millis
  printTime offset "start"
  (<||>)
    (for 5 $ do
      printTime offset "proc 1, before 1000"
      sleepFor 1000
      printTime offset "proc 1, before 2000"
      sleepFor 2000)
    (for 10 $ do
      printTime offset "                     proc 2, before 350"
      sleepFor 350
      printTime offset "                     proc 2, before 750"
      sleepFor 750)

max_stars_repo_name: buzden/idris-arduino-lib

max_issues_repo_name: buzden/idris-arduino-lib

max_forks_repo_name: buzden/idris-arduino-lib


text:
||| ported from https://github.com/pepijnkokke/FirstOrderUnificationInAgda
module Unification

import Data.Fin

%default total
%access public export

||| An identifier
data Name = MkName String

Eq Name where
  (MkName x) == (MkName y) = x == y

||| A term in an untyped lambda-calculus with variables indexed by `v`.
||| Either a variable, an identifier, or a function applied to an argument.
||| We keep track of the depth `d` to ensure terms are finite.
||| @ v the type `Var`s are indexed by
||| @ d the depth of the AST
data TermD : (v : Type) -> (d : Nat) -> Type where
  ||| A variable with index `i`
  Var : (i : v) -> TermD v Z
  ||| an identifier with name `n`
  Identifier : (n : Name) -> TermD v Z
  ||| function application, `f` applied to `x`
  App : (f : TermD v d1) -> (x : TermD v d2) -> TermD v (S (max d1 d2))

||| A TermD with `d` as a reified witness instead of a type param
data Term : (v : Type) -> Type where
  MkTerm : Exists (TermD v) -> Term v

namespace Term
  depth : Term v -> Nat
  depth (MkTerm t) = getWitness t

  {- implicit conversions to/from TermD -}
  implicit
  toTermD : (t : Term v) -> TermD v (depth t)
  toTermD (MkTerm t) = getProof t

  implicit
  fromTermD : TermD v d -> Term v
  fromTermD {d=d} t = MkTerm (Evidence d t)

  {- constructors for Term (making use of implicit conversions to/from TermD) -}
  var : v -> Term v
  var v = Var v

  identifier : {v : Type} -> Name -> Term v
  identifier c = Identifier c

  app : Term v -> Term v -> Term v
  app left right = App left right

  ||| The catamorphism for Term.
  ||| We unpack and use `d` to convince idris `fold'` is total,
  ||| so callers of `fold` can ignore `d` and not worry about totality.
  fold : (v -> r) -> (Name -> r) -> (r -> r -> r) -> Term v -> r
  fold v n f (MkTerm (Evidence d t)) = fold' v n f d t where
    fold' v n f d t = case t of
      Var i => v i
      Identifier c => n c
      App {d1=d1} {d2=d2} l r => f (fold' v n f d1 l) (fold' v n f d2 r)

Functor Term where
  map f t = fold (var . f) identifier app t

Applicative Term where
  pure = var
  mf <*> ma = fold (\f => map f ma) identifier app mf

Monad Term where
  t >>= f = fold f identifier app t

Foldable Term where
  foldr op z t = fold op (const id) (.) t z

Traversable Term where
  traverse f = fold
    (\y => [| var (f y) |])
    (\c => pure (identifier c))
    (\l, r => [| app l r |])

{- Now for some unification... -}

||| A substitution of a `Term (Fin n)` for a variable in `Fin (S n)`.
||| @ n the number of vars after applying the substitution.
data Subst : (n : Nat) -> Type where
  ||| Make a Subst
  ||| @ x the variable to replace
  ||| @ t the term (not mentioning `x`) to replace `x` with
  MkSubst : (x : Fin (S n)) -> (t : Term (Fin n)) -> Subst n

{-
  thick and thin help keep track of var indexes when vars are
  introduced or removed.
-}
||| `thick x` maps each `Fin (S n)` that is not `x` to a unique `Fin n`.
||| Useful when removing `x` from the set of vars (e.g. with a `Subst`).
||| y |-> Just y,        if y < x,
|||       Nothing,       if y = x,
|||       Just (pred y), if y > x
thick : (x, y : Fin (S n)) -> Maybe (Fin n)
thick {n=S k} FZ     (FS y) = Just y              -- y < x
thick {n=S k} (FS x) FZ     = Just FZ             -- y > x
thick {n=S k} (FS x) (FS y) = FS <$> thick x y    -- recurse
thick         _      _      = Nothing             -- y = x

||| `thin x` maps each `Fin n` to a unique `Fin (S n)` that is not `x`.
||| The inverse of `y |-> thick x y` for `y`s s.t. `y != x`.
||| Useful for undoing a `Subst`.
||| y |-> FS y, if y >= x,
|||       y,    if y < x
thin : (x : Fin (S n)) -> (y : Fin n) -> Fin (S n)
thin FZ     y      = FS y
thin x      FZ     = FZ
thin (FS x) (FS y) = FS (thin x y)

||| replaces any occurrance of a `Var y` in `t` with `r` if
||| `x == y` or `Var (thick x y)` otherwise.
||| @ s the substitution to make
||| @ t the term to search and replace in
subst : (s : Subst m) -> (t : Term (Fin (S m))) -> Term (Fin m)
subst (MkSubst x r) t = map (thick x) t >>= (maybe r var)

||| A list of substitutions, of the form
||| `[Subst m d, Subst m-1 d, Subst m-2 d, ...]`.
||| Substitutions are applied left to right.
||| Each `s` in a SubstList reduces the number of variables by one, so
||| successive substitutions operate on the reduced set of var idxs.
||| @ m the number of vars before applying the substitutions.
||| @ n the number of vars remaining after applying the substitutions.
data SubstList : (m : Nat) -> (n : Nat) -> Type where
  Nil : {n : Nat} -> SubstList n n  -- no op, number of vars is unchanged
  (::) : (s : Subst m) ->
         (tail : SubstList m n)
           -> SubstList (S m) n

||| Check that `x` doesn't appear in `t`.
||| If it does, return Nothing.
||| If it doesn't, return `t` but over a smaller set of vars.
check : (x : Fin (S n)) -> (t : Term (Fin (S n))) -> Maybe (Term (Fin n))
check x = traverse (thick x)

||| As long as the var x doesn't appear in t, we can unify x and t
||| by substituting t for x.
flexRigid : Fin n -> Term (Fin n) -> Maybe (Exists (SubstList n))
flexRigid {n=Z} _ _ = Nothing  -- impossible, Fin Z is uninhabited
flexRigid {n=S n'} x t = map (\t' => Evidence n' [MkSubst x t']) (check x t)

||| we can always unify two variables
flexFlex : (x, y : Fin n) -> Exists (SubstList n)
flexFlex {n=Z} _ _ = Evidence Z []  -- impossible, Fin Z is uninhabited
flexFlex {n=S n'} x y = case thick x y of
  Nothing => Evidence (S n') []                -- x = y, no subst needed
  Just y' => Evidence n' [MkSubst x (Var y')]  -- x != y, sub y' for x

||| helper function for unify
unify' : (t1 : TermD (Fin m) d1) ->
         (t2 : TermD (Fin m) d2) ->
         (acc : Exists (SubstList m))
           -> Maybe (Exists (SubstList m))
unify' t1 t2 (Evidence n (s :: tail)) =  -- non-empty `acc`
  map consS $ unify' (subst s t1) (subst s t2) (Evidence n tail) where
    consS (Evidence n' sl) = Evidence n' (s :: sl)
unify' (Var x1) (Var x2) _ = Just (flexFlex x1 x2)
unify' (Var x1) t2       _ = flexRigid x1 t2
unify' t1       (Var x2) _ = flexRigid x2 t1
unify' {m=m} (Identifier c1) (Identifier c2) acc =
  if c1 == c2 then Just acc else Nothing
unify' (App la ra) (App lb rb) acc =
  Just acc >>= unify' la lb >>= unify' ra rb
unify' _ _ _ = Nothing  -- can't unify identifier with function application
                        -- (in first-order unification, anyway)

||| Finds the most general substitutions of terms for variables that makes
||| the two terms equal.
unify : (t1 : Term (Fin m)) -> (t2 : Term (Fin m)) -> Maybe (Exists (SubstList m))
unify {m=m} t1 t2 = unify' t1 t2 (Evidence m [])

max_stars_repo_name: sammthomson/IdrisUnification

max_issues_repo_name: sammthomson/IdrisUnification

max_forks_repo_name: sammthomson/IdrisUnification


text:
module Exercise_5_2_11

import Ch05.LambdaCalculusWithArith

%default total

-- The implementation below is the simple (and naive) one
||| Term representing a function that, given a list of Church numerals (encoded as in ex. 5.2.8),
||| will return their sum
listsum_naive : Term
listsum_naive = lambda 0
                       (\l => l . plus . church_zero)

-- The implementation below uses the fix-point combinator
||| Term representing a function that, given a list of Church numerals (encoded as in ex. 5.2.8),
||| will return their sum
listsum : Term
listsum = fix . g where
  g : Term
  g = lambda 0
             (\f => (lambda 1
                            (\l => IfThenElse (realbool . (isnil . l))
                                              church_zero
                                              (plus . (head . l) . (f . (tail . l))))))

max_stars_repo_name: mr-infty/tapl

max_issues_repo_name: mr-infty/tapl

max_forks_repo_name: mr-infty/tapl


text:
module Commons.Config.JSON.Parser

import Data.PList

import Text.Token
import Text.Lexer
import Text.Parser

import Language.JSON.Lexer

import Commons.Config.JSON.Model
import Commons.Config.JSON.Helpers

%default total
%access private

public export
Parser : Type -> Type
Parser = Grammar JSONToken True

symbol : Punctuation -> Grammar JSONToken True ()
symbol p = match $ JTPunct p

null : Parser ParseResult
null = do
  match JTNull
  pure $ PR VALUE JNull ValidVal

number : Parser ParseResult
number = do
  res <- match JTNumber
  pure $ PR VALUE (JNum res) ValidVal

boolean : Parser ParseResult
boolean = do
  res <- match JTBoolean
  pure $ PR VALUE (JBool res) ValidVal

string' : Parser String
string' = do
  res <- match JTString
  the (Grammar _ False _) $
    case res of
      Just str => pure str
      Nothing  => fail "invalid string"

string : Parser ParseResult
string = do
  res <- match JTString
  the (Grammar _ False _) $
    case res of
      Just str => pure $ PR VALUE (JStr str) ValidVal
      Nothing  => fail "invalid string"

value : Parser ParseResult
value = null <|> string <|> number <|> boolean

mutual
  array : Parser ParseResult
  array = do
      symbol (Square Open)
      commit
      vs <- elements
      symbol (Square Close)
      pure $ PR ARRAY (toArray vs) ValidArr
    where
     elements : Parser (List ParseResult)
     elements = do
       v <- json
       vs <- option Nil $ (symbol Comma) *> sepBy (symbol Comma) json
       pure (v::vs)

  dict : Parser ParseResult
  dict = do
      symbol (Curly Open)
      commit
      kvs <- keypairs
      symbol (Curly Close)
      pure $ PR MAP (toDict kvs) ValidMap
    where
      keypair : Parser (String, ParseResult)
      keypair = do
        key <- string'
        symbol Colon
        value <- json
        pure (key, value)

      keypairs : Parser (List (String, ParseResult))
      keypairs = do
        kp <- keypair
        kps <- option Nil $ (symbol Comma) *> sepBy (symbol Comma) keypair
        pure (kp::kps)

  json : Parser ParseResult
  json = value <|> array <|> dict

export
parseJSON : List JSONToken -> Maybe (JSONDoc DOC)
parseJSON toks =
  case parse json $ filter (not . ignored) toks of
    (Left (Error x xs)) => Nothing
    (Right (a, b)) =>
      case a of
         (PR ty value prf) => Just $ JDoc ty value

max_stars_repo_name: jfdm/idris-common

max_issues_repo_name: jfdm/idris-common

max_forks_repo_name: jfdm/idris-common


text:
module Replica.Core.Types

import Data.String
import Language.JSON

%default total

public export
data OrderSensitive = Ordered | Whatever

export
Show OrderSensitive where
  show Ordered = "Ordered"
  show Whatever = "Whatever"

public export
data Expectation
   = Exact String
   | Partial OrderSensitive (List String)
   | Generated

export
Show Expectation where
  show (Exact x) = "Exact \{show x}"
  show (Partial x xs) = "Partial \{show Ordered} \{show xs}"
  show Generated = "Generated"

public export
record Test where
  constructor MkTest
  name: String
  pending : Bool
  description: Maybe String
  require : List String
  workingDir : Maybe String
  tags: List String
  beforeTest : List String
  afterTest : List String
  -- env: Map String String
  command: String
  input : Maybe String
  mustSucceed : Maybe Bool
  spaceSensitive : Bool
  expectation : Expectation
  file : Maybe String

export
Show Test where
  show x = unwords
    [ "MkTest"
    , show x.name
    , show x.pending
    , show x.description
    , show x.require
    , show x.workingDir
    , show x.tags
    , show x.beforeTest
    , show x.afterTest
    , show x.command
    , show x.input
    , show x.mustSucceed
    , show x.spaceSensitive
    , show x.expectation
    , show x.file
    ]

export
defaultExpected : String
defaultExpected = "expected"

export
defaultFile : String
defaultFile = "file"

export
defaultOutput : String
defaultOutput = "output"

export
defaultInput : String
defaultInput = "input"

public export
record Replica where
  constructor MkReplica
  tests: List Test

public export
data OutputError
  = GoldenIsMissing String
  | DifferentOutput String String
  | PartialOutputMismatch OrderSensitive (List String) String

public export
data FailReason : Type where
  WrongStatus : (expectSuccess : Bool) -> FailReason
  WrongOutput : Maybe String -> OutputError -> FailReason
  ExpectedFileNotFound : String -> FailReason

displaySource : Maybe String -> String
displaySource Nothing = "output"
displaySource (Just x) = "file \{x}"

export
displayFailReason : FailReason -> String
displayFailReason (WrongStatus True) = "[Fails while it should pass]"
displayFailReason (WrongStatus False) = "[Pass but it should fail]"
displayFailReason (WrongOutput src (GoldenIsMissing _)) = "[Missing Golden for \{displaySource src}]"
displayFailReason (WrongOutput src x) = "[Unexpected content for \{displaySource src}]"
displayFailReason (ExpectedFileNotFound src) = "[Missing expected file \"\{src}\"]"

namespace FailReason

  export
  toJSON : FailReason -> JSON
  toJSON (WrongStatus e) = JObject
    [("type", JString "status"), ("expected", JBoolean e), ("given", JBoolean $ not e)]
  toJSON (WrongOutput src (GoldenIsMissing x)) = JObject $
    maybe id ((::) . MkPair "file" . JString) src
      [("type", JString "output"), ("reason", JString "Missing"), ("given", JString x)]
  toJSON (WrongOutput src (DifferentOutput x y)) = JObject $
    maybe id ((::) . MkPair "file" . JString) src
      [("type", JString "output"), ("expected", JString x), ("given", JString y)]
  toJSON (WrongOutput src (PartialOutputMismatch o x y)) = JObject $
    maybe id ((::) . MkPair "file" . JString) src
      [ ("type", JString "output")
      , ("ordered", JBoolean $ case o of
          Ordered => True
          Whatever => False)
      , ("missingParts", JArray $ map JString x)
      , ("given", JString y)]
  toJSON (ExpectedFileNotFound src) = JObject
      [("type", JString "missing"), ("expected", JString src)]

public export
data TestResult
  = Success
  | Fail (List FailReason)
  | Skipped

namespace TestResult

  export
  toJSON : TestResult -> JSON
  toJSON Success = JString "Success"
  toJSON (Fail xs) = JObject [("Fail", JArray $ map toJSON xs)]
  toJSON Skipped = JString "Skipped"

  export
  isSuccess : TestResult -> Bool
  isSuccess Success = True
  isSuccess _ = False

public export
data TestError
  = FileSystemError String
  | InitializationFailed String
  | WrapUpFailed TestResult String
  | RequirementsFailed String
  | Inaccessible

namespace TestError

  export
  toJSON : TestError -> JSON
  toJSON (FileSystemError x) =
    JObject [("type", JString "FileSystemError") , ("content", JString x)]
  toJSON (InitializationFailed x) =
    JObject [("type", JString "InitializationFailed") , ("content", JString x)]
  toJSON (WrapUpFailed x y) =
    JObject [("type", JString "WrapUpFailed"),  ("result", toJSON x), ("content", JString y)]
  toJSON (RequirementsFailed x) =
    JObject [("type", JString "RequirementsFailed"), ("content", JString x)]
  toJSON Inaccessible =
    JObject [("type", JString "Inaccessible")]

export
displayTestError : TestError -> String
displayTestError (FileSystemError x) = "File error: \{x}"
displayTestError (InitializationFailed x) = "Before test action failed: \{x}"
displayTestError (WrapUpFailed x y) =  "After test action failed: \{y}"
displayTestError (RequirementsFailed x) = "Test rely on test \{x}, which failed"
displayTestError Inaccessible = "Test rely on other tests that weren't run"

export
isFullSuccess : Either TestError TestResult -> Bool
isFullSuccess (Right Success) = True
isFullSuccess _ = False

public export
record Stats where
  constructor MkStats
  successes : Nat
  failures  : Nat
  errors    : Nat
  skipped   : Nat

export
Semigroup Stats where
  (<+>) x y = MkStats
    (x.successes + y.successes)
    (x.failures + y.failures)
    (x.errors + y.errors)
    (x.skipped + y.skipped)

export
Monoid Stats where
  neutral = MkStats 0 0 0 0

export
asStats : List (Either TestError TestResult) -> Stats
asStats = foldMap go
  where
    go : Either TestError TestResult -> Stats
    go (Left x) = record {errors = 1} neutral
    go (Right Success) = record {successes = 1} neutral
    go (Right (Fail xs)) = record {failures = 1} neutral
    go (Right Skipped) = record {skipped = 1} neutral

export
countTests : Stats -> Nat
countTests x = x.successes + x.failures + x.errors + x.skipped

export
resultToJSON : Either TestError TestResult -> JSON
resultToJSON (Left x) = JObject [("Error", toJSON x)]
resultToJSON (Right x) = toJSON x

export
reportToJSON : List (String, Either TestError TestResult) -> JSON
reportToJSON = JObject . map (map resultToJSON)

max_stars_repo_name: teto/REPLica

max_issues_repo_name: teto/REPLica

max_forks_repo_name: teto/REPLica