text:
module Data.List

import Data.Nat
import Data.List1
import Data.Fin
import public Data.Zippable

%default total

public export
isNil : List a -> Bool
isNil [] = True
isNil _  = False

public export
isCons : List a -> Bool
isCons [] = False
isCons _  = True

public export
snoc : List a -> a -> List a
snoc xs x = xs ++ [x]

public export
take : Nat -> List a -> List a
take (S k) (x :: xs) = x :: take k xs
take _ _ = []

public export
drop : (n : Nat) -> (xs : List a) -> List a
drop Z     xs      = xs
drop (S n) []      = []
drop (S n) (_::xs) = drop n xs

||| Satisfiable if `k` is a valid index into `xs`.
|||
||| @ k  the potential index
||| @ xs the list into which k may be an index
public export
data InBounds : (k : Nat) -> (xs : List a) -> Type where
    ||| Z is a valid index into any cons cell
    InFirst : InBounds Z (x :: xs)
    ||| Valid indices can be extended
    InLater : InBounds k xs -> InBounds (S k) (x :: xs)

public export
Uninhabited (InBounds k []) where
  uninhabited InFirst impossible
  uninhabited (InLater _) impossible

export
Uninhabited (InBounds k xs) => Uninhabited (InBounds (S k) (x::xs)) where
  uninhabited (InLater y) = uninhabited y

||| Decide whether `k` is a valid index into `xs`.
public export
inBounds : (k : Nat) -> (xs : List a) -> Dec (InBounds k xs)
inBounds _ [] = No uninhabited
inBounds Z (_ :: _) = Yes InFirst
inBounds (S k) (x :: xs) with (inBounds k xs)
  inBounds (S k) (x :: xs) | (Yes prf) = Yes (InLater prf)
  inBounds (S k) (x :: xs) | (No contra)
      = No $ \(InLater y) => contra y

||| Find a particular element of a list.
|||
||| @ ok a proof that the index is within bounds
public export
index : (n : Nat) -> (xs : List a) -> {auto 0 ok : InBounds n xs} -> a
index Z (x :: xs) {ok = InFirst} = x
index (S k) (_ :: xs) {ok = InLater _} = index k xs

public export
index' : (xs : List a) -> Fin (length xs) -> a
index' (x::_)  FZ     = x
index' (_::xs) (FS i) = index' xs i

||| Generate a list by repeatedly applying a partial function until exhausted.
||| @ f the function to iterate
||| @ x the initial value that will be the head of the list
covering
public export
iterate : (f : a -> Maybe a) -> (x : a) -> List a
iterate f x  = x :: case f x of
  Nothing => []
  Just y => iterate f y

covering
public export
unfoldr : (b -> Maybe (a, b)) -> b -> List a
unfoldr f c = case f c of
  Nothing     => []
  Just (a, n) => a :: unfoldr f n

public export
iterateN : Nat -> (a -> a) -> a -> List a
iterateN Z     _ _ = []
iterateN (S n) f x = x :: iterateN n f (f x)

public export
takeWhile : (p : a -> Bool) -> List a -> List a
takeWhile p []      = []
takeWhile p (x::xs) = if p x then x :: takeWhile p xs else []

public export
dropWhile : (p : a -> Bool) -> List a -> List a
dropWhile p []      = []
dropWhile p (x::xs) = if p x then dropWhile p xs else x::xs

||| Applied to a predicate and a list, returns the list of those elements that
||| satisfy the predicate.
public export
filter : (p : a -> Bool) -> List a -> List a
filter p [] = []
filter p (x :: xs)
   = if p x
        then x :: filter p xs
        else filter p xs

||| Find the first element of the list that satisfies the predicate.
public export
find : (p : a -> Bool) -> (xs : List a) -> Maybe a
find p [] = Nothing
find p (x::xs) = if p x then Just x else find p xs

||| Find the index and proof of InBounds of the first element (if exists) of a
||| list that satisfies the given test, else `Nothing`.
public export
findIndex : (a -> Bool) -> (xs : List a) -> Maybe $ Fin (length xs)
findIndex _ [] = Nothing
findIndex p (x :: xs) = if p x
  then Just FZ
  else FS <$> findIndex p xs

||| Find indices of all elements that satisfy the given test.
public export
findIndices : (a -> Bool) -> List a -> List Nat
findIndices p = h 0 where
  h : Nat -> List a -> List Nat
  h _         []  = []
  h lvl (x :: xs) = if p x
    then lvl :: h (S lvl) xs
    else        h (S lvl) xs

||| Find associated information in a list using a custom comparison.
public export
lookupBy : (a -> a -> Bool) -> a -> List (a, b) -> Maybe b
lookupBy p e []      = Nothing
lookupBy p e ((l, r) :: xs) =
  if p e l then
    Just r
  else
    lookupBy p e xs

||| Find associated information in a list using Boolean equality.
public export
lookup : Eq a => a -> List (a, b) -> Maybe b
lookup = lookupBy (==)

||| Check if something is a member of a list using a custom comparison.
public export
elemBy : (a -> a -> Bool) -> a -> List a -> Bool
elemBy p e []      = False
elemBy p e (x::xs) = p e x || elemBy p e xs

public export
nubBy : (a -> a -> Bool) -> List a -> List a
nubBy = nubBy' []
  where
    nubBy' : List a -> (a -> a -> Bool) -> List a -> List a
    nubBy' acc p []      = []
    nubBy' acc p (x::xs) =
      if elemBy p x acc then
        nubBy' acc p xs
      else
        x :: nubBy' (x::acc) p xs

||| O(n^2). The nub function removes duplicate elements from a list. In
||| particular, it keeps only the first occurrence of each element. It is a
||| special case of nubBy, which allows the programmer to supply their own
||| equality test.
|||
||| ```idris example
||| nub (the (List _) [1,2,1,3])
||| ```
public export
nub : Eq a => List a -> List a
nub = nubBy (==)

||| The deleteBy function behaves like delete, but takes a user-supplied equality predicate.
public export
deleteBy : (a -> a -> Bool) -> a -> List a -> List a
deleteBy _  _ []      = []
deleteBy eq x (y::ys) = if x `eq` y then ys else y :: deleteBy eq x ys

||| `delete x` removes the first occurrence of `x` from its list argument. For
||| example,
|||
|||````idris example
|||delete 'a' ['b', 'a', 'n', 'a', 'n', 'a']
|||````
|||
||| It is a special case of deleteBy, which allows the programmer to supply
||| their own equality test.
public export
delete : Eq a => a -> List a -> List a
delete = deleteBy (==)

||| Delete the first occurrence of each element from the second list in the first
||| list where equality is determined by the predicate passed as the first argument.
||| @ p            A function that returns true when its two arguments should be considered equal.
||| @ source       The list to delete elements from.
||| @ undesirables The list of elements to delete.
public export
deleteFirstsBy : (p : a -> a -> Bool) -> (source : List a) -> (undesirables : List a) -> List a
deleteFirstsBy p = foldl (flip (deleteBy p))

infix 7 \\

||| The non-associative list-difference.
||| A specialized form of @deleteFirstsBy@ where the predicate is equality under the @Eq@
||| interface.
||| Deletes the first occurrence of each element of the second list from the first list.
|||
||| In the following example, the result is `[2, 4]`.
||| ```idris example
||| [1, 2, 3, 4] // [1, 3]
||| ```
|||
public export
(\\) : (Eq a) => List a -> List a -> List a
(\\) = foldl (flip delete)

||| The unionBy function returns the union of two lists by user-supplied equality predicate.
public export
unionBy : (a -> a -> Bool) -> List a -> List a -> List a
unionBy eq xs ys = xs ++ foldl (flip (deleteBy eq)) (nubBy eq ys) xs

||| Compute the union of two lists according to their `Eq` implementation.
|||
||| ```idris example
||| union ['d', 'o', 'g'] ['c', 'o', 'w']
||| ```
|||
public export
union : Eq a => List a -> List a -> List a
union = unionBy (==)

||| Like @span@ but using a predicate that might convert a to b, i.e. given a
||| predicate from a to Maybe b and a list of as, returns a tuple consisting of
||| the longest prefix of the list where a -> Just b, and the rest of the list.
public export
spanBy : (a -> Maybe b) -> List a -> (List b, List a)
spanBy p [] = ([], [])
spanBy p (x :: xs) = case p x of
  Nothing => ([], x :: xs)
  Just y => let (ys, zs) = spanBy p xs in (y :: ys, zs)

||| Given a predicate and a list, returns a tuple consisting of the longest
||| prefix of the list whose elements satisfy the predicate, and the rest of the
||| list.
public export
span : (a -> Bool) -> List a -> (List a, List a)
span p []      = ([], [])
span p (x::xs) =
  if p x then
    let (ys, zs) = span p xs in
        (x::ys, zs)
  else
    ([], x::xs)

public export
break : (a -> Bool) -> List a -> (List a, List a)
break p xs = span (not . p) xs

public export
split : (a -> Bool) -> List a -> List1 (List a)
split p xs =
  case break p xs of
    (chunk, [])          => singleton chunk
    (chunk, (c :: rest)) => chunk ::: forget (split p (assert_smaller xs rest))

public export
splitAt : (n : Nat) -> (xs : List a) -> (List a, List a)
splitAt Z xs = ([], xs)
splitAt (S k) [] = ([], [])
splitAt (S k) (x :: xs)
      = let (tk, dr) = splitAt k xs in
            (x :: tk, dr)

public export
partition : (a -> Bool) -> List a -> (List a, List a)
partition p []      = ([], [])
partition p (x::xs) =
  let (lefts, rights) = partition p xs in
    if p x then
      (x::lefts, rights)
    else
      (lefts, x::rights)

||| The inits function returns all initial segments of the argument, shortest
||| first. For example,
|||
||| ```idris example
||| inits [1,2,3]
||| ```
public export
inits : List a -> List (List a)
inits xs = [] :: case xs of
  []        => []
  x :: xs'  => map (x ::) (inits xs')

||| The tails function returns all final segments of the argument, longest
||| first. For example,
|||
||| ```idris example
||| tails [1,2,3] == [[1,2,3], [2,3], [3], []]
|||```
public export
tails : List a -> List (List a)
tails xs = xs :: case xs of
  []        => []
  _ :: xs'  => tails xs'

||| Split on the given element.
|||
||| ```idris example
||| splitOn 0 [1,0,2,0,0,3]
||| ```
|||
public export
splitOn : Eq a => a -> List a -> List1 (List a)
splitOn a = split (== a)

public export
replaceWhen : (a -> Bool) -> a -> List a -> List a
replaceWhen p b l = map (\c => if p c then b else c) l

||| Replaces all occurences of the first argument with the second argument in a list.
|||
||| ```idris example
||| replaceOn '-' ',' ['1', '-', '2', '-', '3']
||| ```
|||
public export
replaceOn : Eq a => a -> a -> List a -> List a
replaceOn a = replaceWhen (== a)

||| Construct a list with `n` copies of `x`.
||| @ n how many copies
||| @ x the element to replicate
public export
replicate : (n : Nat) -> (x : a) -> List a
replicate Z     _ = []
replicate (S n) x = x :: replicate n x

||| Compute the intersect of two lists by user-supplied equality predicate.
export
intersectBy : (a -> a -> Bool) -> List a -> List a -> List a
intersectBy eq xs ys = [x | x <- xs, any (eq x) ys]

||| Compute the intersect of two lists according to the `Eq` implementation for the elements.
export
intersect : Eq a => List a -> List a -> List a
intersect = intersectBy (==)

export
intersectAllBy : (a -> a -> Bool) -> List (List a) -> List a
intersectAllBy eq [] = []
intersectAllBy eq (xs :: xss) = filter (\x => all (elemBy eq x) xss) xs

export
intersectAll : Eq a => List (List a) -> List a
intersectAll = intersectAllBy (==)

---------------------------
-- Zippable --
---------------------------

public export
Zippable List where
  zipWith _ [] _ = []
  zipWith _ _ [] = []
  zipWith f (x :: xs) (y :: ys) = f x y :: zipWith f xs ys

  zipWith3 _ [] _ _ = []
  zipWith3 _ _ [] _ = []
  zipWith3 _ _ _ [] = []
  zipWith3 f (x :: xs) (y :: ys) (z :: zs) = f x y z :: zipWith3 f xs ys zs

  unzipWith f [] = ([], [])
  unzipWith f (x :: xs) = let (b, c) = f x
                              (bs, cs) = unzipWith f xs in
                              (b :: bs, c :: cs)

  unzipWith3 f [] = ([], [], [])
  unzipWith3 f (x :: xs) = let (b, c, d) = f x
                               (bs, cs, ds) = unzipWith3 f xs in
                               (b :: bs, c :: cs, d :: ds)

---------------------------
-- Non-empty List
---------------------------

public export
data NonEmpty : (xs : List a) -> Type where
    IsNonEmpty : NonEmpty (x :: xs)

export
Uninhabited (NonEmpty []) where
  uninhabited IsNonEmpty impossible

||| Get the head of a non-empty list.
||| @ ok proof the list is non-empty
public export
head : (l : List a) -> {auto 0 ok : NonEmpty l} -> a
head [] impossible
head (x :: _) = x

||| Get the tail of a non-empty list.
||| @ ok proof the list is non-empty
public export
tail : (l : List a) -> {auto 0 ok : NonEmpty l} -> List a
tail [] impossible
tail (_ :: xs) = xs

||| Retrieve the last element of a non-empty list.
||| @ ok proof that the list is non-empty
public export
last : (l : List a) -> {auto 0 ok : NonEmpty l} -> a
last [] impossible
last [x] = x
last (x :: xs@(_::_)) = last xs

||| Return all but the last element of a non-empty list.
||| @ ok proof the list is non-empty
public export
init : (l : List a) -> {auto 0 ok : NonEmpty l} -> List a
init [] impossible
init [x] = []
init (x :: xs@(_::_)) = x :: init xs

||| Attempt to get the head of a list. If the list is empty, return `Nothing`.
public export
head' : List a -> Maybe a
head' []      = Nothing
head' (x::_) = Just x

||| Attempt to get the tail of a list. If the list is empty, return `Nothing`.
export
tail' : List a -> Maybe (List a)
tail' []      = Nothing
tail' (_::xs) = Just xs

||| Attempt to retrieve the last element of a non-empty list.
|||
||| If the list is empty, return `Nothing`.
export
last' : List a -> Maybe a
last' [] = Nothing
last' xs@(_::_) = Just (last xs)

||| Attempt to return all but the last element of a non-empty list.
|||
||| If the list is empty, return `Nothing`.
export
init' : List a -> Maybe (List a)
init' [] = Nothing
init' xs@(_::_) = Just (init xs)

public export
foldr1By : (func : a -> b -> b) -> (map : a -> b) ->
           (l : List a) -> {auto 0 ok : NonEmpty l} -> b
foldr1By f map [] impossible
foldr1By f map [x] = map x
foldr1By f map (x :: xs@(_::_)) = f x (foldr1By f map xs)

public export
foldl1By : (func : b -> a -> b) -> (map : a -> b) ->
           (l : List a) -> {auto 0 ok : NonEmpty l} -> b
foldl1By f map [] impossible
foldl1By f map (x::xs) = foldl f (map x) xs

||| Foldr a non-empty list without seeding the accumulator.
||| @ ok proof that the list is non-empty
public export
foldr1 : (a -> a -> a) -> (l : List a) -> {auto 0 ok : NonEmpty l} -> a
foldr1 f xs = foldr1By f id xs

||| Foldl a non-empty list without seeding the accumulator.
||| @ ok proof that the list is non-empty
public export
foldl1 : (a -> a -> a) -> (l : List a) -> {auto 0 ok : NonEmpty l} -> a
foldl1 f xs = foldl1By f id xs

||| Convert to a non-empty list.
||| @ ok proof the list is non-empty
export
toList1 : (l : List a) -> {auto 0 ok : NonEmpty l} -> List1 a
toList1 [] impossible
toList1 (x :: xs) = x ::: xs

||| Convert to a non-empty list, returning Nothing if the list is empty.
export
toList1' : (l : List a) -> Maybe (List1 a)
toList1' [] = Nothing
toList1' (x :: xs) = Just (x ::: xs)

||| Prefix every element in the list with the given element
|||
||| ```idris example
||| with List (mergeReplicate '>' ['a', 'b', 'c', 'd', 'e'])
||| ```
|||
export
mergeReplicate : a -> List a -> List a
mergeReplicate sep []      = []
mergeReplicate sep (y::ys) = sep :: y :: mergeReplicate sep ys

||| Insert some separator between the elements of a list.
|||
||| ````idris example
||| with List (intersperse ',' ['a', 'b', 'c', 'd', 'e'])
||| ````
|||
export
intersperse : a -> List a -> List a
intersperse sep []      = []
intersperse sep (x::xs) = x :: mergeReplicate sep xs

||| Given a separator list and some more lists, produce a new list by
||| placing the separator between each of the lists.
|||
||| @ sep the separator
||| @ xss the lists between which the separator will be placed
|||
||| ```idris example
||| intercalate [0, 0, 0] [ [1, 2, 3], [4, 5, 6], [7, 8, 9] ]
||| ```
export
intercalate : (sep : List a) -> (xss : List (List a)) -> List a
intercalate sep xss = concat $ intersperse sep xss

||| Apply a partial function to the elements of a list, keeping the ones at which
||| it is defined.
public export
mapMaybe : (a -> Maybe b) -> List a -> List b
mapMaybe f []      = []
mapMaybe f (x::xs) =
  case f x of
    Nothing => mapMaybe f xs
    Just j  => j :: mapMaybe f xs

||| Extract all of the values contained in a List of Maybes
public export
catMaybes : List (Maybe a) -> List a
catMaybes = mapMaybe id

--------------------------------------------------------------------------------
-- Sorting
--------------------------------------------------------------------------------

||| Check whether a list is sorted with respect to the default ordering for the type of its elements.
export
sorted : Ord a => List a -> Bool
sorted (x :: xs @ (y :: _)) = x <= y && sorted xs
sorted _ = True

||| Merge two sorted lists using an arbitrary comparison
||| predicate. Note that the lists must have been sorted using this
||| predicate already.
export
mergeBy : (a -> a -> Ordering) -> List a -> List a -> List a
mergeBy order []      right   = right
mergeBy order left    []      = left
mergeBy order (x::xs) (y::ys) =
  -- The code below will emit `y` before `x` whenever `x == y`.
  -- If you change this, `sortBy` will stop being stable, unless you fix `sortBy`, too.
  case order x y of
       LT => x :: mergeBy order xs (y::ys)
       _  => y :: mergeBy order (x::xs) ys

||| Merge two sorted lists using the default ordering for the type of their elements.
export
merge : Ord a => List a -> List a -> List a
merge left right = mergeBy compare left right

||| Sort a list using some arbitrary comparison predicate.
|||
||| @ cmp how to compare elements
||| @ xs the list to sort
export
sortBy : (cmp : a -> a -> Ordering) -> (xs : List a) -> List a
sortBy cmp []  = []
sortBy cmp [x] = [x]
sortBy cmp xs  = let (x, y) = split xs in
    mergeBy cmp
          (sortBy cmp (assert_smaller xs x))
          (sortBy cmp (assert_smaller xs y)) -- not structurally smaller, hence assert
  where
    splitRec : List b -> List a -> (List a -> List a) -> (List a, List a)
    splitRec (_::_::xs) (y::ys) zs = splitRec xs ys (zs . ((::) y))
    splitRec _          ys      zs = (ys, zs [])
    -- In the above base-case clause, we put `ys` on the LHS to get a stable sort.
    -- This is because `mergeBy` prefers taking elements from its RHS operand
    -- if both heads are equal, and all elements in `zs []` precede all elements of `ys`
    -- in the original list.

    split : List a -> (List a, List a)
    split xs = splitRec xs xs id

||| Sort a list using the default ordering for the type of its elements.
export
sort : Ord a => List a -> List a
sort = sortBy compare

export
isPrefixOfBy : (eq : a -> a -> Bool) -> (left, right : List a) -> Bool
isPrefixOfBy p [] _            = True
isPrefixOfBy p _ []            = False
isPrefixOfBy p (x::xs) (y::ys) = p x y && isPrefixOfBy p xs ys

||| The isPrefixOf function takes two lists and returns True iff the first list is a prefix of the second.
export
isPrefixOf : Eq a => List a -> List a -> Bool
isPrefixOf = isPrefixOfBy (==)

export
isSuffixOfBy : (a -> a -> Bool) -> List a -> List a -> Bool
isSuffixOfBy p left right = isPrefixOfBy p (reverse left) (reverse right)

||| The isSuffixOf function takes two lists and returns True iff the first list is a suffix of the second.
export
isSuffixOf : Eq a => List a -> List a -> Bool
isSuffixOf = isSuffixOfBy (==)

||| The isInfixOf function takes two lists and returns True iff the first list
||| is contained, wholly and intact, anywhere within the second.
|||
||| ```idris example
||| isInfixOf ['b','c'] ['a', 'b', 'c', 'd']
||| ```
||| ```idris example
||| isInfixOf ['b','d'] ['a', 'b', 'c', 'd']
||| ```
|||
export
isInfixOf : Eq a => List a -> List a -> Bool
isInfixOf n h = any (isPrefixOf n) (tails h)

||| Transposes rows and columns of a list of lists.
|||
||| ```idris example
||| with List transpose [[1, 2], [3, 4]]
||| ```
|||
||| This also works for non square scenarios, thus
||| involution does not always hold:
|||
|||     transpose [[], [1, 2]] = [[1], [2]]
|||     transpose (transpose [[], [1, 2]]) = [[1, 2]]
export
transpose : List (List a) -> List (List a)
transpose [] = []
transpose (heads :: tails) = spreadHeads heads (transpose tails) where
  spreadHeads : List a -> List (List a) -> List (List a)
  spreadHeads []              tails           = tails
  spreadHeads (head :: heads) []              = [head] :: spreadHeads heads []
  spreadHeads (head :: heads) (tail :: tails) = (head :: tail) :: spreadHeads heads tails

------------------------------------------------------------------------
-- Grouping

||| `groupBy` operates like `group`, but uses the provided equality
||| predicate instead of `==`.
public export
groupBy : (a -> a -> Bool) -> List a -> List (List1 a)
groupBy _ [] = []
groupBy eq (h :: t) = let (ys,zs) = go h t
                       in ys :: zs

  where go : a -> List a -> (List1 a, List (List1 a))
        go v [] = (singleton v,[])
        go v (x :: xs) = let (ys,zs) = go x xs
                          in if eq v x
                                then (cons v ys, zs)
                                else (singleton v, ys :: zs)

||| The `group` function takes a list of values and returns a list of
||| lists such that flattening the resulting list is equal to the
||| argument.  Moreover, each list in the resulting list
||| contains only equal elements.
public export
group : Eq a => List a -> List (List1 a)
group = groupBy (==)

||| `groupWith` operates like `group`, but uses the provided projection when
||| comparing for equality
public export
groupWith : Eq b => (a -> b) -> List a -> List (List1 a)
groupWith f = groupBy (\x,y => f x == f y)

||| `groupAllWith` operates like `groupWith`, but sorts the list
||| first so that each equivalence class has, at most, one list in the
||| output
public export
groupAllWith : Ord b => (a -> b) -> List a -> List (List1 a)
groupAllWith f = groupWith f . sortBy (comparing f)

--------------------------------------------------------------------------------
-- Properties
--------------------------------------------------------------------------------

export
Uninhabited ([] = x :: xs) where
  uninhabited Refl impossible

export
Uninhabited (x :: xs = []) where
  uninhabited Refl impossible

export
{0 xs : List a} -> Either (Uninhabited $ x === y) (Uninhabited $ xs === ys) => Uninhabited (x::xs = y::ys) where
  uninhabited @{Left  z} Refl = uninhabited @{z} Refl
  uninhabited @{Right z} Refl = uninhabited @{z} Refl

||| (::) is injective
export
consInjective : forall x, xs, y, ys .
                the (List a) (x :: xs) = the (List b) (y :: ys) -> (x = y, xs = ys)
consInjective Refl = (Refl, Refl)

reverseReverseOnto : (l, r : List a) -> reverse (reverseOnto l r) = reverseOnto r l
reverseReverseOnto _ [] = Refl
reverseReverseOnto l (x :: xs) = reverseReverseOnto (x :: l) xs

||| List reverse applied twice yields the identity function.
export
reverseInvolutive : (xs : List a) -> reverse (reverse xs) = xs
reverseInvolutive = reverseReverseOnto []

consReverse : (x : a) -> (l, r : List a) -> x :: reverseOnto r l = reverseOnto r (reverseOnto [x] (reverse l))
consReverse _ [] _ = Refl
consReverse x (y::ys) r
  = rewrite consReverse x ys (y :: r) in
      rewrite cong (reverseOnto r . reverse) $ consReverse x ys [y] in
        rewrite reverseInvolutive (y :: reverseOnto [x] (reverse ys)) in
          Refl

consTailRecAppend : (x : a) -> (l, r : List a) -> tailRecAppend (x :: l) r = x :: (tailRecAppend l r)
consTailRecAppend x l r
  = rewrite consReverse x (reverse l) r in
      rewrite reverseInvolutive l in
        Refl

||| Proof that `(++)` and `tailRecAppend` do the same thing, so the %transform
||| directive is safe.
tailRecAppendIsAppend : (xs, ys : List a) -> tailRecAppend xs ys = xs ++ ys
tailRecAppendIsAppend [] ys = Refl
tailRecAppendIsAppend (x::xs) ys =
  trans (consTailRecAppend x xs ys) (cong (x ::) $ tailRecAppendIsAppend xs ys)

||| The empty list is a right identity for append.
export
appendNilRightNeutral : (l : List a) -> l ++ [] = l
appendNilRightNeutral []      = Refl
appendNilRightNeutral (_::xs) = rewrite appendNilRightNeutral xs in Refl

||| Appending lists is associative.
export
appendAssociative : (l, c, r : List a) -> l ++ (c ++ r) = (l ++ c) ++ r
appendAssociative []      c r = Refl
appendAssociative (_::xs) c r = rewrite appendAssociative xs c r in Refl

revOnto : (xs, vs : List a) -> reverseOnto xs vs = reverse vs ++ xs
revOnto _ [] = Refl
revOnto xs (v :: vs)
    = rewrite revOnto (v :: xs) vs in
        rewrite appendAssociative (reverse vs) [v] xs in
                                  rewrite revOnto [v] vs in Refl

export
revAppend : (vs, ns : List a) -> reverse ns ++ reverse vs = reverse (vs ++ ns)
revAppend [] ns = rewrite appendNilRightNeutral (reverse ns) in Refl
revAppend (v :: vs) ns
    = rewrite revOnto [v] vs in
        rewrite revOnto [v] (vs ++ ns) in
          rewrite sym (revAppend vs ns) in
            rewrite appendAssociative (reverse ns) (reverse vs) [v] in
              Refl

export
dropFusion : (n, m : Nat) -> (l : List t) -> drop n (drop m l) = drop (n+m) l
dropFusion  Z     m    l      = Refl
dropFusion (S n)  Z    l      = rewrite plusZeroRightNeutral n in Refl
dropFusion (S n) (S m) []     = Refl
dropFusion (S n) (S m) (x::l) = rewrite plusAssociative n 1 m in
                                rewrite plusCommutative n 1 in
                                dropFusion (S n) m l

export
lengthMap : (xs : List a) -> length (map f xs) = length xs
lengthMap [] = Refl
lengthMap (x :: xs) = cong S (lengthMap xs)


text:
module Coproduct

import Basic
import Unit
import Void

%default total

infixl 5 +

namespace Coproduct
  public export
  data (+) : Type -> Type -> Type where
   Inl : a -> a + b
   Inr : b -> a + b

public export
SumInduction : (p : a + b -> Type)
            -> ((x : a) -> p (Inl x))
            -> ((y : b) -> p (Inr y))
            -> (z : a + b) -> p z
SumInduction p f g (Inl x) = f x
SumInduction p f g (Inr y) = g y

public export
SumRecursion : (p : Type)
            -> ((x : a) -> p)
            -> ((y : b) -> p)
            -> (z : a + b) -> p
SumRecursion p = SumInduction (const p)

public export
Two : Type
Two = Unit + Unit

public export
TwoInduction : (p : Two -> Type)
            -> p (Inl ())
            -> p (Inr ())
            -> (two : Two) -> p two
TwoInduction p pl pr = SumInduction p
  (UnitInduction (p `compose` Inl) pl) (UnitInduction (p `compose` Inr) pr)

ext: idr


text:
module Starfield

-- Background starfield effect

import Effect.SDL
import Effect.StdIO
import Effect.State

import Rnd

data Starfield : Type where -- for labelling state

StarEff : (Type -> Type) -> Type -> Type
StarEff m t = { [Starfield ::: STATE (List (Int, Int)), RND] } Eff m t

initStarfield : List (Int, Int) -> Nat -> StarEff m ()
initStarfield acc Z = Starfield :- put acc
initStarfield acc n
    = do x <- rndInt 0 639
         y <- rndInt 0 479
         initStarfield ((x, y) :: acc) (n - 1)

updateStarfield : StarEff m ()
updateStarfield = do xs <- Starfield :- get
                     xs' <- upd [] xs
                     Starfield :- put xs'
 where
  upd : List (Int, Int) -> List (Int, Int) -> { [RND] } Eff m (List (Int, Int))
  upd acc [] = return acc
  upd acc ((x, y) :: xs)
      = if (y > 479) then do
             x <- rndInt 0 639
             upd ((x, 0) :: acc) xs
           else
             upd ((x, y+1) :: acc) xs

drawStarfield : List (Int, Int) -> { [SDL_ON] } Eff IO ()
drawStarfield [] = return ()
drawStarfield ((x, y) :: xs) = do line white x y x y
                                  drawStarfield xs

max_stars_repo_name: silky/idris-demos

max_issues_repo_name: silky/idris-demos

max_forks_repo_name: silky/idris-demos


text:
||| Horizontal composition
module HoriComp

import Data.Vect
import VectHelp
import ProcessLib

import Proto

%default total
%access public export

resp: {m0,n0,m1,n1: Nat} ->
      {top0: Cut m0} -> {top1: Cut m1} -> {bot0: Cut n0} -> {bot1: Cut n1} ->
      ProcPID (MkNiche top0 bot0) ->
      ProcPID (MkNiche top1 bot1) ->
      (msg : Req (MkNiche (top0 ++ top1) (bot0 ++ bot1))) ->
      Process (ProcIF (MkNiche (top0 ++ top1) (bot0 ++ bot1)))
              (ProcIF (MkNiche (top0 ++ top1) (bot0 ++ bot1)) msg)
              Ready
              Ready
resp {top0 = top0} {top1 = top1} {bot0 = bot0} {bot1 = bot1} pid_a pid_b (Conn (TopOutWire loc) pid' target) =
  case elemConcat top0 top1 loc of
    Left l  => Request pid_a (Conn (TopOutWire l) pid' target)
    Right r => Request pid_b (Conn (TopOutWire r) pid' target)
resp {top0 = top0} {top1 = top1} {bot0 = bot0} {bot1 = bot1} pid_a pid_b (Conn (BotOutWire loc) pid' target) =
  case elemConcat bot0 bot1 loc of
    Left l  => Request pid_a (Conn (BotOutWire l) pid' target)
    Right r => Request pid_b (Conn (BotOutWire r) pid' target)
resp {top0 = top0} {top1 = top1} {bot0 = bot0} {bot1 = bot1} pid_a pid_b (Val (TopInWire loc) x) =
  case elemConcat top0 top1 loc of
    Left l  => Request pid_a (Val (TopInWire l) x)
    Right r => Request pid_b (Val (TopInWire r) x)
resp {top0 = top0} {top1 = top1} {bot0 = bot0} {bot1 = bot1} pid_a pid_b (Val (BotInWire loc) x) =
  case elemConcat bot0 bot1 loc of
    Left l  => Request pid_a (Val (BotInWire l) x)
    Right r => Request pid_b (Val (BotInWire r) x)

||| Monoidal operation on morphisms in the symetric monoidal category of processes
partial
(+): {m0,n0,m1,n1: Nat} ->
     {top0: Cut m0} -> {top1: Cut m1} -> {bot0: Cut n0} -> {bot1: Cut n1} ->
     Hom top0 bot0 -> Hom top1 bot1 -> Hom (top0 ++ top1) (bot0 ++ bot1)
(+) alpha beta = do Just pid_a <- Spawn alpha
                    Just pid_b <- Spawn beta
                    looper pid_a pid_b
  where
    looper: ProcPID (MkNiche top0 bot0) ->
            ProcPID (MkNiche top1 bot1) ->
            Process (ProcIF (MkNiche (top0 ++ top1) (bot0 ++ bot1))) () Ready Looping
    looper pid_a pid_b = do Respond (resp pid_a pid_b)
                            Loop (looper pid_a pid_b)

max_stars_repo_name: jameshaydon/smproc

max_issues_repo_name: jameshaydon/smproc

max_forks_repo_name: jameshaydon/smproc


text:
module Primitives

export
primDartFastUnpack : String
primDartFastUnpack = """
$.List Prelude_Types_fastUnpack($.String s) {
  return s.codeUnits.reversed.fold(
    const [0],
    (acc, charCode) => [1, charCode, acc],
  );
}
"""

export
primDartFastPack : String
primDartFastPack = """
$.String Prelude_Types_fastPack($.List list) {
  final buffer = $.StringBuffer();
  while (list[0] == 1) {
    buffer.writeCharCode(list[1]);
    list = list[2];
  }
  return buffer.toString();
}
"""

export
primDartFastConcat : String
primDartFastConcat = """
$.String Prelude_Types_fastConcat($.List list) {
  final buffer = $.StringBuffer();
  while (list[0] == 1) {
    buffer.write(list[1]);
    list = list[2];
  }
  return buffer.toString();
}
"""

export
primDartIterableFromList : String
primDartIterableFromList = """
$.Iterable<$.dynamic> Dart_Iterable_fromList($.List es) sync* {
  while (es[0] == 1) {
    yield es[1];
    es = es[2];
  }
}
"""

export
refTyDef : String
refTyDef = """
class Ref {
  $.dynamic v;
  Ref(this.v);
}
"""


text:
> module FastSimpleProb.Operations

> import FastSimpleProb.SimpleProb
> import FastSimpleProb.BasicOperations
> import FastSimpleProb.MonadicProperties
> import NonNegDouble.NonNegDouble
> import NonNegDouble.BasicOperations
> import Rel.TotalPreorder
> import NonNegDouble.LTEProperties
> import List.Operations
> import List.Properties
> import Fun.Operations
> import Double.Predicates

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

> |||
> mostProbableProb : {A : Type} -> (Eq A) => SimpleProb A -> (A, NonNegDouble)
> mostProbableProb {A} sp = argmaxMax totalPreorderLTE aps neaps where
>   aps   : List (A, NonNegDouble)
>   aps   = map (pair (id, (prob sp))) (nub (support sp))
>   nes   : List.Operations.NonEmpty (support sp)
>   nes   = mapPreservesNonEmpty fst (toList sp) (nonEmptyLemma1 sp)
>   nens  : List.Operations.NonEmpty (nub (support sp))
>   nens  = nubPreservesNonEmpty (support sp) nes
>   neaps : List.Operations.NonEmpty aps
>   neaps = mapPreservesNonEmpty (pair (id, (prob sp))) (nub (support sp)) nens

> |||
> mostProbable : {A : Type} -> (Eq A) => SimpleProb A -> A
> mostProbable = fst . mostProbableProb

> |||
> maxProbability : {A : Type} -> (Eq A) => SimpleProb A -> NonNegDouble
> maxProbability = snd . mostProbableProb

> |||
> sortToList : {A : Type} -> (Eq A) => SimpleProb A -> List (A, NonNegDouble)
> sortToList {A} sp = sortBy ord aps where
>   aps : List (A, NonNegDouble)
>   aps = map (pair (id, (prob sp))) (nub (support sp))
>   ord : (A, NonNegDouble) -> (A, NonNegDouble) -> Ordering
>   ord (a1, pa1) (a2, pa2) = compare (toDouble pa1) (toDouble pa2)

> |||
> naiveMostProbableProb : {A : Type} -> SimpleProb A -> (A, NonNegDouble)
> naiveMostProbableProb sp = argmaxMax totalPreorderLTE (toList sp) (nonEmptyLemma1 sp)

> |||
> naiveMostProbable : {A : Type} -> SimpleProb A -> A
> naiveMostProbable = fst . naiveMostProbableProb

> |||
> naiveMaxProbability : {A : Type} -> SimpleProb A -> NonNegDouble
> naiveMaxProbability = snd . naiveMostProbableProb

> |||
> naiveSortToList : {A : Type} -> SimpleProb A -> List (A, NonNegDouble)
> naiveSortToList {A} sp = sortBy ord (toList sp) where
>   ord : (A, NonNegDouble) -> (A, NonNegDouble) -> Ordering
>   ord (a1, pa1) (a2, pa2) = if (toDouble pa1) == (toDouble pa2)
>                             then EQ
>                             else if (toDouble pa1) < (toDouble pa2)
>                                  then GT
>                                  else LT

> {-

> ---}

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
module Data.Verified.Fufunctor

import Data.Fufunctor

%default total
%access public export

||| Verified Fufunctor
||| A Fufunctor for which identity and composition laws are verified
interface Fufunctor t => VerifiedFufunctor (t : Type -> Type -> Type -> Type) where
  fufunctorIdentity : {a : Type} -> {b : Type} -> {c : Type} ->
                      (x : t a b c) ->
                      fumap Basics.id Basics.id Basics.id x = x
  fufunctorComposition : {a : Type} -> {b : Type} -> {c : Type} ->
                         {a1 : Type} -> {b1 : Type} -> {c1 : Type} ->
                         (x : t a b c) ->
                         (fa1 : a1 -> a) -> (fb1 : b1 -> b) -> (fc1 : c -> c1) ->
                         (fa2 : a2 -> a1) -> (fb2 : b2 -> b1) -> (fc2 : c1 -> c2) ->
                         (fumap (fa1 . fa2) (fb1 . fb2) (fc2 . fc1) x) =
                         (fumap fa2 fb2 fc2 . fumap fa1 fb1 fc1) x

max_stars_repo_name: lemastero/Idris-Trifunctors

max_issues_repo_name: lemastero/Idris-Trifunctors

max_forks_repo_name: lemastero/Idris-Trifunctors


text:
module Toolkit.Text.Parser.Support

import Text.Lexer
import Text.Parser

%default total

public export
Rule : Type -> Type -> Type -> Type
Rule state tok ty = Grammar state tok True ty

public export
RuleEmpty : Type -> Type -> Type -> Type
RuleEmpty state tok ty = Grammar state tok False ty

export
eoi : (f : a -> Bool) -> RuleEmpty state a ()
eoi f
  = ignore $ nextIs "Not End of Input" (f)

-- [ EOF ]

max_stars_repo_name: gallais/linear-circuits

max_issues_repo_name: gallais/linear-circuits

max_forks_repo_name: gallais/linear-circuits


text:
-- Copyright (c) 2013 Radek Micek

module Main

import Common
import D3

main : IO ()
main = do
  btn <- d3 ?? select "body" >=>
           append "input" >=>
           attr "type" "button" >=>
           property "value" "Show prompt"

  log <- d3 ?? select "body" >=>
           append "ul"

  btn `onClick` \() => do
    res <- prompt "Enter some text"
    let msg = case res of
                Nothing => "Prompt cancelled"
                Just s => "Entered text: " ++ s
    log ?? append "li" >=> text msg
    return ()

max_stars_repo_name: radekm/satviz

max_issues_repo_name: radekm/satviz

max_forks_repo_name: radekm/satviz


text:
module SmallStepImp

import Expr
import Imp
import Maps
import SmallStepExpr

%access public export

%default total

data CStep : (Com, State) -> (Com, State) -> Type where
  CS_AssStep : AStep st a a' -> CStep (i ::= a, st) (i ::= a', st)
  CS_Ass : CStep (i ::= ANum n, st) (SKIP, t_update i n st)
  CS_SeqStep : CStep (c1, st) (c1', st') ->
               CStep ((do c1; c2), st) ((do c1'; c2), st')
  CS_SeqFinish : CStep ((do SKIP; c2), st) (c2, st)
  CS_IfStep : BStep st b b' -> CStep (CIf b c1 c2, st) (CIf b' c1 c2, st)
  CS_IfTrue : CStep (CIf BTrue c1 c2, st) (c1, st)
  CS_IfFalse : CStep (CIf BFalse c1 c2, st) (c2, st)
  CS_While : CStep (WHILE b c, st) (CIf b (do c; WHILE b c) SKIP, st)

syntax [t] "/" [st] "-+>" [t'] "/" [st'] = CStep (t, st) (t', st')


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

import GRL.Lang.GLang

paper : GOAL
paper = mkGoal "My First Paper"

abst : GOAL
abst = mkGoal "Abstract"

bib : GOAL
bib = mkGoal "Bibliography"

intr : GOAL
intr = mkGoal "Intro"

meth : GOAL
meth = mkGoal "Methodology"

res : GOAL
res = mkGoal "Results"

disc : GOAL
disc = mkGoal "Discussion"

wabs : TASK
wabs = mkSatTask "Write Abstract" (SATISFIED)

rabs : TASK
rabs = mkSatTask "Review Abstract" (WEAKSATIS)

wbib : TASK
wbib = mkSatTask "Write Bib" (WEAKSATIS)

rbib : TASK
rbib = mkSatTask "Review Bib" (WEAKSATIS)

wIntro : TASK
wIntro = mkSatTask "Write Intro" (DENIED)

rIntro : TASK
rIntro = mkSatTask "Review Intro" (DENIED)

wMeth : TASK
wMeth = mkSatTask "Write Meth" (DENIED)

rMeth : TASK
rMeth = mkSatTask "Review Meth" (DENIED)

wRes : TASK
wRes = mkSatTask "Write Results" (DENIED)

rRes : TASK
rRes = mkSatTask "Review Results" (DENIED)

wDis : TASK
wDis = mkSatTask "Write Discussion" (DENIED)

rDis : TASK
rDis = mkSatTask "Review Discussion" (DENIED)

paperPlan : GModel
paperPlan = emptyModel
 \= paper
 \= abst   \= wabs   \= rabs   \= bib    \= wbib   \= rbib
 \= intr   \= wIntro \= rIntro \= meth   \= wMeth  \= rMeth
 \= res    \= wRes   \= rRes   \= disc   \= wDis   \= rDis

 \= (paper &= [bib,abst,intr,meth,res,disc])

 \= (wabs   ==> abst  | MAKES)  \= (rabs   ==> abst  | MAKES)
 \= (wbib   ==> bib   | MAKES)  \= (rbib   ==> bib   | MAKES)
 \= (wIntro ==> intr  | MAKES)  \= (rIntro ==> intr  | MAKES)
 \= (wMeth  ==> meth  | MAKES)  \= (rMeth  ==> meth  | MAKES)
 \= (wRes   ==> res   | MAKES)  \= (rRes   ==> res   | MAKES)
 \= (wDis   ==> disc  | MAKES)  \= (rDis   ==> disc  | MAKES)

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

max_stars_repo_name: jfdm/idris-grl

max_issues_repo_name: jfdm/idris-grl

max_forks_repo_name: jfdm/idris-grl


text:
module Sub13LTE108t75

import ProofColDivSeqBase
import ProofColDivSeqPostulate

%default total

-- 6(18t+12)+3 --AB[6,-3,-2]--> 6(4t+1)+3
export
lte108t75 : (l : Nat) -> LTE (S (S (plus (plus l l) (plus l l)))) (S (S (S ((S ((S (l+l+l))+(S (l+l+l)))) + (S ((S (l+l+l))+(S (l+l+l)))) + (S ((S (l+l+l))+(S (l+l+l))))))))
lte108t75 Z     = (lteSuccRight . LTESucc . LTESucc) LTEZero
lte108t75 (S l) =
  let lemma = lte108t75 l in
  rewrite (sym (plusSuccRightSucc l l)) in
  rewrite (sym (plusSuccRightSucc (plus l l) l)) in

  rewrite (sym (plusSuccRightSucc (plus l l) (S (plus l l)))) in
  rewrite (sym (plusSuccRightSucc (plus l l)    (plus l l))) in

  rewrite (sym (plusSuccRightSucc (plus (plus l l) l) (S (S (S (plus (plus l l) l)))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus l l) l)    (S (S (plus (plus l l) l))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus l l) l)       (S (plus (plus l l) l)))) in

  rewrite (sym (plusSuccRightSucc (plus (plus (plus l l) l) (S (plus (plus l l) l))) (S (S (S (S (S (S (S (plus (plus (plus l l) l) (S (plus (plus l l) l)))))))))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus l l) l) (S (plus (plus l l) l)))    (S (S (S (S (S (S (plus (plus (plus l l) l) (S (plus (plus l l) l))))))))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus l l) l) (S (plus (plus l l) l)))       (S (S (S (S (S (plus (plus (plus l l) l) (S (plus (plus l l) l)))))))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus l l) l) (S (plus (plus l l) l)))          (S (S (S (S (plus (plus (plus l l) l) (S (plus (plus l l) l))))))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus l l) l) (S (plus (plus l l) l)))             (S (S (S (plus (plus (plus l l) l) (S (plus (plus l l) l)))))))) in
  rewrite (sym (plusSuccRightSucc (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))))))) in

  rewrite (sym (plusSuccRightSucc (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 (S (S (S (S (S (plus (plus (plus l l) l) (S (plus (plus l l) l)))))))))))) in
  rewrite (sym (plusSuccRightSucc (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 (S (S (S (S (plus (plus (plus l l) l) (S (plus (plus l l) l))))))))))) in
  rewrite (sym (plusSuccRightSucc (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 (S (S (S (plus (plus (plus l l) l) (S (plus (plus l l) l)))))))))) in
  rewrite (sym (plusSuccRightSucc (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 (S (S (plus (plus (plus l l) l) (S (plus (plus l l) l))))))))) in
  rewrite (sym (plusSuccRightSucc (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 (S (plus (plus (plus l l) l) (S (plus (plus l l) l)))))))) in
  rewrite (sym (plusSuccRightSucc (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))))))) in
    (lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . LTESucc . LTESucc . LTESucc . LTESucc) lemma


text:
module Main

%default total

data PowerSource = Petrol | Pedal

{-
4.2 Defining dependent data types
---------------------------------

A dependent data type is a *type* computed from a value.

E.g., : Vect : type of Vect depends on its length.

core idea : because there is no syntactic distinction between types and expressions,
            types can be computed from any expression.

Families of types
-----------------

Vehicle : defines two (i.e., "family") types in one declaration : Vehicle Pedal and Vehicle Petrol.
Defining multiple related types at the same time.
Power source is an index of the Vehicle family.
The index tells you exactly which Vehicle type you mean.
-}
data Vehicle : PowerSource -> Type where
  Bicycle :                 Vehicle Pedal
  Car     : (fuel : Nat) -> Vehicle Petrol
  Bus     : (fuel : Nat) -> Vehicle Petrol

wheels : Vehicle _ -> Nat
wheels Bicycle    = 2
wheels (Car fuel) = 4
wheels (Bus fuel) = 4

refuel : Vehicle Petrol -> Vehicle Petrol
refuel Bicycle impossible
refuel (Car fuel) = Car 100
refuel (Bus fuel) = Bus 200

max_stars_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_issues_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_forks_repo_name: haroldcarr/learn-haskell-coq-ml-etc


text:
module Control.Monad.State.Tuple

import public Control.Monad.State

%default total

export
Monad m => MonadState l (StateT (l, r) m) where
  get = Builtin.fst <$> get
  put = modify . mapFst . const

wrapFst : Functor m => StateT r m a -> StateT (l, r) m a
wrapFst act = ST $ \(x, y) => mapFst (x,) <$> runStateT y act

export
MonadState s (StateT r m) => Monad m => MonadState s (StateT (l, r) m) where
  get = wrapFst get
  put = wrapFst . put


text:
module Compiler.Erlang.Utils.String

import Utils.Hex

%default total

export
showSep : String -> List String -> String
showSep sep [] = ""
showSep sep [x] = x
showSep sep (x :: xs) = x ++ sep ++ showSep sep xs

-- TODO: Does not handle multi-codepoint characters
export
escapeChar : Char -> String -> String
escapeChar c acc =
  let codepoint = cast c
      space = 32
      tilde = 126
      backslash = 92
      doubleQuote = 34
      apostrophe = 39
  in if codepoint < space || codepoint > tilde ||
        codepoint == backslash || codepoint == doubleQuote || codepoint == apostrophe
    then "\\x{" ++ asHex (cast c) ++ "}" ++ acc
    else strCons c acc

export
escapeString : List Char -> String -> String
escapeString [] = id
escapeString (c :: cs) = escapeChar c . escapeString cs

||| Convert a Double to a String. Includes a decimal separator for all Double numbers.
|||
||| > showDouble 42
||| "42.0"
-- TODO: It may be possible to remove this if all codegens agree on making
-- `show {a=Double}` include a decimal separator.
export
showDouble : Double -> String
showDouble x =
  let dblStr = show x
  in if '.' `elem` unpack dblStr
    then dblStr
    else dblStr ++ ".0"


text:
module Incremental

mutual
  data Result : (i, r : Type) -> Type where
    Done : Monoid i => i -> r -> Result i r
    Partial : Monoid i => Inf (Parser i r) -> Result i r
    Failure : Monoid i => String -> Result i r

  data Parser : (i, r : Type) -> Type where
    MkParser : ((i -> Result i r)) -> Parser i r

runParser : Parser i r -> ((i -> Result i r))
runParser (MkParser f) = f

implementation Monoid i => Functor (Result i) where
  map f (Done i r) = Done i (f r)
  map f (Partial k) = assert_total (Partial (MkParser $ map f . runParser k))
  map _ f@(Failure s) = f

implementation Monoid i => Functor (Parser i) where
  map f (MkParser k) = MkParser $ (\x => map f $ k x)

implementation Monoid i => Applicative (Parser i) where
  pure x = MkParser (\i => Done i x)
  (MkParser f) <*> g = MkParser $ \i => case f i of
    Done i' f' => case runParser g i' of
      Done i'' r => Done i'' (f' r)
      Partial k => Partial (MkParser $ map f' . runParser k)
      Failure f => Failure f
    Partial k => Partial $ k <*> g
    Failure f => Failure f

infixl 2 <*>|
(<*>|) : Monoid i => Parser i (a -> b) -> Lazy (Parser i a) -> Parser i b
(<*>|) f g = f <*> g

implementation Monoid i => Monad (Parser i) where
  f >>= g = MkParser $ \i => case runParser f i of
    Done i' f' => runParser (g f') i'
    Partial k => Partial $ k >>= g
    f@(Failure s) => f

interface Applicative f => LazyAlternative (f : Type -> Type) where
  empty : f a
  (<|>) : f a -> Lazy (f a) -> f a

implementation Monoid i => LazyAlternative (Parser i) where
  empty = MkParser . const $ Failure "an alternative is empty"
  f <|> g = MkParser $ \i => case (runParser f i) of
    Failure _ => runParser g i
    Partial k => Partial $
      let cont = MkParser (\i' => runParser k i');
          next = MkParser (\i' => runParser g (i <+> i'))
      in cont <|> next
    done => done

fail : Monoid i => Parser i r
fail = MkParser . const $ Failure ""

item : Parser (List a) a
item = MkParser $ \i => case i of
  [] => Partial item
  (x::xs) => Done xs x

sat : (a -> Bool) -> Parser (List a) a
sat p = do
  i <- item
  if p i then pure i else fail

list : Eq a => List a -> Parser (List a) (List a)
list [] = pure []
list l@(x::xs) = do
  sat (== x)
  list xs
  return l

oneOf : Eq a => List a -> Parser (List a) a
oneOf l = sat (flip elem l)

option : Monoid i => Parser i b -> Parser i (Maybe b)
option p = (Just <$> p) <|> (pure Nothing)

manyTill : Parser (List a) b -> Parser (List a) c -> Parser (List a) (List b)
manyTill p t = option t >>= maybe ((::) <$> p <*>| manyTill p t) (const $ pure [])

many : Parser (List a) b -> Parser (List a) (List b)
many p = option p >>= maybe (pure []) (\x => (::) <$> pure x <*>| many p)

digit : Parser (List Char) Char
digit = oneOf ['0', '1', '2', '3', '4', '5', '6', '7', '8', '9']

int : Parser (List Char) Int
int = cast . pack <$> many digit

feed : Monoid i => Result i r -> i -> Result i r
feed (Partial k) i = runParser k i
feed (Done i r) i' = Done (i <+> i') r
feed (Failure s) _ = Failure s

-- feed (runParser (manyTill item (sat (== 'v'))) (the (List Char) ['a', 'b'])) ['c', 'v', 'w']
-- feed (runParser int $ unpack "12") $ unpack "34."
-- feed (runParser (list ['f', 'o', 'o'] <|> list ['f', 'o', 'r']) ['f', 'o']) ['o']
-- feed (runParser (list ['f', 'o', 'o'] <|> list ['f', 'o', 'r']) ['f', 'o']) ['r']
-- feed (feed (runParser (list ['f', 'o', 'o'] <|> list ['f', 'o', 'r']) ['f']) ['o']) ['o']
-- feed (feed (runParser (list ['f', 'o', 'o'] <|> list ['f', 'o', 'r']) ['f']) ['o']) ['r']

parseWith : Monad m => m i -> Parser i r -> m (Result i r)
parseWith r p = do
  v <- r
  case runParser p v of
    Partial k => parseWith r k
    other => pure other

-- main : IO ()
-- main = do
--   r <- parseWith (unpack <$> getLine) int
--   putStrLn $ case r of
--     Done i n => show n ++ " / " ++ pack i
--     Failure s => "Failure: " ++ s
--     _ => "Partial"

max_stars_repo_name: defanor/parcomb

max_issues_repo_name: defanor/parcomb

max_forks_repo_name: defanor/parcomb


text:
module Network.Curl.Easy.FFI

import System.File
import System.FFI
import Data.Buffer

%default total

private
curl : String -> String
curl func = "C:" ++ func ++ ",libcurl"

-- CURL *curl_easy_init( );
export
%foreign (curl "curl_easy_init")
prim__curl_easy_init : PrimIO AnyPtr

-- void curl_easy_cleanup(CURL *handle);
export
%foreign (curl "curl_easy_cleanup")
prim__curl_easy_cleanup : AnyPtr -> PrimIO ()

{-
 All options are set with an option followed by a parameter.
 That parameter can be a long, a function pointer, an object
 pointer or a curl_off_t, depending on what the specific option
 expects.
-}
-- CURLcode curl_easy_setopt(CURL *handle, CURLoption option, parameter);
export
%foreign (curl "curl_easy_setopt")
prim__curl_easy_setopt_long : AnyPtr -> Int -> Bits64 -> PrimIO Int

export
%foreign (curl "curl_easy_setopt")
prim__curl_easy_setopt_ptr : AnyPtr -> Int -> AnyPtr -> PrimIO Int

export
%foreign (curl "curl_easy_setopt")
prim__curl_easy_setopt_str : AnyPtr -> Int -> String -> PrimIO Int

export
%foreign (curl "curl_easy_setopt")
prim__curl_easy_setopt_buf : AnyPtr -> Int -> Buffer -> PrimIO Int

export
%foreign (curl "curl_easy_setopt")
prim__curl_easy_setopt_file : AnyPtr -> Int -> FilePtr -> PrimIO Int

-- CURLcode curl_easy_perform(CURL *easy_handle);
export
%foreign (curl "curl_easy_perform")
prim__curl_easy_perform : AnyPtr -> PrimIO Int

-- CURLcode curl_easy_getinfo(CURL *curl, CURLINFO info, ... );
export
%foreign (curl "curl_easy_getinfo")
prim__curl_easy_getinfo : AnyPtr -> Int -> AnyPtr -> PrimIO Int


text:
module NatOrder

import Decidable.Order

%default total

-- data NatOrder : Nat -> Nat -> Type = LessThan (LT x y) | Equal (x = y) | GreaterThan (GT x y)
public export
data NatOrder : Nat -> Nat -> Type where
    LessThan : LT x y -> NatOrder x y
    Equal : x = y -> NatOrder x y
    GreaterThan : GT x y -> NatOrder x y

-- export
notGT : Not (LTE x y) -> GT x y
notGT {x = Z} {y = y} contra = void $ contra LTEZero
notGT {x = (S k)} {y = Z} contra = LTESucc LTEZero
notGT {x = (S kx)} {y = (S ky)} contra =
    let ih = notGT {x=kx} {y=ky} (contra . LTESucc) in
    LTESucc ih

-- export
notEqLt : LTE x y -> Not (x = y) -> LT x y
notEqLt {x = Z} {y = Z} x_lte_y x_neq_y = void $ x_neq_y Refl
notEqLt {x = Z} {y = (S k)} x_lte_y x_neq_y = LTESucc LTEZero
notEqLt {x = (S k)} {y = Z} x_lte_y x_neq_y = absurd x_lte_y
notEqLt {x = (S kx)} {y = (S ky)} x_lte_y x_neq_y =
    let ih = notEqLt {x=kx} {y=ky} (fromLteSucc x_lte_y) (x_neq_y . cong {f=S}) in
    LTESucc ih

export
decideOrder : (x : Nat) -> (y : Nat) -> NatOrder x y
decideOrder x y = case decEq x y of
    (Yes prf) => Equal prf
    (No x_neq_y) => case decideLTE x y of
        (Yes x_lte_y) => LessThan (notEqLt x_lte_y x_neq_y)
        (No x_gt_y) => GreaterThan (notGT x_gt_y)

export
eqDecEq : {x : Nat} -> (prf ** decEq x x = Yes prf)
eqDecEq {x = Z} = (Refl ** Refl)
eqDecEq {x = (S k)} =
    let (prf_k ** eq_prf_k) = eqDecEq {x=k} in
    rewrite eq_prf_k in
    (cong prf_k ** Refl)

export
equalDecision : (prf ** decideOrder x x = Equal prf)
equalDecision {x = Z} = (Refl ** Refl)
equalDecision {x = (S k)} =
    let (k_k ** eq_prf_k) = equalDecision {x=k} in
    -- rewrite eq_prf_k in
    ?opuqwer
    -- (cong k_k ** ?opupqwer)

-- equalDecision {x} =
--     case decideOrder x x of
--         (LessThan x) => ?poipqowuier_1
--         (Equal prf) =>
--             let (x_x ** eq_prf_x) = eqDecEq {x=x} in
--             (x_x **
--                 -- rewrite eq_prf_x in
--                 ?pouiqpwerqwer
--             )
--         (GreaterThan x) => ?poipqowuier_3


text:
module Test.Bits8

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

allBits8 : Gen Bits8
allBits8 = bits8 (linear 0 0xffff)

gt0 : Gen Bits8
gt0 = bits8 (linear 1 MaxBits8)

gt1 : Gen Bits8
gt1 = bits8 (linear 2 MaxBits8)

prop_ltMax : Property
prop_ltMax = property $ do
  b8 <- forAll allBits8
  (b8 <= MaxBits8) === True

prop_ltMin : Property
prop_ltMin = property $ do
  b8 <- forAll allBits8
  (b8 >= MinBits8) === True

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

prop_mod : Property
prop_mod = property $ do
  [n,d] <- forAll $ np [allBits8, gt0]
  compare (n `mod` d) d === LT

prop_div : Property
prop_div = property $ do
  [n,d] <- forAll $ np [gt0, gt1]
  compare (n `div` d) n === LT

prop_divMod : Property
prop_divMod = property $ do
  [n,d] <- forAll $ np [allBits8, gt0]
  let x = n `div` d
      r = n `mod` d
  n === x * d + r

export
props : Group
props = MkGroup "Bits8" $
  [ ("prop_ltMax",  prop_ltMax)
  , ("prop_ltMin",  prop_ltMin)
  , ("prop_comp",   prop_comp)
  , ("prop_mod",    prop_mod)
  , ("prop_div",    prop_div)
  , ("prop_divMod", prop_divMod)
  ] ++ ringProps allBits8


text:
module RUS

import Data.Vect
import QStateT
import QuantumOp
import LinearTypes
import Unitary
import Data.List

||| Problem: Given an input qubit |q> and a single-qubit unitary operation U,
|||          return the state U|q>. The "Repeat Until Success" approach solves
|||          this problem in the following way:
|||
||| 1. Prepare a new qubit in state |0>
||| 2. Apply some two-qubit unitary operation U' (depends on U)
||| 3. Measure the auxiliary qubit
||| 4. With (high) probability the result is now U|q> and then stop.
||| 5. With (low) probability the result is state E|q>, where E is some other unitary operator
|||    (depending on U), so we uncompute the error by applying E^dagger and we go back to step 1.

export
RUS : QuantumOp t => (1 _ : Qubit) -> (u' : Unitary 2) -> (e : Unitary 1) -> QStateT (t 1) (t 1) Qubit
RUS q u' e = do
  q' <- newQubit
  [q',q] <- applyUnitary [q',q] u'
  b <- measureQubit q'
  if b then do
         [q] <- applyUnitary [q] (adjoint e)
         RUS q u' e
       else pure q

||| Figure 8 of https://arxiv.org/abs/1311.1074
example_u' : Unitary 2
example_u' = H 0 $ T 0 $ CNOT 0 1 $ H 0 $ CNOT 0 1 $ T 0 $ H 0 IdGate

export
runRUS : QuantumOp t => IO Bool
runRUS = do
  [b] <- run (do
              q <- newQubit {t = t}
              q <- RUS q example_u' IdGate
              measure [q]
         )
  pure b

export
testRUS : IO Bool
testRUS = runRUS {t = SimulatedOp}

export
testMultipleRUS : Nat -> IO ()
testMultipleRUS n = do
  let f = testRUS
  s <- sequence (Data.List.replicate n f)
  let heads = filter (== True) s
  putStrLn $ "Number of '1' outcomes: " ++ (show (length heads)) ++ " out of " ++ (show n) ++ " measurements."

max_stars_repo_name: zamdzhiev/Qimaera

max_issues_repo_name: zamdzhiev/Qimaera

max_forks_repo_name: zamdzhiev/Qimaera


text:
module PatternMatching

zahlen : List Nat
zahlen = [1,2,3,4,5]

person : (String, Nat)
person = ("Max", 40)

data Farbe
  = Rot
  | Blau

data Expression : Type -> Type where
  Falsch : Expression Bool
  Wahr : Expression Bool
  Zahl : Nat -> Expression Nat
  Plus : Expression Nat -> Expression Nat -> Expression Nat
  Gleich : Expression Nat -> Expression Nat -> Expression Bool
  Falls : Expression Bool -> Expression a -> Expression a -> Expression a

istLeer : List a -> Bool
istLeer [] = True
istLeer (x :: xs) = False

name : (String, Nat) -> String
name (n, _) = n

eval : Expression a -> a
eval Falsch = False
eval Wahr = True
eval (Zahl k) = k
eval (Plus x y) = eval x + eval y
eval (Gleich x y) = eval x == eval y
eval (Falls b t e) = if (eval b) then eval t else eval e


text:
module Data.Hashable

import Data.String

||| A default salt used in the implementation of 'hash'.
export
defaultSalt : Bits64
defaultSalt = 14695981039346656037

infixl 10 `hashWithSalt`
infixl 10 `hash`

||| Interface for type that can be hashed.
-- Minimal implementation: 'hashWithSalt'
public export
interface Hashable a where
    hashWithSalt : Bits64 -> a -> Bits64
    hash : a -> Bits64
    hash = hashWithSalt defaultSalt

||| Combine 2 hashes.
export
combine : Bits64 -> Bits64 -> Bits64
combine h1 h2 = (h1 * 16777619) `prim__xor_Bits64` h2

||| Default implementation of 'hashWithSalt' for types which are smaller than Bits64 (eg Bits32, Int).
export
defaultHashWithSalt : Hashable a => Bits64 -> a -> Bits64
defaultHashWithSalt salt x = salt `combine` hash x

export
Hashable Bits8 where
    hash = cast
    hashWithSalt = defaultHashWithSalt

export
Hashable Bits16 where
    hash = cast
    hashWithSalt = defaultHashWithSalt

export
Hashable Bits32 where
    hash = cast
    hashWithSalt = defaultHashWithSalt

export
Hashable Bits64 where
    hash = id
    hashWithSalt = defaultHashWithSalt

export
Hashable Int where
    hash = cast
    hashWithSalt = defaultHashWithSalt

export
Hashable Char where
    hash = cast . ord
    hashWithSalt = defaultHashWithSalt

export
Hashable String where
    hashWithSalt salt str = finalise (foldl step (salt, 0) $ fastUnpack str)
      where
        step : (Bits64, Bits64) -> Char -> (Bits64, Bits64)
        step (s, l) x = (hashWithSalt s x, l + 1)
        finalise : (Bits64, Bits64) -> Bits64
        finalise (s, l) = hashWithSalt s l


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

-- Checking that we can access 'n' from the index even though it's
-- not explicitly brought into scope, and the match requires n to be
-- Z or S k...
vlen : {n : Nat} -> Vect n a -> Nat
vlen [] = n
vlen (x :: xs) = n


text:
-- -------------------------------------------------------------- [ Lens.idr ]
-- Description : Idris port of Control.Lens
-- Copyright   : (c) Huw Campbell
-- --------------------------------------------------------------------- [ EOH ]
module Data.Yoneda

import Data.Morphisms

-- | @Yoneda f a@ can be viewed as the partial application of 'fmap' to its second argument.
public export
data Yoneda : ( f : Type -> Type ) -> ( a : Type ) -> Type where
  MkYoneda : ({0 b : Type} -> (a -> b) -> f b) -> Yoneda f a

-- | The natural isomorphism between @f@ and @'Yoneda' f@ given by the Yoneda lemma
-- is witnessed by 'liftYoneda' and 'lowerYoneda'
--
-- @
-- 'liftYoneda' . 'lowerYoneda' ≡ 'id'
-- 'lowerYoneda' . 'liftYoneda' ≡ 'id'
-- @
--
-- @
-- lowerYoneda (liftYoneda fa) =         -- definition
-- lowerYoneda (Yoneda (\f -> fmap f a)) -- definition
-- (\f -> fmap f fa) id                  -- beta reduction
-- fmap id fa                            -- functor law
-- fa
-- @
--
-- @
-- 'lift' = 'liftYoneda'
-- @
public export
liftYoneda : { f : Type -> Type } -> Functor f => f a -> Yoneda f a
liftYoneda a = MkYoneda (flip map a)

public export
lowerYoneda : {0 a : Type} -> Yoneda f a -> f a
lowerYoneda (MkYoneda f) = f id

public export
implementation Functor f => Functor (Yoneda f) where
  map h (MkYoneda k) = MkYoneda (flip map (k h))

public export
implementation Applicative f => Applicative (Yoneda f) where
  pure a = MkYoneda (\f => pure (f a))
  (MkYoneda m) <*> (MkYoneda n) = MkYoneda (\f => m (f .) <*> n id)


text:
module Data.ByteArray

%include C "array.h"
%link C "array.o"

%access public export
%default total

namespace Byte
  Byte : Type
  Byte = Bits8

  toInt : Byte -> Int
  toInt = prim__zextB8_Int

  fromInt : Int -> Byte
  fromInt = prim__truncInt_B8

export
record ByteArray where
  constructor BA
  ptr : CData
  sz : Int

-- This needn't be precise; it just needs to be enough to be safe.
export
bytesPerInt : Int
bytesPerInt = 8

export
allocate : Int -> IO ByteArray
allocate sz = do
  ptr <- foreign FFI_C "array_alloc" (Int -> IO CData) sz
  pure $ BA ptr sz

export
reallocate : Int -> ByteArray -> IO ()
reallocate newSz (BA ptr sz)
  = foreign FFI_C "array_realloc" (Int -> CData -> IO ()) sz ptr

export
peek : Int -> ByteArray -> IO Byte
peek ofs (BA ptr sz)
  = if (ofs < 0 || ofs >= sz)
      then pure 0
      else foreign FFI_C "array_peek" (Int -> CData -> IO Byte) ofs ptr

export
peekInt : Int -> ByteArray -> IO Int
peekInt ofs (BA ptr sz)
  = if (ofs < 0 || ofs+bytesPerInt > sz)
      then pure 0
      else foreign FFI_C "array_peek_int" (Int -> CData -> IO Int) ofs ptr

export
poke : Int -> Byte -> ByteArray -> IO ()
poke ofs b (BA ptr sz)
  = if (ofs < 0 || ofs >= sz)
      then pure ()
      else foreign FFI_C "array_poke" (Int -> Byte -> CData -> IO ()) ofs b ptr

export
pokeInt : Int -> Int -> ByteArray -> IO ()
pokeInt ofs i (BA ptr sz)
  = if (ofs < 0 || ofs+bytesPerInt > sz)
      then pure ()
      else foreign FFI_C "array_poke_int" (Int -> Int -> CData -> IO ()) ofs i ptr

export
copy : (ByteArray, Int) -> (ByteArray, Int) -> Int -> IO ()
copy (BA srcPtr srcSz, srcIx) (BA dstPtr dstSz, dstIx) count
  = if (srcIx < 0 || dstIx < 0 || (srcIx+count) > srcSz || (dstIx+count) > dstSz)
      then pure ()
      else foreign FFI_C "array_copy" (CData -> Int -> CData -> Int -> Int -> IO ()) srcPtr srcIx dstPtr dstIx count

export
fill : Int -> Int -> Byte -> ByteArray -> IO ()
fill ofs count b (BA ptr sz)
  = if (ofs < 0 || ofs+count > sz)
      then pure ()
      else foreign FFI_C "array_fill" (Int -> Int -> Byte -> CData -> IO ()) ofs count b ptr

export
size : ByteArray -> Int
size (BA ptr sz) = sz

export
compare : (ByteArray, Int) -> (ByteArray, Int) -> Int -> IO Int
compare (BA ptrL szL, ofsL) (BA ptrR szR, ofsR) count
  = if (ofsL < 0 || ofsL+count > szL || ofsR < 0 || ofsR+count > szR)
      then pure 0
      else foreign FFI_C "array_compare" (CData -> Int -> CData -> Int -> Int -> IO Int) ptrL ofsL ptrR ofsR count

export
find : Byte -> ByteArray -> Int -> Int -> IO (Maybe Int)
find b (BA ptr sz) ofs end = do
  ofs <- foreign FFI_C "array_find" (Byte -> CData -> Int -> Int -> IO Int) b ptr ofs end
  if ofs < 0
    then pure $ Nothing
    else pure $ Just ofs

max_stars_repo_name: grin-compiler/idris-grin

max_issues_repo_name: grin-compiler/idris-grin

max_forks_repo_name: grin-compiler/idris-grin


text:
module Temp

import Data.List

safeHead : (l : List a) -> {auto pr : NonEmpty l} -> a
safeHead [] = absurd pr
safeHead (x::xs) = x

safeHead1 : (l : List a) -> {auto pr : NonEmpty l} -> a
safeHead1 @{pr} [] = absurd pr
safeHead1 (x::xs) = x

safeHead2 : (l : List a) -> {auto pr : NonEmpty l} -> a
safeHead2 @{t} [] = absurd t
safeHead2 (x::xs) = x


text:
palindrome : Nat -> String -> Bool
palindrome n str = let longEnough = (length str) > n
                   in longEnough && (isPalindrome str)
    where
      isPalindrome : String -> Bool
      isPalindrome s = (toLower s) == (toLower (reverse s))

showPalindrome : String -> String
showPalindrome str = "Word is palindrome: " ++ show (palindrome 0 str) ++ "\n"

main : IO ()
main = repl "> " showPalindrome


text:
||| Types and functions for reasoning about time.
module System.Clock

import Data.Nat
import Data.String
import PrimIO

%default total

||| The various types of system clock available.
public export
data ClockType
  = ||| The time elapsed since the "epoch:" 00:00:00 UTC, January 1, 1970
    UTC
  | ||| The time elapsed since some arbitrary point in the past
    Monotonic
  | ||| Representing a time duration.
    Duration
  | ||| The amount of CPU time used by the current process.
    Process
  | ||| The amount of CPU time used by the current thread.
    Thread
  | ||| The current process's CPU time consumed by the garbage collector.
    GCCPU
  | ||| The current process's real time consumed by the garbage collector.
    GCReal

export
Show ClockType where
  show UTC       = "UTC"
  show Monotonic = "monotonic"
  show Duration  = "duration"
  show Process   = "process"
  show Thread    = "thread"
  show GCCPU     = "gcCPU"
  show GCReal    = "gcReal"

||| A clock recording some time in seconds and nanoseconds. The "type" of time
||| recorded is indicated by the given `ClockType`.
public export
data Clock : (type : ClockType) -> Type where
  MkClock
    : {type : ClockType}
    -> (seconds : Integer)
    -> (nanoseconds : Integer)
    -> Clock type

public export
Eq (Clock type) where
  (MkClock seconds1 nanoseconds1) == (MkClock seconds2 nanoseconds2) =
    seconds1 == seconds2 && nanoseconds1 == nanoseconds2

public export
Ord (Clock type) where
  compare (MkClock seconds1 nanoseconds1) (MkClock seconds2 nanoseconds2) =
  case compare seconds1 seconds2 of
    LT => LT
    GT => GT
    EQ => compare nanoseconds1 nanoseconds2

public export
Show (Clock type) where
  show (MkClock {type} seconds nanoseconds) =
    show type ++ ": " ++ show seconds ++ "s " ++ show nanoseconds ++ "ns"

||| Display a `Clock`'s content, padding the seconds and nanoseconds as
||| appropriate.
|||
||| @ s   the number of digits used to display the seconds
||| @ ns  the number of digits used to display the nanosecondns
||| @ clk the Clock whose contents to display
export
showTime : (s, ns : Nat) -> (clk : Clock type) -> String
showTime s ns (MkClock seconds nanoseconds) =
  let seconds = show seconds
      quotient : Integer = cast $ 10 `power` minus 9 ns
      nanoseconds = show (cast nanoseconds `div` quotient)
  in concat [ padLeft s '0' seconds
            , "."
            , padRight ns '0' nanoseconds
            , "s"
            ]

||| A helper to deconstruct a Clock.
public export
seconds : Clock type -> Integer
seconds (MkClock s _) = s

||| A helper to deconstruct a Clock.
public export
nanoseconds : Clock type -> Integer
nanoseconds (MkClock _ ns) = ns

||| Make a duration value.
|||
||| @ s  the number of seconds in the duration
||| @ ns the number of nanoseconds in the duration
public export
makeDuration : (s : Integer) -> (ns : Integer) -> Clock Duration
makeDuration = MkClock

||| Opaque clock value manipulated by the back-end.
data OSClock : Type where [external]

||| Note: Backends are required to implement UTC, monotonic time, CPU time in
||| current process/thread, and time duration; the rest are optional.
export
data ClockTypeMandatory
  = Mandatory
  | Optional

||| Determine whether the specified `ClockType` is required to be implemented by
||| all backends.
public export
isClockMandatory : ClockType -> ClockTypeMandatory
isClockMandatory GCCPU  = Optional
isClockMandatory GCReal = Optional
isClockMandatory _      = Mandatory

%foreign "scheme:blodwen-clock-time-monotonic"
         "RefC:clockTimeMonotonic"
prim__clockTimeMonotonic : PrimIO OSClock

||| Get the current backend's monotonic time.
clockTimeMonotonic : IO OSClock
clockTimeMonotonic = fromPrim prim__clockTimeMonotonic

%foreign "scheme:blodwen-clock-time-utc"
         "RefC:clockTimeUtc"
prim__clockTimeUtc : PrimIO OSClock

||| Get the current UTC time.
clockTimeUtc : IO OSClock
clockTimeUtc = fromPrim prim__clockTimeUtc

%foreign "scheme:blodwen-clock-time-process"
         "RefC:clockTimeProcess"
prim__clockTimeProcess : PrimIO OSClock

||| Get the amount of time used by the current process.
clockTimeProcess : IO OSClock
clockTimeProcess = fromPrim prim__clockTimeProcess

%foreign "scheme:blodwen-clock-time-thread"
         "RefC:clockTimeThread"
prim__clockTimeThread : PrimIO OSClock

||| Get the amount of time used by the current thread.
clockTimeThread : IO OSClock
clockTimeThread = fromPrim prim__clockTimeThread

%foreign "scheme:blodwen-clock-time-gccpu"
         "RefC:clockTimeGcCpu"
prim__clockTimeGcCpu : PrimIO OSClock

||| Get the amount of the current process's CPU time consumed by the garbage
||| collector.
clockTimeGcCpu : IO OSClock
clockTimeGcCpu = fromPrim prim__clockTimeGcCpu

%foreign "scheme:blodwen-clock-time-gcreal"
         "RefC:clockTimeGcReal"
prim__clockTimeGcReal : PrimIO OSClock

||| Get the amount of the current process's real-time consumed by the garbage
||| collector.
clockTimeGcReal : IO OSClock
clockTimeGcReal = fromPrim prim__clockTimeGcReal

fetchOSClock : ClockType -> IO OSClock
fetchOSClock UTC       = clockTimeUtc
fetchOSClock Monotonic = clockTimeMonotonic
fetchOSClock Process   = clockTimeProcess
fetchOSClock Thread    = clockTimeThread
fetchOSClock GCCPU     = clockTimeGcCpu
fetchOSClock GCReal    = clockTimeGcReal
fetchOSClock Duration  = clockTimeMonotonic

%foreign "scheme:blodwen-is-time?"
         "RefC:clockValid"
prim__osClockValid : OSClock -> PrimIO Int

||| A test to determine the status of optional clocks.
osClockValid : OSClock -> IO Int
osClockValid clk = fromPrim (prim__osClockValid clk)

%foreign "scheme:blodwen-clock-second"
         "RefC:clockSecond"
prim__osClockSecond : OSClock -> PrimIO Bits64

||| Get the second of time from the given `OSClock`.
osClockSecond : OSClock -> IO Bits64
osClockSecond clk = fromPrim (prim__osClockSecond clk)

%foreign "scheme:blodwen-clock-nanosecond"
         "RefC:clockNanosecond"
prim__osClockNanosecond : OSClock -> PrimIO Bits64

||| Get the nanosecond of time from the given `OSClock`.
osClockNanosecond : OSClock -> IO Bits64
osClockNanosecond clk = fromPrim (prim__osClockNanosecond clk)

||| Convert an `OSClock` to an Idris `Clock`.
fromOSClock : {type : ClockType} -> OSClock -> IO (Clock type)
fromOSClock clk =
  pure $
    MkClock
      {type}
      (cast !(osClockSecond clk))
      (cast !(osClockNanosecond clk))

||| The return type of a function using a `Clock` depends on the type of
||| `Clock`:
||| * `Optional` clocks may not be implemented, so we might not return anything
||| * `Mandatory` clocks have to be implemented, so we _will_ return something
public export
clockTimeReturnType : (typ : ClockType) -> Type
clockTimeReturnType typ with (isClockMandatory typ)
  clockTimeReturnType typ | Optional = Maybe (Clock typ)
  clockTimeReturnType typ | Mandatory = Clock typ

||| Fetch the system clock of a given kind. If the clock is mandatory,
||| we return a `Clock type` else, we return a `Maybe (Clock type)`.
public export
clockTime : (typ : ClockType) -> IO (clockTimeReturnType typ)
clockTime clockType with (isClockMandatory clockType)
  clockTime clockType | Mandatory = fetchOSClock clockType >>= fromOSClock
  clockTime clockType | Optional = do
    clk <- fetchOSClock clockType
    valid <- map (== 1) $ osClockValid clk
    if valid
      then map Just $ fromOSClock clk
      else pure Nothing

||| Convert the time in the given clock to nanoseconds.
toNano : Clock type -> Integer
toNano (MkClock seconds nanoseconds) =
  let scale = 1000000000
   in scale * seconds + nanoseconds

||| Convert some time in nanoseconds to a `Clock` containing that time.
|||
||| @ n the time in nanoseconds
fromNano : {type : ClockType} -> (n : Integer) -> Clock type
fromNano n =
  let scale       = 1000000000
      seconds     = n `div` scale
      nanoseconds = n `mod` scale
   in MkClock seconds nanoseconds

||| Compute difference between two clocks of the same type.
public export
timeDifference : Clock type -> Clock type -> Clock Duration
timeDifference clock duration = fromNano $ toNano clock - toNano duration

||| Add a duration to a clock value.
public export
addDuration : {type : ClockType} -> Clock type -> Clock Duration -> Clock type
addDuration clock duration = fromNano $ toNano clock + toNano duration

||| Subtract a duration from a clock value.
public export
subtractDuration : {type : ClockType} -> Clock type -> Clock Duration -> Clock type
subtractDuration clock duration = fromNano $ toNano clock - toNano duration


text:
module Main

export
Show Really where
  show (Really err) =  ["RR"

main : IO ()
main = putStrLn "LOG"


text:
import Data.Vect

{- 1 -}

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

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

{- 2 -}

addMatrix : Num a => Vect n (Vect m a) -> Vect n (Vect m a) -> Vect n (Vect m a)
addMatrix [] [] = []
addMatrix (x :: xs) (y :: ys) = zipWith (+) x y :: addMatrix xs ys

{- 3 -}

multVecs : Num a => (xs : Vect n a) -> (ys : Vect n a) -> a
multVecs xs ys = sum (zipWith (*) xs ys)

mkRow : Num a => (x : Vect n a) -> (ys_trans : Vect p (Vect n a)) -> Vect p a
mkRow x [] = []
mkRow x (y :: xs) = multVecs x y :: mkRow x xs

multMatrix_helper : Num a => (xs : Vect m (Vect n a)) -> (ys_trans : Vect p (Vect n a)) -> Vect m (Vect p a)
multMatrix_helper [] ys_trans = []
multMatrix_helper (x :: xs) ys_trans
     = mkRow x ys_trans :: multMatrix_helper xs ys_trans

multMatrix : Num a => Vect m (Vect n a) -> Vect n (Vect p a) -> Vect m (Vect p a)
multMatrix xs ys = let ys_trans = transpose_mat ys in
                       multMatrix_helper xs ys_trans

max_stars_repo_name: PiotrJander/TypeDD-Samples

max_issues_repo_name: gdevanla/TypeDD-Samples

max_forks_repo_name: gdevanla/TypeDD-Samples


text:
module Hoare2

import Assn
import Expr
import Hoare
import Imp
import Logic
import Maps

%access public export

%default total

reduce_to_zero : Com
reduce_to_zero = WHILE (not (X == 0)) $
                   X ::= X - 1

reduce_to_zero_correct : HoareTriple (const ())
                                     Hoare2.reduce_to_zero
                                     (\st => st X = 0)
reduce_to_zero_correct =
  let htc = hoare_consequence_pre
              (\st => ((), BAssn (not (X == 0)) st))
              (AssignSub X (X - 1) (const ()))
              (const ())
              (hoare_assign (const ()))
              (\_, _ => ())
      htw = hoare_while (const ()) htc
  in hoare_consequence_post
       (const ())
       (\st => st X = 0)
       (\st => ((), Not (BAssn (not (X == 0)) st)))
       htw
       (\st, (_, contra) =>
           fst (nat_beq_iff (st X) 0)
               (trans (sym (notInvolutive (st X == 0)))
                      (cong {f=not} (fst not_true_iff_false contra))))

slow_assignment : Com
slow_assignment = do
  {-
    {{ X = m }}
    ->> {{ (X = m, Y = n) }}
  -}
  Y ::= 0
  {-
    {{ (X = m, Y = 0) }}
    ->> {{ X + Y = m }}
  -}
  WHILE (not (X == 0)) $ do
    {-
      {{ (X + Y = m, not (X == 0)) }}
      ->> {{ X - 1 + Y + 1 = m }}
    -}
    X ::= X - 1
    -- {{ X + Y + 1 = m }}
    Y ::= Y + 1
    -- {{ X + Y = m }}
  {-
    {{ (X + Y = m, Not (not (X == 0))) }}
    ->> {{ Y = m }}
  -}

slow_assignment_correct : HoareTriple (\st => st X = m)
                                      Hoare2.slow_assignment
                                      (\st => st Y = m)
slow_assignment_correct {m} =
  let hty = hoare_consequence_pre
              (\st => st X = m)
              (AssignSub Y 0 (\st => (st X = m, st Y = 0)))
              (\st => (st X = m, st Y = 0))
              (hoare_assign (\st => (st X = m, st Y = 0)))
              (\st, p_st => (p_st, Refl))
      htx = hoare_consequence_pre
              (\st => (st X + st Y = m, BAssn (not (X == 0)) st))
              (\st => minus (st X) 1 + (st Y + 1) = m)
              (\st => st X + (st Y + 1) = m)
              (hoare_assign (\st => st X + (st Y + 1) = m))
              (\st, (prf, x_prf) =>
                  let lte_prf =
                        notZeroImpliesGTZero
                          (fst (nat_nbeq_iff (st X) 0)
                               (trans (sym (notInvolutive (st X == 0)))
                                      (cong {f=not} x_prf)))
                  in rewrite sym prf
                  in lte_minus_plus_sum lte_prf)
      hty' = hoare_assign (\st => st X + st Y = m)
      ht_body = hoare_seq (\st => (st X + st Y = m, BAssn (not (X == 0)) st))
                          (\st => st X + (st Y + 1) = m)
                          (\st => st X + st Y = m)
                          hty'
                          htx
      htw = hoare_consequence_pre
              (\st => (st X = m, st Y = 0))
              (\st => st X + st Y = m)
              (\st => (st X + st Y = m, Not (BAssn (not (X == 0)) st)))
              (hoare_while (\st => st X + st Y = m) ht_body)
              (\_, (x_prf, y_prf) => trans (plusCong x_prf y_prf)
                                           (plusZeroRightNeutral m))
      ht_program = hoare_seq (\st => st X = m)
                             (\st => (st X = m, st Y = 0))
                             (\st => ( st X + st Y = m
                                     , Not (BAssn (not (X == 0)) st) ))
                             htw
                             hty
  in hoare_consequence_post
       (\st => st X = m)
       (\st => st Y = m)
       (\st => (st X + st Y = m, Not (BAssn (not (X == 0)) st)))
       ht_program
       (\st, (prf, contra) =>
           let st_X_eq_0 =
                 fst (nat_beq_iff (st X) 0)
                     (trans (sym (notInvolutive (st X == 0)))
                            (cong {f=not} (fst not_true_iff_false contra)))
           in replace {P=\x => x + st Y = m} st_X_eq_0 prf)

add_slowly : Com
add_slowly =
  {-
    {{ (X = m, Z = n) }}
    ->> {{ X + Z = m + n }}
  -}
  WHILE (not (X == 0)) $ do
    {-
      {{ (X + Z = m + n, BAssn (not (X == 0)) st) }}
      ->> {{ X - 1 + Z + 1 = m + n }}
    -}
    Z ::= Z + 1
    -- {{ X - 1 + Z = m + n }}
    X ::= X - 1
    -- {{ X + Z = m + n }}
  {-
    {{ (X + Z = m + n, Not (BAssn (not (X == 0)) st)) }}
    ->> {{ Z = m + n }}
  -}

parity : Nat -> Nat
parity Z = 0
parity (S Z) = 1
parity (S (S k)) = parity k

parity_ge_2 : (n : Nat) -> LTE 2 n -> parity (minus n 2) = parity n
parity_ge_2 Z lte_prf = absurd $ succNotLTEzero lte_prf
parity_ge_2 (S Z) lte_prf = absurd $ succNotLTEzero (fromLteSucc lte_prf)
parity_ge_2 (S (S k)) lte_prf = rewrite minusZeroRight k
                                in Refl

parity_lt_2 : (n : Nat) -> Not (LTE 2 n) -> parity n = n
parity_lt_2 Z _ = Refl
parity_lt_2 (S Z) _ = Refl
parity_lt_2 (S (S k)) contra =
  let lte_prf = notLTImpliesGTE contra
  in absurd $ succNotLTEzero (fromLteSucc lte_prf)

parity_correct : HoareTriple (\st => st X = m)
                             (WHILE (2 <= X) $ do
                                X ::= X - 2)
                             (\st => st X = parity m)
parity_correct {m} =
  let htx = hoare_consequence_pre
              (\st => (parity (st X) = parity m, BAssn (2 <= X) st))
              (AssignSub X (X - 2) (\st => parity (st X) = parity m))
              (\st => parity (st X) = parity m)
              (hoare_assign (\st => parity (st X) = parity m))
              (\st, (prf, cond_prf) =>
                  rewrite parity_ge_2 (st X)
                                      (fst (lte_beq_iff 2 (st X)) cond_prf)
                  in prf)
      htw = hoare_while (\st => parity (st X) = parity m) htx
  in hoare_consequence
       (\st => st X = m)
       (\st => parity (st X) = parity m)
       (\st => st X = parity m)
       (\st => (parity (st X) = parity m, Not (BAssn (2 <= X) st)))
       htw
       (\st, p_st => cong p_st)
       (\st, (prf, nbeq_prf) =>
           let lte_prf = fst (lte_nbeq_iff 2 (st X))
                             (fst not_true_iff_false nbeq_prf)
               contra = fromNotLteSucc (lteImpliesNotGT lte_prf)
           in rewrite sym prf
           in sym (parity_lt_2 (st X) contra))

factorial : Com
factorial = do
  {-
    {{ X = m }}
    ->> {{ 1 * X! = m! }}
  -}
  Y ::= 1
  -- {{ Y * X! = m! }}
  WHILE (not (X == 0)) $ do
    {-
      {{ (Y * X! = m!, BAssn (not (X == 0)) st) }}
      ->> {{ Y * X * (X - 1)! = m! }}
    -}
    Y ::= Y * X
    -- {{ Y * (X - 1)! = m! }}
    X ::= X - 1
    -- {{ Y * X! = m! }}
  {-
    {{ (Y * X! = m!, Not (BAssn (not (X == 0)) st)) }}
    ->> {{ Y = m! }}
  -}

lemma1 : (x, y : Nat) -> Either (x = 0) (y = 0) -> minimum x y = 0
lemma1 _ _ (Left x_prf) = rewrite x_prf in Refl
lemma1 Z _ (Right _) = Refl
lemma1 (S _) _ (Right y_prf) = rewrite y_prf in Refl

lemma2 : (x, y : Nat) ->
         minimum (x `minus` 1) (y `minus` 1) = minimum x y `minus` 1
lemma2 Z _ = Refl
lemma2 (S k) Z = minimumZeroZeroLeft (minus k 0)
lemma2 (S k) (S j) = rewrite minusZeroRight k
                     in rewrite minusZeroRight j
                     in rewrite minusZeroRight (minimum k j)
                     in Refl

min : (a, b : Nat) -> Com
min a b = do
  {-
    {{ () }}
    ->> {{ 0 = minimum a b - minimum a b }}
  -}
  X ::= ANum a
  -- {{ 0 = minimum a b - minimum X b }}
  Y ::= ANum b
  -- {{ 0 = minimum a b - minimum X Y }}
  Z ::= 0
  -- {{ Z = minimum a b - minimum X Y }}
  WHILE (not (X == 0) && not (Y == 0)) $ do
    {-
      {{ (Z = minimum a b - minimum X Y, BAssn (not (X == 0) && not (Y == 0)) st) }}
      ->> {{ Z + 1 = minimum a b - minimum (X - 1) (Y - 1) }}
    -}
    X ::= X - 1
    -- {{ Z + 1 = minimum a b - minimum X (Y - 1) }}
    Y ::= Y - 1
    -- {{ Z + 1 = minimum a b - minimum X Y }}
    Z ::= Z + 1
    -- {{ Z = minimum a b - minimum X Y }}
  {-
    {{ (Z = minimum a b - minimum X Y, Not (BAssn (not (X == 0) && not (Y == 0)) st)) }}
    ->> {{ Z ::= minimum a b }}
  -}

two_loops : (a, b, c : Nat) -> Com
two_loops a b c = do
  {-
    {{ () }}
    ->> {{ c = 0 + 0 + c }}
  -}
  X ::= 0
  -- {{ c = X + 0 + c }}
  Y ::= 0
  -- {{ c = X + Y + c }}
  Z ::= ANum c
  -- {{ Z = X + Y + c }}
  WHILE (not (X == ANum a)) $ do
    {-
      {{ (Z = X + Y + c, BAssn (not (X == a)) st) }}
      ->> {{Z + 1 = X + 1 + Y + c }}
    -}
    X ::= X + 1
    -- {{ Z + 1 = X + Y + c }}
    Z ::= Z + 1
    -- {{ Z = X + Y + c }}
  {-
    {{ (Z = X + Y + c, Not (BAssn (not (X == a)) st)) }}
    ->> {{ Z = a + Y + c }}
  -}
  WHILE (not (Y == ANum b)) $ do
    {-
      {{ (Z = a + Y + c, BAssn (not (Y == b)) st) }}
      ->> {{ Z + 1 = a + Y + 1 + c }}
    -}
    Y ::= Y + 1
    -- {{ Z + 1 = a + Y + c }}
    Z ::= Z + 1
    -- {{ Z = a + Y + c }}
  {-
    {{ (Z = a + Y + c, Not (BAssn (not (Y == b)) st)) }}
    ->> {{ Z = a + b + c }}
  -}

dpow2_down : (m : Nat) -> Com
dpow2_down m = do
  {-
    {{ () }}
    ->> {{ (1 = 2^(0+1) - 1, 1 = 2^0) }}
  -}
  X ::= 0
  -- {{ (1 = 2^(X+1) - 1, 1 = 2^X) }}
  Y ::= 1
  -- {{ (Y = 2^(X+1) - 1, 1 = 2^X) }}
  Z ::= 1
  -- {{ (Y = 2^(X+1) - 1, Z = 2^X) }}
  WHILE (not (X == ANum m)) $ do
    {-
      {{ (Y = 2^(X+1) - 1, Z = 2^X, BAssn (not (X == m)) st) }}
      ->> {{ (Y + 2*Z = 2^(X+1+1) - 1, 2*Z = 2^(X+1)) }}
    -}
    Z ::= 2 * Z
    -- {{ (Y + Z = 2^(X+1+1) - 1, Z = 2^(X+1)) }}
    Y ::= Y + Z
    -- {{ (Y = 2^(X+1+1) - 1, Z = 2^(X+1)) }}
    X ::= X + 1
    -- {{ (Y = 2^(X+1) - 1, Z = 2^X) }}
  {-
    {{ (Y = 2^(X+1) - 1, Z = 2^X, Not (BAssn (not (X == m)) st)) }}
    ->> {{ Y = 2^(m+1) - 1 }}
  -}

IsWP : (p : Assertion) -> (c : Com) -> (q : Assertion) -> Type
IsWP p c q = ( HoareTriple p c q
             , (p' : Assertion) -> HoareTriple p' c q -> p' ->> p )

{-
  {{ X = 5 }} SKIP {{ X = 5 }}

  {{ Y + Z = 5 }} X ::= Y + Z {{ X = 5 }}

  {{ True }} X ::= Y {{ X = Y }}

  {{ Either (X = 0, Z = 4) (Not (X = 0), W = 3) }}
  IFB X == 0 THEN Y ::= Z + 1 ELSE Y ::= W + 2 FI
  {{ Y = 5 }}

  {{ Void }} X ::= 5 {{ X = 0 }}

  {{ () }}
  WHILE BTrue $ do X ::= 0
  {{ X = 0 }}
-}

is_wp_example : IsWP (\st => LTE (st Y) 4)
                     (X ::= Y + 1)
                     (\st => LTE (st X) 5)
is_wp_example = (ht, imp)
where ht : HoareTriple (\st => LTE (st Y) 4) (X ::= Y + 1) (\st => LTE (st X) 5)
      ht = hoare_consequence_pre (\st => LTE (st Y) 4)
                                 (\st => LTE (st Y + 1) 5)
                                 (\st => LTE (st X) 5)
                                 (hoare_assign (\st => LTE (st X) 5))
                                 (\st, p_st => rewrite plusCommutative (st Y) 1
                                               in LTESucc p_st)
      imp : (p' : Assertion) ->
            HoareTriple p' (X ::= Y + 1) (\st => LTE (st X) 5) ->
            p' ->> (\st => LTE (st Y) 4)
      imp p' ht' st p'_st =
        fromLteSucc (replace {P=\x => LTE x 5}
                             (plusCommutative (st Y) 1)
                             (ht' st _ (E_Ass Refl) p'_st))

hoare_assign_weakest : IsWP (AssignSub x a q) (x ::= a) q
hoare_assign_weakest {x} {a} {q} = (hoare_assign q, imp)
where imp : (p' : Assertion) -> HoareTriple p' (x ::= a) q ->
            p' ->> AssignSub x a q
      imp p' ht st p'_st = ht st _ (E_Ass Refl) p'_st


text:
module exactLength

-- Equality: Expressing Relationships Between Data

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

-- not good
-- exactLength : (len : Nat) -> (input : Vect m a) -> Maybe (Vect len a)
-- exactLength {m} len input = case m == len of
--                                  False => Nothing
--                                  True => ?exactLength_rhs_2

data EqNat : (num1 : Nat) -> (num2 : Nat) -> Type where
  Same : (num : Nat) -> EqNat num num

-- Functions as Proofs
-- sameS : EqNat k j -> EqNat (S k) (S j)
sameS : (k : Nat) -> (j : Nat) -> (eq : EqNat k j) -> EqNat (S k) (S j)
sameS k k (Same k) = Same (S k)

checkEqNat : (num1 : Nat) -> (num2 : Nat) -> Maybe (EqNat num1 num2)
checkEqNat Z Z = Just $ Same 0
checkEqNat Z (S k) = Nothing
checkEqNat (S k) Z = Nothing
checkEqNat (S k) (S j) = case checkEqNat k j of
                              Nothing => Nothing
                              Just x => Just (sameS _ _ x)

exactLength : (len : Nat) -> (input : Vect m a) -> Maybe (Vect len a)
exactLength {m} len input = case checkEqNat len m of
                                 Nothing => Nothing
                                 Just (Same m) => Just input

-- data (=) : a -> b -> Type where
--   Refl : x = x

-- cong : {func : a -> b} -> x = y -> func x = func y

-- 8.1.7 Exercises
same_cons : {xs : List a} -> {ys : List a} -> xs = ys -> x :: xs = x :: ys
same_cons Refl = Refl

same_lists : {xs : List a} -> {ys : List a} -> x = y -> xs = ys -> x :: xs = y :: ys
same_lists Refl Refl = Refl

data ThreeEq : a -> b -> c -> Type where
  SameSame : ThreeEq x x x

allSameS : (x, y, z : Nat) -> ThreeEq x y z -> ThreeEq (S x) (S y) (S z)
allSameS x x x SameSame = SameSame


text:
module India.Wrapper

import Text.Lexer

%default total

public export
interface Wrapper (0 f : Type -> Type) where
  unwrap : f a -> a

export
Wrapper TokenData where
  unwrap = tok

max_stars_repo_name: berewt/india

max_issues_repo_name: berewt/india

max_forks_repo_name: berewt/india


text:
-- examples in "Type-Driven Development with Idris"
-- chapter 13, section 1

-- check that all functions are total
%default total

--
-- see Door.idr
-- see VendingMachine.idr
--

max_stars_repo_name: pascalpoizat/idris-book

max_issues_repo_name: pascalpoizat/idris-book

max_forks_repo_name: pascalpoizat/idris-book


text:
module Solutions.Day1

import Common

part1 : Integer -> List Integer -> Integer
part1 count (first :: next@( second :: rest )) = let
    count = if first < second then count + 1 else count in
    part1 count next
part1 count xs = count

part2 : Integer -> Integer -> List Integer -> Integer
part2 count slidingSum (fst :: next@(snd :: trd :: rest)) = let
  sum = fst + snd + trd
  count = if sum > slidingSum then count + 1 else count in
  part2 count sum next
part2 count slidingSum other = count - 1

export
run : Solution
run input = do
  values <- linesToInts input
  let sol1 = part1 0 values            -- 1722
  let sol2 = part2 0 0 values       -- 1748
  Right (show sol1, show sol2)


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

module Language.IPKG.Tokens

import Text.Token

%default total

public export
data Punctuation
    = Comma
    | Dot
    | Equal

public export
Eq Punctuation where
    (==) Comma Comma = True
    (==) Dot Dot = True
    (==) Equal Equal = True
    (==) _ _ = False

public export
data Key
    = KVersion
    | KAuthors
    | KMaintainers
    | KLicense
    | KBrief
    | KReadme
    | KHomepage
    | KSourceLoc
    | KBugtracker
    | KDepends
    | KModules
    | KMainMod
    | KExecutable
    | KOptions
    | KSourceDir
    | KBuildDir
    | KOutputDir
    | KPreBuild
    | KPostBuild
    | KPreInstall
    | KPostInstall
    | KPreClean
    | KPostClean

public export
Eq Key where
    KVersion == KVersion = True
    KAuthors == KAuthors = True
    KMaintainers == KMaintainers = True
    KLicense == KLicense = True
    KBrief == KBrief = True
    KReadme == KReadme = True
    KHomepage == KHomepage = True
    KSourceLoc == KSourceLoc = True
    KBugtracker == KBugtracker = True
    KDepends == KDepends = True
    KModules == KModules = True
    KMainMod == KMainMod = True
    KExecutable == KExecutable = True
    KOptions == KOptions = True
    KSourceDir == KSourceDir = True
    KBuildDir == KBuildDir = True
    KOutputDir == KOutputDir = True
    KPreBuild == KPreBuild = True
    KPostBuild == KPostBuild = True
    KPreInstall == KPreInstall = True
    KPostInstall == KPostInstall = True
    KPreClean == KPreClean = True
    KPostClean == KPostClean = True
    _ == _ = False

public export
data IPKGTokenKind
    = ITPackage
    | ITKey Key
    | ITString
    | ITPunct Punctuation
    | ITBare
    | ITIgnored

public export
IPKGToken : Type
IPKGToken = Token IPKGTokenKind

public export
Eq IPKGTokenKind where
    (==) ITPackage ITPackage = True
    (==) (ITKey x) (ITKey y) = x == y
    (==) ITString ITString = True
    (==) (ITPunct x) (ITPunct y) = x == y
    (==) ITBare ITBare = True
    (==) ITIgnored ITIgnored = True
    (==) _ _ = False

private
unescape : List Char -> List Char
unescape ('"'::rest) = loop rest
    where
        loop : List Char -> List Char
        loop [] = []
        loop ('"'::_) = []
        loop ('\\'::'"'::rest) = '"' :: loop rest
        loop (x::rest) = x :: loop rest
unescape _ = []

public export
TokenKind IPKGTokenKind where
    TokType ITPackage = ()
    TokType (ITKey _) = Key
    TokType ITString = String
    TokType (ITPunct _) = ()
    TokType ITBare = String
    TokType ITIgnored = ()

    tokValue ITPackage _ = ()
    tokValue (ITKey k) _ = k
    tokValue ITString s = pack . unescape . unpack $ s
    tokValue (ITPunct _) _ = ()
    tokValue ITBare s = s
    tokValue ITIgnored _ = ()

export
ignored : IPKGToken -> Bool
ignored (Tok ITIgnored _) = True
ignored _ = False

max_stars_repo_name: tiatomee/ipkg-idr

max_issues_repo_name: tiatomee/ipkg-idr

max_forks_repo_name: tiatomee/ipkg-idr


text:
import Js.ASync

export
data ServiceM : Type -> Type where
  PureServ : a -> ServiceM a

get_jsio : ServiceM a -> JS_IO (Either String a)
get_jsio (PureServ x) = do
  pure $ Right x

export
mytst : String -> ServiceM String
mytst x = PureServ $ "ola "

call_fn : (String -> JS_IO String) -> String -> JS_IO String
call_fn f x = jscall
                  "%0(%1)"
                  ((JsFn (String -> JS_IO String)) -> String -> JS_IO String)
                  (MkJsFn f)
                  x

mytstJs : String -> JS_IO String
mytstJs x = do
  r <- get_jsio $ mytst "arst"
  case r of
      Right k => pure k

tst2 : JS_IO String
tst2 = call_fn mytstJs "inputmytst"

export
main : JS_IO ()
main = do
  putStrLn' "start"
  r <- tst2
  putStrLn' "olare"
  putStrLn' r

max_stars_repo_name: rbarreiro/idrisjs

max_issues_repo_name: prozacchiwawa/idrisjs

max_forks_repo_name: prozacchiwawa/idrisjs


text:
module RemoveElem

import Data.Vect

-- Dependent pair implementation of removeElem for fun
depPRemElem : DecEq a => (value : a) -> (xs : Vect n a) -> (len ** Vect len a)
depPRemElem value [] = (_ ** [])
depPRemElem value (x :: xs) = case decEq value x of
                                   (Yes prf) => (_ ** xs)
                                   (No contra) => (_ ** (x :: (snd $ depPRemElem value xs)))

maryInVector : Elem "Mary" ["Pete", "Bob", "Mary"]
maryInVector = There (There Here)

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

removeElem_auto : (value : a) -> (xs : Vect (S n) a) -> {auto prf : Elem value xs} -> Vect n a
removeElem_auto value xs {prf} = removeElem value xs prf

public export
removeElemAuto : (value : a) -> (xs : Vect (S n) a) -> {auto prf : Elem value xs} -> Vect n a
removeElemAuto value (value :: ys) {prf = Here} = ys
removeElemAuto {n = Z} value (y :: []) {prf = (There later)} = absurd later
removeElemAuto {n = (S k)} value (y :: ys) {prf = (There later)} = y :: (removeElemAuto value ys)


text:
module Test.TestFixed

import Test.TestUtil
import Data.Time.Clock.Internal.Fixed

getDec : Integer -> Dec
getDec x = MkFixed x

getPico : Integer -> Pico
getPico x = MkFixed x

export
testAdd: IO ()
testAdd = do
  let a = getPico 1
  let b = getPico 1
  assertEq "testAdd" (a + b) 2 ""

export
testSub: IO ()
testSub = do
  let a = getPico 5
  let b = getPico 3
  assertEq "testSub" (a - b) 2 ""

export
testNegate: IO ()
testNegate = do
  let a = negate $ getPico 5
  assertEq "testNegate" a (-5) (show a)

export
testMultFixed: IO ()
testMultFixed = do
  let a = getDec 123
  let b = getDec 25
  let result = a * b
  assertEq "testMultFixed" result 30 (show result)

export
testFracDiv: IO ()
testFracDiv = do
  let a = getDec 3456
  let b = getDec 1234
  let result = a / b
  assertEq "testMultFixed" result 280 (show result)

export
testRecip: IO ()
testRecip = do
  let a = getDec 3456
  let result = recip a
  assertEq "testRecip" result 2 (show result)

max_stars_repo_name: gdevanla/idris-time

max_issues_repo_name: gdevanla/idris-time

max_forks_repo_name: gdevanla/idris-time


text:
-- This is a test of the substring primitive, both in the Idris
-- evaluator and in some backend. It attempts to exercise that
-- negative indices are equivalent to 0, that it works for mixed
-- single- and multi-byte characters, and that overshooting the end
-- doesn't break things.

-- Single byte test
foo : String
foo = "Hello! here's the thing"

-- The first sentence of the Chinese wikipedia article on Idris (to
-- get mixed single-and-multibyte chars)
firstSentence : String
firstSentence = "Idris 是一个通用的依赖类型纯函数式编程语言，其类型系统与 Agda 以及 Epigram 相似。"

emptyTest : prim__strSubstr 100000 14 Main.firstSentence = ""
emptyTest = Refl

multiTest : prim__strSubstr 10 5 Main.firstSentence = "用的依赖类"
multiTest = Refl

negative : prim__strSubstr (-10) 5 Main.firstSentence = "Idris"
negative = Refl

negativeEnd : prim__strSubstr 0 (-1) Main.firstSentence = ""
negativeEnd = Refl

negativeLength : prim__strSubstr 4 (-4) Main.firstSentence = ""
negativeLength = Refl

main : IO ()
main = do putStrLn $ prim__strSubstr 1 1004 foo
          printLn $ length $ prim__strSubstr 1 1000 foo
          printLn $ length $ prim__strSubstr 1000 2 firstSentence
          putStrLn $ prim__strSubstr 10 5 firstSentence
          putStrLn $ prim__strSubstr (-10) 5 firstSentence
          putStrLn $ "[" ++ prim__strSubstr 0 (-1) firstSentence ++ "]"
          -- Multi-byte dynamic string
          input <- getLine
          putStrLn $ prim__strSubstr 3 8 input
          putStrLn $ show (length (prim__strSubstr 3 8 input))
          putStrLn $ prim__strSubstr 3 8000 input
          putStrLn $ show (length (prim__strSubstr 3 8000 input))
          putStrLn $ prim__strSubstr (-13) 18 input
          putStrLn $ show (length (prim__strSubstr (-13) 18 input))
          putStrLn $ prim__strSubstr 4 (-4) input
          putStrLn $ show (length (prim__strSubstr 4 (-4) input))
          -- Single-byte dynamic string
          input <- getLine
          putStrLn $ prim__strSubstr 3 8 input
          putStrLn $ show (length (prim__strSubstr 3 8 input))
          putStrLn $ prim__strSubstr 3 8000 input
          putStrLn $ show (length (prim__strSubstr 3 8000 input))
          putStrLn $ prim__strSubstr (-13) 18 input
          putStrLn $ show (length (prim__strSubstr (-13) 18 input))
          putStrLn $ prim__strSubstr 4 (-4) input
          putStrLn $ show (length (prim__strSubstr 4 (-4) input))


text:
module DateTime

import Coda.Date
import Coda.Time

{-
  ISO 8601 DateTime Package

  DateTime Representation inclues:

    Year - Month - Day T Hour : Minute : Second (+/-) Offset

  See Time.idr and Date.idr

-}

{-
  Type Definitions
-}

data DateTime : Type where
  MkDateTime : (d : Date) -> (i : Instant) -> DateTime

%name DateTime dt,dt1,dt2,dt3

data LocalDateTime : TimeZone offset -> Type where
  MkLocalDateTime : (tz : TimeZone offset) ->
                    (d : DateTime) ->
                    LocalDateTime tz

%name LocalDateTime ldt,ldt1,ldt2,ldt3

{-
  Standard Interface Implementations
-}

Eq DateTime where
  (==) (MkDateTime d i) (MkDateTime d1 i1) = d == d1 && i == i1

Ord DateTime where
  compare (MkDateTime d i) (MkDateTime d1 i1) =
    case compare d d1 of
         EQ => compare i i1
         r => r

Show DateTime where
  show (MkDateTime d i) = show d ++ "T" ++ show i

Eq (LocalDateTime tz) where
  (==) (MkLocalDateTime tz dt) (MkLocalDateTime tz dt1) = dt == dt1

Ord (LocalDateTime tz) where
  compare (MkLocalDateTime tz dt) (MkLocalDateTime tz dt1) = compare dt dt1

Show (LocalDateTime (MkTimeZone name offset)) where
  show (MkLocalDateTime (MkTimeZone name offset) dt) = show dt ++ show offset

max_stars_repo_name: ostera/idris-coda

max_issues_repo_name: ostera/idris-coda

max_forks_repo_name: ostera/idris-coda


text:
-- hello.idr
main : IO()
main = putStrLn "Hello world!"

max_stars_repo_name: shij-hsu/idr

max_issues_repo_name: shij-hsu/idr

max_forks_repo_name: shij-hsu/idr