text:
module Language.JSON.Accessors

import Data.Either
import Data.List
import Data.Vect
import Language.JSON

%default total

export
lookupAll : Vect n String -> List (String, JSON) -> Either String (Vect n JSON)
lookupAll [] dict            = Right []
lookupAll (key :: keys) dict = [| lookup' key dict :: lookupAll keys dict |]
  where
    lookup' : String -> List (String, a) -> Either String a
    lookup' key = maybeToEither "Missing required key: \{key}." . lookup key

export
bool : JSON -> Either String Bool
bool (JBoolean x) = Right x
bool json = Left "Expected a bool but found \{show json}."

export
string : JSON -> Either String String
string (JString x) = Right x
string json = Left "Expected a string but found \{show json}."

export
integer : JSON -> Either String Integer
integer (JNumber x) = Right $ cast x
integer json = Left "Expected an integer but found \{show json}."

export
array : (JSON -> Either String a) -> JSON -> Either String (List a)
array f (JArray xs) = traverse f xs
array f json = Left "Expected an array but found \{show json}."

export
object : JSON -> Either String (List (String, JSON))
object (JObject xs) = Right xs
object json = Left "Expected an object but found \{show json}."

max_stars_repo_name: mattpolzin/harmony

max_issues_repo_name: mattpolzin/harmony

max_forks_repo_name: mattpolzin/harmony


text:
||| Tabulation gives a bijection between functions `f : Fin n -> a`
||| (up to extensional equality) and vectors `tabulate f : Vect n a`.
module Data.Vect.Properties.Tabulate

import Data.Vect
import Data.Fin

||| Vectors are uniquely determined by their elements
export
vectorExtensionality
  : (xs, ys : Vect n a) -> (ext : (i : Fin n) -> index i xs = index i ys)
 -> xs = ys
vectorExtensionality    []        []     ext = Refl
vectorExtensionality (x :: xs) (y :: ys) ext =
  cong2 (::)
        (ext FZ)
        (vectorExtensionality xs ys (\i => ext (FS i)))

||| Extensionally equivalent functions tabulate to the same vector
export
tabulateExtensional
  : {n : Nat} -> (f, g : Fin n -> a) -> (ext : (i : Fin n) -> f i = g i)
 -> tabulate f = tabulate g
tabulateExtensional {n = 0  } f g ext = Refl
tabulateExtensional {n = S n} f g ext =
  cong2 (::) (ext FZ) (tabulateExtensional (f . FS) (g . FS) (\ i => ext $ FS i))

||| Taking an index amounts to applying the tabulated function
export
indexTabulate : {n : Nat} -> (f : Fin n -> a) -> (i : Fin n) -> index i (tabulate f) = f i
indexTabulate f  FZ    = Refl
indexTabulate f (FS i) = indexTabulate (f . FS) i

||| The empty vector represents the unique function `Fin 0 -> a`
export
emptyInitial : (v : Vect 0 a) -> v = []
emptyInitial [] = Refl

ext: idr


text:
module Test.Leap

import Test.Assertions
import System

import Leap

collect : {default 0 acc : Nat} -> (List (IO Bool)) -> IO Nat
collect {acc} []               = pure acc
collect {acc} (test :: tests) = do
    bool <- test
    case bool of
        True  => collect {acc=acc}   tests
        False => collect {acc=S acc} tests

export
runTests : IO ()
runTests = do
    count <- collect
        [ assertFalse (isLeap 2015)
        , assertTrue  (isLeap 2016)
        , assertFalse (isLeap 2100)
        , assertTrue  (isLeap 2000)
        , assertEquals version "1.0.0"
        ]
    case count of
        Z => exitSuccess
        _ => exitFailure


text:
module Compiler.Jvm.Tuples

public export
second : (a, b, c) -> b
second (_, value, _) = value

public export
third : (a, b, c) -> c
third (_, _, value) = value

public export
updateFirst : c -> (a, b) -> (c, b)
updateFirst v (_, b) = (v, b)

public export
updateSecond : c -> (a, b) -> (a, c)
updateSecond v (a, _) = (a, v)

public export
swap : (a, b) -> (b, a)
swap (x, y) = (y, x)


text:
data Bool = False | True
data Nat = Z | S Nat

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

isZero : Nat -> Bool
isZero Z = True
isZero (S k) = False

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

testZ : Nat -> String
testZ x = if isZero x then "Zero" else
             if isOdd x then "Odd" else "Even"


text:
-- --------------------------------------------------------- [ Model.idr<Code> ]
-- Module      : UML.Code.Model
-- Description : Data types for common code constructs.
-- Copyright   : (c) Jan de Muijnck-Hughes
-- License     : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
module UML.Code.Model

%access public

data DType : Type where
    MkSType : (name : String) -> DType
    MkCType : (name : String) -> (attrs : List (String, String)) -> DType
--    MkLType : (name : String) -> (itemTy : DType) -> DType

DTypes : Type
DTypes = List DType

||| Defines a function in an interface.
data Function : Type where
    ||| Constructs a new function.
    MkPFunc : (name : String)
            -> (ps : List (Pair String String))
            -> (retTy : String) -> Function
    MkFunc : (name : String)
           -> (rety : String)
           -> Function

-- ---------------------------------------------------------------------- [ Eq ]

instance Eq DType where
    (==) (MkSType x)    (MkSType y)    = x == y
    (==) (MkCType x xs) (MkCType y ys) = x == y && xs == ys
    (==) _ _ = False

instance Eq Function where
    (==) (MkPFunc x xs xr) (MkPFunc y ys yr) = x == y && xs == ys && xr == yr
    (==) (MkFunc x xr)     (MkFunc y yr)     = x == y && xr == yr
    (==) _ _ = False

-- -------------------------------------------------------------------- [ Show ]

instance Show DType where
    show (MkSType n) = unwords ["[Data Simple", show n, "]\n"]
    show (MkCType n as) = unwords ["[Data Complex", show n, show as, "]\n"]

instance Show Function where
    show (MkPFunc n ps rty) = unwords ["[Func", show n, show ps, show rty, " ]\n"]
    show (MkFunc n rty)     = unwords ["[Func", show n, show rty, "]\n"]

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

max_stars_repo_name: jfdm/idris-uml

max_issues_repo_name: jfdm/idris-uml

max_forks_repo_name: jfdm/idris-uml


text:
module Algebra.Ring

import Syntax.PreorderReasoning

%default total

public export %inline %tcinline
neg : Neg a => a -> a
neg = negate

||| This interface is a witness that for a (primitive)
||| integral type `a` the axioms of a commutative ring hold:
|||
||| 1. `a` is an abelian group under addition:
|||    1. `+` is associative: `k + (m + n) = (k + m) + n` for all `k,m,n : a`.
|||    2. `+` is commutative: `m + n = n + m` for all `m,n : a`.
|||    3. 0 is the additive identity: `n + 0 = n` for all `n : a`.
|||    4. `neg n` is the additive inverse of `n`:
|||       `n + neg n = 0` for all `n : a`.
|||
||| 2. `a` is a commutative monoid under multiplication:
|||    1. `*` is associative: `k * (m * n) = (k * m) * n` for all `k,m,n : a`.
|||    2. `*` is commutative: `m * n = n * m` for all `m,n : a`.
|||    3. 1 is the multiplicative identity: `n * 1 = n` for all `n : a`.
|||
||| 3. Multiplication is distributive with respect to addition:
|||    `k * (m + n) = (k * m) + (k * n)` for all `k,m,n : a`.
|||
||| 4. Subtraction syntax: `m - n = m + neg n` for all `m,n : a`.
public export
interface Neg a => Ring a where
  ||| Addition is associative.
  0 plusAssociative : {k,m,n : a} -> k + (m + n) === (k + m) + n

  ||| Addition is commutative.
  0 plusCommutative : {m,n : a} -> m + n === n + m

  ||| 0 is the additive identity.
  0 plusZeroLeftNeutral : {n : a} -> 0 + n === n

  ||| `neg n` is the additive inverse of `n`.
  0 plusNegLeftZero : {n : a} -> neg n + n === 0

  ||| Multiplication is associative.
  0 multAssociative : {k,m,n : a} -> k * (m * n) === (k * m) * n

  ||| Multiplication is commutative.
  0 multCommutative : {m,n : a} -> m * n === n * m

  ||| 1 is the multiplicative identity.
  0 multOneLeftNeutral : {n : a} -> 1 * n === n

  ||| Multiplication is distributive with respect to addition.
  0 leftDistributive : {k,m,n : a} -> k * (m + n) === (k * m) + (k * n)

  ||| `m - n` is just "syntactic sugar" for `m + neg n`.
  0 minusIsPlusNeg : {m,n : a} -> m - n === m + neg n

--------------------------------------------------------------------------------
--          Proofs on Addition
--------------------------------------------------------------------------------

||| `n + 0 === n` for all `n : a`.
export
0 plusZeroRightNeutral : Ring a => {n : a} -> n + 0 === n
plusZeroRightNeutral =
  Calc $
    |~ n + 0
    ~~ 0 + n ... plusCommutative
    ~~ n     ... plusZeroLeftNeutral

||| `n + neg n === 0` for all `n : a`.
export
0 plusNegRightZero : Ring a => {n : a} -> n + neg n === 0
plusNegRightZero =
  Calc $
    |~ n + neg n
    ~~ neg n + n ... plusCommutative
    ~~ 0         ... plusNegLeftZero

||| `n - n === 0` for all `n : a`.
export
0 minusSelfZero : Ring a => {n : a} -> n - n === 0
minusSelfZero =
  Calc $
    |~ n - n
    ~~ n + neg n ... minusIsPlusNeg
    ~~ 0         ... plusNegRightZero

||| Law of associativity for subtraction.
export
0 plusMinusAssociative :  Ring a
                       => {k,m,n : a}
                       -> k + (m - n) === (k + m) - n
plusMinusAssociative =
  Calc $
    |~ k + (m - n)
    ~~ k + (m + neg n) ..> cong (k+) minusIsPlusNeg
    ~~ (k + m) + neg n ..> plusAssociative
    ~~ (k + m) - n     ..< minusIsPlusNeg

||| We can solve equations involving addition.
export
0 solvePlusRight :  Ring a
               => {k,m,n : a}
               -> k + m === n
               -> k === n - m
solvePlusRight prf =
  Calc $
    |~ k
    ~~ k + 0        ..< plusZeroRightNeutral
    ~~ k + (m - m)  ..< cong (k +) minusSelfZero
    ~~ (k + m) - m  ..> plusMinusAssociative
    ~~ n - m        ..> cong (\x => x - m) prf

||| We can solve equations involving addition.
export
0 solvePlusLeft :  Ring a
              => {k,m,n : a}
              -> k + m === n
              -> m === n - k
solvePlusLeft prf =
  solvePlusRight $ Calc $
    |~ m + k
    ~~ k + m ... plusCommutative
    ~~ n     ... prf

||| Addition from the left is injective.
export
0 plusLeftInjective : Ring a => {k,m,n : a} -> k + n === m + n -> k === m
plusLeftInjective prf =
  Calc $
    |~ k
    ~~ (m + n) - n ..> solvePlusRight prf
    ~~ m + (n - n) ..< plusMinusAssociative
    ~~ m + 0       ..> cong (m +) minusSelfZero
    ~~ m           ..> plusZeroRightNeutral

||| Addition from the right is injective.
export
0 plusRightInjective : Ring a => {k,m,n : a} -> n + k === n + m -> k === m
plusRightInjective prf =
  plusLeftInjective $
    Calc $
      |~ k + n
      ~~ n + k  ... plusCommutative
      ~~ n + m  ... prf
      ~~ m + n  ... plusCommutative

||| From `m + n === 0` follows that `n` is the
||| additive inverse of `m`.
export
0 solvePlusNegRight :  Ring a
                    => {m,n : a}
                    -> m + n === 0
                    -> n === neg m
solvePlusNegRight prf =
  plusRightInjective (trans prf (sym plusNegRightZero))

||| From `m + n === 0` follows that `m` is the
||| additive inverse of `n`.
export
0 solvePlusNegLeft :  Ring a
                   => {m,n : a}
                   -> m + n === 0
                   -> m === neg n
solvePlusNegLeft prf =
  solvePlusNegRight $ Calc $
    |~ n + m
    ~~ m + n ... plusCommutative
    ~~ 0     ... prf

||| From `m + n === m` follows `n === 0`.
export
0 solvePlusZeroRight :  Ring a => {m,n : a} -> m + n === m -> n === 0
solvePlusZeroRight prf =
    Calc $
      |~ n
      ~~ m - m ... solvePlusLeft prf
      ~~ 0     ... minusSelfZero

||| From `n + m === m` follows `n === 0`.
export
0 solvePlusZeroLeft :  Ring a => {m,n : a} -> n + m === m -> n === 0
solvePlusZeroLeft prf =
    solvePlusZeroRight $ Calc $
      |~ m + n
      ~~ n + m ... plusCommutative
      ~~ m     ... prf

||| Negation is involutory.
export
0 negInvolutory : Ring a => {n : a} -> neg (neg n) === n
negInvolutory = sym $ solvePlusNegLeft plusNegRightZero

||| From `neg n === 0` follows `n === 0`.
export
0 solveNegZero : Ring a => {n : a} -> neg n === 0 -> n === 0
solveNegZero prf =
  Calc $
    |~ n
    ~~ n + 0     ..< plusZeroRightNeutral
    ~~ n + neg n ..< cong (n +) prf
    ~~ 0         ..> plusNegRightZero

||| `neg 0 === 0`
export
0 negZero : Ring a => neg {a} 0 === 0
negZero = solveNegZero negInvolutory

export
0 negDistributes : Ring a => {m,n : a} -> neg (m + n) === neg m + neg n
negDistributes =
  sym $ solvePlusNegLeft $ Calc $
  |~ (neg m + neg n) + (m + n)
  ~~ (neg m + neg n) + (n + m) ... cong ((neg m + neg n) +) plusCommutative
  ~~ ((neg m + neg n) + n) + m ... plusAssociative
  ~~ (neg m + (neg n + n)) + m ..< cong (+m) plusAssociative
  ~~ (neg m + 0) + m           ... cong (\x => neg m + x + m) plusNegLeftZero
  ~~ neg m + m                 ... cong (+m) plusZeroRightNeutral
  ~~ 0                         ... plusNegLeftZero

--------------------------------------------------------------------------------
--          Proofs on Multiplication
--------------------------------------------------------------------------------

||| `n * 1 === n` for all `n : a`.
export
0 multOneRightNeutral : Ring a => {n : a} -> n * 1 === n
multOneRightNeutral =
  Calc $
    |~ n * 1
    ~~ 1 * n ... multCommutative
    ~~ n     ... multOneLeftNeutral

||| Zero is an absorbing element of multiplication.
export
0 multZeroRightAbsorbs : Ring a => {n : a} -> n * 0 === 0
multZeroRightAbsorbs =
  solvePlusZeroRight $ Calc $
    |~ (n * 0) + (n * 0)
    ~~ n * (0 + 0)       ..< leftDistributive
    ~~ n * 0             ..> cong (n *) plusZeroLeftNeutral

||| Zero is an absorbing element of multiplication.
export
0 multZeroLeftAbsorbs : Ring a => {n : a} -> 0 * n === 0
multZeroLeftAbsorbs =
  Calc $
    |~ 0 * n
    ~~ n * 0 ... multCommutative
    ~~ 0     ... multZeroRightAbsorbs

||| Zero is an absorbing element of multiplication.
export
0 multZeroAbsorbs :  Ring a
                  => {m,n : a}
                  -> Either (m === 0) (n === 0)
                  -> m * n === 0
multZeroAbsorbs (Left rfl) =
  Calc $
    |~ m * n
    ~~ 0 * n ... cong (*n) rfl
    ~~ 0     ... multZeroLeftAbsorbs

multZeroAbsorbs (Right rfl) =
  Calc $
    |~ m * n
    ~~ m * 0 ... cong (m*) rfl
    ~~ 0     ... multZeroRightAbsorbs

||| `m * (-n) = - (m * n)`.
export
0 multNegRight : Ring a => {m,n : a} -> m * neg n === neg (m * n)
multNegRight =
  solvePlusNegRight $ Calc $
     |~ m * n + m * neg n
     ~~ m * (n + neg n)   ..< leftDistributive
     ~~ m * 0             ..> cong (m *) plusNegRightZero
     ~~ 0                 ..> multZeroRightAbsorbs

||| `- (m * (-n)) = m * n`.
export
0 negMultNegRight : Ring a => {m,n : a} -> neg (m * neg n) === m * n
negMultNegRight =
  Calc $
    |~ neg (m * neg n)
    ~~ neg (neg (m * n)) ... cong neg multNegRight
    ~~ m * n             ... negInvolutory

||| `(- m) * n = - (m * n)`.
export
0 multNegLeft : Ring a => {m,n : a} -> neg m * n === neg (m * n)
multNegLeft =
  Calc $
    |~ neg m * n
    ~~ n * neg m   ... multCommutative
    ~~ neg (n * m) ... multNegRight
    ~~ neg (m * n) ... cong neg multCommutative

||| `- ((-m) * n) = m * n`.
export
0 negMultNegLeft : Ring a => {m,n : a} -> neg (neg m * n) === m * n
negMultNegLeft =
  Calc $
    |~ neg (neg m * n)
    ~~ neg (neg (m * n)) ... cong neg multNegLeft
    ~~ m * n             ... negInvolutory

||| Multiplication with `(-1)` is negation.
export
0 multMinusOneRight : Ring a => {n : a} -> n * neg 1 === neg n
multMinusOneRight =
  Calc $
    |~ n * neg 1
    ~~ neg (n * 1) ... multNegRight
    ~~ neg n       ... cong neg multOneRightNeutral

||| Multiplication with `(-1)` is negation.
export
0 multMinusOneLeft : Ring a => {n : a} -> neg 1 * n === neg n
multMinusOneLeft =
  Calc $
    |~ neg 1 * n
    ~~ neg (1 * n) ... multNegLeft
    ~~ neg n       ... cong neg multOneLeftNeutral

||| Multiplication of two negations removes negations.
export
0 negMultNeg : Ring a => {m,n : a} -> neg m * neg n === m * n
negMultNeg =
  Calc $
    |~ neg m * neg n
    ~~ neg (m * neg n)   ... multNegLeft
    ~~ neg (neg (m * n)) ... cong neg multNegRight
    ~~ m * n             ... negInvolutory

||| Multiplication is distributive with respect to addition.
export
0 rightDistributive :  Ring a
                    => {k,m,n : a}
                    -> (m + n) * k === m * k + n * k
rightDistributive =
  Calc $
    |~ (m + n) * k
    ~~ k * (m + n)       ... multCommutative
    ~~ (k * m) + (k * n) ... leftDistributive
    ~~ m * k + k * n     ... cong (+ k * n) multCommutative
    ~~ m * k + n * k     ... cong (m * k +) multCommutative

export
0 multPlusSelf : Ring a => {m,n : a} -> m * n + m === m * (n + 1)
multPlusSelf =
  Calc $
    |~ m * n + m
    ~~ m * n + m * 1 ..< cong (m*n +) multOneRightNeutral
    ~~ m * (n + 1)   ..< leftDistributive

--------------------------------------------------------------------------------
--          Implementations
--------------------------------------------------------------------------------

unsafeRefl : a === b
unsafeRefl = believe_me (Refl {x = a})

export
Ring Bits8 where
  plusAssociative     = unsafeRefl
  plusCommutative     = unsafeRefl
  plusZeroLeftNeutral = unsafeRefl
  plusNegLeftZero     = unsafeRefl
  multAssociative     = unsafeRefl
  multCommutative     = unsafeRefl
  multOneLeftNeutral  = unsafeRefl
  leftDistributive    = unsafeRefl
  minusIsPlusNeg      = unsafeRefl

export
Ring Bits16 where
  plusAssociative     = unsafeRefl
  plusCommutative     = unsafeRefl
  plusZeroLeftNeutral = unsafeRefl
  plusNegLeftZero     = unsafeRefl
  multAssociative     = unsafeRefl
  multCommutative     = unsafeRefl
  multOneLeftNeutral  = unsafeRefl
  leftDistributive    = unsafeRefl
  minusIsPlusNeg      = unsafeRefl

export
Ring Bits32 where
  plusAssociative     = unsafeRefl
  plusCommutative     = unsafeRefl
  plusZeroLeftNeutral = unsafeRefl
  plusNegLeftZero     = unsafeRefl
  multAssociative     = unsafeRefl
  multCommutative     = unsafeRefl
  multOneLeftNeutral  = unsafeRefl
  leftDistributive    = unsafeRefl
  minusIsPlusNeg      = unsafeRefl

export
Ring Bits64 where
  plusAssociative     = unsafeRefl
  plusCommutative     = unsafeRefl
  plusZeroLeftNeutral = unsafeRefl
  plusNegLeftZero     = unsafeRefl
  multAssociative     = unsafeRefl
  multCommutative     = unsafeRefl
  multOneLeftNeutral  = unsafeRefl
  leftDistributive    = unsafeRefl
  minusIsPlusNeg      = unsafeRefl

export
Ring Int8 where
  plusAssociative     = unsafeRefl
  plusCommutative     = unsafeRefl
  plusZeroLeftNeutral = unsafeRefl
  plusNegLeftZero     = unsafeRefl
  multAssociative     = unsafeRefl
  multCommutative     = unsafeRefl
  multOneLeftNeutral  = unsafeRefl
  leftDistributive    = unsafeRefl
  minusIsPlusNeg      = unsafeRefl

export
Ring Int16 where
  plusAssociative     = unsafeRefl
  plusCommutative     = unsafeRefl
  plusZeroLeftNeutral = unsafeRefl
  plusNegLeftZero     = unsafeRefl
  multAssociative     = unsafeRefl
  multCommutative     = unsafeRefl
  multOneLeftNeutral  = unsafeRefl
  leftDistributive    = unsafeRefl
  minusIsPlusNeg      = unsafeRefl

export
Ring Int32 where
  plusAssociative     = unsafeRefl
  plusCommutative     = unsafeRefl
  plusZeroLeftNeutral = unsafeRefl
  plusNegLeftZero     = unsafeRefl
  multAssociative     = unsafeRefl
  multCommutative     = unsafeRefl
  multOneLeftNeutral  = unsafeRefl
  leftDistributive    = unsafeRefl
  minusIsPlusNeg      = unsafeRefl

export
Ring Int64 where
  plusAssociative     = unsafeRefl
  plusCommutative     = unsafeRefl
  plusZeroLeftNeutral = unsafeRefl
  plusNegLeftZero     = unsafeRefl
  multAssociative     = unsafeRefl
  multCommutative     = unsafeRefl
  multOneLeftNeutral  = unsafeRefl
  leftDistributive    = unsafeRefl
  minusIsPlusNeg      = unsafeRefl

export
Ring Int where
  plusAssociative     = unsafeRefl
  plusCommutative     = unsafeRefl
  plusZeroLeftNeutral = unsafeRefl
  plusNegLeftZero     = unsafeRefl
  multAssociative     = unsafeRefl
  multCommutative     = unsafeRefl
  multOneLeftNeutral  = unsafeRefl
  leftDistributive    = unsafeRefl
  minusIsPlusNeg      = unsafeRefl

export
Ring Integer where
  plusAssociative     = unsafeRefl
  plusCommutative     = unsafeRefl
  plusZeroLeftNeutral = unsafeRefl
  plusNegLeftZero     = unsafeRefl
  multAssociative     = unsafeRefl
  multCommutative     = unsafeRefl
  multOneLeftNeutral  = unsafeRefl
  leftDistributive    = unsafeRefl
  minusIsPlusNeg      = unsafeRefl


text:
data MyMaybe : (0 x : Type) -> Type where
  MyNothing : MyMaybe a
  MyJust : a -> MyMaybe a

-- Should fail since type argument is deleted
nameOf : Type -> String
nameOf (MyMaybe Bool) = "MyMaybe Bool"
nameOf (MyMaybe Int) = "MyMaybe Int"
nameOf _ = "Unknown"

main : IO ()
main = do
  putStrLn (nameOf (MyMaybe Bool))
  putStrLn (nameOf (MyMaybe Int))
  putStrLn (nameOf Int)


text:
module OrgReader

import System

import TestRunner
import ParsingTest

import Edda.Model
import Edda.Reader.Org

-- ------------------------------------------------------------------- [ Tests ]

test1 : Test
test1 = do
  parseTestGood (attribute "TITLE")  "#+TITLE: I am a Title\n\n"
  parseTestGood (attribute "AUTHOR") "#+AUTHOR: I am an Author\n\n"
  parseTestGood (attribute "DATE")   "#+DATE: I is a date\n\n"

test2 : Test
test2 = parseTestGood (many block) $ "#+CAPTION: sdsd\n#+NAME: asas:asasre\n#+BEGIN_THEOREM\n sdsdsdsd\n#+END_THEOREM"
        ++ "\n#+CAPTION: sdsd\n#+NAME: asas:asasre\n#+BEGIN_COROLLARY\n sdsdsdsd\n#+END_COROLLARY"
        ++ "\n#+CAPTION: sdsd\n#+NAME: asas:asasre\n#+BEGIN_LEMMA\n sdsdsdsd\n#+END_LEMMA"
        ++ "\n#+CAPTION: sdsd\n#+NAME: asas:asasre\n#+BEGIN_PROPOSITION\n sdsdsdsd\n#+END_PROPOSITION"
        ++ "\n#+CAPTION: sdsd\n#+NAME: asas:asasre\n#+BEGIN_PROOF\n sdsdsdsd\n#+END_PROOF"
        ++ "\n#+CAPTION: sdsd\n#+NAME: asas:asasre\n#+BEGIN_DEFINITION\n sdsdsdsd\n#+END_DEFINITION"
        ++ "\n#+CAPTION: sdsd\n#+NAME: asas:asasre\n#+BEGIN_EXAMPLE\n sdsdsdsd\n#+END_EXAMPLE"
        ++ "\n#+CAPTION: sdsd\n#+NAME: asas:asasre\n#+BEGIN_EXERCISE\n sdsdsdsd\n#+END_EXERCISE"
        ++ "\n#+CAPTION: sdsd\n#+NAME: asas:asasre\n#+BEGIN_NOTE\n sdsdsdsd\n#+END_NOTE"
        ++ "\n#+CAPTION: sdsd\n#+NAME: asas:asasre\n#+BEGIN_PROBLEM\n sdsdsdsd\n#+END_PROBLEM"
        ++ "\n#+CAPTION: sdsd\n#+NAME: asas:asasre\n#+BEGIN_QUESTION\n sdsdsdsd\n#+END_QUESTION"
        ++ "\n#+CAPTION: sdsd\n#+NAME: asas:asasre\n#+BEGIN_REMARK\n sdsdsdsd\n#+END_REMARK"
        ++ "\n#+CAPTION: sdsd\n#+NAME: asas:asasre\n#+BEGIN_SOLUTION\n sdsdsdsd\n#+END_SOLUTION\n"

test3 : Test
test3 = do
  parseTestGood (many header) "* Introduction\n\n** Contribution\n\n** Outline\n\n* Methodology\n\n** System\n\n** Procedure\n\n* Results\n\n* Discussion\n\n* Conclusion\n\n"
  parseTestGood (many block) $ "#+CAPTION: sdsd\n#+NAME: asas:asasre\n#+BEGIN_SRC idris\n sldkjf;sdjf;dlfj\n#+END_SRC\n\n"
        ++ "#+BEGIN_SRC idris\n sldkjf;sdjf;dlfj\n#+END_SRC\n\n"
  parseTestGood (block) "#+BEGIN_QUOTE\n dfkljfzdjf\n#+END_QUOTE\n\n"
  parseTestGood (block) "#+CAPTION: sdsd\n #+NAME: asas:asasre\n[[dfjkdjfldjkf]]\n\n"
  parseTestGood (many block)  $ "#+BEGIN_EQUATION\n dfdkfjlkjdfjlk\n#+END_EQUATION\n"
      ++ "#+NAME: asas\n#+BEGIN_EQUATION\n dfdkfjlkjdfjlk\n#+END_EQUATION\n\n"

test4 : Test
test4 = do
  parseTestGood (block) "+ a\n+ b\n+ c\n+ a\n+ b\n+ c\n- a\n- b\n- c\n"
  parseTestGood (block) "1. a\n1. b\n2. c\n3. a\n3. b\n1. c\n2. a\n2. b\n3. c\n"
  parseTestGood (block) "+ Term :: Description+ Term :: Description\n + Term :: Description\n + Term :: Description\n + Term :: Description\n + Term :: Description\n"

orgtests : List Test
orgtests = [test, test1, test2, test3, test4]


text:
module AssRecRule

import Data.Fin
import Data.Vect

%default total

{-
 The recursion function for lists of type `a`. Define this by pattern matching
-}
recList : (a: Type) ->  (x: Type) -> x -> (a -> List a -> x -> x) -> (List a -> x)
recList a x x0 f [] = x0
recList a x x0 f (head::lista) = f head lista (recList a x x0 f lista)
{-
Given a list of type `a` and a function `f: a -> b` get a list of type `b`
by applying `f` to each element.
Note: Define using `recList` and without pattern matching on lists.
-}
mapList : (a: Type) -> (b: Type) -> (f: a -> b) -> List a -> List b
mapList a b f lista = recList a (List b) [] (\a => (\lista => (\listb => (f a)::listb))) lista

{-
Given a list of type `a`, an initial value `init: a` and an operation `op: a -> a -> a`,
get an element of `a` by starting with init and repeatedly applying the elements of the
list,
e.g. fold Nat 1 (*) ([22] :: [3] :: [])  = 1 * 22 * 3
Note: Define using `recList` and without pattern matching on lists.
-}
foldList : (a: Type) ->  (init: a) -> (op : a -> a -> a) -> List a -> a
foldList a a0 op lista = recList a a a0 (\a => (\lista => (\val => op a val))) lista

{-
The induction function on the `Fin` indexed type family. Define this by pattern matching.
-}
inducFin : (xs : (n: Nat) -> Fin n -> Type) ->
  (base : (m: Nat) -> xs (S m) FZ) ->
  (step : (p: Nat) -> (k: Fin p) ->  (prev: xs p k) -> (xs (S p) (FS k))) ->
  (q: Nat) -> (j: Fin q) -> xs q j
inducFin xs base step (S n) FZ = base n
inducFin xs base step (S n) (FS k) = step n k (inducFin xs base step n k)

{-
Given a type `a`, a natural number `q`, an element `j : Fin q` and a vector `v` of length q with entries of type `a`,
get the element in position `j` of `v`. Note that this is always well defined.
Note: Define using `inducList` and without pattern matching on the `Fin` family. You may pattern match on Vectors.
-}

fetchElem : (a: Type) -> (q: Nat) -> (j: Fin q) -> (Vect q a -> a)
fetchElem a q j v = (inducFin xs base step q j) v where
	xs : (n: Nat) -> Fin n -> Type
	xs n k = (Vect n a -> a)
	base : (m: Nat) -> xs (S m) FZ
	base m (x :: v) = x
	step :  (p: Nat) -> (k: Fin p) ->  (prev: xs p k) -> (xs (S p) (FS k))
	step p k prev (x :: v) = prev v


text:
module Network.Curl.Types.SSL

import Network.Curl.Types.Code
import Util
import Derive.Enum
%language ElabReflection

data CurlSSLBackend
  = CURLSSLBACKEND_NONE -- 0,
  | CURLSSLBACKEND_OPENSSL -- 1,
  | CURLSSLBACKEND_GNUTLS -- 2,
  | CURLSSLBACKEND_NSS -- 3,
  | CURLSSLBACKEND_GSKIT -- 5,
  | CURLSSLBACKEND_POLARSSL -- 6, /* deprecated */
  | CURLSSLBACKEND_WOLFSSL -- 7,
  | CURLSSLBACKEND_SCHANNEL -- 8,
  | CURLSSLBACKEND_SECURETRANSPORT -- 9,
  | CURLSSLBACKEND_AXTLS -- 10, /* deprecated */
  | CURLSSLBACKEND_MBEDTLS -- 11,
  | CURLSSLBACKEND_MESALINK -- 12,
  | CURLSSLBACKEND_BEARSSL -- 13

Show CurlSSLBackend where
  show = showEnum

Eq CurlSSLBackend where
  (==) = eqEnum

Ord CurlSSLBackend where
  compare = compareEnum

ToCode CurlSSLBackend where
  toCode = enumTo [0,1,2,3, 5,6,7,8,9,10,11,12,13]

FromCode CurlSSLBackend where
  unsafeFromCode = unsafeEnumFrom [0,1,2,3, 5,6,7,8,9,10,11,12,13]
  fromCode = enumFrom [0,1,2,3, 5,6,7,8,9,10,11,12,13]

data CurlSSLSet
  = CURLSSLSET_OK -- = 0
  | CURLSSLSET_UNKNOWN_BACKEND
  | CURLSSLSET_TOO_LATE
  | CURLSSLSET_NO_BACKENDS

Show CurlSSLSet where
  show = showEnum

Eq CurlSSLSet where
  (==) = eqEnum

Ord CurlSSLSet where
  compare = compareEnum

ToCode CurlSSLSet where
  toCode = enumTo [0..3]

FromCode CurlSSLSet where
  unsafeFromCode = unsafeEnumFrom [0..3]
  fromCode = enumFrom [0..3]

{-
typedef struct {
  curl_sslbackend id;
  const char *name;
} curl_ssl_backend;
-}


text:
module Verified.Applicative.Vect

import Data.Vect
import Verified.Applicative
import Verified.Functor
import Verified.Functor.Vect

applicativeMap_Vect : (vs : Vect n a) -> (g : a -> b) -> map g vs = pure g <*> vs
applicativeMap_Vect []        g = Refl
applicativeMap_Vect (v :: vs) g = rewrite (applicativeMap_Vect vs g) in Refl

applicativeIdentity_Vect : (vs : Vect n a) -> pure id <*> vs = vs
applicativeIdentity_Vect []        = Refl
applicativeIdentity_Vect (x :: xs) = rewrite (applicativeIdentity_Vect xs) in Refl

applicativeInterchange_Vect : (x : a) -> (g : Vect n (a -> b)) -> g <*> pure x = pure (\g' => g' x) <*> g
applicativeInterchange_Vect x []        = Refl
applicativeInterchange_Vect x (f :: fs) = rewrite (applicativeInterchange_Vect x fs) in Refl

applicativeComposition_Vect : (xs : Vect n a) -> (g1 : Vect n (a -> b)) -> (g2 : Vect n (b -> c))
                           -> pure (.) <*> g2 <*> g1 <*> xs = g2 <*> (g1 <*> xs)
applicativeComposition_Vect []        []          []          = Refl
applicativeComposition_Vect (v :: vs) (g1 :: g1s) (g2 :: g2s) = rewrite (applicativeComposition_Vect vs g1s g2s) in Refl

applicativeHomomorphism_Vect : {n : Nat} -> (x : a) -> (g : a -> b)
                            -- pure g <*> pure x = pure (g x)
                            -> Vect.zipWith apply (Vect.replicate n g) (Vect.replicate n x) = Vect.replicate n (g x)
applicativeHomomorphism_Vect {n =    Z } x g = Refl
applicativeHomomorphism_Vect {n = (S k)} x g = rewrite (applicativeHomomorphism_Vect x g {n=k}) in Refl

instance VerifiedApplicative (Vect vlen) where
  applicativeMap = applicativeMap_Vect
  applicativeIdentity = applicativeIdentity_Vect
  applicativeInterchange = applicativeInterchange_Vect
  applicativeComposition = applicativeComposition_Vect
  applicativeHomomorphism = applicativeHomomorphism_Vect

max_stars_repo_name: yurrriq/idris-verified

max_issues_repo_name: yurrriq/idris-verified

max_forks_repo_name: yurrriq/idris-verified


text:
module Instances.ZZ

import public Data.ZZ
import Common.Util
import Common.Interfaces
import Specifications.OrderedGroup
import Specifications.DiscreteOrderedGroup
import Specifications.OrderedRing
import Symmetry.Abelian
import Instances.Notation
import public Instances.OrderZZ

%default total
%access public export

implementation Ringops ZZ where
  Zero = Pos 0
  One = Pos 1

zzMonoid : specifyMonoid {s = ZZ}
zzMonoid = MkMonoid plusAssociativeZ plusZeroLeftNeutralZ plusZeroRightNeutralZ

zzGroup : specifyGroup {s = ZZ}
zzGroup = MkGroup zzMonoid plusNegateInverseRZ plusNegateInverseLZ

zzPartialOrder : specifyPartialOrder {leq = LTEZ}
zzPartialOrder = MkPartialOrder lteReflZ lteTransitiveZ lteAntisymmetricZ

zzTotalOrder : specifyTotalOrder {leq = LTEZ}
zzTotalOrder = MkTotalOrder zzPartialOrder lteTotalZ

zzPartiallyOrderedMagma : specifyPartiallyOrderedMagma {leq = LTEZ}
zzPartiallyOrderedMagma = MkPartiallyOrderedMagma zzPartialOrder
  lteLeftTranslationInvariantZ $
  abelianTranslationInvariantLR plusCommutativeZ lteLeftTranslationInvariantZ

zzPartiallyOrderedGroup : specifyPartiallyOrderedGroup {leq = LTEZ}
zzPartiallyOrderedGroup = MkPartiallyOrderedGroup zzGroup
  zzPartiallyOrderedMagma

zzOrderedGroup : specifyOrderedGroup {leq = LTEZ}
zzOrderedGroup = MkOrderedGroup zzPartiallyOrderedGroup lteTotalZ

zzDiscreteOrderedGroup : specifyDiscreteOrderedGroup {leq = LTEZ}
zzDiscreteOrderedGroup = MkDiscreteOrderedGroup zzOrderedGroup
  plusCommutativeZ lteDiscreteZ

zzRing : specifyRing {s = ZZ}
zzRing = MkRing
  (MkPreRing
    multDistributesOverPlusRightZ
    multDistributesOverPlusLeftZ
    plusCommutativeZ)
  zzGroup
  multAssociativeZ

zzOrderedRing : specifyOrderedRing {leq = LTEZ}
zzOrderedRing = MkOrderedRing
  (MkPartiallyOrderedRing zzRing zzPartiallyOrderedMagma)
  lteTotalZ

zzDiscreteOrderedRing : specifyDiscreteOrderedRing {leq = LTEZ}
zzDiscreteOrderedRing = MkDiscreteOrderedRing zzOrderedRing
  lteDiscreteZ multOneLeftNeutralZ multOneRightNeutralZ (LtePosPos LTEZero)

max_stars_repo_name: jeroennoels/verified-algebra

max_issues_repo_name: jeroennoels/verified-algebra

max_forks_repo_name: jeroennoels/verified-algebra


text:
say : (s:String) -> { auto ok : (=) s "Hello World!"} -> IO ()
say s = printLn s

main : IO ()
main = say "Hello World!"

max_stars_repo_name: janschultecom/idris-examples

max_issues_repo_name: janschultecom/idris-examples

max_forks_repo_name: janschultecom/idris-examples


text:
module Algebra.Preorder

%default total

||| Preorder defines a binary relation using the `<=` operator
public export
interface Preorder a where
  (<=) : a -> a -> Bool
  preorderRefl : {x : a} -> x <= x = True
  preorderTrans : {x, y, z : a} -> x <= y = True -> y <= z = True -> x <= z = True

||| Least Upper Bound, replace max using only Preorder
export
lub : Preorder a => a -> a -> a
lub x y = if x <= y then y else x

||| Greatest Lower Bound, replaces min using only Preorder
export
glb : Preorder a => a -> a -> a
glb x y = if x <= y then x else y

||| Strict less-than using the relation from a preorder
public export
(<) : (Preorder a, Eq a) => a -> a -> Bool
(<) x y = x <= y && x /= y

||| The greatest bound of a bounded lattice, we only need to know about preorders however
public export
interface Preorder a => Top a where
  top : a
  topAbs : {x : a} -> x <= top = True


text:
module UIKit

data Alert = MkAlert Ptr

alert : String -> IO Ptr
alert s = mkForeign (FFun "UIAlertView.alloc().initWithTitle_message_delegate_cancelButtonTitle_otherButtonTitles_(%0, null, null, null, null)" [FString] FPtr) s

show : Ptr -> IO ()
show a = mkForeign (FFun "%0.show()" [FPtr] FUnit) a

max_stars_repo_name: joshvera/idris-objc-demo

max_issues_repo_name: joshvera/idris-objc-demo

max_forks_repo_name: joshvera/idris-objc-demo


text:
module Replica.App.Info

import Control.ANSI
import Control.App
import Control.App.Console

import Data.List
import Data.List1
import Data.String

import Language.JSON

import Replica.App.FileSystem
import Replica.App.Format
import Replica.App.Log
import Replica.App.Replica
import Replica.Command.Info
import Replica.Core
import Replica.Option.Filter
import Replica.Option.Global
import Replica.Other.Decorated
import Replica.Other.String
import Replica.Other.Validation

data InfoContext : Type where

displayTestName : Console e =>
  State GlobalConfig Global e =>
  String -> App e ()
displayTestName x = putStrLn $ "\{!qmark} " ++ (!bold "\{x}:")

displayExpectation : FileSystem (FSError :: e) =>
  Has [ State InfoContext InfoCommand
      , State GlobalConfig Global
      , State CurrentTest Test
      , Console] e => App e ()
displayExpectation = do
  t <- get CurrentTest
  handle (readFile !getExpectedFile)
    (\o => do putStrLn $ withOffset 4 $ "Expected:"
              putStrLn !(expectation o))
    (\err : FSError => putStrLn "No expectation yet.")
  where
    expectation : String -> App e String
    expectation o =
      pure . unlines . map (!blue . withOffset 6) . forget $ lines o

filterTests : FileSystem (FSError :: e) =>
  Has [ State InfoContext InfoCommand
      , State GlobalConfig Global
      , Exception ReplicaError
      , Console
      ] e => (s : List Test) -> App e (List Test)
filterTests s = do
  f <- filter <$> get InfoContext
  debug $ "Filters: \{show f}"
  pure $ filter (keepTest f) s

getLastFailures : FileSystem (FSError :: e) =>
  Has [ State GlobalConfig Global
      , Exception ReplicaError
      , Console
      ] e => App e (List Test)
getLastFailures = do
  repl <- getReplica
  logFile <- lastRunLog <$> getReplicaDir
  lastLog <- catchNew (readFile logFile)
    (\err : FSError => throw $ CantAccessTestFile logFile)
  let Just json = parse lastLog
    | Nothing => throw $ InvalidJSON []
  let Valid report = parseReport json
    | Error err => throw $ InvalidJSON err
  let notWorking = fst <$> filter (not . isFullSuccess . snd) report
  pure $ filter (flip elem notWorking . name) repl.tests

defineActiveTests : FileSystem (FSError :: e) =>
  Has [ State InfoContext InfoCommand
      , State GlobalConfig Global
      , Exception ReplicaError
      , Console
      ] e => App e (List Test)
defineActiveTests = do
  last <- if !((.filter.lastFailures) <$> get InfoContext)
        then getLastFailures
        else do
          repl <- getReplica
          pure repl.tests
  filterTests last

displayTests : FileSystem (FSError :: e) =>
  Has [ State InfoContext InfoCommand
      , State GlobalConfig Global
      , State CurrentTest Test
      , Console] e =>
  App e ()
displayTests = do
  t <- get CurrentTest
  displayTestName t.name
  traverse_ (putStrLn . withOffset 4) t.description
  when (not $ null t.tags)
    $ putStrLn . withOffset 4 $ "Tags: \{show t.tags}"
  when (not $ null t.require)
    $ putStrLn . withOffset 4 $ "Require: \{show t.require}"
  putStrLn $ withOffset 4 "Command : \{show t.command}"
  when !(showExpectation <$> get InfoContext)
    displayExpectation
  putStrLn ""

export
infoReplica :
  FileSystem (FSError :: e) =>
  Has
    [ State InfoContext InfoCommand
    , State GlobalConfig Global
    , Exception ReplicaError
    , Console
    ] e => App e ()
infoReplica = do
  debug $ "Info: \{show !(get InfoContext)}"
  debug $ show !(get GlobalConfig)
  putStrLn ""
  tests <- defineActiveTests
  traverse_ (\t => new t displayTests) tests

max_stars_repo_name: teto/REPLica

max_issues_repo_name: teto/REPLica

max_forks_repo_name: teto/REPLica


text:
module Compiler.Codegen.Rapid

import Data.List
import Data.String
import System
import System.File

import Core.Directory
import Core.CompileExpr
import Core.Context
import Core.Options
import Compiler.Common
import Compiler.VMCode
import Libraries.Utils.Path

import Rapid.Driver

isFgn : (Name, a, NamedDef) -> Bool
isFgn (_, _, (MkNmForeign _ _ _)) = True
isFgn _ = False

shell : List String -> String
shell args = showSep " " $ map shellQuote args
  where
    shellQuote : String -> String
    shellQuote s = s

runShell : List String -> IO ()
runShell args = do
  let cmd = shell args
  ignore $ fPutStrLn stderr $ "+" ++ cmd
  rc <- system cmd
  case rc of
       0 => pure ()
       err_rc => do putStrLn $ "command failed with exit code " ++ show err_rc
                    exitFailure

globalizeStackmap : String -> IO Bool
globalizeStackmap fname = do
  (Right outFile) <- openFile fname Append
  | Left err => do putStrLn $ "error opening asm file: " ++ show err
                   pure False
  ignore $ fPutStr outFile "\n.globl __LLVM_StackMaps\n"
  ignore $ closeFile outFile
  pure True

getDebug : List String -> Bool
getDebug = any isDebug
  where
    isDebug : String -> Bool
    isDebug directive = (trim directive) == "debug"

compile : Ref Ctxt Defs -> (tmpDir : String) -> (outputDir : String) ->
        ClosedTerm -> (outfile : String) -> Core (Maybe String)
compile defs tmpDir outputDir term outfile = do
  let appDirRel = outfile ++ "_rapid" -- relative to build dir
  let appDirGen = outputDir </> appDirRel -- relative to here
  let outputFileName = appDirGen </> (outfile ++ ".ll") -- LLVM IR (text)
  let bcFileName = appDirGen </> (outfile ++ ".bc") -- optimized LLVM bitcode
  let asmFileName = appDirGen </> (outfile ++ ".s") -- compiled assembler
  let objectFileName = appDirGen </> (outfile ++ ".o") -- object file
  let binaryFileName = outputDir </> outfile
  coreLift_ $ mkdirAll appDirGen

  directives <- getDirectives (Other "llvm")
  let debug = getDebug directives
  coreLift_ $ fPutStrLn stderr ("debug: " ++ show debug)

  -- load supporting files first, so we can fail early
  support <- readDataFile $ "rapid" </> "support.ll"
  runtime <- findDataFile $ "rapid" </> "runtime.bc"
  platformLib <- findDataFile $ "rapid" </> "platform.a"
  rapidLLVMPlugin <- findDataFile $ "rapid" </> "librapid.so"

  cd <- getCompileData False VMCode term
  coreLift_ $ fPutStrLn stderr $ "got compiledata"
  let foreigns = map (\(n,_,d) => (n,d)) $ filter isFgn $ namedDefs cd
  let allFunctions = vmcode cd
  let optFlags = [
    "-mem2reg", "-constprop", "-constmerge", "-sccp", "-dce", "-globaldce",
    "-rewrite-statepoints-for-gc"]

  coreLift_ $ writeIR allFunctions foreigns support outputFileName debug

  let lateTransformFlags = ["-rapid-lower"]
  coreLift $ do
    runShell $ ["opt", outputFileName, "-load=" ++ rapidLLVMPlugin] ++ optFlags ++ lateTransformFlags ++ ["-o=" ++ bcFileName]
    runShell ["llc", "--frame-pointer=all", "-tailcallopt", "-o=" ++ asmFileName, bcFileName]
    True <- globalizeStackmap asmFileName
    | False => putStrLn "error"
    runShell ["clang", "-c", "-o", objectFileName, asmFileName]
    runShell ["clang", "-pthread", "-o", binaryFileName, objectFileName, runtime, platformLib, "-lm", "-L/usr/local/lib", "-lgmp"]

    pure ()

  pure $ Nothing

execute : Ref Ctxt Defs -> (tmpDir : String) -> ClosedTerm -> Core ()
execute defs tmpDir term = do
  let tmpExecutableFile = "idris_tmp"
  ignore $ compile defs tmpDir tmpDir term tmpExecutableFile
  coreLift_ $ system (tmpDir </> tmpExecutableFile)
  pure ()

export
rapidCodegen : Codegen
rapidCodegen = MkCG compile execute

max_stars_repo_name: boxfire/rapid

max_issues_repo_name: boxfire/rapid

max_forks_repo_name: boxfire/rapid


text:
module Control.Comonad.Store.Interface

import Control.Comonad
import Control.Comonad.Env.Env
import Control.Comonad.Store.Store
import Control.Comonad.Traced.Traced
import Control.Comonad.Trans

%default total

public export
interface Comonad w => ComonadStore s w | w where
  pos : w a -> s

  peek : s -> w a -> a

  peeks : (s -> s) -> w a -> a
  peeks f w = peek (f (pos w)) w

  seek : s -> w a -> w a
  seek s = peek s . duplicate

  seeks : (s -> s) -> w a -> w a
  seeks f = peeks f . duplicate

  experiment : Functor f => (s -> f s) -> w a -> f a
  experiment f w = map (`peek` w) (f (pos w))

--------------------------------------------------------------------------------
--          Utilities
--------------------------------------------------------------------------------

public export %inline
lowerPos : (ComonadTrans t, ComonadStore s w) => t w a -> s
lowerPos = pos . lower

public export %inline
lowerPeek : (ComonadTrans t, ComonadStore s w) => s -> t w a -> a
lowerPeek s = peek s . lower

public export %inline
lowerExperiment :  (ComonadTrans t, ComonadStore s w, Functor f)
                => (s -> f s) -> t w a -> f a
lowerExperiment f = experiment f . lower

--------------------------------------------------------------------------------
--          Implementations
--------------------------------------------------------------------------------

public export %inline
ComonadStore s w => ComonadStore s (EnvT e w) where
  pos        = lowerPos
  peek       = lowerPeek
  experiment = lowerExperiment

public export %inline
Comonad w => ComonadStore s (StoreT s w) where
  pos                          = val
  peek s (MkStoreT run _)      = extract run s
  seek s                       = record { val = s }
  seeks f                      = record { val $= f }
  experiment f (MkStoreT wf s) = extract wf <$> f s

public export %inline
(ComonadStore s w, Monoid m) => ComonadStore s (TracedT m w) where
  pos        = lowerPos
  peek       = lowerPeek
  experiment = lowerExperiment


text:
module Data.Array

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

%access private
%default covering

-- conId : TTName -> Elab Int

data Prim_Array = Prim_MkArray

-- This creates an uninitialized array because it allocates, which would ruin any pointers to Idris values passed in.
prim_makeArray : Int -> IO Prim_Array
prim_makeArray len = do
  MkRaw arr <- foreign FFI_C "idris_makeArray" (Int -> IO (Raw Prim_Array)) len
  pure arr

prim_indexArray : Int -> Prim_Array -> IO a
prim_indexArray {a} ix arr = do
  MkRaw elem <- foreign FFI_C "idris_indexArray" (Int -> Raw Prim_Array -> IO (Raw a)) ix (MkRaw arr)
  pure elem

prim_setAtArray : Int -> a -> Prim_Array -> IO ()
prim_setAtArray {a} ix elem arr =
  foreign FFI_C "idris_setAtArray" (Int -> Raw a -> Raw (Prim_Array) -> IO ()) ix (MkRaw elem) (MkRaw arr)

-- ###

%access export

namespace IOArray
  data IOArray : Type -> Type where
    MkIOArray : (len : Int) -> (prim_Array : Prim_Array) -> IOArray a

  %used MkIOArray prim_Array

  length : IOArray a -> Int
  length (MkIOArray len parr) = len

  fromList : List a -> IO (IOArray a)
  fromList xs = do
    let len = cast $ length xs
    parr <- prim_makeArray len
    for_ {b = ()} (zip [0 .. len - 1] xs) $ \(ix, elem) => prim_setAtArray ix elem parr
    pure $ MkIOArray len parr

  index : Int -> IOArray a -> IO a
  index ix (MkIOArray len parr) = prim_indexArray ix parr

  setAt : Int -> a -> IOArray a -> IO ()
  setAt ix elem (MkIOArray len parr) = prim_setAtArray ix elem parr

max_stars_repo_name: idris-hackers/idris-array

max_issues_repo_name: idris-hackers/idris-array

max_forks_repo_name: idris-hackers/idris-array


text:
module Data.Profunctor.Interface

import Control.Category
import public Control.Applicative.Const
import public Control.Monad.Identity
import public Data.Morphisms

--------------------------------------------------------------------------------
--          Forget
--------------------------------------------------------------------------------

public export
record Forget (r : Type) (a : Type) (b : Type) where
  constructor MkForget
  fun : a -> Maybe r

public export
Functor (Forget r a) where
  map _ (MkForget fun) = MkForget fun

--------------------------------------------------------------------------------
--          Profunctor
--------------------------------------------------------------------------------

||| A `Profunctor` is a `Functor` from the pair category `(Type^op, Type)`
||| to `Type`.
|||
||| In other words, a `Profunctor` is a type constructor of two type
||| arguments, which is contravariant in its first argument and covariant
||| in its second argument.
|||
||| The `dimap` function can be used to map functions over both arguments
||| simultaneously.
|||
||| A straightforward example of a profunctor is the function arrow `(->)`
||| (represented by `Morphism`).
|||
||| Laws:
|||
||| - Identity: `dimap identity identity = identity`
||| - Composition: `dimap f1 g1 <<< dimap f2 g2 = dimap (f1 >>> f2) (g1 <<< g2)`
public export
interface (forall a . Functor (p a)) => Profunctor (0 p : Type -> Type -> Type) where
  dimap : (i2 -> i1) -> (o1 -> o2) -> p i1 o1 -> p i2 o2

||| Map a function over the (contravariant) first type argument only.
public export
clmap : Profunctor p => (i2 -> i1) -> p i1 o -> p i2 o
clmap f = dimap f id

||| Map a function over the (covariant) second type argument only.
public export
rmap : Profunctor p => (o1 -> o2) -> p i o1 -> p i o2
rmap = dimap id

||| Lift a pure function into any `Profunctor` which is also a `Category`.
public export
arr : Category p => Profunctor p => (a -> b) -> p a b
arr f = rmap f id

--------------------------------------------------------------------------------
--          Implementations
--------------------------------------------------------------------------------

public export
Profunctor Morphism where
  dimap f g (Mor fun) = Mor $ g . fun . f

public export
Profunctor (Forget r) where
  dimap f _ (MkForget fun) = MkForget (fun . f)

public export
Functor m => Profunctor (Kleislimorphism m) where
  dimap f g (Kleisli fun) = Kleisli (map g . fun . f)


text:
module Keys

%default total
%access public

data Digit = Zero | One | Two | Three | Four
           | Five | Six | Seven | Eight | Nine

%name Digit digit

instance Eq Digit where
  Zero == Zero = True
  One == One = True
  Two == Two = True
  Three == Three = True
  Four == Four = True
  Five == Five = True
  Six == Six = True
  Seven == Seven = True
  Eight == Eight = True
  Nine == Nine = True
  _ == _ = False

instance Cast Digit Nat where
  cast Zero = 0
  cast One = 1
  cast Two = 2
  cast Three = 3
  cast Four = 4
  cast Five = 5
  cast Six = 6
  cast Seven = 7
  cast Eight = 8
  cast Nine = 9

data Key = DigitKey Digit
         | A | B | C | D | E | F | G | H | I | J | K | L | M
         | N | O | P | Q | R | S | T | U | V | W | X | Y | Z
         | Backtick
         | Dash
         | EqualSign
         | OpenSquareBracket | CloseSquareBracket
         | Slash | Backslash
         | Tab
         | Semicolon
         | SingleQuote
         | Comma | Period
         | F1 | F2 | F3 | F4 | F5 | F6 | F7 | F8 | F9 | F10 | F11 | F12
         | Escape
         | Insert
         | Delete
         | Backspace
         | Home | End
         | PageUp | PageDown
         | Enter

%name Key key

instance Eq Key where
  (DigitKey x) == (DigitKey y) = x == y
  A == A = True
  B == B = True
  C == C = True
  D == D = True
  E == E = True
  F == F = True
  G == G = True
  H == H = True
  I == I = True
  J == J = True
  K == K = True
  L == L = True
  M == M = True
  N == N = True
  O == O = True
  P == P = True
  Q == Q = True
  R == R = True
  S == S = True
  T == T = True
  U == U = True
  V == V = True
  W == W = True
  X == X = True
  Y == Y = True
  Z == Z = True
  Backtick == Backtick = True
  Dash == Dash = True
  EqualSign == EqualSign = True
  OpenSquareBracket == OpenSquareBracket = True
  CloseSquareBracket == CloseSquareBracket = True
  Slash == Slash = True
  Backslash == Backslash = True
  Tab == Tab = True
  Semicolon == Semicolon = True
  SingleQuote == SingleQuote = True
  Comma == Comma = True
  Period == Period = True
  F1 == F1 = True
  F2 == F2 = True
  F3 == F3 = True
  F4 == F4 = True
  F5 == F5 = True
  F6 == F6 = True
  F7 == F7 = True
  F8 == F8 = True
  F9 == F9 = True
  F10 == F10 = True
  F11 == F11 = True
  F12 == F12 = True
  Escape == Escape = True
  Insert == Insert = True
  Delete == Delete = True
  Backspace == Backspace = True
  Home == Home = True
  End == End = True
  PageUp == PageUp = True
  PageDown == PageDown = True
  Enter == Enter = True
  _ == _ = False

isDigitKey : Key -> Bool
isDigitKey (DigitKey _) = True
isDigitKey _ = False

-- Aliases for readability
Shift : Bool
Shift = True

NoShift : Bool
NoShift = False

record KeyChord where
  constructor KC
  key : Key
  shift : Bool
  alt : Bool
  ctrl : Bool
  fn : Bool
  super : Bool

%name KeyChord keyc

unmod : Key -> KeyChord
unmod key = KC key NoShift False False False False

shifted : Key -> KeyChord
shifted key = record { shift = Shift } $ unmod key

isUnmod : KeyChord -> Bool
isUnmod (KC _ False False False False False) = True
isUnmod _ = False

isDigit : KeyChord -> Bool
isDigit keyc = (isDigitKey . key) keyc && isUnmod keyc

toDigit : KeyChord -> Maybe Digit
toDigit (KC (DigitKey digit) NoShift _ _ _ _) = Just digit
toDigit _ = Nothing

toKey : Char -> Maybe KeyChord
toKey 'a' = Just $ unmod A
toKey 'b' = Just $ unmod B
toKey 'c' = Just $ unmod C
toKey 'd' = Just $ unmod D
toKey 'e' = Just $ unmod E
toKey 'f' = Just $ unmod F
toKey 'g' = Just $ unmod G
toKey 'h' = Just $ unmod H
toKey 'i' = Just $ unmod I
toKey 'j' = Just $ unmod J
toKey 'k' = Just $ unmod K
toKey 'l' = Just $ unmod L
toKey 'm' = Just $ unmod M
toKey 'n' = Just $ unmod N
toKey 'o' = Just $ unmod O
toKey 'p' = Just $ unmod P
toKey 'q' = Just $ unmod Q
toKey 'r' = Just $ unmod R
toKey 's' = Just $ unmod S
toKey 't' = Just $ unmod T
toKey 'u' = Just $ unmod U
toKey 'v' = Just $ unmod V
toKey 'w' = Just $ unmod W
toKey 'x' = Just $ unmod X
toKey 'y' = Just $ unmod Y
toKey 'z' = Just $ unmod Z
toKey 'A' = Just $ shifted A
toKey 'B' = Just $ shifted B
toKey 'C' = Just $ shifted C
toKey 'D' = Just $ shifted D
toKey 'E' = Just $ shifted E
toKey 'F' = Just $ shifted F
toKey 'G' = Just $ shifted G
toKey 'H' = Just $ shifted H
toKey 'I' = Just $ shifted I
toKey 'J' = Just $ shifted J
toKey 'K' = Just $ shifted K
toKey 'L' = Just $ shifted L
toKey 'M' = Just $ shifted M
toKey 'N' = Just $ shifted N
toKey 'O' = Just $ shifted O
toKey 'P' = Just $ shifted P
toKey 'Q' = Just $ shifted Q
toKey 'R' = Just $ shifted R
toKey 'S' = Just $ shifted S
toKey 'T' = Just $ shifted T
toKey 'U' = Just $ shifted U
toKey 'V' = Just $ shifted V
toKey 'W' = Just $ shifted W
toKey 'X' = Just $ shifted X
toKey 'Y' = Just $ shifted Y
toKey 'Z' = Just $ shifted Z
toKey _ = Nothing

toKeys : String -> List KeyChord
toKeys = catMaybes . map toKey . unpack


text:
||| Implementation of ordering relations for the primitive type `Int`
||| This is full of tricks as `Int` is a primitive type that can only
||| be interacted with using either literals or built-in functions.
||| The exported interface should however be safe.
module Data.Int.Order

import Data.Order

%default total

------------------------------------------------------------------------
-- Introduction

-- The type `Int` is a primitive type in Idris. The only handle we have on
-- it is provided by built-in functions. This is what we are going to use
-- to define relations on Int values. For instance, we will declare that
-- `a` is strictly less than `b` whenever `a < b` is provably equal to `True`.

-- These built-in functions only reduce on literals. This means we will not
-- be able to rely on their computational behaviour to prove statements in
-- open contexts.

-- For instance, no amount of pattern-matching will help us prove:
-- LT_not_EQ : LT a b -> Not (EQ a b)

-- Our solution in this file is to use unsafe primitives to manufacture such
-- proofs. This means we are going to essentially postulate some *conditional*
-- results. We do not want such conditional results to reduce to canonical
-- forms too eagerly.

-- Indeed the statement `GT 0 1 -> EQ 0 1` should be provable because 0 is not
-- greater than 1. But its proof should not reduce to a constant function
-- returning the value `Refl` because it is not true that `0` and `1` can be
-- unified. If the proof were to behave this way, we could, in an absurd context,
-- coerce values from any type to any other and cause segmentation faults.

-- Our solution is to be extremely wary of proofs that are passed to us
-- and to only consider returning a magically-crafted output if we have
-- managed to observe that the input is itself in canonical form i.e. to
-- have evaluation stuck on open terms.

-- This is the purpose of the `strictX : X -> Lazy c -> c` functions defined in
-- this file. They all will be waiting until their first argument is in canonical
-- form before returning their second.

------------------------------------------------------------------------
-- Utility functions for equality

||| Pattern-match on an equality proof so that the second argument to
||| strictRefl is only returned once the first is canonical.
export
strictRefl : a === b -> Lazy c -> c
strictRefl Refl p = p

||| Do NOT re-export
unsafeRefl : {0 a, b : t} -> a === b
unsafeRefl = believe_me (the (a === a) Refl)

------------------------------------------------------------------------
-- LT

namespace LT

  ||| `LT a b` is a proof that `a` is less than `b` which is to say that
  ||| the function call `a < b` returns `True`.
  |||
  ||| NB: we do not re-export the constructor so that users cannot force
  ||| our magic functions to blow up in absurd contexts by bypassing the
  ||| safety measures introduced by the `strictX` functions.
  ||| We do provide functions corresponding to the wrapping and unwrapping
  ||| of `LT` but, crucially, they do not let people force `LT` proofs to
  ||| be in canonical form.
  export
  data LT : Int -> Int -> Type where
    MkLT : (a < b) === True -> LT a b

  ||| We may prove `LT a b` by using a proof that `a < b` returns `True`.
  export
  mkLT : (a < b) === True -> LT a b
  mkLT = MkLT

  ||| From a proof that `LT a b`, we may concluded that `a < b` returns `True`.
  export
  runLT : LT a b -> (a < b) === True
  runLT (MkLT eq) = eq

  ||| Do not trust arbitrary `LT` proofs when manufacturing magic ones:
  ||| be strict!
  export
  strictLT : LT a b -> Lazy c -> c
  strictLT (MkLT p) c = strictRefl p c

  ||| LT is decidable, by virtue of being the reflection of a boolean function
  export
  decide : (a, b : Int) -> Dec (LT a b)
  decide a b with (the (test : Bool ** (a < b) === test) (a < b ** Refl))
    decide a b | (True ** p) = Yes (MkLT p)
    decide a b | (False ** p) = No (\ (MkLT q) => absurd (trans (sym p) q))

  ||| LT is a transitive relation. This cannot be proven so we use a magic trick.
  export
  trans : LT a b -> LT b c -> LT a (the Int c)
  trans p q = strictLT p $ strictLT q $ MkLT unsafeRefl

  ||| LT is an irreflexive relation.
  ||| The crash will never happen because the `LT a a` argument will never reduce
  ||| to a canonical form (unless the built-in function (<) is buggy).
  export
  irrefl : Not (LT a a)
  irrefl p = strictLT p
           $ assert_total $ idris_crash "IMPOSSIBLE: LT is irreflexive"

------------------------------------------------------------------------
-- GT

||| GT is defined in terms of LT to avoid code duplication
public export
GT : Int -> Int -> Type
GT = flip LT

export
LT_not_GT : LT a b -> Not (GT a b)
LT_not_GT p q = irrefl (trans p q)

export
GT_not_LT : GT a b -> Not (LT a b)
GT_not_LT = flip LT_not_GT

------------------------------------------------------------------------
-- EQ

namespace EQ

  ||| `EQ a b` is a proof that `a` is equal to `b` which is to say that
  ||| the function call `a == b` returns `True`.
  |||
  ||| NB: we do not re-export the constructor so that users cannot force
  ||| our magic functions to blow up in absurd contexts by bypassing the
  ||| safety measures introduced by the `strictX` functions.
  ||| We do provide functions corresponding to the wrapping and unwrapping
  ||| of `EQ` but, crucially, they do not let people force `EQ` proofs to
  ||| be in canonical form.
  export
  data EQ : Int -> Int -> Type where
    MkEQ : (a == b) === True -> EQ a b

  ||| We may prove `EQ a b` by using a proof that `a == b` returns `True`.
  export
  mkEQ : (a == b) === True -> EQ a b
  mkEQ = MkEQ

  ||| From a proof that `EQ a b`, we may concluded that `a == b` returns `True`.
  export
  runEQ : EQ a b -> (a == b) === True
  runEQ (MkEQ eq) = eq

  ||| Do not trust arbitrary `EQ` proofs when manufacturing magic ones:
  ||| be strict!
  export
  strictEQ : EQ a b -> Lazy c -> c
  strictEQ (MkEQ p) c = strictRefl p c

  ||| EQ is decidable, by virtue of being the reflection of a boolean function
  export
  decide : (a, b : Int) -> Dec (EQ a b)
  decide a b with (the (test : Bool ** (a == b) === test) (a == b ** Refl))
    decide a b | (True  ** p) = Yes (MkEQ p)
    decide a b | (False ** p) = No (\ (MkEQ q) => absurd (trans (sym p) q))

  ||| EQ is a reflexive relation
  export
  refl : EQ a a
  refl = MkEQ unsafeRefl

  ||| EQ is substitutive
  export
  elimEQ : (0 p : Int -> Type) -> EQ a b -> p a -> p b
  elimEQ _ p v = strictEQ p $ believe_me v

  ||| EQ implies propositional equality
  export
  reflect : EQ a b -> a === b
  reflect p = elimEQ (\ b => a === b) p Refl

  ||| EQ is a symmetric relation
  export
  sym : EQ a b -> EQ b a
  sym p = elimEQ (\ b => EQ b a) p refl

  ||| EQ is a transitive relation
  export
  trans : EQ a b -> EQ b c -> EQ a c
  trans p q = elimEQ (\ b => EQ b c) (sym p) q

export
trans_LT_EQ : LT a b -> EQ b c -> LT a c
trans_LT_EQ p q = elimEQ (LT a) q p

export
trans_EQ_LT : EQ a b -> LT b c -> LT a c
trans_EQ_LT p q = elimEQ (\ b => LT b c) (sym p) q

export
LT_not_EQ : LT a b -> Not (EQ a b)
LT_not_EQ p q = irrefl (trans_LT_EQ p (sym q))

export
EQ_not_LT : EQ a b -> Not (LT a b)
EQ_not_LT = flip LT_not_EQ

export
EQ_not_GT : EQ a b -> Not (GT a b)
EQ_not_GT = EQ_not_LT . sym

export
GT_not_EQ : GT a b -> Not (EQ a b)
GT_not_EQ = flip EQ_not_GT

------------------------------------------------------------------------
-- LTE

namespace LTE

  ||| `LTE a b` is a proof that `a` is less or equal to `b` which is to say that
  ||| the function call `a < b` or `a == b` returns `True`.
  |||
  ||| NB: we do not re-export the constructor so that users cannot force
  ||| our magic functions to blow up in absurd contexts by bypassing the
  ||| safety measures introduced by the `strictX` functions.
  export
  data LTE : Int -> Int -> Type where
    MkLT : (a < b)  === True -> LTE a b
    MkEQ : (a == b) === True -> LTE a b

  ||| Unwrap an LTE proof to get either an LT or an EQ one
  export
  runLTE : LTE a b -> Either (LT a b) (EQ a b)
  runLTE (MkLT p) = Left (mkLT p)
  runLTE (MkEQ p) = Right (mkEQ p)

  ||| Do not trust arbitrary `LTE` proofs when manufacturing magic ones:
  ||| be strict!
  export
  strictLTE : LTE a b -> Lazy c -> c
  strictLTE (MkLT p) q = strictRefl p q
  strictLTE (MkEQ p) q = strictRefl p q

  ||| LTE is decidable by virture of both LT and EQ being decidable
  export
  decide : (a, b : Int) -> Dec (LTE a b)
  decide a b with (LT.decide a b)
    decide a b | Yes p = Yes (MkLT (runLT p))
    decide a b | No notLT with (EQ.decide a b)
      decide a b | No notLT | Yes p = Yes (MkEQ (runEQ p))
      decide a b | No notLT | No notEQ = No $ \ case
        MkLT p => notLT (mkLT p)
        MkEQ p => notEQ (mkEQ p)

  ||| LTE is a reflexive relation
  export
  refl : LTE a a
  refl = MkEQ unsafeRefl

  export
  trans_LT_LTE : LT a b -> LTE b c -> LT a c
  trans_LT_LTE p (MkLT q) = trans p (mkLT q)
  trans_LT_LTE p (MkEQ q) = trans_LT_EQ p (mkEQ q)

  export
  trans_LTE_LT : LTE a b -> LT b c -> LT a c
  trans_LTE_LT (MkLT p) q = trans (mkLT p) q
  trans_LTE_LT (MkEQ p) q = trans_EQ_LT (mkEQ p) q

  export
  inject_LT_LTE : LT a b -> LTE a b
  inject_LT_LTE = MkLT . runLT

  export
  inject_EQ_LTE : EQ a b -> LTE a b
  inject_EQ_LTE p = MkEQ (runEQ p)

  ||| LTE is a transitive relation
  export
  trans : LTE a b -> LTE b c -> LTE a c
  trans (MkLT p) q = inject_LT_LTE (trans_LT_LTE (mkLT p) q)
  trans p (MkLT q) = inject_LT_LTE (trans_LTE_LT p (mkLT q))
  trans (MkEQ p) (MkEQ q) = inject_EQ_LTE (trans (mkEQ p) (mkEQ q))

  ||| LTE is an antisymmetric relation
  export
  antisym : LTE a b -> LTE b a -> EQ a b
  antisym (MkEQ p) _ = mkEQ p
  antisym _ (MkEQ p) = EQ.sym (mkEQ p)
  antisym (MkLT p) (MkLT q) = absurd $ LT.irrefl (LT.trans (mkLT p) (mkLT q))

------------------------------------------------------------------------
-- GTE

||| GTE is defined in terms of LTE to avoid code duplication
public export
GTE : Int -> Int -> Type
GTE = flip LTE

------------------------------------------------------------------------
-- Trichotomy and other decidability results

||| Any pair of Ints is related either via LT, EQ, or GT
export
trichotomous : (a, b : Int) -> Trichotomous LT EQ GT a b
trichotomous a b with (LTE.decide a b)
  trichotomous a b | Yes lte = case runLTE lte of
    Left lt  => MkLT lt (LT_not_EQ lt) (LT_not_GT lt)
    Right eq => MkEQ (EQ_not_LT eq) eq (EQ_not_GT eq)
  trichotomous a b | No notLTE = let gt = mkLT unsafeRefl in MkGT (GT_not_LT gt) (GT_not_EQ gt) gt

||| Any pair of Ints is related either via LT or GTE
export
decide_LT_GTE : (a, b : Int) -> Either (LT a b) (GTE a b)
decide_LT_GTE a b with (trichotomous a b)
  decide_LT_GTE a b | MkLT lt _ _ = Left lt
  decide_LT_GTE a b | MkEQ _ eq _ = Right (inject_EQ_LTE (sym eq))
  decide_LT_GTE a b | MkGT _ _ gt = Right (inject_LT_LTE gt)

||| Any pair of Ints is related either via LTE or GT
export
decide_LTE_GT : (a, b : Int) -> Either (LTE a b) (GT a b)
decide_LTE_GT a b with (trichotomous a b)
  decide_LTE_GT a b | MkLT lt _ _ = Left (inject_LT_LTE lt)
  decide_LTE_GT a b | MkEQ _ eq _ = Left (inject_EQ_LTE eq)
  decide_LTE_GT a b | MkGT _ _ gt = Right gt

------------------------------------------------------------------------
-- Some properties

||| Adding one to a strictly smaller Int, yields a smaller Int
export
suc_LT_LTE : {a, b : Int} -> LT a b -> LTE (a + 1) b
suc_LT_LTE p with (the (test : Bool ** (a + 1 == b) === test) (a + 1 == b ** Refl))
  suc_LT_LTE p | (True  ** q) = inject_EQ_LTE $ mkEQ q
  suc_LT_LTE p | (False ** q) = strictLT p $ inject_LT_LTE $ mkLT unsafeRefl

||| Subtracting one to a strictly larger Int, yields a larger Int
export
pred_LT_LTE : {a, b : Int} -> LT a b -> LTE a (b - 1)
pred_LT_LTE p with (the (test : Bool ** (a == b - 1) === test) (a == b - 1 ** Refl))
  pred_LT_LTE p | (True  ** q) = inject_EQ_LTE $ mkEQ q
  pred_LT_LTE p | (False ** q) = strictLT p $ inject_LT_LTE $ mkLT unsafeRefl

||| Adding one to an Int yields a strictly larger one,
||| provided there is no overflow
export
sucBounded : LT a b -> LT a (a + 1)
sucBounded p = strictLT p $ mkLT unsafeRefl


text:
module Compiler.Erlang.Codegen.ErlExprToAbstractFormat.Binary

import Compiler.Erlang.IR.AbstractFormat
import Compiler.Erlang.Codegen.ErlExprToAbstractFormat.Internal

%default total

export
empty : Line -> Expr
empty l = AEBitstring l []

export
zeroPadded : Line -> (size : Expr) -> Expr
zeroPadded l size =
  let zero = AEBitstring l [MkBitSegment l (AELiteral (ALInteger l 0)) ABSDefault ABInteger]
  in genFunCall l "binary" "copy" [zero, size]

export
concat : Line -> Expr -> Expr -> Expr
concat l bin1 bin2 =
  AEBitstring l
    [ MkBitSegment l bin1 ABSDefault ABBinary
    , MkBitSegment l bin2 ABSDefault ABBinary
    ]


text:
-- ---------------------------------------------------------- [ TestRunner.idr ]
-- Module      : TestRunner
-- Description : Defines and runs test.x
--
-- Copyright   : (c) Jan de Muijnck-Hughes
-- License     : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
module TestRunner

import public Effects
import public Effect.StdIO
import public Effect.Exception

-- --------------------------------------------------- [ Type Sigs and Aliases ]
TestEffs : List EFFECT
TestEffs = [STDIO, EXCEPTION String]

Test : Type
Test = {TestEffs} Eff ()

-- ------------------------------------------------------------- [ Test Runner ]
tests : Nat -> List Test -> {TestEffs} Eff ()
tests _ Nil = do
    putStrLn "All tests passed"
    pure ()
tests n (t::ts) = do
    result <- t
    putStrLn $ "Test " ++ show n ++ " Passed"
    tests (S n) ts
-- --------------------------------------------------------------------- [ EOF ]


text:
--Applications of stuff in Primes.idr

module PrimeApple

import Primes
import NatUtils
import gcd
import Data.Fin
import NatOrder
import SriramAssRecRule

%access public export
%default total

--Prime type
isPrime : (p : Nat) -> LTE 2 p -> Type
isPrime p proofLTE = {k : Nat} -> isDivisible p k -> Either (k=1)(k=p)

--Transitivity of divisibility
transDiv : (isDivisible b a) -> (isDivisible c b) -> isDivisible c a
transDiv {a} {b} {c} (n ** pf1) (m ** pf2) = (m*n **
              (lteMultIsLTE (fst pf2) (fst pf1) ,
                rewrite (snd pf2) in
                rewrite (snd pf1) in
                rewrite sym (multAssociative a n m) in
                rewrite multCommutative n m in Refl))

--The smallest factor of a number is prime
leastDivIsPrime : (m : Nat) -> LTE 2 m ->
                  (p : Nat) -> (pGt2 : LTE 2 p) -> isDivisible m p ->
                  ((b : Nat) -> LTE b p -> (isDivisible m b) ->
                   Either (b=1)(b=p)) ->
                  isPrime p pGt2
leastDivIsPrime m mGt2 p pGt2 pDivm func = g where
  g : {k : Nat} -> isDivisible p k -> Either (k=1)(k=p)
  g {k = a} pff = func a (bDivAImpAGtB p a (fst pff) pff) (transDiv pff pDivm)

help10 : (a : Nat) -> (q : Nat) -> (S (S q)) = a ->
         (b : Nat) -> (k : Nat) -> (S (S k)) = b ->
         (prf : isDivisible a b) ->
         (lst : List Nat ** (foldList Nat 1 (*) lst = a,
           (b : NonEmpty lst ** (LTE 1 (last {ok=b} lst),
             (a = mult (head {ok=b} lst) (last {ok=b} lst),
             Either (x: LTE 2 (last {ok=b} lst) ** isPrime (last {ok=b} lst) x) (last {ok=b} lst = 1))))))
help10 a q ww b k ee prf with (prf)
    help10 a q ww b k ee prf | (m ** (pfPos , pfDiv)) =
        ([m , (S (S k))] ** (rewrite multOneRightNeutral (S k) in
                         rewrite ee in
                         rewrite multCommutative m b in (sym pfDiv),
                     (IsNonEmpty ** ((LTESucc LTEZero),
                        ((rewrite ee in
                        rewrite multCommutative m b in pfDiv),
                        Left (LTESucc (LTESucc LTEZero) **
                                leastDivIsPrime
                                (S (S q)) (LTESucc (LTESucc LTEZero))
                                (S (S k)) (LTESucc (LTESucc LTEZero))
                                (m ** (pfPos,
                                      rewrite ww in
                                      rewrite multConstantRight m ee in pfDiv))
                                (?func))
)))))

help11 : (x : Nat) -> (lst : List Nat) -> (ntMT : NonEmpty lst) ->
         last (x :: lst) = last {ok=ntMT} lst
help11 x (y :: xs) IsNonEmpty = Refl

--Factors a number into 2 other numbers, such that the
--first one is smaller and is prime (not proven yet)
--and that the list of factors folded gives back the number

--Give var as n-1
factor2 : (n : Nat) -> (var : Nat) -> (GT n 0) ->
          (lst : List Nat ** (foldList Nat 1 (*) lst = n,
            (b : NonEmpty lst ** (LTE 1 (last {ok=b} lst),
              (n = mult (head {ok=b} lst) (last {ok=b} lst),
                Either (x: LTE 2 (last {ok=b} lst) ** isPrime (last {ok=b} lst) x) (last {ok=b} lst = 1))))))
factor2 Z _ LTEZero impossible
factor2 Z _ (LTESucc _) impossible
factor2 (S Z) _ (LTESucc LTEZero) =
        ([1,1] ** (Refl, (IsNonEmpty **
                  ((LTESucc LTEZero), (Refl, Right Refl)))))
factor2 (S (S k)) Z (LTESucc LTEZero) = assert_unreachable
factor2 (S (S k)) (S Z) (LTESucc LTEZero) =
      ([(S (S k)), 1] **
       (rewrite multOneRightNeutral k in Refl,
       (IsNonEmpty ** ((LTESucc LTEZero),
          (rewrite multOneRightNeutral k in Refl, Right Refl)))))
factor2 (S (S k)) (S (S x)) (LTESucc LTEZero) =
    case decDiv (S (S k)) (LTESucc (LTESucc LTEZero)) (S (S x))
          {euc = eculidDivideAux (S (S k)) (S (S x)) (SIsNotZ)} of
     (Yes prf) => help10 (S (S k)) (k) Refl (S (S x)) (x) Refl prf
     (No contra) => factor2 (S (S k)) (S x) (LTESucc LTEZero)

--Factorises a number completely with proof of folding
factorise : (n : Nat) -> (GT n 0) ->
            (lst : List Nat ** (foldList Nat 1 (*) lst = n))
factorise Z LTEZero impossible
factorise Z (LTESucc _) impossible
factorise (S Z) (LTESucc LTEZero) = ([] ** Refl)
factorise (S (S k)) (LTESucc LTEZero) with
      (factor2 (S (S k)) (S k) (LTESucc LTEZero))
  factorise (S (S k)) (LTESucc LTEZero) |
        (lst ** (fol, (ntMT ** (lastLt, (pf2, primepf))))) = assert_total(
               (( (head {ok=ntMT} lst) ::
                  (fst (factorise (last {ok=ntMT} lst) lastLt))) **
                  (rewrite (snd (factorise (last {ok=ntMT} lst) lastLt))
                  in (sym pf2)) ))

-- creates a list with all the factors of a number upto the second argument
genFact : (n : Nat) -> Nat -> List (k : Nat ** isDivisible n k)
genFact Z Z = []
genFact Z (S k) = []
genFact (S j) Z = []
genFact (S Z) (S k) = [(S Z ** oneDiv (S Z))]
genFact (S (S j)) (S k) =
    case (decDiv (S (S j)) (LTESucc (LTESucc (LTEZero{right = j}))) (S k)
          {euc=eculidDivideAux (S (S j)) (S k) SIsNotZ }) of
               (Yes prf) => (genFact (S (S j)) k) ++ [(S k ** prf)]
               (No contra) => (genFact (S (S j)) k)

--if the List has only 2 elements, i.e 1 and p, then the number is prime. the function outputs a list (secretly genFact)
-- along with the proof that the length of the list of factors is 2
isPrimeWithoutProof : (p: Nat) -> {auto pf: LTE 2 p} -> Type
isPrimeWithoutProof p = length (genFact p p) = 2

-- more than 2 factors implies number is composite
isCompositeWithoutProof : (n: Nat) -> {auto pf: LTE 2 n} -> Type
isCompositeWithoutProof n = Prelude.Nat.GT (Prelude.List.length (genFact n n)) 2

-- Two is a prime
twoPr : (isPrime 2 (LTESucc (LTESucc (LTEZero {right =0}))))
twoPr {k=Z} (x ** pf) = void (SIsNotZ (snd pf))
twoPr {k=(S Z)} (x ** pf) = Left Refl
twoPr {k=(S (S Z))} (x ** pf) = Right Refl
twoPr {k=(S (S (S k)))} pf = void (bGtAImpNotbDivA 2 (S (S (S k))) k (LTESucc (LTESucc (LTESucc (LTEZero {right = k})))) (pf))

--Composite proof
isComposite : (n : Nat) -> LTE 2 n -> Type
isComposite n pflte = (a : Nat ** (b : Nat ** ((GT a 1, GT b 1), n = a*b)))

-- --deciability for Composite numbers
-- decComposite : (n: Nat) -> (pf : LTE 2 n) -> Dec (isComposite n pf)
-- decComposite Z LTEZero impossible
-- decComposite Z (LTESucc _) impossible
-- decComposite (S Z) (LTESucc LTEZero) impossible
-- decComposite (S Z) (LTESucc (LTESucc _)) impossible
-- decComposite (S (S k)) pf = ?decCompositerhs_1
--
--

--if 1<n, a not equal to a*n
aNotEqToMultA : (a : Nat) -> LTE 1 a -> (n : Nat) -> LTE 2 n -> (a = a*n) -> Void
aNotEqToMultA _ _ Z LTEZero _ impossible
aNotEqToMultA _ _ Z (LTESucc _) _ impossible
aNotEqToMultA _ _ (S Z) (LTESucc LTEZero) _ impossible
aNotEqToMultA _ _ (S Z) (LTESucc (LTESucc _)) _ impossible
aNotEqToMultA Z LTEZero (S (S _)) _ _ impossible
aNotEqToMultA Z (LTESucc _) (S (S _)) _ _ impossible
aNotEqToMultA (S j) (LTESucc (LTEZero {right = j})) (S (S k)) (LTESucc (LTESucc (LTEZero {right = k}))) prf =
                              SIsNotZ {x = j+(k*(S j))} (sym (pfeq)) where
                                pfeq  = plusLeftCancel (S j) Z ((S k)*(S j)) pfeq1 where
                                  pfeq1 = rewrite (multCommutative (S (S k)) (S j)) in
                                          trans (plusZeroRightNeutral (S j)) prf

--helper apNat function
apNat : (f: Nat -> Nat) -> (n: Nat) -> (m: Nat) -> n = m -> f n = f m
apNat f m m Refl = Refl

--n is not both prime and composite
notBothPrimeandComp : {n : Nat} -> (pf : LTE 2 n) -> Not (isPrime n pf, isComposite n pf)
notBothPrimeandComp {n = Z} LTEZero _ impossible
notBothPrimeandComp {n = Z} (LTESucc _) _ impossible
notBothPrimeandComp {n = (S Z)} (LTESucc LTEZero) _ impossible
notBothPrimeandComp {n = (S Z)} (LTESucc (LTESucc _)) _ impossible
notBothPrimeandComp {n = (S (S k))} pftwolten (pfprime , (a ** (b ** ((pfagtone, pfbgtone), pfneqab)))) =
                            void (aNotEqToMultA (S (S k)) (lteTransitive (LTESucc (LTEZero {right = (S Z)})) pftwolten) b pfbgtone pfeq) where
                              pfeq = (trans pfneqab funceq) where
                                funceq = (apNat (\x=>(x*b)) a (S (S k)) pfaeqn) where
                                  pfaeqn =  case (pfprime (b ** ((lteTransitive (LTESucc (LTEZero {right = (S Z)})) pfbgtone), pfneqab))) of
                                          Left pf => void ((Prelude.Basics.fst (ltImpliesNotEqNotGT {a=(S Z)} {b = a} pfagtone)) (sym pf))
                                          Right pf => pf
--
-- -- given n >= 2, it is either prime or Composite
-- eitherPrimeOrComp : {n : Nat} -> (pf : LTE 2 n) -> Either (isPrime n pf)(isComposite n pf)
-- eitherPrimeOrComp {n = Z} LTEZero impossible
-- eitherPrimeOrComp {n = Z} (LTESucc _) impossible
-- eitherPrimeOrComp {n = (S Z)} (LTESucc LTEZero) impossible
-- eitherPrimeOrComp {n = (S Z)} (LTESucc (LTESucc _)) impossible
-- eitherPrimeOrComp {n = (S (S k))} pflte = ?rhs_1


text:
%nomangle
continue : Int -> Int
continue x = x + 1

%nomangle "refc:break"
break : Int -> Int
break x = x + 1

main : IO ()
main = pure ()


text:
module Crypto.Hash.SHA2

import Crypto.Hash.Interfaces
import Data.Bits
import Data.DPair
import Data.Fin
import Data.Fin.Extra
import Data.List
import Data.Nat
import Data.Nat.Factor
import Data.Vect
import Utils.Misc
import Utils.Bytes
import Crypto.Hash.MerkleDamgard

export
data Sha256 : Type where
  MkSha256 : MerkleDamgard 8 64 Bits32 -> Sha256

export
data Sha224 : Type where
  MkSha224 : Sha256 -> Sha224

export
data Sha512 : Type where
  MkSha512 : MerkleDamgard 8 128 Bits64 -> Sha512

export
data Sha384 : Type where
  MkSha384 : Sha512 -> Sha384

sha256_init_hash_values : Vect 8 Bits32
sha256_init_hash_values =
  [ 0x6a09e667, 0xbb67ae85, 0x3c6ef372, 0xa54ff53a, 0x510e527f, 0x9b05688c, 0x1f83d9ab, 0x5be0cd19 ]

sha256_round_constants : Vect 64 Bits32
sha256_round_constants =
  [ 0x428a2f98, 0x71374491, 0xb5c0fbcf, 0xe9b5dba5, 0x3956c25b, 0x59f111f1, 0x923f82a4, 0xab1c5ed5
  , 0xd807aa98, 0x12835b01, 0x243185be, 0x550c7dc3, 0x72be5d74, 0x80deb1fe, 0x9bdc06a7, 0xc19bf174
  , 0xe49b69c1, 0xefbe4786, 0x0fc19dc6, 0x240ca1cc, 0x2de92c6f, 0x4a7484aa, 0x5cb0a9dc, 0x76f988da
  , 0x983e5152, 0xa831c66d, 0xb00327c8, 0xbf597fc7, 0xc6e00bf3, 0xd5a79147, 0x06ca6351, 0x14292967
  , 0x27b70a85, 0x2e1b2138, 0x4d2c6dfc, 0x53380d13, 0x650a7354, 0x766a0abb, 0x81c2c92e, 0x92722c85
  , 0xa2bfe8a1, 0xa81a664b, 0xc24b8b70, 0xc76c51a3, 0xd192e819, 0xd6990624, 0xf40e3585, 0x106aa070
  , 0x19a4c116, 0x1e376c08, 0x2748774c, 0x34b0bcb5, 0x391c0cb3, 0x4ed8aa4a, 0x5b9cca4f, 0x682e6ff3
  , 0x748f82ee, 0x78a5636f, 0x84c87814, 0x8cc70208, 0x90befffa, 0xa4506ceb, 0xbef9a3f7, 0xc67178f2 ]

sha256_extend_message : Vect 16 Bits32 -> Stream Bits32
sha256_extend_message xs = prepend (toList xs) $ go xs
  where
  go : Vect 16 Bits32 -> Stream Bits32
  go xs =
    let
      [wi_16, wi_15, wi_7, wi_2] = the (Vect 4 _) $ map (flip index xs) [0, 1, 9, 14]
      s0 = rotr 7  wi_15 `xor` rotr 18 wi_15 `xor` shiftR wi_15 3
      s1 = rotr 17 wi_2 ` xor` rotr 19 wi_2  `xor` shiftR wi_2  10
      w = wi_16 + s0 + wi_7 + s1
    in
      w :: go (tail xs `snoc` w)

sha256_compress : (block : Vect 64 Bits8) -> (h : Vect 8 Bits32) -> Vect 8 Bits32
sha256_compress block hash_values = zipWith (+) hash_values $ go sha256_round_constants (take _ $ sha256_extend_message $ map (from_be {a = Bits32} {n = 4}) $ group 16 4 block) hash_values
  where
  go : (ks : Vect kn Bits32) -> (ws : Vect kn Bits32) -> (h : Vect 8 Bits32) -> Vect 8 Bits32
  go [] _ h = h
  go (k :: ks) (w :: ws) [a,b,c,d,e,f,g,h] =
    let
      s1 = rotr 6 e `xor` rotr 11 e `xor` rotr 25 e
      ch = (e .&. f) `xor` (complement e .&. g)
      temp1 = h + s1 + ch + k + w
      s0 = rotr 2 a `xor` rotr 13 a `xor` rotr 22 a
      maj = (a .&. b) `xor` (a .&. c) `xor` (b .&. c)
      temp2 = s0 + maj
    in
      go ks ws [temp1 + temp2, a, b, c, d + temp1, e, f, g]

sha256_update : List Bits8 -> Sha256 -> Sha256
sha256_update input (MkSha256 s) =
  let
    Fraction _ 64 nblocks residue_nbyte prf = divMod (s.buffer_nbyte + length input) 64
    (blocks, residue) = splitAt (mult nblocks 64) (replace_vect (sym prf) (s.buffer ++ fromList input))
  in
    MkSha256 $ {buffer := residue, buffer_nbyte := _, buffer_nbyte_constraint := elemSmallerThanBound residue_nbyte }
      ( foldl (\s_, block_ => {hash_values $= sha256_compress block_, npassed_blocks $= S} s_) s (group nblocks 64 blocks) )

sha256_finalize : Sha256 -> Vect 32 Bits8
sha256_finalize (MkSha256 s) =
  concat $ map (to_be {n = 4}) $
    case pad_theorem {block_nbyte = 64} {residue_max_nbyte = 55} {length_nbyte = 8} (LTESucc LTEZero) Refl s.buffer_nbyte_constraint s.buffer (integer_to_be _ $ 8 * (cast s.npassed_blocks * 64 + cast s.buffer_nbyte)) of
      Left block => sha256_compress block s.hash_values
      Right blocks => let (x1, x2) = splitAt 64 blocks in sha256_compress x2 $ sha256_compress x1 s.hash_values

sha224_init_hash_values : Vect 8 Bits32
sha224_init_hash_values =
  [ 0xc1059ed8, 0x367cd507, 0x3070dd17, 0xf70e5939, 0xffc00b31, 0x68581511, 0x64f98fa7, 0xbefa4fa4 ]

sha512_init_hash_values : Vect 8 Bits64
sha512_init_hash_values =
  [ 0x6a09e667f3bcc908, 0xbb67ae8584caa73b, 0x3c6ef372fe94f82b, 0xa54ff53a5f1d36f1
  , 0x510e527fade682d1, 0x9b05688c2b3e6c1f, 0x1f83d9abfb41bd6b, 0x5be0cd19137e2179 ]

sha512_round_constants : Vect 80 Bits64
sha512_round_constants =
  [ 0x428a2f98d728ae22, 0x7137449123ef65cd, 0xb5c0fbcfec4d3b2f, 0xe9b5dba58189dbbc, 0x3956c25bf348b538
  , 0x59f111f1b605d019, 0x923f82a4af194f9b, 0xab1c5ed5da6d8118, 0xd807aa98a3030242, 0x12835b0145706fbe
  , 0x243185be4ee4b28c, 0x550c7dc3d5ffb4e2, 0x72be5d74f27b896f, 0x80deb1fe3b1696b1, 0x9bdc06a725c71235
  , 0xc19bf174cf692694, 0xe49b69c19ef14ad2, 0xefbe4786384f25e3, 0x0fc19dc68b8cd5b5, 0x240ca1cc77ac9c65
  , 0x2de92c6f592b0275, 0x4a7484aa6ea6e483, 0x5cb0a9dcbd41fbd4, 0x76f988da831153b5, 0x983e5152ee66dfab
  , 0xa831c66d2db43210, 0xb00327c898fb213f, 0xbf597fc7beef0ee4, 0xc6e00bf33da88fc2, 0xd5a79147930aa725
  , 0x06ca6351e003826f, 0x142929670a0e6e70, 0x27b70a8546d22ffc, 0x2e1b21385c26c926, 0x4d2c6dfc5ac42aed
  , 0x53380d139d95b3df, 0x650a73548baf63de, 0x766a0abb3c77b2a8, 0x81c2c92e47edaee6, 0x92722c851482353b
  , 0xa2bfe8a14cf10364, 0xa81a664bbc423001, 0xc24b8b70d0f89791, 0xc76c51a30654be30, 0xd192e819d6ef5218
  , 0xd69906245565a910, 0xf40e35855771202a, 0x106aa07032bbd1b8, 0x19a4c116b8d2d0c8, 0x1e376c085141ab53
  , 0x2748774cdf8eeb99, 0x34b0bcb5e19b48a8, 0x391c0cb3c5c95a63, 0x4ed8aa4ae3418acb, 0x5b9cca4f7763e373
  , 0x682e6ff3d6b2b8a3, 0x748f82ee5defb2fc, 0x78a5636f43172f60, 0x84c87814a1f0ab72, 0x8cc702081a6439ec
  , 0x90befffa23631e28, 0xa4506cebde82bde9, 0xbef9a3f7b2c67915, 0xc67178f2e372532b, 0xca273eceea26619c
  , 0xd186b8c721c0c207, 0xeada7dd6cde0eb1e, 0xf57d4f7fee6ed178, 0x06f067aa72176fba, 0x0a637dc5a2c898a6
  , 0x113f9804bef90dae, 0x1b710b35131c471b, 0x28db77f523047d84, 0x32caab7b40c72493, 0x3c9ebe0a15c9bebc
  , 0x431d67c49c100d4c, 0x4cc5d4becb3e42b6, 0x597f299cfc657e2a, 0x5fcb6fab3ad6faec, 0x6c44198c4a475817 ]

sha512_extend_message : Vect 16 Bits64 -> Stream Bits64
sha512_extend_message xs = prepend (toList xs) $ go xs
  where
  public export
  go : Vect 16 Bits64 -> Stream Bits64
  go xs =
    let
      [wi_16, wi_15, wi_7, wi_2] = the (Vect 4 _) $ map (flip index xs) [0, 1, 9, 14]
      s0 = rotr 1  wi_15 `xor` rotr 8  wi_15 `xor` shiftR wi_15 7
      s1 = rotr 19 wi_2  `xor` rotr 61 wi_2  `xor` shiftR wi_2  6
      w = wi_16 + s0 + wi_7 + s1
    in
      w :: go (tail xs `snoc` w)

sha512_compress : (block : Vect 128 Bits8) -> (h : Vect 8 Bits64) -> Vect 8 Bits64
sha512_compress block hash_values = zipWith (+) hash_values $ go sha512_round_constants (take _ $ sha512_extend_message $ map (from_be {a = Bits64}) $ group 16 8 block) hash_values
  where
  go : (ks : Vect kn Bits64) -> (ws : Vect kn Bits64) -> (h : Vect 8 Bits64) -> Vect 8 Bits64
  go [] _ h = h
  go (k :: ks) (w :: ws) [a,b,c,d,e,f,g,h] =
    let
      s1 = rotr 14 e `xor` rotr 18 e `xor` rotr 41 e
      ch = (e .&. f) `xor` (complement e .&. g)
      temp1 = h + s1 + ch + k + w
      s0 = rotr 28 a `xor` rotr 34 a `xor` rotr 39 a
      maj = (a .&. b) `xor` (a .&. c) `xor` (b .&. c)
      temp2 = s0 + maj
    in
      go ks ws [temp1 + temp2, a, b, c, d + temp1, e, f, g]

sha512_update : List Bits8 -> Sha512 -> Sha512
sha512_update input (MkSha512 s) =
  let
    Fraction _ 128 nblocks residue_nbyte prf = divMod (s.buffer_nbyte + length input) 128
    (blocks, residue) = splitAt (mult nblocks 128) (replace_vect (sym prf) (s.buffer ++ fromList input))
  in
    MkSha512 $ {buffer := residue, buffer_nbyte := _, buffer_nbyte_constraint := elemSmallerThanBound residue_nbyte }
      ( foldl (\s_, block_ => {hash_values $= sha512_compress block_, npassed_blocks $= S} s_) s (group nblocks 128 blocks) )

sha512_finalize : Sha512 -> Vect 64 Bits8
sha512_finalize (MkSha512 s) =
  concat $ map (to_be {n = 8}) $
    case pad_theorem {block_nbyte = 128} {residue_max_nbyte = 111} {length_nbyte = 16} (LTESucc LTEZero) Refl s.buffer_nbyte_constraint s.buffer (integer_to_be _ $ 8 * (cast s.npassed_blocks * 128 + cast s.buffer_nbyte)) of
      Left block => sha512_compress block s.hash_values
      Right blocks => let (x1, x2) = splitAt 128 blocks in sha512_compress x2 $ sha512_compress x1 s.hash_values

sha384_init_hash_values : Vect 8 Bits64
sha384_init_hash_values =
  [ 0xcbbb9d5dc1059ed8, 0x629a292a367cd507, 0x9159015a3070dd17, 0x152fecd8f70e5939
  , 0x67332667ffc00b31, 0x8eb44a8768581511, 0xdb0c2e0d64f98fa7, 0x47b5481dbefa4fa4 ]

export
Digest Sha256 where
  digest_nbyte = 32
  update = sha256_update
  finalize = sha256_finalize

export
Digest Sha224 where
  digest_nbyte = 28
  update xs (MkSha224 s) = MkSha224 $ update xs s
  finalize (MkSha224 s) = take _ $ finalize s

export
Digest Sha512 where
  digest_nbyte = 64
  update = sha512_update
  finalize = sha512_finalize

export
Digest Sha384 where
  digest_nbyte = 48
  update xs (MkSha384 s) = MkSha384 $ update xs s
  finalize (MkSha384 s) = take _ $ finalize s

export
Hash Sha256 where
  block_nbyte = 64
  initialize = MkSha256 $ mk_merkle_damgard sha256_init_hash_values

export
Hash Sha224 where
  block_nbyte = 64
  initialize = MkSha224 $ MkSha256 $ mk_merkle_damgard sha224_init_hash_values

export
Hash Sha512 where
  block_nbyte = 128
  initialize = MkSha512 $ mk_merkle_damgard sha512_init_hash_values

export
Hash Sha384 where
  block_nbyte = 128
  initialize = MkSha384 $ MkSha512 $ mk_merkle_damgard sha384_init_hash_values


text:
data Foobar : String -> Type where
  MkBar : (s : String) -> Foobar s

test : (foobar : (x ** Foobar x)) -> String
test (MkDPair fst snd) with (snd)
  test (MkDPair fst snd) | (MkBar fst) = ?test_rhs__rhs_

test' : (foobar : (x ** Foobar x)) -> String
test' (s ** foobar) with (foobar)
  test' (s ** foobar) | with_pat = ?test'_rhs_rhs


text:
module Test.Suite

import IdrTest.Test

import Test.Inigo.Account.AccountTest
import Test.Inigo.Archive.ArchiveTest
import Test.Inigo.Package.PackageDepsTest
import Test.Inigo.Package.PackageIndexTest
import Test.Inigo.Package.PackageTest
import Test.Server.Template.TemplateTest

suite : IO ()
suite = do
  runSuites
    [ Test.Inigo.Account.AccountTest.suite
    , Test.Inigo.Archive.ArchiveTest.suite
    , Test.Inigo.Package.PackageDepsTest.suite
    , Test.Inigo.Package.PackageIndexTest.suite
    , Test.Inigo.Package.PackageTest.suite
    , Test.Server.Template.TemplateTest.suite
    ]

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
fstDup: (xs : List a) -> map fst (map dup xs) === xs
fstDup Nil = Refl
fstDup (x::xs) = ?a


text:
%prefix_record_projections off

data T : Nat -> Type where
  MkT : (n : Nat) -> T n

record R where
  n : Nat
  x : T n


text:
-- examples in "Type-Driven Development with Idris"
-- chapter 6

import Data.Vect

-- check that all functions are total
%default total

--
-- section 6.1
--

Position : Type
Position = (Double, Double)

Polygon : Nat -> Type
Polygon n = Vect n Position

tri : Polygon 3
tri = [(0.0, 0.0), (3.0, 0.0), (0.0, 4.0)]

StringOrInt : Bool -> Type
StringOrInt False = String
StringOrInt True = Int

getStringOrInt : (isInt : Bool) -> StringOrInt isInt
getStringOrInt False = "Ninety-four"
getStringOrInt True = 94

valToString : (isInt : Bool) -> StringOrInt isInt -> String
valToString False x = trim x
valToString True x = cast x

--
-- section 6.2
--

||| defines types of functions with n arguments of kind t -> t -> ... -> t
AdderType : (n : Nat) -> Type -> Type
AdderType Z t = t
AdderType (S k) t = (next : t) -> AdderType k t

-- > :let A2 = AdderType 2
-- > :let A4 = AdderType 4
-- > A2 Nat
-- Nat -> Nat -> Nat : Type
-- > A4 Int
-- Int -> Int -> Int -> Int -> Int : Type

||| generic adder of type t -> (t -> t -> ... -> t)
||| where the first argument is the accumulator
adder : Num t => (n : Nat) -> (acc : t) -> AdderType n t
adder Z acc = acc
adder (S k) acc = \next => adder k (next + acc)

||| adder for 3 naturals
add3Nat : AdderType 3 Nat
add3Nat = adder 3 0

val1 : Nat
val1 = add3Nat 1 2 3

val2 : Int
val2 = (adder 4 0) 1 2 3 4

-- > val1
-- 6 : Nat
-- > val2
-- 10 : Int

--
-- section 6.3
-- see DataStore.idr
--

max_stars_repo_name: pascalpoizat/idris-book

max_issues_repo_name: pascalpoizat/idris-book

max_forks_repo_name: pascalpoizat/idris-book


text:
import Data.List

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

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

testOp : (a: Type) -> (Show a, Eq a)
         => (opName : String)
         -> (op : a -> a -> a)
         -> List (a,a,a)
         -> List String
testOp a n op = mapMaybe doTest
  where doTest : (a,a,a) -> Maybe String
        doTest (x,y,res) =
          let myRes = op x y
           in if myRes == res then Nothing
              else Just $  #"Invalid result for \#{n} on \#{showTpe a}. "#
                        ++ #"Inputs: \#{show x}, \#{show y}. "#
                        ++ #"Expected \#{show res} but got \#{show myRes}."#

results : List String
results =
     testOp Int8 "shl" prim__shl_Int8
       [(0,7,0),(1,1,2),(1,3,8),(1,7,-128),(-1,7,-128)]
  ++ testOp Int8 "shr" prim__shr_Int8
       [(0,7,0),(1,1,0),(-128,1,-64),(127,3,15),(-1,3,-1)]
  ++ testOp Int8 "and" prim__and_Int8
       [(127,0,0),(-128,0,0),(23,-1,23),(-128,-1,-128),(15,8,8)]
  ++ testOp Int8 "or" prim__or_Int8
       [(127,0,127),(-128,-1,-1),(23,-1,-1),(15,64,79)]
  ++ testOp Int8 "xor" prim__xor_Int8
       [(127,0,127),(-128,-1,127),(127,-1,-128),(15,64,79),(15,1,14)]

  ++ testOp Bits8 "shl" prim__shl_Bits8
       [(0,7,0),(1,1,2),(1,3,8),(1,7,128),(255,7,128)]
  ++ testOp Bits8 "shr" prim__shr_Bits8
       [(0,7,0),(1,1,0),(255,1,127),(127,3,15),(255,3,31)]
  ++ testOp Bits8 "and" prim__and_Bits8
       [(127,0,0),(255,0,0),(23,255,23),(128,255,128),(15,8,8)]
  ++ testOp Bits8 "or" prim__or_Bits8
       [(127,0,127),(128,255,255),(23,255,255),(15,64,79)]
  ++ testOp Bits8 "xor" prim__xor_Bits8
       [(127,0,127),(128,255,127),(127,255,128),(15,64,79),(15,1,14)]

  ++ testOp Int16 "shl" prim__shl_Int16
       [(0,15,0),(1,1,2),(1,4,16),(1,15,-0x8000),(-1,15,-0x8000)]
  ++ testOp Int16 "shr" prim__shr_Int16
       [(0,15,0),(1,1,0),(-0x8000,1,-0x4000),(0x7fff,3,0x0fff),(-1,3,-1)]
  ++ testOp Int16 "and" prim__and_Int16
       [(0x7fff,0,0),(-0x8000,0,0),(23,-1,23),(-0x8000,-1,-0x8000),(15,8,8)]
  ++ testOp Int16 "or" prim__or_Int16
       [(127,0,127),(-0x8000,-1,-1),(23,-1,-1),(15,64,79)]
  ++ testOp Int16 "xor" prim__xor_Int16
       [(127,0,127),(-0x8000,-1,0x7fff),(0x7fff,-1,-0x8000),(15,64,79),(15,1,14)]

  ++ testOp Bits16 "shl" prim__shl_Bits16
       [(0,15,0),(1,1,2),(1,4,16),(1,15,0x8000),(0xffff,15,0x8000)]
  ++ testOp Bits16 "shr" prim__shr_Bits16
       [(0,15,0),(1,1,0),(0xffff,1,0x7fff),(0x7fff,3,0x0fff),(0xffff,3,0x1fff)]
  ++ testOp Bits16 "and" prim__and_Bits16
       [(0x7fff,0,0),(0xffff,0,0),(23,0xffff,23),(0x8000,0xffff,0x8000),(15,8,8)]
  ++ testOp Bits16 "or" prim__or_Bits16
       [(0x7fff,0,0x7fff),(0x8000,0xffff,0xffff),(23,0xffff,0xffff),(15,64,79)]
  ++ testOp Bits16 "xor" prim__xor_Bits16
       [(0x7fff,0,0x7fff),(0x8000,0xffff,0x7fff),(0x7fff,0xffff,0x8000),(15,64,79),(15,1,14)]

  ++ testOp Int32 "shl" prim__shl_Int32
       [(0,31,0),(1,1,2),(1,4,16),(1,31,-0x80000000),(-1,31,-0x80000000)]
  ++ testOp Int32 "shr" prim__shr_Int32
       [(0,31,0),(1,1,0),(-0x80000000,1,-0x40000000),(0x7fffffff,3,0x0fffffff),(-1,3,-1)]
  ++ testOp Int32 "and" prim__and_Int32
       [(0x7fffffff,0,0),(-0x80000000,0,0),(23,-1,23),(-0x80000000,-1,-0x80000000),(31,8,8)]
  ++ testOp Int32 "or" prim__or_Int32
       [(127,0,127),(-0x80000000,-1,-1),(23,-1,-1),(31,64,95)]
  ++ testOp Int32 "xor" prim__xor_Int32
       [(127,0,127),(-0x80000000,-1,0x7fffffff),(0x7fffffff,-1,-0x80000000),(15,64,79),(15,1,14)]

  ++ testOp Bits32 "shl" prim__shl_Bits32
       [(0,31,0),(1,1,2),(1,4,16),(1,31,0x80000000),(0xffffffff,31,0x80000000)]
  ++ testOp Bits32 "shr" prim__shr_Bits32
       [(0,31,0),(1,1,0),(0xffffffff,1,0x7fffffff),(0x7fffffff,3,0x0fffffff),(0xffffffff,3,0x1fffffff)]
  ++ testOp Bits32 "and" prim__and_Bits32
       [(0x7fffffff,0,0),(0xffffffff,0,0),(23,0xffffffff,23),(0x80000000,0xffffffff,0x80000000),(15,8,8)]
  ++ testOp Bits32 "or" prim__or_Bits32
       [(0x7fffffff,0,0x7fffffff),(0x80000000,0xffffffff,0xffffffff),(23,0xffffffff,0xffffffff),(15,64,79)]
  ++ testOp Bits32 "xor" prim__xor_Bits32
       [(0x7fffffff,0,0x7fffffff),(0x80000000,0xffffffff,0x7fffffff),(0x7fffffff,0xffffffff,0x80000000),(15,64,79),(15,1,14)]

  ++ testOp Int64 "shl" prim__shl_Int64
       [(0,63,0),(1,1,2),(1,4,16),(1,63,-0x8000000000000000),(-1,63,-0x8000000000000000)]
  ++ testOp Int64 "shr" prim__shr_Int64
       [(0,63,0),(1,1,0),(-0x8000000000000000,1,-0x4000000000000000),(0x7fffffffffffffff,3,0x0fffffffffffffff),(-1,3,-1)]
  ++ testOp Int64 "and" prim__and_Int64
       [(0x7fffffffffffffff,0,0),(-0x8000000000000000,0,0),(23,-1,23),(-0x8000000000000000,-1,-0x8000000000000000),(63,8,8)]
  ++ testOp Int64 "or" prim__or_Int64
       [(127,0,127),(-0x8000000000000000,-1,-1),(23,-1,-1),(63,64,127)]
  ++ testOp Int64 "xor" prim__xor_Int64
       [(127,0,127),(-0x8000000000000000,-1,0x7fffffffffffffff),(0x7fffffffffffffff,-1,-0x8000000000000000),(15,64,79),(15,1,14)]

  ++ testOp Bits64 "shl" prim__shl_Bits64
       [(0,63,0),(1,1,2),(1,4,16),(1,63,0x8000000000000000),(0xffffffffffffffff,63,0x8000000000000000)]
  ++ testOp Bits64 "shr" prim__shr_Bits64
       [(0,63,0),(1,1,0),(0xffffffffffffffff,1,0x7fffffffffffffff),(0x7fffffffffffffff,3,0x0fffffffffffffff),(0xffffffffffffffff,3,0x1fffffffffffffff)]
  ++ testOp Bits64 "and" prim__and_Bits64
       [(0x7fffffffffffffff,0,0),(0xffffffffffffffff,0,0),(23,0xffffffffffffffff,23),(0x8000000000000000,0xffffffffffffffff,0x8000000000000000),(15,8,8)]
  ++ testOp Bits64 "or" prim__or_Bits64
       [(0x7fffffffffffffff,0,0x7fffffffffffffff),(0x8000000000000000,0xffffffffffffffff,0xffffffffffffffff),(23,0xffffffffffffffff,0xffffffffffffffff),(15,64,79)]
  ++ testOp Bits64 "xor" prim__xor_Bits64
       [(0x7fffffffffffffff,0,0x7fffffffffffffff),(0x8000000000000000,0xffffffffffffffff,0x7fffffffffffffff),(0x7fffffffffffffff,0xffffffffffffffff,0x8000000000000000),(15,64,79),(15,1,14)]

main : IO ()
main = traverse_ putStrLn results


text:
module Data.Prim.Bits64

import public Control.WellFounded
import public Data.DPair
import public Data.Prim.Ord
import public Algebra.Solver.Ring
import Syntax.PreorderReasoning

%default total

unsafeRefl : a === b
unsafeRefl = believe_me (Refl {x = a})

--------------------------------------------------------------------------------
--          (<)
--------------------------------------------------------------------------------

||| Witness that `m < n === True`.
export
data (<) : (m,n : Bits64) -> Type where
  LT : {0 m,n : Bits64} -> (0 prf : (m < n) === True) -> m < n

||| Contructor for `(<)`.
|||
||| This can only be used in an erased context.
export %hint
0 mkLT : (0 prf : (m < n) === True) -> m < n
mkLT = LT

||| Extractor for `(<)`.
|||
||| This can only be used in an erased context.
export
0 runLT : m < n -> (m < n) === True
runLT (LT prf) = prf

||| We don't trust values of type `(<)` too much,
||| so we use this when creating magical results.
export
strictLT : (0 p : m < n) -> Lazy c -> c
strictLT (LT prf) x = x

--------------------------------------------------------------------------------
--          Aliases
--------------------------------------------------------------------------------

||| Flipped version of `(<)`.
public export
0 (>) : (m,n : Bits64) -> Type
m > n = n < m

||| `m <= n` mean that either `m < n` or `m === n` holds.
public export
0 (<=) : (m,n : Bits64) -> Type
m <= n = Either (m < n) (m === n)

||| Flipped version of `(<=)`.
public export
0 (>=) : (m,n : Bits64) -> Type
m >= n = n <= m

||| `m /= n` mean that either `m < n` or `m > n` holds.
public export
0 (/=) : (m,n : Bits64) -> Type
m /= n = Either (m < n) (m > n)

--------------------------------------------------------------------------------
--          Order
--------------------------------------------------------------------------------

0 ltNotEQ : m < n -> Not (m === n)
ltNotEQ x = strictLT x $ assert_total (idris_crash "IMPOSSIBLE: LT and EQ")

0 ltNotGT : m < n -> Not (n < m)
ltNotGT x = strictLT x $ assert_total (idris_crash "IMPOSSIBLE: LT and GT")

0 eqNotLT : m === n -> Not (m < n)
eqNotLT = flip ltNotEQ

export
comp : (m,n : Bits64) -> Trichotomy (<) m n
comp m n = case prim__lt_Bits64 m n of
  0 => case prim__eq_Bits64 m n of
    0 => GT (ltNotGT $ LT unsafeRefl) (ltNotEQ $ LT unsafeRefl) (LT unsafeRefl)
    x => EQ (eqNotLT unsafeRefl) (unsafeRefl) (eqNotLT unsafeRefl)
  x => LT (LT unsafeRefl) (ltNotEQ $ LT unsafeRefl) (ltNotGT $ LT unsafeRefl)

export
Total Bits64 (<) where
  trichotomy   = comp
  transLT p q  = strictLT p $ strictLT q $ LT unsafeRefl

--------------------------------------------------------------------------------
--          Bounds and Well-Foundedness
--------------------------------------------------------------------------------

||| Lower bound of `Bits64`
public export
MinBits64 : Bits64
MinBits64 = 0

||| Upper bound of `Bits64`
public export
MaxBits64 : Bits64
MaxBits64 = 0xffffffffffffffff

||| `m >= 0` for all `m` of type `Bits64`.
export
0 GTE_MinBits64 : (m : Bits64) -> m >= MinBits64
GTE_MinBits64 m = case comp MinBits64 m of
  LT x f g => %search
  EQ f x g => %search
  GT f g x => assert_total $ idris_crash "IMPOSSIBLE: Bits64 smaller than 0"

||| Not value of type `Bits64` is less than zero.
export
0 Not_LT_MinBits64 : m < 0 -> Void
Not_LT_MinBits64 = GTE_not_LT (GTE_MinBits64 m)

||| `m <= MaxBits64` for all `m` of type `Bits64`.
export
0 LTE_MaxBits64 : (m : Bits64) -> m <= MaxBits64
LTE_MaxBits64 m = case comp m MaxBits64 of
  LT x f g => %search
  EQ f x g => %search
  GT f g x => assert_total
            $ idris_crash "IMPOSSIBLE: Bits64 greater than \{show MaxBits64}"

||| Not value of type `Bits64` is greater than `MaxBits64`.
export
0 Not_GT_MaxBits64 : m > MaxBits64 -> Void
Not_GT_MaxBits64 = LTE_not_GT (LTE_MaxBits64 m)

||| Every value of type `Bits64` is accessible with relation
||| to `(<)`.
export
accessLT : (m : Bits64) -> Accessible (<) m
accessLT m = Access $ \n,lt => accessLT (assert_smaller m n)

||| `(<)` is well founded.
export %inline
WellFounded Bits64 (<) where
  wellFounded = accessLT

||| Every value of type `Bits64` is accessible with relation
||| to `(>)`.
export
accessGT : (m : Bits64) -> Accessible (>) m
accessGT m = Access $ \n,gt => accessGT (assert_smaller m n)

||| `(>)` is well founded.
export %inline
[GT] WellFounded Bits64 (>) where
  wellFounded = accessGT

--------------------------------------------------------------------------------
--          Arithmetics
--------------------------------------------------------------------------------

||| Safe division.
|||
||| This uses `0 < d` as a constraint instead
||| of `0 /= d`, because in my experience, the former
||| is much more useful.
export %inline
sdiv : (n,d : Bits64) -> (0 prf : 0 < d) => Bits64
sdiv n d = n `div` d

||| Refined division.
|||
||| This comes with a proof that the result is
||| strictly smaller than `n`.
|||
||| This uses `0 < n` as a constraint instead
||| of `0 /= n`, because in my experience, the former
||| is much more useful.
export %inline
rdiv :  (n,d : Bits64)
     -> (0 dgt1 : 1 < d)
     => (0 ngt0 : 0 < n)
     => Subset Bits64 (< n)
rdiv n d = Element (n `div` d) (LT unsafeRefl)

||| Safe modulo.
|||
||| This uses `0 < d` as a constraint instead
||| of `0 /= d`, because in my experience, the former
||| is much more useful.
|||
||| If you need the postcondition that the result is strictly
||| smaller than `d`, use `rmod` instead.
export %inline
smod : (n,d : Bits64) -> (0 prf : 0 < d) => Bits64
smod n d = n `mod` d

||| Refined modulo.
|||
||| This comes with a proof that the result is strictly smaller
||| than `d`.
|||
||| It uses `0 < d` as a constraint instead
||| of `0 /= d`, because in my experience, the former
||| is much more useful.
export %inline
rmod : (n,d : Bits64) -> (0 prf : 0 < d) => Subset Bits64 (< d)
rmod n d = Element (n `mod` d) (LT unsafeRefl)