{-# LANGUAGE FlexibleContexts  #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE FlexibleInstances #-}

{-# OPTIONS_GHC -Wno-orphans #-}

---------------------------------------------------------------------
-- | This module contains functions for cleaning up types before
--   they are rendered, e.g. in error messages or annoations,
--   and also some PPrint instances that rely upon tidying.
---------------------------------------------------------------------

module Language.Haskell.Liquid.UX.Tidy (

    -- * Tidying functions
    tidySpecType
  , tidySymbol

    -- * Panic and Exit
  , panicError

    -- * Final result
  , Result (..)

    -- * Error to UserError
  , errorToUserError

    -- * MOVE TO TYPES
  , cinfoError
  ) where

import           Data.Hashable
import           Prelude                                   hiding (error)
import qualified Data.HashMap.Strict                       as M
import qualified Data.HashSet                              as S
import qualified Data.List                                 as L
import qualified Data.Text                                 as T
import qualified Control.Exception                         as Ex
import qualified Language.Haskell.Liquid.GHC.Misc          as GM
-- (dropModuleNames, showPpr, stringTyVar)
import           Language.Fixpoint.Types                   hiding (Result, SrcSpan, Error)
import           Language.Haskell.Liquid.Types.Types
import           Language.Haskell.Liquid.Types.RefType     (rVar, subsTyVarsMeet, FreeVar)
import           Language.Haskell.Liquid.Types.PrettyPrint
import           Data.Generics                             (everywhere, mkT)
import           Text.PrettyPrint.HughesPJ


------------------------------------------------------------------------
-- | Converting Results To Answers -------------------------------------
------------------------------------------------------------------------

class Result a where
  result :: a -> FixResult UserError

instance Result UserError where
  result :: UserError -> FixResult UserError
result UserError
e = forall a. [(a, Maybe [Char])] -> [Char] -> FixResult a
Crash [(UserError
e, forall a. Maybe a
Nothing)] [Char]
""

instance Result [Error] where
  result :: [Error] -> FixResult UserError
result [Error]
es = forall a. [(a, Maybe [Char])] -> [Char] -> FixResult a
Crash ([ (Error -> UserError
errorToUserError Error
e, forall a. Maybe a
Nothing) | Error
e <- [Error]
es]) [Char]
""

instance Result Error where
  result :: Error -> FixResult UserError
result Error
e  = forall a. Result a => a -> FixResult UserError
result [Error
e] --  Crash [pprint e] ""

instance Result (FixResult Cinfo) where
  result :: FixResult Cinfo -> FixResult UserError
result = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Error -> UserError
errorToUserError forall b c a. (b -> c) -> (a -> b) -> a -> c
. Cinfo -> Error
cinfoError)

errorToUserError :: Error -> UserError
errorToUserError :: Error -> UserError
errorToUserError = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SpecType -> Doc
ppSpecTypeErr

-- TODO: move to Types.hs
cinfoError :: Cinfo -> Error
cinfoError :: Cinfo -> Error
cinfoError (Ci SrcSpan
_ (Just Error
e) Maybe Var
_) = Error
e
cinfoError (Ci SrcSpan
l Maybe Error
_ Maybe Var
_)        = forall t. SrcSpan -> Doc -> TError t
ErrOther SrcSpan
l ([Char] -> Doc
text forall a b. (a -> b) -> a -> b
$ [Char]
"Cinfo: " forall a. [a] -> [a] -> [a]
++ forall a. Outputable a => a -> [Char]
GM.showPpr SrcSpan
l)

-------------------------------------------------------------------------
tidySpecType :: Tidy -> SpecType -> SpecType
-------------------------------------------------------------------------
tidySpecType :: Tidy -> SpecType -> SpecType
tidySpecType Tidy
k
  = SpecType -> SpecType
tidyEqual
  forall b c a. (b -> c) -> (a -> b) -> a -> c
. SpecType -> SpecType
tidyValueVars
  forall b c a. (b -> c) -> (a -> b) -> a -> c
. SpecType -> SpecType
tidyDSymbols
  forall b c a. (b -> c) -> (a -> b) -> a -> c
. Tidy -> SpecType -> SpecType
tidySymbols Tidy
k
  forall b c a. (b -> c) -> (a -> b) -> a -> c
. SpecType -> SpecType
tidyInternalRefas
  forall b c a. (b -> c) -> (a -> b) -> a -> c
. Tidy -> SpecType -> SpecType
tidyLocalRefas Tidy
k
  forall b c a. (b -> c) -> (a -> b) -> a -> c
. SpecType -> SpecType
tidyFunBinds
  forall b c a. (b -> c) -> (a -> b) -> a -> c
. SpecType -> SpecType
tidyTyVars

tidyValueVars :: SpecType -> SpecType
tidyValueVars :: SpecType -> SpecType
tidyValueVars = forall r1 r2 c tv. (r1 -> r2) -> RType c tv r1 -> RType c tv r2
mapReft forall a b. (a -> b) -> a -> b
$ \RReft
u -> RReft
u { ur_reft :: Reft
ur_reft = Reft -> Reft
tidyVV forall a b. (a -> b) -> a -> b
$ forall r. UReft r -> r
ur_reft RReft
u }

tidyVV :: Reft -> Reft
tidyVV :: Reft -> Reft
tidyVV r :: Reft
r@(Reft (Symbol
va,Expr
_))
  | Symbol -> Bool
isJunk Symbol
va = Reft -> Symbol -> Reft
shiftVV Reft
r Symbol
v'
  | Bool
otherwise = Reft
r
  where
    v' :: Symbol
v'        = if Symbol
v forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Symbol]
xs then forall a. Symbolic a => a -> Symbol
symbol (Text
"v'" :: T.Text) else Symbol
v
    v :: Symbol
v         = forall a. Symbolic a => a -> Symbol
symbol (Text
"v" :: T.Text)
    xs :: [Symbol]
xs        = forall a. Subable a => a -> [Symbol]
syms Reft
r
    isJunk :: Symbol -> Bool
isJunk    = Symbol -> Symbol -> Bool
isPrefixOfSym Symbol
"x"

tidySymbols :: Tidy -> SpecType -> SpecType
tidySymbols :: Tidy -> SpecType -> SpecType
tidySymbols Tidy
k SpecType
t = forall a. Subable a => (Symbol -> Symbol) -> a -> a
substa (Tidy -> Symbol -> Symbol
shortSymbol Tidy
k forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Symbol
tidySymbol) forall a b. (a -> b) -> a -> b
$ forall c tv r. (Symbol -> Symbol) -> RType c tv r -> RType c tv r
mapBind Symbol -> Symbol
dropBind SpecType
t
  where
    xs :: HashSet Symbol
xs          = forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList (forall a. Subable a => a -> [Symbol]
syms SpecType
t)
    dropBind :: Symbol -> Symbol
dropBind Symbol
x  = if Symbol
x forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`S.member` HashSet Symbol
xs then Symbol -> Symbol
tidySymbol Symbol
x else Symbol
nonSymbol

shortSymbol :: Tidy -> Symbol -> Symbol
shortSymbol :: Tidy -> Symbol -> Symbol
shortSymbol Tidy
Lossy = Symbol -> Symbol
GM.dropModuleNames
shortSymbol Tidy
_     = forall a. a -> a
id

tidyLocalRefas   :: Tidy -> SpecType -> SpecType
tidyLocalRefas :: Tidy -> SpecType -> SpecType
tidyLocalRefas Tidy
k = forall r1 r2 c tv. (r1 -> r2) -> RType c tv r1 -> RType c tv r2
mapReft (Tidy -> RReft -> RReft
txReft' Tidy
k)
  where
    txReft' :: Tidy -> RReft -> RReft
txReft' Tidy
Full                  = forall a. a -> a
id
    txReft' Tidy
Lossy                 = RReft -> RReft
txReft
    txReft :: RReft -> RReft
txReft RReft
u                      = RReft
u { ur_reft :: Reft
ur_reft = (Expr -> Expr) -> Reft -> Reft
mapPredReft Expr -> Expr
dropLocals forall a b. (a -> b) -> a -> b
$ forall r. UReft r -> r
ur_reft RReft
u }
    dropLocals :: Expr -> Expr
dropLocals                    = ListNE Expr -> Expr
pAnd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Symbol -> Bool
isTmp forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Subable a => a -> [Symbol]
syms) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> ListNE Expr
conjuncts
    isTmp :: Symbol -> Bool
isTmp Symbol
x                       = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Symbol -> Symbol -> Bool
`isPrefixOfSym` Symbol
x) [Symbol
anfPrefix, Symbol
"ds_"]

tidyEqual :: SpecType -> SpecType
tidyEqual :: SpecType -> SpecType
tidyEqual = forall r1 r2 c tv. (r1 -> r2) -> RType c tv r1 -> RType c tv r2
mapReft RReft -> RReft
txReft
  where
    txReft :: RReft -> RReft
txReft RReft
u                      = RReft
u { ur_reft :: Reft
ur_reft = (Expr -> Expr) -> Reft -> Reft
mapPredReft Expr -> Expr
dropInternals forall a b. (a -> b) -> a -> b
$ forall r. UReft r -> r
ur_reft RReft
u }
    dropInternals :: Expr -> Expr
dropInternals                 = ListNE Expr -> Expr
pAnd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Eq a => [a] -> [a]
L.nub forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> ListNE Expr
conjuncts

tidyInternalRefas   :: SpecType -> SpecType
tidyInternalRefas :: SpecType -> SpecType
tidyInternalRefas = forall r1 r2 c tv. (r1 -> r2) -> RType c tv r1 -> RType c tv r2
mapReft RReft -> RReft
txReft
  where
    txReft :: RReft -> RReft
txReft RReft
u                      = RReft
u { ur_reft :: Reft
ur_reft = (Expr -> Expr) -> Reft -> Reft
mapPredReft Expr -> Expr
dropInternals forall a b. (a -> b) -> a -> b
$ forall r. UReft r -> r
ur_reft RReft
u }
    dropInternals :: Expr -> Expr
dropInternals                 = ListNE Expr -> Expr
pAnd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Symbol -> Bool
isIntern forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Subable a => a -> [Symbol]
syms) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> ListNE Expr
conjuncts
    isIntern :: Symbol -> Bool
isIntern Symbol
x                    = Symbol
"is$" Symbol -> Symbol -> Bool
`isPrefixOfSym` Symbol
x Bool -> Bool -> Bool
|| Symbol
"$select" Symbol -> Symbol -> Bool
`isSuffixOfSym` Symbol
x


tidyDSymbols :: SpecType -> SpecType
tidyDSymbols :: SpecType -> SpecType
tidyDSymbols SpecType
t = forall c tv r. (Symbol -> Symbol) -> RType c tv r -> RType c tv r
mapBind Symbol -> Symbol
tx forall a b. (a -> b) -> a -> b
$ forall a. Subable a => (Symbol -> Symbol) -> a -> a
substa Symbol -> Symbol
tx SpecType
t
  where
    tx :: Symbol -> Symbol
tx         = [Symbol] -> Symbol -> Symbol
bindersTx [Symbol
x | Symbol
x <- forall a. Subable a => a -> [Symbol]
syms SpecType
t, Symbol -> Bool
isTmp Symbol
x]
    isTmp :: Symbol -> Bool
isTmp      = (Symbol
tempPrefix Symbol -> Symbol -> Bool
`isPrefixOfSym`)

tidyFunBinds :: SpecType -> SpecType
tidyFunBinds :: SpecType -> SpecType
tidyFunBinds SpecType
t = forall c tv r. (Symbol -> Symbol) -> RType c tv r -> RType c tv r
mapBind Symbol -> Symbol
tx forall a b. (a -> b) -> a -> b
$ forall a. Subable a => (Symbol -> Symbol) -> a -> a
substa Symbol -> Symbol
tx SpecType
t
  where
    tx :: Symbol -> Symbol
tx         = [Symbol] -> Symbol -> Symbol
bindersTx forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> [a] -> [a]
filter Symbol -> Bool
GM.isTmpSymbol forall a b. (a -> b) -> a -> b
$ forall t t1 t2. RType t t1 t2 -> [Symbol]
funBinds SpecType
t

tidyTyVars :: SpecType -> SpecType
tidyTyVars :: SpecType -> SpecType
tidyTyVars SpecType
t = forall k r c.
(Eq k, Hashable k, Reftable r, TyConable c,
 SubsTy k (RType c k ()) c, SubsTy k (RType c k ()) r,
 SubsTy k (RType c k ()) k, SubsTy k (RType c k ()) (RType c k ()),
 SubsTy k (RType c k ()) (RTVar k (RType c k ())), FreeVar c k) =>
[(k, RType c k (), RType c k r)] -> RType c k r -> RType c k r
subsTyVarsAll forall {c}. [(RTyVar, RType c RTyVar (), RType c RTyVar RReft)]
αβs SpecType
t
  where
    αβs :: [(RTyVar, RType c RTyVar (), RType c RTyVar RReft)]
αβs  = forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\RTyVar
α RType c RTyVar RReft
β -> (RTyVar
α, forall c tv r. RType c tv r -> RType c tv ()
toRSort RType c RTyVar RReft
β, RType c RTyVar RReft
β)) [RTyVar]
αs forall {c}. [RType c RTyVar RReft]
βs
    αs :: [RTyVar]
αs   = forall a. Eq a => [a] -> [a]
L.nub (forall c tv r. RType c tv r -> [tv]
tyVars SpecType
t)
    βs :: [RType c RTyVar RReft]
βs   = forall a b. (a -> b) -> [a] -> [b]
map (forall r c. Monoid r => Var -> RType c RTyVar r
rVar forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> Var
GM.stringTyVar) [[Char]]
pool
    pool :: [[Char]]
pool = [[Char
c] | Char
c <- [Char
'a'..Char
'z']] forall a. [a] -> [a] -> [a]
++ [ [Char]
"t" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Int
i | Int
i <- [(Int
1::Int)..]]


bindersTx :: [Symbol] -> Symbol -> Symbol
bindersTx :: [Symbol] -> Symbol -> Symbol
bindersTx [Symbol]
ds   = \Symbol
y -> forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
M.lookupDefault Symbol
y Symbol
y HashMap Symbol Symbol
m
  where
    m :: HashMap Symbol Symbol
m          = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
ds forall a b. (a -> b) -> a -> b
$ Int -> Symbol
var forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Int
1::Int)..]
    var :: Int -> Symbol
var        = forall a. Symbolic a => a -> Symbol
symbol forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char
'x' forall a. a -> [a] -> [a]
:) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> [Char]
show


tyVars :: RType c tv r -> [tv]
tyVars :: forall c tv r. RType c tv r -> [tv]
tyVars (RAllP PVU c tv
_ RType c tv r
t)       = forall c tv r. RType c tv r -> [tv]
tyVars RType c tv r
t
tyVars (RAllT RTVU c tv
α RType c tv r
t r
_)     = forall tv s. RTVar tv s -> tv
ty_var_value RTVU c tv
α forall a. a -> [a] -> [a]
: forall c tv r. RType c tv r -> [tv]
tyVars RType c tv r
t
tyVars (RFun Symbol
_ RFInfo
_ RType c tv r
t RType c tv r
t' r
_) = forall c tv r. RType c tv r -> [tv]
tyVars RType c tv r
t forall a. [a] -> [a] -> [a]
++ forall c tv r. RType c tv r -> [tv]
tyVars RType c tv r
t'
tyVars (RAppTy RType c tv r
t RType c tv r
t' r
_)   = forall c tv r. RType c tv r -> [tv]
tyVars RType c tv r
t forall a. [a] -> [a] -> [a]
++ forall c tv r. RType c tv r -> [tv]
tyVars RType c tv r
t'
tyVars (RApp c
_ [RType c tv r]
ts [RTProp c tv r]
_ r
_)   = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap forall c tv r. RType c tv r -> [tv]
tyVars [RType c tv r]
ts
tyVars (RVar tv
α r
_)        = [tv
α]
tyVars (RAllE Symbol
_ RType c tv r
_ RType c tv r
t)     = forall c tv r. RType c tv r -> [tv]
tyVars RType c tv r
t
tyVars (REx Symbol
_ RType c tv r
_ RType c tv r
t)       = forall c tv r. RType c tv r -> [tv]
tyVars RType c tv r
t
tyVars (RExprArg Located Expr
_)      = []
tyVars (RRTy [(Symbol, RType c tv r)]
_ r
_ Oblig
_ RType c tv r
t)    = forall c tv r. RType c tv r -> [tv]
tyVars RType c tv r
t
tyVars (RHole r
_)         = []

subsTyVarsAll
  :: (Eq k, Hashable k,
      Reftable r, TyConable c, SubsTy k (RType c k ()) c,
      SubsTy k (RType c k ()) r,
      SubsTy k (RType c k ()) k,
      SubsTy k (RType c k ()) (RType c k ()),
      SubsTy k (RType c k ()) (RTVar k (RType c k ())),
      FreeVar c k)
   => [(k, RType c k (), RType c k r)] -> RType c k r -> RType c k r
subsTyVarsAll :: forall k r c.
(Eq k, Hashable k, Reftable r, TyConable c,
 SubsTy k (RType c k ()) c, SubsTy k (RType c k ()) r,
 SubsTy k (RType c k ()) k, SubsTy k (RType c k ()) (RType c k ()),
 SubsTy k (RType c k ()) (RTVar k (RType c k ())), FreeVar c k) =>
[(k, RType c k (), RType c k r)] -> RType c k r -> RType c k r
subsTyVarsAll [(k, RType c k (), RType c k r)]
ats = RType c k r -> RType c k r
go
  where
    abm :: HashMap k k
abm            = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [(k
a, k
b) | (k
a, RType c k ()
_, RVar k
b r
_) <- [(k, RType c k (), RType c k r)]
ats]
    go :: RType c k r -> RType c k r
go (RAllT RTVar k (RType c k ())
a RType c k r
t r
r) = forall c tv r. RTVU c tv -> RType c tv r -> r -> RType c tv r
RAllT (forall tv s. tv -> RTVar tv s
makeRTVar forall a b. (a -> b) -> a -> b
$ forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
M.lookupDefault (forall tv s. RTVar tv s -> tv
ty_var_value RTVar k (RType c k ())
a) (forall tv s. RTVar tv s -> tv
ty_var_value RTVar k (RType c k ())
a) HashMap k k
abm) (RType c k r -> RType c k r
go RType c k r
t) r
r
    go RType c k r
t           = forall tv (t :: * -> *) r c.
(Eq tv, Foldable t, Hashable tv, Reftable r, TyConable c,
 SubsTy tv (RType c tv ()) c, SubsTy tv (RType c tv ()) r,
 SubsTy tv (RType c tv ()) (RType c tv ()), FreeVar c tv,
 SubsTy tv (RType c tv ()) tv,
 SubsTy tv (RType c tv ()) (RTVar tv (RType c tv ()))) =>
t (tv, RType c tv (), RType c tv r) -> RType c tv r -> RType c tv r
subsTyVarsMeet [(k, RType c k (), RType c k r)]
ats RType c k r
t


funBinds :: RType t t1 t2 -> [Symbol]
funBinds :: forall t t1 t2. RType t t1 t2 -> [Symbol]
funBinds (RAllT RTVU t t1
_ RType t t1 t2
t t2
_)      = forall t t1 t2. RType t t1 t2 -> [Symbol]
funBinds RType t t1 t2
t
funBinds (RAllP PVU t t1
_ RType t t1 t2
t)        = forall t t1 t2. RType t t1 t2 -> [Symbol]
funBinds RType t t1 t2
t
funBinds (RFun Symbol
b RFInfo
_ RType t t1 t2
t1 RType t t1 t2
t2 t2
_) = Symbol
b forall a. a -> [a] -> [a]
: forall t t1 t2. RType t t1 t2 -> [Symbol]
funBinds RType t t1 t2
t1 forall a. [a] -> [a] -> [a]
++ forall t t1 t2. RType t t1 t2 -> [Symbol]
funBinds RType t t1 t2
t2
funBinds (RApp t
_ [RType t t1 t2]
ts [RTProp t t1 t2]
_ t2
_)    = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap forall t t1 t2. RType t t1 t2 -> [Symbol]
funBinds [RType t t1 t2]
ts
funBinds (RAllE Symbol
b RType t t1 t2
t1 RType t t1 t2
t2)    = Symbol
b forall a. a -> [a] -> [a]
: forall t t1 t2. RType t t1 t2 -> [Symbol]
funBinds RType t t1 t2
t1 forall a. [a] -> [a] -> [a]
++ forall t t1 t2. RType t t1 t2 -> [Symbol]
funBinds RType t t1 t2
t2
funBinds (REx Symbol
b RType t t1 t2
t1 RType t t1 t2
t2)      = Symbol
b forall a. a -> [a] -> [a]
: forall t t1 t2. RType t t1 t2 -> [Symbol]
funBinds RType t t1 t2
t1 forall a. [a] -> [a] -> [a]
++ forall t t1 t2. RType t t1 t2 -> [Symbol]
funBinds RType t t1 t2
t2
funBinds (RVar t1
_ t2
_)         = []
funBinds (RRTy [(Symbol, RType t t1 t2)]
_ t2
_ Oblig
_ RType t t1 t2
t)     = forall t t1 t2. RType t t1 t2 -> [Symbol]
funBinds RType t t1 t2
t
funBinds (RAppTy RType t t1 t2
t1 RType t t1 t2
t2 t2
_)   = forall t t1 t2. RType t t1 t2 -> [Symbol]
funBinds RType t t1 t2
t1 forall a. [a] -> [a] -> [a]
++ forall t t1 t2. RType t t1 t2 -> [Symbol]
funBinds RType t t1 t2
t2
funBinds (RExprArg Located Expr
_)       = []
funBinds (RHole t2
_)          = []


--------------------------------------------------------------------------------
-- | Show an Error, then crash
--------------------------------------------------------------------------------
panicError :: {-(?callStack :: CallStack) =>-} Error -> a
--------------------------------------------------------------------------------
panicError :: forall a. Error -> a
panicError = forall a e. Exception e => e -> a
Ex.throw

-- ^ This function is put in this module as it depends on the Exception instance,
--   which depends on the PPrint instance, which depends on tidySpecType.

--------------------------------------------------------------------------------
-- | Pretty Printing Error Messages --------------------------------------------
--------------------------------------------------------------------------------

-- | Need to put @PPrint Error@ instance here (instead of in Types),
--   as it depends on @PPrint SpecTypes@, which lives in this module.


instance PPrint (CtxError Doc) where
  pprintTidy :: Tidy -> CtxError Doc -> Doc
pprintTidy Tidy
k CtxError Doc
ce = forall a. (PPrint a, Show a) => Tidy -> Doc -> TError a -> Doc
ppError Tidy
k (forall t. CtxError t -> Doc
ctCtx CtxError Doc
ce) forall a b. (a -> b) -> a -> b
$ forall t. CtxError t -> TError t
ctErr CtxError Doc
ce

instance PPrint (CtxError SpecType) where
  pprintTidy :: Tidy -> CtxError SpecType -> Doc
pprintTidy Tidy
k CtxError SpecType
ce = forall a. (PPrint a, Show a) => Tidy -> Doc -> TError a -> Doc
ppError Tidy
k (forall t. CtxError t -> Doc
ctCtx CtxError SpecType
ce) forall a b. (a -> b) -> a -> b
$ SpecType -> Doc
ppSpecTypeErr forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. CtxError t -> TError t
ctErr CtxError SpecType
ce

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

ppSpecTypeErr :: SpecType -> Doc
ppSpecTypeErr :: SpecType -> Doc
ppSpecTypeErr = Tidy -> SpecType -> Doc
ppSpecType Tidy
Lossy

ppSpecType :: Tidy -> SpecType -> Doc
ppSpecType :: Tidy -> SpecType -> Doc
ppSpecType Tidy
k = forall c tv r. OkRT c tv r => Tidy -> RType c tv r -> Doc
rtypeDoc     Tidy
k
             forall b c a. (b -> c) -> (a -> b) -> a -> c
. Tidy -> SpecType -> SpecType
tidySpecType Tidy
k
             forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((forall a. Data a => a -> a) -> forall a. Data a => a -> a
everywhere (forall a b. (Typeable a, Typeable b) => (b -> b) -> a -> a
mkT Expr -> Expr
noCasts))
  where
    noCasts :: Expr -> Expr
noCasts (ECst Expr
x Sort
_) = Expr
x
    noCasts Expr
e          = Expr
e

instance Show Error where
  show :: Error -> [Char]
show Error
e = Doc -> [Char]
render (forall a. PPrint a => a -> Doc
pprint (forall t. TError t -> SrcSpan
pos Error
e) Doc -> Doc -> Doc
<+> forall a. PPrint a => a -> Doc
pprint Error
e)

instance Ex.Exception Error
instance Ex.Exception [Error]