text:
{--
Copyright 2021 Joel Berkeley

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    http://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
--}
||| This module contains the `Tensor` object, an array of values of arbitrary type, along with a
||| number of functions operating on numeric `Tensor`s.
module Tensor

import Data.Vect
import Data.Vect.Elem
import Decidable.Equality

import Error
import public Primitive
import public Types
import Util
import XLA.Client.XlaBuilder
import XLA.Literal

----------------------------- core definitions ----------------------------

||| A `Tensor` is a symbolic value, which may refer to either to a scalar value or array of values,
||| though the runtime representation will likely contain more than its value, and will depend on
||| the specific backend.
|||
||| @shape The `Tensor` shape.
||| @dtype The element type.
export
data Tensor : (0 shape : Shape {rank}) -> (0 dtype : Type) -> Type where
  MkTensor : RawTensor -> Tensor shape dtype

||| Construct a `Tensor` from `Array` data.
export
const : Primitive dtype => {shape : _} -> Array shape {dtype} -> Tensor shape dtype
const xs = MkTensor $ const {rank=length shape} (rewrite lengthCorrect shape in xs)

||| Evaluate a `Tensor`, returning its value as an `Array`.
export
eval : Primitive dtype => {shape : _} -> Tensor shape dtype -> IO $ Array shape {dtype}
eval (MkTensor raw) = eval raw

||| Return a string representation of an unevaluated `Tensor`, detailing all enqueued operations.
||| Useful for debugging.
export
toString : Tensor shape dtype -> IO String
toString (MkTensor raw) = toString raw

||| A mutable tensor. That is, a tensor that can be modified in-place.
|||
||| We can do this in Idris with linearity. Linearity is offered by quantitative type theory*, which
||| allows us to guarantee that a value is used at run time either never (erased), once (linear), or
||| more. In-place mutation traditionally suffers from the problem that you have to reason about
||| what state a value is in in a series of computations: whether it has been mutated and how. For
||| example, in the following pseudo-code,
|||
||| ```
||| a = 1
||| a += 1
||| b = f(a)
||| ```
|||
||| We have to be aware of whether `a` was modified between its initialization and its use in the
||| calculation of `b`. This problem is solved by simply defining a new variable, as
|||
||| ```
||| a = 1
||| a' = a + 1
||| b = f(a')
||| ```
|||
||| but this doesn't provide the same performance benefits of in-place mutation. The conundrum is
||| (at least largely) solved with linear types, because you can require that the action of mutating
||| a value "uses it up" such that the previous reference to it cannot be used any more. In the
||| first example, the mutation `a += 1` would use up `a` and we wouldn't be able to use it in the
||| construction of `b`, so the problem no longer exists.
|||
||| In order to ensure `Variable` is only used as a linear type, it is accessible only via the
||| function `var`.
|||
||| *See http://www.type-driven.org.uk/edwinb
|||
||| @shape The `Variable` shape.
||| @dtype The element type.
export
data Variable : (0 shape : Shape) -> (0 dtype : Type) -> Type where
  MkVariable : Primitive dtype => Array shape {dtype=dtype} -> Variable shape dtype

||| Provides access to a linear `Variable` with initial contents `arr`. For example:
|||
||| ```idris
||| addOne : (1 v : Variable [] Double) -> Variable [] Double
||| addOne v = v += const {shape=[]} 1
|||
||| three : Tensor [] Double
||| three = var 2.0 $ \v => freeze $ addOne v
||| ```
|||
||| @arr The initial contents of the `Variable`.
||| @f A function which uses the `Variable`. The return value of `f` is returned by `var`.
var : Primitive dtype =>
      Array shape {dtype=dtype} -> (1 f : (1 v : Variable shape dtype) -> a) -> a
var arr f = f (MkVariable arr)

||| Convert a `Variable` to a `Tensor`.
freeze : (1 _ : Variable shape dtype) -> Tensor shape dtype

----------------------------- structural operations ----------------------------

||| Get the `idx`-th row from a tensor. For example, `index 1 $ const [[1, 2], [3, 4], [5, 6]]`
||| is equivalent to `const [3, 4]`.
|||
||| @idx The row to fetch.
export
index : (idx : Fin d) -> Tensor (d :: ds) dtype -> Tensor ds dtype

||| Split a `Tensor` along the first axis at the specified index. For example,
||| `split 1 const [[1, 2], [3, 4], [5, 6]]` is equivalent to
||| `(const [[1, 2]], const [[3, 4], [5, 6]])`.
|||
||| @idx The index of the row at which to split the `Tensor`. The row with index `idx` in
|||   the input `Tensor` will appear in the result as the first row in the second `Tensor`.
export
split : (idx : Nat) -> Tensor ((idx + rest) :: tl) dtype
  -> (Tensor (idx :: tl) dtype, Tensor (rest :: tl) dtype)

||| Concatenate two `Tensor`s along their first axis. For example,
||| `concat (const [[1, 2], [3, 4]]) (const [[5, 6]])` is equivalent to
||| `const [[1, 2], [3, 4], [5, 6]]`.
export
concat : Tensor (n :: tl) dtype -> Tensor (m :: tl) dtype -> Tensor ((n + m) :: tl) dtype

||| Add a dimension of length one at the specified `axis`. The new dimension will be at the
||| specified axis in the new `Tensor` (as opposed to the original `Tensor`). For example,
||| `expand 1 $ const [[1, 2], [3, 4], [5, 6]]` is equivalent to
||| `const [[[1, 2]], [[3, 4]], [[5, 6]]]`.
export
expand :
  (axis : Fin (S rank)) -> Tensor {rank=rank} shape dtype -> Tensor (insertAt axis 1 shape) dtype

||| Tranpose the last two axes of a tensor. For example, `(const [[1, 2], [3, 4]]).T` is equivalent
||| to `const [[1, 3], [2, 4]]`.
export
(.T) : forall shape, dtype . Tensor shape dtype ->
       let leading = init (init shape)
           m = last (init shape)
           n = last shape
        in Tensor (leading ++ [n, m]) dtype

||| Cast the tensor elements to a new data type.
export
cast_dtype : Cast dtype dtype' => Tensor shape dtype -> Tensor shape dtype'

||| Construct a diagonal tensor from the specified value, where all off-diagonal elements are zero.
||| For example, `the (Tensor [2, 2] Double) (diag 3)` is equivalent to
||| `const [[3.0, 0.0], [0.0, 3.0]]`.
export
diag : Num dtype => Tensor [] dtype -> Tensor [n, n] dtype

||| A `DimBroadcastable from to` proves that a dimension of size `from` can be broadcast to a
||| dimension of size `to`.
public export
data DimBroadcastable : (0 from : Nat) -> (0 to : Nat) -> Type where
  ||| Proof that any dimension can be broadcast to itself. For example in shapes `[2, 3]` to
  ||| `[2, 3]`.
  Same : DimBroadcastable x x

  ||| Proof that a dimension of length one can be broadcast to any size. For example in shapes
  ||| `[2, 1]` to `[2, 3]`
  Stack : DimBroadcastable 1 _

  ||| Proof that any dimension can be broadcast to zero. For example in shapes `[2, 3]` to `[2, 0]`.
  Zero : DimBroadcastable _ 0

namespace Broadcastable
  ||| A `Broadcastable from to` constitutes proof that the shape `from` can be broadcast to the
  ||| shape `to`.
  public export
  data Broadcastable : (0 from : Shape) -> (0 to : Shape) -> Type where
    ||| Proof that a shape can be broadcast to itself. For example:
    |||
    ||| [] to []
    ||| [3, 4] to [3, 4]
    |||
    ||| Implementation note: we could have used `Broadcast [] []`, which would have resulted in more
    ||| atomic constructors for `Broadcastable`, but the author guesses that this implementation helps
    ||| the type checker avoid applications of `Match`.
    Same : Broadcastable x x

    ||| Proof that a dimension of size `f` can be broadcast to size `t` if these dimensions
    ||| are `DimBroadcastable f t`. For example:
    |||
    ||| [2, 3] to [2, 3]
    ||| [2, 1] to [2, 3]
    ||| [2, 1] to [2, 0]
    Match : {0 from, to : Shape {rank=r}}
            -> {auto 0 _ : DimBroadcastable f t}
            -> Broadcastable from to
            -> Broadcastable (f :: from) (t :: to)

    ||| Proof that broadcasting can add outer dimensions i.e. nesting. For example:
    |||
    ||| [3] to [1, 3]
    ||| [3] to [5, 3]
    Nest : Broadcastable f t -> Broadcastable f (_ :: t)

empty : Primitive dtype => {shape : Shape} -> {auto isEmpty : Elem 0 shape} -> Tensor shape dtype
empty = const (emptyArray shape) where
  emptyArray : (shape : _) -> {auto isEmpty : Elem Z shape} -> Array shape
  emptyArray {isEmpty = Here} (0 :: _) = []
  emptyArray {isEmpty = (There _)} (d :: ds) = replicate d (emptyArray ds)

||| Broadcast a `Tensor` to a new compatible shape. For example,
|||
||| ```idris
||| x : Tensor [2, 3] Double
||| x = broadcast (const [4, 5, 6])
||| ```
|||
||| is equivalent to
|||
||| ```idris
||| x : Tensor [2, 3] Double
||| x = const [[4, 5, 6], [4, 5, 6]]
||| ```
export
broadcast : Primitive dtype => {from : _} -> {to : _} -> {auto prf : Broadcastable from to}
  -> Tensor from dtype -> Tensor to dtype
broadcast xs = case (isElem 0 to, toList from == toList to) of
  (Yes _, False) => empty
  _ =>
    let from_prf = lengthCorrect from
        to_prf = lengthCorrect to in
        rewrite sym to_prf in impl {fr=length from} {tr=length to} {tt=length to} []
          (rewrite to_prf in to) (rewrite from_prf in xs)
          {prf=rewrite to_prf in rewrite from_prf in prf}

    where
    impl : {fr, tr : _} -> {from : Shape {rank=fr}} -> {to : Shape {rank=tr}}
      -> {tl, tt : _} -> (to_leading : Vect tl Nat) -> (to_trailing : Vect tt Nat)
      -> {auto prf : Broadcastable from to_trailing} -> Tensor from dtype -> Tensor to dtype
    impl to_leading _ {prf=Same} (MkTensor raw) =
      MkTensor $ if (length to_leading == 0) then raw else broadcast raw to_leading
    impl {fr = (S r)} to_leading (th' :: tt') {prf=(Match _)} (MkTensor raw) =
      MkTensor $ broadcast (broadcastInDim raw (th' :: tt') (range (S r))) to_leading
    impl to_leading (th' :: tt') {prf=(Nest _)} xs = impl (to_leading ++ [th']) tt' xs

scalarToAnyOk : (to : Shape) -> Broadcastable [] to
scalarToAnyOk [] = Same
scalarToAnyOk (_ :: xs) = Nest (scalarToAnyOk xs)

namespace Squeezable
  ||| A `Squeezable from to` constitutes proof that the shape `from` can be squeezed to the
  ||| shape `to`. Squeezing is the process of removing any number of dimensions of length one.
  public export
  data Squeezable : (0 from : Shape) -> (0 to : Shape) -> Type where
    ||| Proof that a shape can be squeezed to itself. For example:
    |||
    ||| [] to []
    ||| [3, 4] to [3, 4]
    Same : Squeezable x x

    ||| Proof that any dimensions (including those of length 1) can be preserved in the process of
    ||| squeezing. For example:
    |||
    ||| ...
    Match : Squeezable from to -> Squeezable (x :: from) (x :: to)

    ||| Proof that any dimensions of length one can be squeezed out. For example:
    |||
    ||| [1, 3, 1, 1, 4] to [3, 4]
    Nest : Squeezable from to -> Squeezable (1 :: from) to

||| Remove dimensions of length one from a `Tensor` such that it has the desired shape. For example:
|||
||| ```idris
||| x : Tensor [2, 1, 3, 1] Double
||| x = const [[[[4], [5], [6]]], [[[7], [8], [9]]]]
|||
||| y : Tensor [2, 1, 3] Double
||| y = squeeze x
||| ```
|||
||| is equivalent to
|||
||| ```idris
||| y : Tensor [2, 1, 3] Double
||| y = const [[[4, 5, 6]], [[7, 8, 9]]]
||| ```
export
squeeze : {auto 0 _ : Squeezable from to} -> Tensor from dtype -> Tensor to dtype

||| A `Tensor` where every element has the specified value. For example,
|||
||| ```idris
||| fives : Tensor [2, 3] Int
||| fives = fill 5
||| ```
||| is equivalent to
||| ```idris
||| fives : Tensor [2, 3] Int
||| fives = const [[5, 5, 5], [5, 5, 5]]
||| ```
export
fill : Primitive dtype => {shape : _} -> dtype -> Tensor shape dtype
fill = broadcast {prf=scalarToAnyOk shape} . const

----------------------------- numeric operations ----------------------------

infix 6 ==#, /=#

||| Element-wise equality. For example, `const [1, 2] ==# const [1, 3]` is equivalent to
||| `const [True, False]`.
export
(==#) : Eq dtype => Tensor shape dtype -> Tensor shape dtype -> Tensor shape Bool
(MkTensor l) ==# (MkTensor r) = MkTensor (eq l r)

||| Element-wise inequality. For example, `const [1, 2] /=# const [1, 3]` is equivalent to
||| `const [False, True]`.
export
(/=#) : Eq dtype => Tensor shape dtype -> Tensor shape dtype -> Tensor shape Bool
(MkTensor l) /=# (MkTensor r) = MkTensor (ne l r)

infix 6 <#, >#, <=#, >=#

||| Element-wise less than. For example, `const [1, 2, 3] <# const [2, 2, 2]` is equivalent to
||| `const [True, False, False]`.
export
(<#) : Ord dtype => Tensor shape dtype -> Tensor shape dtype -> Tensor shape Bool
(MkTensor l) <# (MkTensor r) = MkTensor (lt l r)

||| Element-wise greater than. For example, `const [1, 2, 3] ># const [2, 2, 2]` is equivalent to
||| `const [False, False, True]`.
export
(>#) : Ord dtype => Tensor shape dtype -> Tensor shape dtype -> Tensor shape Bool
(MkTensor l) ># (MkTensor r) = MkTensor (gt l r)

||| Element-wise less than or equal. For example, `const [1, 2, 3] <=# const [2, 2, 2]` is
||| equivalent to `const [True, True, False]`.
export
(<=#) : Ord dtype => Tensor shape dtype -> Tensor shape dtype -> Tensor shape Bool
(MkTensor l) <=# (MkTensor r) = MkTensor (le l r)

||| Element-wise greater than or equal. For example, `const [1, 2, 3] >=# const [2, 2, 2]` is
||| equivalent to `const [False, True, True]`.
export
(>=#) : Ord dtype => Tensor shape dtype -> Tensor shape dtype -> Tensor shape Bool
(MkTensor l) >=# (MkTensor r) = MkTensor (ge l r)

-- see https://www.python.org/dev/peps/pep-0465/#precedence-and-associativity
infixl 9 @@

||| Matrix multiplication. The tensors are contracted along the last axis of the first tensor and
||| the first axis of the last tensor. For example:
|||
||| ```idris
||| x : Tensor [2, 3] Double
||| x = const [[-1, -2, -3], [0, 1, 2]]
|||
||| y : Tensor [3, 1] Double
||| y = const [[4, 0, 5]]
|||
||| z : Tensor [2, 1] Double
||| z = x @@ y
||| ```
|||
||| is equivalent to
|||
||| ```idris
||| z : Tensor [2, 1] Double
||| z = const [-19, 10]
||| ```
export
(@@) : Num dtype => Tensor l dtype -> Tensor (S n :: tail') dtype ->
       {auto 0 _ : last l = S n} -> Tensor (init l ++ tail') dtype

||| Element-wise addition. For example, `const [1, 2] + const [3, 4]` is equivalent to
||| `const [4, 6]`.
export
(+) : Num dtype => Tensor shape dtype -> Tensor shape dtype -> Tensor shape dtype
(MkTensor ll_raw) + (MkTensor rr_raw) = MkTensor (add ll_raw rr_raw)

||| Element-wise negation. For example, `- const [1, -2]` is equivalent to `const [-1, 2]`.
export
negate : Neg dtype => Tensor shape dtype -> Tensor shape dtype

||| Element-wise subtraction. For example, `const [3, 4] - const [4, 2]` is equivalent to
||| `const [-1, 2]`.
export
(-) : Neg dtype => Tensor shape dtype -> Tensor shape dtype -> Tensor shape dtype

infixl 9 *#, /#

||| Elementwise multiplication. For example, `const [2, 3] *# const [4, 5]` is equivalent to
||| `const [8, 15]`.
export
(*#) : Num dtype => Tensor shape dtype -> Tensor shape dtype -> Tensor shape dtype
(MkTensor l) *# (MkTensor r) = MkTensor (mul l r)

||| Multiplication by a constant. For example, `const 2 * const [3, 5]` is equivalent to
||| `const [6, 10]`.
export
(*) : (Primitive dtype, Num dtype) => Tensor [] dtype -> {shape : _} -> Tensor shape dtype
      -> Tensor shape dtype
l * r = (broadcast {prf=scalarToAnyOk shape} l) *# r

||| Elementwise floating point division. For example, `const [2, 3] /# const [4, 5]` is equivalent to
||| `const [0.5, 0.6]`.
export
(/#) : Fractional dtype => Tensor shape dtype -> Tensor shape dtype -> Tensor shape dtype

||| Floating point division by a constant. For example, `const [3.4, -5.6] / const 2` is equivalent
||| to `const [1.7, -2.8]`.
export
(/) : Fractional dtype => Tensor shape dtype -> Tensor [] dtype -> Tensor shape dtype

infixr 9 ^

-- todo we don't support complex yet
||| Each element in `base` raised to the power of the corresponding element in `exponent`.
||| example, `const [2, 25, -9] ^ const [3, -0.5, 0.5]` is equivalent to `const [8, 0.2, 3i]`.
|||
||| Note: The first root is used.
export
(^) : Num dtype => Tensor shape dtype -> Tensor shape dtype -> Tensor shape dtype

-- todo
||| The element-wise natural exponential.
export
exp : Tensor shape Double -> Tensor shape Double

infix 8 +=
infix 8 -=
infix 8 *=
infix 8 //=

||| Element-wise in-place addition. It is in-place in the sense that the value in memory is mutated
||| in-place. However, since the function is linear its `Variable`, you must still use the result to
||| get the updated value. For example:
|||
||| ```idris
||| addOne : (1 v : Variable [] Double) -> Variable [] Double
||| addOne v = v += const {shape=[]} 1
||| ```
|||
||| Other than the fact that it works on a `Variable`, and mutates the value in-place, it works
||| exactly like `(+)` on a `Tensor`.
export
(+=) : Num dtype => (1 v : Variable shape dtype) -> Tensor shape dtype -> Variable shape dtype

||| Element-wise in-place subtraction. See `(+=)` and `(+)` for details.
export
(-=) : Neg dtype => (1 v : Variable shape dtype) -> Tensor shape dtype -> Variable shape dtype

||| Element-wise in-place multiplication. See `(+=)` and `(*)` for details.
export
(*=) : Num dtype => (1 v : Variable shape dtype) -> Tensor shape dtype -> Variable shape dtype

||| Element-wise in-place division. See `(+=)` and `(/)` for details.
export
(//=) : Fractional dtype =>
        (1 v : Variable shape dtype) -> Tensor shape dtype -> Variable shape dtype

-- todo
||| The element-wise natural logarithm.
export
log : Tensor shape Double -> Tensor shape Double

||| Reduce a `Tensor` along the specified `axis` to the smallest element along that axis, removing
||| the axis in the process. For example, `reduce_min 1 $ const [[-1, 5, 10], [4, 5, 6]]` is
||| equivalent to `const [-1, 5, 6]`.
export
reduce_min : Num dtype => (axis : Fin (S r)) -> Tensor {rank=S r} shape dtype ->
  {auto 0 _ : IsSucc $ index axis shape} -> Tensor (deleteAt axis shape) dtype

||| Reduce a `Tensor` along the specified `axis` to the sum of its components, removing the axis in
||| the process. For example, `reduce_sum 1 $ const [[-1, 2, 3], [4, 5, -6]]` is equivalent to
||| `const [3, 7, -3]`.
export
reduce_sum : Num dtype => (axis : Fin (S r)) -> Tensor {rank=S r} shape dtype ->
  {auto 0 _ : IsSucc $ index axis shape} ->  Tensor (deleteAt axis shape) dtype

---------------------------- other ----------------------------------

||| The determinant of a tensor (with respect to the last two axes). For example,
||| `det $ const [[1, 2], [3, 4]]` is equivalent to `const -2`.
export
det : forall shape, dtype . Neg dtype => Tensor shape dtype ->
      let leading = init (init shape)
          m = last (init shape)
          n = last shape
       in {auto 0 isSquare : m = n} -> {auto 0 nonEmpty : IsSucc m} -> Tensor leading dtype

||| Cholesky decomposition. Finds the lower triangular matrix `L` from `X` s.t. `X = L @@ L.T`.
export
cholesky : Tensor [S n, S n] dtype -> Tensor [S n, S n] dtype

infix 9 \\

||| Find `Y` from `A` and `X` s.t. `X = AY` where `A` is a lower triangular matrix.
export
(\\) : Tensor [n, n] dtype -> Tensor (n :: tl) dtype -> Tensor (n :: tl) dtype

||| Indicates an operation was impossible (at the attempted precision) due to a matrix being
||| singular.
export
data SingularMatrixError = MkSingularMatrixError String

export
Error SingularMatrixError where
  format (MkSingularMatrixError msg) = msg

||| The inverse of a matrix. For example, `inverse $ const [[1, 2], [3, 4]]` is equivalent to
||| `const [[-2, -1], [-1.5, -0.5]]`.
export
inverse : Tensor [S n, S n] Double -> Either SingularMatrixError $ Tensor [S n, S n] Double

||| The product of all elements along the diagonal of a matrix. For example,
||| `trace_product $ const [[2, 3], [4, 5]]` is equivalent to `const 10`.
export
trace_product : Num dtype => Tensor [S n, S n] dtype -> Tensor [] dtype

||| Sum the elements along the diagonal of the input.
export
trace : Num dtype => Tensor [S n, S n] dtype -> Tensor [] dtype

max_stars_repo_name: joelberkeley/spidr

max_issues_repo_name: joelberkeley/spidr

max_forks_repo_name: joelberkeley/spidr


text:
|||
module Toolkit.Data.Graph.EdgeBounded.DegreeCommon

import Decidable.Equality

import Data.String
import Data.List.Elem
import Data.List.Quantifiers

import Toolkit.Decidable.Do
import Toolkit.Decidable.Informative

import Toolkit.Data.Nat
import Toolkit.Data.Pair
import Toolkit.Data.List.Size
import Toolkit.Data.List.Occurs.Does

%default total

namespace HasDegree

  public export
  data DegreeType = I | O

  public export
  record Error where
    constructor MkError
    vertexID : Nat
    degType  : DegreeType
    values   : Occurs.Error

-- [ EOF ]

ext: idr

max_stars_repo_name: gallais/linear-circuits

max_issues_repo_name: gallais/linear-circuits

max_forks_repo_name: gallais/linear-circuits


text:
append : Vect n a -> Vect m a ->
         Vect (n + m) a

append [] ys = ys
append (x :: xs) ys = x :: append xs ys

max_stars_repo_name: RossMeikleham/MSci-Project

max_issues_repo_name: RossMeikleham/MSci-Project

max_forks_repo_name: RossMeikleham/MSci-Project


text:
module SudokuSMT

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

puzzle :  Tensor [3, 3, 3, 3] Int
puzzle = toTensor
           [ [matrix00, matrix01, matrix02],
             [matrix10, matrix11, matrix12],
             [matrix20, matrix21, matrix22] ]
    where
      matrix00 : Vect 3 (Vect 3 Int)
      matrix00 = [ [5, 3, 0],
                   [6, 0, 0],
                   [0, 9, 8] ]
      matrix01 : Vect 3 (Vect 3 Int)
      matrix01 = [ [0, 7, 0],
                   [1, 9, 5],
                   [0, 0, 0] ]
      matrix02 : Vect 3 (Vect 3 Int)
      matrix02 = [ [0, 0, 0],
                   [0, 0, 0],
                   [0, 6, 0] ]
      matrix10 : Vect 3 (Vect 3 Int)
      matrix10 = [ [8, 0, 0],
                   [4, 0, 0],
                   [7, 0, 0] ]
      matrix11 : Vect 3 (Vect 3 Int)
      matrix11 = [ [0, 6, 0],
                   [8, 0, 3],
                   [0, 2, 0] ]
      matrix12 : Vect 3 (Vect 3 Int)
      matrix12 = [ [0, 0, 3],
                   [0, 0, 1],
                   [0, 0, 6] ]
      matrix20 : Vect 3 (Vect 3 Int)
      matrix20 = [ [0, 6, 0],
                   [0, 0, 0],
                   [0, 0, 0] ]
      matrix21 : Vect 3 (Vect 3 Int)
      matrix21 = [ [0, 0, 0],
                   [4, 1, 9],
                   [0, 8, 0] ]
      matrix22 : Vect 3 (Vect 3 Int)
      matrix22 = [ [2, 8, 0],
                   [0, 0, 5],
                   [0, 7, 9] ]

vars : Tensor [3, 3, 3, 3] String
vars = toTensor
        [ [ [ ["x_" ++ show i0 ++ "_" ++ show i1 ++ "_" ++ show i2 ++ "_" ++ show i3
             | i3 <- [0, 1, 2]]
             | i2 <- [0, 1, 2]]
             | i1 <- [0, 1, 2]]
             | i0 <- [0, 1, 2]]

cells : Tensor [3, 3, 3, 3] (Expr (NumT IntT)) -> Expr BoolT
cells ts with (toVect ts)
  cells ts | xssss = let xs = concat $ concat $ concat xssss in
                    and $ map (\x => (int 1) <= x && x <= (int 9)) xs

rows : Tensor [3, 3, 3, 3] (Expr (NumT IntT)) -> Expr BoolT
rows ts with (toVect ts)
  rows ts | xssss = let rs = concat $ map zipRows xssss in
                    and $ map distinct rs
  where
    zipRows : Vect 3 (Vect 3 (Vect 3 (Expr (NumT IntT)))) -> Vect 3 (Vect 9 (Expr (NumT IntT)))
    zipRows xsss = zipWith3 (\xs, ys, zs => xs ++ ys ++ zs) (index 0 xsss) (index 1 xsss) (index 2 xsss)

cols : Tensor [3, 3, 3, 3] (Expr (NumT IntT)) -> Expr BoolT
cols ts with (toVect ts)
  cols ts | xssss = let rs = concat $ map zipCols $ map (map transpose) $ transpose xssss in
                        and $ map distinct rs
  where
    zipCols : Vect 3 (Vect 3 (Vect 3 (Expr (NumT IntT)))) -> Vect 3 (Vect 9 (Expr (NumT IntT)))
    zipCols xsss = zipWith3 (\xs, ys, zs => xs ++ ys ++ zs) (index 0 xsss) (index 1 xsss) (index 2 xsss)

square : Tensor [3, 3, 3, 3] (Expr (NumT IntT)) -> Expr BoolT
square ts with (toVect ts)
  square ts | xssss = and $ map (\xss => distinct (concat xss)) $ concat xssss

instanceCheck : Tensor [3, 3, 3, 3] Int -> Tensor [3, 3, 3, 3] (Expr (NumT IntT)) -> Expr BoolT
instanceCheck insts vars with (toVect insts, toVect vars)
  instanceCheck insts vars | (insts', vars') = let insts'' = concat $ concat $ concat insts' in
                                               let vars'' = concat $ concat $ concat vars' in
                                               and $ zipWith (\inst, var => ite ((int inst) == (int 0)) (bool True) ((int inst) == var)) insts'' vars''

sudoku : Smt ()
sudoku = do vars <- declareVars vars (NumT IntT)
            assert $ cells vars
            assert $ rows vars
            assert $ cols vars
            assert $ square vars
            assert $ instanceCheck puzzle vars
            checkSat
            getModel
            end

max_stars_repo_name: vikfret/idris-snippets

max_issues_repo_name: vikfret/idris-snippets

max_forks_repo_name: vikfret/idris-snippets


text:
import Data.Primitives.Views
import ArithInputs

quiz : Stream Int -> (score : Nat) -> IO ()
quiz (num1 :: num2 :: nums) score
  = do putStrLn ("Score: " ++ show score)
       putStr (show num1 ++ " * " ++ show num2 ++ " ")
       answer <- getLine
       if (cast answer == num1 * num2)
       then do putStrLn "Correct!"
               quiz nums (score + 1)
       else do putStrLn ("Wrong, the answer is " ++ show (num1 * num2))
               quiz nums score

max_stars_repo_name: tekerson/type-driven-development

max_issues_repo_name: tekerson/type-driven-development

max_forks_repo_name: tekerson/type-driven-development


text:
module Transducers.Core

import Control.Monad.State

--------------------------------------------------------------------------------
-- Core (definition of steps, reducers and transducers)
--------------------------------------------------------------------------------

public export
data Status a = Done a | Continue a

export
unStatus : Status a -> a
unStatus (Done a) = a
unStatus (Continue a) = a

export
implementation Functor Status where
  map f (Done a) = Done (f a)
  map f (Continue a) = Continue (f a)

public export
StatelessStep : (acc, x: Type) -> Type
StatelessStep acc x = acc -> x -> acc

public export
Step : (state, acc, x: Type) -> Type
Step state acc x = acc -> x -> State state (Status acc)

public export
record Reducer st acc x where
  constructor MkReducer
  state : st
  runStep : Step st acc x
  complete : st -> acc -> acc

export
terminal : StatelessStep acc x -> Reducer () acc x
terminal fn = MkReducer () step (const id)
  where step acc x = pure $ Continue (fn acc x)

public export
Transducer : (acc, s1, s2, outer, inner: Type) -> Type
Transducer acc s1 s2 outer inner = Reducer s1 acc inner -> Reducer s2 acc outer

--------------------------------------------------------------------------------
-- Helpers to build stateless Reducers and Transducers
--------------------------------------------------------------------------------

export
statelessTransducer : (Step s acc b -> Step s acc a) -> Transducer acc s s a b
statelessTransducer stepTf next =
  MkReducer (state next) (stepTf (runStep next)) (complete next)

export
makeTransducer :
    s'
    -> (Step s acc b -> Step s (s', acc) a)
    -> (Step s acc b -> s' -> acc -> State s acc)
    -> Transducer acc s (s', s) a b
makeTransducer initialState stepTf onComplete next =
  MkReducer (initialState, state next) stepImpl completeImpl
  where
    completeImpl (s', s) acc =
      let acc = evalState (onComplete (runStep next) s' acc) s
      in complete next s acc
    stepImpl acc x = do
      (s1', s1) <- get
      let (result, s2) = runState (stepTf (runStep next) (s1', acc) x) s1
      case result of
        Done (s2', acc) => do
          put (s2', s2)
          pure (Done acc)
        Continue (s2', acc) => do
          put (s2', s2)
          pure (Continue acc)

export
statefulTransducer : s' -> (Step s acc b -> Step s (s', acc) a) -> Transducer acc s (s', s) a b
statefulTransducer initState stepTf = makeTransducer initState stepTf onComplete
  where
    onComplete next _ acc = pure acc

export
withState : s -> Status acc -> Status (s, acc)
withState s = map (\acc => (s, acc))

--------------------------------------------------------------------------------
-- Core (Reductions)
--------------------------------------------------------------------------------

export
runSteps : (Foldable t) => Step st acc x -> acc -> t x -> State st (Status acc)
runSteps step acc xs = foldr stepImpl (pure . id) xs (Continue acc)
  where
    stepImpl _ nextIteration (Done acc) = pure (Done acc)
    stepImpl x nextIteration (Continue acc) = step acc x >>= nextIteration

export
reduce : (Foldable t) => Reducer st acc x -> acc -> t x -> acc
reduce step acc =
  uncurry (complete step)
    . (\(acc, s) => (s, unStatus acc))
    . (flip runState (state step))
    . runSteps (runStep step) acc

export
transduce : (Foldable t) => Transducer acc () s b a -> (acc -> a -> acc) -> acc -> t b -> acc
transduce xf step = reduce (xf (terminal step))

max_stars_repo_name: QuentinDuval/IdrisReducers

max_issues_repo_name: QuentinDuval/IdrisReducers

max_forks_repo_name: QuentinDuval/IdrisReducers


text:
import Data.Vect

data CopK : Type where
  Nil : CopK
  (::) : (head : Type -> Type) -> (tail : CopK) -> CopK

data ElemK : (value : (Type -> Type)) -> CopK -> Type where
  Here : ElemK head (head :: tail)
  There : (later : ElemK x xs) -> ElemK x ( y :: xs)

foo : CopK
foo = List :: (Vect 3) :: Maybe :: Nil

x : ElemK Maybe Main.foo
x = There (There Here)

max_stars_repo_name: janschultecom/seo-router

max_issues_repo_name: janschultecom/seo-router

max_forks_repo_name: janschultecom/seo-router


text:
module Control.Kan

||| left kan extension
data Lan : (Type -> Type) -> Type -> Type where
  FMap : (x -> a) -> g x -> Lan g a

||| 'free' functor for any *->*
Functor (Lan f) where
  map func (FMap g y) = FMap (func . g) y

max_stars_repo_name: idris-industry/idris-free

max_issues_repo_name: idris-industry/idris-free

max_forks_repo_name: idris-industry/idris-free


text:
import Data.Vect

%default total

data GameState : Type where
    NotRunning : GameState
    Running : (guesses : Nat) -> (letters : Nat) -> GameState

letters : String -> List Char
letters = nub . map toUpper . unpack

data GuessResult = Correct | Incorrect

data GameCmd : (ty : Type) -> GameState -> (ty -> GameState) -> Type where
    NewGame : (word : String) ->
              GameCmd () NotRunning (const (Running 6 (length (letters word))))
    Won : GameCmd () (Running (S guesses) 0) (const NotRunning)
    Lost : GameCmd () (Running 0 (S guesses)) (const NotRunning)

    Guess : (c : Char) -> GameCmd GuessResult (Running (S guesses) (S letters))
        (\check =>
            case check of
                Correct => Running (S guesses) letters
                Incorrect => Running guesses (S letters))

    ShowState : GameCmd () state (const state)
    Message : String -> GameCmd () state (const state)
    ReadGuess : GameCmd Char state (const state)

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

namespace Loop
    data GameLoop : (ty : Type) -> GameState -> (ty -> GameState) -> Type where
        (>>=) : GameCmd a state1 state2Fn ->
                ((res : a) -> Inf (GameLoop b (state2Fn res) state3Fn)) ->
                GameLoop b state1 state3Fn
        Exit : GameLoop () NotRunning (const NotRunning)

gameLoop : GameLoop () (Running (S guesses) (S letters)) (const NotRunning)
gameLoop {guesses} {letters} =
    do
        ShowState
        g <- ReadGuess
        ok <- Guess g
        case ok of
            Correct =>
                case letters of
                    Z =>
                        do
                            Won
                            ShowState
                            Exit
                    (S k) =>
                        do
                            Message "Correct"
                            gameLoop
            Incorrect =>
                case guesses of
                    Z =>
                        do
                            Lost
                            ShowState
                            Exit
                    (S k) =>
                        do
                            Message "Incorrect"
                            gameLoop

hangman : GameLoop () NotRunning (const NotRunning)
hangman =
    do
        NewGame "testing"
        gameLoop

data Game : GameState -> Type where
    GameStart : Game NotRunning
    GameWon : (word : String) -> Game NotRunning
    GameLost : (word : String) -> Game NotRunning
    InProgress : (word : String) -> (guesses : Nat) ->
                (missing : Vect letters Char) ->
                Game (Running guesses letters)

Show (Game g) where
    show GameStart = "Starting"
    show (GameWon word) = "Game won: word was " ++ word
    show (GameLost word) = "Game lost: word was " ++ word
    show (InProgress word guesses missing) =
        "\n" ++ pack (map hideMissing (unpack word)) ++
        "\n" ++ show guesses ++ " guesses left"
        where
            hideMissing : Char -> Char
            hideMissing c = if c `elem` missing then '-' else c

data Fuel = Dry | More (Lazy Fuel)

data GameResult : (ty : Type) -> (ty -> GameState) -> Type where
    OK : (res : ty) -> Game (outStateFn res) -> GameResult ty outStateFn
    OutOfFuel : GameResult ty outStateFn

ok : (res : ty) -> Game $ outStateFn res ->
    IO $ GameResult ty outStateFn
ok res st = pure $ OK res st

runCmd : Fuel -> Game inState -> GameCmd ty inState outStateFn ->
        IO (GameResult ty outStateFn)
runCmd fuel state (NewGame word) = ok () (InProgress (toUpper word) _ (fromList $ letters word))
runCmd fuel (InProgress word _ missing) Won = ok () (GameWon word)
runCmd fuel (InProgress word _ missing) Lost = ok () (GameLost word)
runCmd fuel (InProgress word _ missing) (Guess c) =
    case isElem c missing of
        Yes prf => ok Correct (InProgress word _ (dropElem missing prf))
        No contra => ok Incorrect (InProgress word _ missing)
runCmd fuel state ShowState =
    do
        printLn state
        ok () state
runCmd fuel state (Message msg) =
    do
        putStrLn msg
        ok () state
runCmd (More fuel) state ReadGuess =
    do
        putStr "Guess: "
        input <- getLine
        case unpack input of
            [x] =>
                if isAlpha x
                    then ok (toUpper x) state
                    else
                        do
                            putStrLn "Invalid input"
                            runCmd fuel state ReadGuess
            _ =>
                do
                    putStrLn "Invalid input"
                    runCmd fuel state ReadGuess
runCmd fuel state (Pure res) = ok res state
runCmd fuel state (cmd >>= next) =
    do
        OK cmdRes newState <- runCmd fuel state cmd
            | OutOfFuel => pure OutOfFuel
        runCmd fuel newState (next cmdRes)
runCmd Dry _ _ = pure OutOfFuel

run : Fuel -> Game inState -> GameLoop ty inState outStateFn ->
    IO (GameResult ty outStateFn)
run Dry _ _ = pure OutOfFuel
run (More fuel) state (cmd >>= next) =
    do
        OK cmdRes newState <- runCmd fuel state cmd
            | OutOfFuel => pure OutOfFuel
        run fuel newState (next cmdRes)
run (More fuel) state Exit = ok () state

%default partial

forever : Fuel
forever = More forever

main : IO ()
main =
    do
        run forever GameStart hangman
        pure ()


text:
module Inigo.Package.PackageDeps

import Data.List
import Data.Maybe
import Extra.Debug as Debug
import Extra.Either
import Extra.List
import Extra.Op
import Extra.String
import Inigo.Package.ParseHelpers
import Inigo.Package.Package
import SemVar
import Toml
import Toml.Data

||| Information about a package in the index
public export
record PackageDep where
  constructor MkPackageDep
  deps : List (List String, Requirement)
  dev : List (List String, Requirement)

public export
PackageDeps : Type
PackageDeps = List (Version, PackageDep)

public export
PackageDepTree : Type
PackageDepTree = List (List String, PackageDeps)

public export
Show PackageDep where
  show (MkPackageDep deps devDeps) =
    "MkPackageDep{deps=" ++ (show deps) ++ ",dev=" ++ (show devDeps) ++ "}"

public export
Eq PackageDep where
  (MkPackageDep deps0 dev0) == (MkPackageDep deps1 dev1) =
    deps0 == deps1 && dev0 == dev1

||| Helper function to group Toml values by the first part of each key
groupByHead : List (List String, Value) -> List (String, List (List String, Value))
groupByHead toml =
  let
    sorted = sortBy (\(k0, _), (k1, _) => compare k0 k1) toml
    results = foldl accumulate [] sorted
  in
    reverse $ map (\(head, vals) => (head, reverse vals)) results
  where
    accumulate : List (String, List (List String, Value)) -> (List String, Value) -> List (String, List (List String, Value))
    accumulate acc ([], _) = acc -- Skip empty keys
    accumulate [] (hd :: rest, val) = [(hd, [(rest, val)])]
    accumulate ((accKey, accValues) :: accRest) (hd :: rest, val) =
      if accKey == hd then
        (accKey, (rest, val) :: accValues) :: accRest
      else
        (hd, [(rest, val)]) :: (accKey, accValues) :: accRest

parsePackageDepsToml : Toml -> Either String PackageDeps
parsePackageDepsToml toml =
  map reverse $ collapse $ map parsePackageDep (groupByHead toml)
  where
    parsePackageDepToml : Toml -> Either String PackageDep
    parsePackageDepToml toml =
      do
        deps <- parseDeps ["deps"] toml
        devDeps <- parseDeps ["dev"] toml
        pure $ MkPackageDep deps devDeps

    parsePackageDep : (String, List (List String, Value)) -> Either String (Version, PackageDep)
    parsePackageDep (versionStr, depToml) =
      do
        version <- expect ("Invalid version: " ++ versionStr) (parseVersion versionStr)
        packageDep <- parsePackageDepToml depToml
        pure (version, packageDep)

export
parsePackageDeps : String -> Either String PackageDeps
parsePackageDeps pkgDepsToml =
  do
    toml <- expect "Failed to parse PackageDeps Toml" $ parseToml pkgDepsToml
    parsePackageDepsToml toml

export
parsePackageDepTree : String -> Either String PackageDepTree
parsePackageDepTree pkgDepsToml =
  do
    toml <- expect "Failed to parse PackageDeps Toml" $ parseToml pkgDepsToml
    foldl accumulate (Right []) (groupByHead toml)
  where
    accumulate : Either String PackageDepTree -> (String, Toml) -> Either String PackageDepTree
    accumulate (Left err) _ = Left err -- persist error
    accumulate (Right acc) (pkg, toml) =
      map (\packageDep => (split '.' pkg, packageDep) :: acc) (parsePackageDepsToml toml)

export
toToml : PackageDeps -> Toml
toToml =
  concat . map (\(version, (MkPackageDep deps dev)) =>
    showAllDeps version deps dev
    )
  where
    showDep : List String -> (List String, Requirement) -> (List String, Value)
    showDep keyHead (pkg, req) = (keyHead ++ pkg, Str $ show req)

    showDeps : Version -> String -> List (List String, Requirement) -> List (List String, Value)
    showDeps version key = map (showDep [show version, key])

    showAllDeps : Version -> List (List String, Requirement) -> List (List String, Requirement) -> List (List String, Value)
    showAllDeps version deps dev =
      (showDeps version "deps" deps) ++
      (showDeps version "dev" dev)

||| Encode a package, for instance, after adding a new dep
export
encodePackageDeps : PackageDeps -> String
encodePackageDeps = encode . toToml

export
fromPackage : Package -> PackageDep
fromPackage pkg =
  MkPackageDep (deps pkg) (devDeps pkg)

export
updatePackageDep : PackageDeps -> Package -> PackageDeps
updatePackageDep pkgDeps pkg =
  let
    pkgVersion = version pkg
    pkgDep = (pkgVersion, fromPackage pkg)
  in
    case break ((== pkgVersion) . fst) pkgDeps of
      (r, []) =>
        r ++ [pkgDep]
      (r, _ :: rest) =>
        r ++ (pkgDep :: rest)

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
-- ----------------------------------------------------------- [ DataTypes.idr ]
-- Module      : Exercises.DataTypes
-- Description : Solutions to the Chapter 4 exercises in Edwin Brady's
--               book, "Type-Driven Development with Idris."
-- --------------------------------------------------------------------- [ EOH ]
module Exercises.DataTypes

import public Chapter.DataTypes
import public Data.Vect

%access export

on : (b -> b -> c) -> (a -> b) -> a -> a -> c
on g f = \x,y => f x `g` f y

onIdentity : -- ((*) : b -> b -> c) ->
             ((*) `on` Basics.id) x y = (*) x y
onIdentity = Refl

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

flipOn : (a -> b) -> (b -> b -> c) -> a -> a -> c
flipOn = flip on

onFlip : -- (f : a -> b) -> (g : b -> c) ->
         (flipOn f . flipOn g) h x y = (flipOn (g . f)) h x y
onFlip = Refl

-- --------------------------------------------------------- [ 4.1.5 Exercises ]

||| Insert every element of a list into a binary search tree.
|||
||| ```idris example
||| listToTree [1,4,3,5,2]
||| ```
listToTree : Ord a => List a -> Tree a
listToTree = foldr insert Empty

||| Flatten a tree into a list using *inorder* traversal.
|||
||| ```idris example
||| treeToList (listToTree [4,1,8,7,2,3,9,5,6])
||| ```
treeToList : Tree a -> List a
treeToList Empty = []
treeToList (Node l x r) = treeToList l ++ [x] ++ treeToList r

||| An integer arithmetic expression.
public export
data Expr = ||| A single integer.
            Val Int
          | ||| Addition of an expression to an expression.
            Add Expr Expr
          | ||| Subtraction of an expression from an expresison.
            Sub Expr Expr
          | ||| Multiplication of an expression with an expression.
            Mult Expr Expr

||| Evaluate an integer arithmetic expression.
|||
||| ```idris example
||| evaluate (Mult (Val 10) (Add (Val 6) (Val 3)))
||| ```
evaluate : Expr -> Int
evaluate (Val x)    = x
evaluate (Add x y)  = evaluate x + evaluate y
evaluate (Sub x y)  = evaluate x - evaluate y
evaluate (Mult x y) = evaluate x * evaluate y

||| Return the larger of two inputs, or `Nothing` if both inputs are `Nothing`.
|||
||| ```idris example
||| maxMaybe (Just 4) (Just 5)
||| ```
||| ```idris example
||| maxMaybe (Just 4) Nothing
||| ```
maxMaybe : Ord a => Maybe a -> Maybe a -> Maybe a
maxMaybe mx my = (max <$> mx <*> my) <|> mx <|> my

-- --------------------------------------------------------- [ 4.2.4 Exercises ]

public export
data PowerSource = Petrol
                 | Electricity
                 | Pedal

public export
data Vehicle : PowerSource -> Type where
     Unicycle : Vehicle Pedal
     Bicycle : Vehicle Pedal
     GalacticPizzaCar : Vehicle Electricity
     Motorcycle : (fuel : Nat) -> Vehicle Petrol
     Car : (fuel : Nat) -> Vehicle Petrol
     Bus : (fuel : Nat) -> Vehicle Petrol

||| Return the number of wheels on a vehicle.
|||
||| ```idris example
||| wheels GalacticPizzaCar
||| ```
wheels : Vehicle power -> Nat
wheels Unicycle         = 1
wheels Bicycle          = 2
wheels GalacticPizzaCar = 3
wheels (Motorcycle _)   = 2
wheels (Car _)          = 4
wheels (Bus _)          = 4

||| Refuel a petrol-powered vehicle.
|||
||| ```idris example
||| refuel (Car 0)
||| ```
refuel : Vehicle Petrol -> Vehicle Petrol
refuel (Motorcycle _) = Motorcycle  50
refuel (Car _)        = Car 100
refuel (Bus _)        = Bus 200
-- NOTE: refuel Unicycle impossible

||| Get the first n elements of a Vect.
|||
||| ```idris example
||| vectTake 3 [1,2,3,4,5,6,7]
||| ```
|||
||| @ n the number of elements to take
vectTake : (n : Nat) -> Vect (n + m) a -> Vect n a
vectTake Z _             = []
vectTake (S k) (x :: xs) = x :: vectTake k xs

||| Return `Just` the sum of the entries at position `pos` in each of the
||| inputs, if `pos` is within bounds, or `Nothing` otherwise.
|||
||| ```idris example
||| sumEntries 2 [1,2,3,4] [5,6,7,8]
||| ```
||| ```idris example
||| sumEntries 4 [1,2,3,4] [5,6,7,8]
||| ```
|||
||| @ pos a possibly out-of-bounds index into the input vectors
sumEntries : Num a => (pos : Integer) -> Vect n a -> Vect n a -> Maybe a
sumEntries {n} pos xs ys with (integerToFin pos n)
  | m = pure $ ((+) `on` index !m) xs ys

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

max_stars_repo_name: yurrriq/tdd-with-idris

max_issues_repo_name: yurrriq/tdd-with-idris

max_forks_repo_name: yurrriq/tdd-with-idris


text:
main : IO ()
main = putStrLn "Hello sinter world!"


text:
-- | Some simple arithmetic exercises.
module Koans.Arithmetic

-- | There were 32 B/W Episodes of Ivor the Engine, and 72 episodes
-- were produced altogether. How many colour episodes were produced?
add : Bool
add = ?colour + 32 == 72

-- | B/W Episodes of Ivor the Engine were ten minutes long. If you
-- were to watch all the episodes in one sitting how many minutes
-- would it take?
multiply : Bool
multiply = ?b_w_duration == 10 * 32

-- | In what year did the Colourised version of Ivor the Engine first air?
subtract : Bool
subtract = 1977 - ?inception == 3

-- | 26 B/W episodes of Ivor the Engine were discovered in a Pig shed
-- in 2010. There were two seasons. How many episodes per season were
-- there?
division : Bool
division = 26 / ?pigshed == 2
-- this won’t work because integer division is not defined

-- | There were 32 B/W episodes of ten minutes each, and 40 colour
-- episodes of five minutes each. How many minutes of Ivor the Engine
-- exist?
parentheses : Int
parentheses = ?answer

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

max_stars_repo_name: isomorphisms/idris-koans

max_issues_repo_name: isomorphisms/idris-koans

max_forks_repo_name: isomorphisms/idris-koans


text:
module Gen.Eval

import public Control.Monad.Identity
import public Control.Monad.Reader

-- 8YYYY 0   0  o8o  0    0   0  o8o  YY8YY _YYY_ 8YYYo
-- 8___  0   0 8   8 0    0   0 8   8   0   0   0 8___P
-- 8"""  "o o" 8YYY8 0    0   0 8YYY8   0   0   0 8""Yo
-- 8oooo  "8"  0   0 8ooo "ooo" 0   0   0   "ooo" 0   0

public export
Evaluator : Type -> Type -> Type
Evaluator e = ReaderT e (Either String)

public export
environment : Evaluator e e
environment = ask

public export
interface Eval e a where
	eval : a -> Evaluator e a

export
unless : Applicative f => Bool -> Lazy (f ()) -> f ()
unless False f = Force f
unless True f = pure ()

export
replicateM        : (Applicative m) => Nat -> m a -> m (List a)
replicateM cnt0 f = loop cnt0
where
	loop : Nat -> m (List a)
	loop Z     = pure []
	loop (S n) = liftA2 (::) f (loop n)

export
zipWithM          : (Applicative m) => (a -> b -> m c) -> List a -> List b -> m (List c)
zipWithM f xs ys  =  sequence (zipWith f xs ys)

export
groupBy : (a -> a -> Bool) -> List a -> List (List a)
groupBy _  [] = []
groupBy eq (x::xs) = do
	let (ys, zs) = span (eq x) xs
	(x::ys) :: groupBy eq zs

max_stars_repo_name: totalscript/totalscript

max_issues_repo_name: totalscript/totalscript

max_forks_repo_name: totalscript/totalscript


text:
--
-- Primitive casts: Specification
--
-- a. Unsigned integers
--
--    Unsigned integers with a precision of x bit have a valid
--    range of [0,2^x - 1]. When casting from another integral type of value y,
--    the value is checked for being in bounds, and if it is not, the
--    unsigned remainder modulo 2^x of y is returned.
--
--    When casting from a `Double`, the value is first truncated towards 0,
--    before applying the inbounds check and (if necessary) calculating
--    the unsigned remainder modulo 2^x.
--
--    When casting from a `String`, the value is first converted to a floating
--    point number by the backend and then truncated as described above.
--
--    Example: For `Bits8` the valid range is [0,255]. Below are some
--             example casts.
--
--               cast {from = Integer} {to = Bits8} 12   = 12
--               cast {from = Integer} {to = Bits8} 256  = 0
--               cast {from = Integer} {to = Bits8} 259  = 3
--               cast {from = Integer} {to = Bits8} (-2) = 254
--               cast {from = Double} {to = Bits8} (-12.001) = 244
--               cast {from = Double} {to = Bits8} ("-12.001") = 244
--
-- b. Signed integers
--
--    Signed integers with a precision of x bit have a valid
--    range of [-2^(x-1),2^(x-1) - 1]. When casting from another
--    integral type of value y, the unsigned remainder module 2^x
--    is calculated. If the result is >= 2^(x-1), 2^x is subtracted
--    from the result. This is the same behavior as for instance in Haskell.
--
--    When casting from a `Double`, the value is first truncated towards 0,
--    before applying the inbounds check and (if necessary) truncating
--    the value.
--
--    When casting from a `String`, the value is first converted to a floating
--    point number by the backend and then truncated as described above.
--
--    Example: For `Int8` the valid range is [-128,127]. Below are some
--             example casts.
--
--               cast {from = Integer} {to = Int8} 12   = 12
--               cast {from = Integer} {to = Int8} 256  = 0
--               cast {from = Integer} {to = Int8} 259  = 4
--               cast {from = Integer} {to = Int8} (-128) = (-128)
--               cast {from = Integer} {to = Int8} (-129) = 127
--               cast {from = Double}  {to = Int8} (-12.001) = (-12)
--               cast {from = Double}  {to = Int8} ("-12.001") = (-12)
--
-- c. Characters
--
--    Casts from all integral types to `Char` are supported. Note however,
--    that only casts in the non-surrogate range are supported, that is
--    values in the ranges [0,0xd7ff] and [0xe000,0x10ffff], or, in decimal
--    notation, [0,55295] and [57344,1114111].
--
--    All casts from integer types to `Char` are therefore submitted to a
--    bounds check, and, in case the value is out of bounds, are converted to `'\0'`.
--
--
-- Test all casts from and to integral types.
-- The `Cast` implementations in here should go to `Prelude`, once
-- a new minor version of the compiler is released.
--
-- These tests verify also that the full range of integer literals
-- is supported for every integral type.
--
-- Nothing fancy is being done here:
-- All test cases have been hand-written.

import Data.List

--------------------------------------------------------------------------------
--          Int8
--------------------------------------------------------------------------------

Show Int8 where
  show = prim__cast_Int8String

public export
Eq Int8 where
  x == y = intToBool (prim__eq_Int8 x y)

Num Int8 where
  (+) = prim__add_Int8
  (*) = prim__mul_Int8
  fromInteger = prim__cast_IntegerInt8

Neg Int8 where
  (-)    = prim__sub_Int8
  negate = prim__sub_Int8 0

Cast Int8 Bits8 where
  cast = prim__cast_Int8Bits8

Cast Int8 Bits16 where
  cast = prim__cast_Int8Bits16

Cast Int8 Bits32 where
  cast = prim__cast_Int8Bits32

Cast Int8 Bits64 where
  cast = prim__cast_Int8Bits64

Cast Int8 Int16 where
  cast = prim__cast_Int8Int16

Cast Int8 Int32 where
  cast = prim__cast_Int8Int32

Cast Int8 Int64 where
  cast = prim__cast_Int8Int64

Cast Int8 Int where
  cast = prim__cast_Int8Int

Cast Int8 Integer where
  cast = prim__cast_Int8Integer

Cast Int8 String where
  cast = prim__cast_Int8String

Cast Int8 Char where
  cast = prim__cast_Int8Char

Cast Int8 Double where
  cast = prim__cast_Int8Double

--------------------------------------------------------------------------------
--          Int16
--------------------------------------------------------------------------------

public export
Eq Int16 where
  x == y = intToBool (prim__eq_Int16 x y)

Show Int16 where
  show = prim__cast_Int16String

Num Int16 where
  (+) = prim__add_Int16
  (*) = prim__mul_Int16
  fromInteger = prim__cast_IntegerInt16

Neg Int16 where
  (-)    = prim__sub_Int16
  negate = prim__sub_Int16 0

Cast Int16 Bits8 where
  cast = prim__cast_Int16Bits8

Cast Int16 Bits16 where
  cast = prim__cast_Int16Bits16

Cast Int16 Bits32 where
  cast = prim__cast_Int16Bits32

Cast Int16 Bits64 where
  cast = prim__cast_Int16Bits64

Cast Int16 Int8 where
  cast = prim__cast_Int16Int8

Cast Int16 Int32 where
  cast = prim__cast_Int16Int32

Cast Int16 Int64 where
  cast = prim__cast_Int16Int64

Cast Int16 Int where
  cast = prim__cast_Int16Int

Cast Int16 Integer where
  cast = prim__cast_Int16Integer

Cast Int16 String where
  cast = prim__cast_Int16String

Cast Int16 Char where
  cast = prim__cast_Int16Char

Cast Int16 Double where
  cast = prim__cast_Int16Double

--------------------------------------------------------------------------------
--          Int32
--------------------------------------------------------------------------------

Show Int32 where
  show = prim__cast_Int32String

public export
Eq Int32 where
  x == y = intToBool (prim__eq_Int32 x y)

Num Int32 where
  (+) = prim__add_Int32
  (*) = prim__mul_Int32
  fromInteger = prim__cast_IntegerInt32

Neg Int32 where
  (-)    = prim__sub_Int32
  negate = prim__sub_Int32 0

Cast Int32 Bits8 where
  cast = prim__cast_Int32Bits8

Cast Int32 Bits16 where
  cast = prim__cast_Int32Bits16

Cast Int32 Bits32 where
  cast = prim__cast_Int32Bits32

Cast Int32 Bits64 where
  cast = prim__cast_Int32Bits64

Cast Int32 Int8 where
  cast = prim__cast_Int32Int8

Cast Int32 Int16 where
  cast = prim__cast_Int32Int16

Cast Int32 Int64 where
  cast = prim__cast_Int32Int64

Cast Int32 Int where
  cast = prim__cast_Int32Int

Cast Int32 Integer where
  cast = prim__cast_Int32Integer

Cast Int32 String where
  cast = prim__cast_Int32String

Cast Int32 Char where
  cast = prim__cast_Int32Char

Cast Int32 Double where
  cast = prim__cast_Int32Double

--------------------------------------------------------------------------------
--          Int64
--------------------------------------------------------------------------------

Show Int64 where
  show = prim__cast_Int64String

public export
Eq Int64 where
  x == y = intToBool (prim__eq_Int64 x y)

Num Int64 where
  (+) = prim__add_Int64
  (*) = prim__mul_Int64
  fromInteger = prim__cast_IntegerInt64

Neg Int64 where
  (-)    = prim__sub_Int64
  negate = prim__sub_Int64 0

Cast Int64 Bits8 where
  cast = prim__cast_Int64Bits8

Cast Int64 Bits16 where
  cast = prim__cast_Int64Bits16

Cast Int64 Bits32 where
  cast = prim__cast_Int64Bits32

Cast Int64 Bits64 where
  cast = prim__cast_Int64Bits64

Cast Int64 Int8 where
  cast = prim__cast_Int64Int8

Cast Int64 Int16 where
  cast = prim__cast_Int64Int16

Cast Int64 Int32 where
  cast = prim__cast_Int64Int32

Cast Int64 Int where
  cast = prim__cast_Int64Int

Cast Int64 Integer where
  cast = prim__cast_Int64Integer

Cast Int64 String where
  cast = prim__cast_Int64String

Cast Int64 Char where
  cast = prim__cast_Int64Char

Cast Int64 Double where
  cast = prim__cast_Int64Double

--------------------------------------------------------------------------------
--          Int
--------------------------------------------------------------------------------

Cast Int Int8 where
  cast = prim__cast_IntInt8

Cast Int Int16 where
  cast = prim__cast_IntInt16

Cast Int Int32 where
  cast = prim__cast_IntInt32

Cast Int Int64 where
  cast = prim__cast_IntInt64

--------------------------------------------------------------------------------
--          Integer
--------------------------------------------------------------------------------

Cast Integer Int8 where
  cast = prim__cast_IntegerInt8

Cast Integer Int16 where
  cast = prim__cast_IntegerInt16

Cast Integer Int32 where
  cast = prim__cast_IntegerInt32

Cast Integer Int64 where
  cast = prim__cast_IntegerInt64

Cast Integer Char where
  cast = prim__cast_IntegerChar

--------------------------------------------------------------------------------
--          Bits8
--------------------------------------------------------------------------------

Cast Bits8 Int8 where
  cast = prim__cast_Bits8Int8

Cast Bits8 Int16 where
  cast = prim__cast_Bits8Int16

Cast Bits8 Int32 where
  cast = prim__cast_Bits8Int32

Cast Bits8 Int64 where
  cast = prim__cast_Bits8Int64

Cast Bits8 String where
  cast = prim__cast_Bits8String

Cast Bits8 Char where
  cast = prim__cast_Bits8Char

Cast Bits8 Double where
  cast = prim__cast_Bits8Double

--------------------------------------------------------------------------------
--          Bits16
--------------------------------------------------------------------------------

Cast Bits16 Int8 where
  cast = prim__cast_Bits16Int8

Cast Bits16 Int16 where
  cast = prim__cast_Bits16Int16

Cast Bits16 Int32 where
  cast = prim__cast_Bits16Int32

Cast Bits16 Int64 where
  cast = prim__cast_Bits16Int64

Cast Bits16 String where
  cast = prim__cast_Bits16String

Cast Bits16 Char where
  cast = prim__cast_Bits16Char

Cast Bits16 Double where
  cast = prim__cast_Bits16Double

--------------------------------------------------------------------------------
--          Bits32
--------------------------------------------------------------------------------

Cast Bits32 Int8 where
  cast = prim__cast_Bits32Int8

Cast Bits32 Int16 where
  cast = prim__cast_Bits32Int16

Cast Bits32 Int32 where
  cast = prim__cast_Bits32Int32

Cast Bits32 Int64 where
  cast = prim__cast_Bits32Int64

Cast Bits32 String where
  cast = prim__cast_Bits32String

Cast Bits32 Char where
  cast = prim__cast_Bits32Char

Cast Bits32 Double where
  cast = prim__cast_Bits32Double

--------------------------------------------------------------------------------
--          Bits64
--------------------------------------------------------------------------------

Cast Bits64 Int8 where
  cast = prim__cast_Bits64Int8

Cast Bits64 Int16 where
  cast = prim__cast_Bits64Int16

Cast Bits64 Int32 where
  cast = prim__cast_Bits64Int32

Cast Bits64 Int64 where
  cast = prim__cast_Bits64Int64

Cast Bits64 String where
  cast = prim__cast_Bits64String

Cast Bits64 Char where
  cast = prim__cast_Bits64Char

Cast Bits64 Double where
  cast = prim__cast_Bits64Double

--------------------------------------------------------------------------------
--          String
--------------------------------------------------------------------------------

Cast String Bits8 where
  cast = prim__cast_StringBits8

Cast String Bits16 where
  cast = prim__cast_StringBits16

Cast String Bits32 where
  cast = prim__cast_StringBits32

Cast String Bits64 where
  cast = prim__cast_StringBits64

Cast String Int8 where
  cast = prim__cast_StringInt8

Cast String Int16 where
  cast = prim__cast_StringInt16

Cast String Int32 where
  cast = prim__cast_StringInt32

Cast String Int64 where
  cast = prim__cast_StringInt64

--------------------------------------------------------------------------------
--          Double
--------------------------------------------------------------------------------

Cast Double Bits8 where
  cast = prim__cast_DoubleBits8

Cast Double Bits16 where
  cast = prim__cast_DoubleBits16

Cast Double Bits32 where
  cast = prim__cast_DoubleBits32

Cast Double Bits64 where
  cast = prim__cast_DoubleBits64

Cast Double Int8 where
  cast = prim__cast_DoubleInt8

Cast Double Int16 where
  cast = prim__cast_DoubleInt16

Cast Double Int32 where
  cast = prim__cast_DoubleInt32

Cast Double Int64 where
  cast = prim__cast_DoubleInt64

--------------------------------------------------------------------------------
--          Tests
--------------------------------------------------------------------------------

showTpe : Type -> String
showTpe Bits16  = "Bits16"
showTpe Bits32  = "Bits32"
showTpe Bits64  = "Bits64"
showTpe Bits8   = "Bits8"
showTpe Char    = "Char"
showTpe Double  = "Double"
showTpe Int     = "Int"
showTpe Int16   = "Int16"
showTpe Int32   = "Int32"
showTpe Int64   = "Int64"
showTpe Int8    = "Int8"
showTpe Integer = "Integer"
showTpe String  = "String"
showTpe _       = "unknown type"

testCasts : (a: Type) -> (b : Type) -> (Cast a b, Show a, Show b, Eq b) =>
            List (a,b) -> List String
testCasts a b = mapMaybe doTest
  where doTest : (a,b) -> Maybe String
        doTest (x,y) =
          let y2 = cast {to = b} x
           in if y == y2 then Nothing
              else Just $  #"Invalid cast from \#{showTpe a} to \#{showTpe b}: "#
                        ++ #"expected \#{show y} but got \#{show y2} when casting from \#{show x}"#

maxBits8 : Bits8
maxBits8 = 0xff

maxBits16 : Bits16
maxBits16 = 0xffff

maxBits32 : Bits32
maxBits32 = 0xffffffff

maxBits64 : Bits64
maxBits64 = 0xffffffffffffffff

results : List String
results =  testCasts Int8 Int16   [(-129,127),(-128,-128),(0,0),(127,127),(128,-128)]
        ++ testCasts Int8 Int32   [(-129,127),(-128,-128),(0,0),(127,127),(128,-128)]
        ++ testCasts Int8 Int64   [(-129,127),(-128,-128),(0,0),(127,127),(128,-128)]
        ++ testCasts Int8 Int     [(-129,127),(-128,-128),(0,0),(127,127),(128,-128)]
        ++ testCasts Int8 Double  [(-129,127),(-128,-128),(0,0),(127,127),(128,-128)]
        ++ testCasts Int8 String  [(-129,"127"),(-128,"-128"),(0,"0"),(127,"127"),(128,"-128")]
        ++ testCasts Int8 Integer [(-129,127),(-128,-128),(0,0),(127,127),(128,-128)]
        ++ testCasts Int8 Bits8   [(-129,127),(0,0),(127,127),(128,-128)]
        ++ testCasts Int8 Bits16  [(-129,127),(0,0),(127,127),(128,-128)]
        ++ testCasts Int8 Bits32  [(-129,127),(0,0),(127,127),(128,-128)]
        ++ testCasts Int8 Bits64  [(-129,127),(0,0),(127,127),(128,-128)]

        ++ testCasts Int16 Int8    [(-32769,32767),(-32768,0),(0,0),(32767,-1),(32768,0)]
        ++ testCasts Int16 Int32   [(-32769,32767),(-32768,-32768),(0,0),(32767,32767),(32768,-32768)]
        ++ testCasts Int16 Int64   [(-32769,32767),(-32768,-32768),(0,0),(32767,32767),(32768,-32768)]
        ++ testCasts Int16 Int     [(-32769,32767),(-32768,-32768),(0,0),(32767,32767),(32768,-32768)]
        ++ testCasts Int16 Double  [(-32769,32767),(-32768,-32768),(0,0),(32767,32767),(32768,-32768)]
        ++ testCasts Int16 String  [(-32769,"32767"),(-32768,"-32768"),(0,"0"),(32767,"32767"),(32768,"-32768")]
        ++ testCasts Int16 Integer [(-32769,32767),(-32768,-32768),(0,0),(32767,32767),(32768,-32768)]
        ++ testCasts Int16 Bits8   [(-32769,32767),(0,0),(32767,32767),(32768,-32768)]
        ++ testCasts Int16 Bits16  [(-32769,32767),(0,0),(32767,32767),(32768,-32768)]
        ++ testCasts Int16 Bits32  [(-32769,32767),(0,0),(32767,32767),(32768,-32768)]
        ++ testCasts Int16 Bits64  [(-32769,32767),(0,0),(32767,32767),(32768,-32768)]

        ++ testCasts Int32 Int8    [(-2147483649,2147483647),(-2147483648,0),(0,0),(2147483647,-1),(2147483648,0)]
        ++ testCasts Int32 Int16   [(-2147483649,2147483647),(-2147483648,0),(0,0),(2147483647,-1),(2147483648,0)]
        ++ testCasts Int32 Int64   [(-2147483649,2147483647),(-2147483648,-2147483648),(0,0),(2147483647,2147483647),(2147483648,-2147483648)]
        ++ testCasts Int32 Int     [(-2147483649,2147483647),(-2147483648,-2147483648),(0,0),(2147483647,2147483647),(2147483648,-2147483648)]
        ++ testCasts Int32 Double  [(-2147483649,2147483647),(-2147483648,-2147483648),(0,0),(2147483647,2147483647),(2147483648,-2147483648)]
        ++ testCasts Int32 String  [(-2147483649,"2147483647"),(-2147483648,"-2147483648"),(0,"0"),(2147483647,"2147483647"),(2147483648,"-2147483648")]
        ++ testCasts Int32 Integer [(-2147483649,2147483647),(-2147483648,-2147483648),(0,0),(2147483647,2147483647),(2147483648,-2147483648)]
        ++ testCasts Int32 Bits8   [(-2147483649,2147483647),(0,0),(2147483647,2147483647),(2147483648,-2147483648)]
        ++ testCasts Int32 Bits16  [(-2147483649,2147483647),(0,0),(2147483647,2147483647),(2147483648,-2147483648)]
        ++ testCasts Int32 Bits32  [(-2147483649,2147483647),(0,0),(2147483647,2147483647),(2147483648,-2147483648)]
        ++ testCasts Int32 Bits64  [(-2147483649,2147483647),(0,0),(2147483647,2147483647),(2147483648,-2147483648)]

        ++ testCasts Int64 Int8    [(-9223372036854775809,9223372036854775807),(-9223372036854775808,0),(0,0),(9223372036854775807,-1),(9223372036854775808,0)]
        ++ testCasts Int64 Int16   [(-9223372036854775809,9223372036854775807),(-9223372036854775808,0),(0,0),(9223372036854775807,-1),(9223372036854775808,0)]
        ++ testCasts Int64 Int32   [(-9223372036854775809,9223372036854775807),(-9223372036854775808,0),(0,0),(9223372036854775807,-1),(9223372036854775808,0)]
        ++ testCasts Int64 Int     [(-9223372036854775809,9223372036854775807),(-9223372036854775808,-9223372036854775808),(0,0),(9223372036854775807,9223372036854775807),(9223372036854775808,-9223372036854775808)]
        ++ testCasts Int64 Double  [(-9223372036854775809,9223372036854775807),(-9223372036854775808,-9223372036854775808),(0,0),(9223372036854775807,9223372036854775807),(9223372036854775808,-9223372036854775808)]
        ++ testCasts Int64 String  [(-9223372036854775809,"9223372036854775807"),(-9223372036854775808,"-9223372036854775808"),(0,"0"),(9223372036854775807,"9223372036854775807"),(9223372036854775808,"-9223372036854775808")]
        ++ testCasts Int64 Integer [(-9223372036854775809,9223372036854775807),(-9223372036854775808,-9223372036854775808),(0,0),(9223372036854775807,9223372036854775807),(9223372036854775808,-9223372036854775808)]
        ++ testCasts Int64 Bits8   [(-9223372036854775809,255),(0,0),(9223372036854775807,0xff),(9223372036854775808,0)]
        ++ testCasts Int64 Bits16  [(-9223372036854775809,65535),(0,0),(9223372036854775807,0xffff),(9223372036854775808,0)]
        ++ testCasts Int64 Bits32  [(-9223372036854775809,4294967295),(0,0),(9223372036854775807,0xffffffff),(9223372036854775808,0)]
        ++ testCasts Int64 Bits64  [(-9223372036854775809,9223372036854775807),(0,0),(9223372036854775807,9223372036854775807),(9223372036854775808,-9223372036854775808)]

        ++ testCasts Int Int8    [(-9223372036854775809,9223372036854775807),(-9223372036854775808,0),(0,0),(9223372036854775807,-1),(9223372036854775808,0)]
        ++ testCasts Int Int16   [(-9223372036854775809,9223372036854775807),(-9223372036854775808,0),(0,0),(9223372036854775807,-1),(9223372036854775808,0)]
        ++ testCasts Int Int32   [(-9223372036854775809,9223372036854775807),(-9223372036854775808,0),(0,0),(9223372036854775807,-1),(9223372036854775808,0)]
        ++ testCasts Int Int64   [(-9223372036854775809,9223372036854775807),(-9223372036854775808,-9223372036854775808),(0,0),(9223372036854775807,9223372036854775807),(9223372036854775808,-9223372036854775808)]
        ++ testCasts Int Double  [(-9223372036854775809,9223372036854775807),(-9223372036854775808,-9223372036854775808),(0,0),(9223372036854775807,9223372036854775807),(9223372036854775808,-9223372036854775808)]
        ++ testCasts Int String  [(-9223372036854775809,"9223372036854775807"),(-9223372036854775808,"-9223372036854775808"),(0,"0"),(9223372036854775807,"9223372036854775807"),(9223372036854775808,"-9223372036854775808")]
        ++ testCasts Int Integer [(-9223372036854775809,9223372036854775807),(-9223372036854775808,-9223372036854775808),(0,0),(9223372036854775807,9223372036854775807),(9223372036854775808,-9223372036854775808)]
        ++ testCasts Int Bits8   [(-9223372036854775809,255),(0,0),(9223372036854775807,0xff),(9223372036854775808,0)]
        ++ testCasts Int Bits16  [(-9223372036854775809,65535),(0,0),(9223372036854775807,0xffff),(9223372036854775808,0)]
        ++ testCasts Int Bits32  [(-9223372036854775809,4294967295),(0,0),(9223372036854775807,0xffffffff),(9223372036854775808,0)]
        ++ testCasts Int Bits64  [(-9223372036854775809,9223372036854775807),(0,0),(9223372036854775807,9223372036854775807),(9223372036854775808,-9223372036854775808)]

        ++ testCasts Integer Int8    [(-170141183460469231731687303715884105729,-1),(-170141183460469231731687303715884105728,0),(0,0),(170141183460469231731687303715884105727,-1),(170141183460469231731687303715884105728,0)]
        ++ testCasts Integer Int16   [(-170141183460469231731687303715884105729,-1),(-170141183460469231731687303715884105728,0),(0,0),(170141183460469231731687303715884105727,-1),(170141183460469231731687303715884105728,0)]
        ++ testCasts Integer Int32   [(-170141183460469231731687303715884105729,-1),(-170141183460469231731687303715884105728,0),(0,0),(170141183460469231731687303715884105727,-1),(170141183460469231731687303715884105728,0)]
        ++ testCasts Integer Int64   [(-170141183460469231731687303715884105729,-1),(-170141183460469231731687303715884105728,0),(0,0),(170141183460469231731687303715884105727,-1),(170141183460469231731687303715884105728,0)]
        ++ testCasts Integer Int     [(-170141183460469231731687303715884105729,-1),(-170141183460469231731687303715884105728,0),(0,0),(170141183460469231731687303715884105727,-1),(170141183460469231731687303715884105728,0)]
        ++ testCasts Integer String  [(-170141183460469231731687303715884105729,"-170141183460469231731687303715884105729"),(-170141183460469231731687303715884105728,"-170141183460469231731687303715884105728"),(0,"0"),(170141183460469231731687303715884105727,"170141183460469231731687303715884105727"),(170141183460469231731687303715884105728,"170141183460469231731687303715884105728")]
        ++ testCasts Integer Bits8   [(-170141183460469231731687303715884105729,maxBits8),(0,0),(170141183460469231731687303715884105727,0xff),(170141183460469231731687303715884105728,0)]
        ++ testCasts Integer Bits16  [(-170141183460469231731687303715884105729,maxBits16),(0,0),(170141183460469231731687303715884105727,0xffff),(170141183460469231731687303715884105728,0)]
        ++ testCasts Integer Bits32  [(-170141183460469231731687303715884105729,maxBits32),(0,0),(170141183460469231731687303715884105727,0xffffffff),(170141183460469231731687303715884105728,0)]
        ++ testCasts Integer Bits64  [(-170141183460469231731687303715884105729,maxBits64),(0,0),(170141183460469231731687303715884105727,0xffffffffffffffff),(170141183460469231731687303715884105728,0)]

        ++ testCasts Bits8 Int8    [(0,0),(255,-1),(256,0)]
        ++ testCasts Bits8 Int16   [(0,0),(255,255),(256,0)]
        ++ testCasts Bits8 Int32   [(0,0),(255,255),(256,0)]
        ++ testCasts Bits8 Int64   [(0,0),(255,255),(256,0)]
        ++ testCasts Bits8 Int     [(0,0),(255,255),(256,0)]
        ++ testCasts Bits8 Double  [(0,0),(255,255),(256,0)]
        ++ testCasts Bits8 String  [(0,"0"),(255,"255"),(256,"0")]
        ++ testCasts Bits8 Integer [(0,0),(255,255),(256,0)]
        ++ testCasts Bits8 Bits16  [(0,0),(255,255),(256,0)]
        ++ testCasts Bits8 Bits32  [(0,0),(255,255),(256,0)]
        ++ testCasts Bits8 Bits64  [(0,0),(255,255),(256,0)]

        ++ testCasts Bits16 Int8    [(0,0),(0xffff,-1),(0x10000,0)]
        ++ testCasts Bits16 Int16   [(0,0),(0xffff,-1),(0x10000,0)]
        ++ testCasts Bits16 Int32   [(0,0),(0xffff,0xffff),(0x10000,0)]
        ++ testCasts Bits16 Int64   [(0,0),(0xffff,0xffff),(0x10000,0)]
        ++ testCasts Bits16 Int     [(0,0),(0xffff,0xffff),(0x10000,0)]
        ++ testCasts Bits16 Double  [(0,0),(0xffff,0xffff),(0x10000,0)]
        ++ testCasts Bits16 String  [(0,"0"),(0xffff,"65535"),(0x10000,"0")]
        ++ testCasts Bits16 Integer [(0,0),(0xffff,0xffff),(0x10000,0)]
        ++ testCasts Bits16 Bits8   [(0,0),(0xffff,0xff),(0x10000,0)]
        ++ testCasts Bits16 Bits32  [(0,0),(0xffff,0xffff),(0x10000,0)]
        ++ testCasts Bits16 Bits64  [(0,0),(0xffff,0xffff),(0x10000,0)]

        ++ testCasts Bits32 Int8    [(0,0),(0xffffffff,-1),(0x100000000,0)]
        ++ testCasts Bits32 Int16   [(0,0),(0xffffffff,-1),(0x100000000,0)]
        ++ testCasts Bits32 Int32   [(0,0),(0xffffffff,-1),(0x100000000,0)]
        ++ testCasts Bits32 Int64   [(0,0),(0xffffffff,0xffffffff),(0x100000000,0)]
        ++ testCasts Bits32 Int     [(0,0),(0xffffffff,0xffffffff),(0x100000000,0)]
        ++ testCasts Bits32 Double  [(0,0),(0xffffffff,0xffffffff),(0x100000000,0)]
        ++ testCasts Bits32 String  [(0,"0"),(0xffffffff,"4294967295"),(0x100000000,"0")]
        ++ testCasts Bits32 Integer [(0,0),(0xffffffff,0xffffffff),(0x100000000,0)]
        ++ testCasts Bits32 Bits8   [(0,0),(0xffffffff,0xff),(0x100000000,0)]
        ++ testCasts Bits32 Bits16  [(0,0),(0xffffffff,0xffff),(0x100000000,0)]
        ++ testCasts Bits32 Bits64  [(0,0),(0xffffffff,0xffffffff),(0x100000000,0)]

        ++ testCasts Bits64 Int8    [(0,0),(0xffffffffffffffff,-1),(0x10000000000000000,0)]
        ++ testCasts Bits64 Int16   [(0,0),(0xffffffffffffffff,-1),(0x10000000000000000,0)]
        ++ testCasts Bits64 Int32   [(0,0),(0xffffffffffffffff,-1),(0x10000000000000000,0)]
        ++ testCasts Bits64 Int64   [(0,0),(0xffffffffffffffff,-1),(0x10000000000000000,0)]
        ++ testCasts Bits64 Int     [(0,0),(0xffffffffffffffff,-1),(0x10000000000000000,0)]
        ++ testCasts Bits64 Double  [(0,0),(0xffffffffffffffff,0xffffffffffffffff),(0x10000000000000000,0)]
        ++ testCasts Bits64 String  [(0,"0"),(0xffffffffffffffff,"18446744073709551615"),(0x10000000000000000,"0")]
        ++ testCasts Bits64 Integer [(0,0),(0xffffffffffffffff,0xffffffffffffffff),(0x10000000000000000,0)]
        ++ testCasts Bits64 Bits8   [(0,0),(0xffffffffffffffff,0xff),(0x10000000000000000,0)]
        ++ testCasts Bits64 Bits16  [(0,0),(0xffffffffffffffff,0xffff),(0x10000000000000000,0)]
        ++ testCasts Bits64 Bits32  [(0,0),(0xffffffffffffffff,0xffffffff),(0x10000000000000000,0)]

        ++ testCasts String Int8    [("-129",127),("-128",-128),("0",0),("127",127), ("128",-128)]
        ++ testCasts String Int16   [("-32769",32767),("-32768",-32768),("0",0),("32767",32767), ("32768",-32768)]
        ++ testCasts String Int32   [("-2147483649",2147483647),("-2147483648",-2147483648),("0",0),("2147483647",2147483647), ("2147483648",-2147483648)]
        ++ testCasts String Int64   [("-9223372036854775809",9223372036854775807),("-9223372036854775808",-9223372036854775808),("0",0),("9223372036854775807",9223372036854775807), ("9223372036854775808",-9223372036854775808)]
        ++ testCasts String Int     [("-9223372036854775809",9223372036854775807),("-9223372036854775808",-9223372036854775808),("0",0),("9223372036854775807",9223372036854775807), ("9223372036854775808",-9223372036854775808)]
        ++ testCasts String Integer [("-170141183460469231731687303715884105728",-170141183460469231731687303715884105728),("-170141183460469231731687303715884105728",-170141183460469231731687303715884105728),("0",0),("170141183460469231731687303715884105728",170141183460469231731687303715884105728)]
        ++ testCasts String Bits8   [("0",0),("255",255), ("256",0)]
        ++ testCasts String Bits16  [("0",0),("65535",65535), ("65536",0)]
        ++ testCasts String Bits32  [("0",0),("4294967295",4294967295), ("4294967296",0)]
        ++ testCasts String Bits64  [("0",0),("18446744073709551615",18446744073709551615), ("18446744073709551616",0)]

        ++ testCasts Double Int8    [(-129.0, 127),(-128.0,-128),(-12.001,-12),(12.001,12),(127.0,127),(128.0,-128)]
        ++ testCasts Double Int16   [(-32769.0, 32767),(-32768.0,-32768),(-12.001,-12),(12.001,12),(32767.0,32767),(32768.0,-32768)]
        ++ testCasts Double Int32   [(-2147483649.0,2147483647),(-2147483648.0,-2147483648),(-12.001,-12),(12.001,12),(2147483647.0,2147483647),(2147483648.0,-2147483648)]
        ++ testCasts Double Int64   [(-9223372036854775808.0,-9223372036854775808),(-12.001,-12),(12.001,12),(9223372036854775808.0,-9223372036854775808)]
        ++ testCasts Double Int     [(-9223372036854775808.0,-9223372036854775808),(-12.001,-12),(12.001,12),(9223372036854775808.0,-9223372036854775808)]
        ++ testCasts Double Bits8   [(0.0,0),(255.0,255), (256.0,0)]
        ++ testCasts Double Bits16  [(0.0,0),(65535.0,65535), (65536.0,0)]
        ++ testCasts Double Bits32  [(0.0,0),(4294967295.0,4294967295), (4294967296.0,0)]
        ++ testCasts Double Bits64  [(0.0,0),(18446744073709551616.0,0)]

        ++ testCasts Int8 Char    [(-1, '\x0'), (80, 'P')]
        ++ testCasts Int16 Char   [(-1, '\x0'), (80, 'P')]
        ++ testCasts Int32 Char   [(-1, '\x0'), (80, 'P'), (55295, '\xd7ff'), (55296, '\x0'), (57344, '\xe000'), (1114111, '\x10ffff'), (1114112, '\x0')]
        ++ testCasts Int64 Char   [(-1, '\x0'), (80, 'P'), (55295, '\xd7ff'), (55296, '\x0'), (57344, '\xe000'), (1114111, '\x10ffff'), (1114112, '\x0')]
        ++ testCasts Int   Char   [(-1, '\x0'), (80, 'P'), (55295, '\xd7ff'), (55296, '\x0'), (57344, '\xe000'), (1114111, '\x10ffff'), (1114112, '\x0')]
        ++ testCasts Bits8 Char   [(80, 'P')]
        ++ testCasts Bits16 Char  [(80, 'P'), (55295, '\xd7ff'), (55296, '\x0'), (57344, '\xe000')]
        ++ testCasts Bits32 Char  [(80, 'P'), (55295, '\xd7ff'), (55296, '\x0'), (57344, '\xe000'), (1114111, '\x10ffff'), (1114112, '\x0')]
        ++ testCasts Bits64 Char  [(80, 'P'), (55295, '\xd7ff'), (55296, '\x0'), (57344, '\xe000'), (1114111, '\x10ffff'), (1114112, '\x0')]
        ++ testCasts Integer Char [(-1, '\x0'), (80, 'P'), (55295, '\xd7ff'), (55296, '\x0'), (57344, '\xe000'), (1114111, '\x10ffff'), (1114112, '\x0')]

--------------------------------------------------------------------------------
--          Main
--------------------------------------------------------------------------------

main : IO ()
main = traverse_ putStrLn results

max_stars_repo_name: mmhelloworld/idris-jvm

max_issues_repo_name: mmhelloworld/idris-jvm

max_forks_repo_name: mmhelloworld/idris-jvm


text:
module Rect

public export
record Rect where
  constructor CreateRect
  x : Double
  y : Double
  x2 : Double
  y2 : Double

max_stars_repo_name: GrandArchTemplar/IdrisVKAPI

max_issues_repo_name: GrandArchTemplar/IdrisVKAPI

max_forks_repo_name: GrandArchTemplar/IdrisVKAPI


text:
module Mrk.NodeNames

%default total
%access public export

data NodeName : Type where
  Root : NodeName
  Html : NodeName
  Head : NodeName
  Meta : NodeName
  Title : NodeName
  Link : NodeName
  H : (n : Nat) ->
      {auto min : n `GTE` 1} ->
      {auto max : 6 `GTE` n} ->
      NodeName
  Img : NodeName
  Body : NodeName
  Div : NodeName
  P : NodeName
  Ul : NodeName
  Li : NodeName
  A : NodeName
%name NodeName nodeName

Show NodeName where
  show Root = ""
  show Html = "html"
  show Head = "head"
  show Meta = "meta"
  show Title = "title"
  show Link = "link"
  show (H n) = "h" ++ show n
  show Img = "img"
  show Body = "body"
  show Div = "div"
  show P = "p"
  show Ul = "ul"
  show Li = "li"
  show A = "a"

max_stars_repo_name: camelpunch/mrk

max_issues_repo_name: camelpunch/mrk

max_forks_repo_name: camelpunch/mrk


text:
module Process

import System.Concurrency.Raw
import public Data.List -- public, to get proof search machinery

%access public export

-- Process IDs are parameterised by their interface. A request of type
-- 'iface t' will get a response of type 't'
data ProcID : (iface : Type -> Type) -> Type where
     MkPID : Ptr -> ProcID iface

data ServerID : Type where
     MkServer : ProcID iface -> ServerID

implicit MkServer' : ProcID iface -> ServerID
MkServer' = MkServer

data Replied = YesR | NoR

data ReqHandle = MkReqH Nat

-- Current state of a process includes:
--   * the servers it currently has an open connection to
--   * the number of clients it currently has connected
--   * whether it has responded to a request yet

-- Therefore, we can write process types which make clear that a process
-- cannot quit while it is talking to a server, or while it still has clients
-- expecting to communicate with it, or if it has not serviced any requests.
data ProcState : Type where
     MkProcState : (servers : List ServerID) ->
                   (clients : Nat) ->
                   Replied ->
                   ProcState

data Pending : ReqHandle -> List (ReqHandle, Type) -> Type -> Type where
     PendingHere : Pending h ((h, t) :: hs) t
     PendingThere : Pending h hs t -> Pending h ((h', t') :: hs) t

dropPending : (hs : List (ReqHandle, Type)) -> Pending h hs ty ->
              List (ReqHandle, Type)
dropPending ((h, t) :: xs) PendingHere = xs
dropPending ((h', t') :: xs) (PendingThere x)
     = ((h', t') :: dropPending xs x)

data ConnectedTo : ServerID -> ProcState -> Type where
     IsConnectedTo : Elem p servers ->
                     ConnectedTo p (MkProcState servers c reply)

data NoClient : ProcState -> Type where
     IsNoClient : NoClient (MkProcState servers 0 reply)

data OneClient : ProcState -> Type where
     IsOneClient : OneClient (MkProcState servers (S k) reply)

data Reply : ProcState -> Type where
     IsReply : Reply (MkProcState s c YesR)

data NoReply : ProcState -> Type where
     IsNoReply : NoReply (MkProcState s c NoR)

{-- Some useful operations on process state --}
newClient : ProcState -> ProcState
newClient (MkProcState servers clients r)
         = MkProcState servers (S clients) r

setClients : ProcState -> Nat -> ProcState
setClients (MkProcState servers clients r) k
          = MkProcState servers k r

newServer : ProcID iface -> ProcState -> ProcState
newServer p (MkProcState servers clients r)
           = MkProcState (MkServer p :: servers) clients r

dropServer : (pid : ProcID iface) -> (p : ProcState) ->
             ConnectedTo (MkServer pid) p -> ProcState
dropServer pid (MkProcState servers c r) (IsConnectedTo prf)
         = MkProcState (dropElem servers prf) c r

{-
pendingReq : ProcID iface -> (h : ReqHandle) -> iface t ->
             ProcState hs -> ProcState ((h, t) :: hs)
pendingReq {t} p h x (MkProcState s c r) = MkProcState s c r

doneReq : ProcState hs -> (p : Pending h hs) -> ProcState (dropPending hs p)
doneReq (MkProcState s c r) p = MkProcState s c r
-}

replied : ProcState -> ProcState
replied (MkProcState servers clients r)
        = MkProcState servers clients YesR

resetReplied : ProcState -> ProcState
resetReplied (MkProcState servers clients r)
        = MkProcState servers clients NoR

runningServer : Nat -> ProcState
runningServer c = MkProcState [] (S c) NoR

doneServer : ProcState
doneServer = MkProcState [] 0 YesR

init : List ServerID -> ProcState
init s = MkProcState s 0 NoR

{-- Processes themselves.

A process returns some type 'a', responds to requests on the interface
'iface', and has an input and output state.
--}
mutual
  data Process : (a : Type) -> (iface : Type -> Type) ->
                 List (ReqHandle, Type) -> (a -> List (ReqHandle, Type)) ->
                 ProcState -> (a -> ProcState) ->
                 Type where
     -- Some plumbing
     Lift' : IO a -> Process a iface hs (const hs) p (const p)
     Pure : a -> Process a iface hs (const hs) p (const p)
     Quit : a -> Process a iface hs (const hs) p (const (resetReplied p))

     Bind : Process a iface hs hs' p p' ->
            ((x : a) -> Process b iface (hs' x) hs'' (p' x) p'') ->
            Process b iface hs hs'' p p''

     Fork : Process () serveri [] (const []) (runningServer 1) (const Process.doneServer) ->
            Process (ProcID serveri) iface hs (const hs) p (\res => (newServer res p))
     Work : (worker : (pid : ProcID iface) -> Worker [pid] ()) ->
            (waiter : Process t iface hs (const hs) (runningServer 1) (const Process.doneServer)) ->
            Process t iface hs (const hs) p (const p)

     Request : (r : ProcID serveri) -> (x : serveri ty) ->
               {auto connected : ConnectedTo (MkServer r) p} ->
               Process ReqHandle iface
                       hs (\h => (h, ty) :: hs)
                       p (const p)

     GetReply : (h : ReqHandle) ->
                {auto pending : Pending h hs ty} ->
                Process ty iface
                        hs (const (dropPending hs pending))
                        p (const p)

     TimeoutRespond : (timeout : Int) ->
                      (def : res) ->
                      ({t : Type} -> (x : iface t) ->
                                     Response (t, res) iface hs p) ->
                      Process res iface hs (const hs) p (const (replied p))

     Respond : ({t : Type} -> (x : iface t) ->
                              Response (t, res) iface hs p) ->
               Process res iface hs (const hs) p (const (replied p))

     Connect : (r : ProcID serveri) ->
               Process Bool iface
                       hs (const hs)
                       p (\ok => case ok of
                                      True => newServer r p
                                      False => p)

     Disconnect : (r : ProcID serveri) ->
                  {auto connected : ConnectedTo (MkServer r) p} ->
                  Process () iface
                          hs (const hs)
                          p (const (dropServer r p connected))

     CountClients : Process Nat iface hs (const hs) p (\n => setClients p n)

     -- FIXME: The process had better be guaranteed to change the system
     -- state (e.g. finish with a YesR since it starts with a NoR) because
     -- then it can't be used in a Respond, so responding can't loop.
     Loop : Inf (Process t iface hs hs' (resetReplied p) p') ->
            Process t iface hs hs' p p'

  -- 'Running a iface' is the type of a process which is currently
  -- responding to requests (i.e. knows it has at least one client connected)
  -- and will not exit unless there are no clients connected
  Running : Type -> (iface : Type -> Type) -> Type
  Running a iface = {k : Nat} -> Process a iface [] (const []) (runningServer k) (const doneServer)

  Response : Type -> (iface : Type -> Type) -> List (ReqHandle, Type) ->
                     ProcState -> Type
  Response a iface hs p =  Process a iface hs (const hs) p (const p)

  -- 'Program a' is the type of a process which does not respond to any requests
  -- and begins and ends with no connections to any server open.
  Program : Type -> (iface : Type -> Type) -> Type
  Program a iface = Process a iface [] (const []) (init []) (const (init []))

  -- 'Connected s a' is the type of a process which does not respond to any
  -- requests and begins and ends with connections to a given server list.
  Connected : List ServerID -> Type -> Type
  Connected s a = Process a (const Void) [] (const []) (init s) (const (init s))

  -- 'Worker s a' is the type of a process which does not respond to any
  -- requests, and begins with a connection to a server it is to send a
  -- notification to.
  Worker : List ServerID -> Type -> Type
  Worker s a = Process a (const Void) [] (const []) (init s) (const (init []))

implicit
Lift : IO a -> Process a iface hs (const hs) p (const p)
Lift = Lift'

%no_implicit -- helps error messages, and speeds things up a bit
%inline -- so that the productivity checker treats 'bind' as a constructor!
(>>=) : Process a iface hs hs' p p' ->
        ((x : a) -> Process b iface (hs' x) hs'' (p' x) p'') ->
        Process b iface hs hs'' p p''
(>>=) = Bind

TrySend : (proc : ProcID iface) -> iface ty ->
          Process (Maybe ty) iface'
                  hs (const hs)
                  (MkProcState s c r) (const (MkProcState s c r))
TrySend pid req = do True <- Connect pid | False => Pure Nothing
                     h <- Request pid req
                     resp <- GetReply h
                     Disconnect pid
                     Pure (Just resp)

Send : (proc : ProcID iface) -> iface ty ->
       {auto prf : Elem (MkServer proc) s} ->
       Process ty iface'
               hs (const hs)
               (MkProcState s c r) (const (MkProcState s c r))
Send pid req = do h <- Request pid req
                  GetReply h

{--- evaluator --}

-- The evaluator keeps track of the number of client connections open,
-- and manages Connect/Disconnect requests by managing them whenever a
-- 'Respond' or 'TimeoutRespond' is encountered.

data MessageQ : (Type -> Type) -> Type where
     ConnectMsg : MessageQ iface
     CloseMsg : MessageQ iface
     RequestMsg : Nat -> iface t -> MessageQ iface

data MessageR : Type -> Type where
     ReplyMsg : Nat -> (ans : ty) -> MessageR ty

data Message : (Type -> Type) -> List (ReqHandle, Type) -> Type where
     MsgQuery : MessageQ iface -> Message iface hs
     MsgReply : (reply : MessageR ty) -> Message iface hs

readMsg : IO (Maybe (Ptr, Message iface hs))
readMsg {iface} {hs} =
   do if !checkMsgs
      then do (p, _, msg) <- getMsgWithSender {a = Message iface hs}
              pure (Just (p, msg))
      else pure Nothing

readMsgTimeout : Int -> IO (Maybe (Ptr, Message iface hs))
readMsgTimeout {iface} {hs} i =
   do if !(checkMsgsTimeout i)
      then do (pid, _, msg) <- getMsgWithSender {a = Message iface hs}
              pure (Just (pid, msg))
      else pure Nothing

data RespEnv : List (ReqHandle, Type) -> Type where
     Nil : RespEnv []
     (::) : Maybe ty -> RespEnv hs -> RespEnv ((h, ty) :: hs)

record EvalState (iface : Type -> Type) (hs : List (ReqHandle, Type)) where
  constructor MkEvalState
  queue : List (Ptr, MessageQ iface)
  reply : RespEnv hs
  clients : Nat
  nexthandle : Nat

lookup : Pending h hs ty -> RespEnv hs -> Maybe ty
lookup PendingHere (x :: xs) = x
lookup (PendingThere p) (x :: xs) = lookup p xs

dropResp : (pending : Pending h hs ty) ->
           RespEnv hs -> RespEnv (dropPending hs pending)
dropResp PendingHere (x :: xs) = xs
dropResp (PendingThere p) (x :: xs) = x :: dropResp p xs

updateReplies : Pending h hs ty -> ty -> RespEnv hs -> RespEnv hs
updateReplies PendingHere msg (x :: xs) = Just msg :: xs
updateReplies (PendingThere p) msg (x :: xs) = x :: updateReplies p msg xs

total
findPending : (h : ReqHandle) -> RespEnv hs -> Maybe (ty ** Pending h hs ty)
findPending {hs = []} k [] = Nothing
findPending {hs = ((MkReqH h, t) :: hs)} (MkReqH k) (x :: xs) with (decEq h k)
  findPending {hs = ((MkReqH h, t) :: hs)} (MkReqH h) (x :: xs) | (Yes Refl)
       = Just (t ** PendingHere)
  findPending {hs = ((MkReqH h, t) :: hs)} (MkReqH k) (x :: xs) | (No contra)
       = do (ty' ** p') <- findPending (MkReqH k) xs
            Just (ty' ** PendingThere p')

covering
updateQueue : EvalState iface hs -> IO (EvalState iface hs)
updateQueue {iface} {hs} st
  = case !(readMsg {iface} {hs}) of
         Nothing => pure st
         Just (pid, MsgQuery msg) =>
              updateQueue (record { queue = queue st ++ [(pid, msg)] } st)
         Just (pid, MsgReply (ReplyMsg rq ans)) =>
              case findPending (MkReqH rq) (reply st) of
                   Nothing => updateQueue {iface} {hs} st -- can't happen!
                   Just (ty ** pend) =>
                        updateQueue (record { reply = updateReplies pend (believe_me ans) (reply st) } st)

-- Keep updating the queue with incoming messages until either we get a
-- RequestMsg, or we reach a timeout.
covering
updateQueueTimeout : Int -> EvalState iface hs -> IO (EvalState iface hs)
updateQueueTimeout {iface} {hs} i st
  = case !(readMsgTimeout {iface} {hs} i) of
         Nothing => pure st
         Just (pid, MsgQuery (RequestMsg rq msg)) =>
              pure (record { queue = queue st ++ [(pid, RequestMsg rq msg)] } st)
         Just (pid, MsgQuery msg) => do
              -- TODO: Why not update client count here too?
              updateQueueTimeout i (record { queue = queue st ++ [(pid, msg)] } st)
         Just (pid, MsgReply (ReplyMsg rq ans)) =>
              case findPending (MkReqH rq) (reply st) of
                   Nothing => updateQueueTimeout i {iface} {hs} st -- can't happen!
                   Just (ty ** pend) =>
                        updateQueueTimeout i (record { reply = updateReplies pend (believe_me ans) (reply st) } st)

total
removeReq : List (Ptr, MessageQ iface) -> List (Ptr, MessageQ iface) ->
             Maybe (Ptr, (ty ** (Nat, iface ty)), List (Ptr, MessageQ iface))
removeReq acc [] = Nothing
removeReq acc ((pid, RequestMsg rq m) :: xs) = Just (pid, (_ ** (rq, m)), reverse acc ++ xs)
removeReq acc (x :: xs) = removeReq (x :: acc) xs

total
removeConn : Nat ->
             List (Ptr, MessageQ iface) -> List (Ptr, MessageQ iface) ->
             (Nat, List (Ptr, MessageQ iface))
removeConn cl acc [] = (cl, reverse acc)
removeConn cl acc ((pid, ConnectMsg) :: xs)
     = removeConn (cl + 1) acc xs
removeConn cl acc ((pid, CloseMsg) :: xs)
     = removeConn (minus cl 1) acc xs
removeConn cl acc (x :: xs) = removeConn cl (x :: acc) xs

-- Remove the first thing in the event list which is a request, if it
-- exists.
getRequest :  EvalState iface hs -> Maybe (Ptr, (ty ** (Nat, iface ty)), EvalState iface hs)
getRequest (MkEvalState queue reply clients nh)
     = do (pid, req, queue') <- removeReq [] queue
          pure (pid, req, MkEvalState queue' reply clients nh)

countClients : EvalState iface hs -> (Nat, EvalState iface hs)
countClients (MkEvalState queue reply clients nh)
     = let (clients', queue') = removeConn clients [] queue in
           (clients', MkEvalState queue' reply clients' nh)

-- sendResponse : Ptr ->
--                (ty -> EvalState iface hs -> IO a) ->
--                (x, ty) -> EvalState iface hs ->
--                IO a
-- sendResponse {iface} {hs} pid k (resp, val) st = do
--        sendToThread pid (MsgReply {hs} {iface} ?prf (ReplyMsg resp))
--        k val st

covering
eval : EvalState iface hs ->
       {p : ProcState} -> {p' : ty -> ProcState} ->
       Process ty iface hs hs' p p' ->
       ((res : ty) -> EvalState iface (hs' res) -> IO a) -> IO a
eval st (Lift' x) k = do x' <- x
                         k x' st
eval st (Pure x) k = k x st
eval st (Quit x) k = k x st
eval st (Bind x f) k = eval st x (\x', st' => eval st' (f x') k)

eval st (Fork proc) k
        = do ptr <- fork (eval (MkEvalState [] [] 1 0) proc (\_, _ => pure ()))
             k (MkPID ptr) st

eval st (Work proc cont) k
        = do me <- getMyVM
             ptr <- fork (eval (MkEvalState [] [] 0 0) (proc (MkPID me))
                               (\_, _ => pure ()))
             eval (record { clients = clients st + 1 } st) cont k

eval {hs} (MkEvalState q reqs c nh) (Request (MkPID pid) x) k
     = do sendToThread pid 0 (MsgQuery {hs} (RequestMsg nh x))
          k (MkReqH nh) (MkEvalState q (Nothing :: reqs) c (S nh))

eval {p} st (GetReply {pending} h) k
      = do -- Need to keep receiving messages until there's a response
           -- available
           MkEvalState q reqs c nh <- updateQueue st
           case lookup pending reqs of
                Nothing => do checkMsgsTimeout 1
                              eval {p} (MkEvalState q reqs c nh) (GetReply h) k
                Just reply =>
                    k reply (MkEvalState q (dropResp pending reqs) c nh)

eval {iface} {hs} st (TimeoutRespond timeout def f) k
      = do st' <- updateQueueTimeout timeout st
           case getRequest st' of
                Nothing => k def st'
                Just (pid, (_ ** (rq, req)), st'') => do
                     eval st'' (f req) -- (sendResponse pid k) -- ?foo
                       -- this weirdness works around an erasure bug
                       -- which causes a seg fault...
                       (\ r, st''' =>
                            case r of
                               (resp, val) => do
                                  sendToThread pid 0 (MsgReply {iface} {hs} (ReplyMsg rq resp))
                                  k val st''')

eval {iface} {hs} st (Respond f) k
      = do st' <- updateQueue st
           case getRequest st' of
                Nothing => eval {iface} st' (Respond f) k
                Just (pid, (_ ** (rq, req)), st'') => do
                     eval st'' (f req) (\ (resp, val), st''' => do
                       sendToThread pid 0 (MsgReply {iface} {hs} (ReplyMsg rq resp))
                       k val st''')

eval {hs} st (Connect {serveri} (MkPID pid)) k
     = do me <- getMyVM
          if pid == me then k False st else do
            v <- sendToThread pid 0 (MsgQuery {iface=serveri} {hs}
                                              ConnectMsg)
            -- TODO: Wait for ACK
            k (v == 1) st

eval {hs} st (Disconnect {serveri} (MkPID pid)) k
     = do v <- sendToThread pid 0 (MsgQuery {iface=serveri} {hs}
                                            CloseMsg)
          k () st

eval st CountClients k
     = do st' <- updateQueue st
          let (cl, st'') = countClients st'
          k cl st''

eval st (Loop x) k = eval st x k

run : Program a iface -> IO a
run p = eval (MkEvalState [] [] 0 0) p (\res, t => pure res)

max_stars_repo_name: grin-compiler/idris-grin

max_issues_repo_name: grin-compiler/idris-grin

max_forks_repo_name: grin-compiler/idris-grin


text:
import Data.Vect

tryIndex : Integer -> Vect n a -> Maybe a
tryIndex {n} i xs = case integerToFin i n of
                         Nothing => Nothing
                         (Just idx) => Just (index idx xs)

sumEntries : (Num a) => (pos : Integer) -> Vect n a -> Vect n a -> Maybe a
sumEntries {n} pos xs ys = let left = tryIndex pos xs
                               right = tryIndex pos ys
                               in case (left,right) of
                                       (Just x,Just y) => Just (x+y)
                                       _ => Nothing

max_stars_repo_name: janschultecom/idris-examples

max_issues_repo_name: janschultecom/idris-examples

max_forks_repo_name: janschultecom/idris-examples