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

---------------------------------------------------------------------
-- | 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, subsTyVars_meet, 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] -> String -> FixResult UserError
forall a. [a] -> String -> FixResult a
Crash [UserError
e] String
""

instance Result [Error] where
  result :: [Error] -> FixResult UserError
result [Error]
es = [UserError] -> String -> FixResult UserError
forall a. [a] -> String -> FixResult a
Crash (Error -> UserError
errorToUserError (Error -> UserError) -> [Error] -> [UserError]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [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 (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 = (SpecType -> Doc) -> Error -> UserError
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
_)        = 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 -> SpecType -> SpecType
tidySpecType Tidy
k 
  = SpecType -> SpecType
tidyEqual 
  (SpecType -> SpecType)
-> (SpecType -> SpecType) -> SpecType -> SpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SpecType -> SpecType
tidyValueVars
  (SpecType -> SpecType)
-> (SpecType -> SpecType) -> SpecType -> SpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SpecType -> SpecType
tidyDSymbols
  (SpecType -> SpecType)
-> (SpecType -> SpecType) -> SpecType -> SpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Tidy -> SpecType -> SpecType
tidySymbols Tidy
k 
  (SpecType -> SpecType)
-> (SpecType -> SpecType) -> SpecType -> SpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SpecType -> SpecType
tidyInternalRefas
  (SpecType -> SpecType)
-> (SpecType -> SpecType) -> SpecType -> SpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Tidy -> SpecType -> SpecType
tidyLocalRefas Tidy
k
  (SpecType -> SpecType)
-> (SpecType -> SpecType) -> SpecType -> SpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SpecType -> SpecType
tidyFunBinds
  (SpecType -> SpecType)
-> (SpecType -> SpecType) -> SpecType -> SpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SpecType -> SpecType
tidyTyVars

tidyValueVars :: SpecType -> SpecType
tidyValueVars :: SpecType -> SpecType
tidyValueVars = (UReft Reft -> UReft Reft) -> SpecType -> SpecType
forall r1 r2 c tv. (r1 -> r2) -> RType c tv r1 -> RType c tv r2
mapReft ((UReft Reft -> UReft Reft) -> SpecType -> SpecType)
-> (UReft Reft -> UReft Reft) -> SpecType -> SpecType
forall a b. (a -> b) -> a -> b
$ \UReft Reft
u -> UReft Reft
u { ur_reft :: Reft
ur_reft = Reft -> Reft
tidyVV (Reft -> Reft) -> Reft -> Reft
forall a b. (a -> b) -> a -> b
$ UReft Reft -> Reft
forall r. UReft r -> r
ur_reft UReft Reft
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 Symbol -> [Symbol] -> 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 :: [Symbol]
xs        = Reft -> [Symbol]
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 = (Symbol -> Symbol) -> SpecType -> SpecType
forall a. Subable a => (Symbol -> Symbol) -> 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) (SpecType -> SpecType) -> SpecType -> SpecType
forall a b. (a -> b) -> a -> b
$ (Symbol -> Symbol) -> SpecType -> SpecType
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          = [Symbol] -> HashSet Symbol
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList (SpecType -> [Symbol]
forall a. Subable a => a -> [Symbol]
syms SpecType
t)
    dropBind :: Symbol -> Symbol
dropBind Symbol
x  = if Symbol
x Symbol -> HashSet Symbol -> Bool
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
_     = Symbol -> Symbol
forall a. a -> a
id 

tidyLocalRefas   :: Tidy -> SpecType -> SpecType
tidyLocalRefas :: Tidy -> SpecType -> SpecType
tidyLocalRefas Tidy
k = (UReft Reft -> UReft Reft) -> SpecType -> SpecType
forall r1 r2 c tv. (r1 -> r2) -> RType c tv r1 -> RType c tv r2
mapReft (Tidy -> UReft Reft -> UReft Reft
txReft' Tidy
k)
  where
    txReft' :: Tidy -> UReft Reft -> UReft Reft
txReft' Tidy
Full                  = UReft Reft -> UReft Reft
forall a. a -> a
id
    txReft' Tidy
Lossy                 = UReft Reft -> UReft Reft
txReft
    txReft :: UReft Reft -> UReft Reft
txReft UReft Reft
u                      = UReft Reft
u { ur_reft :: Reft
ur_reft = (Expr -> Expr) -> Reft -> Reft
mapPredReft Expr -> Expr
dropLocals (Reft -> Reft) -> Reft -> Reft
forall a b. (a -> b) -> a -> b
$ UReft Reft -> Reft
forall r. UReft r -> r
ur_reft UReft Reft
u }
    dropLocals :: Expr -> Expr
dropLocals                    = ListNE Expr -> Expr
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]
forall a. Subable a => a -> [Symbol]
syms) (ListNE Expr -> ListNE Expr)
-> (Expr -> ListNE Expr) -> Expr -> ListNE Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> ListNE Expr
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 :: SpecType -> SpecType
tidyEqual = (UReft Reft -> UReft Reft) -> SpecType -> SpecType
forall r1 r2 c tv. (r1 -> r2) -> RType c tv r1 -> RType c tv r2
mapReft UReft Reft -> UReft Reft
txReft
  where 
    txReft :: UReft Reft -> UReft Reft
txReft UReft Reft
u                      = UReft Reft
u { ur_reft :: Reft
ur_reft = (Expr -> Expr) -> Reft -> Reft
mapPredReft Expr -> Expr
dropInternals (Reft -> Reft) -> Reft -> Reft
forall a b. (a -> b) -> a -> b
$ UReft Reft -> Reft
forall r. UReft r -> r
ur_reft UReft Reft
u }
    dropInternals :: Expr -> Expr
dropInternals                 = ListNE Expr -> Expr
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
conjuncts

tidyInternalRefas   :: SpecType -> SpecType
tidyInternalRefas :: SpecType -> SpecType
tidyInternalRefas = (UReft Reft -> UReft Reft) -> SpecType -> SpecType
forall r1 r2 c tv. (r1 -> r2) -> RType c tv r1 -> RType c tv r2
mapReft UReft Reft -> UReft Reft
txReft
  where
    txReft :: UReft Reft -> UReft Reft
txReft UReft Reft
u                      = UReft Reft
u { ur_reft :: Reft
ur_reft = (Expr -> Expr) -> Reft -> Reft
mapPredReft Expr -> Expr
dropInternals (Reft -> Reft) -> Reft -> Reft
forall a b. (a -> b) -> a -> b
$ UReft Reft -> Reft
forall r. UReft r -> r
ur_reft UReft Reft
u }
    dropInternals :: Expr -> Expr
dropInternals                 = ListNE Expr -> Expr
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]
forall a. Subable a => a -> [Symbol]
syms) (ListNE Expr -> ListNE Expr)
-> (Expr -> ListNE Expr) -> Expr -> ListNE Expr
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 = (Symbol -> Symbol) -> SpecType -> SpecType
forall c tv r. (Symbol -> Symbol) -> RType c tv r -> RType c tv r
mapBind Symbol -> Symbol
tx (SpecType -> SpecType) -> SpecType -> SpecType
forall a b. (a -> b) -> a -> b
$ (Symbol -> Symbol) -> SpecType -> SpecType
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 <- SpecType -> [Symbol]
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 = (Symbol -> Symbol) -> SpecType -> SpecType
forall c tv r. (Symbol -> Symbol) -> RType c tv r -> RType c tv r
mapBind Symbol -> Symbol
tx (SpecType -> SpecType) -> SpecType -> SpecType
forall a b. (a -> b) -> a -> b
$ (Symbol -> Symbol) -> SpecType -> SpecType
forall a. Subable a => (Symbol -> Symbol) -> a -> a
substa Symbol -> Symbol
tx SpecType
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
$ SpecType -> [Symbol]
forall t t1 t2. RType t t1 t2 -> [Symbol]
funBinds SpecType
t

tidyTyVars :: SpecType -> SpecType
tidyTyVars :: SpecType -> SpecType
tidyTyVars SpecType
t = [(RTyVar, RType RTyCon RTyVar (), SpecType)]
-> SpecType -> SpecType
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 [(RTyVar, RType RTyCon RTyVar (), SpecType)]
forall c.
[(RTyVar, RType c RTyVar (), RType c RTyVar (UReft Reft))]
αβs SpecType
t
  where
    αβs :: [(RTyVar, RType c RTyVar (), RType c RTyVar (UReft Reft))]
αβs  = (RTyVar
 -> RType c RTyVar (UReft Reft)
 -> (RTyVar, RType c RTyVar (), RType c RTyVar (UReft Reft)))
-> [RTyVar]
-> [RType c RTyVar (UReft Reft)]
-> [(RTyVar, RType c RTyVar (), RType c RTyVar (UReft Reft))]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\RTyVar
α RType c RTyVar (UReft Reft)
β -> (RTyVar
α, RType c RTyVar (UReft Reft) -> RType c RTyVar ()
forall c tv r. RType c tv r -> RType c tv ()
toRSort RType c RTyVar (UReft Reft)
β, RType c RTyVar (UReft Reft)
β)) [RTyVar]
αs [RType c RTyVar (UReft Reft)]
forall c. [RType c RTyVar (UReft Reft)]
βs
    αs :: [RTyVar]
αs   = [RTyVar] -> [RTyVar]
forall a. Eq a => [a] -> [a]
L.nub (SpecType -> [RTyVar]
forall c tv r. RType c tv r -> [tv]
tyVars SpecType
t)
    βs :: [RType c RTyVar (UReft Reft)]
βs   = (String -> RType c RTyVar (UReft Reft))
-> [String] -> [RType c RTyVar (UReft Reft)]
forall a b. (a -> b) -> [a] -> [b]
map (Var -> RType c RTyVar (UReft Reft)
forall r c. Monoid r => Var -> RType c RTyVar r
rVar (Var -> RType c RTyVar (UReft Reft))
-> (String -> Var) -> String -> RType c RTyVar (UReft Reft)
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]
++ Integer -> String
forall a. Show a => a -> String
show Integer
i | Integer
i <- [Integer
1..]]


bindersTx :: [Symbol] -> Symbol -> Symbol
bindersTx :: [Symbol] -> Symbol -> Symbol
bindersTx [Symbol]
ds   = \Symbol
y -> Symbol -> Symbol -> HashMap Symbol Symbol -> Symbol
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          = [(Symbol, Symbol)] -> HashMap Symbol Symbol
forall k v. (Eq k, 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
$ Integer -> Symbol
var (Integer -> Symbol) -> [Integer] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Integer
1..]
    var :: Integer -> Symbol
var        = String -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (String -> Symbol) -> (Integer -> String) -> Integer -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char
'x' Char -> String -> String
forall a. a -> [a] -> [a]
:) (String -> String) -> (Integer -> String) -> Integer -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> String
forall a. Show a => a -> String
show


tyVars :: RType c tv r -> [tv]
tyVars :: RType c tv r -> [tv]
tyVars (RAllP PVU c tv
_ RType c tv r
t)     = RType c tv r -> [tv]
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
_)   = RTVU c tv -> tv
forall tv s. RTVar tv s -> tv
ty_var_value RTVU c tv
α tv -> [tv] -> [tv]
forall a. a -> [a] -> [a]
: RType c tv r -> [tv]
forall c tv r. RType c tv r -> [tv]
tyVars RType c tv r
t
tyVars (RImpF Symbol
_ RType c tv r
t RType c tv r
t' r
_) = RType c tv r -> [tv]
forall c tv r. RType c tv r -> [tv]
tyVars RType c tv r
t [tv] -> [tv] -> [tv]
forall a. [a] -> [a] -> [a]
++ RType c tv r -> [tv]
forall c tv r. RType c tv r -> [tv]
tyVars RType c tv r
t'
tyVars (RFun Symbol
_ RType c tv r
t RType c tv r
t' r
_) = RType c tv r -> [tv]
forall c tv r. RType c tv r -> [tv]
tyVars RType c tv r
t [tv] -> [tv] -> [tv]
forall a. [a] -> [a] -> [a]
++ RType c tv r -> [tv]
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
_) = RType c tv r -> [tv]
forall c tv r. RType c tv r -> [tv]
tyVars RType c tv r
t [tv] -> [tv] -> [tv]
forall a. [a] -> [a] -> [a]
++ RType c tv r -> [tv]
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
_) = (RType c tv r -> [tv]) -> [RType c tv r] -> [tv]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap RType c tv r -> [tv]
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)   = RType c tv r -> [tv]
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)     = RType c tv r -> [tv]
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)  = RType c tv r -> [tv]
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 :: [(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            = [(k, k)] -> HashMap k k
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 RTVU c k
a RType c k r
t r
r) = RTVU c k -> RType c k r -> r -> RType c k r
forall c tv r. RTVU c tv -> RType c tv r -> r -> RType c tv r
RAllT (k -> RTVU c k
forall tv s. tv -> RTVar tv s
makeRTVar (k -> RTVU c k) -> k -> RTVU c k
forall a b. (a -> b) -> a -> b
$ k -> k -> HashMap k k -> k
forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
M.lookupDefault (RTVU c k -> k
forall tv s. RTVar tv s -> tv
ty_var_value RTVU c k
a) (RTVU c k -> k
forall tv s. RTVar tv s -> tv
ty_var_value RTVU 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           = [(k, RType c k (), RType c k r)] -> RType c k r -> RType c k r
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
subsTyVars_meet [(k, RType c k (), RType c k r)]
ats RType c k r
t


funBinds :: RType t t1 t2 -> [Symbol]
funBinds :: RType t t1 t2 -> [Symbol]
funBinds (RAllT RTVU t t1
_ RType t t1 t2
t t2
_)    = RType t t1 t2 -> [Symbol]
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)      = RType t t1 t2 -> [Symbol]
forall t t1 t2. RType t t1 t2 -> [Symbol]
funBinds RType t t1 t2
t
funBinds (RImpF Symbol
b RType t t1 t2
t1 RType t t1 t2
t2 t2
_) = Symbol
b Symbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
: RType t t1 t2 -> [Symbol]
forall t t1 t2. RType t t1 t2 -> [Symbol]
funBinds RType t t1 t2
t1 [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ RType t t1 t2 -> [Symbol]
forall t t1 t2. RType t t1 t2 -> [Symbol]
funBinds RType t t1 t2
t2
funBinds (RFun Symbol
b RType t t1 t2
t1 RType t t1 t2
t2 t2
_) = Symbol
b Symbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
: RType t t1 t2 -> [Symbol]
forall t t1 t2. RType t t1 t2 -> [Symbol]
funBinds RType t t1 t2
t1 [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ RType t t1 t2 -> [Symbol]
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
_)  = (RType t t1 t2 -> [Symbol]) -> [RType t t1 t2] -> [Symbol]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap RType t t1 t2 -> [Symbol]
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 Symbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
: RType t t1 t2 -> [Symbol]
forall t t1 t2. RType t t1 t2 -> [Symbol]
funBinds RType t t1 t2
t1 [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ RType t t1 t2 -> [Symbol]
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 Symbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
: RType t t1 t2 -> [Symbol]
forall t t1 t2. RType t t1 t2 -> [Symbol]
funBinds RType t t1 t2
t1 [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ RType t t1 t2 -> [Symbol]
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)   = RType t t1 t2 -> [Symbol]
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
_) = RType t t1 t2 -> [Symbol]
forall t t1 t2. RType t t1 t2 -> [Symbol]
funBinds RType t t1 t2
t1 [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ RType t t1 t2 -> [Symbol]
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 :: Error -> a
panicError = Error -> a
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 = 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 SpecType -> Doc
pprintTidy Tidy
k CtxError SpecType
ce = Tidy -> Doc -> UserError -> Doc
forall a. (PPrint a, Show a) => Tidy -> Doc -> TError a -> Doc
ppError Tidy
k (CtxError SpecType -> Doc
forall t. CtxError t -> Doc
ctCtx CtxError SpecType
ce) (UserError -> Doc) -> UserError -> Doc
forall a b. (a -> b) -> a -> b
$ SpecType -> Doc
ppSpecTypeErr (SpecType -> Doc) -> Error -> UserError
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CtxError SpecType -> Error
forall t. CtxError t -> TError t
ctErr CtxError SpecType
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
. (SpecType -> Doc) -> Error -> UserError
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 = Tidy -> SpecType -> Doc
forall c tv r. OkRT c tv r => Tidy -> RType c tv r -> Doc
rtypeDoc     Tidy
k
             (SpecType -> Doc) -> (SpecType -> SpecType) -> SpecType -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Tidy -> SpecType -> SpecType
tidySpecType Tidy
k
             (SpecType -> SpecType)
-> (SpecType -> SpecType) -> SpecType -> SpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (UReft Reft -> UReft Reft) -> SpecType -> SpecType
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 (ECst Expr
x Sort
_) = Expr
x
    noCasts Expr
e          = Expr
e

instance Show Error where
  show :: Error -> String
show = Error -> String
forall a. PPrint a => a -> String
showpp

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