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

Pretty printing for Core Lint errors #1453

Merged
merged 2 commits into from
Oct 13, 2022
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
6 changes: 5 additions & 1 deletion src/Cryptol/ModuleSystem/Base.hs
Original file line number Diff line number Diff line change
Expand Up @@ -574,7 +574,11 @@ typecheck act i params env = do
Right as ->
let ppIt l = mapM_ (logPrint l . T.pp)
in withLogger ppIt as
Left err -> panic "Core lint failed:" [show err]
Left (loc,err) ->
panic "Core lint failed:"
[ "Location: " ++ show (T.pp loc)
, show (T.pp err)
]
return o

T.InferFailed nameMap warns errs ->
Expand Down
120 changes: 119 additions & 1 deletion src/Cryptol/TypeCheck/Sanity.hs
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,7 @@
-- Maintainer : [email protected]
-- Stability : provisional
-- Portability : portable
{-# Language OverloadedStrings #-}
module Cryptol.TypeCheck.Sanity
( tcExpr
, tcDecls
Expand All @@ -19,8 +20,10 @@ import Cryptol.Parser.Position(thing,Range,emptyRange)
import Cryptol.TypeCheck.AST
import Cryptol.TypeCheck.Subst (apSubst, singleTParamSubst)
import Cryptol.TypeCheck.Monad(InferInput(..))
import Cryptol.ModuleSystem.Name(nameLoc)
import Cryptol.Utils.Ident
import Cryptol.Utils.RecordMap
import Cryptol.Utils.PP

import Data.List (sort)
import qualified Data.Set as Set
Expand Down Expand Up @@ -410,7 +413,11 @@ checkDecl checkSig d =
when checkSig $ checkSchema s
s1 <- exprSchema e
unless (same s s1) $
reportError $ TypeMismatch "DExpr" s s1
let nm = dName d
loc = "definition of " ++ show (pp nm) ++
", at " ++ show (pp (nameLoc nm))
in reportError $ TypeMismatch loc s s1

return (dName d, s)

checkDeclGroup :: DeclGroup -> TcM [(Name, Schema)]
Expand Down Expand Up @@ -586,3 +593,114 @@ lookupVar x =
case Map.lookup x (roVars ro) of
Just s -> return s
Nothing -> reportError $ UndefinedVariable x


instance PP Error where
ppPrec _ err =
case err of

TypeMismatch what expected actual ->
ppErr ("Type mismatch in" <+> text what)
[ "Expected:" <+> pp expected
, "Actual :" <+> pp actual
]

ExpectedMono s ->
ppErr "Not a monomorphic type"
[ pp s ]

TupleSelectorOutOfRange sel sz ->
ppErr "Tuple selector out of range"
[ "Selector:" <+> int sel
, "Size :" <+> int sz
]

MissingField f fs ->
ppErr "Invalid record selector"
[ "Field: " <+> pp f
, "Fields:" <+> commaSep (map pp fs)
]

UnexpectedTupleShape expected actual ->
ppErr "Unexpected tuple shape"
[ "Expected:" <+> int expected
, "Actual :" <+> int actual
]

UnexpectedRecordShape expected actual ->
ppErr "Unexpected record shape"
[ "Expected:" <+> commaSep (map pp expected)
, "Actual :" <+> commaSep (map pp actual)
]

UnexpectedSequenceShape n t ->
ppErr "Unexpected sequence shape"
[ "Expected:" <+> int n
, "Actual :" <+> pp t
]

BadSelector sel t ->
ppErr "Bad selector"
[ "Selector:" <+> pp sel
, "Type :" <+> pp t
]

BadInstantiation ->
ppErr "Bad instantiation" []

Captured x ->
ppErr "Captured type variable"
[ "Variable:" <+> pp x ]

BadProofNoAbs ->
ppErr "Proof application without a proof abstraction" []

BadProofTyVars xs ->
ppErr "Proof application with type abstraction"
[ "Type parameter:" <+> pp x | x <- xs ]

KindMismatch expected actual ->
ppErr "Kind mismatch"
[ "Expected:" <+> pp expected
, "Actual :" <+> pp actual
]

NotEnoughArgumentsInKind k ->
ppErr "Not enough arguments in kind" [ pp k ]

BadApplication t1 t2 ->
ppErr "Bad application"
[ "Function:" <+> pp t1
, "Argument:" <+> pp t2
]

FreeTypeVariable x ->
ppErr "Free type variable"
[ "Variable:" <+> pp x ]

BadTypeApplication kf ka ->
ppErr "Bad type application"
[ "Function :" <+> pp kf
, "Arguments:" <+> commaSep (map pp ka)
]

RepeatedVariableInForall x ->
ppErr "Repeated variable in forall"
[ "Variable:" <+> pp x ]

BadMatch t ->
ppErr "Bad match"
[ "Type:" <+> pp t ]

EmptyArm -> ppErr "Empty comprehension arm" []

UndefinedTypeVaraible x ->
ppErr "Undefined type variable"
[ "Variable:" <+> pp x ]

UndefinedVariable x ->
ppErr "Undefined variable"
[ "Variable:" <+> pp x ]

where
ppErr x ys = hang x 2 (vcat [ "•" <+> y | y <- ys ])