Source

xilocaml / Semantics.hs

Full commit
module Semantics where
import Control.Monad.State
import Data.Maybe
import AbsXilocaml
import ErrM
import TypeEnvironment
import Unification
import PrettyShow
import Common
import Position


-- Checks semantics and returns expression type.
checkSemantics :: Program -> ResultType
checkSemantics p = do
	u <- evalStateT (checkProgram p) startTEnv
	return $ convertUTypeToType u


returnType :: UType -> EnvType UType
returnType = lift . Ok

failurePrefix :: String -> Exp -> String
failurePrefix s x = "Semantic error: " ++ s ++ " in " ++ (prettyShow $ position x) ++ " in " ++ (prettyShow x) ++ "."

failure :: String -> Exp -> EnvType UType
failure s x = lift $ Bad $ failurePrefix s x


-- Checks program for semantic errors and returns its type
-- (with compressed paths - see lookupType function).
checkProgram :: Program -> EnvType UType
checkProgram (Prog _ exp _) = checkExp exp >>= lookupType


checkExp :: Exp -> EnvType UType
checkExp x = case x of
	ELetIn decls exp -> do
		identifiers <- getIdentifiers
		addDecls decls
		t <- checkExp exp
		putIdentifiers identifiers
		return t

	ELetRecIn decls exp -> do
		identifiers <- getIdentifiers
		addRecDecls decls
		t <- checkExp exp
		putIdentifiers identifiers
		return t

	ELambda args exp -> checkFun args exp

	EIfThenElse expCond expTrue expFalse -> do
		c <- checkExp expCond
		t <- checkExp expTrue
		f <- checkExp expFalse
		unify (failurePrefix "expected bool in condition of if statement" x) c UBool
		unify (failurePrefix "expected consistent result types of if statement" x) t f

	EOr expL expR -> do
		l <- checkExp expL
		r <- checkExp expR
		unify (failurePrefix "expected bools in || statement" x) l UBool
		unify (failurePrefix "expected bools in || statement" x) r UBool

	EAnd expL expR -> do
		l <- checkExp expL
		r <- checkExp expR
		unify (failurePrefix "expected bools in && statement" x) l UBool
		unify (failurePrefix "expected bools in && statement" x) r UBool

	ECmp expL _ expR -> do
		l <- checkExp expL
		r <- checkExp expR
		t <- unify (failurePrefix "conflicting types of compared expressions" x) l r
		case t of
			UFun _ _ -> failure "function types are uncomparable" x
			_ -> returnType UBool

	EPrepend expElem expList -> do
		elemType <- checkExp expElem
		listType <- checkExp expList
		unify (failurePrefix "conflicting type of prepended element" x) listType $ UList elemType

	EInfixWeak expL op expR -> do
		l <- checkExp expL
		r <- checkExp expR
		t <- unify (failurePrefix "expected consistent types" x) l r
		if op == OAdd || op == OSub then
			unify (failurePrefix "expected ints" x) t UInt
		else
			unify (failurePrefix "expected floats" x) t UFloat

	EInfixStrong expL op expR -> do
		l <- checkExp expL
		r <- checkExp expR
		t <- unify (failurePrefix "expected consistent types" x) l r
		if op == OMul || op == ODiv || op == OMod then
			unify (failurePrefix "expected ints" x) t UInt
		else
			unify (failurePrefix "expected floats" x) t UFloat

	EUnary op exp -> do
		t <- checkExp exp
		if op == ONeg || op == OPos then
			if isReallyEFloat exp then
				returnType UFloat
			else
				unify (failurePrefix "expected int" x) t UInt
		else
			unify (failurePrefix "expected float" x) t UFloat
		where
			isReallyEFloat :: Exp -> Bool
			isReallyEFloat exp = case exp of
				EUnary _ exp' -> isReallyEFloat exp'
				EFloat _ -> True
				_ -> False

	ENot exp -> do
		t <- checkExp exp
		unify (failurePrefix "expected bool" x) t UBool

	EHead exp -> do
		t <- checkExp exp
		eType <- liftM elemType $ liftM UList nextTerm
		liftM elemType $ unify (failurePrefix "expected list" x) t eType

	ETail exp -> do
		t <- checkExp exp
		lType <- liftM UList nextTerm
		unify (failurePrefix "expected list" x) t lType

	EAppl exp arg -> do
		tExp <- checkExp exp
		tArg <- checkExp arg
		fType <- liftM (UFun tArg) nextTerm
		liftM resType $ unify (failurePrefix "expected function with argument of consistent type" x) tExp fType

	EInt _ -> returnType UInt

	EFloat _ -> returnType UFloat

	EBool _ -> returnType UBool

	EList elems ->
		if elems == [] then
			liftM UList nextTerm
		else do
			let content (ListElement x) = x
			types <- checkExps $ map content elems
			term <- nextTerm
			liftM UList $ foldM (unify $ failurePrefix "expected consistent types in list" x) term types

	EVar (OIdent (_, ident)) -> do
		val <- lookupId ident
		case val of
			Nothing -> failure ("undefined identifier " ++ ident) x
			Just t -> convertPolyToTerm t

	EExplType exp explicitType -> do
		t <- checkExp exp
		explicitType' <- convertTypeToUType explicitType
		unify (failurePrefix "conflicting type of actual and explicitly defined types" x) t explicitType'


checkExps :: [Exp] -> EnvType [UType]
checkExps [] = do
	return []

checkExps (e:es) = do
	t <- checkExp e
	ts <- checkExps es
	return $ t:ts


addDecls :: [LocDecl] -> EnvType ()
addDecls [] = return ()

addDecls (decl:decls) = do
	declType <- case decl of
		LocalVarDecl _ exp ->
			checkExp exp
		LocalVarDeclExplType _ explicitType exp -> do
			t <- checkExp exp
			explicitType' <- convertTypeToUType explicitType
			unify (failurePrefix "conflicting type of actual and explicitly defined types" exp) t explicitType'
		LocalFunDecl _ args exp ->
			checkFun args exp
		LocalFunDeclExplType _ args explicitReturnType exp -> do
			t <- checkFun args exp
			argTerms <- foldM (\acc _ -> liftM (:acc) nextTerm) [] args
			explicitReturnType' <- convertTypeToUType explicitReturnType
			let explicitType' = funType argTerms explicitReturnType'
			unify (failurePrefix "conflicting type of actual and explicitly defined types" exp) t explicitType'
	addDecls decls
	assignId (localDeclIdent decl) declType
	return ()


checkFun :: [Argument] -> Exp -> EnvType UType
checkFun args exp = do
		identifiers <- getIdentifiers
		addArgs args
		t <- checkExp exp
		argTypes <- convertArgsToPolymorphic args
		putIdentifiers identifiers
		resType <- lookupType t
		returnType $ funType argTypes resType
	where
		addArgs :: [Argument] -> EnvType ()
		addArgs [] = return ()

		addArgs (arg:args) = do
			case arg of
				FunArg (OIdent (_, ident)) -> assignNewId ident
				FunArgExplType (OIdent (_, ident)) explicitType -> do
					explicitType' <- convertTypeToUType explicitType
					assignId ident explicitType'
			addArgs args


-- Adds definitions of recursive variables and functions.
-- Only functions may use recursion in their definitions.
-- Difference with ocaml - variables may not have recursive definitions
-- with themselves, so infinite structures are impossible to build.
addRecDecls :: [LocDecl] -> EnvType ()
addRecDecls decls = do
		prepareRecDecls decls
		addRecFunDecls decls
		addRecPolymorphism decls


-- Fully computes type of variables and adds terms (and explicitly
-- defined types) for types of functions.
prepareRecDecls :: [LocDecl] -> EnvType ()
prepareRecDecls [] = return ()

prepareRecDecls (decl:decls) = do
	declType <- case decl of
		LocalVarDecl _ exp ->
			checkExp exp
		LocalVarDeclExplType _ explicitType exp -> do
			t <- checkExp exp
			explicitType' <- convertTypeToUType explicitType
			unify (failurePrefix "conflicting types of actual and explicitly defined types" exp) t explicitType'
		LocalFunDecl _ args exp -> do
			resTerm <- nextTerm
			constructFunType args resTerm
		LocalFunDeclExplType _ args explicitReturnType exp -> do
			explicitReturnType' <- convertTypeToUType explicitReturnType
			constructFunType args explicitReturnType'
	assignId (localDeclIdent decl) declType
	prepareRecDecls decls


-- Computes functions' expressions and unifies their type with known result type.
-- Note: for functions like "let rec f x = f x in f", the return value type will
-- stay unbound forever, but that's not a problem, because it will be never computed,
-- since in case like that all computation paths must end in application of f on it's
-- arguments. Because numeration of UPoly's and UTerm's is the same, there will never
-- be a conflict.
addRecFunDecls :: [LocDecl] -> EnvType ()
addRecFunDecls [] = return ()

addRecFunDecls (decl:decls) = do
		case decl of
			LocalFunDecl (OIdent (_, ident)) args exp ->
				addRecFun ident args exp
			LocalFunDeclExplType (OIdent (_, ident)) args _ exp ->
				addRecFun ident args exp
			_ -> return ()
		addRecFunDecls decls
	where
		addRecFun :: Ident -> [Argument] -> Exp -> EnvType ()
		addRecFun ident args exp = do
			declType <- liftM fromJust $ lookupId ident
			identifiers <- getIdentifiers
			resType <- addRecFunArgs args declType
			t <- checkExp exp
			putIdentifiers identifiers
			unify (failurePrefix "conflicting types of actual and explicitly defined types" exp) resType t
			return ()

-- Changes unbound argument terms into polymorphic type.
addRecPolymorphism :: [LocDecl] -> EnvType ()
addRecPolymorphism [] = return ()

addRecPolymorphism (decl:decls) = do
		case decl of
			LocalFunDecl (OIdent (_, ident)) args _ -> addPolyToFun ident args
			LocalFunDeclExplType (OIdent (_, ident)) args _ _ -> addPolyToFun ident args
			_ -> return ()
		addRecPolymorphism decls
	where
		addPolyToFun :: Ident -> [Argument] -> EnvType ()
		addPolyToFun ident args = do
			declType <- liftM fromJust $ lookupId ident
			identifiers <- getIdentifiers
			addRecFunArgs args declType
			convertArgsToPolymorphic args
			putIdentifiers identifiers


addRecFunArgs :: [Argument] -> UType -> EnvType UType
addRecFunArgs [] t = return t

addRecFunArgs (arg:args) (UFun t1 t2) = do
	case arg of
		FunArg (OIdent (_, ident)) -> assignId ident t1
		FunArgExplType (OIdent (_, ident)) _ -> assignId ident t1
	addRecFunArgs args t2

addRecFunArgs _ _ = error "Internal error: wrong usage of addRecFunArgs"


constructFunType :: [Argument] -> UType -> EnvType UType
constructFunType [] resType = return resType

constructFunType (arg:args) resType = do
	argType <- case arg of
		FunArg _ ->
			nextTerm
		FunArgExplType _ explicitType ->
			convertTypeToUType explicitType
	liftM (UFun argType) $ constructFunType args resType


funType :: [UType] -> UType -> UType
funType [] t = t
funType (argType:argTypes) t = UFun argType (funType argTypes t)


convertArgsToPolymorphic :: [Argument] -> EnvType [UType]
convertArgsToPolymorphic [] = return []

convertArgsToPolymorphic (arg:args) = do
	t <- case arg of
		FunArg (OIdent (_, ident)) ->
			convertIdTypeToPoly ident
		FunArgExplType (OIdent (_, ident)) _ ->
			convertIdTypeToPoly ident
	ts <- convertArgsToPolymorphic args
	return (t:ts)