Commits

Xilexio committed 6d0b930

Initial commit with first version

Comments (0)

Files changed (20)

+module Common where
+import Control.Monad.State
+import qualified Data.Map as Map
+import AbsXilocaml
+
+
+localDeclIdent :: LocDecl -> OIdent
+localDeclIdent (LocalVarDecl ident _) = ident
+localDeclIdent (LocalVarDeclExplType ident _ _) = ident
+localDeclIdent (LocalFunDecl ident _ _) = ident
+localDeclIdent (LocalFunDeclExplType ident _ _ _) = ident
+
+
+identName :: OIdent -> String
+identName (OIdent name) = name
+
+
+comparator :: (Eq a, Ord a) => OCmp -> a -> a -> Bool
+comparator op = case op of
+	OEq -> (==)
+	ONeq -> (/=)
+	OLt -> (<)
+	OLeq -> (<=)
+	OGt -> (>)
+	OGeq -> (>=)
+
+
+startMapEnv :: Ord k => Map.Map k v
+startMapEnv = Map.empty
+
+assignVar :: Ord k => k -> v -> State (Map.Map k v) v
+assignVar k v = do
+	s <- get
+	put $ Map.insert k v s
+	return v
+
+lookupVar :: Ord k => k -> State (Map.Map k v) (Maybe v)
+lookupVar k = do
+	s <- get
+	return $ Map.lookup k s	
+module Interpreter where
+import Control.Monad.State
+import Data.List(findIndex)
+import AbsXilocaml
+import ErrM
+import RunEnvironment
+import PrettyShow
+import Common
+
+
+-- Interprets program and returns result of computation.
+interpret :: Program -> Result
+interpret p = evalStateT (transProgram p) startREnv
+
+
+returnValue :: Value -> EnvRun Value
+returnValue = lift . Ok
+
+runtimeError :: PrettyShowable a => String -> a -> EnvRun Value
+runtimeError s x = lift $ Bad $ "Runtime error: " ++ s ++ " in " ++ (prettyShow x) ++ "."
+
+
+transProgram :: Program -> EnvRun Value
+transProgram (Prog _ exp _) = transExp exp
+
+
+transExp :: Exp -> EnvRun Value
+transExp x = case x of
+	ELetIn decls exp -> do
+		s0 <- get
+		transDecls decls
+		v <- transExp exp
+		put s0
+		return v
+
+	ELetRecIn decls exp -> do
+		s0 <- get
+		-- Here we add basic environment
+		transDecls decls
+		-- Here we loop environment for all functional variables
+		loopEnvironment $ map localDeclIdent $ filter isFunDecl decls
+		v <- transExp exp
+		put s0
+		return v
+
+	ELambda args exp -> transFun args exp
+
+	EIfThenElse expCond expTrue expFalse -> do
+		c <- transExp expCond
+		if bval c then
+			transExp expTrue
+		else
+			transExp expFalse
+
+	EOr expL expR -> do
+		lv <- transExp expL
+		if not $ bval lv then
+			transExp expR
+		else
+			returnValue lv
+
+	EAnd expL expR -> do
+		lv <- transExp expL
+		if bval lv then
+			transExp expR
+		else
+			returnValue lv
+
+	ECmp expL op expR -> do
+		l <- transExp expL
+		r <- transExp expR
+		case l of
+			VFun _ _ _ -> runtimeError "Comparison of functional values" x
+			_ -> returnValue $ VBool $ comparator op l r
+
+	EPrepend expElem expList -> do
+		elemValue <- transExp expElem
+		listValue <- transExp expList
+		returnValue $ VList $ elemValue:(lelems listValue)
+
+	EInfixWeak expL op expR -> do
+		l <- transExp expL
+		r <- transExp expR
+		returnValue $ case op of
+			OAdd -> VInt $ ival l + ival r
+			OSub -> VInt $ ival l - ival r
+			OAddFlt -> VFloat $ fval l + fval r
+			OSubFlt -> VFloat $ fval l - fval r
+
+	EInfixStrong expL op expR -> do
+		l <- transExp expL
+		r <- transExp expR
+		case op of
+			OMul -> returnValue $ VInt $ ival l * ival r
+			ODiv ->
+				if ival r == 0 then
+					runtimeError "Division by zero" x
+				else
+					returnValue $ VInt $ ival l `div` ival r
+			OMulFlt -> returnValue $ VFloat $ fval l * fval r
+			ODivFlt -> returnValue $ VFloat $ fval l / fval r
+			OMod ->
+				if ival r == 0 then
+					runtimeError "Division by zero" x
+				else
+					returnValue $ VInt $ ival l `mod` ival r
+
+	EUnary op exp -> do
+		v <- transExp exp
+		case op of
+			ONeg -> case v of
+				VInt i -> returnValue $ VInt (-i)
+				VFloat f -> returnValue $ VFloat (-f)
+				_ -> error "Internal error: semantic error passed through semantics checker."
+			OPos -> returnValue v
+			ONegFlt -> returnValue $ VFloat $ -fval v
+			OPosFlt -> returnValue v
+
+	ENot exp -> do
+		v <- transExp exp
+		returnValue $ VBool $ not $ bval v
+
+	EHead exp -> do
+		v <- transExp exp
+		case lelems v of
+			[] -> runtimeError "Taking head of empty list" x
+			_ -> returnValue $ head $ lelems v
+
+	ETail exp -> do
+		v <- transExp exp
+		case lelems v of
+			[] -> runtimeError "Taking tail of empty list" x
+			_ -> returnValue $ VList $ tail $ lelems v
+
+	EAppl exp arg -> do
+		expVal <- transExp exp
+		argVal <- transExp arg
+		apply expVal argVal
+
+	EInt n -> returnValue $ VInt n
+
+	EFloat str -> returnValue $ VFloat $ transOFloat str
+
+	ETrue -> returnValue $ VBool True
+
+	EFalse -> returnValue $ VBool False
+
+	EList elems -> do
+		let content (ListElement x) = x
+		values <- transExps $ map content elems
+		returnValue $ VList values
+
+	EVar ident -> lookupEnv ident
+
+	EExplType exp _ -> transExp exp
+
+
+isFunDecl :: LocDecl -> Bool
+isFunDecl decl = case decl of
+	LocalVarDecl _ _ -> False
+	LocalVarDeclExplType _ _ _ -> False
+	_ -> True
+
+
+transExps :: [Exp] -> EnvRun [Value]
+transExps [] = do
+	return []
+
+transExps (exp:exps) = do
+	v <- transExp exp
+	vs <- transExps exps
+	return $ v:vs
+
+
+transOFloat :: OFloat -> Double
+transOFloat (OFloat str) = let
+	exponentDelimiter = findIndex (\x -> x == 'e' || x == 'E') str
+	(fractionStr, exponentStr) = case exponentDelimiter of
+		Nothing -> (str, "")
+		Just delim -> (\(x,y) -> (x, tail y)) $ splitAt delim str
+	fraction =
+		if head fractionStr == '.' then
+			(read $ '0':fractionStr)::Double
+		else if head (reverse fractionStr) == '.' then
+			(read $ fractionStr ++ "0")::Double
+		else
+			(read fractionStr)::Double
+	exponent =
+		if exponentStr == "" then
+			0.0
+		else if head exponentStr == '+' then
+			(read $ tail exponentStr)::Double
+		else
+			(read $ exponentStr)::Double
+	in fraction * (10 ** exponent)
+
+
+transFun :: [Argument] -> Exp -> EnvRun Value
+transFun args exp = do
+	env <- get
+	let argIdents = map argIdent args
+	returnValue $ VFun env argIdents exp
+
+
+argIdent :: Argument -> OIdent
+argIdent (FunArg ident) = ident
+argIdent (FunArgExplType ident _) = ident
+
+
+apply :: Value -> Value -> EnvRun Value
+apply (VFun fenv (farg:fargs) fexp) arg = do
+	s0 <- get
+	put fenv
+	assignEnv farg arg
+	v <- if fargs == [] then
+			transExp fexp
+		else do
+			env <- get
+			returnValue $ VFun env fargs fexp
+	put s0
+	returnValue v
+
+apply _ _ = error "Internal error: wrong usage of apply function."
+
+
+transDecls :: [LocDecl] -> EnvRun ()
+transDecls [] = return ()
+
+transDecls (decl:decls) = do
+	v <- case decl of
+		LocalVarDecl _ exp -> transExp exp
+		LocalVarDeclExplType _ _ exp -> transExp exp
+		LocalFunDecl _ args exp -> transFun args exp
+		LocalFunDeclExplType _ args _ exp -> transFun args exp
+	transDecls decls
+	assignEnv (localDeclIdent decl) v
+module Main where
+import ParXilocaml
+import ErrM
+import Semantics
+import Interpreter
+import PrettyShow
+
+
+main :: IO ()
+main = do
+	interact printResult
+	putStrLn ""
+
+
+printResult :: String -> String
+printResult s =
+	let result = do
+		tree <- pProgram $ myLexer s
+		valueType <- checkSemantics tree
+		value <- interpret tree
+		return (normalize valueType, value)
+	in case result of
+		Ok (valueType, value) -> (prettyShow value) ++ " : " ++ (prettyShow valueType)
+		Bad s -> error s
+PROGRAM=Xilocaml
+
+all: interpreter documentation
+interpreter: $(PROGRAM)
+documentation: doc/$(PROGRAM).pdf
+
+$(PROGRAM): Grammar/AbsXilocaml.hs
+	ghc --make -iGrammar -o $(PROGRAM) Main.hs
+
+doc/$(PROGRAM).pdf: doc/$(PROGRAM).tex
+	pdflatex -output-directory=doc -interaction=batchmode doc/$(PROGRAM)
+
+TestXilocaml Grammar/AbsXilocaml.hs: generate_grammar Xilocaml.cf
+	./generate_grammar
+
+test: Grammar/AbsXilocaml.hs
+	runhaskell -iGrammar -w UnitTests.hs
+
+edit:
+	ghci -iGrammar
+
+clean:
+	rm -f *.o *.hi $(PROGRAM) Grammar/*.o Grammar/*.hi Grammar/TestXilocaml Grammar/*.log Grammar/*.aux Grammar/*.dvi Grammar/*.ps doc/$(PROGRAM).aux doc/$(PROGRAM).log doc/$(PROGRAM).toc doc/$(PROGRAM).out doc/$(PROGRAM).pdf
+
+distclean:
+	rm -f *.o *.hi $(PROGRAM) Grammar/* doc/$(PROGRAM).aux doc/$(PROGRAM).log doc/$(PROGRAM).toc doc/$(PROGRAM).out doc/$(PROGRAM).pdf
+
+.PHONY: clean distclean Xilocaml TestXilocaml edit
+module PrettyShow where
+import Control.Monad.State
+import Data.Char
+import qualified Data.Map as Map
+import TypeEnvironment
+import RunEnvironment
+import AbsXilocaml
+import PrintXilocaml
+import Common
+
+
+class PrettyShowable t where
+	prettyShow :: t -> String
+
+
+instance PrettyShowable Type where
+	prettyShow = prettyShowNormalized . normalize where
+		prettyShowNormalized x = case x of
+			TFun t1 t2 -> let
+					left = case t1 of
+						TFun _ _ -> "(" ++ (prettyShowNormalized t1) ++ ")"
+						_ -> prettyShowNormalized t1
+					right = prettyShowNormalized t2
+				in left ++ " -> " ++ right
+			TList t -> let
+					left = case t of
+						TFun _ _ -> "(" ++ (prettyShowNormalized t) ++ ")"
+						_ -> prettyShowNormalized t
+				in left ++ " list"
+			TInt -> "int"
+			TFloat -> "float"
+			TBool -> "bool"
+			TPoly (OPolyIdent p) -> p
+
+
+instance PrettyShowable UType where
+	prettyShow = prettyShow . convertUTypeToType
+
+
+instance PrettyShowable Value where
+	prettyShow x = case x of
+		VFun _ _ _ -> "<fun>"
+		VList [] -> "[]"
+		VList [x] -> "[" ++ (prettyShow x) ++ "]"
+		VList (x:xs) -> let
+				tailStr = foldl (\x y -> x ++ ";" ++ y) "" $ map prettyShow xs
+			in "[" ++ (prettyShow x) ++ tailStr ++ "]"
+		VFloat f -> show f
+		VInt i -> show i
+		VBool True -> "true"
+		VBool False -> "false"
+
+
+-- Automatically generated printer inserts \n in wrong places.
+instance PrettyShowable Exp where
+	prettyShow = foldr (\c s -> (if c == '\n' then ' ' else c):s) "" . printTree
+
+
+-- Normalize polymorphic identifiers to 'a, 'b, ...
+type NormalizationEnvironment = Map.Map OPolyIdent OPolyIdent
+
+normalize :: Type -> Type
+normalize t = evalState (normalizeImpl t) startMapEnv where
+	normalizeImpl :: Type -> State NormalizationEnvironment Type
+	normalizeImpl t = case t of
+		TFun t1 t2 -> do
+			t1' <- normalizeImpl t1
+			t2' <- normalizeImpl t2
+			return $ TFun t1' t2'
+		TList tl -> do
+			tl' <- normalizeImpl tl
+			return $ TList tl'
+		TPoly p -> do
+			p' <- lookupVar p
+			case p' of
+				Nothing -> do
+					newP <- nextIdent
+					assignVar p newP
+					return $ TPoly newP
+				Just x -> return $ TPoly x
+		_ -> return t
+
+	nextIdent :: State NormalizationEnvironment OPolyIdent
+	nextIdent = do
+		s <- get
+		return $ OPolyIdent $ "'" ++ (identWithNumber $ Map.size s) where
+			identWithNumber :: Int -> String
+			identWithNumber n = letter:number where
+				numLetters = ord 'z' - ord 'a' + 1
+				letter = chr $ ord 'a' + n `mod` numLetters
+				number = if n < numLetters then "" else show $ n `div` numLetters
+Language
+--------
+Xilocaml is a subset of OCaml language.
+
+Build
+-----
+To make both interpreter and documentation run "make".
+To make interpreter run "make interpreter".
+To make documentation run "make documentation".
+To run tests type run "make test".
+To clean compiled files run "make clean".
+To clean everything including generated files run "make distclean".
+To run ghci for debugging with properly included directories (Grammar) run "make edit".
+
+Build requirements
+------------------
+To make interpreter with grammar files provided beforehand (not empty "Grammar/" folder), you need GHC Haskell compiler.
+To make interpreter from scratch, you need GHC Haskell compiler and bnfc (which needs Happy parser generator and Alex lexer generator).
+To make documentation, you need pdflatex.
+
+Files
+-----
+Compiled interpreter will be placed in "./Xilocaml".
+Compiled documentation will be placed in "./doc/Xilocaml.pdf".
+
+Usage
+-----
+To run interpreter, run program "./Xilocaml" after compiling it (make interpreter).
+Input consists of a single expression and is read by interpreter from standard input.
+Output is written on standard output.
+Xilocaml is compatibile with OCaml interpreter, that is:
+* you may end single expression with ";;",
+* you may add "open List;;" in the beggining of the input (for hd and tl functions).
+You can compare results of Xilocaml interpreter and OCaml interpreter in following way:
+echo "1+1;;" | ocaml
+echo "1+1;;" | ./Xilocaml

RunEnvironment.hs

+module RunEnvironment where
+import qualified Data.Map as Map
+import Control.Monad.State
+import ErrM
+import AbsXilocaml
+
+
+-- Look out for comparisons of recursive functions with infinite environments.
+-- Difference with OCaml: int is of infinite precision instead of 31 bit.
+data Value =
+	VFun { fenv :: RunEnvironment, fargs :: [OIdent], fexp :: Exp }
+	| VList { lelems :: [Value] }
+	| VFloat { fval :: Double }
+	| VInt { ival :: Integer }
+	| VBool { bval :: Bool }
+	deriving (Eq,Ord,Show)
+
+
+type Result = Err Value
+type RunEnvironment = Map.Map OIdent Value
+type EnvRun = StateT RunEnvironment Err
+
+
+startREnv :: RunEnvironment
+startREnv = Map.empty
+
+
+assignEnv :: OIdent -> t -> StateT (Map.Map OIdent t) Err ()
+assignEnv ident val = modify $ Map.insert ident val
+
+lookupEnv :: OIdent -> StateT (Map.Map OIdent t) Err t
+lookupEnv ident = do
+	s <- get
+	return $ (Map.!) s ident
+
+tryLookupEnv :: OIdent -> StateT (Map.Map OIdent t) Err (Maybe t)
+tryLookupEnv ident = do
+	s <- get
+	return $ Map.lookup ident s
+
+
+-- Construction of infinite structure with all recursive functions and their environments is placed here
+-- Idea is like
+-- let f = VFun (Map.insert (OIdent "f") f Map.empty) [OIdent "x"] (EVar $ OIdent "x")
+-- but it's few times more evil because of "and"
+loopEnvironment :: [OIdent] -> EnvRun ()
+loopEnvironment idents = do
+	let loop s = let
+			env = loop s
+			updateEnv acc ident =
+				Map.insert ident (VFun env args exp) acc where
+					f = (Map.!) s ident
+					args = fargs f
+					exp = fexp f
+		in foldl updateEnv s idents
+	s <- get
+	put $ loop s
+module Semantics where
+import Control.Monad.State
+import Data.Maybe
+import AbsXilocaml
+import ErrM
+import TypeEnvironment
+import Unification
+import PrettyShow
+import Common
+
+
+-- 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 :: PrettyShowable a => String -> a -> String
+failurePrefix s x = "Semantic error: " ++ s ++ " in " ++ (prettyShow x) ++ "."
+
+failure :: PrettyShowable a => String -> a -> 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
+
+	ETrue -> returnType UBool
+
+	EFalse -> 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 ident -> do
+		val <- lookupId ident
+		case val of
+			Nothing -> failure ("undefined identifier " ++ identName 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 ident -> assignNewId ident
+				FunArgExplType 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 ident args exp ->
+				addRecFun ident args exp
+			LocalFunDeclExplType ident args _ exp ->
+				addRecFun ident args exp
+			_ -> return ()
+		addRecFunDecls decls
+	where
+		addRecFun :: OIdent -> [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 ident args _ -> addPolyToFun ident args
+			LocalFunDeclExplType ident args _ _ -> addPolyToFun ident args
+			_ -> return ()
+		addRecPolymorphism decls
+	where
+		addPolyToFun :: OIdent -> [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 ident -> assignId ident t1
+		FunArgExplType 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 ident ->
+			convertIdTypeToPoly ident
+		FunArgExplType ident _ ->
+			convertIdTypeToPoly ident
+	ts <- convertArgsToPolymorphic args
+	return (t:ts)

TypeEnvironment.hs

+module TypeEnvironment where
+import qualified Data.Map as Map
+import Control.Monad.State
+import Data.Maybe
+import ErrM
+import AbsXilocaml
+import Common
+
+-- Extended type system with two types of polymorphic values
+-- UPoly is polymorphic type
+-- UTerm is yet unspecified type and will become another type
+-- (possibly UPoly) after type inference process
+data UType =
+	UFun { argType :: UType, resType :: UType }
+	| UList { elemType :: UType }
+	| UInt
+	| UFloat
+	| UBool
+	| UPoly Int
+	| UTerm Int
+	deriving (Eq,Ord,Show)
+
+
+type ResultType = Err Type
+
+-- Environment consists of:
+-- * map: all visible identifiers -> their current UType.
+-- * map: currently used UTerms -> their computed type
+--   This map doesn't have UTerms for which no value was computed.
+--   It might contain other UTypes only in internals of some functions,
+--   for example to remember which UTerm is created from which UPoly.
+-- * number for next fresh UTerm
+data TypeEnvironment = TypeEnvironment { idEnv :: Map.Map OIdent UType, tEnv :: Map.Map UType UType, nextN :: Int }
+	deriving (Eq,Ord,Show)
+type EnvType = StateT TypeEnvironment Err
+
+
+startTEnv :: TypeEnvironment
+startTEnv = TypeEnvironment Map.empty Map.empty 0
+
+
+assignId :: OIdent -> UType -> EnvType UType
+assignId k v = do
+	modify $ \s -> TypeEnvironment (Map.insert k v $ idEnv s) (tEnv s) (nextN s)
+	return v
+
+assignType :: UType -> UType -> EnvType UType
+assignType k v = do
+	modify $ \s -> TypeEnvironment (idEnv s) (Map.insert k v $ tEnv s) (nextN s)
+	return v
+
+
+simpleLookupType :: UType -> EnvType (Maybe UType)
+simpleLookupType k = gets $ Map.lookup k . tEnv
+
+lookupId :: OIdent -> EnvType (Maybe UType)
+lookupId k = do
+	t <- gets $ Map.lookup k . idEnv
+	case t of
+		Nothing -> return t
+		Just x -> liftM Just $ lookupType x
+
+-- Looks up type of variable while compressing paths of term equations
+lookupType :: UType -> EnvType UType
+lookupType t = case t of
+	UTerm _ -> do
+		t' <- simpleLookupType t
+		case t' of
+			Nothing -> return t
+			Just x -> lookupType x >>= assignType t
+	UList t' -> liftM UList $ lookupType t'
+	UFun t1 t2 -> liftM2 UFun (lookupType t1) (lookupType t2)
+	_ -> return t
+
+
+nextTerm :: EnvType UType
+nextTerm = do
+	TypeEnvironment i t n <- get
+	put $ TypeEnvironment i t (n+1)
+	return (UTerm n)
+
+
+getIdentifiers :: EnvType (Map.Map OIdent UType)
+getIdentifiers = gets idEnv
+
+putIdentifiers :: Map.Map OIdent UType -> EnvType ()
+putIdentifiers i = modify $ \s -> TypeEnvironment i (tEnv s) (nextN s)
+
+assignNewId :: OIdent -> EnvType UType
+assignNewId ident = nextTerm >>= assignId ident
+
+
+-- Converts UTerm's to UPoly's using the same numeration.
+convertTermToPoly :: UType -> EnvType UType
+convertTermToPoly t = case t of
+	UFun t1 t2 ->
+		liftM2 UFun (convertTermToPoly t1) (convertTermToPoly t2)
+	UList tl ->
+		liftM UList (convertTermToPoly tl)
+	UTerm term -> assignType t $ UPoly term
+	_ -> return t
+
+
+-- Converts terms in type of identifier into UPoly's.
+convertIdTypeToPoly :: OIdent -> EnvType UType
+convertIdTypeToPoly ident = do
+	t <- liftM fromJust $ lookupId ident
+	t' <- convertTermToPoly t
+	assignId ident t'
+
+
+cleanEnvOfNonTerms :: EnvType ()
+cleanEnvOfNonTerms = modify $ \s -> TypeEnvironment (idEnv s) (Map.filterWithKey isUTerm $ tEnv s) (nextN s)
+	where
+		isUTerm :: UType -> t -> Bool
+		isUTerm (UTerm _) _ = True
+		isUTerm _ _ = False
+
+
+convertPolyToTerm :: UType -> EnvType UType
+convertPolyToTerm t = do
+		v <- lookupType t >>= convertPolyToTermImpl
+		cleanEnvOfNonTerms
+		return v
+	where
+		convertPolyToTermImpl :: UType -> EnvType UType
+		convertPolyToTermImpl t = case t of
+			UFun t1 t2 -> liftM2 UFun (convertPolyToTermImpl t1) (convertPolyToTermImpl t2)
+			UList tl -> liftM UList (convertPolyToTermImpl tl)
+			UPoly _ -> do
+				t' <- simpleLookupType t
+				case t' of
+					Nothing -> nextTerm >>= assignType t
+					Just x -> return x
+			_ -> return t
+
+
+-- Converts Type to UType. TPoly are changed to fresh UTerm's.
+convertTypeToUType :: Type -> EnvType UType
+convertTypeToUType t = let
+		t' = evalState (convertTypeToPolyUType t) startMapEnv
+	in convertPolyToTerm t'
+
+type TypeToPolyEnvironment = Map.Map OPolyIdent UType
+convertTypeToPolyUType :: Type -> State TypeToPolyEnvironment UType
+convertTypeToPolyUType t = case t of
+	TFun t1 t2 ->
+		liftM2 UFun (convertTypeToPolyUType t1) (convertTypeToPolyUType t2)
+	TList t' ->
+		liftM UList (convertTypeToPolyUType t')
+	TInt -> return UInt
+	TFloat -> return UFloat
+	TBool -> return UBool
+	TPoly p -> do
+		s <- get
+		t' <- lookupVar p
+		case t' of
+			Nothing -> assignVar p (UPoly $ Map.size s)
+			Just x -> return x
+
+
+-- Converts UType to Type. Both UTerm's and UPoly's are changed to TPoly.
+convertUTypeToType :: UType -> Type
+convertUTypeToType t = case t of
+	UFun t1 t2 -> TFun (convertUTypeToType t1) (convertUTypeToType t2)
+	UList t' -> TList $ convertUTypeToType t'
+	UInt -> TInt
+	UFloat -> TFloat
+	UBool -> TBool
+	UPoly p -> TPoly $ OPolyIdent $ show p
+	UTerm p -> TPoly $ OPolyIdent $ show p
+module Unification where
+import Control.Monad.State
+import ErrM
+import TypeEnvironment
+import PrettyShow
+
+
+unify :: String -> UType -> UType -> EnvType UType
+unify errorPrefix t1 t2 = do
+		t1' <- convertPolyToTerm t1
+		t2' <- convertPolyToTerm t2
+		unifyImpl t1' t2'
+	where
+		unifyImpl t1 t2 = do
+			t1 <- lookupType t1
+			t2 <- lookupType t2
+			case (t1,t2) of
+				(t1', t2') | t1' == t2' -> return t1'
+				(UTerm _, _) ->
+					if occurs t1 t2 then
+						failure "recursive types not supported"
+					else
+						assignType t1 t2
+				(_, UTerm _) -> unifyImpl t2 t1
+				(UList t1', UList t2') -> liftM UList $ unifyImpl t1' t2'
+				(UFun t1' t1'', UFun t2' t2'') ->
+					liftM2 UFun (unifyImpl t1' t2') (unifyImpl t1'' t2'')
+				_ -> failure "conflicting types"
+			where
+				failure :: String -> EnvType UType
+				failure message = lift $ Bad $ errorPrefix ++
+					" Unification of " ++ (prettyShow t1) ++ " and " ++
+					(prettyShow t2) ++ " failed: " ++ message ++ "."
+
+
+occurs :: UType -> UType -> Bool
+occurs term t = case t of
+	UFun t1 t2 -> occurs term t1 || occurs term t2
+	UList t' -> occurs term t'
+	UTerm _ -> term == t
+	_ -> False
+module UnitTests where
+import Test.HUnit
+import qualified Data.Map as Map
+import Control.Monad.State
+import AbsXilocaml
+import ParXilocaml
+import ErrM
+import Semantics
+import Interpreter
+import TypeEnvironment
+import RunEnvironment
+import Unification
+import Common
+import PrettyShow
+import Main hiding (main)
+
+
+tests =
+	TestList [
+		TestLabel "Semantics" $ TestList [
+			TestLabel "Primitive types" $ TestList [
+				assertParsedTypeEquals "1" TInt,
+				assertParsedTypeEquals "1.0" TFloat,
+				assertParsedTypeEquals "1." TFloat,
+				assertParsedTypeEquals "true" TBool
+			],
+			TestLabel "Arithmentic, logical and comparison operations" $ TestList [
+				assertParsedTypeEquals "not true" TBool,
+				assertParsedBadSemantics "not 1.0",
+				assertParsedTypeEquals "true || false" TBool,
+				assertParsedBadSemantics "1 <= 1.0",
+				assertParsedTypeEquals "1 * 3" TInt,
+				assertParsedTypeEquals "1.0 +. 3.0" TFloat,
+				assertParsedBadSemantics "1.0 + 2.0",
+				assertParsedTypeEquals "-. 1.0" TFloat,
+				assertParsedBadSemantics "+. 1",
+				assertParsedTypeEquals "1 + 1 > 2 && 2. *. 3. <= 2. || true && not false" TBool
+			],
+			TestLabel "Unary operators" $ TestList [
+				assertParsedTypeEquals "-1" TInt,
+				assertParsedTypeEquals "-1.0" TFloat,
+				assertParsedTypeEquals "-. -. +. 1." TFloat,
+				assertParsedTypeEquals "+ - - + 1" TInt,
+				assertParsedTypeEquals "+ -. - +. + - 1." TFloat
+			],
+			TestLabel "If-then-else" $ TestList [
+				assertParsedTypeEquals "if 1 > 2 then 1 else 4" TInt,
+				assertParsedTypeEquals "if true then false else true" TBool,
+				assertParsedBadSemantics "if 1 then false else true",
+				assertParsedBadSemantics "if true then 1 else 1.0"
+			],
+			TestLabel "Undefined variable" $ assertParsedBadSemantics "a",
+			TestLabel "Explicit types" $ TestList [
+				assertParsedTypeEquals "(1 : int)" TInt,
+				assertParsedBadSemantics "(1 : bool)",
+				assertParsedTypeEquals "(1+1*1 : int)" TInt,
+				assertParsedTypeEquals "(1 : 'a)" TInt,
+				assertParsedTypeEquals "(fun x -> x : 'a -> 'a)" $
+					TFun basicPolyType basicPolyType,
+				assertParsedTypeEquals "([] : 'a list)" $ TList basicPolyType,
+				assertParsedTypeEquals "(fun x -> x : 'a -> 'b)" $ TFun basicPolyType basicPolyType,
+				assertParsedTypeEquals "(fun x -> x : ('a -> 'a) -> ('b -> 'b))" $
+					TFun (TFun basicPolyType basicPolyType) (TFun basicPolyType basicPolyType)
+			],
+			TestLabel "Lists" $ TestList [
+				assertParsedTypeEquals "[]" $ TList $ basicPolyType,
+				assertParsedTypeEquals "[1]" $ TList TInt,
+				assertParsedTypeEquals "[[]]" $ TList $ TList basicPolyType,
+				assertParsedTypeEquals "1::[1]" $ TList TInt,
+				assertParsedTypeEquals "1::[]" $ TList TInt,
+				assertParsedTypeEquals "[]::[]" $ TList $ TList basicPolyType,
+				assertParsedTypeEquals "hd [1]" TInt,
+				assertParsedTypeEquals "hd [[]]" $ TList basicPolyType,
+				assertParsedTypeEquals "hd []" $ basicPolyType,
+				assertParsedTypeEquals "tl [1.0]" $ TList TFloat,
+				assertParsedTypeEquals "tl [[1.0]]" $ TList $ TList TFloat,
+				assertParsedTypeEquals "tl []" $ TList basicPolyType
+			],
+			TestLabel "Lambda" $ TestList [
+				assertParsedTypeEquals "fun (x : int) -> x" $ TFun TInt TInt,
+				assertParsedBadSemantics "fun (x : int) -> y",
+				assertParsedBadSemantics "fun (x : int) -> not x",
+				assertParsedTypeEquals "fun (x : int) (y : int) -> x + y" $ TFun TInt (TFun TInt TInt),
+				assertParsedTypeEquals "fun (x : int) -> fun (y : int) -> x * y" $ TFun TInt (TFun TInt TInt),
+				assertParsedTypeEquals "(fun (x : int) -> x : int -> int)" $ TFun TInt TInt,
+				assertParsedTypeEquals "fun (f : int -> int) -> f" $ TFun (TFun TInt TInt) (TFun TInt TInt)
+			],
+			TestLabel "Function application" $ TestList [
+				assertParsedTypeEquals "(fun (x : int) -> 2 * x) 3" TInt,
+				assertParsedTypeEquals "(fun x -> 2 * x) 3" TInt,
+				assertParsedTypeEquals "let f (x : int) = x in f 2" TInt
+			],
+			TestLabel "Let in" $ TestList [
+				assertParsedTypeEquals "let a = 2 in a" TInt,
+				assertParsedBadSemantics "let a = 2 in b",
+				assertParsedBadSemantics "let a = a in a",
+				assertParsedTypeEquals "let a : int = 2 in a" TInt,
+				assertParsedBadSemantics "let a : bool = 2 in a",
+				assertParsedTypeEquals "let a (x : int) = x in a" $ TFun TInt TInt,
+				assertParsedBadSemantics "let a (x : int) = not x in a",
+				assertParsedBadSemantics "let a (x : int) : bool = x in a",
+				assertParsedTypeEquals "let a (x : int) : int = 2 in a" $ TFun TInt TInt,
+				assertParsedTypeEquals "let a (x : int) : int = x in a" $ TFun TInt TInt
+			],
+			TestLabel "Let rec" $ TestList [
+				assertParsedTypeEquals "let rec x : int = 2 in x" TInt,
+				assertParsedTypeEquals "let rec l : 'a list = [] in l" $ TList basicPolyType,
+				assertParsedTypeEquals "let rec f (x : int) : int = x in f" $ TFun TInt TInt,
+				assertParsedTypeEquals "let rec f (x : int) : int = g x and g (x : int) : int = f x in f" $ TFun TInt TInt,
+				assertParsedTypeEquals "let rec a : int = 2 and f (x : int) : int = a * x in f 3" TInt
+			],
+			TestLabel "Let rec helper functions" $ TestList [
+				execStateT (prepareRecDecls
+					[LocalVarDecl (OIdent "a") (EInt 1), LocalVarDeclExplType (OIdent "b") TInt $ EInt 2])
+					(TypeEnvironment Map.empty Map.empty 0) ~?=
+					(Ok $ TypeEnvironment (Map.fromList [(OIdent "a", UInt), (OIdent "b", UInt)]) Map.empty 0),
+				execStateT (prepareRecDecls
+					[LocalFunDecl (OIdent "f") [FunArg $ OIdent "x"] $ EVar $ OIdent "x"])
+					(TypeEnvironment Map.empty Map.empty 0) ~?=
+					(Ok $ TypeEnvironment (Map.fromList [(OIdent "f", UFun (UTerm 1) (UTerm 0))]) Map.empty 2),
+				execStateT (prepareRecDecls
+					[LocalFunDecl (OIdent "f") [FunArgExplType (OIdent "x") basicPolyType] $ EVar $ OIdent "x"])
+					(TypeEnvironment Map.empty Map.empty 0) ~?=
+					(Ok $ TypeEnvironment (Map.fromList [(OIdent "f", UFun (UTerm 1) (UTerm 0))]) Map.empty 2),
+				execStateT (prepareRecDecls
+					[LocalFunDecl (OIdent "f") [FunArgExplType (OIdent "x") TInt, FunArg $ OIdent "y"] $ EVar $ OIdent "x"])
+					(TypeEnvironment Map.empty Map.empty 0) ~?=
+					(Ok $ TypeEnvironment (Map.fromList [(OIdent "f", UFun UInt (UFun (UTerm 1) (UTerm 0)))]) Map.empty 2),
+				execStateT (addRecFunDecls
+					[LocalFunDecl (OIdent "f") [FunArg $ OIdent "x"] $ EInt 1])
+					(TypeEnvironment (Map.fromList [(OIdent "f", UFun (UTerm 1) (UTerm 0)), (OIdent "x", UTerm 1)]) Map.empty 2) ~?=
+					(Ok $ TypeEnvironment
+						(Map.fromList [(OIdent "f", UFun (UTerm 1) (UTerm 0)), (OIdent "x", UTerm 1)])
+						(Map.fromList [(UTerm 0, UInt)]) 2),
+				execStateT (addRecFunDecls
+					[LocalFunDecl (OIdent "f") [FunArg $ OIdent "x"] $ EVar $ OIdent "x"])
+					(TypeEnvironment (Map.fromList [(OIdent "f", UFun (UTerm 1) (UTerm 0)), (OIdent "x", UTerm 1)]) Map.empty 2) ~?=
+					(Ok $ TypeEnvironment
+						(Map.fromList [(OIdent "f", UFun (UTerm 1) (UTerm 0)), (OIdent "x", UTerm 1)])
+						(Map.fromList [(UTerm 0, UTerm 1)]) 2),
+				execStateT (addRecFunDecls
+					[LocalFunDecl (OIdent "f") [FunArg $ OIdent "x"] $
+						EIfThenElse
+							(ECmp (EVar $ OIdent "x") OLeq (EInt 42))
+							(EVar $ OIdent "x")
+							(EAppl (EVar $ OIdent "f") (EVar $ OIdent "x"))])
+					(TypeEnvironment (Map.fromList [(OIdent "f", UFun (UTerm 1) (UTerm 0)), (OIdent "x", UTerm 1)]) Map.empty 2) ~?=
+					(Ok $ TypeEnvironment
+						(Map.fromList [(OIdent "f", UFun (UTerm 1) (UTerm 0)), (OIdent "x", UTerm 1)])
+						(Map.fromList [(UTerm 0, UInt), (UTerm 1, UInt), (UTerm 2, UInt)]) 3),
+				execStateT (addRecPolymorphism
+					[LocalFunDecl (OIdent "f") [FunArg $ OIdent "x"] $ EVar $ OIdent "x"])
+					(TypeEnvironment
+						(Map.fromList [(OIdent "f", UFun (UTerm 1) (UTerm 0)), (OIdent "x", UTerm 1)])
+						(Map.fromList [(UTerm 0, UTerm 1)]) 2) ~?=
+					(Ok $ TypeEnvironment
+						(Map.fromList [(OIdent "f", UFun (UTerm 1) (UTerm 0)), (OIdent "x", UTerm 1)])
+						(Map.fromList [(UTerm 0, UTerm 1),(UTerm 1, UPoly 1)]) 2)
+			],
+			TestLabel "Function type checker" $ TestList [
+				assertTypeEquals (checkFun [] (EInt 3)) startTEnv UInt,
+				assertBadSemantics (checkFun [] (EVar $ OIdent "x")) startTEnv,
+				assertTypeEquals (checkFun [FunArgExplType (OIdent "x") TInt] (EInt 2)) startTEnv $ UFun UInt UInt,
+				assertTypeEquals (checkFun [FunArgExplType (OIdent "x") TInt] (EVar $ OIdent "x")) startTEnv $ UFun UInt UInt,
+				assertTypeEquals (checkFun [] (EVar $ OIdent "x"))
+					(TypeEnvironment (Map.fromList[(OIdent "x", UInt)]) Map.empty 0) UInt,
+				assertTypeEquals (checkFun [FunArgExplType (OIdent "x") TBool] (EVar $ OIdent "x"))
+					(TypeEnvironment (Map.fromList [(OIdent "x", UInt)]) Map.empty 0) $ UFun UBool UBool
+			],
+			TestLabel "Type inference" $ TestList [
+				assertParsedTypeEquals "1" TInt,
+				assertParsedTypeEquals "[[];[1]]" $ TList $ TList TInt,
+				assertParsedTypeEquals "[[];[[]]]" $ TList $ TList $ TList basicPolyType,
+				assertParsedTypeEquals "fun x -> x" $ TFun basicPolyType basicPolyType,
+				assertParsedTypeEquals "fun x y -> x" $ TFun basicPolyType $ TFun basicPolyType' basicPolyType,
+				assertParsedTypeEquals "let f x = x in f" $ TFun basicPolyType basicPolyType,
+				assertParsedTypeEquals "let l = [] in l" $ TList basicPolyType,
+				assertParsedTypeEquals "let rec l = [] in l" $ TList basicPolyType,
+				assertParsedTypeEquals "let rec f x = f x in f" $ TFun basicPolyType basicPolyType'
+			],
+			TestLabel "Limitations of type inference in recursion" $ TestList [
+				assertParsedTypeEquals "let rec l = [] and l' = 1::l in l" $ TList TInt,
+				assertParsedBadSemantics "let rec l = [] and l' = 1::l and l'' = []::l in l"
+			],
+			TestLabel "Function comparison" $ TestList [
+				TestLabel "Limitation for polymorphic functions" $
+					assertParsedTypeEquals "let cmp (x : 'a) (y : 'a) : bool = x < y in cmp (fun x -> 3 * x) (fun x -> 2 * x)" TBool,
+				assertParsedBadSemantics "(fun x -> 3 * x) < (fun x -> 2 * x)"
+			],
+			TestLabel "Unification - without testing environment" $ TestList [
+				assertUnifiedTypesEqual UInt UInt UInt,
+				assertUnificationFails UInt UBool,
+				assertUnifiedTypesEqual (UTerm 0) UInt UInt,
+				assertUnifiedTypesEqual (UTerm 0) (UTerm 1) (UTerm 0),
+				assertUnifiedTypesEqual (UTerm 0) (UTerm 1) (UTerm 1),
+				assertUnifiedTypesEqual (UList $ UTerm 0) (UList UInt) (UList UInt),
+				assertUnifiedTypesEqual (UFun UInt UInt) (UFun UInt UInt) (UFun UInt UInt),
+				assertUnificationFails (UFun UInt UBool) (UFun UInt UInt),
+				assertUnificationFails (UFun UBool UInt) (UFun UInt UInt),
+				assertUnifiedTypesEqual (UTerm 0) (UList $ UTerm 1) (UList $ UTerm 1),
+				assertUnifiedTypesEqual (UFun (UTerm 0) UInt) (UFun UBool UInt) (UFun UBool UInt),
+				assertUnificationFails (UFun (UTerm 0) (UTerm 0)) (UFun (UTerm 1) (UFun (UTerm 1) (UTerm 1))),
+				assertUnifiedTypesEqual
+					(UFun (UFun (UTerm 0) (UTerm 0)) (UTerm 0))
+					(UFun (UTerm 1) (UFun (UTerm 2) (UTerm 2)))
+					(UFun (UFun (UFun (UTerm 2) (UTerm 2)) (UFun (UTerm 2) (UTerm 2))) (UFun (UTerm 2) (UTerm 2))),
+				assertUnifiedTypesEqual
+					(UFun (UList $ UFun (UTerm 0) (UTerm 0)) (UTerm 0))
+					(UFun (UList $ UTerm 1) UInt)
+					(UFun (UList $ UFun UInt UInt) UInt),
+				assertUnificationFails (UFun (UList (UTerm 0)) (UTerm 0)) (UFun (UTerm 0) (UList (UTerm 0))),
+				assertUnifiedTypesEqual
+					(UFun (UTerm 0) (UTerm 0))
+					(UFun (UFun (UTerm 1) (UTerm 1)) (UFun (UTerm 2) (UTerm 2)))
+					(UFun (UFun (UTerm 1) (UTerm 1)) (UFun (UTerm 1) (UTerm 1)))
+			],
+			TestLabel "Unification - with testing environment" $ TestList [
+				runStateT (unify "" (UList UInt) (UList UInt))
+					(TypeEnvironment Map.empty Map.empty 0) ~?=
+					Ok (UList UInt, TypeEnvironment Map.empty Map.empty 0),
+				runStateT (unify "" (UTerm 0) (UTerm 1))
+					(TypeEnvironment Map.empty Map.empty 2) ~?=
+					Ok (UTerm 1, TypeEnvironment Map.empty (Map.fromList [(UTerm 0, UTerm 1)]) 2),
+				runStateT (unify "" (UTerm 0) (UTerm 1))
+					(TypeEnvironment Map.empty (Map.fromList [(UTerm 0, UTerm 2)]) 3) ~?=
+					Ok (UTerm 1, TypeEnvironment Map.empty (Map.fromList [(UTerm 2, UTerm 1), (UTerm 0, UTerm 2)]) 3),
+				runStateT (unify "" (UTerm 0) (UTerm 1))
+					(TypeEnvironment Map.empty (Map.fromList [(UTerm 0, UList $ UTerm 2)]) 3) ~?=
+					Ok (UList $ UTerm 2, TypeEnvironment Map.empty (Map.fromList [(UTerm 1, UList $ UTerm 2), (UTerm 0, UList $ UTerm 2)]) 3),
+				runStateT (unify "" (UTerm 0) (UTerm 1))
+					(TypeEnvironment Map.empty (Map.fromList [(UTerm 0, UTerm 1)]) 3) ~?=
+					Ok (UTerm 1, TypeEnvironment Map.empty (Map.fromList [(UTerm 0, UTerm 1)]) 3),
+				assertBad $ runStateT (unify "" (UTerm 0) (UTerm 1))
+					(TypeEnvironment Map.empty (Map.fromList [(UTerm 0, UList $ UTerm 1)]) 3),
+				evalStateT (unify ""
+						(UFun (UTerm 0) (UTerm 0))
+						(UFun (UFun (UPoly 0) (UPoly 0)) (UFun (UPoly 1) (UPoly 1)))
+						>>= lookupType)
+					(TypeEnvironment Map.empty Map.empty 7) ~?=
+					Ok (UFun (UFun (UTerm 8) (UTerm 8)) (UFun (UTerm 8) (UTerm 8)))
+			],
+			TestLabel "Normalization" $ TestList [
+				normalize (TFun TInt TInt) ~?= TFun TInt TInt,
+				normalize (TPoly $ OPolyIdent "'a") ~?= TPoly (OPolyIdent "'a"),
+				normalize
+					(TFun (TFun (TList $ TPoly $ OPolyIdent "'x") TInt) (TFun (TPoly $ OPolyIdent "'y") (TPoly $ OPolyIdent "'x"))) ~?=
+					(TFun (TFun (TList $ TPoly $ OPolyIdent "'a") TInt) (TFun (TPoly $ OPolyIdent "'b") (TPoly $ OPolyIdent "'a")))
+			],
+			TestLabel "Helper functions" $ TestList [
+				occurs (UTerm 2) (UFun UInt (UList $ UTerm 2)) ~?= True,
+				occurs (UTerm 1) (UFun (UFun (UPoly 1) (UTerm 2)) (UList $ UFun UInt (UTerm 3))) ~?= False
+			],
+			TestLabel "UType -> Type conversion" $ TestList [
+				convertUTypeToType (UFun (UFun UInt UBool) (UList $ UFun UFloat UFloat)) ~?=
+					TFun (TFun TInt TBool) (TList $ TFun TFloat TFloat),
+				convertUTypeToType (UFun (UTerm 2) (UList $ UTerm 2)) ~?=
+					TFun (TPoly $ OPolyIdent "2") (TList $ TPoly $ OPolyIdent "2"),
+				normalize (convertUTypeToType $ UFun UInt (UFun (UPoly 2) (UList $ UFun (UPoly 1) (UPoly 2)))) ~?=
+					TFun TInt (TFun (basicPolyType) (TList $ TFun (basicPolyType') (basicPolyType)))
+			],
+			TestLabel "UTerm -> UPoly conversion for identifiers" $ TestList [
+				runStateT (convertIdTypeToPoly $ OIdent "x")
+					(TypeEnvironment (Map.fromList [(OIdent "x", UFun UInt UBool)]) Map.empty 0) ~?=
+					Ok (UFun UInt UBool, TypeEnvironment (Map.fromList [(OIdent "x", UFun UInt UBool)]) Map.empty 0),
+				runStateT (convertIdTypeToPoly $ OIdent "x")
+					(TypeEnvironment (Map.fromList [(OIdent "x", UTerm 1)]) Map.empty 2) ~?=
+					Ok (UPoly 1, TypeEnvironment (Map.fromList [(OIdent "x", UPoly 1)]) (Map.fromList [(UTerm 1, UPoly 1)]) 2),
+				evalStateT (convertIdTypeToPoly $ OIdent "x")
+					(TypeEnvironment
+						(Map.fromList [(OIdent "x", UTerm 2)])
+						(Map.fromList [(UTerm 2, UTerm 1)]) 3) ~?=
+					(Ok $ UPoly 1),
+				evalStateT (convertIdTypeToPoly $ OIdent "x")
+					(TypeEnvironment
+						(Map.fromList [(OIdent "x", UTerm 3)])
+						(Map.fromList [(UTerm 3, UTerm 1), (UTerm 1, UFun UBool (UTerm 0))]) 4) ~?=
+					(Ok $ UFun UBool (UPoly 0)),
+				evalStateT (convertIdTypeToPoly $ OIdent "x")
+					(TypeEnvironment
+						(Map.fromList [(OIdent "x", UTerm 1), (OIdent "y", UTerm 2)])
+						(Map.fromList [(UTerm 2, UTerm 1)]) 4) ~?=
+					(Ok $ UPoly 1)
+			],
+			TestLabel "UPoly -> UTerm conversion" $ TestList [
+				runStateT (convertPolyToTerm $ UFun UInt UBool)
+					(TypeEnvironment Map.empty Map.empty 0) ~?=
+					Ok (UFun UInt UBool, TypeEnvironment Map.empty Map.empty 0),
+				runStateT (convertPolyToTerm $ UFun (UPoly 1) (UPoly 2))
+					(TypeEnvironment Map.empty Map.empty 3) ~?=
+					Ok (UFun (UTerm 3) (UTerm 4), TypeEnvironment Map.empty Map.empty 5),
+				runStateT (convertPolyToTerm $ UFun (UPoly 1) (UPoly 1))
+					(TypeEnvironment Map.empty Map.empty 5) ~?=
+					Ok (UFun (UTerm 5) (UTerm 5), TypeEnvironment Map.empty Map.empty 6),
+				runStateT (convertPolyToTerm $ UFun (UFun UBool (UPoly 1)) (UFun (UPoly 2) (UList $ UPoly 1)))
+					(TypeEnvironment Map.empty Map.empty 3) ~?=
+					Ok (UFun (UFun UBool (UTerm 3)) (UFun (UTerm 4) (UList $ UTerm 3)), TypeEnvironment Map.empty Map.empty 5)
+			],
+			TestLabel "Type -> UType conversion" $ TestList [
+				runStateT (convertTypeToUType $ TFun TBool TBool) startTEnv ~?=
+					Ok (UFun UBool UBool, TypeEnvironment Map.empty Map.empty 0),
+				runStateT (convertTypeToUType $ TFun (TFun basicPolyType basicPolyType') basicPolyType) startTEnv ~?=
+					Ok (UFun (UFun (UTerm 0) (UTerm 1)) (UTerm 0), TypeEnvironment Map.empty Map.empty 2),
+				runStateT (convertTypeToUType $ TFun (TFun basicPolyType basicPolyType) (TFun basicPolyType basicPolyType)) startTEnv ~?=
+					Ok (UFun (UFun (UTerm 0) (UTerm 0)) (UFun (UTerm 0) (UTerm 0)), TypeEnvironment Map.empty Map.empty 1),
+				runState (convertTypeToPolyUType $ TFun (TList TInt) (TFun (TList $ basicPolyType) (TList $ TFun basicPolyType basicPolyType'))) startMapEnv ~?=
+					(UFun (UList UInt) (UFun (UList $ UPoly 0) (UList $ UFun (UPoly 0) (UPoly 1))),
+						Map.fromList [(OPolyIdent "'a", UPoly 0), (OPolyIdent "'b", UPoly 1)])
+			],
+			TestLabel "Hard cases" $ TestList [
+				assertParsedBadSemantics "fun x -> x x",
+				assertParsedBadSemantics "fun x y -> x x y"
+			],
+			TestLabel "Program structure" $ TestList [
+				assertParsedTypeEquals "open List;; hd [1];;" TInt,
+				assertParsedTypeEquals "hd [1];;" TInt,
+				assertParsedTypeEquals "open List;; hd [1]" TInt,
+				assertParsedTypeEquals "hd [1]" TInt
+			]
+		],
+		TestLabel "Interpreter" $ TestList [
+			TestLabel "Primitive types" $ TestList [
+				assertParsedValueEquals "42" $ VInt 42,
+				assertParsedValueEquals "true" $ VBool True,
+				assertParsedValueEquals "false" $ VBool False,
+				assertParsedValueEquals "42.0" $ VFloat 42.0,
+				assertParsedValueEquals "42." $ VFloat 42.0,
+				assertParsedValueEquals "42.e0" $ VFloat 42.0,
+				assertParsedValueEquals "4.2E1" $ VFloat 42.0,
+				assertParsedValueEquals ".42e2" $ VFloat 42.0,
+				assertParsedValueEquals "4.2e+1" $ VFloat 42.0,
+				assertParsedValueEquals "420e-1" $ VFloat 42.0
+			],
+			TestLabel "Arithmentic, logical and comparison operations" $ TestList [
+				assertParsedValueEquals "not true" $ VBool False,
+				assertParsedValueEquals "true || false" $ VBool True,
+				assertParsedValueEquals "false || false" $ VBool False,
+				assertParsedValueEquals "true || true" $ VBool True,
+				assertParsedValueEquals "true && true" $ VBool True,
+				assertParsedValueEquals "true && false" $ VBool False,
+				assertParsedValueEquals "false && false" $ VBool False,
+				assertParsedValueEquals "true || true && false" $ VBool True,
+				assertParsedValueEquals "2 + 2 * 2" $ VInt 6,
+				assertParsedValueEquals "3 / 1 - 1" $ VInt 2,
+				assertParsedRuntimeError "1 / 0",
+				assertParsedRuntimeError "0 / 0",
+				assertParsedValueEquals "1 + 2 <= 3" $ VBool True,
+				assertParsedValueEquals "2 > 2 && 2 < 5" $ VBool False,
+				assertParsedValueEquals "3 = 5 || 3 >= 4" $ VBool False,
+				assertParsedValueEquals "2 >= 3 || 2 = 3 || 3 > 4 && 3 < 4 || 2 <> 2" $ VBool False,
+				assertParsedValueEquals "1 = 1 || 1 = 1 / 0" $ VBool True,
+				assertParsedValueEquals "1 = 0 && 1 = 1 / 0" $ VBool False
+			],
+			TestLabel "If-then-else" $ TestList [
+				assertParsedValueEquals "if 1 > 2 then 1 else 4" $ VInt 4,
+				assertParsedValueEquals "if true then false else true" $ VBool False,
+				assertParsedValueEquals "if true then 1 else 1 / 0" $ VInt 1,
+				assertParsedRuntimeError "if true then 0 / 0 else 2"
+			],
+			TestLabel "Unary operators" $ TestList [
+				assertParsedValueEquals "-1" $ VInt (-1),
+				assertParsedValueEquals "-1.0" $ VFloat (-1.0)
+			],
+			TestLabel "Explicit types" $ TestList [
+				assertParsedValueEquals "(1 : int)" $ VInt 1,
+				assertParsedValueEquals "(1+1*1 : int)" $ VInt 2,
+				assertParsedValueEquals "([] : 'a list)" $ VList []
+			],
+			TestLabel "Lists" $ TestList [
+				assertParsedValueEquals "[]" $ VList [],
+				assertParsedValueEquals "[1]" $ VList [VInt 1],
+				assertParsedValueEquals "[true; false]" $ VList [VBool True, VBool False],
+				assertParsedValueEquals "1::[1]" $ VList [VInt 1, VInt 1],
+				assertParsedValueEquals "1::[]" $ VList [VInt 1],
+				assertParsedValueEquals "[]::[]" $ VList [VList []],
+				assertParsedValueEquals "hd [1]" $ VInt 1,
+				assertParsedValueEquals "hd [[]]" $ VList [],
+				assertParsedRuntimeError "hd []",
+				assertParsedValueEquals "tl [1.0]" $ VList [],
+				assertParsedValueEquals "tl [[1.0]]" $ VList [],
+				assertParsedValueEquals "tl [[1;2];[3]]" $ VList [VList [VInt 3]],
+				assertParsedRuntimeError "tl []",
+				assertParsedRuntimeError "2::[1+1;1/0]"
+			],
+			TestLabel "Lambda" $ TestList [
+				assertParsedValueEquals "fun (x : int) -> x" $ VFun startREnv [OIdent "x"] $ EVar (OIdent "x"),
+				assertParsedValueEquals "fun (x : int) (y : int) -> x + y" $ VFun startREnv [OIdent "x", OIdent "y"] $ EInfixWeak (EVar $ OIdent "x") OAdd (EVar $ OIdent "y"),
+				assertParsedValueEquals "fun (x : int) -> fun (y : int) -> x * y" $ VFun startREnv [OIdent "x"] $ ELambda [FunArgExplType (OIdent "y") TInt] $ EInfixStrong (EVar $ OIdent "x") OMul (EVar $ OIdent "y"),
+				assertParsedValueEquals "fun (f : int -> int) -> f" $ VFun startREnv [OIdent "f"] $ EVar (OIdent "f"),
+				assertParsedValueEquals "fun (x : int) -> x / 0" $ VFun startREnv [OIdent "x"] $ EInfixStrong (EVar $ OIdent "x") ODiv (EInt 0)
+			],
+			TestLabel "Function application" $ TestList [
+				assertParsedValueEquals "(fun (x : int) -> 2 * x) 3" $ VInt 6,
+				assertParsedValueEquals "(fun (x : int) (y : bool) -> if y then 2 * x else 3 * x) 2 false" $ VInt 6,
+				assertParsedValueEquals "(fun (x : int) (y : int) -> x * y) 2" $ VFun (createEnv [("x", VInt 2)]) [OIdent "y"] $ EInfixStrong (EVar $ OIdent "x") OMul (EVar $ OIdent "y"),
+				assertParsedValueEquals "(fun (x : int) (y : bool) -> fun (x : int) -> 2 * x) 2 true" $ VFun (createEnv [("y", VBool True), ("x", VInt 2)]) [OIdent "x"] $ EInfixStrong (EInt 2) OMul (EVar $ OIdent "x")
+			],
+			TestLabel "Comparison of functions" $ assertParsedRuntimeError "(fun x -> x = x) (fun x -> x)",
+			TestLabel "Let in" $ TestList [
+				assertParsedValueEquals "let a = 2 in a" $ VInt 2,
+				assertParsedValueEquals "let a : int = 2 in a" $ VInt 2,
+				assertParsedValueEquals "let a (x : int) = x in a" $ VFun startREnv [OIdent "x"] $ EVar (OIdent "x"),
+				assertParsedValueEquals "let a (x : int) : int = 2 in a" $ VFun startREnv [OIdent "x"] $ EInt 2,
+				assertParsedValueEquals "let a (x : int) : int = x in a" $ VFun startREnv [OIdent "x"] $ EVar (OIdent "x"),
+				assertParsedValueEquals "1 + (let a = 2 in a + a)" $ VInt 5
+			],
+			TestLabel "Let rec" $ TestList [
+				assertParsedValueEquals "let rec a = 2 in a" $ VInt 2,
+				assertParsedValueEquals "let rec f (x : int) : int = if x <= 0 then -1 else 1 + f (x / 2) in f 1024" $ VInt 10,
+				assertParsedValueEquals "let rec f (x : int) : int = if x <= 1 then 1 else x * f (x - 1) in f 6" $ VInt 720,
+				assertParsedValueEquals "let rec a (x : int) : int = 2 and f (x : int) : int = x * a 3 in f 21" $ VInt 42,
+				assertParsedValueEquals "let rec f (x : int) : int = g (x-1) and g (x : int) : int = if x <= 0 then 0 else f x in f 10" $ VInt 0,
+				assertParsedValueEquals "(let y = 2 in let rec f (x : int) : int = g (x-1) and g (x : int) : int = if x = 0 then y else f x in f) 20" $ VInt 2,
+				assertParsedValueEquals "let f = 2 in let g (x : int) = f * x in let rec f (x : int) : int = if x = 0 then 1 else f (x-1) in g (f 3)" $ VInt 2,
+				assertParsedValueEquals "let rec res = 0 and f x = if x <= 0 then res else f (x - 1) in f 10" $ VInt 0
+			],
+			TestLabel "Looping environment" $ TestList [
+				assertVariableFound ["x"] $ Ok $ createEnv [("x", VInt 1)],
+				assertVariableFound ["f", "y"] $ Ok $ createEnv [("f", VFun (createEnv [("y", VInt 1)]) [] ETrue)],
+				assertVariableFound ["f"] $
+					execStateT (loopEnvironment [OIdent "f"]) $ createEnv
+						[("f", VFun startREnv [] ETrue)],
+				assertVariableFound ["f", "f", "f", "f", "f"] $
+					execStateT (loopEnvironment [OIdent "f"]) $
+					createEnv [("f", VFun startREnv [] ETrue)],
+				assertVariableFound ["f", "f", "f", "f", "a"] $
+					execStateT (loopEnvironment [OIdent "f"]) $ createEnv
+						[("f", VFun startREnv [] ETrue),
+						("a", VInt 1)],
+				assertVariableFound ["f", "f", "g", "f", "g"] $
+					execStateT (loopEnvironment [OIdent "f", OIdent "g"]) $ createEnv
+						[("f", VFun startREnv [] ETrue),
+						("g", VFun startREnv [] ETrue),
+						("a", VInt 1)],
+				assertVariableFound ["g", "f", "g", "f", "f", "h", "h", "f", "a"] $
+					execStateT (loopEnvironment [OIdent "f", OIdent "g", OIdent "h"]) $ createEnv
+						[("f", VFun startREnv [] ETrue),
+						("g", VFun startREnv [] ETrue),
+						("h", VFun startREnv [] ETrue),
+						("a", VInt 1),
+						("b", VBool True)]
+			]
+		],
+		TestLabel "Pretty printer" $ TestList [
+			TestLabel "Types" $ TestList [
+				prettyShow (TInt) ~?= "int",
+				prettyShow (TFun TInt (TFun TBool TFloat)) ~?= "int -> bool -> float",
+				prettyShow (TFun (TFun TInt TBool) TBool) ~?= "(int -> bool) -> bool",
+				prettyShow (TList $ TList TBool) ~?= "bool list list",
+				prettyShow (TList $ TFun TBool TInt) ~?= "(bool -> int) list",
+				prettyShow (TFun basicPolyType basicPolyType') ~?= "'a -> 'b"
+			],
+			TestLabel "Values" $ TestList [
+				prettyShow (VInt 42) ~?= "42",
+				prettyShow (VFun startREnv [] ETrue) ~?= "<fun>",
+				prettyShow (VList [VBool True, VBool False]) ~?= "[true;false]",
+				prettyShow (VList [VBool True]) ~?= "[true]",
+				prettyShow (VList []) ~?= "[]",
+				prettyShow (VList [VFun startREnv [] ETrue, VFun startREnv [] ETrue]) ~?= "[<fun>;<fun>]"
+			],
+			TestLabel "UTypes" $ TestList [
+				prettyShow (UFun UInt (UList UBool)) ~?= "int -> bool list",
+				prettyShow (UFun (UPoly 1) (UPoly 2)) ~?= "'a -> 'b",
+				prettyShow (UFun (UList $ UTerm 1) (UTerm 3)) ~?= "'a list -> 'b",
+				prettyShow (UFun (UPoly 2) (UFun (UPoly 1) (UPoly 2))) ~?= "'a -> 'b -> 'a",
+				prettyShow (UFun (UFun (UPoly 1) (UPoly 2)) (UFun (UPoly 1) (UPoly 2))) ~?= "('a -> 'b) -> 'a -> 'b"
+			]
+		],
+		TestLabel "Main program" $ TestList [
+			printResult "1+1" ~?= "2 : int",
+			printResult "[let f (x : int) = 2 * x in f];;" ~?= "[<fun>] : (int -> int) list"
+		],
+		TestLabel "Full check for examples/" $ TestList [
+			TestLabel "arithmetic.ml" $ printResult "1 - 1 - 1 + 11 + 2 * 4 / 2 * 8 + 6 / 3 mod 2;; (* = 42 *)" ~?= "42 : int",
+			TestLabel "factorial.ml" $ printResult
+				"let rec factorial n = \
+				\    if n <= 1 then \
+				\        1 \
+				\    else \
+				\        n * factorial (n-1) \
+				\in factorial 6;;" ~?= "720 : int",
+			TestLabel "identity.ml" $ printResult "let f x = x in f;;" ~?= "<fun> : 'a -> 'a",
+			TestLabel "unary.ml" $ printResult "- -. - + +. + + - - -. - 1.0;;" ~?= "-1.0 : float",
+			TestLabel "factorization.ml" $ printResult
+				"let factorization n = \
+				\    let rec fact n div acc = \
+				\        if n mod div = 0 then \
+				\            fact (n / div) div (div::acc) \
+				\        else if n < div then \
+				\            acc \
+				\        else \
+				\            fact n (div + 1) acc \
+				\    in fact n 2 [] \
+				\in factorization 48;;" ~?= "[3;2;2;2;2] : int list",
+			TestLabel "fold_left.ml" $ printResult
+				"open List;; \
+				\let rec fold_left (f : 'a -> 'b -> 'a) (acc : 'a) (t : 'b list) : 'a = \
+				\    if t = [] then \
+				\        acc \
+				\    else \
+				\        fold_left f (f acc (hd t)) (tl t) \
+				\in fold_left (fun acc e -> acc + e) 0 [1;2;3;4;5];; (* sum of 1..5 *)" ~?= "15 : int"
+		]
+	]
+
+
+main = runTestTT tests
+
+basicPolyType = TPoly $ OPolyIdent "'a"
+basicPolyType' = TPoly $ OPolyIdent "'b"
+
+parsed input = do
+	tree <- pProgram $ myLexer input
+	t <- checkSemantics tree
+	return $ normalize t
+
+interpreted input = do
+	tree <- pProgram $ myLexer input
+	return $ interpret tree
+
+assertParsedTypeEquals :: String -> Type -> Test
+assertParsedTypeEquals input expectedType =
+	case parsed input of
+		Ok t -> t ~?= expectedType
+		Bad s -> TestCase $ assertFailure $ "No type, but expected " ++ (show expectedType) ++ " in " ++ input ++ ". Error message: " ++ s ++ "."
+
+assertParsedBadSemantics :: String -> Test
+assertParsedBadSemantics input =
+	case parsed input of
+		Ok t -> TestCase $ assertFailure $ "Detected type " ++ (show t) ++ ", but expected type error in " ++ input ++ "."
+		Bad s -> TestCase $ assertBool "" True
+
+assertBad :: Show t => Err t -> Test
+assertBad e =
+	case e of
+		Ok x -> TestCase $ assertFailure $ "Expected bad in " ++ (show e)
+		Bad s -> TestCase $ assertBool "" True
+
+assertTypeEquals :: EnvType UType -> TypeEnvironment -> UType -> Test
+assertTypeEquals envType env expectedType =
+	evalStateT envType env ~?= Ok expectedType
+
+assertTypesEquals :: EnvType [UType] -> TypeEnvironment -> [UType] -> Test
+assertTypesEquals envType env expectedTypes =
+	evalStateT envType env ~?= Ok expectedTypes
+
+assertBadSemantics :: EnvType UType -> TypeEnvironment -> Test
+assertBadSemantics envType env =
+	assertBad $ evalStateT envType env
+
+assertParsedValueEquals :: String -> Value -> Test
+assertParsedValueEquals input expectedValue =
+	case interpreted input of
+		Ok (Ok t) -> t ~?= expectedValue
+		Ok (Bad s) -> TestCase $ assertFailure $ "Runtime error, but expected " ++ (show expectedValue) ++ " in " ++ input ++ ". Error message: " ++ s ++ "."
+		Bad s -> TestCase $ assertFailure s
+
+assertParsedRuntimeError :: String -> Test
+assertParsedRuntimeError input =
+	case interpreted input of
+		Ok (Ok t) -> TestCase $ assertFailure $ "Detected value " ++ (show t) ++ ", but expected runtime error in " ++ input ++ "."
+		Ok (Bad s) -> TestCase $ assertBool "" True
+		Bad s -> TestCase $ assertFailure s
+
+-- Input is sequence of identifiers of which every but last must be a function type.
+assertVariableFound :: [String] -> Err RunEnvironment -> Test
+assertVariableFound _ (Bad s) = TestCase $ assertFailure s
+assertVariableFound identStrs (Ok env) = let
+		lookupVariable :: [OIdent] -> EnvRun ()
+		lookupVariable [] = return ()
+		lookupVariable [ident] = do
+			v <- tryLookupEnv ident
+			case v of
+				Nothing -> lift $ Bad $ "Looked up variable " ++ (identName ident) ++ " doesn't exist."
+				Just _ -> return ()
+		lookupVariable (ident:idents) = do
+			v <- tryLookupEnv ident
+			case v of
+				Nothing -> lift $ Bad $ "Looked up variable " ++ (identName ident) ++ " doesn't exist."
+				Just (VFun env _ _) -> do
+					put env
+					lookupVariable idents
+				Just _ -> lift $ Bad $ "Looked up variable " ++ (identName ident) ++ " is not a function."
+		found = evalStateT (lookupVariable $ map OIdent identStrs) env
+	in case found of
+		Ok _ -> TestCase $ assertBool "" True
+		Bad s -> TestCase $ assertFailure s
+
+
+createEnv :: [(String, t)] -> Map.Map OIdent t
+createEnv mapping = Map.fromList $ map (\(s,v) -> (OIdent s, v)) mapping
+
+assertUnifiedTypesEqual :: UType -> UType -> UType -> Test
+assertUnifiedTypesEqual t1 t2 expected =
+	case evalStateT runTest startTEnv of
+		Ok test -> test
+		Bad s -> TestCase $ assertFailure s
+	where
+		runTest :: EnvType Test
+		runTest = do
+			t' <- unify "" t1 t2
+			t'' <- lookupType t'
+			t1' <- lookupType t1
+			t2' <- lookupType t2
+			expected' <- lookupType expected
+			return $ TestLabel "Unification test internals" $ TestList [
+					t'' ~?= expected',
+					t1' ~?= expected',
+					t2' ~?= expected'
+				]
+
+assertUnificationFails :: UType -> UType -> Test
+assertUnificationFails t1 t2 =
+	assertBad $ evalStateT (unify "" t1 t2) startTEnv
+-- This language is subset of Ocaml
+
+-- Unlike in OCaml, nested comments aren't allowed
+comment "(*" "*)" ;
+
+-- More Options than for Double (mainly 1.)
+token OFloat (((digit+ '.' digit*)|('.' digit+))(('e'|'E') ('+'|'-')? digit+)?)|
+             (digit+ ('e'|'E') ('-')? digit+) ;
+-- Identifier for function and argument names
+token OIdent lower (letter | digit | '_' | '\'')* ;
+-- Identifier for polymorphic types
+token OPolyIdent '\'' (letter | digit | '_' | '\'')* ;
+
+Prog. Program ::= ComBeg Exp ComEnd ;
+-- Compability with Ocaml
+CompatibOpen.  ComBeg ::= "open" "List" ";;" ;
+CompatibBeg.   ComBeg ::= ;
+CompatibColon. ComEnd ::= ";;" ;
+CompatibEnd.   ComEnd ::= ;
+
+-- In Ocaml let has every priority and greedy second Exp (possible "1+let a=2 in a + a")
+ELetIn.       Exp  ::= "let" [LocDecl] "in" Exp ;
+ELetRecIn.    Exp  ::= "let" "rec" [LocDecl] "in" Exp ;
+ELambda.      Exp  ::= "fun" [Argument] "->" Exp ;
+EIfThenElse.  Exp  ::= "if" Exp "then" Exp "else" Exp ;
+EOr.          Exp1 ::= Exp1 "||"  Exp2 ;
+EAnd.         Exp2 ::= Exp2 "&&"  Exp3 ;
+ECmp.         Exp3 ::= Exp3 OCmp  Exp4 ;
+-- In Ocaml Exp4 part here is Exp
+EPrepend.     Exp4 ::= Exp5 "::"  Exp4 ;
+EInfixWeak.   Exp5 ::= Exp5 OIfxW Exp6 ;
+EInfixStrong. Exp6 ::= Exp6 OIfxS Exp7 ;
+EUnary.       Exp7 ::=      OUnr  Exp7 ;
+ENot.         Exp8 ::= "not" Exp10 ;
+EHead.        Exp8 ::= "hd"  Exp10 ;
+ETail.        Exp8 ::= "tl"  Exp10 ;
+EAppl.        Exp9 ::= Exp9 Exp10 ;
+EInt.         Exp10 ::= Integer ;
+EFloat.       Exp10 ::= OFloat ;
+ETrue.        Exp10 ::= "true" ;
+EFalse.       Exp10 ::= "false" ;
+EList.        Exp10 ::= "[" [ListElem] "]" ;
+EVar.         Exp11 ::= OIdent ;
+EExplType.    Exp12 ::= "(" Exp ":" Type ")" ;
+
+coercions Exp 12 ;
+
+terminator nonempty Argument "" ;
+FunArg.         Argument ::= OIdent ;
+FunArgExplType. Argument ::= "(" OIdent ":" Type ")" ;
+
+separator nonempty LocDecl "and" ;
+LocalVarDecl.         LocDecl ::= OIdent "=" Exp ;
+LocalVarDeclExplType. LocDecl ::= OIdent ":" Type "=" Exp ;
+LocalFunDecl.         LocDecl ::= OIdent [Argument] "=" Exp ;
+LocalFunDeclExplType. LocDecl ::= OIdent [Argument] ":" Type "=" Exp ;
+
+separator ListElem ";" ;
+ListElement. ListElem ::= Exp ;
+
+OEq.  OCmp ::= "=" ;
+ONeq. OCmp ::= "<>" ;
+OLt.  OCmp ::= "<" ;
+OLeq. OCmp ::= "<=" ;
+OGt.  OCmp ::= ">" ;
+OGeq. OCmp ::= ">=" ;
+
+OAdd.    OIfxW ::= "+" ;
+OSub.    OIfxW ::= "-" ;
+OAddFlt. OIfxW ::= "+." ;
+OSubFlt. OIfxW ::= "-." ;
+
+OMul.    OIfxS ::= "*" ;
+ODiv.    OIfxS ::= "/" ;
+OMulFlt. OIfxS ::= "*." ;
+ODivFlt. OIfxS ::= "/." ;
+OMod.    OIfxS ::= "mod" ;
+
+ONeg.    OUnr ::= "-" ;
+OPos.    OUnr ::= "+" ;
+ONegFlt. OUnr ::= "-." ;
+OPosFlt. OUnr ::= "+." ;
+
+TFun.   Type  ::= Type1 "->" Type ;
+TList.  Type1 ::= Type1 "list" ;
+TInt.   Type2 ::= "int" ;
+TFloat. Type2 ::= "float" ;
+TBool.  Type2 ::= "bool" ;
+TPoly.  Type2 ::= OPolyIdent ;
+
+coercions Type 2 ;
+\documentclass[a4paper,11pt]{article}
+
+\usepackage[a4paper, margin=1.5cm]{geometry}
+
+\author{Jan Wr\'oblewski\\
+student no. 277632 of faculty of\\
+Mathematics, Informatics and Mechanics of University of Warsaw}
+
+\title{The Language Xilocaml}
+
+\setlength{\parindent}{0mm}
+\setlength{\parskip}{1mm}
+
+\usepackage{url}
+\usepackage{hyperref}
+
+\newcommand{\emptyP}{\mbox{$\epsilon$}}
+\newcommand{\terminal}[1]{\mbox{{\texttt {#1}}}}
+\newcommand{\nonterminal}[1]{\mbox{$\langle \mbox{{\sl #1 }} \! \rangle$}}
+\newcommand{\arrow}{\mbox{::=}}
+\newcommand{\delimit}{\mbox{$|$}}
+\newcommand{\reserved}[1]{\mbox{{\texttt {#1}}}}
+\newcommand{\literal}[1]{\mbox{{\texttt {#1}}}}
+\newcommand{\symb}[1]{\mbox{{\texttt {#1}}}}
+\newcommand{\code}[1]{\mbox{{\texttt {#1}}}}
+
+\begin{document}
+
+\maketitle
+\tableofcontents
+
+\section{Introduction}
+
+Xilocaml is a subset of OCaml 3.12. It has following features:
+\begin{itemize}
+	\item purely functional,
+	\item polymorphic lists,
+	\item strong static type system,
+	\item first-class function closures,
+	\item partial function applications,
+	\item type inference (automatic deduction of types) with optional type annotations,
+	\item lambda functions,
+	\item parametric polymorphism.
+\end{itemize}
+
+\section{The lexical structure of Xilocaml}
+
+\subsection{Literals}
+Integer literals \nonterminal{Int}\ are nonempty sequences of digits.
+
+OFloat literals are recognized by the regular expression
+\(({\nonterminal{digit}}+ \mbox{`.'} {\nonterminal{digit}}* \mid \mbox{`.'} {\nonterminal{digit}}+) ((\mbox{`e'} \mid \mbox{`E'}) (\mbox{`{$+$}'} \mid \mbox{`{$-$}'})? {\nonterminal{digit}}+)? \mid {\nonterminal{digit}}+ (\mbox{`e'} \mid \mbox{`E'}) \mbox{`{$-$}'}? {\nonterminal{digit}}+\)
+
+OIdent literals are recognized by the regular expression
+\({\nonterminal{lower}} ({\nonterminal{letter}} \mid {\nonterminal{digit}} \mid \mbox{`\_'} \mid \mbox{`''})*\)
+
+OPoliIdent literals are recognized by the regular expression
+\(\mbox{`''} ({\nonterminal{letter}} \mid {\nonterminal{digit}} \mid \mbox{`\_'} \mid \mbox{`''})*\)
+
+\subsection{Reserved words and symbols}
+The set of reserved words is the set of terminals appearing in the grammar. Those reserved words that consist of non-letter characters are called symbols, and they are treated in a different way from those that are similar to identifiers. The lexer follows rules familiar from languages like Haskell, C, and Java, including longest match and spacing conventions.
+
+The reserved words used in Xilocaml are the following: \\
+
+\begin{tabular}{lll}
+{\reserved{List}} &{\reserved{and}} &{\reserved{bool}} \\
+{\reserved{else}} &{\reserved{false}} &{\reserved{float}} \\
+{\reserved{fun}} &{\reserved{hd}} &{\reserved{if}} \\
+{\reserved{in}} &{\reserved{int}} &{\reserved{let}} \\
+{\reserved{list}} &{\reserved{mod}} &{\reserved{not}} \\
+{\reserved{open}} &{\reserved{rec}} &{\reserved{then}} \\
+{\reserved{tl}} &{\reserved{true}} & \\
+\end{tabular}\\
+
+The symbols used in Xilocaml are the following: \\
+
+\begin{tabular}{lll}
+{\symb{;;}} &{\symb{{$-$}{$>$}}} &{\symb{{$|$}{$|$}}} \\
+{\symb{\&\&}} &{\symb{::}} &{\symb{[}} \\
+{\symb{]}} &{\symb{(}} &{\symb{:}} \\
+{\symb{)}} &{\symb{{$=$}}} &{\symb{;}} \\
+{\symb{{$<$}{$>$}}} &{\symb{{$<$}}} &{\symb{{$<$}{$=$}}} \\
+{\symb{{$>$}}} &{\symb{{$>$}{$=$}}} &{\symb{{$+$}}} \\
+{\symb{{$-$}}} &{\symb{{$+$}.}} &{\symb{{$-$}.}} \\
+{\symb{*}} &{\symb{/}} &{\symb{*.}} \\
+{\symb{/.}} & & \\
+\end{tabular}\\
+
+\subsection{Comments}
+There are no single-line comments in the grammar. \\Multiple-line comments are  enclosed with {\symb{(*}} and {\symb{*)}}. Unlike in OCaml, nested comments are not allowed.
+
+\section{The syntactic structure of Xilocaml}
+Non-terminals are enclosed between $\langle$ and $\rangle$. 
+The symbols  {\arrow}  (production),  {\delimit}  (union) 
+and {\emptyP} (empty rule) belong to the BNF notation. 
+All other symbols are terminals.\\
+
+\begin{tabular}{lll}
+{\nonterminal{Program}} & {\arrow}  &{\nonterminal{ComBeg}} {\nonterminal{Exp}} {\nonterminal{ComEnd}}  \\
+\end{tabular}\\
+
+\begin{tabular}{lll}
+{\nonterminal{ComBeg}} & {\arrow}  &{\terminal{open}} {\terminal{List}} {\terminal{;;}}  \\
+ & {\delimit}  &{\emptyP} \\
+\end{tabular}\\
+
+\begin{tabular}{lll}
+{\nonterminal{ComEnd}} & {\arrow}  &{\terminal{;;}}  \\
+ & {\delimit}  &{\emptyP} \\
+\end{tabular}\\
+
+\begin{tabular}{lll}
+{\nonterminal{Exp}} & {\arrow}  &{\terminal{let}} {\nonterminal{ListLocDecl}} {\terminal{in}} {\nonterminal{Exp}}  \\
+ & {\delimit}  &{\terminal{let}} {\terminal{rec}} {\nonterminal{ListLocDecl}} {\terminal{in}} {\nonterminal{Exp}}  \\
+ & {\delimit}  &{\terminal{fun}} {\nonterminal{ListArgument}} {\terminal{{$-$}{$>$}}} {\nonterminal{Exp}}  \\
+ & {\delimit}  &{\terminal{if}} {\nonterminal{Exp}} {\terminal{then}} {\nonterminal{Exp}} {\terminal{else}} {\nonterminal{Exp}}  \\
+ & {\delimit}  &{\nonterminal{Exp1}}  \\
+\end{tabular}\\
+
+\begin{tabular}{lll}
+{\nonterminal{Exp1}} & {\arrow}  &{\nonterminal{Exp1}} {\terminal{{$|$}{$|$}}} {\nonterminal{Exp2}}  \\
+ & {\delimit}  &{\nonterminal{Exp2}}  \\
+\end{tabular}\\
+
+\begin{tabular}{lll}
+{\nonterminal{Exp2}} & {\arrow}  &{\nonterminal{Exp2}} {\terminal{\&\&}} {\nonterminal{Exp3}}  \\
+ & {\delimit}  &{\nonterminal{Exp3}}  \\
+\end{tabular}\\
+
+\begin{tabular}{lll}
+{\nonterminal{Exp3}} & {\arrow}  &{\nonterminal{Exp3}} {\nonterminal{OCmp}} {\nonterminal{Exp4}}  \\
+ & {\delimit}  &{\nonterminal{Exp4}}  \\
+\end{tabular}\\
+
+\begin{tabular}{lll}
+{\nonterminal{Exp4}} & {\arrow}  &{\nonterminal{Exp5}} {\terminal{::}} {\nonterminal{Exp4}}  \\
+ & {\delimit}  &{\nonterminal{Exp5}}  \\
+\end{tabular}\\
+
+\begin{tabular}{lll}
+{\nonterminal{Exp5}} & {\arrow}  &{\nonterminal{Exp5}} {\nonterminal{OIfxW}} {\nonterminal{Exp6}}  \\
+ & {\delimit}  &{\nonterminal{Exp6}}  \\
+\end{tabular}\\
+
+\begin{tabular}{lll}
+{\nonterminal{Exp6}} & {\arrow}  &{\nonterminal{Exp6}} {\nonterminal{OIfxS}} {\nonterminal{Exp7}}  \\
+ & {\delimit}  &{\nonterminal{Exp7}}  \\
+\end{tabular}\\
+
+\begin{tabular}{lll}
+{\nonterminal{Exp7}} & {\arrow}  &{\nonterminal{OUnr}} {\nonterminal{Exp7}}  \\
+ & {\delimit}  &{\nonterminal{Exp8}}  \\
+\end{tabular}\\
+
+\begin{tabular}{lll}
+{\nonterminal{Exp8}} & {\arrow}  &{\terminal{not}} {\nonterminal{Exp10}}  \\
+ & {\delimit}  &{\terminal{hd}} {\nonterminal{Exp10}}  \\
+ & {\delimit}  &{\terminal{tl}} {\nonterminal{Exp10}}  \\
+ & {\delimit}  &{\nonterminal{Exp9}}  \\
+\end{tabular}\\
+
+\begin{tabular}{lll}
+{\nonterminal{Exp9}} & {\arrow}  &{\nonterminal{Exp9}} {\nonterminal{Exp10}}  \\
+ & {\delimit}  &{\nonterminal{Exp10}}  \\
+\end{tabular}\\
+
+\begin{tabular}{lll}
+{\nonterminal{Exp10}} & {\arrow}  &{\nonterminal{Integer}}  \\
+ & {\delimit}  &{\nonterminal{OFloat}}  \\
+ & {\delimit}  &{\terminal{true}}  \\
+ & {\delimit}  &{\terminal{false}}  \\
+ & {\delimit}  &{\terminal{[}} {\nonterminal{ListListElem}} {\terminal{]}}  \\
+ & {\delimit}  &{\nonterminal{Exp11}}  \\
+\end{tabular}\\
+
+\begin{tabular}{lll}
+{\nonterminal{Exp11}} & {\arrow}  &{\nonterminal{OIdent}}  \\
+ & {\delimit}  &{\nonterminal{Exp12}}  \\
+\end{tabular}\\
+
+\begin{tabular}{lll}
+{\nonterminal{Exp12}} & {\arrow}  &{\terminal{(}} {\nonterminal{Exp}} {\terminal{:}} {\nonterminal{Type}} {\terminal{)}}  \\
+ & {\delimit}  &{\terminal{(}} {\nonterminal{Exp}} {\terminal{)}}  \\
+\end{tabular}\\
+
+\begin{tabular}{lll}
+{\nonterminal{ListArgument}} & {\arrow}  &{\nonterminal{Argument}}  \\
+ & {\delimit}  &{\nonterminal{Argument}} {\nonterminal{ListArgument}}  \\
+\end{tabular}\\
+
+\begin{tabular}{lll}
+{\nonterminal{Argument}} & {\arrow}  &{\nonterminal{OIdent}}  \\
+ & {\delimit}  &{\terminal{(}} {\nonterminal{OIdent}} {\terminal{:}} {\nonterminal{Type}} {\terminal{)}}  \\
+\end{tabular}\\
+
+\begin{tabular}{lll}
+{\nonterminal{ListLocDecl}} & {\arrow}  &{\nonterminal{LocDecl}}  \\
+ & {\delimit}  &{\nonterminal{LocDecl}} {\terminal{and}} {\nonterminal{ListLocDecl}}  \\
+\end{tabular}\\
+
+\begin{tabular}{lll}
+{\nonterminal{LocDecl}} & {\arrow}  &{\nonterminal{OIdent}} {\terminal{{$=$}}} {\nonterminal{Exp}}  \\
+ & {\delimit}  &{\nonterminal{OIdent}} {\terminal{:}} {\nonterminal{Type}} {\terminal{{$=$}}} {\nonterminal{Exp}}  \\
+ & {\delimit}  &{\nonterminal{OIdent}} {\nonterminal{ListArgument}} {\terminal{{$=$}}} {\nonterminal{Exp}}  \\
+ & {\delimit}  &{\nonterminal{OIdent}} {\nonterminal{ListArgument}} {\terminal{:}} {\nonterminal{Type}} {\terminal{{$=$}}} {\nonterminal{Exp}}  \\
+\end{tabular}\\
+
+\begin{tabular}{lll}
+{\nonterminal{ListListElem}} & {\arrow}  &{\emptyP} \\
+ & {\delimit}  &{\nonterminal{ListElem}}  \\
+ & {\delimit}  &{\nonterminal{ListElem}} {\terminal{;}} {\nonterminal{ListListElem}}  \\
+\end{tabular}\\
+
+\begin{tabular}{lll}
+{\nonterminal{ListElem}} & {\arrow}  &{\nonterminal{Exp}}  \\
+\end{tabular}\\
+
+\begin{tabular}{lll}
+{\nonterminal{OCmp}} & {\arrow}  &{\terminal{{$=$}}}  \\
+ & {\delimit}  &{\terminal{{$<$}{$>$}}}  \\
+ & {\delimit}  &{\terminal{{$<$}}}  \\
+ & {\delimit}  &{\terminal{{$<$}{$=$}}}  \\
+ & {\delimit}  &{\terminal{{$>$}}}  \\
+ & {\delimit}  &{\terminal{{$>$}{$=$}}}  \\
+\end{tabular}\\
+
+\begin{tabular}{lll}
+{\nonterminal{OIfxW}} & {\arrow}  &{\terminal{{$+$}}}  \\
+ & {\delimit}  &{\terminal{{$-$}}}  \\
+ & {\delimit}  &{\terminal{{$+$}.}}  \\
+ & {\delimit}  &{\terminal{{$-$}.}}  \\
+\end{tabular}\\
+
+\begin{tabular}{lll}
+{\nonterminal{OIfxS}} & {\arrow}  &{\terminal{*}}  \\
+ & {\delimit}  &{\terminal{/}}  \\
+ & {\delimit}  &{\terminal{*.}}  \\
+ & {\delimit}  &{\terminal{/.}}  \\
+ & {\delimit}  &{\terminal{mod}}  \\
+\end{tabular}\\
+
+\begin{tabular}{lll}
+{\nonterminal{OUnr}} & {\arrow}  &{\terminal{{$-$}}}  \\
+ & {\delimit}  &{\terminal{{$+$}}}  \\
+ & {\delimit}  &{\terminal{{$-$}.}}  \\
+ & {\delimit}  &{\terminal{{$+$}.}}  \\
+\end{tabular}\\
+
+\begin{tabular}{lll}
+{\nonterminal{Type}} & {\arrow}  &{\nonterminal{Type1}} {\terminal{{$-$}{$>$}}} {\nonterminal{Type}}  \\
+ & {\delimit}  &{\nonterminal{Type1}}  \\
+\end{tabular}\\
+
+\begin{tabular}{lll}
+{\nonterminal{Type1}} & {\arrow}  &{\nonterminal{Type1}} {\terminal{list}}  \\
+ & {\delimit}  &{\nonterminal{Type2}}  \\
+\end{tabular}\\
+
+\begin{tabular}{lll}
+{\nonterminal{Type2}} & {\arrow}  &{\terminal{int}}  \\
+ & {\delimit}  &{\terminal{float}}  \\
+ & {\delimit}  &{\terminal{bool}}  \\
+ & {\delimit}  &{\nonterminal{OPolyIdent}}  \\
+ & {\delimit}  &{\terminal{(}} {\nonterminal{Type}} {\terminal{)}}  \\
+\end{tabular}\\
+
+
+\section{Semantics of Xilocaml}
+
+Xilocaml is a subset of OCaml 3.12. with very little changes. All syntactically valid constructions not described below have the same meaning as in language OCaml 3.12. For description of OCaml semantics, see \cite{ocaml}.
+
+\subsection{Arithmetics}
+There are two types of numerical values in Xilocaml on which arithmetic operations may be performed:
+\begin{itemize}
+	\item {\reserved{int}} - integers of arbitrary precision (which differs from OCaml);
+	\item {\reserved{float}} - floating-point numbers of double precision, following standard IEEE-754 (same as in OCaml).
+\end{itemize}
+
+Floating-point operations have the same meaning as in OCaml and integer operations are performed on arbitrary precision integers. For compatibility to OCaml 3.12 implementation, sequence of unary prefix operators {\symb{+}}, {\symb{-}}, {\symb{+.}}, {\symb{-.}} applied to a floating-point constant is allowed and has the standard meaning.
+
+\subsection{Type inference}
+Type inference in Xilocaml behave the same way as in OCaml (without enabled recursive types). If Xilocaml will be unable to detect the type of a value, a semantics error will occur. Xilocaml should be able to deduct types of all its constructions that implementation of OCaml 3.12. is able to.
+
+\subsection{\reserved{let rec}}
+Behaviour of {\reserved{let rec}} in Xilocaml differs from OCaml. In the following construction:
+\begin{verbatim}
+let rec pattern_1 = expr_1 and ... and pattern_n = expr_n in expr
+\end{verbatim}
+binding of names is performed like described below:
+\begin{itemize}
+	\item If {\code{pattern\_i}} is a function definition ({\code{fun\_name arg1\_name arg2\_name ...}}) with at least one argument name, binding of names in {\code{expr\_i}} is the binding of names as in nonrecursive {\reserved{let}} local definition updated by names of variables and functions defined in {\code{pattern\_1 = expr\_1}}, ..., {\code{pattern\_n = expr\_n}};
+	\item Otherwise, biding of names in {\code{expr\_i}} is the same as in nonrecursive {\reserved{let}} local definition.
+\end{itemize}
+
+Type inference in {\reserved{let rec}} local definition behaves the same way as in OCaml.
+
+
+\section{Xilocaml interpreter}
+
+\subsection{Usage}
+Xilocaml interpreter takes as an input a Xilocaml program and writes on standard output computed value and its type. If the computed value is a function, {\code{<fun>}} is written instead with its type. A Xilocaml program consists of a single expression and might be prepended by {\code{open List;;}} or/and appended by {\code{;;}}, for compatibility to OCaml interpreter. That way, input of Xilocaml interpreter may be written in a way to be valid both in Xilocaml and OCaml interpreter and even give the same output (that is, printing out the same value and its type).
+
+\subsection{Errors}
+If an error occurs, it is written on standard error output with its description and nothing is written on standard output. There are different types of errors:
+\begin{itemize}
+	\item syntactic,
+	\item semantic,
+	\item runtime.
+\end{itemize}
+
+Syntactic error will occur if input isn't conforming to Xilocaml grammar. Xilocaml's internals processing the syntactic part of input are based on Haskell libraries Alex and Happy. In some cases, an internal error of those libraries was observed and is written on standard error output the same way as other errors (for example it was observed for an empty or {\code{1+}} input).
+
+Semantic error will occur if input's semantics are incorrect. In most cases that means a type error, when unification of given and expected type failed.
+
+Runtime error might occur in the following cases:
+\begin{itemize}
+	\item division of integer by zero,
+	\item taking head or tail of an empty list,
+	\item comparing functional values (it might not be detected as a semantic error when functional values are passed to a polymorphic function).
+\end{itemize}
+
+
+\begin{thebibliography}{99}
+\addcontentsline{toc}{section}{Bibliography}
+
+\bibitem[OCaml]{ocaml} The OCaml Language. \url{http://caml.inria.fr/pub/docs/manual-ocaml/language.html}
+
+\end{thebibliography}
+
+\end{document}

examples/arithmetic.ml

+1 - 1 - 1 + 11 + 2 * 4 / 2 * 8 + 6 / 3 mod 2;; (* = 42 *)

examples/factorial.ml

+let rec factorial n =
+    if n <= 1 then
+        1
+    else
+        n * factorial (n-1)
+in factorial 6;;

examples/factorization.ml

+let factorization n =
+    let rec fact n div acc =
+        if n mod div = 0 then
+            fact (n / div) div (div::acc)
+        else if n < div then
+            acc
+        else
+            fact n (div + 1) acc
+    in fact n 2 []
+in factorization 48;;

examples/fold_left.ml

+open List;;
+
+let rec fold_left (f : 'a -> 'b -> 'a) (acc : 'a) (t : 'b list) : 'a =
+    if t = [] then
+        acc
+    else
+        fold_left f (f acc (hd t)) (tl t)
+in fold_left (fun acc e -> acc + e) 0 [1;2;3;4;5];; (* sum of 1..5 *)

examples/identity.ml

+let f x = x in f;;

examples/unary.ml

+- -. - + +. + + - - -. - 1.0;;
+#!/bin/bash
+cd Grammar
+make distclean
+cp ../Xilocaml.cf .
+bnfc -m -haskell Xilocaml.cf
+make