{-# 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 (
SrcSpan (..)
, dummySpan
, sourcePosElts
, FixResult (..)
, colorResult
, resultDoc
, resultExit
, Error, Error1
, err
, errLoc
, errMsg
, errs
, catError
, catErrors
, panic
, die
, dieAt
, exit
, 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 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 Data.Function (on)
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
instance Serialize TextDetails
instance Serialize Doc
instance Serialize Error
instance Serialize (FixResult Error)
instance (S.Store a) => S.Store (FixResult a)
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
$c== :: Error -> Error -> Bool
== :: Error -> Error -> Bool
$c/= :: Error -> Error -> Bool
/= :: 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
$ccompare :: Error -> Error -> Ordering
compare :: Error -> Error -> Ordering
$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
>= :: Error -> Error -> Bool
$cmax :: Error -> Error -> Error
max :: Error -> Error -> Error
$cmin :: Error -> Error -> Error
min :: Error -> Error -> 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
$cshowsPrec :: Int -> Error -> ShowS
showsPrec :: Int -> Error -> ShowS
$cshow :: Error -> String
show :: Error -> String
$cshowList :: [Error] -> ShowS
showList :: [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
$cfrom :: forall x. Error -> Rep Error x
from :: forall x. Error -> Rep Error x
$cto :: forall x. Rep Error x -> Error
to :: forall x. Rep Error x -> Error
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
$c== :: Error1 -> Error1 -> Bool
== :: Error1 -> Error1 -> Bool
$c/= :: Error1 -> Error1 -> Bool
/= :: 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
$cshowsPrec :: Int -> Error1 -> ShowS
showsPrec :: Int -> Error1 -> ShowS
$cshow :: Error1 -> String
show :: Error1 -> String
$cshowList :: [Error1] -> ShowS
showList :: [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
$cfrom :: forall x. Error1 -> Rep Error1 x
from :: forall x. Error1 -> Rep Error1 x
$cto :: forall x. Rep Error1 x -> Error1
to :: forall x. Rep Error1 x -> Error1
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
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 a. (a -> a -> a) -> [a] -> a
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 = 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 :: forall a. Error -> a
die = Error -> a
forall a e. Exception e => e -> a
throw
dieAt :: SrcSpan -> Error -> a
dieAt :: forall a. SrcSpan -> Error -> a
dieAt SrcSpan
sp (Error [Error1]
es) = Error -> a
forall a. Error -> a
die ([Error1] -> Error
Error [ Error1
e {errLoc = 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 = 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 a. 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
data FixResult a
= Crash [(a, Maybe String)] String
| Unsafe Solver.Stats ![a]
| Safe Solver.Stats
deriving (Typeable (FixResult a)
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 -> Constr
FixResult a -> DataType
(forall b. Data b => b -> b) -> FixResult a -> FixResult a
forall a. Data a => Typeable (FixResult a)
forall a. Data a => FixResult a -> Constr
forall a. Data a => FixResult a -> DataType
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))
$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)
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> FixResult a -> 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)
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (FixResult a)
$ctoConstr :: forall a. Data a => FixResult a -> Constr
toConstr :: FixResult a -> Constr
$cdataTypeOf :: forall a. Data a => FixResult a -> DataType
dataTypeOf :: FixResult a -> DataType
$cdataCast1 :: forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (FixResult a))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> 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))
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (FixResult a))
$cgmapT :: forall a.
Data a =>
(forall b. Data b => b -> b) -> FixResult a -> FixResult a
gmapT :: (forall b. Data b => b -> b) -> FixResult a -> FixResult a
$cgmapQl :: 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
$cgmapQr :: forall a r r'.
Data a =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> FixResult a -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> FixResult a -> r
$cgmapQ :: forall a u.
Data a =>
(forall d. Data d => d -> u) -> FixResult a -> [u]
gmapQ :: forall u. (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
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> FixResult a -> u
$cgmapM :: forall a (m :: * -> *).
(Data a, Monad 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)
$cgmapMp :: 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)
$cgmapMo :: forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> FixResult a -> m (FixResult a)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> FixResult a -> m (FixResult a)
Data, Typeable, (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
$cfold :: forall m. Monoid m => FixResult m -> m
fold :: forall m. Monoid m => FixResult m -> 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
foldMap' :: forall m a. Monoid m => (a -> m) -> FixResult a -> m
$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
foldr' :: forall a b. (a -> b -> 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
foldl' :: forall b a. (b -> a -> b) -> b -> FixResult a -> b
$cfoldr1 :: forall a. (a -> a -> a) -> FixResult a -> a
foldr1 :: forall a. (a -> a -> a) -> FixResult a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> FixResult a -> a
foldl1 :: forall a. (a -> a -> a) -> FixResult a -> a
$ctoList :: forall a. FixResult a -> [a]
toList :: forall a. FixResult a -> [a]
$cnull :: forall a. FixResult a -> Bool
null :: forall a. FixResult a -> Bool
$clength :: forall a. FixResult a -> Int
length :: forall a. FixResult a -> Int
$celem :: forall a. Eq a => a -> FixResult a -> Bool
elem :: forall a. Eq a => a -> FixResult a -> Bool
$cmaximum :: forall a. Ord a => FixResult a -> a
maximum :: forall a. Ord a => FixResult a -> a
$cminimum :: forall a. Ord a => FixResult a -> a
minimum :: forall a. Ord a => FixResult a -> a
$csum :: forall a. Num a => FixResult a -> a
sum :: forall a. Num a => FixResult a -> a
$cproduct :: forall a. Num a => FixResult a -> a
product :: forall a. Num a => FixResult a -> a
Foldable, (forall a b. (a -> b) -> FixResult a -> FixResult b)
-> (forall a b. a -> FixResult b -> FixResult a)
-> Functor FixResult
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
$cfmap :: forall a b. (a -> b) -> FixResult a -> FixResult b
fmap :: forall a b. (a -> b) -> FixResult a -> FixResult b
$c<$ :: forall a b. a -> FixResult b -> FixResult a
<$ :: forall a b. a -> FixResult b -> FixResult a
Functor, 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
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)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> FixResult a -> f (FixResult b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> FixResult a -> f (FixResult b)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
FixResult (f a) -> f (FixResult a)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
FixResult (f a) -> f (FixResult a)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> FixResult a -> m (FixResult b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> FixResult a -> m (FixResult b)
$csequence :: forall (m :: * -> *) a.
Monad m =>
FixResult (m a) -> m (FixResult a)
sequence :: forall (m :: * -> *) a.
Monad m =>
FixResult (m a) -> m (FixResult a)
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
$cshowsPrec :: forall a. Show a => Int -> FixResult a -> ShowS
showsPrec :: Int -> FixResult a -> ShowS
$cshow :: forall a. Show a => FixResult a -> String
show :: FixResult a -> String
$cshowList :: forall a. Show a => [FixResult a] -> ShowS
showList :: [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
$cfrom :: forall a x. FixResult a -> Rep (FixResult a) x
from :: forall x. FixResult a -> Rep (FixResult a) x
$cto :: forall a x. Rep (FixResult a) x -> FixResult a
to :: forall x. Rep (FixResult a) x -> FixResult a
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 [(a, Maybe String)] -> [(a, Maybe String)] -> Bool
forall a. Eq a => a -> a -> Bool
== [(a, Maybe String)]
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 (ToJSON a) => ToJSON (FixResult a) where
toJSON :: FixResult a -> Value
toJSON = Options -> FixResult a -> Value
forall a.
(Generic a, GToJSON' Value Zero (Rep a)) =>
Options -> a -> Value
genericToJSON Options
defaultOptions
toEncoding :: FixResult a -> Encoding
toEncoding = Options -> FixResult a -> Encoding
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 (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, Maybe String)]
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, Maybe String) -> Doc) -> (a, Maybe String) -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Doc
forall a. Fixpoint a => a -> Doc
toFix (a -> Doc) -> ((a, Maybe String) -> a) -> (a, Maybe String) -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a, Maybe String) -> a
forall a b. (a, b) -> a
fst ((a, Maybe String) -> Doc) -> [(a, Maybe String)] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(a, Maybe String)]
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)
instance (Fixpoint a) => PPrint (FixResult a) where
pprintTidy :: Tidy -> FixResult a -> Doc
pprintTidy Tidy
_ = FixResult a -> Doc
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
errBadDataDecl :: (Loc x, PPrint x) => x -> Error
errBadDataDecl :: forall x. (Loc x, PPrint x) => x -> Error
errBadDataDecl x
d = SrcSpan -> Doc -> Error
err (x -> SrcSpan
forall a. Loc a => a -> SrcSpan
srcSpan x
d) (Doc -> Error) -> Doc -> Error
forall a b. (a -> b) -> a -> b
$ Doc
"Non-regular datatype declaration" Doc -> Doc -> Doc
<+> x -> 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 (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 :: forall a. PPrint a => (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 :: 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 (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
]