text:
module IdrisJvm.File

import Java.Util.Stream
import Java.Lang
import Java.Math
import IdrisJvm.JvmImport
import Data.Vect
import Java.Nio
import Java.IO
import Java.Util
import Java.Util.Concurrent
import IdrisJvm.ClientServerSocket
import IdrisJvm.FileChannelIo
import IdrisJvm.Files
import IdrisJvm.System

%hide Prelude.File.File
%hide Prelude.File.FileError
%hide Prelude.File.Directory
%hide Java.IO.File.File

public export
data File = MkFileStdin
          | MkFileStdout
          | MkFileStderr
          | MkFile FileChannelIo
          | MkFileClientServerSocket ClientServerSocket

public export
Directory : Type
Directory = JDirectory

public export
FileError : Type
FileError = Throwable

export
FileReadError : FileError
FileReadError = believe_me $ unsafePerformIO $ IOException.new "File Read Error"

export
GenericFileError : Int -> FileError
GenericFileError errNo = believe_me $ unsafePerformIO $ IOException.new $ "Generic File Error " ++ show errNo

export
unableToOpenFile : String -> JVM_IO IOException
unableToOpenFile fileName = IOException.new ("Unable to open file: " ++ fileName)

export
unableToReadFile : String -> JVM_IO IOException
unableToReadFile fileName = IOException.new ("Unable to read file: " ++ fileName)

export
unableToWriteFile : String -> JVM_IO IOException
unableToWriteFile fileName = IOException.new ("Unable to write file: " ++ fileName)

modeToOpenOption : Mode -> List OpenOption
modeToOpenOption Read              = [ StandardOpenOption.read ]
modeToOpenOption WriteTruncate     = believe_me <$> [ StandardOpenOption.create, StandardOpenOption.write,
                                        StandardOpenOption.truncateExisting ]
modeToOpenOption Append            = believe_me <$> [ StandardOpenOption.append ]
modeToOpenOption ReadWrite         = believe_me <$> [ StandardOpenOption.create, StandardOpenOption.read,
                                       StandardOpenOption.write ]
modeToOpenOption ReadWriteTruncate = believe_me <$> [ StandardOpenOption.create, StandardOpenOption.read,
                                       StandardOpenOption.write, StandardOpenOption.truncateExisting ]
modeToOpenOption ReadAppend        = believe_me <$> [ StandardOpenOption.read, StandardOpenOption.append ]

export
total
openFile : (f : String) -> (m : Mode) -> JVM_IO (Either FileError File)
openFile f m = assert_total $ do
      path <- Files.createPath f
      ensureParentDir path
      openOptions <- listToArray (modeToOpenOption m)
      exceptionOrFile <- FileChannelIo.open path openOptions
      case exceptionOrFile of
        Left exception => pure $ Left $ believe_me exception
        Right file => pure $ Right (MkFile file)
   where
     hasWriteMode : Bool
     hasWriteMode = case m of
        WriteTruncate => True
        ReadWrite => True
        ReadWriteTruncate => True
        _ => False

     ensureParentDir : Path -> JVM_IO ()
     ensureParentDir path =
       if hasWriteMode then do
         optParent <- nullableToMaybe <$> invokeInstance "getParent" (Path -> JVM_IO Path) path
         case optParent of
            Nothing => pure ()
            Just pathDir => do
              Files.createDirectories pathDir
              pure ()
       else pure ()

export
getChar : File -> JVM_IO Char
getChar (MkFile fileChannelIo) = getChar fileChannelIo
getChar (MkFileClientServerSocket clientServerSocket) = getChar clientServerSocket
getChar MkFileStdin = IO.getChar
getChar _ = do
    putStrLn "Unable to read a character"
    exit 1

export
getLine : File -> JVM_IO String
getLine (MkFile fileChannelIo) = getLine fileChannelIo
getLine (MkFileClientServerSocket clientServerSocket) = ClientServerSocket.getLine clientServerSocket
getLine MkFileStdin = IO.getLine
getLine _ = do
    putStrLn "Unable to read a line"
    exit 1

export
writeString : File -> String -> JVM_IO ()
writeString (MkFile fileChannelIo) str = writeString fileChannelIo str
writeString (MkFileClientServerSocket socket) str = writeString socket str
writeString MkFileStdout str = print str
writeString _ _ = pure ()

export
closeFile : File -> JVM_IO ()
closeFile (MkFile file) = FileChannelIo.close file
closeFile (MkFileClientServerSocket clientServerSocket) = ClientServerSocket.close clientServerSocket
closeFile _ = pure ()

export
getTemporaryFileName : JVM_IO String
getTemporaryFileName = Files.getTemporaryFileName

export
chmod : String -> Int -> JVM_IO ()
chmod = Files.chmod

-- This is returning Int to conform to Idris fileSize function type
-- even though Java's FileChannel returns long
export
fileSize : File -> JVM_IO (Either FileError Int)
fileSize (MkFile f) = do
  exceptionOrSize <- FileChannelIo.size f
  case exceptionOrSize of
    Left exception => pure $ Left $ believe_me exception
    Right size => pure $ Right $ Long.intValue size
fileSize _ = pure . Left . believe_me $ !(IOException.new "Cannot determine size")

export
fflush : File -> JVM_IO ()
fflush (MkFile file) = FileChannelIo.flush file
fflush MkFileStdout = invokeStatic RuntimeClass "flushStdout" (JVM_IO ())
fflush MkFileStderr = invokeStatic RuntimeClass "flushStderr" (JVM_IO ())
fflush _ = pure ()

||| Standard input
export
stdin : File
stdin = MkFileStdin

||| Standard output
export
stdout : File
stdout = MkFileStdout

||| Standard error
export
stderr : File
stderr = MkFileStderr

export
total
readFile : String -> JVM_IO (Either FileError String)
readFile pathStr = assert_total $ Files.readFile pathStr

export
writeFile : String -> String -> JVM_IO (Either FileError ())
writeFile file content = Files.writeFile file content

export
fileModifiedTime : File -> JVM_IO (Either FileError Integer)
fileModifiedTime (MkFile file) = FileChannelIo.getFileModifiedTime file
fileModifiedTime _ = pure . Left $ believe_me !(IOException.new "Cannot get file modified time")

export
fileAccessTime : File -> JVM_IO (Either FileError Integer)
fileAccessTime (MkFile file) = FileChannelIo.getFileAccessTime file
fileAccessTime _ = pure . Left $ believe_me !(IOException.new "Cannot get file access time")

export
fileStatusTime : File -> JVM_IO (Either FileError Integer)
fileStatusTime (MkFile file) = FileChannelIo.getFileStatusTime file
fileStatusTime _ = pure . Left $ believe_me !(IOException.new "Cannot get file status time")

||| Check if a file handle has reached the end
export
fEOF : File -> JVM_IO Bool
fEOF (MkFile file) = FileChannelIo.isEof file
fEOF MkFileStdin = invokeStatic RuntimeClass "isStdinEof" (JVM_IO Bool)
fEOF _ = pure False

export
socketListenAndAccept : String -> Int -> JVM_IO (Either String File)
socketListenAndAccept host port = do
    byteBufferIoOrError <- ClientServerSocket.listenAndAccept host port
    case byteBufferIoOrError of
        Left throwable => Left <$> Objects.toString throwable
        Right byteBufferIo => pure . Right $ MkFileClientServerSocket byteBufferIo

export
fRemove : (s : String) -> JVM_IO Bool
fRemove f = do
    path <- Files.createPath f
    deleteIfExists path

||| Read a line from a file
||| @h a file handle which must be open for reading
export
fGetLine : (h : File) -> JVM_IO (Either FileError String)
fGetLine file = do
  str <- getLine file
  pure $ Right str

||| Read up to a number of characters from a file
||| @h a file handle which must be open for reading
export
fGetChars : (h : File) -> (len : Int) -> JVM_IO (Either FileError String)
fGetChars file len = (Right . pack . reverse) <$> go [] len where
    go : List Char -> Int -> JVM_IO (List Char)
    go acc 0 = pure acc
    go acc n = do
        c <- getChar file
        go (c :: acc) (n - 1)

||| Write a line to a file
||| @h a file handle which must be open for writing
||| @str the line to write to the file
export
fPutStr : (h : File) -> (str : String) -> JVM_IO (Either FileError ())
fPutStr file s = Right <$> writeString file s

export
dirOpen : (d : String) -> JVM_IO (Either FileError Directory)
dirOpen d = Files.openDirectory d

export
dirClose : Directory -> JVM_IO ()
dirClose dir = Files.closeDirectory dir

-- This function is retained for compatibility with other backends as it is part of Idris prelude. It doesn't have
-- much usage in JVM backend as the errors involving directory operations can be directly retrieved from exceptions
-- so the directory object itself doesn't contain the errors.
export
dirError : Directory -> JVM_IO Bool
dirError dir = pure False

export
dirEntry : Directory -> JVM_IO (Either FileError String)
dirEntry dir = Files.nextDirectoryEntry dir

export
total
createDir : String -> JVM_IO (Either FileError ())
createDir d = assert_total $ Files.createDirectory d

export
changeDir : String -> JVM_IO Bool
changeDir = Files.changeDir

export
currentDir : JVM_IO String
currentDir = Files.getWorkingDir


text:
module Bautzen

import Bautzen.Options
import Bautzen.REPL
import Bautzen.Server
import Bautzen.Client
import System

partial
main : IO ()
main = do
  (_ :: args) <- getArgs
  case processOptions args of
    Left err => putStrLn err
    Right options@(MkOptions _ _ ServerMode) => do
      Right () <- server options
        | Left err => putStrLn err
      pure ()
    Right options@(MkOptions _ _ ClientMode) => do
      Right () <- client options
        | Left err => putStrLn err
      pure ()

ext: idr

max_stars_repo_name: steshaw/hsgames

max_issues_repo_name: steshaw/hsgames

max_forks_repo_name: steshaw/hsgames


text:
bools : List Bool
bools = [True, False]

main : IO ()
main = printLn $ or (map id bools)

main2 : IO ()
main2 = printLn $ or (map (\x => x) bools)

main3 : IO ()
main3 = printLn $ or (map (\x => Delay x) bools)

main4 : IO ()
main4 = printLn $ or bools


text:
module Average

export
avg_word_length : String -> Double
avg_word_length sentence = let lettersTotal = lettersCount sentence
                               wordsNr = wordsCount sentence
                           in cast lettersTotal / cast wordsNr
where
	wordsCount : String -> Nat
	wordsCount str = length (words str)

	lettersCount : String -> Nat
	lettersCount str = sum (map length (words str))


text:
module Data.SnocVect.Elem

import Data.SnocVect
import Decidable.Equality

%default total

public export
data Elem : SnocVect k a -> a -> Type where
  Here  : Elem (sx :< x) x
  There : Elem sx x -> Elem (sx :< y) x

export
{sx : SnocVect 0 a} -> Uninhabited (Elem sx x) where
  uninhabited Here impossible
  uninhabited (There x) impossible

neitherHereNorThere : DecEq a => {0 x,y : a} ->
                      Not (x = y) ->
                      Not (Elem sy x) ->
                      Not (Elem (sy :< y) x)
neitherHereNorThere Refl _ Here impossible
neitherHereNorThere _ g (There z) = g z

export
isElem : DecEq a => (x : a) -> (sx : SnocVect k a) -> Dec (Elem sx x)
isElem x [<] = No absurd
isElem x (sx :< y) with (decEq x y)
  isElem y (sx :< y) | (Yes Refl) = Yes Here
  isElem x (sx :< y) | (No contra) with (isElem x sx)
    isElem x (sx :< y) | (No _) | (Yes prf) = Yes (There prf)
    isElem x (sx :< y) | (No yNotX) | (No xNotInSx) =
      No (neitherHereNorThere yNotX xNotInSx)

max_stars_repo_name: mattpolzin/idris-snocvect

max_issues_repo_name: mattpolzin/idris-snocvect

max_forks_repo_name: mattpolzin/idris-snocvect


text:
module Scheme.Parse

import Data.List
import Data.Vect
import Data.String

import Scheme.DParser
import Scheme.Core

%hide Data.Vect.Here
%hide Data.Vect.There

%default total
%access public export

spaces : Parser ()
spaces = skipSome $ char ' '

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

escapedBackslashOrDoubleQuote : Parser (NonEmptyList Char)
escapedBackslashOrDoubleQuote = do
  char '\\'
  x <- oneOf $ unpack "\\\""
  pure $ MkNEList ([x] ** IsNonEmpty)

parseChar : Parser SExp
parseChar = do
  char '#'
  char '\\'
  name <- exactly (oneOf (unpack ".,;$%#\\\"'[]{}()") <|> special <|> digit) <|> some letter
  case name of
       (MkNEList (c :: [] ** _)) => pure $ SEChar c
       (MkNEList (c :: cs ** _)) => case toLower $ pack $ c :: cs of
                                         "space"   => pure $ SEChar ' '
                                         "tab"     => pure $ SEChar '\t'
                                         "newline" => pure $ SEChar '\n'
                                         _         => noParse "Can't parse character"

parseStr : Parser SExp
parseStr = do
  char '"'
  xs <- many $ escapedBackslashOrDoubleQuote <|> (some $ noneOf $ unpack "\\\"")
  char '"'
  pure $ SEStr $ pack $ concat $ map neWeaken xs

parseBool : Parser SExp
parseBool = do
  char '#'
  MkOO (_ ** prf) <- oneOf' $ unpack "tf"
  pure $ case prf of
              Here         => SEBool True
              There Here   => SEBool False
              There (There _) impossible

parseSymbol : Parser SExp
parseSymbol =
  [| (SESymbol . pack)
     [| (letter <|> special) :: (many (letter <|> digit <|> special)) |]
  |]

-- TODO exact/inexact, base modifier, numeric hierarchy
parseNum : Parser SExp
parseNum = do
  msign <- optional $ oneOf' $ unpack "+-"
  xs    <- parsePositive . pack . neWeaken <$> some digit
  case xs of
       Nothing => noParse "Can't parse number"
       Just n  => pure $ SENum $ SNExactInt $ case msign of
                                                   Nothing                => n
                                                   Just (MkOO (_ ** prf)) => case prf of
                                                                                Here         =>  n
                                                                                There Here   => -n
                                                                                There (There _) impossible

mutual
  parseExpr : Parser SExp
  parseExpr =   assert_total
            $   parseNum
            <|> parseStr
            <|> parseSymbol
            <|> parseBool
            <|> parseChar
            <|> parseShortForm "'"  "quote"
            <|> parseShortForm "`"  "quasiquote"
            <|> parseShortForm ",@" "unquote-splicing"
            <|> parseShortForm ","  "unquote"
            <|> parseShortForm "λ"  "lambda"
            <|> parseListLike

  parseShortForm : String -> String -> Parser SExp
  parseShortForm short long = do
    string $ unpack short
    x <- parseExpr
    pure $ SECons (SESymbol long) x

  parseListLike : Parser SExp
  parseListLike = do
    mv <- optional $ char '#'
    char '('
    xs <- sepBy parseExpr spaces
    mx <- optional $ char '.' *> spaces *> parseExpr
    char ')'
    pure $ case mv of
         Nothing => unListify (xs, mx)
         Just _  => SEVect $ fromList $ xs ++ case mx of
                                                   Nothing => []
                                                   Just x  => [SESymbol ".", x]

runParseExpr : String -> Either String SExp
runParseExpr inp =
  case parse parseExpr inp of
       Left  err       => Left err
       Right (r, rest) => case unpack rest of
                               []        => Right r
                               (x :: xs) => Left $ "Trailing garbage: " ++ show rest


text:
module Inigo.Async.CloudFlare.KV

import Inigo.Async.Promise
import Inigo.Async.Util

%foreign (promisifyPrim "(ns,key)=>this[ns] ? this[ns].get(key).then((r) => r || '') : Promise.reject('Unknown KV namespace ' + ns)")
read__prim : String -> String -> promise String

%foreign (promisifyPrim "(ns,key,value)=>this[ns] ? this[ns].put(key,value) : Promise.reject('Unknown KV namespace ' + ns)")
write__prim : String -> String -> String -> promise ()

%foreign (promisifyPrim "(ns,key,value,expirationTtl)=>this[ns] ? this[ns].put(key,value,{expirationTtl: expirationTtl}) : Promise.reject('Unknown KV namespace ' + ns)")
writeTTL__prim : String -> String -> String -> Int -> promise ()

export
read: String -> String -> Promise String
read ns key =
  promisify (read__prim ns key)

export
write: String -> String -> String -> Promise ()
write ns key value =
  promisify (write__prim ns key value)

export
writeTTL: String -> String -> String -> Int -> Promise ()
writeTTL ns key value ttl =
  promisify (writeTTL__prim ns key value ttl)

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
module Show

%default total

record Album where
  constructor MkAlbum
  artist : String
  title : String
  year : Integer

{-
  interface Show ty where
    show : (x : ty) -> String
    showPrec : (d : Prec) -> (x : ty) -> String
-}

Show Album where
  show (MkAlbum artist title year) =
    title ++ " by " ++ artist ++ " (released " ++ show year ++ ")"

help : Album
help = MkAlbum "The Beatles" "Help" 1965

rubbersoul : Album
rubbersoul = MkAlbum "The Beatles" "Rubber Soul" 1965

clouds : Album
clouds = MkAlbum "Joni Mitchell" "Clouds" 1969

hunkydory : Album
hunkydory = MkAlbum "David Bowie" "Hunky Dory" 1971

heroes : Album
heroes = MkAlbum "David Bowie" "Heroes" 1977

collection : List Album
collection = [help, rubbersoul, clouds, hunkydory, heroes]

max_stars_repo_name: timmyjose-study/tdd-with-idris

max_issues_repo_name: timmyjose-study/tdd-with-idris

max_forks_repo_name: timmyjose-study/tdd-with-idris


text:
module Main

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

main : IO ()
main = printLn (sum 50000)


text:
-- exercises in "Type-Driven Development with Idris"
-- chapter 14, section 2, VendingMachine part

import System
import Data.Primitives.Views

-- check that all functions are total
%default total

VendState : Type
VendState = (Nat, Nat)

data Input = COIN
           | VEND
           | CHANGE
           | REFILL Nat

strToInput : String -> Maybe Input
strToInput "insert" = Just COIN
strToInput "vend" = Just VEND
strToInput "change" = Just CHANGE
strToInput x = if all isDigit (unpack x)
                then Just (REFILL (cast x))
                else Nothing

data CoinResult = Inserted | Rejected

data MachineCmd : (ty : Type) ->
                  VendState ->
                  (ty -> VendState) ->
                  Type where
  InsertCoin : MachineCmd CoinResult (pounds, chocs)
                                     (\res => case res of
                                                Inserted => (S pounds, chocs)
                                                Rejected => (pounds, chocs))
  Vend :       MachineCmd () (S pounds, S chocs) $ const (pounds, chocs)
  GetCoins :   MachineCmd () (pounds, chocs)     $ const (Z, chocs)
  Refill :     (bars : Nat) ->
               MachineCmd () (Z, chocs)          $ const (Z, bars + chocs)
  Display :    String ->
               MachineCmd () s                   $ const s
  GetInput :   MachineCmd (Maybe Input) s        $ const s
  Pure :       (res : ty) -> MachineCmd ty (s res) s
  (>>=) :      MachineCmd a s1                     s2 ->
               ((res : a) -> MachineCmd b (s2 res) s3) ->
               MachineCmd b s1                     s3

data MachineIO : VendState -> Type where
  Do : MachineCmd a s1 s2 ->
       ((res : a) -> Inf (MachineIO (s2 res))) -> MachineIO s1

namespace MachineDo
  (>>=) : MachineCmd a s1 s2 ->
          ((res : a) -> Inf (MachineIO (s2 res))) -> MachineIO s1
  (>>=) = Do

getRandom : Int -> Int -> Int
getRandom val max with (divides val max)
  getRandom val 0 | DivByZero = 0
  getRandom ((max * div) + rem) max | (DivBy prf) = abs rem

||| "randomly generates" a valid or invalid coin
randomCoin : IO CoinResult
randomCoin = do seed <- time
                case (getRandom (fromInteger seed) 4) of
                  0 => pure Rejected
                  _ => pure Inserted

runMachine : MachineCmd ty inState outState -> IO ty
runMachine InsertCoin = do Inserted <- randomCoin
                           | Rejected => do putStrLn "bad coin"
                                            pure Rejected
                           putStrLn "good coin"
                           pure Inserted
runMachine Vend = putStrLn "Please take your chocolate"
runMachine {inState = (pounds, _)} GetCoins = putStrLn $ (show pounds) ++ " coins returned"
runMachine (Refill bars) = putStrLn $ "Chocolate remaining: " ++ (show bars)
runMachine (Display x) = putStrLn x
runMachine {inState = (pounds, bars)} GetInput
  = do putStrLn $ "Coins: " ++ (show pounds) ++ "; " ++
                  "Stock: " ++ (show bars)
       putStr "> "
       x <- getLine
       pure (strToInput x)
runMachine (Pure x) = pure x
runMachine (x >>= f) = do x' <- runMachine x
                          runMachine (f x')

data Fuel = Dry | More (Lazy Fuel)

partial
forever : Fuel
forever = More forever

run : Fuel -> MachineIO state -> IO ()
run (More fuel) (Do c f)
     = do res <- runMachine c
          run fuel (f res)
run Dry p = pure ()

mutual
  vend : MachineIO (pounds, chocs)
  vend {pounds = Z} = do Display "Insert a coin"
                         machineLoop
  vend {chocs = Z} = do Display "Out of stock"
                        machineLoop
  vend {pounds = (S k)} {chocs = (S j)} = do Vend
                                             Display "Enjoy!"
                                             machineLoop

  refill : (num : Nat) -> MachineIO (pounds, chocs)
  refill {pounds = Z} num = do Refill num
                               machineLoop
  refill {pounds = (S k)} num = do Display "Cannot refill: Coins in machine"
                                   machineLoop

  machineLoop : MachineIO (pounds, chocs)
  machineLoop =
    do Just x <- GetInput
        | Nothing => do Display "Invalid input"
                        machineLoop
       case x of
         COIN => do Inserted <- InsertCoin | Rejected => do Display "Coin rejected"
                                                            machineLoop
                    Display "Coin inserted"
                    machineLoop
         VEND => vend
         CHANGE => do GetCoins
                      Display "Change returned"
                      machineLoop
         REFILL num => refill num

partial
main : IO ()
main = run forever (machineLoop { pounds = 0 } { chocs = 1} )

max_stars_repo_name: pascalpoizat/idris-book

max_issues_repo_name: pascalpoizat/idris-book

max_forks_repo_name: pascalpoizat/idris-book


text:
module Bautzen.GameUnit

import Data.Fin
import Data.Maybe
import Data.Nat
import Data.Vect

%default total

-- Base Types
-- Section 1.1
public export
data Nation : Type where
  German : Nation
  Russian : Nation
  Polish : Nation

public export
Eq Nation where
  (==) German German = True
  (==) Russian Russian = True
  (==) Polish Polish = True
  (==) _ _ = False

public export
Show Nation where
  show German = "German"
  show Russian = "Russian"
  show Polish = "Polish"

public export
data Side : Type where
  Axis : Side
  Allies : Side

public export
Show Side where
  show Axis = "Axis"
  show Allies = "Allies"

public export
Eq Side where
  Axis == Axis = True
  Allies == Allies = True
  _ == _ = False

public export
flipSide : Side -> Side
flipSide Axis = Allies
flipSide Allies = Axis

public export
side : Nation -> Side
side German = Axis
side Polish = Allies
side Russian = Allies

public export
friendly : Nation -> Nation -> Bool
friendly n n' = side n == side n'

public export
data UnitType : Type where
  Armored : UnitType
  HeavyArmored : UnitType
  MechInfantry : UnitType
  Infantry : UnitType
  HeavyEngineer : UnitType
  Artillery : UnitType
  AntiTank : UnitType
  HQ : UnitType
  SupplyColumn : UnitType

public export
Eq UnitType where
  Armored == Armored = True
  HeavyArmored == HeavyArmored = True
  MechInfantry == MechInfantry = True
  Infantry == Infantry = True
  HeavyEngineer == HeavyEngineer = True
  Artillery == Artillery = True
  AntiTank == AntiTank = True
  HQ == HQ = True
  SupplyColumn == SupplyColumn = True
  _ == _ = False

public export
Show UnitType where
  show Armored = "Armored"
  show HeavyArmored = "HeavyArmored"
  show MechInfantry = "MechInfantry"
  show Infantry = "Infantry"
  show HeavyEngineer = "HeavyEngineer"
  show Artillery = "Artillery"
  show AntiTank = "AntiTank"
  show HQ = "HQ"
  show SupplyColumn = "SupplyColumn"

public export
data UnitSize : Type where
  Regiment : UnitSize
  Brigade : UnitSize
  Division : UnitSize
  Corps : UnitSize
  Army : UnitSize

public export
Show UnitSize where
  show Regiment = "Regiment"
  show Brigade = "Brigade"
  show Division = "Division"
  show Corps = "Corps"
  show Army = "Army"

public export
record StdFactors where
  constructor MkStdFactors
  attack : Nat
  defense : Nat

public export
Show StdFactors where
  show (MkStdFactors atk def) = "Standard attack=" ++ show atk++", defense=" ++ show def

public export
record Arty where
  constructor MkArty
  support : Nat
  distance : Nat

public export
Show Arty where
  show (MkArty sup dist) = "Arty support=" ++ show sup ++ ", distance=" ++ show dist

public export
record Pak where
  constructor MkPak
  antitank : Nat

public export
Show Pak where
  show (MkPak at) = "Antitank factor=" ++ show at

public export
Factors : UnitType -> Type
Factors Armored       = StdFactors
Factors HeavyArmored  = StdFactors
Factors MechInfantry  = StdFactors
Factors Infantry      = StdFactors
Factors HeavyEngineer = StdFactors
Factors Artillery     = Arty
Factors AntiTank      = Pak
Factors HQ            = Arty
Factors SupplyColumn  = Unit

public export
record GameUnit where
  constructor MkGameUnit
  nation : Nation
  unitType : UnitType
  name : String
  parent : Maybe String
  size : UnitSize
  move : Nat
  currentMP : Nat
  steps : Nat
  hits : Fin steps
  combat : Vect steps (Factors unitType)

public export
Show GameUnit where
  show (MkGameUnit nation unitType name parent size move currentMP steps hits combat) =
    "MkGameUnit nation=" ++ show nation ++
    ", unitType=" ++ show unitType ++
    ", name=" ++ name ++
    ", parent=" ++ fromMaybe "" parent ++
    ", size=" ++ show size ++
    ", move=" ++ show move ++
    ", currentMP=" ++ show currentMP ++
    ", steps=" ++ show steps ++
    ", hit=" ++ show (finToNat hits) ++
    ", combat=" ++ case unitType of
                     Armored => show combat
                     HeavyArmored => show combat
                     MechInfantry => show combat
                     Infantry => show combat
                     HeavyEngineer => show combat
                     Artillery => show combat
                     AntiTank => show combat
                     HQ => show combat
                     SupplyColumn => show combat

public export
Eq GameUnit where
  unit == unit' = name unit == name unit' && parent unit == parent unit'

public export
fullName : GameUnit -> String
fullName u = name u ++ maybe "" (\ n => "/" ++ n) (parent u)

public export
isHQ : GameUnit -> Bool
isHQ unit = unitType unit == HQ

||| Check if given `unit` is a HQ for the given formation name
||| To provide valid command for a unit, another unit:
|||
||| * be a `HQ` type of unit
||| * be part of the same formation than the given unit
||| * _or_ be an army/group HQ
|||
||| @hq the HQ we test command for
||| @unit the possibly commanded unit
public export
isHQFor : (hq : GameUnit) -> (unit : GameUnit) -> Bool
isHQFor (MkGameUnit nationality HQ _ Nothing Army _ _ _ _ _ ) unit = nation unit == nationality
isHQFor (MkGameUnit _ HQ _ formation _ _ _ _ _ _ ) unit = parent unit == formation
isHQFor _ _ = False

||| Attack factor of a `unit` when directly involved
||| in a combat
public export
attackCapacity : (unit : GameUnit) -> Nat
attackCapacity (MkGameUnit _ Armored  _ _ _ _ _ _ hits combat) = attack (index hits combat)
attackCapacity (MkGameUnit _ HeavyArmored  _ _ _ _ _ _ hits combat) = attack (index hits combat)
attackCapacity (MkGameUnit _ MechInfantry  _ _ _ _ _ _ hits combat) = attack (index hits combat)
attackCapacity (MkGameUnit _ Infantry  _ _ _ _ _ _ hits combat) = attack (index hits combat)
attackCapacity (MkGameUnit _ HeavyEngineer  _ _ _ _ _ _ hits combat) = attack (index hits combat)
-- all other units have a raw attack factor of 0 because they can't attack alone
attackCapacity _ = 0

||| Defense factor of a `unit` when directly involved
||| in a combat
public export
defenseCapacity : (unit : GameUnit) -> Nat
defenseCapacity (MkGameUnit _ Armored _ _ _ _ _ _ hits combat) = defense (index hits combat)
defenseCapacity (MkGameUnit _ HeavyArmored _ _ _ _ _ _ hits combat) = defense (index hits combat)
defenseCapacity (MkGameUnit _ MechInfantry _ _ _ _ _ _ hits combat) = defense (index hits combat)
defenseCapacity (MkGameUnit _ Infantry _ _ _ _ _ _ hits combat) = defense (index hits combat)
defenseCapacity (MkGameUnit _ HeavyEngineer _ _ _ _ _ _ hits combat) = defense (index hits combat)
defenseCapacity (MkGameUnit _ Artillery _ _ _ _ _ _ _ _) = 1
defenseCapacity (MkGameUnit _ AntiTank _ _ _ _ _ _ _ _) = 1
defenseCapacity (MkGameUnit _ HQ _ _ _ _ _ _ hits combat) =
  case index hits combat of
    (MkArty Z distance) => 0
    (MkArty (S k) distance) => divNatNZ (S k) 2 SIsNotZ
defenseCapacity (MkGameUnit _ SupplyColumn _ _ _ _ _ _ _ _) = 0

||| Is the unit a supporting unit?
public export
isSupportingUnit : (unit : GameUnit) -> Bool
isSupportingUnit unit =
  case unitType unit of
    Artillery => True
    AntiTank => True
    HQ => True
    _ => False

||| Support factor of a unit
public export
supportCapacity : (unit : GameUnit) -> Nat
supportCapacity (MkGameUnit _ Artillery _ _ _ _ _ _  hits combat) = support (index hits combat)
supportCapacity (MkGameUnit _ AntiTank _ _ _ _ _ _ hits combat) = antitank (index hits combat)
supportCapacity (MkGameUnit _ HQ _ _ _ _ _ _ hits combat) = support (index hits combat)
supportCapacity _ = 0

public export
supportDistance : (unit : GameUnit) -> Nat
supportDistance (MkGameUnit _ Artillery _ _ _ _ _ _ hits combat) = distance (index hits combat)
supportDistance (MkGameUnit _ AntiTank _ _ _ _ _ _ _ _) = 0
supportDistance (MkGameUnit _ HQ _ _ _ _ _ _ hits combat) = distance (index hits combat)
supportDistance _ = 0

-- -- list of existing units

-- -- Polish

public export
p13_5dp : GameUnit
p13_5dp = MkGameUnit Polish Infantry "13" (Just "5DP") Regiment 6 6 2 0 [ MkStdFactors 3 4, MkStdFactors 1 3 ]

public export
p15_5dp : GameUnit
p15_5dp = MkGameUnit Polish Infantry "15" (Just "5DP") Regiment 6 6 2 0 [ MkStdFactors 3 4, MkStdFactors 1 3 ]

public export
p17_5dp : GameUnit
p17_5dp = MkGameUnit Polish Infantry "17" (Just "5DP") Regiment 6 6 2 0 [ MkStdFactors 3 4, MkStdFactors 1 3 ]

public export
p5dp : GameUnit
p5dp = MkGameUnit Polish HQ "HQ" (Just "5DP") Division 4 4 1 0 [ MkArty 5 2 ]

public export
p33_7dp : GameUnit
p33_7dp = MkGameUnit Polish Infantry "33" (Just "7DP") Regiment 6 6 2 0 [ MkStdFactors 3 4, MkStdFactors 1 3 ]

public export
p32_8dp : GameUnit
p32_8dp = MkGameUnit Polish Infantry "32" (Just "8DP") Regiment 6 6 2 0 [ MkStdFactors 3 4, MkStdFactors 1 3 ]

public export
p6l : GameUnit
p6l = MkGameUnit Polish Artillery "6L" Nothing Brigade 4 4 1 0 [ MkArty 4 4 ]

public export
p2awp : GameUnit
p2awp = MkGameUnit Polish HQ "2AWP" Nothing Army 3 3 1 0 [ MkArty 9 5 ]

-- -- Russian

public export
r857_294 : GameUnit
r857_294 = MkGameUnit Russian Infantry "857" (Just "294") Brigade 8 8 1 0 [ MkStdFactors 2 4 ]

-- -- German

public export
g21_20pz : GameUnit
g21_20pz = MkGameUnit German Armored "21" (Just "20Pz") Regiment 10 10 2 0 [ MkStdFactors 6 4, MkStdFactors 4 3 ]

public export
g59_20pz : GameUnit
g59_20pz = MkGameUnit German MechInfantry "59" (Just "20Pz") Regiment 10 10 2  0 [ MkStdFactors 4 5, MkStdFactors 2 3 ]

public export
g20pz : GameUnit
g20pz = MkGameUnit German HQ "HQ" (Just "20Pz") Division 8 8 1 0 [ MkArty 6 3 ]

public export
gBrgPzG : GameUnit
gBrgPzG = MkGameUnit German HQ "HQ" (Just "BrgPzG") Division 8 8 1 0 [ MkArty 7 3 ]

public export
g777Arty : GameUnit
g777Arty = MkGameUnit German Artillery "777" Nothing Brigade 5 5 1 0 [ MkArty 6 4 ]

public export
gSupplyColumn : GameUnit
gSupplyColumn = MkGameUnit German SupplyColumn "SC" Nothing Brigade 4 4 1 0 [ () ]


text:
import Language.Reflection

%language ElabReflection

%logging 1

-- This test is for checking changes to how Names are reflected and reified.
-- It currently tests Names that refer to nested functions and Names that refer
-- to nested cases.

-- Please add future tests for Names here if they would fit in. There's plenty
-- of room.

data Identity a = MkIdentity a

nested : Identity Int
nested = MkIdentity foo
  where
    foo : Int
    foo = 12

-- a pattern matching lambda is really a case
cased : Identity Int -> Int
cased = \(MkIdentity x) => x

test : Elab ()
test = do
    n <- quote nested
    logTerm "" 1 "nested" n
    MkIdentity n' <- check {expected=Identity Int} n
    logMsg "" 1 $ show (n' == 12)

    c <- quote cased
    logTerm "" 1 "cased" c
    c' <- check {expected=Identity Int -> Int} c
    logMsg "" 1 $ show (c' (MkIdentity 10))

    pure ()

%runElab test


text:
module GRIN.Opts.Inline

import Data.SortedMap
import Data.List

import GRIN.AST
import GRIN.GrinM
import GRIN.Var

mutual
    elimFetchIdSExp : SExp name -> SExp name
    elimFetchIdSExp (Do e) = mkDo $ elimFetchIdExp e
    elimFetchIdSExp (Fetch _ v) = fetch v
    elimFetchIdSExp (FetchI _ i v) = fetchI i v
    elimFetchIdSExp e = e

    elimFetchIdExp : Exp name -> Exp name
    elimFetchIdExp = mapSExpExp elimFetchIdSExp

mutual
    inlineSExp : MonadVar m => SortedMap name (Def name) -> SExp name -> m (SExp name)
    inlineSExp im (Do e) = mkDo <$> inlineExp im e
    inlineSExp im (App fn as) = case lookup fn im of
        Nothing => pure $ App fn as
        Just (MkDef _ as' e0 _) => do
            putVars $ fromList $ zip as' as
            e1 <- updateVars e0
            e2 <- inlineExp im e1
            pure $ mkDo e2
    inlineSExp im e = pure e

    inlineExp : MonadVar m => SortedMap name (Def name) -> Exp name -> m (Exp name)
    inlineExp im (SimpleExp e) = mkSimpleExp <$> inlineSExp im e
    inlineExp im (Bind val rhs rest) = Bind val <$> inlineSExp im rhs <*> inlineExp im rest
    inlineExp im (Case pat alts) = Case pat <$> traverse (inlineAlt im) alts

    inlineAlt : MonadVar m => SortedMap name (Def name) -> Alt name -> m (Alt name)
    inlineAlt im (MkAlt pat e) = MkAlt pat <$> inlineExp im e

inlineDef : MonadVar m => SortedMap name (Def name) -> Def name -> m (Def name)
inlineDef im (MkDef fn as exp ty) = MkDef fn as <$> (inlineExp im exp) <*> pure ty

export
inlineAll : Monad m => GrinT name m ()
inlineAll = do
    im <- gets toInline
    if null im
        then pure ()
        else do
            MkProg exts defs m <- gets prog
            defs' <- traverse (inlineDef im) defs
            modify $ record { prog = MkProg exts defs' m }
            invalidate CallGraphs


text:
module SMTLib

import Data.Vect

%access public export

data NumTyp = IntT | RealT

data TypeT : Type where
  BoolT : TypeT
  NumT : NumTyp -> TypeT
  BitVecT : Nat -> TypeT

Show TypeT where
  show BoolT = "Bool"
  show (NumT IntT) = "Int"
  show (NumT RealT) = "Real"
  show (BitVecT n) = "BitVec " ++ show n

data Expr : TypeT -> Type where
  VarExpr : String -> (t : TypeT) -> Expr t
  BoolExpr : Bool -> Expr BoolT
  BvExpr : Int -> (n : Nat) -> Expr (BitVecT n)
  BvAddExpr : Expr (BitVecT n) -> Expr (BitVecT n) -> Expr (BitVecT n)
  BvMulExpr : Expr (BitVecT n) -> Expr (BitVecT n) -> Expr (BitVecT n)
  BvAndExpr : Expr (BitVecT n) -> Expr (BitVecT n) -> Expr (BitVecT n)
  BvOrExpr : Expr (BitVecT n) -> Expr (BitVecT n) -> Expr (BitVecT n)
  BvNotExpr : Expr (BitVecT n) -> Expr (BitVecT n)
  IntExpr : Int -> Expr (NumT IntT)
  RealExpr : Double -> Expr (NumT RealT)
  AddExpr : Expr (NumT a) -> Expr (NumT a) -> Expr (NumT a)
  MulExpr : Expr (NumT a) -> Expr (NumT a) -> Expr (NumT a)
  EqualExpr : Expr a -> Expr a -> Expr BoolT
  DistinctExpr : Vect n (Expr a) -> Expr BoolT
  LessOrEqualExpr : Expr (NumT a) -> Expr (NumT a) -> Expr BoolT
  AndExpr : Vect n (Expr BoolT) -> Expr BoolT
  OrExpr : Vect n (Expr BoolT) -> Expr BoolT
  NotExpr : Expr BoolT -> Expr BoolT
  IteExpr : Expr BoolT -> Expr a -> Expr a -> Expr a

bool : Bool -> Expr BoolT
bool x = BoolExpr x

bv : Int -> (n : Nat) -> Expr (BitVecT n)
bv x n = BvExpr x n

int : Int -> Expr (NumT IntT)
int x = IntExpr x

real : Double -> Expr (NumT RealT)
real x = RealExpr x

bvadd : Expr (BitVecT n) -> Expr (BitVecT n) -> Expr (BitVecT n)
bvadd l r = BvAddExpr l r

bvmul : Expr (BitVecT n) -> Expr (BitVecT n) -> Expr (BitVecT n)
bvmul l r = BvMulExpr l r

bvand : Expr (BitVecT n) -> Expr (BitVecT n) -> Expr (BitVecT n)
bvand l r = BvAndExpr l r

bvor : Expr (BitVecT n) -> Expr (BitVecT n) -> Expr (BitVecT n)
bvor l r = BvOrExpr l r

bvnot : Expr (BitVecT n) -> Expr (BitVecT n)
bvnot x = BvNotExpr x

(+) : Expr (NumT a) -> Expr (NumT a) -> Expr (NumT a)
(+) l r = AddExpr l r

(*) : Expr (NumT a) -> Expr (NumT a) -> Expr (NumT a)
(*) l r = MulExpr l r

(==) : Expr a -> Expr a -> Expr BoolT
(==) l r = EqualExpr l r

distinct : Vect n (Expr a) -> Expr BoolT
distinct xs = DistinctExpr xs

(<=) : Expr (NumT a) -> Expr (NumT a) -> Expr BoolT
(<=) l r = LessOrEqualExpr l r

(&&) : Expr BoolT -> Expr BoolT -> Expr BoolT
(&&) l r = AndExpr [l, r]

(||) : Expr BoolT -> Expr BoolT -> Expr BoolT
(||) l r = OrExpr [l, r]

and : Vect n (Expr BoolT) -> Expr BoolT
and xs = AndExpr xs

or : Vect n (Expr BoolT) -> Expr BoolT
or xs = OrExpr xs

not : Expr BoolT -> Expr BoolT
not x = NotExpr x

ite : Expr BoolT -> Expr a -> Expr a -> Expr a
ite p l r = IteExpr p l r

data Cmd : Type -> Type where
  DeclareVarCmd : String -> (t : TypeT) -> Cmd (Expr t)
  DeclareVarsCmd : Traversable f => f String -> (t : TypeT) -> Cmd (f (Expr t))
  AssertCmd : Expr BoolT -> Cmd ()
  CheckSatCmd : Cmd ()
  GetModelCmd : Cmd ()

declareVar : String -> (t : TypeT) -> Cmd (Expr t)
declareVar v t = DeclareVarCmd v t

declareVars : Traversable f => f String -> (t : TypeT) -> Cmd (f (Expr t))
declareVars vs t = DeclareVarsCmd vs t

assert : Expr BoolT -> Cmd ()
assert e = AssertCmd e

checkSat : Cmd ()
checkSat = CheckSatCmd

getModel : Cmd ()
getModel = GetModelCmd

data Smt : Type -> Type where
  Pure : a -> Smt a
  Bind : Cmd a -> (a -> Smt b) -> Smt b

pure : a -> Smt a
pure x = Pure x

(>>=) : Cmd a -> (a -> Smt b) -> Smt b
(>>=) cmd f = Bind cmd f

end : Smt ()
end = Pure ()

compileExpr : Expr t -> String
compileExpr (VarExpr x t) = x
compileExpr (BoolExpr x) = if x then "true" else "false"
compileExpr (BvExpr x n) = "(_ bv" ++ show x ++ " " ++ show n ++ ")"
compileExpr (IntExpr x) = show x
compileExpr (RealExpr x) = show x
compileExpr (BvAddExpr l r) = "(bvadd " ++ compileExpr l ++ " " ++ compileExpr r ++ ")"
compileExpr (BvMulExpr l r) = "(bvmul " ++ compileExpr l ++ " " ++ compileExpr r ++ ")"
compileExpr (BvAndExpr l r) = "(bvand " ++ compileExpr l ++ " " ++ compileExpr r ++ ")"
compileExpr (BvOrExpr l r) = "(bvor " ++ compileExpr l ++ " " ++ compileExpr r ++ ")"
compileExpr (BvNotExpr x) = "(bnot " ++ compileExpr x ++ ")"
compileExpr (AddExpr l r) = "(+ " ++ compileExpr l ++ " " ++ compileExpr r ++ ")"
compileExpr (MulExpr l r) = "(* " ++ compileExpr l ++ " " ++ compileExpr r ++ ")"
compileExpr (EqualExpr l r) = "(= " ++ compileExpr l ++ " " ++ compileExpr r ++ ")"
compileExpr (DistinctExpr xs) = "(distinct " ++ (unlines . toList . map compileExpr) xs ++ ")"
compileExpr (LessOrEqualExpr l r) = "(<= " ++ compileExpr l ++ " " ++ compileExpr r ++ ")"
compileExpr (AndExpr xs) = "(and " ++ (unlines . toList . map compileExpr) xs ++ ")"
compileExpr (OrExpr xs) = "(or " ++ (unlines . toList . map compileExpr) xs ++ ")"
compileExpr (NotExpr x) = "(not " ++ compileExpr x ++ ")"
compileExpr (IteExpr p l r) = "(if " ++ compileExpr p ++ " " ++ compileExpr l ++ " " ++ compileExpr r ++ ")"

compileCmd : Cmd a -> (a, String)
compileCmd (DeclareVarCmd x t) = (VarExpr x t, "(declare-const " ++ x ++ " " ++ show t ++ ")")
compileCmd (DeclareVarsCmd xs t) = (map (\x => VarExpr x t) xs,
                                    (unlines . toList . map (\x => "(declare-const " ++ x ++ " " ++ show t ++ ")")) xs)
compileCmd (AssertCmd e) = ((), "(assert " ++ compileExpr e ++ ")")
compileCmd CheckSatCmd = ((), "(check-sat)")
compileCmd GetModelCmd = ((), "(get-model)")

compile : Smt () -> String
compile (Pure ()) = ""
compile (Bind cmd f) = let (a, s) = compileCmd cmd in
                       let s' = compile $ f a in
                       unlines [s, s']

example0 : Expr BoolT
example0 = (bool True) && (bool True)

example1 : Expr BoolT
example1 = (bv 1 8) == (bv 1 8)

example2 : Cmd ()
example2 = checkSat

example3 : Smt ()
example3 = do x <- declareVar "x" BoolT
              y <- declareVar "y" BoolT
              assert $ x && y
              checkSat
              getModel
              end

example4 : Smt ()
example4 = do [x, y] <- declareVars {f = Vect 2} ["x", "y"] BoolT
              assert $ not (x && y) == (not x || not y)
              checkSat
              getModel
              end

print : Smt () -> IO ()
print smt = putStrLn $ compile smt

max_stars_repo_name: vikfret/idris-snippets

max_issues_repo_name: vikfret/idris-snippets

max_forks_repo_name: vikfret/idris-snippets


text:
module Flexidisc.Record.Endo

import        Flexidisc.RecordContent
import public Flexidisc.Record.Type

%default total
%access export

||| Update a row at a given `Row`, can change its type.
|||
||| Complexity is _O(n)_
|||
||| @ xs     the record
||| @ loc    the proof that the row is in it
||| @ f      the update function
updateByLabel : (xs : Record k header) -> (loc : Row query a header) ->
                (f : a -> a) ->
                Record k header
updateByLabel (Rec xs nub) (R loc) f =
  rewrite sym (changeWithSameTypeIsUnchanged loc) in
          Rec (update xs loc f) (changeValuePreservesNub nub)

||| Update a row at a given `Row`, can change its type.
|||
||| Complexity is _O(n)_
|||
||| @ query  the row name
||| @ xs     the record
||| @ loc    the proof that the row is in it
||| @ f      the update function
update : (query : k) -> (f : a -> a) -> (xs : Record k header) ->
         {auto loc : Row query a header} ->
         Record k header
update _ f xs {loc} = updateByLabel xs loc f

||| Replace a row, can change its type
|||
||| Complexity is _O(n)_
|||
||| @ xs  the record
||| @ loc the proof that the row is in it
||| @ new the new value for the row
setByLabel : (xs : Record k header) -> (loc : Row query ty header) ->
             (new : ty) ->
             Record k header
setByLabel xs loc = updateByLabel xs loc . const

||| Update a row, the update can change the row type.
|||
||| Complexity is _O(n)_
|||
||| @ query the row name
||| @ xs    the record
||| @ loc   the proof that the row is in it
||| @ new   the new value for the row
set : (query : k) -> (new : ty) -> (xs : Record k header) ->
      {auto loc : Row query ty header} ->
      Record k header
set _ new xs {loc} = updateByLabel xs loc (const new)

max_stars_repo_name: berewt/flexidisc

max_issues_repo_name: LIST-LUXEMBOURG/flexidisc

max_forks_repo_name: LIST-LUXEMBOURG/flexidisc


text:
module Another.Fourth

import A.Path.Of.Dires.Second
import Another.One.Third

%default total

example2 : Tree Nat
example2 = map S example


text:
module Chapter3

import Data.Vect

invert : Bool -> Bool
invert False = True
invert True = False

describe_list : List Int -> String
describe_list [] = "Empty List"
describe_list (x :: xs) = "Non-empty, tail = " ++ show xs

word_lengths : List String -> List Nat
word_lengths [] = []
word_lengths (word :: words) = length word :: word_lengths words

xor : Bool -> Bool -> Bool
xor False y = y
xor True y = not y

mutual
  isEven : Nat -> Bool
  isEven Z = True
  isEven (S k) = not (isEven k)

  isOdd : Nat -> Bool
  isOdd Z = False
  isOdd (S k) = isEven k

fourInts : Vect 4 Int
fourInts = [0, 1, 2, 3]

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

insert : Ord elem => (x : elem) -> (xs_sorted : Vect k elem) -> Vect (S k) elem
insert x [] = [x]
insert x (y :: xs) =  if x < y then x :: y :: xs
                               else y :: insert x xs

ins_sort : Ord elem => Vect n elem -> Vect n elem
ins_sort [] = []
ins_sort (x :: xs) = let xs_sorted = ins_sort xs in
                        insert x xs_sorted

list_length : List a -> Nat
list_length [] = 0
list_length (x :: xs) = 1 + list_length xs

list_reverse : List a -> List a
list_reverse [] = []
list_reverse (x :: xs) = (list_reverse xs) ++ [x]

list_map : (a -> b) -> List a -> List b
list_map _ [] = []
list_map f (x :: xs) = f x :: list_map f xs

vec_map : (a -> b) -> Vect n a -> Vect n b
vec_map _ [] = []
vec_map f (x :: xs) = f x :: vec_map f xs

max_stars_repo_name: balajisivaraman/idris-book

max_issues_repo_name: balajisivaraman/idris-book

max_forks_repo_name: balajisivaraman/idris-book


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

module API.Web.HTML.Document

%access public export
%default total

||| The WHATWG DOM standard defines a `Document` interface, which this extends
||| significantly.
|||
||| The original interface specification can be found at
||| https://html.spec.whatwg.org/multipage/browsers.html#the-window-object
record Document where
  constructor New
  ||| self is a non standard field which is used to facilitate integration with
  ||| Javascript.
  self    : Ptr

max_stars_repo_name: blau-io/idris-html

max_issues_repo_name: blau-io/idris-html

max_forks_repo_name: blau-io/idris-html


text:
module Test.Assert

%access export

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

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

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

assertFalse : Bool -> IO ()
assertFalse p = if (not p)
    then putStrLn "Test Passed"
    else putStrLn "Test Failed"

max_stars_repo_name: Risto-Stevcev/idris-catenatable-lists

max_issues_repo_name: Risto-Stevcev/idris-catenable-lists

max_forks_repo_name: Risto-Stevcev/idris-catenatable-lists


text:
module PrettyPrint.SExpr

%default total
%access private

export
mkSExprStr : Show a => String -> a -> String
mkSExprStr k v = concat ["(", k, " (", show v, "))"]

export
mkSExpr : Show a => String -> a -> String
mkSExpr = mkSExprStr

max_stars_repo_name: border-patrol/cordial

max_issues_repo_name: border-patrol/cordial

max_forks_repo_name: border-patrol/cordial


text:
module Twist.Util

import Data.Fin
import Data.Vect

%default total
%access export

max_stars_repo_name: msmorgan/idris-twist

max_issues_repo_name: msmorgan/idris-twist

max_forks_repo_name: msmorgan/idris-twist


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


text:
module Data.Fin.Structural

import Data.Fin
import Data.ZZ
import Control.Isomorphism

import Data.Fin.FinOrdering

%default total

{-
Structure of (Fin)s
* in general
* in terms of ordering
-}

ltePredLeft : LTE (S n) m -> LTE n m
ltePredLeft = fromLteSucc . lteSuccRight

gtnatFZImpliesIsFinSucc :
	(nel : Fin (S nu))
	-> (LTRel Z $ finToNat nel)
	-> (prednel : Fin nu ** nel = FS prednel)
gtnatFZImpliesIsFinSucc FZ ltpr = void $ succNotLTEzero ltpr
gtnatFZImpliesIsFinSucc (FS prednel) ltpr = (prednel ** Refl)

trichotomy : (n,m : Nat) -> Either (n `LT` m) $ Either (n = m) (m `LT` n)
trichotomy Z Z = Right $ Left Refl
trichotomy (S predn) Z = Right $ Right $ zLtSuccIsTrue predn
trichotomy Z (S predm) = Left $ zLtSuccIsTrue predm
trichotomy (S predn) (S predm)
	= either ( Left . LTESucc )
		( Right . either (Left . cong) (Right . LTESucc) )
	$ trichotomy predn predm

||| See (trichotomy)
eqOrGTToLT :
	Either (n = m) (LT m n)
	-> LTE m n
eqOrGTToLT = lteRelToLTE . either (Right . sym) Left

||| Allows: under decEq : (-) {smaller=notLTToGTE notlt}
notLTToGTE : Not (LT a b) -> LTE b a
notLTToGTE {a} {b} nonpr = eqOrGTToLT
	$ either (void . nonpr) id
	$ trichotomy a b

total
FinSZAreFZ : (x : Fin 1) -> x=FZ
FinSZAreFZ FZ = Refl
FinSZAreFZ (FS voda) = FinZElim voda

commuteFSWeaken : (i : Fin n) -> (FS $ weaken i = weaken $ FS i)
commuteFSWeaken i = Refl

{-
"
LTE (S (finToNat last)) (finToNat i)  cannot be a parameter of Prelude.Uninhabited.Uninhabited
(Type class arguments must be injective)
"

> instance Uninhabited (LTE (S $ finToNat $ last {n=n}) (finToNat $ the (Fin (S n)) i)) where {
> 	uninhabited = ?notSNatLastLTEAnything
> }
-}

-- notSNatLastLTEAnything : LTE (S $ finToNat $ last {n=n}) (finToNat $ the (Fin (S n)) i) -> Void

total
notSNatLastLTEAnything : {n : Nat} -> {i : Fin (S n)} -> LTE (S $ finToNat $ last {n=n}) (finToNat i) -> Void
notSNatLastLTEAnything {n} {i=FZ} = uninhabited
notSNatLastLTEAnything {n=Z} {i=FS pri} = FinZElim pri
notSNatLastLTEAnything {n=S predn} {i=FS pri} = notSNatLastLTEAnything . fromLteSucc

finToNatWeaken : {k : Fin n} -> finToNat k = finToNat (weaken k)
finToNatWeaken {k=FZ} = Refl
finToNatWeaken {k=FS k} = cong {f=S} $ finToNatWeaken {k}

partitionNatWknLT : (pnel : Fin n) -> (el : Fin (S n)) -> (elDown : LTRel (finToNat $ weaken pnel) (finToNat el)) -> Either ( LTRel (finToNat $ FS pnel) (finToNat el) ) ( el=FS pnel )
partitionNatWknLT pnel el elDown = map (sym . (finToNatInjective (FS pnel) el)) $ lteToLTERel $ lteFromEqLeft (cong {f=S} $ sym finToNatWeaken) elDown
	where
		lteFromEqLeft : (a=b) -> LTE a c -> LTE b c
		lteFromEqLeft pr lel = rewrite (sym pr) in lel

total
splitFinS : (i : Fin (S predn)) -> Either ( k : Fin predn ** i = weaken k ) ( i = Data.Fin.last )
splitFinS {predn=Z} FZ = Right Refl
splitFinS {predn=Z} (FS j) = absurd j
splitFinS {predn=S prededn} FZ = Left ( FZ ** Refl )
splitFinS {predn=S prededn} (FS prednel) with ( splitFinS prednel )
	| Left ( k ** pr ) = Left ( FS k ** cong pr )
	| Right pr = Right $ cong pr

wknLTLast : (a : Fin n) -> LT (finToNat $ weaken a) (finToNat $ last {n=n})
wknLTLast FZ = zLtSuccIsTrue _
wknLTLast (FS k) = LTESucc $ wknLTLast k

ltenatLastIsTrue2 : (i : Fin (S nu)) -> LTERel (finToNat i) $ finToNat $ last {n=nu}
ltenatLastIsTrue2 FZ {nu=Z} = Right Refl
ltenatLastIsTrue2 (FS k) {nu=Z} = absurd k
ltenatLastIsTrue2 i {nu=S prednu} with (splitFinS i)
	| Left (k ** prwkn) = Left $ rewrite prwkn in wknLTLast {n=S prednu} k
	| Right prLast = Right $ cong {f=finToNat} prLast

{- (ltenatLastIsTrue) subsection -}

notLTSelf : Not (LT a a)
notLTSelf {a=Z} = succNotLTEzero
notLTSelf {a=S preda} = notLTSelf . fromLteSucc

lteUnique : {a, b : Nat} -> (x, y : LTERel a b) -> x = y
lteUnique (Left LTEZero) (Left LTEZero) impossible
lteUnique (Left LTEZero) (Left (LTESucc ltY)) impossible
lteUnique (Left (LTESucc ltX)) (Left LTEZero) impossible
lteUnique (Left (LTESucc ltX)) (Left (LTESucc ltY)) {b=Z} impossible
lteUnique (Left (LTESucc LTEZero)) (Left (LTESucc LTEZero)) {a=Z} {b=S right} = Refl
lteUnique (Left (LTESucc ltX)) (Left (LTESucc ltY)) {a=S left} {b=S right}
	with (lteUnique (Left ltX) (Left ltY))
	| prEq = cong {f=Left . LTESucc} $ leftInjective prEq
lteUnique (Left ltX) (Right prEq) {b}
	= void $ notLTSelf $ replace prEq {P=\x => LT x b} ltX
lteUnique (Right prEq) (Left ltY) {b}
	= void $ notLTSelf $ replace prEq {P=\x => LT x b} ltY
lteUnique (Right Refl) (Right Refl) = Refl
lteUnique (Right Refl) (Right Refl) {a=Z} {b = S right} impossible
lteUnique (Right Refl) (Right Refl) {a = S left} {b=Z} impossible

ltenatLastIsTrue : Iso (nel : Fin (S nu) ** LTERel (finToNat nel) $ finToNat $ last {n=nu}) $ Fin (S nu)
ltenatLastIsTrue = MkIso
	getWitness
	(\nel => (nel ** ltenatLastIsTrue2 nel))
	(\y => Refl)
	ltenatLastIsTrue_fromTo
	where
		ltenatLastIsTrue_fromTo :
			(x : (nel : Fin (S nu)
				** LTERel (finToNat nel) $ finToNat $ last {n=nu}))
			-> (getWitness x ** ltenatLastIsTrue2 (getWitness x)) = x
		ltenatLastIsTrue_fromTo (nel ** ltepr)
			= rewrite sameLTEPr in Refl
			where
				sameLTEPr : ltenatLastIsTrue2 nel = ltepr
				sameLTEPr = lteUnique (ltenatLastIsTrue2 nel) ltepr

{-
Nat algebraic theorems
-}

lteUnsumLeftSummandRight : (x `plus` y) `LT` z -> y `LT` z
lteUnsumLeftSummandRight {x=Z} = id
lteUnsumLeftSummandRight {x=S predx} = lteUnsumLeftSummandRight . ltePredLeft

lteUnsumLeftSummandLeft : (x `plus` y) `LT` z -> x `LT` z
lteUnsumLeftSummandLeft {x} {y} = rewrite (plusCommutative x y)
	in lteUnsumLeftSummandRight

ltePlus : (a, b : Nat) -> b `LTE` (a `plus` b)
ltePlus a Z = LTEZero
ltePlus a (S predb) = rewrite sym $ plusSuccRightSucc a predb in LTESucc $ ltePlus a predb

lteImplSuccMinusPreserved : (a, b : Nat)
	-> b `LTE` a
	-> (S a) `minus` b = S (a `minus` b)
lteImplSuccMinusPreserved a Z _ = cong $ sym $ minusZeroRight a
lteImplSuccMinusPreserved Z (S predb) lteBA = void $ succNotLTEzero lteBA
lteImplSuccMinusPreserved (S preda) (S predb) lteBA
	= lteImplSuccMinusPreserved preda predb $ fromLteSucc lteBA

natPlusInvertibleR : (a, b : Nat) -> (a `plus` b) `minus` b = a
natPlusInvertibleR a Z = trans (cong $ plusZeroRightNeutral a) $ minusZeroRight a
natPlusInvertibleR Z b = sym $ minusZeroN b
natPlusInvertibleR (S preda) (S predb)
	= trans (cong {f=\t => t `minus` predb} $ sym $ plusSuccRightSucc preda predb)
	$ trans (lteImplSuccMinusPreserved (plus preda predb) predb
		$ ltePlus preda predb)
	$ cong {f=S} $ natPlusInvertibleR preda predb

natPlusInvertibleL : (a, b : Nat) -> (b `plus` a) `minus` b = a
natPlusInvertibleL a b = rewrite plusCommutative b a in natPlusInvertibleR a b

lteToSumExpr :
	(x, m : Nat)
	-> m `LTE` x
	-> (k : Nat ** x = m `plus` k)
lteToSumExpr x Z lteMX = (x ** Refl)
lteToSumExpr Z (S predm) lteMX = void $ succNotLTEzero lteMX
lteToSumExpr (S predx) (S predm) lteMX
	= either
		(\ltMX =>
			let ltPMPX = fromLteSucc ltMX
			in let oldpr = lteToSumExpr predx (S predm) ltPMPX
			in (S $ getWitness oldpr
				** cong {f=S} $ trans (getProof oldpr)
				$ plusSuccRightSucc _ _))
		(\eqMX => (Z ** sym $ trans (cong $ plusZeroRightNeutral predm) eqMX))
	$ lteToLTERel lteMX


text:
module Physics.Box2D.Defaults

%access public export

density : Double
density = 0

friction : Double
friction = 0.3

restitution : Double
restitution = 0.15


text:
import Data.Vect

readVectLen : (len : Nat) -> IO (Vect len String)
readVectLen Z = pure []
readVectLen (S k) = do x <- getLine
                       xs <- readVectLen k
                       pure (x :: xs)

testReadVect : IO ()
testReadVect = do output <- readVectLen 4
                  putStrLn(show output)

data VectUnknown : Type -> Type where
     MkVect : (len : Nat) -> Vect len a -> VectUnknown a

readVect : IO (VectUnknown String)
readVect = do x <- getLine
              if (x == "")
                 then pure (MkVect _ [])
                 else do MkVect _ xs <- readVect
                         pure (MkVect _ (x :: xs))

printVect : Show a => VectUnknown a -> IO ()
printVect (MkVect len xs)
      = putStrLn (show xs ++ " (length " ++ show len ++ ")")

mypair : (Int, String)
mypair = (94, "Pages")

anyVect : (n ** Vect n String)
anyVect = (3 ** ?anyVect_rhs)

readVect2 : IO (len ** Vect len String)
readVect2 = do x <- getLine
               if (x == "")
                  then pure (_ ** [])
                  else do (_ ** xs) <- readVect2
                          pure (_ ** x :: xs)

zipInputs : IO ()
zipInputs = do putStrLn "Enter first vector (blank line to end):"
               (len1 ** vec1) <- readVect2
               putStrLn "Enter second vector (blank line to end):"
               (len2 ** vec2) <- readVect2
               case exactLength len1 vec2 of
                  Nothing => putStrLn "Vectors are of different lengths"
                  Just vec2' => printLn (zip vec1 vec2')


text:
module Data.Nat.Equational

import Data.Nat

%default total

||| Subtract a number from both sides of an equation.
||| Due to partial nature of subtraction in natural numbers, an equation of
||| special form is required in order for subtraction to be total.
export
subtractEqLeft : (a : Nat) -> {b, c : Nat} -> a + b = a + c -> b = c
subtractEqLeft 0 prf = prf
subtractEqLeft (S k) prf = subtractEqLeft k $ succInjective (k + b) (k + c) prf

||| Subtract a number from both sides of an equation.
||| Due to partial nature of subtraction in natural numbers, an equation of
||| special form is required in order for subtraction to be total.
export
subtractEqRight : {a, b : Nat} -> (c : Nat) -> a + c = b + c -> a = b
subtractEqRight c prf =
    subtractEqLeft c $
    rewrite plusCommutative c a in
    rewrite plusCommutative c b in
    prf

||| Add a number to both sides of an inequality
export
plusLteLeft : (a : Nat) -> {b, c : Nat} -> LTE b c -> LTE (a + b) (a + c)
plusLteLeft 0 bLTEc = bLTEc
plusLteLeft (S k) bLTEc = LTESucc $ plusLteLeft k bLTEc

||| Add a number to both sides of an inequality
export
plusLteRight : {a, b : Nat} -> (c : Nat) -> LTE a b -> LTE (a + c) (b + c)
plusLteRight c aLTEb =
    rewrite plusCommutative a c in
    rewrite plusCommutative b c in
    plusLteLeft c aLTEb

||| Subtract a number from both sides of an inequality.
||| Due to partial nature of subtraction, we require an inequality of special form.
export
subtractLteLeft : (a : Nat) -> {b, c : Nat} -> LTE (a + b) (a + c) -> LTE b c
subtractLteLeft 0 abLTEac = abLTEac
subtractLteLeft (S k) abLTEac = subtractLteLeft k $ fromLteSucc abLTEac

||| Subtract a number from both sides of an inequality.
||| Due to partial nature of subtraction, we require an inequality of special form.
export
subtractLteRight : {a, b : Nat} -> (c : Nat) -> LTE (a + c) (b + c) -> LTE a b
subtractLteRight c acLTEbc =
    subtractLteLeft c $
    rewrite plusCommutative c a in
    rewrite plusCommutative c b in
    acLTEbc

||| If one of the factors of a product is greater than 0, then the other factor
||| is less than or equal to the product..
export
rightFactorLteProduct : (a, b : Nat) -> LTE b (S a * b)
rightFactorLteProduct a b = lteAddRight b

||| If one of the factors of a product is greater than 0, then the other factor
||| is less than or equal to the product..
export
leftFactorLteProduct : (a, b : Nat) -> LTE a (a * S b)
leftFactorLteProduct a b =
    rewrite multRightSuccPlus a b in
    lteAddRight a


text:
import Data.Either
import Data.List
import Data.Maybe
import Data.String
import Data.String.Parser

import System.File

wordParser : Parser String
wordParser = do chars <- some letter
                pure $ pack chars
outputParser : Parser (List String)
outputParser = do skip $ wordParser `sepBy` spaces
                  spaces
                  token "|"
                  wordParser `sepBy` spaces

parseOutput : String -> Maybe (List String)
parseOutput s = case parse outputParser s of
                     Left _ => Nothing
                     Right (l, _) => Just l

parseLines : (String -> Maybe a) -> String -> List a
parseLines f s = catMaybes $ f <$> lines s

isUnique : String -> Bool
isUnique s = let l = length s in
                 l == 2 || l == 3 || l == 4 || l == 7

run : String -> IO String
run s = do let l = parseLines parseOutput s
           let r = count isUnique $ join l
           pure $ show r

main : IO ()
main = do Right s <- readFile "input.txt"
            | Left err => putStrLn $ show err
          run s >>= putStrLn


text:
module Idris.Desugar.Mutual

import Idris.Syntax

%default total

-- Get the declaration to process on each pass of a mutual block
-- Essentially: types on the first pass
--  i.e. type constructors of data declarations
--       function types
--       interfaces (in full, since it includes function types)
--       records (just the generated type constructor)
--       implementation headers (i.e. note their existence, but not the bodies)
-- Everything else on the second pass
getDecl : Pass -> PDecl -> Maybe PDecl
getDecl p (PImplementation fc vis opts _ is cons n ps iname nusing ds)
    = Just (PImplementation fc vis opts p is cons n ps iname nusing ds)

getDecl p (PNamespace fc ns ds)
    = Just (PNamespace fc ns (assert_total $ mapMaybe (getDecl p) ds))

getDecl AsType d@(PClaim _ _ _ _ _) = Just d
getDecl AsType (PData fc doc vis mbtot (MkPData dfc tyn tyc _ _))
    = Just (PData fc doc vis mbtot (MkPLater dfc tyn tyc))
getDecl AsType d@(PInterface _ _ _ _ _ _ _ _ _) = Just d
getDecl AsType d@(PRecord fc doc vis mbtot n ps _ _)
    = Just (PData fc doc vis mbtot (MkPLater fc n (mkRecType ps)))
  where
    mkRecType : List (Name, RigCount, PiInfo PTerm, PTerm) -> PTerm
    mkRecType [] = PType fc
    mkRecType ((n, c, p, t) :: ts) = PPi fc c p (Just n) t (mkRecType ts)
getDecl AsType d@(PFixity _ _ _ _) = Just d
getDecl AsType d@(PDirective _ _) = Just d
getDecl AsType d = Nothing

getDecl AsDef (PClaim _ _ _ _ _) = Nothing
getDecl AsDef d@(PData _ _ _ _ (MkPLater _ _ _)) = Just d
getDecl AsDef (PInterface _ _ _ _ _ _ _ _ _) = Nothing
getDecl AsDef d@(PRecord _ _ _ _ _ _ _ _) = Just d
getDecl AsDef (PFixity _ _ _ _) = Nothing
getDecl AsDef (PDirective _ _) = Nothing
getDecl AsDef d = Just d

getDecl p (PParameters fc ps pds)
    = Just (PParameters fc ps (assert_total $ mapMaybe (getDecl p) pds))
getDecl p (PUsing fc ps pds)
    = Just (PUsing fc ps (assert_total $ mapMaybe (getDecl p) pds))

getDecl Single d = Just d

export
splitMutual : List PDecl -> (List PDecl, List PDecl)
splitMutual ds = (mapMaybe (getDecl AsType) ds, mapMaybe (getDecl AsDef) ds)


text:
> foo : Nat -> Nat
> foo x = ?foo_rhs
>
> bar : Nat -> Nat
> bar x = plus x ?bar_rhs
>
> -- Rest of file

ext: lidr


text:
module Main

import IdrisJvm.FFI
import IdrisJvm.IO

-- Returning an additional Nat to test that `par` returns a complex type correctly
fibonacci : Integer -> (Nat, Integer)
fibonacci 0 = (0, 0)
fibonacci 1 = (1, 1)
fibonacci n =
  let (fibNat1, fib1) = par $ fibonacci (n - 1) -- Evaluate in parallel using Java's ForkJoin
      (fibNat2, fib2) = par $ fibonacci (n - 2) -- Evaluate in parallel
      fibNat = fibNat1 + fibNat2
  in (fibNat * 2, fib1 + fib2)

shutdownExecutor : JVM_IO ()
shutdownExecutor = javacall (Static clz "shutdownExecutor") (JVM_IO ()) where
  clz = Class "io/github/mmhelloworld/idrisjvm/runtime/Concurrent"

main : JVM_IO ()
main = do
  fork $ printLn "a" -- Run in a new thread using Java's ExecutorService
  fork $ printLn "b" -- Run in another thread
  fork $ printLn $ fibonacci 10
  fork $ printLn "cde"
  fork $ printLn "fg"
  printLn "h"
  shutdownExecutor

max_stars_repo_name: mmhelloworld/idris-jvm-hs

max_issues_repo_name: mmhelloworld/idris-jvm-hs

max_forks_repo_name: mmhelloworld/idris-jvm-hs


text:
module Language.LSP.Message.Progress

import Language.JSON
import Language.LSP.Message.Derive
import Language.LSP.Message.Utils
import Language.Reflection

%language ElabReflection
%default total

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#progress
public export
ProgressToken : Type
ProgressToken = OneOf [Int, String]

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#clientInitiatedProgress
public export
record WorkDoneProgressOptions where
  constructor MkWorkDoneProgressOptions
  workDoneProgress : Maybe Bool
%runElab deriveJSON defaultOpts `{{WorkDoneProgressOptions}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#clientInitiatedProgress
public export
record WorkDoneProgressParams where
  constructor MkWorkDoneProgressParams
  workDoneToken : Maybe ProgressToken
%runElab deriveJSON defaultOpts `{{WorkDoneProgressParams}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#partialResultParams
public export
record PartialResultParams where
  constructor MkPartialResultParams
  partialResultToken : Maybe ProgressToken
%runElab deriveJSON defaultOpts `{{PartialResultParams}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workDoneProgressBegin
public export
record WorkDoneProgressBegin where
  constructor MkWorkDoneProgressBegin
  title : String
  cancellable : Maybe Bool
  message : Maybe String
  percentage : Maybe Int
%runElab deriveJSON (record {staticFields = [("kind", JString "begin")]} defaultOpts) `{{WorkDoneProgressBegin}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workDoneProgressReport
public export
record WorkDoneProgressReport where
  constructor MkWorkDoneProgressReport
  cancellable : Maybe Bool
  message : Maybe String
  percentage : Maybe Int
%runElab deriveJSON (record {staticFields = [("kind", JString "report")]} defaultOpts) `{{WorkDoneProgressReport}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#workDoneProgressEnd
public export
record WorkDoneProgressEnd where
  constructor MkWorkDoneProgressEnd
  message : Maybe String
%runElab deriveJSON (record {staticFields = [("kind", JString "end")]} defaultOpts) `{{WorkDoneProgressEnd}}


text:
module Language.LSP.Metavars

import Core.Context
import Core.Core
import Core.Directory
import Core.Env
import Core.TT
import Core.Name
import Idris.IDEMode.Holes
import Idris.Pretty
import Idris.Pretty.Render
import Idris.REPL.Opts
import Idris.Resugar
import Idris.Syntax
import Language.JSON
import Language.LSP.Message
import Language.LSP.Definition
import Server.Configuration
import Server.Utils
import System.File
import System.Path
import Libraries.Text.PrettyPrint.Prettyprinter.Symbols

%hide Holes.HolePremise
%hide Holes.HoleData
%hide Holes.getUserHolesData

-- Non-exported functions are temporary changes to functions in the module Idris.IDEMode.Holes.
-- TODO: upstream changes to the compiler when stability is reached.

record HolePremise where
  constructor MkHolePremise
  name         : Name
  location     : FC
  type         : IPTerm
  multiplicity : RigCount
  isImplicit   : Bool

record HoleData where
  constructor MkHoleData
  name : Name
  location : FC
  type : IPTerm
  context : List HolePremise

showName : Name -> Bool
showName (UN Underscore) = False
showName (MN _ _) = False
showName _ = True

-- TODO: Check why premise location is replFC.
extractHoleData : {vars : _}
               -> Ref Ctxt Defs
               => Ref Syn SyntaxInfo
               => Defs -> Env Term vars -> Name -> FC -> Nat -> Term vars
               -> Core HoleData
extractHoleData defs env fn fc (S args) (Bind _ _ (Let _ _ val _) sc) =
  extractHoleData defs env fn fc args (subst val sc)
extractHoleData defs env fn fc (S args) (Bind fc' x b sc) = do
  rest <- extractHoleData defs (b :: env) fn fc args sc
  let True = showName x
    | False => pure rest
  ity <- resugar env !(normalise defs env (binderType b))
  let premise = MkHolePremise x fc' ity (multiplicity b) (isImplicit b)
  pure $ record { context $= (premise ::) } rest
extractHoleData defs env fn fc args ty = do
  nty <- normalise defs env ty
  ity <- resugar env nty
  pure $ MkHoleData fn fc ity []

holeData : {vars : _}
        -> Ref Ctxt Defs
        => Ref Syn SyntaxInfo
        => Defs -> Env Term vars -> Name -> FC -> Nat -> Term vars ->
           Core HoleData
holeData gam env fn fc args ty = do
  hdata <- extractHoleData gam env fn fc args ty
  pp <- getPPrint
  pure $ if showImplicits pp
            then hdata
            else record { context $= dropShadows } hdata
  where
    dropShadows : List HolePremise -> List HolePremise
    dropShadows [] = []
    dropShadows (premise :: rest) =
      if premise.name `elem` map name rest
         then            dropShadows rest
         else premise :: dropShadows rest

getUserHolesData : Ref Ctxt Defs
                => Ref Syn SyntaxInfo
                => Core (List HoleData)
getUserHolesData = do
  defs <- get Ctxt
  let ctxt = gamma defs
  ms  <- getUserHoles
  let globs = concat !(traverse (\n => lookupCtxtName n ctxt) ms)
  let holesWithArgs = mapMaybe (\(n, i, gdef) => pure (n, gdef, !(isHole gdef))) globs
  traverse (\(n, gdef, args) => holeData defs [] n (location gdef) args (type gdef)) holesWithArgs

||| Returns the list of metavariables visible in the current context with their location.
||| JSON schema for a single metavariable:
||| {
|||   location: Location | null;
|||   name: string;
|||   type: string;
|||   premises: Premise[]
||| }
||| JSON schema for a single premise:
||| {
|||   location: Location | null;
|||   name: string;
|||   type: string;
|||   isImplicit: bool;
||| }
export
metavarsCmd : Ref Ctxt Defs
           => Ref Syn SyntaxInfo
           => Ref ROpts REPLOpts
           => Ref LSPConf LSPConfiguration
           => Core JSON
metavarsCmd = do
  c <- getColor
  setColor False
  holes <- getUserHolesData
  res <- for holes $ \h => do
    loc <- case h.location of
      MkFC f s e => mkLocation f s e
      MkVirtualFC f s e => mkLocation f s e
      _ => pure Nothing
    let name = show h.name
    type <- render (reAnnotate Syntax $ prettyTerm h.type)
    premises <- for h.context $ \p => do
      loc <- case p.location of
        MkFC f s e => mkLocation f s e
        MkVirtualFC f s e => mkLocation f s e
        _ => pure Nothing
      let name = show p.name
      type <- render (reAnnotate Syntax $ prettyTerm p.type)
      pure $ JObject [("location", toJSON loc), ("name", toJSON name), ("type", toJSON type), ("isImplicit", toJSON p.isImplicit)]
    pure $ JObject [("location", toJSON loc), ("name", toJSON name), ("type", toJSON type), ("premises", JArray premises)]
  setColor c
  pure $ JArray res


text:
module Control.Comonad.Env.Env

import Control.Comonad
import Control.Comonad.Trans
import Control.Monad.Identity

%default total

public export
record EnvT (e : Type) (w : Type -> Type) (a : Type)  where
  constructor MkEnvT
  env : e
  val : w a

public export
Env : (e : Type) -> (a : Type) -> Type
Env e = EnvT e Identity

||| Create an Env using an environment and a value
public export
mkEnv : e -> a -> Env e a
mkEnv e a = MkEnvT e (Id a)

public export
runEnv : Env e a -> (e, a)
runEnv (MkEnvT e (Id a)) = (e, a)

public export
runEnvT : EnvT e w a -> (e, w a)
runEnvT (MkEnvT e wa) = (e, wa)

||| Modifies the environment using the specified function.
public export
local : (e -> e') -> EnvT e w a -> EnvT e' w a
local f = record { env $= f}

--------------------------------------------------------------------------------
--          Interface Implementations
--------------------------------------------------------------------------------

public export
Functor w => Functor (EnvT e w) where
  map g (MkEnvT e wa) = MkEnvT e (map g wa)

public export
(Monoid e, Applicative m) => Applicative (EnvT e m) where
  pure = MkEnvT neutral . pure
  MkEnvT ef wf <*> MkEnvT ea wa = MkEnvT (ef <+> ea) (wf <*> wa)

public export
Foldable w => Foldable (EnvT e w) where
  foldl f acc = foldl f acc . val
  foldr f acc = foldr f acc . val
  null        = null . val

public export
Traversable w => Traversable (EnvT e w) where
  traverse f (MkEnvT e w) = MkEnvT e <$> traverse f w

public export
Comonad w => Comonad (EnvT e w) where
  duplicate (MkEnvT e wa) = MkEnvT e (extend (MkEnvT e) wa)
  extract = extract . val

public export
ComonadTrans (EnvT e) where
  lower (MkEnvT _ wa) = wa

public export
(Semigroup e, ComonadApply w) => ComonadApply (EnvT e w) where
  MkEnvT ef wf <@> MkEnvT ea wa = MkEnvT (ef <+> ea) (wf <@> wa)


text:
module System.File.Error

import System.Errno

import System.File.Support
import public System.File.Types
import System.FFI

%default total

fileClass : String
fileClass = "io/github/mmhelloworld/idrisjvm/runtime/ChannelIo"

%foreign support "idris2_fileError"
         "node:lambda:x=>(x===1?1:0)"
         jvm' fileClass "getErrorNumber" fileClass "int"
prim__error : FilePtr -> PrimIO Int

%foreign support "idris2_fileErrno"
         "node:support:fileErrno,support_system_file"
         jvm' runtimeClass "getErrorNumber" "java/lang/Object" "int"
prim__fileErrno : PrimIO Int

public export
data FileError = GenericFileError Int -- errno
               | FileReadError
               | FileWriteError
               | FileNotFound
               | PermissionDenied
               | FileExists

export
returnError : HasIO io => io (Either FileError a)
returnError
    = do err <- primIO prim__fileErrno
         pure $ Left $
           case err of
              0 => FileReadError
              1 => FileWriteError
              2 => FileNotFound
              3 => PermissionDenied
              4 => FileExists
              _ => GenericFileError (err-5)

export
Show FileError where
  show (GenericFileError errno) = strerror errno
  show FileReadError = "File Read Error"
  show FileWriteError = "File Write Error"
  show FileNotFound = "File Not Found"
  show PermissionDenied = "Permission Denied"
  show FileExists = "File Exists"

export
fileError : HasIO io => File -> io Bool
fileError (FHandle f)
    = do x <- primIO $ prim__error f
         pure (x /= 0)


text:
http://docs.idris-lang.org/en/latest/tutorial/miscellany.html
> module literate

This is a comment. The main program is below

> main : IO ()
> main = putStrLn "Hello literate world!\n"


text:
postInc : Nat -> Nat
postInc = (`plus` 1)

infixr 8 `cons`
cons : Int -> List Int -> List Int
cons = (::)

namespace A
  infixr 8 `nmul`
  nmul : Nat -> Nat -> Nat
  nmul = (*)

namespace B
  nmul : Nat -> Nat -> Nat
  nmul _ y = y

prefix 1 :/
(:/) : Nat -> Nat
(:/) = (1 `plus`)

main : IO ()
main = do
  printLn $ (1 `cons`) [2] == [1,2]
  printLn $ (1 ::) [2]     == [1,2]
  printLn $ (`cons` [2]) 1 == [1,2]
  printLn $ (:: [2]) 1     == [1,2]
  let x : Integer = 4
  printLn $ (- x) == -4         -- prefix, not section
  let io : IO Integer = pure 9
  printLn $ (! io) == 9         -- prefix, not section
  printLn $ (:/ 3) == 4         -- custom prefix operator (#2571)
  printLn $ 1 `cons` 2 `cons` [3] == [1,2,3]
  printLn $ 2 `A.nmul` 3 `B.nmul` 5 == 10
  printLn $ 2 `B.nmul` 3 `A.nmul` 5 == 15

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 MinesweeperSMT

import Data.Vect
import src.SMTLib
import src.Tensor
import src.GridOps

puzzle : Vect 9 (Vect 9 Int)
puzzle = [ [-1, -1, -1, -1,  1,  0,  0,  1, -1],
           [-1, -1,  2,  1,  1,  0,  0,  1,  1],
           [-1, -1,  1,  0,  0,  0,  0,  0,  0],
           [-1,  2,  1,  0,  0,  0,  0,  0,  0],
           [-1,  2,  0,  0,  0,  0,  0,  0,  0],
           [-1,  3,  1,  0,  0,  0,  1,  1,  1],
           [-1, -1,  1,  0,  0,  0,  1, -1, -1],
           [-1, -1,  2,  2,  1,  1,  1, -1, -1],
           [-1, -1, -1, -1, -1, -1, -1, -1, -1] ]

lookup : Fin n -> Fin m -> List Dir ->  Vect n (Vect m (Expr (NumT IntT))) -> Expr (NumT IntT)
lookup n m ds xss = GridOps.lookup n m ds (int 0) xss

equation : Fin n -> Fin m -> Int -> Vect n (Vect m (Expr (NumT IntT))) -> Expr BoolT
equation n m v xss with (toPos n, toPos m)
  equation n m v xss | (First, First) = add [lookup n m [Left] xss, lookup n m [Up] xss, lookup n m [Up, Left] xss] == (int v)
  equation n m v xss | (Last, Last) = add [lookup n m [Right] xss, lookup n m [Down] xss, lookup n m [Down, Right] xss] == (int v)
  equation n m v xss | (First, Last) = add [lookup n m [Right] xss, lookup n m [Up] xss, lookup n m [Up, Right] xss] == (int v)
  equation n m v xss | (Last, First) = add [lookup n m [Left] xss, lookup n m [Down] xss, lookup n m [Down, Left] xss] == (int v)
  equation n m v xss | (First, _) = add [lookup n m [Left] xss, lookup n m [Right] xss, lookup n m [Up] xss,
                                         lookup n m [Up, Right] xss, lookup n m [Up, Left] xss] == (int v)
  equation n m v xss | (Last, _) = add [lookup n m [Left] xss, lookup n m [Right] xss, lookup n m [Down] xss,
                                        lookup n m [Down, Right] xss, lookup n m [Down, Left] xss] == (int v)
  equation n m v xss | (_, First) = add [lookup n m [Left] xss, lookup n m [Down] xss, lookup n m [Down, Left] xss,
                                         lookup n m [Up] xss, lookup n m [Up, Left] xss] == (int v)
  equation n m v xss | (_, Last) = add [lookup n m [Right] xss, lookup n m [Down] xss, lookup n m [Down, Right] xss,
                                        lookup n m [Up] xss, lookup n m [Up, Right] xss] == (int v)
  equation n m v xss | (_, _) = add [lookup n m [Left] xss, lookup n m [Right] xss, lookup n m [Down] xss,
                                     lookup n m [Up] xss, lookup n m [Down, Right] xss, lookup n m [Down, Left] xss,
                                     lookup n m [Up, Right] xss, lookup n m [Up, Left] xss] == (int v)

collect : Vect n (Vect m Int) -> Vect n (Vect m (Expr (NumT IntT))) -> Vect n (Vect m (Expr BoolT))
collect puzzle vars = tabulate (\n => tabulate (\m => let (x, v) = (index n m puzzle, index n m vars) in
                                                      if x < 0 then (v == (int 0)) || (v == (int 1)) else (v == (int 0)) && equation n m x vars))

vars : Tensor [9, 9] String
vars = toTensor $ tabulate (\i0 => tabulate (\i1 => "x_" ++ show (finToNat i0) ++ "_" ++ show (finToNat i1)))

inst : Vect 9 (Vect 9 (Expr (NumT IntT)))
inst = tabulate (\i0 => tabulate (\i1 => int $ index i0 i1 puzzle))

solver : Smt ()
solver = do vars <- declareVars vars (NumT IntT)
            assert $ and $ concat $ collect puzzle (toVect vars)
            assert $ index 0 1 (toVect vars) == (int 1)
            checkSat
            getModel
            end

test : IO ()
test = print solver

max_stars_repo_name: STELIORD/idris-snippets

max_issues_repo_name: stjordanis/idris-snippets

max_forks_repo_name: stjordanis/idris-snippets


text:
import Stuff

interface Functor f where
    map : (a -> b) -> f a -> f b

Functor List where
  map f [] = []
  map f (x :: xs) = f x :: map f xs

data Test : Type -> Type -> Type -> Type where
     MkTest : a -> b -> c -> Test a b c

Functor (Test c d) where
  map = ?foo

-- Checking we can cope with the clash between the a,b here and the
-- a,b in 'map' (the names here get priority, and the ones in map get
-- renamed)
Functor (Test a b) where
  map = ?bar


text:
import Data.Vect

myReverse : Vect n elem -> Vect n elem
myReverse [] = []
myReverse (x :: xs) = reverseProof (myReverse xs ++ [x]) where
                      reverseProof : Vect (len + 1) elem -> Vect (S len) elem
                      reverseProof result = rewrite plusCommutative 1 len in result


text:
module TypedContainers.RBTree.Index

import Data.Nat
import Data.DPair
import Data.List
import TypedContainers.In
import TypedContainers.LawfulOrd
import TypedContainers.RBTree.Base

%default total

public export
data Erased : Type -> Type where
  MkErased : (0 _ : a) -> Erased a

0 helper : LawfulOrd a => (x : a) -> (y : a) -> (z : a) -> (x > y = True) -> (y == z = True) -> (x > z = True)
helper x y z p1 p2 =
  let p1' = convGT x y p1 in
  let p2' = convEQ y z p2 in
  let p3 = equality2 y z x p2' in
  let p4 : (compare x z = GT) = replace {p = \arg => arg = GT} p3 p1' in
  cong (\case {GT => True; _ => False}) p4

public export
indexG : {0 keys : List kt} -> {kord : LawfulOrd kt} -> (k : kt) -> {0 k_in_keys : In (k ==) keys} -> GoodTree {kt, kord, keys, vt} -> Exists $ \k' => Exists $ \_ : compare k' k = EQ => vt k'
indexG k (Empty Refl) impossible
indexG k (RedNode k' v l r) = case the (Subset Ordering (compare k' k ===)) $ Element (compare k' k) Refl of
  Element EQ p0 => Evidence k' $ Evidence p0 v
  Element GT p0 =>
    let 0 p1 = \x, p => helper k' k x (cong (\case {GT => True; _ => False}) p0) p in
    let 0 p2 : In (k ==) (filter (k' >) keys) = inFilter (k' >) (k ==) p1 keys k_in_keys in
    indexG k l {k_in_keys = p2}
  Element LT p0 =>
    let 0 p1 = \x, p => ( let p1' = replace {p = \arg => arg = LT} (equality2 k x k' (convEQ k x p)) p0 in let p1'' = cong (\case {LT => True; _ => False}) p1' in the (k' < x = True) p1'' ) in
    let 0 p2 : In (k ==) (filter (k' <) keys) = inFilter (k' <) (k ==) p1 keys k_in_keys in
    indexG k r {k_in_keys = p2}
indexG k (BlackNode k' v l r) = case the (Subset Ordering (compare k' k ===)) $ Element (compare k' k) Refl of
  Element EQ p0 => Evidence k' $ Evidence p0 v
  Element GT p0 =>
    let 0 p1 = \x, p => helper k' k x (cong (\case {GT => True; _ => False}) p0) p in
    let 0 p2 : In (k ==) (filter (k' >) keys) = inFilter (k' >) (k ==) p1 keys k_in_keys in
    indexG k l {k_in_keys = p2}
  Element LT p0 =>
    let 0 p1 = \x, p => ( let p1' = replace {p = \arg => arg = LT} (equality2 k x k' (convEQ k x p)) p0 in let p1'' = cong (\case {LT => True; _ => False}) p1' in the (k' < x = True) p1'' ) in
    let 0 p2 : In (k ==) (filter (k' <) keys) = inFilter (k' <) (k ==) p1 keys k_in_keys in
    indexG k r {k_in_keys = p2}

public export
indexGMaybe : {0 b : kt -> Type} -> {0 keys : List kt} -> {kord : LawfulOrd kt} -> (k : kt)
  -> {0 foldLeft : (Not $ In (k ==) keys) -> a}
  -> {0 foldRight : (k' : kt) -> (compare k' k = EQ, In (k' ==) keys) -> b k'}
  -> GoodTree {kt, kord, keys, vt}
  -> Either (Erased $ a) (DPair kt $ \k' => Exists $ \_ : b k' => vt k')
indexGMaybe k (Empty Refl) = Left $ MkErased $ foldLeft $ \p => case p of
  MkIn _ _ _ impossible
  MkInCons _ _ _ impossible
indexGMaybe k (RedNode k' v l r {kp}) = case the (Subset Ordering (compare k' k ===)) $ Element (compare k' k) Refl of
  Element EQ p0 => Right $ MkDPair k' $ Evidence (foldRight k' (p0, kp)) v
  Element GT p0 =>
    let
      0 p1 : (x : kt) -> (k == x = True) -> (k' > x = True)
      p1 x pp0 = cong (\case { GT => True; _ => False }) $ sym $ trans (sym p0) (equality2 k x k' (convEQ k x pp0))

      0 foldLeft' : (In (k ==) (filter (k' >) keys) -> Void) -> a
      foldLeft' pp0 = foldLeft $ \pp1 => pp0 $ inFilter (k' >) (k ==) p1 keys pp1

      0 foldRight' : (k'' : kt) -> (compare k'' k = EQ, In (k'' ==) (filter (k' >) keys)) -> b k''
      foldRight' k'' (pp0, pp1) = foldRight k'' (pp0, outFilter pp1)
    in
    indexGMaybe k {foldLeft = foldLeft', foldRight = foldRight'} l
  Element LT p0 =>
    let
      0 p1 : (x : kt) -> (k == x = True) -> (k' < x = True)
      p1 x pp0 = cong (\case { LT => True; _ => False }) $ sym $ trans (sym p0) (equality2 k x k' (convEQ k x pp0))

      0 foldLeft' : (In (k ==) (filter (k' <) keys) -> Void) -> a
      foldLeft' pp0 = foldLeft $ \pp1 => pp0 $ inFilter (k' <) (k ==) p1 keys pp1

      0 foldRight' : (k'' : kt) -> (compare k'' k = EQ, In (k'' ==) (filter (k' <) keys)) -> b k''
      foldRight' k'' (pp0, pp1) = foldRight k'' (pp0, outFilter pp1)
    in
    indexGMaybe k {foldLeft = foldLeft', foldRight = foldRight'} r
indexGMaybe k (BlackNode k' v l r {kp}) = case the (Subset Ordering (compare k' k ===)) $ Element (compare k' k) Refl of
  Element EQ p0 => Right $ MkDPair k' $ Evidence (foldRight k' (p0, kp)) v
  Element GT p0 =>
    let
      0 p1 : (x : kt) -> (k == x = True) -> (k' > x = True)
      p1 x pp0 = cong (\case { GT => True; _ => False }) $ sym $ trans (sym p0) (equality2 k x k' (convEQ k x pp0))

      0 foldLeft' : (In (k ==) (filter (k' >) keys) -> Void) -> a
      foldLeft' pp0 = foldLeft $ \pp1 => pp0 $ inFilter (k' >) (k ==) p1 keys pp1

      0 foldRight' : (k'' : kt) -> (compare k'' k = EQ, In (k'' ==) (filter (k' >) keys)) -> b k''
      foldRight' k'' (pp0, pp1) = foldRight k'' (pp0, outFilter pp1)
    in
    indexGMaybe k {foldLeft = foldLeft', foldRight = foldRight'} l
  Element LT p0 =>
    let
      0 p1 : (x : kt) -> (k == x = True) -> (k' < x = True)
      p1 x pp0 = cong (\case { LT => True; _ => False }) $ sym $ trans (sym p0) (equality2 k x k' (convEQ k x pp0))

      0 foldLeft' : (In (k ==) (filter (k' <) keys) -> Void) -> a
      foldLeft' pp0 = foldLeft $ \pp1 => pp0 $ inFilter (k' <) (k ==) p1 keys pp1

      0 foldRight' : (k'' : kt) -> (compare k'' k = EQ, In (k'' ==) (filter (k' <) keys)) -> b k''
      foldRight' k'' (pp0, pp1) = foldRight k'' (pp0, outFilter pp1)
    in
    indexGMaybe k {foldLeft = foldLeft', foldRight = foldRight'} r

max_stars_repo_name: L-as/idris-rbtree

max_issues_repo_name: L-as/idris-rbtree

max_forks_repo_name: L-as/idris-rbtree


text:
-- ----------------------------------------------------------------- [ Lib.idr ]
-- Module      : Data.Composition
-- Description : Composition extras much like Data.Composition for
--               Haskell
-- --------------------------------------------------------------------- [ EOH ]

||| A bunch of function composition extras, inspired by the Haskell package of the same name.
module Data.Composition

import Hezarfen

%language ElabReflection

%default total

%access export

infixl 9 .*
infixl 9 .**
infixl 9 .***
infixl 9 .****
infixl 9 .*****
infixl 9 -.*
infixl 9 -.**
infixl 9 -.***
infixl 9 -.****
infixl 9 -.*****
infixl 9 *.
infixl 9 **.
infixl 9 ***.
infixl 9 ****.
infixl 9 *****.
infixl 9 &
infixl 9 &~
infixl 9 &~~
infixl 9 &~~~
infixl 9 -.
infixl 9 .$

on : (a -> a -> b) -> (c -> a) -> (c -> c -> b)
on = %runElab hezarfenExpr

||| Infix equivalent to 'on'
(.$) : (a -> a -> b) -> a -> b
(.$) = %runElab hezarfenExpr

||| Backwards function composition
(-.) : (a -> b) -> (b -> c) -> (a -> c)
(-.) = %runElab hezarfenExpr

||| Composition when one function has arity > 1
|||
||| Instead of `f = \x, y => 2 * y + x`, we can write `f = (*2) .* (+)`
(.*) : (c -> d) -> (a -> b -> c) -> (a -> b -> d)
(.*) = %runElab hezarfenExpr

(.**) : (d -> e) -> (a -> b -> c -> d) -> (a -> b -> c -> e)
(.**) = %runElab hezarfenExpr

(.***) : (e -> f) -> (a -> b -> c -> d -> e) -> (a -> b -> c -> d -> f)
(.***) = %runElab hezarfenExpr

(.****) : (f -> g) -> (a -> b -> c -> d -> e -> f) -> (a -> b -> c -> d -> e -> g)
(.****) = %runElab hezarfenExpr

(.*****) : (g -> h) -> (a -> b -> c -> d -> e -> f -> g) -> (a -> b -> c -> d -> e -> f -> h)
(.*****) = %runElab hezarfenExpr

(*.) : (a -> b -> c) -> (c -> d) -> (a -> b -> d)
(*.) = %runElab hezarfenExpr

(**.) : (a -> b -> c -> d) -> (d -> e) -> (a -> b -> c -> e)
(**.) = %runElab hezarfenExpr

(***.) : (a -> b -> c -> d -> e) -> (e -> f) -> (a -> b -> c -> d -> f)
(***.) = %runElab hezarfenExpr

(****.) : (a -> b -> c -> d -> e -> f) -> (f -> g) -> (a -> b -> c -> d -> e -> g)
(****.) = %runElab hezarfenExpr

(*****.) : (a -> b -> c -> d -> e -> f -> g) -> (g -> h) -> (a -> b -> c -> d -> e -> f -> h)
(*****.) = %runElab hezarfenExpr

||| The Oedipus combinator
(-.*) : (d -> b) -> (a -> b -> c) -> (a -> d -> c)
(-.*) = %runElab hezarfenExpr

||| Composition on the last argument rather than the return value
(-.**) : (e -> c) -> (a -> b -> c -> d) -> (a -> b -> e -> d)
(-.**) = %runElab hezarfenExpr

(-.***) : (f -> d) -> (a -> b -> c -> d -> e) -> (a -> b -> c -> f -> e)
(-.***) = %runElab hezarfenExpr

(-.****) : (g -> e) -> (a -> b -> c -> d -> e -> f) -> (a -> b -> c -> d -> g -> f)
(-.****) = %runElab hezarfenExpr

(-.*****) : (h -> f) -> (a -> b -> c -> d -> e -> f -> g) -> (a -> b -> c -> d -> e -> h -> g)
(-.*****) = %runElab hezarfenExpr

||| Backwards function application
(&) : a -> (a -> b) ->  b
(&) = %runElab hezarfenExpr

(&~) : (a -> b -> c) -> b -> a -> c
(&~) = %runElab hezarfenExpr

(&~~) : (a -> b -> c -> d) -> c -> b -> a -> d
(&~~) = %runElab hezarfenExpr

(&~~~) : (a -> b -> c -> d -> e) -> d -> c -> b -> a -> e
(&~~~) = %runElab hezarfenExpr

max_stars_repo_name: vmchale/composition

max_issues_repo_name: vmchale/composition

max_forks_repo_name: vmchale/composition