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

{-# OPTIONS_GHC -Wno-orphans #-}
{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}

module Language.Haskell.Liquid.Types.PredType (
    PrType
  , TyConP (..), DataConP (..)
  , dataConTy
  , dataConPSpecType
  , makeTyConInfo
  , replacePreds
  , replacePredsWithRefs
  , pVartoRConc

  -- * Dummy `Type` that represents _all_ abstract-predicates
  , predType

  -- * Compute @RType@ of a given @PVar@
  , pvarRType
  , substParg
  , pApp
  , pappSort
  , pappArity

  -- * should be elsewhere
  , dataConWorkRep
  , substPVar
  ) where

import           Prelude                         hiding (error)
import           Text.PrettyPrint.HughesPJ
import           Liquid.GHC.API hiding ( panic
                                                        , (<+>)
                                                        , hsep
                                                        , punctuate
                                                        , comma
                                                        , parens
                                                        , showPpr
                                                        )
import           Language.Haskell.Liquid.GHC.TypeRep ()
import           Data.Hashable
import qualified Data.HashMap.Strict             as M
import qualified Data.Maybe                                 as Mb
import qualified Data.List         as L -- (foldl', partition)
-- import           Data.List                       (nub)

import           Language.Fixpoint.Misc

-- import           Language.Fixpoint.Types         hiding (Expr, Predicate)
import qualified Language.Fixpoint.Types                    as F
import qualified Liquid.GHC.API            as Ghc
import           Language.Haskell.Liquid.GHC.Misc
import           Language.Haskell.Liquid.Misc
import           Language.Haskell.Liquid.Types.RefType hiding (generalize)
import           Language.Haskell.Liquid.Types.Types
import           Data.Default

makeTyConInfo :: F.TCEmb Ghc.TyCon -> [Ghc.TyCon] -> [TyConP] -> TyConMap
makeTyConInfo :: TCEmb TyCon -> [TyCon] -> [TyConP] -> TyConMap
makeTyConInfo TCEmb TyCon
tce [TyCon]
fiTcs [TyConP]
tcps = TyConMap
  { tcmTyRTy :: HashMap TyCon RTyCon
tcmTyRTy    = HashMap TyCon RTyCon
tcM
  , tcmFIRTy :: HashMap (TyCon, [Sort]) RTyCon
tcmFIRTy    = HashMap (TyCon, [Sort]) RTyCon
tcInstM
  , tcmFtcArity :: HashMap TyCon Int
tcmFtcArity = HashMap TyCon Int
arities
  }
  where
    tcM :: HashMap TyCon RTyCon
tcM         = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [(TyConP -> TyCon
tcpCon TyConP
tcp, TyConP -> RTyCon
mkRTyCon TyConP
tcp) | TyConP
tcp <- [TyConP]
tcps ]
    tcInstM :: HashMap (TyCon, [Sort]) RTyCon
tcInstM     = TCEmb TyCon
-> [TyCon]
-> HashMap TyCon RTyCon
-> HashMap (TyCon, [Sort]) RTyCon
mkFInstRTyCon TCEmb TyCon
tce [TyCon]
fiTcs HashMap TyCon RTyCon
tcM
    arities :: HashMap TyCon Int
arities     = forall k v.
(?callStack::CallStack, Eq k, Hashable k, Show k) =>
[Char] -> [(k, v)] -> HashMap k v
safeFromList [Char]
"makeTyConInfo" [ (TyCon
c, forall (t :: * -> *) a. Foldable t => t a -> Int
length [Sort]
ts) | (TyCon
c, [Sort]
ts) <- forall k v. HashMap k v -> [k]
M.keys HashMap (TyCon, [Sort]) RTyCon
tcInstM ]

mkFInstRTyCon :: F.TCEmb Ghc.TyCon -> [Ghc.TyCon] -> M.HashMap Ghc.TyCon RTyCon -> M.HashMap (Ghc.TyCon, [F.Sort]) RTyCon
mkFInstRTyCon :: TCEmb TyCon
-> [TyCon]
-> HashMap TyCon RTyCon
-> HashMap (TyCon, [Sort]) RTyCon
mkFInstRTyCon TCEmb TyCon
tce [TyCon]
fiTcs HashMap TyCon RTyCon
tcm = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList
  [ ((TyCon
c, TCEmb TyCon -> Type -> Sort
typeSort TCEmb TyCon
tce forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Type]
ts), RTyCon
rtc)
    | TyCon
fiTc    <- [TyCon]
fiTcs
    , RTyCon
rtc     <- forall a. Maybe a -> [a]
Mb.maybeToList (forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup TyCon
fiTc HashMap TyCon RTyCon
tcm)
    , (TyCon
c, [Type]
ts) <- forall a. Maybe a -> [a]
Mb.maybeToList (TyCon -> Maybe (TyCon, [Type])
famInstArgs TyCon
fiTc)
  ]

mkRTyCon ::  TyConP -> RTyCon
mkRTyCon :: TyConP -> RTyCon
mkRTyCon (TyConP SourcePos
_ TyCon
tc [RTyVar]
αs' [RPVar]
ps VarianceInfo
tyvariance VarianceInfo
predvariance Maybe SizeFun
size)
  = TyCon -> [RPVar] -> TyConInfo -> RTyCon
RTyCon TyCon
tc [RPVar]
pvs' (TyCon -> VarianceInfo -> VarianceInfo -> Maybe SizeFun -> TyConInfo
mkTyConInfo TyCon
tc VarianceInfo
tyvariance VarianceInfo
predvariance Maybe SizeFun
size)
  where
    τs :: [RSort]
τs   = [forall r c. Monoid r => TyVar -> RType c RTyVar r
rVar TyVar
α :: RSort |  TyVar
α <- TyCon -> [TyVar]
tyConTyVarsDef TyCon
tc]
    pvs' :: [RPVar]
pvs' = forall tv ty c. SubsTy tv ty c => [(tv, ty)] -> c -> c
subts (forall a b. [a] -> [b] -> [(a, b)]
zip [RTyVar]
αs' [RSort]
τs) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RPVar]
ps


-------------------------------------------------------------------------------
-- | @dataConPSpecType@ converts a @DataConP@, LH's internal representation for
--   a (refined) data constructor into a @SpecType@ for that constructor.
--   TODO: duplicated with Liquid.Measure.makeDataConType
-------------------------------------------------------------------------------
dataConPSpecType :: Bool -> DataConP -> [(Var, SpecType)]
-------------------------------------------------------------------------------
dataConPSpecType :: Bool -> DataConP -> [(TyVar, RRType RReft)]
dataConPSpecType Bool
allowTC DataConP
dcp    = [(TyVar
workX, RRType RReft
workT), (TyVar
wrapX, RRType RReft
wrapT) ]
  where
    workT :: RRType RReft
workT | Bool
isVanilla   = RRType RReft
wrapT
          | Bool
otherwise   = DataCon -> RRType RReft -> RRType RReft
dcWorkSpecType   DataCon
dc RRType RReft
wrapT
    wrapT :: RRType RReft
wrapT               = Bool -> DataCon -> DataConP -> RRType RReft
dcWrapSpecType   Bool
allowTC  DataCon
dc DataConP
dcp
    workX :: TyVar
workX               = DataCon -> TyVar
dataConWorkId    DataCon
dc            -- This is the weird one for GADTs
    wrapX :: TyVar
wrapX               = DataCon -> TyVar
dataConWrapId    DataCon
dc            -- This is what the user expects to see
    isVanilla :: Bool
isVanilla           = DataCon -> Bool
isVanillaDataCon DataCon
dc
    dc :: DataCon
dc                  = DataConP -> DataCon
dcpCon DataConP
dcp

dcWorkSpecType :: DataCon -> SpecType -> SpecType
dcWorkSpecType :: DataCon -> RRType RReft -> RRType RReft
dcWorkSpecType DataCon
c RRType RReft
wrT    = forall c tv r. RTypeRep c tv r -> RType c tv r
fromRTypeRep (DataCon -> SpecRep -> SpecRep -> SpecRep
meetWorkWrapRep DataCon
c SpecRep
wkR SpecRep
wrR)
  where
    wkR :: SpecRep
wkR                 = DataCon -> SpecRep
dataConWorkRep DataCon
c
    wrR :: SpecRep
wrR                 = forall c tv r. RType c tv r -> RTypeRep c tv r
toRTypeRep RRType RReft
wrT

dataConWorkRep :: DataCon -> SpecRep
dataConWorkRep :: DataCon -> SpecRep
dataConWorkRep DataCon
c = forall c tv r. RType c tv r -> RTypeRep c tv r
toRTypeRep
                 -- . F.tracepp ("DCWR-2: " ++ F.showpp c)
                 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall r. Monoid r => Type -> RRType r
ofType
                 -- . F.tracepp ("DCWR-1: " ++ F.showpp c)
                 forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataCon -> Type
dataConRepType
                 -- . Var.varType
                 -- . dataConWorkId
                 forall a b. (a -> b) -> a -> b
$ DataCon
c
{-
dataConWorkRep :: DataCon -> SpecRep
dataConWorkRep dc = RTypeRep
  { ty_vars   = as
  , ty_preds  = []
  , ty_labels = []
  , ty_binds  = replicate nArgs F.dummySymbol
  , ty_refts  = replicate nArgs mempty
  , ty_args   = ts'
  , ty_res    = t'
  }
  where
    (ts', t')          = F.tracepp "DCWR-1" (ofType <$> ts, ofType t)
    as                 = makeRTVar . rTyVar <$> αs
    tArg
    (αs,_,eqs,th,ts,t) = dataConFullSig dc
    nArgs              = length ts

dataConResultTy :: DataCon -> [TyVar] -> Type -> Type
dataConResultTy dc αs t = mkFamilyTyConApp tc tArgs'
  where
    tArgs'              = take (nArgs - nVars) tArgs ++ (mkTyVarTy <$> αs)
    nVars               = length αs
    nArgs               = length tArgs
    (tc, tArgs)         = fromMaybe err (splitTyConApp_maybe _t)
    err                 = GM.namedPanic dc ("Cannot split result type of DataCon " ++ show dc)

  --  t                 = RT.ofType  $  mkFamilyTyConApp tc tArgs'
  -- as                = makeRTVar . rTyVar <$> αs
  --  (αs,_,_,_,_ts,_t) = dataConFullSig dc

-}

meetWorkWrapRep :: DataCon -> SpecRep -> SpecRep -> SpecRep
meetWorkWrapRep :: DataCon -> SpecRep -> SpecRep -> SpecRep
meetWorkWrapRep DataCon
c SpecRep
workR SpecRep
wrapR
  | Int
0 forall a. Ord a => a -> a -> Bool
<= Int
pad'
  = SpecRep
workR { ty_binds :: [Symbol]
ty_binds = [Symbol]
xs forall a. [a] -> [a] -> [a]
++ forall c tv r. RTypeRep c tv r -> [Symbol]
ty_binds SpecRep
wrapR
          , ty_args :: [RRType RReft]
ty_args  = [RRType RReft]
ts forall a. [a] -> [a] -> [a]
++ forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith forall r. Reftable r => r -> r -> r
F.meet [RRType RReft]
ts' (forall c tv r. RTypeRep c tv r -> [RType c tv r]
ty_args SpecRep
wrapR)
          , ty_res :: RRType RReft
ty_res   = RRType RReft -> RRType RReft -> RRType RReft
strengthenRType (forall c tv r. RTypeRep c tv r -> RType c tv r
ty_res SpecRep
workR)    (forall c tv r. RTypeRep c tv r -> RType c tv r
ty_res  SpecRep
wrapR)
          , ty_preds :: [RPVar]
ty_preds = forall c tv r. RTypeRep c tv r -> [PVar (RType c tv ())]
ty_preds SpecRep
wrapR
          }
  | Bool
otherwise
  = forall a. Maybe SrcSpan -> [Char] -> a
panic (forall a. a -> Maybe a
Just (forall a. NamedThing a => a -> SrcSpan
getSrcSpan DataCon
c)) [Char]
errMsg
  where
    pad' :: Int
pad'      = {- F.tracepp ("MEETWKRAP: " ++ show (ty_vars workR)) $ -} Int
workN forall a. Num a => a -> a -> a
- Int
wrapN
    ([Symbol]
xs, [Symbol]
_)   = forall a. Int -> [a] -> ([a], [a])
splitAt Int
pad' (forall c tv r. RTypeRep c tv r -> [Symbol]
ty_binds SpecRep
workR)
    ([RRType RReft]
ts, [RRType RReft]
ts') = forall a. Int -> [a] -> ([a], [a])
splitAt Int
pad' (forall c tv r. RTypeRep c tv r -> [RType c tv r]
ty_args  SpecRep
workR)
    workN :: Int
workN     = forall (t :: * -> *) a. Foldable t => t a -> Int
length      (forall c tv r. RTypeRep c tv r -> [RType c tv r]
ty_args  SpecRep
workR)
    wrapN :: Int
wrapN     = forall (t :: * -> *) a. Foldable t => t a -> Int
length      (forall c tv r. RTypeRep c tv r -> [RType c tv r]
ty_args  SpecRep
wrapR)
    errMsg :: [Char]
errMsg    = [Char]
"Unsupported Work/Wrap types for Data Constructor " forall a. [a] -> [a] -> [a]
++ forall a. Outputable a => a -> [Char]
showPpr DataCon
c

strengthenRType :: SpecType -> SpecType -> SpecType
strengthenRType :: RRType RReft -> RRType RReft -> RRType RReft
strengthenRType RRType RReft
wkT RRType RReft
wrT = forall b a. b -> (a -> b) -> Maybe a -> b
maybe RRType RReft
wkT (forall r c tv. Reftable r => RType c tv r -> r -> RType c tv r
strengthen RRType RReft
wkT) (forall c tv r. RType c tv r -> Maybe r
stripRTypeBase RRType RReft
wrT)


-- maybe a tc flag is unnecessary but I don't know if {-@ class ... @-}
-- would reach here
dcWrapSpecType :: Bool -> DataCon -> DataConP -> SpecType
dcWrapSpecType :: Bool -> DataCon -> DataConP -> RRType RReft
dcWrapSpecType Bool
allowTC DataCon
dc (DataConP SourcePos
_ DataCon
_ [RTyVar]
vs [RPVar]
ps [RRType RReft]
cs [(Symbol, RRType RReft)]
yts RRType RReft
rt Bool
_ Symbol
_ SourcePos
_)
  = {- F.tracepp ("dcWrapSpecType: " ++ show dc ++ " " ++ F.showpp rt) $ -}
    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 RSort, RReft)]
makeVars' [RPVar]
ps [(Symbol, RFInfo, RRType RReft, RReft)]
ts' RRType RReft
rt'
  where
    isCls :: Bool
isCls    = TyCon -> Bool
Ghc.isClassTyCon forall a b. (a -> b) -> a -> b
$ DataCon -> TyCon
Ghc.dataConTyCon DataCon
dc
    ([Symbol]
as, [RRType RReft]
sts) = forall a b. [(a, b)] -> ([a], [b])
unzip (forall a. [a] -> [a]
reverse [(Symbol, RRType RReft)]
yts)
    mkDSym :: a -> Symbol
mkDSym a
z = forall a. Symbolic a => a -> Symbol
F.symbol a
z Symbol -> Symbol -> Symbol
`F.suffixSymbol` forall a. Symbolic a => a -> Symbol
F.symbol DataCon
dc
    bs :: [Symbol]
bs       = forall a. Symbolic a => a -> Symbol
mkDSym forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol]
as
    tx :: [(Symbol, Expr)]
-> [Symbol] -> [Symbol] -> [c] -> [(Symbol, RFInfo, c, d)]
tx [(Symbol, Expr)]
_  []     []     []     = []
    tx [(Symbol, Expr)]
su (Symbol
x:[Symbol]
xs) (Symbol
y:[Symbol]
ys) (c
t:[c]
ts) = (Symbol
y, Bool -> RFInfo
classRFInfo Bool
allowTC , if Bool
allowTC Bool -> Bool -> Bool
&& Bool
isCls then c
t else forall a. Subable a => Subst -> a -> a
F.subst ([(Symbol, Expr)] -> Subst
F.mkSubst [(Symbol, Expr)]
su) c
t, forall a. Monoid a => a
mempty)
                               forall a. a -> [a] -> [a]
: [(Symbol, Expr)]
-> [Symbol] -> [Symbol] -> [c] -> [(Symbol, RFInfo, c, d)]
tx ((Symbol
x, Symbol -> Expr
F.EVar Symbol
y)forall a. a -> [a] -> [a]
:[(Symbol, Expr)]
su) [Symbol]
xs [Symbol]
ys [c]
ts
    tx [(Symbol, Expr)]
_ [Symbol]
_ [Symbol]
_ [c]
_ = forall a. Maybe SrcSpan -> [Char] -> a
panic forall a. Maybe a
Nothing [Char]
"PredType.dataConPSpecType.tx called on invalid inputs"
    yts' :: [(Symbol, RFInfo, RRType RReft, RReft)]
yts'     = forall {c} {d}.
(Subable c, Monoid d) =>
[(Symbol, Expr)]
-> [Symbol] -> [Symbol] -> [c] -> [(Symbol, RFInfo, c, d)]
tx [] [Symbol]
as [Symbol]
bs [RRType RReft]
sts
    ts' :: [(Symbol, RFInfo, RRType RReft, RReft)]
ts'      = forall a b. (a -> b) -> [a] -> [b]
map (Symbol
"" , Bool -> RFInfo
classRFInfo Bool
allowTC , , forall a. Monoid a => a
mempty) [RRType RReft]
cs forall a. [a] -> [a] -> [a]
++ [(Symbol, RFInfo, RRType RReft, RReft)]
yts'
    subst :: Subst
subst    = [(Symbol, Expr)] -> Subst
F.mkSubst [(Symbol
x, Symbol -> Expr
F.EVar Symbol
y) | (Symbol
x, Symbol
y) <- forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
as [Symbol]
bs]
    rt' :: RRType RReft
rt'      = forall a. Subable a => Subst -> a -> a
F.subst Subst
subst RRType RReft
rt
    makeVars :: [RTVar RTyVar RSort]
makeVars = forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\RTyVar
v TyVar
a -> forall tv s. tv -> RTVInfo s -> RTVar tv s
RTVar RTyVar
v (forall r. Monoid r => TyVar -> RTVInfo (RRType r)
rTVarInfo TyVar
a :: RTVInfo RSort)) [RTyVar]
vs (forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ Type -> ([TyVar], Type)
splitForAllTyCoVars forall a b. (a -> b) -> a -> b
$ DataCon -> Type
dataConRepType DataCon
dc)
    makeVars' :: [(RTVar RTyVar RSort, RReft)]
makeVars' = forall a b. (a -> b) -> [a] -> [b]
map (, forall a. Monoid a => a
mempty) [RTVar RTyVar RSort]
makeVars

instance PPrint TyConP where
  pprintTidy :: Tidy -> TyConP -> Doc
pprintTidy Tidy
k TyConP
tc = Doc
"data" Doc -> Doc -> Doc
<+> forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k (TyConP -> TyCon
tcpCon TyConP
tc)
                           Doc -> Doc -> Doc
<+> forall a. PPrint a => Tidy -> [a] -> Doc
ppComm     Tidy
k (TyConP -> [RTyVar]
tcpFreeTyVarsTy TyConP
tc)
                           Doc -> Doc -> Doc
<+> forall a. PPrint a => Tidy -> [a] -> Doc
ppComm     Tidy
k (TyConP -> [RPVar]
tcpFreePredTy   TyConP
tc)
      --  (parens $ hsep (punctuate comma (pprintTidy k <$> vs))) <+>
      -- (parens $ hsep (punctuate comma (pprintTidy k <$> ps))) <+>
      -- (parens $ hsep (punctuate comma (pprintTidy k <$> ls)))

ppComm :: PPrint a => F.Tidy -> [a] -> Doc
ppComm :: forall a. PPrint a => Tidy -> [a] -> Doc
ppComm Tidy
k = Doc -> Doc
parens forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Doc] -> Doc
hsep forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> [Doc] -> [Doc]
punctuate Doc
comma forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k)




instance Show TyConP where
 show :: TyConP -> [Char]
show = forall a. PPrint a => a -> [Char]
showpp -- showSDoc . ppr

instance PPrint DataConP where
  pprintTidy :: Tidy -> DataConP -> Doc
pprintTidy Tidy
k (DataConP SourcePos
_ DataCon
dc [RTyVar]
vs [RPVar]
ps [RRType RReft]
cs [(Symbol, RRType RReft)]
yts RRType RReft
t Bool
isGadt Symbol
mname SourcePos
_)
     =  forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k DataCon
dc
    Doc -> Doc -> Doc
<+> Doc -> Doc
parens ([Doc] -> Doc
hsep (Doc -> [Doc] -> [Doc]
punctuate Doc
comma (forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RTyVar]
vs)))
    Doc -> Doc -> Doc
<+> Doc -> Doc
parens ([Doc] -> Doc
hsep (Doc -> [Doc] -> [Doc]
punctuate Doc
comma (forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RPVar]
ps)))
    Doc -> Doc -> Doc
<+> Doc -> Doc
parens ([Doc] -> Doc
hsep (Doc -> [Doc] -> [Doc]
punctuate Doc
comma (forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RRType RReft]
cs)))
    Doc -> Doc -> Doc
<+> Doc -> Doc
parens ([Doc] -> Doc
hsep (Doc -> [Doc] -> [Doc]
punctuate Doc
comma (forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, RRType RReft)]
yts)))
    Doc -> Doc -> Doc
<+> forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k Bool
isGadt
    Doc -> Doc -> Doc
<+> forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k Symbol
mname
    Doc -> Doc -> Doc
<+>  forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k RRType RReft
t

instance Show DataConP where
  show :: DataConP -> [Char]
show = forall a. PPrint a => a -> [Char]
showpp

dataConTy :: Monoid r
          => M.HashMap RTyVar (RType RTyCon RTyVar r)
          -> Type -> RType RTyCon RTyVar r
dataConTy :: forall r.
Monoid r =>
HashMap RTyVar (RType RTyCon RTyVar r)
-> Type -> RType RTyCon RTyVar r
dataConTy HashMap RTyVar (RType RTyCon RTyVar r)
m (TyVarTy TyVar
v)
  = forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
M.lookupDefault (forall r c. Monoid r => TyVar -> RType c RTyVar r
rVar TyVar
v) (TyVar -> RTyVar
RTV TyVar
v) HashMap RTyVar (RType RTyCon RTyVar r)
m
dataConTy HashMap RTyVar (RType RTyCon RTyVar r)
m (FunTy AnonArgFlag
_ Type
_ Type
t1 Type
t2)
  = forall r c tv.
Monoid r =>
Symbol -> RType c tv r -> RType c tv r -> RType c tv r
rFun Symbol
F.dummySymbol (forall r.
Monoid r =>
HashMap RTyVar (RType RTyCon RTyVar r)
-> Type -> RType RTyCon RTyVar r
dataConTy HashMap RTyVar (RType RTyCon RTyVar r)
m Type
t1) (forall r.
Monoid r =>
HashMap RTyVar (RType RTyCon RTyVar r)
-> Type -> RType RTyCon RTyVar r
dataConTy HashMap RTyVar (RType RTyCon RTyVar r)
m Type
t2)
dataConTy HashMap RTyVar (RType RTyCon RTyVar r)
m (ForAllTy (Bndr TyVar
α ArgFlag
_) Type
t) -- α :: TyVar
  = forall c tv r. RTVU c tv -> RType c tv r -> r -> RType c tv r
RAllT (forall tv s. tv -> RTVar tv s
makeRTVar (TyVar -> RTyVar
RTV TyVar
α)) (forall r.
Monoid r =>
HashMap RTyVar (RType RTyCon RTyVar r)
-> Type -> RType RTyCon RTyVar r
dataConTy HashMap RTyVar (RType RTyCon RTyVar r)
m Type
t) forall a. Monoid a => a
mempty
dataConTy HashMap RTyVar (RType RTyCon RTyVar r)
m (TyConApp TyCon
c [Type]
ts)
  = forall tv r.
TyCon
-> [RType RTyCon tv r]
-> [RTProp RTyCon tv r]
-> r
-> RType RTyCon tv r
rApp TyCon
c (forall r.
Monoid r =>
HashMap RTyVar (RType RTyCon RTyVar r)
-> Type -> RType RTyCon RTyVar r
dataConTy HashMap RTyVar (RType RTyCon RTyVar r)
m forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Type]
ts) [] forall a. Monoid a => a
mempty
dataConTy HashMap RTyVar (RType RTyCon RTyVar r)
_ Type
_
  = forall a. Maybe SrcSpan -> [Char] -> a
panic forall a. Maybe a
Nothing [Char]
"ofTypePAppTy"

----------------------------------------------------------------------------
-- | Interface: Replace Predicate With Uninterpreted Function Symbol -------
----------------------------------------------------------------------------
replacePredsWithRefs :: (UsedPVar, (F.Symbol, [((), F.Symbol, F.Expr)]) -> F.Expr)
                     -> UReft F.Reft -> UReft F.Reft
replacePredsWithRefs :: (UsedPVar, (Symbol, [((), Symbol, Expr)]) -> Expr)
-> RReft -> RReft
replacePredsWithRefs (UsedPVar
p, (Symbol, [((), Symbol, Expr)]) -> Expr
r) (MkUReft (F.Reft(Symbol
v, Expr
rs)) (Pr [UsedPVar]
ps))
  = forall r. r -> Predicate -> UReft r
MkUReft ((Symbol, Expr) -> Reft
F.Reft (Symbol
v, Expr
rs'')) ([UsedPVar] -> Predicate
Pr [UsedPVar]
ps2)
  where
    rs'' :: Expr
rs''             = forall a. Monoid a => [a] -> a
mconcat forall a b. (a -> b) -> a -> b
$ Expr
rs forall a. a -> [a] -> [a]
: [Expr]
rs'
    rs' :: [Expr]
rs'              = (Symbol, [((), Symbol, Expr)]) -> Expr
r forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol
v,) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. PVar t -> [(t, Symbol, Expr)]
pargs forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [UsedPVar]
ps1
    ([UsedPVar]
ps1, [UsedPVar]
ps2)       = forall a. (a -> Bool) -> [a] -> ([a], [a])
L.partition (forall a. Eq a => a -> a -> Bool
== UsedPVar
p) [UsedPVar]
ps

pVartoRConc :: PVar t -> (F.Symbol, [(a, b, F.Expr)]) -> F.Expr
pVartoRConc :: forall t a b. PVar t -> (Symbol, [(a, b, Expr)]) -> Expr
pVartoRConc PVar t
p (Symbol
v, [(a, b, Expr)]
args) | forall (t :: * -> *) a. Foldable t => t a -> Int
length [(a, b, Expr)]
args forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) a. Foldable t => t a -> Int
length (forall t. PVar t -> [(t, Symbol, Expr)]
pargs PVar t
p)
  = Symbol -> [Expr] -> Expr
pApp (forall t. PVar t -> Symbol
pname PVar t
p) forall a b. (a -> b) -> a -> b
$ Symbol -> Expr
F.EVar Symbol
v forall a. a -> [a] -> [a]
: (forall a b c. (a, b, c) -> c
thd3 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(a, b, Expr)]
args)

pVartoRConc PVar t
p (Symbol
v, [(a, b, Expr)]
args)
  = Symbol -> [Expr] -> Expr
pApp (forall t. PVar t -> Symbol
pname PVar t
p) forall a b. (a -> b) -> a -> b
$ Symbol -> Expr
F.EVar Symbol
v forall a. a -> [a] -> [a]
: [Expr]
args'
  where
    args' :: [Expr]
args' = (forall a b c. (a, b, c) -> c
thd3 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(a, b, Expr)]
args) forall a. [a] -> [a] -> [a]
++ forall a. Int -> [a] -> [a]
drop (forall (t :: * -> *) a. Foldable t => t a -> Int
length [(a, b, Expr)]
args) (forall a b c. (a, b, c) -> c
thd3 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. PVar t -> [(t, Symbol, Expr)]
pargs PVar t
p)

-----------------------------------------------------------------------
-- | @pvarRType π@ returns a trivial @RType@ corresponding to the
--   function signature for a @PVar@ @π@. For example, if
--      @π :: T1 -> T2 -> T3 -> Prop@
--   then @pvarRType π@ returns an @RType@ with an @RTycon@ called
--   @predRTyCon@ `RApp predRTyCon [T1, T2, T3]`
-----------------------------------------------------------------------
pvarRType :: (PPrint r, F.Reftable r) => PVar RSort -> RRType r
-----------------------------------------------------------------------
pvarRType :: forall r. (PPrint r, Reftable r) => RPVar -> RRType r
pvarRType (PV Symbol
_ PVKind RSort
k {- (PVProp τ) -} Symbol
_ [(RSort, Symbol, Expr)]
args) = forall r tv a.
Reftable r =>
PVKind (RType RTyCon tv a)
-> [RType RTyCon tv a] -> RType RTyCon tv r
rpredType PVKind RSort
k (forall a b c. (a, b, c) -> a
fst3 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(RSort, Symbol, Expr)]
args) -- (ty:tys)
  -- where
  --   ty  = uRTypeGen τ
  --   tys = uRTypeGen . fst3 <$> args


-- rpredType    :: (PPrint r, Reftable r) => PVKind (RRType r) -> [RRType r] -> RRType r
rpredType :: F.Reftable r
          => PVKind (RType RTyCon tv a)
          -> [RType RTyCon tv a] -> RType RTyCon tv r
rpredType :: forall r tv a.
Reftable r =>
PVKind (RType RTyCon tv a)
-> [RType RTyCon tv a] -> RType RTyCon tv r
rpredType (PVProp RType RTyCon tv a
t) [RType RTyCon tv a]
ts = forall c tv r.
c -> [RType c tv r] -> [RTProp c tv r] -> r -> RType c tv r
RApp RTyCon
predRTyCon  (forall b c tv a. Reftable b => RType c tv a -> RType c tv b
uRTypeGen forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RType RTyCon tv a
t forall a. a -> [a] -> [a]
: [RType RTyCon tv a]
ts) [] forall a. Monoid a => a
mempty
rpredType PVKind (RType RTyCon tv a)
PVHProp    [RType RTyCon tv a]
ts = forall c tv r.
c -> [RType c tv r] -> [RTProp c tv r] -> r -> RType c tv r
RApp RTyCon
wpredRTyCon (forall b c tv a. Reftable b => RType c tv a -> RType c tv b
uRTypeGen forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>     [RType RTyCon tv a]
ts) [] forall a. Monoid a => a
mempty

predRTyCon   :: RTyCon
predRTyCon :: RTyCon
predRTyCon   = Symbol -> RTyCon
symbolRTyCon Symbol
predName

wpredRTyCon   :: RTyCon
wpredRTyCon :: RTyCon
wpredRTyCon   = Symbol -> RTyCon
symbolRTyCon Symbol
wpredName

symbolRTyCon   :: F.Symbol -> RTyCon
symbolRTyCon :: Symbol -> RTyCon
symbolRTyCon Symbol
n = TyCon -> [RPVar] -> TyConInfo -> RTyCon
RTyCon (Char -> Int -> [Char] -> TyCon
stringTyCon Char
'x' Int
42 forall a b. (a -> b) -> a -> b
$ Symbol -> [Char]
F.symbolString Symbol
n) [] forall a. Default a => a
def

-------------------------------------------------------------------------------------
-- | Instantiate `PVar` with `RTProp` -----------------------------------------------
-------------------------------------------------------------------------------------
-- | @replacePreds@ is the main function used to substitute an (abstract)
--   predicate with a concrete Ref, that is either an `RProp` or `RHProp`
--   type. The substitution is invoked to obtain the `SpecType` resulting
--   at /predicate application/ sites in 'Language.Haskell.Liquid.Constraint'.
--   The range of the `PVar` substitutions are /fresh/ or /true/ `RefType`.
--   That is, there are no further _quantified_ `PVar` in the target.
-------------------------------------------------------------------------------------
replacePreds                 :: String -> SpecType -> [(RPVar, SpecProp)] -> SpecType
-------------------------------------------------------------------------------------
replacePreds :: [Char]
-> RRType RReft
-> [(RPVar, Ref RSort (RRType RReft))]
-> RRType RReft
replacePreds [Char]
msg                 = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' RRType RReft -> (RPVar, Ref RSort (RRType RReft)) -> RRType RReft
go
  where
     go :: RRType RReft -> (RPVar, Ref RSort (RRType RReft)) -> RRType RReft
go RRType RReft
_ (RPVar
_, RProp [(Symbol, RSort)]
_ (RHole RReft
_)) = forall a. Maybe SrcSpan -> [Char] -> a
panic forall a. Maybe a
Nothing [Char]
"replacePreds on RProp _ (RHole _)"
     go RRType RReft
z (RPVar
π, Ref RSort (RRType RReft)
t)                 = [Char]
-> (RPVar, Ref RSort (RRType RReft))
-> RRType RReft
-> RRType RReft
substPred [Char]
msg   (RPVar
π, Ref RSort (RRType RReft)
t)     RRType RReft
z


-- TODO: replace `replacePreds` with
-- instance SubsTy RPVar (Ref RReft SpecType) SpecType where
--   subt (pv, r) t = replacePreds "replacePred" t (pv, r)

-- replacePreds :: String -> SpecType -> [(RPVar, Ref Reft RefType)] -> SpecType
-- replacePreds msg       = foldl' go
--   where go z (π, RProp t) = substPred msg   (π, t)     z
--         go z (π, RPropP r) = replacePVarReft (π, r) <$> z

-------------------------------------------------------------------------------------
substPVar :: PVar BSort -> PVar BSort -> BareType -> BareType
-------------------------------------------------------------------------------------
substPVar :: PVar BSort -> PVar BSort -> BareType -> BareType
substPVar PVar BSort
src PVar BSort
dst = BareType -> BareType
go
  where
    go :: BareType -> BareType
    go :: BareType -> BareType
go (RVar BTyVar
a RReft
r)         = forall c tv r. tv -> r -> RType c tv r
RVar BTyVar
a (RReft -> RReft
goRR RReft
r)
    go (RApp BTyCon
c [BareType]
ts [RTProp BTyCon BTyVar RReft]
rs RReft
r)   = forall c tv r.
c -> [RType c tv r] -> [RTProp c tv r] -> r -> RType c tv r
RApp BTyCon
c (BareType -> BareType
go forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [BareType]
ts) (RTProp BTyCon BTyVar RReft -> RTProp BTyCon BTyVar RReft
goR forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RTProp BTyCon BTyVar RReft]
rs) (RReft -> RReft
goRR RReft
r)
    go (RAllP PVar BSort
q BareType
t)
     | forall t. PVar t -> Symbol
pname PVar BSort
q forall a. Eq a => a -> a -> Bool
== forall t. PVar t -> Symbol
pname PVar BSort
src = forall c tv r. PVU c tv -> RType c tv r -> RType c tv r
RAllP PVar BSort
q BareType
t
     | Bool
otherwise            = forall c tv r. PVU c tv -> RType c tv r -> RType c tv r
RAllP PVar BSort
q (BareType -> BareType
go BareType
t)
    go (RAllT RTVU BTyCon BTyVar
a BareType
t RReft
r)      = forall c tv r. RTVU c tv -> RType c tv r -> r -> RType c tv r
RAllT RTVU BTyCon BTyVar
a   (BareType -> BareType
go BareType
t)  (RReft -> RReft
goRR RReft
r)
    go (RFun Symbol
x RFInfo
i BareType
t BareType
t' RReft
r)  = forall c tv r.
Symbol
-> RFInfo -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun Symbol
x RFInfo
i  (BareType -> BareType
go BareType
t)  (BareType -> BareType
go BareType
t') (RReft -> RReft
goRR RReft
r)
    go (RAllE Symbol
x BareType
t BareType
t')     = forall c tv r.
Symbol -> RType c tv r -> RType c tv r -> RType c tv r
RAllE Symbol
x   (BareType -> BareType
go BareType
t)  (BareType -> BareType
go BareType
t')
    go (REx Symbol
x BareType
t BareType
t')       = forall c tv r.
Symbol -> RType c tv r -> RType c tv r -> RType c tv r
REx Symbol
x     (BareType -> BareType
go BareType
t)  (BareType -> BareType
go BareType
t')
    go (RRTy [(Symbol, BareType)]
e RReft
r Oblig
o BareType
rt)    = forall c tv r.
[(Symbol, RType c tv r)]
-> r -> Oblig -> RType c tv r -> RType c tv r
RRTy [(Symbol, BareType)]
e'   (RReft -> RReft
goRR RReft
r) Oblig
o (BareType -> BareType
go BareType
rt) where e' :: [(Symbol, BareType)]
e' = [(Symbol
x, BareType -> BareType
go BareType
t) | (Symbol
x, BareType
t) <- [(Symbol, BareType)]
e]
    go (RAppTy BareType
t1 BareType
t2 RReft
r)   = forall c tv r. RType c tv r -> RType c tv r -> r -> RType c tv r
RAppTy    (BareType -> BareType
go BareType
t1) (BareType -> BareType
go BareType
t2) (RReft -> RReft
goRR RReft
r)
    go (RHole RReft
r)          = forall c tv r. r -> RType c tv r
RHole     (RReft -> RReft
goRR RReft
r)
    go t :: BareType
t@(RExprArg  Located Expr
_)    = BareType
t
    goR :: BRProp RReft -> BRProp RReft
    goR :: RTProp BTyCon BTyVar RReft -> RTProp BTyCon BTyVar RReft
goR RTProp BTyCon BTyVar RReft
rp = RTProp BTyCon BTyVar RReft
rp {rf_body :: BareType
rf_body = BareType -> BareType
go (forall τ t. Ref τ t -> t
rf_body RTProp BTyCon BTyVar RReft
rp) }
    goRR :: RReft -> RReft
    goRR :: RReft -> RReft
goRR RReft
rr = RReft
rr { ur_pred :: Predicate
ur_pred = Predicate -> Predicate
goP (forall r. UReft r -> Predicate
ur_pred RReft
rr) }
    goP :: Predicate -> Predicate
    goP :: Predicate -> Predicate
goP (Pr [UsedPVar]
ps) = [UsedPVar] -> Predicate
Pr (UsedPVar -> UsedPVar
goPV forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [UsedPVar]
ps)
    goPV :: UsedPVar -> UsedPVar
    goPV :: UsedPVar -> UsedPVar
goPV UsedPVar
pv
      | forall t. PVar t -> Symbol
pname UsedPVar
pv forall a. Eq a => a -> a -> Bool
== forall t. PVar t -> Symbol
pname PVar BSort
src = UsedPVar
pv { pname :: Symbol
pname = forall t. PVar t -> Symbol
pname PVar BSort
dst }
      | Bool
otherwise             = UsedPVar
pv

-------------------------------------------------------------------------------
substPred :: String -> (RPVar, SpecProp) -> SpecType -> SpecType
-------------------------------------------------------------------------------

substPred :: [Char]
-> (RPVar, Ref RSort (RRType RReft))
-> RRType RReft
-> RRType RReft
substPred [Char]
_   (RPVar
rp, RProp [(Symbol, RSort)]
ss (RVar RTyVar
a1 RReft
r1)) t :: RRType RReft
t@(RVar RTyVar
a2 RReft
r2)
  | Bool
isPredInReft Bool -> Bool -> Bool
&& RTyVar
a1 forall a. Eq a => a -> a -> Bool
== RTyVar
a2    = forall c tv r. tv -> r -> RType c tv r
RVar RTyVar
a1 forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) t1 b.
(Foldable t, PPrint t1, Reftable b) =>
t (PVar t1) -> [(Symbol, RSort)] -> b -> b -> b
meetListWithPSubs [UsedPVar]
πs [(Symbol, RSort)]
ss RReft
r1 RReft
r2'
  | Bool
isPredInReft                = forall a. Maybe SrcSpan -> [Char] -> a
panic forall a. Maybe a
Nothing ([Char]
"substPred RVar Var Mismatch" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (RTyVar
a1, RTyVar
a2))
  | Bool
otherwise                   = RRType RReft
t
  where
    (RReft
r2', [UsedPVar]
πs)                   = forall t r. PVar t -> UReft r -> (UReft r, [UsedPVar])
splitRPvar RPVar
rp RReft
r2
    isPredInReft :: Bool
isPredInReft                = Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t a -> Bool
null [UsedPVar]
πs

substPred [Char]
msg su :: (RPVar, Ref RSort (RRType RReft))
su@(RPVar
π, Ref RSort (RRType RReft)
_ ) (RApp RTyCon
c [RRType RReft]
ts [Ref RSort (RRType RReft)]
rs RReft
r)
  | forall (t :: * -> *) a. Foldable t => t a -> Bool
null [UsedPVar]
πs                     = RRType RReft
t'
  | Bool
otherwise                   = forall t t2 tv r.
(PPrint t, PPrint t2, Eq tv, Reftable r, Hashable tv, PPrint tv,
 PPrint r, SubsTy tv (RType RTyCon tv ()) r,
 SubsTy tv (RType RTyCon tv ()) (RType RTyCon tv ()),
 SubsTy tv (RType RTyCon tv ()) RTyCon,
 SubsTy tv (RType RTyCon tv ()) tv, Reftable (RType RTyCon tv r),
 SubsTy tv (RType RTyCon tv ()) (RTVar tv (RType RTyCon tv ())),
 FreeVar RTyCon tv, Reftable (RTProp RTyCon tv r),
 Reftable (RTProp RTyCon tv ())) =>
[Char]
-> (t, Ref RSort (RType RTyCon tv r))
-> RType RTyCon tv r
-> [PVar t2]
-> r
-> RType RTyCon tv r
substRCon [Char]
msg (RPVar, Ref RSort (RRType RReft))
su RRType RReft
t' [UsedPVar]
πs RReft
r2'
  where
    t' :: RRType RReft
t'                          = forall c tv r.
c -> [RType c tv r] -> [RTProp c tv r] -> r -> RType c tv r
RApp RTyCon
c ([Char]
-> (RPVar, Ref RSort (RRType RReft))
-> RRType RReft
-> RRType RReft
substPred [Char]
msg (RPVar, Ref RSort (RRType RReft))
su forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RRType RReft]
ts) ([Char]
-> (RPVar, Ref RSort (RRType RReft))
-> Ref RSort (RRType RReft)
-> Ref RSort (RRType RReft)
substPredP [Char]
msg (RPVar, Ref RSort (RRType RReft))
su forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Ref RSort (RRType RReft)]
rs) RReft
r
    (RReft
r2', [UsedPVar]
πs)                   = forall t r. PVar t -> UReft r -> (UReft r, [UsedPVar])
splitRPvar RPVar
π RReft
r

substPred [Char]
msg (RPVar
p, Ref RSort (RRType RReft)
tp) (RAllP q :: RPVar
q@PV{} RRType RReft
t)
  | RPVar
p forall a. Eq a => a -> a -> Bool
/= RPVar
q                      = forall c tv r. PVU c tv -> RType c tv r -> RType c tv r
RAllP RPVar
q forall a b. (a -> b) -> a -> b
$ [Char]
-> (RPVar, Ref RSort (RRType RReft))
-> RRType RReft
-> RRType RReft
substPred [Char]
msg (RPVar
p, Ref RSort (RRType RReft)
tp) RRType RReft
t
  | Bool
otherwise                   = forall c tv r. PVU c tv -> RType c tv r -> RType c tv r
RAllP RPVar
q RRType RReft
t

substPred [Char]
msg (RPVar, Ref RSort (RRType RReft))
su (RAllT RTVar RTyVar RSort
a RRType RReft
t RReft
r)  = forall c tv r. RTVU c tv -> RType c tv r -> r -> RType c tv r
RAllT RTVar RTyVar RSort
a ([Char]
-> (RPVar, Ref RSort (RRType RReft))
-> RRType RReft
-> RRType RReft
substPred [Char]
msg (RPVar, Ref RSort (RRType RReft))
su RRType RReft
t) RReft
r

substPred [Char]
msg su :: (RPVar, Ref RSort (RRType RReft))
su@(RPVar
rp,Ref RSort (RRType RReft)
prop) (RFun Symbol
x RFInfo
i RRType RReft
rt RRType RReft
rt' RReft
r)
--                        = RFun x (substPred msg su t) (substPred msg su t') r
  | forall (t :: * -> *) a. Foldable t => t a -> Bool
null [UsedPVar]
πs                     = forall c tv r.
Symbol
-> RFInfo -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun Symbol
x RFInfo
i ([Char]
-> (RPVar, Ref RSort (RRType RReft))
-> RRType RReft
-> RRType RReft
substPred [Char]
msg (RPVar, Ref RSort (RRType RReft))
su RRType RReft
rt) ([Char]
-> (RPVar, Ref RSort (RRType RReft))
-> RRType RReft
-> RRType RReft
substPred [Char]
msg (RPVar, Ref RSort (RRType RReft))
su RRType RReft
rt') RReft
r
  | Bool
otherwise                   =
      let sus :: [Subst]
sus = (\UsedPVar
π -> [(Symbol, Expr)] -> Subst
F.mkSubst (forall a b. [a] -> [b] -> [(a, b)]
zip (forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall τ t. Ref τ t -> [(Symbol, τ)]
rf_args Ref RSort (RRType RReft)
prop) (forall a b c. (a, b, c) -> c
thd3 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. PVar t -> [(t, Symbol, Expr)]
pargs UsedPVar
π))) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [UsedPVar]
πs in
      forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\RRType RReft
t Subst
subst -> RRType RReft
t forall r. Reftable r => r -> r -> r
`F.meet` forall a. Subable a => Subst -> a -> a
F.subst Subst
subst (forall τ t. Ref τ t -> t
rf_body Ref RSort (RRType RReft)
prop)) (forall c tv r.
Symbol
-> RFInfo -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun Symbol
x RFInfo
i ([Char]
-> (RPVar, Ref RSort (RRType RReft))
-> RRType RReft
-> RRType RReft
substPred [Char]
msg (RPVar, Ref RSort (RRType RReft))
su RRType RReft
rt) ([Char]
-> (RPVar, Ref RSort (RRType RReft))
-> RRType RReft
-> RRType RReft
substPred [Char]
msg (RPVar, Ref RSort (RRType RReft))
su RRType RReft
rt') RReft
r') [Subst]
sus
  where (RReft
r', [UsedPVar]
πs)                = forall t r. PVar t -> UReft r -> (UReft r, [UsedPVar])
splitRPvar RPVar
rp RReft
r
-- ps has   , pargs :: ![(t, Symbol, Expr)]

substPred [Char]
msg (RPVar, Ref RSort (RRType RReft))
su (RRTy [(Symbol, RRType RReft)]
e RReft
r Oblig
o RRType RReft
t) = forall c tv r.
[(Symbol, RType c tv r)]
-> r -> Oblig -> RType c tv r -> RType c tv r
RRTy (forall b c a. (b -> c) -> (a, b) -> (a, c)
mapSnd ([Char]
-> (RPVar, Ref RSort (RRType RReft))
-> RRType RReft
-> RRType RReft
substPred [Char]
msg (RPVar, Ref RSort (RRType RReft))
su) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, RRType RReft)]
e) RReft
r Oblig
o ([Char]
-> (RPVar, Ref RSort (RRType RReft))
-> RRType RReft
-> RRType RReft
substPred [Char]
msg (RPVar, Ref RSort (RRType RReft))
su RRType RReft
t)
substPred [Char]
msg (RPVar, Ref RSort (RRType RReft))
su (RAllE Symbol
x RRType RReft
t RRType RReft
t') = forall c tv r.
Symbol -> RType c tv r -> RType c tv r -> RType c tv r
RAllE Symbol
x ([Char]
-> (RPVar, Ref RSort (RRType RReft))
-> RRType RReft
-> RRType RReft
substPred [Char]
msg (RPVar, Ref RSort (RRType RReft))
su RRType RReft
t) ([Char]
-> (RPVar, Ref RSort (RRType RReft))
-> RRType RReft
-> RRType RReft
substPred [Char]
msg (RPVar, Ref RSort (RRType RReft))
su RRType RReft
t')
substPred [Char]
msg (RPVar, Ref RSort (RRType RReft))
su (REx Symbol
x RRType RReft
t RRType RReft
t')   = forall c tv r.
Symbol -> RType c tv r -> RType c tv r -> RType c tv r
REx   Symbol
x ([Char]
-> (RPVar, Ref RSort (RRType RReft))
-> RRType RReft
-> RRType RReft
substPred [Char]
msg (RPVar, Ref RSort (RRType RReft))
su RRType RReft
t) ([Char]
-> (RPVar, Ref RSort (RRType RReft))
-> RRType RReft
-> RRType RReft
substPred [Char]
msg (RPVar, Ref RSort (RRType RReft))
su RRType RReft
t')
substPred [Char]
_   (RPVar, Ref RSort (RRType RReft))
_  RRType RReft
t              = RRType RReft
t

-- | Requires: @not $ null πs@
-- substRCon :: String -> (RPVar, SpecType) -> SpecType -> SpecType

substRCon
  :: (PPrint t, PPrint t2, Eq tv, F.Reftable r, Hashable tv, PPrint tv, PPrint r,
      SubsTy tv (RType RTyCon tv ()) r,
      SubsTy tv (RType RTyCon tv ()) (RType RTyCon tv ()),
      SubsTy tv (RType RTyCon tv ()) RTyCon,
      SubsTy tv (RType RTyCon tv ()) tv,
      F.Reftable (RType RTyCon tv r),
      SubsTy tv (RType RTyCon tv ()) (RTVar tv (RType RTyCon tv ())),
      FreeVar RTyCon tv,
      F.Reftable (RTProp RTyCon tv r),
      F.Reftable (RTProp RTyCon tv ()))
  => [Char]
  -> (t, Ref RSort (RType RTyCon tv r))
  -> RType RTyCon tv r
  -> [PVar t2]
  -> r
  -> RType RTyCon tv r
substRCon :: forall t t2 tv r.
(PPrint t, PPrint t2, Eq tv, Reftable r, Hashable tv, PPrint tv,
 PPrint r, SubsTy tv (RType RTyCon tv ()) r,
 SubsTy tv (RType RTyCon tv ()) (RType RTyCon tv ()),
 SubsTy tv (RType RTyCon tv ()) RTyCon,
 SubsTy tv (RType RTyCon tv ()) tv, Reftable (RType RTyCon tv r),
 SubsTy tv (RType RTyCon tv ()) (RTVar tv (RType RTyCon tv ())),
 FreeVar RTyCon tv, Reftable (RTProp RTyCon tv r),
 Reftable (RTProp RTyCon tv ())) =>
[Char]
-> (t, Ref RSort (RType RTyCon tv r))
-> RType RTyCon tv r
-> [PVar t2]
-> r
-> RType RTyCon tv r
substRCon [Char]
msg (t
_, RProp [(Symbol, RSort)]
ss t1 :: RType RTyCon tv r
t1@(RApp RTyCon
c1 [RType RTyCon tv r]
ts1 [RTProp RTyCon tv r]
rs1 r
r1)) t2 :: RType RTyCon tv r
t2@(RApp RTyCon
c2 [RType RTyCon tv r]
ts2 [RTProp RTyCon tv r]
rs2 r
_) [PVar t2]
πs r
r2'
  | RTyCon -> TyCon
rtc_tc RTyCon
c1 forall a. Eq a => a -> a -> Bool
== RTyCon -> TyCon
rtc_tc RTyCon
c2 = forall c tv r.
c -> [RType c tv r] -> [RTProp c tv r] -> r -> RType c tv r
RApp RTyCon
c1 [RType RTyCon tv r]
ts [RTProp RTyCon tv r]
rs forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) t1 b.
(Foldable t, PPrint t1, Reftable b) =>
t (PVar t1) -> [(Symbol, RSort)] -> b -> b -> b
meetListWithPSubs [PVar t2]
πs [(Symbol, RSort)]
ss r
r1 r
r2'
  where
    ts :: [RType RTyCon tv r]
ts                     = forall a. Subable a => Subst -> a -> a
F.subst Subst
su forall a b. (a -> b) -> a -> b
$ forall a b c.
(?callStack::CallStack) =>
[Char] -> (a -> b -> c) -> [a] -> [b] -> [c]
safeZipWith ([Char]
msg forall a. [a] -> [a] -> [a]
++ [Char]
": substRCon")  forall r. Reftable r => r -> r -> r
strSub  [RType RTyCon tv r]
ts1  [RType RTyCon tv r]
ts2
    rs :: [RTProp RTyCon tv r]
rs                     = forall a. Subable a => Subst -> a -> a
F.subst Subst
su forall a b. (a -> b) -> a -> b
$ forall a b c.
(?callStack::CallStack) =>
[Char] -> (a -> b -> c) -> [a] -> [b] -> [c]
safeZipWith ([Char]
msg forall a. [a] -> [a] -> [a]
++ [Char]
": substRCon2") forall {t1} {t2} {t3} {τ}.
Reftable (RType t1 t2 t3) =>
Ref τ (RType t1 t2 t3)
-> Ref τ (RType t1 t2 t3) -> Ref τ (RType t1 t2 t3)
strSubR [RTProp RTyCon tv r]
rs1' [RTProp RTyCon tv r]
rs2'
    ([RTProp RTyCon tv r]
rs1', [RTProp RTyCon tv r]
rs2')           = forall a. [Char] -> (a -> a) -> [a] -> [a] -> ([a], [a])
pad [Char]
"substRCon" forall r. Reftable r => r -> r
F.top [RTProp RTyCon tv r]
rs1 [RTProp RTyCon tv r]
rs2
    strSub :: b -> b -> b
strSub b
x b
r2           = forall (t :: * -> *) t1 b.
(Foldable t, PPrint t1, Reftable b) =>
t (PVar t1) -> [(Symbol, RSort)] -> b -> b -> b
meetListWithPSubs [PVar t2]
πs [(Symbol, RSort)]
ss b
x b
r2
    strSubR :: Ref τ (RType t1 t2 t3)
-> Ref τ (RType t1 t2 t3) -> Ref τ (RType t1 t2 t3)
strSubR Ref τ (RType t1 t2 t3)
x Ref τ (RType t1 t2 t3)
r2          = forall (t :: * -> *) t1 t2 t3 t4 b τ.
(Foldable t, Reftable (RType t1 t2 t3)) =>
t (PVar t4)
-> [(Symbol, b)]
-> Ref τ (RType t1 t2 t3)
-> Ref τ (RType t1 t2 t3)
-> Ref τ (RType t1 t2 t3)
meetListWithPSubsRef [PVar t2]
πs [(Symbol, RSort)]
ss Ref τ (RType t1 t2 t3)
x Ref τ (RType t1 t2 t3)
r2

    su :: Subst
su = [(Symbol, Expr)] -> Subst
F.mkSubst forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\Symbol
s1 Symbol
s2 -> (Symbol
s1, Symbol -> Expr
F.EVar Symbol
s2)) (forall {tv}. RType RTyCon tv r -> [Symbol]
rvs RType RTyCon tv r
t1) (forall {tv}. RType RTyCon tv r -> [Symbol]
rvs RType RTyCon tv r
t2)

    rvs :: RType RTyCon tv r -> [Symbol]
rvs      = forall r c tv a.
(Reftable r, TyConable c) =>
Bool
-> (SEnv (RType c tv r) -> r -> a -> a) -> a -> RType c tv r -> a
foldReft Bool
False (\SEnv (RType RTyCon tv r)
_ r
r [Symbol]
acc -> forall {p}. Reftable p => p -> Symbol
rvReft r
r forall a. a -> [a] -> [a]
: [Symbol]
acc) []
    rvReft :: p -> Symbol
rvReft p
r = let F.Reft(Symbol
s,Expr
_) = forall r. Reftable r => r -> Reft
F.toReft p
r in Symbol
s

substRCon [Char]
msg (t, Ref RSort (RType RTyCon tv r))
su RType RTyCon tv r
t [PVar t2]
_ r
_        = {- panic Nothing -} forall a. [Char] -> [Char] -> a
errorP [Char]
"substRCon: " forall a b. (a -> b) -> a -> b
$ [Char]
msg forall a. [a] -> [a] -> [a]
++ [Char]
" " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
showpp ((t, Ref RSort (RType RTyCon tv r))
su, RType RTyCon tv r
t)

pad :: [Char] -> (a -> a) -> [a] -> [a] -> ([a], [a])
pad :: forall a. [Char] -> (a -> a) -> [a] -> [a] -> ([a], [a])
pad [Char]
_ a -> a
f [] [a]
ys   = (a -> a
f forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [a]
ys, [a]
ys)
pad [Char]
_ a -> a
f [a]
xs []   = ([a]
xs, a -> a
f forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [a]
xs)
pad [Char]
msg a -> a
_ [a]
xs [a]
ys
  | Int
nxs forall a. Eq a => a -> a -> Bool
== Int
nys  = ([a]
xs, [a]
ys)
  | Bool
otherwise   = forall a. Maybe SrcSpan -> [Char] -> a
panic forall a. Maybe a
Nothing forall a b. (a -> b) -> a -> b
$ [Char]
"pad: " forall a. [a] -> [a] -> [a]
++ [Char]
msg
  where
    nxs :: Int
nxs         = forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
xs
    nys :: Int
nys         = forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
ys

substPredP :: [Char]
           -> (RPVar, Ref RSort (RRType RReft))
           -> Ref RSort (RType RTyCon RTyVar RReft)
           -> Ref RSort SpecType
substPredP :: [Char]
-> (RPVar, Ref RSort (RRType RReft))
-> Ref RSort (RRType RReft)
-> Ref RSort (RRType RReft)
substPredP [Char]
_ (RPVar, Ref RSort (RRType RReft))
su p :: Ref RSort (RRType RReft)
p@(RProp [(Symbol, RSort)]
_ (RHole RReft
_))
  = forall a. Maybe SrcSpan -> [Char] -> a
panic forall a. Maybe a
Nothing ([Char]
"PredType.substPredP1 called on invalid inputs: " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
showpp ((RPVar, Ref RSort (RRType RReft))
su, Ref RSort (RRType RReft)
p))
substPredP [Char]
msg (RPVar
p, RProp [(Symbol, RSort)]
ss RRType RReft
prop) (RProp [(Symbol, RSort)]
s RRType RReft
t)
  = forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp [(Symbol, RSort)]
ss' forall a b. (a -> b) -> a -> b
$ [Char]
-> (RPVar, Ref RSort (RRType RReft))
-> RRType RReft
-> RRType RReft
substPred ([Char]
msg forall a. [a] -> [a] -> [a]
++ [Char]
": substPredP") (RPVar
p, forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp [(Symbol, RSort)]
ss {- (subst su prop) -} RRType RReft
prop ) RRType RReft
t
 where
   ss' :: [(Symbol, RSort)]
ss' = forall a. Int -> [a] -> [a]
drop Int
n [(Symbol, RSort)]
ss forall a. [a] -> [a] -> [a]
++  [(Symbol, RSort)]
s
   n :: Int
n   = forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Symbol, RSort)]
ss forall a. Num a => a -> a -> a
- forall (t :: * -> *) a. Foldable t => t a -> Int
length (forall t t1 t2.
PVar (RType t t1 ()) -> RType t t1 (UReft t2) -> [Symbol]
freeArgsPs RPVar
p RRType RReft
t)
   -- su  = mkSubst (zip (fst <$> ss) (EVar . fst <$> ss'))


splitRPvar :: PVar t -> UReft r -> (UReft r, [UsedPVar])
splitRPvar :: forall t r. PVar t -> UReft r -> (UReft r, [UsedPVar])
splitRPvar PVar t
pv (MkUReft r
x (Pr [UsedPVar]
pvs)) = (forall r. r -> Predicate -> UReft r
MkUReft r
x ([UsedPVar] -> Predicate
Pr [UsedPVar]
pvs'), [UsedPVar]
epvs)
  where
    ([UsedPVar]
epvs, [UsedPVar]
pvs')               = forall a. (a -> Bool) -> [a] -> ([a], [a])
L.partition (forall t. PVar t -> UsedPVar
uPVar PVar t
pv forall a. Eq a => a -> a -> Bool
==) [UsedPVar]
pvs

-- TODO: rewrite using foldReft
freeArgsPs :: PVar (RType t t1 ()) -> RType t t1 (UReft t2) -> [F.Symbol]
freeArgsPs :: forall t t1 t2.
PVar (RType t t1 ()) -> RType t t1 (UReft t2) -> [Symbol]
freeArgsPs PVar (RType t t1 ())
p (RVar t1
_ UReft t2
r)
  = forall t1 t. PVar t1 -> UReft t -> [Symbol]
freeArgsPsRef PVar (RType t t1 ())
p UReft t2
r
freeArgsPs PVar (RType t t1 ())
p (RFun Symbol
_ RFInfo
_ RType t t1 (UReft t2)
t1 RType t t1 (UReft t2)
t2 UReft t2
r)
  = forall a. Eq a => [a] -> [a]
L.nub forall a b. (a -> b) -> a -> b
$  forall t1 t. PVar t1 -> UReft t -> [Symbol]
freeArgsPsRef PVar (RType t t1 ())
p UReft t2
r forall a. [a] -> [a] -> [a]
++ forall t t1 t2.
PVar (RType t t1 ()) -> RType t t1 (UReft t2) -> [Symbol]
freeArgsPs PVar (RType t t1 ())
p RType t t1 (UReft t2)
t1 forall a. [a] -> [a] -> [a]
++ forall t t1 t2.
PVar (RType t t1 ()) -> RType t t1 (UReft t2) -> [Symbol]
freeArgsPs PVar (RType t t1 ())
p RType t t1 (UReft t2)
t2
freeArgsPs PVar (RType t t1 ())
p (RAllT RTVU t t1
_ RType t t1 (UReft t2)
t UReft t2
r)
  = forall a. Eq a => [a] -> [a]
L.nub forall a b. (a -> b) -> a -> b
$  forall t t1 t2.
PVar (RType t t1 ()) -> RType t t1 (UReft t2) -> [Symbol]
freeArgsPs PVar (RType t t1 ())
p RType t t1 (UReft t2)
t forall a. [a] -> [a] -> [a]
++ forall t1 t. PVar t1 -> UReft t -> [Symbol]
freeArgsPsRef PVar (RType t t1 ())
p UReft t2
r
freeArgsPs PVar (RType t t1 ())
p (RAllP PVar (RType t t1 ())
p' RType t t1 (UReft t2)
t)
  | PVar (RType t t1 ())
p forall a. Eq a => a -> a -> Bool
== PVar (RType t t1 ())
p'   = []
  | Bool
otherwise = forall t t1 t2.
PVar (RType t t1 ()) -> RType t t1 (UReft t2) -> [Symbol]
freeArgsPs PVar (RType t t1 ())
p RType t t1 (UReft t2)
t
freeArgsPs PVar (RType t t1 ())
p (RApp t
_ [RType t t1 (UReft t2)]
ts [RTProp t t1 (UReft t2)]
_ UReft t2
r)
  = forall a. Eq a => [a] -> [a]
L.nub forall a b. (a -> b) -> a -> b
$ forall t1 t. PVar t1 -> UReft t -> [Symbol]
freeArgsPsRef PVar (RType t t1 ())
p UReft t2
r forall a. [a] -> [a] -> [a]
++ forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (forall t t1 t2.
PVar (RType t t1 ()) -> RType t t1 (UReft t2) -> [Symbol]
freeArgsPs PVar (RType t t1 ())
p) [RType t t1 (UReft t2)]
ts
freeArgsPs PVar (RType t t1 ())
p (RAllE Symbol
_ RType t t1 (UReft t2)
t1 RType t t1 (UReft t2)
t2)
  = forall a. Eq a => [a] -> [a]
L.nub forall a b. (a -> b) -> a -> b
$ forall t t1 t2.
PVar (RType t t1 ()) -> RType t t1 (UReft t2) -> [Symbol]
freeArgsPs PVar (RType t t1 ())
p RType t t1 (UReft t2)
t1 forall a. [a] -> [a] -> [a]
++ forall t t1 t2.
PVar (RType t t1 ()) -> RType t t1 (UReft t2) -> [Symbol]
freeArgsPs PVar (RType t t1 ())
p RType t t1 (UReft t2)
t2
freeArgsPs PVar (RType t t1 ())
p (REx Symbol
_ RType t t1 (UReft t2)
t1 RType t t1 (UReft t2)
t2)
  = forall a. Eq a => [a] -> [a]
L.nub forall a b. (a -> b) -> a -> b
$ forall t t1 t2.
PVar (RType t t1 ()) -> RType t t1 (UReft t2) -> [Symbol]
freeArgsPs PVar (RType t t1 ())
p RType t t1 (UReft t2)
t1 forall a. [a] -> [a] -> [a]
++ forall t t1 t2.
PVar (RType t t1 ()) -> RType t t1 (UReft t2) -> [Symbol]
freeArgsPs PVar (RType t t1 ())
p RType t t1 (UReft t2)
t2
freeArgsPs PVar (RType t t1 ())
p (RAppTy RType t t1 (UReft t2)
t1 RType t t1 (UReft t2)
t2 UReft t2
r)
  = forall a. Eq a => [a] -> [a]
L.nub forall a b. (a -> b) -> a -> b
$ forall t1 t. PVar t1 -> UReft t -> [Symbol]
freeArgsPsRef PVar (RType t t1 ())
p UReft t2
r forall a. [a] -> [a] -> [a]
++ forall t t1 t2.
PVar (RType t t1 ()) -> RType t t1 (UReft t2) -> [Symbol]
freeArgsPs PVar (RType t t1 ())
p RType t t1 (UReft t2)
t1 forall a. [a] -> [a] -> [a]
++ forall t t1 t2.
PVar (RType t t1 ()) -> RType t t1 (UReft t2) -> [Symbol]
freeArgsPs PVar (RType t t1 ())
p RType t t1 (UReft t2)
t2
freeArgsPs PVar (RType t t1 ())
_ (RExprArg Located Expr
_)
  = []
freeArgsPs PVar (RType t t1 ())
p (RHole UReft t2
r)
  = forall t1 t. PVar t1 -> UReft t -> [Symbol]
freeArgsPsRef PVar (RType t t1 ())
p UReft t2
r
freeArgsPs PVar (RType t t1 ())
p (RRTy [(Symbol, RType t t1 (UReft t2))]
env UReft t2
r Oblig
_ RType t t1 (UReft t2)
t)
  = forall a. Eq a => [a] -> [a]
L.nub forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (forall t t1 t2.
PVar (RType t t1 ()) -> RType t t1 (UReft t2) -> [Symbol]
freeArgsPs PVar (RType t t1 ())
p) (forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, RType t t1 (UReft t2))]
env) forall a. [a] -> [a] -> [a]
++ forall t1 t. PVar t1 -> UReft t -> [Symbol]
freeArgsPsRef PVar (RType t t1 ())
p UReft t2
r forall a. [a] -> [a] -> [a]
++ forall t t1 t2.
PVar (RType t t1 ()) -> RType t t1 (UReft t2) -> [Symbol]
freeArgsPs PVar (RType t t1 ())
p RType t t1 (UReft t2)
t

freeArgsPsRef :: PVar t1 -> UReft t -> [F.Symbol]
freeArgsPsRef :: forall t1 t. PVar t1 -> UReft t -> [Symbol]
freeArgsPsRef PVar t1
p (MkUReft t
_ (Pr [UsedPVar]
ps)) = [Symbol
x | (()
_, Symbol
x, Expr
w) <- forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap forall t. PVar t -> [(t, Symbol, Expr)]
pargs [UsedPVar]
ps', Symbol -> Expr
F.EVar Symbol
x forall a. Eq a => a -> a -> Bool
== Expr
w]
  where
   ps' :: [UsedPVar]
ps' = UsedPVar -> UsedPVar
f forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. (a -> Bool) -> [a] -> [a]
filter (forall t. PVar t -> UsedPVar
uPVar PVar t1
p forall a. Eq a => a -> a -> Bool
==) [UsedPVar]
ps
   f :: UsedPVar -> UsedPVar
f UsedPVar
q = UsedPVar
q {pargs :: [((), Symbol, Expr)]
pargs = forall t. PVar t -> [(t, Symbol, Expr)]
pargs UsedPVar
q forall a. [a] -> [a] -> [a]
++ forall a. Int -> [a] -> [a]
drop (forall (t :: * -> *) a. Foldable t => t a -> Int
length (forall t. PVar t -> [(t, Symbol, Expr)]
pargs UsedPVar
q)) (forall t. PVar t -> [(t, Symbol, Expr)]
pargs forall a b. (a -> b) -> a -> b
$ forall t. PVar t -> UsedPVar
uPVar PVar t1
p)}

meetListWithPSubs :: (Foldable t, PPrint t1, F.Reftable b)
                  => t (PVar t1) -> [(F.Symbol, RSort)] -> b -> b -> b
meetListWithPSubs :: forall (t :: * -> *) t1 b.
(Foldable t, PPrint t1, Reftable b) =>
t (PVar t1) -> [(Symbol, RSort)] -> b -> b -> b
meetListWithPSubs t (PVar t1)
πs [(Symbol, RSort)]
ss b
r1 b
r2    = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' (forall r t.
(Reftable r, PPrint t) =>
[(Symbol, RSort)] -> r -> r -> PVar t -> r
meetListWithPSub [(Symbol, RSort)]
ss b
r1) b
r2 t (PVar t1)
πs

meetListWithPSubsRef :: (Foldable t, F.Reftable (RType t1 t2 t3))
                     => t (PVar t4)
                     -> [(F.Symbol, b)]
                     -> Ref τ (RType t1 t2 t3)
                     -> Ref τ (RType t1 t2 t3)
                     -> Ref τ (RType t1 t2 t3)
meetListWithPSubsRef :: forall (t :: * -> *) t1 t2 t3 t4 b τ.
(Foldable t, Reftable (RType t1 t2 t3)) =>
t (PVar t4)
-> [(Symbol, b)]
-> Ref τ (RType t1 t2 t3)
-> Ref τ (RType t1 t2 t3)
-> Ref τ (RType t1 t2 t3)
meetListWithPSubsRef t (PVar t4)
πs [(Symbol, b)]
ss Ref τ (RType t1 t2 t3)
r1 Ref τ (RType t1 t2 t3)
r2 = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' (forall t t1 t2 b τ t3.
Reftable (RType t t1 t2) =>
[(Symbol, b)]
-> Ref τ (RType t t1 t2)
-> Ref τ (RType t t1 t2)
-> PVar t3
-> Ref τ (RType t t1 t2)
meetListWithPSubRef [(Symbol, b)]
ss Ref τ (RType t1 t2 t3)
r1) Ref τ (RType t1 t2 t3)
r2 t (PVar t4)
πs

meetListWithPSub ::  (F.Reftable r, PPrint t) => [(F.Symbol, RSort)]-> r -> r -> PVar t -> r
meetListWithPSub :: forall r t.
(Reftable r, PPrint t) =>
[(Symbol, RSort)] -> r -> r -> PVar t -> r
meetListWithPSub [(Symbol, RSort)]
ss r
r1 r
r2 PVar t
π
  | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\(t
_, Symbol
x, F.EVar Symbol
y) -> Symbol
x forall a. Eq a => a -> a -> Bool
== Symbol
y) (forall t. PVar t -> [(t, Symbol, Expr)]
pargs PVar t
π)
  = r
r2 forall r. Reftable r => r -> r -> r
`F.meet` r
r1
  | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\(t
_, Symbol
x, F.EVar Symbol
y) -> Symbol
x forall a. Eq a => a -> a -> Bool
/= Symbol
y) (forall t. PVar t -> [(t, Symbol, Expr)]
pargs PVar t
π)
  = r
r2 forall r. Reftable r => r -> r -> r
`F.meet` forall a. Subable a => Subst -> a -> a
F.subst Subst
su r
r1
  | Bool
otherwise
  = forall a. Maybe SrcSpan -> [Char] -> a
panic forall a. Maybe a
Nothing forall a b. (a -> b) -> a -> b
$ [Char]
"PredType.meetListWithPSub partial application to " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
showpp PVar t
π
  where
    su :: Subst
su  = [(Symbol, Expr)] -> Subst
F.mkSubst [(Symbol
x, Expr
y) | (Symbol
x, (t
_, Symbol
_, Expr
y)) <- forall a b. [a] -> [b] -> [(a, b)]
zip (forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, RSort)]
ss) (forall t. PVar t -> [(t, Symbol, Expr)]
pargs PVar t
π)]

meetListWithPSubRef :: (F.Reftable (RType t t1 t2))
                    => [(F.Symbol, b)]
                    -> Ref τ (RType t t1 t2)
                    -> Ref τ (RType t t1 t2)
                    -> PVar t3
                    -> Ref τ (RType t t1 t2)
meetListWithPSubRef :: forall t t1 t2 b τ t3.
Reftable (RType t t1 t2) =>
[(Symbol, b)]
-> Ref τ (RType t t1 t2)
-> Ref τ (RType t t1 t2)
-> PVar t3
-> Ref τ (RType t t1 t2)
meetListWithPSubRef [(Symbol, b)]
_ (RProp [(Symbol, τ)]
_ (RHole t2
_)) Ref τ (RType t t1 t2)
_ PVar t3
_ -- TODO: Is this correct?
  = forall a. Maybe SrcSpan -> [Char] -> a
panic forall a. Maybe a
Nothing [Char]
"PredType.meetListWithPSubRef called with invalid input"
meetListWithPSubRef [(Symbol, b)]
_ Ref τ (RType t t1 t2)
_ (RProp [(Symbol, τ)]
_ (RHole t2
_)) PVar t3
_
  = forall a. Maybe SrcSpan -> [Char] -> a
panic forall a. Maybe a
Nothing [Char]
"PredType.meetListWithPSubRef called with invalid input"
meetListWithPSubRef [(Symbol, b)]
ss (RProp [(Symbol, τ)]
s1 RType t t1 t2
r1) (RProp [(Symbol, τ)]
s2 RType t t1 t2
r2) PVar t3
π
  | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\(t3
_, Symbol
x, F.EVar Symbol
y) -> Symbol
x forall a. Eq a => a -> a -> Bool
== Symbol
y) (forall t. PVar t -> [(t, Symbol, Expr)]
pargs PVar t3
π)
  = forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp [(Symbol, τ)]
s1 forall a b. (a -> b) -> a -> b
$ forall a. Subable a => Subst -> a -> a
F.subst Subst
su' RType t t1 t2
r2 forall r. Reftable r => r -> r -> r
`F.meet` RType t t1 t2
r1
  | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\(t3
_, Symbol
x, F.EVar Symbol
y) -> Symbol
x forall a. Eq a => a -> a -> Bool
/= Symbol
y) (forall t. PVar t -> [(t, Symbol, Expr)]
pargs PVar t3
π)
  = forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp [(Symbol, τ)]
s2 forall a b. (a -> b) -> a -> b
$ RType t t1 t2
r2 forall r. Reftable r => r -> r -> r
`F.meet` forall a. Subable a => Subst -> a -> a
F.subst Subst
su RType t t1 t2
r1
  | Bool
otherwise
  = forall a. Maybe SrcSpan -> [Char] -> a
panic forall a. Maybe a
Nothing forall a b. (a -> b) -> a -> b
$ [Char]
"PredType.meetListWithPSubRef partial application to " forall a. [a] -> [a] -> [a]
++ forall a. PPrint a => a -> [Char]
showpp PVar t3
π
  where
    su :: Subst
su  = [(Symbol, Expr)] -> Subst
F.mkSubst [(Symbol
x, Expr
y) | (Symbol
x, (t3
_, Symbol
_, Expr
y)) <- forall a b. [a] -> [b] -> [(a, b)]
zip (forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, b)]
ss) (forall t. PVar t -> [(t, Symbol, Expr)]
pargs PVar t3
π)]
    su' :: Subst
su' = [(Symbol, Expr)] -> Subst
F.mkSubst [(Symbol
x, Symbol -> Expr
F.EVar Symbol
y) | (Symbol
x, Symbol
y) <- forall a b. [a] -> [b] -> [(a, b)]
zip (forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, τ)]
s2) (forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, τ)]
s1)]


----------------------------------------------------------------------------
-- | Interface: Modified CoreSyn.exprType due to predApp -------------------
----------------------------------------------------------------------------
predType   :: Type
predType :: Type
predType   = Symbol -> Type
symbolType Symbol
predName

wpredName, predName :: F.Symbol
predName :: Symbol
predName   = Symbol
"Pred"
wpredName :: Symbol
wpredName  = Symbol
"WPred"

symbolType :: F.Symbol -> Type
symbolType :: Symbol -> Type
symbolType = TyVar -> Type
TyVarTy forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> TyVar
symbolTyVar


substParg :: Functor f => (F.Symbol, F.Expr) -> f Predicate -> f Predicate
substParg :: forall (f :: * -> *).
Functor f =>
(Symbol, Expr) -> f Predicate -> f Predicate
substParg (Symbol
x, Expr
y) = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Predicate -> Predicate
fp
  where
    fxy :: Expr -> Expr
fxy Expr
s        = if Expr
s forall a. Eq a => a -> a -> Bool
== Symbol -> Expr
F.EVar Symbol
x then Expr
y else Expr
s
    fp :: Predicate -> Predicate
fp           = (UsedPVar -> UsedPVar) -> Predicate -> Predicate
subvPredicate (\UsedPVar
pv -> UsedPVar
pv { pargs :: [((), Symbol, Expr)]
pargs = forall t t3 t1 t2. (t -> t3) -> (t1, t2, t) -> (t1, t2, t3)
mapThd3 Expr -> Expr
fxy forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall t. PVar t -> [(t, Symbol, Expr)]
pargs UsedPVar
pv })

-------------------------------------------------------------------------------
-----------------------------  Predicate Application --------------------------
-------------------------------------------------------------------------------
pappArity :: Int
pappArity :: Int
pappArity  = Int
7

pappSort :: Int -> F.Sort
pappSort :: Int -> Sort
pappSort Int
n = Int -> [Sort] -> Sort
F.mkFFunc (Int
2 forall a. Num a => a -> a -> a
* Int
n) forall a b. (a -> b) -> a -> b
$ [Sort
ptycon] forall a. [a] -> [a] -> [a]
++ [Sort]
args forall a. [a] -> [a] -> [a]
++ [Sort
F.boolSort]
  where
    ptycon :: Sort
ptycon = FTycon -> [Sort] -> Sort
F.fAppTC FTycon
predFTyCon forall a b. (a -> b) -> a -> b
$ Int -> Sort
F.FVar forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Int
0..Int
nforall a. Num a => a -> a -> a
-Int
1]
    args :: [Sort]
args   = Int -> Sort
F.FVar forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Int
n..(Int
2forall a. Num a => a -> a -> a
*Int
nforall a. Num a => a -> a -> a
-Int
1)]


predFTyCon :: F.FTycon
predFTyCon :: FTycon
predFTyCon = LocSymbol -> FTycon
F.symbolFTycon forall a b. (a -> b) -> a -> b
$ forall a. a -> Located a
dummyLoc Symbol
predName