A simple implementation of non-nested patterns, desugaring to eliminators

Cases.idr

data Simplex : List a -> List a -> List a -> Type where
  Z : Simplex [] ys ys
  S : Simplex xs ys zs -> Simplex (x :: xs) ys (x :: zs)

data Ty : Type where
  Unit : Ty
  Prod : Ty -> Ty -> Ty
  Sum : Ty -> Ty -> Ty
  Hom : Ty -> Ty -> Ty

mutual
  namespace Cases
    public export
    -- `Cases a xs b` is something that case splits on a variable of type `a`,
    -- branches share free variables in `xs`, and the whole thing has type `b`
    data Cases : Ty -> List Ty -> Ty -> Type where
      Var : Term (a :: xs) b -> Cases a xs b
      Unit : Term xs a -> Cases Unit xs a
      Pair : Term (a :: b :: xs) c -> Cases (Prod a b) xs c
      Sum : Term (a :: xs) c -> Term (b :: xs) c -> Cases (Sum a b) xs c

  namespace Original
    public export
    data Term : List Ty -> Ty -> Type where
      Var : Term [x] x
      Let : Simplex xs ys zs -> Term xs a -> Cases a ys b -> Term zs b
      Pair : Simplex xs ys zs -> Term xs a -> Term ys b -> Term zs (Prod a b)
      Left : Term xs a -> Term xs (Sum a b)
      Right : Term xs b -> Term xs (Sum a b)
      Lambda : Cases a xs b -> Term xs (Hom a b)
      App : Simplex xs ys zs -> Term xs (Hom a b) -> Term ys a -> Term zs b
      
namespace Diet
  public export
  data Term : List Ty -> Ty -> Type where
    Var : Term [x] x
    Let : Simplex xs ys zs
       -> Diet.Term xs a -> Diet.Term (a :: ys) b -> Term zs b
    UnitIntro : Term [] Unit
    UnitElim : Simplex xs ys zs 
            -> Diet.Term xs Unit -> Diet.Term ys a -> Term zs a
    ProdIntro : Simplex xs ys zs 
             -> Diet.Term xs a -> Diet.Term ys b -> Diet.Term zs (Prod a b)
    ProdElim : Simplex xs ys zs 
            -> Diet.Term xs (Prod a b) -> Diet.Term (a :: b :: ys) c -> Term zs c
    SumIntroL : Diet.Term xs a -> Term xs (Sum a b)
    SumIntroR : Diet.Term xs b -> Term xs (Sum a b)
    SumElim : Simplex xs ys zs 
           -> Diet.Term xs (Sum a b) -> Diet.Term (a :: ys) c -> Diet.Term (b :: ys) c -> Diet.Term zs c
    HomIntro : Diet.Term (a :: xs) b -> Diet.Term xs (Hom a b)
    HomElim : Simplex xs ys zs
           -> Diet.Term xs (Hom a b) -> Diet.Term ys a -> Diet.Term zs b

mutual
  uncases : Cases a xs b -> Diet.Term (a :: xs) b
  uncases (Var t) = desugar t
  uncases (Unit t) = UnitElim (S Z) Var (desugar t)
  uncases (Pair t) = ProdElim (S Z) Var (desugar t)
  uncases (Sum t1 t2) = SumElim (S Z) Var (desugar t1) (desugar t2)

  desugar : Original.Term xs a -> Diet.Term xs a
  desugar Var = Var
  desugar (Let sx t c) = Let sx (desugar t) (uncases c)
  desugar (Pair sx t1 t2) = ProdIntro sx (desugar t1) (desugar t2)
  desugar (Left t) = SumIntroL (desugar t)
  desugar (Right t) = SumIntroR (desugar t)
  desugar (Lambda c) = HomIntro (uncases c)
  desugar (App sx t1 t2) = HomElim sx (desugar t1) (desugar t2)

Updated to include function types + lambda cases