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

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

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

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

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

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

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

import           Language.Fixpoint.Misc

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

makeTyConInfo :: F.TCEmb Ghc.TyCon -> [Ghc.TyCon] -> [TyConP] -> TyConMap
makeTyConInfo :: TCEmb TyCon -> [TyCon] -> [TyConP] -> TyConMap
makeTyConInfo TCEmb TyCon
tce [TyCon]
fiTcs [TyConP]
tcps = TyConMap
  { tcmTyRTy :: HashMap TyCon RTyCon
tcmTyRTy    = HashMap TyCon RTyCon
tcM
  , tcmFIRTy :: HashMap (TyCon, [Sort]) RTyCon
tcmFIRTy    = HashMap (TyCon, [Sort]) RTyCon
tcInstM
  , tcmFtcArity :: HashMap TyCon Int
tcmFtcArity = HashMap TyCon Int
arities
  }
  where
    tcM :: HashMap TyCon RTyCon
tcM         = [(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     = [Char] -> [(TyCon, Int)] -> HashMap TyCon Int
forall k v.
(?callStack::CallStack, 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. (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' [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. Monoid 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    = RTypeRep RTyCon RTyVar RReft -> RRType RReft
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                 = RRType RReft -> RTypeRep RTyCon RTyVar RReft
forall c tv r. RType c tv r -> RTypeRep c tv r
toRTypeRep RRType RReft
wrT

dataConWorkRep :: DataCon -> SpecRep
dataConWorkRep :: DataCon -> RTypeRep RTyCon RTyVar RReft
dataConWorkRep DataCon
c = RRType RReft -> RTypeRep RTyCon RTyVar RReft
forall c tv r. RType c tv r -> RTypeRep c tv r
toRTypeRep
                 -- . F.tracepp ("DCWR-2: " ++ F.showpp c)
                 (RRType RReft -> RTypeRep RTyCon RTyVar RReft)
-> (DataCon -> RRType RReft)
-> DataCon
-> RTypeRep RTyCon RTyVar RReft
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> RRType RReft
forall r. Monoid 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 -> 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 = xs ++ ty_binds wrapR
          , ty_args  = ts ++ zipWith F.meet ts' (ty_args wrapR)
          , ty_res   = strengthenRType (ty_res workR)    (ty_res  wrapR)
          , ty_preds = ty_preds wrapR
          }
  | Bool
otherwise
  = Maybe SrcSpan -> [Char] -> RTypeRep RTyCon RTyVar RReft
forall a. 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' (RTypeRep RTyCon RTyVar RReft -> [Symbol]
forall c tv r. RTypeRep c tv r -> [Symbol]
ty_binds RTypeRep 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' (RTypeRep RTyCon RTyVar RReft -> [RRType RReft]
forall c tv r. RTypeRep c tv r -> [RType c tv r]
ty_args  RTypeRep RTyCon RTyVar RReft
workR)
    workN :: Int
workN     = [RRType RReft] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length      (RTypeRep RTyCon RTyVar RReft -> [RRType RReft]
forall c tv r. RTypeRep c tv r -> [RType c tv r]
ty_args  RTypeRep RTyCon RTyVar RReft
workR)
    wrapN :: Int
wrapN     = [RRType RReft] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length      (RTypeRep RTyCon RTyVar RReft -> [RRType RReft]
forall c tv r. RTypeRep c tv r -> [RType c tv r]
ty_args  RTypeRep 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 c tv. Reftable r => RType c tv r -> r -> RType c tv r
strengthen RRType RReft
wkT) (RRType RReft -> Maybe RReft
forall c tv r. RType c tv r -> Maybe r
stripRTypeBase RRType RReft
wrT)


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

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 -> [RPVar] -> Doc
forall a. PPrint a => Tidy -> [a] -> Doc
ppComm     Tidy
k (TyConP -> [RPVar]
tcpFreePredTy   TyConP
tc)
      --  (parens $ hsep (punctuate comma (pprintTidy k <$> vs))) <+>
      -- (parens $ hsep (punctuate comma (pprintTidy k <$> ps))) <+>
      -- (parens $ hsep (punctuate comma (pprintTidy k <$> ls)))

ppComm :: PPrint a => F.Tidy -> [a] -> Doc
ppComm :: forall a. PPrint a => Tidy -> [a] -> Doc
ppComm Tidy
k = Doc -> Doc
parens (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 a b. (a -> b) -> [a] -> [b]
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 -> [Char]
show = TyConP -> [Char]
forall a. PPrint a => a -> [Char]
showpp -- showSDoc . ppr

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

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

dataConTy :: Monoid r
          => M.HashMap RTyVar (RType RTyCon RTyVar r)
          -> Type -> RType RTyCon RTyVar r
dataConTy :: forall r.
Monoid r =>
HashMap RTyVar (RType RTyCon RTyVar r)
-> Type -> RType RTyCon RTyVar r
dataConTy HashMap RTyVar (RType RTyCon RTyVar r)
m (TyVarTy TyVar
v)
  = 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 FunTyFlag
_ Type
_ 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
α ForAllTyFlag
_) 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 -> [Char] -> RType RTyCon RTyVar r
forall a. 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))
  = 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 :: 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 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 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 t. PVar t -> [(t, Symbol, Expr)]
pargs PVar t
p)

-----------------------------------------------------------------------
-- | @pvarRType π@ returns a trivial @RType@ corresponding to the
--   function signature for a @PVar@ @π@. For example, if
--      @π :: T1 -> T2 -> T3 -> Prop@
--   then @pvarRType π@ returns an @RType@ with an @RTycon@ called
--   @predRTyCon@ `RApp predRTyCon [T1, T2, T3]`
-----------------------------------------------------------------------
pvarRType :: (PPrint r, F.Reftable r) => PVar RSort -> RRType r
-----------------------------------------------------------------------
pvarRType :: forall r. (PPrint r, Reftable r) => RPVar -> RRType r
pvarRType (PV Symbol
_ PVKind RSort
k {- (PVProp τ) -} Symbol
_ [(RSort, Symbol, Expr)]
args) = PVKind RSort -> [RSort] -> RType RTyCon RTyVar 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 :: forall r tv a.
Reftable r =>
PVKind (RType RTyCon tv a)
-> [RType RTyCon tv a] -> RType RTyCon tv r
rpredType (PVProp RType RTyCon tv a
t) [RType RTyCon tv a]
ts = 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 -> [RPVar] -> TyConInfo -> RTyCon
RTyCon (Char -> Int -> [Char] -> TyCon
stringTyCon Char
'x' Int
42 ([Char] -> TyCon) -> [Char] -> TyCon
forall a b. (a -> b) -> a -> b
$ Symbol -> [Char]
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 :: [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. 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 :: PVar BSort -> PVar BSort -> BareType -> BareType
-------------------------------------------------------------------------------------
substPVar :: PVar BSort -> PVar BSort -> BareType -> BareType
substPVar PVar BSort
src PVar BSort
dst = BareType -> BareType
go
  where
    go :: BareType -> BareType
    go :: BareType -> BareType
go (RVar BTyVar
a RReft
r)         = BTyVar -> RReft -> BareType
forall c tv r. tv -> r -> RType c tv r
RVar BTyVar
a (RReft -> RReft
goRR RReft
r)
    go (RApp BTyCon
c [BareType]
ts [RTProp BTyCon BTyVar RReft]
rs RReft
r)   = BTyCon
-> [BareType] -> [RTProp BTyCon BTyVar RReft] -> RReft -> BareType
forall c tv r.
c -> [RType c tv r] -> [RTProp c tv r] -> r -> RType c tv r
RApp BTyCon
c (BareType -> BareType
go (BareType -> BareType) -> [BareType] -> [BareType]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [BareType]
ts) (RTProp BTyCon BTyVar RReft -> RTProp BTyCon BTyVar RReft
goR (RTProp BTyCon BTyVar RReft -> RTProp BTyCon BTyVar RReft)
-> [RTProp BTyCon BTyVar RReft] -> [RTProp BTyCon BTyVar RReft]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RTProp BTyCon BTyVar RReft]
rs) (RReft -> RReft
goRR RReft
r)
    go (RAllP PVar BSort
q BareType
t)
     | PVar BSort -> Symbol
forall t. PVar t -> Symbol
pname PVar BSort
q Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== PVar BSort -> Symbol
forall t. PVar t -> Symbol
pname PVar BSort
src = PVar BSort -> BareType -> BareType
forall c tv r. PVU c tv -> RType c tv r -> RType c tv r
RAllP PVar BSort
q BareType
t
     | Bool
otherwise            = PVar BSort -> BareType -> BareType
forall c tv r. PVU c tv -> RType c tv r -> RType c tv r
RAllP PVar BSort
q (BareType -> BareType
go BareType
t)
    go (RAllT RTVU BTyCon BTyVar
a BareType
t RReft
r)      = RTVU BTyCon BTyVar -> BareType -> RReft -> BareType
forall c tv r. RTVU c tv -> RType c tv r -> r -> RType c tv r
RAllT RTVU BTyCon BTyVar
a   (BareType -> BareType
go BareType
t)  (RReft -> RReft
goRR RReft
r)
    go (RFun Symbol
x RFInfo
i BareType
t BareType
t' RReft
r)  = Symbol -> RFInfo -> BareType -> BareType -> RReft -> BareType
forall c tv r.
Symbol
-> RFInfo -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun Symbol
x RFInfo
i  (BareType -> BareType
go BareType
t)  (BareType -> BareType
go BareType
t') (RReft -> RReft
goRR RReft
r)
    go (RAllE Symbol
x BareType
t BareType
t')     = Symbol -> BareType -> BareType -> BareType
forall c tv r.
Symbol -> RType c tv r -> RType c tv r -> RType c tv r
RAllE Symbol
x   (BareType -> BareType
go BareType
t)  (BareType -> BareType
go BareType
t')
    go (REx Symbol
x BareType
t BareType
t')       = Symbol -> BareType -> BareType -> BareType
forall c tv r.
Symbol -> RType c tv r -> RType c tv r -> RType c tv r
REx Symbol
x     (BareType -> BareType
go BareType
t)  (BareType -> BareType
go BareType
t')
    go (RRTy [(Symbol, BareType)]
e RReft
r Oblig
o BareType
rt)    = [(Symbol, BareType)] -> RReft -> Oblig -> BareType -> BareType
forall c tv r.
[(Symbol, RType c tv r)]
-> r -> Oblig -> RType c tv r -> RType c tv r
RRTy [(Symbol, BareType)]
e'   (RReft -> RReft
goRR RReft
r) Oblig
o (BareType -> BareType
go BareType
rt) where e' :: [(Symbol, BareType)]
e' = [(Symbol
x, BareType -> BareType
go BareType
t) | (Symbol
x, BareType
t) <- [(Symbol, BareType)]
e]
    go (RAppTy BareType
t1 BareType
t2 RReft
r)   = BareType -> BareType -> RReft -> BareType
forall c tv r. RType c tv r -> RType c tv r -> r -> RType c tv r
RAppTy    (BareType -> BareType
go BareType
t1) (BareType -> BareType
go BareType
t2) (RReft -> RReft
goRR RReft
r)
    go (RHole RReft
r)          = RReft -> BareType
forall c tv r. r -> RType c tv r
RHole     (RReft -> RReft
goRR RReft
r)
    go t :: BareType
t@(RExprArg  Located Expr
_)    = BareType
t
    goR :: BRProp RReft -> BRProp RReft
    goR :: RTProp BTyCon BTyVar RReft -> RTProp BTyCon BTyVar RReft
goR RTProp BTyCon BTyVar RReft
rp = RTProp BTyCon BTyVar RReft
rp {rf_body = go (rf_body rp) }
    goRR :: RReft -> RReft
    goRR :: RReft -> RReft
goRR RReft
rr = RReft
rr { ur_pred = goP (ur_pred rr) }
    goP :: Predicate -> Predicate
    goP :: Predicate -> Predicate
goP (Pr [UsedPVar]
ps) = [UsedPVar] -> Predicate
Pr (UsedPVar -> UsedPVar
goPV (UsedPVar -> UsedPVar) -> [UsedPVar] -> [UsedPVar]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [UsedPVar]
ps)
    goPV :: UsedPVar -> UsedPVar
    goPV :: UsedPVar -> UsedPVar
goPV UsedPVar
pv
      | UsedPVar -> Symbol
forall t. PVar t -> Symbol
pname UsedPVar
pv Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== PVar BSort -> Symbol
forall t. PVar t -> Symbol
pname PVar BSort
src = UsedPVar
pv { pname = pname dst }
      | Bool
otherwise             = UsedPVar
pv

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

substPred :: [Char]
-> (RPVar, Ref RSort (RRType RReft))
-> RRType RReft
-> RRType RReft
substPred [Char]
_   (RPVar
rp, RProp [(Symbol, RSort)]
ss (RVar RTyVar
a1 RReft
r1)) t :: RRType RReft
t@(RVar RTyVar
a2 RReft
r2)
  | Bool
isPredInReft Bool -> Bool -> Bool
&& RTyVar
a1 RTyVar -> RTyVar -> Bool
forall a. Eq a => a -> a -> Bool
== RTyVar
a2    = RTyVar -> RReft -> RRType RReft
forall c tv r. tv -> r -> RType 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, Reftable 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. 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, Reftable r, Hashable tv, PPrint tv,
 PPrint r, SubsTy tv (RType RTyCon tv ()) r,
 SubsTy tv (RType RTyCon tv ()) (RType RTyCon tv ()),
 SubsTy tv (RType RTyCon tv ()) RTyCon,
 SubsTy tv (RType RTyCon tv ()) tv, Reftable (RType RTyCon tv r),
 SubsTy tv (RType RTyCon tv ()) (RTVar tv (RType RTyCon tv ())),
 FreeVar RTyCon tv, Reftable (RTProp RTyCon tv r),
 Reftable (RTProp RTyCon tv ())) =>
[Char]
-> (t, Ref RSort (RType RTyCon tv r))
-> RType RTyCon tv r
-> [PVar t2]
-> r
-> RType RTyCon tv r
substRCon [Char]
msg (RPVar, Ref RSort (RRType RReft))
su RRType RReft
t' [UsedPVar]
πs RReft
r2'
  where
    t' :: RRType RReft
t'                          = RTyCon
-> [RRType RReft]
-> [Ref RSort (RRType RReft)]
-> RReft
-> RRType RReft
forall c tv r.
c -> [RType c tv r] -> [RTProp c tv r] -> r -> RType c tv r
RApp RTyCon
c ([Char]
-> (RPVar, Ref RSort (RRType RReft))
-> RRType RReft
-> RRType RReft
substPred [Char]
msg (RPVar, Ref RSort (RRType RReft))
su (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 c tv r. PVU c tv -> RType c tv r -> RType 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 c tv r. PVU c tv -> RType c tv r -> RType c tv r
RAllP RPVar
q RRType RReft
t

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

substPred [Char]
msg su :: (RPVar, Ref RSort (RRType RReft))
su@(RPVar
rp,Ref RSort (RRType RReft)
prop) (RFun Symbol
x RFInfo
i RRType RReft
rt RRType RReft
rt' RReft
r)
--                        = RFun x (substPred msg su t) (substPred msg su t') r
  | [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 c tv r.
Symbol
-> RFInfo -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun Symbol
x RFInfo
i ([Char]
-> (RPVar, Ref RSort (RRType RReft))
-> RRType RReft
-> RRType RReft
substPred [Char]
msg (RPVar, Ref RSort (RRType RReft))
su RRType RReft
rt) ([Char]
-> (RPVar, Ref RSort (RRType RReft))
-> RRType RReft
-> RRType RReft
substPred [Char]
msg (RPVar, Ref RSort (RRType RReft))
su RRType RReft
rt') RReft
r
  | Bool
otherwise                   =
      let sus :: [Subst]
sus = (\UsedPVar
π -> [(Symbol, Expr)] -> Subst
F.mkSubst ([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 τ t. Ref τ t -> [(Symbol, τ)]
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 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
      (RRType RReft -> Subst -> RRType RReft)
-> RRType RReft -> [Subst] -> 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 Subst
subst -> RRType RReft
t RRType RReft -> RRType RReft -> RRType RReft
forall r. Reftable r => r -> r -> r
`F.meet` Subst -> RRType RReft -> RRType RReft
forall a. Subable a => Subst -> a -> a
F.subst Subst
subst (Ref RSort (RRType RReft) -> RRType RReft
forall τ t. Ref τ t -> t
rf_body Ref RSort (RRType RReft)
prop)) (Symbol
-> RFInfo -> RRType RReft -> RRType RReft -> RReft -> RRType RReft
forall c tv r.
Symbol
-> RFInfo -> RType c tv r -> RType c tv r -> r -> RType c tv r
RFun Symbol
x RFInfo
i ([Char]
-> (RPVar, Ref RSort (RRType RReft))
-> RRType RReft
-> RRType RReft
substPred [Char]
msg (RPVar, Ref RSort (RRType RReft))
su RRType RReft
rt) ([Char]
-> (RPVar, Ref RSort (RRType RReft))
-> RRType RReft
-> RRType RReft
substPred [Char]
msg (RPVar, Ref RSort (RRType RReft))
su RRType RReft
rt') RReft
r') [Subst]
sus
  where (RReft
r', [UsedPVar]
πs)                = 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 c tv r.
[(Symbol, RType c tv r)]
-> r -> Oblig -> RType c tv r -> RType c tv r
RRTy ((RRType RReft -> RRType RReft)
-> (Symbol, RRType RReft) -> (Symbol, RRType RReft)
forall b c a. (b -> c) -> (a, b) -> (a, c)
mapSnd ([Char]
-> (RPVar, Ref RSort (RRType RReft))
-> RRType RReft
-> RRType RReft
substPred [Char]
msg (RPVar, Ref RSort (RRType RReft))
su) ((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 c tv r.
Symbol -> RType c tv r -> RType c tv r -> RType c tv r
RAllE Symbol
x ([Char]
-> (RPVar, Ref RSort (RRType RReft))
-> RRType RReft
-> RRType RReft
substPred [Char]
msg (RPVar, Ref RSort (RRType RReft))
su RRType RReft
t) ([Char]
-> (RPVar, Ref RSort (RRType RReft))
-> RRType RReft
-> RRType RReft
substPred [Char]
msg (RPVar, Ref RSort (RRType RReft))
su RRType RReft
t')
substPred [Char]
msg (RPVar, Ref RSort (RRType RReft))
su (REx Symbol
x RRType RReft
t RRType RReft
t')   = Symbol -> RRType RReft -> RRType RReft -> RRType RReft
forall c tv r.
Symbol -> RType c tv r -> RType c tv r -> RType c tv r
REx   Symbol
x ([Char]
-> (RPVar, Ref RSort (RRType RReft))
-> RRType RReft
-> RRType RReft
substPred [Char]
msg (RPVar, Ref RSort (RRType RReft))
su RRType RReft
t) ([Char]
-> (RPVar, Ref RSort (RRType RReft))
-> RRType RReft
-> RRType RReft
substPred [Char]
msg (RPVar, Ref RSort (RRType RReft))
su RRType RReft
t')
substPred [Char]
_   (RPVar, Ref RSort (RRType RReft))
_  RRType RReft
t              = RRType RReft
t

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

substRCon
  :: (PPrint t, PPrint t2, Eq tv, F.Reftable r, Hashable tv, PPrint tv, PPrint r,
      SubsTy tv (RType RTyCon tv ()) r,
      SubsTy tv (RType RTyCon tv ()) (RType RTyCon tv ()),
      SubsTy tv (RType RTyCon tv ()) RTyCon,
      SubsTy tv (RType RTyCon tv ()) tv,
      F.Reftable (RType RTyCon tv r),
      SubsTy tv (RType RTyCon tv ()) (RTVar tv (RType RTyCon tv ())),
      FreeVar RTyCon tv,
      F.Reftable (RTProp RTyCon tv r),
      F.Reftable (RTProp RTyCon tv ()))
  => [Char]
  -> (t, Ref RSort (RType RTyCon tv r))
  -> RType RTyCon tv r
  -> [PVar t2]
  -> r
  -> RType RTyCon tv r
substRCon :: forall t t2 tv r.
(PPrint t, PPrint t2, Eq tv, Reftable r, Hashable tv, PPrint tv,
 PPrint r, SubsTy tv (RType RTyCon tv ()) r,
 SubsTy tv (RType RTyCon tv ()) (RType RTyCon tv ()),
 SubsTy tv (RType RTyCon tv ()) RTyCon,
 SubsTy tv (RType RTyCon tv ()) tv, Reftable (RType RTyCon tv r),
 SubsTy tv (RType RTyCon tv ()) (RTVar tv (RType RTyCon tv ())),
 FreeVar RTyCon tv, Reftable (RTProp RTyCon tv r),
 Reftable (RTProp RTyCon tv ())) =>
[Char]
-> (t, Ref RSort (RType RTyCon tv r))
-> RType RTyCon tv r
-> [PVar t2]
-> r
-> RType RTyCon tv r
substRCon [Char]
msg (t
_, RProp [(Symbol, RSort)]
ss t1 :: RType RTyCon tv r
t1@(RApp RTyCon
c1 [RType RTyCon tv r]
ts1 [RTProp RTyCon tv r]
rs1 r
r1)) t2 :: RType RTyCon tv r
t2@(RApp RTyCon
c2 [RType RTyCon tv r]
ts2 [RTProp RTyCon tv r]
rs2 r
_) [PVar t2]
πs r
r2'
  | RTyCon -> TyCon
rtc_tc RTyCon
c1 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
$ [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.
(?callStack::CallStack) =>
[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 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
$ [Char]
-> (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) =>
[Char] -> (a -> b -> c) -> [a] -> [b] -> [c]
safeZipWith ([Char]
msg [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
": substRCon2") RTProp RTyCon tv r -> RTProp RTyCon tv r -> RTProp RTyCon tv r
forall {t1} {t2} {t3} {τ}.
(TyConable t1, PPrint t2, PPrint t1, PPrint t3, Reftable t3,
 Reftable (RType t1 t2 t3), Reftable (RTProp t1 t2 t3),
 Reftable (RTProp t1 t2 ()), Hashable t2, FreeVar t1 t2,
 SubsTy t2 (RType t1 t2 ()) t1, SubsTy t2 (RType t1 t2 ()) t3,
 SubsTy t2 (RType t1 t2 ()) t2,
 SubsTy t2 (RType t1 t2 ()) (RType t1 t2 ()),
 SubsTy t2 (RType t1 t2 ()) (RTVar t2 (RType t1 t2 ()))) =>
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')           = [Char]
-> (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. [Char] -> (a -> a) -> [a] -> [a] -> ([a], [a])
pad [Char]
"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
x 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
x b
r2
    strSubR :: Ref τ (RType t1 t2 t3)
-> Ref τ (RType t1 t2 t3) -> Ref τ (RType t1 t2 t3)
strSubR Ref τ (RType t1 t2 t3)
x Ref τ (RType t1 t2 t3)
r2          = [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)
x 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 {p}. Reftable p => p -> Symbol
rvReft r
r Symbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
: [Symbol]
acc) []
    rvReft :: p -> Symbol
rvReft p
r = let F.Reft(Symbol
s,Expr
_) = p -> Reft
forall r. Reftable r => r -> Reft
F.toReft p
r in Symbol
s

substRCon [Char]
msg (t, Ref RSort (RType RTyCon tv r))
su RType RTyCon tv r
t [PVar t2]
_ r
_        = {- panic Nothing -} [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. 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. 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 τ t. [(Symbol, τ)] -> t -> Ref τ 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 τ t. [(Symbol, τ)] -> t -> Ref τ 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 ()) -> 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 -> 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 :: forall t t1 t2.
PVar (RType t t1 ()) -> RType t t1 (UReft t2) -> [Symbol]
freeArgsPs PVar (RType t t1 ())
p (RVar t1
_ UReft t2
r)
  = 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 (RFun Symbol
_ RFInfo
_ 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 :: 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 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 = pargs q ++ drop (length (pargs q)) (pargs $ uPVar p)}

meetListWithPSubs :: (Foldable t, PPrint t1, F.Reftable b)
                  => t (PVar t1) -> [(F.Symbol, RSort)] -> b -> b -> b
meetListWithPSubs :: forall (t :: * -> *) t1 b.
(Foldable t, PPrint t1, Reftable b) =>
t (PVar t1) -> [(Symbol, RSort)] -> b -> b -> b
meetListWithPSubs t (PVar t1)
πs [(Symbol, RSort)]
ss b
r1 b
r2    = (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 r t.
(Reftable r, PPrint t) =>
[(Symbol, RSort)] -> r -> r -> PVar t -> r
meetListWithPSub [(Symbol, RSort)]
ss b
r1) b
r2 t (PVar t1)
πs

meetListWithPSubsRef :: (Foldable t, F.Reftable (RType t1 t2 t3))
                     => t (PVar t4)
                     -> [(F.Symbol, b)]
                     -> Ref τ (RType t1 t2 t3)
                     -> Ref τ (RType t1 t2 t3)
                     -> Ref τ (RType t1 t2 t3)
meetListWithPSubsRef :: forall (t :: * -> *) t1 t2 t3 t4 b τ.
(Foldable t, Reftable (RType t1 t2 t3)) =>
t (PVar t4)
-> [(Symbol, b)]
-> Ref τ (RType t1 t2 t3)
-> Ref τ (RType t1 t2 t3)
-> Ref τ (RType t1 t2 t3)
meetListWithPSubsRef t (PVar t4)
πs [(Symbol, b)]
ss Ref τ (RType t1 t2 t3)
r1 Ref τ (RType t1 t2 t3)
r2 = (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 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 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 :: forall r t.
(Reftable r, PPrint t) =>
[(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 -> [Char] -> r
forall a. 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]
++ PVar t -> [Char]
forall a. PPrint a => a -> [Char]
showpp PVar t
π
  where
    su :: Subst
su  = [(Symbol, Expr)] -> Subst
F.mkSubst [(Symbol
x, Expr
y) | (Symbol
x, (t
_, Symbol
_, Expr
y)) <- [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 :: forall t t1 t2 b τ t3.
Reftable (RType t t1 t2) =>
[(Symbol, b)]
-> Ref τ (RType t t1 t2)
-> Ref τ (RType t t1 t2)
-> PVar t3
-> Ref τ (RType t t1 t2)
meetListWithPSubRef [(Symbol, b)]
_ (RProp [(Symbol, τ)]
_ (RHole t2
_)) Ref τ (RType t t1 t2)
_ PVar t3
_ -- TODO: Is this correct?
  = Maybe SrcSpan -> [Char] -> Ref τ (RType t t1 t2)
forall a. Maybe SrcSpan -> [Char] -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing [Char]
"PredType.meetListWithPSubRef called with invalid input"
meetListWithPSubRef [(Symbol, b)]
_ Ref τ (RType t t1 t2)
_ (RProp [(Symbol, τ)]
_ (RHole t2
_)) PVar t3
_
  = Maybe SrcSpan -> [Char] -> Ref τ (RType t t1 t2)
forall a. 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 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 -> [Char] -> Ref τ (RType t t1 t2)
forall a. Maybe SrcSpan -> [Char] -> a
panic Maybe SrcSpan
forall a. Maybe a
Nothing ([Char] -> Ref τ (RType t t1 t2))
-> [Char] -> Ref τ (RType t t1 t2)
forall a b. (a -> b) -> a -> b
$ [Char]
"PredType.meetListWithPSubRef partial application to " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ PVar t3 -> [Char]
forall a. PPrint a => a -> [Char]
showpp PVar t3
π
  where
    su :: Subst
su  = [(Symbol, Expr)] -> Subst
F.mkSubst [(Symbol
x, Expr
y) | (Symbol
x, (t3
_, Symbol
_, Expr
y)) <- [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 :: forall (f :: * -> *).
Functor f =>
(Symbol, Expr) -> f Predicate -> f Predicate
substParg (Symbol
x, Expr
y) = (Predicate -> Predicate) -> f Predicate -> f Predicate
forall a b. (a -> b) -> f a -> f b
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 = 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