text:
module NatUtils

import Order

%default total
%access public export

|||Proof of the type that an implication implies its contrapositive
impliesContrapositive : (a : Type) -> (b : Type) -> (a -> b) -> (Not b) -> (Not a)
impliesContrapositive a b aImpliesb bFalse x = bFalse (aImpliesb x)

|||Proof that m = n implies f m = f n
--Taken from Lecture.intro with modifications
--Prelude.Basics.cong serves the same function, use cong instead
functionExtendsEquality : (typ : Type) -> (f : typ -> typ) -> (n : typ) -> (m : typ) -> (n = m) -> (f n = f m)
functionExtendsEquality type f m m Refl = Refl

|||More General function extending equality
total
functionExtendsEquality2 : (typ1 : Type) -> (typ2 : Type) -> (f : typ1 -> typ2) -> (n : typ1) -> (m : typ1) -> (n = m) -> (f n = f m)
functionExtendsEquality2 typ1 typ2 f m m Refl = Refl

|||An injective predecessor "function"
predInjective : (n : Nat) -> (Not (n = Z)) -> (k ** (S k) = n)
predInjective Z proofNotZ = void (proofNotZ Refl)
predInjective (S k) _ = (k ** Refl)

|||Proof that Z is not equal to successor of any natural number
ZIsNotS : {n : Nat} -> (Not (Z = S n))
ZIsNotS {n} proofEq = SIsNotZ (sym proofEq)

|||difference of Nats, taken from Lecture.intro
sub : (a : Nat) -> (b : Nat) -> (LTE b a) -> Nat
sub a Z LTEZero = a
sub (S a) (S b) (LTESucc proofLTE) = sub a b proofLTE

|||Proof that the sum is greater than its parts
partsLTEsum : (a : Nat) -> (b : Nat) -> (LTE a (a + b), LTE b (a + b))
partsLTEsum Z b = (LTEZero, lteRefl)
partsLTEsum (S n) b = (LTESucc (fst (partsLTEsum n b)), lteSuccRight(snd (partsLTEsum n b)))

|||Proof that S a = S b implies a = b
--Same as succInjective, but implicit
predEqual : {a : Nat} -> {b : Nat} -> (S a = S b) -> (a = b)
predEqual Refl = Refl

|||Proof that a != b implies (S a) != (S b)
notEqualSucc : {a : Nat} -> {b : Nat} -> (Not (a = b)) -> (Not ((S a) = (S b)))
notEqualSucc {a} {b} proofNotEq proofEq = proofNotEq (predEqual proofEq)

|||Proof that (S a) != (S b) implies a != b
notEqualPred : {a : Nat} -> {b : Nat} -> (Not ((S a) = (S b))) -> (Not (a = b))
notEqualPred {a} {b} proofNotEq proofEq = proofNotEq (cong proofEq)

|||Proof that (a + b) = 0 implies a = 0 and b = 0
sumZeroImpliesZero : {a : Nat} -> {b : Nat} -> (a + b = Z) -> (a = Z, b = Z)
sumZeroImpliesZero {a = Z} {b = Z} Refl = (Refl, Refl)
sumZeroImpliesZero {a = Z} {b = S k} proofEq = void (SIsNotZ proofEq)
sumZeroImpliesZero {a = S k} {b} proofEq = void (SIsNotZ proofEq)

|||Proof that (a * b) = 0 implies a = 0 or b = 0
multZeroImpliesZero : {a : Nat} -> {b : Nat} -> (a * b = Z) -> Either (a = Z) (b = Z)
multZeroImpliesZero {a = Z} {b} proofZ = Left Refl
multZeroImpliesZero {a = S k} {b = Z} proofZ = Right Refl
multZeroImpliesZero {a = S k} {b = S l} proofZ = void (SIsNotZ proofZ)

|||Proof that a + k = b and k != 0 implies a != b
nonZeroSumNotEqual : {a : Nat} -> {b : Nat} -> {k : Nat} -> (a + k = b) -> (Not (k = Z)) -> (Not (a = b))
nonZeroSumNotEqual {a} {b} {k} proofEq proofNotZ proofaEqb = proofNotZ kEqZ where
	kEqZ = (plusLeftCancel a k Z aPluskEqaPlusZ) where
		aPluskEqaPlusZ = (trans aPluskPlEqbPlusZ (sym ((cong {f = (\n => (n + Z))}) proofaEqb))) where
			aPluskPlEqbPlusZ = rewrite (plusZeroRightNeutral b) in proofEq

|||Proof that a + k = b and a != b implies k != 0
nonEqualSumNotZero : {a : Nat} -> {b : Nat} -> {k : Nat} -> (a + k = b) -> (Not (a = b)) -> (Not (k = Z))
nonEqualSumNotZero {a} {b} {k} proofEq proofaNotEqb proofkEqZ =
	proofaNotEqb proofaEqb where
		proofaEqb = rewrite (plusCommutative Z a) in
				  rewrite (sym proofkEqZ) in
				  proofEq

|||Proof that a != 0 implies a + b != 0
nonZeroSumNotZeroLeft :  {a : Nat} -> (b : Nat) -> (Not (a = Z)) -> Not (a + b = Z)
nonZeroSumNotZeroLeft {a} b proofNotZero proofZero = proofNotZero (fst (sumZeroImpliesZero proofZero))

|||Proof that b != 0 implies a + b != 0
nonZeroSumNotZeroRight :  {a : Nat} -> (b : Nat) -> (Not (b = Z)) -> Not (a + b = Z)
nonZeroSumNotZeroRight {a} b proofNotZero proofZero = proofNotZero (snd (sumZeroImpliesZero proofZero))

|||Proof that a != 0 and b != 0 implies a * b ! = 0
nonZeroMultNotZero : {a : Nat} -> {b : Nat} ->
				 (Not (a = Z)) -> (Not (b = Z)) -> (Not (a * b = Z))
nonZeroMultNotZero {a} {b} aNotZ bNotZ proofZero =
	case (multZeroImpliesZero proofZero) of
		(Left aEqZ) => aNotZ aEqZ
		(Right bEqZ) => bNotZ bEqZ

|||Proof that (S a) + b = a + (S b)
plusSymmetricInS : {a : Nat} -> {b : Nat} -> ((S a) + b = a + (S b))
plusSymmetricInS {a = Z} {b} = Refl
plusSymmetricInS {a = S k} {b} = cong (plusSymmetricInS {a = k} {b})

|||Proof that a = b implies c * a = c * b
multConstantLeft : {a : Nat} -> {b : Nat} -> (c : Nat) -> (a = b) -> ((c * a) = (c * b))
multConstantLeft {a} {b} Z _ = Refl
multConstantLeft {a} {b} (S k) proofEq =
	trans (cong {f = (\n => n + (k * a))} proofEq) (cong {f = (\n => b + n)} inductiveProofEq) where
		inductiveProofEq = multConstantLeft {a} {b} k proofEq

|||Proof that a = b implies a * c = b * c
multConstantRight : {a : Nat} -> {b : Nat} -> (c : Nat) -> (a = b) -> ((a * c) = (b * c))
multConstantRight {a} {b} c proofEq = rewrite (multCommutative a c) in
							   rewrite (multCommutative b c) in
							   multConstantLeft c proofEq

|||Proof that c * a != c * b implies a != b
multConstantLeftNot : {a : Nat} -> {b : Nat} -> {c : Nat} -> (Not ((c * a) = (c * b))) -> (Not (a = b))
multConstantLeftNot {a} {b} {c} proofNotEq proofEq = void (proofNotEq (cong {f = (\n => c * n)} proofEq))

|||Proof that a * c != b * c implies a != b
multConstantRightNot : {a : Nat} -> {b : Nat} -> {c : Nat} -> (Not ((a * c) = (b * c))) -> (Not (a = b))
multConstantRightNot {a} {b} {c} proofNotEq proofEq = void (proofNotEq (cong {f = (\n => n * c)} proofEq))

|||Proof that a * c = b * c implies a = b
multRightCancel : (left1 : Nat) -> (left2 : Nat) -> (right : Nat) ->
				(Not (right = Z)) -> (left1 * right = left2 * right) -> (left1 = left2)
multRightCancel left1 left2 Z rightnotzero prf = void (rightnotzero Refl)
multRightCancel Z Z (S k) rightnotzero prf = Refl
multRightCancel Z (S _) (S _) _ proofEq = void (ZIsNotS proofEq)
multRightCancel (S _) Z (S _) _ proofEq = void (SIsNotZ proofEq)
multRightCancel (S j) (S i) (S k) rightnotzero prf = cong (multRightCancel j i (S k) rightnotzero (plusLeftCancel (S k) (j * (S k)) (i * (S k))  prf))

|||Proof that c * a = c * b implies a = b
multLeftCancel : (left : Nat) -> (right1 : Nat) -> (right2 : Nat) ->
			  (Not (left = Z)) -> (left * right1 = left * right2) -> (right1 = right2)
multLeftCancel c a b notZ proofEq =
	multRightCancel a b c notZ rewriteProof where
		rewriteProof = rewrite (multCommutative a c) in
					rewrite (multCommutative b c) in
					proofEq

|||Proof of distributivity
distributeProof: (a : Nat) -> (b : Nat) -> (d : Nat) -> (m : Nat) -> (n : Nat) ->
(a = m * d) -> (b = n * d) -> ((a + b) = (m + n) * d)
distributeProof a b d m n proofDividesa proofDividesb =
	rewrite (multDistributesOverPlusLeft m n d) in
		(trans (the (a + b = (m * d) + b) (v1)) v2) where
			v1 = plusConstantRight a (m * d) b proofDividesa
			v2 = plusConstantLeft b (n * d) (m * d) proofDividesb

|||Proof that n * a = a and a != 0 implies n = 1
multLeftIdIsOne : {n : Nat} -> {a : Nat} ->
			   (Not (a = Z)) -> (n * a = a) -> (n = 1)
multLeftIdIsOne {n} {a} notZ proofEq = trans (sym (multOneRightNeutral n)) (multRightCancel (n * 1) 1 a notZ (rewrite (sym (multAssociative n 1 a)) in (rewrite (multOneLeftNeutral a) in proofEq)))

|||Proof that p = a * b and a = 1 implies p = b
multOneLeftEqual : {p : Nat} -> {a : Nat} -> {b : Nat} -> (p = a * b) -> (a = 1) -> (p = b)
multOneLeftEqual {p} {a} {b} proofEq aIs1 =
	trans (trans proofEq (cong {f = (\n => n * b)} aIs1)) (multOneLeftNeutral b)

|||Proof that p = a * b and b = 1 implies p = a
multOneRightEqual : {p : Nat} -> {a : Nat} -> {b : Nat} -> (p = a * b) -> (b = 1) -> (p = a)
multOneRightEqual {p} {a} {b} proofEq bIs1 =
	rewrite (sym (multOneRightNeutral a)) in
	rewrite (sym bIs1) in
	proofEq

|||Proof that (a + k = b) and (b + l = a) implies a = b
plusAntiSymmetric : {a : Nat} -> {b : Nat} -> {k : Nat} -> {l : Nat} ->
					  (a + k = b) -> (b + l = a) -> (a = b)
plusAntiSymmetric {a} {b} {k} {l} proofEqLeft proofEqRight =
	(rewrite (sym (plusZeroRightNeutral a)) in (rewrite (sym (fst (sumZeroImpliesZero (plusLeftCancel a (k + l) Z step)))) in proofEqLeft)) where
		step = trans (rewrite (plusAssociative a k l) in (trans (cong {f = (\n => n + l)} proofEqLeft) proofEqRight)) (sym (plusZeroRightNeutral a))

|||Proof that a = r + q * b implies (n * a) = (n * r) + q * (n * b)
extendEqualMult : {a : Nat} -> {b : Nat} -> {q : Nat} -> {r : Nat} ->
			   (a = r + (q * b)) -> (n : Nat) -> ((n * a) = (n * r) + q * (n * b))
extendEqualMult {a} {b} {q} {r} proofEq n =
	rewrite (multAssociative q n b) in
	rewrite (multCommutative q n) in
	rewrite (sym (multAssociative n q b)) in
	rewrite (sym (multDistributesOverPlusRight n r (q * b))) in
	cong {f = (\l => n * l)} proofEq

||| Proof that a = c, b = d and a <= b implies c <= d
lteSubstitutes : {a : Nat} -> {b : Nat} -> {c : Nat} -> {d : Nat} ->
				(LTE a b) -> (a = c) -> (b = d) -> (LTE c d)
lteSubstitutes proofLTE Refl Refl = proofLTE

|||Proof that a < b implies a <= b
ltImpliesLTE : {a : Nat} -> {b : Nat} -> (LT a b) -> (LTE a b)
ltImpliesLTE proofLTE = lteSuccLeft proofLTE

|||Proof that a = b implies a <= b
eqImpliesLTE : {a : Nat} -> {b : Nat} -> (a = b) -> (LTE a b)
eqImpliesLTE {a = Z} {b = Z} Refl = LTEZero
eqImpliesLTE {a = S k} {b = Z} proofEq = void(SIsNotZ proofEq)
eqImpliesLTE {a = Z} {b = S l} proofEq = void(SIsNotZ (sym proofEq))
eqImpliesLTE {a = S k} {b = S l} proofEq = LTESucc (eqImpliesLTE (predEqual proofEq))

|||The theorem that (a <= b) and (b <= a) implies a = b
lteAntiSymmetric : {a : Nat} -> {b : Nat} -> (LTE a b) -> (LTE b a) -> (a = b)
lteAntiSymmetric LTEZero LTEZero = Refl
lteAntiSymmetric (LTESucc a) (LTESucc b) = cong (lteAntiSymmetric a b)

|||Proof that a < b implies S a = b or S a < b
ltImpliesEqOrLT : (a : Nat) -> (b : Nat) -> (LT a b) -> Either (S a = b) (LT (S a) b)
ltImpliesEqOrLT Z (S Z) (LTESucc LTEZero) = Left Refl
ltImpliesEqOrLT Z (S (S b)) (LTESucc LTEZero) = Right (LTESucc (LTESucc LTEZero))
ltImpliesEqOrLT (S a) (S b) proofSaLTSb =
	case (ltImpliesEqOrLT a b (fromLteSucc proofSaLTSb)) of
		(Left proofSaEqb) => Left (cong proofSaEqb)
		(Right proofSaLTb) => Right (LTESucc proofSaLTb)

|||Proof that a <= b implies a <= (c + b)
ltePlusConstant : {a : Nat} -> {b : Nat} -> (c : Nat) -> (LTE a b) -> (LTE a (c + b))
ltePlusConstant {a} {b} c proofLTE = lteSubstitutes (lteTransitive proofLTE (lteAddRight b)) Refl (plusCommutative b c)

|||Proof that a <= b implies (c + a) <= (c + b)
ltePlusConstantLeft : {a : Nat} -> {b : Nat} -> (c : Nat) -> (LTE a b) -> (LTE (c + a) (c + b))
ltePlusConstantLeft Z proofLTE = proofLTE
ltePlusConstantLeft (S k) proofLTE = LTESucc (ltePlusConstantLeft k proofLTE)

|||Proof that a <= b implies (a + c) <= (b + c)
ltePlusConstantRight : {a : Nat} -> {b : Nat} -> (c : Nat) -> (LTE a b) -> (LTE (a + c) (b + c))
ltePlusConstantRight {a} {b} c proofLTE =
	rewrite (plusCommutative a c) in
	rewrite (plusCommutative b c) in
	(ltePlusConstantLeft c proofLTE)

|||Proof that (c + a) <= (c + b) implies a <= b
lteMinusConstantLeft : {a : Nat} -> {b : Nat} -> {c : Nat} -> (LTE (c + a) (c + b)) -> (LTE a b)
lteMinusConstantLeft {c = Z} proofLTE = proofLTE
lteMinusConstantLeft {c = S k} (LTESucc proofLTE) = lteMinusConstantLeft {c = k} proofLTE

|||Proof that (a + c) <= (b + c) implies a <= b
lteMinusConstantRight : {a : Nat} -> {b : Nat} -> {c : Nat} -> (LTE (a + c) (b + c)) -> (LTE a b)
lteMinusConstantRight {a} {b} {c} proofLTE =
	lteMinusConstantLeft (lteSubstitutes proofLTE (plusCommutative a c) (plusCommutative b c))

|||Proof that if a <= b, and c <= d, then (a + c) <= (b + d)
ltePlusIsLTE : {a : Nat} -> {b : Nat} -> {c : Nat} -> {d : Nat} ->
			(LTE a b) -> (LTE c d) -> (LTE (a + c) (b + d))
ltePlusIsLTE {a = a0} {b = b0} {c = c0} {d = d0} proofLeftLTE proofRightLTE =
	lteTransitive (ltePlusConstantRight {a = a0} {b = b0} c0 proofLeftLTE) (ltePlusConstantLeft {a = c0} {b = d0} b0 proofRightLTE)

|||Proof that m <= (S k) * m
lteMultLeft : (k : Nat) -> (m : Nat) -> (LTE m ((S k) * m))
lteMultLeft Z m = rewrite (multOneLeftNeutral m) in (lteRefl)
lteMultLeft (S k) m = ltePlusConstant m (lteMultLeft k m)

|||Proof that if a <= b then a < (c + b) when c is not zero
ltePlusConstantLt : (c : Nat) -> (Not (c = Z)) -> (LTE a b) -> (LT a (c + b))
ltePlusConstantLt Z cnotz prf = void (cnotz Refl)
ltePlusConstantLt (S k) cnotz LTEZero = LTESucc LTEZero
ltePlusConstantLt {a = (S j)} {b = (S i)} (S k) cnotz (LTESucc prf) =
	LTESucc (rewrite (sym (plusSuccRightSucc k i)) in (ltePlusConstantLt (S k) cnotz prf))

|||Proof that a positive number (S m) is less than (S m) multiplied by a number greater that one
ltMultPosByGt1 : (k : Nat) -> (m : Nat) -> (LT (S m) ((S (S k) * (S m))))
ltMultPosByGt1 Z m = rewrite (plusZeroRightNeutral m) in ltePlusConstantLt (S m) SIsNotZ lteRefl
ltMultPosByGt1 (S k) m = ltePlusConstantLt (S m) SIsNotZ (ltImpliesLTE (ltMultPosByGt1 k m))

|||Proof that a <= b implies (c * a) <= (c * b)
lteMultConstantLeft : {a : Nat} -> {b : Nat} -> (c : Nat) -> (LTE a b) -> (LTE (c * a) (c * b))
lteMultConstantLeft {a} {b} Z _ = LTEZero
lteMultConstantLeft {a} {b} (S k) proofLTE =
	ltePlusIsLTE proofLTE (lteMultConstantLeft {a} {b} k proofLTE)

|||Proof that a <= b implies (a * c) <= (b * c)
lteMultConstantRight : {a : Nat} -> {b : Nat} -> (c : Nat) -> (LTE a b) -> (LTE (a * c) (b * c))
lteMultConstantRight {a} {b} c proofLTE = rewrite (multCommutative a c) in
								  rewrite (multCommutative b c) in
								  (lteMultConstantLeft c proofLTE)

|||Proof that if a <= b, and c <= d, then (a * c) <= (b * d)
lteMultIsLTE : {a : Nat} -> {b : Nat} -> {c : Nat} -> {d : Nat} ->
			(LTE a b) -> (LTE c d) -> (LTE (a * c) (b * d))
lteMultIsLTE {a = a0} {b = b0} {c = c0} {d = d0} proofLeftLTE proofRightLTE =
	lteTransitive (lteMultConstantRight {a = a0} {b = b0} c0 proofLeftLTE) (lteMultConstantLeft {a = c0} {b = d0} b0 proofRightLTE)

|||Proof that n is not lesser than n
succNotLTEn : {n : Nat} -> (LT n n) -> Void
succNotLTEn {n = Z} proofLTE = void (succNotLTEzero proofLTE)
succNotLTEn {n = S k} (LTESucc proofLTE) = succNotLTEn {n = k} proofLTE

|||Proof that k < n implies n != 0
gtSuccImpliesNotZ : {k : Nat} -> (n : Nat) -> (LT k n) -> (Not (n = Z))
gtSuccImpliesNotZ {k} n proofLT nIsZ = succNotLTEzero (lteSubstitutes proofLT Refl nIsZ)

|||Proof that a < b implies a != b and !(b < a)
ltImpliesNotEqNotGT : {a : Nat} -> {b : Nat} -> (LT a b) -> (Not (a = b), Not (LT b a))
ltImpliesNotEqNotGT {a} {b = Z} proofLT = void (succNotLTEzero proofLT)
ltImpliesNotEqNotGT {a = Z} {b = S l} proofLT = (ZIsNotS, succNotLTEzero)
ltImpliesNotEqNotGT {a = S k} {b = S l} (LTESucc proofLT) =
	((\proofEq => inductionStep1 (predEqual proofEq)), (\proofLT => inductionStep2 (lteMinusConstantLeft {c = 1} proofLT))) where
		inductionStep1 = fst (ltImpliesNotEqNotGT {a = k} {b = l} proofLT)
		inductionStep2 = snd (ltImpliesNotEqNotGT {a = k} {b = l} proofLT)

|||Proof that a < b implies a != b
ltImpliesNotEq : {a : Nat} -> {b : Nat} -> (LT a b) -> (Not (a = b))
ltImpliesNotEq {a} {b = Z} proofLT proofEq = succNotLTEzero proofLT
ltImpliesNotEq {a = Z} {b = (S l)} proofLT proofEq = ZIsNotS proofEq
ltImpliesNotEq {a = (S k)} {b = (S l)} (LTESucc proofLT) proofEq = ltImpliesNotEq {a = k} {b = l} proofLT (predEqual proofEq)

|||Proof that a = b implies !(a < b) and !(b < a)
eqImpliesNotLTNotGT : {a : Nat} -> {b : Nat} -> (a = b) -> (Not (LT a b), Not (LT b a))
eqImpliesNotLTNotGT {a = k} {b = k} Refl = (succNotLTEn, succNotLTEn)

|||Proof that ! (a <= b) implies (b <= a)
notLTEImpliesGTE : {a : Nat} -> {b : Nat} -> (Not (LTE a b)) -> (LTE b a)
notLTEImpliesGTE {a = Z} {b} contra = void (contra (LTEZero))
notLTEImpliesGTE {a = (S k)} {b = Z} contra = LTEZero
notLTEImpliesGTE {a = (S k)} {b = (S j)} contra =
	LTESucc (notLTEImpliesGTE {a = k} {b = j} (\evidence => contra (LTESucc evidence)))

|||Proof that (a * b) = 1 implies a = 1 and b = 1
multOneImpliesOne : {a : Nat} -> {b : Nat} -> (a * b = 1) -> (a = 1, b = 1)
multOneImpliesOne {a = Z} {b} proofEq = void (ZIsNotS proofEq)
multOneImpliesOne {a} {b = Z} proofEq = void (ZIsNotS (rewrite (sym (multZeroRightZero a)) in proofEq))
multOneImpliesOne {a = S Z} {b = S Z} _ = (Refl, Refl)
multOneImpliesOne {a = (S (S k))} {b = (S l)} proofEq = void (ltImpliesNotEq (lteTransitive (LTESucc (LTESucc LTEZero)) (fst (partsLTEsum (S (S k)) (l * (S (S k)))))) (sym (rewrite (multCommutative (S l) (S (S k))) in proofEq)))
multOneImpliesOne {a = (S k)} {b = (S (S l))} proofEq = void (ltImpliesNotEq (lteTransitive (LTESucc (LTESucc LTEZero)) (fst (partsLTEsum (S (S l)) (k * (S (S l)))))) (sym proofEq))

|||Proof that (a = k * b) and (b = l * a) implies (a = b)
multAntiSymmetric : {a : Nat} -> {b : Nat} -> {k : Nat} -> {l : Nat} ->
					(a = k * b) -> (b = l * a) -> (a = b)
multAntiSymmetric {a = Z} {b} {k} {l} proofEqLeft proofEqRight = sym (rewrite (sym (multZeroRightZero l)) in proofEqRight)
multAntiSymmetric {a = (S n)} {b} {k} {l} proofEqLeft proofEqRight =
	rewrite (sym (multOneLeftNeutral b)) in
	(trans proofEqLeft (cong {f = (\k => k * b)} (fst (multOneImpliesOne (sym (multRightCancel 1 (k * l) (S n) SIsNotZ proofEq)))))) where
		proofEq = rewrite (sym (multAssociative k l (S n))) in
				rewrite (sym proofEqRight) in
				rewrite (multOneLeftNeutral (S n)) in
				proofEqLeft

|||Returns Max of two numbers with proof that it is maximum
max : (a : Nat) -> (b : Nat) -> (n : Nat ** ((LTE a n, LTE b n), Either (a=n) (b=n)))
max a b = case isLTE a b of
	(Yes prf) => (b ** ((prf, lteRefl), (Right Refl)))
	(No contra) => (a ** ((lteRefl, (notLTEImpliesGTE contra)), (Left Refl)))

|||Proof that ! ((S a) < a)
succNotLTEnum : (a : Nat) -> (LTE (S a) a) -> Void
succNotLTEnum Z LTEZero impossible
succNotLTEnum Z (LTESucc _) impossible
succNotLTEnum (S k) (LTESucc proofLTE) = succNotLTEnum k proofLTE

|||Proof that an element of LTE m n implies an lte m n = True
LTEmeanslteTrue: (m: Nat) -> (n: Nat) -> (LTE m n) -> (lte m n = True)
LTEmeanslteTrue Z n LTEZero = Refl
LTEmeanslteTrue (S left) (S right) (LTESucc x) = LTEmeanslteTrue left right x


text:
module Mmhelloworld.IdrisSpringBoot.Boot

import IdrisJvm.IO

%access public export

SpringApplicationClass : JVM_NativeTy
SpringApplicationClass = Class "org/springframework/boot/SpringApplication"

ext: idr

max_stars_repo_name: mmhelloworld/idris-spring-boot

max_issues_repo_name: mmhelloworld/idris-spring-boot

max_forks_repo_name: mmhelloworld/idris-spring-boot


text:
module Frontend.Kotlin.Parser

import Frontend.Kotlin.AST
import Frontend.Kotlin.PrettyPrinter
import Tools.Annotation
import Lightyear.Core
import Lightyear.Char
import Lightyear.Strings
import Lightyear.Combinators
import Lightyear.Position

%access public export

--  __  __ _           ---------------------------------------------------------
-- |  \/  (_)___  ___  ---------------------------------------------------------
-- | |\/| | / __|/ __| ---------------------------------------------------------
-- | |  | | \__ \ (__  ---------------------------------------------------------
-- |_|  |_|_|___/\___| ---------------------------------------------------------
--                     ---------------------------------------------------------

TypePos      : Type
VarPos       : Type
ParamPos     : Type
ParamCPos    : Type
ClassPos     : Type
FunPos       : Type
DeclPos      : Type
FilePos      : Type
ExprPos      : Type
BlockPos     : Type
BlockExprPos : Type
AccessPos    : Type
TypePos      = SyntaxAnn TypeTy      Position
VarPos       = SyntaxAnn VarTy       Position
ParamPos     = SyntaxAnn ParamTy     Position
ParamCPos    = SyntaxAnn ParamCTy    Position
ClassPos     = SyntaxAnn ClassTy     Position
FunPos       = SyntaxAnn FunTy       Position
DeclPos      = SyntaxAnn DeclTy      Position
FilePos      = SyntaxAnn FileTy      Position
ExprPos      = SyntaxAnn ExprTy      Position
BlockPos     = SyntaxAnn BlockTy     Position
BlockExprPos = SyntaxAnn BlockExprTy Position
AccessPos    = SyntaxAnn AccessTy    Position

total filterMap : (a -> Maybe b) -> List a -> List b
filterMap f []       = []
filterMap f (h :: t) = case f h of
                            Just x  => x :: filterMap f t
                            Nothing => filterMap f t

(>>) : Monad m => m a -> m b -> m b
m >> m' = m >>= \_ => m'

infixl 10 <**>
(<**>) : Parser a -> Parser b -> Parser (Either a b)
pa <**> pb = Left  <$> pa
        <|>| Right <$> pb

unmaybe : Maybe (List a) -> List a
unmaybe Nothing  = []
unmaybe (Just l) = l

--  ____              _              -------------------------------------------
-- / ___| _   _ _ __ | |_ __ ___  __ -------------------------------------------
-- \___ \| | | | '_ \| __/ _` \ \/ / -------------------------------------------
--  ___) | |_| | | | | || (_| |>  <  -------------------------------------------
-- |____/ \__, |_| |_|\__\__,_/_/\_\ -------------------------------------------
--        |___/                      -------------------------------------------

ident : Parser String
ident = do
  h <- letter <|> char '_'
  t <- many alphaNum
  pure $ pack $ h :: t

data KeyWord = CLASS | DATA | ELSE | FALSE | FUN
             | IF | NULL | RETURN | THIS | TRUE
             | VAL | VAR | WHILE

Eq KeyWord where
  CLASS  == CLASS  = True
  DATA   == DATA   = True
  ELSE   == ELSE   = True
  FALSE  == FALSE  = True
  FUN    == FUN    = True
  IF     == IF     = True
  NULL   == NULL   = True
  RETURN == RETURN = True
  THIS   == THIS   = True
  TRUE   == TRUE   = True
  VAL    == VAL    = True
  VAR    == VAR    = True
  WHILE  == WHILE  = True
  _      == _      = False

Show KeyWord where
  show CLASS  = "class"
  show DATA   = "data"
  show ELSE   = "else"
  show FALSE  = "false"
  show FUN    = "fun"
  show IF     = "if"
  show NULL   = "null"
  show RETURN = "return"
  show THIS   = "this"
  show TRUE   = "true"
  show VAL    = "val"
  show VAR    = "var"
  show WHILE  = "while"

keyword : KeyWord -> Parser ()
keyword kw = do
  id <- ident
  case parseKey id of
       Nothing => fail $ "Expected " ++ show kw ++ ", got " ++ id
       Just k  => if k == kw then pure ()
                             else fail $ "Expected " ++ show kw ++ ", got " ++ id
 where parseKey : String -> Maybe KeyWord
       parseKey s = List.lookup s
                    [ ("class"  , CLASS  )
                    , ("data"   , DATA   )
                    , ("else"   , ELSE   )
                    , ("false"  , FALSE  )
                    , ("fun"    , FUN    )
                    , ("if"     , IF     )
                    , ("null"   , NULL   )
                    , ("return" , RETURN )
                    , ("this"   , THIS   )
                    , ("true"   , TRUE   )
                    , ("val"    , VAL    )
                    , ("var"    , VAR    )
                    , ("while"  , WHILE  )
                    ]

bit : Parser (Fin 2)
bit = do
  c <- satisfy (\x => x == '0' || x == '1')
  pure $ if c == '0' then FZ else FS (FZ)

hex : Parser (Fin 16)
hex = do
  dg <- map (ord . toUpper) hexDigit
  let val = if dg <= ord '9' then dg - ord '0' else 10 + dg - ord 'A'
  case integerToFin (cast val) 16 of
       Just fin => pure fin
       Nothing  => fail $ "Impossible : hex digit greater than 15 !"

combine : Parser a -> Parser b -> Parser (Either a b)
combine leftP rightP = (Left <$> leftP) <|> (Right <$> rightP)

valueInBase : (n : Integer) -> (Parser (Fin $ fromInteger n)) -> Parser Integer
valueInBase base digitP = do
  msd <- digitP
  tl  <- many (combine digitP (char '_'))
  let digits = msd :: filterMap extractLeft tl
  pure $ foldl (\val => \e => val * base + finToInteger e) 0 digits
 where extractLeft : Either a b -> Maybe a
       extractLeft (Left x)  = Just x
       extractLeft (Right _) = Nothing

number : Parser Integer
number = ((string "0X" <|> string "0x") >! valueInBase 16 hex)
    <|>| ((string "0B" <|> string "0b") >! valueInBase  2 bit)
    <|>| valueInBase 10 digit

car : Parser String
car = string "\\\\"
 <|>| string "\\\""
 <|>| string "\\n"
 <|>| string "\\t"
 <|>| do c <- anyChar
         guard (ord c >= 32 && ord c <= 126 && c /= '\\' && c /= '"')
         pure $ singleton c

string : Parser String
string = concat <$> between (char '"') (char '"') (many car)

mutual
  commentStarString : Parser ()
  commentStarString = (skip $ string "*/")
                 <|>| (commentStar >> commentStarString)
                 <|>| (anyChar >> commentStarString)

  commentStar : Parser ()
  commentStar = string "/*" >! commentStarString

mutual
  commentLineString : Parser ()
  commentLineString = (skip $ endOfLine)
                 <|>| (anyChar >> commentLineString)

  commentLine : Parser ()
  commentLine = string "//" >! commentLineString

comment : Parser ()
comment = commentStar <|>| commentLine

white : Parser ()
white = skip $ many $ (skip $ oneOf " \t\n") <|>| comment

white1 : Parser ()
white1 = skip $ some $ (skip $ oneOf " \t\n") <|>| comment

wstring : String -> Parser ()
wstring str = white >> string str >> white

--  _____                   ____                           ---------------------
-- |_   _|   _ _ __   ___  |  _ \ __ _ _ __ ___  ___ _ __  ---------------------
--   | || | | | '_ \ / _ \ | |_) / _` | '__/ __|/ _ \ '__| ---------------------
--   | || |_| | |_) |  __/ |  __/ (_| | |  \__ \  __/ |    ---------------------
--   |_| \__, | .__/ \___| |_|   \__,_|_|  |___/\___|_|    ---------------------
--       |___/|_|                                          ---------------------

mutual
  typeP : Parser TypePos
  typeP = do
    p  <- getPosition
    tp <- typeNonNull
    mb <- opt $ white >> char '?'
    pure $ case mb of
      Nothing => tp
      Just _  => case tp of
       Ann p' (TNull t) => Ann p' $ TNull t
       _                => Ann p $ TNull tp

  typeNonNull : Parser TypePos
  typeNonNull = typeParenOrFun <|>| commitTo typeParams

  typeParams : Parser TypePos
  typeParams = do
    p  <- getPosition
    tp <- ident
    mtps <- opt $ white >> char '<' >! do
      tps <- sepBy1 typeP $ wstring ","
      skip $ white >> char '>'
      pure $ tps
    pure $ Ann p $ TParam tp $ fromMaybe [] mtps

  typeParenOrFun : Parser TypePos
  typeParenOrFun = do
    p   <- getPosition
    tps <- parens (sepBy typeP $ wstring ",")
    ret <- opt $ wstring "->" >> commitTo typeP
    case ret of
      Nothing => case tps of
                   [tp] => pure tp
                   _    => fail "Invalid syntax"
      Just rt => pure $ Ann p $ TFun tps rt

--  ____                             ____                           ------------
-- |  _ \ __ _ _ __ __ _ _ __ ___   |  _ \ __ _ _ __ ___  ___ _ __  ------------
-- | |_) / _` | '__/ _` | '_ ` _ \  | |_) / _` | '__/ __|/ _ \ '__| ------------
-- |  __/ (_| | | | (_| | | | | | | |  __/ (_| | |  \__ \  __/ |    ------------
-- |_|   \__,_|_|  \__,_|_| |_| |_| |_|   \__,_|_|  |___/\___|_|    ------------
--                                                                  ------------

mutual
  paramP : Parser ParamPos
  paramP = do
    p  <- getPosition
    id <- ident
    white
    skip $ string ":"
    white
    tp <- typeP
    pure $ Ann p $ Param id tp

--  ____                            ____   ____                           ------
-- |  _ \ __ _ _ __ __ _ _ __ ___  / ___| |  _ \ __ _ _ __ ___  ___ _ __  ------
-- | |_) / _` | '__/ _` | '_ ` _ \| |     | |_) / _` | '__/ __|/ _ \ '__| ------
-- |  __/ (_| | | | (_| | | | | | | |___  |  __/ (_| | |  \__ \  __/ |    ------
-- |_|   \__,_|_|  \__,_|_| |_| |_|\____| |_|   \__,_|_|  |___/\___|_|    ------
--                                                                        ------

mutual
  paramCP : Parser ParamCPos
  paramCP = do
    p    <- getPosition
    qual <- string "var" <|>| string "val"
    white1
    id   <- ident
    wstring ":"
    tp   <- typeP
    pure $ Ann p $ if qual == "var" then PCVar id tp
                                    else PCVal id tp

--  _____                   ____                           ---------------------
-- | ____|_  ___ __  _ __  |  _ \ __ _ _ __ ___  ___ _ __  ---------------------
-- |  _| \ \/ / '_ \| '__| | |_) / _` | '__/ __|/ _ \ '__| ---------------------
-- | |___ >  <| |_) | |    |  __/ (_| | |  \__ \  __/ |    ---------------------
-- |_____/_/\_\ .__/|_|    |_|   \__,_|_|  |___/\___|_|    ---------------------
--            |_|                                          ---------------------

mutual
  exprP : Parser ExprPos
  exprP = exprP10

  exprP10 : Parser ExprPos
  exprP10 = exprIf <|>| exprP9

  exprIf : Parser ExprPos
  exprIf = getPosition >>= \p => keyword IF >! do
    wstring "("
    cond <- exprP
    wstring ")"
    body <- blockExprP
    els  <- opt $ do
      white
      keyword ELSE
      white
      blockExprP
    pure $ Ann p $ EIfElse cond body $ case els of
                                         Nothing => Ann p $ BEBlock $ Ann p $ BEmpty
                                         Just el => el

  exprP9 : Parser ExprPos
  exprP9 = exprReturn <|>| exprWhile <|>| exprP8

  exprReturn : Parser ExprPos
  exprReturn = keyword RETURN >! white1 >> exprP

  exprWhile : Parser ExprPos
  exprWhile = getPosition >>= \p => keyword WHILE >! do
    wstring "("
    cond <- exprP
    wstring ")"
    body <- blockExprP
    pure $ Ann p $ EWhile cond body

  exprP8 : Parser ExprPos
  exprP8 = do
    p  <- getPosition
    e1 <- exprP7
    white
    e2 <- opt $ parseEq p e1
    pure $ case e2 of
      Nothing => e1
      Just e' => e'
   where parseEq : Position -> ExprPos -> Parser ExprPos
         parseEq p e1 = do
           skip $ string "="
           white
           er <- exprP
           case e1 of
             Ann _ (EAccess access) => pure $ Ann p $ EAss access er
             _                      => fail "Expected access"

  exprP7 : Parser ExprPos
  exprP7 = do
    p  <- getPosition
    e1 <- exprP6
    white
    e2 <- opt $ binopP p e1 Or exprP7
    pure $ case e2 of
      Nothing => e1
      Just e' => e'

  exprP6 : Parser ExprPos
  exprP6 = do
    p  <- getPosition
    e1 <- exprP5
    white
    e2 <- opt $ binopP p e1 And exprP6
    pure $ case e2 of
      Nothing => e1
      Just e' => e'

  exprP5 : Parser ExprPos
  exprP5 = do
    p  <- getPosition
    e1 <- exprP4
    white
    e2 <- opt $ ( binopP p e1 RefEq     exprP5
             <|>| binopP p e1 RefNeq    exprP5
             <|>| binopP p e1 StructEq  exprP5
             <|>| binopP p e1 StructNeq exprP5)
    pure $ case e2 of
      Nothing => e1
      Just e' => e'

  exprP4 : Parser ExprPos
  exprP4 = do
    p  <- getPosition
    e1 <- exprP3
    white
    e2 <- opt $ ( binopP p e1 Lt exprP4
             <|>| binopP p e1 Le exprP4
             <|>| binopP p e1 Gt exprP4
             <|>| binopP p e1 Ge exprP4)
    pure $ case e2 of
      Nothing => e1
      Just e' => e'

  exprP3 : Parser ExprPos
  exprP3 = do
    p  <- getPosition
    e1 <- exprP2
    white
    e2 <- opt $ ( binopP p e1 Plus exprP3
             <|>| binopP p e1 Subs exprP3)
    pure $ case e2 of
      Nothing => e1
      Just e' => e'

  exprP2 : Parser ExprPos
  exprP2 = do
    p  <- getPosition
    e1 <- exprP1
    white
    e2 <- opt $ ( binopP p e1 Mult   exprP2
             <|>| binopP p e1 Div    exprP2
             <|>| binopP p e1 Modulo exprP2)
    pure $ case e2 of
      Nothing => e1
      Just e' => e'

  binopP : Position -> ExprPos -> Operator -> Parser ExprPos -> Parser ExprPos
  binopP p al op p2 = (string $ show op) >! do
    white
    ar <- p2
    pure $ Ann p $ EOp op al ar

  exprP1 : Parser ExprPos
  exprP1 = getPosition >>= \p => ( string "-" >! white >> exprMinusP p
                              <|>| string "!" >! white >> (Ann p <$> (ENot   <$> exprP1))
                              <|>| exprP0 )

  exprMinusP : Position -> Parser ExprPos
  exprMinusP p = do
    e <- exprP1
    pure $ Ann p $ case e of
      Ann _ (EInt i) => EInt $ -i
      _              => EMinus e

  exprP0 : Parser ExprPos
  exprP0 = do
    p     <- getPosition
    start <- exprP0'
    subs  <- many subP
    pure $ foldl (\ep => \(sym,p',sub) => Ann p $ EAccess $ Ann p'
                                        $ if sym == "?." then ANSub ep sub else ASub ep sub)
                 start subs
   where subP : Parser (String, Position, Ident)
         subP = do
           white
           str <- string "?." <|>| string "."
           white
           p   <- getPosition
           sub <- ident
           pure $(str, p, sub)

  exprP0' : Parser ExprPos
  exprP0' = getPosition >>= \p => ( keyword TRUE  >> pure (Ann p ETrue)
                               <|>| keyword FALSE >> pure (Ann p EFalse)
                               <|>| keyword THIS  >> pure (Ann p EThis)
                               <|>| keyword NULL  >> pure (Ann p ENull)
                               <|>| Ann p <$> (EInt <$> number)
                               <|>| Ann p <$> (EStr <$> string)
                               <|>| keyword FUN >! efunP p
                               <|>| string "(" >> white >>
                                      (exprP >>= \p => white >> string ")" >> pure p)
                               <|>| callP
                               <|>| Ann p <$> (EAccess <$> (Ann p <$> (AIdent <$> ident))))

  efunP : Position -> Parser ExprPos
  efunP p = do
    wstring "("
    args <- sepBy paramP $ wstring ","
    wstring ")"
    tp   <- opt $ string ":" >! white >> typeP
    let typ = case tp of
                Nothing => Ann p $ TParam "Unit" []
                Just t  => t
    white
    body <- blockP
    pure $ Ann p $ EFun args typ body

  callP : Parser ExprPos
  callP = getPosition >>= \p =>
          ident >>= \id =>
          wstring "(" >>= \_ => commitTo $ do
    args <- sepBy exprP $ wstring ","
    white
    string ")"
    pure $ Ann p $ ECall id args

  blockP : Parser BlockPos
  blockP = string "{" >>= \_ => commitTo $ do
    white
    body <- sepBy (varP <**> exprP) $ wstring ";"
    if length body > 0 then opt $ white >> string ";" else pure Nothing
    white
    p <- getPosition
    skip $ string "}"
    pure $ foldr storer (Ann p BEmpty) body
   where storer : Either VarPos ExprPos
               -> BlockPos -> BlockPos
         storer (Left  (Ann p var))  acc = Ann p $ BVar  (Ann p var)  acc
         storer (Right (Ann p expr)) acc = Ann p $ BExpr (Ann p expr) acc

  blockExprP : Parser BlockExprPos
  blockExprP = Ann <$> getPosition <*> ( BEBlock <$> blockP
                                    <|>| BEExpr  <$> commitTo exprP)

  varP : Parser VarPos
  varP = do
    p    <- getPosition
    qual <- string "var" <|>| string "val"
    white1
    id   <- ident
    tp   <- opt $ wstring ":" >! typeP
    wstring "="
    expr <- exprP
    pure $ Ann p $ if qual == "var" then VVar id tp expr
                                    else VVal id tp expr

--   ____ _                 ____                           ---------------------
--  / ___| | __ _ ___ ___  |  _ \ __ _ _ __ ___  ___ _ __  ---------------------
-- | |   | |/ _` / __/ __| | |_) / _` | '__/ __|/ _ \ '__| ---------------------
-- | |___| | (_| \__ \__ \ |  __/ (_| | |  \__ \  __/ |    ---------------------
--  \____|_|\__,_|___/___/ |_|   \__,_|_|  |___/\___|_|    ---------------------
--                                                         ---------------------

mutual
  classP : Parser ClassPos
  classP = do
    p <- getPosition
    keyword DATA
    white1
    keyword CLASS
    white1
    name   <- ident
    params <- opt $ wstring "<" >! do
      prms <- sepBy1 ident $ wstring ","
      white
      skip $ string ">"
      pure prms
    wstring "("
    args   <- sepBy1 paramCP $ wstring ","
    wstring ")"
    body   <- opt $ wstring "{" >! do
      vars <- sepBy varP $ wstring ";"
      if length vars > 0 then opt $ wstring ";" else pure Nothing
      white
      skip $ string "}"
      pure vars
    pure $ Ann p $ Class name (unmaybe params) args (unmaybe body)

--  _____              ____                           --------------------------
-- |  ___|   _ _ __   |  _ \ __ _ _ __ ___  ___ _ __  --------------------------
-- | |_ | | | | '_ \  | |_) / _` | '__/ __|/ _ \ '__| --------------------------
-- |  _|| |_| | | | | |  __/ (_| | |  \__ \  __/ |    --------------------------
-- |_|   \__,_|_| |_| |_|   \__,_|_|  |___/\___|_|    --------------------------
--                                                    --------------------------

mutual
  funP : Parser FunPos
  funP = do
    p <- getPosition
    keyword FUN
    params <- opt $ wstring "<" >! do
      prms <- sepBy1 ident $ wstring ","
      white
      skip $ string ">"
      pure prms
    white
    name   <- ident
    wstring "("
    args   <- sepBy paramP $ wstring ","
    white
    skip $ string ")"
    tp     <- opt $ wstring ":" >! typeP
    let typ = case tp of
                Nothing => Ann p $ TParam "Unit" []
                Just t  => t
    white
    body   <- blockP
    pure $ Ann p $ Fun (unmaybe params) name args typ body

--  ____            _   ____                           -------------------------
-- |  _ \  ___  ___| | |  _ \ __ _ _ __ ___  ___ _ __  -------------------------
-- | | | |/ _ \/ __| | | |_) / _` | '__/ __|/ _ \ '__| -------------------------
-- | |_| |  __/ (__| | |  __/ (_| | |  \__ \  __/ |    -------------------------
-- |____/ \___|\___|_| |_|   \__,_|_|  |___/\___|_|    -------------------------
--                                                     -------------------------

mutual
  declP : Parser DeclPos
  declP = getPosition >>= \p => Ann p <$> declP'

  declP' : Parser (SyntaxF (\id => SyntaxAnn id Position) DeclTy)
  declP' = DFun   <$> funP
      <|>| DClass <$> classP
      <|>| DVar   <$> (varP >>= \v => white >> string ";" >> pure v)

--  _____ _ _        ____                           ----------------------------
-- |  ___(_) | ___  |  _ \ __ _ _ __ ___  ___ _ __  ----------------------------
-- | |_  | | |/ _ \ | |_) / _` | '__/ __|/ _ \ '__| ----------------------------
-- |  _| | | |  __/ |  __/ (_| | |  \__ \  __/ |    ----------------------------
-- |_|   |_|_|\___| |_|   \__,_|_|  |___/\___|_|    ----------------------------
--                                                  ----------------------------

mutual
  fileP : Parser FilePos
  fileP = do
    p     <- getPosition
    white
    decls <- sepBy declP white
    white
    eof
    pure $ Ann p $ File decls


text:
module GLCore

import Types

-- Create the WebGL context from a canvas element
getGLCxt : Element -> IO GLCxt
getGLCxt (MkElem e) = do
  x <- mkForeign (FFun "%0.getContext('webgl')" [FPtr] FPtr) e
  return (MkCxt x)

-- Create a program for building and linking shaders
createProg : GLCxt -> IO GLProgram
createProg (MkCxt x) = do
  p <- mkForeign (FFun "%0.createProgram()" [FPtr] FPtr) x
  return (MkGLProg p)

-- Assign the program to the given webGL context
useProg : (GLProgram, GLCxt) -> IO (GLProgram, GLCxt)
useProg ((MkGLProg y),(MkCxt x)) = do
  mkForeign (FFun "%0.useProgram(%1)" [FPtr,FPtr] FUnit) x y
  return ((MkGLProg y), (MkCxt x))

-- Enable a specific GL setting. I don't know how to access enum properties
-- using the JavaScript FFI yet so this is a bit filthy but easy to change.
enableGLSetting : GLCxt -> IO GLCxt
enableGLSetting (MkCxt c) = do
  _ <- mkForeign (FFun "%0.enable(%0.DEPTH_TEST)" [FPtr] FUnit) c
  return (MkCxt c)

-- Again with the enum properties. But this clears the current context.
glClear : GLCxt -> IO GLCxt
glClear (MkCxt c) = do
  mkForeign (FFun "%0.clear(%0.COLOR_BUFFER_BIT | %0.DEPTH_BUFFER_BIT)" [FPtr] FUnit) c
  return (MkCxt c)

-- Assign a clear colour to the entire gl region.
clearColor : GLCxt -> IO GLCxt
clearColor (MkCxt c) = do
  mkForeign (FFun "%0.clearColor(0.0,0.0,0.0,0.1)" [FPtr] FUnit) c
  return (MkCxt c)

-- Choose a depth effect function - this time we choose to hide objects
-- that are 'behind' closer objects.
depthFun : GLCxt -> IO GLCxt
depthFun (MkCxt c) = do
  mkForeign (FFun "%0.depthFunc(%0.LEQUAL)" [FPtr] FUnit) c
  return (MkCxt c)

-- Create a buffer
-- var vertexPosBuffer = gl.createBuffer()
createBuffer : GLCxt -> IO GLBuffer
createBuffer (MkCxt c) = do
  b <- mkForeign (FFun "%0.createBuffer()" [FPtr] FPtr) c
  return (MkBuf b)

-- Bind the buffer
-- gl.bindBuffer(gl.ARRAY_BUFFER, vertextPosBuffer)
bindArrayBuffer : GLCxt -> GLBuffer -> IO GLCxt
bindArrayBuffer (MkCxt c) (MkBuf b) = do
  mkForeign (FFun "%0.bindBuffer(%0.ARRAY_BUFFER, %1)" [FPtr,FPtr] FUnit) c b
  return (MkCxt c)

-- Retrieve the array buffer type value
bufferType : GLCxt -> IO Int
bufferType (MkCxt c) = mkForeign (FFun "%0.ARRAY_BUFFER" [FPtr] FInt) c
-- Retrieve the static draw style value
drawStyle : GLCxt -> IO Int
drawStyle (MkCxt c) = mkForeign (FFun "%0.STATIC_DRAW" [FPtr] FInt) c

-- Load the buffer data
-- gl.bufferData(gl.ARRAY_BUFFER, new Float32Array(vertices), gl.STATIC_DRAW)
bufferVertexData : F32Array -> GLCxt -> IO GLCxt
bufferVertexData (MkF32Array xs) (MkCxt c) = do
  bType <- bufferType (MkCxt c)
  style <- drawStyle (MkCxt c)
  mkForeign (FFun "%0.bufferData(%1, %2, %3)" [FPtr,FInt,FPtr,FInt] FUnit) c bType xs style
  return (MkCxt c)

-- call gl.drawArrays to specifically draw triangles.
-- First argument is the current program/glcontext
-- start = where on the vertex array to start reading vertices
-- nVertices = number of vertices to be read
drawTriangles : (GLProgram,GLCxt) -> Int -> Int -> IO (GLProgram,GLCxt)
drawTriangles ((MkGLProg p),(MkCxt c)) start nVertices = do
  mkForeign (FFun "%0.drawArrays(%0.TRIANGLES, %1,%2)" [FPtr,FInt,FInt] FUnit) c start nVertices
  return ((MkGLProg p),(MkCxt c))

max_stars_repo_name: mankyKitty/idris-webgl

max_issues_repo_name: mankyKitty/idris-webgl

max_forks_repo_name: mankyKitty/idris-webgl


text:
module Buffer

import Data.Vect

import SizedStrings
import Lines
import Cursor
import Movement
import MaybeFin

%default total
%access public

abstract
data Buffer : Nat -> Type where
  Buffer' : .{size : Vect (S n) Nat} ->
            (linez : Lines size) ->
            (cursor : Cursor n) ->
            Buffer n

%name Buffer buffer

emptyBuffer : Buffer Z
emptyBuffer = Buffer' [empty] zeroCursor

readIntoBuffer : (xs: List String) -> Buffer (pred $ length xs)
readIntoBuffer [] = emptyBuffer
readIntoBuffer (x :: xs) = Buffer' (readFromList $ x :: xs) zeroCursor

writeToList : Buffer n -> List String
writeToList (Buffer' l _) = writeLinesToList l

private
moveByChar : Buffer n -> Move ByCharacter -> Buffer n
moveByChar (Buffer' lines cursor) movement =
  let newCursor = moveByChar movement (length $ index (rowIndex cursor) lines) cursor
  in Buffer' lines newCursor

private
moveByLine : Buffer n -> Move ByLine -> Buffer n
moveByLine (Buffer' lines cursor) movement =
  Buffer' lines (moveByLine movement cursor)

move : Buffer n -> Move by -> Buffer n
move {by = ByCharacter} = moveByChar
move {by = ByLine} = moveByLine

charUnderCursor : Buffer n -> Maybe Char
charUnderCursor (Buffer' linez cursor) =
  charAt (rowIndex cursor) (columnCursor cursor) linez

deleteLine : Buffer n -> Buffer (pred n)
deleteLine {n = Z} _ = emptyBuffer
deleteLine {n = (S _)} (Buffer' linez cursor) =
  let newLines = deleteLine (rowIndex cursor) linez
      newCursor = deleteLine cursor
  in Buffer' newLines newCursor

insertLineAbove : Buffer n -> Buffer (S n)
insertLineAbove (Buffer' linez cursor) =
  let newLines = insertLine (weaken $ rowIndex cursor) empty linez
      newCursor = insertLineAbove cursor
  in Buffer' newLines newCursor

changeChar : Buffer n -> Char -> Buffer n
changeChar (Buffer' linez cursor) c =
  let row = rowIndex cursor
      maybeColumn = columnCursor cursor
  in Buffer' (replaceChar row maybeColumn c linez) cursor

insertTextAfterCursor : Buffer n -> SizedString l -> Buffer n
insertTextAfterCursor (Buffer' linez cursor) str =
  let newLinez = insertAfter (rowIndex cursor) (columnCursor cursor) str linez
      newCursor = insertAfter l cursor
  in Buffer' newLinez newCursor

insertTextBeforeCursor : Buffer n -> SizedString l -> Buffer n
insertTextBeforeCursor (Buffer' linez cursor) str =
  let newLinez = insertBefore (rowIndex cursor) (columnCursor cursor) str linez
      newCursor = insertBefore l cursor
  in Buffer' newLinez newCursor

deleteCharUnderCursor : Buffer n -> Buffer n
deleteCharUnderCursor (Buffer' linez cursor) =
  let newLinez = deleteChar (rowIndex cursor) (columnCursor cursor) linez
  in Buffer' newLinez cursor


text:
module NatDivisors

import NatUtils
import NatOrder

%default total
%access public export

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

--Definitions involving divisibility

|||Type of proof that d divides n
isDivisible : (n : Nat) -> (d : Nat) -> Type
isDivisible n d = (k : Nat ** (n = k * d, Not (d = Z)))

|||Type of proof that d is a common divisor of a and b
isCommonDivisor : (a : Nat) -> (b : Nat) -> (d : Nat) -> Type
isCommonDivisor a b d = (isDivisible a d, isDivisible b d)

|||Type of proof that a given number is "larger" than all common divisors of a and b
isMaxDivisor : (a : Nat) -> (b : Nat) -> (d : Nat) -> Type
isMaxDivisor a b d = (n : Nat) -> (isCommonDivisor a b n) -> (isDivisible d n)

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

-- Division algorithms to get the quotient and reminder

||| Given a, b, and a proof that b != 0, returns q, r and proofs that a = r + (b * q) and  r < b (r < b as LT r b)
--removed possible problems with Rohit's
euclidDivideOld : (a : Nat) -> (b : Nat) -> (Not (b = Z)) ->
			   (q : Nat ** (r : Nat ** ((a = r + (q * b)), LT r b)))
euclidDivideOld _ Z proofEq = void (proofEq Refl)
euclidDivideOld Z (S k) SIsNotZ = (Z ** (Z ** (Refl, LTESucc LTEZero)))
euclidDivideOld (S n) (S k) SIsNotZ =
	case (euclidDivideOld n (S k) SIsNotZ) of
	(q ** (r ** (proofEq, ltproof))) =>
		case (ltImpliesEqOrLT r (S k) ltproof) of
		(Right proofSrLTSk) => (q ** ((S r) ** ((cong proofEq), proofSrLTSk)))
		(Left proofSrEqSk) => ((S q) ** (Z ** ((trans (cong proofEq) (plusConstantRight (S r) (S k) (q * (S k)) proofSrEqSk)), LTESucc LTEZero)))

||| Given a, b, and a proof that b != 0, returns (q, r) and proofs that a = r + q * b and r < b (r < b as LNEQ r b)
euclidDivide : (a : Nat) -> (b : Nat) -> (Not (b = Z)) ->
			(q : Nat ** (r : Nat ** (a = r + (q * b), LNEQ r b)))
euclidDivide _ Z proofeq = void (proofeq Refl)
euclidDivide Z (S k) SIsNotZ = (Z ** (Z ** (Refl, (LEQZero, ZIsNotS))))
euclidDivide (S n) (S k) SIsNotZ =
	case (euclidDivide n (S k) SIsNotZ) of
		(q ** (r ** (proofEq, proofLNEQ))) =>
			case (lneqImpliesEqOrLNEQ r (S k) proofLNEQ) of
				(Right proofSrLNEQSk) => (q ** ((S r) ** ((cong proofEq), proofSrLNEQSk)))
				(Left proofSrEqSk) => ((S q) ** (Z ** ((trans (cong proofEq) (plusConstantRight (S r) (S k) (q * (S k)) proofSrEqSk)), (LEQZero, ZIsNotS))))

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

-- General recursive functions for proofs using Euclid's division algorithms

|||A general algorithm that runs recursively using Euclid's division, with proof (helper function with bound, use euclidRecursion instead)
euclidRecursionBound : (bound : Nat) -> (a : Nat) -> (b : Nat) -> (LTE a bound) -> (LTE (S b) bound) -> (Either (Not (a = Z)) (Not (b = Z))) ->
(proofType : (Nat -> Nat -> Type)) ->
(baseLeft : (k : Nat) -> (Not (k = Z)) -> (proofType k Z)) ->
(baseRight : (k : Nat) -> (Not (k = Z)) -> (proofType Z k)) ->
(proofExtend : {a1 : Nat} -> {b1 : Nat} -> {r1 : Nat} -> {q1 : Nat} -> (proofType b1 r1) -> (a1 = r1 + (q1 * b1)) -> (proofType a1 b1)) ->
(proofType a b)

euclidRecursionBound _ Z Z _ _ notBothZ _ _ _ _ =
	case notBothZ of
		Left notZ => void (notZ Refl)
		Right notZ => void (notZ Refl)

euclidRecursionBound bound (S a) Z _ _ _ _ baseLeft _ _ = baseLeft (S a) SIsNotZ
euclidRecursionBound bound Z (S b) _ _ _ _ _ baseRight _ = baseRight (S b) SIsNotZ

euclidRecursionBound Z (S a) (S b) lteLeft lteRight _ _ _ _ _ = void (succNotLTEzero lteLeft)

euclidRecursionBound (S bound) (S a) (S b) (LTESucc lteLeft) (LTESucc lteRight) _
proofType baseLeft baseRight proofExtend =
	case (euclidDivide (S a) (S b) SIsNotZ) of
		(q ** (r ** (proofEq, proofLNEQ))) =>
			case (euclidRecursionBound bound (S b) r lteRight (lteTransitive (lneqToLT proofLNEQ) lteRight) (Left SIsNotZ) proofType baseLeft baseRight proofExtend) of
				proofRemainder => proofExtend proofRemainder proofEq

|||A general algorithm that runs recursively using Euclid's division, with proof
euclidRecursion : (a : Nat) -> (b : Nat) -> (Either (Not (a = Z)) (Not (b = Z))) ->
(proofType : (Nat -> Nat -> Type)) ->
(baseLeft : (k : Nat) -> (Not (k = Z)) -> (proofType k Z)) ->
(baseRight : (k : Nat) -> (Not (k = Z)) -> (proofType Z k)) ->
(proofExtend : {a1 : Nat} -> {b1 : Nat} -> {r1 : Nat} -> {q1 : Nat} -> (proofType b1 r1) -> (a1 = r1 + (q1 * b1)) -> (proofType a1 b1)) ->
(proofType a b)

euclidRecursion a b notBothZ proofType baseLeft baseRight proofExtend =
	case (isLTE a b) of
		(Yes proofLTE) => euclidRecursionBound (S b) a b (lteTransitive proofLTE (lteSuccRight lteRefl)) lteRefl notBothZ proofType baseLeft baseRight proofExtend
		(No proofNotLTE) => euclidRecursionBound (S a) a b (lteSuccRight lteRefl) (LTESucc (notLTEImpliesGTE proofNotLTE)) notBothZ proofType baseLeft baseRight proofExtend

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

--Basic utility functions involving divisibility

|||Proof d1 divides a1 and a1 = a2, d1 = d2 implies d2 divides a2
eqConservesDivisible : {a1 : Nat} -> {a2 : Nat} -> {d1 : Nat} -> {d2 : Nat} ->
				   (isDivisible a1 d1) -> (a1 = a2) -> (d1 = d2) -> (isDivisible a2 d2)
eqConservesDivisible {a1} {d1} proofDivides Refl Refl = proofDivides

|||Proof that all natural numbers divide zero
zeroDivisible : {n : Nat} -> (Not (n = Z)) -> (isDivisible Z n)
zeroDivisible {n} notZ = (Z ** (sym (multZeroLeftZero n), notZ))

|||Proof that 1 divides all natural numbers
oneDivides : {n : Nat} -> (isDivisible n (S Z))
oneDivides {n} = (n ** ((rewrite (multOneRightNeutral n) in Refl), SIsNotZ))

|||Proof that all natural numbers divide themselves
divisionReflexive : {n : Nat} -> (Not (n = Z)) -> (isDivisible n n)
divisionReflexive {n} notZ = (1 ** (rewrite (multOneLeftNeutral n) in Refl, notZ))

|||Proof that 1 is a common divisor of all pairs of natural numbers
oneCommonDivisor : {a : Nat} -> {b : Nat} -> (isCommonDivisor a b (S Z))
oneCommonDivisor {a} {b} = (oneDivides, oneDivides)

|||Proof that n is a common divisor of n and 0
zeroCommonDivisorRight : {n : Nat} -> (Not (n = Z)) -> (isCommonDivisor n Z n)
zeroCommonDivisorRight {n} notZ = (divisionReflexive notZ, zeroDivisible notZ)

|||Proof that n is a common divisor of 0 and n
zeroCommonDivisorLeft : {n : Nat} -> (Not (n = Z)) -> (isCommonDivisor Z n n)
zeroCommonDivisorLeft {n} notZ = (zeroDivisible notZ, divisionReflexive notZ)

|||Proof that a common divisor of (a, b) is a common divisor of (b, a)
commonDivisorSymmetric : {a : Nat} -> {b : Nat} -> {d : Nat} ->
					(isCommonDivisor a b d) -> (isCommonDivisor b a d)
commonDivisorSymmetric {a} {b} {d} (proofDividesa, proofDividesb) =
	(proofDividesb, proofDividesa)

|||Proof that a divides b and b divides a implies a = b
dividesAntiSymmetric : {a : Nat} -> {b : Nat} ->
				   (isDivisible a b) -> (isDivisible b a) -> (a = b)
dividesAntiSymmetric {a} {b} (k ** (leftEq, leftNotZ)) (l ** (rightEq, rightNotZ)) =
	multAntiSymmetric leftEq rightEq

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

--Utility functions for linear combinations

|||Proof that d divides a implies d divides n * a
dividesMultiple : {a : Nat} -> {d : Nat} ->
			   (isDivisible a d) -> (n : Nat) -> (isDivisible (n * a) d)
dividesMultiple {a} {d} (k ** (proofDiv, notZ)) n = ((n * k) ** (proofEq, notZ)) where
	proofEq = rewrite (sym (multAssociative n k d)) in
			cong {f = (\l => n * l)} proofDiv

|||Proof that a divides n and b divides (n/a) implies b * a divides n
multipleDivides : {n : Nat} -> {a : Nat} -> {b : Nat} -> (proofDiv : isDivisible n a) ->
			   (isDivisible (fst proofDiv) b) -> (isDivisible n (b * a))
multipleDivides {n} {a} {b} (k ** (proofDiv1, aNotZ)) (l ** (proofDiv2, bNotZ)) =
	(l ** (proofEq, nonZeroMultNotZero bNotZ aNotZ)) where
		proofEq = rewrite (multAssociative l b a) in
				rewrite (sym proofDiv2) in proofDiv1

|||Proof that d divides a and n != 0 implies (n * d) divides (n * a)
multipleDividesMultiple : {a : Nat} -> {d : Nat} -> (isDivisible a d) ->
					 (n : Nat) -> (Not (n = Z)) -> (isDivisible (n * a) (n * d))
multipleDividesMultiple {a} {d} (k ** (proofDiv, dNotZ)) n nNotZ =
	(k ** (proofEqExtend, (nonZeroMultNotZero nNotZ dNotZ))) where
		proofEqExtend = rewrite (multAssociative k n d) in
					 rewrite (multCommutative k n) in
					 rewrite (sym (multAssociative n k d)) in
					 cong {f = (\l => (n * l))} proofDiv

|||Proof that d is a common divisor of a and b implies d divides a + b
dividesSum : {a : Nat} -> {b : Nat} -> {d : Nat} ->
		   (isCommonDivisor a b d)-> (isDivisible (a + b) d)
dividesSum {a} {b} {d} ((m ** (proofDividesa, dNotZ1)), (n ** (proofDividesb, dNotZ2))) =
	((m + n) ** ((distributeProof a b d m n proofDividesa proofDividesb), dNotZ1))

|||Proof that d is a common divisor of a and b implies d divides x * a + y * b
dividesLinearCombination : {a : Nat} -> {b : Nat} -> {d : Nat} ->
					  (isCommonDivisor a b d) -> (x : Nat) -> (y : Nat) ->
					  (isDivisible ((x * a) + (y * b)) d)
dividesLinearCombination commonDivisorProof x y =
	dividesSum ((dividesMultiple (fst commonDivisorProof) x), (dividesMultiple (snd commonDivisorProof) y))

|||Proof that d divides (a + b) and d divides b implies d divides a
dividesDifference : {a : Nat} -> {b : Nat} -> {d : Nat} ->
				(isDivisible (a + b) d) -> (isDivisible b d) -> (isDivisible a d)
dividesDifference {a} {b} {d} (n ** (proofDivSum, dNotZ1)) (m ** (proofDivb, dNotZ2)) =
	case (leqDivConstantRight dNotZ1 (eqPreservesLEQ (a ** (plusCommutative b a)) proofDivb proofDivSum)) of
	(l ** proofEq) =>
		(l ** (sym (plusLeftCancel b (l * d) a (rewrite (plusCommutative b a) in (rewrite proofDivSum in (rewrite proofDivb in (trans (sym (multDistributesOverPlusLeft m l d)) (cong {f = (\n => n * d)} proofEq)))))), dNotZ1))

|||Proof that d divides b, d divides r and a = r + q * b implies d divides a
dividesSumExtend : {a : Nat} -> {b : Nat} -> {q : Nat} -> {r : Nat} ->
			    (isDivisible b d) -> (isDivisible r d) -> (a = r + (q * b)) ->
			    (isDivisible a d)
dividesSumExtend {a} {b} {q} {r} divB divR proofEq =
	(eqConservesDivisible (dividesSum (divR, dividesMultiple divB q)) (sym proofEq) Refl)

|||Proof that d divides a, d divides b and a = r + q * b implies d divides r
dividesDiffExtend : {a : Nat} -> {b : Nat} -> {q : Nat} -> {r : Nat} ->
				(isDivisible a d) -> (isDivisible b d) -> (a = r + (q * b)) -> (isDivisible r d)
dividesDiffExtend {a} {b} {q} {r} divA divB proofEq =
	dividesDifference (eqConservesDivisible divA proofEq Refl) (dividesMultiple divB q)

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

-- Proofs involving divisibility with remainders

|||Proof that given a = r + q * b, and d divides b and r, d divides a and b
remExtendsCommDiv : {a : Nat} -> {b : Nat} -> {q : Nat} -> {r : Nat} -> {d : Nat} ->
				(isCommonDivisor b r d) -> (a = r + (q * b)) -> (isCommonDivisor a b d)
remExtendsCommDiv {a} {b} {q} {r} (divB, divR) proofEq = (divA, divB) where
	divA = dividesSumExtend divB divR proofEq

|||Proof that given a = r + q * b, and d divides a and b, d divides b and r
remConservesCommDiv : {a : Nat} -> {b : Nat} -> {q : Nat} -> {r : Nat} -> {d : Nat} ->
				  (isCommonDivisor a b d) -> (a = r + (q * b)) -> (isCommonDivisor b r d)
remConservesCommDiv {a} {b} {q} {r} (divA, divB) proofEq = (divB, divR) where
	divR = dividesDiffExtend divA divB proofEq

|||Proof that given a = r + q * b, and d divides a and b, d divides b and r
remExtendsMaxDiv : {a : Nat} -> {b : Nat} -> {q : Nat} -> {r : Nat} -> {d : Nat} ->
			    (isMaxDivisor b r d) -> (a = r + (q * b)) -> (isMaxDivisor a b d)
remExtendsMaxDiv maxDiv proofEq =
	(\n => (\commDiv => maxDiv n (remConservesCommDiv commDiv proofEq)))

|||Proof that given a = r + q * b, and d divides b and r, d divides a and b
remConservesMaxDiv : {a : Nat} -> {b : Nat} -> {q : Nat} -> {r : Nat} -> {d : Nat} ->
				 (isMaxDivisor a b d) -> (a = r + (q * b)) -> (isMaxDivisor b r d)
remConservesMaxDiv maxDiv proofEq =
	(\n => (\commDiv => maxDiv n (remExtendsCommDiv commDiv proofEq)))

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

--Decidability of divisibility

|||Proof that d divides n and n != 0 implies n >= d
dividesImpliesGEQ : {n : Nat} -> {d : Nat} -> (isDivisible n d) -> (Not (n = Z)) -> (LEQ d n)
dividesImpliesGEQ {n} {d} (k ** (proofEq, dNotZ)) nNotZ =
	case k of
		Z => void (nNotZ proofEq)
		(S l) =>  ((l * d) ** (sym proofEq))

|||Proof that if n = r + q * d, where r ! = 0 and r < d,  then n is not divisible by d
notDivisible : {n : Nat} -> {r : Nat} -> {q : Nat} -> {d : Nat} ->
			(Not (r = Z)) -> (LNEQ r d) -> (n = r + (q * d)) -> (Not (isDivisible n d))
notDivisible {n} {r} {q} {d} rNotZ proofLNEQ proofEq (k ** (proofDiv, dNotZ)) =
	(leqImpliesNotLNEQ dLEQr proofLNEQ) where
		dLEQr = (dividesImpliesGEQ dDividesr rNotZ) where
			dDividesr = dividesDifference (k ** ((trans (sym proofEq) proofDiv), dNotZ)) (q ** (Refl, dNotZ))

|||Decision procedure to check if n is divisible by d
decDivisible : (n : Nat) -> (d : Nat) -> Dec (isDivisible n d)
decDivisible n Z = No (\proofDivides => (snd (snd proofDivides)) Refl)
decDivisible n (S d) =
	case (euclidDivide n (S d) SIsNotZ) of
		(q ** (r ** ((proofEq, proofLNEQ)))) =>
			case r of
				Z => Yes (q ** (proofEq, SIsNotZ))
				(S k) => No (notDivisible SIsNotZ proofLNEQ proofEq)

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


text:
module Client.Action.Init

import Client.Skeleton.Skeleton
import Data.List
import Fmt
import Inigo.Async.Base
import Inigo.Async.FS
import Inigo.Async.Promise
import Inigo.Template
import System.Path

export
init :
    String -> -- template
    String -> -- package namespace
    String -> -- package name
    Promise ()
init tmplFile packageNS packageName = do
    tmplInp <- fs_readFile tmplFile
    tmpl <- liftEither $ runTemplate packageNS packageName tmplFile tmplInp
    ignore $ all $ map writeTmplFile tmpl
    log (fmt "Successfully built %s" tmplFile)
  where
    ensureParent : String -> Promise ()
    ensureParent path = case parent path of
        Just parentPath => unless (parentPath == "") $ fs_mkdir True parentPath
        Nothing => pure ()

    writeTmplFile : (String, String) -> Promise ()
    writeTmplFile (path, contents) = do
        ensureParent path
        fs_writeFile path contents

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
import Data.Vect

read_vect_len : (len : Nat) -> IO (Vect len String)
read_vect_len Z = pure []
read_vect_len (S k) = do
  x <- getLine
  xs <- read_vect_len k
  pure (x :: xs)

read_vect : IO (n ** Vect n String)
read_vect = do
  x <- getLine
  if (x == "")
    then pure (_ ** [])
    else do (_ ** xs) <- read_vect
            pure (_ ** (x :: xs))

zipInputs : IO ()
zipInputs = do
  putStrLn "1:"
  (len1 ** vec1) <- read_vect
  putStrLn "2:"
  (len2 ** vec2) <- read_vect
  case exactLength len1 vec2 of
    Nothing => putStrLn "Input lengths must be equal"
    Just vec2' => printLn (zip vec1 vec2')

max_stars_repo_name: tekerson/type-driven-development

max_issues_repo_name: tekerson/type-driven-development

max_forks_repo_name: tekerson/type-driven-development


text:
module Main

import GLCore
import JSArrays
import Shaders

-- Save time, just get the canvas directly by id
getElemById : String -> IO Element
getElemById s = do
  x <- mkForeign (FFun "document.getElementById(%0)" [FString] FPtr) s
  return (MkElem x)

-- Shader Functions
vShader : String
vShader = "attribute vec2 pos;void main() { gl_Position = vec4(pos, 0, 1); }"
fShader : String
fShader = "precision mediump float;void main() { gl_FragColor = vec4(0,0.8,0,1); }"

-- Create the 2D Vector
-- Populate the 2D Vector
-- var vertices = [-0.5, -0.5, 0.5, -0.5, 0, 0.5]
triangleVertices : List Float
triangleVertices = [-0.5, -0.5, 0.5, -0.5, 0, 0.5]

-- Some basic settings for starting our GL env
baseGLInit : GLCxt -> IO GLCxt
baseGLInit c = do
  clearColor c
  enableGLSetting c
  depthFun c
  glClear c

-- Create an array, populate it with vertices, and use it to create a proper Float32Array
prepareTriangleArray : IO F32Array
prepareTriangleArray = createJSArray >>= fromFloatList triangleVertices >>= createF32Array

-- Wrapper for finding and init'ing our GL env and context
locateInitCanvas : IO GLCxt
locateInitCanvas = getElemById "canvas" >>= getGLCxt >>= baseGLInit

-- Wrapper for the process of assigning a shader variable the correct location
-- for our program to locate vertex information when the shader runs.
assignVertexPositionAttribs : (GLProgram,GLCxt) -> IO (GLProgram,GLCxt)
assignVertexPositionAttribs glProg = getAttribLocation "pos" glProg
                                     >>= setVertexPosAttrib glProg
                                     >>= enableVertexAttribArray
                                     >>= setVertexAttribPointer 2

main : IO ()
main = do
  f32Arr <- prepareTriangleArray -- prepare our vertices
  glCxt <- locateInitCanvas -- start our engines
  buffer <- createBuffer glCxt -- create a buffer to store our vertex information
  bindArrayBuffer glCxt buffer -- bind the buffer to the current gl context
  program <- bufferVertexData f32Arr glCxt >>= createProg -- fill the buffer with vertex info
  -- Pass our shader code to be built,compiled, and linked to the GL context
  compileAndLinkShaders [(Vertex vShader),(Fragment fShader)] program glCxt
    >>= useProg -- set the gl context to use this created program
    >>= assignVertexPositionAttribs -- assign our pointer information for the shaders
    >>= \glProg => drawTriangles glProg 0 3 -- draw our vertices to the screen
  putStrLn "We're finished?"


text:
module Collections.BSTree.Set.Quantifiers

import public Collections.BSTree.Map.Quantifiers

max_stars_repo_name: polendri/idris-collections

max_issues_repo_name: polendri/idris-collections

max_forks_repo_name: polendri/idris-collections


text:
-- SPDX-FileCopyrightText: 2021 The toml-idr developers
--
-- SPDX-License-Identifier: MPL-2.0

module Language.TOML.Tokens

import Text.Bounded
import Text.Token

%default total

public export
strTrue : String
strTrue = "true"

public export
strFalse : String
strFalse = "false"

public export
data Bracket = Open | Close

export
Show Bracket where
    show Open = "open"
    show Close = "close"

public export
Eq Bracket where
    (==) Open Open = True
    (==) Close Close = True
    (==) _ _ = False

public export
data Punctuation
    = Comma
    | Dot
    | Equal
    | NewLine
    | Square Bracket
    | Curly Bracket

export
Show Punctuation where
    show Comma = ","
    show Dot = "."
    show Equal = "="
    show NewLine = "\\n"
    show (Square Open) = "["
    show (Square Close) = "]"
    show (Curly Open) = "("
    show (Curly Close) = ")"

public export
Eq Punctuation where
    (==) Comma Comma = True
    (==) Dot Dot = True
    (==) Equal Equal = True
    (==) NewLine NewLine = True
    (==) (Square x) (Square y) = x == y
    (==) (Curly x) (Curly y) = x == y
    (==) _ _ = False

||| What sort of string this is
||| Names are taken from the [toml spec](https://toml.io/en/v1.0.0#string)
public export
data StringType : Type where
    ||| Double quoted, single-line string
    ||| Supports escaping
    ||| "hello \n world"
    Basic : StringType
    ||| Single quoted, singe-line string
    ||| Does not support escaping
    ||| 'hello \n world'
    Literal : StringType
    -- TODO: the following
    ||| Double quoted, multi-line string
    ||| Supports escaping and line folding
    BasicMultiline : StringType
    ||| Single quoted, multi-line string
    ||| Does not support escaping or line folding
    LiteralMultiline : StringType

export
Show StringType where
    show Basic = "Basic"
    show Literal = "Literal"
    show BasicMultiline = "BasicMultiline"
    show LiteralMultiline = "LiteralMultiline"

export
Eq StringType where
    Basic == Basic = True
    Literal == Literal = True
    BasicMultiline == BasicMultiline = True
    LiteralMultiline == LiteralMultiline = True
    _ == _ = False

public export
data TOMLTokenKind
    = TTBoolean
    | TTInt
    | TTFloat
    | TTString StringType
    | TTPunct Punctuation
    | TTBare
    | TTIgnored

public export
TOMLToken : Type
TOMLToken = Token TOMLTokenKind

export
Show TOMLTokenKind where
    show TTBoolean = "boolean"
    show TTInt = "integer"
    show TTFloat = "float"
    show (TTString type) = "\{show type} string"
    show (TTPunct x) = show x
    show TTBare = "key"
    show TTIgnored = "comment"

public export
Eq TOMLTokenKind where
    (==) TTBoolean TTBoolean = True
    (==) TTInt TTInt = True
    (==) TTFloat TTFloat = True
    (==) (TTString x) (TTString y) = x == y
    (==) (TTPunct x) (TTPunct y) = x == y
    (==) TTBare TTBare = True
    (==) TTIgnored TTIgnored = True
    (==) _ _ = False

charToInt : Char -> Integer
charToInt c =
    if '0' <= c && c <= '9'
        then cast $ ord c - ord '0'
        else cast $ ord (toLower c) - ord 'a'

parameters (sign, base : Integer)
    private
    parseIntLoop :
        List Char ->
        (acc : Integer) ->
        Integer
    parseIntLoop [] acc = acc
    parseIntLoop ('_'::rest) acc = parseIntLoop rest acc
    parseIntLoop (c::rest) acc =
        parseIntLoop rest (acc * base + charToInt c * sign)

private
parseWithSign : List Char -> (sign : Integer) -> Integer
parseWithSign [] sign = 0
parseWithSign ('0'::'b'::rest) sign = parseIntLoop sign 2 rest 0
parseWithSign ('0'::'o'::rest) sign = parseIntLoop sign 8 rest 0
parseWithSign ('0'::'x'::rest) sign = parseIntLoop sign 16 rest 0
parseWithSign rest sign = parseIntLoop sign 10 rest 0

private
parseInt : List Char -> Integer
parseInt [] = 0
parseInt ('+'::rest) = parseWithSign rest 1
parseInt ('-'::rest) = parseWithSign rest (-1)
parseInt rest = parseWithSign rest 1

nan : Double
nan = sqrt (-1)

inf : Double
inf = 1.0 / 0.0

namespace Float
    parameters (sign : Double)
        ||| parse the exponent part of a double
        ||| not including the e
        parseExponent :
            (number : Double) ->
            (acc : Integer) ->
            List Char ->
            Double
        parseExponent number acc [] = sign * number * pow 10 (cast acc)
        parseExponent number acc ('_'::rest) = parseExponent number acc rest
        parseExponent number acc (x::rest) = parseExponent number (10 * acc + charToInt x) rest

        ||| parse the decimal part of a double
        ||| not including the .
        ||| up to and including the e
        parseDecimal :
            (whole : Integer) ->
            (acc : Double) ->
            (exponent : Double) ->
            List Char ->
            Double
        parseDecimal whole acc exponent [] = sign * (cast whole + acc)
        parseDecimal whole acc exponent ('e'::rest) = parseExponent (cast whole + acc) 0 rest
        parseDecimal whole acc exponent ('E'::rest) = parseExponent (cast whole + acc) 0 rest
        parseDecimal whole acc exponent ('_'::rest) = parseDecimal whole acc exponent rest
        parseDecimal whole acc exponent (x::rest) =
            parseDecimal
                whole
                (acc + cast (charToInt x) * exponent)
                (exponent * 0.1)
                rest

        ||| parse the part of the double before the `.`
        parseWhole : (acc : Integer) -> List Char -> Double
        parseWhole acc [] = 0.0
        parseWhole acc ('.'::rest) = parseDecimal acc 0.0 0.1 rest
        parseWhole acc ('e'::rest) = parseExponent (cast acc) 0 rest
        parseWhole acc ('E'::rest) = parseExponent (cast acc) 0 rest
        parseWhole acc ('_'::rest) = parseWhole acc rest
        parseWhole acc (x::rest) = parseWhole (10 * acc + charToInt x) rest

    parseSign : List Char -> Double
    parseSign ('+'::rest) = parseWhole 1.0 0 rest
    parseSign ('-'::rest) = parseWhole (-1.0) 0 rest
    parseSign rest = parseWhole 1.0 0 rest

    export
    parseFloat : String -> Double
    parseFloat "nan" = nan
    parseFloat "+nan" = nan
    parseFloat "-nan" = -nan
    parseFloat "inf" = inf
    parseFloat "+inf" = inf
    parseFloat "-inf" = -inf
    parseFloat x = parseSign (unpack x)

private
unescapeBasic : List Char -> Either String (List Char)
unescapeBasic ('"'::rest) = loop rest
    where
        -- hex digit to int
        hexToInt : Char -> Either String Int
        hexToInt c =
            if isHexDigit c
                then Right $
                    if '0' <= c && c <= '9'
                        then ord c - ord '0'
                        else ord (toLower c) - ord 'a'
                else Left "invalid hex character: '\{cast {to=String} c}'"

        unicodeEscape : List Char -> (acc : Int) -> Either String Char
        unicodeEscape [] acc = pure $ chr acc
        unicodeEscape (c::cs) acc = do
            x <- hexToInt c
            unicodeEscape cs (acc * 16 + x)

        loop : List Char -> Either String (List Char)
        loop [] = Left "unexpected end of input"
        loop ('"'::_) = Right []
        loop ('\\'::'b'::rest) = ('\b' ::) <$> loop rest
        loop ('\\'::'t'::rest) = ('\t' ::) <$> loop rest
        loop ('\\'::'n'::rest) = ('\n' ::) <$> loop rest
        loop ('\\'::'f'::rest) = ('\f' ::) <$> loop rest
        loop ('\\'::'r'::rest) = ('\r' ::) <$> loop rest
        loop ('\\'::'"'::rest) = ('"' ::) <$> loop rest
        loop ('\\'::'\\'::rest) = ('\\' ::) <$> loop rest
        loop ('\\'::'u'::u0::u1::u2::u3::rest) = do
            c <- unicodeEscape [u0, u1, u2, u3] 0
            (c ::) <$> loop rest
        loop ('\\'::'U'::u0::u1::u2::u3::u4::u5::u6::u7::rest) = do
            c <- unicodeEscape [u0, u1, u2, u3, u4, u5, u6, u7] 0
            (c ::) <$> loop rest
        loop ('\\'::_) = Left "invalid escape code"
        loop (x::rest) = (x ::) <$> loop rest
unescapeBasic _ = Left "expected quote"

public export
TokenKind TOMLTokenKind where
    TokType TTBoolean = Bool
    TokType TTInt = Integer
    TokType TTFloat = Double
    -- a string accepted by the lexer isn't necessarily
    -- a valid toml string
    TokType (TTString _) = Either String String
    TokType (TTPunct _) = ()
    TokType TTBare = String
    TokType TTIgnored = ()

    tokValue TTBoolean s = s == strTrue
    tokValue TTInt s = parseInt (unpack s)
    tokValue TTFloat s = parseFloat s

    tokValue (TTString Basic) s = map pack $ unescapeBasic (unpack s)
    tokValue (TTString Literal) s = Left "unimplemted string type: literal"
    tokValue (TTString BasicMultiline) s = Left "unimplemted string type: basic multiline"
    tokValue (TTString LiteralMultiline) s = Left "unimplemted string type: literal multiline"

    tokValue (TTPunct _) _ = ()
    tokValue TTBare s = s
    tokValue TTIgnored _ = ()

export
getString : Token TOMLTokenKind -> Maybe (Either String String)
getString tok@(Tok ((TTString _)) text) = Just (value tok)
getString _ = Nothing

export
getKeyString : Token TOMLTokenKind -> Maybe (Either String String)
getKeyString tok@(Tok ((TTString Basic)) text) = Just (value tok)
getKeyString tok@(Tok ((TTString Literal)) text) = Just (value tok)
getKeyString _ = Nothing

export
ignored : WithBounds TOMLToken -> Bool
ignored (MkBounded (Tok TTIgnored _) _ _) = True
ignored _ = False

max_stars_repo_name: sepiina/toml-idr

max_issues_repo_name: sepiina/toml-idr

max_forks_repo_name: sepiina/toml-idr


text:
module Core.GetType

import Core.CaseTree
import Core.TT
import Core.Context
import Core.Env
import Core.Normalise
import Core.Value

%default covering

-- Get the type of an already typechecked thing.
-- We need this (occasionally) because we don't store types in subterms (e.g. on
-- applications) and we don't keep the type of suterms up to date throughout
-- unification. Perhaps we should? There's a trade off here, and recalculating on
-- the rare occasions it's necessary doesn't seem to cost too much, but keep an
-- eye on it...

mutual
  chk : {vars : _} ->
        {auto c : Ref Ctxt Defs} ->
        Env Term vars -> Term vars -> Core (Glued vars)
  chk env (Local fc r idx p)
      = pure $ gnf env (binderType (getBinder p env))
  chk env (Ref fc nt n)
      = do defs <- get Ctxt
           Just ty <- lookupTyExact n (gamma defs)
               | Nothing => throw (UndefinedName fc n)
           pure $ gnf env (embed ty)
  chk env (Meta fc n i args)
      = do defs <- get Ctxt
           Just mty <- lookupTyExact (Resolved i) (gamma defs)
               | Nothing => throw (UndefinedName fc n)
           chkMeta fc env !(nf defs env (embed mty)) args
  chk env (Bind fc nm b sc)
      = do bt <- chkBinder env b
           sct <- chk {vars = nm :: _} (b :: env) sc
           pure $ gnf env (discharge fc nm b !(getTerm bt) !(getTerm sct))
  chk env (App fc f a)
      = do fty <- chk env f
           case !(getNF fty) of
                NBind _ _ (Pi _ _ _ ty) scdone =>
                      do defs <- get Ctxt
                         aty <- chk env a
                         sc' <- scdone defs (toClosure defaultOpts env a)
                         pure $ glueBack defs env sc'
                _ => do fty' <- getTerm fty
                        throw (NotFunctionType fc env fty')
  chk env (As fc s n p) = chk env p
  chk env (TDelayed fc r tm) = pure (gType fc)
  chk env (TDelay fc r dty tm)
      = do gtm <- chk env tm
           tm' <- getNF gtm
           defs <- get Ctxt
           pure $ glueBack defs env (NDelayed fc r tm')
  chk env (TForce fc r tm)
      = do tm' <- chk env tm
           case !(getNF tm') of
                NDelayed fc _ fty =>
                    do defs <- get Ctxt
                       pure $ glueBack defs env fty
                _ => throw (GenericMsg fc "Not a delayed type")
  chk env (PrimVal fc x) = pure $ gnf env (chkConstant fc x)
  chk env (TType fc) = pure (gType fc)
  chk env (Erased fc _) = pure (gErased fc)

  chkMeta : {vars : _} ->
            {auto c : Ref Ctxt Defs} ->
            FC -> Env Term vars -> NF vars -> List (Term vars) ->
            Core (Glued vars)
  chkMeta fc env ty []
      = do defs <- get Ctxt
           pure $ glueBack defs env ty
  chkMeta fc env (NBind _ _ (Pi _ _ _ ty) scdone) (a :: args)
      = do defs <- get Ctxt
           aty <- chk env a
           sc' <- scdone defs (toClosure defaultOpts env a)
           chkMeta fc env sc' args
  chkMeta fc env ty args
      = do defs <- get Ctxt
           throw (NotFunctionType fc env !(quote defs env ty))

  chkBinder : {vars : _} ->
              {auto c : Ref Ctxt Defs} ->
              Env Term vars -> Binder (Term vars) -> Core (Glued vars)
  chkBinder env b = chk env (binderType b)

  discharge : FC -> (nm : Name) -> Binder (Term vars) ->
              Term vars -> Term (nm :: vars) -> (Term vars)
  discharge fc n (Lam fc' c x ty) bindty scopety
      = Bind fc n (Pi fc' c x ty) scopety
  discharge fc n (Let fc' c val ty) bindty scopety
      = Bind fc n (Let fc' c val ty) scopety
  discharge fc n (Pi _ _ _ _) bindty scopety
      = bindty
  discharge fc n (PVar fc' c p ty) bindty scopety
      = Bind fc n (PVTy fc' c ty) scopety
  discharge fc n (PLet fc' c val ty) bindty scopety
      = Bind fc n (PLet fc' c val ty) scopety
  discharge fc n (PVTy _ _ _) bindty scopety
      = bindty

  chkConstant : FC -> Constant -> Term vars
  chkConstant fc (I x) = PrimVal fc IntType
  chkConstant fc (BI x) = PrimVal fc IntegerType
  chkConstant fc (B8 x) = PrimVal fc Bits8Type
  chkConstant fc (B16 x) = PrimVal fc Bits16Type
  chkConstant fc (B32 x) = PrimVal fc Bits32Type
  chkConstant fc (B64 x) = PrimVal fc Bits64Type
  chkConstant fc (Str x) = PrimVal fc StringType
  chkConstant fc (Ch x) = PrimVal fc CharType
  chkConstant fc (Db x) = PrimVal fc DoubleType
  chkConstant fc WorldVal = PrimVal fc WorldType
  chkConstant fc _ = TType fc

export
getType : {vars : _} ->
          {auto c : Ref Ctxt Defs} ->
          Env Term vars -> (term : Term vars) -> Core (Glued vars)
getType env term = chk env term


text:
module Verpackung.Command

import Verpackung.Derive.Derive
import public Verpackung.IOEither

import Data.String
import Data.String.Extra
import Language.JSON
import Language.Reflection

import System.File.ReadWrite
import System.File.Handle

%default total

%language ElabReflection

public export
record CommandOptions where
  constructor MkCommandOptions
  cwd : Maybe String
%runElab deriveJSON defaultOpts `{CommandOptions}

public export
Show CommandOptions where
  show (MkCommandOptions cwd) =
    "MkCommandOptions \{show cwd}"

public export
initOpts : CommandOptions
initOpts = MkCommandOptions Nothing

public export
record Command where
  constructor MkCommand
  command : String
  args : List String
  options : CommandOptions
%runElab deriveJSON defaultOpts `{Command}

public export
Show Command where
  show (MkCommand command args options) =
    "MkCommand \{show command} \{show args} \{show options}"

public export
prettyCommand : Command -> String
prettyCommand (MkCommand command args options) =
  join " " (command :: args)

%foreign """
node:lambda:(cmd)=> {
  var x = JSON.parse(cmd);
  return function format(proc) {
    if (proc.error) {
    return JSON.stringify(
      { error: proc.error.toString() }
    );
    } else {
      return JSON.stringify(
      { status: proc.status
      , stdout: proc.output[1].toString().substring(0, 1024)
      , stderr: proc.output[2].toString().substring(0, 1024)
      }
    );
    }
  }(require('child_process').spawnSync(x.command, x.args, x.options))
}
"""
exec__prim : String -> PrimIO String
-- TODO error if substring > 1024

public export
record CommandError where
  constructor MkCommandError
  error : String
%runElab deriveJSON defaultOpts `{CommandError}

public export
Show CommandError where
  show (MkCommandError error) =
    "MkResponse \{show error}"

public export
record Response where
  constructor MkResponse
  status : Int
  stdout : String
  stderr : String
%runElab deriveJSON defaultOpts `{Response}

public export
Show Response where
  show (MkResponse status stdout stderr) =
    "MkResponse \{show status} \{show stdout} \{show stderr}"

public export
data VerpackungError
  = JSError CommandError
  | ShellError Response
  | ParseError String
  | OtherError String

public export
Show VerpackungError where
  show (JSError x) = "JSError \{show x}"
  show (ShellError x) = "ShellError \{show x}"
  show (ParseError x) = "ParseError \{show x}"
  show (OtherError x) = "OtherError \{show x}"

parseResponse : String -> Either VerpackungError Response
parseResponse x =
  case Language.JSON.parse x of
       Nothing => Left $ ParseError x
       (Just json) => go json
where
  go : JSON -> Either VerpackungError Response
  go json =
    let err = fromJSON {a=CommandError} json
        res = fromJSON {a=Response} json
    in
    case (res, err) of
         ((Just r), Nothing) =>
            case status r of
                 0 => Right r
                 _ => Left $ ShellError r
         (Nothing, (Just e)) => Left $ JSError e
         _ => Left $ OtherError "Unknown response \{show json}"

exec_internal : Command -> IO String
exec_internal cmd =
  (primIO . exec__prim) (show $ toJSON cmd)

public export
exec : Command -> IOEither VerpackungError Response
exec cmd = MkIOEither $
  do
  putStrLn $ "$ \{prettyCommand cmd}"
  res <- exec_internal cmd
  putStrLn $ "→ \{res}"
  pure $ parseResponse res

public export
getStdout : Command -> IO (Either VerpackungError String)
getStdout cmd = do
  Right res <- liftIOEither $ exec $ cmd
  | Left e => pure $ Left e
  pure $ pure $ trim $ stdout res

max_stars_repo_name: alexhumphreys/verpackung

max_issues_repo_name: alexhumphreys/verpackung

max_forks_repo_name: alexhumphreys/verpackung


text:
module Idris.IDEMode.Commands

import Core.Core
import Core.Context
import Core.Context.Log
import Core.Name
import public Idris.REPL.Opts
import Protocol.Hex

import System.File

import public Protocol.IDE
import public Protocol.SExp

%default total

export
Cast (FileName, NonEmptyFC) FileContext where
  cast (filename, _, (startLine, startCol), (endLine, endCol)) =
    MkFileContext
      { file  = filename
      , range = MkBounds {startLine, startCol, endLine, endCol}
      }

export
getMsg : SExp -> Maybe (IDECommand, Integer)
getMsg (SExpList [cmdexp, IntegerAtom num])
   = do cmd <- fromSExp cmdexp
        pure (cmd, num)
getMsg _ = Nothing

export
SExpable Name where
  toSExp = SymbolAtom . show

sendStr : File -> String -> IO ()
sendStr f st =
  map (const ()) (fPutStr f st)

export
send : {auto c : Ref Ctxt Defs} -> File -> Reply -> Core ()
send f resp
    = do let r = show (toSExp resp) ++ "\n"
         log "ide-mode.send" 20 r
         coreLift $ sendStr f $ leftPad '0' 6 (asHex (cast (length r)))
         coreLift $ sendStr f r
         coreLift $ fflush f


text:
module Test.TestUtil

public export
printSuccess: String -> IO ()
printSuccess s = putStrLn $ "\x1b[32m" ++ s

public export
printFail: String -> IO ()
printFail s = putStrLn $ "\x1b[31m" ++ s

public export
assertEq : Eq a => (name: String) -> (given : a) -> (expected : a) -> (message: String) -> IO ()
assertEq name g e mess = if g == e
  then printSuccess $ (show name) ++ ": Test Passed"
  else printFail $ (show name) ++ ": Test Failed = " ++ mess

public export
assertNotEq : Eq a => (name: String) -> (given : a) -> (expected : a) -> (message: String) -> IO ()
assertNotEq name g e mess = if not (g == e)
  then printSuccess $ (show name) ++ ": Test Passed"
  else printFail $ (show name) ++ ": Test Failed = " ++ mess

public export
assertGT : Ord a => (name: String) -> (given : a) -> (expected : a) -> (message: String) -> IO ()
assertGT name g e message = if (g > e)
  then printSuccess $ (show name) ++ ": Test Passed"
  else printFail $ (show name) ++ ": Test Failed = " ++ message

max_stars_repo_name: gdevanla/idris-time

max_issues_repo_name: gdevanla/idris-time

max_forks_repo_name: gdevanla/idris-time


text:
module Syntax

%default total

showMaybe : {0 a : Type} -> (assumption : Show a) => Maybe a -> String
showMaybe x@ma = case map (id . id) ma of
    Nothing => "Nothing"
    Just a => "Just " ++ show a

nats : List Nat
nats =
  let n = 5
      m = 7
      xs = [id $ id 0]
      ys = [1, 2, m, n, 3] ++ xs
  in [n,id $ id m] ++ [1, 2, m, n, 3] ++ xs

record ANat where
  constructor MkANat
  aNat : Nat

doBlock : Maybe ANat
doBlock
  = do let a = 3
       let b = 5
       (c, _) <- Just (7, 9)
       let (d, e) = (c, c)
       f <- [| Nothing + Just d |]
       pure $ MkANat $ sum [a,b,c,d,e,f]

parameters (x, y, z : Nat)

  add3 : Nat
  add3 = x + y + z

parameters (x, y : Nat) (z, a : Nat)

  add4 : Nat
  add4 = x + y + z + a

anonLam : Maybe (m : Nat ** n ** m === n)
anonLam = map (\m => (m ** m ** Refl))
        $ map (uncurry $ \ m, n => m + n)
        $ map (\ (m, n) => (n, m))
        $ map (\ m => (m, m))
        $ map (\ m => S m.aNat)
        doBlock


text:
module Main

import Flutter

appTitle : String
appTitle = "Idris Demo Home Page"

appHome : IO Stateful
appHome = Stateful.new [initialState @= 0, onBuild @= build]
  where
    build : StatefulWidgetState Int -> BuildContext -> IO Widget
    build state context = upcast <$> Scaffold.new [
      appBar @=> !(AppBar.new [
        title @=> !(Text.new appTitle [])
      ]),
      body @=> !(Center.new [
        child @=> !(Column.new [
          mainAxisAlignment @= MainAxisAlignment.center,
          children @= !(widgets [
            !(Text.new "You have pushed the button this many times:" []),
            !(Text.new (show (get state)) [
              style @= headline4 (textTheme !(Theme.of_ context))
            ])
          ])
        ])
      ]),
      floatingActionButton @=> !(FloatingActionButton.new [
        tooltip @= "Increment",
        child @=> !(Icon.new Icons.add []),
        onPressed @= modify state (+ 1)
      ])
    ]

app : IO Stateless
app = Stateless.new [onBuild @= build]
  where
    build : BuildContext -> IO Widget
    build _ = upcast <$> MaterialApp.new [
      title @= appTitle,
      home @=> !appHome,
      theme @= !(ThemeData.new [
-- This is the theme of your application.
--
-- Try running your application with "flutter run". You'll see the
-- application has a blue toolbar. Then, without quitting the app, try
-- changing the primarySwatch below to Colors.green and then invoke
-- "hot reload" (press "r" in the console where you ran "flutter run",
-- or simply save your changes to "hot reload" in a Flutter IDE).
-- Notice that the counter didn't reset back to zero; the application
-- is not restarted.
        primarySwatch @= Colors.blue
      ])
    ]

main : IO ()
main = runApp !app


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

import Data.Morphisms

public export
data Curried : ( g : Type -> Type ) -> ( h : Type -> Type ) -> ( a : Type ) -> Type where
  MkCurried : (forall r. g (a -> r) -> h r) -> Curried g h a

public export
Functor g => Functor (Curried g h) where
  map f (MkCurried g) = MkCurried (g . map (. f))

public export
Functor g => Applicative (Curried g g) where
  pure a = MkCurried (map (\f => f a))
  (MkCurried mf) <*> (MkCurried ma) = MkCurried (ma . mf . map (.))

public export
liftCurried : Applicative f => f a -> Curried f f a
liftCurried fa = MkCurried (<*> fa)

public export
lowerCurried : Applicative f => Curried f g a -> g a
lowerCurried (MkCurried f) = f (pure id)


text:
module Main

test : List Nat -> List Nat
test xs = map (\x => x + 3) xs

test_main : List Nat -> List Nat
test_main xs = ?test_main_rhs

-- main : IO ()
-- main = putStrLn (show test_main)


text:
module Control.Monad.Logic.Streaming

import Control.Monad.Error.Interface
import Control.Monad.Identity
import Control.Monad.Reader.Interface
import Control.Monad.State.Interface
import Control.Monad.Trans
import Streaming
import public Control.Monad.Logic.Interface

public export
record LogicT (m : Type -> Type) (a : Type) where
  constructor MkLogicT
  observe : Stream (Of a) m ()

export
Monad m => Functor (LogicT m) where
  map f z = MkLogicT $ maps f $ observe z

export
Monad m => Applicative (LogicT m) where
  pure x = MkLogicT $ yield x
  fz <*> xz = MkLogicT $ for (observe fz) $ \f => maps f (observe xz)

export
Monad m => Monad (LogicT m) where
  act >>= react = assert_total $ MkLogicT $ for (observe act) $ \x => observe (react x)

export
Monad m => Alternative (LogicT m) where
  empty = MkLogicT $ pure ()
  xz <|> yz = MkLogicT $ observe xz >> observe yz

export
MonadTrans LogicT where
  lift x = MkLogicT (lift x >>= yield)

export
Monad m => MonadLogic (LogicT m) where
  split z = pure $ case !(lift $ next $ observe z) of
    Left () => Nothing
    Right (x, xs) => Just (x, MkLogicT xs)

export
HasIO m => HasIO (LogicT m) where
  liftIO = lift . liftIO

export
MonadError e m => MonadError e (LogicT m) where
  throwError e = lift $ throwError e
  z `catchError` f = MkLogicT $ observe z `catchError` observe . f

export
MonadState s m => MonadState s (LogicT m) where
  put = lift . put
  get = lift get
  state f = lift (state f)

export
MonadReader s m => MonadReader s (LogicT m) where
  ask = lift ask
  local f z = MkLogicT $ local f (observe z)


text:
module Circuits.Idealised.Interp

import Decidable.Equality

import Data.Nat
import Data.List.Elem
import Data.List.Quantifiers

import Toolkit.Decidable.Informative
import Toolkit.Data.Graph.EdgeBounded
import Toolkit.Data.Graph.EdgeBounded.HasExactDegree.All

import Toolkit.Data.Whole

import Circuits.Idealised.Types
import Circuits.Idealised.Terms

%default total

public export
InterpTy : Ty -> Type
InterpTy TyUnit
  = Unit

InterpTy (TyPort x)
  = Vertex String

InterpTy TyGate
  = Graph String

namespace Environments
  public export
  data Env : List (Ty, Usage) -> Type where
    Empty  : Env Nil
    Extend : InterpTy type -> Env rest -> Env ((type,usage) :: rest)

  export
  lookup : (envO  : Env old )
        -> (prf   : Elem (type,FREE) old)
        -> (which : Use old prf new)
        -> (Env new, InterpTy type)
  lookup (Extend x y) Here H = (Extend x y, x)
  lookup (Extend y z) (There later) (T x)
    = let (newEnv, res) = lookup z later x
      in (Extend y newEnv, res)

namespace Result

  public export
  data Result : (context : List (Ty, Usage))
             -> (type    : Ty)
                        -> Type
    where
      R : (counter : Nat)
       -> (env     : Env new)
       -> (graph   : Graph String)
       -> (result  : InterpTy type)
                  -> Result new type
  public export
  getResult : Result ctxt type -> InterpTy type
  getResult (R _ _ _ res) = res

  public export
  data GetGraph : (res : Result ctxt type) -> Graph String -> Type
    where
      G : (g : Graph String) -> GetGraph (R c e g r) g

  public export
  getGraph : (r : Result ctxt type) -> DPair (Graph String) (GetGraph r)
  getGraph (R counter env graph result) = MkDPair graph (G graph)

interp : (env     : Env old)
      -> (counter : Nat)
      -> (graph   : Graph String)
      -> (term    : Term old type new)
                 -> Result new type

-- [ NOTE ]
--
-- As normal
interp env counter graph (Var prf x)
  = let (newEnv, res) = lookup env prf x
    in R counter newEnv graph res

-- [ NOTE ]
--
-- As normal
interp env counter graph (Seq x y)
  = let R c1 e1 g1 x' = interp env counter graph x
    in interp e1 c1 ((merge g1 x')) y

-- [ NOTE ]
--
-- Ports are leaf nodes in the graph.
interp env counter graph (NewSignal flow dtype body)

  = let n = vertexFromFlow flow (S counter) 1

    in let env' = Extend n env

    in let g'   = insertNode n graph

    in interp env' (S counter) g' body

  where
    vertexFromFlow : Direction -> Nat -> Nat -> Vertex String
    vertexFromFlow INPUT  = driver  ("INPUT : "  <+> show dtype )
    vertexFromFlow OUTPUT = catcher ("OUTPUT : " <+> show dtype )

-- [ NOTE ]
--
-- Wires are internal connected nodes in the graph
interp env counter graph (Wire dtype body)

  = let c1 = S counter
    in let c2 = S c1

    in let chanIN  = node ("CHAN_IN : "  <+> show dtype) c1 1 1
    in let chanOUT = node ("CHAN_OUT : " <+> show dtype) c2 1 1

    in interp (Extend chanIN (Extend chanOUT env))
              c2
              (updateWith graph
                          [chanIN, chanOUT]
                          [(MkPair (ident chanIN) (ident chanOUT))])
              body

-- [ NOTE ]
--
-- Multiplexers are internal nodes connected to other nodes.
interp env counter graph (Mux o c l r)

  = let c1 = S counter

    in let mux = node "MUX" c1 3 1

    in let R c2 e1 g1 vo = interp env c1 graph  o
    in let R c3 e2 g2 vc = interp e1  c2 g1     c
    in let R c4 e3 g3 vl = interp e2  c2 g2     l
    in let R c5 e4 g4 vr = interp e3  c3 g3     r

    in let mg = fromLists [mux]
                          [ (ident vl,  ident mux)
                          , (ident vr,  ident mux)
                          , (ident vc,  ident mux)
                          , (ident mux, ident vo)
                          ]
    in R c5 e4 g4 mg

-- [ NOTE ]
--
-- Multiplexers are internal nodes connected to other nodes.
interp env counter graph (Dup a b i)
  = let c1 = S counter

    in let dup = node "DUP" c1 1 2

    in let R c2 e1 g1 va = interp env c1 graph a
    in let R c3 e2 g2 vb = interp e1  c2 g1    b
    in let R c4 e3 g3 vi = interp e2  c3 g2    i

    in let dg = fromLists [dup]
                          [ MkPair (ident vi)   (ident dup)
                          , MkPair (ident dup) (ident va)
                          , MkPair (ident dup) (ident vb)
                          ]

    in R c4 e3 g3 dg

-- [ NOTE ]
--
-- internal nodes connected to other nodes.
interp env counter graph (Not output input)
  = let c1 = S counter

    in let vnot = node "NOT" c1 1 1

    in let R c2 e1 g1 vo = interp env counter graph output
    in let R c3 e2 g2 vi = interp e1  c2      g1    input

    in let ng = fromLists [vnot]
                          [ MkPair (ident vnot) (ident vo)
                          , MkPair (ident vi)   (ident vnot)
                          ]
    in R c3 e2 g2 ng

-- [ NOTE ]
--
-- internal nodes connected to other nodes.
interp env counter graph (Gate k output inputA inputB)
   = let c1 = S counter

    in let bgate = node (show k) c1 2 1

    in let R c2 e1 g1 vo = interp env c1 graph output
    in let R c3 e2 g2 vl = interp e1  c2 g1    inputA
    in let R c4 e3 g3 vr = interp e2  c3 g2    inputB

    in let bg = fromLists [bgate]
                          [ MkPair (ident bgate) (ident vo)
                          , MkPair (ident vl) (ident bgate)
                          , MkPair (ident vr) (ident bgate)
                          ]

    in R c4 e3 g3 bg

-- [ NOTE ]
--
-- internal nodes connected to other nodes.
interp env counter graph (IndexSingleton o i)
  = let c1 = S counter

    in let vnot = node "IDX_SINGLETON" c1 1 1

    in let R c2 e1 g1 vo = interp env c1  graph o
    in let R c3 e2 g2 vi = interp e1  c2  g1    i

    in let ng = fromLists [vnot]
                          [ MkPair (ident vnot) (ident vo)
                          , MkPair (ident vi)   (ident vnot)
                          ]
    in R c3 e2 g2 ng

-- [ NOTE ]
--
-- internal nodes connected to other nodes.
interp env counter graph (IndexEdge p idx oused ofree i)

  = let c1 = S counter

    in let dup = node "IDX_EDGE" c1 1 2

    in let R c2 e1 g1 va = interp env c1 graph oused
    in let R c3 e2 g2 vb = interp e1  c2 g1    ofree
    in let R c4 e3 g3 vi = interp e2  c3 g2    i

    in let dg = fromLists [dup]
                          [ MkPair (ident vi)  (ident dup)
                          , MkPair (ident dup) (ident va)
                          , MkPair (ident dup) (ident vb)
                          ]

    in R c4 e3 g3 dg

-- [ NOTE ]
--
-- internal nodes connected to other nodes.
interp env counter graph (IndexSplit p idx used freeA freeB i)

  = let c1 = S counter

    in let dup = node "IDX_SPLIT" c1 1 3

    in let R c2 e1 g1 vu = interp env c1 graph used
    in let R c3 e2 g2 va = interp e1  c2 g1    freeA
    in let R c4 e3 g3 vb = interp e2  c3 g2    freeB
    in let R c5 e4 g4 vi = interp e3  c4 g3    i

    in let dg = fromLists [dup]
                          [ MkPair (ident vi)  (ident dup)
                          , MkPair (ident dup) (ident vu)
                          , MkPair (ident dup) (ident va)
                          , MkPair (ident dup) (ident vb)
                          ]

    in R c5 e4 g4 dg

-- [ NOTE ]
--
-- internal nodes connected to other nodes.
interp env counter graph (Merge2L2V output inputA inputB)

  = let c1 = S counter

    in let bgate = node "MERGE_2L2V" c1 2 1

    in let R c2 e1 g1 vo = interp env c1 graph output
    in let R c3 e2 g2 vl = interp e1  c2 g1    inputA
    in let R c4 e3 g3 vr = interp e2  c3 g2    inputB

    in let bg = fromLists [bgate]
                          [ MkPair (ident bgate) (ident vo)
                          , MkPair (ident vl) (ident bgate)
                          , MkPair (ident vr) (ident bgate)
                          ]

    in R c4 e3 g3 bg

-- [ NOTE ]
--
-- internal nodes connected to other nodes.
interp env counter graph (Merge2V2V prf output inputA inputB)

  = let c1 = S counter

    in let bgate = node "MERGE_2V2V" c1 2 1

    in let R c2 e1 g1 vo = interp env c1 graph output
    in let R c3 e2 g2 vl = interp e1  c2 g1    inputA
    in let R c4 e3 g3 vr = interp e2  c3 g2    inputB

    in let bg = fromLists [bgate]
                          [ MkPair (ident bgate) (ident vo)
                          , MkPair (ident vl) (ident bgate)
                          , MkPair (ident vr) (ident bgate)
                          ]

    in R c4 e3 g3 bg

-- [ NOTE ]
--
-- internal nodes connected to other nodes.
interp env counter graph (MergeSingleton output input)
  = let c1 = S counter

    in let vnot = node "MERGE_SINGLETON" c1 1 1

    in let R c2 e1 g1 vo = interp env counter graph output
    in let R c3 e2 g2 vi = interp e1  c2      g1    input

    in let ng = fromLists [vnot]
                          [ MkPair (ident vnot) (ident vo)
                          , MkPair (ident vi)   (ident vnot)
                          ]
    in R c3 e2 g2 ng

interp env counter graph (Stop x)
  = R counter Empty graph MkUnit

public export
data ValidGraph : Graph type -> Type where
  IsValid : HasExactDegrees vs es
         -> ValidGraph (MkGraph vs es)

export
validGraph : {type : Type}
          -> (g    : Graph type)
                  -> DecInfo (HasExactDegree.Error type)
                             (ValidGraph g)
validGraph (MkGraph nodes edges) with (hasExactDegrees nodes edges)
  validGraph (MkGraph nodes edges) | (Yes prf)
    = Yes (IsValid prf)
  validGraph (MkGraph nodes edges) | (No msg contra)
    = No msg (\(IsValid prf) => contra prf)

public export
data Valid : (res  : Result ctxt TyUnit)
                  -> Type
  where
    D : {res : Result ctxt TyUnit}
     -> (g   : Graph String)
            -> GetGraph res g
            -> ValidGraph g
            -> Valid res

isValid : (r : Result ctxt TyUnit)
            -> DecInfo (Graph String, HasExactDegree.Error String)
                       (Valid r)
isValid r with (getGraph r)
  isValid (R c e g r) | (MkDPair g (G g)) with (validGraph g)
    isValid (R c e g r) | (MkDPair g (G g)) | (Yes prf)
      = Yes (D g (G g) prf)
    isValid (R c e g r) | (MkDPair g (G g)) | (No msg contra)
      = No (g,msg) (\(D graph (G graph) prf) => contra prf)

public export
data Run : (term : Term Nil TyUnit Nil) -> Type where
  R : (prf  : Valid (interp Empty Z (MkGraph Nil Nil) term))
           -> Run term

public export
getGraph : Run term -> DPair (Graph String) ValidGraph
getGraph (R (D g x y)) = MkDPair g y

export
run : (term : Term Nil TyUnit Nil)
           -> DecInfo (Graph String, HasExactDegree.Error String) (Run term)
run term with (isValid (interp Empty Z empty term))
  run term | (Yes prf) = Yes (R prf)
  run term | (No msg contra) = No msg (\(R prf) => contra prf)

export
runIO : (term : Term Nil TyUnit Nil)
             -> IO (Either (Graph String, HasExactDegree.Error String)
                           (Run term))
runIO term = pure $ (asEither (run term))

-- [ EOF ]

max_stars_repo_name: gallais/linear-circuits

max_issues_repo_name: gallais/linear-circuits

max_forks_repo_name: gallais/linear-circuits