{-# 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
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 -> UReft Reft -> UReft Reft)
-> Type
-> LocSpecType
-> LocSpecType
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 = Var
-> ModName
-> HashSet StableName
-> SpecType
-> UReft Reft
-> UReft Reft
forall a.
NamedThing a =>
a
-> ModName
-> HashSet StableName
-> SpecType
-> UReft Reft
-> UReft Reft
maybeTrue Var
x ModName
name HashSet StableName
exports
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 = Bool
-> TCEmb TyCon
-> TyConMap
-> a
-> (SpecType -> UReft Reft -> UReft Reft)
-> Type
-> LocSpecType
-> LocSpecType
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 = Bool
-> TCEmb TyCon
-> TyConMap
-> a
-> (SpecType -> UReft Reft -> UReft Reft)
-> Type
-> LocSpecType
-> LocSpecType
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 = UserError -> Located DataConP
forall a e. Exception e => e -> a
Ex.throw (Doc -> UserError
err Doc
"fields")
| Bool
mismatchTyVars = UserError -> Located DataConP
forall a e. Exception e => e -> a
Ex.throw (Doc -> UserError
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
([(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) = DataCon -> ([Var], [Type], [Type], Type)
Ghc.dataConSig DataCon
dc
dcArgs :: [(Symbol, SpecType)]
dcArgs = [(Symbol, SpecType)] -> [(Symbol, SpecType)]
forall a. [a] -> [a]
reverse ([(Symbol, SpecType)] -> [(Symbol, SpecType)])
-> [(Symbol, SpecType)] -> [(Symbol, SpecType)]
forall a b. (a -> b) -> a -> b
$ ((Symbol, SpecType) -> Bool)
-> [(Symbol, SpecType)] -> [(Symbol, SpecType)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool)
-> ((Symbol, SpecType) -> Bool) -> (Symbol, SpecType) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (if Bool
allowTC then SpecType -> Bool
forall c t t1. TyConable c => RType c t t1 -> Bool
isEmbeddedClass else SpecType -> Bool
forall c t t1. TyConable c => RType c t t1 -> Bool
isClassType) (SpecType -> Bool)
-> ((Symbol, SpecType) -> SpecType) -> (Symbol, SpecType) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol, SpecType) -> SpecType
forall a b. (a, b) -> b
snd) (DataConP -> [(Symbol, 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 (RType RTyCon RTyVar ()) -> RTyVar)
-> [RTVar RTyVar (RType RTyCon RTyVar ())] -> [RTyVar]
forall a b. (a -> b) -> [a] -> [b]
map RTVar RTyVar (RType RTyCon RTyVar ()) -> RTyVar
forall tv s. RTVar tv s -> tv
ty_var_value ([RTVar RTyVar (RType RTyCon RTyVar ())] -> [RTyVar])
-> (SpecType -> [RTVar RTyVar (RType RTyCon RTyVar ())])
-> SpecType
-> [RTyVar]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SpecType -> [RTVar RTyVar (RType RTyCon RTyVar ())]
forall tv c r. Eq tv => RType c tv r -> [RTVar tv (RType c tv ())]
freeTyVars) (DataConP -> SpecType
dcpTyRes DataConP
dcpSpecType -> [SpecType] -> [SpecType]
forall a. a -> [a] -> [a]
:((Symbol, SpecType) -> SpecType
forall a b. (a, b) -> b
snd ((Symbol, SpecType) -> SpecType)
-> [(Symbol, SpecType)] -> [SpecType]
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 = 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
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
/= [(Symbol, SpecType)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Symbol, 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 -> UserError
err Doc
things = SrcSpan -> Doc -> Doc -> UserError
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 :: Bool -> F.TCEmb Ghc.TyCon -> Bare.TyConMap
-> Located DataConP
-> ([Ghc.Var], [Ghc.Type], Ghc.Type)
-> ([RTyVar] , [(F.Symbol, SpecType)], SpecType)
-> ([(F.Symbol, SpecType)], SpecType)
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)
= String
-> ([(Symbol, SpecType)], SpecType)
-> ([(Symbol, SpecType)], SpecType)
forall a. PPrint a => String -> a -> a
F.notracepp String
msg (Int -> [(Symbol, SpecType)] -> [(Symbol, SpecType)]
forall a. Int -> [a] -> [a]
drop Int
nTyVars ([Symbol] -> [SpecType] -> [(Symbol, SpecType)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
xs [SpecType]
ts), SpecType
t)
where
(([Symbol]
xs,[RFInfo]
_,[SpecType]
ts,[UReft Reft]
_), SpecType
t) = SpecType
-> (([Symbol], [RFInfo], [SpecType], [UReft Reft]), SpecType)
forall t t1 a.
RType t t1 a
-> (([Symbol], [RFInfo], [RType t t1 a], [a]), RType t t1 a)
bkArrow (LocSpecType -> SpecType
forall a. Located a -> a
val LocSpecType
pT)
pT :: LocSpecType
pT = Bool
-> PlugTV Name
-> TCEmb TyCon
-> TyConMap
-> (SpecType -> UReft Reft -> UReft Reft)
-> Type
-> LocSpecType
-> LocSpecType
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 (Name -> PlugTV Name
forall v. v -> PlugTV v
Bare.LqTV Name
dcName) TCEmb TyCon
embs TyConMap
tyi ((UReft Reft -> UReft Reft) -> SpecType -> UReft Reft -> UReft Reft
forall a b. a -> b -> a
const UReft Reft -> UReft Reft
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 ((() :: Constraint) => 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.
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] [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ [Type]
hsArgs
lqArgs' :: [(Symbol, SpecType)]
lqArgs' = [(Symbol
F.dummySymbol, RTyVar -> UReft Reft -> SpecType
forall c tv r. tv -> r -> RType c tv r
RVar RTyVar
a UReft Reft
forall a. Monoid a => a
mempty) | RTyVar
a <- [RTyVar]
lqAs] [(Symbol, SpecType)]
-> [(Symbol, SpecType)] -> [(Symbol, SpecType)]
forall a. [a] -> [a] -> [a]
++ [(Symbol, SpecType)]
lqArgs
nTyVars :: Int
nTyVars = [Var] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Var]
hsAs
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
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)
= 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 (RType RTyCon RTyVar ()), UReft Reft)]
-> [PVar (RType RTyCon RTyVar ())]
-> [(Symbol, RFInfo, SpecType, UReft Reft)]
-> SpecType
-> SpecType
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 ([RTVar RTyVar (RType RTyCon RTyVar ())]
-> [UReft Reft]
-> [(RTVar RTyVar (RType RTyCon RTyVar ()), UReft Reft)]
forall a b. [a] -> [b] -> [(a, b)]
zip (RTVar RTyVar (RType RTyCon RTyVar ())
-> RTVar RTyVar (RType RTyCon RTyVar ())
forall r i.
Monoid r =>
RTVar RTyVar i -> RTVar RTyVar (RType RTyCon RTyVar r)
updateRTVar (RTVar RTyVar (RType RTyCon RTyVar ())
-> RTVar RTyVar (RType RTyCon RTyVar ()))
-> [RTVar RTyVar (RType RTyCon RTyVar ())]
-> [RTVar RTyVar (RType RTyCon RTyVar ())]
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' []
(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, Monoid r) =>
t (Symbol, RType c tv r) -> RType c tv r -> RType 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 -> UReft Reft -> UReft Reft)
-> SpecType
-> SpecType
-> SpecType
goPlug TCEmb TyCon
tce TyConMap
tyi Doc -> Doc -> Error
forall {t}. Doc -> Doc -> TError t
err SpecType -> UReft Reft -> UReft Reft
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 -> Expr -> Expr) -> SpecType -> SpecType
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)
(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. 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, RTyVar -> () -> RType RTyCon RTyVar ()
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 = [(Symbol, Sort)] -> CoSub
forall k v. (Eq k, 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' :: [PVar (RType RTyCon RTyVar ())]
ps' = (RType RTyCon RTyVar () -> RType RTyCon RTyVar ())
-> PVar (RType RTyCon RTyVar ()) -> PVar (RType RTyCon RTyVar ())
forall a b. (a -> b) -> PVar a -> PVar b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([(RTyVar, RType RTyCon RTyVar ())]
-> RType RTyCon RTyVar () -> RType RTyCon RTyVar ()
forall tv ty c. SubsTy tv ty c => [(tv, ty)] -> c -> c
subts [(RTyVar, RType RTyCon RTyVar ())]
su') (PVar (RType RTyCon RTyVar ()) -> PVar (RType RTyCon RTyVar ()))
-> [PVar (RType RTyCon RTyVar ())]
-> [PVar (RType RTyCon RTyVar ())]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [PVar (RType RTyCon RTyVar ())]
ps
cs' :: [(Symbol, SpecType)]
cs' = [(Symbol
F.dummySymbol, RTyCon
-> [SpecType]
-> [RTProp RTyCon RTyVar (UReft Reft)]
-> UReft Reft
-> SpecType
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
forall a. Monoid a => a
mempty) | (RTyCon
c, [SpecType]
ts) <- [(RTyCon, [SpecType])]
cs2 ]
([RTVar RTyVar (RType RTyCon RTyVar ())]
αs', [UReft Reft]
rs) = [(RTVar RTyVar (RType RTyCon RTyVar ()), UReft Reft)]
-> ([RTVar RTyVar (RType RTyCon RTyVar ())], [UReft Reft])
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 (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. 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 (String -> SpecType -> SpecType
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 = ((Symbol, RType c tv r) -> RType c tv r -> RType c tv r)
-> RType c tv r -> t (Symbol, RType c tv r) -> RType 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 -> RType c tv r -> RType c tv r -> RType c tv r)
-> (Symbol, RType c tv r) -> RType c tv r -> RType c tv r
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (RFInfo -> Symbol -> RType c tv r -> RType c tv r -> RType c tv r
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 = 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)
(RType RTyCon RTyVar () -> Doc
forall a. PPrint a => a -> Doc
pprint (RType RTyCon RTyVar () -> Doc) -> RType RTyCon RTyVar () -> Doc
forall a b. (a -> b) -> a -> b
$ SpecType -> RType RTyCon RTyVar ()
forall c tv r. RType c tv r -> RType c tv ()
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 -> 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)
= 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 (RType RTyCon RTyVar ()), UReft Reft)]
-> [PVar (RType RTyCon RTyVar ())]
-> [(Symbol, RFInfo, SpecType, UReft Reft)]
-> SpecType
-> SpecType
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 ([RTVar RTyVar (RType RTyCon RTyVar ())]
-> [UReft Reft]
-> [(RTVar RTyVar (RType RTyCon RTyVar ()), UReft Reft)]
forall a b. [a] -> [b] -> [(a, b)]
zip (RTVar RTyVar (RType RTyCon RTyVar ())
-> RTVar RTyVar (RType RTyCon RTyVar ())
forall r i.
Monoid r =>
RTVar RTyVar i -> RTVar RTyVar (RType RTyCon RTyVar r)
updateRTVar (RTVar RTyVar (RType RTyCon RTyVar ())
-> RTVar RTyVar (RType RTyCon RTyVar ()))
-> [RTVar RTyVar (RType RTyCon RTyVar ())]
-> [RTVar RTyVar (RType RTyCon RTyVar ())]
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 []
(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, Monoid r) =>
t (Symbol, RType c tv r) -> RType c tv r -> RType 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 -> UReft Reft -> UReft Reft)
-> SpecType
-> SpecType
-> SpecType
goPlug TCEmb TyCon
tce TyConMap
tyi Doc -> Doc -> Error
forall {t}. Doc -> Doc -> TError t
err SpecType -> UReft Reft -> UReft Reft
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 (RType RTyCon RTyVar ())]
as'' = [(RTyVar, RTyVar)]
-> RTVar RTyVar (RType RTyCon RTyVar ())
-> RTVar RTyVar (RType RTyCon RTyVar ())
subRTVar [(RTyVar, RTyVar)]
su (RTVar RTyVar (RType RTyCon RTyVar ())
-> RTVar RTyVar (RType RTyCon RTyVar ()))
-> [RTVar RTyVar (RType RTyCon RTyVar ())]
-> [RTVar RTyVar (RType RTyCon RTyVar ())]
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) = [(RTVar RTyVar (RType RTyCon RTyVar ()), UReft Reft)]
-> ([RTVar RTyVar (RType RTyCon RTyVar ())], [UReft Reft])
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 (RTyCon
-> [SpecType]
-> [RTProp RTyCon RTyVar (UReft Reft)]
-> UReft Reft
-> SpecType
forall c tv r.
c -> [RType c tv r] -> [RTProp c tv r] -> r -> RType c tv r
RApp RTyCon
c [SpecType]
t [] UReft Reft
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. 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 (Type -> SpecType
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 = ((Symbol, RType c tv r) -> RType c tv r -> RType c tv r)
-> RType c tv r -> t (Symbol, RType c tv r) -> RType 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 -> RType c tv r -> RType c tv r -> RType c tv r)
-> (Symbol, RType c tv r) -> RType c tv r -> RType c tv r
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (RFInfo -> Symbol -> RType c tv r -> RType c tv r -> RType c tv r
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 = 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)
(RType RTyCon RTyVar () -> Doc
forall a. PPrint a => a -> Doc
pprint (RType RTyCon RTyVar () -> Doc) -> RType RTyCon RTyVar () -> Doc
forall a b. (a -> b) -> a -> b
$ SpecType -> RType RTyCon RTyVar ()
forall c tv r. RType c tv r -> RType c tv ()
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 -> UReft Reft -> UReft Reft
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 (RType RTyCon RTyVar ()), UReft Reft)]
-> [PVar (RType RTyCon RTyVar ())]
-> [(Symbol, RFInfo, SpecType, UReft Reft)]
-> SpecType
-> SpecType
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 ([RTVar RTyVar (RType RTyCon RTyVar ())]
-> [UReft Reft]
-> [(RTVar RTyVar (RType RTyCon RTyVar ()), UReft Reft)]
forall a b. [a] -> [b] -> [(a, b)]
zip (RTVar RTyVar (RType RTyCon RTyVar ())
-> RTVar RTyVar (RType RTyCon RTyVar ())
forall r i.
Monoid r =>
RTVar RTyVar i -> RTVar RTyVar (RType RTyCon RTyVar r)
updateRTVar (RTVar RTyVar (RType RTyCon RTyVar ())
-> RTVar RTyVar (RType RTyCon RTyVar ()))
-> [RTVar RTyVar (RType RTyCon RTyVar ())]
-> [RTVar RTyVar (RType RTyCon RTyVar ())]
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 [(Symbol, RFInfo, SpecType, UReft Reft)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Symbol, RFInfo, SpecType, UReft Reft)]
cs Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> [(Symbol, RFInfo, SpecType, UReft Reft)] -> Int
forall a. [a] -> Int
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')
(SpecType -> SpecType)
-> (SpecType -> SpecType) -> SpecType -> SpecType
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 Doc -> Doc -> Error
forall {t}. Doc -> Doc -> TError t
err SpecType -> UReft Reft -> UReft Reft
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 (RType RTyCon RTyVar ())]
as'' = [(RTyVar, RTyVar)]
-> RTVar RTyVar (RType RTyCon RTyVar ())
-> RTVar RTyVar (RType RTyCon RTyVar ())
subRTVar [(RTyVar, RTyVar)]
su (RTVar RTyVar (RType RTyCon RTyVar ())
-> RTVar RTyVar (RType RTyCon RTyVar ()))
-> [RTVar RTyVar (RType RTyCon RTyVar ())]
-> [RTVar RTyVar (RType RTyCon RTyVar ())]
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) = [(RTVar RTyVar (RType RTyCon RTyVar ()), UReft Reft)]
-> ([RTVar RTyVar (RType RTyCon RTyVar ())], [UReft Reft])
forall a b. [(a, b)] -> ([a], [b])
unzip [(RTVar RTyVar (RType RTyCon RTyVar ()), UReft Reft)]
as
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. 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' (Type -> SpecType
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 = 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)
(RType RTyCon RTyVar () -> Doc
forall a. PPrint a => a -> Doc
pprint (RType RTyCon RTyVar () -> Doc) -> RType RTyCon RTyVar () -> Doc
forall a b. (a -> b) -> a -> b
$ SpecType -> RType RTyCon RTyVar ()
forall c tv r. RType c tv r -> RType c tv ()
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 (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) = RTVar RTyVar (RType RTyCon RTyVar ())
-> (RTyVar -> RTVar RTyVar (RType RTyCon RTyVar ()))
-> Maybe RTyVar
-> RTVar RTyVar (RType RTyCon RTyVar ())
forall b a. b -> (a -> b) -> Maybe a -> b
Mb.maybe RTVar RTyVar (RType RTyCon RTyVar ())
a (RTyVar
-> RTVInfo (RType RTyCon RTyVar ())
-> RTVar RTyVar (RType RTyCon RTyVar ())
forall tv s. tv -> RTVInfo s -> RTVar tv s
`RTVar` RTVInfo (RType RTyCon RTyVar ())
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 -> 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 = 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)
addHole :: SpecType -> SpecType
addHole :: SpecType -> SpecType
addHole t :: SpecType
t@(RVar RTyVar
v UReft Reft
_) = RTyVar -> UReft Reft -> SpecType
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
_) = RTyCon
-> [SpecType]
-> [RTProp RTyCon RTyVar (UReft Reft)]
-> UReft Reft
-> SpecType
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) = Symbol -> RFInfo -> SpecType -> SpecType -> UReft Reft -> SpecType
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) = RTVar RTyVar (RType RTyCon RTyVar ())
-> SpecType -> UReft Reft -> SpecType
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' = RTVar RTyVar (RType RTyCon RTyVar ())
-> SpecType -> UReft Reft -> SpecType
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') = PVar (RType RTyCon RTyVar ()) -> SpecType -> SpecType
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') = Symbol -> SpecType -> SpecType -> SpecType
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') = Symbol -> SpecType -> SpecType -> SpecType
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') = [(Symbol, SpecType)] -> UReft Reft -> Oblig -> SpecType -> SpecType
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) = SpecType -> SpecType -> UReft Reft -> SpecType
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
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)
| [SpecType] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SpecType]
ts Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [SpecType] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SpecType]
ts' = RTyCon
-> [SpecType]
-> [RTProp RTyCon RTyVar (UReft Reft)]
-> UReft Reft
-> SpecType
forall c tv r.
c -> [RType c tv r] -> [RTProp c tv r] -> r -> RType 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 (UReft Reft)]
p UReft Reft
r
go SpecType
hsT SpecType
lqT = Error -> SpecType
forall a e. 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))
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) = RTyCon
-> [SpecType]
-> [RTProp RTyCon RTyVar (UReft Reft)]
-> UReft Reft
-> SpecType
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
_ = TCEmb TyCon -> TyConMap -> SpecType -> SpecType
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 (RTyCon
-> [SpecType]
-> [RTProp RTyCon RTyVar (UReft Reft)]
-> UReft Reft
-> SpecType
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 (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)
= UReft Reft
r
| Bool
otherwise
= UReft Reft -> UReft Reft
killHoles UReft Reft
r
where
inTarget :: Bool
inTarget = GenModule Unit -> ModuleName
forall unit. GenModule unit -> ModuleName
Ghc.moduleName ((() :: Constraint) => 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. (Eq a, Hashable a) => a -> HashSet a -> Bool
`S.member` HashSet StableName
exports)
killHoles :: RReft -> RReft
killHoles :: UReft Reft -> UReft Reft
killHoles UReft Reft
ur = UReft Reft
ur { ur_reft = tx $ ur_reft ur }
where
tx :: Reft -> Reft
tx Reft
r = (Expr -> Expr) -> Reft -> Reft
F.mapPredReft Expr -> Expr
dropHoles Reft
r
dropHoles :: Expr -> Expr
dropHoles = ListNE Expr -> Expr
F.pAnd (ListNE Expr -> Expr) -> (Expr -> ListNE Expr) -> Expr -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> Bool) -> ListNE Expr -> ListNE Expr
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Expr -> Bool) -> Expr -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Bool
isHole) (ListNE Expr -> ListNE Expr)
-> (Expr -> ListNE Expr) -> Expr -> ListNE Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> ListNE Expr
F.conjuncts