text:
module Data.Matrix.ZZGaussianEliminationLemmas

import Control.Algebra
import Classes.Verified
import Control.Algebra.DiamondInstances
import Control.Algebra.VectorSpace -- definition of module

import Data.Matrix
import Data.Matrix.Algebraic -- module instances; from Idris 0.9.20
import Data.Matrix.AlgebraicVerified

import Data.Vect.Structural
import Data.Matrix.Structural

import Data.ZZ
import Control.Algebra.NumericInstances
import Control.Algebra.ZZVerifiedInstances
import Data.Matrix.ZZVerified

import Data.Matrix.ZZModuleSpan
import Data.Matrix.LinearCombinations

import Data.Matrix.RowEchelon
import Control.Algebra.ZZDivisors

import Data.Fin.FinOrdering
import Data.Fin.Structural

import Control.Isomorphism

%default total

{-
Table of Contents:

* The induction algorithm used to verify first-column elimination
* Nice things for elimination algorithms to talk about
* Preliminary arguments to (elimFirstCol)

---

Guide:

Structure of (elimFirstCol):

succImplWknStep_Qfunclemma => succImplWknStep_stepQfunc => succImplWknStep_unplumbed => succImplWknStep => foldedFully

(mkQfunc, foldedFully) => elimFirstCol (after some work)
-}

{-
The induction algorithm used to verify first-column elimination
-}

{-
BUG: Wrong type displayed given implicit argument in argument

Incorrect type displayed:

\a : Type => \p : ({m : Nat} -> Fin (S m) -> a -> Type) => p (weaken $ FZ {k=Z})
	: (a : Type) ->
	  Fin (S m) -> a -> Type ->
	  a -> Type

Correct type displayed:

\a : Type => \p : ((m : Nat) -> Fin (S m) -> a -> Type) => p 5 (weaken FZ)
	: (a : Type) ->
	  ((m : Nat) -> Fin (S m) -> a -> Type) ->
	  a -> Type

Note that these examples both actually have the correct type, they're just not displayed correctly.
-}

{-
Error discovered while implementing (foldAutoind).

---

It was found that if you replace the argument

> p : (m : Nat) -> Fin (S m) -> a -> Type

with one where (m) is implicit, and rewrite (foldAutoind) & dependencies accordingly, then one can't implement them, because composing (p) with weaken leads to a Universe Inconsistency error, which doesn't appear when the weakening is done in the REPL, only when the resulting proof is loaded in the module.

See (elimFirstCol-oldmaterial.idr) where (fai_regrwkn_chty) and (fai_regrwkn_chty2) are being implemented (for that file's (foldAutoind), (foldAutoind2) resp.) for details.

This differs from the error described in (ImplicitArgsError), in that the values of (p) are irrelevant in creating this Universe Inconsistency error, whereas the one in (ImplicitArgsError) would arise from the values of (p) having implicit arguments of their own.
-}

fai_regrwkn : ( p : (m : Nat) -> Fin (S m) -> a -> Type )
	-> ( (i : Fin (S predn))
		-> ( w : a ** p _ (FS i) w )
		-> ( w' : a ** p _ (weaken i) w' ) )
	-> (i : Fin predn)
	-> ( w : a ** ((p _) . weaken) (FS i) w )
	-> ( w' : a ** ((p _) . weaken) (weaken i) w' )
-- can't be written as `(fn . weaken) i`, nor can `i` be dropped as an argument.
fai_regrwkn p fn i = fn (weaken i)

||| A vector fold over suppressed indices
|||
||| Extends one witness for some predicate
|||
||| p : (m : Nat) -> Fin (S m) -> a -> Type
|||
||| to a (Vect) of them.
|||
||| Best used with those (p) which are trivial for (last) and some (a).
foldAutoind : ( p : (m : Nat) -> Fin (S m) -> a -> Type )
	-> ( (i : Fin predn)
		-> ( w : a ** p _ (FS i) w )
		-> ( w' : a ** p _ (weaken i) w' ) )
	-> ( v : a ** p _ (last {n=predn}) v )
	-> ( xs : Vect (S predn) a ** (i : Fin (S predn)) -> p _ i (index i xs) )
foldAutoind {predn=Z} p regr (v ** pv) = ( [v] ** \i => rewrite sym (the (FZ = i) $ sym $ FinSZAreFZ i) in pv )
foldAutoind {predn=S prededn} p regr (v ** pv) with (regr (last {n=prededn}) (v ** pv))
	| (v' ** pv') with ( foldAutoind {predn=prededn} (\mu => (p $ S mu) . weaken) (fai_regrwkn p regr) (v' ** pv') )
		| (xs ** fn) = ?faiNew
		-- | ( xs ** fn ) = ( xs++[v] ** _ )

faiNew = proof
  intros
  exact (appendedSingletonAsSuccVect xs v ** _)
  intro i
  claim ifLastThenProved (i=last) -> p (S prededn) i (index i $ appendedSingletonAsSuccVect xs v)
  unfocus
  claim ifWeakenedThenProved (j : Fin (S prededn) ** i = weaken j) -> p (S prededn) i (index i $ appendedSingletonAsSuccVect xs v)
  unfocus
  let iAsEither = splitFinS i
  exact either ifWeakenedThenProved ifLastThenProved iAsEither
  intro prIsLast
  rewrite sym prIsLast
  exact rewrite (lastInd {xs=xs} {v=v}) in pv
  intro parIsWeakened
  let prIsWeakened = getProof parIsWeakened
  rewrite sym prIsWeakened
  exact rewrite (weakenedInd {xs=xs} {v=v} {k=getWitness parIsWeakened}) in fn (getWitness parIsWeakened)

fai2_regrwkn : (a : Nat -> Type)
	-> ( p : (m : Nat) -> Fin (S m) -> (a m) -> Type )
	-> ( (i : Fin (S predn))
		-> ( w : a (S predn) ** p _ (FS i) w )
		-> ( w' : a (S predn) ** p _ (weaken i) w' ) )
	-> (i : Fin predn)
	-> ( w  : (a . S) predn ** ((p _) . weaken) (FS i) w )
	-> ( w' : (a . S) predn ** ((p _) . weaken) (weaken i) w' )
-- can't be written as `(fn . weaken) i`, nor can `i` be dropped as an argument.
fai2_regrwkn a p fn i = fn (weaken i)

||| A vector fold over suppressed indices
|||
||| Same strength of result as foldAutoind, but where the predicate is of the form
|||
||| p : (m : Nat) -> Fin (S m) -> (a m) -> Type
|||
||| for when it isn't naturally expressed or proved without affecting
||| the type (a _) of the witnesses dealt with by this process.
{-
(a : Nat -> Type) is not made implicit because Idris isn't likely to deduce it and will likely spend a long time trying anyway.
-}
foldAutoind2 : ( a : Nat -> Type )
	-> ( p : (m : Nat) -> Fin (S m) -> (a m) -> Type )
	-> ( (i : Fin predn)
		-> ( w : a predn ** p _ (FS i) w )
		-> ( w' : a predn ** p _ (weaken i) w' ) )
	-> ( v : a predn ** p _ (last {n=predn}) v )
	-> ( xs : Vect (S predn) (a predn) ** (i : Fin (S predn)) -> p _ i (index i xs) )
foldAutoind2 {predn=Z} _ p regr (v ** pv) = ( [v] ** \i => rewrite sym (the (FZ = i) $ sym $ FinSZAreFZ i) in pv )
foldAutoind2 {predn=S prededn} natToA p regr (v ** pv) with (regr (last {n=prededn}) (v ** pv))
	| (v' ** pv') with ( foldAutoind2 {predn=prededn} (natToA . S) (\mu => (p $ S mu) . weaken) (fai2_regrwkn natToA p regr) (v' ** pv') )
		| (xs ** fn) = ?faiNew2
		-- | ( xs ** fn ) = ( xs++[v] ** _ )

-- Identical to the proof of faiNew
faiNew2 = proof
  intros
  exact (appendedSingletonAsSuccVect xs v ** _)
  intro i
  claim ifLastThenProved (i=last) -> p (S prededn) i (index i $ appendedSingletonAsSuccVect xs v)
  unfocus
  claim ifWeakenedThenProved (j : Fin (S prededn) ** i = weaken j) -> p (S prededn) i (index i $ appendedSingletonAsSuccVect xs v)
  unfocus
  let iAsEither = splitFinS i
  exact either ifWeakenedThenProved ifLastThenProved iAsEither
  intro prIsLast
  rewrite sym prIsLast
  exact rewrite (lastInd {xs=xs} {v=v}) in pv
  intro parIsWeakened
  let prIsWeakened = getProof parIsWeakened
  rewrite sym prIsWeakened
  exact rewrite (weakenedInd {xs=xs} {v=v} {k=getWitness parIsWeakened}) in fn (getWitness parIsWeakened)

{-
Nice things for elimination algorithms to talk about
-}

succImplWknProp :
	(omat : Matrix predonnom (S predm) ZZ)
	-> (senior : Vect (S predm) ZZ)
	-> (nu : Nat)
	-> (fi : Fin (S nu))
	-> Matrix (S nu) (S predm) ZZ
	-> Type
succImplWknProp omat senior nu fi tmat =
	( senior = head tmat
	, downAndNotRightOfEntryImpliesZ tmat fi FZ
	, tmat `bispanslz` (senior::omat) )

succImplWknPropSec2 :
	(nu : Nat)
	-> (fi : Fin (S nu))
	-> Matrix (S nu) (S predm) ZZ
	-> Type
succImplWknPropSec2 nu fi tmat = downAndNotRightOfEntryImpliesZ tmat fi FZ

danrzLast : (omat : Matrix (S predn) (S predm) ZZ)
	-> succImplWknPropSec2 predn (last {n=predn}) omat
danrzLast omat = (\i => \j => void . notSNatLastLTEAnything)

{-
Preliminary arguments to (elimFirstCol)
-}

{- (elimFirstCol) lemmas parameters -}
parameters (predm : Nat) {

{- (mkQFunc) parameters -}
parameters (predn : Nat) {

mkQFunc : (v : Vect (S predn) ZZ)
	-> (xs : Matrix (S predn) (S predm) ZZ)
	-> ( ( i : Fin (S predn) )
		-> (index i $ getCol FZ xs) `quotientOverZZ` (v <:> (getCol FZ xs)) )
	-> ( ( i : Fin (S $ S predn) )
		-> (indices i FZ $ (v<\>xs)::xs) `quotientOverZZ` (head $ v<\>xs) )
mkQFunc v xs fn FZ = quotientOverZZreflFromEq $ indexFZIsheadValued {xs=v<\>xs}
mkQFunc v xs fn (FS k) =
	( (quotientOverZZreflFromEq $ sym $ indexMapChariz {k=k} {f=index FZ} {xs=xs})
		`quotientOverZZtrans` fn k )
	`quotientOverZZtrans`
	( quotientOverZZreflFromEq $ sym $ headVecMatMultChariz {v=v} {xs=xs} )

} {- (mkQFunc) parameters -}

{- succImplWknStep lemmas parameters -}
parameters (
	mat : Matrix _ (S predm) ZZ
	, predn : Nat
	, senior : Vect (S predm) ZZ
	, srQfunc : ( i : Fin _ )
		-> (indices i FZ (senior::mat)) `quotientOverZZ` (head senior)
	, imat : Matrix (S (S predn)) (S predm) ZZ
	) {

succImplWknStep_Qfunclemma :
	( z : Matrix _ _ ZZ )
	-> ( quotchariz :
		( k : Fin _ )
		-> ( LinearCombinations.monoidsum
			$ zipWith (<#>) (index k z) (senior::mat)
			= index k imat ) )
	-> ( j : Fin _ ) -> (indices j FZ imat) `quotientOverZZ` (head senior)
succImplWknStep_Qfunclemma z quotchariz j
	= (getWitness lemma **
		trans (getProof lemma)
		$ trans (cong {f=head} $ quotchariz j)
		$ sym $ indexFZIsheadValued {xs=index j imat})
	where
	lemma : (head $ monoidsum $ zipWith (<#>) (index j z) (senior::mat))
		`quotientOverZZ` (head senior)
	lemma = linearComboQuotientRelation_corrollary senior mat (index j z)
		(\i => quotientOverZZtrans
			(quotientOverZZreflFromEq $ sym indexFZIsheadValued)
			$ srQfunc i)

succImplWknStep_stepQfunc :
	( reprolem : senior::mat `spanslz` imat )
	-> ( j : Fin _ ) -> (indices j FZ imat) `quotientOverZZ` (head senior)
succImplWknStep_stepQfunc reprolem = succImplWknStep_Qfunclemma (getWitness reprolem)
	(\k => trans (sym indexMapChariz)
		$ cong {f=index k} $ getProof reprolem)

{-
COMMENT - (succImplWknStep_unplumbed) PARAMETERS ERROR

Tried to use parameters to treat the assumptions to (succImplWknStep_unplumbed) as
both a (succImplWknProp) value and a tuple (as it's defined to be). The parameters
in the tuple can't be unpacked from it, and tupled definitions won't work neither
as a tupled parameter nor a tuple set equal to the (succImplWknProp) parameter.

Got error:

"
When checking left hand side of ZZGaussianEliminationRedo.seniorIsImatHead:
Can't match on seniorIsImatHead _
                                predm
                                mat
                                predn
                                senior
                                srQfunc
                                imat
                                predm
                                fi
                                prfTuple
"

Same error for others.

Attempted code:

> {- (succImplWknStep_unplumbed) & lemmas parameters -}
> parameters (
> 	fi : Fin (S predn)
> 	, prfTuple : succImplWknProp mat senior (S predn) (FS fi) imat
> 	) {

> seniorIsImatHead : ( senior = head imat )
> seniorIsImatHead = fst prfTuple

> imatDANRZ : downAndNotRightOfEntryImpliesZ imat (FS fi) FZ
> imatDANRZ = let (_,a,_,_) = prfTuple in a

> imatSpansOrig : imat `spanslz` (senior::mat)
> imatSpansOrig with ( prfTuple )
> 	| (_,_,a,_) = a

> origSpansImat : (senior::mat) `spanslz` imat
> origSpansImat with ( prfTuple )
> 	| (_,_,_,a) = a

> } {- (succImplWknStep_unplumbed) & lemmas parameters -}

Still similar errors here:

> {- (succImplWknStep_unplumbed) & lemmas parameters -}
> parameters (
> 	fi : Fin (S predn)
> 	, seniorIsImatHead : ( senior = head imat )
> 	, imatDANRZ : downAndNotRightOfEntryImpliesZ imat (FS fi) FZ
> 	, imatSpansOrig : imat `spanslz` (senior::mat)
> 	, origSpansImat : (senior::mat) `spanslz` imat
> 	) {

> succImplWknStep_stepQfunc' : ( j : Fin _ )
> 	-> (indices j FZ imat) `quotientOverZZ` (head senior)
> succImplWknStep_stepQfunc' = succImplWknStep_stepQfunc origSpansImat

And trying to make sure we use all the same implicit parameters we supplied to the
original definition, we get a different error, saying the (predm) in the type of
(imat) doesn't match the (predm) we're passing (downAndNotRightOfEntryImpliesZ):

> {- (succImplWknStep_unplumbed) & lemmas parameters -}
> parameters (
> 	fi : Fin (S predn)
> 	, seniorIsImatHead : ( senior = head imat )
> 	, imatDANRZ : downAndNotRightOfEntryImpliesZ {n=S $ S predn} {m=S predm} imat (FS fi) (FZ {k=predm})
> 	, imatSpansOrig : imat `spanslz` (senior::mat)
> 	, origSpansImat : (senior::mat) `spanslz` imat
> 	) {

> succImplWknStep_stepQfunc' : ( j : Fin _ )
> 	-> (indices j FZ imat) `quotientOverZZ` (head senior)

> } {- (succImplWknStep_unplumbed) & lemmas parameters -}

Finally, we see that the error that (predm) fails to match with itself
occurs when an extra parameter block is introduced to hold anything further,
whether or not it has any dependence on (predm).

In particular, if (fi : Fin (S predn)) from below is made the sole parameter to
the new block, this causes the error.

END COMMENT - (succImplWknStep_unplumbed) PARAMETERS ERROR

-}

{-
For the proof of (downAndNotRightOfEntryImpliesZ) for the output of the below function in human, consider the modification

> updateAt (weaken fi) (<-> (Sigma.getWitness $ fn (weaken fi)) <#> senior) imat

to imat. According to (fn $ weaken fi), we will get a value (imat') such that

> indices (weaken fi) FZ imat'
	= head $ index (weaken fi) imat <-> (Sigma.getWitness $ fn (weaken fi)) <#> senior
	= head (index (weaken fi) imat)
		<-> head ( (Sigma.getWitness $ fn (weaken fi)) <#> senior )
	= head (index (weaken fi) imat)
		<-> (Sigma.getWitness $ fn (weaken fi)) <.> (head senior)
	=	(by getProof $ fn (weaken fi))
	head (index (weaken fi) imat) <-> head (index (weaken fi) imat)
	=	(by groupInverseIsInverseL $ head (index (weaken fi) imat))
	Pos Z
-}
-- Including proof the head is equal to senior just makes this step easier.

succImplWknStep_unplumbed :
	(fi : Fin (S predn))
	-> succImplWknProp mat senior (S predn) (FS fi) imat
	-> ( imat' : Matrix (S (S predn)) (S predm) ZZ **
		succImplWknProp mat senior (S predn) (weaken fi) imat' )
succImplWknStep_unplumbed fi ( seniorIsImatHead, imatDANRZ, imatSpansOrig, origSpansImat )
	= (jmat ** ( seniorIsJmatHead, jmatDANRZ, jmatBispansOrig ) )
	where
		fn : ( j : Fin _ ) -> (indices j FZ imat) `quotientOverZZ` (head senior)
		fn = succImplWknStep_stepQfunc origSpansImat
		jmat : Matrix (S (S predn)) (S predm) ZZ
		jmat = updateAt (FS fi)
			(<-> (Sigma.getWitness $ fn (FS fi)) <#> senior)
			imat
		seniorIsJmatHead : senior = head jmat
		seniorIsJmatHead = trans seniorIsImatHead
			$ sym updateAtSuccRowVanishesUnderHead
		primatzAtWknFi : indices (FS fi) FZ jmat = Pos Z
		primatzAtWknFi =
			trans (cong {f=index FZ}
				$ indexUpdateAtChariz {xs=imat} {i=FS fi}
				{f=(<-> (Sigma.getWitness $ fn (FS fi)) <#> senior)})
			$ trans (zipWithEntryChariz {i=FZ {k=predm}} {m=(<+>)}
				{x=index (FS fi) imat}
				{y=inverse $ (Sigma.getWitness $ fn (FS fi)) <#> senior})
			$ trans (cong {f=plusZ $ indices (FS fi) FZ imat}
				$ trans (indexCompatInverse
					((<#>) (Sigma.getWitness $ fn $ FS fi) senior)
					FZ)
				(cong {f=inverse} $ indexCompatScaling
					(Sigma.getWitness $ fn $ FS fi)
					senior
					FZ))
			$ trans (cong {f=(<->) $ indices (FS fi) FZ imat}
				$ trans (cong {f=((Sigma.getWitness $ fn $ FS fi)<.>)}
					$ indexFZIsheadValued {xs=senior})
				$ getProof $ fn $ FS fi)
			$ groupInverseIsInverseL $ indices (FS fi) FZ imat
		jmatDANRZ : downAndNotRightOfEntryImpliesZ jmat (weaken fi) FZ
		jmatDANRZ = weakenDownAndNotRightFZ {prednel=fi} {mat=jmat}
			(afterUpdateAtCurStillDownAndNotRight
				{mat=imat} {prednel=fi} {mel=FZ}
				{f=(<-> (Sigma.getWitness $ fn (FS fi)) <#> senior)}
				imatDANRZ)
			primatzAtWknFi
		missingstep : head imat = (Algebra.unity::Algebra.neutral) <\> deleteRow (FS fi) imat
		missingstep = sym $ trans
			( timesVectMatAsLinearCombo (Algebra.unity::Algebra.neutral) $ deleteRow (FS fi) imat )
			$ trans ( cong {f=\m => monoidsum {t=Vect _} $ zipWith ((<#>) {a=ZZ}) (Algebra.unity::Algebra.neutral) m}
				$ headtails $ deleteRow (FS fi) imat )
			$ trans ( cong {f=monoidsum {a=Vect _ ZZ}}
				$ vecHeadtailsEq (zzVecScalarUnityIsUnity $ head
					$ deleteRow (FS fi) imat) Refl )
			$ trans monoidrec2D
			$ trans ( cong {f=((head $ deleteRow (FS fi) imat)<+>)}
				$ trans (sym
					$ timesVectMatAsLinearCombo Algebra.neutral
					$ tail $ deleteRow (FS fi) imat)
				$ zzVecNeutralIsVecMatMultZero
					(tail $ deleteRow (FS fi) imat) )
			$ trans ( zzVecNeutralIsNeutralL $ head $ deleteRow (FS fi) imat )
			$ deleteSuccRowVanishesUnderHead {k=fi} {xs=imat}
		jmatBispansOrig : jmat `bispanslz` (senior::mat)
		jmatBispansOrig =
			bispanslztrans
				( bispanslzreflFromEq {xs=jmat}
				$ cong {f=\z => updateAt (FS fi) (<-> z) imat}
				$ trans ( cong {f=((<#>) {a=ZZ} _)}
					$ trans seniorIsImatHead $ missingstep )
				$ sym
				$ vectMatLScalingCompatibility
					{z=Sigma.getWitness $ fn $ FS fi}
					{la=Algebra.unity::Algebra.neutral}
					{rs=deleteRow (FS fi) imat} )
			$ bispanslztrans
				( bispanslzSubtractiveExchangeAt (FS fi) {xs=imat}
					{z=(Sigma.getWitness $ fn (FS fi))<#>(Algebra.unity::Algebra.neutral)} )
			$ (imatSpansOrig, origSpansImat)

} {- succImplWknStep lemmas parameters -}

{- (succImplWknStep) parameters -}
parameters (
	mat : Matrix _ (S predm) ZZ
	, predn : Nat
	, senior : Vect (S predm) ZZ
	, srQfunc : ( i : Fin _ )
		-> (indices i FZ (senior::mat)) `quotientOverZZ` (head senior)
	) {

{-
Unexpectedly, (succImplWknStep_unplumbed) has to be given (predm) as an argument,
even though it's from the same (parameters) block in which (predm) was declared.

That might explain part of the earlier troubles with parametrizing
(succImplWknStep_unplumbed), if the parameters required (predm) or other implicit
arguments, but they'd passed out of scope from their declaration coming after the
closing of a nested parameter block that also references them.
-}
succImplWknStep :
	(fi : Fin (S predn))
	-> ( imat : Matrix (S (S predn)) (S predm) ZZ
		** succImplWknProp mat senior (S predn) (FS fi) imat )
	-> ( imat' : Matrix (S (S predn)) (S predm) ZZ
		** succImplWknProp mat senior (S predn) (weaken fi) imat' )
succImplWknStep fi imatAndPrs = succImplWknStep_unplumbed predm mat predn senior srQfunc
		(getWitness imatAndPrs)
		fi
		(getProof imatAndPrs)

} {- (succImplWknStep) parameters -}

{- (foldedFully) parameters -}
parameters (
	predn : Nat
	, mat : Matrix (S predn) (S predm) ZZ
	) {

foldedFully :
	(v : Vect (S predn) ZZ)
	-> ( vmatQfunc :
		( i : Fin _ )
		-> (indices i FZ ((v <\> mat)::mat)) `quotientOverZZ` (head $ v <\> mat) )
	-> ( mats : Vect (S (S predn)) $ Matrix (S (S predn)) (S predm) ZZ
		** (i : Fin (S (S predn)))
		-> succImplWknProp mat (v<\>mat) (S predn) i (index i mats) )
foldedFully v vmatQfunc = foldAutoind2 {predn=S predn} (\ne => Matrix (S ne) (S predm) ZZ)
	(succImplWknProp mat (v <\> mat))
	(succImplWknStep predm mat predn (v <\> mat) vmatQfunc)
	( (v<\>mat)::mat ** (Refl, danrzLast ((v <\> mat)::mat), bispanslzrefl) )

} {- (foldedFully) parameters -}

} {- (elimFirstCol) lemmas parameters -}


text:
module Nandb

nandb : (a : Bool) -> (b : Bool) -> Bool
nandb True True = False
nandb a b = True

tn1 : (nandb True True) = False
tn1 = Refl
tn2 : (nandb True False) = True
tn2 = Refl
tn3 : (nandb False False) = True
tn3 = Refl
tn4 : (nandb False True) = True
tn4 = Refl

ext: idr


text:
module CommonTestingStuff

import public Data.SnocList

import public Control.Monad.Coop
import public Control.Monad.State
import public Control.Monad.Writer

%default total

--- Testing-purpose instances ---

export
Show Time where
  show t = show t.asMillis

export
Show FinDuration where
  show d = show d.asMillis

--- Printing stuff ---

public export
interface Monad m => PrintString m where
  printString : String -> m Unit

export
PrintString IO where
  printString = putStrLn

export
printTime : PrintString io => Timed io => (offset : Time) -> String -> io Unit
printTime offset s = printString "[time: \{show {ty=FinDuration} $ !currentTime - offset}] \{s}"

--- Testing-specific stuff ---

export
(===) : (Eq a, Show a, HasIO io) => a -> a -> io ()
x === y = if x == y
            then putStrLn "- [ok]"
            else putStrLn "- [VIOLATION] got \{show x} but expected \{show y}"

--- Monadic stuff ---

export
for : Nat -> Monad m => m a -> m ()
for Z     _ = pure ()
for (S n) a = do ignore a; for n a

export covering
forever : Monad m => m a -> m b
forever x = do ignore x; forever x

--- `Writer`-related stuff ---

export
Monad m => PrintString (WriterT (SnocList String) m) where
  printString = tell . pure

export
Timed m => Monad m => Timed (WriterT w m) where
  currentTime = lift currentTime

export
CanSleep m => CanSleep (WriterT w m) where
  sleepFor  = lift . sleepFor
  sleepTill = lift . sleepTill

export covering
execW : (forall m. PrintString m => CanSleep m => Coop m Unit) -> SnocList String
execW c = execWriter $ evalStateT 0.seconds $ runCoop c {m=StateT Time _} where

  Monad m => Timed (StateT Time m) where
    currentTime = get

  Monad m => CanSleep (StateT Time m) where
    sleepFor d = modify (+d)

  PrintString m => PrintString (StateT s m) where
    printString = lift . printString

--- Liftings for `Coop` ---

export
MonadState st m => MonadState st (Coop m) where
  get = lift get
  put = lift . put

export
MonadWriter w m => MonadWriter w (Coop m) where
  writer = lift . writer
  tell   = lift . tell
  listen = (>>= lift . listen . pure)
  pass   = (>>= lift . pass   . pure)

export
PrintString m => PrintString (Coop m) where
  printString = lift . printString


text:
module Language.Elab.Deriving.Eq

-- Public: Things here we actually use in deriving Eq need to be re-exported to
-- be available at the deriving use-site. A little odd but that's how it is.
-- Otherwise you get extremely vague "Can't reify as X" errors and chances are
-- you don't have an FC to track it down.

import public Language.Elab.Syntax
import public Language.Elab.Types

import public Util
import public Language.Elab.Deriving.Util

import public Language.Reflection

{-
interesting case, happens to work for Show already!
data TagField : Type where
  TF : Eq a => Show a => (name : String) -> (value : a) -> TagField
-}

-- A regular instance might look like (Eq a, Eq b, Eq c) => ...
-- This pairing isn't actually neccesary, it's just notational convenience and
-- we don't really have a reason to emulate it.
-- Eq a => Eq b => ...  is just as valid as (Eq a, Eq b) => ...
-- It also can result in clearer errors.
addEqAutoImps : List String -> TTImp -> TTImp
addEqAutoImps xs retty
  = foldr (\arg,tt => `(Eq ~(iBindVar arg) => ~(tt))) retty xs

-- I want better names here, including better index names
-- e.g we have this now
{-
Language.Elab.Deriving.Eq.eqImplFoo6'Fun : Eq arg6281 => Eq arg6282
  => Eq arg6283 => Foo6' arg6281 arg6282 arg6283 arg6284
    -> Foo6' arg6281 arg6282 arg6283 arg6284 -> Bool
-}

||| e.g. (==) : Foo a b -> Foo a b -> Bool
eqClaim : (opname : Name) -> TypeInfo -> Visibility -> Elab Decl
eqClaim op tyinfo vis = do
  let conargs = pullExplicits tyinfo
      varnames = map (show . name) conargs
      params = map (extractNameStr . name) $ filter (not . isIndex) conargs
      tysig = `(~(tyinfo.type) -> ~(tyinfo.type) -> Bool)
  logMsg "eqClaim" 1 $ ("auto params: ") ++ show params
  -- NB: I can't think of a reason not to Inline here
  pure $ iClaim MW vis [Inline] (mkTy op (addEqAutoImps params tysig))

eqCon : (opname : Name) -> Constructor -> Elab Clause
eqCon op con = do
    let vars = filter (isExplicitPi . piInfo) con.args
        pats = makePatNames vars infVars
        lhs = iVar op `iApp` (makePat con.name (map (map fst) pats))
                      `iApp` (makePat con.name (map (map snd) pats))
        rhs = makeRhs (catMaybes pats)
    logTerm "eqconlhs" 1 "" lhs
    logTerm "eqconrhs" 1 "" rhs
    pure $ patClause lhs rhs
  where
    -- Make our pat names, we use Just to flag the vars we want to use, we don't
    -- compare indices since they're vacuously the same for an Eq interface.
    makePatNames : List ArgInfo
               -> Stream String -> (List (Maybe (Name,Name)))
    makePatNames [] vs = []
    makePatNames (a :: as) (v :: vs)
      =
       let xs = makePatNames as vs
           basicname = UN v
       in if isUse0 a.count || a.isIndex
          then Nothing :: xs
          else Just ((mapName (++ "_1") basicname), (mapName (++ "_2") basicname)) :: xs

    -- The lhs of our function, fields we don't want to use are replaced with _
    makePat : (con : Name) -> (vars : List (Maybe Name)) -> TTImp
    makePat con vars = foldl
      (\tt,v => `(~(tt) ~(maybe implicit' bindNameVar v))) (iVar con) vars

    -- A little wordy here, it's set up this way instead of a fold to avoid an
    -- extra True when building up our && chain. There's no reason to make the
    -- user repeat work every time they use their derived implementation.
    makeRhs : List (Name,Name) -> TTImp
    makeRhs [] = `(True)
    makeRhs [(x,y)] = `( ~(iVar x) == ~(iVar y) )
    makeRhs ((x,y) :: xs) = `( ~(iVar x) == ~(iVar y) && ~(makeRhs xs) )

||| The record that idris would make for you when you write an implementation.
eqObject : (decname : Name) -> (funname : Name) -> TypeInfo
          -> Visibility -> Elab (Decl, Decl)
eqObject decname eqfun tyinfo vis = do
  (qname,_) <- lookupName `{{Eq}}
  [NS _ (DN _ eqcon)] <- getCons qname
    | _ => fail "eqObject: error during Eq constructor lookup"
  let conargs = pullExplicits tyinfo
      varnames = map (show . name) conargs
      varnames' = map (show . name) (filter (not . isIndex) conargs)
      retty = `( Eq ~(appTyCon (map (show . name) conargs)  tyinfo.name))
      tysig = addEqAutoImps varnames' retty
      claim = iClaim MW vis [Hint True] (mkTy decname tysig)
      neqfun = `(\x,y => not (x == y))
      rhs = `( ~(iVar eqcon) ~(iVar eqfun) ~(neqfun))
      body = iDef decname [(patClause (iVar decname) rhs)]
  pure $ (claim,body)

export
||| Usage: %runElab deriveEq Export `{{Foo}}
||| Currently, this adds eqImplFoo and eqImpltFooFun to the module namespace.
||| This is likely to change in the future to only have eqImplFoo being added
||| to the namespace.
deriveEq : Visibility -> Name -> Elab ()
deriveEq vis eqname = do
    (qname,_) <- lookupName eqname -- get the qualified name of our type
    -- create human readable names for our instance components
    let decn = mapName (\d => "eqImpl" ++ d) eqname
        funn = mapName (\d => "eqImpl" ++ d ++ "Fun") eqname
    -- Build general info about the type we're deriving (e.g. Foo) that we want
    -- to keep around.
    tyinfo <- makeTypeInfo qname
    -- The components of our eq-ing function
    funclaim <- eqClaim funn tyinfo Private -- NB private
    funclauses <- traverse (eqCon funn) tyinfo.cons

    -- Our function's complete definition
    let catchall = patClause `(~(iVar funn) ~implicit' ~implicit') `(False)
        fundecl = iDef funn (funclauses ++ [catchall])

    -- The actual eqImplFoo : Eq Foo record.
    (objclaim,objclause) <- eqObject decn funn tyinfo vis

    -- Declare our things into the namespace
    -- Both claims first, otherwise we won't find our own Eq in fundecl
    declare [funclaim, objclaim]
    declare [fundecl, objclause]


text:
module Main

import Data.String

import Test.Golden

atDir : (poolName : String) -> (dir : String) -> IO TestPool
atDir poolName dir = testsInDir dir (not . isPrefixOf "_") poolName [] Nothing

main : IO ()
main = runner
  [ !( "Sequential execution"                           `atDir` "coop-monad/seq"      )
  , !( "Concurrent execution with result merging"       `atDir` "coop-monad/zip"      )
  , !( "Concurrent execution with race"                 `atDir` "coop-monad/race"     )
  , !( "Spawning"                                       `atDir` "coop-monad/spawn"    )
  , !( "Empty computation"                              `atDir` "coop-monad/empty"    )
  ]


text:
{- This file demonstrates the canonical example of dependent types,
 - vectors (implemented as lists) with their lengths encoded at the type level.
 - First note that Idris has built-in natural numbers, defined as follows:

 data Nat = Z | S Nat

 - A Nat is either 0 (Z) or the successor of a Nat, (i.e. N + 1) -}

data Vect : Nat -> Type -> Type where
  Nil  : Vect Z elem
  (::) : (x : elem) -> (xs : Vect len elem) -> Vect (S len) elem

-- Hints for interactive editing
%name Vect xs,ys,zs,ws

{- Let's break this down. We have a type constructor
 -   Vect : Nat -> Type -> Type
 - In Idris, since types are values, type constructors are just functions!
 - This type constructor takes a value of type `Nat` and a value of type `Type`
 - and constructs the type (Vect N Type) of a length N vector of type Type.

 - We also have two term constructors, `Nil` and `(::)`.
 -   Nil : Vect z elem
 - constructs a vector of length `0` with element type `elem` for any type `elem`.
 -   (::) : (x : elem) -> (xs : Vect len elem) -> Vect (S len) elem
 - takes an element and a Vector of length `len`, and returns a vector of
 - length `len + 1`. Note that it does so by construction, i.e. this is where
 - we *define* how the length of a vector is calculated. -}

v1 : Vect 0 Int
v1 = [] -- [] is a built-in synonym for Nil

v2 : Vect 3 Int
v2 = [1,2,3] -- list syntax is overloaded for any type with constructors Nil, ::

-- The following code will throw a compile-time error
--   v3 : Vect 4 Int
--   v3 : [1,2,3]

{- Crucial to the defintion above is the fact that we can use functions to
 - compute types. For example, `Vect (len + 1) elem` uses addition to compute
 - the resulting type. We can write functions whose output types are computed
 - from their input types.

 - Let us write an append function on vectors. -}

append : Vect n a -> Vect m a -> Vect (n + m) a
append xs ys = ?hole

{- Here `?hole` is a hole, which is a valid piece of syntax that Idris can assign
 - a type. In the Idris editor mode (see https://atom.io/packages/language-idris),
 - the shortcut Ctrl-Alt-t shows the type of the value under the cursor as well
 - as the types of all the available values in scope. On the hole above, this yields

 0 m : Nat
 0 a : Type
 0 n : Nat
   ys : Vect m a
   xs : Vect n a
-------------------------------------
hole : Vect (plus n m) a

 - Ctrl-Alt-c on a function argument case splits that argument. Doing so on `xs`:
 -}

append2 : Vect n a -> Vect m a -> Vect (n + m) a
append2 [] ys = ?base2       -- base case
append2 (x :: xs) ys = ?rec2 -- recursive case

{- Inspecting ?base2, we see

 0 m : Nat
 0 a : Type
   ys : Vect m a
 0 n : Nat
-------------------------------------
base2 : Vect m a

- We require a `Vect m a` and have a `Vect m a`, ys.

- Ctrl-Alt-s searches the types and values in scope for a solution to the program,
- i.e. a term with the type of the hole. Running serach on the two holes above
- automatically generates the following code. -}

append3 : Vect n a -> Vect m a -> Vect (n + m) a
append3 [] ys = ys
append3 (x :: xs) ys = x :: append3 xs ys

{- This is amazing! The compiler just discovered our code for us! Note that all
 - this does is replace our usual reasoning "see what fits the type and its
 - probably right," and will thus not always yield the correct program. However,
 - the extra expressivity of dependent types does often allow correct program
 - generation, just via a simple search.

 - Let us consider another example: -}

zipWith : (f : a -> b -> c) -> (xs : Vect n a) -> (ys : Vect n b) -> Vect n c
zipWith f xs ys = ?zipWith_rhs

{- Here, both input vectors are guarenteed to be the same length. This gives
 - the compiler a lot of useful information to help us write our program.
 - First, Ctrl-Alt-c to case split on `xs` yields the following: -}

zipWith2 : (f : a -> b -> c) -> (xs : Vect n a) -> (ys : Vect n b) -> Vect n c
zipWith2 f [] ys = ?zipWith2_rhs_1
zipWith2 f (x :: xs) ys = ?zipWith2_rhs_2

{- Subsequently case splitting again on ys in both the base
 - and recursive case only yields the one possibility for each, since in the
 - base case `ys` is guarenteed to be `[]` and in the recursive case `ys` is
 - guarenteed to be of the form `(y :: ys)`. -}

zipWith3 : (f : a -> b -> c) -> (xs : Vect n a) -> (ys : Vect n b) -> Vect n c
zipWith3 f [] [] = ?zipWith_base
zipWith3 f (x :: xs) (y :: ys) = ?zipWith_rec

{- Searching w/ Ctrl-Alt-s on the two holes above immediately yields the solution! -}

zipWith4 : (f : a -> b -> c) -> (xs : Vect n a) -> (ys : Vect n b) -> Vect n c
zipWith4 f [] [] = []
zipWith4 f (x :: xs) (y :: ys) = f x y :: zipWith4 f xs ys


text:
module Main

import Test.Golden

tests : TestPool
tests = MkTestPool "idv" [] Nothing
  [ "list", "select", "help"
  , "lsp-version-check"
  ]

main : IO ()
main = do
  runner [tests]

max_stars_repo_name: memoryruins/idv

max_issues_repo_name: memoryruins/idv

max_forks_repo_name: memoryruins/idv


text:
module TTImp.Elab.Case

import Core.CaseTree
import Core.Context
import Core.Context.Log
import Core.Core
import Core.Env
import Core.Metadata
import Core.Normalise
import Core.Unify
import Core.TT
import Core.Value

import TTImp.Elab.Check
import TTImp.Elab.Delayed
import TTImp.Elab.ImplicitBind
import TTImp.Elab.Utils
import TTImp.TTImp
import TTImp.Utils

import Data.List
import Data.Maybe
import Data.String
import Libraries.Data.NameMap

%default covering

export
changeVar : (old : Var vs) -> (new : Var vs) -> Term vs -> Term vs
changeVar (MkVar {i=x} old) (MkVar new) (Local fc r idx p)
    = if x == idx
         then Local fc r _ new
         else Local fc r _ p
changeVar old new (Meta fc nm i args)
    = Meta fc nm i (map (changeVar old new) args)
changeVar (MkVar old) (MkVar new) (Bind fc x b sc)
    = Bind fc x (assert_total (map (changeVar (MkVar old) (MkVar new)) b))
           (changeVar (MkVar (Later old)) (MkVar (Later new)) sc)
changeVar old new (App fc fn arg)
    = App fc (changeVar old new fn) (changeVar old new arg)
changeVar old new (As fc s nm p)
    = As fc s (changeVar old new nm) (changeVar old new p)
changeVar old new (TDelayed fc r p)
    = TDelayed fc r (changeVar old new p)
changeVar old new (TDelay fc r t p)
    = TDelay fc r (changeVar old new t) (changeVar old new p)
changeVar old new (TForce fc r p)
    = TForce fc r (changeVar old new p)
changeVar old new tm = tm

findLater : (x : Name) -> (newer : List Name) -> Var (newer ++ x :: older)
findLater x [] = MkVar First
findLater {older} x (_ :: xs)
    = let MkVar p = findLater {older} x xs in
          MkVar (Later p)

toRig1 : {idx : Nat} -> (0 p : IsVar nm idx vs) -> Env Term vs -> Env Term vs
toRig1 First (b :: bs)
    = if isErased (multiplicity b)
         then setMultiplicity b linear :: bs
         else b :: bs
toRig1 (Later p) (b :: bs) = b :: toRig1 p bs

toRig0 : {idx : Nat} -> (0 p : IsVar nm idx vs) -> Env Term vs -> Env Term vs
toRig0 First (b :: bs) = setMultiplicity b erased :: bs
toRig0 (Later p) (b :: bs) = b :: toRig0 p bs

-- When we abstract over the evironment, pi needs to be explicit
explicitPi : Env Term vs -> Env Term vs
explicitPi (Pi fc c _ ty :: env) = Pi fc c Explicit ty :: explicitPi env
explicitPi (b :: env) = b :: explicitPi env
explicitPi [] = []

allow : Maybe (Var vs) -> Env Term vs -> Env Term vs
allow Nothing env = env
allow (Just (MkVar p)) env = toRig1 p env

-- If the name is used elsewhere, update its multiplicity so it's
-- not required to be used in the case block
updateMults : List (Var vs) -> Env Term vs -> Env Term vs
updateMults [] env = env
updateMults (MkVar p :: us) env = updateMults us (toRig0 p env)

findImpsIn : {vars : _} ->
             FC -> Env Term vars -> List (Name, Term vars) -> Term vars ->
             Core ()
findImpsIn fc env ns (Bind _ n b@(Pi _ _ Implicit ty) sc)
    = findImpsIn fc (b :: env)
                 ((n, weaken ty) :: map (\x => (fst x, weaken (snd x))) ns)
                 sc
findImpsIn fc env ns (Bind _ n b sc)
    = findImpsIn fc (b :: env)
                 (map (\x => (fst x, weaken (snd x))) ns)
                 sc
findImpsIn fc env ns ty
    = when (not (isNil ns)) $
           throw (TryWithImplicits fc env (reverse ns))

merge : {vs : List Name} ->
        List (Var vs) -> List (Var vs) -> List (Var vs)
merge [] xs = xs
merge (v :: vs) xs
    = merge vs (v :: filter (not . sameVar v) xs)

-- Extend the list of variables we need in the environment so far, removing
-- duplicates
extendNeeded : {vs : _} ->
               Binder (Term vs) ->
               Env Term vs -> List (Var vs) -> List (Var vs)
extendNeeded (Let _ _ ty val) env needed
    = merge (findUsedLocs env ty) (merge (findUsedLocs env val) needed)
extendNeeded (PLet _ _ ty val) env needed
    = merge (findUsedLocs env ty) (merge (findUsedLocs env val) needed)
extendNeeded b env needed
    = merge (findUsedLocs env (binderType b)) needed

isNeeded : Nat -> List (Var vs) -> Bool
isNeeded x [] = False
isNeeded x (MkVar {i} _ :: xs) = x == i || isNeeded x xs

findScrutinee : {vs : _} ->
                Env Term vs -> RawImp -> Maybe (Var vs)
findScrutinee {vs = n' :: _} (b :: bs) (IVar loc' n)
    = if n' == n && not (isLet b)
         then Just (MkVar First)
         else do MkVar p <- findScrutinee bs (IVar loc' n)
                 Just (MkVar (Later p))
findScrutinee _ _ = Nothing

getNestData : (Name, (Maybe Name, List (Var vars), a)) ->
              (Name, Maybe Name, List (Var vars))
getNestData (n, (mn, enames, _)) = (n, mn, enames)

bindCaseLocals : FC -> List (Name, Maybe Name, List (Var vars)) ->
                 List (Name, Name)-> RawImp -> RawImp
bindCaseLocals fc [] args rhs = rhs
bindCaseLocals fc ((n, mn, envns) :: rest) argns rhs
    = -- trace ("Case local " ++ show (n,mn,envns) ++ " from " ++ show argns) $
        ICaseLocal fc n (fromMaybe n mn)
                 (map getNameFrom envns)
                 (bindCaseLocals fc rest argns rhs)
  where
    getArg : List (Name, Name) -> Nat -> Maybe Name
    getArg [] _ = Nothing
    getArg ((_, x) :: xs) Z = Just x
    getArg (x :: xs) (S k) = getArg xs k

    getNameFrom : Var vars -> Name
    getNameFrom (MkVar {i} _)
        = case getArg argns i of
               Nothing => n
               Just n' => n'

export
caseBlock : {vars : _} ->
            {auto c : Ref Ctxt Defs} ->
            {auto m : Ref MD Metadata} ->
            {auto u : Ref UST UState} ->
            {auto e : Ref EST (EState vars)} ->
            RigCount ->
            ElabInfo -> FC ->
            NestedNames vars ->
            Env Term vars ->
            RawImp -> -- original scrutinee
            Term vars -> -- checked scrutinee
            Term vars -> -- its type
            RigCount -> -- its multiplicity
            List ImpClause -> Maybe (Glued vars) ->
            Core (Term vars, Glued vars)
caseBlock {vars} rigc elabinfo fc nest env scr scrtm scrty caseRig alts expected
    = do -- TODO (or to decide): Blodwen allowed ambiguities in the scrutinee
         -- to be delayed, but now I think it's better to have simpler
         -- resolution rules, and not delay

         est <- get EST
         fullImps <- getToBind fc (elabMode elabinfo)
                               (implicitMode elabinfo) env []
         log "elab.case" 5 $ "Doing a case under unbound implicits " ++ show fullImps

         scrn <- genVarName "scr"
         casen <- genCaseName !(prettyName !(toFullNames (Resolved (defining est))))

         -- Update environment so that linear bindings which were used
         -- (esp. in the scrutinee!) are set to 0 in the case type
         let env = updateMults (linearUsed est) env
         defs <- get Ctxt
         parentDef <- lookupCtxtExact (Resolved (defining est)) (gamma defs)
         let vis = case parentDef of
                        Just gdef =>
                             if visibility gdef == Public
                                then Public
                                else Private
                        Nothing => Public

         -- if the scrutinee is ones of the arguments in 'env' we should
         -- split on that, rather than adding it as a new argument
         let splitOn = findScrutinee env scr

         caseretty_in <- case expected of
                           Just ty => getTerm ty
                           _ =>
                              do nmty <- genName "caseTy"
                                 metaVar fc erased env nmty (TType fc)

         (caseretty, _) <- bindImplicits fc (implicitMode elabinfo) defs env
                                         fullImps caseretty_in (TType fc)
         let casefnty
               = abstractFullEnvType fc (allow splitOn (explicitPi env))
                            (maybe (Bind fc scrn (Pi fc caseRig Explicit scrty)
                                       (weaken caseretty))
                                   (const caseretty) splitOn)
         -- If we can normalise the type without the result being excessively
         -- big do it. It's the depth of stuck applications - 10 is already
         -- pretty much unreadable!
         casefnty <- normaliseSizeLimit defs 10 [] casefnty
         (erasedargs, _) <- findErased casefnty

         logEnv "elab.case" 10 "Case env" env
         logTermNF "elab.case" 2 ("Case function type: " ++ show casen) [] casefnty
         traverse_ addToSave (keys (getMetas casefnty))

         -- If we've had to add implicits to the case type (because there
         -- were unbound implicits) then we're in a bit of a mess. Easiest
         -- way out is to throw an error and try again with the implicits
         -- actually bound! This is rather hacky, but a lot less fiddly than
         -- the alternative of fixing up the environment
         when (not (isNil fullImps)) $ findImpsIn fc [] [] casefnty
         cidx <- addDef casen (record { eraseArgs = erasedargs }
                                (newDef fc casen (if isErased rigc then erased else top)
                                      [] casefnty vis None))

         -- set the totality of the case block to be the same as that
         -- of the parent function
         let tot = fromMaybe PartialOK $ do findSetTotal (flags !parentDef)
         log "elab.case" 5 $
           unwords [ "Setting totality requirement for", show casen
                   , "to", show tot]
         setFlag fc (Resolved cidx) (SetTotal tot)
         let caseRef : Term vars = Ref fc Func (Resolved cidx)

         let applyEnv = applyToFull fc caseRef env
         let appTm : Term vars
                   = maybe (App fc applyEnv scrtm)
                           (const applyEnv)
                           splitOn

         let alts' = map (updateClause casen splitOn nest env) alts
         log "elab.case" 2 $ "Nested: " ++ show (map getNestData (names nest))
         log "elab.case" 2 $ "Generated alts: " ++ show alts'
         logTermNF "elab.case" 2 "Case application" env appTm

         -- Start with empty nested names, since we've extended the rhs with
         -- ICaseLocal so they'll get rebuilt with the right environment
         let nest' = MkNested []
         ust <- get UST
         -- We don't want to keep rechecking delayed elaborators in the
         -- case block, because they're not going to make progress until
         -- we come out again, so save them
         let olddelayed = delayedElab ust
         put UST (record { delayedElab = [] } ust)
         processDecl [InCase] nest' [] (IDef fc casen alts')

         -- If there's no duplication of the scrutinee in the block,
         -- flag it as inlinable.
         -- This will be the case either if the scrutinee is a variable, in
         -- which case the duplication won't hurt, or if there's no variable
         -- duplicated in the body (what ghc calls W-safe)
         -- We'll check that second condition later, after generating the
         -- runtime (erased) case trees
         let inlineOK = maybe False (const True) splitOn
         when inlineOK $ setFlag fc casen Inline

         ust <- get UST
         put UST (record { delayedElab = olddelayed } ust)

         pure (appTm, gnf env caseretty)
  where
    mkLocalEnv : Env Term vs -> Env Term vs
    mkLocalEnv [] = []
    mkLocalEnv (b :: bs)
        = let b' = if isLinear (multiplicity b)
                      then setMultiplicity b erased
                      else b in
              b' :: mkLocalEnv bs

    -- Return the original name in the environment, and what it needs to be
    -- called in the case block. We need to mapping to build the ICaseLocal
    -- so that it applies to the right original variable
    getBindName : Int -> Name -> List Name -> (Name, Name)
    getBindName idx n@(UN un) vs
       = if n `elem` vs then (n, MN (displayUserName un) idx) else (n, n)
    getBindName idx n vs
       = if n `elem` vs then (n, MN "_cn" idx) else (n, n)

    -- Returns a list of names that nestednames should be applied to, mapped
    -- to what the name has become in the case block, and a list of terms for
    -- the LHS of the case to be applied to.
    addEnv : {vs : _} ->
             Int -> Env Term vs -> List Name -> (List (Name, Name), List RawImp)
    addEnv idx [] used = ([], [])
    addEnv idx {vs = v :: vs} (b :: bs) used
        = let n = getBindName idx v used
              (ns, rest) = addEnv (idx + 1) bs (snd n :: used)
              ns' = n :: ns in
              (ns', IAs fc EmptyFC UseLeft (snd n) (Implicit fc True) :: rest)

    -- Replace a variable in the argument list; if the reference is to
    -- a variable kept in the outer environment (therefore not an argument
    -- in the list) don't consume it
    replace : (idx : Nat) -> RawImp -> List RawImp -> List RawImp
    replace Z lhs (old :: xs)
       = let lhs' = case old of
                         IAs loc' nameLoc' side n _ => IAs loc' nameLoc' side n lhs
                         _ => lhs in
             lhs' :: xs
    replace (S k) lhs (x :: xs)
        = x :: replace k lhs xs
    replace _ _ xs = xs

    mkSplit : Maybe (Var vs) ->
              RawImp -> List RawImp ->
              List RawImp
    mkSplit Nothing lhs args = reverse (lhs :: args)
    mkSplit (Just (MkVar {i} prf)) lhs args
        = reverse (replace i lhs args)

    -- Names used in the pattern we're matching on, so don't bind them
    -- in the generated case block
    usedIn : RawImp -> List Name
    usedIn (IBindVar _ n) = [UN $ Basic n]
    usedIn (IApp _ f a) = usedIn f ++ usedIn a
    usedIn (IAs _ _ _ n a) = n :: usedIn a
    usedIn (IAlternative _ _ alts) = concatMap usedIn alts
    usedIn _ = []

    -- Get a name update for the LHS (so that if there's a nested data declaration
    -- the constructors are applied to the environment in the case block)
    nestLHS : FC -> (Name, (Maybe Name, List (Var vars), a)) -> (Name, RawImp)
    nestLHS fc (n, (mn, ns, t))
        = (n, apply (IVar fc (fromMaybe n mn))
                    (map (const (Implicit fc False)) ns))

    applyNested : NestedNames vars -> RawImp -> RawImp
    applyNested nest lhs
        = let fc = getFC lhs in
              substNames [] (map (nestLHS fc) (names nest)) lhs

    updateClause : Name -> Maybe (Var vars) ->
                   NestedNames vars ->
                   Env Term vars -> ImpClause -> ImpClause
    updateClause casen splitOn nest env (PatClause loc' lhs rhs)
        = let (ns, args) = addEnv 0 env (usedIn lhs)
              args' = mkSplit splitOn lhs args
              lhs' = apply (IVar loc' casen) args' in
              PatClause loc' (applyNested nest lhs')
                        (bindCaseLocals loc' (map getNestData (names nest))
                                        ns rhs)
    -- With isn't allowed in a case block but include for completeness
    updateClause casen splitOn nest env (WithClause loc' lhs wval prf flags cs)
        = let (_, args) = addEnv 0 env (usedIn lhs)
              args' = mkSplit splitOn lhs args
              lhs' = apply (IVar loc' casen) args' in
              WithClause loc' (applyNested nest lhs') wval prf flags cs
    updateClause casen splitOn nest env (ImpossibleClause loc' lhs)
        = let (_, args) = addEnv 0 env (usedIn lhs)
              args' = mkSplit splitOn lhs args
              lhs' = apply (IVar loc' casen) args' in
              ImpossibleClause loc' (applyNested nest lhs')

export
checkCase : {vars : _} ->
            {auto c : Ref Ctxt Defs} ->
            {auto m : Ref MD Metadata} ->
            {auto u : Ref UST UState} ->
            {auto e : Ref EST (EState vars)} ->
            RigCount -> ElabInfo ->
            NestedNames vars -> Env Term vars ->
            FC -> (scr : RawImp) -> (ty : RawImp) -> List ImpClause ->
            Maybe (Glued vars) ->
            Core (Term vars, Glued vars)
checkCase rig elabinfo nest env fc scr scrty_in alts exp
    = delayElab fc rig env exp CaseBlock $
        do scrty_exp <- case scrty_in of
                             Implicit _ _ => guessScrType alts
                             _ => pure scrty_in
           (scrtyv, scrtyt) <- check erased elabinfo nest env scrty_exp
                                     (Just (gType fc))
           logTerm "elab.case" 10 "Expected scrutinee type" scrtyv
           -- Try checking at the given multiplicity; if that doesn't work,
           -- try checking at Rig1 (meaning that we're using a linear variable
           -- so the scrutinee should be linear)
           let chrig = if isErased rig then erased else top
           log "elab.case" 5 $ "Checking " ++ show scr ++ " at " ++ show chrig

           (scrtm_in, gscrty, caseRig) <- handle
              (do c <- runDelays (const True) $ check chrig elabinfo nest env scr (Just (gnf env scrtyv))
                  pure (fst c, snd c, chrig))
            $ \case
                e@(LinearMisuse _ _ r _)
                  => branchOne
                     (do c <- runDelays (const True) $ check linear elabinfo nest env scr
                              (Just (gnf env scrtyv))
                         pure (fst c, snd c, linear))
                     (throw e)
                     r
                e => throw e

           scrty <- getTerm gscrty
           logTermNF "elab.case" 5 "Scrutinee type" env scrty
           defs <- get Ctxt
           checkConcrete !(nf defs env scrty)
           caseBlock rig elabinfo fc nest env scr scrtm_in scrty caseRig alts exp
  where
    -- For the moment, throw an error if we haven't been able to work out
    -- the type of the case scrutinee, because we'll need it to build the
    -- type of the case block. But (TODO) consider delaying on failure?
    checkConcrete : NF vs -> Core ()
    checkConcrete (NApp _ (NMeta n i _) _)
        = throw (GenericMsg fc "Can't infer type for case scrutinee")
    checkConcrete _ = pure ()

    applyTo : Defs -> RawImp -> NF [] -> Core RawImp
    applyTo defs ty (NBind fc _ (Pi _ _ Explicit _) sc)
        = applyTo defs (IApp fc ty (Implicit fc False))
               !(sc defs (toClosure defaultOpts [] (Erased fc False)))
    applyTo defs ty (NBind _ x (Pi _ _ _ _) sc)
        = applyTo defs (INamedApp fc ty x (Implicit fc False))
               !(sc defs (toClosure defaultOpts [] (Erased fc False)))
    applyTo defs ty _ = pure ty

    -- Get the name and type of the family the scrutinee is in
    getRetTy : Defs -> NF [] -> Core (Maybe (Name, NF []))
    getRetTy defs (NBind fc _ (Pi _ _ _ _) sc)
        = getRetTy defs !(sc defs (toClosure defaultOpts [] (Erased fc False)))
    getRetTy defs (NTCon _ n _ arity _)
        = do Just ty <- lookupTyExact n (gamma defs)
                  | Nothing => pure Nothing
             pure (Just (n, !(nf defs [] ty)))
    getRetTy _ _ = pure Nothing

    -- Guess a scrutinee type by looking at the alternatives, so that we
    -- have a hint for building the case type
    guessScrType : List ImpClause -> Core RawImp
    guessScrType [] = pure $ Implicit fc False
    guessScrType (PatClause _ x _ :: xs)
        = case getFn x of
               IVar _ n =>
                  do defs <- get Ctxt
                     [(n', (_, ty))] <- lookupTyName n (gamma defs)
                         | _ => guessScrType xs
                     Just (tyn, tyty) <- getRetTy defs !(nf defs [] ty)
                         | _ => guessScrType xs
                     applyTo defs (IVar fc tyn) tyty
               _ => guessScrType xs
    guessScrType (_ :: xs) = guessScrType xs


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

> %name Vect xs, ys, zs

> append : Vect n a -> Vect m a -> Vect (n + m) a
> append {n} xs ys = ?foo

> vadd : Num a => Vect n a -> Vect n a -> Vect n a
> vadd [] ys = ?bar
> vadd (x :: xs) ys = ?baz

> suc : (x : Nat) -> (y : Nat) -> x = y -> S x = S y
> suc x y prf = ?quux

> suc' : x = y -> S x = S y
> suc' {x} {y} prf = ?quuz

ext: lidr


text:
module Minecraft.Core.Item.GenericData

%default total

public export
record GenericItemData where
  constructor MkItem
  {auto givenName : Maybe String}

max_stars_repo_name: po-stulate/postulate

max_issues_repo_name: po-stulate/postulate

max_forks_repo_name: po-stulate/postulate


text:
module Graphics.Cairo.Cairo

import Data.Fin
import Data.Vect
import Graphics.Color
import Graphics.SDL2.SDL
import Graphics.Cairo.Config

%include C "cairo_idris.h"
%include C "cairo.h"
%link C "cairo_idris.o"
%lib C "cairo"

%access private

||| The Cairo Surface
export
data Surface = Srf Ptr

||| A cairo drawing context
export
data DrawingCtx = Ctx Ptr

||| Glfw Window
export
data Window = Win Ptr

||| Glfw Window
export
data Pixels = MkPixels Ptr

public export
Point : Type
Point = (Double, Double)

-- -----------------------------------------------------------------------------
-- Lifecycle

||| Creates a cairo image surface
||| @ width the width of the image
||| @ height the height of the image
export
createSurface : (width: Int) -> (height: Int) -> IO Surface
createSurface width height =
  do ptr <- foreign FFI_C "idr_cairo_create_image_surface" (Int -> Int -> IO Ptr) width height
     pure $ Srf ptr

||| creates a drawing context
||| @ surface the surface for the drawing context
export
createContext : (surface: Surface) -> IO DrawingCtx
createContext (Srf ptrSurface) =
  do ptr <- foreign FFI_C "cairo_create" (Ptr -> IO Ptr) ptrSurface
     pure $ Ctx ptr

||| destroy the drawing context
export
destroyContext : DrawingCtx -> IO ()
destroyContext (Ctx ptr) = foreign FFI_C "cairo_destroy" (Ptr -> IO ()) ptr

||| destroys the surface
export
destroySurface : (surface: Surface) -> IO ()
destroySurface (Srf ptr) =
  foreign FFI_C "cairo_surface_destroy" (Ptr -> IO ()) ptr

export
flushSurface : (surface: Surface) -> IO ()
flushSurface (Srf ptr) = foreign FFI_C "cairo_surface_flush" (Ptr -> IO ()) ptr

export
createSurfaceData : Int -> Int -> IO Pixels
createSurfaceData width height = do p <- foreign FFI_C "idr_create_surface_buffer" (Int -> Int -> IO Ptr) width height
                                    pure $ MkPixels p

export
createSurfaceForData : TextureRaw -> Int -> Int -> IO Surface
createSurfaceForData (MkTextureRaw ptr pitch) width height =
  do p <- foreign FFI_C "idr_surface_for_data" (Ptr -> Int -> Int -> Int -> IO Ptr) ptr width height pitch
     pure $ Srf p

public export
freeSurfaceData : Pixels -> IO ()
freeSurfaceData (MkPixels ptr) = foreign FFI_C "free" (Ptr -> IO ()) ptr

-- -----------------------------------------------------------------------------
-- Fonts / Text (see http://cairographics.org/manual/cairo-text.html )

--cairo_select_font_face (cr, "serif", CAIRO_FONT_SLANT_NORMAL, CAIRO_FONT_WEIGHT_BOLD);

||| sets the font size for the current font
setFontSize : (ctx: DrawingCtx) -> (size: Double) -> IO ()
setFontSize (Ctx ptr) s = foreign FFI_C "cairo_set_font_size" (Ptr -> Double -> IO ()) ptr s

||| Displays the text
showText : (ctx: DrawingCtx) -> (t: String) -> IO ()
showText (Ctx ptr) t = foreign FFI_C "cairo_show_text" (Ptr -> String -> IO ()) ptr t

--void 	cairo_glyph_path ()
--void 	cairo_text_path ()

-- -----------------------------------------------------------------------------
-- Drawing Context http://cairographics.org/manual/cairo-cairo-t.html

||| set the color
||| @ ctx the current drawing context
||| @ r the red component. 0-1
||| @ g the green component. 0-1
||| @ b the blue component. 0-1
||| @ alpha the alpha
public export
setSourceRGBA : (ctx: DrawingCtx) -> (r: Double) -> (g: Double) -> (b: Double) -> (alpha: Double) -> IO ()
setSourceRGBA (Ctx ptr) r g b a = foreign FFI_C "cairo_set_source_rgba" (Ptr -> Double -> Double -> Double -> Double -> IO ()) ptr r g b a

||| sets the line width for the current drawing context

||| @ ctx the current drawing context
||| @ width the line width
public export
setLineWidth : (ctx: DrawingCtx) -> (width: Double) -> IO ()
setLineWidth (Ctx ptr) width = foreign FFI_C "cairo_set_line_width" (Ptr -> Double -> IO ()) ptr width

||| A drawing operator that strokes the current path according to the current line width, line join, line cap, and dash settings
public export
stroke : (ctx: DrawingCtx) -> IO ()
stroke (Ctx ptr) = foreign FFI_C "cairo_stroke" (Ptr -> IO ()) ptr

||| A drawing operator that fills the current path according to the current fill rule, (each sub-path is implicitly closed before being filled)
public export
fill : (ctx: DrawingCtx) -> IO ()
fill (Ctx ptr) = foreign FFI_C "cairo_fill" (Ptr -> IO ()) ptr

-- -----------------------------------------------------------------------------
-- Paths, see also http://cairographics.org/manual/cairo-Paths.html

||| Begin a new sub-path. After this call the current point will be (x , y ).
public export
moveTo : (ctx: DrawingCtx) -> (Double, Double) -> IO ()
moveTo (Ctx ptr) (x, y) = foreign FFI_C "cairo_move_to" (Ptr -> Double -> Double -> IO ()) ptr x y

||| Adds a line to the path from the current point to position (x , y ) in user-space coordinates. After this call the current point will be (x , y ).
||| If there is no current point before the call to cairo_line_to() this function will behave as cairo_move_to(cr , x , y ).
public export
lineTo : (ctx: DrawingCtx) -> (Double, Double) -> IO ()
lineTo (Ctx ptr) (x, y) = foreign FFI_C "cairo_line_to" (Ptr -> Double -> Double -> IO ()) ptr x y

||| Adds a circular arc of the given radius to the current path.
||| The arc is centered at (xc , yc ), begins at angle1 and proceeds in the direction of increasing angles to end at angle2 .
||| If angle2 is less than angle1 it will be progressively increased by 2*M_PI until it is greater than angle1 .
||| Angles are measured in radians.
||| @ ctx the current drawing context
||| @ c x coordinate of the center of the arc
||| @ r radius
||| @ angle1 the start angle, in radians
||| @ angle2 the end angle, in radians
public export
arc : (ctx: DrawingCtx) -> (c: (Double, Double)) -> (r: Double) -> (angle1: Double) -> (angle2: Double) -> IO ()
arc (Ctx ptr) (cx, cy) r angle1 angle2 =
  foreign FFI_C "cairo_arc" (Ptr -> Double -> Double -> Double -> Double -> Double -> IO ()) ptr cx cy r angle1 angle2

||| see documentation of arc.
public export
arcNegative : (ctx: DrawingCtx) -> (Double, Double) -> (r: Double) -> (angle1: Double) -> (angle2: Double) -> IO ()
arcNegative (Ctx ptr) (cx, cy) r angle1 angle2 =
  foreign FFI_C "cairo_arc_negative" (Ptr -> Double -> Double -> Double -> Double -> Double -> IO ()) ptr cx cy r angle1 angle2

--cairo_path_t * 	cairo_copy_path ()
--cairo_path_t * 	cairo_copy_path_flat ()
--void 	cairo_path_destroy ()
--void 	cairo_append_path ()
-- cairo_bool_t 	cairo_has_current_point ()
-- void 	cairo_get_current_point ()
-- void 	cairo_path_extents ()

||| Clears the current path. After this call there will be no path and no current point.
public export
newPath : (ctx: DrawingCtx) -> IO ()
newPath (Ctx ptr) = foreign FFI_C "cairo_new_path" (Ptr -> IO ()) ptr

||| Begin a new sub-path. Note that the existing path is not affected. After this call there will be no current point.
||| In many cases, this call is not needed since new sub-paths are frequently started with moveTo.
||| A call to newSubPath is particularly useful when beginning a new sub-path with one of the arc calls.
||| This makes things easier as it is no longer necessary to manually compute the arc's initial coordinates for a call to cairo_move_to(
public export
newSubPath : (ctx: DrawingCtx) -> IO ()
newSubPath (Ctx ptr) = foreign FFI_C "cairo_new_sub_path" (Ptr -> IO ()) ptr

||| Adds a line segment to the path from the current point to the beginning of the current sub-path,
||| (the most recent point passed to moveTo), and closes this sub-path.
||| After this call the current point will be at the joined endpoint of the sub-path.
public export
closePath : (ctx: DrawingCtx) -> IO ()
closePath (Ctx ptr) = foreign FFI_C "cairo_close_path" (Ptr -> IO ()) ptr

||| Adds a cubic Bézier spline to the path from the current point to position (x3 , y3 ) in user-space coordinates,
||| using (x1 , y1 ) and (x2 , y2 ) as the control points. After this call the current point will be (x3 , y3 ).
public export
curveTo : (ctx: DrawingCtx) -> (Double, Double) -> (Double, Double) -> (Double, Double) -> IO ()
curveTo (Ctx ptr) (x1, y1) (x2, y2) (x3, y3) =
  foreign FFI_C "cairo_curve_to" (Ptr -> Double -> Double -> Double -> Double -> Double -> Double -> IO ()) ptr x1 y1 x2 y2 x3 y3

||| Adds a closed sub-path rectangle of the given size to the current path at position (x , y ) in user-space coordinates.
export
rectangle : (ctx: DrawingCtx) -> (p: Point) -> (width: Double) -> (height: Double) -> IO ()
rectangle (Ctx ptr) (x,y) width height =
  foreign FFI_C "cairo_rectangle" (Ptr -> Double -> Double -> Double -> Double -> IO()) ptr x y width height

||| Relative-coordinate version of cairo_curve_to().
||| All offsets are relative to the current point. Adds a cubic Bézier spline to the path from the current point
||| to a point offset from the current point by (dx3 , dy3 ), using points offset by (dx1 , dy1 )
||| and (dx2 , dy2 ) as the control points. After this call the current point will be offset by (dx3 , dy3 ).
public export
relCurveTo : (ctx: DrawingCtx) -> (Double, Double) -> (Double, Double) -> (Double, Double) -> IO ()
relCurveTo (Ctx ptr) (dx1, dy1) (dx2, dy2) (dx3, dy3) =
  foreign FFI_C "cairo_rel_curve_to" (Ptr -> Double -> Double -> Double -> Double -> Double -> Double -> IO ()) ptr dx1 dy1 dx2 dy2 dx3 dy3

||| Relative-coordinate version of cairo_line_to().
||| Adds a line to the path from the current point to a point that is offset from the current point by (dx , dy )
||| in user space. After this call the current point will be offset by (dx , dy ).
public export
relLineTo : (ctx: DrawingCtx) -> (Double, Double) -> IO ()
relLineTo (Ctx ptr) (dx, dy) = foreign FFI_C "cairo_rel_line_to" (Ptr -> Double -> Double -> IO ()) ptr dx dy

||| Begin a new sub-path. After this call the current point will offset by (dx , dy ).
public export
relMoveTo : (ctx: DrawingCtx) -> (Double, Double) -> IO ()
relMoveTo (Ctx ptr) (dx, dy) = foreign FFI_C "cairo_rel_move_to" (Ptr -> Double -> Double -> IO ()) ptr dx dy

-- -----------------------------------------------------------------------------
-- Transformations

-- see http://cairographics.org/manual/cairo-Transformations.html

||| Modifies the current transformation matrix (CTM) by translating the user-space origin by (tx , ty ).
||| This offset is interpreted as a user-space coordinate according to the CTM in place before the new call to cairo_translate().
||| In other words, the translation of the user-space origin takes place after any existing transformation.
public export
translate : (ctx : DrawingCtx) -> (tx: Double, ty: Double) -> IO ()
translate (Ctx ptr) tx ty = foreign FFI_C "cairo_translate" (Ptr -> Double -> Double -> IO ()) ptr tx ty

||| Modifies the current transformation matrix (CTM) by scaling the X and Y user-space axes by sx and sy respectively.
||| The scaling of the axes takes place after any existing transformation of user space.
public export
scale : (ctx : DrawingCtx) -> (sx: Double, sy: Double) -> IO ()
scale (Ctx ptr) sx sy = foreign FFI_C "cairo_scale" (Ptr -> Double -> Double -> IO ()) ptr sx sy

||| Modifies the current transformation matrix (CTM) by rotating the user-space axes by angle radians.
||| The rotation of the axes takes places after any existing transformation of user space.
||| The rotation direction for positive angles is from the positive X axis toward the positive Y axis.
public export
rotate : (ctx : DrawingCtx) -> (angle: Double) -> IO ()
rotate (Ctx ptr) angle = foreign FFI_C "cairo_rotate" (Ptr -> Double -> IO ()) ptr angle

-- -----------------------------------------------------------------------------
-- Import / Export

-- see http://cairographics.org/manual/cairo-PNG-Support.html

||| writes the surface to an png
||| TODO this should only work on an image surface
||| @ surface the surface to export as a PNG
||| @ filename file name of the PNG
export
writePNG : (surface: Surface) -> (filename: String) -> IO ()
writePNG (Srf ptr) filename =
  foreign FFI_C "cairo_surface_write_to_png" (Ptr -> String -> IO ()) ptr filename

||| creates a cairo image surface from a png
||| @ filename filename of the png
export
createSurfaceFromPNG : (filename: String) -> IO Surface
createSurfaceFromPNG filename = do ptr <- foreign FFI_C "cairo_image_surface_create_from_png" (String -> IO Ptr) filename
                                   pure $ Srf ptr

public export
draw : (ctx: DrawingCtx) -> Vect (S k) (Double, Double) -> IO ()
draw ctx (x :: xs) = do
                        moveTo ctx x
                        draw' xs
                     where draw' : Vect n (Double, Double) -> IO ()
                           draw' []        = pure ()
                           draw' (y :: ys) = do lineTo ctx y
                                                draw' ys

max_stars_repo_name: eckart/cairo-idris

max_issues_repo_name: eckart/cairo-idris

max_forks_repo_name: eckart/cairo-idris


text:
module Inigo.Package.Package

import Data.List
import Data.Maybe
import Extra.Either
import Extra.List
import Extra.String
import Fmt
import public Inigo.Package.ExtraDep
import Inigo.Package.ParseHelpers
import Inigo.Paths
import Inigo.PkgTree
import SemVar
import System.Path
import Toml

public export
record Package where
  constructor MkPackage
  ns : String
  package : String
  version : Version
  description : Maybe String
  link : Maybe String
  readme : Maybe String
  modules : List String
  depends : List String
  license : Maybe String
  sourcedir : String
  main : Maybe String
  executable : Maybe String
  deps : List (List String, Requirement)
  devDeps : List (List String, Requirement)
  extraDeps : List ExtraDep

public export
Show Package where
  show pkg =
    "Package{" ++
      (join "" [
        "ns=", (show $ ns pkg),
        ", package=", (show $ package pkg),
        ", version=", (show $ version pkg),
        ", description=", (show $ description pkg),
        ", link=", (show $ link pkg),
        ", readme=", (limit 50 $ show $ readme pkg),
        ", modules=", (show $ modules pkg),
        ", depends=", (show $ depends pkg),
        ", license=", (show $ license pkg),
        ", sourcedir=", (show $ sourcedir pkg),
        ", main=", (show $ main pkg),
        ", executable=", (show $ executable pkg),
        ", deps=", (show $ deps pkg),
        ", dev-deps=", (show $ devDeps pkg),
        ", extra-deps=", (show $ extraDeps pkg)
      ]) ++ "}"

public export
Eq Package where
  (MkPackage ns0 package0 version0 description0 link0 readme0 modules0 depends0 license0 src0 main0 executable0 deps0 devDeps0 extraDeps0)
    == (MkPackage ns1 package1 version1 description1 link1 readme1 modules1 depends1 license1 src1 main1 executable1 deps1 devDeps1 extraDeps1) =
      ns0 == ns1 && package0 == package1 && version0 == version1 && description0 == description1 && link0 == link1 && readme0 == readme1 &&
      modules0 == modules1 && depends0 == depends1 && license0 == license1 && src0 == src1 && main0 == main1 && executable0 == executable1 &&
      deps0 == deps1 && devDeps0 == devDeps1 && extraDeps0 == extraDeps1

export
parseDeps : List String -> Toml -> Either String (List (List String, Requirement))
parseDeps key toml =
  foldl parseDepsAcc (Right []) (getToml key toml)
  where
    parseDepsAcc : Either String (List (List String, Requirement)) -> (List String, Value) -> Either String (List (List String, Requirement))
    parseDepsAcc accE (key, el) =
      case el of
        Str val =>
          do
            acc <- accE
            dep <- expect ("Invalid requirement: " ++ show key ++ "=" ++ show val) (parseRequirement val)
            pure $ (key, dep) :: acc
        _ =>
          Left ("Invalid dep found: " ++ show key)

||| Attempts to parse a package
export
parsePackage : String -> Either String Package
parsePackage pkgToml =
  do
    toml <- expect "failed to parse Toml" $ parseToml pkgToml
    ns <- string ["ns"] toml
    package <- string ["package"] toml
    versionStr <- string ["version"] toml
    version <- expect ("Invalid version: " ++ versionStr) (parseVersion versionStr)
    description <- maybe (string ["description"] toml)
    link <- maybe (string ["link"] toml)
    readme <- maybe (string ["readme"] toml)
    modules <- listStr ["modules"] toml
    depends <- listStr ["depends"] toml
    license <- maybe (string ["license"] toml)
    sourcedir <- withDefault "" (string ["sourcedir"] toml)
    main <- maybe (string ["main"] toml)
    executable <- maybe (string ["executable"] toml)
    deps <- parseDeps ["deps"] toml
    devDeps <- parseDeps ["dev-deps"] toml
    extraDeps <- parseExtraDeps toml
    pure (MkPackage ns package version description link readme modules depends license sourcedir main executable deps devDeps extraDeps)

-- TODO: Get deps better, e.g. pin instead of `&&`
export
toToml : Package -> Toml
toToml pkg =
  (mapMaybe id [
    Just (["ns"], Str (ns pkg)),
    Just (["package"], Str (package pkg)),
    Just (["version"], Str (show (version pkg))),
    map (\desc => (["description"], Str desc)) (description pkg),
    map (\link => (["link"], Str link)) (link pkg),
    map (\desc => (["readme"], Str desc)) (readme pkg),
    Just (["modules"], Lst (map Str (modules pkg))),
    Just (["depends"], Lst (map Str (depends pkg))),
    map (\license => (["license"], Str license)) (license pkg),
    Just (["sourcedir"], Str (sourcedir pkg)),
    map (\main => (["main"], Str main)) (main pkg),
    map (\executable => (["executable"], Str executable)) (executable pkg)
  ]) ++ (depsVal "deps" (deps pkg)) ++ (depsVal "dev-deps" (devDeps pkg))
  ++ toToml pkg.extraDeps
  where
    depsVal : String -> List (List String, Requirement) -> List (List String, Value)
    depsVal baseKey = map (\(key, req) => (baseKey :: key, Str (show req)))

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

whenCons : Monoid a => List b -> a -> a
whenCons [] _ = neutral
whenCons _ x = x

-- ||| Generates an ipkg for compatibility with the native idris build system
export
generateIPkg : (includeExe : Bool) -> Maybe String -> Package -> String
generateIPkg exe depBuildDir pkg =
  let
    main = fromMaybe "" $ map ("\nmain = " ++) (main pkg)
    executable = if exe
        then fromMaybe "" $ map ("\nexecutable = " ++) (executable pkg)
        else ""
    modules' = whenCons pkg.modules $ fmt "modules = %s " $ join ", " (modules pkg)
    depends' = whenCons pkg.depends $ fmt "depends = %s " $ join ", " (depends pkg)
    buildDir = fromMaybe "build" depBuildDir
  in
    fmt """
package %s

%s
%s

sourcedir = %s
builddir = %s

version = %s%s%s
""" (package pkg) modules' depends' (quote pkg.sourcedir) (quote buildDir) (show $ version pkg) main executable

export
getDepsPackage : Bool -> Package -> List String
getDepsPackage dev pkg =
    let deps : List (List String, Requirement)
        deps = (if dev then pkg.devDeps else []) ++ pkg.deps
    in depsOnto pkg.extraDeps $ map ((inigoDepDir </>) . joinPath . Builtin.fst) deps
    where
    depsOnto : List ExtraDep -> List String -> List String
    depsOnto [] deps = deps
    depsOnto (ed :: eds) deps =
        let dir = getExtraDepDir ed
        in depsOnto eds $ map (dir </>) ed.subDirs ++ deps

export
HasDeps Package String where
    getDeps = getDepsPackage

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
||| Slightly different lexer than the source language because we are more free
||| as to what can be identifiers, and fewer tokens are supported. But otherwise,
||| we can reuse the standard stuff
module Idris.IDEMode.Parser

import Idris.IDEMode.Commands
import Core.Core
import Core.Name
import Core.Metadata
import Core.FC

import Data.Maybe
import Data.List
import Data.String
import Parser.Lexer.Source
import Parser.Source
import Parser.Support
import Libraries.Text.Lexer
import Libraries.Text.Lexer.Tokenizer
import Libraries.Text.Parser
import Libraries.Utils.String

%default total

%hide Text.Lexer.symbols
%hide Parser.Lexer.Source.symbols

symbols : List String
symbols = ["(", ":", ")"]

stringTokens : Tokenizer Token
stringTokens
    = match (someUntil (is '"') (escape (is '\\') any <|> any)) $ StringLit 0

ideTokens : Tokenizer Token
ideTokens =
      match (choice $ exact <$> symbols) Symbol
  <|> match digits (IntegerLit . cast)
  <|> compose (is '"')
              (const $ StringBegin Single)
              (const ())
              (const stringTokens)
              (const $ is '"')
              (const StringEnd)
  <|> match identAllowDashes Ident
  <|> match space (const Comment)

idelex : String -> Either (StopReason, Int, Int, String) (List (WithBounds Token))
idelex str
    = case lex ideTokens str of
           -- Add the EndInput token so that we'll have a line and column
           -- number to read when storing spans in the file
           (tok, (EndInput, l, c, _)) => Right (filter notComment tok ++
                                               [MkBounded EndInput False (MkBounds l c l c)])
           (_, fail) => Left fail
    where
      notComment : WithBounds Token -> Bool
      notComment t = case t.val of
                          Comment => False
                          _ => True

covering
sexp : Rule SExp
sexp
    = do symbol ":"; exactIdent "True"
         pure (BoolAtom True)
  <|> do symbol ":"; exactIdent "False"
         pure (BoolAtom False)
  <|> do i <- intLit
         pure (IntegerAtom i)
  <|> do str <- simpleStr
         pure (StringAtom str)
  <|> do symbol ":"; x <- unqualifiedName
         pure (SymbolAtom x)
  <|> do symbol "("
         xs <- many sexp
         symbol ")"
         pure (SExpList xs)

ideParser : {e : _} ->
            String -> Grammar SemanticDecorations Token e ty -> Either Error ty
ideParser str p
    = do toks   <- mapFst (fromLexError (Virtual Interactive)) $ idelex str
         (_, _, (parsed, _)) <- mapFst (fromParsingErrors (Virtual Interactive)) $ parseWith p toks
         Right parsed

export
covering
parseSExp : String -> Either Error SExp
parseSExp inp
    = ideParser inp (do c <- sexp; eoi; pure c)


text:
||| Borrowed From Idris2 and improved with Test.Unit
module Idealised

import Data.List

import Test.Golden

%default total

tests : TestPool
tests
  = MkTestPool "Tests"
        []
        Nothing
        [
          "idealised-all"
        ]

covering
main : IO ()
main
  = runner [ tests ]

-- [ EOF ]

max_stars_repo_name: gallais/linear-circuits

max_issues_repo_name: gallais/linear-circuits

max_forks_repo_name: gallais/linear-circuits


text:
module Main

import Effekt.CpsStaged
import Effekt.IteratedUnstaged
import Effekt.IteratedStaged
import Effekt.AvoidEta

fail : STM (String :: rs) a
fail = shift0 (\k => do
  pure (Str "no"))

flip : STM (r :: rs) Bool
flip = shift0 (\k => do
  resume k Tru
  resume k Fls)

delimitFail : STM rs String
delimitFail {rs} = do
  a <- reset0 fail
  pure {rs} ((Cat (Str "Answer was: ") a))

emit : Exp a -> STM (List a :: rs) ()
emit a = shift0 (\k => do
  as <- resume k Uni
  pure ((Con a as)))

collect : STM (List a :: rs) b -> STM rs (List a)
collect {rs} {a} m = reset0 {a=List a} {rs} (
  (>>=) {rs=List a :: rs} m (\u => pure {rs=List a :: rs} Emp))

choice : Exp Int -> STM (String :: rs) Int
choice {rs} = letrec (\recurse => \n => do
  ifthenelse ((Sma n (Lit 1)))
    fail
    (do
      b <- flip
      ifthenelse b
        (pure {rs=String::rs} n)
        (recurse ((Sub n (Lit 1))))))

triple : Exp Int -> Exp Int -> STM (String :: rs) (Int, Int, Int)
triple {rs} n s = do
  i  <- choice n
  j  <- choice ((Sub i (Lit 1)))
  k  <- choice ((Sub j (Lit 1)))
  ifthenelse ((Equ ((Add i ((Add j k)))) s))
    (pure {rs=String::rs} (Tri i j k))
    fail

emitTriples : STM (String :: List (Int, Int, Int) :: rs) String
emitTriples {rs} =
  (>>=) {rs=(String :: List (Int, Int, Int) :: rs)} (triple (Lit 9) (Lit 15))  (\ijk =>
  (>>=) {rs=(String :: List (Int, Int, Int) :: rs)} (lift (emit ijk)) (\u =>
  pure {rs=(String :: List (Int, Int, Int) :: rs)} (Str "done")))

emittedTriples : STM [] (List (Int, Int, Int))
emittedTriples = collect {rs=[]} (reset0 (emitTriples {rs=[]}))

first : Exp a -> STM (Maybe a :: rs) ()
first {rs} a = shift0 (\k => do
  pure {rs} ((Jus a)))

firstTriples : STM (String :: Maybe (Int, Int, Int) :: rs) String
firstTriples {rs} =
  (>>=) {rs=(String :: Maybe (Int, Int, Int) :: rs)} (triple (Lit 9) (Lit 15))  (\ijk =>
  (>>=) {rs=(String :: Maybe (Int, Int, Int) :: rs)} (lift (first ijk)) (\u =>
  pure {rs=(String :: Maybe (Int, Int, Int) :: rs)} (Str "done")))
firstTriple : STM [] (Maybe (Int, Int, Int))
firstTriple = reset0 {a=Maybe (Int,Int,Int)} {rs=[]} (
  (>>=) {rs=[Maybe (Int,Int,Int)]} (reset0 (firstTriples {rs=[]})) (\u =>
  pure {rs=[Maybe (Int,Int,Int)]} Noh))

program : Exp (Stm [String,List Int] String -> Stm [] (List Int))
program = Lam (\m =>
  reify (collect {rs=[]} {a=Int} {b=String} (reset0 {rs=[List Int]} (
    reflect {a=String} {rs=[String,List Int]} m))))

main : IO ()
main = putStrLn (pretty 0 emittedTriples)

  -- generated_source : List (Int, Int, Int)
  -- generated_source =
  -- ((((let f0 x1 = (\x2 => (\x3 =>
  --    (if (x1 < 1)
  --      then (x3 "no")
  --      else ((x2 x1) (\x4 => (((f0 (x1 - 1)) x2) x3)))))) in f0) 9) (\x0 => (\x1 =>
  -- ((((let f2 x3 = (\x4 => (\x5 =>
  --    (if (x3 < 1)
  --      then (x5 "no")
  --      else ((x4 x3) (\x6 => (((f2 (x3 - 1)) x4) x5)))))) in f2) (x0 - 1)) (\x2 => (\x3 =>
  -- ((((let f4 x5 = (\x6 => (\x7 =>
  --    (if (x5 < 1)
  --      then (x7 "no")
  --      else ((x6 x5) (\x8 => (((f4 (x5 - 1)) x6) x7)))))) in f4) (x2 - 1)) (\x4 => (\x5 =>
  --        (if ((x0 + (x2 + x4)) == 15)
  --          then ((x0, x2, x4) :: (x5 "done"))
  --          else (x5 "no"))))) x3)))) x1)))) (\x0 => []))

max_stars_repo_name: b-studios/idris-effekt

max_issues_repo_name: b-studios/idris-effekt

max_forks_repo_name: b-studios/idris-effekt


text:
module Set

%default total
%access private

public export
interface Set (s : Type -> Type) a where
  empty : s a
  insert : a -> s a -> s a
  member : a -> s a -> Bool


text:
module Crypto.Hash.MD5

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

export
data MD5 : Type where
  MkMD5 : MerkleDamgard 4 64 Bits32 -> MD5

k_table : Vect 64 Bits32
k_table =
  [ 0xd76aa478, 0xe8c7b756, 0x242070db, 0xc1bdceee
  , 0xf57c0faf, 0x4787c62a, 0xa8304613, 0xfd469501
  , 0x698098d8, 0x8b44f7af, 0xffff5bb1, 0x895cd7be
  , 0x6b901122, 0xfd987193, 0xa679438e, 0x49b40821
  , 0xf61e2562, 0xc040b340, 0x265e5a51, 0xe9b6c7aa
  , 0xd62f105d, 0x02441453, 0xd8a1e681, 0xe7d3fbc8
  , 0x21e1cde6, 0xc33707d6, 0xf4d50d87, 0x455a14ed
  , 0xa9e3e905, 0xfcefa3f8, 0x676f02d9, 0x8d2a4c8a
  , 0xfffa3942, 0x8771f681, 0x6d9d6122, 0xfde5380c
  , 0xa4beea44, 0x4bdecfa9, 0xf6bb4b60, 0xbebfbc70
  , 0x289b7ec6, 0xeaa127fa, 0xd4ef3085, 0x04881d05
  , 0xd9d4d039, 0xe6db99e5, 0x1fa27cf8, 0xc4ac5665
  , 0xf4292244, 0x432aff97, 0xab9423a7, 0xfc93a039
  , 0x655b59c3, 0x8f0ccc92, 0xffeff47d, 0x85845dd1
  , 0x6fa87e4f, 0xfe2ce6e0, 0xa3014314, 0x4e0811a1
  , 0xf7537e82, 0xbd3af235, 0x2ad7d2bb, 0xeb86d391 ]

s_table : Vect 64 (Fin 32)
s_table =
  [ 7, 12, 17, 22, 7, 12, 17, 22, 7, 12, 17, 22, 7, 12, 17, 22
  , 5,  9, 14, 20, 5,  9, 14, 20, 5,  9, 14, 20, 5,  9, 14, 20
  , 4, 11, 16, 23, 4, 11, 16, 23, 4, 11, 16, 23, 4, 11, 16, 23
  , 6, 10, 15, 21, 6, 10, 15, 21, 6, 10, 15, 21, 6, 10, 15, 21 ]

i_table : Vect 64 (Fin 16)
i_table =
  [ 0, 1,  2,  3,  4,  5,  6,  7,  8,  9, 10, 11, 12, 13, 14, 15
  , 1, 6, 11,  0,  5, 10, 15,  4,  9, 14,  3,  8, 13,  2,  7, 12
  , 5, 8, 11, 14,  1,  4,  7, 10, 13,  0,  3,  6,  9, 12, 15,  2
  , 0, 7, 14,  5, 12,  3, 10,  1,  8, 15,  6, 13,  4, 11,  2,  9 ]

s_k_table : Vect 64 (Fin 32, Bits32)
s_k_table = zip s_table k_table

md5_init_hash_values : Vect 4 Bits32
md5_init_hash_values = [ 0x67452301, 0xefcdab89, 0x98badcfe, 0x10325476 ]

md5_compress : (block : Vect 64 Bits8) -> (h : Vect 4 Bits32) -> Vect 4 Bits32
md5_compress block hash_values = zipWith (+) hash_values $ go (_ ** zip calc_m_g s_k_table) hash_values
  where
  calc_m_g : Vect 64 Bits32
  calc_m_g =
    let block' = map (from_le {a = Bits32} {n = 4}) $ group 16 4 block
    in map (\i => index i block') i_table
  loop : Bits32 -> Bits32 -> Bits32 -> Fin 32 -> Bits32 -> Bits32 -> Bits32 -> Bits32 -> Vect 4 Bits32
  loop f m_g k_i s_i a b c d =
    let f = f + a + k_i + m_g
        a = d
        d = c
        c = b
        b = b + rotl s_i f
    in [a, b, c, d]
  go : (n ** Vect n (Bits32, Fin 32, Bits32)) -> Vect 4 Bits32 -> Vect 4 Bits32
  go (Z ** []) abcd = abcd
  go ((S n) ** ((i, s_i, k_i) :: xs)) [a, b, c, d] =
    case n `div` 16 of
      3 => go (n ** xs) $ loop (d `xor` (b .&. (c `xor` d)))    i k_i s_i a b c d
      2 => go (n ** xs) $ loop (c `xor` (d .&. (b `xor` c)))    i k_i s_i a b c d
      1 => go (n ** xs) $ loop (b `xor` c `xor` d)              i k_i s_i a b c d
      _ => go (n ** xs) $ loop (c `xor` (b .|. (complement d))) i k_i s_i a b c d

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

md5_finalize : MD5 -> Vect 16 Bits8
md5_finalize (MkMD5 s) =
  concat $ map (to_le {n = 4}) $
    case pad_theorem {block_nbyte = 64} {residue_max_nbyte = 55} {length_nbyte = 8} (LTESucc LTEZero) Refl s.buffer_nbyte_constraint s.buffer (integer_to_le _ $ 8 * (cast s.npassed_blocks * 64 + cast s.buffer_nbyte)) of
      Left block => md5_compress block s.hash_values
      Right blocks => let (x1, x2) = splitAt 64 blocks in md5_compress x2 $ md5_compress x1 s.hash_values

export
Digest MD5 where
  digest_nbyte = 16
  update = md5_update
  finalize = md5_finalize

export
Hash MD5 where
  block_nbyte = 64
  initialize = MkMD5 $ mk_merkle_damgard md5_init_hash_values


text:
module Main

import Types
import Consensus

%access public export

max_stars_repo_name: cwgoes/ibc-idris-ref

max_issues_repo_name: cwgoes/ibc-idris-ref

max_forks_repo_name: cwgoes/ibc-idris-ref


text:
palindromeLowered : String -> Bool
palindromeLowered str =
  let loweredStr = toLower str in
  loweredStr == reverse loweredStr

palindrome : Nat -> String -> Bool
palindrome len str =
  if length str > len
    then palindromeLowered str
    else False

max_stars_repo_name: jeremy-miller/type-driven-development

max_issues_repo_name: jeremy-miller/type-driven-development

max_forks_repo_name: jeremy-miller/type-driven-development


text:
module Data.Crypto.Hash.MD5

import Data.Bits
import Data.Vect

import Data.Crypto.Hash
import Data.Crypto.Util
import Data.Mod

%default total

||| INSECURE!
public export
data MessageDigest5 : Type where
  MD5 : Vect 4 (Bits 32) -> MessageDigest5

s : Vect 64 Nat
s = concat (map (concat . replicate 4)
                [[7, 12, 17, 22],
                 [5,  9, 14, 20],
                 [4, 11, 16, 23],
                 [6, 10, 15, 21]])

K : Vect 64 (Bits 32)
-- FIXME: `floor` is a `Double`, not integral.
-- K = map (\i => floor (abs (sin (i + 1)) * (2 `pow` 32))) [0..63]
K = map intToBits
        [0xd76aa478, 0xe8c7b756, 0x242070db, 0xc1bdceee,
         0xf57c0faf, 0x4787c62a, 0xa8304613, 0xfd469501,
         0x698098d8, 0x8b44f7af, 0xffff5bb1, 0x895cd7be,
         0x6b901122, 0xfd987193, 0xa679438e, 0x49b40821,
         0xf61e2562, 0xc040b340, 0x265e5a51, 0xe9b6c7aa,
         0xd62f105d, 0x02441453, 0xd8a1e681, 0xe7d3fbc8,
         0x21e1cde6, 0xc33707d6, 0xf4d50d87, 0x455a14ed,
         0xa9e3e905, 0xfcefa3f8, 0x676f02d9, 0x8d2a4c8a,
         0xfffa3942, 0x8771f681, 0x6d9d6122, 0xfde5380c,
         0xa4beea44, 0x4bdecfa9, 0xf6bb4b60, 0xbebfbc70,
         0x289b7ec6, 0xeaa127fa, 0xd4ef3085, 0x04881d05,
         0xd9d4d039, 0xe6db99e5, 0x1fa27cf8, 0xc4ac5665,
         0xf4292244, 0x432aff97, 0xab9423a7, 0xfc93a039,
         0x655b59c3, 0x8f0ccc92, 0xffeff47d, 0x85845dd1,
         0x6fa87e4f, 0xfe2ce6e0, 0xa3014314, 0x4e0811a1,
         0xf7537e82, 0xbd3af235, 0x2ad7d2bb, 0xeb86d391]

implementation Hash MessageDigest5 512 128 where
  initialize {m=m} {n=n} _ msg =
    let msgLength = m * n
    in let padSize = modToNat {n=512} (natToMod 448 - natToMod msgLength)
       in Basics.fst (partition' (append (concat msg)
                                         (or (shiftLeft (intToBits 64) (shiftRightLogical {n=512} (intToBits 1) (intToBits (cast (power 2 padSize)))))
                                             (intToBits (cast msgLength)))))
  initialContext _ = MD5 (map intToBits [0x67452301, 0xefcdab89, 0x98badcfe, 0x10325476])
  updateContext (MD5 [A, B, C, D]) chunk with (the (Vect 16 (Bits 32)) (partition chunk))
    | M = MD5 (zipWith plus [A, B, C, D] (foldl iteration [A, B, C, D] [0..63]))
    where iteration : Vect 4 (Bits 32) -> Fin 64 -> Vect 4 (Bits 32)
          iteration [A, B, C, D] i =
            let iNat = finToNat i
            in let (F, g) =
                     if iNat < 16
                     then ((B `and` C) `or` (complement B `and` D),
                           iNat `tightmod` 16)
                     else if iNat < 32
                          then ((D `and` B) `or` (complement D `and` C),
                                (iNat*5 + 1) `tightmod` 16)
                          else if iNat < 48
                               then (B `xor` (C `xor` D),
                                     (iNat*3 + 5) `tightmod` 16)
                               else (C `xor` (B `or` complement D),
                                     (iNat*7) `tightmod` 16)
               in [C,
                   B,
                   B `plus` rotateLeft (index i s)
                                       ((A `plus` F) `plus` (index i K `plus` index g M)),
                   D]
  finalize (MD5 context) = concat context

-- Tests

dummyMD5 : MessageDigest5
dummyMD5 = MD5 (map intToBits [0, 0, 0, 0])

-- shouldMatch_ : hashMessage {n=8} dummyMD5 [] = intToBits 0xd41d8cd98f00b204e9800998ecf8427e
-- shouldMatch_ = Refl

shouldMatch_a : hashMessage dummyMD5 (map (intToBits {n=8}) [97]) = intToBits 0x0cc175b9c0f1b6a831c399e269772661
shouldMatch_a = Refl

shouldMatch_abc : hashMessage dummyMD5 (map (intToBits {n=8}) [97, 98, 99]) = intToBits 0x900150983cd24fb0d6963f7d28e17f72
shouldMatch_abc = Refl

max_stars_repo_name: idris-hackers/idris-crypto

max_issues_repo_name: idris-hackers/idris-crypto

max_forks_repo_name: idris-hackers/idris-crypto


text:
module Test

import Books

test : String
test = comicBook

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
module Data.Ref

import public Data.IORef
import public Control.Monad.ST

%default total

public export
interface Ref m r | m where
  newRef : {0 a : Type} -> a -> m (r a)
  readRef : {0 a : Type} -> r a -> m a
  writeRef : r a -> a -> m ()

export
HasIO io => Ref io IORef where
  newRef = newIORef
  readRef = readIORef
  writeRef = writeIORef

export
Ref (ST s) (STRef s) where
  newRef = newSTRef
  readRef = readSTRef
  writeRef = writeSTRef


text:
%default total
data InfIO : Type where
     Do : IO a -> (a -> Inf InfIO) -> InfIO

(>>=) : IO a -> (a -> Inf InfIO) -> InfIO
(>>=) = Do

greet : InfIO
greet = do putStr "Enter your name: "
           name <- getLine
           putStrLn ("Hello" ++ name)
           greet


text:
module Main
import Data.Vect

public export

len : Vect n a -> Int
len {n=Z} [] = 0
len {n=S k} (with Vect x::xs) = 1 + len xs

v : Vect ?n Int
v = [1, 2, 3]

main : IO ()
main = do
    putStrLn . show $ len v
    putStrLn .show  $ with List ["a"]
    pure ()

max_stars_repo_name: thautwarm/idris-cam

max_issues_repo_name: thautwarm/idris-cam

max_forks_repo_name: thautwarm/idris-cam


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

Eq e => Eq (Vect n e) where
  (==) Nil Nil = True
  (==) (x :: xs) (y :: ys) = (x == y) && (xs == ys)
  (==) _ _ = False

Foldable (Vect n) where
  foldr f acc [] = acc
  foldr f acc (x :: xs) = f x (foldr f acc xs)

max_stars_repo_name: JnxF/advanced-software-analysis

max_issues_repo_name: JnxF/advanced-software-analysis

max_forks_repo_name: JnxF/advanced-software-analysis


text:
module System.Future

%default total

-- Futures based Concurrency and Parallelism

export
data Future : Type -> Type where [external]

%extern prim__makeFuture : {0 a : Type} -> Lazy a -> Future a

%foreign "scheme:blodwen-await-future"
prim__awaitFuture : {0 a : Type} -> Future a -> a

export
fork : Lazy a -> Future a
fork = prim__makeFuture

export
await : Future a -> a
await f = prim__awaitFuture f

public export
Functor Future where
  map func future = fork $ func (await future)

public export
Applicative Future where
  pure v = fork v
  funcF <*> v = fork $ (await funcF) (await v)

public export
Monad Future where
  join = map await
  v >>= func = join . fork $ func (await v)

export
performFutureIO : HasIO io => Future (IO a) -> io (Future a)
performFutureIO = primIO . prim__io_pure . map unsafePerformIO

export
forkIO : HasIO io => IO a -> io (Future a)
forkIO a = performFutureIO $ fork a


text:
module Main

main : IO ()
main = putStrLn "Happy New Year 1396"

max_stars_repo_name: AliMD/happy-new-year

max_issues_repo_name: AliMD/happy-new-year

max_forks_repo_name: AliMD/happy-new-year


text:
module ZZUtils
import ZZ
import NatUtils
%access public export
%default total

data IsNonNegative : ZZ->Type where
 NonNegative :(IsNonNegative (Pos k))

data NotBothZeroZ :ZZ->ZZ->Type where
  LeftPositive :NotBothZeroZ (Pos (S k)) m
  LeftNegative :NotBothZeroZ (NegS k) m
  RightPositive :NotBothZeroZ m (Pos (S k))
  RightNegative :NotBothZeroZ m (NegS k)

data NotZero:ZZ->Type where
  PositiveZ:NotZero (Pos (S k))
  NegativeZ:NotZero (NegS k)

|||Proof that negative integers are not non negative
negsAreNotNonNegs:(IsNonNegative (NegS k))->Void
negsAreNotNonNegs NonNegative impossible
|||A function that checks whether an integer is non negative and returns a
|||proof or a contradiction
decideIsNonNeg:(a: ZZ) -> Dec (IsNonNegative   a)
decideIsNonNeg (Pos k) = Yes NonNegative
decideIsNonNeg (NegS k) = No (negsAreNotNonNegs)
|||Proof that natural numbers are non negative
naturalsNonNegative: (x:Nat)->IsNonNegative (Pos x)
naturalsNonNegative x = NonNegative

|||The less than type for ZZ
LTZ :ZZ->ZZ->Type
LTZ a b = LTEZ (1+a) b

|||Theorem that if a and b are natural numbers and a<b
|||then, (Pos a) <(Pos b)
ltNatToZZ:{a:Nat}->{b:Nat}->(LT a b)->(LTZ (Pos a) (Pos b))
ltNatToZZ (LTESucc x) = PositiveLTE (LTESucc x)
|||Multiplying positive numbers gives a positive number.
posMultPosIsPos: (IsPositive m)->(IsPositive d)->(IsPositive (m*d))
posMultPosIsPos{m = (Pos (S k))}{d = (Pos (S j))} Positive Positive = Positive
|||The theorem that (-a)*(-b)=a*b
negateMultNegateNeutralZ: {a:ZZ}->{b:ZZ}->((-a)*(-b)=a*b)
negateMultNegateNeutralZ{a}{b} =
  rewrite (multNegateRightZ (-a) b) in
  rewrite (multNegateLeftZ a b ) in
  rewrite (doubleNegElim (a*b)) in Refl
|||Proof that zero times an integer is not positive
posIsNotZeroTimesInteger:((Pos (S k))=(Pos Z)*a)->Void
posIsNotZeroTimesInteger{a = (Pos _)} Refl impossible
posIsNotZeroTimesInteger{a = (NegS _)} Refl impossible
|||Proof that Zero times an integer is not negative
negSIsNotZeroTimesInteger :((NegS k)=(Pos Z)*a)->Void
negSIsNotZeroTimesInteger {a = (Pos _)} Refl impossible
negSIsNotZeroTimesInteger {a = (NegS _)} Refl impossible
|||Converts a nonNegative integer into the corresponding Natural number
nonNegIntegerToNat:(a:ZZ)->(IsNonNegative a)->Nat
nonNegIntegerToNat (Pos k) NonNegative = k


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

public export
record First (a : Type) where
  constructor MkFirst
  getFirst : Maybe a

public export
Semigroup (First a) where
  (MkFirst f) <+> r = case f of
                        Nothing => r
                        Just x  => MkFirst f

public export
Monoid (First a) where
  neutral = MkFirst Nothing


text:
module Main

import Js.Dom
import Control.ST
import Control.ST.ImplicitCall

Gui : Dom m => Type
Gui {m} = DomRef {m} () (const String) (const String) ()

vw : () -> String -> Html String
vw () s = div [] [input [onchange id], div [] [text s]]

pageLoop : Dom m => (d: Var) -> (s:Var) -> ST m () [s:::State String, d:::Gui {m}]
pageLoop d s =
  do
    x <- getInput d
    domPut d x
    pageLoop d s

page : Dom m => ST m () []
page =
  do
    dom <- initBody [] vw () "ola"
    txt <- new ""
    pageLoop dom txt
    delete txt
    clearDom dom

main : JS_IO ()
main = setASync_ $ run page

max_stars_repo_name: rbarreiro/idrisjs

max_issues_repo_name: prozacchiwawa/idrisjs

max_forks_repo_name: prozacchiwawa/idrisjs


text:
||| Module for the parsing and encoding LSP messages, updated to version 3.16.
|||
||| References:
|||   [1] https://microsoft.github.io/language-server-protocol/specifications/specification-3-16/
|||
||| (C) The Idris Community, 2021
module Language.LSP.Message

import public Language.LSP.Message.CallHierarchy
import public Language.LSP.Message.Cancel
import public Language.LSP.Message.ClientCapabilities
import public Language.LSP.Message.CodeAction
import public Language.LSP.Message.CodeLens
import public Language.LSP.Message.Command
import public Language.LSP.Message.Completion
import public Language.LSP.Message.Declaration
import public Language.LSP.Message.Definition
import public Language.LSP.Message.Derive
import public Language.LSP.Message.Diagnostics
import public Language.LSP.Message.DocumentColor
import public Language.LSP.Message.DocumentFormatting
import public Language.LSP.Message.DocumentHighlight
import public Language.LSP.Message.DocumentLink
import public Language.LSP.Message.DocumentSymbols
import public Language.LSP.Message.FoldingRange
import public Language.LSP.Message.Hover
import public Language.LSP.Message.Implementation
import public Language.LSP.Message.Initialize
import public Language.LSP.Message.LinkedEditingRange
import public Language.LSP.Message.Location
import public Language.LSP.Message.Markup
import public Language.LSP.Message.Message
import public Language.LSP.Message.Method
import public Language.LSP.Message.Moniker
import public Language.LSP.Message.Progress
import public Language.LSP.Message.References
import public Language.LSP.Message.Registration
import public Language.LSP.Message.RegularExpressions
import public Language.LSP.Message.Rename
import public Language.LSP.Message.SelectionRange
import public Language.LSP.Message.SemanticTokens
import public Language.LSP.Message.ServerCapabilities
import public Language.LSP.Message.SignatureHelp
import public Language.LSP.Message.TextDocument
import public Language.LSP.Message.Trace
import public Language.LSP.Message.URI
import public Language.LSP.Message.Utils
import public Language.LSP.Message.Window
import public Language.LSP.Message.Workspace


text:
module MergeSortView

import Data.List.Views
import Data.Nat.Views
import Data.Vect
import Data.Vect.Views

mergeSort : Ord a => List a -> List a
mergeSort xs with (splitRec xs)
  mergeSort [] | SplitRecNil = []
  mergeSort [x] | SplitRecOne = [x]
  mergeSort (lefts ++ rights) | (SplitRecPair lrec rrec) = merge (mergeSort lefts | lrec) (mergeSort rights | rrec)

-- 10.2 Ex # 1
total
equalSuffix : Eq a => List a -> List a -> List a
equalSuffix xs ys with (snocList xs)
  equalSuffix [] ys | Empty = []
  equalSuffix (zs ++ [x]) ys | (Snoc rec) with (snocList ys)
    equalSuffix (zs ++ [x]) [] | (Snoc rec) | Empty = []
    equalSuffix (zs ++ [x]) (xs ++ [y]) | (Snoc zsrec) | (Snoc xsrec) = case x == y of
                                                                       False => []
                                                                       True => equalSuffix zs xs | zsrec | xsrec ++ [x]

-- 10.2 Ex # 2
total
vmergeSort : Ord a => Vect n a -> Vect n a
vmergeSort xs with (splitRec xs)
  vmergeSort [] | SplitRecNil = []
  vmergeSort [x] | SplitRecOne = [x]
  vmergeSort (lefts ++ rights) | (SplitRecPair lrec rrec) = merge (vmergeSort lefts | lrec) (vmergeSort rights | rrec)

-- 10.2 Ex # 3
total
toBinary : Nat -> String
toBinary k with (halfRec k)
  toBinary Z | HalfRecZ = ""
  toBinary (n + n) | (HalfRecEven rec) = toBinary n | rec ++ "0"
  toBinary (S (n + n)) | (HalfRecOdd rec) = toBinary n | rec ++ "1"

-- 10.2 Ex # 4
total
palindrome : Eq a => List a -> Bool
palindrome xs with (vList xs)
  palindrome [] | VNil = True
  palindrome [x] | VOne = True
  palindrome (x :: (ys ++ [y])) | (VCons rec) = case x == y of
                                                     False => False
                                                     True => palindrome ys | rec


text:
record Score where
       constructor MkScore
       correct : Nat
       attempted : Nat

record GameState where
       constructor MkGameState
       score : Score
       difficulty : Nat

Show GameState where
    show st = show (correct (score st)) ++ "/"
              ++ show (attempted (score st)) ++ "\n"
              ++ "Difficulty: " ++ show (difficulty st)

initState : GameState
initState = MkGameState (MkScore 0 0) 12

-- Test record update syntax

correct : GameState -> GameState
correct = record { score->correct $= (+1),
                   score->attempted $= (+1) }

wrong : GameState -> GameState
wrong = record { score->attempted $= (+1) }

restart : GameState -> GameState
restart = record { score->attempted = 0,
                   score->correct = 0 }

main : IO ()
main = do let st = initState
          let st' = correct st
          let st'' = wrong st'
          printLn st''
          printLn (restart st'')

max_stars_repo_name: grin-compiler/idris-grin

max_issues_repo_name: grin-compiler/idris-grin

max_forks_repo_name: grin-compiler/idris-grin