Error.hs

{-# OPTIONS -cpp #-}
#include "config.h"
-- | Error codes and error messages
module Error(EMsg, ErrMsg(..), PassMsg(..),prEMsg, prError, eMany,eMsg,isPassMsg) where
import Position
import Util(unwordsWith)
import PPrint
import Data.List(intersperse)

type EMsg = (Position, ErrMsg)

data PassMsg                          -- errors that will be handled somewhere else
        = EGetSort
        | ESplitSig
        | ESplitStruct
        | ESplitPackage
        | ESplitFun
        | ESplitMeta
        | ESplitData
        | ESplitSort
        | ESplitCon
        | ESplitStop
        | ENoArity
        | ENotEqual
        | ELookupProj
        | ENotInSig
        | EMissingRecField
        | ENoSolve
        | EImitate
        | ETooManyArgsCon
        | ETooMany
        | ETooFew
        | EProjImpossible
        | ETermProblem String
       | ENotInDef
     deriving (Show,Eq)

{-
data Warning =
      WNotTerminate String
    | WNotPositive String
-}




data ErrMsg
        = ESyntax String [String]       -- found token, expected tokens
        | EBadCharLit
        | EBadStringLit
        | EBadLexChar Char
        | EUntermComm Position
        | EMissingNL
        | EUnbound String

        | EDuplicate Position String
        | EDuplicateCon String
{-10-}  | ETypeError String String String String String Position
        | EKindError String String String String Position
--      | ETypeTermination String String
--      | EFieldNonKind String String
--      | EConNonKind String String
--      | EVarNonKind String String
        | ENotSum String
        | ENotSumElem String String
        | ENotProduct String String
        | ENotProductOpen
 {-20-} | ENotProductElem String String
        | ENotSumCase String String
        | ENotInType String String
--      | ENoSign String
--      | EBadRecursion String
        | ETermination String String
--         | EHide Bool String
--      | ENoHide String
        | EOverlap
        | EBadPatterns String
 {-30-} | EMissingPatArg String
--         | EExtraPatArg String
--      | ENoArms String
        | ETooManyArgs String
--      | EVaryingArgs String
--      | EVaryingHiddenArgs String
--      | ENoSignature String
--      | ENotHidden
--      | ENotProductCoerce String String
--      | ENotProductCoerceT String String
{-40-}  --  | ENoCoerce String String
        | ENotInRecord String String Position
        | EMany [EMsg]
        | ETEMP String

-- {-1-}        | WNoMatch
--      | WBoundConstr String
        | EConflictingModifiers String String
        | EUntermMeta Position
{-50-}        | EUninstantiated String
        | EUnknownConstraint String
        | EUnknownTactic String
        | ESolveNotApp String String
        | ESolveNonTerm Int
        | ECommand String
        | EInternal String
        | EPass PassMsg
        | EParseCommand String [String]
        | ENotType String String
        | ENotFunction
        | EInLetDef String String String
        | ERefineArity String
        | ERefine Int
        | ENotFun String String
        | ENotEqualValues String Position String
        | EDeclaredNotEqual String String String String
        | ENotEqualConstraints String String
        | ENotSignature String
        | ECanNotInferType String
        | EMissingField String Position
        | ETooManyFields String Position
        | EMisMatchingTypes String String String Position
        | ENotStruct String
        | ENotSetData
        | ENotTypeSig
        | WNotTerminate String
        | WNotPositive [String] String
       --  | WUnknownDataPos String
        --  | WMutual [String]
        --  | Warnings [EMsg]
        | EMissingConstrs [String]
        | ENrConstrArgs String Int
        | EPatternNotConstr
        | EPatternNested
        | ENoMeta
        | ENoOpenInMutual
        | EWrongPlace String
        | ENoFile String
        | ENoOpen
        | EBecause ErrMsg [EMsg]
        | EHiddenArgs
        | ENotClass String
        | EClassTooMany String
        | EClassNotVarArg String
        | ENoInstance String String
        | EIfNotBool String
        | ELookupPrelude String
        | ELastInDo
        | ENoSuchPlugin String
        | EPluginError String       -- ^ Error message for plugin
       deriving (Eq)


instance Show ErrMsg where
--    showsType _ = showString "Errmsg"
    showsPrec _ e = showString "ErrMsg:" . showString (prError e)

instance PPrint ErrMsg where
    pPrint _ _ e = text (show e)


prEMsg (p,m) = let s = prPosition p
               in if null s
                     then prError m
                     else "At: "++s++"\n"++prError m
-- 1
prError (ESyntax s ss)                 = "Syntax error: found token "++s++
                                         if null ss then "" else ", expected "++unwordsOr ss
prError EBadCharLit                    = "Bad Char CSynliteral"
prError EBadStringLit                  = "Bad String literal"
prError (EBadLexChar c)                = "Bad character in input: "++show c
prError (EUntermComm p)                = "Unterminated {- comment, started at "++prPosition p
                                                       -- -}
prError EMissingNL                     = "Missing new line after -- comment"
prError (EUnbound i)                   = "Undefined identifier: "++ishow i
prError (EConflictingModifiers s1 s2)  = "Conflicting modifiers: "++s1++" and "++s2
prError (EDuplicate p i)               = "Duplicate definition of "++ishow i++", other definition at "++prPosition p
prError (EDuplicateCon i)              = "Duplicate constructor names: "++ishow i
prError (ETypeError s msg e t1 t2 pos) =
       "Type error: "++s++
       "\nExpression\n"++e++
       "  has type\n"++t1++
       "  but should have type that is equal to\n"++t2++"\n"++
       prPos "  from " pos ++ msg
prError (EKindError msg e t1 t2 pos) =
     "Sort error: "++"\n"++
       e++ "  has sort\n"++
       t1++"  which is not contained in\n "++
       t2++
       prPos "  from " pos ++ msg
-- prError (ETypeTermination e t) =
--     "Type error: Cannot normalize \n"++t
-- prError (EFieldNonKind t i) = "Field type illegal: "++ i ++" :: " ++ t
-- prError (EConNonKind t i) = "Constructor field type illegal: " ++ t
-- prError (EVarNonKind t i) = "Variable type illegal: " ++ i ++ " :: " ++ t
prError (ENotSum t)           = "Constructor type is not a data: " ++ t
prError (ENotSumElem i t)     = "Constructor type does not contain constructor: " ++ i ++ " in " ++ t
prError (ENotProduct t i)     = "Type of selection expression ( ."++i++" ) not a signature: " ++ t
prError ENotProductOpen       = "Open expression is neither a package nor of signature type"
prError (ENotProductElem t i) = "Signature\n"++t++"\ndoes not contain selector: " ++ i
prError (ENotSumCase t i)     = "Case inspection on a non-data type: " ++ t
prError (ENotInType t i)      = "Type does not contain constructor: " ++ i ++ " in " ++ t
-- prError (ENoSign i) = "Definition must have a (complete) type signature: " ++ i
-- prError (EBadRecursion e) = "Illegal recursion in definition: " ++ e
prError (ETermination e e') = "No termination in:\n" ++ e ++"\nLast evaluation was:\n"++e'
-- prError (EHide b e) = "Argument should " ++ (if b then "" else "not ") ++ "be hidden: " ++ e
-- prError (ENoHide i) = "Cannot figure out hidden argument: " ++ i
prError (EOverlap) = "Overlapping pattern"
prError (EBadPatterns e) = "Bad patterns: " ++ e
prError (EMissingPatArg i) = "Missing/excess arguments to pattern constructor: " ++ i
-- prError (EExtraPatArg i) = "Extra argument to pattern constructor: " ++ i
-- prError (ENoArms e) = "Cannot figure out type of empty case: " ++ e
prError (ETooManyArgs p) = "More function arguments than the function type specifies: " ++ p
-- prError (EVaryingArgs i) = "Varying number of arguments to function: " ++ i
-- prError (EVaryingHiddenArgs i) = "Varying hiding of arguments to function: " ++ i
-- prError (ENotHidden) = "Hiding marker on non-hidden argument"
-- prError (ENotProductCoerce e t) = "Expression not a product: " ++ e ++ ", has type " ++ t
-- prError (ENotProductCoerceT t' t) = "Type not a product: " ++ t ++ "= " ++ t'
-- prError (ENoCoerce t e) = "Impossible coercion: " ++ e ++ " :: " ++ t
prError (ENotInRecord i t pos) = "Selection expression ( ."++i++" ) not in record : " ++ t ++
   prPos "\nnear " pos
prError (EMany es) = "Many:\n" ++ unlines (map prEMsg es)
prError (ETEMP s) = s

-- prError (WNoMatch) = "Missing cases, pattern matching may fail"
-- prError (WBoundConstr i) = "Variable in pattern with same the name as a constructor: " ++ i
-- prError _ = internalError "Missing error message."
prError (EUntermMeta p)        = "Unterminated {! meta variable, started at "++prPosition p
prError (EUninstantiated s)    = "Meta variable ?"++s++" is already instantiated or does not exist"
prError (EUnknownConstraint n) = "There is no such constraint: "++n
prError (EUnknownTactic n)     = "Unknown tactic: "++n
prError (ESolveNotApp n c)     = "You can not apply solve tactic: "++n++" on constraint "++c
prError (ESolveNonTerm n)      = "Solve has not terminated after "++show n++" calls"
prError (ECommand s)           = "Not allowed at this point: "++s
prError (EInternal msg)        = "good error message not implemented yet: \n"++msg++"\n"
prError (EPass p)              = "Internal error  : uncaught exception "++show p
prError (EParseCommand msg ss) = "Command error: found "++ msg++
                                 if null ss then "" else ", expected "++unwordsOr ss
prError (ENotType e t)         = "The type of "++e++" is "++t++". The type should be a sort"
prError (EInLetDef c k msg)    = "Error in the "++k++" of "++c++" because:\n"++msg
prError (ERefineArity t)       = "Can not refine because the number of arguments needed for: \n"++ t ++ " is unknown"
prError (ERefine i)            = "Can not refine, eiher it is not type correct or it has more than "++show i++" arguments"
prError (ENotFun e t)          = "Type error :\n  Expression "++ e ++
                                 "\nis declared to have type \n"++t ++
                                 "\nwhich is not a function type"

prError (ENotEqualValues s1 pos s2)     = "Expression \n"++ s1++"\nis not equal to\n"++s2++
  prPos " at position" pos
prError (EDeclaredNotEqual x t1 t2 msg) = "Variable "++x++" is declared to have type:\n"++t1++"\nwhich is not equal to:\n"++t2++(if null msg then "" else "\nsince \n"++msg)
prError (ENotEqualConstraints c msg)    = "The constraint\n" ++ c ++ "\n is unsolvable"++(if null msg then "\n" else " since\n"++msg)
prError (ENotSignature t)               = "The type of the structure is\n"++t++"\nwhich is not a signature"
prError (ECanNotInferType t)            = "Can not infer the type of:\n"++t
prError (EMissingField c pos)           = "Field: "++c++" at "++prPosition pos++" is missing in the structure"
prError (EMisMatchingTypes c t msg pos) = "Type of "++c++" : \n"++t++" does not match with declared type near "++prPosition pos++(if null msg then "" else " since \n"++msg)
prError (ETooManyFields s pos)          = "The field: "++s++ " is not defined in the signature near: "++prPosition pos
prError (ENotStruct e)                  =  "Expression: "++e++" must reduce to a structure"
prError (ENotSetData)                   = "data must have kind: Set"
prError ENotTypeSig                     = "Type of signature must be a sort"
prError (WNotTerminate str)             = "The call: "++str++"\nmight lead to non-termination"
prError (WNotPositive strs str)         = "The function"++plural "" str++" "++unwordsx "or" strs
                ++ " might have         a negative occurence of "++str


--prError (WMutual ss) = "Can not control the correctness of mutual definitions. Have not checked "++unwordsx "and" ss
--prError (WUnknownDataPos s) = "Can not check positivity of "++s
--prError (Warnings es) = "Warnings:\n" ++ unlines (map prEMsg es)
prError (EMissingConstrs ss) = "Missing constructors in case: "++ unwordsx "and" ss
prError (ENrConstrArgs s i) = "Constructor: "++s++" needs "++(show i)++" arguments"
prError ELastInDo = "an expression must be last in a do-block"

prError EPatternNotConstr    = "Only constructors are allowed in pattern"
prError EPatternNested       = "Nested patterns are not allowed"
prError ENoMeta              = "Imported file must not contain meta variables"
prError ENoOpenInMutual      = "No open definition in mutual definitions"
prError (EWrongPlace s)      = "You can not make " ++s++ " here"
prError (ENoFile f)          = "No such file: "++f
prError ENoOpen              = "Can only open top level packages at this point"
prError (EBecause e ms)      = prError e ++ "Because:\n" ++ unlines (map prEMsg ms)
prError (EHiddenArgs)        = "Hidden arguments/parameters don't match"
prError (ENotClass s)        = s ++ " is not a class"
prError (EClassTooMany s)    = "Only one argument is allowed "++s
prError (EClassNotVarArg s)  = "Argument must be a variables, was: " ++ s
prError (ENoInstance s1 s2)  = s1 ++ " is not an instance of " ++ s2
prError (EIfNotBool s)       = "type of: " ++ s ++ " is not Bool"
prError (ELookupPrelude s)   = "Internal error, could not lookup prelude name: " ++ s
prError (ENoSuchPlugin s) = "No such plugin: " ++ s
prError (EPluginError s) = "Plugin error: " ++ s

prPos :: String -> Position -> String
prPos str pos =
  if pos /= noPosition then str ++ prPosition pos ++ "\n"
                       else ""


eMsg :: Position -> ErrMsg -> EMsg
eMsg p e = (p,e)


isPassMsg (_,EPass _) = True
isPassMsg _ = False

ishow :: String -> String
ishow s = "\"" ++ s ++ "\""

plural s  [_] = s
plural ""  _ = "s"
plural "y" _ = "ies"
plural "s" _ = "es"

unwordsAnd = unwordsx "and"
unwordsOr = unwordsx "or"

unwordsx _ [] = ""
unwordsx _ [x] = x
unwordsx s [x1, x2] = unwords [x1, s, x2]
unwordsx s xs = unwordsWith ", " (init xs++[s++" "++last xs])

eMany es = (noPosition, EMany es)

--eWarning es = (noPosition, Warnings es)