text:
module Rings

import Monoid
import Group

%access public export

||| Distributive Law
total
IsDistributive : (typ : Type) -> ((+) : typ -> typ -> typ)
                  -> ((*) : typ -> typ -> typ) -> Type
IsDistributive typ (+) (*) = (a,b,c : typ) -> ( (a*(b + c) = (a*b) + (a*c)), ((b + c)*a = (b*a) + (c*a)) )

||| The type of proofs that a given type is a ring
total
IsRing : (ring : Type) -> ((+) : ring -> ring -> ring) -> ((*) : ring -> ring -> ring) -> Type
IsRing ring (+) (*) = (IsAbelianGrp ring (+), (Associative ring (*), IsDistributive ring (+) (*)))

||| The type of proofs that a given type is a commutative ring
total
IsCommRing : (ring : Type) -> ((+) : ring -> ring -> ring) -> ((*) : ring -> ring -> ring) -> Type
IsCommRing ring (+) (*) = (IsRing ring (+) (*) , Commutative ring (*))

||| Data type for rings
data Ring: (ring: Type) -> Type where
  MkRing: (ring : Type) -> ((+) : ring -> ring -> ring) -> ((*) : ring -> ring -> ring) -> IsRing ring (+) (*) -> Ring ring

||| Data type for commutative rings
data CRing: (ring: Type) -> Type where
  MkCRing: (ring : Type) -> ((+) : ring -> ring -> ring) -> ((*) : ring -> ring -> ring) -> IsCommRing ring (+) (*) -> CRing ring

|||A function that outputs the addition operation of a ring structure
Ring_Add: (ring: Type) -> Ring ring -> ring -> ring -> ring
Ring_Add ring (MkRing ring (+) (*) x) y z = y+z

|||A function that outputs the multiplication operation of a ring structure
Ring_Mult: (ring: Type) -> Ring ring -> ring -> ring -> ring
Ring_Mult ring (MkRing ring (+) (*) x) y z = y*z

||| Gives the additive identity of the ring
total
RingAdditive_id : (ring : Type) -> (pfr: Ring ring) -> (IdentityExists ring (Ring_Add ring pfr))
RingAdditive_id ring (MkRing ring (+) (*) ((pfGrp,pfAb), pfElse)) = Group_id ring (+) pfGrp

||| Non Zero elements in a ring
total
Ring_NonZero_Elements : (ring : Type) -> Ring ring -> Type
Ring_NonZero_Elements ring pfr = (a : ring ** ((a = e) -> Void)) where
                                             e = fst (RingAdditive_id ring pfr)

||| Type of rings with identity
total
IsRing_with_identity : (ring : Type) -> ((+) : ring -> ring -> ring) -> ((*) : ring -> ring -> ring) -> Type
IsRing_with_identity ring (+) (*) = (IsAbelianGrp ring (+), (IsMonoid ring (*), IsDistributive ring (+) (*)))

||| Useful rings - i.e commutative rings with identity
total
IsUsefulRing :  (ring : Type) -> ((+) : ring -> ring -> ring) -> ((*) : ring -> ring -> ring) -> Type
IsUsefulRing ring (+) (*) = (IsRing_with_identity ring (+) (*), IsCommRing ring (+) (*))

|||Data type for rings with identity
data Ring_with_identity: (ring: Type) -> Type where
  MkRing_with_identity: (ring : Type) -> ((+) : ring -> ring -> ring) -> ((*) : ring -> ring -> ring) -> IsRing_with_identity ring (+) (*) -> Ring_with_identity ring

|||Dat atypes for Useful rings
data URing: (ring: Type) -> Type where
  MkURing: (ring : Type) -> ((+) : ring -> ring -> ring) -> ((*) : ring -> ring -> ring) -> IsUsefulRing ring (+) (*) -> URing ring

||| A function that demonstrates that every Useful ring is commutative
total
URingisCRing: (ring: Type) -> URing ring -> CRing ring
URingisCRing ring (MkURing ring ((+)) ((*)) (a, b)) = MkCRing ring (+) (*) b

|||A function that demonstrates that every commutative ring is a ring
total
CRingisRing: (ring: Type) -> CRing ring -> Ring ring
CRingisRing ring (MkCRing ring ((+)) ((*)) (a, b)) = MkRing ring (+) (*) a

||| A function that demonstrates that every Useful ring is commutative
total
URingisRing_with_identity: (ring: Type) -> URing ring -> Ring_with_identity ring
URingisRing_with_identity ring (MkURing ring ((+)) ((*)) (a, b)) = MkRing_with_identity ring (+) (*) a

||| A function that demonstrates that every ring with identity is a ring
total
Ring_with_identity_isRing: (ring: Type) -> Ring_with_identity ring -> Ring ring
Ring_with_identity_isRing ring (MkRing_with_identity ring ((+)) ((*)) (a, b)) = MkRing ring (+) (*) (a, ((Basics.fst (Basics.fst b)), (Basics.snd b)))

|||A function that outputs the addition operation of a ring structure (with identity) - seemed more convenient than proving that the addition operation arising from the Ring_Add function is the right one
IRing_Add: (ring: Type) -> Ring_with_identity ring -> ring -> ring -> ring
IRing_Add ring (MkRing_with_identity ring (+) (*) x) y z = y +z

|||A function that outputs the multiplication operation of a ring structure (with identity)
IRing_Mult: (ring: Type) -> Ring_with_identity ring -> ring -> ring -> ring
IRing_Mult ring (MkRing_with_identity ring (+) (*) x) y z = y*z

Ring_Mult_identity: (ring: Type) -> (pfr: Ring_with_identity ring) -> DPair ring (\e => IsIdentity ring (IRing_Mult ring pfr) e)
Ring_Mult_identity ring (MkRing_with_identity ring (+) (*) x) = Basics.snd (Basics.fst (Basics.snd x))

||| Rings that have zero divisors
total
Ring_with_zero_divisor : (ring : Type) -> Ring ring -> Type
Ring_with_zero_divisor ring (MkRing ring (+) (*) pfRing) = (a : ring ** (b : ring ** Either (a*b = e) (b*a = e))) where
                                  e = DPair.fst (RingAdditive_id ring (MkRing ring (+) (*) pfRing))

||| The type of proofs that a given type is an Integral Domain
total
IsIntegralDomain : (ring : Type) -> ((+) : ring -> ring -> ring) -> ((*) : ring -> ring -> ring) -> Type
IsIntegralDomain ring (+) (*) = (pfRing : IsUsefulRing ring (+) (*) ** (((a : ring) -> (b : ring) -> (a*b = fst (RingAdditive_id ring (MkRing ring (+) (*) (fst (snd pfRing))) )) -> (Either (a = fst (RingAdditive_id ring (MkRing ring (+) (*) (fst (snd pfRing))) )) (b = fst (RingAdditive_id  ring (MkRing ring (+) (*) (fst (snd pfRing))) )) ) )) )

||| Data type for integral domains
data IntegralDomain: (ring: Type) -> Type where
  MkIntegralDomain: (ring : Type) -> ((+) : ring -> ring -> ring) -> ((*) : ring -> ring -> ring) -> IsIntegralDomain ring (+) (*) -> IntegralDomain ring

|||The type of ring homomorphisms (between rings with identity)
IRHom: (r1: Type) -> Ring_with_identity r1 -> (r2: Type) -> Ring_with_identity r2 -> (f: r1 -> r2) -> Type
IRHom r1 (MkRing_with_identity r1 ((+)) ((*)) pf1) r2 (MkRing_with_identity r2 ((p)) ((m)) pf2) f = (x: r1) -> (y: r1) -> ((f(x+y)) =  (p (f x) (f y)), (f(x*y)) = (m (f x) (f y)), (f e1) = e2) where
  e1 = DPair.fst (Ring_Mult_identity r1 (MkRing_with_identity r1 ((+)) ((*)) pf1))
  e2 = DPair.fst (Ring_Mult_identity r2 (MkRing_with_identity r2 (p) (m) pf2))

|||The type of more flexible ring homomorphisms
RHom:(r1: Type) -> Ring r1 -> (r2: Type) -> Ring r2 -> (f: r1 -> r2) -> Type
RHom r1 (MkRing r1 ((+)) ((*)) pf1) r2 (MkRing r2 ((p)) ((m)) pf2) f = (x: r1) -> (y: r1) -> ((f(x+y)) =  (p (f x) (f y)), (f(x*y)) = (m (f x) (f y)))

|||The type of ideals
IsIdeal: (i: Type) -> Ring i -> (r: Type) -> Ring r -> Type
IsIdeal i pfi r pfr = (DPair (i -> r) (\f => (Inj i r f, RHom i pfi r pfr f, (p: r) -> (t: i) -> (q: i ** ((f q) = (Ring_Mult r pfr p (f t)))) )))

|||The type of principal ideals
IsPrincipalIdeal: (i: Type) -> Ring i -> (r: Type) -> Ring r -> IsIdeal i pfi r pfr -> Type
IsPrincipalIdeal i pfi r pfr (f ** pf) = (p:i ** ((t: i) -> (x: r ** (f t) = (Ring_Mult r pfr x (f p)))) )

|||The type of PID's
IsPID: (ring : Type) -> ((+) : ring -> ring -> ring) -> ((*) : ring -> ring -> ring) -> Type
IsPID ring (+) (*) = (pfURing : IsUsefulRing ring (+) (*) ** ((i: Type) -> (pfi: Ring i) -> (pfIdeal: IsIdeal i pfi ring (CRingisRing ring (URingisCRing ring (MkURing ring (+) (*) pfURing))) ) -> IsPrincipalIdeal i pfi ring (CRingisRing ring (URingisCRing ring (MkURing ring (+) (*) pfURing))) pfIdeal) )

||| Data type for PIDs
data PID: (ring: Type) -> Type where
  MkPID: (ring : Type) -> ((+) : ring -> ring -> ring) -> ((*) : ring -> ring -> ring) -> IsPID ring (+) (*) -> PID ring

||| Euclidean Norm
total
IsEuclideanNorm : (ring : Type) -> ((+) : ring -> ring -> ring) -> ((*) : ring -> ring -> ring) -> (IsIntegralDomain ring (+) (*)) -> (norm : (ring -> Nat)) -> Type
IsEuclideanNorm ring (+) (*) pfIntDomain norm = ( ( (a : ring) -> (b : ring) -> (a = e -> Void) -> (b = e -> Void) -> (LTE (norm a) (norm (a*b))) ) , ( (a : ring) -> (b : ring) -> ((b = e -> Void)) -> (q : ring ** (r : ring ** ( (a = b*q + r) , (LTE (norm r) (norm b) )) )) ) ) where
                                                                                e = fst (RingAdditive_id ring (MkRing ring (+) (*) (fst (snd (fst pfIntDomain))) ) )
||| Euclidean Domain
total
IsEuclideanDomain : (ring : Type) -> ((+) : ring -> ring -> ring) -> ((*) : ring -> ring -> ring) -> Type
IsEuclideanDomain ring (+) (*) = (pfIntDomain : IsIntegralDomain ring (+) (*) ** (EuclNorm : (ring -> Nat) ** (IsEuclideanNorm ring (+) (*) pfIntDomain EuclNorm) ) )

||| Data type for PIDs
data EuclideanDomain: (ring: Type) -> Type where
  MkEuclideanDomain: (ring : Type) -> ((+) : ring -> ring -> ring) -> ((*) : ring -> ring -> ring) -> IsEuclideanDomain ring (+) (*) -> EuclideanDomain ring


text:
module Java.Lang

import IdrisJvm.FFI
import Data.Vect

%access public export

namespace Boolean
  BooleanClass : JVM_NativeTy
  BooleanClass = Class "java/lang/Boolean"

  parseBool : String -> Bool
  parseBool s = unsafePerformIO $ invokeStatic BooleanClass "parseBoolean" (String -> JVM_IO Bool) s

namespace Byte
  ByteClass : JVM_NativeTy
  ByteClass = Class "java/lang/Byte"

  parseByte : String -> Bits8
  parseByte s = unsafePerformIO $ invokeStatic ByteClass "parseByte" (String -> JVM_IO Bits8) s

namespace Character
  CharacterClass : JVM_NativeTy
  CharacterClass = Class "java/lang/Character"

namespace JInteger
  integerClass : String
  integerClass = "java/lang/Integer"

  IntegerClass : JVM_NativeTy
  IntegerClass = Class integerClass

  JInteger : Type
  JInteger = JVM_Native IntegerClass

  parseInt : String -> Int
  parseInt s = unsafePerformIO $ invokeStatic IntegerClass "parseInt" (String -> JVM_IO Int) s

  valueOf : Int -> JInteger
  valueOf n = unsafePerformIO $ invokeStatic IntegerClass "valueOf" (Int -> JVM_IO JInteger) n

namespace Short
  ShortClass : JVM_NativeTy
  ShortClass = Class "java/lang/Short"

  Short : Type
  Short = JVM_Native ShortClass

  parseShort : String -> Bits16
  parseShort s = unsafePerformIO $ invokeStatic ShortClass "parseShort" (String -> JVM_IO Bits16) s

  valueOf : Bits16 -> Short
  valueOf n = unsafePerformIO $ invokeStatic ShortClass "valueOf" (Bits16 -> JVM_IO Short) n

namespace Long
  LongClass : JVM_NativeTy
  LongClass = Class "java/lang/Long"

  Long : Type
  Long = JVM_Native LongClass

  parseLong : String -> Bits64
  parseLong s = unsafePerformIO $ invokeStatic LongClass "parseLong" (String -> JVM_IO Bits64) s

  valueOf : Bits64 -> Long
  valueOf n = unsafePerformIO $ invokeStatic LongClass "valueOf" (Bits64 -> JVM_IO Long) n

  intValue : Bits64 -> Int
  intValue n = unsafePerformIO $ invokeInstance "intValue" (Long -> JVM_IO Int) (Long.valueOf n)

namespace JDouble
  DoubleClass : JVM_NativeTy
  DoubleClass = Class "java/lang/Double"

  JDouble : Type
  JDouble = JVM_Native DoubleClass

  parseDouble : String -> Double
  parseDouble s = unsafePerformIO $ invokeStatic DoubleClass "parseDouble" (String -> JVM_IO Double) s

  valueOf : Double -> JDouble
  valueOf n = unsafePerformIO $ invokeStatic DoubleClass "valueOf" (Double -> JVM_IO JDouble) n

namespace Math

  MathClass : JVM_NativeTy
  MathClass = Class "java/lang/Math"

  Math : Type
  Math = JVM_Native MathClass

  maxInt : Int -> Int -> Int
  maxInt a b = unsafePerformIO $ invokeStatic MathClass "max" (Int -> Int -> JVM_IO Int) a b

  maxDouble : Double -> Double -> Double
  maxDouble a b = unsafePerformIO $ invokeStatic MathClass "max" (Double -> Double -> JVM_IO Double) a b

  maxFloat : JFloat -> JFloat -> JFloat
  maxFloat a b = unsafePerformIO $ invokeStatic MathClass "max" (JFloat -> JFloat -> JVM_IO JFloat) a b

namespace Closeable

  Closeable : Type
  Closeable = JVM_Native (Interface "java/io/Closeable")

  close : Inherits Closeable closeable => closeable -> JVM_IO ()
  close closeable = invokeInstance "close" (Closeable -> JVM_IO ()) (believe_me closeable)

namespace Flushable

  Flushable : Type
  Flushable = JVM_Native (Interface "java/io/Flushable")

  flush : Inherits Flushable flushable => flushable -> JVM_IO ()
  flush flushable = invokeInstance "flush" (Flushable -> JVM_IO ()) (believe_me flushable)

namespace InputStream

  InputStream : Type
  InputStream = JVM_Native (Class "java/io/InputStream")

  Inherits Closeable InputStream where {}

namespace PrintStream

  PrintStream : Type
  PrintStream = JVM_Native $ Class "java/io/PrintStream"

  println : PrintStream -> String -> JVM_IO ()
  println = invokeInstance "println" (PrintStream -> String -> JVM_IO ())

  printCh : PrintStream -> Char -> JVM_IO ()
  printCh = invokeInstance "print" (PrintStream -> Char -> JVM_IO ())

  Inherits Flushable PrintStream where {}

namespace System

  systemClass : String
  systemClass = "java/lang/System"

  SystemClass : JVM_NativeTy
  SystemClass = Class systemClass

  getProperty : String -> JVM_IO (Maybe String)
  getProperty p = nullableStringToMaybe <$> invokeStatic SystemClass "getProperty" (String -> JVM_IO String) p

  getenv : String -> JVM_IO (Maybe String)
  getenv p = nullableStringToMaybe <$> invokeStatic SystemClass "getenv" (String -> JVM_IO String) p

  setProperty : String -> String -> JVM_IO (Maybe String)
  setProperty name value = nullableStringToMaybe <$>
    invokeStatic SystemClass "setProperty" (String -> String -> JVM_IO String) name value

  -- Takes a property name and a default value and returns the property value
  -- if it exists otherwise returns the default value
  getPropertyWithDefault : String -> String -> JVM_IO String
  getPropertyWithDefault = invokeStatic SystemClass "getProperty" (String -> String -> JVM_IO String)

  stdout : PrintStream
  stdout = unsafePerformIO $ getStaticField SystemClass "out" (JVM_IO PrintStream)

  stderr : PrintStream
  stderr = unsafePerformIO $ getStaticField SystemClass "err" (JVM_IO PrintStream)

  stdin : InputStream
  stdin = unsafePerformIO $ getStaticField SystemClass "in" (JVM_IO InputStream)

  lineSeparator : JVM_IO String
  lineSeparator = invokeStatic SystemClass "lineSeparator" (JVM_IO String)

  exit : Int -> JVM_IO ()
  exit = invokeStatic SystemClass "exit" (Int -> JVM_IO ())

namespace Runnable
  Runnable : Type
  Runnable = javaInterface "java/lang/Runnable"

  %inline
  jlambda : JVM_IO () -> Runnable
  jlambda f = javalambda "run" (JVM_IO ()) g
    where
      g : () -> ()
      g x = unsafePerformIO f

  run : Runnable -> JVM_IO ()
  run runnable = invokeInstance "run" (Runnable -> JVM_IO ()) runnable

namespace Thread

  ThreadClass : JVM_NativeTy
  ThreadClass = Class "java/lang/Thread"

  Thread : Type
  Thread = JVM_Native ThreadClass

  fromRunnable : Runnable -> JVM_IO Thread
  fromRunnable runnable = FFI.new (Runnable -> JVM_IO Thread) runnable

  start : Thread -> JVM_IO ()
  start thread = invokeInstance "start" (Thread -> JVM_IO ()) thread

  sleep : Bits64 -> JVM_IO ()
  sleep millis = invokeStatic ThreadClass "sleep" (Bits64 -> JVM_IO ()) millis

  currentThread : JVM_IO Thread
  currentThread = invokeStatic ThreadClass "currentThread" (JVM_IO Thread)

  getId : Thread -> JVM_IO Bits64
  getId thread = invokeInstance "getId" (Thread -> JVM_IO Bits64) thread

  join : Thread -> JVM_IO ()
  join thread = invokeInstance "join" (Thread -> JVM_IO ()) thread

namespace JavaString

  stringClass : String
  stringClass = "java/lang/String"

  StringClass : JVM_NativeTy
  StringClass = Class stringClass

  StringArray : Type
  StringArray = JVM_Array String

  boolToString : Bool -> String
  boolToString b = unsafePerformIO $ invokeStatic StringClass "valueOf" (Bool -> JVM_IO String) b

  charAt : String -> Int -> Char
  charAt str index = unsafePerformIO $ invokeInstance "charAt" (String -> Int -> JVM_IO Char) str index

  charToString : Char -> String
  charToString b = unsafePerformIO $ invokeStatic StringClass "valueOf" (Char -> JVM_IO String) b

  byteToString : Bits8 -> String
  byteToString b = unsafePerformIO $ invokeStatic ByteClass "toString" (Bits8 -> JVM_IO String) b

  shortToString : Bits16 -> String
  shortToString b = unsafePerformIO $ invokeStatic ShortClass "toString" (Bits16 -> JVM_IO String) b

  longToString : Bits64 -> String
  longToString b = unsafePerformIO $ invokeStatic LongClass "toString" (Bits64 -> JVM_IO String) b

  getBytes : String -> JVM_IO (JVM_Array Bits8)
  getBytes str = invokeInstance "getBytes" (String -> String -> JVM_IO (JVM_Array Bits8)) str "UTF-8"

  format : String -> JVM_Array Object -> String
  format fmt args = unsafePerformIO $ invokeStatic StringClass "format" (String -> JVM_Array Object -> JVM_IO String) fmt args

namespace StringBuilder
    StringBuilderClass : JVM_NativeTy
    StringBuilderClass = Class "java/lang/StringBuilder"

    StringBuilder : Type
    StringBuilder = JVM_Native StringBuilderClass

    new : Int -> JVM_IO StringBuilder
    new = FFI.new (Int -> JVM_IO StringBuilder)

    appendString : StringBuilder -> String -> JVM_IO StringBuilder
    appendString = invokeInstance "append" (StringBuilder -> String -> JVM_IO StringBuilder)

    toString : StringBuilder -> JVM_IO String
    toString = invokeInstance "toString" (StringBuilder -> JVM_IO String)

%inline
vectToArray : Vect n elemTy -> {auto jvmType: JVM_Types elemTy} -> JVM_IO (JVM_Array elemTy)
vectToArray {elemTy} xs
    = vectToArray' xs
        (\n => newArray elemTy n)
        (setArray (JVM_Array elemTy -> Int -> elemTy -> JVM_IO ()))
  where
    vectToArray' : Vect n elemTy
                -> (Nat -> JVM_IO (JVM_Array elemTy))
                -> (JVM_Array elemTy -> Int -> elemTy -> JVM_IO ())
                -> JVM_IO (JVM_Array elemTy)
    vectToArray' {n} xs createArray setArray' = do
        arr <- createArray n
        go arr 0 xs
      where
        go : JVM_Array elemTy -> Int -> Vect m elemTy -> JVM_IO (JVM_Array elemTy)
        go arr index [] = pure arr
        go arr index (x :: xs) = do
          setArray' arr index x
          go arr (index + 1) xs

%inline
listToArray : List elemTy -> {auto jvmType: JVM_Types elemTy} -> JVM_IO (JVM_Array elemTy)
listToArray {elemTy} xs
    = assert_total $ listToArray' xs
        (newArray elemTy (length xs))
        (setArray (JVM_Array elemTy -> Int -> elemTy -> JVM_IO ()))
  where
    listToArray' : List elemTy
                -> JVM_IO (JVM_Array elemTy)
                -> (JVM_Array elemTy -> Int -> elemTy -> JVM_IO ())
                -> JVM_IO (JVM_Array elemTy)
    listToArray' xs createArray setArray' = do
        arr <- createArray
        go arr 0 xs
      where
        go : JVM_Array elemTy -> Int -> List elemTy -> JVM_IO (JVM_Array elemTy)
        go arr index [] = pure arr
        go arr index (x :: xs) = do
          setArray' arr index x
          go arr (index + 1) xs

%inline
vectToArray2d : Vect m (Vect n elemTy) -> {auto jvmType: JVM_Types elemTy} -> JVM_IO (JVM_Array (JVM_Array elemTy))
vectToArray2d {elemTy} xs
    = vectToArray2d' xs
        (\m, n => newMultiArray (Int -> Int -> JVM_IO (JVM_Array (JVM_Array elemTy))) (cast m) (cast n))
        (setArray (JVM_Array (JVM_Array elemTy) -> Int -> Int -> elemTy -> JVM_IO ()))
  where
    vectToArray2d' : Vect m (Vect n elemTy)
                  -> (Nat -> Nat -> JVM_IO (JVM_Array (JVM_Array elemTy)))
                  -> (JVM_Array (JVM_Array elemTy) -> Int -> Int -> elemTy -> JVM_IO ())
                  -> JVM_IO (JVM_Array (JVM_Array elemTy))
    vectToArray2d' {m} {n} xs createArray setArray' = do
        arr <- createArray m n
        go arr 0 xs
      where
        createRow : JVM_Array (JVM_Array elemTy) -> Int -> Int -> Vect a elemTy -> JVM_IO ()
        createRow arr row col [] = pure ()
        createRow arr row col (x :: xs) = do
          setArray' arr row col x
          createRow arr row (col + 1) xs

        go : JVM_Array (JVM_Array elemTy) -> Int -> Vect a (Vect b elemTy) -> JVM_IO (JVM_Array (JVM_Array elemTy))
        go {b} arr row [] = pure arr
        go {b} arr row (xs :: xxs) = do
          createRow arr row 0 xs
          go arr (row + 1) xxs

%inline
arrayToVect : JVM_Array elemTy -> {auto jvmType: JVM_Types elemTy} -> JVM_IO (n ** Vect n elemTy)
arrayToVect {elemTy} arr = do
    len <- arrayLength arr
    v <- f 0 len (getArray (JVM_Array elemTy -> Int -> JVM_IO elemTy) arr)
    pure (_ ** v)
  where
    f : (index: Nat) -> (n: Nat) -> (Int -> JVM_IO elemTy) -> JVM_IO (Vect n elemTy)
    f index Z getter = pure []
    f index (S k) getter = do
      rest <- f (index + 1) k getter
      curr <- getter (cast index)
      pure (curr :: rest)

ext: idr


text:
import Data.Fin

data Vect : Nat -> Type -> Type where
     Nil  : Vect Z a
     (::) : (x : a) -> (xs : Vect k a) -> Vect (S k) a
%name Vect xs, ys, zs

||| Indexes into given Vect and guarentees that the given index is in bounds at compile time
index : (i : Fin n) -> Vect n elem -> elem
index FZ (x :: xs) = x
index (FS i) (x :: xs) = index i xs

||| Index into given Vect and returns Nothing if index is out of bounds
tryIndex : {n: _} -> Integer -> Vect n a -> Maybe a
-- if integer can be converted to Fin of size n then apply index function
tryIndex i xs = map (\idx => index idx xs) $ integerToFin i n

||| Appends two Vects with the same element types together
append : Vect n elem -> Vect m elem -> Vect (n + m) elem
append [] ys = ys
append (x :: xs) ys = x :: append xs ys

||| Zips up two elements of equal size
zip : Vect n a -> Vect n b -> Vect n (a, b)
zip [] _ = []
zip (x :: xs) (y :: ys) = (x, y) :: zip xs ys

||| Takes first i values from given Vect
vectTake : (i : Fin (S n)) -> Vect n elem -> Vect (finToNat i) elem
vectTake FZ xs = []
vectTake (FS x) (y :: xs) = y :: vectTake x xs

||| Sums entries at index i for Vects of identical lengths
||| Returns Nothing if index is out of bounds
sumEntries : Num a => {n : _} -> (pos : Integer) -> Vect n a -> Vect n a -> Maybe a
sumEntries pos xs ys = map (\idx => index idx xs + index idx ys) $ integerToFin pos n

||| Sums entries at index i for Vects of identical lengths
||| Returns Nothing if index is out of bounds
sumEntries' : Num a => {n : _} -> (pos : Integer) -> Vect n a -> Vect n a -> Maybe a
sumEntries' pos xs ys = let f = tryIndex pos in [| f xs + f ys |]


text:
module Test.Main

import Data.List
import Data.String
import Hedgehog
import System
import System.Console.GetOpt
import System.File
import Test.Lexer
import Test.Parser
import Text.WebIDL.Codegen as Codegen
import Text.WebIDL.Types
import Text.WebIDL.Parser
import Text.PrettyPrint.Prettyprinter

--------------------------------------------------------------------------------
--          Command line options
--------------------------------------------------------------------------------

record Config where
  constructor MkConfig
  numTests : TestLimit
  files    : List String

init : List String -> Config
init = MkConfig 100

setTests : String -> Config -> Either (List String) Config
setTests s c = maybe (Left ["Not a natural number: " ++ s])
                     (\n => Right $ record { numTests = MkTagged n} c)
                     (parsePositive {a = Nat} s)

descs : List $ OptDescr (Config -> Either (List String) Config)
descs = [ MkOpt ['n'] ["testlimit"] (ReqArg setTests "<tests>")
            "number of tests to be passed by each property"
        ]

applyArgs : List String -> Either (List String) Config
applyArgs args =
  case getOpt RequireOrder descs args of
       MkResult opts n  [] [] => foldl (>>=) (Right $ init n) opts
       MkResult _ _ u e       => Left $ map unknown u ++ e

  where unknown : String -> String
        unknown = ("Unknown option: " ++)

adjust : Config -> Group -> Group
adjust (MkConfig t _) = withTests t

--------------------------------------------------------------------------------
--          Main Function
--------------------------------------------------------------------------------

run : Config -> IO ()
run cfg = do ignore . checkGroup $ adjust cfg Test.Lexer.props
             ignore . checkGroup $ adjust cfg Test.Parser.props

main : IO ()
main = do (pn :: args) <- getArgs
                       |  Nil => putStrLn "Missing executable name. Aborting..."
          Right config <- pure $ applyArgs args
                       | Left es => traverse_ putStrLn es

          run config


text:
module Data.SOP.NS

import Data.List.Elem
import Data.SOP.Interfaces
import Data.SOP.NP
import Data.SOP.Utils

import Decidable.Equality

%default total

||| An n-ary sum.
|||
||| The sum is parameterized by a type constructor f and indexed by a
||| type-level list xs. The length of the list determines the number of choices
||| in the sum and if the i-th element of the list is of type x, then the i-th
||| choice of the sum is of type f x.
|||
||| The constructor names are chosen to resemble Peano-style natural numbers,
||| i.e., Z is for "zero", and S is for "successor". Chaining S and Z chooses
||| the corresponding component of the sum.
|||
||| Note that empty sums (indexed by an empty list) have no non-bottom
||| elements.
|||
||| Two common instantiations of f are the identity functor I and the constant
||| functor K. For I, the sum becomes a direct generalization of the Either
||| type to arbitrarily many choices. For K a, the result is a homogeneous
||| choice type, where the contents of the type-level list are ignored, but its
||| length specifies the number of options.
|||
||| In the context of the SOP approach to generic programming, an n-ary sum
||| describes the top-level structure of a datatype, which is a choice between
||| all of its constructors.
|||
||| Examples:
|||
||| ```idris example
||| the (NS_ Type I [Char,Bool]) (Z 'x')
||| the (NS_ Type I [Char,Bool]) (S $ Z False)
||| ```
public export
data NS_ : (k : Type) -> (f : k -> Type) -> (ks : List k) -> Type where
  Z : (v : f t)  -> NS_ k f (t :: ks)
  S : NS_ k f ks -> NS_ k f (t :: ks)

||| Type alias for `NS_` with type parameter `k` being
||| implicit. This reflects the kind-polymorphic data type
||| in Haskell.
public export
NS : {k : Type} -> (f : k -> Type) -> (ks : List k) -> Type
NS = NS_ k

||| Changes an n-ary sum to the identity context `I`
||| by adjusting the types of stored values accordingly.
public export
toI : NS_ k f ks -> NS I (map f ks)
toI (Z v) = Z v
toI (S x) = S $ toI x

--------------------------------------------------------------------------------
--          Specialized Interface Functions
--------------------------------------------------------------------------------

||| Specialiced version of `hmap`
public export
mapNS : (fun : forall a . f a -> g a) -> NS f ks -> NS g ks
mapNS fun (Z v) = Z $ fun v
mapNS fun (S x) = S $ mapNS fun x

||| Specialization of `hfoldl`
public export
foldlNS : (fun : acc -> el -> acc) -> acc -> NS (K el) ks -> acc
foldlNS fun acc (Z v) = fun acc v
foldlNS fun acc (S x) = foldlNS fun acc x

||| Specialization of `hfoldr`
public export %inline
foldrNS : (fun : el -> Lazy acc -> acc) -> Lazy acc -> NS (K el) ks -> acc
foldrNS fun acc (Z v) = fun v acc
foldrNS fun acc (S x) = foldrNS fun acc x

||| Specialization of `hsequence`
public export
sequenceNS : Applicative g => NS (\a => g (f a)) ks -> g (NS f ks)
sequenceNS (Z v) = map Z v
sequenceNS (S x) = S <$> sequenceNS x

||| Specialization of `hap`
public export
hapNS : NP (\a => f a -> g a) ks -> NS f ks -> NS g ks
hapNS (fun :: _)    (Z v) = Z $ fun v
hapNS (_   :: funs) (S y) = S $ hapNS funs y

||| Specialization of `hcollapse`
public export
collapseNS : NS (K a) ks -> a
collapseNS (Z v) = v
collapseNS (S x) = collapseNS x

--------------------------------------------------------------------------------
--          Injections
--------------------------------------------------------------------------------

||| An injection into an n-ary sum takes a value of the correct
||| type and wraps it in one of the sum's possible choices.
public export
0 Injection : (f : k -> Type) -> (ks : List k) -> (v : k) -> Type
Injection f ks v = f v -> K (NS f ks) v

||| The set of injections into an n-ary sum `NS f ks` can
||| be wrapped in a corresponding n-ary product.
public export
injectionsNP : NP g ks -> NP (Injection f ks) ks
injectionsNP []       = []
injectionsNP (_ :: t) = Z :: mapNP (S .) (injectionsNP t)

||| The set of injections into an n-ary sum `NS f ks` can
||| be wrapped in a corresponding n-ary product.
public export
injections : {ks : _} -> NP (Injection f ks) ks
injections = injectionsNP (pureNP ())

||| Applies all injections to an n-ary product of values.
|||
||| This is not implemented in terms of injections for the
||| following reason: Since we have access to the structure
||| of the n-ary product and thus `ks`, we do not need a
||| runtime reference of `ks`. Therefore, when applying
||| injections to an n-ary product, prefer this function
||| over a combination involving `injections`.
public export
apInjsNP_ : NP f ks -> NP (K $ NS f ks) ks
apInjsNP_ []        = []
apInjsNP_ (v :: vs) = Z v :: mapNP S (apInjsNP_ vs)

||| Alias for `collapseNP . apInjsNP_`
public export
apInjsNP : NP f ks -> List (NS f ks)
apInjsNP = collapseNP . apInjsNP_

--------------------------------------------------------------------------------
--          Extracting and injecting values
--------------------------------------------------------------------------------

||| Injects a value into an n-ary sum.
public export
inject : {0 t : k} -> (v : f t) -> {auto prf : Elem t ks} -> NS f ks
inject v {prf = Here}    = Z v
inject v {prf = There _} = S $ inject v

||| Tries to extract a value of the given type from an n-ary sum.
public export
extract : (0 t : k) -> NS f ks -> {auto prf : Elem t ks} -> Maybe (f t)
extract _ (Z v) {prf = Here}    = Just v
extract _ (S _) {prf = Here}    = Nothing
extract _ (Z _) {prf = There y} = Nothing
extract t (S x) {prf = There y} = extract t x

||| Converts an n-ary sum into the corresponding n-ary product
||| of alternatives.
public export
toNP : {ks : _} -> Alternative g => NS f ks -> NP (g . f) ks
toNP {ks = _ :: _} (Z v) = pure v :: hpure empty
toNP {ks = _ :: _} (S x) = empty  :: toNP x

--------------------------------------------------------------------------------
--          Expanding sums
--------------------------------------------------------------------------------

||| Injects an n-ary sum into a larger n-ary sum.
public export
expand : NS f ks -> {auto prf: Sublist ks ks'} -> NS f ks'
expand (Z v) {prf = SLSame y} = Z v
expand (S x) {prf = SLSame y} = S $ expand x
expand v     {prf = SLDiff y} = S $ expand v
expand _     {prf = SLNil} impossible

||| Tries to narrow down an n-ary sum to a subset of
||| choices. `ks'` must be a sublist (values in the same order) of `ks`.
public export
narrow : NS f ks -> {auto prf: Sublist ks' ks} -> Maybe (NS f ks')
narrow _     {prf = SLNil}    = Nothing
narrow (Z v) {prf = SLSame x} = Just $ Z v
narrow (Z v) {prf = SLDiff x} = Nothing
narrow (S x) {prf = SLSame y} = S <$> narrow x
narrow (S x) {prf = SLDiff y} = narrow x

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

public export %inline
HFunctor k (List k) (NS_ k) where hmap = mapNS

public export %inline
HAp k (List k) (NP_ k) (NS_ k) where hap = hapNS

public export %inline
HFold k (List k) (NS_ k) where
  hfoldl = foldlNS
  hfoldr = foldrNS

public export
HSequence k (List k) (NS_ k) where hsequence = sequenceNS

public export
HCollapse k (List k) (NS_ k) I where hcollapse = collapseNS

public export
(all : NP (Eq . f) ks) => Eq (NS_ k f ks) where
  (==) {all = _::_} (Z v) (Z w) = v == w
  (==) {all = _::_} (S x) (S y) = x == y
  (==) {all = _::_} _     _     = False

public export
(all : NP (Ord . f) ks) => Ord (NS_ k f ks) where
  compare {all = _::_} (Z v) (Z w) = compare v w
  compare {all = _::_} (S x) (S y) = compare x y
  compare {all = _::_} (Z _) (S _) = LT
  compare {all = _::_} (S _) (Z _) = GT

||| Sums have instances of `Semigroup` and `Monoid`
||| only when they consist of a single choice, which must itself be
||| a `Semigroup` or `Monoid`.
public export
(all : NP (Semigroup . f) [k']) =>
Semigroup (NS_ k f [k']) where
  (<+>) {all = _ :: _} (Z l) (Z r) = Z $ l <+> r
  (<+>) {all = _ :: _} (S _) _    impossible
  (<+>) {all = _ :: _} _    (S _) impossible

public export
(all : NP (Show . f) ks) => Show (NS_ k f ks) where
  showPrec {all = _::_} p (Z v) = showCon p "Z" (showArg v)
  showPrec {all = _::_} p (S x) = showCon p "S" (showPrec App x)

||| Sums have instances of `Semigroup` and `Monoid`
||| only when they consist of a single choice, which must itself be
||| a `Semigroup` or `Monoid`.
public export
(all : NP (Monoid . f) [k']) => Monoid (NS_ k f [k']) where
  neutral {all = _ :: _} = Z neutral

public export
Uninhabited (Data.SOP.NS.Z x = Data.SOP.NS.S y) where
  uninhabited Refl impossible

public export
Uninhabited (Data.SOP.NS.S x = Data.SOP.NS.Z y) where
  uninhabited Refl impossible

private
zInjective : Data.SOP.NS.Z x = Data.SOP.NS.Z y -> x = y
zInjective Refl = Refl

private
sInjective : Data.SOP.NS.S x = Data.SOP.NS.S y -> x = y
sInjective Refl = Refl

public export
(all : NP (DecEq . f) ks) => DecEq (NS_ k f ks) where
  decEq {all = _::_} (Z x) (Z y) with (decEq x y)
    decEq {all = _::_} (Z x) (Z x) | Yes Refl = Yes Refl
    decEq {all = _::_} (Z x) (Z y) | No contra = No (contra . zInjective)
  decEq {all = _::_} (Z x) (S y) = No absurd
  decEq {all = _::_} (S x) (Z y) = No absurd
  decEq {all = _::_} (S x) (S y) with (decEq x y)
    decEq {all = _::_} (S x) (S x) | Yes Refl = Yes Refl
    decEq {all = _::_} (S x) (S y) | No contra = No (contra . sInjective)

--------------------------------------------------------------------------------
--          Examples and Tests
--------------------------------------------------------------------------------

Ex1 : let T = NS I [Char,Bool] in (T,T)
Ex1 = (Z 'x', S $ Z False)


text:
-- Testing that 'with' works under parameters that are implicits
parameters {0 A : Type} (pred : A -> Bool)
  foo : A -> Bool
  foo x = case pred x of
    True  => False
    False => True

  bar : (x : A) -> not (pred x) = foo x
  bar  a with (pred a)
   bar a | True  = Refl
   bar a | False = Refl


text:
module Kan
import Control.Monad.Identity
import Data.Morphisms

data Ran : (f : Type -> Type) -> (g : Type -> Type) -> (a : Type) -> Type where
  R : ({b : Type} -> (a -> f b) -> g b) -> Ran f g a

data Lan : (f : Type -> Type) -> (g : Type -> Type) -> (a : Type) -> Type where
  L : (f b -> a) -> g b -> Lan f g a

Functor (Ran f g) where
  map f ran = R (\k => let (R f') = ran in f' (k . f))

Functor (Lan f g) where
  map f (L g h) = L (f . g) h

Yoneda : (Type -> Type) -> Type -> Type
Yoneda f a = Ran Identity f a

CoYoneda : (Type -> Type) -> Type -> Type
CoYoneda f a = Lan Identity f a

Codensity : (Type -> Type) -> Type -> Type
Codensity m a = Ran m m a

Reducer : Type -> Type
Reducer a = Ran Endomorphism Endomorphism a

max_stars_repo_name: STELIORD/idris-snippets

max_issues_repo_name: stjordanis/idris-snippets

max_forks_repo_name: stjordanis/idris-snippets


text:
module Kolgut.Swagger

import Kolgut.Json
import Lightyear.StringFile
import Lightyear.Strings
import Data.String
import Debug.Error

%access public export
%language ElabReflection

rErr : String -> FileError -> String
rErr s f = "Got file error: " ++ s

pErr : String -> String -> String
pErr s1 s2 = "Got parsing error: \n" ++ s1 ++ s2

data Response : Int -> Type where
     Ok : String -> Response 200
     NotFound : Response 404
     NoContent : Response 201
     InternalServerError : Response 503

data Handler : (m : String) -> (p : String) -> (s : Int) -> (a : Type) -> Type where
  Handle : (a -> IO (Response s)) -> Handler m p s a

parseResponse : JsonValue -> Either String Int
parseResponse (JsonObject obj) = let tuples = toList obj
                                     codeStr = head' $ map fst tuples
                                     code = codeStr >>= parsePositive
                                     in
                                        maybeToEither "Invalid status code" code
parseResponse _ = Left "No status codes found"

parseStatusCode : JsonValue -> Either String Int
parseStatusCode (JsonObject obj) =
  do
    jsonResponse <- maybeToEither "No responses found" $ lookup "responses" obj
    code <- parseResponse jsonResponse
    pure code
parseStatusCode v = Left "Status code empty"

parseMethod : JsonValue -> Either String (List (String, Int))
parseMethod (JsonObject obj) =
  let
   get = map (\v => ("GET", v) ) $ lookup "get" obj
   post = map (\v => ("POST", v)) $ lookup "post" obj
   methods = (toList get) ++ (toList post)
  in traverse f methods
     where
       f : (String,JsonValue) -> Either String (String,Int)
       f (m, v) = map (\code => (m,code)) $ parseStatusCode v

parseMethod v = Left "Method empty"

parseAll : (String, JsonValue) -> Either String (List (String, String, Int))
parseAll (path, json) =
  do
    methodCodes <- parseMethod json
    pure $ map (\methodCode => (path, (fst methodCode), (snd methodCode))) methodCodes

parsePaths : JsonValue -> Either String (List (String, String, Int))
parsePaths (JsonObject obj) = let tuples = toList obj
                                  nested = traverse parseAll tuples
                                  all = map (\n => n >>= id) nested
                              in all
parsePaths v = Left "Path empty"

toHandlerType : (String,String,Int) -> Type
toHandlerType (path,method,code) = Handler method path code ()

-- JsonObject
parseSwagger : JsonValue -> Either String (List Type)
parseSwagger (JsonObject values) =
  do
    paths <- maybeToEither "No paths found in swagger" $ lookup "paths" values
    triples <- parsePaths paths
    pure $ map toHandlerType triples

parseSwagger x = Left "Invalid swagger root"

ListOfTypesToTuple : List Type -> Type
ListOfTypesToTuple (t1 :: t2 :: __) = (t1, t2)

json : String
json = """{
  "paths": {
    "/pets": {
      "get": {
        "responses": {
          "200": {
          }
        }
      },
      "post": {
        "responses": {
          "201": {
          }
        }
      }
    }

  }
}
"""

jsonValue : JsonValue
jsonValue = JsonObject $ fromList [
    ("paths",
      JsonObject $ fromList [
        ("/pets",
        JsonObject $ fromList [
          ("get",
          JsonObject $ fromList [
            ("responses",
            JsonObject $ fromList [
              ("201",
              JsonObject $ fromList [])
            ])
          ]),
          ("post",
          JsonObject $ fromList [
            ("responses",
            JsonObject $ fromList [
              ("201",
              JsonObject $ fromList [])
            ])
          ])
        ])
      ])
  ]

loadFile : String -> Either String (Type)
loadFile content = do
  --json <- (Lightyear.Strings.parse jsonToplevelValue) content
  maybeTypes <- parseSwagger Kolgut.Swagger.jsonValue --json
--  ty <- maybeToEither "No types" $ head' maybeTypes
--  pure ty
  pure $ ListOfTypesToTuple maybeTypes

provideTypes : Either FileError String -> Provider (Type)
provideTypes (Left err) = Providers.Error "Some file error"
provideTypes (Right content) = case loadFile content of
                                  Right ty => Provide ty
                                  Left er => Providers.Error er

printFileContents : Either FileError String -> IO ()
printFileContents (Left err) = print "File error"
printFileContents (Right content) = print content

loadSwagger : IO (Provider Type)
loadSwagger = do
            print "Loading file"
            maybeFile <-  readFile "petstore_small.json"
            printFileContents maybeFile
            print "Parsing Json"
            maybeFile <- pure $ Right Kolgut.Swagger.json
            print "Here"
            pure $ provideTypes maybeFile

max_stars_repo_name: janschultecom/kolgut-api

max_issues_repo_name: janschultecom/kolgut-api

max_forks_repo_name: janschultecom/kolgut-api


text:
module hw1

import Data.Vect
import Data.Fin

swap: Vect n a -> Fin n -> Fin n -> Vect n a
swap vect i j = set i (at j vect) (set j (at i vect) vect)
	where
		set: Fin n -> a -> Vect n a -> Vect n a
		set FZ val (x :: xs) = val ::  xs
		set (FS ind) val (x :: xs) = x :: (set ind val xs)

		at: Fin n -> Vect n a -> a
		at FZ (x :: xs) = x
		at (FS ind) (x :: xs) = at ind xs

i : Fin 4
i = 0
j : Fin 4
j = 1

--plus_fin: Fin a -> Fin b -> Fin (a + b)
--plus_fin FZ FZ = FZ
--plus_fin (FS a) FZ = FS (plus_fin a FZ)
--plus_fin FZ (FS b) = FS (plus_fin FZ b)
--plus_fin (FS a) (FS b) = FS (plus_fin a (FS b))

--mul_fin: Fin a -> Fin b -> Fin (a * b)
--mul_fin FZ b = FZ
--mul_fin (FS a) b = plus_fin a (mul_fin a b)

c : Fin 3
c = 2
d : Fin 4
d = 0

dec_fin: Fin (S a) -> Fin a
dec_fin (FS a) = a

a : Fin 4
a = 3
b : Fin 5
b = 2

nat_min: Nat -> Nat -> Nat
nat_min Z (S b) = Z
nat_min (S a) Z = Z
nat_min (S a) (S b) = S (nat_min a b)

max_stars_repo_name: ShuffleZZZ/ITMO

max_issues_repo_name: ShuffleZZZ/ITMO

max_forks_repo_name: ShuffleZZZ/ITMO


text:
module Verified.Monad.Either

import Verified.Monad
import Verified.Applicative
import Verified.Applicative.Either

instance VerifiedMonad (Either e) where
  monadApplicative (Left _) mx = Refl
  monadApplicative (Right _) (Left _) = Refl
  monadApplicative (Right _) (Right _) = Refl
  monadLeftIdentity _ _ = Refl
  monadRightIdentity (Left _) = Refl
  monadRightIdentity (Right _) = Refl
  monadAssociativity (Left _) f g = Refl
  monadAssociativity (Right _) f g = Refl

max_stars_repo_name: yurrriq/idris-verified

max_issues_repo_name: yurrriq/idris-verified

max_forks_repo_name: yurrriq/idris-verified


text:
import Data.Nat
data FizzBuzzReturn =
  Fizz
  | Buzz
  | FizzBuzz
  | Normal Nat

Show FizzBuzzReturn where
  show Fizz = "fizz"
  show Buzz = "buzz"
  show FizzBuzz = "fizzbuzz"
  show (Normal x) = show x

partial fizzBuzzReturn: (x: Nat) -> FizzBuzzReturn
fizzBuzzReturn x with (modNat x (the Nat 3), modNat x (the Nat 5))
  fizzBuzzReturn x | (Z, Z) = FizzBuzz
  fizzBuzzReturn x | (Z, _) = Fizz
  fizzBuzzReturn x | (_, Z) = Buzz
  fizzBuzzReturn x | _ = Normal x

partial fizzBuzzReturnString: (x: Nat) -> String
fizzBuzzReturnString x = show(fizzBuzzReturn x)


text:
||| Applitation of a `replica run` command
module Replica.App.Run

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

import Data.Either
import Data.List
import Data.List1
import Data.Maybe
import Data.String
import Data.String.Extra

import Language.JSON

import System.Future
import System.Path

import Replica.App.Clock
import Replica.App.FileSystem
import Replica.App.Format
import Replica.App.Log
import Replica.App.Replica
import Replica.App.Run.Dependencies
import Replica.App.System

import Replica.Command.Run
import Replica.Core.Parse
import Replica.Core.Types
import Replica.Option.Global
import Replica.Other.Decorated
import Replica.Other.String
import Replica.Other.Validation

%default total

data RunContext : Type where

normalize : String -> String
normalize = removeTrailingNL . unlines . map unwords . filter (not . force . null) . map (assert_total words) . lines

-- Create the folders needed by Replica (usually ./.replica/test and ./.replica/log)
prepareReplicaDir : SystemIO (SystemError :: e) =>
  FileSystem (FSError :: e) =>
  Has [ State RunContext RunCommand
      , State GlobalConfig Global
      , Exception ReplicaError
      , Console
      ] e => App e String
prepareReplicaDir = do
  debug $ "GlobalConfig: \{!(show <$> get GlobalConfig)}"
  catchNew setAbsoluteReplicaDir
    (\err : FSError => throw $ CantAccessTestFile "current directory")
  rDir <- getReplicaDir
  log "Replica directory: \{rDir}"
  debug "Creating test directory: \{testDir rDir}"
  catchNew (system "mkdir -p \{show (testDir rDir)}")
    (\err : SystemError => throw $ CantAccessTestFile "\{show (testDir rDir)}")
  debug "Creating log directory: \{testDir rDir}"
  catchNew (system "mkdir -p \{show (logDir rDir)}")
    (\err : SystemError => throw $ CantAccessTestFile "\{show (logDir rDir)}")
  Just gd <- goldenDir <$> get GlobalConfig
    | Nothing => pure rDir
  debug "Creating golden-value directory: \{gd}"
  catchNew (system "mkdir -p \{show gd}")
    (\err : SystemError => throw $ CantAccessTestFile "\{show gd}")
  pure rDir

-- helper for the execution of the pre/post commands
runAll :
  SystemIO (SystemError :: e) =>
  State GlobalConfig Global e =>
  Exception TestError e =>
  Console e =>
  (phase : Maybe String) ->
  (String -> TestError) ->
  List String -> App e ()
runAll phase liftError [] = pure ()
runAll phase liftError (x :: xs) = do
  maybe (pure ()) (\p => log "\{p}: \{x}") phase
  handle (system "(\{x}) 1> /dev/null 2> /dev/null")
    (const $ runAll phase liftError xs)
    (\err : SystemError => throw $ liftError x)

-- native way to display expectations
expectedVsGiven : State GlobalConfig Global e =>
  Nat -> String -> String -> App e (List String)
expectedVsGiven k expected given = pure $ map (withOffset k) $
  ( "Expected:" :: map !red (lines expected)) ++
  ( "Given:" :: map !green (lines given))

nativeShow : State GlobalConfig Global e =>
  Console e => Nat -> String -> String -> App e ()
nativeShow n expected given =
  traverse_ putStrLn !(expectedVsGiven n expected given)

-- Provide different ways to show the difference between expectations and givens
showDiff : SystemIO (SystemError :: e) =>
  State GlobalConfig Global e =>
  State CurrentTest Test e =>
  Console e => DiffCommand -> Nat -> String -> String -> App e ()
showDiff None n expected given = pure ()
showDiff Native n expected given = nativeShow n expected given
showDiff Diff n x y = catchNew
  (system $ "diff --minimal \{!getExpectedOutput} \{!getOutputFile}")
  (\err : SystemError => pure ())
showDiff GitDiff n x y = catchNew
  (system $ "git diff --minimal --word-diff=color --no-index -- \{!getExpectedOutput} \{!getOutputFile}")
  (\err : SystemError => pure ())
showDiff (Custom z) n x y = catchNew
  (system $ "\{z} \{!getExpectedOutput} \{!getOutputFile}")
  (\err : SystemError => pure ())

getExpectationFile : Has
  [ State CurrentTest Test
  , State GlobalConfig Global ] e => Part -> App e String
getExpectationFile StdOut = getExpectedOutput
getExpectationFile StdErr = getExpectedError
getExpectationFile (FileName x) = getExpectedFile x

-- on mismatch, check if we should replace the golden value
interactiveGolden : SystemIO (SystemError :: e) =>
  FileSystem (FSError :: e) =>
  Has [ State CurrentTest Test
      , State GlobalConfig Global
      , Exception TestError
      , Console
      ] e =>
  (source : Part) ->
  (given : String) ->
  (expected : Maybe String) ->
  App e (Maybe FailReason)
interactiveGolden source given expected = do
  t <- get CurrentTest
  putStrLn $ "\{t.name}: Golden value mismatch for \{!bold (displaySource source)}"
  showExpectedAndGiven
  putStrLn $ "Do you want to \{maybe "set" (const "replace") expected} the golden value? [N/y]"
  if !readAnswer
     then do
       f <- getExpectationFile source
       log $ "Creating expectation file \{f}"
       handle (writeFile f given)
         (const $ pure Nothing)
         (\err : FSError => throw $ FileSystemError "Cannot write golden value in: \{f}")
     else pure . Just $ maybe
       (WrongOutput source given $ singleton (Generated ** Nothing))
       (\x => WrongOutput source given $ singleton (Generated ** Just x))
       expected
  where

    readAnswer : App e Bool
    readAnswer = do
      answer <- getLine
      pure $ toLower answer `elem` ["y", "yes"]

    showExpectedAndGiven : App e ()
    showExpectedAndGiven = do
      let Just str = expected
        | _ => do
          putStrLn "Expected: Nothing Found"
          putStrLn "Given:"
          putStrLn given
      let d = case !(diff <$> get GlobalConfig) of
                   None => Native
                   d' => d'
      showDiff d 0 str given

getExpected : FileSystem (FSError :: e) =>
  Has [ State RunContext RunCommand
      , Exception TestError
      , Console
      ] e => String -> App e (Maybe String)
getExpected src= do
  handle (readFile src)
    (pure . Just)
    (\err : FSError => case err of
        MissingFile _ => pure Nothing
        err => throw $ FileSystemError "Cannot read expectation")

checkConsecutive : (xs : List String) -> (given : String) -> Maybe String
checkConsecutive [] given = Nothing
checkConsecutive (x :: xs) given = do
  let (s::_) = unpack x
      | [] => checkConsecutive xs given
  case break (== s) given of
       (_, "") => Just x
       (_, str) => if isPrefixOf x str
                      then checkConsecutive xs (assert_smaller given $ drop (length x) str)
                      else checkConsecutive (x::xs) (assert_smaller given $ drop 1 str)

checkContains : List String -> String -> Maybe (List1 String)
checkContains xs given =
  fromList $ catMaybes $ map (\exp => guard (not $ isInfixOf exp given) $> exp) xs

getPartContent : SystemIO (SystemError :: e) =>
  FileSystem (FSError :: e) =>
  Has [ State CurrentTest Test
      , State GlobalConfig Global
      , State RunContext RunCommand
      , Exception TestError
      , Console ] e =>
  (part: Part) ->
  App e String
getPartContent StdOut =
  catchNew (readFile !getOutputFile)
    (\err : FSError => throw $ FileSystemError "Standard output cannot be read")
getPartContent StdErr =
  catchNew (readFile !getErrorFile)
    (\err : FSError => throw $ FileSystemError "Standard error cannot be read")
getPartContent (FileName x) =
  catchNew (readFile !(getWatchedFile x))
  (\err : FSError => throw $ FileSystemError "Expected file \{show x} cannot be read")

getPartExpectation : SystemIO (SystemError :: e) =>
  FileSystem (FSError :: e) =>
  Has [ State CurrentTest Test
      , State GlobalConfig Global
      , State RunContext RunCommand
      , Exception TestError
      , Console ] e =>
  (part: Part) ->
  App e (Maybe String)
getPartExpectation part =
  catchNew (Just <$> readFile !(getExpectationFile part)) (\err : FSError => pure Nothing)

checkContent : SystemIO (SystemError :: e) =>
  FileSystem (FSError :: e) =>
  Has [ State CurrentTest Test
      , State GlobalConfig Global
      , Exception TestError
      , Console
      ] e =>
  (spaceSensitive :Bool) ->
  (given : String) ->
  (expected : Maybe String) ->
  Expectation ->
  Maybe (e : Expectation ** ExpectationError e)
checkContent spaceSensitive given _ exp@(Exact expected) = let
  e : String = if spaceSensitive then expected else normalize expected
  g : String = if spaceSensitive then given else normalize given
  in guard (e /= g) $> (exp ** ())
checkContent spaceSensitive given _ exp@(StartsWith expected) = let
  e : String = if spaceSensitive then expected else normalize expected
  g : String = if spaceSensitive then given else normalize given
  in guard (not $ e `isPrefixOf` g) $> (exp ** ())
checkContent spaceSensitive given _ exp@(EndsWith expected) = let
  e : String = if spaceSensitive then expected else normalize expected
  g : String = if spaceSensitive then given else normalize given
  in guard (not $ e `isSuffixOf` g) $> (exp ** ())
checkContent spaceSensitive given _ exp@(Partial Ordered xs) = let
  es = if spaceSensitive then xs else map normalize xs
  g : String = if spaceSensitive then given else normalize given
  in MkDPair exp <$> checkConsecutive es given
checkContent spaceSensitive given _ exp@(Partial Whatever xs) = let
  es = if spaceSensitive then xs else map normalize xs
  g : String = if spaceSensitive then given else normalize given
  in MkDPair exp <$> checkContains es given
checkContent spaceSensitive given Nothing Generated =
  Just (Generated ** Nothing)
checkContent spaceSensitive given (Just expected) Generated = let
  e : String = if spaceSensitive then expected else normalize expected
  g : String = if spaceSensitive then given else normalize given
  in guard (e /= g) $> (Generated ** Just expected)

checkOutput : SystemIO (SystemError :: e) =>
  FileSystem (FSError :: e) =>
  Has [ State CurrentTest Test
      , State GlobalConfig Global
      , State RunContext RunCommand
      , Exception TestError
      , Console ] e =>
  (part: Part) ->
  (expectations : List Expectation) ->
  App e (Maybe FailReason)
checkOutput part expectations = do
  log $ withOffset 4 $ "Check \{displaySource part}"
  debug $ withOffset 4 $ show expectations
  t <- get CurrentTest
  given <- getPartContent part
  golden <- getPartExpectation part
  let result = fromList $ catMaybes $
    checkContent {e} t.spaceSensitive given golden <$> expectations
  debug $ withOffset 4 $ "Errors: \{show $ map (map fst) result}"
  pure $ map (WrongOutput part given) result

checkStatus : Maybe (Either Bool Nat) -> Nat -> Maybe FailReason
checkStatus Nothing y = Nothing
checkStatus (Just (Left True)) y = guard (y /= 0) $> WrongStatus y (Left True)
checkStatus (Just (Left False)) y = guard (y == 0) $> WrongStatus y (Left False)
checkStatus (Just (Right x)) y = guard (y /= x) $> WrongStatus y (Right x)

checkExpectations :  SystemIO (SystemError :: e) =>
  FileSystem (FSError :: e) =>
  Has [ State CurrentTest Test
      , State GlobalConfig Global
      , State RunContext RunCommand
      , Exception TestError
      , Console ] e =>
  (exitCode : Nat) ->
  (duration : Clock Duration) ->
  App e TestResult
checkExpectations exitCode duration = do
  log $ withOffset 2 "Checking expectations"
  t <- get CurrentTest
  ctx <- get RunContext
  let statusCheck = checkStatus t.status exitCode
  expResults <- traverse (uncurry checkOutput) t.expectations
  let failures = maybe id (::) statusCheck $ catMaybes expResults
  debug $ withOffset 4 "Check success"
  let (x :: xs) = failures
    | _ => pure $ Success duration
  let Nothing = statusCheck
    | _ => pure $ Fail failures
  debug $ withOffset 4
        "Check interactive: \{show $ isNothing statusCheck} \{show ctx.interactive}"
  let (Nothing, True) = (statusCheck, ctx.interactive)
    | _ =>  pure $ Fail failures
  [] <- map catMaybes $ traverse askForGolden failures
    | xs => pure $ Fail xs
  pure $ Success duration
  where
    askForGolden : FailReason -> App e (Maybe FailReason)
    askForGolden (WrongOutput x given ((Generated ** expected) ::: [])) =
      interactiveGolden x given expected
    askForGolden x = pure $ Just x

-- if an input is given for a test, write it in a file to pass it to the command
generateInput : FileSystem (FSError :: e) =>
      Has [ State CurrentTest Test
          , State GlobalConfig Global
          , Exception TestError ] e =>
      App e (Maybe String)
generateInput = do
  Just input <- input <$> get CurrentTest
    | _ => pure Nothing
  f <- getInputFile
  catchNew (writeFile f input)
    (\e : FSError => throw $ FileSystemError "Can't write input file \{f}")
  pure (Just f)

-- run the tested commands and gather the outputs (standard output and file output, if provided)
generateOutputs : SystemIO (SystemError :: e) =>
  FileSystem (FSError :: e) =>
  Has [ State CurrentTest Test
      , State GlobalConfig Global
      , State RunContext RunCommand
      , SystemClock
      , Exception TestError
      , Console
      ] e => App e (Either TestResult (Clock Duration, Nat))
generateOutputs = do
  t <- get CurrentTest
  debug $ withOffset 2 "Check pending"
  let False = t.pending
    | True => pure $ Left Skipped
  statusFile <- getStatusFile
  (d, _) <- runCommand !getOutputFile !getErrorFile statusFile
  Right . MkPair d . fromMaybe 0 . parsePositive <$>
    catchNew (readFile statusFile) (\err : FSError => pure "0")
  where
    runCommand : (outputFile, errorFile, statusFile : String) -> App e (Clock Duration, Int)
    runCommand outputFile errorFile statusFile = durationOf $ do
      t <- get CurrentTest
      inputFile <- generateInput
      let cmd = """
                (\{t.command}) \{maybe "" ("< " ++ )inputFile} 1> \"\{outputFile}\" 2> \"\{errorFile}\";
                EXIT_STATUS=$?;
                echo $EXIT_STATUS > \{statusFile};
                exit $EXIT_STATUS
                """
      log $ withOffset 2 "Running command: \{cmd}"
      handle (system cmd) (const $ pure 0) (\(Err n) => pure n)

testCore : SystemIO (SystemError :: e) =>
  FileSystem (FSError :: e) =>
  Has [ State CurrentTest Test
      , State GlobalConfig Global
      , State RunContext RunCommand
      , SystemClock
      , Exception TestError
      , Console
      ] e => App e TestResult
testCore = do
  Right (duration, exitCode) <- generateOutputs
    | Left res => pure res
  checkExpectations exitCode duration

-- the whole test execution, including pre and post operation
performTest : SystemIO (SystemError :: e) =>
  FileSystem (FSError :: e) =>
  Has [ State CurrentTest Test
      , State GlobalConfig Global
      , State RunContext RunCommand
      , SystemClock
      , Exception TestError
      , Console
      ] e => App e TestResult
performTest = do
  t <- get CurrentTest
  runAll (Just "Before") InitializationFailed t.beforeTest
  res <- testCore
  runAll (Just "After") (WrapUpFailed res) t.afterTest
  pure res

-- move to the right directory and perform the test
runTest : SystemIO (SystemError :: e) =>
  FileSystem (FSError :: e) =>
  Has [ State CurrentTest Test
      , State RunContext RunCommand
      , State GlobalConfig Global
      , SystemClock
      , Exception TestError
      , Console
      ] e => App e TestResult
runTest = do
  ctx <- get RunContext
  t <- get CurrentTest
  createTestDir
  createGoldenDir
  let wd = fromMaybe ctx.workingDir t.workingDir
  log "Executing \{t.name}"
  debug $ withOffset 2 $ show t
  log   $ withOffset 2 "Working directory: \{show wd}"
  catchNew (inDir wd performTest)
    (\err : FSError => throw $ FileSystemError
      "Error: cannot enter or exit test working directory \{show wd}")
  where
    inDir : (dir : String) -> App e a -> App (FSError :: e) a
    inDir dir exec = do
      pwd <- getCurrentDir
      changeDir dir
      Right res <- lift $ catch (Right <$> exec)
                                (\err : TestError => pure $ Left err)
        | Left err => changeDir pwd >> lift (throw err)
      changeDir pwd
      pure res
    continueIfExists : FSError -> App e ()
    continueIfExists (FileExists _) = pure ()
    continueIfExists _ = throw $ FileSystemError "Cant't create or access test directory"
    createTestDir : App e ()
    createTestDir = do
      catchNew (createDir !getSingleTestDir) continueIfExists
      catchNew (createDir !getSingleTestFileDir) continueIfExists
    createGoldenDir : App e ()
    createGoldenDir = do
      catchNew (createDir !getSingleTestGoldenDir) continueIfExists
      catchNew (createDir !getSingleTestGoldenFileDir) continueIfExists

displaySuite :
  Has [ State RunContext RunCommand
      , State GlobalConfig Global
      , Console
      ] e => Maybe String -> App e ()
displaySuite suite = putStrLn $ !bold $ maybe "No suite given:" ("Suite: " <+>) suite

testOutput : SystemIO (SystemError :: e) =>
  Has [ State RunContext RunCommand
      , State GlobalConfig Global
      , State CurrentTest Test
      , Console
      ] e => Either TestError TestResult -> App e ()
testOutput (Left y) = do
  t <- get CurrentTest
  putStr (withOffset 2 $ (!yellow "\{!err} \{t.name}: "))
  putStrLn (displayTestError y)
testOutput (Right Skipped) = do
  t <- get CurrentTest
  putStrLn $ withOffset 2 "\{!pending} \{t.name}"
testOutput (Right (Success duration)) = do
  displayTime <- timing <$> get RunContext
  let time = if displayTime then " (\{showDuration duration})" else ""
  t <- get CurrentTest
  if !(hideSuccess <$> get RunContext)
     then pure ()
     else putStrLn $ withOffset 2 "\{!ok} \{t.name}\{time}"
testOutput (Right (Fail xs)) = do
  t <- get CurrentTest
  putStrLn $ withOffset 2 $ !red "\{!ko} \{t.name}:"
  traverse_ (putStrLn . withOffset 6 . !red) (xs >>= displayFailReason)
  traverse_ writeFailure xs
  where
    multilineDisplay : (offset : Nat) -> (content : String) -> App e ()
    multilineDisplay offset = traverse_ (putStrLn . withOffset offset) . lines

    displayError : (given : String)  -> (exp : (e: Expectation ** ExpectationError e)) -> App e ()
    displayError given (MkDPair (Exact x) snd) =
      let content = case !(diff <$> get GlobalConfig) of
            None => multilineDisplay 8 x
            Native => multilineDisplay 8 x
            d' => showDiff d' 8 given x
      in putStrLn (withOffset 6 "Exact expectation mismatch:") >> content
    displayError given (MkDPair (StartsWith x) snd) =
      putStrLn (withOffset 6 "Start mismatch:") >> multilineDisplay 4 x
    displayError given (MkDPair (EndsWith x) snd) =
      putStrLn (withOffset 6 "End mismatch:") >> multilineDisplay 4 x
    displayError given (MkDPair (Partial Ordered ys) snd) = do
      putStrLn (withOffset 6 "Consecutive expectations mismatch, first not found:")
      multilineDisplay 8 snd
    displayError given (MkDPair (Partial Whatever ys) snd) = do
      putStrLn (withOffset 6 "Contains expectations mismatch, not found:")
      traverse_ (multilineDisplay 8) snd
    displayError given (MkDPair Generated Nothing) = pure ()
    displayError given (MkDPair Generated (Just x)) =
      let content = case !(diff <$> get GlobalConfig) of
            None => multilineDisplay 8 x
            Native => multilineDisplay 8 x
            d' => showDiff d' 8 given x
      in putStrLn (withOffset 6 "Golden value expectation mismatch:") >> content

    writeFailure : FailReason -> App e ()
    writeFailure (WrongStatus _ expected) = pure ()
    writeFailure (ExpectedFileNotFound x) = pure ()
    writeFailure (WrongOutput x given ys) = do
      putStrLn $ withOffset 6 $ !bold "Error on \{displaySource x}:"
      traverse_ (displayError given) ys
      putStrLn $ withOffset 6 $ "Given:"
      traverse_ (putStrLn . withOffset 8) $ lines given

data SuiteProcess a = None | Partial a | Total a

runAllTests : SystemIO (SystemError :: TestError :: e) =>
  SystemIO (SystemError :: e) =>
  FileSystem (FSError :: TestError :: e) =>
  SystemClock (TestError :: e) =>
  Console (TestError :: e) =>
  Has [ State RunContext RunCommand
      , State GlobalConfig Global
      , Console
      ] e =>  TestPlan -> App e (List (Maybe String, List (Test, Either TestError TestResult)))
runAllTests plan = do
  putStrLn $ separator 80
  putStrLn $ !bold "Running tests...\n"
  batchTests [] plan
  where
    selectNextSuite : TestPlan -> SuiteProcess (SuitePlan, TestPlan)
    selectNextSuite (Plan (x :: xs) waitingOthers) = Total (x, Plan xs waitingOthers)
    selectNextSuite (Plan [] waitingOthers)
      = case sortBy (flip compare `on` (length . now)) waitingOthers of
             [] => None
             (w::ws) => Partial (w, Plan [] ws)

    prepareBatch : Nat -> SuitePlan -> (List Test, SuitePlan)
    prepareBatch n plan = if n == 0
                             then (plan.now, record {now = []} plan)
                             else map (\n' => record {now = n'} plan) $ splitAt n plan.now

    processTest : Test -> App e (Test, Either TestError TestResult)
    processTest x = do
      let False = x.pending
        | True => pure (x, Right Skipped)
      r <- handle
             (new x runTest)
             (pure . MkPair x . Right)
             (\err : TestError => pure (x, Left err))
      pure r

    processResult : SuitePlan -> TestPlan -> List (Test, Either TestError TestResult) ->
                    Either TestPlan (SuitePlan, TestPlan)
    processResult (SPlan _ [] [] skipped) y xs = Left (updateOnBatchResults xs y)
    processResult x y xs = case updateOnBatchResults xs (record {ready $= (x::)} y) of
                                Plan (x'::now) later => Right (x', Plan now later)
                                p => Left p

    runTotalSuite : List (Test, Either TestError TestResult) -> SuitePlan ->
                    App e (List (Test, Either TestError TestResult))
    runTotalSuite acc plan = do
      n <- threads <$> get RunContext
      case prepareBatch n plan of
           ([], later) => do
             let errs = join [ map (\t => (t, Left Inaccessible)) plan.later
                             , map (\(reason, t) => (t, Left $ RequirementsFailed reason)) plan.skipped
                             ]
             when (not !(interactive <$> get RunContext))
               (traverse_ (\(t, r) => new t (testOutput r)) errs)
             pure $ acc ++ errs
           (now, nextBatches) => do
             debug $ withOffset 4 "Now: \{show $ length now}"
             debug $ withOffset 4 "Later: \{show $ nextBatches.now ++ nextBatches.later}"
             res <- map await <$> traverse (map (fork . delay) . processTest) now
             when (not !(interactive <$> get RunContext))
               (traverse_ (\(t, r) => new t (testOutput r)) res)
             p <- punitive <$> get RunContext
             if p && any (not . isFullSuccess . snd) res
                then pure res
                else do
                   let (suc, fai) = sortResults res
                   let newPlan = updateSuite suc fai nextBatches
                   debug $ displaySuitePlan newPlan
                   runTotalSuite (acc ++ res) $ assert_smaller plan newPlan

    runPartialSuite : (List (Test, Either TestError TestResult)) -> SuitePlan ->
                    App e (Maybe SuitePlan, List (Test, Either TestError TestResult))
    runPartialSuite acc plan = do
      n <- threads <$> get RunContext
      case prepareBatch n plan of
           ([], later) => case acc of
             [] => do
               let errs = join [ map (\t => (t, Left Inaccessible)) plan.later
                               , map (\(reason, t) => (t, Left $ RequirementsFailed reason)) plan.skipped
                               ]
               when (not !(interactive <$> get RunContext))
                 (traverse_ (\(t, r) => new t (testOutput r)) errs)
               pure (Nothing, acc ++ errs)
             _ => pure (Just plan, acc)
           (now, nextBatches) => do
             debug $ withOffset 4 "Now: \{show $ length now}"
             debug $ withOffset 4 "Later: \{show $ nextBatches.now ++ nextBatches.later}"
             res <- map await <$> traverse (map (fork . delay) . processTest) now
             when (not !(interactive <$> get RunContext))
               (traverse_ (\(t, r) => new t (testOutput r)) res)
             p <- punitive <$> get RunContext
             if p && any (not . isFullSuccess . snd) res
                then pure (Nothing, res)
                else do
                   let (suc, fai) = sortResults res
                   let newPlan = updateSuite suc fai nextBatches
                   debug $ displaySuitePlan newPlan
                   runPartialSuite (acc ++ res) $ assert_smaller plan newPlan

    mergeResults : List (Maybe String, List (Test, Either TestError TestResult)) ->
                   (Maybe String, List (Test, Either TestError TestResult)) ->
                   List (Maybe String, List (Test, Either TestError TestResult))
    mergeResults [] x = [x]
    mergeResults (y :: xs) x = if fst y == fst x
                                  then (map (++ snd x) y) :: xs
                                  else y :: mergeResults xs x

    batchTests : List (Maybe String, List (Test, Either TestError TestResult)) ->
                 TestPlan -> App e (List (Maybe String, List (Test, Either TestError TestResult)))
    batchTests acc plan = do
      debug $ withOffset 4 $ "Run a batch"
      p <- punitive <$> get RunContext
      case selectNextSuite plan of
           None => pure acc
           Total (suite, plan') => do
             displaySuite suite.name
             suiteResults <- runTotalSuite [] suite
             let acc' = mergeResults acc (suite.name, suiteResults)
             if p && any (not . isFullSuccess . snd) suiteResults
                then pure acc'
                else
                  batchTests acc' $ assert_smaller plan $ updateOnBatchResults suiteResults plan'
           Partial (suite, plan') => do
             displaySuite suite.name
             (stuckPlan, suiteResults) <- runPartialSuite [] suite
             let acc' = mergeResults acc (suite.name, suiteResults)
             if p && any (not . isFullSuccess . snd) suiteResults
                then pure acc'
                else do
                  let plan'' = record {waitingOthers $= maybe id (::) stuckPlan} plan'
                  batchTests acc' $ assert_smaller plan $ updateOnBatchResults suiteResults plan''

report : Console e => State GlobalConfig Global e => Stats -> App e ()
report x = do
  putStrLn $ separator 80
  putStrLn $ !bold "Summary:"
  let nb = countTests x
  if nb == 0
     then putStrLn $ withOffset 2 "No test"
     else putStrLn $ removeTrailingNL $ unlines $ catMaybes
    [ guard (x.successes > 0) $>
        withOffset 2 "\{!ok} (Success): \{show x.successes} / \{show nb}"
    , guard (x.failures > 0) $>
        withOffset 2 "\{!ko} (Failure): \{show x.failures} / \{show nb}"
    , guard (x.errors > 0) $>
        withOffset 2 "\{!err}  (Errors): \{show x.errors} / \{show nb}"
    , guard (x.skipped > 0) $>
        withOffset 2 "\{!pending}  (Pending): \{show x.skipped} / \{show nb}"
    ]

filterTests : FileSystem (FSError :: e) =>
  Has [ State RunContext RunCommand
      , State GlobalConfig Global
      , Exception ReplicaError
      , Console
      ] e => (s, r : List Test) -> App e TestPlan
filterTests s r = do
  f <- filter <$> get RunContext
  debug $ "Filters: \{show f}"
  let (selected, rejected) = partition (keepTest f) s
  pure $ buildPlan selected (rejected ++ r)

getLastFailures : FileSystem (FSError :: e) =>
  Has [ State GlobalConfig Global
      , Exception ReplicaError
      , Console
      ] e => App e (List Test, 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 ["Can't parse JSON (invalid syntax)"]
  let Valid report = parseReport json
    | Error err => throw $ InvalidJSON err
  let notWorking = fst <$> filter (not . isFullSuccess . snd) report
  let (selected, rejected) = partition (flip elem notWorking . name) repl.tests
  debug $ "Previous invalid tests: \{show selected}"
  pure (selected, rejected)

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

extractReport : (Maybe String, List (Test, Either TestError TestResult)) ->
                List (String, Either TestError TestResult)
extractReport = map (mapFst name) . snd

export
suiteOutput : SystemIO (SystemError :: e) =>
  Has [ State RunContext RunCommand
      , State GlobalConfig Global
      , Console
      ] e =>
  Maybe String -> List (Test, Either TestError TestResult) -> App e ()
suiteOutput suite tests = do
  displaySuite suite
  traverse_ (uncurry (\t, r => new t (testOutput r))) tests

export
runReplica : SystemIO (SystemError :: TestError :: e) =>
  SystemIO (SystemError :: e) =>
  FileSystem (FSError :: TestError :: e) =>
  FileSystem (FSError :: e) =>
  SystemClock (TestError :: e) =>
  Console (TestError :: e) =>
  Has [ State RunContext RunCommand
      , State GlobalConfig Global
      , Exception ReplicaError
      , Console
      ] e => App e Stats
runReplica = do
  debug $ "Run: \{show !(get RunContext)}"
  rDir <- prepareReplicaDir
  plan <- defineActiveTests
  log $ displayPlan plan
  result <- runAllTests plan
  let logFile = lastRunLog rDir
  catchNew (writeFile logFile (show $ reportToJSON $ extractReport =<< result))
    (\err : FSError => throw $ CantAccessTestFile logFile)
  when !(interactive <$> get RunContext)
    (do putStrLn $ separator 80
        putStrLn $ !bold "Test results:"
        traverse_ (uncurry (\t, r => suiteOutput t r)) result)
  let stats = asStats $ map snd $ snd =<< result
  report stats
  pure stats

max_stars_repo_name: claymager/REPLica

max_issues_repo_name: claymager/REPLica

max_forks_repo_name: claymager/REPLica


text:
module Prims

%default total

x : Int
x = 94

foo : String
foo = "Ninety-Four"

bar : Char
bar = 'Z'

quux : Bool
quux = False

max_stars_repo_name: timmyjose-study/idris-from-the-docs

max_issues_repo_name: timmyjose-study/idris-from-the-docs

max_forks_repo_name: timmyjose-study/idris-from-the-docs


text:
foldlA : (a -> b -> a) -> a -> Vector (x::xs) b -> a
foldlA f e v with (flattenA v)
   | (_ ** v') = foldlA' f e v'
     where foldlA' : (a -> b -> a) -> a -> Vector [(S ys)] b -> a
           foldlA' f e v = foldl f e v

max_stars_repo_name: RossMeikleham/MSci-Project

max_issues_repo_name: RossMeikleham/MSci-Project

max_forks_repo_name: RossMeikleham/MSci-Project


text:
-- -------------------------------------------------------------- [ Parser.idr ]
-- Description : A command line argument parser
-- Copyright   : (c) Huw Campbell
-- --------------------------------------------------------------------- [ EOH ]
module Options.Applicative.Maybe
import Control.Monad.Trans

%default total
%access public export

record MaybeT (m : Type -> Type) (a : Type) where
  constructor MT
  runMaybeT : m (Maybe a)

Functor f => Functor (MaybeT f) where
    map f (MT g) = MT $ map (map f) g

Monad f => Applicative (MaybeT f) where
    pure x = MT $ pure $ Just x

    (MT f) <*> (MT a) = MT $ do Just h <- f | Nothing => pure Nothing
                                map (map h) a

Monad f => Alternative (MaybeT f) where
    empty = MT $ pure Nothing
    (MT a) <|> (MT b) = MT $ do Just x <- a | Nothing => b
                                pure $ Just x

MonadTrans MaybeT where
    lift x = MT $ map Just x

Monad f => Monad (MaybeT f) where
    (MT f) >>= k = MT $ do Just a <- f | Nothing => pure Nothing
                           runMaybeT (k a)

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

max_stars_repo_name: statebox/optparse-idris

max_issues_repo_name: statebox/optparse-idris

max_forks_repo_name: statebox/optparse-idris


text:
h : Nat -> () -> Nat
h x = \_ => (+) x 1

h' : Nat -> Lazy Nat
h' x = (+) x 1

{-

*11.2-InfiniteIO> h 1
\underscore => 2 : () -> Nat

*11.2-InfiniteIO> h' 1
Delay 2 : Lazy Nat

-}

max_stars_repo_name: ostera/asdf

max_issues_repo_name: ostera/asdf

max_forks_repo_name: ostera/asdf


text:
module lib.Library1

export
salute1 : String
salute1 = "Hello, from one idris library"


text:
module Rationals

import ZZ
import ZZUtils
import GCDZZ
import Divisors
import BoundedGCD

%default total

-- Everything in this file is total.

-- The functions below are completely based on the code from GCDZZ; they were written to improve
-- readability.

Quotient: (a: ZZ) -> (b: ZZ) -> (IsNonNegative a) -> (IsPositive b) -> (ZZ)
Quotient a b x y = Prelude.Pairs.DPair.fst (QuotRemZ a b x y)

Remainder: (a: ZZ) -> (b: ZZ) -> (IsNonNegative a) -> (IsPositive b) -> (ZZ)
Remainder a b x y = Prelude.Pairs.DPair.fst(Prelude.Pairs.DPair.snd (QuotRemZ a b x y))

%access public export

Pair : Type
Pair = (Integer, Integer)

ZZPair : Type
ZZPair = (ZZ, ZZ)

ZZtoDb : ZZ -> Double
ZZtoDb x = cast{from=Integer}{to=Double} (cast{from=ZZ}{to=Integer} x)

DbtoZZ : Double -> ZZ
DbtoZZ x = cast{from=Integer}{to=ZZ} (cast{from=Double}{to=Integer} x)

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

isFactorInt : Integer -> Integer -> Type  --Needed for defining Integer division
isFactorInt m n = (k : Integer ** (m * k = n))

divides : (m: Integer) -> (n: Integer) -> (k: Integer ** (m * k = n)) -> Integer
divides m n k = (fst k)

--Integer implemetation of gcd
CalcGCD : (Integer, Integer) -> Integer
CalcGCD (a, b) = case (decEq b 0) of
                      (Yes prf) => a
                      (No contra) => toIntegerNat (gcdAlgo (toNat a) (toNat b))

OnlyPositive : (x: Pair) -> Pair
OnlyPositive x = (if (fst x)>0 then fst x else (-1)*(fst x), if(snd x)>0 then (snd x) else (-1)*(snd x))

--Integer implemetation of gcd
gccd : (Integer, Integer) -> Integer
gccd x = CalcGCD (OnlyPositive x)

data ZZNotZero : ZZ -> Type where
  ZZOneNotZero : ZZNotZero 1
  ZZNegativeNotZero : ( n: ZZ ) -> ZZNotZero n -> ZZNotZero (-n)
  ZZPositiveNotZero : ( m: ZZ ) -> LTE 1 (fromIntegerNat (cast(m)))  -> ZZNotZero m

-- A section on the custom equality of Rationals

||| If a is not equal to zero and b is not equal to zero, their product is not equal to zero.
productNonZero: (NotZero a) -> (NotZero b) -> (NotZero (a*b))
productNonZero PositiveZ PositiveZ = PositiveZ
productNonZero PositiveZ NegativeZ = NegativeZ
productNonZero NegativeZ PositiveZ = NegativeZ
productNonZero NegativeZ NegativeZ = PositiveZ

|||A rational number is equal to its component representation (Numerator,Denominator)
pairIsComponents: (x: ZZPair) -> (x=((fst x), (snd x)))
pairIsComponents (a, b) = Refl

--Type for equality of two Rationals
EqRat : (x: ZZPair) -> (NotZero (snd x)) -> (y: ZZPair) -> (NotZero (snd y)) -> Type
EqRat x a y b = (fst x)*(snd y)=(snd x)*(fst y)

|||The analog of 'Refl' for equality of rationals.
EqRatRefl: (x: ZZPair) -> (a: NotZero (snd x)) -> (EqRat x a x a)
EqRatRefl x a = rewrite (multCommutativeZ (fst x) (snd x)) in
                  Refl

|||The analog of 'sym' for equality of rationals.
EqRatSym: (x: ZZPair) -> (a: NotZero (snd x)) -> (y: ZZPair) -> (b: NotZero (snd y)) -> (EqRat x a y b) -> (EqRat y b x a)
EqRatSym x a y b z = rewrite (multCommutativeZ (snd y) (fst x)) in
                     rewrite (multCommutativeZ (fst y) (snd x)) in
                      sym z

equalMeansEqualPairs: (x: ZZPair) -> (a: NotZero (snd x)) -> (y: ZZPair) -> (b: NotZero (snd y)) -> (x=y) -> (((fst x), (snd x)) = ((fst y), (snd y)))
equalMeansEqualPairs x a y b prf = rewrite sym (pairIsComponents x) in
                                   rewrite sym (pairIsComponents y) in
                                     prf

equalMeansCompEqual: (x: ZZPair) -> (a: NotZero (snd x)) -> (y: ZZPair) -> (b: NotZero (snd y)) -> (x=y) -> ((fst x)=(fst y), (snd x)=(snd y))
equalMeansCompEqual y a y b Refl = (Refl, Refl)

eqMeansEqRat: (x: ZZPair) -> (a: NotZero (snd x)) -> (y: ZZPair) -> (b: NotZero (snd y)) -> (x=y) -> (EqRat x a y b)
eqMeansEqRat y a y b Refl = rewrite (multCommutativeZ (fst y) (snd y)) in
                             Refl

|||(0,1) is "equal" to (0,k) for any nonzero k
reducedFormZeroLeft: {k: ZZ} -> (a: NotZero k) -> (EqRat (0,1) PositiveZ (0,k) a)
reducedFormZeroLeft {k} a = rewrite (multZeroLeftZeroZ (k)) in
                              Refl

|||(0,k) is "equal" to (0,1) for any nonzero k
reducedFormZeroRight: (k: ZZ) -> (a: NotZero k) -> (EqRat (0,k) a (0,1) PositiveZ )
reducedFormZeroRight k a = rewrite (multZeroRightZeroZ (k)) in
                              Refl

||| (1,1) is "equal" to (k,k) for any nonzero k
reducedFormOneLeft: {k: ZZ} -> (a: NotZero k) -> (EqRat (1,1) PositiveZ (k,k) a)
reducedFormOneLeft {k} a = Refl

||| (k,k) is "equal" to (1,1) for any nonzero k
reducedFormOneRight: (k: ZZ) -> (a: NotZero k) -> (EqRat (k,k) a (1,1) PositiveZ)
reducedFormOneRight k a = Refl
|||If a = b and c = d, a*c = b*d
multEqualEqual: (a: ZZ) -> (b: ZZ) -> (c: ZZ) -> (d: ZZ) -> (a=b) -> (c=d) -> (a*c=b*d)
multEqualEqual b b d d Refl Refl = Refl

-- some helper functions for the first case of transitivity

transH1: {x: ZZPair} -> {y: ZZPair} -> {z: ZZPair} -> (((fst x)*(snd y)) = ((snd x)*(fst y))) -> (((fst y)*(snd z)) = ((snd y)*(fst z))) ->
((((fst x)*(snd y))*((fst y)*(snd z))) = (((snd x)*(fst y))*((snd y)*(fst z))))
transH1 {x} {y} {z} prf prf1 = (multEqualEqual ((fst x)*(snd y)) ((snd x)*(fst y)) ((fst y)*(snd z)) ((snd y)*(fst z)) prf prf1)

transH2: {x: ZZPair} -> {y: ZZPair} -> {z: ZZPair} -> ((((fst x)*(snd y))*((fst y)*(snd z))) = (((snd x)*(fst y))*((snd y)*(fst z))))
-> ((((fst x)*(snd z))*((fst y)*(snd y))) = (((snd x)*(fst z))*((fst y)*(snd y))))
transH2 {x} {y} {z} prf = rewrite (sym (multAssociativeZ (fst x) (snd z) ((fst y)*(snd y)) ) ) in
                          rewrite (sym (multAssociativeZ (snd x) (fst z) ((fst y)*(snd y)) ) ) in
                          rewrite (multCommutativeZ (fst y) (snd y)) in
                          rewrite (multAssociativeZ (snd z) (snd y) (fst y)) in
                          rewrite (multAssociativeZ (fst x) ((snd z)*(snd y)) (fst y) ) in
                          rewrite (multCommutativeZ (snd z) (snd y)) in
                          rewrite (multAssociativeZ (fst z) (snd y) (fst y)) in
                          rewrite (multCommutativeZ (fst z) (snd y)) in
                          rewrite (multAssociativeZ (fst x) (snd y) (snd z)) in
                          rewrite (multCommutativeZ ((snd y)*(fst z)) (fst y)) in
                          rewrite (multAssociativeZ (snd x) (fst y) ((snd y)*(fst z))) in
                          rewrite (sym (multAssociativeZ ((fst x)*(snd y)) (snd z) (fst y))) in
                          rewrite (multCommutativeZ (snd z) (fst y)) in
                          prf

transH3: {x: ZZPair} -> {y: ZZPair} -> {z: ZZPair} -> ((((fst x)*(snd z))*((fst y)*(snd y))) = (((snd x)*(fst z))*((fst y)*(snd y))))
-> (b: NotZero (snd y)) -> (k: NotZero (fst y)) -> (((fst x)*(snd z)) = ((snd x)*(fst z)))
transH3 {x} {y} {z} prf b k = (multRightCancelZ ((fst x)*(snd z)) ((snd x)*(fst z)) ((fst y)*(snd y)) (productNonZero k b) prf)

|||Nothing is both zero and nonzero.
NotZeroAndNonZero: (k: ZZ) -> (k=0) -> (NotZero k) -> Void
NotZeroAndNonZero (Pos (S _)) Refl PositiveZ impossible
NotZeroAndNonZero (NegS _) Refl NegativeZ impossible

|||The integers are an integral domain.
ZZIntegralDomain: (a: ZZ) -> (b: ZZ) -> (a*b=0) -> (NotZero b) -> (a=0)
ZZIntegralDomain a b prod bNZ = case (decZero a) of
                                    (Yes aNZ) => void (NotZeroAndNonZero (a*b) prod (productNonZero aNZ bNZ))
                                    (No contra) => notNotZeroThenZero (contra)

flipSidesAndTerms: (a: ZZ) -> (b: ZZ) -> (c: ZZ) -> (d: ZZ) -> (a*b=c*d) -> (d*c=b*a)
flipSidesAndTerms a b c d prf = rewrite (multCommutativeZ (b) (a)) in
                                rewrite (multCommutativeZ (d) (c)) in
                                  sym prf

|||If ab=cd and d =0 but b is not zero, then a is zero.
zeroProductZero1: (a: ZZ) -> (b: ZZ) -> (c: ZZ) -> (d: ZZ) -> (a*b=c*d) -> (d = 0) -> (NotZero b) -> (a=0)
zeroProductZero1 a b c d prod dZ bNZ = ZZIntegralDomain (a) (b) (trans (prod) (trans (multEqualEqual c c d (Pos 0) Refl dZ) (multZeroRightZeroZ (c)) )) (bNZ)

|||If ab=cd and a=0 but c is not zero, then d is zero.
zeroProductZero2: (a: ZZ) -> (b: ZZ) -> (c: ZZ) -> (d: ZZ) -> (a*b=c*d) -> (a = 0) -> (NotZero c) -> (d=0)
zeroProductZero2 a b c d prod aZ cNZ = zeroProductZero1 d c b a (flipSidesAndTerms a b c d prod) aZ cNZ

|||If the numerator is zero, the fraction is zero.
allZeroesSame: (x: ZZPair) -> (a: NotZero (snd x)) -> (z: ZZPair) -> (c: NotZero (snd z)) -> (fst x = 0) -> (fst z = 0)
-> EqRat x a z c
allZeroesSame x a z c prf prf1 = rewrite prf in
                                 rewrite prf1 in
                                 rewrite multZeroLeftZeroZ (snd z) in
                                 rewrite multZeroRightZeroZ (snd x) in
                                  Refl

|||The analog of 'trans' for rationals.
EqRatTrans: (x: ZZPair) -> (a: NotZero (snd x)) -> (y: ZZPair) -> (b: NotZero (snd y)) ->
(z: ZZPair) -> (c: NotZero (snd z)) -> (EqRat x a y b) -> (EqRat y b z c) -> (EqRat x a z c)
EqRatTrans x a y b z c pxy pyz = case (decZero (fst y)) of
                                      (Yes k) => (transH3 {x} {y} {z} (transH2 {x} {y} {z} (transH1 {x} {y} {z} pxy pyz)) b k )
                                      (No contra) => (allZeroesSame x a z c (zeroProductZero1 (fst x) (snd y) (snd x) (fst y) pxy (notNotZeroThenZero (contra)) b ) (zeroProductZero2 (fst y) (snd z) (snd y) (fst z) pyz (notNotZeroThenZero (contra)) b ))

-- NOTE: there is another case to be filled in. In the first case, cancellation is possible if the
-- numerator is nonzero. However, if the numerator of Y is zero, then it remains to be shown that
-- X and Z are (0,(snd x)) and (0,(snd z)) respectively (and are thus 'equal').

make_rational : (p: Nat) -> (q: ZZ) -> ZZNotZero q -> ZZPair
make_rational p q x = (fromInt(toIntegerNat(p)), q)

InclusionMap : (n : Nat) -> ZZPair --Includes the naturals in Q
InclusionMap n = make_rational n 1 ZZOneNotZero

AddRationals : (x: ZZPair) -> NotZero (snd x) -> (y: ZZPair) -> NotZero (snd y) -> ZZPair
AddRationals x a y b = ((fst x)*(snd y) + (snd x)*(fst y), (snd x)*(snd y))

MultiplyRationals : (x: ZZPair) -> NotZero (snd x) -> (y: ZZPair) -> NotZero (snd y) -> ZZPair
MultiplyRationals x a y b =((fst x)*(fst y), (snd x)*(snd y))

MultInverse : (x: ZZPair) -> NotZero (fst x) -> NotZero (snd x) -> ZZPair
MultInverse x y z = ((snd x), (fst x))

AddInverse : (x: ZZPair) -> NotZero (snd x) -> ZZPair
AddInverse x a = (-(fst x), (snd x))

Subtraction : (x: ZZPair) -> NotZero (snd x) -> (y: ZZPair) -> NotZero (snd y) -> ZZPair
Subtraction x a y b = AddRationals x a (AddInverse y b) b

Division : (x: ZZPair) -> NotZero (snd x) -> (y: ZZPair) -> NotZero (fst y) -> NotZero (snd y) -> ZZPair
Division x a y b c = MultiplyRationals x a (MultInverse y b c) b

Scaling: (a: ZZ) -> (x: ZZPair) -> ZZPair
Scaling a x = (a*(fst x), (snd x))

remZeroDivisible: (a: ZZ) -> (b: ZZ) -> (quot: ZZ) -> (rem: ZZ) -> (a = rem + quot*b) -> (rem = 0) -> (a=quot*b)
remZeroDivisible a b quot rem prf prf1 = rewrite sym (plusZeroLeftNeutralZ (quot*b)) in
                                         rewrite sym prf1 in
                                         prf

IsRationalZPOS: (x: ZZPair) -> (prf1 :IsNonNegative (fst x)) -> (prf2: IsPositive (snd x)) -> Either (quot: ZZ ** ((fst x)=quot*(snd x))) (NotZero (fst (snd (QuotRemZ (fst x) (snd x) prf1 prf2) )) )
IsRationalZPOS x prf1 prf2 = case (decEq (fst (snd (QuotRemZ (fst x) (snd x) prf1 prf2))) (Pos Z)) of
                          (Yes prf) => Left ( (Quotient (fst x) (snd x) prf1 prf2) **
                          (remZeroDivisible (fst x) (snd x) (Quotient (fst x) (snd x) prf1 prf2) (Remainder (fst x) (snd x) prf1 prf2) (Prelude.Basics.fst (Prelude.Pairs.DPair.snd (Prelude.Pairs.DPair.snd (QuotRemZ (fst x) (snd x) prf1 prf2)) )) prf ) )
                          (No contra) => Right (nonZeroNotZero (fst (snd (QuotRemZ (fst x) (snd x) prf1 prf2))) contra)

CheckIsQuotientZ: (a: ZZ) -> (b: ZZ) -> (NotZero b) -> Either (quot: ZZ ** (a=quot*b)) (ZZPair)
CheckIsQuotientZ a (Pos Z) x impossible
CheckIsQuotientZ (Pos Z) (Pos (S j)) x = case ((IsRationalZPOS ((Pos Z), (Pos (S j))) NonNegative Positive)) of
                                            (Left l) => (Left l)
                                            (Right r) => Right ((Pos Z),(Pos (S j)))
CheckIsQuotientZ (Pos (S k)) (Pos (S j)) x = case ((IsRationalZPOS ((Pos (S k)), (Pos (S j))) NonNegative Positive)) of
                                            (Left l) => (Left l)
                                            (Right r) => Right ((Pos (S k)), (Pos (S j)))
CheckIsQuotientZ (NegS k) (Pos (S j)) x = case ((IsRationalZPOS ((Pos (S k)), (Pos (S j))) NonNegative Positive)) of
                                            (Left l) =>  Left (QRproof1 (Pos (S k)) (Pos (S j)) Refl Refl l)
                                            (Right r) => Right ((Pos (S k)), (Pos (S j)))
CheckIsQuotientZ (Pos Z) (NegS j) x = Left (Pos Z ** Refl)
CheckIsQuotientZ (Pos (S k)) (NegS j) x = case ((IsRationalZPOS ((Pos (S k)), (Pos (S j))) NonNegative Positive)) of
                                            (Left l) =>  Left (QRproof3 (Pos (S k)) (Pos (S j)) Refl Refl l)
                                            (Right r) => Right ((Pos (S k)), (Pos (S j)))
CheckIsQuotientZ (NegS k) (NegS j) x = case ((IsRationalZPOS ((Pos (S k)), (Pos (S j))) NonNegative Positive)) of
                                            (Left l) =>  Left (QRproof4 (Pos (S k)) (Pos (S j)) Refl Refl l)
                                            (Right r) => Right ((Pos (S k)), (Pos (S j)))

-- The following section is on simplification of rationals. There was a function written earlier,
-- called simplifyRational which used the existence of the numeric type 'Double' in Idris so that
-- simplification could actually be done. This has now been superseded by the functions below as
-- the GCD with proof has now been implemented.

-- aByd and bByd are taken from the file 'Divisors.idr' (by Shafil)

|||Extracts a/gcd(a,b) from the definition of GCDZ
aBydNum:GCDZ a b d ->ZZ
aBydNum dGcdab = (fst (fst (fst (snd dGcdab))))

|||Extracts b/gcd(a,b) from the definition of GCDZ
bBydDen:GCDZ a b d ->ZZ
bBydDen dGcdab = (fst (snd (fst (snd dGcdab))))

|||A helper routine which simplifies a rational number.
simplification: (a: ZZ) -> (b: ZZ) -> (NotBothZeroZ a b) -> (y: ZZPair ** (GCDZ (fst y) (snd y) 1))
simplification a b prf = ((aBydNum (snd (gcdZZ a b prf)), bBydDen (snd (gcdZZ a b prf))) ** (divideByGcdThenGcdOne (snd (gcdZZ a b prf))))

|||If b is not zero, then it is not the case that both 'a' and 'b' are zero.
NotZeroNotBothZero: (a: ZZ) -> (b: ZZ) -> (NotZero b) -> (NotBothZeroZ a b)
NotZeroNotBothZero a (Pos (S k)) PositiveZ = RightPositive
NotZeroNotBothZero a (NegS k) NegativeZ = RightNegative

|||This takes a rational number and simplifies it and provides a proof that it is simplified
|||(that is, the numerator and denominator have GCD 1)
simplifyWithProof: (x: ZZPair) -> (NotZero (snd x)) -> (y: ZZPair ** (GCDZ (fst y) (snd y) 1))
simplifyWithProof x prf = (simplification (fst x) (snd x) (NotZeroNotBothZero (fst x) (snd x) prf))

|||Extracting the simplified rational from the dependent pair.
simplifyRationalProof: (x: ZZPair) -> (NotZero (snd x)) -> ZZPair
simplifyRationalProof x prf = fst (simplifyWithProof x prf)

-- below is the old function simplifyRational. I need to make the GCD-based code above
-- compatible with the code that implements simplifyRational before replacing it.

--To prove that the SimplifyRational works, we can just check if the output is equal to the input
-- To be done
simplifyRational : (x : ZZPair) -> ZZPair
simplifyRational (a, b) = (sa, sb) where
  sa = DbtoZZ (da / g) where
    da = ZZtoDb a
    g = cast {from=Integer} {to=Double}
      (gccd (cast {from=ZZ} {to=Integer}a,cast {from=ZZ} {to=Integer}b))
  sb = DbtoZZ (db / g) where
    db = ZZtoDb b
    g = cast {from=Integer} {to=Double}
      (gccd (cast {from=ZZ} {to=Integer}a,cast {from=ZZ} {to=Integer}b))

--Above, I will need to supply a proof that the GCD divides the two numbers. Then, the function defined above will produce the rational in simplified form.

xAndInverseNotZeroPlus : (x: ZZPair) -> (k: NotZero (snd x)) -> (NotZero (snd (AddInverse x k)))
xAndInverseNotZeroPlus x k = k

xAndInverseNotZeroMult : (x: ZZPair) -> (j: NotZero (fst x)) -> (k: NotZero (snd x)) -> (NotZero (snd (MultInverse x j k)))
xAndInverseNotZeroMult x j k = j

{-
FirstIsInverted : (x: ZZPair) -> (k: ZZNotZero (snd x)) -> (a: ZZ) -> (a = (fst x)) -> ((-a) = fst (AddInverse x k))
FirstIsInverted x k a prf = (apZZ (\x => -x) a (fst x) prf)

SecondStaysSame : (x: ZZPair) -> (k: ZZNotZero (snd x)) -> (b: ZZ) -> (b = (snd x)) -> (b = (snd (AddInverse x k)))
SecondStaysSame x k b prf = (apZZ (\x => x) b (snd x) prf)

xplusinverse: (x: ZZPair) -> (k: ZZNotZero (snd x)) -> ZZPair
xplusinverse x k = AddRationals x k (AddInverse x k) (xAndInverseNotZero x k)

addinverselemma: (a: ZZ) -> (b: ZZ) -> ((-a)=b) -> (a + b = ((-a) + a)) -> ((-a)+a =0 ) -> (a + b = 0)
addinverselemma a b prf prf1 prf2 = trans prf1 prf2

addinverseFST: (x: ZZPair) -> (k: ZZNotZero (snd x)) -> (a: ZZ) -> (a = (fst x)) -> (fst (AddInverse x k) = b) -> ((-a) = b)
addinverseFST x k a prf prf1 = trans (FirstIsInverted x k a prf) (prf1)

addinverseSND: (x: ZZPair) -> (k: ZZNotZero (snd x)) -> (c: ZZ) -> (c = (snd x)) -> (snd (AddInverse x k) = b) -> (c = b)
addinverseSND x k c prf prf1 = trans (SecondStaysSame x k c prf) (prf1)
-}

-- Proving the field axioms to show that Q is a field.
-- The first section concerns those axioms which involve only one or two elements of Q.

|||AddRationals is commutative
plusCommutativeQ: (x: ZZPair) -> (a: NotZero (snd x)) -> (y: ZZPair) -> (b: NotZero (snd y)) -> (AddRationals x a y b) = (AddRationals y b x a)
plusCommutativeQ x a y b = rewrite (multCommutativeZ (snd y) (snd x)) in
                           rewrite (plusCommutativeZ ((fst x)*(snd y)) ((snd x)*(fst y))) in
                           rewrite (multCommutativeZ (snd x) (fst y)) in
                           rewrite (multCommutativeZ (snd y) (fst x)) in
                           Refl

|||MultiplyRationals is commutative
multCommutativeQ: (x: ZZPair) -> (a: NotZero (snd x)) -> (y: ZZPair) -> (b: NotZero (snd y)) -> (MultiplyRationals x a y b) = (MultiplyRationals y b x a)
multCommutativeQ x a y b = rewrite (multCommutativeZ (fst x) (fst y)) in
                           rewrite (multCommutativeZ (snd x) (snd y)) in
                           Refl

||| Zero is the right additive identity, meaning that x + 0 = x
zeroAddIdentityRight: (x: ZZPair) -> (a: NotZero (snd x)) -> ((AddRationals x a (0,1) PositiveZ) = x)
zeroAddIdentityRight x a = rewrite (multZeroRightZeroZ (snd x)) in
                      rewrite (multOneRightNeutralZ (fst x)) in
                      rewrite (plusZeroRightNeutralZ (fst x)) in
                      rewrite (multOneRightNeutralZ (snd x)) in
                      rewrite (sym (pairIsComponents x)) in
                      Refl

||| Zero is the left additive identity, meaning that 0 + x = x
zeroAddIdentityLeft: (x: ZZPair) -> (a: NotZero (snd x)) -> ((AddRationals (0,1) PositiveZ x a) = x)
zeroAddIdentityLeft x a = rewrite (multZeroLeftZeroZ (snd x)) in
                      rewrite (multOneLeftNeutralZ (fst x)) in
                      rewrite (plusZeroLeftNeutralZ (fst x)) in
                      rewrite (multOneLeftNeutralZ (snd x)) in
                      rewrite ((pairIsComponents x)) in
                      Refl

|||One is the right multiplicative identity (x*1=x)
oneMultIdentityRight: (x: ZZPair) -> (a: NotZero (snd x)) -> ((MultiplyRationals x a (1,1) PositiveZ) = x)
oneMultIdentityRight x a = rewrite (multOneRightNeutralZ (fst x)) in
                           rewrite (multOneRightNeutralZ (snd x)) in
                           rewrite (sym (pairIsComponents x)) in
                           Refl

|||One is the left multiplicative identity (1*x=x)
oneMultIdentityLeft: (x: ZZPair) -> (a: NotZero (snd x)) -> ((MultiplyRationals (1,1) PositiveZ  x a) = x)
oneMultIdentityLeft x a = rewrite (multOneLeftNeutralZ (fst x)) in
                           rewrite (multOneLeftNeutralZ (snd x)) in
                           rewrite ((pairIsComponents x)) in
                           Refl

||| x plus its additive inverse is equal to (0,(snd x)*(snd x)). A custom equality type is probably required to set
||| this equal to (0,1).
addInverseLeft: (x: ZZPair) -> (a: NotZero (snd x)) -> ((AddRationals x a (AddInverse x a) (xAndInverseNotZeroPlus x a)) = ((Pos 0), (snd x)*(snd x)))
addInverseLeft x a = rewrite (multCommutativeZ (fst x) (snd x)) in
                     rewrite (multNegateRightZ (snd x) (fst x)) in
                     rewrite (plusNegateInverseLZ ((snd x)*(fst x)) ) in
                     Refl

||| The additive inverse of x plus itself is equal to (0,(snd x)*(snd x)). A custom equality type is probably required to set
||| this equal to (0,1).
addInverseRight: (x: ZZPair) -> (a: NotZero (snd x)) -> ((AddRationals (AddInverse x a) (xAndInverseNotZeroPlus x a) x a) = (0, (snd x)*(snd x)))
addInverseRight x a = rewrite (multCommutativeZ (snd x) (fst x)) in
                      rewrite (multNegateLeftZ (fst x) (snd x)) in
                      rewrite (plusNegateInverseRZ ((fst x)*(snd x)) ) in
                      Refl

|||x times its multiplicative inverse is equal to ((fst x)*(snd x), (fst x)*(snd x)). A custom equality type is probably required to set
||| this equal to (1,1).
multInverseLeft: (x: ZZPair) -> (a: NotZero (fst x)) -> (b: NotZero (snd x)) ->
(MultiplyRationals x b (MultInverse x a b) (xAndInverseNotZeroMult x a b)) = ((fst x)*(snd x), (fst x)*(snd x))
multInverseLeft x a b = rewrite (multCommutativeZ (snd x) (fst x)) in
                        Refl

|||The multiplicative inverse of x times itself is equal to ((fst x)*(snd x), (fst x)*(snd x)). A custom equality type is probably required to set
||| this equal to (1,1).
multInverseRight: (x: ZZPair) -> (a: NotZero (fst x)) -> (b: NotZero (snd x)) ->
(MultiplyRationals (MultInverse x a b) (xAndInverseNotZeroMult x a b) x b ) = ((snd x)*(fst x), (snd x)*(fst x))
multInverseRight x a b = rewrite (multCommutativeZ (snd x) (fst x)) in
                         Refl

|||AddRationals is associative. It requires the helper function productNonZero.
plusAssociativeQ: (x: ZZPair) -> (a: NotZero (snd x)) -> (y: ZZPair) -> (b: NotZero (snd y)) -> (z: ZZPair) -> (c: NotZero (snd z)) ->
((AddRationals (AddRationals x a y b) (productNonZero a b) z c) = (AddRationals x a (AddRationals y b z c) (productNonZero b c)))
plusAssociativeQ x a y b z c = rewrite (multAssociativeZ (snd x) (snd y) (snd z)) in
                               rewrite (multDistributesOverPlusLeftZ ((fst x)*(snd y)) ((snd x)*(fst y)) (snd z)) in
                               rewrite (sym (plusAssociativeZ (((fst x)*(snd y))*(snd z)) (((snd x)*(fst y))*(snd z)) (((snd x)*(snd y))*(fst z)) )) in
                               rewrite (sym (multAssociativeZ (snd x) (snd y) (fst z))) in
                               rewrite (sym (multAssociativeZ (snd x) (fst y) (snd z))) in
                               rewrite (sym (multAssociativeZ (fst x) (snd y) (snd z))) in
                               rewrite (multDistributesOverPlusRightZ (snd x) ((fst y)*(snd z)) ((snd y)*(fst z)) ) in
                               Refl

|||MultiplyRationals is associative. It requires the helper function productNonZero.
multAssociativeQ: (x: ZZPair) -> (a: NotZero (snd x)) -> (y: ZZPair) -> (b: NotZero (snd y)) -> (z: ZZPair) -> (c: NotZero (snd z)) ->
((MultiplyRationals (MultiplyRationals x a y b) (productNonZero a b) z c) = (MultiplyRationals x a (MultiplyRationals y b z c) (productNonZero b c)))
multAssociativeQ x a y b z c = rewrite sym (multAssociativeZ (fst x) (fst y) (fst z)) in
                               rewrite sym (multAssociativeZ (snd x) (snd y) (snd z)) in
                               Refl