{-# LANGUAGE CPP                       #-}
{-# LANGUAGE DeriveDataTypeable        #-}
{-# LANGUAGE DeriveGeneric             #-}
{-# LANGUAGE DeriveFoldable            #-}
{-# LANGUAGE DeriveTraversable         #-}
{-# LANGUAGE FlexibleInstances         #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE ScopedTypeVariables       #-}
{-# LANGUAGE StandaloneDeriving        #-}
{-# LANGUAGE OverloadedStrings         #-}
{-# LANGUAGE ViewPatterns              #-}

{-# OPTIONS_GHC -fno-warn-orphans #-}

module Language.Fixpoint.Types.Errors (
  -- * Concrete Location Type
    SrcSpan (..)
  , dummySpan
  , sourcePosElts

  -- * Result

  , FixResult (..)
  , colorResult
  , resultDoc
  , resultExit 

  -- * Error Type
  , Error, Error1

  -- * Constructor
  , err

  -- * Accessors
  , errLoc
  , errMsg
  , errs

  -- * Adding Insult to Injury
  , catError
  , catErrors

  -- * Fatal Exit
  , panic
  , die
  , dieAt
  , exit

  -- * Some popular errors
  , errFreeVarInQual
  , errFreeVarInConstraint
  , errIllScopedKVar
  ) where

import           System.Exit                        (ExitCode (..))
import           Control.Exception
import           Data.Serialize                (Serialize (..))
import           Data.Generics                 (Data)
import           Data.Typeable
#if !MIN_VERSION_base(4,14,0)
import           Data.Semigroup                (Semigroup (..))
#endif

import           Control.DeepSeq
-- import           Data.Hashable
import qualified Data.Binary                   as B
import           GHC.Generics                  (Generic)
import           Language.Fixpoint.Types.PrettyPrint
import           Language.Fixpoint.Types.Spans
import           Language.Fixpoint.Misc
import qualified Language.Fixpoint.Solver.Stats as Solver
import           Text.PrettyPrint.HughesPJ.Compat
-- import           Text.Printf
import           Data.Function (on)

-- import           Debug.Trace

import qualified Text.PrettyPrint.Annotated.HughesPJ as Ann

deriving instance Generic (Ann.AnnotDetails a)
instance Serialize a => Serialize (Ann.AnnotDetails a)
instance Serialize a => Serialize (Ann.Doc a)

instance Serialize Error1
-- FIXME: orphans are bad...
instance Serialize TextDetails

instance Serialize Doc
instance Serialize Error
instance Serialize (FixResult Error)

instance (B.Binary a) => B.Binary (FixResult a)

--------------------------------------------------------------------------------
-- | A BareBones Error Type ----------------------------------------------------
--------------------------------------------------------------------------------

newtype Error = Error [Error1]
                deriving (Error -> Error -> Bool
(Error -> Error -> Bool) -> (Error -> Error -> Bool) -> Eq Error
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Error -> Error -> Bool
$c/= :: Error -> Error -> Bool
== :: Error -> Error -> Bool
$c== :: Error -> Error -> Bool
Eq, Eq Error
Eq Error
-> (Error -> Error -> Ordering)
-> (Error -> Error -> Bool)
-> (Error -> Error -> Bool)
-> (Error -> Error -> Bool)
-> (Error -> Error -> Bool)
-> (Error -> Error -> Error)
-> (Error -> Error -> Error)
-> Ord Error
Error -> Error -> Bool
Error -> Error -> Ordering
Error -> Error -> Error
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Error -> Error -> Error
$cmin :: Error -> Error -> Error
max :: Error -> Error -> Error
$cmax :: Error -> Error -> Error
>= :: Error -> Error -> Bool
$c>= :: Error -> Error -> Bool
> :: Error -> Error -> Bool
$c> :: Error -> Error -> Bool
<= :: Error -> Error -> Bool
$c<= :: Error -> Error -> Bool
< :: Error -> Error -> Bool
$c< :: Error -> Error -> Bool
compare :: Error -> Error -> Ordering
$ccompare :: Error -> Error -> Ordering
$cp1Ord :: Eq Error
Ord, Int -> Error -> ShowS
[Error] -> ShowS
Error -> String
(Int -> Error -> ShowS)
-> (Error -> String) -> ([Error] -> ShowS) -> Show Error
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Error] -> ShowS
$cshowList :: [Error] -> ShowS
show :: Error -> String
$cshow :: Error -> String
showsPrec :: Int -> Error -> ShowS
$cshowsPrec :: Int -> Error -> ShowS
Show, Typeable, (forall x. Error -> Rep Error x)
-> (forall x. Rep Error x -> Error) -> Generic Error
forall x. Rep Error x -> Error
forall x. Error -> Rep Error x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Error x -> Error
$cfrom :: forall x. Error -> Rep Error x
Generic)


errs :: Error -> [Error1]
errs :: Error -> [Error1]
errs (Error [Error1]
es) = [Error1]
es 

data Error1 = Error1
  { Error1 -> SrcSpan
errLoc :: SrcSpan
  , Error1 -> Doc
errMsg :: Doc
  } deriving (Error1 -> Error1 -> Bool
(Error1 -> Error1 -> Bool)
-> (Error1 -> Error1 -> Bool) -> Eq Error1
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Error1 -> Error1 -> Bool
$c/= :: Error1 -> Error1 -> Bool
== :: Error1 -> Error1 -> Bool
$c== :: Error1 -> Error1 -> Bool
Eq, Int -> Error1 -> ShowS
[Error1] -> ShowS
Error1 -> String
(Int -> Error1 -> ShowS)
-> (Error1 -> String) -> ([Error1] -> ShowS) -> Show Error1
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Error1] -> ShowS
$cshowList :: [Error1] -> ShowS
show :: Error1 -> String
$cshow :: Error1 -> String
showsPrec :: Int -> Error1 -> ShowS
$cshowsPrec :: Int -> Error1 -> ShowS
Show, Typeable, (forall x. Error1 -> Rep Error1 x)
-> (forall x. Rep Error1 x -> Error1) -> Generic Error1
forall x. Rep Error1 x -> Error1
forall x. Error1 -> Rep Error1 x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Error1 x -> Error1
$cfrom :: forall x. Error1 -> Rep Error1 x
Generic)

instance Ord Error1 where
  compare :: Error1 -> Error1 -> Ordering
compare = SrcSpan -> SrcSpan -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (SrcSpan -> SrcSpan -> Ordering)
-> (Error1 -> SrcSpan) -> Error1 -> Error1 -> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Error1 -> SrcSpan
errLoc

instance PPrint Error1 where
  pprintTidy :: Tidy -> Error1 -> Doc
pprintTidy Tidy
k (Error1 SrcSpan
l Doc
msg) = (Tidy -> SrcSpan -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k SrcSpan
l Doc -> Doc -> Doc
<-> Doc
": Error")
                                Doc -> Doc -> Doc
$+$ Int -> Doc -> Doc
nest Int
2 Doc
msg

instance PPrint Error where
  pprintTidy :: Tidy -> Error -> Doc
pprintTidy Tidy
k (Error [Error1]
es) = [Doc] -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Tidy -> Error1 -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k (Error1 -> Doc) -> [Error1] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Error1]
es

instance Fixpoint Error1 where
  toFix :: Error1 -> Doc
toFix = Error1 -> Doc
forall a. PPrint a => a -> Doc
pprint

instance Exception Error
instance Exception (FixResult Error)


---------------------------------------------------------------------
catError :: Error -> Error -> Error
---------------------------------------------------------------------
catError :: Error -> Error -> Error
catError (Error [Error1]
e1) (Error [Error1]
e2) = [Error1] -> Error
Error ([Error1]
e1 [Error1] -> [Error1] -> [Error1]
forall a. [a] -> [a] -> [a]
++ [Error1]
e2)

---------------------------------------------------------------------
catErrors :: ListNE Error -> Error
---------------------------------------------------------------------
catErrors :: [Error] -> Error
catErrors = (Error -> Error -> Error) -> [Error] -> Error
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 Error -> Error -> Error
catError

---------------------------------------------------------------------
err :: SrcSpan -> Doc -> Error
---------------------------------------------------------------------
err :: SrcSpan -> Doc -> Error
err SrcSpan
sp Doc
d = [Error1] -> Error
Error [SrcSpan -> Doc -> Error1
Error1 SrcSpan
sp Doc
d]

---------------------------------------------------------------------
panic :: String -> a
---------------------------------------------------------------------
panic :: String -> a
panic = Error -> a
forall a. Error -> a
die (Error -> a) -> (String -> Error) -> String -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SrcSpan -> Doc -> Error
err SrcSpan
dummySpan (Doc -> Error) -> (String -> Doc) -> String -> Error
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Doc
text (String -> Doc) -> ShowS -> String -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String
panicMsg String -> ShowS
forall a. [a] -> [a] -> [a]
++)

panicMsg :: String
panicMsg :: String
panicMsg = String
"PANIC: Please file an issue at https://github.com/ucsd-progsys/liquid-fixpoint \n"

---------------------------------------------------------------------
die :: Error -> a
---------------------------------------------------------------------
die :: Error -> a
die = Error -> a
forall a e. Exception e => e -> a
throw

---------------------------------------------------------------------
dieAt :: SrcSpan -> Error -> a
---------------------------------------------------------------------
dieAt :: SrcSpan -> Error -> a
dieAt SrcSpan
sp (Error [Error1]
es) = Error -> a
forall a. Error -> a
die ([Error1] -> Error
Error [ Error1
e {errLoc :: SrcSpan
errLoc = SrcSpan
sp} | Error1
e <- [Error1]
es])

---------------------------------------------------------------------
exit :: a -> IO a -> IO a
---------------------------------------------------------------------
exit :: a -> IO a -> IO a
exit a
def IO a
act = IO a -> (Error -> IO a) -> IO a
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
catch IO a
act ((Error -> IO a) -> IO a) -> (Error -> IO a) -> IO a
forall a b. (a -> b) -> a -> b
$ \(Error
e :: Error) -> do
  Doc -> IO ()
putDocLn (Doc -> IO ()) -> Doc -> IO ()
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
vcat [Doc
"Unexpected Errors!", Error -> Doc
forall a. PPrint a => a -> Doc
pprint Error
e]
  a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return a
def

putDocLn :: Doc -> IO ()
putDocLn :: Doc -> IO ()
putDocLn = String -> IO ()
putStrLn (String -> IO ()) -> (Doc -> String) -> Doc -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> String
render
---------------------------------------------------------------------
-- | Result ---------------------------------------------------------
---------------------------------------------------------------------

data FixResult a = Crash [a] String
                 | Safe Solver.Stats
                 -- ^ The 'Solver' statistics, which include also the constraints /actually/
                 -- checked. A program will be \"trivially safe\" in case this
                 -- number is 0.
                 | Unsafe Solver.Stats ![a]
                   deriving (Typeable (FixResult a)
DataType
Constr
Typeable (FixResult a)
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> FixResult a -> c (FixResult a))
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (FixResult a))
-> (FixResult a -> Constr)
-> (FixResult a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (FixResult a)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (FixResult a)))
-> ((forall b. Data b => b -> b) -> FixResult a -> FixResult a)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> FixResult a -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> FixResult a -> r)
-> (forall u. (forall d. Data d => d -> u) -> FixResult a -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> FixResult a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> FixResult a -> m (FixResult a))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> FixResult a -> m (FixResult a))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> FixResult a -> m (FixResult a))
-> Data (FixResult a)
FixResult a -> DataType
FixResult a -> Constr
(forall d. Data d => c (t d)) -> Maybe (c (FixResult a))
(forall b. Data b => b -> b) -> FixResult a -> FixResult a
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> FixResult a -> c (FixResult a)
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (FixResult a)
forall a. Data a => Typeable (FixResult a)
forall a. Data a => FixResult a -> DataType
forall a. Data a => FixResult a -> Constr
forall a.
Data a =>
(forall b. Data b => b -> b) -> FixResult a -> FixResult a
forall a u.
Data a =>
Int -> (forall d. Data d => d -> u) -> FixResult a -> u
forall a u.
Data a =>
(forall d. Data d => d -> u) -> FixResult a -> [u]
forall a r r'.
Data a =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> FixResult a -> r
forall a r r'.
Data a =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> FixResult a -> r
forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d) -> FixResult a -> m (FixResult a)
forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> FixResult a -> m (FixResult a)
forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (FixResult a)
forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> FixResult a -> c (FixResult a)
forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (FixResult a))
forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (FixResult a))
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) -> FixResult a -> u
forall u. (forall d. Data d => d -> u) -> FixResult a -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> FixResult a -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> FixResult a -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> FixResult a -> m (FixResult a)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> FixResult a -> m (FixResult a)
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (FixResult a)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> FixResult a -> c (FixResult a)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (FixResult a))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (FixResult a))
$cUnsafe :: Constr
$cSafe :: Constr
$cCrash :: Constr
$tFixResult :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> FixResult a -> m (FixResult a)
$cgmapMo :: forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> FixResult a -> m (FixResult a)
gmapMp :: (forall d. Data d => d -> m d) -> FixResult a -> m (FixResult a)
$cgmapMp :: forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> FixResult a -> m (FixResult a)
gmapM :: (forall d. Data d => d -> m d) -> FixResult a -> m (FixResult a)
$cgmapM :: forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d) -> FixResult a -> m (FixResult a)
gmapQi :: Int -> (forall d. Data d => d -> u) -> FixResult a -> u
$cgmapQi :: forall a u.
Data a =>
Int -> (forall d. Data d => d -> u) -> FixResult a -> u
gmapQ :: (forall d. Data d => d -> u) -> FixResult a -> [u]
$cgmapQ :: forall a u.
Data a =>
(forall d. Data d => d -> u) -> FixResult a -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> FixResult a -> r
$cgmapQr :: forall a r r'.
Data a =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> FixResult a -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> FixResult a -> r
$cgmapQl :: forall a r r'.
Data a =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> FixResult a -> r
gmapT :: (forall b. Data b => b -> b) -> FixResult a -> FixResult a
$cgmapT :: forall a.
Data a =>
(forall b. Data b => b -> b) -> FixResult a -> FixResult a
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (FixResult a))
$cdataCast2 :: forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (FixResult a))
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c (FixResult a))
$cdataCast1 :: forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (FixResult a))
dataTypeOf :: FixResult a -> DataType
$cdataTypeOf :: forall a. Data a => FixResult a -> DataType
toConstr :: FixResult a -> Constr
$ctoConstr :: forall a. Data a => FixResult a -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (FixResult a)
$cgunfold :: forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (FixResult a)
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> FixResult a -> c (FixResult a)
$cgfoldl :: forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> FixResult a -> c (FixResult a)
$cp1Data :: forall a. Data a => Typeable (FixResult a)
Data, Typeable, FixResult a -> Bool
(a -> m) -> FixResult a -> m
(a -> b -> b) -> b -> FixResult a -> b
(forall m. Monoid m => FixResult m -> m)
-> (forall m a. Monoid m => (a -> m) -> FixResult a -> m)
-> (forall m a. Monoid m => (a -> m) -> FixResult a -> m)
-> (forall a b. (a -> b -> b) -> b -> FixResult a -> b)
-> (forall a b. (a -> b -> b) -> b -> FixResult a -> b)
-> (forall b a. (b -> a -> b) -> b -> FixResult a -> b)
-> (forall b a. (b -> a -> b) -> b -> FixResult a -> b)
-> (forall a. (a -> a -> a) -> FixResult a -> a)
-> (forall a. (a -> a -> a) -> FixResult a -> a)
-> (forall a. FixResult a -> [a])
-> (forall a. FixResult a -> Bool)
-> (forall a. FixResult a -> Int)
-> (forall a. Eq a => a -> FixResult a -> Bool)
-> (forall a. Ord a => FixResult a -> a)
-> (forall a. Ord a => FixResult a -> a)
-> (forall a. Num a => FixResult a -> a)
-> (forall a. Num a => FixResult a -> a)
-> Foldable FixResult
forall a. Eq a => a -> FixResult a -> Bool
forall a. Num a => FixResult a -> a
forall a. Ord a => FixResult a -> a
forall m. Monoid m => FixResult m -> m
forall a. FixResult a -> Bool
forall a. FixResult a -> Int
forall a. FixResult a -> [a]
forall a. (a -> a -> a) -> FixResult a -> a
forall m a. Monoid m => (a -> m) -> FixResult a -> m
forall b a. (b -> a -> b) -> b -> FixResult a -> b
forall a b. (a -> b -> b) -> b -> FixResult a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: FixResult a -> a
$cproduct :: forall a. Num a => FixResult a -> a
sum :: FixResult a -> a
$csum :: forall a. Num a => FixResult a -> a
minimum :: FixResult a -> a
$cminimum :: forall a. Ord a => FixResult a -> a
maximum :: FixResult a -> a
$cmaximum :: forall a. Ord a => FixResult a -> a
elem :: a -> FixResult a -> Bool
$celem :: forall a. Eq a => a -> FixResult a -> Bool
length :: FixResult a -> Int
$clength :: forall a. FixResult a -> Int
null :: FixResult a -> Bool
$cnull :: forall a. FixResult a -> Bool
toList :: FixResult a -> [a]
$ctoList :: forall a. FixResult a -> [a]
foldl1 :: (a -> a -> a) -> FixResult a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> FixResult a -> a
foldr1 :: (a -> a -> a) -> FixResult a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> FixResult a -> a
foldl' :: (b -> a -> b) -> b -> FixResult a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> FixResult a -> b
foldl :: (b -> a -> b) -> b -> FixResult a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> FixResult a -> b
foldr' :: (a -> b -> b) -> b -> FixResult a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> FixResult a -> b
foldr :: (a -> b -> b) -> b -> FixResult a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> FixResult a -> b
foldMap' :: (a -> m) -> FixResult a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> FixResult a -> m
foldMap :: (a -> m) -> FixResult a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> FixResult a -> m
fold :: FixResult m -> m
$cfold :: forall m. Monoid m => FixResult m -> m
Foldable, Functor FixResult
Foldable FixResult
Functor FixResult
-> Foldable FixResult
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> FixResult a -> f (FixResult b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    FixResult (f a) -> f (FixResult a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> FixResult a -> m (FixResult b))
-> (forall (m :: * -> *) a.
    Monad m =>
    FixResult (m a) -> m (FixResult a))
-> Traversable FixResult
(a -> f b) -> FixResult a -> f (FixResult b)
forall (t :: * -> *).
Functor t
-> Foldable t
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a.
Monad m =>
FixResult (m a) -> m (FixResult a)
forall (f :: * -> *) a.
Applicative f =>
FixResult (f a) -> f (FixResult a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> FixResult a -> m (FixResult b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> FixResult a -> f (FixResult b)
sequence :: FixResult (m a) -> m (FixResult a)
$csequence :: forall (m :: * -> *) a.
Monad m =>
FixResult (m a) -> m (FixResult a)
mapM :: (a -> m b) -> FixResult a -> m (FixResult b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> FixResult a -> m (FixResult b)
sequenceA :: FixResult (f a) -> f (FixResult a)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
FixResult (f a) -> f (FixResult a)
traverse :: (a -> f b) -> FixResult a -> f (FixResult b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> FixResult a -> f (FixResult b)
$cp2Traversable :: Foldable FixResult
$cp1Traversable :: Functor FixResult
Traversable, Int -> FixResult a -> ShowS
[FixResult a] -> ShowS
FixResult a -> String
(Int -> FixResult a -> ShowS)
-> (FixResult a -> String)
-> ([FixResult a] -> ShowS)
-> Show (FixResult a)
forall a. Show a => Int -> FixResult a -> ShowS
forall a. Show a => [FixResult a] -> ShowS
forall a. Show a => FixResult a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [FixResult a] -> ShowS
$cshowList :: forall a. Show a => [FixResult a] -> ShowS
show :: FixResult a -> String
$cshow :: forall a. Show a => FixResult a -> String
showsPrec :: Int -> FixResult a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> FixResult a -> ShowS
Show, (forall x. FixResult a -> Rep (FixResult a) x)
-> (forall x. Rep (FixResult a) x -> FixResult a)
-> Generic (FixResult a)
forall x. Rep (FixResult a) x -> FixResult a
forall x. FixResult a -> Rep (FixResult a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (FixResult a) x -> FixResult a
forall a x. FixResult a -> Rep (FixResult a) x
$cto :: forall a x. Rep (FixResult a) x -> FixResult a
$cfrom :: forall a x. FixResult a -> Rep (FixResult a) x
Generic)

instance (NFData a) => NFData (FixResult a)

instance Eq a => Eq (FixResult a) where
  Crash [a]
xs String
_   == :: FixResult a -> FixResult a -> Bool
== Crash [a]
ys String
_         = [a]
xs [a] -> [a] -> Bool
forall a. Eq a => a -> a -> Bool
== [a]
ys
  Unsafe Stats
s1 [a]
xs == Unsafe Stats
s2 [a]
ys       = [a]
xs [a] -> [a] -> Bool
forall a. Eq a => a -> a -> Bool
== [a]
ys Bool -> Bool -> Bool
&& Stats
s1 Stats -> Stats -> Bool
forall a. Eq a => a -> a -> Bool
== Stats
s2 
  Safe Stats
s1      == Safe Stats
s2            = Stats
s1 Stats -> Stats -> Bool
forall a. Eq a => a -> a -> Bool
== Stats
s2
  FixResult a
_            == FixResult a
_                  = Bool
False

instance Semigroup (FixResult a) where
  Safe Stats
s1        <> :: FixResult a -> FixResult a -> FixResult a
<> Safe Stats
s2        = Stats -> FixResult a
forall a. Stats -> FixResult a
Safe (Stats
s1 Stats -> Stats -> Stats
forall a. Semigroup a => a -> a -> a
<> Stats
s2)
  Safe Stats
_         <> FixResult a
x              = FixResult a
x
  FixResult a
x              <> Safe Stats
_         = FixResult a
x
  FixResult a
_              <> c :: FixResult a
c@(Crash{})    = FixResult a
c
  c :: FixResult a
c@(Crash{})    <> FixResult a
_              = FixResult a
c
  (Unsafe Stats
s1 [a]
xs) <> (Unsafe Stats
s2 [a]
ys) = Stats -> [a] -> FixResult a
forall a. Stats -> [a] -> FixResult a
Unsafe (Stats
s1 Stats -> Stats -> Stats
forall a. Semigroup a => a -> a -> a
<> Stats
s2) ([a]
xs [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ [a]
ys)

instance Monoid (FixResult a) where
  mempty :: FixResult a
mempty  = Stats -> FixResult a
forall a. Stats -> FixResult a
Safe Stats
forall a. Monoid a => a
mempty
  mappend :: FixResult a -> FixResult a -> FixResult a
mappend = FixResult a -> FixResult a -> FixResult a
forall a. Semigroup a => a -> a -> a
(<>)

instance Functor FixResult where
  fmap :: (a -> b) -> FixResult a -> FixResult b
fmap a -> b
f (Crash [a]
xs String
msg)   = [b] -> String -> FixResult b
forall a. [a] -> String -> FixResult a
Crash (a -> b
f (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [a]
xs) String
msg
  fmap a -> b
f (Unsafe Stats
s [a]
xs)    = Stats -> [b] -> FixResult b
forall a. Stats -> [a] -> FixResult a
Unsafe Stats
s (a -> b
f (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [a]
xs)
  fmap a -> b
_ (Safe Stats
stats)     = Stats -> FixResult b
forall a. Stats -> FixResult a
Safe Stats
stats

resultDoc :: (Fixpoint a) => FixResult a -> Doc
resultDoc :: FixResult a -> Doc
resultDoc (Safe Stats
stats)     = String -> Doc
text String
"Safe (" Doc -> Doc -> Doc
<+> String -> Doc
text (Int -> String
forall a. Show a => a -> String
show (Int -> String) -> Int -> String
forall a b. (a -> b) -> a -> b
$ Stats -> Int
Solver.checked Stats
stats) Doc -> Doc -> Doc
<+> Doc
" constraints checked)" 
resultDoc (Crash [a]
xs String
msg)   = [Doc] -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
text (String
"Crash!: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
msg) Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: (((Doc
"CRASH:" Doc -> Doc -> Doc
<+>) (Doc -> Doc) -> (a -> Doc) -> a -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Doc
forall a. Fixpoint a => a -> Doc
toFix) (a -> Doc) -> [a] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [a]
xs)
resultDoc (Unsafe Stats
_ [a]
xs)    = [Doc] -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
text String
"Unsafe:"           Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: (((Doc
"WARNING:" Doc -> Doc -> Doc
<+>) (Doc -> Doc) -> (a -> Doc) -> a -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Doc
forall a. Fixpoint a => a -> Doc
toFix) (a -> Doc) -> [a] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [a]
xs)

colorResult :: FixResult a -> Moods
colorResult :: FixResult a -> Moods
colorResult (Safe (Stats -> Int
Solver.totalWork -> Int
0)) = Moods
Wary
colorResult (Safe Stats
_)                       = Moods
Happy
colorResult (Unsafe Stats
_ [a]
_)                   = Moods
Angry
colorResult (FixResult a
_)                            = Moods
Sad

resultExit :: FixResult a -> ExitCode
resultExit :: FixResult a -> ExitCode
resultExit (Safe Stats
_stats) = ExitCode
ExitSuccess
resultExit FixResult a
_             = Int -> ExitCode
ExitFailure Int
1

---------------------------------------------------------------------
-- | Catalogue of Errors --------------------------------------------
---------------------------------------------------------------------

errFreeVarInQual :: (PPrint q, Loc q, PPrint x) => q -> x -> Error
errFreeVarInQual :: q -> x -> Error
errFreeVarInQual q
q x
x = SrcSpan -> Doc -> Error
err SrcSpan
sp (Doc -> Error) -> Doc -> Error
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
vcat [ Doc
"Qualifier with free vars"
                                     , q -> Doc
forall a. PPrint a => a -> Doc
pprint q
q
                                     , x -> Doc
forall a. PPrint a => a -> Doc
pprint x
x ]
  where
    sp :: SrcSpan
sp               = q -> SrcSpan
forall a. Loc a => a -> SrcSpan
srcSpan q
q

errFreeVarInConstraint :: (PPrint a) => (Integer, a) -> Error
errFreeVarInConstraint :: (Integer, a) -> Error
errFreeVarInConstraint (Integer
i, a
ss) = SrcSpan -> Doc -> Error
err SrcSpan
dummySpan (Doc -> Error) -> Doc -> Error
forall a b. (a -> b) -> a -> b
$
  [Doc] -> Doc
vcat [ Doc
"Constraint with free vars"
       , Integer -> Doc
forall a. PPrint a => a -> Doc
pprint Integer
i
       , a -> Doc
forall a. PPrint a => a -> Doc
pprint a
ss
       , Doc
"Try using the --prune-unsorted flag"
       ]

errIllScopedKVar :: (PPrint k, PPrint bs) => (k, Integer, Integer, bs) -> Error
errIllScopedKVar :: (k, Integer, Integer, bs) -> Error
errIllScopedKVar (k
k, Integer
inId, Integer
outId, bs
xs) = SrcSpan -> Doc -> Error
err SrcSpan
dummySpan (Doc -> Error) -> Doc -> Error
forall a b. (a -> b) -> a -> b
$
  [Doc] -> Doc
vcat [ Doc
"Ill-scoped KVar" Doc -> Doc -> Doc
<+> k -> Doc
forall a. PPrint a => a -> Doc
pprint k
k
       , Doc
"Missing common binders at def" Doc -> Doc -> Doc
<+> Integer -> Doc
forall a. PPrint a => a -> Doc
pprint Integer
inId Doc -> Doc -> Doc
<+> Doc
"and use" Doc -> Doc -> Doc
<+> Integer -> Doc
forall a. PPrint a => a -> Doc
pprint Integer
outId
       , bs -> Doc
forall a. PPrint a => a -> Doc
pprint bs
xs
       ]