TooLong.agda

TooLong.agda

module TooLong where

open import Agda.Builtin.Nat renaming (Nat to ℕ)
open import Agda.Primitive
open import Agda.Builtin.Bool
open import Agda.Builtin.Equality

data SK : Set where
  S : SK
  K : SK
  _`_ : SK → SK → SK

infixl 2 _`_

data ℕExtractable : (x : SK) → Set where
  zero : ℕExtractable (K ` (S ` K ` K))
  suc  : ∀ {x} → ℕExtractable x
       → ℕExtractable (S ` (S ` (K ` S) ` K) ` x)

data ⊥ : Set where

infix 3 ¬_

¬_ : Set → Set
¬ p = p → ⊥

data Dec (P : Set) : Set where
  yes :   P → Dec P
  no  : ¬ P → Dec P

-- XXX is there a shorter way to write this?
isℕExtractable : (x : SK) → Dec (ℕExtractable x)
isℕExtractable (K ` (S ` K ` K)) = yes zero
isℕExtractable (S ` (S ` (K ` S) ` K) ` x) with isℕExtractable x
... | yes p = yes (suc p)
... | no p = no λ q → p (predExt q)
  where
    predExt : ∀ {x} -- XXX Can this function be inlined?
            → ℕExtractable (S  ` (S ` (K ` S) ` K) ` x)
            → ℕExtractable x
    predExt (suc p) = p
isℕExtractable S = no λ ()
isℕExtractable K = no λ ()
isℕExtractable (S ` x) = no λ ()
isℕExtractable (K ` S) = no λ ()
isℕExtractable (K ` K) = no λ ()
isℕExtractable (K ` (S ` x)) = no λ ()
isℕExtractable (K ` (K ` x)) = no λ ()
isℕExtractable (K ` (S ` S ` x)) = no λ ()
isℕExtractable (K ` (S ` K ` S)) = no λ ()
isℕExtractable (K ` (S ` K ` (x ` y))) = no λ ()
isℕExtractable (K ` (S ` (x ` y) ` z)) = no λ ()
isℕExtractable (K ` (K ` x ` y)) = no λ ()
isℕExtractable (K ` (x ` y ` z ` w)) = no λ ()
isℕExtractable (K ` x ` y) = no λ ()
isℕExtractable (S ` S ` x) = no λ ()
isℕExtractable (S ` K ` x) = no λ ()
isℕExtractable (S ` (S ` x) ` y) = no λ ()
isℕExtractable (S ` (K ` x) ` y) = no λ ()
isℕExtractable (S ` (S ` S ` y) ` z) = no λ ()
isℕExtractable (S ` (S ` K ` y) ` z) = no λ ()
isℕExtractable (S ` (S ` (S ` x₁) ` y) ` z) = no λ ()
isℕExtractable (S ` (S ` (K ` S) ` S) ` z) = no λ ()
isℕExtractable (S ` (S ` (K ` S) ` (y ` y₁)) ` z) = no λ ()
isℕExtractable (S ` (S ` (K ` K) ` x) ` y) = no λ ()
isℕExtractable (S ` (S ` (K ` (x ` y)) ` z) ` w) = no λ ()
isℕExtractable (S ` (S ` (x ` y ` z) ` w) ` u) = no λ ()
isℕExtractable (S ` (K ` x ` y) ` z) = no λ ()
isℕExtractable (S ` (x ` y ` z ` w) ` v) = no λ ()
isℕExtractable (x ` y ` z ` w) = no λ ()

extractℕ : (x : SK) → ℕExtractable x → ℕ
extractℕ (K ` (S ` K ` K)) zero = zero
extractℕ (S ` (S ` (K ` S) ` K) ` x) (suc p) = suc (extractℕ x p)

Not necessarily shorter but a more principled approach:

data anS : SK → Set where
  IsS : anS S

data aK : SK → Set where
  IsK : aK K

data App : SK → Set where
  IsApp : ∀ a b → App (a ` b)

data SApp : SK → Set where
  IsSApp : ∀ a b → SApp (S ` a ` b)

data Id : SK → Set where
  IsId : Id (S ` K ` K)

data ℕExtractable : (x : SK) → Set where
  zero : ℕExtractable (K ` (S ` K ` K))
  suc  : ∀ {x} → ℕExtractable x
       → ℕExtractable (S ` (S ` (K ` S) ` K) ` x)

data ⊥ : Set where

infix 3 ¬_

¬_ : Set → Set
¬ p = p → ⊥

data Dec (P : Set) : Set where
  yes :   P → Dec P
  no  : ¬ P → Dec P

isS : ∀ k → Dec (anS k)
-- Generated by C-c C-a on:
-- isS k = {! -c !}
isS S = yes IsS
isS K = no (λ ())
isS (x ` x₁) = no (λ ())

isK : ∀ k → Dec (aK k)
-- Generated by C-c C-a on:
-- isK k = {! -c !}
isK S = no (λ ())
isK K = yes IsK
isK (x ` x₁) = no (λ ())

isApp : ∀ k → Dec (App k)
-- Generated by C-c C-a on:
-- isApp k = {! -c !}
isApp S = no (λ ())
isApp K = no (λ ())
isApp (x ` x₁) = yes (IsApp x x₁)

isSApp : ∀ k → Dec (SApp k)
isSApp k with isApp k
... | no ¬p = no λ where (IsSApp a b) → ¬p (IsApp (S ` a) b)
... | yes (IsApp ab c) with isApp ab
... | no ¬p = no λ where (IsSApp a b) → ¬p (IsApp S a)
... | yes (IsApp a b) with isS a
... | no ¬p = no (λ where (IsSApp a b) → ¬p IsS)
... | yes IsS = yes (IsSApp b c)

isId : ∀ k → Dec (Id k)
isId k with isSApp k
... | no x = no (λ where IsId → x (IsSApp K K))
... | yes (IsSApp a b) with isK a | isK b
... | no ¬p | _ = no (λ where IsId → ¬p IsK)
... | _ | no ¬q = no (λ where IsId → ¬q IsK)
... | yes IsK | yes IsK = yes IsId