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

{-# OPTIONS_GHC -Wno-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
  , errBadDataDecl
  ) where

import           System.Exit                        (ExitCode (..))
import           Control.Exception
import           Data.Serialize                (Serialize (..))
import           Data.Aeson                    hiding (Error, Result)
import           Data.Generics                 (Data)
import           Data.Typeable
import           Control.DeepSeq
-- import           Data.Hashable
import qualified Data.Store                   as S
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 (S.Store a) => S.Store (FixResult a)

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

newtype Error = Error [Error1]
                deriving (Error -> Error -> Bool
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
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
Ord, Int -> Error -> ShowS
[Error] -> ShowS
Error -> String
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. 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
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
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. 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 = forall a. Ord a => a -> a -> Ordering
compare 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) = (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 forall a b. (a -> b) -> a -> b
$ forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Error1]
es

instance Fixpoint Error1 where
  toFix :: Error1 -> Doc
toFix = 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 forall a. [a] -> [a] -> [a]
++ [Error1]
e2)

---------------------------------------------------------------------
catErrors :: ListNE Error -> Error
---------------------------------------------------------------------
catErrors :: [Error] -> Error
catErrors = 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 :: forall a. String -> a
panic = forall a. Error -> a
die forall b c a. (b -> c) -> (a -> b) -> a -> c
. SrcSpan -> Doc -> Error
err SrcSpan
dummySpan forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String
panicMsg 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 :: forall a. Error -> a
die = forall a e. Exception e => e -> a
throw

---------------------------------------------------------------------
dieAt :: SrcSpan -> Error -> a
---------------------------------------------------------------------
dieAt :: forall a. SrcSpan -> Error -> a
dieAt SrcSpan
sp (Error [Error1]
es) = 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 :: forall a. a -> IO a -> IO a
exit a
def IO a
act = forall e a. Exception e => IO a -> (e -> IO a) -> IO a
catch IO a
act forall a b. (a -> b) -> a -> b
$ \(Error
e :: Error) -> do
  Doc -> IO ()
putDocLn forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
vcat [Doc
"Unexpected Errors!", forall a. PPrint a => a -> Doc
pprint Error
e]
  forall (m :: * -> *) a. Monad m => a -> m a
return a
def

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

data FixResult a
  = Crash [(a, Maybe String)] String
  | Unsafe Solver.Stats ![a]
  | 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.
  deriving (FixResult a -> DataType
FixResult a -> Constr
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 (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))
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(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 (m :: * -> *).
MonadPlus m =>
(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 (m :: * -> *).
Monad m =>
(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 :: forall u. 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 u. (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 :: forall r r'.
(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 :: forall r r'.
(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 (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(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 (t :: * -> *) (c :: * -> *).
Typeable t =>
(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 (c :: * -> *).
(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 (c :: * -> *).
(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)
Data, Typeable, 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 :: forall a. Num a => FixResult a -> a
$cproduct :: forall a. Num a => FixResult a -> a
sum :: forall a. Num a => FixResult a -> a
$csum :: forall a. Num a => FixResult a -> a
minimum :: forall a. Ord a => FixResult a -> a
$cminimum :: forall a. Ord a => FixResult a -> a
maximum :: forall a. Ord a => FixResult a -> a
$cmaximum :: forall a. Ord a => FixResult a -> a
elem :: forall a. Eq a => a -> FixResult a -> Bool
$celem :: forall a. Eq a => a -> FixResult a -> Bool
length :: forall a. FixResult a -> Int
$clength :: forall a. FixResult a -> Int
null :: forall a. FixResult a -> Bool
$cnull :: forall a. FixResult a -> Bool
toList :: forall a. FixResult a -> [a]
$ctoList :: forall a. FixResult a -> [a]
foldl1 :: forall a. (a -> a -> a) -> FixResult a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> FixResult a -> a
foldr1 :: forall a. (a -> a -> a) -> FixResult a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> FixResult a -> a
foldl' :: forall b a. (b -> a -> b) -> b -> FixResult a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> FixResult a -> b
foldl :: forall b a. (b -> a -> b) -> b -> FixResult a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> FixResult a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> FixResult a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> FixResult a -> b
foldr :: forall a b. (a -> b -> b) -> b -> FixResult a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> FixResult a -> b
foldMap' :: forall m a. Monoid m => (a -> m) -> FixResult a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> FixResult a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> FixResult a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> FixResult a -> m
fold :: forall m. Monoid m => FixResult m -> m
$cfold :: forall m. Monoid m => FixResult m -> m
Foldable, forall a b. a -> FixResult b -> FixResult a
forall a b. (a -> b) -> FixResult a -> FixResult b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> FixResult b -> FixResult a
$c<$ :: forall a b. a -> FixResult b -> FixResult a
fmap :: forall a b. (a -> b) -> FixResult a -> FixResult b
$cfmap :: forall a b. (a -> b) -> FixResult a -> FixResult b
Functor, Functor FixResult
Foldable FixResult
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 :: forall (m :: * -> *) a.
Monad m =>
FixResult (m a) -> m (FixResult a)
$csequence :: forall (m :: * -> *) a.
Monad m =>
FixResult (m a) -> m (FixResult a)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> FixResult a -> m (FixResult b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> FixResult a -> m (FixResult b)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
FixResult (f a) -> f (FixResult a)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
FixResult (f a) -> f (FixResult a)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> FixResult a -> f (FixResult b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> FixResult a -> f (FixResult b)
Traversable, Int -> FixResult a -> ShowS
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 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, Maybe String)]
xs String
_   == :: FixResult a -> FixResult a -> Bool
== Crash [(a, Maybe String)]
ys String
_         = [(a, Maybe String)]
xs forall a. Eq a => a -> a -> Bool
== [(a, Maybe String)]
ys
  Unsafe Stats
s1 [a]
xs == Unsafe Stats
s2 [a]
ys       = [a]
xs forall a. Eq a => a -> a -> Bool
== [a]
ys Bool -> Bool -> Bool
&& Stats
s1 forall a. Eq a => a -> a -> Bool
== Stats
s2
  Safe Stats
s1      == Safe Stats
s2            = Stats
s1 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        = forall a. Stats -> FixResult a
Safe (Stats
s1 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) = forall a. Stats -> [a] -> FixResult a
Unsafe (Stats
s1 forall a. Semigroup a => a -> a -> a
<> Stats
s2) ([a]
xs forall a. [a] -> [a] -> [a]
++ [a]
ys)

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

-- instance Functor FixResult where
--   fmap f (Crash xs msg)   = Crash (f <$> xs) msg
--   fmap f (Unsafe s xs)    = Unsafe s (f <$> xs)
--   fmap _ (Safe stats)     = Safe stats

instance (ToJSON a) => ToJSON (FixResult a) where
  toJSON :: FixResult a -> Value
toJSON = forall a.
(Generic a, GToJSON' Value Zero (Rep a)) =>
Options -> a -> Value
genericToJSON Options
defaultOptions
  toEncoding :: FixResult a -> Encoding
toEncoding = forall a.
(Generic a, GToJSON' Encoding Zero (Rep a)) =>
Options -> a -> Encoding
genericToEncoding Options
defaultOptions

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

instance (Fixpoint a) => PPrint (FixResult a) where
  pprintTidy :: Tidy -> FixResult a -> Doc
pprintTidy Tidy
_ = forall a. Fixpoint a => FixResult a -> Doc
resultDoc

colorResult :: FixResult a -> Moods
colorResult :: forall a. 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 :: forall a. FixResult a -> ExitCode
resultExit (Safe Stats
_stats) = ExitCode
ExitSuccess
resultExit FixResult a
_             = Int -> ExitCode
ExitFailure Int
1

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

errBadDataDecl :: (Loc x, PPrint x) => x -> Error
errBadDataDecl :: forall x. (Loc x, PPrint x) => x -> Error
errBadDataDecl x
d = SrcSpan -> Doc -> Error
err (forall a. Loc a => a -> SrcSpan
srcSpan x
d) forall a b. (a -> b) -> a -> b
$ Doc
"Non-regular datatype declaration" Doc -> Doc -> Doc
<+> forall a. PPrint a => a -> Doc
pprint x
d

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

errFreeVarInConstraint :: (PPrint a) => (Integer, a) -> Error
errFreeVarInConstraint :: forall a. PPrint a => (Integer, a) -> Error
errFreeVarInConstraint (Integer
i, a
ss) = SrcSpan -> Doc -> Error
err SrcSpan
dummySpan forall a b. (a -> b) -> a -> b
$
  [Doc] -> Doc
vcat [ Doc
"Constraint with free vars"
       , forall a. PPrint a => a -> Doc
pprint Integer
i
       , 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 :: forall k bs.
(PPrint k, PPrint bs) =>
(k, Integer, Integer, bs) -> Error
errIllScopedKVar (k
k, Integer
inId, Integer
outId, bs
xs) = SrcSpan -> Doc -> Error
err SrcSpan
dummySpan forall a b. (a -> b) -> a -> b
$
  [Doc] -> Doc
vcat [ Doc
"Ill-scoped KVar" Doc -> Doc -> Doc
<+> forall a. PPrint a => a -> Doc
pprint k
k
       , Doc
"Missing common binders at def" Doc -> Doc -> Doc
<+> forall a. PPrint a => a -> Doc
pprint Integer
inId Doc -> Doc -> Doc
<+> Doc
"and use" Doc -> Doc -> Doc
<+> forall a. PPrint a => a -> Doc
pprint Integer
outId
       , forall a. PPrint a => a -> Doc
pprint bs
xs
       ]