module ErasableMonadTest where

open import ErasableMonad

open import Data.Nat
open import Data.Unit
open import Data.Empty
open import Relation.Binary.PropositionalEquality
open import Data.Product

isEven : ℕ → Set
isEven zero = ⊤
isEven (suc zero) = ⊥
isEven (suc (suc n)) = isEven n

Even+ : (a b : ℕ) → isEven a → isEven b → isEven (a + b)
Even+ zero = λ b _ z → z
Even+ (suc zero) = λ b → λ ()
Even+ (suc (suc n)) = Even+ n

_+M_ : (a b : M ℕ) → M ℕ
ma +M mb = ma >>= λ a → 
           mb >>= λ b → 
           return (a + b)

-- MEven+ is a version of Even+ which has all of is arguments in the monad.
MEven+ : {ma mb : M ℕ} → M (smap isEven ma) → M (smap isEven mb) → M (smap isEven (ma +M mb))
MEven+ {ma}{mb} mema memb = ma >>≡ λ a ma≡ →
                            mb >>≡ λ b mb≡ →
                            mema >>= λ ema → 
                            memb >>= λ emb → 
                            return (MEven+' a b ma≡ mb≡ ema emb)
  where
    MEven+' : (a b : ℕ) → ma ≡ return a → mb ≡ return b → 
              smap isEven ma → smap isEven mb → smap isEven (ma +M mb)
    MEven+' a b ma≡ mb≡ ema emb rewrite ma≡ | mb≡
      | Ax1 a (λ x → return (isEven x))
      | Ax1 b (λ x → return (isEven x))
      | Axs (isEven a) 
      | Axs (isEven b)
      | Ax1 a (λ a' → bind (return b) (λ b' → return (a' + b')))
      | Ax1 b (λ b' → return (a + b'))
      | Ax1 (a + b) (λ x → return (isEven x))
      | Axs (isEven (a + b))
      = Even+ a b ema emb

-- Discrimination still exists within the monad:
Mdisc : M (1 ≡ 2 → ⊥)
Mdisc = return (λ ())

-- even though neither discrimination nor uniqueness is provable outide:

out-disc : return 1 ≡ return 2 → ⊥
out-disc = {!!} -- no solution

out-uniq : return 1 ≡ return 2
out-uniq = {!!} -- no solution