\begin{code}
{-# OPTIONS --cubical --postfix-projections --safe #-}

module Countdown where

open import Prelude
open import Data.List
open import Data.Fin

open import Data.Nat using (_+_; _*_; _∸_; _÷_; rem)
open import Data.Nat.Properties using (pred; _≡ᴮ_; _<ᴮ_; discreteℕ)
open import Data.Fin.Properties using (FinToℕ)
open import Dyck
open import Data.Vec.Iterated

\end{code}
%<*ops-def>
\begin{code}
data Op : Type₀ where
  +′ ×′ -′ ÷′ : Op
\end{code}
%</ops-def>
\begin{code}
private
  variable
    n m k : ℕ

Subseq : ℕ → Type₀
Subseq = Vec Bool

module WrongPerm where
\end{code}
%<*wrong-perm>
\begin{code}
    Perm : ℕ → Type₀
    Perm n = Fin n → Fin n
\end{code}
%</wrong-perm>
\begin{code}
module IsoPerm where
\end{code}
%<*isomorphism>
\begin{code}
    Isomorphism : Type a → Type b → Type (a ℓ⊔ b)
    Isomorphism A B = Σ[ f ⦂ (A → B) ] Σ[ g ⦂ (B → A) ] (f ∘ g ≡ id) × (g ∘ f ≡ id)
\end{code}
%</isomorphism>
%<*iso-perm>
\begin{code}
    Perm : ℕ → Type₀
    Perm n = Isomorphism (Fin n) (Fin n)
\end{code}
%</iso-perm>
%<*perm-def>
\begin{code}
Perm : ℕ → Type₀
Perm zero     = ⊤
Perm (suc n)  = Fin (suc n) × Perm n
\end{code}
%</perm-def>
\begin{code}
private
  variable ns : List ℕ

count : Subseq n → ℕ
count = foldr′ (λ x xs → bool   x + xs) 
\end{code}
%<*expr-def>
\begin{code}
ExprTree : ℕ → Type₀
ExprTree zero     = ⊥
ExprTree (suc n)  = Dyck  n × Vec Op n

Transformation : List ℕ → Type₀
Transformation ns =
  Σ[ s ⦂ Subseq (length ns) ]
    let n = count s
    in Perm n × ExprTree n
\end{code}
%</expr-def>
\begin{code}
open import Cardinality.Finite.SplitEnumerable
open import Cardinality.Finite.SplitEnumerable.Inductive
open import Cardinality.Finite.SplitEnumerable.Isomorphism
open import Function.Surjective.Properties

private
  module OpSlop where
    open import Literals.Number
    open import Data.Nat.Literals
    open import Data.Fin.Literals
\end{code}
%<*op-slop>
\begin{code}
    ℰ!⟨Op⟩ : ℰ! Op
    ℰ!⟨Op⟩ .fst = +′ ∷ +′ ∷ ×′ ∷ -′ ∷ ÷′ ∷ []
    ℰ!⟨Op⟩ .snd +′  =  , refl
    ℰ!⟨Op⟩ .snd ×′  =  , refl
    ℰ!⟨Op⟩ .snd -′  =  , refl
    ℰ!⟨Op⟩ .snd ÷′  =  , refl
\end{code}
%</op-slop>
\begin{code}
open import Data.List using (tabulate)
open import Data.List.Membership using (fin∈tabulate)

import Data.Unit.UniversePolymorphic as Poly

ℰ!⟨Poly⊤⟩ : ∀ {ℓ} → ℰ! (Poly.⊤ {ℓ})
ℰ!⟨Poly⊤⟩ .fst = _ ∷ []
ℰ!⟨Poly⊤⟩ .snd _ = f0 , refl
\end{code}
%<*vec-fin>
\begin{code}
ℰ!⟨Vec⟩ : ℰ! A → ℰ! (Vec A n)
ℰ!⟨Vec⟩ {n = zero   } ℰ!⟨A⟩ = ℰ!⟨Poly⊤⟩
ℰ!⟨Vec⟩ {n = suc n  } ℰ!⟨A⟩ = ℰ!⟨A⟩ |×| ℰ!⟨Vec⟩ ℰ!⟨A⟩
\end{code}
%</vec-fin>
\begin{code}
ℰ!⟨Subseq⟩ : ℰ! (Subseq n)
ℰ!⟨Subseq⟩ = ℰ!⟨Vec⟩ ℰ!⟨2⟩
\end{code}
%<*perm-fin>
\begin{code}
ℰ!⟨Perm⟩ : ℰ! (Perm n)
ℰ!⟨Perm⟩ {n = zero   } = ℰ!⟨⊤⟩
ℰ!⟨Perm⟩ {n = suc n  } = ℰ!⟨Fin⟩ |×| ℰ!⟨Perm⟩
\end{code}
%</perm-fin>
\begin{code}
module _ where
  open import Literals.Number
  open import Data.Fin.Literals
\end{code}
%<*op-fin>
\begin{code}
  ℰ!⟨Op⟩ : ℰ! Op
  ℰ!⟨Op⟩ .fst = +′ ∷ ×′ ∷ -′ ∷ ÷′ ∷ []
  ℰ!⟨Op⟩ .snd +′  =  , refl
  ℰ!⟨Op⟩ .snd ×′  =  , refl
  ℰ!⟨Op⟩ .snd -′  =  , refl
  ℰ!⟨Op⟩ .snd ÷′  =  , refl
\end{code}
%</op-fin>
\begin{code}
\end{code}
%<*expr-finite>
\begin{code}
ℰ!⟨ExprTree⟩ : ℰ! (ExprTree n)
ℰ!⟨ExprTree⟩ {n = zero } = ℰ!⟨⊥⟩
ℰ!⟨ExprTree⟩ {n = suc n} = ℰ!⟨Dyck⟩ |×| ℰ!⟨Vec⟩ ℰ!⟨Op⟩

ℰ!⟨Transformation⟩ : ℰ! (Transformation ns)
ℰ!⟨Transformation⟩ = ℰ!⟨Subseq⟩ |Σ| λ _ → ℰ!⟨Perm⟩ |×| ℰ!⟨ExprTree⟩
\end{code}
%</expr-finite>
\begin{code}
runSubseq : (xs : List A) → (ys : Subseq (length xs)) → Vec A (count ys)
runSubseq []       ys = _
runSubseq (x ∷ xs) (false , snd₁) = runSubseq xs snd₁
runSubseq (x ∷ xs) (true , snd₁) = x , runSubseq xs snd₁

insert : A → Fin (suc n) → Vec A n → Vec A (suc n)
insert x f0 xs = x , xs
insert {n = suc _} x (fs i) (x₂ , xs) = x₂ , insert x i xs

runPerm : Perm n → Vec A n → Vec A n
runPerm {n = zero} ps _ = _
runPerm {n = suc n} (fst₁ , snd₁) (x , xs) = insert x fst₁ (runPerm snd₁ xs)

transform : (xs : List ℕ) → Transformation xs → Tree Op ℕ
transform xs (subseq , rest) with count subseq | runSubseq xs subseq
transform xs (subseq , (perm , tree , ops)) | suc n | ys = fromDyck tree ops (runPerm perm ys)
\end{code}
%<*app-op>
\begin{code}
_!⟨_⟩!_ : ℕ → Op → ℕ → Maybe ℕ
x !⟨ +′ ⟩! y = just $! (x + y)
x !⟨ ×′ ⟩! y = just $! (x * y)
x !⟨ -′ ⟩! y =
  if x <ᴮ y
    then nothing
    else just $! (x ∸ y)
x !⟨ ÷′ ⟩! zero = nothing
x !⟨ ÷′ ⟩! suc y =
  if rem x (suc y) ≡ᴮ 
    then just $! (x ÷ suc y)
    else nothing
\end{code}
%</app-op>
%<*eval>
\begin{code}

eval : Tree Op ℕ → Maybe ℕ
eval (leaf x) = just x
eval (xs ⟨ op ⟩ ys) = do
    x ← eval xs
    y ← eval ys
    x !⟨ op ⟩! y
\end{code}
%</eval>
\begin{code}
  where
  open import Data.Maybe.Sugar

open import Data.Maybe.Properties using (discreteMaybe)

Solution : List ℕ → ℕ → Type₀
\end{code}
%<*solution-type>
\begin{code}
Solution ns n = Σ[ e ⦂ Transformation ns ] (eval (transform ns e) ≡ just n)
\end{code}
%</solution-type>
\begin{code}

solution? : ∀ n → (e : Transformation ns) → Dec (eval (transform ns e) ≡ just n)
solution? {ns} n e = discreteMaybe discreteℕ (eval (transform ns e)) (just n)

ℰ!⟨Solutions⟩ :
\end{code}
%<*finite-solution>
\begin{code}
  ℰ! (Solution ns n)
\end{code}
%</finite-solution>
\begin{code}
ℰ!⟨Solutions⟩ {ns = ns} = filter-subobject (λ _ → isSetMaybe _ _) (solution? {ns = ns} _) (ℰ!⟨Transformation⟩ {ns = ns})
  where
  isSetMaybe : isSet (Maybe ℕ)
  isSetMaybe = Discrete→isSet (discreteMaybe discreteℕ)

data Disp : Type₀ where
  lit : ℕ → Disp
  _⟨+⟩_ : Disp → Disp → Disp
  _⟨*⟩_ : Disp → Disp → Disp
  _⟨-⟩_ : Disp → Disp → Disp
  _⟨÷⟩_ : Disp → Disp → Disp

appDispOp : Op → Disp → Disp → Disp
appDispOp +′ = _⟨+⟩_
appDispOp ×′ = _⟨*⟩_
appDispOp -′ = _⟨-⟩_
appDispOp ÷′ = _⟨÷⟩_

dispTree : Tree Op ℕ → Disp
dispTree (leaf x) = lit $! x
dispTree (xs ⟨ o ⟩ ys) = (appDispOp o $! dispTree xs) $! dispTree ys

open import Data.List.Syntax
\end{code}
%<*example-solution>
\begin{code}
exampleSolutions : ℰ! (Solution [  ,  ,  ,  ,  ,  ] )
exampleSolutions = ℰ!⟨Solutions⟩
\end{code}
%</example-solution>
\begin{code}

example : List Disp
example = map (dispTree ∘ transform [  ,  ,  ,  ,  ,  ] ∘ fst) (take  (fst exampleSolutions))

-- Uncomment for an error which contains the solution
-- _ : example ≡ lit 0 ∷ []
-- _ = refl
\end{code}