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

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

module Language.Haskell.Liquid.Types.PredType (
    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           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.DataDecl
import           Language.Haskell.Liquid.Types.Errors
import           Language.Haskell.Liquid.Types.Names
import           Language.Haskell.Liquid.Types.RefType hiding (generalize)
import           Language.Haskell.Liquid.Types.RType
import           Language.Haskell.Liquid.Types.RTypeOp
import           Language.Haskell.Liquid.Types.Types

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         = [(TyCon, RTyCon)] -> HashMap TyCon RTyCon
forall k v. 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     = [Char] -> [(TyCon, Int)] -> HashMap TyCon Int
forall k v.
(HasCallStack, Eq k, Hashable k, Show k) =>
[Char] -> [(k, v)] -> HashMap k v
safeFromList [Char]
"makeTyConInfo" [ (TyCon
c, [Sort] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Sort]
ts) | (TyCon
c, [Sort]
ts) <- HashMap (TyCon, [Sort]) RTyCon -> [(TyCon, [Sort])]
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 = [((TyCon, [Sort]), RTyCon)] -> HashMap (TyCon, [Sort]) RTyCon
forall k v. Hashable k => [(k, v)] -> HashMap k v
M.fromList
  [ ((TyCon
c, TCEmb TyCon -> Type -> Sort
typeSort TCEmb TyCon
tce (Type -> Sort) -> [Type] -> [Sort]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Type]
ts), RTyCon
rtc)
    | TyCon
fiTc    <- [TyCon]
fiTcs
    , RTyCon
rtc     <- Maybe RTyCon -> [RTyCon]
forall a. Maybe a -> [a]
Mb.maybeToList (TyCon -> HashMap TyCon RTyCon -> Maybe RTyCon
forall k v. Hashable k => k -> HashMap k v -> Maybe v
M.lookup TyCon
fiTc HashMap TyCon RTyCon
tcm)
    , (TyCon
c, [Type]
ts) <- Maybe (TyCon, [Type]) -> [(TyCon, [Type])]
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   = [TyVar -> RSort
forall r c. IsReft r => TyVar -> RType c RTyVar r
rVar TyVar
α :: RSort |  TyVar
α <- TyCon -> [TyVar]
tyConTyVarsDef TyCon
tc]
    pvs' :: [RPVar]
pvs' = [(RTyVar, RSort)] -> RPVar -> RPVar
forall tv ty c. SubsTy tv ty c => [(tv, ty)] -> c -> c
subts ([RTyVar] -> [RSort] -> [(RTyVar, RSort)]
forall a b. [a] -> [b] -> [(a, b)]
zip [RTyVar]
αs' [RSort]
τs) (RPVar -> RPVar) -> [RPVar] -> [RPVar]
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    = RTypeRepBV Symbol Symbol RTyCon RTyVar RReft -> RRType RReft
forall b v c tv r. RTypeRepBV b v c tv r -> RTypeBV b v c tv r
fromRTypeRep (DataCon
-> RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
meetWorkWrapRep DataCon
c RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
wkR RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
wrR)
  where
    wkR :: RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
wkR                 = DataCon -> RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
dataConWorkRep DataCon
c
    wrR :: RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
wrR                 = RRType RReft -> RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
forall b v c tv r. RTypeBV b v c tv r -> RTypeRepBV b v c tv r
toRTypeRep RRType RReft
wrT

dataConWorkRep :: DataCon -> SpecRep
dataConWorkRep :: DataCon -> RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
dataConWorkRep DataCon
c = RRType RReft -> RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
forall b v c tv r. RTypeBV b v c tv r -> RTypeRepBV b v c tv r
toRTypeRep
                 -- . F.tracepp ("DCWR-2: " ++ F.showpp c)
                 (RRType RReft -> RTypeRepBV Symbol Symbol RTyCon RTyVar RReft)
-> (DataCon -> RRType RReft)
-> DataCon
-> RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> RRType RReft
forall r. IsReft r => Type -> RRType r
ofType
                 -- . F.tracepp ("DCWR-1: " ++ F.showpp c)
                 (Type -> RRType RReft)
-> (DataCon -> Type) -> DataCon -> RRType RReft
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataCon -> Type
dataConRepType
                 -- . Var.varType
                 -- . dataConWorkId
                 (DataCon -> RTypeRepBV Symbol Symbol RTyCon RTyVar RReft)
-> DataCon -> RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
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
-> RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
-> RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
meetWorkWrapRep DataCon
c RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
workR RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
wrapR
  | Int
0 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
pad'
  = RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
workR { ty_binds = xs ++ ty_binds wrapR
          , ty_args  = ts ++ zipWith meet ts' (ty_args wrapR)
          , ty_res   = strengthenRType (ty_res workR)    (ty_res  wrapR)
          , ty_preds = ty_preds wrapR
          }
  | Bool
otherwise
  = Maybe SrcSpan
-> [Char] -> RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
forall a. HasCallStack => Maybe SrcSpan -> [Char] -> a
panic (SrcSpan -> Maybe SrcSpan
forall a. a -> Maybe a
Just (DataCon -> SrcSpan
forall a. NamedThing a => a -> SrcSpan
getSrcSpan DataCon
c)) [Char]
errMsg
  where
    pad' :: Int
pad'      = {- F.tracepp ("MEETWKRAP: " ++ show (ty_vars workR)) $ -} Int
workN Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
wrapN
    ([Symbol]
xs, [Symbol]
_)   = Int -> [Symbol] -> ([Symbol], [Symbol])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
pad' (RTypeRepBV Symbol Symbol RTyCon RTyVar RReft -> [Symbol]
forall b v c tv r. RTypeRepBV b v c tv r -> [b]
ty_binds RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
workR)
    ([RRType RReft]
ts, [RRType RReft]
ts') = Int -> [RRType RReft] -> ([RRType RReft], [RRType RReft])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
pad' (RTypeRepBV Symbol Symbol RTyCon RTyVar RReft -> [RRType RReft]
forall b v c tv r. RTypeRepBV b v c tv r -> [RTypeBV b v c tv r]
ty_args  RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
workR)
    workN :: Int
workN     = [RRType RReft] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length      (RTypeRepBV Symbol Symbol RTyCon RTyVar RReft -> [RRType RReft]
forall b v c tv r. RTypeRepBV b v c tv r -> [RTypeBV b v c tv r]
ty_args  RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
workR)
    wrapN :: Int
wrapN     = [RRType RReft] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length      (RTypeRepBV Symbol Symbol RTyCon RTyVar RReft -> [RRType RReft]
forall b v c tv r. RTypeRepBV b v c tv r -> [RTypeBV b v c tv r]
ty_args  RTypeRepBV Symbol Symbol RTyCon RTyVar RReft
wrapR)
    errMsg :: [Char]
errMsg    = [Char]
"Unsupported Work/Wrap types for Data Constructor " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ DataCon -> [Char]
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 = RRType RReft
-> (RReft -> RRType RReft) -> Maybe RReft -> RRType RReft
forall b a. b -> (a -> b) -> Maybe a -> b
maybe RRType RReft
wkT (RRType RReft -> RReft -> RRType RReft
forall r b v c tv.
Meet r =>
RTypeBV b v c tv r -> r -> RTypeBV b v c tv r
strengthen RRType RReft
wkT) (RRType RReft -> Maybe RReft
forall b v c tv r. RTypeBV b v 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 [(LHName, RRType RReft)]
yts RRType RReft
rt Bool
_ Symbol
_ SourcePos
_)
  = {- F.tracepp ("dcWrapSpecType: " ++ show dc ++ " " ++ F.showpp rt) $ -}
    [(RTVar RTyVar RSort, RReft)]
-> [RPVar]
-> [(Symbol, RFInfo, RRType RReft, RReft)]
-> RRType RReft
-> RRType RReft
forall tv b v c r.
[(RTVar tv (RTypeBV b v c tv (NoReftB b)), r)]
-> [PVarBV b v (RTypeBV b v c tv (NoReftB b))]
-> [(b, RFInfo, RTypeBV b v c tv r, r)]
-> RTypeBV b v c tv r
-> RTypeBV b v c tv r
mkArrow [(RTVar RTyVar RSort, RReft)]
makeVars' [RPVar]
ps [(Symbol, RFInfo, RRType RReft, RReft)]
ts' RRType RReft
rt'
  where
    isCls :: Bool
isCls    = TyCon -> Bool
Ghc.isClassTyCon (TyCon -> Bool) -> TyCon -> Bool
forall a b. (a -> b) -> a -> b
$ DataCon -> TyCon
Ghc.dataConTyCon DataCon
dc
    ([LHName]
as0, [RRType RReft]
sts) = [(LHName, RRType RReft)] -> ([LHName], [RRType RReft])
forall a b. [(a, b)] -> ([a], [b])
unzip ([(LHName, RRType RReft)] -> [(LHName, RRType RReft)]
forall a. [a] -> [a]
reverse [(LHName, RRType RReft)]
yts)
    as :: [Symbol]
as = (LHName -> Symbol) -> [LHName] -> [Symbol]
forall a b. (a -> b) -> [a] -> [b]
map LHName -> Symbol
lhNameToResolvedSymbol [LHName]
as0
    as1 :: [Symbol]
as1 = (LHName -> Symbol) -> [LHName] -> [Symbol]
forall a b. (a -> b) -> [a] -> [b]
map HasCallStack => LHName -> Symbol
LHName -> Symbol
lhNameToUnqualifiedSymbol [LHName]
as0
    mkDSym :: a -> Symbol
mkDSym a
z = a -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol a
z Symbol -> Symbol -> Symbol
`F.suffixSymbol` DataCon -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol DataCon
dc
    bs :: [Symbol]
bs       = Symbol -> Symbol
forall a. Symbolic a => a -> Symbol
mkDSym (Symbol -> Symbol) -> [Symbol] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol]
as
    tx :: [(Variable c, ExprBV (Variable c) (Variable c))]
-> [Variable c]
-> [Variable c]
-> [c]
-> [(Variable c, RFInfo, c, d)]
tx [(Variable c, ExprBV (Variable c) (Variable c))]
_  []     []     []     = []
    tx [(Variable c, ExprBV (Variable c) (Variable c))]
su (Variable c
x:[Variable c]
xs) (Variable c
y:[Variable c]
ys) (c
t:[c]
ts) = (Variable c
y, Bool -> RFInfo
classRFInfo Bool
allowTC , if Bool
allowTC Bool -> Bool -> Bool
&& Bool
isCls then c
t else SubstV (Variable c) -> c -> c
forall a.
(Subable a, HasCallStack) =>
SubstV (Variable a) -> a -> a
F.subst ([(Variable c, ExprBV (Variable c) (Variable c))]
-> SubstV (Variable c)
forall v. Hashable v => [(v, ExprBV v v)] -> SubstV v
F.mkSubst [(Variable c, ExprBV (Variable c) (Variable c))]
su) c
t, d
forall a. Monoid a => a
mempty)
                               (Variable c, RFInfo, c, d)
-> [(Variable c, RFInfo, c, d)] -> [(Variable c, RFInfo, c, d)]
forall a. a -> [a] -> [a]
: [(Variable c, ExprBV (Variable c) (Variable c))]
-> [Variable c]
-> [Variable c]
-> [c]
-> [(Variable c, RFInfo, c, d)]
tx ((Variable c
x, Variable c -> ExprBV (Variable c) (Variable c)
forall b v. v -> ExprBV b v
F.EVar Variable c
y)(Variable c, ExprBV (Variable c) (Variable c))
-> [(Variable c, ExprBV (Variable c) (Variable c))]
-> [(Variable c, ExprBV (Variable c) (Variable c))]
forall a. a -> [a] -> [a]
:[(Variable c, ExprBV (Variable c) (Variable c))]
su) [Variable c]
xs [Variable c]
ys [c]
ts
    tx [(Variable c, ExprBV (Variable c) (Variable c))]
_ [Variable c]
_ [Variable c]
_ [c]
_ = Maybe SrcSpan -> [Char] -> [(Variable c, RFInfo, c, d)]
forall a. HasCallStack => Maybe SrcSpan -> [Char] -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing [Char]
"PredType.dataConPSpecType.tx called on invalid inputs"
    yts' :: [(Variable (RRType RReft), RFInfo, RRType RReft, RReft)]
yts'     = [(Variable (RRType RReft),
  ExprBV (Variable (RRType RReft)) (Variable (RRType RReft)))]
-> [Variable (RRType RReft)]
-> [Variable (RRType RReft)]
-> [RRType RReft]
-> [(Variable (RRType RReft), RFInfo, RRType RReft, RReft)]
forall {c} {d}.
(Subable c, Monoid d) =>
[(Variable c, ExprBV (Variable c) (Variable c))]
-> [Variable c]
-> [Variable c]
-> [c]
-> [(Variable c, RFInfo, c, d)]
tx [] [Symbol]
[Variable (RRType RReft)]
as1 [Symbol]
[Variable (RRType RReft)]
bs [RRType RReft]
sts
    ts' :: [(Symbol, RFInfo, RRType RReft, RReft)]
ts'      = (RRType RReft -> (Symbol, RFInfo, RRType RReft, RReft))
-> [RRType RReft] -> [(Symbol, RFInfo, RRType RReft, RReft)]
forall a b. (a -> b) -> [a] -> [b]
map (Symbol
"" , Bool -> RFInfo
classRFInfo Bool
allowTC , , RReft
forall a. Monoid a => a
mempty) [RRType RReft]
cs [(Symbol, RFInfo, RRType RReft, RReft)]
-> [(Symbol, RFInfo, RRType RReft, RReft)]
-> [(Symbol, RFInfo, RRType RReft, RReft)]
forall a. [a] -> [a] -> [a]
++ [(Symbol, RFInfo, RRType RReft, RReft)]
yts'
    subst :: SubstV Symbol
subst    = [(Symbol, Expr)] -> SubstV Symbol
forall v. Hashable v => [(v, ExprBV v v)] -> SubstV v
F.mkSubst [(Symbol
x, Symbol -> Expr
forall b v. v -> ExprBV b v
F.EVar Symbol
y) | (Symbol
x, Symbol
y) <- [Symbol] -> [Symbol] -> [(Symbol, Symbol)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
as1 [Symbol]
bs]
    rt' :: RRType RReft
rt'      = SubstV (Variable (RRType RReft)) -> RRType RReft -> RRType RReft
forall a.
(Subable a, HasCallStack) =>
SubstV (Variable a) -> a -> a
F.subst SubstV Symbol
SubstV (Variable (RRType RReft))
subst RRType RReft
rt
    makeVars :: [RTVar RTyVar RSort]
makeVars = (RTVar RTyVar RSort -> Bool)
-> [RTVar RTyVar RSort] -> [RTVar RTyVar RSort]
forall a. (a -> Bool) -> [a] -> [a]
filter (RTVar RTyVar RSort -> [RTVar RTyVar RSort] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [RTVar RTyVar RSort]
fvs) ([RTVar RTyVar RSort] -> [RTVar RTyVar RSort])
-> [RTVar RTyVar RSort] -> [RTVar RTyVar RSort]
forall a b. (a -> b) -> a -> b
$ (RTyVar -> TyVar -> RTVar RTyVar RSort)
-> [RTyVar] -> [TyVar] -> [RTVar RTyVar RSort]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\RTyVar
v TyVar
a -> RTyVar -> RTVInfo RSort -> RTVar RTyVar RSort
forall tv s. tv -> RTVInfo s -> RTVar tv s
RTVar RTyVar
v (TyVar -> RTVInfo RSort
forall r. IsReft r => TyVar -> RTVInfo (RRType r)
rTVarInfo TyVar
a :: RTVInfo RSort)) [RTyVar]
vs (([TyVar], Type) -> [TyVar]
forall a b. (a, b) -> a
fst (([TyVar], Type) -> [TyVar]) -> ([TyVar], Type) -> [TyVar]
forall a b. (a -> b) -> a -> b
$ Type -> ([TyVar], Type)
splitForAllTyCoVars (Type -> ([TyVar], Type)) -> Type -> ([TyVar], Type)
forall a b. (a -> b) -> a -> b
$ DataCon -> Type
dataConRepType DataCon
dc)
    makeVars' :: [(RTVar RTyVar RSort, RReft)]
makeVars' = (RTVar RTyVar RSort -> (RTVar RTyVar RSort, RReft))
-> [RTVar RTyVar RSort] -> [(RTVar RTyVar RSort, RReft)]
forall a b. (a -> b) -> [a] -> [b]
map (, RReft
forall a. Monoid a => a
mempty) [RTVar RTyVar RSort]
makeVars
    fvs :: [RTVar RTyVar RSort]
fvs = RRType RReft -> [RTVar RTyVar RSort]
forall tv v c r.
Eq tv =>
RTypeV v c tv r -> [RTVar tv (RTypeV v c tv (NoReftB Symbol))]
freeTyVars (RRType RReft -> [RTVar RTyVar RSort])
-> RRType RReft -> [RTVar RTyVar RSort]
forall a b. (a -> b) -> a -> b
$ [(RTVar RTyVar RSort, RReft)]
-> [RPVar]
-> [(Symbol, RFInfo, RRType RReft, RReft)]
-> RRType RReft
-> RRType RReft
forall tv b v c r.
[(RTVar tv (RTypeBV b v c tv (NoReftB b)), r)]
-> [PVarBV b v (RTypeBV b v c tv (NoReftB b))]
-> [(b, RFInfo, RTypeBV b v c tv r, r)]
-> RTypeBV b v c tv r
-> RTypeBV b v c tv r
mkArrow [] [RPVar]
ps [(Symbol, RFInfo, RRType RReft, RReft)]
ts' RRType RReft
rt'

dataConTy :: IsReft r
          => M.HashMap RTyVar (RType RTyCon RTyVar r)
          -> Type -> RType RTyCon RTyVar r
dataConTy :: forall r.
IsReft r =>
HashMap RTyVar (RType RTyCon RTyVar r)
-> Type -> RType RTyCon RTyVar r
dataConTy HashMap RTyVar (RType RTyCon RTyVar r)
m (TyVarTy TyVar
v)
  = RType RTyCon RTyVar r
-> RTyVar
-> HashMap RTyVar (RType RTyCon RTyVar r)
-> RType RTyCon RTyVar r
forall k v. Hashable k => v -> k -> HashMap k v -> v
M.lookupDefault (TyVar -> RType RTyCon RTyVar r
forall r c. IsReft 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 FunTyFlag
_ Type
_ Type
t1 Type
t2)
  = Symbol
-> RType RTyCon RTyVar r
-> RType RTyCon RTyVar r
-> RType RTyCon RTyVar r
forall r b v c tv.
IsReft r =>
b -> RTypeBV b v c tv r -> RTypeBV b v c tv r -> RTypeBV b v c tv r
rFun Symbol
F.dummySymbol (HashMap RTyVar (RType RTyCon RTyVar r)
-> Type -> RType RTyCon RTyVar r
forall r.
IsReft r =>
HashMap RTyVar (RType RTyCon RTyVar r)
-> Type -> RType RTyCon RTyVar r
dataConTy HashMap RTyVar (RType RTyCon RTyVar r)
m Type
t1) (HashMap RTyVar (RType RTyCon RTyVar r)
-> Type -> RType RTyCon RTyVar r
forall r.
IsReft 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
α ForAllTyFlag
_) Type
t) -- α :: TyVar
  = RTVar RTyVar RSort
-> RType RTyCon RTyVar r -> r -> RType RTyCon RTyVar r
forall b v c tv r.
RTVUBV b v c tv -> RTypeBV b v c tv r -> r -> RTypeBV b v c tv r
RAllT (RTyVar -> RTVar RTyVar RSort
forall tv s. tv -> RTVar tv s
makeRTVar (TyVar -> RTyVar
RTV TyVar
α)) (HashMap RTyVar (RType RTyCon RTyVar r)
-> Type -> RType RTyCon RTyVar r
forall r.
IsReft r =>
HashMap RTyVar (RType RTyCon RTyVar r)
-> Type -> RType RTyCon RTyVar r
dataConTy HashMap RTyVar (RType RTyCon RTyVar r)
m Type
t) r
forall r. IsReft r => r
trueReft
dataConTy HashMap RTyVar (RType RTyCon RTyVar r)
m (TyConApp TyCon
c [Type]
ts)
  = TyCon
-> [RType RTyCon RTyVar r]
-> [RTProp RTyCon RTyVar r]
-> r
-> RType RTyCon RTyVar r
forall tv r.
TyCon
-> [RType RTyCon tv r]
-> [RTProp RTyCon tv r]
-> r
-> RType RTyCon tv r
rApp TyCon
c (HashMap RTyVar (RType RTyCon RTyVar r)
-> Type -> RType RTyCon RTyVar r
forall r.
IsReft r =>
HashMap RTyVar (RType RTyCon RTyVar r)
-> Type -> RType RTyCon RTyVar r
dataConTy HashMap RTyVar (RType RTyCon RTyVar r)
m (Type -> RType RTyCon RTyVar r)
-> [Type] -> [RType RTyCon RTyVar r]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Type]
ts) [] r
forall r. IsReft r => r
trueReft
dataConTy HashMap RTyVar (RType RTyCon RTyVar r)
_ Type
_
  = Maybe SrcSpan -> [Char] -> RType RTyCon RTyVar r
forall a. HasCallStack => Maybe SrcSpan -> [Char] -> a
panic Maybe SrcSpan
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))
  = ReftBV Symbol Symbol -> PredicateBV Symbol Symbol -> RReft
forall b v r. r -> PredicateBV b v -> UReftBV b v r
MkUReft ((Symbol, Expr) -> ReftBV Symbol Symbol
forall b v. (b, ExprBV b v) -> ReftBV b v
F.Reft (Symbol
v, Expr
rs'')) ([UsedPVar] -> PredicateBV Symbol Symbol
forall b v. [UsedPVarBV b v] -> PredicateBV b v
Pr [UsedPVar]
ps2)
  where
    rs'' :: Expr
rs''             = (Expr -> Expr -> Expr) -> Expr -> [Expr] -> Expr
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Expr -> Expr -> Expr
(F.&.&) Expr
forall b v. ExprBV b v
F.PTrue ([Expr] -> Expr) -> [Expr] -> Expr
forall a b. (a -> b) -> a -> b
$ Expr
rs Expr -> [Expr] -> [Expr]
forall a. a -> [a] -> [a]
: [Expr]
rs'
    rs' :: [Expr]
rs'              = (Symbol, [((), Symbol, Expr)]) -> Expr
r ((Symbol, [((), Symbol, Expr)]) -> Expr)
-> (UsedPVar -> (Symbol, [((), Symbol, Expr)])) -> UsedPVar -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol
v,) ([((), Symbol, Expr)] -> (Symbol, [((), Symbol, Expr)]))
-> (UsedPVar -> [((), Symbol, Expr)])
-> UsedPVar
-> (Symbol, [((), Symbol, Expr)])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UsedPVar -> [((), Symbol, Expr)]
forall b v t. PVarBV b v t -> [(t, b, ExprBV b v)]
pargs (UsedPVar -> Expr) -> [UsedPVar] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [UsedPVar]
ps1
    ([UsedPVar]
ps1, [UsedPVar]
ps2)       = (UsedPVar -> Bool) -> [UsedPVar] -> ([UsedPVar], [UsedPVar])
forall a. (a -> Bool) -> [a] -> ([a], [a])
L.partition (UsedPVar -> UsedPVar -> Bool
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) | [(a, b, Expr)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(a, b, Expr)]
args Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [(t, Symbol, Expr)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (PVar t -> [(t, Symbol, Expr)]
forall b v t. PVarBV b v t -> [(t, b, ExprBV b v)]
pargs PVar t
p)
  = Symbol -> [Expr] -> Expr
forall b v. PredicateCompat b v => v -> [ExprBV b v] -> ExprBV b v
pApp (PVar t -> Symbol
forall b v t. PVarBV b v t -> b
pname PVar t
p) ([Expr] -> Expr) -> [Expr] -> Expr
forall a b. (a -> b) -> a -> b
$ Symbol -> Expr
forall b v. v -> ExprBV b v
F.EVar Symbol
v Expr -> [Expr] -> [Expr]
forall a. a -> [a] -> [a]
: ((a, b, Expr) -> Expr
forall a b c. (a, b, c) -> c
thd3 ((a, b, Expr) -> Expr) -> [(a, b, Expr)] -> [Expr]
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
forall b v. PredicateCompat b v => v -> [ExprBV b v] -> ExprBV b v
pApp (PVar t -> Symbol
forall b v t. PVarBV b v t -> b
pname PVar t
p) ([Expr] -> Expr) -> [Expr] -> Expr
forall a b. (a -> b) -> a -> b
$ Symbol -> Expr
forall b v. v -> ExprBV b v
F.EVar Symbol
v Expr -> [Expr] -> [Expr]
forall a. a -> [a] -> [a]
: [Expr]
args'
  where
    args' :: [Expr]
args' = ((a, b, Expr) -> Expr
forall a b c. (a, b, c) -> c
thd3 ((a, b, Expr) -> Expr) -> [(a, b, Expr)] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(a, b, Expr)]
args) [Expr] -> [Expr] -> [Expr]
forall a. [a] -> [a] -> [a]
++ Int -> [Expr] -> [Expr]
forall a. Int -> [a] -> [a]
drop ([(a, b, Expr)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(a, b, Expr)]
args) ((t, Symbol, Expr) -> Expr
forall a b c. (a, b, c) -> c
thd3 ((t, Symbol, Expr) -> Expr) -> [(t, Symbol, Expr)] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PVar t -> [(t, Symbol, Expr)]
forall b v t. PVarBV b v t -> [(t, b, ExprBV b v)]
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, IsReft r) => PVar RSort -> RRType r
-----------------------------------------------------------------------
pvarRType :: forall r. (PPrint r, IsReft r) => RPVar -> RRType r
pvarRType (PV Symbol
_ RSort
k {- (PVProp τ) -} Symbol
_ [(RSort, Symbol, Expr)]
args) = RSort -> [RSort] -> RType RTyCon RTyVar r
forall r tv a.
IsReft r =>
RType RTyCon tv a -> [RType RTyCon tv a] -> RType RTyCon tv r
rpredType RSort
k ((RSort, Symbol, Expr) -> RSort
forall a b c. (a, b, c) -> a
fst3 ((RSort, Symbol, Expr) -> RSort)
-> [(RSort, Symbol, Expr)] -> [RSort]
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 :: IsReft r
          => RType RTyCon tv a
          -> [RType RTyCon tv a] -> RType RTyCon tv r
rpredType :: forall r tv a.
IsReft r =>
RType RTyCon tv a -> [RType RTyCon tv a] -> RType RTyCon tv r
rpredType RType RTyCon tv a
t [RType RTyCon tv a]
ts = RTyCon
-> [RTypeBV Symbol Symbol RTyCon tv r]
-> [RTPropBV Symbol Symbol RTyCon tv r]
-> r
-> RTypeBV Symbol Symbol RTyCon tv r
forall b v c tv r.
c
-> [RTypeBV b v c tv r]
-> [RTPropBV b v c tv r]
-> r
-> RTypeBV b v c tv r
RApp RTyCon
predRTyCon  (RType RTyCon tv a -> RTypeBV Symbol Symbol RTyCon tv r
forall b c tv a. IsReft b => RType c tv a -> RType c tv b
uRTypeGen (RType RTyCon tv a -> RTypeBV Symbol Symbol RTyCon tv r)
-> [RType RTyCon tv a] -> [RTypeBV Symbol Symbol RTyCon tv r]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RType RTyCon tv a
t RType RTyCon tv a -> [RType RTyCon tv a] -> [RType RTyCon tv a]
forall a. a -> [a] -> [a]
: [RType RTyCon tv a]
ts) [] r
forall r. IsReft r => r
trueReft

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

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

-------------------------------------------------------------------------------------
-- | 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                 = (RRType RReft -> (RPVar, Ref RSort (RRType RReft)) -> RRType RReft)
-> RRType RReft
-> [(RPVar, Ref RSort (RRType RReft))]
-> RRType RReft
forall b a. (b -> a -> b) -> b -> [a] -> b
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
_)) = Maybe SrcSpan -> [Char] -> RRType RReft
forall a. HasCallStack => Maybe SrcSpan -> [Char] -> a
panic Maybe SrcSpan
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 :: PVarV v (BSortV v) -> PVarV v (BSortV v) -> BareTypeParsed -> BareTypeParsed
-------------------------------------------------------------------------------------
substPVar :: forall v.
PVarV v (BSortV v)
-> PVarV v (BSortV v) -> BareTypeParsed -> BareTypeParsed
substPVar PVarV v (BSortV v)
src PVarV v (BSortV v)
dst = BareTypeParsed -> BareTypeParsed
go
  where
    go :: BareTypeParsed -> BareTypeParsed
    go :: BareTypeParsed -> BareTypeParsed
go (RVar BTyVar
a RReftV LocSymbol
r)         = BTyVar -> RReftV LocSymbol -> BareTypeParsed
forall b v c tv r. tv -> r -> RTypeBV b v c tv r
RVar BTyVar
a (RReftV LocSymbol -> RReftV LocSymbol
goRR RReftV LocSymbol
r)
    go (RApp BTyCon
c [BareTypeParsed]
ts [RTPropBV Symbol LocSymbol BTyCon BTyVar (RReftV LocSymbol)]
rs RReftV LocSymbol
r)   = BTyCon
-> [BareTypeParsed]
-> [RTPropBV Symbol LocSymbol BTyCon BTyVar (RReftV LocSymbol)]
-> RReftV LocSymbol
-> BareTypeParsed
forall b v c tv r.
c
-> [RTypeBV b v c tv r]
-> [RTPropBV b v c tv r]
-> r
-> RTypeBV b v c tv r
RApp BTyCon
c (BareTypeParsed -> BareTypeParsed
go (BareTypeParsed -> BareTypeParsed)
-> [BareTypeParsed] -> [BareTypeParsed]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [BareTypeParsed]
ts) (RTPropBV Symbol LocSymbol BTyCon BTyVar (RReftV LocSymbol)
-> RTPropBV Symbol LocSymbol BTyCon BTyVar (RReftV LocSymbol)
goR (RTPropBV Symbol LocSymbol BTyCon BTyVar (RReftV LocSymbol)
 -> RTPropBV Symbol LocSymbol BTyCon BTyVar (RReftV LocSymbol))
-> [RTPropBV Symbol LocSymbol BTyCon BTyVar (RReftV LocSymbol)]
-> [RTPropBV Symbol LocSymbol BTyCon BTyVar (RReftV LocSymbol)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RTPropBV Symbol LocSymbol BTyCon BTyVar (RReftV LocSymbol)]
rs) (RReftV LocSymbol -> RReftV LocSymbol
goRR RReftV LocSymbol
r)
    go (RAllP PVUBV Symbol LocSymbol BTyCon BTyVar
q BareTypeParsed
t)
     | PVUBV Symbol LocSymbol BTyCon BTyVar -> Symbol
forall b v t. PVarBV b v t -> b
pname PVUBV Symbol LocSymbol BTyCon BTyVar
q Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== PVarV v (BSortV v) -> Symbol
forall b v t. PVarBV b v t -> b
pname PVarV v (BSortV v)
src = PVUBV Symbol LocSymbol BTyCon BTyVar
-> BareTypeParsed -> BareTypeParsed
forall b v c tv r.
PVUBV b v c tv -> RTypeBV b v c tv r -> RTypeBV b v c tv r
RAllP PVUBV Symbol LocSymbol BTyCon BTyVar
q BareTypeParsed
t
     | Bool
otherwise            = PVUBV Symbol LocSymbol BTyCon BTyVar
-> BareTypeParsed -> BareTypeParsed
forall b v c tv r.
PVUBV b v c tv -> RTypeBV b v c tv r -> RTypeBV b v c tv r
RAllP PVUBV Symbol LocSymbol BTyCon BTyVar
q (BareTypeParsed -> BareTypeParsed
go BareTypeParsed
t)
    go (RAllT RTVUBV Symbol LocSymbol BTyCon BTyVar
a BareTypeParsed
t RReftV LocSymbol
r)      = RTVUBV Symbol LocSymbol BTyCon BTyVar
-> BareTypeParsed -> RReftV LocSymbol -> BareTypeParsed
forall b v c tv r.
RTVUBV b v c tv -> RTypeBV b v c tv r -> r -> RTypeBV b v c tv r
RAllT RTVUBV Symbol LocSymbol BTyCon BTyVar
a   (BareTypeParsed -> BareTypeParsed
go BareTypeParsed
t)  (RReftV LocSymbol -> RReftV LocSymbol
goRR RReftV LocSymbol
r)
    go (RFun Symbol
x RFInfo
i BareTypeParsed
t BareTypeParsed
t' RReftV LocSymbol
r)  = Symbol
-> RFInfo
-> BareTypeParsed
-> BareTypeParsed
-> RReftV LocSymbol
-> BareTypeParsed
forall b v c tv r.
b
-> RFInfo
-> RTypeBV b v c tv r
-> RTypeBV b v c tv r
-> r
-> RTypeBV b v c tv r
RFun Symbol
x RFInfo
i  (BareTypeParsed -> BareTypeParsed
go BareTypeParsed
t)  (BareTypeParsed -> BareTypeParsed
go BareTypeParsed
t') (RReftV LocSymbol -> RReftV LocSymbol
goRR RReftV LocSymbol
r)
    go (RAllE Symbol
x BareTypeParsed
t BareTypeParsed
t')     = Symbol -> BareTypeParsed -> BareTypeParsed -> BareTypeParsed
forall b v c tv r.
b -> RTypeBV b v c tv r -> RTypeBV b v c tv r -> RTypeBV b v c tv r
RAllE Symbol
x   (BareTypeParsed -> BareTypeParsed
go BareTypeParsed
t)  (BareTypeParsed -> BareTypeParsed
go BareTypeParsed
t')
    go (REx Symbol
x BareTypeParsed
t BareTypeParsed
t')       = Symbol -> BareTypeParsed -> BareTypeParsed -> BareTypeParsed
forall b v c tv r.
b -> RTypeBV b v c tv r -> RTypeBV b v c tv r -> RTypeBV b v c tv r
REx Symbol
x     (BareTypeParsed -> BareTypeParsed
go BareTypeParsed
t)  (BareTypeParsed -> BareTypeParsed
go BareTypeParsed
t')
    go (RRTy [(Symbol, BareTypeParsed)]
e RReftV LocSymbol
r Oblig
o BareTypeParsed
rt)    = [(Symbol, BareTypeParsed)]
-> RReftV LocSymbol -> Oblig -> BareTypeParsed -> BareTypeParsed
forall b v c tv r.
[(b, RTypeBV b v c tv r)]
-> r -> Oblig -> RTypeBV b v c tv r -> RTypeBV b v c tv r
RRTy [(Symbol, BareTypeParsed)]
e'   (RReftV LocSymbol -> RReftV LocSymbol
goRR RReftV LocSymbol
r) Oblig
o (BareTypeParsed -> BareTypeParsed
go BareTypeParsed
rt) where e' :: [(Symbol, BareTypeParsed)]
e' = [(Symbol
x, BareTypeParsed -> BareTypeParsed
go BareTypeParsed
t) | (Symbol
x, BareTypeParsed
t) <- [(Symbol, BareTypeParsed)]
e]
    go (RAppTy BareTypeParsed
t1 BareTypeParsed
t2 RReftV LocSymbol
r)   = BareTypeParsed
-> BareTypeParsed -> RReftV LocSymbol -> BareTypeParsed
forall b v c tv r.
RTypeBV b v c tv r -> RTypeBV b v c tv r -> r -> RTypeBV b v c tv r
RAppTy    (BareTypeParsed -> BareTypeParsed
go BareTypeParsed
t1) (BareTypeParsed -> BareTypeParsed
go BareTypeParsed
t2) (RReftV LocSymbol -> RReftV LocSymbol
goRR RReftV LocSymbol
r)
    go (RHole RReftV LocSymbol
r)          = RReftV LocSymbol -> BareTypeParsed
forall b v c tv r. r -> RTypeBV b v c tv r
RHole     (RReftV LocSymbol -> RReftV LocSymbol
goRR RReftV LocSymbol
r)
    go t :: BareTypeParsed
t@(RExprArg  Located (ExprBV Symbol LocSymbol)
_)    = BareTypeParsed
t
    goR :: BRPropV LocSymbol (RReftV LocSymbol) -> BRPropV LocSymbol (RReftV LocSymbol)
    goR :: RTPropBV Symbol LocSymbol BTyCon BTyVar (RReftV LocSymbol)
-> RTPropBV Symbol LocSymbol BTyCon BTyVar (RReftV LocSymbol)
goR RTPropBV Symbol LocSymbol BTyCon BTyVar (RReftV LocSymbol)
rp = RTPropBV Symbol LocSymbol BTyCon BTyVar (RReftV LocSymbol)
rp {rf_body = go (rf_body rp) }
    goRR :: RReftV LocSymbol -> RReftV LocSymbol
    goRR :: RReftV LocSymbol -> RReftV LocSymbol
goRR RReftV LocSymbol
rr = RReftV LocSymbol
rr { ur_pred = goP (ur_pred rr) }
    goP :: PredicateV LocSymbol -> PredicateV LocSymbol
    goP :: PredicateV LocSymbol -> PredicateV LocSymbol
goP (Pr [UsedPVarBV Symbol LocSymbol]
ps) = [UsedPVarBV Symbol LocSymbol] -> PredicateV LocSymbol
forall b v. [UsedPVarBV b v] -> PredicateBV b v
Pr (UsedPVarBV Symbol LocSymbol -> UsedPVarBV Symbol LocSymbol
goPV (UsedPVarBV Symbol LocSymbol -> UsedPVarBV Symbol LocSymbol)
-> [UsedPVarBV Symbol LocSymbol] -> [UsedPVarBV Symbol LocSymbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [UsedPVarBV Symbol LocSymbol]
ps)
    goPV :: UsedPVarV LocSymbol -> UsedPVarV LocSymbol
    goPV :: UsedPVarBV Symbol LocSymbol -> UsedPVarBV Symbol LocSymbol
goPV UsedPVarBV Symbol LocSymbol
pv
      | UsedPVarBV Symbol LocSymbol -> Symbol
forall b v t. PVarBV b v t -> b
pname UsedPVarBV Symbol LocSymbol
pv Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== PVarV v (BSortV v) -> Symbol
forall b v t. PVarBV b v t -> b
pname PVarV v (BSortV v)
src = UsedPVarBV Symbol LocSymbol
pv { pname = pname dst }
      | Bool
otherwise             = UsedPVarBV Symbol LocSymbol
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 RTyVar -> RTyVar -> Bool
forall a. Eq a => a -> a -> Bool
== RTyVar
a2    = RTyVar -> RReft -> RRType RReft
forall b v c tv r. tv -> r -> RTypeBV b v c tv r
RVar RTyVar
a1 (RReft -> RRType RReft) -> RReft -> RRType RReft
forall a b. (a -> b) -> a -> b
$ [UsedPVar] -> [(Symbol, RSort)] -> RReft -> RReft -> RReft
forall (t :: * -> *) t1 b.
(Foldable t, PPrint t1, Subable b, Variable b ~ Symbol, Meet b) =>
t (PVar t1) -> [(Symbol, RSort)] -> b -> b -> b
meetListWithPSubs [UsedPVar]
πs [(Symbol, RSort)]
ss RReft
r1 RReft
r2'
  | Bool
isPredInReft                = Maybe SrcSpan -> [Char] -> RRType RReft
forall a. HasCallStack => Maybe SrcSpan -> [Char] -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing ([Char]
"substPred RVar Var Mismatch" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ (RTyVar, RTyVar) -> [Char]
forall a. Show a => a -> [Char]
show (RTyVar
a1, RTyVar
a2))
  | Bool
otherwise                   = RRType RReft
t
  where
    (RReft
r2', [UsedPVar]
πs)                   = RPVar -> RReft -> (RReft, [UsedPVar])
forall t r. PVar t -> UReft r -> (UReft r, [UsedPVar])
splitRPvar RPVar
rp RReft
r2
    isPredInReft :: Bool
isPredInReft                = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [UsedPVar] -> Bool
forall a. [a] -> Bool
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)
  | [UsedPVar] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [UsedPVar]
πs                     = RRType RReft
t'
  | Bool
otherwise                   = [Char]
-> (RPVar, Ref RSort (RRType RReft))
-> RRType RReft
-> [UsedPVar]
-> RReft
-> RRType RReft
forall t t2 tv r.
(PPrint t, PPrint t2, Eq tv, IsReft r, Hashable tv, PPrint tv,
 PPrint r, Subable r, Variable r ~ Symbol, ReftBind r ~ Symbol,
 ReftVar r ~ Symbol, SubsTy tv (RType RTyCon tv (NoReftB Symbol)) r,
 SubsTy
   tv
   (RType RTyCon tv (NoReftB Symbol))
   (RType RTyCon tv (NoReftB Symbol)),
 SubsTy tv (RType RTyCon tv (NoReftB Symbol)) RTyCon,
 SubsTy tv (RType RTyCon tv (NoReftB Symbol)) tv,
 SubsTy
   tv
   (RType RTyCon tv (NoReftB Symbol))
   (RTVar tv (RType RTyCon tv (NoReftB Symbol))),
 FreeVar RTyCon tv, Meet (RType RTyCon tv r)) =>
[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'                          = RTyCon
-> [RRType RReft]
-> [Ref RSort (RRType RReft)]
-> RReft
-> RRType RReft
forall b v c tv r.
c
-> [RTypeBV b v c tv r]
-> [RTPropBV b v c tv r]
-> r
-> RTypeBV b v c tv r
RApp RTyCon
c ([Char]
-> (RPVar, Ref RSort (RRType RReft))
-> RRType RReft
-> RRType RReft
substPred [Char]
msg (RPVar, Ref RSort (RRType RReft))
su (RRType RReft -> RRType RReft) -> [RRType RReft] -> [RRType RReft]
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 (Ref RSort (RRType RReft) -> Ref RSort (RRType RReft))
-> [Ref RSort (RRType RReft)] -> [Ref RSort (RRType RReft)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Ref RSort (RRType RReft)]
rs) RReft
r
    (RReft
r2', [UsedPVar]
πs)                   = RPVar -> RReft -> (RReft, [UsedPVar])
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 RPVar -> RPVar -> Bool
forall a. Eq a => a -> a -> Bool
/= RPVar
q                      = RPVar -> RRType RReft -> RRType RReft
forall b v c tv r.
PVUBV b v c tv -> RTypeBV b v c tv r -> RTypeBV b v c tv r
RAllP RPVar
q (RRType RReft -> RRType RReft) -> RRType RReft -> RRType RReft
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                   = RPVar -> RRType RReft -> RRType RReft
forall b v c tv r.
PVUBV b v c tv -> RTypeBV b v c tv r -> RTypeBV b v 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)  = RTVar RTyVar RSort -> RRType RReft -> RReft -> RRType RReft
forall b v c tv r.
RTVUBV b v c tv -> RTypeBV b v c tv r -> r -> RTypeBV b v c tv r
RAllT RTVar RTyVar 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
  | [UsedPVar] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [UsedPVar]
πs                     = Symbol
-> RFInfo -> RRType RReft -> RRType RReft -> RReft -> RRType RReft
forall b v c tv r.
b
-> RFInfo
-> RTypeBV b v c tv r
-> RTypeBV b v c tv r
-> r
-> RTypeBV b v c tv r
RFun Symbol
x RFInfo
i ([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 :: [SubstV Symbol]
sus = (\UsedPVar
π -> [(Symbol, Expr)] -> SubstV Symbol
forall v. Hashable v => [(v, ExprBV v v)] -> SubstV v
F.mkSubst ([Symbol] -> [Expr] -> [(Symbol, Expr)]
forall a b. [a] -> [b] -> [(a, b)]
zip ((Symbol, RSort) -> Symbol
forall a b. (a, b) -> a
fst ((Symbol, RSort) -> Symbol) -> [(Symbol, RSort)] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Ref RSort (RRType RReft) -> [(Symbol, RSort)]
forall b τ t. RefB b τ t -> [(b, τ)]
rf_args Ref RSort (RRType RReft)
prop) (((), Symbol, Expr) -> Expr
forall a b c. (a, b, c) -> c
thd3 (((), Symbol, Expr) -> Expr) -> [((), Symbol, Expr)] -> [Expr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> UsedPVar -> [((), Symbol, Expr)]
forall b v t. PVarBV b v t -> [(t, b, ExprBV b v)]
pargs UsedPVar
π))) (UsedPVar -> SubstV Symbol) -> [UsedPVar] -> [SubstV Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [UsedPVar]
πs in
      (RRType RReft -> SubstV Symbol -> RRType RReft)
-> RRType RReft -> [SubstV Symbol] -> RRType RReft
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\RRType RReft
t SubstV Symbol
subst -> RRType RReft
t RRType RReft -> RRType RReft -> RRType RReft
forall r. Meet r => r -> r -> r
`meet` SubstV (Variable (RRType RReft)) -> RRType RReft -> RRType RReft
forall a.
(Subable a, HasCallStack) =>
SubstV (Variable a) -> a -> a
F.subst SubstV Symbol
SubstV (Variable (RRType RReft))
subst (Ref RSort (RRType RReft) -> RRType RReft
forall b τ t. RefB b τ t -> t
rf_body Ref RSort (RRType RReft)
prop)) (Symbol
-> RFInfo -> RRType RReft -> RRType RReft -> RReft -> RRType RReft
forall b v c tv r.
b
-> RFInfo
-> RTypeBV b v c tv r
-> RTypeBV b v c tv r
-> r
-> RTypeBV b v c tv r
RFun Symbol
x RFInfo
i ([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') [SubstV Symbol]
sus
  where (RReft
r', [UsedPVar]
πs)                = RPVar -> RReft -> (RReft, [UsedPVar])
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) = [(Symbol, RRType RReft)]
-> RReft -> Oblig -> RRType RReft -> RRType RReft
forall b v c tv r.
[(b, RTypeBV b v c tv r)]
-> r -> Oblig -> RTypeBV b v c tv r -> RTypeBV b v c tv r
RRTy ((RRType RReft -> RRType RReft)
-> (Symbol, RRType RReft) -> (Symbol, RRType RReft)
forall a b. (a -> b) -> (Symbol, a) -> (Symbol, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([Char]
-> (RPVar, Ref RSort (RRType RReft))
-> RRType RReft
-> RRType RReft
substPred [Char]
msg (RPVar, Ref RSort (RRType RReft))
su) ((Symbol, RRType RReft) -> (Symbol, RRType RReft))
-> [(Symbol, RRType RReft)] -> [(Symbol, RRType RReft)]
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') = Symbol -> RRType RReft -> RRType RReft -> RRType RReft
forall b v c tv r.
b -> RTypeBV b v c tv r -> RTypeBV b v c tv r -> RTypeBV b v c tv r
RAllE Symbol
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')   = Symbol -> RRType RReft -> RRType RReft -> RRType RReft
forall b v c tv r.
b -> RTypeBV b v c tv r -> RTypeBV b v c tv r -> RTypeBV b v c tv r
REx   Symbol
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, IsReft r, Hashable tv, PPrint tv, PPrint r,
      F.Subable r, F.Variable r ~ F.Symbol, ReftBind r ~ F.Symbol, ReftVar r ~ F.Symbol,
      SubsTy tv (RType RTyCon tv NoReft) r,
      SubsTy tv (RType RTyCon tv NoReft) (RType RTyCon tv NoReft),
      SubsTy tv (RType RTyCon tv NoReft) RTyCon,
      SubsTy tv (RType RTyCon tv NoReft) tv,
      SubsTy tv (RType RTyCon tv NoReft) (RTVar tv (RType RTyCon tv NoReft)),
      FreeVar RTyCon tv,
      Meet (RType RTyCon tv r))
  => [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, IsReft r, Hashable tv, PPrint tv,
 PPrint r, Subable r, Variable r ~ Symbol, ReftBind r ~ Symbol,
 ReftVar r ~ Symbol, SubsTy tv (RType RTyCon tv (NoReftB Symbol)) r,
 SubsTy
   tv
   (RType RTyCon tv (NoReftB Symbol))
   (RType RTyCon tv (NoReftB Symbol)),
 SubsTy tv (RType RTyCon tv (NoReftB Symbol)) RTyCon,
 SubsTy tv (RType RTyCon tv (NoReftB Symbol)) tv,
 SubsTy
   tv
   (RType RTyCon tv (NoReftB Symbol))
   (RTVar tv (RType RTyCon tv (NoReftB Symbol))),
 FreeVar RTyCon tv, Meet (RType RTyCon tv r)) =>
[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 [RTPropBV Symbol Symbol RTyCon tv r]
rs1 r
r1)) t2 :: RType RTyCon tv r
t2@(RApp RTyCon
c2 [RType RTyCon tv r]
ts2 [RTPropBV Symbol Symbol RTyCon tv r]
rs2 r
_) [PVar t2]
πs r
r2'
  | RTyCon -> TyCon
rtc_tc RTyCon
c1 TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== RTyCon -> TyCon
rtc_tc RTyCon
c2 = RTyCon
-> [RType RTyCon tv r]
-> [RTPropBV Symbol Symbol RTyCon tv r]
-> r
-> RType RTyCon tv r
forall b v c tv r.
c
-> [RTypeBV b v c tv r]
-> [RTPropBV b v c tv r]
-> r
-> RTypeBV b v c tv r
RApp RTyCon
c1 [RType RTyCon tv r]
ts [RTPropBV Symbol Symbol RTyCon tv r]
rs (r -> RType RTyCon tv r) -> r -> RType RTyCon tv r
forall a b. (a -> b) -> a -> b
$ [PVar t2] -> [(Symbol, RSort)] -> r -> r -> r
forall (t :: * -> *) t1 b.
(Foldable t, PPrint t1, Subable b, Variable b ~ Symbol, Meet 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                     = SubstV (Variable [RType RTyCon tv r])
-> [RType RTyCon tv r] -> [RType RTyCon tv r]
forall a.
(Subable a, HasCallStack) =>
SubstV (Variable a) -> a -> a
F.subst SubstV (Variable [RType RTyCon tv r])
SubstV (ReftBind r)
su ([RType RTyCon tv r] -> [RType RTyCon tv r])
-> [RType RTyCon tv r] -> [RType RTyCon tv r]
forall a b. (a -> b) -> a -> b
$ [Char]
-> (RType RTyCon tv r -> RType RTyCon tv r -> RType RTyCon tv r)
-> [RType RTyCon tv r]
-> [RType RTyCon tv r]
-> [RType RTyCon tv r]
forall a b c.
HasCallStack =>
[Char] -> (a -> b -> c) -> [a] -> [b] -> [c]
safeZipWith ([Char]
msg [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
": substRCon")  RType RTyCon tv r -> RType RTyCon tv r -> RType RTyCon tv r
forall {b}. (Variable b ~ Symbol, Subable b, Meet b) => b -> b -> b
strSub  [RType RTyCon tv r]
ts1  [RType RTyCon tv r]
ts2
    rs :: [RTPropBV Symbol Symbol RTyCon tv r]
rs                     = SubstV (Variable [RTPropBV Symbol Symbol RTyCon tv r])
-> [RTPropBV Symbol Symbol RTyCon tv r]
-> [RTPropBV Symbol Symbol RTyCon tv r]
forall a.
(Subable a, HasCallStack) =>
SubstV (Variable a) -> a -> a
F.subst SubstV (Variable [RTPropBV Symbol Symbol RTyCon tv r])
SubstV (ReftBind r)
su ([RTPropBV Symbol Symbol RTyCon tv r]
 -> [RTPropBV Symbol Symbol RTyCon tv r])
-> [RTPropBV Symbol Symbol RTyCon tv r]
-> [RTPropBV Symbol Symbol RTyCon tv r]
forall a b. (a -> b) -> a -> b
$ [Char]
-> (RTPropBV Symbol Symbol RTyCon tv r
    -> RTPropBV Symbol Symbol RTyCon tv r
    -> RTPropBV Symbol Symbol RTyCon tv r)
-> [RTPropBV Symbol Symbol RTyCon tv r]
-> [RTPropBV Symbol Symbol RTyCon tv r]
-> [RTPropBV Symbol Symbol RTyCon tv r]
forall a b c.
HasCallStack =>
[Char] -> (a -> b -> c) -> [a] -> [b] -> [c]
safeZipWith ([Char]
msg [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
": substRCon2") RTPropBV Symbol Symbol RTyCon tv r
-> RTPropBV Symbol Symbol RTyCon tv r
-> RTPropBV Symbol Symbol RTyCon tv r
forall {r} {c} {tv} {τ}.
(Variable r ~ Symbol, ReftBind r ~ Symbol, TyConable c, IsReft r,
 Subable r, Meet (RType c tv r), PPrint tv, PPrint c, PPrint r,
 PPrint (ReftVar r), Fixpoint (ReftVar r), Ord (ReftVar r),
 Hashable tv, FreeVar c tv,
 SubsTy tv (RTypeBV Symbol Symbol c tv (NoReftB Symbol)) c,
 SubsTy tv (RTypeBV Symbol Symbol c tv (NoReftB Symbol)) r,
 SubsTy tv (RTypeBV Symbol Symbol c tv (NoReftB Symbol)) tv,
 SubsTy
   tv
   (RTypeBV Symbol Symbol c tv (NoReftB Symbol))
   (RTypeBV Symbol Symbol c tv (NoReftB Symbol)),
 SubsTy
   tv
   (RTypeBV Symbol Symbol c tv (NoReftB Symbol))
   (RTVar tv (RTypeBV Symbol Symbol c tv (NoReftB Symbol)))) =>
RefB Symbol τ (RType c tv r)
-> RefB Symbol τ (RType c tv r) -> RefB Symbol τ (RType c tv r)
strSubR [RTPropBV Symbol Symbol RTyCon tv r]
rs1' [RTPropBV Symbol Symbol RTyCon tv r]
rs2'
    ([RTPropBV Symbol Symbol RTyCon tv r]
rs1', [RTPropBV Symbol Symbol RTyCon tv r]
rs2')           = [Char]
-> (RTPropBV Symbol Symbol RTyCon tv r
    -> RTPropBV Symbol Symbol RTyCon tv r)
-> [RTPropBV Symbol Symbol RTyCon tv r]
-> [RTPropBV Symbol Symbol RTyCon tv r]
-> ([RTPropBV Symbol Symbol RTyCon tv r],
    [RTPropBV Symbol Symbol RTyCon tv r])
forall a. [Char] -> (a -> a) -> [a] -> [a] -> ([a], [a])
pad [Char]
"substRCon" RTPropBV Symbol Symbol RTyCon tv r
-> RTPropBV Symbol Symbol RTyCon tv r
forall r. Top r => r -> r
top [RTPropBV Symbol Symbol RTyCon tv r]
rs1 [RTPropBV Symbol Symbol RTyCon tv r]
rs2
    strSub :: b -> b -> b
strSub b
x b
r2           = [PVar t2] -> [(Symbol, RSort)] -> b -> b -> b
forall (t :: * -> *) t1 b.
(Foldable t, PPrint t1, Subable b, Variable b ~ Symbol, Meet b) =>
t (PVar t1) -> [(Symbol, RSort)] -> b -> b -> b
meetListWithPSubs [PVar t2]
πs [(Symbol, RSort)]
ss b
x b
r2
    strSubR :: RefB Symbol τ (RType c tv r)
-> RefB Symbol τ (RType c tv r) -> RefB Symbol τ (RType c tv r)
strSubR RefB Symbol τ (RType c tv r)
x RefB Symbol τ (RType c tv r)
r2          = [PVar t2]
-> [(Symbol, RSort)]
-> RefB Symbol τ (RType c tv r)
-> RefB Symbol τ (RType c tv r)
-> RefB Symbol τ (RType c tv r)
forall (t :: * -> *) c tv r t4 b τ.
(Foldable t, Meet (RType c tv r), TyConable c, IsReft r, Subable r,
 Variable r ~ Symbol, ReftBind r ~ Symbol) =>
t (PVar t4)
-> [(Symbol, b)]
-> Ref τ (RType c tv r)
-> Ref τ (RType c tv r)
-> Ref τ (RType c tv r)
meetListWithPSubsRef [PVar t2]
πs [(Symbol, RSort)]
ss RefB Symbol τ (RType c tv r)
x RefB Symbol τ (RType c tv r)
r2

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

    rvs :: RTypeBV (ReftBind r) v RTyCon tv r -> [ReftBind r]
rvs      = Bool
-> (SEnvB (ReftBind r) (RTypeBV (ReftBind r) v RTyCon tv r)
    -> r -> [ReftBind r] -> [ReftBind r])
-> [ReftBind r]
-> RTypeBV (ReftBind r) v RTyCon tv r
-> [ReftBind r]
forall r c b v tv z.
(IsReft r, TyConable c, Binder b, ReftBind r ~ b) =>
Bool
-> (SEnvB b (RTypeBV b v c tv r) -> r -> z -> z)
-> z
-> RTypeBV b v c tv r
-> z
foldReft Bool
False (\SEnvB (ReftBind r) (RTypeBV (ReftBind r) v RTyCon tv r)
_ r
r [ReftBind r]
acc -> r -> ReftBind r
forall {p}. ToReft p => p -> ReftBind p
rvReft r
r ReftBind r -> [ReftBind r] -> [ReftBind r]
forall a. a -> [a] -> [a]
: [ReftBind r]
acc) []
    rvReft :: p -> ReftBind p
rvReft p
r = let F.Reft(ReftBind p
s,ExprBV (ReftBind p) (ReftVar p)
_) = p -> ReftBV (ReftBind p) (ReftVar p)
forall r. ToReft r => r -> ReftBV (ReftBind r) (ReftVar r)
toReft p
r in ReftBind p
s

substRCon [Char]
msg (t, Ref RSort (RType RTyCon tv r))
su RType RTyCon tv r
t [PVar t2]
_ r
_        = {- panic Nothing -} [Char] -> [Char] -> RType RTyCon tv r
forall a. [Char] -> [Char] -> a
errorP [Char]
"substRCon: " ([Char] -> RType RTyCon tv r) -> [Char] -> RType RTyCon tv r
forall a b. (a -> b) -> a -> b
$ [Char]
msg [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ ((t, Ref RSort (RType RTyCon tv r)), RType RTyCon tv r) -> [Char]
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 (a -> a) -> [a] -> [a]
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 (a -> a) -> [a] -> [a]
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 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
nys  = ([a]
xs, [a]
ys)
  | Bool
otherwise   = Maybe SrcSpan -> [Char] -> ([a], [a])
forall a. HasCallStack => Maybe SrcSpan -> [Char] -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing ([Char] -> ([a], [a])) -> [Char] -> ([a], [a])
forall a b. (a -> b) -> a -> b
$ [Char]
"pad: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
msg
  where
    nxs :: Int
nxs         = [a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
xs
    nys :: Int
nys         = [a] -> Int
forall a. [a] -> Int
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
_))
  = Maybe SrcSpan -> [Char] -> Ref RSort (RRType RReft)
forall a. HasCallStack => Maybe SrcSpan -> [Char] -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing ([Char]
"PredType.substPredP1 called on invalid inputs: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ ((RPVar, Ref RSort (RRType RReft)), Ref RSort (RRType RReft))
-> [Char]
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)
  = [(Symbol, RSort)] -> RRType RReft -> Ref RSort (RRType RReft)
forall b τ t. [(b, τ)] -> t -> RefB b τ t
RProp [(Symbol, RSort)]
ss' (RRType RReft -> Ref RSort (RRType RReft))
-> RRType RReft -> Ref RSort (RRType RReft)
forall a b. (a -> b) -> a -> b
$ [Char]
-> (RPVar, Ref RSort (RRType RReft))
-> RRType RReft
-> RRType RReft
substPred ([Char]
msg [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
": substPredP") (RPVar
p, [(Symbol, RSort)] -> RRType RReft -> Ref RSort (RRType RReft)
forall b τ t. [(b, τ)] -> t -> RefB b τ t
RProp [(Symbol, RSort)]
ss {- (subst su prop) -} RRType RReft
prop ) RRType RReft
t
 where
   ss' :: [(Symbol, RSort)]
ss' = Int -> [(Symbol, RSort)] -> [(Symbol, RSort)]
forall a. Int -> [a] -> [a]
drop Int
n [(Symbol, RSort)]
ss [(Symbol, RSort)] -> [(Symbol, RSort)] -> [(Symbol, RSort)]
forall a. [a] -> [a] -> [a]
++  [(Symbol, RSort)]
s
   n :: Int
n   = [(Symbol, RSort)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Symbol, RSort)]
ss Int -> Int -> Int
forall a. Num a => a -> a -> a
- [Symbol] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (RPVar -> RRType RReft -> [Symbol]
forall t t1 t2.
PVar (RType t t1 (NoReftB Symbol))
-> 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)) = (r -> PredicateBV Symbol Symbol -> UReftBV Symbol Symbol r
forall b v r. r -> PredicateBV b v -> UReftBV b v r
MkUReft r
x ([UsedPVar] -> PredicateBV Symbol Symbol
forall b v. [UsedPVarBV b v] -> PredicateBV b v
Pr [UsedPVar]
pvs'), [UsedPVar]
epvs)
  where
    ([UsedPVar]
epvs, [UsedPVar]
pvs')               = (UsedPVar -> Bool) -> [UsedPVar] -> ([UsedPVar], [UsedPVar])
forall a. (a -> Bool) -> [a] -> ([a], [a])
L.partition (PVar t -> UsedPVar
forall v t. PVarV v t -> UsedPVarV v
uPVar PVar t
pv UsedPVar -> UsedPVar -> Bool
forall a. Eq a => a -> a -> Bool
==) [UsedPVar]
pvs

-- TODO: rewrite using foldReft
freeArgsPs :: PVar (RType t t1 NoReft) -> RType t t1 (UReft t2) -> [F.Symbol]
freeArgsPs :: forall t t1 t2.
PVar (RType t t1 (NoReftB Symbol))
-> RType t t1 (UReft t2) -> [Symbol]
freeArgsPs PVarBV Symbol Symbol (RType t t1 (NoReftB Symbol))
p (RVar t1
_ UReft t2
r)
  = PVarBV Symbol Symbol (RType t t1 (NoReftB Symbol))
-> UReft t2 -> [Symbol]
forall t1 t. PVar t1 -> UReft t -> [Symbol]
freeArgsPsRef PVarBV Symbol Symbol (RType t t1 (NoReftB Symbol))
p UReft t2
r
freeArgsPs PVarBV Symbol Symbol (RType t t1 (NoReftB Symbol))
p (RFun Symbol
_ RFInfo
_ RTypeBV Symbol Symbol t t1 (UReft t2)
t1 RTypeBV Symbol Symbol t t1 (UReft t2)
t2 UReft t2
r)
  = [Symbol] -> [Symbol]
forall a. Eq a => [a] -> [a]
L.nub ([Symbol] -> [Symbol]) -> [Symbol] -> [Symbol]
forall a b. (a -> b) -> a -> b
$  PVarBV Symbol Symbol (RType t t1 (NoReftB Symbol))
-> UReft t2 -> [Symbol]
forall t1 t. PVar t1 -> UReft t -> [Symbol]
freeArgsPsRef PVarBV Symbol Symbol (RType t t1 (NoReftB Symbol))
p UReft t2
r [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ PVarBV Symbol Symbol (RType t t1 (NoReftB Symbol))
-> RTypeBV Symbol Symbol t t1 (UReft t2) -> [Symbol]
forall t t1 t2.
PVar (RType t t1 (NoReftB Symbol))
-> RType t t1 (UReft t2) -> [Symbol]
freeArgsPs PVarBV Symbol Symbol (RType t t1 (NoReftB Symbol))
p RTypeBV Symbol Symbol t t1 (UReft t2)
t1 [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ PVarBV Symbol Symbol (RType t t1 (NoReftB Symbol))
-> RTypeBV Symbol Symbol t t1 (UReft t2) -> [Symbol]
forall t t1 t2.
PVar (RType t t1 (NoReftB Symbol))
-> RType t t1 (UReft t2) -> [Symbol]
freeArgsPs PVarBV Symbol Symbol (RType t t1 (NoReftB Symbol))
p RTypeBV Symbol Symbol t t1 (UReft t2)
t2
freeArgsPs PVarBV Symbol Symbol (RType t t1 (NoReftB Symbol))
p (RAllT RTVUBV Symbol Symbol t t1
_ RTypeBV Symbol Symbol t t1 (UReft t2)
t UReft t2
r)
  = [Symbol] -> [Symbol]
forall a. Eq a => [a] -> [a]
L.nub ([Symbol] -> [Symbol]) -> [Symbol] -> [Symbol]
forall a b. (a -> b) -> a -> b
$  PVarBV Symbol Symbol (RType t t1 (NoReftB Symbol))
-> RTypeBV Symbol Symbol t t1 (UReft t2) -> [Symbol]
forall t t1 t2.
PVar (RType t t1 (NoReftB Symbol))
-> RType t t1 (UReft t2) -> [Symbol]
freeArgsPs PVarBV Symbol Symbol (RType t t1 (NoReftB Symbol))
p RTypeBV Symbol Symbol t t1 (UReft t2)
t [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ PVarBV Symbol Symbol (RType t t1 (NoReftB Symbol))
-> UReft t2 -> [Symbol]
forall t1 t. PVar t1 -> UReft t -> [Symbol]
freeArgsPsRef PVarBV Symbol Symbol (RType t t1 (NoReftB Symbol))
p UReft t2
r
freeArgsPs PVarBV Symbol Symbol (RType t t1 (NoReftB Symbol))
p (RAllP PVarBV Symbol Symbol (RType t t1 (NoReftB Symbol))
p' RTypeBV Symbol Symbol t t1 (UReft t2)
t)
  | PVarBV Symbol Symbol (RType t t1 (NoReftB Symbol))
p PVarBV Symbol Symbol (RType t t1 (NoReftB Symbol))
-> PVarBV Symbol Symbol (RType t t1 (NoReftB Symbol)) -> Bool
forall a. Eq a => a -> a -> Bool
== PVarBV Symbol Symbol (RType t t1 (NoReftB Symbol))
p'   = []
  | Bool
otherwise = PVarBV Symbol Symbol (RType t t1 (NoReftB Symbol))
-> RTypeBV Symbol Symbol t t1 (UReft t2) -> [Symbol]
forall t t1 t2.
PVar (RType t t1 (NoReftB Symbol))
-> RType t t1 (UReft t2) -> [Symbol]
freeArgsPs PVarBV Symbol Symbol (RType t t1 (NoReftB Symbol))
p RTypeBV Symbol Symbol t t1 (UReft t2)
t
freeArgsPs PVarBV Symbol Symbol (RType t t1 (NoReftB Symbol))
p (RApp t
_ [RTypeBV Symbol Symbol t t1 (UReft t2)]
ts [RTPropBV Symbol Symbol t t1 (UReft t2)]
_ UReft t2
r)
  = [Symbol] -> [Symbol]
forall a. Eq a => [a] -> [a]
L.nub ([Symbol] -> [Symbol]) -> [Symbol] -> [Symbol]
forall a b. (a -> b) -> a -> b
$ PVarBV Symbol Symbol (RType t t1 (NoReftB Symbol))
-> UReft t2 -> [Symbol]
forall t1 t. PVar t1 -> UReft t -> [Symbol]
freeArgsPsRef PVarBV Symbol Symbol (RType t t1 (NoReftB Symbol))
p UReft t2
r [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ (RTypeBV Symbol Symbol t t1 (UReft t2) -> [Symbol])
-> [RTypeBV Symbol Symbol t t1 (UReft t2)] -> [Symbol]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (PVarBV Symbol Symbol (RType t t1 (NoReftB Symbol))
-> RTypeBV Symbol Symbol t t1 (UReft t2) -> [Symbol]
forall t t1 t2.
PVar (RType t t1 (NoReftB Symbol))
-> RType t t1 (UReft t2) -> [Symbol]
freeArgsPs PVarBV Symbol Symbol (RType t t1 (NoReftB Symbol))
p) [RTypeBV Symbol Symbol t t1 (UReft t2)]
ts
freeArgsPs PVarBV Symbol Symbol (RType t t1 (NoReftB Symbol))
p (RAllE Symbol
_ RTypeBV Symbol Symbol t t1 (UReft t2)
t1 RTypeBV Symbol Symbol t t1 (UReft t2)
t2)
  = [Symbol] -> [Symbol]
forall a. Eq a => [a] -> [a]
L.nub ([Symbol] -> [Symbol]) -> [Symbol] -> [Symbol]
forall a b. (a -> b) -> a -> b
$ PVarBV Symbol Symbol (RType t t1 (NoReftB Symbol))
-> RTypeBV Symbol Symbol t t1 (UReft t2) -> [Symbol]
forall t t1 t2.
PVar (RType t t1 (NoReftB Symbol))
-> RType t t1 (UReft t2) -> [Symbol]
freeArgsPs PVarBV Symbol Symbol (RType t t1 (NoReftB Symbol))
p RTypeBV Symbol Symbol t t1 (UReft t2)
t1 [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ PVarBV Symbol Symbol (RType t t1 (NoReftB Symbol))
-> RTypeBV Symbol Symbol t t1 (UReft t2) -> [Symbol]
forall t t1 t2.
PVar (RType t t1 (NoReftB Symbol))
-> RType t t1 (UReft t2) -> [Symbol]
freeArgsPs PVarBV Symbol Symbol (RType t t1 (NoReftB Symbol))
p RTypeBV Symbol Symbol t t1 (UReft t2)
t2
freeArgsPs PVarBV Symbol Symbol (RType t t1 (NoReftB Symbol))
p (REx Symbol
_ RTypeBV Symbol Symbol t t1 (UReft t2)
t1 RTypeBV Symbol Symbol t t1 (UReft t2)
t2)
  = [Symbol] -> [Symbol]
forall a. Eq a => [a] -> [a]
L.nub ([Symbol] -> [Symbol]) -> [Symbol] -> [Symbol]
forall a b. (a -> b) -> a -> b
$ PVarBV Symbol Symbol (RType t t1 (NoReftB Symbol))
-> RTypeBV Symbol Symbol t t1 (UReft t2) -> [Symbol]
forall t t1 t2.
PVar (RType t t1 (NoReftB Symbol))
-> RType t t1 (UReft t2) -> [Symbol]
freeArgsPs PVarBV Symbol Symbol (RType t t1 (NoReftB Symbol))
p RTypeBV Symbol Symbol t t1 (UReft t2)
t1 [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ PVarBV Symbol Symbol (RType t t1 (NoReftB Symbol))
-> RTypeBV Symbol Symbol t t1 (UReft t2) -> [Symbol]
forall t t1 t2.
PVar (RType t t1 (NoReftB Symbol))
-> RType t t1 (UReft t2) -> [Symbol]
freeArgsPs PVarBV Symbol Symbol (RType t t1 (NoReftB Symbol))
p RTypeBV Symbol Symbol t t1 (UReft t2)
t2
freeArgsPs PVarBV Symbol Symbol (RType t t1 (NoReftB Symbol))
p (RAppTy RTypeBV Symbol Symbol t t1 (UReft t2)
t1 RTypeBV Symbol Symbol t t1 (UReft t2)
t2 UReft t2
r)
  = [Symbol] -> [Symbol]
forall a. Eq a => [a] -> [a]
L.nub ([Symbol] -> [Symbol]) -> [Symbol] -> [Symbol]
forall a b. (a -> b) -> a -> b
$ PVarBV Symbol Symbol (RType t t1 (NoReftB Symbol))
-> UReft t2 -> [Symbol]
forall t1 t. PVar t1 -> UReft t -> [Symbol]
freeArgsPsRef PVarBV Symbol Symbol (RType t t1 (NoReftB Symbol))
p UReft t2
r [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ PVarBV Symbol Symbol (RType t t1 (NoReftB Symbol))
-> RTypeBV Symbol Symbol t t1 (UReft t2) -> [Symbol]
forall t t1 t2.
PVar (RType t t1 (NoReftB Symbol))
-> RType t t1 (UReft t2) -> [Symbol]
freeArgsPs PVarBV Symbol Symbol (RType t t1 (NoReftB Symbol))
p RTypeBV Symbol Symbol t t1 (UReft t2)
t1 [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ PVarBV Symbol Symbol (RType t t1 (NoReftB Symbol))
-> RTypeBV Symbol Symbol t t1 (UReft t2) -> [Symbol]
forall t t1 t2.
PVar (RType t t1 (NoReftB Symbol))
-> RType t t1 (UReft t2) -> [Symbol]
freeArgsPs PVarBV Symbol Symbol (RType t t1 (NoReftB Symbol))
p RTypeBV Symbol Symbol t t1 (UReft t2)
t2
freeArgsPs PVarBV Symbol Symbol (RType t t1 (NoReftB Symbol))
_ (RExprArg Located Expr
_)
  = []
freeArgsPs PVarBV Symbol Symbol (RType t t1 (NoReftB Symbol))
p (RHole UReft t2
r)
  = PVarBV Symbol Symbol (RType t t1 (NoReftB Symbol))
-> UReft t2 -> [Symbol]
forall t1 t. PVar t1 -> UReft t -> [Symbol]
freeArgsPsRef PVarBV Symbol Symbol (RType t t1 (NoReftB Symbol))
p UReft t2
r
freeArgsPs PVarBV Symbol Symbol (RType t t1 (NoReftB Symbol))
p (RRTy [(Symbol, RTypeBV Symbol Symbol t t1 (UReft t2))]
env UReft t2
r Oblig
_ RTypeBV Symbol Symbol t t1 (UReft t2)
t)
  = [Symbol] -> [Symbol]
forall a. Eq a => [a] -> [a]
L.nub ([Symbol] -> [Symbol]) -> [Symbol] -> [Symbol]
forall a b. (a -> b) -> a -> b
$ ((Symbol, RTypeBV Symbol Symbol t t1 (UReft t2)) -> [Symbol])
-> [(Symbol, RTypeBV Symbol Symbol t t1 (UReft t2))] -> [Symbol]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (PVarBV Symbol Symbol (RType t t1 (NoReftB Symbol))
-> RTypeBV Symbol Symbol t t1 (UReft t2) -> [Symbol]
forall t t1 t2.
PVar (RType t t1 (NoReftB Symbol))
-> RType t t1 (UReft t2) -> [Symbol]
freeArgsPs PVarBV Symbol Symbol (RType t t1 (NoReftB Symbol))
p (RTypeBV Symbol Symbol t t1 (UReft t2) -> [Symbol])
-> ((Symbol, RTypeBV Symbol Symbol t t1 (UReft t2))
    -> RTypeBV Symbol Symbol t t1 (UReft t2))
-> (Symbol, RTypeBV Symbol Symbol t t1 (UReft t2))
-> [Symbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol, RTypeBV Symbol Symbol t t1 (UReft t2))
-> RTypeBV Symbol Symbol t t1 (UReft t2)
forall a b. (a, b) -> b
snd) [(Symbol, RTypeBV Symbol Symbol t t1 (UReft t2))]
env [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ PVarBV Symbol Symbol (RType t t1 (NoReftB Symbol))
-> UReft t2 -> [Symbol]
forall t1 t. PVar t1 -> UReft t -> [Symbol]
freeArgsPsRef PVarBV Symbol Symbol (RType t t1 (NoReftB Symbol))
p UReft t2
r [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ PVarBV Symbol Symbol (RType t t1 (NoReftB Symbol))
-> RTypeBV Symbol Symbol t t1 (UReft t2) -> [Symbol]
forall t t1 t2.
PVar (RType t t1 (NoReftB Symbol))
-> RType t t1 (UReft t2) -> [Symbol]
freeArgsPs PVarBV Symbol Symbol (RType t t1 (NoReftB Symbol))
p RTypeBV Symbol Symbol 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) <- (UsedPVar -> [((), Symbol, Expr)])
-> [UsedPVar] -> [((), Symbol, Expr)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap UsedPVar -> [((), Symbol, Expr)]
forall b v t. PVarBV b v t -> [(t, b, ExprBV b v)]
pargs [UsedPVar]
ps', Symbol -> Expr
forall b v. v -> ExprBV b v
F.EVar Symbol
x Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
w]
  where
   ps' :: [UsedPVar]
ps' = UsedPVar -> UsedPVar
f (UsedPVar -> UsedPVar) -> [UsedPVar] -> [UsedPVar]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (UsedPVar -> Bool) -> [UsedPVar] -> [UsedPVar]
forall a. (a -> Bool) -> [a] -> [a]
filter (PVar t1 -> UsedPVar
forall v t. PVarV v t -> UsedPVarV v
uPVar PVar t1
p UsedPVar -> UsedPVar -> Bool
forall a. Eq a => a -> a -> Bool
==) [UsedPVar]
ps
   f :: UsedPVar -> UsedPVar
f UsedPVar
q = UsedPVar
q {pargs = pargs q ++ drop (length (pargs q)) (pargs $ uPVar p)}

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

meetListWithPSubsRef :: (Foldable t, Meet (RType c tv r), TyConable c, IsReft r, F.Subable r, F.Variable r ~ F.Symbol, ReftBind r ~ F.Symbol)
                     => t (PVar t4)
                     -> [(F.Symbol, b)]
                     -> Ref τ (RType c tv r)
                     -> Ref τ (RType c tv r)
                     -> Ref τ (RType c tv r)
meetListWithPSubsRef :: forall (t :: * -> *) c tv r t4 b τ.
(Foldable t, Meet (RType c tv r), TyConable c, IsReft r, Subable r,
 Variable r ~ Symbol, ReftBind r ~ Symbol) =>
t (PVar t4)
-> [(Symbol, b)]
-> Ref τ (RType c tv r)
-> Ref τ (RType c tv r)
-> Ref τ (RType c tv r)
meetListWithPSubsRef t (PVar t4)
πs [(Symbol, b)]
ss Ref τ (RType c tv r)
r1 Ref τ (RType c tv r)
r2 = (Ref τ (RType c tv r) -> PVar t4 -> Ref τ (RType c tv r))
-> Ref τ (RType c tv r) -> t (PVar t4) -> Ref τ (RType c tv r)
forall b a. (b -> a -> b) -> b -> t a -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' ([(Symbol, b)]
-> Ref τ (RType c tv r)
-> Ref τ (RType c tv r)
-> PVar t4
-> Ref τ (RType c tv r)
forall c tv r b τ t3.
(Meet (RType c tv r), TyConable c, IsReft r, Subable r,
 Variable r ~ Symbol, ReftBind r ~ Symbol) =>
[(Symbol, b)]
-> Ref τ (RType c tv r)
-> Ref τ (RType c tv r)
-> PVar t3
-> Ref τ (RType c tv r)
meetListWithPSubRef [(Symbol, b)]
ss Ref τ (RType c tv r)
r1) Ref τ (RType c tv r)
r2 t (PVar t4)
πs

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

meetListWithPSubRef :: (Meet (RType c tv r), TyConable c, IsReft r, F.Subable r, F.Variable r ~ F.Symbol, ReftBind r ~ F.Symbol)
                    => [(F.Symbol, b)]
                    -> Ref τ (RType c tv r)
                    -> Ref τ (RType c tv r)
                    -> PVar t3
                    -> Ref τ (RType c tv r)
meetListWithPSubRef :: forall c tv r b τ t3.
(Meet (RType c tv r), TyConable c, IsReft r, Subable r,
 Variable r ~ Symbol, ReftBind r ~ Symbol) =>
[(Symbol, b)]
-> Ref τ (RType c tv r)
-> Ref τ (RType c tv r)
-> PVar t3
-> Ref τ (RType c tv r)
meetListWithPSubRef [(Symbol, b)]
_ (RProp [(Symbol, τ)]
_ (RHole r
_)) RefB Symbol τ (RType c tv r)
_ PVarBV Symbol Symbol t3
_ -- TODO: Is this correct?
  = Maybe SrcSpan -> [Char] -> RefB Symbol τ (RType c tv r)
forall a. HasCallStack => Maybe SrcSpan -> [Char] -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing [Char]
"PredType.meetListWithPSubRef called with invalid input"
meetListWithPSubRef [(Symbol, b)]
_ RefB Symbol τ (RType c tv r)
_ (RProp [(Symbol, τ)]
_ (RHole r
_)) PVarBV Symbol Symbol t3
_
  = Maybe SrcSpan -> [Char] -> RefB Symbol τ (RType c tv r)
forall a. HasCallStack => Maybe SrcSpan -> [Char] -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing [Char]
"PredType.meetListWithPSubRef called with invalid input"
meetListWithPSubRef [(Symbol, b)]
ss (RProp [(Symbol, τ)]
s1 RType c tv r
r1) (RProp [(Symbol, τ)]
s2 RType c tv r
r2) PVarBV Symbol Symbol t3
π
  | ((t3, Symbol, Expr) -> Bool) -> [(t3, Symbol, Expr)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\(t3
_, Symbol
x, F.EVar Symbol
y) -> Symbol
x Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
y) (PVarBV Symbol Symbol t3 -> [(t3, Symbol, Expr)]
forall b v t. PVarBV b v t -> [(t, b, ExprBV b v)]
pargs PVarBV Symbol Symbol t3
π)
  = [(Symbol, τ)] -> RType c tv r -> RefB Symbol τ (RType c tv r)
forall b τ t. [(b, τ)] -> t -> RefB b τ t
RProp [(Symbol, τ)]
s1 (RType c tv r -> RefB Symbol τ (RType c tv r))
-> RType c tv r -> RefB Symbol τ (RType c tv r)
forall a b. (a -> b) -> a -> b
$ SubstV (Variable (RType c tv r)) -> RType c tv r -> RType c tv r
forall a.
(Subable a, HasCallStack) =>
SubstV (Variable a) -> a -> a
F.subst SubstV Symbol
SubstV (Variable (RType c tv r))
su' RType c tv r
r2 RType c tv r -> RType c tv r -> RType c tv r
forall r. Meet r => r -> r -> r
`meet` RType c tv r
r1
  | ((t3, Symbol, Expr) -> Bool) -> [(t3, Symbol, Expr)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\(t3
_, Symbol
x, F.EVar Symbol
y) -> Symbol
x Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
/= Symbol
y) (PVarBV Symbol Symbol t3 -> [(t3, Symbol, Expr)]
forall b v t. PVarBV b v t -> [(t, b, ExprBV b v)]
pargs PVarBV Symbol Symbol t3
π)
  = [(Symbol, τ)] -> RType c tv r -> RefB Symbol τ (RType c tv r)
forall b τ t. [(b, τ)] -> t -> RefB b τ t
RProp [(Symbol, τ)]
s2 (RType c tv r -> RefB Symbol τ (RType c tv r))
-> RType c tv r -> RefB Symbol τ (RType c tv r)
forall a b. (a -> b) -> a -> b
$ RType c tv r
r2 RType c tv r -> RType c tv r -> RType c tv r
forall r. Meet r => r -> r -> r
`meet` SubstV (Variable (RType c tv r)) -> RType c tv r -> RType c tv r
forall a.
(Subable a, HasCallStack) =>
SubstV (Variable a) -> a -> a
F.subst SubstV Symbol
SubstV (Variable (RType c tv r))
su RType c tv r
r1
  | Bool
otherwise
  = Maybe SrcSpan -> [Char] -> RefB Symbol τ (RType c tv r)
forall a. HasCallStack => Maybe SrcSpan -> [Char] -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing ([Char] -> RefB Symbol τ (RType c tv r))
-> [Char] -> RefB Symbol τ (RType c tv r)
forall a b. (a -> b) -> a -> b
$ [Char]
"PredType.meetListWithPSubRef partial application to " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ PVarBV Symbol Symbol t3 -> [Char]
forall a. PPrint a => a -> [Char]
showpp PVarBV Symbol Symbol t3
π
  where
    su :: SubstV Symbol
su  = [(Symbol, Expr)] -> SubstV Symbol
forall v. Hashable v => [(v, ExprBV v v)] -> SubstV v
F.mkSubst [(Symbol
x, Expr
y) | (Symbol
x, (t3
_, Symbol
_, Expr
y)) <- [Symbol] -> [(t3, Symbol, Expr)] -> [(Symbol, (t3, Symbol, Expr))]
forall a b. [a] -> [b] -> [(a, b)]
zip ((Symbol, b) -> Symbol
forall a b. (a, b) -> a
fst ((Symbol, b) -> Symbol) -> [(Symbol, b)] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, b)]
ss) (PVarBV Symbol Symbol t3 -> [(t3, Symbol, Expr)]
forall b v t. PVarBV b v t -> [(t, b, ExprBV b v)]
pargs PVarBV Symbol Symbol t3
π)]
    su' :: SubstV Symbol
su' = [(Symbol, Expr)] -> SubstV Symbol
forall v. Hashable v => [(v, ExprBV v v)] -> SubstV v
F.mkSubst [(Symbol
x, Symbol -> Expr
forall b v. v -> ExprBV b v
F.EVar Symbol
y) | (Symbol
x, Symbol
y) <- [Symbol] -> [Symbol] -> [(Symbol, Symbol)]
forall a b. [a] -> [b] -> [(a, b)]
zip ((Symbol, τ) -> Symbol
forall a b. (a, b) -> a
fst ((Symbol, τ) -> Symbol) -> [(Symbol, τ)] -> [Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, τ)]
s2) ((Symbol, τ) -> Symbol
forall a b. (a, b) -> a
fst ((Symbol, τ) -> Symbol) -> [(Symbol, τ)] -> [Symbol]
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

predName :: F.Symbol
predName :: Symbol
predName   = Symbol
"Pred"

symbolType :: F.Symbol -> Type
symbolType :: Symbol -> Type
symbolType = TyVar -> Type
TyVarTy (TyVar -> Type) -> (Symbol -> TyVar) -> Symbol -> Type
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 (PredicateBV Symbol Symbol) -> f (PredicateBV Symbol Symbol)
substParg (Symbol
x, Expr
y) = (PredicateBV Symbol Symbol -> PredicateBV Symbol Symbol)
-> f (PredicateBV Symbol Symbol) -> f (PredicateBV Symbol Symbol)
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap PredicateBV Symbol Symbol -> PredicateBV Symbol Symbol
fp
  where
    fxy :: Expr -> Expr
fxy Expr
s        = if Expr
s Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol -> Expr
forall b v. v -> ExprBV b v
F.EVar Symbol
x then Expr
y else Expr
s
    fp :: PredicateBV Symbol Symbol -> PredicateBV Symbol Symbol
fp           = (UsedPVar -> UsedPVar)
-> PredicateBV Symbol Symbol -> PredicateBV Symbol Symbol
subvPredicate (\UsedPVar
pv -> UsedPVar
pv { pargs = mapThd3 fxy <$> pargs 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 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
n) ([Sort] -> Sort) -> [Sort] -> Sort
forall a b. (a -> b) -> a -> b
$ [Sort
ptycon] [Sort] -> [Sort] -> [Sort]
forall a. [a] -> [a] -> [a]
++ [Sort]
args [Sort] -> [Sort] -> [Sort]
forall a. [a] -> [a] -> [a]
++ [Sort
F.boolSort]
  where
    ptycon :: Sort
ptycon = FTycon -> [Sort] -> Sort
F.fAppTC FTycon
predFTyCon ([Sort] -> Sort) -> [Sort] -> Sort
forall a b. (a -> b) -> a -> b
$ Int -> Sort
F.FVar (Int -> Sort) -> [Int] -> [Sort]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Int
0..Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1]
    args :: [Sort]
args   = Int -> Sort
F.FVar (Int -> Sort) -> [Int] -> [Sort]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Int
n..(Int
2Int -> Int -> Int
forall a. Num a => a -> a -> a
*Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)]


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