module Type.Error
(
	Error(..)
)

where

-----
import Util

-----
import qualified Shared.Var	as Var
import qualified Shared.VarUtil	as Var
import Shared.Literal
import Shared.Error
import Shared.Base		(SourcePos(..))

import Type.Exp
import Type.Pretty

-- import Type.Util

-----
stage	= "Type.Error"

-----
data Error
	-- Used for debugging
	= ErrorBadness
		{ eMessage	:: String }

	-- Constructor airity
	| ErrorCtorAirity				-- Wrong number of arguments to constructor
		{ eCtorVar		:: Var		--	in pattern match.
		, eCtorAirity		:: Int
		, ePatternAirity 	:: Int }

	-- Constructor mismatch.
	| ErrorUnifyCtorMismatch			-- Type constructors don't match.
		{ eCtor1	:: Type
		, eTypeSource1	:: TypeSource

		, eCtor2	:: Type 
		, eTypeSource2	:: TypeSource }

	-- Infinite types.
	| ErrorInfiniteTypeClassId			-- Cannot construct infinite type through this ClassId
		{ eClassId	:: ClassId }		-- 	This error generated by Type.Squid.Sink when it
							--	tries to enter a class it's seen before.
							--
							--	It should get converted to an ErrorInfiniteTypeGen, which
							--	is more informative.

	| ErrorInfiniteTypeGen				-- Cannot construct inifinite type during generalisation.
		{ eGenVar	:: Var			-- 	The variable that was being generalised.
		, eClassIds	:: [ClassId]		--	The classIds which we tried to re-enter.
		, eType		:: Type			--	The type, up to the bad variables.
		, eLoops	:: [(Var, Type)] }	--	The recurrances found.


	-- Signature mismatch.
	| ErrorSigScheme				-- An inferred type scheme does not match a type signature
		{ eSig		:: (Var, Type)		-- 	typeVar, type
		, eScheme	:: (Var, Type)		-- 	
		, eClashSig	:: Type			--	Offending type from signature.
		, eClashScheme	:: Type }		-- 	Offending type from scheme.

	| ErrorSigEffects
		{ eSig		:: (Var, Type)		-- Some function in the signature is more/less effectful than
		, eScheme	:: (Var, Type)		--	the corresponding function in the scheme
		, eEffSig	:: [Effect]
		, eEffScheme	:: [Effect] }
		
	| ErrorSigForall				-- Inferred type is is not quantified the same a signature.
		{ eSig		:: (Var, Type)		--	
		, eScheme	:: (Var, Type) 		--
		, eErrVar	:: Var }		--	Offending variable.

	-- Type class problems
	| ErrorNoInstance				-- There is no instance for the class at these arguments.
		{ eClassVar	:: Var
		, eTypeArgs	:: [Type] }		
		
	-- Field projection problems.
	| ErrorNoProjections				-- This type has no projections defined for it.
		{ eProj		:: TProj
		, eConstructor	:: Type }		

	| ErrorFieldNotPresent				-- Some field is not a member of this type.
		{ eProj		:: TProj		-- 	Requested projection.
		, eConstructor	:: Type 		-- 	Offending type.
		, eFields	:: [Var] }		--	Possible fields

	| ErrorAmbiguousProjection			-- Tried to project a field from a type variable.
		{ eProj		:: TProj }		-- 	

	-- Purity problems
	| ErrorCannotPurify				-- Cannot purify top-level or write effects.
		{ eEffect	:: Effect		--	The effect we can't purify.
		, eEffectSource	:: TypeSource
		, eFetter	:: Fetter		--	The Pure fetter we were trying to satisfy.
		, eFetterSource	:: TypeSource }

	-- Mutability conflicts.
	| ErrorConstWrite				-- Attempted write to a const region.
		{ eFetter	:: Fetter		--	Const fetter.
		, eFetterSource	:: TypeSource		-- 	Source of Const fetter.
		
		, eEffect	:: Effect		--	Write effect.
		, eEffectSource	:: TypeSource }		-- 	Source of Write effect.
	
	| ErrorPureReadWrite
		{ eReadEff	:: Effect
		, eReadSource	:: TypeSource
		, ePureFetter	:: Fetter
		, ePureSource	:: TypeSource
		, eWriteEff	:: Effect
		, eWriteSource	:: TypeSource }
		
	-- Update soundness problems.
	| ErrorUpdateSoundness				-- Update soundness problem 
		{ eErrVar	:: Var
		, eType		:: Type			--	The offending scheme.
		, eTypeDanger	:: [Type] }		--	The dangerous var(s) which are causing the problem.

	-- Inference screw-ups.
	| ErrorLateConstraint				-- Found out about a mutability constraint too late.
		{ eScheme	:: (Var, Type)		-- 	The scheme we've been using.
		, eRegen	:: Type }		-- 	The scheme we should have used.
		
		
	deriving (Show)

-----	
instance Pretty Error where

 -- Random badness.
 ppr err@(ErrorBadness
 		{ eMessage	= s })
		
	= "    Badness: " % s % "\n"

 -- Constructor Airity.
 ppr err@(ErrorCtorAirity{})
 	= Var.prettyPos (eCtorVar err) % "\n"
	% "    Wrong number of arguments for constructor match.\n"
	% "         constructor: " % eCtorVar err 				% "\n"
	% "          defined at: " % Var.prettyPosBound (eCtorVar err)		% "\n"
	% "                 has: " % eCtorAirity err % " arguments, but has been used here with " % ePatternAirity err % ".\n"


 -- Constructor mismatch.
 ppr err@(ErrorUnifyCtorMismatch 
 		{ eCtor1 	= t1
		, eTypeSource1	= ts1
		, eCtor2 	= t2 
		, eTypeSource2	= ts2})
 	= (getTSP $ selectSourceTS [ts1, ts2])				% "\n"
	% "    Type mismatch during unification.\n"
	% "          cannot match: " % t1				% "\n"
	% "                  with: " % t2				% "\n"
	% "\n"
	% prettyTypeConflict t1 ts1 				
	% "\n"
	% "        conflicts with, " 					% "\n"
	% prettyTypeConflict t2 ts2					
	% "\n"	

 -- Infinite types.
 ppr err@(ErrorInfiniteTypeClassId
 		{ eClassId	= cid })
	= "    Cannot construct infinite type.\n"			
	% "    (through node " % cid % " in the type graph)" 		% "\n"
	 
 -- Signature mismatch.
 ppr err@(ErrorSigScheme{})
	= prettyValuePos (fst $ eScheme err)				% "\n"
	% "    Inferred type for '" 
				% (ppr $ fst $ eScheme err) 
				% "' does not match signature." 	% "\n"
	% "\n"
	% "        in the type of: " % (fst $ eScheme err)		% "\n"
	% "          cannot match: " % eClashScheme  err		% "\n"
	% "                  with: " % eClashSig     err		% "\n"
	% "\n"
	% "         inferred type: " % prettyVTS (eScheme err)		% "\n"
	% "\n"
	% "        type signature: " % prettyVTS (eSig    err) 		% "\n"

 ppr err@(ErrorSigEffects{})
	= prettyValuePos (fst $ eScheme err)				% "\n"
	% "    Inferred type for '" 
				% (ppr $ fst $ eScheme err) 
				% "' has different effects than signature.\n"
	% "\n"
	% "        in the type of: " % (fst $ eScheme err)		% "\n"
	% "          cannot match: " % eEffScheme err			% "\n"
	% "                  with: " % eEffSig err			% "\n"
	% "\n"
	% "         inferred type: " % prettyVTS (eScheme err)		% "\n"
	% "\n"
	% "        type signature: " % prettyVTS (eSig err)		% "\n"
					
 ppr err@(ErrorSigForall{})
	= prettyValuePos (fst $ eScheme err)				% "\n"
	% "    Inferred type for '" 
				% (ppr $ fst $ eScheme err)
				% "' is not quantified the same as signature.\n"
	% "\n"
	% "       offending var: " % eErrVar err			% "\n"
	% "\n"
	% "       inferred type: " % prettyVTS (eScheme err)		% "\n"
	% "\n"
	% "      type signature: " % prettyVTS (eSig err)		% "\n"
	
 -- Type class problems.
 ppr err@(ErrorNoInstance
 		{ eClassVar	= v
		, eTypeArgs	= ts })
	= "    No instance for " % v % " " % " " %!% map prettyTS ts % "\n"
	
 -- Field projection problems.
 ppr err@(ErrorNoProjections
 		{ eProj		= p
		, eConstructor	= t })
	= (getProjSP p)		% "\n"
	% "    Type '" % t	% "' has no projections defined for it.\n"


 ppr err@(ErrorFieldNotPresent 
 		{ eProj		= p
		, eConstructor	= TData v _
		, eFields	= fields })
	= (getProjSP p)							% "\n"
	% "    Type '" % v 	% "' has no field named '" % p		% "'\n"
	% "      possible fields: " % "\n" %!% fields			% "\n"

	
 ppr err@(ErrorAmbiguousProjection
 		{ eProj		= p })
	= (getProjSP p)							% "\n"
	% "    Ambiguous projection: " % p 				% "\n"
	

 -- Purity problems.
 ppr err@(ErrorCannotPurify
 		{ eEffect	= e
		, eEffectSource	= eSource
		, eFetter	= f
		, eFetterSource	= fSource })
		
	= (getTSP eSource)						% "\n" 
	% "    Cannot purify effect `" % e % "'.\n"
	% prettyETS e eSource
	% "\n"
	% "     conflicts with,\n"
	% prettyFTS f fSource


 -- Mutability problems.
 ppr err@(ErrorConstWrite 
 		{ eEffect	= e
		, eEffectSource	= eSource
		, eFetter	= f
		, eFetterSource	= fSource })
	
	= (getTSP eSource)						% "\n"
	% "    Cannot write to Const region.\n"
	% prettyETS e eSource
	% "\n"
	% "     conflicts with,\n"
	% prettyFTS f fSource
	

 ppr err@(ErrorPureReadWrite
		{ eReadEff	= r
		, eReadSource	= rTS
		, ePureFetter	= p
		, ePureSource	= pTS
		, eWriteEff	= w
		, eWriteSource	= wTS })

	= getTSP wTS							% "\n"
	% "    Cannot write to Const region.\n"
	% "      This region is being forced Const because there is a\n"
	% "      purity constraint on a Read effect which accesses it.\n"
	% "\n"
	% prettyETS w wTS
	% "\n"
	% "          conflicts with,\n"
	% prettyETS r rTS
	% "\n"
	% "          which is being purified by,\n"
	% prettyFTS p pTS


 -- Update soundness problems.
 ppr err@(ErrorUpdateSoundness
 		{ eErrVar	= v
		, eType 	= t
		, eTypeDanger	= tDanger })
		
	= prettyValuePos v				% "\n"
	% "    Update soundess problem in scheme for `" % v % "'.\n"
	% prettyVTS (v, t)
	% "\n\n"
	% "        dangerous vars: " % tDanger	% "\n"


 -- Inference screw-ups.
 ppr err@(ErrorLateConstraint
 		{ eScheme	= (v, scheme)
		, eRegen	= regen })
		
	= prettyValuePos v				% "\n"
	% "    The type inference algorithm made an incorrect assumption\n"
	% "        about the mutability of `" % v % "'.\n"
	% "                   (and backtracking isn't implemented yet).\n"
	% "\n"
	% "        scheme we've been using:"
	% prettyVTS (v, scheme)
	% "\n\n"
	% "        scheme we should have used:"
	% prettyVTS (v, regen)
	% "\n\n"
	% "    Please add a type signature for `" % v % "' which provides\n"
	% "        the mutability constraints present in the second scheme.\n"
	% "\n\n"



-----
prettyVTS (v, t)
 	= indent 12 (
		"\n" ++ (Var.name v) ++ "\n  :: "
		++ (indent 2 $ pprStr $ prettyTypeSplit $ t))

prettyValuePos var
	= fromMaybe "?"
	$ liftM (Var.prettyPos)
	$ liftM (\(Var.IValueVar v) -> v)
	$ find  (=@= Var.IValueVar{}) 
	$ Var.info var


-----
-- selectSourceTS
--	Select from a set of possible TypeSource's
--	to find a good representative to report as the
--	main cause of an error.
--
selectSourceTS :: [TypeSource] -> TypeSource
selectSourceTS []
	= panic stage 
	$ "selectSourceTS: no suitable source pos"

selectSourceTS (t : ts)
 = case t of
 	TSIfObj{}	-> selectSourceTS ts
	_		-> t

	

-----
-- prettyTypeConflict
--
prettyTypeConflict :: Type -> TypeSource -> PrettyP	    
prettyTypeConflict t ts
 = case ts of
 	TSLiteral _ (CConst lit)
	 -> "         literal value: " % lit			% "\n"
	 %  "               of type: " % t			% "\n"
	 %  "                    at: " % getTSP ts		% "\n"
	 
	TSInst vDef vInst
	 -> "                use of: " % vDef			% "\n"
	 %  "             with type: " % t			% "\n"
	 %  "                    at: " % getTSP ts		% "\n"
	 
	TSIfObj sp
	 -> "        if-then-else expression"			% "\n"
	  % "         which expects: " % t			% "\n"

	TSApp sp 
	 -> "        function application" 			% "\n"
	  % "         which expects: " % t			% "\n"

	TSLambda sp 
	 -> "        lambda abstraction"			% "\n"
	  % "               of type: " % t			% "\n"

	TSSig sp var
	 -> "          type signature"				% "\n"
	 %  "          for variable: " % var			% "\n"
	 %  "                    at: " % sp			% "\n"

	TSProjCrushed c1 c2 j
	 -> "             projection"				% "\n"
	 %  "              of field: " % j			% "\n"

	TSField vData vCtor vField
	 -> "        declaration of,"				% "\n"
	 %  "                 field: " % vField			% "\n"
	 %  "             with type: " % t			% "\n"
	 %  "        in constructor: " % vCtor			% "\n"
	 %  "          of data type: " % vData			% "\n"
	 %  "                    at: " % getVSP vField		% "\n"

	_ -> ppr "ERROR: prettyTypeConflict: cannot show source of error\n" % "\n"

--	_ -> panic stage
--		$ "prettyTypeConflict: no match for " % show ts % "\n"




prettyFTS :: Fetter -> TypeSource -> PrettyP 
prettyFTS f ts
 = case ts of
 	TSInst vDef vInst
	 -> "            constraint: " % f			% "\n"
	 %  "       from the use of: " % vDef			% "\n"
	 %  "                    at: " % getTSP ts		% "\n"


prettyETS :: Effect -> TypeSource -> PrettyP
prettyETS e ts
 = case ts of
 	TSInst vDef vInst
	 -> "                effect: " % e			% "\n"
	 %  "             caused by: " % vDef			% "\n"
	 %  "                    at: " % getTSP ts		% "\n"
	 
	TSMatchObj sp
	 -> "                effect: " % e			% "\n"
	 %  "             caused by: match expression"		% "\n"
	 %  "                    at: " % getTSP ts		% "\n"
	 
	 
	TSNil
	 -> "                effect: " % e			% "\n"
	 %  " ERROR: prettyETS: cannot show source of error\n"  % "\n" 

	 
prettyTSP ::	TypeSource -> PrettyP
prettyTSP	ts
 = case ts of
 	TSInst vDef vInst
	 -> ppr vDef

	TSMatch sp
	 -> ppr "case"

	_ -> panic stage
		$ "prettyTSP: no match for " % show ts	% "\n"



-----
-- getTSP
--	get TypeSource pos
--	
getTSP :: TypeSource	-> SourcePos
getTSP ts
 	| TSLiteral sp c		<- ts
	= sp

	| TSInst vDefT vInstT 		<- ts
	, Just (Var.IValueVar vInstV)	
		<- find ((=@=) Var.IValueVar{})
		$  Var.info vInstT
			
	, Just (Var.ISourcePos posInst)
		<- find ((=@=) Var.ISourcePos{})
		$  Var.info vInstV
			
	= posInst

	| TSLambda sp			<- ts
	= sp

	| TSMatch sp			<- ts
	= sp
	
	| TSSig sp var			<- ts
	= sp

	| TSField vData vCtor vField	<- ts
	= getVSP vField

	| TSProj{}			<- ts
	= SourcePos ("<internal>", 0, 0)

	| otherwise		
	= SourcePos ("<unknown>", 0, 0)

--	_ -> panic stage
--		$ "getTSP: not match for " % show ts % "\n"


getVSP :: Var	-> SourcePos
getVSP	 var
 = let	Just (Var.ISourcePos pos)
		= find ((=@=) Var.ISourcePos{})
		$ Var.info var
		
   in	pos
 	

getProjSP :: TProj	-> SourcePos
getProjSP    p
 = case p of
 	TJField v	-> getVSP v
	TJFieldR v	-> getVSP v