{-# 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 qualified Data.Bifunctor as Bifunctor
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.DataDecl
import           Language.Haskell.Liquid.Types.Errors
import           Language.Haskell.Liquid.Types.Names
import           Language.Haskell.Liquid.Types.RefType
import           Language.Haskell.Liquid.Types.RType
import           Language.Haskell.Liquid.Types.RTypeOp
import           Language.Haskell.Liquid.Types.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           = PlugTV Var -> Maybe Var
forall v. PlugTV v -> Maybe v
Bare.plugSrc PlugTV Var
kx
    mkPlug :: Var -> LocSpecType
mkPlug Var
x      = Bool
-> PlugTV Var
-> TCEmb TyCon
-> TyConMap
-> (SpecType
    -> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
    -> UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> Type
-> LocSpecType
-> LocSpecType
forall a.
(NamedThing a, PPrint a, Show a) =>
Bool
-> PlugTV a
-> TCEmb TyCon
-> TyConMap
-> (SpecType
    -> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
    -> UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> Type
-> LocSpecType
-> LocSpecType
plugHoles Bool
allowTC PlugTV Var
kx TCEmb TyCon
embs TyConMap
tyi  SpecType
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r Type
τ LocSpecType
t
      where
        τ :: Type
τ         = Type -> Type
Ghc.expandTypeSynonyms (Var -> Type
Ghc.varType Var
x)
        r :: SpecType
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r         = Var
-> ModName
-> HashSet StableName
-> SpecType
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
forall a.
NamedThing a =>
a
-> ModName
-> HashSet StableName
-> SpecType
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
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
    -> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
    -> UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> Type
-> LocSpecType
-> LocSpecType
plugHoles Bool
allowTC (Bare.HsTV a
x) TCEmb TyCon
a TyConMap
b = Bool
-> TCEmb TyCon
-> TyConMap
-> a
-> (SpecType
    -> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
    -> UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> Type
-> LocSpecType
-> LocSpecType
forall a.
(NamedThing a, PPrint a, Show a) =>
Bool
-> TCEmb TyCon
-> TyConMap
-> a
-> (SpecType
    -> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
    -> UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> 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 = Bool
-> TCEmb TyCon
-> TyConMap
-> a
-> (SpecType
    -> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
    -> UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> Type
-> LocSpecType
-> LocSpecType
forall a.
(NamedThing a, PPrint a, Show a) =>
Bool
-> TCEmb TyCon
-> TyConMap
-> a
-> (SpecType
    -> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
    -> UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> Type
-> LocSpecType
-> LocSpecType
plugHolesNew Bool
allowTC TCEmb TyCon
a TyConMap
b a
x
plugHoles Bool
_ PlugTV a
_                   TCEmb TyCon
_ TyConMap
_ = \SpecType
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
_ 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      = TError Doc -> Located DataConP
forall a e. (HasCallStack, Exception e) => e -> a
Ex.throw (Doc -> TError Doc
err Doc
"fields") -- (err $  "fields:" <+> F.pprint (length dts) <+> " vs " <+> F.pprint ( dcArgs))
  | Bool
mismatchTyVars    = TError Doc -> Located DataConP
forall a e. (HasCallStack, Exception e) => e -> a
Ex.throw (Doc -> TError Doc
err Doc
"type variables")
  | Bool
otherwise         = Located DataConP -> DataConP -> Located DataConP
forall l b. Loc l => l -> b -> Located b
F.atLoc Located DataConP
ldcp (DataConP -> Located DataConP) -> DataConP -> Located DataConP
forall a b. (a -> b) -> a -> b
$ String -> DataConP -> DataConP
forall a. PPrint a => String -> a -> a
F.notracepp String
"makePluggedDataCon" (DataConP -> DataConP) -> DataConP -> DataConP
forall a b. (a -> b) -> a -> b
$ DataConP
dcp
                          { dcpFreeTyVars = dcVars
                          , dcpTyArgs     = reverse tArgs
                          , dcpTyRes      = tRes
                          }
  where
    ([(LHName, SpecType)]
tArgs, SpecType
tRes)     = Bool
-> TCEmb TyCon
-> TyConMap
-> Located DataConP
-> ([Var], [Type], Type)
-> ([RTyVar], [(LHName, SpecType)], SpecType)
-> ([(LHName, SpecType)], SpecType)
plugMany Bool
allowTC  TCEmb TyCon
embs TyConMap
tyi Located DataConP
ldcp ([Var]
das, [Type]
dts, Type
dt) ([RTyVar]
dcVars, [(LHName, 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 :: [(LHName, SpecType)]
dcArgs            = [(LHName, SpecType)] -> [(LHName, SpecType)]
forall a. [a] -> [a]
reverse ([(LHName, SpecType)] -> [(LHName, SpecType)])
-> [(LHName, SpecType)] -> [(LHName, SpecType)]
forall a b. (a -> b) -> a -> b
$ ((LHName, SpecType) -> Bool)
-> [(LHName, SpecType)] -> [(LHName, SpecType)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool)
-> ((LHName, SpecType) -> Bool) -> (LHName, SpecType) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (if Bool
allowTC then SpecType -> Bool
forall c v t t1. TyConable c => RTypeV v c t t1 -> Bool
isEmbeddedClass else SpecType -> Bool
forall c v t t1. TyConable c => RTypeV v c t t1 -> Bool
isClassType) (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) (DataConP -> [(LHName, SpecType)]
dcpTyArgs DataConP
dcp)
    dcVars :: [RTyVar]
dcVars            = if Bool
isGADT
                          then [RTyVar] -> [RTyVar]
padGADVars ([RTyVar] -> [RTyVar]) -> [RTyVar] -> [RTyVar]
forall a b. (a -> b) -> a -> b
$ [RTyVar] -> [RTyVar]
forall a. Eq a => [a] -> [a]
L.nub (DataConP -> [RTyVar]
dcpFreeTyVars DataConP
dcp [RTyVar] -> [RTyVar] -> [RTyVar]
forall a. [a] -> [a] -> [a]
++ (SpecType -> [RTyVar]) -> [SpecType] -> [RTyVar]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ((RTVar RTyVar (RTypeV Symbol RTyCon RTyVar NoReft) -> RTyVar)
-> [RTVar RTyVar (RTypeV Symbol RTyCon RTyVar NoReft)] -> [RTyVar]
forall a b. (a -> b) -> [a] -> [b]
map RTVar RTyVar (RTypeV Symbol RTyCon RTyVar NoReft) -> RTyVar
forall tv s. RTVar tv s -> tv
ty_var_value ([RTVar RTyVar (RTypeV Symbol RTyCon RTyVar NoReft)] -> [RTyVar])
-> (SpecType
    -> [RTVar RTyVar (RTypeV Symbol RTyCon RTyVar NoReft)])
-> SpecType
-> [RTyVar]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SpecType -> [RTVar RTyVar (RTypeV Symbol RTyCon RTyVar NoReft)]
forall tv v c r.
Eq tv =>
RTypeV v c tv r -> [RTVar tv (RTypeV v c tv NoReft)]
freeTyVars) (DataConP -> SpecType
dcpTyRes DataConP
dcpSpecType -> [SpecType] -> [SpecType]
forall a. a -> [a] -> [a]
:((LHName, SpecType) -> SpecType
forall a b. (a, b) -> b
snd ((LHName, SpecType) -> SpecType)
-> [(LHName, SpecType)] -> [SpecType]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(LHName, SpecType)]
dcArgs)))
                          else DataConP -> [RTyVar]
dcpFreeTyVars DataConP
dcp
    dc :: DataCon
dc                = DataConP -> DataCon
dcpCon        DataConP
dcp
    dcp :: DataConP
dcp               = Located DataConP -> DataConP
forall a. Located a -> a
val           Located DataConP
ldcp

    isGADT :: Bool
isGADT            = TyCon -> Bool
Ghc.isGadtSyntaxTyCon (TyCon -> Bool) -> TyCon -> Bool
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 (Var -> RTyVar) -> [Var] -> [RTyVar]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> [Var] -> [Var]
forall a. Int -> [a] -> [a]
take ([Var] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Var]
das 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]
vs) [Var]
das) [RTyVar] -> [RTyVar] -> [RTyVar]
forall a. [a] -> [a] -> [a]
++ [RTyVar]
vs

    mismatchFlds :: Bool
mismatchFlds      = [Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
dts Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= [(LHName, SpecType)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(LHName, SpecType)]
dcArgs
    mismatchTyVars :: Bool
mismatchTyVars    = [Var] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Var]
das Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= [RTyVar] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [RTyVar]
dcVars
    err :: Doc -> TError Doc
err Doc
things        = SrcSpan -> Doc -> Doc -> TError Doc
forall t. SrcSpan -> Doc -> Doc -> TError t
ErrBadData (DataConP -> SrcSpan
forall a. Loc a => a -> SrcSpan
GM.fSrcSpan DataConP
dcp) (DataCon -> Doc
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] , [(LHName, SpecType)], SpecType)   -- ^ lq type
         -> ([(LHName, SpecType)], SpecType)              -- ^ plugged lq type
plugMany :: Bool
-> TCEmb TyCon
-> TyConMap
-> Located DataConP
-> ([Var], [Type], Type)
-> ([RTyVar], [(LHName, SpecType)], SpecType)
-> ([(LHName, SpecType)], SpecType)
plugMany Bool
allowTC TCEmb TyCon
embs TyConMap
tyi Located DataConP
ldcp ([Var]
hsAs, [Type]
hsArgs, Type
hsRes) ([RTyVar]
lqAs, [(LHName, SpecType)]
lqArgs, SpecType
lqRes)
                     = String
-> ([(LHName, SpecType)], SpecType)
-> ([(LHName, SpecType)], SpecType)
forall a. PPrint a => String -> a -> a
F.notracepp String
msg (Int -> [(LHName, SpecType)] -> [(LHName, SpecType)]
forall a. Int -> [a] -> [a]
drop Int
nTyVars ([LHName] -> [SpecType] -> [(LHName, SpecType)]
forall a b. [a] -> [b] -> [(a, b)]
zip ((Symbol -> LHName) -> [Symbol] -> [LHName]
forall a b. (a -> b) -> [a] -> [b]
map Symbol -> LHName
lookupLHName [Symbol]
xs) [SpecType]
ts), SpecType
t)
  where
    lookupLHName :: Symbol -> LHName
lookupLHName Symbol
s   = LHName -> Maybe LHName -> LHName
forall a. a -> Maybe a -> a
Mb.fromMaybe (Maybe SrcSpan -> String -> LHName
forall a. HasCallStack => Maybe SrcSpan -> String -> a
panic (SrcSpan -> Maybe SrcSpan
forall a. a -> Maybe a
Just (Located DataConP -> SrcSpan
forall a. Loc a => a -> SrcSpan
GM.fSrcSpan Located DataConP
ldcp)) (String -> LHName) -> String -> LHName
forall a b. (a -> b) -> a -> b
$ String
"unexpected symbol: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Symbol -> String
forall a. Show a => a -> String
show Symbol
s) (Maybe LHName -> LHName) -> Maybe LHName -> LHName
forall a b. (a -> b) -> a -> b
$ Symbol -> [(Symbol, LHName)] -> Maybe LHName
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Symbol
s [(Symbol, LHName)]
lhNameMap
    lhNameMap :: [(Symbol, LHName)]
lhNameMap        = [ (HasCallStack => LHName -> Symbol
LHName -> Symbol
lhNameToUnqualifiedSymbol LHName
n, LHName
n) | LHName
n <- ((LHName, SpecType) -> LHName) -> [(LHName, SpecType)] -> [LHName]
forall a b. (a -> b) -> [a] -> [b]
map (LHName, SpecType) -> LHName
forall a b. (a, b) -> a
fst [(LHName, SpecType)]
lqArgs ]
    (([Symbol]
xs,[RFInfo]
_,[SpecType]
ts,[UReftBV Symbol Symbol (ReftBV Symbol Symbol)]
_), SpecType
t) = SpecType
-> (([Symbol], [RFInfo], [SpecType],
     [UReftBV Symbol Symbol (ReftBV Symbol Symbol)]),
    SpecType)
forall b v t t1 a.
RTypeBV b v t t1 a
-> (([b], [RFInfo], [RTypeBV b v t t1 a], [a]), RTypeBV b v t t1 a)
bkArrow (LocSpecType -> SpecType
forall a. Located a -> a
val LocSpecType
pT)
    pT :: LocSpecType
pT               = Bool
-> PlugTV Name
-> TCEmb TyCon
-> TyConMap
-> (SpecType
    -> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
    -> UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> Type
-> LocSpecType
-> LocSpecType
forall a.
(NamedThing a, PPrint a, Show a) =>
Bool
-> PlugTV a
-> TCEmb TyCon
-> TyConMap
-> (SpecType
    -> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
    -> UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> Type
-> LocSpecType
-> LocSpecType
plugHoles Bool
allowTC (Name -> PlugTV Name
forall v. v -> PlugTV v
Bare.LqTV Name
dcName) TCEmb TyCon
embs TyConMap
tyi ((UReftBV Symbol Symbol (ReftBV Symbol Symbol)
 -> UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> SpecType
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
forall a b. a -> b -> a
const UReftBV Symbol Symbol (ReftBV Symbol Symbol)
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
killHoles) Type
hsT (Located DataConP -> SpecType -> LocSpecType
forall l b. Loc l => l -> b -> Located b
F.atLoc Located DataConP
ldcp SpecType
lqT)
    hsT :: Type
hsT              = (Type -> Type -> Type) -> Type -> [Type] -> Type
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (HasDebugCallStack => FunTyFlag -> Type -> Type -> Type -> Type
FunTyFlag -> Type -> Type -> Type -> Type
Ghc.mkFunTy FunTyFlag
Ghc.FTF_T_T Type
Ghc.ManyTy) Type
hsRes [Type]
hsArgs'
    lqT :: SpecType
lqT              = ((Symbol, SpecType) -> SpecType -> SpecType)
-> SpecType -> [(Symbol, SpecType)] -> SpecType
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((Symbol -> SpecType -> SpecType -> SpecType)
-> (Symbol, SpecType) -> SpecType -> SpecType
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (RFInfo -> Symbol -> SpecType -> SpecType -> SpecType
forall r c tv.
IsReft 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] [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ [Type]
hsArgs
    lqArgs' :: [(Symbol, SpecType)]
lqArgs'          = [(Symbol
F.dummySymbol, RTyVar -> UReftBV Symbol Symbol (ReftBV Symbol Symbol) -> SpecType
forall b v c tv r. tv -> r -> RTypeBV b v c tv r
RVar RTyVar
a UReftBV Symbol Symbol (ReftBV Symbol Symbol)
forall a. Monoid a => a
mempty) | RTyVar
a <- [RTyVar]
lqAs] [(Symbol, SpecType)]
-> [(Symbol, SpecType)] -> [(Symbol, SpecType)]
forall a. [a] -> [a] -> [a]
++ ((LHName, SpecType) -> (Symbol, SpecType))
-> [(LHName, SpecType)] -> [(Symbol, SpecType)]
forall a b. (a -> b) -> [a] -> [b]
map ((LHName -> Symbol) -> (LHName, SpecType) -> (Symbol, SpecType)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
Bifunctor.first HasCallStack => LHName -> Symbol
LHName -> Symbol
lhNameToUnqualifiedSymbol) [(LHName, SpecType)]
lqArgs
    nTyVars :: Int
nTyVars          = [Var] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Var]
hsAs -- == length lqAs
    dcName :: Name
dcName           = DataCon -> Name
Ghc.dataConName (DataCon -> Name)
-> (Located DataConP -> DataCon) -> Located DataConP -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataConP -> DataCon
dcpCon (DataConP -> DataCon)
-> (Located DataConP -> DataConP) -> Located DataConP -> DataCon
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Located DataConP -> DataConP
forall a. Located a -> a
val (Located DataConP -> Name) -> Located DataConP -> Name
forall a b. (a -> b) -> a -> b
$ Located DataConP
ldcp
    msg :: String
msg              = String
"plugMany: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Name, Type, SpecType) -> String
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
    -> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
    -> UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> Type
-> LocSpecType
-> LocSpecType
plugHolesOld Bool
allowTC TCEmb TyCon
tce TyConMap
tyi a
xx SpecType
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
f Type
t0 zz :: LocSpecType
zz@(Loc SourcePos
l SourcePos
l' SpecType
st0)
    = SourcePos -> SourcePos -> SpecType -> LocSpecType
forall a. SourcePos -> SourcePos -> a -> Located a
Loc SourcePos
l SourcePos
l'
    (SpecType -> LocSpecType)
-> (SpecType -> SpecType) -> SpecType -> LocSpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(RTVar RTyVar (RTypeV Symbol RTyCon RTyVar NoReft),
  UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
-> [PVarBV Symbol Symbol (RTypeV Symbol 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 (RTypeV Symbol RTyCon RTyVar NoReft)]
-> [UReftBV Symbol Symbol (ReftBV Symbol Symbol)]
-> [(RTVar RTyVar (RTypeV Symbol RTyCon RTyVar NoReft),
     UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
forall a b. [a] -> [b] -> [(a, b)]
zip (RTVar RTyVar (RTypeV Symbol RTyCon RTyVar NoReft)
-> RTVar RTyVar (RTypeV Symbol RTyCon RTyVar NoReft)
forall r i.
IsReft r =>
RTVar RTyVar i -> RTVar RTyVar (RType RTyCon RTyVar r)
updateRTVar (RTVar RTyVar (RTypeV Symbol RTyCon RTyVar NoReft)
 -> RTVar RTyVar (RTypeV Symbol RTyCon RTyVar NoReft))
-> [RTVar RTyVar (RTypeV Symbol RTyCon RTyVar NoReft)]
-> [RTVar RTyVar (RTypeV Symbol RTyCon RTyVar NoReft)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RTVar RTyVar (RTypeV Symbol RTyCon RTyVar NoReft)]
αs') [UReftBV Symbol Symbol (ReftBV Symbol Symbol)]
rs) [PVarBV Symbol Symbol (RTypeV Symbol RTyCon RTyVar NoReft)]
ps' []
    (SpecType -> SpecType)
-> (SpecType -> SpecType) -> SpecType -> SpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Symbol, SpecType)] -> SpecType -> SpecType
forall {t :: * -> *} {r} {c} {tv}.
(Foldable t, IsReft r) =>
t (Symbol, RTypeBV Symbol Symbol c tv r)
-> RTypeBV Symbol Symbol c tv r -> RTypeBV Symbol Symbol c tv r
makeCls [(Symbol, SpecType)]
cs'
    (SpecType -> SpecType)
-> (SpecType -> SpecType) -> SpecType -> SpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCEmb TyCon
-> TyConMap
-> (Doc -> Doc -> Error)
-> (SpecType
    -> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
    -> UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> SpecType
-> SpecType
-> SpecType
goPlug TCEmb TyCon
tce TyConMap
tyi Doc -> Doc -> Error
forall {t}. Doc -> Doc -> TError t
err SpecType
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
f ([(RTyVar, RTyVar)] -> SpecType -> SpecType
forall tv ty c. SubsTy tv ty c => [(tv, ty)] -> c -> c
subts [(RTyVar, RTyVar)]
su SpecType
rt)
    (SpecType -> SpecType)
-> (SpecType -> SpecType) -> SpecType -> SpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol -> ExprBV Symbol Symbol -> ExprBV Symbol Symbol)
-> SpecType -> SpecType
forall b v c tv.
(b -> ExprBV b v -> ExprBV b v)
-> RTypeBV b v c tv (RReftBV b v) -> RTypeBV b v c tv (RReftBV b v)
mapExprReft (\Symbol
_ -> CoSub -> ExprBV Symbol Symbol -> ExprBV Symbol Symbol
F.applyCoSub CoSub
coSub)
    (SpecType -> SpecType)
-> (SpecType -> SpecType) -> SpecType -> SpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(RTyVar, RTyVar)] -> SpecType -> SpecType
forall tv ty c. SubsTy tv ty c => [(tv, ty)] -> c -> c
subts [(RTyVar, RTyVar)]
su
    (SpecType -> LocSpecType) -> SpecType -> LocSpecType
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 (Bool -> SpecType -> Type
forall r. ToTypeable r => Bool -> RRType r -> Type
toType Bool
False SpecType
rt) SpecType
st Doc -> Doc -> Error
forall {t}. Doc -> Doc -> TError t
err of
                          Left Error
e  -> Error -> [(Var, RTyVar)]
forall a e. (HasCallStack, 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, RTypeV Symbol RTyCon RTyVar NoReft)]
su'          = [(RTyVar
y, RTyVar -> NoReft -> RTypeV Symbol RTyCon RTyVar NoReft
forall b v c tv r. tv -> r -> RTypeBV b v c tv r
RVar (Var -> RTyVar
rTyVar Var
x) NoReft
forall b. NoReftB b
NoReft) | (Var
x, RTyVar
y) <- [(Var, RTyVar)]
tyvsmap] :: [(RTyVar, RSort)]
    coSub :: CoSub
coSub        = [(Symbol, Sort)] -> CoSub
forall k v. Hashable k => [(k, v)] -> HashMap k v
M.fromList [(RTyVar -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol RTyVar
y, Symbol -> Sort
F.FObj (RTyVar -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol RTyVar
x)) | (RTyVar
y, RTyVar
x) <- [(RTyVar, RTyVar)]
su]
    ps' :: [PVarBV Symbol Symbol (RTypeV Symbol RTyCon RTyVar NoReft)]
ps'          = (RTypeV Symbol RTyCon RTyVar NoReft
 -> RTypeV Symbol RTyCon RTyVar NoReft)
-> PVarBV Symbol Symbol (RTypeV Symbol RTyCon RTyVar NoReft)
-> PVarBV Symbol Symbol (RTypeV Symbol RTyCon RTyVar NoReft)
forall a b.
(a -> b) -> PVarBV Symbol Symbol a -> PVarBV Symbol Symbol b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([(RTyVar, RTypeV Symbol RTyCon RTyVar NoReft)]
-> RTypeV Symbol RTyCon RTyVar NoReft
-> RTypeV Symbol RTyCon RTyVar NoReft
forall tv ty c. SubsTy tv ty c => [(tv, ty)] -> c -> c
subts [(RTyVar, RTypeV Symbol RTyCon RTyVar NoReft)]
su') (PVarBV Symbol Symbol (RTypeV Symbol RTyCon RTyVar NoReft)
 -> PVarBV Symbol Symbol (RTypeV Symbol RTyCon RTyVar NoReft))
-> [PVarBV Symbol Symbol (RTypeV Symbol RTyCon RTyVar NoReft)]
-> [PVarBV Symbol Symbol (RTypeV Symbol RTyCon RTyVar NoReft)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [PVarBV Symbol Symbol (RTypeV Symbol RTyCon RTyVar NoReft)]
ps
    cs' :: [(Symbol, SpecType)]
cs'          = [(Symbol
F.dummySymbol, RTyCon
-> [SpecType]
-> [RTProp
      RTyCon RTyVar (UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
-> SpecType
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 RTyCon
c [SpecType]
ts [] UReftBV Symbol Symbol (ReftBV Symbol Symbol)
forall a. Monoid a => a
mempty) | (RTyCon
c, [SpecType]
ts) <- [(RTyCon, [SpecType])]
cs2 ]
    ([RTVar RTyVar (RTypeV Symbol RTyCon RTyVar NoReft)]
αs', [UReftBV Symbol Symbol (ReftBV Symbol Symbol)]
rs)    = [(RTVar RTyVar (RTypeV Symbol RTyCon RTyVar NoReft),
  UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
-> ([RTVar RTyVar (RTypeV Symbol RTyCon RTyVar NoReft)],
    [UReftBV Symbol Symbol (ReftBV Symbol Symbol)])
forall a b. [(a, b)] -> ([a], [b])
unzip [(RTVar RTyVar (RTypeV Symbol RTyCon RTyVar NoReft),
  UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
αs
    ([(RTVar RTyVar (RTypeV Symbol RTyCon RTyVar NoReft),
  UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
αs,[PVarBV Symbol Symbol (RTypeV Symbol RTyCon RTyVar NoReft)]
_,[(RTyCon, [SpecType])]
cs2,SpecType
rt) = SpecType
-> ([(RTVar RTyVar (RTypeV Symbol RTyCon RTyVar NoReft),
      UReftBV Symbol Symbol (ReftBV Symbol Symbol))],
    [PVarBV Symbol Symbol (RTypeV Symbol RTyCon RTyVar NoReft)],
    [(RTyCon, [SpecType])], SpecType)
bkUnivClass (String -> SpecType -> SpecType
forall a. PPrint a => String -> a -> a
F.notracepp String
"hs-spec" (SpecType -> SpecType) -> SpecType -> SpecType
forall a b. (a -> b) -> a -> b
$ Type -> SpecType
forall r. IsReft r => Type -> RRType r
ofType (Type -> Type
Ghc.expandTypeSynonyms Type
t0) :: SpecType)
    ([(RTVar RTyVar (RTypeV Symbol RTyCon RTyVar NoReft),
  UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
_,[PVarBV Symbol Symbol (RTypeV Symbol RTyCon RTyVar NoReft)]
ps,[(RTyCon, [SpecType])]
_ ,SpecType
st) = SpecType
-> ([(RTVar RTyVar (RTypeV Symbol RTyCon RTyVar NoReft),
      UReftBV Symbol Symbol (ReftBV Symbol Symbol))],
    [PVarBV Symbol Symbol (RTypeV Symbol RTyCon RTyVar NoReft)],
    [(RTyCon, [SpecType])], SpecType)
bkUnivClass (String -> SpecType -> SpecType
forall a. PPrint a => String -> a -> a
F.notracepp String
"lq-spec" SpecType
st0)

    makeCls :: t (Symbol, RTypeBV Symbol Symbol c tv r)
-> RTypeBV Symbol Symbol c tv r -> RTypeBV Symbol Symbol c tv r
makeCls t (Symbol, RTypeBV Symbol Symbol c tv r)
cs RTypeBV Symbol Symbol c tv r
t = ((Symbol, RTypeBV Symbol Symbol c tv r)
 -> RTypeBV Symbol Symbol c tv r -> RTypeBV Symbol Symbol c tv r)
-> RTypeBV Symbol Symbol c tv r
-> t (Symbol, RTypeBV Symbol Symbol c tv r)
-> RTypeBV Symbol Symbol c tv r
forall a b. (a -> b -> b) -> b -> t a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((Symbol
 -> RTypeBV Symbol Symbol c tv r
 -> RTypeBV Symbol Symbol c tv r
 -> RTypeBV Symbol Symbol c tv r)
-> (Symbol, RTypeBV Symbol Symbol c tv r)
-> RTypeBV Symbol Symbol c tv r
-> RTypeBV Symbol Symbol c tv r
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (RFInfo
-> Symbol
-> RTypeBV Symbol Symbol c tv r
-> RTypeBV Symbol Symbol c tv r
-> RTypeBV Symbol Symbol c tv r
forall r c tv.
IsReft r =>
RFInfo -> Symbol -> RType c tv r -> RType c tv r -> RType c tv r
rFun' (Bool -> RFInfo
classRFInfo Bool
allowTC))) RTypeBV Symbol Symbol c tv r
t t (Symbol, RTypeBV Symbol Symbol c tv r)
cs
    err :: Doc -> Doc -> TError t
err Doc
hsT Doc
lqT  = SrcSpan
-> Doc
-> Doc
-> Doc
-> Doc
-> Maybe (Doc, Doc)
-> SrcSpan
-> TError t
forall t.
SrcSpan
-> Doc
-> Doc
-> Doc
-> Doc
-> Maybe (Doc, Doc)
-> SrcSpan
-> TError t
ErrMismatch (LocSpecType -> SrcSpan
forall a. Loc a => a -> SrcSpan
GM.fSrcSpan LocSpecType
zz) (a -> Doc
forall a. PPrint a => a -> Doc
pprint a
xx)
                          (String -> Doc
text String
"Plugged Init types old")
                          (Type -> Doc
forall a. PPrint a => a -> Doc
pprint (Type -> Doc) -> Type -> Doc
forall a b. (a -> b) -> a -> b
$ Type -> Type
Ghc.expandTypeSynonyms Type
t0)
                          (RTypeV Symbol RTyCon RTyVar NoReft -> Doc
forall a. PPrint a => a -> Doc
pprint (RTypeV Symbol RTyCon RTyVar NoReft -> Doc)
-> RTypeV Symbol RTyCon RTyVar NoReft -> Doc
forall a b. (a -> b) -> a -> b
$ SpecType -> RTypeV Symbol RTyCon RTyVar NoReft
forall b v c tv r.
Binder b =>
RTypeBV b v c tv r -> RTypeBV b v c tv (NoReftB b)
toRSort SpecType
st0)
                          ((Doc, Doc) -> Maybe (Doc, Doc)
forall a. a -> Maybe a
Just (Doc
hsT, Doc
lqT))
                          (a -> SrcSpan
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
    -> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
    -> UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> Type
-> LocSpecType
-> LocSpecType
plugHolesNew allowTC :: Bool
allowTC@Bool
False TCEmb TyCon
tce TyConMap
tyi a
xx SpecType
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
f Type
t0 zz :: LocSpecType
zz@(Loc SourcePos
l SourcePos
l' SpecType
st0)
    = SourcePos -> SourcePos -> SpecType -> LocSpecType
forall a. SourcePos -> SourcePos -> a -> Located a
Loc SourcePos
l SourcePos
l'
    (SpecType -> LocSpecType)
-> (SpecType -> SpecType) -> SpecType -> LocSpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(RTVar RTyVar (RTypeV Symbol RTyCon RTyVar NoReft),
  UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
-> [PVarBV Symbol Symbol (RTypeV Symbol 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 (RTypeV Symbol RTyCon RTyVar NoReft)]
-> [UReftBV Symbol Symbol (ReftBV Symbol Symbol)]
-> [(RTVar RTyVar (RTypeV Symbol RTyCon RTyVar NoReft),
     UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
forall a b. [a] -> [b] -> [(a, b)]
zip (RTVar RTyVar (RTypeV Symbol RTyCon RTyVar NoReft)
-> RTVar RTyVar (RTypeV Symbol RTyCon RTyVar NoReft)
forall r i.
IsReft r =>
RTVar RTyVar i -> RTVar RTyVar (RType RTyCon RTyVar r)
updateRTVar (RTVar RTyVar (RTypeV Symbol RTyCon RTyVar NoReft)
 -> RTVar RTyVar (RTypeV Symbol RTyCon RTyVar NoReft))
-> [RTVar RTyVar (RTypeV Symbol RTyCon RTyVar NoReft)]
-> [RTVar RTyVar (RTypeV Symbol RTyCon RTyVar NoReft)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RTVar RTyVar (RTypeV Symbol RTyCon RTyVar NoReft)]
as'') [UReftBV Symbol Symbol (ReftBV Symbol Symbol)]
rs) [PVarBV Symbol Symbol (RTypeV Symbol RTyCon RTyVar NoReft)]
ps []
    (SpecType -> SpecType)
-> (SpecType -> SpecType) -> SpecType -> SpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Symbol, SpecType)] -> SpecType -> SpecType
forall {t :: * -> *} {r} {c} {tv}.
(Foldable t, IsReft r) =>
t (Symbol, RTypeBV Symbol Symbol c tv r)
-> RTypeBV Symbol Symbol c tv r -> RTypeBV Symbol Symbol c tv r
makeCls [(Symbol, SpecType)]
cs'
    (SpecType -> SpecType)
-> (SpecType -> SpecType) -> SpecType -> SpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCEmb TyCon
-> TyConMap
-> (Doc -> Doc -> Error)
-> (SpecType
    -> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
    -> UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> SpecType
-> SpecType
-> SpecType
goPlug TCEmb TyCon
tce TyConMap
tyi Doc -> Doc -> Error
forall {t}. Doc -> Doc -> TError t
err SpecType
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
f SpecType
rt'
    (SpecType -> LocSpecType) -> SpecType -> LocSpecType
forall a b. (a -> b) -> a -> b
$ SpecType
st
  where
    rt' :: SpecType
rt'          = SpecType -> SpecType
tx SpecType
rt
    as'' :: [RTVar RTyVar (RTypeV Symbol RTyCon RTyVar NoReft)]
as''         = [(RTyVar, RTyVar)]
-> RTVar RTyVar (RTypeV Symbol RTyCon RTyVar NoReft)
-> RTVar RTyVar (RTypeV Symbol RTyCon RTyVar NoReft)
subRTVar [(RTyVar, RTyVar)]
su (RTVar RTyVar (RTypeV Symbol RTyCon RTyVar NoReft)
 -> RTVar RTyVar (RTypeV Symbol RTyCon RTyVar NoReft))
-> [RTVar RTyVar (RTypeV Symbol RTyCon RTyVar NoReft)]
-> [RTVar RTyVar (RTypeV Symbol RTyCon RTyVar NoReft)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RTVar RTyVar (RTypeV Symbol RTyCon RTyVar NoReft)]
as'
    ([RTVar RTyVar (RTypeV Symbol RTyCon RTyVar NoReft)]
as',[UReftBV Symbol Symbol (ReftBV Symbol Symbol)]
rs)     = [(RTVar RTyVar (RTypeV Symbol RTyCon RTyVar NoReft),
  UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
-> ([RTVar RTyVar (RTypeV Symbol RTyCon RTyVar NoReft)],
    [UReftBV Symbol Symbol (ReftBV Symbol Symbol)])
forall a b. [(a, b)] -> ([a], [b])
unzip [(RTVar RTyVar (RTypeV Symbol RTyCon RTyVar NoReft),
  UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
as
    cs' :: [(Symbol, SpecType)]
cs'          = [ (Symbol
F.dummySymbol, SpecType
ct) | (RTyCon
c, [SpecType]
t) <- [(RTyCon, [SpecType])]
tyCons, let ct :: SpecType
ct = SpecType -> SpecType
tx (RTyCon
-> [SpecType]
-> [RTProp
      RTyCon RTyVar (UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
-> SpecType
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 RTyCon
c [SpecType]
t [] UReftBV Symbol Symbol (ReftBV Symbol Symbol)
forall a. Monoid a => a
mempty) ]
    tx :: SpecType -> SpecType
tx           = [(RTyVar, RTyVar)] -> SpecType -> SpecType
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 (Bool -> SpecType -> Type
forall r. ToTypeable r => Bool -> RRType r -> Type
toType Bool
False SpecType
rt) SpecType
st Doc -> Doc -> Error
forall {t}. Doc -> Doc -> TError t
err of
                          Left Error
e  -> Error -> [(RTyVar, RTyVar)]
forall a e. (HasCallStack, 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 (RTypeV Symbol RTyCon RTyVar NoReft),
  UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
as,[PVarBV Symbol Symbol (RTypeV Symbol RTyCon RTyVar NoReft)]
_,[(RTyCon, [SpecType])]
tyCons,SpecType
rt) = SpecType
-> ([(RTVar RTyVar (RTypeV Symbol RTyCon RTyVar NoReft),
      UReftBV Symbol Symbol (ReftBV Symbol Symbol))],
    [PVarBV Symbol Symbol (RTypeV Symbol RTyCon RTyVar NoReft)],
    [(RTyCon, [SpecType])], SpecType)
bkUnivClass (Type -> SpecType
forall r. IsReft r => Type -> RRType r
ofType (Type -> Type
Ghc.expandTypeSynonyms Type
t0) :: SpecType)
    ([(RTVar RTyVar (RTypeV Symbol RTyCon RTyVar NoReft),
  UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
_,[PVarBV Symbol Symbol (RTypeV Symbol RTyCon RTyVar NoReft)]
ps,[(RTyCon, [SpecType])]
_ ,SpecType
st) = SpecType
-> ([(RTVar RTyVar (RTypeV Symbol RTyCon RTyVar NoReft),
      UReftBV Symbol Symbol (ReftBV Symbol Symbol))],
    [PVarBV Symbol Symbol (RTypeV Symbol RTyCon RTyVar NoReft)],
    [(RTyCon, [SpecType])], SpecType)
bkUnivClass SpecType
st0

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


plugHolesNew allowTC :: Bool
allowTC@Bool
True TCEmb TyCon
tce TyConMap
tyi a
a SpecType
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
f Type
t0 zz :: LocSpecType
zz@(Loc SourcePos
l SourcePos
l' SpecType
st0)
    = SourcePos -> SourcePos -> SpecType -> LocSpecType
forall a. SourcePos -> SourcePos -> a -> Located a
Loc SourcePos
l SourcePos
l'
    (SpecType -> LocSpecType)
-> (SpecType -> SpecType) -> SpecType -> LocSpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(RTVar RTyVar (RTypeV Symbol RTyCon RTyVar NoReft),
  UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
-> [PVarBV Symbol Symbol (RTypeV Symbol 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 (RTypeV Symbol RTyCon RTyVar NoReft)]
-> [UReftBV Symbol Symbol (ReftBV Symbol Symbol)]
-> [(RTVar RTyVar (RTypeV Symbol RTyCon RTyVar NoReft),
     UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
forall a b. [a] -> [b] -> [(a, b)]
zip (RTVar RTyVar (RTypeV Symbol RTyCon RTyVar NoReft)
-> RTVar RTyVar (RTypeV Symbol RTyCon RTyVar NoReft)
forall r i.
IsReft r =>
RTVar RTyVar i -> RTVar RTyVar (RType RTyCon RTyVar r)
updateRTVar (RTVar RTyVar (RTypeV Symbol RTyCon RTyVar NoReft)
 -> RTVar RTyVar (RTypeV Symbol RTyCon RTyVar NoReft))
-> [RTVar RTyVar (RTypeV Symbol RTyCon RTyVar NoReft)]
-> [RTVar RTyVar (RTypeV Symbol RTyCon RTyVar NoReft)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RTVar RTyVar (RTypeV Symbol RTyCon RTyVar NoReft)]
as'') [UReftBV Symbol Symbol (ReftBV Symbol Symbol)]
rs) [PVarBV Symbol Symbol (RTypeV Symbol RTyCon RTyVar NoReft)]
ps (if [(Symbol, RFInfo, SpecType,
  UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
-> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Symbol, RFInfo, SpecType,
  UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
cs Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> [(Symbol, RFInfo, SpecType,
  UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
-> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Symbol, RFInfo, SpecType,
  UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
cs' then [(Symbol, RFInfo, SpecType,
  UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
cs else [(Symbol, RFInfo, SpecType,
  UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
cs')
    -- . makeCls cs'
    (SpecType -> SpecType)
-> (SpecType -> SpecType) -> SpecType -> SpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCEmb TyCon
-> TyConMap
-> (Doc -> Doc -> Error)
-> (SpecType
    -> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
    -> UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> SpecType
-> SpecType
-> SpecType
goPlug TCEmb TyCon
tce TyConMap
tyi Doc -> Doc -> Error
forall {t}. Doc -> Doc -> TError t
err SpecType
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
f SpecType
rt'
    (SpecType -> LocSpecType) -> SpecType -> LocSpecType
forall a b. (a -> b) -> a -> b
$ SpecType
st
  where
    rt' :: SpecType
rt'          = SpecType -> SpecType
tx SpecType
rt
    as'' :: [RTVar RTyVar (RTypeV Symbol RTyCon RTyVar NoReft)]
as''         = [(RTyVar, RTyVar)]
-> RTVar RTyVar (RTypeV Symbol RTyCon RTyVar NoReft)
-> RTVar RTyVar (RTypeV Symbol RTyCon RTyVar NoReft)
subRTVar [(RTyVar, RTyVar)]
su (RTVar RTyVar (RTypeV Symbol RTyCon RTyVar NoReft)
 -> RTVar RTyVar (RTypeV Symbol RTyCon RTyVar NoReft))
-> [RTVar RTyVar (RTypeV Symbol RTyCon RTyVar NoReft)]
-> [RTVar RTyVar (RTypeV Symbol RTyCon RTyVar NoReft)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RTVar RTyVar (RTypeV Symbol RTyCon RTyVar NoReft)]
as'
    ([RTVar RTyVar (RTypeV Symbol RTyCon RTyVar NoReft)]
as',[UReftBV Symbol Symbol (ReftBV Symbol Symbol)]
rs)     = [(RTVar RTyVar (RTypeV Symbol RTyCon RTyVar NoReft),
  UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
-> ([RTVar RTyVar (RTypeV Symbol RTyCon RTyVar NoReft)],
    [UReftBV Symbol Symbol (ReftBV Symbol Symbol)])
forall a b. [(a, b)] -> ([a], [b])
unzip [(RTVar RTyVar (RTypeV Symbol RTyCon RTyVar NoReft),
  UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
as
    -- cs'          = [ (F.dummySymbol, ct) | (c, t) <- cs, let ct = tx (RApp c t [] mempty) ]
    tx :: SpecType -> SpecType
tx           = [(RTyVar, RTyVar)] -> SpecType -> SpecType
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 (Bool -> SpecType -> Type
forall r. ToTypeable r => Bool -> RRType r -> Type
toType Bool
False SpecType
rt) SpecType
st Doc -> Doc -> Error
forall {t}. Doc -> Doc -> TError t
err of
                          Left Error
e  -> Error -> [(RTyVar, RTyVar)]
forall a e. (HasCallStack, 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 (RTypeV Symbol RTyCon RTyVar NoReft),
  UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
as,[PVarBV Symbol Symbol (RTypeV Symbol RTyCon RTyVar NoReft)]
_,[(Symbol, SpecType, UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
cs0,SpecType
rt) = SpecType
-> ([(RTVar RTyVar (RTypeV Symbol RTyCon RTyVar NoReft),
      UReftBV Symbol Symbol (ReftBV Symbol Symbol))],
    [PVarBV Symbol Symbol (RTypeV Symbol RTyCon RTyVar NoReft)],
    [(Symbol, SpecType, UReftBV Symbol Symbol (ReftBV Symbol Symbol))],
    SpecType)
bkUnivClass' (Type -> SpecType
forall r. IsReft r => Type -> RRType r
ofType (Type -> Type
Ghc.expandTypeSynonyms Type
t0) :: SpecType)
    ([(RTVar RTyVar (RTypeV Symbol RTyCon RTyVar NoReft),
  UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
_,[PVarBV Symbol Symbol (RTypeV Symbol RTyCon RTyVar NoReft)]
ps,[(Symbol, SpecType, UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
cs0' ,SpecType
st) = SpecType
-> ([(RTVar RTyVar (RTypeV Symbol RTyCon RTyVar NoReft),
      UReftBV Symbol Symbol (ReftBV Symbol Symbol))],
    [PVarBV Symbol Symbol (RTypeV Symbol RTyCon RTyVar NoReft)],
    [(Symbol, SpecType, UReftBV Symbol Symbol (ReftBV Symbol Symbol))],
    SpecType)
bkUnivClass' SpecType
st0
    cs :: [(Symbol, RFInfo, SpecType,
  UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
cs  = [ (Symbol
x, Bool -> RFInfo
classRFInfo Bool
allowTC, SpecType
t, UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r) | (Symbol
x,SpecType
t,UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r)<-[(Symbol, SpecType, UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
cs0]
    cs' :: [(Symbol, RFInfo, SpecType,
  UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
cs' = [ (Symbol
x, Bool -> RFInfo
classRFInfo Bool
allowTC, SpecType
t, UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r) | (Symbol
x,SpecType
t,UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r)<-[(Symbol, SpecType, UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
cs0']

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

subRTVar :: [(RTyVar, RTyVar)] -> SpecRTVar -> SpecRTVar
subRTVar :: [(RTyVar, RTyVar)]
-> RTVar RTyVar (RTypeV Symbol RTyCon RTyVar NoReft)
-> RTVar RTyVar (RTypeV Symbol RTyCon RTyVar NoReft)
subRTVar [(RTyVar, RTyVar)]
su a :: RTVar RTyVar (RTypeV Symbol RTyCon RTyVar NoReft)
a@(RTVar RTyVar
v RTVInfo (RTypeV Symbol RTyCon RTyVar NoReft)
i) = RTVar RTyVar (RTypeV Symbol RTyCon RTyVar NoReft)
-> (RTyVar -> RTVar RTyVar (RTypeV Symbol RTyCon RTyVar NoReft))
-> Maybe RTyVar
-> RTVar RTyVar (RTypeV Symbol RTyCon RTyVar NoReft)
forall b a. b -> (a -> b) -> Maybe a -> b
Mb.maybe RTVar RTyVar (RTypeV Symbol RTyCon RTyVar NoReft)
a (RTyVar
-> RTVInfo (RTypeV Symbol RTyCon RTyVar NoReft)
-> RTVar RTyVar (RTypeV Symbol RTyCon RTyVar NoReft)
forall tv s. tv -> RTVInfo s -> RTVar tv s
`RTVar` RTVInfo (RTypeV Symbol RTyCon RTyVar NoReft)
i) (RTyVar -> [(RTyVar, RTyVar)] -> Maybe RTyVar
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
    -> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
    -> UReftBV Symbol Symbol (ReftBV Symbol Symbol))
-> SpecType
-> SpecType
-> SpecType
goPlug TCEmb TyCon
tce TyConMap
tyi Doc -> Doc -> Error
err SpecType
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
f = SpecType -> SpecType -> SpecType
go
  where
    go :: SpecType -> SpecType -> SpecType
go SpecType
st (RHole UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r) = (SpecType -> SpecType
addHoles SpecType
t') { rt_reft = f st r }
      where
        t' :: SpecType
t'         = (forall a. Data a => a -> a) -> forall a. Data a => a -> a
everywhere ((SpecType -> SpecType) -> a -> a
forall a b. (Typeable a, Typeable b) => (b -> b) -> a -> a
mkT ((SpecType -> SpecType) -> a -> a)
-> (SpecType -> SpecType) -> a -> a
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 ((SpecType -> SpecType) -> a -> a
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 UReftBV Symbol Symbol (ReftBV Symbol Symbol)
_)       = RTyVar -> UReftBV Symbol Symbol (ReftBV Symbol Symbol) -> SpecType
forall b v c tv r. tv -> r -> RTypeBV b v c tv r
RVar RTyVar
v (SpecType
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
f SpecType
t ((Symbol, ExprBV Symbol Symbol)
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
uReft (Symbol
"v", ExprBV Symbol Symbol
forall v. ExprV v
hole)))
        addHole t :: SpecType
t@(RApp RTyCon
c [SpecType]
ts [RTProp
   RTyCon RTyVar (UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
ps UReftBV Symbol Symbol (ReftBV Symbol Symbol)
_) = RTyCon
-> [SpecType]
-> [RTProp
      RTyCon RTyVar (UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
-> SpecType
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 RTyCon
c [SpecType]
ts [RTProp
   RTyCon RTyVar (UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
ps (SpecType
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
f SpecType
t ((Symbol, ExprBV Symbol Symbol)
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
uReft (Symbol
"v", ExprBV Symbol Symbol
forall v. ExprV v
hole)))
        addHole SpecType
t                  = SpecType
t

    go (RVar RTyVar
_ UReftBV Symbol Symbol (ReftBV Symbol Symbol)
_)       v :: SpecType
v@(RVar RTyVar
_ UReftBV Symbol Symbol (ReftBV Symbol Symbol)
_)       = SpecType
v
    go (RFun Symbol
_ RFInfo
_ SpecType
i SpecType
o UReftBV Symbol Symbol (ReftBV Symbol Symbol)
_) (RFun Symbol
x RFInfo
ii SpecType
i' SpecType
o' UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r)               = 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
ii    (SpecType -> SpecType -> SpecType
go SpecType
i SpecType
i')   (SpecType -> SpecType -> SpecType
go SpecType
o SpecType
o') UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r
    go (RAllT RTVar RTyVar (RTypeV Symbol RTyCon RTyVar NoReft)
_ SpecType
t UReftBV Symbol Symbol (ReftBV Symbol Symbol)
_)    (RAllT RTVar RTyVar (RTypeV Symbol RTyCon RTyVar NoReft)
a SpecType
t' UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r)     = RTVar RTyVar (RTypeV Symbol 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 (RTypeV Symbol RTyCon RTyVar NoReft)
a    (SpecType -> SpecType -> SpecType
go SpecType
t SpecType
t') UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r
    go (RAllT RTVar RTyVar (RTypeV Symbol RTyCon RTyVar NoReft)
a SpecType
t UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r)    SpecType
t'                 = RTVar RTyVar (RTypeV Symbol 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 (RTypeV Symbol RTyCon RTyVar NoReft)
a    (SpecType -> SpecType -> SpecType
go SpecType
t SpecType
t') UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r
    go SpecType
t                (RAllP PVarBV Symbol Symbol (RTypeV Symbol RTyCon RTyVar NoReft)
p SpecType
t')       = PVarBV Symbol Symbol (RTypeV Symbol 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 (RTypeV Symbol RTyCon RTyVar NoReft)
p    (SpecType -> SpecType -> SpecType
go SpecType
t SpecType
t')
    go SpecType
t                (RAllE Symbol
b SpecType
a SpecType
t')     = Symbol -> SpecType -> SpecType -> SpecType
forall b v c tv r.
b -> RTypeBV b v c tv r -> RTypeBV b v c tv r -> RTypeBV b v 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')       = Symbol -> SpecType -> SpecType -> SpecType
forall b v c tv r.
b -> RTypeBV b v c tv r -> RTypeBV b v c tv r -> RTypeBV b v c tv r
REx Symbol
b SpecType
x    (SpecType -> SpecType -> SpecType
go SpecType
t SpecType
t')
    go SpecType
t                (RRTy [(Symbol, SpecType)]
e UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r Oblig
o SpecType
t')    = [(Symbol, SpecType)]
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
-> Oblig
-> SpecType
-> SpecType
forall b v c tv r.
[(b, RTypeBV b v c tv r)]
-> r -> Oblig -> RTypeBV b v c tv r -> RTypeBV b v c tv r
RRTy [(Symbol, SpecType)]
e UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r Oblig
o (SpecType -> SpecType -> SpecType
go SpecType
t SpecType
t')
    go (RAppTy SpecType
t1 SpecType
t2 UReftBV Symbol Symbol (ReftBV Symbol Symbol)
_) (RAppTy SpecType
t1' SpecType
t2' UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r) = SpecType
-> SpecType
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
-> SpecType
forall b v c tv r.
RTypeBV b v c tv r -> RTypeBV b v c tv r -> r -> RTypeBV b v c tv r
RAppTy     (SpecType -> SpecType -> SpecType
go SpecType
t1 SpecType
t1') (SpecType -> SpecType -> SpecType
go SpecType
t2 SpecType
t2') UReftBV Symbol Symbol (ReftBV Symbol Symbol)
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 (UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
_ UReftBV Symbol Symbol (ReftBV Symbol Symbol)
_)  (RApp RTyCon
c [SpecType]
ts' [RTProp
   RTyCon RTyVar (UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
p UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r)
    -- Removing length check because Haskell types can contain kinds which is safe based on the comment above
    --   | length ts == length ts'
      = RTyCon
-> [SpecType]
-> [RTProp
      RTyCon RTyVar (UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
-> SpecType
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 RTyCon
c     ((SpecType -> SpecType -> SpecType)
-> [SpecType] -> [SpecType] -> [SpecType]
forall a. (a -> a -> a) -> [a] -> [a] -> [a]
Misc.zipWithDef SpecType -> SpecType -> SpecType
go [SpecType]
ts ([SpecType] -> [SpecType]) -> [SpecType] -> [SpecType]
forall a b. (a -> b) -> a -> b
$ [SpecType] -> [SpecType] -> [SpecType]
Bare.matchKindArgs [SpecType]
ts [SpecType]
ts') [RTProp
   RTyCon RTyVar (UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
p UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r
    go SpecType
hsT SpecType
lqT                             = Error -> SpecType
forall a e. (HasCallStack, Exception e) => e -> a
Ex.throw (Doc -> Doc -> Error
err (SpecType -> Doc
forall a. PPrint a => a -> Doc
F.pprint SpecType
hsT) (SpecType -> Doc
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 (UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
_ UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r) = RTyCon
-> [SpecType]
-> [RTProp
      RTyCon RTyVar (UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
-> SpecType
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 RTyCon
c' [SpecType]
ts [RTProp
   RTyCon RTyVar (UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
ps UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r
  where
    RApp RTyCon
c' [SpecType]
_ [RTProp
   RTyCon RTyVar (UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
ps UReftBV Symbol Symbol (ReftBV Symbol Symbol)
_ = TCEmb TyCon -> TyConMap -> SpecType -> SpecType
forall r.
(PPrint r, ToReft r,
 SubsTy RTyVar (RTypeV Symbol RTyCon RTyVar NoReft) r,
 Variable r ~ Symbol, ReftBind r ~ Symbol, ReftVar r ~ Symbol,
 IsReft r) =>
TCEmb TyCon -> TyConMap -> RRType r -> RRType r
addTyConInfo TCEmb TyCon
tce TyConMap
tyi (RTyCon
-> [SpecType]
-> [RTProp
      RTyCon RTyVar (UReftBV Symbol Symbol (ReftBV Symbol Symbol))]
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
-> SpecType
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 RTyCon
c [SpecType]
ts [] UReftBV Symbol Symbol (ReftBV Symbol Symbol)
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
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
maybeTrue a
x ModName
target HashSet StableName
exports SpecType
t UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r
  | Bool -> Bool
not (SpecType -> Bool
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)
  = UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r
  | Bool
otherwise
  = UReftBV Symbol Symbol (ReftBV Symbol Symbol)
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
killHoles UReftBV Symbol Symbol (ReftBV Symbol Symbol)
r
  where
    inTarget :: Bool
inTarget    = GenModule Unit -> ModuleName
forall unit. GenModule unit -> ModuleName
Ghc.moduleName (HasDebugCallStack => Name -> GenModule Unit
Name -> GenModule Unit
Ghc.nameModule Name
name) ModuleName -> ModuleName -> Bool
forall a. Eq a => a -> a -> Bool
== ModName -> ModuleName
getModName ModName
target
    name :: Name
name        = a -> Name
forall a. NamedThing a => a -> Name
Ghc.getName a
x
    notExported :: Bool
notExported = Bool -> Bool
not (Name -> StableName
mkStableName (a -> Name
forall a. NamedThing a => a -> Name
Ghc.getName a
x) StableName -> HashSet StableName -> Bool
forall 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 :: UReftBV Symbol Symbol (ReftBV Symbol Symbol)
-> UReftBV Symbol Symbol (ReftBV Symbol Symbol)
killHoles UReftBV Symbol Symbol (ReftBV Symbol Symbol)
ur = UReftBV Symbol Symbol (ReftBV Symbol Symbol)
ur { ur_reft = tx $ ur_reft ur }
  where
    tx :: ReftBV Symbol Symbol -> ReftBV Symbol Symbol
tx ReftBV Symbol Symbol
r = {- traceFix ("killholes: r = " ++ showFix r) $ -} (ExprBV Symbol Symbol -> ExprBV Symbol Symbol)
-> ReftBV Symbol Symbol -> ReftBV Symbol Symbol
F.mapPredReft ExprBV Symbol Symbol -> ExprBV Symbol Symbol
dropHoles ReftBV Symbol Symbol
r
    dropHoles :: ExprBV Symbol Symbol -> ExprBV Symbol Symbol
dropHoles    = ListNE (ExprBV Symbol Symbol) -> ExprBV Symbol Symbol
forall b v.
(Ord b, Hashable b, Ord v) =>
ListNE (ExprBV b v) -> ExprBV b v
F.pAnd (ListNE (ExprBV Symbol Symbol) -> ExprBV Symbol Symbol)
-> (ExprBV Symbol Symbol -> ListNE (ExprBV Symbol Symbol))
-> ExprBV Symbol Symbol
-> ExprBV Symbol Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ExprBV Symbol Symbol -> Bool)
-> ListNE (ExprBV Symbol Symbol) -> ListNE (ExprBV Symbol Symbol)
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool)
-> (ExprBV Symbol Symbol -> Bool) -> ExprBV Symbol Symbol -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExprBV Symbol Symbol -> Bool
isHole) (ListNE (ExprBV Symbol Symbol) -> ListNE (ExprBV Symbol Symbol))
-> (ExprBV Symbol Symbol -> ListNE (ExprBV Symbol Symbol))
-> ExprBV Symbol Symbol
-> ListNE (ExprBV Symbol Symbol)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExprBV Symbol Symbol -> ListNE (ExprBV Symbol Symbol)
forall b v. (Eq b, Eq v) => ExprBV b v -> [ExprBV b v]
F.conjuncts