text:
= IndPrinciples : Induction Principles

> module IndPrinciples
>
> import IndProp
>
> %access public export
> %default total
>

With the Curry-Howard correspondence and its realization in Idris in mind, we
can now take a deeper look at induction principles.

\ \todo[inline]{We've written all induction principles by hand throughout the
chapter, Idris doesn't generate them. Edit the text to reflect this}

== Basics

Every time we declare a new \idr{data} type, Idris automatically generates an
_induction principle_ for this type. This induction principle is a theorem like
any other: If \idr{t} is defined inductively, the corresponding induction
principle is called \idr{t_ind}. Here is the one for natural numbers:

> nat_ind : {P : Nat -> Type} -> P Z -> ((n : Nat) -> P n -> P (S n)) ->
>           ((n : Nat) -> P n)
> nat_ind pz _ Z = pz
> nat_ind pz f (S k) = f k (nat_ind pz f k)

\todo[inline]{Mention it's no coincidence it's similar to fold}

The `induction` tactic is a straightforward wrapper that, at its core, simply
performs `apply t_ind`. To see this more clearly, let's experiment with directly
using `apply nat_ind`, instead of the `induction` tactic, to carry out some
proofs. Here, for example, is an alternate proof of a theorem that we saw in the
`Induction` chapter.

> mult_0_r' : (n : Nat) -> n * Z = Z
> mult_0_r' = nat_ind {P=\x => x*Z = Z}
>   Refl             -- n = Z
>   (\k => id)       -- n = S k

This proof is basically the same as the earlier one, but a few minor differences
are worth noting.

First, in the induction step of the proof (the "\idr{S}" case), we have to do a
little bookkeeping manually (the `intros`) that `induction` does automatically.

Second, we do not introduce \idr{n} into the context before applying
\idr{nat_ind} — the conclusion of \idr{nat_ind} is a quantified formula, and
`apply` needs this conclusion to exactly match the shape of the goal state,
including the quantifier. By contrast, the `induction` tactic works either with
a variable in the context or a quantified variable in the goal.

These conveniences make `induction` nicer to use in practice than applying
induction principles like \idr{nat_ind} directly. But it is important to realize
that, modulo these bits of bookkeeping, applying \idr{nat_ind} is what we are
really doing.

==== Exercise: 2 stars, optional (plus_one_r')

Complete this proof without using the `induction` tactic.

> plus_one_r' : (n : Nat) -> n + 1 = S n
> plus_one_r' n = ?plus_one_r__rhs

$\square$

Idris generates induction principles for every datatype defined with \idr{data},
including those that aren't recursive. Although of course we don't need
induction to prove properties of non-recursive datatypes, the idea of an
induction principle still makes sense for them: it gives a way to prove that a
property holds for all values of the type.

These generated principles follow a similar pattern. If we define a type \idr{t}
with constructors \idr{c1} ... \idr{cn}, Idris generates a theorem with this
shape:

```idris
t_ind : {P : t -> Type},
          ... case for c1 ... ->
          ... case for c2 ... -> ...
          ... case for cn ... ->
        (n : t) -> P n
```

The specific shape of each case depends on the arguments to the corresponding
constructor. Before trying to write down a general rule, let's look at some more
examples. First, an example where the constructors take no arguments:

> data YesNo = Yes' | No'

> yesno_ind : {P : YesNo -> Type} -> P Yes' -> P No' ->
>             ((y : YesNo) -> P y)
> yesno_ind px _ Yes' = px
> yesno_ind _ py No'  = py

==== Exercise: 1 star, optional (rgb)

Write out the induction principle that Idris will generate for the following
datatype. Write down your answer on paper or type it into a comment, and then
compare it with what Idris prints.

> data RGB = Red | Green | Blue

> rgb_ind : ?rgb_ind

$\square$

Here's another example, this time with one of the constructors taking some
arguments.

> data NatList : Type where
>   NNil : NatList
>   NCons : Nat -> NatList -> NatList

> natlist_ind : {P : NatList -> Type} -> P NNil ->
>               ((n : Nat) -> (l : NatList) -> P l -> P (NCons n l)) ->
>               ((l : NatList) -> P l)
> natlist_ind pn _ NNil = pn
> natlist_ind pn f (NCons k x) = f k x (natlist_ind pn f x)

==== Exercise: 1 star, optional (natlist1)

Suppose we had written the above definition a little differently:

> data NatList1 : Type where
>   NNil1 : NatList1
>   NCons1 : NatList1 -> Nat -> NatList1

Now what will the induction principle look like? $\square$

From these examples, we can extract this general rule:

  - The type declaration gives several constructors; each corresponds to one
    clause of the induction principle.

  - Each constructor \idr{c} takes argument types \idr{a1} ... \idr{an}.

  - Each \idr{ai} can be either \idr{t} (the datatype we are defining) or some
    other type \idr{s}.

  - The corresponding case of the induction principle says:

    - "For all values \idr{x1}...\idr{xn} of types \idr{a1}...\idr{an}, if
      \idr{P} holds for each of the inductive arguments (each \idr{xi} of type
      \idr{t}), then \idr{P} holds for \idr{c x1 ... xn}".

==== Exercise: 1 star, optional (byntree_ind)

Write out the induction principle that Idris will generate for the following
datatype. (Again, write down your answer on paper or type it into a comment, and
then compare it with what Idris prints.)

> data Byntree : Type where
>  Bempty : Byntree
>  Bleaf : YesNo -> Byntree
>  Nbranch : YesNo -> Byntree -> Byntree -> Byntree

$\square$

==== Exercise: 1 star, optional (ex_set)

Here is an induction principle for an inductively defined set.

```idris
ExSet_ind : {P : ExSet -> Type} -> ((b : Bool) -> P (Con1 b)) ->
           ((n : Nat) -> (e : ExSet) -> P e -> P (Con2 n e)) ->
           ((e : ExSet) -> P e)
```

Give an \idr{data} definition of \idr{ExSet}:

> -- data ExSet : Type where
> -- FILL IN HERE

$\square$

== Polymorphism

Next, what about polymorphic datatypes?

The inductive definition of polymorphic lists

```idris
data List : (x : Type) -> Type where
  Nil : List x
  Cons : x -> List x -> List x
```

is very similar to that of \idr{NatList}. The main difference is that, here, the
whole definition is _parameterized_ on a set \idr{x}: that is, we are defining a
family of inductive types \idr{List x}, one for each \idr{x}. (Note that,
wherever \idr{List} appears in the body of the declaration, it is always applied
to the parameter \idr{x}.) The induction principle is likewise parameterized on
\idr{x}:

> list_ind : {x : Type} -> {P : List x -> Type} -> P [] ->
>            ((a : x) -> (l : List x) -> P l -> P (a :: l)) ->
>            ((l : List x) -> P l)
> list_ind pn _ [] = pn
> list_ind pn f (h::t) = f h t (list_ind pn f t)

Note that the whole induction principle is parameterized on \idr{x}. That is,
\idr{list_ind} can be thought of as a polymorphic function that, when applied to
a type \idr{x}, gives us back an induction principle specialized to the type
\idr{List x}.

==== Exercise: 1 star, optional (tree)

Write out the induction principle that Idris will generate for the following
datatype. Compare your answer with what Idris prints.

> data Tree : (x : Type) -> Type where
>   Leaf : x -> Tree x
>   Node : Tree x -> Tree x -> Tree x

> tree_ind : ?tree_ind

$\square$

==== Exercise: 1 star, optional (mytype)

Find an inductive definition that gives rise to the following induction
principle:

```idris
mytype_ind : {x : Type} -> {P : MyType x -> Type} ->
             ((a : x) -> P (Constr1 a)) ->
             ((n : Nat) -> P (Constr2 n)) ->
             ((m : MyType x) -> P m -> (n : Nat) -> P (Constr3 m n)) ->
             ((m : MyType x) -> P m)
```

$\square$

==== Exercise: 1 star, optional (foo)

Find an inductive definition that gives rise to the following induction
principle:

```idris
foo_ind : {x, y : Type} -> {P : Foo x y -> Type} ->
       ((a : x) -> P (Bar a)) ->
       ((b : y) -> P (Baz b)) ->
       ((f1 : Nat -> Foo x y) -> ((n : Nat) -> P (f1 n)) -> P (Quux f1)) ->
       ((f2 : Foo x y) -> P f2)
```

$\square$

==== Exercise: 1 star, optional (foo')

Consider the following inductive definition:

> data Foo' : (x : Type) -> Type where
>   C1 : List x -> Foo' x -> Foo' x
>   C2 : Foo' x

What induction principle will Idris generate for \idr{Foo'}? Fill in the blanks,
then check your answer with Idris.)

```idris
foo'_ind : {x : Type} -> {P : Foo' x -> Type} ->
           ((l : List x) -> (f : Foo' x) -> ?hole1 -> ?hole2) ->
           ?hole3 ->
           (f : Foo' x -> ?hole4)
```

$\square$

== Induction Hypotheses

Where does the phrase "induction hypothesis" fit into this story?

The induction principle for numbers

```idris
nat_ind : {P : Nat -> Type} -> P Z -> ((n : Nat) -> P n -> P (S n)) ->
          ((n : Nat) -> P n)
``

is a generic statement that holds for all propositions \idr{P} (or rather,
strictly speaking, for all families of propositions \idr{P} indexed by a number
\idr{n}). Each time we use this principle, we are choosing \idr{P} to be a
particular expression of type \idr{Nat -> Type}.

We can make proofs by induction more explicit by giving this expression a name.
For example, instead of stating the theorem \idr{mult_0_r} as
"\idr{(n : Nat) -> n * 0 = 0}," we can write it as "\idr{(n : Nat) -> P_m0r n}",
where \idr{P_m0r} is defined as...

> P_m0r : (n : Nat) -> Type
> P_m0r n = n * Z = Z

... or equivalently:

> P_m0r' : Nat -> Type
> P_m0r' = \n => n * Z = Z

Now it is easier to see where \idr{P_m0r} appears in the proof.

> mult_0_r'' : (n: Nat) -> P_m0r n
> mult_0_r'' = nat_ind {P=P_m0r}
>   Refl             -- n = Z
>   (\n => id)       -- n = S k

This extra naming step isn't something that we do in normal proofs, but it is
useful to do it explicitly for an example or two, because it allows us to see
exactly what the induction hypothesis is. If we prove \idr{(n : Nat) -> P_m0r n}
by induction on \idr{n} (using either `induction` or `apply nat_ind`), we see
that the first subgoal requires us to prove \idr{P_m0r 0} ("\idr{P} holds for
zero"), while the second subgoal requires us to prove
\idr{(n' : Nat) -> P_m0r n' -> P_m0r (S n')} (that is "\idr{P} holds of
\idr{S n'} if it holds of \idr{n'}" or, more elegantly, "\idr{P} is preserved by
\idr{S}"). The _induction hypothesis_ is the premise of this latter implication
— the assumption that \idr{P} holds of \idr{n'}, which we are allowed to use in
proving that \idr{P} holds for \idr{S n'}.

== More on the `induction` Tactic

The `induction` tactic actually does even more low-level bookkeeping for us than
we discussed above.

Recall the informal statement of the induction principle for natural numbers:

  - If \idr{P n} is some proposition involving a natural number \idr{n}, and we
    want to show that \idr{P} holds for all numbers \idr{n}, we can reason like
    this:

    - show that \idr{P Z} holds

    - show that, if \idr{P n'} holds, then so does \idr{P (S n')}

    - conclude that \idr{P n} holds for all \idr{n}.

So, when we begin a proof with `intros n` and then `induction n`, we are first
telling Idris to consider a _particular_ `n` (by introducing it into the
context) and then telling it to prove something about _all_ numbers (by using
induction).

What Idris actually does in this situation, internally, is to "re-generalize"
the variable we perform induction on. For example, in our original proof that
\idr{plus} is associative...

```coq
Theorem plus_assoc' : forall n m p : Nat,
  n + (m + p) = (n + m) + p.
Proof.
  (* ...we first introduce all 3 variables into the context,
     which amounts to saying "Consider an arbitrary n, m, and
     p..." *)
  intros n m p.
  (* ...We now use the induction tactic to prove P n (that
     is, n + (m + p) = (n + m) + p) for _all_ n,
     and hence also for the particular n that is in the context
     at the moment. *)
  induction n as [| n'].
  - (* n = O *) Refl.
  - (* n = S n' *)
    (* In the second subgoal generated by induction -- the
       "inductive step" -- we must prove that P n' implies
       P (S n') for all n'.  The induction tactic
       automatically introduces n' and P n' into the context
       for us, leaving just P (S n') as the goal. *)
    simpl. rewrite -> IHn'. Refl. Qed.
```

It also works to apply `induction` to a variable that is quantified in the goal.

```coq
Theorem plus_comm' : forall n m : Nat,
  n + m = m + n.
Proof.
  induction n as [| n'].
  - (* n = O *) intros m. rewrite <- plus_n_O. Refl.
  - (* n = S n' *) intros m. simpl. rewrite -> IHn'.
    rewrite <- plus_n_Sm. Refl. Qed.
```

Note that `induction n` leaves `m` still bound in the goal — i.e., what we are
proving inductively is a statement beginning with `forall m`.

If we do `induction` on a variable that is quantified in the goal _after_ some
other quantifiers, the `induction` tactic will automatically introduce the
variables bound by these quantifiers into the context.

```coq
Theorem plus_comm'' : forall n m : Nat,
  n + m = m + n.
Proof.
  (* Let's do induction on m this time, instead of n... *)
  induction m as [| m'].
  - (* m = O *) simpl. rewrite <- plus_n_O. Refl.
  - (* m = S m' *) simpl. rewrite <- IHm'.
    rewrite <- plus_n_Sm. Refl. Qed.
```

==== Exercise: 1 star, optional (plus_explicit_prop)

Rewrite both \idr{plus_assoc'} and \idr{plus_comm'} and their proofs in the same
style as \idr{mult_0_r''} above — that is, for each theorem, give an explicit
definition of the proposition being proved by induction, and state the theorem
and proof in terms of this defined proposition.

> -- FILL IN HERE

$\square$

== Induction Principles in \idr{Type}

Earlier, we looked in detail at the induction principles that Idris generates
for inductively defined _sets_. The induction principles for inductively defined
_propositions_ like \idr{Ev} are a tiny bit more complicated. As with all
induction principles, we want to use the induction principle on \idr{Ev} to
prove things by inductively considering the possible shapes that something in
\idr{Ev} can have. Intuitively speaking, however, what we want to prove are not
statements about evidence but statements about _numbers_: accordingly, we want
an induction principle that lets us prove properties of numbers by induction on
evidence.

For example, from what we've said so far, you might expect the inductive
definition of \idr{Ev}...

```idris
data Ev : Nat -> Type where
  Ev_0 : Ev Z
  Ev_SS : Ev n -> Ev (S (S n))
```

...to give rise to an induction principle that looks like this...

> ev_ind_max : {P : {n : Nat} -> Ev n -> Type} ->
>        P {n=Z} Ev_0 ->
>        ((m : Nat) -> (e : Ev m) -> P {n=m} e -> P {n=S (S m)} (Ev_SS e)) ->
>        ((n : Nat) -> (e : Ev n) -> P {n} e)

... because:

  - Since \idr{Ev} is indexed by a number \idr{n} (every \idr{Ev} object \idr{e}
    is a piece of evidence that some particular number \idr{n} is even), the
    proposition \idr{P} is parameterized by both \idr{n} and \idr{e} — that is,
    the induction principle can be used to prove assertions involving both an
    even number and the evidence that it is even.

  - Since there are two ways of giving evidence of evenness (\idr{Ev} has two
    constructors), applying the induction principle generates two subgoals:

    - We must prove that \idr{P} holds for \idr{Z} and \idr{Ev_0}.

    - We must prove that, whenever \idr{n} is an even number and \idr{e} is an
      evidence of its evenness, if \idr{P} holds of \idr{n} and \idr{e}, then it
      also holds of \idr{S (S n)} and \idr{Ev_SS {n=S (S n)} e}.

  - If these subgoals can be proved, then the induction principle tells us that
    \idr{P} is true for all even numbers \idr{n} and evidence \idr{e} of their
    evenness.

This is more flexibility than we normally need or want: it is giving us a way to
prove logical assertions where the assertion involves properties of some piece
of _evidence_ of evenness, while all we really care about is proving properties
of _numbers_ that are even — we are interested in assertions about numbers, not
about evidence. It would therefore be more convenient to have an induction
principle for proving propositions \idr{P} that are parameterized just by
\idr{n} and whose conclusion establishes \idr{P} for all even numbers \idr{n}:

```idris
       {P : Nat -> Type} ->
       ... ->
       (n : Nat) ->
       Ev n -> P n
```

For this reason, Idris actually generates the following simplified induction
principle for \idr{Ev}:

> ev_ind : {P : Nat -> Type} -> P Z ->
>         ((n : Nat) -> Ev n -> P n -> P (S (S n))) ->
>         ((n : Nat) -> Ev n -> P n)
> ev_ind pz _ Z Ev_0 = pz
> ev_ind pz f (S (S k)) (Ev_SS ev) = f k ev (ev_ind pz f k ev)

In particular, Idris has dropped the evidence term \idr{e} as a parameter of the
the proposition \idr{P}.

In English, \idr{ev_ind} says:

  - Suppose, \idr{P} is a property of natural numbers (that is, \idr{P n} is a
    \idr{Type} for every \idr{n}). To show that \idr{P n} holds whenever \idr{n}
    is even, it suffices to show:

    - \idr{P} holds for \idr{Z},

    - for any \idr{n}, if \idr{n} is even and \idr{P} holds for \idr{n}, then
      \idr{P} holds for \idr{S (S n)}.

As expected, we can apply \idr{ev_ind} directly instead of using `induction`. For
example, we can use it to show that \idr{Ev'} (the slightly awkward alternate
definition of evenness that we saw in an exercise in the `IndProp` chapter)
is equivalent to the cleaner inductive definition \idr{Ev}:

> ev_ev' : Ev n -> Ev' n
> ev_ev' {n} = ev_ind {P=Ev'}
>  Ev'_0
>  (\_, _, ev' => Ev'_sum Ev'_2 ev')
>  n

The precise form of a \idr{data} definition can affect the induction principle
Idris generates.

For example, in chapter `IndProp`, we defined \idr{Le} as:

```idris
data Le : Nat -> Nat -> Type where
  Le_n : Le n n
  Le_S : Le n m -> Le n (S m)
```

This definition can be streamlined a little by observing that the left-hand
argument \idr{n} is the same everywhere in the definition, so we can actually
make it a "general parameter" to the whole definition, rather than an argument
to each constructor.

\todo[inline]{This doesn't actually seem to change anything in our case}

```idris
data Le : (n:Nat) -> Nat -> Type where
  Le_n : Le n n
  Le_S : Le n m -> Le n (S m)
```

The second one is better, even though it looks less symmetric. Why? Because it
gives us a simpler induction principle.

> le_ind : {n : Nat} -> {P : Nat -> Type} -> P n ->
>          ((m : Nat) -> (n <=' m) -> P m -> P (S m)) ->
>          ((n0 : Nat) -> (n <=' n0) -> P n0)
> le_ind {n=n0} pn _ n0 Le_n = pn
> le_ind pn f (S m) (Le_S le) = f m le (le_ind pn f m le)

== Formal vs. Informal Proofs by Induction

Question: What is the relation between a formal proof of a proposition \idr{P}
and an informal proof of the same proposition \idr{P}?

Answer: The latter should _teach_ the reader how to produce the former.

Question: How much detail is needed??

Unfortunately, there is no single right answer; rather, there is a range of
choices.

At one end of the spectrum, we can essentially give the reader the whole formal
proof (i.e., the "informal" proof will amount to just transcribing the formal
one into words). This may give the reader the ability to reproduce the formal
one for themselves, but it probably doesn't _teach_ them anything much.

At the other end of the spectrum, we can say "The theorem is true and you can
figure out why for yourself if you think about it hard enough." This is also not
a good teaching strategy, because often writing the proof requires one or more
significant insights into the thing we're proving, and most readers will give up
before they rediscover all the same insights as we did.

In the middle is the golden mean — a proof that includes all of the essential
insights (saving the reader the hard work that we went through to find the proof
in the first place) plus high-level suggestions for the more routine parts to
save the reader from spending too much time reconstructing these (e.g., what the
\idr{ih} says and what must be shown in each case of an inductive proof), but
not so much detail that the main ideas are obscured.

Since we've spent much of this chapter looking "under the hood" at formal proofs
by induction, now is a good moment to talk a little about _informal_ proofs by
induction.

\todo[inline]{Do we need 2 templates here?}

In the real world of mathematical communication, written proofs range from
extremely longwinded and pedantic to extremely brief and telegraphic. Although
the ideal is somewhere in between, while one is getting used to the style it is
better to start out at the pedantic end. Also, during the learning phase, it is
probably helpful to have a clear standard to compare against. With this in mind,
we offer two templates — one for proofs by induction over _data_ (i.e., where
the thing we're doing induction on lives in \idr{Type}) and one for proofs by
induction over _evidence_ (i.e., where the inductively defined thing lives in
\idr{Type}).

=== Induction Over an Inductively Defined Set

_Template_:

  - _Theorem_: <Universally quantified proposition of the form "For all
    \idr{n:s, P(n)}," where \idr{s} is some inductively defined set.>

    _Proof_: By induction on \idr{n}.

    <one case for each constructor \idr{c} of \idr{s}...>

    - Suppose \idr{n = c a1 ... ak}, where <...and here we state the \idr{IH}
      for each of the \idr{a}'s that has type \idr{s}, if any>. We must show
      <...and here we restate \idr{P(c a1 ... ak)}>.

      <go on and prove \idr{P(n)} to finish the case...>

    - <other cases similarly...> $\square$

_Example_:

  - _Theorem_: For all sets \idr{x}, lists \idr{l : List x}, and numbers
    \idr{n}, if \idr{length l = n} then \idr{index (S n) l = None}.

    _Proof_: By induction on \idr{l}.

    - Suppose \idr{l = []}. We must show, for all numbers \idr{n}, that, if
      \idr{length [] = n}, then \idr{index (S n) [] = None}.

      This follows immediately from the definition of \idr{index}.

    - Suppose \idr{l = x :: l'} for some \idr{x} and \idr{l'}, where
      \idr{length l' = n'} implies \idr{index (S n') l' = None}, for any number
      \idr{n'}. We must show, for all \idr{n}, that, if \idr{length (x::l') = n}
      then \idr{index (S n) (x::l') = None}.

      Let \idr{n} be a number with \idr{length l = n}. Since
      \idr{length l = length (x::l') = S (length l')},
      it suffices to show that
      \idr{index (S (length l')) l' = None}.
      But this follows directly from the induction hypothesis, picking \idr{n'}
      to be \idr{length l'}. $\square$

=== Induction Over an Inductively Defined Proposition

Since inductively defined proof objects are often called "derivation trees,"
this form of proof is also known as _induction on derivations_.

_Template_:

  - _Theorem_: <Proposition of the form "\idr{Q -> P}," where \idr{Q} is some
    inductively defined proposition (more generally, "For all \idr{x} \idr{y}
    \idr{z}, \idr{Q x y z -> P x y z}")>

    _Proof_: By induction on a derivation of \idr{Q}. <Or, more generally,
    "Suppose we are given \idr{x}, \idr{y}, and \idr{z}. We show that
    \idr{Q x y z} implies \idr{P x y z}, by induction on a derivation of
    \idr{Q x y z}"...>

    <one case for each constructor \idr{c} of \idr{Q}...>

      - Suppose the final rule used to show \idr{Q} is \idr{c}. Then <...and
        here we state the types of all of the \idr{a}'s together with any
        equalities that follow from the definition of the constructor and the IH
        for each of the \idr{a}'s that has type \idr{Q}, if there are any>. We
        must show <...and here we restate \idr{P}>.

        <go on and prove \idr{P} to finish the case...>

        <other cases similarly...> $\square$

_Example_

  - _Theorem_: The \idr{<=} relation is transitive — i.e., for all numbers
    \idr{n}, \idr{m}, and \idr{o}, if \idr{n <= m} and \idr{m <= o}, then
    \idr{n <= o}.

    _Proof_: By induction on a derivation of \idr{m <= o}.

      - Suppose the final rule used to show \idr{m <= o} is \idr{Le_n}. Then
        \idr{m = o} and we must show that \idr{n <= m}, which is immediate by
        hypothesis.

      - Suppose the final rule used to show \idr{m <= o} is \idr{Le_S}. Then
        \idr{o = S o'} for some \idr{o'} with \idr{m <= o'}. We must show that
        \idr{n <= S o'}. By induction hypothesis, \idr{n <= o'}.

        But then, by \idr{Le_S}, \idr{n <= S o'}. $\square$

ext: lidr

max_stars_repo_name: diseraluca/software-foundations

max_issues_repo_name: diseraluca/software-foundations

max_forks_repo_name: diseraluca/software-foundations


text:
module Examples

import Hezarfen
import Hezarfen.Hint
import Hezarfen.Prover
import Hezarfen.Definitions

%language ElabReflection
%default total

-- You can generate proofs as expressions, but it's better to
-- generate definitions instead since they are more readable.

f1 : (a -> b) -> (b -> c) -> a -> c
f1 = %runElab hezarfenExpr

-- `f1` is generated as an expression, the rest will be definitions.

f1' : (a -> b) -> (b -> c) -> a -> c
%runElab (hezarfen `{f1'})

-- You can also use the `derive` syntax.

f2 : (a -> b) -> (b -> c) -> (c -> d) -> a -> d
derive f2

f3 : Either a (Either b c) -> Either (Either a b) c
derive f3

f4 : (a, b, c) -> (c, b, a)
derive f4

f5 : (p -> q, p -> r) -> p -> (q, r)
derive f5

f6 : (((a -> b) -> c) -> d) -> ((a -> b) -> c) -> (a -> b) -> d
derive f6

myFst : (a, b) -> a
derive myFst

mySnd : (a, b) -> b
derive mySnd

demorgan1 : Not (Either p q) -> (Not p, Not q)
derive demorgan1

demorgan2 : (Not p, Not q) -> Not (Either p q)
derive demorgan2

demorgan3 : Either (Not p) (Not q) -> Not (p, q)
derive demorgan3

-- This one is classical so it cannot be proved by Hezarfen
-- demorgan4 : Not (p, q) -> Either (Not p) (Not q)
-- demorgan4 = %runElab hezarfen

noContradiction : Not (p , Not p)
derive noContradiction

contrapositive : (p -> q) -> (Not q -> Not p)
derive contrapositive

-- Examples with default values for some types

nat : Nat
%runElab (hezarfen' `{nat} !(add [`{Z}]))

-- Using the more readable syntax

bool : (Bool, a -> a)
obtain bool from [`{True}]

-- Using a lemma
data Even : Nat -> Type where
  EvenZ : Even Z
  EvenSS : Even n -> Even (S (S n))

data Odd : Nat -> Type where
  Odd1 : Odd 1
  OddSS : Odd n -> Odd (S (S n))

evenOrOdd : (n : Nat) -> Either (Even n) (Odd n)
evenOrOdd Z = Left EvenZ
evenOrOdd (S Z) = Right Odd1
evenOrOdd (S (S n)) = case evenOrOdd n of
                           Left ev => Left $ EvenSS ev
                           Right o => Right $ OddSS o

-- You can also use a hint database
hint evenOrOdd
hint EvenSS
hint OddSS

oddOrEven : (n : Nat) -> Either (Odd n) (Even n)
derive' oddOrEven -- derive using hints

evenOrOddSS : (n : Nat) -> Either (Even (S (S n))) (Odd (S (S n)))
derive' evenOrOddSS

decUnit : Dec Unit
derive decUnit

decVoid : Dec Void
derive decVoid

swapEither : Either a b -> Either b a
derive swapEither

swapDec : Dec a -> Dec (Not a)
derive swapDec

notDec : Not a -> Dec a
derive notDec

decNotNot : Dec p -> (Not p -> Void) -> p
derive decNotNot

-- Equalities
eq1 : x = x
derive eq1

eq2 : True = True
derive eq2

-- Treat equalities as an atom if it's not obviously solvable
eq3 : (x = y) -> (x = y)
derive eq3

eq4 : True = False -> False = True
derive eq4

eq5 : x = y -> y = x
derive eq5

eqDec : x = y -> Dec (y = x)
derive eqDec

eqEither : Either (x = y) (y = z) -> Either (z = y) (y = x)
derive eqEither

congS : x = y -> S x = S y
derive congS

decCongB : x = y -> Dec (not x = not y)
derive decCongB

twoToThree : (x = y, y = z) -> (z = y, y = y, y = x)
derive twoToThree

doesntLoop : (a -> b) -> (b -> a) -> a -> b
derive doesntLoop

ext: idr

max_stars_repo_name: joom/hezarfen

max_issues_repo_name: joom/hezarfen

max_forks_repo_name: joom/hezarfen


text:
module Data.Crypto.Hash

import Data.Bits
import Data.Vect

%default total
%access public export

-- TODO: Add `maxMessageLength : Maybe Nat`. This would be `Nothing` for MD5 and
--      `Just (expt 2 64)` for the shorter SHS algos. And it should affect the
--       types of `initialize` and `hashMessage`.
interface Hash h (blockLength : Nat) (outputLength : Nat) | h where
  initialize : h -> Vect m (Bits n) -> List (Bits blockLength)
  initialContext : h -> h
  updateContext : h -> Bits blockLength -> h
  finalize : h -> Bits outputLength

hashMessage : Hash h b outputLength => h -> Vect m (Bits n) -> Bits outputLength
hashMessage hash message =
  finalize (foldl updateContext (initialContext hash) (initialize hash message))

max_stars_repo_name: idris-hackers/idris-crypto

max_issues_repo_name: idris-hackers/idris-crypto

max_forks_repo_name: idris-hackers/idris-crypto


text:
module Graphics.Cairo.Effect

import Data.Vect
import Effects
import Graphics.SDL2.Effect as SDL
import Graphics.Color
import Graphics.Shape
import Graphics.Cairo.Cairo as C

%access public export
%default total

data CairoCtx = MkCairoCtx (Int, Int) SDLRenderer SDLTexture Surface DrawingCtx

data OpenPathCtx = MkOpenPath CairoCtx

drawingCtx : CairoCtx -> DrawingCtx
drawingCtx (MkCairoCtx _ _ _ _ ctx) = ctx

windowSize : CairoCtx -> (Int, Int)
windowSize (MkCairoCtx s _ _ _ ctx) = s

-- Effect resultValue inputResource outputResource
data Cairo : Effect where
     ||| creates the window + renderer. the effect has no result value, consumes no resource and
     ||| the output resource will have type SDLRenderer
     GetCanvas   : SDLCtx               -> sig Cairo () ()          CairoCtx
     CloseCanvas :                         sig Cairo () CairoCtx    ()
     OpenPath    :                         sig Cairo () CairoCtx    OpenPathCtx
     AddPath     :                         sig Cairo () OpenPathCtx OpenPathCtx
     ClosePath   :                         sig Cairo () OpenPathCtx CairoCtx
     Center      :                         sig Cairo () CairoCtx    CairoCtx
     WithCairo   : (DrawingCtx -> IO a) -> sig Cairo a  CairoCtx    CairoCtx

implementation Handler Cairo IO where
  handle ()  (GetCanvas (win, renderer)) k =
         do (width, height) <- getWindowSize win
            texture <- sdlCreateTexture renderer SDL_PIXELFORMAT_ARGB8888 SDL_TEXTUREACCESS_STREAMING width height
            tex <- lockTexture texture
            srf <- C.createSurfaceForData tex width height
            ctx <- C.createContext srf
            k () (MkCairoCtx (width, height) renderer texture srf ctx)
  handle (MkCairoCtx _ renderer texture srf ctx) CloseCanvas k =
         do C.flushSurface srf
            C.destroyContext ctx
            C.destroySurface srf

            unlockTexture texture
            renderCopyFull renderer texture
            k () ()
  handle s (WithCairo f) k = do res <- f (drawingCtx s)
                                k res s
  handle s Center k = do let (w,h) = windowSize s
                         translate (drawingCtx s) (cast w / 2) (cast h / 2)
                         k () s
  handle s OpenPath k = k () (MkOpenPath s)
  handle s AddPath  k = k () s
  handle (MkOpenPath cairoCtx) ClosePath k = k () cairoCtx

CAIRO : Type -> EFFECT
CAIRO res = MkEff res Cairo

CAIRO_OFF : EFFECT
CAIRO_OFF = CAIRO ()

CAIRO_ON : EFFECT
CAIRO_ON = CAIRO CairoCtx

-- ------------------------------------------------------------------------
-- API
-- ------------------------------------------------------------------------

getCanvas : SDLCtx -> { [CAIRO_OFF] ==> [CAIRO_ON] } Eff ()
getCanvas sdlCtx = call $ GetCanvas sdlCtx

closeCanvas : { [CAIRO_ON] ==> [CAIRO_OFF] } Eff ()
closeCanvas = call $ CloseCanvas

-- Drawing Context

setSourceRGBA : Color -> { [CAIRO_ON] } Eff ()
setSourceRGBA color = let (r, g, b, a) = colorToDoubles color
                      in call $ WithCairo (\ctx => C.setSourceRGBA ctx r g b a)

setLineWidth : Double -> { [CAIRO_ON] } Eff ()
setLineWidth width = call $ WithCairo (\ctx => C.setLineWidth ctx width)

stroke : { [CAIRO_ON] } Eff ()
stroke = call $ WithCairo (\ctx => C.stroke ctx)

fill : { [CAIRO_ON] } Eff ()
fill = call $ WithCairo (\ctx => C.fill ctx)

-- Shapes

line : (Double, Double) -> (Double, Double) -> { [CAIRO_ON] } Eff ()
line from to
    = call $ WithCairo (\ctx => do
           C.moveTo ctx from
           C.lineTo ctx to
           C.stroke ctx)

polygon : Path (S (S k)) -> { [CAIRO_ON] } Eff ()
polygon p = call $ WithCairo (\ctx => do C.newPath ctx
                                         C.draw ctx (toPoints p))

triangle : (Double, Double) -> (Double, Double) -> (Double, Double) -> { [CAIRO_ON] } Eff ()
triangle a b c = polygon $ (Line a b) `Append` c
-- transformations

center : { [CAIRO_ON] } Eff ()
center = call Center

rotate : (angle: Double) -> { [CAIRO_ON] } Eff ()
rotate angle = call $ WithCairo (\ctx => C.rotate ctx angle)

max_stars_repo_name: eckart/cairo-idris

max_issues_repo_name: eckart/cairo-idris

max_forks_repo_name: eckart/cairo-idris


text:
module Server.Diagnostics

import Core.Context
import Core.Core
import Core.Directory
import Core.Env
import Core.FC
import Core.Metadata
import Data.OneOf
import Data.String
import Idris.Error
import Idris.Pretty
import Idris.REPL.Opts
import Idris.Resugar
import Idris.Syntax
import Idris.Doc.String
import Language.JSON
import Language.LSP.Message
import Libraries.Data.String.Extra
import Parser.Support
import Server.Configuration
import Server.Log
import Server.Utils
import System.File
import System.Path

keyword : Doc IdrisAnn -> Doc IdrisAnn
keyword = annotate $ Syntax Keyword

buildDiagnostic : DiagnosticSeverity -> Maybe FC -> Doc IdrisAnn -> Maybe (List DiagnosticRelatedInformation) -> Diagnostic
buildDiagnostic severity loc error related =
  MkDiagnostic
    { range              = cast $ fromMaybe replFC loc
    , severity           = Just severity
    , code               = Nothing
    , codeDescription    = Nothing
    , source             = Just "idris2"
    , message            = renderString $ unAnnotateS $ layoutUnbounded error
    , tags               = Nothing
    , relatedInformation = related
    , data_              = Nothing
    }

buildRelatedInformation : URI -> FC -> String -> DiagnosticRelatedInformation
buildRelatedInformation uri fc msg = MkDiagnosticRelatedInformation (MkLocation uri (cast fc)) msg

||| Computes a list of `DiagnosticRelatedInformation` from a compiler error.
|||
||| @uri The URI of the source file.
||| @err The compiler error.
getRelatedErrors : (uri : URI) -> (err : Error) -> List DiagnosticRelatedInformation
getRelatedErrors uri (Fatal err) = getRelatedErrors uri err
getRelatedErrors uri (CantConvert fc _ _ l r) =
  [ buildRelatedInformation uri (getLoc l) "Mismatched type"
  , buildRelatedInformation uri (getLoc r) "Mismatched type"
  ]
getRelatedErrors uri (CantSolveEq fc _ _ l r) =
  [ buildRelatedInformation uri (getLoc l) "Can't solve constraint"
  , buildRelatedInformation uri (getLoc r) "Can't solve constraint type"
  ]
getRelatedErrors uri (PatternVariableUnifies fc fct _ n _) =
  [ buildRelatedInformation uri fct ("Unifies with pattern variable " ++ show n) ]
getRelatedErrors uri (CyclicMeta fc _ _ _) = []
getRelatedErrors uri (WhenUnifying fc _ _ x y _) =
  [ buildRelatedInformation uri (getLoc x) "Error while unification"
  , buildRelatedInformation uri (getLoc y) "Error while unification"
  ]
getRelatedErrors uri (ValidCase _ _ (Right err)) = getRelatedErrors uri err
getRelatedErrors uri (InType _ _ err) = getRelatedErrors uri err
getRelatedErrors uri (InCon _ _ err) = getRelatedErrors uri err
getRelatedErrors uri (InLHS _ _ err) = getRelatedErrors uri err
getRelatedErrors uri (InRHS _ _ err) = getRelatedErrors uri err
getRelatedErrors _ _ = []

pShowMN : {vars : _} -> Term vars -> Env Term vars -> Doc IdrisAnn -> Doc IdrisAnn
pShowMN (Local _ _ _ p) env acc =
  case dropAllNS (nameAt p) of
       MN _ _ => acc <++> parens ("implicitly bound at" <++> pretty (getBinderLoc p env))
       _      => acc
pShowMN _ _ acc = acc

pshow : {vars : _}
     -> Ref Ctxt Defs
     => Ref Syn SyntaxInfo
     => Env Term vars
     -> Term vars
     -> Core (Doc IdrisAnn)
pshow env tm = do
  defs <- get Ctxt
  ntm <- normaliseHoles defs env tm
  itm <- resugar env ntm
  pure $ pShowMN ntm env $ prettyTerm itm

pshowNoNorm : {vars : _}
           -> Ref Ctxt Defs
           => Ref Syn SyntaxInfo
           => Env Term vars
           -> Term vars
           -> Core (Doc IdrisAnn)
pshowNoNorm env tm = do
  defs <- get Ctxt
  itm <- resugar env tm
  pure $ pShowMN tm env $ prettyTerm itm

||| Computes a LSP `Diagnostic` from a compiler warning.
|||
||| @caps The client capabilities related to diagnostics
||| @uri The URI of the source file.
||| @err The compiler warning.
export
warningToDiagnostic : Ref Ctxt Defs
            => Ref Syn SyntaxInfo
            => Ref ROpts REPLOpts
            => (caps : Maybe PublishDiagnosticsClientCapabilities)
            -> (uri : URI)
            -> (warning : Warning)
            -> Core Diagnostic
warningToDiagnostic caps uri warning = do
  defs <- get Ctxt
  warningAnn <- pwarning (killWarningLoc warning)
  let loc = getWarningLoc warning
  let wdir = defs.options.dirs.working_dir
  p <- maybe (pure uri.path) (pure . (wdir </>) <=< nsToSource replFC)
         ((\case PhysicalIdrSrc ident => Just ident; _ => Nothing) . fst <=< isNonEmptyFC =<< loc)
  if uri.path == p
     then do let related = Nothing -- TODO related diagnostics?
             pure $ buildDiagnostic Warning loc warningAnn related
     else pure $ buildDiagnostic Warning (toStart <$> loc) ("In" <++> pretty p <+> colon <++> warningAnn) Nothing

||| Computes a LSP `Diagnostic` from a compiler error.
|||
||| @caps The client capabilities related to diagnostics
||| @uri The URI of the source file.
||| @err The compiler error.
export
errorToDiagnostic : Ref Ctxt Defs
            => Ref Syn SyntaxInfo
            => Ref ROpts REPLOpts
            => (caps : Maybe PublishDiagnosticsClientCapabilities)
            -> (uri : URI)
            -> (error : Error)
            -> Core Diagnostic
errorToDiagnostic caps uri err = do
  defs <- get Ctxt
  error <- perror (killErrorLoc err)
  let loc = getErrorLoc err
  let wdir = defs.options.dirs.working_dir
  p <- maybe (pure uri.path) (pure . (wdir </>) <=< nsToSource replFC)
         ((\case PhysicalIdrSrc ident => Just ident; _ => Nothing) . fst <=< isNonEmptyFC =<< loc)
  if uri.path == p
     then do let related = (flip toMaybe (getRelatedErrors uri err) <=< relatedInformation) =<< caps
             pure $ buildDiagnostic Error loc error related
     else pure $ buildDiagnostic Error (toStart <$> loc) ("In" <++> pretty p <+> colon <++> error) Nothing


text:
data Format = Num Format
            | Str Format
            | Lit String Format
            | End

PrintfType : Format -> Type
PrintfType (Num fmt)   = Int    -> PrintfType fmt
PrintfType (Str fmt)   = String -> PrintfType fmt
PrintfType (Lit x fmt) = PrintfType fmt
PrintfType End         = String

parseFormat : List Char -> Format
parseFormat [] = End
parseFormat ('%' :: 'd' :: xs) = Num (parseFormat xs)
parseFormat ('%' :: 's' :: xs) = Str (parseFormat xs)
parseFormat ('%' :: xs) = Lit "%" (parseFormat xs)
parseFormat (x :: xs) = case parseFormat xs of
                           Lit lit xs' => Lit (strCons x lit) xs'
                           fmt => Lit (strCons x "") fmt

printfFmt : (fmt : Format) -> String -> PrintfType fmt
printfFmt (Num y) x = \i => printfFmt y (x ++ show i)
printfFmt (Str y) x = \s => printfFmt y (x ++ s)
printfFmt (Lit y z) x = printfFmt z (x ++ y)
printfFmt End x = x

printf : (s: String) -> PrintfType (parseFormat (unpack s))
printf s = printfFmt (parseFormat (unpack s)) ""

max_stars_repo_name: fthomas/tdd-talk

max_issues_repo_name: fthomas/tdd-talk

max_forks_repo_name: fthomas/tdd-talk


text:
import ggg

t : Int
t = yyy


text:
module IdrisNet.Packet
import Language.Reflection
import IdrisNet.PacketLang
import Network.Socket
import Effects
import Data.So

%access public
%include C "bindata.h"
%link C "bindata.o"

-- Type synonyms for different arguments to foreign functions
public
BytePos : Type
BytePos = Int

public
Position : Type
Position = Int

public
ByteData : Type
ByteData = Int

public
data ActivePacket : Type where
  ActivePacketRes : BufPtr -> BytePos -> Length -> ActivePacket

public
dumpPacket : BufPtr -> Length -> IO ()
dumpPacket (BPtr pckt) len =
  foreign FFI_C "dumpPacket" (Ptr -> Int -> IO Unit) pckt len

{- Internal FFI Functions -}
foreignCreatePacket : Int -> IO BufPtr
foreignCreatePacket len = map BPtr $ foreign FFI_C "newPacket" (Int -> IO Ptr) len

foreignSetByte : BufPtr -> Position -> ByteData -> IO ()
foreignSetByte (BPtr pckt) dat pos =
  foreign FFI_C "setPacketByte" (Ptr -> Int -> Int -> IO Unit) pckt dat pos

foreignSetBits : BufPtr -> Position -> Position -> ByteData -> IO ()
foreignSetBits (BPtr pckt) start end dat =
  foreign FFI_C "setPacketBits" (Ptr -> Int -> Int -> Int -> IO Unit) pckt start end dat

foreignSetString : BufPtr -> Position -> String -> Int -> Char -> IO ()
foreignSetString (BPtr pckt) start dat len term =
  foreign FFI_C "setPacketString" (Ptr -> Int -> String -> Int -> Char -> IO Unit) pckt start dat len term

foreignGetByte : BufPtr -> Position -> IO ByteData
foreignGetByte (BPtr pckt) pos =
  foreign FFI_C "getPacketByte" (Ptr -> Int -> IO Int) pckt pos

foreignGetBits : BufPtr -> Position -> Position -> IO ByteData
foreignGetBits (BPtr pckt) start end =
  foreign FFI_C "getPacketBits" (Ptr -> Int -> Int -> IO Int) pckt start end

{- Marshalling -}

marshalChunk : ActivePacket -> (c : Chunk) -> (chunkTy c) -> IO Length
marshalChunk (ActivePacketRes pckt pos p_len) (Bit w p) (BInt dat p2) = do
  let len = chunkLength (Bit w p) (BInt dat p2)
  foreignSetBits pckt pos (pos + (natToInt w) - 1) dat
  return len
marshalChunk (ActivePacketRes pckt pos p_len) CBool b = do
  let bit = the Int $ if b then 1 else 0
  foreignSetBits pckt pos pos bit
  return (chunkLength CBool b)
marshalChunk (ActivePacketRes pckt pos p_len) CString str = do
  let len = chunkLength CString str
  --putStrLn $ "CStr length: " ++ (show len)
  foreignSetString pckt pos str len '\0'
  return len
marshalChunk (ActivePacketRes pckt pos p_len) (LString n) str = do
  let len = chunkLength (LString n) str
  foreignSetString pckt pos str len '\0'
  return len
marshalChunk (ActivePacketRes pckt pos p_len) (Decodable n t _ encode_fn) to_encode = do
  let code = encode_fn to_encode
  let len = natToInt n
  foreignSetBits pckt pos (pos + len - 1) (val code)
  return len

marshalChunk (ActivePacketRes pckt pos p_len) (Prop _) x2 = return 0 -- We're not doing anything

marshalList : ActivePacket -> (pl : PacketLang) -> List (mkTy pl) -> IO Length
marshalVect : ActivePacket -> (pl : PacketLang) -> Vect n (mkTy pl) -> IO Length

marshal' : ActivePacket -> (pl : PacketLang) -> mkTy pl -> IO Length
marshal' ap (CHUNK c) c_dat = marshalChunk ap c c_dat
marshal' ap (IF True pl_t _) ite = marshal' ap pl_t ite
marshal' ap (IF False _ pl_f) ite = marshal' ap pl_f ite
marshal' ap (pl_1 // pl_2) x = either (\x_l => marshal' ap pl_1 x_l)
                                      (\x_r => marshal' ap pl_2 x_r) x
marshal' ap (LIST pl) xs = marshalList ap pl xs
marshal' ap (LISTN n pl) xs = marshalVect ap pl xs
marshal' _ NULL _ = return 0
marshal' ap (c >>= k) (x ** y) = do
  len <- marshal' ap c x
  let (ActivePacketRes pckt pos p_len) = ap
  let ap2 = (ActivePacketRes pckt (pos + len) p_len)
  len2 <- marshal' ap2 (k x) y
  return $ len + len2

{- Marshal PacketLang to ByteData -}
--marshalVect : ActivePacket -> (pl : PacketLang) -> Vect n (mkTy pl) -> IO Length
marshalVect ap pl [] = return 0
marshalVect (ActivePacketRes pckt pos p_len) pl (x::xs) = do
  len <- marshal' (ActivePacketRes pckt pos p_len) pl x
  xs_len <- marshalVect (ActivePacketRes pckt (pos + len) p_len) pl xs
  return $ len + xs_len

--marshalList : ActivePacket -> (pl : PacketLang) -> List (mkTy pl) -> IO Length
marshalList ap pl [] = return 0
marshalList (ActivePacketRes pckt pos p_len) pl (x::xs) = do
  len <- marshal' (ActivePacketRes pckt pos p_len) pl x
  xs_len <- marshalList (ActivePacketRes pckt (pos + len) p_len) pl xs
  return $ len + xs_len

{- Unmarshalling Code -}
public
unmarshal' : ActivePacket -> (pl : PacketLang) -> Maybe (mkTy pl, Length)

--unmarshal' : ActivePacket -> (pl : PacketLang) -> Maybe (mkTy pl, Length)
unmarshalCString' : ActivePacket ->
                    Int ->
                    IO (Maybe (List Char, Length))
unmarshalCString' (ActivePacketRes pckt pos p_len) i with (pos + 8 <= p_len)
  -- Firstly we need to check whether we're within the bounds of the packet.
  -- If not, then the parse has failed.
  -- If we're within bounds, we need to read the next character, and recursively
  -- call.
  | True = do
    next_byte <- foreignGetBits pckt pos (pos + 7)
    --putStrLn $ "Byte read: " ++ (show next_byte)
    let char = chr next_byte
    --putStrLn $ "Char: " ++ (show char)
    -- If we're up to a NULL, we've read the string
    if (char == '\0') then do
      return $ Just ([], 8)
    else do -- Otherwise, recursively call
      -- We're assuming sizeof(char) = 8 here
      rest <- unmarshalCString' (ActivePacketRes pckt (pos + 8) p_len) (i + 8)
      case rest of Just (xs, j) => return $ Just (char::xs, j + 8)
                   Nothing => return Nothing
  | False = -- do --putStrLn $ "Pos: " ++ (show pos)
               --putStrLn $ "p_len: " ++ (show p_len)
               return Nothing

unmarshalCString : ActivePacket -> IO (Maybe (String, Length))
unmarshalCString (ActivePacketRes pckt pos p_len) = do
  res <- unmarshalCString' (ActivePacketRes pckt pos p_len) 0
  case res of
       Just (chrs, len) => return $ Just (pack chrs, len)
       Nothing => return Nothing

unmarshalLString' : ActivePacket -> Nat -> IO (List Char)
unmarshalLString' ap Z = return []
unmarshalLString' (ActivePacketRes pckt pos p_len) (S k) = do
  next_byte <- foreignGetBits pckt pos (pos + 7)
  let char = chr next_byte
  rest <- unmarshalLString' (ActivePacketRes pckt (pos + 8) p_len) k
  return $ (char :: rest)

-- We've already bounds-checked the LString against the packet length,
-- meaning it's safe to just return a string.
unmarshalLString : ActivePacket -> Nat -> IO String
unmarshalLString ap n = map pack (unmarshalLString' ap n)

unmarshalBits : ActivePacket -> (c : Chunk) -> IO (Maybe (chunkTy c, Length))
unmarshalBits (ActivePacketRes pckt pos p_len) (Bit width p) with ((pos + (natToInt width) - 1) <= p_len)
  | True = do
    res <- foreignGetBits pckt pos (pos + (natToInt width) - 1)
    --putStrLn $ "Read: " ++ show res
    return $ Just $ (BInt res (assert_total $ believe_me Oh), (natToInt width)) -- Have to trust it, as it's from C
  | False = return Nothing
unmarshalBits _ _ = return Nothing

unmarshalBool : ActivePacket -> IO (Maybe (Bool, Length))
unmarshalBool (ActivePacketRes pckt pos p_len) with (pos <= p_len)
  | True = do
      res <- foreignGetBits pckt pos pos
      --putStrLn $ "Read: " ++ show (res == 1)
      return $ Just (res == 1, 1)
  | False = return Nothing

unmarshalProp : (p : Proposition) -> Maybe (propTy p)
unmarshalProp (P_EQ x y) =
  case decEq x y of
    (Yes p) => Just p
    (No p) =>  Nothing
unmarshalProp (P_BOOL b) =
  case choose b of
    Left p_yes => Just p_yes
    Right _ => Nothing
-- Nothing -- That's just SO not b
unmarshalProp (P_AND prop1 prop2) = do
  p1 <- unmarshalProp prop1
  p2 <- unmarshalProp prop2
  Just (MkBoth p1 p2)
unmarshalProp (P_OR p1 p2) =
  maybe (maybe Nothing
                    (\p2' => Just (Right p2')) (unmarshalProp p2))
                    (\p1' => Just (Left p1')) (unmarshalProp p1)
unmarshalProp (P_LT x y) = Nothing -- TODO

unmarshalChunk : ActivePacket -> (c : Chunk) -> IO (Maybe (chunkTy c, Length))
unmarshalChunk ap (Bit width p) = unmarshalBits ap (Bit width p)
unmarshalChunk ap CBool = unmarshalBool ap
unmarshalChunk ap CString = unmarshalCString ap
unmarshalChunk (ActivePacketRes pckt pos p_len) (LString n) =
  -- Do bounds checking now, if it passes then we're golden later on
  if pos + (8 * (natToInt n)) <= p_len then do
    res <- unmarshalLString (ActivePacketRes pckt pos p_len) n
    return $ Just (res, (8 * (natToInt n)))
  else do
 --   putStrLn "Check failed in unmarshal LString"
    return Nothing
unmarshalChunk (ActivePacketRes pckt pos p_len) (Decodable n t decode_fn _) = do
  let len = natToInt n
  let end_pos = (pos + len)
  if (end_pos <= p_len) then do
    dat <- foreignGetBits pckt pos (end_pos - 1)
    case (decode_fn (BInt dat (believe_me Oh))) of -- Decode using supplied fn
      Just decoded_val => return $ Just (decoded_val, len)
      Nothing => return Nothing
  else return Nothing -- Out of bounds
unmarshalChunk _ (Prop p) =
  case unmarshalProp p of
       Just p' => return $ Just (p', 0)
       Nothing => return Nothing

-- There's an ambiguity problem here, but it's not massively problematic
-- according to Edwin (in reality, RFCs will define markers at the end of
-- lists).
unmarshalList : ActivePacket -> (pl : PacketLang) -> (List (mkTy pl), Length)
unmarshalList (ActivePacketRes pckt pos p_len) pl =
    case (unmarshal' (ActivePacketRes pckt pos p_len) pl) of
      Just (item, len) =>
        let (rest, rest_len) = unmarshalList (ActivePacketRes pckt (pos + len) p_len) pl in
--        let (rest, rest_len) = (fst xs_tup, snd xs_tup) in
          (item :: rest, len + rest_len)
      Nothing => ([], 0) -- Finished parsing list

unmarshalVect : ActivePacket ->
                (pl : PacketLang) ->
                (len : Nat) ->
                Maybe ((Vect len (mkTy pl)), Length)
unmarshalVect _ _ Z = Just ([], 0)
unmarshalVect (ActivePacketRes pckt pos p_len) pl (S k) = do
  (item, len) <- unmarshal' (ActivePacketRes pckt pos p_len) pl
  (rest, rest_len) <- unmarshalVect (ActivePacketRes pckt (pos + len) p_len) pl k
  return (item :: rest, len + rest_len)

-- unmarshal' : ActivePacket -> (pl : PacketLang) -> Maybe (mkTy pl, Length)
unmarshal' ap (CHUNK c) = unsafePerformIO $ unmarshalChunk ap c
unmarshal' ap (IF False yes no) = unmarshal' ap no
unmarshal' ap (IF True yes no) = unmarshal' ap yes
-- Attempt x, if correct then return x.
-- If not, try y. If correct, return y.
-- If neither correct, return Nothing.
unmarshal' ap (x // y) = do
  let x_res = unmarshal' ap x
  --let y_res =
  case x_res of
       Just (pckt, len) => Just (Left pckt, len)
       Nothing => case (unmarshal' ap y) of
                    Just (pckt, len) => Just (Right pckt, len)
                    Nothing => Nothing
unmarshal' ap (LIST pl) = Just (unmarshalList ap pl)
unmarshal' ap (LISTN n pl) = unmarshalVect ap pl n
unmarshal' ap NULL = Just ((), 0)
unmarshal' (ActivePacketRes pckt pos p_len) (c >>= k) = do
  (res, res_len) <- unmarshal' (ActivePacketRes pckt pos p_len) c
  (res2, res2_len) <- unmarshal' (ActivePacketRes pckt (pos + res_len) p_len) (k res)
  return ((res ** res2), res_len + res2_len)

{- Publicly-Facing Functions... -}
-- | Given a packet language and a packet, creates a BufPtr that
-- | may be sent over the network by a UDP or TCP socket
public
marshal : (pl : PacketLang) -> (mkTy pl) -> IO (BufPtr, Length)
marshal pl dat = do
  let pckt_len = bitLength pl dat
  pckt <- foreignCreatePacket pckt_len
  len <- marshal' (ActivePacketRes pckt 0 pckt_len) pl dat
  -- putStrLn "Marshalling: "
--  dumpPacket pckt 1024
  let nat_len' = (intToNat len) `div` 8
  let len' = natToInt nat_len'
  return (pckt, len' + 1)

-- | Given a packet language and a BufPtr, unmarshals the packet
public
unmarshal : (pl : PacketLang) ->
            BufPtr ->
            Length ->
            IO (Maybe (mkTy pl, ByteLength))
unmarshal pl pckt len = do
  --putStrLn "Unmarshalling: "
--  dumpPacket pckt 1024
  return $ (unmarshal' (ActivePacketRes pckt 0 (len * 8)) pl)

-- | Destroys a BufPtr
public
freePacket : BufPtr -> IO ()
freePacket (BPtr pckt) = foreign FFI_C "freePacket" (Ptr -> IO Unit) pckt


text:
module Utils.Matrix

import Utils.Conjugate

%default total
%access public export

Vector : Type -> Type
Vector = List
%name Vector xv, yv, zv

Matrix : Type -> Type
Matrix = Vector . Vector
%name Matrix xm, ym, zm

apply : Num a => Matrix a -> Vector a -> Vector a
apply xm xv = map (\row => sum (zipWith (*) row xv)) xm

transpose : Matrix a -> Matrix a
transpose [] = []
transpose (x :: xs) = zipWith (::) x xs

mmap : (a -> b) -> Matrix a -> Matrix b
mmap f = map (map f)

implementation Conjugate space coSpace => Conjugate (Matrix space) (Matrix coSpace) where
  conjug = Utils.Matrix.transpose . mmap conjug

max_stars_repo_name: GrandArchTemplar/QuantumProgramming

max_issues_repo_name: GrandArchTemplar/QuantumProgramming

max_forks_repo_name: GrandArchTemplar/QuantumProgramming


text:
||| Algebra.Magma: A representation of magmas.
|||
||| A magma is more-or-less the simplest non-trivial example of a algebraic
||| structure. It is simply a set together with a lawless binary operation over
||| it. More formally, it is *any* pair
||| \\(\mathscr{M} = (M:\mathscr{V}, \* : M^2 \to M)\\). It doesn't matter what
||| the function \\(\*\\) is. It can have any properties whatsoever; the only
||| reuirement is that it be a function of the specified type. That is, it must
||| be a total co-injective relation with domain \\(M^2\\) and codomain \\(M\\),
||| where by \"co-injective\" I mean that for every input, there is no more than
||| one output. Together with totality, which states that every input has at
||| least one output, this means that a function is a relation where every input
||| has exactly one output.
|||
||| Magmas aren't especially interesting in and of themselves. Because there are
||| no magma axioms, just a type, there isn't much that can be said about magmas
||| in general. However, they give a useful way to talk about other algebraic
||| structures. A group, for example, is a magma satisfying certain laws. In
||| other words, talking in terms of magmas and related lawless algebraic
||| structures just gives us a more convenient way to talk about the signature
||| of the more interesting ones. (Of course, all of this leads naturally to
||| groups, semigroups, monoids, etc. being extensions of the `Magma`
||| record.)
|||
||| That's not to say there's nothing interesting about magmas. There are
||| interesting combinatorial questions arising from freely generated magmas.
||| That is, consider a magma generated by three elements, \\(a, b, c\\). By
||| \"freely generated\", we mean that there are no equalities except those
||| directly entailed by the axioms; since there aren't any axioms, there aren't
||| any (non-reflexive) equalities! E.g., in a freely generated magma, we know
||| that \\((x\*y)\*z \neq x\*(y\*z)\\) for every \\(x, y, z\\). If they were
||| equal, it would still be a magma, but not a freely generated one. Now, for
||| the free magma with 3 generating elements, how many elements are there with
||| exactly \\(k\\) applications of the operation \\(\*\\)? Or more generally,
||| what if there are \\(n\\) generating elements? If you like combinatorics,
||| you might enjoy working these and related questions out\-\-\-and, as usual,
||| there's a connection to the Catalan numbers.
module Algebra.Magma

%default total

infix 7 |*|

||| The record representing magmas. Note that there are no proofs to be
||| automatically filled in; magmas don't have any extra properties beyond their
||| signature.
public export
record Magma where
  constructor MkMagma
  Set' : Type
  op'  : Set' -> Set' -> Set'

public export
Set : {magma : Magma} -> Type
Set {magma} = Set' magma

public export
(|*|) : {magma : Magma} -> Set {magma} -> Set {magma} -> Set {magma}
(|*|) {magma} = op' magma

{-
public export
AddMagma : (Num ty) => Magma
AddMagma {ty} = MkMagma ty (+)

public export
MultMagma : (Num ty) => Magma
MultMagma {ty} = MkMagma ty (*)

-- -}

-- data Magma : (Set : Type) -> (Set -> Set -> Set) -> Type where
--   Magmoid :
-- {-

max_stars_repo_name: greatBigDot/algebra

max_issues_repo_name: greatBigDot/algebra

max_forks_repo_name: greatBigDot/algebra


text:
module Data.HashSet

import Data.Vector

%default total

public export
HashCode : Type
HashCode = Bits32

public export
interface (Eq a) => Hash a where
  hash : a -> HashCode

public export
Hash HashCode where
  hash = id

public export
Hash Int where
  hash = prim__zextInt_B32

public export
implementation (Hash a, Hash b) => Hash (a, b) where
  hash (x, y) = prim__xorB32 (997 * hash x) (991 * hash y)

Bitmap : Type
Bitmap = Bits32

Index : Type
Index = Nat

Cast Bits32 Nat where
  cast = cast . prim__zextB32_Int

mutual
  data Node a
    = Empty
    | Key HashCode a
    | HashCollision HashCode (Vector a)
    | SubTrie Bitmap (NodeList a)

  NodeList : Type -> Type
  NodeList a = Vector (Node a)

export
record HashSet a where
  constructor MkHashSet
  size : Nat
  root : NodeList a

Show a => Show (Node a) where
  show Empty = "E"
  show (Key h a) = "(K " ++ show a ++ ")"
  show (SubTrie bm l) = "(S " ++ show bm ++ " " ++ assert_total (show l) ++ ")"
  show _ = "*"

export
Show a => Show (HashSet a) where
  show (MkHashSet s r) = "HashSet " ++ show s ++ " " ++ show r

infixl 7 &
(&) : Bits32 -> Bits32 -> Bits32
(&) = prim__andB32

infixl 7 >>
(>>) : Bits32 -> Bits32 -> Bits32
(>>) = prim__lshrB32

infixl 7 <<
(<<) : Bits32 -> Bits32 -> Bits32
(<<) = prim__shlB32

(-) : Bits32 -> Bits32 -> Bits32
(-) x y = prim__zextInt_B32 (prim__zextB32_Int x - prim__zextB32_Int y)

shiftMask : Bits32 -> Bits32 -> Bits32 -> Bits32
shiftMask bits shift mask = (bits >> shift) & mask

popcnt : Bits32 -> Bits32
popcnt x =
  let x = x - shiftMask x 1 0x55555555
      x = (x & 0x33333333) + shiftMask x 2 0x33333333
      x = (x + (x >> 4)) & 0x0F0F0F0F
      x = x + (x >> 8)
      x = x + (x >> 16)
  in x & 0x0000003F

next5Bits : Bits32 -> HashCode -> HashCode
next5Bits level hashCode = shiftMask hashCode (5 * level) 0x1F

bitAt : Bits32 -> Bits32 -> Bool
bitAt pos bits = 1 == shiftMask bits pos 1

setBit : Bits32 -> Bits32 -> Bits32
setBit bitPos bits = prim__orB32 bits (1 << bitPos)

nodeIndex : Bits32 -> Bits32 -> Index
nodeIndex bitPos bitmap = cast (popcnt (bitmap & ((1 << bitPos) - 1)))

nodeAt : Index -> NodeList a -> Node a
nodeAt idx nodes = nodes !! idx

insertNode : Index -> NodeList a -> Node a -> NodeList a
insertNode idx nodes n = unsafeInsertAt idx n nodes

replaceNode : Index -> NodeList a -> Node a -> NodeList a
replaceNode idx nodes n = unsafeReplaceAt idx n nodes

{-
3.1 Search for a key Map Hash Array Mapped Trie (HAMT)

Compute a full 32 bit hash for the key, take the most significant t bits and use them as an integer to index into the root hash table. One of three cases may be encountered. First, the entry is empty indicating that the key is not in the hash tree. Second the entry is a Key/Value pair and the key either matches the desired key indicating success or not, indicating failure. Third, the entry has a 32 bit map sub-hash table and a sub-trie pointer, Base, that points to an ordered list of the non-empty sub-hash table entries.

Take the next 5 bits of the hash and use them as an integer to index into the bit Map. If this bit is a zero the hash table entry is empty indicating failure, otherwise, it’s a one, so count the one bits below it using CTPOP and use the result as the index into the non-empty entry list at Base. This process is repeated taking five more bits of the hash each time until a terminating key/value pair is found or the search fails. Typically, only a few iterations are required and it is important to note that the key is only compared once and that is with the terminating node key.
-}
export
member : (Hash a) => a -> HashSet a -> Bool
member key (MkHashSet _ root) =
  let rootPos = cast (next5Bits 0 hashCode)
  in memberOf root rootPos 1
  where
    hashCode : HashCode
    hashCode = hash key
    memberOf : NodeList a -> Index -> Bits32 -> Bool
    memberOf nodes index nextLevel =
      case nodeAt index nodes of
        Empty => False
        Key existingHashCode existingKey =>
          existingHashCode == hashCode && existingKey == key
        HashCollision existingHashCode keys =>
          existingHashCode == hashCode && elem key keys
        SubTrie bitmap nodes =>
          let
            bitPos = next5Bits nextLevel hashCode
            bitVal = bitAt bitPos bitmap
          in
            if bitVal
              then assert_total (memberOf nodes (nodeIndex bitPos bitmap) (nextLevel + 1))
              else False

{-
3.2 Insertion
The initial steps required to add a new key to the hash tree are identical to the search. The search algorithm is followed until one of two failure modes is encoun- tered.

Either an empty position is discovered in the hash table or a sub-hash table is found. In this case, if this is in the root hash table, the new key/value pair is simply substituted for the empty position. However, if in a sub-hash table then a new bit must be added to the bit map and the sub-hash table increased by one in size. A new sub-hash table must be allocated, the existing sub-table copied to it, the new key/value entry added in sub-hash sorted order and the old hash table made free.

Or the key will collide with an existing one. In which case the existing key must be replaced with a sub-hash table and the next 5 bit hash of the existing key computed. If there is still a collision then this process is repeated until no collision occurs. The existing key is then inserted in the new sub-hash table and the new key added. Each time 5 more bits of the hash are used the probability of a collision reduces by a factor of 1 . Occasionally an entire 32 bit hash may be consumed and 32 a new one must be computed to differentiate the two keys.
-}
insert' : (Hash a) => HashCode -> a -> HashSet a -> HashSet a
insert' hashCode key set@(MkHashSet size root) =
  case nodeAt rootPos root of
     Empty => insertRootNode (Key hashCode key)
     SubTrie bitmap nodes =>
       maybe set insertRootNode (insertIntoSubTrie bitmap nodes 1)
     node@(Key existingHashCode existingKey) =>
       if existingHashCode == hashCode
         then
           if existingKey == key
             then set
             else insertRootNode (collision existingKey)
         else
           maybe set insertRootNode (spawnSubTrie node existingHashCode 1)
     node@(HashCollision existingHashCode keys) =>
       if existingHashCode == hashCode
         then
           if elem key keys
             then set
             else insertRootNode (HashCollision hashCode (key :: keys))
         else
           maybe set insertRootNode (spawnSubTrie node existingHashCode 1)
  where
    rootPos : Index
    rootPos = cast (next5Bits 0 hashCode)
    insertRootNode : Node a -> HashSet a
    insertRootNode = MkHashSet (S size) . replaceNode rootPos root
    collision : a -> Node a
    collision existingKey = HashCollision hashCode (key :: singleton existingKey)
    mutual
      insertIntoSubTrie : Bitmap -> NodeList a -> Bits32 -> Maybe (Node a)
      insertIntoSubTrie bitmap nodes level =
        let
          bitPos = next5Bits level hashCode
          bitVal = bitAt bitPos bitmap
          nodePos = nodeIndex bitPos bitmap
        in
          if bitVal
            then SubTrie bitmap . replaceNode nodePos nodes <$> insertInto (nodeAt nodePos nodes) level
            else Just (SubTrie (setBit bitPos bitmap) (insertNode nodePos nodes (Key hashCode key)))

      insertInto : Node a -> Bits32 -> Maybe (Node a)
      insertInto (SubTrie bitmap nodes) level =
        assert_total (insertIntoSubTrie bitmap nodes (level + 1))
      insertInto node@(Key existingHashCode existingKey) level =
        if existingHashCode == hashCode
          then
            if existingKey == key
              then Nothing
              else Just (collision existingKey)
          else
            assert_total (spawnSubTrie node existingHashCode (level + 1))
      insertInto node@(HashCollision existingHashCode keys) level =
        if existingHashCode == hashCode
          then
            if elem key keys
              then Nothing
              else Just (HashCollision hashCode (key :: keys))
          else
            assert_total (spawnSubTrie node existingHashCode (level + 1))
      insertInto Empty _ = assert_unreachable

      spawnSubTrie : Node a -> HashCode -> Bits32 -> Maybe (Node a)
      spawnSubTrie node existingHashCode level =
        let bitPos = next5Bits level existingHashCode
            bitmap = setBit bitPos 0
        in insertIntoSubTrie bitmap (singleton node) level

export
insert : (Hash a) => a -> HashSet a -> HashSet a
insert key set = insert' (hash key) key set

export
empty : HashSet a
empty = MkHashSet 0 (replicate 32 Empty)

export
length : HashSet a -> Nat
length (MkHashSet size _) = size

fold : (acc -> elem -> acc) -> acc -> HashSet elem -> acc
fold f init (MkHashSet _ nodes) = foldNodes init nodes
  where
   mutual
    foldNodes : acc -> NodeList elem -> acc
    foldNodes acc nodes = foldl foldNode acc nodes
    foldNode : acc -> Node elem -> acc
    foldNode acc Empty = acc
    foldNode acc (Key _ k) = f acc k
    foldNode acc (HashCollision _ keys) = foldl f acc keys
    foldNode acc (SubTrie _ nodes) = assert_total (foldNodes acc nodes)

export
Foldable HashSet where
  foldl = fold
  foldr = fold . flip

export
filter : (Eq elem, Hash elem) => (elem -> Bool) -> HashSet elem -> HashSet elem
filter f (MkHashSet _ nodes) = foldNodes empty nodes
  where
   mutual
    foldNodes : HashSet elem -> NodeList elem -> HashSet elem
    foldNodes acc nodes = foldl foldNode acc nodes
    foldNode : HashSet elem -> Node elem -> HashSet elem
    foldNode acc Empty = acc
    foldNode acc (Key hashCode k) = insertWithHashCode hashCode acc k
    foldNode acc (HashCollision hashCode keys) = foldl (insertWithHashCode hashCode) acc keys
    foldNode acc (SubTrie _ nodes) = assert_total (foldNodes acc nodes)
    insertWithHashCode : HashCode -> HashSet elem -> elem -> HashSet elem
    insertWithHashCode hc acc e = if f e then insert' hc e acc else acc

export
into : (Hash a, Foldable f) => HashSet a -> f a -> HashSet a
into = foldl (flip insert)

export
fromList : (Hash a) => List a -> HashSet a
fromList = foldl (flip insert) empty

export
foldM : Monad m => (acc -> elem -> m acc) -> acc -> HashSet elem -> m acc
foldM f acc (MkHashSet _ nodes) = foldNodes f acc nodes
  where
   mutual
    foldNodes : (Monad m) => (a -> elem -> m a) -> a -> NodeList elem -> m a
    foldNodes f acc nodes = loop (length nodes) acc
      where
        loop Z     acc = pure acc
        loop (S k) acc = foldNode f acc (nodes !! k) >>= loop k
    foldNode : (Monad m) => (a -> elem -> m a) -> a -> Node elem -> m a
    foldNode f acc Empty = pure acc
    foldNode f acc (Key _ k) = f acc k
    foldNode f acc (HashCollision _ keys) = foldKeys f acc keys
    foldNode f acc (SubTrie _ nodes) = assert_total (foldNodes f acc nodes)
    foldKeys : (Monad m) => (a -> elem -> m a) -> a -> Vector elem -> m a
    foldKeys f acc keys = loop (length keys) acc
      where
        loop Z     acc = pure acc
        loop (S k) acc = f acc (keys !! k) >>= loop k

max_stars_repo_name: alaendle/idris-cil

max_issues_repo_name: alaendle/idris-cil

max_forks_repo_name: alaendle/idris-cil


text:
ap : (a -> b -> c) -> (a -> b) -> a -> c
ap f g x = f x (g x)

-- the one with Lazy Bool was making type checking tricky
||| A strict version of the && operator
and : Bool -> Bool -> Bool
and False _ = False
and True x = x

isPalindrome : String -> Bool
isPalindrome = ap (==) reverse

isPalindromeIgnoringCase : String -> Bool
isPalindromeIgnoringCase = (ap (==) reverse) . toLower

-- Maybe I should just give up with this point free thing
-- but it's way too fun to stop
isBigPalindrome : String -> Bool
isBigPalindrome =
  ap (and . ((> 10) . length)) ((ap (==) reverse) . toLower)

-- Ok I give up
isPalindromeOfSize : Nat -> String -> Bool
isPalindromeOfSize n str =
  str == (reverse str) && length str > n

counts : String -> (Nat, Nat)
counts str = ((length . words) str, length str)

topTen : Ord a => List a -> List a
topTen = List.take 10 . reverse . sort

overLen : Nat -> List String -> Nat
overLen n = length . filter ((> n) . length)

main : IO ()
main = repl "\n>> " (show . isBigPalindrome)


text:
module Miscellany

-- auto implicit arguments

-- this is the proof that the passed-in list is non-empty
isCons : List a -> Bool
isCons [] = False
isCons (_ :: _) = True

-- we can use that proof here, explicitly
safehead : (xs : List a)-> (isCons xs = True) -> a
safehead (x :: xs) _ = x

-- we can use the `auto` keyword to search for the proof automatically. Note the braces -
-- we can explicitly supply the proof if we wish to.

bettersafehead : (xs : List a) -> { auto p : isCons xs = True } -> a
bettersafehead (x :: _) = x

-- default implicit arguments

-- note that this case is not representative. The real value of default arguments is in Theorem Proving.

fibonacci : { default 0 lag : Nat } -> { default 1 lead : Nat } -> ( n : Nat ) -> Nat
fibonacci {lag} Z = lag
fibonacci {lag} {lead} (S n) = fibonacci {lag = lead} {lead = lag + lead} n

max_stars_repo_name: timmyjose-study/idris-from-the-docs

max_issues_repo_name: timmyjose-study/idris-from-the-docs

max_forks_repo_name: timmyjose-study/idris-from-the-docs


text:
module Keybindings

import Effects
import Effect.SDL
import Effect.StdIO
import Effect.State
import Data.Fin

import Chip8
import Cpu
import Keypad
import Utilities

%default total

updateKeydown : (pressedKey : Fin 16) -> { [Chip8 ::: STATE Chip8] } Eff Bool
updateKeydown pressedKey =
  do
    chip <- Chip8 :- get
    case State chip of
      Active =>
        let keypad = setKeyPress (Keys chip) pressedKey in
        do
          Chip8 :- put (record { Keys = keypad } chip)
          pure True
      WaitingForKey r =>
        let keypad = setKeyPress (Keys chip) pressedKey in
        let cpu = setRegister (Computer chip) r $ cast pressedKey in
        do
          Chip8 :- put (record { State = Active, Keys = keypad, Computer = incrementPC cpu } chip)
          pure True
      Halted =>
        pure False

updateKeyup : (releasedKey : Fin 16) -> { [Chip8 ::: STATE Chip8] } Eff Bool
updateKeyup releasedKey =
  do
    chip <- Chip8 :- get
    case State chip of
      Active =>
        let keypad = clearKeyPress (Keys chip) releasedKey in
        do
          Chip8 :- put (record { Keys = keypad } chip)
          pure True
      WaitingForKey _ =>
        pure True
      Halted =>
        pure False

export
processKeys : Maybe Event -> { [Chip8 ::: STATE Chip8, STDIO] } Eff Bool
processKeys (Just (KeyDown $ KeyAny '1')) = updateKeydown 0x1
processKeys (Just (KeyUp   $ KeyAny '1')) = updateKeyup   0x1
processKeys (Just (KeyDown $ KeyAny '2')) = updateKeydown 0x2
processKeys (Just (KeyUp   $ KeyAny '2')) = updateKeyup   0x2
processKeys (Just (KeyDown $ KeyAny '3')) = updateKeydown 0x3
processKeys (Just (KeyUp   $ KeyAny '3')) = updateKeyup   0x3
processKeys (Just (KeyDown $ KeyAny '4')) = updateKeydown 0xc
processKeys (Just (KeyUp   $ KeyAny '4')) = updateKeyup   0xc
processKeys (Just (KeyDown $ KeyAny 'q')) = updateKeydown 0x4
processKeys (Just (KeyUp   $ KeyAny 'q')) = updateKeyup   0x4
processKeys (Just (KeyDown $ KeyAny 'w')) = updateKeydown 0x5
processKeys (Just (KeyUp   $ KeyAny 'w')) = updateKeyup   0x5
processKeys (Just (KeyDown $ KeyAny 'e')) = updateKeydown 0x6
processKeys (Just (KeyUp   $ KeyAny 'e')) = updateKeyup   0x6
processKeys (Just (KeyDown $ KeyAny 'r')) = updateKeydown 0xd
processKeys (Just (KeyUp   $ KeyAny 'r')) = updateKeyup   0xd
processKeys (Just (KeyDown $ KeyAny 'a')) = updateKeydown 0x7
processKeys (Just (KeyUp   $ KeyAny 'a')) = updateKeyup   0x7
processKeys (Just (KeyDown $ KeyAny 's')) = updateKeydown 0x8
processKeys (Just (KeyUp   $ KeyAny 's')) = updateKeyup   0x8
processKeys (Just (KeyDown $ KeyAny 'd')) = updateKeydown 0x9
processKeys (Just (KeyUp   $ KeyAny 'd')) = updateKeyup   0x9
processKeys (Just (KeyDown $ KeyAny 'f')) = updateKeydown 0xe
processKeys (Just (KeyUp   $ KeyAny 'f')) = updateKeyup   0xe
processKeys (Just (KeyDown $ KeyAny 'z')) = updateKeydown 0xa
processKeys (Just (KeyUp   $ KeyAny 'z')) = updateKeyup   0xa
processKeys (Just (KeyDown $ KeyAny 'x')) = updateKeydown 0x0
processKeys (Just (KeyUp   $ KeyAny 'x')) = updateKeyup   0x0
processKeys (Just (KeyDown $ KeyAny 'c')) = updateKeydown 0xb
processKeys (Just (KeyUp   $ KeyAny 'c')) = updateKeyup   0xb
processKeys (Just (KeyDown $ KeyAny 'v')) = updateKeydown 0xf
processKeys (Just (KeyUp   $ KeyAny 'v')) = updateKeyup   0xf
processKeys (Just (KeyDown KeyEsc)) = pure False
processKeys (Just AppQuit) =
  do
    chip <- Chip8 :- get
    case isHalted chip of
      Just error => do
        putStrLn $ "Chip8 halted. Reason: " ++ error
        pure False
      _ =>
        pure False
processKeys _ = pure True


text:
import System
import Data.Maybe

f : String -> IO String
f str = do
  putStrLn str
  pure $ str ++ "!!"

main : IO ()
main = do
    prop <- getEnv "foo"
    when (not $ isJust prop) $
      let info = map (\s => show $ length s) !(traverse f ["x", "y", "z"]) in
          putStrLn $ "result " ++ show info


text:
-- ---------------------------------------------------------------- [ Core.idr ]
-- Module      : Lightyear.Core
-- Description : Central Definitions and Instances
--
-- This code is distributed under the BSD 2-clause license.
-- See the file LICENSE in the root directory for its full text.
-- --------------------------------------------------------------------- [ EOH ]
module Lightyear.Core

import Data.Fin
import Control.Monad.Trans
import Control.Monad.State

%access export
%default total

||| Parse results
public export
data Result str a =
  ||| Sucess, returning the remaining string and the parser result
  Success str a |
  ||| Failure, returning a stack trace of errors based on `<?>`
  Failure (List (str, String)) -- a stacktrace of errors based on <?> and friends

implementation Functor (Result str) where
  map f (Success s x ) = Success s (f x)
  map f (Failure es) = Failure es

record ParserT str (m : Type -> Type) a where
  constructor PT
  runParserT :
    (r : Type) ->
    (a -> str -> m r) -> -- uncommitted success
    (a -> str -> m r) -> -- committed success
    (List (str, String) -> m r) -> -- uncommitted error
    (List (str, String) -> m r) -> -- committed error
    str ->
    m r

||| Run a parser monad on some input
execParserT : Monad m => ParserT str m a
                      -> (input : str)
                      -> m (Result str a)
execParserT {str} {m} {a} (PT p) input = p (Result str a) success success failure failure input
  where success x i = pure $ Success i x
        failure = pure . Failure

implementation Monad m => Functor (ParserT str m) where
  map {a} {b} f (PT p) = PT $ \r, us, cs => p r (us . f) (cs . f)

implementation Monad m => Applicative (ParserT str m) where
  pure x = PT (\r, us, cs, ue, ce => us x)

  (<*>) (PT f) (PT g) = PT $ \r, us, cs, ue, ce =>
    f r (\f' => g r (us . f') (cs . f') ue ce)
        (\f' => g r (cs . f') (cs . f') ce ce)
        ue ce

infixl 2 <*>|
||| A variant of <$>, lazy in its second argument, which must NOT be
||| pattern-matched right away because we want to keep it lazy in case
||| it's not used.
(<*>|) : Monad m => ParserT str m (a -> b)
                 -> Lazy (ParserT str m a)
                 -> ParserT str m b
(<*>|) (PT f) x = PT $ \r, us, cs, ue, ce =>
    f r (\f' => let PT g = x in g r (us . f') (cs . f') ue ce)
        (\f' => let PT g = x in g r (cs . f') (cs . f') ce ce)
        ue ce

implementation Monad m => Monad (ParserT str m) where
  (>>=) (PT x) f = PT $ \r, us, cs, ue, ce =>
    x r (\x' => let PT y = f x' in y r us cs ue ce)
        (\x' => let PT y = f x' in y r cs cs ce ce)
        ue ce

implementation Monad m => MonadTrans (ParserT str) where
  lift x = PT $ \r, us, cs, ue, ce, s => (x >>= flip us s)

-- HACK
-- for some reason the MonadState instance does not work with plain lift :(
private
lift' : Monad m => m a -> ParserT str m a
lift' = lift

implementation MonadState s m => MonadState s (ParserT str m) where
  get = lift' get
  put = lift' . put

||| Fail with some error message
fail : String -> ParserT str m a
fail msg = PT $ \r, us, cs, ue, ce, i => ue [(i, msg)]

implementation Monad m => Alternative (ParserT str m) where
  empty = fail "non-empty alternative"

  (<|>) (PT x) (PT y) = PT $ \r, us, cs, ue, ce, i =>
    x r us cs (\err => y r us cs (ue . (err ++))
                                 (ce . (err ++)) i) ce i

infixl 3 <|>|

||| A variant of <|>, lazy in its second argument, which must NOT be
||| pattern-matched right away because we want to keep it lazy in case
||| it's not used.
(<|>|) : Monad m => ParserT str m a
                 -> Lazy (ParserT str m a)
                 -> ParserT str m a
(<|>|) (PT x) y = PT $ \r, us, cs, ue, ce, i =>
  x r us cs (\err => let PT y' = y in y' r us cs (ue . (err ++))
                                                 (ce . (err ++)) i) ce i

infixl 0 <?>
||| Associate an error with parse failure
(<?>) : Monad m => ParserT str m a -> String -> ParserT str m a
(PT f) <?> msg = PT $ \r, us, cs, ue, ce, i =>
  f r us cs (ue . ((i, msg) ::)) (ce . ((i, msg) ::)) i

||| Commit to a parse alternative and prevent backtracking
commitTo : Monad m => ParserT str m a -> ParserT str m a
commitTo (PT f) = PT $ \r, us, cs, ue, ce => f r cs cs ce ce

-- There is no reason that we mark "str" as the determining type
-- other than to aid typeinterface resolution.
--
-- I feel that having this restriction (which is probably okay
-- given that the only streams so far are String and Text anyway)
-- is more acceptable than failing surprisingly
-- any time the unsuspecting user calls "satisfy" without {tok=Char}
-- in an odd context.
--
-- We make "str" the determining type because it's usually fixed
-- by the parser monad you're working in, which helps resolution.
interface Stream tok str | str where
  uncons : str -> Maybe (tok, str)

||| Matches a single element that satisfies some condition, accepting
||| a transformation of successes.
satisfyMaybe : (Monad m, Stream tok str)
                        => (tok -> Maybe out)
                        -> ParserT str m out
satisfyMaybe {tok=tok} {str=str} f =
  PT $ \r, us, cs, ue, ce, i =>
    case uncons {tok=tok} {str=str} i of
      Nothing      => ue [(i, "a token, not EOF")]
      Just (t, i') => case f t of
        Nothing  => ue [(i, "a different token")]
        Just res => us res i'

||| Matches a single element that satisfies some condition.
satisfy : (Monad m, Stream tok str)
                   => (tok -> Bool)
                   -> ParserT str m tok
satisfy p = satisfyMaybe (\t => if p t then Just t else Nothing)

||| Succeeds if and only if the argument parser fails.
|||
||| In Parsec, this combinator is called `notFollowedBy`.
requireFailure : ParserT str m tok -> ParserT str m ()
requireFailure (PT f) = PT $ \r, us, cs, ue, ce, i =>
                               f r
                                 (\t, s => ue [(i, "argument parser to fail")])
                                 (\t, s => ce [(i, "argument parser to fail")])
                                 (\errs => us () i)
                                 (\errs => cs () i)
                                 i
-- --------------------------------------------------------------------- [ EOF ]

max_stars_repo_name: david-christiansen/lightyear

max_issues_repo_name: david-christiansen/lightyear

max_forks_repo_name: david-christiansen/lightyear


text:
module ElemCount

import Data.Vect
import Sortings

%default total

count : Eq a => a -> Vect n a -> Fin (S n)
count _ Nil = 0
count x (y :: xs) = (if x == y then FS else weaken) $ count x xs

data ElemCount : Fin (S n) -> a -> Vect n a -> Type where
  NoElem   :                                    ElemCount FZ         x []
  IncHere  : ElemCount c x xs                -> ElemCount (FS c)     x (x :: xs)
  IncThere : ElemCount c x xs -> Not (x = y) -> ElemCount (weaken c) x (y :: xs)

  -- A variant with non-structural equality
  --IncThere : Eq a => {x, y : a} -> ElemCount c x xs -> Not (So (x == y)) -> ElemCount (weaken c) x (y :: xs)

-- TODO To define permutation through `ElemCount` (probably, the structural one)
-- TODO   and prove equivalence with the structurally defined permutation property.

(+) : Fin (S n) -> Fin (S m) -> Fin (S $ n + m)
(+) {m}     x FZ     = weakenN m x
(+) {n} {m} x (FS y) = rewrite plusSuccRightSucc n m in FS (x + y)

ecConcPresSum : ElemCount ca x as -> ElemCount cb x bs -> ElemCount (ca + cb) x (as ++ bs)
ecConcPresSum = ?ecConcPresSum_impl

||| Proof that permutationproperty preserves elements (i.e. preserves elements count)
permPresElems : Permutation xs ys -> ElemCount n e xs -> ElemCount n e ys
permPresElems EmptyPerm ec = ec
permPresElems {xs=a::as} (InsertPerm ip) (IncHere iec) = ?perm_here
permPresElems (InsertPerm ip) (IncThere iec xy) = ?perm_there

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
module Main

import Data.Vect

vtake : (n:Nat) -> Vect (n+m) a -> Vect n a
vtake Z v = Nil
vtake (S k) (x::xs) = x :: (vtake k xs)

main : IO ()
-- BOOM!
main = putStrLn (show (vtake 5 (1 :: 2 :: 3 :: 4 :: 5 :: Nil)))

max_stars_repo_name: janschultecom/idris-examples

max_issues_repo_name: janschultecom/idris-examples

max_forks_repo_name: janschultecom/idris-examples


text:
module Url

import Control.Monad.Either
import TyTTP.URL

main : IO ()
main = eitherT putStrLn pure $ do
  Left EmptyString <- pure $ Simple.parse ""
    | _ => throwError "empty url is not matched"

  Left EmptyString <- pure $ Simple.parse " \t\r\n"
    | _ => throwError "blank url is not matched"

  Left MissingAuthorityOrPath <- pure $ Simple.parse "http:"
    | _ => throwError "http scheme not recognized"

  Right (MkURL (Just HTTP) Nothing "something" "") <- pure $ Simple.parse "http:something"
    | _ => throwError "http scheme not recognized"

  Right (MkURL (Just HTTPS) Nothing "som" "") <- pure $ Simple.parse " \thttps:som"
    | _ => throwError "https scheme with whitespace not recognized"

  Right (MkURL Nothing (Just "something") "/" "") <- pure $ Simple.parse "//something"
    | _ => throwError "simple authority not recognized"

  Right (MkURL (Just HTTP) (Just "user:passwd@something") "/path/like" "?query=string") <- pure $ Simple.parse "http://user:passwd@something/path/like?query=string"
    | _ => throwError "simple authority not recognized"

  pure ()

max_stars_repo_name: kbertalan/tyttp

max_issues_repo_name: kbertalan/tyttp

max_forks_repo_name: kbertalan/tyttp


text:
module Client.Server

import Inigo.Package.Package
import Extra.String
import SemVar

public export
data Server : Type where
  Dev : Server
  Prod : Server

export
toString : Server -> String
toString server =
  case server of
    Dev =>
      "dev"
    Prod =>
      "prod"

export
getServer : String -> Maybe Server
getServer str =
  case str of
    "dev" =>
      Just Dev
    "prod" =>
      Just Prod
    _ =>
      Nothing

export
host : Server -> String
host Dev = "http://localhost:3000/"
host Prod = "https://inigo.pm/"

export
getArchiveUrl : Package -> String
getArchiveUrl pkg =
  join "/"
    [ "api"
    , "archive"
    , ns pkg
    , package pkg
    , (show . version) pkg
    ]

export
postArchiveUrl : Package -> String
postArchiveUrl pkg =
  join "/"
    [ "api"
    , "archive"
    , ns pkg
    , package pkg
    , (show . version) pkg
    , "post"
    ]

export
postReadmeUrl : Package -> String
postReadmeUrl pkg =
  join "/"
    [ "api"
    , "readme"
    , ns pkg
    , package pkg
    , (show . version) pkg
    , "post"
    ]

export
postPackageUrl : Package -> String
postPackageUrl pkg =
  join "/"
    [ "api"
    , "packages"
    , ns pkg
    , package pkg
    , (show . version) pkg
    , "post"
    ]

export
getPackageUrl : String -> String -> String
getPackageUrl packageNS packageName =
  join "/"
    [ "api"
    , "packages"
    , packageNS
    , packageName
    , "conf"
    ]

export
getPackageVersionUrl : String -> String -> Version -> String
getPackageVersionUrl packageNS packageName version =
  join "/"
    [ "api"
    , "packages"
    , packageNS
    , packageName
    , show version
    , "conf"
    ]

export
getPackageDepTreeUrl : String -> String -> String
getPackageDepTreeUrl packageNS packageName =
  join "/"
    [ "api"
    , "packages"
    , packageNS
    , packageName
    , "deps"
    ]

export
accountPostUrl : String -> String
accountPostUrl ns =
  join "/"
    [ "api"
    , "account"
    , ns
    , "post"
    ]

export
accountLoginUrl : String -> String
accountLoginUrl ns =
  join "/"
    [ "api"
    , "account"
    , ns
    , "login"
    ]

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


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

data EqNat : (num1 : Nat) -> (num2 : Nat) -> Type where
  Same : (num : Nat) -> EqNat num num

sameS : (k:Nat) -> (j:Nat) -> (eq : EqNat k j) -> EqNat (S k) (S j)
sameS j j (Same j) = Same (S j)

checkEqNat : (num1 : Nat) -> (num2 : Nat) -> Maybe (EqNat num1 num2)
checkEqNat Z Z = Just (Same 0)
checkEqNat Z (S k) = Nothing
checkEqNat (S k) Z = Nothing
checkEqNat (S k) (S j) = case checkEqNat k j of
                              Nothing => Nothing
                              (Just eq) => Just (sameS _ _ eq)
checkEqNat2 : (num1 : Nat) -> (num2 : Nat) -> Maybe (num1 = num2)
checkEqNat2 Z Z = Just Refl
checkEqNat2 Z (S k) = Nothing
checkEqNat2 (S k) Z = Nothing
checkEqNat2 (S k) (S j) = case checkEqNat2 k j of
                               Nothing => Nothing
                               Just prf => Just (cong prf)

exactLength : (len : Nat) -> (input : Vect m a) -> Maybe (Vect len a)
exactLength {m} len input = case checkEqNat m len of
                                 Nothing => Nothing
                                 (Just (Same m)) => Just input


text:
module PrintF

----------------------------------------------------------------------
-- Aufwärmen

NNatsFun : Nat -> Type
NNatsFun Z = Nat
NNatsFun (S k) = Nat -> NNatsFun k

adder : (n:Nat) -> Nat -> NNatsFun n
adder Z acc = acc
adder (S k) acc = \n => adder k (acc+n)

----------------------------------------------------------------------
-- PRINTF

-- Beschreibt den Aufbau des Formatstrings:

data Format
     = Num Format
     | Str Format
     | Lit String Format
     | End

-- Typfunktion: Format -> Type

PrintfType : Format -> Type
PrintfType (Num rest) = Integer -> PrintfType rest
PrintfType (Str rest) = String -> PrintfType rest
PrintfType (Lit _ rest) = PrintfType rest
PrintfType End = String

-- Funktion mit Argumenten, die durch `format` gegeben werden
-- und die über `acc` die Ausgabe entsprechend des `format` erstellt

printfToString : (format : Format) -> (acc : String) -> PrintfType format
printfToString (Num rest) acc = \num => printfToString rest (acc ++ show num)
printfToString (Str rest) acc = \str => printfToString rest (acc ++ str)
printfToString (Lit out rest) acc = printfToString rest (acc ++ out)
printfToString End acc = acc

----------------------------------------------------------------------
-- Parsen
parseStringToFormat : String -> Format
parseStringToFormat input = parseChars (unpack input)
  where
    parseChars : List Char -> Format
    parseChars [] = End
    parseChars ('%' :: 'd' :: rest) = Num (parseChars rest)
    parseChars ('%' :: 's' :: rest) = Str (parseChars rest)
    parseChars (c :: rest) =
      case parseChars rest of
        Lit lit rest =>
          Lit (c `strCons` lit) rest
        sonst => Lit (pack [c]) sonst

----------------------------------------------------------------------
-- Endergebnis

printf : (format : String) -> PrintfType (parseStringToFormat format)
printf format = printfToString _ ""


text:
module Sec8_2z_reverse
import Data.Vect

%default total

{-
 proof is needed for typechecker to replace (k + 1) with (S k) - which is by definition (1 + k)
 plusCommutative 1 k states that 1 + k = k + 1 or (S k) = k + 1
 `rewrite LHS=RHS in ax` rewrites ax replacing RHS with LHS (match on RHS and replace it with LHS)
-}
reverseLemma : Vect (k + 1) elem -> Vect (S k) elem
reverseLemma {k} result = rewrite plusCommutative 1 k in result

myReverse : Vect n elem -> Vect n elem
myReverse [] = []
myReverse (x :: xs) = reverseLemma (myReverse xs ++ [x])

{-
excercise 1:
Write plusCommutative in terms of
plusZeroRightNeutral : (left : Nat) -> left + 0 = left
plusSuccRightSucc : (left : Nat) -> (right : Nat) -> S (left + right) = left + S right

Note need to use `rewrite`, simply using
myPlusCommutes (S k) m = plusSuccRightSucc m k
results in error :

...
Specifically:
        Type mismatch between
                plus m (S k)
        and
                plus m (S k)
-}

myPlusCommutes : (n : Nat) -> (m : Nat) -> n + m = m + n
myPlusCommutes Z m = sym (plusZeroRightNeutral m)
-- myPlusCommutes (S k) m = plusSuccRightSucc m k
myPlusCommutes (S k) m = rewrite myPlusCommutes k m in plusSuccRightSucc m k

{-
excercise:
Finish the following replacing
reverse' acc [] = ?reverseLemma_nil acc
  reverseLemma_nil : Vect n1 a -> Vect (plus n1 0) a
reverse' acc (x :: xs) = ?reverseLemma_xs (reverse' (x::acc) xs)
  reverseLemma_xs : Vect (S (plus n1 len)) a -> Vect (plus n1 (S len)) a
-}

reverseLemma_nil : Vect n1 a -> Vect (plus n1 0) a
reverseLemma_nil {n1} xs = rewrite plusZeroRightNeutral n1 in xs

reverseLemma_xs :  Vect ((S n1) + len) a -> Vect (plus n1 (S len)) a
reverseLemma_xs {n1} {len} xs = rewrite sym (plusSuccRightSucc n1 len) in xs

-- note, (S n1) + len is defnitionally the same as S (n1 + len)
reverseLemma_test :  Vect ((S n1) + len) a -> Vect (S (n1 + len)) a
reverseLemma_test = id

myReverse2 : Vect n a -> Vect n a
myReverse2 xs = reverse' [] xs
   where reverse' : Vect n a -> Vect m a -> Vect (n+m) a
         reverse' acc [] = reverseLemma_nil acc
         reverse' acc (x :: xs)
                       = reverseLemma_xs (reverse' (x::acc) xs)

max_stars_repo_name: rpeszek/IdrisTddNotes

max_issues_repo_name: rpeszek/IdrisTddNotes

max_forks_repo_name: rpeszek/IdrisTddNotes


text:
module Field

import Group
import Monoid
import Ring

%access public export

-- For field, proof that multiplicative inverse exists when only non zero elements are considered
total
InvExistsNonZero : (fld : Type) -> ((+) : fld -> fld -> fld) -> ((*) : fld -> fld -> fld) -> (IsGroup fld (+)) -> Type
InvExistsNonZero fld (+) (*) pfgrp = (a : fld) -> (pfid : (IdentityExists fld (*)) ** ((a = fst(fst(snd(pfgrp)))) -> Void) -> (a_inv : fld ** ((a*a_inv) = fst(pfid) , (a_inv*a) = fst(pfid))))

-- multiplication has associativity, identity, but inverse only for non-zero elements
total
IsModGrp : (fld : Type) -> ((+) : fld -> fld -> fld) -> ((*) : fld -> fld -> fld) -> (pfgrp : IsGroup fld (+)) -> Type
IsModGrp fld (+) (*) pfgrp = (Associative fld (*), (IdentityExists fld (*), InvExistsNonZero fld (+) (*) pfgrp))

-- modified abelian property added to the above proof
IsModAbelGrp : (fld : Type) -> ((+) : fld -> fld -> fld) -> ((*) : fld -> fld -> fld) -> (pfgrp : IsGroup fld (+)) -> Type
IsModAbelGrp fld (+) (*) pfgrp = (IsModGrp fld (+) (*) pfgrp, Commutative fld (*))

-- similar to Arka's file on monoids
total
IsField : (fld : Type) -> ((+) : fld -> fld -> fld) -> ((*) : fld -> fld -> fld) -> Type
IsField fld (+) (*) = (pfgrp: IsAbelianGrp fld (+) ** ((IsModAbelGrp fld (+) (*) (fst pfgrp)), IsDistributive fld (+) (*)))