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

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
  ) where

import           Prelude                         hiding (error)
import           DataCon
import           Text.PrettyPrint.HughesPJ
import           Language.Haskell.Liquid.GHC.API
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 Language.Haskell.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 :: HashMap TyCon RTyCon
-> HashMap (TyCon, [Sort]) RTyCon -> HashMap TyCon Int -> TyConMap
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. (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     = String -> [(TyCon, Int)] -> HashMap TyCon Int
forall k v.
(?callStack::CallStack, Eq k, Hashable k, Show k) =>
String -> [(k, v)] -> HashMap k v
safeFromList String
"makeTyConInfo" [ (TyCon
c, [Sort] -> 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. (Eq k, 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. (Eq k, 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' [PVar RSort]
ps VarianceInfo
tyvariance VarianceInfo
predvariance Maybe SizeFun
size)
  = TyCon -> [PVar RSort] -> TyConInfo -> RTyCon
RTyCon TyCon
tc [PVar RSort]
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. Monoid r => TyVar -> RType c RTyVar r
rVar TyVar
α :: RSort |  TyVar
α <- TyCon -> [TyVar]
tyConTyVarsDef TyCon
tc]
    pvs' :: [PVar RSort]
pvs' = [(RTyVar, RSort)] -> PVar RSort -> PVar RSort
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) (PVar RSort -> PVar RSort) -> [PVar RSort] -> [PVar RSort]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [PVar RSort]
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 :: DataConP -> [(Var, SpecType)]
-------------------------------------------------------------------------------
dataConPSpecType :: DataConP -> [(TyVar, SpecType)]
dataConPSpecType DataConP
dcp    = [(TyVar
workX, SpecType
workT), (TyVar
wrapX, SpecType
wrapT) ]
  where
    workT :: SpecType
workT | Bool
isVanilla   = SpecType
wrapT
          | Bool
otherwise   = DataCon -> SpecType -> SpecType
dcWorkSpecType   DataCon
dc SpecType
wrapT
    wrapT :: SpecType
wrapT               = DataCon -> DataConP -> SpecType
dcWrapSpecType   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 -> SpecType -> SpecType
dcWorkSpecType DataCon
c SpecType
wrT    = RTypeRep RTyCon RTyVar RReft -> SpecType
forall c tv r. RTypeRep c tv r -> RType c tv r
fromRTypeRep (DataCon
-> RTypeRep RTyCon RTyVar RReft
-> RTypeRep RTyCon RTyVar RReft
-> RTypeRep RTyCon RTyVar RReft
meetWorkWrapRep DataCon
c RTypeRep RTyCon RTyVar RReft
wkR RTypeRep RTyCon RTyVar RReft
wrR)
  where
    wkR :: RTypeRep RTyCon RTyVar RReft
wkR                 = DataCon -> RTypeRep RTyCon RTyVar RReft
dataConWorkRep DataCon
c
    wrR :: RTypeRep RTyCon RTyVar RReft
wrR                 = SpecType -> RTypeRep RTyCon RTyVar RReft
forall c tv r. RType c tv r -> RTypeRep c tv r
toRTypeRep SpecType
wrT

dataConWorkRep :: DataCon -> SpecRep
dataConWorkRep :: DataCon -> RTypeRep RTyCon RTyVar RReft
dataConWorkRep DataCon
c = SpecType -> RTypeRep RTyCon RTyVar RReft
forall c tv r. RType c tv r -> RTypeRep c tv r
toRTypeRep
                 -- . F.tracepp ("DCWR-2: " ++ F.showpp c)
                 (SpecType -> RTypeRep RTyCon RTyVar RReft)
-> (DataCon -> SpecType) -> DataCon -> RTypeRep RTyCon RTyVar RReft
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> SpecType
forall r. Monoid r => Type -> RRType r
ofType
                 -- . F.tracepp ("DCWR-1: " ++ F.showpp c)
                 (Type -> SpecType) -> (DataCon -> Type) -> DataCon -> SpecType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataCon -> Type
dataConRepType
                 -- . Var.varType
                 -- . dataConWorkId
                 (DataCon -> RTypeRep RTyCon RTyVar RReft)
-> DataCon -> RTypeRep 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
-> RTypeRep RTyCon RTyVar RReft
-> RTypeRep RTyCon RTyVar RReft
-> RTypeRep RTyCon RTyVar RReft
meetWorkWrapRep DataCon
c RTypeRep RTyCon RTyVar RReft
workR RTypeRep RTyCon RTyVar RReft
wrapR
  | Int
0 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
pad
  = RTypeRep RTyCon RTyVar RReft
workR { ty_binds :: [Symbol]
ty_binds = [Symbol]
xs [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ (RTypeRep RTyCon RTyVar RReft -> [Symbol]
forall c tv r. RTypeRep c tv r -> [Symbol]
ty_binds RTypeRep RTyCon RTyVar RReft
wrapR)
          , ty_args :: [SpecType]
ty_args  = [SpecType]
ts [SpecType] -> [SpecType] -> [SpecType]
forall a. [a] -> [a] -> [a]
++ (SpecType -> SpecType -> SpecType)
-> [SpecType] -> [SpecType] -> [SpecType]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith SpecType -> SpecType -> SpecType
forall r. Reftable r => r -> r -> r
F.meet [SpecType]
ts' (RTypeRep RTyCon RTyVar RReft -> [SpecType]
forall c tv r. RTypeRep c tv r -> [RType c tv r]
ty_args RTypeRep RTyCon RTyVar RReft
wrapR) 
          , ty_res :: SpecType
ty_res   = SpecType -> SpecType -> SpecType
strengthenRType (RTypeRep RTyCon RTyVar RReft -> SpecType
forall c tv r. RTypeRep c tv r -> RType c tv r
ty_res RTypeRep RTyCon RTyVar RReft
workR)    (RTypeRep RTyCon RTyVar RReft -> SpecType
forall c tv r. RTypeRep c tv r -> RType c tv r
ty_res  RTypeRep RTyCon RTyVar RReft
wrapR)
          , ty_preds :: [PVar RSort]
ty_preds = RTypeRep RTyCon RTyVar RReft -> [PVar RSort]
forall c tv r. RTypeRep c tv r -> [PVar (RType c tv ())]
ty_preds RTypeRep RTyCon RTyVar RReft
wrapR
          }
  | Bool
otherwise
  = Maybe SrcSpan -> String -> RTypeRep RTyCon RTyVar RReft
forall a. Maybe SrcSpan -> String -> a
panic (SrcSpan -> Maybe SrcSpan
forall a. a -> Maybe a
Just (DataCon -> SrcSpan
forall a. NamedThing a => a -> SrcSpan
getSrcSpan DataCon
c)) String
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 (RTypeRep RTyCon RTyVar RReft -> [Symbol]
forall c tv r. RTypeRep c tv r -> [Symbol]
ty_binds RTypeRep RTyCon RTyVar RReft
workR)
    ([SpecType]
ts, [SpecType]
ts') = Int -> [SpecType] -> ([SpecType], [SpecType])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
pad (RTypeRep RTyCon RTyVar RReft -> [SpecType]
forall c tv r. RTypeRep c tv r -> [RType c tv r]
ty_args  RTypeRep RTyCon RTyVar RReft
workR)
    workN :: Int
workN     = [SpecType] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length      (RTypeRep RTyCon RTyVar RReft -> [SpecType]
forall c tv r. RTypeRep c tv r -> [RType c tv r]
ty_args  RTypeRep RTyCon RTyVar RReft
workR)
    wrapN :: Int
wrapN     = [SpecType] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length      (RTypeRep RTyCon RTyVar RReft -> [SpecType]
forall c tv r. RTypeRep c tv r -> [RType c tv r]
ty_args  RTypeRep RTyCon RTyVar RReft
wrapR)
    errMsg :: String
errMsg    = String
"Unsupported Work/Wrap types for Data Constructor " String -> String -> String
forall a. [a] -> [a] -> [a]
++ DataCon -> String
forall a. Outputable a => a -> String
showPpr DataCon
c

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

dcWrapSpecType :: DataCon -> DataConP -> SpecType
dcWrapSpecType :: DataCon -> DataConP -> SpecType
dcWrapSpecType DataCon
dc (DataConP SourcePos
_ DataCon
_ [RTyVar]
vs [PVar RSort]
ps [SpecType]
cs [(Symbol, SpecType)]
yts SpecType
rt Bool
_ Symbol
_ SourcePos
_)
  = {- F.tracepp ("dcWrapSpecType: " ++ show dc ++ " " ++ F.showpp rt) $ -}
    [(RTVar RTyVar RSort, RReft)]
-> [PVar RSort]
-> [(Symbol, SpecType, RReft)]
-> [(Symbol, SpecType, RReft)]
-> SpecType
-> SpecType
forall tv c r.
[(RTVar tv (RType c tv ()), r)]
-> [PVar (RType c tv ())]
-> [(Symbol, RType c tv r, r)]
-> [(Symbol, RType c tv r, r)]
-> RType c tv r
-> RType c tv r
mkArrow [(RTVar RTyVar RSort, RReft)]
makeVars' [PVar RSort]
ps [] [(Symbol, SpecType, RReft)]
ts' SpecType
rt'
  where
    ([Symbol]
xs, [SpecType]
ts) = [(Symbol, SpecType)] -> ([Symbol], [SpecType])
forall a b. [(a, b)] -> ([a], [b])
unzip ([(Symbol, SpecType)] -> [(Symbol, SpecType)]
forall a. [a] -> [a]
reverse [(Symbol, SpecType)]
yts)
    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)
    ys :: [Symbol]
ys       = 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]
xs
    tx :: [(Symbol, Expr)] -> [Symbol] -> [Symbol] -> [b] -> [(Symbol, b, c)]
tx [(Symbol, Expr)]
_  []     []     []     = []
    tx [(Symbol, Expr)]
su (Symbol
x:[Symbol]
xs) (Symbol
y:[Symbol]
ys) (b
t:[b]
ts) = (Symbol
y, Subst -> b -> b
forall a. Subable a => Subst -> a -> a
F.subst ([(Symbol, Expr)] -> Subst
F.mkSubst [(Symbol, Expr)]
su) b
t, c
forall a. Monoid a => a
mempty)
                               (Symbol, b, c) -> [(Symbol, b, c)] -> [(Symbol, b, c)]
forall a. a -> [a] -> [a]
: [(Symbol, Expr)] -> [Symbol] -> [Symbol] -> [b] -> [(Symbol, b, c)]
tx ((Symbol
x, Symbol -> Expr
F.EVar Symbol
y)(Symbol, Expr) -> [(Symbol, Expr)] -> [(Symbol, Expr)]
forall a. a -> [a] -> [a]
:[(Symbol, Expr)]
su) [Symbol]
xs [Symbol]
ys [b]
ts
    tx [(Symbol, Expr)]
_ [Symbol]
_ [Symbol]
_ [b]
_ = Maybe SrcSpan -> String -> [(Symbol, b, c)]
forall a. Maybe SrcSpan -> String -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing String
"PredType.dataConPSpecType.tx called on invalid inputs"
    yts' :: [(Symbol, SpecType, RReft)]
yts'     = [(Symbol, Expr)]
-> [Symbol]
-> [Symbol]
-> [SpecType]
-> [(Symbol, SpecType, RReft)]
forall b c.
(Subable b, Monoid c) =>
[(Symbol, Expr)] -> [Symbol] -> [Symbol] -> [b] -> [(Symbol, b, c)]
tx [] [Symbol]
xs [Symbol]
ys [SpecType]
ts
    ts' :: [(Symbol, SpecType, RReft)]
ts'      = (SpecType -> (Symbol, SpecType, RReft))
-> [SpecType] -> [(Symbol, SpecType, RReft)]
forall a b. (a -> b) -> [a] -> [b]
map (Symbol
"" , , RReft
forall a. Monoid a => a
mempty) [SpecType]
cs [(Symbol, SpecType, RReft)]
-> [(Symbol, SpecType, RReft)] -> [(Symbol, SpecType, RReft)]
forall a. [a] -> [a] -> [a]
++ [(Symbol, SpecType, RReft)]
yts'
    su :: Subst
su       = [(Symbol, Expr)] -> Subst
F.mkSubst [(Symbol
x, Symbol -> Expr
F.EVar Symbol
y) | (Symbol
x, Symbol
y) <- [Symbol] -> [Symbol] -> [(Symbol, Symbol)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Symbol]
xs [Symbol]
ys]
    rt' :: SpecType
rt'      = Subst -> SpecType -> SpecType
forall a. Subable a => Subst -> a -> a
F.subst Subst
su SpecType
rt
    makeVars :: [RTVar RTyVar RSort]
makeVars = (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. Monoid 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)
splitForAllTys (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] -> [RReft] -> [(RTVar RTyVar RSort, RReft)]
forall a b. [a] -> [b] -> [(a, b)]
zip [RTVar RTyVar RSort]
makeVars (RReft -> [RReft]
forall a. a -> [a]
repeat RReft
forall a. Monoid a => a
mempty)

instance PPrint TyConP where
  pprintTidy :: Tidy -> TyConP -> Doc
pprintTidy Tidy
k TyConP
tc = Doc
"data" Doc -> Doc -> Doc
<+> Tidy -> TyCon -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k (TyConP -> TyCon
tcpCon TyConP
tc) 
                           Doc -> Doc -> Doc
<+> Tidy -> [RTyVar] -> Doc
forall a. PPrint a => Tidy -> [a] -> Doc
ppComm     Tidy
k (TyConP -> [RTyVar]
tcpFreeTyVarsTy TyConP
tc) 
                           Doc -> Doc -> Doc
<+> Tidy -> [PVar RSort] -> Doc
forall a. PPrint a => Tidy -> [a] -> Doc
ppComm     Tidy
k (TyConP -> [PVar RSort]
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 :: Tidy -> [a] -> Doc
ppComm Tidy
k = Doc -> Doc
parens (Doc -> Doc) -> ([a] -> Doc) -> [a] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Doc] -> Doc
hsep ([Doc] -> Doc) -> ([a] -> [Doc]) -> [a] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> [Doc] -> [Doc]
punctuate Doc
comma ([Doc] -> [Doc]) -> ([a] -> [Doc]) -> [a] -> [Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Doc) -> [a] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Tidy -> a -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k)


    

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

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

instance Show DataConP where
  show :: DataConP -> String
show = DataConP -> String
forall a. PPrint a => a -> String
showpp

dataConTy :: Monoid r
          => M.HashMap RTyVar (RType RTyCon RTyVar r)
          -> Type -> RType RTyCon RTyVar r
dataConTy :: 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. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
M.lookupDefault (TyVar -> RType RTyCon RTyVar r
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
t1 Type
t2)
  = Symbol
-> RType RTyCon RTyVar r
-> RType RTyCon RTyVar r
-> RType RTyCon RTyVar r
forall r c tv.
Monoid r =>
Symbol -> RType c tv r -> RType c tv r -> RType c tv r
rFun Symbol
F.dummySymbol (HashMap RTyVar (RType RTyCon RTyVar r)
-> Type -> RType RTyCon RTyVar r
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) (HashMap RTyVar (RType RTyCon RTyVar r)
-> Type -> RType RTyCon RTyVar r
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
  = RTVar RTyVar RSort
-> RType RTyCon RTyVar r -> r -> RType RTyCon RTyVar r
forall c tv r. RTVU c tv -> RType c tv r -> r -> RType 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.
Monoid r =>
HashMap RTyVar (RType RTyCon RTyVar r)
-> Type -> RType RTyCon RTyVar r
dataConTy HashMap RTyVar (RType RTyCon RTyVar r)
m Type
t) r
forall a. Monoid a => a
mempty
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.
Monoid 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 a. Monoid a => a
mempty
dataConTy HashMap RTyVar (RType RTyCon RTyVar r)
_ Type
_
  = Maybe SrcSpan -> String -> RType RTyCon RTyVar r
forall a. Maybe SrcSpan -> String -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing String
"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))
  = Reft -> Predicate -> RReft
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''             = [Expr] -> Expr
forall a. Monoid a => [a] -> a
mconcat ([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 t. PVar t -> [(t, Symbol, Expr)]
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 :: PVar t -> (Symbol, [(a, b, Expr)]) -> Expr
pVartoRConc PVar t
p (Symbol
v, [(a, b, Expr)]
args) | [(a, b, Expr)] -> 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 (t :: * -> *) a. Foldable t => t a -> Int
length (PVar t -> [(t, Symbol, Expr)]
forall t. PVar t -> [(t, Symbol, Expr)]
pargs PVar t
p)
  = Symbol -> [Expr] -> Expr
pApp (PVar t -> Symbol
forall t. PVar t -> Symbol
pname PVar t
p) ([Expr] -> Expr) -> [Expr] -> Expr
forall a b. (a -> b) -> a -> b
$ Symbol -> Expr
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
pApp (PVar t -> Symbol
forall t. PVar t -> Symbol
pname PVar t
p) ([Expr] -> Expr) -> [Expr] -> Expr
forall a b. (a -> b) -> a -> b
$ Symbol -> Expr
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 (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 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 :: PVar RSort -> RRType r
pvarRType (PV Symbol
_ PVKind RSort
k {- (PVProp τ) -} Symbol
_ [(RSort, Symbol, Expr)]
args) = PVKind RSort -> [RSort] -> RRType r
forall r tv a.
Reftable r =>
PVKind (RType RTyCon tv a)
-> [RType RTyCon tv a] -> RType RTyCon tv r
rpredType PVKind 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    :: (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 :: 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 = RTyCon
-> [RType RTyCon tv r]
-> [RTProp RTyCon tv r]
-> r
-> RType RTyCon tv r
forall c tv r.
c -> [RType c tv r] -> [RTProp c tv r] -> r -> RType c tv r
RApp RTyCon
predRTyCon  (RType RTyCon tv a -> RType RTyCon tv r
forall b c tv a. Reftable b => RType c tv a -> RType c tv b
uRTypeGen (RType RTyCon tv a -> RType RTyCon tv r)
-> [RType RTyCon tv a] -> [RType 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 a. Monoid a => a
mempty
rpredType PVKind (RType RTyCon tv a)
PVHProp    [RType RTyCon tv a]
ts = RTyCon
-> [RType RTyCon tv r]
-> [RTProp RTyCon tv r]
-> r
-> RType RTyCon tv r
forall c tv r.
c -> [RType c tv r] -> [RTProp c tv r] -> r -> RType c tv r
RApp RTyCon
wpredRTyCon (RType RTyCon tv a -> RType RTyCon tv r
forall b c tv a. Reftable b => RType c tv a -> RType c tv b
uRTypeGen (RType RTyCon tv a -> RType RTyCon tv r)
-> [RType RTyCon tv a] -> [RType RTyCon tv r]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>     [RType RTyCon tv a]
ts) [] r
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 -> [PVar RSort] -> TyConInfo -> RTyCon
RTyCon (Char -> Int -> String -> TyCon
stringTyCon Char
'x' Int
42 (String -> TyCon) -> String -> TyCon
forall a b. (a -> b) -> a -> b
$ Symbol -> String
F.symbolString Symbol
n) [] TyConInfo
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 :: String -> SpecType -> [(PVar RSort, SpecProp)] -> SpecType
replacePreds String
msg                 = (SpecType -> (PVar RSort, SpecProp) -> SpecType)
-> SpecType -> [(PVar RSort, SpecProp)] -> SpecType
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' SpecType -> (PVar RSort, SpecProp) -> SpecType
go
  where
     go :: SpecType -> (PVar RSort, SpecProp) -> SpecType
go SpecType
_ (PVar RSort
_, RProp [(Symbol, RSort)]
_ (RHole RReft
_)) = Maybe SrcSpan -> String -> SpecType
forall a. Maybe SrcSpan -> String -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing String
"replacePreds on RProp _ (RHole _)"
     go SpecType
z (PVar RSort
π, SpecProp
t)                 = String -> (PVar RSort, SpecProp) -> SpecType -> SpecType
substPred String
msg   (PVar RSort
π, SpecProp
t)     SpecType
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

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

substPred :: String -> (PVar RSort, SpecProp) -> SpecType -> SpecType
substPred String
_   (PVar RSort
π, RProp [(Symbol, RSort)]
ss (RVar RTyVar
a1 RReft
r1)) t :: SpecType
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 -> SpecType
forall c tv r. tv -> r -> RType c tv r
RVar RTyVar
a1 (RReft -> SpecType) -> RReft -> SpecType
forall a b. (a -> b) -> a -> b
$ [UsedPVar] -> [(Symbol, RSort)] -> RReft -> RReft -> RReft
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                = Maybe SrcSpan -> String -> SpecType
forall a. Maybe SrcSpan -> String -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing (String
"substPred RVar Var Mismatch" String -> String -> String
forall a. [a] -> [a] -> [a]
++ (RTyVar, RTyVar) -> String
forall a. Show a => a -> String
show (RTyVar
a1, RTyVar
a2))
  | Bool
otherwise                   = SpecType
t
  where
    (RReft
r2', [UsedPVar]
πs)                   = PVar RSort -> RReft -> (RReft, [UsedPVar])
forall t r. PVar t -> UReft r -> (UReft r, [UsedPVar])
splitRPvar PVar RSort
π RReft
r2
    isPredInReft :: Bool
isPredInReft                = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [UsedPVar] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [UsedPVar]
πs

substPred String
msg su :: (PVar RSort, SpecProp)
su@(PVar RSort
π, SpecProp
_ ) (RApp RTyCon
c [SpecType]
ts [SpecProp]
rs RReft
r)
  | [UsedPVar] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [UsedPVar]
πs                     = SpecType
t'
  | Bool
otherwise                   = String
-> (PVar RSort, SpecProp)
-> SpecType
-> [UsedPVar]
-> RReft
-> SpecType
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 ())) =>
String
-> (t, Ref RSort (RType RTyCon tv r))
-> RType RTyCon tv r
-> [PVar t2]
-> r
-> RType RTyCon tv r
substRCon String
msg (PVar RSort, SpecProp)
su SpecType
t' [UsedPVar]
πs RReft
r2'
  where
    t' :: SpecType
t'                          = RTyCon -> [SpecType] -> [SpecProp] -> RReft -> SpecType
forall c tv r.
c -> [RType c tv r] -> [RTProp c tv r] -> r -> RType c tv r
RApp RTyCon
c (String -> (PVar RSort, SpecProp) -> SpecType -> SpecType
substPred String
msg (PVar RSort, SpecProp)
su (SpecType -> SpecType) -> [SpecType] -> [SpecType]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [SpecType]
ts) (String -> (PVar RSort, SpecProp) -> SpecProp -> SpecProp
substPredP String
msg (PVar RSort, SpecProp)
su (SpecProp -> SpecProp) -> [SpecProp] -> [SpecProp]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [SpecProp]
rs) RReft
r
    (RReft
r2', [UsedPVar]
πs)                   = PVar RSort -> RReft -> (RReft, [UsedPVar])
forall t r. PVar t -> UReft r -> (UReft r, [UsedPVar])
splitRPvar PVar RSort
π RReft
r

substPred String
msg (PVar RSort
p, SpecProp
tp) (RAllP (q :: PVar RSort
q@(PV Symbol
_ PVKind RSort
_ Symbol
_ [(RSort, Symbol, Expr)]
_)) SpecType
t)
  | PVar RSort
p PVar RSort -> PVar RSort -> Bool
forall a. Eq a => a -> a -> Bool
/= PVar RSort
q                      = PVar RSort -> SpecType -> SpecType
forall c tv r. PVU c tv -> RType c tv r -> RType c tv r
RAllP PVar RSort
q (SpecType -> SpecType) -> SpecType -> SpecType
forall a b. (a -> b) -> a -> b
$ String -> (PVar RSort, SpecProp) -> SpecType -> SpecType
substPred String
msg (PVar RSort
p, SpecProp
tp) SpecType
t
  | Bool
otherwise                   = PVar RSort -> SpecType -> SpecType
forall c tv r. PVU c tv -> RType c tv r -> RType c tv r
RAllP PVar RSort
q SpecType
t

substPred String
msg (PVar RSort, SpecProp)
su (RAllT RTVar RTyVar RSort
a SpecType
t RReft
r)  = RTVar RTyVar RSort -> SpecType -> RReft -> SpecType
forall c tv r. RTVU c tv -> RType c tv r -> r -> RType c tv r
RAllT RTVar RTyVar RSort
a (String -> (PVar RSort, SpecProp) -> SpecType -> SpecType
substPred String
msg (PVar RSort, SpecProp)
su SpecType
t) RReft
r

substPred String
msg su :: (PVar RSort, SpecProp)
su@(PVar RSort
π,SpecProp
prop) (RFun Symbol
x SpecType
t SpecType
t' RReft
r)
--                        = RFun x (substPred msg su t) (substPred msg su t') r
  | [UsedPVar] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [UsedPVar]
πs                     = Symbol -> SpecType -> SpecType -> RReft -> SpecType
forall c tv r.
Symbol -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun Symbol
x (String -> (PVar RSort, SpecProp) -> SpecType -> SpecType
substPred String
msg (PVar RSort, SpecProp)
su SpecType
t) (String -> (PVar RSort, SpecProp) -> SpecType -> SpecType
substPred String
msg (PVar RSort, SpecProp)
su SpecType
t') RReft
r
  | Bool
otherwise                   =
      let sus :: [Subst]
sus = (\UsedPVar
π -> [(Symbol, Expr)] -> Subst
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
<$> SpecProp -> [(Symbol, RSort)]
forall τ t. Ref τ t -> [(Symbol, τ)]
rf_args SpecProp
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 t. PVar t -> [(t, Symbol, Expr)]
pargs UsedPVar
π))) (UsedPVar -> Subst) -> [UsedPVar] -> [Subst]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [UsedPVar]
πs in
      (SpecType -> Subst -> SpecType) -> SpecType -> [Subst] -> SpecType
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\SpecType
t Subst
su -> SpecType
t SpecType -> SpecType -> SpecType
forall r. Reftable r => r -> r -> r
`F.meet` Subst -> SpecType -> SpecType
forall a. Subable a => Subst -> a -> a
F.subst Subst
su (SpecProp -> SpecType
forall τ t. Ref τ t -> t
rf_body SpecProp
prop)) (Symbol -> SpecType -> SpecType -> RReft -> SpecType
forall c tv r.
Symbol -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun Symbol
x (String -> (PVar RSort, SpecProp) -> SpecType -> SpecType
substPred String
msg (PVar RSort, SpecProp)
su SpecType
t) (String -> (PVar RSort, SpecProp) -> SpecType -> SpecType
substPred String
msg (PVar RSort, SpecProp)
su SpecType
t') RReft
r') [Subst]
sus
  where (RReft
r', [UsedPVar]
πs)                = PVar RSort -> RReft -> (RReft, [UsedPVar])
forall t r. PVar t -> UReft r -> (UReft r, [UsedPVar])
splitRPvar PVar RSort
π RReft
r
-- ps has   , pargs :: ![(t, Symbol, Expr)]

-- AT: just a copy of the other case, mutatis mutandi. (is there a less hacky way?)
substPred String
msg su :: (PVar RSort, SpecProp)
su@(PVar RSort
π,SpecProp
prop) (RImpF Symbol
x SpecType
t SpecType
t' RReft
r)
  | [UsedPVar] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [UsedPVar]
πs                     = Symbol -> SpecType -> SpecType -> RReft -> SpecType
forall c tv r.
Symbol -> RType c tv r -> RType c tv r -> r -> RType c tv r
RImpF Symbol
x (String -> (PVar RSort, SpecProp) -> SpecType -> SpecType
substPred String
msg (PVar RSort, SpecProp)
su SpecType
t) (String -> (PVar RSort, SpecProp) -> SpecType -> SpecType
substPred String
msg (PVar RSort, SpecProp)
su SpecType
t') RReft
r
  | Bool
otherwise                   =
      let sus :: [Subst]
sus = (\UsedPVar
π -> [(Symbol, Expr)] -> Subst
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
<$> SpecProp -> [(Symbol, RSort)]
forall τ t. Ref τ t -> [(Symbol, τ)]
rf_args SpecProp
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 t. PVar t -> [(t, Symbol, Expr)]
pargs UsedPVar
π))) (UsedPVar -> Subst) -> [UsedPVar] -> [Subst]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [UsedPVar]
πs in
      (SpecType -> Subst -> SpecType) -> SpecType -> [Subst] -> SpecType
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\SpecType
t Subst
su -> SpecType
t SpecType -> SpecType -> SpecType
forall r. Reftable r => r -> r -> r
`F.meet` Subst -> SpecType -> SpecType
forall a. Subable a => Subst -> a -> a
F.subst Subst
su (SpecProp -> SpecType
forall τ t. Ref τ t -> t
rf_body SpecProp
prop)) (Symbol -> SpecType -> SpecType -> RReft -> SpecType
forall c tv r.
Symbol -> RType c tv r -> RType c tv r -> r -> RType c tv r
RImpF Symbol
x (String -> (PVar RSort, SpecProp) -> SpecType -> SpecType
substPred String
msg (PVar RSort, SpecProp)
su SpecType
t) (String -> (PVar RSort, SpecProp) -> SpecType -> SpecType
substPred String
msg (PVar RSort, SpecProp)
su SpecType
t') RReft
r') [Subst]
sus
  where (RReft
r', [UsedPVar]
πs)                = PVar RSort -> RReft -> (RReft, [UsedPVar])
forall t r. PVar t -> UReft r -> (UReft r, [UsedPVar])
splitRPvar PVar RSort
π RReft
r



substPred String
msg (PVar RSort, SpecProp)
su (RRTy [(Symbol, SpecType)]
e RReft
r Oblig
o SpecType
t) = [(Symbol, SpecType)] -> RReft -> Oblig -> SpecType -> SpecType
forall c tv r.
[(Symbol, RType c tv r)]
-> r -> Oblig -> RType c tv r -> RType c tv r
RRTy ((SpecType -> SpecType) -> (Symbol, SpecType) -> (Symbol, SpecType)
forall b c a. (b -> c) -> (a, b) -> (a, c)
mapSnd (String -> (PVar RSort, SpecProp) -> SpecType -> SpecType
substPred String
msg (PVar RSort, SpecProp)
su) ((Symbol, SpecType) -> (Symbol, SpecType))
-> [(Symbol, SpecType)] -> [(Symbol, SpecType)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, SpecType)]
e) RReft
r Oblig
o (String -> (PVar RSort, SpecProp) -> SpecType -> SpecType
substPred String
msg (PVar RSort, SpecProp)
su SpecType
t)
substPred String
msg (PVar RSort, SpecProp)
su (RAllE Symbol
x SpecType
t SpecType
t') = Symbol -> SpecType -> SpecType -> SpecType
forall c tv r.
Symbol -> RType c tv r -> RType c tv r -> RType c tv r
RAllE Symbol
x (String -> (PVar RSort, SpecProp) -> SpecType -> SpecType
substPred String
msg (PVar RSort, SpecProp)
su SpecType
t) (String -> (PVar RSort, SpecProp) -> SpecType -> SpecType
substPred String
msg (PVar RSort, SpecProp)
su SpecType
t')
substPred String
msg (PVar RSort, SpecProp)
su (REx Symbol
x SpecType
t SpecType
t')   = Symbol -> SpecType -> SpecType -> SpecType
forall c tv r.
Symbol -> RType c tv r -> RType c tv r -> RType c tv r
REx   Symbol
x (String -> (PVar RSort, SpecProp) -> SpecType -> SpecType
substPred String
msg (PVar RSort, SpecProp)
su SpecType
t) (String -> (PVar RSort, SpecProp) -> SpecType -> SpecType
substPred String
msg (PVar RSort, SpecProp)
su SpecType
t')
substPred String
_   (PVar RSort, SpecProp)
_  SpecType
t              = SpecType
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 :: String
-> (t, Ref RSort (RType RTyCon tv r))
-> RType RTyCon tv r
-> [PVar t2]
-> r
-> RType RTyCon tv r
substRCon String
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 TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== RTyCon -> TyCon
rtc_tc RTyCon
c2 = RTyCon
-> [RType RTyCon tv r]
-> [RTProp RTyCon tv r]
-> r
-> RType RTyCon tv r
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 (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, 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                     = Subst -> [RType RTyCon tv r] -> [RType RTyCon tv r]
forall a. Subable a => Subst -> a -> a
F.subst Subst
su ([RType RTyCon tv r] -> [RType RTyCon tv r])
-> [RType RTyCon tv r] -> [RType RTyCon tv r]
forall a b. (a -> b) -> a -> b
$ String
-> (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.
(?callStack::CallStack) =>
String -> (a -> b -> c) -> [a] -> [b] -> [c]
safeZipWith (String
msg String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": substRCon")  RType RTyCon tv r -> RType RTyCon tv r -> RType RTyCon tv r
forall r. Reftable r => r -> r -> r
strSub  [RType RTyCon tv r]
ts1  [RType RTyCon tv r]
ts2
    rs :: [RTProp RTyCon tv r]
rs                     = Subst -> [RTProp RTyCon tv r] -> [RTProp RTyCon tv r]
forall a. Subable a => Subst -> a -> a
F.subst Subst
su ([RTProp RTyCon tv r] -> [RTProp RTyCon tv r])
-> [RTProp RTyCon tv r] -> [RTProp RTyCon tv r]
forall a b. (a -> b) -> a -> b
$ String
-> (RTProp RTyCon tv r -> RTProp RTyCon tv r -> RTProp RTyCon tv r)
-> [RTProp RTyCon tv r]
-> [RTProp RTyCon tv r]
-> [RTProp RTyCon tv r]
forall a b c.
(?callStack::CallStack) =>
String -> (a -> b -> c) -> [a] -> [b] -> [c]
safeZipWith (String
msg String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": substRCon2") RTProp RTyCon tv r -> RTProp RTyCon tv r -> RTProp RTyCon tv r
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')           = String
-> (RTProp RTyCon tv r -> RTProp RTyCon tv r)
-> [RTProp RTyCon tv r]
-> [RTProp RTyCon tv r]
-> ([RTProp RTyCon tv r], [RTProp RTyCon tv r])
forall a. String -> (a -> a) -> [a] -> [a] -> ([a], [a])
pad String
"substRCon" RTProp RTyCon tv r -> RTProp RTyCon tv r
forall r. Reftable r => r -> r
F.top [RTProp RTyCon tv r]
rs1 [RTProp RTyCon tv r]
rs2
    strSub :: b -> b -> b
strSub b
r1 b
r2           = [PVar t2] -> [(Symbol, RSort)] -> b -> b -> 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 b
r1 b
r2
    strSubR :: Ref τ (RType t1 t2 t3)
-> Ref τ (RType t1 t2 t3) -> Ref τ (RType t1 t2 t3)
strSubR Ref τ (RType t1 t2 t3)
r1 Ref τ (RType t1 t2 t3)
r2          = [PVar t2]
-> [(Symbol, RSort)]
-> Ref τ (RType t1 t2 t3)
-> Ref τ (RType t1 t2 t3)
-> Ref τ (RType t1 t2 t3)
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)
r1 Ref τ (RType t1 t2 t3)
r2

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

    rvs :: RType RTyCon tv r -> [Symbol]
rvs      = Bool
-> (SEnv (RType RTyCon tv r) -> r -> [Symbol] -> [Symbol])
-> [Symbol]
-> RType RTyCon tv r
-> [Symbol]
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 -> r -> Symbol
forall r. Reftable r => r -> Symbol
rvReft r
r Symbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
: [Symbol]
acc) []
    rvReft :: r -> Symbol
rvReft r
r = let F.Reft(Symbol
s,Expr
_) = r -> Reft
forall r. Reftable r => r -> Reft
F.toReft r
r in Symbol
s

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

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


splitRPvar :: PVar t -> UReft r -> (UReft r, [UsedPVar])
splitRPvar :: PVar t -> UReft r -> (UReft r, [UsedPVar])
splitRPvar PVar t
pv (MkUReft r
x (Pr [UsedPVar]
pvs)) = (r -> Predicate -> UReft r
forall r. r -> Predicate -> UReft r
MkUReft r
x ([UsedPVar] -> Predicate
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 t. PVar t -> UsedPVar
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 ()) -> RType t t1 (UReft t2) -> [F.Symbol]
freeArgsPs :: PVar (RType t t1 ()) -> RType t t1 (UReft t2) -> [Symbol]
freeArgsPs PVar (RType t t1 ())
p (RVar t1
_ UReft t2
r)
  = PVar (RType t t1 ()) -> UReft t2 -> [Symbol]
forall t1 t. PVar t1 -> UReft t -> [Symbol]
freeArgsPsRef PVar (RType t t1 ())
p UReft t2
r
freeArgsPs PVar (RType t t1 ())
p (RImpF Symbol
_ RType t t1 (UReft t2)
t1 RType 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
$  PVar (RType t t1 ()) -> UReft t2 -> [Symbol]
forall t1 t. PVar t1 -> UReft t -> [Symbol]
freeArgsPsRef PVar (RType t t1 ())
p UReft t2
r [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ PVar (RType t t1 ()) -> RType t t1 (UReft t2) -> [Symbol]
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 [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ PVar (RType t t1 ()) -> RType t t1 (UReft t2) -> [Symbol]
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 (RFun Symbol
_ RType t t1 (UReft t2)
t1 RType 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
$  PVar (RType t t1 ()) -> UReft t2 -> [Symbol]
forall t1 t. PVar t1 -> UReft t -> [Symbol]
freeArgsPsRef PVar (RType t t1 ())
p UReft t2
r [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ PVar (RType t t1 ()) -> RType t t1 (UReft t2) -> [Symbol]
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 [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ PVar (RType t t1 ()) -> RType t t1 (UReft t2) -> [Symbol]
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)
  = [Symbol] -> [Symbol]
forall a. Eq a => [a] -> [a]
L.nub ([Symbol] -> [Symbol]) -> [Symbol] -> [Symbol]
forall a b. (a -> b) -> a -> b
$  PVar (RType t t1 ()) -> RType t t1 (UReft t2) -> [Symbol]
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 [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ PVar (RType t t1 ()) -> UReft t2 -> [Symbol]
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 PVar (RType t t1 ()) -> PVar (RType t t1 ()) -> Bool
forall a. Eq a => a -> a -> Bool
== PVar (RType t t1 ())
p'   = []
  | Bool
otherwise = PVar (RType t t1 ()) -> RType t t1 (UReft t2) -> [Symbol]
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)
  = [Symbol] -> [Symbol]
forall a. Eq a => [a] -> [a]
L.nub ([Symbol] -> [Symbol]) -> [Symbol] -> [Symbol]
forall a b. (a -> b) -> a -> b
$ PVar (RType t t1 ()) -> UReft t2 -> [Symbol]
forall t1 t. PVar t1 -> UReft t -> [Symbol]
freeArgsPsRef PVar (RType t t1 ())
p UReft t2
r [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ (RType t t1 (UReft t2) -> [Symbol])
-> [RType t t1 (UReft t2)] -> [Symbol]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (PVar (RType t t1 ()) -> RType t t1 (UReft t2) -> [Symbol]
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)
  = [Symbol] -> [Symbol]
forall a. Eq a => [a] -> [a]
L.nub ([Symbol] -> [Symbol]) -> [Symbol] -> [Symbol]
forall a b. (a -> b) -> a -> b
$ PVar (RType t t1 ()) -> RType t t1 (UReft t2) -> [Symbol]
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 [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ PVar (RType t t1 ()) -> RType t t1 (UReft t2) -> [Symbol]
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)
  = [Symbol] -> [Symbol]
forall a. Eq a => [a] -> [a]
L.nub ([Symbol] -> [Symbol]) -> [Symbol] -> [Symbol]
forall a b. (a -> b) -> a -> b
$ PVar (RType t t1 ()) -> RType t t1 (UReft t2) -> [Symbol]
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 [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ PVar (RType t t1 ()) -> RType t t1 (UReft t2) -> [Symbol]
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)
  = [Symbol] -> [Symbol]
forall a. Eq a => [a] -> [a]
L.nub ([Symbol] -> [Symbol]) -> [Symbol] -> [Symbol]
forall a b. (a -> b) -> a -> b
$ PVar (RType t t1 ()) -> UReft t2 -> [Symbol]
forall t1 t. PVar t1 -> UReft t -> [Symbol]
freeArgsPsRef PVar (RType t t1 ())
p UReft t2
r [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ PVar (RType t t1 ()) -> RType t t1 (UReft t2) -> [Symbol]
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 [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ PVar (RType t t1 ()) -> RType t t1 (UReft t2) -> [Symbol]
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)
  = PVar (RType t t1 ()) -> UReft t2 -> [Symbol]
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)
  = [Symbol] -> [Symbol]
forall a. Eq a => [a] -> [a]
L.nub ([Symbol] -> [Symbol]) -> [Symbol] -> [Symbol]
forall a b. (a -> b) -> a -> b
$ (RType t t1 (UReft t2) -> [Symbol])
-> [RType t t1 (UReft t2)] -> [Symbol]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (PVar (RType t t1 ()) -> RType t t1 (UReft t2) -> [Symbol]
forall t t1 t2.
PVar (RType t t1 ()) -> RType t t1 (UReft t2) -> [Symbol]
freeArgsPs PVar (RType t t1 ())
p) ((Symbol, RType t t1 (UReft t2)) -> RType t t1 (UReft t2)
forall a b. (a, b) -> b
snd ((Symbol, RType t t1 (UReft t2)) -> RType t t1 (UReft t2))
-> [(Symbol, RType t t1 (UReft t2))] -> [RType t t1 (UReft t2)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, RType t t1 (UReft t2))]
env) [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ PVar (RType t t1 ()) -> UReft t2 -> [Symbol]
forall t1 t. PVar t1 -> UReft t -> [Symbol]
freeArgsPsRef PVar (RType t t1 ())
p UReft t2
r [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ PVar (RType t t1 ()) -> RType t t1 (UReft t2) -> [Symbol]
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 :: 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 t. PVar t -> [(t, Symbol, Expr)]
pargs [UsedPVar]
ps'),  (Symbol -> Expr
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 t. PVar t -> UsedPVar
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 :: [((), Symbol, Expr)]
pargs = UsedPVar -> [((), Symbol, Expr)]
forall t. PVar t -> [(t, Symbol, Expr)]
pargs UsedPVar
q [((), Symbol, Expr)]
-> [((), Symbol, Expr)] -> [((), Symbol, Expr)]
forall a. [a] -> [a] -> [a]
++ Int -> [((), Symbol, Expr)] -> [((), Symbol, Expr)]
forall a. Int -> [a] -> [a]
drop ([((), Symbol, Expr)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (UsedPVar -> [((), Symbol, Expr)]
forall t. PVar t -> [(t, Symbol, Expr)]
pargs UsedPVar
q)) (UsedPVar -> [((), Symbol, Expr)]
forall t. PVar t -> [(t, Symbol, Expr)]
pargs (UsedPVar -> [((), Symbol, Expr)])
-> UsedPVar -> [((), Symbol, Expr)]
forall a b. (a -> b) -> a -> b
$ PVar t1 -> UsedPVar
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 :: 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 (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' ([(Symbol, RSort)] -> b -> b -> PVar t1 -> b
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 :: 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 = (Ref τ (RType t1 t2 t3) -> PVar t4 -> Ref τ (RType t1 t2 t3))
-> Ref τ (RType t1 t2 t3) -> t (PVar t4) -> Ref τ (RType t1 t2 t3)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' (([(Symbol, b)]
-> Ref τ (RType t1 t2 t3)
-> Ref τ (RType t1 t2 t3)
-> PVar t4
-> Ref τ (RType t1 t2 t3)
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 :: [(Symbol, RSort)] -> r -> r -> PVar t -> r
meetListWithPSub [(Symbol, RSort)]
ss r
r1 r
r2 PVar 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) (PVar t -> [(t, Symbol, Expr)]
forall t. PVar t -> [(t, Symbol, Expr)]
pargs PVar t
π)
  = r
r2 r -> r -> r
forall r. Reftable r => r -> r -> r
`F.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) (PVar t -> [(t, Symbol, Expr)]
forall t. PVar t -> [(t, Symbol, Expr)]
pargs PVar t
π)
  = r
r2 r -> r -> r
forall r. Reftable r => r -> r -> r
`F.meet` (Subst -> r -> r
forall a. Subable a => Subst -> a -> a
F.subst Subst
su r
r1)
  | Bool
otherwise
  = Maybe SrcSpan -> String -> r
forall a. Maybe SrcSpan -> String -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing (String -> r) -> String -> r
forall a b. (a -> b) -> a -> b
$ String
"PredType.meetListWithPSub partial application to " String -> String -> String
forall a. [a] -> [a] -> [a]
++ PVar t -> String
forall a. PPrint a => a -> String
showpp PVar t
π
  where
    su :: Subst
su  = [(Symbol, Expr)] -> Subst
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) (PVar t -> [(t, Symbol, Expr)]
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 :: [(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?
  = Maybe SrcSpan -> String -> Ref τ (RType t t1 t2)
forall a. Maybe SrcSpan -> String -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing String
"PredType.meetListWithPSubRef called with invalid input"
meetListWithPSubRef [(Symbol, b)]
_ Ref τ (RType t t1 t2)
_ (RProp [(Symbol, τ)]
_ (RHole t2
_)) PVar t3
_
  = Maybe SrcSpan -> String -> Ref τ (RType t t1 t2)
forall a. Maybe SrcSpan -> String -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing String
"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
π
  | ((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) (PVar t3 -> [(t3, Symbol, Expr)]
forall t. PVar t -> [(t, Symbol, Expr)]
pargs PVar t3
π)
  = [(Symbol, τ)] -> RType t t1 t2 -> Ref τ (RType t t1 t2)
forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp [(Symbol, τ)]
s1 (RType t t1 t2 -> Ref τ (RType t t1 t2))
-> RType t t1 t2 -> Ref τ (RType t t1 t2)
forall a b. (a -> b) -> a -> b
$ (Subst -> RType t t1 t2 -> RType t t1 t2
forall a. Subable a => Subst -> a -> a
F.subst Subst
su' RType t t1 t2
r2) RType t t1 t2 -> RType t t1 t2 -> RType t t1 t2
forall r. Reftable r => r -> r -> r
`F.meet` RType t t1 t2
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) (PVar t3 -> [(t3, Symbol, Expr)]
forall t. PVar t -> [(t, Symbol, Expr)]
pargs PVar t3
π)
  = [(Symbol, τ)] -> RType t t1 t2 -> Ref τ (RType t t1 t2)
forall τ t. [(Symbol, τ)] -> t -> Ref τ t
RProp [(Symbol, τ)]
s2 (RType t t1 t2 -> Ref τ (RType t t1 t2))
-> RType t t1 t2 -> Ref τ (RType t t1 t2)
forall a b. (a -> b) -> a -> b
$ RType t t1 t2
r2 RType t t1 t2 -> RType t t1 t2 -> RType t t1 t2
forall r. Reftable r => r -> r -> r
`F.meet` (Subst -> RType t t1 t2 -> RType t t1 t2
forall a. Subable a => Subst -> a -> a
F.subst Subst
su RType t t1 t2
r1)
  | Bool
otherwise
  = Maybe SrcSpan -> String -> Ref τ (RType t t1 t2)
forall a. Maybe SrcSpan -> String -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing (String -> Ref τ (RType t t1 t2))
-> String -> Ref τ (RType t t1 t2)
forall a b. (a -> b) -> a -> b
$ String
"PredType.meetListWithPSubRef partial application to " String -> String -> String
forall a. [a] -> [a] -> [a]
++ PVar t3 -> String
forall a. PPrint a => a -> String
showpp PVar t3
π
  where
    su :: Subst
su  = [(Symbol, Expr)] -> Subst
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) (PVar t3 -> [(t3, Symbol, Expr)]
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) <- [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

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 (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 :: (Symbol, Expr) -> f Predicate -> f Predicate
substParg (Symbol
x, Expr
y) = (Predicate -> Predicate) -> f Predicate -> f Predicate
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 Expr -> Expr -> Bool
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 = (Expr -> Expr) -> ((), Symbol, Expr) -> ((), Symbol, Expr)
forall t t3 t1 t2. (t -> t3) -> (t1, t2, t) -> (t1, t2, t3)
mapThd3 Expr -> Expr
fxy (((), Symbol, Expr) -> ((), Symbol, Expr))
-> [((), Symbol, Expr)] -> [((), Symbol, Expr)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> UsedPVar -> [((), Symbol, Expr)]
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 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