text:
---
title: Logic
subtitle: An Idris port of Coq.Init.Logic
title-meta: "Logic: An Idris port of Coq.Init.Logic"
author:
- |
  \affaddr{Eric Bailey}\
  \affaddr{https://github.com/yurrriq}\
  \email{eric@ericb.me}
author-meta: Eric Bailey
abstract: Here I present an Idris port of the [`Coq.Init.Logic`](https://coq.inria.fr/library/Coq.Init.Logic.html) module from the Coq standard library.
keywords:
- logic
- coq
- idris
pandoc-minted:
  language: idris
---

> ||| An Idris port of Coq.Init.Logic
> module Logic
>
> import Data.Bifunctor
>
> %access export

= Propositional connectives

== Unit

`()` is the always true proposition ($\top$).

```idris
%elim data Unit = MkUnit
```

== Void

`Void` is the always false proposition ($\bot$).

```idris
%elim data Void : Type where
```

== Negation

`Not a`, written `~a`, is the negation of `a`.

> syntax "~" [x] = (Not x)

```idris
Not : Type -> Type
Not a = a -> Void
```

== Conjunction

`And a b`, written `(a, b)`, is the conjunction of `a` and `b`.

`Conj p q` is a proof of `(a, b)` as soon as `p` is a proof of `a` and `q` a proof of `b`.

`proj1` and `proj2` are first and second projections of a conjunction.

> syntax "(" [a] "," [b] ")" = (And a b)
>
> ||| The conjunction of `a` and `b`.
> data And : Type -> Type -> Type where
>      Conj : a -> b -> (a, b)
>
> implementation Bifunctor And where
>     bimap f g (Conj a b) = Conj (f a) (g b)
>
> ||| First projection of a conjunction.
> proj1 : (a, b) -> a
> proj1 (Conj a _) = a
>
> ||| Second projection of a conjunction.
> proj2 : (a, b) -> b
> proj2 (Conj _ b) = b

== Disjunction

`Either a b` is the disjunction of `a` and `b`.

```idris
data Either : Type -> Type -> Type where
     Left   : a -> Either a b
     Right  : b -> Either a b
```

== Biconditional

[Proof Wiki](https://proofwiki.org/wiki/Definition:Biconditional)

 <!-- $\varphi \vdash \psi$\ -->
 <!-- $\underline{\psi \vdash \varphi}$\ -->
 <!-- $\varphi \iff \psi$ -->

`iff a b`, written `a <-> b`, expresses the equivalence of `a` and `b`.

> infixl 9 <->
>
> ||| The biconditional is a *binary connective* that can be voiced:
> ||| *p* **if and only if** *q*.
> public export
> (<->) : Type -> Type -> Type
> (<->) a b = (a -> b, b -> a)

=== Biconditional is Reflexive

[Proof Wiki](https://proofwiki.org/wiki/Biconditional_is_Reflexive)

$\vdash \varphi \iff \varphi$

> ||| The biconditional operator is reflexive.
> iffRefl : a <-> a
> iffRefl = Conj id id

=== Biconditional is Transitive

[Proof Wiki](https://proofwiki.org/wiki/Biconditional_is_Transitive)

 <!-- \[ -->
 <!--   \begin{prooftree} -->
 <!--     \Hypo{ \varphi \iff \psi } -->
 <!--     \Hypo{ \psi \iff \chi } -->
 <!--     \Infer2 { \vdash \varphi \iff \chi } -->
 <!--   \end{prooftree} -->
 <!-- \] -->

> ||| The biconditional operator is transitive.
> iffTrans : (a <-> b) -> (b <-> c) -> (a <-> c)
> iffTrans (Conj ab ba) (Conj bc cb) =
>     Conj (bc . ab) (ba . cb)

=== Biconditional is Commutative

[Proof Wiki](https://proofwiki.org/wiki/Biconditional_is_Commutative)

$\varphi \iff \psi \dashv\vdash \psi \iff \varphi$

or

$\vdash (\varphi \iff \psi) \iff (\psi \iff \varphi)$

> ||| The biconditional operator is commutative.
> iffSym : (a <-> b) -> (b <-> a)
> iffSym (Conj ab ba) = Conj ba ab

=== andIffCompatLeft

$\psi \iff \chi \dashv\vdash (\varphi \land \psi) \iff (\varphi \land \chi)$

> andIffCompatLeft : (b <-> c) -> ((a, b) <-> (a, c))
> andIffCompatLeft = bimap second second

=== andIffCompatRight

$\psi \iff \chi \dashv\vdash (\psi \land \varphi) \iff (\chi \land \varphi)$

> andIffCompatRight : (b <-> c) -> ((b, a) <-> (c, a))
> andIffCompatRight = bimap first first

=== orIffCompatLeft

$\psi \iff \chi \vdash (\varphi \lor \psi) \iff (\varphi \lor \chi)$

> orIffCompatLeft : (b <-> c) ->
>                   (Either a b <-> Either a c)
> orIffCompatLeft = bimap second second

=== orIffCompatRight

$\psi \iff \chi \vdash (\psi \lor \varphi) \iff (\chi \lor \varphi)$

> orIffCompatRight : (b <-> c) ->
>                    (Either b a <-> Either c a)
> orIffCompatRight = bimap first first

=== negVoid

$\neg \varphi \dashv\vdash \varphi \iff \bot$

or

$\vdash \neg \varphi \iff (\varphi \iff \bot)$

> negVoid : (~a) <-> (a <-> Void)
> negVoid = Conj (flip Conj void) proj1

=== andCancelLeft

 <!-- $\psi \implies \varphi$\ -->
 <!-- $\underline{\chi \implies \varphi}$\ -->
 <!-- $((\varphi \land \psi) \iff (\varphi \land \chi)) \iff (\psi \iff \chi)$ -->

> andCancelLeft : (b -> a) ->
>                 (c -> a) ->
>                 (((a, b) <-> (a, c)) <-> (b <-> c))
> andCancelLeft ba ca = Conj (bimap f g) andIffCompatLeft
>   where
>     f h b = proj2 . h $ Conj (ba b) b
>     g h c = proj2 . h $ Conj (ca c) c

=== andCancelRight

> andCancelRight : (b -> a) ->
>                  (c -> a) ->
>                  (((b, a) <-> (c, a)) <-> (b <-> c))
> andCancelRight ba ca = Conj (bimap f g) andIffCompatRight
>   where
>     f h b = proj1 . h $ Conj b (ba b)
>     g h c = proj1 . h $ Conj c (ca c)

=== Conjunction is Commutative

[Proof Wiki](https://proofwiki.org/wiki/Rule_of_Commutation/Conjunction)

==== Formulation 1
$\varphi \land \psi \dashv\vdash \psi \land \varphi$

==== Formulation 2
$\vdash (\varphi \land \psi) \iff (\psi \land \varphi)$

==== Source

> ||| Conjunction is commutative.
> andComm : (a, b) <-> (b, a)
> andComm = Conj swap swap
>   where
>     swap : (p, q) -> (q, p)
>     swap (Conj p q) = Conj q p

=== Conjunction is Associative

[Proof Wiki](https://proofwiki.org/wiki/Rule_of_Association/Conjunction)

==== Formulation 1
$(\varphi \land \psi) \land \chi \dashv\vdash \varphi \land (\psi \land \chi)$

==== Formulation 2
$\vdash ((\varphi \land \psi) \land \chi) \iff (\varphi \land (\psi \land \chi))$

==== Source

> ||| Conjunction is associative.
> andAssoc : ((a, b), c) <-> (a, (b, c))
> andAssoc = Conj f g
>   where
>     f abc@(Conj (Conj a b) c) = Conj a (first proj2 abc)
>     g abc@(Conj a (Conj b c)) = Conj (second proj1 abc) c

=== orCancelLeft

$(\psi \implies \neg \varphi) \implies (\chi \implies \neg \varphi) \implies (((\varphi \lor \psi) \iff (\varphi \lor \chi)) \iff (\psi \iff \chi))$

> orCancelLeft : (b -> ~a) ->
>                (c -> ~a) ->
>                ((Either a b <-> Either a c) <-> (b <-> c))
> orCancelLeft bNotA cNotA = Conj (bimap f g) orIffCompatLeft
>   where
>     f ef b = go (bNotA b) (ef (Right b))
>     g eg c = go (cNotA c) (eg (Right c))
>     go : (~a) -> Either a b -> b
>     go lf = either (void . lf) id

=== orCancelRight

 <!-- $\psi \vdash \neg \varphi$\ -->
 <!-- $\underline{\chi \vdash \neg \varphi}$\ -->
 <!-- $((\psi \lor \varphi) \iff (\chi \lor \varphi)) \iff (\psi \iff \chi)$ -->

> orCancelRight : (b -> ~a) ->
>                 (c -> ~a) ->
>                 ((Either b a <-> Either c a) <-> (b <-> c))
> orCancelRight bNotA cNotA = Conj (bimap f g) orIffCompatRight
>   where
>     f ef b = go (bNotA b) (ef (Left b))
>     g eg c = go (cNotA c) (eg (Left c))
>     go : (~p) -> Either q p -> q
>     go rf = either id (void . rf)

=== Disjunction is Commutative

[Proof Wiki](https://proofwiki.org/wiki/Rule_of_Commutation/Disjunction)

$(\varphi \lor \psi) \iff (\psi \lor \varphi)$

> ||| Disjunction is commutative.
> orComm : Either a b <-> Either b a
> orComm = Conj mirror mirror

=== Disjunction is Associative

[Proof Wiki](https://proofwiki.org/wiki/Rule_of_Association/Disjunction)

$(\varphi \lor \psi) \lor \chi \vdash \varphi \lor (\psi \lor \chi)$

> ||| Disjunction is associative on the left.
> orAssocLeft : Either (Either a b) c -> Either a (Either b c)
> orAssocLeft = either (second Left) (pure . pure)

$\varphi \lor (\psi \lor \chi) \vdash (\varphi \lor \psi) \lor \chi$

> ||| Disjunction is associative on the right.
> orAssocRight : Either a (Either b c) -> Either (Either a b) c
> orAssocRight = either (Left . Left) (first Right)

==== Formulation 1
$(\varphi \lor \psi) \lor \chi \dashv\vdash \varphi \lor (\psi \lor \chi)$

==== Formulation 2
$\vdash ((\varphi \lor \psi) \lor \chi) \iff (\varphi \lor (\psi \lor \chi))$

==== Source

> ||| Disjunction is associative.
> orAssoc : Either (Either a b) c <-> Either a (Either b c)
> orAssoc = Conj orAssocLeft orAssocRight

=== iffAnd

$\varphi \iff \psi \vdash (\varphi \implies \psi) \land (\psi \implies \varphi)$

> iffAnd : (a <-> b) -> (a -> b, b -> a)
> iffAnd = id

=== iffAndTo

$\varphi \iff \psi \dashv\vdash (\varphi \implies \psi) \land (\psi \implies \varphi)$

or

$\vdash (\varphi \iff \psi) \iff ((\varphi \implies \psi) \land (\psi \implies \varphi))$

> iffToAnd : (a <-> b) <-> (a -> b, b -> a)
> iffToAnd = Conj id id

max_stars_repo_name: yurrriq/idris-logic

max_issues_repo_name: yurrriq/idris-logic

max_forks_repo_name: yurrriq/idris-logic


text:
import Data.Vect

data Format = Number Format
            | Str Format
            | Dble Format
            | Chr Format
            | Lit String Format
            | End

PrintfType : Format -> Type
PrintfType (Number fmt) = (i : Int) -> PrintfType fmt
PrintfType (Dble fmt) = (i : Double) -> PrintfType fmt
PrintfType (Str fmt) = (str: String) -> PrintfType fmt
PrintfType (Chr fmt) = (char : Char) -> PrintfType fmt
PrintfType (Lit str fmt) = PrintfType fmt
PrintfType End = String

printfFmt : (fmt : Format) -> (acc: String) -> PrintfType fmt
printfFmt (Number fmt) acc = \i => printfFmt fmt (acc ++ show i)
printfFmt (Dble fmt) acc = \i => printfFmt fmt (acc ++ show i)
printfFmt (Str fmt) acc = \str =>  printfFmt fmt (acc ++ str)
printfFmt (Chr fmt) acc = \char => printfFmt fmt (acc ++ show char)
printfFmt (Lit lit fmt) acc = printfFmt fmt (acc ++ lit)
printfFmt End acc = acc

toFormat : (xs : List Char) -> Format
toFormat [] = End
toFormat ('%' :: 'd' :: chars) = Number (toFormat chars)
toFormat ('%' :: 'f' :: chars) = Dble (toFormat chars)
toFormat ('%' :: 's' :: chars) = Str (toFormat chars)
toFormat ('%' :: 'c' :: chars) = Chr (toFormat chars)
toFormat ('%' :: chars) = Lit "%" (toFormat chars)
toFormat (c :: chars) = case toFormat chars of
                             Lit lit chars' => Lit (strCons c lit) chars'
                             fmt => Lit (strCons c "") fmt

printf : (fmt : String) -> PrintfType (toFormat (unpack fmt))
printf fmt = printfFmt _ ""

Matrix : Nat -> Nat -> Type
Matrix n m = Vect n (Vect m Double)

ext: idr


text:
import TypedContainers.LawfulOrd

%default total

LawfulOrd Nat where
  compare Z Z = EQ
  compare Z (S _) = LT
  compare (S _) Z = GT
  compare (S x) (S y) = TypedContainers.LawfulOrd.compare x y

  reflexivity Z = Refl
  reflexivity (S x) = reflexivity x

  reversion1 Z Z p impossible
  reversion1 (S _) Z p impossible
  reversion1 Z (S _) p = Refl
  reversion1 (S x) (S y) p =
    let rec = reversion1 x y in
    rec p

  reversion2 Z Z p impossible
  reversion2 (S _) Z p = Refl
  reversion2 Z (S _) p impossible
  reversion2 (S x) (S y) p =
    let rec = reversion2 x y in
    rec p

  reversion3 Z Z p = Refl
  reversion3 (S _) Z p impossible
  reversion3 Z (S _) p impossible
  reversion3 (S x) (S y) p =
    let rec = reversion3 x y in
    rec p

  transitivity Z     Z     Z     p0 p1 impossible
  transitivity Z     Z     (S z) p0 p1 impossible
  transitivity Z     (S y) Z     p0 p1 impossible
  transitivity Z     (S y) (S z) p0 p1 = Refl
  transitivity (S x) Z     Z     p0 p1 impossible
  transitivity (S x) Z     (S z) p0 p1 impossible
  transitivity (S x) (S y) Z     p0 p1 impossible
  transitivity (S x) (S y) (S z) p0 p1 =
    let rec = transitivity x y z p0 p1 in
    rec

  equality1 Z     Z     z     p = Refl
  equality1 Z     (S y) Z     p impossible
  equality1 Z     (S y) (S z) p impossible
  equality1 (S x) Z     Z     p impossible
  equality1 (S x) Z     (S z) p impossible
  equality1 (S x) (S y) Z     p = Refl
  equality1 (S x) (S y) (S z) p =
    let rec = equality1 x y z p in
    rec

  equality2 Z     Z     z     p = Refl
  equality2 Z     (S y) Z     p impossible
  equality2 Z     (S y) (S z) p impossible
  equality2 (S x) Z     Z     p impossible
  equality2 (S x) Z     (S z) p impossible
  equality2 (S x) (S y) Z     p = Refl
  equality2 (S x) (S y) (S z) p =
    let rec = equality2 x y z p in
    rec

LawfullerOrd Nat where
  realEquality Z Z p = Refl
  realEquality Z (S _) p impossible
  realEquality (S _) Z p impossible
  realEquality (S x) (S y) p =
    let rec = realEquality x y p in
    cong S rec

max_stars_repo_name: L-as/idris-rbtree

max_issues_repo_name: L-as/idris-rbtree

max_forks_repo_name: L-as/idris-rbtree


text:
module TwoVarDiophEq
import ZZ
import ZZUtils
import Divisors
import GCDZZ
import decDivZ
%access public export
%default total

|||Any integer is a solution for c=xa+yb when a=b=c=0
zeroLinCombZeroZero:a=0->b=0->c=0->(x:ZZ)->(y:ZZ)->c=x*a+y*b
zeroLinCombZeroZero az bz cz x y = rewrite az in
                                       rewrite bz in
                                       rewrite cz in
                                       rewrite multZeroRightZeroZ x in
                                       rewrite multZeroRightZeroZ y in
                                       Refl

|||If a=b=0 and c is not zero, it is impossible that c = xa +yb
notZeroNotLinCombZeroZero:a=0->b=0->NotZero c ->
   (x:ZZ)->(y:ZZ)->c=x*a+y*b->Void
notZeroNotLinCombZeroZero aZ bZ cnotz x y =
  rewrite aZ in
  rewrite bZ in
  rewrite multZeroRightZeroZ x in
  rewrite multZeroRightZeroZ y in
  (notZeroNonZero cnotz)

|||Proves that if d = gcd (a,b) and c= xa +yb , then d|c
gcdDivLinComb:GCDZ a b d->c=x*a+y*b -> IsDivisibleZ c d
gcdDivLinComb (dPos,dcommonfactab,fd)  prf =
  linCombDivLeftWithProof prf dcommonfactab

gcdDivLinCombContra:GCDZ a b d ->((IsDivisibleZ c d) ->Void)->(x:ZZ)->(y:ZZ)->c=x*a+y*b->Void
gcdDivLinCombContra gcdpf f x y prf =
  f (gcdDivLinComb gcdpf prf)

|||Proves that if d = gcd (a,b) and d|c, then there exists integers x and y
|||such that c = xa +yb
multipleOfGcdLinComb:GCDZ a b d -> IsDivisibleZ c d ->
    (x:ZZ**y:ZZ** (c = x*a + y*b))
multipleOfGcdLinComb{a} {d}{b} gcdpf (n**eqpf) =
  (case checkNotBothZero a b of
        (Left (aZ, bZ)) => void (gcdZeroZeroContra (gcdzReplace aZ bZ gcdpf))
        (Right r) =>
          (case gcdIsLinComb gcdpf of
                (j**l**gcdlc) => ((n*j)**(n*l)**
                    (rewrite sym $multAssociativeZ n j a in
                     rewrite sym $multAssociativeZ n l b in
                     rewrite sym $ multDistributesOverPlusRightZ n (j*a) (l*b) in
                     rewrite eqpf in
                     rewrite multCommutativeZ d n in
                     cong gcdlc) )))

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

|||Proves that (b/gcd(a,b))*a = (a/gcd(a,b))*b
divByGcdMultByOtherIsSame:(gcdpf:GCDZ a b d) ->(bByd gcdpf)*a =(aByd gcdpf)*b
divByGcdMultByOtherIsSame {a}{b}{d} (dPos, ((abyd**apf),(bbyd**bpf)),fd) =
  multLeftCancelZ d (bbyd*a) (abyd *b) (posThenNotZero dPos)
    (rewrite multAssociativeZ d bbyd a in
     rewrite multAssociativeZ d abyd b in
     rewrite  sym $ bpf in
     rewrite sym $ apf in
     rewrite multCommutativeZ b a in
     Refl)

|||Proves that for any integer k, k*(-b/(gcd(a,b))) and  k*(a/(gcd(a,b)))
|||are solutions of 0 = xa + yb
homoSolution:(gcdpf:GCDZ a b d)->{k:ZZ}->
   (0 = (k*(-(bByd gcdpf)))*a + (k*((aByd gcdpf)))*b)
homoSolution {a}{b}{d}{k} (dPos, ((abyd**apf),(bbyd**bpf)),fd)  =
  rewrite sym $ multAssociativeZ k (-bbyd) a in
  rewrite sym $ multAssociativeZ k (abyd) b in
  rewrite sym $ multDistributesOverPlusRightZ k ((-bbyd)*a) ((abyd)*b) in
  rewrite multNegateLeftZ bbyd a in
  rewrite divByGcdMultByOtherIsSame (dPos, ((abyd**apf),(bbyd**bpf)),fd) in
  rewrite plusNegateInverseRZ (abyd*b) in
  rewrite multZeroRightZeroZ k in
  Refl

|||Proves that if 0 = xa +yb, then (-b/gcd(a,b)))*y = (a/(gcd(a,b)))*x
divHomoEqByGcd:(gcdpf:GCDZ a b d)->(0 = x*a + y*b)->((-(bByd gcdpf))*y = (aByd gcdpf)*x)
divHomoEqByGcd {x}{y}{a}{b}{d}(dPos, ((abyd**apf),(bbyd**bpf)),fd) prf =
  rewrite sym $plusZeroLeftNeutralZ ((-bbyd)*y) in
  rewrite multNegateLeftZ bbyd y in
  subOnBothSides 0 (abyd*x) ((bbyd)*y)
    (multLeftCancelZ d 0 ((abyd*x)+(bbyd*y)) (posThenNotZero dPos)
     (rewrite multZeroRightZeroZ d in
      rewrite multDistributesOverPlusRightZ d (abyd*x) (bbyd*y) in
      rewrite multAssociativeZ d abyd x in
      rewrite multAssociativeZ d bbyd y in
      rewrite sym $ apf in
      rewrite sym $ bpf in
      rewrite multCommutativeZ a x in
      rewrite multCommutativeZ b y in
      prf))

|||Proves that if  0 = xa + yb then there exists an integer k such that
||| y = k* (a/(gcd(a,b)))
homoOnlySolnForY:(gcdpf:GCDZ a b d)->(0 = x*a + y*b) ->
   (k:ZZ**(y = k * (aByd gcdpf)))
homoOnlySolnForY{a}{b}{d}{x}{y} (dPos, ((abyd**apf),(bbyd**bpf)),fd) prf  =
  (case divHomoEqByGcd (dPos, ((abyd**apf),(bbyd**bpf)),fd) prf  of
    eqpf  =>
     (case caCoprimeThencDivb (x**eqpf) (negatingPreservesGcdLeft1
         (gcdSymZ (divideByGcdThenGcdOne (dPos, ((abyd**apf),(bbyd**bpf)),fd)))) of
           (quot**divpf) => (quot** (rewrite multCommutativeZ quot abyd in divpf))))

|||Proves that if a is not zero then a/(gcd(a,b)) is not zero
divByGcdNotZero:(gcdpf:(GCDZ a b d))->NotZero a ->NotZero (aByd gcdpf)
divByGcdNotZero {a = (Pos (S k))}{b = b}{d = d} (dPos, ((abyd**apf),(bbyd**bpf)),fd)
    PositiveZ = posThenNotZero (posDivByPosIsPos{c=(Pos (S k))} Positive dPos apf)
divByGcdNotZero {a = (NegS k)}{b = b}{d = d} (dPos, ((abyd**apf),(bbyd**bpf)),fd)
NegativeZ = NegSThenNotZero (negDivByPosIsNeg Negative dPos apf)

-- The arguments to the function homoOnlySoln need to be explicit because Idris will not
-- infer the correct arguments in the functions below.

|||Proves that if a is not zero and 0 =xa + yb, then there exists an integer k such that
||| x = k* (-b/(gcd(a,b))) and y = k* (a/(gcd(a,b)))
homoOnlySoln:(x: ZZ) -> (y: ZZ) -> (gcdpf:GCDZ a b d)->(0 = x*a + y*b) ->NotZero a->
   (k:ZZ**((x = k * (-(bByd gcdpf))),(y = k * (aByd gcdpf))))
homoOnlySoln {a}{b}{d} x y (dPos, ((abyd**apf),(bbyd**bpf)),fd) prf anotz =
   (case divHomoEqByGcd (dPos, ((abyd**apf),(bbyd**bpf)),fd) prf of
        divgpf =>
          (case homoOnlySolnForY (dPos, ((abyd**apf),(bbyd**bpf)),fd) prf of
            (k**adivy) => (k**((multLeftCancelZ abyd x (k*(-bbyd))
              (divByGcdNotZero (dPos, ((abyd**apf),(bbyd**bpf)),fd) anotz)
                (rewrite multAssociativeZ abyd k (-bbyd) in
                 rewrite multCommutativeZ abyd k in
                 rewrite sym $ adivy in
                 rewrite multCommutativeZ y (-bbyd) in
                 sym $ divgpf)),adivy))))

gcdSymZwithproof:(gcdpf:GCDZ a b d)->(gcdpf2:(GCDZ b a d)**((aByd gcdpf)=(bByd gcdpf2),(bByd gcdpf)=(aByd gcdpf2)))
gcdSymZwithproof (dPos, ((abyd**apf),(bbyd**bpf)),fd) =
  ((dPos, ((bbyd**bpf),(abyd**apf)),(genFunctionForGcdSym fd))**(Refl,Refl))

|||Same as homoOnlySolution, NotZero a is replaced with NotBothZeroZ a b
homoOnlySolnGen:(x: ZZ) -> (y: ZZ) -> (gcdpf:GCDZ a b d)->(0 = x*a + y*b) ->NotBothZeroZ a b->
   (k:ZZ**((x = k * (-(bByd gcdpf))),(y = k * (aByd gcdpf))))
homoOnlySolnGen {a = (Pos (S k))}{b = b}{d = d} x y gcdpf prf LeftPositive =
  homoOnlySoln x y gcdpf prf PositiveZ
homoOnlySolnGen {a = (NegS k)}{b = b}{d = d} x y gcdpf prf LeftNegative =
  homoOnlySoln x y gcdpf prf NegativeZ
homoOnlySolnGen {a = a}{b = (Pos (S k))}{d = d} x y (dPos, ((abyd**apf),(bbyd**bpf)),fd) prf RightPositive =
  (case gcdSymZwithproof ((dPos, ((abyd**apf),(bbyd**bpf)),fd)) of
    (gcdpf2**(eqpf1,eqpf2)) =>
      (case homoOnlySoln {a=(Pos (S k))}{b=a} {d=d} y x gcdpf2 (rewrite plusCommutativeZ (y*(Pos (S k))) (x*a) in prf )  PositiveZ of
            (j**(ypf,xpf)) => ((-j)**((rewrite multNegNegNeutralZ j bbyd in
                                       rewrite eqpf2 in
                                       xpf ),(rewrite multNegateLeftZ j abyd in
                                              rewrite sym $ multNegateRightZ j abyd in
                                              rewrite eqpf1 in
                                              ypf)))))
homoOnlySolnGen {a = a}{b = (NegS k)}{d = d} x y (dPos, ((abyd**apf),(bbyd**bpf)),fd) prf RightNegative =
    (case gcdSymZwithproof ((dPos, ((abyd**apf),(bbyd**bpf)),fd)) of
      (gcdpf2**(eqpf1,eqpf2)) =>
        (case homoOnlySoln {a=(NegS k)}{b=a} {d=d} y x gcdpf2 (rewrite plusCommutativeZ (y*(NegS k)) (x*a) in prf )  NegativeZ of
              (j**(ypf,xpf)) => ((-j)**((rewrite multNegNegNeutralZ j bbyd in
                                         rewrite eqpf2 in
                                         xpf ),(rewrite multNegateLeftZ j abyd in
                                                rewrite sym $ multNegateRightZ j abyd in
                                                rewrite eqpf1 in
                                                ypf)))))

-- The goal of the following section is to show that the non-homogeneous equation is uniquely solved by the family of
-- solutions ((x_p+k*x_0), (y_p+k*y_0)).

||| Produces the difference of two solutions. It will used to show that the difference of two particular
||| solutions satisfies the homogeneous equation.
solDifference: (a: ZZ) -> (b: ZZ) -> (c: ZZ) -> (x1: ZZ) -> (y1: ZZ) -> (x2: ZZ) ->
(y2: ZZ) -> (c=(x1*a+y1*b)) -> (c=(x2*a+y2*b)) -> ( 0= ( ((x1-x2)*a) + ((y1-y2)*b) ))
solDifference a b c x1 y1 x2 y2 prf prf1 = rewrite (multDistributesOverPlusLeftZ (x1) (-x2) (a)) in
                                           rewrite (multDistributesOverPlusLeftZ (y1) (-y2) (b)) in
                                           rewrite sym (plusAssociativeZ (x1*a) ((-x2)*a) (y1*b+((-y2)*b)) ) in
                                           rewrite (plusCommutativeZ (y1*b) ((-y2)*b)) in
                                           rewrite (plusAssociativeZ ((-x2)*a) ((-y2)*b) (y1*b)) in
                                           rewrite (plusCommutativeZ (((-x2)*a) + ((-y2)*b)) (y1*b)) in
                                           rewrite (plusAssociativeZ (x1*a) (y1*b) (((-x2)*a) + ((-y2)*b))) in
                                           rewrite (multNegateLeftZ (x2) (a)) in
                                           rewrite (multNegateLeftZ (y2) (b)) in
                                           rewrite sym (negateDistributesPlus (x2*a) (y2*b)) in
                                           rewrite sym (plusNegateInverseLZ (x2*a+y2*b)) in
                                           rewrite sym prf in
                                           rewrite sym prf1 in
                                           rewrite (plusNegateInverseLZ c) in
                                           Refl

||| Adding x2 to both sides of the equation:
addToSol: (x1: ZZ) -> (x2: ZZ) -> (x1-x2=d) -> (x1=x2+d)
addToSol x1 x2 prf = rewrite sym prf in
                       rewrite (plusCommutativeZ (x1) (-x2)) in
                       rewrite (plusAssociativeZ (x2) (-x2) (x1)) in
                       rewrite (plusNegateInverseLZ (x2)) in
                       rewrite (plusZeroLeftNeutralZ (x1)) in
                       Refl

||| Proves that two particular solutions differ by a solution of the homogeneous equation.
diffIsHomogeneous: {a: ZZ} -> {b: ZZ} -> {c: ZZ} -> {d: ZZ} ->  {x1: ZZ} -> {y1: ZZ} -> {x2: ZZ} ->
{y2: ZZ} -> (IsDivisibleZ c d) -> (gcdpf:GCDZ a b d) -> NotBothZeroZ a b  ->
    (c=x1*a+y1*b) -> (c=x2*a+y2*b) ->
       (k:ZZ** (( (x1-x2) = (k * (-(bByd gcdpf)))),( (y1-y2) = (k * (aByd gcdpf)))))
diffIsHomogeneous {a}{b}{c}{d}{x1}{y1}{x2}{y2} x gcdpf abnotZ  prf prf1 =
 homoOnlySolnGen {a}{b}{d} (x1-x2) (y1-y2) (gcdpf) (solDifference a b c x1 y1 x2 y2 prf prf1) abnotZ

||| Proves that any solution is a particular solution plus a constant multiple of the solution of
||| the homogeneous equation.
differByHomogeneous: {a: ZZ} -> {b: ZZ} -> {c: ZZ} -> {d: ZZ} ->  {x1: ZZ} -> {y1: ZZ} ->
 (IsDivisibleZ c d) -> (gcdpf:GCDZ a b d) -> NotBothZeroZ a b  ->
   (c=x1*a+y1*b) ->(x2:ZZ)->(y2:ZZ)-> (c=x2*a+y2*b) ->
      (k:ZZ** (( x2 = x1 + (k * (-(bByd gcdpf)))),( y2 = y1 + (k * (aByd gcdpf)))))
differByHomogeneous {x1}{y1} x gcdpf y  prf x2 y2 prf1 =
  (case diffIsHomogeneous x gcdpf y prf1 prf of
        (k**(xpf,ypf)) => (k**((addToSol x2 x1 xpf),(addToSol y2 y1 ypf))))

|||A helper function for allsolutions.
|||It proves that all x and y of the given form satisfies the equation.
helpallsolutions:(gcdpf:(GCDZ a b d))->(bbyd*a=abyd*b)->c = x1*a+y1*b->{k:ZZ}->
   (x3:ZZ)->(y3:ZZ)->(x3=x1+k*(-bbyd))->(y3=y1+k*abyd)->(c=(x3)*a+(y3)*b)
helpallsolutions{bbyd}{abyd} {x1}{y1}{a}{b}{d}{c}{k} gcdpf bydpf eqpf x3 y3 xpf ypf =
  rewrite xpf in
  rewrite ypf in
  rewrite multDistributesOverPlusLeftZ x1 (k*(-bbyd)) a in
  rewrite sym $ plusAssociativeZ (x1*a) ((k*(-bbyd))*a) (multZ (plusZ y1 (multZ k abyd)) b) in
  rewrite plusCommutativeZ ((k*(-bbyd))*a) ((y1+ (k*abyd))*b) in
  rewrite plusAssociativeZ (x1*a) ((y1+ (k*abyd))*b) ((k*(-bbyd))*a) in
  rewrite multDistributesOverPlusLeftZ y1 (k*abyd) b in
  rewrite plusAssociativeZ (x1*a) (y1*b) ((k*abyd)*b) in
  rewrite sym $ eqpf in
  rewrite sym $ plusAssociativeZ c ((k*abyd)*b) ((k*(-bbyd))*a) in
  rewrite sym $ multAssociativeZ k abyd b in
  rewrite sym $ multAssociativeZ k (-bbyd) a in
  rewrite sym $ bydpf in
  rewrite sym $ multDistributesOverPlusRightZ k (bbyd*a) ((-bbyd)*a) in
  rewrite multNegateLeftZ bbyd a in
  rewrite plusNegateInverseLZ (bbyd*a) in
  rewrite multZeroRightZeroZ k in
  rewrite plusZeroRightNeutralZ c in
  Refl

|||The function that generates the third case in findAllSolutions function.
allSolutions:(gcdpf:(GCDZ a b d)) -> IsDivisibleZ c d ->NotBothZeroZ a b ->
   (x1:ZZ**y1:ZZ**pa:ZZ**pb:ZZ**(({k:ZZ}->(x3:ZZ)->(y3:ZZ)->(x3=x1+k*pa)->(y3=y1+k*pb)->(c=x3*a+y3*b)),
     ((x2:ZZ)->(y2:ZZ)->(c=x2*a+y2*b)->(k**((x2=x1+k*pa),(y2=y1+k*pb))))))
allSolutions{a}{b}{d} (dPos, ((abyd**apf),(bbyd**bpf)),fd) dDivc abnotZ =
  (case ((multipleOfGcdLinComb (dPos, ((abyd**apf),(bbyd**bpf)),fd) dDivc),
  (divByGcdMultByOtherIsSame (dPos, ((abyd**apf),(bbyd**bpf)),fd))) of
    ((x1**y1**eqpf),bydpf) =>(x1**y1**(-bbyd)**abyd**(
     (helpallsolutions (dPos, ((abyd**apf),(bbyd**bpf)),fd) bydpf eqpf ),
        ( (differByHomogeneous  dDivc (dPos, ((abyd**apf),(bbyd**bpf)),fd) abnotZ eqpf  ) ))))

|||Given three integers a, b and c, it outputs either
|||a proof that c = xa +yb is impossible or
|||a proof that all integers x and y satisfy the equation (this happens when a=b=c=0)
|||or 4 integers x1 , y1 , pa and pb such that for any integer k,
|||x=x1+k*pa  y=y1+k*pb is a solution of c=xa+yb
|||and whenever c=xa+yb ,there exists an integer, k such that
||| x=x1+k*pa  y=y1+k*pb
findAllSolutions: (a:ZZ)->(b:ZZ)->(c:ZZ)->
  Either ((x:ZZ)->(y:ZZ)->c=x*a+y*b->Void)
  (Either ((x:ZZ)->(y:ZZ)->c=x*a+y*b)
    (x1:ZZ**y1:ZZ**pa:ZZ**pb:ZZ**(({k:ZZ}->(x:ZZ)->(y:ZZ)->(x=x1+k*pa)->(y=y1+k*pb)->(c=x*a+y*b)),
      ((x:ZZ)->(y:ZZ)->(c=x*a+y*b)->(k**((x=x1+k*pa),(y=y1+k*pb)))))))
findAllSolutions a b c =
  (case checkNotBothZero a b of
        (Left (aZ,bZ)) =>
           (case decZero c of
                 (Yes cnotz) => Left (notZeroNotLinCombZeroZero aZ bZ cnotz)
                 (No ciszero) => Right (Left (zeroLinCombZeroZero aZ bZ
                    (notNotZeroThenZero ciszero))))
        (Right abnotZ) =>
          (case gcdZZ a b abnotZ of
            (g**gcdpf) =>
             (case decDivisibleZ c g of
                   (Yes prf) => Right (Right (allSolutions gcdpf prf abnotZ ))
                   (No contra) => Left (gcdDivLinCombContra gcdpf contra ))))


text:
module Main

import TypeCheck
import Machine
import Syntax
import Compile
import Lexer
import Parser

import Effects
import Effect.StdIO

import Control.Monad.Identity
import Lightyear as Ly
import Lightyear.Core as LyC
import Lightyear.Strings as LyS

quit : String
quit = ":q"

prompt : String
prompt = "MiniML> "

welcome : String
welcome = "MiniML. Use " ++ quit ++ " or ^D to quit."

farewell : String
farewell = "Goodbye."

implementation Layout (List Lexeme) where
  lineLengths xs = map (toIntNat . Prelude.Strings.length) . lines $ show xs

lex : String -> Either String (List Lexeme)
lex i = let Id r = LyC.execParserT lexer i in
  case r of
    Success "" lexemes => Right lexemes
    Success left _     => Left $ "Unexpected EOS while lexing: " ++ (show left)
    Failure es         => Left $ formatError i es

parse : List Lexeme -> Either String (List TopLevelCmd)
parse i = let Id r = LyC.execParserT toplevel i in
  case r of
    Success [] cmds    => Right cmds
    Success lexemes _  => Left ("Unexpected EOS while parsing: " ++ (show lexemes))
    Failure es         => Left $ formatError i es

runEither : Frame -> Env -> Either MachineError (MValue, Env)
runEither frm env = the (Either MachineError (MValue, Env)) (mrun frm env)

ErrorMsg : Type
ErrorMsg = String

execCmd : (Ctx, Env) -> TopLevelCmd -> Either ErrorMsg ((Ctx, Env), String)
execCmd (ctx, env) cmd = case cmd of
  TopExpr e => do
    ty <- typeOf ctx e
    let frm = compile e
    (v, env') <- runEither frm env
    pure $ case e of
      Fun name _ pTy rTy body => (((name, ty) :: ctx, (name, v) :: env'), name ++ " : " ++ show ty ++ " = " ++ show v)
      _                       => ((ctx, env'), "- : " ++ show ty ++ " = " ++ show v)
  TopDef name e => do
    ty <- typeOf ctx e
    let frm = compile e
    (v, env') <- runEither frm env
    pure $ (((name, ty) :: ctx, (name, v) :: env'),
            name ++ " : " ++ show ty ++ " = " ++ show v)

execCmds : (Ctx, Env) -> List TopLevelCmd -> IO (Ctx, Env)
execCmds ctxEnv Nil = pure ctxEnv
execCmds ctxEnv (cmd :: cmds) =
  case execCmd ctxEnv cmd of
    Right (ctxEnv', result) => do putStrLn result
                                  ctxEnv'' <- execCmds ctxEnv' cmds
                                  pure ctxEnv''
    Left errMsg             => do putStrLn ("Error: " ++ errMsg)
                                  pure ctxEnv

printTyPair : (Name, Ty) -> IO ()
printTyPair (name, ty) = putStrLn ("  " ++ name ++ " : " ++ show ty)

printTypeEnv : Ctx -> IO ()
printTypeEnv ctx = do
  putStrLn "typing environment {"
  for_ ctx printTyPair
  putStrLn "}"

printValPair : (MName, Lazy MValue) -> IO ()
printValPair (name, v) = putStrLn $ "  " ++ name ++ " : " ++ show (Force v)

printValueEnv : Env -> IO ()
printValueEnv env = do
  putStrLn "value environment {"
  for_ env printValPair
  putStrLn "}"

debugEnvirons : Bool
debugEnvirons = False

mutual
  myRepl : (Ctx, Env) -> IO ()
  myRepl ctxEnv = do
    when (debugEnvirons) (case ctxEnv of
      (ctx, env) => do printTypeEnv ctx
                       printValueEnv env
    )
    putStr prompt
    line <- getLine
    isEof <- fEOF stdin
    if isEof then putStrLn ""
    else if line == quit then pure ()
    else case line of
           ""   => myRepl ctxEnv
           line => case lex line >>= parse of
                     Right cmds => do ctxEnv' <- execCmds ctxEnv cmds
                                      myRepl ctxEnv'
                     Left err   => do putStrLn $ "Error: " ++ err
                                      myRepl ctxEnv

interactive : IO ()
interactive = do
  putStrLn welcome
  myRepl ([], [])
  putStrLn farewell

execFile : (Ctx, Env) -> String -> IO ()
execFile ctxEnv contents =
  case lex contents >>= parse of
    Right cmds => do _ <- execCmds ctxEnv cmds
                     pure ()
    Left err   => putStrLn $ "Error: " ++ err

main : IO ()
main = do
  args <- getArgs
--  putStrLn $ show args
  case args of
    [prog, filename] => do r <- readFile filename
                           case r of
                             Right contents => execFile ([], []) contents
                             Left _         => putStrLn $ "Cannot read " ++ filename
    [prog]           => interactive
    _                => putStrLn "Usage: miniml [filename]"

max_stars_repo_name: steshaw/idris-miniml

max_issues_repo_name: steshaw/idris-miniml

max_forks_repo_name: steshaw/idris-miniml


text:
module RecordList

import Flexidisc.Record
import Flexidisc.Record.Transformation
import Flexidisc.RecordList

||| `RecordList` are Heterogeneous lists of record
people : RecordList String [ [ "firstname" ::: String
                             , "lastname"  ::: String
                             , "age"       ::: Nat
                             , "location"  ::: Maybe String
                             ]
                           , [ "firstname" ::: String
                             , "location"  ::: String
                             ]
                           ]
people = [ [ "firstname" := "John"
           , "lastname"  := "Doe"
           , "age"       := 42
           , "location"  := Nothing
           ]
         , [ "firstname" := "Waldo"
           , "location" := "Hidden"
           ]
         ]

||| We can find the first record that match the partial information we provide
whereIsWaldo : Maybe (header ** Record String header)
whereIsWaldo = firstWith ["firstname" := is "Waldo"] people

whereIsDoe : Maybe (header ** Record String header)
whereIsDoe = firstWith ["lastname" := is "Doe"] people

||| You can even search for something that is not available in every record
whoIs42 : Maybe (header ** Record String header)
whoIs42 = firstWith ["age" := is (the Nat 42)] people

-- with one limitation, if you look for a specific row,
-- it should have the same type in every rows where it's defined
--
-- this would fail:
--
-- whoIsHidden : Maybe (header ** Record String header)
-- whoIsHidden = firstWith ["location" := is "Hidden"] people

max_stars_repo_name: berewt/flexidisc

max_issues_repo_name: LIST-LUXEMBOURG/flexidisc

max_forks_repo_name: LIST-LUXEMBOURG/flexidisc


text:
module Issue660

%default total

data Sig : (a : Type) -> (a -> Type) -> Type where

data Value : Unit -> Type where
  MkV : Sig Unit Value -> Value ()


text:
import Common

list : Iso a b -> Iso (List a) (List b)
list (MkIso abto abfrom abtf abft) = MkIso to from tf ft
  where
    to : List a -> List b
    to [] = []
    to (x :: xs) = abto x :: to xs
    from : List b -> List a
    from [] = []
    from (x :: xs) = abfrom x :: from xs
    tf [] = Refl
    tf (x :: xs) = rewrite (abtf x) in cong (tf xs)
    ft [] = Refl
    ft (x :: xs) = rewrite (abft x) in cong (ft xs)

dep_to : Iso b c -> a -> b -> (a, c)
dep_to (MkIso to' from' tf' ft') x y = (x, (to' y))

dep_from : Iso b c -> a -> c -> (a, b)
dep_from (MkIso to' from' tf' ft') x y = (x, (from' y))

dep : (a -> Iso b c) -> Iso (a, b) (a, c)
dep f = MkIso to from tf ft
  where
    to : (a, b) -> (a, c)
    to (x, y) = dep_to (f x) x y
    from : (a, c) -> (a, b)
    from (x, y) = dep_from (f x) x y
    tf (x, y) = case (inspect $ f x) of
      (match (MkIso to' from' tf' ft') {eq=fx}) => rewrite fx in
        case (dep_from (MkIso to' from' tf' ft') x y) of
          (x', y') => rewrite fx in
            case (dep_to (MkIso to' from' tf' ft') x (from' y)) of
              (x'', y'') => rewrite (tf' y) in Refl
    ft (x, y) = case (inspect $ f x) of
      (match (MkIso to' from' tf' ft') {eq=fx}) => rewrite fx in
        case (dep_to (MkIso to' from' tf' ft') x y) of
          (x', y') => rewrite fx in
            case (dep_from (MkIso to' from' tf' ft') x (to' y)) of
              (x'', y'') => rewrite (ft' y) in Refl

max_stars_repo_name: defanor/morphisms

max_issues_repo_name: defanor/morphisms

max_forks_repo_name: defanor/morphisms


text:
module GRL.Test.Utils

import GRL.Lang.GLang
import GRL.Eval

import Debug.Trace

%default total
%access public export

data TestResults : Type where
  BadModel     : TestResults
  BadResults   : List (GoalNode, SValue, SValue) -> TestResults
  ValidResults : TestResults

getResult : GoalNode -> Strategy -> Maybe (GoalNode, SValue, SValue)
getResult n es =
    let e = getExpSValue n es  in
    let g = getSValue' n       in
      if g == e
        then Nothing
        else Just (n, g, e)
  where
    getSValue' : GoalNode -> SValue
    getSValue' n = fromMaybe NONE (getSValue n)

    getExpectedResult : GoalNode -> Strategy -> Maybe SValue
    getExpectedResult n ss = lookupBy (\x,y => getNodeTitle x == getNodeTitle y) n ss

    getExpSValue : GoalNode -> Strategy -> SValue
    getExpSValue n ss = fromMaybe NONE $ getExpectedResult n ss

collectResults : List GoalNode -> Strategy -> List (GoalNode, SValue, SValue)
collectResults Nil     ss = Nil
collectResults (g::gs) ss =
  case getResult g ss of
    Nothing => collectResults gs ss
    Just x  => x :: collectResults gs ss

partial
execTest : GModel -> Maybe Strategy -> Strategy -> TestResults
execTest m s es =
    case (evaluate FORWARD s m) of
      BadModel   => BadModel
      Result res => case collectResults res es of
        Nil  => ValidResults
        xs   => BadResults xs

partial
printResults : List (GoalNode, SValue, SValue) -> IO ()
printResults Nil     = pure ()
printResults ((n,g,e)::xs) = do
    putStrLn $ unwords
      [show $ getNodeTitle n , show g, show e]
    printResults xs

partial
doTest : GModel -> Strategy -> Strategy -> IO ()
doTest m s es = do
  case execTest m (Just s) es of
    BadModel      => printLn "Bad Model Evaluation"
    ValidResults  => printLn "Test Passed"
    BadResults xs => do
      putStrLn "Tests Failed"
      printResults xs

partial
runEval : GModel -> Maybe Strategy -> IO ()
runEval m s = do
    putStrLn "Results"
    let res = evaluate FORWARD s m
    putStrLn $ fromMaybe "Nout" $ toString res (\x => show x)

max_stars_repo_name: jfdm/idris-grl

max_issues_repo_name: jfdm/idris-grl

max_forks_repo_name: jfdm/idris-grl


text:
module Specdris.SpecTest

import Specdris.Spec
import Specdris.TestUtil

testCase : IO ()
testCase
  = do state <- specWithState $ do
             describe "context 1" $ do
               describe "context 1.1" $ do
                 it "context 1.1.1" $ do
                   1 === 2
                   1 === 1

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

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

export
specSuite : IO ()
specSuite = do putStrLn "\n  spec:"
               testCase

max_stars_repo_name: pheymann/specdris

max_issues_repo_name: pheymann/specdris

max_forks_repo_name: pheymann/specdris


text:
-- exercises in "Type-Driven Development with Idris"
-- chapter 11, section 1

import Data.Primitives.Views

-- check that all functions are total
%default total

data InfList : Type -> Type where
  (::) : (value : elem) -> Inf (InfList elem) -> InfList elem

%name InfList xs, ys, zs

every_other : Stream Int -> Stream Int
every_other (first :: second :: rest) = second :: every_other rest

Functor InfList where
  map f (value :: xs) = f value :: map f xs

countFrom : Integer -> InfList Integer
countFrom x = x :: Delay (countFrom (x + 1))

getPrefix : (count : Nat) -> InfList ty -> List ty
getPrefix Z xs = []
getPrefix (S k) (value :: xs) = value :: getPrefix k xs

data Face = Head | Tails

partial
coinFlips : (count : Nat) -> Stream Int -> List Face
coinFlips n xs = map helper $ take n xs
  where
    total
    helper : Int -> Face
    helper x with (divides x 2)
      helper ((2 * div) + rem) | (DivBy prf)
        = if rem == 0 then Head else Tails

randoms : Int -> Stream Int
randoms seed = let seed' = 1664525 * seed + 1013904223 in
                (seed' `shiftR` 2) :: randoms seed'

square_root_approx : (number : Double) -> (approx : Double) -> Stream Double
square_root_approx number approx
  = approx :: (square_root_approx number next)
    where
      next = (approx + (number / approx)) / 2

square_root_bound : (max : Nat) -> (number : Double) -> (bound : Double) ->
                    (approxs : Stream Double) -> Double
square_root_bound Z _ _ (val :: _) = val
square_root_bound (S k) n bound (val :: xs)
  = if (abs (val * val - n)) <= bound
      then val
      else square_root_bound k n bound xs

square_root : (number : Double) -> Double
square_root n = square_root_bound 100 n 0.00000000001 (square_root_approx n n)

max_stars_repo_name: pascalpoizat/idris-book

max_issues_repo_name: pascalpoizat/idris-book

max_forks_repo_name: pascalpoizat/idris-book


text:
module Text.Parser.Expression

import Text.Parser

public export
data Assoc
   = AssocNone
   | AssocLeft
   | AssocRight

public export
data Op state k a
  = Prefix (Grammar state k True (a -> a))
  | Postfix (Grammar state k True (a -> a))
  | Infix (Grammar state k True (a -> a -> a)) Assoc

public export
OperatorTable : Type -> Type -> Type -> Type
OperatorTable state k a = List (List (Op state k a))

export
buildExpressionParser :
  OperatorTable state k a ->
  Grammar state k True a ->
  Grammar state k True a
buildExpressionParser table term = foldl level term table
  where
    level : Grammar state k True a -> List (Op state k a) -> Grammar state k True a
    level factor ops = parseThese <|> factor
      where
        0 BinOp, UnOp : Type
        BinOp = Grammar state k True (a -> a -> a)
        UnOp = Grammar state k True (a -> a)

        0 SortedOps : Type
        SortedOps = (List BinOp, List BinOp, List BinOp, List UnOp, List UnOp)

        separate : Op state k a -> SortedOps -> SortedOps
        separate op (lassoc, rassoc, nassoc, pre, post) = case op of
          Infix p AssocLeft  => (p::lassoc, rassoc, nassoc, pre, post)
          Infix p AssocRight => (lassoc, p::rassoc, nassoc, pre, post)
          Infix p AssocNone  => (lassoc, rassoc, p::nassoc, pre, post)
          Prefix p           => (lassoc, rassoc, nassoc, p::pre, post)
          Postfix p          => (lassoc, rassoc, nassoc, pre, p::post)

        sortedOps : SortedOps
        sortedOps = foldr separate ([], [], [], [], []) ops

        parseThese : Grammar state k True a
        parseThese =
          let (lassoc, rassoc, nassoc, pre, post) = sortedOps

              termP : Grammar state k True a
              prefixP : Grammar state k False (a -> a)
              postfixP : Grammar state k False (a -> a)
              termP = do
                  f <- prefixP
                  x <- factor
                  g <- postfixP
                  pure $ g (f x)

              prefixP = choice pre <|> pure id
              postfixP = choice post <|> pure id

              rassocP : a -> Grammar state k True a
              rassocP1 : a -> Grammar state k False a
              rassocP x = do
                  f <- choice rassoc
                  y <- termP >>= rassocP1
                  pure $ f x y
              rassocP1 x = rassocP x <|> pure x

              lassocP : a -> Grammar state k True a
              lassocP1 : a -> Grammar state k False a
              lassocP x = do
                  f <- choice lassoc
                  y <- termP
                  lassocP1 $ f x y
              lassocP1 x = lassocP x <|> pure x

              nassocP : a -> Grammar state k True a
              nassocP x = do
                  f <- choice nassoc
                  y <- termP
                  pure $ f x y

          in do
              x <- termP
              rassocP x <|> lassocP x <|> nassocP x <|> pure x


text:
module G2Postulate

import G4LowerFormalPSpring
import G3MiddleFunctionsWinter

%access public export
%default total

-- 13
postulate not : GNat -> GNat
-- 15
postulate forall : GNat -> GNat -> GNat
-- 45
postulate proves : GNat -> GNat -> Bool

postulate r : GNat -> GNat


text:
module Chinmaya.Odds

import Intro
import Evens

-- Q.1.
data IsOdd: Nat -> Type where
  SZOdd: IsOdd (S Z)
  SSOdd: (n: Nat) -> IsOdd (n) -> IsOdd (S (S n))

-- Q.2.
threeOdd: IsOdd 3
threeOdd = SSOdd 1 SZOdd

-- Q.3.
twoNotOdd: IsOdd 2 -> Void
twoNotOdd (SSOdd Z SZOdd) impossible
twoNotOdd (SSOdd Z (SSOdd _ _)) impossible

-- Q.4.
nOddSnEven: (n: Nat) -> IsOdd n -> IsEven (S n)
nOddSnEven (S Z) SZOdd = SSEven Z ZEven
nOddSnEven (S (S k)) (SSOdd k x) = SSEven (S k) (nOddSnEven(k)(x))

-- Q.5.
nEvenSnOdd: (n: Nat) -> IsEven n -> IsOdd (S n)
nEvenSnOdd Z ZEven = SZOdd
nEvenSnOdd (S (S k)) (SSEven k x) = SSOdd (S k) (nEvenSnOdd(k)(x))

-- Q.6.
nEvenorOdd: (n: Nat) -> Either(IsEven n)(IsOdd n)
nEvenorOdd Z = Left(ZEven)
nEvenorOdd (S k) = case (nEvenorOdd k) of
                      Left l => Right(nEvenSnOdd k l)
                      Right r => Left(nOddSnEven k r)

-- Q.7.
nNotBoth: (n: Nat) -> IsEven n -> IsOdd n -> Void
nNotBoth (S Z) ZEven SZOdd impossible
nNotBoth (S Z) (SSEven _ _) SZOdd impossible
nNotBoth (S (S k)) (SSEven k x) (SSOdd k y) = nNotBoth k x y

-- Q.8.
addnmOdd: (n: Nat) -> (m: Nat) -> IsOdd n -> IsOdd m -> IsEven (add n m)
addnmOdd (S Z) m SZOdd y = nOddSnEven m y
addnmOdd (S (S k)) m (SSOdd k x) y = SSEven (add k m) (addnmOdd k m x y)

-- double wasn't loading somehow, so copy-pasted def from Intro
-- double: Nat -> Nat
-- double Z = Z
-- double (S k) = S (S (double k))

-- auxiliary Sequal function
Sequal: {n: Nat} -> {m: Nat} -> (n = m) -> (S n = S m)
Sequal Refl = Refl

-- Q.9.
nSdoublem: (n: Nat) -> IsOdd n -> (DPair Nat (\m => (n = S(double(m)))))
nSdoublem (S Z) SZOdd = (Z ** Refl)
nSdoublem (S (S k)) (SSOdd k x) = (S(fst(nSdoublem k x))** Sequal(Sequal(snd(nSdoublem k x))))


text:
module Main

main : IO ()
main = do
    putStrLn "world!"


text:
module XML.Test.XPath

import Text.PrettyPrint.WL

import Test.Unit.Display
import Test.Unit

import Commons.Text.Parser.Test

import XML.DOM
import XML.XPath

import XML.XPath.Parser

bstore : Document DOCUMENT
bstore = mkSimpleDocument root
  where
    rogElem : Document ELEMENT
    rogElem = "isbn" <+=> "123"

    book1 : Document ELEMENT
    book1 = mkSimpleElement "book"
          <++> ("title" <+=>  "Harry Potter")
          <++> ("price" <+=> "29.99")

    book2 : Document ELEMENT
    book2 = mkSimpleElement "book"
          <++> ("title" <+=>  "Learning XML")
          <++> ("price" <+=> "39.35")
          <++> ("isbn"  <+=> "123456")

    root : Document ELEMENT
    root = mkSimpleElement "bookstore" <++> book1 <++> book2 <++> rogElem

people : Document DOCUMENT
people = mkSimpleDocument root
  where
    p1 : Document ELEMENT
    p1 = mkElementPrefix "person" "pre" <=> "Michael"

    p2 : Document ELEMENT
    p2 = "person" <+=> "Eliezer"

    root : Document ELEMENT
    root = mkSimpleElement "people" <++> p1 <++> p2

mkBook : String -> String -> String -> String -> String -> String -> Document ELEMENT
mkBook n a d f l p = mkSimpleElement "book"
    <++> ("title" <+=> n)
    <++> ("author" <+=> a)
    <++> ("desc" <+=> d)
    <++> ("format" <+=> l)
    <++> ("price" <+=> p)

||| http://en.wikibooks.org/wiki/XQuery/XPath_examples
books : Document DOCUMENT
books = mkSimpleDocument root
  where
    desc : Document ELEMENT
    desc = "desc" <+=> "A list of books useful for people first learning how to build web XML web applications."

    book1 : Document ELEMENT
    book1 = mkBook "XQuery"
                   "Priscilla Walmsley"
                   "This book is a highly detailed, through and complete tour of the W3C Query language.  It covers all the key aspects of the language as well as"
                   "Trade press"
                   "Commercial"
                   "49.95"

    book2 : Document ELEMENT
    book2 = mkBook "XQuery Examples"
                   "Chris Wallace"
                   "This book provides a variety of XQuery example programs and is designed to work with the eXist open-source native XML application server."
                   "Wiki-books"
                   "Creative Commons Sharealike 3.0 Attribution-Non-commercial"
                   "29.95"
    book3 : Document ELEMENT
    book3 = mkBook "XForms Tutorial and Cookbook"
                   "Dan McCreary"
                   "This book is an excellent guide for anyone that is just beginning to learn the XForms standard.  The book is focused on providing the reader with simple, but complete examples of how to create XForms web applications."
                   "Wikibook"
                   "Creative Commons Sharealike 3.0 Attribution-Non-commercial"
                   "29.95"

    book4 : Document ELEMENT
    book4 = mkBook "XRX: XForms, Rest and XQuery"
                   "Dan McCreary"
                   "This book is an overview of the key architectural and design patters."
                   "Wikibook"
                   "Creative Commons Sharealike 3.0 Attribution-Non-commercial"
                   "29.95"

    root : Document ELEMENT
    root = mkSimpleElement "books"
        <++> desc
        <++> book1
        <++> book2
        <++> book3
        <++> book4

myQuery : XPath ELEMENT QUERY
myQuery =  Query $
           (Root (Elem "bookstore"))
       </> ((Elem "book")
       </> (Elem "title"))

queryTest : String
         -> String
         -> Document DOCUMENT
         -> Bool
         -> IO Bool
queryTest title q doc chk = do
  putStrLn $ unwords ["Test:" , title]
  case queryDoc q doc of
    Left err => do
      when (chk) $ do
         let errMsg = vcat [
               text errLine
             , text "An error occured" <+> colon
             , indent 2 $ text (show err)
             , text errLine]
         putStrLn $ Default.toString errMsg
      if chk
        then pure False
        else pure True
    Right ( _ ** Empty) => do
      putStrLn "Empty"
      pure False
    Right (_ ** Nodes _ ns) => do
      printLn ns
      pure chk

export
runTests : IO ()
runTests = do
  putStrLn $ "=> XPath"

  NonReporting.runTests
      [ runParseTest showParseError $ parseTest "Query 1" (parseXPathStr) "/root/@test"
      , runParseTest showParseError $ parseTest "Query 2" (parseXPathStr) "/root/text()"
      , runParseTest showParseError $ parseTest "Query 3" (parseXPathStr) "/bookstore/book/title"
      , queryTest "Query 4" "/books/book/title" books True
      ]

max_stars_repo_name: jfdm/idris-xml

max_issues_repo_name: jfdm/idris-xml

max_forks_repo_name: jfdm/idris-xml


text:
module World

import Data.Vect
import Data.Fin
import Command

%default total

public export
data Heading : Type where
  North : Heading
  South : Heading
  West : Heading
  East : Heading

Show Heading where
  show North = "North"
  show South = "South"
  show West = "West"
  show East = "East"

turnLeftHeading : Heading -> Heading
turnLeftHeading North = West
turnLeftHeading South = East
turnLeftHeading West = South
turnLeftHeading East = North

turnRightHeading : Heading -> Heading
turnRightHeading North = East
turnRightHeading South = West
turnRightHeading West = North
turnRightHeading East = South

public export
data Turtle : Nat -> Nat -> Type where
  MkTurtle : Fin xlimit -> Fin ylimit -> Heading -> Turtle xlimit ylimit

export
Show (Turtle x y) where
  show (MkTurtle x y h) = "Turtle " ++ show (finToNat x) ++ " " ++ show (finToNat y) ++ " " ++ show h

export
turnLeft : Turtle x y -> Turtle x y
turnLeft (MkTurtle x y heading) = MkTurtle x y (turnLeftHeading heading)

export
turnRight : Turtle x y -> Turtle x y
turnRight (MkTurtle x y heading) = MkTurtle x y (turnRightHeading heading)

dec : Fin n -> Fin n
dec FZ = FZ
dec (FS x) = weaken x

incInBound : Fin n -> Fin n
incInBound n = case (strengthen (FS n)) of
                 Left _ => n
                 Right new => new

public export
data Tile : Type where
  Empty : Tile
  Wall : Tile
  Finish : Tile

export
Eq Tile where
  Empty == Empty = True
  Finish == Finish = True
  Wall == Wall = True
  _ == _ = False

public export
data World : Type where
  MkWorld : Turtle xlimit ylimit -> Vect xlimit (Vect ylimit Tile) -> World.World

forwardCoords : Heading -> (Fin xlimit, Fin ylimit) -> (Fin xlimit, Fin ylimit)
forwardCoords North (x, y) = (x, (dec y))
forwardCoords West (x, y) = ((dec x), y)
forwardCoords South (x, y) = (x, (incInBound y))
forwardCoords East (x, y) = ((incInBound x), y)

tileAt : Fin xlimit -> Fin ylimit -> Vect xlimit (Vect ylimit Tile) -> Tile
tileAt x y grid = index y (index x grid)

forward : World.World -> World.World
forward (MkWorld (MkTurtle x y heading) grid) =
  let (maybeNewX, maybeNewY) = forwardCoords heading (x, y)
      tileAtNewPosition = tileAt maybeNewX maybeNewY grid
      (newX, newY) = if tileAtNewPosition == Wall
                     then (x, y)
                     else (maybeNewX, maybeNewY)
   in MkWorld (MkTurtle newX newY heading) grid

export
updateWorld : Command -> World.World -> World.World
updateWorld TurnLeft (MkWorld turtle grid) = MkWorld (turnLeft turtle) grid
updateWorld TurnRight (MkWorld turtle grid) = MkWorld (turnRight turtle) grid
updateWorld Forward world = forward world

export
didWin : World.World -> Bool
didWin (MkWorld (MkTurtle x y _) grid) = tileAt x y grid == Finish

max_stars_repo_name: PeterHajdu/tulis

max_issues_repo_name: PeterHajdu/tulis

max_forks_repo_name: PeterHajdu/tulis


text:
||| FFI binding to the low-Level C Sockets bindings for Idris.
|||
||| Modified (C) The Idris Community, 2020
module Network.FFI

import Network.Socket.Data
import System.FFI

idrisSocketClass : String
idrisSocketClass = "io/github/mmhelloworld/idrisjvm/runtime/IdrisSocket"

-- From idris_net.h

%foreign
  "C:idrnet_socket, libidris2_support, idris_net.h"
  jvm' idrisSocketClass "create" "int int int" idrisSocketClass
export
prim__idrnet_socket : (domain, type, protocol : Int) -> PrimIO SocketDescriptor

%foreign "C:idrnet_close, libidris2_support, idris_net.h"
         jvm' idrisSocketClass ".close" idrisSocketClass "void"
export
prim__idrnet_close : (sockdes : SocketDescriptor) -> PrimIO Int

%foreign "C:idrnet_bind, libidris2_support, idris_net.h"
         jvm' idrisSocketClass ".bind"
             "io/github/mmhelloworld/idris2/runtime/IdrisSocket int int java/lang/String int" "int"
export
prim__idrnet_bind : (sockfd : SocketDescriptor) -> (family, socket_type : Int) ->
                    (host : String) -> (port : Port) -> PrimIO Int

%foreign
  "C:idrnet_connect, libidris2_support, idris_net.h"
  jvm' idrisSocketClass ".connect"
    "io/github/mmhelloworld/idrisjvm/runtime/IdrisSocket int int java/lang/String int" "int"
export
prim__idrnet_connect : (sockfd : SocketDescriptor) -> (family, socket_type : Int) ->
                       (host : String) -> (port : Port) -> PrimIO Int

%foreign "C:idrnet_listen, libidris2_support, idris_net.h"
         jvm' idrisSocketClass ".listen" "io/github/mmhelloworld/idris2/runtime/IdrisSocket int" "int"
export
prim__idrnet_listen : (sockfd : SocketDescriptor) -> (backlog : Int) -> PrimIO Int

%foreign "C:idrnet_fdopen, libidris2_support, idris_net.h"
         jvm idrisSocketClass "toFile"
export
prim__idrnet_fdopen : SocketDescriptor -> String -> PrimIO AnyPtr

%foreign "C:idrnet_sockaddr_family, libidris2_support, idris_net.h"
         jvm' idrisSocketClass "getSocketAddressFamily" "java/lang/Object" "int"
export
prim__idrnet_sockaddr_family : (sockaddr : AnyPtr) -> PrimIO Int

%foreign
  "C:idrnet_sockaddr_ipv4, libidris2_support, idris_net.h"
  jvm' idrisSocketClass "getIpv4Address" "java/lang/Object" "java/lang/String"
export
prim__idrnet_sockaddr_ipv4 : (sockaddr : AnyPtr) -> PrimIO String

%foreign "C:idrnet_sockaddr_unix, libidris2_support, idris_net.h"
         jvm' idrisSocketClass "getIpv4Address" "java/net/SocketAddress" "java/lang/String"
export
prim__idrnet_sockaddr_unix : (sockaddr : AnyPtr) -> PrimIO String

%foreign
  "C:idrnet_sockaddr_ipv4_port, libidris2_support, idris_net.h"
  jvm' idrisSocketClass "getIpv4Port" "java/net/SocketAddress" "int"
export
prim__idrnet_sockaddr_ipv4_port : (sockaddr : AnyPtr) -> PrimIO Int

%foreign
  "C:idrnet_sockaddr_port, libidris2_support, idris_net.h"
  jvm' idrisSocketClass ".getPort" "io/github/mmhelloworld/idrisjvm/runtime/IdrisSocket" "int"
export
prim__idrnet_sockaddr_port : (sockfd : SocketDescriptor) -> PrimIO Int

%foreign
  "C:idrnet_create_sockaddr, libidris2_support, idris_net.h"
  jvm' idrisSocketClass "createSocketAddress" "java/lang/Object" "java/lang/Object"
export
prim__idrnet_create_sockaddr : PrimIO AnyPtr

%foreign "C__collect_safe:idrnet_accept, libidris2_support, idris_net.h"
         "C:idrnet_accept, libidris2_support, idris_net.h"
         jvm' idrisSocketClass ".accept"
             "io/github/mmhelloworld/idrisjvm/runtime/IdrisSocket java/lang/Object" idrisSocketClass
export
prim__idrnet_accept : (sockfd : SocketDescriptor) -> (sockaddr : AnyPtr) -> PrimIO SocketDescriptor

%foreign
  "C:idrnet_send, libidris2_support, idris_net.h"
  jvm' idrisSocketClass ".send" "io/github/mmhelloworld/idrisjvm/runtime/IdrisSocket java/lang/String" "int"
export
prim__idrnet_send : (sockfd : SocketDescriptor) -> (dataString : String) -> PrimIO Int

%foreign
  "C:idrnet_send_buf, libidris2_support, idris_net.h"
  jvm' idrisSocketClass ".send" "io/github/mmhelloworld/idrisjvm/runtime/IdrisSocket java/lang/Object int" "int"
export
prim__idrnet_send_buf : (sockfd : SocketDescriptor) -> (dataBuffer : AnyPtr) -> (len : Int) -> PrimIO Int

%foreign "C__collect_safe:idrnet_recv, libidris2_support, idris_net.h"
         "C:idrnet_recv, libidris2_support, idris_net.h"
         jvm' idrisSocketClass ".receive" "io/github/mmhelloworld/idrisjvm/runtime/IdrisSocket int"
             "io/github/mmhelloworld/idrisjvm/runtime/IdrisSocket$ResultPayload"
export
prim__idrnet_recv : (sockfd : SocketDescriptor) -> (len : Int) -> PrimIO AnyPtr

%foreign "C__collect_safe:idrnet_recv_buf, libidris2_support, idris_net.h"
         "C:idrnet_recv_buf, libidris2_support, idris_net.h"
         jvm' idrisSocketClass ".receive" "io/github/mmhelloworld/idrisjvm/runtime/IdrisSocket java/lang/Object int"
             "io/github/mmhelloworld/idrisjvm/runtime/IdrisSocket$ResultPayload"
export
prim__idrnet_recv_buf : (sockfd : SocketDescriptor) -> (buf : AnyPtr) -> (len : Int) -> PrimIO Int

%foreign
  "C:idrnet_sendto, libidris2_support, idris_net.h"
  jvm' idrisSocketClass ".sendTo"
      "io/github/mmhelloworld/idrisjvm/runtime/IdrisSocket java/lang/String java/lang/String int int" "int"
export
prim__idrnet_sendto : (sockfd : SocketDescriptor) -> (dataString,host : String) ->
                      (port : Port) -> (family : Int) -> PrimIO Int

%foreign
  "C:idrnet_sendto_buf, libidris2_support, idris_net.h"
  jvm' idrisSocketClass ".sendToBuffer"
    "io/github/mmhelloworld/idrisjvm/runtime/IdrisSocket java/lang/Object int java/lang/String int int" "int"
export
prim__idrnet_sendto_buf : (sockfd : SocketDescriptor) -> (dataBuf : AnyPtr) ->
                          (buf_len : Int) -> (host : String) -> (port : Port) ->
                          (family : Int) -> PrimIO Int

%foreign "C__collect_safe:idrnet_recvfrom, libidris2_support, idris_net.h"
         "C:idrnet_recvfrom, libidris2_support, idris_net.h"
         jvm' idrisSocketClass ".receive" "io/github/mmhelloworld/idrisjvm/runtime/IdrisSocket int"
             "io/github/mmhelloworld/idrisjvm/runtime/IdrisSocket$ResultPayload"
export
prim__idrnet_recvfrom : (sockfd : SocketDescriptor) -> (len : Int) -> PrimIO AnyPtr

%foreign "C__collect_safe:idrnet_recvfrom_buf, libidris2_support, idris_net.h"
         "C:idrnet_recvfrom_buf, libidris2_support, idris_net.h"
         jvm' idrisSocketClass ".receive" "io/github/mmhelloworld/idrisjvm/runtime/IdrisSocket java/lang/Object int"
             "io/github/mmhelloworld/idrisjvm/runtime/IdrisSocket$ResultPayload"
export
prim__idrnet_recvfrom_buf : (sockfd : SocketDescriptor) -> (buf : AnyPtr) -> (len : Int) -> PrimIO AnyPtr

%foreign
  "C:idrnet_get_recv_res, libidris2_support, idris_net.h"
  jvm' "io/github/mmhelloworld/idrisjvm/runtime/IdrisSocket$ResultPayload" ".getResult"
    "io/github/mmhelloworld/idrisjvm/runtime/IdrisSocket$ResultPayload" "int"
export
prim__idrnet_get_recv_res : (res_struct : AnyPtr) -> PrimIO Int

%foreign
  "C:idrnet_get_recv_payload, libidris2_support, idris_net.h"
  jvm' "io/github/mmhelloworld/idrisjvm/runtime/IdrisSocket$ResultPayload" ".getPayload"
    "io/github/mmhelloworld/idrisjvm/runtime/IdrisSocket$ResultPayload" "java/lang/Object"
export
prim__idrnet_get_recv_payload : (res_struct : AnyPtr) -> PrimIO String

%foreign
  "C:idrnet_free_recv_struct, libidris2_support, idris_net.h"
  jvm' runtimeClass "free" "java/lang/Object" "void"
export
prim__idrnet_free_recv_struct : (res_struct : AnyPtr) -> PrimIO ()

%foreign
  "C:idrnet_get_recvfrom_res, libidris2_support, idris_net.h"
  jvm' "io/github/mmhelloworld/idrisjvm/runtime/IdrisSocket$ResultPayload" ".getResult"
    "io/github/mmhelloworld/idrisjvm/runtime/IdrisSocket$ResultPayload" "int"
export
prim__idrnet_get_recvfrom_res : (res_struct : AnyPtr) -> PrimIO Int

%foreign
  "C:idrnet_get_recvfrom_payload, libidris2_support, idris_net.h"
  jvm' "io/github/mmhelloworld/idrisjvm/runtime/IdrisSocket$ResultPayload" ".getPayload"
    "io/github/mmhelloworld/idrisjvm/runtime/IdrisSocket$ResultPayload" "java/lang/Object"
export
prim__idrnet_get_recvfrom_payload : (res_struct : AnyPtr) -> PrimIO String

%foreign
  "C:idrnet_get_recvfrom_sockaddr, libidris2_support, idris_net.h"
  jvm' "io/github/mmhelloworld/idrisjvm/runtime/IdrisSocket$ResultPayload" ".getRemoteAddress"
    "io/github/mmhelloworld/idrisjvm/runtime/IdrisSocket$ResultPayload" "java/net/SocketAddress"
export
prim__idrnet_get_recvfrom_sockaddr : (res_struct : AnyPtr) -> PrimIO AnyPtr

%foreign
  "C:idrnet_free_recvfrom_struct, libidris2_support, idris_net.h"
  jvm' runtimeClass "free" "java/lang/Object" "void"
export
prim__idrnet_free_recvfrom_struct : (res_struct : AnyPtr) -> PrimIO ()

%foreign
  "C:idrnet_geteagain, libidris2_support, idris_net.h"
  jvm runtimeClass "getEagain"
export
prim__idrnet_geteagain : PrimIO Int

%foreign
  "C:idrnet_errno, libidris2_support, idris_net.h"
  jvm' runtimeClass "getErrorNumber" "java/lang/Object" "int"
export
prim__idrnet_errno : PrimIO Int

%foreign "C:idrnet_peek, libidris2_support, idris_net.h"
         jvm' idrisSocketClass "peek" "java/lang/Object int" "int"
export
prim__idrnet_peek : (ptr : AnyPtr) -> (offset : {-Unsigned-} Int) -> PrimIO {-Unsigned-} Int

%foreign
  "C:idrnet_poke, libidris2_support, idris_net.h"
  jvm' idrisSocketClass "poke" "java/lang/Object int char" "void"
export
prim__idrnet_poke : (ptr : AnyPtr) -> (offset : {-Unsigned-} Int) ->
                    (val : Int {- should be Char? -}) -> PrimIO ()


text:
module Hamming

import Data.Vect

public export
data Nucleotide = A | C | G | T

public export
implementation Eq Nucleotide where
    l == r = ?eq_rhs

export
hamming_distance : Eq a => Vect n a -> Vect n a -> Nat
hamming_distance s1 s2 = ?hamming_distance_rhs

export
version : String
version = "1.0.0"

max_forks_repo_name: ErikSchierboom/idris


text:
module Minecraft.Base.PreClassic.Cobblestone.Export

import public Minecraft.Base.PreClassic.Cobblestone.Block.Export
import public Minecraft.Base.PreClassic.Cobblestone.Item.Export
import public Minecraft.Base.PreClassic.Cobblestone.ItemEntity.Export

%default total

max_stars_repo_name: po-stulate/postulate

max_issues_repo_name: po-stulate/postulate

max_forks_repo_name: po-stulate/postulate


text:
test : Builtin.Equal S (\x : a => S ?)
test = Refl

test2 : ?
test2 = {a : _} -> the (S = \x : a => S _) Refl


text:
module CIL.System.Environment

import CIL.FFI
import CIL.FFI.Array

%access public export

namespace System.Environment

  EnvironmentTy : CILTy
  EnvironmentTy = corlibTy "System.Environment"

  GetCommandLineArgs : CIL_IO StringArray
  GetCommandLineArgs = invokeStatic EnvironmentTy "GetCommandLineArgs" (CIL_IO StringArray)

getArgs : CIL_IO (List String)
getArgs = do
  args <- GetCommandLineArgs
  toList args

max_stars_repo_name: alaendle/idris-cil

max_issues_repo_name: alaendle/idris-cil

max_forks_repo_name: alaendle/idris-cil


text:
module Language.LSP.Message.FoldingRange

import Language.JSON
import Language.LSP.Message.Derive
import Language.LSP.Message.Progress
import Language.LSP.Message.TextDocument
import Language.LSP.Message.Utils
import Language.Reflection

%language ElabReflection
%default total

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_foldingRange
public export
record FoldingRangeClientCapabilities where
  constructor MkFoldingRangeClientCapabilities
  dynamicRegistration : Maybe Bool
  rangeLimit          : Maybe Int
  lineFoldingOnly     : Maybe Bool
%runElab deriveJSON defaultOpts `{{FoldingRangeClientCapabilities}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_foldingRange
public export
record FoldingRangeOptions where
  constructor MkFoldingRangeOptions
  workDoneProgress : Maybe Bool
%runElab deriveJSON defaultOpts `{{FoldingRangeOptions}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_foldingRange
public export
record FoldingRangeRegistrationOptions where
  constructor MkFoldingRangeRegistrationOptions
  workDoneProgress : Maybe Bool
  documentSelector : OneOf [DocumentSelector, Null]
  id               : Maybe String
%runElab deriveJSON defaultOpts `{{FoldingRangeRegistrationOptions}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_foldingRange
public export
record FoldingRangeParams where
  constructor MkFoldingRangeParams
  workDoneToken      : Maybe ProgressToken
  partialResultToken : Maybe ProgressToken
  textDocument       : TextDocumentIdentifier
%runElab deriveJSON defaultOpts `{{FoldingRangeParams}}

namespace FoldingRangeKind
  ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_foldingRange
  public export
  data FoldingRangeKind = Comment | Imports | Region

export
ToJSON FoldingRangeKind where
  toJSON Comment = JString "comment"
  toJSON Imports = JString "imports"
  toJSON Region  = JString "region"

export
FromJSON FoldingRangeKind where
  fromJSON (JString "comment") = pure Comment
  fromJSON (JString "imports") = pure Imports
  fromJSON (JString "region")  = pure Region
  fromJSON _ = neutral

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_foldingRange
public export
record FoldingRange where
  constructor MkFoldingRange
  startLine      : Int
  startCharacter : Maybe Int
  endLine        : Int
  endCharacter   : Maybe Int
  kind           : Maybe String
%runElab deriveJSON defaultOpts `{{FoldingRange}}


text:
record Album where
  constructor MkAlbum
  artist : String
  title : String
  year : Integer

help : Album
help = MkAlbum "The Beatles" "Help" 1965

rubbersoul : Album
rubbersoul = MkAlbum "The Beatles" "Rubber Soul" 1965

clouds : Album
clouds = MkAlbum "Joni Mitchell" "Clouds" 1969

hunkydory : Album
hunkydory = MkAlbum "David Bowie" "Hunky Dory" 1971

heroes : Album
heroes = MkAlbum "David Bowie" "Heroes" 1977

collection : List Album
collection = [help, rubbersoul, clouds, hunkydory, heroes]

Eq Album where
  (==) (MkAlbum artist1 title1 year1) (MkAlbum artist2 title2 year2)
        = artist1 == artist2 && title1 == title2 && year1 == year2

Ord Album where
  compare (MkAlbum artist1 title1 year1) (MkAlbum artist2 title2 year2)
            = case compare artist1 artist2 of
                   EQ => case compare title1 title2 of
                              EQ => compare year1 year2
                              diff_title => diff_title
                   diff_artist => diff_artist

Show Album where
  show (MkAlbum artist title year)
    = title ++ " by " ++ artist ++ " (released " ++ show year ++ ")"


text:
module Conway

import Data.Vect
import Data.Fin

-- Local Variables:
-- idris-load-packages: ("prelude" "effects" "contrib" "base")
-- End:

board : Nat -> Nat -> Type
board n m = Vect n (Vect m Bool)

printChar : Bool -> String
printChar False = "x"
printChar True = "o"

printRow : Vect m Bool -> String
printRow [] = "\n"
printRow (x :: xs) = (printChar x) ++ (printRow xs)

printBoard : board n m -> String
printBoard = concat . map printRow

listFins : (n : Nat) -> Vect n (Fin n)
listFins Z = []
listFins (S k) = FZ :: (map FS (listFins k))

boardAux : Fin n -> Vect m (Fin n, Fin m)
boardAux {n} {m} f = map (\x => (f,x)) (listFins m)

boardCoords : (n : Nat) -> (m : Nat) -> Vect n (Vect m (Fin n, Fin m))
boardCoords n m = map boardAux (listFins n)

promote : Fin k ->  Fin (S k)
promote FZ = FZ
promote (FS x) = (FS (promote x))

safeDec : Fin n -> Fin n
safeDec FZ = FZ
safeDec (FS x) = promote x

maxFin : (n : Nat) -> Fin (S n)
maxFin Z = FZ
maxFin (S k) = FS (maxFin k)

-- this should return the maximum element in the finite set
safeInc : Fin n -> Fin n
safeInc {n = Z} FZ impossible
safeInc {n = Z} (FS _) impossible
safeInc {n = (S k)} f = case (strengthen f) of
                          Left same => same
                          Right f' => (FS f')

myStrengthen : Fin (S n) -> Either (Fin (S n)) (Fin n)
myStrengthen {n = Z} f = Left FZ
myStrengthen {n = (S k)} FZ = Right FZ
myStrengthen {n = (S k)} (FS x) = case (myStrengthen x) of
                                   Left same => Left (FS x)
                                   Right decked => Right (FS decked)

lastV : Vect (S n) a -> a
lastV (x :: []) = x
lastV (x :: (y :: xs)) = lastV (y :: xs)

filterV : (a -> Bool) -> Vect n a -> (m ** (Vect m a))
filterV f [] = (0 ** [])
filterV f (x :: xs) = case (f x) of
                       True => let (n ** xs') = filterV f xs in (S n ** (x :: xs'))
                       False => filterV f xs

nubV : Eq a => Vect n a -> (m ** (Vect m a))
nubV [] = (Z ** [])
nubV (x :: xs) = let (n ** xs') = filterV (\y => y /= x) xs
                     (n' ** xs'') = nubV xs'
                 in (S n' ** (x :: xs''))

neighCoords : Fin n -> Fin m -> List (Fin n, Fin m)
neighCoords fx fy = [(safeInc fx , fy),
                     (safeInc fx , safeInc fy),
                     (fx , safeInc fy),
                     (safeDec fx, safeInc fy),
                     (safeInc fx , safeDec fy),
                     (safeDec fx, fy),
                     (fx , safeDec fy),
                     (safeDec fx, safeDec fy)]

ixer : board n m -> (Fin n, Fin m) -> Lazy Bool
ixer b (fx, fy) = index fy (index fx b)

rhs : Vect n (Vect m (Fin n, Fin m)) -> (b : Vect n (Vect m Bool)) -> (Fin n, Fin m) -> Bool
rhs coords b f = let neigh = uncurry neighCoords f in and $ map (ixer b) neigh

gameStep : board n m -> board n m
gameStep {n} {m} b = let coords = boardCoords n m in map (map (rhs coords b)) coords

repeatF : Nat -> (a -> a) -> a -> a
repeatF Z f = id
repeatF (S k) f = f . (repeatF k f)

-- this is way too specific, but I'm getting bored
placeBoard : board n m -> Fin n -> Fin m -> board n m
placeBoard b fx fy = updateAt fx (\v => updateAt fy (const True) v) b

blankBoard : board n m
blankBoard {n} {m} = map (map (const False)) (boardCoords n m)

mkBoard : (List (Fin n, Fin m)) -> board n m
mkBoard l = foldr (\f,b => uncurry (placeBoard b) f) blankBoard l

max_stars_repo_name: clarissalittler/idris-practice

max_issues_repo_name: clarissalittler/idris-practice

max_forks_repo_name: clarissalittler/idris-practice


text:
module Parser.Source

import public Parser.Lexer.Source
import public Parser.Rule.Source
import public Parser.Unlit

import System.File
import Utils.Either

%default total

export
runParserTo : {e : _} ->
              Maybe LiterateStyle -> (WithBounds Token -> Bool) ->
              String -> Grammar Token e ty -> Either (ParseError Token) ty
runParserTo lit pred str p
    = do str    <- mapError LitFail $ unlit lit str
         toks   <- mapError LexFail $ lexTo pred str
         parsed <- mapError toGenericParsingError $ parse p toks
         Right (fst parsed)

export
runParser : {e : _} ->
            Maybe LiterateStyle -> String -> Grammar Token e ty -> Either (ParseError Token) ty
runParser lit = runParserTo lit (const False)

export covering
parseFile : (fn : String) -> Rule ty -> IO (Either (ParseError Token) ty)
parseFile fn p
    = do Right str <- readFile fn
             | Left err => pure (Left (FileFail err))
         pure (runParser (isLitFile fn) str p)


text:
module Date

import Coda.Range

%access public export
%default total

{-
  ISO 8601 Date Package

  Date Representation inclues:

    Year - Month - Day

  Show interface includes zero-padding of up to 3 zeroes for Year, and 1 zero
  for month and day.

-}

{-
  Type Definitions
-}

data Year : Type where
  MkYear : (year : Integer) -> Year

%name Year y,y1,y2,y3

isLeap : Year -> Bool
isLeap (MkYear year) = (modNatNZ (toNat year) 4 SIsNotZ) == 0

data Month : Type where
  January   : Month
  February  : Month
  March     : Month
  April     : Month
  May       : Month
  June      : Month
  July      : Month
  August    : Month
  September : Month
  October   : Month
  November  : Month
  December  : Month

%name Month m,m1,m2,m3

monthOrder : Month -> Nat
monthOrder January   = 1
monthOrder February  = 2
monthOrder March     = 3
monthOrder April     = 4
monthOrder May       = 5
monthOrder June      = 6
monthOrder July      = 7
monthOrder August    = 8
monthOrder September = 9
monthOrder October   = 10
monthOrder November  = 11
monthOrder December  = 12

monthDays : Year -> Month -> Nat
monthDays _    January   = 30
monthDays year February  = if isLeap year then 29 else 28
monthDays _    March     = 30
monthDays _    April     = 31
monthDays _    May       = 30
monthDays _    June      = 31
monthDays _    July      = 30
monthDays _    August    = 31
monthDays _    September = 30
monthDays _    October   = 31
monthDays _    November  = 30
monthDays _    December  = 31

previousMonth : Month -> Month
previousMonth January   = December
previousMonth February  = January
previousMonth March     = February
previousMonth April     = March
previousMonth May       = April
previousMonth June      = May
previousMonth July      = June
previousMonth August    = July
previousMonth September = August
previousMonth October   = September
previousMonth November  = October
previousMonth December  = November

data Day : Type where
  MkDay : (day : Nat) -> Day

%name Day d,d1,d2,d3

inDayRange : Nat -> Day -> Type
inDayRange n (MkDay day) = inRange (MkRange Z (S n)) day

validDate : Year -> Month -> Day -> Type
validDate year month = inDayRange (monthDays year month)

data Date : Type where
  MkDate : (year : Year) ->
           (month : Month) ->
           (day : Day) ->
           { auto p : (validDate year month day) } -> Date

%name Date d,d1,d2,d3

{-
  Standard Interface Implementations
-}

Eq Year where
  (==) (MkYear y) (MkYear y') = y == y'

Eq Month where
  (==) x y  = monthOrder x == monthOrder y

Eq Day where
  (==) (MkDay y) (MkDay y') = y == y'

Eq Date where
  (==) (MkDate y m d) (MkDate y' m' d') = d == d' && m == m' && y == y'

Ord Year where
  compare (MkYear y) (MkYear y') = compare y y'

Ord Month where
  compare x y = compare (monthOrder x) (monthOrder y)

Ord Day where
  compare (MkDay d) (MkDay d') = compare d d'

Ord Date where
  compare (MkDate y m d) (MkDate y' m' d') =
    case compare y y' of
         EQ => case compare m m' of
                    EQ => compare d d'
                    result => result
         result => result

Show Year where
  show (MkYear year) =
    let s = show year
    in case length s of
            Z => "0000"
            (S Z) => "000" ++ s
            (S (S Z)) => "00" ++ s
            (S (S (S Z))) => "0" ++ s
            _ => s

Show Month where
  show x =
    let s = show $ monthOrder x
    in case length s of
            (S Z) => "0" ++ s
            _ => s

Show Day where
  show (MkDay day) =
    let s = show day
    in case length s of
            (S Z) => "0" ++ s
            _ => s

Show Date where
  show (MkDate y m d) = show y ++ "-" ++ show m ++ "-" ++ show d

max_stars_repo_name: ostera/idris-coda

max_issues_repo_name: ostera/idris-coda

max_forks_repo_name: ostera/idris-coda


text:
module Weekdays

data Weekday = Mon | Tue | Wed | Thu | Fri | Sat | Sun

total next_day : Weekday -> Weekday
next_day Mon = Tue
next_day Tue = Wed
next_day Wed = Thu
next_day Thu = Fri
next_day Fri = Sat
next_day Sat = Sun
next_day Sun = Mon

first_proof : next_day Mon = Tue
first_proof = Refl

total prev_day : Weekday -> Weekday
prev_day Mon = Sun
prev_day Tue = Mon
prev_day Wed = Tue
prev_day Thu = Wed
prev_day Fri = Thu
prev_day Sat = Fri
prev_day Sun = Sat

second_proof : prev_day Mon = Sun
second_proof = Refl

is_it_monday : Weekday -> Bool
is_it_monday Mon = True
is_it_monday _   = False

-- rewriting day = Mon in is_it_monday day
third_proof : (day : Weekday) -> day = Mon -> is_it_monday day = True
third_proof day day_eq_mon = rewrite day_eq_mon in Refl

is_it_sunday : Weekday -> Bool
is_it_sunday Sun = True
is_it_sunday _   = False

-- for x in weekdays, x = Sun -> is_it_sunday x = true
fourth_proof : (day: Weekday) -> day = Sun -> is_it_sunday day = True
fourth_proof day day_eq_sun = rewrite day_eq_sun in Refl

-- same as Void idris type
data Void'

contradiction_proof : is_it_monday Tue = True -> Void'
contradiction_proof Refl impossible

one_eq_two_contradiction : 1 = 2 -> Void'
one_eq_two_contradiction Refl impossible


text:
-- Minimal implicational modal logic, PHOAS approach, initial encoding

module Pi.BoxMp

%default total

-- Types

infixr 0 :=>
data Ty : Type where
  UNIT  :             Ty
  (:=>) : Ty -> Ty -> Ty
  BOX   : Ty       -> Ty

-- Context and truth judgement with modal depth

Cx : Type
Cx = Nat -> Ty -> Type

isTrue : Ty -> Nat -> Cx -> Type
isTrue a d tc = tc d a

-- Terms

infixl 1 :$
data Tm : Nat -> Cx -> Ty -> Type where
  var    : isTrue a d tc                  -> Tm d tc a
  lam'   : (isTrue a d tc -> Tm d tc b)   -> Tm d tc (a :=> b)
  (:$)   : Tm d tc (a :=> b) -> Tm d tc a -> Tm d tc b
  box    : Tm (succ d) tc a               -> Tm d tc (BOX a)
  unbox' : Tm d tc (BOX a)   -> (isTrue a gd tc -> Tm d tc b) -> Tm d tc b

lam'' : (Tm d tc a -> Tm d tc b) -> Tm d tc (a :=> b)
lam'' f = lam' $ \x => f (var x)

unbox'' : Tm d tc (BOX a) -> (Tm gd tc a -> Tm d tc b) -> Tm d tc b
unbox'' x' f = unbox' x' $ \x => f (var x)

syntax "lam"   {a} ":=>" [b]         = lam''   (\a => b)
syntax "unbox" [a'] as {a} ":=>" [b] = unbox'' a' (\a => b)

Thm : Ty -> Type
Thm a = {d : Nat} -> {tc : Cx} -> Tm d tc a

-- Example theorems

rNec : Thm a -> Thm (BOX a)
rNec x =
  box x

aK : Thm (BOX (a :=> b) :=> BOX a :=> BOX b)
aK =
  lam f' :=>
    lam x' :=>
      unbox f' as f :=>
        unbox x' as x :=> box (f :$ x)

aT : Thm (BOX a :=> a)
aT =
  lam x' :=>
    unbox x' as x :=> x

a4 : Thm (BOX a :=> BOX (BOX a))
a4 =
  lam x' :=>
    unbox x' as x :=> box (box x)

t1 : Thm (a :=> BOX (a :=> a))
t1 =
  lam x :=> box (lam y :=> y)

max_stars_repo_name: mietek/formal-logic

max_issues_repo_name: mietek/formal-logic

max_forks_repo_name: mietek/formal-logic


text:
import Effects
import Effect.StdIO
import Effect.State

counter : Eff () [STATE Int, STDIO]
counter = do putStrLn $ "Counter at " ++ show !get
             x <- getStr
             if trim x /= "" then pure ()
                             else do put (!get + 1)
                                     counter

startCounter : Eff () [STDIO]
startCounter = do putStrLn "Off we go!"
                  new (STATE Int) 0 counter
                  putStrLn "Finished!"

main : IO ()
main = run startCounter

max_stars_repo_name: grin-compiler/idris-grin

max_issues_repo_name: grin-compiler/idris-grin

max_forks_repo_name: grin-compiler/idris-grin


text:
module Main

import lib.Library1
import lib.Library3

main : IO ()
main = putStrLn (Library1.salute ++ "\n\n" ++ Library3.salute)


text:
module Streaming.Encoding.Base64

import Streaming.Internal as S
import Streaming.API as S

import Data.Functor.Of

import Streaming.Bytes

import System.File

import Data.Strings

-- import Data.LazyList
import Data.List -- zip

import Data.IOArray

import Control.Monad.State

import Util

import Language.Reflection

import public Streaming.Encoding.Base64.Alphabet

-- base64 is an encoding _from_ binary data _to_ binary data matching a
-- restricted alphabet of characters.
-- https://tools.ietf.org/rfc/rfc4648#section-1

export
data EncodeError = CodepointOutOfRange
                 | InvalidStartByte Bits8
                 | CodepointEndedEarly

export
Show EncodeError where
  show CodepointOutOfRange = "CodepointOutOfRange"
  show (InvalidStartByte x) = "InvalidStartByte " ++ show x
  show CodepointEndedEarly = "CodepointEndedEarly"

export
data DecodeError = CharNotInAlphabet Char | DataEndedEarly | TooMuchPadding

export
Show DecodeError where
  show (CharNotInAlphabet x) = "CharNotInAlphabet: " ++ show x
  show DataEndedEarly = "Encoded data ended early"
  show TooMuchPadding = "TooMuchPadding"

-- base64 can't have a decode error because it pads missing bits.
export
encodeBase64 : Monad m => Alphabet -> Stream (Of Bits8) m r
          -> Stream (Of Char) m r
encodeBase64 alph str0
    = str0 &$
       chunksOf 3 -- this foldl needs to account for folding over 3 instead of less
    |> mapf (store (\str => foldl (\acc,b => shiftL acc 8 .|. cast b) 0
                              (take'' 3 $ str <* replicate 3 0)) -- pad to 3
            |> length -- <^ compute length and combine bits in one pass
            |> \res => effect $ do
                       len :> b <- res
                       pure $ case len of
                         1 => splitGroup 2 b <* yield 65 <* yield 65 -- pads
                         2 => splitGroup 3 b <* yield 65
                         _ => splitGroup 4 b)
    -- ^ Combine up to three Bits8, note the number we got, split based on it
    |> concats
    |> encode alph
  where
    -- Split the Int into 4 six bit parts. Left as Int to skip a cast.
    -- Because we construct the pieces ourself we don't need to do checks later
    -- to be sure our Int fits into our alphabet. Their size means they must.
    splitGroup : forall r. Int -> Of Int r -> Stream (Of Int) m r
    splitGroup n (x :> r) = (iterate (`shiftR`6) x
                         &$ take {r=()} 4
                         |> maps (.&. 0x3F)
                         |> rev -- the shifting makes the order backward
                         |> take n) *> pure r
                         -- e. = 101 46
                         -- Z S 4 = 25 28 56
                         -- A G U u = 0 6 20 46
    -- Take our six bit parts and convert them to chars.
    encode : forall r. Alphabet -> Stream (Of Int) m r -> Stream (Of Char) m r
    encode alph str0 = effect $ do
      Right (b :> str) <- inspect str0
        | Left r => pure . pure $ r
      pure $ if b == 65 -- pad
        then yield alph.pad *> encode alph str
        else yield (alph.toChar b) *> encode alph str

-- What to do if encoded data ends early?
-- Return what was decoded and the rest of the stream?
||| decode Char (from an Alphabet) to binary data
export
decodeBase64 : Monad m => Alphabet -> Stream (Of Char) m r
         -> Stream (Of Bits8) m (Either DecodeError r)
decodeBase64 alph str0 = str0
                      &$ S.filter (not . alph.whitespace) -- ignore whitespace
                      |> validate alph
                      |> chunksOf 4
                      |> mapf (graft alph)
                      |> concats
  where
    -- Ensure the encountered character is part of our alphabet
    validate : forall r. Alphabet -> Stream (Of Char) m r
            -> Stream (Of Char) m (Either DecodeError r)
    validate alph str0 = effect $ do
       Right (c :> str) <- inspect str0
         | Left l => pure . pure . Right $ l
       pure $ if c /= alph.pad
         then case alph.fromChar c of
                Nothing => pure . Left $ CharNotInAlphabet c
                Just _ => wrap (c :> validate alph str)
         else wrap (c :> validate alph str)

    -- Split the collected bytes into `n` eight bit parts.
    splitGroup : forall r. Int -> Of Int r -> Stream (Of Bits8) m r
    splitGroup n (x :> r) = (iterate (`shiftR`8) x
                         &$ take {r=()} 3
                         |> rev
                         |> take n
                         |> maps cast) -- the shifting makes the order backward
                         *> Return r
    -- process 4 chars into 3 bytes
    -- store, check length gotten, unSplit, use what length demands pad otherwise
    graft : forall r. Alphabet -> Stream (Of Char) m r -> Stream (Of Bits8) m r
    graft alph str0 = str0 &$ store (maps (maybe 0 id . alph.fromChar)
                                    |> foldl (\acc,c => shiftL acc 6 .|. c) 0) -- merge chars)
                           |> (length . S.filter (/= alph.pad))
                           |> \x => effect $ do
                             len :> res <- x
                             case len of
                               -- 1 => pure . pure $ Left TooMuchPadding
                               2 => pure (splitGroup 1 res)
                               3 => pure (splitGroup 2 res)
                               _ => pure (splitGroup len res)
-- doesn't quite handle padding right yet


text:
module GameServer.Protocol.Options

import Network.Socket.Data

public export
data RunMode : Type where
  TesterMode : RunMode
  MockMode : RunMode

public export
record Options where
  constructor MkOptions
  ||| The port to use for protocol, either to listen or connect to
  port : Port

  ||| The host to bind server to or connect to
  ||| defaults to `localhost` which will only allow local connections
  host : String

  ||| The mode this instance runs in
  ||| default mode is `TesterMode`
  runMode : RunMode

parseInteger : List Char -> Integer -> Maybe Integer
parseInteger []        acc = Just acc
parseInteger (c :: cs) acc =
  if (c >= '0' && c <= '9')
  then parseInteger cs ((acc * 10) + ((cast c) - (cast '0')))
  else Nothing

export
defaultOptions : Options
defaultOptions = MkOptions 34567 "localhost" TesterMode

doProcessOptions : List String -> Options -> Either String Options
doProcessOptions []                        opts = Right opts
doProcessOptions ("--host" :: arg :: args) opts =
  doProcessOptions args (record { host = arg } opts)
doProcessOptions ("--port" :: arg :: args) opts =
  case parseInteger (unpack arg) 0 of
    Nothing => Left $ "cannot parse " ++ arg ++ " as a port number"
    (Just x) => doProcessOptions args (record { port = fromInteger x } opts)
doProcessOptions ("tester" :: args) opts =
  doProcessOptions args (record { runMode = TesterMode } opts)
doProcessOptions ("mock" :: args) opts =
  doProcessOptions args (record { runMode = MockMode } opts)
doProcessOptions (arg :: _) _ = Left $ "unknown argument " ++ arg

||| Process arguments from the command-line, turning them into
||| `Options`.
|||
||| Returns a `Left` if there's an error in the processing, or
||| a `Right` with the `Options` data filled in.
export
processOptions : List String -> Either String Options
processOptions args = doProcessOptions args defaultOptions

namespace OptionsTest

  can_parse_port_option :
    doProcessOptions [ "--port" , "123" ] Options.defaultOptions = Right (MkOptions 123 "localhost" TesterMode)
  can_parse_port_option = Refl

  can_parse_host_option :
    doProcessOptions [ "--host" , "foo" ] Options.defaultOptions = Right (MkOptions 34567 "foo" TesterMode)
  can_parse_host_option = Refl

  can_parse_run_mode_option :
    doProcessOptions [ "mock" ] Options.defaultOptions = Right (MkOptions 34567 "localhost" MockMode )
  can_parse_run_mode_option = Refl

  can_parse_mock_mode_with_host_port :
    doProcessOptions [ "mock" ,  "--host" , "foo",  "--port" , "123"  ] Options.defaultOptions
      = Right (MkOptions 123 "foo" MockMode )
  can_parse_mock_mode_with_host_port= Refl

max_stars_repo_name: steshaw/hsgames

max_issues_repo_name: steshaw/hsgames

max_forks_repo_name: steshaw/hsgames


text:
||| mutable array
|||
||| Copyright 2021, HATTORI, Hiroki
||| This file is released under the MIT license, see LICENSE for more detail.
|||
module Data.Container.Mutable.RingQueue

import Data.Container.Mutable.Array

import Data.Nat
import Data.IORef
import Data.Fin
import Data.So

%default total

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

export
record IORingQueue t where
  constructor MkIORingQueue
  content : IOArray (Maybe t)
  loc : IORef (Nat, Nat)

export newIORingQueue : HasIO io
  => (cap:Nat) -> {auto 0 capacity_isnt_zer: So (cap /= 0)}
  -> io (IORingQueue t)
newIORingQueue cap@(S c) = pure $ MkIORingQueue !(newIOArray cap Nothing) !(newIORef (0, 0))

export null : HasIO io => IORingQueue a -> io Bool
null q = readIORef q.loc >>= pure . (0 ==) . snd

export length : HasIO io => IORingQueue a -> io Nat
length q = readIORef q.loc >>= pure . snd

export push : HasIO io => a -> IORingQueue a -> io Bool
push x q = do
  (n, m) <- readIORef q.loc
  if m >= capacity q.content
     then pure False
     else do
       writeIOArray q.content (restrict q.content (cast $ n + m)) (Just x)
       writeIORef q.loc (n, m + 1)
       pure True

export pull : HasIO io => IORingQueue a -> io (Maybe a)
pull q = do
  (n, (S m)) <- readIORef q.loc
   | (_, Z) => pure Nothing
  writeIORef q.loc ((n + 1) `mod` (capacity q.content), m)
  let i = restrict q.content $ cast n
  r <- readIOArray q.content i
  writeIOArray q.content i Nothing
  pure r

{-
export
HasIO io => MutableQueue io IORingQueue where
    null q = readIORef q.loc >>= pure . (0 ==) . snd
    length q = readIORef q.loc >>= pure . snd

    push x q = do
      (n, m) <- readIORef q.loc
      if m >= capacity q.content
         then pure False
         else do
           writeIOArray q.content (restrict q.content (cast $ n + m)) (Just x)
           writeIORef q.loc (n, m + 1)
           pure True

    pull q = do
      (n, (S m)) <- readIORef q.loc
        | (_, Z) => pure Nothing
      writeIORef q.loc ((n + 1) `mod` (capacity q.content), m)
      let i = restrict q.content $ cast n
      r <- readIOArray q.content i
      writeIOArray q.content i Nothing
      pure r

-}

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