Commit 55dd621b authored by marton bognar's avatar marton bognar
Browse files

Reintroduce variable types

parent b583e600
module SystemFBase where
import Data.List
data Variable = Z | S Variable deriving(Show, Eq)
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 deriving(Show, Eq)
......@@ -10,18 +10,21 @@ data Type = TyVar Variable | TyArr Type Type | TyAll Type | TyBase deriving(Show
plus (Z) h = h
plus h (Z) = h
plus x1 (S x2) = (S (plus x1 x2))
plus x1 (STypeVar x2) = (STypeVar (plus x1 x2))
plus x1 (STermVar x2) = (STermVar (plus x1 x2))
minus (Z) (Z) = (Z)
minus (Z) _ = (error "You cannot substract zero with a positive number")
minus result (Z) = result
minus (S h1) (S h2) = (minus h1 h2)
minus (STypeVar h1) (STypeVar h2) = (minus h1 h2)
minus (STermVar h1) (STermVar h2) = (minus h1 h2)
minus _ _ = (error "differing namespace found in minus")
generateHnatTermVar 0 c = c
generateHnatTermVar n c = (S (generateHnatTermVar (n - 1) c))
generateHnatTermVar n c = (STermVar (generateHnatTermVar (n - 1) c))
generateHnatTypeVar 0 c = c
generateHnatTypeVar n c = (S (generateHnatTypeVar (n - 1) 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)
......@@ -40,14 +43,14 @@ termshiftminus d t = (termmap (termshiftHelpminus d) (typeshiftHelpminus d) (Z)
typeshiftminus d t = (typemap (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 (S c) x) (typemap onTypeVar c t))
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 (S c) t1))
termmap onTermVar onTypeVar c (TmTAbs t1) = (TmTAbs (termmap onTermVar onTypeVar (STypeVar c) t1))
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 (S c) t1))
typemap onTypeVar c (TyAll t1) = (TyAll (typemap onTypeVar (STypeVar c) t1))
typemap onTypeVar c (TyBase) = (TyBase)
termSubstituteHelp sub c (TmVar var) = if (var == c) then (termshiftplus c sub) else (TmVar var)
......@@ -61,17 +64,18 @@ typeSubstituteHelp sub c (TyVar var) = if (var == c) then (typeshiftplus c sub)
typeTypeSubstitute sub orig t = (typemap (typeSubstituteHelp sub) orig t)
freeVariablesTerm c (TmVar var) = if (var >= c) then [(minus var c)] else []
freeVariablesTerm c (TmAbs x t) = (nub (concat [(freeVariablesTerm (S c) x),(freeVariablesType c t)]))
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 (S c) t1)]))
freeVariablesTerm c (TmTAbs t1) = (nub (concat [(freeVariablesTerm (STypeVar c) t1)]))
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 (S c) t1)]))
freeVariablesType c (TyAll t1) = (nub (concat [(freeVariablesType (STypeVar c) t1)]))
freeVariablesType c (TyBase) = (nub (concat [[]]))
instance Ord Variable where
compare (Z) (Z) = (EQ)
compare (Z) _ = (LT)
compare _ (Z) = (GT)
compare (S h1) (S h2) = (compare h1 h2)
compare (STermVar h1) (STermVar h2) = (compare h1 h2)
compare (STypeVar h1) (STypeVar h2) = (compare h1 h2)
......@@ -9,8 +9,8 @@ data Env
nth :: Env -> Variable -> Maybe Env
nth env Z = Just env
nth (ETypeVar env) (S x) = nth env x
nth (ETermVar _ env) (S x) = nth env x
nth (ETypeVar env) (STypeVar x) = nth env x
nth (ETermVar _ env) (STermVar x) = nth env x
nth _ _ = Nothing
isVal :: Term -> Bool
......@@ -21,9 +21,10 @@ isVal _ = False
getTypeFromEnv :: Env -> Variable -> Either String Type
getTypeFromEnv (ETermVar ty _) Z = return ty
getTypeFromEnv _ Z = Left "wrong or no binding for term"
getTypeFromEnv (ETermVar _ rest) (S h) = getTypeFromEnv rest h
getTypeFromEnv (ETypeVar rest) (S h) = getTypeFromEnv rest h
getTypeFromEnv _ (S h) = Left "No variable type"
getTypeFromEnv (ETermVar _ rest) (STermVar h) = getTypeFromEnv rest h
getTypeFromEnv (ETypeVar rest) (STypeVar h) = getTypeFromEnv rest h
getTypeFromEnv _ (STermVar h) = Left "wrong term binding"
getTypeFromEnv _ (STypeVar h) = Left "No variable type"
--evaluation
stepEval :: Term -> Maybe Term
......@@ -32,14 +33,14 @@ stepEval (TmApp (TmAbs t ty) t2)
| isVal t2 =
Just
(termshiftminus
(S Z)
(termTermSubstitute (termshiftplus (S Z) t2) Z t))
(STermVar Z)
(termTermSubstitute (termshiftplus (STermVar Z) t2) Z t))
--type application
stepEval (TmTApp (TmTAbs t) ty) =
Just
(termshiftminus
(S Z)
(termTypeSubstitute (typeshiftplus (S Z) ty) Z t))
(STypeVar Z)
(termTypeSubstitute (typeshiftplus (STypeVar Z) ty) Z t))
--R-CTXT
stepEval (TmApp t1 t2)
| isVal t1 = do
......@@ -92,8 +93,8 @@ typeOf (TmTApp (TmTAbs t) ty) ctx =
if (wellFormed ty ctx) then
typeOf
(termshiftminus
(S Z)
(termTypeSubstitute (typeshiftplus (S Z) ty) Z t)) ctx
(STypeVar Z)
(termTypeSubstitute (typeshiftplus (STypeVar Z) ty) Z t)) ctx
else Left (show ty ++ " is not well-formed")
typeOf (TmTAbs t) ctx = do
ty <- typeOf t (ETypeVar ctx)
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment