{-# 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(..), ForAllTyFlag(Required))
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 (LocSymbol -> Symbol
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 Line -> Line -> Bool
forall a. Eq a => a -> a -> Bool
== Line
ln' Bool -> Bool -> Bool
&& Line
ln Line -> Line -> Bool
forall a. Eq a => a -> a -> Bool
== Int -> Line
F.safePos Int
1 Bool -> Bool -> Bool
&& Line
c Line -> Line -> Bool
forall a. Eq a => a -> a -> Bool
== Line
c' Bool -> Bool -> Bool
&& Line
c' Line -> Line -> Bool
forall a. Eq a => a -> a -> Bool
== Int -> Line
F.safePos Int
1
where
(Line
ln , Line
c) = SourcePos -> (Line, Line)
spe (LocSymbol -> SourcePos
forall a. Located a -> SourcePos
loc LocSymbol
sym)
(Line
ln', Line
c') = SourcePos -> (Line, Line)
spe (LocSymbol -> SourcePos
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 Symbol -> HashSet Symbol -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`S.member` HashSet Symbol
wiredInNames
wiredInNames :: S.HashSet F.Symbol
wiredInNames :: HashSet Symbol
wiredInNames = [Symbol] -> HashSet Symbol
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 = (Symbol -> Bool) -> [Symbol] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Symbol -> Symbol -> Bool
`F.isPrefixOfSym` LocSymbol -> Symbol
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)(Symbol, Sort) -> [(Symbol, Sort)] -> [(Symbol, Sort)]
forall a. a -> [a] -> [a]
:[(Int -> Symbol
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" (ForAllTyBinder -> Type -> Type
Ghc.ForAllTy (Var -> ForAllTyFlag -> ForAllTyBinder
forall var argf. var -> argf -> VarBndr var argf
Ghc.Bndr Var
dictionaryTyVar ForAllTyFlag
Required) (Type -> Type) -> Type -> Type
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 = [(Var, Expr Var)] -> Bind Var
forall b. [(b, Expr b)] -> Bind b
Rec [(Var
v, Var -> Expr Var -> Expr Var
forall b. b -> Expr b -> Expr b
Lam Var
a (Expr Var -> Expr Var) -> Expr Var -> Expr Var
forall a b. (a -> b) -> a -> b
$ Expr Var -> Expr Var -> Expr Var
forall b. Expr b -> Expr b -> Expr b
App (Var -> Expr Var
forall b. Var -> Expr b
Var Var
v) (Type -> Expr Var
forall b. Type -> Expr b
Type (Type -> Expr Var) -> Type -> Expr Var
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 = ([TyConP], [Located DataConP]) -> [TyConP]
forall a b. (a, b) -> a
fst ([TyConP], [Located DataConP])
wiredTyDataCons
wiredDataCons :: [Located DataConP]
wiredDataCons :: [Located DataConP]
wiredDataCons = ([TyConP], [Located DataConP]) -> [Located DataConP]
forall a b. (a, b) -> b
snd ([TyConP], [Located DataConP])
wiredTyDataCons
wiredTyDataCons :: ([TyConP] , [Located DataConP])
wiredTyDataCons :: ([TyConP], [Located DataConP])
wiredTyDataCons = ([[TyConP]] -> [TyConP]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[TyConP]]
tcs, DataConP -> Located DataConP
forall a. a -> Located a
dummyLoc (DataConP -> Located DataConP) -> [DataConP] -> [Located DataConP]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [[DataConP]] -> [DataConP]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[DataConP]]
dcs)
where
([[TyConP]]
tcs, [[DataConP]]
dcs) = [([TyConP], [DataConP])] -> ([[TyConP]], [[DataConP]])
forall a b. [(a, b)] -> ([a], [b])
unzip ([([TyConP], [DataConP])] -> ([[TyConP]], [[DataConP]]))
-> [([TyConP], [DataConP])] -> ([[TyConP]], [[DataConP]])
forall a b. (a -> b) -> a -> b
$ ([TyConP], [DataConP])
listTyDataCons ([TyConP], [DataConP])
-> [([TyConP], [DataConP])] -> [([TyConP], [DataConP])]
forall a. a -> [a] -> [a]
: (Int -> ([TyConP], [DataConP]))
-> [Int] -> [([TyConP], [DataConP])]
forall a b. (a -> b) -> [a] -> [b]
map Int -> ([TyConP], [DataConP])
tupleTyDataCons [Int
2..Int
maxArity]
charDataCon :: Located DataConP
charDataCon :: Located DataConP
charDataCon = DataConP -> Located DataConP
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",SpecType
forall {tv}. RType RTyCon tv RReft
lt)] SpecType
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 = TyCon
-> [RType RTyCon tv RReft]
-> [RTProp RTyCon tv RReft]
-> RReft
-> RType RTyCon tv RReft
forall tv r.
TyCon
-> [RType RTyCon tv r]
-> [RTProp RTyCon tv r]
-> r
-> RType RTyCon tv r
rApp TyCon
c [] [] RReft
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] (SizeFun -> Maybe SizeFun
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 = Var -> RSort
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 = Symbol
-> PVKind RSort -> Symbol -> [(RSort, Symbol, Expr)] -> PVar RSort
forall t.
Symbol -> PVKind t -> Symbol -> [(t, Symbol, Expr)] -> PVar t
PV Symbol
"p" (RSort -> PVKind RSort
forall t. t -> PVKind t
PVProp RSort
t) (Maybe Integer -> Symbol
F.vv Maybe Integer
forall a. Maybe a
Nothing) [(RSort
t, Symbol
fld, Symbol -> Expr
F.EVar Symbol
fld)]
px :: RReft
px = PVar RSort -> RReft
forall t. PVar t -> RReft
pdVarReft (PVar RSort -> RReft) -> PVar RSort -> RReft
forall a b. (a -> b) -> a -> b
$ Symbol
-> PVKind RSort -> Symbol -> [(RSort, Symbol, Expr)] -> PVar RSort
forall t.
Symbol -> PVKind t -> Symbol -> [(t, Symbol, Expr)] -> PVar t
PV Symbol
"p" (RSort -> PVKind RSort
forall t. t -> PVKind t
PVProp RSort
t) (Maybe Integer -> Symbol
F.vv Maybe Integer
forall a. Maybe a
Nothing) [(RSort
t, Symbol
fld, Symbol -> Expr
F.EVar Symbol
xHead)]
lt :: SpecType
lt = TyCon
-> [SpecType] -> [RTProp RTyCon RTyVar RReft] -> RReft -> SpecType
forall tv r.
TyCon
-> [RType RTyCon tv r]
-> [RTProp RTyCon tv r]
-> r
-> RType RTyCon tv r
rApp TyCon
c [SpecType
forall {c}. RType c RTyVar RReft
xt] [[(Symbol, RSort)] -> RReft -> RTProp RTyCon RTyVar RReft
forall τ r c tv. [(Symbol, τ)] -> r -> Ref τ (RType c tv r)
rPropP [] (RReft -> RTProp RTyCon RTyVar RReft)
-> RReft -> RTProp RTyCon RTyVar RReft
forall a b. (a -> b) -> a -> b
$ PVar RSort -> RReft
forall t. PVar t -> RReft
pdVarReft PVar RSort
p] RReft
forall a. Monoid a => a
mempty
xt :: RType c RTyVar RReft
xt = Var -> RType c RTyVar RReft
forall r c. Monoid r => Var -> RType c RTyVar r
rVar Var
tyv
xst :: SpecType
xst = TyCon
-> [SpecType] -> [RTProp RTyCon RTyVar RReft] -> RReft -> SpecType
forall tv r.
TyCon
-> [RType RTyCon tv r]
-> [RTProp RTyCon tv r]
-> r
-> RType RTyCon tv r
rApp TyCon
c [RTyVar -> RReft -> SpecType
forall c tv r. tv -> r -> RType c tv r
RVar (Var -> RTyVar
RTV Var
tyv) RReft
px] [[(Symbol, RSort)] -> RReft -> RTProp RTyCon RTyVar RReft
forall τ r c tv. [(Symbol, τ)] -> r -> Ref τ (RType c tv r)
rPropP [] (RReft -> RTProp RTyCon RTyVar RReft)
-> RReft -> RTProp RTyCon RTyVar RReft
forall a b. (a -> b) -> a -> b
$ PVar RSort -> RReft
forall t. PVar t -> RReft
pdVarReft PVar RSort
p] RReft
forall a. Monoid a => a
mempty
cargs :: [(Symbol, SpecType)]
cargs = [(Symbol
xTail, SpecType
xst), (Symbol
xHead, SpecType
forall {c}. RType c RTyVar RReft
xt)]
fsize :: SizeFun
fsize = LocSymbol -> SizeFun
SymSizeFun (Symbol -> LocSymbol
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 (Var -> RTyVar) -> [Var] -> [RTyVar]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Var]
tyvs) [PVar RSort]
ps VarianceInfo
tyvarinfo VarianceInfo
pdvarinfo Maybe SizeFun
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 (Var -> RTyVar) -> [Var] -> [RTyVar]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Var]
tyvs) [PVar RSort]
ps [] [(Symbol, SpecType)]
forall {c}. [(Symbol, RType c RTyVar RReft)]
cargs SpecType
lt Bool
False Symbol
wiredInName SourcePos
l0])
where
tyvarinfo :: VarianceInfo
tyvarinfo = Int -> Variance -> VarianceInfo
forall a. Int -> a -> [a]
replicate Int
n Variance
Covariant
pdvarinfo :: VarianceInfo
pdvarinfo = Int -> Variance -> VarianceInfo
forall a. Int -> a -> [a]
replicate (Int
nInt -> Int -> Int
forall 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) = (Var -> RSort
forall r c. Monoid r => Var -> RType c RTyVar r
rVar (Var -> RSort) -> [Var] -> [RSort]
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" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show Int
n)
ps :: [PVar RSort]
ps = [Symbol] -> [RSort] -> [(Symbol, Expr)] -> [PVar RSort]
forall t. [Symbol] -> [t] -> [(Symbol, Expr)] -> [PVar t]
mkps [Symbol]
pnames (RSort
taRSort -> [RSort] -> [RSort]
forall a. a -> [a] -> [a]
:[RSort]
ts) ((Symbol
fld, Symbol -> Expr
F.EVar Symbol
fld) (Symbol, Expr) -> [(Symbol, Expr)] -> [(Symbol, Expr)]
forall a. a -> [a] -> [a]
: [Symbol] -> [Expr] -> [(Symbol, Expr)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
flds (Symbol -> Expr
F.EVar (Symbol -> Expr) -> [Symbol] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol]
flds))
ups :: [UsedPVar]
ups = PVar RSort -> UsedPVar
forall t. PVar t -> UsedPVar
uPVar (PVar RSort -> UsedPVar) -> [PVar RSort] -> [UsedPVar]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [PVar RSort]
ps
pxs :: [PVar RSort]
pxs = [Symbol] -> [RSort] -> [(Symbol, Expr)] -> [PVar RSort]
forall t. [Symbol] -> [t] -> [(Symbol, Expr)] -> [PVar t]
mkps [Symbol]
pnames (RSort
taRSort -> [RSort] -> [RSort]
forall a. a -> [a] -> [a]
:[RSort]
ts) ((Symbol
fld, Symbol -> Expr
F.EVar Symbol
x1) (Symbol, Expr) -> [(Symbol, Expr)] -> [(Symbol, Expr)]
forall a. a -> [a] -> [a]
: [Symbol] -> [Expr] -> [(Symbol, Expr)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
flds (Symbol -> Expr
F.EVar (Symbol -> Expr) -> [Symbol] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol]
xs))
lt :: SpecType
lt = TyCon
-> [SpecType] -> [RTProp RTyCon RTyVar RReft] -> RReft -> SpecType
forall tv r.
TyCon
-> [RType RTyCon tv r]
-> [RTProp RTyCon tv r]
-> r
-> RType RTyCon tv r
rApp TyCon
c (Var -> SpecType
forall r c. Monoid r => Var -> RType c RTyVar r
rVar (Var -> SpecType) -> [Var] -> [SpecType]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Var]
tyvs) ([(Symbol, RSort)] -> RReft -> RTProp RTyCon RTyVar RReft
forall τ r c tv. [(Symbol, τ)] -> r -> Ref τ (RType c tv r)
rPropP [] (RReft -> RTProp RTyCon RTyVar RReft)
-> (UsedPVar -> RReft) -> UsedPVar -> RTProp RTyCon RTyVar RReft
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UsedPVar -> RReft
forall t. PVar t -> RReft
pdVarReft (UsedPVar -> RTProp RTyCon RTyVar RReft)
-> [UsedPVar] -> [RTProp RTyCon RTyVar RReft]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [UsedPVar]
ups) RReft
forall a. Monoid a => a
mempty
xts :: [RType c RTyVar RReft]
xts = (Var -> PVar RSort -> RType c RTyVar RReft)
-> [Var] -> [PVar RSort] -> [RType c RTyVar RReft]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\Var
v PVar RSort
p -> RTyVar -> RReft -> RType c RTyVar RReft
forall c tv r. tv -> r -> RType c tv r
RVar (Var -> RTyVar
RTV Var
v) (PVar RSort -> RReft
forall t. PVar t -> RReft
pdVarReft PVar RSort
p)) [Var]
tvs [PVar RSort]
pxs
cargs :: [(Symbol, RType c RTyVar RReft)]
cargs = [(Symbol, RType c RTyVar RReft)]
-> [(Symbol, RType c RTyVar RReft)]
forall a. [a] -> [a]
reverse ([(Symbol, RType c RTyVar RReft)]
-> [(Symbol, RType c RTyVar RReft)])
-> [(Symbol, RType c RTyVar RReft)]
-> [(Symbol, RType c RTyVar RReft)]
forall a b. (a -> b) -> a -> b
$ (Symbol
x1, Var -> RType c RTyVar RReft
forall r c. Monoid r => Var -> RType c RTyVar r
rVar Var
tv) (Symbol, RType c RTyVar RReft)
-> [(Symbol, RType c RTyVar RReft)]
-> [(Symbol, RType c RTyVar RReft)]
forall a. a -> [a] -> [a]
: [Symbol]
-> [RType c RTyVar RReft] -> [(Symbol, RType c RTyVar RReft)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
xs [RType c RTyVar RReft]
forall {c}. [RType c RTyVar RReft]
xts
pnames :: [Symbol]
pnames = [Char] -> [Symbol]
mks_ [Char]
"p"
mks :: [Char] -> [Symbol]
mks [Char]
x = (\Int
i -> [Char] -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol ([Char]
x[Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show Int
i)) (Int -> Symbol) -> [Int] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Int
1..Int
n]
mks_ :: [Char] -> [Symbol]
mks_ [Char]
x = (\Int
i -> [Char] -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol ([Char]
x[Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show Int
i)) (Int -> Symbol) -> [Int] -> [Symbol]
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) = [PVar t] -> [PVar t]
forall a. [a] -> [a]
reverse ([PVar t] -> [PVar t]) -> [PVar t] -> [PVar t]
forall a b. (a -> b) -> a -> b
$ [Symbol]
-> [t]
-> [(Symbol, Expr)]
-> [(t, Symbol, Expr)]
-> [PVar t]
-> [PVar t]
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)]
_ = Maybe SrcSpan -> [Char] -> [PVar t]
forall a. Maybe SrcSpan -> [Char] -> a
panic Maybe SrcSpan
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 = [Symbol]
-> [t]
-> [(Symbol, Expr)]
-> [(t, Symbol, Expr)]
-> [PVar t]
-> [PVar t]
forall t.
[Symbol]
-> [t]
-> [(Symbol, Expr)]
-> [(t, Symbol, Expr)]
-> [PVar t]
-> [PVar t]
mkps_ [Symbol]
ns [t]
ts [(Symbol, Expr)]
xs ((t, Symbol, Expr)
a(t, Symbol, Expr) -> [(t, Symbol, Expr)] -> [(t, Symbol, Expr)]
forall a. a -> [a] -> [a]
:[(t, Symbol, Expr)]
args) (PVar t
pPVar t -> [PVar t] -> [PVar t]
forall a. a -> [a] -> [a]
:[PVar t]
ps)
where
p :: PVar t
p = Symbol -> PVKind t -> Symbol -> [(t, Symbol, Expr)] -> PVar t
forall t.
Symbol -> PVKind t -> Symbol -> [(t, Symbol, Expr)] -> PVar t
PV Symbol
n (t -> PVKind t
forall t. t -> PVKind t
PVProp t
t) (Maybe Integer -> Symbol
F.vv Maybe Integer
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]
_ = Maybe SrcSpan -> [Char] -> [PVar t]
forall a. Maybe SrcSpan -> [Char] -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing [Char]
"Bare : mkps_"
isDerivedInstance :: Ghc.ClsInst -> Bool
isDerivedInstance :: ClsInst -> Bool
isDerivedInstance ClsInst
i = [Char] -> Bool -> Bool
forall a. PPrint a => [Char] -> a -> a
F.notracepp ([Char]
"IS-DERIVED: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Symbol -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp Symbol
classSym)
(Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Symbol -> HashSet Symbol -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
S.member Symbol
classSym HashSet Symbol
derivingClasses
where
classSym :: Symbol
classSym = Class -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol (Class -> Symbol) -> (ClsInst -> Class) -> ClsInst -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ClsInst -> Class
Ghc.is_cls (ClsInst -> Symbol) -> ClsInst -> Symbol
forall a b. (a -> b) -> a -> b
$ ClsInst
i
derivingClasses :: S.HashSet F.Symbol
derivingClasses :: HashSet Symbol
derivingClasses = [Symbol] -> HashSet Symbol
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"
]