text:
||| Signal raising and handling.
|||
||| NOTE that there are important differences between
||| what can be done out-of-box in Windows and POSIX based
||| operating systems. This module tries to honor both
||| by putting things only available in POSIX environments
||| into appropriately named namespaces or data types.
module System.Signal

import Data.Fuel
import Data.List
import Data.List.Elem
import System.Errno

%default total

signalFFI : String -> String
signalFFI fn = "C:" ++ fn ++ ", libidris2_support, idris_signal.h"

--
-- Signals
--
%foreign signalFFI "sighup"
prim__sighup : Int

%foreign signalFFI "sigint"
prim__sigint : Int

%foreign signalFFI "sigabrt"
prim__sigabrt : Int

%foreign signalFFI "sigquit"
prim__sigquit : Int

%foreign signalFFI "sigill"
prim__sigill : Int

%foreign signalFFI "sigsegv"
prim__sigsegv : Int

%foreign signalFFI "sigtrap"
prim__sigtrap : Int

%foreign signalFFI "sigfpe"
prim__sigfpe : Int

%foreign signalFFI "sigusr1"
prim__sigusr1 : Int

%foreign signalFFI "sigusr2"
prim__sigusr2 : Int

public export
data PosixSignal = ||| Hangup (i.e. controlling terminal closed)
                   SigHUP
                 | ||| Quit
                   SigQUIT
                 | ||| Trap (as used by debuggers)
                   SigTRAP
                 | SigUser1
                 | SigUser2

export
Eq PosixSignal where
  SigHUP   == SigHUP   = True
  SigQUIT  == SigQUIT  = True
  SigTRAP  == SigTRAP  = True
  SigUser1 == SigUser1 = True
  SigUser2 == SigUser2 = True
  _ == _ = False

public export
data Signal = ||| Interrupt (e.g. ctrl+c pressed)
              SigINT
            | ||| Abnormal termination
              SigABRT
            | ||| Ill-formed instruction
              SigILL
            | ||| Segmentation fault
              SigSEGV
            | ||| Floating-point error
              SigFPE
            | ||| Signals only available on POSIX operating systems
              SigPosix PosixSignal

export
Eq Signal where
  SigINT   == SigINT   = True
  SigABRT  == SigABRT  = True
  SigILL   == SigILL   = True
  SigSEGV  == SigSEGV  = True
  SigFPE   == SigFPE   = True
  SigPosix x == SigPosix y = x == y
  _ == _ = False

signalCode : Signal -> Int
signalCode SigINT   = prim__sigint
signalCode SigABRT  = prim__sigabrt
signalCode SigILL   = prim__sigill
signalCode SigSEGV  = prim__sigsegv
signalCode SigFPE   = prim__sigfpe
signalCode (SigPosix SigHUP  ) = prim__sighup
signalCode (SigPosix SigQUIT ) = prim__sigquit
signalCode (SigPosix SigTRAP ) = prim__sigtrap
signalCode (SigPosix SigUser1) = prim__sigusr1
signalCode (SigPosix SigUser2) = prim__sigusr2

toSignal : Int -> Maybe Signal
toSignal (-1) = Nothing
toSignal x    = lookup x codes
  where
    codes : List (Int, Signal)
    codes = [
              (prim__sigint , SigINT)
            , (prim__sigabrt, SigABRT)
            , (prim__sigill , SigILL)
            , (prim__sigsegv, SigSEGV)
            , (prim__sigfpe , SigFPE)
            , (prim__sighup , SigPosix SigHUP)
            , (prim__sigquit, SigPosix SigQUIT)
            , (prim__sigtrap, SigPosix SigTRAP)
            , (prim__sigusr1, SigPosix SigUser1)
            , (prim__sigusr2, SigPosix SigUser2)
            ]

--
-- Signal Handling
--
%foreign signalFFI "ignore_signal"
prim__ignoreSignal : Int -> PrimIO Int

%foreign signalFFI "default_signal"
prim__defaultSignal : Int -> PrimIO Int

%foreign signalFFI "collect_signal"
prim__collectSignal : Int -> PrimIO Int

%foreign signalFFI "handle_next_collected_signal"
prim__handleNextCollectedSignal : PrimIO Int

%foreign signalFFI "send_signal"
prim__sendSignal : Int -> Int -> PrimIO Int

%foreign signalFFI "raise_signal"
prim__raiseSignal : Int -> PrimIO Int

||| An Error represented by a code. See
||| relevant `errno` documentation.
||| https://man7.org/linux/man-pages/man3/errno.3.html
public export
data SignalError = Error Int

getError : HasIO io => io SignalError
getError = Error <$> getErrno

isError : Int -> Bool
isError (-1) = True
isError _    = False

||| Ignore the given signal.
||| Be careful doing this, as most signals have useful
||| default behavior -- you might want to set the signal
||| to its default behavior instead with `defaultSignal`.
export
ignoreSignal : HasIO io => Signal -> io (Either SignalError ())
ignoreSignal sig = do
  res <- primIO $ prim__ignoreSignal (signalCode sig)
  case isError res of
       False => pure $ Right ()
       True  => Left <$> getError

||| Use the default handler for the given signal.
||| You can use this function to unset custom
||| handling of a signal.
export
defaultSignal : HasIO io => Signal -> io (Either SignalError ())
defaultSignal sig = do
  res <- primIO $ prim__defaultSignal (signalCode sig)
  case isError res of
       False => pure $ Right ()
       True  => Left <$> getError

||| Collect the given signal.
|||
||| This replaces the existing handling of the given signal
||| and instead results in Idris collecting occurrences of
||| the signal until you call `handleNextCollectedSignal`.
|||
||| First, call `collectSignal` for any number of signals.
||| Then, call `handleNextCollectedSignal` in each main loop
||| of your program to retrieve (and mark as handled) the next
||| signal that was collected, if any.
|||
||| Signals are not queued, so the return order of signals is
||| not specified and signals may be deduplicated.
export
collectSignal : HasIO io => Signal -> io (Either SignalError ())
collectSignal sig = do
  res <- primIO $ prim__collectSignal (signalCode sig)
  case isError res of
       False => pure $ Right ()
       True  => Left <$> getError

||| Get next collected signal under the pretense of handling it.
|||
||| Calling this "marks" the signal as handled so the next time
||| this function is called you will retrieve the next unhandled
||| signal instead of the same signal again.
|||
||| You get back Nothing if there are no pending signals.
export
handleNextCollectedSignal : HasIO io => io (Maybe Signal)
handleNextCollectedSignal =
  toSignal <$> primIO prim__handleNextCollectedSignal

||| Get many collected signals and mark them as handled.
|||
||| Use `forever` as your fuel if you don't want or need to
||| retain totality. Alternatively, pick a max number to
||| retrieve and use `limit/1` as your fuel.
export
handleManyCollectedSignals : HasIO io => Fuel -> io (List Signal)
handleManyCollectedSignals Dry = pure []
handleManyCollectedSignals (More fuel) = do
  Just next <- handleNextCollectedSignal
    | Nothing => pure []
  pure $ next :: !(handleManyCollectedSignals fuel)

||| Send a signal to the current process.
export
raiseSignal : HasIO io => Signal -> io (Either SignalError ())
raiseSignal sig = do
  res <- primIO $ prim__raiseSignal (signalCode sig)
  case isError res of
       False => pure $ Right ()
       True  => Left <$> getError

namespace Posix
  ||| Send a signal to a POSIX process using a PID to identify the process.
  export
  sendSignal : HasIO io => Signal -> (pid : Int) -> io (Either SignalError ())
  sendSignal sig pid = do
    res <- primIO $ prim__sendSignal pid (signalCode sig)
    case isError res of
         False => pure $ Right ()
         True  => Left <$> getError


text:
module Test

import Data.List
import Data.Vect
import Data.Either
import Data.Maybe
import Data.String
import Data.Ref
import Data.Stream
import Control.Monad.Reader
import Control.Monad.Writer
import Control.Monad.Either
import Control.Monad.Identity
import Control.Monad.Free
import Control.Monad.State
import Control.Monad.List

import Control.EffectAlgebra
import Control.Effect.Exception
import Control.Effect.Labelled
import Control.Effect.Lift
import Control.Effect.Reader
import Control.Effect.Writer
import Control.Effect.State
import Control.Effect.NonDet
import Control.Cont.Void
import Control.Cont.State
import Control.Cont.Thread
import Control.Cont.Out
import Control.Cont.IO
import Control.Cont.Exception

-------------------------------------
throwSnapshot : (Syntax sig, Inj (EitherC (e, s)) sig, Inj (StateC s) sig) => e -> Free sig a
throwSnapshot err = do
  v <- Cont.State.get {s}
  throw (err, v)

decr : (Syntax sig, Inj (StateC Int) sig, Inj (EitherC ()) sig) => Free sig ()
decr = do
  x <- Cont.State.get {s = Int}
  if x > 0 then Cont.State.put (x - 1)
     else throw ()

incrC : (Syntax sig, Inj (StateC Int) sig) => Free sig ()
incrC = do
  x <- Cont.State.get {s = Int}
  Cont.State.put (x + 1)

testStateExc : Syntax sig
           => (s : Inj (StateC Int) sig)
           => (e : Inj (EitherC (String, Int)) sig)
           => Free sig (String, Int)
testStateExc = do
  catch {e = (String, Int)} (incrC >> throwSnapshot {s = Int} "thrown") \(str, i) => do
    incrC >> return (str ++ "-return", i + 22)

testStateExcRun : Either (String, Int) (Int, (String, Int))
testStateExcRun = runVoidC . runEitherC . runStateC 3 $ testStateExc
  {e = T L R}
  {s = L}

-------------------------------------

tripleDecr : Syntax sig => (s : Inj (StateC Int) sig) => (e : Inj (EitherC ()) sig) => Free sig ()
tripleDecr = decr >> catch (decr >> decr) return

tripleDecrInst : Free (StateC Int :+: (EitherC () :+: VoidE)) ()
tripleDecrInst = tripleDecr
  {e = MkInj (Inr . Inl)}
  {s = MkInj Inl}

tripleDecrInst' : Free (EitherC () :+: (StateC Int :+: VoidE)) ()
tripleDecrInst' = tripleDecr
  {e = MkInj Inl}
  {s = MkInj (Inr . Inl)}

runLocal : Either () (Int, ())
runLocal = runVoidC . runEitherC . runStateC 2 $ tripleDecrInst

runGlobal : (Int, Either () ())
runGlobal = runVoidC . runStateC 2 . runEitherC $ tripleDecrInst'

-----------------------

%hide Control.Monad.Writer.Interface.tell
%hide Control.Monad.Reader.Interface.ask

testFused : (al : Algebra sig m)
         => (r : Inj (ReaderE Nat) sig)
         => (w : Inj (WriterE (List Nat)) sig)
         => m String
testFused = do
  x <- ask
  tell {w = List Nat} [x + 1]
  tell {w = List Nat} [x + 3, x + 2]
  pure "Done"

handleFused : ReaderT Nat (WriterT (List Nat) Identity) String
handleFused = testFused {sig = ReaderE Nat :+: WriterE (List Nat) :+: VoidE}
               {r = L}
               {w = T L R}
               {al = Reader.Algebra.Reader
                      @{Writer.Algebra.ConcatLeft}}

runFused : List Nat
runFused = runIdentity . map snd . runWriterT . runReaderT 20 $ handleFused

-----------------------

testEitherE : (al : Algebra sig m)
           => (r : Inj (ReaderE Nat) sig)
           => (w : Inj (WriterE (List Nat)) sig)
           => (e : Inj (EitherE String) sig)
           => (toThrow : Bool)
           -> m String
testEitherE toThrow = do
  x <- ask
  tell {w = List Nat} [1, x]
  tell {w = List Nat} [3, 2]
  r <- try {e = String}
        (do tell {w = List Nat} [6, 5, 4]
            if toThrow then fail "fail" else pure "pure")
    (\er => pure "on throw")
  pure r

handleEitherE : Bool -> (WriterT (List Nat) $ ReaderT Nat $ EitherT String Identity) String
handleEitherE x = testEitherE x
  {sig = WriterE (List Nat) :+: ReaderE Nat :+: EitherE String :+: VoidE}
  {w = L}
  {r = T L R}
  {e = T (T L R) R}
  {al = Algebra.ConcatLeft @{%search} @{Algebra.Reader @{Algebra.Either}}}

runEitherE : Bool -> Either String (String, List Nat)
runEitherE x = runIdentity . runEitherT . runReaderT 0 . runWriterT $ handleEitherE x

-----------------------

readerSum : (rx : InjL "x" (ReaderE Int) sig)
         => (ry : InjL "y" (ReaderE Int) sig)
         => (al : Algebra sig m)
         => m Int
readerSum = do
  a <- labelled "x" Ask
  b <- labelled "y" Ask
  pure (a + b)

runReaderSum : Int
runReaderSum =
  runIdentity . runReaderT 1 . runReaderT 2 $ readerSum
  {sig = ReaderE Int :+: ReaderE Int :+: VoidE}
  {rx = Label L}
  {ry = Label (T L R)}
  {al = Reader @{Reader}}

-----------------------

testWriterIO : (r : Inj (ReaderE Int) sig)
            => (io : Inj (Lift IO) sig)
            => (al : Algebra sig m)
            => m ()
testWriterIO = do
  x <- ask {r = Int}
  lift {n = IO} (putStrLn (show x))

runTestWriterIO : IO ()
runTestWriterIO = runReaderT 2 $ testWriterIO
  {sig = ReaderE Int :+: Lift IO}
  {r = L}
  {io = R}
  {al = Reader}

-----------------------

incrE : (s : Inj (StateE Int) sig)
     => (al : Algebra sig m)
     => m ()
incrE = do
  x <- ask {r = Int}
  tell (x + 1)

runIncr : Int
runIncr = runIdentity . map fst . runStateT 0 $ incrE
  {sig = StateE Int :+: VoidE}
  {s = L}
  {al = State}

-----------------------

standaloneList : (l : Inj ChoiceE sig)
              => (al : Algebra sig m)
              => m (Int, Int)
standaloneList = do
  x <- oneOf [1, 2, 3, 4]
  y <- oneOf [5, 6, 7, 8]
  pure (x, y)

runStandaloneList : List (Int, Int)
runStandaloneList = runIdentity . runListT $ standaloneList
  {sig = ChoiceE :+: VoidC}
  {l = L}
  {al = Algebra.Concat}

-----------------------

%hide Trans.lift

tooBig : (l : Inj ChoiceE sig)
      => (e : Inj (EitherE Int) sig)
      => (al : Algebra sig m)
      => List Int
      -> m Int
tooBig list = do
  v <- oneOf list
  if v > 5 then fail {e = Int} v else pure v

tooBigCatch : (l : Inj ChoiceE sig)
           => (e : Inj (EitherE Int) sig)
           => (al : Algebra sig m)
           => List Int
           -> m Int
tooBigCatch list = do
  v <- oneOf list
  try (if v > 5 then fail v else pure v)
   \v => if v > the Int 7 then fail v else pure v

runTooBig : ?
runTooBig = runIdentity . runListT' . runEitherT $ tooBig [5, 7, 1]
 {sig = EitherE Int :+: ChoiceE :+: VoidE}
 {e = L}
 {l = T L R}
 {al = Algebra.Either @{Algebra.Concat}}

runTooBig' : ?
runTooBig' = runIdentity . runEitherT . runListT $ tooBig [5, 7, 1]
 {sig =  ChoiceE :+: EitherE Int :+: VoidE}
 {l = L}
 {e = T L R}
 {al = Algebra.Concat @{Algebra.Either}}

runTooBigCatch : ?
runTooBigCatch = runIdentity . runListT . runEitherT $ tooBigCatch [5, 7, 1]
 {sig = EitherE Int :+: ChoiceE :+: VoidE}
 {e = L}
 {l = T L R}
 {al = Algebra.Either @{Algebra.Concat}}

runTooBigCatch' : ?
runTooBigCatch' = runIdentity . runEitherT . runListT $ tooBigCatch [5, 7, 1]
 {sig =  ChoiceE :+: EitherE Int :+: VoidE}
 {l = L}
 {e = T L R}
 {al = Algebra.Concat @{Algebra.Either}}

-----------------------

||| Generate squares up to n.
||| For every pair of squares, write its sum
||| to the context only if the sum is odd.
||| We test the system by performing the writes all the time
||| inside a `try` block. But if a sum is even we fail inside that block.
||| The system handles backtracking of state for us.
||| We also print intermediate results to console.
exceptionStateListPrint :
     (l : Inj ChoiceE sig)
  => (r : Inj (ReaderE Int) sig)
  => (w : Inj (WriterE (List Int)) sig)
  => (e : Inj (EitherE String) sig)
  => (io : Inj (LiftE IO) sig)
  => (al : Algebra sig m)
  => m ()
exceptionStateListPrint = do
  n <- ask
  let gen = oneOf (takeBefore (> n) $ map (\x => x * x) [2..])
  x <- gen
  y <- gen
  try {e = String}
    (do tell {w = List Int} [x + y]
        if (x + y) `mod` 2 == 0
           then
             fail "even"
           else do
             lift {n = IO} (putStrLn "odd: \{show x} + \{show y} = \{show (x + y)}"))
    (\_ => pure ())

runExceptionStateListPrint : IO ()
runExceptionStateListPrint = do
  res <- runEitherT . runWriterT . runListT . runReaderT 50 $ exceptionStateListPrint
   {sig = ReaderE Int :+: ChoiceE :+: WriterE (List Int) :+: EitherE String :+: Lift IO}
   {r = L}
   {l = T L R}
   {w = T (T L R) R}
   {e = T (T (T L R) R) R}
   {io = T (T (T R R) R) R}
   {al = Algebra.Reader
          @{Algebra.Concat
            @{Algebra.ConcatLeft
              @{%search}
              @{Algebra.Either}}}}
  printLn (map snd res)

-----------------------

pythag : (l : Inj ChoiceE sig)
      => (al : Algebra sig m)
      => (alt : Alternative m)
      => m (Int, Int, Int)
pythag = do
  a <- oneOf [1..10]
  b <- oneOf [1..10]
  c <- oneOf [1..10]
  guard (a * a + b * b == c * c)
  pure (a, b, c)

runPythag : ?
runPythag = runIdentity . runListT $ pythag
  {sig = ChoiceE :+: VoidC}
  {l = L}
  {al = Algebra.Concat @{Algebra.Void}}
  {alt = ListT}

-----------------------

main : IO ()
main = pure ()

ext: idr


text:
> module Finite.Operations

> import Data.Fin
> import Data.Vect
> import Data.Vect.Quantifiers
> import Control.Isomorphism

> import Finite.Predicates
> import Fin.Operations
> --import Isomorphism.Operations
> import Sigma.Sigma
> import Pairs.Operations

> %default total

> %access public export

Finite types are dependent pairs: an |n : Nat| (the cardinality of the
type) and an isomorphism to |Fin n|. Here we extract the cardinality.

> ||| Cardinality of finite types
> card : {A : Type} -> (fA : Finite A) -> Nat
> card = getWitness

Finite types are dependent pairs: an |n : Nat| (the cardinality of the
type) and an isomorphism to |Fin n|. Here we extract the isomorphism.

> ||| Isomorphism of finite types
> iso : {A : Type} -> (fA : Finite A) -> Iso A (Fin (card fA))
> iso = getProof

> {-

Finite types are dependent pairs: an |n : Nat| (the cardinality of the
type) and an isomorphism to |Fin n|. Here we extract the components of
the isomorphism.

> ||| For a finite type |A| of cardinality |n|, maps |A|-values to |Fin n|-values
> toFin : {A : Type} -> (fA : Finite A) -> (A -> Fin (card fA))
> toFin (Evidence n (MkIso to from toFrom fromTo)) = to

> ||| For a finite type |A| of cardinality |n|, maps |Fin n|-values to |A|-values
> fromFin : {A : Type} -> (fA : Finite A) -> (Fin (card fA) -> A)
> fromFin (Evidence n (MkIso to from toFrom fromTo)) = from

> ||| |toFin| is the left inverse of |fromFin|
> toFinFromFin : {A : Type} -> (fA : Finite A) -> (k : Fin (card fA)) -> toFin fA (fromFin fA k) = k
> toFinFromFin (Evidence n (MkIso to from toFrom fromTo)) = toFrom

> ||| |fromFin| is the left inverse of |toFin|
> FromFinToFin : {A : Type} -> (fA : Finite A) -> (a : A) -> fromFin fA (toFin fA a) = a
> FromFinToFin (Evidence n (MkIso to from toFrom fromTo)) = fromTo

> -}

We can represent a finite type |A| of cardinality |n| with a vector of
elements of type |A| of length |n|. This can be done by calling
|FinOperations.toVect| on the finite function associated (via ||) to |A|.

> ||| Maps a finite type |A| of cardinality |n| to a vector of |A|-values of length |n|
> toVect : {A : Type} -> (fA : Finite A) -> Vect (card fA) A
> toVect (MkSigma _ iso) = toVect (from iso)
> -- toVect fA = toVect (from (iso fA))
> -- toVect fA = toVect (fromFin fA)

> |||
> CardZ : {A : Type} -> Finite A -> Type
> CardZ fA = card fA = Z

> |||
> CardNotZ : {A : Type} -> Finite A -> Type
> CardNotZ = Not . CardZ
> -- CardNotZ fA = LT Z (card fA)

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
> module NonNegRational.LTEProperties

> import Syntax.PreorderReasoning

> import NonNegRational.NonNegRational
> import NonNegRational.BasicOperations
> import NonNegRational.BasicProperties
> import NonNegRational.Predicates
> import Fraction.Fraction
> import Fraction.BasicOperations
> import Fraction.Predicates
> import Fraction.BasicProperties
> import Fraction.Normalize
> import Fraction.NormalizeProperties
> import Fraction.EqProperties
> import Fraction.LTEProperties
> import Fraction.Normal
> import Subset.Properties
> import Unique.Predicates
> import Nat.Positive
> import Num.Refinements
> import Pairs.Operations
> import Nat.LTEProperties
> import Nat.OperationsProperties
> -- import ListProperties
> import Rel.TotalPreorder

> %default total
> %access public export

|LTE| is a total preorder:

> ||| LTE is reflexive
> reflexiveLTE : (x : NonNegRational) -> x `LTE` x
> reflexiveLTE x = reflexiveLTE (toFraction x)
> %freeze reflexiveLTE

> ||| LTE is transitive
> transitiveLTE : (x, y, z : NonNegRational) -> x `LTE` y -> y `LTE` z -> x `LTE` z
> transitiveLTE x y z xLTEy yLTEz = transitiveLTE (toFraction x) (toFraction y) (toFraction z) xLTEy yLTEz
> %freeze transitiveLTE

> ||| LTE is total
> totalLTE : (x, y : NonNegRational) -> Either (x `LTE` y) (y `LTE` x)
> totalLTE x y = totalLTE (toFraction x) (toFraction y)
> %freeze totalLTE

> ||| LTE is a total preorder
> totalPreorderLTE : TotalPreorder NonNegRational.Predicates.LTE
> totalPreorderLTE = MkTotalPreorder LTE reflexiveLTE transitiveLTE totalLTE

Properties of |LTE| and |plus|:

> ||| LTE is monotone w.r.t. `plus`
> monotonePlusLTE : {a, b, c, d : NonNegRational} ->
>                   a `LTE` b -> c `LTE` d -> (a + c) `LTE` (b + d)
> monotonePlusLTE {a} {b} {c} {d} aLTEb cLTEd = s4 where
>   s1 : LTE (toFraction a + toFraction c) (toFraction b + toFraction d)
>   s1 = Fraction.LTEProperties.monotonePlusLTE aLTEb cLTEd
>   s2 : LTE (normalize (toFraction a + toFraction c))
>            (normalize (toFraction b + toFraction d))
>   s2 = normalizeLTELemma (toFraction a + toFraction c) (toFraction b + toFraction d) s1
>   s3 : LTE (toFraction (fromFraction (toFraction a + toFraction c)))
>            (toFraction (fromFraction (toFraction b + toFraction d)))
>   s3 = s2
>   s4 : LTE (fromFraction (toFraction a + toFraction c)) (fromFraction (toFraction b + toFraction d))
>   s4 = s3
>   s5 : LTE (a + c) (b + d)
>   s5 = s4
> %freeze monotonePlusLTE

Properties of |LTE| and |mult|:

> ||| LTE is monotone w.r.t. `(*)`
> monotoneMultLTE : {a, b, c, d : NonNegRational} ->
>                   a `LTE` b -> c `LTE` d -> (a * c) `LTE` (b * d)
> monotoneMultLTE {a} {b} {c} {d} aLTEb cLTEd = s4 where
>   s1 : LTE (toFraction a * toFraction c) (toFraction b * toFraction d)
>   s1 = Fraction.LTEProperties.monotoneMultLTE aLTEb cLTEd
>   s2 : LTE (normalize (toFraction a * toFraction c))
>            (normalize (toFraction b * toFraction d))
>   s2 = normalizeLTELemma (toFraction a * toFraction c) (toFraction b * toFraction d) s1
>   s3 : LTE (toFraction (fromFraction (toFraction a * toFraction c)))
>            (toFraction (fromFraction (toFraction b * toFraction d)))
>   s3 = s2
>   s4 : LTE (fromFraction (toFraction a * toFraction c)) (fromFraction (toFraction b * toFraction d))
>   s4 = s3
>   s5 : LTE (a * c) (b * d)
>   s5 = s4
> %freeze monotoneMultLTE

> {-

> ---}


text:
module Flexidisc.OrdList.Row

import Flexidisc.OrdList.Label
import Flexidisc.OrdList.Type

%default total
%access public export

||| Proof that a key value pair is part of an `OrdList`. If you don't need the value, use `Label`.
data OrdRow : (l : k) -> (ty : v) -> OrdList k o v -> Type where
  ||| The label is in the first element of the list
  Here  :                             OrdRow l ty ((l, ty) :: xs)
  ||| The label is in the tail
  There : (later : OrdRow l ty xs) -> OrdRow l ty (x::xs)

%name OrdRow lbl, loc, prf, e, elem

||| Demote it to a label existence proof
labelFromOrdRow : OrdRow l v xs -> OrdLabel l xs
labelFromOrdRow Here          = Here
labelFromOrdRow (There later) = There (labelFromOrdRow later)

Uninhabited (OrdRow k v []) where
  uninhabited Here      impossible
  uninhabited (There _) impossible

||| Map a row and its header simultaneously
mapRow : {xs : OrdList k o a} -> (f : a -> b) -> (loc : OrdRow l ty xs) -> OrdRow l (f ty) (map f xs)
mapRow f loc {xs = []} = absurd loc
mapRow f Here {xs = ((k, x) :: xs)} = Here
mapRow f (There later) {xs = ((k, x) :: xs)} = There (mapRow f later)

||| Given a proof that an element is in a vector, remove it
dropOrdRow : (xs : OrdList k o v) -> (loc : OrdRow l ty xs) -> OrdList k o v
dropOrdRow xs = dropLabel xs . labelFromOrdRow

||| Update a value in the list given it's location and an update function
changeValue : (xs : OrdList k o v) -> (loc : OrdRow l old xs) -> (new : v) ->
             OrdList k o v
changeValue xs loc new = changeValue xs (labelFromOrdRow loc) new

changeWithSameTypeIsUnchanged : (row : OrdRow l x xs) -> changeValue xs row x = xs
changeWithSameTypeIsUnchanged Here = Refl
changeWithSameTypeIsUnchanged (There later) = cong $ changeWithSameTypeIsUnchanged later

findInsertOrdRow : (l : k) -> (xs : OrdList k o v) -> OrdRow l ty (insert (l,ty) xs)
findInsertOrdRow l [] = Here
findInsertOrdRow l ((kx, vx) :: xs) with (l < kx)
  | True  = Here
  | False = There (findInsertOrdRow l xs)

dropInsertInv : (l : k) -> (ty : v) -> (xs : OrdList k o v) ->
                dropOrdRow (insert (l, ty) xs) (findInsertOrdRow l xs) = xs
dropInsertInv l ty [] = Refl
dropInsertInv l ty ((kx,vx) :: xs) with (l < kx)
  | True  = Refl
  | False = cong (dropInsertInv l ty xs)

max_stars_repo_name: berewt/flexidisc

max_issues_repo_name: LIST-LUXEMBOURG/flexidisc

max_forks_repo_name: LIST-LUXEMBOURG/flexidisc


text:
module ProofColDivSeqBase

%default total
%access export

-- ----- from libs/contrib/Data/CoList.idr -----
public export
codata CoList : Type -> Type where
  Nil  : CoList a
  (::) : a -> CoList a -> CoList a

implementation Functor CoList where
  map f []        = []
  map f (x :: xs) = f x :: map f xs

implementation Show a => Show (CoList a) where
  show xs = "[" ++ show' "" 20 xs ++ "]" where
    show' : String -> (n : Nat) -> (xs : CoList a) -> String
    show' acc Z     _         = acc ++ "..."
    show' acc (S n) []        = acc
    show' acc (S n) [x]       = acc ++ show x
    show' acc (S n) (x :: xs) = show' (acc ++ (show x) ++ ", ") n xs

unfoldr : (a -> Maybe (b, a)) -> a -> CoList b
unfoldr f x =
  case f x of
    Just (y, new_x) => y :: (unfoldr f new_x)
    _               => []
-- ----- from libs/contrib/Data/CoList.idr -----

-- ----- from libs/contrib/Data/Nat/DivMod/IteratedSubtraction.idr -----
public export
data LT' : (n, m : Nat) -> Type where
  ||| n < 1 + n
  LTSucc : LT' n (S n)
  ||| n < m implies that n < m + 1
  LTStep : LT' n m -> LT' n (S m)

||| Nothing is strictly less than zero
implementation Uninhabited (LT' n 0) where
  uninhabited LTSucc impossible

||| Zero is less than any non-zero number.
LTZeroLeast : LT' Z (S n)
LTZeroLeast {n = Z}   = LTSucc
LTZeroLeast {n = S n} = LTStep LTZeroLeast

||| If n < m, then 1 + n < 1 + m
ltSuccSucc : LT' n m -> LT' (S n) (S m)
ltSuccSucc LTSucc      = LTSucc
ltSuccSucc (LTStep lt) = LTStep $ ltSuccSucc lt

||| If n + 1 < m, then n < m
lteToLt' : LTE (S n) m -> LT' n m
lteToLt' {n = Z}   (LTESucc x) = LTZeroLeast
lteToLt' {n = S k} (LTESucc x) = ltSuccSucc $ lteToLt' x

implementation WellFounded LT' where
  wellFounded x = Access (acc x)
    where
      ||| Show accessibility by induction on the structure of the LT' witness
      acc : (x, y : Nat) -> LT' y x -> Accessible LT' y
      -- Zero is vacuously accessible: there's nothing smaller to check
      acc Z     y lt = absurd lt
      -- If the element being accessed is one smaller, we're done
      acc (S y) y LTSucc = Access (acc y)
      -- If the element is more than one smaller, we need to go further
      acc (S k) y (LTStep smaller) = acc k y smaller
-- ----- from libs/contrib/Data/Nat/DivMod/IteratedSubtraction.idr -----

-- ---------------------------------
-- mod2
public export
data Parity : Nat -> Type where
  Even : Parity (n + n)
  Odd  : Parity (S (n + n))
helpEven : (j : Nat) -> Parity (S j + S j) -> Parity (S (S (plus j j)))
helpEven j p = rewrite plusSuccRightSucc j j in p
helpOdd : (j : Nat) -> Parity (S (S (j + S j))) -> Parity (S (S (S (j + j))))
helpOdd j p = rewrite plusSuccRightSucc j j in p
parity : (n : Nat) -> Parity n
parity Z     = Even {n=Z}
parity (S Z) = Odd {n=Z}
parity (S (S k)) with (parity k)
  parity (S (S (j + j)))     | Even = helpEven j (Even {n = S j})
  parity (S (S (S (j + j)))) | Odd  = helpOdd j (Odd {n = S j})

-- mod3
public export
data Mod3 : Nat -> Type where
  ThreeZero : Mod3 (n + n + n)
  ThreeOne  : Mod3 (S (n + n + n))
  ThreeTwo  : Mod3 (S (S (n + n + n)))
helpThreeZero : (j : Nat) -> (plus (plus (S j) (S j)) (S j)) = S (S (S (plus (plus j j) j)))
helpThreeZero j = rewrite sym $ plusSuccRightSucc j j in
                  rewrite sym $ plusSuccRightSucc (plus j j) j in Refl
helpThreeOne : (j : Nat) -> S (plus (plus (S j) (S j)) (S j)) = S (S (S (S (plus (plus j j) j))))
helpThreeOne j = cong {f=S} $ helpThreeZero j
helpThreeTwo : (j : Nat) -> S (S (plus (plus (S j) (S j)) (S j))) = S (S (S (S (S (plus (plus j j) j)))))
helpThreeTwo j = cong {f=S} $ helpThreeOne j
mod3 : (n : Nat) -> Mod3 n
mod3 Z         = ThreeZero {n=Z}
mod3 (S Z)     = ThreeOne {n=Z}
mod3 (S (S Z)) = ThreeTwo {n=Z}
mod3 (S (S (S k))) with (mod3 k)
  mod3 (S (S (S (j + j + j))))         | ThreeZero =
    rewrite sym $ helpThreeZero j in ThreeZero {n=S j}
  mod3 (S (S (S (S (j + j + j)))))     | ThreeOne =
    rewrite sym $ helpThreeOne j in ThreeOne {n=S j}
  mod3 (S (S (S (S (S (j + j + j)))))) | ThreeTwo =
    rewrite sym $ helpThreeTwo j in ThreeTwo {n=S j}
-- ---------------------------------

-- ---------------------------------
dsp : List Integer -> CoList Integer -> CoList Integer
dsp _                      []        = []
dsp []                    (y :: ys) = y  :: ys
dsp (x :: [])             (y :: ys) = y  :: ys
dsp (x1 :: x2 :: [])      (y :: ys) = x1 :: (x2 + y) :: ys
dsp (x1 :: x2 :: x3 :: _) (y :: ys) = x1 :: x2       :: (x3 + y) :: ys

countEven : Nat -> Nat -> Nat -> (Nat, Nat)
countEven n Z      acc = (acc, n)
countEven n (S nn) acc =
  if (modNatNZ n 2 SIsNotZ) == 1
    then (acc, n)
    else countEven (divNatNZ n 2 SIsNotZ) nn (acc+1)

-- divSeqの実装
divSeq : Nat -> CoList Integer
divSeq n = divSeq' (S (S (S (n+n+n+n+n+n)))) (S (S (S (n+n+n+n+n+n)))) where
  divSeq' : Nat -> Nat -> CoList Integer
  divSeq' n     Z     = []
  divSeq' Z     (S k) = []
  divSeq' (S n) (S k) with (parity n)
    divSeq' (S (S (j + j))) (S k) | Odd  = divSeq' (S j) k --実際はここへは来ない
    divSeq' (S (j + j))     (S k) | Even =
      map toIntegerNat
        (unfoldr (\b => if b <= 1 then Nothing
                                  else Just (countEven (b*3+1) (b*3+1) 0) ) (S (j + j)))

{-
72t+45  E[2,-4] y=x/12-3/4  6t+3        12x+7
*8.                    <---------------------
108t+99=6(18t+16)+3 EF[2,1,-2] y=2x/9-1 24t+21=6(4t+3)+3         4x+4+2t
*6.
108t+27=6(18t+4)+3  CF[4,1,-2] y=8x/9-3  96t+21=6(16t+3)+3       x+1+2t
*5.
216t+225=6(36t+37)+3  FE[5,0,-4] y=2x/9-5  48t+45=6(8t+7)+3      4x+9+4t
*14.
108t+111=6(18t+18)+3  FB[5,-1,-2] y=4x/9-13/3  48t+45=6(8t+7)+3  2x+11+2t

0
1+w
  1+2v
    1+2(2u)             2. 9. 11.  4. 13.
    1+2(1+2u)
      3+4(2t)
        3+8(2s)         2. 9. 11.  8.  6.
        3+8(1+2s)       2. 9. 11.  8.
      3+4(1+2t)         2. 9. 11.  5. 14.
  1+1+2v
    1+1+2(2u)           2. 9. 11.  3. 12.
    1+1+2(1+2u)
      4+4(2t)           2. 9. 11.  3. 12.  7.
      4+4(1+2t)         2. 9. 11.  3. 12.
-}
-- この部分の実装は、コンストラクタIsFirstLimited01~14の正当性を補強している
allDivSeq : Nat -> List (CoList Integer)
allDivSeq Z     = [[1, 4], [2, -4] `dsp` [3,2,3,4], [3, 0, -4] `dsp` [2,3,1,1,5,4], [4, -4] `dsp` [1,1,1,5,4], [1, -2] `dsp` [6], [3, -1, -2] `dsp` [1,1,2,1,4,1,3,1,2,3,4]] -- 6*<0>+3 = 3
allDivSeq (S w) with (parity w)
  allDivSeq (S (v + v))     | Even with (parity v)
    allDivSeq (S ((u + u) + (u + u)))         | Even | Even
      = let x = (S ((u + u) + (u + u)))
        in [divSeq x, [2, -4] `dsp` divSeq (12*x+7), [4, -4] `dsp` divSeq (3*x+2), [1, -2] `dsp` divSeq (6*x+3), [6, -2, -4] `dsp` divSeq (9*x+16), [6, -3, -2] `dsp` divSeq (4*x+2*u+8)]
    allDivSeq (S ((S (u + u)) + (S (u + u)))) | Even | Odd  with (parity u)
      allDivSeq (S ((S ((t + t) + (t + t))) + (S ((t + t) + (t + t)))))                 | Even | Odd  | Even with (parity t)
        allDivSeq (S ((S (((s + s) + (s + s)) + ((s + s) + (s + s)))) + (S (((s + s) + (s + s)) + ((s + s) + (s + s))))))                                 | Even | Odd  | Even | Even
          = let x = (S ((S (((s + s) + (s + s)) + ((s + s) + (s + s)))) + (S (((s + s) + (s + s)) + ((s + s) + (s + s))))))
            in [divSeq x, [2, -4] `dsp` divSeq (12*x+7), [4, -4] `dsp` divSeq (3*x+2), [1, -2] `dsp` divSeq (6*x+3), [2, 1, -2] `dsp` divSeq (4*x+8*s+4), [4, 1, -2] `dsp` divSeq (x+2*s+1)]
        allDivSeq (S ((S (((S (s + s)) + (S (s + s))) + ((S (s + s)) + (S (s + s))))) + (S (((S (s + s)) + (S (s + s))) + ((S (s + s)) + (S (s + s))))))) | Even | Odd  | Even | Odd
          = let x = (S ((S (((S (s + s)) + (S (s + s))) + ((S (s + s)) + (S (s + s))))) + (S (((S (s + s)) + (S (s + s))) + ((S (s + s)) + (S (s + s)))))))
            in [divSeq x, [2, -4] `dsp` divSeq (12*x+7), [4, -4] `dsp` divSeq (3*x+2), [1, -2] `dsp` divSeq (6*x+3), [2, 1, -2] `dsp` divSeq (4*x+8*s+4)]
      allDivSeq (S ((S ((S (t + t)) + (S (t + t)))) + (S ((S (t + t)) + (S (t + t)))))) | Even | Odd  | Odd
        = let x = (S ((S ((S (t + t)) + (S (t + t)))) + (S ((S (t + t)) + (S (t + t))))))
          in [divSeq x, [2, -4] `dsp` divSeq (12*x+7), [4, -4] `dsp` divSeq (3*x+2), [1, -2] `dsp` divSeq (6*x+3), [5, 0, -4] `dsp` divSeq (4*x+4*t+9), [5, -1, -2] `dsp` divSeq (2*x+2*t+11)]
  allDivSeq (S (S (v + v))) | Odd  with (parity v)
    allDivSeq (S (S ((u + u) + (u + u))))         | Odd  | Even
      = let x = (S (S ((u + u) + (u + u))))
        in [divSeq x, [2, -4] `dsp` divSeq (12*x+7), [4, -4] `dsp` divSeq (3*x+2), [1, -2] `dsp` divSeq (6*x+3), [3, 0, -4] `dsp` divSeq (18*x+13), [3, -1, -2] `dsp` divSeq (9*x+6)]
    allDivSeq (S (S ((S (u + u)) + (S (u + u))))) | Odd  | Odd with (parity u)
      allDivSeq (S (S ((S ((t + t) + (t + t))) + (S ((t + t) + (t + t))))))                 | Odd  | Odd | Even
        = let x = (S (S ((S ((t + t) + (t + t))) + (S ((t + t) + (t + t))))))
          in [divSeq x, [2, -4] `dsp` divSeq (12*x+7), [4, -4] `dsp` divSeq (3*x+2), [1, -2] `dsp` divSeq (6*x+3), [3, 0, -4] `dsp` divSeq (18*x+13), [3, -1, -2] `dsp` divSeq (9*x+6), [1, 3, -2] `dsp` divSeq (2*x+2*t+2)]
      allDivSeq (S (S ((S ((S (t + t)) + (S (t + t)))) + (S ((S (t + t)) + (S (t + t))))))) | Odd  | Odd | Odd
        = let x = (S (S ((S ((S (t + t)) + (S (t + t)))) + (S ((S (t + t)) + (S (t + t)))))))
          in [divSeq x, [2, -4] `dsp` divSeq (12*x+7), [4, -4] `dsp` divSeq (3*x+2), [1, -2] `dsp` divSeq (6*x+3), [3, 0, -4] `dsp` divSeq (18*x+13), [3, -1, -2] `dsp` divSeq (9*x+6)]
-- ---------------------------------

-- ---------------------------------
mutual
  public export
  data FirstLimited : List (CoList Integer) -> Type where
    IsFirstLimited01    : (FirstLimited . ProofColDivSeqBase.allDivSeq) 1 -- 6*<1>+3 = 9
    IsFirstLimited02    : (l : Nat)
      -> (AllLimited . ProofColDivSeqBase.allDivSeq) l
        -> (FirstLimited . ProofColDivSeqBase.allDivSeq) (S (((S (l+l))+(S (l+l))) + ((S (l+l))+(S (l+l))) + ((S (l+l))+(S (l+l)))))
    IsFirstLimited03    : (m : Nat)
      -> (AllLimited . ProofColDivSeqBase.allDivSeq) (m+m)
        -> (FirstLimited . ProofColDivSeqBase.allDivSeq) (S (((S (S ((m+m+m)+(m+m+m))))+(S (S ((m+m+m)+(m+m+m))))) + ((S (S ((m+m+m)+(m+m+m))))+(S (S ((m+m+m)+(m+m+m))))) + ((S (S ((m+m+m)+(m+m+m))))+(S (S ((m+m+m)+(m+m+m)))))))
    IsFirstLimited04    : (m : Nat)
      -> (AllLimited . ProofColDivSeqBase.allDivSeq) (S ((m+m)+(m+m)))
        -> (FirstLimited . ProofColDivSeqBase.allDivSeq) (S (((S (S ((S (m+m+m))+(S (m+m+m)))))+(S (S ((S (m+m+m))+(S (m+m+m)))))) + ((S (S ((S (m+m+m))+(S (m+m+m)))))+(S (S ((S (m+m+m))+(S (m+m+m)))))) + ((S (S ((S (m+m+m))+(S (m+m+m)))))+(S (S ((S (m+m+m))+(S (m+m+m))))))))
    IsFirstLimited05    : (m : Nat)
      -> (AllLimited . ProofColDivSeqBase.allDivSeq) (S (S (S (S (S (S (S (m+m+m+m)+(m+m+m+m))))))))
        -> (FirstLimited . ProofColDivSeqBase.allDivSeq) (S (((S (S ((S (S (m+m+m)))+(S (S (m+m+m))))))+(S (S ((S (S (m+m+m)))+(S (S (m+m+m))))))) + ((S (S ((S (S (m+m+m)))+(S (S (m+m+m))))))+(S (S ((S (S (m+m+m)))+(S (S (m+m+m))))))) + ((S (S ((S (S (m+m+m)))+(S (S (m+m+m))))))+(S (S ((S (S (m+m+m)))+(S (S (m+m+m)))))))))
    IsFirstLimited06    : (l : Nat)
      -> (AllLimited . ProofColDivSeqBase.allDivSeq) (S (S (S (l+l+l+l)+(l+l+l+l)+(l+l+l+l)+(l+l+l+l))))
        -> (FirstLimited . ProofColDivSeqBase.allDivSeq) (S ((S ((l+l+l)+(l+l+l))) + (S ((l+l+l)+(l+l+l))) + (S ((l+l+l)+(l+l+l)))))
    IsFirstLimited07    : (l : Nat)
      -> (AllLimited . ProofColDivSeqBase.allDivSeq) (S (S (S (S (l+l+l+l)+(l+l+l+l)))))
        -> (FirstLimited . ProofColDivSeqBase.allDivSeq) (S ((S ((S (l+l+l))+(S (l+l+l)))) + (S ((S (l+l+l))+(S (l+l+l)))) + (S ((S (l+l+l))+(S (l+l+l))))))
    IsFirstLimited08    : (l : Nat)
      -> (AllLimited . ProofColDivSeqBase.allDivSeq) (S (S (S ((l+l)+(l+l)))))
        -> (FirstLimited . ProofColDivSeqBase.allDivSeq) (S ((S ((S (S (l+l+l)))+(S (S (l+l+l))))) + (S ((S (S (l+l+l)))+(S (S (l+l+l))))) + (S ((S (S (l+l+l)))+(S (S (l+l+l)))))))
    IsFirstLimited09    : (j : Nat)
      -> (AllLimited . ProofColDivSeqBase.allDivSeq) j
        -> (FirstLimited . ProofColDivSeqBase.allDivSeq) (S (S (plus (plus j j) j)))
    IsFirstLimited10    : (FirstLimited . ProofColDivSeqBase.allDivSeq) 0 -- 6*<0>+3 = 3
    IsFirstLimited11    : (k : Nat)
      -> (AllLimited . ProofColDivSeqBase.allDivSeq) k
        -> (FirstLimited . ProofColDivSeqBase.allDivSeq) (S (S (S (   (k+k)  +    (k+k)  +    (k+k)))))
    IsFirstLimited12    : (l : Nat)
      -> (AllLimited . ProofColDivSeqBase.allDivSeq) (l+l)
        -> (FirstLimited . ProofColDivSeqBase.allDivSeq) (S (S (S ((S ((l+l+l)+(l+l+l))) + (S ((l+l+l)+(l+l+l))) + (S ((l+l+l)+(l+l+l)))))))
    IsFirstLimited13    : (l : Nat)
      -> (AllLimited . ProofColDivSeqBase.allDivSeq) (S ((l+l)+(l+l)))
        -> (FirstLimited . ProofColDivSeqBase.allDivSeq) (S (S (S ((S ((S (l+l+l))+(S (l+l+l)))) + (S ((S (l+l+l))+(S (l+l+l)))) + (S ((S (l+l+l))+(S (l+l+l))))))))
    IsFirstLimited14    : (l : Nat)
      -> (AllLimited . ProofColDivSeqBase.allDivSeq) (S (S (S (S (S (S (S (l+l+l+l)+(l+l+l+l))))))))
        -> (FirstLimited . ProofColDivSeqBase.allDivSeq) (S (S (S ((S ((S (S (l+l+l)))+(S (S (l+l+l))))) + (S ((S (S (l+l+l)))+(S (S (l+l+l))))) + (S ((S (S (l+l+l)))+(S (S (l+l+l)))))))))

    IsFirstLimitedSuff2_1 : (z : Nat)
      -> (FirstLimited . ProofColDivSeqBase.allDivSeq) z
        -> (FirstLimited . ProofColDivSeqBase.allDivSeq) (1 + 2 * (2 * z))
    IsFirstLimitedSuff2_2 : (z : Nat)
      -> (FirstLimited . ProofColDivSeqBase.allDivSeq) z
        -> (FirstLimited . ProofColDivSeqBase.allDivSeq) (12 * (1 + 2 * (2 * z)) + 7)
    IsFirstLimitedSuff2_3 : (z : Nat)
      -> (FirstLimited . ProofColDivSeqBase.allDivSeq) z
        -> (FirstLimited . ProofColDivSeqBase.allDivSeq) (3 * (1 + 2 * (2 * z)) + 2)
    IsFirstLimitedSuff2_4 : (z : Nat)
      -> (FirstLimited . ProofColDivSeqBase.allDivSeq) z
        -> (FirstLimited . ProofColDivSeqBase.allDivSeq) (6 * (1 + 2 * (2 * z)) + 3)
    IsFirstLimitedSuff2_5 : (z : Nat)
      -> (FirstLimited . ProofColDivSeqBase.allDivSeq) z
        -> (FirstLimited . ProofColDivSeqBase.allDivSeq) (9 * (1 + 2 * (2 * z)) + 16)
    IsFirstLimitedSuff2_6 : (z : Nat)
      -> (FirstLimited . ProofColDivSeqBase.allDivSeq) z
        -> (FirstLimited . ProofColDivSeqBase.allDivSeq) (4 * (1 + 2 * (2 * z)) + 2 * z + 8)

    IsFirstLimitedSuff3_1 : (z : Nat)
      -> (FirstLimited . ProofColDivSeqBase.allDivSeq) z
        -> (FirstLimited . ProofColDivSeqBase.allDivSeq) (3 + 8 * (2 * z))
    IsFirstLimitedSuff3_2 : (z : Nat)
      -> (FirstLimited . ProofColDivSeqBase.allDivSeq) z
        -> (FirstLimited . ProofColDivSeqBase.allDivSeq) (12 * (3 + 8 * (2 * z)) + 7)
    IsFirstLimitedSuff3_3 : (z : Nat)
      -> (FirstLimited . ProofColDivSeqBase.allDivSeq) z
        -> (FirstLimited . ProofColDivSeqBase.allDivSeq) (3 * (3 + 8 * (2 * z)) + 2)
    IsFirstLimitedSuff3_4 : (z : Nat)
      -> (FirstLimited . ProofColDivSeqBase.allDivSeq) z
        -> (FirstLimited . ProofColDivSeqBase.allDivSeq) (6 * (3 + 8 * (2 * z)) + 3)
    IsFirstLimitedSuff3_5 : (z : Nat)
      -> (FirstLimited . ProofColDivSeqBase.allDivSeq) z
        -> (FirstLimited . ProofColDivSeqBase.allDivSeq) (4 * (3 + 8 * (2 * z)) + 8 * z + 4)
    IsFirstLimitedSuff3_6 : (z : Nat)
      -> (FirstLimited . ProofColDivSeqBase.allDivSeq) z
        -> (FirstLimited . ProofColDivSeqBase.allDivSeq) ((3 + 8 * (2 * z)) + 2 * z + 1)

    IsFirstLimitedSuff4_1 : (z : Nat)
      -> (FirstLimited . ProofColDivSeqBase.allDivSeq) z
        -> (FirstLimited . ProofColDivSeqBase.allDivSeq) (3 + 8 * (1 + 2 * z))
    IsFirstLimitedSuff4_2 : (z : Nat)
      -> (FirstLimited . ProofColDivSeqBase.allDivSeq) z
        -> (FirstLimited . ProofColDivSeqBase.allDivSeq) (12 * (3 + 8 * (1 + 2 * z)) + 7)
    IsFirstLimitedSuff4_3 : (z : Nat)
      -> (FirstLimited . ProofColDivSeqBase.allDivSeq) z
        -> (FirstLimited . ProofColDivSeqBase.allDivSeq) (3 * (3 + 8 * (1 + 2 * z)) + 2)
    IsFirstLimitedSuff4_4 : (z : Nat)
      -> (FirstLimited . ProofColDivSeqBase.allDivSeq) z
        -> (FirstLimited . ProofColDivSeqBase.allDivSeq) (6 * (3 + 8 * (1 + 2 * z)) + 3)
    IsFirstLimitedSuff4_5 : (z : Nat)
      -> (FirstLimited . ProofColDivSeqBase.allDivSeq) z
        -> (FirstLimited . ProofColDivSeqBase.allDivSeq) (4 * (3 + 8 * (1 + 2 * z)) + 8 * z + 4)

    IsFirstLimitedSuff5_1 : (z : Nat)
      -> (FirstLimited . ProofColDivSeqBase.allDivSeq) z
        -> (FirstLimited . ProofColDivSeqBase.allDivSeq) (3 + 4 * (1 + 2 * z))
    IsFirstLimitedSuff5_2 : (z : Nat)
      -> (FirstLimited . ProofColDivSeqBase.allDivSeq) z
        -> (FirstLimited . ProofColDivSeqBase.allDivSeq) (12 * (3 + 4 * (1 + 2 * z)) + 7)
    IsFirstLimitedSuff5_3 : (z : Nat)
      -> (FirstLimited . ProofColDivSeqBase.allDivSeq) z
        -> (FirstLimited . ProofColDivSeqBase.allDivSeq) (3 * (3 + 4 * (1 + 2 * z)) + 2)
    IsFirstLimitedSuff5_4 : (z : Nat)
      -> (FirstLimited . ProofColDivSeqBase.allDivSeq) z
        -> (FirstLimited . ProofColDivSeqBase.allDivSeq) (6 * (3 + 4 * (1 + 2 * z)) + 3)
    IsFirstLimitedSuff5_5 : (z : Nat)
      -> (FirstLimited . ProofColDivSeqBase.allDivSeq) z
        -> (FirstLimited . ProofColDivSeqBase.allDivSeq) (4 * (3 + 4 * (1 + 2 * z)) + 4 * z + 9)
    IsFirstLimitedSuff5_6 : (z : Nat)
      -> (FirstLimited . ProofColDivSeqBase.allDivSeq) z
        -> (FirstLimited . ProofColDivSeqBase.allDivSeq) (2 * (3 + 4 * (1 + 2 * z)) + 2 * z + 11)

    IsFirstLimitedSuff6_1 : (z : Nat)
      -> (FirstLimited . ProofColDivSeqBase.allDivSeq) z
        -> (FirstLimited . ProofColDivSeqBase.allDivSeq) (1 + 1 + 2 * (2 * z))
    IsFirstLimitedSuff6_2 : (z : Nat)
      -> (FirstLimited . ProofColDivSeqBase.allDivSeq) z
        -> (FirstLimited . ProofColDivSeqBase.allDivSeq) (12 * (1 + 1 + 2 * (2 * z)) + 7)
    IsFirstLimitedSuff6_3 : (z : Nat)
      -> (FirstLimited . ProofColDivSeqBase.allDivSeq) z
        -> (FirstLimited . ProofColDivSeqBase.allDivSeq) (3 * (1 + 1 + 2 * (2 * z)) + 2)
    IsFirstLimitedSuff6_4 : (z : Nat)
      -> (FirstLimited . ProofColDivSeqBase.allDivSeq) z
        -> (FirstLimited . ProofColDivSeqBase.allDivSeq) (6 * (1 + 1 + 2 * (2 * z)) + 3)
    IsFirstLimitedSuff6_5 : (z : Nat)
      -> (FirstLimited . ProofColDivSeqBase.allDivSeq) z
        -> (FirstLimited . ProofColDivSeqBase.allDivSeq) (18 * (1 + 1 + 2 * (2 * z)) + 13)
    IsFirstLimitedSuff6_6 : (z : Nat)
      -> (FirstLimited . ProofColDivSeqBase.allDivSeq) z
        -> (FirstLimited . ProofColDivSeqBase.allDivSeq) (9 * (1 + 1 + 2 * (2 * z)) + 6)

    IsFirstLimitedSuff7_1 : (z : Nat)
      -> (FirstLimited . ProofColDivSeqBase.allDivSeq) z
        -> (FirstLimited . ProofColDivSeqBase.allDivSeq) (4 + 4 * (2 * z))
    IsFirstLimitedSuff7_2 : (z : Nat)
      -> (FirstLimited . ProofColDivSeqBase.allDivSeq) z
        -> (FirstLimited . ProofColDivSeqBase.allDivSeq) (12 * (4 + 4 * (2 * z)) + 7)
    IsFirstLimitedSuff7_3 : (z : Nat)
      -> (FirstLimited . ProofColDivSeqBase.allDivSeq) z
        -> (FirstLimited . ProofColDivSeqBase.allDivSeq) (3 * (4 + 4 * (2 * z)) + 2)
    IsFirstLimitedSuff7_4 : (z : Nat)
      -> (FirstLimited . ProofColDivSeqBase.allDivSeq) z
        -> (FirstLimited . ProofColDivSeqBase.allDivSeq) (6 * (4 + 4 * (2 * z)) + 3)
    IsFirstLimitedSuff7_5 : (z : Nat)
      -> (FirstLimited . ProofColDivSeqBase.allDivSeq) z
        -> (FirstLimited . ProofColDivSeqBase.allDivSeq) (18 * (4 + 4 * (2 * z)) + 13)
    IsFirstLimitedSuff7_6 : (z : Nat)
      -> (FirstLimited . ProofColDivSeqBase.allDivSeq) z
        -> (FirstLimited . ProofColDivSeqBase.allDivSeq) (9 * (4 + 4 * (2 * z)) + 6)
    IsFirstLimitedSuff7_7 : (z : Nat)
      -> (FirstLimited . ProofColDivSeqBase.allDivSeq) z
        -> (FirstLimited . ProofColDivSeqBase.allDivSeq) (2 * (4 + 4 * (2 * z)) + 2 * z + 2)

    IsFirstLimitedSuff8_1 : (z : Nat)
      -> (FirstLimited . ProofColDivSeqBase.allDivSeq) z
        -> (FirstLimited . ProofColDivSeqBase.allDivSeq) (4 + 4 * (1 + 2 * z))
    IsFirstLimitedSuff8_2 : (z : Nat)
      -> (FirstLimited . ProofColDivSeqBase.allDivSeq) z
        -> (FirstLimited . ProofColDivSeqBase.allDivSeq) (12 * (4 + 4 * (1 + 2 * z)) + 7)
    IsFirstLimitedSuff8_3 : (z : Nat)
      -> (FirstLimited . ProofColDivSeqBase.allDivSeq) z
        -> (FirstLimited . ProofColDivSeqBase.allDivSeq) (3 * (4 + 4 * (1 + 2 * z)) + 2)
    IsFirstLimitedSuff8_4 : (z : Nat)
      -> (FirstLimited . ProofColDivSeqBase.allDivSeq) z
        -> (FirstLimited . ProofColDivSeqBase.allDivSeq) (6 * (4 + 4 * (1 + 2 * z)) + 3)
    IsFirstLimitedSuff8_5 : (z : Nat)
      -> (FirstLimited . ProofColDivSeqBase.allDivSeq) z
        -> (FirstLimited . ProofColDivSeqBase.allDivSeq) (18 * (4 + 4 * (1 + 2 * z)) + 13)
    IsFirstLimitedSuff8_6 : (z : Nat)
      -> (FirstLimited . ProofColDivSeqBase.allDivSeq) z
        -> (FirstLimited . ProofColDivSeqBase.allDivSeq) (9 * (4 + 4 * (1 + 2 * z)) + 6)

  public export
  data AllLimited : List (CoList Integer) -> Type where
    IsAllLimited00 : (AllLimited . ProofColDivSeqBase.allDivSeq) Z -- 6*<0>+3 = 3
    IsAllLimited01 : (z : Nat)
      -> (AllLimited . ProofColDivSeqBase.allDivSeq) Z
        -> (AllLimited . ProofColDivSeqBase.allDivSeq) (1 + 2 * (2 * z))
          -> (AllLimited . ProofColDivSeqBase.allDivSeq) (3 + 8 * (2 * z))
            -> (AllLimited . ProofColDivSeqBase.allDivSeq) (3 + 8 * (1 + 2 * z))
              -> (AllLimited . ProofColDivSeqBase.allDivSeq) (3 + 4 * (1 + 2 * z))
                -> (AllLimited . ProofColDivSeqBase.allDivSeq) (1 + 1 + 2 * (2 * z))
                  -> (AllLimited . ProofColDivSeqBase.allDivSeq) (4 + 4 * (2 * z))
                    -> (AllLimited . ProofColDivSeqBase.allDivSeq) (4 + 4 * (1 + 2 * z))
                      -> (AllLimited . ProofColDivSeqBase.allDivSeq) z
    IsAllLimited02 : (z : Nat)
      -> (FirstLimited . ProofColDivSeqBase.allDivSeq) (1 + 2 * (2 * z))
        -> (FirstLimited . ProofColDivSeqBase.allDivSeq) (12 * (1 + 2 * (2 * z)) + 7)
          -> (FirstLimited . ProofColDivSeqBase.allDivSeq) (3 * (1 + 2 * (2 * z)) + 2)
            -> (FirstLimited . ProofColDivSeqBase.allDivSeq) (6 * (1 + 2 * (2 * z)) + 3)
              -> (FirstLimited . ProofColDivSeqBase.allDivSeq) (9 * (1 + 2 * (2 * z)) + 16)
                -> (FirstLimited . ProofColDivSeqBase.allDivSeq) (4 * (1 + 2 * (2 * z)) + 2 * z + 8)
                  -> (AllLimited . ProofColDivSeqBase.allDivSeq) (1 + 2 * (2 * z))
    IsAllLimited03 : (z : Nat)
      -> (FirstLimited . ProofColDivSeqBase.allDivSeq) (3 + 8 * (2 * z))
        -> (FirstLimited . ProofColDivSeqBase.allDivSeq) (12 * (3 + 8 * (2 * z)) + 7)
          -> (FirstLimited . ProofColDivSeqBase.allDivSeq) (3 * (3 + 8 * (2 * z)) + 2)
            -> (FirstLimited . ProofColDivSeqBase.allDivSeq) (6 * (3 + 8 * (2 * z)) + 3)
              -> (FirstLimited . ProofColDivSeqBase.allDivSeq) (4 * (3 + 8 * (2 * z)) + 8 * z + 4)
                -> (FirstLimited . ProofColDivSeqBase.allDivSeq) ((3 + 8 * (2 * z)) + 2 * z + 1)
                  -> (AllLimited . ProofColDivSeqBase.allDivSeq) (3 + 8 * (2 * z))
    IsAllLimited04 : (z : Nat)
      -> (FirstLimited . ProofColDivSeqBase.allDivSeq) (3 + 8 * (1 + 2 * z))
        -> (FirstLimited . ProofColDivSeqBase.allDivSeq) (12 * (3 + 8 * (1 + 2 * z)) + 7)
          -> (FirstLimited . ProofColDivSeqBase.allDivSeq) (3 * (3 + 8 * (1 + 2 * z)) + 2)
            -> (FirstLimited . ProofColDivSeqBase.allDivSeq) (6 * (3 + 8 * (1 + 2 * z)) + 3)
              -> (FirstLimited . ProofColDivSeqBase.allDivSeq) (4 * (3 + 8 * (1 + 2 * z)) + 8 * z + 4)
                -> (AllLimited . ProofColDivSeqBase.allDivSeq) (3 + 8 * (1 + 2 * z))
    IsAllLimited05 : (z : Nat)
      -> (FirstLimited . ProofColDivSeqBase.allDivSeq) (3 + 4 * (1 + 2 * z))
        -> (FirstLimited . ProofColDivSeqBase.allDivSeq) (12 * (3 + 4 * (1 + 2 * z)) + 7)
          -> (FirstLimited . ProofColDivSeqBase.allDivSeq) (3 * (3 + 4 * (1 + 2 * z)) + 2)
            -> (FirstLimited . ProofColDivSeqBase.allDivSeq) (6 * (3 + 4 * (1 + 2 * z)) + 3)
              -> (FirstLimited . ProofColDivSeqBase.allDivSeq) (4 * (3 + 4 * (1 + 2 * z)) + 4 * z + 9)
                -> (FirstLimited . ProofColDivSeqBase.allDivSeq) (2 * (3 + 4 * (1 + 2 * z)) + 2 * z + 11)
                  -> (AllLimited . ProofColDivSeqBase.allDivSeq) (3 + 4 * (1 + 2 * z))
    IsAllLimited06 : (z : Nat)
      -> (FirstLimited . ProofColDivSeqBase.allDivSeq) (1 + 1 + 2 * (2 * z))
        -> (FirstLimited . ProofColDivSeqBase.allDivSeq) (12 * (1 + 1 + 2 * (2 * z)) + 7)
          -> (FirstLimited . ProofColDivSeqBase.allDivSeq) (3 * (1 + 1 + 2 * (2 * z)) + 2)
            -> (FirstLimited . ProofColDivSeqBase.allDivSeq) (6 * (1 + 1 + 2 * (2 * z)) + 3)
              -> (FirstLimited . ProofColDivSeqBase.allDivSeq) (18 * (1 + 1 + 2 * (2 * z)) + 13)
                -> (FirstLimited . ProofColDivSeqBase.allDivSeq) (9 * (1 + 1 + 2 * (2 * z)) + 6)
                  -> (AllLimited . ProofColDivSeqBase.allDivSeq) (1 + 1 + 2 * (2 * z))
    IsAllLimited07 : (z : Nat)
      -> (FirstLimited . ProofColDivSeqBase.allDivSeq) (4 + 4 * (2 * z))
        -> (FirstLimited . ProofColDivSeqBase.allDivSeq) (12 * (4 + 4 * (2 * z)) + 7)
          -> (FirstLimited . ProofColDivSeqBase.allDivSeq) (3 * (4 + 4 * (2 * z)) + 2)
            -> (FirstLimited . ProofColDivSeqBase.allDivSeq) (6 * (4 + 4 * (2 * z)) + 3)
              -> (FirstLimited . ProofColDivSeqBase.allDivSeq) (18 * (4 + 4 * (2 * z)) + 13)
                -> (FirstLimited . ProofColDivSeqBase.allDivSeq) (9 * (4 + 4 * (2 * z)) + 6)
                  -> (FirstLimited . ProofColDivSeqBase.allDivSeq) (2 * (4 + 4 * (2 * z)) + 2 * z + 2)
                    -> (AllLimited . ProofColDivSeqBase.allDivSeq) (4 + 4 * (2 * z))
    IsAllLimited08 : (z : Nat)
      -> (FirstLimited . ProofColDivSeqBase.allDivSeq) (4 + 4 * (1 + 2 * z))
        -> (FirstLimited . ProofColDivSeqBase.allDivSeq) (12 * (4 + 4 * (1 + 2 * z)) + 7)
          -> (FirstLimited . ProofColDivSeqBase.allDivSeq) (3 * (4 + 4 * (1 + 2 * z)) + 2)
            -> (FirstLimited . ProofColDivSeqBase.allDivSeq) (6 * (4 + 4 * (1 + 2 * z)) + 3)
              -> (FirstLimited . ProofColDivSeqBase.allDivSeq) (18 * (4 + 4 * (1 + 2 * z)) + 13)
                -> (FirstLimited . ProofColDivSeqBase.allDivSeq) (9 * (4 + 4 * (1 + 2 * z)) + 6)
                  -> (AllLimited . ProofColDivSeqBase.allDivSeq) (4 + 4 * (1 + 2 * z))
  --Uninhabited (AllLimited xs) where --使わなかった
  --  uninhabited a impossible
  --allToVoid : (x : Nat) -> Not $ AllLimited (allDivSeq (S x))
  --allToVoid x prf impossible
-- ---------------------------------


text:
%default total

%hide Prelude.Nat.LT
%hide Prelude.Interfaces.LT
%hide Prelude.Interfaces.(<=)
%hide Prelude.Interfaces.(>)
%hide Prelude.List.filter
%hide Prelude.List.merge
%hide Prelude.List.splitAt
%hide Prelude.WellFounded.Smaller

someList : List Nat
someList = [9,1,5,5,0,2,3,7,6,11,1]

data Acc : (lessThan : a -> a -> Type) -> (x : a) -> Type where
  MkAcc :
    -- potentially infinite tuple
    -- potentially infinite number of children in the tree
    -- but each subtree has a finite depth
    (acc : (y : a) -> (y `lessThan` x) -> Acc lessThan y)
      -> Acc lessThan x

interface WF (lt : a -> a -> Type) where
  wf : (x : _) -> Acc lt x

------------------------------------------

data LE : Nat -> Nat -> Type where
  LEZ : Z `LE` n
  LES : m `LE` n -> S m `LE` S n

LT : Nat -> Nat -> Type
LT m n = LE (S m) n

leRefl : x `LE` x
leRefl {x = Z} = LEZ
leRefl {x = (S x)} = LES leRefl

leTrans : (x `LE` y) -> (y `LE` z) -> (x `LE` z)
leTrans  LEZ _ = LEZ
leTrans (LES xLEy) (LES yLEz) = LES $ leTrans xLEy yLEz

wfLT : (x : Nat) -> Acc LT x
wfLT x = MkAcc (f x)
  where
    f : (x : Nat) -> (y : Nat) -> (y `LT` x) -> Acc LT y
    f (S x) y (LES yLEx) = MkAcc (\z, zLTy => f x z $ leTrans zLTy yLEx)
    -- LEZ cannot prove "strictly smaller than" because LT has (S _) on the LHS
    -- and LEZ has Z on the LHS

{-
decLE : (m, n : Nat) -> Dec (m `LE` n)
decLE Z n = Yes LEZ
decLE (S k) Z = No lemmaLTZ
decLE (S k) (S j) with (decLE k j)
  | Yes yep = Yes $ LES yep
  | No nope = No $ f nope
    where
      f : (LE k j -> Void) -> LE (S k) (S j) -> Void
      f nope (LES pf) = nope pf
-}

(<=) : Nat -> Nat -> Bool
(<=) Z n = True
(<=) (S m) Z = False
(<=) (S m) (S n) = m <= n

(>) : Nat -> Nat -> Bool
(>) m n = not (m <= n)

filter : (a -> Bool) -> List a -> List a
filter p [] = []
filter p (x :: xs) with (p x)
  | True = x :: filter p xs
  | False = filter p xs

------------------------------------------

shorter : List a -> List a -> Type
shorter xs ys = length xs `LT` length ys

wfShorter : (xs : List a) -> Acc Main.shorter xs
wfShorter xs = MkAcc (f xs)
  where
    f : (xs : List a) -> (ys : List a) -> (ys `Main.shorter` xs) -> Acc Main.shorter ys
    f (x :: xs) ys (LES ysLExs) = MkAcc (\zs, zsLTys => f xs zs $ leTrans zsLTys ysLExs)

-----------------------------------------

{- Comes from Prelude now
interface Sized a where
  size : a -> Nat
-}

Smaller : Sized a => a -> a -> Type
Smaller x y = size x `LT` size y

SizeAcc : Sized a => a -> Type
SizeAcc x = Acc Smaller x

wfSmaller : Sized a => (x : a) -> SizeAcc x
wfSmaller x = MkAcc $ f (size x)
  where
    f : (sizeX : Nat) -> (y : a) -> (size y `LT` sizeX) -> SizeAcc y
    f (S n) y (LES yLEx)
      = MkAcc (\z, zLTy =>
          f n z (leTrans zLTy yLEx)
        )

{- comes from Prelude now
implementation Sized (List a) where
  size = length
-}

{-
wfSmaller : Sized a => (x : a) -> Acc Smaller x
wfSmaller x = MkAcc (f x)
  where
    f : (x, y : a) -> (y `Smaller` x) -> Acc Smaller y
    f x y pf with (size x) proof xSize
      f x y pf | Z = lemmaLTZ pf
      f x y (LES yLEx) | S n = MkAcc (\z, zLTy => f x z $ leTrans zLTy ?rhs)
      -- we cannot do this because for the inductive step, we need a subterm of x
      -- but we have no way to obtain it
-}

-----------------------------------------

-- qSort with Acc

leS : (m `LE` n) -> (m `LE` S n)
leS  LEZ    = LEZ
leS (LES x) = LES (leS x)

filterLen : {p : a -> Bool} -> {xs : List a} -> length (filter p xs) `LE` length xs
filterLen {xs = []} = LEZ
filterLen {p} {xs = x :: xs} with (p x)
  | True = LES $ filterLen
  | False = leS $ filterLen

qsort' : (xs : List Nat) -> (Acc Main.shorter xs) -> List Nat
qsort' [] acc = []
qsort' (x :: xs) (MkAcc acc) =
  qsort' (filter (<= x) xs) (acc _ $ LES filterLen)
  ++ [x]
  ++ qsort' (filter (> x) xs) (acc _ $ LES filterLen)

qsort : List Nat -> List Nat
qsort xs = qsort' xs (wfShorter xs)

------------------------

-- QSortAcc directly

data QSortAcc : List Nat -> Type where
  QNil : QSortAcc []
  QCons : QSortAcc (filter (<= x) xs) -> QSortAcc (filter (> x) xs) -> QSortAcc (x :: xs)

qsortAccLo : (x : _) -> QSortAcc xs -> QSortAcc (filter (<= x) xs)
qsortAccLo x pf = ?rhsX1

qsortAccHi : (x : _) -> QSortAcc xs -> QSortAcc (filter (> x) xs)
qsortAccHi x pf = ?rhsX2

qsortA' : (xs : List Nat) -> QSortAcc xs -> List Nat
qsortA' [] QNil = []
qsortA' (x :: xs) (QCons lo hi)
    = qsortA' (filter (<= x) xs) lo
    ++ [x]
    ++ qsortA' (filter (> x) xs) hi

obsBool : (x : Bool) -> Either (x = True) (x = False)
obsBool True = Left Refl
obsBool False = Right Refl

filterDbl : (p : a -> Bool) -> (xs : List a) -> filter p (filter p xs) = filter p xs
filterDbl p xs = ?filterDblHole

qsortAcc : (xs : List Nat) -> QSortAcc xs
qsortAcc [] = QNil
qsortAcc (x :: xs) = QCons (f x xs) ?rhsX3
  where
    f : (x : Nat) -> (xs : List Nat) -> QSortAcc (filter (<= x) xs)
    f x [] = QNil
    f x (y :: xs) with (y <= x)
      | True = ?qSortAccA
      | False = ?qSortAccB

{-
    f x [y] with (y <= x)
      | True = QCons QNil QNil
      | False = QNil
    f x (y :: z :: xs) with (y <= x)
      | True = ?rhs
      | False = ?rhs2
-}

qsortA : List Nat -> List Nat
qsortA xs = qsortA' xs (qsortAcc xs)

---

-- via Acc

qsortAcc' : (xs : List Nat) -> Acc Main.shorter xs -> QSortAcc xs
qsortAcc' [] acc = QNil
qsortAcc' (x :: xs) (MkAcc acc)
    = QCons
        (qsortAcc' _ (acc _ $ LES filterLen))
        (qsortAcc' _ (acc _ $ LES filterLen))

qsort2 : List Nat -> List Nat
qsort2 xs = qsortA' xs $ qsortAcc' xs (wfShorter xs)

---

data Split : List a -> Type where
  SNil : Split []
  SOne : (x : a) -> Split [x]
  SMore :
    (x : a) -> (xs : List a)
    -> (y : a) -> (ys : List a)
    -> Split (x :: xs ++ y :: ys)

pushL : (x : a) -> Split xs -> Split (x :: xs)
pushL x  SNil = SOne x
pushL x (SOne y) = SMore x [] y []
pushL x (SMore y ys z zs) = SMore x (y :: ys) z zs

{-
split : (xs : List a) -> Split xs
split [] = SNil
split [x] = SOne x
split (x :: y :: xs) = step (1 + length xs) x y xs
  where
    step : (counter : Nat) -> (x, y : a) -> (xs : List a) -> Split (x :: y :: xs)
    step  Z    x y xs = SMore x [] y xs
    step (S Z) x y xs = SMore x [] y xs
    step (S (S k)) x y [] = SMore x [] y []
    step (S (S k)) x y (z :: xs) = pushL x $ step k y z xs
-}

halve : (xs : List a) -> Split xs
halve []  = SNil
halve [x] = SOne x
halve (x :: y :: xs) with (1 + length xs)
  halve (x :: y :: xs) |      Z  = SMore x [] y xs
  halve (x :: y :: xs) |    S Z  = SMore x [] y xs
  halve (x :: y :: []) | S (S k) = SMore x [] y []
  halve (x :: y :: z :: zs) | S (S k) = pushL x (halve (y :: z :: zs) | k)

shorterL : xs `shorter` (xs ++ y :: ys)
shorterL {xs = []} = LES LEZ
shorterL {xs = (x :: xs)} = LES shorterL

shorterR : ys `shorter` (x :: xs ++ ys)
shorterR {xs = []} = LES leRefl
shorterR {xs = x :: xs} = leS $ shorterR {x=x}

merge : List Nat -> List Nat -> List Nat
merge (x :: xs) (y :: ys) with (x <= y)
  | True  = x :: merge xs (y :: ys)
  | False = y :: merge (x :: xs) ys
merge [] ys = ys
merge xs [] = xs

msort1' : (xs : List Nat) -> (Acc Main.shorter xs) -> List Nat
msort1' xs acc with (halve xs)
  msort1' []  acc | SNil = []
  msort1' [x] acc | SOne x = [x]
  msort1' (y :: ys ++ z :: zs) (MkAcc acc) | SMore y ys z zs
    = merge
        (msort1' (y :: ys) (acc _ $ shorterL {xs = y::ys}))
        (msort1' (z :: zs) (acc _ $ shorterR {ys = z::zs}))

msort1 : List Nat -> List Nat
msort1 xs = msort1' xs (wfShorter xs)

---------------------------

mutual
  data MSAcc' : Split xs -> Type where
    MSNil : MSAcc' SNil
    MSOne : MSAcc' (SOne x)
    MSMore :
      MSAcc (x :: xs)
      -> MSAcc (y :: ys)
      -> MSAcc' (SMore x xs y ys)

  MSAcc : List a -> Type
  MSAcc xs = MSAcc' (halve xs)

msAcc : (xs : List Nat) -> MSAcc xs
msAcc xs with (wfShorter xs)
  msAcc xs | acc with (halve xs)
    msAcc []  | acc | SNil   = MSNil
    msAcc [x] | acc | SOne x = MSOne
    msAcc (y :: ys ++ z :: zs) | MkAcc acc | SMore y ys z zs
      = MSMore
        (msAcc _ | acc _ (shorterL {xs = y :: ys}))
        (msAcc _ | acc _ (shorterR {ys = z :: zs}))

msort2' : (xs : List Nat) -> MSAcc xs -> List Nat
msort2' xs acc with (halve xs)
  msort2' []  MSNil | SNil   = []
  msort2' [x] MSOne | SOne x = [x]
  msort2' (y :: ys ++ z :: zs) (MSMore accL accR) | SMore y ys z zs
    = merge
        (msort2' (y :: ys) accL)
        (msort2' (z :: zs) accR)

msort2 : List Nat -> List Nat
msort2 xs = msort2' xs (msAcc xs)

-- views for convenience
-- views for termination

-- Acc is more general induction hypothesis than QSortAcc
-- more general => easier to work with (easier to prove from)
  -- probably a bit harder to prove BUT
  -- still obviously true
  -- and proving the inductive step may be easier (actually feasible at all)

-- end up with views

-----------------------------------------------

%default total

subst : (f : a -> Type) -> x = y -> f x -> f y
subst f Refl = \x => x

data SplitC : (List a -> Type) -> List a -> Type where
  SCNil : SplitC srg []
  SCOne : (x : a) -> SplitC srg [x]
  SCMore :
    (x : a) -> (xs : List a)
    -> (y : a) -> (ys : List a)
    -> (rxs : srg (x :: xs))
    -> (rys : srg (y :: ys))
    -> SplitC srg (x :: xs ++ y :: ys)

data SplitRecC : List a -> Type where
  SRC : ((n : Nat) -> SplitC SplitRecC xs) -> SplitRecC xs

pushSC : (x : a) -> SplitC (const ()) xs -> SplitC (const ()) (x :: xs)
pushSC x  SCNil = SCOne x
pushSC x (SCOne y) = SCMore x [] y [] () ()
pushSC x (SCMore y ys z zs () ()) = SCMore x (y::ys) z zs () ()

splitAt : (n : Nat) -> (xs : List a) -> SplitC (const ()) xs
splitAt n [] = SCNil
splitAt n [x] = SCOne x
splitAt Z (x :: y :: ys) = SCMore x [] y ys () ()
splitAt (S k) (x :: y :: ys) = pushSC x $ splitAt k (y :: ys)

lemmaApp : (xs : List a) -> (ys : List a) -> length ys `LE` length (xs ++ ys)
lemmaApp []      ys = leRefl
lemmaApp (x::xs) ys = leS $ lemmaApp xs ys

splitC : (xs : List a) -> (n : Nat) -> SplitC SplitRecC xs
splitC xs n with (wfSmaller xs)
  splitC xs n | acc with (splitAt n xs)
    splitC []  n | acc | SCNil = SCNil
    splitC [x] n | acc | SCOne x = SCOne x
    splitC (y :: ys ++ z :: zs) n | MkAcc acc | SCMore y ys z zs () ()
        = SCMore y ys z zs
            (SRC $ \n' => splitC (y :: ys) n' | acc _ (LES shorterL))
            (SRC $ \n' => splitC (z :: zs) n' | acc _ (LES $ lemmaApp ys (z::zs)))

splitRecC : (xs : List a) -> SplitRecC xs
splitRecC xs = SRC $ splitC xs

unpack' : Nat -> List Nat -> List (List Nat)
unpack' x xs with (splitRecC (x :: xs))
  unpack' x    xs   | SRC splitAt with (splitAt x)
    unpack' x  []   | SRC splitAt | SCOne x = []  -- dangling length tag
    unpack' x (ys ++ z :: zs) | SRC splitAt | SCMore x ys z zs rys rzs
        = ys :: unpack' z zs | rzs

unpackL : List Nat -> List (List Nat)
unpackL []        = []
unpackL (x :: xs) = unpack' x xs

packL : List (List Nat) -> List Nat
packL [] = [0]
packL (xs :: xss) = length xs :: xs ++ packL xss

{-
*views> unpackL [1,3,0,3,1,2,3,2,0,1,4,1,2,3,4,0]
[[3], [1, 2, 3], [0, 1], [1, 2, 3, 4]] : List (List Nat)
-}

---------------------------------------------------------

{-
data ModView : Nat -> Nat -> Type where
  Base : ModView x y
  Step : ModView x y -> ModView x (x + y)

modView : (x', y : Nat) -> ModView (S x') y
modView  x'    Z = Base
modView  Z    (S y') = ?rhs_1  -- dividing by 1
modView (S k) (S y') = ?rhs_3
-}

{-
mod : (x : Nat) -> (y : Nat) -> Nat
mod x y acc with
-}

data SplitRec : List a -> Type where
  SRNil : SplitRec []
  SROne : (x : a) -> SplitRec [x]
  SRMore :
    (x : a) -> (xs : List a)
    -> (y : a) -> (ys : List a)
    -> (sxs : SplitRec (x :: xs))
    -> (sys : SplitRec (y :: ys))
    -> SplitRec (x :: xs ++ y :: ys)

splitRec : (xs : List a) -> SplitRec xs
splitRec xs with (wfSmaller xs)
  splitRec xs | acc with (halve xs)
    splitRec []  | acc | SNil   = SRNil
    splitRec [x] | acc | SOne x = SROne x
    splitRec (y :: ys ++ z :: zs) | MkAcc acc | SMore y ys z zs
      = SRMore y ys z zs
          (splitRec _ | acc _ (shorterL {xs = y::ys}))
          (splitRec _ | acc _ (shorterR {x=z} {ys = z::zs}))

msortR : List Nat -> List Nat
msortR xs with (splitRec xs)
  msortR []  | SRNil   = []
  msortR [x] | SROne x = [x]
  msortR (y :: ys ++ z :: zs) | SRMore y ys z zs sys szs
    = merge
        (msortR (y :: ys) | sys)
        (msortR (z :: zs) | szs)

------------------------

data SnocViewRec : List a -> Type where
  SVRNil : SnocViewRec (Nil {elem=a})
  SVRSnoc : (sxs : SnocViewRec xs)
    -> (x : a)
    -> SnocViewRec (xs ++ [x])

%hide Prelude.Basics.cong

cong : {f : a -> b} -> x = y -> f x = f y
cong Refl = Refl

appNil : (xs : List a) -> xs ++ [] = xs
appNil [] = Refl
appNil (x :: xs) = cong $ appNil xs

appAssoc : (xs : List a) -> (ys : List a) -> (zs : List a) -> xs ++ (ys ++ zs) = (xs ++ ys) ++ zs
appAssoc [] ys zs = Refl
appAssoc (x :: xs) ys zs = cong $ appAssoc xs ys zs

sr : (sxs : SnocViewRec xs) -> (ys : List a) -> SnocViewRec (xs ++ ys)
sr {xs} sxs [] = rewrite appNil xs in sxs
sr {xs} sxs (y :: ys) = rewrite appAssoc xs [y] ys in sr (SVRSnoc sxs y) ys

snocViewRec : (xs : List a) -> SnocViewRec xs
snocViewRec = sr SVRNil

--------------------

data VList : List a -> Type where
  VNil : VList []
  VOne : (x : a) -> VList [x]
  VMore : (x : a) -> VList xs -> (y : a) -> VList (x :: xs ++ [y])

pushV : (x : a) -> VList xs -> VList (x :: xs)
pushV x  VNil = VOne x
pushV x (VOne y) = VMore x VNil y
pushV x (VMore y ys z) = VMore x (pushV y ys) z

vList : (xs : List a) -> VList xs
vList [] = VNil
vList (x :: xs) = pushV x (vList xs)

{-
vStep : SnocViewRec (x :: xs ++ [y]) -> SnocViewRec (x :: xs)
vStep {x} {xs} {y} (SVRSnoc {xs = x :: xs} sxs y) = sxs
-}

max_stars_repo_name: MaxDesiatov/ttstar

max_issues_repo_name: MaxDesiatov/ttstar

max_forks_repo_name: MaxDesiatov/ttstar


text:
module Flutter.Widgets.Functions

import Dart.FFI
import public Dart.Core -- for DartList
import public Dart.FFI.Upcast
import public Dart.FFI.UpcastList
import Flutter.FFI

%foreign "Dart:runApp,package:flutter/widgets.dart"
prim__runApp : Widget -> PrimIO ()

export
runApp : IsAssignableFrom Widget widget => widget -> IO ()
runApp w = primIO (prim__runApp (upcast w))

export
widgets : UpcastList Widget -> IO (DartList Widget)
widgets ws = into !List.new ws


text:
module Local

empty : ()
empty = ()

max_stars_repo_name: chrrasmussen/Idris-Deps

max_issues_repo_name: chrrasmussen/Idris-Deps

max_forks_repo_name: chrrasmussen/Idris-Deps


text:
module Main

import BTree

main : IO ()
main = do let t = toTree [1,8,2,7,9,3]
          print (BTree.toList t)


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

insert : a -> Vect x a -> Vect (S x) a
insert = Cons

max_stars_repo_name: LucasTornai/pgc-ufabc

max_issues_repo_name: LucasTornai/pgc-ufabc

max_forks_repo_name: LucasTornai/pgc-ufabc


text:
-- --------------------------------------------------------------- [ Day08.idr ]
-- Module      : Data.Advent.Day08
-- Description : My solution to the Day 8 puzzle of the 2016 Advent of Code.
-- Copyright   : Copyright (c) 2016, Eric Bailey
-- License     : MIT
-- Link        : http://adventofcode.com/2016/day/7
-- --------------------------------------------------------------------- [ EOH ]
||| Day 8: Two-Factor Authentication
module Data.Advent.Day08

import Data.Vect

import public Lightyear
import public Lightyear.Char
import public Lightyear.Strings
import public Lightyear.StringFile

%default total

-- -------------------------------------------------------------- [ Data Types ]

%access public export

data Pixel = Off | On

implementation Eq Pixel where
    On  == On  = True
    Off == Off = True
    px1 == px2 = False

implementation Show Pixel where
    show Off = "."
    show On  = "#"

Screen : Nat -> Nat -> Type
Screen w h = Vect h (Vect w Pixel)

implementation [showScreen] Show (Screen w h) where
    show = unlines . toList . map (concatMap show)

data Rect : Nat -> Nat -> Type where
     MkRect : Fin w -> Fin h -> Rect w h

implementation Show (Fin n) where
    show = show . finToNat

-- showFin : Fin n -> String
-- showFin = show . finToNat

implementation Show (Rect w h) where
    show (MkRect w h) = "rect " ++ show w ++ "x" ++ show h

data Rotate : Nat -> Nat -> Type where
     Row : Fin w -> Fin h -> Rotate h w
     Col : Fin w -> Fin h -> Rotate w h

implementation Show (Rotate xy by) where
    show (Row y by) = "rotate row y=" ++ show y ++ " by " ++ show by
    show (Col x by) = "rotate column x=" ++ show x ++ " by " ++ show by

-- ----------------------------------------------------------------- [ Parsers ]

%access export

partial
side : (n : Nat) -> Parser (Fin n)
side n = do Just len <- (\m => integerToFin m n) <$> integer
              | Nothing => fail "out of bounds"
            pure len

partial
rect : Parser (Rect w h)
rect = liftA2 MkRect (token "rect" *> side w)
                     (token "x"    *> side h)  <?> "rect AxB"

partial
maybeFin : (n : Nat) -> Parser (Maybe (Fin n))
maybeFin n = marshal <$> integer <* spaces <?>
             "a number strictly less than " ++ show n
  where
    marshal : Integer -> Maybe (Fin n)
    marshal m = integerToFin m n

partial
row : Parser (Rotate w h)
row {w} {h} = do Just y  <- token "rotate row y=" *> maybeFin h
                 Just by <- token "by" *> maybeFin w
                 pure $ Row y by

partial
column : Parser (Rotate w h)
column {w} {h} = do Just x  <- token "rotate column x=" *> maybeFin w
                    Just by <- token "by" *> maybeFin h
                    pure $ Col x by

partial
rotation : Parser (Rotate w h)
rotation = row <|> column <?> "a rotation"

partial
rectOrRotation : Parser (Either (Rect w h) (Rotate w h))
rectOrRotation {w} {h} = case !(opt (rect {w} {h})) of
                              Just rec => pure $ Left rec
                              Nothing  => Right <$> rotation {w} {h}

-- ----------------------------------------------------------------- [ Helpers ]

%access private

mapIndexed : (f : (a, Nat) -> a) -> Vect n a -> Vect n a
mapIndexed f xs {n} = map f (zip xs (go n Z))
  where
    go : (m : Nat) -> Nat -> Vect m Nat
    go Z _     = []
    go (S k) x = x :: go k (S x)

-- ------------------------------------------------------------------ [ Proofs ]

%access private

finToLTE : (f : Fin n) -> LTE (finToNat f) n
finToLTE FZ               = LTEZero
finToLTE (FS _) {n = S _} = LTESucc (finToLTE _)

total compositeLemma : (left, right : Nat) -> {auto smaller : LTE left right} ->
  (k : Nat ** right = left + k)
compositeLemma left right = (right - left ** go left right)
  where
    go : (left, right : Nat) -> {auto smaller : LTE left right} ->
      right = left + (right - left)
    go Z right        = rewrite minusZeroRight right in Refl
    go (S k) (S j) {smaller} =
        let inductiveHypothesis = go k j {smaller = fromLteSucc smaller} in
            eqSucc j (k + (minus j k)) inductiveHypothesis

total updateLemma : (prf : n = finToNat by + m) -> n = m + finToNat by
updateLemma {by} {m} prf = rewrite plusCommutative m (finToNat by) in prf

-- -- ---------------------------------------------------------------- [ Logic ]

turnOn : Rect sw sh -> Screen sw sh -> Screen sw sh
turnOn (MkRect w h) = mapIndexed f
  where
    g : (Pixel, Nat) -> Pixel
    g (col, x) = if x < (finToNat w) then On else col
    f : (Vect m Pixel, Nat) -> Vect m Pixel
    f (row, y) = if y < (finToNat h) then mapIndexed g row else row

namespace Vect

  rotate : (by : Fin n) -> Vect (finToNat by + m) a ->
           (m ** Vect (m + finToNat by) a)
  rotate by xs {m} = let (ys,zs) = splitAt (finToNat by) xs in
                         (m ** zs ++ ys)

updateRow : (by : Fin n) -> (row : Vect n Pixel) -> Vect n Pixel
updateRow {n} by row =
    let (m ** prf)    = compositeLemma (finToNat by) n {smaller = finToLTE by}
        (_ ** newRow) = rotate by $ the (Vect (finToNat by + m) _) $
                        rewrite sym prf in row in
                        rewrite updateLemma prf in
                                newRow

namespace Fin

    rotate : Fin n -> Fin n
    rotate f {n} = let x = (-) n (finToNat f) {smaller = finToLTE f} in
                       fromMaybe f (natToFin x n) -- HACK

namespace Screen

  empty : {w, h : Nat} -> Screen w h
  empty {w} {h} = replicate h (replicate w Off)

  rotate : (Rotate w h) -> Screen w h -> Screen w h
  rotate (Row y by) screen     = updateAt y (updateRow (rotate by)) screen
  rotate (Col x by) screen {h} = transpose $
                                 updateAt x (updateRow (rotate by)) $
                                 transpose screen

howManyLit : Screen w h -> Nat
howManyLit = foldr ((+) . foldr go Z) Z
  where
    go : Pixel -> Nat -> Nat
    go On  = S
    go Off = id

justDoIt : List (Either (Rect w h) (Rotate w h)) -> Screen w h
justDoIt = foldl (\s => either (flip turnOn s) (flip rotate s)) empty

-- ---------------------------------------------------------------- [ Examples ]

ex1 : Screen 7 3
ex1 = turnOn (MkRect 3 2) empty

ex2 : Screen 7 3
ex2 = rotate (Col 1 1) ex1

ex3 : Screen 7 3
ex3 = rotate (Row 0 4) ex2

ex4 : Screen 7 3
ex4 = rotate (Col 1 1) ex3

partial
examples : Either String (List (Either (Rect 7 3) (Rotate 7 3)))
examples = parse (some (rectOrRotation <* spaces)) $ unlines [
             "rect 3x2",
             "rotate column x=1 by 1",
             "rotate row y=0 by 4",
             "rotate column x=1 by 1"
           ]

||| Convenient representation of Part One examples for the REPL.
partial
prettyExamples : Either String (List (List String))
prettyExamples = transpose .
                 map (lines . show @{showScreen}) .
                 scanl (\s => either (flip turnOn s) (flip rotate s)) empty <$>
                 examples

-- -------------------------------------------------------------- [ Main Logic ]

%access export

main' : Parser a -> (a -> String) -> IO ()
main' p f =
    either putStrLn (putStrLn . f)
           !(run $ parseFile (const show) (const id) p "input/day08.txt")

-- ---------------------------------------------------------------- [ Part One ]

namespace PartOne

    partial main : IO ()
    main = main' (some (rectOrRotation {w=50} {h=6} <* spaces))
                 (show . howManyLit . justDoIt)

-- ---------------------------------------------------------------- [ Part Two ]

namespace PartTwo

    partial main : IO ()
    main = main' (some (rectOrRotation {w=50} {h=6} <* spaces))
                 (show @{showScreen} . justDoIt)

-- -------------------------------------------------------------------- [ Main ]

namespace Main

    partial main : IO ()
    main = putStr   "Part One: " *> PartOne.main *>
           putStrLn "Part Two:"  *> PartTwo.main

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

max_stars_repo_name: yurrriq/advent-of-code


text:
module sorting_with_proof

import Data.Vect
import Data.Fin

||| Vectors of Natural numbers
total
NatVect : Nat -> Type
NatVect n = Vect n Nat

||| The type Fin n -> Fin n
total
F_Fin : Nat -> Type
F_Fin n = (Fin n) -> (Fin n)

||| Identity function
total
Idt : (t : Type) -> t -> t
Idt s a = a

||| The type of permutation/bijection of {1,...,n}.
||| Notice that for finite sets one sided inverse is enough.
||| Also I have a strong feeling that using univalence the last part of the definition is
||| equivalent to saying that (g . f) and Idt are equivalent
total
Perm : Nat -> Type
Perm n = ( f : F_Fin n ** ( g : F_Fin n ** ((a : (Fin n)) -> ((g (f a)) = a))))

||| Second definition of perm. I have strong feeling that using univalence this is equivalent
||| to the first definition.
total
Perm2 : Nat -> Type
Perm2 n = ( f : F_Fin n ** ( g : F_Fin n ** ((g . f) = (Idt (Fin n)))))

data Finite : Nat -> Type where
    FinZ : (k : Nat) -> (Finite (S k))
    FinS : (k : Nat) -> (Finite k) -> (Finite (S k))

total
Finite_to_Fin : (k : Nat) -> (Finite k) -> (Fin k)
Finite_to_Fin Z a impossible
Finite_to_Fin (S k) (FinZ k) = FZ
Finite_to_Fin (S k) (FinS k nm) = FS (Finite_to_Fin k nm)

total
Fin_to_Finite : (k : Nat) -> (Fin k) -> (Finite k)
Fin_to_Finite Z a impossible
Fin_to_Finite (S k) FZ = FinZ k
Fin_to_Finite (S k) (FS l) = FinS k (Fin_to_Finite k l)

||| Predecessor function for finite
total
predFinite : (k : Nat) -> (Finite k) -> (Finite k)
predFinite Z a impossible
predFinite (S k) (FinZ k) = FinZ k
predFinite (S (S k)) (FinS (S k) (FinZ k)) = FinZ (S k)
predFinite (S (S k)) (FinS (S k) l) = FinS (S k) (predFinite (S k) l)

||| Predecessor function for fin
total
predFin : (n : Nat) -> (Fin n) -> (Fin n)
predFin n a = Finite_to_Fin n ( predFinite n (Fin_to_Finite n a))

||| Type of proofs that a vector is sorted in increasing order.
||| Note that the predecessor function takes care of the first index
total
SortProof : (n : Nat) -> (NatVect n) -> (Fin n) -> Type
SortProof Z v a impossible
SortProof (S k) v l = LTE (Vect.index (pred l) v) (Vect.index l v)

||| Type of the sorted vectors.
SortedVect : Type
SortedVect = (n : Nat ** (v : (NatVect n)  ** ((k : Fin n) -> (SortProof n v k))))


text:
module TestRunner

import CIO
import Idrlisp

%default covering

data Command
  = ParseSuccess String String
  | ParseFailure String
  | CompileSuccess String String
  | CompileFailure String
  | EvalSuccess String String
  | EvalFailure String
  | EvalAll String

record TestCase where
  constructor MkTestCase
  header : String
  command : Command

namespace Exec
  parsing : String -> CIO String Value
  parsing input = either throw pure $ parseExpr input

  compiling : Context -> Value -> CIO String (Code Value)
  compiling ctx value = lift (compileExpr ctx value) >>= either throw pure

  evaluating : Context -> Value -> CIO String Value
  evaluating ctx value = lift (evalExpr ctx value) >>= either throw pure

  outputs : Show a => String -> a -> CIO String ()
  outputs expected a =
    if trim (show a) == expected
       then pure ()
       else throw $ show a

  outputs' : String -> Value -> CIO String ()
  outputs' expected a = do
    a' <- lift $ showIO a
    if trim a' == expected
       then pure ()
       else throw a'

  fails : Show b => (a -> CIO String b) -> a -> CIO String ()
  fails f x = do
    err <- (Just <$> f x) `catch` \_ => pure Nothing
    case err of
      Nothing => pure ()
      Just x => throw $ show x

  execCommand : Context -> Command -> CIO String ()
  execCommand ctx (ParseSuccess input output) = parsing input >>= outputs output
  execCommand ctx (ParseFailure input) = fails parsing input
  execCommand ctx (CompileSuccess input output) = parsing input >>= compiling ctx >>= outputs output
  execCommand ctx (CompileFailure input) = parsing input >>= fails (compiling ctx)
  execCommand ctx (EvalSuccess input output) = parsing input >>= evaluating ctx >>= outputs' output
  execCommand ctx (EvalFailure input) = parsing input >>= fails (evaluating ctx)
  execCommand ctx (EvalAll input) = do
    program <- either throw pure $ parseProgram input
    result <- lift $ evalProgram ctx program
    case result of
      Left (_, err) => throw err
      Right _ => pure ()

  execTestCase : Context -> TestCase -> CIO String Bool
  execTestCase ctx (MkTestCase header command) =
    do
      execCommand ctx command
      pure False
    `catch`
    \e => do
      lift $ fPutStrLn stderr $ "Test failed at " ++ header ++ ": " ++ e
      pure True

namespace Read
  readLine : File -> CIO String String
  readLine fh =
    case !(lift $ fGetLine fh) of
      Right s =>
        case length s of
          Z => throw "End of input"
          S k => pure $ substr 0 k s
      Left e => throw $ show e

  readLines : Nat -> File -> CIO String String
  readLines k fh = do
    strs <- sequence $ replicate k $ readLine fh
    pure $ concat $ intersperse "\n" strs

  readCommand : File -> CIO String Command
  readCommand fh =
    case split (== ' ') !(readLine fh) of
      ["PARSE_SUCCESS", input, output] => do
        input <- readLines (cast input) fh
        output <- readLines (cast output) fh
        pure $ ParseSuccess input output
      ["PARSE_FAILURE", input] => do
        input <- readLines (cast input) fh
        pure $ ParseFailure input
      ["COMPILE_SUCCESS", input, output] => do
        input <- readLines (cast input) fh
        output <- readLines (cast output) fh
        pure $ CompileSuccess input output
      ["COMPILE_FAILURE", input] => do
        input <- readLines (cast input) fh
        pure $ CompileFailure input
      ["EVAL_SUCCESS", input, output] => do
        input <- readLines (cast input) fh
        output <- readLines (cast output) fh
        pure $ EvalSuccess input output
      ["EVAL_FAILURE", input] => do
        input <- readLines (cast input) fh
        pure $ EvalFailure input
      ["EVAL_ALL", input] => do
        input <- readLines (cast input) fh
        pure $ EvalAll input
      xs =>
        throw $ "Unknown test comamnd: " ++ show xs

  readTestCases : File -> CIO String (List TestCase)
  readTestCases fh = do
    header <- (Just <$> readLine fh) `catch` \_ => pure Nothing
    case header of
      Nothing => pure []
      Just header => do
        command <- readCommand fh
        testCases <- readTestCases fh
        pure $ MkTestCase header command :: testCases

export
run : Context -> File -> IO (Either String Nat)
run ctx fh = runCIO $ do
  testCases <- readTestCases fh
  results <- traverse (execTestCase ctx) testCases
  pure $ length $ filter id results

max_stars_repo_name: yubrot/idrlisp

max_issues_repo_name: yubrot/idrlisp

max_forks_repo_name: yubrot/idrlisp


text:
module Main
import System
import Data.Fuel
import Control.Monad.Reader
import Data.SortedSet

%default total
%hide Prelude.Pairs.DPair.fst
%hide Data.SortedSet.toList

data Colour = Error | Pending | Done

putStatus : Colour -> String -> IO ()
putStatus col = putStrLn . (colour++) . (++"\x1b[0m")
  where
    colour : String
    colour = case col of
                  Error   => "\x1b[38;5;1m"
                  Done    => "\x1b[38;5;2m"
                  Pending => "\x1b[38;5;3m"

err : String -> IO ()
err = putStatus Error

errExists : String -> IO ()
errExists file = err $ file ++ " does not exist"

errOpen : String -> IO ()
errOpen file = err $ file ++ " cannot be opened"

errTime : IO ()
errTime = err "cannot get modification time"

filename : String -> String
filename = fst . break (=='.')

extension : String -> String
extension = snd . break (=='.')

ytdl : (playlist : String) -> IO ()
ytdl pl = do
  putStatus Pending $ "downloading " ++ pl
  system $ unwords
    [ "pushd $HOME/music/" ++ (filename pl) ++ " > /dev/null;"
    , "youtube-dl"
    , "-xio '%(title)s.%(ext)s'"
    , "--geo-bypass"
    , "--external-downloader=aria2c"
    , "--add-metadata"
    , "--external-downloader-args='-j 8 -c -x 8 -m 10 -k 5M -s 8'"
    , "-a"
    , "../" ++ pl
    , "> /dev/null;"
    , "popd > /dev/null"
    ]
  putStatus Done "done"

mpd : (playlist : String) -> IO ()
mpd pl = do
  let dr = filename pl
  putStatus Pending $ "updating mpd " ++ dr ++ "..."
  system $ concatMap (++" > /dev/null;")
    [ "mpc rm " ++ dr
    , "mpc clear"
    , "mpc add " ++ dr
    , "mpc save " ++ dr
    ]
  putStatus Done "done"

data Options = CreateMissing
             | UpdateMPD
             | DownloadSongs
             | DisplayHelp

Show Options where
  show CreateMissing = "create missing"
  show UpdateMPD = "update mpd"
  show DownloadSongs = "download songs"
  show DisplayHelp = "display help"

Eq Options where
  CreateMissing == CreateMissing = True
  UpdateMPD     == UpdateMPD     = True
  DownloadSongs == DownloadSongs = True
  DisplayHelp   == DisplayHelp   = True
  _             == _             = False

Ord Options where
  compare DisplayHelp DisplayHelp     = EQ
  compare DisplayHelp x               = LT
  compare x DisplayHelp               = GT
  compare CreateMissing CreateMissing = EQ
  compare UpdateMPD UpdateMPD         = EQ
  compare DownloadSongs DownloadSongs = EQ
  compare CreateMissing UpdateMPD     = LT
  compare CreateMissing DownloadSongs = LT
  compare DownloadSongs UpdateMPD     = LT
  compare UpdateMPD CreateMissing     = GT
  compare UpdateMPD DownloadSongs     = GT
  compare DownloadSongs CreateMissing = GT

update : Fuel -> SortedSet Options -> String -> IO ()
update Dry _ _ = pure ()
update (More more) opts pl = do
  let dr = filename pl
  Right playlist  <- openFile pl Read | Left _ => errOpen pl
  Right directory <- openFile dr Read | Left _ =>
    do closeFile playlist
       errExists dr
       when (CreateMissing `contains` opts) $ do
            putStatus Pending "creating directory..."
            Right _ <- createDir dr | Left _ => err ("failed to create " ++ dr)
            update more opts pl
  let cleanup = do closeFile playlist
                   closeFile directory
  Right dirtime   <- fileModifiedTime directory | Left _ => do cleanup; errTime
  Right lsttime   <- fileModifiedTime playlist  | Left _ => do cleanup; errTime
  when (dirtime < lsttime) $ do ytdl pl; mpd pl
  cleanup

loop : Fuel -> Directory -> IO (List String)
loop Dry _ = pure empty -- convince the type checker that we're total
loop (More more) dir = do
  Right entry <- dirEntry dir | Left _ => pure []
  entries     <- loop more dir
  pure $ filter ((==".lst") . extension) (entry :: entries)

option : List String -> List Options
option [] = []
option ("-A" :: xs) = CreateMissing :: option xs
option ("-D" :: xs) = DownloadSongs :: option xs
option ("-U" :: xs) = UpdateMPD     :: option xs
option (_ :: xs) = option xs

help : IO ()
help = putStrLn """
usage: update -[ADU]

-A  Add missing directories
-D  Download songs
-U  Update MPD playlists"""

partial
main : IO ()
main = do
  options <- map option getArgs
  case DisplayHelp `elem` options of
       True => help
       False => do
         system "mpc update"
         Just home <- getEnv "HOME" | Nothing => errExists "HOME"
         let music = home ++ "/music"
         Right dir <- dirOpen music | Left _ => errExists music
         True      <- changeDir music | False => errOpen music
         lst       <- loop forever dir
         traverse_ (update forever $ fromList options) lst
         dirClose dir
         pure ()

max_stars_repo_name: simonank/dotfiles

max_issues_repo_name: simonank/dotfiles

max_forks_repo_name: simonank/dotfiles


text:
module Charsets

%default total
%access public export

data Charset : Type where
  UTF8 : Charset
%name Charset charset

max_stars_repo_name: camelpunch/mrk

max_issues_repo_name: camelpunch/mrk

max_forks_repo_name: camelpunch/mrk


text:
-- Case-typed argument is defined in `TTImp` as an intermediate function applied to *all* previous arguments
-- (disregarding whether there exists an actual dependency of not).
-- The follolwing check ensures that those types being applied to different count of arguments mean the same type.

x : {a : Type} -> (xs : List a) -> (v : List a) -> (0 _ : case v of [] => Unit; (x::xs) => Void) -> Nat
y : {a : Type} ->                  (v : List a) -> (0 _ : case v of [] => Unit; (x::xs) => Void) -> Nat

xy : {a : Type} -> (xs : List a) -> (v : List a) -> (0 c : case v of [] => Unit; (x::xs) => Void) -> x {a} xs v c = y {a} v c

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
module Replica.App.FileSystem

import Control.App
import System.Directory

%default covering

public export
data FSError
  = MissingFile String
  | CantAccess String
  | CantWriteFile String
  | CantReadFile String
  | CantCreate String
  | UnmanagedError String
  | FileExists String

export total
toFSError : FileError -> String -> FSError
toFSError (GenericFileError i) = UnmanagedError
toFSError FileReadError = CantReadFile
toFSError FileWriteError = CantWriteFile
toFSError FileNotFound = MissingFile
toFSError PermissionDenied = CantAccess
toFSError FileExists = FileExists

public export
interface Exception FSError e => FileSystem e where
  createDir : (dirname : String) -> App e ()
  getCurrentDir : App e String
  changeDir : (dirname : String) -> App e ()
  removeDir : (dirname : String) -> App e ()
  writeFile : (filename : String) -> (content : String) -> App e ()
  readFile : (filename : String) -> App e String

export
Has [PrimIO, Exception FSError] e => FileSystem e where
  createDir d = do
    Right x <- primIO $ createDir d
      | Left err => throw (toFSError err d)
    pure x
  getCurrentDir = do
    Just dir <- primIO currentDir
      | Nothing => throw (UnmanagedError "current dir")
    pure dir
  changeDir d = do
    res <- primIO $ changeDir d
    if res
       then pure ()
       else throw (CantAccess d)
  removeDir d = primIO $ removeDir d
  writeFile f content = do
    Right x <- primIO $ writeFile f content
      | Left err => throw (toFSError err f)
    pure x
  readFile f = do
    Right x <- primIO $ readFile f
      | Left err => throw (toFSError err f)
    pure x

max_stars_repo_name: teto/REPLica

max_issues_repo_name: teto/REPLica

max_forks_repo_name: teto/REPLica


text:
module Data.Time.LocalTime.ZonedTime

import Data.Time.LocalTime.TimeZone
import Data.Time.LocalTime.Internal.LocalTime
import Data.Time.Clock.Internal.UTCTime
-- import Data.Time.Clock.System

import Generics.Derive

%default total
%language ElabReflection

-- ---------------------------------------------------------------------------

||| A local time together with a time zone.
|||
||| There is no 'Eq' instance for @ZonedTime@.
||| If you want to compare local times, use 'zonedTimeToLocalTime'.
||| If you want to compare absolute times, use 'zonedTimeToUTC'.
public export
record ZonedTime where
  constructor MkZonedTime
  localtime : LocalTime
  timezone : TimeZone
%runElab derive "ZonedTime" [Generic, Eq, Ord, DecEq]

public export
Show ZonedTime where
  show x = show x.localtime ++ " " ++ show x.timezone

-- ---------------------------------------------------------------------------

export utcToZonedTime : TimeZone -> UTCTime -> ZonedTime
utcToZonedTime zone time = MkZonedTime (utcToLocalTime zone time) zone

export zonedTimeToUTC : ZonedTime -> UTCTime
zonedTimeToUTC x = localTimeToUTC x.timezone x.localtime

{-  FIXME: timezone
export getZonedTime : IO ZonedTime
getZonedTime = do
    t <- getCurrentTime
    zone <- getTimeZone t
    return (utcToZonedTime zone t)

export utcToLocalZonedTime : UTCTime -> IO ZonedTime
utcToLocalZonedTime t = do
    zone <- getTimeZone t
    return (utcToZonedTime zone t)
    -}

-- --------------------------------------------------------------------------
-- vim: tw=80 sw=2 expandtab :


text:
module Main

import Fs
import Control.Monad.Free
import Data.Vect

anyVect : (n ** Vect n String)
anyVect = (3 ** ["Rod", "Jane", "Freddy"])

data FileSystemF next
  = WriteFile FilePath String next
  | ReadFile FilePath (String -> next)

FileSystem : Type -> Type
FileSystem = Free FileSystemF

Functor FileSystemF where
  map f (WriteFile filePath contents next) = WriteFile filePath contents (f next)
  map f (ReadFile filePath fNext) = ReadFile filePath (f . fNext)

writeFile : FilePath -> Contents -> FileSystem Unit
writeFile filePath contents = liftFree $ WriteFile filePath contents ()

readFile : FilePath -> FileSystem String
readFile filePath = liftFree $ ReadFile filePath id

echoHello : FileSystem Unit
echoHello = do
  writeFile "foo.txt" "hello, world!"
  contents <- readFile "foo.txt"
  writeFile "foo.txt" (contents <+> "!")

interpreter : FileSystemF a -> JS_IO a
interpreter (WriteFile filePath contents next) = writeFileSync filePath contents *> pure next
interpreter (ReadFile filePath fNext) = do
  contents <- readFileSync filePath
  pure (fNext contents)

main : JS_IO ()
main = foldFree interpreter echoHello

max_stars_repo_name: idris-industry/idris-free

max_issues_repo_name: idris-industry/idris-free

max_forks_repo_name: idris-industry/idris-free


text:
data Bad : Type where
  R : (Bad -> Nat) -> Bad


text:
module Control.Monad.Morph

import Control.Monad.Either
import Control.Monad.Identity
import Control.Monad.Maybe
import Control.Monad.RWS
import Control.Monad.Reader
import Control.Monad.State
import Control.Monad.Writer

export
generalize : Applicative m => Identity a -> m a
generalize = pure . runIdentity

public export
interface MFunctor (0 t : (Type -> Type) -> (Type -> Type)) where
  hoist : Monad m => (forall b. m b -> m' b) -> t m a -> t m' a

export
MFunctor (EitherT e) where
  hoist k = MkEitherT . k . runEitherT

export
MFunctor MaybeT where
  hoist k = MkMaybeT . k  . runMaybeT

export
MFunctor (ReaderT s) where
  hoist k m = MkReaderT $ k . flip runReaderT m

export
Monoid s => MFunctor (WriterT s) where
  hoist k m = MkWriterT $ k . unWriterT m

export
MFunctor (StateT s) where
  hoist k m = ST $ k . flip runStateT m

export
MFunctor (RWST r w s) where
  hoist k m = MkRWST $ \r, w, s => k $ unRWST m r w s


text:
> module SequentialDecisionProblems.ReachabilityDefaults

> import SequentialDecisionProblems.CoreTheory

> import Sigma.Sigma

> %default total
> %auto_implicits off

This is the default implementation of |Reachable|: all states at the
first decision step are reachable; a state at decision step |t' = t + 1|
is reachable iff it has a reachable predecessor:

> SequentialDecisionProblems.CoreTheory.Reachable {t' = Z}   x' = Unit
> SequentialDecisionProblems.CoreTheory.Reachable {t' = S t} x' = Sigma (State t) (\ x => ReachablePred {t = t} x x')

If users can show that the monad |M| fulfills the specification

> allElemSpec1 : {A : Type} -> {P : A -> Type} ->
>                (ma : M A) -> ((a : A) -> a `Elem` ma -> P a) -> All P ma

we can easily shoe that if |x| is reachable and admits a control |y|,
then all states that can be obtained by selecting |y| in |x| are also
reachable, as required by the core theory:

> SequentialDecisionProblems.CoreTheory.reachableSpec1 {t} x r y = s where
>   f : (x' : State (S t)) -> x' `Elem` (nexts t x y) -> Reachable {t' = S t} x'
>   f x' x'en = MkSigma x (r, MkSigma y x'en)
>   s : All Reachable (nexts t x y)
>   s = allElemSpec1 (nexts t x y) f

> {-

> ---}


text:
module DateRange

import Coda.Date
import Coda.Range

%access public export
%default total

daysToMonth : Year -> Month -> Integer
daysToMonth year month = count month' (monthOrder month')
  where
    count : Month -> Nat -> Integer
    count m Z = 0
    count m (S k) = (toIntegerNat $ monthDays year m) + count (previousMonth m) k

    month' : Month
    month' = previousMonth month

daysInDate : Date -> Integer
daysInDate (MkDate year@(MkYear y) month (MkDay days)) =
  let
    yearDays = (y - 1) * 365
    monthDays = daysToMonth year month
  in
    yearDays + monthDays + (toIntegerNat days)

-- Distance Date Integer where

max_stars_repo_name: ostera/idris-coda

max_issues_repo_name: ostera/idris-coda

max_forks_repo_name: ostera/idris-coda


text:
module Cordial.Model.Common.Direction

import Cordial.Model.Common.Essential

%access public export
%default total

||| How information flows through the channel.
data Flow : Type where
  PC     : Flow -- Producer to Consumer
  CP     : Flow -- Consumer to Producer
  PCCP   : Flow -- Bi Directional
  ConstP : Flow -- Always producer
  ConstC : Flow -- Always consume

data DirectionTy = IsIn | IsOut | IsInOut

data DirectionKind : Endpoint -> Flow -> DirectionTy -> Type where
    InPC  : DirectionKind CONSUMER PC IsIn
    OutPC : DirectionKind PRODUCER PC IsOut

    InCP  : DirectionKind PRODUCER CP IsIn
    OutCP : DirectionKind CONSUMER CP IsOut

    InOut : DirectionKind pccp PCCP IsInOut

    OutConstP : DirectionKind p ConstP IsOut
    InConstC  : DirectionKind c ConstC IsIn

%hint
calcDirTy : Endpoint -> Flow -> DirectionTy
calcDirTy PRODUCER PC     = IsOut
calcDirTy CONSUMER PC     = IsIn
calcDirTy PRODUCER CP     = IsIn
calcDirTy CONSUMER CP     = IsOut
calcDirTy y        PCCP   = IsInOut
calcDirTy y        ConstP = IsOut
calcDirTy y        ConstC = IsIn

%hint
calcDirKind : (endpoint : Endpoint)
           -> (flow     : Flow)
           -> DirectionKind endpoint flow (calcDirTy endpoint flow)
calcDirKind e f with (e)
  calcDirKind e f | PRODUCER with (f)
    calcDirKind e f | PRODUCER | PC = OutPC
    calcDirKind e f | PRODUCER | CP = InCP
    calcDirKind e f | PRODUCER | PCCP = InOut
    calcDirKind e f | PRODUCER | ConstP = OutConstP
    calcDirKind e f | PRODUCER | ConstC = InConstC

  calcDirKind e f | CONSUMER with (f)
    calcDirKind e f | CONSUMER | PC = InPC
    calcDirKind e f | CONSUMER | CP = OutCP
    calcDirKind e f | CONSUMER | PCCP = InOut
    calcDirKind e f | CONSUMER | ConstP = OutConstP
    calcDirKind e f | CONSUMER | ConstC = InConstC

||| The 'actual' direction of information flow through an interface
data Direction : (ty : DirectionTy)
              -> (endpoint : Endpoint)
              -> (flow : Flow)
              -> (prf  : DirectionKind endpoint flow ty)
              -> Type
  where
    IN    : Direction IsIn    endpoint flow kind
    OUT   : Direction IsOut   endpoint flow kind
    INOUT : Direction IsInOut endpoint flow kind

%hint
calcDirection : (endpoint : Endpoint)
             -> (flow     : Flow)
             -> Direction (calcDirTy endpoint flow) endpoint flow (calcDirKind endpoint flow)
calcDirection endpoint flow with (calcDirKind endpoint flow)
  calcDirection CONSUMER PC | InPC = IN
  calcDirection PRODUCER PC | OutPC = OUT
  calcDirection PRODUCER CP | InCP = IN
  calcDirection CONSUMER CP | OutCP = OUT
  calcDirection endpoint PCCP | InOut = INOUT
  calcDirection endpoint ConstP | OutConstP = OUT
  calcDirection endpoint ConstC | InConstC = IN

namespace Calculated
     Direction : (endpoint : Endpoint)
              -> (flow : Flow)
              -> Type
     Direction endpoint flow = Direction.Direction (calcDirTy endpoint flow) endpoint flow (calcDirKind endpoint flow)
-- --------------------------------------------------------------------- [ EOF ]

max_stars_repo_name: border-patrol/cordial

max_issues_repo_name: border-patrol/cordial

max_forks_repo_name: border-patrol/cordial


text:
module Logic.Basic

%access public
%default total

infixl 2 <=>
infixl 2 <-->

data (<=>) : (a : Type) -> (b : Type) -> Type where
   (<-->) : (a -> b) -> (b -> a) -> a <=> b

-- 等値の対称性
eq_sym : (a <=> b) -> (b <=> a)
eq_sym (f <--> g) = (g <--> f)

-- 等値性から射を導出..ってか取り出してるだけ
--   TODO:この演算子使い辛くね？
infixl 5 ->>
infixl 5 <<-
(->>): (a <=> b) -> a -> b
(->>) (f <--> _) = f

(<<-) : (a <=> b) -> b -> a
(<<-) (_ <--> g) = g

-- 三段論法
syllogism : (a -> b) -> (b -> c) -> a -> c
syllogism f g = g . f

-- 三段同値
syllogism_eq : a <=> b -> b <=> c -> a <=> c
syllogism_eq (f <--> f') (g <--> g') = (g . f) <--> (f' . g')

-- トートロジー同値
tautology_eq : a <=> a
tautology_eq = id <--> id

namespace and
  infixl 5 /\
  (/\) : Type -> Type -> Type
  (/\) a b = (a,b)

  associative_law : (a /\ b) /\ c <=> a /\ (b /\ c)
  associative_law = (\((a,b),c) => (a,(b,c))) <--> (\(a,(b,c)) => ((a,b),c))

  commulative_law : a /\ b -> b /\ a
  commulative_law (a, b) = (b, a)

  idempotence_and : a /\ a -> a
  idempotence_and (a,a) = a

  -- assoc : (a /\ b) /\ c = a /\ (b /\ c)
  -- assoc = ?assoc

namespace or
  infixl 5 \/
  (\/) : Type -> Type -> Type
  (\/) a b = Either a b

  associative_law_1 : ((a \/ b) \/ c) -> (a \/ (b \/ c))
  associative_law_1 (Right c) = Right $ Right c
  associative_law_1 (Left (Left a)) = Left a
  associative_law_1 (Left (Right b)) = Right (Left b)

  associative_law_2 : (a \/ (b \/ c)) -> ((a \/ b) \/ c)
  associative_law_2 (Left a) = Left $ Left a
  associative_law_2 (Right (Left b)) = Left $ Right b
  associative_law_2 (Right (Right c)) = Right c

  associative_law : ((a \/ b) \/ c) <=> (a \/ (b \/ c))
  associative_law = associative_law_1 <--> associative_law_2

  commulative_law : a \/ b -> b \/ a  -- TODO: 片方変換できれば自動的に等値が導けるケース
  commulative_law x = either x Right Left

  idempotence_or : a \/ a -> a
  idempotence_or x = either x id id

absorption_law_1 : (a /\ b) \/ a -> a
absorption_law_1 (Left (a,b)) = a
absorption_law_1 (Right a) = a

absorption_law_2 : (a \/ b) /\ a -> a
absorption_law_2 (_, a) = a

partition_law : a /\ (b \/ c) <=> (a /\ b) \/ (a /\ c)
partition_law = l <--> r
  where
     l (a, (Left b)) = Left (a, b)
     l (a, (Right c)) = Right (a, c)
     r (Left (a,b)) = (a, Left b)
     r (Right (a,c)) = (a, Right c)

partition_law_1 : (b \/ c) /\ a <=> (a /\ b) \/ (a /\ c)
--partition_law_1 = let (f <--> g) = partition_law
--                   in (f . and.commulative_law) <--> (and.commulative_law . g)

dm_nor : Not (a \/ b) <=> (Not a) /\ (Not b)
dm_nand : Not (a /\ b) <=> (Not a) \/ (Not b)

max_stars_repo_name: seagull-kamome/idris-toy

max_issues_repo_name: seagull-kamome/idris-toy

max_forks_repo_name: seagull-kamome/idris-toy