text:
module Data.Matrix.LinearCombinations

import Control.Algebra
import Control.Algebra.VectorSpace -- definition of module
import Classes.Verified -- definition of verified algebras other than modules
import Control.Algebra.DiamondInstances
import Data.Matrix
import Data.Matrix.Algebraic -- module instances; from Idris 0.9.20

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

import Data.ZZ

import Control.Algebra.ZZVerifiedInstances
import Data.Matrix.AlgebraicVerified

%default total

monoidsum : (Foldable t, Monoid a) => t a -> a
{-
-- Idris version 0.9.18
monoidsum = Control.Algebra.sum
-}
-- Idris version 0.9.20
monoidsum = sum'
--

{-
Basic theorems regarding
* Abelian groups
* Vect _ _
* Matrix _ _ _
* Vect _ ZZ
	ideally generalized from ZZ to other verified rings
* Matrix _ _ ZZ
	ideally generalized from ZZ to other verified rings
-}

doubleSumInnerSwap : VerifiedAbelianGroup t => (a, b, c, d : t) -> (a<+>b)<+>(c<+>d) = (a<+>c)<+>(b<+>d)
doubleSumInnerSwap a b c d = trans (sym $ semigroupOpIsAssociative a b (c<+>d))
	$ trans ( cong {f=(a<+>)} $ trans (semigroupOpIsAssociative b c d)
		$ trans (cong {f=(<+>d)} $ abelianGroupOpIsCommutative b c)
		$ sym $ semigroupOpIsAssociative c b d)
	$ semigroupOpIsAssociative a c (b<+>d)

doubleSumInnerSwap_Vect : VerifiedRingWithUnity t => (a, b, c, d : Vect n t)
	-> (a<+>b)<+>(c<+>d) = (a<+>c)<+>(b<+>d)
doubleSumInnerSwap_Vect a b c d = trans (sym $ semigroupOpIsAssociative_Vect a b (c<+>d))
	$ trans ( cong {f=(a<+>)} $ trans (semigroupOpIsAssociative_Vect b c d)
		$ trans (cong {f=(<+>d)} $ abelianGroupOpIsCommutative_Vect b c)
		$ sym $ semigroupOpIsAssociative_Vect c b d)
	$ semigroupOpIsAssociative_Vect a c (b<+>d)

total
lemma_VectAddHead : (v, w : Vect (S n) ZZ) -> head(v<+>w) = (head v)<+>(head w)
lemma_VectAddHead (vv::vvs) (ww::wws) = Refl

total
matrixAddHead : (x, y : Matrix (S predn) m ZZ) -> Vect.head (x<+>y) = (Vect.head x)<+>(Vect.head y)
matrixAddHead (x::xs) (y::ys) = Refl

total
lemma_VectAddTail : (x, y : Vect (S predn) ZZ) -> Vect.tail (x<+>y) = (Vect.tail x)<+>(Vect.tail y)
lemma_VectAddTail (x::xs) (y::ys) = Refl

total
matrixAddTail : (x, y : Matrix (S predn) m ZZ) -> Vect.tail (x<+>y) = (Vect.tail x)<+>(Vect.tail y)
matrixAddTail (x::xs) (y::ys) = Refl

lemma_VectAddEntrywise : .{n : Nat} -> (ni : Fin n) -> (v, w : Vect n ZZ) -> index ni (v<+>w) = (index ni v)<+>(index ni w)
{-
-- -- This proof follows the structure of `index`'s definition
--
-- without ni arg: (.) void FinZAbsurd; >> No such variable __pi_arg7; seems a silly failure of type inference
lemma_VectAddEntrywise {n=Z} ni = void $ FinZAbsurd ni
lemma_VectAddEntrywise FZ = ?lemma_VectAddEntrywise_rhs_1
lemma_VectAddEntrywise (FS npredi) = ?lemma_VectAddEntrywise_rhs_2
lemma_VectAddEntrywise_rhs_1 = proof
  intros
  rewrite sym (indexFZIsheadValued {xs=v})
  rewrite sym (indexFZIsheadValued {xs=w})
  exact (rewrite (indexFZIsheadValued {xs=v<+>w}) in (lemma_VectAddHead v w))
lemma_VectAddEntrywise_rhs_2 = proof
	intros
	claim indpred ( (r : ZZ) -> (rs : Vect k ZZ) -> index (FS npredi) (r::rs) = index npredi rs )
	-- ^ trivial
	unfocus
	{-
	-- No-opping stuff demonstrating the problem how the thm fails
	rewrite sym ( indpred (head $ v<+>w) (tail $ v<+>w) )
	rewrite sym ( indpred (head v) (tail v) )
	rewrite sym ( indpred (head w) (tail w) )
	-}
	rewrite sym ( the (v = (head v)::(tail v)) Refl )
	>> When checking argument value to function Prelude.Basics.the:
        Unifying v and head v :: tail v would lead to infinite value
-}
-- -- Alternative proof (>points):
lemma_VectAddEntrywise {n=Z} ni v w = void $ FinZAbsurd ni
lemma_VectAddEntrywise FZ (vv::vvs) (ww::wws) = Refl
lemma_VectAddEntrywise (FS npredi) (vv::vvs) (ww::wws) = lemma_VectAddEntrywise npredi vvs wws

monoidrec1D : {v : ZZ} -> {vs : Vect n ZZ} -> monoidsum (v::vs) = v <+> monoidsum vs
monoidrec1D = monoidrec _ _

monoidrec2D : {v : Vect m ZZ} -> {vs : Vect n (Vect m ZZ)} -> monoidsum (v::vs) = v <+> (monoidsum vs)
monoidrec2D = monoidrec _ _

total
headOfSumIsSumOfHeadsArg : ((v : Vect (S n) ZZ) ->
                    (w : Vect (S n) ZZ) -> head (v <+> w) = head v <+> head w) -> (xs : Vect (S m) (Vect (S n) ZZ)) -> head (monoidsum xs) = monoidsum (map head xs)
headOfSumIsSumOfHeadsArg {n} pr (v::[]) = rewrite sym (pr v (replicate (S n) (Pos 0))) in Refl
headOfSumIsSumOfHeadsArg {m = S m'} {n} pr (v::(vsv::vss)) = conclusion3
	where
		vs : Vect (S m') (Vect (S n) ZZ)
		vs = vsv::vss
		imedform0: monoidsum (map head (v::vs)) = monoidsum ( (head v) :: (map head vs) )
		imedform0 = cong {f=monoidsum} (mapheadrec {v=v} {vs=vs})
		recappl : monoidsum (map head (v::vs)) = head v <+> monoidsum (map head vs)
		recappl = trans imedform0 (the (monoidsum ( (head v) :: (map head vs) ) = (head v) <+> monoidsum (map head vs) ) monoidrec1D)
		imedform1 : head (monoidsum (v::vs)) = head ( v <+> monoidsum vs )
		{-
		original: imedform1 = cong {f=head} monoidrec2D
		Spurious type mismatch error results. monoidrec2D is assumed the wrong implicit args, perhaps, or else one of the foldrImpl gets one recursion rewrite instead of none.
		-}
		imedform1 = cong {f=head} (monoidrec2D {v=v} {vs=vs})
		homomorphismapply : head (monoidsum (v::vs)) = head v <+> (head (monoidsum vs))
		homomorphismapply = trans imedform1 (lemma_VectAddHead v (monoidsum vs))
		conclusion0 : (head (monoidsum (v::vs)) = head v <+> (head (monoidsum vs)), head v <+> monoidsum (map head vs) = monoidsum (map head (v::vs)))
		conclusion0 = (homomorphismapply, sym recappl)
		conclusion1 : head (monoidsum vs) = monoidsum (map head vs) -> (head (monoidsum (v::vs)) = head v <+> monoidsum (map head vs), head v <+> monoidsum (map head vs) = monoidsum (map head (v::vs)))
		conclusion1 pr = (rewrite sym pr in homomorphismapply, sym recappl)
		conclusion2 : head (monoidsum vs) = monoidsum (map head vs) -> head (monoidsum (v::vs)) = monoidsum (map head (v::vs))
		conclusion2 pr = uncurry trans (conclusion1 pr)
		-- bizarrely, this does not work
		-- conclusion2 pr = trans (rewrite sym pr in homomorphismapply) (sym recappl)
		proof0 : head (monoidsum vs) = monoidsum (map head vs)
		proof0 = headOfSumIsSumOfHeadsArg pr vs
		conclusion3 : head (monoidsum (v::vs)) = monoidsum (map head (v::vs))
		conclusion3 = conclusion2 proof0

total
headOfSumIsSumOfHeads : (xs : Vect m (Vect (S n) ZZ)) -> head (monoidsum xs) = monoidsum (map head xs)
headOfSumIsSumOfHeads {m=Z} [] = Refl
headOfSumIsSumOfHeads {m=S m} xs = headOfSumIsSumOfHeadsArg lemma_VectAddHead xs
{-
-- This should work but is picky.
headOfSumIsSumOfHeads {m=Z} xs = trans zveqpr (sym $ trans bandy bundy)
	where
		bandy : (the (Vect Z ZZ -> ZZ) monoidsum) (map head xs) = monoidsum (map head Data.Vect.Nil)
		-- bandy = trans ( sym $ trans ( cong {f=monoidsum . (map head)} (the ([]=xs) zeroVecEq) ) ( the ((monoidsum . (map head)) $ xs = monoidsum (map head xs)) Refl ) ) (the ((monoidsum . map head) [] = monoidsum (map Data.Vect.head Data.Vect.Nil)) Refl)
		bundy : monoidsum (map Data.Vect.head Data.Vect.Nil) = Pos Z
		bundy = Refl
		zveqpr : Data.Vect.head $ monoidsum xs = monoidsum (map Data.Vect.head xs)
		zveqpr = ?zveqpr'
		zveqpr' = proof
			rewrite sym (the (xs=[]) zeroVecEq)
			trivial
-}
{-
-- Works in REPL
headOfSumIsSumOfHeads {m=Z} = ?headOfSumIsSumOfHeads_Z_pr
headOfSumIsSumOfHeads_Z_pr = proof
  intros
  let bandy = trans ( sym $ trans ( cong {f=monoidsum . (map head)} (the ([]=xs) zeroVecEq) ) ( the ((monoidsum . (map head)) $ xs = monoidsum (map head xs)) Refl ) ) (the ((monoidsum . map head) [] = monoidsum (map Data.Vect.head Data.Vect.Nil)) Refl)
  unfocus
  unfocus
  unfocus
  unfocus
  unfocus
  search
  search
  search
  let bundy = the (monoidsum (map Data.Vect.head Data.Vect.Nil) = Pos Z) $ Refl
  exact trans _ (sym $ trans bandy bundy)
  unfocus
  unfocus
  rewrite sym (the (xs=[]) zeroVecEq)
  trivial
  exact n
  exact n
-}

tailOfSumIsSumOfTails :
	{vs : Matrix n (S predw) ZZ}
	-> tail (monoidsum vs) = monoidsum (map tail vs)
tailOfSumIsSumOfTails {vs=[]} = Refl
tailOfSumIsSumOfTails {vs=v::vs} =
	trans ( cong {f=tail} monoidrec2D )
	$ trans ( lemma_VectAddTail _ _ )
	$ trans ( cong {f=(<+>) (tail v)} $ tailOfSumIsSumOfTails {vs=vs} )
	$ sym $ monoidrec2D

total
dotproductRewrite : {v : Vect _ ZZ} -> v <:> w = monoidsum (zipWith (<.>) v w)
dotproductRewrite = Refl

{-
Central theorems:
* timesVectMatAsLinearCombo
* timesMatMatAsMultipleLinearCombos
-}

timesMatMatAsTVecMat_EntryChariz : (vs : Matrix (S n') n ZZ) -> (xs : Matrix n w ZZ) -> Data.Vect.head (vs <> xs) = (Data.Vect.head vs) <\> xs
timesMatMatAsTVecMat_EntryChariz vs [] = ?timesMatMatAsTVecMat_EntryCharizTriv
timesMatMatAsTVecMat_EntryChariz vs (xx::xxs) = ?timesMatMatAsTVecMat_EntryChariz'

timesMatMatAsTVecMat_EntryCharizTriv = proof
  intros
  rewrite sym $ headtails vs
  rewrite sym $ zeroVecVecId vs
  exact Refl

timesMatMatAsTVecMat_EntryChariz' = proof
  intros
  rewrite sym $ headtails vs
  exact Refl

total
zippyLemA : (the (Vect 0 ZZ) []) <\> (the (Matrix 0 w ZZ) []) = replicate w (Pos 0)
zippyLemA {w = Z} = Refl
zippyLemA {w = S n} = cong (zippyLemA {w=n})

total
zippyLemB : replicate w (Pos 0) = monoidsum (zipWith (<#>) (the (Vect 0 ZZ) []) (the (Matrix 0 w ZZ) []))
zippyLemB {w = Z} = Refl
zippyLemB {w = S n} = cong (zippyLemB {w=n})

timesVectMatAsLinearCombo_EntryCharizLeft : (v : Vect n ZZ) -> (xs : Matrix n (S predw) ZZ) -> head (v <\> xs) = monoidsum $ zipWith (*) v (map head xs)
timesVectMatAsLinearCombo_EntryCharizLeft [] [] = Refl
-- Order of definitions issue - below line should be uncommented, line below it eliminated along with proof, and this whole section moved below the definition of timesVectMatAsHeadTail_ByTransposeElimination, requiring many declarations to move.
-- timesVectMatAsLinearCombo_EntryCharizLeft (vv::vvs) (xx::xxs) = cong {f=head} $ timesVectMatAsHeadTail_ByTransposeElimination {scals=(vv::vvs)} {vects=(xx::xxs)}
timesVectMatAsLinearCombo_EntryCharizLeft (vv::vvs) (xx::xxs) = ?timesVectMatAsLinearCombo_EntryCharizLeft'

-- Reduce addition over (Vect n ZZ) to entrywise addition over ZZ to change (head.monoidsum) into (monoidsum.(map head)).
timesVectMatAsLinearCombo_EntryCharizRight : (v : Vect n ZZ) -> (xs : Matrix n (S predw) ZZ) -> monoidsum $ zipWith (*) v (map head xs) = head $ monoidsum (zipWith (<#>) v xs)
timesVectMatAsLinearCombo_EntryCharizRight [] [] = Refl
timesVectMatAsLinearCombo_EntryCharizRight (vv::vvs) (xx::xxs) = ?timesVectMatAsLinearCombo_EntryCharizRight'
{-
Writing the proof as direct processing of equalities, rather than in the shell, resulted in tragedy.

timesVectMatAsLinearCombo_EntryCharizRight (vv::vvs) (xx::xxs) = sym $ reductComposition putHeadInside reduceMultUnderHeadTo1D
	where
		putHeadInside : Data.Vect.head (monoidsum (zipWith (<#>) (vv::vvs) (xx::xxs))) = monoidsum (map head (zipWith (<#>) (vv::vvs) (xx::xxs)))
		putHeadInside = headOfSumIsSumOfHeads (zipWith (<#>) (vv::vvs) (xx::xxs))
		reduceMultUnderHeadTo1D : map head (zipWith (<#>) (vv::vvs) (xx::xxs)) = zipWith (*) (vv::vvs) (map head (xx::xxs))
		reduceMultUnderHeadTo1D = ?reduceMultUnderHeadTo1D'
		reductComposition : head (monoidsum (zipWith (<#>) (vv::vvs) (xx::xxs))) = monoidsum (map head (zipWith (<#>) (vv::vvs) (xx::xxs))) -> map head (zipWith (<#>) (vv::vvs) (xx::xxs)) = zipWith (*) (vv::vvs) (map head (xx::xxs)) -> head (monoidsum (zipWith (<#>) (vv::vvs) (xx::xxs))) = monoidsum (zipWith (*) (vv::vvs) (map head (xx::xxs)))
		reductComposition pr0 pr1 = ?reductComposition'
		{-
		For some reason, trying any of these proofs makes Idris claim (vv) is expected to be a (Nat).

		composeReducts = rewrite sym reduceMultUnderHeadTo1D in putHeadInside
		composeReducts = trans putHeadInside (cong {f=monoidsum} reduceMultUnderHeadTo1D)
		-}
		-- composeReducts : head (monoidsum (zipWith (<#>) (vv::vvs) (xx::xxs))) = monoidsum (zipWith (*) (vv::vvs) (map head (xx::xxs)))
		-- composeReducts = reductComposition putHeadInside reduceMultUnderHeadTo1D
-}

reduceMultUnderHeadTo1D : {xxs : Matrix n (S m) ZZ} -> map Data.Vect.head (zipWith (<#>) (vv::vvs) (xx::xxs)) = zipWith (the (ZZ -> ZZ -> ZZ) (*)) (vv::vvs) (map Data.Vect.head (xx::xxs))
reduceMultUnderHeadTo1D {n=Z} {vv} {xx}
	= vecHeadtailsEq (headMapChariz {xs=xx}) zeroVecEq
reduceMultUnderHeadTo1D {n=S predn} {vv} {xx} {vvs} {xxs}
	= vecHeadtailsEq (headMapChariz {f=multZ vv} {xs=xx})
	$ rewrite headtails vvs in rewrite headtails xxs in
	reduceMultUnderHeadTo1D {vv=head vvs} {vvs=tail vvs} {xx=head xxs} {xxs=tail xxs}

timesVectMatAsLinearCombo_EntryCharizRight' = proof
  intros
  claim putHeadInside head (monoidsum (zipWith (<#>) (vv::vvs) (xx::xxs))) = monoidsum (map head (zipWith (<#>) (vv::vvs) (xx::xxs)))
  unfocus
  exact sym $ trans putHeadInside (cong {f=monoidsum} $ reduceMultUnderHeadTo1D {vv=vv} {xx=xx})
  exact headOfSumIsSumOfHeads (zipWith (<#>) (vv::vvs) (xx::xxs))

timesVectMatAsLinearCombo_EntryChariz : (v : Vect n ZZ) -> (xs : Matrix n (S predw) ZZ) -> head (v <\> xs) = head $ monoidsum (zipWith (<#>) v xs)
timesVectMatAsLinearCombo_EntryChariz v xs = trans (timesVectMatAsLinearCombo_EntryCharizLeft v xs) (timesVectMatAsLinearCombo_EntryCharizRight v xs)

transParaphraseGeneral0 : (vs : Matrix n (S predw) ZZ) -> transpose vs = (head $ transpose vs) :: (tail $ transpose vs)
transParaphraseGeneral0 vs = headtails (transpose vs)

transposeNTail2 : {xs : Matrix n (S predw) ZZ} -> tail $ transpose xs = transpose $ map tail xs
transposeNTail2 = ?transposeNTail2'
transposeNTail2' = proof
  intros
  rewrite sym (sym $ transposeIsInvolution {xs=tail (transpose xs)})
  exact cong {f=transpose} transposeNTail

transParaphraseGeneral1 : (vs : Matrix n (S predw) ZZ) -> transpose vs = (map Data.Vect.head vs) :: ( transpose $ map Data.Vect.tail vs )
transParaphraseGeneral1 {n} {predw} vs = ?transParaphraseGeneral1'

transParaphraseGeneral1' = proof
  intros
  rewrite sym (transParaphraseGeneral0 vs)
  rewrite sym (transposeNTail2 {xs=vs})
  rewrite sym (transposeNHead {xs=vs})
  exact Refl

observationTransposeFormInMult0 : {vects : Matrix n (S predw) ZZ} -> scals <\> vects = map (\ARG => scals <:> ARG) ( (map Data.Vect.head vects) :: ( transpose $ map Data.Vect.tail vects ) )
observationTransposeFormInMult0 {scals} {vects} = cong {f=map (\ARG => scals <:> ARG)} (transParaphraseGeneral1 vects)

observationTransposeFormInMult1 : {vects : Matrix n (S predw) ZZ} -> scals <\> vects = ( scals <:> (map Data.Vect.head vects) ) :: map (\ARG => scals <:> ARG) ( transpose $ map Data.Vect.tail vects )
observationTransposeFormInMult1 = observationTransposeFormInMult0

{-
Recurses over the inner dimension of the matrix.
Hence, reduces (timesVectMatAsLinearCombo scals vects) to the cases ( timesVectMatAsLinearCombo (_::_) ([] :: _) )
-}
timesVectMatAsHeadTail_ByTransposeElimination : {vects : Matrix n (S predw) ZZ} -> scals <\> vects = (scals <:> map Data.Vect.head vects) :: ( scals <\> map Data.Vect.tail vects )
timesVectMatAsHeadTail_ByTransposeElimination = observationTransposeFormInMult1

compressMonoidsum_lem1 : {vects : Matrix n (S predw) ZZ} -> monoidsum ( zipWith (<.>) scals (map Data.Vect.head vects) ) :: monoidsum ( zipWith (<#>) scals (map Data.Vect.tail vects) ) = ( head $ monoidsum ( zipWith (<#>) scals vects ) ) :: monoidsum ( zipWith (<#>) scals (map Data.Vect.tail vects) )
compressMonoidsum_lem1 {scals} {vects} = cong {f=(:: monoidsum ( zipWith (<#>) scals (map Data.Vect.tail vects) ) )} (timesVectMatAsLinearCombo_EntryCharizRight scals vects)

compressMonoidsum_lem2 : {n : Nat} -> {scals : Vect n ZZ} -> {predw : Nat} -> {vects : Vect n (Vect (S predw) ZZ)} -> Data.Vect.(::) (Data.Vect.head $ monoidsum ( zipWith (<#>) scals vects )) ( monoidsum ( zipWith (<#>) scals (map Data.Vect.tail vects) ) ) = monoidsum ( zipWith (<#>) scals vects )
compressMonoidsum_lem2 = ?compressMonoidsum_lem2'

rewriteZipWithUnderTail : {scals : Vect n ZZ} -> {vects : Matrix n (S predw) ZZ} -> map Data.Vect.tail $ Data.Vect.zipWith (<#>) scals vects = Data.Vect.zipWith (<#>) scals (map Data.Vect.tail vects)
rewriteZipWithUnderTail {scals=[]} {vects=[]} = Refl
rewriteZipWithUnderTail {scals=z::zs} {vects=v::vs}
	= vecHeadtailsEq
		(rewrite headtails v in Refl)
	$ rewriteZipWithUnderTail {scals=zs} {vects=vs}

compressMonoidsum_lem3 : {n : Nat} -> {scals : Vect n ZZ} -> {predw : Nat} -> {vects : Vect n (Vect (S predw) ZZ)} -> monoidsum ( zipWith (<#>) scals (map Data.Vect.tail vects) ) = tail $ monoidsum ( zipWith (<#>) scals vects )
compressMonoidsum_lem3 {predw=Z} {n} = zeroVecEq
compressMonoidsum_lem3 {predw=S predpredw} {n=Z} = ?compressMonoidsum_lem3_rhs_majZ
compressMonoidsum_lem3 {predw=S predpredw} {n=S predn} {scals} {vects} = trans (cong {f=monoidsum} $ sym rewriteZipWithUnderTail) (sym tailOfSumIsSumOfTails)

compressMonoidsum_lem3_rhs_majZ = proof
  intros
  rewrite sym $ the (scals=[]) zeroVecEq
  rewrite sym $ the (vects=[]) zeroVecEq
  trivial

compressMonoidsum_lem2' = proof
	intros
	rewrite sym (headtails $ monoidsum ( zipWith (<#>) scals vects ))
	exact (vectConsCong ( head (monoidsum (zipWith (<#>) scals vects)) ) _ _ compressMonoidsum_lem3)

compressMonoidsum : {vects : Matrix n (S predw) ZZ} -> monoidsum ( zipWith (<.>) scals (map Data.Vect.head vects) ) :: monoidsum ( zipWith (<#>) scals (map Data.Vect.tail vects) ) = monoidsum ( zipWith (<#>) scals vects )
compressMonoidsum = ?compressMonoidsum'

compressMonoidsum' = proof
	intros
	exact trans (compressMonoidsum_lem1 {scals=scals} {vects=vects}) compressMonoidsum_lem2

timesVectMatAsLinearCombo_EntryCharizLeft' = proof
  intros
  exact cong {f=head} $ timesVectMatAsHeadTail_ByTransposeElimination {scals=(vv::vvs)} {vects=(xx::xxs)}

timesVectMatAsLinearCombo :
	(v : Vect n ZZ) -> (xs : Matrix n w ZZ)
	-> ( v <\> xs = monoidsum (zipWith (<#>) v xs) )
timesVectMatAsLinearCombo [] [] = trans zippyLemA zippyLemB
timesVectMatAsLinearCombo zs xs {n=S predn} {w=Z} = zeroVecEq
timesVectMatAsLinearCombo zs xs {n=S predn} {w=S predw}
	= flip trans (compressMonoidsum {scals=zs} {vects=xs})
	$ trans (timesVectMatAsHeadTail_ByTransposeElimination {scals=zs} {vects=xs})
	$ vecHeadtailsEq dotproductRewrite
	$ timesVectMatAsLinearCombo zs (map Data.Vect.tail xs)

timesMatMatAsMultipleLinearCombos_EntryChariz : (vs : Matrix (S n') n ZZ) -> (xs : Matrix n w ZZ) -> Data.Vect.head (vs <> xs) = monoidsum $ zipWith (<#>) (Data.Vect.head vs) xs
timesMatMatAsMultipleLinearCombos_EntryChariz vs xs = rewrite sym (timesVectMatAsLinearCombo (head vs) xs) in (timesMatMatAsTVecMat_EntryChariz vs xs)

timesMatMatAsMultipleLinearCombos : (vs : Matrix n' n ZZ) -> (xs : Matrix n w ZZ) -> vs <> xs = map (\zs => monoidsum $ zipWith (<#>) zs xs) vs
timesMatMatAsMultipleLinearCombos [] xs = Refl
timesMatMatAsMultipleLinearCombos (v::vs) xs
	= trans ( headtails $ (v::vs)<>xs )
	$ vecHeadtailsEq ( timesMatMatAsMultipleLinearCombos_EntryChariz (v::vs) xs )
	$ timesMatMatAsMultipleLinearCombos vs xs

{-
* Prove the dot product is a bilinear map from (ZZ)-(Vect)s to (ZZ) (or at least, up to symmetry in the arguments).
* Prove ZZ matrices form an algebra. Should work for ring. Proof it's a ring follows from associativity of matrix multiplication for a commutative ground ring.
* Distributivities of matrix-matrix, vector-matrix, and matrix-vector multiplication over matrix addition and vector addition.
* Prove transposition is an antiendomorphism of multiplication for ZZ matrices, and an endomorphism of addition, hence an antiendomorphism of the matrix ring.
* Some Algebra.neutral is a zero element proofs.
* Prove scalar multiplication of the left factor in a vector- or matrix-matrix product
is the same as multiplying the product by the same scalar. (Note rel. to bilinearity)
-}

-- This & the mirrored statement form the theorem that the dot product is a bilinear map from vects to the scalar ring.
-- This would be better with binary cong / leibniz equality on the (<+>)s.
dotProductRightDistributesOverVectorPlus : (l, c, r : Vect n ZZ) -> (l<+>c)<:>r = (l<:>r)<+>(c<:>r)
dotProductRightDistributesOverVectorPlus [] [] [] = Refl
dotProductRightDistributesOverVectorPlus (l::ls) (c::cs) (r::rs) = trans monoidrec1D $
	trans (cong {f=(((l<+>c)<.>r) <+>)} $ dotProductRightDistributesOverVectorPlus ls cs rs)
	$ trans (cong {f=(<+>((ls<:>rs)<+>(cs<:>rs)))} $ ringOpIsDistributiveR_ZZ l c r)
	$ trans (doubleSumInnerSwap (l<.>r) (c<.>r) (ls<:>rs) (cs<:>rs))
	$ rewrite monoidrec1D {v=l<.>r} {vs=zipWith (<.>) ls rs} in rewrite monoidrec1D {v=c<.>r} {vs=zipWith (<.>) cs rs} in Refl

dotProductLeftDistributesOverVectorPlus : (l, c, r : Vect n ZZ) -> l<:>(c<+>r) = (l<:>c)<+>(l<:>r)
dotProductLeftDistributesOverVectorPlus [] [] [] = Refl
dotProductLeftDistributesOverVectorPlus (l::ls) (c::cs) (r::rs) = trans monoidrec1D $
	trans (cong {f=((l<.>(c<+>r)) <+>)} $ dotProductLeftDistributesOverVectorPlus ls cs rs)
	$ trans (cong {f=(<+>((ls<:>cs)<+>(ls<:>rs)))} $ ringOpIsDistributiveL_ZZ l c r)
	$ trans (doubleSumInnerSwap (l<.>c) (l<.>r) (ls<:>cs) (ls<:>rs))
	$ rewrite monoidrec1D {v=l<.>r} {vs=zipWith (<.>) ls rs} in rewrite monoidrec1D {v=l<.>c} {vs=zipWith (<.>) ls cs} in Refl

matrixMultLeftDistributesOverVectorPlus : (l : Matrix n m ZZ) -> (c, r : Vect m ZZ) -> l</>(c<+>r) = (l</>c)<+>(l</>r)
matrixMultLeftDistributesOverVectorPlus [] c r = Refl
matrixMultLeftDistributesOverVectorPlus (x::xs) c r = vecHeadtailsEq (dotProductRightDistributesOverVectorPlus c r x) $ matrixMultLeftDistributesOverVectorPlus xs c r

matrixMultRightDistributesOverVectorPlus : (l, c : Vect n ZZ) -> (r : Matrix n m ZZ) -> (l<+>c)<\>r = (l<\>r)<+>(c<\>r)
matrixMultRightDistributesOverVectorPlus l c r = matrixMultLeftDistributesOverVectorPlus (transpose r) l c

matrixAddEntrywise : (x, y : Matrix n m ZZ)
	-> (i : Fin n) -> (j : Fin m)
	-> indices i j (x<+>y) = (indices i j x)<+>(indices i j y)
matrixAddEntrywise [] [] i j = FinZElim i
matrixAddEntrywise (x::xs) (y::ys) FZ j = lemma_VectAddEntrywise j x y
matrixAddEntrywise (x::xs) (y::ys) (FS preli) j = matrixAddEntrywise xs ys preli j

{-
DISPLACED TO BE DEPENDED ON SOONER:

* lemma_VectAddHead
* matrixAddHead
* lemma_VectAddTail
* matrixAddTail

Related:
* headOfSumIsSumOfHeads
* tailOfSumIsSumOfTails
-}

matrixAddMapHead : (x, y : Matrix n (S predm) ZZ) -> map Vect.head $ x<+>y = (map Vect.head x)<+>(map Vect.head y)
matrixAddMapHead [] [] = Refl
matrixAddMapHead (x::xs) (y::ys) = vecHeadtailsEq (lemma_VectAddHead x y) $ matrixAddMapHead xs ys

matrixAddMapTail : (x, y : Matrix n (S predm) ZZ) -> map Vect.tail $ x<+>y = (map Vect.tail x)<+>(map Vect.tail y)
matrixAddMapTail [] [] = Refl
matrixAddMapTail (x::xs) (y::ys) = vecHeadtailsEq (lemma_VectAddTail x y) $ matrixAddMapTail xs ys

matrixTransposeEndoMatrixPlus : (x, y : Matrix n m ZZ) -> transpose (x<+>y) = (transpose x)<+>(transpose y)
matrixTransposeEndoMatrixPlus x y = vecIndexwiseEq
	$ \i => vecIndexwiseEq
		$ \j => trans (transposeIndicesChariz j i)
			$ trans (matrixAddEntrywise x y j i)
			$ trans (cong {f=(<+>(indices j i y))}
				$ sym $ transposeIndicesChariz j i)
			$ trans (cong {f=((indices i j $ transpose x)<+>)}
				$ sym $ transposeIndicesChariz j i)
			$ sym $ matrixAddEntrywise (transpose x) (transpose y) i j

vectorTimesLeftDistributesOverMatrixPlus : (l : Vect n ZZ) -> (c, r : Matrix n m ZZ)
	-> l<\>(c<+>r) = (l<\>c)<+>(l<\>r)
vectorTimesLeftDistributesOverMatrixPlus {m=Z} l c r = zeroVecEq
vectorTimesLeftDistributesOverMatrixPlus {m=S predm} l c r =
	trans (timesVectMatAsHeadTail_ByTransposeElimination {scals=l} {vects=c<+>r})
	$ trans (vecHeadtailsEq (cong {f=(l<:>)} $ matrixAddMapHead c r) $ cong {f=(l<\>)} $ matrixAddMapTail c r)
	$ trans (vecHeadtailsEq (dotProductLeftDistributesOverVectorPlus l (map head c) (map head r)) $ vectorTimesLeftDistributesOverMatrixPlus l (map tail c) (map tail r))
	$ trans (cong $ sym $ timesVectMatAsHeadTail_ByTransposeElimination {scals=l} {vects=r})
	$ cong {f=(<+>(l<\>r))} $ sym $ timesVectMatAsHeadTail_ByTransposeElimination {scals=l} {vects=c}

{-
-- Equational reasoning vrsn
	l<\>(c<+>r)    ={ timesVectMatAsHeadTail_ByTransposeElimination {scals=l} {vects=c<+>r} }=
	(l <:> map head (c<+>r))::(l<\>map tail (c<+>r)) ={ vecHeadtailsEq (cong {f=(l<:>)} $ matrixAddMapHead c r) (cong {f=(l<\>)} $ matrixAddMapTail c r) }=
	(l <:> ((map head c)<+>(map head r)))::(l<\>((map tail c)<+>(map tail r))) ={ vecHeadtailsEq (dotProductLeftDistributesOverVectorPlus l (map head c) ( map head r)) $ vectorTimesLeftDistributesOverMatrixPlus l (map tail c) (map tail r) }=
	( (l<:>(map head c))::(l<\>(map tail c)) ) <+> ( (l<:>(map head r)) :: (l<\>(map tail r)) )    ={ cong $ sym $ timesVectMatAsHeadTail_ByTransposeElimination {scals=l} {vects=r} }=
	( (l<:>(map head c))::(l<\>(map tail c)) ) <+> ( l<\>r )    ={ cong {f=(<+>(l<\>r))} $ sym $ timesVectMatAsHeadTail_ByTransposeElimination {scals=l} {vects=c} }=
	(l<\>c)<+>(l<\>r)
	qed
-}

matrixMultRightDistributesOverMatrixPlus : (l, c : Matrix n k ZZ) -> (r : Matrix k m ZZ) -> (l<+>c)<>r = (l<>r)<+>(c<>r)
matrixMultRightDistributesOverMatrixPlus [] [] r = zeroVecEq
matrixMultRightDistributesOverMatrixPlus (l::ls) (c::cs) r = vecHeadtailsEq
	(matrixMultRightDistributesOverVectorPlus l c r)
	$ matrixMultRightDistributesOverMatrixPlus ls cs r

{-
Could use (matrixTransposeAntiendoMatrixMult) to avoid repeating the proof, but
that assumes the ring is commutative, so that prevents future full generality.
-}
matrixMultLeftDistributesOverMatrixPlus : (l : Matrix n k ZZ) -> (c, r : Matrix k m ZZ) -> l<>(c<+>r) = (l<>c)<+>(l<>r)
matrixMultLeftDistributesOverMatrixPlus [] c r = Refl
matrixMultLeftDistributesOverMatrixPlus (l::ls) c r = vecHeadtailsEq (vectorTimesLeftDistributesOverMatrixPlus l c r) $ matrixMultLeftDistributesOverMatrixPlus ls c r

-- Further interactions with the transpose
-- The below are true if and only if the ring is commutative.

dotProductCommutative : (x, y : Vect n ZZ) -> x<:>y = y<:>x
dotProductCommutative [] [] = Refl
dotProductCommutative (x::xs) (y::ys) = trans monoidrec1D
	$ trans (cong {f=(<+>(xs<:>ys))} $ ringOpIsCommutative_ZZ x y)
	$ trans (cong {f=((y<.>x)<+>)} $ dotProductCommutative xs ys)
	$ sym $ monoidrec1D

matrixTransposeAntiendoMatrixMult : (x : Matrix n k ZZ) -> (y : Matrix k m ZZ) -> transpose (x<>y) = (transpose y)<>(transpose x)
matrixTransposeAntiendoMatrixMult x y = vecIndexwiseEq
	$ \i => vecIndexwiseEq
		$ \j => trans (transposeIndicesChariz j i)
			$ trans (cong {f=index i} $ indexMapChariz {k=j} {xs=x} {f=((transpose y)</>)})
			$ trans indexMapChariz
			$ trans (dotProductCommutative _ _)
			$ trans (sym $ indexMapChariz {k=j} {f=((index i (transpose y))<:>)} {xs=x})
			$ trans (cong {f=index j} $ matVecMultIsVecTransposeMult (index i $ transpose y) x)
			$ cong {f=index j} $ sym $ indexMapChariz {k=i} {f=(<\>(transpose x))} {xs=transpose y}

{-
-- Equational reasoning vrsn (not formatted in the syntax for that, though)
matrixTransposeAntiendoMatrixMult x y = vecIndexwiseEq
	$ \i => vecIndexwiseEq
		$ \j => trans (transposeIndicesChariz j i)
			$ trans (cong {f=index i} indexMapChariz) -- ((x!j)<\>y)!i
				-- === ((transpose y)</>(x!j))!i
			$ trans indexMapChariz
				-- (index j x)<:>(index i $ transpose y)
			$ trans (dotProductCommutative _ _)
				-- (index i $ transpose y)<:>(index j x)
			$ trans (sym $ indexMapChariz {k=j} {f=((index i $ transpose y)<:>)} {xs=x})
				-- index j $ map ((index i $ transpose y)<:>) x
				-- === index j $ x</>(index i $ transpose y)
			$ trans (cong {f=index j} $ matVecMultIsVecTransposeMult (index i $ transpose y) x)
				-- index j $ (index i $ transpose y)<\>(transpose x)
			$ trans (cong {f=index j} $ sym $ indexMapChariz {k=i} {f=(<\>(transpose x))} {xs=transpose y})
				-- index j $ index i $ map (<\> (transpose x)) (transpose y)
-}

{-
dotCancelsHeadWithLeadingZeroL : VerifiedRing a => (x, y : Vect n a) -> (Algebra.neutral::x)<:>(r::y) = x<:>y
dotCancelsHeadWithLeadingZeroL x y {r} = trans (monoidrec (Algebra.neutral<.>r) $ zipWith (<.>) x y)
	$ trans (cong {f=((Algebra.neutral<.>r)<+>)} ?dotcancelsLpatch) -- something like dotproductRewrite, up to sym
	$ trans (cong {f=(<+> (x<:>y))} $ ringNeutralIsMultZeroL r)
	$ monoidNeutralIsNeutralR $ x<:>y

dotCancelsHeadWithLeadingZeroR : VerifiedRing a => (x, y : Vect n a) -> (r::x)<:>(Algebra.neutral::y) = x<:>y
-}

dotCancelsHeadWithLeadingZeroL : (x, y : Vect n ZZ) -> (Algebra.neutral::x)<:>(r::y) = x<:>y
dotCancelsHeadWithLeadingZeroL x y {r} = trans monoidrec1D
	$ trans (cong {f=(<+> (x<:>y))} $ ringNeutralIsMultZeroL r)
	$ monoidNeutralIsNeutralR $ x<:>y

dotCancelsHeadWithLeadingZeroR : (x, y : Vect n ZZ) -> (r::x)<:>(Algebra.neutral::y) = x<:>y
dotCancelsHeadWithLeadingZeroR x y {r} = trans monoidrec1D
	$ trans (cong {f=(<+> (x<:>y))} $ ringNeutralIsMultZeroR r)
	$ monoidNeutralIsNeutralR $ x<:>y

neutralVectIsDotProductZero_L : (x : Vect nu ZZ) -> Algebra.neutral <:> x = Algebra.neutral
neutralVectIsDotProductZero_L [] = Refl
neutralVectIsDotProductZero_L (x::xs) = trans (dotCancelsHeadWithLeadingZeroL Algebra.neutral xs) $ neutralVectIsDotProductZero_L xs

{-
-- Mixture of instance problems and problem generalizing (dotCancelsHeadWithLeadingZeroR).

neutralVectIsDotProductZero_R : VerifiedRing a => (x : Vect n a) -> x<:>Algebra.neutral = Algebra.neutral {a=a}
neutralVectIsDotProductZero_R [] = ?neutralVectIsDotProductZero_R_ReflCase
neutralVectIsDotProductZero_R (x::xs) = trans (dotCancelsHeadWithLeadingZeroR xs Algebra.neutral) $ neutralVectIsDotProductZero_R xs
-}

neutralVectIsDotProductZero_R : (x : Vect nu ZZ) -> x <:> Algebra.neutral = Algebra.neutral
neutralVectIsDotProductZero_R [] = Refl
neutralVectIsDotProductZero_R (x::xs) = trans (dotCancelsHeadWithLeadingZeroR xs Algebra.neutral) $ neutralVectIsDotProductZero_R xs

neutralVectIsVectTimesZero : (x : Matrix nu mu ZZ) -> Algebra.neutral <\> x = Algebra.neutral
neutralVectIsVectTimesZero xs {mu=Z} = zeroVecEq
neutralVectIsVectTimesZero xs {mu=S predmu} = trans timesVectMatAsHeadTail_ByTransposeElimination
	$ vecHeadtailsEq
		(neutralVectIsDotProductZero_L $ map head xs)
		$ neutralVectIsVectTimesZero $ map tail xs

emptyVectIsTimesVectZero : (x : Matrix nu Z ZZ) -> x</>[] = Algebra.neutral
emptyVectIsTimesVectZero [] = Refl
emptyVectIsTimesVectZero (x::xs) = vecHeadtailsEq (neutralVectIsDotProductZero_L x)
	$ emptyVectIsTimesVectZero xs

neutralMatIsMultZeroL : (x : Matrix nu mu ZZ) -> Algebra.neutral <> x = Algebra.neutral
neutralMatIsMultZeroL x = vecIndexwiseEq $ \i => trans indexMapChariz $ trans (cong {f=(<\>x)} indexReplicateChariz) $ trans (neutralVectIsVectTimesZero x) $ sym $ indexReplicateChariz

matMultCancelsHeadWithZeroColExtensionL : (map ((Pos 0)::) xs)<>(z::ys) = xs<>ys
matMultCancelsHeadWithZeroColExtensionL {xs} {ys} {z} = vecIndexwiseEq
	$ \i => vecIndexwiseEq
		$ \j => trans (matMultIndicesChariz {l=map ((Pos 0)::) xs} {r=z::ys})
			$ trans (cong {f=(<:>(getCol j $ z::ys))} indexMapChariz)
			$ trans (dotCancelsHeadWithLeadingZeroL {r=index j z} (index i xs) (getCol j ys))
			$ sym $ matMultIndicesChariz {l=xs} {r=ys}

timesPreservesLeadingZeroExtensionR : xs<>(map ((Pos 0)::) ys) = map ((Pos 0)::) $ xs<>ys
timesPreservesLeadingZeroExtensionR {xs} {ys} = vecIndexwiseEq $ \i => vecIndexwiseEq $ \j => filmy i j
	where
		filmy : (i : _) -> (j : _) -> indices i j $ xs<>(map ((Pos 0)::) ys) = indices i j $ map ((Pos 0)::) $ xs<>ys
		filmy i FZ = trans matMultIndicesChariz
			$ trans (cong {f=((index i xs)<:>)} $ leadingElemExtensionFirstColReplicate $ Pos 0)
			$ trans (neutralVectIsDotProductZero_R $ index i xs)
			$ sym $ cong {f=index FZ} $ indexMapChariz {f=((Pos 0)::)}
		filmy i (FS prelj) = trans matMultIndicesChariz
			$ trans (cong {f=((index i xs)<:>)} leadingElemExtensionColFSId)
			$ trans (sym $ matMultIndicesChariz)
			$ sym $ cong {f=index $ FS prelj} $ indexMapChariz {f=((Pos 0)::)}

{-
-- Type mismatch due to instance mismatch b-n
--   (<.>) {{(@@constructor of Classes.Verified.VerifiedRing#Ring a) constrarg}}
-- and
--   (<.>) {{(@@constructor of Control.Algebra.RingWithUnity#Ring a) constrarg1}}
-- Also tried (VerifiedRingWithUnity a =>)
scaledNeutralIsNeutral : (VerifiedRing a, RingWithUnity a) =>
	{m : Nat}
	-> (z : a)
	-> z<#>(the (Vect m a) Algebra.neutral) = Algebra.neutral
scaledNeutralIsNeutral _ {m=Z} = Refl
scaledNeutralIsNeutral z {m=S predm} = vecHeadtailsEq (ringNeutralIsMultZeroR z)
	$ scaledNeutralIsNeutral z {m=predm}
-}

scaledNeutralIsNeutral_zz : {m : Nat}
	-> (z : ZZ)
	-> z<#>(the (Vect m ZZ) Algebra.neutral) = Algebra.neutral
scaledNeutralIsNeutral_zz _ {m=Z} = Refl
scaledNeutralIsNeutral_zz z {m=S predm} = vecHeadtailsEq (ringNeutralIsMultZeroR z)
	$ scaledNeutralIsNeutral_zz z {m=predm}

vectVectLScalingCompatibility : {z : ZZ} -> (z<#>l)<:>r = z<.>(l<:>r)
vectVectLScalingCompatibility {z} {l=[]} {r=[]} = sym $ ringNeutralIsMultZeroR z
vectVectLScalingCompatibility {z} {l=l::ls} {r=r::rs} =
	trans (dotproductRewrite {v=z<#>(l::ls)} {w=r::rs})
	$ trans (cong {f=monoidsum} $ vecHeadtailsEq (sym $ ringOpIsAssociative z l r) Refl)
	$ trans monoidrec1D
	$ trans (cong {f=((z<.>(l<.>r))<+>)}
		$ trans (sym $ dotproductRewrite {v=z<#>ls} {w=rs})
		$ (vectVectLScalingCompatibility {z=z} {l=ls} {r=rs}))
	$ trans (sym $ ringOpIsDistributiveL z (l<.>r) (ls<:>rs))
	-- z<.>(l<.>r <+> ls<:>rs)
	$ cong {f=(z<.>)}
	$ trans (cong {f=((l<.>r)<+>)} $ dotproductRewrite {v=ls} {w=rs})
	-- (l<.>r)<+>(monoidsum $ zipWith (<.>) ls rs)
	$ trans (sym monoidrec1D)
	$ sym $ dotproductRewrite {v=l::ls} {w=r::rs}

-- Note the relationship to bilinearity of matrix multiplication
vectMatLScalingCompatibility : {z : ZZ} -> {rs : Matrix k m ZZ} -> (z <#> la) <\> rs = z <#> (la <\> rs)
vectMatLScalingCompatibility {z} {la=[]} {rs=[]} =
	trans zippyLemA
	$ sym $ trans (cong {f=(z<#>)} zippyLemA)
	$ scaledNeutralIsNeutral_zz z
vectMatLScalingCompatibility {z} {la=l::la} {rs=r::rs} {m=Z} = zeroVecEq
-- vectMatLScalingCompatibility {z} {la=l::la} {rs=r::rs} {m=S predm} = ?vMLSC_rhs_2
vectMatLScalingCompatibility {z} {la=l::la} {rs=r::rs} {m=S predm} =
	trans (timesVectMatAsHeadTail_ByTransposeElimination
		{scals=z<#>(l::la)} {vects=r::rs})
	$ trans ( vecHeadtailsEq
			(vectVectLScalingCompatibility {z=z} {l=l::la} {r=map head $ r::rs})
			$ vectMatLScalingCompatibility {z=z}
				{la=l::la} {rs=map tail $ r::rs} )
	$ sym $ cong {f=(z<#>)} $ timesVectMatAsHeadTail_ByTransposeElimination
		{scals=l::la} {vects=r::rs}

matMatLScalingCompatibility :
	(scal : ZZ)
	-> (xs : Matrix n k ZZ)
	-> (ys : Matrix k m ZZ)
	-> (scal <#> xs) <> ys = scal <#> (xs <> ys)
matMatLScalingCompatibility _ [] _ = zeroVecEq
matMatLScalingCompatibility scal (x::xs) ys = vecHeadtailsEq
	vectMatLScalingCompatibility
	$ matMatLScalingCompatibility scal xs ys

{-
Type mismatch between

	(<.>) {{(@@constructor of Classes.Verified.VerifiedRing#Ring a)
		(@@constructor of Classes.Verified.VerifiedRingWithUnity#VerifiedRing a)}}
		neutral
		x =
	neutral (Type of ringNeutralIsMultZeroL x)

and

	(<.>) {{(@@constructor of Control.Algebra.RingWithUnity#Ring a)
		(@@constructor of Classes.Verified.VerifiedRingWithUnity#RingWithUnity a)}}
		neutral
		x =
	neutral (Expected type)

---

neutralScalarIsScalarMultNeutral_Vect : VerifiedRingWithUnity a => (xs : Vect n a)
	-> (the a Algebra.neutral)<#>xs = Algebra.neutral
neutralScalarIsScalarMultNeutral_Vect [] = Refl
neutralScalarIsScalarMultNeutral_Vect (x::xs) = vecHeadtailsEq
	(ringNeutralIsMultZeroL x)
	$ neutralScalarIsScalarMultNeutral_Vect xs
-}

neutralScalarIsScalarMultNeutral_zzVect : (xs : Vect n ZZ)
	-> (the ZZ Algebra.neutral)<#>xs = Algebra.neutral
neutralScalarIsScalarMultNeutral_zzVect [] = Refl
neutralScalarIsScalarMultNeutral_zzVect (x::xs) = vecHeadtailsEq
	(ringNeutralIsMultZeroL x)
	$ neutralScalarIsScalarMultNeutral_zzVect xs

-- Can prove for arbitrary module by showing the LHS is its own double by distributivity
-- groupElemOwnDoubleImpliesNeut
neutralScalarIsScalarMultNeutral_zzMat : (xs : Matrix n m ZZ)
	-> (the ZZ Algebra.neutral)<#>xs = Algebra.neutral
neutralScalarIsScalarMultNeutral_zzMat [] = Refl
neutralScalarIsScalarMultNeutral_zzMat (x::xs) = vecHeadtailsEq
	(neutralScalarIsScalarMultNeutral_zzVect x)
	$ neutralScalarIsScalarMultNeutral_zzMat xs

vectTimesNegOneIsNeg_zz : (xs : Vect n ZZ)
	-> (Algebra.inverse $ the ZZ $ Algebra.unity) <#> xs = Algebra.inverse xs
vectTimesNegOneIsNeg_zz xs = groupOpIsCancellativeR_Vect _ _ xs
	$ trans (cong {f=(((Algebra.inverse $ Algebra.unity {a=ZZ}) <#> xs)<+>)}
		$ sym $ moduleScalarUnityIsUnity_Vect {ok=Refl} xs)
	$ trans (sym $ moduleScalarMultDistributiveWRTModuleAddition_Vect {ok=Refl}
		(Algebra.inverse $ Algebra.unity {a=ZZ}) (Algebra.unity {a=ZZ}) xs)
	$ trans (cong {f=(<#>xs)} $ groupInverseIsInverseR $ Algebra.unity {a=ZZ})
	$ trans (neutralScalarIsScalarMultNeutral_zzVect xs)
	$ sym $ groupInverseIsInverseR_Vect xs

matTimesNegOneIsNeg_zz : (xs : Matrix n m ZZ)
	-> (Algebra.inverse $ the ZZ $ Algebra.unity) <#> xs = Algebra.inverse xs
matTimesNegOneIsNeg_zz xs = groupOpIsCancellativeR _ _ xs
	$ trans (cong {f=(((Algebra.inverse $ Algebra.unity {a=ZZ}) <#> xs)<+>)}
		$ sym $ moduleScalarUnityIsUnity_Mat {a=ZZ} xs)
	$ trans (sym $ moduleScalarMultDistributiveWRTModuleAddition_Mat
		(Algebra.inverse $ Algebra.unity {a=ZZ}) (Algebra.unity {a=ZZ}) xs)
	$ trans (cong {f=(<#>xs)} $ groupInverseIsInverseR $ Algebra.unity {a=ZZ})
	$ trans (neutralScalarIsScalarMultNeutral_zzMat xs)
	$ sym $ groupInverseIsInverseR xs

{-
When checking type of ZZModuleSpan.negScalarToScaledNeg:
When checking an application of function Control.Algebra.VectorSpace.<#>:
        Can't resolve type class Group r

---

negScalarToScaledNeg : (VerifiedRingWithUnity r, VerifiedModule r a) -> (s : r) -> (x : a) -> (inverse s) <#> x = s <#> (inverse x)

-----

We require generalizations to other rings for:

	neutralScalarIsScalarMultNeutral_zzVect
	neutralScalarIsScalarMultNeutral_zzMat

	vectTimesNegOneIsNeg_zz
	matTimesNegOneIsNeg_zz

---

negScalarToScaledNegVect : VerifiedRingWithUnity r => (s : r) -> (x : Vect _ r) -> (inverse s) <#> x = s <#> (inverse x)

negScalarToScaledNegMat : VerifiedRingWithUnity r => (s : r) -> (x : Matrix _ _ r) -> (inverse s) <#> x = s <#> (inverse x)
-}

negScalarToScaledNegVect_zz : (s : ZZ)
	-> (x : Vect _ ZZ)
	-> (inverse s) <#> x = s <#> (inverse x)
negScalarToScaledNegVect_zz s x =
	trans (cong {f=(<#>x)}
		$ trans (negativeIsNegOneTimesRight s) $ ringOpIsCommutative_ZZ _ s)
	$ trans (sym $ moduleScalarMultiplyComposition_Vect s _ x)
	$ cong {f=(s<#>)} $ vectTimesNegOneIsNeg_zz x

negScalarToScaledNegMat_zz : (s : ZZ)
	-> (x : Matrix _ _ ZZ)
	-> (inverse s) <#> x = s <#> (inverse x)
negScalarToScaledNegMat_zz s x =
	trans (cong {f=(<#>x)}
		$ trans (negativeIsNegOneTimesRight s) $ ringOpIsCommutative_ZZ _ s)
	$ trans (sym $ moduleScalarMultiplyComposition_Mat s _ x)
	$ cong {f=(s<#>)} $ matTimesNegOneIsNeg_zz x


text:
data IsS : (Nat -> Nat) -> Type where
  Indeed : (s : Nat -> Nat) -> s === S -> IsS s

------------------------------------------------------------------------
-- 1.
-- the S pattern is forced by the fact the parameter is instantiated
-- so everything is fine

-- either left implicit
indeed : IsS S -> S === S
indeed (Indeed _ eq) = eq

-- or made explicit
indeed2 : IsS S -> S === S
indeed2 (Indeed S eq) = eq

------------------------------------------------------------------------
-- 2. The S pattern is not forced by the parameter (a generic variable)

-- either don't match on it
indeed3 : IsS s -> s === S
indeed3 (Indeed s eq) = eq

-- or match on the proof that forces it
indeed4 : IsS s -> s === S
indeed4 (Indeed S Refl) = Refl
--              ^ forced by Refl

-- If you don't: too bad!
fail : IsS s -> s === S
fail (Indeed S eq) = eq
--             ^ not Refl, S not forced! OUCH

ext: idr


text:
module TTImp.Utils

import Core.Context
import Core.Options
import Core.TT
import TTImp.TTImp

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

import Libraries.Utils.String

%default covering

export
getUnique : List String -> String -> String
getUnique xs x = if x `elem` xs then getUnique xs (x ++ "'") else x

-- Extract the RawImp pieces from a ImpDecl so they can be searched for unquotes
-- Used in findBindableNames{,Quot}
rawImpFromDecl : ImpDecl -> List RawImp
rawImpFromDecl decl = case decl of
    IClaim fc1 y z ys ty => [getFromTy ty]
    IData fc1 y (MkImpData fc2 n tycon opts datacons)
        => tycon :: map getFromTy datacons
    IData fc1 y (MkImpLater fc2 n tycon) => [tycon]
    IDef fc1 y ys => getFromClause !ys
    IParameters fc1 ys zs => rawImpFromDecl !zs ++ map getParamTy ys
    IRecord fc1 y z (MkImpRecord fc n params conName fields) => do
        (a, b) <- map (snd . snd) params
        getFromPiInfo a ++ [b] ++ getFromIField !fields
    INamespace fc1 ys zs => rawImpFromDecl !zs
    ITransform fc1 y z w => [z, w]
    IRunElabDecl fc1 y => [] -- Not sure about this either
    IPragma _ f => []
    ILog k => []
    IBuiltin _ _ _ => []
  where getParamTy : (a, b, c, RawImp) -> RawImp
        getParamTy (_, _, _, ty) = ty
        getFromTy : ImpTy -> RawImp
        getFromTy (MkImpTy _ _ _ ty) = ty
        getFromClause : ImpClause -> List RawImp
        getFromClause (PatClause fc1 lhs rhs) = [lhs, rhs]
        getFromClause (WithClause fc1 lhs wval prf flags ys) = [wval, lhs] ++ getFromClause !ys
        getFromClause (ImpossibleClause fc1 lhs) = [lhs]
        getFromPiInfo : PiInfo RawImp -> List RawImp
        getFromPiInfo (DefImplicit x) = [x]
        getFromPiInfo _ = []
        getFromIField : IField -> List RawImp
        getFromIField (MkIField fc x y z w) = getFromPiInfo y ++ [w]

-- Bind lower case names in argument position
-- Don't go under case, let, or local bindings, or IAlternative
export
findBindableNames : (arg : Bool) -> List Name -> (used : List String) ->
                    RawImp -> List (String, String)

-- Helper to traverse the inside of a quoted expression, looking for unquotes
findBindableNamesQuot : List Name -> (used : List String) -> RawImp ->
                        List (String, String)

findBindableNames True env used (IVar fc nm@(UN (Basic n)))
    = if not (nm `elem` env) && lowerFirst n
         then [(n, getUnique used n)]
         else []
findBindableNames arg env used (IPi fc rig p mn aty retty)
    = let env' = case mn of
                      Nothing => env
                      Just n => n :: env in
          findBindableNames True env used aty ++
          findBindableNames True env' used retty
findBindableNames arg env used (ILam fc rig p mn aty sc)
    = let env' = case mn of
                      Nothing => env
                      Just n => n :: env in
      findBindableNames True env used aty ++
      findBindableNames True env' used sc
findBindableNames arg env used (IApp fc fn av)
    = findBindableNames False env used fn ++ findBindableNames True env used av
findBindableNames arg env used (INamedApp fc fn n av)
    = findBindableNames False env used fn ++ findBindableNames True env used av
findBindableNames arg env used (IAutoApp fc fn av)
    = findBindableNames False env used fn ++ findBindableNames True env used av
findBindableNames arg env used (IWithApp fc fn av)
    = findBindableNames False env used fn ++ findBindableNames True env used av
findBindableNames arg env used (IAs fc _ _ (UN (Basic n)) pat)
    = (n, getUnique used n) :: findBindableNames arg env used pat
findBindableNames arg env used (IAs fc _ _ n pat)
    = findBindableNames arg env used pat
findBindableNames arg env used (IMustUnify fc r pat)
    = findBindableNames arg env used pat
findBindableNames arg env used (IDelayed fc r t)
    = findBindableNames arg env used t
findBindableNames arg env used (IDelay fc t)
    = findBindableNames arg env used t
findBindableNames arg env used (IForce fc t)
    = findBindableNames arg env used t
findBindableNames arg env used (IQuote fc t)
    = findBindableNamesQuot env used t
findBindableNames arg env used (IQuoteDecl fc d)
    = findBindableNamesQuot env used !(rawImpFromDecl !d)
findBindableNames arg env used (IAlternative fc u alts)
    = concatMap (findBindableNames arg env used) alts
-- We've skipped case, let and local - rather than guess where the
-- name should be bound, leave it to the programmer
findBindableNames arg env used tm = []

findBindableNamesQuot env used (IPi fc x y z argTy retTy)
    = findBindableNamesQuot env used ![argTy, retTy]
findBindableNamesQuot env used (ILam fc x y z argTy lamTy)
    = findBindableNamesQuot env used ![argTy, lamTy]
findBindableNamesQuot env used (ILet fc lhsfc x y nTy nVal scope)
    = findBindableNamesQuot env used ![nTy, nVal, scope]
findBindableNamesQuot env used (ICase fc x ty xs)
    = findBindableNamesQuot env used !([x, ty] ++ getRawImp !xs)
  where getRawImp : ImpClause -> List RawImp
        getRawImp (PatClause fc1 lhs rhs) = [lhs, rhs]
        getRawImp (WithClause fc1 lhs wval prf flags ys) = [wval, lhs] ++ getRawImp !ys
        getRawImp (ImpossibleClause fc1 lhs) = [lhs]
findBindableNamesQuot env used (ILocal fc xs x)
    = findBindableNamesQuot env used !(x :: rawImpFromDecl !xs)
findBindableNamesQuot env used (ICaseLocal fc uname internalName args x)
    = findBindableNamesQuot env used x
findBindableNamesQuot env used (IApp fc x y)
    = findBindableNamesQuot env used ![x, y]
findBindableNamesQuot env used (INamedApp fc x y z)
    = findBindableNamesQuot env used ![x, z]
findBindableNamesQuot env used (IAutoApp fc x y)
    = findBindableNamesQuot env used ![x, y]
findBindableNamesQuot env used (IWithApp fc x y)
    = findBindableNamesQuot env used ![x, y]
findBindableNamesQuot env used (IRewrite fc x y)
    = findBindableNamesQuot env used ![x, y]
findBindableNamesQuot env used (ICoerced fc x)
    = findBindableNamesQuot env used x
findBindableNamesQuot env used (IBindHere fc x y)
    = findBindableNamesQuot env used y
findBindableNamesQuot env used (IUpdate fc xs x)
    = findBindableNamesQuot env used !(x :: map getRawImp xs)
  where getRawImp : IFieldUpdate -> RawImp
        getRawImp (ISetField path y) = y
        getRawImp (ISetFieldApp path y) = y
findBindableNamesQuot env used (IAs fc nfc x y z)
    = findBindableNamesQuot env used z
findBindableNamesQuot env used (IDelayed fc x y)
    = findBindableNamesQuot env used y
findBindableNamesQuot env used (IDelay fc x)
    = findBindableNamesQuot env used x
findBindableNamesQuot env used (IForce fc x)
    = findBindableNamesQuot env used x
findBindableNamesQuot env used (IUnquote fc x)
    = findBindableNames True env used x
findBindableNamesQuot env used (IWithUnambigNames fc xs x)
    = findBindableNamesQuot env used x
findBindableNamesQuot env used (IVar fc x) = []
findBindableNamesQuot env used (ISearch fc depth) = []
findBindableNamesQuot env used (IAlternative fc x xs) = []
findBindableNamesQuot env used (IBindVar fc x) = []
findBindableNamesQuot env used (IPrimVal fc c) = []
findBindableNamesQuot env used (IType fc) = []
findBindableNamesQuot env used (IHole fc x) = []
findBindableNamesQuot env used (Implicit fc bindIfUnsolved) = []
-- These are the ones I'm not sure about
findBindableNamesQuot env used (IMustUnify fc x y)
    = findBindableNamesQuot env used y
findBindableNamesQuot env used (IUnifyLog fc k x)
    = findBindableNamesQuot env used x
-- Should f `(g `(List ~(x))) bind "x" as a parameter to "f"?
-- Depends how (or if) recursive quoting works
findBindableNamesQuot env used (IQuote fc x) = []
findBindableNamesQuot env used (IQuoteName fc x) = []
findBindableNamesQuot env used (IQuoteDecl fc xs) = []
findBindableNamesQuot env used (IRunElab fc x) = []

export
findUniqueBindableNames :
  {auto c : Ref Ctxt Defs} ->
  FC -> (arg : Bool) -> (env : List Name) -> (used : List String) ->
  RawImp -> Core (List (String, String))
findUniqueBindableNames fc arg env used t
  = do let assoc = nub (findBindableNames arg env used t)
       when (showShadowingWarning !getSession) $
         do defs <- get Ctxt
            let ctxt = gamma defs
            ns <- map catMaybes $ for assoc $ \ (n, _) => do
                    ns <- lookupCtxtName (UN (Basic n)) ctxt
                    let ns = flip mapMaybe ns $ \(n, _, d) =>
                               case definition d of
                                -- do not warn about holes: `?a` is not actually
                                -- getting shadowed as it will not become a
                                -- toplevel declaration
                                 Hole _ _ => Nothing
                                 _ => pure n
                    pure $ MkPair n <$> fromList ns
            whenJust (fromList ns) $ recordWarning . ShadowingGlobalDefs fc
       pure assoc

export
findAllNames : (env : List Name) -> RawImp -> List Name
findAllNames env (IVar fc n)
    = if not (n `elem` env) then [n] else []
findAllNames env (IPi fc rig p mn aty retty)
    = let env' = case mn of
                      Nothing => env
                      Just n => n :: env in
          findAllNames env aty ++ findAllNames env' retty
findAllNames env (ILam fc rig p mn aty sc)
    = let env' = case mn of
                      Nothing => env
                      Just n => n :: env in
      findAllNames env' aty ++ findAllNames env' sc
findAllNames env (IApp fc fn av)
    = findAllNames env fn ++ findAllNames env av
findAllNames env (INamedApp fc fn n av)
    = findAllNames env fn ++ findAllNames env av
findAllNames env (IAutoApp fc fn av)
    = findAllNames env fn ++ findAllNames env av
findAllNames env (IWithApp fc fn av)
    = findAllNames env fn ++ findAllNames env av
findAllNames env (IAs fc _ _ n pat)
    = n :: findAllNames env pat
findAllNames env (IMustUnify fc r pat)
    = findAllNames env pat
findAllNames env (IDelayed fc r t)
    = findAllNames env t
findAllNames env (IDelay fc t)
    = findAllNames env t
findAllNames env (IForce fc t)
    = findAllNames env t
findAllNames env (IQuote fc t)
    = findAllNames env t
findAllNames env (IUnquote fc t)
    = findAllNames env t
findAllNames env (IAlternative fc u alts)
    = concatMap (findAllNames env) alts
-- We've skipped case, let and local - rather than guess where the
-- name should be bound, leave it to the programmer
findAllNames env tm = []

-- Find the names in a type that affect the 'using' declarations (i.e.
-- the ones that mean the declaration will be added).
export
findIBindVars : RawImp -> List Name
findIBindVars (IPi fc rig p mn aty retty)
    = findIBindVars aty ++ findIBindVars retty
findIBindVars (ILam fc rig p mn aty sc)
    = findIBindVars aty ++ findIBindVars sc
findIBindVars (IApp fc fn av)
    = findIBindVars fn ++ findIBindVars av
findIBindVars (INamedApp fc fn n av)
    = findIBindVars fn ++ findIBindVars av
findIBindVars (IAutoApp fc fn av)
    = findIBindVars fn ++ findIBindVars av
findIBindVars (IWithApp fc fn av)
    = findIBindVars fn ++ findIBindVars av
findIBindVars (IBindVar fc v)
    = [UN (Basic v)]
findIBindVars (IDelayed fc r t)
    = findIBindVars t
findIBindVars (IDelay fc t)
    = findIBindVars t
findIBindVars (IForce fc t)
    = findIBindVars t
findIBindVars (IAlternative fc u alts)
    = concatMap findIBindVars alts
-- We've skipped case, let and local - rather than guess where the
-- name should be bound, leave it to the programmer
findIBindVars tm = []

mutual
  -- Substitute for either an explicit variable name, or a bound variable name
  substNames' : Bool -> List Name -> List (Name, RawImp) ->
                RawImp -> RawImp
  substNames' False bound ps (IVar fc n)
      = if not (n `elem` bound)
           then case lookup n ps of
                     Just t => t
                     _ => IVar fc n
           else IVar fc n
  substNames' True bound ps (IBindVar fc n)
      = if not (UN (Basic n) `elem` bound)
           then case lookup (UN $ Basic n) ps of
                     Just t => t
                     _ => IBindVar fc n
           else IBindVar fc n
  substNames' bvar bound ps (IPi fc r p mn argTy retTy)
      = let bound' = maybe bound (\n => n :: bound) mn in
            IPi fc r p mn (substNames' bvar bound ps argTy)
                          (substNames' bvar bound' ps retTy)
  substNames' bvar bound ps (ILam fc r p mn argTy scope)
      = let bound' = maybe bound (\n => n :: bound) mn in
            ILam fc r p mn (substNames' bvar bound ps argTy)
                           (substNames' bvar bound' ps scope)
  substNames' bvar bound ps (ILet fc lhsFC r n nTy nVal scope)
      = let bound' = n :: bound in
            ILet fc lhsFC r n (substNames' bvar bound ps nTy)
                              (substNames' bvar bound ps nVal)
                              (substNames' bvar bound' ps scope)
  substNames' bvar bound ps (ICase fc y ty xs)
      = ICase fc (substNames' bvar bound ps y) (substNames' bvar bound ps ty)
                 (map (substNamesClause' bvar bound ps) xs)
  substNames' bvar bound ps (ILocal fc xs y)
      = let bound' = definedInBlock emptyNS xs ++ bound in
            ILocal fc (map (substNamesDecl' bvar bound ps) xs)
                      (substNames' bvar bound' ps y)
  substNames' bvar bound ps (IApp fc fn arg)
      = IApp fc (substNames' bvar bound ps fn) (substNames' bvar bound ps arg)
  substNames' bvar bound ps (INamedApp fc fn y arg)
      = INamedApp fc (substNames' bvar bound ps fn) y (substNames' bvar bound ps arg)
  substNames' bvar bound ps (IAutoApp fc fn arg)
      = IAutoApp fc (substNames' bvar bound ps fn) (substNames' bvar bound ps arg)
  substNames' bvar bound ps (IWithApp fc fn arg)
      = IWithApp fc (substNames' bvar bound ps fn) (substNames' bvar bound ps arg)
  substNames' bvar bound ps (IAlternative fc y xs)
      = IAlternative fc y (map (substNames' bvar bound ps) xs)
  substNames' bvar bound ps (ICoerced fc y)
      = ICoerced fc (substNames' bvar bound ps y)
  substNames' bvar bound ps (IAs fc nameFC s y pattern)
      = IAs fc nameFC s y (substNames' bvar bound ps pattern)
  substNames' bvar bound ps (IMustUnify fc r pattern)
      = IMustUnify fc r (substNames' bvar bound ps pattern)
  substNames' bvar bound ps (IDelayed fc r t)
      = IDelayed fc r (substNames' bvar bound ps t)
  substNames' bvar bound ps (IDelay fc t)
      = IDelay fc (substNames' bvar bound ps t)
  substNames' bvar bound ps (IForce fc t)
      = IForce fc (substNames' bvar bound ps t)
  substNames' bvar bound ps tm = tm

  substNamesClause' : Bool -> List Name -> List (Name, RawImp) ->
                      ImpClause -> ImpClause
  substNamesClause' bvar bound ps (PatClause fc lhs rhs)
      = let bound' = map (UN . Basic) (map snd (findBindableNames True bound [] lhs))
                     ++ findIBindVars lhs
                     ++ bound in
            PatClause fc (substNames' bvar [] [] lhs)
                         (substNames' bvar bound' ps rhs)
  substNamesClause' bvar bound ps (WithClause fc lhs wval prf flags cs)
      = let bound' = map (UN . Basic) (map snd (findBindableNames True bound [] lhs))
                     ++ findIBindVars lhs
                     ++ bound in
            WithClause fc (substNames' bvar [] [] lhs)
                          (substNames' bvar bound' ps wval) prf flags cs
  substNamesClause' bvar bound ps (ImpossibleClause fc lhs)
      = ImpossibleClause fc (substNames' bvar bound [] lhs)

  substNamesTy' : Bool -> List Name -> List (Name, RawImp) ->
                  ImpTy -> ImpTy
  substNamesTy' bvar bound ps (MkImpTy fc nameFC n ty)
      = MkImpTy fc nameFC n (substNames' bvar bound ps ty)

  substNamesData' : Bool -> List Name -> List (Name, RawImp) ->
                    ImpData -> ImpData
  substNamesData' bvar bound ps (MkImpData fc n con opts dcons)
      = MkImpData fc n (substNames' bvar bound ps con) opts
                  (map (substNamesTy' bvar bound ps) dcons)
  substNamesData' bvar bound ps (MkImpLater fc n con)
      = MkImpLater fc n (substNames' bvar bound ps con)

  substNamesDecl' : Bool -> List Name -> List (Name, RawImp ) ->
                   ImpDecl -> ImpDecl
  substNamesDecl' bvar bound ps (IClaim fc r vis opts td)
      = IClaim fc r vis opts (substNamesTy' bvar bound ps td)
  substNamesDecl' bvar bound ps (IDef fc n cs)
      = IDef fc n (map (substNamesClause' bvar bound ps) cs)
  substNamesDecl' bvar bound ps (IData fc vis d)
      = IData fc vis (substNamesData' bvar bound ps d)
  substNamesDecl' bvar bound ps (INamespace fc ns ds)
      = INamespace fc ns (map (substNamesDecl' bvar bound ps) ds)
  substNamesDecl' bvar bound ps d = d

export
substNames : List Name -> List (Name, RawImp) ->
             RawImp -> RawImp
substNames = substNames' False

export
substBindVars : List Name -> List (Name, RawImp) ->
                RawImp -> RawImp
substBindVars = substNames' True

export
substNamesClause : List Name -> List (Name, RawImp) ->
                   ImpClause -> ImpClause
substNamesClause = substNamesClause' False

mutual
  export
  substLoc : FC -> RawImp -> RawImp
  substLoc fc' (IVar fc n) = IVar fc' n
  substLoc fc' (IPi fc r p mn argTy retTy)
      = IPi fc' r p mn (substLoc fc' argTy)
                      (substLoc fc' retTy)
  substLoc fc' (ILam fc r p mn argTy scope)
      = ILam fc' r p mn (substLoc fc' argTy)
                        (substLoc fc' scope)
  substLoc fc' (ILet fc lhsFC r n nTy nVal scope)
      = ILet fc' fc' r n (substLoc fc' nTy)
                     (substLoc fc' nVal)
                     (substLoc fc' scope)
  substLoc fc' (ICase fc y ty xs)
      = ICase fc' (substLoc fc' y) (substLoc fc' ty)
                  (map (substLocClause fc') xs)
  substLoc fc' (ILocal fc xs y)
      = ILocal fc' (map (substLocDecl fc') xs)
                   (substLoc fc' y)
  substLoc fc' (IApp fc fn arg)
      = IApp fc' (substLoc fc' fn) (substLoc fc' arg)
  substLoc fc' (INamedApp fc fn y arg)
      = INamedApp fc' (substLoc fc' fn) y (substLoc fc' arg)
  substLoc fc' (IAutoApp fc fn arg)
      = IAutoApp fc' (substLoc fc' fn) (substLoc fc' arg)
  substLoc fc' (IWithApp fc fn arg)
      = IWithApp fc' (substLoc fc' fn) (substLoc fc' arg)
  substLoc fc' (IAlternative fc y xs)
      = IAlternative fc' y (map (substLoc fc') xs)
  substLoc fc' (ICoerced fc y)
      = ICoerced fc' (substLoc fc' y)
  substLoc fc' (IAs fc nameFC s y pattern)
      = IAs fc' fc' s y (substLoc fc' pattern)
  substLoc fc' (IMustUnify fc r pattern)
      = IMustUnify fc' r (substLoc fc' pattern)
  substLoc fc' (IDelayed fc r t)
      = IDelayed fc' r (substLoc fc' t)
  substLoc fc' (IDelay fc t)
      = IDelay fc' (substLoc fc' t)
  substLoc fc' (IForce fc t)
      = IForce fc' (substLoc fc' t)
  substLoc fc' tm = tm

  export
  substLocClause : FC -> ImpClause -> ImpClause
  substLocClause fc' (PatClause fc lhs rhs)
      = PatClause fc' (substLoc fc' lhs)
                      (substLoc fc' rhs)
  substLocClause fc' (WithClause fc lhs wval prf flags cs)
      = WithClause fc' (substLoc fc' lhs)
                       (substLoc fc' wval)
                       prf
                       flags
                       (map (substLocClause fc') cs)
  substLocClause fc' (ImpossibleClause fc lhs)
      = ImpossibleClause fc' (substLoc fc' lhs)

  substLocTy : FC -> ImpTy -> ImpTy
  substLocTy fc' (MkImpTy fc nameFC n ty)
      = MkImpTy fc' fc' n (substLoc fc' ty)

  substLocData : FC -> ImpData -> ImpData
  substLocData fc' (MkImpData fc n con opts dcons)
      = MkImpData fc' n (substLoc fc' con) opts
                        (map (substLocTy fc') dcons)
  substLocData fc' (MkImpLater fc n con)
      = MkImpLater fc' n (substLoc fc' con)

  substLocDecl : FC -> ImpDecl -> ImpDecl
  substLocDecl fc' (IClaim fc r vis opts td)
      = IClaim fc' r vis opts (substLocTy fc' td)
  substLocDecl fc' (IDef fc n cs)
      = IDef fc' n (map (substLocClause fc') cs)
  substLocDecl fc' (IData fc vis d)
      = IData fc' vis (substLocData fc' d)
  substLocDecl fc' (INamespace fc ns ds)
      = INamespace fc' ns (map (substLocDecl fc') ds)
  substLocDecl fc' d = d

nameNum : String -> (String, Int)
nameNum str
    = case span isDigit (reverse str) of
           ("", _) => (str, 0)
           (nums, pre)
              => case unpack pre of
                      ('_' :: rest) => (reverse (pack rest), cast (reverse nums))
                      _ => (str, 0)

export
uniqueName : Defs -> List String -> String -> Core String
uniqueName defs used n
    = if !usedName
         then uniqueName defs used (next n)
         else pure n
  where
    usedName : Core Bool
    usedName
        = pure $ case !(lookupTyName (UN $ Basic n) (gamma defs)) of
                      [] => n `elem` used
                      _ => True

    next : String -> String
    next str
        = let (n, i) = nameNum str in
              n ++ "_" ++ show (i + 1)


text:
module Regex.Type

import Pruviloj.Core
import Pruviloj.Derive.DecEq

infixl 7 :.:
infixl 6 :|:
infixl 6 :&:

%default total

||| The type of regular expressions over a given token type.
public export
data Regex : Type where
  ||| The regular expression matching nothing
  Ø     : Regex
  ||| The regular expression matching an empty string
  Ɛ     : Regex
  ||| The regular expression matching a single token
  Tok   : Char -> Regex
  ||| Kleene star
  Star  : Regex -> Regex
  ||| Union of two regular expressions
  (:|:) : Regex -> Regex -> Regex
  ||| Complement of regular expressions
  Comp  : Regex -> Regex
  ||| Intersection of two regular expressions
  (:&:) : Regex -> Regex -> Regex
  ||| Sequence one regular expression after another
  (:.:) : Regex -> Regex -> Regex

||| Decidable equality on regular expressions
public export
regexDecEq : (r : Regex) -> (s : Regex) -> Dec (r = s)
%runElab (deriveDecEq `{regexDecEq})

implementation DecEq Regex where
  decEq a b = regexDecEq a b

-- implementation Functor Regex where
--   map f Ø         = Ø
--   map f Ɛ         = Ɛ
--   map f (Tok t)   = Tok (f t)
--   map f (Comp r)  = Comp (map f r)
--   map f (Star r)  = Star (map f r)
--   map f (r :|: s) = (map f r) :|: (map f s)
--   map f (r :&: s) = (map f r) :&: (map f s)
--   map f (r :.: s) = (map f r) :.: (map f s)

max_stars_repo_name: taktoa/idris-regexp

max_issues_repo_name: taktoa/idris-regexp

max_forks_repo_name: taktoa/idris-regexp


text:
module Language.Elab.Deriving.Selectors

import public Language.Reflection

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

import public Util

%language ElabReflection

{-
This pattern comes up a lot

isNoSugar : UnelabMode -> Bool
isNoSugar (NoSugar _) = True
isNoSugar _ = False
isDefImp : PiInfo t -> Bool
isDefImp (DefImplicit _) = True
isDefImp _ = False

We should have a deriving or converstion for this sort of thing, where you
select the 'true' case and all others are false. e.g.

data Foo : Type where
  Bif : Foo
  Waf : Int -> Foo

deriveSelectors Foo
results in

isBif : Foo -> Bool
isBif Bif = True
isBif _ = False

isWaf : Foo -> Bool
isWaf (Waf _) = True
isWaf _ = False
-}

-- Is this name pollution? Should we prefer `isCon Waf`
-- e.g. isCon Waf  isCon Bif

data Foo : Type where
  Bif : Foo
  Waf : Int -> Foo
  (:::) : Bool -> Bool -> Foo -- not really doable with singular functions, is::: ?

select : TTImp -> Visibility -> Constructor -> Elab ()
select dty vis con = do
  let n = mapName ("is" ++) con.name -- isWaf
      c = iClaim MW vis [] $ mkTy n `( ~dty -> Bool)
      expargs = filter (isExplicitPi . piInfo) con.args
      c1 = patClause (iVar n `iApp` foldl (\xs,_ => `(~xs _) ) (iVar con.name) expargs)
                     `(True)
      catchall = patClause `(~(iVar n) _) `(False)
      d = iDef n [c1,catchall]
  declare [c,d]
  pure ()

||| Derives a selector for any non-operator constructor
||| Simply because I'm not sure how to let you type the letters: e.g. is:::
export
deriveSelectors : Visibility -> Name -> Elab ()
deriveSelectors vis tn = do
  ti <- makeTypeInfo tn
  let cons' = filter (not . isOpName . name) ti.cons
  traverse_ (select ti.type vis) cons'

fetchRoot : TTImp -> TTImp
fetchRoot (IApp _ y _) = fetchRoot y
fetchRoot ty = ty

isCon : Name -> Constructor -> Elab Clause
isCon cn con = ?isCon_rhs

-- This is kind of tough, we don't have a good way to say
-- isFooCon (:::)   isFooCon Waf at the same type.
-- If we take a Name, e.g.:
-- isFooCon `{{(:::)}}   isFooCon `{{Waf}}
-- We don't have a good way to enforce it's valid to use
-- adding Maybe is a bit too much work for the user to deal with
deriveIsCon : Visibility -> Name -> Elab ()
deriveIsCon vis cn = do
  ti <- makeTypeInfo cn
  let n = mapName (\n => "is" ++ n ++ "Con") ti.name -- isFooCon, need to get Foo from cn
  let c = iClaim MW vis [] $ mkTy `{{Foo}} `( Name -> Bool)
  let catchall = patClause `(~(iVar n) _) `(False)

  defs <- traverse (isCon ti.name) ti.cons
  pure ()

%runElab deriveSelectors Private `{{Foo}}
-- %runElab deriveIsCon Private `{{Foo}}

foo1 : Foo -> Bool
foo1 x = isWaf x

foo2 : Foo -> Bool
foo2 x = isBif x

-- foo3 : Foo -> Bool
-- foo3 x = is::: x -- isn't generated


text:
module System.Time

import Data.Nat

import System       -- for `sleep` for `IO` implementations
import System.Clock -- for `clockTime` for `IO` implementations

%default total

----------------------------------------------------------
--- Common stuff for absolute time and finite duration ---
----------------------------------------------------------

public export %inline
UntypedTime : Type
UntypedTime = Nat

export
interface TimeValue a where
  (.millis)  : UntypedTime -> a
  (.seconds) : UntypedTime -> a
  (.minutes) : UntypedTime -> a
  (.hours)   : UntypedTime -> a
  (.days)    : UntypedTime -> a

  -- back conversions may lose data
  (.asMillis)  : a -> UntypedTime
  (.asSeconds) : a -> UntypedTime
  (.asMinutes) : a -> UntypedTime
  (.asHours)   : a -> UntypedTime
  (.asDays)    : a -> UntypedTime

  -- appropriate components when we represent this time value as `DD HH:MM:SS.ms`
  (.millisComponent)  : a -> UntypedTime
  (.secondsComponent) : a -> UntypedTime
  (.minutesComponent) : a -> UntypedTime
  (.hoursComponent)   : a -> UntypedTime
  (.daysComponent)    : a -> UntypedTime

  x.seconds = (1000 * x).millis
  x.minutes = (60 * x).seconds
  x.hours   = (60 * x).minutes
  x.days    = (24 * x).hours

  x.asSeconds = divNatNZ x.asMillis  1000 SIsNonZero
  x.asMinutes = divNatNZ x.asSeconds 60   SIsNonZero
  x.asHours   = divNatNZ x.asMinutes 60   SIsNonZero
  x.asDays    = divNatNZ x.asHours   24   SIsNonZero

  x.millisComponent  = modNatNZ x.asMillis  1000 SIsNonZero
  x.secondsComponent = modNatNZ x.asSeconds 60   SIsNonZero
  x.minutesComponent = modNatNZ x.asMinutes 60   SIsNonZero
  x.hoursComponent   = modNatNZ x.asHours   24   SIsNonZero
  x.daysComponent    = x.asDays

---------------------
--- Absolute time ---
---------------------

-- Well, absolute time is anyway a finite duration from some point in past...
namespace AbsTime

  export
  record Time where
    constructor MkTime
    millis : UntypedTime

  export
  TimeValue Time where
    (.millis)   = MkTime
    (.asMillis) = millis

  export
  Eq Time where
    (==) = (==) `on` (.asMillis)

  export
  Ord Time where
    compare = compare `on` (.asMillis)

----------------------------
--- Finite time duration ---
----------------------------

namespace FiniteDuration

  export
  record FinDuration where
    constructor MkFinDuration
    millis : UntypedTime

  export
  TimeValue FinDuration where
    (.millis) = MkFinDuration
    (.asMillis) = millis

  export
  Eq FinDuration where
    (==) = (==) `on` (.asMillis)

  export
  Ord FinDuration where
    compare = compare `on` (.asMillis)

  export
  Semigroup FinDuration where
    (<+>) = MkFinDuration .: (+) `on` (.asMillis)

  export
  Monoid FinDuration where
    neutral = MkFinDuration 0

  export
  (*) : Nat -> FinDuration -> FinDuration
  n * d = (n * d.asMillis).millis

  -- May lose data! `z * (d / z)` may be less than `d`
  export
  (/) : FinDuration -> (z : Nat) -> (0 _ : NonZero z) => FinDuration
  d / z = (divNatNZ d.asMillis z %search).millis

------------------------------------------------------------
--- Operations between absolute time and finite duration ---
------------------------------------------------------------

-- This is an absolute difference. `y + (x - y)` may be more than `x` if `x < y`
export
(-) : Time -> Time -> FinDuration
x - y = ((x `max` y).asMillis `minus` (x `min` y).asMillis).millis

export
(+) : Time -> FinDuration -> Time
t + d = (t.asMillis + d.asMillis).millis

------------------
--- Interfaces ---
------------------

public export
interface Timed m where
  currentTime : m Time

public export
interface Timed m => Monad m => CanSleep m where
  sleepTill : Time -> m Unit
  sleepTill t = sleepFor $ t - !currentTime

  sleepFor : FinDuration -> m Unit
  sleepFor d = sleepTill $ !currentTime + d

--------------------------------
--- Implementations for `IO` ---
--------------------------------

namespace Timed

  export
  [HasIO] HasIO io => Timed io where
    currentTime = liftIO $ (.millis) . fromInteger . millisOfClock <$> clockTime UTC where
      millisOfClock : Clock _ -> Integer
      millisOfClock (MkClock secs nanos) = secs * 1000 + nanos `div` 1000000

namespace CanSleep

  export
  [HasIO] HasIO io => CanSleep io using Timed.HasIO where
    sleepFor d = do
      sleep $ cast d.asSeconds
      let (msComp ** _) = toIntWithPrf d.millisComponent
      usleep msComp
      where
        %inline
        toIntWithPrf : Nat -> (x : Int ** So (x >= 0))
        toIntWithPrf k = (cast k ** believe_me {- we are converting from `Nat` -} Oh)

export
Timed IO where
  currentTime = currentTime @{HasIO}

export
CanSleep IO where
  sleepFor = sleepFor @{HasIO}


text:
module LTLS

import Control.Monad.Error.Either
import Control.Linear.LIO
import Crypto.Random
import Crypto.Random.C
import Data.Either
import Data.List
import Data.List1
import Data.String
import Data.String.Extra
import Data.String.Parser
import Debug.Trace
import Network.Socket
import Network.TLS
import Network.TLS.Certificate.System
import System
import System.File.ReadWrite
import Utils.Bytes
import Utils.Handle
import Utils.Handle.C
import Utils.IPAddr
import Utils.Misc

||| Constructs a HTTP GET request given a hostname
test_http_body : String -> List Bits8
test_http_body hostname =
  string_to_ascii
  $ join "\r\n"
  [ "GET / HTTP/1.1"
  , "Host: " <+> hostname
  , "Connection: close"
  , "User-Agent: curl"
  , "Accept: */*"
  , "Content-Length: 0"
  , ""
  , ""
  ]

tls_connect : List Certificate -> String -> Int -> EitherT String IO (List Bits8)
tls_connect certs target_hostname port = do
  Right sock <- socket AF_INET Stream 0
  | Left err => throwE "unable to create socket: \{show err}"
  0 <- connect sock (Hostname target_hostname) port
  | _ => throwE "unable to connect"

  -- Here we begin TLS communication in a linear fasion
  MkEitherT $ run $ do
    let handle = socket_to_handle sock
    -- Perform handshake with the TLS server
    -- Here we supply the chosen cipher suites,
    -- key exhange groups for TLS handshake
    (True # handle) <-
      tls_handshake
        -- the hostname of the server to be connected to
        target_hostname
        -- the elliptic curves x25519, secp256r1, secp384r1
        -- are chosen for key exchange
        -- RFC 8446 specifies that secp256r1 MUST be supported,
        -- and x25519 SHOULD be supported as well
        -- We put x25519 first because we prefer x25519 over secp256r1
        -- since the x25519 implementation is faster and simpler
        -- secp384r1 is also added to test with https://ecc384.badssl.com/
        -- note that key generation can take some time, so I prefer to keep
        -- this list short
        -- more groups such as x448 and secp521r1 are implemented but not used
        -- here
        (X25519 ::: [SECP256r1, SECP384r1])
        -- here we specify the supported signature algorithms that will be
        -- used to verify TLS handshake given the server's certificate
        supported_signature_algorithms
        -- here we specify the supported cipher suites that will be used
        -- to encrypt communication with the server
        -- we want to support both TLS 1.3 and TLS 1.2 so we supply both
        (tls13_supported_cipher_suites <+> tls12_supported_cipher_suites)
        -- handle of the underlying socket
        handle
        -- the function which will be used to verify the server's certificate
        -- more documentation can be found in Network.TLS.Verify
        -- if you want to skip certificate verification, you can use certificate_ignore_check
        -- or implement your own CertificateCheck function
        -- (certificate_ignore_check target_hostname)
        (certificate_check certs target_hostname)
    | (False # (error # ())) => pure $ Left error

    -- send data to the server
    -- here I split the data to two chunks for testing purpose
    -- you can just send the data without splitting
    let (data1, data2) = splitAt 40 $ test_http_body target_hostname
    (True # handle) <- write handle data1
    | (False # (error # ())) => pure $ Left error

    (True # handle) <- write handle data2
    | (False # (error # ())) => pure $ Left error

    -- I did read twice here for testing purpose
    -- read 100 bytes of data from the server
    (True # (output1 # handle)) <- read handle 100
    | (False # (error # ())) => pure $ Left error

    -- read 100 bytes of data from the server again
    (True # (output2 # handle)) <- read handle 100
    | (False # (error # ())) => pure $ Left error

    close handle
    pure $ Right (output1 <+> output2)

||| Given a list of trusted certificates, server hostname, server port,
||| connect to the server and send a HTTP request.
||| Arguments:
|||
||| target_hostname : String
||| target_hostname is the hostname of the server to be connected. It can
||| be a DNS hostname, IPv4 address, or IPv6 address.
|||
||| port : Int
||| port is the port number of the server to be connected. The port number
||| for https server is 443.
tls_test : String -> Int -> IO ()
tls_test target_hostname port = do
  putStrLn "reading cert store"
  Right certs <- get_system_trusted_certs
  | Left err => putStrLn "error while reading: \{show err}"
  Right response <- runEitherT $ tls_connect certs target_hostname port
  | Left err => putStrLn err
  putStrLn (ascii_to_string response)
  putStrLn "ok"

tls_test_targets : List (Bool, String, Int)
tls_test_targets =
  [ (True, "sha256.badssl.com", 443)
  -- TODO: change back to True when they are fixed
  -- https://github.com/chromium/badssl.com/issues/501
  , (False, "sha384.badssl.com", 443)
  , (False, "sha512.badssl.com", 443)
  , (True, "github.com", 443)
  , (True, "google.com", 443)
  -- TODO: investigate why these 2 are not working
  -- , ("ecc256.badssl.com", 443)
  -- , ("ecc384.badssl.com", 443)
  , (True, "tls-v1-2.badssl.com", 1012)
  , (False, "expired.badssl.com", 443)
  , (False, "wrong.host.badssl.com", 443)
  , (False, "self.signed.badssl.com", 443)
  , (False, "untrusted-root.badssl.com", 443)
  ]

export
tls_test_unit : EitherT String IO ()
tls_test_unit = do
  putStrLn "reading cert store"
  certs <- MkEitherT get_system_trusted_certs
  results <- liftIO $ traverse (go certs) tls_test_targets
  let [] = filter not results
  | failed => throwE "\{show $ length failed} tls connections failed"
  pure ()
  where
    go : List Certificate -> (Bool, String, Int) -> IO Bool
    go certs (should_work, target, port) = do
      putStr "testing on \{target} \{show port}: "
      Right _ <- runEitherT $ tls_connect certs target port
      | Left err =>
          if should_work
             then putStrLn "error: \{err}" $> False
             else putStrLn "expected error: \{err}" $> True
      if should_work
         then putStrLn "ok" $> True
         else putStrLn "ok when it should not be ok" $> False


text:
module And.A.Proof

import Yet.Another.Path as Val

%default total

equality : Val.val === 2+3
equality = Refl


text:
module Test.Crayons

import Crayons

%access export

main : IO ()
main = do
  putStrLn $ bright "bright" <+> dim "dim" <+> underscore "underscore" <+> blink "blink"
  putStrLn $ black "black" <+> red "red" <+> green "green" <+> yellow "yellow" <+> blue "blue" <+>
             magenta "magenta" <+> cyan "cyan" <+> white "white"
  putStrLn $ bgBlack "black" <+> bgRed "red" <+> bgGreen "green" <+> bgYellow "yellow" <+> bgBlue "blue" <+>
             bgMagenta "magenta" <+> bgCyan "cyan" <+> bgWhite "white"

max_stars_repo_name: Risto-Stevcev/idris-crayons

max_issues_repo_name: Risto-Stevcev/idris-crayons

max_forks_repo_name: Risto-Stevcev/idris-crayons


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

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

%default total

defaultEndianness : BitEndianness
defaultEndianness = ABBig

genSerialiseDecodeResultSuccess : Line -> Expr -> Expr
genSerialiseDecodeResultSuccess l value =
  genDataCtorExpr l (constructorName (NS serialiseCoreNS (UN (Basic "Success")))) [value]

genSerialiseDecodeResultFail : Line -> String -> Expr
genSerialiseDecodeResultFail l err =
  genDataCtorExpr l (constructorName (NS serialiseCoreNS (UN (Basic "Fail")))) [genStringLiteralExpr l err]

genSerialiseMkIteratorRes : Line -> Expr -> Expr -> Expr
genSerialiseMkIteratorRes l value it =
  genDataCtorExpr l (constructorName (NS serialiseCoreNS (UN (Basic "MkIteratorRes")))) [value, it]

-- Similar to the following Erlang code:
-- ```
-- <<Bin/binary, Value:8/integer>>.
-- ```
setGeneric : (targetTSL : TypeSpecifierList) -> (targetSize : Int) -> Line -> (builder : Expr) -> (value : Expr) -> Expr
setGeneric targetTSL targetSize l builder value =
  let binary =
        AEBitstring l
          [ MkBitSegment l builder ABSDefault                       ABBinary
          , MkBitSegment l value   (ABSInteger l (cast targetSize)) targetTSL
          ]
  in binary

-- Similar to the following Erlang code:
-- ```
-- get_byte(<<Value:8/integer, NewIt/binary>>) ->
--   {{next, Value}, NewIt};
-- get_byte(It) ->
--   {fail, It}.
-- ```
getGeneric : (targetTSL : TypeSpecifierList) -> (targetSize : Int) -> Line -> (it : Expr) -> Expr
getGeneric targetTSL targetSize l it =
  let successPattern = APBitstring l
        [ MkBitSegment l (ABPVar l "Value") (ABSInteger l (cast targetSize)) targetTSL
        , MkBitSegment l (ABPVar l "NewIt") ABSDefault                       ABBinary
        ]
      successBody =
        genSerialiseMkIteratorRes l (genSerialiseDecodeResultSuccess l (AEVar l "Value")) (AEVar l "NewIt") ::: []
      failPattern = APVar l "It"
      failBody =
        genSerialiseMkIteratorRes l (genSerialiseDecodeResultFail l "Failed to decode number") (AEVar l "It") ::: []
      funExpr = AEFun l 1
        (MkFunClause l
            [successPattern]
            []
            successBody :::
          [ MkFunClause l
              [failPattern]
              []
              failBody
          ]
        )
  in AEFunCall l funExpr [it]

export
setUnsignedInt : (size : Int) -> Line -> (builder : Expr) -> (value : Expr) -> Expr
setUnsignedInt = setGeneric (ABInteger {endianness=defaultEndianness})

export
getUnsignedInt : (size : Int) -> Line -> (it : Expr) -> Expr
getUnsignedInt = getGeneric (ABInteger {endianness=defaultEndianness})

export
setSignedInt : (size : Int) -> Line -> (builder : Expr) -> (value : Expr) -> Expr
setSignedInt = setGeneric (ABInteger {endianness=defaultEndianness})

export
getSignedInt : (size : Int) -> Line -> (it : Expr) -> Expr
getSignedInt = getGeneric (ABInteger {endianness=defaultEndianness})

export
setDouble : Line -> (builder : Expr) -> (value : Expr) -> Expr
setDouble = setGeneric (ABFloat {endianness=defaultEndianness}) 64

export
getDouble : Line -> (it : Expr) -> Expr
getDouble = getGeneric (ABFloat {endianness=defaultEndianness}) 64

-- Similar to the following Erlang code:
-- ```
-- set_binary(Bin, Value) ->
--   Size = erlang:byte_size(Value),
--   <<Bin/binary, Size:32/integer, Value/binary>>.
-- ```
export
setBinary : Line -> (builder : Expr) -> (value : Expr) -> Expr
setBinary l builder value =
  let binary =
        AEBitstring l
          [ MkBitSegment l (AEVar l "Bin")   ABSDefault        ABBinary
          , MkBitSegment l (AEVar l "Size")  (ABSInteger l 32) (ABInteger {endianness=defaultEndianness})
          , MkBitSegment l (AEVar l "Value") ABSDefault        ABBinary
          ]
      body =
        AEMatch l (APVar l "Size") (genFunCall l "erlang" "byte_size" [AEVar l "Value"]) :::
        [ binary
        ]
      funExpr = AEFun l 2
        (singleton $ MkFunClause l
          [APVar l "Bin", APVar l "Value"]
          []
          body
        )
  in AEFunCall l funExpr [builder, value]

-- Similar to the following Erlang code:
-- ```
-- get_binary(<<Size:32/integer, Value:Size/binary, NewIt/binary>>) ->
--   {{next, Value}, NewIt};
-- get_binary(It) ->
--   {fail, It}.
-- ```
export
getBinary : Line -> (it : Expr) -> Expr
getBinary l it =
  let successPattern = APBitstring l
        [ MkBitSegment l (ABPVar l "Size")  (ABSInteger l 32) (ABInteger {endianness=defaultEndianness})
        , MkBitSegment l (ABPVar l "Value") (ABSVar l "Size") ABBinary
        , MkBitSegment l (ABPVar l "NewIt") ABSDefault        ABBinary
        ]
      successBody =
        genSerialiseMkIteratorRes l (genSerialiseDecodeResultSuccess l (AEVar l "Value")) (AEVar l "NewIt") ::: []
      failPattern = APVar l "It"
      failBody =
        genSerialiseMkIteratorRes l (genSerialiseDecodeResultFail l "Failed to decode binary") (AEVar l "It") ::: []
      funExpr = AEFun l 1
        (MkFunClause l
            [successPattern]
            []
            successBody :::
          [ MkFunClause l
              [failPattern]
              []
              failBody
          ]
        )
  in AEFunCall l funExpr [it]


text:
isSingleton : Bool -> Type
isSingleton True = Nat
isSingleton False = List Nat

mkSingle : (x:Bool) -> isSingleton x
mkSingle True = 0
mkSingle False = []

sum : (single : Bool) -> isSingleton single -> Nat
sum True x = x
sum False [] = 0
sum False (x::xs) = x + sum False xs

max_stars_repo_name: shij-hsu/idr

max_issues_repo_name: shij-hsu/idr

max_forks_repo_name: shij-hsu/idr


text:
module Collections.BSTree.Set.Elem

import public Collections.BSTree.Map.Elem

max_stars_repo_name: polendri/idris-collections

max_issues_repo_name: polendri/idris-collections

max_forks_repo_name: polendri/idris-collections


text:
-- --------------------------------------------------------------- [ Error.idr ]
-- Module    : Error.idr
-- Copyright : (c) Jan de Muijnck-Hughes
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
module Config.Error

%access public export

data ConfigError : Type where
  PureParseErr : String -> ConfigError
  ParseError   : String -> String -> ConfigError
  FileNotFound : String -> FileError -> ConfigError

Show ConfigError where
  show (PureParseErr err)   = unlines ["Parse Error:", err]
  show (ParseError fn err)  =
    unlines [ unwords ["Parse Error:", fn, "error was:"]
            , err
            ]
  show (FileNotFound fname err) =
    unlines [ unwords ["File", show fname, "caused error:"]
            , show err
            ]

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

max_stars_repo_name: jfdm/idris-config

max_issues_repo_name: jfdm/idris-config

max_forks_repo_name: jfdm/idris-config


text:
module LightClick.IR.Channel.MicroSV

import Data.List
import Data.Vect
import Data.String

import Toolkit.Data.DList
import Toolkit.Data.DVect
import Toolkit.Data.DList.DeBruijn

import LightClick.Error

import LightClick.Types.Direction

import LightClick.IR.ModuleCentric

import LightClick.IR.Channel.MicroSV.InterpTy
import LightClick.IR.Channel.MicroSV.Error
import LightClick.IR.Channel.MicroSV.Intermediate

import Language.SystemVerilog.MetaTypes
import Language.SystemVerilog.Micro

%default covering

data TEnv : (local,global : Context) -> Type where
     MkEnv : (global : Context)
          -> (decls : Decls global)
          -> (local : Context)
          -> TEnv local global

ConvertFuncSig : (local, global : Context) -> Ty -> Type
ConvertFuncSig local global type =
     (env : TEnv local global)
  -> (expr : MicroSvIR local type)
  -> Either TError (Expr local global type)

convertExpr :  (env : TEnv local global)
  -> (expr : MicroSvIR local type)
  -> Either TError (Expr local global type)

convertDecl : {type : Ty}
           -> {global : Context}
           -> (decls : Micro.Decls global)
           -> (bind  : String)
           -> (expr  : MicroSvIR Nil type)
           -> Either TError (ValidDecl type TYPE, Expr Nil global type)
convertDecl decls bind expr {type} {global} with (validDecl type TYPE)
  convertDecl decls bind expr {global} | (Yes prfVDecl) with (convertExpr (MkEnv global decls Nil) expr)
    convertDecl decls bind expr {global} | (Yes prfVDecl) | (Left l) = Left $ Nested "Converting Decl" l
    convertDecl decls bind expr {global} | (Yes prfVDecl) | (Right newDecl) = Right (prfVDecl, newDecl)

  convertDecl decls bind expr | (No contra) = Left MalformedExpr

data ValidDecls : List Ty
               -> Context
               -> Type
  where
    Empty : ValidDecls Nil Nil
    Extend : (name : String)
          -> (prf  : ValidDecl type TYPE)
          -> (rest : ValidDecls types kvs)
          -> ValidDecls (type::types) ((name,type)::kvs)

convertDecls : (decls : Intermediate.Decls types)
            -> Either TError (global ** (ValidDecls types global, Decls global))

convertDecls [] = Right (_ ** (Empty, Empty))

convertDecls (MkDecl binder expr :: rest) with (convertDecls rest)
  convertDecls (MkDecl binder expr :: rest) | Left l
    = Left $ Nested "Converting Decls" l

  convertDecls (MkDecl binder expr :: rest) | Right (ctxt ** MkPair ps ds) with (convertDecl ds binder expr)

    convertDecls (MkDecl binder expr :: rest) | Right (ctxt ** MkPair ps ds) | (Left l)
      = Left l

    convertDecls (MkDecl binder expr :: rest) | Right (ctxt ** MkPair ps ds) | (Right (p,d))
      = Right (_ ** MkPair (Extend binder p ps) (DeclAdd binder d p ds))

convertData : {n : Nat} -> (f : ConvertFuncSig local global a)
           -> (env : TEnv local global)
           -> (ds : Vect (S n) (Pair String (MicroSvIR local a)))
           -> Either TError (Vect (S n) (Pair String (Expr local global a)))

convertData {n=n} f env ((k,v) :: xs) with (xs)
  convertData {n=Z} f env ((k,v) :: xs) | []
    = do r <- f env v
         pure [(k,r)]

  convertData {n=S n}f env ((k,v) :: xs) | (y :: ys)
    = do r <- (f env v)
         ys' <- convertData f env (y::ys)
         pure $ (k,r) :: ys'

convertPorts : (env : TEnv local global)
            -> (ports : DList String (\a => MicroSvIR local (PORT a)) names)
            -> Either TError (DList String (\s => Expr local global (PORT s)) names)

convertPorts env Nil = Right Nil

convertPorts env (elem :: rest)
  = do r <- convertExpr env elem
       rs <- convertPorts env rest
       pure (r::rs)

convertChans : (f : ConvertFuncSig local global CHAN)
            -> (env : TEnv local global)
            -> (ds : List (Pair String (MicroSvIR local CHAN)))
            -> Either TError (List (Pair String (Expr local global CHAN)))

convertChans _ _ Nil = Right Nil

convertChans f env ((k,v) :: xs) with (xs)
  convertChans f env ((k,v) :: xs) | []
    = do r <- f env v
         pure [(k,r)]

  convertChans f env ((k,v) :: xs) | (y :: ys)
    = do r <- f env v
         ys' <- convertChans f env (y::ys)
         pure $ (k,r) :: ys'

-- [ Implementation of `convertExpr` ]
convertExpr env End = pure End

convertExpr env (Local label x) = pure $ Local label x

convertExpr env (Global label ty) with (env)
  convertExpr env (Global label ty) | (MkEnv global decls local) with (isElem (label,ty) global)
    convertExpr env (Global label ty) | (MkEnv global decls local) | (Yes idx)
      = pure (Global label idx)
    convertExpr env (Global label ty) | (MkEnv global decls local) | (No contra)
      = Left $ General $ unwords ["Attempting to generate Global ref failed:", show label]

-- [ Structural Statements ]
convertExpr env (Let this beThis {typeE} withType {ty} inThis) with (validLet typeE ty)
  convertExpr env (Let this beThis {typeE} withType {ty} inThis) | Yes prf with (env)
    convertExpr env (Let this beThis {typeE} withType {ty} inThis) | Yes prf | MkEnv global decls local
      = do beThis' <- convertExpr (MkEnv global decls local) beThis
           withType' <- convertExpr (MkEnv global decls local) withType
           inThis' <- convertExpr (MkEnv global decls ((this,typeE)::local)) inThis
           pure (Let this beThis' withType' prf inThis')

  convertExpr env (Let this beThis {typeE} withType {ty} inThis) | No x
    = Left $ General $ unwords ["Invalid Let:", show typeE, show ty]

convertExpr env (Seq x y) with (convertExpr env x)
  convertExpr env (Seq x y) | Left err = Left err

  convertExpr env (Seq x y) | Right x' with (convertExpr env y)
    convertExpr env (Seq x y) | Right x' | Left err
      = Left err
    convertExpr env (Seq x y) | Right x' | Right y'
      = pure (Seq x' y')

-- [ The TYPE ]
convertExpr env TYPE = pure TYPE

-- [ The GATE ]
convertExpr env GATE = pure GATE

-- [ Data types ]
convertExpr env DataLogic = pure DataLogic
convertExpr env (DataArray type size)
  = do type' <- convertExpr env type
       pure (DataArray type' size)

convertExpr env (DataStruct xs)
  = do xs' <- convertData convertExpr env xs
       pure (DataStruct xs')

convertExpr env (DataUnion xs)
  = do xs' <- convertData convertExpr env xs
       pure (DataUnion xs')

-- [ Module constructors ]
convertExpr env (Port label dir type)
  = do type' <- convertExpr env type
       pure (Port label dir type')

convertExpr env (MDecl ports)
  = do ps <- convertPorts env ports
       pure (MDecl ps)

-- [ Value Constructors ]
convertExpr env NewChan = pure NewChan

convertExpr env (NewModule xs)
  = do xs' <- convertChans convertExpr env xs
       pure (NewModule xs')

-- [ Gates ]
convertExpr env (Not o i)
  = do o' <- convertExpr env o
       i' <- convertExpr env i
       pure (Not o' i')

convertExpr env (Gate ty o ins)
  = do o' <- convertExpr env o
       ins' <- traverse (convertExpr env) ins
       pure (Gate ty o' ins')

export
covering
convertSpec : (expr : MicroSvIrSpec)
                   -> Either TError Spec
convertSpec (MkMSVIRSpec decls expr) with (convertDecls decls)
  convertSpec (MkMSVIRSpec decls expr) | (Left l)
    = Left $ Nested "Attempting to build decls" l

  convertSpec (MkMSVIRSpec decls expr) | (Right (gs ** (prfVDecls,decls'))) with (convertExpr (MkEnv gs decls' Nil) expr)

    convertSpec (MkMSVIRSpec decls expr) | (Right (gs ** (prfVDecls,decls'))) | (Left l)
      = Left $ Nested "Attempted to build Spec" l

    convertSpec (MkMSVIRSpec decls expr) | (Right (gs ** (prfVDecls,decls'))) | (Right r)
      = pure (MkSpec decls' r)

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

max_stars_repo_name: border-patrol/lightclick

max_issues_repo_name: border-patrol/lightclick

max_forks_repo_name: border-patrol/lightclick


text:
module Specdris.SpecIOTest

import Specdris.SpecIO
import Specdris.TestUtil

testCase : IO ()
testCase
  = do state <- specIOWithState $ do
             describe "context 1" $ do
               describe "context 1.1" $ do
                 it "context 1.1.1" $ do
                   a <- pure 1

                   pure $ do a === 2
                             a === 1

               it "context 1.2" $ do
                 pure $ "hello" `shouldSatisfy` (\str => (length str) > 5)
               it "context 1.3" $ do
                 pure $ 1 `shouldBe` 2
               it "context 1.4" $ do
                 pure $ pendingWith "for some reason"

       testAndPrint "spec io test" state (MkState 4 3 1 Nothing) (==)

withBeforeAndAfterAll : IO ()
withBeforeAndAfterAll
  = do state <- specIOWithState {beforeAll = putStrLn "beforeAll"} {afterAll = putStrLn "afterAll"} $ do
                  describe "context 1" $ do
                    it "context 1.1" $ do
                      pure $ 1 === 1

       testAndPrint "spec io test with before and after all" state (MkState 1 0 0 Nothing) (==)

around : IO SpecResult -> IO SpecResult
around spec = do putStrLn "before"
                 result <- spec
                 putStrLn "after"

                 pure result

withAround : IO ()
withAround
  = do state <- specIOWithState {around = around} $ do
                  describe "context 1" $ do
                    it "context 1.1" $ do
                      putStrLn "      => expectation"
                      pure $ 1 === 1

       testAndPrint "spec io test with around" state (MkState 1 0 0 Nothing) (==)

export
specSuite : IO ()
specSuite = do putStrLn "\n  spec-io:"
               testCase
               withBeforeAndAfterAll
               withAround

max_stars_repo_name: pheymann/specdris

max_issues_repo_name: pheymann/specdris

max_forks_repo_name: pheymann/specdris