SystemFImpl.hs 3.21 KB
Newer Older
1
module SystemFImpl  where
2

3
import SystemFBase
Gilles Coremans's avatar
Gilles Coremans committed
4

5
6
7
8
9
10
data Env
  = Nil
  | ETypeVar Env
  | ETermVar Type
             Env
  deriving (Show, Eq)
Gilles Coremans's avatar
Gilles Coremans committed
11

12
13
nth :: Env -> Variable -> Maybe Env
nth env Z = Just env
marton bognar's avatar
marton bognar committed
14
15
nth (ETypeVar env) (STypeVar x) = nth env x
nth (ETermVar _ env) (STermVar x) = nth env x
16
nth _ _ = Nothing
17
18
19
20
21
22

isVal :: Term -> Bool
isVal (TmAbs x t)              = True
isVal (TmTAbs t1)              = True
isVal _ = False

Gilles Coremans's avatar
Gilles Coremans committed
23
getTypeFromEnv :: Env -> Variable -> Either String Type
24
getTypeFromEnv (ETermVar (TyVar i) _) Z = return $ TyVar (STermVar i)
25
26
getTypeFromEnv (ETermVar ty _) Z = return ty
getTypeFromEnv _ Z = Left "wrong or no binding for term"
27
28
29
30
31
32
33
34
35
36
getTypeFromEnv (ETermVar _ rest) (STermVar h) = do
  t <- getTypeFromEnv rest h
  case t of
    (TyVar i) -> return $ TyVar (STermVar i)
    otherwise -> return t
getTypeFromEnv (ETypeVar rest) (STypeVar h) = do
  t <- getTypeFromEnv rest h
  case t of
    (TyVar i) -> return $ TyVar (STypeVar i)
    otherwise -> return t
marton bognar's avatar
marton bognar committed
37
getTypeFromEnv _ (STermVar h) = Left "wrong term binding"
38
getTypeFromEnv _ (STypeVar h) = Left "No variable type"
39

40
41
42
43
44
45
46
47
--evaluation
stepEval :: Term -> Maybe Term
--function application
stepEval (TmApp (TmAbs t ty) t2)
  | isVal t2 =
    Just
      (termshiftminus
         (STermVar Z)
Gilles Coremans's avatar
Gilles Coremans committed
48
         (termTermSubstitute (termshiftplus (STermVar Z) t2) Z t))
49
50
51
52
53
--type application
stepEval (TmTApp (TmTAbs t) ty) =
  Just
    (termshiftminus
       (STypeVar Z)
Gilles Coremans's avatar
Gilles Coremans committed
54
       (termTypeSubstitute (typeshiftplus (STypeVar Z) ty) Z t))
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
--R-CTXT
stepEval (TmApp t1 t2)
  | isVal t1 = do
    newt2 <- stepEval t2
    return (TmApp t1 newt2)
  | otherwise = do
    newt1 <- stepEval t1
    return (TmApp newt1 t2)
stepEval (TmTApp t ty)
  | not (isVal t) = do
    newt <- stepEval t
    return (TmTApp newt ty)
stepEval _ = Nothing

--evaluates a term
fullEval :: Term -> Term
fullEval t = maybe t (fullEval) t2
  where
    t2 = stepEval t

75
wellFormed :: Type -> Env -> Bool
76
wellFormed (TyVar i) env       = case (nth env i) of
77
78
79
80
  Nothing -> False
  Just (ETermVar _ _) -> False
  Just (ETypeVar _) -> True
  Just Nil -> False
81
82
83
wellFormed (TyArr ty1 ty2) env = wellFormed ty1 env && wellFormed ty2 env
wellFormed (TyAll ty) env      = wellFormed ty (ETypeVar env)
wellFormed (TyBase) env        = True
84
85
86

typeOf :: Term -> Env -> Either String Type
typeOf (TmVar nat) ctx = getTypeFromEnv ctx nat
87
88
89
typeOf (TmAbs t ty) ctx =
  if (wellFormed ty ctx) then do
    ty2 <- typeOf t (ETermVar ty ctx)
90
    return $ TyArr ty (typeshiftminus (STermVar Z) ty2)
91
  else Left (show ty ++ " is not well-formed")
92
93
94
95
96
97
98
99
100
101
102
typeOf (TmApp t1 t2) ctx =
  case (typeOf t1 ctx) of
    Right (TyArr ty1 ty2) ->
      case (typeOf t2 ctx) of
        Right ty ->
          if ty == ty1
            then Right ty2
            else Left "different parameter expected"
        Left a -> Left a
    Left a -> Left a
    _ -> Left "arrow type expected"
103
typeOf (TmTApp t ty) ctx =
104
  if (wellFormed ty ctx) then
105
106
107
108
109
110
111
    case (typeOf t ctx) of
      Right (TyAll ty2) -> return
        (typeshiftminus
           (STypeVar Z)
           (typeTypeSubstitute (typeshiftplus (STypeVar Z) ty) Z ty2))
      Left a -> Left a
      Right _ -> Left "not a type abstraction"
112
  else Left (show ty ++ " is not well-formed")
113
114
115
typeOf (TmTAbs t) ctx = do
  ty <- typeOf t (ETypeVar ctx)
  return (TyAll ty)
Gilles Coremans's avatar
Gilles Coremans committed
116