CPS for the CoC

excerpt.hs

-- The language of sorts (S, T, U)
data Sort = Prop
          | SortPi1 String Type Sort
          | SortPi2 String Sort Sort

-- The language of types (A, B, D)
data Type = TypeBound Int
          | TypeApplication1 Type Term
          | TypeApplication2 Type Type
          | TypeLambda1 String Type Type
          | TypeLambda2 String Sort Type
          | TypePi1 String Type Type
          | TypePi2 String Sort Type

-- The language of terms (M, N, P)
data Term = TermBound Int
          | TermApplication1 Term Term
          | TermApplication2 Term Type
          | TermLambda1 String Type Term
          | TermLambda2 String Sort Term

class CPSConv1 a where
  cps_barthe' :: Monad m => Context -> a -> StateT Int m a

instance CPSConv1 Sort where
  cps_barthe' g (Prop) =
    return Prop
  cps_barthe' g (SortPi1 s t b) = do
    t' <- cps_barthe' g t
    b' <- cps_barthe' (shift ((s, Type t):g)) b
    return $ SortPi1 s (negation (negation t')) b'
  cps_barthe' g (SortPi2 s t b) = do
    t' <- cps_barthe' g t
    b' <- cps_barthe' (shift ((s, Sort t):g)) b
    return $ SortPi2 s t' b'

instance CPSConv1 Type where
  cps_barthe' g e@(TypeBound n) =
    return e
  cps_barthe' g (TypeApplication1 f x) = do
    f' <- cps_barthe' g f
    x' <- cps_barthe' g x
    return $ TypeApplication1 f' x'
  cps_barthe' g (TypeApplication2 f x) = do
    f' <- cps_barthe' g f
    x' <- cps_barthe' g x
    return $ TypeApplication2 f' x'
  cps_barthe' g (TypeLambda1 s t b) = do
    t' <- cps_barthe' g t
    b' <- cps_barthe' (shift ((s, Type t):g)) b
    return $ TypeLambda1 s (negation (negation t')) b'
  cps_barthe' g (TypeLambda2 s t b) = do
    t' <- cps_barthe' g t
    b' <- cps_barthe' (shift ((s, Sort t):g)) b
    return $ TypeLambda2 s t' b'
  cps_barthe' g (TypePi1 s t b) = do
    t' <- cps_barthe' g t
    b' <- cps_barthe' (shift ((s, Type t):g)) b
    return $ TypePi1 s (negation (negation t')) (negation (negation b'))
  cps_barthe' g (TypePi2 s t b) = do
    t' <- cps_barthe' g t
    b' <- cps_barthe' (shift ((s, Sort t):g)) b
    return $ TypePi2 s t' (negation (negation b'))

instance CPSConv1 Term where
  cps_barthe' g e@(TermBound n) = do
    k <- fresh "k"
    et' <- cps_barthe' g et
    return $
      TermLambda1 k (negation et') $
        (TermApplication1 (shift e) $
          (TermBound 0))
    where
      Right (Type et) = typeof g e
  cps_barthe' g e@(TermApplication1 f x) = do
    k <- fresh "k"
    j <- fresh "j"
    et' <- cps_barthe' g et
    f' <- cps_barthe' g f
    ft' <- cps_barthe' g ft
    x' <- cps_barthe' g x
    return $ TermLambda1 k (negation et') (TermApplication1 (shift f') (
               TermLambda1 j (shift ft') (TermApplication1 (TermApplication1 (TermBound 0) (shift (shift x'))) (TermBound 1))
             ))
    where
      Right (Type et) = typeof g e
      Right (Type ft) = typeof g f
  cps_barthe' g e@(TermApplication2 f x) = do
    k <- fresh "k"
    j <- fresh "j"
    et' <- cps_barthe' g et
    f' <- cps_barthe' g f
    ft' <- cps_barthe' g ft
    x' <- cps_barthe' g x
    return $ TermLambda1 k (negation et') (TermApplication1 (shift f') (
               TermLambda1 j (shift ft') (TermApplication1 (TermApplication2 (TermBound 0) (shift (shift x'))) (TermBound 1))
             ))
    where
      Right (Type et) = typeof g e
      Right (Type ft) = typeof g f
  cps_barthe' g e@(TermLambda1 s t b) = do
    k <- fresh "k"
    et' <- cps_barthe' g et
    t' <- cps_barthe' g t
    b' <- cps_barthe' (shift ((s, Type t):g)) b
    return $
      TermLambda1 k (negation et') $
        (TermApplication1 (TermBound 0) $
          (shift (TermLambda1 s (negation (negation t')) b')))
    where
      Right (Type et) = typeof g e
  cps_barthe' g e@(TermLambda2 s t b) = do
    k <- fresh "k"
    et' <- cps_barthe' g et
    t' <- cps_barthe' g t
    b' <- cps_barthe' (shift ((s, Sort t):g)) b
    return $
      TermLambda1 k (negation et') $
        (TermApplication1 (TermBound 0) $
          (shift (TermLambda2 s t' b')))
    where
      Right (Type et) = typeof g e