content: {-# LANGUAGE GADTs, DataKinds, KindSignatures, StandaloneDeriving, TypeFamilies,
      UndecidableInstances, RankNTypes #-}
  
  module Relevant where
  
  --------------------------------------------------------------------------
  -- NATURAL NUMBERS
  --------------------------------------------------------------------------
  
  -- usual type level numbers and singletons
  data Nat = Z | S Nat deriving Show
  data Natty :: Nat -> * where
    Zy :: Natty Z
    Sy :: Natty n -> Natty (S n)
  deriving instance Show (Natty n)
  class NATTY (n :: Nat) where
    natty :: Natty n
  instance NATTY Z where
    natty = Zy
  instance NATTY n => NATTY (S n) where
    natty = Sy natty
  
  
  --------------------------------------------------------------------------
  -- ORDER PRESERVING EMBEDDINGS
  --------------------------------------------------------------------------
  
  -- order preserving embeddings
  data OPE :: Nat -> Nat -> * where
    OPEI :: Natty n -> OPE n n
    OPES :: OPE n m -> OPE (S n) (S m)
    OPE' :: OPE n m -> OPE n (S m)
  deriving instance Show (OPE n m)
  
  -- smart constructor maximizing use of OPEI
  opeS :: OPE n m -> OPE (S n) (S m)
  opeS (OPEI n) = OPEI (Sy n)
  opeS p        = OPES p
  
  -- finding both ends of an OPE
  opeEnds :: OPE n m -> (Natty n, Natty m)
  opeEnds (OPEI n) = (n, n)
  opeEnds (OPES p) = case opeEnds p of
    (n, m) -> (Sy n, Sy m)
  opeEnds (OPE' p) = case opeEnds p of
    (n, m) -> (n, Sy m)
  
  -- composition of OPEs
  (<^>) :: OPE m p -> OPE n m -> OPE n p
  OPEI _ <^> q      = q
  p      <^> OPEI _ = p
  OPES p <^> OPES q = opeS (p <^> q)
  OPES p <^> OPE' q = OPE' (p <^> q)
  OPE' p <^> q      = OPE' (p <^> q)
  
  -- OPEs from empty
  nOPE :: Natty n -> OPE Z n
  nOPE Zy     = OPEI Zy
  nOPE (Sy n) = OPE' (nOPE n)
  
  
  --------------------------------------------------------------------------
  -- LAMBDA CALCULUS
  --------------------------------------------------------------------------
  
  -- Finite sets are OPEs from one
  type Fin = OPE (S Z)
  fZ :: NATTY n => Fin (S n)
  fZ = opeS (nOPE natty)
  fS :: Fin n -> Fin (S n)
  fS = OPE'
  
  -- Yer traditional well scoped lambda terms
  data Tm :: Nat -> * where
    V :: Fin n -> Tm n
    (:$) :: Tm n -> Tm n -> Tm n
    L :: Tm (S n) -> Tm n
  deriving instance Show (Tm n)
  
  
  --------------------------------------------------------------------------
  -- OPE COPRODUCTS
  --------------------------------------------------------------------------
  
  -- Encoding pairs of OPEs with the same target,
  -- ensuring that the target is *covered*.
  data OPE2 :: Nat -> Nat -> Nat -> * where
    OPEII :: Natty m -> OPE2 m m m
    OPESS :: OPE2 n n' m -> OPE2 (S n) (S n') (S m)
    OPES' :: OPE2 n n' m -> OPE2 (S n) n' (S m)
    OPE'S :: OPE2 n n' m -> OPE2 n (S n') (S m)
  deriving instance Show (OPE2 n n' m)
  
  -- smart constructor, ya da ya da
  opeSS :: OPE2 n n' m -> OPE2 (S n) (S n') (S m)
  opeSS (OPEII n) = OPEII (Sy n)
  opeSS p         = OPESS p
  
  -- extract left OPE
  lope :: OPE2 n n' m -> OPE n m
  lope (OPEII n) = OPEI n
  lope (OPESS p) = opeS (lope p)
  lope (OPES' p) = opeS (lope p)
  lope (OPE'S p) = OPE' (lope p)
  
  -- extract right OPE
  rope :: OPE2 n n' m -> OPE n' m
  rope (OPEII n) = OPEI n
  rope (OPESS p) = opeS (rope p)
  rope (OPES' p) = OPE' (rope p)
  rope (OPE'S p) = opeS (rope p)
  
  -- construct OPE2 full on left, empty on right
  alll :: Natty n -> OPE2 n Z n
  alll Zy     = OPEII Zy
  alll (Sy n) = OPES' (alll n)
  
  -- construct OPE2 empty on left, full on right
  allr :: Natty n -> OPE2 Z n n
  allr Zy     = OPEII Zy
  allr (Sy n) = OPE'S (allr n)
  
  -- if you have two OPEs targeting m', then we can compute the
  -- OPE2 which targets the union of their images, and the OPE which
  -- embeds *that* in m' (representing the points hit by neither);
  -- it's a kind of coproduct calculation, being the smallest thing
  -- supporting both injections
  
  data COPOPE :: Nat -> Nat -> Nat -> * where
    COPOPE :: OPE2 n n' m -> OPE m m' -> COPOPE n n' m'
  copOPE :: OPE n m' -> OPE n' m' -> COPOPE n n' m'
  copOPE (OPEI n) (OPEI _) = COPOPE (OPEII n)   (OPEI n)
  copOPE (OPEI (Sy n))   q = copOPE (OPES (OPEI n)) q
  copOPE p   (OPEI (Sy n)) = copOPE p (OPES (OPEI n))
  copOPE (OPES p) (OPES q) = case copOPE p q of
    COPOPE pq r -> COPOPE (opeSS pq) (opeS r)
  copOPE (OPES p) (OPE' q) = case copOPE p q of
    COPOPE pq r -> COPOPE (OPES' pq) (opeS r)
  copOPE (OPE' p) (OPES q) = case copOPE p q of
    COPOPE pq r -> COPOPE (OPE'S pq) (opeS r)
  copOPE (OPE' p) (OPE' q) = case copOPE p q of
    COPOPE pq r -> COPOPE pq (OPE' r)
  
  -- annoying lemma: if the sources of an OPE2 are nonzero,
  -- the target certainly is
  data OPE2SSS :: Nat -> Nat -> Nat -> * where
    OPE2SSS :: OPE2 (S n) (S n') (S m) -> OPE2SSS (S n) (S n') (S m)
  ope2SSS :: OPE2 (S n) (S n') m -> OPE2SSS (S n) (S n') m
  ope2SSS (OPEII n) = OPE2SSS (OPEII n)
  ope2SSS (OPESS p) = OPE2SSS (opeSS p)
  ope2SSS (OPES' p) = OPE2SSS (OPES' p)
  ope2SSS (OPE'S p) = OPE2SSS (OPE'S p)
  
  
  --------------------------------------------------------------------------
  -- UNDERGROUND RELEVANT TERMS
  --------------------------------------------------------------------------
  
  -- closed terms
  data Cl :: * where
    (:$$) :: Cl -> Cl -> Cl
    CL :: Un (S Z) -> Cl
    CK :: Cl -> Cl
  deriving instance Show Cl
  
  -- stations are either variables or junctions with action in both branches
  data St :: Nat -> * where
    It :: St (S Z)
    Ap :: OPE2 (S n) (S n') (S m) -> Un (S n) -> Un (S n') -> St (S m)
  deriving instance Show (St n)
  
  -- tubes binding n variables have only closed terms either side
  data Tu :: Nat -> * where
    TH :: Tu Z
    TL :: Tu m -> Tu (S m)
    TK :: Tu m -> Tu m
    TF :: Tu m -> Cl -> Tu m
    TA :: Cl -> Tu m -> Tu m
  deriving instance Show (Tu m)
  
  -- abacus addition adds number bound to number free
  type family Abacus (m :: Nat) (n :: Nat) :: Nat where
    Abacus Z n = n
    Abacus (S m) n = Abacus m (S n)
  
  -- underground relevant terms are either closed,
  -- or they're tubes which bring us to a station
  data Un :: Nat -> * where
    UC :: Cl -> Un Z
    UTJ :: Natty m -> Tu m -> St (Abacus m (S n)) -> Un (S n)
  deriving instance Show (Un n)
  
  -- for every term, we can find the variables it actually uses and
  -- build the underground relevant representation over just those,
  -- with the OPE that embeds back where we came from
  data TM :: Nat -> * where
    MkTM :: OPE n m -> Un n -> TM m
  deriving instance Show (TM n)
  
  tm :: Tm m -> TM m
  tm (V i) = MkTM i (UTJ Zy TH It)
  tm (L t) = case tm t of
    MkTM (OPE' r) (UC c)      -> MkTM r (UC (CK c))
    MkTM (OPE' r) (UTJ k t j) -> MkTM r (UTJ k (TK t) j)
    MkTM (OPES r) (UTJ k t j) -> case opeEnds r of
      (Zy, _)   -> MkTM r (UC (CL (UTJ k t j)))
      (Sy _, _) -> MkTM r (UTJ (Sy k) (TL t) j)
    MkTM (OPEI (Sy Zy))     (UTJ k t j) -> MkTM (OPEI Zy) (UC (CL (UTJ k t j)))
    MkTM (OPEI (Sy (Sy n))) (UTJ k t j) -> MkTM (OPEI (Sy n)) (UTJ (Sy k) (TL t) j)
  tm (f :$ s) = case (tm f, tm s) of
    (MkTM r (UC cf), MkTM _ (UC cs))     -> MkTM r (UC (cf :$$ cs))
    (MkTM _ (UC cf), MkTM r (UTJ k t j)) -> MkTM r (UTJ k (TA cf t) j)
    (MkTM r (UTJ k t j), MkTM _ (UC cs)) -> MkTM r (UTJ k (TF t cs) j)
    (MkTM r uf@(UTJ _ _ _), MkTM r' us@(UTJ _ _ _)) -> case copOPE r r' of
      COPOPE p pr -> case ope2SSS p of
        OPE2SSS p -> MkTM pr (UTJ Zy TH (Ap p uf us))
  
  -- we can still do a case analysis like it's a regular term, but
  -- we get a reliable distinction between vacuous and relevant abstraction
  caseUn :: Natty m ->
    p (S Z) ->
    (forall n n'. OPE2 n n' m -> Un n -> Un n' -> p m) ->
    (Un m -> p m) ->
    (Un (S m) -> p m) ->
    Un m -> p m
  caseUn m v a k l (UC (f :$$ s))         = a (OPEII Zy) (UC f) (UC s)
  caseUn m v a k l (UC (CK t))            = k (UC t)
  caseUn m v a k l (UC (CL u))            = l u
  caseUn m v a k l (UTJ Zy TH It)         = v
  caseUn m v a k l (UTJ Zy TH (Ap p f s)) = a p f s
  caseUn m v a k l (UTJ n (TK t) j)       = k (UTJ n t j)
  caseUn m v a k l (UTJ (Sy n) (TL t) j)  = l (UTJ n t j)
  caseUn m v a k l (UTJ n (TF t s) j)     = a (alll m) (UTJ n t j) (UC s)
  caseUn m v a k l (UTJ n (TA f t) j)     = a (allr m) (UC f) (UTJ n t j)
  
  