text:
> module SequentialDecisionProblems.CoreTheory

> import Sigma.Sigma
> import Sigma.Operations

> %default total
> %access public export
> %auto_implicits off

* Preliminaries

In a nutshell, the core theory introduces the notion of policy, policy
sequence, optimality of policy sequences and implements a generic
backwards induction algorithm |backwardsInduction| for computing optimal
policy sequences.

However, the core theory does not implement a machine checkable proof
that |backwardsInduction| is correct that is, that its result is an
optimal policy sequence.

This is done in the full theory presented in |FullTheory|. Both here and
in |FullTheory|, the assumptions are implemented as holes
(metavariables, forward declarations, partial definitions, etc.). The
idea is that users that wish to apply the theory (typically, for
computing optimal solutions for a specific decision problem) will
fill-in the holes by providing problem-specific implementations.

* Sequential decision processes

A sequential decision problem (SDP) is specified in terms of, among
others, its underlying decision process.

In a decision process, a decision maker is required to perform a number
of decision steps. At each step, the decision maker is in (observes) a
state and is required to select a control (action, option). The idea is
that, upon selecting a control in a given state, the decision maker will
enter (observe) a new state. In a deterministic decision process, such
new state is uniquely defined in terms of the current decision step,
state and selected control. But in decision processes under uncertainty,
the decision maker only knows which new states are "possible" (again,
for a given decision step, "current" state and selected control) and,
perhaps, their probabilities. But it does not know which one will
actually occur.

Thus, in order to specify a decision process, one has to first specify
what are the possible states at each decision step:

> State : (t : Nat) -> Type

Then, one has to explain which controls can be selected at a given step
and for a given state:

> Ctrl : (t : Nat) -> (x : State t) -> Type

Finally, one has to explain which "next" states are possible at a given
decision step, in a given state and for a selected control. In the
deterministic case, one could provide such explanation by defining a
stepping function

< next : (t : Nat) -> (x : State t) -> (y : Ctrl t x) -> State (S t)

But what if the decision process has uncertain outcomes? In this case,
we follow an approach originally proposed by Ionescu [1] and generalize
|next| to a monadic transition function:

> M : Type -> Type

> nexts : (t : Nat) -> (x : State t) -> (y : Ctrl t x) -> M (State (S t))

For reasons that will become clear in the sequel, |M| is is required
to be a functor:

> fmap  :  {A, B : Type} ->
>          (A -> B) -> M A -> M B
> postulate functorSpec1  :  fmap . id = id
> postulate functorSpec2  :  {A, B, C : Type} -> {f : B -> C} -> {g : A -> B} ->
>                            fmap (f . g) = (fmap f) . (fmap g)

In the above specification and throughout this file, we use postulates
to denote assumptions that we consider to be conceptually relevant but
that are not necessary for the theory. Thus, strictly speaking, |M| is
not required to be a functor, just to implement |fmap|.

In specific decision processes, we expect |M| to be |Id| (deterministic
SDP), |List| (non-deterministic SDP) or |Prob| (stochastic SDP). But our
assumptions are general enough to specify other kinds of decision
processes.

* Sequential decision problems

In order to obtain a problem from a decision process, we introduce the
additional assumption that, with each transition from the current state
to a new state, the decision maker receives a certain reward (payoff,
etc.)

> Val : Type

> reward : (t : Nat) -> (x : State t) -> (y : Ctrl t x) -> (x' : State (S t)) -> Val

Since the original work of Bellman [1957], this has turned out to be a
useful abstraction. The idea is that the decision maker seeks controls
that maximize the sum of the rewards obtained in a decision
process. Thus, values of type |Val| have to be "addable"

> plus : Val -> Val -> Val

We will also need |Val| to be equipped with a "zero"

> zero : Val

and with a binary "comparison" relation

> LTE : Val -> Val -> Type

In a deterministic case, implementing the above assumptions completely
defines a sequential decision problem. But whenever a decision step has
an uncertain outcome, uncertainties about "next" states naturally yield
uncertainties about rewards. In these cases, the decision makes faces a
number of possible rewards (one for each possible next state) and has to
explain how it measures such chances. In stochastic decision problems,
possible next states (and, therefore possible rewards) are labelled with
probabilities. In these cases, possible rewards are often measured in
terms of their expected value.  Here, again, we follow the approach
proposed by Ionescu in [2] and introduce a measure

> meas : M Val -> Val

that characterizes how the decision maker values uncertainties about
rewards in a single decision step. It is possible that a decision maker
values uncertainties according to different measures at different
decision steps. This could be easily formalized by generalising

< meas : M Val -> Val

to

< meas : (t : Nat) -> (x : State t) -> (M Val -> Val)

* Solving sequential decision problems

Implementing the above holes defines a specific SDP unambiguously. But
in order to compute controls that maximize the sum of the rewards over
an arbitrary number of decision steps, we need to be able to assess that
all "next" states in an |M|-structure satisfy certain properties. This
requires |M| to be a "container":

> Elem     : {A : Type} -> A -> M A -> Type
> NotEmpty : {A : Type} -> M A -> Type
> All      : {A : Type} -> (P : A -> Type) -> M A -> Type
> tagElem  : {A : Type} -> (ma : M A) -> M (Sigma A (\ a => a `Elem` ma))

> allElemSpec0                 :  {A : Type} -> {P : A -> Type} ->
>                                 (a : A) -> (ma : M A) -> All P ma -> a `Elem` ma -> P a

> postulate elemNotEmptySpec0  :  {A : Type} ->
>                                 (a : A) -> (ma : M A) -> a `Elem` ma -> NotEmpty ma

> postulate elemNotEmptySpec1  :  {A : Type} ->
>                                 (ma : M A) -> NotEmpty ma -> Sigma A (\ a => a `Elem` ma)

> postulate tagElemSpec        :  {A : Type} -> (ma : M A) -> fmap outl (tagElem ma) = ma

The theory presented here relies on two further notions: viability and
reachability.

* Viability

Intuitively, a state |x : State t| is viable for |n| steps if, in spite
of the uncertainties of the decision process, one can make |n| decision
steps starting from |x| without bumping into a dead end. Here, dead ends
are states for which no controls are available. In concrete decision
problems, they could represent exceptional outcomes: aborting a
computation, running out of fuel, being shot dead.

> Viable : {t : Nat} -> (n : Nat) -> State t -> Type

Thus, every state is viable for zero steps

> postulate viableSpec0 : {t : Nat} ->
>                         (x : State t) -> Viable Z x

and a state is viable for |S n| steps iff there exists a control that
leads to a non-empty |M|-structure of next states which are viable for
|n| steps. We call such controls "good" controls:

> Good : (t : Nat) -> (x : State t) -> (n : Nat) -> (Ctrl t x) -> Type
> Good t x n y = (NotEmpty (nexts t x y), All (Viable {t = S t} n) (nexts t x y))

> GoodCtrl : (t : Nat) -> (x : State t) -> (n : Nat) -> Type
> GoodCtrl t x n = Sigma (Ctrl t x) (Good t x n)
> -- GoodCtrl t x n = Sigma (Ctrl t x) (\ y => (NotEmpty (nexts t x y), All (Viable {t = S t} n) (nexts t x y)))

> viableSpec1 : {t : Nat} -> {n : Nat} ->
>               (x : State t) -> Viable (S n) x -> GoodCtrl t x n

> postulate viableSpec2 : {t : Nat} -> {n : Nat} ->
>                         (x : State t) -> GoodCtrl t x n -> Viable (S n) x

Auxiliary functions:

> |||
> ctrl : {t, n : Nat} -> {x : State t} -> GoodCtrl t x n -> Ctrl t x
> ctrl (MkSigma y _) = y

> |||
> -- good : {t, n : Nat} -> {x : State t} -> (y : GoodCtrl t x n) -> Good t x n (ctrl y)
> -- good (MkSigma _ p) = p

> |||
> allViable : {t, n : Nat} -> {x : State t} -> (y : GoodCtrl t x n) -> All (Viable n) (nexts t x (ctrl y))
> allViable (MkSigma _ p) = snd p

* Reachability

Viability is, strictly speaking, all what is needed to formalize the
notion of policies as functions that associate "good" controls to
viable states.

But in a decision problem, not all viable states are actually
reachable. Thus, we would like to further restrict the domain of
policies to states that can actually be reached. Intuitively, a state is
reachable if there are controls that allow for a path from some initial
state to that state. Thus, tautologically, every initial state is
reachable:

> Reachable : {t' : Nat} -> State t' -> Type

> postulate reachableSpec0 : (x : State Z) -> Reachable x

Moreover, if |x| is reachable and admits a control |y|, then all states
that can be obtained by selecting |y| in |x| are also reachable:

> reachableSpec1  :  {t : Nat} -> (x : State t) -> Reachable x -> (y : Ctrl t x) -> All Reachable (nexts t x y)

And the other way round:

> Pred : {t : Nat} -> State t -> State (S t) -> Type
> Pred {t} x x'  =  Sigma (Ctrl t x) (\ y => x' `Elem` nexts t x y)

> ReachablePred : {t : Nat} -> State t -> State (S t) -> Type
> ReachablePred x x'  = (Reachable x, x `Pred` x')

> postulate reachableSpec2  :  {t : Nat} -> (x' : State (S t)) -> Reachable x' -> Sigma (State t) (\ x => x `ReachablePred` x')

* Policies and policy sequences

Policies are functions that associate to every state |x| at decision
step |t| which is reachable and viable for |S m| steps (from which |S
m| more decision steps are doable) a good control:

> Policy : (t : Nat) -> (n : Nat) -> Type
> Policy t Z      =  Unit
> Policy t (S m)  =  (x : State t) -> Reachable x -> Viable (S m) x -> GoodCtrl t x m

A policy sequence for making |n| decision steps starting from some
(reachable, viable for |n| steps) state at decision step |t| is a list
of policies of length |n|, one for each decision step:

> data PolicySeq : (t : Nat) -> (n : Nat) -> Type where
>   Nil   :  {t : Nat} ->
>            PolicySeq t Z
>   (::)  :  {t, n : Nat} ->
>            Policy t (S n) -> PolicySeq (S t) n -> PolicySeq t (S n)

Fold for |PolicySeq|:

> foldPolicySeq : {X : (t : Nat) -> (n : Nat) -> Type} ->
>                 ((t : Nat) -> X t Z) ->
>                 ((t : Nat) -> (n : Nat) -> Policy t (S n) -> X (S t) n -> X t (S n)) ->
>                 (t : Nat) -> (n : Nat) -> PolicySeq t n -> X t n
> foldPolicySeq e f t Z Nil = e t
> foldPolicySeq e f t (S n) (p :: ps) = f t n p (foldPolicySeq e f (S t) n ps)

* The value of policy sequences

As mentioned before, the idea of a decision problem is that the
decision maker seeks controls that maximize the sum of the rewards
obtained in a decision process.

Thus, in order to meaningfully define a notion of optimality for policy
sequences, we have to compute the value (in terms of possible sums of
rewards) of making decisions according to a given policy sequence.

Specifically, for a policy sequence |ps : PolicySeq tn| and a reachable,
viable for |n| steps state |x : State t|, we have to compute the value
(in terms of possible sums of rewards) of making |n| decision steps with
|ps| starting from |x|:

<   val : {t : Nat} -> {n : Nat} ->
<         (x : State t) -> Reachable x -> Viable n x -> PolicySeq t n -> Val

The case |n = Z| (and |ps = Nil|) is trivial. Here, we are not making
any decision step. Thus, we do not collect any reward and the value is
just zero:

<   val {t} {n = Z} x r v ps = zero

If |n = S m| and |ps| consists of a policy |p : Policy t (S m)| and of a
policy sequence |ps : PolicySeq (S t) m|, things are more complicated:

<   val {t} {n = S m} x r v (p :: ps) = ?

Here, we first have to compute the rewards obtained by selecting the
control |y = ctrl (p x r v)| in the first decision step. We get one
possible reward for each state in |nexts t x y|. Thus, if |x' `Elem`
(nexts t x y)|, its corresponding reward is

< reward t x y x'

Next, we have to add to all these rewards (one for every |x'|) the
values of making |m| further decision steps with |ps| starting from
|x'|:

< val x' r' v' ps

To do so, we have to provide reachability and viability evidences |r'|
and |v'| for |x'|. Finally, we have to reduce all possible values to a
single aggregated value. Here is where the measure |meas| comes into
place.

It is useful to introduce the notion of those possible states that can
be obtained by selecting the control |y : Ctrl t x| in |x : State t|:

> PossibleNextState  :  {t : Nat} ->
>                       (x  : State t) -> (y : Ctrl t x) -> Type
> PossibleNextState {t} x y = Sigma (State (S t)) (\ x' => x' `Elem` (nexts t x y))

With this notion in place and assuming

<   val : {t : Nat} -> {n : Nat} ->
<         (x : State t) -> Reachable x -> Viable n x -> PolicySeq t n -> Val

to be available, we can implement

> mutual

>   sval  :  {t, m : Nat} ->
>            (x  : State t) -> (r  : Reachable x) -> (v  : Viable (S m) x) ->
>            (gy  : GoodCtrl t x m) -> (ps : PolicySeq (S t) m) ->
>            PossibleNextState x (ctrl gy) -> Val
> {-
>   sval {t} {m} x r v gy ps (MkSigma x' x'emx') = reward t x y x' `plus` val x' r' v' ps where
>     y   : Ctrl t x
>     y   = ctrl gy
>     mx' : M (State (S t))
>     mx' = nexts t x y
>     ar' : All Reachable mx'
>     ar' = reachableSpec1 x r y
>     av' : All (Viable m) mx'
>     av' = allViable gy
>     r'  : Reachable x'
>     r'  = allElemSpec0 x' mx' ar' x'emx'
>     v'  : Viable m x'
>     v'  = allElemSpec0 x' mx' av' x'emx'
> -}
>   sval {t} {m} x r v gy ps (MkSigma x' x'emx') =
>     let y   : Ctrl t x
>             = ctrl gy in
>     let mx' : M (State (S t))
>             = nexts t x y in
>     let ar' : All Reachable mx'
>             = reachableSpec1 x r y in
>     let av' : All (Viable m) mx'
>             = allViable gy in
>     let r'  : Reachable x'
>             = allElemSpec0 x' mx' ar' x'emx' in
>     let v'  : Viable m x'
>             = allElemSpec0 x' mx' av' x'emx' in
>     reward t x y x' `plus` val x' r' v' ps

And finally

>   val  :  {t, n : Nat} ->
>           (x : State t) -> (r : Reachable x) -> (v : Viable n x) -> PolicySeq t n -> Val
>   val {t} {n = Z} x r v ps = zero
>   val {t} {n = S m} x r v (p :: ps) = meas (fmap (sval x r v gy ps) (tagElem mx')) where
>     gy   :  GoodCtrl t x m
>     gy   =  p x r v
>     y    :  Ctrl t x
>     y    =  ctrl gy
>     mx'  :  M (State (S t))
>     mx'  =  nexts t x y

* Optimality of policy sequences

With a function for computing the value (in terms of "possible" sums
of rewards) of making |n| decision steps with a policy sequence
starting from some specific state, we can formalise what it means for
one such sequence to be optimal.

Informally, we say that a policy sequence |ps| for making |n| decision
steps starting from states in |State t| which are reachable and viable
for |n| steps is optimal if its value is at least as good as the value
of any other policy sequence for making |n| decision steps starting
from states in |State t|. Formally:

> |||
> OptPolicySeq  :  {t, n : Nat} ->
>                  PolicySeq t n -> Type
>
> {-
> OptPolicySeq {t} {n} ps  =  (ps' : PolicySeq t n) ->
>                             (x : State t) -> (r : Reachable x) -> (v : Viable n x) ->
>                             val x r v ps' `LTE` val x r v ps
> -}
> OptPolicySeq {t} {n} ps  =  (x : State t) -> (r : Reachable x) -> (v : Viable n x) ->
>                             (ps' : PolicySeq t n) ->
>                             val x r v ps' `LTE` val x r v ps

Notice that the above notion of optimality is very strong. It entails a
quantification over all (viable and reachable) states of |Stete t| to
which the first policy of the sequence can be applied.

Thus, if we manage to compute an optimal policy sequence of length |n|
for making |n| decisions starting from step |t|, we have the guarantee
that, no matter which state we will happen to be at decision step |t|,
there is no better way to make |n| decision steps than that encoded by
our policy.

In other words, we have |n| rules for making ``best'' (in terms of
``possible'' sums of rewards) decisions.

Thus, an obvious question is whether it is at all possible to compute
sequences of policies that are optimal in the above sense. As we shall
see in |FullTheory|, if the assumptions put forward here and in
|ExtraAssumptions| are fulfilled, the answer to this question is
positive.

In the rest of this file, we implement a generic backwards induction
algorithm for computing optimal policy sequences for an arbitrary number
of decision steps.

* Optimal extensions of policy sequences

The computation at the core of backwards induction is the computation
of an optimal extension of a policy sequence. An extension of a policy
sequence for making |m| decision steps starting from states at
decision step |S t| is just a policy for taking decisions at step |t|,
that is, a policy that is put *in front* of the list of policies that
will deal with any resulting future states.

Informally, a policy |p| is an optimal extension of a policy sequence
|ps| if there is no better way than |p :: ps| to make |S m| decision
steps at step |t|. Formally:

> |||
> OptExt  :  {t, m : Nat} ->
>            PolicySeq (S t) m -> Policy t (S m) -> Type
> {-
> OptExt {t} {m} ps p  =  (p' : Policy t (S m)) ->
>                         (x : State t) -> (r : Reachable x) -> (v : Viable (S m) x) ->
>                         val x r v (p' :: ps) `LTE` val x r v (p :: ps)
> -}
> OptExt {t} {m} ps p  =  (x : State t) -> (r : Reachable x) -> (v : Viable (S m) x) ->
>                         (p' : Policy t (S m)) ->
>                         val x r v (p' :: ps) `LTE` val x r v (p :: ps)

The idea behind the notion of optimal extension is that if |p| is an
optimal extension of |ps| and |ps| is optimal, then |p :: ps| is
optimal.  This is Bellman's principle of optimality [1] which we will
implement in |FullTheory|.

The strong requirement of optimality implies that |p| is optimal for
every state, therefore, the control obtained by applying |p| to a given
state |x| must be optimal, i.e., it must maximise the function |cval x r
v ps|:

> |||
> cval  :  {t, n : Nat} ->
>          (x : State t) -> (r : Reachable x) -> (v : Viable (S n) x) ->
>          (ps : PolicySeq (S t) n) -> GoodCtrl t x n -> Val
> cval {t} x r v ps gy = meas (fmap (sval x r v gy ps) (tagElem mx')) where
>   y    :  Ctrl t x
>   y    =  ctrl gy
>   mx'  :  M (State (S t))
>   mx'  =  nexts t x y

Let |cvalargmax| be a function that delivers the control that leads to
the maximal value of |cval x r v ps|:

> cvalargmax  :  {t, n : Nat} ->
>                (x  : State t) -> (r : Reachable x) -> (v : Viable (S n) x) ->
>                (ps : PolicySeq (S t) n) -> GoodCtrl t x n

The controls obtained by maximising |cval x r v ps| for each of the
states |x : State t| will deliver a policy which is an optimal extension
of |ps|.  Thus, the problem of maximising |val| has been reduced to the
maximisation of |cval| for the states at time |t|.  Therefore, the
function that computes this optimal extension is:

> |||
> optExt  :  {t, n : Nat} ->
>            PolicySeq (S t) n -> Policy t (S n)
> optExt {t} {n} ps = p where
>   p : Policy t (S n)
>   p x r v = cvalargmax x r v ps

* Generic machine checkable backwards induction

If |LTE| is reflexive, it is straightforward to show that empty policy
sequences (that is, sequences for performing zero decision steps) are
optimal. Therefore, we have a starting point for the recursive process
of extending optimal policy sequences. This suggests the following
implementations of backwards induction:

> backwardsInduction : (t : Nat) -> (n : Nat) -> PolicySeq t n
> backwardsInduction t  Z     =  Nil
> {-
> backwardsInduction t (S n)  =  optExt ps :: ps where
>   ps : PolicySeq (S t) n
>   ps = backwardsInduction (S t) n
> -}
> backwardsInduction t (S n)  =  let ps = backwardsInduction (S t) n in
>                                optExt ps :: ps

> {-

> take : {t : Nat} -> (n : Nat) -> (m : Nat) -> PolicySeq t n -> Sigma Nat (\ m' => PolicySeq t m')
> take {t}    Z   m          ps  = MkSigma Z Nil
> take {t} (S n)  Z          ps  = MkSigma Z Nil
> take {t} (S n) (S m) (p :: ps) = MkSigma (S m') (p' :: ps') where
>   mps' : Sigma Nat (\ m' => PolicySeq (S t) m')
>   mps' = take n m ps
>   m'   : Nat
>   m'   = outl mps'
>   ps'  : PolicySeq (S t) m'
>   ps'  = outr mps'
>   p'   : Policy t (S m')
>   p'   = ?this_might_work -- p

> bi : (t : Nat) -> (n : Nat) -> (m : Nat) -> PolicySeq t n
> bi t  Z    m  =  Nil
> bi t (S n) m  =  p :: ps where
>   ps        : PolicySeq (S t) n
>   ps        = bi (S t) n m
>   m'        : Nat
>   m'        = outl (take n m ps)
>   ps'       : PolicySeq (S t) m'
>   ps'       = outr (take n m ps)
>   p         : Policy t (S n)
>   p         = ?this_will_not_work -- optExt ps'

> -}

This file contains all the *computational* elements that the user must
specify in order to be able to run |backwardsInduction|.  The results
are going to fulfill the condition of optimality only if several
assumptions hold, some of which we have introduced only informally (and
others not at all).  For example, we have not formalised the requirement
that |cvalargmax| delivers an optimal control, or that |LTE| is
reflexive (and we haven't even mentioned its transitivity, which is also
required).

These additional assumptions are formulated in the file |FullTheory|,
where we also implement a machine-checked proof of the correctness of
|backwardsInduction| under these assumptions.

This separation has been introduced in order to enable users that do not
want to deal with formal proofs to use the framework for computing
optimal policies.  Of course, the optimality of the results will, in
this case, not be machine-checked.

> {-

> ---}

[1] Bellman, Richard; "Dynamic Programming", Princeton University Press,
    1957

[2] Ionescu, Cezar; "Vulnerability Modelling and Monadic Dynamical
    Systems", Freie Universitaet Berlin, 2009


text:
||| Defines functions to use in place of `RegExp`'s data constructors, in order to create
||| regular expressions which are "normalized" to a canonical form as much as possible. This adds
||| some compile-time complexity but results in smaller DFAs for testing language membership.
module RegExp.Equivalences

import Data.List
import Decidable.Equality

import public RegExp.Types

%default total

||| Constructs a "normalized" `Cat`, which applies the following rules:
|||   - ∅ · r ≈ ∅
|||   - r · ∅ ≈ ∅
|||   - ε · r ≈ r
|||   - r · ε ≈ r
|||   - (r · s) · t ≈ r · (s · t)
export
normCat : DecEq a => RegExp a -> RegExp a -> RegExp a
normCat Null      _     = Null
normCat _         Null  = Null
normCat Empty     r     = r
normCat r         Empty = r
normCat (Cat r s) t     = Cat r (Cat s t)
normCat r         s     = Cat r s

||| Constructs a "normalized" `Disj`, which applies the following rules:
|||
|||   - ∅ + r ≈ r
|||   - r + r ≈ r
|||   - (r + s) + t ≈ r + (s + t)
|||
||| Note that the remaining equivalence (symmetry) is not captured:
|||
|||   - r + s ≈ s + r
export
normDisj : DecEq a => RegExp a -> RegExp a -> RegExp a
normDisj Null r    = r
normDisj r    Null = r
normDisj r s with (decEq r s)
  normDisj r          r | (Yes Refl) = r
  normDisj (Disj r s) t | (No _)     = Disj r (Disj s t)
  normDisj r          s | (No _)     = Disj r s

||| Constructs a "normalized" `Conj`, which applies the following rules:
|||   - ∅ & r ≈ ∅
|||   - r & r ≈ r
|||   - (r & s) & t ≈ r & (s & t)
|||
||| Note that the remaining equivalence (symmetry) is not captured:
|||
|||   - r & s ≈ s & r
export
normConj : DecEq a => RegExp a -> RegExp a -> RegExp a
normConj Null _    = Null
normConj _    Null = Null
normConj r s with (decEq r s)
  normConj r r          | (Yes Refl) = r
  normConj (Conj r s) t | (No _)     = Conj r (Conj s t)
  normConj r s          | (No _)     = Conj r s

||| Proof (by exhaustion) that `normCat` is sound.
export
normCat_isSound : DecEq a =>
                  {xs : List a} ->
                  {r : RegExp a} ->
                  {s : RegExp a} ->
                  Matches (normCat r s) xs ->
                  Matches (Cat r s) xs
normCat_isSound      {r=Null}       {s}            p = absurd p
normCat_isSound      {r=Empty}      {s=Null}       p = absurd p
normCat_isSound      {r=Empty}      {s=Empty}      p = InCat Refl InEmpty p
normCat_isSound      {r=Empty}      {s=(Lit _)}    p = InCat Refl InEmpty p
normCat_isSound      {r=Empty}      {s=(Cat _ _)}  p = InCat Refl InEmpty p
normCat_isSound      {r=Empty}      {s=(Disj _ _)} p = InCat Refl InEmpty p
normCat_isSound      {r=Empty}      {s=(Conj _ _)} p = InCat Refl InEmpty p
normCat_isSound      {r=Empty}      {s=(Star _)}   p = InCat Refl InEmpty p
normCat_isSound      {r=(Lit _)}    {s=Null}       p = absurd p
normCat_isSound {xs} {r=(Lit _)}    {s=Empty}      p = InCat (sym $ appendNilRightNeutral xs) p InEmpty
normCat_isSound      {r=(Lit _)}    {s=(Lit _)}    p = p
normCat_isSound      {r=(Lit _)}    {s=(Cat _ _)}  p = p
normCat_isSound      {r=(Lit _)}    {s=(Disj _ _)} p = p
normCat_isSound      {r=(Lit _)}    {s=(Conj _ _)} p = p
normCat_isSound      {r=(Lit _)}    {s=(Star _)}   p = p
normCat_isSound      {r=(Cat _ _)}  {s=Null}       p = absurd p
normCat_isSound {xs} {r=(Cat _ _)}  {s=Empty}      p = InCat (sym $ appendNilRightNeutral xs) p InEmpty
normCat_isSound {xs=xs++(ys++zs)} {r=(Cat _ _)} {s=(Lit _)} (InCat {xs} {ys=ys++zs} Refl pr (InCat {xs=ys} {ys=zs} Refl ps pl)) =
  InCat (appendAssociative xs ys zs) (InCat Refl pr ps) pl
normCat_isSound {xs=xs++(ys++zs)} {r=(Cat _ _)} {s=(Cat _ _)} (InCat {xs} {ys=ys++zs} Refl pr (InCat {xs=ys} {ys=zs} Refl ps pl)) =
  InCat (appendAssociative xs ys zs) (InCat Refl pr ps) pl
normCat_isSound {xs=xs++(ys++zs)} {r=(Cat _ _)} {s=(Disj _ _)} (InCat {xs} {ys=ys++zs} Refl pr (InCat {xs=ys} {ys=zs} Refl ps pl)) =
  InCat (appendAssociative xs ys zs) (InCat Refl pr ps) pl
normCat_isSound {xs=xs++(ys++zs)} {r=(Cat _ _)} {s=(Conj _ _)} (InCat {xs} {ys=ys++zs} Refl pr (InCat {xs=ys} {ys=zs} Refl ps pl)) =
  InCat (appendAssociative xs ys zs) (InCat Refl pr ps) pl
normCat_isSound {xs=xs++(ys++zs)} {r=(Cat _ _)} {s=(Star _)} (InCat {xs} {ys=ys++zs} Refl pr (InCat {xs=ys} {ys=zs} Refl ps pl)) =
  InCat (appendAssociative xs ys zs) (InCat Refl pr ps) pl
normCat_isSound      {r=(Disj _ _)} {s=Null}       p = absurd p
normCat_isSound {xs} {r=(Disj _ _)} {s=Empty}      p = InCat (sym $ appendNilRightNeutral xs) p InEmpty
normCat_isSound      {r=(Disj _ _)} {s=(Lit z)}    p = p
normCat_isSound      {r=(Disj _ _)} {s=(Cat z w)}  p = p
normCat_isSound      {r=(Disj _ _)} {s=(Disj z w)} p = p
normCat_isSound      {r=(Disj _ _)} {s=(Conj z w)} p = p
normCat_isSound      {r=(Disj _ _)} {s=(Star z)}   p = p
normCat_isSound      {r=(Conj _ _)} {s=Null}       p = absurd p
normCat_isSound {xs} {r=(Conj _ _)} {s=Empty}      p = InCat (sym $ appendNilRightNeutral xs) p InEmpty
normCat_isSound      {r=(Conj _ _)} {s=(Lit z)}    p = p
normCat_isSound      {r=(Conj _ _)} {s=(Cat z w)}  p = p
normCat_isSound      {r=(Conj _ _)} {s=(Disj z w)} p = p
normCat_isSound      {r=(Conj _ _)} {s=(Conj z w)} p = p
normCat_isSound      {r=(Conj _ _)} {s=(Star z)}   p = p
normCat_isSound      {r=(Star _)}   {s=Null}       p = absurd p
normCat_isSound {xs} {r=(Star _)}   {s=Empty}      p = InCat (sym $ appendNilRightNeutral xs) p InEmpty
normCat_isSound      {r=(Star _)}   {s=(Lit y)}    p = p
normCat_isSound      {r=(Star _)}   {s=(Cat y z)}  p = p
normCat_isSound      {r=(Star _)}   {s=(Disj y z)} p = p
normCat_isSound      {r=(Star _)}   {s=(Conj y z)} p = p
normCat_isSound      {r=(Star _)}   {s=(Star y)}   p = p

||| Proof (by exhaustion) that `normCat` is complete.
export
normCat_isComplete : DecEq a =>
                     {xs : List a} ->
                     {r : RegExp a} ->
                     {s : RegExp a} ->
                     Matches (Cat r s) xs ->
                     Matches (normCat r s) xs
normCat_isComplete {r=Null}                      (InCat _ pr _) = absurd pr
normCat_isComplete                {s=Null}       (InCat _ _ ps) = absurd ps
normCat_isComplete {r=Empty}      {s=Empty}      (InCat pCat InEmpty ps) = rewrite pCat in ps
normCat_isComplete {r=Empty}      {s=(Lit _)}    (InCat pCat InEmpty ps) = rewrite pCat in ps
normCat_isComplete {r=Empty}      {s=(Cat _ _)}  (InCat pCat InEmpty ps) = rewrite pCat in ps
normCat_isComplete {r=Empty}      {s=(Disj _ _)} (InCat pCat InEmpty ps) = rewrite pCat in ps
normCat_isComplete {r=Empty}      {s=(Conj _ _)} (InCat pCat InEmpty ps) = rewrite pCat in ps
normCat_isComplete {r=Empty}      {s=(Star _)}   (InCat pCat InEmpty ps) = rewrite pCat in ps
normCat_isComplete {r=(Lit _)}    {s=Empty}      (InCat {xs} Refl pr InEmpty) = rewrite (appendNilRightNeutral xs) in pr
normCat_isComplete {r=(Lit _)}    {s=(Lit _)}    p = p
normCat_isComplete {r=(Lit _)}    {s=(Cat _ _)}  p = p
normCat_isComplete {r=(Lit _)}    {s=(Disj _ _)} p = p
normCat_isComplete {r=(Lit _)}    {s=(Conj _ _)} p = p
normCat_isComplete {r=(Lit _)}    {s=(Star _)}   p = p
normCat_isComplete {r=(Cat _ _)}  {s=Empty} (InCat {xs} Refl pr InEmpty) = rewrite (appendNilRightNeutral xs) in pr
normCat_isComplete {xs=(xs'++ys)++[x]} {r=(Cat _ _)} {s=(Lit x)} (InCat {xs=xs'++ys} {ys=[x]} Refl (InCat {xs=xs'} {ys} Refl pr ps) InLit) =
  InCat (sym $ appendAssociative xs' ys [x]) pr (InCat Refl ps InLit)
normCat_isComplete {xs=(xs'++ys)++zs} {r=(Cat _ _)} {s=(Cat _ _)} (InCat {xs=xs'++ys} {ys=zs} Refl (InCat {xs=xs'} {ys} Refl pr ps) pt) =
  InCat (sym $ appendAssociative xs' ys zs) pr (InCat Refl ps pt)
normCat_isComplete {xs=(xs'++ys)++zs} {r=(Cat _ _)} {s=(Disj _ _)} (InCat {xs=xs'++ys} {ys=zs} Refl (InCat {xs=xs'} {ys} Refl pr ps) pt) =
  InCat (sym $ appendAssociative xs' ys zs) pr (InCat Refl ps pt)
normCat_isComplete {xs=(xs'++ys)++zs} {r=(Cat _ _)} {s=(Conj _ _)} (InCat {xs=xs'++ys} {ys=zs} Refl (InCat {xs=xs'} {ys} Refl pr ps) pt) =
  InCat (sym $ appendAssociative xs' ys zs) pr (InCat Refl ps pt)
normCat_isComplete {xs=(xs'++ys)++zs} {r=(Cat _ _)} {s=(Star _)} (InCat {xs=xs'++ys} {ys=zs} Refl (InCat {xs=xs'} {ys} Refl pr ps) pt) =
  InCat (sym $ appendAssociative xs' ys zs) pr (InCat Refl ps pt)
normCat_isComplete {r=(Disj _ _)} {s=Empty}      (InCat {xs} Refl pr InEmpty) = rewrite (appendNilRightNeutral xs) in pr
normCat_isComplete {r=(Disj _ _)} {s=(Lit _)}    p = p
normCat_isComplete {r=(Disj _ _)} {s=(Cat _ _)}  p = p
normCat_isComplete {r=(Disj _ _)} {s=(Disj _ _)} p = p
normCat_isComplete {r=(Disj _ _)} {s=(Conj _ _)} p = p
normCat_isComplete {r=(Disj _ _)} {s=(Star _)}   p = p
normCat_isComplete {r=(Conj _ _)} {s=Empty}      (InCat {xs} Refl pr InEmpty) = rewrite (appendNilRightNeutral xs) in pr
normCat_isComplete {r=(Conj _ _)} {s=(Lit _)}    p = p
normCat_isComplete {r=(Conj _ _)} {s=(Cat _ _)}  p = p
normCat_isComplete {r=(Conj _ _)} {s=(Disj _ _)} p = p
normCat_isComplete {r=(Conj _ _)} {s=(Conj _ _)} p = p
normCat_isComplete {r=(Conj _ _)} {s=(Star _)}   p = p
normCat_isComplete {r=(Star _)}   {s=Empty}      (InCat {xs} Refl pr InEmpty) = rewrite (appendNilRightNeutral xs) in pr
normCat_isComplete {r=(Star _)}   {s=(Lit _)}    p = p
normCat_isComplete {r=(Star _)}   {s=(Cat _ _)}  p = p
normCat_isComplete {r=(Star _)}   {s=(Disj _ _)} p = p
normCat_isComplete {r=(Star _)}   {s=(Conj _ _)} p = p
normCat_isComplete {r=(Star _)}   {s=(Star _)}   p = p

||| Proof (by exhaustion) that `normDisj` is sound.
export
normDisj_isSound : DecEq a =>
                   {xs : List a} ->
                   {r : RegExp a} ->
                   {s : RegExp a} ->
                   Matches (normDisj r s) xs ->
                   Matches (Disj r s) xs
normDisj_isSound {r=Null}                      p                     = InDisjR p
normDisj_isSound {r=Empty}      {s=Null}       p                     = InDisjL p
normDisj_isSound {r=Empty}      {s=Empty}      p                     = p
normDisj_isSound {r=Empty}      {s=(Lit _)}    p                     = p
normDisj_isSound {r=Empty}      {s=(Cat _ _)}  p                     = p
normDisj_isSound {r=Empty}      {s=(Disj _ _)} p                     = p
normDisj_isSound {r=Empty}      {s=(Conj _ _)} p                     = p
normDisj_isSound {r=Empty}      {s=(Star _)}   p                     = p
normDisj_isSound {r=(Lit _)}    {s=Null}       p                     = InDisjL p
normDisj_isSound {r=(Lit _)}    {s=Empty}      p                     = p
normDisj_isSound {r=(Lit x)}    {s=(Lit y)}    p with (decEq x y)
  normDisj_isSound {r=(Lit x)}  {s=(Lit x)}    p | (Yes Refl)        = InDisjL p
  normDisj_isSound {r=(Lit x)}  {s=(Lit y)}    p | (No _)       = p
normDisj_isSound {r=(Lit _)}    {s=(Cat _ _)}  p                     = p
normDisj_isSound {r=(Lit _)}    {s=(Disj _ _)} p                     = p
normDisj_isSound {r=(Lit _)}    {s=(Conj _ _)} p                     = p
normDisj_isSound {r=(Lit _)}    {s=(Star _)}   p                     = p
normDisj_isSound {r=(Cat _ _)}  {s=Null}       p                     = InDisjL p
normDisj_isSound {r=(Cat _ _)}  {s=Empty}      p                     = p
normDisj_isSound {r=(Cat _ _)}  {s=(Lit _)}    p                     = p
normDisj_isSound {r=(Cat r s)}  {s=(Cat t u)}  p with (decEq r t)
  normDisj_isSound {r=(Cat r s)} {s=(Cat r u)} p | (Yes Refl) with (decEq s u)
    normDisj_isSound {r=(Cat r s)} {s=(Cat r s)} p | (Yes Refl) | (Yes Refl) = InDisjL p
    normDisj_isSound {r=(Cat r s)} {s=(Cat r u)} p | (Yes Refl) | (No _) = p
  normDisj_isSound {r=(Cat r s)} {s=(Cat t u)} p | (No _) = p
normDisj_isSound {r=(Cat _ _)}  {s=(Disj _ _)} p                     = p
normDisj_isSound {r=(Cat _ _)}  {s=(Conj _ _)} p                     = p
normDisj_isSound {r=(Cat _ _)}  {s=(Star _)}   p                     = p
normDisj_isSound {r=(Disj _ _)} {s=Null}       p                     = InDisjL p
normDisj_isSound {r=(Disj _ _)} {s=Empty}      (InDisjL p)           = InDisjL (InDisjL p)
normDisj_isSound {r=(Disj _ _)} {s=Empty}      (InDisjR (InDisjL p)) = InDisjL (InDisjR p)
normDisj_isSound {r=(Disj _ _)} {s=Empty}      (InDisjR (InDisjR p)) = InDisjR p
normDisj_isSound {r=(Disj _ _)} {s=(Lit _)}    (InDisjL p)           = InDisjL (InDisjL p)
normDisj_isSound {r=(Disj _ _)} {s=(Lit _)}    (InDisjR (InDisjL p)) = InDisjL (InDisjR p)
normDisj_isSound {r=(Disj _ _)} {s=(Lit _)}    (InDisjR (InDisjR p)) = InDisjR p
normDisj_isSound {r=(Disj _ _)} {s=(Cat _ _)}  (InDisjL p)           = InDisjL (InDisjL p)
normDisj_isSound {r=(Disj _ _)} {s=(Cat _ _)}  (InDisjR (InDisjL p)) = InDisjL (InDisjR p)
normDisj_isSound {r=(Disj _ _)} {s=(Cat _ _)}  (InDisjR (InDisjR p)) = InDisjR p
normDisj_isSound {r=(Disj r s)} {s=(Disj t u)} p with (decEq r t)
  normDisj_isSound {r=(Disj r s)} {s=(Disj r u)} p                     | (Yes Refl) with (decEq s u)
    normDisj_isSound {r=(Disj r s)} {s=(Disj r s)} p                     | (Yes Refl) | (Yes Refl) = InDisjL p
    normDisj_isSound {r=(Disj r s)} {s=(Disj r u)} (InDisjL p)           | (Yes Refl) | (No _)     = InDisjL (InDisjL p)
    normDisj_isSound {r=(Disj r s)} {s=(Disj r u)} (InDisjR (InDisjL p)) | (Yes Refl) | (No _)     = InDisjL (InDisjR p)
    normDisj_isSound {r=(Disj r s)} {s=(Disj r u)} (InDisjR (InDisjR p)) | (Yes Refl) | (No _)     = InDisjR p
  normDisj_isSound {r=(Disj r s)} {s=(Disj t u)} (InDisjL p)           | (No _) = InDisjL (InDisjL p)
  normDisj_isSound {r=(Disj r s)} {s=(Disj t u)} (InDisjR (InDisjL p)) | (No _) = InDisjL (InDisjR p)
  normDisj_isSound {r=(Disj r s)} {s=(Disj t u)} (InDisjR (InDisjR p)) | (No _) = InDisjR p
normDisj_isSound {r=(Disj _ _)} {s=(Conj _ _)} (InDisjL p)           = InDisjL (InDisjL p)
normDisj_isSound {r=(Disj _ _)} {s=(Conj _ _)} (InDisjR (InDisjL p)) = InDisjL (InDisjR p)
normDisj_isSound {r=(Disj _ _)} {s=(Conj _ _)} (InDisjR (InDisjR p)) = InDisjR p
normDisj_isSound {r=(Disj _ _)} {s=(Star _)}   (InDisjL p)           = InDisjL (InDisjL p)
normDisj_isSound {r=(Disj _ _)} {s=(Star _)}   (InDisjR (InDisjL p)) = InDisjL (InDisjR p)
normDisj_isSound {r=(Disj _ _)} {s=(Star _)}   (InDisjR (InDisjR p)) = InDisjR p
normDisj_isSound {r=(Conj _ _)} {s=Null}       p                     = InDisjL p
normDisj_isSound {r=(Conj _ _)} {s=Empty}      p                     = p
normDisj_isSound {r=(Conj _ _)} {s=(Lit _)}    p                     = p
normDisj_isSound {r=(Conj _ _)} {s=(Cat _ _)}  p                     = p
normDisj_isSound {r=(Conj _ _)} {s=(Disj _ _)} p                     = p
normDisj_isSound {r=(Conj r s)} {s=(Conj t u)} p with (decEq r t)
  normDisj_isSound {r=(Conj r s)} {s=(Conj r u)} p | (Yes Refl) with (decEq s u)
    normDisj_isSound {r=(Conj r s)} {s=(Conj r s)} p | (Yes Refl) | (Yes Refl) = InDisjL p
    normDisj_isSound {r=(Conj r s)} {s=(Conj r u)} p | (Yes Refl) | (No _) = p
  normDisj_isSound {r=(Conj r s)} {s=(Conj t u)} p | (No _) = p
normDisj_isSound {r=(Conj _ _)} {s=(Star _)}   p                     = p
normDisj_isSound {r=(Star _)}   {s=Null}       p                     = InDisjL p
normDisj_isSound {r=(Star _)}   {s=Empty}      p                     = p
normDisj_isSound {r=(Star _)}   {s=(Lit _)}    p                     = p
normDisj_isSound {r=(Star _)}   {s=(Cat _ _)}  p                     = p
normDisj_isSound {r=(Star _)}   {s=(Disj _ _)} p                     = p
normDisj_isSound {r=(Star _)}   {s=(Conj _ _)} p                     = p
normDisj_isSound {r=(Star r)}   {s=(Star s)}   p with (decEq r s)
  normDisj_isSound {r=(Star r)} {s=(Star r)}   p | (Yes Refl)        = InDisjL p
  normDisj_isSound {r=(Star r)} {s=(Star s)}   p | (No _)            = p

||| Proof (by exhaustion) that `normDisj` is complete.
export
normDisj_isComplete : DecEq a =>
                      {xs : List a} ->
                      {r : RegExp a} ->
                      {s : RegExp a} ->
                      Matches (Disj r s) xs ->
                      Matches (normDisj r s) xs
normDisj_isComplete {r=Null}                      (InDisjL p)           = absurd p
normDisj_isComplete {r=Null}                      (InDisjR p)           = p
normDisj_isComplete {r=Empty}      {s=Null}       (InDisjL p)           = p
normDisj_isComplete {r=Empty}      {s=Null}       (InDisjR p)           = absurd p
normDisj_isComplete {r=Empty}      {s=Empty}      (InDisjL p)           = InDisjL p
normDisj_isComplete {r=Empty}      {s=Empty}      (InDisjR p)           = InDisjR p
normDisj_isComplete {r=Empty}      {s=(Lit _)}    p                     = p
normDisj_isComplete {r=Empty}      {s=(Cat _ _)}  p                     = p
normDisj_isComplete {r=Empty}      {s=(Disj _ _)} p                     = p
normDisj_isComplete {r=Empty}      {s=(Conj _ _)} p                     = p
normDisj_isComplete {r=Empty}      {s=(Star _)}   p                     = p
normDisj_isComplete {r=(Lit _)}    {s=Null}       (InDisjL p)           = p
normDisj_isComplete {r=(Lit _)}    {s=Null}       (InDisjR p)           = absurd p
normDisj_isComplete {r=(Lit _)}    {s=Empty}      p                     = p
normDisj_isComplete {r=(Lit x)}    {s=(Lit y)}    p with (decEq x y)
  normDisj_isComplete {r=(Lit x)}  {s=(Lit x)}    (InDisjL p) | (Yes Refl) = p
  normDisj_isComplete {r=(Lit x)}  {s=(Lit x)}    (InDisjR p) | (Yes Refl) = p
  normDisj_isComplete {r=(Lit x)}  {s=(Lit y)}    p           | (No _)     = p
normDisj_isComplete {r=(Lit _)}    {s=(Cat _ _)} p                      = p
normDisj_isComplete {r=(Lit _)}    {s=(Disj _ _)} p                     = p
normDisj_isComplete {r=(Lit _)}    {s=(Conj _ _)} p                     = p
normDisj_isComplete {r=(Lit _)}    {s=(Star _)} p                       = p
normDisj_isComplete {r=(Cat _ _)}  {s=Null} (InDisjL p)                 = p
normDisj_isComplete {r=(Cat _ _)}  {s=Null} (InDisjR p)                 = absurd p
normDisj_isComplete {r=(Cat _ _)}  {s=Empty} p = p
normDisj_isComplete {r=(Cat _ _)}  {s=(Lit _)} p = p
normDisj_isComplete {r=(Cat r s)}  {s=(Cat t u)} p with (decEq r t)
  normDisj_isComplete {r=(Cat r s)} {s=(Cat r u)} p | (Yes Refl) with (decEq s u)
    normDisj_isComplete {r=(Cat r s)} {s=(Cat r s)} (InDisjL p) | (Yes Refl) | (Yes Refl) = p
    normDisj_isComplete {r=(Cat r s)} {s=(Cat r s)} (InDisjR p) | (Yes Refl) | (Yes Refl) = p
    normDisj_isComplete {r=(Cat r s)} {s=(Cat r u)} p           | (Yes Refl) | (No _)     = p
  normDisj_isComplete {r=(Cat r s)} {s=(Cat t u)} p             | (No _) = p
normDisj_isComplete {r=(Cat _ _)}  {s=(Disj _ _)} p                     = p
normDisj_isComplete {r=(Cat _ _)}  {s=(Conj _ _)} p                     = p
normDisj_isComplete {r=(Cat _ _)}  {s=(Star _)} p                       = p
normDisj_isComplete {r=(Disj _ _)} {s=Null}       (InDisjL p)           = p
normDisj_isComplete {r=(Disj _ _)} {s=Null}       (InDisjR p)           = absurd p
normDisj_isComplete {r=(Disj _ _)} {s=Empty}      (InDisjL (InDisjL p)) = InDisjL p
normDisj_isComplete {r=(Disj _ _)} {s=Empty}      (InDisjL (InDisjR p)) = InDisjR (InDisjL p)
normDisj_isComplete {r=(Disj _ _)} {s=Empty}      (InDisjR p)           = InDisjR (InDisjR p)
normDisj_isComplete {r=(Disj _ _)} {s=(Lit _)}    (InDisjL (InDisjL p)) = InDisjL p
normDisj_isComplete {r=(Disj _ _)} {s=(Lit _)}    (InDisjL (InDisjR p)) = InDisjR (InDisjL p)
normDisj_isComplete {r=(Disj _ _)} {s=(Lit _)}    (InDisjR p)           = InDisjR (InDisjR p)
normDisj_isComplete {r=(Disj _ _)} {s=(Cat _ _)}  (InDisjL (InDisjL p)) = InDisjL p
normDisj_isComplete {r=(Disj _ _)} {s=(Cat _ _)}  (InDisjL (InDisjR p)) = InDisjR (InDisjL p)
normDisj_isComplete {r=(Disj _ _)} {s=(Cat _ _)}  (InDisjR p)           = InDisjR (InDisjR p)
normDisj_isComplete {r=(Disj r s)} {s=(Disj t u)} p with (decEq r t)
  normDisj_isComplete {r=(Disj r s)} {s=(Disj r u)} p                       | (Yes Refl) with (decEq s u)
    normDisj_isComplete {r=(Disj r s)} {s=(Disj r s)} (InDisjL p)             | (Yes Refl) | (Yes Refl) = p
    normDisj_isComplete {r=(Disj r s)} {s=(Disj r s)} (InDisjR p)             | (Yes Refl) | (Yes Refl) = p
    normDisj_isComplete {r=(Disj r s)} {s=(Disj r u)} (InDisjL (InDisjL p)) | (Yes Refl) | (No _)       = InDisjL p
    normDisj_isComplete {r=(Disj r s)} {s=(Disj r u)} (InDisjL (InDisjR p)) | (Yes Refl) | (No _)       = InDisjR (InDisjL p)
    normDisj_isComplete {r=(Disj r s)} {s=(Disj r u)} (InDisjR p)             | (Yes Refl) | (No _)     = InDisjR (InDisjR p)
  normDisj_isComplete {r=(Disj r s)} {s=(Disj t u)} (InDisjL (InDisjL p))   | (No _)                    = InDisjL p
  normDisj_isComplete {r=(Disj r s)} {s=(Disj t u)} (InDisjL (InDisjR p))   | (No _)                    = InDisjR (InDisjL p)
  normDisj_isComplete {r=(Disj r s)} {s=(Disj t u)} (InDisjR p)               | (No _)                  = InDisjR (InDisjR p)
normDisj_isComplete {r=(Disj _ _)} {s=(Conj _ _)} (InDisjL (InDisjL p)) = InDisjL p
normDisj_isComplete {r=(Disj _ _)} {s=(Conj _ _)} (InDisjL (InDisjR p)) = InDisjR (InDisjL p)
normDisj_isComplete {r=(Disj _ _)} {s=(Conj _ _)} (InDisjR p)           = InDisjR (InDisjR p)
normDisj_isComplete {r=(Disj _ _)} {s=(Star _)}   (InDisjL (InDisjL p)) = InDisjL p
normDisj_isComplete {r=(Disj _ _)} {s=(Star _)}   (InDisjL (InDisjR p)) = InDisjR (InDisjL p)
normDisj_isComplete {r=(Disj _ _)} {s=(Star _)}   (InDisjR p)           = InDisjR (InDisjR p)
normDisj_isComplete {r=(Conj _ _)} {s=Null}       (InDisjL p)           = p
normDisj_isComplete {r=(Conj _ _)} {s=Null}       (InDisjR p)           = absurd p
normDisj_isComplete {r=(Conj _ _)} {s=Empty}      p                     = p
normDisj_isComplete {r=(Conj _ _)} {s=(Lit _)}    p                     = p
normDisj_isComplete {r=(Conj _ _)} {s=(Cat _ _)}  p                     = p
normDisj_isComplete {r=(Conj _ _)} {s=(Disj _ _)} p                     = p
normDisj_isComplete {r=(Conj r s)} {s=(Conj t u)} p with (decEq r t)
  normDisj_isComplete {r=(Conj r s)} {s=(Conj r u)} p | (Yes Refl) with (decEq s u)
    normDisj_isComplete {r=(Conj r s)} {s=(Conj r s)} (InDisjL p) | (Yes Refl) | (Yes Refl) = p
    normDisj_isComplete {r=(Conj r s)} {s=(Conj r s)} (InDisjR p) | (Yes Refl) | (Yes Refl) = p
    normDisj_isComplete {r=(Conj r s)} {s=(Conj r u)} p           | (Yes Refl) | (No _)     = p
  normDisj_isComplete {r=(Conj r s)} {s=(Conj t u)} p | (No _)                              = p
normDisj_isComplete {r=(Conj _ _)} {s=(Star _)}   p                     = p
normDisj_isComplete {r=(Star _)} {s=Null}         (InDisjL p)           = p
normDisj_isComplete {r=(Star _)} {s=Null}         (InDisjR p)           = absurd p
normDisj_isComplete {r=(Star _)} {s=Empty}        p                     = p
normDisj_isComplete {r=(Star _)} {s=(Lit _)}      p                     = p
normDisj_isComplete {r=(Star _)} {s=(Cat _ _)}    p                     = p
normDisj_isComplete {r=(Star _)} {s=(Disj _ _)}   p                     = p
normDisj_isComplete {r=(Star _)} {s=(Conj _ _)}   p                     = p
normDisj_isComplete {r=(Star r)} {s=(Star s)} p with (decEq r s)
  normDisj_isComplete {r=(Star r)} {s=(Star r)}   (InDisjL p) | (Yes Refl) = p
  normDisj_isComplete {r=(Star r)} {s=(Star r)}   (InDisjR p) | (Yes Refl) = p
  normDisj_isComplete {r=(Star r)} {s=(Star s)}   p           | (No _)     = p

||| Proof (by exhaustion) that `normConj` is sound.
export
normConj_isSound : DecEq a =>
                   {xs : List a} ->
                   {r : RegExp a} ->
                   {s : RegExp a} ->
                   Matches (normConj r s) xs ->
                   Matches (Conj r s) xs
normConj_isSound {r=Null}       {s}       p = absurd p
normConj_isSound {r=Empty}      {s=Null}       p = absurd p
normConj_isSound {r=Empty}      {s=Empty}      p = p
normConj_isSound {r=Empty}      {s=(Lit _)}    p = p
normConj_isSound {r=Empty}      {s=(Cat _ _)}  p = p
normConj_isSound {r=Empty}      {s=(Disj _ _)} p = p
normConj_isSound {r=Empty}      {s=(Conj _ _)} p = p
normConj_isSound {r=Empty}      {s=(Star _)}   p = p
normConj_isSound {r=(Lit _)}    {s=Null}       p = absurd p
normConj_isSound {r=(Lit _)}    {s=Empty}      p = p
normConj_isSound {r=(Lit x)}    {s=(Lit y)}    p with (decEq x y)
  normConj_isSound {r=(Lit x)}    {s=(Lit x)}    p | (Yes Refl) = InConj p p
  normConj_isSound {r=(Lit x)}    {s=(Lit y)}    p | (No _)     = p
normConj_isSound {r=(Lit _)}    {s=(Cat _ _)}  p = p
normConj_isSound {r=(Lit _)}    {s=(Disj _ _)} p = p
normConj_isSound {r=(Lit _)}    {s=(Conj _ _)} p = p
normConj_isSound {r=(Lit _)}    {s=(Star _)}   p = p
normConj_isSound {r=(Cat _ _)}  {s=Null}       p = absurd p
normConj_isSound {r=(Cat _ _)}  {s=Empty}      p = p
normConj_isSound {r=(Cat _ _)}  {s=(Lit _)}    p = p
normConj_isSound {r=(Cat r s)}  {s=(Cat t u)}  p with (decEq r t)
  normConj_isSound {r=(Cat r s)} {s=(Cat r u)} p | (Yes Refl) with (decEq s u)
    normConj_isSound {r=(Cat r s)} {s=(Cat r s)} p | (Yes Refl) | (Yes Refl) = InConj p p
    normConj_isSound {r=(Cat r s)} {s=(Cat r u)} p | (Yes Refl) | (No _) = p
  normConj_isSound {r=(Cat r s)} {s=(Cat t u)} p | (No _) = p
normConj_isSound {r=(Cat _ _)}  {s=(Disj _ _)} p = p
normConj_isSound {r=(Cat _ _)}  {s=(Conj _ _)} p = p
normConj_isSound {r=(Cat _ _)}  {s=(Star _)}   p = p
normConj_isSound {r=(Disj _ _)} {s=Null}       p = absurd p
normConj_isSound {r=(Disj _ _)} {s=Empty}      p = p
normConj_isSound {r=(Disj _ _)} {s=(Lit _)}    p = p
normConj_isSound {r=(Disj _ _)} {s=(Cat _ _)}  p = p
normConj_isSound {r=(Disj r s)} {s=(Disj t u)} p with (decEq r t)
  normConj_isSound {r=(Disj r s)} {s=(Disj r u)} p | (Yes Refl) with (decEq s u)
    normConj_isSound {r=(Disj r s)} {s=(Disj r s)} p | (Yes Refl) | (Yes Refl) = InConj p p
    normConj_isSound {r=(Disj r s)} {s=(Disj r u)} p | (Yes Refl) | (No _) = p
  normConj_isSound {r=(Disj r s)} {s=(Disj t u)} p | (No _) = p
normConj_isSound {r=(Disj _ _)} {s=(Conj _ _)} p = p
normConj_isSound {r=(Disj _ _)} {s=(Star _)}   p = p
normConj_isSound {r=(Conj _ _)} {s=Null}       p = absurd p
normConj_isSound {r=(Conj _ _)} {s=Empty}      (InConj pr (InConj ps pt)) = InConj (InConj pr ps) pt
normConj_isSound {r=(Conj _ _)} {s=(Lit _)}    (InConj pr (InConj ps pt)) = InConj (InConj pr ps) pt
normConj_isSound {r=(Conj _ _)} {s=(Cat _ _)}  (InConj pr (InConj ps pt)) = InConj (InConj pr ps) pt
normConj_isSound {r=(Conj _ _)} {s=(Disj _ _)} (InConj pr (InConj ps pt)) = InConj (InConj pr ps) pt
normConj_isSound {r=(Conj r s)} {s=(Conj t u)} p with (decEq r t)
  normConj_isSound {r=(Conj r s)} {s=(Conj r u)} p | (Yes Refl) with (decEq s u)
    normConj_isSound {r=(Conj r s)} {s=(Conj r s)} p | (Yes Refl) | (Yes Refl) = InConj p p
    normConj_isSound {r=(Conj r s)} {s=(Conj r u)} (InConj _ (InConj ps (InConj pt pu))) | (Yes Refl) | (No _) =
      InConj (InConj pt ps) (InConj pt pu)
  normConj_isSound {r=(Conj r s)} {s=(Conj t u)} (InConj pr (InConj ps (InConj pt pu))) | (No _) =
    InConj (InConj pr ps) (InConj pt pu)
normConj_isSound {r=(Conj _ _)} {s=(Star _)}   (InConj pr (InConj ps pt)) = InConj (InConj pr ps) pt
normConj_isSound {r=(Star _)}   {s=Null}       p = absurd p
normConj_isSound {r=(Star _)}   {s=Empty}      p = p
normConj_isSound {r=(Star _)}   {s=(Lit _)}    p = p
normConj_isSound {r=(Star _)}   {s=(Cat _ _)}  p = p
normConj_isSound {r=(Star _)}   {s=(Disj _ _)} p = p
normConj_isSound {r=(Star _)}   {s=(Conj _ _)} p = p
normConj_isSound {r=(Star r)}   {s=(Star s)}   p with (decEq r s)
  normConj_isSound {r=(Star r)}   {s=(Star r)}   p | (Yes Refl) = InConj p p
  normConj_isSound {r=(Star r)}   {s=(Star s)}   p | (No _)     = p

||| Proof (by exhaustion) that `normCat` is complete.
export
normConj_isComplete : DecEq a =>
                      {xs : List a} ->
                      {r : RegExp a} ->
                      {s : RegExp a} ->
                      Matches (Conj r s) xs ->
                      Matches (normConj r s) xs
normConj_isComplete {r=Null}                      (InConj p _) = absurd p
normConj_isComplete                {s=Null}       (InConj _ p) = absurd p
normConj_isComplete {r=Empty}      {s=Empty}      p = p
normConj_isComplete {r=Empty}      {s=(Lit _)}    p = p
normConj_isComplete {r=Empty}      {s=(Cat _ _)}  p = p
normConj_isComplete {r=Empty}      {s=(Disj _ _)} p = p
normConj_isComplete {r=Empty}      {s=(Conj _ _)} p = p
normConj_isComplete {r=Empty}      {s=(Star _)}   p = p
normConj_isComplete {r=(Lit _)}    {s=Empty}      p = p
normConj_isComplete {r=(Lit x)}    {s=(Lit y)}    p with (decEq x y)
  normConj_isComplete {r=(Lit x)}  {s=(Lit x)}    (InConj p _) | Yes Refl = p
  normConj_isComplete {r=(Lit x)}  {s=(Lit y)}    p            | No _     = p
normConj_isComplete {r=(Lit _)}    {s=(Cat _ _)}  p = p
normConj_isComplete {r=(Lit _)}    {s=(Disj _ _)} p = p
normConj_isComplete {r=(Lit _)}    {s=(Conj _ _)} p = p
normConj_isComplete {r=(Lit _)}    {s=(Star _)}   p = p
normConj_isComplete {r=(Cat _ _)}  {s=Empty}      p = p
normConj_isComplete {r=(Cat _ _)}  {s=(Lit _)}    p = p
normConj_isComplete {r=(Cat r s)}   {s=(Cat t u)} p with (decEq (Cat r s) (Cat t u))
  normConj_isComplete {r=(Cat r s)} {s=(Cat r s)} (InConj p _) | Yes Refl = p
  normConj_isComplete {r=(Cat r s)} {s=(Cat t u)} p            | No _     = p
normConj_isComplete {r=(Cat _ _)}  {s=(Disj _ _)} p = p
normConj_isComplete {r=(Cat _ _)}  {s=(Conj _ _)} p = p
normConj_isComplete {r=(Cat _ _)}  {s=(Star _)}   p = p
normConj_isComplete {r=(Disj _ _)} {s=Empty}      p = p
normConj_isComplete {r=(Disj _ _)} {s=(Lit _)}    p = p
normConj_isComplete {r=(Disj _ _)} {s=(Cat _ _)}  p = p
normConj_isComplete {r=(Disj r s)}   {s=(Disj t u)} p with (decEq (Disj r s) (Disj t u))
  normConj_isComplete {r=(Disj r s)} {s=(Disj r s)} (InConj p _) | Yes Refl = p
  normConj_isComplete {r=(Disj r s)} {s=(Disj t u)} p            | No _     = p
normConj_isComplete {r=(Disj _ _)} {s=(Conj _ _)} p = p
normConj_isComplete {r=(Disj _ _)} {s=(Star _)}   p = p
normConj_isComplete {r=(Conj _ _)} {s=Empty}      (InConj (InConj pr ps) pt) = InConj pr (InConj ps pt)
normConj_isComplete {r=(Conj _ _)} {s=(Lit _)}    (InConj (InConj pr ps) pt) = InConj pr (InConj ps pt)
normConj_isComplete {r=(Conj _ _)} {s=(Cat _ _)}  (InConj (InConj pr ps) pt) = InConj pr (InConj ps pt)
normConj_isComplete {r=(Conj _ _)} {s=(Disj _ _)} (InConj (InConj pr ps) pt) = InConj pr (InConj ps pt)
normConj_isComplete {r=(Conj r s)} {s=(Conj t u)} p with (decEq (Conj r s) (Conj t u))
  normConj_isComplete {r=(Conj r s)} {s=(Conj r s)} (InConj p _)                           | Yes Refl = p
  normConj_isComplete {r=(Conj r s)} {s=(Conj t u)} (InConj (InConj pr ps) (InConj pt pu)) | No _     =
    InConj pr (InConj ps (InConj pt pu))
normConj_isComplete {r=(Conj _ _)} {s=(Star _)}   (InConj (InConj pr ps) pt) = InConj pr (InConj ps pt)
normConj_isComplete {r=(Star _)}   {s=Empty}      p = p
normConj_isComplete {r=(Star _)}   {s=(Lit _)}    p = p
normConj_isComplete {r=(Star _)}   {s=(Cat _ _)}  p = p
normConj_isComplete {r=(Star _)}   {s=(Disj _ _)} p = p
normConj_isComplete {r=(Star _)}   {s=(Conj _ _)} p = p
normConj_isComplete {r=(Star r)}   {s=(Star s)}   p with (decEq r s)
  normConj_isComplete {r=(Star r)} {s=(Star r)}   (InConj p _) | Yes Refl = p
  normConj_isComplete {r=(Star r)} {s=(Star s)}   p            | No _     = p

ext: idr

max_stars_repo_name: polendri/idris-regex

max_issues_repo_name: polendri/idris-regex

max_forks_repo_name: polendri/idris-regexp


text:
data InfIO: Type where
  Do: IO a -> (a -> Inf InfIO) -> InfIO

(>>=) : IO a -> (a -> Inf InfIO) -> InfIO
(>>=) = Do

data Fuel = Dry | More (Lazy Fuel)

forever: Fuel
forever = More forever

tank: Nat -> Fuel
tank Z = Dry
tank (S k) = More (tank k)

printLoop: String -> InfIO
printLoop msg =
  do
    putStrLn msg
    printLoop msg

run: InfIO -> IO()
run (Do action cont) =
  do
    res <- action
    run (cont res)

runFuel: Fuel -> InfIO -> IO()
runFuel Dry         y                = putStrLn "Out of fuel"
runFuel (More fuel) (Do action cont) =
  do
    res <- action
    runFuel fuel (cont res)

max_stars_repo_name: coffius/idris-exercises

max_issues_repo_name: coffius/idris-exercises

max_forks_repo_name: coffius/idris-exercises


text:
module LinearTypes

import Data.Vect

infixr 10 ::
infix 5 #

%default total

public export
data LFstPair : Type -> Type -> Type where
  (#) : (1 _ : a) -> b -> LFstPair a b

public export
data LVect : Nat -> Type ->  Type where
  Nil : LVect Z a
  (::) : (1 _ : a) -> (1 _ : LVect k a) -> LVect (S k) a

public export
Show a => Show (LVect n a) where
  show v = "[" ++ show' v ++ "]" where
    show' :  LVect k a -> String
    show' Nil = ""
    show' [x] = show x
    show' (x :: xs) = show x ++ " , " ++ show' xs

public export
(Show a, Show b) => Show (LPair a b) where
  show ( a # b ) = "( " ++ show a ++ " # " ++ show b ++ " )"

public export
(Show a, Show b) => Show (LFstPair a b) where
  show ( a # b ) = "( " ++ show a ++ " # " ++ show b ++ " )"

public export
(++) : (1 xs : LVect m a) -> (1 ys : LVect n a) -> LVect (m + n) a
(++) []      ys = ys
(++) (x::xs) ys = x :: (xs ++ ys)

public export
splitAt : {n : Nat} -> (i : Nat) -> (1 xs : LVect (i+n) a) -> LPair (LVect i a) (LVect n a)
splitAt 0 xs            = [] # xs
splitAt (S k) (x :: xs) = let ys # zs = LinearTypes.splitAt k xs in
                              (x :: ys) # zs

||| diff n i = n - i
public export
diff : Nat -> Nat -> Nat
diff Z     n = Z
diff (S k) n = S (diff k n)

export
lemmaDiffZero : (n : Nat) -> diff n 0 = n
lemmaDiffZero 0 = Refl
lemmaDiffZero (S k) = rewrite lemmaDiffZero k in Refl

public export
consLin : (1 _ : Bool) -> (1 _ : Vect n Bool) -> Vect (S n) Bool
consLin False [] = [False]
consLin False (x :: xs) = False :: x :: xs
consLin True [] = [True]
consLin True (x :: xs) = True :: x :: xs

public export
toVect : (1 _ : LVect n Bool) -> Vect n Bool
toVect [] = []
toVect (x :: xs) = x `consLin` (toVect xs)

max_stars_repo_name: zamdzhiev/Qimaera

max_issues_repo_name: zamdzhiev/Qimaera

max_forks_repo_name: zamdzhiev/Qimaera


text:
foo : List Char -> ()
foo cs = case cs of
  "bar" => ()
  _ => ()


text:
{-
Copyright 2018, Mokshasoft AB (mokshasoft.com)

This software may be distributed and modified according to the terms of
the BSD 2-Clause license. Note that NO WARRANTY is provided.
See "LICENSE_BSD2.txt" for details.
-}

module Main

import seL4.seL4

main : IO ()
main = debugPrint "seL4 <3 Idris\n"


text:
module Prelude.EqOrd

import Builtin
import Prelude.Basics
import Prelude.Ops

%default total

------------------------
-- EQUALITY, ORDERING --
------------------------

||| The Eq interface defines inequality and equality.
public export
interface Eq ty where
  constructor MkEq
  (==) : ty -> ty -> Bool
  (/=) : ty -> ty -> Bool

  x == y = not (x /= y)
  x /= y = not (x == y)

public export
Eq Void where
  _ == _ impossible

public export
Eq () where
  _ == _ = True

public export
Eq Bool where
  True == True = True
  False == False = True
  _ == _ = False

public export
Eq Int where
  x == y = intToBool (prim__eq_Int x y)

public export
Eq Integer where
  x == y = intToBool (prim__eq_Integer x y)

public export
Eq Bits8 where
  x == y = intToBool (prim__eq_Bits8 x y)

public export
Eq Bits16 where
  x == y = intToBool (prim__eq_Bits16 x y)

public export
Eq Bits32 where
  x == y = intToBool (prim__eq_Bits32 x y)

public export
Eq Bits64 where
  x == y = intToBool (prim__eq_Bits64 x y)

public export
Eq Int8 where
  x == y = intToBool (prim__eq_Int8 x y)

public export
Eq Int16 where
  x == y = intToBool (prim__eq_Int16 x y)

public export
Eq Int32 where
  x == y = intToBool (prim__eq_Int32 x y)

public export
Eq Int64 where
  x == y = intToBool (prim__eq_Int64 x y)

public export
Eq Double where
  x == y = intToBool (prim__eq_Double x y)

public export
Eq Char where
  x == y = intToBool (prim__eq_Char x y)

public export
Eq String where
  x == y = intToBool (prim__eq_String x y)

public export
Eq a => Eq b => Eq (a, b) where
  (x1, y1) == (x2, y2) = x1 == x2 && y1 == y2

public export
data Ordering = LT | EQ | GT

public export
Eq Ordering where
  LT == LT = True
  EQ == EQ = True
  GT == GT = True
  _  == _  = False

||| The Ord interface defines comparison operations on ordered data types.
public export
interface Eq ty => Ord ty where
  constructor MkOrd
  compare : ty -> ty -> Ordering
  compare x y = if x < y then LT else if x == y then EQ else GT

  (<) : ty -> ty -> Bool
  (<) x y = compare x y == LT

  (>) : ty -> ty -> Bool
  (>) x y = compare x y == GT

  (<=) : ty -> ty -> Bool
  (<=) x y = compare x y /= GT

  (>=) : ty -> ty -> Bool
  (>=) x y = compare x y /= LT

  max : ty -> ty -> ty
  max x y = if x > y then x else y

  min : ty -> ty -> ty
  min x y = if (x < y) then x else y

export
comparing : Ord a => (b -> a) -> b -> b -> Ordering
comparing p x y = compare (p x) (p y)

public export
Ord Void where
  compare _ _ impossible

public export
Ord () where
  compare _ _ = EQ

public export
Ord Bool where
  compare False False = EQ
  compare False True = LT
  compare True False = GT
  compare True True = EQ

public export
Ord Int where
  (<) x y = intToBool (prim__lt_Int x y)
  (<=) x y = intToBool (prim__lte_Int x y)
  (>) x y = intToBool (prim__gt_Int x y)
  (>=) x y = intToBool (prim__gte_Int x y)

public export
Ord Integer where
  (<) x y = intToBool (prim__lt_Integer x y)
  (<=) x y = intToBool (prim__lte_Integer x y)
  (>) x y = intToBool (prim__gt_Integer x y)
  (>=) x y = intToBool (prim__gte_Integer x y)

-- Used for the nat hack
public export
compareInteger : (x, y : Integer) -> Ordering
compareInteger = compare

public export
Ord Bits8 where
  (<) x y = intToBool (prim__lt_Bits8 x y)
  (<=) x y = intToBool (prim__lte_Bits8 x y)
  (>) x y = intToBool (prim__gt_Bits8 x y)
  (>=) x y = intToBool (prim__gte_Bits8 x y)

public export
Ord Bits16 where
  (<) x y = intToBool (prim__lt_Bits16 x y)
  (<=) x y = intToBool (prim__lte_Bits16 x y)
  (>) x y = intToBool (prim__gt_Bits16 x y)
  (>=) x y = intToBool (prim__gte_Bits16 x y)

public export
Ord Bits32 where
  (<) x y = intToBool (prim__lt_Bits32 x y)
  (<=) x y = intToBool (prim__lte_Bits32 x y)
  (>) x y = intToBool (prim__gt_Bits32 x y)
  (>=) x y = intToBool (prim__gte_Bits32 x y)

public export
Ord Bits64 where
  (<) x y = intToBool (prim__lt_Bits64 x y)
  (<=) x y = intToBool (prim__lte_Bits64 x y)
  (>) x y = intToBool (prim__gt_Bits64 x y)
  (>=) x y = intToBool (prim__gte_Bits64 x y)

public export
Ord Int8 where
  (<) x y = intToBool (prim__lt_Int8 x y)
  (<=) x y = intToBool (prim__lte_Int8 x y)
  (>) x y = intToBool (prim__gt_Int8 x y)
  (>=) x y = intToBool (prim__gte_Int8 x y)

public export
Ord Int16 where
  (<) x y = intToBool (prim__lt_Int16 x y)
  (<=) x y = intToBool (prim__lte_Int16 x y)
  (>) x y = intToBool (prim__gt_Int16 x y)
  (>=) x y = intToBool (prim__gte_Int16 x y)

public export
Ord Int32 where
  (<) x y = intToBool (prim__lt_Int32 x y)
  (<=) x y = intToBool (prim__lte_Int32 x y)
  (>) x y = intToBool (prim__gt_Int32 x y)
  (>=) x y = intToBool (prim__gte_Int32 x y)

public export
Ord Int64 where
  (<) x y = intToBool (prim__lt_Int64 x y)
  (<=) x y = intToBool (prim__lte_Int64 x y)
  (>) x y = intToBool (prim__gt_Int64 x y)
  (>=) x y = intToBool (prim__gte_Int64 x y)

public export
Ord Double where
  (<) x y = intToBool (prim__lt_Double x y)
  (<=) x y = intToBool (prim__lte_Double x y)
  (>) x y = intToBool (prim__gt_Double x y)
  (>=) x y = intToBool (prim__gte_Double x y)

public export
Ord String where
  (<) x y = intToBool (prim__lt_String x y)
  (<=) x y = intToBool (prim__lte_String x y)
  (>) x y = intToBool (prim__gt_String x y)
  (>=) x y = intToBool (prim__gte_String x y)

public export
Ord Char where
  (<) x y = intToBool (prim__lt_Char x y)
  (<=) x y = intToBool (prim__lte_Char x y)
  (>) x y = intToBool (prim__gt_Char x y)
  (>=) x y = intToBool (prim__gte_Char x y)

public export
Ord a => Ord b => Ord (a, b) where
  compare (x1, y1) (x2, y2)
      = if x1 /= x2 then compare x1 x2
                    else compare y1 y2


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

max_stars_repo_name: janschultecom/idris-examples

max_issues_repo_name: janschultecom/idris-examples

max_forks_repo_name: janschultecom/idris-examples


text:
module Web.Internal.CssPrim

import JS
import Web.Internal.Types

--------------------------------------------------------------------------------
--          Interfaces
--------------------------------------------------------------------------------

namespace CSSGroupingRule

  export
  %foreign "browser:lambda:x=>x.cssRules"
  prim__cssRules : CSSGroupingRule -> PrimIO CSSRuleList

  export
  %foreign "browser:lambda:(x,a)=>x.deleteRule(a)"
  prim__deleteRule : CSSGroupingRule -> Bits32 -> PrimIO ()

  export
  %foreign "browser:lambda:(x,a,b)=>x.insertRule(a,b)"
  prim__insertRule :  CSSGroupingRule
                   -> String
                   -> UndefOr Bits32
                   -> PrimIO Bits32

namespace CSSImportRule

  export
  %foreign "browser:lambda:x=>x.href"
  prim__href : CSSImportRule -> PrimIO String

  export
  %foreign "browser:lambda:x=>x.media"
  prim__media : CSSImportRule -> PrimIO MediaList

  export
  %foreign "browser:lambda:x=>x.styleSheet"
  prim__styleSheet : CSSImportRule -> PrimIO CSSStyleSheet

namespace CSSMarginRule

  export
  %foreign "browser:lambda:x=>x.name"
  prim__name : CSSMarginRule -> PrimIO String

  export
  %foreign "browser:lambda:x=>x.style"
  prim__style : CSSMarginRule -> PrimIO CSSStyleDeclaration

namespace CSSNamespaceRule

  export
  %foreign "browser:lambda:x=>x.namespaceURI"
  prim__namespaceURI : CSSNamespaceRule -> PrimIO String

  export
  %foreign "browser:lambda:x=>x.prefix"
  prim__prefix : CSSNamespaceRule -> PrimIO String

namespace CSSPageRule

  export
  %foreign "browser:lambda:x=>x.selectorText"
  prim__selectorText : CSSPageRule -> PrimIO String

  export
  %foreign "browser:lambda:(x,v)=>{x.selectorText = v}"
  prim__setSelectorText : CSSPageRule -> String -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.style"
  prim__style : CSSPageRule -> PrimIO CSSStyleDeclaration

namespace CSSPseudoElement

  export
  %foreign "browser:lambda:x=>x.element"
  prim__element : CSSPseudoElement -> PrimIO Element

  export
  %foreign "browser:lambda:x=>x.type"
  prim__type : CSSPseudoElement -> PrimIO String

namespace CSSRule

  export
  %foreign "browser:lambda:x=>x.cssText"
  prim__cssText : CSSRule -> PrimIO String

  export
  %foreign "browser:lambda:(x,v)=>{x.cssText = v}"
  prim__setCssText : CSSRule -> String -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.parentRule"
  prim__parentRule : CSSRule -> PrimIO (Nullable CSSRule)

  export
  %foreign "browser:lambda:x=>x.parentStyleSheet"
  prim__parentStyleSheet : CSSRule -> PrimIO (Nullable CSSStyleSheet)

  export
  %foreign "browser:lambda:x=>x.type"
  prim__type : CSSRule -> PrimIO Bits16

namespace CSSRuleList

  export
  %foreign "browser:lambda:x=>x.length"
  prim__length : CSSRuleList -> PrimIO Bits32

  export
  %foreign "browser:lambda:(x,a)=>x.item(a)"
  prim__item : CSSRuleList -> Bits32 -> PrimIO (Nullable CSSRule)

namespace CSSStyleDeclaration

  export
  %foreign "browser:lambda:x=>x.cssFloat"
  prim__cssFloat : CSSStyleDeclaration -> PrimIO String

  export
  %foreign "browser:lambda:(x,v)=>{x.cssFloat = v}"
  prim__setCssFloat : CSSStyleDeclaration -> String -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.cssText"
  prim__cssText : CSSStyleDeclaration -> PrimIO String

  export
  %foreign "browser:lambda:(x,v)=>{x.cssText = v}"
  prim__setCssText : CSSStyleDeclaration -> String -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.length"
  prim__length : CSSStyleDeclaration -> PrimIO Bits32

  export
  %foreign "browser:lambda:x=>x.parentRule"
  prim__parentRule : CSSStyleDeclaration -> PrimIO (Nullable CSSRule)

  export
  %foreign "browser:lambda:(x,a)=>x.getPropertyPriority(a)"
  prim__getPropertyPriority : CSSStyleDeclaration -> String -> PrimIO String

  export
  %foreign "browser:lambda:(x,a)=>x.getPropertyValue(a)"
  prim__getPropertyValue : CSSStyleDeclaration -> String -> PrimIO String

  export
  %foreign "browser:lambda:(x,a)=>x.item(a)"
  prim__item : CSSStyleDeclaration -> Bits32 -> PrimIO String

  export
  %foreign "browser:lambda:(x,a)=>x.removeProperty(a)"
  prim__removeProperty : CSSStyleDeclaration -> String -> PrimIO String

  export
  %foreign "browser:lambda:(x,a,b,c)=>x.setProperty(a,b,c)"
  prim__setProperty :  CSSStyleDeclaration
                    -> String
                    -> String
                    -> UndefOr String
                    -> PrimIO ()

namespace CSSStyleRule

  export
  %foreign "browser:lambda:x=>x.selectorText"
  prim__selectorText : CSSStyleRule -> PrimIO String

  export
  %foreign "browser:lambda:(x,v)=>{x.selectorText = v}"
  prim__setSelectorText : CSSStyleRule -> String -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.style"
  prim__style : CSSStyleRule -> PrimIO CSSStyleDeclaration

namespace CSSStyleSheet

  export
  %foreign "browser:lambda:x=>x.cssRules"
  prim__cssRules : CSSStyleSheet -> PrimIO CSSRuleList

  export
  %foreign "browser:lambda:x=>x.ownerRule"
  prim__ownerRule : CSSStyleSheet -> PrimIO (Nullable CSSRule)

  export
  %foreign "browser:lambda:x=>x.rules"
  prim__rules : CSSStyleSheet -> PrimIO CSSRuleList

  export
  %foreign "browser:lambda:(x,a,b,c)=>x.addRule(a,b,c)"
  prim__addRule :  CSSStyleSheet
                -> UndefOr String
                -> UndefOr String
                -> UndefOr Bits32
                -> PrimIO Int32

  export
  %foreign "browser:lambda:(x,a)=>x.deleteRule(a)"
  prim__deleteRule : CSSStyleSheet -> Bits32 -> PrimIO ()

  export
  %foreign "browser:lambda:(x,a,b)=>x.insertRule(a,b)"
  prim__insertRule : CSSStyleSheet -> String -> UndefOr Bits32 -> PrimIO Bits32

  export
  %foreign "browser:lambda:(x,a)=>x.removeRule(a)"
  prim__removeRule : CSSStyleSheet -> UndefOr Bits32 -> PrimIO ()

namespace MediaList

  export
  %foreign "browser:lambda:x=>x.length"
  prim__length : MediaList -> PrimIO Bits32

  export
  %foreign "browser:lambda:x=>x.mediaText"
  prim__mediaText : MediaList -> PrimIO String

  export
  %foreign "browser:lambda:(x,v)=>{x.mediaText = v}"
  prim__setMediaText : MediaList -> String -> PrimIO ()

  export
  %foreign "browser:lambda:(x,a)=>x.appendMedium(a)"
  prim__appendMedium : MediaList -> String -> PrimIO ()

  export
  %foreign "browser:lambda:(x,a)=>x.deleteMedium(a)"
  prim__deleteMedium : MediaList -> String -> PrimIO ()

  export
  %foreign "browser:lambda:(x,a)=>x.item(a)"
  prim__item : MediaList -> Bits32 -> PrimIO (Nullable String)

namespace StyleSheet

  export
  %foreign "browser:lambda:x=>x.disabled"
  prim__disabled : StyleSheet -> PrimIO Boolean

  export
  %foreign "browser:lambda:(x,v)=>{x.disabled = v}"
  prim__setDisabled : StyleSheet -> Boolean -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.href"
  prim__href : StyleSheet -> PrimIO (Nullable String)

  export
  %foreign "browser:lambda:x=>x.media"
  prim__media : StyleSheet -> PrimIO MediaList

  export
  %foreign "browser:lambda:x=>x.ownerNode"
  prim__ownerNode :  StyleSheet
                  -> PrimIO (Nullable (Union2 Element ProcessingInstruction))

  export
  %foreign "browser:lambda:x=>x.parentStyleSheet"
  prim__parentStyleSheet : StyleSheet -> PrimIO (Nullable CSSStyleSheet)

  export
  %foreign "browser:lambda:x=>x.title"
  prim__title : StyleSheet -> PrimIO (Nullable String)

  export
  %foreign "browser:lambda:x=>x.type"
  prim__type : StyleSheet -> PrimIO String

namespace StyleSheetList

  export
  %foreign "browser:lambda:x=>x.length"
  prim__length : StyleSheetList -> PrimIO Bits32

  export
  %foreign "browser:lambda:(x,a)=>x.item(a)"
  prim__item : StyleSheetList -> Bits32 -> PrimIO (Nullable CSSStyleSheet)

--------------------------------------------------------------------------------
--          Mixins
--------------------------------------------------------------------------------

namespace ElementCSSInlineStyle

  export
  %foreign "browser:lambda:x=>x.style"
  prim__style : ElementCSSInlineStyle -> PrimIO CSSStyleDeclaration

namespace LinkStyle

  export
  %foreign "browser:lambda:x=>x.sheet"
  prim__sheet : LinkStyle -> PrimIO (Nullable CSSStyleSheet)


text:
module Pow

namespace Preloaded
  %access public export
  %default total

  ||| Divides a natural number by 2 and returns
  ||| the quotient and the remainder as a boolean value:
  ||| True = remainder is 1, False = remainder is 0.
  divMod2 : Nat -> (Nat, Bool)
  divMod2 Z     = (Z, False)
  divMod2 (S Z) = (Z, True)
  divMod2 (S (S n)) = case divMod2 n of (q, r) => (S q, r)

  -- The first argument (k) helps Idris to prove
  -- that the function terminates.
  powSqrAux : Nat -> Nat -> Nat -> Nat
  powSqrAux Z _ _ = 1
  powSqrAux _ _ Z = 1
  powSqrAux (S k) b e =
      case divMod2 e of
          (e', False) => powSqrAux k (b * b) e'
          (e', True) => b * powSqrAux k (b * b) e'

  powSqr : Nat -> Nat -> Nat
  powSqr b e = powSqrAux e b e

%access export
%default total

-- The following lemma is useful
divMod2Lemma : (n : Nat) -> n = 2 * fst (divMod2 n) + if snd (divMod2 n) then 1 else 0
divMod2Lemma Z     = Refl
divMod2Lemma (S Z) = Refl
divMod2Lemma (S (S k)) with (divMod2 k) proof eq
    | (q, _) = rewrite divMod2Lemma k in
               rewrite sym eq in
               rewrite sym $ plusSuccRightSucc q (q + 0) in
               Refl

powEq : (b, e : Nat) -> powSqr b e = power b e
powEq b e with (divMod2 e) proof eq
  | (e', True)  = ?proof_rhs_1
  | (e', False) = rewrite divMod2Lemma e in
                  rewrite sym eq in
                  rewrite plusZeroRightNeutral e' in
                  rewrite plusZeroRightNeutral $ e'+e' in
                  ?proof_rhs_2

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
module Mod1

foo : Nat
foo = 1


text:
module Lists

%access public export
%default total

--proof that something is an element of the list
total
isElementOfList : (typ : Type) -> (ls : List typ) -> (a : typ) -> Type
isElementOfList typ ls a = (n : Nat ** (fromMaybe (index' n ls) = a))

--proof that right addition preserves equality (somehow cong was messing up)
total
addl: (x: Type) -> (z: List x) -> (l = y) -> (l ++ z = y ++ z)
addl x z Refl = Refl

-- Proof that the auxiliary reverseOnto used to define rev behaves the way it should (semi-pseudo-contravariantly as I choose to call it)
total
revontoeq: (x: Type) -> (y: List x) -> (l: List x) -> ((reverseOnto y l)  = ((reverseOnto [] l) ++ y))
revontoeq x y [] = Refl
revontoeq x [] (z :: xs) = sym (appendNilRightNeutral (reverseOnto [] (z::xs)))
revontoeq x (y :: ys) (z :: xs) = trans (trans (revontoeq x (z::y::ys) xs) ((appendAssociative (reverseOnto [] xs) [z] (y::ys)))) (sym (addl x (y::ys) (revontoeq x [z] xs)))

--Proof that reverse is pseudo-contravariant on concatenation
total
reviscontra: (x: Type) -> (y: List x) -> (l: List x) -> (reverse(y++l) =  reverse(l)++reverse(y))
reviscontra x [] z = sym (appendNilRightNeutral (reverseOnto [] z))
reviscontra x (y :: xs) z = trans (trans (trans (revontoeq x [y] (xs++z)) (addl x [y] (reviscontra x xs z))) (sym (appendAssociative (reverse z) (reverse xs) [y]))) (cong(sym (revontoeq x [y] xs)))

-- Proof that the reverse function is self-inverse
total
reveq: (x: Type) -> (l: List x) -> (l = reverse(reverse l))
reveq x [] = Refl
reveq x (y :: xs) = sym (trans (trans (cong(reviscontra x [y] xs)) (reviscontra x (reverse xs) (reverse [y]))) (cong(sym (reveq x xs))))


text:
module Diff

-- Based on https://arxiv.org/pdf/1803.10228.pdf

import src.Expr

interface DiffSymantics (rep : TypeT -> Type) where
  d : Double -> rep DoubleT
  (+) : rep DoubleT -> rep DoubleT -> rep DoubleT
  (*) : rep DoubleT -> rep DoubleT -> rep DoubleT
  grad : (rep DoubleT -> rep DoubleT) -> Code (ArrowT DoubleT DoubleT)

data Reverse : TypeT -> Type where
  R : (((Code DoubleT, Code (VarT DoubleT)) -> Code UnitT) -> Code UnitT) -> Reverse a

DiffSymantics Reverse where
  d x = R (\k => letVal (double x) (\x => newVar (double 0) (\d => k (x, d))))

  (+) (R l) (R r) = R (\k => l (\(lv, ld) =>
                             r (\(rv, rd) => letVal (lv <+> rv) (\x =>
                                             newVar (double 0) (\d =>
                                                  seqs [k (x, d),
                                                  assign (deref ld <+> deref d) ld,
                                                  assign (deref rd <+> deref d) rd])))))

  (*) (R l) (R r) = R (\k => l (\(lv, ld) =>
                             r (\(rv, rd) => letVal (lv <*> rv) (\x =>
                                             newVar (double 0) (\d =>
                                                  seqs [k (x, d),
                                                  assign ((deref d <*> rv) <+> deref ld) ld,
                                                  assign ((deref d <*> lv) <+> deref rd) rd])))))

  grad f = lam (\x =>  newVar (double 0) (\d => let (R g) = f $ R (\k => k (x, d)) in
                                                seq (g (\(_, d) => assign (double 1) d)) (deref d)))

example : DiffSymantics rep => rep DoubleT -> rep DoubleT
example x = (d 2 * x) + (x * x * x)

test : String
test = compile (grad {rep = Reverse} example)

max_stars_repo_name: STELIORD/idris-snippets

max_issues_repo_name: stjordanis/idris-snippets

max_forks_repo_name: stjordanis/idris-snippets


text:
module Stochastic

import Simple
import Effects
import Effect.Random

%default total

data Rule : Type -> Type where
  MkRule : a -> List (Int, List a) -> Rule a

data StochasticLSystem : Type -> Type where
  MkStoch : List a -> List (Rule a) -> StochasticLSystem a

makeGenerator : Eq a => List (Rule a) -> Eff (a -> List a) [RND]
makeGenerator _ = pure $ \x => [x]
--todo: finish

translate : Eq a => StochasticLSystem a -> Eff (LSys a) [RND]
translate (MkStoch axiom rules) = do
  generator <- makeGenerator rules
  pure $ MkLSys axiom generator

max_stars_repo_name: PeterHajdu/ilsys

max_issues_repo_name: PeterHajdu/ilsys

max_forks_repo_name: PeterHajdu/ilsys


text:
> module NonNegRational.Measures

> import Syntax.PreorderReasoning

> import NonNegRational.NonNegRational
> import NonNegRational.BasicOperations
> import NonNegRational.BasicProperties
> import Nat.Positive
> import Fraction.Fraction
> import Fraction.Normal

> %default total
> %access public export
> %auto_implicits off

> |||
> factor : {A : Type} -> List A -> NonNegRational
> factor Nil = 1
> factor (a :: as) = fromFraction (1, Element (S (length as)) MkPositive)

> |||
> average : List NonNegRational -> NonNegRational
> average xs = (sum xs) * (factor xs)

> {-

> ---}

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
module Replica.Other.String

import Data.List
import Data.String
import Data.String.Extra

%default total

export
separator : Nat -> String
separator = pack . flip replicate '-'

export
withOffset : Nat -> String -> String
withOffset k = (++) (pack $ replicate k ' ')

export
removeTrailingNL : String -> String
removeTrailingNL str = if "\n" `isSuffixOf` str then dropLast 1 str else str

max_stars_repo_name: claymager/REPLica

max_issues_repo_name: claymager/REPLica

max_forks_repo_name: claymager/REPLica


text:
module NatGCD

import NatUtils
import NatOrder
import NatDivisors

%default total
%access public export

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

-- Definitions

|||Type of proof that d is the GCD of a and b, where atleast one of a and b are non-zero
isGCD : (a : Nat) -> (b : Nat) -> (g : Nat) -> Type
isGCD a b g = ((isCommonDivisor a b g), (isMaxDivisor a b g))

|||Type that stores the GCD of two numbers
gcd : (a : Nat) -> (b : Nat) -> Type
gcd a b = (d : Nat ** (isGCD a b d))

|||Type of proof that a and b are coprime
coprime : (a : Nat) -> (b : Nat) -> Type
coprime a b = ((n : Nat) -> (isCommonDivisor a b n) -> (n = 1))

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

--Basic proofs involving GCDs and coprime numbers

|||Proof that if a1 = a2, b1 = b2 then gcd (a1, b1) = gcd (a2, b2)
eqConservesGCD : {a1 : Nat} -> {b1 : Nat} -> {g1 : Nat} ->
			  {a2 : Nat} -> {b2 : Nat} -> {g2 : Nat} ->
			  (a1 = a2) -> (b1 = b2) -> (g1 = g2) ->
			  (isGCD a1 b1 g1) -> (isGCD a2 b2 g2)
eqConservesGCD {a1} {b1} {g1} Refl Refl Refl proofGCD = proofGCD

|||Proof that if a1 = a2, b1 = b2 and a1 and b1 are coprime, a2 and b2 are coprime
eqConservesCoprime : {a1 : Nat} -> {b1 : Nat} -> {a2 : Nat} -> {b2 : Nat} ->
				 (a1 = a2) -> (b1 = b2) -> (coprime a1 b1) -> (coprime a2 b2)
eqConservesCoprime {a1} {b1} Refl Refl proofCoprime = proofCoprime

|||Proof that the gcd is unique
gcdUnique : {a : Nat} -> {b : Nat} ->
		  (gcd1 : (gcd a b)) -> (gcd2 : (gcd a b)) -> ((fst gcd1) = (fst gcd2))
gcdUnique {a} {b} (g1 ** (commDiv1, maxDiv1)) (g2 ** (commDiv2, maxDiv2)) = dividesAntiSymmetric (maxDiv1 g2 commDiv2) (maxDiv2 g1 commDiv1)

|||Proof that gcd is symmetric
gcdSymmetric : {a : Nat} -> {b : Nat} -> {g : Nat} -> (isGCD a b g) -> (isGCD b a g)
gcdSymmetric {a} {b} {g} (commonDiv, maxDiv) = (commonDivisorSymmetric commonDiv, (\n => (\commDiv => (maxDiv n (commonDivisorSymmetric commDiv)))))

|||Proof that coprimality is symmetric
coprimeSymmetric : {a : Nat} -> {b : Nat} -> (coprime a b) -> (coprime b a)
coprimeSymmetric {a} {b} proofCoprime =
	(\n => (\commDiv => (proofCoprime n (commonDivisorSymmetric commDiv))))

|||Proof that gcd (a, b) = 1 implies a and b are coprime
gcdOneImpliesCoprime : {a : Nat} -> {b : Nat} -> (isGCD a b 1) -> (coprime a b)
gcdOneImpliesCoprime {a} {b} (commonDivisor, maxDivisor) =
	(\n => (\commonDiv => dividesAntiSymmetric oneDivides (maxDivisor n commonDiv)))

|||Proof that gcd (a, b) exists implies that both a and b are not zero
gcdImpliesNotBothZ : {a : Nat} -> {b : Nat} -> {g : Nat} ->
				 (isGCD a b g) -> Either (Not (a = Z)) (Not (b = Z))
gcdImpliesNotBothZ {a = Z} {b = Z} {g} (commonDiv, maxDiv) =
	void ((lneqImpliesNotLEQ (ltToLNEQ lteRefl)) (dividesImpliesGEQ (maxDiv (S g) (zeroDivisible SIsNotZ, zeroDivisible SIsNotZ)) (snd (snd (fst commonDiv)))))
gcdImpliesNotBothZ {a = (S k)} {b} {g} _ = (Left SIsNotZ)
gcdImpliesNotBothZ {a} {b = (S l)} {g} _ = (Right SIsNotZ)

|||Proof that a and b are coprime implies gcd (a, b) = 1
coprimeImpliesGCDOne : {a : Nat} -> {b : Nat} -> (coprime a b) -> (isGCD a b 1)
coprimeImpliesGCDOne {a} {b} proofCoprime = (oneCommonDivisor, (\n => (\commonDiv => eqConservesDivisible oneDivides Refl (sym (proofCoprime n commonDiv)))))

|||Proof that given g = gcd (a, b), 1 = gcd(a/g, b/g)
divImpliesGCDOne : {a : Nat} -> {b : Nat} -> {g : Nat} -> (proofGCD : isGCD a b g) ->
			    (isGCD (fst (fst (fst proofGCD))) (fst (snd (fst proofGCD))) 1)
divImpliesGCDOne {a} {b} {g} ((divLeft1, divRight1), maxDiv) =
	coprimeImpliesGCDOne proofCoprime where
		proofCoprime : (coprime (fst divLeft1) (fst divRight1))
		proofCoprime n (divLeft2, divRight2) = (multLeftIdIsOne (snd (snd divLeft1)) (dividesAntiSymmetric (dividesMultiple (divisionReflexive (snd (snd divLeft1))) n) (maxDiv (n * g) (multipleDivides divLeft1 divLeft2, multipleDivides divRight1 divRight2))))

|||Generates gcd (a, Z) given a and a proof that a != 0
gcdRightZero : (a : Nat) -> (Not (a = Z)) -> (gcd a Z)
gcdRightZero a notZ = (a ** ((zeroCommonDivisorRight notZ, (\n => (\proofCommonDivisor => (fst proofCommonDivisor))))))

|||Generates gcd (Z, b) given b and a proof that b != 0
gcdLeftZero : (b : Nat) -> (Not (b = Z)) -> (gcd Z b)
gcdLeftZero b notZ = (b ** (zeroCommonDivisorLeft notZ, (\n => (\proofCommonDivisor => (snd proofCommonDivisor)))))

|||Proof that gcd (a, Z) = a
gcdRightZeroRefl : (a : Nat) -> (proofGCD : (gcd a Z)) -> (a = (fst proofGCD))
gcdRightZeroRefl a (g ** ((divA, divZ), maxDiv)) =
	case (gcdImpliesNotBothZ ((divA, divZ), maxDiv)) of
		(Left notZ) => dividesAntiSymmetric divA (maxDiv a ((divisionReflexive notZ), (zeroDivisible notZ)))
		(Right notZ) => void (notZ Refl)

|||Proof that gcd (Z, b) = b
gcdLeftZeroRefl : (b : Nat) -> (proofGCD : (gcd Z b)) -> (b = (fst proofGCD))
gcdLeftZeroRefl b (g ** ((divZ, divB), maxDiv)) =
	case (gcdImpliesNotBothZ ((divZ, divB), maxDiv)) of
		(Left notZ) => void (notZ Refl)
		(Right notZ) => dividesAntiSymmetric divB (maxDiv b ((zeroDivisible notZ), (divisionReflexive notZ)))

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

--Proofs used in Euclid's division algorithm for the GCD

|||Proof that given gcd (b, r) = g, a = r + q * b, and b ! = 0, gcd (a, b) = g
remainderExtendsGCD : {a : Nat} -> {b : Nat} -> {g : Nat} -> {r : Nat} -> {q : Nat} ->
				  (isGCD b r g) -> (a = r + (q * b)) -> (isGCD a b g)
remainderExtendsGCD {a} {b} {g} {r} {q} (commDiv, maxDiv) proofEq =
	(remExtendsCommDiv commDiv proofEq, remExtendsMaxDiv maxDiv proofEq)

|||Proof that given gcd (a, b) = g, a = r + q * b, and b ! = 0, gcd (b, r) = g
remainderConservesGCD : {a : Nat} -> {b : Nat} -> {g : Nat} -> {r : Nat} -> {q : Nat} ->
				    (isGCD a b g) -> (a = r + (q * b)) -> (isGCD b r g)
remainderConservesGCD {a} {b} {g} {r} {q} (commDiv, maxDiv) proofEq =
	(remConservesCommDiv commDiv proofEq, remConservesMaxDiv maxDiv proofEq)

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

-- Euclid's algorithm for the GCD of two numbers

|||Returns gcd (a, b) with proof that it is the gcd
euclidGCD : (a : Nat) -> (b : Nat) -> (Either (Not (a = Z)) (Not (b = Z))) -> (gcd a b)
euclidGCD a b notBothZ =
	euclidRecursion a b notBothZ (\a => (\b => (gcd a b))) gcdRightZero gcdLeftZero (\proofGCD => (\proofEq => ((fst proofGCD) ** remainderExtendsGCD (snd proofGCD) proofEq)))

|||Returns gcd (a, b) with proof that it is the gcd and an auxilliary proof
euclidGCDExtend : (a : Nat) -> (b : Nat) -> (Either (Not (a = Z)) (Not (b = Z))) ->
(proofType : (Nat -> Nat -> Nat -> Type)) ->
(baseLeft : (k : Nat) -> (Not (k = Z)) -> (proofType k Z k)) ->
(baseRight : (k : Nat) -> (Not (k = Z)) -> (proofType Z k k)) ->
(proofExtend : {a1 : Nat} -> {b1 : Nat} -> {g1 : Nat} -> {r1 : Nat} -> {q1 : Nat} -> (proofType b1 r1 g1) -> (a1 = r1 + (q1 * b1)) -> (isGCD b1 r1 g1) -> (proofType a1 b1 g1)) ->
(g : Nat ** ((isGCD a b g), (proofType a b g)))

euclidGCDExtend a b notBothZ proofType baseLeft baseRight proofExtend =
	(euclidRecursion a b notBothZ (\a => (\b => (typeNew a b))) baseLeftNew baseRightNew extendNew) where

	typeNew : Nat -> Nat -> Type
	typeNew a b = (g : Nat ** ((isGCD a b g), (proofType a b g)))

	baseLeftNew : (k : Nat) -> (Not (k = Z)) -> (typeNew k Z)
	baseLeftNew k notZ = (k ** ((snd (gcdRightZero k notZ)), (baseLeft k notZ)))

	baseRightNew : (k : Nat) -> (Not (k = Z)) -> (typeNew Z k)
	baseRightNew k notZ = (k ** ((snd (gcdLeftZero k notZ)), (baseRight k notZ)))

	extendNew : {a1 : Nat} -> {b1 : Nat} -> {r1 : Nat} -> {q1 : Nat} -> (typeNew b1 r1) -> (a1 = r1 + (q1 * b1)) -> (typeNew a1 b1)
	extendNew (g ** (proofGCD, proofAux)) proofEq = (g ** ((remainderExtendsGCD proofGCD proofEq), (proofExtend proofAux proofEq proofGCD)))

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

--More proofs

|||Proof that if g = gcd (a, b) and n != 0, n * g = gcd (n * a, n * b)
gcdMult : {a : Nat} -> {b : Nat} -> {g : Nat} ->
		(isGCD a b g) -> (n : Nat) -> (Not (n = Z)) -> (isGCD (n * a) (n * b) (n * g))

gcdMult {a} {b} {g} proofGCD n notZ = ((euclidRecursion a b (gcdImpliesNotBothZ proofGCD) (\a => (\b => proofType a b)) baseLeft baseRight proofExtend) g proofGCD n notZ) where

	proofType : Nat -> Nat -> Type
	proofType a1 b1 = (g1 : Nat) -> (isGCD a1 b1 g1) -> (n1 : Nat) -> (Not (n1 = Z)) -> (isGCD (n1 * a1) (n1 * b1) (n1 * g1))

	baseLeft : (k : Nat) -> (Not (k = Z)) -> (proofType k Z)
	baseLeft k kNotZ g1 prfGCD n1 nNotZ = (eqConservesGCD Refl (sym (multZeroRightZero n1)) proofEq (snd (gcdRightZero (n1 * k) (nonZeroMultNotZero nNotZ kNotZ)))) where
		proofEq = (cong {f = (\l => n1 * l)} (gcdRightZeroRefl k (g1 ** prfGCD)))

	baseRight : (k : Nat) -> (Not (k = Z)) -> (proofType Z k)
	baseRight k kNotZ g1 prfGCD n1 nNotZ = (eqConservesGCD (sym (multZeroRightZero n1)) Refl proofEq (snd (gcdLeftZero (n1 * k) (nonZeroMultNotZero nNotZ kNotZ)))) where
		proofEq = (cong {f = (\l => n1 * l)} (gcdLeftZeroRefl k (g1 ** prfGCD)))

	proofExtend : {a1 : Nat} -> {b1 : Nat} -> {r1 : Nat} -> {q1 : Nat} -> (proofType b1 r1) -> (a1 = r1 + (q1 * b1)) -> (proofType a1 b1)
	proofExtend {a1} {b1} {r1} {q1} remProof proofEq g1 prfGCD n1 nNotZ = (remainderExtendsGCD (remProof g1 (remainderConservesGCD prfGCD proofEq) n1 nNotZ) (extendEqualMult proofEq n1))

|||Proof that d divides (a * b) and d and a are coprime implies d divides b
coprimeImpliesDiv : {d : Nat} -> {a : Nat} -> {b : Nat} ->
				(isDivisible (a * b) d) -> (coprime a d) -> (isDivisible b d)
coprimeImpliesDiv {d} {a} {b = Z} (k ** (proofDiv, notZ)) _ = zeroDivisible notZ
coprimeImpliesDiv {d} {a} {b = (S n)} (k ** (proofDiv, notZ)) proofCoprime = eqConservesDivisible ((snd (gcdMult (coprimeImpliesGCDOne proofCoprime) (S n) SIsNotZ)) d (eqConservesDivisible (k ** (proofDiv, notZ)) (multCommutative a (S n)) Refl, dividesMultiple (divisionReflexive notZ) (S n))) (multOneRightNeutral (S n)) Refl

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

--deprecated functions

{-

|||Returns gcd (a, b) with proof that it is the gcd (helper function with bound to make euclidGCD total)
euclidGCDBound : (bound : Nat) -> (a : Nat) -> (b : Nat) -> (LTE a bound) -> (LTE (S b) bound) -> (Either (Not (a = Z)) (Not (b = Z))) -> (d : Nat ** (isGCD a b d))

euclidGCDBound bound a b leftLTE rightLTE notBothZ =
	euclidGCDBoundGen bound a b leftLTE rightLTE notBothZ isGCD baseLeft baseRight remainderExtendsGCD where
		baseLeft = (\a => (\notZ => (a ** ((zeroCommonDivisorRight notZ, (\n => (\proofCommonDivisor => (fst proofCommonDivisor))))))))
		baseRight = (\b => (\notZ => (b ** (zeroCommonDivisorLeft notZ, (\n => (\proofCommonDivisor => (snd proofCommonDivisor)))))))

euclidGCDBound _ Z Z _ _ notBothZ =
	case notBothZ of
		Left notZ => void (notZ Refl)
		Right notZ => void (notZ Refl)
euclidGCDBound _ (S a) Z _ _ _ = ((S a) ** ((zeroCommonDivisorRight SIsNotZ, (\n => (\proofCommonDivisor => (fst proofCommonDivisor))))))
euclidGCDBound _ Z (S b) _ _ _ = ((S b) ** (zeroCommonDivisorLeft SIsNotZ, (\n => (\proofCommonDivisor => (snd proofCommonDivisor)))))
euclidGCDBound Z (S a) (S b) lteLeft lteRight _ = void (succNotLTEzero lteLeft)
euclidGCDBound (S bound) (S a) (S b) (LTESucc lteLeft) (LTESucc lteRight) notBothZ =
	case (euclidDivide (S a) (S b) SIsNotZ) of
	(q ** (r ** (proofEq, proofLNEQ))) =>
		case (euclidGCDBound bound (S b) r lteRight (lteTransitive (lneqToLT proofLNEQ) lteRight) (Left SIsNotZ)) of
		(d ** proofGCD) =>
			(d ** remainderExtendsGCD SIsNotZ proofEq proofGCD)
-}

{-

euclidGCD a b notBothZ =
	case (isLTE a b) of
		(Yes proofLTE) => euclidGCDBound (S b) a b (lteTransitive proofLTE (lteSuccRight lteRefl)) lteRefl notBothZ
		(No proofNotLTE) => euclidGCDBound (S a) a b (lteSuccRight lteRefl) (LTESucc (notLTEImpliesGTE proofNotLTE)) notBothZ

-}


text:
module gcd

import NatUtils

%default total
%access public export

|||Auxilliary proof for euclidDivide
--Proof to finish euclidDivide, couldn't add it as a where clause within euclidDivide. If someone knows how to do that, please do so.
extendedEqualityProof : (a : Nat) -> (b : Nat) -> (q : Nat) -> (r : Nat)->
					((S r) = b) -> (a = r + (q * b)) -> (S a = (S q) * b)
extendedEqualityProof a b q r proofSmlEq proofBigEq =
	trans (cong proofBigEq) (plusConstantRight (S r) b (q * b) proofSmlEq)

||| Given a, b, and a proof that b != 0, returns (q, r) and proofs that a = bq + r, r < b
--removed possible problems with Rohit's
euclidDivide : (a : Nat) -> (b : Nat) ->
  (b = Z -> Void) -> (q : Nat ** (r : Nat ** ((a = r + (q * b)), LT r b)))
euclidDivide a Z pf = void(pf Refl)
euclidDivide Z (S k) SIsNotZ = (Z ** (Z ** (Refl, LTESucc LTEZero)))
euclidDivide (S n) (S k) SIsNotZ =
  case (euclidDivide n (S k) SIsNotZ) of
		(q ** (r ** (equalityProof, ltproof))) =>
        case (ltImpliesEqOrLT r (S k) ltproof) of
						(Right proofSrLTSk) => (q ** ((S r) ** ((cong equalityProof), proofSrLTSk)))
						(Left proofSreqSk) => ((S q) ** (Z ** ((extendedEqualityProof n (S k) q r proofSreqSk equalityProof), LTESucc LTEZero)))

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

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

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

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

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

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

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

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

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

|||Proof that d divides a implies d divides c * a
dividesMultiple : {a : Nat} -> {d : Nat} -> (isDivisible a d proofNotZ) -> (c : Nat)-> (isDivisible (c * a) d proofNotZ)
dividesMultiple {d} (n ** Refl) c = ((c * n) ** (rewrite (multAssociative c n d) in Refl))

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

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

|||Proof d divides a and a = b implies d divides b
eqConservesDivisible : {a : Nat} -> {b : Nat} -> {d : Nat} -> {proofNotZ : Not (d = Z)} ->
					(isDivisible a d proofNotZ) -> (a = b) -> (isDivisible b d proofNotZ)
eqConservesDivisible {a} {d} (n ** proofDivides) Refl = (n ** proofDivides)

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


text:
module Js.DOM.Document

import Control.Monad.Syntax
import Js
import Js.Object
import Js.DOM.Element

%default total
%access export

getElement : (id : String) -> JS_IO Element
getElement = js "document.getElementById(%0)" (String -> JS_IO Ptr) >=> pure . MkElement

write : String -> JS_IO ()
write = js "document.write(%0)" (String -> JS_IO ())

max_stars_repo_name: jheiling/idris-js

max_issues_repo_name: jheiling/idris-js

max_forks_repo_name: jheiling/idris-js


text:
module Ex7

import Data.List

%default total

data Shape = Triangle Double Double
           | Rectangle Double Double
           | Circle Double

area : Shape -> Double
area (Triangle b h) = 0.5 * b * h
area (Rectangle l b) = l * b
area (Circle r) = pi * r * r

Eq Shape where
  (==) (Triangle x y) (Triangle a b) = x == a && y == b
  (==) (Rectangle x y) (Rectangle a b) = x == a && y == b
  (==) (Circle x) (Circle y) = x == y
  (==) _ _  = False

Ord Shape where
  compare x y = compare (area x) (area y)

testShapes : List Shape
testShapes = [Circle 3, Triangle 3 9, Rectangle 2 6, Circle 4, Rectangle 2 7]

data Expr num = Val num
              | Add (Expr num) (Expr num)
              | Sub (Expr num) (Expr num)
              | Mul (Expr num) (Expr num)
              | Div (Expr num) (Expr num)
              | Abs (Expr num)

eval : (Abs ty, Neg ty, Integral ty) => Expr ty -> ty
eval (Val num) = num
eval (Add x y) = eval x + eval y
eval (Sub x y) = eval x - eval y
eval (Mul x y) = eval x * eval y
eval (Div x y) = eval x `div` eval y
eval (Abs x) = abs (eval x)

Num ty => Num (Expr ty) where
  (+) = Add
  (*) = Mul
  fromInteger = Val . fromInteger

Neg ty => Neg (Expr ty) where
  negate x = 0 - x
  (-) = Sub

Abs ty => Abs (Expr ty) where
  abs = Abs

Show ty => Show (Expr ty) where
  show (Val n) = show n
  show (Add x y) = "(" ++ show x ++ " + " ++ show y ++ ")"
  show (Sub x y) = "(" ++ show x ++ " - " ++ show y ++ ")"
  show (Mul x y) = "(" ++ show x ++ " * " ++ show y ++ ")"
  show (Div x y) = "(" ++ show x ++ " / " ++ show y ++ ")"
  show (Abs x) = "abs (" ++ show x ++ ")"

(Eq ty, Neg ty, Integral ty, Abs ty) => Eq (Expr ty) where
  (==) x y = eval x == eval y

e0 : Expr Int
e0 = Add (Val 6) (Mul (Val 3) (Val 12))

e1 : Expr Int
e1 = Add (Mul (Val 3) (Val 6)) (Val 12)

(Abs ty, Neg ty, Integral ty) => Cast (Expr ty) ty where
  cast e = eval e

foobar : Integer
foobar = let x = the (Expr Integer) 6 * 3 + 12 in
             the Integer (cast x)

foobaz : Int
foobaz = let y = the (Expr Int) 1 + 2 * 3 + 4 * 5 in
             the Int (cast y)

Functor Expr where
  -- map : (a -> b) -> Expr a -> Expr b
  map func (Val n) = Val (func n)
  map func (Add x y) = Add (map func x) (map func y)
  map func (Sub x y) = Sub (map func x) (map func y)
  map func (Mul x y) = Mul (map func x) (map func y)
  map func (Div x y) = Div (map func x) (map func y)
  map func (Abs x) = Abs (map func x)

data Vect : (len : Nat) -> (elem : Type) -> Type where
  Nil : Vect Z elem
  (::) : (x : elem) -> Vect len elem -> Vect (S len) elem

Eq elem => Eq (Vect n elem) where
  (==) [] [] = True
  (==) (x :: xs) (y :: ys) = x == y && xs == ys

Foldable (Vect n) where
  -- foldr : (a -> b -> b) -> b -> Vect n a -> b
  foldr func acc [] = acc
  foldr func acc (x :: xs) = func x (foldr func acc xs)

max_stars_repo_name: timmyjose-study/tdd-with-idris

max_issues_repo_name: timmyjose-study/tdd-with-idris

max_forks_repo_name: timmyjose-study/tdd-with-idris


text:
-- ---------------------------------------------------------------- [ Util.idr ]

module Data.ML.Util

%access public export

||| Convert a Bool to an Integer, as in C99's <stdbool.h>.
||| @ bool a Bool to convert
boolToInteger : (bool : Bool) -> Integer
boolToInteger False = 0
boolToInteger True  = 1

||| Cast Bools to Integers via `boolToInteger`.
implementation Cast Bool Integer where
  cast = boolToInteger

||| Simplified clone of `numpy.unique`.
|||
||| Return the sorted unique elements of a list.
|||
||| ```
||| unique = sort . nub
||| ```
unique : Ord a => List a -> List a
unique = sort . nub

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

max_stars_repo_name: yurrriq/real-world-machine-learning

max_issues_repo_name: yurrriq/real-world-machine-learning

max_forks_repo_name: yurrriq/real-world-machine-learning


text:
module Client.Action.Test

import Client.Action.Build as Build
import Fmt
import Inigo.Async.Base
import Inigo.Async.Promise
import Inigo.Package.CodeGen as CodeGen
import Inigo.Package.Package

-- TODO: Consider moving this out from Inigo into toml config
export
test : CodeGen -> Promise ()
test codeGen =
  do
    pkg <- Build.writeIPkgFile
    log (fmt "Running tests...")
    ignore $ system "idris2" ["--find-ipkg", "Test/Suite.idr", "--cg", CodeGen.toString codeGen, "-x", "suite"] Nothing True True

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo