Horrible pattern matching hack

match.agda

{-# OPTIONS --universe-polymorphism #-}
module match where
open import Data.List hiding (or)
open import Category.Monad
open import Category.Functor
open import Function
open import Data.Maybe
open import Data.Bool
open import Data.Nat
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary
open import Level using (Level)
open import Data.Product
open import Data.Unit

isEven : ℕ → Bool
isEven zero = true
isEven (suc zero) = false
isEven (suc (suc n)) = isEven n

toTuple : List Set → Set
toTuple [] = ⊤
toTuple (A ∷ As) = A × toTuple As

toCont : List Set → Set → Set
toCont [] R = R
toCont (A ∷ AS) R = A → toCont AS R

tcat : ∀{AS} → toTuple AS → ∀{BS} → toTuple BS → toTuple (AS ++ BS)
tcat {[]} tt rest = rest
tcat {A ∷ AS} (a , as) rest = a , tcat {AS} as rest

tapp : ∀{AS} → toTuple AS → ∀{X} → toCont AS X → X
tapp {[]} tt r = r
tapp {A ∷ AS} (a , as) f = tapp {AS} as (f a)

record Matcher (A : Set) (Binds : List Set) : Set where
  field match : A → Maybe (toTuple Binds)

var : {A : Set} → Matcher A [ A ]
var = record { match = λ x → just (x , tt) }

wild : {A : Set} → Matcher A []
wild = record { match = λ _ → just tt }

con : {A : Set}{{eq : (a b : A) → Dec (a ≡ b)}} → A → Matcher A []
con {A} {{eq}} ref = record { match = λ x → test x } 
  where test : A → Maybe ⊤
        test x with eq ref x
        ... | yes _ = just tt
        ... | no _ = nothing

combine : ∀{RA} → Maybe (toTuple RA) → ∀{RB} → Maybe (toTuple RB)
  → Maybe (toTuple (RA ++ RB))
combine {RA} ma mb = ma >>= λ a → mb >>= λ b → just (tcat {RA} a b)
  where open RawMonad Data.Maybe.monad

pair : ∀{A RA} → Matcher A RA → ∀{B RB} → Matcher B RB → Matcher (A × B) (RA ++ RB)
pair {A} {RA} ma mb = record { match = λ p → 
  combine {RA} (Matcher.match ma (proj₁ p)) (Matcher.match mb (proj₂ p)) }

or : ∀{A RA} → Matcher A RA → Matcher A RA → Matcher A RA
or {A} {RA} ma mb = record { match = λ a → Matcher.match ma a ∣ Matcher.match mb a }
  where open RawMonadPlus Data.Maybe.monadPlus

cons : ∀{A RA} → Matcher A RA → ∀{RB} → Matcher (List A) RB →
  Matcher (List A) (RA ++ RB)
cons {A} {RA} mhead {RB} mrest = record { match = dec }
  where dec : List A → Maybe (toTuple (RA ++ RB))
        dec [] = nothing
        dec (a ∷ as) = combine {RA} (Matcher.match mhead a) (Matcher.match mrest as)

nil : ∀{A} → Matcher (List A) []
nil {A} = record { match = dec }
  where dec : List A → Maybe ⊤
        dec [] = just tt
        dec (_ ∷ _) = nothing

trueP : Matcher Bool []
trueP = record { match = dec }
  where dec : Bool → Maybe ⊤ 
        dec true = just tt
        dec _ = nothing

falseP : Matcher Bool []
falseP = record { match = dec }
  where dec : Bool → Maybe ⊤ 
        dec false = just tt
        dec _ = nothing

view : {A B : Set}{R : List Set} → (A → B) → Matcher B R → Matcher A R
view {A} {_} {R} f m = record { match = λ a → Matcher.match m (f a) }

_⇒_ : ∀{A Binds B} → Matcher A Binds → toCont Binds B → A → Maybe B
_⇒_ {A} {Binds} matcher k a = (λ bs → tapp {Binds} bs k) <$> Matcher.match matcher a
  where open RawFunctor Data.Maybe.functor

_||_ : {A B : Set} → (A → Maybe B) → (A → Maybe B) → A → Maybe B
f || g = λ a → f a ∣ g a
  where open RawMonadPlus Data.Maybe.monadPlus

case_of_ : {A B : Set} → A → (A → Maybe B) → Maybe B
case a of alts = alts a

case_of_||else_ : {A B : Set} → A → (A → Maybe B) → B → B
case a of alts ||else def with alts a
... | just v = v
... | nothing = def

infixr 1 _||_
infix 2 _⇒_
infix 0 case_of_ case_of_||else_

example : Maybe ℕ
example = case (1 ∷ 2 ∷ []) of
    nil ⇒ 0
 || cons wild nil ⇒ 1
 || cons var (cons var nil) ⇒ λ x y → x + y

mysum : List ℕ → ℕ
mysum l = case l of
    cons var nil ⇒ (λ x → x)
 || cons var (cons var var) ⇒ (λ x y rest → mysum (x + y ∷ rest))
 ||else 0

evenSum : List ℕ → ℕ
evenSum l = case l of
    view (isEven ∘ length) falseP ⇒ 0
 || cons var (cons var var) ⇒ (λ x y rest → mysum (x + y ∷ rest))
 ||else 0