text:
module BinaryFormats

import Control.Pipeline
import Data.Vect
import Data.ZZ

import BinaryFormats.Data.Bit
import BinaryFormats.Data.List

%default total

mutual
    ||| A universe of binary data formats
    data Format : Type where
        FBad : Format
        FEnd : Format
        FBit : Format
        FByte : Format
        FChar : Format
        FU8 : Format
        FU16 : Format -- TODO: Endianness
        FU32 : Format -- TODO: Endianness
        FS8 : Format
        FS16 : Format -- TODO: Endianness
        FS32 : Format -- TODO: Endianness
        FRef : Format
        FPtr : Nat -> List Bit -> Format -> Format
        FVect : Nat -> Format -> Format
        FPlus : Format -> Format -> Format
        FSkip : Format -> Format -> Format
        FRead : (f : Format) -> (embed f -> Format) -> Format

    ||| Interprets `Format` as an Idris type
    embed : Format -> Type
    embed FBad = Void
    embed FEnd = Unit
    embed FBit = Bit
    embed FByte = Bits8
    embed FChar = Char
    embed FU8 = Nat
    embed FU16 = Nat
    embed FU32 = Nat
    embed FS8 = ZZ
    embed FS16 = ZZ
    embed FS32 = ZZ
    embed FRef = List Bit
    embed (FPtr _ _ f) = Lazy (Maybe (embed f))
    embed (FVect n a) = Vect n (embed a)
    embed (FPlus f1 f2) = Either (embed f1) (embed f2)
    embed (FSkip _ f) = embed f
    embed (FRead f1 f2) = (f : embed f1 ** embed (f2 f))

||| Require a predicate to be satisfied
satisfy : (f : Format) -> (embed f -> Bool) -> Format
satisfy f pred =
    FRead f  (\x => if pred x then FEnd else FBad)

||| Require a character literal to be parsed
char : Char -> Format
char c =
    satisfy FChar ((==) c)

||| Sequence two binary formats, one after the other
(>>) : Format -> Format -> Format
(>>) x f = FSkip x f

||| Parsed one format and then use it to figure out what to parse next
(>>=) : (f : Format) -> (embed f -> Format) -> Format
(>>=) x f = FRead x f

Parser : Type -> Type
Parser a = (bits : List Bit) -> Maybe (a, List Bit)

parseBit : Parser Bit
parseBit [] = Nothing
parseBit (bit :: bits) = Just (bit, bits)

parseUNum : {a : Type} -> Num a => Nat -> Parser a
parseUNum size bits =
    trySplitAt size bits
        |> map (\(headBits, tailBits) => (go headBits 0, tailBits))
    where
        go : {a : Type} -> Num a => List Bit -> a -> a
        go [] acc = acc
        go (O :: bits) acc = go bits (2 * acc)
        go (I :: bits) acc = go bits (1 + (2 * acc))

parseUInt : Nat -> Parser Nat
parseUInt = parseUNum

-- FXME: Two's complement?
parseSInt : Nat -> Parser ZZ
parseSInt Z bits = Just (0, bits)
parseSInt (S _) [] = Nothing
parseSInt (S size) (O :: bits) = parseUInt size bits |> map (\(n, bits') => (Pos n, bits'))
parseSInt (S size) (I :: bits) = parseUInt size bits |> map (\(n, bits') => (negNat n, bits'))

parseChar : Parser Char
parseChar bits =
    parseUInt 16 bits  -- Idris' `Char`s are supposedly 2 bytes wide
        |> map (\(n, bits') => (chr (toIntNat n), bits'))

mutual
    parseVect : {n : Nat} -> (f : Format) -> Parser (Vect n (embed f))
    parseVect {n} f = rewrite plusCommutative Z n in go n []
        where
            go : {m : Nat} -> (n : Nat) -> Vect m (embed f) -> Parser (Vect (n + m) (embed f))
            go {m} Z acc bits = Just (reverse acc, bits)
            go {m} (S k) acc bits with (parse f bits)
                | Nothing = Nothing
                | Just (elem, bits'') =
                    rewrite plusSuccRightSucc k m in go k (elem :: acc) bits''

    ||| Interpret a binary format specification as a parser
    parse : (f : Format) -> Parser (embed f)
    parse FBad bits = Nothing
    parse FEnd bits = Just ((), bits)
    parse FBit bits = parseBit bits
    parse FByte bits = parseUNum 8 bits
    parse FChar bits = parseChar bits
    parse FU8 bits = parseUInt 8 bits
    parse FU16 bits = parseUInt 16 bits
    parse FU32 bits = parseUInt 32 bits
    parse FS8 bits = parseSInt 8 bits
    parse FS16 bits = parseSInt 16 bits
    parse FS32 bits = parseSInt 32 bits
    parse FRef bits = Just (bits, bits)
    parse (FPtr offset refBits f) bits with (tryDrop offset refBits)
        | Nothing = Nothing
        | Just refBits' = Just (Delay (parse f refBits' |> map fst), bits)
    parse (FVect n f) bits = parseVect f bits
    parse (FPlus f1 f2) bits with (parse f1 bits)
        | (Just (x, bits')) = Just (Left x, bits')
        | Nothing with (parse f2 bits)
            | (Just (y, bits')) = Just (Right y, bits')
            | Nothing = Nothing
    parse (FSkip f1 f2) bits with (parse f1 bits)
        | Nothing = Nothing
        | (Just (x, bits')) = parse f2 bits'
    parse (FRead f1 f2) bits with (parse f1 bits)
        | Nothing = Nothing
        | (Just (x, bits')) with (parse (f2 x) bits')
            | Nothing = Nothing
            | Just (y, bits'') = Just ((x ** y), bits'')

||| PBM binary format
pbm : Format
pbm = do
    char 'p'
    char '4'
    char ' '
    n <- FU16
    char ' '
    m <- FU16
    char '\n'
    bs <- FVect n (FVect m FBit)
    FEnd

||| Parse PBM data from a string of bits
parsePbm : Parser (embed BinaryFormats.pbm)
parsePbm = parse pbm

test : Format
test = do
    x <- FBit
    case x of
        O => FU8
        I => FS8

testPtr : Format
testPtr = do
    start <- FRef
    offset <- FU16
    ptr <- FPtr offset start <| do
        namesLen <- FU16
        names <- FVect namesLen <| do
            nameLen <- FU16
            name <- FVect nameLen FChar
            FEnd
        FEnd
    FEnd

max_stars_repo_name: brendanzab/idris-power-of-pi

max_issues_repo_name: brendanzab/idris-power-of-pi

max_forks_repo_name: brendanzab/idris-power-of-pi


text:
module Replica.App.FileSystem

import Control.App
import System.Directory
import System.Path

%default covering

public export
data FSError
  = MissingFile String
  | CantAccess String
  | CantWriteFile String
  | CantReadFile String
  | CantCreate String
  | UnmanagedError String
  | FileExists String

export total
toFSError : FileError -> String -> FSError
toFSError (GenericFileError i) = UnmanagedError
toFSError FileReadError = CantReadFile
toFSError FileWriteError = CantWriteFile
toFSError FileNotFound = MissingFile
toFSError PermissionDenied = CantAccess
toFSError FileExists = FileExists

public export
interface Exception FSError e => FileSystem e where
  createDir : (dirname : String) -> App e ()
  getCurrentDir : App e String
  changeDir : (dirname : String) -> App e ()
  removeDir : (dirname : String) -> App e ()
  writeFile : (filename : String) -> (content : String) -> App e ()
  readFile : (filename : String) -> App e String

export
Has [PrimIO, Exception FSError] e => FileSystem e where
  createDir d = do
    Right x <- primIO $ createDir d
      | Left err => throw (toFSError err d)
    pure x
  getCurrentDir = do
    Just dir <- primIO currentDir
      | Nothing => throw (UnmanagedError "current dir")
    pure dir
  changeDir d = do
    res <- primIO $ changeDir d
    if res
       then pure ()
       else throw (CantAccess d)
  removeDir d = primIO $ removeDir d
  writeFile f content = do
    case splitParent f of
      Just ("", filename) => pure ()
      Just (dir, filename) => buildDirectory dir
      Nothing => pure ()
    Right x <- primIO $ writeFile f content
      | Left err => throw (toFSError err f)
    pure x
    where
      buildDirectory : String -> App e ()
      buildDirectory dir = do
        Left _ <- primIO $ openDir dir
          | _ => pure ()
        let Just (parent, _) = splitParent dir
          | Nothing => throw (CantAccess dir)
        buildDirectory parent
        createDir dir
  readFile f = do
    Right x <- primIO $ readFile f
      | Left err => throw (toFSError err f)
    pure x

ext: idr

max_stars_repo_name: claymager/REPLica

max_issues_repo_name: claymager/REPLica

max_forks_repo_name: claymager/REPLica


text:
module RecordDoc

record A (a : Type) where
  anA : a

record Tuple (a, b : Type) where
  proj1 : a
  proj2 : b

record Singleton {0 a : Type} (v : a) where
  value : a
  0 equal : value = v


text:
import System
import System.Info

main : IO ()
main = do
  0 <- system "bash zero.sh"
    | r => do putStrLn ("expecting zero, got " ++ (show r))
              exitFailure
  -- `system` returns result of `waitpid` which is not trivial to decode
  let True = !(System.system "bash seventeen.sh") /= 0
    | False => putStrLn "expecting 17, got zero"

  let nastyStr = "Hello \"world\" $PATH %PATH% \\\" `echo 'Uh, oh'`"
  ignore $ system $ "echo " ++ escapeArg nastyStr
  ignore $ system ["echo", nastyStr]

  if not isWindows
     then do ignore $ system $ "echo " ++ escapeArg "Hello\nworld"
             ignore $ system ["echo", "Hello\nworld"]
     else do putStrLn "Hello\nworld\nHello\nworld" -- Windows has no way of escaping '\n', so skip test


text:
data DoorResult = OK | Jammed

data DoorState = DoorOpen | DoorClosed

data DoorCmd : (ty : Type) -> DoorState -> (ty -> DoorState) -> Type where
    Open : DoorCmd DoorResult DoorClosed
        (\res => case res of
            OK => DoorOpen
            Jammed => DoorClosed)
    Close : DoorCmd () DoorOpen (const DoorClosed)
    RingBell : DoorCmd () DoorClosed (const DoorClosed)

    Display : String -> DoorCmd () state (const state)

    Pure : (res : ty) -> DoorCmd ty (stateFn res) stateFn
    (>>=) : DoorCmd a state1 state2Fn ->
            ((res : a) -> DoorCmd b (state2Fn res) state3Fn) ->
            DoorCmd b state1 state3Fn

doorProg : DoorCmd () DoorClosed (const DoorClosed)
doorProg =
    do
        RingBell
        OK <- Open | Jammed => Display "Door Jammed"
        Display "Glad To Be Of Service"
        Close


text:
module Minecraft.Base.PreClassic.GrassBlock.Block

import public Minecraft.Base.PreClassic.GrassBlock
import public Minecraft.Core.Block.Export
import public Minecraft.Core.Block.Break.Export
import public Minecraft.Data.Type.Vtbl

%default total

namespace Export
  public export %hint grassBlockBlock : Block GrassBlock.Block
  public export %hint breakGrassBlock : Break GrassBlock.Block
  public export %hint grassBlockVtbl  : Vtbl  GrassBlock.Block

max_stars_repo_name: po-stulate/postulate

max_issues_repo_name: po-stulate/postulate

max_forks_repo_name: po-stulate/postulate


text:
import Command

readCmd : String -> Either String (Command a)
readCmd input = case words input of
  [] => Left "No Command"
  (cmd :: args) => Left ("Unknown Command " ++ cmd)

cmd : ConsoleIO ()
cmd = do
  PutStr "$ \n"
  input <- GetLine
  case readCmd input of
    Left err => PutStr err
    Right _ => PutStr "OK"
  cmd

-- partial
-- main : IO ()
-- main = do
--   Just score <- run forever (quiz (arithInputs (fromInteger seed)) (MkScore 0 0))
--        | Nothing => putStrLn "Out Of Fuel"

--   putStrLn ("Final Score: " ++ show score)

max_stars_repo_name: tekerson/type-driven-development

max_issues_repo_name: tekerson/type-driven-development

max_forks_repo_name: tekerson/type-driven-development


text:
myPlusCommutes: (left: Nat) -> (right: Nat) -> left + right = right + left
myPlusCommutes Z right = rewrite plusZeroRightNeutral right in Refl
myPlusCommutes (S left) right =
  rewrite myPlusCommutes left right in
  rewrite plusSuccRightSucc right left in Refl

max_stars_repo_name: coffius/idris-exercises

max_issues_repo_name: coffius/idris-exercises

max_forks_repo_name: coffius/idris-exercises


text:
> module SequentialDecisionProblems.FullTheory

> import SequentialDecisionProblems.CoreTheory

> import Sigma.Sigma
> import Sigma.Operations
> import Nat.OperationsProperties
> import Nat.Predicates
> import Nat.LTEProperties
> import Finite.Predicates
> import Finite.Properties
> import Decidable.Predicates
> import Decidable.Properties

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

* The avoidability theory:

We can build a theory of avoidability on the top of the theory of
monadic SDPs. First we have to explain what it means for a possible
future state to be avoidable. For this, we have to introduce a
reachability relation:

> ReachableFrom : State t'' -> State t -> Type
> ReachableFrom  {t'' = Z   }  {t}  x''  x  =  (t = Z ,     x = x'')
> ReachableFrom  {t'' = S t'}  {t}  x''  x  =
>   Either  (t = S t' ,  x = x'') (Sigma (State t') (\ x' => (x' `ReachableFrom` x , x' `Pred` x'')))

It is easy to show that we are indeed modeling reachability of "future"
states:

> reachableFromLemma : (x'' : State t'') -> (x : State t) -> x'' `ReachableFrom` x -> t'' `GTE` t
> reachableFromLemma {t'' = Z}     {t = Z}     x'' x prf                   = LTEZero
> reachableFromLemma {t'' = S t'}  {t = Z}     x'' x prf                   = LTEZero
> reachableFromLemma {t'' = Z}     {t = S m}   x'' x (prf1 , prf2)         = void (uninhabited (sym prf1))
> reachableFromLemma {t'' = S t'}  {t = S t'}  x'' x (Left (Refl , prf2))  = eqInLTE (S t') (S t') Refl
> reachableFromLemma {t'' = S t'}  {t = t}     x'' x (Right (MkSigma x' (prf1 , prf2)))  = s2 where
>     s1  :  t' `GTE` t
>     s1  =  reachableFromLemma x' x prf1
>     s2  :  S t' `GTE` t
>     s2  =  idSuccPreservesLTE t t' s1

Now we can explain what it means for a state |x'| to be avoidable in a
decision process starting from a previous state |x|:

> Alternative : (x : State t) -> (m : Nat) -> (x' : State t') -> (x'' : State t') -> Type
> Alternative x m x' x'' = (x'' `ReachableFrom` x , Viable m x'' , Not (x'' = x'))

> AvoidableFrom'  :  (x' : State t') -> (x : State t) -> x' `ReachableFrom` x -> Viable n x' -> Type
> AvoidableFrom' {t'} {n} x' x r v = Sigma (State t') (\ x'' => Alternative x n x' x'')

> AvoidableFrom  :  (x' : State t') -> (x : State t) -> x' `ReachableFrom` x -> (m : Nat) -> Type
> AvoidableFrom {t'} x' x r m = Sigma (State t') (\ x'' => Alternative x m x' x'')

* Decidability of |Viable|

A relevant question for applications is under which conditions
avoidability is decidable. A fundamental result is that, for a finite
type |A| and a decidable predicate |P : A -> Type|, |Sigma A P| is
decidable, see

< finiteDecSigmaLemma : {A : Type} -> {P : A -> Type} -> Finite A -> Dec1 P -> Dec (Sigma A P)

in |Finite.Properties|.

> decEqState : (x : State t) -> (x' : State t') -> Dec (x = x')

> SequentialDecisionProblems.CoreTheory.Viable {t}  Z     _  =  Unit
> SequentialDecisionProblems.CoreTheory.Viable {t} (S m)  x  =  GoodCtrl t x m

> SequentialDecisionProblems.CoreTheory.viableSpec0 _ = ()
> SequentialDecisionProblems.CoreTheory.viableSpec1 x = id
> SequentialDecisionProblems.CoreTheory.viableSpec2 x = id

> finCtrl      :  (x : State t) -> Finite (Ctrl t x)
> -- decAll       :  {A : Type} -> (P : A -> Type) -> ((a : A) -> Dec (P a)) -> (ma : M A) -> Dec (All P ma)
> -- decNotEmpty  :  {A : Type} -> (ma : M A) -> Dec (NotEmpty ma)
> decAll       :  (P : (State t) -> Type) -> ((x : State t) -> Dec (P x)) -> (mx : M (State t)) -> Dec (All P mx)
> decNotEmpty  :  (mx : M (State t)) -> Dec (NotEmpty mx)

> mutual

>   decGood  :  (x : State t) ->  (m : Nat) -> (y : Ctrl t x) -> Dec (Good t x m y)
>   decGood {t} x m y = decPair (decNotEmpty mx') (decAll (Viable m) (decViable m) mx') where
>     mx' : M (State (S t))
>     mx' = nexts t x y

>   decViable : (n : Nat) -> (x : State t) -> Dec (Viable n x)
>   decViable      Z    _ = Yes ()
>   decViable {t} (S m) x = finiteDecSigmaLemma (finCtrl x) (decGood x m)

* Decidability of |ReachableFrom|

> -- decElem : {A : Type} -> (a : A) -> (ma : M A) -> Dec (a `Elem` ma)
> decElem : (x : State t) -> (mx : M (State t)) -> Dec (x `Elem` mx)

> decPred : (x : State t) -> (x' : State (S t)) -> Dec (x `Pred` x')
> decPred {t} x x' = finiteDecSigmaLemma (finCtrl x) (\ y => decElem x' (nexts t x y))

> finState :  (t : Nat) -> Finite (State t)

> decReachableFrom : (x'' : State t'') -> (x : State t) -> Dec (x'' `ReachableFrom` x)
> decReachableFrom {t'' = Z   } {t} x'' x = decPair dp dq where
>   dp : Dec (t = Z)
>   dp = decEq t Z
>   dq : Dec (x = x'')
>   dq = decEqState x x''
> decReachableFrom {t'' = S t'} {t} x'' x = decEither dp dq where
>   dp : Dec (t = S t' , x = x'')
>   dp = decPair (decEq t (S t')) (decEqState x x'')
>   dq : Dec (Sigma (State t') (\ x' => (x' `ReachableFrom` x , x' `Pred` x'')))
>   dq = finiteDecSigmaLemma fState dRP where
>     fState  :  Finite (State t')
>     fState  =  finState t'
>     -- dRP : Dec1 (\ x' => (x' `ReachableFrom` x , x' `Pred` x''))
>     dRP : (x' : State t') -> Dec (x' `ReachableFrom` x , x' `Pred` x'')
>     dRP x' = decPair drf dpred where
>       drf    :  Dec (x' `ReachableFrom` x)
>       drf    =  decReachableFrom x' x
>       dpred  :  Dec (x' `Pred` x'')
>       dpred  =  decPred x' x''

> {-

> ---}

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
module File

-- Example of streaming from/to files.

import Streaming
import Streaming.Bytes as B
import Streaming.Char as C
import Streaming.Encoding.UTF8
import Util -- withFile

import System.File
import Data.Strings

import Data.List as L -- reverse

-------------------------------------------------
-- Streaming File Read Example
{- Here we read a file, split on newlines, split on words, reverse each word,
   unwords, unlines and spit it back out.
   This is written in a 'forward' style to follow along with the steps the
   stream takes. One could as easily use . and $ and write this in regular
   'reverse' style Idris/Haskell composition.
-}
-------------------------------------------------

export
main : IO ()
main = do
    let filename = "text.txt"
    Right res <- readFile filename
      | Left err => fileBad filename err
    putStrLn res
    B.bits8FromFile' filename
      &$ decodeUtf8
      |> encodeUtf8 -- encoding roundtripping test, temporary
      |> decodeUtf8 -- encoding roundtripping test, temporary
      |> C.lines
      |> S.mapf (C.words |> S.mapf S.rev |> C.unwords)
      |> C.unlines
      -- We collect the Chars into a String here instead of just piping them
      -- to stdout because the idris backend for printing has some issues
      -- right now with non-ascii Chars. Strings don't exhibit this issue.
      -- More directly single-Char printing uses putchar which on the c-side
      -- casts from int to char which is lossy.
      |> S.foldr strCons "" >>= putStrLn . fstOf
    pure ()
  where
    fileBad : String -> FileError -> IO ()
    fileBad fname err = printLn $ "File error: " ++ fname ++ ", " ++ show err


text:
import Data.List
import Data.Vect
import Data.String.Parser

import System.File

Vec3 : Type
Vec3 = Vect 3 Integer

minusV : Vec3 -> Vec3 -> Vec3
minusV [x1,y1,z1] [x2,y2,z2] = [x1-x2,y1-y2,z1-z2]

maxV : Vec3 -> Vec3 -> Vec3
maxV [x1,y1,z1] [x2,y2,z2] = [max x1 x2, max y1 y2, max z1 z2]

minV : Vec3 -> Vec3 -> Vec3
minV [x1,y1,z1] [x2,y2,z2] = [min x1 x2, min y1 y2, min z1 z2]

Cube : Type
Cube = (Vec3, Vec3)

isCorrect : Cube -> Maybe Cube
isCorrect c@([x1,y1,z1], [x2,y2,z2]) =
  if x1 < x2 && y1 < y2 && z1 < z2
     then Just c
     else Nothing
intersect : Cube -> Cube -> Maybe Cube
intersect (min1, max1) (min2, max2) = isCorrect (maxV min1 min2, minV max1 max2)

volume : Cube -> Integer
volume (min, max) = product $ (abs <$> minusV max min)

data Command = On Cube | Off Cube

isOn : Command -> Bool
isOn (On _) = True
isOn _ = False

invert : Command -> Command
invert (On c) = Off c
invert (Off c) = On c

getCube : Command -> Cube
getCube (On c) = c
getCube (Off c) = c

Input : Type
Input = List Command

rangeParser : Parser (Integer, Integer)
rangeParser = do skip letter
                 skip $ char '='
                 min <- integer
                 token ".."
                 max <- integer
                 pure (min, max + 1)

commandParser : Parser Command
commandParser = do cmd <- (token "on" $> On) <|> (token "off" $> Off)
                   [(xmin, xmax),(ymin,ymax),(zmin,zmax)] <- commaSep rangeParser
                     | _ => fail "no ranges"
                   pure $ cmd ([xmin,ymin,zmin],[xmax,ymax,zmax])

parser : Parser Input
parser = some (commandParser <* spaces)

Cubes : Type
Cubes = List Cube

addCube' : List Command -> Cube -> (Integer, List Command)
addCube' [] c = (0, [])
addCube' ((On c) :: cs) b = case intersect b c of
                                 Nothing => addCube' cs b
                                 (Just overlap) => let (v, os) = addCube' cs b in
                                                       (v - volume overlap, (Off overlap) :: os)
addCube' ((Off c) :: cs) b = case intersect b c of
                                  Nothing => addCube' cs b
                                  (Just overlap) => let (v, os) = addCube' cs b in
                                                       (v + volume overlap, (On overlap) :: os)

addCube : List Command -> Cube -> (Integer, List Command)
addCube cs c = case addCube' cs c of
                    (vol, []) => (vol, cs)
                    (vol, os) => (vol, os ++ cs)

doCmd : (Integer, List Command) -> Command -> (Integer, List Command)
doCmd (vol, cs) c@(On b) = let (v, cs) = addCube cs b in
                               (v + vol + volume b, c :: cs)
doCmd (vol, cs) (Off b) = mapFst ((+) vol) $ addCube cs b

cmdInBounds : Cube -> Command -> Maybe Command
cmdInBounds b (On c) = On <$> intersect b c
cmdInBounds b (Off c) = Off <$> intersect b c

part1 : Input -> IO String
part1 a = let bound : Cube = ([-50,-50,-50], [51,51,51])
              cs = catMaybes $ cmdInBounds bound <$> a in
              pure $ show $ fst $ foldl doCmd (0, []) cs

part2 : Input -> IO String
part2 a = pure $ show $ fst $ foldl doCmd (0, []) a

main : IO ()
main = do Right input <- readFile "input.txt"
            | Left err => printLn err
          Right (a, _) <- pure $ parse parser input
            | Left err => printLn err
          part1 a >>= putStrLn
          part2 a >>= putStrLn


text:
module Main

import System
import Network.Socket
import Network.Socket.Data
import Network.Socket.Raw

%cg chez libidris_net

runServer : IO (Either String (Port, ThreadID))
runServer = do
  Right sock <- socket AF_INET Stream 0
        | Left fail => pure (Left $ "Failed to open socket: " ++ show fail)
  res <- bind sock (Just (Hostname "localhost")) 0
  if res /= 0
    then pure (Left $ "Failed to bind socket with error: " ++ show res)
    else do
      port <- getSockPort sock
      res <- listen sock
      if res /= 0
        then pure (Left $ "Failed to listen on socket with error: " ++ show res)
        else do
          forked <- fork (serve port sock)
          pure $ Right (port, forked)

  where
    serve : Port -> Socket -> IO ()
    serve port sock = do
      Right (s, _) <- accept sock
        | Left err => putStrLn ("Failed to accept on socket with error: " ++ show err)
      Right  (str, _) <- recv s 1024
        | Left err => putStrLn ("Failed to accept on socket with error: " ++ show err)
      putStrLn ("Received: " ++ str)
      Right n <- send s ("echo: " ++ str)
        | Left err => putStrLn ("Server failed to send data with error: " ++ show err)
      pure ()

runClient : Port -> IO ()
runClient serverPort = do
  Right sock <- socket AF_INET Stream 0
    | Left fail => putStrLn ("Failed to open socket: " ++ show fail)
  res <- connect sock (Hostname "localhost") serverPort
  if res /= 0
    then putStrLn ("Failed to connect client to port " ++ show serverPort ++ ": " ++ show res)
    else do
      Right n <- send sock ("hello world!")
        | Left err => putStrLn ("Client failed to send data with error: " ++ show err)
      Right (str, _) <- recv sock 1024
        | Left err => putStrLn ("Client failed to receive on socket with error: " ++ show err)
      -- assuming that stdout buffers get flushed in between system calls, this is "guaranteed"
      -- to be printed after the server prints its own message
      putStrLn ("Received: " ++ str)

main : IO ()
main = do
  Right (serverPort, tid) <- runServer
    | Left err => putStrLn $ "[server] " ++ err
  runClient serverPort

max_stars_repo_name: boxfire/rapid

max_issues_repo_name: boxfire/rapid

max_forks_repo_name: boxfire/rapid


text:
module NanoParsec.Parser

import NanoParsec.MonadPlus

%access export

record Parser a where
    constructor MkParser
    parse : String -> List (a, String)

runParser : Parser a -> String -> Maybe a
runParser p st =
    case parse p st of
        [(res, "")]  => Just res
        [(_, remSt)] => Nothing
        _            => Nothing

item : Parser Char
item = MkParser $ \st =>
    case st of
        "" => []
        _  => [(strHead st, strTail st)]

implementation Functor Parser where
    map f (MkParser cs) = MkParser (\st => [(f a, b) | (a, b) <- cs st])

implementation Applicative Parser where
    pure a = MkParser (\st => [(a, st)])
    (MkParser cs1) <*> (MkParser cs2) =
        MkParser (\st => [(f a, st2) | (f, st1) <- cs1 st, (a, st2) <- cs2 st1])

implementation Monad Parser where
    p >>= f = MkParser $ \st => concatMap (\(a, st') => parse (f a) st') $ parse p st

combine : Parser a -> Parser a -> Parser a
combine p1 p2 = MkParser (\st => parse p1 st ++ parse p2 st)

failure : Parser a
failure = MkParser (\cs => [])

option : Parser a -> Parser a -> Parser a
option p1 p2 = MkParser $ \st =>
    case parse p1 st of
        []  => parse p2 st
        res => res

satisfy : (Char -> Bool) -> Parser Char
satisfy pred = item >>= \ch => if (pred ch) then (return ch) else failure

implementation MonadPlus Parser where
    mzero = failure
    mplus = option

implementation Alternative Parser where
    empty = failure
    (<|>) = option

||| Extract at least one success.
some : (Alternative f, Applicative f) => f a -> f (List a)
some v = some_v
    where
        mutual
            some_v : f (List a)
            some_v = (map (::) v) <*> many_v

            many_v : f (List a)
            many_v = some_v <|> pure []

||| Extracts 0 or more successes.
many : (Alternative f, Applicative f) => f a -> f (List a)
many v = many_v
    where
        mutual
            many_v : f (List a)
            many_v = some_v <|> pure []

            some_v : f (List a)
            some_v = (map (::) v) <*> many_v

sepBy1 : Parser a -> Parser sep -> Parser (List a)
sepBy1 p sep = do
    first     <- p
    remainder <- many (sep >>= \_ => p)
    return (first :: remainder)

sepBy : Parser a -> Parser sep -> Parser (list a)
sepBy p sep = (p `sepBy1` sep) <|> pure List.Nil

max_stars_repo_name: stallmanifold/idris-nanoparsec

max_issues_repo_name: lambdaxymox/idris-nanoparsec

max_forks_repo_name: lambdaxymox/idris-nanoparsec


text:
module Control.Monad.Coop.Sync

import Data.SortedMap

%default total

--- Stuff for runtime syncronisation between discrete events ---

export
record Sync (0 t : k) where
  constructor Sy
  unSy : Nat

export %inline
Eq (Sync sk) where
  (==) = (==) `on` unSy

export %inline
Ord (Sync sk) where
  compare = compare `on` unSy

export
newUniqueSync : SortedMap (Sync sk) whatever -> Sync sk
newUniqueSync syncs = Sy $ case unSy . fst <$> leftMost syncs of
  Nothing    => Z
  Just (S x) => x                                              -- either minimal minus 1
  Just Z     => maybe Z (S . unSy . fst) $ rightMost syncs     -- or maximal plus 1


text:
module StlcProp

import Expr
import Logic
import Maps
import Stlc

%access public export

%default total

cannonical_forms_bool : HasType Maps.empty t TyBool -> Value t ->
                        Either (t = Tru) (t = Fls)
cannonical_forms_bool (T_Var _) V_Abs impossible
cannonical_forms_bool (T_Abs _) V_Abs impossible
cannonical_forms_bool (T_App _ _) V_Abs impossible
cannonical_forms_bool T_Tru V_Abs impossible
cannonical_forms_bool T_Fls V_Abs impossible
cannonical_forms_bool (T_Test _ _ _) V_Abs impossible
cannonical_forms_bool _ V_Tru = Left Refl
cannonical_forms_bool _ V_Fls = Right Refl

cannonical_forms_fun : HasType Maps.empty t (TyArrow ty1 ty2) -> Value t ->
                       (x : Id ** u : Tm ** t = Abs x ty1 u)
cannonical_forms_fun (T_Abs {t12} ty) (V_Abs {x}) = (x ** t12 ** Refl)
cannonical_forms_fun (T_Var _) V_Tru impossible
cannonical_forms_fun (T_Abs _) V_Tru impossible
cannonical_forms_fun (T_App _ _) V_Tru impossible
cannonical_forms_fun T_Tru V_Tru impossible
cannonical_forms_fun T_Fls V_Tru impossible
cannonical_forms_fun (T_Test _ _ _) V_Tru impossible
cannonical_forms_fun (T_Var _) V_Fls impossible
cannonical_forms_fun (T_Abs _) V_Fls impossible
cannonical_forms_fun (T_App _ _) V_Fls impossible
cannonical_forms_fun T_Tru V_Fls impossible
cannonical_forms_fun T_Fls V_Fls impossible
cannonical_forms_fun (T_Test _ _ _) V_Fls impossible

progress : HasType Maps.empty t ty -> Either (Value t) (t' : Tm ** (t -+> t'))
progress (T_Var prf) = absurd prf
progress (T_Abs _) = Left V_Abs
progress (T_App ht1 ht2) = case progress ht1 of
  Left v1 => case progress ht2 of
    Left v2 => let (x ** u ** prf) = cannonical_forms_fun ht1 v1
               in rewrite prf
               in Right (subst x _ u ** ST_AppAbs v2)
    Right (t2 ** s2) => Right (App _ t2 ** ST_App2 v1 s2)
  Right (t1 ** s1) => Right (App t1 _ ** ST_App1 s1)
progress T_Tru = Left V_Tru
progress T_Fls = Left V_Fls
progress (T_Test {t2} {t3} ht1 ht2 ht3) = case progress ht1 of
  Left v1 => case cannonical_forms_bool ht1 v1 of
    Left prf => rewrite prf
                in Right (t2 ** ST_TestTru)
    Right prf => rewrite prf
                 in Right (t3 ** ST_TestFls)
  Right (t1' ** s1) => Right (Test t1' t2 t3 ** ST_Test s1)

data AppearsFreeIn : Id -> Tm -> Type where
  AFI_Var : AppearsFreeIn x (Var x)
  AFI_App1 : AppearsFreeIn x t1 -> AppearsFreeIn x (App t1 t2)
  AFI_App2 : AppearsFreeIn x t2 -> AppearsFreeIn x (App t1 t2)
  AFI_Abs : Not (y = x) -> AppearsFreeIn x t -> AppearsFreeIn x (Abs y ty t)
  AFI_Test1 : AppearsFreeIn x t1 -> AppearsFreeIn x (Test t1 t2 t3)
  AFI_Test2 : AppearsFreeIn x t2 -> AppearsFreeIn x (Test t1 t2 t3)
  AFI_Test3 : AppearsFreeIn x t3 -> AppearsFreeIn x (Test t1 t2 t3)

Closed : (t : Tm) -> Type
Closed t = (x : Id) -> Not (AppearsFreeIn x t)

free_in_context : AppearsFreeIn x t -> HasType gamma t ty ->
                  (ty' : Ty ** gamma x = Just ty')
free_in_context {ty} AFI_Var (T_Var prf) = (ty ** prf)
free_in_context (AFI_App1 afi) (T_App ht1 _) = free_in_context afi ht1
free_in_context (AFI_App2 afi) (T_App _ ht2) = free_in_context afi ht2
free_in_context {x} {gamma} (AFI_Abs contra afi) (T_Abs {ty11} ht) =
  let (ty' ** prf) = free_in_context afi ht
  in (ty' ** replace {P=\r => (if r then Just ty11 else gamma x) = Just ty'}
                     (snd beq_id_false_iff contra)
                     prf)
free_in_context (AFI_Test1 afi) (T_Test ht1 _ _) = free_in_context afi ht1
free_in_context (AFI_Test2 afi) (T_Test _ ht2 _) = free_in_context afi ht2
free_in_context (AFI_Test3 afi) (T_Test _ _ ht3) = free_in_context afi ht3

typeable_empty__closed : HasType Maps.empty t ty -> Closed t
typeable_empty__closed (T_Var prf) = absurd prf
typeable_empty__closed (T_Abs {ty11} ht) = \x, afi => case afi of
  AFI_Abs contra afi => let (ty' ** prf) = free_in_context afi ht
                        in uninhabited (replace {P=\r => (if r
                                                             then Just ty11
                                                             else Nothing)
                                                         = Just ty'}
                                                (snd beq_id_false_iff contra)
                                                prf)
typeable_empty__closed (T_App ht1 ht2) = \_, afi => case afi of
  AFI_App1 afi => let (_ ** prf) = free_in_context afi ht1
                  in uninhabited prf
  AFI_App2 afi => let (_ ** prf) = free_in_context afi ht2
                  in uninhabited prf
typeable_empty__closed T_Tru = \_, afi => case afi of
  AFI_Var impossible
  (AFI_App1 _) impossible
  (AFI_App2 _) impossible
  (AFI_Abs _ _) impossible
  (AFI_Test1 _) impossible
  (AFI_Test2 _) impossible
  (AFI_Test3 _) impossible
typeable_empty__closed T_Fls = \_, afi => case afi of
  AFI_Var impossible
  (AFI_App1 _) impossible
  (AFI_App2 _) impossible
  (AFI_Abs _ _) impossible
  (AFI_Test1 _) impossible
  (AFI_Test2 _) impossible
  (AFI_Test3 _) impossible
typeable_empty__closed (T_Test ht1 ht2 ht3) = \_, afi => case afi of
  AFI_Test1 afi => let (_ ** prf) = free_in_context afi ht1
                   in uninhabited prf
  AFI_Test2 afi => let (_ ** prf) = free_in_context afi ht2
                   in uninhabited prf
  AFI_Test3 afi => let (_ ** prf) = free_in_context afi ht3
                   in uninhabited prf

context_invariance : HasType gamma t ty ->
                     ((x : Id) -> AppearsFreeIn x t -> gamma x = gamma' x) ->
                     HasType gamma' t ty
context_invariance (T_Var {x} prf) f = T_Var (rewrite sym (f x AFI_Var) in prf)
context_invariance {gamma} {gamma'} (T_Abs {x=y} {ty11} {t12} ht) f =
  T_Abs (context_invariance ht f')
where f' : (z : Id) -> AppearsFreeIn z t12 ->
           (update y ty11 gamma) z = (update y ty11 gamma') z
      f' z afi with (decEq y z)
        f' z afi | Yes prf = rewrite snd beq_id_true_iff prf in Refl
        f' z afi | No contra = rewrite snd beq_id_false_iff contra
                               in f z (AFI_Abs contra afi)
context_invariance {gamma} {gamma'} (T_App {t1} {t2} ht1 ht2) f =
  T_App (context_invariance ht1 f1) (context_invariance ht2 f2)
where f1 : (y : Id) -> AppearsFreeIn y t1 -> gamma y = gamma' y
      f1 y afi = f y (AFI_App1 afi)
      f2 : (y : Id) -> AppearsFreeIn y t2 -> gamma y = gamma' y
      f2 y afi = f y (AFI_App2 afi)
context_invariance T_Tru _ = T_Tru
context_invariance T_Fls _ = T_Fls
context_invariance {gamma} {gamma'} (T_Test {t1} {t2} {t3} ht1 ht2 ht3) f =
  T_Test (context_invariance ht1 f1)
         (context_invariance ht2 f2)
         (context_invariance ht3 f3)
where f1 : (y : Id) -> AppearsFreeIn y t1 -> gamma y = gamma' y
      f1 y afi = f y (AFI_Test1 afi)
      f2 : (y : Id) -> AppearsFreeIn y t2 -> gamma y = gamma' y
      f2 y afi = f y (AFI_Test2 afi)
      f3 : (y : Id) -> AppearsFreeIn y t3 -> gamma y = gamma' y
      f3 y afi = f y (AFI_Test3 afi)

substitution_preserves_typing : HasType (Maps.update x ty2 gamma) t ty ->
                                HasType Maps.empty v ty2 ->
                                HasType gamma (subst x v t) ty
substitution_preserves_typing {x} {ty2} {ty} {gamma} {t = Var y} (T_Var prf) htv
  with (decEq x y)
  substitution_preserves_typing {x} {ty2} {ty} {gamma} {t = Var y}
                                (T_Var prf) htv | Yes prf' =
    let ty2_eq_ty = justInjective
                      (replace
                        {P=\r => (if r then Just ty2 else gamma y) = Just ty}
                        (snd beq_id_true_iff prf')
                        prf)
    in rewrite sym ty2_eq_ty
    in context_invariance htv (\z, afi =>
                                absurd (typeable_empty__closed htv z afi))
  substitution_preserves_typing {x} {ty2} {ty} {gamma} {t = Var y}
                                (T_Var prf) htv | No contra =
    T_Var (replace {P=\r => (if r then Just ty2 else gamma y) = Just ty}
                   (snd beq_id_false_iff contra) prf)
substitution_preserves_typing (T_App ht1 ht2) htv =
  T_App (substitution_preserves_typing ht1 htv)
        (substitution_preserves_typing ht2 htv)
substitution_preserves_typing {x} {ty2} {gamma} {t = Abs y ty t}
                              (T_Abs {ty12} ht) htv with (decEq x y)
    substitution_preserves_typing {x} {ty2} {gamma} {t = Abs y ty t}
                                  (T_Abs {ty12} ht) htv | Yes prf =
      let ht' = replace
                  {P=\r => HasType r t ty12}
                  (update_shadow {x=y} {v2=ty} {v1=ty2} {m=gamma})
                  (replace
                    {P=\r => HasType (\y1 => if beq_id y y1
                                                then Just ty
                                                else if beq_id r y1
                                                     then Just ty2
                                                     else gamma y1)
                                     t
                                     ty12}
                    prf
                    ht)
      in T_Abs ht'
    substitution_preserves_typing {x} {ty2} {gamma} {t = Abs y ty t}
                                  (T_Abs {ty12} ht) htv | No contra =
      T_Abs (substitution_preserves_typing
              (context_invariance
                ht
                (\z, afi =>
                  cong {f=\g => g z}
                       (update_permute {v1=ty} {v2=ty2} {m=gamma} contra)))
              htv)
substitution_preserves_typing T_Tru _ = T_Tru
substitution_preserves_typing T_Fls _ = T_Fls
substitution_preserves_typing (T_Test ht1 ht2 ht3) htv =
  T_Test (substitution_preserves_typing ht1 htv)
         (substitution_preserves_typing ht2 htv)
         (substitution_preserves_typing ht3 htv)

preservation : HasType Maps.empty t ty -> t -+> t' -> HasType Maps.empty t' ty
preservation (T_Var prf) _ = absurd prf
preservation (T_Abs ht) s = absurd s
preservation (T_App (T_Abs ht1) ht2) (ST_AppAbs v) =
  substitution_preserves_typing ht1 ht2
preservation (T_App ht1 ht2) (ST_App1 s1) = T_App (preservation ht1 s1) ht2
preservation (T_App ht1 ht2) (ST_App2 v1 s2) = T_App ht1 (preservation ht2 s2)
preservation T_Tru s = absurd s
preservation T_Fls s = absurd s
preservation (T_Test _ ht2 _) ST_TestTru = ht2
preservation (T_Test _ _ ht3) ST_TestFls = ht3
preservation (T_Test ht1 ht2 ht3) (ST_Test s) =
  T_Test (preservation ht1 s) ht2 ht3

subject_expansion : (  t : Tm ** t' : Tm ** ty : Ty
                    ** ( t -+> t'
                       , HasType Maps.empty t' ty
                       , Not (HasType Maps.empty t ty) ))
subject_expansion = (  App (Abs X (TyArrow TyBool TyBool) (Var X)) Tru
                    ** subst X Tru (Var X)
                    ** TyBool
                    ** ( ST_AppAbs V_Tru
                       , T_Tru
                       , \ht => case ht of
                           T_App (T_Abs (T_Var prf)) _ =>
                             uninhabited (justInjective prf) ))

Stuck : (t : Tm) -> Type
Stuck t = (NormalForm Step t, Not (Value t))

soundness : HasType Maps.empty t ty -> t -+>* t' -> Not (Stuck t')
soundness ht MultiRefl (nf, not_value) = case progress ht of
  Left v => not_value v
  Right p => nf p
soundness ht (MultiStep once next) (nf, not_value) =
  soundness (preservation ht once) next (nf, not_value)

unique_types : HasType gamma e ty -> HasType gamma e ty' -> ty = ty'
unique_types (T_Var prf1) (T_Var prf2) = justInjective (trans (sym prf1) prf2)
unique_types (T_Abs ht1) (T_Abs ht2) = rewrite unique_types ht1 ht2 in Refl
unique_types {ty} {ty'} (T_App ht1 ht2) (T_App {ty11=ty2} ht3 ht4) =
  let prf = replace {P=\r => TyArrow r ty = TyArrow ty2 ty'}
                    (unique_types ht2 ht4)
                    (unique_types ht1 ht3)
  in case prf of
    Refl => Refl
unique_types T_Tru T_Tru = Refl
unique_types T_Fls T_Fls = Refl
unique_types (T_Test _ ht1 _) (T_Test _ ht2 _) = unique_types ht1 ht2


text:
|||
module Sessions.Projection.Error

%default total

public export
data Error = InvalidBranch | Loop

-- [ EOF ]

max_stars_repo_name: DSbD-AppControl/sessions-playground

max_issues_repo_name: DSbD-AppControl/sessions-playground

max_forks_repo_name: DSbD-AppControl/sessions-playground


text:
module Ch03.Exercise_3_5_17

import Ch03.Arith

%default total

--------------------------------------------------------------------------------
-- Exercise 3.5.17
--------------------------------------------------------------------------------

||| Big step evaluation rules expressed in terms of reflexive-transitive closure
||| of small-step evaluation rules
data BInE : Term -> Term -> Type where
  BInEValue : {pf : IsValue v} -> BInE v v
  BInEIfTrue : {pf : IsValue v2} ->
               {t1, t2, t3 : Term} ->
               EvalsToStar t1 True ->
               EvalsToStar t2 v2 ->
               BInE (IfThenElse t1 t2 t3) v2
  BInEIfFalse : {pf : IsValue v3} ->
                {t1, t2, t3 : Term} ->
                EvalsToStar t1 False ->
                EvalsToStar t3 v3 ->
                BInE (IfThenElse t1 t2 t3) v3
  BInESucc : {pf : IsNumValue nv1} ->
             {t1 : Term} ->
             EvalsToStar t1 nv1 ->
             BInE (Succ t1) (Succ nv1)
  BInEPredZero : {t1 : Term} ->
                 EvalsToStar t1 Zero ->
                 BInE (Pred t1) Zero
  BInEPredSucc : {t1 : Term} ->
                 {pf : IsNumValue nv1} ->
                 EvalsToStar t1 (Succ nv1) ->
                 BInE (Pred t1) nv1
  BInEIsZeroZero : {t1 : Term} ->
                   EvalsToStar t1 Zero ->
                   BInE (IsZero t1) True
  BInEIsZeroSucc : {t1 : Term} ->
                   {pf : IsNumValue nv1} ->
                   EvalsToStar t1 (Succ nv1) ->
                   BInE (IsZero t1) False

||| Given a (one-step) derivation in the `BInE`-calculus, computes its corresponding derivation
||| in the `E`-calculus.
from_BInE_to_E : BInE t v -> EvalsToStar t v
from_BInE_to_E BInEValue = Refl
from_BInE_to_E (BInEIfTrue {t2} {t3} x y) = map {func=(\t => IfThenElse t t2 t3)} EIf x
                                            ++ Cons EIfTrue y
from_BInE_to_E (BInEIfFalse {t2} {t3} x y) = map {func=(\t => IfThenElse t t2 t3)} EIf x
                                            ++ Cons EIfFalse y
from_BInE_to_E (BInESucc x) = map ESucc x
from_BInE_to_E (BInEPredZero x) = map EPred x ++ weaken EPredZero
from_BInE_to_E (BInEPredSucc {pf} x) = map EPred x ++ weaken (EPredSucc {pf=pf})
from_BInE_to_E (BInEIsZeroZero x) = map EIsZero x ++ weaken EIsZeroZero
from_BInE_to_E (BInEIsZeroSucc {pf} x) = map EIsZero x ++ weaken (EIsZeroSucc {pf=pf})

--------------------------------------------------------------------------------
-- Sublemmas of `from_E_to_BInE`
--------------------------------------------------------------------------------

lemma_EIfTrue : {t2, t3 : Term} ->
                {pf : IsValue v} ->
                (d' : EvalsToStar t2 v) ->
                (r : BInE (IfThenElse True t2 t3) v ** Cons EIfTrue d' = from_BInE_to_E r)
lemma_EIfTrue {pf} d' = (BInEIfTrue {pf=pf} Refl d' ** Refl)

lemma_EIfFalse : {t2, t3 : Term} ->
                 {pf : IsValue v} ->
                 (d' : EvalsToStar t3 v) ->
                 (r : BInE (IfThenElse False t2 t3) v ** Cons EIfFalse d' = from_BInE_to_E r)
lemma_EIfFalse {pf} d' = (BInEIfFalse {pf=pf} Refl d' ** Refl)

lemma_EIf : {t1, t2, t3 : Term} ->
            {pf : IsValue v} ->
            {x : EvalsTo t1 t1'} ->
            (d' : EvalsToStar (IfThenElse t1' t2 t3) v) ->
            (r' : BInE (IfThenElse t1' t2 t3) v ** d' = from_BInE_to_E r') ->
            (r : BInE (IfThenElse t1 t2 t3) v ** Cons (EIf x) d' = from_BInE_to_E r)
lemma_EIf {pf} {x} d' (r' ** pf') = case r' of
                                         BInEValue {pf} => absurd (ifThenElseNotNormal pf)
                                         BInEIfTrue d1 d2 => (BInEIfTrue {pf=pf} (Cons x d1) d2 ** cong pf')
                                         BInEIfFalse d1 d2 => (BInEIfFalse {pf=pf} (Cons x d1) d2 ** cong pf')

lemma_ESucc : {t1 : Term} ->
              {pf : IsValue v} ->
              (x : EvalsTo t1 t1') ->
              (r' : BInE (Succ t1') v ** d' = from_BInE_to_E r') ->
              (r : BInE (Succ t1) v ** Cons (ESucc x) d' = from_BInE_to_E r)
lemma_ESucc {pf} x (r' ** pf') = case r' of
                                      BInEValue => case succIsValueIf pf of
                                                        nv_pf@(ConvertedFrom nv) => (BInESucc {pf=nv_pf} (weaken x) ** cong pf')
                                      BInESucc {pf} d'' => (BInESucc {pf=pf} (Cons x d'') ** cong pf')

lemma_EPred : {t1, t1' : Term} ->
              {pf : IsValue v} ->
              (x : EvalsTo t1 t1') ->
              (r' : BInE (Pred t1') v ** d' = from_BInE_to_E r') ->
              (r : BInE (Pred t1) v ** Cons (EPred x) d' = from_BInE_to_E r)
lemma_EPred {pf} x (r' ** pf') = case r' of
                                      BInEValue {pf=pf_val} => absurd (predNotValue pf_val)
                                      BInEPredZero y => (BInEPredZero (Cons x y) ** cong pf')
                                      BInEPredSucc {pf=pf_v} y => (BInEPredSucc {pf=pf_v} (Cons x y) ** cong pf')

lemma_EIsZero : {t1, t1', v : Term} ->
                {pf : IsValue v} ->
                (x : EvalsTo t1 t1') ->
                (r' : BInE (IsZero t1') v ** d' = from_BInE_to_E r') ->
                (r : BInE (IsZero t1) v ** Cons (EIsZero x) d' = from_BInE_to_E r)
lemma_EIsZero {pf} x (r' ** pf') = case r' of
                                        BInEValue {pf=pf_val} => absurd (isZeroNotValue pf_val)
                                        BInEIsZeroZero y => (BInEIsZeroZero (Cons x y) ** cong pf')
                                        BInEIsZeroSucc {pf=pf_v} y => (BInEIsZeroSucc {pf=pf_v} (Cons x y) ** cong pf')

||| Deconstructs a derivation of a term `t` to a value `v` in the `E`-calculus into a (one-step) derivation
||| in the `BInE`-calculus.
from_E_to_BInE : {pf : IsValue v} ->
                 (d : EvalsToStar t v) -> (r : BInE t v ** d = from_BInE_to_E r)
from_E_to_BInE {pf} {t = True} Refl = (BInEValue {pf=ConvertedFrom (Left True)} {v=True} ** Refl)
from_E_to_BInE {pf} {t = True} (Cons x y) = absurd (valuesDontEvaluate {pf=ConvertedFrom (Left True)} x)
from_E_to_BInE {pf} {t = False} Refl = (BInEValue {pf=ConvertedFrom (Left False)} {v=False} ** Refl)
from_E_to_BInE {pf} {t = False} (Cons x y) = absurd (valuesDontEvaluate {pf=ConvertedFrom (Left False)} x)
from_E_to_BInE {pf} {t = (IfThenElse x y z)} Refl = absurd (ifThenElseNotNormal pf)
from_E_to_BInE {pf} {t = (IfThenElse x y z)} (Cons w s) = case w of
                                                               EIfTrue => lemma_EIfTrue {pf=pf} s
                                                               EIfFalse => lemma_EIfFalse {pf=pf} s
                                                               (EIf r) => lemma_EIf {pf=pf} s (from_E_to_BInE {pf=pf} s)
from_E_to_BInE {pf} {t = Zero} d = case valuesAreNormal' {pf=ConvertedFrom (Right Zero)} d of
                                        Refl => case d of
                                                     Refl => (BInEValue {pf=ConvertedFrom (Right Zero)} ** Refl)
                                                     (Cons x y) => absurd (valuesDontEvaluate {pf=ConvertedFrom (Right Zero)} x)
from_E_to_BInE {pf} {t = (Succ x)} Refl = case succIsValueIf pf of
                                               ConvertedFrom nv => (BInEValue {pf=ConvertedFrom (Right (Succ nv))} ** Refl)
from_E_to_BInE {pf} {t = (Succ x)} (Cons y z) = case y of
                                                     ESucc y' => lemma_ESucc {pf=pf} y' (from_E_to_BInE {pf=pf} z)
from_E_to_BInE {pf} {t = (Pred x)} Refl = absurd (predNotValue pf)
from_E_to_BInE {pf} {t = (Pred x)} (Cons y z) = case y of
                                                     EPredZero => case valuesAreNormal {pf=ConvertedFrom (Right Zero)} z of
                                                                       Refl => (BInEPredZero Refl ** Refl)
                                                     EPredSucc {nv1} {pf=pf_nv} => case valuesAreNormal {pf=numValueIsValue pf_nv} z of
                                                                                Refl => (BInEPredSucc {pf=pf_nv} Refl ** Refl)
                                                     EPred y' => lemma_EPred {pf=pf} y' (from_E_to_BInE {pf=pf} z)
from_E_to_BInE {pf} {t = (IsZero x)} Refl = absurd (isZeroNotValue pf)
from_E_to_BInE {pf} {t = (IsZero x)} (Cons y z) = case y of
                                                       EIsZeroZero => case valuesAreNormal {pf=ConvertedFrom (Left True)} z of
                                                                           Refl => (BInEIsZeroZero Refl ** Refl)
                                                       EIsZeroSucc => case valuesAreNormal {pf=ConvertedFrom (Left False)} z of
                                                                           Refl => (BInEIsZeroSucc Refl ** Refl)
                                                       EIsZero y' => lemma_EIsZero {pf=pf} y' (from_E_to_BInE {pf=pf} z)

||| Converts a derivation in `BInE`-calculus to a derivation in the `B`-calculus.
from_BInE_to_B : {pf : IsValue v} -> BInE t v -> BigEvalsTo t v
from_BInE_to_B {pf} BInEValue = BValue {pf=pf}
from_BInE_to_B {pf} (BInEIfTrue y z) = let pf_true = ConvertedFrom (Left True)
                                           y' = fst (from_E_to_BInE {pf=pf_true} y)
                                           z' = fst (from_E_to_BInE {pf=pf} z) in
                                           BIfTrue {pf=pf} (from_BInE_to_B {pf=pf_true} y') (from_BInE_to_B {pf=pf} z')
from_BInE_to_B {pf} (BInEIfFalse y z) = let pf_false = ConvertedFrom (Left False)
                                            y' = fst (from_E_to_BInE {pf=pf_false} y)
                                            z' = fst (from_E_to_BInE {pf=pf} z) in
                                            BIfFalse {pf=pf} (from_BInE_to_B {pf=pf_false} y') (from_BInE_to_B {pf=pf} z')
from_BInE_to_B {pf} (BInESucc {pf=pf_nv} y) = let y' = fst (from_E_to_BInE {pf=numValueIsValue pf_nv} y) in
                                                  BSucc {pf=pf_nv} (from_BInE_to_B {pf=numValueIsValue pf_nv} y')
from_BInE_to_B {pf} (BInEPredZero x) = let pf_zero = ConvertedFrom (Right Zero)
                                           x' = fst (from_E_to_BInE {pf=pf_zero} x) in
                                           BPredZero (from_BInE_to_B {pf=pf_zero} x')
from_BInE_to_B {pf} (BInEPredSucc {pf=pf_v} y) = let pf_succ = numValueIsValue (succNumValueIsNumValue pf_v)
                                                     y' = fst (from_E_to_BInE {pf=pf_succ} y) in
                                                     BPredSucc {pf=pf_v} (from_BInE_to_B {pf=pf_succ} y')
from_BInE_to_B {pf} (BInEIsZeroZero x) = let pf_zero = ConvertedFrom (Right Zero)
                                             x' = fst (from_E_to_BInE {pf=pf_zero} x) in
                                             BIsZeroZero (from_BInE_to_B {pf=pf_zero} x')
from_BInE_to_B {pf} (BInEIsZeroSucc {pf=pf_v} y) = let pf_succ = numValueIsValue (succNumValueIsNumValue pf_v)
                                                       y' = fst (from_E_to_BInE {pf=pf_succ} y) in
                                                       BIsZeroSucc {pf=pf_v} (from_BInE_to_B {pf=pf_succ} y')

||| Proof that if a term `t` evaluates to a value `v` under the reflexive transitive
||| closure of the small-step evaluation rules, then it also evaluates to it under the
||| big-step evaluation rules.
starImpliesBig : {pf : IsValue v} -> EvalsToStar t v -> BigEvalsTo t v
starImpliesBig {pf} d = from_BInE_to_B {pf=pf} (fst (from_E_to_BInE {pf=pf} d))

||| Proof that if a term `t` evaluates to a value `v` under the big-step evaluation rules,
||| then it also evaluates to it under the reflexive transitive closure of the small-step
||| rules.
bigImpliesStar : {pf : IsValue v} -> BigEvalsTo t v -> EvalsToStar t v
bigImpliesStar {pf} BValue = Refl
bigImpliesStar {pf} (BIfTrue y z) = let y' = bigImpliesStar {pf=ConvertedFrom (Left True)} y
                                        z' = bigImpliesStar {pf=pf} z in
                                        from_BInE_to_E (BInEIfTrue {pf=pf} y' z')
bigImpliesStar {pf} (BIfFalse y z) = let y' = bigImpliesStar {pf=ConvertedFrom (Left False)} y
                                         z' = bigImpliesStar {pf=pf} z in
                                         from_BInE_to_E (BInEIfFalse {pf=pf} y' z')
bigImpliesStar {pf} (BSucc {pf=pf_nv} y) = let y' = bigImpliesStar {pf=numValueIsValue pf_nv} y in
                                               from_BInE_to_E (BInESucc {pf=pf_nv} y')
bigImpliesStar {pf} (BPredZero x) = let x' = bigImpliesStar {pf=pf} x in
                                        from_BInE_to_E (BInEPredZero x')
bigImpliesStar {pf} (BPredSucc {pf=pf_nv} y) = let y' = bigImpliesStar {pf=numValueIsValue (succNumValueIsNumValue pf_nv)} y in
                                                   from_BInE_to_E (BInEPredSucc {pf=pf_nv} y')
bigImpliesStar {pf} (BIsZeroZero x) = let x' = bigImpliesStar {pf=ConvertedFrom (Right Zero)} x in
                                          from_BInE_to_E (BInEIsZeroZero x')
bigImpliesStar {pf} (BIsZeroSucc {pf=pf_nv} y) = let y' = bigImpliesStar {pf=numValueIsValue (succNumValueIsNumValue pf_nv)} y in
                                                     from_BInE_to_E (BInEIsZeroSucc {pf=pf_nv} y')

max_stars_repo_name: mr-infty/tapl

max_issues_repo_name: mr-infty/tapl

max_forks_repo_name: mr-infty/tapl


text:
fib : HasIO io => Integer -> io Integer
fib 0 = pure 0
fib 1 = pure 1
fib n = pure $ !(fib (n - 1)) + !(fib (n - 2))

main : IO ()
main =  do
  value <- getLine
  printLn !(fib (cast value))


text:
tupleBug : Pair () a -> ()
tupleBug (_, (_, _)) = ()

odd : a -> Bool
odd () = False


text:
import Aoc
import Data.List
import Data.List1
import Data.SortedMap as M
%default total

-- Return pairwise deltas between elements of a list.
deltas : List1 Integer -> List Integer
deltas (x:::xs) = zipWith (-) xs (x::xs)

-- Index into a map, returning 0 for a missing key.
(!.) : M.SortedMap k Integer -> k -> Integer
(!.) m k = maybe 0 id (M.lookup k m)
infixr 10 !.

-- Given the sorted "init" adapters and the "final" adapters,
-- count possible paths from 0 to final.
countPaths : List1 Integer -> Integer -> Integer
countPaths initAdapters final =
  -- let's do some ~dynamic programming~ with foldr and a map
  let m0 = M.singleton final 1
      f = (\k, m => M.insert k (m!.(k+1) + m!.(k+2) + m!.(k+3)) m)
  in foldr f m0 initAdapters !. 0

main : IO ()
main = do
  ns <- readIntegerLines {a=Integer}
  let sorted = sort ns
  let initAdapters = 0 ::: sorted
  let final = last initAdapters + 3
  let adapters = 0 ::: (sorted ++ [final])
  let ds = deltas adapters
  putStr "*   "; printLn $ count (==1) ds * count (==3) ds
  putStr "**  "; printLn $ countPaths initAdapters final


text:
module Main

import Test.Pipes

export
main : IO ()
main = run_tests

max_stars_repo_name: QuentinDuval/IdrisPipes

max_issues_repo_name: QuentinDuval/IdrisPipes

max_forks_repo_name: QuentinDuval/IdrisPipes


text:
module xquant.Math.Hilbert

import xquant.Core.Types
import Data.Matrix
import Data.Complex

-- Normalize
normalize : StateSpace n Float -> StateSpace n Float
normalize q = map (\(r :+ i) => (r / (sqrt sqn)) :+ (i / (sqrt sqn))) q where
   sqn : Double
   sqn = sum $ map ((\x => x*x) . magnitude) q

conjugate : (Num a , Neg a) => Complex a -> Complex a
conjugate (r :+ i) = r :+ -i

-- Infix Hilbert inner product
--   should be more general, but no official declaration for Num a => Num (Complex a)
||| Hilbert Inner product
(<|>) : StateSpace n Float -> StateSpace n Float -> Complex Float
(<|>) q w = sum $ zipWith (*) (map Complex.conjugate q) w

-- Hermitian conjugate (adjoint) on complex matrices
dagger : (Num a , Neg a) => Matrix n m (Complex a) -> Matrix m n (Complex a)
dagger h = map (map Hilbert.conjugate) $ transpose h

-- Complex number divide
(/) : Complex Float -> Complex Float -> Complex Float
(/) (a:+b) (c:+d) = let real = (a*c+b*d)/(c*c+d*d)
                        imag = (b*c-a*d)/(c*c+d*d)
                    in  (real :+ imag)

max_stars_repo_name: BlackBrane/xquant

max_issues_repo_name: fieldstrength/xquant

max_forks_repo_name: fieldstrength/xquant


text:
> module NonNegDouble.LTEProperties

> import NonNegDouble.NonNegDouble
> import NonNegDouble.Constants
> import NonNegDouble.Predicates
> import NonNegDouble.BasicOperations
> import NonNegDouble.Operations
> import NonNegDouble.Properties
> import Double.Predicates
> import Double.Postulates
> import Double.Properties
> import Rel.TotalPreorder

> %default total
> %access public export

* |LTE| is a total preorder:

> ||| LTE is reflexive
> reflexiveLTE : (x : NonNegDouble) -> x `LTE` x
> reflexiveLTE x = reflexiveLTE (toDouble x)

> ||| LTE is transitive
> transitiveLTE : (x, y, z : NonNegDouble) -> x `LTE` y -> y `LTE` z -> x `LTE` z
> transitiveLTE x y z xLTEy yLTEz = transitiveLTE (toDouble x) (toDouble y) (toDouble z) xLTEy yLTEz

> ||| LTE is total
> totalLTE : (x, y : NonNegDouble) -> Either (x `LTE` y) (y `LTE` x)
> totalLTE x y = totalLTE (toDouble x) (toDouble y)

> ||| LTE is a total preorder
> totalPreorderLTE : TotalPreorder NonNegDouble.Predicates.LTE
> totalPreorderLTE = MkTotalPreorder LTE reflexiveLTE transitiveLTE totalLTE

* Properties of |LTE| and |plus|:

> using implementation NumNonNegDouble
>   ||| LTE is monotone w.r.t. `(+)`
>   monotonePlusLTE : {a, b, c, d : NonNegDouble} ->
>                     a `LTE` b -> c `LTE` d -> (a + c) `LTE` (b + d)
>   monotonePlusLTE {a} {b} {c} {d} aLTEb cLTEd = s3 where
>     s1 : (toDouble a) + (toDouble c) `LTE` (toDouble b) + (toDouble d)
>     s1 = monotonePlusLTE {a = toDouble a} {b = toDouble b} {c = toDouble c} {d = toDouble d} aLTEb cLTEd
>     s2 : toDouble (a + c) `LTE` (toDouble b) + (toDouble d)
>     s2 = replace {P = \ X => X `LTE` (toDouble b) + (toDouble d)} (sym (toDoublePlusLemma a c)) s1
>     s3 : toDouble (a + c) `LTE` toDouble (b + d)
>     s3 = replace {P = \ X => toDouble (a + c) `LTE` X} (sym (toDoublePlusLemma b d)) s2

* Properties of |LTE| and |mult|:

> using implementation NumNonNegDouble
>   ||| LTE is monotone w.r.t. `(*)`
>   monotoneMultLTE : {a, b, c, d : NonNegDouble} ->
>                     a `LTE` b -> c `LTE` d -> (a * c) `LTE` (b * d)
>   monotoneMultLTE {a} {b} {c} {d} aLTEb cLTEd = s3 where
>     s1 : (toDouble a) * (toDouble c) `LTE` (toDouble b) * (toDouble d)
>     s1 = monotoneMultLTE {a = toDouble a} {b = toDouble b} {c = toDouble c} {d = toDouble d} aLTEb cLTEd
>     s2 : toDouble (a * c) `LTE` (toDouble b) * (toDouble d)
>     s2 = replace {P = \ X => X `LTE` (toDouble b) * (toDouble d)} (sym (toDoubleMultLemma a c)) s1
>     s3 : toDouble (a * c) `LTE` toDouble (b * d)
>     s3 = replace {P = \ X => toDouble (a * c) `LTE` X} (sym (toDoubleMultLemma b d)) s2

* Properties of |LTE| and |sum|:

> using implementation NumNonNegDouble
>   ||| |sum| is monotone
>   monotoneSum : {A : Type} ->
>                 (f : A -> NonNegDouble) -> (g : A -> NonNegDouble) ->
>                 (p : (a : A) -> f a `LTE` g a) ->
>                 (as : List A) ->
>                 sum (map f as) `LTE` sum (map g as)
>   monotoneSum f g p Nil = reflexiveLTE 0.0
>   monotoneSum f g p (a :: as) =
>     monotonePlusLTE {a = f a} {b = g a} {c = sum (map f as)} {d = sum (map g as)} (p a) (monotoneSum f g p as)

> {-

> ---}


text:
module Basic

infixl 0 $

%inline public export
($) : (a -> b) -> a -> b
($) f x = f x

public export
the : (a : Type) -> (x : a) -> a
the _ x = x

public export
id : a -> a
id x = x

public export
const : a -> b -> a
const x _ = x

infixl 1 .
infixl 1 `compose`

||| In the stdlib it is the (.) operator.
public export
compose : (b -> c) -> (a -> b) -> a -> c
compose f g x = f (g x)

||| Instead of going via the stdlib route of naming conventions,
||| we choose the (.) operator to denote the dependent function
||| composition. Also note that the order of the operands is reversed.
public export
(.) : {p : a -> Type}
   -> (f : (x : a) -> p x)
   -> {q : {x : a} -> p x -> Type}
   -> (g : {x : a} -> (y : p x) -> q {x} y)
   -> ((x : a) -> q {x} (f x))
f . g = \x => g (f x)

public export
domain : {a : Type} -> (a -> b) -> Type
domain _ = a

public export
codomain : {b : Type} -> (a -> b) -> Type
codomain _ = b

public export
typeOf : {a : Type} -> a -> Type
typeOf _ = a


text:
import Data.String

Interpolation Bool where
  interpolate True = "TT"
  interpolate False = "FF"

Interpolation Nat where
  interpolate Z = "0"
  interpolate (S n) = "S \{n}"

Interpolation Integer where
  interpolate = show

test : String
test = "\{2}\{True}: \{True}\{True}"


text:
module Data.Trifunctor

%default total
%access public export

||| Trifunctor is abstraction over type with 3 type parameters
||| Progression of abstractions: Functor => Bifunctor => Trifunctor
interface Trifunctor (t : Type -> Type -> Type -> Type) where
  timap : (r -> rr) -> (e -> ee) -> (a -> aa) -> t r e a -> t rr ee aa

  bimap : (e -> ee) -> (a -> aa) -> t r e a -> t r ee aa
  bimap = timap id

  map : (a -> aa) -> t r e a -> t r e aa
  map = timap id id

  mapLeft : (e -> ee) -> t r e a -> t r ee a
  mapLeft e = timap id e id

max_stars_repo_name: lemastero/Idris-Trifunctors

max_issues_repo_name: lemastero/Idris-Trifunctors

max_forks_repo_name: lemastero/Idris-Trifunctors


text:
module Text.CSS.Color

import Data.Maybe
import Text.CSS.Percentage
import Text.CSS.Render

%default total

--------------------------------------------------------------------------------
--          Color
--------------------------------------------------------------------------------

public export
data Color : Type where
  RGBA : (red,green,blue : Bits8) -> (transparency : Percentage) -> Color
  HSLA : (hue : Double) -> (sat,light,transparency : Percentage) -> Color

public export %inline
rgb : (red,green,blue : Bits8) -> Color
rgb r g b = RGBA r g b 100

public export %inline
hsl : (hue : Double) -> (sat,light : Percentage) -> Color
hsl h s l = HSLA h s l 100

public export
transparent : Color
transparent = RGBA 0 0 0 0

export
Render Color where
  render (RGBA r g b a) = "rgba(\{show r},\{show g},\{show b},\{render a})"
  render (HSLA h s l a) = "hsla(\{show h},\{render s},\{render l},\{render a})"

export
Show Color where show = render

--------------------------------------------------------------------------------
--          X11 Colors (https://www.w3.org/TR/css3-color/#svg-color)
--------------------------------------------------------------------------------

export
aliceblue : Color
aliceblue = rgb 240 248 255

export
antiquewhite : Color
antiquewhite = rgb 250 235 215

export
aqua : Color
aqua = rgb 0 255 255

export
aquamarine : Color
aquamarine = rgb 127 255 212

export
azure : Color
azure = rgb 240 255 255

export
beige : Color
beige = rgb 245 245 220

export
bisque : Color
bisque = rgb 255 228 196

export
blanchedalmond : Color
blanchedalmond = rgb 255 235 205

export
black : Color
black = rgb 0 0 0

export
blue : Color
blue = rgb 0 0 255

export
blueviolet : Color
blueviolet = rgb 138 43 226

export
brown : Color
brown = rgb 165 42 42

export
burlywood : Color
burlywood = rgb 222 184 135

export
cadetblue : Color
cadetblue = rgb 95 158 160

export
chartreuse : Color
chartreuse = rgb 127 255 0

export
chocolate : Color
chocolate = rgb 210 105 30

export
coral : Color
coral = rgb 255 127 80

export
cornflowerblue : Color
cornflowerblue = rgb 100 149 237

export
cornsilk : Color
cornsilk = rgb 255 248 220

export
crimson : Color
crimson = rgb 220 20 60

export
cyan : Color
cyan = rgb 0 255 255

export
darkblue : Color
darkblue = rgb 0 0 139

export
darkcyan : Color
darkcyan = rgb 0 139 139

export
darkgoldenrod : Color
darkgoldenrod = rgb 184 134 11

export
darkgray : Color
darkgray = rgb 169 169 169

export
darkgreen : Color
darkgreen = rgb 0 100 0

export
darkgrey : Color
darkgrey = rgb 169 169 169

export
darkkhaki : Color
darkkhaki = rgb 189 183 107

export
darkmagenta : Color
darkmagenta = rgb 139 0 139

export
darkolivegreen : Color
darkolivegreen = rgb 85 107 47

export
darkorange : Color
darkorange = rgb 255 140 0

export
darkorchid : Color
darkorchid = rgb 153 50 204

export
darkred : Color
darkred = rgb 139 0 0

export
darksalmon : Color
darksalmon = rgb 233 150 122

export
darkseagreen : Color
darkseagreen = rgb 143 188 143

export
darkslateblue : Color
darkslateblue = rgb 72 61 139

export
darkslategray : Color
darkslategray = rgb 47 79 79

export
darkslategrey : Color
darkslategrey = rgb 47 79 79

export
darkturquoise : Color
darkturquoise = rgb 0 206 209

export
darkviolet : Color
darkviolet = rgb 148 0 211

export
deeppink : Color
deeppink = rgb 255 20 147

export
deepskyblue : Color
deepskyblue = rgb 0 191 255

export
dimgray : Color
dimgray = rgb 105 105 105

export
dimgrey : Color
dimgrey = rgb 105 105 105

export
dodgerblue : Color
dodgerblue = rgb 30 144 255

export
firebrick : Color
firebrick = rgb 178 34 34

export
floralwhite : Color
floralwhite = rgb 255 250 240

export
forestgreen : Color
forestgreen = rgb 34 139 34

export
fuchsia : Color
fuchsia = rgb 255 0 255

export
gainsboro : Color
gainsboro = rgb 220 220 220

export
ghostwhite : Color
ghostwhite = rgb 248 248 255

export
gold : Color
gold = rgb 255 215 0

export
goldenrod : Color
goldenrod = rgb 218 165 32

export
gray : Color
gray = rgb 128 128 128

export
green : Color
green = rgb 0 128 0

export
greenyellow : Color
greenyellow = rgb 173 255 47

export
grey : Color
grey = rgb 128 128 128

export
honeydew : Color
honeydew = rgb 240 255 240

export
hotpink : Color
hotpink = rgb 255 105 180

export
indianred : Color
indianred = rgb 205 92 92

export
indigo : Color
indigo = rgb 75 0 130

export
ivory : Color
ivory = rgb 255 255 240

export
khaki : Color
khaki = rgb 240 230 140

export
lavender : Color
lavender = rgb 230 230 250

export
lavenderblush : Color
lavenderblush = rgb 255 240 245

export
lawngreen : Color
lawngreen = rgb 124 252 0

export
lemonchiffon : Color
lemonchiffon = rgb 255 250 205

export
lightblue : Color
lightblue = rgb 173 216 230

export
lightcoral : Color
lightcoral = rgb 240 128 128

export
lightcyan : Color
lightcyan = rgb 224 255 255

export
lightgoldenrodyellow : Color
lightgoldenrodyellow = rgb 250 250 210

export
lightgray : Color
lightgray = rgb 211 211 211

export
lightgreen : Color
lightgreen = rgb 144 238 144

export
lightgrey : Color
lightgrey = rgb 211 211 211

export
lightpink : Color
lightpink = rgb 255 182 193

export
lightsalmon : Color
lightsalmon = rgb 255 160 122

export
lightseagreen : Color
lightseagreen = rgb 32 178 170

export
lightskyblue : Color
lightskyblue = rgb 135 206 250

export
lightslategray : Color
lightslategray = rgb 119 136 153

export
lightslategrey : Color
lightslategrey = rgb 119 136 153

export
lightsteelblue : Color
lightsteelblue = rgb 176 196 222

export
lightyellow : Color
lightyellow = rgb 255 255 224

export
lime : Color
lime = rgb 0 255 0

export
limegreen : Color
limegreen = rgb 50 205 50

export
linen : Color
linen = rgb 250 240 230

export
magenta : Color
magenta = rgb 255 0 255

export
maroon : Color
maroon = rgb 128 0 0

export
mediumaquamarine : Color
mediumaquamarine = rgb 102 205 170

export
mediumblue : Color
mediumblue = rgb 0 0 205

export
mediumorchid : Color
mediumorchid = rgb 186 85 211

export
mediumpurple : Color
mediumpurple = rgb 147 112 219

export
mediumseagreen : Color
mediumseagreen = rgb 60 179 113

export
mediumslateblue : Color
mediumslateblue = rgb 123 104 238

export
mediumspringgreen : Color
mediumspringgreen = rgb 0 250 154

export
mediumturquoise : Color
mediumturquoise = rgb 72 209 204

export
mediumvioletred : Color
mediumvioletred = rgb 199 21 133

export
midnightblue : Color
midnightblue = rgb 25 25 112

export
mintcream : Color
mintcream = rgb 245 255 250

export
mistyrose : Color
mistyrose = rgb 255 228 225

export
moccasin : Color
moccasin = rgb 255 228 181

export
navajowhite : Color
navajowhite = rgb 255 222 173

export
navy : Color
navy = rgb 0 0 128

export
oldlace : Color
oldlace = rgb 253 245 230

export
olive : Color
olive = rgb 128 128 0

export
olivedrab : Color
olivedrab = rgb 107 142 35

export
orange : Color
orange = rgb 255 165 0

export
orangered : Color
orangered = rgb 255 69 0

export
orchid : Color
orchid = rgb 218 112 214

export
palegoldenrod : Color
palegoldenrod = rgb 238 232 170

export
palegreen : Color
palegreen = rgb 152 251 152

export
paleturquoise : Color
paleturquoise = rgb 175 238 238

export
palevioletred : Color
palevioletred = rgb 219 112 147

export
papayawhip : Color
papayawhip = rgb 255 239 213

export
peachpuff : Color
peachpuff = rgb 255 218 185

export
peru : Color
peru = rgb 205 133 63

export
pink : Color
pink = rgb 255 192 203

export
plum : Color
plum = rgb 221 160 221

export
powderblue : Color
powderblue = rgb 176 224 230

export
purple : Color
purple = rgb 128 0 128

export
red : Color
red = rgb 255 0 0

export
rosybrown : Color
rosybrown = rgb 188 143 143

export
royalblue : Color
royalblue = rgb 65 105 225

export
saddlebrown : Color
saddlebrown = rgb 139 69 19

export
salmon : Color
salmon = rgb 250 128 114

export
sandybrown : Color
sandybrown = rgb 244 164 96

export
seagreen : Color
seagreen = rgb 46 139 87

export
seashell : Color
seashell = rgb 255 245 238

export
sienna : Color
sienna = rgb 160 82 45

export
silver : Color
silver = rgb 192 192 192

export
skyblue : Color
skyblue = rgb 135 206 235

export
slateblue : Color
slateblue = rgb 106 90 205

export
slategray : Color
slategray = rgb 112 128 144

export
slategrey : Color
slategrey = rgb 112 128 144

export
snow : Color
snow = rgb 255 250 250

export
springgreen : Color
springgreen = rgb 0 255 127

export
steelblue : Color
steelblue = rgb 70 130 180

export
tan : Color
tan = rgb 210 180 140

export
teal : Color
teal = rgb 0 128 128

export
thistle : Color
thistle = rgb 216 191 216

export
tomato : Color
tomato = rgb 255 99 71

export
turquoise : Color
turquoise = rgb 64 224 208

export
violet : Color
violet = rgb 238 130 238

export
wheat : Color
wheat = rgb 245 222 179

export
white : Color
white = rgb 255 255 255

export
whitesmoke : Color
whitesmoke = rgb 245 245 245

export
yellow : Color
yellow = rgb 255 255 0

export
yellowgreen : Color
yellowgreen = rgb 154 205 50


text:
import Data.Vect

insert : Ord elem =>
         (x : elem) -> (xsSorted : Vect len elem) -> Vect (S len) elem
insert x [] = [x]
insert x (y :: xs) = case x < y of
                          False => y :: insert x xs
                          True => x :: y :: xs

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

max_stars_repo_name: DimaSamoz/idris-book

max_issues_repo_name: DimaSamoz/idris-book

max_forks_repo_name: DimaSamoz/idris-book


text:
module IdrisScript.Objects.Unpacked

import IdrisScript

%access public export

setProperty : ToJS from to
           => String
           -> from
           -> JSValue (JSObject c)
           -> JS_IO (JSValue (JSObject c))
setProperty {from} {to} prop val obj = do
  jscall "%0[%1] = %2" (Ptr -> String -> Ptr -> JS_IO Ptr)
         (unpack obj) prop (unpack (toJS {from}{to} val))
  pure obj

max_stars_repo_name: jimmyhmiller/IdrisScript

max_issues_repo_name: jimmyhmiller/IdrisScript

max_forks_repo_name: jimmyhmiller/IdrisScript


text:
module GridSDL

import Effects
import Effect.SDL
import Effect.State

import Grid

%access public export

gray : Colour
gray = MkCol 128 128 128 255

record Config where
    constructor MkConfig
    width, height : Int

%name Config config

record GridWindow where
    constructor MkGridWindow
    leftX, topX, columnN, rowN : Int

mouseToPoint : (Int, Int) -> Config -> GridWindow -> Point
mouseToPoint (x, y) config (MkGridWindow wLeft wTop wColumnN wRowN) =
    ((x * wColumnN `div` width config) + wLeft, (y * wRowN `div` height config) + wTop)

drawGrid : Config -> GridWindow -> Grid -> Eff () [SDL_ON]
drawGrid (MkConfig width height) (MkGridWindow wLeft wTop wColumnN wRowN) grid = do
    mapE (\column => drawColumn column) [(wLeft + 1) .. (wLeft + wColumnN)]
    pure ()
  where
    cellWidth : Int
    cellWidth = width `div` wColumnN

    cellHeight : Int
    cellHeight = height `div` wRowN

    cellMargin : Int
    cellMargin = 1

    --lifeMargin : Int
    --lifeMargin = 1 + cellMargin

    drawCell : Int -> Int -> Eff () [SDL_ON]
    drawCell column row =
        let left = width * (column - wLeft - 1) `div` wColumnN
            top = height * (row - wTop - 1) `div` wRowN
        in do
            rectangle gray (left) (top) (cellWidth) (cellHeight)
            when (inBounds (column - 1, row - 1) grid) $ rectangle
                    (if (containsLife (column - 1, row - 1) grid) then white else black)
                    (left + cellMargin) (top + cellMargin)
                    (cellWidth - 2 * cellMargin) (cellHeight - 2 * cellMargin)

            --rectangle gray (left + cellMargin) (top + cellMargin)
            --        (cellWidth - 2 * cellMargin) (cellHeight - 2 * cellMargin)
            --when (containsLife (column - 1, row - 1) grid) $ rectangle red
            --        (left + lifeMargin) (top + lifeMargin)
            --        (cellWidth - 2 * lifeMargin) (cellHeight - 2 * lifeMargin)

            --when (containsLife (column - 1, row - 1) grid) $ rectangle white
            --        (left + cellMargin) (top + cellMargin)
            --        (cellWidth - 2 * cellMargin) (cellHeight - 2 * cellMargin)

    drawColumn : Int -> Eff () [SDL_ON]
    drawColumn column = mapE (\row => drawCell column row) [(wTop + 1) .. (wTop + wRowN)] *> pure ()

max_stars_repo_name: artemohanjanyan/game-of-life

max_issues_repo_name: artemohanjanyan/game-of-life

max_forks_repo_name: artemohanjanyan/game-of-life


text:
module WebAssembly.Structure.Values

import public WebAssembly.Structure.Values.Bytes
import public WebAssembly.Structure.Values.Integers
import public WebAssembly.Structure.Values.FloatingPoint
import public WebAssembly.Structure.Values.Names

max_stars_repo_name: RaoulSchaffranek/idris-webassembly

max_issues_repo_name: RaoulSchaffranek/idris-webassembly

max_forks_repo_name: RaoulSchaffranek/idris-webassembly


text:
module System.Errno

import System.FFI

%default total

%foreign "C:idris2_getErrno, libidris2_support, idris_support.h"
         jvm' runtimeClass "getErrorNumber" "java/lang/Object" "int"
prim__getErrno : PrimIO Int

%foreign "C:idris2_strerror, libidris2_support, idris_support.h"
         "node:lambda:errno=>'Error code: '+errno"
         jvm' runtimeClass "getErrorMessage" "int" "String"
prim__strerror : Int -> PrimIO String

||| Fetch libc `errno` global variable.
export
getErrno : HasIO io => io Int
getErrno = primIO prim__getErrno

||| Convert numeric `errno` to string.
export
strerror : Int -> String
strerror errno = unsafePerformIO $ primIO $ prim__strerror errno


text:
module Web.Internal.AnimationTypes

import JS

--------------------------------------------------------------------------------
--          Enums
--------------------------------------------------------------------------------

namespace AnimationPlayState

  public export
  data AnimationPlayState = Idle | Running | Paused | Finished

  public export
  Show AnimationPlayState where
    show Idle = "idle"
    show Running = "running"
    show Paused = "paused"
    show Finished = "finished"

  public export
  Eq AnimationPlayState where
    (==) = (==) `on` show

  public export
  Ord AnimationPlayState where
    compare = compare `on` show

  public export
  read : String -> Maybe AnimationPlayState
  read "idle" = Just Idle
  read "running" = Just Running
  read "paused" = Just Paused
  read "finished" = Just Finished
  read _ = Nothing

  public export
  fromString :  (s : String)
             -> {auto 0 _ : IsJust (AnimationPlayState.read s)}
             -> AnimationPlayState
  fromString s = fromJust $ read s

  export
  ToFFI AnimationPlayState String where
    toFFI = show

  export
  FromFFI AnimationPlayState String where
    fromFFI = read

namespace FillMode

  public export
  data FillMode = None | Forwards | Backwards | Both | Auto

  public export
  Show FillMode where
    show None = "none"
    show Forwards = "forwards"
    show Backwards = "backwards"
    show Both = "both"
    show Auto = "auto"

  public export
  Eq FillMode where
    (==) = (==) `on` show

  public export
  Ord FillMode where
    compare = compare `on` show

  public export
  read : String -> Maybe FillMode
  read "none" = Just None
  read "forwards" = Just Forwards
  read "backwards" = Just Backwards
  read "both" = Just Both
  read "auto" = Just Auto
  read _ = Nothing

  public export
  fromString : (s : String) -> {auto 0 _ : IsJust (FillMode.read s)} -> FillMode
  fromString s = fromJust $ read s

  export
  ToFFI FillMode String where
    toFFI = show

  export
  FromFFI FillMode String where
    fromFFI = read

namespace PlaybackDirection

  public export
  data PlaybackDirection = Normal | Reverse | Alternate | AlternateReverse

  public export
  Show PlaybackDirection where
    show Normal = "normal"
    show Reverse = "reverse"
    show Alternate = "alternate"
    show AlternateReverse = "alternate-reverse"

  public export
  Eq PlaybackDirection where
    (==) = (==) `on` show

  public export
  Ord PlaybackDirection where
    compare = compare `on` show

  public export
  read : String -> Maybe PlaybackDirection
  read "normal" = Just Normal
  read "reverse" = Just Reverse
  read "alternate" = Just Alternate
  read "alternate-reverse" = Just AlternateReverse
  read _ = Nothing

  public export
  fromString :  (s : String)
             -> {auto 0 _ : IsJust (PlaybackDirection.read s)}
             -> PlaybackDirection
  fromString s = fromJust $ read s

  export
  ToFFI PlaybackDirection String where
    toFFI = show

  export
  FromFFI PlaybackDirection String where
    fromFFI = read

namespace IterationCompositeOperation

  public export
  data IterationCompositeOperation = Replace | Accumulate

  public export
  Show IterationCompositeOperation where
    show Replace = "replace"
    show Accumulate = "accumulate"

  public export
  Eq IterationCompositeOperation where
    (==) = (==) `on` show

  public export
  Ord IterationCompositeOperation where
    compare = compare `on` show

  public export
  read : String -> Maybe IterationCompositeOperation
  read "replace" = Just Replace
  read "accumulate" = Just Accumulate
  read _ = Nothing

  public export
  fromString :  (s : String)
             -> {auto 0 _ : IsJust (IterationCompositeOperation.read s)}
             -> IterationCompositeOperation
  fromString s = fromJust $ read s

  export
  ToFFI IterationCompositeOperation String where
    toFFI = show

  export
  FromFFI IterationCompositeOperation String where
    fromFFI = read

namespace CompositeOperation

  public export
  data CompositeOperation = Replace | Add | Accumulate

  public export
  Show CompositeOperation where
    show Replace = "replace"
    show Add = "add"
    show Accumulate = "accumulate"

  public export
  Eq CompositeOperation where
    (==) = (==) `on` show

  public export
  Ord CompositeOperation where
    compare = compare `on` show

  public export
  read : String -> Maybe CompositeOperation
  read "replace" = Just Replace
  read "add" = Just Add
  read "accumulate" = Just Accumulate
  read _ = Nothing

  public export
  fromString :  (s : String)
             -> {auto 0 _ : IsJust (CompositeOperation.read s)}
             -> CompositeOperation
  fromString s = fromJust $ read s

  export
  ToFFI CompositeOperation String where
    toFFI = show

  export
  FromFFI CompositeOperation String where
    fromFFI = read

namespace CompositeOperationOrAuto

  public export
  data CompositeOperationOrAuto = Replace | Add | Accumulate | Auto

  public export
  Show CompositeOperationOrAuto where
    show Replace = "replace"
    show Add = "add"
    show Accumulate = "accumulate"
    show Auto = "auto"

  public export
  Eq CompositeOperationOrAuto where
    (==) = (==) `on` show

  public export
  Ord CompositeOperationOrAuto where
    compare = compare `on` show

  public export
  read : String -> Maybe CompositeOperationOrAuto
  read "replace" = Just Replace
  read "add" = Just Add
  read "accumulate" = Just Accumulate
  read "auto" = Just Auto
  read _ = Nothing

  public export
  fromString :  (s : String)
             -> {auto 0 _ : IsJust (CompositeOperationOrAuto.read s)}
             -> CompositeOperationOrAuto
  fromString s = fromJust $ read s

  export
  ToFFI CompositeOperationOrAuto String where
    toFFI = show

  export
  FromFFI CompositeOperationOrAuto String where
    fromFFI = read

--------------------------------------------------------------------------------
--          Interfaces
--------------------------------------------------------------------------------

export data Animation : Type where [external]

export
ToFFI Animation Animation where toFFI = id

export
FromFFI Animation Animation where fromFFI = Just

export
SafeCast Animation where
  safeCast = unsafeCastOnPrototypeName "Animation"

export data AnimationEffect : Type where [external]

export
ToFFI AnimationEffect AnimationEffect where toFFI = id

export
FromFFI AnimationEffect AnimationEffect where fromFFI = Just

export
SafeCast AnimationEffect where
  safeCast = unsafeCastOnPrototypeName "AnimationEffect"

export data AnimationPlaybackEvent : Type where [external]

export
ToFFI AnimationPlaybackEvent AnimationPlaybackEvent where toFFI = id

export
FromFFI AnimationPlaybackEvent AnimationPlaybackEvent where fromFFI = Just

export
SafeCast AnimationPlaybackEvent where
  safeCast = unsafeCastOnPrototypeName "AnimationPlaybackEvent"

export data AnimationTimeline : Type where [external]

export
ToFFI AnimationTimeline AnimationTimeline where toFFI = id

export
FromFFI AnimationTimeline AnimationTimeline where fromFFI = Just

export
SafeCast AnimationTimeline where
  safeCast = unsafeCastOnPrototypeName "AnimationTimeline"

export data DocumentTimeline : Type where [external]

export
ToFFI DocumentTimeline DocumentTimeline where toFFI = id

export
FromFFI DocumentTimeline DocumentTimeline where fromFFI = Just

export
SafeCast DocumentTimeline where
  safeCast = unsafeCastOnPrototypeName "DocumentTimeline"

export data KeyframeEffect : Type where [external]

export
ToFFI KeyframeEffect KeyframeEffect where toFFI = id

export
FromFFI KeyframeEffect KeyframeEffect where fromFFI = Just

export
SafeCast KeyframeEffect where
  safeCast = unsafeCastOnPrototypeName "KeyframeEffect"

--------------------------------------------------------------------------------
--          Dictionaries
--------------------------------------------------------------------------------

export data AnimationPlaybackEventInit : Type where [external]

export
ToFFI AnimationPlaybackEventInit AnimationPlaybackEventInit where toFFI = id

export
FromFFI AnimationPlaybackEventInit AnimationPlaybackEventInit where fromFFI = Just

export data BaseComputedKeyframe : Type where [external]

export
ToFFI BaseComputedKeyframe BaseComputedKeyframe where toFFI = id

export
FromFFI BaseComputedKeyframe BaseComputedKeyframe where fromFFI = Just

export data BaseKeyframe : Type where [external]

export
ToFFI BaseKeyframe BaseKeyframe where toFFI = id

export
FromFFI BaseKeyframe BaseKeyframe where fromFFI = Just

export data BasePropertyIndexedKeyframe : Type where [external]

export
ToFFI BasePropertyIndexedKeyframe BasePropertyIndexedKeyframe where toFFI = id

export
FromFFI BasePropertyIndexedKeyframe BasePropertyIndexedKeyframe where fromFFI = Just

export data ComputedEffectTiming : Type where [external]

export
ToFFI ComputedEffectTiming ComputedEffectTiming where toFFI = id

export
FromFFI ComputedEffectTiming ComputedEffectTiming where fromFFI = Just

export data DocumentTimelineOptions : Type where [external]

export
ToFFI DocumentTimelineOptions DocumentTimelineOptions where toFFI = id

export
FromFFI DocumentTimelineOptions DocumentTimelineOptions where fromFFI = Just

export data EffectTiming : Type where [external]

export
ToFFI EffectTiming EffectTiming where toFFI = id

export
FromFFI EffectTiming EffectTiming where fromFFI = Just

export data KeyframeAnimationOptions : Type where [external]

export
ToFFI KeyframeAnimationOptions KeyframeAnimationOptions where toFFI = id

export
FromFFI KeyframeAnimationOptions KeyframeAnimationOptions where fromFFI = Just

export data KeyframeEffectOptions : Type where [external]

export
ToFFI KeyframeEffectOptions KeyframeEffectOptions where toFFI = id

export
FromFFI KeyframeEffectOptions KeyframeEffectOptions where fromFFI = Just

export data OptionalEffectTiming : Type where [external]

export
ToFFI OptionalEffectTiming OptionalEffectTiming where toFFI = id

export
FromFFI OptionalEffectTiming OptionalEffectTiming where fromFFI = Just

--------------------------------------------------------------------------------
--          Mixins
--------------------------------------------------------------------------------

export data Animatable : Type where [external]

export
ToFFI Animatable Animatable where toFFI = id

export
FromFFI Animatable Animatable where fromFFI = Just


text:
module Day3a

import System.File
import Data.Strings
import Data.Either
import Data.List
import Data.List.Quantifiers
import Data.List.Elem
import Decidable.Equality
import Data.Void
import Data.Fin
import Data.Nat
import Data.Vect
import Data.Fin.Extra

------------
-- Sine Helper functions
-----------

-- Convert Either to have Strings for the error case
stringEither : Show a => Either a b -> Either String b
stringEither = bimap show id

-- Print the value of an Either, or its error string
ePrint : Show a => Either String a -> IO ()
ePrint ma = case ma of
  Left e => putStrLn ("ERROR: " ++ e)
  Right x => putStrLn (show x)

------------
-- Data types describing and functions the solution
-----------

--Each square has either a tree or is open
data Contents = Tree | Open

-- A row is a vector of contents with the given length
Row : Nat -> Type
Row n = Vect n Contents

-- Count the trees in the nth square of a given row
count : Row length -> Fin length -> Nat
count row x  with (index x row)
  count row x  | Tree = 1
  count row x  | Open = 0

-- A map of given height is a vector with that many elements,
-- each containing a row of the same length
Map : (length : Nat) -> (height : Nat) -> Type
Map len height = Vect height (Row len)

-- Given a location in one row, get the next location
-- in the following row
nextX : {length : Nat} -> {auto ok: GT length Z} -> Fin length -> Fin length
nextX {length} x with (divMod (3 + (finToNat x)) length)
  nextX x | (Fraction _ _ _ r _) = r

-- A proof that, if we walk going 3 down 1 starting at
-- the given position in the top row of the map,
-- we meet the given number of trees
data WalkCount : (theMap : Map length height) -> (start : Fin length) -> (count : Nat) -> Type where
  -- We have either 0 or 1 trees in the last row
  Done : WalkCount [] start 0
  -- Otherwise, we have some number of trees, plus however many trees come after
  Step :
    {auto ok: GT length Z}
    -> {m : Map length height}
    -> {x : Fin length}
    -> {row : Row length}
    -> WalkCount m (nextX x) subCount
    -> WalkCount (row ::  m) x (count {length = length} row x + subCount)

-- A solution:
-- Given a map and a start point,
-- it contains a count, and a proof that the count is correct
record Soln {0 length : Nat} {0 height : Nat} (theMap : Map length height)  (start : Fin length) where
  constructor MkSoln
  {theCount : Nat}
  0 correct : WalkCount theMap start theCount

-- Show that the count is decidable for any map and start point
decCount : {length : Nat} -> {auto ok: GT length Z} -> (theMap : Map length height) -> (start : Fin length) -> Soln theMap start
decCount [] start = MkSoln Done
decCount ( row :: rows) start with (decCount rows (nextX start))
  decCount (row :: rows) start | (MkSoln pf) = MkSoln (Step pf)

-- ------------------------
-- -- Input processing
-- ------------------------

-- Try converting a string into a row
stringToContents : (length : Nat) -> List Char -> Either String (Row length)
stringToContents 0 [] = pure Nil
stringToContents (S n) ('.' :: rest) = (Open ::) <$> stringToContents n rest
stringToContents (S n) ('#' :: rest) = (Tree ::) <$> stringToContents n rest
stringToContents _ _ = Left "bad parse"

-- Our main function: read the input into a map
-- then find and print its solution
main : IO ()
main = do
  mContents <- readFile "Day3.in"
  soln <- pure $ do
    theLines <- lines <$> (stringEither mContents)
    case theLines of
      [] => Left "No input"
      (row :: rows) => do
      let height = S (length rows)
      let len = length row
      case len of
        Z => Left "Empty row"
        S len => do
          let rowVec = fromList (row :: rows)
          theMap <- traverse (stringToContents $ S len) $ map fastUnpack rowVec
          pure $ theCount $ decCount theMap FZ
  ePrint soln
  -- pure $ do
  --   lines <- lines <$> mContents
  --   let height = length lines
  --   case height of
  --     [] => Left "No input"
  --     (row :: rows) => do
  --       let len = length row
  --       pure ?ret
    -- traverse (\line => maybeToEither "Bad int" (parseInteger line)) lines


text:
import Data.Vect

-- `minus` is saturating subtraction, so this works like we want it to
eq_max : (n, k : Nat) -> maximum k n = plus (n `minus` k) k
eq_max  n     Z    = rewrite minusZeroRight n in rewrite plusZeroRightNeutral n in Refl
eq_max  Z    (S _) = Refl
eq_max (S n) (S k) = rewrite sym $ plusSuccRightSucc (n `minus` k) k in rewrite eq_max n k in Refl

leftPad : (x : a) -> (n : Nat) -> (xs : Vect k a) -> Vect (maximum k n) a
leftPad {k} x n xs = rewrite eq_max n k in replicate (n `minus` k) x ++ xs

leftPadProp : {xs : Vect k a} -> (m : Nat ** leftPad x n xs = {- rewrite somehow? `the Type (rewrite xxx in replicate ...)`? -} replicate m x ++ xs)
leftPadProp {n} {k} = (n `minus` k ** ?x)

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
module Data.Functor.Foldable.Exotic

import Control.Arrow
import Control.Monad.Identity
import Control.Comonad
import Control.Comonad.Cofree
import Data.Functor.Foldable.Mod
import Data.Functor.Foldable.Instances

%access public export

infixl 9 .*

(.*) : (c -> d) -> (a -> b -> c) -> (a -> b -> d)
(.*) f g x y = f (g x y)

||| Gibbons' metamorphism. Tear down a structure, transform it, and then build up a new structure
meta : (Functor f, Corecursive f t', Recursive g t) => (a -> f a) -> (b -> a) -> (g b -> b) -> t -> t'
meta f e g = ana f . e . cata g

||| Erwig's metamorphism. Essentially a hylomorphism with a natural
||| transformation in between. This allows us to use more than one functor in a
||| hylomorphism.
hyloPro : (Functor f, Functor g) => (f a -> a) -> ({c:_} -> g c -> f c) -> (b -> g b) -> b -> a
hyloPro h e k = g
  where g x = h . e . map g . k $ x

||| A dynamorphism builds up with an anamorphism and tears down with a
||| histomorphism. Useful for lexical scoping.
dynaPro : (Functor f, Functor g) => (f (Cofree f a) -> a) -> ({c:_} -> g c -> f c) -> (b -> g b) -> b -> a
dynaPro phi eta psi = ghylo distHisto distAna phi (eta . map Id . psi)

||| A dynamorphism without a natural transformation in between.
dyna : (Functor f) => (f (Cofree f a) -> a) -> (b -> f b) -> b -> a
dyna phi = dynaPro phi id

||| Mendler's catamorphism
mcata : ({y : _} -> ((y -> c) -> f y -> c)) -> Fix f -> c
mcata psi = psi (mcata psi) . unfix

--Basically, this forms an F-algebra from a loopkup functoin plus a function that gives us the lookup function
||| Mendler's histomorphism
mhisto : ({y : _} -> ((y -> c) -> (y -> f y) -> f y -> c)) -> Fix f -> c
mhisto psi = psi (mhisto psi) unfix . unfix

||| Elgot algebra (see [this paper](https://arxiv.org/abs/cs/0609040))
elgot : Functor f => (f a -> a) -> (b -> Either a (f b)) -> b -> a
elgot phi psi = h where h = (id `either` phi . map h) . psi

||| Anamorphism that allows shortcuts.
micro : (Functor f, Corecursive f a) => (b -> Either a (f b)) -> b -> a
micro = elgot embed

||| Elgot coalgebra
coelgot : Functor f => ((a, f b) -> b) -> (a -> f a) -> a -> b
coelgot phi psi = h where h = phi . (\x => (x, (map h . psi) x))

max_stars_repo_name: ajnavarro/language-dataset

max_issues_repo_name: ajnavarro/language-dataset

max_forks_repo_name: ajnavarro/language-dataset