text:
module Data.ByteString.Internal

import Data.Buffer
import Data.List
import System.File
import System.File.Support

%default total

--------------------------------------------------------------------------------
--          FFI
--------------------------------------------------------------------------------

%foreign "scheme:blodwen-buffer-getbyte"
         "RefC:getBufferByte"
         "node:lambda:(buf,offset)=>buf.readUInt8(offset)"
prim__getBits8 : Buffer -> (offset : Bits32) -> Bits8

%foreign "scheme:blodwen-new-buffer"
         "RefC:newBuffer"
         "node:lambda:s=>Buffer.alloc(s)"
prim__newBuffer : Bits32 -> Buffer

%foreign "scheme:blodwen-buffer-size"
         "RefC:getBufferSize"
         "node:lambda:b => b.length"
prim__bufferSize : Buffer -> Bits32

%foreign "scheme:blodwen-buffer-setbyte"
         "RefC:setBufferByte"
         "node:lambda:(buf,offset,value)=>buf.writeUInt8(value, offset)"
prim__setBits8 : Buffer -> (offset : Bits32) -> (val : Bits8) -> PrimIO Int

%foreign "scheme:blodwen-buffer-copydata"
         "RefC:copyBuffer"
         "node:lambda:(b1,o1,length,b2,o2)=>b1.copy(b2,o2,o1,o1+length)"
prim__copyData : (src : Buffer) -> (srcOffset, len : Bits32) ->
                 (dst : Buffer) -> (dstOffset : Bits32) -> PrimIO Int

%foreign supportC "idris2_readBufferData"
         "node:lambda:(f,b,l,m) => require('fs').readSync(f.fd,b,l,m)"
prim__readBufferData :  FilePtr
                     -> Buffer
                     -> (offset : Bits32)
                     -> (maxbytes : Bits32) -> PrimIO Int

--------------------------------------------------------------------------------
--          ByteString
--------------------------------------------------------------------------------

||| Internally represented by a `Data.Buffer` together
||| with its length and offset.
|||
||| The internal buffer is treated as being immutable,
||| so operations modifying a `ByteString` will create
||| and write to a new `Buffer`.
export
record ByteString where
  constructor BS
  buf    : Buffer
  offset : Bits32
  len    : Bits32

--------------------------------------------------------------------------------
--          Unsafe Operations
--------------------------------------------------------------------------------

||| Wraps a `Buffer` in a `ByteString` *without making a copy*.
||| Use this for efficient reading of data from a file or other resource
||| into a `ByteString`, but make sure to not reuse the
||| `Buffer` in question elsewhere.
export %inline
unsafeFromBuffer : Buffer -> ByteString
unsafeFromBuffer b = BS b 0 $ prim__bufferSize b

||| Reads the value of a `ByteString` at the given position
||| *without checking the bounds*.
export %inline
unsafeGetBits8 : Bits32 -> ByteString -> Bits8
unsafeGetBits8 n (BS buf o _) = prim__getBits8 buf (o + n)

--------------------------------------------------------------------------------
--          Making ByteStrings
--------------------------------------------------------------------------------

||| The empty `ByteString`.
export
empty : ByteString
empty = BS (prim__newBuffer 0) 0 0

||| Converts a list of values to a `ByteString` using
||| the given conversion function. O(n).
export
fromList : (a -> Bits8) -> List a -> ByteString
fromList f vs =
  let len = cast {to = Bits32} $ length vs
   in unsafePerformIO $ fromPrim $ go vs 0 (prim__newBuffer len)
  where go : List a -> Bits32 -> Buffer -> PrimIO ByteString
        go []        ix buf w = MkIORes (BS buf 0 ix) w
        go (b :: bs) ix buf w =
          case prim__setBits8 buf ix (f b) w of
            -- this is a hack: Without this (completely useless) pattern
            -- match, the call to `prim__setBits8` is erased and ignored
            MkIORes 0 w2 => go bs (ix+1) buf w2
            MkIORes _ w2 => go bs (ix+1) buf w2

||| Converts a list of `Bits8` values to a `ByteString`.
export %inline
pack : List Bits8 -> ByteString
pack = fromList id

||| Creates a `ByteString` holding a single `Bits8` value.
export %inline
singleton : Bits8 -> ByteString
singleton = pack . (::[])

||| Converts a `String` to a `ByteString`. O(n).
|||
||| Note: All characters are truncated to 8 bits in the
||| process, so this will mangle UTF-8 encoded strings.
export %inline
FromString ByteString where
  fromString = fromList cast . fastUnpack

||| Converts a `ByteString` to a list of values using
||| the given conversion function.
export
toList : (Bits8 -> a) -> ByteString -> List a
toList f bs = go Nil bs.len
  where go : List a -> Bits32 -> List a
        go as 0 = as
        go as n =
          let ix = assert_smaller n (n-1)
           in go (f (unsafeGetBits8 ix bs) :: as) ix

||| Converts a `ByteString` to a list of `Bits8` values. O(n).
export %inline
unpack : ByteString -> List Bits8
unpack = toList id

||| Converts a `ByteString` to a String. All characters
||| will be in the range [0,255], so this does not perform
||| any character decoding.
export %inline
Show ByteString where
  show = show . fastPack . toList cast

--------------------------------------------------------------------------------
--          Comparing ByteStrings
--------------------------------------------------------------------------------

comp : ByteString -> ByteString -> Ordering
comp (BS _ _ 0) (BS _ _ 0)      = EQ  -- short cut for empty strings
comp bs1      bs2 = go 0 (min bs1.len bs2.len)
  where go : (pos, maxPos : Bits32) -> Ordering
        go pos maxPos =
          if pos == maxPos then compare bs1.len bs2.len
          else case compare (unsafeGetBits8 pos bs1) (unsafeGetBits8 pos bs2) of
                 EQ => go (assert_smaller pos $ pos + 1) maxPos
                 o  => o

export %inline
Eq ByteString where
  a == b = case comp a b of
             EQ => True
             _  => False

export %inline
Ord ByteString where
  compare = comp

--------------------------------------------------------------------------------
--          Core Functionality
--------------------------------------------------------------------------------

||| Length (number of `Bits8`) of the `ByteString`. O(1).
export %inline
length : ByteString -> Bits32
length = len

||| `True` if the given `ByteString` has zero length. O(1).
export %inline
null : ByteString -> Bool
null = (== 0) . length

export
generate : Bits32 -> (Bits32 -> Bits8) -> ByteString
generate 0 _ = empty
generate l f = unsafePerformIO $ fromPrim $ go l (prim__newBuffer l)
  where go : Bits32 -> Buffer -> PrimIO ByteString
        go 0 buf w = MkIORes (BS buf 0 l) w
        go n buf w =
          let ix = n - 1
           in case prim__setBits8 buf ix (f ix) w of
                MkIORes 0 w2 => go (assert_smaller n ix) buf w2
                MkIORes _ w2 => go (assert_smaller n ix) buf w2

export
replicate : Bits32 -> Bits8 -> ByteString
replicate n = generate n . const

export
getBits8 : Bits32 -> ByteString -> Maybe Bits8
getBits8 n bs = if bs.len > n then Just (unsafeGetBits8 n bs) else Nothing

--------------------------------------------------------------------------------
--          Concatenating ByteStrings
--------------------------------------------------------------------------------

||| Concatenate a list of `ByteString`. This allocates
||| a buffer of sufficient size in advance, so it is much
||| faster than `concat`, or `concatMap` for large `ByteString`s.
export
fastConcat : List ByteString -> ByteString
fastConcat bs = case filter ((> 0) . len) bs of
  Nil => empty
  [b] => b
  bs2 =>
    let tot = foldl (\a,b => a + b.len) 0 bs2
     in unsafePerformIO $ fromPrim $ go bs2 (prim__newBuffer tot) 0
      where go :  List ByteString
               -> Buffer
               -> (offset : Bits32)
               -> PrimIO ByteString
            go []        buf o w = MkIORes (BS buf 0 o) w
            go (BS src so sl :: bs) buf o w =
              case prim__copyData src so sl buf o w of
                -- this is a hack: Without this (completely useless) pattern
                -- match, the call to `prim__setBits8` is erased and ignored
                MkIORes 0 w2 => go bs buf (o + sl) w2
                MkIORes _ w2 => go bs buf (o + sl) w2

||| Concatenate two `ByteString`s. O(n + m).
export %inline
append : ByteString -> ByteString -> ByteString
append b1 b2 = fastConcat [b1,b2]

||| Prepend a single `Bits8` to a `ByteString`. O(n).
export %inline
cons : Bits8 -> ByteString -> ByteString
cons = append . singleton

||| Append a single `Bits8` to a `ByteString`. O(n).
export %inline
snoc : Bits8 -> ByteString -> ByteString
snoc w bs = bs `append` singleton w

export %inline
Semigroup ByteString where
  (<+>) = append

export %inline
Monoid ByteString where
  neutral = empty

--------------------------------------------------------------------------------
--          Inspecting ByteStrings
--------------------------------------------------------------------------------

||| Try to read the first element of a `ByteString`. O(1).
export
head : ByteString -> Maybe Bits8
head (BS _ _ 0)   = Nothing
head (BS buf o l) = Just (prim__getBits8 buf o)

||| Try to drop the first `Bits8` from a `ByteString`. O(1).
export
tail : ByteString -> Maybe ByteString
tail (BS _ _ 0)   = Nothing
tail (BS buf o l) = Just (BS buf (o+1) (l-1))

||| Try to split the first `Bits8` from a `ByteString`. O(1).
export
uncons : ByteString -> Maybe (Bits8, ByteString)
uncons (BS _ _ 0)   = Nothing
uncons (BS buf o l) = Just (prim__getBits8 buf o, BS buf (o+1) (l-1))

||| Try to read the last `Bits8` from a `ByteString`. O(1).
export
last : ByteString -> Maybe Bits8
last (BS _ _ 0)   = Nothing
last (BS buf o l) = Just (prim__getBits8 buf (o + l-1))

||| Try to drop the last `Bits8` from a `ByteString`. O(1).
export
init : ByteString -> Maybe ByteString
init (BS _ _ 0)   = Nothing
init (BS buf o l) = Just (BS buf o (l-1))

||| Try to split the last `Bits8` from a `ByteString`. O(1).
export
unsnoc : ByteString -> Maybe (Bits8, ByteString)
unsnoc (BS _ _ 0)   = Nothing
unsnoc (BS buf o l) = Just (prim__getBits8 buf (o + l-1), BS buf o (l-1))

--------------------------------------------------------------------------------
--          Mapping ByteStrings
--------------------------------------------------------------------------------

||| Converts every `Bits8` in a `ByteString` by applying the given
||| function. O(n).
export
map : (Bits8 -> Bits8) -> ByteString -> ByteString
map f bs = generate bs.len (\b => f $ unsafeGetBits8 b bs)

||| Interpreting the values stored in a `ByteString` as 8 bit characters,
||| convert every lower-case character to its upper-case form.
export
toUpper : ByteString -> ByteString
toUpper = map (cast . Prelude.toUpper . cast)

||| Interpreting the values stored in a `ByteString` as 8 bit characters,
||| convert every upper-case character to its lower-case form.
export
toLower : ByteString -> ByteString
toLower = map (cast . Prelude.toLower . cast)

export
reverse : ByteString -> ByteString
reverse bs = generate bs.len (\n => unsafeGetBits8 (bs.len - 1 - n) bs)

--------------------------------------------------------------------------------
--          Folding
--------------------------------------------------------------------------------

||| True, if the predicate holds for all bytes in the given `ByteString`
export
all : (Bits8 -> Bool) -> ByteString -> Bool
all p bs = go bs.len
  where go : Bits32 -> Bool
        go 0 = True
        go n =
          let n2 = n-1
           in if p (unsafeGetBits8 n2 bs)
              then go (assert_smaller n n2) else False

||| True, if the predicate holds for at least one byte in the given `ByteString`
export
any : (Bits8 -> Bool) -> ByteString -> Bool
any p bs = go bs.len
  where go : Bits32 -> Bool
        go 0 = False
        go n =
          let n2 = n-1
           in if p (unsafeGetBits8 n2 bs)
              then True else go (assert_smaller n n2)

||| True, if the given `Bits8` appears in the `ByteString`.
export %inline
elem : Bits8 -> ByteString -> Bool
elem b = any (b ==)

export
foldl : (a -> Bits8 -> a) -> a -> ByteString -> a
foldl f ini bs = go 0 ini
  where go : Bits32 -> a -> a
        go n acc = case getBits8 n bs of
          Nothing => acc
          Just v  => go (assert_smaller n (n+1)) (f acc v)

export
foldr : (Bits8 -> a -> a) -> a -> ByteString -> a
foldr f ini bs = go bs.len ini
  where go : Bits32 -> a -> a
        go 0 acc = acc
        go n acc =
          let ix = n - 1
           in go (assert_smaller n ix) (f (unsafeGetBits8 ix bs) acc)

||| The `findIndex` function takes a predicate and a `ByteString` and
||| returns the index of the first element in the ByteString
||| satisfying the predicate.
export
findIndex : (Bits8 -> Bool) -> ByteString -> Maybe Bits32
findIndex p bs = go 0 bs.len
  where go : Bits32 -> Bits32 -> Maybe Bits32
        go n l =
          if n >= l then Nothing
          else if p (unsafeGetBits8 n bs) then Just n
          else go (assert_smaller n (n+1)) l

||| Return the index of the first occurence of the given
||| byte in the `ByteString`, or `Nothing`, if the byte
||| does not appear in the ByteString.
export
elemIndex : Bits8 -> ByteString -> Maybe Bits32
elemIndex c = findIndex (c ==)

export
find : (Bits8 -> Bool) -> ByteString -> Maybe Bits8
find p bs = (`unsafeGetBits8` bs) <$> findIndex p bs

--------------------------------------------------------------------------------
--          Substrings
--------------------------------------------------------------------------------

findIndexOrLength : (Bits8 -> Bool) -> ByteString -> Bits32
findIndexOrLength p bs = go 0 bs.len
  where go : Bits32 -> Bits32 -> Bits32
        go n l = if n >= l then l
                 else if p (unsafeGetBits8 n bs) then n
                 else go (assert_smaller n (n+1)) l

findFromEndUntil : (Bits8 -> Bool) -> ByteString -> Bits32
findFromEndUntil p bs = go bs.len
  where go : Bits32 -> Bits32
        go 0 = 0
        go n =
          let n2 = n - 1
           in if p (unsafeGetBits8 n2 bs) then n else go (assert_smaller n n2)

||| Like `substr` for `String`, this extracts a substring
||| of the given `ByteString` at the given start position
||| and of the given length. If the `start` position is out
||| of bounds, the empty `ByteString` is returned. If the
||| length is too large, a substring going till the end of
||| the original `ByteString` is returned. O(1).
export
substring : (start,length : Bits32) -> ByteString -> ByteString
substring start length (BS buf o l) =
  if start >= l then empty
  else BS buf (o + start) (min (l - start) length)

generateMaybe : Bits32 -> (Bits32 -> Maybe Bits8) -> ByteString
generateMaybe 0 _ = empty
generateMaybe l f = unsafePerformIO $ fromPrim $ go 0 0 (prim__newBuffer l)
  where go : (ix,at : Bits32) -> Buffer -> PrimIO ByteString
        go ix at buf w =
          if ix >= l then MkIORes (BS buf 0 at) w else
          case f ix of
            Nothing => go (assert_smaller ix $ ix+1) at buf w
            Just b  => case prim__setBits8 buf at b w of
              MkIORes 0 w2 => go (assert_smaller ix $ ix+1) (at + 1) buf w2
              MkIORes _ w2 => go (assert_smaller ix $ ix+1) (at + 1) buf w2

export
mapMaybe : (Bits8 -> Maybe Bits8) -> ByteString -> ByteString
mapMaybe f bs = generateMaybe bs.len (\b => f $ unsafeGetBits8 b bs)

export
filter : (Bits8 -> Bool) -> ByteString -> ByteString
filter p = mapMaybe (\b => if p b then Just b else Nothing)

||| Return a `ByteString` with the first `n` values of
||| the input string. O(1)
export
take : Bits32 -> ByteString -> ByteString
take n (BS buf o l) = BS buf o (min n l)

||| Return a `ByteString` with the last `n` values of
||| the input string. O(1)
export
takeEnd : Bits32 -> ByteString -> ByteString
takeEnd n (BS buf o l) =
  let n' = min n l in BS buf (o + (l - n')) n'

||| Remove the first `n` values from a `ByteString`. O(1)
export
drop : Bits32 -> ByteString -> ByteString
drop n (BS buf o l) = if n >= l then empty else BS buf (o + n) (l - n)

||| Remove the last `n` values from a `ByteString`. O(1)
export
dropEnd : Bits32 -> ByteString -> ByteString
dropEnd n (BS buf o l) = if n >= l then empty else BS buf o (l - n)

export
splitAt : Bits32 -> ByteString -> (ByteString, ByteString)
splitAt 0 bs           = (empty, bs)
splitAt n (BS buf o l) =
  if n >= l then (BS buf o l, empty)
  else (BS buf o n, BS buf (o+n) (l -n))

||| Extracts the longest prefix of elements satisfying the
||| predicate.
export
takeWhile : (Bits8 -> Bool) -> ByteString -> ByteString
takeWhile p bs = take (findIndexOrLength (not . p) bs) bs

||| Returns the longest (possibly empty) suffix of elements
||| satisfying the predicate.
export
takeWhileEnd : (Bits8 -> Bool) -> ByteString -> ByteString
takeWhileEnd f bs = drop (findFromEndUntil (not . f) bs) bs

||| Drops the longest (possibly empty) prefix of elements
||| satisfying the predicate and returns the remainder.
export
dropWhile : (Bits8 -> Bool) -> ByteString -> ByteString
dropWhile f bs = drop (findIndexOrLength (not . f) bs) bs

||| Drops the longest (possibly empty) suffix of elements
||| satisfying the predicate and returns the remainder.
export
dropWhileEnd : (Bits8 -> Bool) -> ByteString -> ByteString
dropWhileEnd f bs = take (findFromEndUntil (not . f) bs) bs

||| Returns the longest (possibly empty) prefix of elements which do not
||| satisfy the predicate and the remainder of the string.
export
break : (Bits8 -> Bool) -> ByteString -> (ByteString, ByteString)
break p bs = let n = findIndexOrLength p bs in (take n bs, drop n bs)

||| Returns the longest (possibly empty) suffix of elements which do not
||| satisfy the predicate and the remainder of the string.
export
breakEnd : (Bits8 -> Bool) -> ByteString -> (ByteString, ByteString)
breakEnd  p bs = splitAt (findFromEndUntil p bs) bs

||| Returns the longest (possibly empty) prefix of elements
||| satisfying the predicate and the remainder of the string.
export %inline
span : (Bits8 -> Bool) -> ByteString -> (ByteString, ByteString)
span p = break (not . p)

||| Returns the longest (possibly empty) suffix of elements
||| satisfying the predicate and the remainder of the string.
export
spanEnd : (Bits8 -> Bool) -> ByteString -> (ByteString, ByteString)
spanEnd  p bs = splitAt (findFromEndUntil (not . p) bs) bs

||| Splits a 'ByteString' into components delimited by
||| separators, where the predicate returns True for a separator element.
||| The resulting components do not contain the separators. Two adjacent
||| separators result in an empty component in the output. eg.
export
splitWith : (Bits8 -> Bool) -> ByteString -> List ByteString
splitWith _ (BS _ _ 0)   = []
splitWith p (BS buf o l) = go 0 o 0 Nil
  where go :  (index         : Bits32)
           -> (currentOffset : Bits32)
           -> (currentLength : Bits32)
           -> List ByteString
           -> List ByteString
        go ix co cl bs =
          if ix >= l then reverse (BS buf co cl :: bs)
          else if p (prim__getBits8 buf (ix + o)) then
            let nbs = BS buf co cl :: bs
             in go (assert_smaller ix (ix+1)) (co+cl+1) 0 nbs
          else go (assert_smaller ix (ix+1)) co (cl+1) bs

||| Break a `ByteString` into pieces separated by the byte
||| argument, consuming the delimiter.
|||
||| As for all splitting functions in this library, this function does
||| not copy the substrings, it just constructs new `ByteString`s that
||| are slices of the original.
export
split : Bits8 -> ByteString -> List ByteString
split b = splitWith (b ==)

--------------------------------------------------------------------------------
--          Reading and Writing from and to Files
--------------------------------------------------------------------------------

export
readChunk : HasIO io => Bits32 -> File -> io (Either FileError ByteString)
readChunk max (FHandle h) = do
  let buf = prim__newBuffer max
  read     <- primIO (prim__readBufferData h buf 0 max)
  if read >= 0
     then pure (Right $ BS buf 0 (cast read))
     else pure (Left FileReadError)

export
write : HasIO io => File -> ByteString -> io (Either (FileError,Int) ())
write h (BS buf o l) = writeBufferData h buf (cast o) (cast l)


text:
module Main

main : IO ()
main = putStrLn "Thank you for watching my videos! :)"

ext: idr

max_stars_repo_name: Nikolaj-K/idris

max_issues_repo_name: Nikolaj-K/idris

max_forks_repo_name: Nikolaj-K/idris


text:
-- ----------------------------------------------------------------- [ Set.idr ]
-- Module    : Set.idr
-- Copyright : (c) 2015,2016 See CONTRIBUTORS.md
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
||| Testing Stacks using silly stupid tests
module Data.AVL.Test.Set

import Test.Unit
import Test.Random.Values

import Data.AVL.Set

%access export

list1 : List Integer
list1 = rndListIntU 123456789 (0,100) 30

list2 : List Integer
list2 = rndListIntU 987654321 (101,200) 30

set1' : Set Integer
set1' = Set.insert 101 $ Set.fromList list1

set1 : Set Integer
set1 = Set.fromList list1

set2 : Set Integer
set2 = Set.fromList list2

-- ------------------------------------------------------------ [ Construction ]
partial
testBuilding : IO Bool
testBuilding = genericTest
    (Just "List, Building" )
    (Set.size set1 == 30 && (sorted $ Set.toList $ Set.fromList list1))
    True
    (==)

-- ---------------------------------------------------------------- [ Updating ]

partial
testUpdate : IO Bool
testUpdate = genericTest
    (Just "Insert")
    (Set.size set1' == 31 && Set.size set1 == 30)
    True
    (==)

partial
testMerge : IO Bool
testMerge = genericTest
    (Just "Union")
    (Set.size $ Set.union set1 set2)
    (60)
    (==)

partial
testDiff : IO Bool
testDiff = genericTest
   (Just "Difference")
   (Set.toList $ Set.difference (Set.fromList [1,2,3]) (Set.fromList [2,3,4]))
   [1]
   (==)

partial
testIntersection : IO Bool
testIntersection = genericTest
    (Just "Intersection")
    (Set.size $ Set.intersection set1 set1)
    30
    (==)

partial
testContains : IO Bool
testContains = genericTest
    (Just "Contains")
    (Set.contains 102 $ set1)
    (False)
    (==)

partial
runTest : IO ()
runTest = do
    putStrLn "Testing Set"
    putStrLn infoLine
    NonReporting.runTests [
        testBuilding
      , testUpdate
      , testMerge
      , testContains
      , testDiff
      , testIntersection
    ]

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

max_stars_repo_name: MarcelineVQ/idris-containers

max_issues_repo_name: MarcelineVQ/idris-containers

max_forks_repo_name: MarcelineVQ/idris-containers


text:
module Test.Int64

import Data.Prim.Int64
import Data.SOP
import Hedgehog
import Test.RingLaws

allInt64 : Gen Int64
allInt64 = int64 (linear (-0x8000000000000000) 0xffffffffffffffff)

prop_ltMax : Property
prop_ltMax = property $ do
  b8 <- forAll allInt64
  (b8 <= MaxInt64) === True

prop_ltMin : Property
prop_ltMin = property $ do
  b8 <- forAll allInt64
  (b8 >= MinInt64) === True

prop_comp : Property
prop_comp = property $ do
  [m,n] <- forAll $ np [allInt64, allInt64]
  toOrdering (comp m n) === compare m n

export
props : Group
props = MkGroup "Int64" $
  [ ("prop_ltMax",  prop_ltMax)
  , ("prop_ltMin",  prop_ltMin)
  , ("prop_comp",   prop_comp)
  ] ++ ringProps allInt64


text:
module Toolkit.Data.Nat

import Decidable.Equality

%default total

public export
toNat : Int -> Nat
toNat = (integerToNat . cast)

public export
data Plus : (x,y,z : Nat) -> Type where
  Zero : Plus Z y y
  One  : Plus    n  x    z
      -> Plus (S n) x (S z)

export
plus : (x,y : Nat) -> DPair Nat (Plus x y)
plus Z y
  = MkDPair y Zero

plus (S k) y with (Nat.plus k y)
  plus (S k) y | (MkDPair fst snd)
    = MkDPair (S fst) (One snd)

resWhenZeroIsMore : (y = z -> Void) -> Plus 0 y z -> Void
resWhenZeroIsMore f Zero = f Refl

resWhenOneIsZero :  Plus (S k) y 0 -> Void
resWhenOneIsZero Zero impossible
resWhenOneIsZero (One x) impossible

export
isPlus : (x,y,z : Nat) -> Dec (Plus x y z)
isPlus Z y z with (decEq y z)
  isPlus Z y y | (Yes Refl)
    = Yes Zero

  isPlus Z y z | (No contra)
    = No (resWhenZeroIsMore contra)

isPlus (S k) y 0 = No resWhenOneIsZero

isPlus (S k) y (S j) with (isPlus k y j)
  isPlus (S k) y (S j) | (Yes prf)
    = Yes (One prf)

  isPlus (S k) y (S j) | (No contra)
    = No (\(One prf) => contra prf)

-- [ EOF ]

max_stars_repo_name: gallais/linear-circuits

max_issues_repo_name: gallais/linear-circuits

max_forks_repo_name: gallais/linear-circuits


text:
{-------------------------------------------------------------
            Equivlance relation rules mod n.
-------------------------------------------------------------}

|||
||| ModEq n x y is (aweful) prefix notation for a type x == y (mod n).
|||
||| This is a singleton dependent type, and it is inhabited solely
||| by its constructor.  So you can pattern match on tye constructor
||| by there are no values.
|||
data ModEq : (n:Nat) -> (x:Nat) -> (y:Nat) -> Type where
    {- 3 constructors, we mostly think of n, x, y as implicit.
        reflexive:      x==x (mod n),
        left-induct:    x == y (mod n) => x+n == y      (mod n)
        right-induct:   x == y (mod n) => x == (y+n)    (mod n)
    -}
  Reflex : (x:Nat) -> ModEq n x x  --- Needs syntatic sugar, for now prefix
  LInd : (ModEq n x y) -> ModEq n (x+n) y
  RInd : (ModEq n x y) -> ModEq n x (y+n)

{- Proof of reflexive property. -}
total
isRefl : (x:Nat) -> ModEq n x x
isRefl x = Reflex x

{----- Proof of symmetric property. -----}
total
isSym : (ModEq n x y) -> ModEq n y x
{- x=x => x=x -}
isSym (Reflex x) = Reflex x
{-
    (LInd (x=y=>(x+n)=y)
  & u={x=y})
  -------------------
    u={x=y}
  ------------------
    y=x (induct on u)
   ------------------
    RInd y=x = y=(x+n)
 -}
isSym (LInd u)   = RInd (isSym u)
{- x=(y+n) => u={x=y} => y=x (induct) => (y+n)=x -}
isSym (RInd u)   = LInd (isSym u)

{----- Proof of transitive property. -----}
total isTrans : (ModEq n x y) -> (ModEq n y z) -> (ModEq n x z)
--isTrans (RInd _) (LInd _) = ?isTrans_rhs_1
{- x=x & x=y => x=y -}
isTrans (Reflex x) v = v
isTrans u (Reflex y) = u
{- ((x=y=>(x+n)=y) & y=z) => x=y & y=z => x=z (induct) => (x+n)=z -}
isTrans (LInd u) v = LInd (isTrans u v)
isTrans u (RInd v) = RInd (isTrans u v)
{- (x=y=>x=(y+n)) & (y=z=>(y+n)=z) => x=y & y=z => x=z (induct) -}
isTrans (RInd u) (LInd v) {n} {x} {y=x+n} = isTrans u v  -- Note: need to expose implicit y=x+n

{----- Proof of congruence property. -----}
total isCong : (ModEq n x y) -> (ModEq n a b) -> (ModEq n (x+a) (y+b))
isCong (Reflex x) (Reflex a) = Reflex (x+a)
isCong {n} (LInd {x} u) (Reflex a) =
    {-
        (x+n) == y (mod n) because u={x == y (mod n)}
        a == a (mod n)
        ---------------------------------------------
        x+a == y+a (mod n)        (induct)
        ---------------------------------------------
        (x+a)+n == y+a (mod n)    (LInd)
        ---------------------------------------------
        x+(a+n) == y+a (mod n)    (Associative)
        ---------------------------------------------
        x+(n+a) == y+a (mod n)    (Commutative)
        ---------------------------------------------
        (x+n)+a == y+a (mod n)    (Associative)
    -}
    let w = (x+a)+n in LInd (isCong u (Reflex a))
    rewrite plusCommutative n x in
        rewrite plusAssociative n x a in
            rewrite plusAssociative (x+a) n in w

isCong {n} (RInd {y} u) (Reflex a) =
--    rewrite plusAssociative y n a in
        rewrite plusCommutative a n in
            rewrite plusAssociative y a n in
                RInd (isCong u (Reflex a))
isCong {n} {x} u (LInd {x=a} v) =   -- imiplicitly need n, x, a in scope.
    {-
        u={x == y (mod n) }
        (a+n) == b only if, v={a==b}
        ----------------------
        x+a == y+b by induction on u, v
        ----------------------
        (x+a)+n == y+b by LInd
        x+(a+n) == y+b by associativity
     -}
    rewrite plusAssociative x a n  in LInd (isCong u v)
isCong {n} {y} u (RInd {y=b} v) =   -- imiplicitly need n, x, a in scope.
    {-
        u={x == y (mod n) }
        a == (b+n) only if, v={a==b}
        ----------------------
        x+a == y+b by induction on u, v
        ----------------------
        x+a == (y+b)+n by RInd
        x+a == y+(b+n) by associativity
    -}
    rewrite plusAssociative y b n  in RInd (isCong u v)

max_stars_repo_name: algeboy/BlackBoxType

max_issues_repo_name: algeboy/BlackBoxType

max_forks_repo_name: algeboy/BlackBoxType


text:
module Minecraft.Base.PreClassic.Dirt.Item.Export

import public Minecraft.Core.Entity.Pickup.Export
import public Minecraft.Base.PreClassic.Dirt.Block
import public Minecraft.Base.PreClassic.Dirt.Item
import public Minecraft.Base.PreClassic.Dirt.ItemEntity

%default total

[dirtItem']
Item Dirt.Item where
  id = "minecraft:dirt"
  stackable = Just 64
  givenName = \x => x.base.givenName
  proj = \x => new Dirt.ItemEntity Dirt.MkItemEntity

[putDirt']
Put Dirt.Item where
  putItem self = new Dirt.Block Dirt.MkBlock

[dirtVtbl']
Vtbl Dirt.Item where
  vtable (Item Dirt.Item) = Just dirtItem
  vtable (Put  Dirt.Item) = Just putDirt
  vtable _ = Nothing

dirtItem = dirtItem'
putDirt  = putDirt'
dirtVtbl = dirtVtbl'

max_stars_repo_name: po-stulate/postulate

max_issues_repo_name: po-stulate/postulate

max_forks_repo_name: po-stulate/postulate


text:
-- | Exercises on Lists
module Koans.Lists

-- | What is the type of this list.
nats : List Int
nats = [0,1,2,3,4,5,6,7,9]

-- | Reproduce the list [0,1,3,5,7,9,2,4,6,8] using the following functions.
odds : List Int
odds = [1,3,5,7,9]

evens : List Int
evens = [2,4,6,8]

zero : Int
zero = 0

zeroOddsEvens : Bool
zeroOddsEvens = (zero ++ odds ++ evens) == [0,1,3,5,7,9,2,4,6,8]

-- | Complete the result of following functions.

headOList : Bool
headOList = 5 == Vect.head [5,4,3,2,1]

tailOList : Bool
tailOList = [1,2,3,4,5] == Vect.tail [0,1,2,3,4,5]

lastOList : Bool
lastOList = 1 == Vect.last [5,4,3,2,1]

initOList : Bool
initOList = [1,2,3,4,5] == Vect.init [1,2,3,4,5,6]

lengthOList : Bool
lengthOList = 5 == List.length [1,2,3,4,5]

reverseTheList : Bool
reverseTheList = [5,4,3,2,1] == List.reverse [1,2,3,4,5]

first3 : Bool
first3 = [1,2,3] == take 3 [1..10]

drop3 : Bool
drop3 = [4,5,6,7,8,9,10] == drop 3 [1..10]

countAllTheNumbers : Bool
countAllTheNumbers = 55  == sum [1..10]

timesAllTheNnumbers : Bool
timesAllTheNnumbers = 3628800 == product [1..10]

elementOrNot : Bool
elementOrNot = List.elem 4 [4] == True

-- | Make this function true
stopPete : Bool
stopPete = take 4 (repeat 3) == [3,3,3,3]

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

max_stars_repo_name: harrisi/on-being-better

max_issues_repo_name: harrisi/on-being-better

max_forks_repo_name: harrisi/on-being-better


text:
{-
The String
-}
module Main

import CIL.FFI
import CIL.FFI.Array

%inline
ByRef : CILTy -> Type
ByRef refTy = CILRef refTy (interpCILTy refTy)

namespace ByRef

  %inline
  ByRefTy : CILTy -> Type
  ByRefTy refTy = CIL $ CILTyGen (CILTyRef "" "ByRef") [refTy]

  %inline
  new : (refTy : CILTy)
     -> {auto fty : FTy FFI_CIL [] (interpCILTy refTy -> CIL_IO (ByRefTy refTy))}
     -> interpCILTy refTy
     -> CIL_IO (ByRef refTy)
  new refTy value = do
    ref <- CIL.FFI.new (interpCILTy refTy -> CIL_IO (ByRefTy refTy)) value
    pure (believe_me ref)

  %inline
  get : CILRef refTy refT
     -> {auto fty : FTy FFI_CIL [] (CILRef refTy refT -> CIL_IO refT)}
     -> CIL_IO refT
  get {refTy} {refT} a =
    invokeInstance "get" (CILRef refTy refT -> CIL_IO refT) a

StringTy : CILTy
StringTy = CILTyStr

FixtureTy : CILTy
FixtureTy = CILTyRef "" "Fixture"

passStringByRef : ByRef StringTy -> CIL_IO ()
passStringByRef = invokeStatic FixtureTy "PassStringByRef" (ByRef StringTy -> CIL_IO ())

main : CIL_IO ()
main = do
  ref <- ByRef.new StringTy "Not the string"
  passStringByRef ref
  get ref >>= putStrLn

-- Local Variables:
-- idris-load-packages: ("cil")
-- End:

max_stars_repo_name: alaendle/idris-cil

max_issues_repo_name: alaendle/idris-cil

max_forks_repo_name: alaendle/idris-cil


text:
import Data.Vect

data VectN : Type -> Type where
     MkVectN : (n : Nat) -> Vect n a -> VectN a

doSearch : Nat -> VectN Int
doSearch n = MkVectN ?vlength [1,2,3,4]


text:
import Control.Monad.State
import Data.List
import Data.String
import Data.MSF.Trans
import Generics.Derive
import JSON
import Rhone.JS
import Web.Html

%default total
%language ElabReflection

record Item where
  constructor MkI
  id   : Nat
  todo : String
  done : Bool

%runElab derive "Item" [Generic,Meta,Eq,FromJSON,ToJSON]

data Ev = New | Clear | Mark Bool | Hash
        | Edit Nat | Abort Nat | Delete Nat | Upd Nat | Toggle Nat Bool

%runElab derive "Ev" [Generic,Eq]

new : ElemRef HTMLInputElement
new = Id Input "new-todo"

liId : Nat -> ElemRef HTMLLIElement
liId n = Id Li "item_\{show n}"

editId : Nat -> ElemRef HTMLInputElement
editId n = Id Input "edit_\{show n}"

itemView : Item -> Node Ev
itemView (MkI n lbl done) =
  li [ ref (liId n), class (if done then "completed" else "") ]
     [ div [ class "view" ]
           [ input [ class "toggle", type CheckBox, checked done
                   , onChecked (Toggle n) ] []
           , label [ onDblClick (Edit n) ] [ Text lbl ]
           , button [ class "destroy", onClick (Delete n) ] [] ]
     , input [ ref (editId n), class "edit", value lbl
             , onEnterDown (Upd n), onEscDown (Abort n), onBlur (Upd n) ] [] ]

ST : Type
ST = List Item

newId : MonadState ST m => MSF m i Nat
newId = get >>^ (maybe 0 (S . id) . getAt 0)

mod : MonadState ST m => (i -> ST -> ST) -> MSF m i ()
mod f = arr f >>! modify

modAt : MonadState ST m => (i -> Item -> Item) -> MSF m (NP I [Nat,i]) ()
modAt f = mod $ \[n,v] => map (\t => if t.id == n then f v t else t)

newVal : LiftJSIO m => MSF m i (Event String)
newVal = valueOf new >>> runEffect (setValue new "") >>> trim ^>> isNot ""

countStr : Nat -> String
countStr 1 = "1 item left"
countStr k = "\{show k} items left"

items : NP I [List Item, String] -> List (Node Ev)
items [is,"#/active"]    = map itemView . filter (not . done) $ reverse is
items [is,"#/completed"] = map itemView . filter done $ reverse is
items [is,_]             = map itemView $ reverse is

disp : MSF (StateT ST $ DomIO Ev JSIO) i ()
disp = get >>> fan
  [ fan [id, windowHash] >>> arr items >>! innerHtmlAtN (Id Ul "todo-list")
  , isNil ^>- [hiddenAt (Id Section "main"), hiddenAt (Id Footer "footer")]
  , all done ^>> isChecked (Id Input "toggle-all")
  , (not . any done) ^>> hiddenAt (Id Button "clear-completed")
  , count (not . done) ^>> countStr ^>> innerHtml (Id Span "todo-count")
  , encode ^>> setItemAt "todomvc-idris2" ]
  >>> windowHash >>-
        [ ifIs "#/active"    "selected" >>> classAt (Id A "sel-active")
        , ifIs "#/completed" "selected" >>> classAt (Id A "sel-completed")
        , ifIs "#/"          "selected" >>> classAt (Id A "sel-all") ]

update : MSF (StateT ST $ DomIO Ev JSIO) (NP I [Nat,String]) ()
update = bool (\[_,s] => null s) >>> collect
           [ mod (\[i,_] => filter $ (/= i) . id)
           , modAt (\s => {todo := s}) ]

controller : MSF (StateT ST $ DomIO Ev JSIO) Ev ()
controller = (toI . unSOP . from) ^>> collect
  [ newVal ?>> [| MkI newId id (pure False) |] >>> mod (::) >>> disp
  , mod (\_ => filter $ not . done) >>> disp
  , mod (\[b] => map {done := b}) >>> disp
  , disp
  , fan [ hd >>^ liId, const "editing" ] >>> attribute_ "class"
  , disp
  , mod (\[i] => filter $ (/= i) . id) >>> disp
  , hd >>> fan [id, editId ^>> value >>^ trim] >>> update >>> disp
  , modAt (\b => {done := b}) >>> disp ]

ui : DomIO Ev JSIO (MSF (DomIO Ev JSIO) Ev (), JSIO ())
ui =  do
  setAttribute new (onEnterDown New)
  setAttribute (Id Button "clear-completed") (onClick Clear)
  setAttribute (Id Input "toggle-all") (onChecked Mark)
  handleEvent Window (HashChange Hash)
  ini <- liftJSIO (window >>= localStorage >>= (`getItem` "todomvc-idris2"))
  pure (loopState (fromMaybe Nil $ ini >>= decodeMaybe) controller, pure ())

main : IO ()
main = runJS . ignore $ reactimateDomIni Hash "todo" ui


text:
module Main

import Control.IOExcept
import Control.ST
import Control.ST.File
import Control.ST.ImplicitCall

increment : (x : Var) -> STrans m () [ x ::: State Int ]
                                     (const [x ::: State Int])
increment x = do num <- read x
                 write x (num + 1)

readFileCount : (ConsoleIO m, File m) =>
                   (fileHandle : Var)
                -> (count : Var)
                -> {auto prf   : ValidModeRead mode}
                -> ST m (Either FileError (List String))
                      [ count      ::: (State Int),
                        fileHandle ::: FileHandleI {m} mode ]
readFileCount fh cnt =
     readAcc fh cnt []
     where
          readAcc : (ConsoleIO m, File m) =>
                       (fileHandle : Var)
                    -> (count : Var)
                    -> List String
                    -> {auto prf   : ValidModeRead mode}
                    -> ST m (Either FileError (List String))
                          [ count      ::: (State Int),
                            fileHandle ::: FileHandleI {m} mode ]
          readAcc fileHandle cnt acc = with ST do
            e <- (eof fileHandle)
            if (not e)
               then do Right str <- (readLine fileHandle)
                             | Left ferr => pure (Left ferr)
                       (increment cnt)
                       readAcc fileHandle cnt (str :: acc)
               else do let rev = reverse acc
                       pure (Right rev)

testFile : (ConsoleIO m, File m) => ST m () []
testFile = with ST do
              Right fileHandle <- open "testFile" Read
                    | Left ferr => do putStrLn (show ferr)
                                      pure ()
              count <- new 0
              Right fContents <- readFileCount fileHandle count
                    | Left ferr => do putStrLn (show ferr)
                                      delete count
                                      close fileHandle
                                      pure ()
              putStrLn (show fContents)
              putStrLn (show !(read count))
              delete count
              close fileHandle
              pure ()

main : IO ()
main = do putStrLn "--test IO:"
          run testFile
          putStrLn "--test IOExcept:"
          ioe_run (run testFile)
                  (\err => putStrLn err)
                  (\ok  => printLn ok)

-- EOF -------------------------------------------------------------------------

max_stars_repo_name: grin-compiler/idris-grin

max_issues_repo_name: grin-compiler/idris-grin

max_forks_repo_name: grin-compiler/idris-grin


text:
data ListLast : List a -> Type where
    Empty : ListLast []
    NonEmpty : (xs : List a) -> (x : a) -> ListLast (xs ++ [x])

describeHelper : Show a => (input : List a) -> (form : ListLast input) -> String
describeHelper [] Empty = "Empty"
describeHelper (xs ++ [x]) (NonEmpty xs x) =
    "Non-empty, initial portion = " ++ show xs

total
listLast : (xs : List a) -> ListLast xs
listLast [] = Empty
listLast (x :: xs) =
    case listLast xs of
        Empty => NonEmpty [] x
        NonEmpty ys y => NonEmpty (x :: ys) y

descibeListEnd : Show a => List a -> String
descibeListEnd xs = describeHelper xs (listLast xs)

descibeListEndWith : Show a => List a -> String
descibeListEndWith input with (listLast input)
  descibeListEndWith [] | Empty = "Empty"
  descibeListEndWith (xs ++ [x]) | (NonEmpty xs x) =
    "Non-empty, initial portion = " ++ show xs

myReverse : List a -> List a
myReverse input with (listLast input)
  myReverse [] | Empty = []
  myReverse (xs ++ [x]) | (NonEmpty xs x) = x :: myReverse xs


text:
module Libgit.Repository

import Control.Monad.Managed

import Libgit.Clone
import Libgit.FFI
import Libgit.Git
import Libgit.Types

||| A sum type representing the different ways to instantiate a GitRepository.
public export
data GitRepositoryOptions : Type where
  ||| Clone a repository given options, a URL, and a local path.
  GitRepositoryClone : CloneOpts -> (url : String) -> (localPath : String) -> GitRepositoryOptions
  ||| Open an existing repository using a local path.
  GitRepositoryOpen : (path : String) -> GitRepositoryOptions

withOpenedRepository : (path : String)
                    -> (action : (GitResult GitRepository -> IO a)
                    -> IO a
withOpenedRepository path act = do
  cresult <- primIO (prim_git_open_repository path)
  result <- getGitResult cresult
  res <- act (MkGitRepository <$> result)
  case result of
    Left _ => pure res
    Right ptr => pure res <* primIO (prim_git_repository_free ptr)

||| Opens an existing Git repository.
|||
||| Returns the Git repository pointed to by the provided path.
|||
||| @path Local path to the Git repository.
export
openedRepository : (path : String)
                -> Managed (GitResult GitRepository)
openedRepository path = managed (withOpenedRepository path)

||| Given GitRepositoryOptions, obtain a managed reference to a GitRepository
||| by cloning a repository or opening an existing repository.
|||
||| Returns a managed reference to a GitRepository.
|||
||| @options A GitRepositoryOptions specifying the strategy to use.
export
repository : (options : GitRepositoryOptions)
          -> Managed (GitResult GitRepository)
repository (GitRepositoryClone opts url localPath) = clonedRepository opts url localPath
repository (GitRepositoryOpen path) = openedRepository path

||| A sum type representing the various strategies for git reset.
|||
||| + GitResetSoft - Move the head to the given commit
||| + GitResetMixed - Soft plus reset index to the commit
||| + GitResetHard - Mixed plus changes in working tree discarded
public export
data GitResetType =
    GitResetSoft
  | GitResetMixed
  | GitResetHard

gitResetTypeToInt : GitResetType -> Int
gitResetTypeToInt GitResetSoft = 1
gitResetTypeToInt GitResetMixed = 2
gitResetTypeToInt GitResetHard = 3

||| Set the current head to a commit or tag.
|||
||| Returns a Git error code.
|||
||| @repo The Git repository containing the commit or tag.
||| @obj  The Git object (must be either a commit or a tag) to set HEAD to.
||| @rst  The type of reset to perform. An instance of GitResetType.
export
resetRepository : (repo : GitRepository)
               -> {typ : GitObjectType}
               -> {auto 0 prf : IsCommitish typ}
               -> (obj : GitObject typ)
               -> (rst : GitResetType)
               -> IO Int
resetRepository (MkGitRepository repoPtr) (MkGitObject objPtr) resetType = do
  let rt = gitResetTypeToInt resetType
      cgrOptions = git_checkout_options_init
  (err, optsPtr) <- getGitResultPair cgrOptions
  let freeOpts = primIO (prim_free optsPtr)
  case err of
    0 => do
      res <- primIO (prim_git_reset repoPtr objPtr rt optsPtr)
      pure res <* freeOpts
    _ => pure err <* freeOpts

max_forks_repo_name: bigs/libgit-idris


text:
module Sub03Apply54x30

import ProofColDivSeqBase
import ProofColDivSeqPostulate
import ProofColDivSeqPostuProof

%default total
-- %language ElabReflection

-- 3(18x+10) --A[6,-4]->C[4,-4]--> 3(8x+3)
export
apply54x30 : (Not . P) (S (S (S (plus (plus (plus (plus (plus l l) l) (S (plus (plus l l) l))) (S (S (plus (plus (plus l l) l) (S (plus (plus l l) l))))))
                         (S (S (plus (plus (plus l l) l) (S (plus (plus l l) l)))))))))
  -> (m : Nat **
        (LTE (S m)
             (S (S (S (plus (plus (plus (plus (plus l l) l) (S (plus (plus l l) l))) (S (S (plus (plus (plus l l) l) (S (plus (plus l l) l))))))
                            (S (S (plus (plus (plus l l) l) (S (plus (plus l l) l))))))))),
         (Not . P) m))
apply54x30 {l} col = ((S (S (S (plus (plus (plus l l) (plus l l)) (plus (plus l l) (plus l l)))))) ** (lte54x30 l, ac54x30To24x9 l col)) where
  lte54x30 : (l:Nat) -> LTE (S (S (S (S (plus (plus (plus l l) (plus l l)) (plus (plus l l) (plus l l)))))))
                            (S (S (S (plus (plus (plus (plus (plus l l) l) (S (plus (plus l l) l))) (S (S (plus (plus (plus l l) l) (S (plus (plus l l) l))))))
                                           (S (S (plus (plus (plus l l) l) (S (plus (plus l l) l)))))))))
  lte54x30 Z = (lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . LTESucc . LTESucc . LTESucc . LTESucc) LTEZero
  lte54x30 (S k) = let lemma = lte54x30 k in
    rewrite (sym (plusSuccRightSucc k k)) in
    rewrite (sym (plusSuccRightSucc (plus k k) (S (plus k k)))) in
    rewrite (sym (plusSuccRightSucc (plus k k) (plus k k))) in
    rewrite (sym (plusSuccRightSucc (plus (plus k k) (plus k k)) (S (S (S (plus (plus k k) (plus k k))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus k k) (plus k k)) (S (S (plus (plus k k) (plus k k)))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus k k) (plus k k)) (S (plus (plus k k) (plus k k))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus k k) (plus k k)) (plus (plus k k) (plus k k)))) in
    rewrite (sym (plusSuccRightSucc (plus k k) k)) in
    rewrite (sym (plusSuccRightSucc (plus (plus k k) k) (S (S (S (plus (plus k k) k)))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus k k) k) (S (S (plus (plus k k) k))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus k k) k) (S (plus (plus k k) k)))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus k k) k) (S (plus (plus k k) k))) (S (S (S (S (S (S (S (plus (plus (plus k k) k) (S (plus (plus k k) k)))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus k k) k) (S (plus (plus k k) k))) (S (S (S (S (S (S (plus (plus (plus k k) k) (S (plus (plus k k) k))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus k k) k) (S (plus (plus k k) k))) (S (S (S (S (S (plus (plus (plus k k) k) (S (plus (plus k k) k)))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus k k) k) (S (plus (plus k k) k))) (S (S (S (S (plus (plus (plus k k) k) (S (plus (plus k k) k))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus k k) k) (S (plus (plus k k) k))) (S (S (S (plus (plus (plus k k) k) (S (plus (plus k k) k)))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus k k) k) (S (plus (plus k k) k))) (S (S (plus (plus (plus k k) k) (S (plus (plus k k) k))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus k k) k) (S (plus (plus k k) k))) (S (S (plus (plus (plus k k) k) (S (plus (plus k k) k))))))  (S (S (S (S (S (S (S (plus (plus (plus k k) k) (S (plus (plus k k) k)))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus k k) k) (S (plus (plus k k) k))) (S (S (plus (plus (plus k k) k) (S (plus (plus k k) k))))))  (S (S (S (S (S (S (plus (plus (plus k k) k) (S (plus (plus k k) k))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus k k) k) (S (plus (plus k k) k))) (S (S (plus (plus (plus k k) k) (S (plus (plus k k) k))))))  (S (S (S (S (S (plus (plus (plus k k) k) (S (plus (plus k k) k)))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus k k) k) (S (plus (plus k k) k))) (S (S (plus (plus (plus k k) k) (S (plus (plus k k) k))))))  (S (S (S (S (plus (plus (plus k k) k) (S (plus (plus k k) k))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus k k) k) (S (plus (plus k k) k))) (S (S (plus (plus (plus k k) k) (S (plus (plus k k) k))))))  (S (S (S (plus (plus (plus k k) k) (S (plus (plus k k) k)))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus k k) k) (S (plus (plus k k) k))) (S (S (plus (plus (plus k k) k) (S (plus (plus k k) k))))))  (S (S (plus (plus (plus k k) k) (S (plus (plus k k) k))))))) in
      (lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc) lemma


text:
module Starknet

-- Copied from official Prelude and excluded PrimIO and IO
import public Builtin
-- import public PrimIO
import public Prelude.Basics as Prelude
import public Prelude.Cast as Prelude
import public Prelude.EqOrd as Prelude
import public Prelude.Interfaces as Prelude
import public Prelude.Interpolation as Prelude
-- import public Prelude.IO as Prelude
import public Prelude.Num as Prelude
import public Prelude.Ops as Prelude
import public Prelude.Show as Prelude
import public Prelude.Types as Prelude
import public Prelude.Uninhabited as Prelude

import public Common
import public Common.Casts
import public Common.Pedersen
import public Common.Felt
import public Common.Dict
import public Common.Memory
import public Starknet.Syscall

max_stars_repo_name: skyro-compiler/skyro

max_issues_repo_name: skyro-compiler/skyro

max_forks_repo_name: skyro-compiler/skyro


text:
module System.File

import Data.List
import Data.Strings
import System.Info

public export
data Mode = Read | WriteTruncate | Append | ReadWrite | ReadWriteTruncate | ReadAppend

public export
FilePtr : Type
FilePtr = AnyPtr

support : String -> String
support fn = "C:" ++ fn ++ ", libidris2_support"

libc : String -> String
libc fn = "C:" ++ fn ++ ", libc 6"

%foreign support "idris2_openFile"
         "node:support:openFile,support_system_file"
prim__open : String -> String -> PrimIO FilePtr

%foreign support "idris2_closeFile"
         "node:lambdaRequire:fs:(fp) => __require_fs.closeSync(fp.fd)"
prim__close : FilePtr -> PrimIO ()

%foreign support "idris2_fileError"
         "node:lambda:x=>(x===1n?BigInt(1):BigInt(0))"
prim__error : FilePtr -> PrimIO Int

%foreign support "idris2_fileErrno"
         "node:lambda:()=>-BigInt(process.__lasterr.errno)"
prim__fileErrno : PrimIO Int

%foreign support "idris2_readLine"
         "node:support:readLine,support_system_file"
prim__readLine : FilePtr -> PrimIO (Ptr String)

%foreign support "idris2_readChars"
prim__readChars : Int -> FilePtr -> PrimIO (Ptr String)
%foreign "C:fgetc,libc 6"
prim__readChar : FilePtr -> PrimIO Int

%foreign support "idris2_writeLine"
         "node:lambdaRequire:fs:(filePtr, line) => __require_fs.writeSync(filePtr.fd, line, undefined, 'utf-8')"
prim__writeLine : FilePtr -> String -> PrimIO Int

%foreign support "idris2_eof"
         "node:lambda:x=>(x.eof?1n:0n)"
prim__eof : FilePtr -> PrimIO Int

%foreign "C:fflush,libc 6"
prim__flush : FilePtr -> PrimIO Int
%foreign support "idris2_popen"
prim__popen : String -> String -> PrimIO FilePtr
%foreign support "idris2_pclose"
prim__pclose : FilePtr -> PrimIO ()

%foreign support "idris2_removeFile"
prim__removeFile : String -> PrimIO Int

%foreign support "idris2_fileSize"
         "node:lambdaRequire:fs:fp=>__require_fs.fstatSync(fp.fd, {bigint: true}).size"
prim__fileSize : FilePtr -> PrimIO Int

%foreign support "idris2_fileSize"
prim__fPoll : FilePtr -> PrimIO Int

%foreign support "idris2_fileAccessTime"
prim__fileAccessTime : FilePtr -> PrimIO Int

%foreign support "idris2_fileModifiedTime"
         "node:lambdaRequire:fs:fp=>__require_fs.fstatSync(fp.fd, {bigint: true}).mtimeMs / 1000n"
prim__fileModifiedTime : FilePtr -> PrimIO Int

%foreign support "idris2_fileStatusTime"
prim__fileStatusTime : FilePtr -> PrimIO Int

%foreign support "idris2_stdin"
         "node:lambda:x=>({fd:0, buffer: Buffer.alloc(0), name:'<stdin>', eof: false})"
prim__stdin : FilePtr

%foreign support "idris2_stdout"
         "node:lambda:x=>({fd:1, buffer: Buffer.alloc(0), name:'<stdout>', eof: false})"
prim__stdout : FilePtr

%foreign support "idris2_stderr"
         "node:lambda:x=>({fd:2, buffer: Buffer.alloc(0), name:'<stderr>', eof: false})"
prim__stderr : FilePtr

%foreign libc "chmod"
         "node:support:chmod,support_system_file"
prim__chmod : String -> Int -> PrimIO Int

modeStr : Mode -> String
modeStr Read              = if isWindows then "rb" else "r"
modeStr WriteTruncate     = if isWindows then "wb" else "w"
modeStr Append            = if isWindows then "ab" else "a"
modeStr ReadWrite         = if isWindows then "rb+" else "r+"
modeStr ReadWriteTruncate = if isWindows then "wb+" else "w+"
modeStr ReadAppend        = if isWindows then "ab+" else "a+"

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

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

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

ok : HasIO io => a -> io (Either FileError a)
ok x = pure (Right x)

public export
data File : Type where
     FHandle : FilePtr -> File

export
stdin : File
stdin = FHandle prim__stdin

export
stdout : File
stdout = FHandle prim__stdout

export
stderr : File
stderr = FHandle prim__stderr

export
openFile : HasIO io => String -> Mode -> io (Either FileError File)
openFile f m
    = do res <- primIO (prim__open f (modeStr m))
         if prim__nullAnyPtr res /= 0
            then returnError
            else ok (FHandle res)

export
closeFile : HasIO io => File -> io ()
closeFile (FHandle f) = primIO (prim__close f)

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

export
fGetLine : HasIO io => (h : File) -> io (Either FileError String)
fGetLine (FHandle f)
    = do res <- primIO (prim__readLine f)
         if prim__nullPtr res /= 0
            then returnError
            else ok (prim__getString res)

export
fGetChars : HasIO io => (h : File) -> Int -> io (Either FileError String)
fGetChars (FHandle f) max
    = do res <- primIO (prim__readChars max f)
         if prim__nullPtr res /= 0
            then returnError
            else ok (prim__getString res)

export
fGetChar : HasIO io => (h : File) -> io (Either FileError Char)
fGetChar (FHandle h)
    = do c <- primIO (prim__readChar h)
         ferr <- primIO (prim__error h)
         if (ferr /= 0)
            then returnError
            else ok (cast c)

export
fPutStr : HasIO io => (h : File) -> String -> io (Either FileError ())
fPutStr (FHandle f) str
    = do res <- primIO (prim__writeLine f str)
         if res == 0
            then returnError
            else ok ()

export
fPutStrLn : HasIO io => (h : File) -> String -> io (Either FileError ())
fPutStrLn f str = fPutStr f (str ++ "\n")

export
fEOF : HasIO io => (h : File) -> io Bool
fEOF (FHandle f)
    = do res <- primIO (prim__eof f)
         pure (res /= 0)

export
fflush : HasIO io => (h : File) -> io ()
fflush (FHandle f)
    = do primIO (prim__flush f)
         pure ()

export
popen : HasIO io => String -> Mode -> io (Either FileError File)
popen f m = do
    ptr <- primIO (prim__popen f (modeStr m))
    if prim__nullAnyPtr ptr /= 0
        then returnError
        else pure (Right (FHandle ptr))

export
pclose : HasIO io => File -> io ()
pclose (FHandle h) = primIO (prim__pclose h)

export
fileAccessTime : HasIO io => (h : File) -> io (Either FileError Int)
fileAccessTime (FHandle f)
    = do res <- primIO (prim__fileAccessTime f)
         if res > 0
            then ok res
            else returnError

export
fileModifiedTime : HasIO io => (h : File) -> io (Either FileError Int)
fileModifiedTime (FHandle f)
    = do res <- primIO (prim__fileModifiedTime f)
         if res > 0
            then ok res
            else returnError

export
fileStatusTime : HasIO io => (h : File) -> io (Either FileError Int)
fileStatusTime (FHandle f)
    = do res <- primIO (prim__fileStatusTime f)
         if res > 0
            then ok res
            else returnError

export
removeFile : HasIO io => String -> io (Either FileError ())
removeFile fname
    = do res <- primIO (prim__removeFile fname)
         if res == 0
            then ok ()
            else returnError

export
fileSize : HasIO io => (h : File) -> io (Either FileError Int)
fileSize (FHandle f)
    = do res <- primIO (prim__fileSize f)
         if res >= 0
            then ok res
            else returnError

export
fPoll : HasIO io => File -> io Bool
fPoll (FHandle f)
    = do p <- primIO (prim__fPoll f)
         pure (p > 0)

export
readFile : HasIO io => String -> io (Either FileError String)
readFile file
  = do Right h <- openFile file Read
          | Left err => returnError
       Right content <- read [] h
          | Left err => do closeFile h
                           returnError
       closeFile h
       pure (Right (fastAppend content))
  where
    read : List String -> File -> io (Either FileError (List String))
    read acc h
        = do eof <- fEOF h
             if eof
                then pure (Right (reverse acc))
                else
                  do Right str <- fGetLine h
                        | Left err => returnError
                     read (str :: acc) h

||| Write a string to a file
export
writeFile : HasIO io =>
            (filepath : String) -> (contents : String) ->
            io (Either FileError ())
writeFile fn contents = do
     Right h  <- openFile fn WriteTruncate
        | Left err => pure (Left err)
     Right () <- fPutStr h contents
        | Left err => do closeFile h
                         pure (Left err)
     closeFile h
     pure (Right ())

namespace FileMode
  public export
  data FileMode = Read | Write | Execute

public export
record Permissions where
  constructor MkPermissions
  user   : List FileMode
  group  : List FileMode
  others : List FileMode

mkMode : Permissions -> Int
mkMode p
    = getMs (user p) * 64 + getMs (group p) * 8 + getMs (others p)
  where
    getM : FileMode -> Int
    getM Read = 4
    getM Write = 2
    getM Execute = 1

    getMs : List FileMode -> Int
    getMs = sum . map getM

export
chmodRaw : HasIO io => String -> Int -> io (Either FileError ())
chmodRaw fname p
    = do ok <- primIO $ prim__chmod fname p
         if ok == 0
            then pure (Right ())
            else returnError

export
chmod : HasIO io => String -> Permissions -> io (Either FileError ())
chmod fname p = chmodRaw fname (mkMode p)


text:
module Chapter4

import Chapter3

import Data.Bool
import Data.InSet
import Data.InSet.List
import Data.List
import Data.List.Equalities

import Decidable.Equality

%default total

-- Section 4.1 --

public export
data Surj : (f : a -> b) -> Type where
  SurjPrf : ((x : a) -> (y ** x = f y)) -> Surj f

export
to_list_not_surj : Not $ (f : a -> List a) -> Surj f
to_list_not_surj surj = let SurjPrf f = surj \x => [x] in
                        let (y ** prf) = f [] in
                        lemma_val_not_nil $ sym prf

public export
EqRefl : Type -> Type
EqRefl a = Eq a => (x : a) -> x == x = True

export
to_set_not_surj : Equality a => EqRefl a -> Not $ (f : a -> InSet a) -> Surj f
to_set_not_surj er surj = let SurjPrf f = surj \x => [x] in
                          let (y ** prf) = f [] in
                          non_empty_is_not_empty (y ** x_in_x_etc y []) $ sym prf

-- Exercise 4.1 --

export
lemma_4_1 : {t, a : ty -> ty -> Type} ->
            (T : (x, y : ty) -> Either (t x y) (t y x)) ->
            (A : (x, y : ty) -> a x y -> a y x -> x = y) ->
            (TA : (x, y : ty) -> t x y -> a x y) ->
            {x, y : ty} -> a x y -> t x y
lemma_4_1 tl al tal axy = case tl x y of
  Left  txy => txy
  Right tyx => rewrite al x y axy $ tal y x tyx in either id id $ tl y y

  -- Alternatively, you can write a proof without usage of `tl y y`:
  --Right tyx => let u = al x y axy $ tal y x tyx in
  --             rewrite u in
  --             rewrite cong (t y) $ sym u in
  --             tyx

-- Exercise 4.2 --

length_of_init : (x : a) -> (xs : List a) -> length (init $ x::xs) = length xs
length_of_init _ []      = Refl
length_of_init _ (x::xs) = rewrite length_of_init x xs in Refl

last_goes_right : (x : a) -> (xs, ys : List a) -> init (x::xs) ++ last (x::xs)::ys = x::xs ++ ys
last_goes_right _ []      _  = Refl
last_goes_right _ (x::xs) ys = rewrite last_goes_right x xs ys in Refl

export
lemma_4_2 : (xs : List a) -> (ys ** zs ** (xs = ys ++ zs, Either (length ys = length zs) (length ys = 1 + length zs)))
lemma_4_2 [] = ([] ** [] ** (Refl, Left Refl))
lemma_4_2 (x::xs) = let (ys ** zs ** (xyz, lengths)) = lemma_4_2 xs in
                    rewrite xyz in
                    case lengths of
                      Left yz => (x::ys ** zs ** rewrite yz in (Refl, Right Refl))
                      Right ySz => let (yh::ytl) = ys in
                                   (x :: init ys ** last ys :: zs ** rewrite length_of_init x ys in
                                                                     rewrite ySz in
                                                                     rewrite last_goes_right yh ytl zs in
                                                                     (Refl, Left Refl))

  -- I did the proof of ex. 4.2 by case analysis rather than by suggesting `take (half $ 1 + length xs) xs` and `drop (half $ 1 + length xs) xs` as
  -- `ys` and `zs` respectively because this solution is simpler for Idris since it does not involve `Nat` division and other arithmetics.
  -- Standard library also seems to not to contain lemmas about `take` and `drop`, thus I need to formulate and prove them myself.
  -- It is possible, but tough.

-- Section 4.4.6 --

export
not_ev_3 : Not $ Ev 3
not_ev_3 (EvSS _) impossible

export
ev_suc_thus_not : Ev (S m) -> Not $ Ev m
ev_suc_thus_not (EvSS x) (EvSS y) = ev_suc_thus_not x y

-- Exercise 4.3 --

export
ev_ss_thus_ev : Ev (S $ S n) -> Ev n
ev_ss_thus_ev (EvSS x) = x

-- Exercise 4.4 --

-- Look to `not_ev_3` above. Solution is the same since there's no special method for __rule inversion__.

-- Exercise 4.5 --

-- Well, the solution is the same as in the chapter 3:
--iter_then_star : Iter r n x y -> Star r x y
--iter_then_star IterZ       = Refl
--iter_then_star (IterS x z) = Step x (iter_then_star z)

-- Exercise 4.6 --

-- `elems` is defined in `Data.InSet.List`.

falseNotTrue : Not (False = True)
falseNotTrue Refl impossible

namespace Exercise_4_6

  export %hint %inline
  UsedEquality : DecEq a => Equality a
  UsedEquality = PropositionalEq

  export
  list_splits : DecEq a => (xs : List a) -> (x : a) -> (x `isin` elems xs = True) -> (ys ** zs ** (xs = ys ++ x :: zs, x `isin` elems ys = False))
  list_splits [] x prf = absurd $ falseNotTrue rewrite sym $ not_in_empty x in prf
  list_splits (y::ys) x prf = case @@(x =?= y) of
    (True  ** p) => ([] ** ys ** (rewrite eq_val_to_prf {x} {y} @{PropositionalEq} p in Refl
                                , rewrite not_in_empty x in Refl))
    (False ** p) => let (subl ** subr ** (eq, f)) = list_splits ys x (is_in_tail x y (elems ys) p prf) in
                    (y::subl ** subr ** (rewrite eq in Refl, not_in_both x y (elems subl) p f))

-- Exercise 4.7 --

public export
balanced : Nat -> List Alpha -> Bool
balanced 0     []     = True
balanced n     (A::w) = balanced (S n) w
balanced (S n) (B::w) = balanced n w
balanced _     _      = False

replicate_appended : (n : Nat) -> (x : a) -> (w : List a) -> replicate n x ++ x::w = x :: replicate n x ++ w
replicate_appended 0     x w = Refl
replicate_appended (S n) x w = rewrite replicate_appended n x w in Refl

list_splits : (u, v, x, y : List a) -> u ++ v = x ++ y -> Either (m ** (u = x ++ m, y = m ++ v)) (m ** (x = u ++ m, v = m ++ y))
list_splits [] _ x  _ prf = Right (x ** (Refl, prf))
list_splits u  _ [] _ prf = Left  (u ** (Refl, sym prf))
list_splits (_::us) v (_::xs) y prf = rewrite fst $ consInjective prf in
                                      case list_splits us v xs y $ snd $ consInjective prf of
                                        Right (m ** (ux, vy)) => rewrite ux in Right (m ** (Refl, vy))
                                        Left  (m ** (ux, vy)) => rewrite ux in Left  (m ** (Refl, vy))

append_is_nil : (l, r : List a) -> l ++ r = [] -> (l = [], r = [])
append_is_nil [] [] Refl = (Refl, Refl)

append_is_singleton : (l, r : List a) -> (x : a) -> [x] = l ++ r -> Either (l = [x], r = []) (l = [], r = [x])
append_is_singleton [] [x] x Refl = Right (Refl, Refl)
append_is_singleton [x] [] x Refl = Left (Refl, Refl)
append_is_singleton [_] (_::_) _ Refl impossible
append_is_singleton (_::_::_) _ _ Refl impossible

analyze_s : S lr -> Either (lr = []) $
                    Either (w ** sw : S w ** lr = [A] ++ w ++ [B])
                           (w ** v ** sw : S w ** sv : S v ** lr = w ++ v)
analyze_s Empty = Left Refl
analyze_s (Asb {w} sw) = Right $ Left (w ** sw ** Refl)
analyze_s (Ss {w} {v} sw sv) = Right $ Right (w ** v ** sw ** sv ** Refl)

s_can_insert_ab : (l, r : List Alpha) -> S (l ++ r) -> S (l ++ [A, B] ++ r)
s_can_insert_ab l r s = case analyze_s s of
                          Left lr_nil => rewrite fst $ append_is_nil l r lr_nil in
                                         rewrite snd $ append_is_nil l r lr_nil in
                                         Asb Empty
                          Right $ Left (w ** sw ** eq) =>
                            case list_splits l r [A] (w ++ [B]) eq of
                              Left (m ** (l_Am, wB_mr)) => rewrite l_Am in case list_splits m r w [B] $ sym wB_mr of
                                Left (k ** (m_wk, kr)) => rewrite m_wk in case append_is_singleton k r B kr of
                                  Left  (kB, rn) => rewrite kB in
                                                    rewrite rn in
                                                    Ss (Asb sw) (Asb Empty)
                                  Right (kn, rB) => rewrite kn in
                                                    rewrite rB in
                                                    rewrite appendNilRightNeutral w in
                                                    rewrite appendAssociative w [A, B] [B] in
                                                    Asb $ Ss sw $ Asb Empty
                                Right (k ** (w_mk, r_kB)) =>
                                  rewrite r_kB in
                                  rewrite appendAssociative m (A::B::k) [B] in
                                  Asb $ s_can_insert_ab (assert_smaller l m) (assert_smaller r k) rewrite sym w_mk in sw
                              Right (m ** (lm, r_mwB)) => rewrite r_mwB in case append_is_singleton l m A lm of
                                Left (lA, mn) => rewrite lA in
                                                 rewrite mn in
                                                 Asb $ Ss (Asb Empty) sw
                                Right (ln, mA) => rewrite ln in
                                                  rewrite mA in
                                                  rewrite sym eq in
                                                  Ss (Asb Empty) s
                          Right $ Right (w ** v ** sw ** sv ** eq) => case list_splits l r w v eq of
                            Left (m ** (l_wm, v_rm)) =>
                              rewrite l_wm in
                              rewrite sym $ appendAssociative w m (A::B::r) in
                              Ss sw $ s_can_insert_ab (assert_smaller l m) r rewrite sym v_rm in sv
                            Right (m ** (w_lm, r_mv)) =>
                              rewrite r_mv in
                              rewrite appendAssociative l (A::B::m) v in
                              flip Ss sv $ s_can_insert_ab l (assert_smaller r m) rewrite sym w_lm in sw

init_last_decomp : (xs : List a) -> {auto ne : NonEmpty xs} -> xs = init xs ++ [last xs]
init_last_decomp (_::[])        = Refl
init_last_decomp (x::xs@(_::_)) = rewrite sym $ init_last_decomp xs in Refl

not_s_start_b : (w : List Alpha) -> Not $ S $ B::w
not_s_start_b _ Empty impossible

not_s_end_a : (w : List Alpha) -> Not $ S $ w ++ [A]
not_s_end_a [] Empty impossible
not_s_end_a (A::_) Empty impossible
not_s_end_a (B::_) Empty impossible

s_can_elim_ab : (l, r : List Alpha) -> S (l ++ [A, B] ++ r) -> S (l ++ r)
s_can_elim_ab [] r s = case analyze_s s of
  Right $ Left (w ** sw ** _) => case w of B::w' => absurd $ not_s_start_b w' sw
  Right $ Right (w ** v ** sw ** sv ** eq) => case w of
    [] => assert_total {-assert_smaller s sv-} $ s_can_elim_ab [] r rewrite eq in sv
    A::B::w' => rewrite snd $ consInjective $ snd $ consInjective eq in
                flip Ss sv $ assert_total {-assert_smaller s sw-} $ s_can_elim_ab [] w' sw
s_can_elim_ab (l::ls) [] s = rewrite appendNilRightNeutral ls in case analyze_s s of
  Right $ Left (w ** sw ** eq) => let u = fst $ snocInjective {xs=ls++[A]} {x=B} {ys=w} {y=B}
                                            rewrite sym $ appendAssociative ls [A] [B] in snd $ consInjective eq in
                                  absurd $ not_s_end_a ls rewrite u in sw
  Right $ Right (w ** v ** sw ** sv ** eq) => case list_splits (l::ls) [A, B] w v eq of
    Left (m ** (lls_wm, v_mAB)) => rewrite lls_wm in
                                   Ss sw $ the (S m) rewrite sym $ appendNilRightNeutral m in
                                             assert_total {-assert_smaller s sv-} s_can_elim_ab m [] rewrite sym v_mAB in sv
    Right (m ** (w_llsm, aB_mv)) => case m of
      [] => let u = fst $ snocInjective {xs=l::ls++[A]} {x=B} {ys=w++[A]} {y=B}
                      rewrite sym $ appendAssociative w [A] [B] in
                      rewrite aB_mv in
                      rewrite sym $ appendAssociative ls [A] [B] in
                      eq in
            rewrite fst $ snocInjective {xs=l::ls} u in sw
      A::m'::ms' => let (_, v_n) = append_is_nil _ _ $ sym $ snd $ consInjective $ snd $ consInjective aB_mv in
                    rewrite sym $ appendNilRightNeutral (l::ls) in
                    assert_total {-assert_smaller s sw-} $ s_can_elim_ab (l::ls) []
                      let u = the ([A, B] = A::m'::ms') $ rewrite sym $ appendNilRightNeutral ms' in rewrite sym v_n in aB_mv in
                      rewrite cong (ls ++) u in
                      rewrite sym w_llsm in
                      sw
s_can_elim_ab (l::ls) (r::rs) s = case analyze_s s of
  Right $ Left (w ** sw ** eq) => rewrite init_last_decomp (r::rs) in
                                  let (eq_l, eqL) = consInjective eq in
                                  let (eq_r, eqR) = snocInjective {xs=ls ++ A::B::init (r::rs)} {x=last $ r::rs} {y=B}
                                                      rewrite sym $ appendAssociative ls (init $ A::B::r::rs) [last $ A::B::r::rs] in
                                                      rewrite sym $ init_last_decomp $ A::B::r::rs in
                                                      eqL in
                                  rewrite eq_l in
                                  rewrite eqR in
                                  rewrite appendAssociative ls (init $ r::rs) [B] in
                                  Asb $ s_can_elim_ab ls (init $ r::rs) rewrite eq_r in sw
  Right $ Right (w ** v ** sw ** sv ** eq) => case list_splits (l::ls) (A::B::r::rs) w v eq of
    Left (m ** (lls_wm, w_ABrrs)) => rewrite cong (++ r::rs) lls_wm in
                                     rewrite sym $ appendAssociative w m (r::rs) in
                                     Ss sw $ assert_total {-assert_smaller s sv-} $ s_can_elim_ab m (r::rs) rewrite sym w_ABrrs in sv
    Right (m ** (w_llsm, aBrrs_mv)) => case m of
      [] => rewrite cong (++ r::rs) $ the (l::ls=w) rewrite sym $ appendNilRightNeutral ls in sym w_llsm in
            Ss sw $ s_can_elim_ab (assert_smaller (l::ls) []) (r::rs) rewrite aBrrs_mv in sv
      A::B::m' => rewrite snd $ consInjective $ snd $ consInjective aBrrs_mv in
                  rewrite appendAssociative (l::ls) m' v in
                  flip Ss sv $ s_can_elim_ab (l::ls) (assert_smaller (r::rs) m') rewrite sym w_llsm in sw
      A::A::_ => case fst $ consInjective $ snd $ consInjective aBrrs_mv of Refl impossible

balanced_appended : (n : Nat) -> (l, r : List Alpha) -> balanced n l = True -> balanced 0 r = True -> balanced n (l ++ r) = True
balanced_appended 0      []    _ _   prf = prf
balanced_appended 0     (A::l) r plf prf = balanced_appended 1 l r plf prf
balanced_appended (S n) (A::l) r plf prf = balanced_appended (S $ S n) l r plf prf
balanced_appended (S n) (B::l) r plf prf = balanced_appended n l r plf prf

-- There are a four statements instead of one because `balanced` is coded with `Bool` but `S.S` is inductive data type.

export
balanced_true_as_s : (n : Nat) -> (w : List Alpha) -> balanced n w = True -> S.S $ replicate n A ++ w
balanced_true_as_s 0     []     _   = Empty
balanced_true_as_s 0     (A::w) prf = balanced_true_as_s 1 w prf
balanced_true_as_s (S n) (A::w) prf = rewrite appendAssociative (replicate (S n) A) [A] w in
                                      rewrite replicate_appended n A [] in
                                      rewrite appendNilRightNeutral $ replicate n A in
                                      balanced_true_as_s (2 + n) w prf
balanced_true_as_s (S n) (B::w) prf = rewrite sym $ replicate_appended n A (B::w) in
                                      s_can_insert_ab (replicate n A) w $ balanced_true_as_s n w prf

export
s_as_balanced_true : (n : Nat) -> (w : List Alpha) -> S.S $ replicate n A ++ w -> balanced n w = True
s_as_balanced_true 0 [] Empty = Refl
s_as_balanced_true 0 (A :: w ++ [B]) (Asb x) = s_as_balanced_true 1 (w ++ [B]) (Asb x)
s_as_balanced_true 0 (w ++ v) (Ss x y) = let xx = assert_total $ s_as_balanced_true 0 w x in
                                         let yy = assert_total $ s_as_balanced_true 0 v y in
                                         balanced_appended 0 w v xx yy
s_as_balanced_true (S n) [] Empty impossible
s_as_balanced_true (S n) (A::w) x = s_as_balanced_true (S $ S n) w rewrite sym $ replicate_appended n A w in x
s_as_balanced_true (S n) (B::w) x = s_as_balanced_true n w $ s_can_elim_ab (replicate n A) w rewrite replicate_appended n A (B::w) in x

export
balanced_false_as_not_s : (n : Nat) -> (w : List Alpha) -> balanced n w = False -> Not $ S.S $ replicate n A ++ w
balanced_false_as_not_s n w prf s = falseNotTrue $ rewrite sym prf in s_as_balanced_true n w s

export
not_s_as_balanced_false : (n : Nat) -> (w : List Alpha) -> Not $ S.S $ replicate n A ++ w -> balanced n w = False
not_s_as_balanced_false n w f = case decEq (balanced n w) False of
  Yes p => p
  No no => absurd $ f $ balanced_true_as_s n w $ notFalseIsTrue no

max_stars_repo_name: buzden/prog-prove-exercises

max_issues_repo_name: buzden/prog-prove-exercises

max_forks_repo_name: buzden/prog-prove-exercises


text:
module Prims

x:Int
x=42

foo:String
foo="Sausage machine"

bar:Char
bar='Z'

quux:Bool
quux=False

myplus:Nat->Nat->Nat
myplus Z y = y
myplus (S k) y = S (plus k y)

myreverse : List a -> List a
myreverse xs = revAcc [] xs where
  revAcc : List a -> List a -> List a
  revAcc acc [] = acc
  revAcc acc (x::xs) = revAcc (x::acc) xs

foo2 : Int -> Int
foo2 x = case isLT of
          Yes => x*2
          No => x*4
      where
        data myLT = Yes | No
        isLT:myLT
        isLT = if x <20 then Yes else No

even : Nat -> Bool
even Z = True
even (S k) = odd k where
  odd Z = False
  odd (S k) = even k

max_stars_repo_name: shij-hsu/idr

max_issues_repo_name: shij-hsu/idr

max_forks_repo_name: shij-hsu/idr


text:
-- Exercises_5_3.idr

-- Read a List from stdin and write content to given file

import Data.Vect

||| Reads a list of strings from stdin, until a blank line is given
readToBlank : IO (List String)
readToBlank = do putStrLn "Enter text (blank line to end):"
                 x <- getLine
                 if x == ""
                    then pure []
                    else do xs <- readToBlank
                            pure (x :: xs)

||| Converts a list of strings to a single string,
||| where each list entry is separated by newline
||| @ls List of String
spreadListToLines : (ls : List String) -> String
spreadListToLines [] = "\n"
spreadListToLines (x :: xs) = x ++ "\n" ++ spreadListToLines xs

||| Reads a list of string from stdin and writes it
||| to the given filename
readAndSave : IO ()
readAndSave = do
  ls <- readToBlank
  putStr "Enter filename: "
  fileName <- getLine
  Right () <- writeFile fileName (spreadListToLines ls)
  putStrLn ("Data written to file " ++ fileName ++ "\n")

readLines : (fid : File) -> IO (n : Nat ** Vect n String)
readLines fid = do
  eof <- fEOF fid
  if eof
     then pure (_ ** [])
     else do Right x <- fGetLine fid | Left err => do
                   putStrLn ("Error: " ++ (show err))
                   pure (_ ** [])
             (_ ** xs) <- readLines fid
             pure (_ ** (x :: xs))

||| Read a Vect of string from a given file.
||| Each line is an Vect entry
readVectFile : (filename : String) -> IO (n ** Vect n String)
readVectFile filename = do
  Right fid <- openFile filename Read | Left err => do
    putStrLn ("Error: " ++ (show err))
    pure (0 ** [])
  readLines fid

max_stars_repo_name: kkirstein/proglang-playground

max_issues_repo_name: kkirstein/proglang-playground

max_forks_repo_name: kkirstein/proglang-playground


text:
module Commons.Text.Parser.Location

import Text.Lexer
import Text.Parser

import Commons.Data.Location
import Commons.Text.Parser.Support

%default total
%access export

column : RuleEmpty tok Nat
column = do
  tok <- peek
  pure ((toNat . col) tok)

location : RuleEmpty tok Location
location = do
  tok <- peek
  pure (MkLoc Nothing ((toNat . line) tok) ((toNat . col) tok))

namespace WithFileName
  location : String -> RuleEmpty tok Location
  location fname = do
    l <- location
    pure (record { source = Just fname} l)

max_stars_repo_name: jfdm/idris-common

max_issues_repo_name: jfdm/idris-common

max_forks_repo_name: jfdm/idris-common


text:
import Data.Vect

-- Reimplement transpose_mat using zipWith instead of transpose_helper.

create_empties : Vect n (Vect 0 elem)
create_empties = replicate _ []

transpose_helper : (x : Vect n elem) ->
                   (xs_trans : Vect n (Vect k elem)) ->
                   Vect n (Vect (S k) elem)
transpose_helper [] [] = []
transpose_helper (x :: xs) (y :: ys) = (x :: y) :: transpose_helper xs ys

transpose_mat : Vect m (Vect n elem) -> Vect n (Vect m elem)
transpose_mat [] = create_empties
transpose_mat (x :: xs) = let xs_trans = transpose_mat xs in
                              zipWith (::) x xs_trans

-- *ex_3_3_3> transpose_mat [[1,2], [3,4], [5,6]]
-- [[1, 3, 5], [2, 4, 6]] : Vect 2 (Vect 3 Integer)

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


text:
%noinline %inline
foo : Int -> Int
foo x = x


text:
module Extra.Pair

infixl 0 :>

||| A pair with its second argument being lazy, heavily using in `Extra.Streaming`
public export
data Of : (a : Type) -> (b : Type) -> Type where
  (:>) : a -> Lazy b -> Of a b

export
Bifunctor Of where
  mapFst f (a :> b) = f a :> b
  mapSnd f (a :> b) = a :> f b
  bimap f g (a :> b) = f a :> g b

export
Functor (Of a) where
  map = mapSnd


text:
-- SPDX-FileCopyrightText: 2021 The ipkg-idr developers
--
-- SPDX-License-Identifier: MPL-2.0

module TestRunner

import Language.IPKG

import System
import System.File

parseIPKGFile : (path : String) -> IO ()
parseIPKGFile path = do
    putStrLn $ "Parsing file " ++ show path

    Right src <- readFile path
        | Left err => do
            putStrLn $ "Error reading file: " ++ show err
            pure ()

    Right pkg <- pure $ parseIPKG src
        | Left err => do
            putStrLn $ "Error parsing file: " ++ err
            pure ()

    printLn pkg

main : IO ()
main = do
    (_ :: args) <- getArgs
        | [] => pure ()
    for_ args \path => do
        parseIPKGFile path

max_stars_repo_name: tiatomee/ipkg-idr

max_issues_repo_name: tiatomee/ipkg-idr

max_forks_repo_name: tiatomee/ipkg-idr


text:
module Util

import Data.List

infixl 1 <&>
export
(<&>) : Functor f => f a -> (a -> b) -> f b
x <&> f = f <$> x

infixl 4 <$,$>

-- For when Lazy is causing type problems
infixr 4 &&|
export
(&&|) : Bool -> Bool -> Bool
(&&|) x y = x && y

export
catMaybes : List (Maybe a) -> List a
catMaybes z = foldr (\m,f => maybe f (\x => (x ::) . f) m) id z []

export
unzip : List (a,b) -> (List a, List b)
unzip = foldr (\(x,y),(xs,ys) => (x :: xs, y :: ys)) ([],[])

export
isJust : Maybe a -> Bool
isJust (Just _ ) = True
isJust _ = False

export
unless : Applicative f => Bool -> Lazy (f ()) -> f ()
unless b act = if b then pure () else act

-- slow, preserves order
export
difference : Eq a => List a -> List a -> List a
difference xs ys = foldr (\y,xs => delete y xs) xs ys

-- TODO: bring this up with other devs for idris about it's merits and negatives
-- Intended use is to crash in places that crashing is correct to do because the
-- failure isn't recoverable anyway
export
total -- the lie
%foreign "scheme:lambda (x) (blodwen-error-quit x)"
         -- "javascript:lambda:(x)=>{throw new IdrisError(x)}"
lie_idris_crash : String -> a


text:
module Circuits.Split

import Decidable.Equality
import Data.Nat

import Toolkit.Decidable.Informative
import Toolkit.Data.Whole

%default total

namespace EdgeCase

  ||| Index for indexing the first and last elements.
  |||
  ||| These will result in a *single* free vector returned.
  public export
  data Index : (vSize : Whole)
            -> (idx   : Nat)
            -> (free  : Whole)
                     -> Type
    where
      ||| Edgecase for a pivot of value 0, implies that the length of vector is >=2
      First : Index (W (S (S n)) ItIsSucc)
                             Z
                    (W    (S n)  ItIsSucc)
      ||| Edgecase for a vector with length >= 2 where pivot is length - 1
      Last  : Index (W (S (S n)) ItIsSucc)
                          (S n)
                    (W    (S n)  ItIsSucc)

  Uninhabited (s ** Index (W (S Z) ItIsSucc) pivot s) where
    uninhabited (MkDPair _ _) impossible

  urgh : (S k = S j -> Void) -> DPair Whole (\s => Index (W (S (S k)) ItIsSucc) (S j) s) -> Void
  urgh f (MkDPair (W (S j) ItIsSucc) Last) = f Refl
--

  public export
  data Error = VectIsOne
             | InvalidPivot Nat Nat

  export
  index : (size  : Whole)
       -> (pivot : Nat)
                -> DecInfo Error (s ** Index size pivot s)

  -- [ NOTE ] Vector of length cannot be indexed with remaining slots
  index (W (S 0) ItIsSucc) 0
    = No VectIsOne absurd

  -- [ NOTE ] Selecting first element
  index (W (S (S k)) ItIsSucc) 0
    = Yes (MkDPair (W (S k) ItIsSucc) First)

  -- [ NOTE ] Selecting last element
  index (W (S 0) ItIsSucc) (S j)
    = No VectIsOne absurd

  index (W (S (S k)) ItIsSucc) (S j) with (decEq (S k) (S j))
    index (W (S (S k)) ItIsSucc) (S k) | (Yes Refl)
      = Yes (MkDPair (W (S k) ItIsSucc) Last)
    index (W (S (S k)) ItIsSucc) (S j) | (No contra)
      = No (InvalidPivot (S j) (S (S k))) (urgh contra)

namespace Pivot

  ||| Index a vector such that we return the length of the unused vectors to the left and right of the pivot.
  |||
  ||| We decrement the pivot until we reach the position in the vector we require.
  ||| For the left half we increment from zero.
  ||| For the right half we decrement from the length of the vector.
  public export
  data Index : (left_counter  : Nat)
            -> (pivot         : Nat)
            -> (right_counter : Whole)
            -> (a,b : Whole) -- results
                     -> Type
    where
      ||| Stop counting when we reach the pivot.
      |||
      ||| The stopping condition is that:
      |||
      ||| + The left half is at least one;
      ||| + The right half is at least one;
      ||| + This implies that the vector is at least length three;
      |||
      Stop : Index (S l)              -- left of pivot
                   Z                  -- empty pivot
                   (W (S (S r)) ItIsSucc) -- right of pivot
                   (W    (S l)  ItIsSucc)
                   (W    (S r)  ItIsSucc)

      ||| Reduce the size of the pivot, and update the counters.
      Step : Index (S l)   p  (W    (S r)  ItIsSucc) a b
          -> Index    l (S p) (W (S (S r)) ItIsSucc) a b

  Uninhabited ((a ** b ** Index Z Z r a b)) where
    uninhabited (MkDPair _ (MkDPair _ _)) impossible

  Uninhabited ((a ** b ** Index l (S p) (W (S Z) ItIsSucc) a b)) where
    uninhabited (MkDPair _ (MkDPair _ _)) impossible

  Uninhabited ((a ** b ** Index (S l) Z (W (S Z) ItIsSucc) a b)) where
    uninhabited (MkDPair _ (MkDPair _ _)) impossible

  public export
  data Error = IsEdgeCase | OutOfBounds

  outOfFuel : ((a ** b ** Index (S l)    k  (W    (S j)  ItIsSucc) a b) -> Void)
           ->  (a ** b ** Index    l  (S k) (W (S (S j)) ItIsSucc) a b) -> Void
  outOfFuel contra (MkDPair a (MkDPair b (Step x))) = contra (MkDPair a (MkDPair b x))

  index' : (l,p : Nat)
        -> (r   : Whole)
               -> DecInfo Pivot.Error (a ** b ** Index l p r a b)

  index' 0 Z r
    = No IsEdgeCase absurd

  index' (S k) Z (W (S Z) ItIsSucc)
    = No IsEdgeCase absurd

  index' (S k) Z (W (S (S j)) ItIsSucc)
    = Yes (MkDPair (W (S k) ItIsSucc) (MkDPair (W (S j) ItIsSucc) Stop))

  index' l (S k) (W (S 0) ItIsSucc)
    = No OutOfBounds absurd

  index' l (S k) (W (S (S j)) ItIsSucc) with (index' (S l) k (W (S j) ItIsSucc))
    index' l (S k) (W (S (S j)) ItIsSucc) | (Yes (MkDPair a (MkDPair b prf)))
      = Yes (MkDPair a (MkDPair b (Step prf)))

    index' l (S k) (W (S (S j)) ItIsSucc) | (No msgWhyNot prfWhyNot)
      = No msgWhyNot (outOfFuel prfWhyNot)

  export
  index : (p : Nat)
       -> (r : Whole)
            -> DecInfo Pivot.Error (a ** b ** Index Z p r a b)
  index = index' Z

namespace Join

  public export
  data Plus : (a,b,c : Nat) -> Type where
    Stop : Plus Z b b
    Step : Plus    a  b    c
        -> Plus (S a) b (S c)

  export
  plus : (a,b : Nat) -> DPair Nat (Plus a b)
  plus Z b
    = MkDPair b Stop
  plus (S k) b with (Join.plus k b)
    plus (S 0) b | (MkDPair b Stop)
      = MkDPair (S b) (Step Stop)

    plus (S (S a)) b | (MkDPair (S c) (Step x))
      = MkDPair (S (S c)) (Step (Step x))

  errWhenZ : (b = c -> Void) -> Plus 0 b c -> Void
  errWhenZ f Stop = f Refl

  cIsZero : Plus (S k) b 0 -> Void
  cIsZero Stop impossible
  cIsZero (Step x) impossible

  errIsLater : (Plus k b j -> Void) -> Plus (S k) b (S j) -> Void
  errIsLater f (Step x) = f x

  export
  isPlus : (a,b,c : Nat) -> Dec (Plus a b c)
  isPlus Z b c with (decEq b c)
    isPlus Z b b | (Yes Refl)
      = Yes Stop

    isPlus Z b c | (No contra)
      = No (errWhenZ contra)

  isPlus (S k) b 0
    = No cIsZero

  isPlus (S k) b (S j) with (isPlus k b j)
    isPlus (S k) b (S j) | (Yes prf)
      = Yes (Step prf)

    isPlus (S k) b (S j) | (No contra)
      = No (errIsLater contra)

  namespace Whole
    public export
    data Plus : (a,b,c : Whole) -> Type where
      P : (comp : Join.Plus (S a) (S b) (S c))
               -> Plus (W (S a) ItIsSucc)
                       (W (S b) ItIsSucc)
                       (W (S c) ItIsSucc)
    export
    plus : (a,b : Whole) -> DPair Whole (Plus a b)
    plus (W (S n) ItIsSucc) (W (S j) ItIsSucc) with (Join.plus n (S j))
      plus (W (S n) ItIsSucc) (W (S j) ItIsSucc) | (MkDPair c prf)
        = (W (S c) ItIsSucc ** P (Step prf))

    isNotPlus : (Plus (S a) (S b) (S c) -> Void) -> Plus (W (S a) ItIsSucc) (W (S b) ItIsSucc) (W (S c) ItIsSucc) -> Void
    isNotPlus f (P comp) = f comp

    export
    isPlus : (a,b,c : Whole) -> Dec (Plus a b c)
    isPlus (W (S a) ItIsSucc) (W (S b) ItIsSucc) (W (S c) ItIsSucc) with (isPlus (S a) (S b) (S c))
      isPlus (W (S a) ItIsSucc) (W (S b) ItIsSucc) (W (S c) ItIsSucc) | (Yes prf)
        = Yes (P prf)
      isPlus (W (S a) ItIsSucc) (W (S b) ItIsSucc) (W (S c) ItIsSucc) | (No contra)
        = No (isNotPlus contra)

-- [ EOF ]


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

import System.File

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

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

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

lenEq : Nat -> String -> Bool
lenEq n s = length s == n

sortString : String -> String
sortString s = pack $ sort $ unpack s

decodeall : List String -> Maybe (List (String, String))
decodeall l = do one <- find (lenEq 2) l
                 four <- find (lenEq 4) l
                 seven <- find (lenEq 3) l
                 eight <- find (lenEq 7) l
                 let zeroorsixornine = filter (lenEq 6) l
                 nine <- find (\x => (==) 4 $ length $ intersect (unpack x) (unpack four)) zeroorsixornine
                 let zeroorsix = delete nine zeroorsixornine
                 six <- find (\x => (==) 1 $ length $ intersect (unpack x) (unpack one)) zeroorsix
                 zero <- head' $ delete six $ zeroorsix
                 let twothreeorfive = filter (lenEq 5) l
                 three <- find (\x => (==) 2 $ length $ intersect (unpack x) (unpack one)) twothreeorfive
                 let twoorfive = delete three twothreeorfive
                 two <- find (\x => (==) 2 $ length $ ((\\) `on` unpack) six x) twoorfive
                 five <- head' $ delete three $ delete two $ twoorfive
                 pure $ [
                   (sortString $ zero, "0"),
                   (sortString $ one, "1"),
                   (sortString $ two, "2"),
                   (sortString $ three, "3"),
                   (sortString $ four, "4"),
                   (sortString $ five, "5"),
                   (sortString $ six, "6"),
                   (sortString $ seven, "7"),
                   (sortString $ eight, "8"),
                   (sortString $ nine, "9")
                   ]

decode : (List String, List String) -> Maybe Nat
decode (i, o) = do m <- decodeall i
                   parsePositive $ fastAppend $ catMaybes $ ((flip lookup) m . sortString <$> o)

run : String -> IO String
run s = do let l = parseLines parseOutput s
           let r = sum $ catMaybes $ decode <$> l
           pure $ show r

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


text:
module WebAssembly.Validation.Modules.Functions

import WebAssembly.Structure
import WebAssembly.Validation.Conventions
import WebAssembly.Validation.Instructions
import WebAssembly.Validation.Types

||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/modules.html#functions)
|||
||| ```
||| C.types[x] = [t1*] -> [t2*]    C,locals t1* t*, labels [t2*], return [t2*] ⊢ expr : [t2*]
||| -----------------------------------------------------------------------------------------
||| C ⊢ {type x, locals t*, body expr} : [t1*] -> [t2*]
||| ```
public export
data ValidFunc : Context -> Func -> FuncType -> Type where
 MkValidFunc : (c : Context)
            -> (x : TypeIdx)
            -> (t : ResultType)
            -> (t1 : ResultType)
            -> (t2 : ResultType)
            -> (expr : Expr)
            -> {auto in_bounds: InBounds x (types c)}
            -> (index x (types c) = (t1 ->> t2))
            -> ValidSequence (record {locals = (t1 ++ t), labels = [t2], return = (Just t2)} c) expr ([] ->> t2)
            -> ValidFunc c (MkFunc x t expr) (t1 ->> t2)

max_stars_repo_name: RaoulSchaffranek/idris-webassembly

max_issues_repo_name: RaoulSchaffranek/idris-webassembly

max_forks_repo_name: RaoulSchaffranek/idris-webassembly


text:
module Metamorphic

-- Based on https://bitbucket.org/josh-hs-ko/MetamorphismsInAgda/raw/master/MetamorphismsInAgda.pdf

data AlgList : (a : Type) -> {s : Type} -> (f : a -> s -> s) -> (e : s) -> s -> Type where
  Nil : AlgList a f e e
  (::) : (x : a) -> {st : s} -> AlgList a f e st -> AlgList a f e (f x st)

codata CoAlgList : (b : Type) -> {s : Type} -> (g : s -> Maybe (b, s)) -> s -> Type where
  Empty : {st : s} -> g st = Nothing -> CoAlgList b g st
  Cons : (x : b) -> {st, st' : s} -> g st = Just (x, st') -> CoAlgList b g st' -> CoAlgList b g st

testAlgList : AlgList Nat (\x, s => x + s) 0 3
testAlgList = 1 :: 1 :: 1 :: Nil

testCoAlgList : (st : Nat) -> CoAlgList Nat (\x => Just (x, S x)) st
testCoAlgList st = Cons st Refl (testCoAlgList (S st))

fromLeftAlg : {a, s : Type} -> (s -> a -> s) -> a -> (s -> s) -> (s -> s)
fromLeftAlg f a s = s . flip f a

parameters (a : Type, b : Type, s : Type, f : s -> a -> s, g : s -> Maybe (b, s),
            sc : {x : a} -> {y : b} -> {st, st' : s} -> g st = Just (y, st') -> g (f st x) = Just (y, f st' x))

  cbp : (st : s) -> {h : s -> s} -> AlgList a (fromLeftAlg f) (\x => x) h -> CoAlgList b g (h st)
  cbp s [] with (g s) proof prf
    cbp s [] | Nothing = Empty (sym prf)
    cbp s [] | Just (y, s') = Cons y (sym prf) (cbp s' [])
  cbp s (a :: as) = cbp (f s a) as

  lemma : {st : s} -> {y : b} -> {st' : s} -> {h : s -> s} -> AlgList a (fromLeftAlg f) (\x => x) h -> g st = Just (y, st') -> g (h st) = Just (y, h st')
  lemma [] eq = eq
  lemma (a :: as) eq = lemma as (sc eq)

  stream : (st : s) -> {h : s -> s} -> AlgList a (fromLeftAlg f) (\x => x) h -> CoAlgList b g (h st)
  stream s as with (g s) proof prf
    stream s [] | Nothing  = Empty (sym prf)
    stream s (a :: as) | Nothing  = stream (f s a) as
    stream s as | Just (y, s') = Cons y (lemma as (sym prf)) (stream s' as)

max_stars_repo_name: STELIORD/idris-snippets

max_issues_repo_name: stjordanis/idris-snippets

max_forks_repo_name: stjordanis/idris-snippets