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

module Language.Haskell.Liquid.Constraint.Types
  ( -- * Constraint Generation Monad
    CG

    -- * Constraint information
  , CGInfo (..)

    -- * Constraint Generation Environment
  , CGEnv (..)

    -- * Logical constraints (FIXME: related to bounds?)
  , LConstraint (..)

    -- * Fixpoint environment
  , FEnv (..)
  , initFEnv
  , insertsFEnv
  -- , removeFEnv

   -- * Hole Environment
  , HEnv
  , fromListHEnv
  , elemHEnv

   -- * Subtyping Constraints
  , SubC (..)
  , FixSubC

  , subVar

   -- * Well-formedness Constraints
  , WfC (..)
  , FixWfC

   -- * Invariants
  , RTyConInv
  , mkRTyConInv
  , addRTyConInv
  , addRInv

  -- * Aliases?
  , RTyConIAl
  , mkRTyConIAl

  , removeInvariant, restoreInvariant, makeRecInvariants

  , getTemplates

  , getLocation
  ) where

import Prelude hiding (error)
import           Text.PrettyPrint.HughesPJ hiding ((<>))
import qualified Data.HashMap.Strict as M
import qualified Data.HashSet        as S
import qualified Data.List           as L
import           Control.DeepSeq
import           Data.Maybe               (isJust, mapMaybe)
import           Control.Monad.State

import           Language.Haskell.Liquid.GHC.SpanStack
import           Liquid.GHC.API    as Ghc hiding ( (<+>)
                                                                  , vcat
                                                                  , parens
                                                                  , ($+$)
                                                                  )
import           Language.Haskell.Liquid.Misc           (thrd3)
import           Language.Haskell.Liquid.WiredIn        (wiredSortedSyms)
import qualified Language.Fixpoint.Types            as F
import           Language.Fixpoint.Misc

import qualified Language.Haskell.Liquid.UX.CTags      as Tg

import           Language.Haskell.Liquid.Types hiding   (binds)

type CG = State CGInfo

data CGEnv = CGE
  { CGEnv -> SpanStack
cgLoc    :: !SpanStack         -- ^ Location in original source file
  , CGEnv -> REnv
renv     :: !REnv              -- ^ SpecTypes for Bindings in scope
  , CGEnv -> SEnv Var
syenv    :: !(F.SEnv Var)      -- ^ Map from free Symbols (e.g. datacons) to Var
  , CGEnv -> RDEnv
denv     :: !RDEnv             -- ^ Dictionary Environment
  , CGEnv -> SEnv Sort
litEnv   :: !(F.SEnv F.Sort)   -- ^ Global  literals
  , CGEnv -> SEnv Sort
constEnv :: !(F.SEnv F.Sort)   -- ^ Distinct literals
  , CGEnv -> FEnv
fenv   :: !FEnv              -- ^ Fixpoint Environment
  , CGEnv -> HashSet Var
recs   :: !(S.HashSet Var)   -- ^ recursive defs being processed (for annotations)
  , CGEnv -> RTyConInv
invs   :: !RTyConInv         -- ^ Datatype invariants
  , CGEnv -> RTyConInv
rinvs  :: !RTyConInv         -- ^ Datatype recursive invariants: ignored in the base case assumed in rec call
  , CGEnv -> RTyConInv
ial    :: !RTyConIAl         -- ^ Datatype checkable invariants
  , CGEnv -> REnv
grtys  :: !REnv              -- ^ Top-level variables with (assert)-guarantees to verify
  , CGEnv -> REnv
assms  :: !REnv              -- ^ Top-level variables with assumed types
  , CGEnv -> REnv
intys  :: !REnv              -- ^ Top-level variables with auto generated internal types
  , CGEnv -> TCEmb TyCon
emb    :: F.TCEmb Ghc.TyCon   -- ^ How to embed GHC Tycons into fixpoint sorts
  , CGEnv -> TagEnv
tgEnv  :: !Tg.TagEnv          -- ^ Map from top-level binders to fixpoint tag
  , CGEnv -> Maybe Var
tgKey  :: !(Maybe Tg.TagKey)                     -- ^ Current top-level binder
  , CGEnv -> Maybe (HashMap Symbol SpecType)
trec   :: !(Maybe (M.HashMap F.Symbol SpecType)) -- ^ Type of recursive function with decreasing constraints
  , CGEnv -> HashMap Symbol CoreExpr
lcb    :: !(M.HashMap F.Symbol CoreExpr)         -- ^ Let binding that have not been checked (c.f. LAZYVARs)
  , CGEnv -> HashMap Var Expr
forallcb :: !(M.HashMap Var F.Expr)              -- ^ Polymorhic let bindings
  , CGEnv -> HEnv
holes  :: !HEnv                                  -- ^ Types with holes, will need refreshing
  , CGEnv -> LConstraint
lcs    :: !LConstraint                           -- ^ Logical Constraints
  , CGEnv -> Maybe (TError SpecType)
cerr   :: !(Maybe (TError SpecType))             -- ^ error that should be reported at the user
  , CGEnv -> TargetInfo
cgInfo :: !TargetInfo                            -- ^ top-level TargetInfo
  , CGEnv -> Maybe Var
cgVar  :: !(Maybe Var)                           -- ^ top level function being checked
  } -- deriving (Data, Typeable)

instance HasConfig CGEnv where
  getConfig :: CGEnv -> Config
getConfig = forall t. HasConfig t => t -> Config
getConfig forall b c a. (b -> c) -> (a -> b) -> a -> c
. CGEnv -> TargetInfo
cgInfo

newtype LConstraint = LC [[(F.Symbol, SpecType)]]

instance Monoid LConstraint where
  mempty :: LConstraint
mempty  = [[(Symbol, SpecType)]] -> LConstraint
LC []
  mappend :: LConstraint -> LConstraint -> LConstraint
mappend = forall a. Semigroup a => a -> a -> a
(<>)

instance Semigroup LConstraint where
  LC [[(Symbol, SpecType)]]
cs1 <> :: LConstraint -> LConstraint -> LConstraint
<> LC [[(Symbol, SpecType)]]
cs2 = [[(Symbol, SpecType)]] -> LConstraint
LC ([[(Symbol, SpecType)]]
cs1 forall a. [a] -> [a] -> [a]
++ [[(Symbol, SpecType)]]
cs2)

instance PPrint CGEnv where
  pprintTidy :: Tidy -> CGEnv -> Doc
pprintTidy Tidy
k = forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k forall b c a. (b -> c) -> (a -> b) -> a -> c
. CGEnv -> REnv
renv

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

getLocation :: CGEnv -> SrcSpan
getLocation :: CGEnv -> SrcSpan
getLocation = SpanStack -> SrcSpan
srcSpan forall b c a. (b -> c) -> (a -> b) -> a -> c
. CGEnv -> SpanStack
cgLoc

--------------------------------------------------------------------------------
-- | Subtyping Constraints -----------------------------------------------------
--------------------------------------------------------------------------------

-- RJ: what is the difference between these two?

data SubC     = SubC { SubC -> CGEnv
senv  :: !CGEnv
                     , SubC -> SpecType
lhs   :: !SpecType
                     , SubC -> SpecType
rhs   :: !SpecType
                     }
              | SubR { senv  :: !CGEnv
                     , SubC -> Oblig
oblig :: !Oblig
                     , SubC -> RReft
ref   :: !RReft
                     }

data WfC      = WfC  !CGEnv !SpecType
              -- deriving (Data, Typeable)

type FixSubC    = F.SubC Cinfo
type FixWfC     = F.WfC Cinfo
type FixBindEnv = F.BindEnv Cinfo

subVar :: FixSubC -> Maybe Var
subVar :: FixSubC -> Maybe Var
subVar = Cinfo -> Maybe Var
ci_var forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (c :: * -> *) a. TaggedC c a => c a -> a
F.sinfo

instance PPrint SubC where
  pprintTidy :: Tidy -> SubC -> Doc
pprintTidy Tidy
k c :: SubC
c@SubC {} =
    Doc
"The environment:"
    Doc -> Doc -> Doc
$+$
    Doc
""
    Doc -> Doc -> Doc
$+$
    forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k (SubC -> CGEnv
senv SubC
c)
    Doc -> Doc -> Doc
$+$
    Doc
""
    Doc -> Doc -> Doc
$+$
    Doc
"Location: " forall a. Semigroup a => a -> a -> a
<> forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k (CGEnv -> SrcSpan
getLocation (SubC -> CGEnv
senv SubC
c))
    Doc -> Doc -> Doc
$+$
    Doc
"The constraint:"
    Doc -> Doc -> Doc
$+$
    Doc
""
    Doc -> Doc -> Doc
$+$
    Doc
"||-" Doc -> Doc -> Doc
<+> [Doc] -> Doc
vcat [ forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k (SubC -> SpecType
lhs SubC
c)
                   , Doc
"<:"
                   , forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k (SubC -> SpecType
rhs SubC
c) ]

  pprintTidy Tidy
k c :: SubC
c@SubR {} =
    Doc
"The environment:"
    Doc -> Doc -> Doc
$+$
    Doc
""
    Doc -> Doc -> Doc
$+$
    forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k (SubC -> CGEnv
senv SubC
c)
    Doc -> Doc -> Doc
$+$
    Doc
""
    Doc -> Doc -> Doc
$+$
    Doc
"Location: " forall a. Semigroup a => a -> a -> a
<> forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k (CGEnv -> SrcSpan
getLocation (SubC -> CGEnv
senv SubC
c))
    Doc -> Doc -> Doc
$+$
    Doc
"The constraint:"
    Doc -> Doc -> Doc
$+$
    Doc
""
    Doc -> Doc -> Doc
$+$
    Doc
"||-" Doc -> Doc -> Doc
<+> [Doc] -> Doc
vcat [ forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k (SubC -> RReft
ref SubC
c)
                   , Doc -> Doc
parens (forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k (SubC -> Oblig
oblig SubC
c))]

instance PPrint WfC where
  pprintTidy :: Tidy -> WfC -> Doc
pprintTidy Tidy
k (WfC CGEnv
_ SpecType
r) = {- pprintTidy k w <> text -} Doc
"<...> |-" Doc -> Doc -> Doc
<+> forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k SpecType
r


--------------------------------------------------------------------------------
-- | Generation: Types ---------------------------------------------------------
--------------------------------------------------------------------------------
data CGInfo = CGInfo
  { CGInfo -> SEnv Sort
fEnv       :: !(F.SEnv F.Sort)                    -- ^ top-level fixpoint env
  , CGInfo -> [SubC]
hsCs       :: ![SubC]                             -- ^ subtyping constraints over RType
  , CGInfo -> [WfC]
hsWfs      :: ![WfC]                              -- ^ wellformedness constraints over RType
  , CGInfo -> [FixSubC]
fixCs      :: ![FixSubC]                          -- ^ subtyping over Sort (post-splitting)
  , CGInfo -> [FixWfC]
fixWfs     :: ![FixWfC]                           -- ^ wellformedness constraints over Sort (post-splitting)
  , CGInfo -> Integer
freshIndex :: !Integer                            -- ^ counter for generating fresh KVars
  , CGInfo -> FixBindEnv
binds      :: !FixBindEnv                         -- ^ set of environment binders
  , CGInfo -> [Int]
ebinds     :: ![F.BindId]                         -- ^ existentials
  , CGInfo -> AnnInfo (Annot SpecType)
annotMap   :: !(AnnInfo (Annot SpecType))         -- ^ source-position annotation map
  , CGInfo -> TyConMap
tyConInfo  :: !TyConMap                           -- ^ information about type-constructors
  , CGInfo -> HashMap TyCon SpecType
newTyEnv   :: !(M.HashMap Ghc.TyCon SpecType)     -- ^ Mapping of new type type constructors with their refined types.
  , CGInfo -> HashMap Var [Located Expr]
termExprs  :: !(M.HashMap Var [F.Located F.Expr]) -- ^ Terminating Metrics for Recursive functions
  , CGInfo -> HashSet Var
specLVars  :: !(S.HashSet Var)                    -- ^ Set of variables to ignore for termination checking
  , CGInfo -> HashSet Var
specLazy   :: !(S.HashSet Var)                    -- ^ "Lazy binders", skip termination checking
  , CGInfo -> HashSet Var
specTmVars :: !(S.HashSet Var)                    -- ^ Binders that FAILED struct termination check that MUST be checked
  , CGInfo -> HashSet TyCon
autoSize   :: !(S.HashSet Ghc.TyCon)              -- ^ ? FIX THIS
  , CGInfo -> TCEmb TyCon
tyConEmbed :: !(F.TCEmb Ghc.TyCon)                -- ^ primitive Sorts into which TyCons should be embedded
  , CGInfo -> Kuts
kuts       :: !F.Kuts                             -- ^ Fixpoint Kut variables (denoting "back-edges"/recursive KVars)
  , CGInfo -> [HashSet KVar]
kvPacks    :: ![S.HashSet F.KVar]                 -- ^ Fixpoint "packs" of correlated kvars
  , CGInfo -> SEnv Sort
cgLits     :: !(F.SEnv F.Sort)                    -- ^ Global symbols in the refinement logic
  , CGInfo -> SEnv Sort
cgConsts   :: !(F.SEnv F.Sort)                    -- ^ Distinct constant symbols in the refinement logic
  , CGInfo -> [DataDecl]
cgADTs     :: ![F.DataDecl]                       -- ^ ADTs extracted from Haskell 'data' definitions
  , CGInfo -> Bool
tcheck     :: !Bool                               -- ^ Check Termination (?)
  , CGInfo -> Bool
cgiTypeclass :: !Bool                             -- ^ Enable typeclass support
  , CGInfo -> Bool
pruneRefs  :: !Bool                               -- ^ prune unsorted refinements
  , CGInfo -> [TError SpecType]
logErrors  :: ![Error]                            -- ^ Errors during constraint generation
  , CGInfo -> KVProf
kvProf     :: !KVProf                             -- ^ Profiling distribution of KVars
  , CGInfo -> Int
recCount   :: !Int                                -- ^ number of recursive functions seen (for benchmarks)
  , CGInfo -> HashMap Int SrcSpan
bindSpans  :: M.HashMap F.BindId SrcSpan          -- ^ Source Span associated with Fixpoint Binder
  , CGInfo -> Bool
allowHO    :: !Bool
  , CGInfo -> TargetInfo
ghcI       :: !TargetInfo
  , CGInfo -> [(Var, SpecType)]
dataConTys :: ![(Var, SpecType)]                  -- ^ Refined Types of Data Constructors
  , CGInfo -> Templates
unsorted   :: !F.Templates                        -- ^ Potentially unsorted expressions
  }


getTemplates :: CG F.Templates
getTemplates :: CG Templates
getTemplates = do
  Bool
fg    <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets CGInfo -> Bool
pruneRefs
  Templates
ts    <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets CGInfo -> Templates
unsorted
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ if Bool
fg then Templates
F.anything else Templates
ts


instance PPrint CGInfo where
  pprintTidy :: Tidy -> CGInfo -> Doc
pprintTidy = Tidy -> CGInfo -> Doc
pprCGInfo

pprCGInfo :: F.Tidy -> CGInfo -> Doc
pprCGInfo :: Tidy -> CGInfo -> Doc
pprCGInfo Tidy
_k CGInfo
_cgi
  =  Doc
"*********** Constraint Information (omitted) *************"
  -- -$$ (text "*********** Haskell SubConstraints ***********")
  -- -$$ (pprintLongList $ hsCs  cgi)
  -- -$$ (text "*********** Haskell WFConstraints ************")
  -- -$$ (pprintLongList $ hsWfs cgi)
  -- -$$ (text "*********** Fixpoint SubConstraints **********")
  -- -$$ (F.toFix  $ fixCs cgi)
  -- -$$ (text "*********** Fixpoint WFConstraints ************")
  -- -$$ (F.toFix  $ fixWfs cgi)
  -- -$$ (text "*********** Fixpoint Kut Variables ************")
  -- -$$ (F.toFix  $ kuts cgi)
  -- -$$ "*********** Literals in Source     ************"
  -- -$$ F.pprint (cgLits _cgi)
  -- -$$ (text "*********** KVar Distribution *****************")
  -- -$$ (pprint $ kvProf cgi)
  -- -$$ (text "Recursive binders:" <+> pprint (recCount cgi))


--------------------------------------------------------------------------------
-- | Helper Types: HEnv --------------------------------------------------------
--------------------------------------------------------------------------------

newtype HEnv = HEnv (S.HashSet F.Symbol)

fromListHEnv :: [F.Symbol] -> HEnv
fromListHEnv :: [Symbol] -> HEnv
fromListHEnv = HashSet Symbol -> HEnv
HEnv forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList

elemHEnv :: F.Symbol -> HEnv -> Bool
elemHEnv :: Symbol -> HEnv -> Bool
elemHEnv Symbol
x (HEnv HashSet Symbol
s) = Symbol
x forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`S.member` HashSet Symbol
s

--------------------------------------------------------------------------------
-- | Helper Types: Invariants --------------------------------------------------
--------------------------------------------------------------------------------
data RInv = RInv { RInv -> [RRType ()]
_rinv_args :: [RSort]   -- empty list means that the invariant is generic
                                           -- for all type arguments
                 , RInv -> SpecType
_rinv_type :: SpecType
                 , RInv -> Maybe Var
_rinv_name :: Maybe Var
                 } deriving Int -> RInv -> ShowS
[RInv] -> ShowS
RInv -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [RInv] -> ShowS
$cshowList :: [RInv] -> ShowS
show :: RInv -> String
$cshow :: RInv -> String
showsPrec :: Int -> RInv -> ShowS
$cshowsPrec :: Int -> RInv -> ShowS
Show

type RTyConInv = M.HashMap RTyCon [RInv]
type RTyConIAl = M.HashMap RTyCon [RInv]

--------------------------------------------------------------------------------
mkRTyConInv    :: [(Maybe Var, F.Located SpecType)] -> RTyConInv
--------------------------------------------------------------------------------
mkRTyConInv :: [(Maybe Var, Located SpecType)] -> RTyConInv
mkRTyConInv [(Maybe Var, Located SpecType)]
tss = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k [v]
group [ (RTyCon
c, [RRType ()] -> SpecType -> Maybe Var -> RInv
RInv (forall {tv} {c} {r}.
(Eq tv, Eq c) =>
[RType c tv r] -> [RType c tv ()]
go [SpecType]
ts) SpecType
t Maybe Var
v) | (Maybe Var
v, t :: SpecType
t@(RApp RTyCon
c [SpecType]
ts [RTProp RTyCon RTyVar RReft]
_ RReft
_)) <- forall {a} {tv} {c} {r}.
(a, Located (RType tv c r)) -> (a, RType tv c r)
strip forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Maybe Var, Located SpecType)]
tss]
  where
    strip :: (a, Located (RType tv c r)) -> (a, RType tv c r)
strip = forall b c a. (b -> c) -> (a, b) -> (a, c)
mapSnd (forall t1 t2 t3. (t1, t2, t3) -> t3
thrd3 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall tv c r.
RType tv c r
-> ([(RTVar c (RType tv c ()), r)], [PVar (RType tv c ())],
    RType tv c r)
bkUniv forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Located a -> a
val)
    go :: [RType c tv r] -> [RType c tv ()]
go [RType c tv r]
ts | forall {tv} {r} {c}. (Eq tv, Eq r, Eq c) => [RType c tv r] -> Bool
generic (forall c tv r. RType c tv r -> RType c tv ()
toRSort forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RType c tv r]
ts) = []
          | Bool
otherwise                = forall c tv r. RType c tv r -> RType c tv ()
toRSort forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [RType c tv r]
ts

    generic :: [RType c tv r] -> Bool
generic [RType c tv r]
ts = let ts' :: [RType c tv r]
ts' = forall a. Eq a => [a] -> [a]
L.nub [RType c tv r]
ts in
                 forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all forall c tv r. RType c tv r -> Bool
isRVar [RType c tv r]
ts' Bool -> Bool -> Bool
&& forall (t :: * -> *) a. Foldable t => t a -> Int
length [RType c tv r]
ts' forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) a. Foldable t => t a -> Int
length [RType c tv r]
ts

mkRTyConIAl :: [(a, F.Located SpecType)] -> RTyConInv
mkRTyConIAl :: forall a. [(a, Located SpecType)] -> RTyConInv
mkRTyConIAl    = [(Maybe Var, Located SpecType)] -> RTyConInv
mkRTyConInv forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((forall a. Maybe a
Nothing,) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd)

addRTyConInv :: RTyConInv -> SpecType -> SpecType
addRTyConInv :: RTyConInv -> SpecType -> SpecType
addRTyConInv RTyConInv
m SpecType
t
  = case SpecType -> RTyConInv -> Maybe [SpecType]
lookupRInv SpecType
t RTyConInv
m of
      Maybe [SpecType]
Nothing -> SpecType
t
      Just [SpecType]
ts -> forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' SpecType -> SpecType -> SpecType
conjoinInvariantShift SpecType
t [SpecType]
ts

lookupRInv :: SpecType -> RTyConInv -> Maybe [SpecType]
lookupRInv :: SpecType -> RTyConInv -> Maybe [SpecType]
lookupRInv (RApp RTyCon
c [SpecType]
ts [RTProp RTyCon RTyVar RReft]
_ RReft
_) RTyConInv
m
  = case forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup RTyCon
c RTyConInv
m of
      Maybe [RInv]
Nothing   -> forall a. Maybe a
Nothing
      Just [RInv]
invs -> forall a. a -> Maybe a
Just (forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe ([SpecType] -> RInv -> Maybe SpecType
goodInvs [SpecType]
ts) [RInv]
invs)
lookupRInv SpecType
_ RTyConInv
_
  = forall a. Maybe a
Nothing

goodInvs :: [SpecType] -> RInv -> Maybe SpecType
goodInvs :: [SpecType] -> RInv -> Maybe SpecType
goodInvs [SpecType]
_ (RInv []  SpecType
t Maybe Var
_)
  = forall a. a -> Maybe a
Just SpecType
t
goodInvs [SpecType]
ts (RInv [RRType ()]
ts' SpecType
t Maybe Var
_)
  | forall (t :: * -> *). Foldable t => t Bool -> Bool
and (forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith RRType () -> RRType () -> Bool
unifiable [RRType ()]
ts' (forall c tv r. RType c tv r -> RType c tv ()
toRSort forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [SpecType]
ts))
  = forall a. a -> Maybe a
Just SpecType
t
  | Bool
otherwise
  = forall a. Maybe a
Nothing


unifiable :: RSort -> RSort -> Bool
unifiable :: RRType () -> RRType () -> Bool
unifiable RRType ()
t1 RRType ()
t2 = forall a. Maybe a -> Bool
isJust forall a b. (a -> b) -> a -> b
$ Type -> Type -> Maybe TCvSubst
tcUnifyTy (forall r. ToTypeable r => Bool -> RRType r -> Type
toType Bool
False RRType ()
t1) (forall r. ToTypeable r => Bool -> RRType r -> Type
toType Bool
False RRType ()
t2)

addRInv :: RTyConInv -> (Var, SpecType) -> (Var, SpecType)
addRInv :: RTyConInv -> (Var, SpecType) -> (Var, SpecType)
addRInv RTyConInv
m (Var
x, SpecType
t)
  | Var
x forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Var]
ids , Just [SpecType]
invs <- SpecType -> RTyConInv -> Maybe [SpecType]
lookupRInv (forall {c} {tv} {r}. RType c tv r -> RType c tv r
res SpecType
t) RTyConInv
m
  = (Var
x, SpecType -> RReft -> SpecType
addInvCond SpecType
t (forall a. Monoid a => [a] -> a
mconcat forall a b. (a -> b) -> a -> b
$ forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe forall c tv r. RType c tv r -> Maybe r
stripRTypeBase [SpecType]
invs))
  | Bool
otherwise
  = (Var
x, SpecType
t)
   where
     ids :: [Var]
ids = [Var
id' | RTyCon
tc <- forall k v. HashMap k v -> [k]
M.keys RTyConInv
m
               , DataCon
dc <- TyCon -> [DataCon]
Ghc.tyConDataCons forall a b. (a -> b) -> a -> b
$ RTyCon -> TyCon
rtc_tc RTyCon
tc
               , AnId Var
id' <- DataCon -> [TyThing]
Ghc.dataConImplicitTyThings DataCon
dc]
     res :: RType c tv r -> RType c tv r
res = forall c tv r. RTypeRep c tv r -> RType c tv r
ty_res forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall c tv r. RType c tv r -> RTypeRep c tv r
toRTypeRep

conjoinInvariantShift :: SpecType -> SpecType -> SpecType
conjoinInvariantShift :: SpecType -> SpecType -> SpecType
conjoinInvariantShift SpecType
t1 SpecType
t2
  = SpecType -> SpecType -> SpecType
conjoinInvariant SpecType
t1 (forall c (f :: * -> *) tv.
(TyConable c, Reftable (f Reft), Functor f) =>
RType c tv (f Reft) -> Symbol -> RType c tv (f Reft)
shiftVV SpecType
t2 (forall r c tv. Reftable r => RType c tv r -> Symbol
rTypeValueVar SpecType
t1))

conjoinInvariant :: SpecType -> SpecType -> SpecType
conjoinInvariant :: SpecType -> SpecType -> SpecType
conjoinInvariant (RApp RTyCon
c [SpecType]
ts [RTProp RTyCon RTyVar RReft]
rs RReft
r) (RApp RTyCon
ic [SpecType]
its [RTProp RTyCon RTyVar RReft]
_ RReft
ir)
  | RTyCon
c forall a. Eq a => a -> a -> Bool
== RTyCon
ic Bool -> Bool -> Bool
&& forall (t :: * -> *) a. Foldable t => t a -> Int
length [SpecType]
ts forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) a. Foldable t => t a -> Int
length [SpecType]
its
  = forall c tv r.
c -> [RType c tv r] -> [RTProp c tv r] -> r -> RType c tv r
RApp RTyCon
c (forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith SpecType -> SpecType -> SpecType
conjoinInvariantShift [SpecType]
ts [SpecType]
its) [RTProp RTyCon RTyVar RReft]
rs (RReft
r forall r. Reftable r => r -> r -> r
`F.meet` RReft
ir)

conjoinInvariant t :: SpecType
t@(RApp RTyCon
_ [SpecType]
_ [RTProp RTyCon RTyVar RReft]
_ RReft
r) (RVar RTyVar
_ RReft
ir)
  = SpecType
t { rt_reft :: RReft
rt_reft = RReft
r forall r. Reftable r => r -> r -> r
`F.meet` RReft
ir }

conjoinInvariant t :: SpecType
t@(RVar RTyVar
_ RReft
r) (RVar RTyVar
_ RReft
ir)
  = SpecType
t { rt_reft :: RReft
rt_reft = RReft
r forall r. Reftable r => r -> r -> r
`F.meet` RReft
ir }

conjoinInvariant SpecType
t SpecType
_
  = SpecType
t

removeInvariant  :: CGEnv -> CoreBind -> (CGEnv, RTyConInv)
removeInvariant :: CGEnv -> CoreBind -> (CGEnv, RTyConInv)
removeInvariant CGEnv
γ CoreBind
cbs
  = (CGEnv
γ { invs :: RTyConInv
invs  = forall v1 v2 k. (v1 -> v2) -> HashMap k v1 -> HashMap k v2
M.map (forall a. (a -> Bool) -> [a] -> [a]
filter RInv -> Bool
f) (CGEnv -> RTyConInv
invs CGEnv
γ)
       , rinvs :: RTyConInv
rinvs = forall v1 v2 k. (v1 -> v2) -> HashMap k v1 -> HashMap k v2
M.map (forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. RInv -> Bool
f)) (CGEnv -> RTyConInv
invs CGEnv
γ)}
    , CGEnv -> RTyConInv
invs CGEnv
γ)
  where
    f :: RInv -> Bool
f RInv
i | Just Var
v  <- RInv -> Maybe Var
_rinv_name RInv
i, Var
v forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` forall {a}. Bind a -> [a]
binds CoreBind
cbs
        = Bool
False
        | Bool
otherwise
        = Bool
True
    binds :: Bind a -> [a]
binds (NonRec a
x Expr a
_) = [a
x]
    binds (Rec [(a, Expr a)]
xes)    = forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(a, Expr a)]
xes

restoreInvariant :: CGEnv -> RTyConInv -> CGEnv
restoreInvariant :: CGEnv -> RTyConInv -> CGEnv
restoreInvariant CGEnv
γ RTyConInv
is = CGEnv
γ {invs :: RTyConInv
invs = RTyConInv
is}

makeRecInvariants :: CGEnv -> [Var] -> CGEnv
makeRecInvariants :: CGEnv -> [Var] -> CGEnv
makeRecInvariants CGEnv
γ [Var
x] = CGEnv
γ {invs :: RTyConInv
invs = forall k v.
(Eq k, Hashable k) =>
(v -> v -> v) -> HashMap k v -> HashMap k v -> HashMap k v
M.unionWith forall a. [a] -> [a] -> [a]
(++) (CGEnv -> RTyConInv
invs CGEnv
γ) RTyConInv
is}
  where
    is :: RTyConInv
is  =  forall v1 v2 k. (v1 -> v2) -> HashMap k v1 -> HashMap k v2
M.map (forall a b. (a -> b) -> [a] -> [b]
map RInv -> RInv
g forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> Bool) -> [a] -> [a]
filter (forall a. Maybe a -> Bool
isJust forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Var -> Type
varType Var
x Type -> Type -> Maybe TCvSubst
`tcUnifyTy`) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall r. ToTypeable r => Bool -> RRType r -> Type
toType Bool
False forall b c a. (b -> c) -> (a -> b) -> a -> c
. RInv -> SpecType
_rinv_type)) (CGEnv -> RTyConInv
rinvs CGEnv
γ)
    g :: RInv -> RInv
g RInv
i = RInv
i{_rinv_type :: SpecType
_rinv_type = forall {tv}. RType RTyCon tv RReft -> RType RTyCon tv RReft
guard' forall a b. (a -> b) -> a -> b
$ RInv -> SpecType
_rinv_type RInv
i}

    guard' :: RType RTyCon tv RReft -> RType RTyCon tv RReft
guard' (RApp RTyCon
c [RType RTyCon tv RReft]
ts [RTProp RTyCon tv RReft]
rs RReft
r)
      | Just Symbol -> Expr
f <- SizeFun -> Symbol -> Expr
szFun forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TyConInfo -> Maybe SizeFun
sizeFunction (RTyCon -> TyConInfo
rtc_info RTyCon
c)
      = forall c tv r.
c -> [RType c tv r] -> [RTProp c tv r] -> r -> RType c tv r
RApp RTyCon
c [RType RTyCon tv RReft]
ts [RTProp RTyCon tv RReft]
rs (forall r. r -> Predicate -> UReft r
MkUReft ((Symbol -> Expr) -> Reft -> Reft
ref Symbol -> Expr
f forall a b. (a -> b) -> a -> b
$ forall r. Reftable r => r -> Reft
F.toReft RReft
r) forall a. Monoid a => a
mempty)
      | Bool
otherwise
      = forall c tv r.
c -> [RType c tv r] -> [RTProp c tv r] -> r -> RType c tv r
RApp RTyCon
c [RType RTyCon tv RReft]
ts [RTProp RTyCon tv RReft]
rs forall a. Monoid a => a
mempty
    guard' RType RTyCon tv RReft
t
      = RType RTyCon tv RReft
t

    ref :: (Symbol -> Expr) -> Reft -> Reft
ref Symbol -> Expr
f (F.Reft(Symbol
v, Expr
rr))
      = (Symbol, Expr) -> Reft
F.Reft (Symbol
v, Expr -> Expr -> Expr
F.PImp (Brel -> Expr -> Expr -> Expr
F.PAtom Brel
F.Lt (Symbol -> Expr
f Symbol
v) (Symbol -> Expr
f forall a b. (a -> b) -> a -> b
$ forall a. Symbolic a => a -> Symbol
F.symbol Var
x)) Expr
rr)

makeRecInvariants CGEnv
γ [Var]
_ = CGEnv
γ

--------------------------------------------------------------------------------
-- | Fixpoint Environment ------------------------------------------------------
--------------------------------------------------------------------------------

data FEnv = FE
  { FEnv -> IBindEnv
feBinds :: !F.IBindEnv        -- ^ Integer Keys for Fixpoint Environment
  , FEnv -> SEnv Sort
feEnv   :: !(F.SEnv F.Sort)   -- ^ Fixpoint Environment
  , FEnv -> SEnv Int
feIdEnv :: !(F.SEnv F.BindId) -- ^ Map from Symbol to current BindId
  }

insertFEnv :: FEnv -> ((F.Symbol, F.Sort), F.BindId) -> FEnv
insertFEnv :: FEnv -> ((Symbol, Sort), Int) -> FEnv
insertFEnv (FE IBindEnv
benv SEnv Sort
env SEnv Int
ienv) ((Symbol
x, Sort
t), Int
i)
  = IBindEnv -> SEnv Sort -> SEnv Int -> FEnv
FE ([Int] -> IBindEnv -> IBindEnv
F.insertsIBindEnv [Int
i] IBindEnv
benv)
       (forall a. Symbol -> a -> SEnv a -> SEnv a
F.insertSEnv Symbol
x Sort
t      SEnv Sort
env)
       (forall a. Symbol -> a -> SEnv a -> SEnv a
F.insertSEnv Symbol
x Int
i      SEnv Int
ienv)

insertsFEnv :: FEnv -> [((F.Symbol, F.Sort), F.BindId)] -> FEnv
insertsFEnv :: FEnv -> [((Symbol, Sort), Int)] -> FEnv
insertsFEnv = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
L.foldl' FEnv -> ((Symbol, Sort), Int) -> FEnv
insertFEnv

initFEnv :: [(F.Symbol, F.Sort)] -> FEnv
initFEnv :: [(Symbol, Sort)] -> FEnv
initFEnv [(Symbol, Sort)]
xts = IBindEnv -> SEnv Sort -> SEnv Int -> FEnv
FE IBindEnv
benv0 SEnv Sort
env0 forall {a}. SEnv a
ienv0
  where
    benv0 :: IBindEnv
benv0    = IBindEnv
F.emptyIBindEnv
    env0 :: SEnv Sort
env0     = forall a. [(Symbol, a)] -> SEnv a
F.fromListSEnv ([(Symbol, Sort)]
wiredSortedSyms forall a. [a] -> [a] -> [a]
++ [(Symbol, Sort)]
xts)
    ienv0 :: SEnv a
ienv0    = forall {a}. SEnv a
F.emptySEnv

--------------------------------------------------------------------------------
-- | Forcing Strictness --------------------------------------------------------
--------------------------------------------------------------------------------
instance NFData RInv where
  rnf :: RInv -> ()
rnf (RInv [RRType ()]
x SpecType
y Maybe Var
z) = forall a. NFData a => a -> ()
rnf [RRType ()]
x seq :: forall a b. a -> b -> b
`seq` forall a. NFData a => a -> ()
rnf SpecType
y seq :: forall a b. a -> b -> b
`seq` forall a. NFData a => a -> ()
rnf Maybe Var
z

instance NFData CGEnv where
  rnf :: CGEnv -> ()
rnf (CGE SpanStack
x1 REnv
_ SEnv Var
x3 RDEnv
_ SEnv Sort
x4 SEnv Sort
x5 FEnv
x55 HashSet Var
x6 RTyConInv
x7 RTyConInv
x8 RTyConInv
x9 REnv
_ REnv
_ REnv
_ TCEmb TyCon
x10 TagEnv
_ Maybe Var
_ Maybe (HashMap Symbol SpecType)
_ HashMap Symbol CoreExpr
_ HashMap Var Expr
_ HEnv
_ LConstraint
_ Maybe (TError SpecType)
_ TargetInfo
_ Maybe Var
_)
    = SpanStack
x1 seq :: forall a b. a -> b -> b
`seq` {- rnf x2 `seq` -} seq :: forall a b. a -> b -> b
seq SEnv Var
x3
         seq :: forall a b. a -> b -> b
`seq` forall a. NFData a => a -> ()
rnf SEnv Sort
x5
         seq :: forall a b. a -> b -> b
`seq` forall a. NFData a => a -> ()
rnf FEnv
x55
         seq :: forall a b. a -> b -> b
`seq` forall a. NFData a => a -> ()
rnf HashSet Var
x6
         seq :: forall a b. a -> b -> b
`seq` RTyConInv
x7
         seq :: forall a b. a -> b -> b
`seq` forall a. NFData a => a -> ()
rnf RTyConInv
x8
         seq :: forall a b. a -> b -> b
`seq` forall a. NFData a => a -> ()
rnf RTyConInv
x9
         seq :: forall a b. a -> b -> b
`seq` forall a. NFData a => a -> ()
rnf TCEmb TyCon
x10
         seq :: forall a b. a -> b -> b
`seq` forall a. NFData a => a -> ()
rnf SEnv Sort
x4

instance NFData FEnv where
  rnf :: FEnv -> ()
rnf (FE IBindEnv
x1 SEnv Sort
x2 SEnv Int
x3) = forall a. NFData a => a -> ()
rnf IBindEnv
x1 seq :: forall a b. a -> b -> b
`seq` forall a. NFData a => a -> ()
rnf SEnv Sort
x2 seq :: forall a b. a -> b -> b
`seq` forall a. NFData a => a -> ()
rnf SEnv Int
x3

instance NFData SubC where
  rnf :: SubC -> ()
rnf (SubC CGEnv
x1 SpecType
x2 SpecType
x3)
    = forall a. NFData a => a -> ()
rnf CGEnv
x1 seq :: forall a b. a -> b -> b
`seq` forall a. NFData a => a -> ()
rnf SpecType
x2 seq :: forall a b. a -> b -> b
`seq` forall a. NFData a => a -> ()
rnf SpecType
x3
  rnf (SubR CGEnv
x1 Oblig
_ RReft
x2)
    = forall a. NFData a => a -> ()
rnf CGEnv
x1 seq :: forall a b. a -> b -> b
`seq` forall a. NFData a => a -> ()
rnf RReft
x2

instance NFData WfC where
  rnf :: WfC -> ()
rnf (WfC CGEnv
x1 SpecType
x2)
    = forall a. NFData a => a -> ()
rnf CGEnv
x1 seq :: forall a b. a -> b -> b
`seq` forall a. NFData a => a -> ()
rnf SpecType
x2

instance NFData CGInfo where
  rnf :: CGInfo -> ()
rnf CGInfo
x = ({-# SCC "CGIrnf1" #-}  forall a. NFData a => a -> ()
rnf (CGInfo -> [SubC]
hsCs CGInfo
x))       seq :: forall a b. a -> b -> b
`seq`
          ({-# SCC "CGIrnf2" #-}  forall a. NFData a => a -> ()
rnf (CGInfo -> [WfC]
hsWfs CGInfo
x))      seq :: forall a b. a -> b -> b
`seq`
          ({-# SCC "CGIrnf3" #-}  forall a. NFData a => a -> ()
rnf (CGInfo -> [FixSubC]
fixCs CGInfo
x))      seq :: forall a b. a -> b -> b
`seq`
          ({-# SCC "CGIrnf4" #-}  forall a. NFData a => a -> ()
rnf (CGInfo -> [FixWfC]
fixWfs CGInfo
x))     seq :: forall a b. a -> b -> b
`seq`
          ({-# SCC "CGIrnf6" #-}  forall a. NFData a => a -> ()
rnf (CGInfo -> Integer
freshIndex CGInfo
x)) seq :: forall a b. a -> b -> b
`seq`
          ({-# SCC "CGIrnf7" #-}  forall a. NFData a => a -> ()
rnf (CGInfo -> FixBindEnv
binds CGInfo
x))      seq :: forall a b. a -> b -> b
`seq`
          ({-# SCC "CGIrnf8" #-}  forall a. NFData a => a -> ()
rnf (CGInfo -> AnnInfo (Annot SpecType)
annotMap CGInfo
x))   seq :: forall a b. a -> b -> b
`seq`
          ({-# SCC "CGIrnf10" #-} forall a. NFData a => a -> ()
rnf (CGInfo -> Kuts
kuts CGInfo
x))       seq :: forall a b. a -> b -> b
`seq`
          ({-# SCC "CGIrnf10" #-} forall a. NFData a => a -> ()
rnf (CGInfo -> [HashSet KVar]
kvPacks CGInfo
x))    seq :: forall a b. a -> b -> b
`seq`
          ({-# SCC "CGIrnf10" #-} forall a. NFData a => a -> ()
rnf (CGInfo -> SEnv Sort
cgLits CGInfo
x))     seq :: forall a b. a -> b -> b
`seq`
          ({-# SCC "CGIrnf10" #-} forall a. NFData a => a -> ()
rnf (CGInfo -> SEnv Sort
cgConsts CGInfo
x))   seq :: forall a b. a -> b -> b
`seq`
          ({-# SCC "CGIrnf10" #-} forall a. NFData a => a -> ()
rnf (CGInfo -> KVProf
kvProf CGInfo
x))