{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE FlexibleInstances #-}
{-# OPTIONS_GHC -Wno-orphans #-}
module Language.Haskell.Liquid.UX.Tidy (
tidySpecType
, tidySymbol
, panicError
, Result (..)
, errorToUserError
, 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
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
class Result a where
result :: a -> FixResult UserError
instance Result UserError where
result :: UserError -> FixResult UserError
result UserError
e = [(UserError, Maybe [Char])] -> [Char] -> FixResult UserError
forall a. [(a, Maybe [Char])] -> [Char] -> FixResult a
Crash [(UserError
e, Maybe [Char]
forall a. Maybe a
Nothing)] [Char]
""
instance Result [Error] where
result :: [Error] -> FixResult UserError
result [Error]
es = [(UserError, Maybe [Char])] -> [Char] -> FixResult UserError
forall a. [(a, Maybe [Char])] -> [Char] -> FixResult a
Crash ([ (Error -> UserError
errorToUserError Error
e, Maybe [Char]
forall a. Maybe a
Nothing) | Error
e <- [Error]
es]) [Char]
""
instance Result Error where
result :: Error -> FixResult UserError
result Error
e = [Error] -> FixResult UserError
forall a. Result a => a -> FixResult UserError
result [Error
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 = (RType 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 RType RTyCon RTyVar RReft -> Doc
ppSpecTypeErr
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 ([Char] -> Doc
text ([Char] -> Doc) -> [Char] -> Doc
forall a b. (a -> b) -> a -> b
$ [Char]
"Cinfo: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ SrcSpan -> [Char]
forall a. Outputable a => a -> [Char]
GM.showPpr SrcSpan
l)
tidySpecType :: Tidy -> SpecType -> SpecType
tidySpecType :: Tidy -> RType RTyCon RTyVar RReft -> RType RTyCon RTyVar RReft
tidySpecType Tidy
k
= RType RTyCon RTyVar RReft -> RType RTyCon RTyVar RReft
tidyEqual
(RType RTyCon RTyVar RReft -> RType RTyCon RTyVar RReft)
-> (RType RTyCon RTyVar RReft -> RType RTyCon RTyVar RReft)
-> RType RTyCon RTyVar RReft
-> RType RTyCon RTyVar RReft
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RType RTyCon RTyVar RReft -> RType RTyCon RTyVar RReft
tidyValueVars
(RType RTyCon RTyVar RReft -> RType RTyCon RTyVar RReft)
-> (RType RTyCon RTyVar RReft -> RType RTyCon RTyVar RReft)
-> RType RTyCon RTyVar RReft
-> RType RTyCon RTyVar RReft
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RType RTyCon RTyVar RReft -> RType RTyCon RTyVar RReft
tidyDSymbols
(RType RTyCon RTyVar RReft -> RType RTyCon RTyVar RReft)
-> (RType RTyCon RTyVar RReft -> RType RTyCon RTyVar RReft)
-> RType RTyCon RTyVar RReft
-> RType RTyCon RTyVar RReft
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Tidy -> RType RTyCon RTyVar RReft -> RType RTyCon RTyVar RReft
tidySymbols Tidy
k
(RType RTyCon RTyVar RReft -> RType RTyCon RTyVar RReft)
-> (RType RTyCon RTyVar RReft -> RType RTyCon RTyVar RReft)
-> RType RTyCon RTyVar RReft
-> RType RTyCon RTyVar RReft
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RType RTyCon RTyVar RReft -> RType RTyCon RTyVar RReft
tidyInternalRefas
(RType RTyCon RTyVar RReft -> RType RTyCon RTyVar RReft)
-> (RType RTyCon RTyVar RReft -> RType RTyCon RTyVar RReft)
-> RType RTyCon RTyVar RReft
-> RType RTyCon RTyVar RReft
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Tidy -> RType RTyCon RTyVar RReft -> RType RTyCon RTyVar RReft
tidyLocalRefas Tidy
k
(RType RTyCon RTyVar RReft -> RType RTyCon RTyVar RReft)
-> (RType RTyCon RTyVar RReft -> RType RTyCon RTyVar RReft)
-> RType RTyCon RTyVar RReft
-> RType RTyCon RTyVar RReft
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RType RTyCon RTyVar RReft -> RType RTyCon RTyVar RReft
tidyFunBinds
(RType RTyCon RTyVar RReft -> RType RTyCon RTyVar RReft)
-> (RType RTyCon RTyVar RReft -> RType RTyCon RTyVar RReft)
-> RType RTyCon RTyVar RReft
-> RType RTyCon RTyVar RReft
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RType RTyCon RTyVar RReft -> RType RTyCon RTyVar RReft
tidyTyVars
tidyValueVars :: SpecType -> SpecType
tidyValueVars :: RType RTyCon RTyVar RReft -> RType RTyCon RTyVar RReft
tidyValueVars = (RReft -> RReft)
-> RType RTyCon RTyVar RReft -> RType RTyCon RTyVar RReft
forall r1 r2 c tv. (r1 -> r2) -> RType c tv r1 -> RType c tv r2
mapReft ((RReft -> RReft)
-> RType RTyCon RTyVar RReft -> RType RTyCon RTyVar RReft)
-> (RReft -> RReft)
-> RType RTyCon RTyVar RReft
-> RType RTyCon RTyVar RReft
forall a b. (a -> b) -> a -> b
$ \RReft
u -> RReft
u { ur_reft = tidyVV $ ur_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 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 :: [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 -> RType RTyCon RTyVar RReft -> RType RTyCon RTyVar RReft
tidySymbols Tidy
k RType RTyCon RTyVar RReft
t = (Symbol -> Symbol)
-> RType RTyCon RTyVar RReft -> RType RTyCon RTyVar RReft
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) (RType RTyCon RTyVar RReft -> RType RTyCon RTyVar RReft)
-> RType RTyCon RTyVar RReft -> RType RTyCon RTyVar RReft
forall a b. (a -> b) -> a -> b
$ (Symbol -> Symbol)
-> RType RTyCon RTyVar RReft -> RType RTyCon RTyVar RReft
forall c tv r. (Symbol -> Symbol) -> RType c tv r -> RType c tv r
mapBind Symbol -> Symbol
dropBind RType RTyCon RTyVar RReft
t
where
xs :: HashSet Symbol
xs = [Symbol] -> HashSet Symbol
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList (RType RTyCon RTyVar RReft -> [Symbol]
forall a. Subable a => a -> [Symbol]
syms RType RTyCon RTyVar RReft
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 -> RType RTyCon RTyVar RReft -> RType RTyCon RTyVar RReft
tidyLocalRefas Tidy
k = (RReft -> RReft)
-> RType RTyCon RTyVar RReft -> RType RTyCon RTyVar RReft
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 = RReft -> RReft
forall a. a -> a
id
txReft' Tidy
Lossy = RReft -> RReft
txReft
txReft :: RReft -> RReft
txReft RReft
u = RReft
u { ur_reft = mapPredReft dropLocals $ ur_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 :: RType RTyCon RTyVar RReft -> RType RTyCon RTyVar RReft
tidyEqual = (RReft -> RReft)
-> RType RTyCon RTyVar RReft -> RType RTyCon RTyVar RReft
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 = mapPredReft dropInternals $ ur_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 :: RType RTyCon RTyVar RReft -> RType RTyCon RTyVar RReft
tidyInternalRefas = (RReft -> RReft)
-> RType RTyCon RTyVar RReft -> RType RTyCon RTyVar RReft
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 = mapPredReft dropInternals $ ur_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 :: RType RTyCon RTyVar RReft -> RType RTyCon RTyVar RReft
tidyDSymbols RType RTyCon RTyVar RReft
t = (Symbol -> Symbol)
-> RType RTyCon RTyVar RReft -> RType RTyCon RTyVar RReft
forall c tv r. (Symbol -> Symbol) -> RType c tv r -> RType c tv r
mapBind Symbol -> Symbol
tx (RType RTyCon RTyVar RReft -> RType RTyCon RTyVar RReft)
-> RType RTyCon RTyVar RReft -> RType RTyCon RTyVar RReft
forall a b. (a -> b) -> a -> b
$ (Symbol -> Symbol)
-> RType RTyCon RTyVar RReft -> RType RTyCon RTyVar RReft
forall a. Subable a => (Symbol -> Symbol) -> a -> a
substa Symbol -> Symbol
tx RType RTyCon RTyVar RReft
t
where
tx :: Symbol -> Symbol
tx = [Symbol] -> Symbol -> Symbol
bindersTx [Symbol
x | Symbol
x <- RType RTyCon RTyVar RReft -> [Symbol]
forall a. Subable a => a -> [Symbol]
syms RType RTyCon RTyVar RReft
t, Symbol -> Bool
isTmp Symbol
x]
isTmp :: Symbol -> Bool
isTmp = (Symbol
tempPrefix Symbol -> Symbol -> Bool
`isPrefixOfSym`)
tidyFunBinds :: SpecType -> SpecType
tidyFunBinds :: RType RTyCon RTyVar RReft -> RType RTyCon RTyVar RReft
tidyFunBinds RType RTyCon RTyVar RReft
t = (Symbol -> Symbol)
-> RType RTyCon RTyVar RReft -> RType RTyCon RTyVar RReft
forall c tv r. (Symbol -> Symbol) -> RType c tv r -> RType c tv r
mapBind Symbol -> Symbol
tx (RType RTyCon RTyVar RReft -> RType RTyCon RTyVar RReft)
-> RType RTyCon RTyVar RReft -> RType RTyCon RTyVar RReft
forall a b. (a -> b) -> a -> b
$ (Symbol -> Symbol)
-> RType RTyCon RTyVar RReft -> RType RTyCon RTyVar RReft
forall a. Subable a => (Symbol -> Symbol) -> a -> a
substa Symbol -> Symbol
tx RType 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
$ RType RTyCon RTyVar RReft -> [Symbol]
forall t t1 t2. RType t t1 t2 -> [Symbol]
funBinds RType RTyCon RTyVar RReft
t
tidyTyVars :: SpecType -> SpecType
tidyTyVars :: RType RTyCon RTyVar RReft -> RType RTyCon RTyVar RReft
tidyTyVars RType RTyCon RTyVar RReft
t = [(RTyVar, RType RTyCon RTyVar (), RType RTyCon RTyVar RReft)]
-> RType RTyCon RTyVar RReft -> RType RTyCon RTyVar RReft
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 (), RType RTyCon RTyVar RReft)]
forall {c}. [(RTyVar, RType c RTyVar (), RType c RTyVar RReft)]
αβs RType RTyCon RTyVar RReft
t
where
αβs :: [(RTyVar, RType c RTyVar (), RType c RTyVar RReft)]
αβs = (RTyVar
-> RType c RTyVar RReft
-> (RTyVar, RType c RTyVar (), RType c RTyVar RReft))
-> [RTyVar]
-> [RType c RTyVar RReft]
-> [(RTyVar, RType c RTyVar (), RType c RTyVar RReft)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\RTyVar
α RType c RTyVar RReft
β -> (RTyVar
α, RType c RTyVar RReft -> RType c RTyVar ()
forall c tv r. RType c tv r -> RType c tv ()
toRSort RType c RTyVar RReft
β, RType c RTyVar RReft
β)) [RTyVar]
αs [RType c RTyVar RReft]
forall {c}. [RType c RTyVar RReft]
βs
αs :: [RTyVar]
αs = [RTyVar] -> [RTyVar]
forall a. Eq a => [a] -> [a]
L.nub (RType RTyCon RTyVar RReft -> [RTyVar]
forall c tv r. RType c tv r -> [tv]
tyVars RType RTyCon RTyVar RReft
t)
βs :: [RType c RTyVar RReft]
βs = ([Char] -> RType c RTyVar RReft)
-> [[Char]] -> [RType c RTyVar RReft]
forall a b. (a -> b) -> [a] -> [b]
map (Var -> RType c RTyVar RReft
forall r c. Monoid r => Var -> RType c RTyVar r
rVar (Var -> RType c RTyVar RReft)
-> ([Char] -> Var) -> [Char] -> RType c RTyVar RReft
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']] [[Char]] -> [[Char]] -> [[Char]]
forall a. [a] -> [a] -> [a]
++ [ [Char]
"t" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
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 -> 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
$ 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 = [Char] -> Symbol
forall a. Symbolic a => a -> Symbol
symbol ([Char] -> Symbol) -> (Int -> [Char]) -> Int -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char
'x' Char -> [Char] -> [Char]
forall a. a -> [a] -> [a]
:) ([Char] -> [Char]) -> (Int -> [Char]) -> Int -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> [Char]
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) = 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 (RFun Symbol
_ RFInfo
_ 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 :: 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 = [(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 RTVar k (RType c k ())
a RType c k r
t r
r) = RTVar k (RType 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 -> RTVar k (RType c k ())
forall tv s. tv -> RTVar tv s
makeRTVar (k -> RTVar k (RType c k ())) -> k -> RTVar k (RType 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 (RTVar k (RType c k ()) -> k
forall tv s. RTVar tv s -> tv
ty_var_value RTVar k (RType c k ())
a) (RTVar k (RType c k ()) -> k
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 = [(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
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
_) = 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 (RFun Symbol
b RFInfo
_ 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
_) = []
panicError :: Error -> a
panicError :: forall a. Error -> a
panicError = Error -> a
forall a e. Exception e => e -> a
Ex.throw
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 (RType RTyCon RTyVar RReft) -> Doc
pprintTidy Tidy
k CtxError (RType RTyCon RTyVar RReft)
ce = Tidy -> Doc -> UserError -> Doc
forall a. (PPrint a, Show a) => Tidy -> Doc -> TError a -> Doc
ppError Tidy
k (CtxError (RType RTyCon RTyVar RReft) -> Doc
forall t. CtxError t -> Doc
ctCtx CtxError (RType RTyCon RTyVar RReft)
ce) (UserError -> Doc) -> UserError -> Doc
forall a b. (a -> b) -> a -> b
$ RType RTyCon RTyVar RReft -> Doc
ppSpecTypeErr (RType RTyCon RTyVar RReft -> Doc) -> Error -> UserError
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> CtxError (RType RTyCon RTyVar RReft) -> Error
forall t. CtxError t -> TError t
ctErr CtxError (RType 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
. (RType 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 RType RTyCon RTyVar RReft -> Doc
ppSpecTypeErr
ppSpecTypeErr :: SpecType -> Doc
ppSpecTypeErr :: RType RTyCon RTyVar RReft -> Doc
ppSpecTypeErr = Tidy -> RType RTyCon RTyVar RReft -> Doc
ppSpecType Tidy
Lossy
ppSpecType :: Tidy -> SpecType -> Doc
ppSpecType :: Tidy -> RType RTyCon RTyVar RReft -> Doc
ppSpecType Tidy
k = Tidy -> RType RTyCon RTyVar RReft -> Doc
forall c tv r. OkRT c tv r => Tidy -> RType c tv r -> Doc
rtypeDoc Tidy
k
(RType RTyCon RTyVar RReft -> Doc)
-> (RType RTyCon RTyVar RReft -> RType RTyCon RTyVar RReft)
-> RType RTyCon RTyVar RReft
-> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Tidy -> RType RTyCon RTyVar RReft -> RType RTyCon RTyVar RReft
tidySpecType Tidy
k
(RType RTyCon RTyVar RReft -> RType RTyCon RTyVar RReft)
-> (RType RTyCon RTyVar RReft -> RType RTyCon RTyVar RReft)
-> RType RTyCon RTyVar RReft
-> RType RTyCon RTyVar RReft
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (RReft -> RReft)
-> RType RTyCon RTyVar RReft -> RType RTyCon RTyVar RReft
forall a b.
(a -> b) -> RType RTyCon RTyVar a -> RType 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 (ECst Expr
x Sort
_) = Expr
x
noCasts Expr
e = Expr
e
instance Show Error where
show :: Error -> [Char]
show Error
e = Doc -> [Char]
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]