Commit 9d78e10c authored by Gilles Coremans's avatar Gilles Coremans
Browse files

Add new generated code to FCO & Fi+ systems

- Modify Elaborate.hs to use the new code, not succesfully
- Add tests for FCO
parent 03d7bb26
{-# LANGUAGE GADTs, KindSignatures, NPlusKPatterns #-}
module Comble where
import qualified Data.Array as A
import Control.Applicative
type Card = Integer
data Comble :: * -> * where
Empty :: Comble e
Pure :: e -> Comble e
Alt :: Comble e -> Comble e -> Card -> Comble e
App :: Comble (arg -> e) -> Comble arg -> Card -> Comble e
card :: Comble e -> Card
card Empty = 0
card (Pure _) = 1
card (Alt _ _ n) = n
card (App _ _ n) = n
instance Functor Comble where
fmap f x = pure f <*> x
instance Applicative Comble where
pure x = Pure x
f <*> x = App f x (card f * card x)
instance Alternative Comble where
empty = Empty
t <|> u = Alt t u (card t + card u)
infixl 9 !
(!) :: Comble e -> Integer -> e
Pure x ! 0 = x
Alt t u _ ! k = if k < m then t ! k else u ! (k - m)
where m = card t
App t u _ ! k = (t ! (k `div` n)) (u ! (k `mod` n))
where n = card u
toList :: Comble e -> [e]
toList c = go c [] where
go Empty acc = acc
go (Pure x) acc = x : acc
go (Alt t u _) acc = go t (go u acc)
go (App (Pure fun) arg _) acc = (fun <$> (toList arg)) ++ acc
go (App fun arg _) acc = ((toList fun) <*> (toList arg)) ++ acc
splitn :: (Integral a) => Integer -> a -> [[a]]
splitn 0 _ = [[0]] -- This function is used to distribute sizes over branches, returning 0 here means only size-0, eg 'empty' can be generated.
splitn 1 x = [[x]]
splitn n x = concatMap (\y -> map (y:) $ splitn (n-1) (x-y)) [1..(x-1)]
asum :: [Comble val] -> Comble val
asum = foldr (<|>) empty
......@@ -6,57 +6,12 @@ module Elaborate
, goodelaborate
) where
import Fi
import FiImpl
import Variables
import FiSorts as Fi
import FCoSorts as Co
import FiImpl
data Term
= TmVarCo HNat
| TmAbsCo Term
Type
| TmAppCo Term
Term
| TmTAppCo Term
Type
| TmTAbsCo Term
| TmTopCo
| TmTupleCo Term
Term
| TmIntCo Int
| TmCast Coercion
Term
deriving (Show, Eq)
data Type
= TyVarCo HNat
| TyArrCo Type
Type
| TyAllCo Type
| TyIntCo
| TyTopCo
| TyProdCo Type
Type
deriving (Show, Eq)
data Coercion
= CoId
| CoTrans Coercion
Coercion
| CoTop
| CoBot
| CoArrow Coercion
Coercion
| CoTuple Coercion
Coercion
| CoProj1
| CoProj2
| CoAll Coercion
| CoDistArrow
| CoTopArrow
| CoTopAll
| CoDistAll
deriving (Show, Eq)
getTypeFromEnv :: Env -> HNat -> Either String FiType
getTypeFromEnv :: Env -> Variable -> Either String FiType
getTypeFromEnv (ETermVar ty _) Z = return ty
getTypeFromEnv _ Z = Left "wrong or no binding for FiTerm"
getTypeFromEnv (ETermVar _ rest) (STermVar h) = getTypeFromEnv rest h
......@@ -65,52 +20,52 @@ getTypeFromEnv (ETypeVar _ rest) (STypeVar h) = getTypeFromEnv rest h
getTypeFromEnv _ (STypeVar h) = Left "No variable FiType"
elaborate :: FiTerm -> Env -> Either String Term
elaborate TmTop ctx = return TmTopCo
elaborate (TmInt i) ctx = return (TmIntCo i)
elaborate (TmVar hnat) ctx = return (TmVarCo hnat)
elaborate (TmAbs t ty) ctx = do
elaborate Fi.TmTop ctx = return Co.TmTop
elaborate (Fi.TmInt i) ctx = return (Co.TmInt i)
elaborate (Fi.TmVar hnat) ctx = return (Co.TmVar hnat)
elaborate (Fi.TmAbs t ty) ctx = do
term <- elaborate t (ETermVar ty ctx)
return (TmAbsCo term (convertType ty))
elaborate (TmApp t1 t2) ctx = do
return (Co.TmAbs term (convertType ty))
elaborate (Fi.TmApp t1 t2) ctx = do
term1 <- elaborate t1 ctx
term2 <- elaborate t2 ctx
ty2 <- typeOf t2 ctx
case typeOf t1 ctx of
Right (TyArr ty3 ty4) -> do
Right (Fi.TyArr ty3 ty4) -> do
a <- (algoSubtypingCo EmptyQueue ty2 ty3)
return (TmAppCo term1 (TmCast a term2))
return (Co.TmApp term1 (Co.TmCast a term2))
_ -> Left "Wrong use of elaborate"
elaborate (TmMerge t1 t2) ctx = do
elaborate (Fi.TmMerge t1 t2) ctx = do
term1 <- elaborate t1 ctx
term2 <- elaborate t2 ctx
return (TmTupleCo term1 term2)
elaborate (TmRecord t str) ctx = do
return (Co.TmTuple term1 term2)
elaborate (Fi.TmRecord t str) ctx = do
term <- elaborate t ctx
return term
elaborate (TmProj t str) ctx = do
elaborate (Fi.TmProj t str) ctx = do
term <- elaborate t ctx
return term
elaborate (TmAnn t ty) ctx = do
elaborate (Fi.TmAnn t ty) ctx = do
tyt <- typeOf t ctx
term <- elaborate t ctx
sub <- (algoSubtypingCo EmptyQueue tyt ty)
return (TmCast sub term)
return (Co.TmCast sub term)
elaborate (TypeApp t ty) ctx = do
term <- elaborate t ctx
return (TmTAppCo term (convertType ty))
elaborate (TmAll ty t) ctx = do
return (Co.TmTApp term (convertType ty))
elaborate (Fi.TmAll ty t) ctx = do
term <- elaborate t (ETypeVar ty ctx)
return (TmTAbsCo term)
return (Co.TmTAbs term)
convertType :: FiType -> Type
convertType TyInt = TyIntCo
convertType (TyAnd ty1 ty2) = TyProdCo (convertType ty1) (convertType ty2)
convertType TyBot = TyAllCo (TyVarCo Z)
convertType TyTop = TyTopCo
convertType (TyRecord ty _) = convertType ty
convertType (TyVar hnat) = TyVarCo hnat
convertType (TyArr ty1 ty2) = TyArrCo (convertType ty1) (convertType ty2)
convertType (TyAll ty tyB) = TyAllCo (convertType tyB)
convertType Fi.TyInt = Co.TyInt
convertType (Fi.TyAnd ty1 ty2) = Co.TyProd (convertType ty1) (convertType ty2)
convertType Fi.TyBot = Co.TyAll (Co.TyVar Z)
convertType Fi.TyTop = Co.TyTop
convertType (Fi.TyRecord ty _) = convertType ty
convertType (Fi.TyVar hnat) = Co.TyVar hnat
convertType (Fi.TyArr ty1 ty2) = Co.TyArr (convertType ty1) (convertType ty2)
convertType (Fi.TyAll ty tyB) = Co.TyAll (convertType tyB)
pushQueue :: Queue -> Queue -> Queue
pushQueue EmptyQueue q = q
......@@ -119,45 +74,45 @@ pushQueue (TypeQueue ty q) newq = TypeQueue ty (pushQueue q newq)
pushQueue (TypeStarQueue ty q) newq = TypeStarQueue ty (pushQueue q newq)
isTypeConstant :: FiType -> Bool
isTypeConstant TyInt = True
isTypeConstant TyBot = True
isTypeConstant (TyVar _) = True
isTypeConstant Fi.TyInt = True
isTypeConstant Fi.TyBot = True
isTypeConstant (Fi.TyVar _) = True
isTypeConstant _ = False
algoSubtypingCo :: Queue -> FiType -> FiType -> Either String Coercion
algoSubtypingCo q tyA TyTop = do
algoSubtypingCo q tyA Fi.TyTop = do
a <- (calcQueueTop q)
return (CoTrans a (CoTop))
algoSubtypingCo q tyA (TyAnd ty1 ty2) = do
algoSubtypingCo q tyA (Fi.TyAnd ty1 ty2) = do
a <- (algoSubtypingCo q tyA ty1)
b <- (algoSubtypingCo q tyA ty2)
c <- (calcQueueAnd q)
return (CoTrans c (CoTuple a b))
algoSubtypingCo q tyA (TyArr ty1 ty2) =
algoSubtypingCo q tyA (Fi.TyArr ty1 ty2) =
algoSubtypingCo (pushQueue q (TypeQueue ty1 EmptyQueue)) tyA ty2
algoSubtypingCo EmptyQueue tyA tyB
| tyA == tyB && isTypeConstant tyA = return CoId
algoSubtypingCo q TyBot c
algoSubtypingCo q Fi.TyBot c
| isTypeConstant c = return CoBot
algoSubtypingCo q tyA (TyRecord tyB str) =
algoSubtypingCo q tyA (Fi.TyRecord tyB str) =
algoSubtypingCo (pushQueue q (LabelQueue str EmptyQueue)) tyA tyB
algoSubtypingCo q tyA (TyAll ty1 ty2) =
algoSubtypingCo q tyA (Fi.TyAll ty1 ty2) =
algoSubtypingCo (pushQueue q (TypeStarQueue ty1 EmptyQueue)) tyA ty2
algoSubtypingCo (TypeQueue ty q) (TyArr ty1 ty2) tyB
algoSubtypingCo (TypeQueue ty q) (Fi.TyArr ty1 ty2) tyB
| isTypeConstant tyB = do
a <- (algoSubtypingCo EmptyQueue ty ty1)
b <- (algoSubtypingCo q ty2 tyB)
return (CoArrow a b)
algoSubtypingCo (LabelQueue str1 q) (TyRecord ty2 str2) tyB
algoSubtypingCo (LabelQueue str1 q) (Fi.TyRecord ty2 str2) tyB
| isTypeConstant tyB && str1 == str2 = algoSubtypingCo q ty2 tyB
algoSubtypingCo q (TyAnd ty1 ty2) tyB
algoSubtypingCo q (Fi.TyAnd ty1 ty2) tyB
| isTypeConstant tyB && algoSubtyping q ty1 tyB = do
a <- (algoSubtypingCo q ty1 tyB)
return (CoTrans a (CoProj1))
| isTypeConstant tyB && algoSubtyping q ty2 tyB = do
a <- (algoSubtypingCo q ty2 tyB)
return (CoTrans a (CoProj2))
algoSubtypingCo (TypeStarQueue ty q) (TyAll ty1 ty2) tyB
algoSubtypingCo (TypeStarQueue ty q) (Fi.TyAll ty1 ty2) tyB
| isTypeConstant tyB = do
a <- (algoSubtypingCo q ty2 tyB)
return (CoAll a)
......
module FCO
( Env(..)
, HNat(..)
, Coercion(..)
, coerciontypeSubstitute
, freeVariablesCoercion
, coercionshiftplus
, coercionshiftminus
, Type(..)
, typetypeSubstitute
, freeVariablesType
, typeshiftplus
, typeshiftminus
, Term(..)
, termtermSubstitute
, termtypeSubstitute
, freeVariablesTerm
, termshiftplus
, termshiftminus
, generateHnatTypeVar
, generateHnatTermVar
) where
import Data.List
data Coercion
= CoId
| CoTrans Coercion
Coercion
| CoTop Type
| CoBot Type
| CoArrow Coercion
Coercion
| CoTuple Coercion
Coercion
| CoProj1 Type
| CoProj2 Type
| CoAll Coercion
| CoDistArrow
| CoTopArrow
| CoTopAll
| CoDistAll
deriving (Show, Eq)
data Type
= TyVar HNat
| TyArr Type
Type
| TyAll Type
| TyInt
| TyTop
| TyProd Type
Type
deriving (Show, Eq)
data Term
= TmVar HNat
| TmAbs Term
Type
| TmApp Term
Term
| TmTApp Term
Type
| TmTAbs Term
| TmTop
| TmTuple Term
Term
| TmInt Int
| TmCast Coercion
Term
deriving (Show, Eq)
data HNat
= Z
| STypeVar HNat
| STermVar HNat
deriving (Show, Eq)
plus x1 (STypeVar x2) = STypeVar (plus x1 x2)
plus x1 (STermVar x2) = STermVar (plus x1 x2)
plus Z h = h
plus h Z = h
instance Ord HNat where
compare (STypeVar h1) (STypeVar h2) = compare h1 h2
compare (STypeVar h1) (STermVar h2) =
error "differing namespace found in compare "
compare (STermVar h1) (STypeVar h2) =
error "differing namespace found in compare "
compare (STermVar h1) (STermVar h2) = compare h1 h2
compare Z Z = EQ
compare Z _ = LT
compare _ Z = GT
minus (STypeVar h1) (STypeVar h2) = minus h1 h2
minus (STypeVar h1) (STermVar h2) = error "differing namespace found in minus "
minus (STermVar h1) (STypeVar h2) = error "differing namespace found in minus "
minus (STermVar h1) (STermVar h2) = minus h1 h2
minus Z Z = Z
minus Z _ = error " You cannot substract zero with a positive number "
minus result Z = result
data Env
= Nil
| ETypeVar Env
| ETermVar Type
Env
deriving (Show, Eq)
generateHnatTypeVar 0 c = c
generateHnatTypeVar n c = STypeVar (generateHnatTypeVar (n - 1) c)
generateHnatTermVar 0 c = c
generateHnatTermVar n c = STermVar (generateHnatTermVar (n - 1) c)
coercionmap :: (HNat -> Type -> Type) -> HNat -> Coercion -> Coercion
coercionmap onTypeVar c (CoId) = CoId
coercionmap onTypeVar c (CoTrans co1 co2) =
CoTrans (coercionmap onTypeVar c co1) (coercionmap onTypeVar c co2)
coercionmap onTypeVar c (CoTop ty) = CoTop (typemap onTypeVar c ty)
coercionmap onTypeVar c (CoBot ty) = CoBot (typemap onTypeVar c ty)
coercionmap onTypeVar c (CoArrow co1 co2) =
CoArrow (coercionmap onTypeVar c co1) (coercionmap onTypeVar c co2)
coercionmap onTypeVar c (CoTuple co1 co2) =
CoTuple (coercionmap onTypeVar c co1) (coercionmap onTypeVar c co2)
coercionmap onTypeVar c (CoProj1 ty2) = CoProj1 (typemap onTypeVar c ty2)
coercionmap onTypeVar c (CoProj2 ty1) = CoProj2 (typemap onTypeVar c ty1)
coercionmap onTypeVar c (CoAll co1) = CoAll (coercionmap onTypeVar c co1)
coercionmap onTypeVar c (CoDistArrow) = CoDistArrow
coercionmap onTypeVar c (CoTopArrow) = CoTopArrow
coercionmap onTypeVar c (CoTopAll) = CoTopAll
coercionmap onTypeVar c (CoDistAll) = CoDistAll
typemap :: (HNat -> Type -> Type) -> HNat -> Type -> Type
typemap onTypeVar c (TyVar hnat) = onTypeVar c (TyVar hnat)
typemap onTypeVar c (TyArr t1 t2) =
TyArr (typemap onTypeVar c t1) (typemap onTypeVar c t2)
typemap onTypeVar c (TyAll t1) = TyAll (typemap onTypeVar (STypeVar c) t1)
typemap onTypeVar c (TyInt) = TyInt
typemap onTypeVar c (TyTop) = TyTop
typemap onTypeVar c (TyProd t1 t2) =
TyProd (typemap onTypeVar c t1) (typemap onTypeVar c t2)
termmap ::
(HNat -> Term -> Term) -> (HNat -> Type -> Type) -> HNat -> Term -> Term
termmap onTermVar onTypeVar c (TmVar hnat) = onTermVar c (TmVar hnat)
termmap onTermVar onTypeVar c (TmAbs x t) =
TmAbs (termmap onTermVar onTypeVar (STermVar c) x) (typemap onTypeVar c t)
termmap onTermVar onTypeVar c (TmApp t1 t2) =
TmApp (termmap onTermVar onTypeVar c t1) (termmap onTermVar onTypeVar c t2)
termmap onTermVar onTypeVar c (TmTApp t1 t) =
TmTApp (termmap onTermVar onTypeVar c t1) (typemap onTypeVar c t)
termmap onTermVar onTypeVar c (TmTAbs t1) =
TmTAbs (termmap onTermVar onTypeVar (STypeVar c) t1)
termmap onTermVar onTypeVar c (TmTop) = TmTop
termmap onTermVar onTypeVar c (TmTuple e1 e2) =
TmTuple (termmap onTermVar onTypeVar c e1) (termmap onTermVar onTypeVar c e2)
termmap onTermVar onTypeVar c (TmInt int0) = TmInt int0
termmap onTermVar onTypeVar c (TmCast co e) =
TmCast (coercionmap onTypeVar c co) (termmap onTermVar onTypeVar c e)
typeshiftHelpplus d c (TyVar hnat)
| hnat >= c = TyVar (plus hnat d)
| otherwise = TyVar hnat
termshiftHelpplus d c (TmVar hnat)
| hnat >= c = TmVar (plus hnat d)
| otherwise = TmVar hnat
coercionshiftplus :: HNat -> Coercion -> Coercion
coercionshiftplus d t = coercionmap (typeshiftHelpplus d) Z t
typeshiftplus :: HNat -> Type -> Type
typeshiftplus d t = typemap (typeshiftHelpplus d) Z t
termshiftplus :: HNat -> Term -> Term
termshiftplus d t = termmap (termshiftHelpplus d) (typeshiftHelpplus d) Z t
typeshiftHelpminus d c (TyVar hnat)
| hnat >= c = TyVar (minus hnat d)
| otherwise = TyVar hnat
termshiftHelpminus d c (TmVar hnat)
| hnat >= c = TmVar (minus hnat d)
| otherwise = TmVar hnat
coercionshiftminus :: HNat -> Coercion -> Coercion
coercionshiftminus d t = coercionmap (typeshiftHelpminus d) Z t
typeshiftminus :: HNat -> Type -> Type
typeshiftminus d t = typemap (typeshiftHelpminus d) Z t
termshiftminus :: HNat -> Term -> Term
termshiftminus d t = termmap (termshiftHelpminus d) (typeshiftHelpminus d) Z t
typeSubstituteHelp sub orig c (TyVar hnat)
| hnat == plus orig c = typeshiftplus c sub
| otherwise = TyVar hnat
termSubstituteHelp sub orig c (TmVar hnat)
| hnat == plus orig c = termshiftplus c sub
| otherwise = TmVar hnat
coerciontypeSubstitute :: Type -> HNat -> Coercion -> Coercion
coerciontypeSubstitute sub orig t =
coercionmap (typeSubstituteHelp sub orig) Z t
typetypeSubstitute :: Type -> HNat -> Type -> Type
typetypeSubstitute sub orig t = typemap (typeSubstituteHelp sub orig) Z t
termtermSubstitute :: Term -> HNat -> Term -> Term
termtermSubstitute sub orig t =
termmap (termSubstituteHelp sub orig) (\c x -> x) Z t
termtypeSubstitute :: Type -> HNat -> Term -> Term
termtypeSubstitute sub orig t =
termmap (\c x -> x) (typeSubstituteHelp sub orig) Z t
freeVariablesCoercion :: HNat -> Coercion -> [HNat]
freeVariablesCoercion c (CoId) = nub ([])
freeVariablesCoercion c (CoTrans co1 co2) =
nub ((freeVariablesCoercion c co1) ++ (freeVariablesCoercion c co2))
freeVariablesCoercion c (CoTop ty) = nub ((freeVariablesType c ty))
freeVariablesCoercion c (CoBot ty) = nub ((freeVariablesType c ty))
freeVariablesCoercion c (CoArrow co1 co2) =
nub ((freeVariablesCoercion c co1) ++ (freeVariablesCoercion c co2))
freeVariablesCoercion c (CoTuple co1 co2) =
nub ((freeVariablesCoercion c co1) ++ (freeVariablesCoercion c co2))
freeVariablesCoercion c (CoProj1 ty2) = nub ((freeVariablesType c ty2))
freeVariablesCoercion c (CoProj2 ty1) = nub ((freeVariablesType c ty1))
freeVariablesCoercion c (CoAll co1) = nub ((freeVariablesCoercion c co1))
freeVariablesCoercion c (CoDistArrow) = nub ([])
freeVariablesCoercion c (CoTopArrow) = nub ([])
freeVariablesCoercion c (CoTopAll) = nub ([])
freeVariablesCoercion c (CoDistAll) = nub ([])
freeVariablesType :: HNat -> Type -> [HNat]
freeVariablesType c (TyVar hnat)
| hnat >= c = [minus hnat c]
| otherwise = []
freeVariablesType c (TyArr t1 t2) =
nub ((freeVariablesType c t1) ++ (freeVariablesType c t2))
freeVariablesType c (TyAll t1) = nub ((freeVariablesType (STypeVar c) t1))
freeVariablesType c (TyInt) = nub ([])
freeVariablesType c (TyTop) = nub ([])
freeVariablesType c (TyProd t1 t2) =
nub ((freeVariablesType c t1) ++ (freeVariablesType c t2))
freeVariablesTerm :: HNat -> Term -> [HNat]
freeVariablesTerm c (TmVar hnat)
| hnat >= c = [minus hnat c]
| otherwise = []
freeVariablesTerm c (TmAbs x t) =
nub ((freeVariablesTerm (STermVar c) x) ++ (freeVariablesType c t))
freeVariablesTerm c (TmApp t1 t2) =
nub ((freeVariablesTerm c t1) ++ (freeVariablesTerm c t2))
freeVariablesTerm c (TmTApp t1 t) =
nub ((freeVariablesTerm c t1) ++ (freeVariablesType c t))
freeVariablesTerm c (TmTAbs t1) = nub ((freeVariablesTerm (STypeVar c) t1))
freeVariablesTerm c (TmTop) = nub ([])
freeVariablesTerm c (TmTuple e1 e2) =
nub ((freeVariablesTerm c e1) ++ (freeVariablesTerm c e2))
freeVariablesTerm c (TmInt _) = nub ([])
freeVariablesTerm c (TmCast co e) =
nub ((freeVariablesCoercion c co) ++ (freeVariablesTerm c e))
module HaskellOutputFCoSecond
module FCoImpl
( Term(..)
, Type(..)
, Coercion(..)
, isVal
, stepEval
, typeOf
, fullEval
, HNat(..)
, Variable(..)
, Env(..)
) where
import FCO
import FCoSorts
import Variables
data Env
= Nil
| ETypeVar Env
| ETermVar Type
Env
deriving (Show, Eq)
isVal :: Term -> Bool
isVal (TmAbs x t) = True
......@@ -23,7 +33,7 @@ isVal (TmCast (CoTopArrow) e) = isVal e
isVal (TmCast (CoDistAll) e) = isVal e
isVal _ = False
getTypeFromEnv :: Env -> HNat -> Either String Type
getTypeFromEnv :: Env -> Variable -> Either String Type
getTypeFromEnv (ETermVar ty _) Z = return ty
getTypeFromEnv _ Z = Left "wrong or no binding for term"
getTypeFromEnv (ETermVar _ rest) (STermVar h) = getTypeFromEnv rest h
......@@ -39,13 +49,13 @@ stepEval (TmApp (TmAbs t ty) t2)
Just
(termshiftminus
(STermVar Z)
(termtermSubstitute (termshiftplus (STermVar Z) t2) Z t))
(termTermSubstitute (termshiftplus (STermVar Z) t2) Z t))
--type application
stepEval (TmTApp (TmTAbs t) ty) =
Just
(termshiftminus
(STypeVar Z)
(termtypeSubstitute (typeshiftplus (STypeVar Z) ty) Z t))
(termTypeSubstitute (typeshiftplus (STypeVar Z) ty) Z t))
--R-proj1
stepEval (TmCast (CoProj1 ty) (TmTuple e1 e2))
| not (isVal e1) = do
......@@ -247,7 +257,7 @@ typeOf (TmTApp t ty) ctx =
return
(typeshiftminus
(STypeVar Z)
(typetypeSubstitute (typeshiftplus (STypeVar Z) ty) Z ty2))
(typeTypeSubstitute (typeshiftplus (STypeVar Z) ty) Z ty2))
Left a -> Left a
_ -> Left "not a type abstraction"
typeOf (TmTAbs t) ctx = do
......
module FCoSorts where
import Data.List
import Control.Applicative
import Comble
import Test.QuickCheck
import Variables
data Term = TmVar Variable
| TmAbs Term Type
| TmApp Term Term
| TmTApp Term Type
| TmTAbs Term
| TmTop
| TmTuple Term Term
| TmInt Int
| TmCast Coercion