Skip to content

GitLab

Commit 79c9cedd authored by Gilles Coremans's avatar Gilles Coremans
Browse files

Merge branch 'master' into genterm

parents 78258ed6 9b7806d7
Hide whitespace changes
Inline Side-by-side
FCO/Elaborate.hs
View file @ 79c9cedd
module Elaborate
( Term(..)
, Type(..)
, Coercion(..)
, elaborate
, goodelaborate
) where
module Elaborate where
import Variables
import FiSorts as Fi
import FCoSorts as Co
import FiImpl
import FCoSorts
import qualified FiSorts as FP
import qualified FiImpl as FIm
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
getTypeFromEnv _ (STermVar h) = Left "wrong FiTerm binding"
getTypeFromEnv (ETypeVar _ rest) (STypeVar h) = getTypeFromEnv rest h
getTypeFromEnv _ (STypeVar h) = Left "No variable FiType"
varTranslate :: FP.Variable -> Variable
varTranslate FP.Z = Z
varTranslate (FP.STermVar var) = STermVar (varTranslate var)
varTranslate (FP.STypeVar var) = STypeVar (varTranslate var)
elaborate :: FiTerm -> Env -> Either String Term
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 (Co.TmAbs term (convertType ty))
elaborate (Fi.TmApp t1 t2) ctx = do
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"
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 (Fi.TyArr ty3 ty4) -> do
a <- (algoSubtypingCo EmptyQueue ty2 ty3)
return (Co.TmApp term1 (Co.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 (Fi.TmMerge t1 t2) ctx = do
elaborate (FP.TmMerge t1 t2) ctx = do
term1 <- elaborate t1 ctx
term2 <- elaborate t2 ctx
return (Co.TmTuple term1 term2)
elaborate (Fi.TmRecord t str) ctx = do
return (TmTuple term1 term2)
elaborate (FP.TmRecord t str) ctx = do
term <- elaborate t ctx
return term
elaborate (Fi.TmProj t str) ctx = do
elaborate (FP.TmProj t str) ctx = do
term <- elaborate t ctx
return term
elaborate (Fi.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)
return (Co.TmCast sub term)
elaborate (TypeApp t ty) ctx = do
sub <- (algoSubtypingCo FIm.EmptyQueue tyt ty)
return (TmCast sub term)
elaborate (FP.TypeApp t ty) ctx = do
term <- elaborate t ctx
return (Co.TmTApp term (convertType ty))
elaborate (Fi.TmAll ty t) ctx = do
term <- elaborate t (ETypeVar ty ctx)
return (Co.TmTAbs 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 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)
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 Fi.TyInt = True
isTypeConstant Fi.TyBot = True
isTypeConstant (Fi.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 Fi.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 (Fi.TyAnd ty1 ty2) = do
return (CoTrans a (CoTopAll))
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 (Fi.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 Fi.TyBot c
| isTypeConstant c = return CoBot
algoSubtypingCo q tyA (Fi.TyRecord tyB str) =
algoSubtypingCo (pushQueue q (LabelQueue str EmptyQueue)) tyA tyB
algoSubtypingCo q tyA (Fi.TyAll ty1 ty2) =
algoSubtypingCo (pushQueue q (TypeStarQueue ty1 EmptyQueue)) tyA ty2
algoSubtypingCo (TypeQueue ty q) (Fi.TyArr ty1 ty2) tyB
algoSubtypingCo q FP.TyBot c
| isTypeConstant c = return $ CoBot (convertType c)
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) (Fi.TyRecord ty2 str2) tyB
algoSubtypingCo (FIm.LabelQueue str1 q) (FP.TyRecord ty2 str2) tyB
| isTypeConstant tyB && str1 == str2 = algoSubtypingCo q ty2 tyB
algoSubtypingCo q (Fi.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
return (CoTrans a (CoProj1 (convertType ty1)))
| isTypeConstant tyB && FIm.algoSubtyping q ty2 tyB = do
a <- (algoSubtypingCo q ty2 tyB)
return (CoTrans a (CoProj2))
algoSubtypingCo (TypeStarQueue ty q) (Fi.TyAll ty1 ty2) tyB
return (CoTrans a (CoProj2 (convertType ty2)))
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 CoTopAll
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
return (CoTrans (CoArrow CoTopAll a) CoTopArrow)
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 CoTopAll
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/FCoBase.hs 0 → 100644
View file @ 79c9cedd
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)
termshiftminus d t = (termmap (termshiftHelpminus d) (typeshiftHelpminus d) (Z) t)
typeshiftminus d t = (typemap (typeshiftHelpminus d) (Z) t)
coercionshiftminus d t = (coercionmap (typeshiftHelpminus d) (Z) t)
termmap onTermVar onTypeVar c (TmVar var) = (onTermVar c (TmVar var))
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 int1) = (TmInt int1)
termmap onTermVar onTypeVar c (TmCast co e) = (TmCast (coercionmap onTypeVar c co) (termmap onTermVar onTypeVar c e))
typemap onTypeVar c (TyVar var) = (onTypeVar c (TyVar var))
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))
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)
termSubstituteHelp sub c (TmVar var) = if (var == c) then (termshiftplus c sub) else (TmVar var)
termTermSubstitute sub orig t = (termmap (termSubstituteHelp sub) (\c x -> x) orig t)
termTypeSubstitute sub orig t = (termmap (\c x -> x) (typeSubstituteHelp sub) orig t)
typeSubstituteHelp sub c (TyVar var) = if (var == c) then (typeshiftplus c sub) else (TyVar var)
typeTypeSubstitute sub orig t = (typemap (typeSubstituteHelp sub) orig t)
coercionTypeSubstitute sub orig t = (coercionmap (typeSubstituteHelp sub) orig t)
freeVariablesTerm c (TmVar var) = if (var >= c) then [(minus var c)] else []
freeVariablesTerm c (TmAbs x t) = (nub (concat [(freeVariablesTerm (STermVar c) x),(freeVariablesType c t)]))
freeVariablesTerm c (TmApp t1 t2) = (nub (concat [(freeVariablesTerm c t1),(freeVariablesTerm c t2)]))
freeVariablesTerm c (TmTApp t1 t) = (nub (concat [(freeVariablesTerm c t1),(freeVariablesType c t)]))
freeVariablesTerm c (TmTAbs t1) = (nub (concat [(freeVariablesTerm (STypeVar c) t1)]))
freeVariablesTerm c (TmTop) = (nub (concat [[]]))
freeVariablesTerm c (TmTuple e1 e2) = (nub (concat [(freeVariablesTerm c e1),(freeVariablesTerm c e2)]))
freeVariablesTerm c (TmInt int1) = (nub (concat [[]]))
freeVariablesTerm c (TmCast co e) = (nub (concat [(freeVariablesCoercion c co),(freeVariablesTerm c e)]))
freeVariablesType c (TyVar var) = if (var >= c) then [(minus var c)] else []
freeVariablesType c (TyArr t1 t2) = (nub (concat [(freeVariablesType c t1),(freeVariablesType c t2)]))
freeVariablesType c (TyAll t1) = (nub (concat [(freeVariablesType (STypeVar c) t1)]))
freeVariablesType c (TyInt) = (nub (concat [[]]))
freeVariablesType c (TyTop) = (nub (concat [[]]))
freeVariablesType c (TyProd t1 t2) = (nub (concat [(freeVariablesType c t1),(freeVariablesType c t2)]))
freeVariablesCoercion c (CoId) = (nub (concat [[]]))
freeVariablesCoercion c (CoTrans co1 co2) = (nub (concat [(freeVariablesCoercion c co1),(freeVariablesCoercion c co2)]))
freeVariablesCoercion c (CoTop ty) = (nub (concat [(freeVariablesType c ty)]))
freeVariablesCoercion c (CoBot ty) = (nub (concat [(freeVariablesType c ty)]))
freeVariablesCoercion c (CoArrow co1 co2) = (nub (concat [(freeVariablesCoercion c co1),(freeVariablesCoercion c co2)]))
freeVariablesCoercion c (CoTuple co1 co2) = (nub (concat [(freeVariablesCoercion c co1),(freeVariablesCoercion c co2)]))
freeVariablesCoercion c (CoProj1 ty2) = (nub (concat [(freeVariablesType c ty2)]))
freeVariablesCoercion c (CoProj2 ty1) = (nub (concat [(freeVariablesType c ty1)]))
freeVariablesCoercion c (CoAll co1) = (nub (concat [(freeVariablesCoercion c co1)]))
freeVariablesCoercion c (CoDistArrow) = (nub (concat [[]]))
freeVariablesCoercion c (CoTopArrow) = (nub (concat [[]]))
freeVariablesCoercion c (CoTopAll) = (nub (concat [[]]))
freeVariablesCoercion c (CoDistAll) = (nub (concat [[]]))
instance Ord Variable where
compare (Z) (Z) = (EQ)
compare (Z) _ = (LT)
compare _ (Z) = (GT)
compare (STermVar h1) (STermVar h2) = (compare h1 h2)
compare (STermVar h1) (STypeVar h2) = (error "differing namespace found in compare")
compare (STypeVar h1) (STermVar h2) = (error "differing namespace found in compare")
compare (STypeVar h1) (STypeVar h2) = (compare h1 h2)
FCO/FCoImpl.hs
View file @ 79c9cedd
module FCoImpl
( Term(..)
, Type(..)
, Coercion(..)
, isVal
, stepEval
, typeOf
, typeOfCo
, typeOfCoReverse
, fullEval
, Variable(..)
, Env(..)
) where
module FCoImpl where
import FCoSorts
import Variables
data Env
= Nil
......
FCO/FCoSorts.hs
View file @ 79c9cedd
......@@ -4,8 +4,6 @@ import Control.Applicative
import Comble
import Test.QuickCheck
import Variables
data Term = TmVar Variable
| TmAbs Term Type
| TmApp Term Term
......@@ -40,6 +38,11 @@ data Coercion = CoId
| CoDistAll
deriving(Show, Eq)
data Variable = Z
| STermVar Variable
| STypeVar Variable
deriving(Show, Eq)
plus (Z) h = h
plus h (Z) = h
plus x1 (STermVar x2) = (STermVar (plus x1 x2))
......
FCO/FiImpl.hs
View file @ 79c9cedd
module FiImpl
( FiTerm(..)
, FiType(..)
, Queue(..)
, typeOf
, Variable(..)
, Env(..)
, fiTermshiftplus
, fiTermshiftminus
, fiTypeshiftminus
, fiTypeshiftplus
, algoSubtyping
, disjointness
) where
module FiImpl where
import FiSorts
import Variables
data Env
= Nil
......
FCO/FiPlusBase.hs 0 → 100644
View file @ 79c9cedd
module FiPlusBase where
import Data.List
data Variable = Z | STermVar Variable | STypeVar Variable deriving(Show, Eq)
data FiTerm = TmVar Variable | TmInt Int | TmTop | TmAbs FiTerm FiType | TmApp FiTerm FiTerm | TmMerge FiTerm FiTerm | TmAnn FiTerm FiType | TmRecord FiTerm String | TmProj FiTerm String | TmAll FiType FiTerm | TypeApp FiTerm FiType deriving(Show, Eq)
data FiType = TyTop | TyBot | TyInt | TyArr FiType FiType | TyAnd FiType FiType | TyRecord FiType String | TyVar Variable | TyAll FiType FiType 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))
fiTermshiftHelpplus d c (TmVar var) = if (var >= c) then (TmVar (plus var d)) else (TmVar var)
fiTypeshiftHelpplus d c (TyVar var) = if (var >= c) then (TyVar (plus var d)) else (TyVar var)
fiTermshiftplus d t = (fiTermmap (fiTermshiftHelpplus d) (fiTypeshiftHelpplus d) (Z) t)
fiTypeshiftplus d t = (fiTypemap (fiTypeshiftHelpplus d) (Z) t)
fiTermshiftHelpminus d c (TmVar var) = if (var >= c) then (TmVar (minus var d)) else (TmVar var)
fiTypeshiftHelpminus d c (TyVar var) = if (var >= c) then (TyVar (minus var d)) else (TyVar var)
fiTermshiftminus d t = (fiTermmap (fiTermshiftHelpminus d) (fiTypeshiftHelpminus d) (Z) t)
fiTypeshiftminus d t = (fiTypemap (fiTypeshiftHelpminus d) (Z) t)
fiTermmap onTermVar onTypeVar c (TmVar var) = (onTermVar c (TmVar var))
fiTermmap onTermVar onTypeVar c (TmInt int1) = (TmInt int1)
fiTermmap onTermVar onTypeVar c (TmTop) = (TmTop)
fiTermmap onTermVar onTypeVar c (TmAbs t ty) = (TmAbs (fiTermmap onTermVar onTypeVar (STermVar c) t) (fiTypemap onTypeVar c ty))
fiTermmap onTermVar onTypeVar c (TmApp t1 t2) = (TmApp (fiTermmap onTermVar onTypeVar c t1) (fiTermmap onTermVar onTypeVar c t2))
fiTermmap onTermVar onTypeVar c (TmMerge t1 t2) = (TmMerge (fiTermmap onTermVar onTypeVar c t1) (fiTermmap onTermVar onTypeVar c t2))
fiTermmap onTermVar onTypeVar c (TmAnn t ty) = (TmAnn (fiTermmap onTermVar onTypeVar c t) (fiTypemap onTypeVar c ty))
fiTermmap onTermVar onTypeVar c (TmRecord t string1) = (TmRecord (fiTermmap onTermVar onTypeVar c t) string1)
fiTermmap onTermVar onTypeVar c (TmProj t string1) = (TmProj (fiTermmap onTermVar onTypeVar c t) string1)
fiTermmap onTermVar onTypeVar c (TmAll ty t) = (TmAll (fiTypemap onTypeVar c ty) (fiTermmap onTermVar onTypeVar (STypeVar c) t))
fiTermmap onTermVar onTypeVar c (TypeApp t ty) = (TypeApp (fiTermmap onTermVar onTypeVar c t) (fiTypemap onTypeVar c ty))
fiTypemap onTypeVar c (TyTop) = (TyTop)
fiTypemap onTypeVar c (TyBot) = (TyBot)
fiTypemap onTypeVar c (TyInt) = (TyInt)
fiTypemap onTypeVar c (TyArr ty1 ty2) = (TyArr (fiTypemap onTypeVar c ty1) (fiTypemap onTypeVar c ty2))
fiTypemap onTypeVar c (TyAnd ty1 ty2) = (TyAnd (fiTypemap onTypeVar c ty1) (fiTypemap onTypeVar c ty2))
fiTypemap onTypeVar c (TyRecord ty string1) = (TyRecord (fiTypemap onTypeVar c ty) string1)
fiTypemap onTypeVar c (TyVar var) = (onTypeVar c (TyVar var))
fiTypemap onTypeVar c (TyAll tyStar ty) = (TyAll (fiTypemap onTypeVar c tyStar) (fiTypemap onTypeVar (STypeVar c) ty))
fiTermSubstituteHelp sub c (TmVar var) = if (var == c) then (fiTermshiftplus c sub) else (TmVar var)
fiTermFiTermSubstitute sub orig t = (fiTermmap (fiTermSubstituteHelp sub) (\c x -> x) orig t)
fiTermFiTypeSubstitute sub orig t = (fiTermmap (\c x -> x) (fiTypeSubstituteHelp sub) orig t)
fiTypeSubstituteHelp sub c (TyVar var) = if (var == c) then (fiTypeshiftplus c sub) else (TyVar var)
fiTypeFiTypeSubstitute sub orig t = (fiTypemap (fiTypeSubstituteHelp sub) orig t)
freeVariablesFiTerm c (TmVar var) = if (var >= c) then [(minus var c)] else []
freeVariablesFiTerm c (TmInt int1) = (nub (concat [[]]))
freeVariablesFiTerm c (TmTop) = (nub (concat [[]]))
freeVariablesFiTerm c (TmAbs t ty) = (nub (concat [(freeVariablesFiTerm (STermVar c) t),(freeVariablesFiType c ty)]))
freeVariablesFiTerm c (TmApp t1 t2) = (nub (concat [(freeVariablesFiTerm c t1),(freeVariablesFiTerm c t2)]))
freeVariablesFiTerm c (TmMerge t1 t2) = (nub (concat [(freeVariablesFiTerm c t1),(freeVariablesFiTerm c t2)]))
freeVariablesFiTerm c (TmAnn t ty) = (nub (concat [(freeVariablesFiTerm c t),(freeVariablesFiType c ty)]))
freeVariablesFiTerm c (TmRecord t string1) = (nub (concat [(freeVariablesFiTerm c t)]))
freeVariablesFiTerm c (TmProj t string1) = (nub (concat [(freeVariablesFiTerm c t)]))
freeVariablesFiTerm c (TmAll ty t) = (nub (concat [(freeVariablesFiType c ty),(freeVariablesFiTerm (STypeVar c) t)]))
freeVariablesFiTerm c (TypeApp t ty) = (nub (concat [(freeVariablesFiTerm c t),(freeVariablesFiType c ty)]))
freeVariablesFiType c (TyTop) = (nub (concat [[]]))
freeVariablesFiType c (TyBot) = (nub (concat [[]]))
freeVariablesFiType c (TyInt) = (nub (concat [[]]))
freeVariablesFiType c (TyArr ty1 ty2) = (nub (concat [(freeVariablesFiType c ty1),(freeVariablesFiType c ty2)]))
freeVariablesFiType c (TyAnd ty1 ty2) = (nub (concat [(freeVariablesFiType c ty1),(freeVariablesFiType c ty2)]))
freeVariablesFiType c (TyRecord ty string1) = (nub (concat [(freeVariablesFiType c ty)]))
freeVariablesFiType c (TyVar var) = if (var >= c) then [(minus var c)] else []
freeVariablesFiType c (TyAll tyStar ty) = (nub (concat [(freeVariablesFiType c tyStar),(freeVariablesFiType (STypeVar c) ty)]))
instance Ord Variable where
compare (Z) (Z) = (EQ)
compare (Z) _ = (LT)
compare _ (Z) = (GT)
compare (STermVar h1) (STermVar h2) = (compare h1 h2)
compare (STermVar h1) (STypeVar h2) = (error "differing namespace found in compare")
compare (STypeVar h1) (STermVar h2) = (error "differing namespace found in compare")
compare (STypeVar h1) (STypeVar h2) = (compare h1 h2)
FCO/FiSorts.hs
View file @ 79c9cedd
......@@ -4,12 +4,16 @@ import Control.Applicative
import Comble
import Test.QuickCheck
import Variables
data FiTerm = TmVar Variable | TmInt Int | TmTop | TmAbs FiTerm FiType | TmApp FiTerm FiTerm | TmMerge FiTerm FiTerm | TmAnn FiTerm FiType | TmRecord FiTerm String | TmProj FiTerm String | TmAll FiType FiTerm | TypeApp FiTerm FiType deriving(Show, Eq)
data FiType = TyTop | TyBot | TyInt | TyArr FiType FiType | TyAnd FiType FiType | TyRecord FiType String | TyVar Variable | TyAll FiType FiType deriving(Show, Eq)
data Variable = Z
| STermVar Variable
| STypeVar Variable
deriving(Show, Eq)
plus (Z) h = h