Use updated FCo and Fi+ specifications for their implementation

FCO/Elaborate.hs

-module Elaborate
-  ( Term(..)
-  , Type(..)
-  , Coercion(..)
-  , elaborate
-  , goodelaborate
-  ) where
+module Elaborate where
 
-import           Fi
-import           FiImpl
+import           FCoBase
+import qualified FiPlusBase as FP
+import qualified FiImpl as FIm
 
-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)
+varTranslate :: FP.Variable -> Variable
+varTranslate FP.Z              = Z
+varTranslate (FP.STermVar var) = STermVar (varTranslate var)
+varTranslate (FP.STypeVar var) = STypeVar (varTranslate var)
 
-data Type
-  = TyVarCo HNat
-  | TyArrCo Type
-            Type
-  | TyAllCo Type
-  | TyIntCo
-  | TyTopCo
-  | TyProdCo Type
-             Type
-  deriving (Show, Eq)
+getTypeFromEnv :: FIm.Env -> FP.Variable -> Either String FP.FiType
+getTypeFromEnv (FIm.ETermVar ty _) FP.Z = return ty
+getTypeFromEnv _ FP.Z = Left "wrong or no binding for FiTerm"
+getTypeFromEnv (FIm.ETermVar _ rest) (FP.STermVar h) = getTypeFromEnv rest h
+getTypeFromEnv _ (FP.STermVar h) = Left "wrong FiTerm binding"
+getTypeFromEnv (FIm.ETypeVar _ rest) (FP.STypeVar h) = getTypeFromEnv rest h
+getTypeFromEnv _ (FP.STypeVar h) = Left "No variable FP.FiType"
 
-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 (ETermVar ty _) Z = return ty
-getTypeFromEnv _ Z = Left "wrong or no binding for FiTerm"
-getTypeFromEnv (ETermVar _ rest) (STermVar h) = getTypeFromEnv rest h
-getTypeFromEnv _ (STermVar h) = Left "wrong FiTerm binding"
-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
-  term <- elaborate t (ETermVar ty ctx)
-  return (TmAbsCo term (convertType ty))
-elaborate (TmApp t1 t2) ctx = do
+elaborate :: FP.FiTerm -> FIm.Env -> Either String Term
+elaborate FP.TmTop ctx = return TmTop
+elaborate (FP.TmInt i) ctx = return (TmInt i)
+elaborate (FP.TmVar hnat) ctx = return (TmVar (varTranslate hnat))
+elaborate (FP.TmAbs t ty) ctx = do
+  term <- elaborate t (FIm.ETermVar ty ctx)
+  return (TmAbs term (convertType ty))
+elaborate (FP.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
-      a <- (algoSubtypingCo EmptyQueue ty2 ty3)
-      return (TmAppCo term1 (TmCast a term2))
+  ty2 <- FIm.typeOf t2 ctx
+  case FIm.typeOf t1 ctx of
+    Right (FP.TyArr ty3 ty4) -> do
+      a <- (algoSubtypingCo FIm.EmptyQueue ty2 ty3)
+      return (TmApp term1 (TmCast a term2))
     _ -> Left "Wrong use of elaborate"
-elaborate (TmMerge t1 t2) ctx = do
+elaborate (FP.TmMerge t1 t2) ctx = do
   term1 <- elaborate t1 ctx
   term2 <- elaborate t2 ctx
-  return (TmTupleCo term1 term2)
-elaborate (TmRecord t str) ctx = do
+  return (TmTuple term1 term2)
+elaborate (FP.TmRecord t str) ctx = do
   term <- elaborate t ctx
   return term
-elaborate (TmProj t str) ctx = do
+elaborate (FP.TmProj t str) ctx = do
   term <- elaborate t ctx
   return term
-elaborate (TmAnn t ty) ctx = do
-  tyt <- typeOf t ctx
+elaborate (FP.TmAnn t ty) ctx = do
+  tyt <- FIm.typeOf t ctx
   term <- elaborate t ctx
-  sub <- (algoSubtypingCo EmptyQueue tyt ty)
+  sub <- (algoSubtypingCo FIm.EmptyQueue tyt ty)
   return (TmCast sub term)
-elaborate (TypeApp t ty) ctx = do
+elaborate (FP.TypeApp t ty) ctx = do
   term <- elaborate t ctx
-  return (TmTAppCo term (convertType ty))
-elaborate (TmAll ty t) ctx = do
-  term <- elaborate t (ETypeVar ty ctx)
-  return (TmTAbsCo term)
+  return (TmTApp term (convertType ty))
+elaborate (FP.TmAll ty t) ctx = do
+  term <- elaborate t (FIm.ETypeVar ty ctx)
+  return (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 :: FP.FiType -> Type
+convertType FP.TyInt           = TyInt
+convertType (FP.TyAnd ty1 ty2) = TyProd (convertType ty1) (convertType ty2)
+convertType FP.TyBot           = TyAll (TyVar Z)
+convertType FP.TyTop           = TyTop
+convertType (FP.TyRecord ty _) = convertType ty
+convertType (FP.TyVar hnat)    = TyVar (varTranslate hnat)
+convertType (FP.TyArr ty1 ty2) = TyArr (convertType ty1) (convertType ty2)
+convertType (FP.TyAll ty tyB)  = TyAll (convertType tyB)
 
-pushQueue :: Queue -> Queue -> Queue
-pushQueue EmptyQueue q              = q
-pushQueue (LabelQueue str q) newq   = LabelQueue str (pushQueue q newq)
-pushQueue (TypeQueue ty q) newq     = TypeQueue ty (pushQueue q newq)
-pushQueue (TypeStarQueue ty q) newq = TypeStarQueue ty (pushQueue q newq)
+pushQueue :: FIm.Queue -> FIm.Queue -> FIm.Queue
+pushQueue FIm.EmptyQueue q              = q
+pushQueue (FIm.LabelQueue str q) newq   = FIm.LabelQueue str (pushQueue q newq)
+pushQueue (FIm.TypeQueue ty q) newq     = FIm.TypeQueue ty (pushQueue q newq)
+pushQueue (FIm.TypeStarQueue ty q) newq = FIm.TypeStarQueue ty (pushQueue q newq)
 
-isTypeConstant :: FiType -> Bool
-isTypeConstant TyInt     = True
-isTypeConstant TyBot     = True
-isTypeConstant (TyVar _) = True
-isTypeConstant _         = False
+isTypeConstant :: FP.FiType -> Bool
+isTypeConstant FP.TyInt     = True
+isTypeConstant FP.TyBot     = True
+isTypeConstant (FP.TyVar _) = True
+isTypeConstant _            = False
 
-algoSubtypingCo :: Queue -> FiType -> FiType -> Either String Coercion
-algoSubtypingCo q tyA TyTop = do
+algoSubtypingCo :: FIm.Queue -> FP.FiType -> FP.FiType -> Either String Coercion
+algoSubtypingCo q tyA FP.TyTop = do
   a <- (calcQueueTop q)
   return (CoTrans a (CoTop))
-algoSubtypingCo q tyA (TyAnd ty1 ty2) = do
+algoSubtypingCo q tyA (FP.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 (pushQueue q (TypeQueue ty1 EmptyQueue)) tyA ty2
-algoSubtypingCo EmptyQueue tyA tyB
+algoSubtypingCo q tyA (FP.TyArr ty1 ty2) =
+  algoSubtypingCo (pushQueue q (FIm.TypeQueue ty1 FIm.EmptyQueue)) tyA ty2
+algoSubtypingCo FIm.EmptyQueue tyA tyB
   | tyA == tyB && isTypeConstant tyA = return CoId
-algoSubtypingCo q TyBot c
+algoSubtypingCo q FP.TyBot c
   | isTypeConstant c = return CoBot
-algoSubtypingCo q tyA (TyRecord tyB str) =
-  algoSubtypingCo (pushQueue q (LabelQueue str EmptyQueue)) tyA tyB
-algoSubtypingCo q tyA (TyAll ty1 ty2) =
-  algoSubtypingCo (pushQueue q (TypeStarQueue ty1 EmptyQueue)) tyA ty2
-algoSubtypingCo (TypeQueue ty q) (TyArr ty1 ty2) tyB
+algoSubtypingCo q tyA (FP.TyRecord tyB str) =
+  algoSubtypingCo (pushQueue q (FIm.LabelQueue str FIm.EmptyQueue)) tyA tyB
+algoSubtypingCo q tyA (FP.TyAll ty1 ty2) =
+  algoSubtypingCo (pushQueue q (FIm.TypeStarQueue ty1 FIm.EmptyQueue)) tyA ty2
+algoSubtypingCo (FIm.TypeQueue ty q) (FP.TyArr ty1 ty2) tyB
   | isTypeConstant tyB = do
-    a <- (algoSubtypingCo EmptyQueue ty ty1)
+    a <- (algoSubtypingCo FIm.EmptyQueue ty ty1)
     b <- (algoSubtypingCo q ty2 tyB)
     return (CoArrow a b)
-algoSubtypingCo (LabelQueue str1 q) (TyRecord ty2 str2) tyB
+algoSubtypingCo (FIm.LabelQueue str1 q) (FP.TyRecord ty2 str2) tyB
   | isTypeConstant tyB && str1 == str2 = algoSubtypingCo q ty2 tyB
-algoSubtypingCo q (TyAnd ty1 ty2) tyB
-  | isTypeConstant tyB && algoSubtyping q ty1 tyB = do
+algoSubtypingCo q (FP.TyAnd ty1 ty2) tyB
+  | isTypeConstant tyB && FIm.algoSubtyping q ty1 tyB = do
     a <- (algoSubtypingCo q ty1 tyB)
     return (CoTrans a (CoProj1))
-  | isTypeConstant tyB && algoSubtyping q ty2 tyB = do
+  | isTypeConstant tyB && FIm.algoSubtyping q ty2 tyB = do
     a <- (algoSubtypingCo q ty2 tyB)
     return (CoTrans a (CoProj2))
-algoSubtypingCo (TypeStarQueue ty q) (TyAll ty1 ty2) tyB
+algoSubtypingCo (FIm.TypeStarQueue ty q) (FP.TyAll ty1 ty2) tyB
   | isTypeConstant tyB = do
     a <- (algoSubtypingCo q ty2 tyB)
     return (CoAll a)
 algoSubtypingCo _ _ _ = Left "no subtype"
 
-calcQueueTop :: Queue -> Either String Coercion
-calcQueueTop EmptyQueue = return CoTop
-calcQueueTop (LabelQueue _ q) = do
+calcQueueTop :: FIm.Queue -> Either String Coercion
+calcQueueTop FIm.EmptyQueue = return CoTop
+calcQueueTop (FIm.LabelQueue _ q) = do
   a <- (calcQueueTop q)
   return (CoTrans a CoId)
-calcQueueTop (TypeQueue _ q) = do
+calcQueueTop (FIm.TypeQueue _ q) = do
   a <- (calcQueueTop q)
   return (CoTrans (CoArrow CoTop a) CoTopArrow)
-calcQueueTop (TypeStarQueue _ q) = do
+calcQueueTop (FIm.TypeStarQueue _ q) = do
   a <- (calcQueueTop q)
   return (CoTrans (CoAll a) CoTopAll)
 
-calcQueueAnd :: Queue -> Either String Coercion
-calcQueueAnd EmptyQueue = return CoTop
-calcQueueAnd (LabelQueue _ q) = do
+calcQueueAnd :: FIm.Queue -> Either String Coercion
+calcQueueAnd FIm.EmptyQueue = return CoTop
+calcQueueAnd (FIm.LabelQueue _ q) = do
   a <- (calcQueueAnd q)
   return (CoTrans a CoId)
-calcQueueAnd (TypeQueue _ q) = do
+calcQueueAnd (FIm.TypeQueue _ q) = do
   a <- (calcQueueAnd q)
   return (CoTrans (CoArrow CoId a) CoDistArrow)
-calcQueueAnd (TypeStarQueue _ q) = do
+calcQueueAnd (FIm.TypeStarQueue _ q) = do
   a <- (calcQueueAnd q)
   return (CoTrans (CoAll a) CoDistAll)
 
 goodelaborate term = do
-  ty <- typeOf term Nil
-  elaborate term Nil
+  ty <- FIm.typeOf term FIm.Nil
+  elaborate term FIm.Nil

FCO/FCO.hs

-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))

FCO/FCoBase.hs

+module FCoBase where
+import Data.List 
+
+data Variable = Z | STermVar Variable | STypeVar Variable deriving(Show, Eq)
+
+data Term = TmVar Variable | TmAbs Term Type | TmApp Term Term | TmTApp Term Type | TmTAbs Term | TmTop | TmTuple Term Term | TmInt Int | TmCast Coercion Term deriving(Show, Eq)
+
+data Type = TyVar Variable | TyArr Type Type | TyAll Type | TyInt | TyTop | TyProd Type Type deriving(Show, Eq)
+
+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)
+
+
+plus (Z) h = h
+plus h (Z) = h
+plus x1 (STermVar x2) = (STermVar (plus x1 x2))
+plus x1 (STypeVar x2) = (STypeVar (plus x1 x2))
+
+minus (Z) (Z) = (Z)
+minus (Z) _ = (error "You cannot substract zero with a positive number")
+minus result (Z) = result
+minus (STermVar h1) (STermVar h2) = (minus h1 h2)
+minus (STermVar h1) (STypeVar h2) = (error "differing namespace found in minus")
+minus (STypeVar h1) (STermVar h2) = (error "differing namespace found in minus")
+minus (STypeVar h1) (STypeVar h2) = (minus h1 h2)
+
+generateHnatTermVar 0 c = c
+generateHnatTermVar n c = (STermVar (generateHnatTermVar (n - 1) c))
+
+generateHnatTypeVar 0 c = c
+generateHnatTypeVar n c = (STypeVar (generateHnatTypeVar (n - 1) c))
+
+termshiftHelpplus d c (TmVar var) = if (var >= c) then (TmVar (plus var d)) else (TmVar var)
+
+typeshiftHelpplus d c (TyVar var) = if (var >= c) then (TyVar (plus var d)) else (TyVar var)
+
+termshiftplus d t = (termmap (termshiftHelpplus d) (typeshiftHelpplus d) (Z) t)
+
+typeshiftplus d t = (typemap (typeshiftHelpplus d) (Z) t)
+
+coercionshiftplus d t = (coercionmap (typeshiftHelpplus d) (Z) t)
+
+termshiftHelpminus d c (TmVar var) = if (var >= c) then (TmVar (minus var d)) else (TmVar var)
+
+typeshiftHelpminus d c (TyVar var) = if (var >= c) then (TyVar (minus var d)) else (TyVar var)