{-# LANGUAGE OverloadedStrings #-}
{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
module Language.Haskell.Liquid.WiredIn
( wiredTyCons
, wiredDataCons
, wiredSortedSyms
, charDataCon
, dictionaryVar
, dictionaryTyVar
, dictionaryBind
, proofTyConName
, combineProofsName
, isWiredIn
, isWiredInName
, dcPrefix
, isDerivedInstance
) where
import Prelude hiding (error)
import Language.Haskell.Liquid.GHC.Misc
import qualified Liquid.GHC.API as Ghc
import Liquid.GHC.API (Var, Arity, TyVar, Bind(..), Boxity(..), Expr(..), ArgFlag(..))
import Language.Haskell.Liquid.Types.Types
import Language.Haskell.Liquid.Types.RefType
import Language.Haskell.Liquid.Types.Variance
import Language.Haskell.Liquid.Types.PredType
import Language.Haskell.Liquid.Types.Names (selfSymbol)
import qualified Language.Fixpoint.Types as F
import qualified Data.HashSet as S
import Language.Haskell.Liquid.GHC.TypeRep ()
isWiredIn :: F.LocSymbol -> Bool
isWiredIn :: LocSymbol -> Bool
isWiredIn LocSymbol
x = LocSymbol -> Bool
isWiredInLoc LocSymbol
x Bool -> Bool -> Bool
|| Symbol -> Bool
isWiredInName (forall a. Located a -> a
val LocSymbol
x) Bool -> Bool -> Bool
|| LocSymbol -> Bool
isWiredInShape LocSymbol
x
isWiredInLoc :: F.LocSymbol -> Bool
isWiredInLoc :: LocSymbol -> Bool
isWiredInLoc LocSymbol
sym = Line
ln forall a. Eq a => a -> a -> Bool
== Line
ln' Bool -> Bool -> Bool
&& Line
ln forall a. Eq a => a -> a -> Bool
== Int -> Line
F.safePos Int
1 Bool -> Bool -> Bool
&& Line
c forall a. Eq a => a -> a -> Bool
== Line
c' Bool -> Bool -> Bool
&& Line
c' forall a. Eq a => a -> a -> Bool
== Int -> Line
F.safePos Int
1
where
(Line
ln , Line
c) = SourcePos -> (Line, Line)
spe (forall a. Located a -> SourcePos
loc LocSymbol
sym)
(Line
ln', Line
c') = SourcePos -> (Line, Line)
spe (forall a. Located a -> SourcePos
locE LocSymbol
sym)
spe :: SourcePos -> (Line, Line)
spe SourcePos
l = (Line
x, Line
y) where ([Char]
_, Line
x, Line
y) = SourcePos -> ([Char], Line, Line)
F.sourcePosElts SourcePos
l
isWiredInName :: F.Symbol -> Bool
isWiredInName :: Symbol -> Bool
isWiredInName Symbol
x = Symbol
x forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`S.member` HashSet Symbol
wiredInNames
wiredInNames :: S.HashSet F.Symbol
wiredInNames :: HashSet Symbol
wiredInNames = forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList [ Symbol
"head", Symbol
"tail", Symbol
"fst", Symbol
"snd", Symbol
"len"]
isWiredInShape :: F.LocSymbol -> Bool
isWiredInShape :: LocSymbol -> Bool
isWiredInShape LocSymbol
x = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Symbol -> Symbol -> Bool
`F.isPrefixOfSym` forall a. Located a -> a
val LocSymbol
x) [Symbol
F.anfPrefix, Symbol
F.tempPrefix, Symbol
dcPrefix]
dcPrefix :: F.Symbol
dcPrefix :: Symbol
dcPrefix = Symbol
"lqdc"
wiredSortedSyms :: [(F.Symbol, F.Sort)]
wiredSortedSyms :: [(Symbol, Sort)]
wiredSortedSyms = (Symbol
selfSymbol,Sort
selfSort)forall a. a -> [a] -> [a]
:[(forall a. Show a => a -> Symbol
pappSym Int
n, Int -> Sort
pappSort Int
n) | Int
n <- [Int
1..Int
pappArity]]
where selfSort :: Sort
selfSort = Int -> Sort -> Sort
F.FAbs Int
1 (Int -> Sort
F.FVar Int
0)
dictionaryVar :: Var
dictionaryVar :: Var
dictionaryVar = [Char] -> Type -> Var
stringVar [Char]
"tmp_dictionary_var" (TyCoVarBinder -> Type -> Type
Ghc.ForAllTy (forall var argf. var -> argf -> VarBndr var argf
Ghc.Bndr Var
dictionaryTyVar ArgFlag
Required) forall a b. (a -> b) -> a -> b
$ Var -> Type
Ghc.TyVarTy Var
dictionaryTyVar)
dictionaryTyVar :: TyVar
dictionaryTyVar :: Var
dictionaryTyVar = [Char] -> Var
stringTyVar [Char]
"da"
dictionaryBind :: Bind Var
dictionaryBind :: Bind Var
dictionaryBind = forall b. [(b, Expr b)] -> Bind b
Rec [(Var
v, forall b. b -> Expr b -> Expr b
Lam Var
a forall a b. (a -> b) -> a -> b
$ forall b. Expr b -> Expr b -> Expr b
App (forall b. Var -> Expr b
Var Var
v) (forall b. Type -> Expr b
Type forall a b. (a -> b) -> a -> b
$ Var -> Type
Ghc.TyVarTy Var
a))]
where
v :: Var
v = Var
dictionaryVar
a :: Var
a = Var
dictionaryTyVar
combineProofsName :: String
combineProofsName :: [Char]
combineProofsName = [Char]
"combineProofs"
proofTyConName :: F.Symbol
proofTyConName :: Symbol
proofTyConName = Symbol
"Proof"
maxArity :: Arity
maxArity :: Int
maxArity = Int
7
wiredTyCons :: [TyConP]
wiredTyCons :: [TyConP]
wiredTyCons = forall a b. (a, b) -> a
fst ([TyConP], [Located DataConP])
wiredTyDataCons
wiredDataCons :: [Located DataConP]
wiredDataCons :: [Located DataConP]
wiredDataCons = forall a b. (a, b) -> b
snd ([TyConP], [Located DataConP])
wiredTyDataCons
wiredTyDataCons :: ([TyConP] , [Located DataConP])
wiredTyDataCons :: ([TyConP], [Located DataConP])
wiredTyDataCons = (forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[TyConP]]
tcs, forall a. a -> Located a
dummyLoc forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[DataConP]]
dcs)
where
([[TyConP]]
tcs, [[DataConP]]
dcs) = forall a b. [(a, b)] -> ([a], [b])
unzip forall a b. (a -> b) -> a -> b
$ ([TyConP], [DataConP])
listTyDataCons forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map Int -> ([TyConP], [DataConP])
tupleTyDataCons [Int
2..Int
maxArity]
charDataCon :: Located DataConP
charDataCon :: Located DataConP
charDataCon = forall a. a -> Located a
dummyLoc (SourcePos
-> DataCon
-> [RTyVar]
-> [PVar RSort]
-> [SpecType]
-> [(Symbol, SpecType)]
-> SpecType
-> Bool
-> Symbol
-> SourcePos
-> DataConP
DataConP SourcePos
l0 DataCon
Ghc.charDataCon [] [] [] [(Symbol
"charX",forall {tv}. RType RTyCon tv RReft
lt)] forall {tv}. RType RTyCon tv RReft
lt Bool
False Symbol
wiredInName SourcePos
l0)
where
l0 :: SourcePos
l0 = [Char] -> SourcePos
F.dummyPos [Char]
"LH.Bare.charTyDataCons"
c :: TyCon
c = TyCon
Ghc.charTyCon
lt :: RType RTyCon tv RReft
lt = forall tv r.
TyCon
-> [RType RTyCon tv r]
-> [RTProp RTyCon tv r]
-> r
-> RType RTyCon tv r
rApp TyCon
c [] [] forall a. Monoid a => a
mempty
listTyDataCons :: ([TyConP] , [DataConP])
listTyDataCons :: ([TyConP], [DataConP])
listTyDataCons = ( [SourcePos
-> TyCon
-> [RTyVar]
-> [PVar RSort]
-> VarianceInfo
-> VarianceInfo
-> Maybe SizeFun
-> TyConP
TyConP SourcePos
l0 TyCon
c [Var -> RTyVar
RTV Var
tyv] [PVar RSort
p] [Variance
Covariant] [Variance
Covariant] (forall a. a -> Maybe a
Just SizeFun
fsize)]
, [SourcePos
-> DataCon
-> [RTyVar]
-> [PVar RSort]
-> [SpecType]
-> [(Symbol, SpecType)]
-> SpecType
-> Bool
-> Symbol
-> SourcePos
-> DataConP
DataConP SourcePos
l0 DataCon
Ghc.nilDataCon [Var -> RTyVar
RTV Var
tyv] [PVar RSort
p] [] [] SpecType
lt Bool
False Symbol
wiredInName SourcePos
l0
, SourcePos
-> DataCon
-> [RTyVar]
-> [PVar RSort]
-> [SpecType]
-> [(Symbol, SpecType)]
-> SpecType
-> Bool
-> Symbol
-> SourcePos
-> DataConP
DataConP SourcePos
l0 DataCon
Ghc.consDataCon [Var -> RTyVar
RTV Var
tyv] [PVar RSort
p] [] [(Symbol, SpecType)]
cargs SpecType
lt Bool
False Symbol
wiredInName SourcePos
l0])
where
l0 :: SourcePos
l0 = [Char] -> SourcePos
F.dummyPos [Char]
"LH.Bare.listTyDataCons"
c :: TyCon
c = TyCon
Ghc.listTyCon
[Var
tyv] = TyCon -> [Var]
tyConTyVarsDef TyCon
c
t :: RSort
t = forall r c. Monoid r => Var -> RType c RTyVar r
rVar Var
tyv :: RSort
fld :: Symbol
fld = Symbol
"fldList"
xHead :: Symbol
xHead = Symbol
"head"
xTail :: Symbol
xTail = Symbol
"tail"
p :: PVar RSort
p = forall t.
Symbol -> PVKind t -> Symbol -> [(t, Symbol, Expr)] -> PVar t
PV Symbol
"p" (forall t. t -> PVKind t
PVProp RSort
t) (Maybe Integer -> Symbol
F.vv forall a. Maybe a
Nothing) [(RSort
t, Symbol
fld, Symbol -> Expr
F.EVar Symbol
fld)]
px :: RReft
px = forall t. PVar t -> RReft
pdVarReft forall a b. (a -> b) -> a -> b
$ forall t.
Symbol -> PVKind t -> Symbol -> [(t, Symbol, Expr)] -> PVar t
PV Symbol
"p" (forall t. t -> PVKind t
PVProp RSort
t) (Maybe Integer -> Symbol
F.vv forall a. Maybe a
Nothing) [(RSort
t, Symbol
fld, Symbol -> Expr
F.EVar Symbol
xHead)]
lt :: SpecType
lt = forall tv r.
TyCon
-> [RType RTyCon tv r]
-> [RTProp RTyCon tv r]
-> r
-> RType RTyCon tv r
rApp TyCon
c [forall {c}. RType c RTyVar RReft
xt] [forall τ r c tv. [(Symbol, τ)] -> r -> Ref τ (RType c tv r)
rPropP [] forall a b. (a -> b) -> a -> b
$ forall t. PVar t -> RReft
pdVarReft PVar RSort
p] forall a. Monoid a => a
mempty
xt :: RType c RTyVar RReft
xt = forall r c. Monoid r => Var -> RType c RTyVar r
rVar Var
tyv
xst :: SpecType
xst = forall tv r.
TyCon
-> [RType RTyCon tv r]
-> [RTProp RTyCon tv r]
-> r
-> RType RTyCon tv r
rApp TyCon
c [forall c tv r. tv -> r -> RType c tv r
RVar (Var -> RTyVar
RTV Var
tyv) RReft
px] [forall τ r c tv. [(Symbol, τ)] -> r -> Ref τ (RType c tv r)
rPropP [] forall a b. (a -> b) -> a -> b
$ forall t. PVar t -> RReft
pdVarReft PVar RSort
p] forall a. Monoid a => a
mempty
cargs :: [(Symbol, SpecType)]
cargs = [(Symbol
xTail, SpecType
xst), (Symbol
xHead, forall {c}. RType c RTyVar RReft
xt)]
fsize :: SizeFun
fsize = LocSymbol -> SizeFun
SymSizeFun (forall a. a -> Located a
dummyLoc Symbol
"len")
wiredInName :: F.Symbol
wiredInName :: Symbol
wiredInName = Symbol
"WiredIn"
tupleTyDataCons :: Int -> ([TyConP] , [DataConP])
tupleTyDataCons :: Int -> ([TyConP], [DataConP])
tupleTyDataCons Int
n = ( [SourcePos
-> TyCon
-> [RTyVar]
-> [PVar RSort]
-> VarianceInfo
-> VarianceInfo
-> Maybe SizeFun
-> TyConP
TyConP SourcePos
l0 TyCon
c (Var -> RTyVar
RTV forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Var]
tyvs) [PVar RSort]
ps VarianceInfo
tyvarinfo VarianceInfo
pdvarinfo forall a. Maybe a
Nothing]
, [SourcePos
-> DataCon
-> [RTyVar]
-> [PVar RSort]
-> [SpecType]
-> [(Symbol, SpecType)]
-> SpecType
-> Bool
-> Symbol
-> SourcePos
-> DataConP
DataConP SourcePos
l0 DataCon
dc (Var -> RTyVar
RTV forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Var]
tyvs) [PVar RSort]
ps [] forall {c}. [(Symbol, RType c RTyVar RReft)]
cargs SpecType
lt Bool
False Symbol
wiredInName SourcePos
l0])
where
tyvarinfo :: VarianceInfo
tyvarinfo = forall a. Int -> a -> [a]
replicate Int
n Variance
Covariant
pdvarinfo :: VarianceInfo
pdvarinfo = forall a. Int -> a -> [a]
replicate (Int
nforall a. Num a => a -> a -> a
-Int
1) Variance
Covariant
l0 :: SourcePos
l0 = [Char] -> SourcePos
F.dummyPos [Char]
"LH.Bare.tupleTyDataCons"
c :: TyCon
c = Boxity -> Int -> TyCon
Ghc.tupleTyCon Boxity
Boxed Int
n
dc :: DataCon
dc = Boxity -> Int -> DataCon
Ghc.tupleDataCon Boxity
Boxed Int
n
tyvs :: [Var]
tyvs@(Var
tv:[Var]
tvs) = TyCon -> [Var]
tyConTyVarsDef TyCon
c
(RSort
ta:[RSort]
ts) = (forall r c. Monoid r => Var -> RType c RTyVar r
rVar forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Var]
tyvs) :: [RSort]
flds :: [Symbol]
flds = [Char] -> [Symbol]
mks [Char]
"fld_Tuple"
fld :: Symbol
fld = Symbol
"fld_Tuple"
Symbol
x1:[Symbol]
xs = [Char] -> [Symbol]
mks ([Char]
"x_Tuple" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Int
n)
ps :: [PVar RSort]
ps = forall t. [Symbol] -> [t] -> [(Symbol, Expr)] -> [PVar t]
mkps [Symbol]
pnames (RSort
taforall a. a -> [a] -> [a]
:[RSort]
ts) ((Symbol
fld, Symbol -> Expr
F.EVar Symbol
fld) forall a. a -> [a] -> [a]
: forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
flds (Symbol -> Expr
F.EVar forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol]
flds))
ups :: [UsedPVar]
ups = forall t. PVar t -> UsedPVar
uPVar forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [PVar RSort]
ps
pxs :: [PVar RSort]
pxs = forall t. [Symbol] -> [t] -> [(Symbol, Expr)] -> [PVar t]
mkps [Symbol]
pnames (RSort
taforall a. a -> [a] -> [a]
:[RSort]
ts) ((Symbol
fld, Symbol -> Expr
F.EVar Symbol
x1) forall a. a -> [a] -> [a]
: forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
flds (Symbol -> Expr
F.EVar forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol]
xs))
lt :: SpecType
lt = forall tv r.
TyCon
-> [RType RTyCon tv r]
-> [RTProp RTyCon tv r]
-> r
-> RType RTyCon tv r
rApp TyCon
c (forall r c. Monoid r => Var -> RType c RTyVar r
rVar forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Var]
tyvs) (forall τ r c tv. [(Symbol, τ)] -> r -> Ref τ (RType c tv r)
rPropP [] forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. PVar t -> RReft
pdVarReft forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [UsedPVar]
ups) forall a. Monoid a => a
mempty
xts :: [RType c RTyVar RReft]
xts = forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\Var
v PVar RSort
p -> forall c tv r. tv -> r -> RType c tv r
RVar (Var -> RTyVar
RTV Var
v) (forall t. PVar t -> RReft
pdVarReft PVar RSort
p)) [Var]
tvs [PVar RSort]
pxs
cargs :: [(Symbol, RType c RTyVar RReft)]
cargs = forall a. [a] -> [a]
reverse forall a b. (a -> b) -> a -> b
$ (Symbol
x1, forall r c. Monoid r => Var -> RType c RTyVar r
rVar Var
tv) forall a. a -> [a] -> [a]
: forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
xs forall {c}. [RType c RTyVar RReft]
xts
pnames :: [Symbol]
pnames = [Char] -> [Symbol]
mks_ [Char]
"p"
mks :: [Char] -> [Symbol]
mks [Char]
x = (\Int
i -> forall a. Symbolic a => a -> Symbol
F.symbol ([Char]
xforall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Int
i)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Int
1..Int
n]
mks_ :: [Char] -> [Symbol]
mks_ [Char]
x = (\Int
i -> forall a. Symbolic a => a -> Symbol
F.symbol ([Char]
xforall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Int
i)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Int
2..Int
n]
mkps :: [F.Symbol]
-> [t] -> [(F.Symbol, F.Expr)] -> [PVar t]
mkps :: forall t. [Symbol] -> [t] -> [(Symbol, Expr)] -> [PVar t]
mkps [Symbol]
ns (t
t:[t]
ts) ((Symbol
f,Expr
x):[(Symbol, Expr)]
fxs) = forall a. [a] -> [a]
reverse forall a b. (a -> b) -> a -> b
$ forall t.
[Symbol]
-> [t]
-> [(Symbol, Expr)]
-> [(t, Symbol, Expr)]
-> [PVar t]
-> [PVar t]
mkps_ [Symbol]
ns [t]
ts [(Symbol, Expr)]
fxs [(t
t, Symbol
f, Expr
x)] []
mkps [Symbol]
_ [t]
_ [(Symbol, Expr)]
_ = forall a. Maybe SrcSpan -> [Char] -> a
panic forall a. Maybe a
Nothing [Char]
"Bare : mkps"
mkps_ :: [F.Symbol]
-> [t]
-> [(F.Symbol, F.Expr)]
-> [(t, F.Symbol, F.Expr)]
-> [PVar t]
-> [PVar t]
mkps_ :: forall t.
[Symbol]
-> [t]
-> [(Symbol, Expr)]
-> [(t, Symbol, Expr)]
-> [PVar t]
-> [PVar t]
mkps_ [] [t]
_ [(Symbol, Expr)]
_ [(t, Symbol, Expr)]
_ [PVar t]
ps = [PVar t]
ps
mkps_ (Symbol
n:[Symbol]
ns) (t
t:[t]
ts) ((Symbol
f, Expr
x):[(Symbol, Expr)]
xs) [(t, Symbol, Expr)]
args [PVar t]
ps = forall t.
[Symbol]
-> [t]
-> [(Symbol, Expr)]
-> [(t, Symbol, Expr)]
-> [PVar t]
-> [PVar t]
mkps_ [Symbol]
ns [t]
ts [(Symbol, Expr)]
xs ((t, Symbol, Expr)
aforall a. a -> [a] -> [a]
:[(t, Symbol, Expr)]
args) (PVar t
pforall a. a -> [a] -> [a]
:[PVar t]
ps)
where
p :: PVar t
p = forall t.
Symbol -> PVKind t -> Symbol -> [(t, Symbol, Expr)] -> PVar t
PV Symbol
n (forall t. t -> PVKind t
PVProp t
t) (Maybe Integer -> Symbol
F.vv forall a. Maybe a
Nothing) [(t, Symbol, Expr)]
args
a :: (t, Symbol, Expr)
a = (t
t, Symbol
f, Expr
x)
mkps_ [Symbol]
_ [t]
_ [(Symbol, Expr)]
_ [(t, Symbol, Expr)]
_ [PVar t]
_ = forall a. Maybe SrcSpan -> [Char] -> a
panic forall a. Maybe a
Nothing [Char]
"Bare : mkps_"
isDerivedInstance :: Ghc.ClsInst -> Bool
isDerivedInstance :: ClsInst -> Bool
isDerivedInstance ClsInst
i = forall a. PPrint a => [Char] -> a -> a
F.notracepp ([Char]
"IS-DERIVED: " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
F.showpp Symbol
classSym)
forall a b. (a -> b) -> a -> b
$ forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
S.member Symbol
classSym HashSet Symbol
derivingClasses
where
classSym :: Symbol
classSym = forall a. Symbolic a => a -> Symbol
F.symbol forall b c a. (b -> c) -> (a -> b) -> a -> c
. ClsInst -> Class
Ghc.is_cls forall a b. (a -> b) -> a -> b
$ ClsInst
i
derivingClasses :: S.HashSet F.Symbol
derivingClasses :: HashSet Symbol
derivingClasses = forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList
[ Symbol
"GHC.Classes.Eq"
, Symbol
"GHC.Classes.Ord"
, Symbol
"GHC.Enum.Enum"
, Symbol
"GHC.Show.Show"
, Symbol
"GHC.Read.Read"
, Symbol
"GHC.Base.Monad"
, Symbol
"GHC.Base.Applicative"
, Symbol
"GHC.Base.Functor"
, Symbol
"Data.Foldable.Foldable"
, Symbol
"Data.Traversable.Traversable"
, Symbol
"GHC.Real.Fractional"
]