implementation module Sil.Check

import StdBool
import StdFile
from StdFunc import flip, o
import StdList
import StdOverloaded
import StdString
import StdTuple

import Data.Error
from Data.Func import $, mapSt, seqSt
import Data.List
import Data.Maybe
import Data.Tuple
from Text import <+

import Sil.Syntax
import Sil.Types

instance toString CheckError
where
	toString NoMainFunction
		= "Error: no main function."
	toString (MainFunctionInvalidType t)
		= "Error: function 'main' should not have arguments has type " <+ t <+ "."
	toString (DuplicateFunctionName n)
		= "Error: multiply defined: '" <+ n <+ "'."
	toString (DuplicateLocalName f arg)
		= "Error: multiply defined: '" <+ arg <+ "' in '" <+ f <+ "'."
	toString (ReturnExpressionFromVoid f)
		= "Type error: an expression was returned from void function '" <+ f <+ "'."
	toString (NoReturnFromNonVoid f)
		= "Type error: no return from non-void function '" <+ f <+ "'."
	toString (LocalVoid f l)
		= "Type error: local variable '" <+ l <+ "' in '" <+ f <+ "' cannot have type Void."
	toString (BasicGlobal g)
		= "Error: global variable '" <+ g <+ "' cannot have a basic type."

instance <<< CheckError where <<< f e = f <<< toString e <<< "\r\n"

checkProgram :: *(Maybe *File) Program -> *([CheckError], *Maybe *File)
checkProgram err prog
	= checkErrors
	[ checkFunctionNames
	, checkMainFunction
	, checkGlobals
	] prog
	$ appFst flatten $ mapSt (flip checkFunction) prog.p_funs err
where
	checkMainFunction :: Program -> [CheckError]
	checkMainFunction p = case [f \\ f <- p.p_funs | f.f_name == "main"] of
		[] -> [NoMainFunction]
		_  -> []

	checkFunctionNames :: Program -> [CheckError]
	checkFunctionNames p =
		[ DuplicateFunctionName $ hd fs
		\\ fs <- tails [f.f_name \\ f <- p.p_funs]
		| not (isEmpty fs) && isMember (hd fs) (tl fs)]

	checkGlobals :: Program -> [CheckError]
	checkGlobals p =
		[ BasicGlobal g.init_name
		\\ g <- p.p_globals
		| (typeSize g.init_type).bsize <> 0]

checkFunction :: *(Maybe *File) Function -> *([CheckError], *Maybe *File)
checkFunction err f = checkErrors
	[ checkLocals
	, checkReturnAndVoid
	, checkMainFunctionType
	] f
	$ noErrors err
where
	checkReturnAndVoid :: Function -> [CheckError]
	checkReturnAndVoid f = case f.f_type of
		TVoid -> case [st \\ st=:(Return (Just _)) <- allStatements f] of
			[] -> []
			_  -> [ReturnExpressionFromVoid f.f_name]
		_     -> if (sureToReturn f.f_code) [] [NoReturnFromNonVoid f.f_name]
	where
		sureToReturn :: CodeBlock -> Bool
		sureToReturn cb = case cb.cb_content of
			[]  -> False
			sts -> case last sts of
				Return _       -> True
				While _ cb`    -> sureToReturn cb`
				If bs (Just e) -> all sureToReturn [e:map snd bs]
				If bs Nothing  -> all (sureToReturn o snd) bs
				MachineStm _   -> True // Let's assume the user is not stupid
				_              -> False

	checkMainFunctionType :: Function -> [CheckError]
	checkMainFunctionType f=:{f_name="main",f_args=[]} = []
	checkMainFunctionType f=:{f_name="main"} = [MainFunctionInvalidType $ fromOk $ fromJust $ type zero f]
	checkMainFunctionType _ = []

	checkLocals :: Function -> [CheckError]
	checkLocals f =
		checkDupName [a.arg_name \\ a <- f.f_args] f.f_code ++
		concatMap checkVoid (allLocals f)
	where
		checkDupName :: [Name] CodeBlock -> [CheckError]
		checkDupName defined cb =
			[DuplicateLocalName f.f_name l \\ l <- defined | isMember l locals] ++
			concatMap (checkDupName (locals ++ defined)) (underlyingCBs cb)
		where locals = [i.init_name \\ i <- cb.cb_init]

		underlyingCBs :: CodeBlock -> [CodeBlock]
		underlyingCBs cb = concatMap findCBs cb.cb_content
		where
			findCBs (Declaration _ _) = []
			findCBs (Application _)   = []
			findCBs (Return _)        = []
			findCBs (If bs (Just e))  = [e:map snd bs]
			findCBs (If bs Nothing)   = map snd bs
			findCBs (While _ cb)      = [cb]
			findCBs (MachineStm _)    = []

		checkVoid :: (Type, Name) -> [CheckError]
		checkVoid (TVoid, n) = [LocalVoid f.f_name n]
		checkVoid _          = []

checkErrors :: [(a -> [CheckError])] a *([CheckError], Maybe *File) -> *([CheckError], *Maybe *File)
checkErrors cks x st = seqSt error (concatMap (flip ($) x) cks) st

error :: CheckError *([CheckError], *Maybe *File) -> *([CheckError], *Maybe *File)
error e (es, err) = ([e:es], err <?< e)

noErrors :: *(Maybe *File) -> *([CheckError], *Maybe *File)
noErrors f = ([], f)

(<?<) infixl :: !*(Maybe *File) !a -> *Maybe *File | <<< a
(<?<) (Just f) x = Just (f <<< x)
(<?<) Nothing  _ = Nothing