{-# LANGUAGE ImplicitParams      #-}
{-# LANGUAGE TupleSections       #-}
{-# LANGUAGE FlexibleInstances   #-}
{-# LANGUAGE OverloadedStrings   #-}
{-# LANGUAGE DeriveGeneric       #-}
{-# LANGUAGE DeriveDataTypeable  #-}
{-# LANGUAGE DeriveFunctor       #-}
{-# LANGUAGE OverloadedStrings   #-}
{-# LANGUAGE DerivingStrategies  #-}
{-# LANGUAGE DerivingVia         #-}

-- | 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 (..)

  -- * 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
  , realSrcSpan
  , unpackRealSrcSpan
  , srcSpanFileMb
  ) where

import           Prelude                      hiding (error)
import           SrcLoc
import           FastString
import           HscTypes (srcErrorMessages, SourceError)
import           ErrUtils
import           Bag

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           System.Directory
import           System.FilePath
import           Text.PrettyPrint.HughesPJ
import           Text.Parsec.Error            (ParseError)
import           Text.Parsec.Error            (errorMessages, showErrorMessages)

import           Language.Fixpoint.Types      (pprint, showpp, Tidy (..), PPrint (..), Symbol, Expr)
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

instance PPrint ParseError where
  pprintTidy :: Tidy -> ParseError -> Doc
pprintTidy Tidy
_ ParseError
e = [Doc] -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> [Doc]
forall a. [a] -> [a]
tail ([Doc] -> [Doc]) -> [Doc] -> [Doc]
forall a b. (a -> b) -> a -> b
$ String -> Doc
text (String -> Doc) -> [String] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [String]
ls
    where
      ls :: [String]
ls         = String -> [String]
lines (String -> [String]) -> String -> [String]
forall a b. (a -> b) -> a -> b
$ String
-> String -> String -> String -> String -> [Message] -> String
showErrorMessages String
"or" String
"unknown parse error"
                               String
"expecting" String
"unexpected" String
"end of input"
                               (ParseError -> [Message]
errorMessages ParseError
e)

--------------------------------------------------------------------------------
-- | Context information for Error Messages ------------------------------------
--------------------------------------------------------------------------------
data CtxError t = CtxError
  { CtxError t -> TError t
ctErr :: TError t
  , CtxError t -> Doc
ctCtx :: Doc
  } deriving (a -> CtxError b -> CtxError a
(a -> b) -> CtxError a -> CtxError b
(forall a b. (a -> b) -> CtxError a -> CtxError b)
-> (forall a b. a -> CtxError b -> CtxError a) -> Functor CtxError
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
<$ :: a -> CtxError b -> CtxError a
$c<$ :: forall a b. a -> CtxError b -> CtxError a
fmap :: (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 = CtxError t -> TError t
forall t. CtxError t -> TError t
ctErr CtxError t
e1 TError t -> TError t -> Bool
forall a. Eq a => a -> a -> Bool
== CtxError t -> TError t
forall t. CtxError t -> TError t
ctErr CtxError t
e2

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

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

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

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

srcSpanContext :: FileBody -> SrcSpan -> Doc
srcSpanContext :: [String] -> SrcSpan -> Doc
srcSpanContext [String]
fb SrcSpan
sp
  | Just (Int
l, Int
c, Int
l', Int
c') <- SrcSpan -> Maybe (Int, Int, Int, Int)
srcSpanInfo SrcSpan
sp
  = Int -> Int -> Int -> [String] -> Doc
makeContext Int
l Int
c Int
c' ([String] -> Int -> Int -> [String]
getFileLines [String]
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)
              = (Int, Int, Int, Int) -> Maybe (Int, Int, Int, Int)
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
_ = Maybe (Int, Int, Int, Int)
forall a. Maybe a
Nothing

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

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

type FileBody = [String]

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

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

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

makeContext1 :: Int -> Int -> Int -> String -> Doc
makeContext1 :: Int -> Int -> Int -> String -> Doc
makeContext1 Int
l Int
c Int
c' String
s = [Doc] -> Doc
vcat [ String -> Doc
text String
" "
                             , Int -> Doc
forall a. Show a => a -> Doc
lnum Int
l Doc -> Doc -> Doc
<+> (String -> Doc
text String
s Doc -> Doc -> Doc
$+$ Doc
cursor)
                             , String -> Doc
text String
" "
                             , String -> Doc
text String
" "
                             ]
  where
    lnum :: a -> Doc
lnum a
n            = String -> Doc
text (a -> String
forall a. Show a => a -> String
show a
n) Doc -> Doc -> Doc
<+> String -> Doc
text String
"|"
    cursor :: Doc
cursor            = Int -> Doc
blanks (Int
c Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Doc -> Doc -> Doc
<-> Int -> Doc
pointer (Int -> Int -> Int
forall a. Ord a => a -> a -> a
max Int
1 (Int
c' Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
c))
    blanks :: Int -> Doc
blanks Int
n          = String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ Int -> Char -> String
forall a. Int -> a -> [a]
replicate Int
n Char
' '
    pointer :: Int -> Doc
pointer Int
n         = String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ Int -> Char -> String
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
(Oblig -> Oblig -> Bool) -> (Oblig -> Oblig -> Bool) -> Eq Oblig
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. Oblig -> Rep Oblig x)
-> (forall x. Rep Oblig x -> Oblig) -> Generic Oblig
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
DataType
Constr
Typeable Oblig
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Oblig -> c Oblig)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Oblig)
-> (Oblig -> Constr)
-> (Oblig -> DataType)
-> (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))
-> ((forall b. Data b => b -> b) -> Oblig -> Oblig)
-> (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 u. (forall d. Data d => d -> u) -> Oblig -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Oblig -> u)
-> (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 (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Oblig -> m Oblig)
-> Data Oblig
Oblig -> DataType
Oblig -> Constr
(forall b. Data b => b -> b) -> Oblig -> Oblig
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Oblig -> c Oblig
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c 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)
$cOCons :: Constr
$cOInv :: Constr
$cOTerm :: Constr
$tOblig :: DataType
gmapMo :: (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 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 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 :: Int -> (forall d. Data d => d -> u) -> Oblig -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Oblig -> u
gmapQ :: (forall d. Data d => d -> u) -> Oblig -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Oblig -> [u]
gmapQr :: (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 :: (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 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 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 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 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
$cp1Data :: Typeable Oblig
Data, Typeable)
  deriving Int -> Oblig -> Int
Oblig -> Int
(Int -> Oblig -> Int) -> (Oblig -> Int) -> Hashable Oblig
forall 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 -> String
show Oblig
OTerm = String
"termination-condition"
  show Oblig
OInv  = String
"invariant-obligation"
  show Oblig
OCons = String
"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 = String -> Doc
text String
"Constraint Check"
ppOblig Oblig
OTerm = String -> Doc
text String
"Termination Check"
ppOblig Oblig
OInv  = String -> Doc
text String
"Invariant Check"

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

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

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

  | ErrSubTypeModel
               { pos  :: !SrcSpan
               , msg  :: !Doc
               , TError t -> HashMap Symbol (WithModel t)
ctxM  :: !(M.HashMap Symbol (WithModel 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)
               , TError t -> Symbol
svar :: !Symbol
               , TError t -> t
thl  :: !t
               } -- ^ hole type

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

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

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

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

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

  | ErrDupAlias { pos  :: !SrcSpan
                , var  :: !Doc
                , TError t -> Doc
kind :: !Doc
                , 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
                , 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
                , TError t -> Doc
dcon  :: !Doc
                , TError t -> Doc
field :: !Doc
                } -- ^ duplicate fields in same datacon

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

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

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

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

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

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

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

  | ErrMeas     { pos :: !SrcSpan
                , 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
                , TError t -> Doc
hs    :: !Doc
                , TError t -> Doc
lqTy  :: !Doc
                , TError t -> Maybe (Doc, Doc)
diff  :: !(Maybe (Doc, Doc))  -- ^ specific pair of things that mismatch
                , TError t -> SrcSpan
lqPos :: !SrcSpan -- ^ lq type location
                } -- ^ Mismatch between Liquid and Haskell types

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

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

  | ErrIllegalAliasApp { pos   :: !SrcSpan
                       , TError t -> Doc
dname :: !Doc
                       , 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
                , TError t -> [Doc]
bind :: ![Doc]
                , msg  :: !Doc
                } -- ^ Termination Error

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

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

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

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

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

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

  | ErrFilePragma { pos :: !SrcSpan
                  }

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

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

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

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

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

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

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

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

  deriving (Typeable, (forall x. TError t -> Rep (TError t) x)
-> (forall x. Rep (TError t) x -> TError t) -> Generic (TError t)
forall x. Rep (TError t) x -> TError t
forall x. TError t -> Rep (TError t) x
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 , a -> TError b -> TError a
(a -> b) -> TError a -> TError b
(forall a b. (a -> b) -> TError a -> TError b)
-> (forall a b. a -> TError b -> TError a) -> Functor TError
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
<$ :: a -> TError b -> TError a
$c<$ :: forall a b. a -> TError b -> TError a
fmap :: (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 :: Doc -> [SrcSpan] -> TError t
errDupSpecs Doc
d spans :: [SrcSpan]
spans@(SrcSpan
sp:[SrcSpan]
_) = SrcSpan -> Doc -> [SrcSpan] -> TError t
forall t. SrcSpan -> Doc -> [SrcSpan] -> TError t
ErrDupSpecs SrcSpan
sp Doc
d [SrcSpan]
spans
errDupSpecs Doc
_ [SrcSpan]
_            = Maybe SrcSpan -> String -> TError t
forall a. Maybe SrcSpan -> String -> a
impossible Maybe SrcSpan
forall a. Maybe a
Nothing String
"errDupSpecs with empty spans!"

instance NFData ParseError where
  rnf :: ParseError -> ()
rnf ParseError
t = ParseError -> () -> ()
seq ParseError
t ()

-- 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 = TError a -> SrcSpan
forall t. TError t -> SrcSpan
errSpan TError a
e1 SrcSpan -> SrcSpan -> Bool
forall a. Eq a => a -> a -> Bool
== TError a -> SrcSpan
forall t. TError t -> SrcSpan
errSpan TError a
e2

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


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

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

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

data WithModel t
  = NoModel t
  | WithModel !Doc t
  deriving (a -> WithModel b -> WithModel a
(a -> b) -> WithModel a -> WithModel b
(forall a b. (a -> b) -> WithModel a -> WithModel b)
-> (forall a b. a -> WithModel b -> WithModel a)
-> Functor WithModel
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
<$ :: a -> WithModel b -> WithModel a
$c<$ :: forall a b. a -> WithModel b -> WithModel a
fmap :: (a -> b) -> WithModel a -> WithModel b
$cfmap :: forall a b. (a -> b) -> WithModel a -> WithModel b
Functor, Int -> WithModel t -> ShowS
[WithModel t] -> ShowS
WithModel t -> String
(Int -> WithModel t -> ShowS)
-> (WithModel t -> String)
-> ([WithModel t] -> ShowS)
-> Show (WithModel t)
forall t. Show t => Int -> WithModel t -> ShowS
forall t. Show t => [WithModel t] -> ShowS
forall t. Show t => WithModel t -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [WithModel t] -> ShowS
$cshowList :: forall t. Show t => [WithModel t] -> ShowS
show :: WithModel t -> String
$cshow :: forall t. Show t => WithModel t -> String
showsPrec :: Int -> WithModel t -> ShowS
$cshowsPrec :: forall t. Show t => Int -> WithModel t -> ShowS
Show, WithModel t -> WithModel t -> Bool
(WithModel t -> WithModel t -> Bool)
-> (WithModel t -> WithModel t -> Bool) -> Eq (WithModel t)
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 x. WithModel t -> Rep (WithModel t) x)
-> (forall x. Rep (WithModel t) x -> WithModel t)
-> Generic (WithModel t)
forall x. Rep (WithModel t) x -> WithModel t
forall x. WithModel t -> Rep (WithModel t) x
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 :: 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 FastString
s) = String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ FastString -> String
unpackFS FastString
s
pprSrcSpan (RealSrcSpan RealSrcSpan
s)   = RealSrcSpan -> Doc
pprRealSrcSpan RealSrcSpan
s

pprRealSrcSpan :: RealSrcSpan -> Doc
pprRealSrcSpan :: RealSrcSpan -> Doc
pprRealSrcSpan RealSrcSpan
span
  | Int
sline Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
eline Bool -> Bool -> Bool
&& Int
scol Int -> Int -> Bool
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 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
eline =
    [Doc] -> Doc
hcat ([Doc] -> Doc) -> [Doc] -> Doc
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
           ] [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ if Int
ecol Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
scol Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
1 then [] else [Char -> Doc
char Char
'-' Doc -> Doc -> Doc
<-> Int -> Doc
int (Int
ecol Int -> Int -> Int
forall a. Num a => a -> a -> a
- 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 = String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ ShowS
normalise ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ FastString -> String
unpackFS FastString
path
   ecol' :: Int
ecol'   = if Int
ecol Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 then Int
ecol else Int
ecol Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1

instance Show UserError where
  show :: TError Doc -> String
show = TError Doc -> String
forall a. PPrint a => a -> String
showpp

instance Ex.Exception UserError

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

-- | Construct and show an Error, then crash
panicDoc :: {- (?callStack :: CallStack) => -} SrcSpan -> Doc -> a
panicDoc :: SrcSpan -> Doc -> a
panicDoc SrcSpan
sp Doc
d = TError Doc -> a
forall a e. Exception e => e -> a
Ex.throw (SrcSpan -> Doc -> TError Doc
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 :: Maybe SrcSpan -> String -> a
panic Maybe SrcSpan
sp String
d = SrcSpan -> Doc -> a
forall a. SrcSpan -> Doc -> a
panicDoc (Maybe SrcSpan -> SrcSpan
sspan Maybe SrcSpan
sp) (String -> Doc
text String
d)
  where
    sspan :: Maybe SrcSpan -> SrcSpan
sspan  = SrcSpan -> Maybe SrcSpan -> SrcSpan
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 :: Maybe SrcSpan -> String -> a
todo Maybe SrcSpan
s String
m  = Maybe SrcSpan -> String -> a
forall a. Maybe SrcSpan -> String -> a
panic Maybe SrcSpan
s (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines
            [ String
"This functionality is currently unimplemented. "
            , String
"If this functionality is critical to you, please contact us at: "
            , String
"https://github.com/ucsd-progsys/liquidhaskell/issues"
            , String
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 :: Maybe SrcSpan -> String -> a
impossible Maybe SrcSpan
s String
m = Maybe SrcSpan -> String -> a
forall a. Maybe SrcSpan -> String -> a
panic Maybe SrcSpan
s (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [String]
msg String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
m
   where
      msg :: [String]
msg = [ String
"This should never happen! If you are seeing this message, "
            , String
"please submit a bug report at "
            , String
"https://github.com/ucsd-progsys/liquidhaskell/issues "
            , String
"with this message and the source file that caused this error."
            , String
""
            ]



-- type CtxError = Error
--------------------------------------------------------------------------------
ppError :: (PPrint a, Show a) => Tidy -> Doc -> TError a -> Doc
--------------------------------------------------------------------------------
ppError :: Tidy -> Doc -> TError a -> Doc
ppError Tidy
k Doc
dCtx TError a
e = Tidy -> Doc -> TError a -> Doc
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 = (Doc -> Doc -> Doc) -> Doc -> [Doc] -> Doc
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 ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
L.intersperse Doc
d [Doc]
ds

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

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 :: 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 [ String -> Doc
text String
"The inferred type"
                , String -> Doc
text String
"VV :" Doc -> Doc -> Doc
<+> Tidy -> t -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
td t
tA]
      , Int -> [Doc] -> Doc
nests Int
2 [ String -> Doc
text String
"is not a subtype of the required type"
                , String -> Doc
text String
"VV :" Doc -> Doc -> Doc
<+> Tidy -> t -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
td t
tE]
      , Tidy -> HashMap Symbol t -> Doc
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 :: Tidy -> HashMap Symbol t -> Doc
ppContext Tidy
td HashMap Symbol t
c
  | Int
0 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< [(Symbol, t)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Symbol, t)]
xts = Int -> [Doc] -> Doc
nests Int
2 [ String -> Doc
text String
"in the context"
                             , [Doc] -> Doc
vsep (((Symbol, t) -> Doc) -> [(Symbol, t)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map ((Symbol -> t -> Doc) -> (Symbol, t) -> Doc
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (Tidy -> Symbol -> t -> Doc
forall t. PPrint t => Tidy -> Symbol -> t -> Doc
pprintBind Tidy
td)) [(Symbol, t)]
xts)
                             ]
  | Bool
otherwise      = Doc
empty
  where
    xts :: [(Symbol, t)]
xts            = HashMap Symbol t -> [(Symbol, t)]
forall k v. HashMap k v -> [(k, v)]
M.toList HashMap Symbol t
c

pprintBind :: PPrint t => Tidy -> Symbol -> t -> Doc
pprintBind :: Tidy -> Symbol -> t -> Doc
pprintBind Tidy
td Symbol
v t
t = Tidy -> Symbol -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
td Symbol
v Doc -> Doc -> Doc
<+> Char -> Doc
char Char
':' Doc -> Doc -> Doc
<+> Tidy -> t -> 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 :: 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 [ String -> Doc
text String
"The inferred type"
                , Tidy -> Symbol -> WithModel t -> Doc
forall t. PPrint t => Tidy -> Symbol -> WithModel t -> Doc
pprintModel Tidy
td Symbol
"VV" WithModel t
tA]
      , Int -> [Doc] -> Doc
nests Int
2 [ String -> Doc
text String
"is not a subtype of the required type"
                , Tidy -> Symbol -> WithModel t -> Doc
forall t. PPrint t => Tidy -> Symbol -> WithModel t -> Doc
pprintModel Tidy
td Symbol
"VV" (t -> WithModel t
forall t. t -> WithModel t
NoModel t
tE)]
      , Int -> [Doc] -> Doc
nests Int
2 [ String -> Doc
text String
"in the context"
                , [Doc] -> Doc
vsep (((Symbol, WithModel t) -> Doc) -> [(Symbol, WithModel t)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map ((Symbol -> WithModel t -> Doc) -> (Symbol, WithModel t) -> Doc
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (Tidy -> Symbol -> WithModel t -> Doc
forall t. PPrint t => Tidy -> Symbol -> WithModel t -> Doc
pprintModel Tidy
td)) (HashMap Symbol (WithModel t) -> [(Symbol, WithModel t)]
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 ([Doc] -> Doc) -> ([Doc] -> [Doc]) -> [Doc] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
L.intersperse (Char -> Doc
char Char
' ')

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

ppPropInContext :: (PPrint p, PPrint c) => Tidy -> p -> c -> Doc
ppPropInContext :: Tidy -> p -> c -> Doc
ppPropInContext Tidy
td p
p c
c
  = Doc -> [Doc] -> Doc
sepVcat Doc
blankLine
      [ Int -> [Doc] -> Doc
nests Int
2 [ String -> Doc
text String
"Property"
                , Tidy -> p -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
td p
p]
      , Int -> [Doc] -> Doc
nests Int
2 [ String -> Doc
text String
"Not provable in context"
                , Tidy -> c -> Doc
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 [ Text
"filename"  Text -> String -> Pair
forall kv v. (KeyValue kv, ToJSON v) => Text -> v -> kv
.= String
f
                     , Text
"startLine" Text -> Int -> Pair
forall kv v. (KeyValue kv, ToJSON v) => Text -> v -> kv
.= Int
l1
                     , Text
"startCol"  Text -> Int -> Pair
forall kv v. (KeyValue kv, ToJSON v) => Text -> v -> kv
.= Int
c1
                     , Text
"endLine"   Text -> Int -> Pair
forall kv v. (KeyValue kv, ToJSON v) => Text -> v -> kv
.= Int
l2
                     , Text
"endCol"    Text -> Int -> Pair
forall kv v. (KeyValue kv, ToJSON v) => Text -> v -> kv
.= Int
c2
                     ]
    where
      (String
f, Int
l1, Int
c1, Int
l2, Int
c2) = RealSrcSpan -> (String, Int, Int, Int, Int)
unpackRealSrcSpan RealSrcSpan
sp

unpackRealSrcSpan :: RealSrcSpan -> (String, Int, Int, Int, Int)
unpackRealSrcSpan :: RealSrcSpan -> (String, Int, Int, Int, Int)
unpackRealSrcSpan RealSrcSpan
rsp = (String
f, Int
l1, Int
c1, Int
l2, Int
c2)
  where
    f :: String
f                 = FastString -> String
unpackFS (FastString -> String) -> FastString -> String
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) = String -> Int -> Int -> Int -> Int -> RealSrcSpan
realSrcSpan (String -> Int -> Int -> Int -> Int -> RealSrcSpan)
-> Parser String
-> Parser (Int -> Int -> Int -> Int -> RealSrcSpan)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Object
v Object -> Text -> Parser String
forall a. FromJSON a => Object -> Text -> Parser a
.: Text
"filename"
                                     Parser (Int -> Int -> Int -> Int -> RealSrcSpan)
-> Parser Int -> Parser (Int -> Int -> Int -> RealSrcSpan)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Object
v Object -> Text -> Parser Int
forall a. FromJSON a => Object -> Text -> Parser a
.: Text
"startLine"
                                     Parser (Int -> Int -> Int -> RealSrcSpan)
-> Parser Int -> Parser (Int -> Int -> RealSrcSpan)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Object
v Object -> Text -> Parser Int
forall a. FromJSON a => Object -> Text -> Parser a
.: Text
"startCol"
                                     Parser (Int -> Int -> RealSrcSpan)
-> Parser Int -> Parser (Int -> RealSrcSpan)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Object
v Object -> Text -> Parser Int
forall a. FromJSON a => Object -> Text -> Parser a
.: Text
"endLine"
                                     Parser (Int -> RealSrcSpan) -> Parser Int -> Parser RealSrcSpan
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Object
v Object -> Text -> Parser Int
forall a. FromJSON a => Object -> Text -> Parser a
.: Text
"endCol"
  parseJSON Value
_          = Parser RealSrcSpan
forall a. Monoid a => a
mempty

realSrcSpan :: FilePath -> Int -> Int -> Int -> Int -> RealSrcSpan
realSrcSpan :: String -> Int -> Int -> Int -> Int -> RealSrcSpan
realSrcSpan String
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 (String -> FastString
fsLit String
f) Int
l1 Int
c1
    loc2 :: RealSrcLoc
loc2                  = FastString -> Int -> Int -> RealSrcLoc
mkRealSrcLoc (String -> FastString
fsLit String
f) Int
l2 Int
c2

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


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

instance FromJSON SrcSpan where
  parseJSON :: Value -> Parser SrcSpan
parseJSON (Object Object
v) = do Bool
tag <- Object
v Object -> Text -> Parser Bool
forall a. FromJSON a => Object -> Text -> Parser a
.: Text
"realSpan"
                            case Bool
tag of
                              Bool
False -> SrcSpan -> Parser SrcSpan
forall (m :: * -> *) a. Monad m => a -> m a
return SrcSpan
noSrcSpan
                              Bool
True  -> RealSrcSpan -> SrcSpan
RealSrcSpan (RealSrcSpan -> SrcSpan) -> Parser RealSrcSpan -> Parser SrcSpan
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Object
v Object -> Text -> Parser RealSrcSpan
forall a. FromJSON a => Object -> Text -> Parser a
.: Text
"spanInfo"
  parseJSON Value
_          = Parser SrcSpan
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 [ Text
"pos" Text -> SrcSpan -> Pair
forall kv v. (KeyValue kv, ToJSON v) => Text -> v -> kv
.= (TError a -> SrcSpan
forall t. TError t -> SrcSpan
pos TError a
e)
                    , Text
"msg" Text -> String -> Pair
forall kv v. (KeyValue kv, ToJSON v) => Text -> v -> kv
.= (Doc -> String
render (Doc -> String) -> Doc -> String
forall a b. (a -> b) -> a -> b
$ Tidy -> Doc -> TError a -> Doc
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) = SrcSpan -> String -> TError a
forall a. SrcSpan -> String -> TError a
errSaved (SrcSpan -> String -> TError a)
-> Parser SrcSpan -> Parser (String -> TError a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Object
v Object -> Text -> Parser SrcSpan
forall a. FromJSON a => Object -> Text -> Parser a
.: Text
"pos"
                                  Parser (String -> TError a) -> Parser String -> Parser (TError a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Object
v Object -> Text -> Parser String
forall a. FromJSON a => Object -> Text -> Parser a
.: Text
"msg"
  parseJSON Value
_          = Parser (TError a)
forall a. Monoid a => a
mempty

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


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

hint :: TError a -> Doc
hint :: TError a -> Doc
hint TError a
e = Doc -> (Doc -> Doc) -> Maybe Doc -> Doc
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)) (TError a -> Maybe Doc
forall a t. IsString a => TError t -> Maybe a
go TError a
e)
  where
    go :: TError t -> Maybe a
go (ErrMismatch {}) = a -> Maybe a
forall a. a -> Maybe a
Just a
"Use the hole '_' instead of the mismatched component (in the Liquid specification)"
    go (ErrBadGADT {})  = a -> Maybe a
forall a. a -> Maybe a
Just a
"Use the hole '_' to specify the type of the constructor"
    go (ErrSubType {})  = a -> Maybe a
forall a. a -> Maybe a
Just a
"Use \"--no-totality\" to deactivate totality checking."
    go (ErrNoSpec {})   = a -> Maybe a
forall a. a -> Maybe a
Just a
"Run 'liquid' on the source file first."
    go TError t
_                = Maybe a
forall a. Maybe a
Nothing

--------------------------------------------------------------------------------
ppError' :: (PPrint a, Show a) => Tidy -> Doc -> TError a -> Doc
--------------------------------------------------------------------------------
ppError' :: Tidy -> Doc -> TError a -> Doc
ppError' Tidy
td Doc
dCtx (ErrAssType SrcSpan
_ Oblig
o Doc
_ HashMap Symbol a
c a
p)
  = Tidy -> Oblig -> Doc
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 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Tidy -> a -> HashMap Symbol a -> Doc
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
_ HashMap Symbol a
_ a
_ a
tE)
  | Tidy -> a -> Bool
forall a. PPrint a => Tidy -> a -> Bool
totalityType Tidy
td a
tE
  = String -> Doc
text String
"Totality Error"
        Doc -> Doc -> Doc
$+$ Doc
dCtx
        Doc -> Doc -> Doc
$+$ String -> Doc
text String
"Your function is not total: not all patterns are defined."
        Doc -> Doc -> Doc
$+$ TError a -> Doc
forall a. TError a -> 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
$+$ [Symbol] -> 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
$+$ Symbol -> Doc
forall a. PPrint a => a -> Doc
pprint Symbol
x Doc -> Doc -> Doc
<+> Doc
"::" Doc -> Doc -> Doc
<+> a -> Doc
forall a. PPrint a => a -> Doc
pprint a
t
        Doc -> Doc -> Doc
$+$ Doc
msg

ppError' Tidy
td Doc
dCtx (ErrSubType SrcSpan
_ Doc
_ HashMap Symbol a
c a
tA a
tE)
  = String -> Doc
text String
"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 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Tidy -> a -> a -> HashMap Symbol a -> Doc
forall t. PPrint t => Tidy -> t -> t -> HashMap Symbol t -> Doc
ppReqInContext Tidy
td a
tA a
tE HashMap Symbol a
c))

ppError' Tidy
td Doc
dCtx (ErrSubTypeModel SrcSpan
_ Doc
_ HashMap Symbol (WithModel a)
c WithModel a
tA a
tE)
  = String -> Doc
text String
"Liquid Type Mismatch"
        Doc -> Doc -> Doc
$+$ Int -> Doc -> Doc
nest Int
4 (Doc
dCtx
                    Doc -> Doc -> Doc
$+$ (Tidy -> Doc -> Doc
ppFull Tidy
td (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Tidy -> WithModel a -> a -> HashMap Symbol (WithModel a) -> Doc
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))

ppError' Tidy
td  Doc
dCtx (ErrFCrash SrcSpan
_ Doc
_ HashMap Symbol a
c a
tA a
tE)
  = String -> Doc
text String
"Fixpoint Crash on Constraint"
        Doc -> Doc -> Doc
$+$ Doc
dCtx
        Doc -> Doc -> Doc
$+$ (Tidy -> Doc -> Doc
ppFull Tidy
td (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Tidy -> a -> a -> HashMap Symbol a -> Doc
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)
  = String -> Doc
text String
"Cannot parse specification:"
        Doc -> Doc -> Doc
$+$ Doc
dCtx
        Doc -> Doc -> Doc
$+$ (Int -> Doc -> Doc
nest Int
4 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ ParseError -> Doc
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
<+> 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 [ Doc -> Doc
forall a. PPrint a => a -> Doc
pprint Doc
v Doc -> Doc -> Doc
<+> Doc
Misc.dcolon Doc -> Doc -> Doc
<+> a -> Doc
forall a. PPrint a => a -> Doc
pprint a
t
                         , Doc -> Doc
forall a. PPrint a => a -> Doc
pprint Doc
s
                         ])
    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)
  = String -> Doc
text String
"Cannot lift" Doc -> Doc -> 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 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
text String
"Please export the binder from the module to enable lifting.")

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

ppError' Tidy
_ Doc
dCtx err :: TError a
err@(ErrBadGADT SrcSpan
_ Doc
v Doc
s)
  = String -> Doc
text String
"Bad GADT specification for" Doc -> Doc -> Doc
<+> Doc -> Doc
forall a. PPrint a => a -> Doc
ppTicks Doc
v
        Doc -> Doc -> Doc
$+$ Doc
dCtx
        Doc -> Doc -> Doc
$+$ Doc -> Doc
forall a. PPrint a => a -> Doc
pprint Doc
s
        Doc -> Doc -> Doc
$+$ TError a -> Doc
forall a. TError a -> Doc
hint TError a
err

ppError' Tidy
_ Doc
dCtx (ErrDataCon SrcSpan
_ Doc
d Doc
s)
  = Doc
"Malformed refined data constructor" Doc -> Doc -> 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 (ErrBadQual SrcSpan
_ Doc
n Doc
d)
  = String -> Doc
text String
"Illegal qualifier specification for" Doc -> Doc -> Doc
<+> Doc -> Doc
forall a. PPrint a => a -> Doc
ppTicks Doc
n
        Doc -> Doc -> Doc
$+$ Doc
dCtx
        Doc -> Doc -> 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)
  = String -> Doc
text String
"Illegal termination specification for" Doc -> Doc -> 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 -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ ((String -> Doc
text String
"Termination metric" Doc -> Doc -> Doc
<+> Expr -> Doc
forall a. PPrint a => a -> Doc
ppTicks Expr
e Doc -> Doc -> Doc
<+> String -> Doc
text String
"is" Doc -> Doc -> Doc
<+> Doc
msg Doc -> Doc -> Doc
<+> Doc
"in type signature")
                        Doc -> Doc -> Doc
$+$ Int -> Doc -> Doc
nest Int
4 (a -> Doc
forall a. PPrint a => a -> Doc
pprint a
t)
                        Doc -> Doc -> Doc
$+$ Doc -> Doc
forall a. PPrint a => a -> Doc
pprint Doc
s))

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

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

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

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

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

ppError' Tidy
_ Doc
dCtx (ErrDupSpecs SrcSpan
_ Doc
v [SrcSpan]
ls)
  = String -> Doc
text String
"Multiple specifications for" Doc -> Doc -> 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)
  = String -> Doc
text String
"Multiple instance measures" Doc -> Doc -> Doc
<+> Doc -> Doc
forall a. PPrint a => a -> Doc
ppTicks Doc
v Doc -> Doc -> Doc
<+> String -> Doc
text String
"for type" Doc -> Doc -> 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)
  = String -> Doc
text String
"Multiple measures named" Doc -> Doc -> 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)
  = String -> Doc
text String
"Malformed refined data constructor" Doc -> Doc -> Doc
<+> Doc
dc
        Doc -> Doc -> Doc
$+$ Doc
dCtx
        Doc -> Doc -> Doc
$+$ (Int -> Doc -> Doc
nest Int
4 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
text String
"Duplicated definitions for field" Doc -> Doc -> Doc
<+> Doc -> Doc
forall a. PPrint a => a -> Doc
ppTicks Doc
x)

ppError' Tidy
_ Doc
dCtx (ErrDupNames SrcSpan
_ Doc
x [Doc]
ns)
  = String -> Doc
text String
"Ambiguous specification symbol" Doc -> Doc -> 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)
  = String -> Doc
text String
"Multiple definitions of" Doc -> Doc -> Doc
<+> Doc -> Doc
forall a. PPrint a => a -> Doc
pprint Doc
k Doc -> Doc -> 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)
  = String -> Doc
text String
"Unbound variable" Doc -> Doc -> 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)
  = String -> Doc
text String
"Cannot apply unbound abstract refinement" Doc -> Doc -> 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)
  = String -> Doc
text String
"GHC Error"
        Doc -> Doc -> Doc
$+$ Doc
dCtx
        Doc -> Doc -> Doc
$+$ (Int -> Doc -> Doc
nest Int
4 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> Doc
forall a. PPrint a => a -> Doc
pprint Doc
s)

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

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

ppError' Tidy
_ Doc
dCtx (ErrResolve SrcSpan
_ Doc
kind Doc
v Doc
msg)
  = (String -> Doc
text String
"Unknown" Doc -> Doc -> Doc
<+> Doc
kind Doc -> Doc -> 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)
  = String -> Doc
text String
"Malformed predicate application"
        Doc -> Doc -> Doc
$+$ Doc
dCtx
        Doc -> Doc -> Doc
$+$ (Int -> Doc -> Doc
nest Int
4 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
vcat
                        [ Doc
"The" Doc -> Doc -> Doc
<+> String -> Doc
text (Int -> String
Misc.intToString Int
i) Doc -> Doc -> Doc
<+> Doc
"argument of" Doc -> Doc -> Doc
<+> Doc
c Doc -> Doc -> Doc
<+> Doc
"is predicate" Doc -> Doc -> Doc
<+> Doc -> Doc
forall a. PPrint a => a -> Doc
ppTicks Doc
p
                        , Doc
"which expects" Doc -> Doc -> Doc
<+> Int -> 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
<+> Int -> 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
<+> 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
<+> SrcSpan -> Doc
forall a. PPrint a => a -> Doc
pprint SrcSpan
hsSp
              , Doc -> ((Doc, Doc) -> Doc) -> Maybe (Doc, Doc) -> Doc
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
              , TError a -> Doc
forall a. TError a -> Doc
hint TError a
e
              ]

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

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

ppError' Tidy
_ Doc
dCtx (ErrAliasApp SrcSpan
_ Doc
name SrcSpan
dl Doc
s)
  = String -> Doc
text String
"Malformed application of type alias" Doc -> Doc -> 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) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
vcat [ String -> Doc
text String
"The alias" Doc -> Doc -> Doc
<+> Doc -> Doc
forall a. PPrint a => a -> Doc
ppTicks Doc
name Doc -> Doc -> Doc
<+> Doc
"defined at:" Doc -> Doc -> Doc
<+> SrcSpan -> 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
_)
  = String -> Doc
text String
"Illegal pragma"
        Doc -> Doc -> Doc
$+$ Doc
dCtx
        Doc -> Doc -> Doc
$+$ String -> Doc
text String
"--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 [ String -> Doc
text String
"Cannot find .bspec file "
           , Int -> Doc -> Doc
nest Int
4 Doc
bspecF
           , String -> Doc
text String
"for the source file "
           , Int -> Doc -> Doc
nest Int
4 Doc
srcF
           , TError a -> Doc
forall a. TError a -> Doc
hint TError a
err
           ]

ppError' Tidy
_ Doc
dCtx (ErrOther SrcSpan
_ Doc
s)
  = String -> Doc
text String
"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)
  = String -> Doc
text String
"Termination Error"
        Doc -> Doc -> Doc
$+$ Doc
dCtx
        Doc -> Doc -> Doc
<+> ([Doc] -> Doc
hsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
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)
  = String -> Doc
text String
"Structural Termination Error"
        Doc -> Doc -> Doc
$+$ Doc
dCtx
        Doc -> Doc -> Doc
<+> (String -> Doc
text String
"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)
  = String -> Doc
text String
"Law Instance Error"
        Doc -> Doc -> Doc
$+$ Doc
dCtx
        Doc -> Doc -> Doc
<+> (String -> Doc
text String
"The instance" Doc -> Doc -> Doc
<+> Doc
i Doc -> Doc -> Doc
<+> String -> Doc
text String
"of class" Doc -> Doc -> Doc
<+> Doc
c Doc -> Doc -> Doc
<+> String -> Doc
text String
"is not valid.") Doc -> Doc -> Doc
$+$ Doc
s

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

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

ppError' Tidy
_ Doc
dCtx (ErrTyCon SrcSpan
_ Doc
msg Doc
ty)
  = String -> Doc
text String
"Illegal data refinement for" Doc -> Doc -> 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 )
  = String -> Doc
text String
"Rewrite error"
        Doc -> Doc -> Doc
$+$ Doc
dCtx
        Doc -> Doc -> Doc
$+$ Int -> Doc -> Doc
nest Int
4 Doc
msg

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

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

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

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

ppNames :: [Doc] -> Doc
ppNames :: [Doc] -> Doc
ppNames [Doc]
ds = Doc -> [Doc] -> Doc
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 :: Doc -> [a] -> Doc
ppList Doc
d [a]
ls
  = Int -> Doc -> Doc
nest Int
4 (Doc -> [Doc] -> Doc
sepVcat Doc
blankLine (Doc
d Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: [ String -> Doc
text String
"*" Doc -> Doc -> Doc
<+> a -> 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 :: String -> SourceError -> [TError t]
sourceErrors String
s = (ErrMsg -> [TError t]) -> [ErrMsg] -> [TError t]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (String -> ErrMsg -> [TError t]
forall t. String -> ErrMsg -> [TError t]
errMsgErrors String
s) ([ErrMsg] -> [TError t])
-> (SourceError -> [ErrMsg]) -> SourceError -> [TError t]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bag ErrMsg -> [ErrMsg]
forall a. Bag a -> [a]
bagToList (Bag ErrMsg -> [ErrMsg])
-> (SourceError -> Bag ErrMsg) -> SourceError -> [ErrMsg]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SourceError -> Bag ErrMsg
srcErrorMessages

errMsgErrors :: String -> ErrMsg -> [TError t]
errMsgErrors :: String -> ErrMsg -> [TError t]
errMsgErrors String
s ErrMsg
e = [ SrcSpan -> Doc -> TError t
forall t. SrcSpan -> Doc -> TError t
ErrGhc (ErrMsg -> SrcSpan
errMsgSpan ErrMsg
e) Doc
msg ]
   where
     msg :: Doc
msg         =  String -> Doc
text String
s
                Doc -> Doc -> Doc
$+$ Int -> Doc -> Doc
nest Int
4 (String -> Doc
text (ErrMsg -> String
forall a. Show a => a -> String
show ErrMsg
e))