{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TupleSections #-}
module Language.Haskell.Liquid.Bare.DataType
( dataConMap
, makeDataConChecker
, makeDataConSelector
, addClassEmbeds
, makeDataDecls
, makeConTypes
, makeRecordSelectorSigs
, meetDataConSpec
, dataDeclSize
) where
import qualified Control.Exception as Ex
import Control.Monad (forM, unless)
import Control.Monad.Reader
import qualified Data.List as L
import qualified Data.HashMap.Strict as M
import qualified Data.HashSet as S
import qualified Data.Maybe as Mb
import qualified Language.Fixpoint.Types as F
import qualified Language.Haskell.Liquid.GHC.Misc as GM
import qualified Liquid.GHC.API as Ghc
import Language.Haskell.Liquid.Types.PredType (dataConPSpecType)
import qualified Language.Haskell.Liquid.Types.RefType as RT
import Language.Haskell.Liquid.Types.Types
import Language.Haskell.Liquid.Types.Meet
import qualified Language.Fixpoint.Misc as Misc
import qualified Language.Haskell.Liquid.Misc as Misc
import Language.Haskell.Liquid.Types.Variance
import Language.Haskell.Liquid.WiredIn
import Language.Haskell.Liquid.Types.Names (selfSymbol)
import qualified Language.Haskell.Liquid.Measure as Ms
import qualified Language.Haskell.Liquid.Bare.Types as Bare
import qualified Language.Haskell.Liquid.Bare.Resolve as Bare
import Text.Printf (printf)
import Text.PrettyPrint ((<+>))
dataConMap :: [F.DataDecl] -> Bare.DataConMap
dataConMap :: [DataDecl] -> DataConMap
dataConMap [DataDecl]
ds = [((Symbol, Int), Symbol)] -> DataConMap
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList ([((Symbol, Int), Symbol)] -> DataConMap)
-> [((Symbol, Int), Symbol)] -> DataConMap
forall a b. (a -> b) -> a -> b
$ do
DataDecl
d <- [DataDecl]
ds
DataCtor
c <- DataDecl -> [DataCtor]
F.ddCtors DataDecl
d
let fs :: [Symbol]
fs = DataField -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol (DataField -> Symbol) -> [DataField] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DataCtor -> [DataField]
F.dcFields DataCtor
c
[(Symbol, Int)] -> [Symbol] -> [((Symbol, Int), Symbol)]
forall a b. [a] -> [b] -> [(a, b)]
zip ((DataCtor -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol DataCtor
c,) (Int -> (Symbol, Int)) -> [Int] -> [(Symbol, Int)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Int
1..]) [Symbol]
fs
makeDataConChecker :: Ghc.DataCon -> F.Symbol
makeDataConChecker :: DataCon -> Symbol
makeDataConChecker = Symbol -> Symbol
F.testSymbol (Symbol -> Symbol) -> (DataCon -> Symbol) -> DataCon -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataCon -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol
makeDataConSelector :: Maybe Bare.DataConMap -> Ghc.DataCon -> Int -> F.Symbol
makeDataConSelector :: Maybe DataConMap -> DataCon -> Int -> Symbol
makeDataConSelector Maybe DataConMap
dmMb DataCon
d Int
i = Symbol -> (Symbol, Int) -> DataConMap -> Symbol
forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
M.lookupDefault Symbol
def (DataCon -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol DataCon
d, Int
i) DataConMap
dm
where
dm :: DataConMap
dm = DataConMap -> Maybe DataConMap -> DataConMap
forall a. a -> Maybe a -> a
Mb.fromMaybe DataConMap
forall k v. HashMap k v
M.empty Maybe DataConMap
dmMb
def :: Symbol
def = DataCon -> Int -> Symbol
makeDataConSelector' DataCon
d Int
i
makeDataConSelector' :: Ghc.DataCon -> Int -> F.Symbol
makeDataConSelector' :: DataCon -> Int -> Symbol
makeDataConSelector' DataCon
d Int
i
= [Char] -> Symbol -> Maybe Int -> Symbol
symbolMeasure [Char]
"$select" (DataCon -> Symbol
dcSymbol DataCon
d) (Int -> Maybe Int
forall a. a -> Maybe a
Just Int
i)
dcSymbol :: Ghc.DataCon -> F.Symbol
dcSymbol :: DataCon -> Symbol
dcSymbol = Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol (Var -> Symbol) -> (DataCon -> Var) -> DataCon -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataCon -> Var
Ghc.dataConWorkId
symbolMeasure :: String -> F.Symbol -> Maybe Int -> F.Symbol
symbolMeasure :: [Char] -> Symbol -> Maybe Int -> Symbol
symbolMeasure [Char]
f Symbol
d Maybe Int
iMb = (Symbol -> Symbol -> Symbol) -> [Symbol] -> Symbol
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 Symbol -> Symbol -> Symbol
F.suffixSymbol (Symbol
dcPrefix Symbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
: [Char] -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol [Char]
f Symbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
: Symbol
d Symbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
: [Symbol]
rest)
where
rest :: [Symbol]
rest = [Symbol] -> (Int -> [Symbol]) -> Maybe Int -> [Symbol]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] (Symbol -> [Symbol]
forall t. t -> [t]
Misc.single (Symbol -> [Symbol]) -> (Int -> Symbol) -> Int -> [Symbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol ([Char] -> Symbol) -> (Int -> [Char]) -> Int -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> [Char]
forall a. Show a => a -> [Char]
show) Maybe Int
iMb
addClassEmbeds :: Maybe [Ghc.ClsInst] -> [Ghc.TyCon] -> F.TCEmb Ghc.TyCon
-> F.TCEmb Ghc.TyCon
addClassEmbeds :: Maybe [ClsInst] -> [TyCon] -> TCEmb TyCon -> TCEmb TyCon
addClassEmbeds Maybe [ClsInst]
instenv [TyCon]
fiTcs = [TyCon] -> TCEmb TyCon -> TCEmb TyCon
makeFamInstEmbeds [TyCon]
fiTcs (TCEmb TyCon -> TCEmb TyCon)
-> (TCEmb TyCon -> TCEmb TyCon) -> TCEmb TyCon -> TCEmb TyCon
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe [ClsInst] -> TCEmb TyCon -> TCEmb TyCon
makeNumEmbeds Maybe [ClsInst]
instenv
makeFamInstEmbeds :: [Ghc.TyCon] -> F.TCEmb Ghc.TyCon -> F.TCEmb Ghc.TyCon
makeFamInstEmbeds :: [TyCon] -> TCEmb TyCon -> TCEmb TyCon
makeFamInstEmbeds [TyCon]
cs0 TCEmb TyCon
embeds = (TCEmb TyCon -> (TyCon, Sort) -> TCEmb TyCon)
-> TCEmb TyCon -> [(TyCon, Sort)] -> TCEmb TyCon
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' TCEmb TyCon -> (TyCon, Sort) -> TCEmb TyCon
forall {a}. Hashable a => TCEmb a -> (a, Sort) -> TCEmb a
embed TCEmb TyCon
embeds [(TyCon, Sort)]
famInstSorts
where
famInstSorts :: [(TyCon, Sort)]
famInstSorts = [Char] -> [(TyCon, Sort)] -> [(TyCon, Sort)]
forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"famInstTcs"
[ (TyCon
c, TCEmb TyCon -> Type -> Sort
RT.typeSort TCEmb TyCon
embeds Type
ty)
| TyCon
c <- [TyCon]
cs
, Type
ty <- Maybe Type -> [Type]
forall a. Maybe a -> [a]
Mb.maybeToList (TyCon -> Maybe Type
RT.famInstTyConType TyCon
c) ]
embed :: TCEmb a -> (a, Sort) -> TCEmb a
embed TCEmb a
embs (a
c, Sort
t) = a -> Sort -> TCArgs -> TCEmb a -> TCEmb a
forall a.
(Eq a, Hashable a) =>
a -> Sort -> TCArgs -> TCEmb a -> TCEmb a
F.tceInsert a
c Sort
t TCArgs
F.NoArgs TCEmb a
embs
cs :: [TyCon]
cs = [Char] -> [TyCon] -> [TyCon]
forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"famInstTcs-all" [TyCon]
cs0
makeNumEmbeds :: Maybe [Ghc.ClsInst] -> F.TCEmb Ghc.TyCon -> F.TCEmb Ghc.TyCon
makeNumEmbeds :: Maybe [ClsInst] -> TCEmb TyCon -> TCEmb TyCon
makeNumEmbeds Maybe [ClsInst]
Nothing TCEmb TyCon
x = TCEmb TyCon
x
makeNumEmbeds (Just [ClsInst]
is) TCEmb TyCon
x = (TCEmb TyCon -> ClsInst -> TCEmb TyCon)
-> TCEmb TyCon -> [ClsInst] -> TCEmb TyCon
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' TCEmb TyCon -> ClsInst -> TCEmb TyCon
makeNumericInfoOne TCEmb TyCon
x [ClsInst]
is
makeNumericInfoOne :: F.TCEmb Ghc.TyCon -> Ghc.ClsInst -> F.TCEmb Ghc.TyCon
makeNumericInfoOne :: TCEmb TyCon -> ClsInst -> TCEmb TyCon
makeNumericInfoOne TCEmb TyCon
m ClsInst
is
| TyCon -> Bool
forall c. TyConable c => c -> Bool
isFracCls TyCon
cls, Just TyCon
tc <- ClsInst -> Maybe TyCon
instanceTyCon ClsInst
is
= (Sort -> Sort -> Sort)
-> TyCon -> Sort -> TCArgs -> TCEmb TyCon -> TCEmb TyCon
forall a.
(Eq a, Hashable a) =>
(Sort -> Sort -> Sort) -> a -> Sort -> TCArgs -> TCEmb a -> TCEmb a
F.tceInsertWith ((Sort -> Sort -> Sort) -> Sort -> Sort -> Sort
forall a b c. (a -> b -> c) -> b -> a -> c
flip Sort -> Sort -> Sort
mappendSortFTC) TyCon
tc (TyCon -> Bool -> Bool -> Sort
ftc TyCon
tc Bool
True Bool
True) TCArgs
F.NoArgs TCEmb TyCon
m
| TyCon -> Bool
forall c. TyConable c => c -> Bool
isNumCls TyCon
cls, Just TyCon
tc <- ClsInst -> Maybe TyCon
instanceTyCon ClsInst
is
= (Sort -> Sort -> Sort)
-> TyCon -> Sort -> TCArgs -> TCEmb TyCon -> TCEmb TyCon
forall a.
(Eq a, Hashable a) =>
(Sort -> Sort -> Sort) -> a -> Sort -> TCArgs -> TCEmb a -> TCEmb a
F.tceInsertWith ((Sort -> Sort -> Sort) -> Sort -> Sort -> Sort
forall a b c. (a -> b -> c) -> b -> a -> c
flip Sort -> Sort -> Sort
mappendSortFTC) TyCon
tc (TyCon -> Bool -> Bool -> Sort
ftc TyCon
tc Bool
True Bool
False) TCArgs
F.NoArgs TCEmb TyCon
m
| Bool
otherwise
= TCEmb TyCon
m
where
cls :: TyCon
cls = Class -> TyCon
Ghc.classTyCon (ClsInst -> Class
Ghc.is_cls ClsInst
is)
ftc :: TyCon -> Bool -> Bool -> Sort
ftc TyCon
c Bool
f1 Bool
f2 = FTycon -> Sort
F.FTC (Located Symbol -> Bool -> Bool -> FTycon
F.symbolNumInfoFTyCon (Symbol -> Located Symbol
forall a. a -> Located a
dummyLoc (Symbol -> Located Symbol) -> Symbol -> Located Symbol
forall a b. (a -> b) -> a -> b
$ TyCon -> Symbol
RT.tyConName TyCon
c) Bool
f1 Bool
f2)
mappendSortFTC :: F.Sort -> F.Sort -> F.Sort
mappendSortFTC :: Sort -> Sort -> Sort
mappendSortFTC (F.FTC FTycon
x) (F.FTC FTycon
y) = FTycon -> Sort
F.FTC (FTycon -> FTycon -> FTycon
F.mappendFTC FTycon
x FTycon
y)
mappendSortFTC Sort
s (F.FTC FTycon
_) = Sort
s
mappendSortFTC (F.FTC FTycon
_) Sort
s = Sort
s
mappendSortFTC Sort
s1 Sort
s2 = Maybe SrcSpan -> [Char] -> Sort
forall a. Maybe SrcSpan -> [Char] -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing ([Char]
"mappendSortFTC: s1 = " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Sort -> [Char]
forall a. PPrint a => a -> [Char]
showpp Sort
s1 [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" s2 = " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Sort -> [Char]
forall a. PPrint a => a -> [Char]
showpp Sort
s2)
instanceTyCon :: Ghc.ClsInst -> Maybe Ghc.TyCon
instanceTyCon :: ClsInst -> Maybe TyCon
instanceTyCon = [Type] -> Maybe TyCon
go ([Type] -> Maybe TyCon)
-> (ClsInst -> [Type]) -> ClsInst -> Maybe TyCon
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ClsInst -> [Type]
Ghc.is_tys
where
go :: [Type] -> Maybe TyCon
go [Ghc.TyConApp TyCon
c [Type]
_] = TyCon -> Maybe TyCon
forall a. a -> Maybe a
Just TyCon
c
go [Type]
_ = Maybe TyCon
forall a. Maybe a
Nothing
type DataPropDecl = (DataDecl, Maybe SpecType)
makeDataDecls :: Config -> F.TCEmb Ghc.TyCon -> ModName
-> [(ModName, Ghc.TyCon, DataPropDecl)]
-> [Located DataConP]
-> (Diagnostics, [F.DataDecl])
makeDataDecls :: Config
-> TCEmb TyCon
-> ModName
-> [(ModName, TyCon, DataPropDecl)]
-> [Located DataConP]
-> (Diagnostics, [DataDecl])
makeDataDecls Config
cfg TCEmb TyCon
tce ModName
name [(ModName, TyCon, DataPropDecl)]
tds [Located DataConP]
ds
| Bool
makeDecls = ([Warning] -> [Error] -> Diagnostics
mkDiagnostics [Warning]
warns [], [DataDecl]
okDecs)
| Bool
otherwise = (Diagnostics
forall a. Monoid a => a
mempty, [])
where
makeDecls :: Bool
makeDecls = Config -> Bool
forall t. HasConfig t => t -> Bool
exactDCFlag Config
cfg Bool -> Bool -> Bool
&& Bool -> Bool
not (Config -> Bool
noADT Config
cfg)
warns :: [Warning]
warns = (DataDecl -> Warning
forall a. (Loc a, Symbolic a) => a -> Warning
mkWarnDecl (DataDecl -> Warning)
-> ((TyCon, (DataPropDecl, [(DataCon, DataConP)])) -> DataDecl)
-> (TyCon, (DataPropDecl, [(DataCon, DataConP)]))
-> Warning
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataPropDecl -> DataDecl
forall a b. (a, b) -> a
fst (DataPropDecl -> DataDecl)
-> ((TyCon, (DataPropDecl, [(DataCon, DataConP)])) -> DataPropDecl)
-> (TyCon, (DataPropDecl, [(DataCon, DataConP)]))
-> DataDecl
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (DataPropDecl, [(DataCon, DataConP)]) -> DataPropDecl
forall a b. (a, b) -> a
fst ((DataPropDecl, [(DataCon, DataConP)]) -> DataPropDecl)
-> ((TyCon, (DataPropDecl, [(DataCon, DataConP)]))
-> (DataPropDecl, [(DataCon, DataConP)]))
-> (TyCon, (DataPropDecl, [(DataCon, DataConP)]))
-> DataPropDecl
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TyCon, (DataPropDecl, [(DataCon, DataConP)]))
-> (DataPropDecl, [(DataCon, DataConP)])
forall a b. (a, b) -> b
snd ((TyCon, (DataPropDecl, [(DataCon, DataConP)])) -> Warning)
-> [(TyCon, (DataPropDecl, [(DataCon, DataConP)]))] -> [Warning]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(TyCon, (DataPropDecl, [(DataCon, DataConP)]))]
badTcs) [Warning] -> [Warning] -> [Warning]
forall a. [a] -> [a] -> [a]
++ (DataDecl -> Warning
forall a. (Loc a, Symbolic a) => a -> Warning
mkWarnDecl (DataDecl -> Warning) -> [DataDecl] -> [Warning]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [DataDecl]
badDecs)
tds' :: [(TyCon, (ModName, DataPropDecl))]
tds' = ModName
-> [(ModName, TyCon, DataPropDecl)]
-> [(TyCon, (ModName, DataPropDecl))]
resolveTyCons ModName
name [(ModName, TyCon, DataPropDecl)]
tds
tcDds :: [(TyCon, (DataPropDecl, [(DataCon, DataConP)]))]
tcDds = ((TyCon, (DataPropDecl, [(DataCon, DataConP)])) -> Bool)
-> [(TyCon, (DataPropDecl, [(DataCon, DataConP)]))]
-> [(TyCon, (DataPropDecl, [(DataCon, DataConP)]))]
forall a. (a -> Bool) -> [a] -> [a]
filter ((TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
/= TyCon
Ghc.listTyCon) (TyCon -> Bool)
-> ((TyCon, (DataPropDecl, [(DataCon, DataConP)])) -> TyCon)
-> (TyCon, (DataPropDecl, [(DataCon, DataConP)]))
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TyCon, (DataPropDecl, [(DataCon, DataConP)])) -> TyCon
forall a b. (a, b) -> a
fst)
([(TyCon, (DataPropDecl, [(DataCon, DataConP)]))]
-> [(TyCon, (DataPropDecl, [(DataCon, DataConP)]))])
-> [(TyCon, (DataPropDecl, [(DataCon, DataConP)]))]
-> [(TyCon, (DataPropDecl, [(DataCon, DataConP)]))]
forall a b. (a -> b) -> a -> b
$ [(TyCon, (ModName, DataPropDecl))]
-> [Located DataConP]
-> [(TyCon, (DataPropDecl, [(DataCon, DataConP)]))]
groupDataCons [(TyCon, (ModName, DataPropDecl))]
tds' [Located DataConP]
ds
([(TyCon, (DataPropDecl, [(DataCon, DataConP)]))]
okTcs, [(TyCon, (DataPropDecl, [(DataCon, DataConP)]))]
badTcs) = ((TyCon, (DataPropDecl, [(DataCon, DataConP)])) -> Bool)
-> [(TyCon, (DataPropDecl, [(DataCon, DataConP)]))]
-> ([(TyCon, (DataPropDecl, [(DataCon, DataConP)]))],
[(TyCon, (DataPropDecl, [(DataCon, DataConP)]))])
forall a. (a -> Bool) -> [a] -> ([a], [a])
L.partition (TyCon, (DataPropDecl, [(DataCon, DataConP)])) -> Bool
forall a b c. (a, (b, [(DataCon, c)])) -> Bool
isVanillaTc [(TyCon, (DataPropDecl, [(DataCon, DataConP)]))]
tcDds
decs :: [DataDecl]
decs = [ TCEmb TyCon
-> TyCon -> DataPropDecl -> [(DataCon, DataConP)] -> DataDecl
makeFDataDecls TCEmb TyCon
tce TyCon
tc DataPropDecl
dd [(DataCon, DataConP)]
ctors | (TyCon
tc, (DataPropDecl
dd, [(DataCon, DataConP)]
ctors)) <- [(TyCon, (DataPropDecl, [(DataCon, DataConP)]))]
okTcs]
([DataDecl]
okDecs,[DataDecl]
badDecs) = [DataDecl] -> ([DataDecl], [DataDecl])
checkRegularData [DataDecl]
decs
isVanillaTc :: (a, (b, [(Ghc.DataCon, c)])) -> Bool
isVanillaTc :: forall a b c. (a, (b, [(DataCon, c)])) -> Bool
isVanillaTc (a
_, (b
_, [(DataCon, c)]
ctors)) = ((DataCon, c) -> Bool) -> [(DataCon, c)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (DataCon -> Bool
Ghc.isVanillaDataCon (DataCon -> Bool)
-> ((DataCon, c) -> DataCon) -> (DataCon, c) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (DataCon, c) -> DataCon
forall a b. (a, b) -> a
fst) [(DataCon, c)]
ctors
checkRegularData :: [F.DataDecl] -> ([F.DataDecl], [F.DataDecl])
checkRegularData :: [DataDecl] -> ([DataDecl], [DataDecl])
checkRegularData [DataDecl]
ds = ([DataDecl]
oks, [DataDecl]
badDs)
where
badDs :: [DataDecl]
badDs = [DataDecl] -> [DataDecl]
F.checkRegular [DataDecl]
ds
badSyms :: HashSet Symbol
badSyms = [Symbol] -> HashSet Symbol
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ([Symbol] -> HashSet Symbol)
-> ([DataDecl] -> [Symbol]) -> [DataDecl] -> HashSet Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (DataDecl -> Symbol) -> [DataDecl] -> [Symbol]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DataDecl -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol ([DataDecl] -> HashSet Symbol) -> [DataDecl] -> HashSet Symbol
forall a b. (a -> b) -> a -> b
$ [DataDecl]
badDs
oks :: [DataDecl]
oks = [ DataDecl
d | DataDecl
d <- [DataDecl]
ds, Bool -> Bool
not (Symbol -> HashSet Symbol -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
S.member (DataDecl -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol DataDecl
d) HashSet Symbol
badSyms) ]
mkWarnDecl :: (F.Loc a, F.Symbolic a) => a -> Warning
mkWarnDecl :: forall a. (Loc a, Symbolic a) => a -> Warning
mkWarnDecl a
d = SrcSpan -> Doc -> Warning
mkWarning (a -> SrcSpan
forall a. Loc a => a -> SrcSpan
GM.fSrcSpan a
d) (Doc
"Non-regular data declaration" Doc -> Doc -> Doc
<+> Symbol -> Doc
forall a. PPrint a => a -> Doc
pprint (a -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol a
d))
resolveTyCons :: ModName -> [(ModName, Ghc.TyCon, DataPropDecl)]
-> [(Ghc.TyCon, (ModName, DataPropDecl))]
resolveTyCons :: ModName
-> [(ModName, TyCon, DataPropDecl)]
-> [(TyCon, (ModName, DataPropDecl))]
resolveTyCons ModName
mn [(ModName, TyCon, DataPropDecl)]
mtds = [(TyCon
tc, (ModName
m, DataPropDecl
d)) | (TyCon
tc, [(ModName, DataPropDecl)]
mds) <- HashMap TyCon [(ModName, DataPropDecl)]
-> [(TyCon, [(ModName, DataPropDecl)])]
forall k v. HashMap k v -> [(k, v)]
M.toList HashMap TyCon [(ModName, DataPropDecl)]
tcDecls
, (ModName
m, DataPropDecl
d) <- Maybe (ModName, DataPropDecl) -> [(ModName, DataPropDecl)]
forall a. Maybe a -> [a]
Mb.maybeToList (Maybe (ModName, DataPropDecl) -> [(ModName, DataPropDecl)])
-> Maybe (ModName, DataPropDecl) -> [(ModName, DataPropDecl)]
forall a b. (a -> b) -> a -> b
$ ModName
-> TyCon
-> [(ModName, DataPropDecl)]
-> Maybe (ModName, DataPropDecl)
resolveDecls ModName
mn TyCon
tc [(ModName, DataPropDecl)]
mds ]
where
tcDecls :: HashMap TyCon [(ModName, DataPropDecl)]
tcDecls = [(TyCon, (ModName, DataPropDecl))]
-> HashMap TyCon [(ModName, DataPropDecl)]
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k [v]
Misc.group [ (TyCon
tc, (ModName
m, DataPropDecl
d)) | (ModName
m, TyCon
tc, DataPropDecl
d) <- [(ModName, TyCon, DataPropDecl)]
mtds ]
resolveDecls :: ModName -> Ghc.TyCon -> Misc.ListNE (ModName, DataPropDecl)
-> Maybe (ModName, DataPropDecl)
resolveDecls :: ModName
-> TyCon
-> [(ModName, DataPropDecl)]
-> Maybe (ModName, DataPropDecl)
resolveDecls ModName
mName TyCon
tc [(ModName, DataPropDecl)]
mds = [Char]
-> Maybe (ModName, DataPropDecl) -> Maybe (ModName, DataPropDecl)
forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
msg (Maybe (ModName, DataPropDecl) -> Maybe (ModName, DataPropDecl))
-> Maybe (ModName, DataPropDecl) -> Maybe (ModName, DataPropDecl)
forall a b. (a -> b) -> a -> b
$
case ((ModName, DataPropDecl) -> Bool)
-> [(ModName, DataPropDecl)] -> [(ModName, DataPropDecl)]
forall a. (a -> Bool) -> [a] -> [a]
filter (ModName, DataPropDecl) -> Bool
forall {b}. (ModName, b) -> Bool
isHomeDef [(ModName, DataPropDecl)]
mds of
(ModName, DataPropDecl)
x:[(ModName, DataPropDecl)]
_ -> (ModName, DataPropDecl) -> Maybe (ModName, DataPropDecl)
forall a. a -> Maybe a
Just (ModName, DataPropDecl)
x
[(ModName, DataPropDecl)]
_ -> case ((ModName, DataPropDecl) -> Bool)
-> [(ModName, DataPropDecl)] -> [(ModName, DataPropDecl)]
forall a. (a -> Bool) -> [a] -> [a]
filter (ModName, DataPropDecl) -> Bool
forall {b}. (ModName, b) -> Bool
isLHAssumptionsDef [(ModName, DataPropDecl)]
mds of
[(ModName, DataPropDecl)
x] -> (ModName, DataPropDecl) -> Maybe (ModName, DataPropDecl)
forall a. a -> Maybe a
Just (ModName, DataPropDecl)
x
xs :: [(ModName, DataPropDecl)]
xs@((ModName, DataPropDecl)
_:[(ModName, DataPropDecl)]
_) -> [Char] -> Maybe (ModName, DataPropDecl)
forall a. HasCallStack => [Char] -> a
error ([Char] -> Maybe (ModName, DataPropDecl))
-> [Char] -> Maybe (ModName, DataPropDecl)
forall a b. (a -> b) -> a -> b
$
[Char]
"Multiple spec declarations of " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Symbol -> [Char]
forall a. Show a => a -> [Char]
show (TyCon -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol TyCon
tc) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
[Char]
" found in _LHAssumption modules: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [ModName] -> [Char]
forall a. Show a => a -> [Char]
show (((ModName, DataPropDecl) -> ModName)
-> [(ModName, DataPropDecl)] -> [ModName]
forall a b. (a -> b) -> [a] -> [b]
map (ModName, DataPropDecl) -> ModName
forall a b. (a, b) -> a
fst [(ModName, DataPropDecl)]
xs) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
[Char]
". Please, remove some of them."
[] -> ((ModName, DataPropDecl) -> Bool)
-> [(ModName, DataPropDecl)] -> Maybe (ModName, DataPropDecl)
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
L.find (ModName, DataPropDecl) -> Bool
forall {b}. (ModName, b) -> Bool
isMyDef [(ModName, DataPropDecl)]
mds
where
msg :: [Char]
msg = [Char]
"resolveDecls" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ (ModName, TyCon) -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp (ModName
mName, TyCon
tc)
isMyDef :: (ModName, b) -> Bool
isMyDef = (ModName
mName ModName -> ModName -> Bool
forall a. Eq a => a -> a -> Bool
==) (ModName -> Bool)
-> ((ModName, b) -> ModName) -> (ModName, b) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ModName, b) -> ModName
forall a b. (a, b) -> a
fst
isHomeDef :: (ModName, b) -> Bool
isHomeDef = (Symbol
tcHome Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
==) (Symbol -> Bool)
-> ((ModName, b) -> Symbol) -> (ModName, b) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModName -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol (ModName -> Symbol)
-> ((ModName, b) -> ModName) -> (ModName, b) -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ModName, b) -> ModName
forall a b. (a, b) -> a
fst
tcHome :: Symbol
tcHome = Symbol -> Symbol
GM.takeModuleNames (TyCon -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol TyCon
tc)
isLHAssumptionsDef :: (ModName, b) -> Bool
isLHAssumptionsDef = [Char] -> [Char] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
L.isSuffixOf [Char]
"_LHAssumptions" ([Char] -> Bool)
-> ((ModName, b) -> [Char]) -> (ModName, b) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleName -> [Char]
Ghc.moduleNameString (ModuleName -> [Char])
-> ((ModName, b) -> ModuleName) -> (ModName, b) -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModName -> ModuleName
getModName (ModName -> ModuleName)
-> ((ModName, b) -> ModName) -> (ModName, b) -> ModuleName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ModName, b) -> ModName
forall a b. (a, b) -> a
fst
groupDataCons :: [(Ghc.TyCon, (ModName, DataPropDecl))]
-> [Located DataConP]
-> [(Ghc.TyCon, (DataPropDecl, [(Ghc.DataCon, DataConP)]))]
groupDataCons :: [(TyCon, (ModName, DataPropDecl))]
-> [Located DataConP]
-> [(TyCon, (DataPropDecl, [(DataCon, DataConP)]))]
groupDataCons [(TyCon, (ModName, DataPropDecl))]
tds [Located DataConP]
ds = [ (TyCon
tc, (DataPropDecl
d, [(DataCon, DataConP)]
dds')) | (TyCon
tc, ((ModName
m, DataPropDecl
d), [(DataCon, DataConP)]
dds)) <- [(TyCon, ((ModName, DataPropDecl), [(DataCon, DataConP)]))]
tcDataCons
, let dds' :: [(DataCon, DataConP)]
dds' = ((DataCon, DataConP) -> Bool)
-> [(DataCon, DataConP)] -> [(DataCon, DataConP)]
forall a. (a -> Bool) -> [a] -> [a]
filter (ModName -> DataConP -> Bool
isResolvedDataConP ModName
m (DataConP -> Bool)
-> ((DataCon, DataConP) -> DataConP) -> (DataCon, DataConP) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (DataCon, DataConP) -> DataConP
forall a b. (a, b) -> b
snd) [(DataCon, DataConP)]
dds
]
where
tcDataCons :: [(TyCon, ((ModName, DataPropDecl), [(DataCon, DataConP)]))]
tcDataCons = HashMap TyCon ((ModName, DataPropDecl), [(DataCon, DataConP)])
-> [(TyCon, ((ModName, DataPropDecl), [(DataCon, DataConP)]))]
forall k v. HashMap k v -> [(k, v)]
M.toList (HashMap TyCon ((ModName, DataPropDecl), [(DataCon, DataConP)])
-> [(TyCon, ((ModName, DataPropDecl), [(DataCon, DataConP)]))])
-> HashMap TyCon ((ModName, DataPropDecl), [(DataCon, DataConP)])
-> [(TyCon, ((ModName, DataPropDecl), [(DataCon, DataConP)]))]
forall a b. (a -> b) -> a -> b
$ ((ModName, DataPropDecl)
-> [(DataCon, DataConP)]
-> ((ModName, DataPropDecl), [(DataCon, DataConP)]))
-> HashMap TyCon (ModName, DataPropDecl)
-> HashMap TyCon [(DataCon, DataConP)]
-> HashMap TyCon ((ModName, DataPropDecl), [(DataCon, DataConP)])
forall k v1 v2 v3.
Eq k =>
(v1 -> v2 -> v3) -> HashMap k v1 -> HashMap k v2 -> HashMap k v3
M.intersectionWith (,) HashMap TyCon (ModName, DataPropDecl)
declM HashMap TyCon [(DataCon, DataConP)]
ctorM
declM :: HashMap TyCon (ModName, DataPropDecl)
declM = [(TyCon, (ModName, DataPropDecl))]
-> HashMap TyCon (ModName, DataPropDecl)
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [(TyCon, (ModName, DataPropDecl))]
tds
ctorM :: HashMap TyCon [(DataCon, DataConP)]
ctorM = [(TyCon, (DataCon, DataConP))]
-> HashMap TyCon [(DataCon, DataConP)]
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k [v]
Misc.group [(DataCon -> TyCon
Ghc.dataConTyCon DataCon
d, (DataCon
d, DataConP
dcp)) | Loc SourcePos
_ SourcePos
_ DataConP
dcp <- [Located DataConP]
ds, let d :: DataCon
d = DataConP -> DataCon
dcpCon DataConP
dcp]
isResolvedDataConP :: ModName -> DataConP -> Bool
isResolvedDataConP :: ModName -> DataConP -> Bool
isResolvedDataConP ModName
m DataConP
dp = ModName -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol ModName
m Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== DataConP -> Symbol
dcpModule DataConP
dp
makeFDataDecls :: F.TCEmb Ghc.TyCon -> Ghc.TyCon -> DataPropDecl -> [(Ghc.DataCon, DataConP)]
-> F.DataDecl
makeFDataDecls :: TCEmb TyCon
-> TyCon -> DataPropDecl -> [(DataCon, DataConP)] -> DataDecl
makeFDataDecls TCEmb TyCon
tce TyCon
tc DataPropDecl
dd [(DataCon, DataConP)]
ctors = TCEmb TyCon
-> TyCon -> DataDecl -> [(DataCon, DataConP)] -> DataDecl
makeDataDecl TCEmb TyCon
tce TyCon
tc (DataPropDecl -> DataDecl
forall a b. (a, b) -> a
fst DataPropDecl
dd) [(DataCon, DataConP)]
ctors
makeDataDecl :: F.TCEmb Ghc.TyCon -> Ghc.TyCon -> DataDecl -> [(Ghc.DataCon, DataConP)]
-> F.DataDecl
makeDataDecl :: TCEmb TyCon
-> TyCon -> DataDecl -> [(DataCon, DataConP)] -> DataDecl
makeDataDecl TCEmb TyCon
tce TyCon
tc DataDecl
dd [(DataCon, DataConP)]
ctors
= F.DDecl
{ ddTyCon :: FTycon
F.ddTyCon = FTycon
ftc
, ddVars :: Int
F.ddVars = [Var] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([Var] -> Int) -> [Var] -> Int
forall a b. (a -> b) -> a -> b
$ TyCon -> [Var]
GM.tyConTyVarsDef TyCon
tc
, ddCtors :: [DataCtor]
F.ddCtors = TCEmb TyCon -> FTycon -> (DataCon, DataConP) -> DataCtor
makeDataCtor TCEmb TyCon
tce FTycon
ftc ((DataCon, DataConP) -> DataCtor)
-> [(DataCon, DataConP)] -> [DataCtor]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(DataCon, DataConP)]
ctors
}
where
ftc :: FTycon
ftc = Located Symbol -> FTycon
F.symbolFTycon (TyCon -> DataDecl -> Located Symbol
tyConLocSymbol TyCon
tc DataDecl
dd)
tyConLocSymbol :: Ghc.TyCon -> DataDecl -> LocSymbol
tyConLocSymbol :: TyCon -> DataDecl -> Located Symbol
tyConLocSymbol TyCon
tc DataDecl
dd = DataName -> Symbol -> Located Symbol
forall l b. Loc l => l -> b -> Located b
F.atLoc (DataDecl -> DataName
tycName DataDecl
dd) (TyCon -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol TyCon
tc)
makeDataCtor :: F.TCEmb Ghc.TyCon -> F.FTycon -> (Ghc.DataCon, DataConP) -> F.DataCtor
makeDataCtor :: TCEmb TyCon -> FTycon -> (DataCon, DataConP) -> DataCtor
makeDataCtor TCEmb TyCon
tce FTycon
c (DataCon
d, DataConP
dp) = F.DCtor
{ dcName :: Located Symbol
F.dcName = DataCon -> Located Symbol
forall a. (Symbolic a, NamedThing a) => a -> Located Symbol
GM.namedLocSymbol DataCon
d
, dcFields :: [DataField]
F.dcFields = TCEmb TyCon
-> FTycon
-> [RTyVar]
-> [(Located Symbol, SpecType)]
-> [DataField]
makeDataFields TCEmb TyCon
tce FTycon
c [RTyVar]
as [(Located Symbol, SpecType)]
xts
}
where
as :: [RTyVar]
as = DataConP -> [RTyVar]
dcpFreeTyVars DataConP
dp
xts :: [(Located Symbol, SpecType)]
xts = [ (Symbol -> Located Symbol
fld Symbol
x, SpecType
t) | (Symbol
x, SpecType
t) <- [(Symbol, SpecType)] -> [(Symbol, SpecType)]
forall a. [a] -> [a]
reverse (DataConP -> [(Symbol, SpecType)]
dcpTyArgs DataConP
dp) ]
fld :: Symbol -> Located Symbol
fld = DataConP -> Symbol -> Located Symbol
forall l b. Loc l => l -> b -> Located b
F.atLoc DataConP
dp (Symbol -> Located Symbol)
-> (Symbol -> Symbol) -> Symbol -> Located Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataCon -> DataConP -> Symbol -> Symbol
fieldName DataCon
d DataConP
dp
fieldName :: Ghc.DataCon -> DataConP -> F.Symbol -> F.Symbol
fieldName :: DataCon -> DataConP -> Symbol -> Symbol
fieldName DataCon
d DataConP
dp Symbol
x
| DataConP -> Bool
dcpIsGadt DataConP
dp = Symbol -> Symbol -> Symbol
F.suffixSymbol (DataCon -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol DataCon
d) Symbol
x
| Bool
otherwise = Symbol
x
makeDataFields :: F.TCEmb Ghc.TyCon -> F.FTycon -> [RTyVar] -> [(F.LocSymbol, SpecType)]
-> [F.DataField]
makeDataFields :: TCEmb TyCon
-> FTycon
-> [RTyVar]
-> [(Located Symbol, SpecType)]
-> [DataField]
makeDataFields TCEmb TyCon
tce FTycon
_c [RTyVar]
as [(Located Symbol, SpecType)]
xts = [ Located Symbol -> Sort -> DataField
F.DField Located Symbol
x (SpecType -> Sort
fSort SpecType
t) | (Located Symbol
x, SpecType
t) <- [(Located Symbol, SpecType)]
xts]
where
su :: [(Symbol, Int)]
su = [Symbol] -> [Int] -> [(Symbol, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip (RTyVar -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol (RTyVar -> Symbol) -> [RTyVar] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RTyVar]
as) [Int
0..]
fSort :: SpecType -> Sort
fSort = [(Symbol, Int)] -> Sort -> Sort
F.substVars [(Symbol, Int)]
su (Sort -> Sort) -> (SpecType -> Sort) -> SpecType -> Sort
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> Int) -> Sort -> Sort
F.mapFVar (Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [RTyVar] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [RTyVar]
as) (Sort -> Sort) -> (SpecType -> Sort) -> SpecType -> Sort
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCEmb TyCon -> SpecType -> Sort
forall r.
(PPrint r, Reftable r, SubsTy RTyVar (RType RTyCon RTyVar ()) r,
Reftable (RTProp RTyCon RTyVar r)) =>
TCEmb TyCon -> RRType r -> Sort
RT.rTypeSort TCEmb TyCon
tce
meetDataConSpec :: Bool -> F.TCEmb Ghc.TyCon -> [(Ghc.Var, SpecType)] -> [DataConP]
-> [(Ghc.Var, SpecType)]
meetDataConSpec :: Bool
-> TCEmb TyCon
-> [(Var, SpecType)]
-> [DataConP]
-> [(Var, SpecType)]
meetDataConSpec Bool
allowTC TCEmb TyCon
emb [(Var, SpecType)]
xts [DataConP]
dcs = HashMap Var SpecType -> [(Var, SpecType)]
forall k v. HashMap k v -> [(k, v)]
M.toList (HashMap Var SpecType -> [(Var, SpecType)])
-> HashMap Var SpecType -> [(Var, SpecType)]
forall a b. (a -> b) -> a -> b
$ (SrcSpan, SpecType) -> SpecType
forall a b. (a, b) -> b
snd ((SrcSpan, SpecType) -> SpecType)
-> HashMap Var (SrcSpan, SpecType) -> HashMap Var SpecType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (HashMap Var (SrcSpan, SpecType)
-> (Var, SpecType) -> HashMap Var (SrcSpan, SpecType))
-> HashMap Var (SrcSpan, SpecType)
-> [(Var, SpecType)]
-> HashMap Var (SrcSpan, SpecType)
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' HashMap Var (SrcSpan, SpecType)
-> (Var, SpecType) -> HashMap Var (SrcSpan, SpecType)
forall {a}.
(PPrint a, NamedThing a, Hashable a) =>
HashMap a (SrcSpan, SpecType)
-> (a, SpecType) -> HashMap a (SrcSpan, SpecType)
upd HashMap Var (SrcSpan, SpecType)
dcm0 [(Var, SpecType)]
xts
where
dcm0 :: HashMap Var (SrcSpan, SpecType)
dcm0 = ((SrcSpan, SpecType) -> (SrcSpan, SpecType) -> (SrcSpan, SpecType))
-> [(Var, (SrcSpan, SpecType))] -> HashMap Var (SrcSpan, SpecType)
forall k v.
(Eq k, Hashable k) =>
(v -> v -> v) -> [(k, v)] -> HashMap k v
M.fromListWith (SrcSpan, SpecType) -> (SrcSpan, SpecType) -> (SrcSpan, SpecType)
forall {b} {a} {a}. Reftable b => (a, b) -> (a, b) -> (a, b)
meetM (Bool -> [DataConP] -> [(Var, (SrcSpan, SpecType))]
dataConSpec' Bool
allowTC [DataConP]
dcs)
upd :: HashMap a (SrcSpan, SpecType)
-> (a, SpecType) -> HashMap a (SrcSpan, SpecType)
upd HashMap a (SrcSpan, SpecType)
dcm (a
x, SpecType
t) = a
-> (SrcSpan, SpecType)
-> HashMap a (SrcSpan, SpecType)
-> HashMap a (SrcSpan, SpecType)
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert a
x (a -> SrcSpan
forall a. NamedThing a => a -> SrcSpan
Ghc.getSrcSpan a
x, SpecType
tx') HashMap a (SrcSpan, SpecType)
dcm
where
tx' :: SpecType
tx' = SpecType
-> ((SrcSpan, SpecType) -> SpecType)
-> Maybe (SrcSpan, SpecType)
-> SpecType
forall b a. b -> (a -> b) -> Maybe a -> b
maybe SpecType
t (a -> SpecType -> (SrcSpan, SpecType) -> SpecType
forall {a}.
(PPrint a, NamedThing a) =>
a -> SpecType -> (SrcSpan, SpecType) -> SpecType
meetX a
x SpecType
t) (a -> HashMap a (SrcSpan, SpecType) -> Maybe (SrcSpan, SpecType)
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup a
x HashMap a (SrcSpan, SpecType)
dcm)
meetM :: (a, b) -> (a, b) -> (a, b)
meetM (a
l,b
t) (a
_,b
t') = (a
l, b
t b -> b -> b
forall r. Reftable r => r -> r -> r
`F.meet` b
t')
meetX :: a -> SpecType -> (SrcSpan, SpecType) -> SpecType
meetX a
x SpecType
t (SrcSpan
sp', SpecType
t') = [Char] -> SpecType -> SpecType
forall a. PPrint a => [Char] -> a -> a
F.notracepp (a -> SpecType -> SpecType -> [Char]
forall {a} {b} {c}.
(PPrint a, PPrint b, PPrint c) =>
a -> b -> c -> [Char]
_msg a
x SpecType
t SpecType
t') (SpecType -> SpecType) -> SpecType -> SpecType
forall a b. (a -> b) -> a -> b
$ TCEmb TyCon
-> Doc -> (SrcSpan, SpecType) -> (SrcSpan, SpecType) -> SpecType
meetVarTypes TCEmb TyCon
emb (a -> Doc
forall a. PPrint a => a -> Doc
pprint a
x) (a -> SrcSpan
forall a. NamedThing a => a -> SrcSpan
Ghc.getSrcSpan a
x, SpecType
t) (SrcSpan
sp', SpecType
t')
_msg :: a -> b -> c -> [Char]
_msg a
x b
t c
t' = [Char]
"MEET-VAR-TYPES: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ (a, b, c) -> [Char]
forall a. PPrint a => a -> [Char]
showpp (a
x, b
t, c
t')
dataConSpec' :: Bool -> [DataConP] -> [(Ghc.Var, (Ghc.SrcSpan, SpecType))]
dataConSpec' :: Bool -> [DataConP] -> [(Var, (SrcSpan, SpecType))]
dataConSpec' Bool
allowTC = (DataConP -> [(Var, (SrcSpan, SpecType))])
-> [DataConP] -> [(Var, (SrcSpan, SpecType))]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap DataConP -> [(Var, (SrcSpan, SpecType))]
tx
where
tx :: DataConP -> [(Var, (SrcSpan, SpecType))]
tx DataConP
dcp = [ (Var
x, (SrcSpan, SpecType)
res) | (Var
x, SpecType
t0) <- Bool -> DataConP -> [(Var, SpecType)]
dataConPSpecType Bool
allowTC DataConP
dcp
, let t :: SpecType
t = Var -> SpecType -> SpecType
forall r.
(PPrint r, Reftable r, SubsTy RTyVar (RType RTyCon RTyVar ()) r,
Reftable (RTProp RTyCon RTyVar r)) =>
Var -> RType RTyCon RTyVar r -> RType RTyCon RTyVar r
RT.expandProductType Var
x SpecType
t0
, let res :: (SrcSpan, SpecType)
res = (DataConP -> SrcSpan
forall a. Loc a => a -> SrcSpan
GM.fSrcSpan DataConP
dcp, SpecType
t)
]
makeConTypes :: ModName -> Bare.Env -> [(ModName, Ms.BareSpec)]
-> Bare.Lookup ([(ModName, TyConP, Maybe DataPropDecl)], [[Located DataConP]])
makeConTypes :: ModName
-> Env
-> [(ModName, BareSpec)]
-> Lookup
([(ModName, TyConP, Maybe DataPropDecl)], [[Located DataConP]])
makeConTypes ModName
myName Env
env [(ModName, BareSpec)]
specs =
[([(ModName, TyConP, Maybe DataPropDecl)], [[Located DataConP]])]
-> ([(ModName, TyConP, Maybe DataPropDecl)], [[Located DataConP]])
forall a b. [([a], [b])] -> ([a], [b])
Misc.concatUnzip ([([(ModName, TyConP, Maybe DataPropDecl)], [[Located DataConP]])]
-> ([(ModName, TyConP, Maybe DataPropDecl)], [[Located DataConP]]))
-> Either
[Error]
[([(ModName, TyConP, Maybe DataPropDecl)], [[Located DataConP]])]
-> Lookup
([(ModName, TyConP, Maybe DataPropDecl)], [[Located DataConP]])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((ModName, BareSpec)
-> Lookup
([(ModName, TyConP, Maybe DataPropDecl)], [[Located DataConP]]))
-> [(ModName, BareSpec)]
-> Either
[Error]
[([(ModName, TyConP, Maybe DataPropDecl)], [[Located DataConP]])]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (ModName
-> Env
-> (ModName, BareSpec)
-> Lookup
([(ModName, TyConP, Maybe DataPropDecl)], [[Located DataConP]])
makeConTypes' ModName
myName Env
env) [(ModName, BareSpec)]
specs
makeConTypes' :: ModName -> Bare.Env -> (ModName, Ms.BareSpec)
-> Bare.Lookup ([(ModName, TyConP, Maybe DataPropDecl)], [[Located DataConP]])
makeConTypes' :: ModName
-> Env
-> (ModName, BareSpec)
-> Lookup
([(ModName, TyConP, Maybe DataPropDecl)], [[Located DataConP]])
makeConTypes' ModName
_myName Env
env (ModName
name, BareSpec
spec) = do
[DataDecl]
dcs' <- Env -> ModName -> [DataDecl] -> Lookup [DataDecl]
canonizeDecls Env
env ModName
name [DataDecl]
dcs
let dcs'' :: [DataDecl]
dcs'' = BareSpec -> [DataDecl] -> [DataDecl]
dataDeclSize BareSpec
spec [DataDecl]
dcs'
let gvs :: [(Maybe DataDecl, Maybe (Located Symbol, [Variance]))]
gvs = [DataDecl]
-> [(Located Symbol, [Variance])]
-> [(Maybe DataDecl, Maybe (Located Symbol, [Variance]))]
groupVariances [DataDecl]
dcs'' [(Located Symbol, [Variance])]
vdcs
[((ModName, TyConP, Maybe DataPropDecl), [Located DataConP])]
zong <- [Lookup
((ModName, TyConP, Maybe DataPropDecl), [Located DataConP])]
-> Lookup
[((ModName, TyConP, Maybe DataPropDecl), [Located DataConP])]
forall a. [Lookup a] -> Lookup [a]
catLookups ([Lookup
((ModName, TyConP, Maybe DataPropDecl), [Located DataConP])]
-> Lookup
[((ModName, TyConP, Maybe DataPropDecl), [Located DataConP])])
-> ([(Maybe DataDecl, Maybe (Located Symbol, [Variance]))]
-> [Lookup
((ModName, TyConP, Maybe DataPropDecl), [Located DataConP])])
-> [(Maybe DataDecl, Maybe (Located Symbol, [Variance]))]
-> Lookup
[((ModName, TyConP, Maybe DataPropDecl), [Located DataConP])]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Maybe DataDecl, Maybe (Located Symbol, [Variance]))
-> Lookup
((ModName, TyConP, Maybe DataPropDecl), [Located DataConP]))
-> [(Maybe DataDecl, Maybe (Located Symbol, [Variance]))]
-> [Lookup
((ModName, TyConP, Maybe DataPropDecl), [Located DataConP])]
forall a b. (a -> b) -> [a] -> [b]
map ((Maybe DataDecl
-> Maybe (Located Symbol, [Variance])
-> Lookup
((ModName, TyConP, Maybe DataPropDecl), [Located DataConP]))
-> (Maybe DataDecl, Maybe (Located Symbol, [Variance]))
-> Lookup
((ModName, TyConP, Maybe DataPropDecl), [Located DataConP])
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (Env
-> ModName
-> Maybe DataDecl
-> Maybe (Located Symbol, [Variance])
-> Lookup
((ModName, TyConP, Maybe DataPropDecl), [Located DataConP])
ofBDataDecl Env
env ModName
name)) ([(Maybe DataDecl, Maybe (Located Symbol, [Variance]))]
-> Lookup
[((ModName, TyConP, Maybe DataPropDecl), [Located DataConP])])
-> [(Maybe DataDecl, Maybe (Located Symbol, [Variance]))]
-> Lookup
[((ModName, TyConP, Maybe DataPropDecl), [Located DataConP])]
forall a b. (a -> b) -> a -> b
$ [(Maybe DataDecl, Maybe (Located Symbol, [Variance]))]
gvs
([(ModName, TyConP, Maybe DataPropDecl)], [[Located DataConP]])
-> Lookup
([(ModName, TyConP, Maybe DataPropDecl)], [[Located DataConP]])
forall a. a -> Either [Error] a
forall (m :: * -> *) a. Monad m => a -> m a
return ([((ModName, TyConP, Maybe DataPropDecl), [Located DataConP])]
-> ([(ModName, TyConP, Maybe DataPropDecl)], [[Located DataConP]])
forall a b. [(a, b)] -> ([a], [b])
unzip [((ModName, TyConP, Maybe DataPropDecl), [Located DataConP])]
zong)
where
dcs :: [DataDecl]
dcs = BareSpec -> [DataDecl]
forall ty bndr. Spec ty bndr -> [DataDecl]
Ms.dataDecls BareSpec
spec
vdcs :: [(Located Symbol, [Variance])]
vdcs = BareSpec -> [(Located Symbol, [Variance])]
forall ty bndr. Spec ty bndr -> [(Located Symbol, [Variance])]
Ms.dvariance BareSpec
spec
type DSizeMap = M.HashMap F.Symbol (F.Symbol, [F.Symbol])
normalizeDSize :: [([LocBareType], F.LocSymbol)] -> DSizeMap
normalizeDSize :: [([LocBareType], Located Symbol)] -> DSizeMap
normalizeDSize [([LocBareType], Located Symbol)]
ds = [(Symbol, (Symbol, [Symbol]))] -> DSizeMap
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList ((([LocBareType], Located Symbol) -> [(Symbol, (Symbol, [Symbol]))])
-> [([LocBareType], Located Symbol)]
-> [(Symbol, (Symbol, [Symbol]))]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ([LocBareType], Located Symbol) -> [(Symbol, (Symbol, [Symbol]))]
forall {tv} {r} {a}.
([Located (RType BTyCon tv r)], Located a)
-> [(Symbol, (a, [Symbol]))]
go [([LocBareType], Located Symbol)]
ds)
where go :: ([Located (RType BTyCon tv r)], Located a)
-> [(Symbol, (a, [Symbol]))]
go ([Located (RType BTyCon tv r)]
ts,Located a
x) = let xs :: [Symbol]
xs = (Located (RType BTyCon tv r) -> Maybe Symbol)
-> [Located (RType BTyCon tv r)] -> [Symbol]
forall a b. (a -> Maybe b) -> [a] -> [b]
Mb.mapMaybe (RType BTyCon tv r -> Maybe Symbol
forall {tv} {r}. RType BTyCon tv r -> Maybe Symbol
getTc (RType BTyCon tv r -> Maybe Symbol)
-> (Located (RType BTyCon tv r) -> RType BTyCon tv r)
-> Located (RType BTyCon tv r)
-> Maybe Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Located (RType BTyCon tv r) -> RType BTyCon tv r
forall a. Located a -> a
val) [Located (RType BTyCon tv r)]
ts
in [(Symbol
tc, (Located a -> a
forall a. Located a -> a
val Located a
x, [Symbol]
xs)) | Symbol
tc <- [Symbol]
xs]
getTc :: RType BTyCon tv r -> Maybe Symbol
getTc (RAllT RTVU BTyCon tv
_ RType BTyCon tv r
t r
_) = RType BTyCon tv r -> Maybe Symbol
getTc RType BTyCon tv r
t
getTc (RApp BTyCon
c [RType BTyCon tv r]
_ [RTProp BTyCon tv r]
_ r
_) = Symbol -> Maybe Symbol
forall a. a -> Maybe a
Just (Located Symbol -> Symbol
forall a. Located a -> a
val (Located Symbol -> Symbol) -> Located Symbol -> Symbol
forall a b. (a -> b) -> a -> b
$ BTyCon -> Located Symbol
btc_tc BTyCon
c)
getTc RType BTyCon tv r
_ = Maybe Symbol
forall a. Maybe a
Nothing
dataDeclSize :: Ms.BareSpec -> [DataDecl] -> [DataDecl]
dataDeclSize :: BareSpec -> [DataDecl] -> [DataDecl]
dataDeclSize BareSpec
spec [DataDecl]
dcs = DSizeMap -> DataDecl -> DataDecl
makeSize DSizeMap
smap (DataDecl -> DataDecl) -> [DataDecl] -> [DataDecl]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [DataDecl]
dcs
where smap :: DSizeMap
smap = [([LocBareType], Located Symbol)] -> DSizeMap
normalizeDSize ([([LocBareType], Located Symbol)] -> DSizeMap)
-> [([LocBareType], Located Symbol)] -> DSizeMap
forall a b. (a -> b) -> a -> b
$ BareSpec -> [([LocBareType], Located Symbol)]
forall ty bndr. Spec ty bndr -> [([ty], Located Symbol)]
Ms.dsize BareSpec
spec
makeSize :: DSizeMap -> DataDecl -> DataDecl
makeSize :: DSizeMap -> DataDecl -> DataDecl
makeSize DSizeMap
smap DataDecl
d
| Just (Symbol, [Symbol])
p <- Symbol -> DSizeMap -> Maybe (Symbol, [Symbol])
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup (DataName -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol (DataName -> Symbol) -> DataName -> Symbol
forall a b. (a -> b) -> a -> b
$ DataDecl -> DataName
tycName DataDecl
d) DSizeMap
smap
= DataDecl
d {tycDCons = fmap (fmap (makeSizeCtor p)) (tycDCons d) }
| Bool
otherwise
= DataDecl
d
makeSizeCtor :: (F.Symbol, [F.Symbol]) -> DataCtor -> DataCtor
makeSizeCtor :: (Symbol, [Symbol]) -> DataCtor -> DataCtor
makeSizeCtor (Symbol
s,[Symbol]
xs) DataCtor
d = DataCtor
d {dcFields = Misc.mapSnd (mapBot go) <$> dcFields d}
where
go :: RType c tv RReft -> RType c tv RReft
go (RApp c
c [RType c tv RReft]
ts [RTProp c tv RReft]
rs RReft
r) | c -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol c
c Symbol -> [Symbol] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Symbol]
xs
= c
-> [RType c tv RReft]
-> [RTProp c tv RReft]
-> RReft
-> RType c tv RReft
forall c tv r.
c -> [RType c tv r] -> [RTProp c tv r] -> r -> RType c tv r
RApp c
c [RType c tv RReft]
ts [RTProp c tv RReft]
rs (RReft
r RReft -> RReft -> RReft
forall r. Reftable r => r -> r -> r
`F.meet` RReft
rsz)
go RType c tv RReft
t = RType c tv RReft
t
rsz :: RReft
rsz = Reft -> Predicate -> RReft
forall r. r -> Predicate -> UReft r
MkUReft ((Symbol, Expr) -> Reft
F.Reft (Symbol
F.vv_, Brel -> Expr -> Expr -> Expr
F.PAtom Brel
F.Lt
(Expr -> Expr -> Expr
F.EApp (Symbol -> Expr
F.EVar Symbol
s) (Symbol -> Expr
F.EVar Symbol
F.vv_))
(Expr -> Expr -> Expr
F.EApp (Symbol -> Expr
F.EVar Symbol
s) (Symbol -> Expr
F.EVar Symbol
selfSymbol))
))
Predicate
forall a. Monoid a => a
mempty
catLookups :: [Bare.Lookup a] -> Bare.Lookup [a]
catLookups :: forall a. [Lookup a] -> Lookup [a]
catLookups = [Either [Error] a] -> Either [Error] [a]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence ([Either [Error] a] -> Either [Error] [a])
-> ([Either [Error] a] -> [Either [Error] a])
-> [Either [Error] a]
-> Either [Error] [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Either [Error] a -> Maybe (Either [Error] a))
-> [Either [Error] a] -> [Either [Error] a]
forall a b. (a -> Maybe b) -> [a] -> [b]
Mb.mapMaybe Either [Error] a -> Maybe (Either [Error] a)
forall a. Lookup a -> Maybe (Lookup a)
skipResolve
skipResolve :: Bare.Lookup a -> Maybe (Bare.Lookup a)
skipResolve :: forall a. Lookup a -> Maybe (Lookup a)
skipResolve (Left [Error]
es) = [Error] -> Maybe (Either [Error] a)
forall e a. [e] -> Maybe (Either [e] a)
left' ((Error -> Bool) -> [Error] -> [Error]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Error -> Bool) -> Error -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Error -> Bool
forall t. TError t -> Bool
isErrResolve) [Error]
es)
skipResolve (Right a
v) = Either [Error] a -> Maybe (Either [Error] a)
forall a. a -> Maybe a
Just (a -> Either [Error] a
forall a b. b -> Either a b
Right a
v)
isErrResolve :: TError t -> Bool
isErrResolve :: forall t. TError t -> Bool
isErrResolve ErrResolve {} = Bool
True
isErrResolve TError t
_ = Bool
False
left' :: [e] -> Maybe (Either [e] a)
left' :: forall e a. [e] -> Maybe (Either [e] a)
left' [] = Maybe (Either [e] a)
forall a. Maybe a
Nothing
left' [e]
es = Either [e] a -> Maybe (Either [e] a)
forall a. a -> Maybe a
Just ([e] -> Either [e] a
forall a b. a -> Either a b
Left [e]
es)
canonizeDecls :: Bare.Env -> ModName -> [DataDecl] -> Bare.Lookup [DataDecl]
canonizeDecls :: Env -> ModName -> [DataDecl] -> Lookup [DataDecl]
canonizeDecls Env
env ModName
name [DataDecl]
dataDecls = do
[Maybe (Symbol, DataDecl)]
kds <- [DataDecl]
-> (DataDecl -> Either [Error] (Maybe (Symbol, DataDecl)))
-> Either [Error] [Maybe (Symbol, DataDecl)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [DataDecl]
dataDecls ((DataDecl -> Either [Error] (Maybe (Symbol, DataDecl)))
-> Either [Error] [Maybe (Symbol, DataDecl)])
-> (DataDecl -> Either [Error] (Maybe (Symbol, DataDecl)))
-> Either [Error] [Maybe (Symbol, DataDecl)]
forall a b. (a -> b) -> a -> b
$ \DataDecl
d -> do
Maybe Symbol
k <- Env -> ModName -> DataDecl -> Lookup (Maybe Symbol)
dataDeclKey Env
env ModName
name DataDecl
d
Maybe (Symbol, DataDecl)
-> Either [Error] (Maybe (Symbol, DataDecl))
forall a. a -> Either [Error] a
forall (m :: * -> *) a. Monad m => a -> m a
return ((Symbol -> (Symbol, DataDecl))
-> Maybe Symbol -> Maybe (Symbol, DataDecl)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (, DataDecl
d) Maybe Symbol
k)
case ((Symbol, [DataDecl]) -> Either [DataDecl] DataDecl)
-> [(Symbol, DataDecl)] -> Either [DataDecl] [DataDecl]
forall k v e.
(Eq k, Hashable k) =>
((k, [v]) -> Either e v) -> [(k, v)] -> Either e [v]
Misc.uniqueByKey' (Symbol, [DataDecl]) -> Either [DataDecl] DataDecl
forall a. (a, [DataDecl]) -> Either [DataDecl] DataDecl
selectDD ([Maybe (Symbol, DataDecl)] -> [(Symbol, DataDecl)]
forall a. [Maybe a] -> [a]
Mb.catMaybes [Maybe (Symbol, DataDecl)]
kds) of
Left [DataDecl]
decls -> [Error] -> Lookup [DataDecl]
forall a b. a -> Either a b
Left [[DataDecl] -> Error
forall {t}. [DataDecl] -> TError t
err [DataDecl]
decls]
Right [DataDecl]
decls -> [DataDecl] -> Lookup [DataDecl]
forall a. a -> Either [Error] a
forall (m :: * -> *) a. Monad m => a -> m a
return [DataDecl]
decls
where
err :: [DataDecl] -> TError t
err ds :: [DataDecl]
ds@(DataDecl
d:[DataDecl]
_) = Doc -> ListNE SrcSpan -> TError t
forall t. Doc -> ListNE SrcSpan -> TError t
errDupSpecs (DataName -> Doc
forall a. PPrint a => a -> Doc
pprint (DataDecl -> DataName
tycName DataDecl
d)) (DataDecl -> SrcSpan
forall a. Loc a => a -> SrcSpan
GM.fSrcSpan (DataDecl -> SrcSpan) -> [DataDecl] -> ListNE SrcSpan
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [DataDecl]
ds)
err [DataDecl]
_ = Maybe SrcSpan -> [Char] -> TError t
forall a. Maybe SrcSpan -> [Char] -> a
impossible Maybe SrcSpan
forall a. Maybe a
Nothing [Char]
"canonizeDecls"
dataDeclKey :: Bare.Env -> ModName -> DataDecl -> Bare.Lookup (Maybe F.Symbol)
dataDeclKey :: Env -> ModName -> DataDecl -> Lookup (Maybe Symbol)
dataDeclKey Env
env ModName
name DataDecl
d = do
Maybe TyCon
tcMb <- Env -> ModName -> [Char] -> DataName -> Lookup (Maybe TyCon)
Bare.lookupGhcDnTyCon Env
env ModName
name [Char]
"canonizeDecls" (DataDecl -> DataName
tycName DataDecl
d)
case Maybe TyCon
tcMb of
Maybe TyCon
Nothing ->
Maybe Symbol -> Lookup (Maybe Symbol)
forall a. a -> Either [Error] a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Symbol
forall a. Maybe a
Nothing
Just TyCon
tc -> do
[DataCtor]
_ <- Env
-> ModName
-> TyCon
-> DataDecl
-> Maybe [DataCtor]
-> Lookup [DataCtor]
checkDataCtors Env
env ModName
name TyCon
tc DataDecl
d (DataDecl -> Maybe [DataCtor]
tycDCons DataDecl
d)
Maybe Symbol -> Lookup (Maybe Symbol)
forall a. a -> Either [Error] a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Symbol -> Lookup (Maybe Symbol))
-> Maybe Symbol -> Lookup (Maybe Symbol)
forall a b. (a -> b) -> a -> b
$ Symbol -> Maybe Symbol
forall a. a -> Maybe a
Just (TyCon -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol TyCon
tc)
checkDataCtors :: Bare.Env -> ModName -> Ghc.TyCon -> DataDecl -> Maybe [DataCtor] -> Bare.Lookup [DataCtor]
checkDataCtors :: Env
-> ModName
-> TyCon
-> DataDecl
-> Maybe [DataCtor]
-> Lookup [DataCtor]
checkDataCtors Env
_env ModName
_name TyCon
_c DataDecl
_dd Maybe [DataCtor]
Nothing = [DataCtor] -> Lookup [DataCtor]
forall a. a -> Either [Error] a
forall (m :: * -> *) a. Monad m => a -> m a
return []
checkDataCtors Env
env ModName
name TyCon
c DataDecl
dd (Just [DataCtor]
cons) = do
let dcs :: S.HashSet F.Symbol
dcs :: HashSet Symbol
dcs = [Symbol] -> HashSet Symbol
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ([Symbol] -> HashSet Symbol)
-> (TyCon -> [Symbol]) -> TyCon -> HashSet Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (DataCon -> Symbol) -> [DataCon] -> [Symbol]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DataCon -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol ([DataCon] -> [Symbol])
-> (TyCon -> [DataCon]) -> TyCon -> [Symbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyCon -> [DataCon]
Ghc.tyConDataCons (TyCon -> HashSet Symbol) -> TyCon -> HashSet Symbol
forall a b. (a -> b) -> a -> b
$ TyCon
c
[Maybe DataCon]
mbDcs <- (DataCtor -> Either [Error] (Maybe DataCon))
-> [DataCtor] -> Either [Error] [Maybe DataCon]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Env
-> ModName
-> Either [Error] DataCon
-> Either [Error] (Maybe DataCon)
forall e r. Env -> ModName -> Either e r -> Either e (Maybe r)
Bare.failMaybe Env
env ModName
name (Either [Error] DataCon -> Either [Error] (Maybe DataCon))
-> (DataCtor -> Either [Error] DataCon)
-> DataCtor
-> Either [Error] (Maybe DataCon)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Env
-> ModName -> [Char] -> Located Symbol -> Either [Error] DataCon
Bare.lookupGhcDataCon Env
env ModName
name [Char]
"checkDataCtors" (Located Symbol -> Either [Error] DataCon)
-> (DataCtor -> Located Symbol)
-> DataCtor
-> Either [Error] DataCon
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataCtor -> Located Symbol
dcName) [DataCtor]
cons
let rdcs :: HashSet Symbol
rdcs = [Symbol] -> HashSet Symbol
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ([Symbol] -> HashSet Symbol)
-> ([Maybe DataCon] -> [Symbol])
-> [Maybe DataCon]
-> HashSet Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (DataCon -> Symbol) -> [DataCon] -> [Symbol]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DataCon -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol ([DataCon] -> [Symbol])
-> ([Maybe DataCon] -> [DataCon]) -> [Maybe DataCon] -> [Symbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Maybe DataCon] -> [DataCon]
forall a. [Maybe a] -> [a]
Mb.catMaybes ([Maybe DataCon] -> HashSet Symbol)
-> [Maybe DataCon] -> HashSet Symbol
forall a b. (a -> b) -> a -> b
$ [Maybe DataCon]
mbDcs
if HashSet Symbol
dcs HashSet Symbol -> HashSet Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== HashSet Symbol
rdcs
then (DataCtor -> Either [Error] DataCtor)
-> [DataCtor] -> Lookup [DataCtor]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM DataCtor -> Either [Error] DataCtor
checkDataCtorDupField [DataCtor]
cons
else [Error] -> Lookup [DataCtor]
forall a b. a -> Either a b
Left [Located Symbol -> HashSet Symbol -> HashSet Symbol -> Error
errDataConMismatch (DataName -> Located Symbol
dataNameSymbol (DataDecl -> DataName
tycName DataDecl
dd)) HashSet Symbol
dcs HashSet Symbol
rdcs]
checkDataCtorDupField :: DataCtor -> Bare.Lookup DataCtor
checkDataCtorDupField :: DataCtor -> Either [Error] DataCtor
checkDataCtorDupField DataCtor
d
| Symbol
x : [Symbol]
_ <- [Symbol]
dups = [Error] -> Either [Error] DataCtor
forall a b. a -> Either a b
Left [Located Symbol -> Symbol -> Error
forall {a} {a} {t}.
(PPrint a, PPrint a) =>
Located a -> a -> TError t
err Located Symbol
sym Symbol
x]
| Bool
otherwise = DataCtor -> Either [Error] DataCtor
forall a. a -> Either [Error] a
forall (m :: * -> *) a. Monad m => a -> m a
return DataCtor
d
where
sym :: Located Symbol
sym = DataCtor -> Located Symbol
dcName DataCtor
d
xts :: [(Symbol, RType BTyCon BTyVar RReft)]
xts = DataCtor -> [(Symbol, RType BTyCon BTyVar RReft)]
dcFields DataCtor
d
dups :: [Symbol]
dups = [ Symbol
x | (Symbol
x, [RType BTyCon BTyVar RReft]
ts) <- [(Symbol, RType BTyCon BTyVar RReft)]
-> [(Symbol, [RType BTyCon BTyVar RReft])]
forall k v. (Eq k, Hashable k) => [(k, v)] -> [(k, [v])]
Misc.groupList [(Symbol, RType BTyCon BTyVar RReft)]
xts, Int
2 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= [RType BTyCon BTyVar RReft] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [RType BTyCon BTyVar RReft]
ts ]
err :: Located a -> a -> TError t
err Located a
lc a
x = SrcSpan -> Doc -> Doc -> TError t
forall t. SrcSpan -> Doc -> Doc -> TError t
ErrDupField (SourcePos -> SrcSpan
GM.sourcePosSrcSpan (SourcePos -> SrcSpan) -> SourcePos -> SrcSpan
forall a b. (a -> b) -> a -> b
$ Located a -> SourcePos
forall a. Located a -> SourcePos
loc Located a
lc) (a -> Doc
forall a. PPrint a => a -> Doc
pprint (a -> Doc) -> a -> Doc
forall a b. (a -> b) -> a -> b
$ Located a -> a
forall a. Located a -> a
val Located a
lc) (a -> Doc
forall a. PPrint a => a -> Doc
pprint a
x)
selectDD :: (a, [DataDecl]) -> Either [DataDecl] DataDecl
selectDD :: forall a. (a, [DataDecl]) -> Either [DataDecl] DataDecl
selectDD (a
_,[DataDecl
d]) = DataDecl -> Either [DataDecl] DataDecl
forall a b. b -> Either a b
Right DataDecl
d
selectDD (a
_, [DataDecl]
ds) = case [ DataDecl
d | DataDecl
d <- [DataDecl]
ds, DataDecl -> DataDeclKind
tycKind DataDecl
d DataDeclKind -> DataDeclKind -> Bool
forall a. Eq a => a -> a -> Bool
== DataDeclKind
DataReflected ] of
[DataDecl
d] -> DataDecl -> Either [DataDecl] DataDecl
forall a b. b -> Either a b
Right DataDecl
d
[DataDecl]
_ -> [DataDecl] -> Either [DataDecl] DataDecl
forall a b. a -> Either a b
Left [DataDecl]
ds
groupVariances :: [DataDecl]
-> [(LocSymbol, [Variance])]
-> [(Maybe DataDecl, Maybe (LocSymbol, [Variance]))]
groupVariances :: [DataDecl]
-> [(Located Symbol, [Variance])]
-> [(Maybe DataDecl, Maybe (Located Symbol, [Variance]))]
groupVariances [DataDecl]
dcs [(Located Symbol, [Variance])]
vdcs = [DataDecl]
-> [(Located Symbol, [Variance])]
-> [(Maybe DataDecl, Maybe (Located Symbol, [Variance]))]
forall {a} {b}.
Symbolic a =>
[a]
-> [(Located Symbol, b)] -> [(Maybe a, Maybe (Located Symbol, b))]
merge ([DataDecl] -> [DataDecl]
forall a. Ord a => [a] -> [a]
L.sort [DataDecl]
dcs) (((Located Symbol, [Variance])
-> (Located Symbol, [Variance]) -> Ordering)
-> [(Located Symbol, [Variance])] -> [(Located Symbol, [Variance])]
forall a. (a -> a -> Ordering) -> [a] -> [a]
L.sortBy (\(Located Symbol, [Variance])
x (Located Symbol, [Variance])
y -> Located Symbol -> Located Symbol -> Ordering
forall a. Ord a => a -> a -> Ordering
compare ((Located Symbol, [Variance]) -> Located Symbol
forall a b. (a, b) -> a
fst (Located Symbol, [Variance])
x) ((Located Symbol, [Variance]) -> Located Symbol
forall a b. (a, b) -> a
fst (Located Symbol, [Variance])
y)) [(Located Symbol, [Variance])]
vdcs)
where
merge :: [a]
-> [(Located Symbol, b)] -> [(Maybe a, Maybe (Located Symbol, b))]
merge (a
d:[a]
ds) ((Located Symbol, b)
v:[(Located Symbol, b)]
vs)
| a -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol a
d Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== (Located Symbol, b) -> Symbol
forall {c} {b}. (Located c, b) -> c
sym (Located Symbol, b)
v = (a -> Maybe a
forall a. a -> Maybe a
Just a
d, (Located Symbol, b) -> Maybe (Located Symbol, b)
forall a. a -> Maybe a
Just (Located Symbol, b)
v) (Maybe a, Maybe (Located Symbol, b))
-> [(Maybe a, Maybe (Located Symbol, b))]
-> [(Maybe a, Maybe (Located Symbol, b))]
forall a. a -> [a] -> [a]
: [a]
-> [(Located Symbol, b)] -> [(Maybe a, Maybe (Located Symbol, b))]
merge [a]
ds [(Located Symbol, b)]
vs
| a -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol a
d Symbol -> Symbol -> Bool
forall a. Ord a => a -> a -> Bool
< (Located Symbol, b) -> Symbol
forall {c} {b}. (Located c, b) -> c
sym (Located Symbol, b)
v = (a -> Maybe a
forall a. a -> Maybe a
Just a
d, Maybe (Located Symbol, b)
forall a. Maybe a
Nothing) (Maybe a, Maybe (Located Symbol, b))
-> [(Maybe a, Maybe (Located Symbol, b))]
-> [(Maybe a, Maybe (Located Symbol, b))]
forall a. a -> [a] -> [a]
: [a]
-> [(Located Symbol, b)] -> [(Maybe a, Maybe (Located Symbol, b))]
merge [a]
ds ((Located Symbol, b)
v(Located Symbol, b)
-> [(Located Symbol, b)] -> [(Located Symbol, b)]
forall a. a -> [a] -> [a]
:[(Located Symbol, b)]
vs)
| Bool
otherwise = (Maybe a
forall a. Maybe a
Nothing, (Located Symbol, b) -> Maybe (Located Symbol, b)
forall a. a -> Maybe a
Just (Located Symbol, b)
v) (Maybe a, Maybe (Located Symbol, b))
-> [(Maybe a, Maybe (Located Symbol, b))]
-> [(Maybe a, Maybe (Located Symbol, b))]
forall a. a -> [a] -> [a]
: [a]
-> [(Located Symbol, b)] -> [(Maybe a, Maybe (Located Symbol, b))]
merge (a
da -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
ds) [(Located Symbol, b)]
vs
merge [] [(Located Symbol, b)]
vs = (Maybe a
forall a. Maybe a
Nothing,) (Maybe (Located Symbol, b) -> (Maybe a, Maybe (Located Symbol, b)))
-> ((Located Symbol, b) -> Maybe (Located Symbol, b))
-> (Located Symbol, b)
-> (Maybe a, Maybe (Located Symbol, b))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Located Symbol, b) -> Maybe (Located Symbol, b)
forall a. a -> Maybe a
Just ((Located Symbol, b) -> (Maybe a, Maybe (Located Symbol, b)))
-> [(Located Symbol, b)] -> [(Maybe a, Maybe (Located Symbol, b))]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Located Symbol, b)]
vs
merge [a]
ds [] = (,Maybe (Located Symbol, b)
forall a. Maybe a
Nothing) (Maybe a -> (Maybe a, Maybe (Located Symbol, b)))
-> (a -> Maybe a) -> a -> (Maybe a, Maybe (Located Symbol, b))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Maybe a
forall a. a -> Maybe a
Just (a -> (Maybe a, Maybe (Located Symbol, b)))
-> [a] -> [(Maybe a, Maybe (Located Symbol, b))]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [a]
ds
sym :: (Located c, b) -> c
sym = Located c -> c
forall a. Located a -> a
val (Located c -> c)
-> ((Located c, b) -> Located c) -> (Located c, b) -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Located c, b) -> Located c
forall a b. (a, b) -> a
fst
checkDataDecl :: Ghc.TyCon -> DataDecl -> Bool
checkDataDecl :: TyCon -> DataDecl -> Bool
checkDataDecl TyCon
c DataDecl
d = [Char] -> Bool -> Bool
forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
_msg (Bool
isGADT Bool -> Bool -> Bool
|| Int
cN Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
dN Bool -> Bool -> Bool
|| Maybe [DataCtor] -> Bool
forall a. Maybe a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (DataDecl -> Maybe [DataCtor]
tycDCons DataDecl
d))
where
_msg :: [Char]
_msg = [Char] -> [Char] -> [Char] -> Int -> Int -> [Char]
forall r. PrintfType r => [Char] -> r
printf [Char]
"checkDataDecl: D = %s, c = %s, cN = %d, dN = %d" (DataDecl -> [Char]
forall a. Show a => a -> [Char]
show DataDecl
d) (TyCon -> [Char]
forall a. Show a => a -> [Char]
show TyCon
c) Int
cN Int
dN
cN :: Int
cN = [Var] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (TyCon -> [Var]
GM.tyConTyVarsDef TyCon
c)
dN :: Int
dN = [Symbol] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (DataDecl -> [Symbol]
tycTyVars DataDecl
d)
isGADT :: Bool
isGADT = TyCon -> Bool
Ghc.isGadtSyntaxTyCon TyCon
c
getDnTyCon :: Bare.Env -> ModName -> DataName -> Bare.Lookup Ghc.TyCon
getDnTyCon :: Env -> ModName -> DataName -> Lookup TyCon
getDnTyCon Env
env ModName
name DataName
dn = do
Maybe TyCon
tcMb <- Env -> ModName -> [Char] -> DataName -> Lookup (Maybe TyCon)
Bare.lookupGhcDnTyCon Env
env ModName
name [Char]
"ofBDataDecl-1" DataName
dn
case Maybe TyCon
tcMb of
Just TyCon
tc -> TyCon -> Lookup TyCon
forall a. a -> Either [Error] a
forall (m :: * -> *) a. Monad m => a -> m a
return TyCon
tc
Maybe TyCon
Nothing -> [Error] -> Lookup TyCon
forall a b. a -> Either a b
Left [ SrcSpan -> Doc -> Doc -> Error
forall t. SrcSpan -> Doc -> Doc -> TError t
ErrBadData (DataName -> SrcSpan
forall a. Loc a => a -> SrcSpan
GM.fSrcSpan DataName
dn) (DataName -> Doc
forall a. PPrint a => a -> Doc
pprint DataName
dn) Doc
"Unknown Type Constructor" ]
ofBDataDecl :: Bare.Env -> ModName -> Maybe DataDecl -> Maybe (LocSymbol, [Variance])
-> Bare.Lookup ( (ModName, TyConP, Maybe DataPropDecl), [Located DataConP] )
ofBDataDecl :: Env
-> ModName
-> Maybe DataDecl
-> Maybe (Located Symbol, [Variance])
-> Lookup
((ModName, TyConP, Maybe DataPropDecl), [Located DataConP])
ofBDataDecl Env
env ModName
name (Just dd :: DataDecl
dd@(DataDecl DataName
tc [Symbol]
as [PVar BSort]
ps Maybe [DataCtor]
cts SourcePos
pos Maybe SizeFun
sfun Maybe (RType BTyCon BTyVar RReft)
pt DataDeclKind
_)) Maybe (Located Symbol, [Variance])
maybe_invariance_info = do
let Loc SourcePos
lc SourcePos
lc' Symbol
_ = DataName -> Located Symbol
dataNameSymbol DataName
tc
let πs :: [RPVar]
πs = Env -> ModName -> SourcePos -> PVar BSort -> RPVar
Bare.ofBPVar Env
env ModName
name SourcePos
pos (PVar BSort -> RPVar) -> [PVar BSort] -> [RPVar]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [PVar BSort]
ps
let αs :: [RTyVar]
αs = Var -> RTyVar
RTV (Var -> RTyVar) -> (Symbol -> Var) -> Symbol -> RTyVar
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Var
GM.symbolTyVar (Symbol -> RTyVar) -> [Symbol] -> [RTyVar]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol]
as
let n :: Int
n = [RTyVar] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [RTyVar]
αs
let initmap :: [(UsedPVar, Int)]
initmap = [UsedPVar] -> [Int] -> [(UsedPVar, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip (RPVar -> UsedPVar
forall t. PVar t -> UsedPVar
RT.uPVar (RPVar -> UsedPVar) -> [RPVar] -> [UsedPVar]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RPVar]
πs) [Int
0..]
TyCon
tc' <- Env -> ModName -> DataName -> Lookup TyCon
getDnTyCon Env
env ModName
name DataName
tc
[DataConP]
cts' <- (DataCtor -> Either [Error] DataConP)
-> [DataCtor] -> Either [Error] [DataConP]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Env
-> ModName
-> SourcePos
-> SourcePos
-> TyCon
-> [RTyVar]
-> [PVar BSort]
-> [RPVar]
-> DataCtor
-> Either [Error] DataConP
ofBDataCtor Env
env ModName
name SourcePos
lc SourcePos
lc' TyCon
tc' [RTyVar]
αs [PVar BSort]
ps [RPVar]
πs) ([DataCtor] -> Maybe [DataCtor] -> [DataCtor]
forall a. a -> Maybe a -> a
Mb.fromMaybe [] Maybe [DataCtor]
cts)
Bool -> Either [Error] () -> Either [Error] ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (TyCon -> DataDecl -> Bool
checkDataDecl TyCon
tc' DataDecl
dd) ([Error] -> Either [Error] ()
forall a b. a -> Either a b
Left [Error
forall {t}. TError t
err])
let pd :: Maybe SpecType
pd = Env
-> ModName
-> SourcePos
-> Maybe [PVar BSort]
-> RType BTyCon BTyVar RReft
-> SpecType
Bare.ofBareType Env
env ModName
name SourcePos
lc ([PVar BSort] -> Maybe [PVar BSort]
forall a. a -> Maybe a
Just []) (RType BTyCon BTyVar RReft -> SpecType)
-> Maybe (RType BTyCon BTyVar RReft) -> Maybe SpecType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Char]
-> Maybe (RType BTyCon BTyVar RReft)
-> Maybe (RType BTyCon BTyVar RReft)
forall a. PPrint a => [Char] -> a -> a
F.tracepp [Char]
"ofBDataDecl-prop" Maybe (RType BTyCon BTyVar RReft)
pt
let tys :: [SpecType]
tys = [SpecType
t | DataConP
dcp <- [DataConP]
cts', (Symbol
_, SpecType
t) <- DataConP -> [(Symbol, SpecType)]
dcpTyArgs DataConP
dcp]
let varInfo :: [(Int, Bool)]
varInfo = [(Int, Bool)] -> [(Int, Bool)]
forall a. Eq a => [a] -> [a]
L.nub ([(Int, Bool)] -> [(Int, Bool)]) -> [(Int, Bool)] -> [(Int, Bool)]
forall a b. (a -> b) -> a -> b
$ (SpecType -> [(Int, Bool)]) -> [SpecType] -> [(Int, Bool)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ([(UsedPVar, Int)] -> Bool -> SpecType -> [(Int, Bool)]
forall a. [(UsedPVar, a)] -> Bool -> SpecType -> [(a, Bool)]
getPsSig [(UsedPVar, Int)]
initmap Bool
True) [SpecType]
tys
let defPs :: [Variance]
defPs = [(Int, Bool)] -> Int -> Variance
forall a. Eq a => [(a, Bool)] -> a -> Variance
varSignToVariance [(Int, Bool)]
varInfo (Int -> Variance) -> [Int] -> [Variance]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Int
0 .. ([RPVar] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [RPVar]
πs Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)]
let ([Variance]
tvi, [Variance]
pvi) = case Maybe (Located Symbol, [Variance])
maybe_invariance_info of
Maybe (Located Symbol, [Variance])
Nothing -> ([], [Variance]
defPs)
Just (Located Symbol
_,[Variance]
is) -> let is_n :: [Variance]
is_n = Int -> [Variance] -> [Variance]
forall a. Int -> [a] -> [a]
drop Int
n [Variance]
is in
(Int -> [Variance] -> [Variance]
forall a. Int -> [a] -> [a]
take Int
n [Variance]
is, if [Variance] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Variance]
is_n then [Variance]
defPs else [Variance]
is_n)
let tcp :: TyConP
tcp = SourcePos
-> TyCon
-> [RTyVar]
-> [RPVar]
-> [Variance]
-> [Variance]
-> Maybe SizeFun
-> TyConP
TyConP SourcePos
lc TyCon
tc' [RTyVar]
αs [RPVar]
πs [Variance]
tvi [Variance]
pvi Maybe SizeFun
sfun
((ModName, TyConP, Maybe DataPropDecl), [Located DataConP])
-> Lookup
((ModName, TyConP, Maybe DataPropDecl), [Located DataConP])
forall a. a -> Either [Error] a
forall (m :: * -> *) a. Monad m => a -> m a
return ((ModName
name, TyConP
tcp, DataPropDecl -> Maybe DataPropDecl
forall a. a -> Maybe a
Just (DataDecl
dd { tycDCons = cts }, Maybe SpecType
pd)), SourcePos -> SourcePos -> DataConP -> Located DataConP
forall a. SourcePos -> SourcePos -> a -> Located a
Loc SourcePos
lc SourcePos
lc' (DataConP -> Located DataConP) -> [DataConP] -> [Located DataConP]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [DataConP]
cts')
where
err :: TError t
err = SrcSpan -> Doc -> Doc -> TError t
forall t. SrcSpan -> Doc -> Doc -> TError t
ErrBadData (DataName -> SrcSpan
forall a. Loc a => a -> SrcSpan
GM.fSrcSpan DataName
tc) (DataName -> Doc
forall a. PPrint a => a -> Doc
pprint DataName
tc) Doc
"Mismatch in number of type variables"
ofBDataDecl Env
env ModName
name Maybe DataDecl
Nothing (Just (Located Symbol
tc, [Variance]
is)) =
case Env -> ModName -> [Char] -> Located Symbol -> Lookup TyCon
Bare.lookupGhcTyCon Env
env ModName
name [Char]
"ofBDataDecl-2" Located Symbol
tc of
Left [Error]
e -> [Error]
-> Lookup
((ModName, TyConP, Maybe DataPropDecl), [Located DataConP])
forall a b. a -> Either a b
Left [Error]
e
Right TyCon
tc' -> ((ModName, TyConP, Maybe DataPropDecl), [Located DataConP])
-> Lookup
((ModName, TyConP, Maybe DataPropDecl), [Located DataConP])
forall a b. b -> Either a b
Right ((ModName
name, SourcePos
-> TyCon
-> [RTyVar]
-> [RPVar]
-> [Variance]
-> [Variance]
-> Maybe SizeFun
-> TyConP
TyConP SourcePos
srcpos TyCon
tc' [] [] [Variance]
tcov [Variance]
forall a. [a]
tcontr Maybe SizeFun
forall a. Maybe a
Nothing, Maybe DataPropDecl
forall a. Maybe a
Nothing), [])
where
([Variance]
tcov, [a]
tcontr) = ([Variance]
is, [])
srcpos :: SourcePos
srcpos = [Char] -> SourcePos
F.dummyPos [Char]
"LH.DataType.Variance"
ofBDataDecl Env
_ ModName
_ Maybe DataDecl
Nothing Maybe (Located Symbol, [Variance])
Nothing
= Maybe SrcSpan
-> [Char]
-> Lookup
((ModName, TyConP, Maybe DataPropDecl), [Located DataConP])
forall a. Maybe SrcSpan -> [Char] -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing [Char]
"Bare.DataType.ofBDataDecl called on invalid inputs"
ofBDataCtor :: Bare.Env
-> ModName
-> F.SourcePos
-> F.SourcePos
-> Ghc.TyCon
-> [RTyVar]
-> [PVar BSort]
-> [PVar RSort]
-> DataCtor
-> Bare.Lookup DataConP
ofBDataCtor :: Env
-> ModName
-> SourcePos
-> SourcePos
-> TyCon
-> [RTyVar]
-> [PVar BSort]
-> [RPVar]
-> DataCtor
-> Either [Error] DataConP
ofBDataCtor Env
env ModName
name SourcePos
l SourcePos
l' TyCon
tc [RTyVar]
αs [PVar BSort]
ps [RPVar]
πs DataCtor
dc = do
DataCon
c' <- Env
-> ModName -> [Char] -> Located Symbol -> Either [Error] DataCon
Bare.lookupGhcDataCon Env
env ModName
name [Char]
"ofBDataCtor" (DataCtor -> Located Symbol
dcName DataCtor
dc)
DataConP -> Either [Error] DataConP
forall a. a -> Either [Error] a
forall (m :: * -> *) a. Monad m => a -> m a
return (Env
-> ModName
-> SourcePos
-> SourcePos
-> TyCon
-> [RTyVar]
-> [PVar BSort]
-> [RPVar]
-> DataCtor
-> DataCon
-> DataConP
ofBDataCtorTc Env
env ModName
name SourcePos
l SourcePos
l' TyCon
tc [RTyVar]
αs [PVar BSort]
ps [RPVar]
πs DataCtor
dc DataCon
c')
ofBDataCtorTc :: Bare.Env -> ModName -> F.SourcePos -> F.SourcePos ->
Ghc.TyCon -> [RTyVar] -> [PVar BSort] -> [PVar RSort] -> DataCtor -> Ghc.DataCon ->
DataConP
ofBDataCtorTc :: Env
-> ModName
-> SourcePos
-> SourcePos
-> TyCon
-> [RTyVar]
-> [PVar BSort]
-> [RPVar]
-> DataCtor
-> DataCon
-> DataConP
ofBDataCtorTc Env
env ModName
name SourcePos
l SourcePos
l' TyCon
tc [RTyVar]
αs [PVar BSort]
ps [RPVar]
πs _ctor :: DataCtor
_ctor@(DataCtor Located Symbol
_c [Symbol]
as [RType BTyCon BTyVar RReft]
_ [(Symbol, RType BTyCon BTyVar RReft)]
xts Maybe (RType BTyCon BTyVar RReft)
res) DataCon
c' =
DataConP
{ dcpLoc :: SourcePos
dcpLoc = SourcePos
l
, dcpCon :: DataCon
dcpCon = DataCon
c'
, dcpFreeTyVars :: [RTyVar]
dcpFreeTyVars = Symbol -> RTyVar
RT.symbolRTyVar (Symbol -> RTyVar) -> [Symbol] -> [RTyVar]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol]
as
, dcpFreePred :: [RPVar]
dcpFreePred = [RPVar]
πs
, dcpTyConstrs :: [SpecType]
dcpTyConstrs = [SpecType]
cs
, dcpTyArgs :: [(Symbol, SpecType)]
dcpTyArgs = [(Symbol, SpecType)]
zts
, dcpTyRes :: SpecType
dcpTyRes = SpecType
ot
, dcpIsGadt :: Bool
dcpIsGadt = Bool
isGadt
, dcpModule :: Symbol
dcpModule = ModName -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol ModName
name
, dcpLocE :: SourcePos
dcpLocE = SourcePos
l'
}
where
ts' :: [SpecType]
ts' = Env
-> ModName
-> SourcePos
-> Maybe [PVar BSort]
-> RType BTyCon BTyVar RReft
-> SpecType
Bare.ofBareType Env
env ModName
name SourcePos
l ([PVar BSort] -> Maybe [PVar BSort]
forall a. a -> Maybe a
Just [PVar BSort]
ps) (RType BTyCon BTyVar RReft -> SpecType)
-> [RType BTyCon BTyVar RReft] -> [SpecType]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RType BTyCon BTyVar RReft]
ts
res' :: Maybe SpecType
res' = Env
-> ModName
-> SourcePos
-> Maybe [PVar BSort]
-> RType BTyCon BTyVar RReft
-> SpecType
Bare.ofBareType Env
env ModName
name SourcePos
l ([PVar BSort] -> Maybe [PVar BSort]
forall a. a -> Maybe a
Just [PVar BSort]
ps) (RType BTyCon BTyVar RReft -> SpecType)
-> Maybe (RType BTyCon BTyVar RReft) -> Maybe SpecType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (RType BTyCon BTyVar RReft)
res
t0' :: SpecType
t0' = DataCon -> [RTyVar] -> SpecType -> Maybe SpecType -> SpecType
dataConResultTy DataCon
c' [RTyVar]
αs SpecType
t0 Maybe SpecType
res'
_cfg :: Config
_cfg = Env -> Config
forall t. HasConfig t => t -> Config
getConfig Env
env
([(Symbol, SpecType)]
yts, SpecType
ot) = Bool
-> ModName
-> Located ()
-> ([(Symbol, SpecType)], SpecType)
-> ([(Symbol, SpecType)], SpecType)
forall a.
Bool
-> ModName
-> Located a
-> ([(Symbol, SpecType)], SpecType)
-> ([(Symbol, SpecType)], SpecType)
qualifyDataCtor (Bool -> Bool
not Bool
isGadt) ModName
name Located ()
dLoc ([Symbol] -> [SpecType] -> [(Symbol, SpecType)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
xs [SpecType]
ts', SpecType
t0')
zts :: [(Symbol, SpecType)]
zts = (Int -> (Symbol, SpecType) -> (Symbol, SpecType))
-> [Int] -> [(Symbol, SpecType)] -> [(Symbol, SpecType)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (DataCon -> Int -> (Symbol, SpecType) -> (Symbol, SpecType)
forall a. DataCon -> Int -> (Symbol, a) -> (Symbol, a)
normalizeField DataCon
c') [Int
1..] ([(Symbol, SpecType)] -> [(Symbol, SpecType)]
forall a. [a] -> [a]
reverse [(Symbol, SpecType)]
yts)
usedTvs :: HashSet RTyVar
usedTvs = [RTyVar] -> HashSet RTyVar
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList (RTVar RTyVar (RType RTyCon RTyVar ()) -> RTyVar
forall tv s. RTVar tv s -> tv
ty_var_value (RTVar RTyVar (RType RTyCon RTyVar ()) -> RTyVar)
-> [RTVar RTyVar (RType RTyCon RTyVar ())] -> [RTyVar]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (SpecType -> [RTVar RTyVar (RType RTyCon RTyVar ())])
-> [SpecType] -> [RTVar RTyVar (RType RTyCon RTyVar ())]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap SpecType -> [RTVar RTyVar (RType RTyCon RTyVar ())]
forall tv c r. Eq tv => RType c tv r -> [RTVar tv (RType c tv ())]
RT.freeTyVars (SpecType
t0'SpecType -> [SpecType] -> [SpecType]
forall a. a -> [a] -> [a]
:[SpecType]
ts'))
cs :: [SpecType]
cs = [ SpecType
p | SpecType
p <- Type -> SpecType
forall r. Monoid r => Type -> RRType r
RT.ofType (Type -> SpecType) -> [Type] -> [SpecType]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DataCon -> [Type]
Ghc.dataConTheta DataCon
c', HashSet RTyVar -> SpecType -> Bool
keepPredType HashSet RTyVar
usedTvs SpecType
p ]
([Symbol]
xs, [RType BTyCon BTyVar RReft]
ts) = [(Symbol, RType BTyCon BTyVar RReft)]
-> ([Symbol], [RType BTyCon BTyVar RReft])
forall a b. [(a, b)] -> ([a], [b])
unzip [(Symbol, RType BTyCon BTyVar RReft)]
xts
t0 :: SpecType
t0 = case TyCon -> Maybe Type
RT.famInstTyConType TyCon
tc of
Maybe Type
Nothing -> TyCon -> [RTyVar] -> [RPVar] -> SpecType
forall a. TyCon -> [RTyVar] -> [PVar a] -> SpecType
RT.gApp TyCon
tc [RTyVar]
αs [RPVar]
πs
Just Type
ty -> Type -> SpecType
forall r. Monoid r => Type -> RRType r
RT.ofType Type
ty
isGadt :: Bool
isGadt = Maybe (RType BTyCon BTyVar RReft) -> Bool
forall a. Maybe a -> Bool
Mb.isJust Maybe (RType BTyCon BTyVar RReft)
res
dLoc :: Located ()
dLoc = SourcePos -> SourcePos -> () -> Located ()
forall a. SourcePos -> SourcePos -> a -> Located a
F.Loc SourcePos
l SourcePos
l' ()
errDataConMismatch :: LocSymbol -> S.HashSet F.Symbol -> S.HashSet F.Symbol -> Error
errDataConMismatch :: Located Symbol -> HashSet Symbol -> HashSet Symbol -> Error
errDataConMismatch Located Symbol
d HashSet Symbol
dcs HashSet Symbol
rdcs = SrcSpan -> Doc -> [Doc] -> [Doc] -> Error
forall t. SrcSpan -> Doc -> [Doc] -> [Doc] -> TError t
ErrDataConMismatch SrcSpan
sp Doc
v (Symbol -> Doc
forall a. PPrint a => a -> Doc
ppTicks (Symbol -> Doc) -> [Symbol] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HashSet Symbol -> [Symbol]
forall a. HashSet a -> [a]
S.toList HashSet Symbol
dcs) (Symbol -> Doc
forall a. PPrint a => a -> Doc
ppTicks (Symbol -> Doc) -> [Symbol] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HashSet Symbol -> [Symbol]
forall a. HashSet a -> [a]
S.toList HashSet Symbol
rdcs)
where
v :: Doc
v = Symbol -> Doc
forall a. PPrint a => a -> Doc
pprint (Located Symbol -> Symbol
forall a. Located a -> a
val Located Symbol
d)
sp :: SrcSpan
sp = SourcePos -> SrcSpan
GM.sourcePosSrcSpan (Located Symbol -> SourcePos
forall a. Located a -> SourcePos
loc Located Symbol
d)
varSignToVariance :: Eq a => [(a, Bool)] -> a -> Variance
varSignToVariance :: forall a. Eq a => [(a, Bool)] -> a -> Variance
varSignToVariance [(a, Bool)]
varsigns a
i = case ((a, Bool) -> Bool) -> [(a, Bool)] -> [(a, Bool)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\(a, Bool)
p -> (a, Bool) -> a
forall a b. (a, b) -> a
fst (a, Bool)
p a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
i) [(a, Bool)]
varsigns of
[] -> Variance
Invariant
[(a
_, Bool
b)] -> if Bool
b then Variance
Covariant else Variance
Contravariant
[(a, Bool)]
_ -> Variance
Bivariant
getPsSig :: [(UsedPVar, a)] -> Bool -> SpecType -> [(a, Bool)]
getPsSig :: forall a. [(UsedPVar, a)] -> Bool -> SpecType -> [(a, Bool)]
getPsSig [(UsedPVar, a)]
m Bool
pos (RAllT RTVar RTyVar (RType RTyCon RTyVar ())
_ SpecType
t RReft
r)
= [(UsedPVar, a)] -> Bool -> RReft -> [(a, Bool)]
forall a b t. [(UsedPVar, a)] -> b -> UReft t -> [(a, b)]
addps [(UsedPVar, a)]
m Bool
pos RReft
r [(a, Bool)] -> [(a, Bool)] -> [(a, Bool)]
forall a. [a] -> [a] -> [a]
++ [(UsedPVar, a)] -> Bool -> SpecType -> [(a, Bool)]
forall a. [(UsedPVar, a)] -> Bool -> SpecType -> [(a, Bool)]
getPsSig [(UsedPVar, a)]
m Bool
pos SpecType
t
getPsSig [(UsedPVar, a)]
m Bool
pos (RApp RTyCon
_ [SpecType]
ts [RTProp RTyCon RTyVar RReft]
rs RReft
r)
= [(UsedPVar, a)] -> Bool -> RReft -> [(a, Bool)]
forall a b t. [(UsedPVar, a)] -> b -> UReft t -> [(a, b)]
addps [(UsedPVar, a)]
m Bool
pos RReft
r [(a, Bool)] -> [(a, Bool)] -> [(a, Bool)]
forall a. [a] -> [a] -> [a]
++ (SpecType -> [(a, Bool)]) -> [SpecType] -> [(a, Bool)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ([(UsedPVar, a)] -> Bool -> SpecType -> [(a, Bool)]
forall a. [(UsedPVar, a)] -> Bool -> SpecType -> [(a, Bool)]
getPsSig [(UsedPVar, a)]
m Bool
pos) [SpecType]
ts
[(a, Bool)] -> [(a, Bool)] -> [(a, Bool)]
forall a. [a] -> [a] -> [a]
++ (RTProp RTyCon RTyVar RReft -> [(a, Bool)])
-> [RTProp RTyCon RTyVar RReft] -> [(a, Bool)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ([(UsedPVar, a)]
-> Bool -> RTProp RTyCon RTyVar RReft -> [(a, Bool)]
forall a.
[(UsedPVar, a)]
-> Bool -> RTProp RTyCon RTyVar RReft -> [(a, Bool)]
getPsSigPs [(UsedPVar, a)]
m Bool
pos) [RTProp RTyCon RTyVar RReft]
rs
getPsSig [(UsedPVar, a)]
m Bool
pos (RVar RTyVar
_ RReft
r)
= [(UsedPVar, a)] -> Bool -> RReft -> [(a, Bool)]
forall a b t. [(UsedPVar, a)] -> b -> UReft t -> [(a, b)]
addps [(UsedPVar, a)]
m Bool
pos RReft
r
getPsSig [(UsedPVar, a)]
m Bool
pos (RAppTy SpecType
t1 SpecType
t2 RReft
r)
= [(UsedPVar, a)] -> Bool -> RReft -> [(a, Bool)]
forall a b t. [(UsedPVar, a)] -> b -> UReft t -> [(a, b)]
addps [(UsedPVar, a)]
m Bool
pos RReft
r [(a, Bool)] -> [(a, Bool)] -> [(a, Bool)]
forall a. [a] -> [a] -> [a]
++ [(UsedPVar, a)] -> Bool -> SpecType -> [(a, Bool)]
forall a. [(UsedPVar, a)] -> Bool -> SpecType -> [(a, Bool)]
getPsSig [(UsedPVar, a)]
m Bool
pos SpecType
t1 [(a, Bool)] -> [(a, Bool)] -> [(a, Bool)]
forall a. [a] -> [a] -> [a]
++ [(UsedPVar, a)] -> Bool -> SpecType -> [(a, Bool)]
forall a. [(UsedPVar, a)] -> Bool -> SpecType -> [(a, Bool)]
getPsSig [(UsedPVar, a)]
m Bool
pos SpecType
t2
getPsSig [(UsedPVar, a)]
m Bool
pos (RFun Symbol
_ RFInfo
_ SpecType
t1 SpecType
t2 RReft
r)
= [(UsedPVar, a)] -> Bool -> RReft -> [(a, Bool)]
forall a b t. [(UsedPVar, a)] -> b -> UReft t -> [(a, b)]
addps [(UsedPVar, a)]
m Bool
pos RReft
r [(a, Bool)] -> [(a, Bool)] -> [(a, Bool)]
forall a. [a] -> [a] -> [a]
++ [(UsedPVar, a)] -> Bool -> SpecType -> [(a, Bool)]
forall a. [(UsedPVar, a)] -> Bool -> SpecType -> [(a, Bool)]
getPsSig [(UsedPVar, a)]
m Bool
pos SpecType
t2 [(a, Bool)] -> [(a, Bool)] -> [(a, Bool)]
forall a. [a] -> [a] -> [a]
++ [(UsedPVar, a)] -> Bool -> SpecType -> [(a, Bool)]
forall a. [(UsedPVar, a)] -> Bool -> SpecType -> [(a, Bool)]
getPsSig [(UsedPVar, a)]
m (Bool -> Bool
not Bool
pos) SpecType
t1
getPsSig [(UsedPVar, a)]
m Bool
pos (RHole RReft
r)
= [(UsedPVar, a)] -> Bool -> RReft -> [(a, Bool)]
forall a b t. [(UsedPVar, a)] -> b -> UReft t -> [(a, b)]
addps [(UsedPVar, a)]
m Bool
pos RReft
r
getPsSig [(UsedPVar, a)]
_ Bool
_ SpecType
z
= Maybe SrcSpan -> [Char] -> [(a, Bool)]
forall a. Maybe SrcSpan -> [Char] -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing ([Char] -> [(a, Bool)]) -> [Char] -> [(a, Bool)]
forall a b. (a -> b) -> a -> b
$ [Char]
"getPsSig" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ SpecType -> [Char]
forall a. Show a => a -> [Char]
show SpecType
z
getPsSigPs :: [(UsedPVar, a)] -> Bool -> SpecProp -> [(a, Bool)]
getPsSigPs :: forall a.
[(UsedPVar, a)]
-> Bool -> RTProp RTyCon RTyVar RReft -> [(a, Bool)]
getPsSigPs [(UsedPVar, a)]
m Bool
pos (RProp [(Symbol, RType RTyCon RTyVar ())]
_ (RHole RReft
r)) = [(UsedPVar, a)] -> Bool -> RReft -> [(a, Bool)]
forall a b t. [(UsedPVar, a)] -> b -> UReft t -> [(a, b)]
addps [(UsedPVar, a)]
m Bool
pos RReft
r
getPsSigPs [(UsedPVar, a)]
m Bool
pos (RProp [(Symbol, RType RTyCon RTyVar ())]
_ SpecType
t) = [(UsedPVar, a)] -> Bool -> SpecType -> [(a, Bool)]
forall a. [(UsedPVar, a)] -> Bool -> SpecType -> [(a, Bool)]
getPsSig [(UsedPVar, a)]
m Bool
pos SpecType
t
addps :: [(UsedPVar, a)] -> b -> UReft t -> [(a, b)]
addps :: forall a b t. [(UsedPVar, a)] -> b -> UReft t -> [(a, b)]
addps [(UsedPVar, a)]
m b
pos (MkUReft t
_ Predicate
ps) = (, b
pos) (a -> (a, b)) -> (UsedPVar -> a) -> UsedPVar -> (a, b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UsedPVar -> a
forall {t}. PVar t -> a
f (UsedPVar -> (a, b)) -> [UsedPVar] -> [(a, b)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Predicate -> [UsedPVar]
pvars Predicate
ps
where
f :: PVar t -> a
f = a -> Maybe a -> a
forall a. a -> Maybe a -> a
Mb.fromMaybe (Maybe SrcSpan -> [Char] -> a
forall a. Maybe SrcSpan -> [Char] -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing [Char]
"Bare.addPs: notfound") (Maybe a -> a) -> (PVar t -> Maybe a) -> PVar t -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (UsedPVar -> [(UsedPVar, a)] -> Maybe a
forall a b. Eq a => a -> [(a, b)] -> Maybe b
`L.lookup` [(UsedPVar, a)]
m) (UsedPVar -> Maybe a) -> (PVar t -> UsedPVar) -> PVar t -> Maybe a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PVar t -> UsedPVar
forall t. PVar t -> UsedPVar
RT.uPVar
keepPredType :: S.HashSet RTyVar -> SpecType -> Bool
keepPredType :: HashSet RTyVar -> SpecType -> Bool
keepPredType HashSet RTyVar
tvs SpecType
p
| Just (RTyVar
tv, SpecType
_) <- SpecType -> Maybe (RTyVar, SpecType)
eqSubst SpecType
p = RTyVar -> HashSet RTyVar -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
S.member RTyVar
tv HashSet RTyVar
tvs
| Bool
otherwise = Bool
True
dataConResultTy :: Ghc.DataCon
-> [RTyVar]
-> SpecType
-> Maybe SpecType
-> SpecType
dataConResultTy :: DataCon -> [RTyVar] -> SpecType -> Maybe SpecType -> SpecType
dataConResultTy DataCon
c [RTyVar]
_ SpecType
_ (Just SpecType
t) = [Char] -> SpecType -> SpecType
forall a. PPrint a => [Char] -> a -> a
F.notracepp ([Char]
"dataConResultTy-3 : vanilla = " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Bool -> [Char]
forall a. Show a => a -> [Char]
show (DataCon -> Bool
Ghc.isVanillaDataCon DataCon
c) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" : ") SpecType
t
dataConResultTy DataCon
c [RTyVar]
_ SpecType
t Maybe SpecType
_
| DataCon -> Bool
Ghc.isVanillaDataCon DataCon
c = [Char] -> SpecType -> SpecType
forall a. PPrint a => [Char] -> a -> a
F.notracepp ([Char]
"dataConResultTy-1 : " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ DataCon -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp DataCon
c) SpecType
t
| Bool
otherwise = [Char] -> SpecType -> SpecType
forall a. PPrint a => [Char] -> a -> a
F.notracepp ([Char]
"dataConResultTy-2 : " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ DataCon -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp DataCon
c) (SpecType -> SpecType) -> SpecType -> SpecType
forall a b. (a -> b) -> a -> b
$ Type -> SpecType
forall r. Monoid r => Type -> RRType r
RT.ofType Type
ct
where
([Var]
_,[Var]
_,[EqSpec]
_,[Type]
_,[Scaled Type]
_,Type
ct) = DataCon -> ([Var], [Var], [EqSpec], [Type], [Scaled Type], Type)
Ghc.dataConFullSig DataCon
c
eqSubst :: SpecType -> Maybe (RTyVar, SpecType)
eqSubst :: SpecType -> Maybe (RTyVar, SpecType)
eqSubst (RApp RTyCon
c [SpecType
_, SpecType
_, RVar RTyVar
a RReft
_, SpecType
t] [RTProp RTyCon RTyVar RReft]
_ RReft
_)
| RTyCon -> TyCon
rtc_tc RTyCon
c TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
Ghc.eqPrimTyCon = (RTyVar, SpecType) -> Maybe (RTyVar, SpecType)
forall a. a -> Maybe a
Just (RTyVar
a, SpecType
t)
eqSubst SpecType
_ = Maybe (RTyVar, SpecType)
forall a. Maybe a
Nothing
normalizeField :: Ghc.DataCon -> Int -> (F.Symbol, a) -> (F.Symbol, a)
normalizeField :: forall a. DataCon -> Int -> (Symbol, a) -> (Symbol, a)
normalizeField DataCon
c Int
i (Symbol
x, a
t)
| Symbol -> Bool
isTmp Symbol
x = (Symbol
xi, a
t)
| Bool
otherwise = (Symbol
x , a
t)
where
isTmp :: Symbol -> Bool
isTmp = Symbol -> Symbol -> Bool
F.isPrefixOfSym Symbol
F.tempPrefix
xi :: Symbol
xi = Maybe DataConMap -> DataCon -> Int -> Symbol
makeDataConSelector Maybe DataConMap
forall a. Maybe a
Nothing DataCon
c Int
i
type CtorType = ([(F.Symbol, SpecType)], SpecType)
qualifyDataCtor :: Bool -> ModName -> F.Located a -> CtorType -> CtorType
qualifyDataCtor :: forall a.
Bool
-> ModName
-> Located a
-> ([(Symbol, SpecType)], SpecType)
-> ([(Symbol, SpecType)], SpecType)
qualifyDataCtor Bool
qualFlag ModName
name Located a
l ct :: ([(Symbol, SpecType)], SpecType)
ct@([(Symbol, SpecType)]
xts, SpecType
st)
| Bool
qualFlag = ([(Symbol, SpecType)]
xts', SpecType
t')
| Bool
otherwise = ([(Symbol, SpecType)], SpecType)
ct
where
t' :: SpecType
t' = Subst -> RReft -> RReft
forall a. Subable a => Subst -> a -> a
F.subst Subst
su (RReft -> RReft) -> SpecType -> SpecType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SpecType
st
xts' :: [(Symbol, SpecType)]
xts' = [ (Symbol
qx, Subst -> SpecType -> SpecType
forall a. Subable a => Subst -> a -> a
F.subst Subst
su SpecType
t) | (Symbol
qx, SpecType
t, Maybe Symbol
_) <- [(Symbol, SpecType, Maybe Symbol)]
fields ]
su :: Subst
su = [(Symbol, Expr)] -> Subst
F.mkSubst [ (Symbol
x, Symbol -> Expr
forall a. Symbolic a => a -> Expr
F.eVar Symbol
qx) | (Symbol
qx, SpecType
_, Just Symbol
x) <- [(Symbol, SpecType, Maybe Symbol)]
fields ]
fields :: [(Symbol, SpecType, Maybe Symbol)]
fields = [ (Symbol
qx, SpecType
t, Maybe Symbol
mbX) | (Symbol
x, SpecType
t) <- [(Symbol, SpecType)]
xts, let (Maybe Symbol
mbX, Symbol
qx) = ModName -> Located Symbol -> (Maybe Symbol, Symbol)
qualifyField ModName
name (Located a -> Symbol -> Located Symbol
forall l b. Loc l => l -> b -> Located b
F.atLoc Located a
l Symbol
x) ]
qualifyField :: ModName -> LocSymbol -> (Maybe F.Symbol, F.Symbol)
qualifyField :: ModName -> Located Symbol -> (Maybe Symbol, Symbol)
qualifyField ModName
name Located Symbol
lx
| Bool
needsQual = (Symbol -> Maybe Symbol
forall a. a -> Maybe a
Just Symbol
x, [Char] -> Symbol -> Symbol
forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
msg (Symbol -> Symbol) -> Symbol -> Symbol
forall a b. (a -> b) -> a -> b
$ ModName -> Symbol -> Symbol
qualifyModName ModName
name Symbol
x)
| Bool
otherwise = (Maybe Symbol
forall a. Maybe a
Nothing, Symbol
x)
where
msg :: [Char]
msg = [Char]
"QUALIFY-NAME: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Symbol -> [Char]
forall a. Show a => a -> [Char]
show Symbol
x [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" in module " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Symbol -> [Char]
forall a. Show a => a -> [Char]
show (ModName -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol ModName
name)
x :: Symbol
x = Located Symbol -> Symbol
forall a. Located a -> a
val Located Symbol
lx
needsQual :: Bool
needsQual = Bool -> Bool
not (Located Symbol -> Bool
isWiredIn Located Symbol
lx)
checkRecordSelectorSigs :: [(Ghc.Var, LocSpecType)] -> [(Ghc.Var, LocSpecType)]
checkRecordSelectorSigs :: [(Var, LocSpecType)] -> [(Var, LocSpecType)]
checkRecordSelectorSigs [(Var, LocSpecType)]
vts = [ (Var
v, Var -> [LocSpecType] -> LocSpecType
forall {b} {a}.
(PPrint b, PPrint a) =>
a -> [Located b] -> Located b
take1 Var
v [LocSpecType]
lspecTys) | (Var
v, [LocSpecType]
lspecTys) <- [(Var, LocSpecType)] -> [(Var, [LocSpecType])]
forall k v. (Eq k, Hashable k) => [(k, v)] -> [(k, [v])]
Misc.groupList [(Var, LocSpecType)]
vts ]
where
take1 :: a -> [Located b] -> Located b
take1 a
v [Located b]
lsts = case (Located b -> [Char]) -> [Located b] -> [Located b]
forall k a. (Eq k, Hashable k) => (a -> k) -> [a] -> [a]
Misc.nubHashOn (b -> [Char]
forall a. PPrint a => a -> [Char]
showpp (b -> [Char]) -> (Located b -> b) -> Located b -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Located b -> b
forall a. Located a -> a
val) [Located b]
lsts of
[Located b
t] -> Located b
t
(Located b
t:[Located b]
ts) -> Error -> Located b
forall a e. Exception e => e -> a
Ex.throw (SrcSpan -> Doc -> ListNE SrcSpan -> Error
forall t. SrcSpan -> Doc -> ListNE SrcSpan -> TError t
ErrDupSpecs (Located b -> SrcSpan
forall a. Loc a => a -> SrcSpan
GM.fSrcSpan Located b
t) (a -> Doc
forall a. PPrint a => a -> Doc
pprint a
v) (Located b -> SrcSpan
forall a. Loc a => a -> SrcSpan
GM.fSrcSpan (Located b -> SrcSpan) -> [Located b] -> ListNE SrcSpan
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Located b]
ts) :: Error)
[Located b]
_ -> Maybe SrcSpan -> [Char] -> Located b
forall a. Maybe SrcSpan -> [Char] -> a
impossible Maybe SrcSpan
forall a. Maybe a
Nothing [Char]
"checkRecordSelectorSigs"
strengthenClassSel :: Ghc.Var -> LocSpecType -> LocSpecType
strengthenClassSel :: Var -> LocSpecType -> LocSpecType
strengthenClassSel Var
v LocSpecType
lt = LocSpecType
lt { val = st }
where
st :: SpecType
st = Reader (Int, [Symbol]) SpecType -> (Int, [Symbol]) -> SpecType
forall r a. Reader r a -> r -> a
runReader (SpecType -> Reader (Int, [Symbol]) SpecType
go (LocSpecType -> SpecType
forall a. Located a -> a
F.val LocSpecType
lt)) (Int
1, [])
s :: Located Symbol
s = Var -> Located Symbol
forall a. (Symbolic a, NamedThing a) => a -> Located Symbol
GM.namedLocSymbol Var
v
extend :: F.Symbol -> (Int, [F.Symbol]) -> (Int, [F.Symbol])
extend :: Symbol -> (Int, [Symbol]) -> (Int, [Symbol])
extend Symbol
x (Int
i, [Symbol]
xs) = (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1, Symbol
x Symbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
: [Symbol]
xs)
go :: SpecType -> Reader (Int, [F.Symbol]) SpecType
go :: SpecType -> Reader (Int, [Symbol]) SpecType
go (RAllT RTVar RTyVar (RType RTyCon RTyVar ())
a SpecType
t RReft
r) = RTVar RTyVar (RType RTyCon RTyVar ())
-> SpecType -> RReft -> SpecType
forall c tv r. RTVU c tv -> RType c tv r -> r -> RType c tv r
RAllT RTVar RTyVar (RType RTyCon RTyVar ())
a (SpecType -> RReft -> SpecType)
-> Reader (Int, [Symbol]) SpecType
-> ReaderT (Int, [Symbol]) Identity (RReft -> SpecType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SpecType -> Reader (Int, [Symbol]) SpecType
go SpecType
t ReaderT (Int, [Symbol]) Identity (RReft -> SpecType)
-> ReaderT (Int, [Symbol]) Identity RReft
-> Reader (Int, [Symbol]) SpecType
forall a b.
ReaderT (Int, [Symbol]) Identity (a -> b)
-> ReaderT (Int, [Symbol]) Identity a
-> ReaderT (Int, [Symbol]) Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> RReft -> ReaderT (Int, [Symbol]) Identity RReft
forall a. a -> ReaderT (Int, [Symbol]) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure RReft
r
go (RAllP RPVar
p SpecType
t ) = RPVar -> SpecType -> SpecType
forall c tv r. PVU c tv -> RType c tv r -> RType c tv r
RAllP RPVar
p (SpecType -> SpecType)
-> Reader (Int, [Symbol]) SpecType
-> Reader (Int, [Symbol]) SpecType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SpecType -> Reader (Int, [Symbol]) SpecType
go SpecType
t
go (RFun Symbol
x RFInfo
i SpecType
tx SpecType
t RReft
r) | SpecType -> Bool
forall c t t1. TyConable c => RType c t t1 -> Bool
isEmbeddedClass SpecType
tx =
Symbol -> RFInfo -> SpecType -> SpecType -> RReft -> SpecType
forall c tv r.
Symbol
-> RFInfo -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun Symbol
x RFInfo
i SpecType
tx (SpecType -> RReft -> SpecType)
-> Reader (Int, [Symbol]) SpecType
-> ReaderT (Int, [Symbol]) Identity (RReft -> SpecType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SpecType -> Reader (Int, [Symbol]) SpecType
go SpecType
t ReaderT (Int, [Symbol]) Identity (RReft -> SpecType)
-> ReaderT (Int, [Symbol]) Identity RReft
-> Reader (Int, [Symbol]) SpecType
forall a b.
ReaderT (Int, [Symbol]) Identity (a -> b)
-> ReaderT (Int, [Symbol]) Identity a
-> ReaderT (Int, [Symbol]) Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> RReft -> ReaderT (Int, [Symbol]) Identity RReft
forall a. a -> ReaderT (Int, [Symbol]) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure RReft
r
go (RFun Symbol
x RFInfo
i SpecType
tx SpecType
t RReft
r) = do
Symbol
x' <- Symbol -> Int -> Symbol
unDummy Symbol
x (Int -> Symbol)
-> ReaderT (Int, [Symbol]) Identity Int
-> ReaderT (Int, [Symbol]) Identity Symbol
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Int, [Symbol]) -> Int) -> ReaderT (Int, [Symbol]) Identity Int
forall a.
((Int, [Symbol]) -> a) -> ReaderT (Int, [Symbol]) Identity a
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
reader (Int, [Symbol]) -> Int
forall a b. (a, b) -> a
fst
RReft
r' <- Located Symbol -> [Symbol] -> RReft
forall a. Symbolic a => Located Symbol -> [a] -> RReft
singletonApp Located Symbol
s ([Symbol] -> RReft)
-> ReaderT (Int, [Symbol]) Identity [Symbol]
-> ReaderT (Int, [Symbol]) Identity RReft
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([Symbol] -> [Symbol]
forall a. [a] -> [a]
L.reverse ([Symbol] -> [Symbol])
-> ReaderT (Int, [Symbol]) Identity [Symbol]
-> ReaderT (Int, [Symbol]) Identity [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Int, [Symbol]) -> [Symbol])
-> ReaderT (Int, [Symbol]) Identity [Symbol]
forall a.
((Int, [Symbol]) -> a) -> ReaderT (Int, [Symbol]) Identity a
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
reader (Int, [Symbol]) -> [Symbol]
forall a b. (a, b) -> b
snd)
Symbol -> RFInfo -> SpecType -> SpecType -> RReft -> SpecType
forall c tv r.
Symbol
-> RFInfo -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun Symbol
x' RFInfo
i SpecType
tx (SpecType -> RReft -> SpecType)
-> Reader (Int, [Symbol]) SpecType
-> ReaderT (Int, [Symbol]) Identity (RReft -> SpecType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Int, [Symbol]) -> (Int, [Symbol]))
-> Reader (Int, [Symbol]) SpecType
-> Reader (Int, [Symbol]) SpecType
forall a.
((Int, [Symbol]) -> (Int, [Symbol]))
-> ReaderT (Int, [Symbol]) Identity a
-> ReaderT (Int, [Symbol]) Identity a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (Symbol -> (Int, [Symbol]) -> (Int, [Symbol])
extend Symbol
x') (SpecType -> Reader (Int, [Symbol]) SpecType
go SpecType
t) ReaderT (Int, [Symbol]) Identity (RReft -> SpecType)
-> ReaderT (Int, [Symbol]) Identity RReft
-> Reader (Int, [Symbol]) SpecType
forall a b.
ReaderT (Int, [Symbol]) Identity (a -> b)
-> ReaderT (Int, [Symbol]) Identity a
-> ReaderT (Int, [Symbol]) Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> RReft -> ReaderT (Int, [Symbol]) Identity RReft
forall a. a -> ReaderT (Int, [Symbol]) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (RReft -> RReft -> RReft
forall r. Reftable r => r -> r -> r
F.meet RReft
r RReft
r')
go SpecType
t = SpecType -> RReft -> SpecType
forall r c tv. Reftable r => RType c tv r -> r -> RType c tv r
RT.strengthen SpecType
t (RReft -> SpecType) -> ([Symbol] -> RReft) -> [Symbol] -> SpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Located Symbol -> [Symbol] -> RReft
forall a. Symbolic a => Located Symbol -> [a] -> RReft
singletonApp Located Symbol
s ([Symbol] -> RReft) -> ([Symbol] -> [Symbol]) -> [Symbol] -> RReft
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Symbol] -> [Symbol]
forall a. [a] -> [a]
L.reverse ([Symbol] -> SpecType)
-> ReaderT (Int, [Symbol]) Identity [Symbol]
-> Reader (Int, [Symbol]) SpecType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Int, [Symbol]) -> [Symbol])
-> ReaderT (Int, [Symbol]) Identity [Symbol]
forall a.
((Int, [Symbol]) -> a) -> ReaderT (Int, [Symbol]) Identity a
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
reader (Int, [Symbol]) -> [Symbol]
forall a b. (a, b) -> b
snd
singletonApp :: F.Symbolic a => F.LocSymbol -> [a] -> UReft F.Reft
singletonApp :: forall a. Symbolic a => Located Symbol -> [a] -> RReft
singletonApp Located Symbol
s [a]
ys = Reft -> Predicate -> RReft
forall r. r -> Predicate -> UReft r
MkUReft Reft
r Predicate
forall a. Monoid a => a
mempty
where r :: Reft
r = Expr -> Reft
forall a. Expression a => a -> Reft
F.exprReft (Located Symbol -> [Expr] -> Expr
F.mkEApp Located Symbol
s (a -> Expr
forall a. Symbolic a => a -> Expr
F.eVar (a -> Expr) -> [a] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [a]
ys))
unDummy :: F.Symbol -> Int -> F.Symbol
unDummy :: Symbol -> Int -> Symbol
unDummy Symbol
x Int
i | Symbol
x Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
/= Symbol
F.dummySymbol = Symbol
x
| Bool
otherwise = [Char] -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol ([Char]
"_cls_lq" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show Int
i)
makeRecordSelectorSigs :: Bare.Env -> ModName -> [Located DataConP] -> [(Ghc.Var, LocSpecType)]
makeRecordSelectorSigs :: Env -> ModName -> [Located DataConP] -> [(Var, LocSpecType)]
makeRecordSelectorSigs Env
env ModName
name = [(Var, LocSpecType)] -> [(Var, LocSpecType)]
checkRecordSelectorSigs ([(Var, LocSpecType)] -> [(Var, LocSpecType)])
-> ([Located DataConP] -> [(Var, LocSpecType)])
-> [Located DataConP]
-> [(Var, LocSpecType)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Located DataConP -> [(Var, LocSpecType)])
-> [Located DataConP] -> [(Var, LocSpecType)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Located DataConP -> [(Var, LocSpecType)]
makeOne
where
makeOne :: Located DataConP -> [(Var, LocSpecType)]
makeOne (Loc SourcePos
l SourcePos
l' DataConP
dcp)
| Just Class
cls <- Maybe Class
maybe_cls
= let cfs :: [Var]
cfs = Class -> [Var]
Ghc.classAllSelIds Class
cls in
((Var, LocSpecType) -> (Var, LocSpecType))
-> [(Var, LocSpecType)] -> [(Var, LocSpecType)]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((,) (Var -> LocSpecType -> (Var, LocSpecType))
-> ((Var, LocSpecType) -> Var)
-> (Var, LocSpecType)
-> LocSpecType
-> (Var, LocSpecType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Var, LocSpecType) -> Var
forall a b. (a, b) -> a
fst ((Var, LocSpecType) -> LocSpecType -> (Var, LocSpecType))
-> ((Var, LocSpecType) -> LocSpecType)
-> (Var, LocSpecType)
-> (Var, LocSpecType)
forall a b.
((Var, LocSpecType) -> a -> b)
-> ((Var, LocSpecType) -> a) -> (Var, LocSpecType) -> b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Var -> LocSpecType -> LocSpecType)
-> (Var, LocSpecType) -> LocSpecType
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Var -> LocSpecType -> LocSpecType
strengthenClassSel)
[(Var
v, SourcePos -> SourcePos -> SpecType -> LocSpecType
forall a. SourcePos -> SourcePos -> a -> Located a
Loc SourcePos
l SourcePos
l' SpecType
t)| (Var
v,SpecType
t) <- [Var] -> [SpecType] -> [(Var, SpecType)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Var]
cfs ([SpecType] -> [SpecType]
forall a. [a] -> [a]
reverse ([SpecType] -> [SpecType]) -> [SpecType] -> [SpecType]
forall a b. (a -> b) -> a -> b
$ ((Symbol, SpecType) -> SpecType)
-> [(Symbol, SpecType)] -> [SpecType]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Symbol, SpecType) -> SpecType
forall a b. (a, b) -> b
snd [(Symbol, SpecType)]
args)]
| [FieldLabel] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [FieldLabel]
fls
Bool -> Bool -> Bool
|| ((Symbol, SpecType) -> Bool) -> [(Symbol, SpecType)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (SpecType -> Bool
forall t t1 t2. RType t t1 t2 -> Bool
isFunTy (SpecType -> Bool)
-> ((Symbol, SpecType) -> SpecType) -> (Symbol, SpecType) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol, SpecType) -> SpecType
forall a b. (a, b) -> b
snd) [(Symbol, SpecType)]
args Bool -> Bool -> Bool
&& Bool -> Bool
not (Env -> Bool
forall t. HasConfig t => t -> Bool
higherOrderFlag Env
env)
Bool -> Bool -> Bool
|| DataConP -> Bool
dcpIsGadt DataConP
dcp
= []
| Bool
otherwise
= [ (Var
v, LocSpecType
t) | (Just Var
v, LocSpecType
t) <- [Maybe Var] -> [LocSpecType] -> [(Maybe Var, LocSpecType)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Maybe Var]
fs [LocSpecType]
ts ]
where
maybe_cls :: Maybe Class
maybe_cls = TyCon -> Maybe Class
Ghc.tyConClass_maybe (DataCon -> TyCon
Ghc.dataConTyCon DataCon
dc)
dc :: DataCon
dc = DataConP -> DataCon
dcpCon DataConP
dcp
fls :: [FieldLabel]
fls = DataCon -> [FieldLabel]
Ghc.dataConFieldLabels DataCon
dc
fs :: [Maybe Var]
fs = Env -> ModName -> Name -> Maybe Var
forall a.
(NamedThing a, Symbolic a) =>
Env -> ModName -> a -> Maybe Var
Bare.lookupGhcNamedVar Env
env ModName
name (Name -> Maybe Var)
-> (FieldLabel -> Name) -> FieldLabel -> Maybe Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FieldLabel -> Name
Ghc.flSelector (FieldLabel -> Maybe Var) -> [FieldLabel] -> [Maybe Var]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [FieldLabel]
fls
ts :: [ LocSpecType ]
ts :: [LocSpecType]
ts = [ SourcePos -> SourcePos -> SpecType -> LocSpecType
forall a. SourcePos -> SourcePos -> a -> Located a
Loc SourcePos
l SourcePos
l' ([(RTVar RTyVar (RType RTyCon RTyVar ()), RReft)]
-> [RPVar]
-> [(Symbol, RFInfo, SpecType, RReft)]
-> SpecType
-> SpecType
forall tv c r.
[(RTVar tv (RType c tv ()), r)]
-> [PVar (RType c tv ())]
-> [(Symbol, RFInfo, RType c tv r, r)]
-> RType c tv r
-> RType c tv r
mkArrow ((RTVar RTyVar (RType RTyCon RTyVar ())
-> (RTVar RTyVar (RType RTyCon RTyVar ()), RReft))
-> [RTVar RTyVar (RType RTyCon RTyVar ())]
-> [(RTVar RTyVar (RType RTyCon RTyVar ()), RReft)]
forall a b. (a -> b) -> [a] -> [b]
map (, RReft
forall a. Monoid a => a
mempty) (RTyVar -> RTVar RTyVar (RType RTyCon RTyVar ())
forall tv s. tv -> RTVar tv s
makeRTVar (RTyVar -> RTVar RTyVar (RType RTyCon RTyVar ()))
-> [RTyVar] -> [RTVar RTyVar (RType RTyCon RTyVar ())]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DataConP -> [RTyVar]
dcpFreeTyVars DataConP
dcp)) []
[(Symbol
z, Bool -> RFInfo
classRFInfo Bool
True, SpecType
res, RReft
forall a. Monoid a => a
mempty)]
(SpecType -> SpecType
forall {r}.
RType RTyCon RTyVar (UReft r) -> RType RTyCon RTyVar (UReft r)
dropPreds (Subst -> SpecType -> SpecType
forall a. Subable a => Subst -> a -> a
F.subst Subst
su SpecType
t SpecType -> RReft -> SpecType
forall r c tv. Reftable r => RType c tv r -> r -> RType c tv r
`RT.strengthen` RReft
mt)))
| (Symbol
x, SpecType
t) <- [(Symbol, SpecType)] -> [(Symbol, SpecType)]
forall a. [a] -> [a]
reverse [(Symbol, SpecType)]
args
, let vv :: Symbol
vv = SpecType -> Symbol
forall r c tv. Reftable r => RType c tv r -> Symbol
rTypeValueVar SpecType
t
, let mt :: RReft
mt = (Symbol, Expr) -> RReft
RT.uReft (Symbol
vv, Brel -> Expr -> Expr -> Expr
F.PAtom Brel
F.Eq (Symbol -> Expr
F.EVar Symbol
vv) (Expr -> Expr -> Expr
F.EApp (Symbol -> Expr
F.EVar Symbol
x) (Symbol -> Expr
F.EVar Symbol
z)))
]
su :: Subst
su = [(Symbol, Expr)] -> Subst
F.mkSubst [ (Symbol
x, Expr -> Expr -> Expr
F.EApp (Symbol -> Expr
F.EVar Symbol
x) (Symbol -> Expr
F.EVar Symbol
z)) | Symbol
x <- (Symbol, SpecType) -> Symbol
forall a b. (a, b) -> a
fst ((Symbol, SpecType) -> Symbol) -> [(Symbol, SpecType)] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, SpecType)]
args ]
args :: [(Symbol, SpecType)]
args = DataConP -> [(Symbol, SpecType)]
dcpTyArgs DataConP
dcp
z :: Symbol
z = Symbol
"lq$recSel"
res :: SpecType
res = SpecType -> SpecType
forall {r}.
RType RTyCon RTyVar (UReft r) -> RType RTyCon RTyVar (UReft r)
dropPreds (DataConP -> SpecType
dcpTyRes DataConP
dcp)
dropPreds :: RType RTyCon RTyVar (UReft r) -> RType RTyCon RTyVar (UReft r)
dropPreds = (UReft r -> UReft r)
-> RType RTyCon RTyVar (UReft r) -> RType RTyCon RTyVar (UReft r)
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 (\(MkUReft r
r Predicate
_ps) -> r -> Predicate -> UReft r
forall r. r -> Predicate -> UReft r
MkUReft r
r Predicate
forall a. Monoid a => a
mempty)