{-# LANGUAGE FlexibleContexts  #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TupleSections     #-}

module Language.Haskell.Liquid.Bare.DataType
  ( dataConMap

  -- * Names for accessing Data Constuctors
  , makeDataConChecker
  , makeDataConSelector
  , addClassEmbeds

  -- * Constructors
  , makeDataDecls
  , makeConTypes
  , makeRecordSelectorSigs
  , meetDataConSpec
  -- , makeTyConEmbeds

  , 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' stores the names of those ctor-fields that have been declared
--   as SMT ADTs so we don't make up new names for them.
--------------------------------------------------------------------------------
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 d' creates the measure for `is$d` which tests whether
--   a given value was created by 'd'. e.g. is$Nil or is$Cons.
--------------------------------------------------------------------------------
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 d' creates the selector `select$d$i`
--   which projects the i-th field of a constructed value.
--   e.g. `select$Cons$1` and `select$Cons$2` are respectively
--   equivalent to `head` and `tail`.
--------------------------------------------------------------------------------
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 = {- simpleSymbolVar -} 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


--------------------------------------------------------------------------------
-- | makeClassEmbeds: sort-embeddings for numeric, and family-instance tycons
--------------------------------------------------------------------------------
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 : embed family instance tycons, see [NOTE:FamInstEmbeds]
--------------------------------------------------------------------------------
--     Query.R$58$EntityFieldBlobdog
--   with the actual family instance  types that have numeric instances as int [Check!]
--------------------------------------------------------------------------------
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

{-
famInstTyConType :: Ghc.TyCon -> Maybe Ghc.Type
famInstTyConType c = case Ghc.tyConFamInst_maybe c of
    Just (c', ts) -> F.tracepp ("famInstTyConType: " ++ F.showpp (c, Ghc.tyConArity c, ts))
                     $ Just (famInstType (Ghc.tyConArity c) c' ts)
    Nothing       -> Nothing

famInstType :: Int -> Ghc.TyCon -> [Ghc.Type] -> Ghc.Type
famInstType n c ts = Ghc.mkTyConApp c (take (length ts - n) ts)
-}

{- | [NOTE:FamInstEmbeds] GHC represents family instances in two ways:

     (1) As an applied type,
     (2) As a special tycon.

     For example, consider `tests/pos/ExactGADT4.hs`:

        class PersistEntity record where
          data EntityField record :: * -> *

        data Blob = B { xVal :: Int, yVal :: Int }

        instance PersistEntity Blob where
           data EntityField Blob dog where
             BlobXVal :: EntityField Blob Int
             BlobYVal :: EntityField Blob Int

     here, the type of the constructor `BlobXVal` can be represented as:

     (1) EntityField Blob Int,

     or

     (2) R$58$EntityFieldBlobdog Int

     PROBLEM: For various reasons, GHC will use _both_ representations interchangeably,
     which messes up our sort-checker.

     SOLUTION: To address the above, we create an "embedding"

        R$58$EntityFieldBlobdog :-> EntityField Blob

     So that all occurrences of the (2) are treated as (1) by the sort checker.

 -}

--------------------------------------------------------------------------------
-- | makeNumEmbeds: embed types that have numeric instances as int [Check!]
--------------------------------------------------------------------------------
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

--------------------------------------------------------------------------------
-- | Create Fixpoint DataDecl from LH DataDecls --------------------------------
--------------------------------------------------------------------------------

-- | A 'DataPropDecl' is associated with a (`TyCon` and) `DataDecl`, and defines the
--   sort of relation that is established by terms of the given `TyCon`.
--   A 'DataPropDecl' say, 'pd' is associated with a 'dd' of type 'DataDecl' when
--   'pd' is the `SpecType` version of the `BareType` given by `tycPropTy dd`.

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         = {- F.notracepp "BAD-Data" . -} [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))


-- [NOTE:Orphan-TyCons]

{- | 'resolveTyCons' will prune duplicate 'TyCon' definitions, as follows:

      Let the "home" of a 'TyCon' be the module where it is defined.
      There are three kinds of 'DataDecl' definitions:

      1. A  "home"-definition is one that belongs to its home module,
      2. An "orphan"-definition is one that belongs to some non-home module.

      A 'DataUser' definition SHOULD be a "home" definition
          - otherwise you can avoid importing the definition
            and hence, unsafely pass its invariants!

      So, 'resolveTyConDecls' implements the following protocol:

      (a) If there is a "Home" definition,
          then use it, and IGNORE others.

      (b) If there are ONLY "orphan" definitions,
          then pick the one from an _LHAssumptions module.

      (c) If there are ONLY "orphan" definitions,
          and none in _LHAssumptions modules,
          then pick the one from the module being analyzed.

-}
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 ]

-- | See [NOTE:Orphan-TyCons], the below function tells us which of (possibly many)
--   DataDecls to use.
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)

-- [NOTE:ADT] We need to POST-PROCESS the 'Sort' so that:
-- 1. The poly tyvars are replaced with debruijn
--    versions e.g. 'List a_a1m' becomes 'List @(1)'
-- 2. The "self" type is replaced with just itself
--    (i.e. without any type applications.)

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

{-
muSort :: F.FTycon -> Int -> F.Sort -> F.Sort
muSort c n  = V.mapSort tx
  where
    ct      = F.fTyconSort c
    me      = F.fTyconSelfSort c n
    tx t    = if t == me then ct else t
-}

--------------------------------------------------------------------------------
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)
                ]
--------------------------------------------------------------------------------
-- | Bare Predicate: DataCon Definitions ---------------------------------------
--------------------------------------------------------------------------------
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 ds' returns a subset of 'ds' with duplicates, e.g. arising
--   due to automatic lifting (via 'makeHaskellDataDecls'). We require that the
--   lifted versions appear LATER in the input list, and always use those
--   instead of the unlifted versions.

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
            -- [ (k, d) | d <- ds, k <- rights [dataDeclKey env name d] ]
  -- case Misc.uniqueByKey' selectDD kds of
    -- Left  decls  -> err    decls
    -- Right decls  -> decls
  where
    -- kds          = F.tracepp "canonizeDecls" [ (k, d) | d <- ds, k <- rights [dataDeclKey env name d] ]
    err :: [DataDecl] -> TError t
err ds :: [DataDecl]
ds@(DataDecl
d:[DataDecl]
_) = {- uError $ -} 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)

-- | Perform sanity check on the data constructors of a LH datatype declaration.
--
-- In the special situation where the LH datatype declaration is only used to
-- attach a termination measure, we pass 'Nothing', and our check always succeeds.
--
-- Otherwise, we check that the constructors match the constructors for the
-- Haskell datatype. This replaces an older check that only verified that any
-- constructor we list in a datatype is indeed a constructor of that corresponding
-- Haskell datatype.
--
-- We also check that constructors do not have duplicate fields.
--
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
  -- The GHC data constructors (these are qualified)
  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

  -- The data constructors in the spec (which we have to qualify for them to match the GHC data constructors)
  [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]

-- | Checks whether the given data constructor has duplicate fields.
--
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' checks that the supplied DataDecl is indeed a refinement
--   of the GHC TyCon. We just check that the right tyvars are supplied
--   as errors in the names and types of the constructors will be caught
--   elsewhere. [e.g. tests/errors/BadDataDecl.hs]

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" ]
  --  ugh              = impossible Nothing "getDnTyCon"


-- FIXME: ES: why the maybes?
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"

-- TODO:EFFECTS:ofBDataCon
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


-- | This computes the result of a `DataCon` application.
--   For 'isVanillaDataCon' we can just use the `TyCon`
--   applied to the relevant tyvars.
dataConResultTy :: Ghc.DataCon
                -> [RTyVar]         -- ^ DataConP ty-vars
                -> SpecType         -- ^ vanilla result type
                -> Maybe SpecType   -- ^ user-provided result type
                -> 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

-- | `qualifyDataCtor` qualfies the field names for each `DataCtor` to
--   ensure things work properly when exported.
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                    --    no field labels
    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)   -- OR function-valued fields
    Bool -> Bool -> Bool
|| DataConP -> Bool
dcpIsGadt DataConP
dcp              -- OR GADT style datcon
    = []
    | 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 -- NOTE: the reverse here is correct
             , let vv :: Symbol
vv = SpecType -> Symbol
forall r c tv. Reftable r => RType c tv r -> Symbol
rTypeValueVar SpecType
t
               -- the measure singleton refinement, eg `v = getBar foo`
             , 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)

      -- FIXME: this is clearly imprecise, but the preds in the DataConP seem
      -- to be malformed. If we leave them in, tests/pos/kmp.hs fails with
      -- a malformed predicate application. Niki, help!!
      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)