text:
> module SequentialDecisionProblems.applications.Main

> import Data.Fin
> import Data.List
> import Data.List.Quantifiers
> import Data.Vect
> import Data.So
> import Effects
> import Effect.Exception
> import Effect.StdIO

> import SequentialDecisionProblems.CoreTheory
> import SequentialDecisionProblems.FullTheory
> import SequentialDecisionProblems.TabBackwardsInduction1
> import SequentialDecisionProblems.Utils
> import SequentialDecisionProblems.FastStochasticDefaults
> import SequentialDecisionProblems.CoreTheoryOptDefaults
> import SequentialDecisionProblems.FullTheoryOptDefaults
> import SequentialDecisionProblems.TabBackwardsInductionOptDefaults1

> import SequentialDecisionProblems.applications.LowHigh
> import SequentialDecisionProblems.applications.AvailableUnavailable
> import SequentialDecisionProblems.applications.GoodBad

> import FastSimpleProb.SimpleProb
> import FastSimpleProb.BasicOperations
> import FastSimpleProb.BasicProperties
> import FastSimpleProb.MonadicOperations
> import FastSimpleProb.MonadicProperties
> import FastSimpleProb.Measures
> import FastSimpleProb.MeasuresProperties
> import FastSimpleProb.Operations
> import Sigma.Sigma
> import Double.Predicates
> import Double.Postulates
> import Double.Operations
> import Double.Properties
> import NonNegDouble.NonNegDouble
> import NonNegDouble.Constants
> import NonNegDouble.BasicOperations
> import NonNegDouble.Operations
> import NonNegDouble.Properties
> import NonNegDouble.Predicates
> import NonNegDouble.LTEProperties
> import Finite.Predicates
> import Finite.Operations
> import Finite.Properties
> import Decidable.Predicates
> import Decidable.Properties
> import LocalEffect.Exception
> import LocalEffect.StdIO
> import Fin.Operations
> import List.Operations
> import Vect.Operations
> import Unit.Properties

> -- %default total
> %auto_implicits off

> -- %logging 5

* Introduction

We specify a second emissions game as a stochastic sequential decision
problem with a single decision maker.

The idea is that "best" decisions on levels of greenhouse gases (GHG)
emissions (that is, how much GHG shall be allowed to be emitted in a
given time period) are affected by three major sources of uncertainty:

1) uncertainty about the (typically negative) effects of high GHG
concentrations in the atmosphere,

2) uncertainty about the availability of effective (cheap, efficient)
technologies for reducing GHG emissions,

3) uncertainty about the capability of actually implementing a decision
on a given GHG emission level.

We study the effects of 1), 2) and 3) on optimal sequences of emission
policies. The idea is to design an emission game that accounts for all
three sources of uncertainty and yet is simple enough to support
investigating the logical consequences of different assumptions through
comparisons and parametric studies.

* Controls

We consider a game in which, at each decision step, the decision maker
can select between low and high GHG emissions

> SequentialDecisionProblems.CoreTheory.Ctrl _ _ = LowHigh

Low emissions, if implemented, increase the cumulated GHG emissions less
than high emissions.

* States

At each decision step, the decision maker has to choose an option on the
basis of four data: the cumulated GHG emissions, the current emission
level (low or high), the availability of effective technologies for
reducing GHG emissions and the state of the world. Effective
technologies for reducing GHG emissions can be either available or
unavailable. The state of the world can be either good or bad:

> CumulatedEmissions : (t : Nat) -> Type
> CumulatedEmissions t = Fin (S t)

> SequentialDecisionProblems.CoreTheory.State t
> = (CumulatedEmissions t, LowHigh, AvailableUnavailable, GoodBad)

The idea is that the game starts with zero cumulated emissions, high
emission levels, unavailable GHG technologies and with the world in a
good state.

In these conditions, the probability to turn to the bad state is
low. But if the cumulated emissions increase beyond a fixed critical
threshold, the probability that the state of the world turns bad
increases. If the world is the bad state, there is no chance to come
back to the good state.

Similarly, the probability that effective technologies for reducing GHG
emissions become available increases after a fixed number of decision
steps. Once available, effective technologies stay available for ever.

The capability of actually implementing a decision on a given GHG
emission level in general depends on many factors. In our simplified
setup, we just investigate the effect of inertia: implementing low
emissions is easier when low emission policies are already in place than
when the current emission policies are high emission
policies. Similarly, implementing high emission policies is easier under
high emissions policies than under low emissions policies.

* Transition function

> -- The critical cumulated emissions threshold
> crE : Double
> crE = 4.0

> -- The critical number of decision steps
> crN : Nat
> crN = 2

> -- The probability of staying in a good world when the cumulated
> -- emissions are |<=| the critical threshold |crE|
> pS1  :  NonNegDouble
> pS1  =  cast 0.9 -- cast 0.8 -- cast 1.0 -- cast 0.9

> -- The probability of staying in a good world when the cumulated
> -- emissions are |>=| the critical threshold |crE|
> pS2  :  NonNegDouble
> pS2  =  cast 0.1 -- cast 0.2 -- cast 0.0 -- cast 0.1

> -- Sanity check
> pS2LTEpS1 : pS2 `NonNegDouble.Predicates.LTE` pS1
> pS2LTEpS1 = MkLTE Oh

> -- The probability of effective technologies for reducing GHG
> -- emissions becoming available when the number of decision steps is
> -- below |crN|
> pA1  :  NonNegDouble
> pA1  =  cast 0.1 -- cast 0.0 -- cast 0.1

> -- The probability of effective technologies for reducing GHG
> -- emissions becoming available when the number of decision steps is
> -- above |crN|
> pA2  :  NonNegDouble
> pA2  =  cast 0.9 -- cast 1.0 -- cast 0.9

> -- Sanity check
> pA1LTEpA2 : pA1 `NonNegDouble.Predicates.LTE` pA2
> pA1LTEpA2 = MkLTE Oh

> -- The probability being able to implement low emission policies when
> -- the current emissions are low and low emissions are selected
> pLL  :  NonNegDouble
> pLL  =  cast 0.9 -- cast 1.0 -- cast 0.9 -- cast 0.5

> -- The probability being able to implement low emission policies when
> -- the current emissions are high and low emissions are selected
> pLH  :  NonNegDouble
> pLH  =  cast 0.7 -- cast 1.0 -- cast 0.7 -- cast 0.5

> -- Sanity check
> pLHLTEpLL : pLH `NonNegDouble.Predicates.LTE` pLL
> pLHLTEpLL = MkLTE Oh

> -- The probability being able to implement high emission policies when
> -- the current emissions are low and high emissions are selected
> pHL  :  NonNegDouble
> pHL  =  cast 0.7 -- cast 1.0 -- cast 0.7 -- cast 0.5

> -- The probability being able to implement high emission policies when
> -- the current emissions are high and high emissions are selected
> pHH  :  NonNegDouble
> pHH  =  cast 0.9 -- cast 1.0 -- cast 0.9 -- cast 0.5

> -- Sanity check
> pHLLTEpHH : pHL `NonNegDouble.Predicates.LTE` pHH
> pHLLTEpHH = MkLTE Oh

Low emissions leave the cumulated emissions unchanged, high emissions
increase the cumulated emissions by one:

> -- The transition function:
>
> -- The transition function: high emissions
>
> -- The transition function: high emissions, unavailable GHG technologies
>
> -- The transition function: high emissions, unavailable GHG technologies, good world
>
> using implementation NumNonNegDouble
>
>   SequentialDecisionProblems.CoreTheory.nexts t (e, High, Unavailable, Good) Low =
>     let ttres = mkSimpleProb
>                 [((weaken e, Low,  Unavailable, Good),        pLH  * (one - pA1) *        pS1),
>                  ((    FS e, High, Unavailable, Good), (one - pLH) * (one - pA1) *        pS1),
>                  ((weaken e, Low,    Available, Good),        pLH  *        pA1  *        pS1),
>                  ((    FS e, High,   Available, Good), (one - pLH) *        pA1  *        pS1),
>                  ((weaken e, Low,  Unavailable,  Bad),        pLH  * (one - pA1) * (one - pS1)),
>                  ((    FS e, High, Unavailable,  Bad), (one - pLH) * (one - pA1) * (one - pS1)),
>                  ((weaken e, Low,    Available,  Bad),        pLH  *        pA1  * (one - pS1)),
>                  ((    FS e, High,   Available,  Bad), (one - pLH) *        pA1  * (one - pS1))] in
>     let tfres = mkSimpleProb
>                 [((weaken e, Low,  Unavailable, Good),        pLH  * (one - pA1) *        pS2),
>                  ((    FS e, High, Unavailable, Good), (one - pLH) * (one - pA1) *        pS2),
>                  ((weaken e, Low,    Available, Good),        pLH  *        pA1  *        pS2),
>                  ((    FS e, High,   Available, Good), (one - pLH) *        pA1  *        pS2),
>                  ((weaken e, Low,  Unavailable,  Bad),        pLH  * (one - pA1) * (one - pS2)),
>                  ((    FS e, High, Unavailable,  Bad), (one - pLH) * (one - pA1) * (one - pS2)),
>                  ((weaken e, Low,    Available,  Bad),        pLH  *        pA1  * (one - pS2)),
>                  ((    FS e, High,   Available,  Bad), (one - pLH) *        pA1  * (one - pS2))] in
>     let ftres = mkSimpleProb
>                 [((weaken e, Low,  Unavailable, Good),        pLH  * (one - pA2) *        pS1),
>                  ((    FS e, High, Unavailable, Good), (one - pLH) * (one - pA2) *        pS1),
>                  ((weaken e, Low,    Available, Good),        pLH  *        pA2  *        pS1),
>                  ((    FS e, High,   Available, Good), (one - pLH) *        pA2  *        pS1),
>                  ((weaken e, Low,  Unavailable,  Bad),        pLH  * (one - pA2) * (one - pS1)),
>                  ((    FS e, High, Unavailable,  Bad), (one - pLH) * (one - pA2) * (one - pS1)),
>                  ((weaken e, Low,    Available,  Bad),        pLH  *        pA2  * (one - pS1)),
>                  ((    FS e, High,   Available,  Bad), (one - pLH) *        pA2  * (one - pS1))] in
>     let ffres = mkSimpleProb
>                 [((weaken e, Low,  Unavailable, Good),        pLH  * (one - pA2) *        pS2),
>                  ((    FS e, High, Unavailable, Good), (one - pLH) * (one - pA2) *        pS2),
>                  ((weaken e, Low,    Available, Good),        pLH  *        pA2  *        pS2),
>                  ((    FS e, High,   Available, Good), (one - pLH) *        pA2  *        pS2),
>                  ((weaken e, Low,  Unavailable,  Bad),        pLH  * (one - pA2) * (one - pS2)),
>                  ((    FS e, High, Unavailable,  Bad), (one - pLH) * (one - pA2) * (one - pS2)),
>                  ((weaken e, Low,    Available,  Bad),        pLH  *        pA2  * (one - pS2)),
>                  ((    FS e, High,   Available,  Bad), (one - pLH) *        pA2  * (one - pS2))] in
>     case (t <= crN) of
>       True  =>   case (fromFin e <= crE) of
>                  True  =>   trim ttres
>                  False =>   trim tfres
>       False =>   case (fromFin e <= crE) of
>                  True  =>   trim ftres
>                  False =>   trim ffres
>   SequentialDecisionProblems.CoreTheory.nexts t (e, High, Unavailable, Good) High =
>     let ttres = mkSimpleProb
>                 [((weaken e, Low,  Unavailable, Good), (one - pHH) * (one - pA1) *        pS1),
>                  ((    FS e, High, Unavailable, Good),        pHH  * (one - pA1) *        pS1),
>                  ((weaken e, Low,    Available, Good), (one - pHH) *        pA1  *        pS1),
>                  ((    FS e, High,   Available, Good),        pHH  *        pA1  *        pS1),
>                  ((weaken e, Low,  Unavailable,  Bad), (one - pHH) * (one - pA1) * (one - pS1)),
>                  ((    FS e, High, Unavailable,  Bad),        pHH  * (one - pA1) * (one - pS1)),
>                  ((weaken e, Low,    Available,  Bad), (one - pHH) *        pA1  * (one - pS1)),
>                  ((    FS e, High,   Available,  Bad),        pHH  *        pA1  * (one - pS1))] in
>     let tfres = mkSimpleProb
>                 [((weaken e, Low,  Unavailable, Good), (one - pHH) * (one - pA1) *        pS2),
>                  ((    FS e, High, Unavailable, Good),        pHH  * (one - pA1) *        pS2),
>                  ((weaken e, Low,    Available, Good), (one - pHH) *        pA1  *        pS2),
>                  ((    FS e, High,   Available, Good),        pHH  *        pA1  *        pS2),
>                  ((weaken e, Low,  Unavailable,  Bad), (one - pHH) * (one - pA1) * (one - pS2)),
>                  ((    FS e, High, Unavailable,  Bad),        pHH  * (one - pA1) * (one - pS2)),
>                  ((weaken e, Low,    Available,  Bad), (one - pHH) *        pA1  * (one - pS2)),
>                  ((    FS e, High,   Available,  Bad),        pHH  *        pA1  * (one - pS2))] in
>     let ftres = mkSimpleProb
>                 [((weaken e, Low,  Unavailable, Good), (one - pHH) * (one - pA2) *        pS1),
>                  ((    FS e, High, Unavailable, Good),        pHH  * (one - pA2) *        pS1),
>                  ((weaken e, Low,    Available, Good), (one - pHH) *        pA2  *        pS1),
>                  ((    FS e, High,   Available, Good),        pHH  *        pA2  *        pS1),
>                  ((weaken e, Low,  Unavailable,  Bad), (one - pHH) * (one - pA2) * (one - pS1)),
>                  ((    FS e, High, Unavailable,  Bad),        pHH  * (one - pA2) * (one - pS1)),
>                  ((weaken e, Low,    Available,  Bad), (one - pHH) *        pA2  * (one - pS1)),
>                  ((    FS e, High,   Available,  Bad),        pHH  *        pA2  * (one - pS1))] in
>     let ffres = mkSimpleProb
>                 [((weaken e, Low,  Unavailable, Good), (one - pHH) * (one - pA2) *        pS2),
>                  ((    FS e, High, Unavailable, Good),        pHH  * (one - pA2) *        pS2),
>                  ((weaken e, Low,    Available, Good), (one - pHH) *        pA2  *        pS2),
>                  ((    FS e, High,   Available, Good),        pHH  *        pA2  *        pS2),
>                  ((weaken e, Low,  Unavailable,  Bad), (one - pHH) * (one - pA2) * (one - pS2)),
>                  ((    FS e, High, Unavailable,  Bad),        pHH  * (one - pA2) * (one - pS2)),
>                  ((weaken e, Low,    Available,  Bad), (one - pHH) *        pA2  * (one - pS2)),
>                  ((    FS e, High,   Available,  Bad),        pHH  *        pA2  * (one - pS2))] in
>     case (t <= crN) of
>       True  =>   case (fromFin e <= crE) of
>                  True  =>   trim ttres
>                  False =>   trim tfres
>       False =>   case (fromFin e <= crE) of
>                  True  =>   trim ftres
>                  False =>   trim ffres
>
>   -- The transition function: high emissions, unavailable GHG technologies, bad world
>   SequentialDecisionProblems.CoreTheory.nexts t (e, High, Unavailable, Bad) Low =
>     let ttres = mkSimpleProb
>                 [((weaken e, Low,  Unavailable,  Bad),        pLH  * (one - pA1)),
>                  ((    FS e, High, Unavailable,  Bad), (one - pLH) * (one - pA1)),
>                  ((weaken e, Low,    Available,  Bad),        pLH  *        pA1 ),
>                  ((    FS e, High,   Available,  Bad), (one - pLH) *        pA1 )] in
>     let tfres = mkSimpleProb
>                 [((weaken e, Low,  Unavailable,  Bad),        pLH  * (one - pA1)),
>                  ((    FS e, High, Unavailable,  Bad), (one - pLH) * (one - pA1)),
>                  ((weaken e, Low,    Available,  Bad),        pLH  *        pA1 ),
>                  ((    FS e, High,   Available,  Bad), (one - pLH) *        pA1 )] in
>     let ftres = mkSimpleProb
>                 [((weaken e, Low,  Unavailable,  Bad),        pLH  * (one - pA2)),
>                  ((    FS e, High, Unavailable,  Bad), (one - pLH) * (one - pA2)),
>                  ((weaken e, Low,    Available,  Bad),        pLH  *        pA2 ),
>                  ((    FS e, High,   Available,  Bad), (one - pLH) *        pA2 )] in
>     let ffres = mkSimpleProb
>                 [((weaken e, Low,  Unavailable,  Bad),        pLH  * (one - pA2)),
>                  ((    FS e, High, Unavailable,  Bad), (one - pLH) * (one - pA2)),
>                  ((weaken e, Low,    Available,  Bad),        pLH  *        pA2 ),
>                  ((    FS e, High,   Available,  Bad), (one - pLH) *        pA2 )] in
>     case (t <= crN) of
>       True  =>   case (fromFin e <= crE) of
>                  True  =>   trim ttres
>                  False =>   trim tfres
>       False =>   case (fromFin e <= crE) of
>                  True  =>   trim ftres
>                  False =>   trim ffres
>   SequentialDecisionProblems.CoreTheory.nexts t (e, High, Unavailable, Bad) High =
>     let ttres = mkSimpleProb
>                 [((weaken e, Low,  Unavailable,  Bad), (one - pHH) * (one - pA1)),
>                  ((    FS e, High, Unavailable,  Bad),        pHH  * (one - pA1)),
>                  ((weaken e, Low,    Available,  Bad), (one - pHH) *        pA1 ),
>                  ((    FS e, High,   Available,  Bad),        pHH  *        pA1 )] in
>     let tfres = mkSimpleProb
>                 [((weaken e, Low,  Unavailable,  Bad), (one - pHH) * (one - pA1)),
>                  ((    FS e, High, Unavailable,  Bad),        pHH  * (one - pA1)),
>                  ((weaken e, Low,    Available,  Bad), (one - pHH) *        pA1 ),
>                  ((    FS e, High,   Available,  Bad),        pHH  *        pA1 )] in
>     let ftres = mkSimpleProb
>                 [((weaken e, Low,  Unavailable,  Bad), (one - pHH) * (one - pA2)),
>                  ((    FS e, High, Unavailable,  Bad),        pHH  * (one - pA2)),
>                  ((weaken e, Low,    Available,  Bad), (one - pHH) *        pA2 ),
>                  ((    FS e, High,   Available,  Bad),        pHH  *        pA2 )] in
>     let ffres = mkSimpleProb
>                 [((weaken e, Low,  Unavailable,  Bad), (one - pHH) * (one - pA2)),
>                  ((    FS e, High, Unavailable,  Bad),        pHH  * (one - pA2)),
>                  ((weaken e, Low,    Available,  Bad), (one - pHH) *        pA2 ),
>                  ((    FS e, High,   Available,  Bad),        pHH  *        pA2 )] in
>     case (t <= crN) of
>       True  =>   case (fromFin e <= crE) of
>                  True  =>   trim ttres
>                  False =>   trim tfres
>       False =>   case (fromFin e <= crE) of
>                  True  =>   trim ftres
>                  False =>   trim ffres
>
>
>   -- The transition function: high emissions, available GHG technologies
>
>   -- The transition function: high emissions, available GHG technologies, good world
>   SequentialDecisionProblems.CoreTheory.nexts t (e, High, Available, Good) Low =
>     let ttres = mkSimpleProb
>                 [((weaken e, Low,    Available, Good),        pLH  *        pS1),
>                  ((    FS e, High,   Available, Good), (one - pLH) *        pS1),
>                  ((weaken e, Low,    Available,  Bad),        pLH  * (one - pS1)),
>                  ((    FS e, High,   Available,  Bad), (one - pLH) * (one - pS1))] in
>     let tfres = mkSimpleProb
>                 [((weaken e, Low,    Available, Good),        pLH  *        pS2),
>                  ((    FS e, High,   Available, Good), (one - pLH) *        pS2),
>                  ((weaken e, Low,    Available,  Bad),        pLH  * (one - pS2)),
>                  ((    FS e, High,   Available,  Bad), (one - pLH) * (one - pS2))] in
>     let ftres = mkSimpleProb
>                 [((weaken e, Low,    Available, Good),        pLH  *        pS1),
>                  ((    FS e, High,   Available, Good), (one - pLH) *        pS1),
>                  ((weaken e, Low,    Available,  Bad),        pLH  * (one - pS1)),
>                  ((    FS e, High,   Available,  Bad), (one - pLH) * (one - pS1))] in
>     let ffres = mkSimpleProb
>                 [((weaken e, Low,    Available, Good),        pLH  *        pS2),
>                  ((    FS e, High,   Available, Good), (one - pLH) *        pS2),
>                  ((weaken e, Low,    Available,  Bad),        pLH  * (one - pS2)),
>                  ((    FS e, High,   Available,  Bad), (one - pLH) * (one - pS2))] in
>     case (t <= crN) of
>       True  =>   case (fromFin e <= crE) of
>                  True  =>   trim ttres
>                  False =>   trim tfres
>       False =>   case (fromFin e <= crE) of
>                  True  =>   trim ftres
>                  False =>   trim ffres
>   SequentialDecisionProblems.CoreTheory.nexts t (e, High, Available, Good) High =
>     let ttres = mkSimpleProb
>                 [((weaken e, Low,    Available, Good), (one - pHH) *        pS1),
>                  ((    FS e, High,   Available, Good),        pHH  *        pS1),
>                  ((weaken e, Low,    Available,  Bad), (one - pHH) * (one - pS1)),
>                  ((    FS e, High,   Available,  Bad),        pHH  * (one - pS1))] in
>     let tfres = mkSimpleProb
>                 [((weaken e, Low,    Available, Good), (one - pHH) *        pS2),
>                  ((    FS e, High,   Available, Good),        pHH  *        pS2),
>                  ((weaken e, Low,    Available,  Bad), (one - pHH) * (one - pS2)),
>                  ((    FS e, High,   Available,  Bad),        pHH  * (one - pS2))] in
>     let ftres = mkSimpleProb
>                 [((weaken e, Low,    Available, Good), (one - pHH) *        pS1),
>                  ((    FS e, High,   Available, Good),        pHH  *        pS1),
>                  ((weaken e, Low,    Available,  Bad), (one - pHH) * (one - pS1)),
>                  ((    FS e, High,   Available,  Bad),        pHH  * (one - pS1))] in
>     let ffres = mkSimpleProb
>                 [((weaken e, Low,    Available, Good), (one - pHH) *        pS2),
>                  ((    FS e, High,   Available, Good),        pHH  *        pS2),
>                  ((weaken e, Low,    Available,  Bad), (one - pHH) * (one - pS2)),
>                  ((    FS e, High,   Available,  Bad),        pHH  * (one - pS2))] in
>     case (t <= crN) of
>       True  =>   case (fromFin e <= crE) of
>                  True  =>   trim ttres
>                  False =>   trim tfres
>       False =>   case (fromFin e <= crE) of
>                  True  =>   trim ftres
>                  False =>   trim ffres
>
>   -- The transition function: high emissions, available GHG technologies, bad world
>   SequentialDecisionProblems.CoreTheory.nexts t (e, High, Available, Bad) Low =
>     let ttres = mkSimpleProb
>                 [((weaken e, Low,    Available,  Bad),        pLH ),
>                  ((    FS e, High,   Available,  Bad), (one - pLH))] in
>     let tfres = mkSimpleProb
>                 [((weaken e, Low,    Available,  Bad),        pLH ),
>                  ((    FS e, High,   Available,  Bad), (one - pLH))] in
>     let ftres = mkSimpleProb
>                 [((weaken e, Low,    Available,  Bad),        pLH ),
>                  ((    FS e, High,   Available,  Bad), (one - pLH))] in
>     let ffres = mkSimpleProb
>                 [((weaken e, Low,    Available,  Bad),        pLH ),
>                  ((    FS e, High,   Available,  Bad), (one - pLH))] in
>     case (t <= crN) of
>       True  =>   case (fromFin e <= crE) of
>                  True  =>   trim ttres
>                  False =>   trim tfres
>       False =>   case (fromFin e <= crE) of
>                  True  =>   trim ftres
>                  False =>   trim ffres
>   SequentialDecisionProblems.CoreTheory.nexts t (e, High, Available, Bad) High =
>     let ttres = mkSimpleProb
>                 [((weaken e, Low,    Available,  Bad), (one - pHH)),
>                  ((    FS e, High,   Available,  Bad),        pHH )] in
>     let tfres = mkSimpleProb
>                 [((weaken e, Low,    Available,  Bad), (one - pHH)),
>                  ((    FS e, High,   Available,  Bad),        pHH )] in
>     let ftres = mkSimpleProb
>                 [((weaken e, Low,    Available,  Bad), (one - pHH)),
>                  ((    FS e, High,   Available,  Bad),        pHH )] in
>     let ffres = mkSimpleProb
>                 [((weaken e, Low,    Available,  Bad), (one - pHH)),
>                  ((    FS e, High,   Available,  Bad),        pHH )] in
>     case (t <= crN) of
>       True  =>   case (fromFin e <= crE) of
>                  True  =>   trim ttres
>                  False =>   trim tfres
>       False =>   case (fromFin e <= crE) of
>                  True  =>   trim ftres
>                  False =>   trim ffres
>
>
>
>
>   -- The transition function: low emissions
>
>   -- The transition function: low emissions, unavailable GHG technologies
>
>   -- The transition function: low emissions, unavailable GHG technologies, good world
>   SequentialDecisionProblems.CoreTheory.nexts t (e, Low, Unavailable, Good) Low =
>     let ttres = mkSimpleProb
>                 [((weaken e, Low,  Unavailable, Good),        pLL  * (one - pA1) *        pS1),
>                  ((    FS e, High, Unavailable, Good), (one - pLL) * (one - pA1) *        pS1),
>                  ((weaken e, Low,    Available, Good),        pLL  *        pA1  *        pS1),
>                  ((    FS e, High,   Available, Good), (one - pLL) *        pA1  *        pS1),
>                  ((weaken e, Low,  Unavailable,  Bad),        pLL  * (one - pA1) * (one - pS1)),
>                  ((    FS e, High, Unavailable,  Bad), (one - pLL) * (one - pA1) * (one - pS1)),
>                  ((weaken e, Low,    Available,  Bad),        pLL  *        pA1  * (one - pS1)),
>                  ((    FS e, High,   Available,  Bad), (one - pLL) *        pA1  * (one - pS1))] in
>     let tfres = mkSimpleProb
>                 [((weaken e, Low,  Unavailable, Good),        pLL  * (one - pA1) *        pS2),
>                  ((    FS e, High, Unavailable, Good), (one - pLL) * (one - pA1) *        pS2),
>                  ((weaken e, Low,    Available, Good),        pLL  *        pA1  *        pS2),
>                  ((    FS e, High,   Available, Good), (one - pLL) *        pA1  *        pS2),
>                  ((weaken e, Low,  Unavailable,  Bad),        pLL  * (one - pA1) * (one - pS2)),
>                  ((    FS e, High, Unavailable,  Bad), (one - pLL) * (one - pA1) * (one - pS2)),
>                  ((weaken e, Low,    Available,  Bad),        pLL  *        pA1  * (one - pS2)),
>                  ((    FS e, High,   Available,  Bad), (one - pLL) *        pA1  * (one - pS2))] in
>     let ftres = mkSimpleProb
>                 [((weaken e, Low,  Unavailable, Good),        pLL  * (one - pA2) *        pS1),
>                  ((    FS e, High, Unavailable, Good), (one - pLL) * (one - pA2) *        pS1),
>                  ((weaken e, Low,    Available, Good),        pLL  *        pA2  *        pS1),
>                  ((    FS e, High,   Available, Good), (one - pLL) *        pA2  *        pS1),
>                  ((weaken e, Low,  Unavailable,  Bad),        pLL  * (one - pA2) * (one - pS1)),
>                  ((    FS e, High, Unavailable,  Bad), (one - pLL) * (one - pA2) * (one - pS1)),
>                  ((weaken e, Low,    Available,  Bad),        pLL  *        pA2  * (one - pS1)),
>                  ((    FS e, High,   Available,  Bad), (one - pLL) *        pA2  * (one - pS1))] in
>     let ffres = mkSimpleProb
>                 [((weaken e, Low,  Unavailable, Good),        pLL  * (one - pA2) *        pS2),
>                  ((    FS e, High, Unavailable, Good), (one - pLL) * (one - pA2) *        pS2),
>                  ((weaken e, Low,    Available, Good),        pLL  *        pA2  *        pS2),
>                  ((    FS e, High,   Available, Good), (one - pLL) *        pA2  *        pS2),
>                  ((weaken e, Low,  Unavailable,  Bad),        pLL  * (one - pA2) * (one - pS2)),
>                  ((    FS e, High, Unavailable,  Bad), (one - pLL) * (one - pA2) * (one - pS2)),
>                  ((weaken e, Low,    Available,  Bad),        pLL  *        pA2  * (one - pS2)),
>                  ((    FS e, High,   Available,  Bad), (one - pLL) *        pA2  * (one - pS2))] in
>     case (t <= crN) of
>       True  =>   case (fromFin e <= crE) of
>                  True  =>   trim ttres
>                  False =>   trim tfres
>       False =>   case (fromFin e <= crE) of
>                  True  =>   trim ftres
>                  False =>   trim ffres
>   SequentialDecisionProblems.CoreTheory.nexts t (e, Low, Unavailable, Good) High =
>     let ttres = mkSimpleProb
>                 [((weaken e, Low,  Unavailable, Good), (one - pHL) * (one - pA1) *        pS1),
>                  ((    FS e, High, Unavailable, Good),        pHL  * (one - pA1) *        pS1),
>                  ((weaken e, Low,    Available, Good), (one - pHL) *        pA1  *        pS1),
>                  ((    FS e, High,   Available, Good),        pHL  *        pA1  *        pS1),
>                  ((weaken e, Low,  Unavailable,  Bad), (one - pHL) * (one - pA1) * (one - pS1)),
>                  ((    FS e, High, Unavailable,  Bad),        pHL  * (one - pA1) * (one - pS1)),
>                  ((weaken e, Low,    Available,  Bad), (one - pHL) *        pA1  * (one - pS1)),
>                  ((    FS e, High,   Available,  Bad),        pHL  *        pA1  * (one - pS1))] in
>     let tfres = mkSimpleProb
>                 [((weaken e, Low,  Unavailable, Good), (one - pHL) * (one - pA1) *        pS2),
>                  ((    FS e, High, Unavailable, Good),        pHL  * (one - pA1) *        pS2),
>                  ((weaken e, Low,    Available, Good), (one - pHL) *        pA1  *        pS2),
>                  ((    FS e, High,   Available, Good),        pHL  *        pA1  *        pS2),
>                  ((weaken e, Low,  Unavailable,  Bad), (one - pHL) * (one - pA1) * (one - pS2)),
>                  ((    FS e, High, Unavailable,  Bad),        pHL  * (one - pA1) * (one - pS2)),
>                  ((weaken e, Low,    Available,  Bad), (one - pHL) *        pA1  * (one - pS2)),
>                  ((    FS e, High,   Available,  Bad),        pHL  *        pA1  * (one - pS2))] in
>     let ftres = mkSimpleProb
>                 [((weaken e, Low,  Unavailable, Good), (one - pHL) * (one - pA2) *        pS1),
>                  ((    FS e, High, Unavailable, Good),        pHL  * (one - pA2) *        pS1),
>                  ((weaken e, Low,    Available, Good), (one - pHL) *        pA2  *        pS1),
>                  ((    FS e, High,   Available, Good),        pHL  *        pA2  *        pS1),
>                  ((weaken e, Low,  Unavailable,  Bad), (one - pHL) * (one - pA2) * (one - pS1)),
>                  ((    FS e, High, Unavailable,  Bad),        pHL  * (one - pA2) * (one - pS1)),
>                  ((weaken e, Low,    Available,  Bad), (one - pHL) *        pA2  * (one - pS1)),
>                  ((    FS e, High,   Available,  Bad),        pHL  *        pA2  * (one - pS1))] in
>     let ffres = mkSimpleProb
>                 [((weaken e, Low,  Unavailable, Good), (one - pHL) * (one - pA2) *        pS2),
>                  ((    FS e, High, Unavailable, Good),        pHL  * (one - pA2) *        pS2),
>                  ((weaken e, Low,    Available, Good), (one - pHL) *        pA2  *        pS2),
>                  ((    FS e, High,   Available, Good),        pHL  *        pA2  *        pS2),
>                  ((weaken e, Low,  Unavailable,  Bad), (one - pHL) * (one - pA2) * (one - pS2)),
>                  ((    FS e, High, Unavailable,  Bad),        pHL  * (one - pA2) * (one - pS2)),
>                  ((weaken e, Low,    Available,  Bad), (one - pHL) *        pA2  * (one - pS2)),
>                  ((    FS e, High,   Available,  Bad),        pHL  *        pA2  * (one - pS2))] in
>     case (t <= crN) of
>       True  =>   case (fromFin e <= crE) of
>                  True  =>   trim ttres
>                  False =>   trim tfres
>       False =>   case (fromFin e <= crE) of
>                  True  =>   trim ftres
>                  False =>   trim ffres
>
>   -- The transition function: low emissions, unavailable GHG technologies, bad world
>   SequentialDecisionProblems.CoreTheory.nexts t (e, Low, Unavailable, Bad) Low =
>     let ttres = mkSimpleProb
>                 [((weaken e, Low,  Unavailable,  Bad),        pLL  * (one - pA1)),
>                  ((    FS e, High, Unavailable,  Bad), (one - pLL) * (one - pA1)),
>                  ((weaken e, Low,    Available,  Bad),        pLL  *        pA1 ),
>                  ((    FS e, High,   Available,  Bad), (one - pLL) *        pA1 )] in
>     let tfres = mkSimpleProb
>                 [((weaken e, Low,  Unavailable,  Bad),        pLL  * (one - pA1)),
>                  ((    FS e, High, Unavailable,  Bad), (one - pLL) * (one - pA1)),
>                  ((weaken e, Low,    Available,  Bad),        pLL  *        pA1 ),
>                  ((    FS e, High,   Available,  Bad), (one - pLL) *        pA1 )] in
>     let ftres = mkSimpleProb
>                 [((weaken e, Low,  Unavailable,  Bad),        pLL  * (one - pA2)),
>                  ((    FS e, High, Unavailable,  Bad), (one - pLL) * (one - pA2)),
>                  ((weaken e, Low,    Available,  Bad),        pLL  *        pA2 ),
>                  ((    FS e, High,   Available,  Bad), (one - pLL) *        pA2 )] in
>     let ffres = mkSimpleProb
>                 [((weaken e, Low,  Unavailable,  Bad),        pLL  * (one - pA2)),
>                  ((    FS e, High, Unavailable,  Bad), (one - pLL) * (one - pA2)),
>                  ((weaken e, Low,    Available,  Bad),        pLL  *        pA2 ),
>                  ((    FS e, High,   Available,  Bad), (one - pLL) *        pA2 )] in
>     case (t <= crN) of
>       True  =>   case (fromFin e <= crE) of
>                  True  =>   trim ttres
>                  False =>   trim tfres
>       False =>   case (fromFin e <= crE) of
>                  True  =>   trim ftres
>                  False =>   trim ffres
>   SequentialDecisionProblems.CoreTheory.nexts t (e, Low, Unavailable, Bad) High =
>     let ttres = mkSimpleProb
>                 [((weaken e, Low,  Unavailable,  Bad), (one - pHL) * (one - pA1)),
>                  ((    FS e, High, Unavailable,  Bad),        pHL  * (one - pA1)),
>                  ((weaken e, Low,    Available,  Bad), (one - pHL) *        pA1 ),
>                  ((    FS e, High,   Available,  Bad),        pHL  *        pA1 )] in
>     let tfres = mkSimpleProb
>                 [((weaken e, Low,  Unavailable,  Bad), (one - pHL) * (one - pA1)),
>                  ((    FS e, High, Unavailable,  Bad),        pHL  * (one - pA1)),
>                  ((weaken e, Low,    Available,  Bad), (one - pHL) *        pA1 ),
>                  ((    FS e, High,   Available,  Bad),        pHL  *        pA1 )] in
>     let ftres = mkSimpleProb
>                 [((weaken e, Low,  Unavailable,  Bad), (one - pHL) * (one - pA2)),
>                  ((    FS e, High, Unavailable,  Bad),        pHL  * (one - pA2)),
>                  ((weaken e, Low,    Available,  Bad), (one - pHL) *        pA2 ),
>                  ((    FS e, High,   Available,  Bad),        pHL  *        pA2 )] in
>     let ffres = mkSimpleProb
>                 [((weaken e, Low,  Unavailable,  Bad), (one - pHL) * (one - pA2)),
>                  ((    FS e, High, Unavailable,  Bad),        pHL  * (one - pA2)),
>                  ((weaken e, Low,    Available,  Bad), (one - pHL) *        pA2 ),
>                  ((    FS e, High,   Available,  Bad),        pHL  *        pA2 )] in
>     case (t <= crN) of
>       True  =>   case (fromFin e <= crE) of
>                  True  =>   trim ttres
>                  False =>   trim tfres
>       False =>   case (fromFin e <= crE) of
>                  True  =>   trim ftres
>                  False =>   trim ffres
>
>
>   -- The transition function: low emissions, available GHG technologies
>
>   -- The transition function: low emissions, available GHG technologies, good world
>   SequentialDecisionProblems.CoreTheory.nexts t (e, Low, Available, Good) Low =
>     let ttres = mkSimpleProb
>                 [((weaken e, Low,    Available, Good),        pLL  *        pS1),
>                  ((    FS e, High,   Available, Good), (one - pLL) *        pS1),
>                  ((weaken e, Low,    Available,  Bad),        pLL  * (one - pS1)),
>                  ((    FS e, High,   Available,  Bad), (one - pLL) * (one - pS1))] in
>     let tfres = mkSimpleProb
>                 [((weaken e, Low,    Available, Good),        pLL  *        pS2),
>                  ((    FS e, High,   Available, Good), (one - pLL) *        pS2),
>                  ((weaken e, Low,    Available,  Bad),        pLL  * (one - pS2)),
>                  ((    FS e, High,   Available,  Bad), (one - pLL) * (one - pS2))] in
>     let ftres = mkSimpleProb
>                 [((weaken e, Low,    Available, Good),        pLL  *        pS1),
>                  ((    FS e, High,   Available, Good), (one - pLL) *        pS1),
>                  ((weaken e, Low,    Available,  Bad),        pLL  * (one - pS1)),
>                  ((    FS e, High,   Available,  Bad), (one - pLL) * (one - pS1))] in
>     let ffres = mkSimpleProb
>                 [((weaken e, Low,    Available, Good),        pLL  *        pS2),
>                  ((    FS e, High,   Available, Good), (one - pLL) *        pS2),
>                  ((weaken e, Low,    Available,  Bad),        pLL  * (one - pS2)),
>                  ((    FS e, High,   Available,  Bad), (one - pLL) * (one - pS2))] in
>     case (t <= crN) of
>       True  =>   case (fromFin e <= crE) of
>                  True  =>   trim ttres
>                  False =>   trim tfres
>       False =>   case (fromFin e <= crE) of
>                  True  =>   trim ftres
>                  False =>   trim ffres
>   SequentialDecisionProblems.CoreTheory.nexts t (e, Low, Available, Good) High =
>     let ttres = mkSimpleProb
>                 [((weaken e, Low,    Available, Good), (one - pHL) *        pS1),
>                  ((    FS e, High,   Available, Good),        pHL  *        pS1),
>                  ((weaken e, Low,    Available,  Bad), (one - pHL) * (one - pS1)),
>                  ((    FS e, High,   Available,  Bad),        pHL  * (one - pS1))] in
>     let tfres = mkSimpleProb
>                 [((weaken e, Low,    Available, Good), (one - pHL) *        pS2),
>                  ((    FS e, High,   Available, Good),        pHL  *        pS2),
>                  ((weaken e, Low,    Available,  Bad), (one - pHL) * (one - pS2)),
>                  ((    FS e, High,   Available,  Bad),        pHL  * (one - pS2))] in
>     let ftres = mkSimpleProb
>                 [((weaken e, Low,    Available, Good), (one - pHL) *        pS1),
>                  ((    FS e, High,   Available, Good),        pHL  *        pS1),
>                  ((weaken e, Low,    Available,  Bad), (one - pHL) * (one - pS1)),
>                  ((    FS e, High,   Available,  Bad),        pHL  * (one - pS1))] in
>     let ffres = mkSimpleProb
>                 [((weaken e, Low,    Available, Good), (one - pHL) *        pS2),
>                  ((    FS e, High,   Available, Good),        pHL  *        pS2),
>                  ((weaken e, Low,    Available,  Bad), (one - pHL) * (one - pS2)),
>                  ((    FS e, High,   Available,  Bad),        pHL  * (one - pS2))] in
>     case (t <= crN) of
>       True  =>   case (fromFin e <= crE) of
>                  True  =>   trim ttres
>                  False =>   trim tfres
>       False =>   case (fromFin e <= crE) of
>                  True  =>   trim ftres
>                  False =>   trim ffres
>
>   -- The transition function: low emissions, available GHG technologies, bad world
>   SequentialDecisionProblems.CoreTheory.nexts t (e, Low, Available, Bad) Low =
>     let ttres = mkSimpleProb
>                 [((weaken e, Low,    Available,  Bad),        pLL ),
>                  ((    FS e, High,   Available,  Bad), (one - pLL))] in
>     let tfres = mkSimpleProb
>                 [((weaken e, Low,    Available,  Bad),        pLL ),
>                  ((    FS e, High,   Available,  Bad), (one - pLL))] in
>     let ftres = mkSimpleProb
>                 [((weaken e, Low,    Available,  Bad),        pLL ),
>                  ((    FS e, High,   Available,  Bad), (one - pLL))] in
>     let ffres = mkSimpleProb
>                 [((weaken e, Low,    Available,  Bad),        pLL ),
>                  ((    FS e, High,   Available,  Bad), (one - pLL))] in
>     case (t <= crN) of
>       True  =>   case (fromFin e <= crE) of
>                  True  =>   trim ttres
>                  False =>   trim tfres
>       False =>   case (fromFin e <= crE) of
>                  True  =>   trim ftres
>                  False =>   trim ffres
>   SequentialDecisionProblems.CoreTheory.nexts t (e, Low, Available, Bad) High =
>     let ttres = mkSimpleProb
>                 [((weaken e, Low,    Available,  Bad), (one - pHL)),
>                  ((    FS e, High,   Available,  Bad),        pHL )] in
>     let tfres = mkSimpleProb
>                 [((weaken e, Low,    Available,  Bad), (one - pHL)),
>                  ((    FS e, High,   Available,  Bad),        pHL )] in
>     let ftres = mkSimpleProb
>                 [((weaken e, Low,    Available,  Bad), (one - pHL)),
>                  ((    FS e, High,   Available,  Bad),        pHL )] in
>     let ffres = mkSimpleProb
>                 [((weaken e, Low,    Available,  Bad), (one - pHL)),
>                  ((    FS e, High,   Available,  Bad),        pHL )] in
>     case (t <= crN) of
>       True  =>   case (fromFin e <= crE) of
>                  True  =>   trim ttres
>                  False =>   trim tfres
>       False =>   case (fromFin e <= crE) of
>                  True  =>   trim ftres
>                  False =>   trim ffres

* |Val| and |LTE|:

> SequentialDecisionProblems.CoreTheory.Val =
>   NonNegDouble.NonNegDouble

> SequentialDecisionProblems.CoreTheory.plus =
>   NonNegDouble.Operations.plus

> SequentialDecisionProblems.CoreTheory.zero =
>   fromInteger @{NumNonNegDouble} 0

> SequentialDecisionProblems.CoreTheory.LTE =
>   NonNegDouble.Predicates.LTE

> SequentialDecisionProblems.FullTheory.reflexiveLTE =
>   NonNegDouble.LTEProperties.reflexiveLTE

> SequentialDecisionProblems.FullTheory.transitiveLTE =
>   NonNegDouble.LTEProperties.transitiveLTE

> SequentialDecisionProblems.FullTheory.monotonePlusLTE =
>   NonNegDouble.LTEProperties.monotonePlusLTE

> SequentialDecisionProblems.CoreTheoryOptDefaults.totalPreorderLTE =
>   NonNegDouble.LTEProperties.totalPreorderLTE

* Reward function

The idea is that being in a good world yields one unit of benefits per
step and being in a bad world yield less benefits:

> -- Ratio of the benefits in a bad world and the benefits in a good world
> badOverGood : NonNegDouble
> badOverGood = cast 0.89 -- cast 0.89 -- cast 0.5

> -- Sanity check
> badOverGoodLTEone : badOverGood `NonNegDouble.Predicates.LTE` one
> badOverGoodLTEone = MkLTE Oh

Emitting GHGs also brings benefits. These are a fraction of the step
benefits in a good world and low emissions bring less benefits than high
emissions:

> -- Ratio between low emissions and step benefits in good world, when
> -- effective technologies for reducing GHG emissions are unavailable
> lowOverGoodUnavailable : NonNegDouble
> lowOverGoodUnavailable = cast 0.1 -- cast 0.0 -- cast 0.1

> -- Ratio between low emissions and step benefits in good world, when
> -- effective technologies for reducing GHG emissions are available
> lowOverGoodAvailable : NonNegDouble
> lowOverGoodAvailable = cast 0.2 -- cast 0.1 -- cast 0.2

> -- Ratio between high emissions and step benefits in a good world
> highOverGood : NonNegDouble
> highOverGood = cast 0.3

> -- Sanity check
> lowOverGoodUnavailableLTEone : lowOverGoodUnavailable `NonNegDouble.Predicates.LTE` one
> lowOverGoodUnavailableLTEone = MkLTE Oh

> -- Sanity check
> lowOverGoodAvailableLTEone : lowOverGoodAvailable `NonNegDouble.Predicates.LTE` one
> lowOverGoodAvailableLTEone = MkLTE Oh

> -- Sanity check
> lowOverGoodUnavailableLTElowOverGoodAvailable : lowOverGoodUnavailable `NonNegDouble.Predicates.LTE` lowOverGoodAvailable
> lowOverGoodUnavailableLTElowOverGoodAvailable = MkLTE Oh

> -- Sanity check
> highOverGoodLTEone : highOverGood `NonNegDouble.Predicates.LTE` one
> highOverGoodLTEone = MkLTE Oh

> -- Sanity check
> lowLTEhigh : lowOverGoodAvailable `NonNegDouble.Predicates.LTE` highOverGood
> lowLTEhigh = MkLTE Oh

The reward only depend on the next state, not on the current state or on
the selected control:

> -- Reward function:
>
> using implementation NumNonNegDouble
>
>   SequentialDecisionProblems.CoreTheory.reward _ _ _ (e, High, Unavailable, Good) =
>     one               + one * highOverGood
>   SequentialDecisionProblems.CoreTheory.reward _ _ _ (e, High, Unavailable,  Bad) =
>     one * badOverGood + one * highOverGood
>
>   SequentialDecisionProblems.CoreTheory.reward _ _ _ (e, High,   Available, Good) =
>     one               + one * highOverGood
>   SequentialDecisionProblems.CoreTheory.reward _ _ _ (e, High,   Available,  Bad) =
>     one * badOverGood + one * highOverGood
>
>   SequentialDecisionProblems.CoreTheory.reward _ _ _ (e,  Low, Unavailable, Good) =
>     one               + one * lowOverGoodUnavailable
>   SequentialDecisionProblems.CoreTheory.reward _ _ _ (e,  Low, Unavailable,  Bad) =
>     one * badOverGood + one * lowOverGoodUnavailable
>
>   SequentialDecisionProblems.CoreTheory.reward _ _ _ (e,  Low,   Available, Good) =
>     one               + one * lowOverGoodAvailable
>   SequentialDecisionProblems.CoreTheory.reward _ _ _ (e,  Low,   Available,  Bad) =
>     one * badOverGood + one * lowOverGoodAvailable

* Completing the problem specification

To be able to apply the verified, generic backwards induction algorithm
of |CoreTheory| to compute optimal policies for our problem, we have to
explain how the decision maker accounts for uncertainties on rewards
induced by uncertainties in the transition function. We first assume
that the decision maker measures uncertain rewards by their expected
value:

> SequentialDecisionProblems.CoreTheory.meas = expectedValue -- worst -- expectedValue
> SequentialDecisionProblems.FullTheory.measMon = monotoneExpectedValue -- monotoneWorst -- monotoneExpectedValue

Further on, we have to implement the notions of viability and
reachability. We start by positing that all states are viable for any
number of steps:

> -- Viable : (n : Nat) -> State t -> Type
> SequentialDecisionProblems.CoreTheory.Viable n x = Unit

From this definition, it trivially follows that all elements of an
arbitrary list of states are viable for an arbitrary number of steps:

> viableLemma : {t, n : Nat} -> (xs : List (State t)) -> All (Viable n) xs
> viableLemma  Nil      = Nil
> viableLemma {t} {n} (x :: xs) = () :: (viableLemma {t} {n} xs)

This fact and the (less trivial) result that simple probability
distributions are never empty, see |nonEmptyLemma| in
|MonadicProperties| in |SimpleProb|, allows us to show that the above
definition of |Viable| fulfills |viableSpec1|:

> -- viableSpec1 : (x : State t) -> Viable (S n) x -> GoodCtrl t x
> SequentialDecisionProblems.CoreTheory.viableSpec1 {t} {n} s v =
>   MkSigma High (ne, av) where
>     ne : SequentialDecisionProblems.CoreTheory.NotEmpty (nexts t s High)
>     ne = nonEmptyLemma (nexts t s High)
>     av : SequentialDecisionProblems.CoreTheory.All (Viable {t = S t} n) (nexts t s High)
>     av = viableLemma {t = S t} (support (nexts t s High))

> SequentialDecisionProblems.Utils.finiteViable n x = finiteUnit

> SequentialDecisionProblems.Utils.decidableViable n x = decidableUnit

For reachability, we proceed in a similar way. We say that all states
are reachable

> -- Reachable : State t' -> Type
> SequentialDecisionProblems.CoreTheory.Reachable x' = Unit

which immediately implies |reachableSpec1|:

> -- reachableSpec1 : (x : State t) -> Reachable {t' = t} x -> (y : Ctrl t x) -> All (Reachable {t' = S t}) (nexts t x y)
> SequentialDecisionProblems.CoreTheory.reachableSpec1 {t} x r y = all (nexts t x y) where
>   all : (sp : SimpleProb  (State (S t))) -> SequentialDecisionProblems.CoreTheory.All (Reachable {t' = S t}) sp
>   all sp = all' (support sp) where
>     all' : (xs : List (State (S t))) -> Data.List.Quantifiers.All (Reachable {t' = S t}) xs
>     all' Nil = Nil
>     all' (x :: xs) = () :: (all' xs)

and decidability of |Reachable|:

> SequentialDecisionProblems.TabBackwardsInduction1.decidableReachable x = decidableUnit

Finally, we have to show that controls are finite

> -- finiteCtrl : {t : Nat} -> (x : State t) -> Finite (Ctrl t x)
> SequentialDecisionProblems.Utils.finiteCtrl _ = finiteLowHigh

and, in order to use the fast, tail-recursive tabulated version of
backwards induction, that states are finite:

> SequentialDecisionProblems.TabBackwardsInduction1.finiteState t =
>   finiteTuple4 finiteFin finiteLowHigh finiteAvailableUnavailable finiteGoodBad

* Optimal policies, optimal decisions, ...

We can now apply the results of our |CoreTheory| and of the |FullTheory|
to compute verified optimal policies, possible state-control sequences,
etc. To this end, we need to be able to show the outcome of the decision
process. This means implemeting functions to print states and controls:

> -- showState : {t : Nat} -> State t -> String
> SequentialDecisionProblems.Utils.showState {t} (e, High, Unavailable, Good) =
>   "(" ++ show (finToNat e) ++ ",H,U,G)"
> SequentialDecisionProblems.Utils.showState {t} (e, High, Unavailable,  Bad) =
>   "(" ++ show (finToNat e) ++ ",H,U,B)"
> SequentialDecisionProblems.Utils.showState {t} (e, High,   Available, Good) =
>   "(" ++ show (finToNat e) ++ ",H,A,G)"
> SequentialDecisionProblems.Utils.showState {t} (e, High,   Available,  Bad) =
>   "(" ++ show (finToNat e) ++ ",H,A,B)"
> SequentialDecisionProblems.Utils.showState {t} (e,  Low, Unavailable, Good) =
>   "(" ++ show (finToNat e) ++ ",L,U,G)"
> SequentialDecisionProblems.Utils.showState {t} (e,  Low, Unavailable,  Bad) =
>   "(" ++ show (finToNat e) ++ ",L,U,B)"
> SequentialDecisionProblems.Utils.showState {t} (e,  Low,   Available, Good) =
>   "(" ++ show (finToNat e) ++ ",L,A,G)"
> SequentialDecisionProblems.Utils.showState {t} (e,  Low,   Available,  Bad) =
>   "(" ++ show (finToNat e) ++ ",L,A,B)"

> -- showControl : {t : Nat} -> {x : State t} -> Ctrl t x -> String
> SequentialDecisionProblems.Utils.showCtrl {t} {x}  Low = "L"
> SequentialDecisionProblems.Utils.showCtrl {t} {x} High = "H"

> -- ad-hoc trajectories computation
> adHocPossibleStateCtrlSeqs : {t, n : Nat} ->
>                              (ps : PolicySeq t n) ->
>                              (x : State t) ->
>                              SimpleProb (StateCtrlSeq t n)
> adHocPossibleStateCtrlSeqs {t} {n = Z}         Nil  x =
>   FastSimpleProb.MonadicOperations.ret (Nil x)
> adHocPossibleStateCtrlSeqs {t} {n = S m} (p :: ps') x =
> {-
>   FastSimpleProb.MonadicOperations.fmap ((MkSigma x y) ::) (FastSimpleProb.MonadicOperations.naivebind mx' f) where
>     y   :  Ctrl t x
>     y   =  ctrl (p x () ())
>     mx' :  SimpleProb (State (S t))
>     mx' =  nexts t x y
>     f   :  State (S t) -> M (StateCtrlSeq (S t) m)
>     f   =  adHocPossibleStateCtrlSeqs {n = m} ps'
> ---}
> --{-
>   let y   =  ctrl (p x () ()) in
>   let mx' =  nexts t x y in
>   let f   =  adHocPossibleStateCtrlSeqs {n = m} ps' in
>   FastSimpleProb.MonadicOperations.fmap ((MkSigma x y) ::) (FastSimpleProb.MonadicOperations.naivebind mx' f)
> ---}

> -- ad-hoc trajectories computation
> %freeze cardReachableAndViableState
> adHocPossibleStateCtrlSeqs1 : {t, n : Nat} ->
>                               (pts : PolicyTableSeq t n) ->
>                               (x : State t) ->
>                               SimpleProb (StateCtrlSeq t n)
> adHocPossibleStateCtrlSeqs1 {t} {n = Z}         Nil  x =
>   FastSimpleProb.MonadicOperations.ret (Nil x)
> {-
> adHocPossibleStateCtrlSeqs1 {t} {n = S m} (pt :: pts') x =
>   FastSimpleProb.MonadicOperations.fmap ((MkSigma x y) ::) (FastSimpleProb.MonadicOperations.naivebind mx' f) where
>     gy  :  GoodCtrl t x m
>     gy  =  goodCtrl x () () pt
>     y   :  Ctrl t x
>     y   =  ctrl gy
>     mx' :  SimpleProb (State (S t))
>     mx' =  nexts t x y
>     f   :  State (S t) -> M (StateCtrlSeq (S t) m)
>     f   =  adHocPossibleStateCtrlSeqs1 {n = m} pts'
> -}
> adHocPossibleStateCtrlSeqs1 {t} {n = S m} (pt :: pts') x =
>   let y   =  ctrl (goodCtrl x () () pt) in
>   let mx' =  nexts t x y in
>   let f   =  adHocPossibleStateCtrlSeqs1 {n = m} pts' in
>   FastSimpleProb.MonadicOperations.fmap ((MkSigma x y) ::) (FastSimpleProb.MonadicOperations.naivebind mx' f)

> constHigh : (t : Nat) -> (n : Nat) -> PolicySeq t n
> constHigh t  Z    = Nil
> constHigh t (S n) = p :: (constHigh (S t) n) where
>   p : Policy t (S n)
>   p x r v = MkSigma High (ne, av) where
>     ne : SequentialDecisionProblems.CoreTheory.NotEmpty (nexts t x High)
>     ne = nonEmptyLemma (nexts t x High)
>     av : SequentialDecisionProblems.CoreTheory.All (Viable {t = S t} n) (nexts t x High)
>     av = viableLemma {t = S t} (support (nexts t x High))

> ||| Constant low policy sequences
> constLow : (t : Nat) -> (n : Nat) -> PolicySeq t n
> constLow t  Z    = Nil
> constLow t (S n) = p :: (constLow (S t) n) where
>   p : Policy t (S n)
>   p x r v = MkSigma Low (ne, av) where
>     ne : SequentialDecisionProblems.CoreTheory.NotEmpty (nexts t x Low)
>     ne = nonEmptyLemma (nexts t x Low)
>     av : SequentialDecisionProblems.CoreTheory.All (Viable {t = S t} n) (nexts t x Low)
>     av = viableLemma {t = S t} (support (nexts t x Low))

>
> using implementation ShowNonNegDouble
>
>   computation : { [STDIO] } Eff ()
>   computation =
>     do putStr ("enter number of steps:\n")
>        nSteps <- getNat
>        putStrLn "nSteps (number of decision steps):"
>        putStrLn ("  " ++ show nSteps)
>
>        putStrLn "crE (crit. cumulated emissions threshold):"
>        putStrLn ("  " ++ show crE)
>        putStrLn "crN (crit. number of decision steps):"
>        putStrLn ("  " ++ show crN)
>
>        putStrLn "pS1 (prob. of staying in a good world, cumulated emissions below crE):"
>        putStrLn ("  " ++ show pS1)
>        putStrLn "pS2 (prob. of staying in a good world, cumulated emissions above crE):"
>        putStrLn ("  " ++ show pS2)
>
>        putStrLn "pA1 (prob. of eff. tech. becoming available, number of steps below crN):"
>        putStrLn ("  " ++ show pA1)
>        putStrLn "pA2 (prob. of eff. tech. becoming available, number of steps above crN):"
>        putStrLn ("  " ++ show pA2)
>
>        putStrLn "pLL (prob. of low emission policies, emissions low, low selected):"
>        putStrLn ("  " ++ show pLL)
>        putStrLn "pLH (prob. of low emission policies, emissions high, low selected):"
>        putStrLn ("  " ++ show pLH)
>        putStrLn "pHL (prob. of high emission policies, emissions low, high selected):"
>        putStrLn ("  " ++ show pHL)
>        putStrLn "pHH (prob. of high emission policies, emissions high, high selected):"
>        putStrLn ("  " ++ show pHH)
>
>        putStrLn "badOverGood (step benefits ratio: bad over good world):"
>        putStrLn ("  " ++ show badOverGood)
>        putStrLn "lowOverGoodUnavailable (benefits ratio: low emissions over step, good world, eff. tech. unavailable):"
>        putStrLn ("  " ++ show lowOverGoodUnavailable)
>        putStrLn "lowOverGoodAvailable (benefits ratio: low emissions over step, good world, eff. tech. available):"
>        putStrLn ("  " ++ show lowOverGoodAvailable)
>        putStrLn "highOverGood (benefits ratio: High emissions over step, good world):"
>        putStrLn ("  " ++ show highOverGood)
>
>        putStrLn "computing constHigh policies ..."
>        constHigh_ps <- pure (constHigh Z nSteps)
>
>        putStrLn "computing constHigh state-control sequences ..."
>        constHigh_mxys <- pure (adHocPossibleStateCtrlSeqs constHigh_ps (FZ, High, Unavailable, Good))
>        putStrLn "pairing constHigh state-control sequences with their values ..."
>        constHigh_mxysv <- pure (possibleStateCtrlSeqsRewards' constHigh_mxys)
>        -- putStrLn "constHigh state-control sequences and their values:"
>        -- putStrLn (showlong constHigh_mxysv)
>
>        putStrLn "computing (naively) the number of constHigh state-control sequences ..."
>        constHigh_n <- pure (length (toList constHigh_mxysv))
>        putStrLn "number of constHigh state-control sequences:"
>        putStrLn ("  " ++ show constHigh_n)
>
>        putStrLn "computing (naively) the most probable constHigh state-control sequence ..."
>        constHigh_xysv <- pure (naiveMostProbableProb constHigh_mxysv)
>        putStrLn "most probable constHigh state-control sequence and its probability:"
>        putStrLn ("  " ++ show constHigh_xysv)
>
>        putStrLn "sorting (naively) the constHigh state-control sequence ..."
>        constHigh_xysvs <- pure (naiveSortToList constHigh_mxysv)
>        putStrLn "most probable constHigh state-control sequences (first 3) and their probabilities:"
>        putStrLn (showlong (take 3 constHigh_xysvs))
>
>        putStrLn "measure of constHigh rewards:"
>        putStrLn ("  " ++ show (meas (SequentialDecisionProblems.CoreTheory.fmap snd constHigh_mxysv)))
>
>        putStrLn "computing constLow policies ..."
>        constLow_ps <- pure (constLow Z nSteps)
>
>        putStrLn "computing constLow state-control sequences ..."
>        constLow_mxys <- pure (adHocPossibleStateCtrlSeqs constLow_ps (FZ, High, Unavailable, Good))
>        putStrLn "pairing constLow state-control sequences with their values ..."
>        constLow_mxysv <- pure (possibleStateCtrlSeqsRewards' constLow_mxys)
>
>        putStrLn "computing (naively) the number of constLow state-control sequences ..."
>        constLow_n <- pure (length (toList constLow_mxysv))
>        putStrLn "number of constLow state-control sequences:"
>        putStrLn ("  " ++ show constLow_n)
>
>        putStrLn "computing (naively) the most probable constLow state-control sequence ..."
>        constLow_xysv <- pure (naiveMostProbableProb constLow_mxysv)
>        putStrLn "most probable constLow state-control sequence and its probability:"
>        putStrLn ("  " ++ show constLow_xysv)
>
>        putStrLn "sorting (naively) the constLow state-control sequence ..."
>        constLow_xysvs <- pure (naiveSortToList constLow_mxysv)
>        putStrLn "most probable constLow state-control sequences (first 3) and their probabilities:"
>        putStrLn (showlong (take 3 constLow_xysvs))
>
>        putStrLn "measure of constLow rewards:"
>        putStrLn ("  " ++ show (meas (SequentialDecisionProblems.CoreTheory.fmap snd constLow_mxysv)))
>
>        putStrLn "computing optimal policies ..."
>        ps <- pure (tabTailRecursiveBackwardsInduction1 Z nSteps)
>
>        putStrLn "computing possible state-control sequences ..."
>        mxys <- pure (adHocPossibleStateCtrlSeqs1 ps (FZ, High, Unavailable, Good))
>        putStrLn "pairing possible state-control sequences with their values ..."
>        mxysv <- pure (possibleStateCtrlSeqsRewards' mxys)
>        -- putStrLn "possible state-control sequences and their values:"
>        -- putStrLn (showlong mxysv)
>
>        putStrLn "computing (naively) the number of possible state-control sequences ..."
>        n <- pure (length (toList mxysv))
>        putStrLn "number of possible state-control sequences:"
>        putStrLn ("  " ++ show n)
>
>        putStrLn "computing (naively) the most probable state-control sequence ..."
>        xysv <- pure (naiveMostProbableProb mxysv)
>        putStrLn "most probable state-control sequence and its probability:"
>        putStrLn ("  " ++ show xysv)
>
>        putStrLn "sorting (naively) the possible state-control sequence ..."
>        xysvs <- pure (naiveSortToList mxysv)
>        putStrLn "most probable state-control sequences (first 3) and their probabilities:"
>        putStrLn (showlong (take 3 xysvs))
>
>        putStrLn "measure of possible rewards:"
>        putStrLn ("  " ++ show (meas (SequentialDecisionProblems.CoreTheory.fmap snd mxysv)))

>        putStrLn "done!"

> main : IO ()
> main = run computation

> {-

> ---}

-- Local Variables:
-- idris-packages: ("effects")
-- End:

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
import Data.Vect

MkBig : Nat -> Type
MkBig Z = Int
MkBig (S k) = ((n ** Vect n Int), MkBig k)

bigEx : (n : Nat) -> MkBig n
bigEx Z = 94
bigEx (S k) = ((2 ** [0,0]), bigEx k)

data VWrap : Type -> Type where
     MkVWrap : (0 n : Nat) -> Vect n a -> VWrap a

export
MkBig' : Nat -> Type
MkBig' Z = Int
MkBig' (S k) = (VWrap Int, MkBig' k)

namespace Foo
  public
  export
  bigEx' : (n : Nat) -> MkBig' n
  bigEx' Z = 94
  bigEx' (S k) = (MkVWrap 1 [0], bigEx' k)

eqBigs : bigEx 1000000 = bigEx 1000000
eqBigs = Refl

eqBigs' : bigEx' 800000 = bigEx' 800000
eqBigs' = Refl

ext: idr


text:
module Cordial.Model.Interface.PortGroup

import Data.Vect
import Data.DList
import Data.Ranged

import Text.Markup.Edda

import Cordial.Model.Common
import Cordial.Model.Specification
import Cordial.Model.Projection

import Cordial.Model.Interface.Kinds
import Cordial.Model.Interface.Ports

%default total
%access public export

{- [ NOTE ]

We take note, at the type level, if the port is required or not. We
use this information with `PortGroup` below to describe thinnings.

With Port notice how we constrain the value level values using type
level values. This is core principle behind how we type check our
ports/interfaces against an abstract definition. We first project the
definition based on the kind of interface, and use that projection in
the type to source values.

-}

||| A collection of ports that respects the projected port group.
|||
||| Universe that logical names arise from.
||| Are we producing/consuming information.
||| The originating projected port type that constrains the value level values.
|||
data PortGroup : (annot    : Type)
              -> (labelTy  : Type)
              -> (endpoint : Endpoint)
              -> (endian   : Maybe Endian)
              -> (ps       : PortGroupTy annot labelTy)
              -> (pportTys : DList (PortTy annot labelTy) (ProjectedPortTy labelTy endpoint) ps)
              -> Type
  where
    ||| No ports
    Empty : PortGroup annot labelTy endpoint endian Nil Nil

    ||| Add a port to the group such that the description comes from
    ||| the projected port list.
    Add  : {type : PortTy annot labelTy}
        -> {projectedType : ProjectedPortTy labelTy endpoint type}
        -> (port : Port annot labelTy type projectedType endpoint endian)

        -> (rest : PortGroup annot labelTy endpoint endian ps pps)
        -> PortGroup annot labelTy endpoint endian (type          :: ps)
                                                   (projectedType :: pps)

    ||| Skip an optional port from the projected port list.
    Skip : (rest : PortGroup annot labelTy endpoint endian ps pps)
        -> (prf  : OptionalProjectedPort type endpoint projectedType)
        -> PortGroup annot labelTy endpoint endian (type :: ps) (projectedType :: pps)

infixr 5 <::>, <::~>

(<::>) : {type : PortTy annot labelTy}
      -> {projectedType : ProjectedPortTy labelTy endpoint type}
      -> (port : Port annot labelTy type projectedType endpoint endian)
      -> (rest : PortGroup annot labelTy endpoint endian ps pps)
      -> PortGroup annot labelTy endpoint endian (type::ps) (projectedType::pps)
(<::>) port rest = Add port rest

(<::~>) : (port : Port annot labelTy type projectedType endpoint endian)
       -> (rest : PortGroup annot labelTy endpoint endian ps pps)
       -> {auto prf : OptionalProjectedPort typeOfSkipped endpoint projectedTypeOfSkipped}
       -> PortGroup annot labelTy endpoint endian
                    (type::typeOfSkipped::ps)
                    (projectedType::projectedTypeOfSkipped::pps)
(<::~>) port rest {prf} = Add port (Skip rest prf)

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

max_stars_repo_name: border-patrol/cordial

max_issues_repo_name: border-patrol/cordial

max_forks_repo_name: border-patrol/cordial


text:
||| This file implements a ``Tanaka-Garrigue''-style dependently-typed red-black tree
|||
||| The original implementation and reasoning was initially developed in Coq by
||| K. Tanaka and J. Garrigue (and me) while trying to formalize dynamic bit vectors.
|||
||| I rewrote the dependently-typed development in Idris for a clearer
||| presentation, as the original was largely unreadable and very complicated.

module RedBlack

import Data.Vect

%default total

-- Color and color functions
public export
data Color = Red | Black

ColorValid : Color -> Color -> Type
ColorValid Red Red = Void
ColorValid _ _ = ()

validAnyBlack : (c : Color) -> ColorValid c Black
validAnyBlack Red = ()
validAnyBlack Black = ()

incrBlack : Nat -> Color -> Nat
incrBlack d Red = d
incrBlack d Black = S d

inv : Color -> Color
inv Red = Black
inv Black = Red

-- Red-black tree as an indexed inductive family
-- Invariants:
-- (1) no red node has a red child
-- (2) every path to a leaf has the same ``black-depth''
export
data Tree : Nat -> Color -> Type -> Type where
  Leaf : Tree 0 Black a
  Node : {d : Nat} -> {cl : Color} -> {cr : Color} -> (c : Color) ->
         ColorValid c cl -> ColorValid c cr ->
         Tree d cl a -> a -> Tree d cr a -> Tree (incrBlack d c) c a

export
empty : Tree 0 Black a
empty = Leaf

RNode : Tree d Black a -> a -> Tree d Black a -> Tree d Red a
RNode l v r = Node Red () () l v r

BNode : Tree d cl a -> a -> Tree d cr a -> Tree (incrBlack d Black) Black a
BNode l v r = Node Black () () l v r

export
member : Ord a => a -> Tree d c a -> Bool
member x Leaf = False
member x (Node _ _ _ l v r) with (compare x v)
  | LT = member x l
  | EQ = True
  | GT = member x r

size : Tree d c a -> Nat
size Leaf = 0
size (Node _ _ _ l v r) = S (size l + size r)

inOrderVec : (t : Tree d c a) -> Vect (size t) a
inOrderVec Leaf = Nil
inOrderVec (Node _ _ _ l v r) = rewrite plusSuccRightSucc (size l) (size r)
                                in      inOrderVec l ++ (v :: (inOrderVec r))

-- We need an intermediate representation for a potentially malformed tree which may occur in insertion
data InsTree : Nat -> Color -> Type -> Type where
  Fix : {d : Nat} -> Tree d Black a -> a -> Tree d Black a -> a ->
        Tree d Black a -> InsTree d Red a
  T : {d : Nat} -> {c : Color} -> (pc : Color) -> Tree d c a -> InsTree d pc a

insTreeColor : InsTree d c a -> Color
insTreeColor (Fix _ _ _ _ _) = Red
insTreeColor (T _ _) = Black

fixColor : InsTree d c a -> Color
fixColor (Fix _ _ _ _ _) = Black
fixColor (T {c = c} _ _) = c

fixInsTree : (t : InsTree d c a) -> Tree (incrBlack d (inv (insTreeColor t))) (fixColor t) a
fixInsTree (Fix t1 a t2 b t3) = BNode (RNode t1 a t2) b t3
fixInsTree (T _ t) = t

balanceL : (c : Color) -> (l : InsTree d cl a) -> a -> (r : Tree d cr a) ->
           ColorValid c (insTreeColor l) -> ColorValid c cr -> InsTree (incrBlack d c) c a
balanceL Black (Fix t1 a t2 b t3) c t4 _ _ = T Black (RNode (BNode t1 a t2) b (BNode t3 c t4))
balanceL Black (T _ l) v r _ _ = T Black (BNode l v r)
balanceL {cl = Black} {cr = Black} Red (T _ (Node {cl = Black} {cr = Black} Red _ _ t1 a t2)) b t3 _ _ = Fix t1 a t2 b t3
balanceL {cr = Red} Red (T _ (Node Red _ _ _ _ _)) _ _ _ _ impossible
balanceL {cl = Black} {cr = Black} Red (T {c = Black} _ l) v r _ _ = T Red (RNode l v r)
balanceL {cr = Red} Red (T _ _) _ _ _ _ impossible

balanceR : (c : Color) -> (l : Tree d cl a) -> a -> (r : InsTree d cr a) ->
           ColorValid c cl -> ColorValid c (insTreeColor r) -> InsTree (incrBlack d c) c a
balanceR Black t1 a (Fix t2 b t3 c t4) _ _ = T Black (RNode (BNode t1 a t2) b (BNode t3 c t4))
balanceR Black l v (T _ r) _ _ = T Black (BNode l v r)
balanceR {cl = Black} {cr = Black} Red t1 a (T _ (Node {cl = Black} {cr = Black} Red _ _ t2 b t3)) _ _ = Fix t1 a t2 b t3
balanceR {cl = Red} Red _ _ (T _ (Node Red _ _ _ _ _)) _ _ impossible
balanceR {cl = Black} {cr = Black} Red l v (T {c = Black} _ r) _ _ = T Red (RNode l v r)
balanceR {cl = Red} Red _ _ (T _ _) _ _ impossible

ins : Ord a => a -> Tree d c a -> InsTree d c a
ins x Leaf = T Black (RNode Leaf x Leaf)
ins x (Node c validL validR l v r) with (compare x v)
  | LT with (ins x l) proof insL
    ins x (Node Black _ validR l v r) | _ | Fix _ _ _ _ _ = balanceL Black (ins x l) v r () validR
    ins x (Node c _ validR l v r)     | _ | T _ _         = balanceL c (ins x l) v r leftValidPrf validR
      where leftValidPrf = rewrite (sym insL) in (validAnyBlack c)
  | EQ = T c (Node c validL validR l v r)
  | GT with (ins x r) proof insR
    ins x (Node Black validL _ l v r) | _ | Fix _ _ _ _ _ = balanceR Black l v (ins x r) validL ()
    ins x (Node c validL _ l v r)     | _ | T _ _         = balanceR c l v (ins x r) validL rightValidPrf
      where rightValidPrf = rewrite (sym insR) in (validAnyBlack c)

blacken : Tree d c a -> Tree (incrBlack d (inv c)) Black a
blacken Leaf = Leaf
blacken (Node c _ _ l v r) with (c)
  | Red = Node Black () () l v r
  | Black = Node Black () () l v r

export
insert : Ord a => a -> Tree d Black a -> (d : Nat ** Tree d Black a)
insert {d = d} x t with (ins x t)
  | T _ t' = (_ ** blacken t')

max_stars_repo_name: xuanruiqi/dtp

max_issues_repo_name: xuanruiqi/dtp

max_forks_repo_name: xuanruiqi/dtp


text:
module Main
import Effects
import IdrisWeb.CGI.Cgi
import IdrisWeb.Session.Session
import IdrisWeb.Session.SessionUtils
import IdrisWeb.DB.SQLite.SQLiteNew

ThreadID : Type
ThreadID = Int

DB_NAME : String
DB_NAME = "/tmp/messageboard.db"

UserID : Type
UserID = Int

USERID_VAR : String
USERID_VAR = "user_id"

----------
-- Handler info
----------
handleRegisterForm : Maybe String -> Maybe String -> FormHandler [CGI (InitialisedCGI TaskRunning),
                                                                  SESSION (SessionRes SessionUninitialised),
                                                                  SQLITE ()
                                                                 ]

handlePost : Maybe Int -> Maybe String -> FormHandler [CGI (InitialisedCGI TaskRunning),
                                                            SESSION (SessionRes SessionUninitialised),
                                                            SQLITE ()
                                                      ]

handleNewThread : Maybe String -> Maybe String -> FormHandler [CGI (InitialisedCGI TaskRunning),
                                                               SESSION (SessionRes SessionUninitialised),
                                                               SQLITE ()
                                                              ]

handleLoginForm : Maybe String -> Maybe String -> FormHandler [CGI (InitialisedCGI TaskRunning),
                                                                  SESSION (SessionRes SessionUninitialised),
                                                                  SQLITE ()
                                                              ]

handlers : HandlerList
handlers = [(([FormString, FormString], [CgiEffect, SessionEffect, SqliteEffect]) ** (handleRegisterForm, "handleRegisterForm")),
            (([FormString, FormString], [CgiEffect, SessionEffect, SqliteEffect]) ** (handleLoginForm, "handleLoginForm")),
            (([FormString, FormString], [CgiEffect, SessionEffect, SqliteEffect]) ** (handleNewThread, "handleNewThread")),
            (([FormInt, FormString], [CgiEffect, SessionEffect, SqliteEffect]) ** (handlePost, "handlePost"))]

-- Template system would be nice...
htmlPreamble : String
htmlPreamble = "<title>IdrisWeb Message Board</title>"

htmlPostamble : String
htmlPostamble = ""

notLoggedIn : EffM IO [CGI (InitialisedCGI TaskRunning),
                       SESSION (SessionRes SessionInitialised),
                       SQLITE ()]
                      [CGI (InitialisedCGI TaskRunning),
                       SESSION (SessionRes SessionUninitialised),
                       SQLITE ()] ()
notLoggedIn = do output htmlPreamble
                 output "
Error

You must be logged in to do that!"
                 output htmlPostamble
                 discardSession

outputWithPreamble : String -> Eff IO [CGI (InitialisedCGI TaskRunning)] ()
outputWithPreamble txt = do output htmlPreamble
                            output txt
                            output htmlPostamble
-----------
-- Post Creation
-----------
postInsert : Int -> Int -> String -> Eff IO [SQLITE ()] Bool
postInsert uid thread_id content = do
  conn_res <- openDB DB_NAME
  if_valid then do
    let sql = "INSERT INTO `Posts` (`UserID`, `ThreadID`, `Content`) VALUES (?, ?, ?)"
    ps_res <- prepareStatement sql
    if_valid then do
      bindInt 1 uid
      bindInt 2 thread_id
      bindText 3 content
      bind_res <- finishBind
      if_valid then do
        executeStatement
        finalise
        closeDB
        return True
      else do
        cleanupBindFail
        return  False
    else do
      cleanupPSFail
      return False
  else
    return False

addPostToDB : Int -> String -> SessionData -> EffM IO [CGI (InitialisedCGI TaskRunning),
                                                       SESSION (SessionRes SessionInitialised),
                                                       SQLITE ()]
                                                      [CGI (InitialisedCGI TaskRunning),
                                                       SESSION (SessionRes SessionUninitialised),
                                                       SQLITE ()] ()
addPostToDB thread_id content sd = do
-- TODO: would be nice to abstract this out
  case lookup USERID_VAR sd of
    Just (SInt uid) => do insert_res <- postInsert uid thread_id content
                          if insert_res then do
                            -- TODO: redirection would be nice
                            outputWithPreamble "Post successful"
                            discardSession
                            return ()
                          else do
                            outputWithPreamble "There was an error adding the post to the database."
                            discardSession
                            return ()
    Nothing => do notLoggedIn
                  return ()

handlePost (Just thread_id) (Just content) = do withSession (addPostToDB thread_id content) notLoggedIn
                                                pure ()
handlePost _ _ = do outputWithPreamble"
Error

There was an error processing your post."
                    pure ()

newPostForm : Int -> UserForm
newPostForm thread_id = do
  addHidden FormInt thread_id
  addTextBox "Post Content" FormString Nothing
  useEffects [CgiEffect, SessionEffect, SqliteEffect]
  addSubmit handlePost handlers

showNewPostForm : Int -> CGIProg [SESSION (SessionRes SessionUninitialised), SQLITE ()] ()
showNewPostForm thread_id = do
  output htmlPreamble
  output "
Create new post
"
  addForm (newPostForm thread_id)
  output htmlPostamble

-----------
-- Thread Creation
-----------

threadInsert : Int -> String -> String -> Eff IO [SQLITE ()] (Maybe QueryError)
threadInsert uid title content = do
  let query = "INSERT INTO `Threads` (`UserID`, `Title`) VALUES (?, ?)"
  insert_res <- executeInsert DB_NAME query [(1, DBInt uid), (2, DBText title)]
  case insert_res of
    Left err => return (Just err)
    Right thread_id => do
      post_res <- postInsert uid thread_id content
      if post_res then return Nothing else return $ Just (ExecError "post")

addNewThread : String -> String -> SessionData -> EffM IO [CGI (InitialisedCGI TaskRunning),
                                                       SESSION (SessionRes SessionInitialised),
                                                       SQLITE ()]
                                                      [CGI (InitialisedCGI TaskRunning),
                                                       SESSION (SessionRes SessionUninitialised),
                                                       SQLITE ()] ()
addNewThread title content sd = do
  case lookup USERID_VAR sd of
    Just (SInt uid) =>
      do insert_res <- threadInsert uid title content
         case insert_res of
           Just err => do
             output $ "There was an error adding the thread to the database: " ++ show err
             discardSession
             return ()
           Nothing => do
             output "Thread added successfully"
             discardSession
             return ()
    Nothing => do notLoggedIn
                  return ()

-- Create a new thread, given the title and content
handleNewThread (Just title) (Just content) = do withSession (addNewThread title content) notLoggedIn
                                                 pure ()
handleNewThread _ _ = do outputWithPreamble "
Error

There was an error posting your thread."
                         pure ()

newThreadForm : UserForm
newThreadForm = do
  addTextBox "Title" FormString Nothing
  addTextBox "Post Content" FormString Nothing -- password field would be good
  useEffects [CgiEffect, SessionEffect, SqliteEffect]
  addSubmit handleNewThread handlers

showNewThreadForm : CGIProg [SESSION (SessionRes SessionUninitialised), SQLITE ()] ()
showNewThreadForm = do output htmlPreamble
                       output "
New Thread
"
                       addForm newThreadForm
                       output htmlPostamble

-----------
-- Registration
-----------

insertUser : String -> String -> Eff IO [SQLITE ()] (Either QueryError Int)
insertUser name pwd = executeInsert DB_NAME query bind_vals
  where query = "INSERT INTO `Users` (`Username`, `Password`) VALUES (?, ?)"
        bind_vals = [(1, DBText name), (2, DBText pwd)]

userExists' : EffM IO [SQLITE (Either (SQLiteExecuting InvalidRow) (SQLiteExecuting ValidRow))]
              [SQLITE ()] Bool
userExists' =
  if_valid then do
    finaliseValid
    closeDB
    return True
  else do
    finaliseInvalid
    closeDB
    return False

userExists : String -> Eff IO [SQLITE ()] (Either QueryError Bool)
userExists username = do
  conn_res <- openDB DB_NAME
  if_valid then do
    let sql = "SELECT * FROM `Users` WHERE `Username` = ?"
    ps_res <- prepareStatement sql
    if_valid then do
      bindText 1 username
      bind_res <- finishBind
      if_valid then do
        executeStatement
        res <- userExists'
        return $ Right res
      else do
        let be = getBindError bind_res
        cleanupBindFail
        return $ Left be
    else do
      cleanupPSFail
      return $ Left (getQueryError ps_res)
  else
    return $ Left (getQueryError conn_res)

handleRegisterForm (Just name) (Just pwd) = do
  user_exists_res <- userExists name
  case user_exists_res of
    Left err => do outputWithPreamble "Error checking for user existence"
                   pure ()
    Right user_exists =>
      if (not user_exists) then do
        insert_res <- insertUser name pwd
        case insert_res of
          Left err => do outputWithPreamble ("Error inserting new user" ++ (show err))
                         pure ()
          Right insert_res => do outputWithPreamble "User created successfully!"
                                 pure ()
      else do outputWithPreamble "This user already exists; please pick another name!"
              pure ()

handleRegisterForm _ _ = do outputWithPreamble "Error processing form input data."
                            pure ()

registerForm : UserForm
registerForm = do
  addTextBox "Username" FormString Nothing
  addTextBox "Password" FormString Nothing -- password field would be good
  useEffects [CgiEffect, SessionEffect, SqliteEffect]
  addSubmit handleRegisterForm handlers

showRegisterForm : CGIProg [SESSION (SessionRes SessionUninitialised), SQLITE ()] ()
showRegisterForm = do output htmlPreamble
                      output "
Create a new account
"
                      addForm registerForm
                      output htmlPostamble

-----------
-- Login
-----------
alreadyLoggedIn : SessionData ->
                  EffM IO [CGI (InitialisedCGI TaskRunning),
                           SESSION (SessionRes SessionInitialised),
                           SQLITE ()]
                          [CGI (InitialisedCGI TaskRunning),
                           SESSION (SessionRes SessionUninitialised),
                           SQLITE ()] ()
alreadyLoggedIn _ = do outputWithPreamble "
Error

You appear to already be logged in!"
                       discardSession
-- If the credentials match, return an ID
-- Maybe consolidate the Maybe UserID into the Either, or possibly keep them
-- distinct to encapsulate the system error vs auth failure
authUser' : EffM IO [SQLITE (Either (SQLiteExecuting InvalidRow)
                                    (SQLiteExecuting ValidRow))]
                    [SQLITE ()]
                    (Either QueryError (Maybe UserID))
authUser' =
  if_valid then do
    user_id <- getColumnInt 0
    finaliseValid
    closeDB
    return $ Right (Just user_id)
  else do
    finaliseInvalid
    closeDB
    return $ Right Nothing

authUser : String -> String -> Eff IO [SQLITE ()] (Either QueryError (Maybe UserID))
authUser username password = do
  conn_res <- openDB DB_NAME
  if_valid then do
    let sql = "SELECT `UserID` FROM `Users` WHERE `Username` = ? AND `Password` = ?"
    ps_res <- prepareStatement sql
    if_valid then do
      bindText 1 username
      bindText 2 password
      bind_res <- finishBind
      if_valid then do
        executeStatement
        authUser'
      else do
        let be = getBindError bind_res
        cleanupBindFail
        return $ Left be
    else do
      cleanupPSFail
      return $ Left (getQueryError ps_res)
  else
    return $ Left (getQueryError conn_res)

setSession : UserID -> Eff IO [CGI (InitialisedCGI TaskRunning), SESSION (SessionRes SessionUninitialised), SQLITE ()] Bool
setSession user_id = do
  create_res <- createSession [(USERID_VAR, SInt user_id)]
  sess_res <- setSessionCookie
  db_res <- writeSessionToDB
  return (sess_res && db_res)

handleLoginForm (Just name) (Just pwd) = do
  auth_res <- authUser name pwd
  case auth_res of
    Right (Just uid) => do
      set_sess_res <- setSession uid
      if set_sess_res then do
        output $ "Welcome, " ++ name
        return ()
      else do
        output "Could not set session"
        return ()
    Right Nothing => do
      output "Invalid username or password"
      return ()
    Left err => do
      output $ "Error: " ++ (show err)
      return ()

loginForm : UserForm
loginForm = do
  addTextBox "Username" FormString Nothing
  addTextBox "Password" FormString Nothing -- password field would be good
  useEffects [CgiEffect, SessionEffect, SqliteEffect]
  addSubmit handleLoginForm handlers

showLoginForm : CGIProg [SESSION (SessionRes SessionUninitialised), SQLITE ()] ()
showLoginForm = do output htmlPreamble
                   output "
Log in
"
                   addForm loginForm
                   output ""

-----------
-- Post / Thread Display
-----------

collectPostResults : Eff IO [SQLITE (SQLiteExecuting ValidRow)] (List DBVal) -- (List (String, String))
collectPostResults = do name <- getColumnText 0
                        content <- getColumnText 1
                        pure [DBText name, DBText content]
-- Gets the posts
getPosts : Int -> Eff IO [SQLITE ()] (Either QueryError ResultSet)
getPosts thread_id =
  executeSelect DB_NAME query bind_vals collectPostResults
 where query = "SELECT `Username`, `Content` FROM `Posts` NATURAL JOIN `Users` WHERE `ThreadID` = ?"
       bind_vals = [(1, DBInt thread_id)]

collectThreadResults : Eff IO [SQLITE (SQLiteExecuting ValidRow)] (List DBVal)
collectThreadResults = do thread_id <- getColumnInt 0
                          title <- getColumnText 1
                          uid <- getColumnInt 2
                          username <- getColumnText 3
                          pure [DBInt thread_id, DBText title, DBInt uid, DBText username]

-- Returns (Title, Thread starter ID, Thread starter name)
getThreads : Eff IO [SQLITE ()] (Either QueryError ResultSet)
getThreads = executeSelect DB_NAME query [] collectThreadResults
  where query = "SELECT `ThreadID`, `Title`, `UserID`, `Username` FROM `Threads` NATURAL JOIN `Users`"

traversePosts : ResultSet -> Eff IO [CGI (InitialisedCGI TaskRunning)] ()
traversePosts [] = pure ()
traversePosts (x :: xs) = do traverseRow x
                             traversePosts xs
  where traverseRow : List DBVal -> Eff IO [CGI (InitialisedCGI TaskRunning)] ()
        traverseRow ((DBText name)::(DBText content)::[]) = output $ "
" ++ name ++ "	" ++ content ++ "
"
        traverseRow _ = pure () -- invalid row, discard

printPosts : ThreadID -> CGIProg [SQLITE ()] ()
printPosts thread_id = do
  post_res <- getPosts thread_id
  case post_res of
    Left err => do output $ "Could not retrieve posts, error: " ++ (show err)
                   return ()
    Right posts => do output "
"
                      traversePosts posts
                      output "
"
                      output $ "New post
"
                      return ()

traverseThreads : ResultSet -> Eff IO [CGI (InitialisedCGI TaskRunning)] ()
traverseThreads [] = pure ()
traverseThreads (x::xs) = do traverseRow x
                             traverseThreads xs
  where traverseRow : List DBVal -> Eff IO [CGI (InitialisedCGI TaskRunning)] ()
        traverseRow ((DBInt thread_id)::(DBText title)::(DBInt user_id)::(DBText username)::[]) =
           (output $ "
" ++ title ++ "	" ++ username ++ "
")
        traverseRow _ = pure ()

printThreads : CGIProg [SQLITE ()] ()
printThreads = do
  thread_res <- getThreads
  case thread_res of
    Left err => do output $ "Could not retrieve threads, error: " ++ (show err)
                   return ()
    Right threads => do output htmlPreamble
                        output "

Title	Author
"
                        traverseThreads threads
                        output "

"
                        output "Create a new thread
"
                        output "Register
"
                        output "Log In
"
                        output htmlPostamble
                        return ()
-----------
-- Request handling
-----------
handleNonFormRequest : Maybe String -> Maybe Int -> CGIProg [SESSION (SessionRes SessionUninitialised), SQLITE ()] ()
handleNonFormRequest (Just "newthread") Nothing = showNewThreadForm
handleNonFormRequest (Just "newpost") (Just thread_id) = showNewPostForm thread_id
handleNonFormRequest (Just "showthread") (Just thread_id) = printPosts thread_id
handleNonFormRequest (Just "register") Nothing = showRegisterForm
handleNonFormRequest (Just "login") Nothing = showLoginForm
handleNonFormRequest Nothing _ =  printThreads

-- Hacky, probably best to use the parser
strToInt : String -> Int
strToInt s = cast s

handleRequest : CGIProg [SESSION (SessionRes SessionUninitialised), SQLITE ()] ()
handleRequest = do handler_set <- isHandlerSet
                   if handler_set then do
                     handleForm handlers
                     return ()
                   else do
                     action <- queryGetVar "action"
                     thread_id <- queryGetVar "thread_id"
                     handleNonFormRequest action (map strToInt thread_id)

main : IO ()
main = do runCGI [initCGIState, InvalidSession, ()] handleRequest
          pure ()

max_stars_repo_name: idris-hackers/IdrisWeb

max_issues_repo_name: idris-hackers/IdrisWeb

max_forks_repo_name: idris-hackers/IdrisWeb


text:
plusnZ : (n : Nat) -> n + 0 = n
plusnZ 0 = Refl
plusnZ (S k) = rewrite plusnZ k in Refl

plusnSm : (n, m : Nat) -> n + (S m) = S (n + m)
plusnSm Z m = Refl
plusnSm (S k) m = rewrite plusnSm k m in Refl

plusCommutes : (n, m : Nat) -> n + m = m + n
plusCommutes Z m = sym (plusnZ m)
plusCommutes (S k) m = rewrite plusCommutes k m in sym (plusnSm m k)

wrongCommutes : (n, m : Nat) -> n + m = m + n
wrongCommutes Z m = sym (plusnZ m)
wrongCommutes (S k) m = rewrite plusCommutes m k in ?bar

wrongCommutes2 : (n, m : Nat) -> n + m = m + n
wrongCommutes2 Z m = sym (plusnZ m)
wrongCommutes2 (S k) m = rewrite m in ?bar


text:
public export
data Phase = Gas | Liquid | Solid

public export
data ChangePhase : Phase -> Phase -> Type where
	Sequence : ChangePhase a b -> ChangePhase b c -> ChangePhase a c
	Condense : ChangePhase Gas Liquid
	Freeze : ChangePhase Liquid Solid
	Melt : ChangePhase Solid Liquid
	Vaporize : ChangePhase Liquid Gas
	Sublimate : ChangePhase Solid Gas

public export
inferred : { auto transition : ChangePhase l r } -> ChangePhase l r
inferred { transition } = transition

test : ChangePhase Gas Solid
test = inferred


text:
module Cairo.Output

import Common

public export
%foreign
    "apStable:True"
    """
    code:
    func Cairo_Output_cairooutput(value, output_ptr) -> (output_ptr):
        assert [output_ptr] = value
        return (output_ptr + 1)
    end
    """
cairooutput :  Felt -> PrimCairoUnit

-- Outputs the given value (and keeps track ouf the output_ptr)
public export %inline
output : Felt -> Cairo ()
output val = fromPrimCairoUnit (cairooutput val)

max_stars_repo_name: skyro-compiler/skyro

max_issues_repo_name: skyro-compiler/skyro

max_forks_repo_name: skyro-compiler/skyro


text:
module Data.Binary.Digit

%default total

||| This is essentially Bool but with names that are easier
||| to understand
public export
data Digit : Type where
  O : Digit
  I : Digit

||| Translation to Bool
public export
isI : Digit -> Bool
isI I = True
isI O = False

public export
toNat : Digit -> Nat
toNat O = 0
toNat I = 1


text:
module IdrisJvm.Data.Strings

import IdrisJvm.IO
import Java.Lang

%hide Prelude.Strings.StringBuffer

public export
StringsClass : JVM_NativeTy
StringsClass = Class "io/github/mmhelloworld/idrisjvm/runtime/Strings"

export
bytesLengthUtf8 : String -> JVM_IO Int
bytesLengthUtf8 = invokeStatic StringsClass "bytesLengthUtf8" (String -> JVM_IO Int)

export
StringBuffer : Type
StringBuffer = StringBuilder

export
newStringBuffer : (len : Int) -> JVM_IO StringBuffer
newStringBuffer len = StringBuilder.new len

export
addToStringBuffer : StringBuffer -> String -> JVM_IO ()
addToStringBuffer buffer str = StringBuilder.appendString buffer str >>= (\buf => pure ())

export
getStringFromBuffer : StringBuffer -> JVM_IO String
getStringFromBuffer buffer = StringBuilder.toString buffer


text:
||| For Plain Merge we need to compare Local types for equality.
module Sessions.Local.Same

import Decidable.Equality
import Data.List
import Data.List.Elem

import Data.List1

import Sessions.Meta
import Sessions.Local

%default total

notEC : Local.End = Choice ty whom selections -> Void
notEC Refl impossible

notVVElem : (x = y -> Void) -> Local.Call x = Local.Call y -> Void
notVVElem f Refl = f Refl

notVR : Local.Call x = Local.Rec y -> Void
notVR Refl impossible

notVC : Local.Call x = Choice ty whom selections -> Void
notVC Refl impossible

notRRBody : (x = y -> Void) -> Local.Rec x = Local.Rec y -> Void
notRRBody f Refl = f Refl

notRC : Local.Rec x = Choice ty whom selections -> Void
notRC Refl impossible

notCCTy : (tyA = tyB -> Void) -> Local.Choice tyA a as = Local.Choice tyB b bs -> Void
notCCTy f Refl = f Refl

notCCWhom : (a = b -> Void) -> Local.Choice tyA a as = Local.Choice tyA b bs -> Void
notCCWhom f Refl = f Refl

notCCSels : (as = bs -> Void) -> Local.Choice tyA a as = Local.Choice tyA a bs -> Void
notCCSels f Refl = f Refl

mutual

  export
  same : DecEq role label msg
      => (a,b : Local role label msg rs g)
             -> Dec (Equal a b)
  same End End = Yes Refl
  same End (Choice ty whom selections)
    = No (notEC)

  same (Call x) (Call y) with (decEq x y)
    same (Call x) (Call x) | (Yes Refl)
      = Yes Refl
    same (Call x) (Call y) | (No contra)
      = No (notVVElem contra)

  same (Call x) (Rec y)
    = No notVR
  same (Call x) (Choice ty whom selections)
    = No notVC

  same (Rec x) (Call y)
    = No (negEqSym notVR)
  same (Rec x) (Rec y) with (same x y)
    same (Rec x) (Rec x) | (Yes Refl) = Yes Refl
    same (Rec x) (Rec y) | (No contra)
      = No (notRRBody contra)

  same (Rec x) (Choice ty whom selections)
    = No notRC

  same (Choice ty whom selections) End
    = No (negEqSym notEC)
  same (Choice ty whom selections) (Call x)
    = No (negEqSym notVC)
  same (Choice ty whom selections) (Rec x)
    = No (negEqSym notRC)

  same (Choice tyA a as) (Choice tyB b bs) with (decEq tyA tyB)
    same (Choice tyA a as) (Choice tyA b bs) | (Yes Refl) with (decEq a b)
      same (Choice tyA a as) (Choice tyA a bs) | (Yes Refl) | (Yes Refl) with (List1.same as bs)
        same (Choice tyA a as) (Choice tyA a as) | (Yes Refl) | (Yes Refl) | (Yes Refl)
          = Yes Refl
        same (Choice tyA a as) (Choice tyA a bs) | (Yes Refl) | (Yes Refl) | (No contra)
          = No (notCCSels contra)

      same (Choice tyA a as) (Choice tyA b bs) | (Yes Refl) | (No contra)
        = No (notCCWhom contra)

    same (Choice tyA a as) (Choice tyB b bs) | (No contra)
      = No (notCCTy contra)

  namespace Pair

    notPairSameLabel : {am, bm : _}
                    -> {ab, bb : _}
                    -> (al = bl -> Void) -> (al, (am, ab)) = (bl, (bm, bb)) -> Void
    notPairSameLabel f Refl = f Refl

    notPairSameMsg : {al : _}
                  -> {ab, bb : _}
                  -> (am = bm -> Void) -> (al, (am, ab)) = (al, (bm, bb)) -> Void
    notPairSameMsg f Refl = f Refl

    notPairSameRest : {al : _}
                   -> {am : _}
                   -> (ab = bb -> Void) -> (al, (am, ab)) = (al, (am, bb)) -> Void
    notPairSameRest f Refl = f Refl

    export
    same : DecEq role label msg
        => (x,y : Branch role label msg rs g)
               -> Dec (Equal x y)
    same (al, (am, ab)) (bl, (bm, bb)) with (decEq al bl)
      same (al, (am, ab)) (al, (bm, bb)) | (Yes Refl) with (decEq am bm)
        same (al, (am, ab)) (al, (am, bb)) | (Yes Refl) | (Yes Refl) with (same ab bb)
          same (al, (am, ab)) (al, (am, ab)) | (Yes Refl) | (Yes Refl) | (Yes Refl)
            = Yes Refl
          same (al, (am, ab)) (al, (am, bb)) | (Yes Refl) | (Yes Refl) | (No contra)
            = No (notPairSameRest contra)
        same (al, (am, ab)) (al, (bm, bb)) | (Yes Refl) | (No contra)
          = No (notPairSameMsg contra)
      same (al, (am, ab)) (bl, (bm, bb)) | (No contra)
        = No (notPairSameLabel contra)

  namespace List

    notSamesRightEmpty : [] = x :: xs -> Void
    notSamesRightEmpty Refl impossible

    notSamesHead : {xs, ys : Branches' roel label msg rs g}
                -> (x = y -> Void)
                -> (::) x xs = (::) y ys
                -> Void
    notSamesHead f Refl = f Refl

    notSamesTail : {xs, ys : Branches' roel label msg rs g}
                -> (xs = ys -> Void)
                -> x :: xs = x :: ys
                -> Void
    notSamesTail f Refl = f Refl

    export
    same : DecEq role label msg
        => (as, bs : Branches' role label msg rs g)
                  -> Dec (Equal as bs)

    same [] [] = Yes Refl
    same [] (x :: xs) = No (notSamesRightEmpty)
    same (x :: xs) [] = No (negEqSym notSamesRightEmpty)
    same (x :: xs) (y :: ys) with (Pair.same x y)
      same (x :: xs) (x :: ys) | (Yes Refl) with (same xs ys)
        same (x :: ys) (x :: ys) | (Yes Refl) | (Yes Refl)
          = Yes Refl
        same (x :: xs) (x :: ys) | (Yes Refl) | (No contra)
          = No (notSamesTail contra)
      same (x :: xs) (y :: ys) | (No contra)
        = No (notSamesHead contra)

  namespace List1

    notSames1Head : (a = b -> Void) -> a ::: as = b ::: bs -> Void
    notSames1Head f Refl = f Refl

    notSames1Tail : (as = bs -> Void) -> a ::: as = a ::: bs -> Void
    notSames1Tail f Refl = f Refl

    export
    same : DecEq role label msg
        => (as, bs : Branches role label msg rs g)
                  -> Dec (Equal as bs)

    same (a ::: as) (b ::: bs) with (same a b)
      same (a ::: as) (a ::: bs) | (Yes Refl) with (same as bs)
        same (a ::: bs) (a ::: bs) | (Yes Refl) | (Yes Refl)
          = Yes Refl
        same (a ::: as) (a ::: bs) | (Yes Refl) | (No contra)
          = No (notSames1Tail contra)
      same (a ::: as) (b ::: bs) | (No contra)
        = No (notSames1Head contra)

-- [ EOF ]

max_stars_repo_name: DSbD-AppControl/sessions-playground

max_issues_repo_name: DSbD-AppControl/sessions-playground

max_forks_repo_name: DSbD-AppControl/sessions-playground


text:
module Main

import Dart.Core
import Dart.FFI.Elab

%language ElabReflection

%runElab importDart [
  package "package:sqlite3/sqlite3.dart" [
    final "Sqlite3" "sqlite3",
    class' "Sqlite3" [
      final "Version" "version",
      io "Database" "openInMemory" []
    ],
    class' "Version" [
    ],
    class' "Database" [
      io "void" "execute" ["sql" :: "String"],
      io "PreparedStatement" "prepare" ["sql" :: "String"],
      io "ResultSet" "select" ["sql" :: "String", "parameters" :: "Dart.Core.List" :<> "Object"],
      io "void" "dispose" []
    ],
    class' "PreparedStatement" [
      io "void" "execute" ["parameters" :: "Dart.Core.List" :<> "Object"],
      io "void" "dispose" []
    ],
    class' "ResultSet" [
      extends ("Iterable" :<> "Row")
    ],
    class' "Row" [
    ]
  ]
]

%inline
objectList : UpcastList Object -> Core.List Object
objectList = fromList . toList

main : IO ()
main = do
  putStrLn ("Using sqlite3 " ++ !(sqlite3 @. version @. toString))
  db <- sqlite3 @. openInMemory
  db @. execute """
    CREATE TABLE artists (
      id INTEGER NOT NULL PRIMARY KEY,
      name TEXT NOT NULL
    );
  """
  stmt <- db @. prepare "INSERT INTO artists (name) VALUES (?)"
  stmt @. execute (objectList ["The Beatles"])
  stmt @. execute (objectList ["Led Zeppelin"])
  stmt @. execute (objectList ["The Who"])
  stmt @. execute (objectList ["Nirvana"])
  dispose stmt

  resultSet <- db @. select "SELECT * FROM artists WHERE name LIKE ?" (objectList ["The %"])

  resultSet @. forEach {element = Row} print

  dispose db


text:
longer : String -> String -> Nat
longer word1 word2 =
    let len1 = length word1
        len2 = length word2 in
            if len1 > len2 then len1 else len2

pythagoras : Double -> Double -> Double
pythagoras x y = sqrt (square x + square y)
    where
        square : Double -> Double
        square x = x * x

max_stars_repo_name: curtisalexander/tdd-idris

max_issues_repo_name: curtisalexander/tdd-idris

max_forks_repo_name: curtisalexander/tdd-idris