{-# LANGUAGE FlexibleContexts    #-}
{-# LANGUAGE FlexibleInstances   #-}
{-# LANGUAGE OverloadedStrings   #-}
{-# LANGUAGE DeriveGeneric       #-}
{-# LANGUAGE DeriveDataTypeable  #-}
{-# LANGUAGE DeriveFunctor       #-}
{-# LANGUAGE DerivingVia         #-}

{-# OPTIONS_GHC -Wno-incomplete-patterns #-} -- TODO(#1918): Only needed for GHC <9.0.1.
{-# OPTIONS_GHC -Wno-orphans #-} -- PPrint and aeson instances.

-- | This module contains the *types* related creating Errors.
--   It depends only on Fixpoint and basic haskell libraries,
--   and hence, should be importable everywhere.

module Language.Haskell.Liquid.Types.Errors (
  -- * Generic Error Type
    TError (..)

  -- * Parse error synonym
  , ParseError

  -- * Error with Source Context
  , CtxError (..)
  , errorsWithContext

  -- * Subtyping Obligation Type
  , Oblig (..)

  -- * Adding a Model of the context
  , WithModel (..), dropModel

  -- * Panic (unexpected failures)
  , UserError
  , panic
  , panicDoc
  , todo
  , impossible
  , uError
  , sourceErrors
  , errDupSpecs

  -- * Printing Errors
  , ppError
  , ppTicks

  -- * SrcSpan Helpers
  , packRealSrcSpan
  , unpackRealSrcSpan
  , srcSpanFileMb
  ) where

import           Prelude                      hiding (error, span)

import           GHC.Generics
import           Control.DeepSeq
import qualified Control.Exception            as Ex
import           Data.Typeable                (Typeable)
import           Data.Generics                (Data)
import qualified Data.Binary                  as B
import qualified Data.Maybe                   as Mb
import           Data.Aeson                   hiding (Result)
import           Data.Hashable
import qualified Data.HashMap.Strict          as M
import qualified Data.List                    as L
import           Data.Void
import           System.Directory
import           System.FilePath
import           Text.PrettyPrint.HughesPJ
import qualified Text.Megaparsec              as P

import           Liquid.GHC.API as Ghc hiding ( Expr
                                                               , ($+$)
                                                               , nest
                                                               , text
                                                               , blankLine
                                                               , (<+>)
                                                               , vcat
                                                               , hsep
                                                               , comma
                                                               , colon
                                                               , parens
                                                               , empty
                                                               , char
                                                               , panic
                                                               , int
                                                               , hcat
                                                               )
import           Language.Fixpoint.Types      (pprint, showpp, Tidy (..), PPrint (..), Symbol, Expr, SubcId)
import qualified Language.Fixpoint.Misc       as Misc
import qualified Language.Haskell.Liquid.Misc     as Misc
import           Language.Haskell.Liquid.Misc ((<->))
import           Language.Haskell.Liquid.Types.Generics

type ParseError = P.ParseError String Void

instance PPrint ParseError where
  pprintTidy :: Tidy -> ParseError -> Doc
pprintTidy Tidy
_ ParseError
e = [Doc] -> Doc
vcat forall a b. (a -> b) -> a -> b
$ FilePath -> Doc
text forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [FilePath]
ls
    where
      ls :: [FilePath]
ls         = FilePath -> [FilePath]
lines forall a b. (a -> b) -> a -> b
$ forall s e.
(VisualStream s, ShowErrorComponent e) =>
ParseError s e -> FilePath
P.parseErrorTextPretty ParseError
e

--------------------------------------------------------------------------------
-- | Context information for Error Messages ------------------------------------
--------------------------------------------------------------------------------
data CtxError t = CtxError
  { forall t. CtxError t -> TError t
ctErr :: TError t
  , forall t. CtxError t -> Doc
ctCtx :: Doc
  } deriving (forall a b. a -> CtxError b -> CtxError a
forall a b. (a -> b) -> CtxError a -> CtxError b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> CtxError b -> CtxError a
$c<$ :: forall a b. a -> CtxError b -> CtxError a
fmap :: forall a b. (a -> b) -> CtxError a -> CtxError b
$cfmap :: forall a b. (a -> b) -> CtxError a -> CtxError b
Functor)

instance Eq (CtxError t) where
  CtxError t
e1 == :: CtxError t -> CtxError t -> Bool
== CtxError t
e2 = forall t. CtxError t -> TError t
ctErr CtxError t
e1 forall a. Eq a => a -> a -> Bool
== forall t. CtxError t -> TError t
ctErr CtxError t
e2

--------------------------------------------------------------------------------
errorsWithContext :: [TError Doc] -> IO [CtxError Doc]
--------------------------------------------------------------------------------
errorsWithContext :: [UserError] -> IO [CtxError Doc]
errorsWithContext [UserError]
es
  = forall (m :: * -> *) (t :: * -> *) a b.
(Monad m, Traversable t) =>
(a -> m [b]) -> t a -> m [b]
Misc.concatMapM (Maybe FilePath, [UserError]) -> IO [CtxError Doc]
fileErrors
  forall a b. (a -> b) -> a -> b
$ forall k v. (Eq k, Hashable k) => [(k, v)] -> [(k, [v])]
Misc.groupList [ (SrcSpan -> Maybe FilePath
srcSpanFileMb (forall t. TError t -> SrcSpan
pos UserError
e), UserError
e) | UserError
e <- [UserError]
es ]

fileErrors :: (Maybe FilePath, [TError Doc]) -> IO [CtxError Doc]
fileErrors :: (Maybe FilePath, [UserError]) -> IO [CtxError Doc]
fileErrors (Maybe FilePath
fp, [UserError]
errs) = do
  [FilePath]
fb  <- Maybe FilePath -> IO [FilePath]
getFileBody Maybe FilePath
fp
  forall (m :: * -> *) a. Monad m => a -> m a
return ([FilePath] -> UserError -> CtxError Doc
errorWithContext [FilePath]
fb forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [UserError]
errs)

errorWithContext :: FileBody -> TError Doc -> CtxError Doc
errorWithContext :: [FilePath] -> UserError -> CtxError Doc
errorWithContext [FilePath]
fb UserError
e = forall t. TError t -> Doc -> CtxError t
CtxError UserError
e ([FilePath] -> SrcSpan -> Doc
srcSpanContext [FilePath]
fb (forall t. TError t -> SrcSpan
pos UserError
e))

srcSpanContext :: FileBody -> SrcSpan -> Doc
srcSpanContext :: [FilePath] -> SrcSpan -> Doc
srcSpanContext [FilePath]
fb SrcSpan
sp
  | Just (Int
l, Int
c, Int
l', Int
c') <- SrcSpan -> Maybe (Int, Int, Int, Int)
srcSpanInfo SrcSpan
sp
  = Int -> Int -> Int -> [FilePath] -> Doc
makeContext Int
l Int
c Int
c' ([FilePath] -> Int -> Int -> [FilePath]
getFileLines [FilePath]
fb Int
l Int
l')
  | Bool
otherwise
  = Doc
empty

srcSpanInfo :: SrcSpan -> Maybe (Int, Int, Int, Int)
srcSpanInfo :: SrcSpan -> Maybe (Int, Int, Int, Int)
srcSpanInfo (RealSrcSpan RealSrcSpan
s Maybe BufSpan
_)
              = forall a. a -> Maybe a
Just (Int
l, Int
c, Int
l', Int
c')
  where
     l :: Int
l        = RealSrcSpan -> Int
srcSpanStartLine RealSrcSpan
s
     c :: Int
c        = RealSrcSpan -> Int
srcSpanStartCol  RealSrcSpan
s
     l' :: Int
l'       = RealSrcSpan -> Int
srcSpanEndLine   RealSrcSpan
s
     c' :: Int
c'       = RealSrcSpan -> Int
srcSpanEndCol    RealSrcSpan
s
srcSpanInfo SrcSpan
_ = forall a. Maybe a
Nothing

getFileLines :: FileBody -> Int -> Int -> [String]
getFileLines :: [FilePath] -> Int -> Int -> [FilePath]
getFileLines [FilePath]
fb Int
i Int
j = forall a. Int -> Int -> [a] -> [a]
slice (Int
i forall a. Num a => a -> a -> a
- Int
1) (Int
j forall a. Num a => a -> a -> a
- Int
1) [FilePath]
fb

getFileBody :: Maybe FilePath -> IO FileBody
getFileBody :: Maybe FilePath -> IO [FilePath]
getFileBody Maybe FilePath
Nothing  =
  forall (m :: * -> *) a. Monad m => a -> m a
return []
getFileBody (Just FilePath
f) = do
  Bool
b <- FilePath -> IO Bool
doesFileExist FilePath
f
  if Bool
b then FilePath -> [FilePath]
lines forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FilePath -> IO FilePath
Misc.sayReadFile FilePath
f
       else forall (m :: * -> *) a. Monad m => a -> m a
return []

type FileBody = [String]

slice :: Int -> Int -> [a] -> [a]
slice :: forall a. Int -> Int -> [a] -> [a]
slice Int
i Int
j [a]
xs = forall a. Int -> [a] -> [a]
take (Int
j forall a. Num a => a -> a -> a
- Int
i forall a. Num a => a -> a -> a
+ Int
1) (forall a. Int -> [a] -> [a]
drop Int
i [a]
xs)

makeContext :: Int -> Int -> Int -> [String] -> Doc
makeContext :: Int -> Int -> Int -> [FilePath] -> Doc
makeContext Int
_ Int
_ Int
_  []  = Doc
empty
makeContext Int
l Int
c Int
c' [FilePath
s] = Int -> Int -> Int -> FilePath -> Doc
makeContext1 Int
l Int
c Int
c' FilePath
s
makeContext Int
l Int
_ Int
_  [FilePath]
ss  = [Doc] -> Doc
vcat forall a b. (a -> b) -> a -> b
$ FilePath -> Doc
text FilePath
" "
                              forall a. a -> [a] -> [a]
: forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Int -> FilePath -> Doc
makeContextLine [Int
l..] [FilePath]
ss
                              forall a. [a] -> [a] -> [a]
++ [ FilePath -> Doc
text FilePath
" "
                                 , FilePath -> Doc
text FilePath
" " ]

makeContextLine :: Int -> String -> Doc
makeContextLine :: Int -> FilePath -> Doc
makeContextLine Int
l FilePath
s = forall {a}. Show a => a -> Doc
lnum Int
l Doc -> Doc -> Doc
<+> FilePath -> Doc
text FilePath
s
  where
    lnum :: a -> Doc
lnum a
n          = FilePath -> Doc
text (forall a. Show a => a -> FilePath
show a
n) Doc -> Doc -> Doc
<+> FilePath -> Doc
text FilePath
"|"

makeContext1 :: Int -> Int -> Int -> String -> Doc
makeContext1 :: Int -> Int -> Int -> FilePath -> Doc
makeContext1 Int
l Int
c Int
c' FilePath
s = [Doc] -> Doc
vcat [ FilePath -> Doc
text FilePath
" "
                             , forall {a}. Show a => a -> Doc
lnum Int
l Doc -> Doc -> Doc
<+> (FilePath -> Doc
text FilePath
s Doc -> Doc -> Doc
$+$ Doc
cursor)
                             , FilePath -> Doc
text FilePath
" "
                             , FilePath -> Doc
text FilePath
" "
                             ]
  where
    lnum :: a -> Doc
lnum a
n            = FilePath -> Doc
text (forall a. Show a => a -> FilePath
show a
n) Doc -> Doc -> Doc
<+> FilePath -> Doc
text FilePath
"|"
    cursor :: Doc
cursor            = Int -> Doc
blanks (Int
c forall a. Num a => a -> a -> a
- Int
1) Doc -> Doc -> Doc
<-> Int -> Doc
pointer (forall a. Ord a => a -> a -> a
max Int
1 (Int
c' forall a. Num a => a -> a -> a
- Int
c))
    blanks :: Int -> Doc
blanks Int
n          = FilePath -> Doc
text forall a b. (a -> b) -> a -> b
$ forall a. Int -> a -> [a]
replicate Int
n Char
' '
    pointer :: Int -> Doc
pointer Int
n         = FilePath -> Doc
text forall a b. (a -> b) -> a -> b
$ forall a. Int -> a -> [a]
replicate Int
n Char
'^'

--------------------------------------------------------------------------------
-- | Different kinds of Check "Obligations" ------------------------------------
--------------------------------------------------------------------------------

data Oblig
  = OTerm -- ^ Obligation that proves termination
  | OInv  -- ^ Obligation that proves invariants
  | OCons -- ^ Obligation that proves subtyping constraints
  deriving (Oblig -> Oblig -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Oblig -> Oblig -> Bool
$c/= :: Oblig -> Oblig -> Bool
== :: Oblig -> Oblig -> Bool
$c== :: Oblig -> Oblig -> Bool
Eq, forall x. Rep Oblig x -> Oblig
forall x. Oblig -> Rep Oblig x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Oblig x -> Oblig
$cfrom :: forall x. Oblig -> Rep Oblig x
Generic, Typeable Oblig
Oblig -> DataType
Oblig -> Constr
(forall b. Data b => b -> b) -> Oblig -> Oblig
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Oblig -> u
forall u. (forall d. Data d => d -> u) -> Oblig -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Oblig -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Oblig -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Oblig -> m Oblig
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Oblig -> m Oblig
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Oblig
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Oblig -> c Oblig
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Oblig)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Oblig)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Oblig -> m Oblig
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Oblig -> m Oblig
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Oblig -> m Oblig
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Oblig -> m Oblig
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Oblig -> m Oblig
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Oblig -> m Oblig
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Oblig -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Oblig -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> Oblig -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Oblig -> [u]
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Oblig -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Oblig -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Oblig -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Oblig -> r
gmapT :: (forall b. Data b => b -> b) -> Oblig -> Oblig
$cgmapT :: (forall b. Data b => b -> b) -> Oblig -> Oblig
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Oblig)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Oblig)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Oblig)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Oblig)
dataTypeOf :: Oblig -> DataType
$cdataTypeOf :: Oblig -> DataType
toConstr :: Oblig -> Constr
$ctoConstr :: Oblig -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Oblig
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Oblig
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Oblig -> c Oblig
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Oblig -> c Oblig
Data, Typeable)
  deriving Eq Oblig
Int -> Oblig -> Int
Oblig -> Int
forall a. Eq a -> (Int -> a -> Int) -> (a -> Int) -> Hashable a
hash :: Oblig -> Int
$chash :: Oblig -> Int
hashWithSalt :: Int -> Oblig -> Int
$chashWithSalt :: Int -> Oblig -> Int
Hashable via Generically Oblig

instance B.Binary Oblig
instance Show Oblig where
  show :: Oblig -> FilePath
show Oblig
OTerm = FilePath
"termination-condition"
  show Oblig
OInv  = FilePath
"invariant-obligation"
  show Oblig
OCons = FilePath
"constraint-obligation"

instance NFData Oblig

instance PPrint Oblig where
  pprintTidy :: Tidy -> Oblig -> Doc
pprintTidy Tidy
_ = Oblig -> Doc
ppOblig

ppOblig :: Oblig -> Doc
ppOblig :: Oblig -> Doc
ppOblig Oblig
OCons = FilePath -> Doc
text FilePath
"Constraint Check"
ppOblig Oblig
OTerm = FilePath -> Doc
text FilePath
"Termination Check"
ppOblig Oblig
OInv  = FilePath -> Doc
text FilePath
"Invariant Check"

--------------------------------------------------------------------------------
-- | Generic Type for Error Messages -------------------------------------------
--------------------------------------------------------------------------------

-- | INVARIANT : all Error constructors should have a pos field

data TError t =
    ErrSubType { forall t. TError t -> SrcSpan
pos  :: !SrcSpan
               , forall t. TError t -> Doc
msg  :: !Doc
               , forall t. TError t -> Maybe SubcId
cid  :: Maybe SubcId
               , forall t. TError t -> HashMap Symbol t
ctx  :: !(M.HashMap Symbol t)
               , forall t. TError t -> t
tact :: !t
               , forall t. TError t -> t
texp :: !t
               } -- ^ liquid type error

  | ErrSubTypeModel
               { pos  :: !SrcSpan
               , msg  :: !Doc
               , cid  :: Maybe SubcId
               , forall t. TError t -> HashMap Symbol (WithModel t)
ctxM  :: !(M.HashMap Symbol (WithModel t))
               , forall t. TError t -> WithModel t
tactM :: !(WithModel t)
               , texp :: !t
               } -- ^ liquid type error with a counter-example

  | ErrFCrash  { pos  :: !SrcSpan
               , msg  :: !Doc
               , ctx  :: !(M.HashMap Symbol t)
               , tact :: !t
               , texp :: !t
               } -- ^ liquid type error

  | ErrHole    { pos  :: !SrcSpan
               , msg  :: !Doc
               , ctx  :: !(M.HashMap Symbol t)
               , forall t. TError t -> Symbol
svar :: !Symbol
               , forall t. TError t -> t
thl  :: !t
               } -- ^ hole type

  | ErrHoleCycle
               { pos  :: !SrcSpan
               , forall t. TError t -> [Symbol]
holesCycle :: [Symbol] -- Var?
               } -- ^ hole dependencies form a cycle error

  | ErrAssType { pos  :: !SrcSpan
               , forall t. TError t -> Oblig
obl  :: !Oblig
               , msg  :: !Doc
               , ctx  :: !(M.HashMap Symbol t)
               , forall t. TError t -> t
cond :: t
               } -- ^ condition failure error

  | ErrParse    { pos  :: !SrcSpan
                , msg  :: !Doc
                , forall t. TError t -> ParseError
pErr :: !ParseError
                } -- ^ specification parse error

  | ErrTySpec   { pos :: !SrcSpan
                , forall t. TError t -> Maybe Doc
knd :: !(Maybe Doc)
                , forall t. TError t -> Doc
var :: !Doc
                , forall t. TError t -> t
typ :: !t
                , msg :: !Doc
                } -- ^ sort error in specification

  | ErrTermSpec { pos  :: !SrcSpan
                , var  :: !Doc
                , msg  :: !Doc
                , forall t. TError t -> Expr
exp  :: !Expr
                , typ  :: !t
                , forall t. TError t -> Doc
msg' :: !Doc
                } -- ^ sort error in specification

  | ErrDupAlias { pos  :: !SrcSpan
                , var  :: !Doc
                , forall t. TError t -> Doc
kind :: !Doc
                , forall t. TError t -> [SrcSpan]
locs :: ![SrcSpan]
                } -- ^ multiple alias with same name error

  | ErrDupSpecs { pos :: !SrcSpan
                , var :: !Doc
                , locs:: ![SrcSpan]
                } -- ^ multiple specs for same binder error

  | ErrDupIMeas { pos   :: !SrcSpan
                , var   :: !Doc
                , forall t. TError t -> Doc
tycon :: !Doc
                , locs  :: ![SrcSpan]
                } -- ^ multiple definitions of the same instance measure

  | ErrDupMeas  { pos   :: !SrcSpan
                , var   :: !Doc
                , locs  :: ![SrcSpan]
                } -- ^ multiple definitions of the same measure

  | ErrDupField { pos   :: !SrcSpan
                , forall t. TError t -> Doc
dcon  :: !Doc
                , forall t. TError t -> Doc
field :: !Doc
                } -- ^ duplicate fields in same datacon

  | ErrDupNames { pos   :: !SrcSpan
                , var   :: !Doc
                , forall t. TError t -> [Doc]
names :: ![Doc]
                } -- ^ name resolves to multiple possible GHC vars

  | ErrBadData  { pos :: !SrcSpan
                , var :: !Doc
                , msg :: !Doc
                } -- ^ bad data type specification (?)

  | ErrDataCon  { pos :: !SrcSpan
                , var :: !Doc
                , msg :: !Doc
                } -- ^ refined datacon mismatches haskell datacon

  | ErrDataConMismatch
                { pos  :: !SrcSpan
                , var  :: !Doc
                , forall t. TError t -> [Doc]
dcs  :: [Doc]
                , forall t. TError t -> [Doc]
rdcs :: [Doc]
                } -- ^ constructors in refinement do not match original datatype

  | ErrInvt     { pos :: !SrcSpan
                , forall t. TError t -> t
inv :: !t
                , msg :: !Doc
                } -- ^ Invariant sort error

  | ErrIAl      { pos :: !SrcSpan
                , inv :: !t
                , msg :: !Doc
                } -- ^ Using  sort error

  | ErrIAlMis   { pos :: !SrcSpan
                , forall t. TError t -> t
tAs :: !t
                , forall t. TError t -> t
tUs :: !t
                , msg :: !Doc
                } -- ^ Incompatible using error

  | ErrMeas     { pos :: !SrcSpan
                , forall t. TError t -> Doc
ms  :: !Doc
                , msg :: !Doc
                } -- ^ Measure sort error

  | ErrHMeas    { pos :: !SrcSpan
                , ms  :: !Doc
                , msg :: !Doc
                } -- ^ Haskell bad Measure error

  | ErrUnbound  { pos :: !SrcSpan
                , var :: !Doc
                } -- ^ Unbound symbol in specification

  | ErrUnbPred  { pos :: !SrcSpan
                , var :: !Doc
                } -- ^ Unbound predicate being applied

  | ErrGhc      { pos :: !SrcSpan
                , msg :: !Doc
                } -- ^ GHC error: parsing or type checking

  | ErrResolve  { pos  :: !SrcSpan
                , kind :: !Doc
                , var  :: !Doc
                , msg  :: !Doc
                } -- ^ Name resolution error

  | ErrMismatch { pos   :: !SrcSpan -- ^ haskell type location
                , var   :: !Doc
                , msg   :: !Doc
                , forall t. TError t -> Doc
hs    :: !Doc
                , forall t. TError t -> Doc
lqTy  :: !Doc
                , forall t. TError t -> Maybe (Doc, Doc)
diff  :: !(Maybe (Doc, Doc))  -- ^ specific pair of things that mismatch
                , forall t. TError t -> SrcSpan
lqPos :: !SrcSpan -- ^ lq type location
                } -- ^ Mismatch between Liquid and Haskell types

  | ErrPartPred { pos  :: !SrcSpan
                , forall t. TError t -> Doc
ectr :: !Doc
                , var  :: !Doc
                , forall t. TError t -> Int
argN :: !Int
                , forall t. TError t -> Int
expN :: !Int
                , forall t. TError t -> Int
actN :: !Int
                } -- ^ Mismatch in expected/actual args of abstract refinement

  | ErrAliasCycle { pos    :: !SrcSpan
                  , forall t. TError t -> [(SrcSpan, Doc)]
acycle :: ![(SrcSpan, Doc)]
                  } -- ^ Cyclic Refined Type Alias Definitions

  | ErrIllegalAliasApp { pos   :: !SrcSpan
                       , forall t. TError t -> Doc
dname :: !Doc
                       , forall t. TError t -> SrcSpan
dpos  :: !SrcSpan
                       } -- ^ Illegal RTAlias application (from BSort, eg. in PVar)

  | ErrAliasApp { pos   :: !SrcSpan
                , dname :: !Doc
                , dpos  :: !SrcSpan
                , msg   :: !Doc
                }

  | ErrTermin   { pos  :: !SrcSpan
                , forall t. TError t -> [Doc]
bind :: ![Doc]
                , msg  :: !Doc
                } -- ^ Termination Error

  | ErrStTerm   { pos  :: !SrcSpan
                , dname :: !Doc
                , msg  :: !Doc
                } -- ^ Termination Error

  | ErrILaw     { pos   :: !SrcSpan
                , forall t. TError t -> Doc
cname :: !Doc
                , forall t. TError t -> Doc
iname :: !Doc
                , msg   :: !Doc
                } -- ^ Instance Law Error

  | ErrRClass   { pos   :: !SrcSpan
                , forall t. TError t -> Doc
cls   :: !Doc
                , forall t. TError t -> [(SrcSpan, Doc)]
insts :: ![(SrcSpan, Doc)]
                } -- ^ Refined Class/Interfaces Conflict

  | ErrMClass   { pos   :: !SrcSpan
                , var   :: !Doc
                } -- ^ Standalone class method refinements

  | ErrBadQual  { pos   :: !SrcSpan
                , forall t. TError t -> Doc
qname :: !Doc
                , msg   :: !Doc
                } -- ^ Non well sorted Qualifier

  | ErrSaved    { pos :: !SrcSpan
                , forall t. TError t -> Doc
nam :: !Doc
                , msg :: !Doc
                } -- ^ Previously saved error, that carries over after DiffCheck

  | ErrFilePragma { pos :: !SrcSpan
                  }

  | ErrTyCon    { pos    :: !SrcSpan
                , msg    :: !Doc
                , forall t. TError t -> Doc
tcname :: !Doc
                }

  | ErrLiftExp  { pos    :: !SrcSpan
                , msg    :: !Doc
                }

  | ErrParseAnn { pos :: !SrcSpan
                , msg :: !Doc
                }

  | ErrNoSpec   { pos  :: !SrcSpan
                , forall t. TError t -> Doc
srcF :: !Doc
                , forall t. TError t -> Doc
bspF :: !Doc
                }

  | ErrFail     { pos :: !SrcSpan
                , var :: !Doc
                }

  | ErrFailUsed { pos     :: !SrcSpan
                , var     :: !Doc
                , forall t. TError t -> [Doc]
clients :: ![Doc]
                }

  | ErrRewrite  { pos :: !SrcSpan
                , msg :: !Doc
                }

  | ErrPosTyCon { pos  :: SrcSpan
                , forall t. TError t -> Doc
tc   :: !Doc
                , forall t. TError t -> Doc
dc   :: !Doc
                }


  | ErrOther    { pos   :: SrcSpan
                , msg   :: !Doc
                } -- ^ Sigh. Other.

  deriving (Typeable, forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall t x. Rep (TError t) x -> TError t
forall t x. TError t -> Rep (TError t) x
$cto :: forall t x. Rep (TError t) x -> TError t
$cfrom :: forall t x. TError t -> Rep (TError t) x
Generic , forall a b. a -> TError b -> TError a
forall a b. (a -> b) -> TError a -> TError b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> TError b -> TError a
$c<$ :: forall a b. a -> TError b -> TError a
fmap :: forall a b. (a -> b) -> TError a -> TError b
$cfmap :: forall a b. (a -> b) -> TError a -> TError b
Functor )

errDupSpecs :: Doc -> Misc.ListNE SrcSpan -> TError t
errDupSpecs :: forall t. Doc -> [SrcSpan] -> TError t
errDupSpecs Doc
d spans :: [SrcSpan]
spans@(SrcSpan
sp:[SrcSpan]
_) = forall t. SrcSpan -> Doc -> [SrcSpan] -> TError t
ErrDupSpecs SrcSpan
sp Doc
d [SrcSpan]
spans
errDupSpecs Doc
_ [SrcSpan]
_            = forall a. Maybe SrcSpan -> FilePath -> a
impossible forall a. Maybe a
Nothing FilePath
"errDupSpecs with empty spans!"

-- FIXME ES: this is very suspicious, why can't we have multiple errors
-- arising from the same span?

instance Eq (TError a) where
  TError a
e1 == :: TError a -> TError a -> Bool
== TError a
e2 = forall t. TError t -> SrcSpan
errSpan TError a
e1 forall a. Eq a => a -> a -> Bool
== forall t. TError t -> SrcSpan
errSpan TError a
e2

errSpan :: TError a -> SrcSpan
errSpan :: forall t. TError t -> SrcSpan
errSpan =  forall t. TError t -> SrcSpan
pos

--------------------------------------------------------------------------------
-- | Simple unstructured type for panic ----------------------------------------
--------------------------------------------------------------------------------
type UserError  = TError Doc

instance PPrint UserError where
  pprintTidy :: Tidy -> UserError -> Doc
pprintTidy Tidy
k = forall a. (PPrint a, Show a) => Tidy -> Doc -> TError a -> Doc
ppError Tidy
k Doc
empty forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
Lossy)

data WithModel t
  = NoModel t
  | WithModel !Doc t
  deriving (forall a b. a -> WithModel b -> WithModel a
forall a b. (a -> b) -> WithModel a -> WithModel b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> WithModel b -> WithModel a
$c<$ :: forall a b. a -> WithModel b -> WithModel a
fmap :: forall a b. (a -> b) -> WithModel a -> WithModel b
$cfmap :: forall a b. (a -> b) -> WithModel a -> WithModel b
Functor, Int -> WithModel t -> ShowS
forall t. Show t => Int -> WithModel t -> ShowS
forall t. Show t => [WithModel t] -> ShowS
forall t. Show t => WithModel t -> FilePath
forall a.
(Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
showList :: [WithModel t] -> ShowS
$cshowList :: forall t. Show t => [WithModel t] -> ShowS
show :: WithModel t -> FilePath
$cshow :: forall t. Show t => WithModel t -> FilePath
showsPrec :: Int -> WithModel t -> ShowS
$cshowsPrec :: forall t. Show t => Int -> WithModel t -> ShowS
Show, WithModel t -> WithModel t -> Bool
forall t. Eq t => WithModel t -> WithModel t -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: WithModel t -> WithModel t -> Bool
$c/= :: forall t. Eq t => WithModel t -> WithModel t -> Bool
== :: WithModel t -> WithModel t -> Bool
$c== :: forall t. Eq t => WithModel t -> WithModel t -> Bool
Eq, forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall t x. Rep (WithModel t) x -> WithModel t
forall t x. WithModel t -> Rep (WithModel t) x
$cto :: forall t x. Rep (WithModel t) x -> WithModel t
$cfrom :: forall t x. WithModel t -> Rep (WithModel t) x
Generic)

instance NFData t => NFData (WithModel t)

dropModel :: WithModel t -> t
dropModel :: forall t. WithModel t -> t
dropModel WithModel t
m = case WithModel t
m of
  NoModel t
t     -> t
t
  WithModel Doc
_ t
t -> t
t

instance PPrint SrcSpan where
  pprintTidy :: Tidy -> SrcSpan -> Doc
pprintTidy Tidy
_ = SrcSpan -> Doc
pprSrcSpan

pprSrcSpan :: SrcSpan -> Doc
pprSrcSpan :: SrcSpan -> Doc
pprSrcSpan (UnhelpfulSpan UnhelpfulSpanReason
reason) = FilePath -> Doc
text forall a b. (a -> b) -> a -> b
$ case UnhelpfulSpanReason
reason of
  UnhelpfulSpanReason
UnhelpfulNoLocationInfo -> FilePath
"UnhelpfulNoLocationInfo"
  UnhelpfulSpanReason
UnhelpfulWiredIn        -> FilePath
"UnhelpfulWiredIn"
  UnhelpfulSpanReason
UnhelpfulInteractive    -> FilePath
"UnhelpfulInteractive"
  UnhelpfulSpanReason
UnhelpfulGenerated      -> FilePath
"UnhelpfulGenerated"
  UnhelpfulOther FastString
fs       -> FastString -> FilePath
unpackFS FastString
fs
pprSrcSpan (RealSrcSpan RealSrcSpan
s Maybe BufSpan
_)      = RealSrcSpan -> Doc
pprRealSrcSpan RealSrcSpan
s

pprRealSrcSpan :: RealSrcSpan -> Doc
pprRealSrcSpan :: RealSrcSpan -> Doc
pprRealSrcSpan RealSrcSpan
span
  | Int
sline forall a. Eq a => a -> a -> Bool
== Int
eline Bool -> Bool -> Bool
&& Int
scol forall a. Eq a => a -> a -> Bool
== Int
ecol =
    [Doc] -> Doc
hcat [ Doc
pathDoc Doc -> Doc -> Doc
<-> Doc
colon
         , Int -> Doc
int Int
sline Doc -> Doc -> Doc
<-> Doc
colon
         , Int -> Doc
int Int
scol
         ]
  | Int
sline forall a. Eq a => a -> a -> Bool
== Int
eline =
    [Doc] -> Doc
hcat forall a b. (a -> b) -> a -> b
$ [ Doc
pathDoc Doc -> Doc -> Doc
<-> Doc
colon
           , Int -> Doc
int Int
sline Doc -> Doc -> Doc
<-> Doc
colon
           , Int -> Doc
int Int
scol
           ] forall a. [a] -> [a] -> [a]
++ [Char -> Doc
char Char
'-' Doc -> Doc -> Doc
<-> Int -> Doc
int (Int
ecol forall a. Num a => a -> a -> a
- Int
1) | (Int
ecol forall a. Num a => a -> a -> a
- Int
scol) forall a. Ord a => a -> a -> Bool
> Int
1]
  | Bool
otherwise =
    [Doc] -> Doc
hcat [ Doc
pathDoc Doc -> Doc -> Doc
<-> Doc
colon
         , Doc -> Doc
parens (Int -> Doc
int Int
sline Doc -> Doc -> Doc
<-> Doc
comma Doc -> Doc -> Doc
<-> Int -> Doc
int Int
scol)
         , Char -> Doc
char Char
'-'
         , Doc -> Doc
parens (Int -> Doc
int Int
eline Doc -> Doc -> Doc
<-> Doc
comma Doc -> Doc -> Doc
<-> Int -> Doc
int Int
ecol')
         ]
 where
   path :: FastString
path  = RealSrcSpan -> FastString
srcSpanFile      RealSrcSpan
span
   sline :: Int
sline = RealSrcSpan -> Int
srcSpanStartLine RealSrcSpan
span
   eline :: Int
eline = RealSrcSpan -> Int
srcSpanEndLine   RealSrcSpan
span
   scol :: Int
scol  = RealSrcSpan -> Int
srcSpanStartCol  RealSrcSpan
span
   ecol :: Int
ecol  = RealSrcSpan -> Int
srcSpanEndCol    RealSrcSpan
span

   pathDoc :: Doc
pathDoc = FilePath -> Doc
text forall a b. (a -> b) -> a -> b
$ ShowS
normalise forall a b. (a -> b) -> a -> b
$ FastString -> FilePath
unpackFS FastString
path
   ecol' :: Int
ecol'   = if Int
ecol forall a. Eq a => a -> a -> Bool
== Int
0 then Int
ecol else Int
ecol forall a. Num a => a -> a -> a
- Int
1

instance Show UserError where
  show :: UserError -> FilePath
show = forall a. PPrint a => a -> FilePath
showpp

instance Ex.Exception UserError

-- | Construct and show an Error, then crash
uError :: UserError -> a
uError :: forall a. UserError -> a
uError = forall a e. Exception e => e -> a
Ex.throw

-- | Construct and show an Error, then crash
panicDoc :: {- (?callStack :: CallStack) => -} SrcSpan -> Doc -> a
panicDoc :: forall a. SrcSpan -> Doc -> a
panicDoc SrcSpan
sp Doc
d = forall a e. Exception e => e -> a
Ex.throw (forall t. SrcSpan -> Doc -> TError t
ErrOther SrcSpan
sp Doc
d :: UserError)

-- | Construct and show an Error, then crash
panic :: {- (?callStack :: CallStack) => -} Maybe SrcSpan -> String -> a
panic :: forall a. Maybe SrcSpan -> FilePath -> a
panic Maybe SrcSpan
sp FilePath
d = forall a. SrcSpan -> Doc -> a
panicDoc (Maybe SrcSpan -> SrcSpan
sspan Maybe SrcSpan
sp) (FilePath -> Doc
text FilePath
d)
  where
    sspan :: Maybe SrcSpan -> SrcSpan
sspan  = forall a. a -> Maybe a -> a
Mb.fromMaybe SrcSpan
noSrcSpan

-- | Construct and show an Error with an optional SrcSpan, then crash
--   This function should be used to mark unimplemented functionality
todo :: {- (?callStack :: CallStack) => -} Maybe SrcSpan -> String -> a
todo :: forall a. Maybe SrcSpan -> FilePath -> a
todo Maybe SrcSpan
s FilePath
m  = forall a. Maybe SrcSpan -> FilePath -> a
panic Maybe SrcSpan
s forall a b. (a -> b) -> a -> b
$ [FilePath] -> FilePath
unlines
            [ FilePath
"This functionality is currently unimplemented. "
            , FilePath
"If this functionality is critical to you, please contact us at: "
            , FilePath
"https://github.com/ucsd-progsys/liquidhaskell/issues"
            , FilePath
m
            ]

-- | Construct and show an Error with an optional SrcSpan, then crash
--   This function should be used to mark impossible-to-reach codepaths
impossible :: {- (?callStack :: CallStack) => -} Maybe SrcSpan -> String -> a
impossible :: forall a. Maybe SrcSpan -> FilePath -> a
impossible Maybe SrcSpan
s FilePath
m = forall a. Maybe SrcSpan -> FilePath -> a
panic Maybe SrcSpan
s forall a b. (a -> b) -> a -> b
$ [FilePath] -> FilePath
unlines [FilePath]
msg forall a. [a] -> [a] -> [a]
++ FilePath
m
   where
      msg :: [FilePath]
msg = [ FilePath
"This should never happen! If you are seeing this message, "
            , FilePath
"please submit a bug report at "
            , FilePath
"https://github.com/ucsd-progsys/liquidhaskell/issues "
            , FilePath
"with this message and the source file that caused this error."
            , FilePath
""
            ]



-- type CtxError = Error
--------------------------------------------------------------------------------
ppError :: (PPrint a, Show a) => Tidy -> Doc -> TError a -> Doc
--------------------------------------------------------------------------------
ppError :: forall a. (PPrint a, Show a) => Tidy -> Doc -> TError a -> Doc
ppError Tidy
k Doc
dCtx TError a
e = forall a. (PPrint a, Show a) => Tidy -> Doc -> TError a -> Doc
ppError' Tidy
k Doc
dCtx TError a
e

nests :: Int -> [Doc] -> Doc
nests :: Int -> [Doc] -> Doc
nests Int
n = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\Doc
d Doc
acc ->  Doc
d Doc -> Doc -> Doc
$+$ Int -> Doc -> Doc
nest Int
n Doc
acc) Doc
empty
-- nests n = foldr (\d acc -> nest n (d $+$ acc)) empty

sepVcat :: Doc -> [Doc] -> Doc
sepVcat :: Doc -> [Doc] -> Doc
sepVcat Doc
d [Doc]
ds = [Doc] -> Doc
vcat forall a b. (a -> b) -> a -> b
$ forall a. a -> [a] -> [a]
L.intersperse Doc
d [Doc]
ds

blankLine :: Doc
blankLine :: Doc
blankLine = Int -> FilePath -> Doc
sizedText Int
5 FilePath
"."

ppFull :: Tidy -> Doc -> Doc
ppFull :: Tidy -> Doc -> Doc
ppFull Tidy
Full  Doc
d = Doc
d
ppFull Tidy
Lossy Doc
_ = Doc
empty

ppReqInContext :: PPrint t => Tidy -> t -> t -> M.HashMap Symbol t -> Doc
ppReqInContext :: forall t. PPrint t => Tidy -> t -> t -> HashMap Symbol t -> Doc
ppReqInContext Tidy
td t
tA t
tE HashMap Symbol t
c
  = Doc -> [Doc] -> Doc
sepVcat Doc
blankLine
      [ Int -> [Doc] -> Doc
nests Int
2 [ FilePath -> Doc
text FilePath
"The inferred type"
                , FilePath -> Doc
text FilePath
"VV :" Doc -> Doc -> Doc
<+> forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
td t
tA]
      , Int -> [Doc] -> Doc
nests Int
2 [ FilePath -> Doc
text FilePath
"is not a subtype of the required type"
                , FilePath -> Doc
text FilePath
"VV :" Doc -> Doc -> Doc
<+> forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
td t
tE]
      , forall t. PPrint t => Tidy -> HashMap Symbol t -> Doc
ppContext Tidy
td HashMap Symbol t
c
      ]

ppContext :: PPrint t => Tidy -> M.HashMap Symbol t -> Doc
ppContext :: forall t. PPrint t => Tidy -> HashMap Symbol t -> Doc
ppContext Tidy
td HashMap Symbol t
c
  | Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Symbol, t)]
xts) = Int -> [Doc] -> Doc
nests Int
2 [ FilePath -> Doc
text FilePath
"in the context"
                             , [Doc] -> Doc
vsep (forall a b. (a -> b) -> [a] -> [b]
map (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (forall t. PPrint t => Tidy -> Symbol -> t -> Doc
pprintBind Tidy
td)) [(Symbol, t)]
xts)
                             ]
  | Bool
otherwise      = Doc
empty
  where
    xts :: [(Symbol, t)]
xts            = forall k v. HashMap k v -> [(k, v)]
M.toList HashMap Symbol t
c

pprintBind :: PPrint t => Tidy -> Symbol -> t -> Doc
pprintBind :: forall t. PPrint t => Tidy -> Symbol -> t -> Doc
pprintBind Tidy
td Symbol
v t
t = forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
td Symbol
v Doc -> Doc -> Doc
<+> Char -> Doc
char Char
':' Doc -> Doc -> Doc
<+> forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
td t
t

ppReqModelInContext
  :: (PPrint t) => Tidy -> WithModel t -> t -> M.HashMap Symbol (WithModel t) -> Doc
ppReqModelInContext :: forall t.
PPrint t =>
Tidy -> WithModel t -> t -> HashMap Symbol (WithModel t) -> Doc
ppReqModelInContext Tidy
td WithModel t
tA t
tE HashMap Symbol (WithModel t)
c
  = Doc -> [Doc] -> Doc
sepVcat Doc
blankLine
      [ Int -> [Doc] -> Doc
nests Int
2 [ FilePath -> Doc
text FilePath
"The inferred type"
                , forall t. PPrint t => Tidy -> Symbol -> WithModel t -> Doc
pprintModel Tidy
td Symbol
"VV" WithModel t
tA]
      , Int -> [Doc] -> Doc
nests Int
2 [ FilePath -> Doc
text FilePath
"is not a subtype of the required type"
                , forall t. PPrint t => Tidy -> Symbol -> WithModel t -> Doc
pprintModel Tidy
td Symbol
"VV" (forall t. t -> WithModel t
NoModel t
tE)]
      , Int -> [Doc] -> Doc
nests Int
2 [ FilePath -> Doc
text FilePath
"in the context"
                , [Doc] -> Doc
vsep (forall a b. (a -> b) -> [a] -> [b]
map (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (forall t. PPrint t => Tidy -> Symbol -> WithModel t -> Doc
pprintModel Tidy
td)) (forall k v. HashMap k v -> [(k, v)]
M.toList HashMap Symbol (WithModel t)
c))
                ]
      ]

vsep :: [Doc] -> Doc
vsep :: [Doc] -> Doc
vsep = [Doc] -> Doc
vcat forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> [a] -> [a]
L.intersperse (Char -> Doc
char Char
' ')

pprintModel :: PPrint t => Tidy -> Symbol -> WithModel t -> Doc
pprintModel :: forall t. PPrint t => Tidy -> Symbol -> WithModel t -> Doc
pprintModel Tidy
td Symbol
v WithModel t
wm = case WithModel t
wm of
  NoModel t
t
    -> forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
td Symbol
v Doc -> Doc -> Doc
<+> Char -> Doc
char Char
':' Doc -> Doc -> Doc
<+> forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
td t
t
  WithModel Doc
m t
t
    -> forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
td Symbol
v Doc -> Doc -> Doc
<+> Char -> Doc
char Char
':' Doc -> Doc -> Doc
<+> forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
td t
t Doc -> Doc -> Doc
$+$
       forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
td Symbol
v Doc -> Doc -> Doc
<+> Char -> Doc
char Char
'=' Doc -> Doc -> Doc
<+> forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
td Doc
m

ppPropInContext :: (PPrint p, PPrint c) => Tidy -> p -> c -> Doc
ppPropInContext :: forall p c. (PPrint p, PPrint c) => Tidy -> p -> c -> Doc
ppPropInContext Tidy
td p
p c
c
  = Doc -> [Doc] -> Doc
sepVcat Doc
blankLine
      [ Int -> [Doc] -> Doc
nests Int
2 [ FilePath -> Doc
text FilePath
"Property"
                , forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
td p
p]
      , Int -> [Doc] -> Doc
nests Int
2 [ FilePath -> Doc
text FilePath
"Not provable in context"
                , forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
td c
c
                ]
      ]

instance ToJSON RealSrcSpan where
  toJSON :: RealSrcSpan -> Value
toJSON RealSrcSpan
sp = [Pair] -> Value
object [ Key
"filename"  forall kv v. (KeyValue kv, ToJSON v) => Key -> v -> kv
.= FilePath
f
                     , Key
"startLine" forall kv v. (KeyValue kv, ToJSON v) => Key -> v -> kv
.= Int
l1
                     , Key
"startCol"  forall kv v. (KeyValue kv, ToJSON v) => Key -> v -> kv
.= Int
c1
                     , Key
"endLine"   forall kv v. (KeyValue kv, ToJSON v) => Key -> v -> kv
.= Int
l2
                     , Key
"endCol"    forall kv v. (KeyValue kv, ToJSON v) => Key -> v -> kv
.= Int
c2
                     ]
    where
      (FilePath
f, Int
l1, Int
c1, Int
l2, Int
c2) = RealSrcSpan -> (FilePath, Int, Int, Int, Int)
unpackRealSrcSpan RealSrcSpan
sp

unpackRealSrcSpan :: RealSrcSpan -> (String, Int, Int, Int, Int)
unpackRealSrcSpan :: RealSrcSpan -> (FilePath, Int, Int, Int, Int)
unpackRealSrcSpan RealSrcSpan
rsp = (FilePath
f, Int
l1, Int
c1, Int
l2, Int
c2)
  where
    f :: FilePath
f                 = FastString -> FilePath
unpackFS forall a b. (a -> b) -> a -> b
$ RealSrcSpan -> FastString
srcSpanFile RealSrcSpan
rsp
    l1 :: Int
l1                = RealSrcSpan -> Int
srcSpanStartLine RealSrcSpan
rsp
    c1 :: Int
c1                = RealSrcSpan -> Int
srcSpanStartCol  RealSrcSpan
rsp
    l2 :: Int
l2                = RealSrcSpan -> Int
srcSpanEndLine   RealSrcSpan
rsp
    c2 :: Int
c2                = RealSrcSpan -> Int
srcSpanEndCol    RealSrcSpan
rsp


instance FromJSON RealSrcSpan where
  parseJSON :: Value -> Parser RealSrcSpan
parseJSON (Object Object
v) =
    FilePath -> Int -> Int -> Int -> Int -> RealSrcSpan
packRealSrcSpan
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Object
v forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"filename"
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Object
v forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"startLine"
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Object
v forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"startCol"
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Object
v forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"endLine"
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Object
v forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"endCol"
  parseJSON Value
_          = forall a. Monoid a => a
mempty

packRealSrcSpan :: FilePath -> Int -> Int -> Int -> Int -> RealSrcSpan
packRealSrcSpan :: FilePath -> Int -> Int -> Int -> Int -> RealSrcSpan
packRealSrcSpan FilePath
f Int
l1 Int
c1 Int
l2 Int
c2 = RealSrcLoc -> RealSrcLoc -> RealSrcSpan
mkRealSrcSpan RealSrcLoc
loc1 RealSrcLoc
loc2
  where
    loc1 :: RealSrcLoc
loc1                  = FastString -> Int -> Int -> RealSrcLoc
mkRealSrcLoc (FilePath -> FastString
fsLit FilePath
f) Int
l1 Int
c1
    loc2 :: RealSrcLoc
loc2                  = FastString -> Int -> Int -> RealSrcLoc
mkRealSrcLoc (FilePath -> FastString
fsLit FilePath
f) Int
l2 Int
c2

srcSpanFileMb :: SrcSpan -> Maybe FilePath
srcSpanFileMb :: SrcSpan -> Maybe FilePath
srcSpanFileMb (RealSrcSpan RealSrcSpan
s Maybe BufSpan
_) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ FastString -> FilePath
unpackFS forall a b. (a -> b) -> a -> b
$ RealSrcSpan -> FastString
srcSpanFile RealSrcSpan
s
srcSpanFileMb SrcSpan
_                 = forall a. Maybe a
Nothing


instance ToJSON SrcSpan where
  toJSON :: SrcSpan -> Value
toJSON (RealSrcSpan RealSrcSpan
rsp Maybe BufSpan
_) = [Pair] -> Value
object [ Key
"realSpan" forall kv v. (KeyValue kv, ToJSON v) => Key -> v -> kv
.= Bool
True, Key
"spanInfo" forall kv v. (KeyValue kv, ToJSON v) => Key -> v -> kv
.= RealSrcSpan
rsp ]
  toJSON (UnhelpfulSpan UnhelpfulSpanReason
_)   = [Pair] -> Value
object [ Key
"realSpan" forall kv v. (KeyValue kv, ToJSON v) => Key -> v -> kv
.= Bool
False ]

instance FromJSON SrcSpan where
  parseJSON :: Value -> Parser SrcSpan
parseJSON (Object Object
v) = do Bool
tag <- Object
v forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"realSpan"
                            if Bool
tag
                              then RealSrcSpan -> Maybe BufSpan -> SrcSpan
RealSrcSpan forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Object
v forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"spanInfo" forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Maybe a
Nothing
                              else forall (m :: * -> *) a. Monad m => a -> m a
return SrcSpan
noSrcSpan
  parseJSON Value
_          = forall a. Monoid a => a
mempty

-- Default definition use ToJSON and FromJSON
instance ToJSONKey SrcSpan
instance FromJSONKey SrcSpan

instance (PPrint a, Show a) => ToJSON (TError a) where
  toJSON :: TError a -> Value
toJSON TError a
e = [Pair] -> Value
object [ Key
"pos" forall kv v. (KeyValue kv, ToJSON v) => Key -> v -> kv
.= forall t. TError t -> SrcSpan
pos TError a
e
                    , Key
"msg" forall kv v. (KeyValue kv, ToJSON v) => Key -> v -> kv
.= Doc -> FilePath
render (forall a. (PPrint a, Show a) => Tidy -> Doc -> TError a -> Doc
ppError' Tidy
Full Doc
empty TError a
e)
                    ]

instance FromJSON (TError a) where
  parseJSON :: Value -> Parser (TError a)
parseJSON (Object Object
v) = forall a. SrcSpan -> FilePath -> TError a
errSaved forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Object
v forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"pos"
                                  forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Object
v forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"msg"
  parseJSON Value
_          = forall a. Monoid a => a
mempty

errSaved :: SrcSpan -> String -> TError a
errSaved :: forall a. SrcSpan -> FilePath -> TError a
errSaved SrcSpan
sp FilePath
body | FilePath
n : [FilePath]
m <- FilePath -> [FilePath]
lines FilePath
body = forall t. SrcSpan -> Doc -> Doc -> TError t
ErrSaved SrcSpan
sp (FilePath -> Doc
text FilePath
n) (FilePath -> Doc
text forall a b. (a -> b) -> a -> b
$ [FilePath] -> FilePath
unlines [FilePath]
m)

totalityType :: PPrint a =>  Tidy -> a -> Bool
totalityType :: forall a. PPrint a => Tidy -> a -> Bool
totalityType Tidy
td a
tE = forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
td a
tE forall a. Eq a => a -> a -> Bool
== FilePath -> Doc
text FilePath
"{VV : Addr# | 5 < 4}"

hint :: TError a -> Doc
hint :: forall t. TError t -> Doc
hint TError a
e = forall b a. b -> (a -> b) -> Maybe a -> b
maybe Doc
empty (\Doc
d -> Doc
"" Doc -> Doc -> Doc
$+$ (Doc
"HINT:" Doc -> Doc -> Doc
<+> Doc
d)) (forall {a} {t}. IsString a => TError t -> Maybe a
go TError a
e)
  where
    go :: TError t -> Maybe a
go ErrMismatch {} = forall a. a -> Maybe a
Just a
"Use the hole '_' instead of the mismatched component (in the Liquid specification)"
    go ErrSubType {}  = forall a. a -> Maybe a
Just a
"Use \"--no-totality\" to deactivate totality checking."
    go ErrNoSpec {}   = forall a. a -> Maybe a
Just a
"Run 'liquid' on the source file first."
    go TError t
_              = forall a. Maybe a
Nothing

--------------------------------------------------------------------------------
ppError' :: (PPrint a, Show a) => Tidy -> Doc -> TError a -> Doc
--------------------------------------------------------------------------------
ppError' :: forall a. (PPrint a, Show a) => Tidy -> Doc -> TError a -> Doc
ppError' Tidy
td Doc
dCtx (ErrAssType SrcSpan
_ Oblig
o Doc
_ HashMap Symbol a
c a
p)
  = forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
td Oblig
o
        Doc -> Doc -> Doc
$+$ Doc
dCtx
        Doc -> Doc -> Doc
$+$ Tidy -> Doc -> Doc
ppFull Tidy
td (forall p c. (PPrint p, PPrint c) => Tidy -> p -> c -> Doc
ppPropInContext Tidy
td a
p HashMap Symbol a
c)

ppError' Tidy
td Doc
dCtx err :: TError a
err@(ErrSubType SrcSpan
_ Doc
_ Maybe SubcId
_ HashMap Symbol a
_ a
_ a
tE)
  | forall a. PPrint a => Tidy -> a -> Bool
totalityType Tidy
td a
tE
  = FilePath -> Doc
text FilePath
"Totality Error"
        Doc -> Doc -> Doc
$+$ Doc
dCtx
        Doc -> Doc -> Doc
$+$ FilePath -> Doc
text FilePath
"Your function is not total: not all patterns are defined."
        Doc -> Doc -> Doc
$+$ forall t. TError t -> Doc
hint TError a
err -- "Hint: Use \"--no-totality\" to deactivate totality checking."

ppError' Tidy
_td Doc
_dCtx (ErrHoleCycle SrcSpan
_ [Symbol]
holes)
  = Doc
"Cycle of holes found"
        Doc -> Doc -> Doc
$+$ forall a. PPrint a => a -> Doc
pprint [Symbol]
holes

ppError' Tidy
_td Doc
_dCtx (ErrHole SrcSpan
_ Doc
msg HashMap Symbol a
_ Symbol
x a
t)
  = Doc
"Hole Found"
        Doc -> Doc -> Doc
$+$ forall a. PPrint a => a -> Doc
pprint Symbol
x Doc -> Doc -> Doc
<+> Doc
"::" Doc -> Doc -> Doc
<+> forall a. PPrint a => a -> Doc
pprint a
t
        Doc -> Doc -> Doc
$+$ Doc
msg

ppError' Tidy
td Doc
dCtx (ErrSubType SrcSpan
_ Doc
_ Maybe SubcId
cid HashMap Symbol a
c a
tA a
tE)
  = FilePath -> Doc
text FilePath
"Liquid Type Mismatch"
    Doc -> Doc -> Doc
$+$ Int -> Doc -> Doc
nest Int
4
          (Doc
blankLine
           Doc -> Doc -> Doc
$+$ Doc
dCtx
           Doc -> Doc -> Doc
$+$ Tidy -> Doc -> Doc
ppFull Tidy
td (forall t. PPrint t => Tidy -> t -> t -> HashMap Symbol t -> Doc
ppReqInContext Tidy
td a
tA a
tE HashMap Symbol a
c)
           Doc -> Doc -> Doc
$+$ forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. Monoid a => a
mempty (\SubcId
i -> FilePath -> Doc
text FilePath
"Constraint id" Doc -> Doc -> Doc
<+> FilePath -> Doc
text (forall a. Show a => a -> FilePath
show SubcId
i)) Maybe SubcId
cid)

ppError' Tidy
td Doc
dCtx (ErrSubTypeModel SrcSpan
_ Doc
_ Maybe SubcId
cid HashMap Symbol (WithModel a)
c WithModel a
tA a
tE)
  = FilePath -> Doc
text FilePath
"Liquid Type Mismatch"
    Doc -> Doc -> Doc
$+$ Int -> Doc -> Doc
nest Int
4
          (Doc
dCtx
          Doc -> Doc -> Doc
$+$ Tidy -> Doc -> Doc
ppFull Tidy
td (forall t.
PPrint t =>
Tidy -> WithModel t -> t -> HashMap Symbol (WithModel t) -> Doc
ppReqModelInContext Tidy
td WithModel a
tA a
tE HashMap Symbol (WithModel a)
c)
          Doc -> Doc -> Doc
$+$ forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. Monoid a => a
mempty (\SubcId
i -> FilePath -> Doc
text FilePath
"Constraint id" Doc -> Doc -> Doc
<+> FilePath -> Doc
text (forall a. Show a => a -> FilePath
show SubcId
i)) Maybe SubcId
cid)

ppError' Tidy
td  Doc
dCtx (ErrFCrash SrcSpan
_ Doc
_ HashMap Symbol a
c a
tA a
tE)
  = FilePath -> Doc
text FilePath
"Fixpoint Crash on Constraint"
        Doc -> Doc -> Doc
$+$ Doc
dCtx
        Doc -> Doc -> Doc
$+$ Tidy -> Doc -> Doc
ppFull Tidy
td (forall t. PPrint t => Tidy -> t -> t -> HashMap Symbol t -> Doc
ppReqInContext Tidy
td a
tA a
tE HashMap Symbol a
c)

ppError' Tidy
_ Doc
dCtx (ErrParse SrcSpan
_ Doc
_ ParseError
e)
  = FilePath -> Doc
text FilePath
"Cannot parse specification:"
        Doc -> Doc -> Doc
$+$ Doc
dCtx
        Doc -> Doc -> Doc
$+$ Int -> Doc -> Doc
nest Int
4 (forall a. PPrint a => a -> Doc
pprint ParseError
e)

ppError' Tidy
_ Doc
dCtx (ErrTySpec SrcSpan
_ Maybe Doc
_k Doc
v a
t Doc
s)
  = (Doc
"Illegal type specification for" Doc -> Doc -> Doc
<+> forall a. PPrint a => a -> Doc
ppTicks Doc
v) --  <-> ppKind k <-> ppTicks v)
  -- = dSp <+> ("Illegal type specification for" <+> _ppKind k <-> ppTicks v)
        Doc -> Doc -> Doc
$+$ Doc
dCtx
        Doc -> Doc -> Doc
$+$ Int -> Doc -> Doc
nest Int
4 ([Doc] -> Doc
vcat [ forall a. PPrint a => a -> Doc
pprint Doc
v Doc -> Doc -> Doc
<+> Doc
Misc.dcolon Doc -> Doc -> Doc
<+> forall a. PPrint a => a -> Doc
pprint a
t
                         , forall a. PPrint a => a -> Doc
pprint Doc
s
                         , forall a. PPrint a => a -> Doc
pprint Maybe Doc
_k
                         ])
    where
      _ppKind :: Maybe Doc -> Doc
_ppKind Maybe Doc
Nothing  = Doc
empty
      _ppKind (Just Doc
d) = Doc
d Doc -> Doc -> Doc
<-> Doc
" "

ppError' Tidy
_ Doc
dCtx (ErrLiftExp SrcSpan
_ Doc
v)
  = FilePath -> Doc
text FilePath
"Cannot lift" Doc -> Doc -> Doc
<+> forall a. PPrint a => a -> Doc
ppTicks Doc
v Doc -> Doc -> Doc
<+> Doc
"into refinement logic"
        Doc -> Doc -> Doc
$+$ Doc
dCtx
        Doc -> Doc -> Doc
$+$ Int -> Doc -> Doc
nest Int
4 (FilePath -> Doc
text FilePath
"Please export the binder from the module to enable lifting.")

ppError' Tidy
_ Doc
dCtx (ErrBadData SrcSpan
_ Doc
v Doc
s)
  = FilePath -> Doc
text FilePath
"Bad Data Specification"
        Doc -> Doc -> Doc
$+$ Doc
dCtx
        Doc -> Doc -> Doc
$+$ (forall a. PPrint a => a -> Doc
pprint Doc
s Doc -> Doc -> Doc
<+> Doc
"for" Doc -> Doc -> Doc
<+> forall a. PPrint a => a -> Doc
ppTicks Doc
v)

ppError' Tidy
_ Doc
dCtx (ErrDataCon SrcSpan
_ Doc
d Doc
s)
  = Doc
"Malformed refined data constructor" Doc -> Doc -> Doc
<+> forall a. PPrint a => a -> Doc
ppTicks Doc
d
        Doc -> Doc -> Doc
$+$ Doc
dCtx
        Doc -> Doc -> Doc
$+$ Doc
s

ppError' Tidy
_ Doc
dCtx (ErrDataConMismatch SrcSpan
_ Doc
d [Doc]
dcs [Doc]
rdcs)
  = FilePath -> Doc
text FilePath
"Data constructors in refinement do not match original datatype for" Doc -> Doc -> Doc
<+> forall a. PPrint a => a -> Doc
ppTicks Doc
d
        Doc -> Doc -> Doc
$+$ Doc
dCtx
        Doc -> Doc -> Doc
$+$ Int -> Doc -> Doc
nest Int
4 (FilePath -> Doc
text FilePath
"Constructors in Haskell declaration: " Doc -> Doc -> Doc
<+> [Doc] -> Doc
hsep (forall a. a -> [a] -> [a]
L.intersperse Doc
comma [Doc]
dcs))
        Doc -> Doc -> Doc
$+$ Int -> Doc -> Doc
nest Int
4 (FilePath -> Doc
text FilePath
"Constructors in refinement         : " Doc -> Doc -> Doc
<+> [Doc] -> Doc
hsep (forall a. a -> [a] -> [a]
L.intersperse Doc
comma [Doc]
rdcs))

ppError' Tidy
_ Doc
dCtx (ErrBadQual SrcSpan
_ Doc
n Doc
d)
  = FilePath -> Doc
text FilePath
"Illegal qualifier specification for" Doc -> Doc -> Doc
<+> forall a. PPrint a => a -> Doc
ppTicks Doc
n
        Doc -> Doc -> Doc
$+$ Doc
dCtx
        Doc -> Doc -> Doc
$+$ forall a. PPrint a => a -> Doc
pprint Doc
d

ppError' Tidy
_ Doc
dCtx (ErrTermSpec SrcSpan
_ Doc
v Doc
msg Expr
e a
t Doc
s)
  = FilePath -> Doc
text FilePath
"Illegal termination specification for" Doc -> Doc -> Doc
<+> forall a. PPrint a => a -> Doc
ppTicks Doc
v
        Doc -> Doc -> Doc
$+$ Doc
dCtx
        Doc -> Doc -> Doc
$+$ Int -> Doc -> Doc
nest Int
4 ((FilePath -> Doc
text FilePath
"Termination metric" Doc -> Doc -> Doc
<+> forall a. PPrint a => a -> Doc
ppTicks Expr
e Doc -> Doc -> Doc
<+> FilePath -> Doc
text FilePath
"is" Doc -> Doc -> Doc
<+> Doc
msg Doc -> Doc -> Doc
<+> Doc
"in type signature")
                     Doc -> Doc -> Doc
$+$ Int -> Doc -> Doc
nest Int
4 (forall a. PPrint a => a -> Doc
pprint a
t)
                     Doc -> Doc -> Doc
$+$ forall a. PPrint a => a -> Doc
pprint Doc
s)

ppError' Tidy
_ Doc
_ (ErrInvt SrcSpan
_ a
t Doc
s)
  = FilePath -> Doc
text FilePath
"Bad Invariant Specification"
        Doc -> Doc -> Doc
$+$ Int -> Doc -> Doc
nest Int
4 (FilePath -> Doc
text FilePath
"invariant " Doc -> Doc -> Doc
<+> forall a. PPrint a => a -> Doc
pprint a
t Doc -> Doc -> Doc
$+$ forall a. PPrint a => a -> Doc
pprint Doc
s)

ppError' Tidy
_ Doc
_ (ErrIAl SrcSpan
_ a
t Doc
s)
  = FilePath -> Doc
text FilePath
"Bad Using Specification"
        Doc -> Doc -> Doc
$+$ Int -> Doc -> Doc
nest Int
4 (FilePath -> Doc
text FilePath
"as" Doc -> Doc -> Doc
<+> forall a. PPrint a => a -> Doc
pprint a
t Doc -> Doc -> Doc
$+$ forall a. PPrint a => a -> Doc
pprint Doc
s)

ppError' Tidy
_ Doc
_ (ErrIAlMis SrcSpan
_ a
t1 a
t2 Doc
s)
  = FilePath -> Doc
text FilePath
"Incompatible Using Specification"
        Doc -> Doc -> Doc
$+$ Int -> Doc -> Doc
nest Int
4 ((FilePath -> Doc
text FilePath
"using" Doc -> Doc -> Doc
<+> forall a. PPrint a => a -> Doc
pprint a
t1 Doc -> Doc -> Doc
<+> FilePath -> Doc
text FilePath
"as" Doc -> Doc -> Doc
<+> forall a. PPrint a => a -> Doc
pprint a
t2) Doc -> Doc -> Doc
$+$ forall a. PPrint a => a -> Doc
pprint Doc
s)

ppError' Tidy
_ Doc
_ (ErrMeas SrcSpan
_ Doc
t Doc
s)
  = FilePath -> Doc
text FilePath
"Bad Measure Specification"
        Doc -> Doc -> Doc
$+$ Int -> Doc -> Doc
nest Int
4 (FilePath -> Doc
text FilePath
"measure " Doc -> Doc -> Doc
<+> forall a. PPrint a => a -> Doc
pprint Doc
t Doc -> Doc -> Doc
$+$ forall a. PPrint a => a -> Doc
pprint Doc
s)

ppError' Tidy
_ Doc
dCtx (ErrHMeas SrcSpan
_ Doc
t Doc
s)
  = FilePath -> Doc
text FilePath
"Cannot lift Haskell function" Doc -> Doc -> Doc
<+> forall a. PPrint a => a -> Doc
ppTicks Doc
t Doc -> Doc -> Doc
<+> FilePath -> Doc
text FilePath
"to logic"
        Doc -> Doc -> Doc
$+$ Doc
dCtx
        Doc -> Doc -> Doc
$+$ Int -> Doc -> Doc
nest Int
4 (forall a. PPrint a => a -> Doc
pprint Doc
s)

ppError' Tidy
_ Doc
dCtx (ErrDupSpecs SrcSpan
_ Doc
v [SrcSpan]
ls)
  = FilePath -> Doc
text FilePath
"Multiple specifications for" Doc -> Doc -> Doc
<+> forall a. PPrint a => a -> Doc
ppTicks Doc
v Doc -> Doc -> Doc
<+> Doc
colon
        Doc -> Doc -> Doc
$+$ Doc
dCtx
        Doc -> Doc -> Doc
$+$ [SrcSpan] -> Doc
ppSrcSpans [SrcSpan]
ls

ppError' Tidy
_ Doc
dCtx (ErrDupIMeas SrcSpan
_ Doc
v Doc
t [SrcSpan]
ls)
  = FilePath -> Doc
text FilePath
"Multiple instance measures" Doc -> Doc -> Doc
<+> forall a. PPrint a => a -> Doc
ppTicks Doc
v Doc -> Doc -> Doc
<+> FilePath -> Doc
text FilePath
"for type" Doc -> Doc -> Doc
<+> forall a. PPrint a => a -> Doc
ppTicks Doc
t
        Doc -> Doc -> Doc
$+$ Doc
dCtx
        Doc -> Doc -> Doc
$+$ [SrcSpan] -> Doc
ppSrcSpans [SrcSpan]
ls

ppError' Tidy
_ Doc
dCtx (ErrDupMeas SrcSpan
_ Doc
v [SrcSpan]
ls)
  = FilePath -> Doc
text FilePath
"Multiple measures named" Doc -> Doc -> Doc
<+> forall a. PPrint a => a -> Doc
ppTicks Doc
v
        Doc -> Doc -> Doc
$+$ Doc
dCtx
        Doc -> Doc -> Doc
$+$ [SrcSpan] -> Doc
ppSrcSpans [SrcSpan]
ls

ppError' Tidy
_ Doc
dCtx (ErrDupField SrcSpan
_ Doc
dc Doc
x)
  = FilePath -> Doc
text FilePath
"Malformed refined data constructor" Doc -> Doc -> Doc
<+> Doc
dc
        Doc -> Doc -> Doc
$+$ Doc
dCtx
        Doc -> Doc -> Doc
$+$ Int -> Doc -> Doc
nest Int
4 (FilePath -> Doc
text FilePath
"Duplicated definitions for field" Doc -> Doc -> Doc
<+> forall a. PPrint a => a -> Doc
ppTicks Doc
x)

ppError' Tidy
_ Doc
dCtx (ErrDupNames SrcSpan
_ Doc
x [Doc]
ns)
  = FilePath -> Doc
text FilePath
"Ambiguous specification symbol" Doc -> Doc -> Doc
<+> forall a. PPrint a => a -> Doc
ppTicks Doc
x
        Doc -> Doc -> Doc
$+$ Doc
dCtx
        Doc -> Doc -> Doc
$+$ [Doc] -> Doc
ppNames [Doc]
ns

ppError' Tidy
_ Doc
dCtx (ErrDupAlias SrcSpan
_ Doc
k Doc
v [SrcSpan]
ls)
  = FilePath -> Doc
text FilePath
"Multiple definitions of" Doc -> Doc -> Doc
<+> forall a. PPrint a => a -> Doc
pprint Doc
k Doc -> Doc -> Doc
<+> forall a. PPrint a => a -> Doc
ppTicks Doc
v
        Doc -> Doc -> Doc
$+$ Doc
dCtx
        Doc -> Doc -> Doc
$+$ [SrcSpan] -> Doc
ppSrcSpans [SrcSpan]
ls

ppError' Tidy
_ Doc
dCtx (ErrUnbound SrcSpan
_ Doc
x)
  = FilePath -> Doc
text FilePath
"Unbound variable" Doc -> Doc -> Doc
<+> forall a. PPrint a => a -> Doc
pprint Doc
x
        Doc -> Doc -> Doc
$+$ Doc
dCtx

ppError' Tidy
_ Doc
dCtx (ErrUnbPred SrcSpan
_ Doc
p)
  = FilePath -> Doc
text FilePath
"Cannot apply unbound abstract refinement" Doc -> Doc -> Doc
<+> forall a. PPrint a => a -> Doc
ppTicks Doc
p
        Doc -> Doc -> Doc
$+$ Doc
dCtx

ppError' Tidy
_ Doc
dCtx (ErrGhc SrcSpan
_ Doc
s)
  = FilePath -> Doc
text FilePath
"GHC Error"
        Doc -> Doc -> Doc
$+$ Doc
dCtx
        Doc -> Doc -> Doc
$+$ Int -> Doc -> Doc
nest Int
4 (forall a. PPrint a => a -> Doc
pprint Doc
s)

ppError' Tidy
_ Doc
_ (ErrFail SrcSpan
_ Doc
s)
  = FilePath -> Doc
text FilePath
"Failure Error:"
        Doc -> Doc -> Doc
$+$ FilePath -> Doc
text FilePath
"Definition of" Doc -> Doc -> Doc
<+> forall a. PPrint a => a -> Doc
pprint Doc
s Doc -> Doc -> Doc
<+> FilePath -> Doc
text FilePath
"declared to fail is safe."

ppError' Tidy
_ Doc
_ (ErrFailUsed SrcSpan
_ Doc
s [Doc]
xs)
  = FilePath -> Doc
text FilePath
"Failure Error:"
        Doc -> Doc -> Doc
$+$ FilePath -> Doc
text FilePath
"Binder" Doc -> Doc -> Doc
<+> forall a. PPrint a => a -> Doc
pprint Doc
s Doc -> Doc -> Doc
<+> FilePath -> Doc
text FilePath
"declared to fail is used by"
        Doc -> Doc -> Doc
<+> [Doc] -> Doc
hsep (forall a. a -> [a] -> [a]
L.intersperse Doc
comma [Doc]
xs)

ppError' Tidy
_ Doc
dCtx (ErrResolve SrcSpan
_ Doc
kind Doc
v Doc
msg)
  = (FilePath -> Doc
text FilePath
"Unknown" Doc -> Doc -> Doc
<+> Doc
kind Doc -> Doc -> Doc
<+> forall a. PPrint a => a -> Doc
ppTicks Doc
v)
        Doc -> Doc -> Doc
$+$ Doc
dCtx
        Doc -> Doc -> Doc
$+$ Int -> Doc -> Doc
nest Int
4 Doc
msg

ppError' Tidy
_ Doc
dCtx (ErrPartPred SrcSpan
_ Doc
c Doc
p Int
i Int
eN Int
aN)
  = FilePath -> Doc
text FilePath
"Malformed predicate application"
        Doc -> Doc -> Doc
$+$ Doc
dCtx
        Doc -> Doc -> Doc
$+$ Int -> Doc -> Doc
nest Int
4 ([Doc] -> Doc
vcat
                        [ Doc
"The" Doc -> Doc -> Doc
<+> FilePath -> Doc
text (Int -> FilePath
Misc.intToString Int
i) Doc -> Doc -> Doc
<+> Doc
"argument of" Doc -> Doc -> Doc
<+> Doc
c Doc -> Doc -> Doc
<+> Doc
"is predicate" Doc -> Doc -> Doc
<+> forall a. PPrint a => a -> Doc
ppTicks Doc
p
                        , Doc
"which expects" Doc -> Doc -> Doc
<+> forall a. PPrint a => a -> Doc
pprint Int
eN Doc -> Doc -> Doc
<+> Doc
"arguments" Doc -> Doc -> Doc
<+> Doc
"but is given only" Doc -> Doc -> Doc
<+> forall a. PPrint a => a -> Doc
pprint Int
aN
                        , Doc
" "
                        , Doc
"Abstract predicates cannot be partially applied; for a possible fix see:"
                        , Doc
" "
                        , Int -> Doc -> Doc
nest Int
4 Doc
"https://github.com/ucsd-progsys/liquidhaskell/issues/594"
                        ])

ppError' Tidy
_ Doc
dCtx e :: TError a
e@(ErrMismatch SrcSpan
_ Doc
x Doc
msg Doc
τ Doc
t Maybe (Doc, Doc)
cause SrcSpan
hsSp)
  = Doc
"Specified type does not refine Haskell type for" Doc -> Doc -> Doc
<+> forall a. PPrint a => a -> Doc
ppTicks Doc
x Doc -> Doc -> Doc
<+> Doc -> Doc
parens Doc
msg
        Doc -> Doc -> Doc
$+$ Doc
dCtx
        Doc -> Doc -> Doc
$+$ Doc -> [Doc] -> Doc
sepVcat Doc
blankLine
              [ Doc
"The Liquid type"
              , Int -> Doc -> Doc
nest Int
4 Doc
t
              , Doc
"is inconsistent with the Haskell type"
              , Int -> Doc -> Doc
nest Int
4 Doc
τ
              , Doc
"defined at" Doc -> Doc -> Doc
<+> forall a. PPrint a => a -> Doc
pprint SrcSpan
hsSp
              , forall b a. b -> (a -> b) -> Maybe a -> b
maybe Doc
empty (Doc, Doc) -> Doc
ppCause Maybe (Doc, Doc)
cause
              ]
    where
      ppCause :: (Doc, Doc) -> Doc
ppCause (Doc
hsD, Doc
lqD) = Doc -> [Doc] -> Doc
sepVcat Doc
blankLine
              [ Doc
"Specifically, the Liquid component"
              , Int -> Doc -> Doc
nest Int
4 Doc
lqD
              , Doc
"is inconsistent with the Haskell component"
              , Int -> Doc -> Doc
nest Int
4 Doc
hsD
              , forall t. TError t -> Doc
hint TError a
e
              ]

ppError' Tidy
_ Doc
dCtx (ErrAliasCycle SrcSpan
_ [(SrcSpan, Doc)]
acycle)
  = FilePath -> Doc
text FilePath
"Cyclic type alias definition for" Doc -> Doc -> Doc
<+> forall a. PPrint a => a -> Doc
ppTicks Doc
n0
        Doc -> Doc -> Doc
$+$ Doc
dCtx
        Doc -> Doc -> Doc
$+$ Int -> Doc -> Doc
nest Int
4 (Doc -> [Doc] -> Doc
sepVcat Doc
blankLine (Doc
hdr forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map forall {a} {a}. (PPrint a, PPrint a) => (a, a) -> Doc
describe [(SrcSpan, Doc)]
acycle))
  where
    hdr :: Doc
hdr             = FilePath -> Doc
text FilePath
"The following alias definitions form a cycle:"
    describe :: (a, a) -> Doc
describe (a
p, a
n) = FilePath -> Doc
text FilePath
"*" Doc -> Doc -> Doc
<+> forall a. PPrint a => a -> Doc
ppTicks a
n Doc -> Doc -> Doc
<+> Doc -> Doc
parens (FilePath -> Doc
text FilePath
"defined at:" Doc -> Doc -> Doc
<+> forall a. PPrint a => a -> Doc
pprint a
p)
    n0 :: Doc
n0              = forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> a
head forall a b. (a -> b) -> a -> b
$ [(SrcSpan, Doc)]
acycle

ppError' Tidy
_ Doc
dCtx (ErrIllegalAliasApp SrcSpan
_ Doc
dn SrcSpan
dl)
  = FilePath -> Doc
text FilePath
"Refinement type alias cannot be used in this context"
        Doc -> Doc -> Doc
$+$ Doc
dCtx
        Doc -> Doc -> Doc
$+$ FilePath -> Doc
text FilePath
"Type alias:" Doc -> Doc -> Doc
<+> forall a. PPrint a => a -> Doc
pprint Doc
dn
        Doc -> Doc -> Doc
$+$ FilePath -> Doc
text FilePath
"Defined at:" Doc -> Doc -> Doc
<+> forall a. PPrint a => a -> Doc
pprint SrcSpan
dl

ppError' Tidy
_ Doc
dCtx (ErrAliasApp SrcSpan
_ Doc
name SrcSpan
dl Doc
s)
  = FilePath -> Doc
text FilePath
"Malformed application of type alias" Doc -> Doc -> Doc
<+> forall a. PPrint a => a -> Doc
ppTicks Doc
name
        Doc -> Doc -> Doc
$+$ Doc
dCtx
        Doc -> Doc -> Doc
$+$ Int -> Doc -> Doc
nest Int
4 ([Doc] -> Doc
vcat [ FilePath -> Doc
text FilePath
"The alias" Doc -> Doc -> Doc
<+> forall a. PPrint a => a -> Doc
ppTicks Doc
name Doc -> Doc -> Doc
<+> Doc
"defined at:" Doc -> Doc -> Doc
<+> forall a. PPrint a => a -> Doc
pprint SrcSpan
dl
                           , Doc
s ])

ppError' Tidy
_ Doc
dCtx (ErrSaved SrcSpan
_ Doc
name Doc
s)
  = Doc
name -- <+> "(saved)"
        Doc -> Doc -> Doc
$+$ Doc
dCtx
        Doc -> Doc -> Doc
$+$ {- nest 4 -} Doc
s

ppError' Tidy
_ Doc
dCtx (ErrFilePragma SrcSpan
_)
  = FilePath -> Doc
text FilePath
"Illegal pragma"
        Doc -> Doc -> Doc
$+$ Doc
dCtx
        Doc -> Doc -> Doc
$+$ FilePath -> Doc
text FilePath
"--idirs, --c-files, and --ghc-option cannot be used in file-level pragmas"

ppError' Tidy
_ Doc
_ err :: TError a
err@(ErrNoSpec SrcSpan
_ Doc
srcF Doc
bspecF)
  =   [Doc] -> Doc
vcat [ FilePath -> Doc
text FilePath
"Cannot find .bspec file "
           , Int -> Doc -> Doc
nest Int
4 Doc
bspecF
           , FilePath -> Doc
text FilePath
"for the source file "
           , Int -> Doc -> Doc
nest Int
4 Doc
srcF
           , forall t. TError t -> Doc
hint TError a
err
           ]

ppError' Tidy
_ Doc
dCtx (ErrOther SrcSpan
_ Doc
s)
  = FilePath -> Doc
text FilePath
"Uh oh."
        Doc -> Doc -> Doc
$+$ Doc
dCtx
        Doc -> Doc -> Doc
$+$ Int -> Doc -> Doc
nest Int
4 Doc
s

ppError' Tidy
_ Doc
dCtx (ErrTermin SrcSpan
_ [Doc]
xs Doc
s)
  = FilePath -> Doc
text FilePath
"Termination Error"
        Doc -> Doc -> Doc
$+$ Doc
dCtx
        Doc -> Doc -> Doc
<+> [Doc] -> Doc
hsep (forall a. a -> [a] -> [a]
L.intersperse Doc
comma [Doc]
xs) Doc -> Doc -> Doc
$+$ Doc
s

ppError' Tidy
_ Doc
dCtx (ErrStTerm SrcSpan
_ Doc
x Doc
s)
  = FilePath -> Doc
text FilePath
"Structural Termination Error"
        Doc -> Doc -> Doc
$+$ Doc
dCtx
        Doc -> Doc -> Doc
<+> (FilePath -> Doc
text FilePath
"Cannot prove termination for size" Doc -> Doc -> Doc
<+> Doc
x) Doc -> Doc -> Doc
$+$ Doc
s
ppError' Tidy
_ Doc
dCtx (ErrILaw SrcSpan
_ Doc
c Doc
i Doc
s)
  = FilePath -> Doc
text FilePath
"Law Instance Error"
        Doc -> Doc -> Doc
$+$ Doc
dCtx
        Doc -> Doc -> Doc
<+> (FilePath -> Doc
text FilePath
"The instance" Doc -> Doc -> Doc
<+> Doc
i Doc -> Doc -> Doc
<+> FilePath -> Doc
text FilePath
"of class" Doc -> Doc -> Doc
<+> Doc
c Doc -> Doc -> Doc
<+> FilePath -> Doc
text FilePath
"is not valid.") Doc -> Doc -> Doc
$+$ Doc
s

ppError' Tidy
_ Doc
dCtx (ErrMClass SrcSpan
_ Doc
v)
  = FilePath -> Doc
text FilePath
"Standalone class method refinement"
    Doc -> Doc -> Doc
$+$ Doc
dCtx
    Doc -> Doc -> Doc
$+$ (FilePath -> Doc
text FilePath
"Invalid type specification for" Doc -> Doc -> Doc
<+> Doc
v)
    Doc -> Doc -> Doc
$+$ FilePath -> Doc
text FilePath
"Use class or instance refinements instead."

ppError' Tidy
_ Doc
_ (ErrRClass SrcSpan
p0 Doc
c [(SrcSpan, Doc)]
is)
  = FilePath -> Doc
text FilePath
"Refined classes cannot have refined instances"
    Doc -> Doc -> Doc
$+$ Int -> Doc -> Doc
nest Int
4 (Doc -> [Doc] -> Doc
sepVcat Doc
blankLine forall a b. (a -> b) -> a -> b
$ Doc
describeCls forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map forall {a}. PPrint a => (a, Doc) -> Doc
describeInst [(SrcSpan, Doc)]
is)
  where
    describeCls :: Doc
describeCls
      =   FilePath -> Doc
text FilePath
"Refined class definition for:" Doc -> Doc -> Doc
<+> Doc
c
      Doc -> Doc -> Doc
$+$ FilePath -> Doc
text FilePath
"Defined at:" Doc -> Doc -> Doc
<+> forall a. PPrint a => a -> Doc
pprint SrcSpan
p0
    describeInst :: (a, Doc) -> Doc
describeInst (a
p, Doc
t)
      =   FilePath -> Doc
text FilePath
"Refined instance for:" Doc -> Doc -> Doc
<+> Doc
t
      Doc -> Doc -> Doc
$+$ FilePath -> Doc
text FilePath
"Defined at:" Doc -> Doc -> Doc
<+> forall a. PPrint a => a -> Doc
pprint a
p

ppError' Tidy
_ Doc
dCtx (ErrTyCon SrcSpan
_ Doc
msg Doc
ty)
  = FilePath -> Doc
text FilePath
"Illegal data refinement for" Doc -> Doc -> Doc
<+> forall a. PPrint a => a -> Doc
ppTicks Doc
ty
        Doc -> Doc -> Doc
$+$ Doc
dCtx
        Doc -> Doc -> Doc
$+$ Int -> Doc -> Doc
nest Int
4 Doc
msg

ppError' Tidy
_ Doc
dCtx (ErrRewrite SrcSpan
_ Doc
msg )
  = FilePath -> Doc
text FilePath
"Rewrite error"
        Doc -> Doc -> Doc
$+$ Doc
dCtx
        Doc -> Doc -> Doc
$+$ Int -> Doc -> Doc
nest Int
4 Doc
msg

ppError' Tidy
_ Doc
dCtx (ErrPosTyCon SrcSpan
_ Doc
tc Doc
dc)
  = FilePath -> Doc
text FilePath
"Negative occurence of" Doc -> Doc -> Doc
<+> Doc
tc Doc -> Doc -> Doc
<+> Doc
"in" Doc -> Doc -> Doc
<+> Doc
dc
        Doc -> Doc -> Doc
$+$ Doc
dCtx
        Doc -> Doc -> Doc
$+$ [Doc] -> Doc
vcat
            [Doc
"\n"
             , Doc
"To deactivate or understand the need of positivity check, see:"
             , Doc
" "
             , Int -> Doc -> Doc
nest Int
2 Doc
"https://ucsd-progsys.github.io/liquidhaskell/options/#positivity-check"
            ]

ppError' Tidy
_ Doc
dCtx (ErrParseAnn SrcSpan
_ Doc
msg)
  = FilePath -> Doc
text FilePath
"Malformed annotation"
        Doc -> Doc -> Doc
$+$ Doc
dCtx
        Doc -> Doc -> Doc
$+$ Int -> Doc -> Doc
nest Int
4 Doc
msg

ppTicks :: PPrint a => a -> Doc
ppTicks :: forall a. PPrint a => a -> Doc
ppTicks = Doc -> Doc
ticks forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. PPrint a => a -> Doc
pprint

ticks :: Doc -> Doc
ticks :: Doc -> Doc
ticks Doc
d = FilePath -> Doc
text FilePath
"`" Doc -> Doc -> Doc
<-> Doc
d Doc -> Doc -> Doc
<-> FilePath -> Doc
text FilePath
"`"

ppSrcSpans :: [SrcSpan] -> Doc
ppSrcSpans :: [SrcSpan] -> Doc
ppSrcSpans = forall a. PPrint a => Doc -> [a] -> Doc
ppList (FilePath -> Doc
text FilePath
"Conflicting definitions at")

ppNames :: [Doc] -> Doc
ppNames :: [Doc] -> Doc
ppNames [Doc]
ds = forall a. PPrint a => Doc -> [a] -> Doc
ppList Doc
"Could refer to any of the names" [Doc]
ds -- [text "-" <+> d | d <- ds]

ppList :: (PPrint a) => Doc -> [a] -> Doc
ppList :: forall a. PPrint a => Doc -> [a] -> Doc
ppList Doc
d [a]
ls
  = Int -> Doc -> Doc
nest Int
4 (Doc -> [Doc] -> Doc
sepVcat Doc
blankLine (Doc
d forall a. a -> [a] -> [a]
: [ FilePath -> Doc
text FilePath
"*" Doc -> Doc -> Doc
<+> forall a. PPrint a => a -> Doc
pprint a
l | a
l <- [a]
ls ]))

-- | Convert a GHC error into a list of our errors.

sourceErrors :: String -> SourceError -> [TError t]
sourceErrors :: forall t. FilePath -> SourceError -> [TError t]
sourceErrors FilePath
s =
  forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap forall {e} {t}. Show (MsgEnvelope e) => MsgEnvelope e -> [TError t]
errMsgErrors forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Bag a -> [a]
bagToList forall b c a. (b -> c) -> (a -> b) -> a -> c
. SourceError -> ErrorMessages
srcErrorMessages
  where
    errMsgErrors :: MsgEnvelope e -> [TError t]
errMsgErrors MsgEnvelope e
e = [ forall t. SrcSpan -> Doc -> TError t
ErrGhc (forall e. MsgEnvelope e -> SrcSpan
errMsgSpan MsgEnvelope e
e) Doc
msg ]
      where
        msg :: Doc
msg = FilePath -> Doc
text FilePath
s Doc -> Doc -> Doc
$+$ Int -> Doc -> Doc
nest Int
4 (FilePath -> Doc
text (forall a. Show a => a -> FilePath
show MsgEnvelope e
e))