{-# 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

  ) where

import           Prelude                                hiding (error)

-- import           Text.Parsec
-- import           Var
-- import           Data.Maybe
-- import           Language.Haskell.Liquid.GHC.TypeRep

import qualified Control.Exception                      as Ex
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.Visitor        as V
import qualified Language.Fixpoint.Types                as F
import qualified Language.Haskell.Liquid.GHC.Misc       as GM 
import qualified Language.Haskell.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 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 qualified Language.Haskell.Liquid.Bare.Misc      as GM
-- import           Language.Haskell.Liquid.Bare.Env
-- import           Language.Haskell.Liquid.Bare.Lookup
-- import           Language.Haskell.Liquid.Bare.OfType

import           Text.Printf                     (printf)
import           Text.PrettyPrint.HughesPJ       ((<+>))
-- import           Debug.Trace (trace)

--------------------------------------------------------------------------------
-- | '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
  = String -> Symbol -> Maybe Int -> Symbol
symbolMeasure String
"$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 -} Id -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol (Id -> Symbol) -> (DataCon -> Id) -> DataCon -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataCon -> Id
Ghc.dataConWorkId

symbolMeasure :: String -> F.Symbol -> Maybe Int -> F.Symbol
symbolMeasure :: String -> Symbol -> Maybe Int -> Symbol
symbolMeasure String
f Symbol
d Maybe Int
iMb = (Symbol -> Symbol -> Symbol) -> [Symbol] -> Symbol
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]
: String -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol String
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 a. a -> [a]
Misc.singleton (Symbol -> [Symbol]) -> (Int -> Symbol) -> Int -> [Symbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol (String -> Symbol) -> (Int -> String) -> Int -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> String
forall a. Show a => a -> String
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
embs = (TCEmb TyCon -> (TyCon, Sort) -> TCEmb TyCon)
-> TCEmb TyCon -> [(TyCon, Sort)] -> TCEmb TyCon
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' TCEmb TyCon -> (TyCon, Sort) -> TCEmb TyCon
forall a. (Eq a, Hashable a) => TCEmb a -> (a, Sort) -> TCEmb a
embed TCEmb TyCon
embs [(TyCon, Sort)]
famInstSorts
  where
    famInstSorts :: [(TyCon, Sort)]
famInstSorts          = String -> [(TyCon, Sort)] -> [(TyCon, Sort)]
forall a. PPrint a => String -> a -> a
F.notracepp String
"famInstTcs"
                            [ (TyCon
c, TCEmb TyCon -> Type -> Sort
RT.typeSort TCEmb TyCon
embs 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                    = String -> [TyCon] -> [TyCon]
forall a. PPrint a => String -> a -> a
F.notracepp String
"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 (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 (LocSymbol -> Bool -> Bool -> FTycon
F.symbolNumInfoFTyCon (Symbol -> LocSymbol
forall a. a -> Located a
dummyLoc (Symbol -> LocSymbol) -> Symbol -> LocSymbol
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 -> String -> Sort
forall a. Maybe SrcSpan -> String -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing (String
"mappendSortFTC: s1 = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Sort -> String
forall a. PPrint a => a -> String
showpp Sort
s1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" s2 = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Sort -> String
forall a. PPrint a => a -> String
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]
              -> [F.DataDecl]
makeDataDecls :: Config
-> TCEmb TyCon
-> ModName
-> [(ModName, TyCon, DataPropDecl)]
-> [Located DataConP]
-> [DataDecl]
makeDataDecls Config
cfg TCEmb TyCon
tce ModName
name [(ModName, TyCon, DataPropDecl)]
tds [Located DataConP]
ds
  | Bool
makeDecls = [ 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, (ModName, DataPropDecl))]
-> [Located DataConP]
-> [(TyCon, (DataPropDecl, [(DataCon, DataConP)]))]
groupDataCons [(TyCon, (ModName, DataPropDecl))]
tds' (String -> [Located DataConP] -> [Located DataConP]
forall a. PPrint a => String -> a -> a
F.notracepp String
"makeDataDecls" [Located DataConP]
ds)
                , TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
/= TyCon
Ghc.listTyCon
                ]
  | Bool
otherwise = []
  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)
    tds' :: [(TyCon, (ModName, DataPropDecl))]
tds'      = ModName
-> [(ModName, TyCon, DataPropDecl)]
-> [(TyCon, (ModName, DataPropDecl))]
resolveTyCons ModName
name [(ModName, TyCon, DataPropDecl)]
tds

-- [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 MUST 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 module being analyzed.

      We COULD relax to allow for exactly one orphan `DataUser` definition
      which is the one that should be selected, but that seems like a
      slippery slope, as you can avoid importing the definition
      and hence, unsafely pass its invariants! (Feature not bug?)

-}
resolveTyCons :: ModName -> [(ModName, Ghc.TyCon, DataPropDecl)]
              -> [(Ghc.TyCon, (ModName, DataPropDecl))]
resolveTyCons :: ModName
-> [(ModName, TyCon, DataPropDecl)]
-> [(TyCon, (ModName, DataPropDecl))]
resolveTyCons ModName
m [(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
m 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  = String
-> Maybe (ModName, DataPropDecl) -> Maybe (ModName, DataPropDecl)
forall a. PPrint a => String -> a -> a
F.notracepp String
msg (Maybe (ModName, DataPropDecl) -> Maybe (ModName, DataPropDecl))
-> Maybe (ModName, DataPropDecl) -> Maybe (ModName, DataPropDecl)
forall a b. (a -> b) -> a -> b
$ [Maybe (ModName, DataPropDecl)] -> Maybe (ModName, DataPropDecl)
forall a. [Maybe a] -> Maybe a
Misc.firstMaybes ([Maybe (ModName, DataPropDecl)] -> Maybe (ModName, DataPropDecl))
-> [Maybe (ModName, DataPropDecl)] -> Maybe (ModName, DataPropDecl)
forall a b. (a -> b) -> a -> b
$ (((ModName, DataPropDecl) -> Bool)
-> [(ModName, DataPropDecl)] -> Maybe (ModName, DataPropDecl)
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
`L.find` [(ModName, DataPropDecl)]
mds) (((ModName, DataPropDecl) -> Bool)
 -> Maybe (ModName, DataPropDecl))
-> [(ModName, DataPropDecl) -> Bool]
-> [Maybe (ModName, DataPropDecl)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [ (ModName, DataPropDecl) -> Bool
forall b. (ModName, b) -> Bool
isHomeDef , (ModName, DataPropDecl) -> Bool
forall b. (ModName, b) -> Bool
isMyDef]
  where
    msg :: String
msg                    = String
"resolveDecls" String -> String -> String
forall a. [a] -> [a] -> [a]
++ (ModName, TyCon) -> String
forall a. PPrint a => a -> String
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)

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, Hashable 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
                               -- ++ maybeToList (makePropDecl tce tc dd) -- TODO: AUTO-INDPRED

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
  = DDecl :: FTycon -> Int -> [DataCtor] -> DataDecl
F.DDecl
      { ddTyCon :: FTycon
F.ddTyCon = FTycon
ftc
      , ddVars :: Int
F.ddVars  = [Id] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length                ([Id] -> Int) -> [Id] -> Int
forall a b. (a -> b) -> a -> b
$  TyCon -> [Id]
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 = LocSymbol -> FTycon
F.symbolFTycon (TyCon -> DataDecl -> LocSymbol
tyConLocSymbol TyCon
tc DataDecl
dd)

tyConLocSymbol :: Ghc.TyCon -> DataDecl -> LocSymbol
tyConLocSymbol :: TyCon -> DataDecl -> LocSymbol
tyConLocSymbol TyCon
tc DataDecl
dd = DataName -> Symbol -> LocSymbol
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) = DCtor :: LocSymbol -> [DataField] -> DataCtor
F.DCtor
  { dcName :: LocSymbol
F.dcName    = DataCon -> LocSymbol
forall a. (Symbolic a, NamedThing a) => a -> LocSymbol
GM.namedLocSymbol DataCon
d
  , dcFields :: [DataField]
F.dcFields  = TCEmb TyCon
-> FTycon -> [RTyVar] -> [(LocSymbol, SpecType)] -> [DataField]
makeDataFields TCEmb TyCon
tce FTycon
c [RTyVar]
as [(LocSymbol, SpecType)]
xts
  }
  where
    as :: [RTyVar]
as          = DataConP -> [RTyVar]
dcpFreeTyVars DataConP
dp
    xts :: [(LocSymbol, SpecType)]
xts         = [ (Symbol -> LocSymbol
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 -> LocSymbol
fld         = DataConP -> Symbol -> LocSymbol
forall l b. Loc l => l -> b -> Located b
F.atLoc DataConP
dp (Symbol -> LocSymbol) -> (Symbol -> Symbol) -> Symbol -> LocSymbol
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] -> [(LocSymbol, SpecType)] -> [DataField]
makeDataFields TCEmb TyCon
tce FTycon
_c [RTyVar]
as [(LocSymbol, SpecType)]
xts = [ LocSymbol -> Sort -> DataField
F.DField LocSymbol
x (SpecType -> Sort
fSort SpecType
t) | (LocSymbol
x, SpecType
t) <- [(LocSymbol, 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 (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 :: F.TCEmb Ghc.TyCon -> [(Ghc.Var, SpecType)] -> [DataConP] 
                -> [(Ghc.Var, SpecType)]
--------------------------------------------------------------------------------
meetDataConSpec :: TCEmb TyCon -> [(Id, SpecType)] -> [DataConP] -> [(Id, SpecType)]
meetDataConSpec TCEmb TyCon
emb [(Id, SpecType)]
xts [DataConP]
dcs  = HashMap Id SpecType -> [(Id, SpecType)]
forall k v. HashMap k v -> [(k, v)]
M.toList (HashMap Id SpecType -> [(Id, SpecType)])
-> HashMap Id SpecType -> [(Id, SpecType)]
forall a b. (a -> b) -> a -> b
$ (SrcSpan, SpecType) -> SpecType
forall a b. (a, b) -> b
snd ((SrcSpan, SpecType) -> SpecType)
-> HashMap Id (SrcSpan, SpecType) -> HashMap Id SpecType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (HashMap Id (SrcSpan, SpecType)
 -> (Id, SpecType) -> HashMap Id (SrcSpan, SpecType))
-> HashMap Id (SrcSpan, SpecType)
-> [(Id, SpecType)]
-> HashMap Id (SrcSpan, SpecType)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' HashMap Id (SrcSpan, SpecType)
-> (Id, SpecType) -> HashMap Id (SrcSpan, SpecType)
forall a.
(PPrint a, NamedThing a, Eq a, Hashable a) =>
HashMap a (SrcSpan, SpecType)
-> (a, SpecType) -> HashMap a (SrcSpan, SpecType)
upd HashMap Id (SrcSpan, SpecType)
dcm0 [(Id, SpecType)]
xts
  where
    dcm0 :: HashMap Id (SrcSpan, SpecType)
dcm0                     = [(Id, (SrcSpan, SpecType))] -> HashMap Id (SrcSpan, SpecType)
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList ([DataConP] -> [(Id, (SrcSpan, SpecType))]
dataConSpec' [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)
    meetX :: a -> SpecType -> (SrcSpan, SpecType) -> SpecType
meetX a
x SpecType
t (SrcSpan
sp', SpecType
t')      = String -> SpecType -> SpecType
forall a. PPrint a => String -> a -> a
F.notracepp (a -> SpecType -> SpecType -> String
forall a b c.
(PPrint a, PPrint b, PPrint c) =>
a -> b -> c -> String
_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 -> String
_msg a
x b
t c
t'              = String
"MEET-VAR-TYPES: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (a, b, c) -> String
forall a. PPrint a => a -> String
showpp (a
x, b
t, c
t')

dataConSpec' :: [DataConP] -> [(Ghc.Var, (Ghc.SrcSpan, SpecType))]
dataConSpec' :: [DataConP] -> [(Id, (SrcSpan, SpecType))]
dataConSpec' = (DataConP -> [(Id, (SrcSpan, SpecType))])
-> [DataConP] -> [(Id, (SrcSpan, SpecType))]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap DataConP -> [(Id, (SrcSpan, SpecType))]
tx 
  where
    tx :: DataConP -> [(Id, (SrcSpan, SpecType))]
tx DataConP
dcp   =  [ (Id
x, (SrcSpan, SpecType)
res) | (Id
x, SpecType
t0) <- DataConP -> [(Id, SpecType)]
dataConPSpecType DataConP
dcp
                          , let t :: SpecType
t    = Id -> SpecType -> SpecType
forall r.
(PPrint r, Reftable r, SubsTy RTyVar (RType RTyCon RTyVar ()) r,
 Reftable (RTProp RTyCon RTyVar r)) =>
Id -> RType RTyCon RTyVar r -> RType RTyCon RTyVar r
RT.expandProductType Id
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 :: Bare.Env -> (ModName, Ms.BareSpec) 
             -> ([(ModName, TyConP, Maybe DataPropDecl)], [[Located DataConP]])
makeConTypes :: Env
-> (ModName, BareSpec)
-> ([(ModName, TyConP, Maybe DataPropDecl)], [[Located DataConP]])
makeConTypes Env
env (ModName
name, BareSpec
spec) 
         = [((ModName, TyConP, Maybe DataPropDecl), [Located DataConP])]
-> ([(ModName, TyConP, Maybe DataPropDecl)], [[Located DataConP]])
forall a b. [(a, b)] -> ([a], [b])
unzip  [ Env
-> ModName
-> Maybe DataDecl
-> Maybe (LocSymbol, [Variance])
-> ((ModName, TyConP, Maybe DataPropDecl), [Located DataConP])
ofBDataDecl Env
env ModName
name Maybe DataDecl
x Maybe (LocSymbol, [Variance])
y | (Maybe DataDecl
x, Maybe (LocSymbol, [Variance])
y) <- [(Maybe DataDecl, Maybe (LocSymbol, [Variance]))]
gvs ] 
  where 
    gvs :: [(Maybe DataDecl, Maybe (LocSymbol, [Variance]))]
gvs  = [DataDecl]
-> [(LocSymbol, [Variance])]
-> [(Maybe DataDecl, Maybe (LocSymbol, [Variance]))]
groupVariances [DataDecl]
dcs' [(LocSymbol, [Variance])]
vdcs
    dcs' :: [DataDecl]
dcs' = Env -> ModName -> [DataDecl] -> [DataDecl]
canonizeDecls Env
env ModName
name [DataDecl]
dcs
    dcs :: [DataDecl]
dcs  = BareSpec -> [DataDecl]
forall ty bndr. Spec ty bndr -> [DataDecl]
Ms.dataDecls BareSpec
spec 
    vdcs :: [(LocSymbol, [Variance])]
vdcs = BareSpec -> [(LocSymbol, [Variance])]
forall ty bndr. Spec ty bndr -> [(LocSymbol, [Variance])]
Ms.dvariance BareSpec
spec 

-- | '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] -> [DataDecl]
canonizeDecls :: Env -> ModName -> [DataDecl] -> [DataDecl]
canonizeDecls Env
env ModName
name [DataDecl]
ds =
  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 [(Symbol, DataDecl)]
kds of
    Left  [DataDecl]
decls  -> [DataDecl] -> [DataDecl]
forall p. [DataDecl] -> p
err    [DataDecl]
decls
    Right [DataDecl]
decls  -> [DataDecl]
decls
  where
    kds :: [(Symbol, DataDecl)]
kds          = [ (Symbol
k, DataDecl
d) | DataDecl
d <- [DataDecl]
ds, Symbol
k <- Maybe Symbol -> [Symbol]
forall a. Maybe a -> [a]
Mb.maybeToList (Env -> ModName -> DataDecl -> Maybe Symbol
dataDeclKey Env
env ModName
name DataDecl
d) ] 
    err :: [DataDecl] -> p
err ds :: [DataDecl]
ds@(DataDecl
d:[DataDecl]
_) = UserError -> p
forall a. UserError -> a
uError (Doc -> ListNE SrcSpan -> UserError
forall t. Doc -> ListNE SrcSpan -> TError t
errDupSpecs (DataName -> Doc
forall a. PPrint a => a -> Doc
pprint (DataName -> Doc) -> DataName -> Doc
forall a b. (a -> b) -> a -> b
$ 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 -> String -> p
forall a. Maybe SrcSpan -> String -> a
impossible Maybe SrcSpan
forall a. Maybe a
Nothing String
"canonizeDecls"

dataDeclKey :: Bare.Env -> ModName -> DataDecl -> Maybe F.Symbol 
-- dataDeclKey env name = fmap F.symbol . Bare.lookupGhcDnTyCon env name "canonizeDecls" . tycName
dataDeclKey :: Env -> ModName -> DataDecl -> Maybe Symbol
dataDeclKey Env
env ModName
name DataDecl
d = do 
  TyCon
tc    <- Env -> ModName -> String -> DataName -> Maybe TyCon
Bare.lookupGhcDnTyCon Env
env ModName
name String
"canonizeDecls" (DataDecl -> DataName
tycName DataDecl
d)
  [DataCtor]
_     <- Env -> ModName -> TyCon -> [DataCtor] -> Maybe [DataCtor]
checkDataCtors Env
env ModName
name TyCon
tc (DataDecl -> [DataCtor]
tycDCons DataDecl
d)   
  Symbol -> Maybe Symbol
forall (m :: * -> *) a. Monad m => a -> m a
return (TyCon -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol TyCon
tc)

checkDataCtors :: Bare.Env -> ModName -> Ghc.TyCon -> [DataCtor] -> Maybe [DataCtor] 
checkDataCtors :: Env -> ModName -> TyCon -> [DataCtor] -> Maybe [DataCtor]
checkDataCtors Env
env ModName
name TyCon
c = (DataCtor -> Maybe DataCtor) -> [DataCtor] -> Maybe [DataCtor]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Env
-> ModName -> TyCon -> HashSet Symbol -> DataCtor -> Maybe DataCtor
checkDataCtor2 Env
env ModName
name TyCon
c HashSet Symbol
dcs (DataCtor -> Maybe DataCtor)
-> (DataCtor -> DataCtor) -> DataCtor -> Maybe DataCtor
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataCtor -> DataCtor
checkDataCtor1) 
  where 
    dcs :: HashSet Symbol
dcs                   = [Symbol] -> HashSet Symbol
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList ([Symbol] -> HashSet Symbol)
-> ([DataCon] -> [Symbol]) -> [DataCon] -> HashSet Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (DataCon -> Symbol) -> [DataCon] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DataCon -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol ([DataCon] -> HashSet Symbol) -> [DataCon] -> HashSet Symbol
forall a b. (a -> b) -> a -> b
$ TyCon -> [DataCon]
Ghc.tyConDataCons TyCon
c

checkDataCtor2 :: Bare.Env -> ModName -> Ghc.TyCon -> S.HashSet F.Symbol -> DataCtor 
               -> Maybe DataCtor 
checkDataCtor2 :: Env
-> ModName -> TyCon -> HashSet Symbol -> DataCtor -> Maybe DataCtor
checkDataCtor2 Env
env ModName
name TyCon
c HashSet Symbol
dcs DataCtor
d = do
  let dn :: LocSymbol
dn = DataCtor -> LocSymbol
dcName DataCtor
d
  DataCon
ctor  <- Env -> ModName -> Either UserError DataCon -> Maybe DataCon
forall r. Env -> ModName -> Either UserError r -> Maybe r
Bare.failMaybe Env
env ModName
name (Env -> ModName -> String -> LocSymbol -> Either UserError DataCon
forall a.
ResolveSym a =>
Env -> ModName -> String -> LocSymbol -> Either UserError a
Bare.resolveLocSym Env
env ModName
name String
"checkDataCtor2" LocSymbol
dn :: Either UserError Ghc.DataCon) 
  let x :: Symbol
x  = DataCon -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol DataCon
ctor 
  if Symbol -> HashSet Symbol -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
S.member Symbol
x HashSet Symbol
dcs 
    then DataCtor -> Maybe DataCtor
forall a. a -> Maybe a
Just DataCtor
d
    else UserError -> Maybe DataCtor
forall a e. Exception e => e -> a
Ex.throw (TyCon -> LocSymbol -> UserError
errInvalidDataCon TyCon
c LocSymbol
dn)

checkDataCtor1 :: DataCtor -> DataCtor 
checkDataCtor1 :: DataCtor -> DataCtor
checkDataCtor1 DataCtor
d 
  | Symbol
x : [Symbol]
_ <- [Symbol]
dups = UserError -> DataCtor
forall a. UserError -> a
uError (LocSymbol -> Symbol -> UserError
forall a a t. (PPrint a, PPrint a) => Located a -> a -> TError t
err LocSymbol
lc Symbol
x :: UserError)
  | Bool
otherwise     = DataCtor
d 
    where
      lc :: LocSymbol
lc          = DataCtor -> LocSymbol
dcName   DataCtor
d 
      xts :: [(Symbol, BareType)]
xts         = DataCtor -> [(Symbol, BareType)]
dcFields DataCtor
d
      dups :: [Symbol]
dups        = [ Symbol
x | (Symbol
x, [BareType]
ts) <- [(Symbol, BareType)] -> [(Symbol, [BareType])]
forall k v. (Eq k, Hashable k) => [(k, v)] -> [(k, [v])]
Misc.groupList [(Symbol, BareType)]
xts, Int
2 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= [BareType] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [BareType]
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 :: (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]
-> [(LocSymbol, [Variance])]
-> [(Maybe DataDecl, Maybe (LocSymbol, [Variance]))]
groupVariances [DataDecl]
dcs [(LocSymbol, [Variance])]
vdcs     =  [DataDecl]
-> [(LocSymbol, [Variance])]
-> [(Maybe DataDecl, Maybe (LocSymbol, [Variance]))]
forall a b.
Symbolic a =>
[a] -> [(LocSymbol, b)] -> [(Maybe a, Maybe (LocSymbol, b))]
merge ([DataDecl] -> [DataDecl]
forall a. Ord a => [a] -> [a]
L.sort [DataDecl]
dcs) (((LocSymbol, [Variance]) -> (LocSymbol, [Variance]) -> Ordering)
-> [(LocSymbol, [Variance])] -> [(LocSymbol, [Variance])]
forall a. (a -> a -> Ordering) -> [a] -> [a]
L.sortBy (\(LocSymbol, [Variance])
x (LocSymbol, [Variance])
y -> LocSymbol -> LocSymbol -> Ordering
forall a. Ord a => a -> a -> Ordering
compare ((LocSymbol, [Variance]) -> LocSymbol
forall a b. (a, b) -> a
fst (LocSymbol, [Variance])
x) ((LocSymbol, [Variance]) -> LocSymbol
forall a b. (a, b) -> a
fst (LocSymbol, [Variance])
y)) [(LocSymbol, [Variance])]
vdcs)
  where
    merge :: [a] -> [(LocSymbol, b)] -> [(Maybe a, Maybe (LocSymbol, b))]
merge (a
d:[a]
ds) ((LocSymbol, b)
v:[(LocSymbol, b)]
vs)
      | a -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol a
d Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== (LocSymbol, b) -> Symbol
forall c b. (Located c, b) -> c
sym (LocSymbol, b)
v = (a -> Maybe a
forall a. a -> Maybe a
Just a
d, (LocSymbol, b) -> Maybe (LocSymbol, b)
forall a. a -> Maybe a
Just (LocSymbol, b)
v)  (Maybe a, Maybe (LocSymbol, b))
-> [(Maybe a, Maybe (LocSymbol, b))]
-> [(Maybe a, Maybe (LocSymbol, b))]
forall a. a -> [a] -> [a]
: [a] -> [(LocSymbol, b)] -> [(Maybe a, Maybe (LocSymbol, b))]
merge [a]
ds [(LocSymbol, b)]
vs
      | a -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol a
d Symbol -> Symbol -> Bool
forall a. Ord a => a -> a -> Bool
<  (LocSymbol, b) -> Symbol
forall c b. (Located c, b) -> c
sym (LocSymbol, b)
v = (a -> Maybe a
forall a. a -> Maybe a
Just a
d, Maybe (LocSymbol, b)
forall a. Maybe a
Nothing) (Maybe a, Maybe (LocSymbol, b))
-> [(Maybe a, Maybe (LocSymbol, b))]
-> [(Maybe a, Maybe (LocSymbol, b))]
forall a. a -> [a] -> [a]
: [a] -> [(LocSymbol, b)] -> [(Maybe a, Maybe (LocSymbol, b))]
merge [a]
ds ((LocSymbol, b)
v(LocSymbol, b) -> [(LocSymbol, b)] -> [(LocSymbol, b)]
forall a. a -> [a] -> [a]
:[(LocSymbol, b)]
vs)
      | Bool
otherwise           = (Maybe a
forall a. Maybe a
Nothing, (LocSymbol, b) -> Maybe (LocSymbol, b)
forall a. a -> Maybe a
Just (LocSymbol, b)
v) (Maybe a, Maybe (LocSymbol, b))
-> [(Maybe a, Maybe (LocSymbol, b))]
-> [(Maybe a, Maybe (LocSymbol, b))]
forall a. a -> [a] -> [a]
: [a] -> [(LocSymbol, b)] -> [(Maybe a, Maybe (LocSymbol, b))]
merge (a
da -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
ds) [(LocSymbol, b)]
vs
    merge []     [(LocSymbol, b)]
vs         = ((Maybe a
forall a. Maybe a
Nothing,) (Maybe (LocSymbol, b) -> (Maybe a, Maybe (LocSymbol, b)))
-> ((LocSymbol, b) -> Maybe (LocSymbol, b))
-> (LocSymbol, b)
-> (Maybe a, Maybe (LocSymbol, b))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (LocSymbol, b) -> Maybe (LocSymbol, b)
forall a. a -> Maybe a
Just) ((LocSymbol, b) -> (Maybe a, Maybe (LocSymbol, b)))
-> [(LocSymbol, b)] -> [(Maybe a, Maybe (LocSymbol, b))]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(LocSymbol, b)]
vs
    merge [a]
ds     []         = ((,Maybe (LocSymbol, b)
forall a. Maybe a
Nothing) (Maybe a -> (Maybe a, Maybe (LocSymbol, b)))
-> (a -> Maybe a) -> a -> (Maybe a, Maybe (LocSymbol, b))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Maybe a
forall a. a -> Maybe a
Just) (a -> (Maybe a, Maybe (LocSymbol, b)))
-> [a] -> [(Maybe a, Maybe (LocSymbol, 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 = String -> Bool -> Bool
forall a. PPrint a => String -> a -> a
F.notracepp String
_msg (Bool
isGADT Bool -> Bool -> Bool
|| Int
cN Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
dN Bool -> Bool -> Bool
|| [DataCtor] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (DataDecl -> [DataCtor]
tycDCons DataDecl
d))
  where
    _msg :: String
_msg          = String -> String -> String -> Int -> Int -> String
forall r. PrintfType r => String -> r
printf String
"checkDataDecl: D = %s, c = %s, cN = %d, dN = %d" (DataDecl -> String
forall a. Show a => a -> String
show DataDecl
d) (TyCon -> String
forall a. Show a => a -> String
show TyCon
c) Int
cN Int
dN
    cN :: Int
cN            = [Id] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (TyCon -> [Id]
GM.tyConTyVarsDef TyCon
c)
    dN :: Int
dN            = [Symbol] -> 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 -> Ghc.TyCon
getDnTyCon :: Env -> ModName -> DataName -> TyCon
getDnTyCon Env
env ModName
name DataName
dn = TyCon -> Maybe TyCon -> TyCon
forall a. a -> Maybe a -> a
Mb.fromMaybe TyCon
forall a. a
ugh (Env -> ModName -> String -> DataName -> Maybe TyCon
Bare.lookupGhcDnTyCon Env
env ModName
name String
"ofBDataDecl-1" DataName
dn)
  where 
    ugh :: a
ugh                = Maybe SrcSpan -> String -> a
forall a. Maybe SrcSpan -> String -> a
impossible Maybe SrcSpan
forall a. Maybe a
Nothing String
"getDnTyCon"

-- FIXME: ES: why the maybes?
ofBDataDecl :: Bare.Env -> ModName -> Maybe DataDecl -> (Maybe (LocSymbol, [Variance]))
            -> ( (ModName, TyConP, Maybe DataPropDecl), [Located DataConP])
ofBDataDecl :: Env
-> ModName
-> Maybe DataDecl
-> Maybe (LocSymbol, [Variance])
-> ((ModName, TyConP, Maybe DataPropDecl), [Located DataConP])
ofBDataDecl Env
env ModName
name (Just dd :: DataDecl
dd@(DataDecl DataName
tc [Symbol]
as [PVar BSort]
ps [DataCtor]
cts SourcePos
pos Maybe SizeFun
sfun Maybe BareType
pt DataDeclKind
_)) Maybe (LocSymbol, [Variance])
maybe_invariance_info
  | Bool -> Bool
not (TyCon -> DataDecl -> Bool
checkDataDecl TyCon
tc' DataDecl
dd)
  = UserError
-> ((ModName, TyConP, Maybe DataPropDecl), [Located DataConP])
forall a. UserError -> a
uError UserError
err
  | Bool
otherwise
  = ((ModName
name, TyConP
tcp, DataPropDecl -> Maybe DataPropDecl
forall a. a -> Maybe a
Just (DataDecl
dd { tycDCons :: [DataCtor]
tycDCons = [DataCtor]
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
    π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
    tc' :: TyCon
tc'        = Env -> ModName -> DataName -> TyCon
getDnTyCon Env
env ModName
name DataName
tc
    -- cts        = checkDataCtors env name tc' cts0
    cts' :: [DataConP]
cts'       = Env
-> ModName
-> SourcePos
-> SourcePos
-> TyCon
-> [RTyVar]
-> [PVar BSort]
-> [RPVar]
-> DataCtor
-> DataConP
ofBDataCtor Env
env ModName
name SourcePos
lc SourcePos
lc' TyCon
tc' [RTyVar]
αs [PVar BSort]
ps [RPVar]
πs (DataCtor -> DataConP) -> [DataCtor] -> [DataConP]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [DataCtor]
cts
    pd :: Maybe SpecType
pd         = Env
-> ModName
-> SourcePos
-> Maybe [PVar BSort]
-> BareType
-> SpecType
Bare.ofBareType Env
env ModName
name SourcePos
lc ([PVar BSort] -> Maybe [PVar BSort]
forall a. a -> Maybe a
Just []) (BareType -> SpecType) -> Maybe BareType -> Maybe SpecType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe BareType
pt
    tys :: [SpecType]
tys        = [SpecType
t | DataConP
dcp <- [DataConP]
cts', (Symbol
_, SpecType
t) <- DataConP -> [(Symbol, SpecType)]
dcpTyArgs DataConP
dcp]
    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..]
    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
    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 (t :: * -> *) a. Foldable t => t a -> Int
length [RPVar]
πs Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)]
    ([Variance]
tvi, [Variance]
pvi) = [Variance] -> ([Variance], [Variance])
f [Variance]
defPs
    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
    err :: UserError
err          = SrcSpan -> Doc -> Doc -> UserError
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" :: UserError
    αs :: [RTyVar]
αs           = Id -> RTyVar
RTV (Id -> RTyVar) -> (Symbol -> Id) -> Symbol -> RTyVar
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Id
GM.symbolTyVar (Symbol -> RTyVar) -> [Symbol] -> [RTyVar]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol]
as
    n :: Int
n            = [RTyVar] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [RTyVar]
αs
    Loc SourcePos
lc SourcePos
lc' Symbol
_ = DataName -> LocSymbol
dataNameSymbol DataName
tc
    f :: [Variance] -> ([Variance], [Variance])
f [Variance]
defPs      = case Maybe (LocSymbol, [Variance])
maybe_invariance_info of
                     Maybe (LocSymbol, [Variance])
Nothing     -> ([], [Variance]
defPs)
                     Just (LocSymbol
_,[Variance]
is) -> (Int -> [Variance] -> [Variance]
forall a. Int -> [a] -> [a]
take Int
n [Variance]
is, if [Variance] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Int -> [Variance] -> [Variance]
forall a. Int -> [a] -> [a]
drop Int
n [Variance]
is) then [Variance]
defPs else (Int -> [Variance] -> [Variance]
forall a. Int -> [a] -> [a]
drop Int
n [Variance]
is))

ofBDataDecl Env
env ModName
name Maybe DataDecl
Nothing (Just (LocSymbol
tc, [Variance]
is))
  = ((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
    tc' :: TyCon
tc'            = Env -> ModName -> String -> LocSymbol -> TyCon
Bare.lookupGhcTyCon Env
env ModName
name String
"ofBDataDecl-2" LocSymbol
tc
    ([Variance]
tcov, [a]
tcontr) = ([Variance]
is, [])
    srcpos :: SourcePos
srcpos         = String -> SourcePos
F.dummyPos String
"LH.DataType.Variance"

ofBDataDecl Env
_ ModName
_ Maybe DataDecl
Nothing Maybe (LocSymbol, [Variance])
Nothing
  = Maybe SrcSpan
-> String
-> ((ModName, TyConP, Maybe DataPropDecl), [Located DataConP])
forall a. Maybe SrcSpan -> String -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing String
"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
            -> DataConP
ofBDataCtor :: Env
-> ModName
-> SourcePos
-> SourcePos
-> TyCon
-> [RTyVar]
-> [PVar BSort]
-> [RPVar]
-> DataCtor
-> DataConP
ofBDataCtor Env
env ModName
name SourcePos
l SourcePos
l' TyCon
tc [RTyVar]
αs [PVar BSort]
ps [RPVar]
πs _ctor :: DataCtor
_ctor@(DataCtor LocSymbol
c [Symbol]
as [BareType]
_ [(Symbol, BareType)]
xts Maybe BareType
res) = DataConP :: SourcePos
-> DataCon
-> [RTyVar]
-> [RPVar]
-> [SpecType]
-> [(Symbol, SpecType)]
-> SpecType
-> Bool
-> Symbol
-> SourcePos
-> DataConP
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
    c' :: DataCon
c'            = Env -> ModName -> String -> LocSymbol -> DataCon
Bare.lookupGhcDataCon Env
env ModName
name String
"ofBDataCtor" LocSymbol
c
    ts' :: [SpecType]
ts'           = Env
-> ModName
-> SourcePos
-> Maybe [PVar BSort]
-> BareType
-> SpecType
Bare.ofBareType Env
env ModName
name SourcePos
l ([PVar BSort] -> Maybe [PVar BSort]
forall a. a -> Maybe a
Just [PVar BSort]
ps) (BareType -> SpecType) -> [BareType] -> [SpecType]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [BareType]
ts
    res' :: Maybe SpecType
res'          = Env
-> ModName
-> SourcePos
-> Maybe [PVar BSort]
-> BareType
-> SpecType
Bare.ofBareType Env
env ModName
name SourcePos
l ([PVar BSort] -> Maybe [PVar BSort]
forall a. a -> Maybe a
Just [PVar BSort]
ps) (BareType -> SpecType) -> Maybe BareType -> Maybe SpecType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe BareType
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)     = -- F.tracepp ("dataConTys: " ++ F.showpp (c, αs)) $ 
                      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, [BareType]
ts)      = [(Symbol, BareType)] -> ([Symbol], [BareType])
forall a b. [(a, b)] -> ([a], [b])
unzip [(Symbol, BareType)]
xts
    t0 :: SpecType
t0            = case TyCon -> Maybe Type
RT.famInstTyConType TyCon
tc of
                      Maybe Type
Nothing -> String -> SpecType -> SpecType
forall a. PPrint a => String -> a -> a
F.notracepp String
"dataConResult-3: " (SpecType -> SpecType) -> SpecType -> SpecType
forall a b. (a -> b) -> a -> b
$ 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 BareType -> Bool
forall a. Maybe a -> Bool
Mb.isJust Maybe BareType
res
    dLoc :: Located ()
dLoc          = SourcePos -> SourcePos -> () -> Located ()
forall a. SourcePos -> SourcePos -> a -> Located a
F.Loc SourcePos
l SourcePos
l' ()




errInvalidDataCon :: Ghc.TyCon -> LocSymbol -> UserError
errInvalidDataCon :: TyCon -> LocSymbol -> UserError
errInvalidDataCon TyCon
c LocSymbol
d = SrcSpan -> Doc -> Doc -> UserError
forall t. SrcSpan -> Doc -> Doc -> TError t
ErrBadGADT SrcSpan
sp Doc
v Doc
msg
  where
    v :: Doc
v                 = Symbol -> Doc
forall a. PPrint a => a -> Doc
pprint (LocSymbol -> Symbol
forall a. Located a -> a
val LocSymbol
d)
    sp :: SrcSpan
sp                = SourcePos -> SrcSpan
GM.sourcePosSrcSpan (LocSymbol -> SourcePos
forall a. Located a -> SourcePos
loc LocSymbol
d)
    msg :: Doc
msg               = TyCon -> Doc
forall a. PPrint a => a -> Doc
ppTicks TyCon
c Doc -> Doc -> Doc
<+> Doc
"is not the type constructed by" Doc -> Doc -> Doc
<+> Doc -> Doc
forall a. PPrint a => a -> Doc
ppTicks Doc
v

varSignToVariance :: Eq a => [(a, Bool)] -> a -> Variance
varSignToVariance :: [(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 :: [(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
_ 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 -> String -> [(a, Bool)]
forall a. Maybe SrcSpan -> String -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing (String -> [(a, Bool)]) -> String -> [(a, Bool)]
forall a b. (a -> b) -> a -> b
$ String
"getPsSig" String -> String -> String
forall a. [a] -> [a] -> [a]
++ SpecType -> String
forall a. Show a => a -> String
show SpecType
z

getPsSigPs :: [(UsedPVar, a)] -> Bool -> SpecProp -> [(a, Bool)]
getPsSigPs :: [(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 :: [(UsedPVar, a)] -> b -> UReft t -> [(a, b)]
addps [(UsedPVar, a)]
m b
pos (MkUReft t
_ Predicate
ps) = ((a -> b -> (a, b)) -> b -> a -> (a, b)
forall a b c. (a -> b -> c) -> b -> a -> c
flip (,)) 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 -> String -> a
forall a. Maybe SrcSpan -> String -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing String
"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
_ [RTyVar]
_ SpecType
_ (Just SpecType
t) = SpecType
t
dataConResultTy DataCon
c [RTyVar]
_ SpecType
t Maybe SpecType
_
  | DataCon -> Bool
Ghc.isVanillaDataCon DataCon
c     = String -> SpecType -> SpecType
forall a. PPrint a => String -> a -> a
F.notracepp (String
"dataConResultTy-1 : " String -> String -> String
forall a. [a] -> [a] -> [a]
++ DataCon -> String
forall a. PPrint a => a -> String
F.showpp DataCon
c) (SpecType -> SpecType) -> SpecType -> SpecType
forall a b. (a -> b) -> a -> b
$ SpecType
t
  | Bool
otherwise                  = String -> SpecType -> SpecType
forall a. PPrint a => String -> a -> a
F.notracepp (String
"dataConResultTy-2 : " String -> String -> String
forall a. [a] -> [a] -> [a]
++ DataCon -> String
forall a. PPrint a => a -> String
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
    ([Id]
_,[Id]
_,[EqSpec]
_,[Type]
_,[Type]
_,Type
ct)             = DataCon -> ([Id], [Id], [EqSpec], [Type], [Type], Type)
Ghc.dataConFullSig DataCon
c
    -- _tr0                    = Ghc.dataConRepType c
    -- _tr1                    = Ghc.varType (Ghc.dataConWorkId c)
    -- _tr2                    = Ghc.varType (Ghc.dataConWrapId 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 :: 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 :: 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
t)
 | 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
t
   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 -> LocSymbol -> (Maybe Symbol, Symbol)
qualifyField ModName
name (Located a -> Symbol -> LocSymbol
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 -> LocSymbol -> (Maybe Symbol, Symbol)
qualifyField ModName
name LocSymbol
lx
 | Bool
needsQual = (Symbol -> Maybe Symbol
forall a. a -> Maybe a
Just Symbol
x, String -> Symbol -> Symbol
forall a. PPrint a => String -> a -> a
F.notracepp String
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 :: String
msg       = String
"QUALIFY-NAME: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Symbol -> String
forall a. Show a => a -> String
show Symbol
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" in module " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Symbol -> String
forall a. Show a => a -> String
show (ModName -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol ModName
name)
   x :: Symbol
x         = LocSymbol -> Symbol
forall a. Located a -> a
val LocSymbol
lx
   needsQual :: Bool
needsQual = Bool -> Bool
not (LocSymbol -> Bool
isWiredIn LocSymbol
lx)

checkRecordSelectorSigs :: [(Ghc.Var, LocSpecType)] -> [(Ghc.Var, LocSpecType)]
checkRecordSelectorSigs :: [(Id, LocSpecType)] -> [(Id, LocSpecType)]
checkRecordSelectorSigs [(Id, LocSpecType)]
vts = [ (Id
v, Id -> [LocSpecType] -> LocSpecType
forall a a. (PPrint a, PPrint a) => a -> [Located a] -> Located a
take1 Id
v [LocSpecType]
ts) | (Id
v, [LocSpecType]
ts) <- [(Id, LocSpecType)] -> [(Id, [LocSpecType])]
forall k v. (Eq k, Hashable k) => [(k, v)] -> [(k, [v])]
Misc.groupList [(Id, LocSpecType)]
vts ] 
  where 
    take1 :: a -> [Located a] -> Located a
take1 a
v [Located a]
ts              = case (Located a -> String) -> [Located a] -> [Located a]
forall k a. (Eq k, Hashable k) => (a -> k) -> [a] -> [a]
Misc.nubHashOn (a -> String
forall a. PPrint a => a -> String
showpp (a -> String) -> (Located a -> a) -> Located a -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Located a -> a
forall a. Located a -> a
val) [Located a]
ts of 
                                [Located a
t]    -> Located a
t 
                                (Located a
t:[Located a]
ts) -> Error -> Located a
forall a e. Exception e => e -> a
Ex.throw (SrcSpan -> Doc -> ListNE SrcSpan -> Error
forall t. SrcSpan -> Doc -> ListNE SrcSpan -> TError t
ErrDupSpecs (Located a -> SrcSpan
forall a. Loc a => a -> SrcSpan
GM.fSrcSpan Located a
t) (a -> Doc
forall a. PPrint a => a -> Doc
pprint a
v) (Located a -> SrcSpan
forall a. Loc a => a -> SrcSpan
GM.fSrcSpan (Located a -> SrcSpan) -> [Located a] -> ListNE SrcSpan
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Located a]
ts) :: Error)
                                [Located a]
_      -> Maybe SrcSpan -> String -> Located a
forall a. Maybe SrcSpan -> String -> a
impossible Maybe SrcSpan
forall a. Maybe a
Nothing String
"checkRecordSelectorSigs"

makeRecordSelectorSigs :: Bare.Env -> ModName -> [Located DataConP] -> [(Ghc.Var, LocSpecType)]
makeRecordSelectorSigs :: Env -> ModName -> [Located DataConP] -> [(Id, LocSpecType)]
makeRecordSelectorSigs Env
env ModName
name = [(Id, LocSpecType)] -> [(Id, LocSpecType)]
checkRecordSelectorSigs ([(Id, LocSpecType)] -> [(Id, LocSpecType)])
-> ([Located DataConP] -> [(Id, LocSpecType)])
-> [Located DataConP]
-> [(Id, LocSpecType)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Located DataConP -> [(Id, LocSpecType)])
-> [Located DataConP] -> [(Id, LocSpecType)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Located DataConP -> [(Id, LocSpecType)]
makeOne
  where
  makeOne :: Located DataConP -> [(Id, LocSpecType)]
makeOne (Loc SourcePos
l SourcePos
l' DataConP
dcp)
    | [FieldLabel] -> 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 
    = [ (Id
v, LocSpecType
t) | (Just Id
v, LocSpecType
t) <- [Maybe Id] -> [LocSpecType] -> [(Maybe Id, LocSpecType)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Maybe Id]
fs [LocSpecType]
ts ] 
    where
      dc :: DataCon
dc  = DataConP -> DataCon
dcpCon DataConP
dcp
      fls :: [FieldLabel]
fls = DataCon -> [FieldLabel]
Ghc.dataConFieldLabels DataCon
dc
      fs :: [Maybe Id]
fs  = Env -> ModName -> Name -> Maybe Id
forall a.
(NamedThing a, Symbolic a) =>
Env -> ModName -> a -> Maybe Id
Bare.lookupGhcNamedVar Env
env ModName
name (Name -> Maybe Id)
-> (FieldLabel -> Name) -> FieldLabel -> Maybe Id
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FieldLabel -> Name
forall a. FieldLbl a -> a
Ghc.flSelector (FieldLabel -> Maybe Id) -> [FieldLabel] -> [Maybe Id]
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, SpecType, RReft)]
-> [(Symbol, SpecType, RReft)]
-> SpecType
-> SpecType
forall tv c r.
[(RTVar tv (RType c tv ()), r)]
-> [PVar (RType c tv ())]
-> [(Symbol, RType c tv r, r)]
-> [(Symbol, RType c tv r, r)]
-> RType c tv r
-> RType c tv r
mkArrow ([RTVar RTyVar (RType RTyCon RTyVar ())]
-> [RReft] -> [(RTVar RTyVar (RType RTyCon RTyVar ()), RReft)]
forall a b. [a] -> [b] -> [(a, b)]
zip (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) (RReft -> [RReft]
forall a. a -> [a]
repeat RReft
forall a. Monoid a => a
mempty)) []
                                 [] [(Symbol
z, 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    = String -> Symbol -> Symbol
forall a. PPrint a => String -> a -> a
F.notracepp (String
"makeRecordSelectorSigs:" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [(Symbol, SpecType)] -> String
forall a. Show a => a -> String
show [(Symbol, SpecType)]
args) 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 (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)