Skip to content

Comparing changes

Choose two branches to see what’s changed or to start a new pull request. If you need to, you can also compare across forks.

Open a pull request

Create a new pull request by comparing changes across two branches. If you need to, you can also compare across forks.
...
  • 16 commits
  • 17 files changed
  • 0 commit comments
  • 1 contributor
View
1 .gitignore
@@ -5,3 +5,4 @@ cabal-dev
*.chi
*.chs.h
.virthualenv
+.DS_Store
View
2 README.md
@@ -5,6 +5,8 @@ Implementation of OCamlMin language based on min-caml project.
Changelog
=========
+* 1 II 2013
+ * Added type inference
* 31 I 2013
* Syntax of type expressions
* 30 I 2013
View
9 Syntax/Expr.hs
@@ -1,11 +1,4 @@
-module Syntax.Expr (
- FunClause(..),
- pprFunClause,
- Expr(..),
- isAtomicExpr,
- pprAExpr,
- pprExpr
-) where
+module Syntax.Expr where
import Syntax.BinaryPrim
import Syntax.Constant
import Syntax.Pattern
View
6 Syntax/Pattern.hs
@@ -5,7 +5,7 @@ module Syntax.Pattern where
data Pattern =
Pwildcard
- | Pval String
+ | Pvar String
| Pconst Constant
| Ptuple [Pattern]
| Pcons Pattern Pattern
@@ -13,7 +13,7 @@ module Syntax.Pattern where
isAtomicPattern :: Pattern -> Bool
isAtomicPattern Pwildcard = True
- isAtomicPattern (Pval _) = True
+ isAtomicPattern (Pvar _) = True
isAtomicPattern (Pconst _) = True
isAtomicPattern _ = False
@@ -25,7 +25,7 @@ module Syntax.Pattern where
pprPattern :: Pattern -> Iseq
pprPattern Pwildcard =
iStr "_"
- pprPattern (Pval v) =
+ pprPattern (Pvar v) =
iStr v
pprPattern (Pconst c) =
pprConstant c
View
19 TypeInference.hs
@@ -0,0 +1,19 @@
+module TypeInference where
+ import Syntax.Expr
+ import Syntax.Pattern
+ import Syntax.Constant
+ import Types
+
+ import TypeInference.Env
+ import TypeInference.Expr
+ import TypeInference.Constraints
+ import TypeInference.Counter
+
+ import Control.Monad.Error
+ import Control.Monad.State
+
+ typeOfExpression :: Env -> Expr -> Either String Type
+ typeOfExpression env e =
+ case fst $ runState (runErrorT $ typeOfExpr env emptyConstraints e) emptyState of
+ Left s -> Left s
+ Right (a, _) -> Right a
View
28 TypeInference/BinaryPrim.hs
@@ -0,0 +1,28 @@
+{-# LANGUAGE
+ FlexibleContexts
+ #-}
+
+module TypeInference.BinaryPrim where
+ import Syntax.BinaryPrim
+ import Types
+
+ import TypeInference.Counter
+
+ import Control.Monad.State
+
+ typeOfBinaryPrim :: MonadState Counter m => BinaryPrim -> m Type
+ typeOfBinaryPrim BPeq = do
+ v <- freshVar
+ return $ Tfun [v, v] Tbool
+ typeOfBinaryPrim BPlt = return $ Tfun [Tint, Tint] Tbool
+ typeOfBinaryPrim BPgt = return $ Tfun [Tint, Tint] Tbool
+ typeOfBinaryPrim BPor = return $ Tfun [Tbool, Tbool] Tbool
+ typeOfBinaryPrim BPand = return $ Tfun [Tbool, Tbool] Tbool
+ typeOfBinaryPrim BPadd = return $ Tfun [Tint, Tint] Tint
+ typeOfBinaryPrim BPsub = return $ Tfun [Tint, Tint] Tint
+ typeOfBinaryPrim BPmult = return $ Tfun [Tint, Tint] Tint
+ typeOfBinaryPrim BPdiv = return $ Tfun [Tint, Tint] Tint
+ typeOfBinaryPrim BPmod = return $ Tfun [Tint, Tint] Tint
+ typeOfBinaryPrim BPassign = do
+ v <- freshVar
+ return $ Tfun [Tref v, v] Tunit
View
19 TypeInference/Constant.hs
@@ -0,0 +1,19 @@
+{-# LANGUAGE
+ FlexibleContexts
+ #-}
+
+module TypeInference.Constant where
+ import Syntax.Constant
+ import Types
+
+ import TypeInference.Counter
+
+ import Control.Monad.State
+
+ typeOfConstant :: MonadState Counter m => Constant -> m Type
+ typeOfConstant (Cint _) = return Tint
+ typeOfConstant (Cbool _) = return Tbool
+ typeOfConstant Cnil = do
+ v <- freshVar
+ return $ Tlist v
+ typeOfConstant Cunit = return Tunit
View
13 TypeInference/Constraints.hs
@@ -0,0 +1,13 @@
+module TypeInference.Constraints where
+ import Types
+
+ type Constraints = [(Type, Type)]
+
+ emptyConstraints :: Constraints
+ emptyConstraints = []
+
+ singleConstraint :: Type -> Type -> Constraints
+ singleConstraint t1 t2 = [(t1, t2)]
+
+ addConstraints :: Constraints -> Constraints -> Constraints
+ addConstraints = (++)
View
19 TypeInference/Counter.hs
@@ -0,0 +1,19 @@
+{-# LANGUAGE
+ FlexibleContexts
+ #-}
+
+module TypeInference.Counter where
+ import Types
+
+ import Control.Monad.State
+
+ type Counter = Integer
+
+ emptyState :: Counter
+ emptyState = 0
+
+ freshVar :: MonadState Counter m => m Type
+ freshVar = do
+ n <- get
+ put $ n + 1
+ return $ Tvar $ 'a' : show n
View
23 TypeInference/Env.hs
@@ -0,0 +1,23 @@
+{-# LANGUAGE
+ FlexibleContexts
+ #-}
+
+module TypeInference.Env (Env, emptyEnv, get, extend) where
+ import Types
+ import Utils.Errors
+
+ import Control.Monad.Error
+
+ type Env = [(String, Type)]
+
+ emptyEnv :: Env
+ emptyEnv = []
+
+ get :: MonadError String m => String -> Env -> m Type
+ get v env =
+ case v `lookup` env of
+ Nothing -> throwError $ unboundVariable v
+ Just tp -> return tp
+
+ extend :: Env -> (String, Type) -> Env
+ extend = flip (:)
View
100 TypeInference/Expr.hs
@@ -0,0 +1,100 @@
+{-# LANGUAGE
+ FlexibleContexts
+ #-}
+
+module TypeInference.Expr (typeOfExpr) where
+ import Syntax.Expr
+ import Types
+
+ import TypeInference.BinaryPrim
+ import TypeInference.Constant
+ import TypeInference.Constraints
+ import TypeInference.Counter
+ import TypeInference.Env
+ import TypeInference.Pattern
+ import TypeInference.UnaryPrim
+ import TypeInference.Unification
+
+ import Control.Monad.Error
+ import Control.Monad.State hiding (get)
+
+ typeOfFunClause :: (MonadState Counter m, MonadError String m) =>
+ Env -> Constraints -> FunClause -> m (Type, Subst)
+ typeOfFunClause env cns fc = do
+ tbcns <- mapM typeAndBindingsOfPattern $ arguments fc
+ let (tas, bas, cas) = unzip3 tbcns
+ (t, s) <- typeOfExpr (concat bas ++ env) (concat cas ++ cns) $ body fc
+ s' <- unify (concat cas ++ cns)
+ return (Tfun tas t `applySubst` s `applySubst` s', s ++ s')
+
+ typeOfFunction :: (MonadState Counter m, MonadError String m) =>
+ Env -> Constraints -> [FunClause] -> m (Type, Subst)
+ typeOfFunction env cns fcs = do
+ tfcs <- mapM (typeOfFunClause env cns) fcs
+ let (t:tps, ss) = unzip tfcs
+ s <- unify $ cns ++ map ((,) t) tps
+ let subst = foldl (++) s ss
+ return (t `applySubst` subst, subst)
+
+
+ typeOfExpr :: (MonadState Counter m, MonadError String m) =>
+ Env -> Constraints -> Expr -> m (Type, Subst)
+ typeOfExpr _ cns (Econst c) = do
+ t <- typeOfConstant c
+ s <- unify cns
+ return (t `applySubst` s, s)
+ typeOfExpr _ cns (Euprim up) = do
+ t <- typeOfUnaryPrim up
+ s <- unify cns
+ return (t `applySubst` s, s)
+ typeOfExpr _ cns (Ebprim bp) = do
+ t <- typeOfBinaryPrim bp
+ s <- unify cns
+ return (t `applySubst` s, s)
+ typeOfExpr env cns (Evar n) = do
+ t <- n `get` env
+ s <- unify cns
+ return (t `applySubst` s, s)
+ typeOfExpr env cns (Efun fcs) =
+ typeOfFunction env cns fcs
+ typeOfExpr env cns (Elet p e1 e2) = do
+ (tp, bs, cs) <- typeAndBindingsOfPattern p
+ (t1, s1) <- typeOfExpr env cns e1
+ let cns' = singleConstraint t1 tp `addConstraints` cs `addConstraints` cns
+ let env' = map (\(n, t) -> (n, t `applySubst` s1)) bs ++ env
+ typeOfExpr env' cns' e2
+ typeOfExpr env cns (Eletrec n fcs e2) = do
+ v <- freshVar
+ (t1, s1) <- typeOfFunction (env `extend` (n, v)) cns fcs
+ let cns' = singleConstraint v t1 `addConstraints` cns
+ s <- unify cns'
+ typeOfExpr (env `extend` (n, t1 `applySubst` s1 `applySubst` s)) cns' e2
+ typeOfExpr env cns (Eapply e1 as) = do
+ (t1, s1) <- typeOfExpr env cns e1
+ tas <- mapM (typeOfExpr env cns) as
+ let (ts, _) = unzip tas
+ v <- freshVar
+ s <- unify $ singleConstraint t1 (Tfun ts v) `addConstraints` cns
+ return (v `applySubst` s `applySubst` s1, s)
+ typeOfExpr env cns (Etuple es) = do
+ tas <- mapM (typeOfExpr env cns) es
+ s <- unify cns
+ return (Ttuple (map fst tas) `applySubst` s, s)
+ typeOfExpr env cns (Econs e1 e2) = do
+ (t1, s1) <- typeOfExpr env cns e1
+ (t2, s2) <- typeOfExpr env cns e2
+ s <- unify $ singleConstraint t2 (Tlist t1) `addConstraints` cns
+ return (t2 `applySubst` s `applySubst` s1 `applySubst` s2, s ++ s1 ++ s2)
+ typeOfExpr env cns (Eif e1 e2 e3) = do
+ (t1, _) <- typeOfExpr env cns e1
+ (t2, s2) <- typeOfExpr env cns e2
+ (t3, s3) <- typeOfExpr env cns e3
+ s <- unify $ singleConstraint t2 t3 `addConstraints`
+ singleConstraint t1 Tbool `addConstraints`
+ cns
+ return (t2 `applySubst` s `applySubst` s2 `applySubst` s3, s ++ s2 ++ s3)
+ typeOfExpr env cns (Eseq e1 e2) = do
+ (t1, _) <- typeOfExpr env cns e1
+ (t2, s2) <- typeOfExpr env cns e2
+ s <- unify $ singleConstraint t1 Tunit `addConstraints` cns
+ return (t2 `applySubst` s, s ++ s2)
View
62 TypeInference/Pattern.hs
@@ -0,0 +1,62 @@
+{-# LANGUAGE
+ FlexibleContexts
+ #-}
+
+module TypeInference.Pattern (typeAndBindingsOfPattern) where
+ import Syntax.Pattern
+ import Types
+ import Utils.Errors
+
+ import TypeInference.Constant
+ import TypeInference.Constraints
+ import TypeInference.Counter
+ import TypeInference.Env
+
+ import Control.Monad.Error
+ import Control.Monad.State
+
+ idsDistinct :: [String] -> Bool
+ idsDistinct [] = True
+ idsDistinct (x:xs) = idsDistinct' x xs xs where
+ idsDistinct' _ [] [] = True
+ idsDistinct' _ [] (y:ys) = idsDistinct' y ys ys
+ idsDistinct' x' (z:zs) ys
+ | x' /= z = idsDistinct' x' zs ys
+ | otherwise = False
+
+ getids :: Pattern -> [String]
+ getids Pwildcard = []
+ getids (Pvar n) = [n]
+ getids (Pconst _) = []
+ getids (Ptuple ps) = concatMap getids ps
+ getids (Pcons p1 p2) = getids p1 ++ getids p2
+
+ typeAndBindingsOfPattern :: (MonadError String m, MonadState Counter m) =>
+ Pattern -> m (Type, Env, Constraints)
+ typeAndBindingsOfPattern p
+ | idsDistinct $ getids p = typeAndBindingsOfPattern' p
+ | otherwise = throwError $ overlappingIds p
+ where
+ typeAndBindingsOfPattern' :: (MonadError String m,
+ MonadState Counter m) =>
+ Pattern -> m (Type, Env, Constraints)
+ typeAndBindingsOfPattern' Pwildcard = do
+ v <- freshVar
+ return (v, emptyEnv, emptyConstraints)
+ typeAndBindingsOfPattern' (Pvar n) = do
+ v <- freshVar
+ return (v, emptyEnv `extend` (n, v), emptyConstraints)
+ typeAndBindingsOfPattern' (Pconst c) = do
+ t <- typeOfConstant c
+ return (t, emptyEnv, emptyConstraints)
+ typeAndBindingsOfPattern' (Ptuple ps) = do
+ tbcs <- mapM typeAndBindingsOfPattern ps
+ return (Ttuple $ map (\(a, _, _) -> a) tbcs,
+ concatMap (\(_, b, _) -> b) tbcs,
+ concatMap (\(_, _, c) -> c) tbcs)
+ typeAndBindingsOfPattern' (Pcons p1 p2) = do
+ (t1, b1, c1) <- typeAndBindingsOfPattern p1
+ (t2, b2, c2) <- typeAndBindingsOfPattern p2
+ return (t2, b1 ++ b2,
+ singleConstraint t2 (Tlist t1) `addConstraints`
+ c1 `addConstraints` c2 )
View
21 TypeInference/UnaryPrim.hs
@@ -0,0 +1,21 @@
+{-# LANGUAGE
+ FlexibleContexts
+ #-}
+
+module TypeInference.UnaryPrim where
+ import Syntax.UnaryPrim
+ import Types
+
+ import TypeInference.Counter
+
+ import Control.Monad.State
+
+ typeOfUnaryPrim :: MonadState Counter m => UnaryPrim -> m Type
+ typeOfUnaryPrim UPnot = return $ Tfun [Tbool] Tbool
+ typeOfUnaryPrim UPref = do
+ v <- freshVar
+ return $ Tfun [v] $ Tref v
+ typeOfUnaryPrim UPderef = do
+ v <- freshVar
+ return $ Tfun [Tref v] v
+ typeOfUnaryPrim UPminus = return $ Tfun [Tint] Tint
View
48 TypeInference/Unification.hs
@@ -0,0 +1,48 @@
+{-# LANGUAGE
+ FlexibleContexts
+ #-}
+
+module TypeInference.Unification (unify) where
+ import Types
+ import Utils.Errors
+
+ import TypeInference.Constraints
+
+ import Control.Exception.Base
+ import Control.Monad.Error
+
+ canUnify :: Type -> Type -> Bool
+ canUnify (Tvar _) _ = True
+ canUnify _ (Tvar _) = True
+ canUnify (Tlist t1) (Tlist t2) = canUnify t1 t2
+ canUnify (Tref t1) (Tref t2) = canUnify t1 t2
+ canUnify (Ttuple ts1) (Ttuple ts2) =
+ length ts1 == length ts2 &&
+ and (zipWith canUnify ts1 ts2)
+ canUnify (Tfun as1 t1) (Tfun as2 t2) =
+ length as1 == length as2 &&
+ and (zipWith canUnify as1 as2) &&
+ canUnify t1 t2
+ canUnify t1 t2 = t1 == t2
+
+ newConstraints :: Type -> Type -> Constraints
+ newConstraints (Tlist t1) (Tlist t2) = [(t1, t2)]
+ newConstraints (Tref t1) (Tref t2) = [(t1, t2)]
+ newConstraints (Ttuple ts1) (Ttuple ts2) = zip ts1 ts2
+ newConstraints (Tfun as1 t1) (Tfun as2 t2) = (t1, t2) : zip as1 as2
+ newConstraints t1 t2 = assert (t1 == t2) []
+
+ unify :: MonadError String m => Constraints -> m Subst
+ unify cns = unify' cns emptySubst where
+ unify' :: MonadError String m => Constraints -> Subst -> m Subst
+ unify' [] s = return s
+ unify' ((a, b):cs) s = do
+ let a' = a `applySubst` s
+ let b' = b `applySubst` s
+ case (a', b') of
+ (Tvar i, _) -> unify' cs $ composeSubst (singleSubst i b') s
+ (_, Tvar i) -> unify' cs $ composeSubst (singleSubst i a') s
+ (_, _) ->
+ if canUnify a' b'
+ then unify' (newConstraints a' b' `addConstraints` cs) s
+ else throwError $ cannotUnify a' b'
View
8 Types.hs
@@ -1,4 +1,10 @@
module Types (
- Type(..)
+ Type(..),
+ Subst,
+ emptySubst,
+ composeSubst,
+ singleSubst,
+ applySubst
) where
import Types.Base
+ import Types.Subst
View
33 Types/Subst.hs
@@ -0,0 +1,33 @@
+module Types.Subst (
+ Subst,
+ emptySubst,
+ composeSubst,
+ singleSubst,
+ applySubst
+) where
+ import Types.Base
+
+ type Subst = [(String, Type)]
+
+ emptySubst :: Subst
+ emptySubst = []
+
+ composeSubst :: Subst -> Subst -> Subst
+ composeSubst = flip (++)
+
+ singleSubst :: String -> Type -> Subst
+ singleSubst i t = [(i, t)]
+
+ applySubst :: Type -> Subst -> Type
+ applySubst = foldl $ flip applySingleSubst
+
+ applySingleSubst :: (String, Type) -> Type -> Type
+ applySingleSubst (sb, tb) (Tvar v)
+ | sb == v = tb
+ | otherwise = Tvar v
+ applySingleSubst sb (Tlist tp) = Tlist $ applySingleSubst sb tp
+ applySingleSubst sb (Tref tp) = Tref $ applySingleSubst sb tp
+ applySingleSubst sb (Ttuple ts) = Ttuple $ map (applySingleSubst sb) ts
+ applySingleSubst sb (Tfun as tp) =
+ Tfun (map (applySingleSubst sb) as) $ applySingleSubst sb tp
+ applySingleSubst _ tp = tp
View
14 Utils/Errors.hs
@@ -0,0 +1,14 @@
+module Utils.Errors (
+ unboundVariable,
+ overlappingIds,
+ cannotUnify
+) where
+
+ unboundVariable :: String -> String
+ unboundVariable v = "Unbound variable " ++ v
+
+ overlappingIds :: Show a => a -> String
+ overlappingIds p = "Overlapping identifires in: " ++ show p
+
+ cannotUnify :: Show a => a -> a -> String
+ cannotUnify t1 t2 = "Cannot unify " ++ show t1 ++ " with " ++ show t2

No commit comments for this range

Something went wrong with that request. Please try again.