{-# LANGUAGE OverloadedStrings     #-}
{-# LANGUAGE PartialTypeSignatures #-}

{-# OPTIONS_GHC -Wno-incomplete-record-updates #-}
{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}

module Language.Haskell.Liquid.Bare.Plugged
  ( makePluggedSig
  , makePluggedDataCon
  ) where

import Prelude hiding (error)
import Data.Generics.Aliases (mkT)
import Data.Generics.Schemes (everywhere)

import           Text.PrettyPrint.HughesPJ
import qualified Control.Exception                 as Ex
import qualified Data.HashMap.Strict               as M
import qualified Data.HashSet                      as S
import qualified Data.Maybe                        as Mb
import qualified Data.List                         as L
import qualified Language.Fixpoint.Types           as F
import qualified Language.Fixpoint.Types.Visitor   as F
import qualified Language.Haskell.Liquid.GHC.Misc  as GM
import qualified Liquid.GHC.API   as Ghc
import           Language.Haskell.Liquid.GHC.Types (StableName, mkStableName)
import           Language.Haskell.Liquid.Types.RefType ()
import           Language.Haskell.Liquid.Types
import qualified Language.Haskell.Liquid.Misc       as Misc
import qualified Language.Haskell.Liquid.Bare.Types as Bare
import qualified Language.Haskell.Liquid.Bare.Misc  as Bare

---------------------------------------------------------------------------------------
-- [NOTE: Plug-Holes-TyVars] We have _two_ versions of `plugHoles:
-- * `HsTyVars` ensures that the returned signature uses the GHC type variables;
--   We need this as these tyvars can appear in the SOURCE (as type annotations, or
--   as the types of lambdas) and renaming them will cause problems;
-- * `LqTyVars` ensures that the returned signatuer uses the LIQUID type variables;
--   We need this e.g. for class specifications where we cannot change the tyvars
--   used inside method signatures as that messes up the type for the data-constructor
--   for the dictionary (as we need to use the same tyvars as are "bound" in the class
--   definition).
-- In short, use `HsTyVars` when we also have to analyze the binder's SOURCE; and
-- otherwise, use `LqTyVars`.
---------------------------------------------------------------------------------------

--------------------------------------------------------------------------------
-- | NOTE: Be *very* careful with the use functions from RType -> GHC.Type,
--   e.g. toType, in this module as they cannot handle LH type holes. Since
--   this module is responsible for plugging the holes we obviously cannot
--   assume, as in e.g. L.H.L.Constraint.* that they do not appear.
--------------------------------------------------------------------------------
makePluggedSig :: Bool -> ModName -> F.TCEmb Ghc.TyCon -> TyConMap -> S.HashSet StableName
               -> Bare.PlugTV Ghc.Var -> LocSpecType
               -> LocSpecType

makePluggedSig :: Bool
-> ModName
-> TCEmb TyCon
-> TyConMap
-> HashSet StableName
-> PlugTV Var
-> LocSpecType
-> LocSpecType
makePluggedSig Bool
allowTC ModName
name TCEmb TyCon
embs TyConMap
tyi HashSet StableName
exports PlugTV Var
kx LocSpecType
t
  | Just Var
x <- Maybe Var
kxv = Var -> LocSpecType
mkPlug Var
x
  | Bool
otherwise     = LocSpecType
t
  where
    kxv :: Maybe Var
kxv           = forall v. PlugTV v -> Maybe v
Bare.plugSrc PlugTV Var
kx
    mkPlug :: Var -> LocSpecType
mkPlug Var
x      = forall a.
(NamedThing a, PPrint a, Show a) =>
Bool
-> PlugTV a
-> TCEmb TyCon
-> TyConMap
-> (SpecType -> UReft Reft -> UReft Reft)
-> Type
-> LocSpecType
-> LocSpecType
plugHoles Bool
allowTC PlugTV Var
kx TCEmb TyCon
embs TyConMap
tyi  SpecType -> UReft Reft -> UReft Reft
r Type
τ LocSpecType
t
      where
        τ :: Type
τ         = Type -> Type
Ghc.expandTypeSynonyms (Var -> Type
Ghc.varType Var
x)
        r :: SpecType -> UReft Reft -> UReft Reft
r         = forall a.
NamedThing a =>
a
-> ModName
-> HashSet StableName
-> SpecType
-> UReft Reft
-> UReft Reft
maybeTrue Var
x ModName
name HashSet StableName
exports
    -- x = case kx of { Bare.HsTV x -> x ; Bare.LqTV x -> x }


-- makePluggedDataCon = makePluggedDataCon_old
-- plugHoles          = plugHolesOld
-- makePluggedDataCon = makePluggedDataCon_new

-- plugHoles _         = plugHolesOld

plugHoles :: (Ghc.NamedThing a, PPrint a, Show a)
          => Bool
          -> Bare.PlugTV a
          -> F.TCEmb Ghc.TyCon
          -> Bare.TyConMap
          -> (SpecType -> RReft -> RReft)
          -> Ghc.Type
          -> LocSpecType
          -> LocSpecType
plugHoles :: forall a.
(NamedThing a, PPrint a, Show a) =>
Bool
-> PlugTV a
-> TCEmb TyCon
-> TyConMap
-> (SpecType -> UReft Reft -> UReft Reft)
-> Type
-> LocSpecType
-> LocSpecType
plugHoles Bool
allowTC (Bare.HsTV a
x) TCEmb TyCon
a TyConMap
b = forall a.
(NamedThing a, PPrint a, Show a) =>
Bool
-> TCEmb TyCon
-> TyConMap
-> a
-> (SpecType -> UReft Reft -> UReft Reft)
-> Type
-> LocSpecType
-> LocSpecType
plugHolesOld Bool
allowTC TCEmb TyCon
a TyConMap
b a
x
plugHoles Bool
allowTC (Bare.LqTV a
x) TCEmb TyCon
a TyConMap
b = forall a.
(NamedThing a, PPrint a, Show a) =>
Bool
-> TCEmb TyCon
-> TyConMap
-> a
-> (SpecType -> UReft Reft -> UReft Reft)
-> Type
-> LocSpecType
-> LocSpecType
plugHolesNew Bool
allowTC TCEmb TyCon
a TyConMap
b a
x
plugHoles Bool
_ PlugTV a
_                   TCEmb TyCon
_ TyConMap
_ = \SpecType -> UReft Reft -> UReft Reft
_ Type
_ LocSpecType
t -> LocSpecType
t


makePluggedDataCon :: Bool -> F.TCEmb Ghc.TyCon -> Bare.TyConMap -> Located DataConP -> Located DataConP
makePluggedDataCon :: Bool
-> TCEmb TyCon -> TyConMap -> Located DataConP -> Located DataConP
makePluggedDataCon Bool
allowTC TCEmb TyCon
embs TyConMap
tyi Located DataConP
ldcp
  | Bool
mismatchFlds      = forall a e. Exception e => e -> a
Ex.throw (Doc -> UserError
err Doc
"fields") -- (err $  "fields:" <+> F.pprint (length dts) <+> " vs " <+> F.pprint ( dcArgs))
  | Bool
mismatchTyVars    = forall a e. Exception e => e -> a
Ex.throw (Doc -> UserError
err Doc
"type variables")
  | Bool
otherwise         = forall l b. Loc l => l -> b -> Located b
F.atLoc Located DataConP
ldcp forall a b. (a -> b) -> a -> b
$ forall a. PPrint a => String -> a -> a
F.notracepp String
"makePluggedDataCon" forall a b. (a -> b) -> a -> b
$ DataConP
dcp
                          { dcpFreeTyVars :: [RTyVar]
dcpFreeTyVars = [RTyVar]
dcVars
                          , dcpTyArgs :: [(Symbol, SpecType)]
dcpTyArgs     = forall a. [a] -> [a]
reverse [(Symbol, SpecType)]
tArgs
                          , dcpTyRes :: SpecType
dcpTyRes      = SpecType
tRes
                          }
  where
    ([(Symbol, SpecType)]
tArgs, SpecType
tRes)     = Bool
-> TCEmb TyCon
-> TyConMap
-> Located DataConP
-> ([Var], [Type], Type)
-> ([RTyVar], [(Symbol, SpecType)], SpecType)
-> ([(Symbol, SpecType)], SpecType)
plugMany Bool
allowTC  TCEmb TyCon
embs TyConMap
tyi Located DataConP
ldcp ([Var]
das, [Type]
dts, Type
dt) ([RTyVar]
dcVars, [(Symbol, SpecType)]
dcArgs, DataConP -> SpecType
dcpTyRes DataConP
dcp)
    ([Var]
das, [Type]
_, [Type]
dts, Type
dt) = {- F.notracepp ("makePluggedDC: " ++ F.showpp dc) $ -} DataCon -> ([Var], [Type], [Type], Type)
Ghc.dataConSig DataCon
dc
    dcArgs :: [(Symbol, SpecType)]
dcArgs            = forall a. [a] -> [a]
reverse forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. (if Bool
allowTC then forall c t t1. TyConable c => RType c t t1 -> Bool
isEmbeddedClass else forall c t t1. TyConable c => RType c t t1 -> Bool
isClassType) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) (DataConP -> [(Symbol, SpecType)]
dcpTyArgs DataConP
dcp)
    dcVars :: [RTyVar]
dcVars            = if Bool
isGADT
                          then [RTyVar] -> [RTyVar]
padGADVars forall a b. (a -> b) -> a -> b
$ forall a. Eq a => [a] -> [a]
L.nub (DataConP -> [RTyVar]
dcpFreeTyVars DataConP
dcp forall a. [a] -> [a] -> [a]
++ forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (forall a b. (a -> b) -> [a] -> [b]
map forall tv s. RTVar tv s -> tv
ty_var_value forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall tv c r. Eq tv => RType c tv r -> [RTVar tv (RType c tv ())]
freeTyVars) (DataConP -> SpecType
dcpTyRes DataConP
dcpforall a. a -> [a] -> [a]
:(forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, SpecType)]
dcArgs)))
                          else DataConP -> [RTyVar]
dcpFreeTyVars DataConP
dcp
    dc :: DataCon
dc                = DataConP -> DataCon
dcpCon        DataConP
dcp
    dcp :: DataConP
dcp               = forall a. Located a -> a
val           Located DataConP
ldcp

    isGADT :: Bool
isGADT            = TyCon -> Bool
Ghc.isGadtSyntaxTyCon forall a b. (a -> b) -> a -> b
$ DataCon -> TyCon
Ghc.dataConTyCon DataCon
dc

    -- hack to match LH and GHC GADT vars, since it is unclear how ghc generates free vars
    padGADVars :: [RTyVar] -> [RTyVar]
padGADVars [RTyVar]
vs = (Var -> RTyVar
RTV forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Int -> [a] -> [a]
take (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Var]
das forall a. Num a => a -> a -> a
- forall (t :: * -> *) a. Foldable t => t a -> Int
length [RTyVar]
vs) [Var]
das) forall a. [a] -> [a] -> [a]
++ [RTyVar]
vs

    mismatchFlds :: Bool
mismatchFlds      = forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
dts forall a. Eq a => a -> a -> Bool
/= forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Symbol, SpecType)]
dcArgs
    mismatchTyVars :: Bool
mismatchTyVars    = forall (t :: * -> *) a. Foldable t => t a -> Int
length [Var]
das forall a. Eq a => a -> a -> Bool
/= forall (t :: * -> *) a. Foldable t => t a -> Int
length [RTyVar]
dcVars
    err :: Doc -> UserError
err Doc
things        = forall t. SrcSpan -> Doc -> Doc -> TError t
ErrBadData (forall a. Loc a => a -> SrcSpan
GM.fSrcSpan DataConP
dcp) (forall a. PPrint a => a -> Doc
pprint DataCon
dc) (Doc
"GHC and Liquid specifications have different numbers of" Doc -> Doc -> Doc
<+> Doc
things) :: UserError


-- | @plugMany@ is used to "simultaneously" plug several different types,
--   e.g. as arise in the fields of a data constructor. To do so we create
--   a single "function type" that is then passed into @plugHoles@.
--   We also pass in the type parameters as dummy arguments, because, e.g.
--   we want @plugMany@ on the two types
--
--      forall a. a -> a -> Bool
--      forall b. _ -> _ -> _
--
--   to return something like
--
--      forall b. b -> b -> Bool
--
--   and not, forall b. a -> a -> Bool.

plugMany :: Bool -> F.TCEmb Ghc.TyCon -> Bare.TyConMap
         -> Located DataConP
         -> ([Ghc.Var], [Ghc.Type],             Ghc.Type)   -- ^ hs type
         -> ([RTyVar] , [(F.Symbol, SpecType)], SpecType)   -- ^ lq type
         -> ([(F.Symbol, SpecType)], SpecType)              -- ^ plugged lq type
plugMany :: Bool
-> TCEmb TyCon
-> TyConMap
-> Located DataConP
-> ([Var], [Type], Type)
-> ([RTyVar], [(Symbol, SpecType)], SpecType)
-> ([(Symbol, SpecType)], SpecType)
plugMany Bool
allowTC TCEmb TyCon
embs TyConMap
tyi Located DataConP
ldcp ([Var]
hsAs, [Type]
hsArgs, Type
hsRes) ([RTyVar]
lqAs, [(Symbol, SpecType)]
lqArgs, SpecType
lqRes)
                     = forall a. PPrint a => String -> a -> a
F.notracepp String
msg (forall a. Int -> [a] -> [a]
drop Int
nTyVars (forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
xs [SpecType]
ts), SpecType
t)
  where
    (([Symbol]
xs,[RFInfo]
_,[SpecType]
ts,[UReft Reft]
_), SpecType
t) = forall t t1 a.
RType t t1 a
-> (([Symbol], [RFInfo], [RType t t1 a], [a]), RType t t1 a)
bkArrow (forall a. Located a -> a
val LocSpecType
pT)
    pT :: LocSpecType
pT               = forall a.
(NamedThing a, PPrint a, Show a) =>
Bool
-> PlugTV a
-> TCEmb TyCon
-> TyConMap
-> (SpecType -> UReft Reft -> UReft Reft)
-> Type
-> LocSpecType
-> LocSpecType
plugHoles Bool
allowTC (forall v. v -> PlugTV v
Bare.LqTV Name
dcName) TCEmb TyCon
embs TyConMap
tyi (forall a b. a -> b -> a
const UReft Reft -> UReft Reft
killHoles) Type
hsT (forall l b. Loc l => l -> b -> Located b
F.atLoc Located DataConP
ldcp SpecType
lqT)
    hsT :: Type
hsT              = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (AnonArgFlag -> Type -> Type -> Type -> Type
Ghc.mkFunTy AnonArgFlag
Ghc.VisArg Type
Ghc.Many) Type
hsRes [Type]
hsArgs'
    lqT :: SpecType
lqT              = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (forall r c tv.
Monoid r =>
RFInfo -> Symbol -> RType c tv r -> RType c tv r -> RType c tv r
rFun' (Bool -> RFInfo
classRFInfo Bool
allowTC))) SpecType
lqRes [(Symbol, SpecType)]
lqArgs'
    hsArgs' :: [Type]
hsArgs'          = [ Var -> Type
Ghc.mkTyVarTy Var
a               | Var
a <- [Var]
hsAs] forall a. [a] -> [a] -> [a]
++ [Type]
hsArgs
    lqArgs' :: [(Symbol, SpecType)]
lqArgs'          = [(Symbol
F.dummySymbol, forall c tv r. tv -> r -> RType c tv r
RVar RTyVar
a forall a. Monoid a => a
mempty) | RTyVar
a <- [RTyVar]
lqAs] forall a. [a] -> [a] -> [a]
++ [(Symbol, SpecType)]
lqArgs
    nTyVars :: Int
nTyVars          = forall (t :: * -> *) a. Foldable t => t a -> Int
length [Var]
hsAs -- == length lqAs
    dcName :: Name
dcName           = DataCon -> Name
Ghc.dataConName forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataConP -> DataCon
dcpCon forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Located a -> a
val forall a b. (a -> b) -> a -> b
$ Located DataConP
ldcp
    msg :: String
msg              = String
"plugMany: " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> String
F.showpp (Name
dcName, Type
hsT, SpecType
lqT)

plugHolesOld, plugHolesNew
  :: (Ghc.NamedThing a, PPrint a, Show a)
  => Bool
  -> F.TCEmb Ghc.TyCon
  -> Bare.TyConMap
  -> a
  -> (SpecType -> RReft -> RReft)
  -> Ghc.Type
  -> LocSpecType
  -> LocSpecType

-- NOTE: this use of toType is safe as rt' is derived from t.
plugHolesOld :: forall a.
(NamedThing a, PPrint a, Show a) =>
Bool
-> TCEmb TyCon
-> TyConMap
-> a
-> (SpecType -> UReft Reft -> UReft Reft)
-> Type
-> LocSpecType
-> LocSpecType
plugHolesOld Bool
allowTC TCEmb TyCon
tce TyConMap
tyi a
xx SpecType -> UReft Reft -> UReft Reft
f Type
t0 zz :: LocSpecType
zz@(Loc SourcePos
l SourcePos
l' SpecType
st0)
    = forall a. SourcePos -> SourcePos -> a -> Located a
Loc SourcePos
l SourcePos
l'
    forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall tv c r.
[(RTVar tv (RType c tv ()), r)]
-> [PVar (RType c tv ())]
-> [(Symbol, RFInfo, RType c tv r, r)]
-> RType c tv r
-> RType c tv r
mkArrow (forall a b. [a] -> [b] -> [(a, b)]
zip (forall r i.
Monoid r =>
RTVar RTyVar i -> RTVar RTyVar (RType RTyCon RTyVar r)
updateRTVar forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RTVar RTyVar (RType RTyCon RTyVar ())]
αs') [UReft Reft]
rs) [PVar (RType RTyCon RTyVar ())]
ps' []
    forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {t :: * -> *} {r} {c} {tv}.
(Foldable t, Monoid r) =>
t (Symbol, RType c tv r) -> RType c tv r -> RType c tv r
makeCls [(Symbol, SpecType)]
cs'
    forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCEmb TyCon
-> TyConMap
-> (Doc -> Doc -> Error)
-> (SpecType -> UReft Reft -> UReft Reft)
-> SpecType
-> SpecType
-> SpecType
goPlug TCEmb TyCon
tce TyConMap
tyi forall {t}. Doc -> Doc -> TError t
err SpecType -> UReft Reft -> UReft Reft
f (forall tv ty c. SubsTy tv ty c => [(tv, ty)] -> c -> c
subts [(RTyVar, RTyVar)]
su SpecType
rt)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall c tv.
(Symbol -> Expr -> Expr)
-> RType c tv (UReft Reft) -> RType c tv (UReft Reft)
mapExprReft (\Symbol
_ -> CoSub -> Expr -> Expr
F.applyCoSub CoSub
coSub)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall tv ty c. SubsTy tv ty c => [(tv, ty)] -> c -> c
subts [(RTyVar, RTyVar)]
su
    forall a b. (a -> b) -> a -> b
$ SpecType
st
  where
    tyvsmap :: [(Var, RTyVar)]
tyvsmap      = case Bool
-> Type
-> SpecType
-> (Doc -> Doc -> Error)
-> Either Error MapTyVarST
Bare.runMapTyVars Bool
allowTC (forall r. ToTypeable r => Bool -> RRType r -> Type
toType Bool
False SpecType
rt) SpecType
st forall {t}. Doc -> Doc -> TError t
err of
                          Left Error
e  -> forall a e. Exception e => e -> a
Ex.throw Error
e
                          Right MapTyVarST
s -> MapTyVarST -> [(Var, RTyVar)]
Bare.vmap MapTyVarST
s
    su :: [(RTyVar, RTyVar)]
su           = [(RTyVar
y, Var -> RTyVar
rTyVar Var
x)           | (Var
x, RTyVar
y) <- [(Var, RTyVar)]
tyvsmap]
    su' :: [(RTyVar, RType RTyCon RTyVar ())]
su'          = [(RTyVar
y, forall c tv r. tv -> r -> RType c tv r
RVar (Var -> RTyVar
rTyVar Var
x) ()) | (Var
x, RTyVar
y) <- [(Var, RTyVar)]
tyvsmap] :: [(RTyVar, RSort)]
    coSub :: CoSub
coSub        = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [(forall a. Symbolic a => a -> Symbol
F.symbol RTyVar
y, Symbol -> Sort
F.FObj (forall a. Symbolic a => a -> Symbol
F.symbol RTyVar
x)) | (RTyVar
y, RTyVar
x) <- [(RTyVar, RTyVar)]
su]
    ps' :: [PVar (RType RTyCon RTyVar ())]
ps'          = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall tv ty c. SubsTy tv ty c => [(tv, ty)] -> c -> c
subts [(RTyVar, RType RTyCon RTyVar ())]
su') forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [PVar (RType RTyCon RTyVar ())]
ps
    cs' :: [(Symbol, SpecType)]
cs'          = [(Symbol
F.dummySymbol, forall c tv r.
c -> [RType c tv r] -> [RTProp c tv r] -> r -> RType c tv r
RApp RTyCon
c [SpecType]
ts [] forall a. Monoid a => a
mempty) | (RTyCon
c, [SpecType]
ts) <- [(RTyCon, [SpecType])]
cs2 ]
    ([RTVar RTyVar (RType RTyCon RTyVar ())]
αs', [UReft Reft]
rs)    = forall a b. [(a, b)] -> ([a], [b])
unzip [(RTVar RTyVar (RType RTyCon RTyVar ()), UReft Reft)]
αs
    ([(RTVar RTyVar (RType RTyCon RTyVar ()), UReft Reft)]
αs,[PVar (RType RTyCon RTyVar ())]
_,[(RTyCon, [SpecType])]
cs2,SpecType
rt) = SpecType
-> ([(RTVar RTyVar (RType RTyCon RTyVar ()), UReft Reft)],
    [PVar (RType RTyCon RTyVar ())], [(RTyCon, [SpecType])], SpecType)
bkUnivClass (forall a. PPrint a => String -> a -> a
F.notracepp String
"hs-spec" forall a b. (a -> b) -> a -> b
$ forall r. Monoid r => Type -> RRType r
ofType (Type -> Type
Ghc.expandTypeSynonyms Type
t0) :: SpecType)
    ([(RTVar RTyVar (RType RTyCon RTyVar ()), UReft Reft)]
_,[PVar (RType RTyCon RTyVar ())]
ps,[(RTyCon, [SpecType])]
_ ,SpecType
st) = SpecType
-> ([(RTVar RTyVar (RType RTyCon RTyVar ()), UReft Reft)],
    [PVar (RType RTyCon RTyVar ())], [(RTyCon, [SpecType])], SpecType)
bkUnivClass (forall a. PPrint a => String -> a -> a
F.notracepp String
"lq-spec" SpecType
st0)

    makeCls :: t (Symbol, RType c tv r) -> RType c tv r -> RType c tv r
makeCls t (Symbol, RType c tv r)
cs RType c tv r
t = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (forall r c tv.
Monoid r =>
RFInfo -> Symbol -> RType c tv r -> RType c tv r -> RType c tv r
rFun' (Bool -> RFInfo
classRFInfo Bool
allowTC))) RType c tv r
t t (Symbol, RType c tv r)
cs
    err :: Doc -> Doc -> TError t
err Doc
hsT Doc
lqT  = forall t.
SrcSpan
-> Doc
-> Doc
-> Doc
-> Doc
-> Maybe (Doc, Doc)
-> SrcSpan
-> TError t
ErrMismatch (forall a. Loc a => a -> SrcSpan
GM.fSrcSpan LocSpecType
zz) (forall a. PPrint a => a -> Doc
pprint a
xx)
                          (String -> Doc
text String
"Plugged Init types old")
                          (forall a. PPrint a => a -> Doc
pprint forall a b. (a -> b) -> a -> b
$ Type -> Type
Ghc.expandTypeSynonyms Type
t0)
                          (forall a. PPrint a => a -> Doc
pprint forall a b. (a -> b) -> a -> b
$ forall c tv r. RType c tv r -> RType c tv ()
toRSort SpecType
st0)
                          (forall a. a -> Maybe a
Just (Doc
hsT, Doc
lqT))
                          (forall a. NamedThing a => a -> SrcSpan
Ghc.getSrcSpan a
xx)



plugHolesNew :: forall a.
(NamedThing a, PPrint a, Show a) =>
Bool
-> TCEmb TyCon
-> TyConMap
-> a
-> (SpecType -> UReft Reft -> UReft Reft)
-> Type
-> LocSpecType
-> LocSpecType
plugHolesNew allowTC :: Bool
allowTC@Bool
False TCEmb TyCon
tce TyConMap
tyi a
xx SpecType -> UReft Reft -> UReft Reft
f Type
t0 zz :: LocSpecType
zz@(Loc SourcePos
l SourcePos
l' SpecType
st0)
    = forall a. SourcePos -> SourcePos -> a -> Located a
Loc SourcePos
l SourcePos
l'
    forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall tv c r.
[(RTVar tv (RType c tv ()), r)]
-> [PVar (RType c tv ())]
-> [(Symbol, RFInfo, RType c tv r, r)]
-> RType c tv r
-> RType c tv r
mkArrow (forall a b. [a] -> [b] -> [(a, b)]
zip (forall r i.
Monoid r =>
RTVar RTyVar i -> RTVar RTyVar (RType RTyCon RTyVar r)
updateRTVar forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RTVar RTyVar (RType RTyCon RTyVar ())]
as'') [UReft Reft]
rs) [PVar (RType RTyCon RTyVar ())]
ps []
    forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {t :: * -> *} {r} {c} {tv}.
(Foldable t, Monoid r) =>
t (Symbol, RType c tv r) -> RType c tv r -> RType c tv r
makeCls [(Symbol, SpecType)]
cs'
    forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCEmb TyCon
-> TyConMap
-> (Doc -> Doc -> Error)
-> (SpecType -> UReft Reft -> UReft Reft)
-> SpecType
-> SpecType
-> SpecType
goPlug TCEmb TyCon
tce TyConMap
tyi forall {t}. Doc -> Doc -> TError t
err SpecType -> UReft Reft -> UReft Reft
f SpecType
rt'
    forall a b. (a -> b) -> a -> b
$ SpecType
st
  where
    rt' :: SpecType
rt'          = SpecType -> SpecType
tx SpecType
rt
    as'' :: [RTVar RTyVar (RType RTyCon RTyVar ())]
as''         = [(RTyVar, RTyVar)]
-> RTVar RTyVar (RType RTyCon RTyVar ())
-> RTVar RTyVar (RType RTyCon RTyVar ())
subRTVar [(RTyVar, RTyVar)]
su forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RTVar RTyVar (RType RTyCon RTyVar ())]
as'
    ([RTVar RTyVar (RType RTyCon RTyVar ())]
as',[UReft Reft]
rs)     = forall a b. [(a, b)] -> ([a], [b])
unzip [(RTVar RTyVar (RType RTyCon RTyVar ()), UReft Reft)]
as
    cs' :: [(Symbol, SpecType)]
cs'          = [ (Symbol
F.dummySymbol, SpecType
ct) | (RTyCon
c, [SpecType]
t) <- [(RTyCon, [SpecType])]
tyCons, let ct :: SpecType
ct = SpecType -> SpecType
tx (forall c tv r.
c -> [RType c tv r] -> [RTProp c tv r] -> r -> RType c tv r
RApp RTyCon
c [SpecType]
t [] forall a. Monoid a => a
mempty) ]
    tx :: SpecType -> SpecType
tx           = forall tv ty c. SubsTy tv ty c => [(tv, ty)] -> c -> c
subts [(RTyVar, RTyVar)]
su
    su :: [(RTyVar, RTyVar)]
su           = case Bool
-> Type
-> SpecType
-> (Doc -> Doc -> Error)
-> Either Error MapTyVarST
Bare.runMapTyVars Bool
allowTC (forall r. ToTypeable r => Bool -> RRType r -> Type
toType Bool
False SpecType
rt) SpecType
st forall {t}. Doc -> Doc -> TError t
err of
                          Left Error
e  -> forall a e. Exception e => e -> a
Ex.throw Error
e
                          Right MapTyVarST
s -> [ (Var -> RTyVar
rTyVar Var
x, RTyVar
y) | (Var
x, RTyVar
y) <- MapTyVarST -> [(Var, RTyVar)]
Bare.vmap MapTyVarST
s]
    ([(RTVar RTyVar (RType RTyCon RTyVar ()), UReft Reft)]
as,[PVar (RType RTyCon RTyVar ())]
_,[(RTyCon, [SpecType])]
tyCons,SpecType
rt) = SpecType
-> ([(RTVar RTyVar (RType RTyCon RTyVar ()), UReft Reft)],
    [PVar (RType RTyCon RTyVar ())], [(RTyCon, [SpecType])], SpecType)
bkUnivClass (forall r. Monoid r => Type -> RRType r
ofType (Type -> Type
Ghc.expandTypeSynonyms Type
t0) :: SpecType)
    ([(RTVar RTyVar (RType RTyCon RTyVar ()), UReft Reft)]
_,[PVar (RType RTyCon RTyVar ())]
ps,[(RTyCon, [SpecType])]
_ ,SpecType
st) = SpecType
-> ([(RTVar RTyVar (RType RTyCon RTyVar ()), UReft Reft)],
    [PVar (RType RTyCon RTyVar ())], [(RTyCon, [SpecType])], SpecType)
bkUnivClass SpecType
st0

    makeCls :: t (Symbol, RType c tv r) -> RType c tv r -> RType c tv r
makeCls t (Symbol, RType c tv r)
cs RType c tv r
t = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (forall r c tv.
Monoid r =>
RFInfo -> Symbol -> RType c tv r -> RType c tv r -> RType c tv r
rFun' (Bool -> RFInfo
classRFInfo Bool
allowTC))) RType c tv r
t t (Symbol, RType c tv r)
cs
    err :: Doc -> Doc -> TError t
err Doc
hsT Doc
lqT  = forall t.
SrcSpan
-> Doc
-> Doc
-> Doc
-> Doc
-> Maybe (Doc, Doc)
-> SrcSpan
-> TError t
ErrMismatch (forall a. Loc a => a -> SrcSpan
GM.fSrcSpan LocSpecType
zz) (forall a. PPrint a => a -> Doc
pprint a
xx)
                          (String -> Doc
text String
"Plugged Init types new - TC disallowed")
                          (forall a. PPrint a => a -> Doc
pprint forall a b. (a -> b) -> a -> b
$ Type -> Type
Ghc.expandTypeSynonyms Type
t0)
                          (forall a. PPrint a => a -> Doc
pprint forall a b. (a -> b) -> a -> b
$ forall c tv r. RType c tv r -> RType c tv ()
toRSort SpecType
st0)
                          (forall a. a -> Maybe a
Just (Doc
hsT, Doc
lqT))
                          (forall a. NamedThing a => a -> SrcSpan
Ghc.getSrcSpan a
xx)


plugHolesNew allowTC :: Bool
allowTC@Bool
True TCEmb TyCon
tce TyConMap
tyi a
a SpecType -> UReft Reft -> UReft Reft
f Type
t0 zz :: LocSpecType
zz@(Loc SourcePos
l SourcePos
l' SpecType
st0)
    = forall a. SourcePos -> SourcePos -> a -> Located a
Loc SourcePos
l SourcePos
l'
    forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall tv c r.
[(RTVar tv (RType c tv ()), r)]
-> [PVar (RType c tv ())]
-> [(Symbol, RFInfo, RType c tv r, r)]
-> RType c tv r
-> RType c tv r
mkArrow (forall a b. [a] -> [b] -> [(a, b)]
zip (forall r i.
Monoid r =>
RTVar RTyVar i -> RTVar RTyVar (RType RTyCon RTyVar r)
updateRTVar forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RTVar RTyVar (RType RTyCon RTyVar ())]
as'') [UReft Reft]
rs) [PVar (RType RTyCon RTyVar ())]
ps (if forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Symbol, RFInfo, SpecType, UReft Reft)]
cs forall a. Ord a => a -> a -> Bool
> forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Symbol, RFInfo, SpecType, UReft Reft)]
cs' then [(Symbol, RFInfo, SpecType, UReft Reft)]
cs else [(Symbol, RFInfo, SpecType, UReft Reft)]
cs')
    -- . makeCls cs'
    forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCEmb TyCon
-> TyConMap
-> (Doc -> Doc -> Error)
-> (SpecType -> UReft Reft -> UReft Reft)
-> SpecType
-> SpecType
-> SpecType
goPlug TCEmb TyCon
tce TyConMap
tyi forall {t}. Doc -> Doc -> TError t
err SpecType -> UReft Reft -> UReft Reft
f SpecType
rt'
    forall a b. (a -> b) -> a -> b
$ SpecType
st
  where
    rt' :: SpecType
rt'          = SpecType -> SpecType
tx SpecType
rt
    as'' :: [RTVar RTyVar (RType RTyCon RTyVar ())]
as''         = [(RTyVar, RTyVar)]
-> RTVar RTyVar (RType RTyCon RTyVar ())
-> RTVar RTyVar (RType RTyCon RTyVar ())
subRTVar [(RTyVar, RTyVar)]
su forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RTVar RTyVar (RType RTyCon RTyVar ())]
as'
    ([RTVar RTyVar (RType RTyCon RTyVar ())]
as',[UReft Reft]
rs)     = forall a b. [(a, b)] -> ([a], [b])
unzip [(RTVar RTyVar (RType RTyCon RTyVar ()), UReft Reft)]
as
    -- cs'          = [ (F.dummySymbol, ct) | (c, t) <- cs, let ct = tx (RApp c t [] mempty) ]
    tx :: SpecType -> SpecType
tx           = forall tv ty c. SubsTy tv ty c => [(tv, ty)] -> c -> c
subts [(RTyVar, RTyVar)]
su
    su :: [(RTyVar, RTyVar)]
su           = case Bool
-> Type
-> SpecType
-> (Doc -> Doc -> Error)
-> Either Error MapTyVarST
Bare.runMapTyVars Bool
allowTC (forall r. ToTypeable r => Bool -> RRType r -> Type
toType Bool
False SpecType
rt) SpecType
st forall {t}. Doc -> Doc -> TError t
err of
                          Left Error
e  -> forall a e. Exception e => e -> a
Ex.throw Error
e
                          Right MapTyVarST
s -> [ (Var -> RTyVar
rTyVar Var
x, RTyVar
y) | (Var
x, RTyVar
y) <- MapTyVarST -> [(Var, RTyVar)]
Bare.vmap MapTyVarST
s]
    ([(RTVar RTyVar (RType RTyCon RTyVar ()), UReft Reft)]
as,[PVar (RType RTyCon RTyVar ())]
_,[(Symbol, SpecType, UReft Reft)]
cs0,SpecType
rt) = SpecType
-> ([(RTVar RTyVar (RType RTyCon RTyVar ()), UReft Reft)],
    [PVar (RType RTyCon RTyVar ())], [(Symbol, SpecType, UReft Reft)],
    SpecType)
bkUnivClass' (forall r. Monoid r => Type -> RRType r
ofType (Type -> Type
Ghc.expandTypeSynonyms Type
t0) :: SpecType)
    ([(RTVar RTyVar (RType RTyCon RTyVar ()), UReft Reft)]
_,[PVar (RType RTyCon RTyVar ())]
ps,[(Symbol, SpecType, UReft Reft)]
cs0' ,SpecType
st) = SpecType
-> ([(RTVar RTyVar (RType RTyCon RTyVar ()), UReft Reft)],
    [PVar (RType RTyCon RTyVar ())], [(Symbol, SpecType, UReft Reft)],
    SpecType)
bkUnivClass' SpecType
st0
    cs :: [(Symbol, RFInfo, SpecType, UReft Reft)]
cs  = [ (Symbol
x, Bool -> RFInfo
classRFInfo Bool
allowTC, SpecType
t, UReft Reft
r) | (Symbol
x,SpecType
t,UReft Reft
r)<-[(Symbol, SpecType, UReft Reft)]
cs0]
    cs' :: [(Symbol, RFInfo, SpecType, UReft Reft)]
cs' = [ (Symbol
x, Bool -> RFInfo
classRFInfo Bool
allowTC, SpecType
t, UReft Reft
r) | (Symbol
x,SpecType
t,UReft Reft
r)<-[(Symbol, SpecType, UReft Reft)]
cs0']

    err :: Doc -> Doc -> TError t
err Doc
hsT Doc
lqT  = forall t.
SrcSpan
-> Doc
-> Doc
-> Doc
-> Doc
-> Maybe (Doc, Doc)
-> SrcSpan
-> TError t
ErrMismatch (forall a. Loc a => a -> SrcSpan
GM.fSrcSpan LocSpecType
zz) (forall a. PPrint a => a -> Doc
pprint a
a)
                          (String -> Doc
text String
"Plugged Init types new - TC allowed")
                          (forall a. PPrint a => a -> Doc
pprint forall a b. (a -> b) -> a -> b
$ Type -> Type
Ghc.expandTypeSynonyms Type
t0)
                          (forall a. PPrint a => a -> Doc
pprint forall a b. (a -> b) -> a -> b
$ forall c tv r. RType c tv r -> RType c tv ()
toRSort SpecType
st0)
                          (forall a. a -> Maybe a
Just (Doc
hsT, Doc
lqT))
                          (forall a. NamedThing a => a -> SrcSpan
Ghc.getSrcSpan a
a)

subRTVar :: [(RTyVar, RTyVar)] -> SpecRTVar -> SpecRTVar
subRTVar :: [(RTyVar, RTyVar)]
-> RTVar RTyVar (RType RTyCon RTyVar ())
-> RTVar RTyVar (RType RTyCon RTyVar ())
subRTVar [(RTyVar, RTyVar)]
su a :: RTVar RTyVar (RType RTyCon RTyVar ())
a@(RTVar RTyVar
v RTVInfo (RType RTyCon RTyVar ())
i) = forall b a. b -> (a -> b) -> Maybe a -> b
Mb.maybe RTVar RTyVar (RType RTyCon RTyVar ())
a (forall tv s. tv -> RTVInfo s -> RTVar tv s
`RTVar` RTVInfo (RType RTyCon RTyVar ())
i) (forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup RTyVar
v [(RTyVar, RTyVar)]
su)

goPlug :: F.TCEmb Ghc.TyCon -> Bare.TyConMap -> (Doc -> Doc -> Error) -> (SpecType -> RReft -> RReft) -> SpecType -> SpecType
       -> SpecType
goPlug :: TCEmb TyCon
-> TyConMap
-> (Doc -> Doc -> Error)
-> (SpecType -> UReft Reft -> UReft Reft)
-> SpecType
-> SpecType
-> SpecType
goPlug TCEmb TyCon
tce TyConMap
tyi Doc -> Doc -> Error
err SpecType -> UReft Reft -> UReft Reft
f = SpecType -> SpecType -> SpecType
go
  where
    go :: SpecType -> SpecType -> SpecType
go SpecType
st (RHole UReft Reft
r) = (SpecType -> SpecType
addHoles SpecType
t') { rt_reft :: UReft Reft
rt_reft = SpecType -> UReft Reft -> UReft Reft
f SpecType
st UReft Reft
r }
      where
        t' :: SpecType
t'         = (forall a. Data a => a -> a) -> forall a. Data a => a -> a
everywhere (forall a b. (Typeable a, Typeable b) => (b -> b) -> a -> a
mkT forall a b. (a -> b) -> a -> b
$ TCEmb TyCon -> TyConMap -> SpecType -> SpecType
addRefs TCEmb TyCon
tce TyConMap
tyi) SpecType
st
        addHoles :: SpecType -> SpecType
addHoles   = (forall a. Data a => a -> a) -> forall a. Data a => a -> a
everywhere (forall a b. (Typeable a, Typeable b) => (b -> b) -> a -> a
mkT SpecType -> SpecType
addHole)
        -- NOTE: make sure we only add holes to RVar and RApp (NOT RFun)
        addHole :: SpecType -> SpecType
        addHole :: SpecType -> SpecType
addHole t :: SpecType
t@(RVar RTyVar
v UReft Reft
_)       = forall c tv r. tv -> r -> RType c tv r
RVar RTyVar
v (SpecType -> UReft Reft -> UReft Reft
f SpecType
t ((Symbol, Expr) -> UReft Reft
uReft (Symbol
"v", Expr
hole)))
        addHole t :: SpecType
t@(RApp RTyCon
c [SpecType]
ts [RTProp RTyCon RTyVar (UReft Reft)]
ps UReft Reft
_) = forall c tv r.
c -> [RType c tv r] -> [RTProp c tv r] -> r -> RType c tv r
RApp RTyCon
c [SpecType]
ts [RTProp RTyCon RTyVar (UReft Reft)]
ps (SpecType -> UReft Reft -> UReft Reft
f SpecType
t ((Symbol, Expr) -> UReft Reft
uReft (Symbol
"v", Expr
hole)))
        addHole SpecType
t                  = SpecType
t

    go (RVar RTyVar
_ UReft Reft
_)       v :: SpecType
v@(RVar RTyVar
_ UReft Reft
_)       = SpecType
v
    go (RFun Symbol
_ RFInfo
_ SpecType
i SpecType
o UReft Reft
_) (RFun Symbol
x RFInfo
ii SpecType
i' SpecType
o' UReft Reft
r)               = forall c tv r.
Symbol
-> RFInfo -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun Symbol
x RFInfo
ii    (SpecType -> SpecType -> SpecType
go SpecType
i SpecType
i')   (SpecType -> SpecType -> SpecType
go SpecType
o SpecType
o') UReft Reft
r
    go (RAllT RTVar RTyVar (RType RTyCon RTyVar ())
_ SpecType
t UReft Reft
_)    (RAllT RTVar RTyVar (RType RTyCon RTyVar ())
a SpecType
t' UReft Reft
r)     = forall c tv r. RTVU c tv -> RType c tv r -> r -> RType c tv r
RAllT RTVar RTyVar (RType RTyCon RTyVar ())
a    (SpecType -> SpecType -> SpecType
go SpecType
t SpecType
t') UReft Reft
r
    go (RAllT RTVar RTyVar (RType RTyCon RTyVar ())
a SpecType
t UReft Reft
r)    SpecType
t'                 = forall c tv r. RTVU c tv -> RType c tv r -> r -> RType c tv r
RAllT RTVar RTyVar (RType RTyCon RTyVar ())
a    (SpecType -> SpecType -> SpecType
go SpecType
t SpecType
t') UReft Reft
r
    go SpecType
t                (RAllP PVar (RType RTyCon RTyVar ())
p SpecType
t')       = forall c tv r. PVU c tv -> RType c tv r -> RType c tv r
RAllP PVar (RType RTyCon RTyVar ())
p    (SpecType -> SpecType -> SpecType
go SpecType
t SpecType
t')
    go SpecType
t                (RAllE Symbol
b SpecType
a SpecType
t')     = forall c tv r.
Symbol -> RType c tv r -> RType c tv r -> RType c tv r
RAllE Symbol
b SpecType
a  (SpecType -> SpecType -> SpecType
go SpecType
t SpecType
t')
    go SpecType
t                (REx Symbol
b SpecType
x SpecType
t')       = forall c tv r.
Symbol -> RType c tv r -> RType c tv r -> RType c tv r
REx Symbol
b SpecType
x    (SpecType -> SpecType -> SpecType
go SpecType
t SpecType
t')
    go SpecType
t                (RRTy [(Symbol, SpecType)]
e UReft Reft
r Oblig
o SpecType
t')    = forall c tv r.
[(Symbol, RType c tv r)]
-> r -> Oblig -> RType c tv r -> RType c tv r
RRTy [(Symbol, SpecType)]
e UReft Reft
r Oblig
o (SpecType -> SpecType -> SpecType
go SpecType
t SpecType
t')
    go (RAppTy SpecType
t1 SpecType
t2 UReft Reft
_) (RAppTy SpecType
t1' SpecType
t2' UReft Reft
r) = forall c tv r. RType c tv r -> RType c tv r -> r -> RType c tv r
RAppTy     (SpecType -> SpecType -> SpecType
go SpecType
t1 SpecType
t1') (SpecType -> SpecType -> SpecType
go SpecType
t2 SpecType
t2') UReft Reft
r
    -- zipWithDefM: if ts and ts' have different length then the liquid and haskell types are different.
    -- keep different types for now, as a pretty error message will be created at Bare.Check
    go (RApp RTyCon
_ [SpecType]
ts [RTProp RTyCon RTyVar (UReft Reft)]
_ UReft Reft
_)  (RApp RTyCon
c [SpecType]
ts' [RTProp RTyCon RTyVar (UReft Reft)]
p UReft Reft
r)
      | forall (t :: * -> *) a. Foldable t => t a -> Int
length [SpecType]
ts forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) a. Foldable t => t a -> Int
length [SpecType]
ts'            = forall c tv r.
c -> [RType c tv r] -> [RTProp c tv r] -> r -> RType c tv r
RApp RTyCon
c     (forall a. (a -> a -> a) -> [a] -> [a] -> [a]
Misc.zipWithDef SpecType -> SpecType -> SpecType
go [SpecType]
ts forall a b. (a -> b) -> a -> b
$ [SpecType] -> [SpecType] -> [SpecType]
Bare.matchKindArgs [SpecType]
ts [SpecType]
ts') [RTProp RTyCon RTyVar (UReft Reft)]
p UReft Reft
r
    go SpecType
hsT SpecType
lqT                             = forall a e. Exception e => e -> a
Ex.throw (Doc -> Doc -> Error
err (forall a. PPrint a => a -> Doc
F.pprint SpecType
hsT) (forall a. PPrint a => a -> Doc
F.pprint SpecType
lqT))

    -- otherwise                          = Ex.throw err
    -- If we reach the default case, there's probably an error, but we defer
    -- throwing it as checkGhcSpec does a much better job of reporting the
    -- problem to the user.
    -- go st               _                 = st

addRefs :: F.TCEmb Ghc.TyCon -> TyConMap -> SpecType -> SpecType
addRefs :: TCEmb TyCon -> TyConMap -> SpecType -> SpecType
addRefs TCEmb TyCon
tce TyConMap
tyi (RApp RTyCon
c [SpecType]
ts [RTProp RTyCon RTyVar (UReft Reft)]
_ UReft Reft
r) = forall c tv r.
c -> [RType c tv r] -> [RTProp c tv r] -> r -> RType c tv r
RApp RTyCon
c' [SpecType]
ts [RTProp RTyCon RTyVar (UReft Reft)]
ps UReft Reft
r
  where
    RApp RTyCon
c' [SpecType]
_ [RTProp RTyCon RTyVar (UReft Reft)]
ps UReft Reft
_ = forall r.
(PPrint r, Reftable r, SubsTy RTyVar (RType RTyCon RTyVar ()) r,
 Reftable (RTProp RTyCon RTyVar r)) =>
TCEmb TyCon -> TyConMap -> RRType r -> RRType r
addTyConInfo TCEmb TyCon
tce TyConMap
tyi (forall c tv r.
c -> [RType c tv r] -> [RTProp c tv r] -> r -> RType c tv r
RApp RTyCon
c [SpecType]
ts [] UReft Reft
r)
addRefs TCEmb TyCon
_ TyConMap
_ SpecType
t  = SpecType
t

maybeTrue :: Ghc.NamedThing a => a -> ModName -> S.HashSet StableName -> SpecType -> RReft -> RReft
maybeTrue :: forall a.
NamedThing a =>
a
-> ModName
-> HashSet StableName
-> SpecType
-> UReft Reft
-> UReft Reft
maybeTrue a
x ModName
target HashSet StableName
exports SpecType
t UReft Reft
r
  | Bool -> Bool
not (forall t t1 t2. RType t t1 t2 -> Bool
isFunTy SpecType
t) Bool -> Bool -> Bool
&& (Name -> Bool
Ghc.isInternalName Name
name Bool -> Bool -> Bool
|| Bool
inTarget Bool -> Bool -> Bool
&& Bool
notExported)
  = UReft Reft
r
  | Bool
otherwise
  = UReft Reft -> UReft Reft
killHoles UReft Reft
r
  where
    inTarget :: Bool
inTarget    = forall unit. GenModule unit -> ModuleName
Ghc.moduleName (HasDebugCallStack => Name -> Module
Ghc.nameModule Name
name) forall a. Eq a => a -> a -> Bool
== ModName -> ModuleName
getModName ModName
target
    name :: Name
name        = forall a. NamedThing a => a -> Name
Ghc.getName a
x
    notExported :: Bool
notExported = Bool -> Bool
not (Name -> StableName
mkStableName (forall a. NamedThing a => a -> Name
Ghc.getName a
x) forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`S.member` HashSet StableName
exports)

-- killHoles r@(U (Reft (v, rs)) _ _) = r { ur_reft = Reft (v, filter (not . isHole) rs) }

killHoles :: RReft -> RReft
killHoles :: UReft Reft -> UReft Reft
killHoles UReft Reft
ur = UReft Reft
ur { ur_reft :: Reft
ur_reft = Reft -> Reft
tx forall a b. (a -> b) -> a -> b
$ forall r. UReft r -> r
ur_reft UReft Reft
ur }
  where
    tx :: Reft -> Reft
tx Reft
r = {- traceFix ("killholes: r = " ++ showFix r) $ -} (Expr -> Expr) -> Reft -> Reft
F.mapPredReft Expr -> Expr
dropHoles Reft
r
    dropHoles :: Expr -> Expr
dropHoles    = ListNE Expr -> Expr
F.pAnd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Bool
isHole) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> ListNE Expr
F.conjuncts