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

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

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

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

  , dataDeclSize
  ) where

import qualified Control.Exception                      as Ex
import           Control.Monad (forM, unless)
import           Control.Monad.Reader
import qualified Data.List                              as L
import qualified Data.HashMap.Strict                    as M
import qualified Data.HashSet                           as S
import qualified Data.Maybe                             as Mb

import qualified Language.Fixpoint.Types                as F
import qualified Language.Haskell.Liquid.GHC.Misc       as GM
import qualified Liquid.GHC.API        as Ghc
import           Language.Haskell.Liquid.Types.DataDecl
import           Language.Haskell.Liquid.Types.Errors
import           Language.Haskell.Liquid.Types.Names
import           Language.Haskell.Liquid.Types.PredType (dataConPSpecType)
import qualified Language.Haskell.Liquid.Types.RefType  as RT
import           Language.Haskell.Liquid.Types.RType
import           Language.Haskell.Liquid.Types.RTypeOp
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           Language.Haskell.Liquid.UX.Config
import qualified Text.PrettyPrint.HughesPJ as PJ
import           Text.Printf                     (printf)
import Text.PrettyPrint ((<+>))

--------------------------------------------------------------------------------
-- | 'DataConMap' stores the names of those ctor-fields that have been declared
--   as SMT ADTs so we don't make up new names for them.
--------------------------------------------------------------------------------
dataConMap :: [F.DataDecl] -> Bare.DataConMap
dataConMap :: [DataDecl] -> DataConMap
dataConMap [DataDecl]
ds = [((Symbol, Int), Symbol)] -> DataConMap
forall k v. 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
  d     <- [DataDecl]
ds
  c     <- F.ddCtors d
  let 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
  zip ((F.symbol c,) <$> [1..]) 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. Hashable k => v -> k -> HashMap k v -> v
M.lookupDefault Symbol
def (DataCon -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol DataCon
d, Int
i) DataConMap
dm
  where
    dm :: DataConMap
dm                       = DataConMap -> Maybe DataConMap -> DataConMap
forall a. a -> Maybe a -> a
Mb.fromMaybe DataConMap
forall k v. HashMap k v
M.empty Maybe DataConMap
dmMb
    def :: Symbol
def                      = DataCon -> Int -> Symbol
makeDataConSelector' DataCon
d Int
i


makeDataConSelector' :: Ghc.DataCon -> Int -> F.Symbol
makeDataConSelector' :: DataCon -> Int -> Symbol
makeDataConSelector' DataCon
d Int
i
  = [Char] -> Symbol -> Maybe Int -> Symbol
symbolMeasure [Char]
"$select" (DataCon -> Symbol
dcSymbol DataCon
d) (Int -> Maybe Int
forall a. a -> Maybe a
Just Int
i)

dcSymbol :: Ghc.DataCon -> F.Symbol
dcSymbol :: DataCon -> Symbol
dcSymbol = {- simpleSymbolVar -} Var -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol (Var -> Symbol) -> (DataCon -> Var) -> DataCon -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataCon -> Var
Ghc.dataConWorkId

symbolMeasure :: String -> F.Symbol -> Maybe Int -> F.Symbol
symbolMeasure :: [Char] -> Symbol -> Maybe Int -> Symbol
symbolMeasure [Char]
f Symbol
d Maybe Int
iMb = (Symbol -> Symbol -> Symbol) -> [Symbol] -> Symbol
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 Symbol -> Symbol -> Symbol
F.suffixSymbol (Symbol
dcPrefix Symbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
: [Char] -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol [Char]
f Symbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
: Symbol
d Symbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
: [Symbol]
rest)
  where
    rest :: [Symbol]
rest          = [Symbol] -> (Int -> [Symbol]) -> Maybe Int -> [Symbol]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] (Symbol -> [Symbol]
forall t. t -> [t]
Misc.single (Symbol -> [Symbol]) -> (Int -> Symbol) -> Int -> [Symbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol ([Char] -> Symbol) -> (Int -> [Char]) -> Int -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> [Char]
forall a. Show a => a -> [Char]
show) Maybe Int
iMb


--------------------------------------------------------------------------------
-- | makeClassEmbeds: sort-embeddings for numeric, and family-instance tycons
--------------------------------------------------------------------------------
addClassEmbeds :: Maybe [Ghc.ClsInst] -> [Ghc.TyCon] -> F.TCEmb Ghc.TyCon
               -> F.TCEmb Ghc.TyCon
addClassEmbeds :: Maybe [ClsInst] -> [TyCon] -> TCEmb TyCon -> TCEmb TyCon
addClassEmbeds Maybe [ClsInst]
instenv [TyCon]
fiTcs = [TyCon] -> TCEmb TyCon -> TCEmb TyCon
makeFamInstEmbeds [TyCon]
fiTcs (TCEmb TyCon -> TCEmb TyCon)
-> (TCEmb TyCon -> TCEmb TyCon) -> TCEmb TyCon -> TCEmb TyCon
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe [ClsInst] -> TCEmb TyCon -> TCEmb TyCon
makeNumEmbeds Maybe [ClsInst]
instenv

--------------------------------------------------------------------------------
-- | makeFamInstEmbeds : embed family instance tycons, see [NOTE:FamInstEmbeds]
--------------------------------------------------------------------------------
--     Query.R$58$EntityFieldBlobdog
--   with the actual family instance  types that have numeric instances as int [Check!]
--------------------------------------------------------------------------------
makeFamInstEmbeds :: [Ghc.TyCon] -> F.TCEmb Ghc.TyCon -> F.TCEmb Ghc.TyCon
makeFamInstEmbeds :: [TyCon] -> TCEmb TyCon -> TCEmb TyCon
makeFamInstEmbeds [TyCon]
cs0 TCEmb TyCon
embeds = (TCEmb TyCon -> (TyCon, Sort) -> TCEmb TyCon)
-> TCEmb TyCon -> [(TyCon, Sort)] -> TCEmb TyCon
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' TCEmb TyCon -> (TyCon, Sort) -> TCEmb TyCon
forall {a}. Hashable a => TCEmb a -> (a, Sort) -> TCEmb a
embed TCEmb TyCon
embeds [(TyCon, Sort)]
famInstSorts
  where
    famInstSorts :: [(TyCon, Sort)]
famInstSorts          = [Char] -> [(TyCon, Sort)] -> [(TyCon, Sort)]
forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"famInstTcs"
                            [ (TyCon
c, TCEmb TyCon -> Type -> Sort
RT.typeSort TCEmb TyCon
embeds Type
ty)
                                | TyCon
c   <- [TyCon]
cs
                                , Type
ty  <- Maybe Type -> [Type]
forall a. Maybe a -> [a]
Mb.maybeToList (TyCon -> Maybe Type
RT.famInstTyConType TyCon
c) ]
    embed :: TCEmb a -> (a, Sort) -> TCEmb a
embed TCEmb a
embs (a
c, Sort
t)     = a -> Sort -> TCArgs -> TCEmb a -> TCEmb a
forall a.
(Eq a, Hashable a) =>
a -> Sort -> TCArgs -> TCEmb a -> TCEmb a
F.tceInsert a
c Sort
t TCArgs
F.NoArgs TCEmb a
embs
    cs :: [TyCon]
cs                    = [Char] -> [TyCon] -> [TyCon]
forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
"famInstTcs-all" [TyCon]
cs0

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

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

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

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

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

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

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

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

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

     (1) EntityField Blob Int,

     or

     (2) R$58$EntityFieldBlobdog Int

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

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

        R$58$EntityFieldBlobdog :-> EntityField Blob

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

 -}

--------------------------------------------------------------------------------
-- | makeNumEmbeds: embed types that have numeric instances as int [Check!]
--------------------------------------------------------------------------------
makeNumEmbeds :: Maybe [Ghc.ClsInst] -> F.TCEmb Ghc.TyCon -> F.TCEmb Ghc.TyCon
makeNumEmbeds :: Maybe [ClsInst] -> TCEmb TyCon -> TCEmb TyCon
makeNumEmbeds Maybe [ClsInst]
Nothing TCEmb TyCon
x   = TCEmb TyCon
x
makeNumEmbeds (Just [ClsInst]
is) TCEmb TyCon
x = (TCEmb TyCon -> ClsInst -> TCEmb TyCon)
-> TCEmb TyCon -> [ClsInst] -> TCEmb TyCon
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' TCEmb TyCon -> ClsInst -> TCEmb TyCon
makeNumericInfoOne TCEmb TyCon
x [ClsInst]
is

makeNumericInfoOne :: F.TCEmb Ghc.TyCon -> Ghc.ClsInst -> F.TCEmb Ghc.TyCon
makeNumericInfoOne :: TCEmb TyCon -> ClsInst -> TCEmb TyCon
makeNumericInfoOne TCEmb TyCon
m ClsInst
is
  | TyCon -> Bool
forall c. TyConable c => c -> Bool
isFracCls TyCon
cls, Just TyCon
tc <- ClsInst -> Maybe TyCon
instanceTyCon ClsInst
is
  = (Sort -> Sort -> Sort)
-> TyCon -> Sort -> TCArgs -> TCEmb TyCon -> TCEmb TyCon
forall a.
(Eq a, Hashable a) =>
(Sort -> Sort -> Sort) -> a -> Sort -> TCArgs -> TCEmb a -> TCEmb a
F.tceInsertWith ((Sort -> Sort -> Sort) -> Sort -> Sort -> Sort
forall a b c. (a -> b -> c) -> b -> a -> c
flip Sort -> Sort -> Sort
mappendSortFTC) TyCon
tc (TyCon -> Bool -> Bool -> Sort
ftc TyCon
tc Bool
True Bool
True) TCArgs
F.NoArgs TCEmb TyCon
m
  | TyCon -> Bool
forall c. TyConable c => c -> Bool
isNumCls  TyCon
cls, Just TyCon
tc <- ClsInst -> Maybe TyCon
instanceTyCon ClsInst
is
  = (Sort -> Sort -> Sort)
-> TyCon -> Sort -> TCArgs -> TCEmb TyCon -> TCEmb TyCon
forall a.
(Eq a, Hashable a) =>
(Sort -> Sort -> Sort) -> a -> Sort -> TCArgs -> TCEmb a -> TCEmb a
F.tceInsertWith ((Sort -> Sort -> Sort) -> Sort -> Sort -> Sort
forall a b c. (a -> b -> c) -> b -> a -> c
flip Sort -> Sort -> Sort
mappendSortFTC) TyCon
tc (TyCon -> Bool -> Bool -> Sort
ftc TyCon
tc Bool
True Bool
False) TCArgs
F.NoArgs TCEmb TyCon
m
  | Bool
otherwise
  = TCEmb TyCon
m
  where
    cls :: TyCon
cls         = Class -> TyCon
Ghc.classTyCon (ClsInst -> Class
Ghc.is_cls ClsInst
is)
    ftc :: TyCon -> Bool -> Bool -> Sort
ftc TyCon
c Bool
f1 Bool
f2 = FTycon -> Sort
F.FTC (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 -> [Char] -> Sort
forall a. HasCallStack => Maybe SrcSpan -> [Char] -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing ([Char]
"mappendSortFTC: s1 = " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Sort -> [Char]
forall a. PPrint a => a -> [Char]
showpp Sort
s1 [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" s2 = " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Sort -> [Char]
forall a. PPrint a => a -> [Char]
showpp Sort
s2)

instanceTyCon :: Ghc.ClsInst -> Maybe Ghc.TyCon
instanceTyCon :: ClsInst -> Maybe TyCon
instanceTyCon = [Type] -> Maybe TyCon
go ([Type] -> Maybe TyCon)
-> (ClsInst -> [Type]) -> ClsInst -> Maybe TyCon
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ClsInst -> [Type]
Ghc.is_tys
  where
    go :: [Type] -> Maybe TyCon
go [Ghc.TyConApp TyCon
c [Type]
_] = TyCon -> Maybe TyCon
forall a. a -> Maybe a
Just TyCon
c
    go [Type]
_                  = Maybe TyCon
forall a. Maybe a
Nothing

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

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

type DataPropDecl = (DataDecl, Maybe SpecType)

makeDataDecls :: F.TCEmb Ghc.TyCon -> ModName
              -> [(ModName, Ghc.TyCon, DataPropDecl)]
              -> [Located DataConP]
              -> (Diagnostics, [F.DataDecl])
makeDataDecls :: TCEmb TyCon
-> ModName
-> [(ModName, TyCon, DataPropDecl)]
-> [Located DataConP]
-> (Diagnostics, [DataDecl])
makeDataDecls TCEmb TyCon
tce ModName
name [(ModName, TyCon, DataPropDecl)]
tds [Located DataConP]
ds = ([Warning] -> [Error] -> Diagnostics
mkDiagnostics [Warning]
warns [], [DataDecl]
okDecs)
  where
    warns :: [Warning]
warns            =
      (Located Doc -> Warning
mkWarnDecl (Located Doc -> Warning)
-> ((TyCon, (DataPropDecl, [(DataCon, DataConP)])) -> Located Doc)
-> (TyCon, (DataPropDecl, [(DataCon, DataConP)]))
-> Warning
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (LHName -> Doc) -> Located LHName -> Located Doc
forall a b. (a -> b) -> Located a -> Located b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap LHName -> Doc
forall a. PPrint a => a -> Doc
pprint (Located LHName -> Located Doc)
-> ((TyCon, (DataPropDecl, [(DataCon, DataConP)]))
    -> Located LHName)
-> (TyCon, (DataPropDecl, [(DataCon, DataConP)]))
-> Located Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataName -> Located LHName
dataNameSymbol (DataName -> Located LHName)
-> ((TyCon, (DataPropDecl, [(DataCon, DataConP)])) -> DataName)
-> (TyCon, (DataPropDecl, [(DataCon, DataConP)]))
-> Located LHName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataDeclP Symbol BareType -> DataName
forall v ty. DataDeclP v ty -> DataName
tycName (DataDeclP Symbol BareType -> DataName)
-> ((TyCon, (DataPropDecl, [(DataCon, DataConP)]))
    -> DataDeclP Symbol BareType)
-> (TyCon, (DataPropDecl, [(DataCon, DataConP)]))
-> DataName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataPropDecl -> DataDeclP Symbol BareType
forall a b. (a, b) -> a
fst (DataPropDecl -> DataDeclP Symbol BareType)
-> ((TyCon, (DataPropDecl, [(DataCon, DataConP)])) -> DataPropDecl)
-> (TyCon, (DataPropDecl, [(DataCon, DataConP)]))
-> DataDeclP Symbol BareType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (DataPropDecl, [(DataCon, DataConP)]) -> DataPropDecl
forall a b. (a, b) -> a
fst ((DataPropDecl, [(DataCon, DataConP)]) -> DataPropDecl)
-> ((TyCon, (DataPropDecl, [(DataCon, DataConP)]))
    -> (DataPropDecl, [(DataCon, DataConP)]))
-> (TyCon, (DataPropDecl, [(DataCon, DataConP)]))
-> DataPropDecl
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TyCon, (DataPropDecl, [(DataCon, DataConP)]))
-> (DataPropDecl, [(DataCon, DataConP)])
forall a b. (a, b) -> b
snd ((TyCon, (DataPropDecl, [(DataCon, DataConP)])) -> Warning)
-> [(TyCon, (DataPropDecl, [(DataCon, DataConP)]))] -> [Warning]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(TyCon, (DataPropDecl, [(DataCon, DataConP)]))]
badTcs) [Warning] -> [Warning] -> [Warning]
forall a. [a] -> [a] -> [a]
++
      (Located Doc -> Warning
mkWarnDecl (Located Doc -> Warning)
-> (DataDecl -> Located Doc) -> DataDecl -> Warning
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\DataDecl
d -> DataDecl -> Doc -> Located Doc
forall l b. Loc l => l -> b -> Located b
F.atLoc DataDecl
d (Symbol -> Doc
forall a. PPrint a => a -> Doc
pprint (Symbol -> Doc) -> Symbol -> Doc
forall a b. (a -> b) -> a -> b
$ DataDecl -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol DataDecl
d)) (DataDecl -> Warning) -> [DataDecl] -> [Warning]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [DataDecl]
badDecs)
    tds' :: [(TyCon, (ModName, DataPropDecl))]
tds'             = ModName
-> [(ModName, TyCon, DataPropDecl)]
-> [(TyCon, (ModName, DataPropDecl))]
resolveTyCons ModName
name [(ModName, TyCon, DataPropDecl)]
tds
    tcDds :: [(TyCon, (DataPropDecl, [(DataCon, DataConP)]))]
tcDds            = ((TyCon, (DataPropDecl, [(DataCon, DataConP)])) -> Bool)
-> [(TyCon, (DataPropDecl, [(DataCon, DataConP)]))]
-> [(TyCon, (DataPropDecl, [(DataCon, DataConP)]))]
forall a. (a -> Bool) -> [a] -> [a]
filter ((TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
/= TyCon
Ghc.listTyCon) (TyCon -> Bool)
-> ((TyCon, (DataPropDecl, [(DataCon, DataConP)])) -> TyCon)
-> (TyCon, (DataPropDecl, [(DataCon, DataConP)]))
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TyCon, (DataPropDecl, [(DataCon, DataConP)])) -> TyCon
forall a b. (a, b) -> a
fst)
                     ([(TyCon, (DataPropDecl, [(DataCon, DataConP)]))]
 -> [(TyCon, (DataPropDecl, [(DataCon, DataConP)]))])
-> [(TyCon, (DataPropDecl, [(DataCon, DataConP)]))]
-> [(TyCon, (DataPropDecl, [(DataCon, DataConP)]))]
forall a b. (a -> b) -> a -> b
$ [(TyCon, (ModName, DataPropDecl))]
-> [Located DataConP]
-> [(TyCon, (DataPropDecl, [(DataCon, DataConP)]))]
groupDataCons [(TyCon, (ModName, DataPropDecl))]
tds' [Located DataConP]
ds
    ([(TyCon, (DataPropDecl, [(DataCon, DataConP)]))]
okTcs, [(TyCon, (DataPropDecl, [(DataCon, DataConP)]))]
badTcs)  = ((TyCon, (DataPropDecl, [(DataCon, DataConP)])) -> Bool)
-> [(TyCon, (DataPropDecl, [(DataCon, DataConP)]))]
-> ([(TyCon, (DataPropDecl, [(DataCon, DataConP)]))],
    [(TyCon, (DataPropDecl, [(DataCon, DataConP)]))])
forall a. (a -> Bool) -> [a] -> ([a], [a])
L.partition (TyCon, (DataPropDecl, [(DataCon, DataConP)])) -> Bool
forall a b c. (a, (b, [(DataCon, c)])) -> Bool
isVanillaTc [(TyCon, (DataPropDecl, [(DataCon, DataConP)]))]
tcDds
    decs :: [DataDecl]
decs             = [ TCEmb TyCon
-> TyCon -> DataPropDecl -> [(DataCon, DataConP)] -> DataDecl
makeFDataDecls TCEmb TyCon
tce TyCon
tc DataPropDecl
dd [(DataCon, DataConP)]
ctors | (TyCon
tc, (DataPropDecl
dd, [(DataCon, DataConP)]
ctors)) <- [(TyCon, (DataPropDecl, [(DataCon, DataConP)]))]
okTcs]
    ([DataDecl]
okDecs,[DataDecl]
badDecs) = [DataDecl] -> ([DataDecl], [DataDecl])
checkRegularData [DataDecl]
decs

isVanillaTc :: (a, (b, [(Ghc.DataCon, c)])) -> Bool
isVanillaTc :: forall a b c. (a, (b, [(DataCon, c)])) -> Bool
isVanillaTc (a
_, (b
_, [(DataCon, c)]
ctors)) = ((DataCon, c) -> Bool) -> [(DataCon, c)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (DataCon -> Bool
Ghc.isVanillaDataCon (DataCon -> Bool)
-> ((DataCon, c) -> DataCon) -> (DataCon, c) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (DataCon, c) -> DataCon
forall a b. (a, b) -> a
fst) [(DataCon, c)]
ctors

checkRegularData :: [F.DataDecl] -> ([F.DataDecl], [F.DataDecl])
checkRegularData :: [DataDecl] -> ([DataDecl], [DataDecl])
checkRegularData [DataDecl]
ds = ([DataDecl]
oks, [DataDecl]
badDs)
  where
    badDs :: [DataDecl]
badDs           = [DataDecl] -> [DataDecl]
F.checkRegular [DataDecl]
ds
    badSyms :: HashSet Symbol
badSyms         = {- F.notracepp "BAD-Data" . -} [Symbol] -> HashSet Symbol
forall a. Hashable a => [a] -> HashSet a
S.fromList ([Symbol] -> HashSet Symbol)
-> ([DataDecl] -> [Symbol]) -> [DataDecl] -> HashSet Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (DataDecl -> Symbol) -> [DataDecl] -> [Symbol]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DataDecl -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol ([DataDecl] -> HashSet Symbol) -> [DataDecl] -> HashSet Symbol
forall a b. (a -> b) -> a -> b
$ [DataDecl]
badDs
    oks :: [DataDecl]
oks             = [ DataDecl
d |  DataDecl
d <- [DataDecl]
ds, Bool -> Bool
not (Symbol -> HashSet Symbol -> Bool
forall a. Hashable a => a -> HashSet a -> Bool
S.member (DataDecl -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol DataDecl
d) HashSet Symbol
badSyms) ]

mkWarnDecl :: Located PJ.Doc -> Warning
mkWarnDecl :: Located Doc -> Warning
mkWarnDecl Located Doc
d = SrcSpan -> Doc -> Warning
mkWarning (Located Doc -> SrcSpan
forall a. Loc a => a -> SrcSpan
GM.fSrcSpan Located Doc
d) (Doc
"Non-regular data declaration" Doc -> Doc -> Doc
<+> Located Doc -> Doc
forall a. Located a -> a
val Located Doc
d)


-- [NOTE:Orphan-TyCons]

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

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

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

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

      So, 'resolveTyConDecls' implements the following protocol:

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

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

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

-}
resolveTyCons :: ModName -> [(ModName, Ghc.TyCon, DataPropDecl)]
              -> [(Ghc.TyCon, (ModName, DataPropDecl))]
resolveTyCons :: ModName
-> [(ModName, TyCon, DataPropDecl)]
-> [(TyCon, (ModName, DataPropDecl))]
resolveTyCons ModName
mn [(ModName, TyCon, DataPropDecl)]
mtds = [(TyCon
tc, (ModName
m, DataPropDecl
d)) | (TyCon
tc, [(ModName, DataPropDecl)]
mds) <- HashMap TyCon [(ModName, DataPropDecl)]
-> [(TyCon, [(ModName, DataPropDecl)])]
forall k v. HashMap k v -> [(k, v)]
M.toList HashMap TyCon [(ModName, DataPropDecl)]
tcDecls
                                      , (ModName
m, DataPropDecl
d)    <- Maybe (ModName, DataPropDecl) -> [(ModName, DataPropDecl)]
forall a. Maybe a -> [a]
Mb.maybeToList (Maybe (ModName, DataPropDecl) -> [(ModName, DataPropDecl)])
-> Maybe (ModName, DataPropDecl) -> [(ModName, DataPropDecl)]
forall a b. (a -> b) -> a -> b
$ ModName
-> TyCon
-> [(ModName, DataPropDecl)]
-> Maybe (ModName, DataPropDecl)
resolveDecls ModName
mn TyCon
tc [(ModName, DataPropDecl)]
mds ]
  where
    tcDecls :: HashMap TyCon [(ModName, DataPropDecl)]
tcDecls          = [(TyCon, (ModName, DataPropDecl))]
-> HashMap TyCon [(ModName, DataPropDecl)]
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k [v]
Misc.group [ (TyCon
tc, (ModName
m, DataPropDecl
d)) | (ModName
m, TyCon
tc, DataPropDecl
d) <- [(ModName, TyCon, DataPropDecl)]
mtds ]

-- | See [NOTE:Orphan-TyCons], the below function tells us which of (possibly many)
--   DataDecls to use.
resolveDecls :: ModName -> Ghc.TyCon -> Misc.ListNE (ModName, DataPropDecl)
             -> Maybe (ModName, DataPropDecl)
resolveDecls :: ModName
-> TyCon
-> [(ModName, DataPropDecl)]
-> Maybe (ModName, DataPropDecl)
resolveDecls ModName
mName TyCon
tc [(ModName, DataPropDecl)]
mds  = [Char]
-> Maybe (ModName, DataPropDecl) -> Maybe (ModName, DataPropDecl)
forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
msg (Maybe (ModName, DataPropDecl) -> Maybe (ModName, DataPropDecl))
-> Maybe (ModName, DataPropDecl) -> Maybe (ModName, DataPropDecl)
forall a b. (a -> b) -> a -> b
$
    case ((ModName, DataPropDecl) -> Bool)
-> [(ModName, DataPropDecl)] -> [(ModName, DataPropDecl)]
forall a. (a -> Bool) -> [a] -> [a]
filter (ModName, DataPropDecl) -> Bool
forall {b}. (ModName, b) -> Bool
isHomeDef [(ModName, DataPropDecl)]
mds of
      (ModName, DataPropDecl)
x:[(ModName, DataPropDecl)]
_ -> (ModName, DataPropDecl) -> Maybe (ModName, DataPropDecl)
forall a. a -> Maybe a
Just (ModName, DataPropDecl)
x
      [(ModName, DataPropDecl)]
_ -> case ((ModName, DataPropDecl) -> Bool)
-> [(ModName, DataPropDecl)] -> [(ModName, DataPropDecl)]
forall a. (a -> Bool) -> [a] -> [a]
filter (ModName, DataPropDecl) -> Bool
forall {b}. (ModName, b) -> Bool
isLHAssumptionsDef [(ModName, DataPropDecl)]
mds of
        [(ModName, DataPropDecl)
x] -> (ModName, DataPropDecl) -> Maybe (ModName, DataPropDecl)
forall a. a -> Maybe a
Just (ModName, DataPropDecl)
x
        xs :: [(ModName, DataPropDecl)]
xs@((ModName, DataPropDecl)
_:[(ModName, DataPropDecl)]
_) -> [Char] -> Maybe (ModName, DataPropDecl)
forall a. HasCallStack => [Char] -> a
error ([Char] -> Maybe (ModName, DataPropDecl))
-> [Char] -> Maybe (ModName, DataPropDecl)
forall a b. (a -> b) -> a -> b
$
          [Char]
"Multiple spec declarations of " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Symbol -> [Char]
forall a. Show a => a -> [Char]
show (TyCon -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol TyCon
tc) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
          [Char]
" found in _LHAssumption modules: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [ModName] -> [Char]
forall a. Show a => a -> [Char]
show (((ModName, DataPropDecl) -> ModName)
-> [(ModName, DataPropDecl)] -> [ModName]
forall a b. (a -> b) -> [a] -> [b]
map (ModName, DataPropDecl) -> ModName
forall a b. (a, b) -> a
fst [(ModName, DataPropDecl)]
xs) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++
          [Char]
". Please, remove some of them."
        [] -> ((ModName, DataPropDecl) -> Bool)
-> [(ModName, DataPropDecl)] -> Maybe (ModName, DataPropDecl)
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
L.find (ModName, DataPropDecl) -> Bool
forall {b}. (ModName, b) -> Bool
isMyDef [(ModName, DataPropDecl)]
mds
  where
    msg :: [Char]
msg                    = [Char]
"resolveDecls" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ (ModName, TyCon) -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp (ModName
mName, TyCon
tc)
    isMyDef :: (ModName, b) -> Bool
isMyDef                = (ModName
mName ModName -> ModName -> Bool
forall a. Eq a => a -> a -> Bool
==)             (ModName -> Bool)
-> ((ModName, b) -> ModName) -> (ModName, b) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ModName, b) -> ModName
forall a b. (a, b) -> a
fst
    isHomeDef :: (ModName, b) -> Bool
isHomeDef              = (Symbol
tcHome Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
==) (Symbol -> Bool)
-> ((ModName, b) -> Symbol) -> (ModName, b) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModName -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol (ModName -> Symbol)
-> ((ModName, b) -> ModName) -> (ModName, b) -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ModName, b) -> ModName
forall a b. (a, b) -> a
fst
    tcHome :: Symbol
tcHome                 = Symbol -> Symbol
GM.takeModuleNames (TyCon -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol TyCon
tc)
    isLHAssumptionsDef :: (ModName, b) -> Bool
isLHAssumptionsDef     = [Char] -> [Char] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
L.isSuffixOf [Char]
"_LHAssumptions" ([Char] -> Bool)
-> ((ModName, b) -> [Char]) -> (ModName, b) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleName -> [Char]
Ghc.moduleNameString (ModuleName -> [Char])
-> ((ModName, b) -> ModuleName) -> (ModName, b) -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModName -> ModuleName
getModName (ModName -> ModuleName)
-> ((ModName, b) -> ModName) -> (ModName, b) -> ModuleName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ModName, b) -> ModName
forall a b. (a, b) -> a
fst

groupDataCons :: [(Ghc.TyCon, (ModName, DataPropDecl))]
              -> [Located DataConP]
              -> [(Ghc.TyCon, (DataPropDecl, [(Ghc.DataCon, DataConP)]))]
groupDataCons :: [(TyCon, (ModName, DataPropDecl))]
-> [Located DataConP]
-> [(TyCon, (DataPropDecl, [(DataCon, DataConP)]))]
groupDataCons [(TyCon, (ModName, DataPropDecl))]
tds [Located DataConP]
ds = [ (TyCon
tc, (DataPropDecl
d, [(DataCon, DataConP)]
dds')) | (TyCon
tc, ((ModName
m, DataPropDecl
d), [(DataCon, DataConP)]
dds)) <- [(TyCon, ((ModName, DataPropDecl), [(DataCon, DataConP)]))]
tcDataCons
                                         , let dds' :: [(DataCon, DataConP)]
dds' = ((DataCon, DataConP) -> Bool)
-> [(DataCon, DataConP)] -> [(DataCon, DataConP)]
forall a. (a -> Bool) -> [a] -> [a]
filter (ModName -> DataConP -> Bool
isResolvedDataConP ModName
m (DataConP -> Bool)
-> ((DataCon, DataConP) -> DataConP) -> (DataCon, DataConP) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (DataCon, DataConP) -> DataConP
forall a b. (a, b) -> b
snd) [(DataCon, DataConP)]
dds
                       ]
  where
    tcDataCons :: [(TyCon, ((ModName, DataPropDecl), [(DataCon, DataConP)]))]
tcDataCons       = HashMap TyCon ((ModName, DataPropDecl), [(DataCon, DataConP)])
-> [(TyCon, ((ModName, DataPropDecl), [(DataCon, DataConP)]))]
forall k v. HashMap k v -> [(k, v)]
M.toList (HashMap TyCon ((ModName, DataPropDecl), [(DataCon, DataConP)])
 -> [(TyCon, ((ModName, DataPropDecl), [(DataCon, DataConP)]))])
-> HashMap TyCon ((ModName, DataPropDecl), [(DataCon, DataConP)])
-> [(TyCon, ((ModName, DataPropDecl), [(DataCon, DataConP)]))]
forall a b. (a -> b) -> a -> b
$ ((ModName, DataPropDecl)
 -> [(DataCon, DataConP)]
 -> ((ModName, DataPropDecl), [(DataCon, DataConP)]))
-> HashMap TyCon (ModName, DataPropDecl)
-> HashMap TyCon [(DataCon, DataConP)]
-> HashMap TyCon ((ModName, DataPropDecl), [(DataCon, DataConP)])
forall k v1 v2 v3.
Eq k =>
(v1 -> v2 -> v3) -> HashMap k v1 -> HashMap k v2 -> HashMap k v3
M.intersectionWith (,) HashMap TyCon (ModName, DataPropDecl)
declM HashMap TyCon [(DataCon, DataConP)]
ctorM
    declM :: HashMap TyCon (ModName, DataPropDecl)
declM            = [(TyCon, (ModName, DataPropDecl))]
-> HashMap TyCon (ModName, DataPropDecl)
forall k v. 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
-> DataDeclP Symbol BareType
-> [(DataCon, DataConP)]
-> DataDecl
makeDataDecl TCEmb TyCon
tce TyCon
tc (DataPropDecl -> DataDeclP Symbol BareType
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
-> DataDeclP Symbol BareType
-> [(DataCon, DataConP)]
-> DataDecl
makeDataDecl TCEmb TyCon
tce TyCon
tc DataDeclP Symbol BareType
dd [(DataCon, DataConP)]
ctors
  = F.DDecl
      { ddTyCon :: FTycon
F.ddTyCon = FTycon
ftc
      , ddVars :: Int
F.ddVars  = [Var] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length                ([Var] -> Int) -> [Var] -> Int
forall a b. (a -> b) -> a -> b
$  TyCon -> [Var]
GM.tyConTyVarsDef TyCon
tc
      , ddCtors :: [DataCtor]
F.ddCtors = TCEmb TyCon -> FTycon -> (DataCon, DataConP) -> DataCtor
makeDataCtor TCEmb TyCon
tce FTycon
ftc ((DataCon, DataConP) -> DataCtor)
-> [(DataCon, DataConP)] -> [DataCtor]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(DataCon, DataConP)]
ctors
      }
  where
    ftc :: FTycon
ftc = LocSymbol -> FTycon
F.symbolFTycon (TyCon -> DataDeclP Symbol BareType -> LocSymbol
tyConLocSymbol TyCon
tc DataDeclP Symbol BareType
dd)

tyConLocSymbol :: Ghc.TyCon -> DataDecl -> LocSymbol
tyConLocSymbol :: TyCon -> DataDeclP Symbol BareType -> LocSymbol
tyConLocSymbol TyCon
tc DataDeclP Symbol BareType
dd = DataName -> Symbol -> LocSymbol
forall l b. Loc l => l -> b -> Located b
F.atLoc (DataDeclP Symbol BareType -> DataName
forall v ty. DataDeclP v ty -> DataName
tycName DataDeclP Symbol BareType
dd) (TyCon -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol TyCon
tc)

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

makeDataCtor :: F.TCEmb Ghc.TyCon -> F.FTycon -> (Ghc.DataCon, DataConP) -> F.DataCtor
makeDataCtor :: TCEmb TyCon -> FTycon -> (DataCon, DataConP) -> DataCtor
makeDataCtor TCEmb TyCon
tce FTycon
c (DataCon
d, DataConP
dp) = F.DCtor
  { dcName :: 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 -> LocSymbol) -> Symbol -> LocSymbol
forall a b. (a -> b) -> a -> b
$ LHName -> Symbol
lhNameToResolvedSymbol LHName
x, SpecType
t) | (LHName
x, SpecType
t) <- [(LHName, SpecType)] -> [(LHName, SpecType)]
forall a. [a] -> [a]
reverse (DataConP -> [(LHName, 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 a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [RTyVar]
as) (Sort -> Sort) -> (SpecType -> Sort) -> SpecType -> Sort
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCEmb TyCon -> SpecType -> Sort
forall r.
(PPrint r, IsReft r, ReftBind r ~ Symbol, ReftVar r ~ Symbol,
 SubsTy RTyVar (RType RTyCon RTyVar NoReft) r) =>
TCEmb TyCon -> RRType r -> Sort
RT.rTypeSort TCEmb TyCon
tce

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

--------------------------------------------------------------------------------
meetDataConSpec :: Bool -> F.TCEmb Ghc.TyCon -> [(Ghc.Var, SpecType)] -> [DataConP]
                -> [(Ghc.Var, SpecType)]
--------------------------------------------------------------------------------
meetDataConSpec :: Bool
-> TCEmb TyCon
-> [(Var, SpecType)]
-> [DataConP]
-> [(Var, SpecType)]
meetDataConSpec Bool
allowTC TCEmb TyCon
emb [(Var, SpecType)]
xts [DataConP]
dcs  = HashMap Var SpecType -> [(Var, SpecType)]
forall k v. HashMap k v -> [(k, v)]
M.toList (HashMap Var SpecType -> [(Var, SpecType)])
-> HashMap Var SpecType -> [(Var, SpecType)]
forall a b. (a -> b) -> a -> b
$ (SrcSpan, SpecType) -> SpecType
forall a b. (a, b) -> b
snd ((SrcSpan, SpecType) -> SpecType)
-> HashMap Var (SrcSpan, SpecType) -> HashMap Var SpecType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (HashMap Var (SrcSpan, SpecType)
 -> (Var, SpecType) -> HashMap Var (SrcSpan, SpecType))
-> HashMap Var (SrcSpan, SpecType)
-> [(Var, SpecType)]
-> HashMap Var (SrcSpan, SpecType)
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' HashMap Var (SrcSpan, SpecType)
-> (Var, SpecType) -> HashMap Var (SrcSpan, SpecType)
forall {a}.
(PPrint a, NamedThing a, Hashable a) =>
HashMap a (SrcSpan, SpecType)
-> (a, SpecType) -> HashMap a (SrcSpan, SpecType)
upd HashMap Var (SrcSpan, SpecType)
dcm0 [(Var, SpecType)]
xts
  where
    dcm0 :: HashMap Var (SrcSpan, SpecType)
dcm0                     = ((SrcSpan, SpecType) -> (SrcSpan, SpecType) -> (SrcSpan, SpecType))
-> [(Var, (SrcSpan, SpecType))] -> HashMap Var (SrcSpan, SpecType)
forall k v. Hashable k => (v -> v -> v) -> [(k, v)] -> HashMap k v
M.fromListWith (SrcSpan, SpecType) -> (SrcSpan, SpecType) -> (SrcSpan, SpecType)
forall {b} {a} {a}. Meet b => (a, b) -> (a, b) -> (a, b)
meetM (Bool -> [DataConP] -> [(Var, (SrcSpan, SpecType))]
dataConSpec' Bool
allowTC [DataConP]
dcs)
    upd :: HashMap a (SrcSpan, SpecType)
-> (a, SpecType) -> HashMap a (SrcSpan, SpecType)
upd HashMap a (SrcSpan, SpecType)
dcm (a
x, SpecType
t)           = a
-> (SrcSpan, SpecType)
-> HashMap a (SrcSpan, SpecType)
-> HashMap a (SrcSpan, SpecType)
forall k v. 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. Hashable k => k -> HashMap k v -> Maybe v
M.lookup a
x HashMap a (SrcSpan, SpecType)
dcm)
    meetM :: (a, b) -> (a, b) -> (a, b)
meetM (a
l,b
t) (a
_,b
t')       = (a
l, b
t b -> b -> b
forall r. Meet r => r -> r -> r
`meet` b
t')
    meetX :: a -> SpecType -> (SrcSpan, SpecType) -> SpecType
meetX a
x SpecType
t (SrcSpan
sp', SpecType
t')      = [Char] -> SpecType -> SpecType
forall a. PPrint a => [Char] -> a -> a
F.notracepp (a -> SpecType -> SpecType -> [Char]
forall {a} {b} {c}.
(PPrint a, PPrint b, PPrint c) =>
a -> b -> c -> [Char]
_msg a
x SpecType
t SpecType
t') (SpecType -> SpecType) -> SpecType -> SpecType
forall a b. (a -> b) -> a -> b
$ TCEmb TyCon
-> Doc -> (SrcSpan, SpecType) -> (SrcSpan, SpecType) -> SpecType
meetVarTypes TCEmb TyCon
emb (a -> Doc
forall a. PPrint a => a -> Doc
pprint a
x) (a -> SrcSpan
forall a. NamedThing a => a -> SrcSpan
Ghc.getSrcSpan a
x, SpecType
t) (SrcSpan
sp', SpecType
t')
    _msg :: a -> b -> c -> [Char]
_msg a
x b
t c
t'              = [Char]
"MEET-VAR-TYPES: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ (a, b, c) -> [Char]
forall a. PPrint a => a -> [Char]
showpp (a
x, b
t, c
t')

dataConSpec' :: Bool -> [DataConP] -> [(Ghc.Var, (Ghc.SrcSpan, SpecType))]
dataConSpec' :: Bool -> [DataConP] -> [(Var, (SrcSpan, SpecType))]
dataConSpec' Bool
allowTC = (DataConP -> [(Var, (SrcSpan, SpecType))])
-> [DataConP] -> [(Var, (SrcSpan, SpecType))]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap DataConP -> [(Var, (SrcSpan, SpecType))]
tx
  where
    tx :: DataConP -> [(Var, (SrcSpan, SpecType))]
tx DataConP
dcp   =  [ (Var
x, (SrcSpan, SpecType)
res) | (Var
x, SpecType
t0) <- Bool -> DataConP -> [(Var, SpecType)]
dataConPSpecType Bool
allowTC DataConP
dcp
                          , let t :: SpecType
t    = Var -> SpecType -> SpecType
forall r.
(PPrint r, IsReft r, SubsTy RTyVar (RType RTyCon RTyVar NoReft) r,
 ReftBind r ~ Symbol, ReftVar r ~ Symbol, Variable r ~ Symbol) =>
Var -> RType RTyCon RTyVar r -> RType RTyCon RTyVar r
RT.expandProductType Var
x SpecType
t0
                          , let res :: (SrcSpan, SpecType)
res  = (DataConP -> SrcSpan
forall a. Loc a => a -> SrcSpan
GM.fSrcSpan DataConP
dcp, SpecType
t)
                ]
--------------------------------------------------------------------------------
-- | Bare Predicate: DataCon Definitions ---------------------------------------
--------------------------------------------------------------------------------
makeConTypes :: ModName -> Bare.Env -> [(ModName, Ms.BareSpec)]
             -> Bare.Lookup ([(ModName, TyConP, Maybe DataPropDecl)], [[Located DataConP]])
makeConTypes :: ModName
-> Env
-> [(ModName, BareSpec)]
-> Lookup
     ([(ModName, TyConP, Maybe DataPropDecl)], [[Located DataConP]])
makeConTypes ModName
myName Env
env [(ModName, BareSpec)]
specs =
  [([(ModName, TyConP, Maybe DataPropDecl)], [[Located DataConP]])]
-> ([(ModName, TyConP, Maybe DataPropDecl)], [[Located DataConP]])
forall a b. [([a], [b])] -> ([a], [b])
Misc.concatUnzip ([([(ModName, TyConP, Maybe DataPropDecl)], [[Located DataConP]])]
 -> ([(ModName, TyConP, Maybe DataPropDecl)], [[Located DataConP]]))
-> Either
     [Error]
     [([(ModName, TyConP, Maybe DataPropDecl)], [[Located DataConP]])]
-> Lookup
     ([(ModName, TyConP, Maybe DataPropDecl)], [[Located DataConP]])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((ModName, BareSpec)
 -> Lookup
      ([(ModName, TyConP, Maybe DataPropDecl)], [[Located DataConP]]))
-> [(ModName, BareSpec)]
-> Either
     [Error]
     [([(ModName, TyConP, Maybe DataPropDecl)], [[Located DataConP]])]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (ModName
-> Env
-> (ModName, BareSpec)
-> Lookup
     ([(ModName, TyConP, Maybe DataPropDecl)], [[Located DataConP]])
makeConTypes' ModName
myName Env
env) [(ModName, BareSpec)]
specs


-- Essentially transforms the data declarations inside the specs
--- into LH's enhanced types for type constructors and data constructors
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) = Env
-> ModName
-> BareSpec
-> [DataDeclP Symbol BareType]
-> [(Located LHName, [Variance])]
-> Lookup
     ([(ModName, TyConP, Maybe DataPropDecl)], [[Located DataConP]])
makeConTypes'' Env
env ModName
name BareSpec
spec [DataDeclP Symbol BareType]
dcs [(Located LHName, [Variance])]
vdcs
  where
    dcs :: [DataDeclP Symbol BareType]
dcs  = BareSpec -> [DataDeclP Symbol BareType]
forall lname ty. Spec lname ty -> [DataDeclP lname ty]
Ms.dataDecls BareSpec
spec
    vdcs :: [(Located LHName, [Variance])]
vdcs = BareSpec -> [(Located LHName, [Variance])]
forall lname ty. Spec lname ty -> [(Located LHName, [Variance])]
Ms.dvariance BareSpec
spec

-- Essentially transforms the data declarations into LH's enhanced types for type constructors and
-- data constructors
makeConTypes'' :: Bare.Env -> ModName -> Ms.BareSpec -> [DataDecl] -> [(F.Located LHName, [Variance])]
             -> Bare.Lookup ([(ModName, TyConP, Maybe DataPropDecl)], [[Located DataConP]])
makeConTypes'' :: Env
-> ModName
-> BareSpec
-> [DataDeclP Symbol BareType]
-> [(Located LHName, [Variance])]
-> Lookup
     ([(ModName, TyConP, Maybe DataPropDecl)], [[Located DataConP]])
makeConTypes'' Env
env ModName
name BareSpec
spec [DataDeclP Symbol BareType]
dcs [(Located LHName, [Variance])]
vdcs = do
  dcs'   <- Env
-> ModName
-> [DataDeclP Symbol BareType]
-> Lookup [DataDeclP Symbol BareType]
canonizeDecls Env
env ModName
name [DataDeclP Symbol BareType]
dcs
  let dcs'' = BareSpec
-> [DataDeclP Symbol BareType] -> [DataDeclP Symbol BareType]
dataDeclSize BareSpec
spec [DataDeclP Symbol BareType]
dcs'
  let gvs = [DataDeclP Symbol BareType]
-> [(Located LHName, [Variance])]
-> [(Maybe (DataDeclP Symbol BareType),
     Maybe (Located LHName, [Variance]))]
groupVariances [DataDeclP Symbol BareType]
dcs'' [(Located LHName, [Variance])]
vdcs
  zong <- catLookups . map (uncurry (ofBDataDecl env name)) $ gvs
  return (unzip zong)


type DSizeMap = M.HashMap LHName (F.Symbol, [LHName])
normalizeDSize :: [([LocBareType], F.Symbol)] -> DSizeMap
normalizeDSize :: [([LocBareType], Symbol)] -> DSizeMap
normalizeDSize [([LocBareType], Symbol)]
ds = [(LHName, (Symbol, [LHName]))] -> DSizeMap
forall k v. Hashable k => [(k, v)] -> HashMap k v
M.fromList ((([LocBareType], Symbol) -> [(LHName, (Symbol, [LHName]))])
-> [([LocBareType], Symbol)] -> [(LHName, (Symbol, [LHName]))]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ([LocBareType], Symbol) -> [(LHName, (Symbol, [LHName]))]
forall {b} {v} {tv} {r} {a}.
([Located (RTypeBV b v BTyCon tv r)], a)
-> [(LHName, (a, [LHName]))]
go [([LocBareType], Symbol)]
ds)
  where go :: ([Located (RTypeBV b v BTyCon tv r)], a)
-> [(LHName, (a, [LHName]))]
go ([Located (RTypeBV b v BTyCon tv r)]
ts,a
x) = let xs :: [LHName]
xs = (Located (RTypeBV b v BTyCon tv r) -> Maybe LHName)
-> [Located (RTypeBV b v BTyCon tv r)] -> [LHName]
forall a b. (a -> Maybe b) -> [a] -> [b]
Mb.mapMaybe (RTypeBV b v BTyCon tv r -> Maybe LHName
forall {b} {v} {tv} {r}. RTypeBV b v BTyCon tv r -> Maybe LHName
getTc (RTypeBV b v BTyCon tv r -> Maybe LHName)
-> (Located (RTypeBV b v BTyCon tv r) -> RTypeBV b v BTyCon tv r)
-> Located (RTypeBV b v BTyCon tv r)
-> Maybe LHName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Located (RTypeBV b v BTyCon tv r) -> RTypeBV b v BTyCon tv r
forall a. Located a -> a
val) [Located (RTypeBV b v BTyCon tv r)]
ts
                    in [(LHName
tc, (a
x, [LHName]
xs)) | LHName
tc <- [LHName]
xs]
        getTc :: RTypeBV b v BTyCon tv r -> Maybe LHName
getTc (RAllT RTVUBV b v BTyCon tv
_ RTypeBV b v BTyCon tv r
t r
_)  = RTypeBV b v BTyCon tv r -> Maybe LHName
getTc RTypeBV b v BTyCon tv r
t
        getTc (RApp BTyCon
c [RTypeBV b v BTyCon tv r]
_ [RTPropBV b v BTyCon tv r]
_ r
_) = LHName -> Maybe LHName
forall a. a -> Maybe a
Just (Located LHName -> LHName
forall a. Located a -> a
val (Located LHName -> LHName) -> Located LHName -> LHName
forall a b. (a -> b) -> a -> b
$ BTyCon -> Located LHName
btc_tc BTyCon
c)
        getTc RTypeBV b v BTyCon tv r
_ = Maybe LHName
forall a. Maybe a
Nothing

dataDeclSize :: Ms.BareSpec -> [DataDecl] -> [DataDecl]
dataDeclSize :: BareSpec
-> [DataDeclP Symbol BareType] -> [DataDeclP Symbol BareType]
dataDeclSize BareSpec
spec [DataDeclP Symbol BareType]
dcs = DSizeMap -> DataDeclP Symbol BareType -> DataDeclP Symbol BareType
makeSize DSizeMap
smap (DataDeclP Symbol BareType -> DataDeclP Symbol BareType)
-> [DataDeclP Symbol BareType] -> [DataDeclP Symbol BareType]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [DataDeclP Symbol BareType]
dcs
  where smap :: DSizeMap
smap = [([LocBareType], Symbol)] -> DSizeMap
normalizeDSize ([([LocBareType], Symbol)] -> DSizeMap)
-> [([LocBareType], Symbol)] -> DSizeMap
forall a b. (a -> b) -> a -> b
$ BareSpec -> [([LocBareType], Symbol)]
forall lname ty. Spec lname ty -> [([Located ty], lname)]
Ms.dsize BareSpec
spec


makeSize :: DSizeMap -> DataDecl -> DataDecl
makeSize :: DSizeMap -> DataDeclP Symbol BareType -> DataDeclP Symbol BareType
makeSize DSizeMap
smap DataDeclP Symbol BareType
d
  | Just (Symbol, [LHName])
p <- LHName -> DSizeMap -> Maybe (Symbol, [LHName])
forall k v. Hashable k => k -> HashMap k v -> Maybe v
M.lookup (Located LHName -> LHName
forall a. Located a -> a
val (Located LHName -> LHName) -> Located LHName -> LHName
forall a b. (a -> b) -> a -> b
$ DataName -> Located LHName
dataNameSymbol (DataName -> Located LHName) -> DataName -> Located LHName
forall a b. (a -> b) -> a -> b
$ DataDeclP Symbol BareType -> DataName
forall v ty. DataDeclP v ty -> DataName
tycName DataDeclP Symbol BareType
d) DSizeMap
smap
  = DataDeclP Symbol BareType
d {tycDCons = fmap (fmap (makeSizeCtor p)) (tycDCons d) }
  | Bool
otherwise
   = DataDeclP Symbol BareType
d

makeSizeCtor :: (F.Symbol, [LHName]) -> DataCtor -> DataCtor
makeSizeCtor :: (Symbol, [LHName]) -> DataCtorP BareType -> DataCtorP BareType
makeSizeCtor (Symbol
s,[LHName]
xs) DataCtorP BareType
d = DataCtorP BareType
d {dcFields = fmap (mapBot go) <$> dcFields d}
  where
    go :: RTypeBV
  b v BTyCon tv (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> RTypeBV
     b v BTyCon tv (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
go (RApp BTyCon
c [RTypeBV
   b v BTyCon tv (UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
ts [RTPropBV
   b v BTyCon tv (UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
rs UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r) | Located LHName -> LHName
forall a. Located a -> a
val (BTyCon -> Located LHName
btc_tc BTyCon
c) LHName -> [LHName] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [LHName]
xs
                        = BTyCon
-> [RTypeBV
      b v BTyCon tv (UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
-> [RTPropBV
      b v BTyCon tv (UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
-> RTypeBV
     b v BTyCon tv (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
forall b v c tv r.
c
-> [RTypeBV b v c tv r]
-> [RTPropBV b v c tv r]
-> r
-> RTypeBV b v c tv r
RApp BTyCon
c [RTypeBV
   b v BTyCon tv (UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
ts [RTPropBV
   b v BTyCon tv (UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
rs (UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r UReftBV Symbol Symbol (ReftBV Symbol Symbol)
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
forall r. Meet r => r -> r -> r
`meet` UReftBV Symbol Symbol (ReftBV Symbol Symbol)
rsz)
    go RTypeBV
  b v BTyCon tv (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
t                = RTypeBV
  b v BTyCon tv (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
t
    rsz :: UReftBV Symbol Symbol (ReftBV Symbol Symbol)
rsz  = ReftBV Symbol Symbol
-> PredicateBV Symbol Symbol
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
forall b v r. r -> PredicateBV b v -> UReftBV b v r
MkUReft ((Symbol, Expr) -> ReftBV Symbol Symbol
forall b v. (b, ExprBV b v) -> ReftBV b v
F.Reft (Symbol
F.vv_, Brel -> Expr -> Expr -> Expr
forall b v. Brel -> ExprBV b v -> ExprBV b v -> ExprBV b v
F.PAtom Brel
F.Lt
                                      (Expr -> Expr -> Expr
forall b v. ExprBV b v -> ExprBV b v -> ExprBV b v
F.EApp (Symbol -> Expr
forall b v. v -> ExprBV b v
F.EVar Symbol
s) (Symbol -> Expr
forall b v. v -> ExprBV b v
F.EVar Symbol
F.vv_))
                                      (Expr -> Expr -> Expr
forall b v. ExprBV b v -> ExprBV b v -> ExprBV b v
F.EApp (Symbol -> Expr
forall b v. v -> ExprBV b v
F.EVar Symbol
s) (Symbol -> Expr
forall b v. v -> ExprBV b v
F.EVar Symbol
selfSymbol))
                                      ))
                   PredicateBV Symbol Symbol
forall a. Monoid a => a
mempty


catLookups :: [Bare.Lookup a] -> Bare.Lookup [a]
catLookups :: forall a. [Lookup a] -> Lookup [a]
catLookups = [Either [Error] a] -> Either [Error] [a]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence ([Either [Error] a] -> Either [Error] [a])
-> ([Either [Error] a] -> [Either [Error] a])
-> [Either [Error] a]
-> Either [Error] [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Either [Error] a -> Maybe (Either [Error] a))
-> [Either [Error] a] -> [Either [Error] a]
forall a b. (a -> Maybe b) -> [a] -> [b]
Mb.mapMaybe Either [Error] a -> Maybe (Either [Error] a)
forall a. Lookup a -> Maybe (Lookup a)
skipResolve

skipResolve  :: Bare.Lookup a -> Maybe (Bare.Lookup a)
skipResolve :: forall a. Lookup a -> Maybe (Lookup a)
skipResolve (Left [Error]
es) = [Error] -> Maybe (Either [Error] a)
forall e a. [e] -> Maybe (Either [e] a)
left' ((Error -> Bool) -> [Error] -> [Error]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Error -> Bool) -> Error -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Error -> Bool
forall t. TError t -> Bool
isErrResolve) [Error]
es)
skipResolve (Right a
v) = Either [Error] a -> Maybe (Either [Error] a)
forall a. a -> Maybe a
Just (a -> Either [Error] a
forall a b. b -> Either a b
Right a
v)

isErrResolve :: TError t -> Bool
isErrResolve :: forall t. TError t -> Bool
isErrResolve ErrResolve {} = Bool
True
isErrResolve TError t
_             =  Bool
False

left' :: [e] -> Maybe (Either [e] a)
left' :: forall e a. [e] -> Maybe (Either [e] a)
left' [] = Maybe (Either [e] a)
forall a. Maybe a
Nothing
left' [e]
es = Either [e] a -> Maybe (Either [e] a)
forall a. a -> Maybe a
Just ([e] -> Either [e] a
forall a b. a -> Either a b
Left [e]
es)


-- | 'canonizeDecls ds' returns a subset of 'ds' with duplicates, e.g. arising
--   due to automatic lifting (via 'makeHaskellDataDecls'). We require that the
--   lifted versions appear LATER in the input list, and always use those
--   instead of the unlifted versions.

canonizeDecls :: Bare.Env -> ModName -> [DataDecl] -> Bare.Lookup [DataDecl]
canonizeDecls :: Env
-> ModName
-> [DataDeclP Symbol BareType]
-> Lookup [DataDeclP Symbol BareType]
canonizeDecls Env
env ModName
name [DataDeclP Symbol BareType]
dataDecls = do
  kds <- [DataDeclP Symbol BareType]
-> (DataDeclP Symbol BareType
    -> Either [Error] (Maybe (Symbol, DataDeclP Symbol BareType)))
-> Either [Error] [Maybe (Symbol, DataDeclP Symbol BareType)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [DataDeclP Symbol BareType]
dataDecls ((DataDeclP Symbol BareType
  -> Either [Error] (Maybe (Symbol, DataDeclP Symbol BareType)))
 -> Either [Error] [Maybe (Symbol, DataDeclP Symbol BareType)])
-> (DataDeclP Symbol BareType
    -> Either [Error] (Maybe (Symbol, DataDeclP Symbol BareType)))
-> Either [Error] [Maybe (Symbol, DataDeclP Symbol BareType)]
forall a b. (a -> b) -> a -> b
$ \DataDeclP Symbol BareType
d -> do
           k <- Env
-> ModName -> DataDeclP Symbol BareType -> Lookup (Maybe Symbol)
dataDeclKey Env
env ModName
name DataDeclP Symbol BareType
d
           return (fmap (, d) k)
  case Misc.uniqueByKey' selectDD (Mb.catMaybes kds) of
    Left  [DataDeclP Symbol BareType]
decls  -> [Error] -> Lookup [DataDeclP Symbol BareType]
forall a b. a -> Either a b
Left [[DataDeclP Symbol BareType] -> Error
forall {v} {ty} {t}. [DataDeclP v ty] -> TError t
err [DataDeclP Symbol BareType]
decls]
    Right [DataDeclP Symbol BareType]
decls  -> [DataDeclP Symbol BareType] -> Lookup [DataDeclP Symbol BareType]
forall a. a -> Either [Error] a
forall (m :: * -> *) a. Monad m => a -> m a
return [DataDeclP Symbol BareType]
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 :: [DataDeclP v ty] -> TError t
err ds :: [DataDeclP v ty]
ds@(DataDeclP v ty
d:[DataDeclP v ty]
_) = {- uError $ -} Doc -> ListNE SrcSpan -> TError t
forall t. Doc -> ListNE SrcSpan -> TError t
errDupSpecs (DataName -> Doc
forall a. PPrint a => a -> Doc
pprint (DataDeclP v ty -> DataName
forall v ty. DataDeclP v ty -> DataName
tycName DataDeclP v ty
d)) (DataDeclP v ty -> SrcSpan
forall a. Loc a => a -> SrcSpan
GM.fSrcSpan (DataDeclP v ty -> SrcSpan) -> [DataDeclP v ty] -> ListNE SrcSpan
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [DataDeclP v ty]
ds)
    err [DataDeclP v ty]
_        = Maybe SrcSpan -> [Char] -> TError t
forall a. Maybe SrcSpan -> [Char] -> a
impossible Maybe SrcSpan
forall a. Maybe a
Nothing [Char]
"canonizeDecls"

dataDeclKey :: Bare.Env -> ModName -> DataDecl -> Bare.Lookup (Maybe F.Symbol)
dataDeclKey :: Env
-> ModName -> DataDeclP Symbol BareType -> Lookup (Maybe Symbol)
dataDeclKey Env
env ModName
name DataDeclP Symbol BareType
d = do
  tcMb  <- Env -> ModName -> DataName -> Lookup (Maybe TyCon)
Bare.lookupGhcDnTyCon Env
env ModName
name (DataDeclP Symbol BareType -> DataName
forall v ty. DataDeclP v ty -> DataName
tycName DataDeclP Symbol BareType
d)
  case tcMb of
    Maybe TyCon
Nothing ->
      Maybe Symbol -> Lookup (Maybe Symbol)
forall a. a -> Either [Error] a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Symbol
forall a. Maybe a
Nothing
    Just TyCon
tc -> do
      _ <- Env
-> ModName
-> TyCon
-> DataDeclP Symbol BareType
-> Maybe [DataCtorP BareType]
-> Lookup [DataCtorP BareType]
checkDataCtors Env
env ModName
name TyCon
tc DataDeclP Symbol BareType
d (DataDeclP Symbol BareType -> Maybe [DataCtorP BareType]
forall v ty. DataDeclP v ty -> Maybe [DataCtorP ty]
tycDCons DataDeclP Symbol BareType
d)
      return $ Just (F.symbol 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, and that any
-- field name reused across constructors would induce the same selector sort.
-- This rejects ambiguous data annotations such as using the same selector name
-- for different field types in different constructors.
--
checkDataCtors :: Bare.Env -> ModName -> Ghc.TyCon -> DataDecl -> Maybe [DataCtor] -> Bare.Lookup [DataCtor]
checkDataCtors :: Env
-> ModName
-> TyCon
-> DataDeclP Symbol BareType
-> Maybe [DataCtorP BareType]
-> Lookup [DataCtorP BareType]
checkDataCtors Env
_env ModName
_name TyCon
_c DataDeclP Symbol BareType
_dd Maybe [DataCtorP BareType]
Nothing     = [DataCtorP BareType] -> Lookup [DataCtorP BareType]
forall a. a -> Either [Error] a
forall (m :: * -> *) a. Monad m => a -> m a
return []
checkDataCtors  Env
env  ModName
name  TyCon
c  DataDeclP Symbol BareType
dd (Just [DataCtorP BareType]
cons) = do
  -- The GHC data constructors (these are qualified)
  let dcs :: S.HashSet F.Symbol
      dcs :: HashSet Symbol
dcs = [Symbol] -> HashSet Symbol
forall a. Hashable a => [a] -> HashSet a
S.fromList ([Symbol] -> HashSet Symbol)
-> (TyCon -> [Symbol]) -> TyCon -> HashSet Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (DataCon -> Symbol) -> [DataCon] -> [Symbol]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DataCon -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol ([DataCon] -> [Symbol])
-> (TyCon -> [DataCon]) -> TyCon -> [Symbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyCon -> [DataCon]
Ghc.tyConDataCons (TyCon -> HashSet Symbol) -> TyCon -> HashSet Symbol
forall a b. (a -> b) -> a -> b
$ TyCon
c

  -- The data constructors in the spec (which we have to qualify for them to match the GHC data constructors)
  mbDcs <- (DataCtorP BareType -> Either [Error] (Maybe DataCon))
-> [DataCtorP BareType] -> Either [Error] [Maybe DataCon]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Env
-> ModName
-> Either [Error] DataCon
-> Either [Error] (Maybe DataCon)
forall e r. Env -> ModName -> Either e r -> Either e (Maybe r)
Bare.failMaybe Env
env ModName
name (Either [Error] DataCon -> Either [Error] (Maybe DataCon))
-> (DataCtorP BareType -> Either [Error] DataCon)
-> DataCtorP BareType
-> Either [Error] (Maybe DataCon)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HasCallStack => Env -> Located LHName -> Either [Error] DataCon
Env -> Located LHName -> Either [Error] DataCon
Bare.lookupGhcDataConLHName Env
env (Located LHName -> Either [Error] DataCon)
-> (DataCtorP BareType -> Located LHName)
-> DataCtorP BareType
-> Either [Error] DataCon
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataCtorP BareType -> Located LHName
forall ty. DataCtorP ty -> Located LHName
dcName) [DataCtorP BareType]
cons
  let rdcs = [Symbol] -> HashSet Symbol
forall a. Hashable a => [a] -> HashSet a
S.fromList ([Symbol] -> HashSet Symbol)
-> ([Maybe DataCon] -> [Symbol])
-> [Maybe DataCon]
-> HashSet Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (DataCon -> Symbol) -> [DataCon] -> [Symbol]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DataCon -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol ([DataCon] -> [Symbol])
-> ([Maybe DataCon] -> [DataCon]) -> [Maybe DataCon] -> [Symbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Maybe DataCon] -> [DataCon]
forall a. [Maybe a] -> [a]
Mb.catMaybes ([Maybe DataCon] -> HashSet Symbol)
-> [Maybe DataCon] -> HashSet Symbol
forall a b. (a -> b) -> a -> b
$ [Maybe DataCon]
mbDcs
  if dcs == rdcs
    then do
      cons' <- mapM checkDataCtorDupField cons
      checkDataCtorFieldTypes cons'
    else Left [errDataConMismatch (getLHNameSymbol <$> dataNameSymbol (tycName dd)) dcs rdcs]

-- | Checks whether the given data constructor has duplicate fields.
--
checkDataCtorDupField :: DataCtor -> Bare.Lookup DataCtor
checkDataCtorDupField :: DataCtorP BareType -> Either [Error] (DataCtorP BareType)
checkDataCtorDupField DataCtorP BareType
d
  | LHName
x : [LHName]
_ <- [LHName]
dups = [Error] -> Either [Error] (DataCtorP BareType)
forall a b. a -> Either a b
Left [Located LHName -> LHName -> Error
forall {a} {a} {t}.
(PPrint a, PPrint a) =>
Located a -> a -> TError t
err Located LHName
sym LHName
x]
  | Bool
otherwise     = DataCtorP BareType -> Either [Error] (DataCtorP BareType)
forall a. a -> Either [Error] a
forall (m :: * -> *) a. Monad m => a -> m a
return DataCtorP BareType
d
    where
      sym :: Located LHName
sym         = DataCtorP BareType -> Located LHName
forall ty. DataCtorP ty -> Located LHName
dcName   DataCtorP BareType
d
      xts :: [(LHName, BareType)]
xts         = DataCtorP BareType -> [(LHName, BareType)]
forall ty. DataCtorP ty -> [(LHName, ty)]
dcFields DataCtorP BareType
d
      dups :: [LHName]
dups        = [ LHName
x | (LHName
x, [BareType]
ts) <- [(LHName, BareType)] -> [(LHName, [BareType])]
forall k v. (Eq k, Hashable k) => [(k, v)] -> [(k, [v])]
Misc.groupList [(LHName, BareType)]
xts, Int
2 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= [BareType] -> Int
forall a. [a] -> 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)

-- | Checks whether selectors shared across constructors have compatible types.
--
-- We only reject field names that would denote different selector sorts, because
-- those become duplicate logic definitions once selector measures are generated.
checkDataCtorFieldTypes :: [DataCtor] -> Bare.Lookup [DataCtor]
checkDataCtorFieldTypes :: [DataCtorP BareType] -> Lookup [DataCtorP BareType]
checkDataCtorFieldTypes [DataCtorP BareType]
ds
  | []     <- [TError (ZonkAny 0)]
forall {t}. [TError t]
errs = [DataCtorP BareType] -> Lookup [DataCtorP BareType]
forall a. a -> Either [Error] a
forall (m :: * -> *) a. Monad m => a -> m a
return [DataCtorP BareType]
ds
  | Error
e : [Error]
_  <- [Error]
forall {t}. [TError t]
errs = [Error] -> Lookup [DataCtorP BareType]
forall a b. a -> Either a b
Left [Error
e]
  | Bool
otherwise      = Maybe SrcSpan -> [Char] -> Lookup [DataCtorP BareType]
forall a. Maybe SrcSpan -> [Char] -> a
impossible Maybe SrcSpan
forall a. Maybe a
Nothing [Char]
"checkDataCtorFieldTypes"
  where
    errs :: [TError t]
errs = [ Symbol
-> [(Located LHName, RTypeBV Symbol Symbol BTyCon BTyVar NoReft,
     BareType)]
-> TError t
forall {a} {a} {a} {b} {t}.
(PPrint a, PPrint a, PPrint a) =>
a -> [(Located a, b, a)] -> TError t
err Symbol
x [(Located LHName, RTypeBV Symbol Symbol BTyCon BTyVar NoReft,
  BareType)]
xts
           | (Symbol
x, [(Located LHName, RTypeBV Symbol Symbol BTyCon BTyVar NoReft,
  BareType)]
xts) <- [(Symbol,
  (Located LHName, RTypeBV Symbol Symbol BTyCon BTyVar NoReft,
   BareType))]
-> [(Symbol,
     [(Located LHName, RTypeBV Symbol Symbol BTyCon BTyVar NoReft,
       BareType)])]
forall k v. (Eq k, Hashable k) => [(k, v)] -> [(k, [v])]
Misc.groupList [(Symbol,
  (Located LHName, RTypeBV Symbol Symbol BTyCon BTyVar NoReft,
   BareType))]
fieldTys
           , let tys :: [(Located LHName, RTypeBV Symbol Symbol BTyCon BTyVar NoReft,
  BareType)]
tys = ((Located LHName, RTypeBV Symbol Symbol BTyCon BTyVar NoReft,
  BareType)
 -> RTypeBV Symbol Symbol BTyCon BTyVar NoReft)
-> [(Located LHName, RTypeBV Symbol Symbol BTyCon BTyVar NoReft,
     BareType)]
-> [(Located LHName, RTypeBV Symbol Symbol BTyCon BTyVar NoReft,
     BareType)]
forall k a. (Eq k, Hashable k) => (a -> k) -> [a] -> [a]
Misc.nubHashOn (\(Located LHName
_, RTypeBV Symbol Symbol BTyCon BTyVar NoReft
s, BareType
_) -> RTypeBV Symbol Symbol BTyCon BTyVar NoReft
s) [(Located LHName, RTypeBV Symbol Symbol BTyCon BTyVar NoReft,
  BareType)]
xts
           , Int
2 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= [(Located LHName, RTypeBV Symbol Symbol BTyCon BTyVar NoReft,
  BareType)]
-> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Located LHName, RTypeBV Symbol Symbol BTyCon BTyVar NoReft,
  BareType)]
tys
           ]

    fieldTys :: [(Symbol,
  (Located LHName, RTypeBV Symbol Symbol BTyCon BTyVar NoReft,
   BareType))]
fieldTys =
      [ ( HasCallStack => LHName -> Symbol
LHName -> Symbol
lhNameToUnqualifiedSymbol LHName
x
        , (DataCtorP BareType -> Located LHName
forall ty. DataCtorP ty -> Located LHName
dcName DataCtorP BareType
d, BareType -> RTypeBV Symbol Symbol BTyCon BTyVar NoReft
forall b v c tv r.
Binder b =>
RTypeBV b v c tv r -> RTypeBV b v c tv (NoReftB b)
toRSort BareType
t, BareType
t)
        )
      | DataCtorP BareType
d <- [DataCtorP BareType]
ds
      , Maybe BareType -> Bool
forall a. Maybe a -> Bool
Mb.isNothing (DataCtorP BareType -> Maybe BareType
forall ty. DataCtorP ty -> Maybe ty
dcResult DataCtorP BareType
d)
      , (LHName
x, BareType
t) <- DataCtorP BareType -> [(LHName, BareType)]
forall ty. DataCtorP ty -> [(LHName, ty)]
dcFields DataCtorP BareType
d
      , Bool -> Bool
not (Symbol -> Bool
GM.isTmpSymbol (HasCallStack => LHName -> Symbol
LHName -> Symbol
lhNameToUnqualifiedSymbol LHName
x))
      ]

    err :: a -> [(Located a, b, a)] -> TError t
err a
x xts :: [(Located a, b, a)]
xts@((Located a
dc, b
_, a
_) : [(Located a, b, a)]
_) =
      SrcSpan -> Doc -> Doc -> TError t
forall t. SrcSpan -> Doc -> Doc -> TError t
ErrBadData (Located a -> SrcSpan
forall a. Loc a => a -> SrcSpan
GM.fSrcSpan Located a
dc) (a -> Doc
forall a. PPrint a => a -> Doc
pprint a
x) (Doc -> TError t) -> Doc -> TError t
forall a b. (a -> b) -> a -> b
$
        [Char] -> Doc
PJ.text [Char]
"Field has incompatible selector types across constructors:"
        Doc -> Doc -> Doc
PJ.$+$ Int -> Doc -> Doc
PJ.nest Int
4 ([Doc] -> Doc
PJ.vcat [ Doc -> Doc
PJ.parens (a -> Doc
forall a. PPrint a => a -> Doc
pprint (Located a -> a
forall a. Located a -> a
val Located a
dc')) Doc -> Doc -> Doc
<+> a -> Doc
forall a. PPrint a => a -> Doc
pprint a
x Doc -> Doc -> Doc
<+> Doc
"::" Doc -> Doc -> Doc
<+> a -> Doc
forall a. PPrint a => a -> Doc
pprint a
t | (Located a
dc', b
_, a
t) <- [(Located a, b, a)]
xts ])
    err a
_ [] =
      Maybe SrcSpan -> [Char] -> TError t
forall a. Maybe SrcSpan -> [Char] -> a
impossible Maybe SrcSpan
forall a. Maybe a
Nothing [Char]
"checkDataCtorFieldTypes"

selectDD :: (a, [DataDecl]) -> Either [DataDecl] DataDecl
selectDD :: forall a.
(a, [DataDeclP Symbol BareType])
-> Either [DataDeclP Symbol BareType] (DataDeclP Symbol BareType)
selectDD (a
_,[DataDeclP Symbol BareType
d]) = DataDeclP Symbol BareType
-> Either [DataDeclP Symbol BareType] (DataDeclP Symbol BareType)
forall a b. b -> Either a b
Right DataDeclP Symbol BareType
d
selectDD (a
_, [DataDeclP Symbol BareType]
ds) = case [ DataDeclP Symbol BareType
d | DataDeclP Symbol BareType
d <- [DataDeclP Symbol BareType]
ds, DataDeclP Symbol BareType -> DataDeclKind
forall v ty. DataDeclP v ty -> DataDeclKind
tycKind DataDeclP Symbol BareType
d DataDeclKind -> DataDeclKind -> Bool
forall a. Eq a => a -> a -> Bool
== DataDeclKind
DataUser ] of
                     [DataDeclP Symbol BareType
du] -> case [ DataDeclP Symbol BareType
d | DataDeclP Symbol BareType
d <- [DataDeclP Symbol BareType]
ds, DataDeclP Symbol BareType -> DataDeclKind
forall v ty. DataDeclP v ty -> DataDeclKind
tycKind DataDeclP Symbol BareType
d DataDeclKind -> DataDeclKind -> Bool
forall a. Eq a => a -> a -> Bool
== DataDeclKind
DataReflected ] of
                        [DataDeclP Symbol BareType
dr] -> DataDeclP Symbol BareType
-> Either [DataDeclP Symbol BareType] (DataDeclP Symbol BareType)
forall a b. b -> Either a b
Right DataDeclP Symbol BareType
dr
                        [] -> DataDeclP Symbol BareType
-> Either [DataDeclP Symbol BareType] (DataDeclP Symbol BareType)
forall a b. b -> Either a b
Right DataDeclP Symbol BareType
du
                        [DataDeclP Symbol BareType]
drs -> [DataDeclP Symbol BareType]
-> Either [DataDeclP Symbol BareType] (DataDeclP Symbol BareType)
forall a b. a -> Either a b
Left [DataDeclP Symbol BareType]
drs
                     [DataDeclP Symbol BareType]
dus -> [DataDeclP Symbol BareType]
-> Either [DataDeclP Symbol BareType] (DataDeclP Symbol BareType)
forall a b. a -> Either a b
Left [DataDeclP Symbol BareType]
dus

groupVariances :: [DataDecl]
               -> [(Located LHName, [Variance])]
               -> [(Maybe DataDecl, Maybe (Located LHName, [Variance]))]
groupVariances :: [DataDeclP Symbol BareType]
-> [(Located LHName, [Variance])]
-> [(Maybe (DataDeclP Symbol BareType),
     Maybe (Located LHName, [Variance]))]
groupVariances [DataDeclP Symbol BareType]
dcs [(Located LHName, [Variance])]
vdcs     =  [DataDeclP Symbol BareType]
-> [(Located LHName, [Variance])]
-> [(Maybe (DataDeclP Symbol BareType),
     Maybe (Located LHName, [Variance]))]
forall {v} {ty} {b}.
[DataDeclP v ty]
-> [(Located LHName, b)]
-> [(Maybe (DataDeclP v ty), Maybe (Located LHName, b))]
merge ([DataDeclP Symbol BareType] -> [DataDeclP Symbol BareType]
forall a. Ord a => [a] -> [a]
L.sort [DataDeclP Symbol BareType]
dcs) (((Located LHName, [Variance])
 -> (Located LHName, [Variance]) -> Ordering)
-> [(Located LHName, [Variance])] -> [(Located LHName, [Variance])]
forall a. (a -> a -> Ordering) -> [a] -> [a]
L.sortBy (\(Located LHName, [Variance])
x (Located LHName, [Variance])
y -> Located LHName -> Located LHName -> Ordering
forall a. Ord a => a -> a -> Ordering
compare ((Located LHName, [Variance]) -> Located LHName
forall a b. (a, b) -> a
fst (Located LHName, [Variance])
x) ((Located LHName, [Variance]) -> Located LHName
forall a b. (a, b) -> a
fst (Located LHName, [Variance])
y)) [(Located LHName, [Variance])]
vdcs)
  where
    merge :: [DataDeclP v ty]
-> [(Located LHName, b)]
-> [(Maybe (DataDeclP v ty), Maybe (Located LHName, b))]
merge (DataDeclP v ty
d:[DataDeclP v ty]
ds) ((Located LHName, b)
v:[(Located LHName, b)]
vs)
      | DataDeclP v ty -> LHName
forall {v} {ty}. DataDeclP v ty -> LHName
ddName DataDeclP v ty
d LHName -> LHName -> Bool
forall a. Eq a => a -> a -> Bool
== (Located LHName, b) -> LHName
forall {c} {b}. (Located c, b) -> c
sym (Located LHName, b)
v = (DataDeclP v ty -> Maybe (DataDeclP v ty)
forall a. a -> Maybe a
Just DataDeclP v ty
d, (Located LHName, b) -> Maybe (Located LHName, b)
forall a. a -> Maybe a
Just (Located LHName, b)
v)  (Maybe (DataDeclP v ty), Maybe (Located LHName, b))
-> [(Maybe (DataDeclP v ty), Maybe (Located LHName, b))]
-> [(Maybe (DataDeclP v ty), Maybe (Located LHName, b))]
forall a. a -> [a] -> [a]
: [DataDeclP v ty]
-> [(Located LHName, b)]
-> [(Maybe (DataDeclP v ty), Maybe (Located LHName, b))]
merge [DataDeclP v ty]
ds [(Located LHName, b)]
vs
      | DataDeclP v ty -> LHName
forall {v} {ty}. DataDeclP v ty -> LHName
ddName DataDeclP v ty
d LHName -> LHName -> Bool
forall a. Ord a => a -> a -> Bool
<  (Located LHName, b) -> LHName
forall {c} {b}. (Located c, b) -> c
sym (Located LHName, b)
v = (DataDeclP v ty -> Maybe (DataDeclP v ty)
forall a. a -> Maybe a
Just DataDeclP v ty
d, Maybe (Located LHName, b)
forall a. Maybe a
Nothing) (Maybe (DataDeclP v ty), Maybe (Located LHName, b))
-> [(Maybe (DataDeclP v ty), Maybe (Located LHName, b))]
-> [(Maybe (DataDeclP v ty), Maybe (Located LHName, b))]
forall a. a -> [a] -> [a]
: [DataDeclP v ty]
-> [(Located LHName, b)]
-> [(Maybe (DataDeclP v ty), Maybe (Located LHName, b))]
merge [DataDeclP v ty]
ds ((Located LHName, b)
v(Located LHName, b)
-> [(Located LHName, b)] -> [(Located LHName, b)]
forall a. a -> [a] -> [a]
:[(Located LHName, b)]
vs)
      | Bool
otherwise           = (Maybe (DataDeclP v ty)
forall a. Maybe a
Nothing, (Located LHName, b) -> Maybe (Located LHName, b)
forall a. a -> Maybe a
Just (Located LHName, b)
v) (Maybe (DataDeclP v ty), Maybe (Located LHName, b))
-> [(Maybe (DataDeclP v ty), Maybe (Located LHName, b))]
-> [(Maybe (DataDeclP v ty), Maybe (Located LHName, b))]
forall a. a -> [a] -> [a]
: [DataDeclP v ty]
-> [(Located LHName, b)]
-> [(Maybe (DataDeclP v ty), Maybe (Located LHName, b))]
merge (DataDeclP v ty
dDataDeclP v ty -> [DataDeclP v ty] -> [DataDeclP v ty]
forall a. a -> [a] -> [a]
:[DataDeclP v ty]
ds) [(Located LHName, b)]
vs
    merge []     [(Located LHName, b)]
vs         = (Maybe (DataDeclP v ty)
forall a. Maybe a
Nothing,) (Maybe (Located LHName, b)
 -> (Maybe (DataDeclP v ty), Maybe (Located LHName, b)))
-> ((Located LHName, b) -> Maybe (Located LHName, b))
-> (Located LHName, b)
-> (Maybe (DataDeclP v ty), Maybe (Located LHName, b))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Located LHName, b) -> Maybe (Located LHName, b)
forall a. a -> Maybe a
Just ((Located LHName, b)
 -> (Maybe (DataDeclP v ty), Maybe (Located LHName, b)))
-> [(Located LHName, b)]
-> [(Maybe (DataDeclP v ty), Maybe (Located LHName, b))]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Located LHName, b)]
vs
    merge [DataDeclP v ty]
ds     []         = (,Maybe (Located LHName, b)
forall a. Maybe a
Nothing) (Maybe (DataDeclP v ty)
 -> (Maybe (DataDeclP v ty), Maybe (Located LHName, b)))
-> (DataDeclP v ty -> Maybe (DataDeclP v ty))
-> DataDeclP v ty
-> (Maybe (DataDeclP v ty), Maybe (Located LHName, b))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataDeclP v ty -> Maybe (DataDeclP v ty)
forall a. a -> Maybe a
Just (DataDeclP v ty
 -> (Maybe (DataDeclP v ty), Maybe (Located LHName, b)))
-> [DataDeclP v ty]
-> [(Maybe (DataDeclP v ty), Maybe (Located LHName, b))]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [DataDeclP v ty]
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
    ddName :: DataDeclP v ty -> LHName
ddName = Located LHName -> LHName
forall a. Located a -> a
val (Located LHName -> LHName)
-> (DataDeclP v ty -> Located LHName) -> DataDeclP v ty -> LHName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataName -> Located LHName
dataNameSymbol (DataName -> Located LHName)
-> (DataDeclP v ty -> DataName) -> DataDeclP v ty -> Located LHName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataDeclP v ty -> DataName
forall v ty. DataDeclP v ty -> DataName
tycName


-- | '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 -> DataDeclP Symbol BareType -> Bool
checkDataDecl TyCon
c DataDeclP Symbol BareType
d = [Char] -> Bool -> Bool
forall a. PPrint a => [Char] -> a -> a
F.notracepp [Char]
_msg (Bool
isGADT Bool -> Bool -> Bool
|| Int
cN Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
dN Bool -> Bool -> Bool
|| Maybe [DataCtorP BareType] -> Bool
forall a. Maybe a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (DataDeclP Symbol BareType -> Maybe [DataCtorP BareType]
forall v ty. DataDeclP v ty -> Maybe [DataCtorP ty]
tycDCons DataDeclP Symbol BareType
d))
  where
    _msg :: [Char]
_msg          = [Char] -> [Char] -> [Char] -> Int -> Int -> [Char]
forall r. PrintfType r => [Char] -> r
printf [Char]
"checkDataDecl: D = %s, c = %s, cN = %d, dN = %d" (DataDeclP Symbol BareType -> [Char]
forall a. Show a => a -> [Char]
show DataDeclP Symbol BareType
d) (TyCon -> [Char]
forall a. Show a => a -> [Char]
show TyCon
c) Int
cN Int
dN
    cN :: Int
cN            = [Var] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (TyCon -> [Var]
GM.tyConTyVarsDef TyCon
c)
    dN :: Int
dN            = [Symbol] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (DataDeclP Symbol BareType -> [Symbol]
forall v ty. DataDeclP v ty -> [Symbol]
tycTyVars         DataDeclP Symbol BareType
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
  tcMb <- Env -> ModName -> DataName -> Lookup (Maybe TyCon)
Bare.lookupGhcDnTyCon Env
env ModName
name DataName
dn
  case tcMb of
    Just TyCon
tc -> TyCon -> Lookup TyCon
forall a. a -> Either [Error] a
forall (m :: * -> *) a. Monad m => a -> m a
return TyCon
tc
    Maybe TyCon
Nothing -> [Error] -> Lookup TyCon
forall a b. a -> Either a b
Left [ SrcSpan -> Doc -> Doc -> Error
forall t. SrcSpan -> Doc -> Doc -> TError t
ErrBadData (DataName -> SrcSpan
forall a. Loc a => a -> SrcSpan
GM.fSrcSpan DataName
dn) (DataName -> Doc
forall a. PPrint a => a -> Doc
pprint DataName
dn) Doc
"Unknown Type Constructor" ]
  --  ugh              = impossible Nothing "getDnTyCon"


-- FIXME: ES: why the maybes?
ofBDataDecl :: Bare.Env -> ModName -> Maybe DataDecl -> Maybe (Located LHName, [Variance])
            -> Bare.Lookup ( (ModName, TyConP, Maybe DataPropDecl), [Located DataConP] )
ofBDataDecl :: Env
-> ModName
-> Maybe (DataDeclP Symbol BareType)
-> Maybe (Located LHName, [Variance])
-> Lookup
     ((ModName, TyConP, Maybe DataPropDecl), [Located DataConP])
ofBDataDecl Env
env ModName
name (Just dd :: DataDeclP Symbol BareType
dd@(DataDecl DataName
tc [Symbol]
as [PVarV Symbol (RTypeBV Symbol Symbol BTyCon BTyVar NoReft)]
ps Maybe [DataCtorP BareType]
cts SourcePos
pos Maybe (SizeFunV Symbol)
sfun Maybe BareType
pt DataDeclKind
_)) Maybe (Located LHName, [Variance])
maybe_invariance_info = do
  let Loc SourcePos
lc SourcePos
lc' LHName
_ = DataName -> Located LHName
dataNameSymbol DataName
tc
  let πs :: [PVarBV Symbol Symbol (RType RTyCon RTyVar NoReft)]
πs           = Env
-> SourcePos
-> PVarV Symbol (RTypeBV Symbol Symbol BTyCon BTyVar NoReft)
-> PVarBV Symbol Symbol (RType RTyCon RTyVar NoReft)
Bare.ofBPVar Env
env SourcePos
pos (PVarV Symbol (RTypeBV Symbol Symbol BTyCon BTyVar NoReft)
 -> PVarBV Symbol Symbol (RType RTyCon RTyVar NoReft))
-> [PVarV Symbol (RTypeBV Symbol Symbol BTyCon BTyVar NoReft)]
-> [PVarBV Symbol Symbol (RType RTyCon RTyVar NoReft)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [PVarV Symbol (RTypeBV Symbol Symbol BTyCon BTyVar NoReft)]
ps
  let αs :: [RTyVar]
αs           = Var -> RTyVar
RTV (Var -> RTyVar) -> (Symbol -> Var) -> Symbol -> RTyVar
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Var
GM.symbolTyVar (Symbol -> RTyVar) -> [Symbol] -> [RTyVar]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol]
as
  let n :: Int
n            = [RTyVar] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [RTyVar]
αs
  let initmap :: [(PVarBV Symbol Symbol (), Int)]
initmap      = [PVarBV Symbol Symbol ()]
-> [Int] -> [(PVarBV Symbol Symbol (), Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip (PVarBV Symbol Symbol (RType RTyCon RTyVar NoReft)
-> PVarBV Symbol Symbol ()
forall v t. PVarV v t -> UsedPVarV v
RT.uPVar (PVarBV Symbol Symbol (RType RTyCon RTyVar NoReft)
 -> PVarBV Symbol Symbol ())
-> [PVarBV Symbol Symbol (RType RTyCon RTyVar NoReft)]
-> [PVarBV Symbol Symbol ()]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [PVarBV Symbol Symbol (RType RTyCon RTyVar NoReft)]
πs) [Int
0..]
  tc'             <- Env -> ModName -> DataName -> Lookup TyCon
getDnTyCon Env
env ModName
name DataName
tc
  cts'            <- mapM (ofBDataCtor env name lc lc' tc' αs ps πs) (Mb.fromMaybe [] cts)
  unless (checkDataDecl tc' dd) (Left [err])
  let pd           = HasCallStack =>
Env
-> SourcePos
-> Maybe
     [PVarV Symbol (RTypeBV Symbol Symbol BTyCon BTyVar NoReft)]
-> BareType
-> SpecType
Env
-> SourcePos
-> Maybe
     [PVarV Symbol (RTypeBV Symbol Symbol BTyCon BTyVar NoReft)]
-> BareType
-> SpecType
Bare.ofBareType Env
env SourcePos
lc ([PVarV Symbol (RTypeBV Symbol Symbol BTyCon BTyVar NoReft)]
-> Maybe
     [PVarV Symbol (RTypeBV Symbol Symbol BTyCon BTyVar NoReft)]
forall a. a -> Maybe a
Just []) (BareType -> SpecType) -> Maybe BareType -> Maybe SpecType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Char] -> Maybe BareType -> Maybe BareType
forall a. PPrint a => [Char] -> a -> a
F.tracepp [Char]
"ofBDataDecl-prop" Maybe BareType
pt
  let tys          = [SpecType
t | DataConP
dcp <- [DataConP]
cts', (LHName
_, SpecType
t) <- DataConP -> [(LHName, SpecType)]
dcpTyArgs DataConP
dcp]
  let 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 ([(PVarBV Symbol Symbol (), Int)]
-> Bool -> SpecType -> [(Int, Bool)]
forall a.
[(PVarBV Symbol Symbol (), a)] -> Bool -> SpecType -> [(a, Bool)]
getPsSig [(PVarBV Symbol Symbol (), Int)]
initmap Bool
True) [SpecType]
tys
  let 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 .. ([PVarBV Symbol Symbol (RType RTyCon RTyVar NoReft)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [PVarBV Symbol Symbol (RType RTyCon RTyVar NoReft)]
πs Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)]
  let (tvi, pvi)   = case maybe_invariance_info of
                       Maybe (Located LHName, [Variance])
Nothing     -> ([], [Variance]
defPs)
                       Just (Located LHName
_,[Variance]
is) -> let is_n :: [Variance]
is_n = Int -> [Variance] -> [Variance]
forall a. Int -> [a] -> [a]
drop Int
n [Variance]
is in
                                      (Int -> [Variance] -> [Variance]
forall a. Int -> [a] -> [a]
take Int
n [Variance]
is, if [Variance] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Variance]
is_n then [Variance]
defPs else [Variance]
is_n)
  let tcp          = SourcePos
-> TyCon
-> [RTyVar]
-> [PVarBV Symbol Symbol (RType RTyCon RTyVar NoReft)]
-> [Variance]
-> [Variance]
-> Maybe (SizeFunV Symbol)
-> TyConP
TyConP SourcePos
lc TyCon
tc' [RTyVar]
αs [PVarBV Symbol Symbol (RType RTyCon RTyVar NoReft)]
πs [Variance]
tvi [Variance]
pvi Maybe (SizeFunV Symbol)
sfun
  return ((name, tcp, Just (dd { tycDCons = cts }, pd)), Loc lc lc' <$> cts')
  where
    err :: TError t
err            = SrcSpan -> Doc -> Doc -> TError t
forall t. SrcSpan -> Doc -> Doc -> TError t
ErrBadData (DataName -> SrcSpan
forall a. Loc a => a -> SrcSpan
GM.fSrcSpan DataName
tc) (DataName -> Doc
forall a. PPrint a => a -> Doc
pprint DataName
tc) Doc
"Mismatch in number of type variables"

ofBDataDecl Env
env ModName
name Maybe (DataDeclP Symbol BareType)
Nothing (Just (Located LHName
tc, [Variance]
is)) =
  case HasCallStack => GHCTyLookupEnv -> Located LHName -> Lookup TyCon
GHCTyLookupEnv -> Located LHName -> Lookup TyCon
Bare.lookupGhcTyConLHName (Env -> GHCTyLookupEnv
Bare.reTyLookupEnv Env
env) Located LHName
tc of
    Left [Error]
e    -> [Error]
-> Lookup
     ((ModName, TyConP, Maybe DataPropDecl), [Located DataConP])
forall a b. a -> Either a b
Left [Error]
e
    Right TyCon
tc' -> ((ModName, TyConP, Maybe DataPropDecl), [Located DataConP])
-> Lookup
     ((ModName, TyConP, Maybe DataPropDecl), [Located DataConP])
forall a b. b -> Either a b
Right ((ModName
name, SourcePos
-> TyCon
-> [RTyVar]
-> [PVarBV Symbol Symbol (RType RTyCon RTyVar NoReft)]
-> [Variance]
-> [Variance]
-> Maybe (SizeFunV Symbol)
-> TyConP
TyConP SourcePos
srcpos TyCon
tc' [] [] [Variance]
tcov [Variance]
forall a. [a]
tcontr Maybe (SizeFunV Symbol)
forall a. Maybe a
Nothing, Maybe DataPropDecl
forall a. Maybe a
Nothing), [])
  where
    ([Variance]
tcov, [a]
tcontr) = ([Variance]
is, [])
    srcpos :: SourcePos
srcpos         = [Char] -> SourcePos
F.dummyPos [Char]
"LH.DataType.Variance"

ofBDataDecl Env
_ ModName
_ Maybe (DataDeclP Symbol BareType)
Nothing Maybe (Located LHName, [Variance])
Nothing
  = Maybe SrcSpan
-> [Char]
-> Lookup
     ((ModName, TyConP, Maybe DataPropDecl), [Located DataConP])
forall a. HasCallStack => Maybe SrcSpan -> [Char] -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing [Char]
"Bare.DataType.ofBDataDecl called on invalid inputs"

-- TODO:EFFECTS:ofBDataCon
ofBDataCtor :: Bare.Env
            -> ModName
            -> F.SourcePos
            -> F.SourcePos
            -> Ghc.TyCon
            -> [RTyVar]
            -> [PVar BSort]
            -> [PVar RSort]
            -> DataCtor
            -> Bare.Lookup DataConP
ofBDataCtor :: Env
-> ModName
-> SourcePos
-> SourcePos
-> TyCon
-> [RTyVar]
-> [PVarV Symbol (RTypeBV Symbol Symbol BTyCon BTyVar NoReft)]
-> [PVarBV Symbol Symbol (RType RTyCon RTyVar NoReft)]
-> DataCtorP BareType
-> Either [Error] DataConP
ofBDataCtor Env
env ModName
name SourcePos
l SourcePos
l' TyCon
tc [RTyVar]
αs [PVarV Symbol (RTypeBV Symbol Symbol BTyCon BTyVar NoReft)]
ps [PVarBV Symbol Symbol (RType RTyCon RTyVar NoReft)]
πs DataCtorP BareType
dc = do
  c' <- HasCallStack => Env -> Located LHName -> Either [Error] DataCon
Env -> Located LHName -> Either [Error] DataCon
Bare.lookupGhcDataConLHName Env
env (DataCtorP BareType -> Located LHName
forall ty. DataCtorP ty -> Located LHName
dcName DataCtorP BareType
dc)
  return (ofBDataCtorTc env name l l' tc αs ps πs dc 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]
-> [PVarV Symbol (RTypeBV Symbol Symbol BTyCon BTyVar NoReft)]
-> [PVarBV Symbol Symbol (RType RTyCon RTyVar NoReft)]
-> DataCtorP BareType
-> DataCon
-> DataConP
ofBDataCtorTc Env
env ModName
name SourcePos
l SourcePos
l' TyCon
tc [RTyVar]
αs [PVarV Symbol (RTypeBV Symbol Symbol BTyCon BTyVar NoReft)]
ps [PVarBV Symbol Symbol (RType RTyCon RTyVar NoReft)]
πs _ctor :: DataCtorP BareType
_ctor@(DataCtor Located LHName
_c [Symbol]
as [BareType]
_ [(LHName, 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 (Symbol -> RTyVar) -> [Symbol] -> [RTyVar]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol]
as
    , dcpFreePred :: [PVarBV Symbol Symbol (RType RTyCon RTyVar NoReft)]
dcpFreePred   = [PVarBV Symbol Symbol (RType RTyCon RTyVar NoReft)]
πs
    , dcpTyConstrs :: [SpecType]
dcpTyConstrs  = [SpecType]
cs
    , dcpTyArgs :: [(LHName, SpecType)]
dcpTyArgs     = [(LHName, SpecType)]
zts
    , dcpTyRes :: SpecType
dcpTyRes      = SpecType
ot
    , dcpIsGadt :: Bool
dcpIsGadt     = Bool
isGadt
    , dcpModule :: Symbol
dcpModule     = ModName -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol ModName
name
    , dcpLocE :: SourcePos
dcpLocE       = SourcePos
l'
    }
  where
    ts' :: [SpecType]
ts'           = HasCallStack =>
Env
-> SourcePos
-> Maybe
     [PVarV Symbol (RTypeBV Symbol Symbol BTyCon BTyVar NoReft)]
-> BareType
-> SpecType
Env
-> SourcePos
-> Maybe
     [PVarV Symbol (RTypeBV Symbol Symbol BTyCon BTyVar NoReft)]
-> BareType
-> SpecType
Bare.ofBareType Env
env SourcePos
l ([PVarV Symbol (RTypeBV Symbol Symbol BTyCon BTyVar NoReft)]
-> Maybe
     [PVarV Symbol (RTypeBV Symbol Symbol BTyCon BTyVar NoReft)]
forall a. a -> Maybe a
Just [PVarV Symbol (RTypeBV Symbol Symbol BTyCon BTyVar NoReft)]
ps) (BareType -> SpecType) -> [BareType] -> [SpecType]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [BareType]
ts
    res' :: Maybe SpecType
res'          = HasCallStack =>
Env
-> SourcePos
-> Maybe
     [PVarV Symbol (RTypeBV Symbol Symbol BTyCon BTyVar NoReft)]
-> BareType
-> SpecType
Env
-> SourcePos
-> Maybe
     [PVarV Symbol (RTypeBV Symbol Symbol BTyCon BTyVar NoReft)]
-> BareType
-> SpecType
Bare.ofBareType Env
env SourcePos
l ([PVarV Symbol (RTypeBV Symbol Symbol BTyCon BTyVar NoReft)]
-> Maybe
     [PVarV Symbol (RTypeBV Symbol Symbol BTyCon BTyVar NoReft)]
forall a. a -> Maybe a
Just [PVarV Symbol (RTypeBV Symbol Symbol BTyCon BTyVar NoReft)]
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
    yts :: [(LHName, SpecType)]
yts           = [LHName] -> [SpecType] -> [(LHName, SpecType)]
forall a b. [a] -> [b] -> [(a, b)]
zip [LHName]
xs [SpecType]
ts'
    ot :: SpecType
ot            = SpecType
t0'
    zts :: [(LHName, SpecType)]
zts           = (Int -> (LHName, SpecType) -> (LHName, SpecType))
-> [Int] -> [(LHName, SpecType)] -> [(LHName, SpecType)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (DataCon -> Int -> (LHName, SpecType) -> (LHName, SpecType)
forall a. DataCon -> Int -> (LHName, a) -> (LHName, a)
normalizeField DataCon
c') [Int
1..] ([(LHName, SpecType)] -> [(LHName, SpecType)]
forall a. [a] -> [a]
reverse [(LHName, SpecType)]
yts)
    usedTvs :: HashSet RTyVar
usedTvs       = [RTyVar] -> HashSet RTyVar
forall a. Hashable a => [a] -> HashSet a
S.fromList (RTVar RTyVar (RType RTyCon RTyVar NoReft) -> RTyVar
forall tv s. RTVar tv s -> tv
ty_var_value (RTVar RTyVar (RType RTyCon RTyVar NoReft) -> RTyVar)
-> [RTVar RTyVar (RType RTyCon RTyVar NoReft)] -> [RTyVar]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (SpecType -> [RTVar RTyVar (RType RTyCon RTyVar NoReft)])
-> [SpecType] -> [RTVar RTyVar (RType RTyCon RTyVar NoReft)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap SpecType -> [RTVar RTyVar (RType RTyCon RTyVar NoReft)]
forall tv v c r.
Eq tv =>
RTypeV v c tv r -> [RTVar tv (RTypeV v c tv NoReft)]
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. IsReft 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 ]
    ([LHName]
xs, [BareType]
ts)      = [(LHName, BareType)] -> ([LHName], [BareType])
forall a b. [(a, b)] -> ([a], [b])
unzip [(LHName, BareType)]
xts
    t0 :: SpecType
t0            = case TyCon -> Maybe Type
RT.famInstTyConType TyCon
tc of
                      Maybe Type
Nothing -> TyCon
-> [RTyVar]
-> [PVarBV Symbol Symbol (RType RTyCon RTyVar NoReft)]
-> SpecType
forall a. TyCon -> [RTyVar] -> [PVar a] -> SpecType
RT.gApp TyCon
tc [RTyVar]
αs [PVarBV Symbol Symbol (RType RTyCon RTyVar NoReft)]
πs
                      Just Type
ty -> Type -> SpecType
forall r. IsReft r => Type -> RRType r
RT.ofType Type
ty
    isGadt :: Bool
isGadt        = Maybe BareType -> Bool
forall a. Maybe a -> Bool
Mb.isJust Maybe BareType
res

errDataConMismatch :: LocSymbol -> S.HashSet F.Symbol -> S.HashSet F.Symbol -> Error
errDataConMismatch :: LocSymbol -> HashSet Symbol -> HashSet Symbol -> Error
errDataConMismatch LocSymbol
d HashSet Symbol
dcs HashSet Symbol
rdcs = SrcSpan -> Doc -> [Doc] -> [Doc] -> Error
forall t. SrcSpan -> Doc -> [Doc] -> [Doc] -> TError t
ErrDataConMismatch SrcSpan
sp Doc
v (Symbol -> Doc
forall a. PPrint a => a -> Doc
ppTicks (Symbol -> Doc) -> [Symbol] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HashSet Symbol -> [Symbol]
forall a. HashSet a -> [a]
S.toList HashSet Symbol
dcs) (Symbol -> Doc
forall a. PPrint a => a -> Doc
ppTicks (Symbol -> Doc) -> [Symbol] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HashSet Symbol -> [Symbol]
forall a. HashSet a -> [a]
S.toList HashSet Symbol
rdcs)
  where
    v :: Doc
v                 = Symbol -> Doc
forall a. PPrint a => a -> Doc
pprint (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)

varSignToVariance :: Eq a => [(a, Bool)] -> a -> Variance
varSignToVariance :: forall a. Eq a => [(a, Bool)] -> a -> Variance
varSignToVariance [(a, Bool)]
varsigns a
i = case ((a, Bool) -> Bool) -> [(a, Bool)] -> [(a, Bool)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\(a, Bool)
p -> (a, Bool) -> a
forall a b. (a, b) -> a
fst (a, Bool)
p a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
i) [(a, Bool)]
varsigns of
                                []       -> Variance
Invariant
                                [(a
_, Bool
b)] -> if Bool
b then Variance
Covariant else Variance
Contravariant
                                [(a, Bool)]
_        -> Variance
Bivariant

getPsSig :: [(UsedPVar, a)] -> Bool -> SpecType -> [(a, Bool)]
getPsSig :: forall a.
[(PVarBV Symbol Symbol (), a)] -> Bool -> SpecType -> [(a, Bool)]
getPsSig [(PVarBV Symbol Symbol (), a)]
m Bool
pos (RAllT RTVar RTyVar (RType RTyCon RTyVar NoReft)
_ SpecType
t UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r)
  = [(PVarBV Symbol Symbol (), a)]
-> Bool
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
-> [(a, Bool)]
forall a b t.
[(PVarBV Symbol Symbol (), a)] -> b -> UReft t -> [(a, b)]
addps [(PVarBV Symbol Symbol (), a)]
m Bool
pos UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r [(a, Bool)] -> [(a, Bool)] -> [(a, Bool)]
forall a. [a] -> [a] -> [a]
++  [(PVarBV Symbol Symbol (), a)] -> Bool -> SpecType -> [(a, Bool)]
forall a.
[(PVarBV Symbol Symbol (), a)] -> Bool -> SpecType -> [(a, Bool)]
getPsSig [(PVarBV Symbol Symbol (), a)]
m Bool
pos SpecType
t
getPsSig [(PVarBV Symbol Symbol (), a)]
m Bool
pos (RApp RTyCon
_ [SpecType]
ts [RTPropBV
   Symbol
   Symbol
   RTyCon
   RTyVar
   (UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
rs UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r)
  = [(PVarBV Symbol Symbol (), a)]
-> Bool
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
-> [(a, Bool)]
forall a b t.
[(PVarBV Symbol Symbol (), a)] -> b -> UReft t -> [(a, b)]
addps [(PVarBV Symbol Symbol (), a)]
m Bool
pos UReftBV Symbol Symbol (ReftBV Symbol Symbol)
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 ([(PVarBV Symbol Symbol (), a)] -> Bool -> SpecType -> [(a, Bool)]
forall a.
[(PVarBV Symbol Symbol (), a)] -> Bool -> SpecType -> [(a, Bool)]
getPsSig [(PVarBV Symbol Symbol (), a)]
m Bool
pos) [SpecType]
ts
    [(a, Bool)] -> [(a, Bool)] -> [(a, Bool)]
forall a. [a] -> [a] -> [a]
++ (RTPropBV
   Symbol
   Symbol
   RTyCon
   RTyVar
   (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
 -> [(a, Bool)])
-> [RTPropBV
      Symbol
      Symbol
      RTyCon
      RTyVar
      (UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
-> [(a, Bool)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ([(PVarBV Symbol Symbol (), a)]
-> Bool
-> RTPropBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> [(a, Bool)]
forall a.
[(PVarBV Symbol Symbol (), a)]
-> Bool
-> RTPropBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> [(a, Bool)]
getPsSigPs [(PVarBV Symbol Symbol (), a)]
m Bool
pos) [RTPropBV
   Symbol
   Symbol
   RTyCon
   RTyVar
   (UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
rs
getPsSig [(PVarBV Symbol Symbol (), a)]
m Bool
pos (RVar RTyVar
_ UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r)
  = [(PVarBV Symbol Symbol (), a)]
-> Bool
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
-> [(a, Bool)]
forall a b t.
[(PVarBV Symbol Symbol (), a)] -> b -> UReft t -> [(a, b)]
addps [(PVarBV Symbol Symbol (), a)]
m Bool
pos UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r
getPsSig [(PVarBV Symbol Symbol (), a)]
m Bool
pos (RAppTy SpecType
t1 SpecType
t2 UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r)
  = [(PVarBV Symbol Symbol (), a)]
-> Bool
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
-> [(a, Bool)]
forall a b t.
[(PVarBV Symbol Symbol (), a)] -> b -> UReft t -> [(a, b)]
addps [(PVarBV Symbol Symbol (), a)]
m Bool
pos UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r [(a, Bool)] -> [(a, Bool)] -> [(a, Bool)]
forall a. [a] -> [a] -> [a]
++ [(PVarBV Symbol Symbol (), a)] -> Bool -> SpecType -> [(a, Bool)]
forall a.
[(PVarBV Symbol Symbol (), a)] -> Bool -> SpecType -> [(a, Bool)]
getPsSig [(PVarBV Symbol Symbol (), a)]
m Bool
pos SpecType
t1 [(a, Bool)] -> [(a, Bool)] -> [(a, Bool)]
forall a. [a] -> [a] -> [a]
++ [(PVarBV Symbol Symbol (), a)] -> Bool -> SpecType -> [(a, Bool)]
forall a.
[(PVarBV Symbol Symbol (), a)] -> Bool -> SpecType -> [(a, Bool)]
getPsSig [(PVarBV Symbol Symbol (), a)]
m Bool
pos SpecType
t2
getPsSig [(PVarBV Symbol Symbol (), a)]
m Bool
pos (RFun Symbol
_ RFInfo
_ SpecType
t1 SpecType
t2 UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r)
  = [(PVarBV Symbol Symbol (), a)]
-> Bool
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
-> [(a, Bool)]
forall a b t.
[(PVarBV Symbol Symbol (), a)] -> b -> UReft t -> [(a, b)]
addps [(PVarBV Symbol Symbol (), a)]
m Bool
pos UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r [(a, Bool)] -> [(a, Bool)] -> [(a, Bool)]
forall a. [a] -> [a] -> [a]
++ [(PVarBV Symbol Symbol (), a)] -> Bool -> SpecType -> [(a, Bool)]
forall a.
[(PVarBV Symbol Symbol (), a)] -> Bool -> SpecType -> [(a, Bool)]
getPsSig [(PVarBV Symbol Symbol (), a)]
m Bool
pos SpecType
t2 [(a, Bool)] -> [(a, Bool)] -> [(a, Bool)]
forall a. [a] -> [a] -> [a]
++ [(PVarBV Symbol Symbol (), a)] -> Bool -> SpecType -> [(a, Bool)]
forall a.
[(PVarBV Symbol Symbol (), a)] -> Bool -> SpecType -> [(a, Bool)]
getPsSig [(PVarBV Symbol Symbol (), a)]
m (Bool -> Bool
not Bool
pos) SpecType
t1
getPsSig [(PVarBV Symbol Symbol (), a)]
m Bool
pos (RHole UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r)
  = [(PVarBV Symbol Symbol (), a)]
-> Bool
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
-> [(a, Bool)]
forall a b t.
[(PVarBV Symbol Symbol (), a)] -> b -> UReft t -> [(a, b)]
addps [(PVarBV Symbol Symbol (), a)]
m Bool
pos UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r
getPsSig [(PVarBV Symbol Symbol (), a)]
_ Bool
_ SpecType
z
  = Maybe SrcSpan -> [Char] -> [(a, Bool)]
forall a. HasCallStack => Maybe SrcSpan -> [Char] -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing ([Char] -> [(a, Bool)]) -> [Char] -> [(a, Bool)]
forall a b. (a -> b) -> a -> b
$ [Char]
"getPsSig" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ SpecType -> [Char]
forall a. Show a => a -> [Char]
show SpecType
z

getPsSigPs :: [(UsedPVar, a)] -> Bool -> SpecProp -> [(a, Bool)]
getPsSigPs :: forall a.
[(PVarBV Symbol Symbol (), a)]
-> Bool
-> RTPropBV
     Symbol
     Symbol
     RTyCon
     RTyVar
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> [(a, Bool)]
getPsSigPs [(PVarBV Symbol Symbol (), a)]
m Bool
pos (RProp [(Symbol, RType RTyCon RTyVar NoReft)]
_ (RHole UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r)) = [(PVarBV Symbol Symbol (), a)]
-> Bool
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
-> [(a, Bool)]
forall a b t.
[(PVarBV Symbol Symbol (), a)] -> b -> UReft t -> [(a, b)]
addps [(PVarBV Symbol Symbol (), a)]
m Bool
pos UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r
getPsSigPs [(PVarBV Symbol Symbol (), a)]
m Bool
pos (RProp [(Symbol, RType RTyCon RTyVar NoReft)]
_ SpecType
t) = [(PVarBV Symbol Symbol (), a)] -> Bool -> SpecType -> [(a, Bool)]
forall a.
[(PVarBV Symbol Symbol (), a)] -> Bool -> SpecType -> [(a, Bool)]
getPsSig [(PVarBV Symbol Symbol (), a)]
m Bool
pos SpecType
t

addps :: [(UsedPVar, a)] -> b -> UReft t -> [(a, b)]
addps :: forall a b t.
[(PVarBV Symbol Symbol (), a)] -> b -> UReft t -> [(a, b)]
addps [(PVarBV Symbol Symbol (), a)]
m b
pos (MkUReft t
_ PredicateBV Symbol Symbol
ps) = (, b
pos) (a -> (a, b))
-> (PVarBV Symbol Symbol () -> a)
-> PVarBV Symbol Symbol ()
-> (a, b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PVarBV Symbol Symbol () -> a
forall {t}. PVarBV Symbol Symbol t -> a
f  (PVarBV Symbol Symbol () -> (a, b))
-> [PVarBV Symbol Symbol ()] -> [(a, b)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PredicateBV Symbol Symbol -> [PVarBV Symbol Symbol ()]
forall b v. PredicateBV b v -> [UsedPVarBV b v]
pvars PredicateBV Symbol Symbol
ps
  where
    f :: PVarBV Symbol Symbol t -> a
f = a -> Maybe a -> a
forall a. a -> Maybe a -> a
Mb.fromMaybe (Maybe SrcSpan -> [Char] -> a
forall a. HasCallStack => Maybe SrcSpan -> [Char] -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing [Char]
"Bare.addPs: notfound") (Maybe a -> a)
-> (PVarBV Symbol Symbol t -> Maybe a)
-> PVarBV Symbol Symbol t
-> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (PVarBV Symbol Symbol ()
-> [(PVarBV Symbol Symbol (), a)] -> Maybe a
forall a b. Eq a => a -> [(a, b)] -> Maybe b
`L.lookup` [(PVarBV Symbol Symbol (), a)]
m) (PVarBV Symbol Symbol () -> Maybe a)
-> (PVarBV Symbol Symbol t -> PVarBV Symbol Symbol ())
-> PVarBV Symbol Symbol t
-> Maybe a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PVarBV Symbol Symbol t -> PVarBV Symbol Symbol ()
forall v t. PVarV v t -> UsedPVarV v
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. Hashable a => a -> HashSet a -> Bool
S.member RTyVar
tv HashSet RTyVar
tvs
  | Bool
otherwise                 = Bool
True


-- | This computes the result of a `DataCon` application.
--   For 'isVanillaDataCon' we can just use the `TyCon`
--   applied to the relevant tyvars.
dataConResultTy :: Ghc.DataCon
                -> [RTyVar]         -- ^ DataConP ty-vars
                -> SpecType         -- ^ vanilla result type
                -> Maybe SpecType   -- ^ user-provided result type
                -> SpecType
dataConResultTy :: DataCon -> [RTyVar] -> SpecType -> Maybe SpecType -> SpecType
dataConResultTy DataCon
c [RTyVar]
_ SpecType
_ (Just SpecType
t) = [Char] -> SpecType -> SpecType
forall a. PPrint a => [Char] -> a -> a
F.notracepp ([Char]
"dataConResultTy-3 : vanilla = " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Bool -> [Char]
forall a. Show a => a -> [Char]
show (DataCon -> Bool
Ghc.isVanillaDataCon DataCon
c) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" : ") SpecType
t
dataConResultTy DataCon
c [RTyVar]
_ SpecType
t Maybe SpecType
_
  | DataCon -> Bool
Ghc.isVanillaDataCon DataCon
c     = [Char] -> SpecType -> SpecType
forall a. PPrint a => [Char] -> a -> a
F.notracepp ([Char]
"dataConResultTy-1 : " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ DataCon -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp DataCon
c) SpecType
t
  | Bool
otherwise                  = [Char] -> SpecType -> SpecType
forall a. PPrint a => [Char] -> a -> a
F.notracepp ([Char]
"dataConResultTy-2 : " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ DataCon -> [Char]
forall a. PPrint a => a -> [Char]
F.showpp DataCon
c) (SpecType -> SpecType) -> SpecType -> SpecType
forall a b. (a -> b) -> a -> b
$ Type -> SpecType
forall r. IsReft 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 UReftBV Symbol Symbol (ReftBV Symbol Symbol)
_, SpecType
t] [RTPropBV
   Symbol
   Symbol
   RTyCon
   RTyVar
   (UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
_ UReftBV Symbol Symbol (ReftBV Symbol Symbol)
_)
  | 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 -> (LHName, a) -> (LHName, a)
normalizeField :: forall a. DataCon -> Int -> (LHName, a) -> (LHName, a)
normalizeField DataCon
c Int
i (LHName
x, a
t)
  | LHName -> Bool
isTmp LHName
x   = (LHName
xi, a
t)
  | Bool
otherwise = (LHName
x , a
t)
  where
    isTmp :: LHName -> Bool
isTmp     = Symbol -> Symbol -> Bool
F.isPrefixOfSym Symbol
F.tempPrefix (Symbol -> Bool) -> (LHName -> Symbol) -> LHName -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HasCallStack => LHName -> Symbol
LHName -> Symbol
lhNameToUnqualifiedSymbol
    xi :: LHName
xi        = Symbol -> LHName
makeGeneratedLogicLHName (Maybe DataConMap -> DataCon -> Int -> Symbol
makeDataConSelector Maybe DataConMap
forall a. Maybe a
Nothing DataCon
c Int
i)

checkRecordSelectorSigs :: [(Ghc.Var, LocSpecType)] -> [(Ghc.Var, LocSpecType)]
checkRecordSelectorSigs :: [(Var, LocSpecType)] -> [(Var, LocSpecType)]
checkRecordSelectorSigs [(Var, LocSpecType)]
vts = [ (Var
v, Var -> [LocSpecType] -> LocSpecType
forall {a} {a}.
(PPrint a, PPrint a) =>
a -> [Located a] -> Located a
take1 Var
v [LocSpecType]
lspecTys) | (Var
v, [LocSpecType]
lspecTys) <- [(Var, LocSpecType)] -> [(Var, [LocSpecType])]
forall k v. (Eq k, Hashable k) => [(k, v)] -> [(k, [v])]
Misc.groupList [(Var, LocSpecType)]
vts ]
  where
    take1 :: a -> [Located a] -> Located a
take1 a
v [Located a]
lsts            = case (Located a -> [Char]) -> [Located a] -> [Located a]
forall k a. (Eq k, Hashable k) => (a -> k) -> [a] -> [a]
Misc.nubHashOn (a -> [Char]
forall a. PPrint a => a -> [Char]
showpp (a -> [Char]) -> (Located a -> a) -> Located a -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Located a -> a
forall a. Located a -> a
val) [Located a]
lsts of
                                [Located a
t]    -> Located a
t
                                (Located a
t:[Located a]
ts) -> Error -> Located a
forall a e. (HasCallStack, 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 -> [Char] -> Located a
forall a. Maybe SrcSpan -> [Char] -> a
impossible Maybe SrcSpan
forall a. Maybe a
Nothing [Char]
"checkRecordSelectorSigs"


strengthenClassSel :: Ghc.Var -> LocSpecType -> LocSpecType
strengthenClassSel :: Var -> LocSpecType -> LocSpecType
strengthenClassSel Var
v LocSpecType
lt = LocSpecType
lt { val = st }
 where
  st :: SpecType
st = Reader (Int, [Symbol]) SpecType -> (Int, [Symbol]) -> SpecType
forall r a. Reader r a -> r -> a
runReader (SpecType -> Reader (Int, [Symbol]) SpecType
go (LocSpecType -> SpecType
forall a. Located a -> a
F.val LocSpecType
lt)) (Int
1, [])
  s :: LocSymbol
s = Var -> LocSymbol
forall a. (Symbolic a, NamedThing a) => a -> LocSymbol
GM.namedLocSymbol Var
v
  extend :: F.Symbol -> (Int, [F.Symbol]) -> (Int, [F.Symbol])
  extend :: Symbol -> (Int, [Symbol]) -> (Int, [Symbol])
extend Symbol
x (Int
i, [Symbol]
xs) = (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1, Symbol
x Symbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
: [Symbol]
xs)
  go :: SpecType -> Reader (Int, [F.Symbol]) SpecType
  go :: SpecType -> Reader (Int, [Symbol]) SpecType
go (RAllT RTVar RTyVar (RType RTyCon RTyVar NoReft)
a SpecType
t UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r) = RTVar RTyVar (RType RTyCon RTyVar NoReft)
-> SpecType
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
-> SpecType
forall b v c tv r.
RTVUBV b v c tv -> RTypeBV b v c tv r -> r -> RTypeBV b v c tv r
RAllT RTVar RTyVar (RType RTyCon RTyVar NoReft)
a (SpecType
 -> UReftBV Symbol Symbol (ReftBV Symbol Symbol) -> SpecType)
-> Reader (Int, [Symbol]) SpecType
-> ReaderT
     (Int, [Symbol])
     Identity
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol) -> SpecType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SpecType -> Reader (Int, [Symbol]) SpecType
go SpecType
t ReaderT
  (Int, [Symbol])
  Identity
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol) -> SpecType)
-> ReaderT
     (Int, [Symbol])
     Identity
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> Reader (Int, [Symbol]) SpecType
forall a b.
ReaderT (Int, [Symbol]) Identity (a -> b)
-> ReaderT (Int, [Symbol]) Identity a
-> ReaderT (Int, [Symbol]) Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
-> ReaderT
     (Int, [Symbol])
     Identity
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
forall a. a -> ReaderT (Int, [Symbol]) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r
  go (RAllP PVarBV Symbol Symbol (RType RTyCon RTyVar NoReft)
p SpecType
t  ) = PVarBV Symbol Symbol (RType RTyCon RTyVar NoReft)
-> SpecType -> SpecType
forall b v c tv r.
PVUBV b v c tv -> RTypeBV b v c tv r -> RTypeBV b v c tv r
RAllP PVarBV Symbol Symbol (RType RTyCon RTyVar NoReft)
p (SpecType -> SpecType)
-> Reader (Int, [Symbol]) SpecType
-> Reader (Int, [Symbol]) SpecType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SpecType -> Reader (Int, [Symbol]) SpecType
go SpecType
t
  go (RFun Symbol
x RFInfo
i SpecType
tx SpecType
t UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r) | SpecType -> Bool
forall c v t t1. TyConable c => RTypeV v c t t1 -> Bool
isEmbeddedClass SpecType
tx =
    Symbol
-> RFInfo
-> SpecType
-> SpecType
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
-> SpecType
forall b v c tv r.
b
-> RFInfo
-> RTypeBV b v c tv r
-> RTypeBV b v c tv r
-> r
-> RTypeBV b v c tv r
RFun Symbol
x RFInfo
i SpecType
tx (SpecType
 -> UReftBV Symbol Symbol (ReftBV Symbol Symbol) -> SpecType)
-> Reader (Int, [Symbol]) SpecType
-> ReaderT
     (Int, [Symbol])
     Identity
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol) -> SpecType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SpecType -> Reader (Int, [Symbol]) SpecType
go SpecType
t ReaderT
  (Int, [Symbol])
  Identity
  (UReftBV Symbol Symbol (ReftBV Symbol Symbol) -> SpecType)
-> ReaderT
     (Int, [Symbol])
     Identity
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> Reader (Int, [Symbol]) SpecType
forall a b.
ReaderT (Int, [Symbol]) Identity (a -> b)
-> ReaderT (Int, [Symbol]) Identity a
-> ReaderT (Int, [Symbol]) Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
-> ReaderT
     (Int, [Symbol])
     Identity
     (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
forall a. a -> ReaderT (Int, [Symbol]) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r
  go (RFun Symbol
x RFInfo
i SpecType
tx SpecType
t UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r) = do
    x' <- Symbol -> Int -> Symbol
unDummy Symbol
x (Int -> Symbol)
-> ReaderT (Int, [Symbol]) Identity Int
-> ReaderT (Int, [Symbol]) Identity Symbol
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Int, [Symbol]) -> Int) -> ReaderT (Int, [Symbol]) Identity Int
forall a.
((Int, [Symbol]) -> a) -> ReaderT (Int, [Symbol]) Identity a
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
reader (Int, [Symbol]) -> Int
forall a b. (a, b) -> a
fst
    r' <- singletonApp s <$> (L.reverse <$> reader snd)
    RFun x' i tx <$> local (extend x') (go t) <*> pure (meet r r')
  go SpecType
t = SpecType
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol) -> SpecType
forall r b v c tv.
Meet r =>
RTypeBV b v c tv r -> r -> RTypeBV b v c tv r
RT.strengthen SpecType
t (UReftBV Symbol Symbol (ReftBV Symbol Symbol) -> SpecType)
-> ([Symbol] -> UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> [Symbol]
-> SpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LocSymbol
-> [Symbol] -> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
forall a.
Symbolic a =>
LocSymbol -> [a] -> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
singletonApp LocSymbol
s ([Symbol] -> UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> ([Symbol] -> [Symbol])
-> [Symbol]
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Symbol] -> [Symbol]
forall a. [a] -> [a]
L.reverse ([Symbol] -> SpecType)
-> ReaderT (Int, [Symbol]) Identity [Symbol]
-> Reader (Int, [Symbol]) SpecType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Int, [Symbol]) -> [Symbol])
-> ReaderT (Int, [Symbol]) Identity [Symbol]
forall a.
((Int, [Symbol]) -> a) -> ReaderT (Int, [Symbol]) Identity a
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
reader (Int, [Symbol]) -> [Symbol]
forall a b. (a, b) -> b
snd

singletonApp :: F.Symbolic a => F.LocSymbol -> [a] -> UReft F.Reft
singletonApp :: forall a.
Symbolic a =>
LocSymbol -> [a] -> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
singletonApp LocSymbol
s [a]
ys = ReftBV Symbol Symbol
-> PredicateBV Symbol Symbol
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
forall b v r. r -> PredicateBV b v -> UReftBV b v r
MkUReft ReftBV Symbol Symbol
r PredicateBV Symbol Symbol
forall a. Monoid a => a
mempty
  where r :: ReftBV Symbol Symbol
r = Expr -> ReftBV Symbol Symbol
forall a. Expression a => a -> ReftBV Symbol Symbol
F.exprReft (LocSymbol -> [Expr] -> Expr
forall v b. Located v -> [ExprBV b v] -> ExprBV b v
F.mkEApp LocSymbol
s (a -> Expr
forall a. Symbolic a => a -> Expr
F.eVar (a -> Expr) -> [a] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [a]
ys))


unDummy :: F.Symbol -> Int -> F.Symbol
unDummy :: Symbol -> Int -> Symbol
unDummy Symbol
x Int
i | Symbol
x Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
/= Symbol
F.dummySymbol = Symbol
x
            | Bool
otherwise          = [Char] -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol ([Char]
"_cls_lq" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show Int
i)

makeRecordSelectorSigs :: Bare.Env -> [Located DataConP] -> [(Ghc.Var, LocSpecType)]
makeRecordSelectorSigs :: Env -> [Located DataConP] -> [(Var, LocSpecType)]
makeRecordSelectorSigs Env
env = [(Var, LocSpecType)] -> [(Var, LocSpecType)]
checkRecordSelectorSigs ([(Var, LocSpecType)] -> [(Var, LocSpecType)])
-> ([Located DataConP] -> [(Var, LocSpecType)])
-> [Located DataConP]
-> [(Var, LocSpecType)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Located DataConP -> [(Var, LocSpecType)])
-> [Located DataConP] -> [(Var, LocSpecType)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Located DataConP -> [(Var, LocSpecType)]
makeOne
  where
  makeOne :: Located DataConP -> [(Var, LocSpecType)]
makeOne (Loc SourcePos
l SourcePos
l' DataConP
dcp)
    | Just Class
cls <- Maybe Class
maybe_cls
    = let cfs :: [Var]
cfs = Class -> [Var]
Ghc.classAllSelIds Class
cls in
        ((Var, LocSpecType) -> (Var, LocSpecType))
-> [(Var, LocSpecType)] -> [(Var, LocSpecType)]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((,) (Var -> LocSpecType -> (Var, LocSpecType))
-> ((Var, LocSpecType) -> Var)
-> (Var, LocSpecType)
-> LocSpecType
-> (Var, LocSpecType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Var, LocSpecType) -> Var
forall a b. (a, b) -> a
fst ((Var, LocSpecType) -> LocSpecType -> (Var, LocSpecType))
-> ((Var, LocSpecType) -> LocSpecType)
-> (Var, LocSpecType)
-> (Var, LocSpecType)
forall a b.
((Var, LocSpecType) -> a -> b)
-> ((Var, LocSpecType) -> a) -> (Var, LocSpecType) -> b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Var -> LocSpecType -> LocSpecType)
-> (Var, LocSpecType) -> LocSpecType
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Var -> LocSpecType -> LocSpecType
strengthenClassSel)
          [(Var
v, SourcePos -> SourcePos -> SpecType -> LocSpecType
forall a. SourcePos -> SourcePos -> a -> Located a
Loc SourcePos
l SourcePos
l' SpecType
t)| (Var
v,SpecType
t) <- [Var] -> [SpecType] -> [(Var, SpecType)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Var]
cfs ([SpecType] -> [SpecType]
forall a. [a] -> [a]
reverse ([SpecType] -> [SpecType]) -> [SpecType] -> [SpecType]
forall a b. (a -> b) -> a -> b
$ ((LHName, SpecType) -> SpecType)
-> [(LHName, SpecType)] -> [SpecType]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (LHName, SpecType) -> SpecType
forall a b. (a, b) -> b
snd [(LHName, SpecType)]
args)]
    | [FieldLabel] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [FieldLabel]
fls                    --    no field labels
    Bool -> Bool -> Bool
|| ((LHName, SpecType) -> Bool) -> [(LHName, 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)
-> ((LHName, SpecType) -> SpecType) -> (LHName, SpecType) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (LHName, SpecType) -> SpecType
forall a b. (a, b) -> b
snd) [(LHName, SpecType)]
args Bool -> Bool -> Bool
&& Bool -> Bool
not (Env -> Bool
forall t. HasConfig t => t -> Bool
higherOrderFlag Env
env)   -- OR function-valued fields
    Bool -> Bool -> Bool
|| DataConP -> Bool
dcpIsGadt DataConP
dcp              -- OR GADT style datcon
    = []
    | Bool
otherwise
    = [ (Var
v, LocSpecType
t) | (Just Var
v, LocSpecType
t) <- [Maybe Var] -> [LocSpecType] -> [(Maybe Var, LocSpecType)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Maybe Var]
fs [LocSpecType]
ts ]
    where
      maybe_cls :: Maybe Class
maybe_cls = TyCon -> Maybe Class
Ghc.tyConClass_maybe (DataCon -> TyCon
Ghc.dataConTyCon DataCon
dc)
      dc :: DataCon
dc  = DataConP -> DataCon
dcpCon DataConP
dcp
      fls :: [FieldLabel]
fls = DataCon -> [FieldLabel]
Ghc.dataConFieldLabels DataCon
dc
      fs :: [Maybe Var]
fs  = Env -> Name -> Maybe Var
Bare.lookupGhcId Env
env (Name -> Maybe Var)
-> (FieldLabel -> Name) -> FieldLabel -> Maybe Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FieldLabel -> Name
Ghc.flSelector (FieldLabel -> Maybe Var) -> [FieldLabel] -> [Maybe Var]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [FieldLabel]
fls
      ts :: [ LocSpecType ]
      ts :: [LocSpecType]
ts = [ SourcePos -> SourcePos -> SpecType -> LocSpecType
forall a. SourcePos -> SourcePos -> a -> Located a
Loc SourcePos
l SourcePos
l' ([(RTVar RTyVar (RType RTyCon RTyVar NoReft),
  UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
-> [PVarBV Symbol Symbol (RType RTyCon RTyVar NoReft)]
-> [(Symbol, RFInfo, SpecType,
     UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
-> SpecType
-> SpecType
forall tv b v c r.
[(RTVar tv (RTypeBV b v c tv (NoReftB b)), r)]
-> [PVarBV b v (RTypeBV b v c tv (NoReftB b))]
-> [(b, RFInfo, RTypeBV b v c tv r, r)]
-> RTypeBV b v c tv r
-> RTypeBV b v c tv r
mkArrow ((RTVar RTyVar (RType RTyCon RTyVar NoReft)
 -> (RTVar RTyVar (RType RTyCon RTyVar NoReft),
     UReftBV Symbol Symbol (ReftBV Symbol Symbol)))
-> [RTVar RTyVar (RType RTyCon RTyVar NoReft)]
-> [(RTVar RTyVar (RType RTyCon RTyVar NoReft),
     UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
forall a b. (a -> b) -> [a] -> [b]
map (, UReftBV Symbol Symbol (ReftBV Symbol Symbol)
forall a. Monoid a => a
mempty) (RTyVar -> RTVar RTyVar (RType RTyCon RTyVar NoReft)
forall tv s. tv -> RTVar tv s
makeRTVar (RTyVar -> RTVar RTyVar (RType RTyCon RTyVar NoReft))
-> [RTyVar] -> [RTVar RTyVar (RType RTyCon RTyVar NoReft)]
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, UReftBV Symbol Symbol (ReftBV Symbol Symbol)
forall a. Monoid a => a
mempty)]
                                 (SpecType -> SpecType
forall {b} {v} {r}.
RTypeBV Symbol Symbol RTyCon RTyVar (UReftBV b v r)
-> RTypeBV Symbol Symbol RTyCon RTyVar (UReftBV Symbol Symbol r)
dropPreds (SubstV (Variable SpecType) -> SpecType -> SpecType
forall a.
(Subable a, HasCallStack) =>
SubstV (Variable a) -> a -> a
F.subst SubstV Symbol
SubstV (Variable SpecType)
su SpecType
t SpecType
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol) -> SpecType
forall r b v c tv.
Meet r =>
RTypeBV b v c tv r -> r -> RTypeBV b v c tv r
`RT.strengthen` UReftBV Symbol Symbol (ReftBV Symbol Symbol)
mt)))
             | (LHName
x, SpecType
t) <- [(LHName, SpecType)] -> [(LHName, SpecType)]
forall a. [a] -> [a]
reverse [(LHName, SpecType)]
args -- NOTE: the reverse here is correct
             , let vv :: ReftBind (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
vv = SpecType -> ReftBind (UReftBV Symbol Symbol (ReftBV Symbol Symbol))
forall r b v c tv.
(ToReft r, Binder (ReftBind r)) =>
RTypeBV b v c tv r -> ReftBind r
rTypeValueVar SpecType
t
               -- the measure singleton refinement, eg `v = getBar foo`
             , let mt :: UReftBV Symbol Symbol (ReftBV Symbol Symbol)
mt = (Symbol, Expr) -> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
RT.uReft (Symbol
vv, Brel -> Expr -> Expr -> Expr
forall b v. Brel -> ExprBV b v -> ExprBV b v -> ExprBV b v
F.PAtom Brel
F.Eq (Symbol -> Expr
forall b v. v -> ExprBV b v
F.EVar Symbol
vv) (Expr -> Expr -> Expr
forall b v. ExprBV b v -> ExprBV b v -> ExprBV b v
F.EApp (Symbol -> Expr
forall b v. v -> ExprBV b v
F.EVar (Symbol -> Expr) -> Symbol -> Expr
forall a b. (a -> b) -> a -> b
$ LHName -> Symbol
lhNameToResolvedSymbol LHName
x) (Symbol -> Expr
forall b v. v -> ExprBV b v
F.EVar Symbol
z)))
             ]

      su :: SubstV Symbol
su   = [(Symbol, Expr)] -> SubstV Symbol
forall v. Hashable v => [(v, ExprBV v v)] -> SubstV v
F.mkSubst [ (HasCallStack => LHName -> Symbol
LHName -> Symbol
lhNameToUnqualifiedSymbol LHName
x, Expr -> Expr -> Expr
forall b v. ExprBV b v -> ExprBV b v -> ExprBV b v
F.EApp (Symbol -> Expr
forall b v. v -> ExprBV b v
F.EVar (LHName -> Symbol
lhNameToResolvedSymbol LHName
x)) (Symbol -> Expr
forall b v. v -> ExprBV b v
F.EVar Symbol
z)) | LHName
x <- (LHName, SpecType) -> LHName
forall a b. (a, b) -> a
fst ((LHName, SpecType) -> LHName) -> [(LHName, SpecType)] -> [LHName]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(LHName, SpecType)]
args ]
      args :: [(LHName, SpecType)]
args = DataConP -> [(LHName, SpecType)]
dcpTyArgs DataConP
dcp
      z :: Symbol
z    = Symbol
"lq$recSel"
      res :: SpecType
res  = SpecType -> SpecType
forall {b} {v} {r}.
RTypeBV Symbol Symbol RTyCon RTyVar (UReftBV b v r)
-> RTypeBV Symbol Symbol RTyCon RTyVar (UReftBV Symbol Symbol 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 :: RTypeBV Symbol Symbol RTyCon RTyVar (UReftBV b v r)
-> RTypeBV Symbol Symbol RTyCon RTyVar (UReftBV Symbol Symbol r)
dropPreds = (UReftBV b v r -> UReftBV Symbol Symbol r)
-> RTypeBV Symbol Symbol RTyCon RTyVar (UReftBV b v r)
-> RTypeBV Symbol Symbol RTyCon RTyVar (UReftBV Symbol Symbol r)
forall a b.
(a -> b)
-> RTypeBV Symbol Symbol RTyCon RTyVar a
-> RTypeBV Symbol Symbol RTyCon RTyVar b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(MkUReft r
r PredicateBV b v
_ps) -> r -> PredicateBV Symbol Symbol -> UReftBV Symbol Symbol r
forall b v r. r -> PredicateBV b v -> UReftBV b v r
MkUReft r
r PredicateBV Symbol Symbol
forall a. Monoid a => a
mempty)