{-# 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.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 = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList forall a b. (a -> b) -> a -> b
$ do
  DataDecl
d     <- [DataDecl]
ds
  DataCtor
c     <- DataDecl -> [DataCtor]
F.ddCtors DataDecl
d
  let fs :: [Symbol]
fs = forall a. Symbolic a => a -> Symbol
F.symbol forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DataCtor -> [DataField]
F.dcFields DataCtor
c
  forall a b. [a] -> [b] -> [(a, b)]
zip ((forall a. Symbolic a => a -> Symbol
F.symbol DataCtor
c,) 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
M.lookupDefault Symbol
def (forall a. Symbolic a => a -> Symbol
F.symbol DataCon
d, Int
i) DataConMap
dm
  where
    dm :: DataConMap
dm                       = forall a. a -> Maybe a -> a
Mb.fromMaybe 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) (forall a. a -> Maybe a
Just Int
i)

dcSymbol :: Ghc.DataCon -> F.Symbol
dcSymbol :: DataCon -> Symbol
dcSymbol = {- simpleSymbolVar -} forall a. Symbolic a => a -> Symbol
F.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 = forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 Symbol -> Symbol -> Symbol
F.suffixSymbol (Symbol
dcPrefix forall a. a -> [a] -> [a]
: forall a. Symbolic a => a -> Symbol
F.symbol [Char]
f forall a. a -> [a] -> [a]
: Symbol
d forall a. a -> [a] -> [a]
: [Symbol]
rest)
  where
    rest :: [Symbol]
rest          = forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] (forall t. t -> [t]
Misc.single forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Symbolic a => a -> Symbol
F.symbol forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 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 = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' forall {a}. Hashable a => TCEmb a -> (a, Sort) -> TCEmb a
embed TCEmb TyCon
embeds [(TyCon, Sort)]
famInstSorts
  where
    famInstSorts :: [(TyCon, Sort)]
famInstSorts          = 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  <- 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)     = 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                    = 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 = 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
  | forall c. TyConable c => c -> Bool
isFracCls TyCon
cls, Just TyCon
tc <- ClsInst -> Maybe TyCon
instanceTyCon ClsInst
is
  = forall a.
(Eq a, Hashable a) =>
(Sort -> Sort -> Sort) -> a -> Sort -> TCArgs -> TCEmb a -> TCEmb a
F.tceInsertWith (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
  | forall c. TyConable c => c -> Bool
isNumCls  TyCon
cls, Just TyCon
tc <- ClsInst -> Maybe TyCon
instanceTyCon ClsInst
is
  = forall a.
(Eq a, Hashable a) =>
(Sort -> Sort -> Sort) -> a -> Sort -> TCArgs -> TCEmb a -> TCEmb a
F.tceInsertWith (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 (forall a. a -> Located a
dummyLoc 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        = forall a. Maybe SrcSpan -> [Char] -> a
panic forall a. Maybe a
Nothing ([Char]
"mappendSortFTC: s1 = " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
showpp Sort
s1 forall a. [a] -> [a] -> [a]
++ [Char]
" s2 = " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
showpp Sort
s2)

instanceTyCon :: Ghc.ClsInst -> Maybe Ghc.TyCon
instanceTyCon :: ClsInst -> Maybe TyCon
instanceTyCon = [Type] -> Maybe TyCon
go 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]
_] = forall a. a -> Maybe a
Just TyCon
c
    go [Type]
_                  = 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        = (forall a. Monoid a => a
mempty, [])
  where
    makeDecls :: Bool
makeDecls        = forall t. HasConfig t => t -> Bool
exactDCFlag Config
cfg Bool -> Bool -> Bool
&& Bool -> Bool
not (Config -> Bool
noADT Config
cfg)
    warns :: [Warning]
warns            = (forall a. (Loc a, Symbolic a) => a -> Warning
mkWarnDecl forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(TyCon, (DataPropDecl, [(DataCon, DataConP)]))]
badTcs) forall a. [a] -> [a] -> [a]
++ (forall a. (Loc a, Symbolic a) => a -> Warning
mkWarnDecl 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            = forall a. (a -> Bool) -> [a] -> [a]
filter ((forall a. Eq a => a -> a -> Bool
/= TyCon
Ghc.listTyCon) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst)
                     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)  = forall a. (a -> Bool) -> [a] -> ([a], [a])
L.partition 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)) = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (DataCon -> Bool
Ghc.isVanillaDataCon forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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" . -} forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Symbolic a => a -> Symbol
F.symbol forall a b. (a -> b) -> a -> b
$ [DataDecl]
badDs
    oks :: [DataDecl]
oks             = [ DataDecl
d |  DataDecl
d <- [DataDecl]
ds, Bool -> Bool
not (forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
S.member (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 (forall a. Loc a => a -> SrcSpan
GM.fSrcSpan a
d) (Doc
"Non-regular data declaration" Doc -> Doc -> Doc
<+> forall a. PPrint a => a -> Doc
pprint (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) <- forall k v. HashMap k v -> [(k, v)]
M.toList HashMap TyCon [(ModName, DataPropDecl)]
tcDecls
                                      , (ModName
m, DataPropDecl
d)    <- forall a. Maybe a -> [a]
Mb.maybeToList 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          = 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  = forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
msg forall a b. (a -> b) -> a -> b
$
    case forall a. (a -> Bool) -> [a] -> [a]
filter forall {b}. (ModName, b) -> Bool
isHomeDef [(ModName, DataPropDecl)]
mds of
      (ModName, DataPropDecl)
x:[(ModName, DataPropDecl)]
_ -> forall a. a -> Maybe a
Just (ModName, DataPropDecl)
x
      [(ModName, DataPropDecl)]
_ -> case forall a. (a -> Bool) -> [a] -> [a]
filter forall {b}. (ModName, b) -> Bool
isLHAssumptionsDef [(ModName, DataPropDecl)]
mds of
        [(ModName, DataPropDecl)
x] -> forall a. a -> Maybe a
Just (ModName, DataPropDecl)
x
        xs :: [(ModName, DataPropDecl)]
xs@((ModName, DataPropDecl)
_:[(ModName, DataPropDecl)]
_) -> forall a. HasCallStack => [Char] -> a
error forall a b. (a -> b) -> a -> b
$
          [Char]
"Multiple spec declarations of " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (forall a. Symbolic a => a -> Symbol
F.symbol TyCon
tc) forall a. [a] -> [a] -> [a]
++
          [Char]
" found in _LHAssumption modules: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(ModName, DataPropDecl)]
xs) forall a. [a] -> [a] -> [a]
++
          [Char]
". Please, remove some of them."
        [] -> forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
L.find forall {b}. (ModName, b) -> Bool
isMyDef [(ModName, DataPropDecl)]
mds
  where
    msg :: [Char]
msg                    = [Char]
"resolveDecls" forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
F.showpp (ModName
mName, TyCon
tc)
    isMyDef :: (ModName, b) -> Bool
isMyDef                = (ModName
mName forall a. Eq a => a -> a -> Bool
==)             forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst
    isHomeDef :: (ModName, b) -> Bool
isHomeDef              = (Symbol
tcHome forall a. Eq a => a -> a -> Bool
==) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Symbolic a => a -> Symbol
F.symbol forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst
    tcHome :: Symbol
tcHome                 = Symbol -> Symbol
GM.takeModuleNames (forall a. Symbolic a => a -> Symbol
F.symbol TyCon
tc)
    isLHAssumptionsDef :: (ModName, b) -> Bool
isLHAssumptionsDef     = forall a. Eq a => [a] -> [a] -> Bool
L.isSuffixOf [Char]
"_LHAssumptions" forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleName -> [Char]
Ghc.moduleNameString forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModName -> ModuleName
getModName forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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' = forall a. (a -> Bool) -> [a] -> [a]
filter (ModName -> DataConP -> Bool
isResolvedDataConP ModName
m forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) [(DataCon, DataConP)]
dds
                       ]
  where
    tcDataCons :: [(TyCon, ((ModName, DataPropDecl), [(DataCon, DataConP)]))]
tcDataCons       = forall k v. HashMap k v -> [(k, v)]
M.toList forall a b. (a -> b) -> a -> b
$ 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            = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [(TyCon, (ModName, DataPropDecl))]
tds
    ctorM :: HashMap TyCon [(DataCon, DataConP)]
ctorM            = 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 = forall a. Symbolic a => a -> Symbol
F.symbol ModName
m 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 (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  = forall (t :: * -> *) a. Foldable t => t a -> Int
length                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 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 = forall l b. Loc l => l -> b -> Located b
F.atLoc (DataDecl -> DataName
tycName DataDecl
dd) (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    = 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) <- forall a. [a] -> [a]
reverse (DataConP -> [(Symbol, SpecType)]
dcpTyArgs DataConP
dp) ]
    fld :: Symbol -> Located Symbol
fld         = forall l b. Loc l => l -> b -> Located b
F.atLoc DataConP
dp 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 (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    = forall a b. [a] -> [b] -> [(a, b)]
zip (forall a. Symbolic a => a -> Symbol
F.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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> Int) -> Sort -> Sort
F.mapFVar (forall a. Num a => a -> a -> a
+ forall (t :: * -> *) a. Foldable t => t a -> Int
length [RTyVar]
as) forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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  = forall k v. HashMap k v -> [(k, v)]
M.toList forall a b. (a -> b) -> a -> b
$ forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' 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                     = forall k v.
(Eq k, Hashable k) =>
(v -> v -> v) -> [(k, v)] -> HashMap k v
M.fromListWith 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)           = forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert a
x (forall a. NamedThing a => a -> SrcSpan
Ghc.getSrcSpan a
x, SpecType
tx') HashMap a (SrcSpan, SpecType)
dcm
                                where
                                  tx' :: SpecType
tx' = forall b a. b -> (a -> b) -> Maybe a -> b
maybe SpecType
t (forall {a}.
(PPrint a, NamedThing a) =>
a -> SpecType -> (SrcSpan, SpecType) -> SpecType
meetX a
x SpecType
t) (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 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')      = forall a. PPrint a => [Char] -> a -> a
F.notracepp (forall {a} {b} {c}.
(PPrint a, PPrint b, PPrint c) =>
a -> b -> c -> [Char]
_msg a
x SpecType
t SpecType
t') forall a b. (a -> b) -> a -> b
$ TCEmb TyCon
-> Doc -> (SrcSpan, SpecType) -> (SrcSpan, SpecType) -> SpecType
meetVarTypes TCEmb TyCon
emb (forall a. PPrint a => a -> Doc
pprint a
x) (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: " forall a. [a] -> [a] -> [a]
++ 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 = 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    = 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  = (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 =
  forall a b. [([a], [b])] -> ([a], [b])
Misc.concatUnzip forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t 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 <- forall a. [Lookup a] -> Lookup [a]
catLookups forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (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)) forall a b. (a -> b) -> a -> b
$ [(Maybe DataDecl, Maybe (Located Symbol, [Variance]))]
gvs
  forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. [(a, b)] -> ([a], [b])
unzip [((ModName, TyConP, Maybe DataPropDecl), [Located DataConP])]
zong)
  where
    dcs :: [DataDecl]
dcs  = forall ty bndr. Spec ty bndr -> [DataDecl]
Ms.dataDecls BareSpec
spec
    vdcs :: [(Located Symbol, [Variance])]
vdcs = 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 = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList (forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap 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 = forall a b. (a -> Maybe b) -> [a] -> [b]
Mb.mapMaybe (forall {tv} {r}. RType BTyCon tv r -> Maybe Symbol
getTc forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Located a -> a
val) [Located (RType BTyCon tv r)]
ts
                    in [(Symbol
tc, (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
_) = forall a. a -> Maybe a
Just (forall a. Located a -> a
val forall a b. (a -> b) -> a -> b
$ BTyCon -> Located Symbol
btc_tc BTyCon
c)
        getTc RType BTyCon tv r
_ = 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [DataDecl]
dcs
  where smap :: DSizeMap
smap = [([LocBareType], Located Symbol)] -> DSizeMap
normalizeDSize forall a b. (a -> b) -> a -> b
$ 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 <- forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup (forall a. Symbolic a => a -> Symbol
F.symbol forall a b. (a -> b) -> a -> b
$ DataDecl -> DataName
tycName DataDecl
d) DSizeMap
smap
  = DataDecl
d {tycDCons :: Maybe [DataCtor]
tycDCons = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Symbol, [Symbol]) -> DataCtor -> DataCtor
makeSizeCtor (Symbol, [Symbol])
p)) (DataDecl -> Maybe [DataCtor]
tycDCons DataDecl
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 :: [(Symbol, BareType)]
dcFields = forall b c a. (b -> c) -> (a, b) -> (a, c)
Misc.mapSnd (forall c tv r.
(RType c tv r -> RType c tv r) -> RType c tv r -> RType c tv r
mapBot forall {c} {tv}. Symbolic c => RType c tv RReft -> RType c tv RReft
go) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DataCtor -> [(Symbol, BareType)]
dcFields DataCtor
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) | forall a. Symbolic a => a -> Symbol
F.symbol c
c forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Symbol]
xs
                        = 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 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  = 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))
                                      ))
                   forall a. Monoid a => a
mempty


catLookups :: [Bare.Lookup a] -> Bare.Lookup [a]
catLookups :: forall a. [Lookup a] -> Lookup [a]
catLookups = forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> Maybe b) -> [a] -> [b]
Mb.mapMaybe 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) = forall e a. [e] -> Maybe (Either [e] a)
left' (forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. TError t -> Bool
isErrResolve) [Error]
es)
skipResolve (Right a
v) = forall a. a -> Maybe a
Just (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' [] = forall a. Maybe a
Nothing
left' [e]
es = forall a. a -> Maybe a
Just (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 <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [DataDecl]
dataDecls 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
           forall (m :: * -> *) a. Monad m => a -> m a
return (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (, DataDecl
d) Maybe Symbol
k)
  case forall k v e.
(Eq k, Hashable k) =>
((k, [v]) -> Either e v) -> [(k, v)] -> Either e [v]
Misc.uniqueByKey' forall a. (a, [DataDecl]) -> Either [DataDecl] DataDecl
selectDD (forall a. [Maybe a] -> [a]
Mb.catMaybes [Maybe (Symbol, DataDecl)]
kds) of
    Left  [DataDecl]
decls  -> forall a b. a -> Either a b
Left [forall {t}. [DataDecl] -> TError t
err [DataDecl]
decls]
    Right [DataDecl]
decls  -> 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 $ -} forall t. Doc -> ListNE SrcSpan -> TError t
errDupSpecs (forall a. PPrint a => a -> Doc
pprint (DataDecl -> DataName
tycName DataDecl
d)) (forall a. Loc a => a -> SrcSpan
GM.fSrcSpan forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [DataDecl]
ds)
    err [DataDecl]
_        = forall a. Maybe SrcSpan -> [Char] -> a
impossible 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 ->
      forall (m :: * -> *) a. Monad m => a -> m a
return 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)
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just (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     = 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 = forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Symbolic a => a -> Symbol
F.symbol forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyCon -> [DataCon]
Ghc.tyConDataCons 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 <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall e r. Env -> ModName -> Either e r -> Either e (Maybe r)
Bare.failMaybe Env
env ModName
name 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" forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataCtor -> Located Symbol
dcName) [DataCtor]
cons
  let rdcs :: HashSet Symbol
rdcs = forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Symbolic a => a -> Symbol
F.symbol forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [Maybe a] -> [a]
Mb.catMaybes forall a b. (a -> b) -> a -> b
$ [Maybe DataCon]
mbDcs
  if HashSet Symbol
dcs forall a. Eq a => a -> a -> Bool
== HashSet Symbol
rdcs
    then forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM DataCtor -> Lookup DataCtor
checkDataCtorDupField [DataCtor]
cons
    else 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 -> Lookup DataCtor
checkDataCtorDupField DataCtor
d
  | Symbol
x : [Symbol]
_ <- [Symbol]
dups = forall a b. a -> Either a b
Left [forall {a} {a} {t}.
(PPrint a, PPrint a) =>
Located a -> a -> TError t
err Located Symbol
sym Symbol
x]
  | Bool
otherwise     = forall (m :: * -> *) a. Monad m => a -> m a
return DataCtor
d
    where
      sym :: Located Symbol
sym         = DataCtor -> Located Symbol
dcName   DataCtor
d
      xts :: [(Symbol, BareType)]
xts         = DataCtor -> [(Symbol, BareType)]
dcFields DataCtor
d
      dups :: [Symbol]
dups        = [ Symbol
x | (Symbol
x, [BareType]
ts) <- forall k v. (Eq k, Hashable k) => [(k, v)] -> [(k, [v])]
Misc.groupList [(Symbol, BareType)]
xts, Int
2 forall a. Ord a => a -> a -> Bool
<= forall (t :: * -> *) a. Foldable t => t a -> Int
length [BareType]
ts ]
      err :: Located a -> a -> TError t
err Located a
lc a
x    = forall t. SrcSpan -> Doc -> Doc -> TError t
ErrDupField (SourcePos -> SrcSpan
GM.sourcePosSrcSpan forall a b. (a -> b) -> a -> b
$ forall a. Located a -> SourcePos
loc Located a
lc) (forall a. PPrint a => a -> Doc
pprint forall a b. (a -> b) -> a -> b
$ forall a. Located a -> a
val Located a
lc) (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]) = 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 forall a. Eq a => a -> a -> Bool
== DataDeclKind
DataReflected ] of
                     [DataDecl
d] -> forall a b. b -> Either a b
Right DataDecl
d
                     [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     =  forall {a} {b}.
Symbolic a =>
[a]
-> [(Located Symbol, b)] -> [(Maybe a, Maybe (Located Symbol, b))]
merge (forall a. Ord a => [a] -> [a]
L.sort [DataDecl]
dcs) (forall a. (a -> a -> Ordering) -> [a] -> [a]
L.sortBy (\(Located Symbol, [Variance])
x (Located Symbol, [Variance])
y -> forall a. Ord a => a -> a -> Ordering
compare (forall a b. (a, b) -> a
fst (Located Symbol, [Variance])
x) (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)
      | forall a. Symbolic a => a -> Symbol
F.symbol a
d forall a. Eq a => a -> a -> Bool
== forall {c} {b}. (Located c, b) -> c
sym (Located Symbol, b)
v = (forall a. a -> Maybe a
Just a
d, forall a. a -> Maybe a
Just (Located Symbol, b)
v)  forall a. a -> [a] -> [a]
: [a]
-> [(Located Symbol, b)] -> [(Maybe a, Maybe (Located Symbol, b))]
merge [a]
ds [(Located Symbol, b)]
vs
      | forall a. Symbolic a => a -> Symbol
F.symbol a
d forall a. Ord a => a -> a -> Bool
<  forall {c} {b}. (Located c, b) -> c
sym (Located Symbol, b)
v = (forall a. a -> Maybe a
Just a
d, forall a. Maybe a
Nothing) forall a. a -> [a] -> [a]
: [a]
-> [(Located Symbol, b)] -> [(Maybe a, Maybe (Located Symbol, b))]
merge [a]
ds ((Located Symbol, b)
vforall a. a -> [a] -> [a]
:[(Located Symbol, b)]
vs)
      | Bool
otherwise           = (forall a. Maybe a
Nothing, forall a. a -> Maybe a
Just (Located Symbol, b)
v) forall a. a -> [a] -> [a]
: [a]
-> [(Located Symbol, b)] -> [(Maybe a, Maybe (Located Symbol, b))]
merge (a
dforall a. a -> [a] -> [a]
:[a]
ds) [(Located Symbol, b)]
vs
    merge []     [(Located Symbol, b)]
vs         = (forall a. Maybe a
Nothing,) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a
Just forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Located Symbol, b)]
vs
    merge [a]
ds     []         = (,forall a. Maybe a
Nothing) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a
Just forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [a]
ds
    sym :: (Located c, b) -> c
sym                     = forall a. Located a -> a
val forall b c a. (b -> c) -> (a -> b) -> a -> 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 = forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
_msg (Bool
isGADT Bool -> Bool -> Bool
|| Int
cN forall a. Eq a => a -> a -> Bool
== Int
dN Bool -> Bool -> Bool
|| forall (t :: * -> *) a. Foldable t => t a -> Bool
null (DataDecl -> Maybe [DataCtor]
tycDCons DataDecl
d))
  where
    _msg :: [Char]
_msg          = forall r. PrintfType r => [Char] -> r
printf [Char]
"checkDataDecl: D = %s, c = %s, cN = %d, dN = %d" (forall a. Show a => a -> [Char]
show DataDecl
d) (forall a. Show a => a -> [Char]
show TyCon
c) Int
cN Int
dN
    cN :: Int
cN            = forall (t :: * -> *) a. Foldable t => t a -> Int
length (TyCon -> [Var]
GM.tyConTyVarsDef TyCon
c)
    dN :: Int
dN            = 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 -> forall (m :: * -> *) a. Monad m => a -> m a
return TyCon
tc
    Maybe TyCon
Nothing -> forall a b. a -> Either a b
Left [ forall t. SrcSpan -> Doc -> Doc -> TError t
ErrBadData (forall a. Loc a => a -> SrcSpan
GM.fSrcSpan DataName
dn) (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 BareType
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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [PVar BSort]
ps
  let αs :: [RTyVar]
αs           = Var -> RTyVar
RTV forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Var
GM.symbolTyVar forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol]
as
  let n :: Int
n            = forall (t :: * -> *) a. Foldable t => t a -> Int
length [RTyVar]
αs
  let initmap :: [(UsedPVar, Int)]
initmap      = forall a b. [a] -> [b] -> [(a, b)]
zip (forall t. PVar t -> UsedPVar
RT.uPVar 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'            <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Env
-> ModName
-> SourcePos
-> SourcePos
-> TyCon
-> [RTyVar]
-> [PVar BSort]
-> [RPVar]
-> DataCtor
-> Lookup DataConP
ofBDataCtor Env
env ModName
name SourcePos
lc SourcePos
lc' TyCon
tc' [RTyVar]
αs [PVar BSort]
ps [RPVar]
πs) (forall a. a -> Maybe a -> a
Mb.fromMaybe [] Maybe [DataCtor]
cts)
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (TyCon -> DataDecl -> Bool
checkDataDecl TyCon
tc' DataDecl
dd) (forall a b. a -> Either a b
Left [forall {t}. TError t
err])
  let pd :: Maybe SpecType
pd           = Env
-> ModName
-> SourcePos
-> Maybe [PVar BSort]
-> BareType
-> SpecType
Bare.ofBareType Env
env ModName
name SourcePos
lc (forall a. a -> Maybe a
Just []) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. PPrint a => [Char] -> a -> a
F.tracepp [Char]
"ofBDataDecl-prop" Maybe BareType
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      = forall a. Eq a => [a] -> [a]
L.nub forall a b. (a -> b) -> a -> b
$  forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (forall a. [(UsedPVar, a)] -> Bool -> SpecType -> [(a, Bool)]
getPsSig [(UsedPVar, Int)]
initmap Bool
True) [SpecType]
tys
  let defPs :: [Variance]
defPs        = forall a. Eq a => [(a, Bool)] -> a -> Variance
varSignToVariance [(Int, Bool)]
varInfo forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Int
0 .. (forall (t :: * -> *) a. Foldable t => t a -> Int
length [RPVar]
πs 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 = forall a. Int -> [a] -> [a]
drop Int
n [Variance]
is in
                                      (forall a. Int -> [a] -> [a]
take Int
n [Variance]
is, if 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
  forall (m :: * -> *) a. Monad m => a -> m a
return ((ModName
name, TyConP
tcp, forall a. a -> Maybe a
Just (DataDecl
dd { tycDCons :: Maybe [DataCtor]
tycDCons = Maybe [DataCtor]
cts }, Maybe SpecType
pd)), forall a. SourcePos -> SourcePos -> a -> Located a
Loc SourcePos
lc SourcePos
lc' forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [DataConP]
cts')
  where
    err :: TError t
err            = forall t. SrcSpan -> Doc -> Doc -> TError t
ErrBadData (forall a. Loc a => a -> SrcSpan
GM.fSrcSpan DataName
tc) (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    -> forall a b. a -> Either a b
Left [Error]
e
    Right TyCon
tc' -> 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 forall a. [a]
tcontr forall a. Maybe a
Nothing, 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
  = forall a. Maybe SrcSpan -> [Char] -> a
panic 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
-> Lookup 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)
  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 [BareType]
_ [(Symbol, BareType)]
xts Maybe BareType
res) DataCon
c' =
  DataConP
    { dcpLoc :: SourcePos
dcpLoc        = SourcePos
l
    , dcpCon :: DataCon
dcpCon        = DataCon
c'
    , dcpFreeTyVars :: [RTyVar]
dcpFreeTyVars = Symbol -> RTyVar
RT.symbolRTyVar 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     = 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]
-> BareType
-> SpecType
Bare.ofBareType Env
env ModName
name SourcePos
l (forall a. a -> Maybe a
Just [PVar BSort]
ps) 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 (forall a. a -> Maybe a
Just [PVar BSort]
ps) 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          = forall t. HasConfig t => t -> Config
getConfig Env
env
    ([(Symbol, SpecType)]
yts, SpecType
ot)     = forall a.
Bool
-> ModName
-> Located a
-> ([(Symbol, SpecType)], SpecType)
-> ([(Symbol, SpecType)], SpecType)
qualifyDataCtor (Bool -> Bool
not Bool
isGadt) ModName
name Located ()
dLoc (forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
xs [SpecType]
ts', SpecType
t0')
    zts :: [(Symbol, SpecType)]
zts           = forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (forall a. DataCon -> Int -> (Symbol, a) -> (Symbol, a)
normalizeField DataCon
c') [Int
1..] (forall a. [a] -> [a]
reverse [(Symbol, SpecType)]
yts)
    usedTvs :: HashSet RTyVar
usedTvs       = forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList (forall tv s. RTVar tv s -> tv
ty_var_value forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap forall tv c r. Eq tv => RType c tv r -> [RTVar tv (RType c tv ())]
RT.freeTyVars (SpecType
t0'forall a. a -> [a] -> [a]
:[SpecType]
ts'))
    cs :: [SpecType]
cs            = [ SpecType
p | SpecType
p <- forall r. Monoid r => Type -> RRType r
RT.ofType 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)      = 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 -> forall a. TyCon -> [RTyVar] -> [PVar a] -> SpecType
RT.gApp TyCon
tc [RTyVar]
αs [RPVar]
πs
                      Just Type
ty -> forall r. Monoid r => Type -> RRType r
RT.ofType Type
ty
    isGadt :: Bool
isGadt        = forall a. Maybe a -> Bool
Mb.isJust Maybe BareType
res
    dLoc :: Located ()
dLoc          = 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 = forall t. SrcSpan -> Doc -> [Doc] -> [Doc] -> TError t
ErrDataConMismatch SrcSpan
sp Doc
v (forall a. PPrint a => a -> Doc
ppTicks forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. HashSet a -> [a]
S.toList HashSet Symbol
dcs) (forall a. PPrint a => a -> Doc
ppTicks forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. HashSet a -> [a]
S.toList HashSet Symbol
rdcs)
  where
    v :: Doc
v                 = forall a. PPrint a => a -> Doc
pprint (forall a. Located a -> a
val Located Symbol
d)
    sp :: SrcSpan
sp                = SourcePos -> SrcSpan
GM.sourcePosSrcSpan (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 forall a. (a -> Bool) -> [a] -> [a]
filter (\(a, Bool)
p -> forall a b. (a, b) -> a
fst (a, Bool)
p 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 RTVU RTyCon RTyVar
_ SpecType
t RReft
r)
  = forall a b t. [(UsedPVar, a)] -> b -> UReft t -> [(a, b)]
addps [(UsedPVar, a)]
m Bool
pos RReft
r forall a. [a] -> [a] -> [a]
++  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)
  = forall a b t. [(UsedPVar, a)] -> b -> UReft t -> [(a, b)]
addps [(UsedPVar, a)]
m Bool
pos RReft
r forall a. [a] -> [a] -> [a]
++ forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (forall a. [(UsedPVar, a)] -> Bool -> SpecType -> [(a, Bool)]
getPsSig [(UsedPVar, a)]
m Bool
pos) [SpecType]
ts
    forall a. [a] -> [a] -> [a]
++ forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (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)
  = 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)
  = forall a b t. [(UsedPVar, a)] -> b -> UReft t -> [(a, b)]
addps [(UsedPVar, a)]
m Bool
pos RReft
r forall a. [a] -> [a] -> [a]
++ forall a. [(UsedPVar, a)] -> Bool -> SpecType -> [(a, Bool)]
getPsSig [(UsedPVar, a)]
m Bool
pos SpecType
t1 forall a. [a] -> [a] -> [a]
++ 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)
  = forall a b t. [(UsedPVar, a)] -> b -> UReft t -> [(a, b)]
addps [(UsedPVar, a)]
m Bool
pos RReft
r forall a. [a] -> [a] -> [a]
++ forall a. [(UsedPVar, a)] -> Bool -> SpecType -> [(a, Bool)]
getPsSig [(UsedPVar, a)]
m Bool
pos SpecType
t2 forall a. [a] -> [a] -> [a]
++ 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)
  = 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
  = forall a. Maybe SrcSpan -> [Char] -> a
panic forall a. Maybe a
Nothing forall a b. (a -> b) -> a -> b
$ [Char]
"getPsSig" forall a. [a] -> [a] -> [a]
++ 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)) = 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) = 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) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {t}. PVar t -> a
f  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Predicate -> [UsedPVar]
pvars Predicate
ps
  where
    f :: PVar t -> a
f = forall a. a -> Maybe a -> a
Mb.fromMaybe (forall a. Maybe SrcSpan -> [Char] -> a
panic forall a. Maybe a
Nothing [Char]
"Bare.addPs: notfound") forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a b. Eq a => a -> [(a, b)] -> Maybe b
`L.lookup` [(UsedPVar, a)]
m) forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = 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) = forall a. PPrint a => [Char] -> a -> a
F.notracepp ([Char]
"dataConResultTy-3 : vanilla = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (DataCon -> Bool
Ghc.isVanillaDataCon DataCon
c) forall a. [a] -> [a] -> [a]
++ [Char]
" : ") SpecType
t
dataConResultTy DataCon
c [RTyVar]
_ SpecType
t Maybe SpecType
_
  | DataCon -> Bool
Ghc.isVanillaDataCon DataCon
c     = forall a. PPrint a => [Char] -> a -> a
F.notracepp ([Char]
"dataConResultTy-1 : " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
F.showpp DataCon
c) SpecType
t
  | Bool
otherwise                  = forall a. PPrint a => [Char] -> a -> a
F.notracepp ([Char]
"dataConResultTy-2 : " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
F.showpp DataCon
c) forall a b. (a -> b) -> a -> b
$ 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 forall a. Eq a => a -> a -> Bool
== TyCon
Ghc.eqPrimTyCon = forall a. a -> Maybe a
Just (RTyVar
a, SpecType
t)
eqSubst 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 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'        = forall a. Subable a => Subst -> a -> a
F.subst Subst
su forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SpecType
st
   xts' :: [(Symbol, SpecType)]
xts'      = [ (Symbol
qx, 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, 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 (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 = (forall a. a -> Maybe a
Just Symbol
x, forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
msg forall a b. (a -> b) -> a -> b
$ ModName -> Symbol -> Symbol
qualifyModName ModName
name Symbol
x)
 | Bool
otherwise = (forall a. Maybe a
Nothing, Symbol
x)
 where
   msg :: [Char]
msg       = [Char]
"QUALIFY-NAME: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Symbol
x forall a. [a] -> [a] -> [a]
++ [Char]
" in module " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (forall a. Symbolic a => a -> Symbol
F.symbol ModName
name)
   x :: Symbol
x         = 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, forall {b} {a}.
(PPrint b, PPrint a) =>
a -> [Located b] -> Located b
take1 Var
v [LocSpecType]
lspecTys) | (Var
v, [LocSpecType]
lspecTys) <- 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 forall k a. (Eq k, Hashable k) => (a -> k) -> [a] -> [a]
Misc.nubHashOn (forall a. PPrint a => a -> [Char]
showpp forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Located a -> a
val) [Located b]
lsts of
                                [Located b
t]    -> Located b
t
                                (Located b
t:[Located b]
ts) -> forall a e. Exception e => e -> a
Ex.throw (forall t. SrcSpan -> Doc -> ListNE SrcSpan -> TError t
ErrDupSpecs (forall a. Loc a => a -> SrcSpan
GM.fSrcSpan Located b
t) (forall a. PPrint a => a -> Doc
pprint a
v) (forall a. Loc a => a -> SrcSpan
GM.fSrcSpan forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Located b]
ts) :: Error)
                                [Located b]
_      -> forall a. Maybe SrcSpan -> [Char] -> a
impossible forall a. Maybe a
Nothing [Char]
"checkRecordSelectorSigs"


strengthenClassSel :: Ghc.Var -> LocSpecType -> LocSpecType
strengthenClassSel :: Var -> LocSpecType -> LocSpecType
strengthenClassSel Var
v LocSpecType
lt = LocSpecType
lt { val :: SpecType
val = SpecType
st }
 where
  st :: SpecType
st = forall r a. Reader r a -> r -> a
runReader (SpecType -> Reader (Int, [Symbol]) SpecType
go (forall a. Located a -> a
F.val LocSpecType
lt)) (Int
1, [])
  s :: Located Symbol
s = 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 forall a. Num a => a -> a -> a
+ Int
1, Symbol
x forall a. a -> [a] -> [a]
: [Symbol]
xs)
  go :: SpecType -> Reader (Int, [F.Symbol]) SpecType
  go :: SpecType -> Reader (Int, [Symbol]) SpecType
go (RAllT RTVU RTyCon RTyVar
a SpecType
t RReft
r) = forall c tv r. RTVU c tv -> RType c tv r -> r -> RType c tv r
RAllT RTVU RTyCon RTyVar
a forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SpecType -> Reader (Int, [Symbol]) SpecType
go SpecType
t forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure RReft
r
  go (RAllP RPVar
p SpecType
t  ) = forall c tv r. PVU c tv -> RType c tv r -> RType c tv r
RAllP RPVar
p 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) | forall c t t1. TyConable c => RType c t t1 -> Bool
isEmbeddedClass SpecType
tx =
    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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SpecType -> Reader (Int, [Symbol]) SpecType
go SpecType
t forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
reader forall a b. (a, b) -> a
fst
    RReft
r' <- forall a. Symbolic a => Located Symbol -> [a] -> RReft
singletonApp Located Symbol
s forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall a. [a] -> [a]
L.reverse forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
reader forall a b. (a, b) -> b
snd)
    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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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) forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall r. Reftable r => r -> r -> r
F.meet RReft
r RReft
r')
  go SpecType
t = forall r c tv. Reftable r => RType c tv r -> r -> RType c tv r
RT.strengthen SpecType
t forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Symbolic a => Located Symbol -> [a] -> RReft
singletonApp Located Symbol
s forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> [a]
L.reverse forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
reader 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 = forall r. r -> Predicate -> UReft r
MkUReft Reft
r forall a. Monoid a => a
mempty
  where r :: Reft
r = forall a. Expression a => a -> Reft
F.exprReft (Located Symbol -> [Expr] -> Expr
F.mkEApp Located Symbol
s (forall a. Symbolic a => a -> Expr
F.eVar 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 forall a. Eq a => a -> a -> Bool
/= Symbol
F.dummySymbol = Symbol
x
            | Bool
otherwise          = forall a. Symbolic a => a -> Symbol
F.symbol ([Char]
"_cls_lq" forall a. [a] -> [a] -> [a]
++ 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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
        forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Var -> LocSpecType -> LocSpecType
strengthenClassSel)
          [(Var
v, forall a. SourcePos -> SourcePos -> a -> Located a
Loc SourcePos
l SourcePos
l' SpecType
t)| (Var
v,SpecType
t) <- forall a b. [a] -> [b] -> [(a, b)]
zip [Var]
cfs (forall a. [a] -> [a]
reverse forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a, b) -> b
snd [(Symbol, SpecType)]
args)]
    | forall (t :: * -> *) a. Foldable t => t a -> Bool
null [FieldLabel]
fls                    --    no field labels
    Bool -> Bool -> Bool
|| forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (forall t t1 t2. RType t t1 t2 -> Bool
isFunTy forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) [(Symbol, SpecType)]
args Bool -> Bool -> Bool
&& Bool -> Bool
not (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) <- 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  = forall a.
(NamedThing a, Symbolic a) =>
Env -> ModName -> a -> Maybe Var
Bare.lookupGhcNamedVar Env
env ModName
name forall b c a. (b -> c) -> (a -> b) -> a -> c
. FieldLabel -> Name
Ghc.flSelector forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [FieldLabel]
fls
      ts :: [ LocSpecType ]
      ts :: [LocSpecType]
ts = [ forall a. SourcePos -> SourcePos -> a -> Located a
Loc SourcePos
l SourcePos
l' (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 (forall a b. (a -> b) -> [a] -> [b]
map (, forall a. Monoid a => a
mempty) (forall tv s. tv -> RTVar tv s
makeRTVar 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, forall a. Monoid a => a
mempty)]
                                 (forall {r}.
RType RTyCon RTyVar (UReft r) -> RType RTyCon RTyVar (UReft r)
dropPreds (forall a. Subable a => Subst -> a -> a
F.subst Subst
su SpecType
t forall r c tv. Reftable r => RType c tv r -> r -> RType c tv r
`RT.strengthen` RReft
mt)))
             | (Symbol
x, SpecType
t) <- forall a. [a] -> [a]
reverse [(Symbol, SpecType)]
args -- NOTE: the reverse here is correct
             , let vv :: Symbol
vv = 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 <- forall a b. (a, b) -> a
fst 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  = 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 = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(MkUReft r
r Predicate
_ps) -> forall r. r -> Predicate -> UReft r
MkUReft r
r forall a. Monoid a => a
mempty)