text:
(** * Smallstep: Small-step Operational Semantics *)

> ||| Smallstep: Small-step Operational Semantics
> module Smallstep
>
> %access public export
>

(** The evaluators we have seen so far (for [aexp]s, [bexp]s,
    commands, ...) have been formulated in a "big-step" style: they
    specify how a given expression can be evaluated to its final
    value (or a command plus a store to a final store) "all in one big
    step."

    This style is simple and natural for many purposes -- indeed,
    Gilles Kahn, who popularized it, called it _natural semantics_.
    But there are some things it does not do well.  In particular, it
    does not give us a natural way of talking about _concurrent_
    programming languages, where the semantics of a program -- i.e.,
    the essence of how it behaves -- is not just which input states
    get mapped to which output states, but also includes the
    intermediate states that it passes through along the way, since
    these states can also be observed by concurrently executing code.

    Another shortcoming of the big-step style is more technical, but
    critical in many situations.  Suppose we want to define a variant
    of Imp where variables could hold _either_ numbers _or_ lists of
    numbers.  In the syntax of this extended language, it will be
    possible to write strange expressions like [2 + nil], and our
    semantics for arithmetic expressions will then need to say
    something about how such expressions behave.  One possibility is
    to maintain the convention that every arithmetic expressions
    evaluates to some number by choosing some way of viewing a list as
    a number -- e.g., by specifying that a list should be interpreted
    as [0] when it occurs in a context expecting a number.  But this
    is really a bit of a hack.

    A much more natural approach is simply to say that the behavior of
    an expression like [2+nil] is _undefined_ -- i.e., it doesn't
    evaluate to any result at all.  And we can easily do this: we just
    have to formulate [aeval] and [beval] as [Inductive] propositions
    rather than Fixpoints, so that we can make them partial functions
    instead of total ones.

    Now, however, we encounter a serious deficiency.  In this
    language, a command might fail to map a given starting state to
    any ending state for _two quite different reasons_: either because
    the execution gets into an infinite loop or because, at some
    point, the program tries to do an operation that makes no sense,
    such as adding a number to a list, so that none of the evaluation
    rules can be applied.

    These two outcomes -- nontermination vs. getting stuck in an
    erroneous configuration -- should not be confused.  In particular, we
    want to _allow_ the first (permitting the possibility of infinite
    loops is the price we pay for the convenience of programming with
    general looping constructs like [while]) but _prevent_ the
    second (which is just wrong), for example by adding some form of
    _typechecking_ to the language.  Indeed, this will be a major
    topic for the rest of the course.  As a first step, we need a way
    of presenting the semantics that allows us to distinguish
    nontermination from erroneous "stuck states."

    So, for lots of reasons, we'd often like to have a finer-grained
    way of defining and reasoning about program behaviors.  This is
    the topic of the present chapter.  Our goal is to replace the
    "big-step" [eval] relation with a "small-step" relation that
    specifies, for a given program, how the "atomic steps" of
    computation are performed. *)

(* ################################################################# *)
(** * A Toy Language *)

(** To save space in the discussion, let's go back to an
    incredibly simple language containing just constants and
    addition.  (We use single letters -- [C] and [P] (for Constant and
    Plus) -- as constructor names, for brevity.)  At the end of the
    chapter, we'll see how to apply the same techniques to the full
    Imp language.  *)

> data Tm : Type where
>   C : Nat -> Tm         -- Constant
>   P : Tm -> Tm -> Tm    -- Plus

(** Here is a standard evaluator for this language, written in
    the big-step style that we've been using up to this point. *)

> evalF : (t : Tm) -> Nat
> evalF (C n) = n
> evalF (P a1 a2) = evalF a1 + evalF a2

(** Here is the same evaluator, written in exactly the same
    style, but formulated as an inductively defined relation.  Again,
    we use the notation [t \\ n] for "[t] evaluates to [n]." *)
(**

                               --------                                (E_Const)
                               C n \\ n

                               t1 \\ n1
                               t2 \\ n2
                           ------------------                          (E_Plus)
                           P t1 t2 \\ n1 + n2
*)

Reserved Notation " t '\\' n " (at level 50, left associativity).

> mutual
>   infixl 6 #
>   (#) : Tm -> Nat -> Type
>   (#) = Eval
>
>   data Eval : Tm -> Nat -> Type where
>     E_Const : C n # n
>     E_Plus  : t1 # n1 -> t2 # n2 -> P t1 t2 # n1 + n2
>

Module SimpleArith1.

> namespace SimpleArith1

(** Now, here is the corresponding _small-step_ evaluation relation. *)
(**
                     -------------------------------        (ST_PlusConstConst)
                     P (C n1) (C n2) ==> C (n1 + n2)

                              t1 ==> t1'
                         --------------------                        (ST_Plus1)
                         P t1 t2 ==> P t1' t2

                              t2 ==> t2'
                      ---------------------------                    (ST_Plus2)
                      P (C n1) t2 ==> P (C n1) t2'
*)

Reserved Notation " t '==>' t' " (at level 40).

>   mutual
>     infixl 6 >=>
>     (>=>) : Tm -> Tm -> Type
>     (>=>) = Step
>
>     data Step : Tm -> Tm -> Type where
>       ST_PlusConstConst : P (C n1) (C n2) >=> C (n1 + n2)
>       ST_Plus1 : t1 >=> t1' -> P t1 t2 >=> P t1' t2
>       ST_Plus2 : t2 >=> t2' -> P (C n1) t2 >=> P (C n1) t2'
>

(** Things to notice:

    - We are defining just a single reduction step, in which
      one [P] node is replaced by its value.

    - Each step finds the _leftmost_ [P] node that is ready to
      go (both of its operands are constants) and rewrites it in
      place.  The first rule tells how to rewrite this [P] node
      itself; the other two rules tell how to find it.

    - A term that is just a constant cannot take a step. *)

(** Let's pause and check a couple of examples of reasoning with
    the [step] relation... *)

(** If [t1] can take a step to [t1'], then [P t1 t2] steps
    to [P t1' t2]: *)

>   test_step_1 :
>      P
>        (P (C 0) (C 3))
>        (P (C 2) (C 4))
>      >=>
>      P
>        (C (0 + 3))
>        (P (C 2) (C 4))
>   test_step_1  = ST_Plus1 ST_PlusConstConst

(** **** Exercise: 1 star (test_step_2)  *)
(** Right-hand sides of sums can take a step only when the
    left-hand side is finished: if [t2] can take a step to [t2'],
    then [P (C n) t2] steps to [P (C n)
    t2']: *)

>   test_step_2 :
>      P
>        (C 0)
>        (P
>          (C 2)
>          (P (C 0) (C 3)))
>      >=>
>      P
>        (C 0)
>        (P
>          (C 2)
>          (C (0 + 3)))
>   test_step_2 = ST_Plus2 (ST_Plus2 ST_PlusConstConst)

End SimpleArith1.

(* ################################################################# *)
(** * Relations *)

(** We will be working with several different single-step relations,
    so it is helpful to generalize a bit and state a few definitions
    and theorems about relations in general.  (The optional chapter
    [Rel.v] develops some of these ideas in a bit more detail; it may
    be useful if the treatment here is too dense.)

    A _binary relation_ on a set [X] is a family of propositions
    parameterized by two elements of [X] -- i.e., a proposition about
    pairs of elements of [X].  *)

Definition relation (X: Type) := X -> X -> Prop.

> Relation : Type -> Type
> Relation t = t -> t -> Type

(** Our main examples of such relations in this chapter will be
    the single-step reduction relation, [==>], and its multi-step
    variant, [==>*] (defined below), but there are many other
    examples -- e.g., the "equals," "less than," "less than or equal
    to," and "is the square of" relations on numbers, and the "prefix
    of" relation on lists and strings. *)

(** One simple property of the [==>] relation is that, like the
    big-step evaluation relation for Imp, it is _deterministic_.

    _Theorem_: For each [t], there is at most one [t'] such that [t]
    steps to [t'] ([t ==> t'] is provable).  This is the
    same as saying that [==>] is deterministic. *)

(** _Proof sketch_: We show that if [x] steps to both [y1] and
    [y2], then [y1] and [y2] are equal, by induction on a derivation
    of [step x y1].  There are several cases to consider, depending on
    the last rule used in this derivation and the last rule in the
    given derivation of [step x y2].

      - If both are [ST_PlusConstConst], the result is immediate.

      - The cases when both derivations end with [ST_Plus1] or
        [ST_Plus2] follow by the induction hypothesis.

      - It cannot happen that one is [ST_PlusConstConst] and the other
        is [ST_Plus1] or [ST_Plus2], since this would imply that [x]
        has the form [P t1 t2] where both [t1] and [t2] are
        constants (by [ST_PlusConstConst]) _and_ one of [t1] or [t2]
        has the form [P _].

      - Similarly, it cannot happen that one is [ST_Plus1] and the
        other is [ST_Plus2], since this would imply that [x] has the
        form [P t1 t2] where [t1] has both the form [P t11 t12] and the
        form [C n]. [] *)

(** Formally: *)

Definition deterministic {X: Type} (R: relation X) :=
  forall x y1 y2 : X, R x y1 -> R x y2 -> y1 = y2.

> deterministic : {xt: Type} -> (r: Relation xt) -> Type
> deterministic {xt} r = {x, y1, y2: xt} -> r x y1 -> r x y2 -> y1 = y2

Module SimpleArith2.
Import SimpleArith1.

> namespace SimpleArith2

>   step_deterministic : deterministic Step
>   step_deterministic ST_PlusConstConst hyp =
>     case hyp of
>       ST_PlusConstConst => Refl
>       ST_Plus1 _ impossible
>       ST_Plus2 _ impossible
>   step_deterministic (ST_Plus1 l) hyp =
>     case hyp of
>       ST_PlusConstConst impossible
>       ST_Plus1 l' => rewrite step_deterministic l l' in Refl
>       ST_Plus2 _ impossible
>   step_deterministic (ST_Plus2 r) hyp =
>     case hyp of
>       ST_PlusConstConst impossible
>       ST_Plus1 _ impossible
>       ST_Plus2 r' => rewrite step_deterministic r r' in Refl

Theorem step_deterministic:
  deterministic step.
Proof.
  unfold deterministic. intros x y1 y2 Hy1 Hy2.
  generalize dependent y2.
  induction Hy1; intros y2 Hy2.
    - (* ST_PlusConstConst *) inversion Hy2.
      + (* ST_PlusConstConst *) reflexivity.
      + (* ST_Plus1 *) inversion H2.
      + (* ST_Plus2 *) inversion H2.
    - (* ST_Plus1 *) inversion Hy2.
      + (* ST_PlusConstConst *)
        rewrite <- H0 in Hy1. inversion Hy1.
      + (* ST_Plus1 *)
        rewrite <- (IHHy1 t1'0).
        reflexivity. assumption.
      + (* ST_Plus2 *)
        rewrite <- H in Hy1. inversion Hy1.
    - (* ST_Plus2 *) inversion Hy2.
      + (* ST_PlusConstConst *)
        rewrite <- H1 in Hy1. inversion Hy1.
      + (* ST_Plus1 *) inversion H2.
      + (* ST_Plus2 *)
        rewrite <- (IHHy1 t2'0).
        reflexivity. assumption.
Qed.

End SimpleArith2.

(** There is some annoying repetition in this proof.  Each use of
    [inversion Hy2] results in three subcases, only one of which is
    relevant (the one that matches the current case in the induction
    on [Hy1]).  The other two subcases need to be dismissed by finding
    the contradiction among the hypotheses and doing inversion on it.

    The following custom tactic, called [solve_by_inverts], can be
    helpful in such cases.  It will solve the goal if it can be solved
    by inverting some hypothesis; otherwise, it fails. *)

Ltac solve_by_inverts n :=
  match goal with | H : ?T |- _ =>
  match type of T with Prop =>
    solve [
      inversion H;
      match n with S (S (?n')) => subst; solve_by_inverts (S n') end ]
  end end.

(** The details of how this works are not important for now, but it
    illustrates the power of Coq's [Ltac] language for
    programmatically defining special-purpose tactics.  It looks
    through the current proof state for a hypothesis [H] (the first
    [match]) of type [Prop] (the second [match]) such that performing
    inversion on [H] (followed by a recursive invocation of the same
    tactic, if its argument [n] is greater than one) completely solves
    the current goal.  If no such hypothesis exists, it fails.

    We will usually want to call [solve_by_inverts] with argument
    [1] (especially as larger arguments can lead to very slow proof
    checking), so we define [solve_by_invert] as a shorthand for this
    case. *)

Ltac solve_by_invert :=
  solve_by_inverts 1.

(** Let's see how a proof of the previous theorem can be simplified
    using this tactic... *)

Module SimpleArith3.
Import SimpleArith1.

Theorem step_deterministic_alt: deterministic step.
Proof.
  intros x y1 y2 Hy1 Hy2.
  generalize dependent y2.
  induction Hy1; intros y2 Hy2;
    inversion Hy2; subst; try solve_by_invert.
  - (* ST_PlusConstConst *) reflexivity.
  - (* ST_Plus1 *)
    apply IHHy1 in H2. rewrite H2. reflexivity.
  - (* ST_Plus2 *)
    apply IHHy1 in H2. rewrite H2. reflexivity.
Qed.

End SimpleArith3.

(* ================================================================= *)
(** ** Values *)

(** Next, it will be useful to slightly reformulate the
    definition of single-step reduction by stating it in terms of
    "values." *)

(** It is useful to think of the [==>] relation as defining an
    _abstract machine_:

      - At any moment, the _state_ of the machine is a term.

      - A _step_ of the machine is an atomic unit of computation --
        here, a single "add" operation.

      - The _halting states_ of the machine are ones where there is no
        more computation to be done. *)

(** We can then execute a term [t] as follows:

      - Take [t] as the starting state of the machine.

      - Repeatedly use the [==>] relation to find a sequence of
        machine states, starting with [t], where each state steps to
        the next.

      - When no more reduction is possible, "read out" the final state
        of the machine as the result of execution. *)

(** Intuitively, it is clear that the final states of the
    machine are always terms of the form [C n] for some [n].
    We call such terms _values_. *)

Inductive value : tm -> Prop :=
  | v_const : forall n, value (C n).

> data Value : Tm -> Type where
>   V_const : (n : Nat) -> Value (C n)
>

(** Having introduced the idea of values, we can use it in the
    definition of the [==>] relation to write [ST_Plus2] rule in a
    slightly more elegant way: *)

(**
                     -------------------------------        (ST_PlusConstConst)
                     P (C n1) (C n2) ==> C (n1 + n2)

                              t1 ==> t1'
                         --------------------                        (ST_Plus1)
                         P t1 t2 ==> P t1' t2

                               value v1
                              t2 ==> t2'
                         --------------------                        (ST_Plus2)
                         P v1 t2 ==> P v1 t2'
*)
(** Again, the variable names here carry important information:
    by convention, [v1] ranges only over values, while [t1] and [t2]
    range over arbitrary terms.  (Given this convention, the explicit
    [value] hypothesis is arguably redundant.  We'll keep it for now,
    to maintain a close correspondence between the informal and Coq
    versions of the rules, but later on we'll drop it in informal
    rules for brevity.) *)

(**  Here are the formal rules: *)

Reserved Notation " t '==>' t' " (at level 40).

Inductive step : tm -> tm -> Prop :=
  | ST_PlusConstConst : forall n1 n2,
          P (C n1) (C n2)
      ==> C (n1 + n2)
  | ST_Plus1 : forall t1 t1' t2,
        t1 ==> t1' ->
        P t1 t2 ==> P t1' t2
  | ST_Plus2 : forall v1 t2 t2',
        value v1 ->                     (* <----- n.b. *)
        t2 ==> t2' ->
        P v1 t2 ==> P v1 t2'

  where " t '==>' t' " := (step t t').

> mutual
>   infixl 6 >>>
>   (>>>) : Tm -> Tm -> Type
>   (>>>) = Smallstep.Step
>
>   data Step : Tm -> Tm -> Type where
>     ST_PlusConstConst : P (C n1) (C n2) >>> C (n1 + n2)
>     ST_Plus1 : t1 >>> t1' -> P t1 t2 >>> P t1' t2
>     ST_Plus2 : Value v1 -> t2 >>> t2' -> P v1 t2 >>> P v1 t2'

(** **** Exercise: 3 stars, recommended (redo_determinism)  *)
(** As a sanity check on this change, let's re-verify determinism.

    _Proof sketch_: We must show that if [x] steps to both [y1] and
    [y2], then [y1] and [y2] are equal.  Consider the final rules used
    in the derivations of [step x y1] and [step x y2].

    - If both are [ST_PlusConstConst], the result is immediate.

    - It cannot happen that one is [ST_PlusConstConst] and the other
      is [ST_Plus1] or [ST_Plus2], since this would imply that [x] has
      the form [P t1 t2] where both [t1] and [t2] are constants (by
      [ST_PlusConstConst]) _and_ one of [t1] or [t2] has the form [P _].

    - Similarly, it cannot happen that one is [ST_Plus1] and the other
      is [ST_Plus2], since this would imply that [x] has the form [P
      t1 t2] where [t1] both has the form [P t11 t12] and is a
      value (hence has the form [C n]).

    - The cases when both derivations end with [ST_Plus1] or
      [ST_Plus2] follow by the induction hypothesis. [] *)

(** Most of this proof is the same as the one above.  But to get
    maximum benefit from the exercise you should try to write your
    formal version from scratch and just use the earlier one if you
    get stuck. *)

Theorem step_deterministic :
  deterministic step.
Proof.
  (* FILL IN HERE *) Admitted.
(** [] *)

(* ================================================================= *)
(** ** Strong Progress and Normal Forms *)

(** The definition of single-step reduction for our toy language
    is fairly simple, but for a larger language it would be easy to
    forget one of the rules and accidentally create a situation where
    some term cannot take a step even though it has not been
    completely reduced to a value.  The following theorem shows that
    we did not, in fact, make such a mistake here. *)

(** _Theorem_ (_Strong Progress_): If [t] is a term, then either [t]
    is a value or else there exists a term [t'] such that [t ==> t']. *)

(** _Proof_: By induction on [t].

    - Suppose [t = C n]. Then [t] is a value.

    - Suppose [t = P t1 t2], where (by the IH) [t1] either is a value
      or can step to some [t1'], and where [t2] is either a value or
      can step to some [t2']. We must show [P t1 t2] is either a value
      or steps to some [t'].

      - If [t1] and [t2] are both values, then [t] can take a step, by
        [ST_PlusConstConst].

      - If [t1] is a value and [t2] can take a step, then so can [t],
        by [ST_Plus2].

      - If [t1] can take a step, then so can [t], by [ST_Plus1].  []

   Or, formally: *)

Theorem strong_progress : forall t,
  value t \/ (exists t', t ==> t').
Proof.
  induction t.
    - (* C *) left. apply v_const.
    - (* P *) right. inversion IHt1.
      + (* l *) inversion IHt2.
        * (* l *) inversion H. inversion H0.
          exists (C (n + n0)).
          apply ST_PlusConstConst.
        * (* r *) inversion H0 as [t' H1].
          exists (P t1 t').
          apply ST_Plus2. apply H. apply H1.
      + (* r *) inversion H as [t' H0].
          exists (P t' t2).
          apply ST_Plus1. apply H0.  Qed.

>  strong_progress : (t: Tm) -> Either (Value t) (t': Tm ** t >=> t')
>  strong_progress (C n) = Left (V_const n)
>  strong_progress (P l r) = Right (
>     case l of
>       (C n) => case r of
>         (C n')  => (C (n + n') ** ST_PlusConstConst)
>         (P l' r') =>
>           let indHyp = strong_progress (P (C n) r')
>           in case indHyp of
>             Right ir => ?hole -- (P (C n) (P l r) ** ?hole) -- ST_Plus2 (P l r ** ir))
>             Left il => ?hole02
>       (P l' r') => case r of
>         (C n)  => ?hole11
>         (P l'' r'') => ?hole12
>   )

(** This important property is called _strong progress_, because
    every term either is a value or can "make progress" by stepping to
    some other term.  (The qualifier "strong" distinguishes it from a
    more refined version that we'll see in later chapters, called
    just _progress_.) *)

(** The idea of "making progress" can be extended to tell us something
    interesting about values: in this language, values are exactly the
    terms that _cannot_ make progress in this sense.

    To state this observation formally, let's begin by giving a name
    to terms that cannot make progress.  We'll call them _normal
    forms_.  *)

Definition normal_form {X:Type} (R:relation X) (t:X) : Prop :=
  ~ exists t', R t t'.

(** Note that this definition specifies what it is to be a normal form
    for an _arbitrary_ relation [R] over an arbitrary set [X], not
    just for the particular single-step reduction relation over terms
    that we are interested in at the moment.  We'll re-use the same
    terminology for talking about other relations later in the
    course. *)

(** We can use this terminology to generalize the observation we made
    in the strong progress theorem: in this language, normal forms and
    values are actually the same thing. *)

Lemma value_is_nf : forall v,
  value v -> normal_form step v.
Proof.
  unfold normal_form. intros v H. inversion H.
  intros contra. inversion contra. inversion H1.
Qed.

Lemma nf_is_value : forall t,
  normal_form step t -> value t.
Proof. (* a corollary of [strong_progress]... *)
  unfold normal_form. intros t H.
  assert (G : value t \/ exists t', t ==> t').
    { apply strong_progress. }
  inversion G.
    + (* l *) apply H0.
    + (* r *) exfalso. apply H. assumption.  Qed.

Corollary nf_same_as_value : forall t,
  normal_form step t <-> value t.
Proof.
  split. apply nf_is_value. apply value_is_nf. Qed.

(** Why is this interesting?

    Because [value] is a syntactic concept -- it is defined by looking
    at the form of a term -- while [normal_form] is a semantic one --
    it is defined by looking at how the term steps.  It is not obvious
    that these concepts should coincide!  *)

(** Indeed, we could easily have written the definitions so that they
    would _not_ coincide. *)

(** **** Exercise: 3 stars, optional (value_not_same_as_normal_form1)  *)
(** We might, for example, mistakenly define [value] so that it
    includes some terms that are not finished reducing. *)
(** (Even if you don't work this exercise and the following ones
    in Coq, make sure you can think of an example of such a term.) *)

Module Temp1.

Inductive value : tm -> Prop :=
| v_const : forall n, value (C n)
| v_funny : forall t1 n2,                       (* <---- *)
              value (P t1 (C n2)).

Reserved Notation " t '==>' t' " (at level 40).

Inductive step : tm -> tm -> Prop :=
  | ST_PlusConstConst : forall n1 n2,
      P (C n1) (C n2) ==> C (n1 + n2)
  | ST_Plus1 : forall t1 t1' t2,
      t1 ==> t1' ->
      P t1 t2 ==> P t1' t2
  | ST_Plus2 : forall v1 t2 t2',
      value v1 ->
      t2 ==> t2' ->
      P v1 t2 ==> P v1 t2'

  where " t '==>' t' " := (step t t').

Lemma value_not_same_as_normal_form :
  exists v, value v /\ ~ normal_form step v.
Proof.
  (* FILL IN HERE *) Admitted.
End Temp1.

(** [] *)

(** **** Exercise: 2 stars, optional (value_not_same_as_normal_form2)  *)
(** Alternatively, we might mistakenly define [step] so that it
    permits something designated as a value to reduce further. *)

Module Temp2.

Inductive value : tm -> Prop :=
| v_const : forall n, value (C n).

Reserved Notation " t '==>' t' " (at level 40).

Inductive step : tm -> tm -> Prop :=
  | ST_Funny : forall n,                         (* <---- *)
      C n ==> P (C n) (C 0)
  | ST_PlusConstConst : forall n1 n2,
      P (C n1) (C n2) ==> C (n1 + n2)
  | ST_Plus1 : forall t1 t1' t2,
      t1 ==> t1' ->
      P t1 t2 ==> P t1' t2
  | ST_Plus2 : forall v1 t2 t2',
      value v1 ->
      t2 ==> t2' ->
      P v1 t2 ==> P v1 t2'

  where " t '==>' t' " := (step t t').

Lemma value_not_same_as_normal_form :
  exists v, value v /\ ~ normal_form step v.
Proof.
  (* FILL IN HERE *) Admitted.

End Temp2.
(** [] *)

(** **** Exercise: 3 stars, optional (value_not_same_as_normal_form3)  *)
(** Finally, we might define [value] and [step] so that there is some
    term that is not a value but that cannot take a step in the [step]
    relation.  Such terms are said to be _stuck_. In this case this is
    caused by a mistake in the semantics, but we will also see
    situations where, even in a correct language definition, it makes
    sense to allow some terms to be stuck. *)

Module Temp3.

Inductive value : tm -> Prop :=
  | v_const : forall n, value (C n).

Reserved Notation " t '==>' t' " (at level 40).

Inductive step : tm -> tm -> Prop :=
  | ST_PlusConstConst : forall n1 n2,
      P (C n1) (C n2) ==> C (n1 + n2)
  | ST_Plus1 : forall t1 t1' t2,
      t1 ==> t1' ->
      P t1 t2 ==> P t1' t2

  where " t '==>' t' " := (step t t').

(** (Note that [ST_Plus2] is missing.) *)

Lemma value_not_same_as_normal_form :
  exists t, ~ value t /\ normal_form step t.
Proof.
  (* FILL IN HERE *) Admitted.

End Temp3.
(** [] *)

(* ----------------------------------------------------------------- *)
(** *** Additional Exercises *)

Module Temp4.

(** Here is another very simple language whose terms, instead of being
    just addition expressions and numbers, are just the booleans true
    and false and a conditional expression... *)

Inductive tm : Type :=
  | ttrue : tm
  | tfalse : tm
  | tif : tm -> tm -> tm -> tm.

Inductive value : tm -> Prop :=
  | v_true : value ttrue
  | v_false : value tfalse.

Reserved Notation " t '==>' t' " (at level 40).

Inductive step : tm -> tm -> Prop :=
  | ST_IfTrue : forall t1 t2,
      tif ttrue t1 t2 ==> t1
  | ST_IfFalse : forall t1 t2,
      tif tfalse t1 t2 ==> t2
  | ST_If : forall t1 t1' t2 t3,
      t1 ==> t1' ->
      tif t1 t2 t3 ==> tif t1' t2 t3

  where " t '==>' t' " := (step t t').

(** **** Exercise: 1 star (smallstep_bools)  *)
(** Which of the following propositions are provable?  (This is just a
    thought exercise, but for an extra challenge feel free to prove
    your answers in Coq.) *)

Definition bool_step_prop1 :=
  tfalse ==> tfalse.

(* FILL IN HERE *)

Definition bool_step_prop2 :=
     tif
       ttrue
       (tif ttrue ttrue ttrue)
       (tif tfalse tfalse tfalse)
  ==>
     ttrue.

(* FILL IN HERE *)

Definition bool_step_prop3 :=
     tif
       (tif ttrue ttrue ttrue)
       (tif ttrue ttrue ttrue)
       tfalse
   ==>
     tif
       ttrue
       (tif ttrue ttrue ttrue)
       tfalse.

(* FILL IN HERE *)
(** [] *)

(** **** Exercise: 3 stars, optional (progress_bool)  *)
(** Just as we proved a progress theorem for plus expressions, we can
    do so for boolean expressions, as well. *)

Theorem strong_progress : forall t,
  value t \/ (exists t', t ==> t').
Proof.
  (* FILL IN HERE *) Admitted.
(** [] *)

(** **** Exercise: 2 stars, optional (step_deterministic)  *)
Theorem step_deterministic :
  deterministic step.
Proof.
  (* FILL IN HERE *) Admitted.
(** [] *)

Module Temp5.

(** **** Exercise: 2 stars (smallstep_bool_shortcut)  *)
(** Suppose we want to add a "short circuit" to the step relation for
    boolean expressions, so that it can recognize when the [then] and
    [else] branches of a conditional are the same value (either
    [ttrue] or [tfalse]) and reduce the whole conditional to this
    value in a single step, even if the guard has not yet been reduced
    to a value. For example, we would like this proposition to be
    provable:

         tif
            (tif ttrue ttrue ttrue)
            tfalse
            tfalse
     ==>
         tfalse.
*)

(** Write an extra clause for the step relation that achieves this
    effect and prove [bool_step_prop4]. *)

Reserved Notation " t '==>' t' " (at level 40).

Inductive step : tm -> tm -> Prop :=
  | ST_IfTrue : forall t1 t2,
      tif ttrue t1 t2 ==> t1
  | ST_IfFalse : forall t1 t2,
      tif tfalse t1 t2 ==> t2
  | ST_If : forall t1 t1' t2 t3,
      t1 ==> t1' ->
      tif t1 t2 t3 ==> tif t1' t2 t3
  (* FILL IN HERE *)

  where " t '==>' t' " := (step t t').

Definition bool_step_prop4 :=
         tif
            (tif ttrue ttrue ttrue)
            tfalse
            tfalse
     ==>
         tfalse.

Example bool_step_prop4_holds :
  bool_step_prop4.
Proof.
  (* FILL IN HERE *) Admitted.
(** [] *)

(** **** Exercise: 3 stars, optional (properties_of_altered_step)  *)
(** It can be shown that the determinism and strong progress theorems
    for the step relation in the lecture notes also hold for the
    definition of step given above.  After we add the clause
    [ST_ShortCircuit]...

    - Is the [step] relation still deterministic?  Write yes or no and
      briefly (1 sentence) explain your answer.

      Optional: prove your answer correct in Coq. *)

(* FILL IN HERE *)
(**
   - Does a strong progress theorem hold? Write yes or no and
     briefly (1 sentence) explain your answer.

     Optional: prove your answer correct in Coq.
*)

(* FILL IN HERE *)
(**
   - In general, is there any way we could cause strong progress to
     fail if we took away one or more constructors from the original
     step relation? Write yes or no and briefly (1 sentence) explain
     your answer.

(* FILL IN HERE *)
*)
(** [] *)

End Temp5.
End Temp4.

(* ################################################################# *)
(** * Multi-Step Reduction *)

(** We've been working so far with the _single-step reduction_
    relation [==>], which formalizes the individual steps of an
    abstract machine for executing programs.

    We can use the same machine to reduce programs to completion -- to
    find out what final result they yield.  This can be formalized as
    follows:

    - First, we define a _multi-step reduction relation_ [==>*], which
      relates terms [t] and [t'] if [t] can reach [t'] by any number
      (including zero) of single reduction steps.

    - Then we define a "result" of a term [t] as a normal form that
      [t] can reach by multi-step reduction. *)

(** Since we'll want to reuse the idea of multi-step reduction many
    times, let's take a little extra trouble and define it
    generically.

    Given a relation [R], we define a relation [multi R], called the
    _multi-step closure of [R]_ as follows. *)

Inductive multi {X:Type} (R: relation X) : relation X :=
  | multi_refl  : forall (x : X), multi R x x
  | multi_step : forall (x y z : X),
                    R x y ->
                    multi R y z ->
                    multi R x z.

(** (In the [Rel] chapter of _Logical Foundations_ and
    the Coq standard library, this relation is called
    [clos_refl_trans_1n].  We give it a shorter name here for the sake
    of readability.) *)

(** The effect of this definition is that [multi R] relates two
    elements [x] and [y] if

       - [x = y], or
       - [R x y], or
       - there is some nonempty sequence [z1], [z2], ..., [zn] such that

           R x z1
           R z1 z2
           ...
           R zn y.

    Thus, if [R] describes a single-step of computation, then [z1]...[zn]
    is the sequence of intermediate steps of computation between [x] and
    [y]. *)

(** We write [==>*] for the [multi step] relation on terms. *)

Notation " t '==>*' t' " := (multi step t t') (at level 40).

(** The relation [multi R] has several crucial properties.

    First, it is obviously _reflexive_ (that is, [forall x, multi R x
    x]).  In the case of the [==>*] (i.e., [multi step]) relation, the
    intuition is that a term can execute to itself by taking zero
    steps of execution.

    Second, it contains [R] -- that is, single-step executions are a
    particular case of multi-step executions.  (It is this fact that
    justifies the word "closure" in the term "multi-step closure of
    [R].") *)

Theorem multi_R : forall (X:Type) (R:relation X) (x y : X),
       R x y -> (multi R) x y.
Proof.
  intros X R x y H.
  apply multi_step with y. apply H. apply multi_refl.   Qed.

(** Third, [multi R] is _transitive_. *)

Theorem multi_trans :
  forall (X:Type) (R: relation X) (x y z : X),
      multi R x y  ->
      multi R y z ->
      multi R x z.
Proof.
  intros X R x y z G H.
  induction G.
    - (* multi_refl *) assumption.
    - (* multi_step *)
      apply multi_step with y. assumption.
      apply IHG. assumption.  Qed.

(** In particular, for the [multi step] relation on terms, if
    [t1==>*t2] and [t2==>*t3], then [t1==>*t3]. *)

(* ================================================================= *)
(** ** Examples *)

(** Here's a specific instance of the [multi step] relation: *)

Lemma test_multistep_1:
      P
        (P (C 0) (C 3))
        (P (C 2) (C 4))
   ==>*
      C ((0 + 3) + (2 + 4)).
Proof.
  apply multi_step with
            (P (C (0 + 3))
               (P (C 2) (C 4))).
  apply ST_Plus1. apply ST_PlusConstConst.
  apply multi_step with
            (P (C (0 + 3))
               (C (2 + 4))).
  apply ST_Plus2. apply v_const.
  apply ST_PlusConstConst.
  apply multi_R.
  apply ST_PlusConstConst. Qed.

(** Here's an alternate proof of the same fact that uses [eapply] to
    avoid explicitly constructing all the intermediate terms. *)

Lemma test_multistep_1':
      P
        (P (C 0) (C 3))
        (P (C 2) (C 4))
  ==>*
      C ((0 + 3) + (2 + 4)).
Proof.
  eapply multi_step. apply ST_Plus1. apply ST_PlusConstConst.
  eapply multi_step. apply ST_Plus2. apply v_const.
  apply ST_PlusConstConst.
  eapply multi_step. apply ST_PlusConstConst.
  apply multi_refl.  Qed.

(** **** Exercise: 1 star, optional (test_multistep_2)  *)
Lemma test_multistep_2:
  C 3 ==>* C 3.
Proof.
  (* FILL IN HERE *) Admitted.
(** [] *)

(** **** Exercise: 1 star, optional (test_multistep_3)  *)
Lemma test_multistep_3:
      P (C 0) (C 3)
   ==>*
      P (C 0) (C 3).
Proof.
  (* FILL IN HERE *) Admitted.
(** [] *)

(** **** Exercise: 2 stars (test_multistep_4)  *)
Lemma test_multistep_4:
      P
        (C 0)
        (P
          (C 2)
          (P (C 0) (C 3)))
  ==>*
      P
        (C 0)
        (C (2 + (0 + 3))).
Proof.
  (* FILL IN HERE *) Admitted.
(** [] *)

(* ================================================================= *)
(** ** Normal Forms Again *)

(** If [t] reduces to [t'] in zero or more steps and [t'] is a
    normal form, we say that "[t'] is a normal form of [t]." *)

Definition step_normal_form := normal_form step.

Definition normal_form_of (t t' : tm) :=
  (t ==>* t' /\ step_normal_form t').

(** We have already seen that, for our language, single-step reduction is
    deterministic -- i.e., a given term can take a single step in
    at most one way.  It follows from this that, if [t] can reach
    a normal form, then this normal form is unique.  In other words, we
    can actually pronounce [normal_form t t'] as "[t'] is _the_
    normal form of [t]." *)

(** **** Exercise: 3 stars, optional (normal_forms_unique)  *)
Theorem normal_forms_unique:
  deterministic normal_form_of.
Proof.
  (* We recommend using this initial setup as-is! *)
  unfold deterministic. unfold normal_form_of.
  intros x y1 y2 P1 P2.
  inversion P1 as [P11 P12]; clear P1.
  inversion P2 as [P21 P22]; clear P2.
  generalize dependent y2.
  (* FILL IN HERE *) Admitted.
(** [] *)

(** Indeed, something stronger is true for this language (though not
    for all languages): the reduction of _any_ term [t] will
    eventually reach a normal form -- i.e., [normal_form_of] is a
    _total_ function.  Formally, we say the [step] relation is
    _normalizing_. *)

Definition normalizing {X:Type} (R:relation X) :=
  forall t, exists t',
    (multi R) t t' /\ normal_form R t'.

(** To prove that [step] is normalizing, we need a couple of lemmas.

    First, we observe that, if [t] reduces to [t'] in many steps, then
    the same sequence of reduction steps within [t] is also possible
    when [t] appears as the left-hand child of a [P] node, and
    similarly when [t] appears as the right-hand child of a [P]
    node whose left-hand child is a value. *)

Lemma multistep_congr_1 : forall t1 t1' t2,
     t1 ==>* t1' ->
     P t1 t2 ==>* P t1' t2.
Proof.
  intros t1 t1' t2 H. induction H.
    - (* multi_refl *) apply multi_refl.
    - (* multi_step *) apply multi_step with (P y t2).
        apply ST_Plus1. apply H.
        apply IHmulti.  Qed.

(** **** Exercise: 2 stars (multistep_congr_2)  *)
Lemma multistep_congr_2 : forall t1 t2 t2',
     value t1 ->
     t2 ==>* t2' ->
     P t1 t2 ==>* P t1 t2'.
Proof.
  (* FILL IN HERE *) Admitted.
(** [] *)

(** With these lemmas in hand, the main proof is a straightforward
    induction.

    _Theorem_: The [step] function is normalizing -- i.e., for every
    [t] there exists some [t'] such that [t] steps to [t'] and [t'] is
    a normal form.

    _Proof sketch_: By induction on terms.  There are two cases to
    consider:

    - [t = C n] for some [n].  Here [t] doesn't take a step, and we
      have [t' = t].  We can derive the left-hand side by reflexivity
      and the right-hand side by observing (a) that values are normal
      forms (by [nf_same_as_value]) and (b) that [t] is a value (by
      [v_const]).

    - [t = P t1 t2] for some [t1] and [t2].  By the IH, [t1] and [t2]
      have normal forms [t1'] and [t2'].  Recall that normal forms are
      values (by [nf_same_as_value]); we know that [t1' = C n1] and
      [t2' = C n2], for some [n1] and [n2].  We can combine the [==>*]
      derivations for [t1] and [t2] using [multi_congr_1] and
      [multi_congr_2] to prove that [P t1 t2] reduces in many steps to
      [C (n1 + n2)].

      It is clear that our choice of [t' = C (n1 + n2)] is a value,
      which is in turn a normal form. [] *)

Theorem step_normalizing :
  normalizing step.
Proof.
  unfold normalizing.
  induction t.
    - (* C *)
      exists (C n).
      split.
      + (* l *) apply multi_refl.
      + (* r *)
        (* We can use [rewrite] with "iff" statements, not
           just equalities: *)
        rewrite nf_same_as_value. apply v_const.
    - (* P *)
      destruct IHt1 as [t1' [H11 H12]].
      destruct IHt2 as [t2' [H21 H22]].
      rewrite nf_same_as_value in H12. rewrite nf_same_as_value in H22.
      inversion H12 as [n1 H]. inversion H22 as [n2 H'].
      rewrite <- H in H11.
      rewrite <- H' in H21.
      exists (C (n1 + n2)).
      split.
        + (* l *)
          apply multi_trans with (P (C n1) t2).
          * apply multistep_congr_1. apply H11.
          * apply multi_trans with
             (P (C n1) (C n2)).
            { apply multistep_congr_2. apply v_const. apply H21. }
            { apply multi_R. apply ST_PlusConstConst. }
        + (* r *)
          rewrite nf_same_as_value. apply v_const.  Qed.

(* ================================================================= *)
(** ** Equivalence of Big-Step and Small-Step *)

(** Having defined the operational semantics of our tiny programming
    language in two different ways (big-step and small-step), it makes
    sense to ask whether these definitions actually define the same
    thing!  They do, though it takes a little work to show it.  The
    details are left as an exercise. *)

(** **** Exercise: 3 stars (eval__multistep)  *)
Theorem eval__multistep : forall t n,
  t \\ n -> t ==>* C n.

(** The key ideas in the proof can be seen in the following picture:

       P t1 t2 ==>            (by ST_Plus1)
       P t1' t2 ==>           (by ST_Plus1)
       P t1'' t2 ==>          (by ST_Plus1)
       ...
       P (C n1) t2 ==>        (by ST_Plus2)
       P (C n1) t2' ==>       (by ST_Plus2)
       P (C n1) t2'' ==>      (by ST_Plus2)
       ...
       P (C n1) (C n2) ==>    (by ST_PlusConstConst)
       C (n1 + n2)

    That is, the multistep reduction of a term of the form [P t1 t2]
    proceeds in three phases:
       - First, we use [ST_Plus1] some number of times to reduce [t1]
         to a normal form, which must (by [nf_same_as_value]) be a
         term of the form [C n1] for some [n1].
       - Next, we use [ST_Plus2] some number of times to reduce [t2]
         to a normal form, which must again be a term of the form [C
         n2] for some [n2].
       - Finally, we use [ST_PlusConstConst] one time to reduce [P (C
         n1) (C n2)] to [C (n1 + n2)]. *)

(** To formalize this intuition, you'll need to use the congruence
    lemmas from above (you might want to review them now, so that
    you'll be able to recognize when they are useful), plus some basic
    properties of [==>*]: that it is reflexive, transitive, and
    includes [==>]. *)

Proof.
  (* FILL IN HERE *) Admitted.
(** [] *)

(** **** Exercise: 3 stars, advanced (eval__multistep_inf)  *)
(** Write a detailed informal version of the proof of [eval__multistep].

(* FILL IN HERE *)
*)
(** [] *)

(** For the other direction, we need one lemma, which establishes a
    relation between single-step reduction and big-step evaluation. *)

(** **** Exercise: 3 stars (step__eval)  *)
Lemma step__eval : forall t t' n,
     t ==> t' ->
     t' \\ n ->
     t \\ n.
Proof.
  intros t t' n Hs. generalize dependent n.
  (* FILL IN HERE *) Admitted.
(** [] *)

(** The fact that small-step reduction implies big-step evaluation is
    now straightforward to prove, once it is stated correctly.

    The proof proceeds by induction on the multi-step reduction
    sequence that is buried in the hypothesis [normal_form_of t t']. *)

(** Make sure you understand the statement before you start to
    work on the proof.  *)

(** **** Exercise: 3 stars (multistep__eval)  *)
Theorem multistep__eval : forall t t',
  normal_form_of t t' -> exists n, t' = C n /\ t \\ n.
Proof.
  (* FILL IN HERE *) Admitted.
(** [] *)

(* ================================================================= *)
(** ** Additional Exercises *)

(** **** Exercise: 3 stars, optional (interp_tm)  *)
(** Remember that we also defined big-step evaluation of terms as a
    function [evalF].  Prove that it is equivalent to the existing
    semantics.  (Hint: we just proved that [eval] and [multistep] are
    equivalent, so logically it doesn't matter which you choose.
    One will be easier than the other, though!) *)

Theorem evalF_eval : forall t n,
  evalF t = n <-> t \\ n.
Proof.
  (* FILL IN HERE *) Admitted.
(** [] *)

(** **** Exercise: 4 stars (combined_properties)  *)
(** We've considered arithmetic and conditional expressions
    separately.  This exercise explores how the two interact. *)

Module Combined.

Inductive tm : Type :=
  | C : nat -> tm
  | P : tm -> tm -> tm
  | ttrue : tm
  | tfalse : tm
  | tif : tm -> tm -> tm -> tm.

Inductive value : tm -> Prop :=
  | v_const : forall n, value (C n)
  | v_true : value ttrue
  | v_false : value tfalse.

Reserved Notation " t '==>' t' " (at level 40).

Inductive step : tm -> tm -> Prop :=
  | ST_PlusConstConst : forall n1 n2,
      P (C n1) (C n2) ==> C (n1 + n2)
  | ST_Plus1 : forall t1 t1' t2,
      t1 ==> t1' ->
      P t1 t2 ==> P t1' t2
  | ST_Plus2 : forall v1 t2 t2',
      value v1 ->
      t2 ==> t2' ->
      P v1 t2 ==> P v1 t2'
  | ST_IfTrue : forall t1 t2,
      tif ttrue t1 t2 ==> t1
  | ST_IfFalse : forall t1 t2,
      tif tfalse t1 t2 ==> t2
  | ST_If : forall t1 t1' t2 t3,
      t1 ==> t1' ->
      tif t1 t2 t3 ==> tif t1' t2 t3

  where " t '==>' t' " := (step t t').

(** Earlier, we separately proved for both plus- and if-expressions...

    - that the step relation was deterministic, and

    - a strong progress lemma, stating that every term is either a
      value or can take a step.

    Formally prove or disprove these two properties for the combined
    language.  (That is, state a theorem saying that the property
    holds or does not hold, and prove your theorem.) *)

(* FILL IN HERE *)

End Combined.
(** [] *)

(* ################################################################# *)
(** * Small-Step Imp *)

(** Now for a more serious example: a small-step version of the Imp
    operational semantics. *)

(** The small-step reduction relations for arithmetic and
    boolean expressions are straightforward extensions of the tiny
    language we've been working up to now.  To make them easier to
    read, we introduce the symbolic notations [==>a] and [==>b] for
    the arithmetic and boolean step relations. *)

Inductive aval : aexp -> Prop :=
  | av_num : forall n, aval (ANum n).

(** We are not actually going to bother to define boolean
    values, since they aren't needed in the definition of [==>b]
    below (why?), though they might be if our language were a bit
    larger (why?). *)

Reserved Notation " t '/' st '==>a' t' "
                  (at level 40, st at level 39).

Inductive astep : state -> aexp -> aexp -> Prop :=
  | AS_Id : forall st i,
      AId i / st ==>a ANum (st i)
  | AS_Plus : forall st n1 n2,
      APlus (ANum n1) (ANum n2) / st ==>a ANum (n1 + n2)
  | AS_Plus1 : forall st a1 a1' a2,
      a1 / st ==>a a1' ->
      (APlus a1 a2) / st ==>a (APlus a1' a2)
  | AS_Plus2 : forall st v1 a2 a2',
      aval v1 ->
      a2 / st ==>a a2' ->
      (APlus v1 a2) / st ==>a (APlus v1 a2')
  | AS_Minus : forall st n1 n2,
      (AMinus (ANum n1) (ANum n2)) / st ==>a (ANum (minus n1 n2))
  | AS_Minus1 : forall st a1 a1' a2,
      a1 / st ==>a a1' ->
      (AMinus a1 a2) / st ==>a (AMinus a1' a2)
  | AS_Minus2 : forall st v1 a2 a2',
      aval v1 ->
      a2 / st ==>a a2' ->
      (AMinus v1 a2) / st ==>a (AMinus v1 a2')
  | AS_Mult : forall st n1 n2,
      (AMult (ANum n1) (ANum n2)) / st ==>a (ANum (mult n1 n2))
  | AS_Mult1 : forall st a1 a1' a2,
      a1 / st ==>a a1' ->
      (AMult a1 a2) / st ==>a (AMult a1' a2)
  | AS_Mult2 : forall st v1 a2 a2',
      aval v1 ->
      a2 / st ==>a a2' ->
      (AMult v1 a2) / st ==>a (AMult v1 a2')

    where " t '/' st '==>a' t' " := (astep st t t').

Reserved Notation " t '/' st '==>b' t' "
                  (at level 40, st at level 39).

Inductive bstep : state -> bexp -> bexp -> Prop :=
| BS_Eq : forall st n1 n2,
    (BEq (ANum n1) (ANum n2)) / st ==>b
    (if (beq_nat n1 n2) then BTrue else BFalse)
| BS_Eq1 : forall st a1 a1' a2,
    a1 / st ==>a a1' ->
    (BEq a1 a2) / st ==>b (BEq a1' a2)
| BS_Eq2 : forall st v1 a2 a2',
    aval v1 ->
    a2 / st ==>a a2' ->
    (BEq v1 a2) / st ==>b (BEq v1 a2')
| BS_LtEq : forall st n1 n2,
    (BLe (ANum n1) (ANum n2)) / st ==>b
             (if (leb n1 n2) then BTrue else BFalse)
| BS_LtEq1 : forall st a1 a1' a2,
    a1 / st ==>a a1' ->
    (BLe a1 a2) / st ==>b (BLe a1' a2)
| BS_LtEq2 : forall st v1 a2 a2',
    aval v1 ->
    a2 / st ==>a a2' ->
    (BLe v1 a2) / st ==>b (BLe v1 a2')
| BS_NotTrue : forall st,
    (BNot BTrue) / st ==>b BFalse
| BS_NotFalse : forall st,
    (BNot BFalse) / st ==>b BTrue
| BS_NotStep : forall st b1 b1',
    b1 / st ==>b b1' ->
    (BNot b1) / st ==>b (BNot b1')
| BS_AndTrueTrue : forall st,
    (BAnd BTrue BTrue) / st ==>b BTrue
| BS_AndTrueFalse : forall st,
    (BAnd BTrue BFalse) / st ==>b BFalse
| BS_AndFalse : forall st b2,
    (BAnd BFalse b2) / st ==>b BFalse
| BS_AndTrueStep : forall st b2 b2',
    b2 / st ==>b b2' ->
    (BAnd BTrue b2) / st ==>b (BAnd BTrue b2')
| BS_AndStep : forall st b1 b1' b2,
    b1 / st ==>b b1' ->
    (BAnd b1 b2) / st ==>b (BAnd b1' b2)

where " t '/' st '==>b' t' " := (bstep st t t').

(** The semantics of commands is the interesting part.  We need two
    small tricks to make it work:

       - We use [SKIP] as a "command value" -- i.e., a command that
         has reached a normal form.

            - An assignment command reduces to [SKIP] (and an updated
              state).

            - The sequencing command waits until its left-hand
              subcommand has reduced to [SKIP], then throws it away so
              that reduction can continue with the right-hand
              subcommand.

       - We reduce a [WHILE] command by transforming it into a
         conditional followed by the same [WHILE]. *)

(** (There are other ways of achieving the effect of the latter
    trick, but they all share the feature that the original [WHILE]
    command needs to be saved somewhere while a single copy of the loop
    body is being reduced.) *)

Reserved Notation " t '/' st '==>' t' '/' st' "
                  (at level 40, st at level 39, t' at level 39).

Inductive cstep : (com * state) -> (com * state) -> Prop :=
  | CS_AssStep : forall st i a a',
      a / st ==>a a' ->
      (i ::= a) / st ==> (i ::= a') / st
  | CS_Ass : forall st i n,
      (i ::= (ANum n)) / st ==> SKIP / (st & { i --> n })
  | CS_SeqStep : forall st c1 c1' st' c2,
      c1 / st ==> c1' / st' ->
      (c1 ;; c2) / st ==> (c1' ;; c2) / st'
  | CS_SeqFinish : forall st c2,
      (SKIP ;; c2) / st ==> c2 / st
  | CS_IfTrue : forall st c1 c2,
      IFB BTrue THEN c1 ELSE c2 FI / st ==> c1 / st
  | CS_IfFalse : forall st c1 c2,
      IFB BFalse THEN c1 ELSE c2 FI / st ==> c2 / st
  | CS_IfStep : forall st b b' c1 c2,
      b / st ==>b b' ->
          IFB b THEN c1 ELSE c2 FI / st
      ==> (IFB b' THEN c1 ELSE c2 FI) / st
  | CS_While : forall st b c1,
          (WHILE b DO c1 END) / st
      ==> (IFB b THEN (c1;; (WHILE b DO c1 END)) ELSE SKIP FI) / st

  where " t '/' st '==>' t' '/' st' " := (cstep (t,st) (t',st')).

(* ################################################################# *)
(** * Concurrent Imp *)

(** Finally, to show the power of this definitional style, let's
    enrich Imp with a new form of command that runs two subcommands in
    parallel and terminates when both have terminated.  To reflect the
    unpredictability of scheduling, the actions of the subcommands may
    be interleaved in any order, but they share the same memory and
    can communicate by reading and writing the same variables. *)

Module CImp.

Inductive com : Type :=
  | CSkip : com
  | CAss : string -> aexp -> com
  | CSeq : com -> com -> com
  | CIf : bexp -> com -> com -> com
  | CWhile : bexp -> com -> com
  (* New: *)
  | CPar : com -> com -> com.

Notation "'SKIP'" :=
  CSkip.
Notation "x '::=' a" :=
  (CAss x a) (at level 60).
Notation "c1 ;; c2" :=
  (CSeq c1 c2) (at level 80, right associativity).
Notation "'WHILE' b 'DO' c 'END'" :=
  (CWhile b c) (at level 80, right associativity).
Notation "'IFB' b 'THEN' c1 'ELSE' c2 'FI'" :=
  (CIf b c1 c2) (at level 80, right associativity).
Notation "'PAR' c1 'WITH' c2 'END'" :=
  (CPar c1 c2) (at level 80, right associativity).

Inductive cstep : (com * state)  -> (com * state) -> Prop :=
    (* Old part *)
  | CS_AssStep : forall st i a a',
      a / st ==>a a' ->
      (i ::= a) / st ==> (i ::= a') / st
  | CS_Ass : forall st i n,
      (i ::= (ANum n)) / st ==> SKIP / st & { i --> n }
  | CS_SeqStep : forall st c1 c1' st' c2,
      c1 / st ==> c1' / st' ->
      (c1 ;; c2) / st ==> (c1' ;; c2) / st'
  | CS_SeqFinish : forall st c2,
      (SKIP ;; c2) / st ==> c2 / st
  | CS_IfTrue : forall st c1 c2,
      (IFB BTrue THEN c1 ELSE c2 FI) / st ==> c1 / st
  | CS_IfFalse : forall st c1 c2,
      (IFB BFalse THEN c1 ELSE c2 FI) / st ==> c2 / st
  | CS_IfStep : forall st b b' c1 c2,
      b /st ==>b b' ->
          (IFB b THEN c1 ELSE c2 FI) / st
      ==> (IFB b' THEN c1 ELSE c2 FI) / st
  | CS_While : forall st b c1,
          (WHILE b DO c1 END) / st
      ==> (IFB b THEN (c1;; (WHILE b DO c1 END)) ELSE SKIP FI) / st
    (* New part: *)
  | CS_Par1 : forall st c1 c1' c2 st',
      c1 / st ==> c1' / st' ->
      (PAR c1 WITH c2 END) / st ==> (PAR c1' WITH c2 END) / st'
  | CS_Par2 : forall st c1 c2 c2' st',
      c2 / st ==> c2' / st' ->
      (PAR c1 WITH c2 END) / st ==> (PAR c1 WITH c2' END) / st'
  | CS_ParDone : forall st,
      (PAR SKIP WITH SKIP END) / st ==> SKIP / st
  where " t '/' st '==>' t' '/' st' " := (cstep (t,st) (t',st')).

Definition cmultistep := multi cstep.

Notation " t '/' st '==>*' t' '/' st' " :=
   (multi cstep  (t,st) (t',st'))
   (at level 40, st at level 39, t' at level 39).

(** Among the many interesting properties of this language is the fact
    that the following program can terminate with the variable [X] set
    to any value. *)

Definition par_loop : com :=
  PAR
    Y ::= 1
  WITH
    WHILE Y = 0 DO
      X ::= X + 1
    END
  END.

(** In particular, it can terminate with [X] set to [0]: *)

Example par_loop_example_0:
  exists st',
       par_loop / { --> 0 }  ==>* SKIP / st'
    /\ st' X = 0.
Proof.
  eapply ex_intro. split.
  unfold par_loop.
  eapply multi_step. apply CS_Par1.
    apply CS_Ass.
  eapply multi_step. apply CS_Par2. apply CS_While.
  eapply multi_step. apply CS_Par2. apply CS_IfStep.
    apply BS_Eq1. apply AS_Id.
  eapply multi_step. apply CS_Par2. apply CS_IfStep.
    apply BS_Eq. simpl.
  eapply multi_step. apply CS_Par2. apply CS_IfFalse.
  eapply multi_step. apply CS_ParDone.
  eapply multi_refl.
  reflexivity. Qed.

(** It can also terminate with [X] set to [2]: *)

Example par_loop_example_2:
  exists st',
       par_loop / { --> 0 } ==>* SKIP / st'
    /\ st' X = 2.
Proof.
  eapply ex_intro. split.
  eapply multi_step. apply CS_Par2. apply CS_While.
  eapply multi_step. apply CS_Par2. apply CS_IfStep.
    apply BS_Eq1. apply AS_Id.
  eapply multi_step. apply CS_Par2. apply CS_IfStep.
    apply BS_Eq. simpl.
  eapply multi_step. apply CS_Par2. apply CS_IfTrue.
  eapply multi_step. apply CS_Par2. apply CS_SeqStep.
    apply CS_AssStep. apply AS_Plus1. apply AS_Id.
  eapply multi_step. apply CS_Par2. apply CS_SeqStep.
    apply CS_AssStep. apply AS_Plus.
  eapply multi_step. apply CS_Par2. apply CS_SeqStep.
    apply CS_Ass.
  eapply multi_step. apply CS_Par2. apply CS_SeqFinish.

  eapply multi_step. apply CS_Par2. apply CS_While.
  eapply multi_step. apply CS_Par2. apply CS_IfStep.
    apply BS_Eq1. apply AS_Id.
  eapply multi_step. apply CS_Par2. apply CS_IfStep.
    apply BS_Eq. simpl.
  eapply multi_step. apply CS_Par2. apply CS_IfTrue.
  eapply multi_step. apply CS_Par2. apply CS_SeqStep.
    apply CS_AssStep. apply AS_Plus1. apply AS_Id.
  eapply multi_step. apply CS_Par2. apply CS_SeqStep.
    apply CS_AssStep. apply AS_Plus.
  eapply multi_step. apply CS_Par2. apply CS_SeqStep.
    apply CS_Ass.

  eapply multi_step. apply CS_Par1. apply CS_Ass.
  eapply multi_step. apply CS_Par2. apply CS_SeqFinish.
  eapply multi_step. apply CS_Par2. apply CS_While.
  eapply multi_step. apply CS_Par2. apply CS_IfStep.
    apply BS_Eq1. apply AS_Id.
  eapply multi_step. apply CS_Par2. apply CS_IfStep.
    apply BS_Eq. simpl.
  eapply multi_step. apply CS_Par2. apply CS_IfFalse.
  eapply multi_step. apply CS_ParDone.
  eapply multi_refl.
  reflexivity. Qed.

(** More generally... *)

(** **** Exercise: 3 stars, optional (par_body_n__Sn)  *)
Lemma par_body_n__Sn : forall n st,
  st X = n /\ st Y = 0 ->
  par_loop / st ==>* par_loop / st & { X --> S n}.
Proof.
  (* FILL IN HERE *) Admitted.
(** [] *)

(** **** Exercise: 3 stars, optional (par_body_n)  *)
Lemma par_body_n : forall n st,
  st X = 0 /\ st Y = 0 ->
  exists st',
    par_loop / st ==>*  par_loop / st' /\ st' X = n /\ st' Y = 0.
Proof.
  (* FILL IN HERE *) Admitted.
(** [] *)

(** ... the above loop can exit with [X] having any value
    whatsoever. *)

Theorem par_loop_any_X:
  forall n, exists st',
    par_loop / { --> 0 } ==>*  SKIP / st'
    /\ st' X = n.
Proof.
  intros n.
  destruct (par_body_n n { --> 0 }).
    split; unfold t_update; reflexivity.

  rename x into st.
  inversion H as [H' [HX HY]]; clear H.
  exists (st & { Y --> 1 }). split.
  eapply multi_trans with (par_loop,st). apply H'.
  eapply multi_step. apply CS_Par1. apply CS_Ass.
  eapply multi_step. apply CS_Par2. apply CS_While.
  eapply multi_step. apply CS_Par2. apply CS_IfStep.
    apply BS_Eq1. apply AS_Id. rewrite t_update_eq.
  eapply multi_step. apply CS_Par2. apply CS_IfStep.
    apply BS_Eq. simpl.
  eapply multi_step. apply CS_Par2. apply CS_IfFalse.
  eapply multi_step. apply CS_ParDone.
  apply multi_refl.

  rewrite t_update_neq. assumption. intro X; inversion X.
Qed.

End CImp.

(* ################################################################# *)
(** * A Small-Step Stack Machine *)

(** Our last example is a small-step semantics for the stack machine
    example from the [Imp] chapter of _Logical Foundations_. *)

Definition stack := list nat.
Definition prog  := list sinstr.

Inductive stack_step : state -> prog * stack -> prog * stack -> Prop :=
  | SS_Push : forall st stk n p',
    stack_step st (SPush n :: p', stk)      (p', n :: stk)
  | SS_Load : forall st stk i p',
    stack_step st (SLoad i :: p', stk)      (p', st i :: stk)
  | SS_Plus : forall st stk n m p',
    stack_step st (SPlus :: p', n::m::stk)  (p', (m+n)::stk)
  | SS_Minus : forall st stk n m p',
    stack_step st (SMinus :: p', n::m::stk) (p', (m-n)::stk)
  | SS_Mult : forall st stk n m p',
    stack_step st (SMult :: p', n::m::stk)  (p', (m*n)::stk).

Theorem stack_step_deterministic : forall st,
  deterministic (stack_step st).
Proof.
  unfold deterministic. intros st x y1 y2 H1 H2.
  induction H1; inversion H2; reflexivity.
Qed.

Definition stack_multistep st := multi (stack_step st).

(** **** Exercise: 3 stars, advanced (compiler_is_correct)  *)
(** Remember the definition of [compile] for [aexp] given in the
    [Imp] chapter of _Logical Foundations_. We want now to
    prove [compile] correct with respect to the stack machine.

    State what it means for the compiler to be correct according to
    the stack machine small step semantics and then prove it. *)

Definition compiler_is_correct_statement : Prop
  (* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.

Theorem compiler_is_correct : compiler_is_correct_statement.
Proof.
(* FILL IN HERE *) Admitted.
(** [] *)

(** $Date$ *)

max_stars_repo_name: jutaro/ProgrammingLanguageFoundations

max_issues_repo_name: jutaro/ProgrammingLanguageFoundations

max_forks_repo_name: jutaro/ProgrammingLanguageFoundations


text:
module Dart.Core

import System.FFI

%foreign "Dart:print,dart:core"
prim__print : AnyPtr -> PrimIO ()

export
print : HasIO io => a -> io ()
print a = primIO $ prim__print (believe_me a)

mutual
  public export
  Object : Type
  Object = Struct "Object,dart:core" [("hashCode", Int)]

  public export
  Symbol : Type
  Symbol = Struct "Symbol,dart:core" [("hashCode", Int)]

  public export
  Iterable : Type -> Type
  Iterable ty = Struct "Iterable,dart:core" [("first", ty), ("last", ty)]

  public export
  DartList : Type -> Type
  DartList ty = Struct "List,dart:core" [("length", Int), ("first", ty), ("last", ty)]

  public export
  DartMap : Type -> Type -> Type
  DartMap key val = Struct "Map,dart:core" [("keys", Iterable key), ("values", Iterable val)]

namespace Object
  %foreign "Dart:.toString"
  prim__toString : Object -> PrimIO String

  public export
  toString : HasIO io => a -> io String
  toString o = primIO $ prim__toString (believe_me o)

public export
DartBool : Type
DartBool = Struct "bool,dart:core" [("hashCode", Int)]

export
%extern prim__dart_true : DartBool

export
%extern prim__dart_false : DartBool

export
%extern prim__dart_eq : a -> a -> DartBool

export
%extern prim__dart_if : DartBool -> a -> a -> a

namespace DartBool
  %inline
  public export
  true : DartBool
  true = prim__dart_true

  %inline
  public export
  false : DartBool
  false = prim__dart_false

  %inline
  public export
  fromBool : Bool -> DartBool
  fromBool b = prim__dart_eq b True

  %inline
  public export
  toBool : DartBool -> Bool
  toBool b = prim__dart_if b True False

export
Cast Bool DartBool where
  cast = fromBool

export
Cast DartBool Bool where
  cast = toBool

export
Eq DartBool where
  (==) x y = toBool (prim__dart_eq x y)

export
Show DartBool where
  show b = show (toBool b)

public export
%extern prim__dart_list_new : (elTy : Type) -> (1 x : %World) -> IORes (DartList elTy)

namespace List
  %inline
  export
  new : HasIO io => {elTy : Type} -> io (DartList elTy)
  new = primIO $ prim__dart_list_new elTy

  export
  %foreign "Dart:.add"
  prim__list_add : DartList AnyPtr -> AnyPtr -> PrimIO ()

  %inline
  export
  add : HasIO io => {0 elTy : Type} -> elTy -> DartList elTy -> io ()
  add e list = primIO $ prim__list_add (believe_me list) (believe_me e)

namespace Map
  %foreign "Dart:Map,dart:core"
  prim__new : PrimIO (DartMap _ _)

  %inline
  export
  new : HasIO io => io (DartMap _ _)
  new = primIO prim__new

  %foreign "Dart:[]"
  prim__put : DartMap key val -> key -> val -> PrimIO ()

  export
  put : HasIO io => {0 key : Type} -> key -> {0 val : Type} -> val -> DartMap key val -> io ()
  put k v m = primIO $ prim__put m k v

%inline
public export
Duration : Type
Duration = Struct "Duration,dart:core" [
  ("inMilliseconds", Int),
  ("inMicroseconds", Int)
]

namespace Duration

  %foreign "Dart:const Duration.microsecondsPerMinute,dart:core"
  public export
  microsecondsPerMinute : Int

  %foreign "Dart:const Duration.microsecondsPerSecond,dart:core"
  public export
  microsecondsPerSecond : Int

  %foreign "Dart:const Duration.microsecondsPerMillisecond,dart:core"
  public export
  microsecondsPerMillisecond : Int

  %inline
  public export
  inMilliseconds : Duration -> Int
  inMilliseconds = (`getField` "inMilliseconds")

  %inline
  public export
  inMicroseconds : Duration -> Int
  inMicroseconds = (`getField` "inMicroseconds")

ext: idr


text:
module Data.Profunctor.Choice

import Control.Category
import Data.Profunctor.Interface


text:
module Data.String.Iterator

import Control.Monad.Identity
import public Data.List.Lazy

%default total

-- Backend-dependent string iteration type,
-- parameterised by the string that it iterates over.
--
-- Beware: the index is checked only up to definitional equality.
-- In theory, you could run `decEq` on two strings
-- with the same content but allocated in different memory locations
-- and use the obtained Refl to coerce iterators between them.
--
-- The strictly correct solution is to make the iterators independent
-- from the exact memory location of the string given to `uncons`.
-- (For example, byte offsets satisfy this requirement.)
export
data StringIterator : String -> Type where [external]

-- This function is private
-- to avoid subverting the linearity guarantees of withString.
%foreign
  "scheme:blodwen-string-iterator-new"
  "RefC:stringIteratorNew"
  "javascript:stringIterator:new"
private
fromString : (str : String) -> StringIterator str

-- This function uses a linear string iterator
-- so that backends can use mutating iterators.
export
withString : (str : String) -> ((1 it : StringIterator str) -> a) -> a
withString str f = f (fromString str)

||| Runs the action `f` on the slice `res` of the original string `str` represented by the
||| iterator `it`
%foreign
  "scheme:blodwen-string-iterator-to-string"
  "RefC:stringIteratorToString"
  "javascript:stringIterator:toString"
export
withIteratorString : (str : String)
                  -> (1 it : StringIterator str)
                  -> (f : (res : String) -> a)
                  -> a

-- We use a custom data type instead of Maybe (Char, StringIterator)
-- to remove one level of pointer indirection
-- in every iteration of something that's likely to be a hot loop,
-- and to avoid one allocation per character.
--
-- The Char field of Character is unrestricted for flexibility.
public export
data UnconsResult : String -> Type where
  EOF : UnconsResult str
  Character : (c : Char) -> (1 it : StringIterator str) -> UnconsResult str

-- We pass the whole string to the uncons function
-- to avoid yet another allocation per character
-- because for many backends, StringIterator can be simply an integer
-- (e.g. byte offset into an UTF-8 string).
%foreign
  "scheme:blodwen-string-iterator-next"
  "RefC:stringIteratorNext"
  "javascript:stringIterator:next"
export
uncons : (str : String) -> (1 it : StringIterator str) -> UnconsResult str

export
foldl : (accTy -> Char -> accTy) -> accTy -> String -> accTy
foldl op acc str = withString str (loop acc)
  where
    loop : accTy -> (1 it : StringIterator str) -> accTy
    loop acc it =
      case uncons str it of
        EOF => acc
        Character c it' => loop (acc `op` c) (assert_smaller it it')

export
unpack : String -> LazyList Char
unpack str = runIdentity $ withString str unpack'
  where
    -- This is a Functor instance of Identity, but linear in second argument
    %inline
    mapId : forall a, b. (a -> b) -> (1 x : Identity a) -> Identity b
    mapId f (Id x) = Id (f x)

    unpack' : (1 it : StringIterator str) -> Identity (Lazy (LazyList Char))
    unpack' it =
      case uncons str it of
        EOF => pure []
        Character c it' => mapId (c ::) (unpack' $ assert_smaller it it')


text:
import public Lightyear
import public Lightyear.Char
import public Lightyear.Strings

data Expression
  = Numeral Integer
  | Plus Expression Expression
  | Minus Expression Expression
  | Times Expression Expression
  | Divide Expression Expression
  | Negate Expression

E : Type
E = Expression

mutual
  Show Expression where
    show (Numeral n) = "(Numeral " ++ (show n) ++ ")"
    show (Plus l r) = _show "Plus" l r
    show (Minus l r) = _show "Minus" l r
    show (Times l r) = _show "Times" l r
    show (Divide l r) = _show "Divide" l r
    show (Negate e) = "(Negate " ++ (show e) ++ ")"

  _show : String -> Expression -> Expression -> String
  _show x l r = "(" ++ x ++ " " ++ (show l) ++ " " ++ (show r) ++ ")"

numeral : Parser Expression
numeral = do i <- integer
             pure (Numeral i)

minus : Parser ()
minus = token "-"

lparen : Parser ()
lparen = token ("(")

rparen : Parser ()
rparen = token (")")

infixOp : Parser () -> (E -> E -> E) -> Parser (E -> E -> E)
infixOp l ctor = do
  _ <- l
  pure ctor

addOp : Parser (Expression -> Expression -> Expression)
addOp = infixOp (token "+") Plus <|> infixOp (token "-") Minus

mulOp : Parser (Expression -> Expression -> Expression)
mulOp = infixOp (token "*") Times <|> infixOp (token "/") Times

mutual
  expression : Parser Expression
  expression = chainl1 term addOp

  term : Parser Expression
  term = chainl1 factor mulOp

  negate : Parser Expression
  negate = do
    _ <- minus
    f <- factor
    pure $ Negate f

  subExp : Parser Expression
  subExp = do
    _ <- lparen
    expr <- expression
    _ <- rparen
    pure expr

  factor : Parser Expression
  factor = spaces *>
           (numeral
           <|> subExp
           <|> negate) <* spaces

max_stars_repo_name: alexhumphreys/pl-playground

max_issues_repo_name: alexhumphreys/pl-playground

max_forks_repo_name: alexhumphreys/pl-playground


text:
import Data.List

data MySnocList : List a -> Type where
     Empty : MySnocList []
     Snoc : (x, xs : _) -> (rec : MySnocList xs) -> MySnocList (xs ++ [x])

snocListHelp : {input : _} -> (snoc : MySnocList input) -> (rest : List a) -> MySnocList (input ++ rest)
snocListHelp snoc [] = rewrite appendNilRightNeutral input in snoc
snocListHelp snoc (x :: xs) = rewrite appendAssociative input [x] xs
                              in snocListHelp (Snoc x input snoc) xs

mySnocList : (xs : List a) -> MySnocList xs
mySnocList [] = Empty
mySnocList xs = snocListHelp Empty xs

myReverseHelper : (input : List a) -> MySnocList input -> List a
myReverseHelper [] Empty = []
myReverseHelper (xs ++ [x]) (Snoc x xs rec) = x :: myReverseHelper xs rec

-- myReverse : List a -> List a
-- myReverse input = myReverseHelper input (mySnocList input)

myReverse : List a -> List a
myReverse input with (mySnocList input)
  myReverse [] | Empty = []
  myReverse (xs ++ [x]) | (Snoc x xs rec) = x :: myReverse xs | rec

isSuffix : Eq a => List a -> List a -> Bool
isSuffix xs ys with (mySnocList xs, mySnocList ys)
  isSuffix _ _ | (Snoc x xs xsrec, Snoc y ys ysrec) = (x == y) && (isSuffix _ _ | (xsrec, ysrec))
  isSuffix _ _ | (Empty, s) = True
  isSuffix _ _ | (s, Empty) = False


text:
module Data.Foldable.Extras

%default total
%access export

iter : Foldable t => Monad m => (a -> m ()) -> t a -> m ()
iter f = foldlM (\(), x => f x) ()

max_stars_repo_name: jheiling/idris-extras

max_issues_repo_name: jheiling/idris-extras

max_forks_repo_name: jheiling/idris-extras


text:
module LazyLazy

import Data.List as L
import Data.List.Lazy

%default total

coef : Nat
coef = 10000

longId : Nat -> Nat
longId n = foldr max n $ L.replicate n n

level3 : LazyList Nat
level3 = iterateN coef (+1) 0 >>= replicate coef . longId >>= replicate coef . longId

main : IO ()
main = putStrLn $ show $ head' level3

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
module Linear

import ZZ
import Rationals
import Data.Vect
import GCDZZ
import ZZUtils

%default total
%access public export

-- Old code. It has been superseded by DiophantineSolver.

{-

NatToZZ: Nat -> ZZ
NatToZZ Z = 0
NatToZZ (S k) = (NatToZZ k) + 1

FST: (Nat,Nat) -> Nat --some issues with fst
FST (a, b) = a

SND: (Nat,Nat) -> Nat --some issues with snd
SND (a, b) = b

findSignDiff: (b: ZZ) -> (c: ZZ) -> ZZ
findSignDiff b c = if (b>c) then 1 else if (b<c) then (-1) else 0

-- The old Euclid division function. Although Vrunda wrote an updated version which is total, I needed this one
-- as I don't want to pass a proof to the QuotRem function right now.

Eucl: (a: Nat) -> (b: Nat) -> (Nat, Nat)
Eucl Z b = (Z,Z)
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 => (Z, S k)

isFactor : Nat -> Nat -> Type
isFactor m n = (k : Nat ** (m * k = n)) -- will be useful in solving Diophantine equations:
                                        -- if the denominator is a factor of the numerator, there is an integer solution

is_a_zero: (a: ZZ) -> Bool
is_a_zero (Pos Z) = True
is_a_zero (Pos (S k)) = False
is_a_zero (NegS k) = False
-}

data SolExists : Type where
  YesExists : SolExists
  DNExist : SolExists

ApZZ : (f: ZZ -> ZZ)-> n = m -> f n = f m -- like apNat, but for ZZ
ApZZ f Refl = Refl

-- Helper functions for the case ax = 0 --

ZeroSum: (a: ZZ) -> (b: ZZ) -> (a = 0) -> (b = 0) -> (a + b = 0) --sum of two zeroes is zero
ZeroSum a b prf prf1 = rewrite prf in
                       rewrite (plusZeroLeftNeutralZ (b)) in
                        prf1

triviality1: (a: ZZ) -> (b: ZZ) -> (b = 0) -> (a*b=0) -- premultiplying 0 by anything returns 0
triviality1 a b prf = trans (apZZ (\x => a*x) b 0 prf) (multZeroRightZeroZ(a))

triviality2: (a: ZZ) -> (0*a=0) -- 0 times anything is zero
triviality2 a = multZeroLeftZeroZ(a)

triviality3: (a: ZZ) -> (a*0=0) -- 0 times anything is zero
triviality3 a = multZeroRightZeroZ(a)

ZeroProof: (a: ZZ) -> (b: ZZ) -> (b = 0) -> (0*a + 1*b = 0) -- shows that the rational number (0,1) satisfies ax = 0
ZeroProof a b prf = trans (trans (ApZZ (\x=> x + 1*b) (triviality2 a)) (ApZZ (\x => 0 + x) (triviality1 1 b prf))) (ZeroSum 0 0 Refl Refl)

-- Helper functions for the case ax + b = 0

triviality4: (a: ZZ) -> (b: ZZ) -> (a*b = b*a)
triviality4 a b = multCommutativeZ a (b)

triviality5: (a: ZZ) -> (b: ZZ) -> (a*(-b)+b*a = a*(-b) + a*b )
triviality5 a b = ApZZ (\x=> a*(-b) + x) (triviality4 b a)

triviality6: (a: ZZ) -> (b: ZZ) -> ( (a*(-b)) + (a*b) = a*( (-b)+b ) )
triviality6 a b = sym ( multDistributesOverPlusRightZ a (-b) b )

triviality7: (a: ZZ) -> (b: ZZ) -> ( a*((-b) + b) = 0)
triviality7 a b = trans (ApZZ (\x => a*x) (plusNegateInverseRZ(b))) (triviality3(a))

SolutionProof: (a: ZZ) -> (b: ZZ) -> (a*(-b)+b*a=0)
SolutionProof a b = trans (trans (triviality5 a b) (triviality6 a b)) (triviality7 a b)

--Solving a linear equation ax + b = 0 in the case when b = 0 (Basically, this shows that ax=0 is uniquely solved by (0,1))

trivialeqSolver : (a: ZZ) -> (b : ZZ) -> (b = 0) -> Either (x : ZZPair ** ( (SolExists, (( (fst x)*a + (snd x)*b = 0 ),(NotZero (snd x)))))) (SolExists)
trivialeqSolver a b prf = Left (((0,1) ** (YesExists, ((ZeroProof a b prf), PositiveZ))))

-- Solving the linear equation ax+b = 0 in general

eqSolver : (a: ZZ) -> (b : ZZ) -> (NotZero a) -> (NotZero b) -> Either (x : ZZPair ** ( (SolExists, a*(fst x) + b*(snd x) = 0), NotZero (snd x)) ) (SolExists)
eqSolver a b x y = Left ((-b, a) ** ((YesExists, (SolutionProof a b)), x)) -- The solution is (-b/a), a rational number, with proof.

-- Helper functions for ax + b = c

helper1: (a: ZZ) -> (b: ZZ) -> (c: ZZ) -> (a*(c+(-b))= a*c + a*(-b))
helper1 a b c = multDistributesOverPlusRightZ (a) (c) (-b)

helper2: (a: ZZ) -> (b: ZZ) -> (c: ZZ) -> ( a*(c-b) + b*a = a*c+ a*(-b)+ b*a )
helper2 a b c = ApZZ (\x => x+ b*a) (helper1 (a) (b) (c))

helper3: (a: ZZ) -> (b: ZZ) -> (a*(-b)+b*a= 0)
helper3 a b = trans (trans (triviality5 a b) (triviality6 a b)) (triviality7 a b)

helper4: (a: ZZ) -> (b: ZZ) -> (c: ZZ) -> (a*c + a*(-b) + b*a = a*c)
helper4 a b c = rewrite sym (plusAssociativeZ (a*c) (a*(-b)) (b*a)) in
                rewrite helper3 a b in
                rewrite plusZeroRightNeutralZ (multZ a c) in Refl

GeneralProof: (a: ZZ) -> (b: ZZ) -> (c: ZZ) -> ( a*(c-b) + b*a = a*c )
GeneralProof a b c = trans (helper2 a b c) (helper4 a b c)

-- Solving the linear equation ax + b = c (2x +3 = 7, for example) over the rationals

GeneralEqSolver: (a: ZZ) -> (b: ZZ) -> (c: ZZ) -> (a0: NotZero a) ->
  (x : ZZPair ** ( (SolExists, a*(fst x) + b*(snd x) = (snd x)*c), (NotZero (snd x))) )
GeneralEqSolver a b c a0 = ( ( (c-b) , a ) ** ( (YesExists, (GeneralProof a b c)), a0 )) -- Solves the equation with proof

{-

-- This is previously used code. It has been superseded by DiophantineSolver

-- Now, we can use the rational solution of the linear equation ax + b = c to check whether this equation has an integer
-- solution; if it did, the denominator of the rational solution would divide the numerator. If it didn't, the equation
-- would have no solutions in the integers.

IsSolutionZ: (a: ZZ) -> (b: ZZ) -> (c: ZZ) -> (a0: NotZero a) -> Either (ZZPair) (ZZ)
IsSolutionZ a b c a0 = case (SND (Eucl (absZ(c-b)) (absZ a) )) of
                            Z => Right ((NatToZZ(FST (Eucl (absZ(c-b)) (absZ a) )))*(findSignDiff c b))
                            (S k) => Left((c-b),a)

-}

-- some helper functions for the DiophantineProof

helper5: (quot: ZZ) -> (a: ZZ) -> (quot*a=a*quot)
helper5 quot a = multCommutativeZ (quot) (a)

helper6: (a: ZZ) -> (b: ZZ) -> (c: ZZ) -> (quot: ZZ) -> (c-b=quot*a) -> (c-b=a*quot)
helper6 a b c quot prf = trans (prf) (helper5 (quot) (a))

helper7: (a: ZZ) -> (b: ZZ) -> (c: ZZ) -> (quot: ZZ) -> (c-b=a*quot) -> ((c-b+b)=a*quot+b)
helper7 a b c quot prf = ApZZ (\x => x+ b) (prf)

helper8: (b: ZZ) -> (-b+b=0)
helper8 b = plusNegateInverseRZ b

helper10: (c: ZZ) -> (b: ZZ) -> ((c-b)+b=c)
helper10 c b = rewrite sym (plusAssociativeZ (c) (-b) (b)) in
               rewrite plusNegateInverseRZ (b) in
               rewrite plusZeroRightNeutralZ c in
               Refl

helper11: (a: ZZ) -> (b: ZZ) -> (c: ZZ) -> (quot: ZZ) -> (c-b=a*quot) -> (c=a*quot+b)
helper11 a b c quot prf = trans (sym (helper10 c b)) (helper7 a b c quot prf)

-- If a Diophantine equation has a solution, this generates the proof.

DiophantineProof: (a: ZZ) -> (b: ZZ) -> (c: ZZ) -> (quot: ZZ) -> (c-b=quot*a) -> ((a*quot+b=c))
DiophantineProof a b c quot x = sym (helper11 (a) (b) (c) (quot) (helper6 a b c quot x))

--This solves the equation ax+b=c and if it has an integer solution, it generates the solution with proof.

DiophantineSolver: (a: ZZ) -> (b: ZZ) -> (c: ZZ) -> (a0: NotZero a)
-> Either (x: ZZ ** (a*x+b=c)) (x : ZZPair ** ( (SolExists, a*(fst x) + b*(snd x) = (snd x)*c), (NotZero (snd x))) )
DiophantineSolver a b c a0 = case (CheckIsQuotientZ (c-b) (a) a0) of
                                  (Left l) => Left ((fst l) ** (DiophantineProof a b c (fst l) (snd l)))
                                  (Right r) => Right (GeneralEqSolver a b c (a0))

 -- Now, for 2 variable Diophantine equations

||| The solution of the homogeneous equation ax + by =0 is any integer multiple of (-b,a)
homogeneous: (a: ZZ) -> (b: ZZ) -> (k: ZZ) -> ((a*(k*(-b))+b*(k*a))=0)
homogeneous a b k = rewrite (multAssociativeZ (a) (k) (-b)) in
                    rewrite (multCommutativeZ (a) (k)) in
                    rewrite (multAssociativeZ (b) (k) (a)) in
                    rewrite (multCommutativeZ (b) (k)) in
                    rewrite sym (multAssociativeZ (k) (a) (-b)) in
                    rewrite sym (multAssociativeZ (k) (b) (a)) in
                    rewrite sym (multDistributesOverPlusRightZ k (a*(-b)) (b*a)) in
                    rewrite (SolutionProof (a) (b)) in
                    rewrite multZeroRightZeroZ k in
                    Refl


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

import public Minecraft.Base.PreClassic.Cobblestone
import public Minecraft.Core.Item.Export
import public Minecraft.Core.Item.Put.Export
import public Minecraft.Data.Type.Vtbl

%default total

namespace Export
  public export %hint cobblestoneItem : Item Cobblestone.Item
  public export %hint putCobblestone  : Put  Cobblestone.Item
  public export %hint cobblestoneVtbl : Vtbl Cobblestone.Item

max_stars_repo_name: po-stulate/postulate

max_issues_repo_name: po-stulate/postulate

max_forks_repo_name: po-stulate/postulate


text:
CBool : Type
CBool = (B : Type) -> B -> B -> B

toBool : CBool -> Bool
toBool = \b => b Bool True False

ctrue : CBool
ctrue = \b, t, f => t

and : CBool -> CBool -> CBool
and = \a, b, bb, t, f => a bb (b bb t f) f

CNat : Type
CNat = (n : Type) -> (n -> n) -> n -> n

add : CNat -> CNat -> CNat
add = \a, b, n, s, z => a n s (b n s z)

cmul : CNat -> CNat -> CNat
cmul = \a, b, n, s => a n (b n s)

suc : CNat -> CNat
suc = \a, n, s, z => s (a n s z)

CEq : {A : Type} -> A -> A -> Type
CEq = \x, y => (P : A -> Type) -> P x -> P y

crefl : {A : Type} -> {x : A} -> CEq {A} x x
crefl = \p, px => px

n2 : CNat
n2 = \n, s, z => s (s z)

n3 : CNat
n3 = \n, s, z => s (s (s z))

n4 : CNat
n4 = \n, s, z => s (s (s (s z)))

n5 : CNat
n5 = \n, s, z => s (s (s (s (s z))))

n10 : CNat
n10  = cmul n2 n5

n10b : CNat
n10b = cmul n5 n2

n15 : CNat
n15 = add n10  n5

n15b : CNat
n15b   = add n10b n5

n18 : CNat
n18    = add n15  n3

n18b : CNat
n18b   = add n15b n3

n19 : CNat
n19    = add n15  n4

n19b : CNat
n19b   = add n15b n4

n20 : CNat
n20    = cmul n2 n10

n20b : CNat
n20b   = cmul n2 n10b

n21 : CNat
n21    = suc n20

n21b : CNat
n21b   = suc n20b

n22 : CNat
n22    = suc n21

n22b : CNat
n22b   = suc n21b

n23 : CNat
n23    = suc n22

n23b : CNat
n23b   = suc n22b

n100 : CNat
n100   = cmul n10   n10

n100b : CNat
n100b  = cmul n10b  n10b

n10k : CNat
n10k   = cmul n100  n100

n10kb : CNat
n10kb  = cmul n100b n100b

n100k : CNat
n100k  = cmul n10k  n10

n100kb : CNat
n100kb = cmul n10kb n10b

n1M : CNat
n1M    = cmul n10k  n100

n1Mb : CNat
n1Mb   = cmul n10kb n100b

n5M : CNat
n5M    = cmul n1M   n5

n5Mb : CNat
n5Mb   = cmul n1Mb  n5

n10M : CNat
n10M   = cmul n5M   n2

n10Mb : CNat
n10Mb  = cmul n5Mb  n2

Tree : Type
Tree = (T : Type) -> (T -> T -> T) -> T -> T

leaf : Tree
leaf = \t, n, l => l

node : Tree -> Tree -> Tree
node = \t1, t2, t, n, l => n (t1 t n l) (t2 t n l)

fullTree : CNat -> Tree
fullTree = \n => n Tree (\t => node t t) leaf

-- full tree with given trees at bottom level
fullTreeWithLeaf : Tree -> CNat -> Tree
fullTreeWithLeaf = \bottom, n => n Tree (\t => node t t) bottom

forceTree : Tree -> CBool
forceTree = \t => t CBool and ctrue

t15 : Tree
t15  = fullTree n15
t15b : Tree
t15b = fullTree n15b
t18 : Tree
t18  = fullTree n18
t18b : Tree
t18b = fullTree n18b
t19 : Tree
t19  = fullTree n19
t19b : Tree
t19b = fullTree n19b
t20 : Tree
t20  = fullTree n20
t20b : Tree
t20b = fullTree n20b
t21 : Tree
t21  = fullTree n21
t21b : Tree
t21b = fullTree n21b
t22 : Tree
t22  = fullTree n22
t22b : Tree
t22b = fullTree n22b
t23 : Tree
t23  = fullTree n23
t23b : Tree
t23b = fullTree n23b

-- CNat conversion
--------------------------------------------------------------------------------

-- convn1M : CEq Main.n1M Main.n1Mb
-- convn1M = crefl

-- convn5M : CEq Main.n5M Main.n5Mb
-- convn5M = crefl

-- convn10M : CEq Main.n10M Main.n10Mb
-- convn10M = crefl

-- Full tree conversion
--------------------------------------------------------------------------------

-- convt15  : CEq Main.t15  Main.t15b
-- convt15  = crefl
-- convt18  : CEq Main.t18  Main.t18b
-- convt18  = crefl
-- convt19  : CEq Main.t19  Main.t19b
-- convt19  = crefl
-- convt20  : CEq Main.t20  Main.t20b
-- convt20  = crefl
-- convt21  : CEq Main.t21  Main.t21b
-- convt21  = crefl
-- convt22  : CEq Main.t22  Main.t22b
-- convt22  = crefl
-- convt23  : CEq Main.t23  Main.t23b
-- convt23  = crefl

-- Full meta-containing tree conversion
--------------------------------------------------------------------------------

-- convmt15 : CEq Main.t15b  (fullTreeWithLeaf ? Main.n15 )
-- convmt15 = crefl
-- convmt18 : CEq Main.t18b  (fullTreeWithLeaf ? Main.n18 )
-- convmt18 = crefl
-- convmt19 : CEq Main.t19b  (fullTreeWithLeaf ? Main.n19 )
-- convmt19 = crefl
-- convmt20 : CEq Main.t20b  (fullTreeWithLeaf ? Main.n20 )
-- convmt20 = crefl
-- convmt21 : CEq Main.t21b  (fullTreeWithLeaf ? Main.n21 )
-- convmt21 = crefl
-- convmt22 : CEq Main.t22b  (fullTreeWithLeaf ? Main.n22 )
-- convmt22 = crefl
-- convmt23 : CEq Main.t23b  (fullTreeWithLeaf ? Main.n23 )
-- convmt23 = crefl

-- Full tree forcing
--------------------------------------------------------------------------------

-- forcet15 : CEq (toBool (forceTree Main.t15)) True
-- forcet15 = crefl
-- forcet18 : CEq (toBool (forceTree Main.t18)) True
-- forcet18 = crefl
-- forcet19 : CEq (toBool (forceTree Main.t19)) True
-- forcet19 = crefl
-- forcet20 : CEq (toBool (forceTree Main.t20)) True
-- forcet20 = crefl
-- forcet21 : CEq (toBool (forceTree Main.t21)) True
-- forcet21 = crefl
forcet22 : CEq (toBool (forceTree Main.t22)) True
forcet22 = crefl
-- forcet23 : CEq (toBool (forceTree Main.t23)) True
-- forcet23 = crefl

max_stars_repo_name: Kha/smalltt

max_issues_repo_name: Kha/smalltt

max_forks_repo_name: Kha/smalltt


text:
module Core.Directory

import Core.Context
import Core.Context.Log
import Core.Core
import Core.FC
import Core.Name
import Core.Options
import Libraries.Utils.Path

import Data.List
import Data.String
import Data.Maybe

import System.Directory
import System.File
import System.Info

%default total

public export
data IdrSrcExt = E_idr | E_lidr | E_yaff | E_org | E_md

public export
Eq IdrSrcExt where
  E_idr  == E_idr  = True
  E_lidr == E_lidr = True
  E_yaff == E_yaff = True
  E_org  == E_org  = True
  E_md   == E_md   = True
  _      == _      = False

public export
Show IdrSrcExt where
  show E_idr  = "idr"
  show E_lidr = "lidr"
  show E_yaff = "yaff"
  show E_org  = "org"
  show E_md   = "md"

public export
listOfExtensions : List IdrSrcExt
listOfExtensions = [E_idr, E_lidr, E_yaff, E_org, E_md]

-- Return the name of the first file available in the list
-- Used in LSP.
export
firstAvailable : {auto c : Ref Ctxt Defs} ->
                 List String -> Core (Maybe String)
firstAvailable [] = pure Nothing
firstAvailable (f :: fs)
    = do log "import.file" 30 $ "Attempting to read " ++ f
         Right ok <- coreLift $ openFile f Read
               | Left err => firstAvailable fs
         coreLift $ closeFile ok
         pure (Just f)

export
covering
findDataFile : {auto c : Ref Ctxt Defs} ->
               String -> Core String
findDataFile fname
    = do d <- getDirs
         let fs = map (\p => p </> fname) (data_dirs d)
         Just f <- firstAvailable fs
            | Nothing => throw (InternalError ("Can't find data file " ++ fname ++
                                               " in any of " ++ show fs))
         pure f

export
covering
readDataFile : {auto c : Ref Ctxt Defs} ->
               String -> Core String
readDataFile fname
    = do f <- findDataFile fname
         Right d <- coreLift $ readFile f
            | Left err => throw (FileErr f err)
         pure d

-- Look for a library file required by a code generator. Look in the
-- library directories, and in the lib/ subdirectoriy of all the 'extra import'
-- directories
export
findLibraryFile : {auto c : Ref Ctxt Defs} ->
                  String -> Core String
findLibraryFile fname
    = do d <- getDirs
         let fs = map (\p => p </> fname)
                      (lib_dirs d ++ map (\x => x </> "lib")
                                         (extra_dirs d))
         Just f <- firstAvailable fs
            | Nothing => throw (InternalError ("Can't find library " ++ fname))
         pure f

-- Given a namespace, return the full path to the checked module,
-- looking first in the build directory then in the extra_dirs
export
nsToPath : {auto c : Ref Ctxt Defs} ->
           FC -> ModuleIdent -> Core (Either Error String)
nsToPath loc ns
    = do d <- getDirs
         let fnameBase = ModuleIdent.toPath ns
         let fs = map (\p => p </> fnameBase <.> "ttc")
                      ((build_dir d </> "ttc") :: extra_dirs d)
         Just f <- firstAvailable fs
            | Nothing => pure (Left (ModuleNotFound loc ns))
         pure (Right f)

-- Given a namespace, return the path to the source module relative
-- to the working directory, if the module exists.
export
nsToSource : {auto c : Ref Ctxt Defs} ->
             FC -> ModuleIdent -> Core String
nsToSource loc ns
    = do d <- getDirs
         let fnameOrig = ModuleIdent.toPath ns
         let fnameBase = maybe fnameOrig (\srcdir => srcdir </> fnameOrig) (source_dir d)
         let fs = map ((fnameBase <.>) . show) listOfExtensions
         Just f <- firstAvailable fs
            | Nothing => throw (ModuleNotFound loc ns)
         pure f

-- Given a filename in the working directory + source directory, return the correct
-- namespace for it
export
mbPathToNS : String -> Maybe String -> String -> Maybe ModuleIdent
mbPathToNS wdir sdir fname =
  let
    sdir = fromMaybe "" sdir
    base = if isAbsolute fname then wdir </> sdir else sdir
  in
    unsafeFoldModuleIdent . reverse . splitPath . Path.dropExtension
      <$> Path.dropBase base fname

export
corePathToNS : String -> Maybe String -> String -> Core ModuleIdent
corePathToNS wdir sdir fname = do
  let err = UserError $
          "Source file "
       ++ show fname
       ++ " is not in the source directory "
       ++ show (wdir </> fromMaybe "" sdir)
  maybe (throw err) pure (mbPathToNS wdir sdir fname)

export
ctxtPathToNS : {auto c : Ref Ctxt Defs} -> String -> Core ModuleIdent
ctxtPathToNS fname = do
  defs <- get Ctxt
  let wdir = defs.options.dirs.working_dir
  let sdir = defs.options.dirs.source_dir
  corePathToNS wdir sdir fname

dirExists : String -> IO Bool
dirExists dir = do Right d <- openDir dir
                       | Left _ => pure False
                   closeDir d
                   pure True

-- Create subdirectories, if they don't exist
export
covering
mkdirAll : String -> IO (Either FileError ())
mkdirAll dir = if parse dir == emptyPath
                  then pure (Right ())
                  else do exist <- dirExists dir
                          if exist
                             then pure (Right ())
                             else do Right () <- case parent dir of
                                          Just parent => mkdirAll parent
                                          Nothing => pure (Right ())
                                        | err => pure err
                                     createDir dir

-- Given a namespace (i.e. a module name), make the build directory for the
-- corresponding ttc file
export
covering
makeBuildDirectory : {auto c : Ref Ctxt Defs} ->
                     ModuleIdent -> Core ()
makeBuildDirectory ns
    = do d <- getDirs
         let bdir = build_dir d </> "ttc"
         let ns = reverse $ fromMaybe [] $ tail' $ unsafeUnfoldModuleIdent ns -- first item is file name
         let ndir = joinPath ns
         Right _ <- coreLift $ mkdirAll (bdir </> ndir)
            | Left err => throw (FileErr (build_dir d </> ndir) err)
         pure ()

export
covering
ensureDirectoryExists : String -> Core ()
ensureDirectoryExists dir
    = do Right _ <- coreLift $ mkdirAll dir
            | Left err => throw (FileErr dir err)
         pure ()

-- Given a source file, return the name of the ttc file to generate
export
getTTCFileName : {auto c : Ref Ctxt Defs} ->
                 String -> String -> Core String
getTTCFileName inp ext
    = do -- Get its namespace from the file relative to the working directory
         -- and generate the ttc file from that
         ns <- ctxtPathToNS inp
         let fname = ModuleIdent.toPath ns <.> ext
         d <- getDirs
         let bdir = build_dir d
         pure $ bdir </> "ttc" </> fname

-- Given a source file, return the name of the corresponding object file.
-- As above, but without the build directory
export
getObjFileName : {auto c : Ref Ctxt Defs} ->
                 String -> String -> Core String
getObjFileName inp ext
    = do -- Get its namespace from the file relative to the working directory
         -- and generate the ttc file from that
         ns <- ctxtPathToNS inp
         let fname = ModuleIdent.toPath ns <.> ext
         pure $ fname

-- Given a root executable name, return the name in the build directory
export
getExecFileName : {auto c : Ref Ctxt Defs} -> String -> Core String
getExecFileName efile
    = do d <- getDirs
         pure $ build_dir d </> efile

getEntries : Directory -> IO (List String)
getEntries d
    = do Right f <- dirEntry d
             | Left err => pure []
         ds <- assert_total $ getEntries d
         pure (f :: ds)

dirEntries : String -> IO (Either FileError (List String))
dirEntries dir
    = do Right d <- openDir dir
             | Left err => pure (Left err)
         ds <- getEntries d
         closeDir d
         pure (Right ds)

-- Find an ipkg file in any of the directories above this one
-- returns the directory, the ipkg file name, and the directories we've
-- gone up
export
covering
findIpkgFile : IO (Maybe (String, String, String))
findIpkgFile
    = do Just dir <- currentDir
              | Nothing => pure Nothing
         res <- findIpkgFile' dir ""
         pure res
  where
    covering
    findIpkgFile' : String -> String -> IO (Maybe (String, String, String))
    findIpkgFile' dir up
        = do Right files <- dirEntries dir
                 | Left err => pure Nothing
             let Just f = find (\f => extension f == Just "ipkg") files
                 | Nothing => case splitParent dir of
                                   Just (parent, end) => findIpkgFile' parent (end </> up)
                                   Nothing => pure Nothing
             pure $ Just (dir, f, up)


text:
import Data.Vect
import Data.List.Views
import Data.Vect.Views
import Data.Nat.Views

-- Page 270
-- Exercise 1
data TakeN : List a -> Type where
  Fewer : TakeN xs
  Exact : (n_xs : List a) -> TakeN (n_xs ++ rest)

takeN : (n : Nat) -> (xs : List a) -> TakeN xs
takeN Z _ = Exact []
takeN (S k) [] = Fewer
takeN (S k) (x :: xs) = case takeN k xs of
                             Fewer => Fewer
                             Exact n_xs => Exact (x :: n_xs)

groupByN : (n : Nat) -> (xs : List a) -> List (List a)
groupByN n xs with (takeN n xs)
  groupByN n xs | Fewer = [xs]
  groupByN n (n_xs ++ rest) | (Exact n_xs) = n_xs :: groupByN n rest

-- Exercise 2
halves : List a -> (List a, List a)
halves xs with (takeN ((length xs) `div` 2) xs)
  halves xs | Fewer = ([], xs)
  halves (n_xs ++ rest) | Exact (n_xs) = (n_xs, rest)

-- Page 279
-- Exercise 1
equalSuffix : Eq a => List a -> List a -> List a
equalSuffix x y with (snocList x)
  equalSuffix [] y | Empty = []
  equalSuffix (xs ++ [x_item]) y | (Snoc recX) with (snocList y)
    equalSuffix (xs ++ [x_item]) [] | (Snoc recX) | Empty = []
    equalSuffix (xs ++ [x_item]) (ys ++ [y_item]) | (Snoc recX) | (Snoc recY) =
      if x_item == y_item then equalSuffix xs ys | recX | rexY ++ [x_item] else []

-- Exercise 4
total
palindrome : Eq a => List a -> Bool
palindrome xs with (vList xs)
  palindrome [] | VNil = True
  palindrome [x] | VOne = True
  palindrome (first :: (ys ++ [last])) | (VCons rec) =
    (first == last) && palindrome ys | rec

-- Page 287
-- Exercise 2
export
data Shape = Triangle Double Double
           | Rectangle Double Double
           | Circle Double
{-
area : Shape -> Double
area s with (shapeView s)
  area (triangle base height) | STriangle = ?area_rhs_1
  area (rectangle width height) | SRectangle = ?area_rhs_2
  area (circle radius) | SCircle = ?area_rhs_3
-}

-- Page 304
-- Exercise 1
total
every_other : Stream a -> Stream a
every_other (x :: _ :: xs) = x :: every_other xs

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

%name InfList xs, ys, zs

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

-- Exercise 4
total
square_root_approx : (number : Double) -> (approx : Double) -> Stream Double
square_root_approx number approx =
  let next = (approx + (number / approx)) / 2 in -- Newton's method
  approx :: square_root_approx number next

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

total
square_root : (number : Double) -> Double
square_root number =
  let recursiveCall = square_root_approx number number in
  square_root_bound 100 number 0.00000000001 recursiveCall

-- Page 314
-- Exercise 1
data InfIO : Type where
  Do : IO a
       -> (a -> Inf InfIO)
       -> InfIO

total
totalREPL : (prompt : String) -> (action : String -> String) -> InfIO
totalREPL prompt action = Do (putStrLn prompt) (\_ => totalREPL prompt action)

-- Page 322
-- Exercise 1
-- (Done in class)

max_stars_repo_name: JnxF/advanced-software-analysis

max_issues_repo_name: JnxF/advanced-software-analysis

max_forks_repo_name: JnxF/advanced-software-analysis


text:
module Main

import IdrisUnit
import Control.App
import Control.App.Console

hanoi : Int -> a -> a -> a -> List (a, a)
hanoi 0 a b c = []
hanoi 1 a b c = [(a, c)]
hanoi n a b c = hanoi (n-1) a c b ++ [(a, c)] ++ hanoi (n-1) b a c

spec : Spec es => App es ()
spec = do
    describe "example" $ do
        context "arith" $ do
            it "1+1 = 2" $ do
                1+1 `shouldBe` 2
            it "1*1 = 1" $ do
                1*1 `shouldBe` 1
    describe "hanoi" $ do
        it "3 level" $ do
            hanoi 3 'A' 'B' 'C' `shouldBe` [('A', 'C'), ('A', 'B'), ('C', 'B'), ('A', 'C'), ('B', 'A'), ('B', 'C'), ('A', 'C')]
        it "4 level" $ do
            hanoi 4 'A' 'B' 'C' `shouldBe` [('A', 'B'), ('A', 'C'), ('B', 'C'), ('A', 'B'), ('C', 'A'), ('C', 'B'), ('A', 'B'), ('A', 'C'), ('B', 'C'), ('B', 'A'), ('C', 'A'), ('B', 'C'), ('A', 'B'), ('A', 'C'), ('B', 'C')]

main : IO ()
main = run spec

max_stars_repo_name: dannypsnl/idris-unit

max_issues_repo_name: dannypsnl/idris-unit

max_forks_repo_name: dannypsnl/idris-unit