Skip to content

Instantly share code, notes, and snippets.

@takanuva
Created February 12, 2019 22:38
Show Gist options
  • Save takanuva/f09111e2693da64d0fdb9af0b2394053 to your computer and use it in GitHub Desktop.
Save takanuva/f09111e2693da64d0fdb9af0b2394053 to your computer and use it in GitHub Desktop.
CPS for the CoC
-- 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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment