implementation module Sil.Check

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

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

import Sil.Error
import Sil.Syntax
import Sil.Types
import Sil.Util.Parser

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

	checkFunctionNames :: Program -> [Error]
	checkFunctionNames p =
		[ Ck_DuplicateFunctionName (errpos $ hd fs) (hd fs).f_name
		\\ fs <- tails [f \\ f <- p.p_funs]
		| let names = [f.f_name \\ f <- fs]
		  in  not (isEmpty names) && isMember (hd names) (tl names)]

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

checkFunction :: *(? *File) Function -> *([Error], * ? *File)
checkFunction err f = checkErrors
	[ checkLocals
	, checkReturnAndVoid
	, checkMainFunctionType
	] f
	$ noErrors err
where
	checkReturnAndVoid :: Function -> [Error]
	checkReturnAndVoid f = case f.f_type of
		TVoid -> [Ck_ReturnExpressionFromVoid (errpos st) f.f_name \\ st=:(Return _ (?Just _)) <- allStatements f]
		_     -> if (sureToReturn f.f_code) [] [Ck_NoReturnFromNonVoid (errpos f) 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 ?None     -> all (sureToReturn o snd) bs
				MachineStm _ _    -> True // Let's assume the user is not stupid
				_                 -> False

	checkMainFunctionType :: Function -> [Error]
	checkMainFunctionType {f_name="main",f_args=[]}
		= []
	checkMainFunctionType f=:{f_name="main"}
		= [Ck_MainFunctionInvalidType (errpos f) $ fromOk $ fromJust $ type zero f]
	checkMainFunctionType _
		= []

	checkLocals :: Function -> [Error]
	checkLocals f =
		checkDupName [a.arg_name \\ a <- f.f_args] f.f_code ++
		concatMap checkVoid (allLocals f)
	where
		checkDupName :: [Name] CodeBlock -> [Error]
		checkDupName defined cb =
			[Ck_DuplicateLocalName (errpos f) 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 ?None)     = map snd bs
			findCBs (While _ _ cb)      = [cb]
			findCBs (MachineStm _ _)    = []

		checkVoid :: (Type, Name) -> [Error]
		checkVoid (TVoid, n) = [Ck_LocalVoid (errpos f) n]
		checkVoid _          = []

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

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

noErrors :: *(? *File) -> *([Error], * ? *File)
noErrors f = ([], f)

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