text:
> module SequentialDecisionProblems.applications.Main

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

> import SequentialDecisionProblems.CoreTheory
> import SequentialDecisionProblems.FullTheory
> import SequentialDecisionProblems.TabBackwardsInduction
> import SequentialDecisionProblems.Utils
> import SequentialDecisionProblems.NonDeterministicDefaults
> import SequentialDecisionProblems.CoreTheoryOptDefaults
> import SequentialDecisionProblems.FullTheoryOptDefaults
> import SequentialDecisionProblems.TabBackwardsInductionOptDefaults

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

> 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 NonNegDouble.Measures
> import NonNegDouble.MeasureProperties
> 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 List.Properties
> import Unit.Properties

> -- %default total
> %auto_implicits off

> -- %logging 5

* Controls

> SequentialDecisionProblems.CoreTheory.Ctrl _ _ = LowHigh

* States

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

* Transition function

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

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

> -- 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
> SequentialDecisionProblems.CoreTheory.nexts t (e, High, Unavailable, Good) Low =
>   let ttres : List (State (S t))
>             = [(weaken e, Low,  Unavailable, Good),
>                (    FS e, High, Unavailable, Good),
>                (weaken e, Low,    Available, Good),
>                (    FS e, High,   Available, Good),
>                (weaken e, Low,  Unavailable,  Bad),
>                (    FS e, High, Unavailable,  Bad),
>                (weaken e, Low,    Available,  Bad),
>                (    FS e, High,   Available,  Bad)] in
>   let tfres : List (State (S t))
>             = [(weaken e, Low,  Unavailable, Good),
>                (    FS e, High, Unavailable, Good),
>                (weaken e, Low,    Available, Good),
>                (    FS e, High,   Available, Good),
>                (weaken e, Low,  Unavailable,  Bad),
>                (    FS e, High, Unavailable,  Bad),
>                (weaken e, Low,    Available,  Bad),
>                (    FS e, High,   Available,  Bad)] in
>   let ftres : List (State (S t))
>             = [(weaken e, Low,  Unavailable, Good),
>                (    FS e, High, Unavailable, Good),
>                (weaken e, Low,    Available, Good),
>                (    FS e, High,   Available, Good),
>                (weaken e, Low,  Unavailable,  Bad),
>                (    FS e, High, Unavailable,  Bad),
>                (weaken e, Low,    Available,  Bad),
>                (    FS e, High,   Available,  Bad)] in
>   let ffres : List (State (S t))
>             = [(weaken e, Low,  Unavailable, Good),
>                (    FS e, High, Unavailable, Good),
>                (weaken e, Low,    Available, Good),
>                (    FS e, High,   Available, Good),
>                (weaken e, Low,  Unavailable,  Bad),
>                (    FS e, High, Unavailable,  Bad),
>                (weaken e, Low,    Available,  Bad),
>                (    FS e, High,   Available,  Bad)] in
>   case (t <= crN) of
>     True  => case (fromFin e <= crE) of
>                True  => ttres
>                False => tfres
>     False => case (fromFin e <= crE) of
>                True  => ftres
>                False => ffres
> SequentialDecisionProblems.CoreTheory.nexts t (e, High, Unavailable, Good) High =
>   let ttres : List (State (S t))
>             = [(weaken e, Low,  Unavailable, Good),
>                (    FS e, High, Unavailable, Good),
>                (weaken e, Low,    Available, Good),
>                (    FS e, High,   Available, Good),
>                (weaken e, Low,  Unavailable,  Bad),
>                (    FS e, High, Unavailable,  Bad),
>                (weaken e, Low,    Available,  Bad),
>                (    FS e, High,   Available,  Bad)] in
>   let tfres : List (State (S t))
>             = [(weaken e, Low,  Unavailable, Good),
>                (    FS e, High, Unavailable, Good),
>                (weaken e, Low,    Available, Good),
>                (    FS e, High,   Available, Good),
>                (weaken e, Low,  Unavailable,  Bad),
>                (    FS e, High, Unavailable,  Bad),
>                (weaken e, Low,    Available,  Bad),
>                (    FS e, High,   Available,  Bad)] in
>   let ftres : List (State (S t))
>             = [(weaken e, Low,  Unavailable, Good),
>                (    FS e, High, Unavailable, Good),
>                (weaken e, Low,    Available, Good),
>                (    FS e, High,   Available, Good),
>                (weaken e, Low,  Unavailable,  Bad),
>                (    FS e, High, Unavailable,  Bad),
>                (weaken e, Low,    Available,  Bad),
>                (    FS e, High,   Available,  Bad)] in
>   let ffres : List (State (S t))
>             = [(weaken e, Low,  Unavailable, Good),
>                (    FS e, High, Unavailable, Good),
>                (weaken e, Low,    Available, Good),
>                (    FS e, High,   Available, Good),
>                (weaken e, Low,  Unavailable,  Bad),
>                (    FS e, High, Unavailable,  Bad),
>                (weaken e, Low,    Available,  Bad),
>                (    FS e, High,   Available,  Bad)] in
>   case (t <= crN) of
>     True  => case (fromFin e <= crE) of
>                True  => ttres
>                False => tfres
>     False => case (fromFin e <= crE) of
>                True  => ftres
>                False => ffres
>
> -- The transition function: high emissions, unavailable GHG technologies, bad world
> SequentialDecisionProblems.CoreTheory.nexts t (e, High, Unavailable, Bad) Low =
>   let ttres : List (State (S t))
>             = [(weaken e, Low,  Unavailable,  Bad),
>                (    FS e, High, Unavailable,  Bad),
>                (weaken e, Low,    Available,  Bad),
>                (    FS e, High,   Available,  Bad)] in
>   let tfres : List (State (S t))
>             = [(weaken e, Low,  Unavailable,  Bad),
>                (    FS e, High, Unavailable,  Bad),
>                (weaken e, Low,    Available,  Bad),
>                (    FS e, High,   Available,  Bad)] in
>   let ftres : List (State (S t))
>             = [(weaken e, Low,  Unavailable,  Bad),
>                (    FS e, High, Unavailable,  Bad),
>                (weaken e, Low,    Available,  Bad),
>                (    FS e, High,   Available,  Bad)] in
>   let ffres : List (State (S t))
>             = [(weaken e, Low,  Unavailable,  Bad),
>                (    FS e, High, Unavailable,  Bad),
>                (weaken e, Low,    Available,  Bad),
>                (    FS e, High,   Available,  Bad)] in
>   case (t <= crN) of
>     True  => case (fromFin e <= crE) of
>                True  => ttres
>                False => tfres
>     False => case (fromFin e <= crE) of
>                True  => ftres
>                False => ffres
> SequentialDecisionProblems.CoreTheory.nexts t (e, High, Unavailable, Bad) High =
>   let ttres : List (State (S t))
>             = [(weaken e, Low,  Unavailable,  Bad),
>                (    FS e, High, Unavailable,  Bad),
>                (weaken e, Low,    Available,  Bad),
>                (    FS e, High,   Available,  Bad)] in
>   let tfres : List (State (S t))
>             = [(weaken e, Low,  Unavailable,  Bad),
>                (    FS e, High, Unavailable,  Bad),
>                (weaken e, Low,    Available,  Bad),
>                (    FS e, High,   Available,  Bad)] in
>   let ftres : List (State (S t))
>             = [(weaken e, Low,  Unavailable,  Bad),
>                (    FS e, High, Unavailable,  Bad),
>                (weaken e, Low,    Available,  Bad),
>                (    FS e, High,   Available,  Bad)] in
>   let ffres : List (State (S t))
>             = [(weaken e, Low,  Unavailable,  Bad),
>                (    FS e, High, Unavailable,  Bad),
>                (weaken e, Low,    Available,  Bad),
>                (    FS e, High,   Available,  Bad)] in
>   case (t <= crN) of
>     True  => case (fromFin e <= crE) of
>                True  => ttres
>                False => tfres
>     False => case (fromFin e <= crE) of
>                True  => ftres
>                False => 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 : List (State (S t))
>             = [(weaken e, Low,    Available, Good),
>                (    FS e, High,   Available, Good),
>                (weaken e, Low,    Available,  Bad),
>                (    FS e, High,   Available,  Bad)] in
>   let tfres : List (State (S t))
>             = [(weaken e, Low,    Available, Good),
>                (    FS e, High,   Available, Good),
>                (weaken e, Low,    Available,  Bad),
>                (    FS e, High,   Available,  Bad)] in
>   let ftres : List (State (S t))
>             = [(weaken e, Low,    Available, Good),
>                (    FS e, High,   Available, Good),
>                (weaken e, Low,    Available,  Bad),
>                (    FS e, High,   Available,  Bad)] in
>   let ffres : List (State (S t))
>             = [(weaken e, Low,    Available, Good),
>                (    FS e, High,   Available, Good),
>                (weaken e, Low,    Available,  Bad),
>                (    FS e, High,   Available,  Bad)] in
>   case (t <= crN) of
>     True  => case (fromFin e <= crE) of
>                True  => ttres
>                False => tfres
>     False => case (fromFin e <= crE) of
>                True  => ftres
>                False => ffres
> SequentialDecisionProblems.CoreTheory.nexts t (e, High, Available, Good) High =
>   let ttres : List (State (S t))
>             = [(weaken e, Low,    Available, Good),
>                (    FS e, High,   Available, Good),
>                (weaken e, Low,    Available,  Bad),
>                (    FS e, High,   Available,  Bad)] in
>   let tfres : List (State (S t))
>             = [(weaken e, Low,    Available, Good),
>                (    FS e, High,   Available, Good),
>                (weaken e, Low,    Available,  Bad),
>                (    FS e, High,   Available,  Bad)] in
>   let ftres : List (State (S t))
>             = [(weaken e, Low,    Available, Good),
>                (    FS e, High,   Available, Good),
>                (weaken e, Low,    Available,  Bad),
>                (    FS e, High,   Available,  Bad)] in
>   let ffres : List (State (S t))
>             = [(weaken e, Low,    Available, Good),
>                (    FS e, High,   Available, Good),
>                (weaken e, Low,    Available,  Bad),
>                (    FS e, High,   Available,  Bad)] in
>   case (t <= crN) of
>     True  => case (fromFin e <= crE) of
>                True  => ttres
>                False => tfres
>     False => case (fromFin e <= crE) of
>                True  => ftres
>                False => ffres
>
> -- The transition function: high emissions, available GHG technologies, bad world
> SequentialDecisionProblems.CoreTheory.nexts t (e, High, Available, Bad) Low =
>   let ttres : List (State (S t))
>             = [(weaken e, Low,    Available,  Bad),
>                (    FS e, High,   Available,  Bad)] in
>   let tfres : List (State (S t))
>             = [(weaken e, Low,    Available,  Bad),
>                (    FS e, High,   Available,  Bad)] in
>   let ftres : List (State (S t))
>             = [(weaken e, Low,    Available,  Bad),
>                (    FS e, High,   Available,  Bad)] in
>   let ffres : List (State (S t))
>             = [(weaken e, Low,    Available,  Bad),
>                (    FS e, High,   Available,  Bad)] in
>   case (t <= crN) of
>     True  => case (fromFin e <= crE) of
>                True  => ttres
>                False => tfres
>     False => case (fromFin e <= crE) of
>                True  => ftres
>                False => ffres
> SequentialDecisionProblems.CoreTheory.nexts t (e, High, Available, Bad) High =
>   let ttres : List (State (S t))
>             = [(weaken e, Low,    Available,  Bad),
>                (    FS e, High,   Available,  Bad)] in
>   let tfres : List (State (S t))
>             = [(weaken e, Low,    Available,  Bad),
>                (    FS e, High,   Available,  Bad)] in
>   let ftres : List (State (S t))
>             = [(weaken e, Low,    Available,  Bad),
>                (    FS e, High,   Available,  Bad)] in
>   let ffres : List (State (S t))
>             = [(weaken e, Low,    Available,  Bad),
>                (    FS e, High,   Available,  Bad)] in
>   case (t <= crN) of
>     True  => case (fromFin e <= crE) of
>                True  => ttres
>                False => tfres
>     False => case (fromFin e <= crE) of
>                True  => ftres
>                False => 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 : List (State (S t))
>             = [(weaken e, Low,  Unavailable, Good),
>                (    FS e, High, Unavailable, Good),
>                (weaken e, Low,    Available, Good),
>                (    FS e, High,   Available, Good),
>                (weaken e, Low,  Unavailable,  Bad),
>                (    FS e, High, Unavailable,  Bad),
>                (weaken e, Low,    Available,  Bad),
>                (    FS e, High,   Available,  Bad)] in
>   let tfres : List (State (S t))
>             = [(weaken e, Low,  Unavailable, Good),
>                (    FS e, High, Unavailable, Good),
>                (weaken e, Low,    Available, Good),
>                (    FS e, High,   Available, Good),
>                (weaken e, Low,  Unavailable,  Bad),
>                (    FS e, High, Unavailable,  Bad),
>                (weaken e, Low,    Available,  Bad),
>                (    FS e, High,   Available,  Bad)] in
>   let ftres : List (State (S t))
>             = [(weaken e, Low,  Unavailable, Good),
>                (    FS e, High, Unavailable, Good),
>                (weaken e, Low,    Available, Good),
>                (    FS e, High,   Available, Good),
>                (weaken e, Low,  Unavailable,  Bad),
>                (    FS e, High, Unavailable,  Bad),
>                (weaken e, Low,    Available,  Bad),
>                (    FS e, High,   Available,  Bad)] in
>   let ffres : List (State (S t))
>             = [(weaken e, Low,  Unavailable, Good),
>                (    FS e, High, Unavailable, Good),
>                (weaken e, Low,    Available, Good),
>                (    FS e, High,   Available, Good),
>                (weaken e, Low,  Unavailable,  Bad),
>                (    FS e, High, Unavailable,  Bad),
>                (weaken e, Low,    Available,  Bad),
>                (    FS e, High,   Available,  Bad)] in
>   case (t <= crN) of
>     True  => case (fromFin e <= crE) of
>                True  => ttres
>                False => tfres
>     False => case (fromFin e <= crE) of
>                True  => ftres
>                False => ffres
> SequentialDecisionProblems.CoreTheory.nexts t (e, Low, Unavailable, Good) High =
>   let ttres : List (State (S t))
>             = [(weaken e, Low,  Unavailable, Good),
>                (    FS e, High, Unavailable, Good),
>                (weaken e, Low,    Available, Good),
>                (    FS e, High,   Available, Good),
>                (weaken e, Low,  Unavailable,  Bad),
>                (    FS e, High, Unavailable,  Bad),
>                (weaken e, Low,    Available,  Bad),
>                (    FS e, High,   Available,  Bad)] in
>   let tfres : List (State (S t))
>             = [(weaken e, Low,  Unavailable, Good),
>                (    FS e, High, Unavailable, Good),
>                (weaken e, Low,    Available, Good),
>                (    FS e, High,   Available, Good),
>                (weaken e, Low,  Unavailable,  Bad),
>                (    FS e, High, Unavailable,  Bad),
>                (weaken e, Low,    Available,  Bad),
>                (    FS e, High,   Available,  Bad)] in
>   let ftres : List (State (S t))
>             = [(weaken e, Low,  Unavailable, Good),
>                (    FS e, High, Unavailable, Good),
>                (weaken e, Low,    Available, Good),
>                (    FS e, High,   Available, Good),
>                (weaken e, Low,  Unavailable,  Bad),
>                (    FS e, High, Unavailable,  Bad),
>                (weaken e, Low,    Available,  Bad),
>                (    FS e, High,   Available,  Bad)] in
>   let ffres : List (State (S t))
>             = [(weaken e, Low,  Unavailable, Good),
>                (    FS e, High, Unavailable, Good),
>                (weaken e, Low,    Available, Good),
>                (    FS e, High,   Available, Good),
>                (weaken e, Low,  Unavailable,  Bad),
>                (    FS e, High, Unavailable,  Bad),
>                (weaken e, Low,    Available,  Bad),
>                (    FS e, High,   Available,  Bad)] in
>   case (t <= crN) of
>     True  => case (fromFin e <= crE) of
>                True  => ttres
>                False => tfres
>     False => case (fromFin e <= crE) of
>                True  => ftres
>                False => ffres
>
> -- The transition function: low emissions, unavailable GHG technologies, bad world
> SequentialDecisionProblems.CoreTheory.nexts t (e, Low, Unavailable, Bad) Low =
>   let ttres : List (State (S t))
>             = [(weaken e, Low,  Unavailable,  Bad),
>                (    FS e, High, Unavailable,  Bad),
>                (weaken e, Low,    Available,  Bad),
>                (    FS e, High,   Available,  Bad)] in
>   let tfres : List (State (S t))
>             = [(weaken e, Low,  Unavailable,  Bad),
>                (    FS e, High, Unavailable,  Bad),
>                (weaken e, Low,    Available,  Bad),
>                (    FS e, High,   Available,  Bad)] in
>   let ftres : List (State (S t))
>             = [(weaken e, Low,  Unavailable,  Bad),
>                (    FS e, High, Unavailable,  Bad),
>                (weaken e, Low,    Available,  Bad),
>                (    FS e, High,   Available,  Bad)] in
>   let ffres : List (State (S t))
>             = [(weaken e, Low,  Unavailable,  Bad),
>                (    FS e, High, Unavailable,  Bad),
>                (weaken e, Low,    Available,  Bad),
>                (    FS e, High,   Available,  Bad)] in
>   case (t <= crN) of
>     True  => case (fromFin e <= crE) of
>                True  => ttres
>                False => tfres
>     False => case (fromFin e <= crE) of
>                True  => ftres
>                False => ffres
> SequentialDecisionProblems.CoreTheory.nexts t (e, Low, Unavailable, Bad) High =
>   let ttres : List (State (S t))
>             = [(weaken e, Low,  Unavailable,  Bad),
>                (    FS e, High, Unavailable,  Bad),
>                (weaken e, Low,    Available,  Bad),
>                (    FS e, High,   Available,  Bad)] in
>   let tfres : List (State (S t))
>             = [(weaken e, Low,  Unavailable,  Bad),
>                (    FS e, High, Unavailable,  Bad),
>                (weaken e, Low,    Available,  Bad),
>                (    FS e, High,   Available,  Bad)] in
>   let ftres : List (State (S t))
>             = [(weaken e, Low,  Unavailable,  Bad),
>                (    FS e, High, Unavailable,  Bad),
>                (weaken e, Low,    Available,  Bad),
>                (    FS e, High,   Available,  Bad)] in
>   let ffres : List (State (S t))
>             = [(weaken e, Low,  Unavailable,  Bad),
>                (    FS e, High, Unavailable,  Bad),
>                (weaken e, Low,    Available,  Bad),
>                (    FS e, High,   Available,  Bad)] in
>   case (t <= crN) of
>     True  => case (fromFin e <= crE) of
>                True  => ttres
>                False => tfres
>     False => case (fromFin e <= crE) of
>                True  => ftres
>                False => 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 : List (State (S t))
>             = [(weaken e, Low,    Available, Good),
>                (    FS e, High,   Available, Good),
>                (weaken e, Low,    Available,  Bad),
>                (    FS e, High,   Available,  Bad)] in
>   let tfres : List (State (S t))
>             = [(weaken e, Low,    Available, Good),
>                (    FS e, High,   Available, Good),
>                (weaken e, Low,    Available,  Bad),
>                (    FS e, High,   Available,  Bad)] in
>   let ftres : List (State (S t))
>             = [(weaken e, Low,    Available, Good),
>                (    FS e, High,   Available, Good),
>                (weaken e, Low,    Available,  Bad),
>                (    FS e, High,   Available,  Bad)] in
>   let ffres : List (State (S t))
>             = [(weaken e, Low,    Available, Good),
>                (    FS e, High,   Available, Good),
>                (weaken e, Low,    Available,  Bad),
>                (    FS e, High,   Available,  Bad)] in
>   case (t <= crN) of
>     True  => case (fromFin e <= crE) of
>                True  => ttres
>                False => tfres
>     False => case (fromFin e <= crE) of
>                True  => ftres
>                False => ffres
> SequentialDecisionProblems.CoreTheory.nexts t (e, Low, Available, Good) High =
>   let ttres : List (State (S t))
>             = [(weaken e, Low,    Available, Good),
>                (    FS e, High,   Available, Good),
>                (weaken e, Low,    Available,  Bad),
>                (    FS e, High,   Available,  Bad)] in
>   let tfres : List (State (S t))
>             = [(weaken e, Low,    Available, Good),
>                (    FS e, High,   Available, Good),
>                (weaken e, Low,    Available,  Bad),
>                (    FS e, High,   Available,  Bad)] in
>   let ftres : List (State (S t))
>             = [(weaken e, Low,    Available, Good),
>                (    FS e, High,   Available, Good),
>                (weaken e, Low,    Available,  Bad),
>                (    FS e, High,   Available,  Bad)] in
>   let ffres : List (State (S t))
>             = [(weaken e, Low,    Available, Good),
>                (    FS e, High,   Available, Good),
>                (weaken e, Low,    Available,  Bad),
>                (    FS e, High,   Available,  Bad)] in
>   case (t <= crN) of
>     True  => case (fromFin e <= crE) of
>                True  => ttres
>                False => tfres
>     False => case (fromFin e <= crE) of
>                True  => ftres
>                False => ffres
>
> -- The transition function: low emissions, available GHG technologies, bad world
> SequentialDecisionProblems.CoreTheory.nexts t (e, Low, Available, Bad) Low =
>   let ttres : List (State (S t))
>             = [(weaken e, Low,    Available,  Bad),
>                (    FS e, High,   Available,  Bad)] in
>   let tfres : List (State (S t))
>             = [(weaken e, Low,    Available,  Bad),
>                (    FS e, High,   Available,  Bad)] in
>   let ftres : List (State (S t))
>             = [(weaken e, Low,    Available,  Bad),
>                (    FS e, High,   Available,  Bad)] in
>   let ffres : List (State (S t))
>             = [(weaken e, Low,    Available,  Bad),
>                (    FS e, High,   Available,  Bad)] in
>   case (t <= crN) of
>     True  => case (fromFin e <= crE) of
>                True  => ttres
>                False => tfres
>     False => case (fromFin e <= crE) of
>                True  => ftres
>                False => ffres
> SequentialDecisionProblems.CoreTheory.nexts t (e, Low, Available, Bad) High =
>   let ttres : List (State (S t))
>             = [(weaken e, Low,    Available,  Bad),
>                (    FS e, High,   Available,  Bad)] in
>   let tfres : List (State (S t))
>             = [(weaken e, Low,    Available,  Bad),
>                (    FS e, High,   Available,  Bad)] in
>   let ftres : List (State (S t))
>             = [(weaken e, Low,    Available,  Bad),
>                (    FS e, High,   Available,  Bad)] in
>   let ffres : List (State (S t))
>             = [(weaken e, Low,    Available,  Bad),
>                (    FS e, High,   Available,  Bad)] in
>   case (t <= crN) of
>     True  => case (fromFin e <= crE) of
>                True  => ttres
>                False => tfres
>     False => case (fromFin e <= crE) of
>                True  => ftres
>                False => 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

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

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

> -- 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

> -- 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

> -- 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

> -- 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 = average
> SequentialDecisionProblems.FullTheory.measMon = monotoneAverage

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)) -> SequentialDecisionProblems.CoreTheory.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 |List|, 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 Low (ne, av) where
>     ne : SequentialDecisionProblems.CoreTheory.NotEmpty (nexts t s Low)
>     ne = ?kika -- nonEmptyLemma (nexts t s Low)
>     av : SequentialDecisionProblems.CoreTheory.All (Viable {t = S t} n) (nexts t s Low)
>     av = viableLemma {t = S t} (nexts t s Low)

> 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 : (xs : List (State (S t))) -> SequentialDecisionProblems.CoreTheory.All (Reachable {t' = S t}) xs
>   all Nil = Nil
>   all (x :: xs) = () :: (all xs)

and decidability of |Reachable|:

> SequentialDecisionProblems.TabBackwardsInduction.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.TabBackwardsInduction.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} -> (x : State t) ->
>                                (ps : PolicySeq t n) ->
>                                M (StateCtrlSeq t n)
> adHocPossibleStateCtrlSeqs {t} {n = Z}    x  Nil        =
>   [(Nil x)]
> adHocPossibleStateCtrlSeqs {t} {n = S m}  x (p :: ps')  =
>   map ((MkSigma x y) ::) (mx' >>= f) where
>     y   :  Ctrl t x
>     y   =  ctrl (p x () ())
>     mx' :  M (State (S t))
>     mx' =  nexts t x y
>     f   :  State (S t) -> M (StateCtrlSeq (S t) m)
>     f x' = adHocPossibleStateCtrlSeqs {n = m} x' ps'

> adHocApp : {t, m, n : Nat} ->
>            StateCtrlSeq t m -> Policy (t + m) (S n) -> M (StateCtrlSeq t (S m))
> adHocApp {t} {m = Z} {n} (Nil {t} x) p = map (f . g) (nexts t x y) where
>   q : Policy t (S n)
>   q = replace {P = \ X => Policy X (S n)} (plusZeroRightNeutral t) p
>   y : Ctrl t x
>   y = ctrl (q x () ())
>   f : StateCtrlSeq (S t) Z -> StateCtrlSeq t (S Z)
>   f = ((MkSigma x y) ::)
>   g : State (S t) -> StateCtrlSeq (S t) Z
>   g x' = Nil x'
> adHocApp {t} {m = S m'} {n} (xy :: xys) p = map f (adHocApp xys q) where
>   f : StateCtrlSeq (S t) (S m') -> StateCtrlSeq t (S (S m'))
>   f = (xy ::)
>   q : Policy (S t + m') (S n)
>   q = replace {P = \ X => Policy X (S n)} (sym (plusSuccRightSucc t m')) p

> adHocExtend : {t, m, n : Nat} ->
>               M (StateCtrlSeq t m) -> PolicySeq (t + m) n -> M (StateCtrlSeq t (m + n))
> adHocExtend mxys {t} {m} {n = Z}         Nil  =
>   replace {P = \ X => M (StateCtrlSeq t X)} (sym (plusZeroRightNeutral m)) mxys
> adHocExtend mxys {t} {m} {n = S n'} (p :: ps) = s2 where
>   s1 : M (StateCtrlSeq t (plus (S m) n'))
>   s1 = adHocExtend mxys' (replace {P = \ X => PolicySeq X n'} (plusSuccRightSucc t m) ps) where
>     mxys' : M (StateCtrlSeq t (S m))
>     mxys' = mxys >>= f where
>       f : StateCtrlSeq t m ->  M (StateCtrlSeq t (S m))
>       f xys = adHocApp xys p
>   s2 : M (StateCtrlSeq t (plus m (S n')))
>   s2 = replace {P = \ X => M (StateCtrlSeq t X)} (plusSuccRightSucc m n') s1

> adHocPossibleStateCtrlSeqs1 : {t, n : Nat} -> (x : State t) ->
>                               (ps : PolicySeq t n) -> M (StateCtrlSeq t n)
> adHocPossibleStateCtrlSeqs1 {t} {n} x ps = s2 where
>
>   s1 : M (StateCtrlSeq t (Z + n))
>   s1 = adHocExtend [(Nil {t} x)] (replace {P = \ X => PolicySeq X n} (sym (plusZeroRightNeutral t)) ps)
>   s2 : M (StateCtrlSeq t n)
>   s2 = replace {P = \ X => M (StateCtrlSeq t X)} (plusZeroLeftNeutral n) s1

>
> using implementation ShowNonNegDouble
>
>   computation : { [STDIO] } Eff ()
>   computation =
>     do putStr ("enter number of steps:\n")
>        nSteps <- getNat
>        case (decidableViable {t = Z} nSteps (FZ, High, Unavailable, Good)) of
>          (Yes v) => do putStrLn ("computing optimal policies ...")
>                        -- ps   <- pure (backwardsInduction Z nSteps)
>                        ps   <- pure (tabTailRecursiveBackwardsInduction Z nSteps)
>                        putStrLn ("computing optimal controls ...")
>                        -- mxys <- pure (possibleStateCtrlSeqs (FZ, High, Unavailable, Good) () v ps)
>                        mxys <- pure (adHocPossibleStateCtrlSeqs (FZ, High, Unavailable, Good) ps)
>                        putStrLn "possible state-control sequences:"
>                        putStr "  "
>                        putStrLn (showlong mxys)
>                        mvs <- pure (possibleRewards' mxys)
>                        putStrLn "possible rewards:"
>                        putStr "  "
>                        putStrLn (show mvs)
>                        putStrLn ("done!")
>          (No _)  => putStrLn ("initial state non viable for " ++ cast {from = Int} (cast nSteps) ++ " steps")

> main : IO ()
> main = run computation

> {-

> ---}

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


text:
module Client.Action.Push

import Data.Maybe
import Client.Server
import Client.Util
import Data.Buffer
import Extra.Buffer
import Inigo.Async.Archive
import Inigo.Async.Fetch
import Inigo.Async.FS
import Inigo.Async.Promise
import Inigo.Package.Package
import Inigo.Async.Package
import Inigo.Util.Url.Url
import Toml
import System.Path

pushArchive : Server -> String -> Package -> String -> Promise ()
pushArchive server session pkg rootPath =
  do
    contents <- Inigo.Async.Archive.buildArchive pkg rootPath
    let url = toString (fromHostPath (host server) (postArchiveUrl pkg))
    ignore $ assertOk url $ request url "POST" contents [auth session]

pushReadme : Server -> String -> Package -> String -> Promise ()
pushReadme server session pkg contents =
  do
    let url = toString (fromHostPath (host server) (postReadmeUrl pkg))
    ignore $ assertOk url $ request url "POST" contents [auth session]

pushPackage : Server -> String -> Package -> Promise ()
pushPackage server session pkg =
  do
    let url = toString (fromHostPath (host server) (postPackageUrl pkg))
    ignore $ assertOk url $ request url "POST" (encode $ toToml pkg) [auth session]

maybePushReadme : Server -> String -> Maybe String -> Package -> Promise ()
maybePushReadme _ _ Nothing pkg = pure ()
maybePushReadme server session (Just path) pkg =
  do
    contents <- fs_readFile path
    pushReadme server session pkg contents

export
push : Server -> String -> String -> Promise ()
push server session packageFile =
  do
    pkg <- readPackage packageFile
    let rootPath = fromMaybe "" $ parent packageFile
    pushArchive server session pkg rootPath
    maybePushReadme server session (map (rootPath </>) (readme pkg)) pkg
    pushPackage server session pkg

ext: idr

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
module Network.Curl.Prim.Other

import Derive.Prim
%language ElabReflection

-------------------------------------------------
-- Other
-------------------------------------------------
-- curl_formadd
-- curl_formfree
-- curl_formget
-- curl_free
-- curl_getdate

-- curl_pushheader_byname
-- curl_pushheader_bynum
-- curl_share_cleanup
-- curl_share_init
-- curl_share_setopt
-- curl_share_strerror
-- curl_slist_append
-- curl_slist_free_all
-- curl_url
-- curl_url_cleanup
-- curl_url_dup
-- curl_url_get
-- curl_url_set
-- curl_version
-- curl_version_info
-------------------------------------------------

%runElab makeHasIO "curl_free" Export
          `[ %foreign "C:curl_free,libcurl,curl/curl.h"
             export
             prim_curl_free : Ptr Bits8 -> PrimIO () ] --`


text:
module Chapter5

import Naturality
import SumsAndProducts

%default total

Exercise_5_1_1_product_unit_as_subject : {ccc : CartesianClosedCategory} ->
    {x, a : CCC_object ccc} ->
    CCC_morphism {ccc} x a ->
    CCC_morphism {ccc} x (CCC_product {ccc} (CCC_terminal ccc) a)
Exercise_5_1_1_product_unit_as_subject f =
    CCC_morphism_product (fst (CCC_is_terminal ccc x)) f

Exercise_5_1_1_product_unit_subject_change : {ccc : CartesianClosedCategory} ->
    (a : CCC_object ccc) ->
    SubjectChange {cat=(CCC_cat ccc)} (CCC_product {ccc} (CCC_terminal ccc) a) a
Exercise_5_1_1_product_unit_subject_change {ccc} a x f =
    After (CCC_cat ccc) (CCC_second _ _) f

Exercise_5_1_1_product_unit_subject_change_is_natural :
    {ccc : CartesianClosedCategory} ->
    (a : CCC_object ccc) ->
    SubjectChangeIsNatural {cat=CCC_cat ccc}
        {subjectA=(CCC_product {ccc} (CCC_terminal ccc) a)}
        {subjectB=a}
        (Exercise_5_1_1_product_unit_subject_change {ccc} a)
Exercise_5_1_1_product_unit_subject_change_is_natural {ccc} a y x g =
    functionalExtensionality (\f => sym (Associativity _ _ _ _))

Exercise_5_1_1_product_unit_isomorphism : {ccc : CartesianClosedCategory} ->
    (a : CCC_object ccc) ->
    CCC_morphism {ccc} (CCC_product {ccc} (CCC_terminal ccc) a) a
Exercise_5_1_1_product_unit_isomorphism {ccc} a =
    SubjectChangeInducedMorphism (Exercise_5_1_1_product_unit_subject_change a)

{- This is not the only choice of arrow with this domain and codomain --
 - see Exercise 5.1.4 below. -}
Exercise_5_1_2 : {ccc : CartesianClosedCategory} -> (a, b : CCC_object ccc) ->
    CCC_morphism {ccc}
        (CCC_sum {ccc} b (CCC_product {ccc} a b))
        (CCC_product {ccc} (CCC_sum {ccc} (CCC_terminal ccc) a) b)
Exercise_5_1_2 {ccc} a b =
    CCC_morphism_product
        (CCC_morphism_sum
            ((CCC_left (CCC_terminal ccc) a) .* fst (CCC_is_terminal ccc b))
            ((CCC_right _ _) .* (CCC_first a b)))
        (CCC_morphism_sum
            (CCC_id b)
            (CCC_second a b))

Exercise_5_1_3 : {ccc : CartesianClosedCategory} -> (a, b : CCC_object ccc) ->
    CCC_morphism {ccc}
        (CCC_sum {ccc} b (CCC_product {ccc} a b))
        (CCC_product {ccc} (CCC_sum {ccc} (CCC_terminal ccc) a) b)
Exercise_5_1_3 a b =
    CCC_morphism_sum
        (CCC_morphism_product
            ((CCC_left (CCC_terminal ccc) a) .* fst (CCC_is_terminal ccc b))
            (CCC_id b))
        (CCC_morphism_product
            ((CCC_right _ _) .* (CCC_first a b))
            (CCC_second a b))

Exercise_5_1_4_maybe_AB : {a, b : Type} -> Either b (a, b) -> (Maybe a, b)
Exercise_5_1_4_maybe_AB (Left y) = (Nothing, y)
Exercise_5_1_4_maybe_AB (Right (x, y)) = (Just x, y)

{- The type signature for Exercise 5.1.4 allows a bit of leeway --
 - but not much: -}
Exercise_5_1_4_maybe_AB_alternate :
    {a, b : Type} -> Either b (a, b) -> (Maybe a, b)
{- We have no choice aboue this one:  we have no witness for type "a", so the
 - only "Maybe a" we can come up with is "Nothing". And we have only one
 - witness for type "b", so we have to choose that. -}
Exercise_5_1_4_maybe_AB_alternate (Left y) = (Nothing, y)
{- Here we do have one alternative: even though we have a witness for type "a"
 - in this case, we could choose not to use it, and to return "Nothing"
 - anyway. -}
Exercise_5_1_4_maybe_AB_alternate (Right (_, y)) = (Nothing, y)

max_stars_repo_name: rokopt/dao-fp-exercises

max_issues_repo_name: rokopt/dao-fp-exercises

max_forks_repo_name: rokopt/dao-fp-exercises


text:
public export
record Rec where
  x : Int

f : Rec
f = {x := 4} ?foo

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
{-
Write a function, maxMaybe : Ord a => Maybe a -> Maybe a -> Maybe a,
that returns the larger of the two inputs, or Nothing if both inputs
are Nothing.

For example:
> maxMaybe (Just 4) (Just 5)
Just 5 : Maybe Integer

> maxMaybe (Just 4) Nothing
Just 4 : Maybe Integer
 -}

maxMaybe : Ord a => Maybe a -> Maybe a -> Maybe a
maxMaybe Nothing y = y
maxMaybe x y = if x > y then x else y -- Maybe is defined as Ord in the Prelude ;)


text:
module A.Path.Of.Dires.First

%default total

public export
data Tree : Type -> Type where
  Leaf : a -> Tree a
  Node : Tree a -> Tree a -> Tree a


text:
module Prelude.IO

import Builtin
import PrimIO
import Prelude.Basics
import Prelude.Interfaces
import Prelude.Show

%default total

--------
-- IO --
--------

public export
Functor IO where
  map f io = io_bind io $ io_pure . f

%inline
public export
Applicative IO where
  pure x = io_pure x
  f <*> a
      = io_bind f (\f' =>
          io_bind a (\a' =>
            io_pure (f' a')))

%inline
public export
Monad IO where
  b >>= k = io_bind b k

public export
interface Monad io => HasIO io where
  constructor MkHasIO
  liftIO : IO a -> io a

public export
interface Monad io => HasLinearIO io where
  constructor MkHasLinearIO
  liftIO1 : (1 _ : IO a) -> io a

public export %inline
HasLinearIO IO where
  liftIO1 x = x

public export %inline
HasLinearIO io => HasIO io where
  liftIO x = liftIO1 x

export %inline
primIO : HasIO io => (fn : (1 x : %World) -> IORes a) -> io a
primIO op = liftIO (fromPrim op)

export %inline
primIO1 : HasLinearIO io => (1 fn : (1 x : %World) -> IORes a) -> io a
primIO1 op = liftIO1 (fromPrim op)

%extern
prim__onCollectAny : AnyPtr -> (AnyPtr -> PrimIO ()) -> PrimIO GCAnyPtr
%extern
prim__onCollect : Ptr t -> (Ptr t -> PrimIO ()) -> PrimIO (GCPtr t)

export
onCollectAny : HasIO io => AnyPtr -> (AnyPtr -> IO ()) -> io GCAnyPtr
onCollectAny ptr c = primIO (prim__onCollectAny ptr (\x => toPrim (c x)))

export
onCollect : HasIO io => Ptr t -> (Ptr t -> IO ()) -> io (GCPtr t)
onCollect ptr c = primIO (prim__onCollect ptr (\x => toPrim (c x)))

%foreign "C:idris2_getString, libidris2_support, idris_support.h"
         "javascript:lambda:x=>x"
         "jvm:getString,io/github/mmhelloworld/idrisjvm/runtime/Objects"
export
prim__getString : Ptr String -> String

%foreign "C:putchar,libc 6"
         "jvm:putChar(char void),io/github/mmhelloworld/idrisjvm/runtime/Console"
prim__putChar : Char -> (1 x : %World) -> IORes ()
%foreign "C:getchar,libc 6"
         "jvm:getChar(java/lang/Object char),io/github/mmhelloworld/idrisjvm/runtime/Console"
%extern prim__getChar : (1 x : %World) -> IORes Char

%foreign "C:idris2_getStr, libidris2_support, idris_support.h"
         "node:support:getStr,support_system_file"
         "jvm:getString(java/lang/Object java/lang/String),io/github/mmhelloworld/idrisjvm/runtime/Console"
prim__getStr : PrimIO String

%foreign "C:idris2_putStr, libidris2_support, idris_support.h"
         "node:lambda:x=>process.stdout.write(x)"
         "browser:lambda:x=>console.log(x)"
         "jvm:printString,io/github/mmhelloworld/idrisjvm/runtime/Console"
prim__putStr : String -> PrimIO ()

||| Output a string to stdout without a trailing newline.
export
putStr : HasIO io => String -> io ()
putStr str = primIO (prim__putStr str)

||| Output a string to stdout with a trailing newline.
export
putStrLn : HasIO io => String -> io ()
putStrLn str = putStr (prim__strAppend str "\n")

||| Read one line of input from stdin, without the trailing newline.
export
getLine : HasIO io => io String
getLine = primIO prim__getStr

||| Write one single-byte character to stdout.
export
putChar : HasIO io => Char -> io ()
putChar c = primIO (prim__putChar c)

||| Write one multi-byte character to stdout, with a trailing newline.
export
putCharLn : HasIO io => Char -> io ()
putCharLn c = putStrLn (prim__cast_CharString c)

||| Read one single-byte character from stdin.
export
getChar : HasIO io => io Char
getChar = primIO prim__getChar

%foreign "scheme:blodwen-thread"
         "jvm:fork(java/util/function/Function#apply#java/lang/Object#java/lang/Object java/util/concurrent/ForkJoinTask),io/github/mmhelloworld/idrisjvm/runtime/Runtime"
export
prim__fork : (1 prog : PrimIO ()) -> PrimIO ThreadID

export
fork : (1 prog : IO ()) -> IO ThreadID
fork act = fromPrim (prim__fork (toPrim act))

%foreign "scheme:blodwen-thread-wait"
         "jvm:await(java/util/concurrent/ForkJoinTask void),io/github/mmhelloworld/idrisjvm/runtime/Runtime"
export
prim__threadWait : (1 threadID : ThreadID) -> PrimIO ()

export
threadWait : (1 threadID : ThreadID) -> IO ()
threadWait threadID = fromPrim (prim__threadWait threadID)

||| Output something showable to stdout, without a trailing newline.
export
print : (HasIO io, Show a) => a -> io ()
print x = putStr $ show x

||| Output something showable to stdout, with a trailing newline.
export
printLn : (HasIO io, Show a) => a -> io ()
printLn x = putStrLn $ show x


text:
module System.IO.Handle.Windows

%default total

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

%foreign "scheme,chez:(foreign-procedure #f \"GetStdHandle\" (unsigned-32) void*)"
         "javascript:lambda:(x) => 0"
prim__win_GetStdHandle : Bits32 -> PrimIO AnyPtr

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

public export data Handle = MkHandle AnyPtr

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

export getStdin : HasIO io => io Handle
getStdin = pure $ MkHandle !(primIO $ prim__win_GetStdHandle $ cast (-10))

export getStdout : HasIO io => io Handle
getStdout = pure $ MkHandle !(primIO $ prim__win_GetStdHandle $ cast (-11))

export getStderr : HasIO io => io Handle
getStderr = pure $ MkHandle !(primIO $ prim__win_GetStdHandle $ cast (-13))

-- ---------------------------------------------------------------------------
-- vim: tw=80 sw=2 expandtab :


text:
module Main

import Data.Vect

data DataStore: Type where
    MkData: (size: Nat) -> (items: Vect size String) -> DataStore

size: DataStore -> Nat
size (MkData size' items') = size'

items: (store: DataStore) -> Vect (size store) String
items (MkData size' items') = items'

addToStore: DataStore -> String -> DataStore
addToStore (MkData size items) newItem = MkData _ (addToData items)
    where
        addToData: Vect old String -> Vect (S old) String
        addToData [] = [newItem]
        addToData (x :: xs) = x :: addToData xs

data Command = Add String
						 | Get Integer
						 | Size
             | Quit

parseCommand : (cmd : String) -> (args : String) -> Maybe Command
parseCommand "add" str = Just (Add str)
parseCommand "get" val = case all isDigit (unpack val) of
	True  => Just(Get(cast val))
	False => Nothing
parseCommand "size" "" = Just Size
parseCommand "quit" "" = Just Quit
parseCommand _ _ = Nothing

parse: String -> Maybe Command
parse input = case span (/= ' ') input of
    (cmd, args) => parseCommand cmd (ltrim args)

getEntry : (pos : Integer) -> (store : DataStore) -> Maybe (String, DataStore)
getEntry pos store =
	let
		currItems = items store
	in
		case integerToFin pos (size store) of
			Nothing => Just("Out of range\n", store)
			Just id => Just((index id currItems) ++ "\n", store)

total processCommand : (cmd : Command) -> (store : DataStore) -> Maybe (String, DataStore)
processCommand (Add item) store =
	let
		newStore = addToStore store item
		newId = show (size store)
	in
		Just("ID: " ++ newId ++ "\n", newStore)
processCommand (Get pos) store = getEntry pos store
processCommand Size store = Just("Size: " ++ show (size store) ++ "\n", store)
processCommand Quit store = Nothing

processInput : DataStore -> String -> Maybe (String, DataStore)
processInput store input = case parse input of
    Nothing => Just("Invalid command\n", store)
    Just cmd => processCommand cmd store

main : IO ()
main = replWith (MkData _ []) ":>> " processInput

max_stars_repo_name: coffius/idris-exercises

max_issues_repo_name: coffius/idris-exercises

max_forks_repo_name: coffius/idris-exercises


text:
||| FFI definitions for the  Flutter.FFI API.
module Flutter.FFI

import Dart.Core
import Dart.FFI

mutual
  %inline
  public export
  Key : Type
  Key = Struct "Key,package:flutter/foundation.dart" []

  %inline
  public export
  TextStyle : Type
  TextStyle = Struct "TextStyle,package:flutter/painting.dart" [
    ("textAlign", TextAlign)
  ]

  %inline
  public export
  AlignmentGeometry : Type
  AlignmentGeometry = Struct "AlignmentGeometry,package:flutter/painting.dart" []

  %inline
  public export
  Alignment : Type
  Alignment = Struct "Alignment,package:flutter/painting.dart" []

  %inline
  public export
  MaterialColor : Type
  MaterialColor = Struct "MaterialColor,package:flutter/material.dart" []

  %inline
  public export
  Colors : Type
  Colors = Struct "Colors,package:flutter/material.dart" []

  %inline
  public export
  CircularProgressIndicator : Type
  CircularProgressIndicator = Struct "CircularProgressIndicator,package:flutter/material.dart" []

  %inline
  public export
  VisualDensity : Type
  VisualDensity = Struct "VisualDensity,package:flutter/material.dart" []

  %inline
  public export
  TextTheme : Type
  TextTheme = Struct "TextTheme,package:flutter/material.dart" [
    ("headline1", TextStyle),
    ("headline2", TextStyle),
    ("headline3", TextStyle),
    ("headline4", TextStyle)
  ]

  %inline
  public export
  Theme : Type
  Theme = Struct "Theme,package:flutter/material.dart" []

  %inline
  public export
  ThemeData : Type
  ThemeData = Struct "ThemeData,package:flutter/material.dart" [
    ("textTheme", TextTheme)
  ]

  %inline
  public export
  Scaffold : Type
  Scaffold = Struct "Scaffold,package:flutter/material.dart" []

  %inline
  public export
  AppBar : Type
  AppBar = Struct "AppBar,package:flutter/material.dart" []

  %inline
  public export
  Icons : Type
  Icons = Struct "Icons,package:flutter/material.dart" []

  %inline
  public export
  IconButton : Type
  IconButton = Struct "IconButton,package:flutter/material.dart" []

  %inline
  public export
  FloatingActionButton : Type
  FloatingActionButton = Struct "FloatingActionButton,package:flutter/material.dart" []

  %inline
  public export
  Slider : Type
  Slider = Struct "Slider,package:flutter/material.dart" []

  %inline
  public export
  MaterialApp : Type
  MaterialApp = Struct "MaterialApp,package:flutter/material.dart" []

  %inline
  public export
  MainAxisAlignment : Type
  MainAxisAlignment = Struct "MainAxisAlignment,package:flutter/widgets.dart" []

  %inline
  public export
  IconData : Type
  IconData = Struct "IconData,package:flutter/widgets.dart" []

  %inline
  public export
  Icon : Type
  Icon = Struct "Icon,package:flutter/widgets.dart" []

  %inline
  public export
  Widget : Type
  Widget = Struct "Widget,package:flutter/widgets.dart" []

  %inline
  public export
  BuildContext : Type
  BuildContext = Struct "BuildContext,package:flutter/widgets.dart" []

  %inline
  public export
  Center : Type
  Center = Struct "Center,package:flutter/widgets.dart" []

  %inline
  public export
  Column : Type
  Column = Struct "Column,package:flutter/widgets.dart" []

  %inline
  public export
  Expanded : Type
  Expanded = Struct "Expanded,package:flutter/widgets.dart" []

  %inline
  public export
  Row : Type
  Row = Struct "Row,package:flutter/widgets.dart" []

  %inline
  public export
  Text : Type
  Text = Struct "Text,package:flutter/widgets.dart" []

  %inline
  public export
  GestureDetector : Type
  GestureDetector = Struct "GestureDetector,package:flutter/widgets.dart" []

  %inline
  public export
  CustomPaint : Type
  CustomPaint = Struct "CustomPaint,package:flutter/widgets.dart" []

  %inline
  public export
  CustomPainter : Type
  CustomPainter = Struct "CustomPainter,package:flutter/widgets.dart" []

  %inline
  public export
  AppLifecycleState : Type
  AppLifecycleState = Struct "AppLifecycleState,dart:ui" []

  %inline
  public export
  Color : Type
  Color = Struct "Color,dart:ui" []

  %inline
  public export
  Canvas : Type
  Canvas = Struct "Canvas,dart:ui" []

  %inline
  public export
  PaintingStyle : Type
  PaintingStyle = Struct "PaintingStyle,dart:ui" []

  %inline
  public export
  Paint : Type
  Paint = Struct "Paint,dart:ui" [
    ("style", PaintingStyle),
    ("strokeWidth", Double)
  ]

  %inline
  public export
  Offset : Type
  Offset = Struct "Offset,dart:ui" [
    ("dx", Double),
    ("dy", Double)
  ]

  %inline
  public export
  Size : Type
  Size = Struct "Size,dart:ui" [
    ("width", Double),
    ("height", Double)
  ]

  %inline
  public export
  Path : Type
  Path = Struct "Path,dart:ui" []

  %inline
  public export
  Velocity : Type
  Velocity = Struct "Velocity,dart:ui" [
    ("pixelsPerSecond", Offset)
  ]

  %inline
  public export
  TextAlign : Type
  TextAlign = Struct "TextAlign,dart:ui" []

  %inline
  public export
  TapDownDetails : Type
  TapDownDetails = Struct "TapDownDetails,package:flutter/gestures.dart" [
    ("globalPosition", Offset),
    ("localPosition", Offset)
  ]

  %inline
  public export
  TapUpDetails : Type
  TapUpDetails = Struct "TapUpDetails,package:flutter/gestures.dart" [
    ("globalPosition", Offset),
    ("localPosition", Offset)
  ]

  %inline
  public export
  LongPressStartDetails : Type
  LongPressStartDetails = Struct "LongPressStartDetails,package:flutter/gestures.dart" [
    ("globalPosition", Offset),
    ("localPosition", Offset)
  ]

  %inline
  public export
  LongPressMoveUpdateDetails : Type
  LongPressMoveUpdateDetails = Struct "LongPressMoveUpdateDetails,package:flutter/gestures.dart" [
    ("localOffsetFromOrigin", Offset),
    ("localPosition", Offset)
  ]

  %inline
  public export
  LongPressEndDetails : Type
  LongPressEndDetails = Struct "LongPressEndDetails,package:flutter/gestures.dart" [
    ("globalPosition", Offset),
    ("localPosition", Offset)
  ]

namespace TextStyle
  export
  textAlign : TextStyle -> TextAlign
  textAlign this = getField this "textAlign"

namespace Alignment
  export
  IsAssignableFrom AlignmentGeometry Alignment where

  export
  %foreign "Dart:const Alignment.centerLeft,package:flutter/painting.dart"
  centerLeft : Alignment

  export
  %foreign "Dart:const Alignment.centerRight,package:flutter/painting.dart"
  centerRight : Alignment

namespace Colors
  export
  %foreign "Dart:const Colors.black,package:flutter/material.dart"
  black : MaterialColor

  export
  %foreign "Dart:const Colors.blue,package:flutter/material.dart"
  blue : MaterialColor

  export
  %foreign "Dart:const Colors.brown,package:flutter/material.dart"
  brown : MaterialColor

  export
  %foreign "Dart:const Colors.cyan,package:flutter/material.dart"
  cyan : MaterialColor

  export
  %foreign "Dart:const Colors.green,package:flutter/material.dart"
  green : MaterialColor

  export
  %foreign "Dart:const Colors.grey,package:flutter/material.dart"
  grey : MaterialColor

  export
  %foreign "Dart:const Colors.purple,package:flutter/material.dart"
  purple : MaterialColor

  export
  %foreign "Dart:const Colors.red,package:flutter/material.dart"
  red : MaterialColor

  export
  %foreign "Dart:const Colors.transparent,package:flutter/material.dart"
  transparent : MaterialColor

  export
  %foreign "Dart:const Colors.white,package:flutter/material.dart"
  white : MaterialColor

  export
  %foreign "Dart:const Colors.yellow,package:flutter/material.dart"
  yellow : MaterialColor

namespace CircularProgressIndicator
  export
  IsAssignableFrom Widget CircularProgressIndicator where

  namespace New
    data Tag : Type where

    %inline
    public export
    key : Parameter CircularProgressIndicator.New.Tag
    key = mkParameter "key" Key
    %inline
    public export
    NamedParameters : Type
    NamedParameters = Parameters [CircularProgressIndicator.New.key]

  %inline
  public export
  new : HasIO io => CircularProgressIndicator.New.NamedParameters -> io CircularProgressIndicator
  new  ps = primIO $ prim__dart_new CircularProgressIndicator [] ps

namespace VisualDensity
  export
  %foreign "Dart:const VisualDensity.adaptivePlatformDensity,package:flutter/material.dart"
  adaptivePlatformDensity : VisualDensity

namespace TextTheme
  export
  headline1 : TextTheme -> TextStyle
  headline1 this = getField this "headline1"

  export
  headline2 : TextTheme -> TextStyle
  headline2 this = getField this "headline2"

  export
  headline3 : TextTheme -> TextStyle
  headline3 this = getField this "headline3"

  export
  headline4 : TextTheme -> TextStyle
  headline4 this = getField this "headline4"

namespace Theme
  %foreign "Dart:Theme.of,package:flutter/material.dart"
  prim__of : (context : BuildContext) -> PrimIO ThemeData

  export
  of_ : HasIO io => (context : BuildContext) -> io ThemeData
  of_ context = primIO $ prim__of context

namespace ThemeData
  namespace New
    data Tag : Type where

    %inline
    public export
    primarySwatch : Parameter ThemeData.New.Tag
    primarySwatch = mkParameter "primarySwatch" MaterialColor

    %inline
    public export
    visualDensity : Parameter ThemeData.New.Tag
    visualDensity = mkParameter "visualDensity" VisualDensity
    %inline
    public export
    NamedParameters : Type
    NamedParameters = Parameters [ThemeData.New.primarySwatch, ThemeData.New.visualDensity]

  %inline
  public export
  new : HasIO io => ThemeData.New.NamedParameters -> io ThemeData
  new  ps = primIO $ prim__dart_new ThemeData [] ps

  export
  textTheme : ThemeData -> TextTheme
  textTheme this = getField this "textTheme"

namespace Scaffold
  export
  IsAssignableFrom Widget Scaffold where

  namespace New
    data Tag : Type where

    %inline
    public export
    appBar : Parameter Scaffold.New.Tag
    appBar = mkParameter "appBar" Widget

    %inline
    public export
    body : Parameter Scaffold.New.Tag
    body = mkParameter "body" Widget

    %inline
    public export
    floatingActionButton : Parameter Scaffold.New.Tag
    floatingActionButton = mkParameter "floatingActionButton" Widget
    %inline
    public export
    NamedParameters : Type
    NamedParameters = Parameters [Scaffold.New.appBar, Scaffold.New.body, Scaffold.New.floatingActionButton]

  %inline
  public export
  new : HasIO io => Scaffold.New.NamedParameters -> io Scaffold
  new  ps = primIO $ prim__dart_new Scaffold [] ps

namespace AppBar
  export
  IsAssignableFrom Widget AppBar where

  namespace New
    data Tag : Type where

    %inline
    public export
    title : Parameter AppBar.New.Tag
    title = mkParameter "title" Widget
    %inline
    public export
    NamedParameters : Type
    NamedParameters = Parameters [AppBar.New.title]

  %inline
  public export
  new : HasIO io => AppBar.New.NamedParameters -> io AppBar
  new  ps = primIO $ prim__dart_new AppBar [] ps

namespace Icons
  export
  %foreign "Dart:const Icons.add,package:flutter/material.dart"
  add : IconData

  export
  %foreign "Dart:const Icons.add_circle_outline,package:flutter/material.dart"
  add_circle_outline : IconData

  export
  %foreign "Dart:const Icons.remove,package:flutter/material.dart"
  remove : IconData

  export
  %foreign "Dart:const Icons.remove_circle_outline,package:flutter/material.dart"
  remove_circle_outline : IconData

  export
  %foreign "Dart:const Icons.play_arrow,package:flutter/material.dart"
  play_arrow : IconData

  export
  %foreign "Dart:const Icons.stop,package:flutter/material.dart"
  stop : IconData

  export
  %foreign "Dart:const Icons.stop_circle,package:flutter/material.dart"
  stop_circle : IconData

  export
  %foreign "Dart:const Icons.stop_circle_outlined,package:flutter/material.dart"
  stop_circle_outlined : IconData

  export
  %foreign "Dart:const Icons.stop_circle_rounded,package:flutter/material.dart"
  stop_circle_rounded : IconData

  export
  %foreign "Dart:const Icons.stop_circle_sharp,package:flutter/material.dart"
  stop_circle_sharp : IconData

  export
  %foreign "Dart:const Icons.stop_outlined,package:flutter/material.dart"
  stop_outlined : IconData

  export
  %foreign "Dart:const Icons.stop_rounded,package:flutter/material.dart"
  stop_rounded : IconData

namespace IconButton
  export
  IsAssignableFrom Widget IconButton where

  namespace New
    data Tag : Type where

    %inline
    public export
    onPressed : Parameter IconButton.New.Tag
    onPressed = mkParameter "onPressed" (IO ())

    %inline
    public export
    tooltip : Parameter IconButton.New.Tag
    tooltip = mkParameter "tooltip" String

    %inline
    public export
    icon : Parameter IconButton.New.Tag
    icon = mkParameter "icon" Widget

    %inline
    public export
    alignment : Parameter IconButton.New.Tag
    alignment = mkParameter "alignment" AlignmentGeometry
    %inline
    public export
    NamedParameters : Type
    NamedParameters = Parameters [ IconButton.New.onPressed
    , IconButton.New.tooltip
    , IconButton.New.icon
    , IconButton.New.alignment ]

  %inline
  public export
  new : HasIO io => IconButton.New.NamedParameters -> io IconButton
  new  ps = primIO $ prim__dart_new IconButton [] ps

namespace FloatingActionButton
  export
  IsAssignableFrom Widget FloatingActionButton where

  namespace New
    data Tag : Type where

    %inline
    public export
    onPressed : Parameter FloatingActionButton.New.Tag
    onPressed = mkParameter "onPressed" (IO ())

    %inline
    public export
    tooltip : Parameter FloatingActionButton.New.Tag
    tooltip = mkParameter "tooltip" String

    %inline
    public export
    child : Parameter FloatingActionButton.New.Tag
    child = mkParameter "child" Widget
    %inline
    public export
    NamedParameters : Type
    NamedParameters = Parameters [ FloatingActionButton.New.onPressed
    , FloatingActionButton.New.tooltip
    , FloatingActionButton.New.child ]

  %inline
  public export
  new : HasIO io => FloatingActionButton.New.NamedParameters -> io FloatingActionButton
  new  ps = primIO $ prim__dart_new FloatingActionButton [] ps

namespace Slider
  export
  IsAssignableFrom Widget Slider where

  namespace New
    data Tag : Type where

    %inline
    public export
    value : Parameter Slider.New.Tag
    value = mkParameter "value" Double

    %inline
    public export
    onChanged : Parameter Slider.New.Tag
    onChanged = mkParameter "onChanged" (Double -> IO ())

    %inline
    public export
    onChangeStart : Parameter Slider.New.Tag
    onChangeStart = mkParameter "onChangeStart" (Double -> IO ())

    %inline
    public export
    onChangeEnd : Parameter Slider.New.Tag
    onChangeEnd = mkParameter "onChangeEnd" (Double -> IO ())

    %inline
    public export
    min : Parameter Slider.New.Tag
    min = mkParameter "min" Double

    %inline
    public export
    max : Parameter Slider.New.Tag
    max = mkParameter "max" Double

    %inline
    public export
    divisions : Parameter Slider.New.Tag
    divisions = mkParameter "divisions" Int

    %inline
    public export
    label : Parameter Slider.New.Tag
    label = mkParameter "label" String
    %inline
    public export
    NamedParameters : Type
    NamedParameters = Parameters [ Slider.New.value
    , Slider.New.onChanged
    , Slider.New.onChangeStart
    , Slider.New.onChangeEnd
    , Slider.New.min
    , Slider.New.max
    , Slider.New.divisions
    , Slider.New.label ]

  %inline
  public export
  new : HasIO io => Slider.New.NamedParameters -> io Slider
  new  ps = primIO $ prim__dart_new Slider [] ps

namespace MaterialApp
  export
  IsAssignableFrom Widget MaterialApp where

  namespace New
    data Tag : Type where

    %inline
    public export
    title : Parameter MaterialApp.New.Tag
    title = mkParameter "title" String

    %inline
    public export
    home : Parameter MaterialApp.New.Tag
    home = mkParameter "home" Widget

    %inline
    public export
    theme : Parameter MaterialApp.New.Tag
    theme = mkParameter "theme" ThemeData
    %inline
    public export
    NamedParameters : Type
    NamedParameters = Parameters [MaterialApp.New.title, MaterialApp.New.home, MaterialApp.New.theme]

  %inline
  public export
  new : HasIO io => MaterialApp.New.NamedParameters -> io MaterialApp
  new  ps = primIO $ prim__dart_new MaterialApp [] ps

namespace MainAxisAlignment
  export
  %foreign "Dart:const MainAxisAlignment.start,package:flutter/widgets.dart"
  start : MainAxisAlignment
  export
  %foreign "Dart:const MainAxisAlignment.end,package:flutter/widgets.dart"
  end : MainAxisAlignment
  export
  %foreign "Dart:const MainAxisAlignment.center,package:flutter/widgets.dart"
  center : MainAxisAlignment
  export
  %foreign "Dart:const MainAxisAlignment.spaceBetween,package:flutter/widgets.dart"
  spaceBetween : MainAxisAlignment
  export
  %foreign "Dart:const MainAxisAlignment.spaceAround,package:flutter/widgets.dart"
  spaceAround : MainAxisAlignment
  export
  %foreign "Dart:const MainAxisAlignment.spaceEvenly,package:flutter/widgets.dart"
  spaceEvenly : MainAxisAlignment

namespace Icon
  export
  IsAssignableFrom Widget Icon where

  namespace New
    data Tag : Type where

    %inline
    public export
    key : Parameter Icon.New.Tag
    key = mkParameter "key" Key
    %inline
    public export
    NamedParameters : Type
    NamedParameters = Parameters [Icon.New.key]

  %inline
  public export
  new : HasIO io => (icon : IconData) -> Icon.New.NamedParameters -> io Icon
  new icon ps = primIO $ prim__dart_new Icon [icon] ps

namespace Center
  export
  IsAssignableFrom Widget Center where

  namespace New
    data Tag : Type where

    %inline
    public export
    child : Parameter Center.New.Tag
    child = mkParameter "child" Widget
    %inline
    public export
    NamedParameters : Type
    NamedParameters = Parameters [Center.New.child]

  %inline
  public export
  new : HasIO io => Center.New.NamedParameters -> io Center
  new  ps = primIO $ prim__dart_new Center [] ps

namespace Column
  export
  IsAssignableFrom Widget Column where

  namespace New
    data Tag : Type where

    %inline
    public export
    children : Parameter Column.New.Tag
    children = mkParameter "children" (DartList Widget)

    %inline
    public export
    mainAxisAlignment : Parameter Column.New.Tag
    mainAxisAlignment = mkParameter "mainAxisAlignment" MainAxisAlignment
    %inline
    public export
    NamedParameters : Type
    NamedParameters = Parameters [Column.New.children, Column.New.mainAxisAlignment]

  %inline
  public export
  new : HasIO io => Column.New.NamedParameters -> io Column
  new  ps = primIO $ prim__dart_new Column [] ps

namespace Expanded
  export
  IsAssignableFrom Widget Expanded where

  namespace New
    data Tag : Type where

    %inline
    public export
    child : Parameter Expanded.New.Tag
    child = mkParameter "child" Widget
    %inline
    public export
    NamedParameters : Type
    NamedParameters = Parameters [Expanded.New.child]

  %inline
  public export
  new : HasIO io => Expanded.New.NamedParameters -> io Expanded
  new  ps = primIO $ prim__dart_new Expanded [] ps

namespace Row
  export
  IsAssignableFrom Widget Row where

  namespace New
    data Tag : Type where

    %inline
    public export
    children : Parameter Row.New.Tag
    children = mkParameter "children" (DartList Widget)

    %inline
    public export
    mainAxisAlignment : Parameter Row.New.Tag
    mainAxisAlignment = mkParameter "mainAxisAlignment" MainAxisAlignment
    %inline
    public export
    NamedParameters : Type
    NamedParameters = Parameters [Row.New.children, Row.New.mainAxisAlignment]

  %inline
  public export
  new : HasIO io => Row.New.NamedParameters -> io Row
  new  ps = primIO $ prim__dart_new Row [] ps

namespace Text
  export
  IsAssignableFrom Widget Text where

  namespace New
    data Tag : Type where

    %inline
    public export
    textScaleFactor : Parameter Text.New.Tag
    textScaleFactor = mkParameter "textScaleFactor" Double

    %inline
    public export
    style : Parameter Text.New.Tag
    style = mkParameter "style" TextStyle

    %inline
    public export
    textAlign : Parameter Text.New.Tag
    textAlign = mkParameter "textAlign" TextAlign
    %inline
    public export
    NamedParameters : Type
    NamedParameters = Parameters [Text.New.textScaleFactor, Text.New.style, Text.New.textAlign]

  %inline
  public export
  new : HasIO io => (text : String) -> Text.New.NamedParameters -> io Text
  new text ps = primIO $ prim__dart_new Text [text] ps

namespace GestureDetector
  export
  IsAssignableFrom Widget GestureDetector where

  namespace New
    data Tag : Type where

    %inline
    public export
    key : Parameter GestureDetector.New.Tag
    key = mkParameter "key" Key

    %inline
    public export
    child : Parameter GestureDetector.New.Tag
    child = mkParameter "child" Widget

    %inline
    public export
    onTapDown : Parameter GestureDetector.New.Tag
    onTapDown = mkParameter "onTapDown" (TapDownDetails -> IO ())

    %inline
    public export
    onTapUp : Parameter GestureDetector.New.Tag
    onTapUp = mkParameter "onTapUp" (TapUpDetails -> IO ())

    %inline
    public export
    onTap : Parameter GestureDetector.New.Tag
    onTap = mkParameter "onTap" (IO ())

    %inline
    public export
    onTapCancel : Parameter GestureDetector.New.Tag
    onTapCancel = mkParameter "onTapCancel" (IO ())

    %inline
    public export
    onSecondaryTap : Parameter GestureDetector.New.Tag
    onSecondaryTap = mkParameter "onSecondaryTap" (IO ())

    %inline
    public export
    onSecondaryTapCancel : Parameter GestureDetector.New.Tag
    onSecondaryTapCancel = mkParameter "onSecondaryTapCancel" (IO ())

    %inline
    public export
    onDoubleTap : Parameter GestureDetector.New.Tag
    onDoubleTap = mkParameter "onDoubleTap" (IO ())

    %inline
    public export
    onDoubleTapCancel : Parameter GestureDetector.New.Tag
    onDoubleTapCancel = mkParameter "onDoubleTapCancel" (IO ())

    %inline
    public export
    onSecondaryTapDown : Parameter GestureDetector.New.Tag
    onSecondaryTapDown = mkParameter "onSecondaryTapDown" (TapDownDetails -> IO ())

    %inline
    public export
    onSecondaryTapUp : Parameter GestureDetector.New.Tag
    onSecondaryTapUp = mkParameter "onSecondaryTapUp" (TapUpDetails -> IO ())

    %inline
    public export
    onLongPress : Parameter GestureDetector.New.Tag
    onLongPress = mkParameter "onLongPress" (IO ())

    %inline
    public export
    onLongPressStart : Parameter GestureDetector.New.Tag
    onLongPressStart = mkParameter "onLongPressStart" (LongPressStartDetails -> IO ())

    %inline
    public export
    onLongPressMoveUpdate : Parameter GestureDetector.New.Tag
    onLongPressMoveUpdate = mkParameter "onLongPressMoveUpdate" (LongPressMoveUpdateDetails -> IO ())

    %inline
    public export
    onLongPressEnd : Parameter GestureDetector.New.Tag
    onLongPressEnd = mkParameter "onLongPressEnd" (LongPressEndDetails -> IO ())
    %inline
    public export
    NamedParameters : Type
    NamedParameters = Parameters [ GestureDetector.New.key
    , GestureDetector.New.child
    , GestureDetector.New.onTapDown
    , GestureDetector.New.onTapUp
    , GestureDetector.New.onTap
    , GestureDetector.New.onTapCancel
    , GestureDetector.New.onSecondaryTap
    , GestureDetector.New.onSecondaryTapCancel
    , GestureDetector.New.onDoubleTap
    , GestureDetector.New.onDoubleTapCancel
    , GestureDetector.New.onSecondaryTapDown
    , GestureDetector.New.onSecondaryTapUp
    , GestureDetector.New.onLongPress
    , GestureDetector.New.onLongPressStart
    , GestureDetector.New.onLongPressMoveUpdate
    , GestureDetector.New.onLongPressEnd ]

  %inline
  public export
  new : HasIO io => GestureDetector.New.NamedParameters -> io GestureDetector
  new  ps = primIO $ prim__dart_new GestureDetector [] ps

namespace CustomPaint
  export
  IsAssignableFrom Widget CustomPaint where

  namespace New
    data Tag : Type where

    %inline
    public export
    key : Parameter CustomPaint.New.Tag
    key = mkParameter "key" Key

    %inline
    public export
    child : Parameter CustomPaint.New.Tag
    child = mkParameter "child" Widget

    %inline
    public export
    painter : Parameter CustomPaint.New.Tag
    painter = mkParameter "painter" CustomPainter

    %inline
    public export
    foregroundPainter : Parameter CustomPaint.New.Tag
    foregroundPainter = mkParameter "foregroundPainter" CustomPainter

    %inline
    public export
    size : Parameter CustomPaint.New.Tag
    size = mkParameter "size" Size

    %inline
    public export
    isComplex : Parameter CustomPaint.New.Tag
    isComplex = mkParameter "isComplex" DartBool

    %inline
    public export
    willChange : Parameter CustomPaint.New.Tag
    willChange = mkParameter "willChange" DartBool
    %inline
    public export
    NamedParameters : Type
    NamedParameters = Parameters [ CustomPaint.New.key
    , CustomPaint.New.child
    , CustomPaint.New.painter
    , CustomPaint.New.foregroundPainter
    , CustomPaint.New.size
    , CustomPaint.New.isComplex
    , CustomPaint.New.willChange ]

  %inline
  public export
  new : HasIO io => CustomPaint.New.NamedParameters -> io CustomPaint
  new  ps = primIO $ prim__dart_new CustomPaint [] ps

namespace AppLifecycleState
  export
  %foreign "Dart:const AppLifecycleState.detached,dart:ui"
  detached : AppLifecycleState
  export
  %foreign "Dart:const AppLifecycleState.inactive,dart:ui"
  inactive : AppLifecycleState
  export
  %foreign "Dart:const AppLifecycleState.paused,dart:ui"
  paused : AppLifecycleState
  export
  %foreign "Dart:const AppLifecycleState.resumed,dart:ui"
  resumed : AppLifecycleState

namespace Canvas
  %foreign "Dart:.drawPath"
  prim__drawPath : (this : Canvas) -> (path : Path) -> (paint : Paint) -> PrimIO ()

  export
  drawPath : HasIO io => (path : Path) -> (paint : Paint) -> (this : Canvas) -> io ()
  drawPath path paint this = primIO $ prim__drawPath this path paint

namespace PaintingStyle
  export
  %foreign "Dart:const PaintingStyle.stroke,dart:ui"
  stroke : PaintingStyle

namespace Paint
  %inline
  public export
  new : HasIO io => io Paint
  new  = primIO $ prim__dart_new Paint [] (the (Parameters {tag = Void} []) [])

  export
  style : Paint -> PaintingStyle
  style this = getField this "style"

  export
  setStyle : PaintingStyle -> Paint -> IO ()
  setStyle value this = setField this "style" value

  export
  strokeWidth : Paint -> Double
  strokeWidth this = getField this "strokeWidth"

  export
  setStrokeWidth : Double -> Paint -> IO ()
  setStrokeWidth value this = setField this "strokeWidth" value

namespace Offset
  %inline
  public export
  new : HasIO io => (dx : Double) -> (dy : Double) -> io Offset
  new dx dy = primIO $ prim__dart_new Offset [dx, dy] (the (Parameters {tag = Void} []) [])

  export
  dx : Offset -> Double
  dx this = getField this "dx"

  export
  dy : Offset -> Double
  dy this = getField this "dy"

namespace Size
  export
  width : Size -> Double
  width this = getField this "width"

  export
  height : Size -> Double
  height this = getField this "height"

namespace Path
  %inline
  public export
  new : HasIO io => io Path
  new  = primIO $ prim__dart_new Path [] (the (Parameters {tag = Void} []) [])

  %foreign "Dart:.moveTo"
  prim__moveTo : (this : Path) -> (x : Double) -> (y : Double) -> PrimIO ()

  export
  moveTo : HasIO io => (x : Double) -> (y : Double) -> (this : Path) -> io ()
  moveTo x y this = primIO $ prim__moveTo this x y

  %foreign "Dart:.lineTo"
  prim__lineTo : (this : Path) -> (x : Double) -> (y : Double) -> PrimIO ()

  export
  lineTo : HasIO io => (x : Double) -> (y : Double) -> (this : Path) -> io ()
  lineTo x y this = primIO $ prim__lineTo this x y

namespace Velocity
  export
  pixelsPerSecond : Velocity -> Offset
  pixelsPerSecond this = getField this "pixelsPerSecond"

namespace TextAlign
  export
  %foreign "Dart:const TextAlign.left,dart:ui"
  left : TextAlign
  export
  %foreign "Dart:const TextAlign.right,dart:ui"
  right : TextAlign
  export
  %foreign "Dart:const TextAlign.center,dart:ui"
  center : TextAlign
  export
  %foreign "Dart:const TextAlign.start,dart:ui"
  start : TextAlign
  export
  %foreign "Dart:const TextAlign.end,dart:ui"
  end : TextAlign
  export
  %foreign "Dart:const TextAlign.justify,dart:ui"
  justify : TextAlign

namespace TapDownDetails
  export
  globalPosition : TapDownDetails -> Offset
  globalPosition this = getField this "globalPosition"

  export
  localPosition : TapDownDetails -> Offset
  localPosition this = getField this "localPosition"

namespace TapUpDetails
  export
  globalPosition : TapUpDetails -> Offset
  globalPosition this = getField this "globalPosition"

  export
  localPosition : TapUpDetails -> Offset
  localPosition this = getField this "localPosition"

namespace LongPressStartDetails
  export
  globalPosition : LongPressStartDetails -> Offset
  globalPosition this = getField this "globalPosition"

  export
  localPosition : LongPressStartDetails -> Offset
  localPosition this = getField this "localPosition"

namespace LongPressMoveUpdateDetails
  export
  localOffsetFromOrigin : LongPressMoveUpdateDetails -> Offset
  localOffsetFromOrigin this = getField this "localOffsetFromOrigin"

  export
  localPosition : LongPressMoveUpdateDetails -> Offset
  localPosition this = getField this "localPosition"

namespace LongPressEndDetails
  export
  globalPosition : LongPressEndDetails -> Offset
  globalPosition this = getField this "globalPosition"

  export
  localPosition : LongPressEndDetails -> Offset
  localPosition this = getField this "localPosition"


text:
module Palindrome

import Data.Strings
import System.REPL

%default total

palindrome : String -> Bool
palindrome s = toLower s == toLower (reverse s)

checkPalindrome : (str : String) -> String
checkPalindrome str = if palindrome str
                         then "Yes" ++ "\n"
                         else "No" ++ "\n"

partial
main : IO ()
main = repl "Enter a string: " checkPalindrome

max_stars_repo_name: timmyjose-study/tdd-with-idris

max_issues_repo_name: timmyjose-study/tdd-with-idris

max_forks_repo_name: timmyjose-study/tdd-with-idris


text:
module Text.CSS.Dir

import Data.List
import Text.CSS.Length
import Text.CSS.Percentage
import Text.CSS.Render

%default total

public export
data Dir : Type -> Type where
  All    : a -> Dir a
  Left   : a -> Dir a
  Right  : a -> Dir a
  Top    : a -> Dir a
  Bottom : a -> Dir a
  ||| Vertical and horizontal width
  VH   : (v, h : a) -> Dir a
  ||| Top, horizontal, bottom width
  THB  : (t, h, b : a) -> Dir a
  ||| Top, right, bottom, left
  TRBL : (t, r, b, l : a) -> Dir a

-- prefix
prfx : Dir a -> String
prfx (Left _)   = "-left"
prfx (Right _)  = "-right"
prfx (Top _)    = "-top"
prfx (Bottom _) = "-bottom"
prfx _          = ""

export
vals : Dir a -> List a
vals (All  x)       = [x]
vals (Left  x)      = [x]
vals (Right  x)     = [x]
vals (Top  x)       = [x]
vals (Bottom  x)    = [x]
vals (VH   v h)     = [v,h]
vals (THB  t h b)   = [t,h,b]
vals (TRBL t r b l) = [t,r,b,l]

export
render : (prop : String) -> (a -> String) -> Dir a -> String
render prop f d =
  let vs  = fastConcat . intersperse " " . map f $ vals d
      pre = prfx d
   in "\{prop}\{pre}: \{vs}"

export
render2 : (prop,suffix : String) -> (a -> String) -> Dir a -> String
render2 prop suffix f d =
  let vs  = fastConcat . intersperse " " . map f $ vals d
      pre = prfx d
   in "\{prop}\{pre}-\{suffix}: \{vs}"

export %inline
Cast Length a => Cast Length (Dir a) where
  cast = All . cast

export %inline
Cast Percentage a => Cast Percentage (Dir a) where
  cast = All . cast


text:
module Bautzen.Game.Core

import Bautzen.Combats
import Bautzen.GameUnit
import Bautzen.Pos
import Bautzen.Terrain

import Data.Fin
import Data.Nat

%default total

||| * see section 8.2
public export
data CombatPhase : Type where
  NoCombat : CombatPhase
  AssignTacticalSupport : (side : Side) -> (combat : CombatState) -> CombatPhase
  AssignStrategicSupport : (side : Side) -> (combat : CombatState) -> CombatPhase
  Resolve : (combat : CombatState) -> CombatPhase
  ApplyLosses : (side : Side) -> (combat : CombatState) -> CombatPhase

public export
data GameSegment : Type where
  Supply : GameSegment
  Move : GameSegment
  Combat : (phase : CombatPhase) -> GameSegment
  GameEnd : GameSegment

public export
Show GameSegment where
  show Supply = "Supply"
  show Move = "Move"
  show (Combat _) = "Combat"
  show GameEnd = "GameEnd"

public export
record GameState where
  constructor MkGameState
  turn : Fin 6
  side : Side
  segment : GameSegment
  units : List (GameUnit, Pos)

public export
Show GameState where
  show (MkGameState turn side segment units) =
    "GameState: turn=" ++
    show (finToInteger turn) ++
    ", side=" ++ show side ++
    ", " ++ show segment ++
    ", units=" ++ show units

public export
data GameError : Type where
  NoSuchUnits : (unitName : List String) -> GameError
  NotYourTurn : (side : Side) -> GameError
  EnemyInHex : (unit : GameUnit) -> (hex : Pos) -> GameError
  MoveFromZocToZoc : (unit : GameUnit) -> (to : Pos) -> GameError
  ForbiddenTerrain : (from : Pos) -> (to : Pos) -> GameError
  InvalidMove : (from : Pos) -> (to : Pos) -> GameError
  NotEnoughMPs : (unit : GameUnit) -> (from : Pos)-> (to : Pos) -> (mp : Nat) -> GameError
  NotAdjacentTo : (units : List GameUnit) -> (target : Pos) -> GameError
  NothingToAttack : (target : Pos) -> GameError
  AttackingOwnUnits : (units : List GameUnit) -> (target : Pos) -> GameError
  NotSupportingUnits: (units : List GameUnit) -> GameError
  NotInSupportRange: (units : List GameUnit) -> GameError
  NotInChainOfCommand : (units : List GameUnit) -> GameError
  NoSupplyColumnThere : (hex : Pos) -> GameError
  NoStepsToLose : (side : Side) -> GameError
  CombatInProgress : (side : Side) -> GameError
  GameHasEnded : GameError

public export
Show GameError where
  show (NoSuchUnits unitNames) = "No such units: " ++ show unitNames
  show (NotYourTurn side) = "Not your turn: " ++ show side
  show (EnemyInHex unit hex) = "Target hex is occupied by enemy: " ++ show hex
  show (MoveFromZocToZoc unit to) = "Cannot move from a ZoC to a ZoC: " ++ show to
  show (ForbiddenTerrain from to) = "Unit cannot enter terrain: " ++ show from ++ " -> " ++ show to
  show (InvalidMove from to) = "Move is invalid: " ++ show from ++ " -> " ++ show to
  show (NotEnoughMPs unit from to mp) = "Unit has not enough MPs: " ++ show mp ++ ", " ++ show from ++ " -> " ++ show to
  show (NotAdjacentTo units target) = "Units are not adjacent to target hex: " ++ show units ++ " -> " ++ show target
  show (NotInSupportRange units) = "Units are not in support range: " ++ show units
  show (NotSupportingUnits units) = "Units are not support units (HQ or Artillery): " ++ show units
  show (NotInChainOfCommand units) = "HQ cannot provide support to other formation's units: " ++ show units
  show (NoSupplyColumnThere hex) = "No supply column there: " ++ show hex
  show (NoStepsToLose side) = "No steps to lose for " ++ show side
  show (NothingToAttack target) = "Attacked hex is empty: " ++ show target
  show (AttackingOwnUnits units target) = "Attacking own units: " ++ show units ++ " -> " ++ show target
  show (CombatInProgress side) = "Combat in progress for: " ++ show side
  show GameHasEnded = "Game has ended"

public export
data Command : (segment : GameSegment) -> Type where
  MoveTo : (unitName : String) -> (to : Pos) -> Command Move
  AttackWith : (unitNames : List String) -> (target : Pos) -> Command (Combat NoCombat)
  NextSegment : Command segment
  TacticalSupport : (unitNames : List String) -> Command (Combat $ AssignTacticalSupport side combatState)
  ResolveCombat : (combatState : CombatState) -> Command (Combat $ Resolve combatState)
  LoseStep : (unitName : String) -> Command (Combat $ ApplyLosses side combatState)

public export
Show (Command segment) where
  show (MoveTo unitName to) = "MoveTo " ++ unitName ++ " -> " ++ show to
  show (AttackWith unitNames target) = "AttackWith " ++ show unitNames ++ " -> " ++ show target
  show NextSegment = "NextSegment"
  show (TacticalSupport unitNames) = "TacticalSupport " ++ show unitNames
  show (ResolveCombat state) = "ResolveCombat " ++ show state
  show (LoseStep unitName) = "LoseStep " ++ show unitName

public export
data Event : Type where

  ||| Unit has moved from some position to some other position
  Moved : (unit : GameUnit) -> (from : Pos) -> (to : Pos) -> (cost : Cost)
        -> { auto prf : LTE (toNat cost) (currentMP unit) }
        -> Event

  ||| Some attackers have engaged combat with some defenders on the given target hex.
  |||
  ||| The target hex can be inferred from the `defenders`' position, eg. all `defenders`
  ||| should be in the same hex.
  |||
  ||| @attackers list of attacker's units and their positions
  ||| @defenders list of defender's units and their positions
  ||| @target the attacked position
  CombatEngaged : (attackers : List (GameUnit, Pos)) -> (defenders : List (GameUnit, Pos)) -> (target : Pos) -> Event

  ||| Units provide tactical support for some side in current combat
  |||
  ||| @supportedSide the side which is given support
  ||| @supportUnits units and positions that provide support
  TacticalSupportProvided : (supportedSide : Side) -> (supportUnits : List (GameUnit, Pos)) -> Event

  ||| A supply column is used to provide support to units engaged in a combat
  |||
  ||| @supportedSide the side which is given support
  ||| @hex the position of the supply column
  SupplyColumnUsed : (supportedSide : Side) -> (hex : Pos) -> Event

  ||| Combat has been resolved yielding the given losses
  |||
  ||| @state the state of the combat (before any loss has been applied)
  ||| @losses losses to apply on engaged units
  CombatResolved : (state : CombatState) -> (losses : Losses) -> Event

  ||| Given unit has lost a step
  |||
  ||| Depending on the current state of the unit, this can either
  ||| either reduce the unit or destroy it.
  |||
  ||| @side the side the unit is part of (useful to look for the unit in
  ||| the combat state
  ||| @unit the unit to apply a step loss to
  ||| @remainingLosses  losses  remaining to apply
  StepLost : (side : Side) -> (unit : GameUnit) -> (remainingLosses : Losses) -> Event

  ||| The segment has been advanced one step.
  |||
  ||| @from the previous segment
  ||| @to the new segment
  SegmentChanged : (from : GameSegment)  -> (to : GameSegment) -> Event

  ||| Axis turn is over, move to Allies turn
  AxisTurnDone : Event

  ||| Turn ended, start a new turn
  TurnEnded : Fin 6 -> Event

  ||| Game has ended
  GameEnded : Event

public export
Show Event where
  show (Moved unit from to cost) = "Moved " ++ name unit ++ " from " ++ show from ++ " to " ++ show to ++ " for "  ++ show (toNat cost) ++ " mps"
  show (CombatEngaged atk def tgt) = "CombatEngaged " ++ show (map (GameUnit.name . fst) atk) ++ " -> " ++ show (map (GameUnit.name . fst) def) ++ " @ " ++ show tgt
  show (TacticalSupportProvided side units) = "TacticalSupportProvided " ++ show (map (GameUnit.name . fst) units) ++ " -> " ++ show side
  show (SupplyColumnUsed side hex) = "SupplyColumnUsed " ++ show side ++ " @ " ++ show hex
  show (CombatResolved state losses) = "CombatResolved " ++ show state ++ " : " ++ show losses
  show (StepLost side unit remain) = "Step Lost " ++ show unit ++ " @ " ++ show side ++  " (" ++ show remain++")"
  show (SegmentChanged from to) = "Segment Changed " ++ show from ++ " -> " ++ show to
  show AxisTurnDone = "Axis Turn Over"
  show (TurnEnded n) = "Turn Ended: " ++ show (finToNat n)
  show GameEnded = "Game Ended"

public export
data Game : Type where
  MkGame : (events : List Event) -> (curState : GameState) -> (gameMap : Map) -> Game

public export
Show Game where
  show (MkGame events state gameMap) = "Game: " ++ show events ++ "\n" ++ show state ++ "\n" ++ show gameMap

public export
curSegment : Game -> GameSegment
curSegment (MkGame _ (MkGameState _ _  segment _) _) = segment

public export
data QueryError : Type where
  NoSupplyPathFor : (unitName: String) -> (pos : Pos) -> QueryError
  UnitDoesNotExist : (unitName: String) -> QueryError

max_stars_repo_name: steshaw/hsgames

max_issues_repo_name: steshaw/hsgames

max_forks_repo_name: steshaw/hsgames


text:
-- --------------------------------------------------------------- [ Day07.idr ]
-- Module      : Data.Advent.Day07
-- Description : My solution to the Day 7 puzzle of the 2016 Advent of Code.
-- Copyright   : Copyright (c) 2016, Eric Bailey
-- License     : MIT
-- Link        : http://adventofcode.com/2016/day/7
-- --------------------------------------------------------------------- [ EOH ]
||| Day 7: Signals and Noise
module Data.Advent.Day07

import Control.Arrow
import Control.Category
import Data.Morphisms

import public Lightyear
import public Lightyear.Char
import public Lightyear.Strings
import public Lightyear.StringFile

%default total

-- -------------------------------------------------------------- [ Main Logic ]

%access export

main' : Show b => Parser a -> (a -> b) -> IO ()
main' p f =
    either putStrLn (printLn . f)
           !(run $ parseFile (const show) (const id) p "input/day07.txt")

-- ---------------------------------------------------- [ Part One: Data Types ]

%access public export

ABBA : Type
ABBA = Vect 4 Char

Sequence : Type
Sequence = List ABBA

Segment : Type
Segment = (Sequence, Sequence)

Address : Type
Address = List Segment

Input : Type
Input = List Address

-- ------------------------------------------------------- [ Part One: Helpers ]

%access private

letterExcept : Char -> Parser Char
letterExcept c = satisfy (\x => x /= c && isAlpha x) <?>
                 "a letter that's not " ++ singleton c

maybeSkipLetter : Parser a -> Parser (Maybe a)
maybeSkipLetter p = Just <$> p <|> (skip letter *> pure Nothing)

-- ------------------------------------------------------- [ Part One: Parsers ]

%access export
%default partial

total
abba : Parser ABBA
abba = do a  <- letter
          b  <- letterExcept a
          char b
          char a
          pure [a,b,b,a] <?> "an ABBA"

total
maybeAbba : Parser (Maybe ABBA)
maybeAbba = maybeSkipLetter abba <?> "maybe an ABBA or skip a letter"

abbas : Parser Sequence
abbas = catMaybes <$> some maybeAbba <?> "a list of ABBAs"

hypernetSequence : Parser Sequence
hypernetSequence = between (char '[') (char ']') abbas <?> "a hypernet sequence"

segment : Parser Segment
segment = liftA2 MkPair abbas (hypernetSequence <|> pure []) <?> "a segment"

-- --------------------------------------------------------- [ Part One: Logic ]

%default total

supportsTLS : Address -> Bool
supportsTLS seg = any (not . isNil . fst) seg &&
                  all (isNil . snd) seg

supportTLS : Input -> Nat
supportTLS = List.length . filter id . map supportsTLS

-- ------------------------------------------------------ [ Part One: Examples ]

||| ```idris example
||| map supportsTLS <$> parse (some (some segment <* spaces)) partOneExamples
||| ```
||| ```idris example
||| supportTLS <$> parse (some (some segment <* spaces)) partOneExamples
||| ```
partOneExamples : String
partOneExamples =
    "abba[mnop]qrst\nabcd[bddb]xyyx\naaaa[qwer]tyui\nioxxoj[asdfgh]zxcvbn"

-- ---------------------------------------------------------- [ Part One: Main ]

namespace PartOne

    partial
    main : IO ()
    main = main' (some (some segment <* spaces)) supportTLS

-- ---------------------------------------------------- [ Part Two: Data Types ]

%access public export

ABA : Type
ABA = Vect 3 Char

BAB : Type
BAB = Vect 3 Char

-- ------------------------------------------------------- [ Part Two: Helpers ]

%access export

abaToBab : ABA -> BAB
abaToBab [a,b,_] = [b,a,b]

-- ------------------------------------------------------- [ Part Two: Parsers ]

%access export
%default partial

xyxs : Parser (List (Vect 3 Char))
xyxs = go <$> some letter
  where
    go : List Char -> List ABA
    go (x::t@(y::z::zs)) = let ts = go t in if x == z then [x,y,x] :: ts else ts
    go _                 = []

abas : Parser (List ABA)
abas = xyxs

babs : Parser (List BAB)
babs = xyxs

hypernetSequence' : Parser (List BAB)
hypernetSequence' = between (char '[') (char ']') babs <?> "a hypernet sequence"

segment' : Parser (List ABA, List BAB)
segment' = liftA2 MkPair abas (hypernetSequence' <|> pure []) <?> "a segment"

-- --------------------------------------------------------- [ Part Two: Logic ]

%access export
%default total

supportsSSL : List (List ABA, List BAB) -> Bool
supportsSSL = applyMor $ smash >>> grab
  where
    smash : List (List ABA, List BAB) ~> (List BAB, List BAB)
    smash = arrow (concatMap (map abaToBab . fst)) &&& arrow (concatMap snd)
    grab : (List BAB, List BAB) ~> Bool
    grab = arrow (uncurry (flip (any . flip elem)))

supportSSL : List (List (List ABA, List BAB)) -> Nat
supportSSL = List.length . filter id . map supportsSSL

-- ------------------------------------------------------ [ Part Two: Examples ]

||| ```idris example
||| map supportsSSL <$> parse (some (some segment' <* spaces)) partTwoExamples
||| ```
||| ```idris example
||| supportSSL <$> parse (some (some segment' <* spaces)) partTwoExamples
||| ```
partTwoExamples : String
partTwoExamples = "aba[bab]xyz\nxyx[xyx]xyx\naaa[kek]eke\nzazbz[bzb]cdb"

-- ---------------------------------------------------------- [ Part Two: Main ]

namespace PartTwo

    partial
    main : IO ()
    main = main' (some (some segment' <* spaces)) supportSSL

-- -------------------------------------------------------------------- [ Main ]

namespace Main

    partial
    main : IO ()
    main = putStr "Part One: " *> PartOne.main *>
           putStr "Part Two: " *> PartTwo.main

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

max_stars_repo_name: yurrriq/advent-of-code