{-# 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
  , tidyInternalRefas
  , 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.Errors
import           Language.Haskell.Liquid.Types.RType
import           Language.Haskell.Liquid.Types.RTypeOp
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 = [(UserError, Maybe String)] -> String -> FixResult UserError
forall a. [(a, Maybe String)] -> String -> FixResult a
Crash [(UserError
e, Maybe String
forall a. Maybe a
Nothing)] String
""

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

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

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

errorToUserError :: Error -> UserError
errorToUserError :: Error -> UserError
errorToUserError = (RTypeBV Symbol Symbol RTyCon RTyVar RReft -> Doc)
-> Error -> UserError
forall a b. (a -> b) -> TError a -> TError b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap RTypeBV Symbol Symbol RTyCon RTyVar RReft -> 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
_)        = SrcSpan -> Doc -> Error
forall t. SrcSpan -> Doc -> TError t
ErrOther SrcSpan
l (String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ String
"Cinfo: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SrcSpan -> String
forall a. Outputable a => a -> String
GM.showPpr SrcSpan
l)

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

tidyValueVars :: SpecType -> SpecType
tidyValueVars :: RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
tidyValueVars = (RReft -> RReft)
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall r1 r2 b v c tv.
(r1 -> r2) -> RTypeBV b v c tv r1 -> RTypeBV b v c tv r2
mapReft ((RReft -> RReft)
 -> RTypeBV Symbol Symbol RTyCon RTyVar RReft
 -> RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> (RReft -> RReft)
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall a b. (a -> b) -> a -> b
$ \RReft
u -> RReft
u { ur_reft = tidyVV $ ur_reft u }

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

tidySymbols :: Tidy -> SpecType -> SpecType
tidySymbols :: Tidy
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
tidySymbols Tidy
k RTypeBV Symbol Symbol RTyCon RTyVar RReft
t = (Variable (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
 -> Variable (RTypeBV Symbol Symbol RTyCon RTyVar RReft))
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall a. Subable a => (Variable a -> Variable a) -> a -> a
substa (Tidy -> Symbol -> Symbol
shortSymbol Tidy
k (Symbol -> Symbol) -> (Symbol -> Symbol) -> Symbol -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Symbol
tidySymbol) (RTypeBV Symbol Symbol RTyCon RTyVar RReft
 -> RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall a b. (a -> b) -> a -> b
$ (Symbol -> Symbol)
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall b b' v c tv r.
(Hashable b, Hashable b') =>
(b -> b') -> RTypeBV b v c tv r -> RTypeBV b' v c tv r
mapBind Symbol -> Symbol
dropBind RTypeBV Symbol Symbol RTyCon RTyVar RReft
t
  where
    xs :: HashSet Symbol
xs          = [Symbol] -> HashSet Symbol
forall a. Hashable a => [a] -> HashSet a
S.fromList (RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> [Variable (RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
forall a. Subable a => a -> [Variable a]
syms RTypeBV Symbol Symbol RTyCon RTyVar RReft
t)
    dropBind :: Symbol -> Symbol
dropBind Symbol
x  = if Symbol
x Symbol -> HashSet Symbol -> Bool
forall 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
_     = Symbol -> Symbol
forall a. a -> a
id

tidyLocalRefas   :: Tidy -> SpecType -> SpecType
tidyLocalRefas :: Tidy
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
tidyLocalRefas Tidy
k = (RReft -> RReft)
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall r1 r2 b v c tv.
(r1 -> r2) -> RTypeBV b v c tv r1 -> RTypeBV b v c tv r2
mapReft (Tidy -> RReft -> RReft
forall {b} {v}.
Tidy
-> UReftBV b v (ReftBV Symbol Symbol)
-> UReftBV b v (ReftBV Symbol Symbol)
txReft' Tidy
k)
  where
    txReft' :: Tidy
-> UReftBV b v (ReftBV Symbol Symbol)
-> UReftBV b v (ReftBV Symbol Symbol)
txReft' Tidy
Full                  = UReftBV b v (ReftBV Symbol Symbol)
-> UReftBV b v (ReftBV Symbol Symbol)
forall a. a -> a
id
    txReft' Tidy
Lossy                 = UReftBV b v (ReftBV Symbol Symbol)
-> UReftBV b v (ReftBV Symbol Symbol)
forall {b} {v}.
UReftBV b v (ReftBV Symbol Symbol)
-> UReftBV b v (ReftBV Symbol Symbol)
txReft
    txReft :: UReftBV b v (ReftBV Symbol Symbol)
-> UReftBV b v (ReftBV Symbol Symbol)
txReft UReftBV b v (ReftBV Symbol Symbol)
u                      = UReftBV b v (ReftBV Symbol Symbol)
u { ur_reft = mapPredReft dropLocals $ ur_reft u }
    dropLocals :: Expr -> Expr
dropLocals                    = ListNE Expr -> Expr
forall b v.
(Ord b, Hashable b, Ord v) =>
ListNE (ExprBV b v) -> ExprBV b v
pAnd (ListNE Expr -> Expr) -> (Expr -> ListNE Expr) -> Expr -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> Bool) -> ListNE Expr -> ListNE Expr
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Expr -> Bool) -> Expr -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol -> Bool) -> [Symbol] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Symbol -> Bool
isTmp ([Symbol] -> Bool) -> (Expr -> [Symbol]) -> Expr -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> [Symbol]
Expr -> [Variable Expr]
forall a. Subable a => a -> [Variable a]
syms) (ListNE Expr -> ListNE Expr)
-> (Expr -> ListNE Expr) -> Expr -> ListNE Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> ListNE Expr
forall b v. (Eq b, Eq v) => ExprBV b v -> [ExprBV b v]
conjuncts
    isTmp :: Symbol -> Bool
isTmp Symbol
x                       = (Symbol -> Bool) -> [Symbol] -> Bool
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 :: RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
tidyEqual = (RReft -> RReft)
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall r1 r2 b v c tv.
(r1 -> r2) -> RTypeBV b v c tv r1 -> RTypeBV b v c tv r2
mapReft RReft -> RReft
forall {b} {v}.
UReftBV b v (ReftBV Symbol Symbol)
-> UReftBV b v (ReftBV Symbol Symbol)
txReft
  where
    txReft :: UReftBV b v (ReftBV Symbol Symbol)
-> UReftBV b v (ReftBV Symbol Symbol)
txReft UReftBV b v (ReftBV Symbol Symbol)
u                      = UReftBV b v (ReftBV Symbol Symbol)
u { ur_reft = mapPredReft dropInternals $ ur_reft u }
    dropInternals :: Expr -> Expr
dropInternals                 = ListNE Expr -> Expr
forall b v.
(Ord b, Hashable b, Ord v) =>
ListNE (ExprBV b v) -> ExprBV b v
pAnd (ListNE Expr -> Expr) -> (Expr -> ListNE Expr) -> Expr -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ListNE Expr -> ListNE Expr
forall a. Eq a => [a] -> [a]
L.nub (ListNE Expr -> ListNE Expr)
-> (Expr -> ListNE Expr) -> Expr -> ListNE Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> ListNE Expr
forall b v. (Eq b, Eq v) => ExprBV b v -> [ExprBV b v]
conjuncts

-- | Drop conjuncts that contain data constructor testing or
-- selector functions.
tidyInternalRefas   :: SpecType -> SpecType
tidyInternalRefas :: RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
tidyInternalRefas = (RReft -> RReft)
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall r1 r2 b v c tv.
(r1 -> r2) -> RTypeBV b v c tv r1 -> RTypeBV b v c tv r2
mapReft RReft -> RReft
forall {b} {v}.
UReftBV b v (ReftBV Symbol Symbol)
-> UReftBV b v (ReftBV Symbol Symbol)
txReft
  where
    txReft :: UReftBV b v (ReftBV Symbol Symbol)
-> UReftBV b v (ReftBV Symbol Symbol)
txReft UReftBV b v (ReftBV Symbol Symbol)
u                      = UReftBV b v (ReftBV Symbol Symbol)
u { ur_reft = mapPredReft dropInternals $ ur_reft u }
    dropInternals :: Expr -> Expr
dropInternals                 = ListNE Expr -> Expr
forall b v.
(Ord b, Hashable b, Ord v) =>
ListNE (ExprBV b v) -> ExprBV b v
pAnd (ListNE Expr -> Expr) -> (Expr -> ListNE Expr) -> Expr -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> Bool) -> ListNE Expr -> ListNE Expr
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Expr -> Bool) -> Expr -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol -> Bool) -> [Symbol] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Symbol -> Bool
isIntern ([Symbol] -> Bool) -> (Expr -> [Symbol]) -> Expr -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> [Symbol]
Expr -> [Variable Expr]
forall a. Subable a => a -> [Variable a]
syms) (ListNE Expr -> ListNE Expr)
-> (Expr -> ListNE Expr) -> Expr -> ListNE Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> ListNE Expr
forall b v. (Eq b, Eq v) => ExprBV b v -> [ExprBV b v]
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 :: RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
tidyDSymbols RTypeBV Symbol Symbol RTyCon RTyVar RReft
t = (Symbol -> Symbol)
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall b b' v c tv r.
(Hashable b, Hashable b') =>
(b -> b') -> RTypeBV b v c tv r -> RTypeBV b' v c tv r
mapBind Symbol -> Symbol
tx (RTypeBV Symbol Symbol RTyCon RTyVar RReft
 -> RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall a b. (a -> b) -> a -> b
$ (Variable (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
 -> Variable (RTypeBV Symbol Symbol RTyCon RTyVar RReft))
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall a. Subable a => (Variable a -> Variable a) -> a -> a
substa Symbol -> Symbol
Variable (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> Variable (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
tx RTypeBV Symbol Symbol RTyCon RTyVar RReft
t
  where
    tx :: Symbol -> Symbol
tx         = [Symbol] -> Symbol -> Symbol
bindersTx [Symbol
x | Symbol
x <- RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> [Variable (RTypeBV Symbol Symbol RTyCon RTyVar RReft)]
forall a. Subable a => a -> [Variable a]
syms RTypeBV Symbol Symbol RTyCon RTyVar RReft
t, Symbol -> Bool
isTmp Symbol
x]
    isTmp :: Symbol -> Bool
isTmp      = (Symbol
tempPrefix Symbol -> Symbol -> Bool
`isPrefixOfSym`)

tidyFunBinds :: SpecType -> SpecType
tidyFunBinds :: RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
tidyFunBinds RTypeBV Symbol Symbol RTyCon RTyVar RReft
t = (Symbol -> Symbol)
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall b b' v c tv r.
(Hashable b, Hashable b') =>
(b -> b') -> RTypeBV b v c tv r -> RTypeBV b' v c tv r
mapBind Symbol -> Symbol
tx (RTypeBV Symbol Symbol RTyCon RTyVar RReft
 -> RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall a b. (a -> b) -> a -> b
$ (Variable (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
 -> Variable (RTypeBV Symbol Symbol RTyCon RTyVar RReft))
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall a. Subable a => (Variable a -> Variable a) -> a -> a
substa Symbol -> Symbol
Variable (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> Variable (RTypeBV Symbol Symbol RTyCon RTyVar RReft)
tx RTypeBV Symbol Symbol RTyCon RTyVar RReft
t
  where
    tx :: Symbol -> Symbol
tx         = [Symbol] -> Symbol -> Symbol
bindersTx ([Symbol] -> Symbol -> Symbol) -> [Symbol] -> Symbol -> Symbol
forall a b. (a -> b) -> a -> b
$ (Symbol -> Bool) -> [Symbol] -> [Symbol]
forall a. (a -> Bool) -> [a] -> [a]
filter Symbol -> Bool
GM.isTmpSymbol ([Symbol] -> [Symbol]) -> [Symbol] -> [Symbol]
forall a b. (a -> b) -> a -> b
$ RTypeBV Symbol Symbol RTyCon RTyVar RReft -> [Symbol]
forall t t1 t2. RType t t1 t2 -> [Symbol]
funBinds RTypeBV Symbol Symbol RTyCon RTyVar RReft
t

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


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


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

subsTyVarsAll
  :: (Eq k, Hashable k,
      IsReft r, TyConable c, SubsTy k (RType c k NoReft) c,
      SubsTy k (RType c k NoReft) r,
      SubsTy k (RType c k NoReft) k,
      SubsTy k (RType c k NoReft) (RType c k NoReft),
      SubsTy k (RType c k NoReft) (RTVar k (RType c k NoReft)),
      FreeVar c k)
   => [(k, RType c k NoReft, RType c k r)] -> RType c k r -> RType c k r
subsTyVarsAll :: forall k r c.
(Eq k, Hashable k, IsReft r, TyConable c,
 SubsTy k (RType c k NoReft) c, SubsTy k (RType c k NoReft) r,
 SubsTy k (RType c k NoReft) k,
 SubsTy k (RType c k NoReft) (RType c k NoReft),
 SubsTy k (RType c k NoReft) (RTVar k (RType c k NoReft)),
 FreeVar c k) =>
[(k, RType c k NoReft, RType c k r)] -> RType c k r -> RType c k r
subsTyVarsAll [(k, RType c k NoReft, RType c k r)]
ats = RType c k r -> RType c k r
go
  where
    abm :: HashMap k k
abm            = [(k, k)] -> HashMap k k
forall k v. Hashable k => [(k, v)] -> HashMap k v
M.fromList [(k
a, k
b) | (k
a, RType c k NoReft
_, RVar k
b r
_) <- [(k, RType c k NoReft, RType c k r)]
ats]
    go :: RType c k r -> RType c k r
go (RAllT RTVar k (RType c k NoReft)
a RType c k r
t r
r) = RTVar k (RType c k NoReft) -> RType c k r -> r -> RType c k r
forall b v c tv r.
RTVUBV b v c tv -> RTypeBV b v c tv r -> r -> RTypeBV b v c tv r
RAllT (k -> RTVar k (RType c k NoReft)
forall tv s. tv -> RTVar tv s
makeRTVar (k -> RTVar k (RType c k NoReft))
-> k -> RTVar k (RType c k NoReft)
forall a b. (a -> b) -> a -> b
$ k -> k -> HashMap k k -> k
forall k v. Hashable k => v -> k -> HashMap k v -> v
M.lookupDefault (RTVar k (RType c k NoReft) -> k
forall tv s. RTVar tv s -> tv
ty_var_value RTVar k (RType c k NoReft)
a) (RTVar k (RType c k NoReft) -> k
forall tv s. RTVar tv s -> tv
ty_var_value RTVar k (RType c k NoReft)
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           = [(k, RType c k NoReft, RType c k r)] -> RType c k r -> RType c k r
forall tv (t :: * -> *) r c b v.
(Eq tv, Foldable t, Hashable tv, IsReft r, TyConable c, Binder b,
 SubsTy tv (RTypeBV b v c tv (NoReftB b)) c,
 SubsTy tv (RTypeBV b v c tv (NoReftB b)) r,
 SubsTy
   tv (RTypeBV b v c tv (NoReftB b)) (RTypeBV b v c tv (NoReftB b)),
 FreeVar c tv, SubsTy tv (RTypeBV b v c tv (NoReftB b)) tv,
 SubsTy
   tv
   (RTypeBV b v c tv (NoReftB b))
   (RTVar tv (RTypeBV b v c tv (NoReftB b)))) =>
t (tv, RTypeBV b v c tv (NoReftB b), RTypeBV b v c tv r)
-> RTypeBV b v c tv r -> RTypeBV b v c tv r
subsTyVarsMeet [(k, RType c k NoReft, 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 RTVUBV Symbol Symbol t t1
_ RTypeBV Symbol Symbol t t1 t2
t t2
_)      = RTypeBV Symbol Symbol t t1 t2 -> [Symbol]
forall t t1 t2. RType t t1 t2 -> [Symbol]
funBinds RTypeBV Symbol Symbol t t1 t2
t
funBinds (RAllP PVUBV Symbol Symbol t t1
_ RTypeBV Symbol Symbol t t1 t2
t)        = RTypeBV Symbol Symbol t t1 t2 -> [Symbol]
forall t t1 t2. RType t t1 t2 -> [Symbol]
funBinds RTypeBV Symbol Symbol t t1 t2
t
funBinds (RFun Symbol
b RFInfo
_ RTypeBV Symbol Symbol t t1 t2
t1 RTypeBV Symbol Symbol t t1 t2
t2 t2
_) = Symbol
b Symbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
: RTypeBV Symbol Symbol t t1 t2 -> [Symbol]
forall t t1 t2. RType t t1 t2 -> [Symbol]
funBinds RTypeBV Symbol Symbol t t1 t2
t1 [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ RTypeBV Symbol Symbol t t1 t2 -> [Symbol]
forall t t1 t2. RType t t1 t2 -> [Symbol]
funBinds RTypeBV Symbol Symbol t t1 t2
t2
funBinds (RApp t
_ [RTypeBV Symbol Symbol t t1 t2]
ts [RTPropBV Symbol Symbol t t1 t2]
_ t2
_)    = (RTypeBV Symbol Symbol t t1 t2 -> [Symbol])
-> [RTypeBV Symbol Symbol t t1 t2] -> [Symbol]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap RTypeBV Symbol Symbol t t1 t2 -> [Symbol]
forall t t1 t2. RType t t1 t2 -> [Symbol]
funBinds [RTypeBV Symbol Symbol t t1 t2]
ts
funBinds (RAllE Symbol
b RTypeBV Symbol Symbol t t1 t2
t1 RTypeBV Symbol Symbol t t1 t2
t2)    = Symbol
b Symbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
: RTypeBV Symbol Symbol t t1 t2 -> [Symbol]
forall t t1 t2. RType t t1 t2 -> [Symbol]
funBinds RTypeBV Symbol Symbol t t1 t2
t1 [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ RTypeBV Symbol Symbol t t1 t2 -> [Symbol]
forall t t1 t2. RType t t1 t2 -> [Symbol]
funBinds RTypeBV Symbol Symbol t t1 t2
t2
funBinds (REx Symbol
b RTypeBV Symbol Symbol t t1 t2
t1 RTypeBV Symbol Symbol t t1 t2
t2)      = Symbol
b Symbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
: RTypeBV Symbol Symbol t t1 t2 -> [Symbol]
forall t t1 t2. RType t t1 t2 -> [Symbol]
funBinds RTypeBV Symbol Symbol t t1 t2
t1 [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ RTypeBV Symbol Symbol t t1 t2 -> [Symbol]
forall t t1 t2. RType t t1 t2 -> [Symbol]
funBinds RTypeBV Symbol Symbol t t1 t2
t2
funBinds (RVar t1
_ t2
_)         = []
funBinds (RRTy [(Symbol, RTypeBV Symbol Symbol t t1 t2)]
_ t2
_ Oblig
_ RTypeBV Symbol Symbol t t1 t2
t)     = RTypeBV Symbol Symbol t t1 t2 -> [Symbol]
forall t t1 t2. RType t t1 t2 -> [Symbol]
funBinds RTypeBV Symbol Symbol t t1 t2
t
funBinds (RAppTy RTypeBV Symbol Symbol t t1 t2
t1 RTypeBV Symbol Symbol t t1 t2
t2 t2
_)   = RTypeBV Symbol Symbol t t1 t2 -> [Symbol]
forall t t1 t2. RType t t1 t2 -> [Symbol]
funBinds RTypeBV Symbol Symbol t t1 t2
t1 [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ RTypeBV Symbol Symbol t t1 t2 -> [Symbol]
forall t t1 t2. RType t t1 t2 -> [Symbol]
funBinds RTypeBV Symbol Symbol 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 = Error -> a
forall a e. (HasCallStack, 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 = Tidy -> Doc -> UserError -> Doc
forall a. (PPrint a, Show a) => Tidy -> Doc -> TError a -> Doc
ppError Tidy
k (CtxError Doc -> Doc
forall t. CtxError t -> Doc
ctCtx CtxError Doc
ce) (UserError -> Doc) -> UserError -> Doc
forall a b. (a -> b) -> a -> b
$ CtxError Doc -> UserError
forall t. CtxError t -> TError t
ctErr CtxError Doc
ce

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

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

ppSpecTypeErr :: SpecType -> Doc
ppSpecTypeErr :: RTypeBV Symbol Symbol RTyCon RTyVar RReft -> Doc
ppSpecTypeErr = Tidy -> RTypeBV Symbol Symbol RTyCon RTyVar RReft -> Doc
ppSpecType Tidy
Lossy

ppSpecType :: Tidy -> SpecType -> Doc
ppSpecType :: Tidy -> RTypeBV Symbol Symbol RTyCon RTyVar RReft -> Doc
ppSpecType Tidy
k = Tidy -> RTypeBV Symbol Symbol RTyCon RTyVar RReft -> Doc
forall b v c tv r.
OkRTBV b v c tv r =>
Tidy -> RTypeBV b v c tv r -> Doc
rtypeDoc     Tidy
k
             (RTypeBV Symbol Symbol RTyCon RTyVar RReft -> Doc)
-> (RTypeBV Symbol Symbol RTyCon RTyVar RReft
    -> RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Tidy
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
tidySpecType Tidy
k
             (RTypeBV Symbol Symbol RTyCon RTyVar RReft
 -> RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> (RTypeBV Symbol Symbol RTyCon RTyVar RReft
    -> RTypeBV Symbol Symbol RTyCon RTyVar RReft)
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (RReft -> RReft)
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeBV Symbol Symbol RTyCon RTyVar RReft
forall a b.
(a -> b)
-> RTypeBV Symbol Symbol RTyCon RTyVar a
-> RTypeBV Symbol Symbol RTyCon RTyVar b
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 ((Expr -> Expr) -> a -> a
forall a b. (Typeable a, Typeable b) => (b -> b) -> a -> a
mkT Expr -> Expr
noCasts))
  where
    noCasts :: Expr -> Expr
    noCasts :: Expr -> Expr
noCasts (ECst Expr
x Sort
_) = Expr
x
    noCasts Expr
e          = Expr
e

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

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