text:
= Imp : Simple Imperative Programs

> module Imp

> import Logic

In this chapter, we begin a new direction that will continue for the rest of the
course. Up to now most of our attention has been focused on various aspects of
Idris itself, while from now on we'll mostly be using Idris to formalize other
things. (We'll continue to pause from time to time to introduce a few additional
aspects of Idris.)

Our first case study is a _simple imperative programming language_ called Imp,
embodying a tiny core fragment of conventional mainstream languages such as C
and Java. Here is a familiar mathematical function written in Imp.

```
     Z ::= X;;
     Y ::= 1;;
     WHILE not (Z == 0) DO
       Y ::= Y * Z;;
       Z ::= Z - 1
     END
```

This chapter looks at how to define the _syntax_ and _semantics_ of Imp; the
chapters that follow develop a theory of _program equivalence_ and introduce
_Hoare Logic_, a widely used logic for reasoning about imperative programs.

> import Maps

> %hide (\\)

> %default total
> %access public export

== Arithmetic and Boolean Expressions

We'll present Imp in three parts: first a core language of _arithmetic and
boolean expressions_, then an extension of these expressions with _variables_,
and finally a language of _commands_ including assignment, conditions,
sequencing, and loops.

=== Syntax

These two definitions specify the _abstract syntax_ of arithmetic and boolean
expressions.

> data AExp0 : Type where
>   ANum0 : Nat -> AExp0
>   APlus0 : AExp0 -> AExp0 -> AExp0
>   AMinus0 : AExp0 -> AExp0 -> AExp0
>   AMult0 : AExp0 -> AExp0 -> AExp0
>
> data BExp0 : Type where
>   BTrue0 : BExp0
>   BFalse0 : BExp0
>   BEq0 : AExp0 -> AExp0 -> BExp0
>   BLe0 : AExp0 -> AExp0 -> BExp0
>   BNot0 : BExp0 -> BExp0
>   BAnd0 : BExp0 -> BExp0 -> BExp0

In this chapter, we'll elide the translation from the concrete syntax that a
programmer would actually write to these abstract syntax trees — the process
that, for example, would translate the string \idr{"1+2*3"} to the AST

```idris
      APlus0 (ANum0 1) (AMult0 (ANum0 2) (ANum0 3))
```

The optional chapter `ImpParser` develops a simple implementation of a lexical
analyzer and parser that can perform this translation. You do _not_ need to
understand that chapter to understand this one, but if you haven't taken a
course where these techniques are covered (e.g., a compilers course) you may
want to skim it.

For comparison, here's a conventional BNF (Backus-Naur Form) grammar defining
the same abstract syntax:

```
    a ::= Nat
        | a + a
        | a - a
        | a * a

    b ::= True
        | False
        | a = a
        | a ≤ a
        | not b
        | b and b
```

Compared to the Idris version above...

  - The BNF is more informal — for example, it gives some suggestions about the
    surface syntax of expressions (like the fact that the addition operation is
    written \idr{+} and is an infix symbol) while leaving other aspects of
    lexical analysis and parsing (like the relative precedence of \idr{+},
    \idr{-}, and \idr{*}, the use of parens to explicitly group subexpressions,
    etc.) unspecified. Some additional information (and human intelligence)
    would be required to turn this description into a formal definition, for
    example when implementing a compiler.

    The Idris version consistently omits all this information and concentrates
    on the abstract syntax only.

  - On the other hand, the BNF version is lighter and easier to read. Its
    informality makes it flexible, a big advantage in situations like
    discussions at the blackboard, where conveying general ideas is more
    important than getting every detail nailed down precisely.

    Indeed, there are dozens of BNF-like notations and people switch freely
    among them, usually without bothering to say which form of BNF they're using
    because there is no need to: a rough-and-ready informal understanding is all
    that's important.

It's good to be comfortable with both sorts of notations: informal ones for
communicating between humans and formal ones for carrying out implementations
and proofs.

=== Evaluation

_Evaluating_ an arithmetic expression produces a number.

> aeval0 : (a : AExp0) -> Nat
> aeval0 (ANum0 n) = n
> aeval0 (APlus0 a1 a2) = (aeval0 a1) + (aeval0 a2)
> aeval0 (AMinus0 a1 a2) = (aeval0 a1) `minus` (aeval0 a2)
> aeval0 (AMult0 a1 a2) = (aeval0 a1) * (aeval0 a2)

> test_aeval1 : aeval0 (APlus0 (ANum0 2) (ANum0 2)) = 4
> test_aeval1 = Refl

Similarly, evaluating a boolean expression yields a boolean.

> beval0 : (b : BExp0) -> Bool
> beval0 BTrue0 = True
> beval0 BFalse0 = False
> beval0 (BEq0 a1 a2) = (aeval0 a1) == (aeval0 a2)
> beval0 (BLe0 a1 a2) = lte (aeval0 a1) (aeval0 a2)
> beval0 (BNot0 b1) = not (beval0 b1)
> beval0 (BAnd0 b1 b2) = (beval0 b1) && (beval0 b2)

=== Optimization

We haven't defined very much yet, but we can already get some mileage out of the
definitions. Suppose we define a function that takes an arithmetic expression
and slightly simplifies it, changing every occurrence of \idr{0+e} (i.e.,
\idr{(APlus0 (ANum0 0) e}) into just \idr{e}.

> optimize_0plus : (a : AExp0) -> AExp0
> optimize_0plus (ANum0 n) = ANum0 n
> optimize_0plus (APlus0 (ANum0 Z) e2) =
>   optimize_0plus e2
> optimize_0plus (APlus0 e1 e2) =
>   APlus0 (optimize_0plus e1) (optimize_0plus e2)
> optimize_0plus (AMinus0 e1 e2) =
>   AMinus0 (optimize_0plus e1) (optimize_0plus e2)
> optimize_0plus (AMult0 e1 e2) =
>   AMult0 (optimize_0plus e1) (optimize_0plus e2)

To make sure our optimization is doing the right thing we can test it on some
examples and see if the output looks OK.

> test_optimize_0plus :
>   optimize_0plus (APlus0 (ANum0 2)
>                         (APlus0 (ANum0 0)
>                                (APlus0 (ANum0 0) (ANum0 1))))
>   = APlus0 (ANum0 2) (ANum0 1)

But if we want to be sure the optimization is correct — i.e., that evaluating an
optimized expression gives the same result as the original — we should prove it.

> optimize_0plus_sound : aeval0 (optimize_0plus a) = aeval0 a
> optimize_0plus_sound {a=ANum0 _} = Refl
> optimize_0plus_sound {a=APlus0 (ANum0 Z) y} =
>   optimize_0plus_sound {a=y}
> optimize_0plus_sound {a=APlus0 (ANum0 (S k)) y} =
>   cong {f=\x=>S(k+x)} $ optimize_0plus_sound {a=y}
> optimize_0plus_sound {a=APlus0 (APlus0 x z) y} =
>   rewrite optimize_0plus_sound {a=APlus0 x z} in
>   rewrite optimize_0plus_sound {a=y} in
>   Refl
> optimize_0plus_sound {a=APlus0 (AMinus0 x z) y} =
>   rewrite optimize_0plus_sound {a=x} in
>   rewrite optimize_0plus_sound {a=y} in
>   rewrite optimize_0plus_sound {a=z} in
>   Refl
> optimize_0plus_sound {a=APlus0 (AMult0 x z) y} =
>   rewrite optimize_0plus_sound {a=x} in
>   rewrite optimize_0plus_sound {a=y} in
>   rewrite optimize_0plus_sound {a=z} in
>   Refl
> optimize_0plus_sound {a=AMinus0 x y} =
>   rewrite optimize_0plus_sound {a=x} in
>   rewrite optimize_0plus_sound {a=y} in
>   Refl
> optimize_0plus_sound {a=AMult0 x y} =
>   rewrite optimize_0plus_sound {a=x} in
>   rewrite optimize_0plus_sound {a=y} in
>   Refl

== Coq Automation

\ \todo[inline]{Move the whole subsection to \idr{Pruviloj} chapter?}

The amount of repetition in this last proof is a little annoying. And if either
the language of arithmetic expressions or the optimization being proved sound
were significantly more complex, it would start to be a real problem.

So far, we've been doing all our proofs using just a small handful of Coq's
tactics and completely ignoring its powerful facilities for constructing parts
of proofs automatically. This section introduces some of these facilities, and
we will see more over the next several chapters. Getting used to them will take
some energy — Coq's automation is a power tool — but it will allow us to scale
up our efforts to more complex definitions and more interesting properties
without becoming overwhelmed by boring, repetitive, low-level details.

=== Tacticals

Tacticals is Coq's term for tactics that take other tactics as arguments —
"higher-order tactics," if you will.

==== The `try` Tactical

\ \todo[inline]{Exists in Pruviloj}

If `T` is a tactic, then `try T` is a tactic that is just like `T` except that,
if `T` fails, `try T` successfully does nothing at all (instead of failing).

```coq
Theorem silly1 : forall ae, aeval ae = aeval ae.
Proof. try Refl. (* this just does Refl *) Qed.

Theorem silly2 : forall (P : Type), P -> P.
Proof.
  intros P HP.
  try Refl. (* just Refl would have failed *)
  apply HP. (* we can still finish the proof in some other way *)
Qed.
```

There is no real reason to use `try` in completely manual proofs like these, but
it is very useful for doing automated proofs in conjunction with the `;`
tactical, which we show next.

==== The `;` Tactical (Simple Form)

\ \todo[inline]{Approximated by \idr{andThen} in Pruviloj}

In its most common form, the `;` tactical takes two tactics as arguments. The
compound tactic `T;T'` first performs `T` and then performs `T'` on each subgoal
generated by `T`.

For example, consider the following trivial lemma:

```coq
Lemma foo : forall n, lte 0 n = True.
Proof.
  intros.
  destruct n.
    (* Leaves two subgoals, which are discharged identically...  *)
    - (* n=0 *) simpl. Refl.
    - (* n=Sn' *) simpl. Refl.
Qed.
```

We can simplify this proof using the `;` tactical:

```coq
Lemma foo' : forall n, lte 0 n = True.
Proof.
  intros.
  (* destruct the current goal *)
  destruct n;
  (* then simpl each resulting subgoal *)
  simpl;
  (* and do Refl on each resulting subgoal *)
  Refl.
Qed.
```

Using `try` and `;` together, we can get rid of the repetition in the proof that
was bothering us a little while ago.

\ \todo[inline]{Mention
\href{http://docs.idris-lang.org/en/latest/reference/misc.html\#alternatives}{Alternatives} ?}

```coq
Theorem optimize_0plus_sound': forall a,
  aeval (optimize_0plus a) = aeval a.
Proof.
  intros a.
  induction a;
    (* Most cases follow directly by the IH... *)
    try (simpl; rewrite IHa1; rewrite IHa2; Refl).
    (* ... but the remaining cases -- ANum and APlus --
       are different: *)
  - (* ANum *) Refl.
  - (* APlus *)
    destruct a1;
      (* Again, most cases follow directly by the IH: *)
      try (simpl; simpl in IHa1; rewrite IHa1;
           rewrite IHa2; Refl).
    (* The interesting case, on which the try...
       does nothing, is when e1 = ANum n. In this
       case, we have to destruct n (to see whether
       the optimization applies) and rewrite with the
       induction hypothesis. *)
    + (* a1 = ANum n *) destruct n;
      simpl; rewrite IHa2; Refl. Qed.
```

Coq experts often use this "`...; try...`" idiom after a tactic like `induction`
to take care of many similar cases all at once. Naturally, this practice has an
analog in informal proofs. For example, here is an informal proof of the
optimization theorem that matches the structure of the formal one:

_Theorem_: For all arithmetic expressions `a`,
```
       aeval (optimize_0plus a) = aeval a.
```
_Proof_: By induction on `a`. Most cases follow directly from the `IH`. The
remaining cases are as follows:

  - Suppose `a = ANum n` for some `n`. We must show
```
       aeval (optimize_0plus (ANum n)) = aeval (ANum n).
```
    This is immediate from the definition of `optimize_0plus`.

  - Suppose `a = APlus a1 a2` for some `a1` and `a2`. We must show
```
       aeval (optimize_0plus (APlus a1 a2)) = aeval (APlus a1 a2).
```

    Consider the possible forms of `a1`. For most of them, `optimize_0plus`
    simply calls itself recursively for the subexpressions and rebuilds a new
    expression of the same form as `a1`; in these cases, the result follows
    directly from the `IH`. The interesting case is when `a1 = ANum n` for some
    `n`. If `n = ANum 0`, then
```
       optimize_0plus (APlus a1 a2) = optimize_0plus a2
```
    and the `IH` for `a2` is exactly what we need. On the other hand, if `n = S
    n'` for some `n'`, then again `optimize_0plus` simply calls itself
    recursively, and the result follows from the `IH`. $\square$

However, this proof can still be improved: the first case (for `a = ANum n`) is
very trivial — even more trivial than the cases that we said simply followed
from the `IH` — yet we have chosen to write it out in full. It would be better
and clearer to drop it and just say, at the top, "Most cases are either
immediate or direct from the `IH`. The only interesting case is the one for
`APlus...`" We can make the same improvement in our formal proof too. Here's how
it looks:

```coq
Theorem optimize_0plus_sound'': forall a,
  aeval (optimize_0plus a) = aeval a.
Proof.
  intros a.
  induction a;
    (* Most cases follow directly by the IH *)
    try (simpl; rewrite IHa1; rewrite IHa2; Refl);
    (* ... or are immediate by definition *)
    try Refl.
  (* The interesting case is when a = APlus a1 a2. *)
  - (* APlus *)
    destruct a1; try (simpl; simpl in IHa1; rewrite IHa1;
                      rewrite IHa2; Refl).
    + (* a1 = ANum n *) destruct n;
      simpl; rewrite IHa2; Refl. Qed.
```

==== The `;` Tactical (General Form)

The ; tactical also has a more general form than the simple `T;T'` we've seen
above. If `T, T1, ..., Tn` are tactics, then

```coq
      T; [T1 | T2 | ... | Tn]
```

is a tactic that first performs `T` and then performs `T1` on the first subgoal
generated by `T`, performs `T2` on the second subgoal, etc.

So `T;T'` is just special notation for the case when all of the `Ti`'s are the
same tactic; i.e.,` T;T`' is shorthand for:

```coq
      T; [T' | T' | ... | T']
```

==== The `repeat` Tactical

\ \todo[inline]{Approximated by \idr{repeatUntilFail} in Pruviloj}

The `repeat` tactical takes another tactic and keeps applying this tactic until
it fails. Here is an example showing that `10` is in a long list using `repeat`.

```coq
Theorem In10 : In 10 [1;2;3;4;5;6;7;8;9;10].
Proof.
  repeat (try (left; Refl); right).
Qed.
```

The tactic `repeat T` never fails: if the tactic `T` doesn't apply to the
original goal, then repeat still succeeds without changing the original goal
(i.e., it repeats zero times).

```coq
Theorem In10' : In 10 [1;2;3;4;5;6;7;8;9;10].
Proof.
  repeat (left; Refl).
  repeat (right; try (left; Refl)).
Qed.
```

The tactic `repeat T` also does not have any upper bound on the number of times
it applies `T`. If `T` is a tactic that always succeeds, then `repeat T` will
loop forever (e.g., `repeat simpl` loops forever, since `simpl` always
succeeds). While evaluation in Coq's term language, Gallina, is guaranteed to
terminate, tactic evaluation is not! This does not affect Coq's logical
consistency, however, since the job of `repeat` and other tactics is to guide
Coq in constructing proofs; if the construction process diverges, this simply
means that we have failed to construct a proof, not that we have constructed a
wrong one.

==== Exercise: 3 stars (optimize_0plus_b)

Since the \idr{optimize_0plus} transformation doesn't change the value of
\idr{AExp}s, we should be able to apply it to all the \idr{AExp}s that appear in
a \idr{BExp} without changing the \idr{BExp}'s value. Write a function which
performs that transformation on \idr{BExp}s, and prove it is sound. Use the
tacticals we've just seen to make the proof as elegant as possible.

> optimize_0plus_b : (b : BExp0) -> BExp0
> optimize_0plus_b b = ?optimize_0plus_b_rhs

> optimize_0plus_b_sound : beval0 (optimize_0plus_b b) = beval0 b
> optimize_0plus_b_sound = ?optimize_0plus_b_sound_rhs

$\square$

==== Exercise: 4 stars, optional (optimizer)

_Design exercise_: The optimization implemented by our \idr{optimize_0plus}
function is only one of many possible optimizations on arithmetic and boolean
expressions. Write a more sophisticated optimizer and prove it correct. (You
will probably find it easiest to start small — add just a single, simple
optimization and prove it correct — and build up to something more interesting
incrementially.)

> --FILL IN HERE

$\square$

=== Defining New Tactic Notations

Coq also provides several ways of "programming" tactic scripts.

  - The `Tactic Notation` idiom illustrated below gives a handy way to define
    "shorthand tactics" that bundle several tactics into a single command.

  - For more sophisticated programming, Coq offers a built-in programming
    language called `Ltac` with primitives that can examine and modify the proof
    state. The details are a bit too complicated to get into here (and it is
    generally agreed that `Ltac` is not the most beautiful part of Coq's
    design!), but they can be found in the reference manual and other books on
    Coq, and there are many examples of `Ltac` definitions in the Coq standard
    library that you can use as examples.

  - There is also an OCaml API, which can be used to build tactics that access
    Coq's internal structures at a lower level, but this is seldom worth the
    trouble for ordinary Coq users.

The `Tactic Notation` mechanism is the easiest to come to grips with, and it
offers plenty of power for many purposes. Here's an example.

```coq
Tactic Notation "simpl_and_try" tactic(c) :=
  simpl;
  try c.
```

This defines a new tactical called `simpl_and_try` that takes one tactic `c` as
an argument and is defined to be equivalent to the tactic `simpl; try c`. Now
writing "`simpl_and_try Refl.`" in a proof will be the same as writing "`simpl;
try Refl.`"

=== The `omega` Tactic

\ \todo[inline]{Related to https://github.com/forestbelton/cooper}

The `omega` tactic implements a decision procedure for a subset of first-order
logic called _Presburger arithmetic_. It is based on the Omega algorithm
invented in 1991 by William Pugh [Pugh 1991].

If the goal is a universally quantified formula made out of

  - numeric constants, addition (`+` and `S`), subtraction (`-` and `pred`), and
    multiplication by constants (this is what makes it Presburger arithmetic),

  - equality (`=` and `/=`) and inequality (`<=`), and

  - the logical connectives `/\`, `\/`, `Not`, and `->`,

then invoking `omega` will either solve the goal or tell you that it is actually
false.

```coq
Example silly_presburger_example : forall m n o p,
  m + n <= n + o /\ o + 3 = p + 3 ->
  m <= p.
Proof.
  intros. omega.
Qed.
```

=== A Few More Handy Tactics

Finally, here are some miscellaneous tactics that you may find convenient.

  - `clear H`: Delete hypothesis `H` from the context.

  - `subst x`: Find an assumption `x = e` or `e = x` in the context, replace `x`
     with `e` throughout the context and current goal, and clear the assumption.

  - `subst`: Substitute away all assumptions of the form `x = e` or `e = x`.

  - `rename... into...`: Change the name of a hypothesis in the proof context.
    For example, if the context includes a variable named `x`, then `rename x
    into y` will change all occurrences of `x` to `y`.

  - `assumption`: Try to find a hypothesis `H` in the context that exactly
    matches the goal; if one is found, behave like `apply H`.

  - `contradiction`: Try to find a hypothesis `H` in the current context that is
    logically equivalent to `Void`. If one is found, solve the goal.

  - `constructor`: Try to find a constructor `c` (from some `Inductive`
    definition in the current environment) that can be applied to solve the
    current goal. If one is found, behave like `apply c`.

We'll see examples below.

== Evaluation as a Relation

We have presented \idr{aeval} and \idr{beval} as functions. Another way to think
about evaluation — one that we will see is often more flexible — is as a
_relation_ between expressions and their values. This leads naturally to
\idr{data} definitions like the following one for arithmetic expressions...

```idris
data AEvalR : AExp0 -> Nat -> Type where
  E_ANum : (n: Nat) -> AEvalR (ANum n) n
  E_APlus : (e1, e2 : AExp0) -> (n1, n2 : Nat) ->
    AEvalR e1 n1 ->
    AEvalR e2 n2 ->
    AEvalR (APlus e1 e2) (n1 + n2)
  E_AMinus : (e1, e2 : AExp0) -> (n1, n2 : Nat) ->
    AEvalR e1 n1 ->
    AEvalR e2 n2 ->
    AEvalR (AMinus0 e1 e2) (n1 `minus` n2)
  E_AMult : (e1, e2: AExp0) -> (n1, n2 : Nat) ->
    AEvalR e1 n1 ->
    AEvalR e2 n2 ->
    AEvalR (AMult0 e1 e2) (n1 * n2)
```

\todo[inline]{Edit}

It will be convenient to have an infix notation for \idr{AEvalR}. We'll write
\idr{e \\ n} to mean that arithmetic expression \idr{e} evaluates to value
\idr{n}.

In fact, Idris provides a way to use this notation in the definition of
\idr{AevalR} itself. This reduces confusion by avoiding situations where we're
working on a proof involving statements in the form \idr{e \\ n} but we have to
refer back to a definition written using the form \idr{AEvalR e n}.

We do this by first "reserving" the notation, then giving the definition
together with a declaration of what the notation means.

> data (\\) : AExp0 -> (n : Nat) -> Type where
>   E_ANum : (ANum0 n) \\ n
>   E_APlus : e1 \\ n1 -> e2 \\ n2 -> n = n1 + n2 ->
>             (APlus0 e1 e2) \\ n

\todo[inline]{We don't use \idr{-} since it requires a proof of \idr{LTE n1 n2}}

>   E_AMinus : e1 \\ n1 -> e2 \\ n2 -> n = n1 `minus` n2 ->
>              (AMinus0 e1 e2) \\ n
>   E_AMult : e1 \\ n1 -> e2 \\ n2 -> n = n1 * n2 ->
>             (AMult0 e1 e2) \\ n

> AEvalR : AExp0 -> Nat -> Type
> AEvalR = (\\)

=== Inference Rule Notation

\ \todo[inline]{Add hyperlink}

In informal discussions, it is convenient to write the rules for \idr{AEvalR}
and similar relations in the more readable graphical form of inference rules,
where the premises above the line justify the conclusion below the line (we have
already seen them in the `IndProp` chapter).

For example, the constructor \idr{E_APlus}...

```idris
  E_APlus : (e1 \\ n1) -> (e2 \\ n2) -> (n = n1 + n2) ->
            (APlus0 e1 e2) \\ n
```

...would be written like this as an inference rule:

\[
  \begin{prooftree}
    \hypo{\idr{e1 \\ n1}}
    \hypo{\idr{e2 \\ n2}}
    \infer2[\idr{E_APlus}]{\idr{APlus e1 e2 \\ n1+n2}}
  \end{prooftree}
\]

Formally, there is nothing deep about inference rules: they are just
implications. You can read the rule name on the right as the name of the
constructor and read each of the linebreaks between the premises above the line
(as well as the line itself) as \idr{->}. All the variables mentioned in the
rule (\idr{e1}, \idr{n1}, etc.) are implicitly bound by universal quantifiers at
the beginning. (Such variables are often called _metavariables_ to distinguish
them from the variables of the language we are defining. At the moment, our
arithmetic expressions don't include variables, but we'll soon be adding them.)
The whole collection of rules is understood as being wrapped in an function
declaration. In informal prose, this is either elided or else indicated by
saying something like "Let \idr{AEvalR} be the smallest relation closed under
the following rules...".

For example, \idr{\\} is the smallest relation closed under these rules:

\[
  \begin{prooftree}
    \infer0[\idr{E_ANum}]{\idr{ANum n \\ n}}
  \end{prooftree}
\]

\[
  \begin{prooftree}
    \hypo{\idr{e1 \\ n1}}
    \hypo{\idr{e2 \\ n2}}
    \infer2[\idr{E_APlus}]{\idr{APlus e1 e2 \\ n1+n2}}
  \end{prooftree}
\]

\[
  \begin{prooftree}
    \hypo{\idr{e1 \\ n1}}
    \hypo{\idr{e2 \\ n2}}
    \infer2[\idr{E_AMinus}]{\idr{AMinus e1 e2 \\ n1-n2}}
  \end{prooftree}
\]

\[
  \begin{prooftree}
    \hypo{\idr{e1 \\ n1}}
    \hypo{\idr{e2 \\ n2}}
    \infer2[\idr{E_AMult}]{\idr{AMult e1 e2 \\ n1*n2}}
  \end{prooftree}
\]

=== Equivalence of the Definitions

It is straightforward to prove that the relational and functional definitions of
evaluation agree:

> aeval_iff_aevalR : (a \\ n) <-> aeval0 a = n
> aeval_iff_aevalR = (to, fro)
> where
>   to : (a \\ n) -> aeval0 a = n
>   to E_ANum = Refl
>   to (E_APlus x y xy) =
>     rewrite xy in
>     rewrite to x in
>     rewrite to y in Refl
>   to (E_AMinus x y xy) =
>     rewrite xy in
>     rewrite to x in
>     rewrite to y in Refl
>   to (E_AMult x y xy) =
>     rewrite xy in
>     rewrite to x in
>     rewrite to y in Refl
>   fro : (aeval0 a = n) -> (a \\ n)
>   fro {a=ANum0 n} Refl = E_ANum
>   fro {a=APlus0 x y} prf =
>     E_APlus (fro Refl) (fro Refl) (sym prf)
>   fro {a=AMinus0 x y} prf =
>     E_AMinus (fro Refl) (fro Refl) (sym prf)
>   fro {a=AMult0 x y} prf =
>     E_AMult (fro Refl) (fro Refl) (sym prf)

We can make the proof quite a bit shorter by making more use of tacticals.

```coq
Theorem aeval_iff_aevalR' : forall a n,
  (a \\ n) <-> aeval a = n.
Proof.
  (* WORKED IN CLASS *)
  split.
  - (* -> *)
    intros H; induction H; subst; Refl.
  - (* <- *)
    generalize dependent n.
    induction a; simpl; intros; subst; constructor;
       try apply IHa1; try apply IHa2; Refl.
Qed.
```

==== Exercise: 3 stars (bevalR)

Write a relation \idr{BEvalR} in the same style as \idr{AEvalR}, and prove that
it is equivalent to \idr{beval0}.

> -- data BEvalR : BExp0 -> (b : Bool) -> Type where
>   -- FILL IN HERE
>
> -- beval_iff_bevalR : (BEvalR b bv) <-> beval0 b = bv

$\square$

=== Computational vs. Relational Definitions

For the definitions of evaluation for arithmetic and boolean expressions, the
choice of whether to use functional or relational definitions is mainly a matter
of taste: either way works.

However, there are circumstances where relational definitions of evaluation work
much better than functional ones.

For example, suppose that we wanted to extend the arithmetic operations by
considering also a division operation:

> namespace AEvalRDiv

>   data AExpD : Type where
>     ANumD : Nat -> AExpD
>     APlusD : AExpD -> AExpD -> AExpD
>     AMinusD : AExpD -> AExpD -> AExpD
>     AMultD : AExpD -> AExpD -> AExpD
>     ADivD : AExpD -> AExpD -> AExpD -- <--- new

Extending the definition of \idr{aeval} to handle this new operation would not
be straightforward (what should we return as the result of
\idr{ADiv (ANum 5) (ANum 0)}?). But extending \idr{AEvalR} is straightforward.

>   infix 5 \\\

>   data (\\\) : AExpD -> (n : Nat) -> Type where
>     E_ANumD : (ANumD n) \\\ n
>     E_APlusD : e1 \\\ n1 -> e2 \\\ n2 -> n = n1 + n2 ->
>       (APlusD e1 e2) \\\ n
>     E_AMinusD : e1 \\\ n1 -> e2 \\\ n2 -> n = n1 `minus` n2 ->
>       (AMinusD e1 e2) \\\ n
>     E_AMultD : e1 \\\ n1 -> e2 \\\ n2 -> n = n1 * n2 ->
>       (AMultD e1 e2) \\\ n
>     E_ADivD : e1 \\\ n1 -> e2 \\\ n2 -> n2 `GT` 0 -> n1 = n2*n3 ->
>       (ADivD e1 e2) \\\ n3

>   AEvalRD : AExpD -> Nat -> Type
>   AEvalRD = (\\\)

Suppose, instead, that we want to extend the arithmetic operations by a
nondeterministic number generator \idr{any} that, when evaluated, may yield any
number. (Note that this is not the same as making a _probabilistic_ choice among
all possible numbers — we're not specifying any particular distribution of
results, but just saying what results are _possible_.)

> namespace AEvalRAny

>   data AExpA : Type where
>     AAnyA : AExpA -- <--- new
>     ANumA : Nat -> AExpA
>     APlusA : AExpA -> AExpA -> AExpA
>     AMinusA : AExpA -> AExpA -> AExpA
>     AMultA : AExpA -> AExpA -> AExpA

Again, extending \idr{aeval} would be tricky, since now evaluation is _not_ a
deterministic function from expressions to numbers, but extending \idr{AEvalR}
is no problem:

>   infix 5 \\\

>   data (\\\) : AExpA -> (n : Nat) -> Type where
>     E_AnyA : AAnyA \\\ n
>     E_ANumA : (ANumA n) \\\ n
>     E_APlusA : e1 \\\ n1 -> e2 \\\ n2 -> n = n1 + n2 ->
>       (APlusA e1 e2) \\\ n
>     E_AMinusA : e1 \\\ n1 -> e2 \\\ n2 -> n = n1 `minus` n2 ->
>       (AMinusA e1 e2) \\\ n
>     E_AMultA : e1 \\\ n1 -> e2 \\\ n2 -> n = n1 * n2 ->
>       (AMultA e1 e2) \\\ n

>   AEvalRA : AExpA -> Nat -> Type
>   AEvalRA = (\\\)

At this point you maybe wondering: which style should I use by default? The
examples above show that relational definitions are fundamentally more powerful
than functional ones. For situations like these, where the thing being defined
is not easy to express as a function, or indeed where it is _not_ a function,
there is no choice. But what about when both styles are workable?

\ \todo[inline]{Edit}

One point in favor of relational definitions is that some people feel they are
more elegant and easier to understand. Another is that Idris automatically
generates nice inversion and induction principles from function definitions.

On the other hand, functional definitions can often be more convenient:

  - Functions are by definition deterministic and defined on all arguments; for
    a relation we have to show these properties explicitly if we need them.

  - With functions we can also take advantage of Idris's computation mechanism
    to simplify expressions during proofs.

Furthermore, functions can be directly "extracted" to executable code in C
or JavaScript.

Ultimately, the choice often comes down to either the specifics of a particular
situation or simply a question of taste. Indeed, in large Idris developments it
is common to see a definition given in _both_ functional and relational styles,
plus a lemma stating that the two coincide, allowing further proofs to switch
from one point of view to the other at will.

== Expressions With Variables

Let's turn our attention back to defining Imp. The next thing we need to do is
to enrich our arithmetic and Boolean expressions with variables. To keep things
simple, we'll assume that all variables are global and that they only hold
numbers.

=== States

Since we'll want to look variables up to find out their current values, we'll
reuse the type \idr{Id} from the `Maps` chapter for the type of variables in
Imp.

A _machine state_ (or just _state_) represents the current values of _all_
variables at some point in the execution of a program.

For simplicity, we assume that the state is defined for _all_ variables, even
though any given program is only going to mention a finite number of them. The
state captures all of the information stored in memory. For Imp programs,
because each variable stores a natural number, we can represent the state as a
mapping from identifiers to \idr{Nat}. For more complex programming languages,
the state might have more structure.

> State : Type
> State = TotalMap Nat

> empty_state : State
> empty_state = t_empty 0

=== Syntax

We can add variables to the arithmetic expressions we had before by simply
adding one more constructor:

> data AExp : Type where
>   ANum : Nat -> AExp
>   AId : Id -> AExp -- <----- NEW
>   APlus : AExp -> AExp -> AExp
>   AMinus : AExp -> AExp -> AExp
>   AMult : AExp -> AExp -> AExp

Defining a few variable names as notational shorthands will make examples easier
to read:

> W : Id
> W = MkId "W"
> X : Id
> X = MkId "X"
> Y : Id
> Y = MkId "Y"
> Z : Id
> Z = MkId "Z"

\todo[inline]{Edit}

(This convention for naming program variables (\idr{X}, \idr{Y}, \idr{Z})
clashes a bit with our earlier use of uppercase letters for types. Since we're
not using polymorphism heavily in the chapters devoped to Imp, this overloading
should not cause confusion.)

The definition of \idr{BExp}s is unchanged (except for using the new
\idr{AExp}s):

> data BExp : Type where
>   BTrue : BExp
>   BFalse : BExp
>   BEq : AExp -> AExp -> BExp
>   BLe : AExp -> AExp -> BExp
>   BNot : BExp -> BExp
>   BAnd : BExp -> BExp -> BExp

=== Evaluation

The arith and boolean evaluators are extended to handle variables in the obvious
way, taking a state as an extra argument:

> aeval : (st : State) -> (a : AExp) -> Nat
> aeval _ (ANum n) = n
> aeval st (AId i) = st i
> aeval st (APlus a1 a2) = (aeval st a1) + (aeval st a2)
> aeval st (AMinus a1 a2) = (aeval st a1) `minus` (aeval st a2)
> aeval st (AMult a1 a2) = (aeval st a1) * (aeval st a2)
>
> beval : (st : State) -> (b : BExp) -> Bool
> beval _ BTrue = True
> beval _ BFalse = False
> beval st (BEq a1 a2) = (aeval st a1) == (aeval st a2)
> beval st (BLe a1 a2) = lte (aeval st a1) (aeval st a2)
> beval st (BNot b1) = not (beval st b1)
> beval st (BAnd b1 b2) = (beval st b1) && (beval st b2)

> aexp1 : aeval (t_update X 5 Imp.empty_state)
>               (APlus (ANum 3) (AMult (AId X) (ANum 2)))
>         = 13
> aexp1 = Refl

> bexp1 : beval (t_update X 5 Imp.empty_state)
>               (BAnd BTrue (BNot (BLe (AId X) (ANum 4))))
>         = True
> bexp1 = Refl

== Commands

Now we are ready define the syntax and behavior of Imp _commands_ (sometimes
called _statements_).

=== Syntax

Informally, commands \idr{c} are described by the following BNF grammar. (We
choose this slightly awkward concrete syntax for the sake of being able to
define Imp syntax using Idris's \idr{syntax} mechanism. In particular, we use
\idr{IFB} to avoid conflicting with the \idr{if} notation from the standard
library.)

```
     c ::= SKIP | x ::= a | c ;; c | IFB b THEN c ELSE c FI
         | WHILE b DO c END
```

For example, here's factorial in Imp:

```
     Z ::= X;;
     Y ::= 1;;
     WHILE not (Z = 0) DO
       Y ::= Y * Z;;
       Z ::= Z - 1
     END
```

When this command terminates, the variable \idr{Y} will contain the factorial of
the initial value of \idr{X}.

Here is the formal definition of the abstract syntax of commands:

> data Com : Type where
>   CSkip : Com
>   CAss : Id -> AExp -> Com
>   CSeq : Com -> Com -> Com
>   CIf : BExp -> Com -> Com -> Com
>   CWhile : BExp -> Com -> Com

As usual, we can use a few `Notation` declarations to make things more readable.
To avoid conflicts with Idris's built-in notations, we keep this light — in
particular, we don't introduce any notations for \idr{AExp}s and \idr{BExp}s to
avoid confusion with the numeric and boolean operators we've already defined.

\ \todo[inline]{Explain do-notation}

> infix 5 ::=

> SKIP : Com
> SKIP = CSkip

> (::=) : Id -> AExp -> Com
> (::=) = CAss

> (>>=) : Com -> (() -> Com) -> Com
> (>>=) c f = CSeq c (f ())

> WHILE : BExp -> Com -> Com
> WHILE = CWhile

> syntax IFB [c1] THEN [c2] ELSE [c3] FI = CIf c1 c2 c3

For example, here is the factorial function again, written as a formal
definition to Idris:

> fact_in_idris : Com
> fact_in_idris = do
>  Z ::= AId X
>  Y ::= ANum 1
>  WHILE (BNot (BEq (AId Z) (ANum 0))) $ do
>    Y ::= AMult (AId Y) (AId Z)
>    Z ::= AMinus (AId Z) (ANum 1)

=== More Examples

==== Assignment:

> plus2 : Com
> plus2 =
>  X ::= APlus (AId X) (ANum 2)

> XtimesYinZ : Com
> XtimesYinZ =
>  Z ::= AMult (AId X) (AId Y)

> subtract_slowly_body : Com
> subtract_slowly_body = do
>   Z ::= AMinus (AId Z) (ANum 1)
>   X ::= AMinus (AId X) (ANum 1)

==== Loops

> subtract_slowly : Com
> subtract_slowly =
>  WHILE (BNot (BEq (AId X) (ANum 0))) $ do
>    subtract_slowly_body

> subtract_3_from_5_slowly : Com
> subtract_3_from_5_slowly = do
>   X ::= ANum 3
>   Z ::= ANum 5
>   subtract_slowly

==== An infinite loop:

> loop : Com
> loop = WHILE BTrue SKIP

== Evaluating Commands

Next we need to define what it means to evaluate an Imp command. The fact that
\idr{WHILE} loops don't necessarily terminate makes defining an evaluation
function tricky...

=== Evaluation as a Function (Failed Attempt)

Here's an attempt at defining an evaluation function for commands, omitting the
\idr{WHILE} case.

> ceval_fun_no_while : (st : State) -> (c : Com) -> State
> ceval_fun_no_while st CSkip = st
> ceval_fun_no_while st (CAss x a) = t_update x (aeval st a) st
> ceval_fun_no_while st (CSeq c1 c2) =
>   let st' = ceval_fun_no_while st c1
>   in ceval_fun_no_while st' c2
> ceval_fun_no_while st (CIf b c1 c2) =
>   if beval st b
>     then ceval_fun_no_while st c1
>     else ceval_fun_no_while st c2
> ceval_fun_no_while st (CWhile b c) = st   -- bogus

In a traditional functional programming language like OCaml or Haskell we could
add the \idr{WHILE} case as follows:

```idris
...
ceval_fun st (CWhile b c) =
  if (beval st b)
    then ceval_fun st (CSeq c $ CWhile b c)
    else st
```

Idris doesn't accept such a definition ("Imp.ceval_fun is possibly not total due
to recursive path Imp.ceval_fun --> Imp.ceval_fun --> Imp.ceval_fun") because
the function we want to define is not guaranteed to terminate. Indeed, it
_doesn't_ always terminate: for example, the full version of the \idr{ceval_fun}
function applied to the \idr{loop} program above would never terminate. Since
Idris is not just a functional programming language but also a consistent logic,
any potentially non-terminating function needs to be rejected. Here is an
(invalid!) program showing what would go wrong if Idris allowed non-terminating
recursive functions:

\ \todo[inline]{Edit, discuss \idr{partial}}

```idris
loop_false : (n : Nat) -> Void
loop_false n = loop_false n
```

That is, propositions like \idr{Void} would become provable (\idr{loop_false 0}
would be a proof of \idr{Void}), which would be a disaster for Idris's logical
consistency.

Thus, because it doesn't terminate on all inputs, \idr{ceval_fun} cannot be
written in Idris — at least not without additional tricks and workarounds (see
chapter `ImpCEvalFun` if you're curious about what those might be).

=== Evaluation as a Relation

Here's a better way: define \idr{CEval} as a _relation_ rather than a _function_
— i.e., define it with \idr{data}, as we did for \idr{AEvalR} above.

This is an important change. Besides freeing us from awkward workarounds, it
gives us a lot more flexibility in the definition. For example, if we add
nondeterministic features like \idr{any} to the language, we want the definition
of evaluation to be nondeterministic — i.e., not only will it not be total, it
will not even be a function!

We'll use the notation \idr{c / st \\ st'} for the \idr{CEval} relation:
\idr{c / st \\ st'} means that executing program \idr{c} in a starting state
\idr{st} results in an ending state \idr{st'}. This can be pronounced "\idr{c}
takes state \idr{st} to \idr{st'}".

==== Operational Semantics

Here is an informal definition of evaluation, presented as inference rules for
readability:

\[
  \begin{prooftree}
    \infer0[\idr{E_Skip}]{\idr{SKIP / st \\ st}}
  \end{prooftree}
\]

\[
  \begin{prooftree}
    \hypo{\idr{aeval st a1 = n}}
    \infer1[\idr{E_Ass}]{\idr{x := a1 / st \\ (t_update st x n)}}
  \end{prooftree}
\]

\[
  \begin{prooftree}
    \hypo{\idr{c1 / st \\ st'}}
    \hypo{\idr{c2 / st' \\ st''}}
    \infer2[\idr{E_Seq}]{\idr{c1;;c2 / st \\ st''}}
  \end{prooftree}
\]

\[
  \begin{prooftree}
    \hypo{\idr{beval st b1 = True}}
    \hypo{\idr{c1 / st \\ st'}}
    \infer2[\idr{E_IfTrue}]{\idr{IF b1 THEN c1 ELSE c2 FI / st \\ st'}}
  \end{prooftree}
\]

\[
  \begin{prooftree}
    \hypo{\idr{beval st b1 = False}}
    \hypo{\idr{c2 / st \\ st'}}
    \infer2[\idr{E_IfFalse}]{\idr{IF b1 THEN c1 ELSE c2 FI / st \\ st'}}
  \end{prooftree}
\]

\[
  \begin{prooftree}
    \hypo{\idr{beval st b = False}}
    \infer1[\idr{E_WhileEnd}]{\idr{WHILE b DO c END / st \\ st}}
  \end{prooftree}
\]

\[
  \begin{prooftree}
    \hypo{\idr{beval st b = True}}
    \hypo{\idr{c / st \\ st'}}
    \hypo{\idr{WHILE b DO c END / st' \\ st''}}
    \infer3[\idr{E_WhileLoop}]{\idr{WHILE b DO c END / st \\ st''}}
  \end{prooftree}
\]

Here is the formal definition. Make sure you understand how it corresponds to
the inference rules.

> data CEval : Com -> State -> State -> Type where
>   E_Skip : CEval CSkip st st
>   E_Ass : aeval st a1 = n -> CEval (CAss x a1) st (t_update x n st)
>   E_Seq : CEval c1 st st' -> CEval c2 st' st'' ->
>     CEval (CSeq c1 c2) st st''
>   E_IfTrue : beval st b = True -> CEval c1 st st' ->
>     CEval (CIf b c1 c2) st st'
>   E_IfFalse : beval st b = False -> CEval c2 st st' ->
>     CEval (CIf b c1 c2) st st'
>   E_WhileEnd : beval st b = False ->
>     CEval (CWhile b c) st st
>   E_WhileLoop : beval st b = True ->
>     CEval c st st' -> CEval (CWhile b c) st' st'' ->
>     CEval (CWhile b c) st st''

> syntax [c1] "/" [st] "\\\\" [st'] = CEval c1 st st'

The cost of defining evaluation as a relation instead of a function is that we
now need to construct _proofs_ that some program evaluates to some result state,
rather than just letting Idris's computation mechanism do it for us.

 test : Com
 test = do
   X ::= ANum 2
   IFB BLe (AId X) (ANum 1)
     THEN (Y ::= ANum 3)
     ELSE (Z ::= ANum 4)
   FI

> ceval_example1 : (do
>   X ::= ANum 2
>   IFB BLe (AId X) (ANum 1)
>     THEN (Y ::= ANum 3)
>     ELSE (Z ::= ANum 4)
>   FI)
>   / Imp.empty_state
>  \\ (t_update Z 4 $ t_update X 2 $ Imp.empty_state)
> ceval_example1 =
>   E_Seq
>     (E_Ass Refl)
>     (E_IfFalse Refl
>                (E_Ass Refl))

==== Exercise: 2 stars (ceval_example2)

> ceval_example2 : (do
>    X ::= ANum 0
>    Y ::= ANum 1
>    Z ::= ANum 2)
>    / Imp.empty_state
>   \\ (t_update Z 2 $ t_update Y 1 $ t_update X 0 $ Imp.empty_state)
> ceval_example2 = ?ceval_example2_rhs

$\square$

==== Exercise: 3 stars, advanced (pup_to_n)

Write an Imp program that sums the numbers from \idr{1} to \idr{X} (inclusive:
\idr{1 + 2 + ... + X}) in the variable \idr{Y}. Prove that this program executes
as intended for \idr{X = 2} (this is trickier than you might expect).

> pup_to_n : Com
> pup_to_n = ?pup_to_n_rhs

> pup_to_2_ceval :
>   Imp.pup_to_n / (t_update X 2 Imp.empty_state) \\
>    (t_update X 0 $
>     t_update Y 3 $
>     t_update X 1 $
>     t_update Y 2 $
>     t_update Y 0 $
>     t_update X 2 $
>     Imp.empty_state)
> pup_to_2_ceval = ?pup_to_2_ceval_rhs

$\square$

=== Determinism of Evaluation

Changing from a computational to a relational definition of evaluation is a good
move because it frees us from the artificial requirement that evaluation should
be a total function. But it also raises a question: Is the second definition of
evaluation really a partial function? Or is it possible that, beginning from the
same state \idr{st}, we could evaluate some command \idr{c} in different ways to
reach two different output states \idr{st'} and \idr{st''}?

In fact, this cannot happen: \idr{CEval} _is_ a partial function:

> ceval_deterministic : (c / st \\ st1) -> (c / st \\ st2) -> st1 = st2
> ceval_deterministic E_Skip E_Skip = Refl
> ceval_deterministic (E_Ass aev1) (E_Ass aev2) =
>   rewrite sym aev1 in
>   rewrite sym aev2 in Refl
> ceval_deterministic {st2} (E_Seq cev11 cev12)
>                           (E_Seq {c2} cev21 cev22) =
>   let ih = ceval_deterministic cev11 cev21
>       cev22' = replace (sym ih) cev22 {P=\x=>CEval c2 x st2}
>   in ceval_deterministic cev12 cev22'
> ceval_deterministic (E_IfTrue _ cev1) (E_IfTrue _ cev2) =
>   ceval_deterministic cev1 cev2
> ceval_deterministic (E_IfTrue prf1 _) (E_IfFalse prf2 _) =
>   absurd $ replace prf1 prf2 {P=\x=>x=False}
> ceval_deterministic (E_IfFalse prf1 _) (E_IfTrue prf2 _) =
>   absurd $ replace prf2 prf1 {P=\x=>x=False}
> ceval_deterministic (E_IfFalse _ cev1) (E_IfFalse _ cev2) =
>   ceval_deterministic cev1 cev2
> ceval_deterministic (E_WhileEnd _) (E_WhileEnd _) = Refl
> ceval_deterministic (E_WhileEnd prf1) (E_WhileLoop prf2 _ _) =
>   absurd $ replace prf2 prf1 {P=\x=>x=False}
> ceval_deterministic (E_WhileLoop prf1 _ _) (E_WhileEnd prf2) =
>   absurd $ replace prf1 prf2 {P=\x=>x=False}
> ceval_deterministic {st2} (E_WhileLoop _ cev11 cev12)
>                           (E_WhileLoop {b} {c} _ cev21 cev22) =
>   let ih = ceval_deterministic cev11 cev21
>       cev22' = replace (sym ih) cev22 {P=\x=>CEval (CWhile b c) x st2}
>   in ceval_deterministic cev12 cev22'

== Reasoning About Imp Programs

We'll get deeper into systematic techniques for reasoning about Imp programs in
the following chapters, but we can do quite a bit just working with the bare
definitions. This section explores some examples.

> plus2_spec : st X = n -> (Imp.plus2 / st \\ st') -> st' X = n + 2

\todo[inline]{Edit}

Inverting `Heval` essentially forces Idris to expand one step of the \idr{CEval}
computation — in this case revealing that \idr{st'} must be st extended with the
new value of \idr{X}, since \idr{plus2} is an assignment

> plus2_spec Refl (E_Ass Refl) = Refl

==== Exercise: 3 stars, recommendedM (XtimesYinZ_spec)

State and prove a specification of \idr{XtimesYinZ}.

> -- FILL IN HERE

$\square$

==== Exercise: 3 stars, recommended (loop_never_stops)

> loop_never_stops : Not (Imp.loop / st \\ st')
> loop_never_stops contra = ?loop_never_stops_rhs

\todo[inline]{Edit the hint}

```coq
Proof.
  intros st st' contra. unfold loop in contra.
  remember (WHILE BTrue DO SKIP END) as loopdef
           eqn:Heqloopdef.
```

Proceed by induction on the assumed derivation showing that loopdef terminates.
Most of the cases are immediately contradictory (and so can be solved in one
step with inversion).

  (* FILL IN HERE *) Admitted.

$\square$

==== Exercise: 3 stars (no_whilesR)

Consider the following function:

> no_whiles : (c : Com) -> Bool
> no_whiles CSkip = True
> no_whiles (CAss _ _) = True
> no_whiles (CSeq c1 c2) = (no_whiles c1) && (no_whiles c2)
> no_whiles (CIf _ ct cf) = (no_whiles ct) && (no_whiles cf)
> no_whiles (CWhile _ _) = False

This predicate yields \idr{True} just on programs that have no while loops.
Using \idr{data}, write a property \idr{No_whilesR} such that \idr{No_whilesR c}
is provable exactly when \idr{c} is a program with no while loops. Then prove
its equivalence with \idr{no_whiles}.

> data No_whilesR : Com -> Type where
>   Remove_Me_No_whilesR : No_whilesR CSkip

> no_whiles_eqv : (no_whiles c = True) <-> (No_whilesR c)
> no_whiles_eqv = ?no_whiles_eqv_rhs

$\square$

==== Exercise: 4 starsM (no_whiles_terminating)

Imp programs that don't involve while loops always terminate. State and prove a
theorem \idr{no_whiles_terminating} that says this. Use either \idr{no_whiles}
or \idr{No_whilesR}, as you prefer.

> -- FILL IN HERE

$\square$

== Additional Exercises

==== Exercise: 3 stars (stack_compiler)

HP Calculators, programming languages like Forth and Postscript and abstract
machines like the Java Virtual Machine all evaluate arithmetic expressions using
a stack. For instance, the expression

```
      (2*3)+(3*(4-2))
```

would be entered as

```
      2 3 * 3 4 2 - * +
```

and evaluated like this (where we show the program being evaluated on the right
and the contents of the stack on the left):

```
      [ ]           |    2 3 * 3 4 2 - * +
      [2]           |    3 * 3 4 2 - * +
      [3, 2]        |    * 3 4 2 - * +
      [6]           |    3 4 2 - * +
      [3, 6]        |    4 2 - * +
      [4, 3, 6]     |    2 - * +
      [2, 4, 3, 6]  |    - * +
      [2, 3, 6]     |    * +
      [6, 6]        |    +
      [12]          |
```

The task of this exercise is to write a small compiler that translates
\idr{AExp}s into stack machine instructions.

The instruction set for our stack language will consist of the following
instructions:

  - \idr{SPush n}: Push the number \idr{n} on the stack.

  - \idr{SLoad x}: Load the identifier \idr{x} from the store and push it on the
    stack

  - \idr{SPlus}: Pop the two top numbers from the stack, add them, and push the
    result onto the stack.

  - \idr{SMinus}: Similar, but subtract.

  - \idr{SMult}: Similar, but multiply.

> data SInstr : Type where
>   SPush : Nat -> SInstr
>   SLoad : Id -> SInstr
>   SPlus : SInstr
>   SMinus : SInstr
>   SMult : SInstr

Write a function to evaluate programs in the stack language. It should take as
input a state, a stack represented as a list of numbers (top stack item is the
head of the list), and a program represented as a list of instructions, and it
should return the stack after executing the program. Test your function on the
examples below.

Note that the specification leaves unspecified what to do when encountering an
\idr{SPlus}, \idr{SMinus}, or \idr{SMult} instruction if the stack contains less
than two elements. In a sense, it is immaterial what we do, since our compiler
will never emit such a malformed program.

> s_execute : (st : State) -> (stack : List Nat) -> (prog : List SInstr) ->
>             List Nat
> s_execute st stack prog = ?s_execute_rhs

> s_execute1 : s_execute Imp.empty_state [] [SPush 5, SPush 3, SPush 1, SMinus]
>              = [2,5]
> s_execute1 = ?s_execute1_rhs

> s_execute2 : s_execute (t_update X 3 Imp.empty_state) [3,4]
>                        [SPush 4, SLoad X, SMult, SPlus]
>              = [15,4]
> s_execute2 = ?s_execute2_rhs

Next, write a function that compiles an \idr{AExp} into a stack machine program.
The effect of running the program should be the same as pushing the value of the
expression on the stack.

> s_compile : (e : AExp) -> List SInstr
> s_compile e = ?s_compile_rhs

After you've defined \idr{s_compile}, prove the following to test that it works.

> s_compile1 : s_compile (AMinus (AId X) (AMult (ANum 2) (AId Y)))
>              = [SLoad X, SPush 2, SLoad Y, SMult, SMinus]
> s_compile1 = ?s_compile1_rhs

$\square$

==== Exercise: 4 stars, advanced (stack_compiler_correct)

Now we'll prove the correctness of the compiler implemented in the previous
exercise. Remember that the specification left unspecified what to do when
encountering an \idr{SPlus}, \idr{SMinus}, or \idr{SMult} instruction if the
stack contains less than two elements. (In order to make your correctness proof
easier you might find it helpful to go back and change your implementation!)

Prove the following theorem. You will need to start by stating a more general
lemma to get a usable induction hypothesis; the main theorem will then be a
simple corollary of this lemma.

\ \todo[inline]{Tip: make parameters explicit in general lemma, or Idris will
get lost}

> s_compile_correct : (st : State) -> (e : AExp) -> s_execute st [] (s_compile e) = [aeval st e]
> s_compile_correct st e = ?s_compile_correct_rhs

$\square$

==== Exercise: 3 stars, optional (short_circuit)

\ \todo[inline]{This already happens since Idris's \idr{&&} short-circuits}

Most modern programming languages use a "short-circuit" evaluation rule for
boolean \idr{and}: to evaluate \idr{BAnd b1 b2}, first evaluate \idr{b1}. If it
evaluates to \idr{False}, then the entire \idr{BAnd} expression evaluates to
\idr{False} immediately, without evaluating \idr{b2}. Otherwise, \idr{b2} is
evaluated to determine the result of the \idr{BAnd} expression.

Write an alternate version of \idr{beval} that performs short-circuit
evaluation of \idr{BAnd} in this manner, and prove that it is equivalent to
\idr{beval}.

> -- FILL IN HERE

$\square$

==== Exercise: 4 stars, advanced (break_imp)

Imperative languages like C and Java often include a \idr{break} or similar
statement for interrupting the execution of loops. In this exercise we consider
how to add \idr{break} to Imp. First, we need to enrich the language of commands
with an additional case.

> namespace ComBreak

>   data ComB : Type where
>     CSkipB : ComB
>     CBreakB : ComB  -- <-- new
>     CAssB : Id -> AExp -> ComB
>     CSeqB : ComB -> ComB -> ComB
>     CIfB : BExp -> ComB -> ComB -> ComB
>     CWhileB : BExp -> ComB -> ComB

>   infix 5 ::=

>   SKIP : ComB
>   SKIP = CSkipB

>   BREAK : ComB
>   BREAK = CBreakB

>   (::=) : Id -> AExp -> ComB
>   (::=) = CAssB

>   (>>=) : ComB -> (() -> ComB) -> ComB
>   (>>=) c f = CSeqB c (f ())

>   WHILE : BExp -> ComB -> ComB
>   WHILE = CWhileB

>   syntax IFB [c1] THEN [c2] ELSE [c3] FI = CIfB c1 c2 c3

Next, we need to define the behavior of \idr{BREAK}. Informally, whenever
\idr{BREAK} is executed in a sequence of commands, it stops the execution of
that sequence and signals that the innermost enclosing loop should terminate.
(If there aren't any enclosing loops, then the whole program simply terminates.)
The final state should be the same as the one in which the \idr{BREAK} statement
was executed.

One important point is what to do when there are multiple loops enclosing a
given \idr{BREAK}. In those cases, \idr{BREAK} should only terminate the
_innermost_ loop. Thus, after executing the following...

```
       X ::= 0;;
       Y ::= 1;;
       WHILE not (0 == Y) DO
         WHILE TRUE DO
           BREAK
         END;;
         X ::= 1;;
         Y ::= Y - 1
       END
```

... the value of \idr{X} should be \idr{1}, and not \idr{0}.

One way of expressing this behavior is to add another parameter to the
evaluation relation that specifies whether evaluation of a command executes a
\idr{BREAK} statement:

>   data Result : Type where
>     SContinue : Result
>     SBreak : Result

Intuitively, \idr{c // st \\ s / st'} means that, if \idr{c} is started in state
\idr{st}, then it terminates in state \idr{st'} and either signals that the
innermost surrounding loop (or the whole program) should exit immediately
(\idr{s = SBreak}) or that execution should continue normally
(\idr{s = SContinue}).

The definition of the "\idr{c // st \\ s / st'}" relation is very similar to the
one we gave above for the regular evaluation relation (\idr{c / st \\ st'}) —
we just need to handle the termination signals appropriately:

  - If the command is \idr{SKIP}, then the state doesn't change and execution of
    any enclosing loop can continue normally.

  - If the command is \idr{BREAK}, the state stays unchanged but we signal a
    \idr{SBreak}.

  - If the command is an assignment, then we update the binding for that
    variable in the state accordingly and signal that execution can continue
    normally.

  - If the command is of the form \idr{IFB b THEN c1 ELSE c2 FI}, then the state
    is updated as in the original semantics of Imp, except that we also
    propagate the signal from the execution of whichever branch was taken.

  - If the command is a sequence \idr{c1 ;; c2}, we first execute \idr{c1}. If
    this yields a \idr{SBreak}, we skip the execution of \idr{c2} and propagate
    the \idr{SBreak} signal to the surrounding context; the resulting state is
    the same as the one obtained by executing \idr{c1} alone. Otherwise, we
    execute \idr{c2} on the state obtained after executing \idr{c1}, and
    propagate the signal generated there.

  - Finally, for a loop of the form \idr{WHILE b DO c END}, the semantics is
    almost the same as before. The only difference is that, when \idr{b}
    evaluates to \idr{True}, we execute \idr{c} and check the signal that it
    raises. If that signal is \idr{SContinue}, then the execution proceeds as in
    the original semantics. Otherwise, we stop the execution of the loop, and
    the resulting state is the same as the one resulting from the execution of
    the current iteration. In either case, since \idr{BREAK} only terminates the
    innermost loop, \idr{WHILE} signals \idr{SContinue}.

Based on the above description, complete the definition of the \idr{CEvalB}
relation.

>   data CEvalB : ComB -> State -> Result -> State -> Type where
>     E_SkipB : CEvalB CSkipB st SContinue st
>     -- FILL IN HERE

>   syntax [c1] "//" [st] "\\\\" [s] "/" [st'] = CEvalB c1 st s st'

Now prove the following properties of your definition of \idr{CEvalB}:

>   break_ignore : ((do BREAK; c) // st \\ s / st') -> st = st'
>   break_ignore x = ?break_ignore_rhs

>   while_continue : ((WHILE b c) // st \\ s / st') -> s = SContinue
>   while_continue x = ?while_continue_rhs

>   while_stops_on_break : beval st b = True ->
>                          (c // st \\ SBreak / st') ->
>                          ((WHILE b c) // st \\ SContinue / st')
>   while_stops_on_break prf x = ?while_stops_on_break_rhs

$\square$

==== Exercise: 3 stars, advanced, optional (while_break_true)

>   while_break_true : ((WHILE b c) // st \\ SContinue / st') ->
>                      beval st' b = True ->
>                      (st'' ** c // st'' \\ SBreak / st')
>   while_break_true x prf = ?while_break_true_rhs

$\square$

==== Exercise: 4 stars, advanced, optional (cevalB_deterministic)

These will come in handy in the following exercise:

>   Uninhabited (SBreak = SContinue) where
>     uninhabited Refl impossible
>
>   Uninhabited (SContinue = SBreak) where
>     uninhabited Refl impossible

>   cevalB_deterministic : (c // st \\ s1 / st1) ->
>                          (c // st \\ s2 / st2) ->
>                          (st1 = st2, s1 = s2)
>   cevalB_deterministic x y = ?cevalB_deterministic_rhs

$\square$

==== Exercise: 4 stars, optional (add_for_loop)

Add C-style \idr{for} loops to the language of commands, update the \idr{CEval}
definition to define the semantics of \idr{for} loops, and add cases for
\idr{for} loops as needed so that all the proofs in this file are accepted by
Idris.

A \idr{for} loop should be parameterized by (a) a statement executed initially,
(b) a test that is run on each iteration of the loop to determine whether the
loop should continue, (c) a statement executed at the end of each loop
iteration, and (d) a statement that makes up the body of the loop. (You don't
need to worry about making up a concrete notation for \idr{for} loops, but feel
free to play with this too if you like.)

> -- FILL IN HERE

$\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 Text.WebIDL.Types.Argument

import Data.Bitraversable
import Data.Bifoldable
import Data.Traversable
import Text.WebIDL.Types.Attribute
import Text.WebIDL.Types.Identifier
import Text.WebIDL.Types.Numbers
import Text.WebIDL.Types.StringLit
import Text.WebIDL.Types.Type
import Generics.Derive

%language ElabReflection

||| ConstValue ::
|||     BooleanLiteral
|||     FloatLiteral
|||     integer
|||
||| BooleanLiteral ::
|||     true
|||     false
public export
data ConstValue = B Bool | F FloatLit | I IntLit

%runElab derive "ConstValue" [Generic,Meta,Eq,Show,HasAttributes]

||| Default ::
|||     = DefaultValue
|||     ε
|||
||| (part of Default)] DefaultValue ::
|||     ConstValue
|||     string
|||     [ ]
|||     { }
|||     null
public export
data Default = None
             | EmptyList
             | EmptySet
             | Null
             | S StringLit
             | C ConstValue

%runElab derive "Default" [Generic,Meta,Eq,Show,HasAttributes]

||| ArgumentName ::
|||     ArgumentNameKeyword
|||     identifier
public export
record ArgumentName where
  constructor MkArgName
  value : String

%runElab derive "ArgumentName" [Generic,Meta,Eq,Show,HasAttributes]

public export
record ArgF (a : Type) (b : Type) where
  constructor MkArg
  attrs    : a
  type     : IdlTypeF a b
  name     : ArgumentName

%runElab derive "ArgF" [Generic,Meta,Eq,Show]

public export
Arg : Type
Arg = ArgF ExtAttributeList Identifier

public export
record OptArgF (a : Type) (b : Type) where
  constructor MkOptArg
  attrs     : a
  typeAttrs : a
  type      : IdlTypeF a b
  name      : ArgumentName
  def       : Default

%runElab derive "OptArgF" [Generic,Meta,Eq,Show]

public export
OptArg : Type
OptArg = OptArgF ExtAttributeList Identifier

||| ArgumentList ::
|||     Argument Arguments
|||     ε
|||
||| Arguments ::
|||     , Argument Arguments
|||     ε
|||
||| Argument ::
|||     ExtendedAttributeList ArgumentRest
|||
||| Ellipsis ::
|||     ...
|||     ε
||| ArgumentRest ::
|||     optional TypeWithExtendedAttributes ArgumentName Default
|||     Type Ellipsis ArgumentName
public export
data ArgumentListF : (a : Type) -> (b : Type) -> Type where
  VarArg :  (args : List $ ArgF a b)
         -> (vararg : ArgF a b)
         -> ArgumentListF a b

  NoVarArg :  (args : List $ ArgF a b)
           -> (optArgs : List $ OptArgF a b)
           -> ArgumentListF a b

%runElab derive "ArgumentListF" [Generic,Meta,Eq,Show]

public export
ArgumentList : Type
ArgumentList = ArgumentListF ExtAttributeList Identifier

--------------------------------------------------------------------------------
--          Implementations
--------------------------------------------------------------------------------

mutual
  export
  Bifunctor ArgF where bimap = assert_total bimapDefault

  export
  Bifoldable ArgF where bifoldr = bifoldrDefault

  export
  Bitraversable ArgF where
    bitraverse f g (MkArg a t n) =
      [| MkArg (f a) (bitraverse f g t) (pure n) |]

  export
  Functor (ArgF a) where map = bimap id

  export
  Foldable (ArgF a) where foldr = bifoldr (const id)

  export
  Traversable (ArgF a) where traverse = bitraverse pure

mutual
  export
  Bifunctor OptArgF where bimap = assert_total bimapDefault

  export
  Bifoldable OptArgF where bifoldr = bifoldrDefault

  export
  Bitraversable OptArgF where
    bitraverse f g (MkOptArg a1 a2 t n d) =
      [| MkOptArg (f a1) (f a2) (bitraverse f g t) (pure n) (pure d) |]

  export
  Functor (OptArgF a) where map = bimap id

  export
  Foldable (OptArgF a) where foldr = bifoldr (const id)

  export
  Traversable (OptArgF a) where traverse = bitraverse pure

mutual
  export
  Bifunctor ArgumentListF where bimap = assert_total bimapDefault

  export
  Bifoldable ArgumentListF where bifoldr = bifoldrDefault

  export
  Bitraversable ArgumentListF where
    bitraverse f g (VarArg as a) =
      [| VarArg (traverse (bitraverse f g) as) (bitraverse f g a) |]
    bitraverse f g (NoVarArg as os) =
      [| NoVarArg (traverse (bitraverse f g) as) (traverse (bitraverse f g) os) |]

  export
  Functor (ArgumentListF a) where map = bimap id

  export
  Foldable (ArgumentListF a) where foldr = bifoldr (const id)

  export
  Traversable (ArgumentListF a) where traverse = bitraverse pure

  export
  HasAttributes a => HasAttributes (ArgumentListF a b) where
    attributes = bifoldMap attributes (const Nil)

ext: idr


text:
module Submodule.DepC

import Submodule.DepD

empty : ()
empty = ()

max_stars_repo_name: chrrasmussen/Idris-Deps

max_issues_repo_name: chrrasmussen/Idris-Deps

max_forks_repo_name: chrrasmussen/Idris-Deps


text:
import Decidable.Equality

data Elem : a -> List a -> Type where
     Here : Elem x (x :: xs)
     There : (later : Elem x xs) -> Elem x (y :: xs)

data Last : List a -> a -> Type where
     LastOne : Last [value] value
     LastCons : (prf : Last xs value) -> Last (x :: xs) value

last123 : Last [1,2,3] 3
last123 = LastCons (LastCons LastOne)

isNotNill : Last [] value -> Void
isNotNill LastOne impossible
isNotNill (LastCons prf) impossible

isNotLastOne : (value = x -> Void) -> Last [x] value -> Void
isNotLastOne notLastOne LastOne = notLastOne Refl
isNotLastOne _ (LastCons prf) = isNotNill prf

notInTail : (xs = [] -> Void) ->
            (Last xs value -> Void) ->
            Last (x :: xs) value -> Void
notInTail hasMore noMore LastOne = hasMore Refl
notInTail hasMore noMore (LastCons later) = noMore later

isLast : DecEq a => (xs : List a) -> (value : a) -> Dec (Last xs value)
isLast [] value = No isNotNill
isLast (x :: xs) value
    = case decEq xs [] of
           Yes Refl => case decEq value x of
                            Yes Refl => Yes LastOne
                            No notLastOne => No (isNotLastOne notLastOne)
           No hasMore => case isLast xs value of
                              Yes prf => Yes (LastCons prf)
                              No noMore => No (notInTail hasMore noMore)


text:
module Minecraft.Base.PreClassic.Cobblestone

import public Minecraft.Core.Block.GenericData
import public Minecraft.Core.Entity.Pickup.GenericData
import public Minecraft.Core.Item.GenericData

%default total

public export
record Block where
  constructor MkBlock
  {auto base : GenericBlockData}

public export
record Item where
  constructor MkItem
  {auto base : GenericItemData}

public export
record ItemEntity where
  constructor MkItemEntity
  {auto base : GenericItemEntityData Cobblestone.Item}

max_stars_repo_name: po-stulate/postulate

max_issues_repo_name: po-stulate/postulate

max_forks_repo_name: po-stulate/postulate


text:
module Tests

import System
import Data.Strings             --isInfixOf
import Language.JSON
import Language.JSON.Data
import Language.JSON.Decode

test : String -> (() -> Either String Bool) -> IO ()
test name f = do
    putStrLn $ "Test: " ++ name
    case f () of
        Right _ => putStrLn "OK"
        Left err => do
            putStrLn $ "Failed: " ++ err
            exitFailure

--------------------------------------------------------------------------------
-- `int` tests
--------------------------------------------------------------------------------

testInt : Bool -> String -> Either String Bool
testInt val str =
    case (val, Language.JSON.Decode.decodeString int str) of
        (True, Right v) => Right True
        (True, Left err) => Left (show err)
        (False, Left err) => Right False
        (False, Right v) => Left $ "Expected to fail but succeeded: " ++ str

intTests : IO ()
intTests = do
    test "whole int" $ \() => testInt True "4"
    test "-whole int" $ \() => testInt True "-4"
    test "whole float" $ \() => testInt True "4.0"
    test "-whole float" $ \() => testInt True "-4.0"
    test "large int" $ \() => testInt True "1801439850948"
    test "-large int" $ \() => testInt True "-1801439850948"
    test "float" $ \() => testInt False "4.2"
    test "-float" $ \() => testInt False "-4.2"
    test "Infinity" $ \() => testInt False "Infinity"
    test "-Infinity" $ \() => testInt False "-Infinity"
    test "NaN" $ \() => testInt False "NaN"
    test "-NaN" $ \() => testInt False "-NaN"
    test "true" $ \() => testInt False "true"
    test "false" $ \() => testInt False "false"
    test "string" $ \() => testInt False "\"string\""
    test "object" $ \() => testInt False "{}"
    test "null" $ \() => testInt False "null"
    test "undefined" $ \() => testInt False "undefined"

--------------------------------------------------------------------------------
-- `field` tests
--------------------------------------------------------------------------------

||| A test JSON object
||| Note `parse (show t1json)` on the REPL is unusably slow (minutes...).  Use :exec putStrLn (show (<whatever>)) instead.
t1json : JSON
t1json = JObject [
                 ("foo", JNumber 42)
                 ,("bar", JArray [JNumber 2, JNumber 4, JNumber 6])
                 ,("baz", JObject [
                                 ("quux", JString "Hellow world!")
                                 ,("ary1", JArray [JString "alpha", JString "beta" ])
                                 ,("nobj", JObject [
                                                  ("ary2", JArray [JBoolean True, JBoolean False])
                                 ])
                 ])
                 ,("ary0", JArray [
                          JObject [
                                  ("aa", JNumber 22)
                                  ,("bb", JNumber 33)
                          ]
                 ])
       ]

||| Test that is expected to pass.
||| @expectedVal The value expected to be returned on success.
||| @actualVal The Either error message or actual value structure returned by the decoding function.
testPass : (Show a, Eq a) => (expectedVal : a) -> (actualVal : Either JSONError a) -> Either String Bool
testPass x (Left err) = Left $ "Failed: " ++ (show err)
testPass x (Right y) = if x == y
                         then Right True
                         else Left $ "expected " ++ (show x) ++ " got " ++ (show y)

||| Test that is expected to fail.
||| @expectedErr The error message expected to be triggered.
||| @actualVal The Either error message or actual value structure returned by the decoding function.
testFail : (Show a, Eq a) => (expectedErr : JSONError) -> (actualVal : Either JSONError a) -> Either String Bool
testFail x (Left err) = if x == err
                           then Right True -- expected error
                           else Left $ "wrong error, expected <" ++ (show x) ++ ">, got <" ++ (show err) ++ ">"
testFail _ (Right x) = Left $ "Expected to fail but succeeded: " ++ (show x)

||| Test related to field access.
fieldTests : IO ()
fieldTests = do
  -- test valid field access
  test "field exists, number, value same" $ \()
    => testPass 5 (field "foo" int (JObject [("foo", JNumber 5)]))
  test "field exists, string, value same" $ \()
    => testPass "hello" (field "foo" string (JObject [("foo", JString "hello")]))
  test "field exists, null, value same" $ \()
    => testPass True (field "foo" null (JObject [("foo", JNull)]))
  test "field exists, boolean, value same" $ \()
    => testPass False (field "foo" bol (JObject [("foo", JBoolean False)]))
  test "field exists, array, value same" $ \()
    => testPass [4,5,6]
      (field "foo" (list int) (JObject [("foo", JArray [JNumber 4, JNumber 5, JNumber 6])]))
  test "field exists, key/value pairs, value same" $ \()
    => testPass [("foo", [4,5,6]), ("alpha", [1,2,3]), ("delta", [7,8,9])]
      (keyValuePairs (list int) (JObject [("foo", JArray [JNumber 4, JNumber 5, JNumber 6]),
                                          ("alpha", JArray [JNumber 1, JNumber 2, JNumber 3]),
                                          ("delta", JArray [JNumber 7, JNumber 8, JNumber 9])]))

  -- test invalid field access
  test "field exists, wrong decoder type" $ \()
    => testFail (JSONTypeErr JTNumber JTString) (field "foo" int (JObject [("foo", JString "hello")]))

  test "field not exists, number" $ \()
    => testFail (JSONNoSuchField "bar" "{\n\"foo\": 5.0\n}") (field "bar" int (JObject [("foo", JNumber 5)]))

  -- test error generation when trying to access things which are not fields.
  test "filed of non-object, null" $ \()
    => testFail (JSONTypeErr JTObject JTNull) (field "foo" int (JNull))
  test "field of non-object, boolean" $ \()
    => testFail (JSONTypeErr JTObject JTBoolean) (field "foo" int (JBoolean True))
  test "field of non-object, number" $ \()
    => testFail (JSONTypeErr JTObject JTNumber) (field "foo" int (JNumber 5))
  test "field of non-object, string" $ \()
    => testFail (JSONTypeErr JTObject JTString) (field "foo" int (JString "hello"))
  test "field of non-object, array" $ \()
    => testFail (JSONTypeErr JTObject JTArray) (field "foo" int (JArray []))

--------------------------------------------------------------------------------
-- Other testing
--------------------------------------------------------------------------------

-- customTests : IO ()
-- customTests =
--     test "customDecoder preserves user error messages" $ \() => assertion
--     where
--         jsonString : String
--         jsonString = "{ \"foo\": \"bar\" }"

--         customErrorMessage : String
--         customErrorMessage = "I want to see this message!"

--         myDecoder : Decoder Int
--         myDecoder = andThen (\foo => fail customErrorMessage) (field "foo" string)

--         assertion : Either String Bool
--         assertion =
--             case decodeString myDecoder jsonString of
--                 Right _ =>
--                     Left $ "expected `customDecoder` to produce Left, but got Right"

--                 Left message =>
--                     if isInfixOf customErrorMessage message then
--                         Right True
--                     else
--                         Left $
--                             "expected `customDecoder` to preserve user's error message '"
--                                 ++ customErrorMessage
--                                 ++ "', but instead got: "
--                                 ++ message

export
tests : IO ()
tests = do
    intTests
    fieldTests
    --customTests

max_stars_repo_name: scotek/idris-json-decode

max_issues_repo_name: scotek/idris-json-decode

max_forks_repo_name: scotek/idris-json-decode


text:
-- ------------------------------------------------------------- [ Tibetan.idr ]
-- Module      : Text.Parse.Tibetan
-- Description : Parsers for Tibetan numerals.
-- --------------------------------------------------------------------- [ EOH ]
||| This module contains an integer parser for Tibetan numerals.
module Text.Parse.Tibetan

import public Data.Composition
import public Lightyear
import public Lightyear.Char
import public Lightyear.Strings

parseDigit : (Integral a) => Char -> a -> Parser a
parseDigit c i = do
  char c
  pure i

-- TODO figure out how to make this lazy
parseNumeral : Parser Int
parseNumeral = foldr (<|>) (parseDigit '༠' 0) $ zipWith parseDigit s (0::[1..10])
  where s = unpack "༠༡༢༣༤༥༦༧༨༩"

parseNumeralFake : Parser Int
parseNumeralFake = foldr (<|>) (parseDigit '0' 0) $ zipWith parseDigit s (0::[1..10])
  where s = unpack "0123456789"

parseLatin : Parser Int
parseLatin = do
  digits <- reverse <$> some parseNumeralFake
  (pure . (\x => div x 10) $ foldr ((*10) .* (+)) 0 digits) <?> "Tibetan integer"

||| A lightyear parser for Tibetan numerals.
export
parseNumber : Parser Int
parseNumber = do
  digits <- reverse <$> some parseNumeral
  (pure . (\x => div x 10) $ foldr ((*10) .* (+)) 0 digits) <?> "Tibetan integer"

||| Given a 'String', try to parse it as an integer written using Tibetan numerals. If this fails, return a 'String' explaining why.
export
readBo : String -> Either String Int
readBo = parse (parseNumber)

export
readTest : String -> Either String Int
readTest = parse parseLatin


text:
module Data.SOP.Utils

import Data.List
import Data.String

%default total

||| Type-level identity function.
public export
I : Type -> Type
I v = v

||| Type-level constant function.
public export
K : Type -> k -> Type
K t _ = t

--------------------------------------------------------------------------------
--          Interface Conversions
--------------------------------------------------------------------------------

||| Materializes an implicit value.
|||
||| This is useful for instance to convert a heterogeneous list of
||| `Ord` values to one of `Eq` values:
|||
||| ```idris example
||| ordToEqNP : NP (Ord . f) ks -> NP (Eq . f) ks
||| ordToEqNP = mapNP (\_ => materialize Eq)
||| ```
public export
materialize : (0 c : k -> Type) -> (instance : c v) => c v
materialize _ {instance} = instance

--------------------------------------------------------------------------------
--          Singleton Lists
--------------------------------------------------------------------------------

||| Witness that a list is actually a singleton list.
public export
data SingletonList : (vs : List a) -> Type where
  IsSingletonList : (v : a) -> SingletonList [v]

public export
Uninhabited (SingletonList []) where
  uninhabited v impossible

public export
Uninhabited (SingletonList $ a :: b :: t) where
  uninhabited v impossible

||| Covering function for singleton lists.
public export
singletonList : (vs : List a) -> Dec (SingletonList vs)
singletonList []              = No absurd
singletonList (v :: [])       = Yes (IsSingletonList v)
singletonList (_ :: (_ :: _)) = No absurd

--------------------------------------------------------------------------------
--          Updating Lists
--------------------------------------------------------------------------------

||| View for updating a single occurence of a value
||| in a list
public export
data UpdateOnce :  (t   : k)
                -> (t'  : k)
                -> (ks  : List k)
                -> (ks' : List k)
                -> Type where
  UpdateHere  : UpdateOnce t t' (t :: ks) (t' :: ks)
  UpdateThere : UpdateOnce t t' ks ks' -> UpdateOnce t t' (k :: ks) (k :: ks')

||| View for updating several occurences of a value
||| in a list
public export
data UpdateMany :  (t   : k)
                -> (t'  : k)
                -> (ks  : List k)
                -> (ks' : List k)
                -> Type where
  UMNil      : UpdateMany t t' [] []
  UMConsSame : UpdateMany t t' ks ks' -> UpdateMany t t' (t::ks) (t'::ks')
  UMConsDiff : UpdateMany t t' ks ks' -> UpdateMany t t' (k::ks) (k::ks')

--------------------------------------------------------------------------------
--          Sublists
--------------------------------------------------------------------------------

||| View of the second List containing all values (in the same order)
||| of the first List interleaved with arbitrary additional values.
public export
data Sublist : (ks : List k) -> (ks' : List k) -> Type where
  SLNil  : Sublist [] ks'
  SLSame : Sublist ks ks' -> Sublist (k::ks) (k::ks')
  SLDiff : Sublist ks ks' -> Sublist ks (k::ks')

--------------------------------------------------------------------------------
--          Enumerations
--------------------------------------------------------------------------------

||| Witness that a list of list of types (representing the
||| constructors and fields of an ADT) represents an enum type, i.e.
||| that all constructors are nullary.
public export
data EnumType : (kss : List $ List k) -> Type where
  EZ : EnumType Nil
  ES : EnumType kss -> EnumType ([] :: kss)

||| If `ks :: kss` is an enum type, then so is `kss`
public export
0 enumTail : EnumType (ks :: kss) -> EnumType kss
enumTail (ES x) = x

--------------------------------------------------------------------------------
--          Show Utilities
--------------------------------------------------------------------------------

export
dispStringList : List String -> String
dispStringList ss = "[" ++ fastConcat (intersperse "," ss) ++ "]"


text:
module Utils.Term

import System.FFI

%default total

libterm : String -> String
libterm s = "C:" ++ s ++ ", libidris2_support"

%foreign libterm "idris2_setupTerm"
prim__setupTerm : PrimIO ()

%foreign libterm "idris2_getTermCols"
prim__getTermCols : PrimIO Int

%foreign libterm "idris2_getTermLines"
prim__getTermLines : PrimIO Int

export
setupTerm : IO ()
setupTerm = primIO prim__setupTerm

export
getTermCols : IO Int
getTermCols = primIO prim__getTermCols

export
getTermLines : IO Int
getTermLines = primIO prim__getTermLines


text:
module Main

import Data.IOArray
import Data.String

big : Int
big = 200000

huge : Int
huge = 100000000

medium : Int
medium = 100000

small : Int
small = 4000

makeBigString : String -> IO ()
makeBigString s = do
  putStrLn ("string length is now " ++ (show $ strLength s))
  if strLength s > huge
     then putStrLn "max string length reached"
     else makeBigString (s ++ s)

main : IO ()
main = do
  arrLvl1 <- newArray small
  arrLvl2 <- newArray small
  ignore $ writeArray arrLvl1 42 arrLvl2
  arrLvl3 <- newArray small
  ignore $ writeArray arrLvl2 42 arrLvl3
  ignore $ writeArray arrLvl3 42 "The MAGIC string"

  med <- newArray medium
  ignore $ writeArray med 0 "first medium array element"
  ignore $ writeArray med (medium - 1) "last medium array element"
  ignore $ writeArray med (medium `div` 2) "somewhere in the middle (medium)"
  printLn =<< readArray med 0
  printLn =<< readArray med (medium - 1)
  printLn =<< readArray med (medium `div` 2)

  arr <- newArray big
  ignore $ writeArray arr 0 "first array element"
  ignore $ writeArray arr (big - 1) "last array element"
  ignore $ writeArray arr (big `div` 2) "somewhere in the middle"
  printLn =<< readArray arr 0
  printLn =<< readArray arr (big - 1)
  printLn =<< readArray arr (big `div` 2)

  makeBigString "Pi3ce"
  makeBigString "Pi3c"
  pure ()

  (Just readLvl2) <- readArray arrLvl1 42
    | Nothing => printLn "ERROR: lvl2 not found in lvl1"
  (Just readLvl3) <- readArray readLvl2 42
    | Nothing => printLn "ERROR: lvl3 not found in lvl2"
  (Just result) <- readArray readLvl3 42
    | Nothing => printLn "ERROR: result not found in lvl3"
  printLn result


text:
module CFT.Splits

import CFT
import Data.Vect

addToCorrectBucket : (value : a)
                  -> {n : Nat}
                  -> (choice : Ty (TyFromNat n) [])
                  -> (vect : Vect n (List a))
                  -> Vect n (List a)
addToCorrectBucket value {n = 0} choice [] = []
addToCorrectBucket value {n = (S k)} (Left Unit) (y :: xs) = (value :: y) :: xs
addToCorrectBucket value {n = (S k)} (Right x) (y :: xs) = y :: addToCorrectBucket value x xs

-- Split a list into `n` lists using a function that allows you to map each element
-- to its `n`th bucket
splitN : (n : Nat) -> (p : a -> Ty (TyFromNat n) []) -> List a -> Vect n (List a)
splitN n p [] = replicate n []
splitN n p (x :: xs) = let check = p x
                           rec = splitN n p xs in
                           addToCorrectBucket x check rec

fromBool : Bool -> Ty (TyFromNat 2) []
fromBool True = Left Unit
fromBool False = Right (Left Unit)

isEven : Nat -> Bool
isEven Z = True
isEven (S k) = not (isEven k)

splitTwoTest : Splits.splitN 2 (Splits.fromBool . Splits.isEven) [1 .. 4] === [[2,4], [1,3]]
splitTwoTest = Refl

--
-- DEFINING POLYNOMIALS
--
-- The goal is to have a type of polynomials that we are going to analyse and
-- see if we can split them into polynomials with 1 solution, 2 solutions or 0 solutions
record Polynomial where
  constructor MkPoly
  x2 : Int -- x squared term
  x : Int -- x term
  c : Int -- constant term

-- A polynomial a * x^2 + b * x + c has
-- 2 solutions if b^2 - 4*a*c > 0
-- 1 solution if b^2 - 4*a*c === 0
-- 0 solutions if b^2 - 4*a*c < 0
solutions : Polynomial -> Ty (TyFromNat 3) []
solutions (MkPoly a b c) =
  let v = b * b - 4 * a * c in
      if v > 0 then Left Unit -- 2 solutions
               else if v == 0 then Right (Left Unit) -- 1 solution
               else Right (Right (Left Unit)) -- no solutions

poly1 : Polynomial
poly1 = MkPoly 2 1 3 -- 0 solutions

poly2 : Polynomial
poly2 = MkPoly (-1) 2 3 -- 2 solutions

poly3 : Polynomial
poly3 = MkPoly 1 2 1 -- 1 solution

split3Test : splitN 3 Splits.solutions [Splits.poly1, Splits.poly2, Splits.poly3]
         === [[Splits.poly2],[Splits.poly3],[Splits.poly1]]
split3Test = Refl

max_stars_repo_name: andrevidela/dev-notes

max_issues_repo_name: andrevidela/dev-notes

max_forks_repo_name: andrevidela/dev-notes


text:
import Providers
-- import Data.HVect
-- import Data.Fin

%default total
%language TypeProviders

-- Enumerating observations, in order to be able to reason about
-- sequences, and to avoid introducing contradictory types.

-- Assumptions could depend on a few observations at once, so
-- something like lists of observations should be used instead of
-- single ones, and checks against permutations then, perhaps.

-- #, input, output
postulate blackbox : Integer -> Integer -> Integer

partial parseDigit : Char -> Integer
parseDigit '0' = 0
parseDigit '1' = 1
parseDigit '2' = 2
parseDigit '3' = 3
parseDigit '4' = 4
parseDigit '5' = 5
parseDigit '6' = 6
parseDigit '7' = 7
parseDigit '8' = 8
parseDigit '9' = 9

partial parseInt : String -> Integer
parseInt s = foldl (\x,y => 10*x + parseDigit y) 0 (unpack s)

partial parseState : String -> (Integer, Integer)
parseState s = case (words s) of
  [w1, w2] => (parseInt w1, parseInt w2)

partial experiment : Integer -> IO (Provider Type)
experiment inp = do
  val <- readFile "/tmp/black-box-test"
  (n, out) <- return $ parseState val
  fh <- openFile "/tmp/black-box-test" Write
  fwrite fh $ show (n + 1) ++ " " ++ show (out + inp)
  closeFile fh
  return (Provide (blackbox (n + 1) inp = (out + inp)))

%provide (first : Type) with (experiment 2)
%provide (second : Type) with (experiment 4)
%provide (third : Type) with (experiment 1)

alwaysIncreases' : blackbox num1 inp1 = out1 -> blackbox num2 inp2 = out2 -> Type
alwaysIncreases' {num1} {num2} {out1} {out2} b1 b2 = (if num1 <= num2 then out1 <= out2 else out2 <= out1) = True

increasesByInput' : blackbox num1 inp1 = out1 -> blackbox num2 inp2 = out2 -> Type
increasesByInput' {num1} {num2} {inp1} {inp2} {out1} {out2} b1 b2 = case (num1 == num2 - 1) of
  True => out2 = out1 + inp2
  False => case (num1 == num2 + 1) of
    True => out1 = out2 + inp1
    False => Unit

c1IncreasesByInput' : (b1:first) -> (b2:second) -> increasesByInput' b1 b2
c1IncreasesByInput' b1 b2 = Refl

c2IncreasesByInput' : (b1:first) -> (b2:second) -> increasesByInput' b2 b1
c2IncreasesByInput' b1 b2 = Refl

c3IncreasesByInput' : (b1:first) -> (b3:third) -> increasesByInput' b1 b3
c3IncreasesByInput' b1 b3 = MkUnit

max_stars_repo_name: defanor/black-box-reasoning

max_issues_repo_name: defanor/black-box-reasoning

max_forks_repo_name: defanor/black-box-reasoning


text:
module Main

import Control.Monad.Identity
import Control.Monad.Trans

import Data.Nat
import Data.String.Parser
import Data.String.Parser.Expression

%default partial

table : OperatorTable Nat
table =
  [ [ Infix (token "^" $> power ) AssocRight]
  , [ Infix (token "*" $> (*)   ) AssocLeft ]
  , [ Infix (token "+" $> (+)   ) AssocLeft ]
  ]

table' : OperatorTable Integer
table' =
  [ [ Infix (token "*" $> (*) ) AssocLeft
    , Infix (token "/" $> div ) AssocLeft
    ]
  , [ Infix (token "+" $> (+) ) AssocLeft
    , Infix (token "-" $> (-) ) AssocLeft
    ]
  ]

mutual
  term : Parser Nat
  term = lexeme (natural <|> expr)
         <?> "simple expression"

  expr : Parser Nat
  expr = buildExpressionParser Nat table term

mutual
  term' : Parser Integer
  term' = lexeme (integer <|> expr')
          <?> "simple expression"

  expr' : Parser Integer
  expr' = buildExpressionParser Integer table' term'

run : Show a => Parser a -> String -> IO ()
run p s = case parse (p <* eos) s of
                Left err => putStrLn err
                Right (xs, _) => printLn xs

main : IO ()
main = do run natural "5678"
          run integer "-3"
          run expr "1+4^3^2^1"
          run expr' "4 + 2 * 3"
          run expr' "13-3+1*2-10/2"


text:
module Toolkit.Decidable.Equality.Indexed

import public Decidable.Equality

%default total

public export
data Equals : (t : Type)
           -> (e : t -> Type)
           -> {i,j : t}
           -> (x : e i)
           -> (y : e j)
                -> Type
  where
    Same : {  i,j : t}
        -> {  x      : e i}
        -> {  y      : e j}
        -> (  prfIdx : i = j)
        -> (  prfVal : x = y)
                   -> Equals t e x y

public export
interface DecEq iTy
       => DecEqIdx (iTy : Type)
                   (eTy : iTy -> Type) | eTy
  where
     decEq : {i,j : iTy}
          -> (x : eTy i)
          -> (y : eTy j)
          -> (prf : i = j)
          -> Dec (Equals iTy eTy x y)

export
sym : {i,j : iTy}
   -> {a : eTy i}
   -> {b : eTy j}
   -> (rule : Equals iTy eTy a b) -> Equals iTy eTy b a
sym (Same Refl Refl) = Same Refl Refl

export
negEqSym : {i,j : iTy}
        -> {a : eTy i}
        -> {b : eTy j}
        -> (Equals iTy eTy a b -> Void)
        -> (Equals iTy eTy b a -> Void)
negEqSym p h = p (sym h)

export
trans : {i,j,k : iTy}
     -> {a : eTy i}
     -> {b : eTy j}
     -> {c : eTy k}
     -> (ab : Equals iTy eTy a b)
     -> (bc : Equals iTy eTy b c)
           -> Equals iTy eTy a c
trans {i = i} {j = i} {k = k} {a = a} {b = a} {c = c} (Same Refl Refl) bc with (bc)
  trans {i = i} {j = i} {k = i} {a = a} {b = a} {c = a} (Same Refl Refl) bc | (Same Refl Refl) = (Same Refl Refl)

namespace Index
  public export
  indexAreSame : {i,j : iTy}
              -> (contra : i = j -> Void)
              -> {x : eTy i}
              -> {y : eTy j}
              -> (prf    : Equals iTy eTy x y)
                        -> Void
  indexAreSame contra (Same Refl prfVal) = contra Refl

  public export
  decEq : {iTy : Type}
       -> {eTy : iTy -> Type}
       -> DecEqIdx iTy eTy
       => {i : iTy}
       -> {j : iTy}
       -> (x : eTy i)
       -> (y : eTy j)
       -> Dec (Equals iTy eTy x y)
  decEq x y {i} {j} {eTy} with (decEq i j)
    decEq x y {i = i} {j = i} {eTy = eTy} | (Yes Refl) = Indexed.decEq x y Refl
    decEq x y {i = i} {j = j} {eTy = eTy} | (No contra) = No (indexAreSame contra)

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

max_stars_repo_name: gallais/linear-circuits

max_issues_repo_name: gallais/linear-circuits

max_forks_repo_name: gallais/linear-circuits


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

module Text.Markup.Edda

import public Text.Markup.Edda.Model
import public Text.Markup.Edda.Walk
import public Text.Markup.Edda.Query

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

max_stars_repo_name: jfdm/edda

max_issues_repo_name: jfdm/edda

max_forks_repo_name: jfdm/edda


text:
module Input

import Command

%default total

public export
data Input : Type where
  Quit : Input
  RunProgram : Input
  AppendCommand : Command -> Input
  DeleteCommand : Input

getArrow : IO (Maybe Input)
getArrow = do
  c <- getChar
  pure $ case c of
           'A' => Just $ AppendCommand Forward
           'C' => Just $ AppendCommand TurnRight
           'D' => Just $ AppendCommand TurnLeft
           _   => Nothing

getSpecial : IO (Maybe Input)
getSpecial = do
  c <- getChar
  case c of
    '[' => getArrow
    _ => pure Nothing

export
getInput : IO (Maybe Input)
getInput = do
  c <- getChar
  case (ord c) of
    27 => getSpecial
    113 => pure $ Just Quit
    104 => pure $ Just $ AppendCommand TurnLeft
    108 => pure $ Just $ AppendCommand TurnRight
    106 => pure $ Just $ AppendCommand Forward
    13  => pure $ Just RunProgram
    127 => pure $ Just DeleteCommand
    _   => pure $ Nothing

max_stars_repo_name: PeterHajdu/tulis

max_issues_repo_name: PeterHajdu/tulis

max_forks_repo_name: PeterHajdu/tulis


text:
module Ratio

%access public export

-- TODO: This could probably all be better...

gcd : (Integral a, Abs a, Eq a) => a -> a -> a
gcd n m = gcd' (abs n) (abs m)
    where
        gcd' : a -> a -> a
        gcd' n m =
            if m == 0
                then n
                else gcd' m (n `mod` m)

nonZero : (Integral a, Eq a) => a -> Bool
nonZero n = n /= 0

infixl 7 .%
data Ratio : Type -> Type where
    (.%) : (Integral a, Eq a, Abs a, Ord a, Neg a) => a -> a -> Ratio a

infixl 7 :%
(:%) : (Integral a, Eq a, Abs a, Ord a, Neg a) =>
  a -> a -> Maybe (Ratio a)
(:%) n m =
  case m == 0 of
    False =>
        let cd = gcd n m
            num = (n `div` cd) -- TODO: Should be `quot`?
            den = (m `div` cd) -- TODO: Should be `quot`?
        in Just $ num .% den
    True => Nothing

Rational : Type
Rational = Ratio Integer

numerator : Ratio a -> a
numerator (n .% _) = n

denominator : Ratio a -> a
denominator (_ .% d) = d

Eq a => Eq (Ratio a) where
  (a .% b) == (c .% d) = (a * d) == (c * b)

Ord a => Ord (Ratio a) where
  compare (a .% b) (c .% d) = compare (a * d) (c * b)

rationalDiv : Ratio a -> Ratio a -> Maybe (Ratio a)
rationalDiv (a .% b) (c .% d) = (a * d) :% (b * c)

-- rationalMod : Ratio a -> Ratio a -> Maybe (Ratio a)
-- rationalMod a b = (a - b) * a `div` b

rationalAdd : Ratio a -> Ratio a -> Maybe (Ratio a)
rationalAdd (a .% b) (c .% d) = ((a * d) + (b * c)) :% (b * d)

rationalMul : Ratio a -> Ratio a -> Maybe (Ratio a)
rationalMul (a .% b) (c .% d) = (a * c) :% (b * d)

rationalFromInteger : Integer -> Maybe (Ratio Integer)
rationalFromInteger i = (fromInteger i) :% 1

rationalNegate : Ratio a -> Maybe (Ratio a)
rationalNegate (a .% b) = (negate a) :% b

rationalSub : Ratio a -> Ratio a -> Maybe (Ratio a)
rationalSub (a .% b) (c .% d) = ((a * d) - (c * b)) :% (b * d)

Show a => Show (Ratio a) where
    show (n .% d) = show n ++ " % " ++ show d

rationalCast : Rational -> Maybe Double
rationalCast (a .% b) =
  case b == 0 of
    False => Just $ (cast a) / (cast b)
    True => Nothing

max_stars_repo_name: ebenpack/lidrisp

max_issues_repo_name: ebenpack/lidrisp

max_forks_repo_name: ebenpack/lidrisp


text:
module TicTacToe.GameState

import TicTacToe.Player

%default total
%access export

public export
data EndState = Draw
              | Won Player

public export
data GameState = InPlay
               | Ended EndState

Show EndState where
  show Draw = "Draw"
  show (Won p) = "Won " ++ show p

Show GameState where
  show InPlay = "InPlay"
  show (Ended s) = "Ended " ++ show s

max_stars_repo_name: ShinKage/DT-TicTacToe

max_issues_repo_name: ShinKage/DT-TicTacToe

max_forks_repo_name: ShinKage/DT-TicTacToe


text:
module Basen

import Data.Fin

--Fin to Nat
tonatFin: (n: Nat) -> Fin(n) -> Nat
tonatFin (S k) FZ = Z
tonatFin (S k) (FS x) = S (tonatFin k x)

--List Fin to Nat
tonat: (n: Nat) -> List (Fin(n)) -> Nat
tonat n [] = Z
tonat n (x :: xs) = (tonatFin n x)*(power n (length xs)) + (tonat n xs)

--Euclid's div
Eucl: (a: Nat) -> (b: Nat) -> (Nat, Nat)
Eucl Z b = (0,0)
Eucl (S k) b = case (lte (S (S k)) b) of
                    False => (S(fst(Eucl (minus (S k) b) b)), snd(Eucl (minus (S k) b) b))
                    True => (0, S k)

--Nat to Fin (modular values)
tofinNat: (a: Nat) -> (n: Nat) -> Fin n
tofinNat Z (S j) = FZ
tofinNat (S k) (S j) = case lte (S k) (S j) of
                True => FS (tofinNat k j)
                False =>  (tofinNat (snd(Eucl (S k) (S j))) (S j))

--left strips FZ from lists
strp: List (Fin n) -> List (Fin n)
strp [] = []
strp (x :: xs) = case x of
                      FZ => strp(xs)
                      (FS y) => x::xs

-- Nat to List Fin n (base n representation)
tofin: Nat -> (n: Nat) -> List (Fin n)
tofin Z (S j) = [FZ]
tofin (S k) (S j) = strp(reverse(rem :: reverse(tofin q (S j)))) where
                    rem = tofinNat (snd(Eucl (S k) (S j))) (S j)
                    q = fst(Eucl (S k) (S j))

--adding two Fin n's
addfin: (n: Nat) -> Fin (S n) -> Fin (S n) -> Fin (S n) -> (Fin (S n), Fin (S n))
addfin n x y z = case (tofin ((tonatFin (S n) x)+ (tonatFin (S n) y) + (tonatFin (S n) z)) (S n)) of
                    [l] => (FZ, l)
                    [k, l] => (k,l)

--adding two reversed lists as specified
addfinl: (n: Nat) -> List (Fin (S n)) -> List (Fin (S n)) -> List (Fin (S n))
addfinl n [] ys = strp(ys)
addfinl n (x :: xs) [] = strp(x::xs)
addfinl n (x :: xs) (y :: ys) = (snd(addfin n FZ x y)::(addfinl n (addfinl n [fst(addfin n FZ x y)] xs) ys))

--adding two lists
addfinlist: (n: Nat) -> List (Fin (S n)) -> List (Fin (S n)) -> List (Fin (S n))
addfinlist n xs ys = reverse(addfinl n (reverse xs) (reverse ys))

--embedding Fin n in Fin S n vertically
embn: (n: Nat) -> Fin n -> Fin (S n)
embn (S k) FZ = FZ
embn (S k) (FS x) = FS (embn k x)

--Unused mulfinNat - multiplies two Fin n's
mulfinNat: (n: Nat) -> Fin (n) -> Fin (n) -> (Fin (n), Fin (n))
mulfinNat (S n) x y =  case tofin ((tonatFin (S n) x)*(tonatFin (S n) y)) (S n) of
                    [l] => (FZ, l)
                    [k,l] => (k,l)

--multiply two reversed lists in Fin S n
mulfinl: (n: Nat) -> List (Fin (S n)) -> List (Fin (S n)) -> List (Fin (S n))
mulfinl n xs [] = []
mulfinl n xs (FZ :: ys) = FZ :: (mulfinl n xs ys)
mulfinl n xs ((FS x) :: ys) = addfinl n (mulfinl n xs ((embn n x)::ys)) xs

--multpily two lists
mulfinList: (n: Nat) -> List (Fin (S n)) -> List (Fin (S n)) -> List (Fin (S n))
mulfinList n xs ys = reverse(mulfinl n (reverse xs) (reverse ys))


text:
module Compiler.Jvm.ExtPrim

import Core.Context
import Core.Name

||| Extended primitives for the scheme backend, outside the standard set of primFn
public export
data ExtPrim = JvmStaticMethodCall | JvmInstanceMethodCall
             | NewIORef | ReadIORef | WriteIORef
             | NewArray | ArrayGet | ArraySet
             | GetField | SetField
             | VoidElim
             | SysOS | SysCodegen
             | MakeFuture
             | Unknown Name

export
Show ExtPrim where
  show JvmStaticMethodCall = "JvmStaticMethodCall"
  show JvmInstanceMethodCall = "JvmInstanceMethodCall"
  show NewIORef = "NewIORef"
  show ReadIORef = "ReadIORef"
  show WriteIORef = "WriteIORef"
  show NewArray = "NewArray"
  show ArrayGet = "ArrayGet"
  show ArraySet = "ArraySet"
  show GetField = "GetField"
  show SetField = "SetField"
  show VoidElim = "VoidElim"
  show SysOS = "SysOS"
  show SysCodegen = "SysCodegen"
  show MakeFuture = "MakeFuture"
  show (Unknown n) = "Unknown " ++ show n

||| Match on a user given name to get the scheme primitive
export
toPrim : Name -> ExtPrim
toPrim pn@(NS _ n)
    = cond [(n == UN (Basic "prim__jvmStatic"), JvmStaticMethodCall),
            (n == UN (Basic "prim__jvmInstance"), JvmInstanceMethodCall),
            (n == UN (Basic "prim__newIORef"), NewIORef),
            (n == UN (Basic "prim__readIORef"), ReadIORef),
            (n == UN (Basic "prim__writeIORef"), WriteIORef),
            (n == UN (Basic "prim__newArray"), NewArray),
            (n == UN (Basic "prim__arrayGet"), ArrayGet),
            (n == UN (Basic "prim__arraySet"), ArraySet),
            (n == UN (Basic "prim__getField"), GetField),
            (n == UN (Basic "prim__setField"), SetField),
            (n == UN (Basic "void"), VoidElim),
            (n == UN (Basic "prim__os"), SysOS),
            (n == UN (Basic "prim__codegen"), SysCodegen),
            (n == UN (Basic "prim__makeFuture"), MakeFuture)
            ]
           (Unknown pn)
toPrim pn = Unknown pn


text:
{- Ctrl-Alt-A: Add definition
   Ctrl-Alt-C: Case split
   Ctrl-Alt-D: Documentation
   Ctrl-Alt-L: Lift hole: Lifts a hole to the top level as a new function definition
   Ctrl-Alt-M: Match: Replaces a hole with a case expression that matches on an intermediate result
   Ctrl-Alt-R: Reloads and typechecks the current buffer
   Ctrl-Alt-S: Search
   Ctrl-Alt-T: Type-check: Displays the type under cursor -}
module Main

import Data.Vect

data WorldState : (guesses_remaning : Nat) -> (letters : Nat) -> Type where
  MkWorldState : (word : String) ->
                 (missing : Vect letters Char) ->
                 WorldState guesses_remaning letters

data Finished : Type where
  Lost : (game : WorldState 0 (S letters)) -> Finished
  Won  : (game : WorldState (S letters) 0) -> Finished

data ValidInput : List Char -> Type where
  Letter : (c : Char) -> ValidInput [c]

isValidNil : ValidInput [] -> Void
isValidNil (Letter _) impossible

isValidMore : ValidInput (x :: (y :: ys)) -> Void
isValidMore (Letter _) impossible

isValidInput : (cs : List Char) -> Dec (ValidInput cs)
isValidInput [] = No isValidNil
isValidInput (x :: []) = Yes (Letter x)
isValidInput (x :: (y :: ys)) = No isValidMore

isValidString : (s : String) -> Dec (ValidInput (unpack s))
isValidString s = isValidInput (unpack s)

readGuess : IO (x ** ValidInput x)
readGuess = do
  putStr "Guess:"
  x <- getLine
  case isValidString (toUpper x) of
    Yes prf => pure (_ ** prf)
    No contra => do putStrLn "Invalid guess"
                    readGuess

processGuess : (letter : Char) ->
               WorldState (S guesses) (S letters) ->
               Either (WorldState guesses (S letters))
                      (WorldState (S guesses) letters)
processGuess letter (MkWorldState word missing) = case isElem letter missing of
  (Yes elem) => Right (MkWorldState word (dropElem missing elem))
  (No contra) => Left (MkWorldState word missing)

game : WorldState (S guesses) (S letters) -> IO Finished
game {guesses} {letters} st = do
  (_ ** Letter letter) <- readGuess
  case processGuess letter st of
    Left badGuess => do putStrLn "Wrong!"
                        case guesses of
                          Z => pure (Lost badGuess)
                          S _ => game badGuess
    Right goodGuess => do putStrLn "Right!"
                          case letters of
                            Z => pure (Won goodGuess)
                            S _ => game goodGuess

main : IO ()
main = do
  result <- game {guesses = 2} (MkWorldState "Test" ['T', 'E', 'S'])
  case result of
    Lost (MkWorldState word missing) =>
      putStrLn ("You lose. The word was " ++ word)
    Won (MkWorldState word missing) =>
      putStrLn "You win!"

max_stars_repo_name: pdani/idris-grin

max_issues_repo_name: pdani/idris-grin

max_forks_repo_name: pdani/idris-grin