Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Tc errors #964

Merged
merged 6 commits into from
Nov 17, 2020
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion cryptol-remote-api/src/CryptolServer/Data/Type.hs
Original file line number Diff line number Diff line change
Expand Up @@ -50,7 +50,7 @@ instance JSON.ToJSON JSONKind where
instance JSON.ToJSON JSONType where
toJSON (JSONType ns t) = convert t
where
convert (TCon (TError _ _) _) =
convert (TCon (TError {}) _) =
-- TODO: figure out what to do in this situation
error "JSON conversion of errors is not yet supported"
convert (TCon (TC tc) args) =
Expand Down
4 changes: 2 additions & 2 deletions cryptol-remote-api/src/CryptolServer/Exceptions.hs
Original file line number Diff line number Diff line change
Expand Up @@ -84,7 +84,7 @@ cryptolError modErr warns =
(20720, [ ("source", jsonPretty src)
, ("errors", jsonList (map jsonShow errs))
])
TypeCheckingFailed src errs ->
TypeCheckingFailed src _nameMap errs ->
-- TODO: structured error here
(20730, [ ("source", jsonPretty src)
, ("errors", jsonList (map jsonShow errs))
Expand Down Expand Up @@ -119,7 +119,7 @@ cryptolError modErr warns =
-- TODO: structured error here
jsonList . concatMap
(\w -> case w of
TypeCheckWarnings tcwarns ->
TypeCheckWarnings _nameMap tcwarns ->
map (jsonPretty . snd) tcwarns
RenamerWarnings rnwarns ->
map jsonPretty rnwarns)
Expand Down
4 changes: 2 additions & 2 deletions src/Cryptol/Eval/Type.hs
Original file line number Diff line number Diff line change
Expand Up @@ -132,8 +132,8 @@ evalType env ty =
_ -> evalPanic "evalType" ["not a value type", show ty]
TCon (TF f) ts -> Left $ evalTF f (map num ts)
TCon (PC p) _ -> evalPanic "evalType" ["invalid predicate symbol", show p]
TCon (TError _ x) _ -> evalPanic "evalType"
["Lingering typer error", show (pp x)]
TCon (TError _) ts -> evalPanic "evalType"
$ "Lingering invalid type" : map (show . pp) ts
where
val = evalValType env
num = evalNumType env
Expand Down
10 changes: 5 additions & 5 deletions src/Cryptol/ModuleSystem/Base.hs
Original file line number Diff line number Diff line change
Expand Up @@ -505,10 +505,10 @@ typecheck act i params env = do

case out of

T.InferOK warns seeds supply' o ->
T.InferOK nameMap warns seeds supply' o ->
do setNameSeeds seeds
setSupply supply'
typeCheckWarnings warns
typeCheckWarnings nameMap warns
menv <- getModuleEnv
case meCoreLint menv of
NoCoreLint -> return ()
Expand All @@ -519,9 +519,9 @@ typecheck act i params env = do
Left err -> panic "Core lint failed:" [show err]
return o

T.InferFailed warns errs ->
do typeCheckWarnings warns
typeCheckingFailed errs
T.InferFailed nameMap warns errs ->
do typeCheckWarnings nameMap warns
typeCheckingFailed nameMap errs

-- | Generate input for the typechecker.
genInferInput :: Range -> PrimMap ->
Expand Down
22 changes: 11 additions & 11 deletions src/Cryptol/ModuleSystem/Monad.hs
Original file line number Diff line number Diff line change
Expand Up @@ -96,7 +96,7 @@ data ModuleError
-- ^ Problems during the NoPat phase
| NoIncludeErrors ImportSource [NoInc.IncludeError]
-- ^ Problems during the NoInclude phase
| TypeCheckingFailed ImportSource [(Range,T.Error)]
| TypeCheckingFailed ImportSource T.NameMap [(Range,T.Error)]
-- ^ Problems during type checking
| OtherFailure String
-- ^ Problems after type checking, eg. specialization
Expand Down Expand Up @@ -128,7 +128,7 @@ instance NFData ModuleError where
RenamerErrors src errs -> src `deepseq` errs `deepseq` ()
NoPatErrors src errs -> src `deepseq` errs `deepseq` ()
NoIncludeErrors src errs -> src `deepseq` errs `deepseq` ()
TypeCheckingFailed src errs -> src `deepseq` errs `deepseq` ()
TypeCheckingFailed nm src errs -> nm `deepseq` src `deepseq` errs `deepseq` ()
ModuleNameMismatch expected found ->
expected `deepseq` found `deepseq` ()
DuplicateModuleName name path1 path2 ->
Expand Down Expand Up @@ -176,7 +176,7 @@ instance PP ModuleError where

NoIncludeErrors _src errs -> vcat (map NoInc.ppIncludeError errs)

TypeCheckingFailed _src errs -> vcat (map T.ppError errs)
TypeCheckingFailed _src nm errs -> vcat (map (T.ppNamedError nm) errs)

ModuleNameMismatch expected found ->
hang (text "[error]" <+> pp (P.srcRange found) <.> char ':')
Expand Down Expand Up @@ -239,10 +239,10 @@ noIncludeErrors errs = do
src <- getImportSource
ModuleT (raise (NoIncludeErrors src errs))

typeCheckingFailed :: [(Range,T.Error)] -> ModuleM a
typeCheckingFailed errs = do
typeCheckingFailed :: T.NameMap -> [(Range,T.Error)] -> ModuleM a
typeCheckingFailed nameMap errs = do
src <- getImportSource
ModuleT (raise (TypeCheckingFailed src errs))
ModuleT (raise (TypeCheckingFailed src nameMap errs))

moduleNameMismatch :: P.ModName -> Located P.ModName -> ModuleM a
moduleNameMismatch expected found =
Expand Down Expand Up @@ -273,22 +273,22 @@ errorInFile file (ModuleT m) = ModuleT (m `handle` h)
-- Warnings --------------------------------------------------------------------

data ModuleWarning
= TypeCheckWarnings [(Range,T.Warning)]
= TypeCheckWarnings T.NameMap [(Range,T.Warning)]
| RenamerWarnings [RenamerWarning]
deriving (Show, Generic, NFData)

instance PP ModuleWarning where
ppPrec _ w = case w of
TypeCheckWarnings ws -> vcat (map T.ppWarning ws)
TypeCheckWarnings nm ws -> vcat (map (T.ppNamedWarning nm) ws)
RenamerWarnings ws -> vcat (map pp ws)

warn :: [ModuleWarning] -> ModuleM ()
warn = ModuleT . put

typeCheckWarnings :: [(Range,T.Warning)] -> ModuleM ()
typeCheckWarnings ws
typeCheckWarnings :: T.NameMap -> [(Range,T.Warning)] -> ModuleM ()
typeCheckWarnings nameMap ws
| null ws = return ()
| otherwise = warn [TypeCheckWarnings ws]
| otherwise = warn [TypeCheckWarnings nameMap ws]

renamerWarnings :: [RenamerWarning] -> ModuleM ()
renamerWarnings ws
Expand Down
4 changes: 2 additions & 2 deletions src/Cryptol/REPL/Command.hs
Original file line number Diff line number Diff line change
Expand Up @@ -1554,10 +1554,10 @@ moduleCmdResult (res,ws0) = do
isDefaultWarn _ = False

filterDefaults w | warnDefaulting = Just w
filterDefaults (M.TypeCheckWarnings xs) =
filterDefaults (M.TypeCheckWarnings nameMap xs) =
case filter (not . isDefaultWarn . snd) xs of
[] -> Nothing
ys -> Just (M.TypeCheckWarnings ys)
ys -> Just (M.TypeCheckWarnings nameMap ys)
filterDefaults w = Just w

isShadowWarn (M.SymbolShadowed {}) = True
Expand Down
14 changes: 14 additions & 0 deletions src/Cryptol/TypeCheck.hs
Original file line number Diff line number Diff line change
Expand Up @@ -21,6 +21,10 @@ module Cryptol.TypeCheck
, Warning(..)
, ppWarning
, ppError
, WithNames(..)
, NameMap
, ppNamedWarning
, ppNamedError
) where

import Cryptol.ModuleSystem.Name
Expand All @@ -43,6 +47,7 @@ import Cryptol.TypeCheck.InferTypes(VarType(..), SolverConfig(..))
import Cryptol.TypeCheck.Solve(proveModuleTopLevel)
import Cryptol.TypeCheck.CheckModuleInstance(checkModuleInstance)
import Cryptol.TypeCheck.Monad(withParamType,withParameterConstraints)
import Cryptol.TypeCheck.PP(WithNames(..),NameMap)
import Cryptol.Utils.Ident (exprModName,packIdent)
import Cryptol.Utils.PP
import Cryptol.Utils.Panic(panic)
Expand Down Expand Up @@ -122,3 +127,12 @@ ppError :: (Range,Error) -> Doc
ppError (r,w) = text "[error] at" <+> pp r <.> colon $$ nest 2 (pp w)


ppNamedWarning :: NameMap -> (Range,Warning) -> Doc
ppNamedWarning nm (r,w) =
text "[warning] at" <+> pp r <.> colon $$ nest 2 (pp (WithNames w nm))

ppNamedError :: NameMap -> (Range,Error) -> Doc
ppNamedError nm (r,e) =
text "[error] at" <+> pp r <.> colon $$ nest 2 (pp (WithNames e nm))


1 change: 0 additions & 1 deletion src/Cryptol/TypeCheck/AST.hs
Original file line number Diff line number Diff line change
Expand Up @@ -25,7 +25,6 @@ module Cryptol.TypeCheck.AST
, Pragma(..)
, Fixity(..)
, PrimMap(..)
, TCErrorMessage(..)
, module Cryptol.TypeCheck.Type
) where

Expand Down
18 changes: 10 additions & 8 deletions src/Cryptol/TypeCheck/CheckModuleInstance.hs
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,6 @@ import Cryptol.TypeCheck.Monad
import Cryptol.TypeCheck.Infer
import Cryptol.TypeCheck.Subst
import Cryptol.TypeCheck.Error
import Cryptol.Utils.PP
import Cryptol.Utils.Panic


Expand Down Expand Up @@ -61,10 +60,12 @@ checkTyParams func inst =
tParams = Map.fromList [ (tpId x, x) | x0 <- Map.elems (mParamTypes inst)
, let x = mtpParam x0 ]

tpId x = case tpName x of
Just n -> nameIdent n
tpName' x = case tpName x of
Just n -> n
Nothing -> panic "inferModuleInstance.tpId" ["Missing name"]

tpId = nameIdent . tpName'

-- Find a definition for a given type parameter
checkTParamDefined tp0 =
let tp = mtpParam tp0
Expand All @@ -78,8 +79,9 @@ checkTyParams func inst =
case Map.lookup x tParams of
Just tp1 -> checkTP tp tp1
Nothing ->
do recordError $ ErrorMsg $
text "Missing definition for type parameter:" <+> pp x
do let x' = Located { thing = x,
srcRange = nameLoc (tpName' tp) }
recordError (MissingModTParam x')
return (tp, TVar (TVBound tp)) -- hm, maybe just stop!

-- Check that a type parameter defined as a type synonym is OK
Expand Down Expand Up @@ -148,9 +150,9 @@ checkValParams func tMap inst =
case Map.lookup (nameIdent x) valMap of
Just (n,sD) -> do e <- makeValParamDef n sD (apSubst su sP)
return (x,e)
Nothing -> do recordError $ ErrorMsg
$ text "Mising definition for value parameter"
<+> pp x
Nothing -> do recordError (MissingModVParam
Located { thing = nameIdent x
, srcRange = nameLoc x })
return (x, panic "checkValParams" ["Should not use this"])


Expand Down
Loading